MAIN BEGIN : [Fri Jun 2 08:27:21 2006] READ BEGIN : csp/orb03.csp [Fri Jun 2 08:27:21 2006] READ END : csp/orb03.csp (1 seconds) [Fri Jun 2 08:27:22 2006] READ CPU : 1.4 = 1.4 + 0 + 0 + 0 # BOUND : makespan 648 1297 GENERATE_CNF 1297 BEGIN : [Fri Jun 2 08:27:22 2006] GENERATE_CNF 1297 END : 131551 variables 1371331 clauses 30913545 bytes (66 seconds) [Fri Jun 2 08:28:28 2006] GENERATE_CNF 1297 CPU : 66.34 = 66.24 + 0.1 + 0 + 0 MODIFY_CNF 972 BEGIN : [Fri Jun 2 08:28:28 2006] MODIFY_CNF 972 END : 30913551 bytes (0 seconds) [Fri Jun 2 08:28:28 2006] MODIFY_CNF 972 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 972 BEGIN : [Fri Jun 2 08:28:28 2006] CMD : minisat /work/tamura/csp2sat54032.cnf /work/tamura/csp2sat54032.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 601693 1759970 | 200564 0 0 NaNQ | 0.000 % | | 102 | 601693 1759970 | 220620 102 998 9.8 | 65.413 % | | 254 | 601693 1759970 | 242682 254 2231 8.8 | 65.413 % | | 479 | 601693 1759970 | 266950 479 4415 9.2 | 65.413 % | | 816 | 601693 1759970 | 293645 816 7801 9.6 | 65.413 % | | 1324 | 601693 1759970 | 323010 1324 13500 10.2 | 65.413 % | | 2085 | 601693 1759970 | 355311 2085 21089 10.1 | 65.413 % | | 3225 | 586308 1715027 | 390842 2176 20972 9.6 | 69.736 % | ==============================================================================) restarts : 8 conflicts : 3529 (338 /sec) decisions : 4915 (471 /sec) propagations : 22397868 (2145911 /sec) inspects : 149650124 (14337787 /sec) conflict literals : 33708 (34.27 % deleted) CPU time : 10.4375 s UNSATISFIABLE VERIFY_CNF 972 END : (11 seconds) [Fri Jun 2 08:28:39 2006] VERIFY_CNF 972 CPU : 10.77 = 0 + 0 + 10.75 + 0.02 # RESULT : makespan 972 UNSATISFIABLE # BOUND : makespan 973 1297 MODIFY_CNF 1135 BEGIN : [Fri Jun 2 08:28:39 2006] MODIFY_CNF 1135 END : 30913551 bytes (0 seconds) [Fri Jun 2 08:28:39 2006] MODIFY_CNF 1135 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1135 BEGIN : [Fri Jun 2 08:28:39 2006] CMD : minisat /work/tamura/csp2sat54032.cnf /work/tamura/csp2sat54032.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 766320 2237385 | 255440 0 0 NaNQ | 0.000 % | ==============================================================================) restarts : 1 conflicts : 13 (8 /sec) decisions : 170 (109 /sec) propagations : 176715 (113067 /sec) inspects : 1287126 (823539 /sec) conflict literals : 138 (4.17 % deleted) CPU time : 1.56292 s SATISFIABLE VERIFY_CNF 1135 END : (2 seconds) [Fri Jun 2 08:28:41 2006] VERIFY_CNF 1135 CPU : 2.05 = 0 + 0.01 + 2 + 0.04 # RESULT : makespan 1135 SATISFIABLE SHOW_RESULT 1135 BEGIN : [Fri Jun 2 08:28:41 2006] # ASSIGN : makespan 1135 # ASSIGN : s_0_0 16 # ASSIGN : s_0_1 125 # ASSIGN : s_0_2 194 # ASSIGN : s_0_3 219 # ASSIGN : s_0_4 224 # ASSIGN : s_0_5 376 # ASSIGN : s_0_6 391 # ASSIGN : s_0_7 525 # ASSIGN : s_0_8 536 # ASSIGN : s_0_9 553 # ASSIGN : s_1_0 139 # ASSIGN : s_1_1 264 # ASSIGN : s_1_2 312 # ASSIGN : s_1_3 399 # ASSIGN : s_1_4 437 # ASSIGN : s_1_5 455 # ASSIGN : s_1_6 479 # ASSIGN : s_1_7 543 # ASSIGN : s_1_8 635 # ASSIGN : s_1_9 736 # ASSIGN : s_2_0 127 # ASSIGN : s_2_1 196 # ASSIGN : s_2_2 259 # ASSIGN : s_2_3 352 # ASSIGN : s_2_4 444 # ASSIGN : s_2_5 469 # ASSIGN : s_2_6 541 # ASSIGN : s_2_7 592 # ASSIGN : s_2_8 673 # ASSIGN : s_2_9 731 # ASSIGN : s_3_0 7 # ASSIGN : s_3_1 37 # ASSIGN : s_3_2 112 # ASSIGN : s_3_3 142 # ASSIGN : s_3_4 230 # ASSIGN : s_3_5 274 # ASSIGN : s_3_6 366 # ASSIGN : s_3_7 420 # ASSIGN : s_3_8 746 # ASSIGN : s_3_9 981 # ASSIGN : s_4_0 72 # ASSIGN : s_4_1 150 # ASSIGN : s_4_2 279 # ASSIGN : s_4_3 353 # ASSIGN : s_4_4 379 # ASSIGN : s_4_5 649 # ASSIGN : s_4_6 682 # ASSIGN : s_4_7 774 # ASSIGN : s_4_8 888 # ASSIGN : s_4_9 1001 # ASSIGN : s_5_0 340 # ASSIGN : s_5_1 360 # ASSIGN : s_5_2 465 # ASSIGN : s_5_3 558 # ASSIGN : s_5_4 646 # ASSIGN : s_5_5 712 # ASSIGN : s_5_6 782 # ASSIGN : s_5_7 873 # ASSIGN : s_5_8 926 # ASSIGN : s_5_9 1039 # ASSIGN : s_6_0 486 # ASSIGN : s_6_1 507 # ASSIGN : s_6_2 705 # ASSIGN : s_6_3 727 # ASSIGN : s_6_4 783 # ASSIGN : s_6_5 817 # ASSIGN : s_6_6 857 # ASSIGN : s_6_7 910 # ASSIGN : s_6_8 1010 # ASSIGN : s_6_9 1072 # ASSIGN : s_7_0 5 # ASSIGN : s_7_1 43 # ASSIGN : s_7_2 106 # ASSIGN : s_7_3 233 # ASSIGN : s_7_4 274 # ASSIGN : s_7_5 291 # ASSIGN : s_7_6 577 # ASSIGN : s_7_7 618 # ASSIGN : s_7_8 956 # ASSIGN : s_7_9 972 # ASSIGN : s_8_0 527 # ASSIGN : s_8_1 600 # ASSIGN : s_8_2 668 # ASSIGN : s_8_3 757 # ASSIGN : s_8_4 781 # ASSIGN : s_8_5 880 # ASSIGN : s_8_6 972 # ASSIGN : s_8_7 979 # ASSIGN : s_8_8 1039 # ASSIGN : s_8_9 1058 # ASSIGN : s_9_0 404 # ASSIGN : s_9_1 456 # ASSIGN : s_9_2 476 # ASSIGN : s_9_3 546 # ASSIGN : s_9_4 644 # ASSIGN : s_9_5 667 # ASSIGN : s_9_6 736 # ASSIGN : s_9_7 817 # ASSIGN : s_9_8 1030 # ASSIGN : s_9_9 1054 SHOW_RESULT 1135 END : 1135 (1 seconds) [Fri Jun 2 08:28:42 2006] SHOW_RESULT 1135 CPU : 0.359999999999999 = 0.359999999999999 + 0 + 0 + 0 # BOUND : makespan 973 1135 MODIFY_CNF 1054 BEGIN : [Fri Jun 2 08:28:42 2006] MODIFY_CNF 1054 END : 30913551 bytes (0 seconds) [Fri Jun 2 08:28:42 2006] MODIFY_CNF 1054 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1054 BEGIN : [Fri Jun 2 08:28:42 2006] CMD : minisat /work/tamura/csp2sat54032.cnf /work/tamura/csp2sat54032.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 685239 2002323 | 228413 0 0 NaNQ | 0.000 % | | 100 | 685239 2002323 | 251254 100 1283 12.8 | 59.114 % | | 250 | 685239 2002323 | 276379 250 2783 11.1 | 59.114 % | | 475 | 685239 2002323 | 304017 475 6137 12.9 | 59.114 % | | 812 | 685239 2002323 | 334419 812 10531 13.0 | 59.114 % | | 1318 | 685239 2002323 | 367861 1318 17683 13.4 | 59.114 % | | 2079 | 685239 2002323 | 404647 2079 26209 12.6 | 59.114 % | | 3220 | 685239 2002323 | 445112 3220 40595 12.6 | 59.114 % | | 4928 | 685239 2002323 | 489623 4928 71907 14.6 | 59.114 % | ==============================================================================) restarts : 9 conflicts : 6294 (327 /sec) decisions : 9494 (494 /sec) propagations : 40958760 (2129496 /sec) inspects : 342532476 (17808682 /sec) conflict literals : 92084 (29.80 % deleted) CPU time : 19.234 s SATISFIABLE VERIFY_CNF 1054 END : (20 seconds) [Fri Jun 2 08:29:02 2006] VERIFY_CNF 1054 CPU : 19.8 = 0 + 0.01 + 19.66 + 0.13 # RESULT : makespan 1054 SATISFIABLE SHOW_RESULT 1054 BEGIN : [Fri Jun 2 08:29:02 2006] # ASSIGN : makespan 1054 # ASSIGN : s_0_0 438 # ASSIGN : s_0_1 534 # ASSIGN : s_0_2 603 # ASSIGN : s_0_3 697 # ASSIGN : s_0_4 702 # ASSIGN : s_0_5 757 # ASSIGN : s_0_6 856 # ASSIGN : s_0_7 944 # ASSIGN : s_0_8 955 # ASSIGN : s_0_9 972 # ASSIGN : s_1_0 106 # ASSIGN : s_1_1 122 # ASSIGN : s_1_2 170 # ASSIGN : s_1_3 237 # ASSIGN : s_1_4 275 # ASSIGN : s_1_5 322 # ASSIGN : s_1_6 354 # ASSIGN : s_1_7 416 # ASSIGN : s_1_8 567 # ASSIGN : s_1_9 663 # ASSIGN : s_2_0 103 # ASSIGN : s_2_1 210 # ASSIGN : s_2_2 273 # ASSIGN : s_2_3 366 # ASSIGN : s_2_4 483 # ASSIGN : s_2_5 508 # ASSIGN : s_2_6 603 # ASSIGN : s_2_7 658 # ASSIGN : s_2_8 744 # ASSIGN : s_2_9 802 # ASSIGN : s_3_0 3 # ASSIGN : s_3_1 33 # ASSIGN : s_3_2 68 # ASSIGN : s_3_3 95 # ASSIGN : s_3_4 186 # ASSIGN : s_3_5 230 # ASSIGN : s_3_6 329 # ASSIGN : s_3_7 367 # ASSIGN : s_3_8 470 # ASSIGN : s_3_9 586 # ASSIGN : s_4_0 69 # ASSIGN : s_4_1 190 # ASSIGN : s_4_2 293 # ASSIGN : s_4_3 368 # ASSIGN : s_4_4 412 # ASSIGN : s_4_5 489 # ASSIGN : s_4_6 580 # ASSIGN : s_4_7 703 # ASSIGN : s_4_8 862 # ASSIGN : s_4_9 906 # ASSIGN : s_5_0 374 # ASSIGN : s_5_1 394 # ASSIGN : s_5_2 451 # ASSIGN : s_5_3 532 # ASSIGN : s_5_4 628 # ASSIGN : s_5_5 694 # ASSIGN : s_5_6 772 # ASSIGN : s_5_7 863 # ASSIGN : s_5_8 900 # ASSIGN : s_5_9 958 # ASSIGN : s_6_0 12 # ASSIGN : s_6_1 319 # ASSIGN : s_6_2 542 # ASSIGN : s_6_3 564 # ASSIGN : s_6_4 620 # ASSIGN : s_6_5 654 # ASSIGN : s_6_6 739 # ASSIGN : s_6_7 817 # ASSIGN : s_6_8 948 # ASSIGN : s_6_9 977 # ASSIGN : s_7_0 342 # ASSIGN : s_7_1 530 # ASSIGN : s_7_2 593 # ASSIGN : s_7_3 629 # ASSIGN : s_7_4 655 # ASSIGN : s_7_5 672 # ASSIGN : s_7_6 792 # ASSIGN : s_7_7 807 # ASSIGN : s_7_8 905 # ASSIGN : s_7_9 972 # ASSIGN : s_8_0 117 # ASSIGN : s_8_1 273 # ASSIGN : s_8_2 394 # ASSIGN : s_8_3 641 # ASSIGN : s_8_4 665 # ASSIGN : s_8_5 764 # ASSIGN : s_8_6 899 # ASSIGN : s_8_7 921 # ASSIGN : s_8_8 1021 # ASSIGN : s_8_9 1040 # ASSIGN : s_9_0 16 # ASSIGN : s_9_1 83 # ASSIGN : s_9_2 107 # ASSIGN : s_9_3 177 # ASSIGN : s_9_4 308 # ASSIGN : s_9_5 331 # ASSIGN : s_9_6 346 # ASSIGN : s_9_7 427 # ASSIGN : s_9_8 498 # ASSIGN : s_9_9 522 SHOW_RESULT 1054 END : 1054 (0 seconds) [Fri Jun 2 08:29:02 2006] SHOW_RESULT 1054 CPU : 0.359999999999999 = 0.359999999999999 + 0 + 0 + 0 # BOUND : makespan 973 1054 MODIFY_CNF 1013 BEGIN : [Fri Jun 2 08:29:02 2006] MODIFY_CNF 1013 END : 30913551 bytes (0 seconds) [Fri Jun 2 08:29:02 2006] MODIFY_CNF 1013 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1013 BEGIN : [Fri Jun 2 08:29:02 2006] CMD : minisat /work/tamura/csp2sat54032.cnf /work/tamura/csp2sat54032.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 644198 1883341 | 214732 0 0 NaNQ | 0.000 % | | 100 | 644198 1883341 | 236205 100 1171 11.7 | 62.262 % | | 250 | 644198 1883341 | 259825 250 2802 11.2 | 62.262 % | | 477 | 644198 1883341 | 285808 477 4742 9.9 | 62.262 % | | 815 | 644198 1883341 | 314389 815 10834 13.3 | 62.262 % | | 1321 | 644198 1883341 | 345828 1321 16717 12.7 | 62.262 % | | 2080 | 644198 1883341 | 380410 2080 27135 13.0 | 62.262 % | | 3219 | 644198 1883341 | 418451 3219 41866 13.0 | 62.262 % | | 4927 | 644198 1883341 | 460297 4927 71657 14.5 | 62.262 % | | 7489 | 644198 1883341 | 506326 7489 113383 15.1 | 62.262 % | | 11334 | 644198 1883341 | 556959 11334 164579 14.5 | 62.262 % | ==============================================================================) restarts : 11 conflicts : 11791 (373 /sec) decisions : 16826 (533 /sec) propagations : 71121320 (2252676 /sec) inspects : 554689168 (17569063 /sec) conflict literals : 171369 (30.64 % deleted) CPU time : 31.5719 s SATISFIABLE VERIFY_CNF 1013 END : (32 seconds) [Fri Jun 2 08:29:34 2006] VERIFY_CNF 1013 CPU : 32.04 = 0.0100000000000051 + 0.00999999999999998 + 31.98 + 0.04 # RESULT : makespan 1013 SATISFIABLE SHOW_RESULT 1013 BEGIN : [Fri Jun 2 08:29:34 2006] # ASSIGN : makespan 1013 # ASSIGN : s_0_0 189 # ASSIGN : s_0_1 372 # ASSIGN : s_0_2 445 # ASSIGN : s_0_3 534 # ASSIGN : s_0_4 539 # ASSIGN : s_0_5 594 # ASSIGN : s_0_6 609 # ASSIGN : s_0_7 734 # ASSIGN : s_0_8 751 # ASSIGN : s_0_9 823 # ASSIGN : s_1_0 27 # ASSIGN : s_1_1 62 # ASSIGN : s_1_2 110 # ASSIGN : s_1_3 177 # ASSIGN : s_1_4 227 # ASSIGN : s_1_5 258 # ASSIGN : s_1_6 282 # ASSIGN : s_1_7 344 # ASSIGN : s_1_8 436 # ASSIGN : s_1_9 532 # ASSIGN : s_2_0 374 # ASSIGN : s_2_1 441 # ASSIGN : s_2_2 504 # ASSIGN : s_2_3 597 # ASSIGN : s_2_4 682 # ASSIGN : s_2_5 707 # ASSIGN : s_2_6 779 # ASSIGN : s_2_7 841 # ASSIGN : s_2_8 940 # ASSIGN : s_2_9 998 # ASSIGN : s_3_0 5 # ASSIGN : s_3_1 127 # ASSIGN : s_3_2 162 # ASSIGN : s_3_3 245 # ASSIGN : s_3_4 327 # ASSIGN : s_3_5 413 # ASSIGN : s_3_6 505 # ASSIGN : s_3_7 530 # ASSIGN : s_3_8 585 # ASSIGN : s_3_9 613 # ASSIGN : s_4_0 232 # ASSIGN : s_4_1 285 # ASSIGN : s_4_2 368 # ASSIGN : s_4_3 444 # ASSIGN : s_4_4 470 # ASSIGN : s_4_5 576 # ASSIGN : s_4_6 615 # ASSIGN : s_4_7 724 # ASSIGN : s_4_8 902 # ASSIGN : s_4_9 975 # ASSIGN : s_5_0 42 # ASSIGN : s_5_1 90 # ASSIGN : s_5_2 134 # ASSIGN : s_5_3 215 # ASSIGN : s_5_4 303 # ASSIGN : s_5_5 369 # ASSIGN : s_5_6 439 # ASSIGN : s_5_7 641 # ASSIGN : s_5_8 690 # ASSIGN : s_5_9 745 # ASSIGN : s_6_0 169 # ASSIGN : s_6_1 190 # ASSIGN : s_6_2 346 # ASSIGN : s_6_3 444 # ASSIGN : s_6_4 500 # ASSIGN : s_6_5 536 # ASSIGN : s_6_6 600 # ASSIGN : s_6_7 678 # ASSIGN : s_6_8 810 # ASSIGN : s_6_9 839 # ASSIGN : s_7_0 3 # ASSIGN : s_7_1 35 # ASSIGN : s_7_2 98 # ASSIGN : s_7_3 134 # ASSIGN : s_7_4 160 # ASSIGN : s_7_5 259 # ASSIGN : s_7_6 398 # ASSIGN : s_7_7 477 # ASSIGN : s_7_8 625 # ASSIGN : s_7_9 697 # ASSIGN : s_8_0 371 # ASSIGN : s_8_1 547 # ASSIGN : s_8_2 593 # ASSIGN : s_8_3 707 # ASSIGN : s_8_4 731 # ASSIGN : s_8_5 830 # ASSIGN : s_8_6 922 # ASSIGN : s_8_7 929 # ASSIGN : s_8_8 980 # ASSIGN : s_8_9 999 # ASSIGN : s_9_0 38 # ASSIGN : s_9_1 283 # ASSIGN : s_9_2 371 # ASSIGN : s_9_3 441 # ASSIGN : s_9_4 556 # ASSIGN : s_9_5 579 # ASSIGN : s_9_6 653 # ASSIGN : s_9_7 768 # ASSIGN : s_9_8 905 # ASSIGN : s_9_9 932 SHOW_RESULT 1013 END : 1013 (0 seconds) [Fri Jun 2 08:29:34 2006] SHOW_RESULT 1013 CPU : 0.349999999999994 = 0.349999999999994 + 0 + 0 + 0 # BOUND : makespan 973 1013 MODIFY_CNF 993 BEGIN : [Fri Jun 2 08:29:34 2006] MODIFY_CNF 993 END : 30913551 bytes (0 seconds) [Fri Jun 2 08:29:34 2006] MODIFY_CNF 993 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 993 BEGIN : [Fri Jun 2 08:29:34 2006] CMD : minisat /work/tamura/csp2sat54032.cnf /work/tamura/csp2sat54032.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 623384 1822920 | 207794 0 0 NaNQ | 0.000 % | | 101 | 623384 1822920 | 228573 101 1203 11.9 | 63.799 % | | 251 | 623384 1822920 | 251430 251 2369 9.4 | 63.799 % | | 476 | 623384 1822920 | 276573 476 4357 9.2 | 63.799 % | | 813 | 623384 1822920 | 304231 813 7678 9.4 | 63.799 % | | 1320 | 623384 1822920 | 334654 1320 12631 9.6 | 63.799 % | | 2081 | 623384 1822920 | 368119 2081 21470 10.3 | 63.799 % | | 3220 | 623384 1822920 | 404931 3220 36365 11.3 | 63.799 % | | 4928 | 623384 1822920 | 445424 4928 56117 11.4 | 63.799 % | | 7490 | 622776 1821098 | 489967 7317 88049 12.0 | 63.800 % | ==============================================================================) restarts : 10 conflicts : 10954 (375 /sec) decisions : 15130 (518 /sec) propagations : 67488291 (2310176 /sec) inspects : 493236656 (16883871 /sec) conflict literals : 132169 (34.68 % deleted) CPU time : 29.2135 s UNSATISFIABLE VERIFY_CNF 993 END : (30 seconds) [Fri Jun 2 08:30:04 2006] VERIFY_CNF 993 CPU : 29.61 = 0 + 0 + 29.57 + 0.04 # RESULT : makespan 993 UNSATISFIABLE # BOUND : makespan 994 1013 MODIFY_CNF 1003 BEGIN : [Fri Jun 2 08:30:04 2006] MODIFY_CNF 1003 END : 30913551 bytes (0 seconds) [Fri Jun 2 08:30:04 2006] MODIFY_CNF 1003 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1003 BEGIN : [Fri Jun 2 08:30:04 2006] CMD : minisat /work/tamura/csp2sat54032.cnf /work/tamura/csp2sat54032.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 634188 1854321 | 211396 0 0 NaNQ | 0.000 % | | 100 | 634188 1854321 | 232535 100 1348 13.5 | 63.030 % | | 250 | 634188 1854321 | 255789 250 2721 10.9 | 63.030 % | | 476 | 634188 1854321 | 281368 476 4948 10.4 | 63.030 % | | 813 | 634188 1854321 | 309504 813 9088 11.2 | 63.030 % | | 1319 | 634188 1854321 | 340455 1319 15375 11.7 | 63.030 % | | 2078 | 634188 1854321 | 374500 2078 23362 11.2 | 63.030 % | | 3217 | 634188 1854321 | 411951 3217 35017 10.9 | 63.030 % | | 4925 | 634188 1854321 | 453146 4925 56565 11.5 | 63.030 % | | 7487 | 634188 1854321 | 498460 7487 94251 12.6 | 63.030 % | | 11332 | 634188 1854321 | 548306 11332 146856 13.0 | 63.030 % | | 17098 | 599773 1753767 | 603137 11128 141715 12.7 | 65.082 % | ==============================================================================) restarts : 12 conflicts : 18673 (368 /sec) decisions : 25301 (499 /sec) propagations : 117538345 (2319092 /sec) inspects : 882222463 (17406701 /sec) conflict literals : 252961 (35.51 % deleted) CPU time : 50.6829 s UNSATISFIABLE VERIFY_CNF 1003 END : (51 seconds) [Fri Jun 2 08:30:55 2006] VERIFY_CNF 1003 CPU : 51.08 = 0 + 0.01 + 51.03 + 0.04 # RESULT : makespan 1003 UNSATISFIABLE # BOUND : makespan 1004 1013 MODIFY_CNF 1008 BEGIN : [Fri Jun 2 08:30:55 2006] MODIFY_CNF 1008 END : 30913551 bytes (0 seconds) [Fri Jun 2 08:30:55 2006] MODIFY_CNF 1008 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1008 BEGIN : [Fri Jun 2 08:30:55 2006] CMD : minisat /work/tamura/csp2sat54032.cnf /work/tamura/csp2sat54032.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 639193 1868831 | 213064 0 0 NaNQ | 0.000 % | | 101 | 639193 1868831 | 234370 101 1448 14.3 | 62.646 % | | 251 | 639193 1868831 | 257807 251 2783 11.1 | 62.646 % | | 476 | 639193 1868831 | 283588 476 4656 9.8 | 62.646 % | | 813 | 639193 1868831 | 311947 813 10689 13.1 | 62.646 % | | 1319 | 639193 1868831 | 343141 1319 15712 11.9 | 62.646 % | | 2079 | 639193 1868831 | 377455 2079 25127 12.1 | 62.646 % | | 3218 | 639193 1868831 | 415201 3218 38378 11.9 | 62.646 % | ==============================================================================) restarts : 8 conflicts : 4020 (339 /sec) decisions : 5831 (491 /sec) propagations : 25338797 (2135571 /sec) inspects : 191634747 (16151110 /sec) conflict literals : 50495 (28.49 % deleted) CPU time : 11.8651 s SATISFIABLE VERIFY_CNF 1008 END : (13 seconds) [Fri Jun 2 08:31:08 2006] VERIFY_CNF 1008 CPU : 12.34 = 0.00999999999999091 + 0.01 + 12.28 + 0.04 # RESULT : makespan 1008 SATISFIABLE SHOW_RESULT 1008 BEGIN : [Fri Jun 2 08:31:08 2006] # ASSIGN : makespan 1008 # ASSIGN : s_0_0 271 # ASSIGN : s_0_1 367 # ASSIGN : s_0_2 440 # ASSIGN : s_0_3 532 # ASSIGN : s_0_4 537 # ASSIGN : s_0_5 595 # ASSIGN : s_0_6 686 # ASSIGN : s_0_7 806 # ASSIGN : s_0_8 817 # ASSIGN : s_0_9 842 # ASSIGN : s_1_0 24 # ASSIGN : s_1_1 52 # ASSIGN : s_1_2 107 # ASSIGN : s_1_3 174 # ASSIGN : s_1_4 215 # ASSIGN : s_1_5 238 # ASSIGN : s_1_6 262 # ASSIGN : s_1_7 324 # ASSIGN : s_1_8 416 # ASSIGN : s_1_9 512 # ASSIGN : s_2_0 369 # ASSIGN : s_2_1 436 # ASSIGN : s_2_2 499 # ASSIGN : s_2_3 592 # ASSIGN : s_2_4 677 # ASSIGN : s_2_5 702 # ASSIGN : s_2_6 774 # ASSIGN : s_2_7 836 # ASSIGN : s_2_8 935 # ASSIGN : s_2_9 993 # ASSIGN : s_3_0 2 # ASSIGN : s_3_1 100 # ASSIGN : s_3_2 161 # ASSIGN : s_3_3 233 # ASSIGN : s_3_4 370 # ASSIGN : s_3_5 422 # ASSIGN : s_3_6 521 # ASSIGN : s_3_7 546 # ASSIGN : s_3_8 691 # ASSIGN : s_3_9 740 # ASSIGN : s_4_0 135 # ASSIGN : s_4_1 188 # ASSIGN : s_4_2 337 # ASSIGN : s_4_3 414 # ASSIGN : s_4_4 465 # ASSIGN : s_4_5 571 # ASSIGN : s_4_6 610 # ASSIGN : s_4_7 743 # ASSIGN : s_4_8 897 # ASSIGN : s_4_9 970 # ASSIGN : s_5_0 32 # ASSIGN : s_5_1 87 # ASSIGN : s_5_2 131 # ASSIGN : s_5_3 212 # ASSIGN : s_5_4 303 # ASSIGN : s_5_5 370 # ASSIGN : s_5_6 440 # ASSIGN : s_5_7 551 # ASSIGN : s_5_8 593 # ASSIGN : s_5_9 710 # ASSIGN : s_6_0 189 # ASSIGN : s_6_1 210 # ASSIGN : s_6_2 315 # ASSIGN : s_6_3 370 # ASSIGN : s_6_4 440 # ASSIGN : s_6_5 474 # ASSIGN : s_6_6 514 # ASSIGN : s_6_7 645 # ASSIGN : s_6_8 805 # ASSIGN : s_6_9 834 # ASSIGN : s_7_0 0 # ASSIGN : s_7_1 32 # ASSIGN : s_7_2 95 # ASSIGN : s_7_3 131 # ASSIGN : s_7_4 157 # ASSIGN : s_7_5 239 # ASSIGN : s_7_6 407 # ASSIGN : s_7_7 457 # ASSIGN : s_7_8 588 # ASSIGN : s_7_9 604 # ASSIGN : s_8_0 426 # ASSIGN : s_8_1 542 # ASSIGN : s_8_2 588 # ASSIGN : s_8_3 702 # ASSIGN : s_8_4 726 # ASSIGN : s_8_5 825 # ASSIGN : s_8_6 917 # ASSIGN : s_8_7 924 # ASSIGN : s_8_8 975 # ASSIGN : s_8_9 994 # ASSIGN : s_9_0 35 # ASSIGN : s_9_1 190 # ASSIGN : s_9_2 300 # ASSIGN : s_9_3 410 # ASSIGN : s_9_4 508 # ASSIGN : s_9_5 531 # ASSIGN : s_9_6 567 # ASSIGN : s_9_7 648 # ASSIGN : s_9_8 719 # ASSIGN : s_9_9 927 SHOW_RESULT 1008 END : 1008 (0 seconds) [Fri Jun 2 08:31:08 2006] SHOW_RESULT 1008 CPU : 0.350000000000009 = 0.350000000000009 + 0 + 0 + 0 # BOUND : makespan 1004 1008 MODIFY_CNF 1006 BEGIN : [Fri Jun 2 08:31:08 2006] MODIFY_CNF 1006 END : 30913551 bytes (0 seconds) [Fri Jun 2 08:31:08 2006] MODIFY_CNF 1006 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1006 BEGIN : [Fri Jun 2 08:31:08 2006] CMD : minisat /work/tamura/csp2sat54032.cnf /work/tamura/csp2sat54032.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 637191 1863027 | 212397 0 0 NaNQ | 0.000 % | | 100 | 637191 1863027 | 233636 100 1228 12.3 | 62.799 % | | 251 | 637191 1863027 | 257000 251 3029 12.1 | 62.799 % | | 477 | 637191 1863027 | 282700 477 4768 10.0 | 62.799 % | | 814 | 637191 1863027 | 310970 814 8273 10.2 | 62.799 % | | 1320 | 637191 1863027 | 342067 1320 16643 12.6 | 62.799 % | | 2080 | 637191 1863027 | 376274 2080 24334 11.7 | 62.799 % | | 3220 | 637191 1863027 | 413901 3220 38571 12.0 | 62.799 % | | 4928 | 637191 1863027 | 455291 4928 59491 12.1 | 62.799 % | | 7490 | 637191 1863027 | 500821 7490 93167 12.4 | 62.799 % | | 11334 | 637191 1863027 | 550903 11334 147810 13.0 | 62.799 % | ==============================================================================) restarts : 11 conflicts : 12491 (373 /sec) decisions : 17080 (511 /sec) propagations : 77275558 (2309715 /sec) inspects : 591349994 (17675057 /sec) conflict literals : 163707 (32.16 % deleted) CPU time : 33.4568 s SATISFIABLE VERIFY_CNF 1006 END : (34 seconds) [Fri Jun 2 08:31:42 2006] VERIFY_CNF 1006 CPU : 33.92 = 0.00999999999999091 + 0.00999999999999998 + 33.86 + 0.04 # RESULT : makespan 1006 SATISFIABLE SHOW_RESULT 1006 BEGIN : [Fri Jun 2 08:31:42 2006] # ASSIGN : makespan 1006 # ASSIGN : s_0_0 185 # ASSIGN : s_0_1 365 # ASSIGN : s_0_2 438 # ASSIGN : s_0_3 530 # ASSIGN : s_0_4 535 # ASSIGN : s_0_5 593 # ASSIGN : s_0_6 684 # ASSIGN : s_0_7 788 # ASSIGN : s_0_8 799 # ASSIGN : s_0_9 816 # ASSIGN : s_1_0 25 # ASSIGN : s_1_1 54 # ASSIGN : s_1_2 108 # ASSIGN : s_1_3 175 # ASSIGN : s_1_4 223 # ASSIGN : s_1_5 241 # ASSIGN : s_1_6 265 # ASSIGN : s_1_7 327 # ASSIGN : s_1_8 419 # ASSIGN : s_1_9 515 # ASSIGN : s_2_0 367 # ASSIGN : s_2_1 434 # ASSIGN : s_2_2 497 # ASSIGN : s_2_3 590 # ASSIGN : s_2_4 675 # ASSIGN : s_2_5 700 # ASSIGN : s_2_6 772 # ASSIGN : s_2_7 834 # ASSIGN : s_2_8 933 # ASSIGN : s_2_9 991 # ASSIGN : s_3_0 3 # ASSIGN : s_3_1 123 # ASSIGN : s_3_2 158 # ASSIGN : s_3_3 241 # ASSIGN : s_3_4 323 # ASSIGN : s_3_5 401 # ASSIGN : s_3_6 493 # ASSIGN : s_3_7 529 # ASSIGN : s_3_8 623 # ASSIGN : s_3_9 651 # ASSIGN : s_4_0 228 # ASSIGN : s_4_1 281 # ASSIGN : s_4_2 364 # ASSIGN : s_4_3 437 # ASSIGN : s_4_4 463 # ASSIGN : s_4_5 569 # ASSIGN : s_4_6 608 # ASSIGN : s_4_7 717 # ASSIGN : s_4_8 832 # ASSIGN : s_4_9 968 # ASSIGN : s_5_0 34 # ASSIGN : s_5_1 88 # ASSIGN : s_5_2 132 # ASSIGN : s_5_3 213 # ASSIGN : s_5_4 301 # ASSIGN : s_5_5 368 # ASSIGN : s_5_6 438 # ASSIGN : s_5_7 559 # ASSIGN : s_5_8 596 # ASSIGN : s_5_9 692 # ASSIGN : s_6_0 102 # ASSIGN : s_6_1 188 # ASSIGN : s_6_2 342 # ASSIGN : s_6_3 368 # ASSIGN : s_6_4 484 # ASSIGN : s_6_5 518 # ASSIGN : s_6_6 558 # ASSIGN : s_6_7 671 # ASSIGN : s_6_8 841 # ASSIGN : s_6_9 870 # ASSIGN : s_7_0 1 # ASSIGN : s_7_1 33 # ASSIGN : s_7_2 96 # ASSIGN : s_7_3 132 # ASSIGN : s_7_4 158 # ASSIGN : s_7_5 242 # ASSIGN : s_7_6 386 # ASSIGN : s_7_7 460 # ASSIGN : s_7_8 543 # ASSIGN : s_7_9 602 # ASSIGN : s_8_0 424 # ASSIGN : s_8_1 540 # ASSIGN : s_8_2 586 # ASSIGN : s_8_3 700 # ASSIGN : s_8_4 724 # ASSIGN : s_8_5 823 # ASSIGN : s_8_6 915 # ASSIGN : s_8_7 922 # ASSIGN : s_8_8 973 # ASSIGN : s_8_9 992 # ASSIGN : s_9_0 36 # ASSIGN : s_9_1 281 # ASSIGN : s_9_2 367 # ASSIGN : s_9_3 437 # ASSIGN : s_9_4 555 # ASSIGN : s_9_5 578 # ASSIGN : s_9_6 611 # ASSIGN : s_9_7 728 # ASSIGN : s_9_8 898 # ASSIGN : s_9_9 925 SHOW_RESULT 1006 END : 1006 (1 seconds) [Fri Jun 2 08:31:43 2006] SHOW_RESULT 1006 CPU : 0.350000000000009 = 0.350000000000009 + 0 + 0 + 0 # BOUND : makespan 1004 1006 MODIFY_CNF 1005 BEGIN : [Fri Jun 2 08:31:43 2006] MODIFY_CNF 1005 END : 30913551 bytes (0 seconds) [Fri Jun 2 08:31:43 2006] MODIFY_CNF 1005 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1005 BEGIN : [Fri Jun 2 08:31:43 2006] CMD : minisat /work/tamura/csp2sat54032.cnf /work/tamura/csp2sat54032.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 636190 1860125 | 212063 0 0 NaNQ | 0.000 % | | 100 | 636190 1860125 | 233269 100 1391 13.9 | 62.876 % | | 251 | 636190 1860125 | 256596 251 3899 15.5 | 62.876 % | | 476 | 636190 1860125 | 282255 476 6245 13.1 | 62.876 % | | 813 | 636190 1860125 | 310481 813 9850 12.1 | 62.876 % | | 1319 | 636190 1860125 | 341529 1319 16126 12.2 | 62.876 % | | 2079 | 636190 1860125 | 375682 2079 24427 11.7 | 62.876 % | | 3218 | 636190 1860125 | 413250 3218 38706 12.0 | 62.876 % | | 4927 | 636190 1860125 | 454575 4927 59361 12.0 | 62.876 % | | 7489 | 629593 1840929 | 500033 6518 77953 12.0 | 63.329 % | | 11333 | 629593 1840929 | 550036 10362 135267 13.1 | 63.329 % | ==============================================================================) restarts : 11 conflicts : 14987 (371 /sec) decisions : 20739 (514 /sec) propagations : 92724530 (2297196 /sec) inspects : 698849503 (17313591 /sec) conflict literals : 198971 (34.29 % deleted) CPU time : 40.3642 s SATISFIABLE VERIFY_CNF 1005 END : (41 seconds) [Fri Jun 2 08:32:24 2006] VERIFY_CNF 1005 CPU : 40.82 = 0.00999999999999091 + 0.01 + 40.76 + 0.04 # RESULT : makespan 1005 SATISFIABLE SHOW_RESULT 1005 BEGIN : [Fri Jun 2 08:32:24 2006] # ASSIGN : makespan 1005 # ASSIGN : s_0_0 184 # ASSIGN : s_0_1 364 # ASSIGN : s_0_2 437 # ASSIGN : s_0_3 529 # ASSIGN : s_0_4 534 # ASSIGN : s_0_5 592 # ASSIGN : s_0_6 683 # ASSIGN : s_0_7 803 # ASSIGN : s_0_8 814 # ASSIGN : s_0_9 839 # ASSIGN : s_1_0 24 # ASSIGN : s_1_1 59 # ASSIGN : s_1_2 107 # ASSIGN : s_1_3 174 # ASSIGN : s_1_4 222 # ASSIGN : s_1_5 256 # ASSIGN : s_1_6 280 # ASSIGN : s_1_7 342 # ASSIGN : s_1_8 434 # ASSIGN : s_1_9 530 # ASSIGN : s_2_0 366 # ASSIGN : s_2_1 433 # ASSIGN : s_2_2 496 # ASSIGN : s_2_3 589 # ASSIGN : s_2_4 674 # ASSIGN : s_2_5 699 # ASSIGN : s_2_6 771 # ASSIGN : s_2_7 833 # ASSIGN : s_2_8 932 # ASSIGN : s_2_9 990 # ASSIGN : s_3_0 2 # ASSIGN : s_3_1 122 # ASSIGN : s_3_2 157 # ASSIGN : s_3_3 240 # ASSIGN : s_3_4 322 # ASSIGN : s_3_5 368 # ASSIGN : s_3_6 503 # ASSIGN : s_3_7 528 # ASSIGN : s_3_8 638 # ASSIGN : s_3_9 666 # ASSIGN : s_4_0 227 # ASSIGN : s_4_1 280 # ASSIGN : s_4_2 363 # ASSIGN : s_4_3 436 # ASSIGN : s_4_4 462 # ASSIGN : s_4_5 568 # ASSIGN : s_4_6 607 # ASSIGN : s_4_7 716 # ASSIGN : s_4_8 831 # ASSIGN : s_4_9 967 # ASSIGN : s_5_0 39 # ASSIGN : s_5_1 87 # ASSIGN : s_5_2 131 # ASSIGN : s_5_3 212 # ASSIGN : s_5_4 300 # ASSIGN : s_5_5 367 # ASSIGN : s_5_6 437 # ASSIGN : s_5_7 574 # ASSIGN : s_5_8 611 # ASSIGN : s_5_9 707 # ASSIGN : s_6_0 186 # ASSIGN : s_6_1 207 # ASSIGN : s_6_2 341 # ASSIGN : s_6_3 438 # ASSIGN : s_6_4 494 # ASSIGN : s_6_5 528 # ASSIGN : s_6_6 573 # ASSIGN : s_6_7 670 # ASSIGN : s_6_8 840 # ASSIGN : s_6_9 869 # ASSIGN : s_7_0 0 # ASSIGN : s_7_1 32 # ASSIGN : s_7_2 95 # ASSIGN : s_7_3 131 # ASSIGN : s_7_4 157 # ASSIGN : s_7_5 257 # ASSIGN : s_7_6 460 # ASSIGN : s_7_7 475 # ASSIGN : s_7_8 558 # ASSIGN : s_7_9 601 # ASSIGN : s_8_0 365 # ASSIGN : s_8_1 539 # ASSIGN : s_8_2 585 # ASSIGN : s_8_3 699 # ASSIGN : s_8_4 723 # ASSIGN : s_8_5 822 # ASSIGN : s_8_6 914 # ASSIGN : s_8_7 921 # ASSIGN : s_8_8 972 # ASSIGN : s_8_9 991 # ASSIGN : s_9_0 35 # ASSIGN : s_9_1 187 # ASSIGN : s_9_2 366 # ASSIGN : s_9_3 436 # ASSIGN : s_9_4 554 # ASSIGN : s_9_5 577 # ASSIGN : s_9_6 626 # ASSIGN : s_9_7 743 # ASSIGN : s_9_8 815 # ASSIGN : s_9_9 924 SHOW_RESULT 1005 END : 1005 (0 seconds) [Fri Jun 2 08:32:24 2006] SHOW_RESULT 1005 CPU : 0.350000000000009 = 0.350000000000009 + 0 + 0 + 0 # BOUND : makespan 1004 1005 MODIFY_CNF 1004 BEGIN : [Fri Jun 2 08:32:24 2006] MODIFY_CNF 1004 END : 30913551 bytes (0 seconds) [Fri Jun 2 08:32:24 2006] MODIFY_CNF 1004 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1004 BEGIN : [Fri Jun 2 08:32:24 2006] CMD : minisat /work/tamura/csp2sat54032.cnf /work/tamura/csp2sat54032.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 635189 1857223 | 211729 0 0 NaNQ | 0.000 % | | 100 | 635189 1857223 | 232901 100 1299 13.0 | 62.953 % | | 251 | 635189 1857223 | 256192 251 2497 9.9 | 62.953 % | | 476 | 635189 1857223 | 281811 476 4728 9.9 | 62.953 % | | 813 | 635189 1857223 | 309992 813 8637 10.6 | 62.953 % | | 1319 | 635189 1857223 | 340991 1319 14235 10.8 | 62.953 % | | 2079 | 635189 1857223 | 375090 2079 24127 11.6 | 62.953 % | | 3218 | 635189 1857223 | 412599 3218 38446 11.9 | 62.953 % | | 4926 | 635189 1857223 | 453859 4926 57418 11.7 | 62.953 % | | 7488 | 635189 1857223 | 499245 7488 92188 12.3 | 62.953 % | | 11332 | 635189 1857223 | 549170 11332 161820 14.3 | 62.953 % | | 17099 | 617750 1806365 | 604087 14533 210832 14.5 | 64.065 % | ==============================================================================) restarts : 12 conflicts : 19730 (374 /sec) decisions : 27212 (515 /sec) propagations : 120894964 (2288962 /sec) inspects : 924068155 (17495825 /sec) conflict literals : 282155 (35.87 % deleted) CPU time : 52.8165 s UNSATISFIABLE VERIFY_CNF 1004 END : (53 seconds) [Fri Jun 2 08:33:17 2006] VERIFY_CNF 1004 CPU : 53.21 = 0.00999999999999091 + 0.01 + 53.15 + 0.04 # RESULT : makespan 1004 UNSATISFIABLE # BOUND : makespan 1005 1005 MAIN END : (356 seconds) [Fri Jun 2 08:33:17 2006] MAIN CPU : 355.51 = 69.82 + 0.18 + 285.04 + 0.47