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