MAIN BEGIN : [Thu Jun 1 15:59:10 2006] READ BEGIN : csp/la16.csp [Thu Jun 1 15:59:10 2006] READ END : csp/la16.csp (1 seconds) [Thu Jun 1 15:59:11 2006] READ CPU : 1.4 = 1.4 + 0 + 0 + 0 # BOUND : makespan 717 1230 GENERATE_CNF 1230 BEGIN : [Thu Jun 1 15:59:11 2006] GENERATE_CNF 1230 END : 124715 variables 1296251 clauses 29091873 bytes (63 seconds) [Thu Jun 1 16:00:14 2006] GENERATE_CNF 1230 CPU : 62.84 = 62.76 + 0.08 + 0 + 0 MODIFY_CNF 973 BEGIN : [Thu Jun 1 16:00:14 2006] MODIFY_CNF 973 END : 29091879 bytes (0 seconds) [Thu Jun 1 16:00:14 2006] MODIFY_CNF 973 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 973 BEGIN : [Thu Jun 1 16:00:14 2006] CMD : minisat /work/tamura/csp2sat29658.cnf /work/tamura/csp2sat29658.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 556209 1624152 | 185403 0 0 NaNQ | 0.000 % | | 100 | 556209 1624152 | 203943 100 1077 10.8 | 64.033 % | | 250 | 556209 1624152 | 224337 250 2603 10.4 | 64.033 % | | 477 | 556209 1624152 | 246771 477 4572 9.6 | 64.033 % | | 814 | 556209 1624152 | 271448 814 7362 9.0 | 64.033 % | ==============================================================================) restarts : 5 conflicts : 904 (261 /sec) decisions : 1424 (411 /sec) propagations : 5132922 (1480715 /sec) inspects : 34931716 (10076897 /sec) conflict literals : 8202 (26.32 % deleted) CPU time : 3.46651 s SATISFIABLE VERIFY_CNF 973 END : (4 seconds) [Thu Jun 1 16:00:18 2006] VERIFY_CNF 973 CPU : 3.86 = 0.0100000000000051 + 0.00999999999999995 + 3.81 + 0.03 # RESULT : makespan 973 SATISFIABLE SHOW_RESULT 973 BEGIN : [Thu Jun 1 16:00:18 2006] # ASSIGN : makespan 973 # ASSIGN : s_0_0 76 # ASSIGN : s_0_1 97 # ASSIGN : s_0_2 168 # ASSIGN : s_0_3 353 # ASSIGN : s_0_4 405 # ASSIGN : s_0_5 517 # ASSIGN : s_0_6 551 # ASSIGN : s_0_7 604 # ASSIGN : s_0_8 625 # ASSIGN : s_0_9 680 # ASSIGN : s_1_0 81 # ASSIGN : s_1_1 362 # ASSIGN : s_1_2 418 # ASSIGN : s_1_3 516 # ASSIGN : s_1_4 624 # ASSIGN : s_1_5 672 # ASSIGN : s_1_6 738 # ASSIGN : s_1_7 780 # ASSIGN : s_1_8 857 # ASSIGN : s_1_9 934 # ASSIGN : s_2_0 9 # ASSIGN : s_2_1 43 # ASSIGN : s_2_2 149 # ASSIGN : s_2_3 211 # ASSIGN : s_2_4 230 # ASSIGN : s_2_5 322 # ASSIGN : s_2_6 474 # ASSIGN : s_2_7 546 # ASSIGN : s_2_8 636 # ASSIGN : s_2_9 775 # ASSIGN : s_3_0 124 # ASSIGN : s_3_1 229 # ASSIGN : s_3_2 430 # ASSIGN : s_3_3 517 # ASSIGN : s_3_4 571 # ASSIGN : s_3_5 595 # ASSIGN : s_3_6 678 # ASSIGN : s_3_7 719 # ASSIGN : s_3_8 812 # ASSIGN : s_3_9 913 # ASSIGN : s_4_0 107 # ASSIGN : s_4_1 220 # ASSIGN : s_4_2 319 # ASSIGN : s_4_3 344 # ASSIGN : s_4_4 431 # ASSIGN : s_4_5 631 # ASSIGN : s_4_6 680 # ASSIGN : s_4_7 776 # ASSIGN : s_4_8 877 # ASSIGN : s_4_9 894 # ASSIGN : s_5_0 8 # ASSIGN : s_5_1 54 # ASSIGN : s_5_2 130 # ASSIGN : s_5_3 158 # ASSIGN : s_5_4 169 # ASSIGN : s_5_5 335 # ASSIGN : s_5_6 387 # ASSIGN : s_5_7 622 # ASSIGN : s_5_8 703 # ASSIGN : s_5_9 780 # ASSIGN : s_6_0 189 # ASSIGN : s_6_1 205 # ASSIGN : s_6_2 264 # ASSIGN : s_6_3 310 # ASSIGN : s_6_4 401 # ASSIGN : s_6_5 444 # ASSIGN : s_6_6 494 # ASSIGN : s_6_7 612 # ASSIGN : s_6_8 847 # ASSIGN : s_6_9 875 # ASSIGN : s_7_0 31 # ASSIGN : s_7_1 133 # ASSIGN : s_7_2 298 # ASSIGN : s_7_3 339 # ASSIGN : s_7_4 419 # ASSIGN : s_7_5 473 # ASSIGN : s_7_6 657 # ASSIGN : s_7_7 671 # ASSIGN : s_7_8 863 # ASSIGN : s_7_9 902 # ASSIGN : s_8_0 136 # ASSIGN : s_8_1 393 # ASSIGN : s_8_2 500 # ASSIGN : s_8_3 566 # ASSIGN : s_8_4 599 # ASSIGN : s_8_5 664 # ASSIGN : s_8_6 710 # ASSIGN : s_8_7 764 # ASSIGN : s_8_8 853 # ASSIGN : s_8_9 895 # ASSIGN : s_9_0 80 # ASSIGN : s_9_1 184 # ASSIGN : s_9_2 265 # ASSIGN : s_9_3 359 # ASSIGN : s_9_4 455 # ASSIGN : s_9_5 482 # ASSIGN : s_9_6 555 # ASSIGN : s_9_7 600 # ASSIGN : s_9_8 815 # ASSIGN : s_9_9 889 SHOW_RESULT 973 END : 973 (0 seconds) [Thu Jun 1 16:00:18 2006] SHOW_RESULT 973 CPU : 0.349999999999994 = 0.349999999999994 + 0 + 0 + 0 # BOUND : makespan 717 973 MODIFY_CNF 845 BEGIN : [Thu Jun 1 16:00:18 2006] MODIFY_CNF 845 END : 29091879 bytes (0 seconds) [Thu Jun 1 16:00:18 2006] MODIFY_CNF 845 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 845 BEGIN : [Thu Jun 1 16:00:18 2006] CMD : minisat /work/tamura/csp2sat29658.cnf /work/tamura/csp2sat29658.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 392302 1145784 | 130767 0 0 NaNQ | 0.000 % | ==============================================================================) restarts : 1 conflicts : 10 (6 /sec) decisions : 14 (8 /sec) propagations : 129378 (73949 /sec) inspects : 692041 (395554 /sec) conflict literals : 15 (37.50 % deleted) CPU time : 1.74955 s UNSATISFIABLE VERIFY_CNF 845 END : (3 seconds) [Thu Jun 1 16:00:21 2006] VERIFY_CNF 845 CPU : 2.05 = 0.0100000000000051 + 0.01 + 2 + 0.03 # RESULT : makespan 845 UNSATISFIABLE # BOUND : makespan 846 973 MODIFY_CNF 909 BEGIN : [Thu Jun 1 16:00:21 2006] MODIFY_CNF 909 END : 29091879 bytes (0 seconds) [Thu Jun 1 16:00:21 2006] MODIFY_CNF 909 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 909 BEGIN : [Thu Jun 1 16:00:21 2006] CMD : minisat /work/tamura/csp2sat29658.cnf /work/tamura/csp2sat29658.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 478718 1398179 | 159572 0 0 NaNQ | 0.000 % | | 100 | 478718 1398179 | 175529 99 944 9.5 | 69.260 % | ==============================================================================) restarts : 2 conflicts : 193 (89 /sec) decisions : 237 (110 /sec) propagations : 1315331 (607808 /sec) inspects : 7443015 (3439380 /sec) conflict literals : 1409 (30.00 % deleted) CPU time : 2.16406 s UNSATISFIABLE VERIFY_CNF 909 END : (2 seconds) [Thu Jun 1 16:00:23 2006] VERIFY_CNF 909 CPU : 2.5 = 0 + 0 + 2.46 + 0.04 # RESULT : makespan 909 UNSATISFIABLE # BOUND : makespan 910 973 MODIFY_CNF 941 BEGIN : [Thu Jun 1 16:00:23 2006] MODIFY_CNF 941 END : 29091879 bytes (0 seconds) [Thu Jun 1 16:00:23 2006] MODIFY_CNF 941 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 941 BEGIN : [Thu Jun 1 16:00:23 2006] CMD : minisat /work/tamura/csp2sat29658.cnf /work/tamura/csp2sat29658.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 520191 1519341 | 173397 0 0 NaNQ | 0.000 % | | 100 | 520191 1519341 | 190736 98 786 8.0 | 66.659 % | | 250 | 520191 1519341 | 209810 247 1665 6.7 | 67.316 % | | 475 | 520191 1519341 | 230791 472 3420 7.2 | 67.316 % | ==============================================================================) restarts : 4 conflicts : 794 (232 /sec) decisions : 1072 (313 /sec) propagations : 4804558 (1404996 /sec) inspects : 29084202 (8505090 /sec) conflict literals : 5310 (32.05 % deleted) CPU time : 3.41962 s UNSATISFIABLE VERIFY_CNF 941 END : (4 seconds) [Thu Jun 1 16:00:27 2006] VERIFY_CNF 941 CPU : 3.75 = 0 + 0.01 + 3.71 + 0.03 # RESULT : makespan 941 UNSATISFIABLE # BOUND : makespan 942 973 MODIFY_CNF 957 BEGIN : [Thu Jun 1 16:00:27 2006] MODIFY_CNF 957 END : 29091879 bytes (0 seconds) [Thu Jun 1 16:00:27 2006] MODIFY_CNF 957 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 957 BEGIN : [Thu Jun 1 16:00:27 2006] CMD : minisat /work/tamura/csp2sat29658.cnf /work/tamura/csp2sat29658.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 537932 1570943 | 179310 0 0 NaNQ | 0.000 % | | 100 | 537932 1570943 | 197241 99 1195 12.1 | 65.337 % | | 250 | 537932 1570943 | 216965 248 2277 9.2 | 65.339 % | | 475 | 537932 1570943 | 238661 473 4281 9.1 | 65.339 % | | 813 | 536720 1567310 | 262527 787 7688 9.8 | 65.339 % | ==============================================================================) restarts : 5 conflicts : 982 (267 /sec) decisions : 1471 (399 /sec) propagations : 5635028 (1530161 /sec) inspects : 36666667 (9956631 /sec) conflict literals : 9464 (28.11 % deleted) CPU time : 3.68264 s SATISFIABLE VERIFY_CNF 957 END : (4 seconds) [Thu Jun 1 16:00:31 2006] VERIFY_CNF 957 CPU : 4.13999999999999 = 0.00999999999999091 + 0 + 4.01 + 0.12 # RESULT : makespan 957 SATISFIABLE SHOW_RESULT 957 BEGIN : [Thu Jun 1 16:00:31 2006] # ASSIGN : makespan 957 # ASSIGN : s_0_0 89 # ASSIGN : s_0_1 175 # ASSIGN : s_0_2 246 # ASSIGN : s_0_3 263 # ASSIGN : s_0_4 379 # ASSIGN : s_0_5 471 # ASSIGN : s_0_6 512 # ASSIGN : s_0_7 565 # ASSIGN : s_0_8 586 # ASSIGN : s_0_9 641 # ASSIGN : s_1_0 42 # ASSIGN : s_1_1 97 # ASSIGN : s_1_2 207 # ASSIGN : s_1_3 305 # ASSIGN : s_1_4 384 # ASSIGN : s_1_5 405 # ASSIGN : s_1_6 555 # ASSIGN : s_1_7 743 # ASSIGN : s_1_8 841 # ASSIGN : s_1_9 918 # ASSIGN : s_2_0 94 # ASSIGN : s_2_1 128 # ASSIGN : s_2_2 315 # ASSIGN : s_2_3 380 # ASSIGN : s_2_4 399 # ASSIGN : s_2_5 491 # ASSIGN : s_2_6 651 # ASSIGN : s_2_7 694 # ASSIGN : s_2_8 796 # ASSIGN : s_2_9 920 # ASSIGN : s_3_0 2 # ASSIGN : s_3_1 173 # ASSIGN : s_3_2 384 # ASSIGN : s_3_3 471 # ASSIGN : s_3_4 518 # ASSIGN : s_3_5 570 # ASSIGN : s_3_6 653 # ASSIGN : s_3_7 703 # ASSIGN : s_3_8 820 # ASSIGN : s_3_9 897 # ASSIGN : s_4_0 286 # ASSIGN : s_4_1 396 # ASSIGN : s_4_2 454 # ASSIGN : s_4_3 479 # ASSIGN : s_4_4 554 # ASSIGN : s_4_5 597 # ASSIGN : s_4_6 664 # ASSIGN : s_4_7 760 # ASSIGN : s_4_8 861 # ASSIGN : s_4_9 878 # ASSIGN : s_5_0 3 # ASSIGN : s_5_1 337 # ASSIGN : s_5_2 426 # ASSIGN : s_5_3 481 # ASSIGN : s_5_4 498 # ASSIGN : s_5_5 559 # ASSIGN : s_5_6 608 # ASSIGN : s_5_7 820 # ASSIGN : s_5_8 855 # ASSIGN : s_5_9 862 # ASSIGN : s_6_0 22 # ASSIGN : s_6_1 38 # ASSIGN : s_6_2 109 # ASSIGN : s_6_3 171 # ASSIGN : s_6_4 262 # ASSIGN : s_6_5 377 # ASSIGN : s_6_6 427 # ASSIGN : s_6_7 549 # ASSIGN : s_6_8 636 # ASSIGN : s_6_9 764 # ASSIGN : s_7_0 110 # ASSIGN : s_7_1 155 # ASSIGN : s_7_2 242 # ASSIGN : s_7_3 283 # ASSIGN : s_7_4 373 # ASSIGN : s_7_5 438 # ASSIGN : s_7_6 504 # ASSIGN : s_7_7 540 # ASSIGN : s_7_8 752 # ASSIGN : s_7_9 791 # ASSIGN : s_8_0 250 # ASSIGN : s_8_1 505 # ASSIGN : s_8_2 542 # ASSIGN : s_8_3 608 # ASSIGN : s_8_4 686 # ASSIGN : s_8_5 712 # ASSIGN : s_8_6 720 # ASSIGN : s_8_7 748 # ASSIGN : s_8_8 837 # ASSIGN : s_8_9 879 # ASSIGN : s_9_0 42 # ASSIGN : s_9_1 111 # ASSIGN : s_9_2 192 # ASSIGN : s_9_3 303 # ASSIGN : s_9_4 413 # ASSIGN : s_9_5 440 # ASSIGN : s_9_6 509 # ASSIGN : s_9_7 568 # ASSIGN : s_9_8 646 # ASSIGN : s_9_9 736 SHOW_RESULT 957 END : 957 (1 seconds) [Thu Jun 1 16:00:32 2006] SHOW_RESULT 957 CPU : 0.370000000000014 = 0.360000000000014 + 0.01 + 0 + 0 # BOUND : makespan 942 957 MODIFY_CNF 949 BEGIN : [Thu Jun 1 16:00:32 2006] MODIFY_CNF 949 END : 29091879 bytes (0 seconds) [Thu Jun 1 16:00:32 2006] MODIFY_CNF 949 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 949 BEGIN : [Thu Jun 1 16:00:32 2006] CMD : minisat /work/tamura/csp2sat29658.cnf /work/tamura/csp2sat29658.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 528431 1543252 | 176143 0 0 NaNQ | 0.000 % | | 101 | 528431 1543252 | 193757 99 871 8.8 | 66.008 % | | 255 | 528431 1543252 | 213133 253 2029 8.0 | 66.008 % | | 481 | 528431 1543252 | 234446 479 3986 8.3 | 66.008 % | ==============================================================================) restarts : 4 conflicts : 798 (238 /sec) decisions : 1246 (372 /sec) propagations : 4822452 (1438977 /sec) inspects : 31487062 (9395460 /sec) conflict literals : 6677 (28.48 % deleted) CPU time : 3.35131 s SATISFIABLE VERIFY_CNF 949 END : (3 seconds) [Thu Jun 1 16:00:35 2006] VERIFY_CNF 949 CPU : 3.72 = 0 + 0 + 3.69 + 0.03 # RESULT : makespan 949 SATISFIABLE SHOW_RESULT 949 BEGIN : [Thu Jun 1 16:00:35 2006] # ASSIGN : makespan 949 # ASSIGN : s_0_0 154 # ASSIGN : s_0_1 200 # ASSIGN : s_0_2 271 # ASSIGN : s_0_3 323 # ASSIGN : s_0_4 403 # ASSIGN : s_0_5 476 # ASSIGN : s_0_6 510 # ASSIGN : s_0_7 571 # ASSIGN : s_0_8 592 # ASSIGN : s_0_9 647 # ASSIGN : s_1_0 139 # ASSIGN : s_1_1 256 # ASSIGN : s_1_2 321 # ASSIGN : s_1_3 419 # ASSIGN : s_1_4 498 # ASSIGN : s_1_5 604 # ASSIGN : s_1_6 670 # ASSIGN : s_1_7 756 # ASSIGN : s_1_8 833 # ASSIGN : s_1_9 910 # ASSIGN : s_2_0 3 # ASSIGN : s_2_1 37 # ASSIGN : s_2_2 113 # ASSIGN : s_2_3 175 # ASSIGN : s_2_4 194 # ASSIGN : s_2_5 340 # ASSIGN : s_2_6 429 # ASSIGN : s_2_7 563 # ASSIGN : s_2_8 788 # ASSIGN : s_2_9 912 # ASSIGN : s_3_0 67 # ASSIGN : s_3_1 316 # ASSIGN : s_3_2 385 # ASSIGN : s_3_3 472 # ASSIGN : s_3_4 510 # ASSIGN : s_3_5 534 # ASSIGN : s_3_6 617 # ASSIGN : s_3_7 658 # ASSIGN : s_3_8 751 # ASSIGN : s_3_9 834 # ASSIGN : s_4_0 287 # ASSIGN : s_4_1 385 # ASSIGN : s_4_2 461 # ASSIGN : s_4_3 486 # ASSIGN : s_4_4 561 # ASSIGN : s_4_5 607 # ASSIGN : s_4_6 656 # ASSIGN : s_4_7 752 # ASSIGN : s_4_8 853 # ASSIGN : s_4_9 870 # ASSIGN : s_5_0 2 # ASSIGN : s_5_1 183 # ASSIGN : s_5_2 259 # ASSIGN : s_5_3 287 # ASSIGN : s_5_4 416 # ASSIGN : s_5_5 477 # ASSIGN : s_5_6 563 # ASSIGN : s_5_7 693 # ASSIGN : s_5_8 747 # ASSIGN : s_5_9 756 # ASSIGN : s_6_0 85 # ASSIGN : s_6_1 101 # ASSIGN : s_6_2 160 # ASSIGN : s_6_3 206 # ASSIGN : s_6_4 297 # ASSIGN : s_6_5 375 # ASSIGN : s_6_6 425 # ASSIGN : s_6_7 555 # ASSIGN : s_6_8 894 # ASSIGN : s_6_9 922 # ASSIGN : s_7_0 10 # ASSIGN : s_7_1 55 # ASSIGN : s_7_2 142 # ASSIGN : s_7_3 286 # ASSIGN : s_7_4 371 # ASSIGN : s_7_5 685 # ASSIGN : s_7_6 728 # ASSIGN : s_7_7 742 # ASSIGN : s_7_8 812 # ASSIGN : s_7_9 851 # ASSIGN : s_8_0 106 # ASSIGN : s_8_1 511 # ASSIGN : s_8_2 548 # ASSIGN : s_8_3 614 # ASSIGN : s_8_4 678 # ASSIGN : s_8_5 704 # ASSIGN : s_8_6 712 # ASSIGN : s_8_7 740 # ASSIGN : s_8_8 829 # ASSIGN : s_8_9 871 # ASSIGN : s_9_0 12 # ASSIGN : s_9_1 81 # ASSIGN : s_9_2 162 # ASSIGN : s_9_3 306 # ASSIGN : s_9_4 402 # ASSIGN : s_9_5 429 # ASSIGN : s_9_6 516 # ASSIGN : s_9_7 662 # ASSIGN : s_9_8 754 # ASSIGN : s_9_9 828 SHOW_RESULT 949 END : 949 (1 seconds) [Thu Jun 1 16:00:36 2006] SHOW_RESULT 949 CPU : 0.359999999999999 = 0.359999999999999 + 0 + 0 + 0 # BOUND : makespan 942 949 MODIFY_CNF 945 BEGIN : [Thu Jun 1 16:00:36 2006] MODIFY_CNF 945 END : 29091879 bytes (0 seconds) [Thu Jun 1 16:00:36 2006] MODIFY_CNF 945 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 945 BEGIN : [Thu Jun 1 16:00:36 2006] CMD : minisat /work/tamura/csp2sat29658.cnf /work/tamura/csp2sat29658.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 524756 1532631 | 174918 0 0 NaNQ | 0.000 % | | 100 | 524756 1532631 | 192409 98 742 7.6 | 66.334 % | | 250 | 524756 1532631 | 211650 248 1903 7.7 | 66.334 % | ==============================================================================) restarts : 3 conflicts : 300 (129 /sec) decisions : 535 (230 /sec) propagations : 1979936 (850622 /sec) inspects : 12758570 (5481347 /sec) conflict literals : 2388 (28.12 % deleted) CPU time : 2.32763 s SATISFIABLE VERIFY_CNF 945 END : (3 seconds) [Thu Jun 1 16:00:39 2006] VERIFY_CNF 945 CPU : 2.7 = 0 + 0.01 + 2.65 + 0.04 # RESULT : makespan 945 SATISFIABLE SHOW_RESULT 945 BEGIN : [Thu Jun 1 16:00:39 2006] # ASSIGN : makespan 945 # ASSIGN : s_0_0 143 # ASSIGN : s_0_1 164 # ASSIGN : s_0_2 235 # ASSIGN : s_0_3 321 # ASSIGN : s_0_4 442 # ASSIGN : s_0_5 472 # ASSIGN : s_0_6 506 # ASSIGN : s_0_7 567 # ASSIGN : s_0_8 588 # ASSIGN : s_0_9 643 # ASSIGN : s_1_0 44 # ASSIGN : s_1_1 99 # ASSIGN : s_1_2 153 # ASSIGN : s_1_3 251 # ASSIGN : s_1_4 364 # ASSIGN : s_1_5 376 # ASSIGN : s_1_6 666 # ASSIGN : s_1_7 752 # ASSIGN : s_1_8 829 # ASSIGN : s_1_9 906 # ASSIGN : s_2_0 1 # ASSIGN : s_2_1 35 # ASSIGN : s_2_2 121 # ASSIGN : s_2_3 183 # ASSIGN : s_2_4 202 # ASSIGN : s_2_5 437 # ASSIGN : s_2_6 516 # ASSIGN : s_2_7 559 # ASSIGN : s_2_8 784 # ASSIGN : s_2_9 908 # ASSIGN : s_3_0 56 # ASSIGN : s_3_1 184 # ASSIGN : s_3_2 381 # ASSIGN : s_3_3 468 # ASSIGN : s_3_4 506 # ASSIGN : s_3_5 530 # ASSIGN : s_3_6 613 # ASSIGN : s_3_7 654 # ASSIGN : s_3_8 747 # ASSIGN : s_3_9 830 # ASSIGN : s_4_0 283 # ASSIGN : s_4_1 393 # ASSIGN : s_4_2 459 # ASSIGN : s_4_3 484 # ASSIGN : s_4_4 560 # ASSIGN : s_4_5 603 # ASSIGN : s_4_6 652 # ASSIGN : s_4_7 748 # ASSIGN : s_4_8 849 # ASSIGN : s_4_9 866 # ASSIGN : s_5_0 0 # ASSIGN : s_5_1 299 # ASSIGN : s_5_2 375 # ASSIGN : s_5_3 403 # ASSIGN : s_5_4 413 # ASSIGN : s_5_5 475 # ASSIGN : s_5_6 559 # ASSIGN : s_5_7 689 # ASSIGN : s_5_8 743 # ASSIGN : s_5_9 752 # ASSIGN : s_6_0 114 # ASSIGN : s_6_1 130 # ASSIGN : s_6_2 193 # ASSIGN : s_6_3 239 # ASSIGN : s_6_4 330 # ASSIGN : s_6_5 373 # ASSIGN : s_6_6 423 # ASSIGN : s_6_7 551 # ASSIGN : s_6_8 890 # ASSIGN : s_6_9 918 # ASSIGN : s_7_0 11 # ASSIGN : s_7_1 106 # ASSIGN : s_7_2 253 # ASSIGN : s_7_3 294 # ASSIGN : s_7_4 369 # ASSIGN : s_7_5 681 # ASSIGN : s_7_6 724 # ASSIGN : s_7_7 738 # ASSIGN : s_7_8 808 # ASSIGN : s_7_9 847 # ASSIGN : s_8_0 474 # ASSIGN : s_8_1 507 # ASSIGN : s_8_2 544 # ASSIGN : s_8_3 610 # ASSIGN : s_8_4 674 # ASSIGN : s_8_5 700 # ASSIGN : s_8_6 708 # ASSIGN : s_8_7 736 # ASSIGN : s_8_8 825 # ASSIGN : s_8_9 867 # ASSIGN : s_9_0 39 # ASSIGN : s_9_1 108 # ASSIGN : s_9_2 189 # ASSIGN : s_9_3 314 # ASSIGN : s_9_4 410 # ASSIGN : s_9_5 437 # ASSIGN : s_9_6 613 # ASSIGN : s_9_7 658 # ASSIGN : s_9_8 750 # ASSIGN : s_9_9 824 SHOW_RESULT 945 END : 945 (0 seconds) [Thu Jun 1 16:00:39 2006] SHOW_RESULT 945 CPU : 0.359999999999999 = 0.359999999999999 + 0 + 0 + 0 # BOUND : makespan 942 945 MODIFY_CNF 943 BEGIN : [Thu Jun 1 16:00:39 2006] MODIFY_CNF 943 END : 29091879 bytes (0 seconds) [Thu Jun 1 16:00:39 2006] MODIFY_CNF 943 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 943 BEGIN : [Thu Jun 1 16:00:39 2006] CMD : minisat /work/tamura/csp2sat29658.cnf /work/tamura/csp2sat29658.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 522049 1524713 | 174016 0 0 NaNQ | 0.000 % | | 100 | 522049 1524713 | 191417 98 585 6.0 | 66.497 % | | 251 | 522049 1524713 | 210559 249 1688 6.8 | 66.497 % | | 476 | 519913 1518329 | 231615 453 2964 6.5 | 66.497 % | | 813 | 508039 1483292 | 254776 558 3844 6.9 | 67.719 % | ==============================================================================) restarts : 5 conflicts : 937 (251 /sec) decisions : 1242 (333 /sec) propagations : 5789455 (1553671 /sec) inspects : 35667841 (9571903 /sec) conflict literals : 6176 (34.36 % deleted) CPU time : 3.72631 s UNSATISFIABLE VERIFY_CNF 943 END : (4 seconds) [Thu Jun 1 16:00:43 2006] VERIFY_CNF 943 CPU : 4.07000000000001 = 0.0100000000000051 + 0.01 + 4.01 + 0.04 # RESULT : makespan 943 UNSATISFIABLE # BOUND : makespan 944 945 MODIFY_CNF 944 BEGIN : [Thu Jun 1 16:00:43 2006] MODIFY_CNF 944 END : 29091879 bytes (0 seconds) [Thu Jun 1 16:00:43 2006] MODIFY_CNF 944 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 944 BEGIN : [Thu Jun 1 16:00:43 2006] CMD : minisat /work/tamura/csp2sat29658.cnf /work/tamura/csp2sat29658.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 522979 1527402 | 174326 0 0 NaNQ | 0.000 % | | 100 | 522979 1527402 | 191758 98 596 6.1 | 66.416 % | | 251 | 522979 1527402 | 210934 249 1830 7.3 | 66.416 % | | 476 | 520840 1521009 | 232027 450 3406 7.6 | 66.658 % | | 816 | 510956 1491930 | 255230 634 4676 7.4 | 67.345 % | ==============================================================================) restarts : 5 conflicts : 1028 (264 /sec) decisions : 1452 (372 /sec) propagations : 6115558 (1567888 /sec) inspects : 37948131 (9729028 /sec) conflict literals : 7364 (33.56 % deleted) CPU time : 3.90051 s UNSATISFIABLE VERIFY_CNF 944 END : (4 seconds) [Thu Jun 1 16:00:47 2006] VERIFY_CNF 944 CPU : 4.3 = 0 + 0 + 4.18 + 0.12 # RESULT : makespan 944 UNSATISFIABLE # BOUND : makespan 945 945 MAIN END : (97 seconds) [Thu Jun 1 16:00:47 2006] MAIN CPU : 96.78 = 65.64 + 0.14 + 30.52 + 0.48