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