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