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