MAIN BEGIN : [Thu Jun 1 15:42:31 2006] READ BEGIN : csp/la12.csp [Thu Jun 1 15:42:31 2006] READ END : csp/la12.csp (2 seconds) [Thu Jun 1 15:42:33 2006] READ CPU : 2.62 = 2.62 + 0 + 0 + 0 # BOUND : makespan 1039 1286 GENERATE_CNF 1286 BEGIN : [Thu Jun 1 15:42:33 2006] GENERATE_CNF 1286 END : 131049 variables 2592789 clauses 59326466 bytes (129 seconds) [Thu Jun 1 15:44:42 2006] GENERATE_CNF 1286 CPU : 128.16 = 127.99 + 0.17 + 0 + 0 MODIFY_CNF 1162 BEGIN : [Thu Jun 1 15:44:42 2006] MODIFY_CNF 1162 END : 59326472 bytes (0 seconds) [Thu Jun 1 15:44:42 2006] MODIFY_CNF 1162 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1162 BEGIN : [Thu Jun 1 15:44:42 2006] CMD : minisat /work/tamura/csp2sat98308.cnf /work/tamura/csp2sat98308.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 2024360 5978623 | 674786 0 0 NaNQ | 0.000 % | ==============================================================================) restarts : 1 conflicts : 12 (5 /sec) decisions : 313 (126 /sec) propagations : 148164 (59638 /sec) inspects : 1928935 (776423 /sec) conflict literals : 131 (2.96 % deleted) CPU time : 2.48439 s SATISFIABLE VERIFY_CNF 1162 END : (3 seconds) [Thu Jun 1 15:44:45 2006] VERIFY_CNF 1162 CPU : 3.59000000000002 = 0.0100000000000193 + 0.01 + 3.52 + 0.05 # RESULT : makespan 1162 SATISFIABLE SHOW_RESULT 1162 BEGIN : [Thu Jun 1 15:44:45 2006] # ASSIGN : makespan 1162 # ASSIGN : s_0_0 95 # ASSIGN : s_0_1 122 # ASSIGN : s_0_2 204 # ASSIGN : s_0_3 639 # ASSIGN : s_0_4 827 # ASSIGN : s_1_0 0 # ASSIGN : s_1_1 288 # ASSIGN : s_1_2 406 # ASSIGN : s_1_3 497 # ASSIGN : s_1_4 543 # ASSIGN : s_2_0 329 # ASSIGN : s_2_1 773 # ASSIGN : s_2_2 837 # ASSIGN : s_2_3 890 # ASSIGN : s_2_4 974 # ASSIGN : s_3_0 179 # ASSIGN : s_3_1 241 # ASSIGN : s_3_2 345 # ASSIGN : s_3_3 1034 # ASSIGN : s_3_4 1108 # ASSIGN : s_4_0 50 # ASSIGN : s_4_1 118 # ASSIGN : s_4_2 206 # ASSIGN : s_4_3 236 # ASSIGN : s_4_4 382 # ASSIGN : s_5_0 6 # ASSIGN : s_5_1 117 # ASSIGN : s_5_2 306 # ASSIGN : s_5_3 317 # ASSIGN : s_5_4 439 # ASSIGN : s_6_0 301 # ASSIGN : s_6_1 396 # ASSIGN : s_6_2 487 # ASSIGN : s_6_3 520 # ASSIGN : s_6_4 564 # ASSIGN : s_7_0 298 # ASSIGN : s_7_1 540 # ASSIGN : s_7_2 584 # ASSIGN : s_7_3 639 # ASSIGN : s_7_4 692 # ASSIGN : s_8_0 33 # ASSIGN : s_8_1 266 # ASSIGN : s_8_2 367 # ASSIGN : s_8_3 564 # ASSIGN : s_8_4 1013 # ASSIGN : s_9_0 40 # ASSIGN : s_9_1 620 # ASSIGN : s_9_2 921 # ASSIGN : s_9_3 928 # ASSIGN : s_9_4 1073 # ASSIGN : s_10_0 59 # ASSIGN : s_10_1 330 # ASSIGN : s_10_2 396 # ASSIGN : s_10_3 660 # ASSIGN : s_10_4 1156 # ASSIGN : s_11_0 574 # ASSIGN : s_11_1 616 # ASSIGN : s_11_2 700 # ASSIGN : s_11_3 936 # ASSIGN : s_11_4 1034 # ASSIGN : s_12_0 435 # ASSIGN : s_12_1 515 # ASSIGN : s_12_2 541 # ASSIGN : s_12_3 715 # ASSIGN : s_12_4 748 # ASSIGN : s_13_0 394 # ASSIGN : s_13_1 721 # ASSIGN : s_13_2 790 # ASSIGN : s_13_3 865 # ASSIGN : s_13_4 889 # ASSIGN : s_14_0 286 # ASSIGN : s_14_1 317 # ASSIGN : s_14_2 743 # ASSIGN : s_14_3 756 # ASSIGN : s_14_4 835 # ASSIGN : s_15_0 215 # ASSIGN : s_15_1 433 # ASSIGN : s_15_2 671 # ASSIGN : s_15_3 751 # ASSIGN : s_15_4 776 # ASSIGN : s_16_0 476 # ASSIGN : s_16_1 538 # ASSIGN : s_16_2 576 # ASSIGN : s_16_3 677 # ASSIGN : s_16_4 773 # ASSIGN : s_17_0 253 # ASSIGN : s_17_1 523 # ASSIGN : s_17_2 768 # ASSIGN : s_17_3 813 # ASSIGN : s_17_4 855 # ASSIGN : s_18_0 684 # ASSIGN : s_18_1 818 # ASSIGN : s_18_2 882 # ASSIGN : s_18_3 971 # ASSIGN : s_18_4 1067 # ASSIGN : s_19_0 865 # ASSIGN : s_19_1 883 # ASSIGN : s_19_2 906 # ASSIGN : s_19_3 933 # ASSIGN : s_19_4 1026 SHOW_RESULT 1162 END : 1162 (1 seconds) [Thu Jun 1 15:44:46 2006] SHOW_RESULT 1162 CPU : 0.349999999999994 = 0.349999999999994 + 0 + 0 + 0 # BOUND : makespan 1039 1162 MODIFY_CNF 1100 BEGIN : [Thu Jun 1 15:44:46 2006] MODIFY_CNF 1100 END : 59326471 bytes (0 seconds) [Thu Jun 1 15:44:46 2006] MODIFY_CNF 1100 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1100 BEGIN : [Thu Jun 1 15:44:46 2006] CMD : minisat /work/tamura/csp2sat98308.cnf /work/tamura/csp2sat98308.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1900298 5612699 | 633432 0 0 NaNQ | 0.000 % | ==============================================================================) restarts : 1 conflicts : 11 (4 /sec) decisions : 374 (141 /sec) propagations : 185077 (69851 /sec) inspects : 2567023 (968839 /sec) conflict literals : 100 (3.85 % deleted) CPU time : 2.64959 s SATISFIABLE VERIFY_CNF 1100 END : (4 seconds) [Thu Jun 1 15:44:50 2006] VERIFY_CNF 1100 CPU : 3.7 = 0 + 0.01 + 3.62 + 0.07 # RESULT : makespan 1100 SATISFIABLE SHOW_RESULT 1100 BEGIN : [Thu Jun 1 15:44:50 2006] # ASSIGN : makespan 1100 # ASSIGN : s_0_0 12 # ASSIGN : s_0_1 108 # ASSIGN : s_0_2 210 # ASSIGN : s_0_3 294 # ASSIGN : s_0_4 683 # ASSIGN : s_1_0 61 # ASSIGN : s_1_1 320 # ASSIGN : s_1_2 378 # ASSIGN : s_1_3 407 # ASSIGN : s_1_4 470 # ASSIGN : s_2_0 361 # ASSIGN : s_2_1 721 # ASSIGN : s_2_2 775 # ASSIGN : s_2_3 828 # ASSIGN : s_2_4 912 # ASSIGN : s_3_0 529 # ASSIGN : s_3_1 878 # ASSIGN : s_3_2 935 # ASSIGN : s_3_3 972 # ASSIGN : s_3_4 1046 # ASSIGN : s_4_0 111 # ASSIGN : s_4_1 317 # ASSIGN : s_4_2 378 # ASSIGN : s_4_3 425 # ASSIGN : s_4_4 1043 # ASSIGN : s_5_0 35 # ASSIGN : s_5_1 181 # ASSIGN : s_5_2 270 # ASSIGN : s_5_3 281 # ASSIGN : s_5_4 377 # ASSIGN : s_6_0 124 # ASSIGN : s_6_1 190 # ASSIGN : s_6_2 292 # ASSIGN : s_6_3 458 # ASSIGN : s_6_4 491 # ASSIGN : s_7_0 284 # ASSIGN : s_7_1 478 # ASSIGN : s_7_2 511 # ASSIGN : s_7_3 577 # ASSIGN : s_7_4 624 # ASSIGN : s_8_0 19 # ASSIGN : s_8_1 51 # ASSIGN : s_8_2 407 # ASSIGN : s_8_3 502 # ASSIGN : s_8_4 951 # ASSIGN : s_9_0 26 # ASSIGN : s_9_1 558 # ASSIGN : s_9_2 871 # ASSIGN : s_9_3 964 # ASSIGN : s_9_4 1017 # ASSIGN : s_10_0 45 # ASSIGN : s_10_1 115 # ASSIGN : s_10_2 179 # ASSIGN : s_10_3 598 # ASSIGN : s_10_4 708 # ASSIGN : s_11_0 275 # ASSIGN : s_11_1 325 # ASSIGN : s_11_2 638 # ASSIGN : s_11_3 866 # ASSIGN : s_11_4 964 # ASSIGN : s_12_0 195 # ASSIGN : s_12_1 360 # ASSIGN : s_12_2 386 # ASSIGN : s_12_3 653 # ASSIGN : s_12_4 723 # ASSIGN : s_13_0 339 # ASSIGN : s_13_1 659 # ASSIGN : s_13_2 728 # ASSIGN : s_13_3 803 # ASSIGN : s_13_4 827 # ASSIGN : s_14_0 446 # ASSIGN : s_14_1 461 # ASSIGN : s_14_2 681 # ASSIGN : s_14_3 694 # ASSIGN : s_14_4 1080 # ASSIGN : s_15_0 540 # ASSIGN : s_15_1 566 # ASSIGN : s_15_2 609 # ASSIGN : s_15_3 689 # ASSIGN : s_15_4 714 # ASSIGN : s_16_0 408 # ASSIGN : s_16_1 470 # ASSIGN : s_16_2 506 # ASSIGN : s_16_3 569 # ASSIGN : s_16_4 711 # ASSIGN : s_17_0 591 # ASSIGN : s_17_1 665 # ASSIGN : s_17_2 706 # ASSIGN : s_17_3 751 # ASSIGN : s_17_4 1070 # ASSIGN : s_18_0 659 # ASSIGN : s_18_1 756 # ASSIGN : s_18_2 820 # ASSIGN : s_18_3 909 # ASSIGN : s_18_4 1005 # ASSIGN : s_19_0 810 # ASSIGN : s_19_1 833 # ASSIGN : s_19_2 856 # ASSIGN : s_19_3 871 # ASSIGN : s_19_4 1038 SHOW_RESULT 1100 END : 1100 (0 seconds) [Thu Jun 1 15:44:50 2006] SHOW_RESULT 1100 CPU : 0.349999999999994 = 0.349999999999994 + 0 + 0 + 0 # BOUND : makespan 1039 1100 MODIFY_CNF 1069 BEGIN : [Thu Jun 1 15:44:50 2006] MODIFY_CNF 1069 END : 59326471 bytes (0 seconds) [Thu Jun 1 15:44:50 2006] MODIFY_CNF 1069 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1069 BEGIN : [Thu Jun 1 15:44:50 2006] CMD : minisat /work/tamura/csp2sat98308.cnf /work/tamura/csp2sat98308.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1838267 5429737 | 612755 0 0 NaNQ | 0.000 % | | 103 | 1838267 5429737 | 674030 103 1787 17.3 | 34.795 % | | 253 | 1838267 5429737 | 741433 253 4008 15.8 | 34.795 % | | 479 | 1838267 5429737 | 815576 479 10004 20.9 | 34.795 % | ==============================================================================) restarts : 4 conflicts : 769 (176 /sec) decisions : 1655 (379 /sec) propagations : 2241649 (513558 /sec) inspects : 33820842 (7748291 /sec) conflict literals : 13926 (9.39 % deleted) CPU time : 4.36494 s SATISFIABLE VERIFY_CNF 1069 END : (6 seconds) [Thu Jun 1 15:44:56 2006] VERIFY_CNF 1069 CPU : 5.73000000000002 = 0.0100000000000193 + 0.00999999999999998 + 5.48 + 0.23 # RESULT : makespan 1069 SATISFIABLE SHOW_RESULT 1069 BEGIN : [Thu Jun 1 15:44:56 2006] # ASSIGN : makespan 1069 # ASSIGN : s_0_0 90 # ASSIGN : s_0_1 117 # ASSIGN : s_0_2 407 # ASSIGN : s_0_3 788 # ASSIGN : s_0_4 858 # ASSIGN : s_1_0 104 # ASSIGN : s_1_1 799 # ASSIGN : s_1_2 849 # ASSIGN : s_1_3 969 # ASSIGN : s_1_4 1028 # ASSIGN : s_2_0 179 # ASSIGN : s_2_1 195 # ASSIGN : s_2_2 283 # ASSIGN : s_2_3 335 # ASSIGN : s_2_4 376 # ASSIGN : s_3_0 179 # ASSIGN : s_3_1 249 # ASSIGN : s_3_2 336 # ASSIGN : s_3_3 373 # ASSIGN : s_3_4 454 # ASSIGN : s_4_0 517 # ASSIGN : s_4_1 589 # ASSIGN : s_4_2 653 # ASSIGN : s_4_3 683 # ASSIGN : s_4_4 972 # ASSIGN : s_5_0 1 # ASSIGN : s_5_1 95 # ASSIGN : s_5_2 184 # ASSIGN : s_5_3 199 # ASSIGN : s_5_4 712 # ASSIGN : s_6_0 113 # ASSIGN : s_6_1 285 # ASSIGN : s_6_2 484 # ASSIGN : s_6_3 684 # ASSIGN : s_6_4 704 # ASSIGN : s_7_0 169 # ASSIGN : s_7_1 570 # ASSIGN : s_7_2 596 # ASSIGN : s_7_3 651 # ASSIGN : s_7_4 717 # ASSIGN : s_8_0 278 # ASSIGN : s_8_1 724 # ASSIGN : s_8_2 801 # ASSIGN : s_8_3 840 # ASSIGN : s_8_4 896 # ASSIGN : s_9_0 98 # ASSIGN : s_9_1 137 # ASSIGN : s_9_2 177 # ASSIGN : s_9_3 327 # ASSIGN : s_9_4 421 # ASSIGN : s_10_0 35 # ASSIGN : s_10_1 263 # ASSIGN : s_10_2 393 # ASSIGN : s_10_3 594 # ASSIGN : s_10_4 650 # ASSIGN : s_11_0 241 # ASSIGN : s_11_1 306 # ASSIGN : s_11_2 491 # ASSIGN : s_11_3 833 # ASSIGN : s_11_4 987 # ASSIGN : s_12_0 341 # ASSIGN : s_12_1 428 # ASSIGN : s_12_2 585 # ASSIGN : s_12_3 793 # ASSIGN : s_12_4 941 # ASSIGN : s_13_0 557 # ASSIGN : s_13_1 662 # ASSIGN : s_13_2 875 # ASSIGN : s_13_3 950 # ASSIGN : s_13_4 979 # ASSIGN : s_14_0 504 # ASSIGN : s_14_1 756 # ASSIGN : s_14_2 949 # ASSIGN : s_14_3 957 # ASSIGN : s_14_4 1049 # ASSIGN : s_15_0 367 # ASSIGN : s_15_1 447 # ASSIGN : s_15_2 508 # ASSIGN : s_15_3 634 # ASSIGN : s_15_4 656 # ASSIGN : s_16_0 490 # ASSIGN : s_16_1 552 # ASSIGN : s_16_2 588 # ASSIGN : s_16_3 660 # ASSIGN : s_16_4 1029 # ASSIGN : s_17_0 519 # ASSIGN : s_17_1 835 # ASSIGN : s_17_2 853 # ASSIGN : s_17_3 926 # ASSIGN : s_17_4 931 # ASSIGN : s_18_0 199 # ASSIGN : s_18_1 506 # ASSIGN : s_18_2 764 # ASSIGN : s_18_3 878 # ASSIGN : s_18_4 974 # ASSIGN : s_19_0 77 # ASSIGN : s_19_1 114 # ASSIGN : s_19_2 154 # ASSIGN : s_19_3 1023 # ASSIGN : s_19_4 1061 SHOW_RESULT 1069 END : 1069 (0 seconds) [Thu Jun 1 15:44:56 2006] SHOW_RESULT 1069 CPU : 0.349999999999994 = 0.349999999999994 + 0 + 0 + 0 # BOUND : makespan 1039 1069 MODIFY_CNF 1054 BEGIN : [Thu Jun 1 15:44:56 2006] MODIFY_CNF 1054 END : 59326471 bytes (0 seconds) [Thu Jun 1 15:44:56 2006] MODIFY_CNF 1054 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1054 BEGIN : [Thu Jun 1 15:44:56 2006] CMD : minisat /work/tamura/csp2sat98308.cnf /work/tamura/csp2sat98308.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1808252 5341207 | 602750 0 0 NaNQ | 0.000 % | | 103 | 1808252 5341207 | 663025 103 1580 15.3 | 35.951 % | | 253 | 1808252 5341207 | 729327 253 3411 13.5 | 35.951 % | | 478 | 1808252 5341207 | 802260 478 6762 14.1 | 35.951 % | | 816 | 1808252 5341207 | 882486 816 15056 18.5 | 35.951 % | ==============================================================================) restarts : 5 conflicts : 830 (165 /sec) decisions : 1897 (377 /sec) propagations : 2899263 (575868 /sec) inspects : 46371874 (9210639 /sec) conflict literals : 15198 (14.59 % deleted) CPU time : 5.0346 s SATISFIABLE VERIFY_CNF 1054 END : (6 seconds) [Thu Jun 1 15:45:02 2006] VERIFY_CNF 1054 CPU : 6.14999999999999 = 0.00999999999999091 + 0.01 + 6.06 + 0.07 # RESULT : makespan 1054 SATISFIABLE SHOW_RESULT 1054 BEGIN : [Thu Jun 1 15:45:02 2006] # ASSIGN : makespan 1054 # ASSIGN : s_0_0 301 # ASSIGN : s_0_1 678 # ASSIGN : s_0_2 777 # ASSIGN : s_0_3 861 # ASSIGN : s_0_4 1016 # ASSIGN : s_1_0 441 # ASSIGN : s_1_1 510 # ASSIGN : s_1_2 551 # ASSIGN : s_1_3 872 # ASSIGN : s_1_4 906 # ASSIGN : s_2_0 7 # ASSIGN : s_2_1 23 # ASSIGN : s_2_2 144 # ASSIGN : s_2_3 196 # ASSIGN : s_2_4 287 # ASSIGN : s_3_0 239 # ASSIGN : s_3_1 341 # ASSIGN : s_3_2 398 # ASSIGN : s_3_3 787 # ASSIGN : s_3_4 992 # ASSIGN : s_4_0 212 # ASSIGN : s_4_1 324 # ASSIGN : s_4_2 473 # ASSIGN : s_4_3 523 # ASSIGN : s_4_4 611 # ASSIGN : s_5_0 18 # ASSIGN : s_5_1 107 # ASSIGN : s_5_2 197 # ASSIGN : s_5_3 208 # ASSIGN : s_5_4 668 # ASSIGN : s_6_0 800 # ASSIGN : s_6_1 890 # ASSIGN : s_6_2 981 # ASSIGN : s_6_3 1014 # ASSIGN : s_6_4 1034 # ASSIGN : s_7_0 15 # ASSIGN : s_7_1 28 # ASSIGN : s_7_2 52 # ASSIGN : s_7_3 339 # ASSIGN : s_7_4 467 # ASSIGN : s_8_0 10 # ASSIGN : s_8_1 298 # ASSIGN : s_8_2 385 # ASSIGN : s_8_3 435 # ASSIGN : s_8_4 491 # ASSIGN : s_9_0 80 # ASSIGN : s_9_1 148 # ASSIGN : s_9_2 190 # ASSIGN : s_9_3 779 # ASSIGN : s_9_4 965 # ASSIGN : s_10_0 17 # ASSIGN : s_10_1 601 # ASSIGN : s_10_2 665 # ASSIGN : s_10_3 901 # ASSIGN : s_10_4 1048 # ASSIGN : s_11_0 197 # ASSIGN : s_11_1 280 # ASSIGN : s_11_2 383 # ASSIGN : s_11_3 503 # ASSIGN : s_11_4 604 # ASSIGN : s_12_0 720 # ASSIGN : s_12_1 840 # ASSIGN : s_12_2 866 # ASSIGN : s_12_3 941 # ASSIGN : s_12_4 947 # ASSIGN : s_13_0 13 # ASSIGN : s_13_1 77 # ASSIGN : s_13_2 99 # ASSIGN : s_13_3 545 # ASSIGN : s_13_4 676 # ASSIGN : s_14_0 3 # ASSIGN : s_14_1 77 # ASSIGN : s_14_2 188 # ASSIGN : s_14_3 196 # ASSIGN : s_14_4 927 # ASSIGN : s_15_0 415 # ASSIGN : s_15_1 717 # ASSIGN : s_15_2 760 # ASSIGN : s_15_3 879 # ASSIGN : s_15_4 904 # ASSIGN : s_16_0 362 # ASSIGN : s_16_1 424 # ASSIGN : s_16_2 460 # ASSIGN : s_16_3 569 # ASSIGN : s_16_4 974 # ASSIGN : s_17_0 111 # ASSIGN : s_17_1 156 # ASSIGN : s_17_2 174 # ASSIGN : s_17_3 749 # ASSIGN : s_17_4 769 # ASSIGN : s_18_0 234 # ASSIGN : s_18_1 307 # ASSIGN : s_18_2 371 # ASSIGN : s_18_3 580 # ASSIGN : s_18_4 756 # ASSIGN : s_19_0 455 # ASSIGN : s_19_1 754 # ASSIGN : s_19_2 851 # ASSIGN : s_19_3 866 # ASSIGN : s_19_4 1046 SHOW_RESULT 1054 END : 1054 (1 seconds) [Thu Jun 1 15:45:03 2006] SHOW_RESULT 1054 CPU : 0.349999999999994 = 0.349999999999994 + 0 + 0 + 0 # BOUND : makespan 1039 1054 MODIFY_CNF 1046 BEGIN : [Thu Jun 1 15:45:03 2006] MODIFY_CNF 1046 END : 59326470 bytes (0 seconds) [Thu Jun 1 15:45:03 2006] MODIFY_CNF 1046 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1046 BEGIN : [Thu Jun 1 15:45:03 2006] CMD : minisat /work/tamura/csp2sat98308.cnf /work/tamura/csp2sat98308.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1792244 5293991 | 597414 0 0 NaNQ | 0.000 % | | 101 | 1792244 5293991 | 657155 101 2217 22.0 | 36.568 % | | 252 | 1792244 5293991 | 722870 252 4401 17.5 | 36.568 % | ==============================================================================) restarts : 3 conflicts : 358 (92 /sec) decisions : 1059 (272 /sec) propagations : 1526705 (391575 /sec) inspects : 22681434 (5817414 /sec) conflict literals : 5902 (15.30 % deleted) CPU time : 3.89889 s SATISFIABLE VERIFY_CNF 1046 END : (5 seconds) [Thu Jun 1 15:45:08 2006] VERIFY_CNF 1046 CPU : 5.04000000000002 = 0.0100000000000193 + 0.01 + 4.95 + 0.07 # RESULT : makespan 1046 SATISFIABLE SHOW_RESULT 1046 BEGIN : [Thu Jun 1 15:45:08 2006] # ASSIGN : makespan 1046 # ASSIGN : s_0_0 415 # ASSIGN : s_0_1 542 # ASSIGN : s_0_2 625 # ASSIGN : s_0_3 730 # ASSIGN : s_0_4 1008 # ASSIGN : s_1_0 396 # ASSIGN : s_1_1 522 # ASSIGN : s_1_2 845 # ASSIGN : s_1_3 879 # ASSIGN : s_1_4 898 # ASSIGN : s_2_0 104 # ASSIGN : s_2_1 120 # ASSIGN : s_2_2 321 # ASSIGN : s_2_3 660 # ASSIGN : s_2_4 698 # ASSIGN : s_3_0 438 # ASSIGN : s_3_1 730 # ASSIGN : s_3_2 787 # ASSIGN : s_3_3 824 # ASSIGN : s_3_4 984 # ASSIGN : s_4_0 192 # ASSIGN : s_4_1 260 # ASSIGN : s_4_2 339 # ASSIGN : s_4_3 369 # ASSIGN : s_4_4 563 # ASSIGN : s_5_0 15 # ASSIGN : s_5_1 186 # ASSIGN : s_5_2 279 # ASSIGN : s_5_3 290 # ASSIGN : s_5_4 403 # ASSIGN : s_6_0 635 # ASSIGN : s_6_1 750 # ASSIGN : s_6_2 845 # ASSIGN : s_6_3 899 # ASSIGN : s_6_4 919 # ASSIGN : s_7_0 33 # ASSIGN : s_7_1 80 # ASSIGN : s_7_2 131 # ASSIGN : s_7_3 236 # ASSIGN : s_7_4 912 # ASSIGN : s_8_0 86 # ASSIGN : s_8_1 380 # ASSIGN : s_8_2 500 # ASSIGN : s_8_3 731 # ASSIGN : s_8_4 791 # ASSIGN : s_9_0 67 # ASSIGN : s_9_1 299 # ASSIGN : s_9_2 537 # ASSIGN : s_9_3 652 # ASSIGN : s_9_4 701 # ASSIGN : s_10_0 4 # ASSIGN : s_10_1 462 # ASSIGN : s_10_2 544 # ASSIGN : s_10_3 966 # ASSIGN : s_10_4 1040 # ASSIGN : s_11_0 373 # ASSIGN : s_11_1 446 # ASSIGN : s_11_2 507 # ASSIGN : s_11_3 526 # ASSIGN : s_11_4 624 # ASSIGN : s_12_0 180 # ASSIGN : s_12_1 841 # ASSIGN : s_12_2 878 # ASSIGN : s_12_3 953 # ASSIGN : s_12_4 959 # ASSIGN : s_13_0 775 # ASSIGN : s_13_1 837 # ASSIGN : s_13_2 897 # ASSIGN : s_13_3 972 # ASSIGN : s_13_4 996 # ASSIGN : s_14_0 0 # ASSIGN : s_14_1 41 # ASSIGN : s_14_2 859 # ASSIGN : s_14_3 867 # ASSIGN : s_14_4 939 # ASSIGN : s_15_0 0 # ASSIGN : s_15_1 26 # ASSIGN : s_15_2 93 # ASSIGN : s_15_3 709 # ASSIGN : s_15_4 784 # ASSIGN : s_16_0 69 # ASSIGN : s_16_1 137 # ASSIGN : s_16_2 173 # ASSIGN : s_16_3 300 # ASSIGN : s_16_4 1006 # ASSIGN : s_17_0 104 # ASSIGN : s_17_1 174 # ASSIGN : s_17_2 268 # ASSIGN : s_17_3 620 # ASSIGN : s_17_4 814 # ASSIGN : s_18_0 275 # ASSIGN : s_18_1 339 # ASSIGN : s_18_2 450 # ASSIGN : s_18_3 539 # ASSIGN : s_18_4 635 # ASSIGN : s_19_0 444 # ASSIGN : s_19_1 484 # ASSIGN : s_19_2 522 # ASSIGN : s_19_3 874 # ASSIGN : s_19_4 1038 SHOW_RESULT 1046 END : 1046 (0 seconds) [Thu Jun 1 15:45:08 2006] SHOW_RESULT 1046 CPU : 0.349999999999994 = 0.349999999999994 + 0 + 0 + 0 # BOUND : makespan 1039 1046 MODIFY_CNF 1042 BEGIN : [Thu Jun 1 15:45:08 2006] MODIFY_CNF 1042 END : 59326470 bytes (0 seconds) [Thu Jun 1 15:45:08 2006] MODIFY_CNF 1042 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1042 BEGIN : [Thu Jun 1 15:45:08 2006] CMD : minisat /work/tamura/csp2sat98308.cnf /work/tamura/csp2sat98308.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1784240 5270383 | 594746 0 0 NaNQ | 0.000 % | | 100 | 1784240 5270383 | 654220 100 1960 19.6 | 36.876 % | ==============================================================================) restarts : 2 conflicts : 149 (47 /sec) decisions : 625 (195 /sec) propagations : 562738 (175850 /sec) inspects : 9516008 (2973652 /sec) conflict literals : 2525 (10.11 % deleted) CPU time : 3.20011 s SATISFIABLE VERIFY_CNF 1042 END : (5 seconds) [Thu Jun 1 15:45:13 2006] VERIFY_CNF 1042 CPU : 4.42999999999999 = 0.00999999999999091 + 0.00999999999999998 + 4.19 + 0.22 # RESULT : makespan 1042 SATISFIABLE SHOW_RESULT 1042 BEGIN : [Thu Jun 1 15:45:13 2006] # ASSIGN : makespan 1042 # ASSIGN : s_0_0 0 # ASSIGN : s_0_1 83 # ASSIGN : s_0_2 376 # ASSIGN : s_0_3 460 # ASSIGN : s_0_4 510 # ASSIGN : s_1_0 164 # ASSIGN : s_1_1 814 # ASSIGN : s_1_2 863 # ASSIGN : s_1_3 896 # ASSIGN : s_1_4 971 # ASSIGN : s_2_0 8 # ASSIGN : s_2_1 58 # ASSIGN : s_2_2 112 # ASSIGN : s_2_3 505 # ASSIGN : s_2_4 543 # ASSIGN : s_3_0 482 # ASSIGN : s_3_1 548 # ASSIGN : s_3_2 637 # ASSIGN : s_3_3 701 # ASSIGN : s_3_4 914 # ASSIGN : s_4_0 221 # ASSIGN : s_4_1 382 # ASSIGN : s_4_2 565 # ASSIGN : s_4_3 595 # ASSIGN : s_4_4 915 # ASSIGN : s_5_0 23 # ASSIGN : s_5_1 290 # ASSIGN : s_5_2 380 # ASSIGN : s_5_3 464 # ASSIGN : s_5_4 556 # ASSIGN : s_6_0 672 # ASSIGN : s_6_1 738 # ASSIGN : s_6_2 859 # ASSIGN : s_6_3 972 # ASSIGN : s_6_4 992 # ASSIGN : s_7_0 50 # ASSIGN : s_7_1 64 # ASSIGN : s_7_2 88 # ASSIGN : s_7_3 165 # ASSIGN : s_7_4 202 # ASSIGN : s_8_0 294 # ASSIGN : s_8_1 379 # ASSIGN : s_8_2 443 # ASSIGN : s_8_3 500 # ASSIGN : s_8_4 988 # ASSIGN : s_9_0 1 # ASSIGN : s_9_1 24 # ASSIGN : s_9_2 214 # ASSIGN : s_9_3 775 # ASSIGN : s_9_4 953 # ASSIGN : s_10_0 20 # ASSIGN : s_10_1 225 # ASSIGN : s_10_2 289 # ASSIGN : s_10_3 875 # ASSIGN : s_10_4 1036 # ASSIGN : s_11_0 741 # ASSIGN : s_11_1 794 # ASSIGN : s_11_2 855 # ASSIGN : s_11_3 870 # ASSIGN : s_11_4 968 # ASSIGN : s_12_0 559 # ASSIGN : s_12_1 676 # ASSIGN : s_12_2 702 # ASSIGN : s_12_3 777 # ASSIGN : s_12_4 783 # ASSIGN : s_13_0 186 # ASSIGN : s_13_1 354 # ASSIGN : s_13_2 381 # ASSIGN : s_13_3 486 # ASSIGN : s_13_4 819 # ASSIGN : s_14_0 544 # ASSIGN : s_14_1 605 # ASSIGN : s_14_2 696 # ASSIGN : s_14_3 704 # ASSIGN : s_14_4 1012 # ASSIGN : s_15_0 117 # ASSIGN : s_15_1 143 # ASSIGN : s_15_2 301 # ASSIGN : s_15_3 674 # ASSIGN : s_15_4 892 # ASSIGN : s_16_0 639 # ASSIGN : s_16_1 783 # ASSIGN : s_16_2 829 # ASSIGN : s_16_3 892 # ASSIGN : s_16_4 1002 # ASSIGN : s_17_0 639 # ASSIGN : s_17_1 684 # ASSIGN : s_17_2 716 # ASSIGN : s_17_3 997 # ASSIGN : s_17_4 1032 # ASSIGN : s_18_0 6 # ASSIGN : s_18_1 133 # ASSIGN : s_18_2 197 # ASSIGN : s_18_3 286 # ASSIGN : s_18_4 391 # ASSIGN : s_19_0 70 # ASSIGN : s_19_1 110 # ASSIGN : s_19_2 149 # ASSIGN : s_19_3 164 # ASSIGN : s_19_4 456 SHOW_RESULT 1042 END : 1042 (0 seconds) [Thu Jun 1 15:45:13 2006] SHOW_RESULT 1042 CPU : 0.360000000000014 = 0.360000000000014 + 0 + 0 + 0 # BOUND : makespan 1039 1042 MODIFY_CNF 1040 BEGIN : [Thu Jun 1 15:45:13 2006] MODIFY_CNF 1040 END : 59326470 bytes (0 seconds) [Thu Jun 1 15:45:13 2006] MODIFY_CNF 1040 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1040 BEGIN : [Thu Jun 1 15:45:13 2006] CMD : minisat /work/tamura/csp2sat98308.cnf /work/tamura/csp2sat98308.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1780238 5258579 | 593412 0 0 NaNQ | 0.000 % | | 101 | 1780238 5258579 | 652753 101 2303 22.8 | 37.030 % | | 251 | 1780238 5258579 | 718028 251 4588 18.3 | 37.030 % | | 476 | 1780238 5258579 | 789831 476 8505 17.9 | 37.030 % | | 813 | 1780238 5258579 | 868814 813 13225 16.3 | 37.030 % | | 1319 | 1780238 5258579 | 955695 1319 20926 15.9 | 37.030 % | ==============================================================================) restarts : 6 conflicts : 1497 (214 /sec) decisions : 2822 (403 /sec) propagations : 6192812 (883569 /sec) inspects : 83392349 (11898128 /sec) conflict literals : 23009 (22.67 % deleted) CPU time : 7.00886 s SATISFIABLE VERIFY_CNF 1040 END : (8 seconds) [Thu Jun 1 15:45:21 2006] VERIFY_CNF 1040 CPU : 8.11 = 0 + 0.01 + 8.03 + 0.0700000000000001 # RESULT : makespan 1040 SATISFIABLE SHOW_RESULT 1040 BEGIN : [Thu Jun 1 15:45:21 2006] # ASSIGN : makespan 1040 # ASSIGN : s_0_0 16 # ASSIGN : s_0_1 349 # ASSIGN : s_0_2 431 # ASSIGN : s_0_3 515 # ASSIGN : s_0_4 757 # ASSIGN : s_1_0 134 # ASSIGN : s_1_1 207 # ASSIGN : s_1_2 927 # ASSIGN : s_1_3 970 # ASSIGN : s_1_4 1019 # ASSIGN : s_2_0 20 # ASSIGN : s_2_1 36 # ASSIGN : s_2_2 718 # ASSIGN : s_2_3 894 # ASSIGN : s_2_4 988 # ASSIGN : s_3_0 584 # ASSIGN : s_3_1 664 # ASSIGN : s_3_2 724 # ASSIGN : s_3_3 761 # ASSIGN : s_3_4 835 # ASSIGN : s_4_0 444 # ASSIGN : s_4_1 770 # ASSIGN : s_4_2 859 # ASSIGN : s_4_3 889 # ASSIGN : s_4_4 983 # ASSIGN : s_5_0 417 # ASSIGN : s_5_1 560 # ASSIGN : s_5_2 649 # ASSIGN : s_5_3 660 # ASSIGN : s_5_4 845 # ASSIGN : s_6_0 39 # ASSIGN : s_6_1 258 # ASSIGN : s_6_2 378 # ASSIGN : s_6_3 411 # ASSIGN : s_6_4 475 # ASSIGN : s_7_0 119 # ASSIGN : s_7_1 270 # ASSIGN : s_7_2 294 # ASSIGN : s_7_3 438 # ASSIGN : s_7_4 956 # ASSIGN : s_8_0 86 # ASSIGN : s_8_1 349 # ASSIGN : s_8_2 646 # ASSIGN : s_8_3 784 # ASSIGN : s_8_4 891 # ASSIGN : s_9_0 4 # ASSIGN : s_9_1 87 # ASSIGN : s_9_2 127 # ASSIGN : s_9_3 135 # ASSIGN : s_9_4 143 # ASSIGN : s_10_0 23 # ASSIGN : s_10_1 144 # ASSIGN : s_10_2 208 # ASSIGN : s_10_3 363 # ASSIGN : s_10_4 411 # ASSIGN : s_11_0 542 # ASSIGN : s_11_1 587 # ASSIGN : s_11_2 648 # ASSIGN : s_11_3 663 # ASSIGN : s_11_4 761 # ASSIGN : s_12_0 331 # ASSIGN : s_12_1 482 # ASSIGN : s_12_2 512 # ASSIGN : s_12_3 926 # ASSIGN : s_12_4 932 # ASSIGN : s_13_0 3 # ASSIGN : s_13_1 42 # ASSIGN : s_13_2 93 # ASSIGN : s_13_3 184 # ASSIGN : s_13_4 226 # ASSIGN : s_14_0 1 # ASSIGN : s_14_1 299 # ASSIGN : s_14_2 403 # ASSIGN : s_14_3 470 # ASSIGN : s_14_4 495 # ASSIGN : s_15_0 10 # ASSIGN : s_15_1 92 # ASSIGN : s_15_2 168 # ASSIGN : s_15_3 248 # ASSIGN : s_15_4 270 # ASSIGN : s_16_0 413 # ASSIGN : s_16_1 506 # ASSIGN : s_16_2 597 # ASSIGN : s_16_3 795 # ASSIGN : s_16_4 943 # ASSIGN : s_17_0 685 # ASSIGN : s_17_1 721 # ASSIGN : s_17_2 739 # ASSIGN : s_17_3 840 # ASSIGN : s_17_4 849 # ASSIGN : s_18_0 230 # ASSIGN : s_18_1 299 # ASSIGN : s_18_2 508 # ASSIGN : s_18_3 831 # ASSIGN : s_18_4 945 # ASSIGN : s_19_0 46 # ASSIGN : s_19_1 64 # ASSIGN : s_19_2 90 # ASSIGN : s_19_3 105 # ASSIGN : s_19_4 250 SHOW_RESULT 1040 END : 1040 (1 seconds) [Thu Jun 1 15:45:22 2006] SHOW_RESULT 1040 CPU : 0.349999999999994 = 0.349999999999994 + 0 + 0 + 0 # BOUND : makespan 1039 1040 MODIFY_CNF 1039 BEGIN : [Thu Jun 1 15:45:22 2006] MODIFY_CNF 1039 END : 59326470 bytes (0 seconds) [Thu Jun 1 15:45:22 2006] MODIFY_CNF 1039 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1039 BEGIN : [Thu Jun 1 15:45:22 2006] CMD : minisat /work/tamura/csp2sat98308.cnf /work/tamura/csp2sat98308.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1778238 5252679 | 592746 0 0 NaNQ | 0.000 % | | 100 | 1778238 5252679 | 652020 100 1884 18.8 | 37.107 % | | 250 | 1778238 5252679 | 717222 250 5048 20.2 | 37.107 % | | 476 | 1778238 5252679 | 788944 476 6982 14.7 | 37.108 % | | 813 | 1778238 5252679 | 867839 813 10843 13.3 | 37.107 % | | 1320 | 1778238 5252679 | 954623 1320 19950 15.1 | 37.108 % | | 2079 | 1778238 5252679 | 1050085 2079 31609 15.2 | 37.107 % | | 3218 | 1778238 5252679 | 1155094 3218 46102 14.3 | 37.107 % | ==============================================================================) restarts : 8 conflicts : 4732 (392 /sec) decisions : 7597 (629 /sec) propagations : 14886623 (1231826 /sec) inspects : 194248232 (16073487 /sec) conflict literals : 72171 (18.53 % deleted) CPU time : 12.085 s SATISFIABLE VERIFY_CNF 1039 END : (13 seconds) [Thu Jun 1 15:45:35 2006] VERIFY_CNF 1039 CPU : 13.29 = 0 + 0.01 + 13.21 + 0.07 # RESULT : makespan 1039 SATISFIABLE SHOW_RESULT 1039 BEGIN : [Thu Jun 1 15:45:35 2006] # ASSIGN : makespan 1039 # ASSIGN : s_0_0 414 # ASSIGN : s_0_1 482 # ASSIGN : s_0_2 616 # ASSIGN : s_0_3 861 # ASSIGN : s_0_4 906 # ASSIGN : s_1_0 70 # ASSIGN : s_1_1 527 # ASSIGN : s_1_2 921 # ASSIGN : s_1_3 970 # ASSIGN : s_1_4 988 # ASSIGN : s_2_0 0 # ASSIGN : s_2_1 16 # ASSIGN : s_2_2 347 # ASSIGN : s_2_3 489 # ASSIGN : s_2_4 706 # ASSIGN : s_3_0 249 # ASSIGN : s_3_1 321 # ASSIGN : s_3_2 378 # ASSIGN : s_3_3 415 # ASSIGN : s_3_4 758 # ASSIGN : s_4_0 120 # ASSIGN : s_4_1 188 # ASSIGN : s_4_2 744 # ASSIGN : s_4_3 886 # ASSIGN : s_4_4 967 # ASSIGN : s_5_0 437 # ASSIGN : s_5_1 527 # ASSIGN : s_5_2 616 # ASSIGN : s_5_3 627 # ASSIGN : s_5_4 708 # ASSIGN : s_6_0 122 # ASSIGN : s_6_1 359 # ASSIGN : s_6_2 486 # ASSIGN : s_6_3 568 # ASSIGN : s_6_4 968 # ASSIGN : s_7_0 230 # ASSIGN : s_7_1 238 # ASSIGN : s_7_2 262 # ASSIGN : s_7_3 450 # ASSIGN : s_7_4 597 # ASSIGN : s_8_0 19 # ASSIGN : s_8_1 616 # ASSIGN : s_8_2 681 # ASSIGN : s_8_3 789 # ASSIGN : s_8_4 845 # ASSIGN : s_9_0 0 # ASSIGN : s_9_1 847 # ASSIGN : s_9_2 899 # ASSIGN : s_9_3 948 # ASSIGN : s_9_4 956 # ASSIGN : s_10_0 26 # ASSIGN : s_10_1 680 # ASSIGN : s_10_2 754 # ASSIGN : s_10_3 887 # ASSIGN : s_10_4 950 # ASSIGN : s_11_0 80 # ASSIGN : s_11_1 241 # ASSIGN : s_11_2 302 # ASSIGN : s_11_3 317 # ASSIGN : s_11_4 812 # ASSIGN : s_12_0 0 # ASSIGN : s_12_1 89 # ASSIGN : s_12_2 411 # ASSIGN : s_12_3 610 # ASSIGN : s_12_4 774 # ASSIGN : s_13_0 23 # ASSIGN : s_13_1 93 # ASSIGN : s_13_2 115 # ASSIGN : s_13_3 730 # ASSIGN : s_13_4 781 # ASSIGN : s_14_0 399 # ASSIGN : s_14_1 519 # ASSIGN : s_14_2 700 # ASSIGN : s_14_3 990 # ASSIGN : s_14_4 1009 # ASSIGN : s_15_0 193 # ASSIGN : s_15_1 219 # ASSIGN : s_15_2 279 # ASSIGN : s_15_3 588 # ASSIGN : s_15_4 720 # ASSIGN : s_16_0 157 # ASSIGN : s_16_1 311 # ASSIGN : s_16_2 564 # ASSIGN : s_16_3 634 # ASSIGN : s_16_4 927 # ASSIGN : s_17_0 564 # ASSIGN : s_17_1 598 # ASSIGN : s_17_2 1002 # ASSIGN : s_17_3 1024 # ASSIGN : s_17_4 1029 # ASSIGN : s_18_0 62 # ASSIGN : s_18_1 126 # ASSIGN : s_18_2 190 # ASSIGN : s_18_3 825 # ASSIGN : s_18_4 944 # ASSIGN : s_19_0 139 # ASSIGN : s_19_1 355 # ASSIGN : s_19_2 396 # ASSIGN : s_19_3 526 # ASSIGN : s_19_4 1031 SHOW_RESULT 1039 END : 1039 (1 seconds) [Thu Jun 1 15:45:36 2006] SHOW_RESULT 1039 CPU : 0.370000000000005 = 0.370000000000005 + 0 + 0 + 0 # BOUND : makespan 1039 1039 MAIN END : (185 seconds) [Thu Jun 1 15:45:36 2006] MAIN CPU : 183.66 = 133.5 + 0.25 + 49.06 + 0.85