c This Formular is generated by mcnf
c
c    horn? no 
c    forced? no 
c    mixed sat? no 
c    clause length = 3 
c
p cnf 150  645 
 23 -41 59 0
145 52 -86 0
-92 -130 88 0
-110 -97 144 0
-104 2 90 0
-17 -39 110 0
133 -81 -113 0
-18 70 -111 0
-112 20 54 0
130 -110 37 0
-137 124 91 0
-7 -32 -108 0
100 118 6 0
18 -34 -84 0
-106 118 51 0
-44 -23 130 0
-11 -125 60 0
54 -43 127 0
124 122 83 0
-148 39 48 0
34 98 17 0
-41 -121 145 0
-26 107 -106 0
-101 88 -136 0
-141 -48 -31 0
14 -70 119 0
57 26 -1 0
98 35 -89 0
-133 -114 32 0
-102 -98 88 0
68 -91 -129 0
66 -27 -140 0
-48 -25 33 0
-79 61 -10 0
-150 -130 -64 0
-147 29 82 0
-89 130 79 0
-77 -94 -31 0
5 -8 19 0
131 118 -27 0
-36 51 -17 0
-19 115 -61 0
-103 -119 -49 0
-92 -82 -135 0
8 -76 -70 0
22 -5 25 0
120 -140 15 0
136 39 -26 0
-12 113 -35 0
98 -80 55 0
141 136 29 0
-65 143 -140 0
136 8 -115 0
-115 53 99 0
129 146 100 0
-58 5 48 0
-87 84 -65 0
-3 148 -94 0
103 -123 -38 0
72 -100 -82 0
-84 -41 -99 0
-53 -63 52 0
-54 -141 61 0
133 -61 43 0
106 33 -114 0
-131 -137 80 0
-20 26 99 0
40 -4 -73 0
19 -22 35 0
144 16 -13 0
-11 56 97 0
-138 43 -85 0
99 -68 102 0
14 123 86 0
-98 5 85 0
71 -45 -59 0
76 123 124 0
108 8 70 0
123 -43 146 0
127 -39 10 0
-64 -70 89 0
55 12 -47 0
-30 130 -114 0
-122 12 -35 0
-123 -46 14 0
-26 -21 83 0
-39 48 31 0
41 105 33 0
147 -25 84 0
6 -113 49 0
-32 -122 26 0
133 125 -66 0
-65 -101 -95 0
-19 -101 22 0
105 136 126 0
9 -36 -42 0
-53 -132 102 0
109 60 111 0
51 -25 -16 0
85 -82 -133 0
131 -94 23 0
-150 -30 -4 0
112 107 58 0
138 -60 89 0
-1 -67 -147 0
-120 -108 24 0
16 -130 31 0
18 -42 -135 0
-138 -102 53 0
-141 -106 -101 0
-68 58 34 0
-93 -66 143 0
-2 103 -114 0
130 -15 -30 0
68 82 90 0
-95 -137 -87 0
-142 -21 -53 0
57 -146 -91 0
-99 -112 132 0
113 -62 4 0
81 24 -59 0
4 -145 7 0
-45 36 -146 0
-102 -5 -90 0
6 -96 -146 0
-82 -80 -100 0
-127 100 96 0
-134 50 110 0
107 136 21 0
-131 -74 -100 0
52 14 -27 0
102 -131 -72 0
-123 97 128 0
-98 -32 147 0
123 58 139 0
-20 -85 47 0
-37 69 91 0
-56 128 146 0
86 85 4 0
-27 -69 -57 0
119 -37 63 0
-34 -8 -69 0
-142 -147 -79 0
-144 -70 -65 0
-66 -1 -146 0
101 -68 -134 0
-14 -115 112 0
-33 81 50 0
92 62 -105 0
-83 -125 79 0
26 49 96 0
-114 75 -142 0
129 -40 -12 0
62 -92 141 0
94 -31 -25 0
-52 -134 -21 0
24 106 7 0
-96 9 52 0
36 -99 -143 0
-76 -59 -121 0
-73 -133 62 0
25 3 10 0
-45 114 -49 0
-148 -107 -35 0
81 59 -57 0
130 82 -120 0
-95 -50 -102 0
144 125 84 0
129 68 -111 0
11 139 3 0
55 19 -92 0
124 -4 -16 0
-44 -102 -71 0
-131 -122 -59 0
35 145 -105 0
-48 -117 12 0
-106 114 74 0
-66 82 -133 0
127 -39 -98 0
-2 14 -77 0
-99 -98 -104 0
-31 42 -58 0
-135 78 -28 0
93 -41 -125 0
123 77 119 0
-37 -131 117 0
-85 121 -95 0
-89 60 -34 0
53 120 139 0
-132 133 140 0
-119 68 -3 0
-138 -142 -64 0
39 73 48 0
20 -91 44 0
72 100 36 0
-84 -18 135 0
-29 91 34 0
-82 -61 -90 0
-54 3 70 0
1 -82 137 0
-104 76 53 0
130 -41 -96 0
-31 65 28 0
100 97 13 0
56 -46 -104 0
-78 -37 23 0
-136 -105 75 0
-49 -149 122 0
-87 -68 112 0
121 142 -52 0
21 -111 -20 0
78 76 98 0
60 -56 64 0
46 69 100 0
15 138 28 0
49 -83 -21 0
62 53 38 0
-75 -114 -101 0
-20 41 1 0
-5 63 -32 0
-27 -150 113 0
7 -29 112 0
-91 47 107 0
98 -81 39 0
-70 42 -61 0
44 -46 -128 0
81 148 131 0
49 104 -110 0
-44 129 81 0
138 115 -102 0
27 -109 18 0
-107 -46 5 0
-150 -137 122 0
110 -35 132 0
101 104 140 0
24 29 -15 0
49 -139 -26 0
72 76 -100 0
46 144 -126 0
53 135 47 0
-98 -61 -78 0
-91 150 99 0
80 125 -99 0
-121 -64 128 0
-39 144 146 0
134 -133 93 0
-21 36 -44 0
-143 -81 -71 0
76 81 -2 0
64 67 -85 0
93 135 104 0
-79 67 -84 0
-68 -29 -16 0
-77 -46 -57 0
-19 12 1 0
74 14 137 0
75 -128 -99 0
-93 18 -12 0
-85 82 -28 0
-76 -29 137 0
79 -56 -72 0
97 8 98 0
28 109 65 0
22 -2 3 0
25 -69 41 0
-70 -73 78 0
112 -84 19 0
107 6 144 0
-93 -68 63 0
-107 142 -124 0
-19 73 41 0
-108 -25 -111 0
11 40 -95 0
-65 -4 58 0
33 55 17 0
124 71 92 0
42 -125 -29 0
92 -111 1 0
-26 30 66 0
-109 40 -69 0
-145 19 41 0
-91 -75 -32 0
-80 19 92 0
143 81 -87 0
-72 -123 132 0
-110 93 -46 0
-57 -119 -4 0
69 -18 101 0
68 -91 -86 0
-97 71 73 0
106 19 -114 0
-80 75 111 0
-15 -81 66 0
120 9 -104 0
-6 109 -23 0
99 -143 -102 0
55 73 44 0
-64 -22 -137 0
-142 106 -87 0
49 -17 -58 0
-4 -43 -87 0
-74 10 3 0
24 89 31 0
88 60 -123 0
123 -54 -150 0
125 -128 -137 0
-142 -7 -101 0
4 148 -65 0
50 -96 42 0
6 -92 100 0
-100 97 -53 0
-27 -149 -142 0
104 146 -114 0
150 -80 67 0
87 -108 -128 0
111 -63 46 0
-148 25 52 0
105 -106 41 0
-40 123 -149 0
-141 -100 58 0
-68 -98 -84 0
17 -109 -106 0
113 -53 64 0
-73 10 72 0
107 -123 -80 0
-143 57 -34 0
122 125 71 0
3 -125 -92 0
-79 106 139 0
-22 -27 -134 0
-52 93 150 0
-51 21 140 0
-149 64 -37 0
69 -148 87 0
69 -19 -34 0
-146 -22 -77 0
-10 -8 145 0
-62 127 119 0
79 136 36 0
22 112 51 0
-39 10 -42 0
-91 14 -6 0
-141 75 110 0
147 -101 12 0
-65 139 17 0
136 82 39 0
26 138 56 0
-15 63 143 0
2 19 -116 0
-68 -116 -71 0
114 -67 -45 0
-46 120 80 0
20 -16 -65 0
-28 142 104 0
-75 72 120 0
109 -120 117 0
96 -17 30 0
-27 -138 46 0
-26 27 28 0
-134 -95 -104 0
-4 48 79 0
31 146 68 0
-91 -47 23 0
22 -13 49 0
80 -126 -13 0
143 84 1 0
121 -85 48 0
-73 85 -114 0
117 -92 -113 0
-83 -71 80 0
48 96 -92 0
-100 137 80 0
64 98 -9 0
-128 9 21 0
-44 105 82 0
132 -98 -131 0
-69 -96 134 0
-72 6 -105 0
9 -10 6 0
-40 -142 133 0
-6 96 -131 0
-134 -87 72 0
-125 -7 18 0
-76 -96 61 0
-109 -15 -1 0
-124 -142 -61 0
81 -112 -16 0
15 -52 107 0
-84 -57 -139 0
3 96 -128 0
119 -12 -105 0
-109 47 -44 0
75 -64 23 0
76 30 60 0
28 25 143 0
119 147 41 0
6 -135 -53 0
21 34 -15 0
-47 141 140 0
-3 -82 38 0
25 -56 -63 0
-72 134 74 0
-76 -54 -67 0
50 -143 123 0
-52 -101 109 0
4 120 -102 0
-5 -107 -64 0
110 -6 -150 0
-9 146 89 0
-8 87 -138 0
-13 -30 -53 0
43 -100 106 0
138 130 -52 0
23 -71 -86 0
-11 43 111 0
-139 98 96 0
-146 144 75 0
3 9 -28 0
-52 44 -24 0
111 57 -22 0
114 -23 -37 0
92 121 -73 0
-65 -74 -102 0
45 30 18 0
47 128 121 0
7 12 27 0
123 12 122 0
-139 93 -117 0
-63 -80 -125 0
-144 -44 119 0
118 -28 -145 0
134 -111 119 0
-17 -81 128 0
-19 45 47 0
92 85 7 0
24 14 -51 0
-15 9 -110 0
-144 54 -29 0
-44 -29 -39 0
-129 -69 15 0
7 148 -75 0
56 30 -108 0
-113 -5 48 0
136 -20 87 0
-104 89 -133 0
-29 -79 -105 0
53 41 149 0
4 19 -16 0
109 147 -11 0
-108 -124 -59 0
47 121 61 0
-121 -126 -87 0
-130 140 11 0
-138 149 17 0
119 -1 -11 0
9 -138 -72 0
115 -109 -122 0
42 58 -96 0
-73 40 135 0
-127 7 -28 0
89 -43 -106 0
-6 -76 -53 0
85 18 -38 0
-16 -143 130 0
27 59 25 0
-23 -134 101 0
-73 -1 -137 0
-106 -62 130 0
83 -107 -42 0
-81 134 -32 0
-13 62 61 0
25 -113 55 0
-124 44 93 0
3 119 -141 0
18 112 -82 0
126 78 32 0
-90 -65 -34 0
-26 50 16 0
-3 6 21 0
92 -67 -13 0
143 -92 6 0
-95 67 111 0
-102 87 -86 0
19 57 -95 0
-91 141 61 0
32 7 -118 0
83 -126 12 0
80 56 9 0
104 -42 120 0
-43 -22 11 0
-130 6 31 0
43 126 -37 0
-126 -99 46 0
48 -68 110 0
37 -8 62 0
-72 91 -43 0
14 -80 -61 0
-40 -110 -28 0
-5 141 59 0
5 -44 -33 0
-102 -13 -84 0
-79 128 51 0
-69 67 -144 0
-88 -7 -78 0
22 125 129 0
-47 -143 82 0
102 66 23 0
36 124 -116 0
116 8 -125 0
-128 -26 -70 0
-25 -126 -102 0
2 58 4 0
74 -95 -31 0
-7 -90 -109 0
-76 110 139 0
105 91 -44 0
-145 48 -57 0
-55 146 61 0
-37 42 -125 0
-108 -99 -67 0
15 -48 -73 0
-58 -98 -16 0
-81 -150 -84 0
26 -122 10 0
108 75 130 0
-6 -36 120 0
46 -2 -22 0
-150 47 117 0
51 63 -24 0
92 21 -65 0
-145 -51 122 0
38 -24 67 0
-26 86 -79 0
43 -70 -29 0
-57 -71 113 0
-58 137 -29 0
140 -59 12 0
74 -80 -123 0
108 -17 118 0
80 68 23 0
-108 -47 -87 0
-81 137 31 0
-137 109 105 0
48 130 70 0
-75 -83 133 0
127 -91 -89 0
36 -8 -73 0
91 86 -66 0
98 -93 68 0
83 -33 -4 0
107 78 -46 0
-56 -12 55 0
-62 -48 78 0
54 -35 84 0
4 24 -8 0
25 -110 -73 0
-52 35 89 0
117 67 98 0
-60 -78 74 0
147 2 -89 0
149 94 51 0
148 65 -86 0
137 -83 -31 0
-88 -46 -82 0
87 -50 -83 0
-100 42 -3 0
28 137 86 0
34 43 -3 0
-5 -141 -21 0
14 31 97 0
-119 -64 30 0
108 122 115 0
-39 -72 38 0
107 116 34 0
57 56 46 0
30 -43 -132 0
-90 -81 -54 0
-124 39 -127 0
-33 129 22 0
-132 -76 -83 0
14 42 -132 0
13 95 38 0
-5 -3 44 0
-120 112 35 0
-28 19 -131 0
-110 -16 21 0
-40 103 129 0
-83 24 -12 0
34 -124 -52 0
-124 -142 -106 0
-83 62 124 0
-138 -43 17 0
-125 53 59 0
-76 -63 -36 0
65 104 -142 0
-129 -140 5 0
16 80 50 0
-67 20 -73 0
37 80 -14 0
72 -121 99 0
7 120 -146 0
18 -88 17 0
87 37 -81 0
-110 -49 16 0
-119 43 68 0
-112 -4 69 0
141 -14 -23 0
144 20 -16 0
-113 80 116 0
-56 93 -80 0
-46 -10 117 0
-121 122 55 0
-78 23 -58 0
44 138 18 0
-46 -130 11 0
89 -148 68 0
97 -83 22 0
-40 -3 -74 0
36 -139 87 0
-122 44 -141 0
-41 107 90 0
8 -108 133 0
80 -148 61 0
103 130 -145 0
51 -5 36 0
133 -26 11 0
-123 142 -130 0
14 -101 87 0
-82 -57 11 0
-69 147 47 0
9 -21 59 0
42 65 34 0
109 -34 -4 0
-76 -40 -15 0
129 -35 -108 0
-58 147 -16 0
8 -57 22 0
-95 -37 76 0
56 -7 74 0
-31 -70 74 0
-134 -3 59 0
-107 126 132 0
-21 111 95 0
131 115 -32 0
95 66 -43 0
%
0