c ind 2 3 4 5 6 7 8 9 0
c ind 10 11 12 13 14 15 16 17 18 19 0
c ind 20 21 22 23 24 25 26 27 28 29 0
c ind 30 31 32 33 34 35 36 37 38 39 0
c ind 40 41 42 43 44 45 46 47 48 49 0
c ind 50 51 52 53 54 55 56 57 58 59 0
c ind 60 61 62 63 64 65 66 67 68 69 0
c ind 70 71 72 73 74 75 76 77 78 79 0
c ind 80 81 82 83 84 85 86 87 88 89 0
c ind 90 91 92 93 94 95 96 97 98 99 0
c ind 100 101 102 103 104 105 106 107 108 109 0
c ind 110 111 112 113 114 115 116 117 118 119 0
c ind 120 121 122 123 124 125 126 127 128 129 0
c ind 130 131 132 133 134 135 136 137 138 139 0
c ind 140 141 142 143 144 145 146 147 148 149 0
c ind 150 151 152 153 154 155 156 157 158 159 0
c ind 160 161 162 163 164 165 166 167 168 169 0
c ind 170 171 172 173 174 175 176 177 178 179 0
c ind 180 181 182 183 184 185 186 187 188 189 0
c ind 190 191 192 193 194 195 196 197 198 199 0
c ind 200 201 202 203 204 205 206 207 208 209 0
c ind 210 211 212 213 214 215 216 217 218 219 0
c ind 220 221 222 223 224 225 226 227 228 229 0
c ind 230 231 232 233 234 235 236 237 238 239 0
c ind 240 241 242 243 244 245 246 247 248 249 0
c ind 250 251 252 253 254 255 256 257 258 259 0
c ind 260 261 262 263 264 265 266 267 268 269 0
c ind 270 271 272 273 274 275 276 277 278 279 0
c ind 280 281 282 283 284 285 286 287 288 289 0
c ind 290 291 292 293 294 295 296 297 298 299 0
c ind 300 301 302 303 304 305 306 307 308 309 0
c ind 310 311 312 313 314 315 316 317 318 319 0
c ind 320 321 322 323 324 325 326 327 328 329 0
c ind 330 331 332 333 334 335 336 337 338 339 0
c ind 340 341 342 343 344 345 346 347 348 349 0
c ind 350 351 352 353 354 355 356 357 358 359 0
c ind 360 361 362 363 364 365 366 367 368 369 0
c ind 370 371 372 373 374 375 376 377 378 379 0
c ind 380 381 382 383 384 385 386 387 388 389 0
c ind 390 391 392 393 394 395 396 397 398 399 0
c ind 400 401 402 403 404 405 406 407 408 409 0
c ind 410 411 412 413 414 415 416 417 418 419 0
c ind 420 421 422 423 424 425 426 427 428 429 0
c ind 430 431 432 433 434 435 436 437 438 439 0
c ind 440 441 442 443 444 445 446 447 448 449 0
c ind 450 451 452 453 454 455 456 457 458 459 0
c ind 460 461 462 463 464 465 466 467 468 469 0
c ind 470 471 472 473 474 475 476 477 478 479 0
c ind 480 481 482 483 484 485 486 487 488 489 0
c ind 490 491 492 493 494 495 496 497 498 499 0
c ind 500 501 502 503 504 505 506 507 508 509 0
c ind 510 511 512 513 514 515 516 517 518 519 0
c ind 520 521 522 523 524 525 526 527 528 529 0
c ind 530 531 532 533 534 535 536 537 538 539 0
c ind 540 541 542 543 544 545 546 547 548 549 0
c ind 550 551 552 553 554 555 556 557 558 559 0
c ind 560 561 562 563 564 565 566 567 568 569 0
c ind 570 571 572 573 574 575 576 577 578 579 0
c ind 580 581 582 583 584 585 586 587 588 589 0
c ind 590 591 592 593 594 595 596 597 598 599 0
c ind 600 601 602 603 604 605 606 607 608 609 0
c ind 610 611 612 613 614 615 616 617 618 619 0
c ind 620 621 622 623 624 625 626 627 628 629 0
c ind 630 631 632 633 634 635 636 637 638 639 0
c ind 640 641 642 643 644 645 646 647 648 649 0
c ind 650 651 652 653 654 655 656 657 658 659 0
c ind 660 661 662 663 664 665 666 667 668 669 0
c ind 670 671 672 673 674 675 676 677 678 679 0
c ind 680 681 682 683 684 685 686 687 688 689 0
c ind 690 691 692 693 694 695 696 697 698 699 0
c ind 700 701 702 703 704 705 706 707 708 709 0
c ind 710 711 712 713 714 715 716 717 718 719 0
c ind 720 721 722 723 724 725 726 727 728 729 0
c ind 730 731 732 733 734 735 736 737 738 739 0
c ind 740 741 742 743 744 745 746 747 748 749 0
c ind 750 751 752 753 754 755 756 757 758 759 0
c ind 760 761 762 763 764 765 766 767 768 769 0
c ind 770 771 772 773 774 775 776 777 778 779 0
c ind 780 781 782 783 784 785 786 787 788 789 0
c ind 790 791 792 793 794 795 796 797 798 799 0
c ind 800 801 802 803 804 805 806 807 808 809 0
c ind 810 811 812 813 814 815 816 817 818 819 0
c ind 820 821 822 823 824 825 826 827 828 829 0
c ind 830 831 832 833 834 835 836 837 838 839 0
c ind 840 841 842 843 844 845 846 847 848 849 0
c ind 850 851 852 853 854 855 856 857 858 859 0
c ind 860 861 862 863 864 865 866 867 868 869 0
c ind 870 871 872 873 874 875 876 877 878 879 0
c ind 880 881 882 883 884 885 886 887 888 889 0
c ind 890 891 892 893 894 895 896 897 898 899 0
c ind 900 901 902 903 904 905 906 907 908 909 0
c ind 910 911 912 913 914 915 916 917 918 919 0
c ind 920 921 922 923 924 925 926 927 928 929 0
c ind 930 931 932 933 934 935 936 937 938 939 0
c ind 940 941 942 943 944 945 946 947 948 949 0
c ind 950 951 952 953 954 955 956 957 958 959 0
c ind 960 961 962 963 964 965 966 967 968 969 0
c ind 970 971 972 973 974 975 976 977 978 979 0
c ind 980 981 982 983 984 985 986 987 988 989 0
c ind 990 991 992 993 994 995 996 997 998 999 0
c ind 1000 1001 1002 1003 1004 1005 1006 1007 1008 1009 0
c ind 1010 1011 1012 1013 1014 1015 1016 1017 1018 1019 0
c ind 1020 1021 1022 1023 1024 1025 0
p cnf 1026 961
1026 0
-677 0
-676 0
675 0
-674 0
-133 0
-132 0
131 0
-130 0
-29 0
28 0
27 0
-26 0
-205 0
204 0
-203 0
202 0
-389 0
388 0
387 0
-386 0
65 0
64 0
63 0
62 0
-25 0
24 0
-23 0
22 0
53 0
52 0
-51 0
-50 0
225 0
-224 0
223 0
-222 0
-9 0
-8 0
-7 0
6 0
-261 0
260 0
-259 0
-258 0
-329 0
328 0
327 0
-326 0
-685 0
684 0
-683 0
-682 0
-937 0
936 0
935 0
934 0
-73 0
-72 0
71 0
-70 0
585 0
-584 0
583 0
-582 0
-153 0
152 0
151 0
150 0
277 0
-276 0
-275 0
-274 0
289 0
-288 0
287 0
286 0
-269 0
268 0
267 0
-266 0
161 0
-160 0
-159 0
158 0
37 0
-36 0
-35 0
-34 0
-613 0
-612 0
-611 0
610 0
517 0
-516 0
-515 0
-514 0
61 0
60 0
59 0
-58 0
-137 0
-136 0
135 0
134 0
-21 0
20 0
-19 0
-18 0
645 0
-644 0
643 0
-642 0
-17 0
-16 0
15 0
14 0
285 0
-284 0
283 0
-282 0
105 0
-104 0
103 0
-102 0
45 0
-44 0
43 0
-42 0
837 0
836 0
-835 0
834 0
-325 0
324 0
-323 0
322 0
229 0
-228 0
227 0
226 0
-13 0
-12 0
11 0
-10 0
185 0
184 0
183 0
182 0
281 0
-280 0
-279 0
278 0
109 0
-108 0
107 0
106 0
777 0
776 0
-775 0
774 0
-929 0
928 0
-927 0
926 0
-933 0
932 0
931 0
-930 0
-805 0
804 0
-803 0
-802 0
-509 0
508 0
-507 0
506 0
421 0
420 0
419 0
-418 0
-333 0
332 0
331 0
330 0
113 0
112 0
-111 0
-110 0
773 0
772 0
-771 0
-770 0
165 0
-164 0
163 0
-162 0
525 0
-524 0
523 0
-522 0
-373 0
-372 0
-371 0
370 0
-141 0
140 0
-139 0
-138 0
781 0
780 0
779 0
-778 0
-85 0
84 0
-83 0
82 0
125 0
124 0
123 0
122 0
-69 0
-68 0
-67 0
66 0
357 0
356 0
-355 0
354 0
241 0
240 0
239 0
-238 0
701 0
-700 0
-699 0
-698 0
221 0
-220 0
-219 0
218 0
597 0
596 0
-595 0
594 0
833 0
-832 0
831 0
830 0
173 0
172 0
-171 0
-170 0
-553 0
-552 0
-551 0
550 0
485 0
484 0
483 0
482 0
293 0
292 0
-291 0
-290 0
521 0
-520 0
-519 0
518 0
-149 0
148 0
147 0
-146 0
-273 0
272 0
271 0
270 0
581 0
-580 0
-579 0
578 0
177 0
176 0
-175 0
174 0
-197 0
-196 0
195 0
194 0
-621 0
-620 0
619 0
618 0
709 0
-708 0
707 0
706 0
57 0
56 0
-55 0
54 0
397 0
-396 0
-395 0
-394 0
533 0
532 0
-531 0
-530 0
-265 0
264 0
-263 0
262 0
657 0
656 0
-655 0
654 0
717 0
716 0
-715 0
714 0
-565 0
564 0
-563 0
-562 0
97 0
-96 0
-95 0
-94 0
-89 0
88 0
87 0
-86 0
-693 0
692 0
691 0
-690 0
361 0
360 0
359 0
-358 0
653 0
652 0
-651 0
-650 0
-393 0
392 0
391 0
390 0
117 0
116 0
-115 0
114 0
157 0
-156 0
-155 0
-154 0
-77 0
-76 0
75 0
74 0
-321 0
-320 0
319 0
318 0
41 0
-40 0
-39 0
38 0
-817 0
816 0
815 0
814 0
401 0
-400 0
-399 0
398 0
-453 0
452 0
451 0
450 0
537 0
536 0
-535 0
534 0
721 0
720 0
719 0
-718 0
101 0
-100 0
-99 0
98 0
821 0
-820 0
-819 0
-818 0
901 0
900 0
899 0
-898 0
-689 0
688 0
-687 0
686 0
725 0
724 0
723 0
722 0
349 0
-348 0
347 0
346 0
245 0
244 0
243 0
242 0
-93 0
92 0
91 0
90 0
-253 0
-252 0
-251 0
250 0
337 0
-336 0
-335 0
-334 0
301 0
300 0
299 0
-298 0
457 0
-456 0
-455 0
-454 0
661 0
660 0
659 0
-658 0
593 0
592 0
-591 0
-590 0
461 0
-460 0
-459 0
458 0
605 0
604 0
603 0
602 0
953 0
-952 0
951 0
950 0
905 0
904 0
903 0
902 0
1021 0
1020 0
-1019 0
1018 0
-145 0
144 0
-143 0
142 0
181 0
180 0
179 0
-178 0
-201 0
200 0
-199 0
-198 0
845 0
844 0
843 0
842 0
-877 0
876 0
875 0
874 0
545 0
544 0
543 0
542 0
957 0
956 0
-955 0
-954 0
529 0
-528 0
527 0
526 0
-809 0
808 0
-807 0
806 0
-797 0
-796 0
795 0
-794 0
-33 0
32 0
31 0
30 0
169 0
-168 0
167 0
166 0
353 0
352 0
-351 0
-350 0
541 0
540 0
539 0
-538 0
-741 0
-740 0
739 0
738 0
-313 0
-312 0
-311 0
310 0
341 0
-340 0
-339 0
338 0
217 0
-216 0
-215 0
-214 0
-441 0
-440 0
439 0
438 0
-801 0
-800 0
799 0
798 0
297 0
296 0
-295 0
294 0
-213 0
212 0
211 0
210 0
-629 0
628 0
-627 0
626 0
-569 0
568 0
-567 0
566 0
-81 0
80 0
-79 0
-78 0
-633 0
632 0
631 0
-630 0
-997 0
996 0
995 0
994 0
-865 0
864 0
-863 0
-862 0
417 0
416 0
-415 0
414 0
649 0
-648 0
647 0
646 0
-869 0
868 0
-867 0
866 0
49 0
-48 0
47 0
46 0
413 0
412 0
-411 0
-410 0
233 0
232 0
-231 0
-230 0
-557 0
-556 0
555 0
-554 0
345 0
-344 0
343 0
-342 0
-813 0
812 0
811 0
-810 0
425 0
424 0
423 0
422 0
941 0
-940 0
-939 0
-938 0
-985 0
984 0
-983 0
-982 0
-733 0
-732 0
-731 0
730 0
305 0
304 0
303 0
302 0
405 0
-404 0
403 0
-402 0
-437 0
-436 0
435 0
-434 0
-925 0
924 0
-923 0
-922 0
-445 0
444 0
-443 0
-442 0
-617 0
-616 0
615 0
-614 0
-573 0
572 0
571 0
-570 0
-981 0
-980 0
979 0
978 0
477 0
476 0
-475 0
474 0
589 0
-588 0
587 0
586 0
365 0
364 0
363 0
362 0
469 0
-468 0
467 0
466 0
-921 0
-920 0
919 0
918 0
-745 0
744 0
-743 0
-742 0
-561 0
-560 0
559 0
558 0
713 0
712 0
-711 0
-710 0
-625 0
624 0
-623 0
-622 0
829 0
-828 0
827 0
-826 0
237 0
236 0
-235 0
234 0
705 0
-704 0
-703 0
702 0
473 0
472 0
-471 0
-470 0
-673 0
-672 0
-671 0
670 0
1001 0
-1000 0
-999 0
-998 0
-853 0
-852 0
-851 0
850 0
881 0
-880 0
-879 0
-878 0
-493 0
-492 0
-491 0
490 0
761 0
-760 0
-759 0
-758 0
-757 0
756 0
755 0
754 0
641 0
-640 0
-639 0
-638 0
-209 0
208 0
207 0
-206 0
-917 0
-916 0
915 0
-914 0
-505 0
504 0
-503 0
-502 0
-317 0
-316 0
315 0
-314 0
121 0
120 0
119 0
-118 0
-385 0
384 0
-383 0
-382 0
-637 0
636 0
635 0
634 0
841 0
840 0
839 0
-838 0
-857 0
-856 0
855 0
-854 0
1017 0
1016 0
-1015 0
-1014 0
465 0
-464 0
463 0
-462 0
897 0
896 0
-895 0
-894 0
-577 0
576 0
575 0
574 0
965 0
964 0
963 0
962 0
785 0
784 0
783 0
782 0
-973 0
-972 0
-971 0
970 0
-913 0
-912 0
-911 0
910 0
945 0
-944 0
-943 0
942 0
409 0
-408 0
407 0
406 0
-977 0
-976 0
975 0
-974 0
-681 0
-680 0
679 0
678 0
765 0
-764 0
-763 0
762 0
-697 0
696 0
695 0
694 0
-873 0
872 0
871 0
-870 0
-433 0
-432 0
-431 0
430 0
-749 0
748 0
-747 0
746 0
-497 0
-496 0
495 0
-494 0
-793 0
-792 0
-791 0
790 0
961 0
960 0
-959 0
958 0
-193 0
-192 0
-191 0
190 0
-753 0
752 0
751 0
-750 0
885 0
-884 0
-883 0
882 0
481 0
480 0
479 0
-478 0
-501 0
-500 0
499 0
498 0
-989 0
988 0
-987 0
986 0
1005 0
-1004 0
-1003 0
1002 0
1009 0
-1008 0
1007 0
-1006 0
601 0
600 0
599 0
-598 0
949 0
-948 0
947 0
-946 0
825 0
-824 0
-823 0
822 0
889 0
-888 0
887 0
-886 0
893 0
-892 0
891 0
890 0
769 0
-768 0
767 0
-766 0
1013 0
-1012 0
1011 0
1010 0
1025 0
1024 0
1023 0
-1022 0
-449 0
448 0
-447 0
446 0
-381 0
-380 0
379 0
378 0
-861 0
-860 0
859 0
858 0
665 0
664 0
663 0
662 0
-377 0
-376 0
375 0
-374 0
-257 0
-256 0
255 0
-254 0
-513 0
512 0
511 0
-510 0
-993 0
992 0
991 0
-990 0
-737 0
-736 0
735 0
-734 0