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