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