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