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