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