c ind 10 103 115 127 13 139 151 163 177 189 0
c ind 193 198 203 208 213 22 25 27 285 287 0
c ind 30 326 328 33 330 332 334 336 338 340 0
c ind 36 39 42 45 48 5 51 54 57 6 0
c ind 60 63 66 76 78 80 82 9 0
p cnf 340 1026
-1 -2 11 0
-1 2 318 0
-100 -101 -34 0
-100 101 34 0
-101 -102 -104 0
-101 102 104 0
-102 -25 -103 0
-102 25 103 0
-104 25 0
-104 31 0
-105 106 109 0
-106 107 108 0
-107 28 0
-107 96 0
-108 28 0
-108 97 0
-109 96 0
-109 97 0
-11 -12 14 0
-11 12 68 0
-110 -111 39 0
-110 -39 111 0
-111 -112 -117 0
-111 112 117 0
-112 -113 -40 0
-112 113 40 0
-113 -114 -116 0
-113 114 116 0
-114 -25 -115 0
-114 25 115 0
-116 103 0
-116 104 0
-117 118 121 0
-118 119 120 0
-119 101 0
-119 34 0
-12 -13 9 0
-12 -9 13 0
-120 105 0
-120 34 0
-121 101 0
-121 105 0
-122 -123 45 0
-122 -45 123 0
-123 -124 -129 0
-123 124 129 0
-124 -125 -46 0
-124 125 46 0
-125 -126 -128 0
-125 126 128 0
-126 -25 -127 0
-126 25 127 0
-128 115 0
-128 116 0
-129 130 133 0
-130 131 132 0
-131 113 0
-131 40 0
-132 117 0
-132 40 0
-133 113 0
-133 117 0
-134 -135 51 0
-134 -51 135 0
-135 -136 -141 0
-135 136 141 0
-136 -137 -52 0
-136 137 52 0
-137 -138 -140 0
-137 138 140 0
-138 -25 -139 0
-138 25 139 0
-14 15 0
-14 62 0
-140 127 0
-140 128 0
-141 142 145 0
-142 143 144 0
-143 125 0
-143 46 0
-144 129 0
-144 46 0
-145 125 0
-145 129 0
-146 -147 57 0
-146 -57 147 0
-147 -148 -153 0
-147 148 153 0
-148 -149 -58 0
-148 149 58 0
-149 -150 -152 0
-149 150 152 0
-15 16 0
-15 56 0
-150 -25 -151 0
-150 25 151 0
-152 139 0
-152 140 0
-153 154 157 0
-154 155 156 0
-155 137 0
-155 52 0
-156 141 0
-156 52 0
-157 137 0
-157 141 0
-158 -159 63 0
-158 -63 159 0
-159 -160 -165 0
-159 160 165 0
-16 17 0
-16 50 0
-160 -161 -64 0
-160 161 64 0
-161 -162 -164 0
-161 162 164 0
-162 -25 -163 0
-162 25 163 0
-164 151 0
-164 152 0
-165 166 169 0
-166 167 168 0
-167 149 0
-167 58 0
-168 153 0
-168 58 0
-169 149 0
-169 153 0
-17 18 0
-17 44 0
-170 -171 175 0
-170 171 293 0
-171 172 0
-171 81 0
-172 173 0
-172 79 0
-173 174 0
-173 77 0
-174 -13 76 0
-174 -76 13 0
-175 -176 178 0
-175 176 215 0
-176 -13 177 0
-176 -177 13 0
-178 179 0
-178 210 0
-179 180 0
-179 205 0
-18 19 0
-18 38 0
-180 181 0
-180 200 0
-181 182 0
-181 195 0
-182 183 0
-182 190 0
-183 184 0
-183 186 0
-184 185 0
-184 21 0
-185 -27 96 0
-185 -96 27 0
-186 -187 33 0
-186 -33 187 0
-187 -188 -104 0
-187 188 104 0
-188 -25 -189 0
-188 25 189 0
-19 20 0
-19 32 0
-190 -191 39 0
-190 -39 191 0
-191 -192 -194 0
-191 192 194 0
-192 -25 -193 0
-192 25 193 0
-194 104 0
-194 189 0
-195 -196 45 0
-195 -45 196 0
-196 -197 -199 0
-196 197 199 0
-197 -25 -198 0
-197 25 198 0
-199 193 0
-199 194 0
-2 3 7 0
-20 21 0
-20 26 0
-200 -201 51 0
-200 -51 201 0
-201 -202 -204 0
-201 202 204 0
-202 -25 -203 0
-202 25 203 0
-204 198 0
-204 199 0
-205 -206 57 0
-205 -57 206 0
-206 -207 -209 0
-206 207 209 0
-207 -25 -208 0
-207 25 208 0
-209 203 0
-209 204 0
-21 -22 23 0
-21 -23 22 0
-210 -211 63 0
-210 -63 211 0
-211 -212 -214 0
-211 212 214 0
-212 -25 -213 0
-212 25 213 0
-214 208 0
-214 209 0
-215 216 0
-215 280 0
-216 217 0
-216 270 0
-217 218 0
-217 260 0
-218 219 0
-218 250 0
-219 220 0
-219 240 0
-220 221 0
-220 230 0
-221 222 0
-221 225 0
-222 -22 223 0
-222 -223 22 0
-223 -224 -25 0
-223 224 25 0
-224 -23 -30 0
-224 23 30 0
-225 -226 27 0
-225 -27 226 0
-226 -227 -229 0
-226 227 229 0
-227 -228 -36 0
-227 228 36 0
-228 -188 -31 0
-228 188 31 0
-229 23 0
-229 30 0
-23 -24 -25 0
-23 24 25 0
-230 -231 33 0
-230 -33 231 0
-231 -232 -235 0
-231 232 235 0
-232 -233 -42 0
-232 233 42 0
-233 -192 -234 0
-233 192 234 0
-234 189 0
-234 31 0
-235 236 239 0
-236 237 238 0
-237 228 0
-237 36 0
-238 229 0
-238 36 0
-239 228 0
-239 229 0
-24 -25 -25 0
-24 25 25 0
-240 -241 39 0
-240 -39 241 0
-241 -242 -245 0
-241 242 245 0
-242 -243 -48 0
-242 243 48 0
-243 -197 -244 0
-243 197 244 0
-244 193 0
-244 234 0
-245 246 249 0
-246 247 248 0
-247 233 0
-247 42 0
-248 235 0
-248 42 0
-249 233 0
-249 235 0
-25 0
-250 -251 45 0
-250 -45 251 0
-251 -252 -255 0
-251 252 255 0
-252 -253 -54 0
-252 253 54 0
-253 -202 -254 0
-253 202 254 0
-254 198 0
-254 244 0
-255 256 259 0
-256 257 258 0
-257 243 0
-257 48 0
-258 245 0
-258 48 0
-259 243 0
-259 245 0
-26 -27 28 0
-26 -28 27 0
-260 -261 51 0
-260 -51 261 0
-261 -262 -265 0
-261 262 265 0
-262 -263 -60 0
-262 263 60 0
-263 -207 -264 0
-263 207 264 0
-264 203 0
-264 254 0
-265 266 269 0
-266 267 268 0
-267 253 0
-267 54 0
-268 255 0
-268 54 0
-269 253 0
-269 255 0
-270 -271 57 0
-270 -57 271 0
-271 -272 -275 0
-271 272 275 0
-272 -273 -66 0
-272 273 66 0
-273 -212 -274 0
-273 212 274 0
-274 208 0
-274 264 0
-275 276 279 0
-276 277 278 0
-277 263 0
-277 60 0
-278 265 0
-278 60 0
-279 263 0
-279 265 0
-28 -29 -31 0
-28 29 31 0
-280 -281 63 0
-280 -63 281 0
-281 -282 -288 0
-281 282 288 0
-282 -283 -287 0
-282 283 287 0
-283 -284 -286 0
-283 284 286 0
-284 -25 -285 0
-284 25 285 0
-286 213 0
-286 274 0
-288 289 292 0
-289 290 291 0
-29 -25 -30 0
-29 25 30 0
-290 273 0
-290 66 0
-291 275 0
-291 66 0
-292 273 0
-292 275 0
-293 -294 303 0
-293 294 318 0
-294 295 0
-294 302 0
-295 296 0
-295 302 0
-296 297 0
-296 302 0
-297 298 0
-297 302 0
-298 299 0
-298 81 0
-299 300 0
-299 79 0
-3 -4 0
-300 301 0
-300 75 0
-301 -13 78 0
-301 -78 13 0
-302 -25 25 0
-303 304 0
-303 317 0
-304 305 0
-304 316 0
-305 306 0
-305 315 0
-306 307 0
-306 314 0
-307 308 0
-307 313 0
-308 309 0
-308 312 0
-309 310 0
-309 311 0
-31 25 0
-310 -22 25 0
-310 -25 22 0
-311 -25 27 0
-311 -27 25 0
-312 -25 33 0
-312 -33 25 0
-313 -25 39 0
-313 -39 25 0
-314 -25 45 0
-314 -45 25 0
-315 -25 51 0
-315 -51 25 0
-316 -25 57 0
-316 -57 25 0
-317 -25 63 0
-317 -63 25 0
-318 319 0
-318 339 0
-319 320 0
-319 337 0
-32 -33 34 0
-32 -34 33 0
-320 321 0
-320 335 0
-321 322 0
-321 333 0
-322 323 0
-322 331 0
-323 324 0
-323 329 0
-324 325 0
-324 327 0
-325 -22 326 0
-325 -326 22 0
-327 -27 328 0
-327 -328 27 0
-329 -33 330 0
-329 -330 33 0
-331 -332 39 0
-331 -39 332 0
-333 -334 45 0
-333 -45 334 0
-335 -336 51 0
-335 -51 336 0
-337 -338 57 0
-337 -57 338 0
-339 -340 63 0
-339 -63 340 0
-34 -35 -37 0
-34 35 37 0
-35 -25 -36 0
-35 25 36 0
-37 30 0
-37 31 0
-38 -39 40 0
-38 -40 39 0
-4 -5 6 0
-4 -6 5 0
-40 -41 -43 0
-40 41 43 0
-41 -25 -42 0
-41 25 42 0
-43 36 0
-43 37 0
-44 -45 46 0
-44 -46 45 0
-46 -47 -49 0
-46 47 49 0
-47 -25 -48 0
-47 25 48 0
-49 42 0
-49 43 0
-50 -51 52 0
-50 -52 51 0
-52 -53 -55 0
-52 53 55 0
-53 -25 -54 0
-53 25 54 0
-55 48 0
-55 49 0
-56 -57 58 0
-56 -58 57 0
-58 -59 -61 0
-58 59 61 0
-59 -25 -60 0
-59 25 60 0
-61 54 0
-61 55 0
-62 -63 64 0
-62 -64 63 0
-64 -65 -67 0
-64 65 67 0
-65 -25 -66 0
-65 25 66 0
-67 60 0
-67 61 0
-68 -69 71 0
-68 69 318 0
-69 3 0
-69 70 0
-7 -8 0
-70 -13 5 0
-70 -5 13 0
-71 -72 83 0
-71 72 170 0
-72 73 0
-72 81 0
-73 74 0
-73 79 0
-74 75 0
-74 77 0
-75 -25 76 0
-75 -76 25 0
-77 -25 78 0
-77 -78 25 0
-79 -25 80 0
-79 -80 25 0
-8 -10 9 0
-8 -9 10 0
-81 -25 82 0
-81 -82 25 0
-83 158 0
-83 84 0
-84 146 0
-84 85 0
-85 134 0
-85 86 0
-86 122 0
-86 87 0
-87 110 0
-87 88 0
-88 89 0
-88 98 0
-89 90 0
-89 93 0
-90 -22 91 0
-90 -91 22 0
-91 -92 -25 0
-91 92 25 0
-92 -23 -23 0
-92 23 23 0
-93 -27 94 0
-93 -94 27 0
-94 -95 -97 0
-94 95 97 0
-95 -96 -28 0
-95 96 28 0
-96 -24 -31 0
-96 24 31 0
-97 23 0
-98 -33 99 0
-98 -99 33 0
-99 -100 -105 0
-99 100 105 0
1 -11 -318 0
1 -2 -11 0
1 0
1 2 -318 0
100 -101 34 0
100 -34 101 0
101 -102 104 0
101 -104 102 0
102 -103 25 0
102 -25 103 0
104 -25 -31 0
105 -106 0
105 -109 0
106 -107 0
106 -108 0
107 -96 -28 0
108 -28 -97 0
109 -96 -97 0
11 -12 -14 0
11 -14 -68 0
11 12 -68 0
110 -39 -111 0
110 39 111 0
111 -112 117 0
111 -117 112 0
112 -113 40 0
112 -40 113 0
113 -114 116 0
113 -116 114 0
114 -115 25 0
114 -25 115 0
116 -103 -104 0
117 -118 0
117 -121 0
118 -119 0
118 -120 0
119 -101 -34 0
12 -9 -13 0
12 9 13 0
120 -34 -105 0
121 -101 -105 0
122 -45 -123 0
122 45 123 0
123 -124 129 0
123 -129 124 0
124 -125 46 0
124 -46 125 0
125 -126 128 0
125 -128 126 0
126 -127 25 0
126 -25 127 0
128 -115 -116 0
129 -130 0
129 -133 0
13 0
130 -131 0
130 -132 0
131 -113 -40 0
132 -40 -117 0
133 -113 -117 0
134 -51 -135 0
134 51 135 0
135 -136 141 0
135 -141 136 0
136 -137 52 0
136 -52 137 0
137 -138 140 0
137 -140 138 0
138 -139 25 0
138 -25 139 0
14 -15 -62 0
140 -127 -128 0
141 -142 0
141 -145 0
142 -143 0
142 -144 0
143 -125 -46 0
144 -46 -129 0
145 -125 -129 0
146 -57 -147 0
146 57 147 0
147 -148 153 0
147 -153 148 0
148 -149 58 0
148 -58 149 0
149 -150 152 0
149 -152 150 0
15 -16 -56 0
150 -151 25 0
150 -25 151 0
152 -139 -140 0
153 -154 0
153 -157 0
154 -155 0
154 -156 0
155 -137 -52 0
156 -52 -141 0
157 -137 -141 0
158 -63 -159 0
158 63 159 0
159 -160 165 0
159 -165 160 0
16 -17 -50 0
160 -161 64 0
160 -64 161 0
161 -162 164 0
161 -164 162 0
162 -163 25 0
162 -25 163 0
164 -151 -152 0
165 -166 0
165 -169 0
166 -167 0
166 -168 0
167 -149 -58 0
168 -58 -153 0
169 -149 -153 0
17 -18 -44 0
170 -171 -175 0
170 -175 -293 0
170 171 -293 0
171 -172 -81 0
172 -173 -79 0
173 -174 -77 0
174 -76 -13 0
174 76 13 0
175 -176 -178 0
175 -178 -215 0
175 176 -215 0
176 -177 -13 0
176 177 13 0
178 -179 -210 0
179 -180 -205 0
18 -19 -38 0
180 -181 -200 0
181 -182 -195 0
182 -183 -190 0
183 -184 -186 0
184 -21 -185 0
185 -27 -96 0
185 27 96 0
186 -33 -187 0
186 33 187 0
187 -104 188 0
187 -188 104 0
188 -189 25 0
188 -25 189 0
19 -20 -32 0
190 -39 -191 0
190 39 191 0
191 -192 194 0
191 -194 192 0
192 -193 25 0
192 -25 193 0
194 -189 -104 0
195 -45 -196 0
195 45 196 0
196 -197 199 0
196 -199 197 0
197 -198 25 0
197 -25 198 0
199 -193 -194 0
2 -3 0
2 -7 0
20 -21 -26 0
200 -51 -201 0
200 51 201 0
201 -202 204 0
201 -204 202 0
202 -203 25 0
202 -25 203 0
204 -198 -199 0
205 -57 -206 0
205 57 206 0
206 -207 209 0
206 -209 207 0
207 -208 25 0
207 -25 208 0
209 -203 -204 0
21 -22 -23 0
21 22 23 0
210 -63 -211 0
210 63 211 0
211 -212 214 0
211 -214 212 0
212 -213 25 0
212 -25 213 0
214 -208 -209 0
215 -216 -280 0
216 -217 -270 0
217 -218 -260 0
218 -219 -250 0
219 -220 -240 0
220 -221 -230 0
221 -222 -225 0
222 -22 -223 0
222 22 223 0
223 -224 25 0
223 -25 224 0
224 -23 30 0
224 -30 23 0
225 -27 -226 0
225 27 226 0
226 -227 229 0
226 -229 227 0
227 -228 36 0
227 -36 228 0
228 -188 31 0
228 -31 188 0
229 -23 -30 0
23 -24 25 0
23 -25 24 0
230 -33 -231 0
230 33 231 0
231 -232 235 0
231 -235 232 0
232 -233 42 0
232 -42 233 0
233 -192 234 0
233 -234 192 0
234 -189 -31 0
235 -236 0
235 -239 0
236 -237 0
236 -238 0
237 -228 -36 0
238 -36 -229 0
239 -228 -229 0
24 -25 25 0
240 -39 -241 0
240 39 241 0
241 -242 245 0
241 -245 242 0
242 -243 48 0
242 -48 243 0
243 -197 244 0
243 -244 197 0
244 -193 -234 0
245 -246 0
245 -249 0
246 -247 0
246 -248 0
247 -233 -42 0
248 -42 -235 0
249 -233 -235 0
250 -45 -251 0
250 45 251 0
251 -252 255 0
251 -255 252 0
252 -253 54 0
252 -54 253 0
253 -202 254 0
253 -254 202 0
254 -198 -244 0
255 -256 0
255 -259 0
256 -257 0
256 -258 0
257 -243 -48 0
258 -48 -245 0
259 -243 -245 0
26 -27 -28 0
26 27 28 0
260 -51 -261 0
260 51 261 0
261 -262 265 0
261 -265 262 0
262 -263 60 0
262 -60 263 0
263 -207 264 0
263 -264 207 0
264 -203 -254 0
265 -266 0
265 -269 0
266 -267 0
266 -268 0
267 -253 -54 0
268 -54 -255 0
269 -253 -255 0
270 -57 -271 0
270 57 271 0
271 -272 275 0
271 -275 272 0
272 -273 66 0
272 -66 273 0
273 -212 274 0
273 -274 212 0
274 -208 -264 0
275 -276 0
275 -279 0
276 -277 0
276 -278 0
277 -263 -60 0
278 -60 -265 0
279 -263 -265 0
28 -29 31 0
28 -31 29 0
280 -63 -281 0
280 63 281 0
281 -282 288 0
281 -288 282 0
282 -283 287 0
282 -287 283 0
283 -284 286 0
283 -286 284 0
284 -25 285 0
284 -285 25 0
286 -213 -274 0
288 -289 0
288 -292 0
289 -290 0
289 -291 0
29 -25 30 0
29 -30 25 0
290 -273 -66 0
291 -66 -275 0
292 -273 -275 0
293 -294 -303 0
293 -303 -318 0
293 294 -318 0
294 -295 -302 0
295 -296 -302 0
296 -297 -302 0
297 -298 -302 0
298 -299 -81 0
299 -300 -79 0
3 4 0
300 -75 -301 0
301 -78 -13 0
301 78 13 0
302 -25 -25 0
302 25 25 0
303 -304 -317 0
304 -305 -316 0
305 -306 -315 0
306 -307 -314 0
307 -308 -313 0
308 -309 -312 0
309 -310 -311 0
31 -25 -25 0
310 -22 -25 0
310 22 25 0
311 -27 -25 0
311 27 25 0
312 -33 -25 0
312 33 25 0
313 -39 -25 0
313 39 25 0
314 -45 -25 0
314 45 25 0
315 -51 -25 0
315 51 25 0
316 -57 -25 0
316 57 25 0
317 -63 -25 0
317 63 25 0
318 -319 -339 0
319 -320 -337 0
32 -33 -34 0
32 33 34 0
320 -321 -335 0
321 -322 -333 0
322 -323 -331 0
323 -324 -329 0
324 -325 -327 0
325 -22 -326 0
325 22 326 0
327 -27 -328 0
327 27 328 0
329 -33 -330 0
329 33 330 0
331 -39 -332 0
331 39 332 0
333 -45 -334 0
333 45 334 0
335 -51 -336 0
335 51 336 0
337 -57 -338 0
337 57 338 0
339 -63 -340 0
339 63 340 0
34 -35 37 0
34 -37 35 0
35 -25 36 0
35 -36 25 0
37 -30 -31 0
38 -39 -40 0
38 39 40 0
4 -5 -6 0
4 5 6 0
40 -41 43 0
40 -43 41 0
41 -25 42 0
41 -42 25 0
43 -36 -37 0
44 -45 -46 0
44 45 46 0
46 -47 49 0
46 -49 47 0
47 -25 48 0
47 -48 25 0
49 -42 -43 0
50 -51 -52 0
50 51 52 0
52 -53 55 0
52 -55 53 0
53 -25 54 0
53 -54 25 0
55 -48 -49 0
56 -57 -58 0
56 57 58 0
58 -59 61 0
58 -61 59 0
59 -25 60 0
59 -60 25 0
61 -54 -55 0
62 -63 -64 0
62 63 64 0
64 -65 67 0
64 -67 65 0
65 -25 66 0
65 -66 25 0
67 -60 -61 0
68 -69 -71 0
68 -71 -318 0
68 69 -318 0
69 -3 -70 0
7 8 0
70 -5 -13 0
70 5 13 0
71 -72 -83 0
71 -83 -170 0
71 72 -170 0
72 -73 -81 0
73 -74 -79 0
74 -75 -77 0
75 -76 -25 0
75 76 25 0
77 -78 -25 0
77 78 25 0
79 -80 -25 0
79 80 25 0
8 -9 -10 0
8 9 10 0
81 -82 -25 0
81 82 25 0
83 -84 -158 0
84 -85 -146 0
85 -86 -134 0
86 -87 -122 0
87 -88 -110 0
88 -89 -98 0
89 -90 -93 0
90 -22 -91 0
90 22 91 0
91 -25 92 0
91 -92 25 0
92 -23 23 0
93 -27 -94 0
93 27 94 0
94 -95 97 0
94 -97 95 0
95 -28 96 0
95 -96 28 0
96 -24 31 0
96 -31 24 0
97 -23 -23 0
98 -33 -99 0
98 33 99 0
99 -100 105 0
99 -105 100 0