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