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