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