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