c AI planning file sortnetsort7.v.stepl.005.qcnf (Jussi.Rintanen@NICTA.com.au) p cnf 667 2195 e 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 0 a 154 1 2 3 4 5 6 7 0 e 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 0 -41 42 0 -42 43 0 -43 44 0 -44 45 0 -45 46 0 -46 47 0 -157 -154 8 0 -157 -8 154 0 -157 156 0 -156 157 0 -156 154 155 0 -154 156 0 -155 156 0 -155 -154 0 154 155 0 1 -9 0 -1 9 223 222 221 220 219 218 0 -223 49 0 -223 -2 0 -223 1 0 -49 -1 2 223 0 -222 50 0 -222 -3 0 -222 1 0 -50 -1 3 222 0 -221 51 0 -221 -4 0 -221 1 0 -51 -1 4 221 0 -220 52 0 -220 -5 0 -220 1 0 -52 -1 5 220 0 -219 53 0 -219 -6 0 -219 1 0 -53 -1 6 219 0 -218 54 0 -218 -7 0 -218 1 0 -54 -1 7 218 0 2 -10 224 0 -2 10 229 228 227 226 225 0 -224 49 0 -224 -2 0 -224 1 0 -49 -1 2 224 0 -229 55 0 -229 -3 0 -229 2 0 -55 -2 3 229 0 -228 56 0 -228 -4 0 -228 2 0 -56 -2 4 228 0 -227 57 0 -227 -5 0 -227 2 0 -57 -2 5 227 0 -226 58 0 -226 -6 0 -226 2 0 -58 -2 6 226 0 -225 59 0 -225 -7 0 -225 2 0 -59 -2 7 225 0 3 -11 231 230 0 -3 11 235 234 233 232 0 -231 50 0 -231 -3 0 -231 1 0 -50 -1 3 231 0 -230 55 0 -230 -3 0 -230 2 0 -55 -2 3 230 0 -235 60 0 -235 -4 0 -235 3 0 -60 -3 4 235 0 -234 61 0 -234 -5 0 -234 3 0 -61 -3 5 234 0 -233 62 0 -233 -6 0 -233 3 0 -62 -3 6 233 0 -232 63 0 -232 -7 0 -232 3 0 -63 -3 7 232 0 4 -12 238 237 236 0 -4 12 241 240 239 0 -238 51 0 -238 -4 0 -238 1 0 -51 -1 4 238 0 -237 56 0 -237 -4 0 -237 2 0 -56 -2 4 237 0 -236 60 0 -236 -4 0 -236 3 0 -60 -3 4 236 0 -241 64 0 -241 -5 0 -241 4 0 -64 -4 5 241 0 -240 65 0 -240 -6 0 -240 4 0 -65 -4 6 240 0 -239 66 0 -239 -7 0 -239 4 0 -66 -4 7 239 0 5 -13 245 244 243 242 0 -5 13 247 246 0 -245 52 0 -245 -5 0 -245 1 0 -52 -1 5 245 0 -244 57 0 -244 -5 0 -244 2 0 -57 -2 5 244 0 -243 61 0 -243 -5 0 -243 3 0 -61 -3 5 243 0 -242 64 0 -242 -5 0 -242 4 0 -64 -4 5 242 0 -247 67 0 -247 -6 0 -247 5 0 -67 -5 6 247 0 -246 68 0 -246 -7 0 -246 5 0 -68 -5 7 246 0 6 -14 252 251 250 249 248 0 -6 14 253 0 -252 53 0 -252 -6 0 -252 1 0 -53 -1 6 252 0 -251 58 0 -251 -6 0 -251 2 0 -58 -2 6 251 0 -250 62 0 -250 -6 0 -250 3 0 -62 -3 6 250 0 -249 65 0 -249 -6 0 -249 4 0 -65 -4 6 249 0 -248 67 0 -248 -6 0 -248 5 0 -67 -5 6 248 0 -253 69 0 -253 -7 0 -253 6 0 -69 -6 7 253 0 7 -15 259 258 257 256 255 254 0 -7 15 0 -259 54 0 -259 -7 0 -259 1 0 -54 -1 7 259 0 -258 59 0 -258 -7 0 -258 2 0 -59 -2 7 258 0 -257 63 0 -257 -7 0 -257 3 0 -63 -3 7 257 0 -256 66 0 -256 -7 0 -256 4 0 -66 -4 7 256 0 -255 68 0 -255 -7 0 -255 5 0 -68 -5 7 255 0 -254 69 0 -254 -7 0 -254 6 0 -69 -6 7 254 0 8 -16 0 -8 16 0 -49 -1 2 -9 0 -49 -1 2 10 0 -50 -1 3 -9 0 -50 -1 3 11 0 -51 -1 4 -9 0 -51 -1 4 12 0 -52 -1 5 -9 0 -52 -1 5 13 0 -53 -1 6 -9 0 -53 -1 6 14 0 -54 -1 7 -9 0 -54 -1 7 15 0 -55 -2 3 -10 0 -55 -2 3 11 0 -56 -2 4 -10 0 -56 -2 4 12 0 -57 -2 5 -10 0 -57 -2 5 13 0 -58 -2 6 -10 0 -58 -2 6 14 0 -59 -2 7 -10 0 -59 -2 7 15 0 -60 -3 4 -11 0 -60 -3 4 12 0 -61 -3 5 -11 0 -61 -3 5 13 0 -62 -3 6 -11 0 -62 -3 6 14 0 -63 -3 7 -11 0 -63 -3 7 15 0 -64 -4 5 -12 0 -64 -4 5 13 0 -65 -4 6 -12 0 -65 -4 6 14 0 -66 -4 7 -12 0 -66 -4 7 15 0 -67 -5 6 -13 0 -67 -5 6 14 0 -68 -5 7 -13 0 -68 -5 7 15 0 -69 -6 7 -14 0 -69 -6 7 15 0 -186 187 0 -54 187 0 -186 -54 0 -185 186 0 -53 186 0 -185 -53 0 -184 185 0 -52 185 0 -184 -52 0 -183 184 0 -51 184 0 -183 -51 0 -49 183 0 -50 183 0 -49 -50 0 -181 182 0 -59 182 0 -181 -59 0 -180 181 0 -58 181 0 -180 -58 0 -179 180 0 -57 180 0 -179 -57 0 -55 179 0 -56 179 0 -55 -56 0 -49 -59 0 -49 -58 0 -49 -57 0 -49 -56 0 -49 -55 0 -177 178 0 -63 178 0 -177 -63 0 -176 177 0 -62 177 0 -176 -62 0 -60 176 0 -61 176 0 -60 -61 0 -175 -63 0 -175 -62 0 -175 -61 0 -175 -60 0 -50 175 0 -55 175 0 -50 -55 0 -173 174 0 -66 174 0 -173 -66 0 -64 173 0 -65 173 0 -64 -65 0 -172 -66 0 -172 -65 0 -172 -64 0 -171 172 0 -60 172 0 -171 -60 0 -51 171 0 -56 171 0 -51 -56 0 -67 170 0 -68 170 0 -67 -68 0 -169 -68 0 -169 -67 0 -168 169 0 -64 169 0 -168 -64 0 -167 168 0 -61 168 0 -167 -61 0 -52 167 0 -57 167 0 -52 -57 0 -166 -69 0 -165 166 0 -67 166 0 -165 -67 0 -164 165 0 -65 165 0 -164 -65 0 -163 164 0 -62 164 0 -163 -62 0 -53 163 0 -58 163 0 -53 -58 0 -161 162 0 -69 162 0 -161 -69 0 -160 161 0 -68 161 0 -160 -68 0 -159 160 0 -66 160 0 -159 -66 0 -158 159 0 -63 159 0 -158 -63 0 -54 158 0 -59 158 0 -54 -59 0 -216 217 0 -49 217 0 -216 -49 0 -215 216 0 -50 216 0 -215 -50 0 -214 215 0 -51 215 0 -214 -51 0 -213 214 0 -52 214 0 -213 -52 0 -54 213 0 -53 213 0 -54 -53 0 -212 -49 0 -211 212 0 -55 212 0 -211 -55 0 -210 211 0 -56 211 0 -210 -56 0 -209 210 0 -57 210 0 -209 -57 0 -59 209 0 -58 209 0 -59 -58 0 -208 -50 0 -208 -55 0 -207 208 0 -60 208 0 -207 -60 0 -206 207 0 -61 207 0 -206 -61 0 -63 206 0 -62 206 0 -63 -62 0 -55 205 0 -50 205 0 -55 -50 0 -204 -51 0 -204 -56 0 -204 -60 0 -203 204 0 -64 204 0 -203 -64 0 -66 203 0 -65 203 0 -66 -65 0 -201 202 0 -51 202 0 -201 -51 0 -60 201 0 -56 201 0 -60 -56 0 -200 -52 0 -200 -57 0 -200 -61 0 -200 -64 0 -68 200 0 -67 200 0 -68 -67 0 -198 199 0 -52 199 0 -198 -52 0 -197 198 0 -57 198 0 -197 -57 0 -64 197 0 -61 197 0 -64 -61 0 -69 -53 0 -69 -58 0 -69 -62 0 -69 -65 0 -69 -67 0 -195 196 0 -53 196 0 -195 -53 0 -194 195 0 -58 195 0 -194 -58 0 -193 194 0 -62 194 0 -193 -62 0 -67 193 0 -65 193 0 -67 -65 0 -191 192 0 -54 192 0 -191 -54 0 -190 191 0 -59 191 0 -190 -59 0 -189 190 0 -63 190 0 -189 -63 0 -188 189 0 -66 189 0 -188 -66 0 -69 188 0 -68 188 0 -69 -68 0 9 -17 0 -9 17 325 324 323 322 321 320 0 -325 70 0 -325 -10 0 -325 9 0 -70 -9 10 325 0 -324 71 0 -324 -11 0 -324 9 0 -71 -9 11 324 0 -323 72 0 -323 -12 0 -323 9 0 -72 -9 12 323 0 -322 73 0 -322 -13 0 -322 9 0 -73 -9 13 322 0 -321 74 0 -321 -14 0 -321 9 0 -74 -9 14 321 0 -320 75 0 -320 -15 0 -320 9 0 -75 -9 15 320 0 10 -18 326 0 -10 18 331 330 329 328 327 0 -326 70 0 -326 -10 0 -326 9 0 -70 -9 10 326 0 -331 76 0 -331 -11 0 -331 10 0 -76 -10 11 331 0 -330 77 0 -330 -12 0 -330 10 0 -77 -10 12 330 0 -329 78 0 -329 -13 0 -329 10 0 -78 -10 13 329 0 -328 79 0 -328 -14 0 -328 10 0 -79 -10 14 328 0 -327 80 0 -327 -15 0 -327 10 0 -80 -10 15 327 0 11 -19 333 332 0 -11 19 337 336 335 334 0 -333 71 0 -333 -11 0 -333 9 0 -71 -9 11 333 0 -332 76 0 -332 -11 0 -332 10 0 -76 -10 11 332 0 -337 81 0 -337 -12 0 -337 11 0 -81 -11 12 337 0 -336 82 0 -336 -13 0 -336 11 0 -82 -11 13 336 0 -335 83 0 -335 -14 0 -335 11 0 -83 -11 14 335 0 -334 84 0 -334 -15 0 -334 11 0 -84 -11 15 334 0 12 -20 340 339 338 0 -12 20 343 342 341 0 -340 72 0 -340 -12 0 -340 9 0 -72 -9 12 340 0 -339 77 0 -339 -12 0 -339 10 0 -77 -10 12 339 0 -338 81 0 -338 -12 0 -338 11 0 -81 -11 12 338 0 -343 85 0 -343 -13 0 -343 12 0 -85 -12 13 343 0 -342 86 0 -342 -14 0 -342 12 0 -86 -12 14 342 0 -341 87 0 -341 -15 0 -341 12 0 -87 -12 15 341 0 13 -21 347 346 345 344 0 -13 21 349 348 0 -347 73 0 -347 -13 0 -347 9 0 -73 -9 13 347 0 -346 78 0 -346 -13 0 -346 10 0 -78 -10 13 346 0 -345 82 0 -345 -13 0 -345 11 0 -82 -11 13 345 0 -344 85 0 -344 -13 0 -344 12 0 -85 -12 13 344 0 -349 88 0 -349 -14 0 -349 13 0 -88 -13 14 349 0 -348 89 0 -348 -15 0 -348 13 0 -89 -13 15 348 0 14 -22 354 353 352 351 350 0 -14 22 355 0 -354 74 0 -354 -14 0 -354 9 0 -74 -9 14 354 0 -353 79 0 -353 -14 0 -353 10 0 -79 -10 14 353 0 -352 83 0 -352 -14 0 -352 11 0 -83 -11 14 352 0 -351 86 0 -351 -14 0 -351 12 0 -86 -12 14 351 0 -350 88 0 -350 -14 0 -350 13 0 -88 -13 14 350 0 -355 90 0 -355 -15 0 -355 14 0 -90 -14 15 355 0 15 -23 361 360 359 358 357 356 0 -15 23 0 -361 75 0 -361 -15 0 -361 9 0 -75 -9 15 361 0 -360 80 0 -360 -15 0 -360 10 0 -80 -10 15 360 0 -359 84 0 -359 -15 0 -359 11 0 -84 -11 15 359 0 -358 87 0 -358 -15 0 -358 12 0 -87 -12 15 358 0 -357 89 0 -357 -15 0 -357 13 0 -89 -13 15 357 0 -356 90 0 -356 -15 0 -356 14 0 -90 -14 15 356 0 16 -24 0 -16 24 0 -70 -9 10 -17 0 -70 -9 10 18 0 -71 -9 11 -17 0 -71 -9 11 19 0 -72 -9 12 -17 0 -72 -9 12 20 0 -73 -9 13 -17 0 -73 -9 13 21 0 -74 -9 14 -17 0 -74 -9 14 22 0 -75 -9 15 -17 0 -75 -9 15 23 0 -76 -10 11 -18 0 -76 -10 11 19 0 -77 -10 12 -18 0 -77 -10 12 20 0 -78 -10 13 -18 0 -78 -10 13 21 0 -79 -10 14 -18 0 -79 -10 14 22 0 -80 -10 15 -18 0 -80 -10 15 23 0 -81 -11 12 -19 0 -81 -11 12 20 0 -82 -11 13 -19 0 -82 -11 13 21 0 -83 -11 14 -19 0 -83 -11 14 22 0 -84 -11 15 -19 0 -84 -11 15 23 0 -85 -12 13 -20 0 -85 -12 13 21 0 -86 -12 14 -20 0 -86 -12 14 22 0 -87 -12 15 -20 0 -87 -12 15 23 0 -88 -13 14 -21 0 -88 -13 14 22 0 -89 -13 15 -21 0 -89 -13 15 23 0 -90 -14 15 -22 0 -90 -14 15 23 0 -288 289 0 -75 289 0 -288 -75 0 -287 288 0 -74 288 0 -287 -74 0 -286 287 0 -73 287 0 -286 -73 0 -285 286 0 -72 286 0 -285 -72 0 -70 285 0 -71 285 0 -70 -71 0 -283 284 0 -80 284 0 -283 -80 0 -282 283 0 -79 283 0 -282 -79 0 -281 282 0 -78 282 0 -281 -78 0 -76 281 0 -77 281 0 -76 -77 0 -70 -80 0 -70 -79 0 -70 -78 0 -70 -77 0 -70 -76 0 -279 280 0 -84 280 0 -279 -84 0 -278 279 0 -83 279 0 -278 -83 0 -81 278 0 -82 278 0 -81 -82 0 -277 -84 0 -277 -83 0 -277 -82 0 -277 -81 0 -71 277 0 -76 277 0 -71 -76 0 -275 276 0 -87 276 0 -275 -87 0 -85 275 0 -86 275 0 -85 -86 0 -274 -87 0 -274 -86 0 -274 -85 0 -273 274 0 -81 274 0 -273 -81 0 -72 273 0 -77 273 0 -72 -77 0 -88 272 0 -89 272 0 -88 -89 0 -271 -89 0 -271 -88 0 -270 271 0 -85 271 0 -270 -85 0 -269 270 0 -82 270 0 -269 -82 0 -73 269 0 -78 269 0 -73 -78 0 -268 -90 0 -267 268 0 -88 268 0 -267 -88 0 -266 267 0 -86 267 0 -266 -86 0 -265 266 0 -83 266 0 -265 -83 0 -74 265 0 -79 265 0 -74 -79 0 -263 264 0 -90 264 0 -263 -90 0 -262 263 0 -89 263 0 -262 -89 0 -261 262 0 -87 262 0 -261 -87 0 -260 261 0 -84 261 0 -260 -84 0 -75 260 0 -80 260 0 -75 -80 0 -318 319 0 -70 319 0 -318 -70 0 -317 318 0 -71 318 0 -317 -71 0 -316 317 0 -72 317 0 -316 -72 0 -315 316 0 -73 316 0 -315 -73 0 -75 315 0 -74 315 0 -75 -74 0 -314 -70 0 -313 314 0 -76 314 0 -313 -76 0 -312 313 0 -77 313 0 -312 -77 0 -311 312 0 -78 312 0 -311 -78 0 -80 311 0 -79 311 0 -80 -79 0 -310 -71 0 -310 -76 0 -309 310 0 -81 310 0 -309 -81 0 -308 309 0 -82 309 0 -308 -82 0 -84 308 0 -83 308 0 -84 -83 0 -76 307 0 -71 307 0 -76 -71 0 -306 -72 0 -306 -77 0 -306 -81 0 -305 306 0 -85 306 0 -305 -85 0 -87 305 0 -86 305 0 -87 -86 0 -303 304 0 -72 304 0 -303 -72 0 -81 303 0 -77 303 0 -81 -77 0 -302 -73 0 -302 -78 0 -302 -82 0 -302 -85 0 -89 302 0 -88 302 0 -89 -88 0 -300 301 0 -73 301 0 -300 -73 0 -299 300 0 -78 300 0 -299 -78 0 -85 299 0 -82 299 0 -85 -82 0 -90 -74 0 -90 -79 0 -90 -83 0 -90 -86 0 -90 -88 0 -297 298 0 -74 298 0 -297 -74 0 -296 297 0 -79 297 0 -296 -79 0 -295 296 0 -83 296 0 -295 -83 0 -88 295 0 -86 295 0 -88 -86 0 -293 294 0 -75 294 0 -293 -75 0 -292 293 0 -80 293 0 -292 -80 0 -291 292 0 -84 292 0 -291 -84 0 -290 291 0 -87 291 0 -290 -87 0 -90 290 0 -89 290 0 -90 -89 0 17 -25 0 -17 25 427 426 425 424 423 422 0 -427 91 0 -427 -18 0 -427 17 0 -91 -17 18 427 0 -426 92 0 -426 -19 0 -426 17 0 -92 -17 19 426 0 -425 93 0 -425 -20 0 -425 17 0 -93 -17 20 425 0 -424 94 0 -424 -21 0 -424 17 0 -94 -17 21 424 0 -423 95 0 -423 -22 0 -423 17 0 -95 -17 22 423 0 -422 96 0 -422 -23 0 -422 17 0 -96 -17 23 422 0 18 -26 428 0 -18 26 433 432 431 430 429 0 -428 91 0 -428 -18 0 -428 17 0 -91 -17 18 428 0 -433 97 0 -433 -19 0 -433 18 0 -97 -18 19 433 0 -432 98 0 -432 -20 0 -432 18 0 -98 -18 20 432 0 -431 99 0 -431 -21 0 -431 18 0 -99 -18 21 431 0 -430 100 0 -430 -22 0 -430 18 0 -100 -18 22 430 0 -429 101 0 -429 -23 0 -429 18 0 -101 -18 23 429 0 19 -27 435 434 0 -19 27 439 438 437 436 0 -435 92 0 -435 -19 0 -435 17 0 -92 -17 19 435 0 -434 97 0 -434 -19 0 -434 18 0 -97 -18 19 434 0 -439 102 0 -439 -20 0 -439 19 0 -102 -19 20 439 0 -438 103 0 -438 -21 0 -438 19 0 -103 -19 21 438 0 -437 104 0 -437 -22 0 -437 19 0 -104 -19 22 437 0 -436 105 0 -436 -23 0 -436 19 0 -105 -19 23 436 0 20 -28 442 441 440 0 -20 28 445 444 443 0 -442 93 0 -442 -20 0 -442 17 0 -93 -17 20 442 0 -441 98 0 -441 -20 0 -441 18 0 -98 -18 20 441 0 -440 102 0 -440 -20 0 -440 19 0 -102 -19 20 440 0 -445 106 0 -445 -21 0 -445 20 0 -106 -20 21 445 0 -444 107 0 -444 -22 0 -444 20 0 -107 -20 22 444 0 -443 108 0 -443 -23 0 -443 20 0 -108 -20 23 443 0 21 -29 449 448 447 446 0 -21 29 451 450 0 -449 94 0 -449 -21 0 -449 17 0 -94 -17 21 449 0 -448 99 0 -448 -21 0 -448 18 0 -99 -18 21 448 0 -447 103 0 -447 -21 0 -447 19 0 -103 -19 21 447 0 -446 106 0 -446 -21 0 -446 20 0 -106 -20 21 446 0 -451 109 0 -451 -22 0 -451 21 0 -109 -21 22 451 0 -450 110 0 -450 -23 0 -450 21 0 -110 -21 23 450 0 22 -30 456 455 454 453 452 0 -22 30 457 0 -456 95 0 -456 -22 0 -456 17 0 -95 -17 22 456 0 -455 100 0 -455 -22 0 -455 18 0 -100 -18 22 455 0 -454 104 0 -454 -22 0 -454 19 0 -104 -19 22 454 0 -453 107 0 -453 -22 0 -453 20 0 -107 -20 22 453 0 -452 109 0 -452 -22 0 -452 21 0 -109 -21 22 452 0 -457 111 0 -457 -23 0 -457 22 0 -111 -22 23 457 0 23 -31 463 462 461 460 459 458 0 -23 31 0 -463 96 0 -463 -23 0 -463 17 0 -96 -17 23 463 0 -462 101 0 -462 -23 0 -462 18 0 -101 -18 23 462 0 -461 105 0 -461 -23 0 -461 19 0 -105 -19 23 461 0 -460 108 0 -460 -23 0 -460 20 0 -108 -20 23 460 0 -459 110 0 -459 -23 0 -459 21 0 -110 -21 23 459 0 -458 111 0 -458 -23 0 -458 22 0 -111 -22 23 458 0 24 -32 0 -24 32 0 -91 -17 18 -25 0 -91 -17 18 26 0 -92 -17 19 -25 0 -92 -17 19 27 0 -93 -17 20 -25 0 -93 -17 20 28 0 -94 -17 21 -25 0 -94 -17 21 29 0 -95 -17 22 -25 0 -95 -17 22 30 0 -96 -17 23 -25 0 -96 -17 23 31 0 -97 -18 19 -26 0 -97 -18 19 27 0 -98 -18 20 -26 0 -98 -18 20 28 0 -99 -18 21 -26 0 -99 -18 21 29 0 -100 -18 22 -26 0 -100 -18 22 30 0 -101 -18 23 -26 0 -101 -18 23 31 0 -102 -19 20 -27 0 -102 -19 20 28 0 -103 -19 21 -27 0 -103 -19 21 29 0 -104 -19 22 -27 0 -104 -19 22 30 0 -105 -19 23 -27 0 -105 -19 23 31 0 -106 -20 21 -28 0 -106 -20 21 29 0 -107 -20 22 -28 0 -107 -20 22 30 0 -108 -20 23 -28 0 -108 -20 23 31 0 -109 -21 22 -29 0 -109 -21 22 30 0 -110 -21 23 -29 0 -110 -21 23 31 0 -111 -22 23 -30 0 -111 -22 23 31 0 -390 391 0 -96 391 0 -390 -96 0 -389 390 0 -95 390 0 -389 -95 0 -388 389 0 -94 389 0 -388 -94 0 -387 388 0 -93 388 0 -387 -93 0 -91 387 0 -92 387 0 -91 -92 0 -385 386 0 -101 386 0 -385 -101 0 -384 385 0 -100 385 0 -384 -100 0 -383 384 0 -99 384 0 -383 -99 0 -97 383 0 -98 383 0 -97 -98 0 -91 -101 0 -91 -100 0 -91 -99 0 -91 -98 0 -91 -97 0 -381 382 0 -105 382 0 -381 -105 0 -380 381 0 -104 381 0 -380 -104 0 -102 380 0 -103 380 0 -102 -103 0 -379 -105 0 -379 -104 0 -379 -103 0 -379 -102 0 -92 379 0 -97 379 0 -92 -97 0 -377 378 0 -108 378 0 -377 -108 0 -106 377 0 -107 377 0 -106 -107 0 -376 -108 0 -376 -107 0 -376 -106 0 -375 376 0 -102 376 0 -375 -102 0 -93 375 0 -98 375 0 -93 -98 0 -109 374 0 -110 374 0 -109 -110 0 -373 -110 0 -373 -109 0 -372 373 0 -106 373 0 -372 -106 0 -371 372 0 -103 372 0 -371 -103 0 -94 371 0 -99 371 0 -94 -99 0 -370 -111 0 -369 370 0 -109 370 0 -369 -109 0 -368 369 0 -107 369 0 -368 -107 0 -367 368 0 -104 368 0 -367 -104 0 -95 367 0 -100 367 0 -95 -100 0 -365 366 0 -111 366 0 -365 -111 0 -364 365 0 -110 365 0 -364 -110 0 -363 364 0 -108 364 0 -363 -108 0 -362 363 0 -105 363 0 -362 -105 0 -96 362 0 -101 362 0 -96 -101 0 -420 421 0 -91 421 0 -420 -91 0 -419 420 0 -92 420 0 -419 -92 0 -418 419 0 -93 419 0 -418 -93 0 -417 418 0 -94 418 0 -417 -94 0 -96 417 0 -95 417 0 -96 -95 0 -416 -91 0 -415 416 0 -97 416 0 -415 -97 0 -414 415 0 -98 415 0 -414 -98 0 -413 414 0 -99 414 0 -413 -99 0 -101 413 0 -100 413 0 -101 -100 0 -412 -92 0 -412 -97 0 -411 412 0 -102 412 0 -411 -102 0 -410 411 0 -103 411 0 -410 -103 0 -105 410 0 -104 410 0 -105 -104 0 -97 409 0 -92 409 0 -97 -92 0 -408 -93 0 -408 -98 0 -408 -102 0 -407 408 0 -106 408 0 -407 -106 0 -108 407 0 -107 407 0 -108 -107 0 -405 406 0 -93 406 0 -405 -93 0 -102 405 0 -98 405 0 -102 -98 0 -404 -94 0 -404 -99 0 -404 -103 0 -404 -106 0 -110 404 0 -109 404 0 -110 -109 0 -402 403 0 -94 403 0 -402 -94 0 -401 402 0 -99 402 0 -401 -99 0 -106 401 0 -103 401 0 -106 -103 0 -111 -95 0 -111 -100 0 -111 -104 0 -111 -107 0 -111 -109 0 -399 400 0 -95 400 0 -399 -95 0 -398 399 0 -100 399 0 -398 -100 0 -397 398 0 -104 398 0 -397 -104 0 -109 397 0 -107 397 0 -109 -107 0 -395 396 0 -96 396 0 -395 -96 0 -394 395 0 -101 395 0 -394 -101 0 -393 394 0 -105 394 0 -393 -105 0 -392 393 0 -108 393 0 -392 -108 0 -111 392 0 -110 392 0 -111 -110 0 25 -33 0 -25 33 529 528 527 526 525 524 0 -529 112 0 -529 -26 0 -529 25 0 -112 -25 26 529 0 -528 113 0 -528 -27 0 -528 25 0 -113 -25 27 528 0 -527 114 0 -527 -28 0 -527 25 0 -114 -25 28 527 0 -526 115 0 -526 -29 0 -526 25 0 -115 -25 29 526 0 -525 116 0 -525 -30 0 -525 25 0 -116 -25 30 525 0 -524 117 0 -524 -31 0 -524 25 0 -117 -25 31 524 0 26 -34 530 0 -26 34 535 534 533 532 531 0 -530 112 0 -530 -26 0 -530 25 0 -112 -25 26 530 0 -535 118 0 -535 -27 0 -535 26 0 -118 -26 27 535 0 -534 119 0 -534 -28 0 -534 26 0 -119 -26 28 534 0 -533 120 0 -533 -29 0 -533 26 0 -120 -26 29 533 0 -532 121 0 -532 -30 0 -532 26 0 -121 -26 30 532 0 -531 122 0 -531 -31 0 -531 26 0 -122 -26 31 531 0 27 -35 537 536 0 -27 35 541 540 539 538 0 -537 113 0 -537 -27 0 -537 25 0 -113 -25 27 537 0 -536 118 0 -536 -27 0 -536 26 0 -118 -26 27 536 0 -541 123 0 -541 -28 0 -541 27 0 -123 -27 28 541 0 -540 124 0 -540 -29 0 -540 27 0 -124 -27 29 540 0 -539 125 0 -539 -30 0 -539 27 0 -125 -27 30 539 0 -538 126 0 -538 -31 0 -538 27 0 -126 -27 31 538 0 28 -36 544 543 542 0 -28 36 547 546 545 0 -544 114 0 -544 -28 0 -544 25 0 -114 -25 28 544 0 -543 119 0 -543 -28 0 -543 26 0 -119 -26 28 543 0 -542 123 0 -542 -28 0 -542 27 0 -123 -27 28 542 0 -547 127 0 -547 -29 0 -547 28 0 -127 -28 29 547 0 -546 128 0 -546 -30 0 -546 28 0 -128 -28 30 546 0 -545 129 0 -545 -31 0 -545 28 0 -129 -28 31 545 0 29 -37 551 550 549 548 0 -29 37 553 552 0 -551 115 0 -551 -29 0 -551 25 0 -115 -25 29 551 0 -550 120 0 -550 -29 0 -550 26 0 -120 -26 29 550 0 -549 124 0 -549 -29 0 -549 27 0 -124 -27 29 549 0 -548 127 0 -548 -29 0 -548 28 0 -127 -28 29 548 0 -553 130 0 -553 -30 0 -553 29 0 -130 -29 30 553 0 -552 131 0 -552 -31 0 -552 29 0 -131 -29 31 552 0 30 -38 558 557 556 555 554 0 -30 38 559 0 -558 116 0 -558 -30 0 -558 25 0 -116 -25 30 558 0 -557 121 0 -557 -30 0 -557 26 0 -121 -26 30 557 0 -556 125 0 -556 -30 0 -556 27 0 -125 -27 30 556 0 -555 128 0 -555 -30 0 -555 28 0 -128 -28 30 555 0 -554 130 0 -554 -30 0 -554 29 0 -130 -29 30 554 0 -559 132 0 -559 -31 0 -559 30 0 -132 -30 31 559 0 31 -39 565 564 563 562 561 560 0 -31 39 0 -565 117 0 -565 -31 0 -565 25 0 -117 -25 31 565 0 -564 122 0 -564 -31 0 -564 26 0 -122 -26 31 564 0 -563 126 0 -563 -31 0 -563 27 0 -126 -27 31 563 0 -562 129 0 -562 -31 0 -562 28 0 -129 -28 31 562 0 -561 131 0 -561 -31 0 -561 29 0 -131 -29 31 561 0 -560 132 0 -560 -31 0 -560 30 0 -132 -30 31 560 0 32 -40 0 -32 40 0 -112 -25 26 -33 0 -112 -25 26 34 0 -113 -25 27 -33 0 -113 -25 27 35 0 -114 -25 28 -33 0 -114 -25 28 36 0 -115 -25 29 -33 0 -115 -25 29 37 0 -116 -25 30 -33 0 -116 -25 30 38 0 -117 -25 31 -33 0 -117 -25 31 39 0 -118 -26 27 -34 0 -118 -26 27 35 0 -119 -26 28 -34 0 -119 -26 28 36 0 -120 -26 29 -34 0 -120 -26 29 37 0 -121 -26 30 -34 0 -121 -26 30 38 0 -122 -26 31 -34 0 -122 -26 31 39 0 -123 -27 28 -35 0 -123 -27 28 36 0 -124 -27 29 -35 0 -124 -27 29 37 0 -125 -27 30 -35 0 -125 -27 30 38 0 -126 -27 31 -35 0 -126 -27 31 39 0 -127 -28 29 -36 0 -127 -28 29 37 0 -128 -28 30 -36 0 -128 -28 30 38 0 -129 -28 31 -36 0 -129 -28 31 39 0 -130 -29 30 -37 0 -130 -29 30 38 0 -131 -29 31 -37 0 -131 -29 31 39 0 -132 -30 31 -38 0 -132 -30 31 39 0 -492 493 0 -117 493 0 -492 -117 0 -491 492 0 -116 492 0 -491 -116 0 -490 491 0 -115 491 0 -490 -115 0 -489 490 0 -114 490 0 -489 -114 0 -112 489 0 -113 489 0 -112 -113 0 -487 488 0 -122 488 0 -487 -122 0 -486 487 0 -121 487 0 -486 -121 0 -485 486 0 -120 486 0 -485 -120 0 -118 485 0 -119 485 0 -118 -119 0 -112 -122 0 -112 -121 0 -112 -120 0 -112 -119 0 -112 -118 0 -483 484 0 -126 484 0 -483 -126 0 -482 483 0 -125 483 0 -482 -125 0 -123 482 0 -124 482 0 -123 -124 0 -481 -126 0 -481 -125 0 -481 -124 0 -481 -123 0 -113 481 0 -118 481 0 -113 -118 0 -479 480 0 -129 480 0 -479 -129 0 -127 479 0 -128 479 0 -127 -128 0 -478 -129 0 -478 -128 0 -478 -127 0 -477 478 0 -123 478 0 -477 -123 0 -114 477 0 -119 477 0 -114 -119 0 -130 476 0 -131 476 0 -130 -131 0 -475 -131 0 -475 -130 0 -474 475 0 -127 475 0 -474 -127 0 -473 474 0 -124 474 0 -473 -124 0 -115 473 0 -120 473 0 -115 -120 0 -472 -132 0 -471 472 0 -130 472 0 -471 -130 0 -470 471 0 -128 471 0 -470 -128 0 -469 470 0 -125 470 0 -469 -125 0 -116 469 0 -121 469 0 -116 -121 0 -467 468 0 -132 468 0 -467 -132 0 -466 467 0 -131 467 0 -466 -131 0 -465 466 0 -129 466 0 -465 -129 0 -464 465 0 -126 465 0 -464 -126 0 -117 464 0 -122 464 0 -117 -122 0 -522 523 0 -112 523 0 -522 -112 0 -521 522 0 -113 522 0 -521 -113 0 -520 521 0 -114 521 0 -520 -114 0 -519 520 0 -115 520 0 -519 -115 0 -117 519 0 -116 519 0 -117 -116 0 -518 -112 0 -517 518 0 -118 518 0 -517 -118 0 -516 517 0 -119 517 0 -516 -119 0 -515 516 0 -120 516 0 -515 -120 0 -122 515 0 -121 515 0 -122 -121 0 -514 -113 0 -514 -118 0 -513 514 0 -123 514 0 -513 -123 0 -512 513 0 -124 513 0 -512 -124 0 -126 512 0 -125 512 0 -126 -125 0 -118 511 0 -113 511 0 -118 -113 0 -510 -114 0 -510 -119 0 -510 -123 0 -509 510 0 -127 510 0 -509 -127 0 -129 509 0 -128 509 0 -129 -128 0 -507 508 0 -114 508 0 -507 -114 0 -123 507 0 -119 507 0 -123 -119 0 -506 -115 0 -506 -120 0 -506 -124 0 -506 -127 0 -131 506 0 -130 506 0 -131 -130 0 -504 505 0 -115 505 0 -504 -115 0 -503 504 0 -120 504 0 -503 -120 0 -127 503 0 -124 503 0 -127 -124 0 -132 -116 0 -132 -121 0 -132 -125 0 -132 -128 0 -132 -130 0 -501 502 0 -116 502 0 -501 -116 0 -500 501 0 -121 501 0 -500 -121 0 -499 500 0 -125 500 0 -499 -125 0 -130 499 0 -128 499 0 -130 -128 0 -497 498 0 -117 498 0 -497 -117 0 -496 497 0 -122 497 0 -496 -122 0 -495 496 0 -126 496 0 -495 -126 0 -494 495 0 -129 495 0 -494 -129 0 -132 494 0 -131 494 0 -132 -131 0 33 -41 0 -33 41 631 630 629 628 627 626 0 -631 133 0 -631 -34 0 -631 33 0 -133 -33 34 631 0 -630 134 0 -630 -35 0 -630 33 0 -134 -33 35 630 0 -629 135 0 -629 -36 0 -629 33 0 -135 -33 36 629 0 -628 136 0 -628 -37 0 -628 33 0 -136 -33 37 628 0 -627 137 0 -627 -38 0 -627 33 0 -137 -33 38 627 0 -626 138 0 -626 -39 0 -626 33 0 -138 -33 39 626 0 34 -42 632 0 -34 42 637 636 635 634 633 0 -632 133 0 -632 -34 0 -632 33 0 -133 -33 34 632 0 -637 139 0 -637 -35 0 -637 34 0 -139 -34 35 637 0 -636 140 0 -636 -36 0 -636 34 0 -140 -34 36 636 0 -635 141 0 -635 -37 0 -635 34 0 -141 -34 37 635 0 -634 142 0 -634 -38 0 -634 34 0 -142 -34 38 634 0 -633 143 0 -633 -39 0 -633 34 0 -143 -34 39 633 0 35 -43 639 638 0 -35 43 643 642 641 640 0 -639 134 0 -639 -35 0 -639 33 0 -134 -33 35 639 0 -638 139 0 -638 -35 0 -638 34 0 -139 -34 35 638 0 -643 144 0 -643 -36 0 -643 35 0 -144 -35 36 643 0 -642 145 0 -642 -37 0 -642 35 0 -145 -35 37 642 0 -641 146 0 -641 -38 0 -641 35 0 -146 -35 38 641 0 -640 147 0 -640 -39 0 -640 35 0 -147 -35 39 640 0 36 -44 646 645 644 0 -36 44 649 648 647 0 -646 135 0 -646 -36 0 -646 33 0 -135 -33 36 646 0 -645 140 0 -645 -36 0 -645 34 0 -140 -34 36 645 0 -644 144 0 -644 -36 0 -644 35 0 -144 -35 36 644 0 -649 148 0 -649 -37 0 -649 36 0 -148 -36 37 649 0 -648 149 0 -648 -38 0 -648 36 0 -149 -36 38 648 0 -647 150 0 -647 -39 0 -647 36 0 -150 -36 39 647 0 37 -45 653 652 651 650 0 -37 45 655 654 0 -653 136 0 -653 -37 0 -653 33 0 -136 -33 37 653 0 -652 141 0 -652 -37 0 -652 34 0 -141 -34 37 652 0 -651 145 0 -651 -37 0 -651 35 0 -145 -35 37 651 0 -650 148 0 -650 -37 0 -650 36 0 -148 -36 37 650 0 -655 151 0 -655 -38 0 -655 37 0 -151 -37 38 655 0 -654 152 0 -654 -39 0 -654 37 0 -152 -37 39 654 0 38 -46 660 659 658 657 656 0 -38 46 661 0 -660 137 0 -660 -38 0 -660 33 0 -137 -33 38 660 0 -659 142 0 -659 -38 0 -659 34 0 -142 -34 38 659 0 -658 146 0 -658 -38 0 -658 35 0 -146 -35 38 658 0 -657 149 0 -657 -38 0 -657 36 0 -149 -36 38 657 0 -656 151 0 -656 -38 0 -656 37 0 -151 -37 38 656 0 -661 153 0 -661 -39 0 -661 38 0 -153 -38 39 661 0 39 -47 667 666 665 664 663 662 0 -39 47 0 -667 138 0 -667 -39 0 -667 33 0 -138 -33 39 667 0 -666 143 0 -666 -39 0 -666 34 0 -143 -34 39 666 0 -665 147 0 -665 -39 0 -665 35 0 -147 -35 39 665 0 -664 150 0 -664 -39 0 -664 36 0 -150 -36 39 664 0 -663 152 0 -663 -39 0 -663 37 0 -152 -37 39 663 0 -662 153 0 -662 -39 0 -662 38 0 -153 -38 39 662 0 40 -48 0 -40 48 0 -133 -33 34 -41 0 -133 -33 34 42 0 -134 -33 35 -41 0 -134 -33 35 43 0 -135 -33 36 -41 0 -135 -33 36 44 0 -136 -33 37 -41 0 -136 -33 37 45 0 -137 -33 38 -41 0 -137 -33 38 46 0 -138 -33 39 -41 0 -138 -33 39 47 0 -139 -34 35 -42 0 -139 -34 35 43 0 -140 -34 36 -42 0 -140 -34 36 44 0 -141 -34 37 -42 0 -141 -34 37 45 0 -142 -34 38 -42 0 -142 -34 38 46 0 -143 -34 39 -42 0 -143 -34 39 47 0 -144 -35 36 -43 0 -144 -35 36 44 0 -145 -35 37 -43 0 -145 -35 37 45 0 -146 -35 38 -43 0 -146 -35 38 46 0 -147 -35 39 -43 0 -147 -35 39 47 0 -148 -36 37 -44 0 -148 -36 37 45 0 -149 -36 38 -44 0 -149 -36 38 46 0 -150 -36 39 -44 0 -150 -36 39 47 0 -151 -37 38 -45 0 -151 -37 38 46 0 -152 -37 39 -45 0 -152 -37 39 47 0 -153 -38 39 -46 0 -153 -38 39 47 0 -594 595 0 -138 595 0 -594 -138 0 -593 594 0 -137 594 0 -593 -137 0 -592 593 0 -136 593 0 -592 -136 0 -591 592 0 -135 592 0 -591 -135 0 -133 591 0 -134 591 0 -133 -134 0 -589 590 0 -143 590 0 -589 -143 0 -588 589 0 -142 589 0 -588 -142 0 -587 588 0 -141 588 0 -587 -141 0 -139 587 0 -140 587 0 -139 -140 0 -133 -143 0 -133 -142 0 -133 -141 0 -133 -140 0 -133 -139 0 -585 586 0 -147 586 0 -585 -147 0 -584 585 0 -146 585 0 -584 -146 0 -144 584 0 -145 584 0 -144 -145 0 -583 -147 0 -583 -146 0 -583 -145 0 -583 -144 0 -134 583 0 -139 583 0 -134 -139 0 -581 582 0 -150 582 0 -581 -150 0 -148 581 0 -149 581 0 -148 -149 0 -580 -150 0 -580 -149 0 -580 -148 0 -579 580 0 -144 580 0 -579 -144 0 -135 579 0 -140 579 0 -135 -140 0 -151 578 0 -152 578 0 -151 -152 0 -577 -152 0 -577 -151 0 -576 577 0 -148 577 0 -576 -148 0 -575 576 0 -145 576 0 -575 -145 0 -136 575 0 -141 575 0 -136 -141 0 -574 -153 0 -573 574 0 -151 574 0 -573 -151 0 -572 573 0 -149 573 0 -572 -149 0 -571 572 0 -146 572 0 -571 -146 0 -137 571 0 -142 571 0 -137 -142 0 -569 570 0 -153 570 0 -569 -153 0 -568 569 0 -152 569 0 -568 -152 0 -567 568 0 -150 568 0 -567 -150 0 -566 567 0 -147 567 0 -566 -147 0 -138 566 0 -143 566 0 -138 -143 0 -624 625 0 -133 625 0 -624 -133 0 -623 624 0 -134 624 0 -623 -134 0 -622 623 0 -135 623 0 -622 -135 0 -621 622 0 -136 622 0 -621 -136 0 -138 621 0 -137 621 0 -138 -137 0 -620 -133 0 -619 620 0 -139 620 0 -619 -139 0 -618 619 0 -140 619 0 -618 -140 0 -617 618 0 -141 618 0 -617 -141 0 -143 617 0 -142 617 0 -143 -142 0 -616 -134 0 -616 -139 0 -615 616 0 -144 616 0 -615 -144 0 -614 615 0 -145 615 0 -614 -145 0 -147 614 0 -146 614 0 -147 -146 0 -139 613 0 -134 613 0 -139 -134 0 -612 -135 0 -612 -140 0 -612 -144 0 -611 612 0 -148 612 0 -611 -148 0 -150 611 0 -149 611 0 -150 -149 0 -609 610 0 -135 610 0 -609 -135 0 -144 609 0 -140 609 0 -144 -140 0 -608 -136 0 -608 -141 0 -608 -145 0 -608 -148 0 -152 608 0 -151 608 0 -152 -151 0 -606 607 0 -136 607 0 -606 -136 0 -605 606 0 -141 606 0 -605 -141 0 -148 605 0 -145 605 0 -148 -145 0 -153 -137 0 -153 -142 0 -153 -146 0 -153 -149 0 -153 -151 0 -603 604 0 -137 604 0 -603 -137 0 -602 603 0 -142 603 0 -602 -142 0 -601 602 0 -146 602 0 -601 -146 0 -151 601 0 -149 601 0 -151 -149 0 -599 600 0 -138 600 0 -599 -138 0 -598 599 0 -143 599 0 -598 -143 0 -597 598 0 -147 598 0 -597 -147 0 -596 597 0 -150 597 0 -596 -150 0 -153 596 0 -152 596 0 -153 -152 0