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