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