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