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