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