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