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 250  1065 
 -180 -169 -139 0
-172 -115 164 0
170 196 -14 0
16 46 -163 0
-17 194 102 0
-104 190 -235 0
154 -30 -38 0
103 -158 -175 0
-78 191 8 0
169 -61 7 0
86 89 206 0
243 234 93 0
-10 152 -238 0
-147 96 -104 0
-219 6 -208 0
-242 -110 32 0
11 -172 -96 0
-183 -212 47 0
-83 -43 -160 0
83 -166 2 0
233 132 137 0
-127 -90 -238 0
-117 126 151 0
-228 129 90 0
-135 -147 203 0
162 -170 225 0
114 61 144 0
-40 149 213 0
237 -41 -137 0
114 -62 99 0
-158 -109 -205 0
186 20 -199 0
-166 160 -130 0
136 -87 -232 0
224 27 -222 0
106 -249 -27 0
-199 -67 203 0
127 -61 233 0
-198 74 169 0
89 -70 -108 0
228 247 198 0
-189 -5 145 0
-214 29 101 0
-28 -232 -113 0
-29 250 -28 0
86 37 -165 0
112 230 -225 0
-46 85 -155 0
185 58 171 0
7 -33 -82 0
203 4 -177 0
87 -148 197 0
188 199 -151 0
-32 29 -239 0
34 83 -25 0
-5 -69 -197 0
149 22 130 0
162 22 231 0
-243 145 -104 0
-224 -131 -13 0
-191 -1 -198 0
-119 -80 -155 0
31 -85 10 0
-86 139 18 0
-119 93 -246 0
-10 -31 -242 0
-91 36 -2 0
-234 64 -10 0
-116 160 -45 0
-248 218 7 0
-234 108 127 0
-148 -156 80 0
74 -134 177 0
240 242 162 0
-199 122 228 0
-52 99 -183 0
222 221 153 0
165 193 187 0
93 16 -54 0
-15 -249 -50 0
68 -6 13 0
-248 -155 -56 0
-204 -121 -117 0
204 55 -159 0
-186 74 -208 0
-150 -134 167 0
248 131 -5 0
229 -236 81 0
-239 79 -97 0
106 22 229 0
-225 156 178 0
-242 66 -192 0
207 -98 208 0
-80 182 -163 0
82 -184 20 0
105 221 183 0
92 103 -66 0
-6 56 -34 0
-47 173 -159 0
-208 -181 -170 0
-4 -95 -137 0
186 219 -102 0
-187 -7 6 0
197 -17 21 0
92 -183 50 0
177 164 135 0
-61 35 -230 0
112 -223 -237 0
-215 -140 -223 0
-105 86 130 0
194 23 203 0
91 146 86 0
50 170 94 0
-243 -1 -176 0
163 -90 6 0
83 188 -124 0
-87 -107 -104 0
-43 226 81 0
172 -4 118 0
17 -132 -194 0
-124 6 -125 0
205 127 -247 0
219 -92 -148 0
166 -151 -163 0
137 15 -13 0
-16 -160 -191 0
31 -111 -109 0
199 -138 -249 0
-4 -103 128 0
48 22 -139 0
-245 117 -85 0
167 37 102 0
-183 12 158 0
159 111 198 0
160 -75 -105 0
224 129 72 0
-49 231 -115 0
170 188 189 0
173 27 -157 0
203 222 -8 0
11 243 19 0
160 -99 64 0
-202 -169 -7 0
186 168 -153 0
26 240 -186 0
-174 -57 -199 0
25 49 98 0
-157 -24 15 0
-39 -100 -178 0
156 -217 -204 0
-47 173 -56 0
245 -140 243 0
-189 134 88 0
-214 86 101 0
106 183 8 0
59 70 179 0
58 -60 -182 0
-115 91 43 0
204 -7 -176 0
95 3 -135 0
108 -121 228 0
79 43 102 0
-170 -207 -94 0
-53 -111 144 0
182 9 43 0
-224 219 -226 0
245 84 3 0
-100 -14 -51 0
-80 29 -70 0
13 188 243 0
-161 -228 72 0
97 174 160 0
-194 119 -18 0
203 141 22 0
-7 -127 -217 0
-102 -93 -198 0
-249 -77 51 0
-162 120 -189 0
-173 67 141 0
-224 96 130 0
161 197 -155 0
236 118 -211 0
106 189 5 0
-44 -41 185 0
187 -209 -119 0
129 -59 160 0
-168 -152 -147 0
14 43 -111 0
137 130 19 0
-95 249 211 0
177 -194 167 0
114 144 -235 0
183 34 214 0
22 189 -179 0
43 104 240 0
112 244 -249 0
112 -194 -118 0
-17 -137 -172 0
-30 -201 -162 0
-200 33 24 0
-245 -148 -85 0
218 -38 107 0
-224 -151 -196 0
119 161 77 0
-202 69 -100 0
-66 -3 -33 0
-64 214 -247 0
-230 -22 -30 0
-51 36 -71 0
193 -18 8 0
-178 -59 19 0
-169 -22 228 0
44 171 -48 0
234 147 250 0
244 216 83 0
18 -185 133 0
50 -63 113 0
53 21 225 0
64 -79 -217 0
-129 -126 -205 0
-36 -144 148 0
10 229 104 0
-177 -59 -102 0
-221 222 -25 0
-177 164 -32 0
-94 161 -51 0
-32 -89 -209 0
217 138 -23 0
15 -9 -152 0
-196 122 -100 0
135 -97 -186 0
119 53 124 0
222 -151 110 0
55 -197 -192 0
39 14 -228 0
150 -113 87 0
250 69 102 0
210 45 -15 0
110 -139 149 0
-179 21 54 0
-109 185 -183 0
244 -18 202 0
-210 -100 -69 0
178 29 42 0
-117 -8 44 0
-241 -22 13 0
57 209 -49 0
33 -14 -39 0
5 -165 236 0
70 108 -72 0
-192 -20 -6 0
236 1 -180 0
224 -41 -247 0
-220 -147 -150 0
19 -13 249 0
75 67 -47 0
-51 6 -241 0
-215 14 -40 0
196 -244 79 0
-235 217 -34 0
10 -131 -226 0
46 -12 2 0
35 -207 55 0
6 -113 73 0
-106 -192 238 0
49 -185 -175 0
20 36 -146 0
63 -106 95 0
196 185 125 0
40 124 -25 0
-71 61 133 0
130 104 -158 0
163 187 85 0
-19 249 -198 0
-226 57 90 0
198 -155 -163 0
204 30 -102 0
-90 -218 -162 0
-188 -243 -214 0
-102 111 38 0
-43 -58 -27 0
203 -92 206 0
-29 -43 -228 0
156 155 194 0
-101 142 190 0
11 125 -107 0
-214 32 87 0
-180 115 82 0
109 212 -203 0
131 182 -134 0
-120 81 -90 0
221 -80 202 0
-97 179 -151 0
-227 -195 -168 0
172 -128 -180 0
21 68 -80 0
-31 14 26 0
-18 169 204 0
125 73 -234 0
-40 -174 109 0
218 250 -124 0
243 141 181 0
-43 139 170 0
36 -182 90 0
1 -13 -15 0
165 -199 243 0
-205 239 243 0
137 50 3 0
-73 81 -243 0
4 -101 -229 0
11 -124 -159 0
105 116 -143 0
-212 -137 -198 0
25 -16 -74 0
-233 -182 -25 0
171 -210 107 0
-234 -67 -135 0
-25 126 -22 0
215 -116 -231 0
-213 115 91 0
221 246 -249 0
-97 -59 -28 0
-115 -209 -68 0
101 -145 -23 0
240 -147 19 0
120 -105 -90 0
79 29 -222 0
47 124 114 0
22 -111 190 0
-199 181 -19 0
-62 -130 -8 0
65 -76 -219 0
193 229 101 0
101 -115 -221 0
-162 108 93 0
84 137 -234 0
-30 -102 -57 0
226 -80 217 0
-186 237 173 0
-67 188 189 0
-13 201 -151 0
227 71 -39 0
-21 44 -7 0
-46 -56 -129 0
-50 -28 -92 0
-2 -200 -160 0
-90 -172 21 0
55 -225 134 0
205 -7 58 0
237 25 -47 0
-37 -15 -183 0
-146 -6 50 0
-6 -189 -229 0
-142 204 -197 0
219 24 -197 0
-249 138 -223 0
59 -229 144 0
112 151 -216 0
-29 -181 -169 0
148 99 229 0
53 112 218 0
164 -102 -30 0
85 -70 75 0
-15 -189 -45 0
139 -62 -24 0
-196 -208 248 0
-214 -145 142 0
-168 37 170 0
-107 101 -18 0
76 173 -243 0
-236 -235 105 0
-24 112 -232 0
-15 23 220 0
14 122 -156 0
-212 -98 -112 0
-102 -183 135 0
43 189 -144 0
-207 118 20 0
-231 65 -157 0
-76 58 -27 0
-87 113 156 0
-3 -112 10 0
-143 92 230 0
198 -249 -97 0
33 -210 249 0
-32 -233 -123 0
9 205 -53 0
131 -243 29 0
-143 -104 -44 0
-181 240 138 0
190 80 -16 0
3 26 173 0
243 174 -16 0
67 -177 -25 0
-38 96 221 0
-209 214 98 0
193 29 -140 0
-138 76 -107 0
75 163 -68 0
81 -60 78 0
-70 -195 67 0
-33 -112 -121 0
-105 115 -30 0
-103 -93 38 0
-153 23 120 0
-84 144 -49 0
242 94 79 0
65 121 -170 0
219 185 -30 0
-66 -9 245 0
40 -73 213 0
-56 213 -118 0
189 -139 4 0
45 -202 -21 0
46 -23 135 0
109 247 -196 0
-95 140 -131 0
96 212 94 0
-184 -115 -28 0
-81 235 -8 0
89 -133 212 0
202 48 -186 0
-37 -105 -170 0
-206 137 104 0
-218 -172 26 0
-190 225 -182 0
-197 210 -182 0
91 -79 -45 0
250 -163 -134 0
-145 113 147 0
-220 -27 6 0
-36 125 225 0
-158 97 95 0
200 -107 216 0
-59 103 223 0
-237 -242 87 0
-7 -179 -140 0
247 53 244 0
144 205 -207 0
-220 97 18 0
3 37 -33 0
104 -36 -244 0
12 51 -133 0
246 10 189 0
75 -144 -121 0
19 232 194 0
-212 46 -222 0
-95 -73 21 0
-210 171 -85 0
2 100 -26 0
-34 -135 -201 0
96 -205 7 0
36 -4 140 0
-132 191 235 0
98 -92 -109 0
94 -248 109 0
5 -71 -56 0
-79 -173 -219 0
33 110 -141 0
-26 174 72 0
-108 -140 34 0
68 -189 -79 0
89 -29 137 0
-8 29 225 0
-129 -72 223 0
235 64 160 0
26 -98 -32 0
-69 60 11 0
71 125 37 0
95 151 153 0
-88 84 -171 0
90 -128 48 0
104 51 -78 0
-121 77 69 0
-239 217 241 0
-248 122 175 0
-119 209 -154 0
184 183 -186 0
206 167 -20 0
115 -62 -108 0
195 200 -15 0
145 -237 -92 0
184 86 -104 0
62 52 -67 0
222 190 -202 0
-222 239 -104 0
-119 3 208 0
-131 234 195 0
-134 -165 -93 0
91 216 -107 0
196 16 -139 0
-21 119 249 0
88 -209 -33 0
-73 76 50 0
-83 -116 10 0
-89 -104 70 0
-224 -174 190 0
22 240 -226 0
-191 96 243 0
35 93 134 0
-99 120 144 0
-240 72 220 0
-197 66 -112 0
90 61 -230 0
-100 -86 83 0
-23 -230 234 0
-213 137 -152 0
-53 -12 -11 0
49 23 -192 0
17 -205 -78 0
-213 -211 188 0
-28 89 223 0
-125 -74 -50 0
-16 36 6 0
199 -80 66 0
-236 141 213 0
-8 115 -178 0
18 168 21 0
50 69 44 0
-166 225 186 0
-234 -237 5 0
-35 -167 -207 0
-161 -165 -168 0
-189 31 39 0
89 -3 39 0
-139 -217 -26 0
-235 -197 -102 0
191 -70 -163 0
78 -189 175 0
-181 11 -13 0
8 173 213 0
218 -50 -71 0
-68 181 49 0
124 -115 -238 0
59 -162 -169 0
68 -138 -126 0
-154 -139 -241 0
205 26 -161 0
53 -128 63 0
199 234 205 0
-71 -123 -223 0
-137 56 -32 0
107 -235 15 0
215 41 147 0
71 -29 57 0
110 -217 -234 0
225 -50 -192 0
247 34 -207 0
-32 15 235 0
1 -113 -94 0
-168 248 206 0
-38 55 168 0
-202 59 -128 0
103 102 -193 0
-153 30 -98 0
-235 -4 234 0
-59 -193 -118 0
-71 123 238 0
126 -134 -159 0
-54 124 217 0
137 104 -57 0
183 102 154 0
-230 148 -198 0
-25 221 112 0
121 -93 206 0
-140 -130 -178 0
158 -183 -73 0
136 -213 -48 0
-62 -205 -115 0
-6 8 -246 0
-35 -235 118 0
183 -88 49 0
-155 35 -245 0
-96 180 129 0
113 108 24 0
97 103 215 0
247 120 -131 0
-157 52 -109 0
-100 -210 164 0
-60 250 -135 0
231 220 196 0
42 -123 158 0
199 192 226 0
-11 -212 -16 0
201 224 241 0
67 -82 79 0
-39 -168 203 0
-16 -160 -35 0
47 -228 108 0
54 -102 245 0
-153 3 178 0
62 -54 -222 0
-108 15 91 0
-39 52 -34 0
-168 -37 162 0
115 -226 -185 0
-158 45 -209 0
-31 60 232 0
212 -116 72 0
-26 147 44 0
-195 224 -243 0
117 -227 28 0
-216 180 -131 0
235 -65 62 0
64 -198 188 0
124 -79 20 0
-100 -74 -66 0
199 115 -146 0
26 47 -62 0
127 167 182 0
-111 147 145 0
219 -112 176 0
-250 188 190 0
-143 -43 -47 0
189 6 66 0
187 181 -236 0
184 30 110 0
184 -64 36 0
-123 102 -96 0
-69 246 230 0
-224 -52 231 0
207 -66 -71 0
-164 -107 -199 0
1 102 10 0
70 -90 -62 0
99 -199 228 0
-120 -114 175 0
76 93 -206 0
-182 -42 37 0
8 208 148 0
-245 -106 -71 0
82 -55 91 0
105 70 -113 0
245 -26 195 0
-89 224 40 0
-108 38 152 0
-155 92 -141 0
-16 203 205 0
-30 8 74 0
56 128 14 0
142 -221 94 0
130 53 195 0
154 -64 246 0
-156 -221 17 0
19 1 183 0
-89 237 -16 0
-35 -159 216 0
21 -82 77 0
25 95 -237 0
96 92 182 0
74 -212 14 0
-3 -178 -203 0
232 -177 -212 0
75 218 246 0
-243 -104 161 0
-201 207 -247 0
-8 48 -67 0
91 247 150 0
-204 -129 60 0
-18 182 172 0
-214 56 10 0
-99 -27 103 0
138 -77 -116 0
-129 82 -49 0
-6 -49 171 0
-230 -191 82 0
-45 -248 128 0
-16 51 191 0
52 -216 -152 0
90 159 -232 0
35 65 149 0
217 -98 -47 0
-208 -11 10 0
218 195 -62 0
52 -134 -124 0
-242 179 23 0
-189 12 -174 0
-195 -63 180 0
51 180 17 0
-78 -100 196 0
-160 124 17 0
-8 -203 -73 0
101 133 -240 0
103 138 -131 0
-181 78 -29 0
-215 189 35 0
43 129 -2 0
42 -161 -73 0
233 -44 47 0
42 -93 -126 0
231 -183 -94 0
64 207 -93 0
5 -114 63 0
236 -128 -47 0
-80 33 52 0
-110 83 202 0
167 -161 -73 0
-161 230 -7 0
227 41 30 0
232 153 -52 0
53 -217 236 0
-120 85 -244 0
86 -4 198 0
244 -204 44 0
43 -209 -20 0
-248 44 93 0
67 168 -97 0
-28 196 -194 0
230 31 125 0
-140 -95 61 0
-36 -187 -96 0
-140 237 -62 0
176 74 -117 0
-39 29 -185 0
15 192 82 0
-127 136 -208 0
-116 -154 -114 0
-99 -66 233 0
120 -224 60 0
41 -151 -52 0
143 102 38 0
227 190 206 0
-249 -216 162 0
12 51 -70 0
-182 145 107 0
-136 159 184 0
-225 235 198 0
-26 73 -30 0
33 -66 11 0
-59 69 9 0
-248 187 -183 0
-190 84 -175 0
-201 -39 -72 0
-190 9 191 0
65 170 -146 0
98 83 -134 0
-221 203 76 0
-144 39 128 0
91 -209 -112 0
109 223 -142 0
202 -144 59 0
-78 144 25 0
243 -182 -153 0
224 238 130 0
-59 -128 11 0
-176 -84 200 0
57 -247 17 0
196 144 -237 0
-20 238 -121 0
-187 132 -18 0
-3 -8 -234 0
75 -49 150 0
-146 -76 -194 0
-16 193 195 0
27 -28 -150 0
-193 -228 -239 0
-79 5 -29 0
-28 242 -234 0
178 140 -100 0
141 52 -220 0
22 -38 172 0
241 43 -106 0
-178 49 193 0
-68 197 -206 0
109 210 -34 0
-23 22 -166 0
-44 23 -173 0
100 -219 242 0
109 198 208 0
46 225 -237 0
207 75 9 0
-3 -62 63 0
119 60 -74 0
121 210 151 0
105 -69 240 0
78 -103 -117 0
-128 -228 -195 0
45 -21 214 0
-71 1 25 0
-238 183 117 0
-20 -102 117 0
-20 66 -69 0
119 -50 241 0
-148 -239 -121 0
221 -198 -132 0
-102 194 -7 0
-59 99 10 0
97 181 -65 0
209 160 -221 0
-29 -53 129 0
66 -242 247 0
-17 -174 27 0
241 -166 106 0
37 -88 -60 0
144 222 -119 0
-119 103 -169 0
-207 -78 -168 0
-24 212 -69 0
219 -76 85 0
-18 -85 226 0
-59 -6 190 0
-222 -153 79 0
43 159 12 0
-108 7 127 0
-196 -52 152 0
-7 -247 -45 0
198 196 143 0
77 -127 -187 0
140 95 232 0
-84 -232 68 0
25 159 -3 0
-61 53 172 0
-231 -156 132 0
143 -133 -214 0
-141 -233 -232 0
-214 244 -42 0
193 123 199 0
121 -57 -184 0
121 -117 -60 0
84 132 -191 0
-197 53 -153 0
134 212 -88 0
111 -197 -220 0
221 -69 62 0
-238 235 185 0
-87 -246 77 0
204 -118 -58 0
-205 61 81 0
-119 75 -97 0
-233 91 234 0
192 105 28 0
-115 48 128 0
-57 -45 -139 0
166 89 -67 0
-11 1 245 0
-110 -134 55 0
-242 26 193 0
220 -160 -159 0
22 -217 -218 0
45 -236 -148 0
66 -13 61 0
-185 131 -64 0
148 14 -89 0
-207 -142 -184 0
-62 221 155 0
-137 -76 -71 0
235 130 -92 0
227 -155 150 0
-32 168 162 0
134 154 59 0
-96 -250 144 0
-127 -180 -220 0
103 205 132 0
-21 51 11 0
20 -149 7 0
146 -32 119 0
130 74 -244 0
-75 -144 -176 0
49 166 245 0
-162 -118 158 0
-37 -91 127 0
-220 10 -148 0
185 -184 -82 0
55 -189 -143 0
-58 159 108 0
-60 113 143 0
-10 -237 -34 0
-97 -134 -76 0
156 48 -154 0
-38 154 -59 0
197 179 247 0
-114 125 -250 0
40 129 82 0
-80 213 -123 0
-134 -48 -122 0
77 -139 169 0
88 -92 -159 0
36 -29 -70 0
193 -224 90 0
-34 91 148 0
145 -110 -229 0
98 21 50 0
197 143 -67 0
-143 202 -184 0
-83 -51 231 0
70 -100 123 0
6 11 -76 0
-93 -213 75 0
121 122 36 0
-194 -187 103 0
187 237 157 0
-114 41 82 0
-121 188 61 0
29 218 162 0
-117 -216 203 0
-26 -76 -106 0
4 -249 182 0
-183 59 215 0
-34 32 30 0
-211 -212 -17 0
-33 -207 232 0
-30 -143 114 0
-237 -161 110 0
13 -188 -145 0
93 -202 109 0
-38 -88 245 0
-206 119 225 0
153 -7 -135 0
-116 -98 -141 0
250 72 -82 0
123 116 51 0
-228 -248 -146 0
227 -66 -248 0
-108 -35 -5 0
-130 193 -56 0
173 249 -223 0
-17 -38 -145 0
195 -17 135 0
-164 -221 47 0
41 -106 -87 0
-175 79 219 0
147 135 -48 0
178 48 -16 0
-104 -16 173 0
181 -219 191 0
-238 144 175 0
216 -188 178 0
12 -158 -78 0
-228 -74 197 0
-236 -155 93 0
-23 160 -207 0
-240 82 -186 0
198 -106 72 0
-206 110 114 0
26 -246 -242 0
-181 -193 -73 0
134 130 19 0
234 245 219 0
-96 -226 -211 0
47 154 -215 0
201 202 -79 0
-211 223 -98 0
93 25 -140 0
162 -175 136 0
92 -181 -167 0
192 -169 -140 0
239 -154 -201 0
232 226 17 0
-31 198 -21 0
180 -160 85 0
-35 -157 -222 0
153 166 -67 0
95 234 -176 0
-206 136 -159 0
-131 232 137 0
-17 113 -9 0
-151 189 102 0
167 -136 -87 0
-53 -202 -78 0
189 58 -112 0
-178 38 52 0
-122 -176 27 0
-77 -59 -203 0
-106 -204 150 0
-62 -104 -135 0
-113 107 -195 0
4 -165 145 0
98 -215 -97 0
-248 -234 201 0
225 -228 -220 0
-16 -14 5 0
180 -182 211 0
-112 59 -63 0
-204 107 174 0
-20 229 -68 0
-137 104 -232 0
-188 243 92 0
248 -178 -112 0
-1 -89 77 0
14 12 -59 0
50 138 250 0
192 217 56 0
-88 -113 -49 0
-170 174 22 0
-76 -112 27 0
31 243 -164 0
-93 -216 159 0
19 87 137 0
1 -205 233 0
37 -26 -192 0
90 -191 -127 0
195 -63 117 0
128 229 -203 0
73 47 -193 0
135 -106 169 0
212 7 -20 0
239 205 53 0
-222 -186 242 0
162 22 -85 0
-247 212 -9 0
244 249 -184 0
3 -76 -148 0
68 152 141 0
-97 238 -111 0
85 89 -149 0
-20 248 185 0
145 14 97 0
-248 -137 179 0
229 -43 242 0
-26 -59 -171 0
110 171 -172 0
-65 18 196 0
189 -58 151 0
121 174 139 0
195 -39 171 0
-40 72 243 0
144 181 -133 0
103 -31 -250 0
-98 -18 -120 0
99 -75 -171 0
92 -231 205 0
199 -86 2 0
23 26 124 0
218 126 -39 0
-219 -211 -244 0
-23 -72 165 0
49 -105 192 0
143 -209 -141 0
36 198 -45 0
-242 -4 117 0
-169 166 -83 0
-191 179 -131 0
-132 72 136 0
183 250 99 0
-248 -38 -122 0
-151 -97 -138 0
173 -180 141 0
-49 -52 -76 0
239 -131 -128 0
-92 134 -200 0
182 -17 -227 0
-31 -172 145 0
-175 -23 116 0
127 196 195 0
166 124 216 0
-247 18 98 0
188 117 -19 0
147 -212 -16 0
76 88 -168 0
102 8 -74 0
-147 120 178 0
91 30 -131 0
102 9 130 0
89 95 178 0
207 216 -28 0
190 -179 20 0
132 14 142 0
181 223 12 0
151 -179 -127 0
98 -142 -207 0
25 -111 168 0
157 110 -104 0
51 53 198 0
-94 13 -217 0
-211 188 -43 0