MAIN BEGIN : [Thu Jun 1 16:52:35 2006] READ BEGIN : csp/la24.csp [Thu Jun 1 16:52:35 2006] READ END : csp/la24.csp (3 seconds) [Thu Jun 1 16:52:38 2006] READ CPU : 3.09 = 3.09 + 0 + 0 + 0 # BOUND : makespan 857 1356 GENERATE_CNF 1356 BEGIN : [Thu Jun 1 16:52:38 2006] GENERATE_CNF 1356 END : 206451 variables 3132690 clauses 73284012 bytes (153 seconds) [Thu Jun 1 16:55:11 2006] GENERATE_CNF 1356 CPU : 153.31 = 153.09 + 0.22 + 0 + 0 MODIFY_CNF 1106 BEGIN : [Thu Jun 1 16:55:11 2006] MODIFY_CNF 1106 END : 73284018 bytes (0 seconds) [Thu Jun 1 16:55:11 2006] MODIFY_CNF 1106 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1106 BEGIN : [Thu Jun 1 16:55:11 2006] CMD : minisat /work/tamura/csp2sat62102.cnf /work/tamura/csp2sat62102.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1585948 4667766 | 528649 0 0 NaNQ | 0.000 % | ==============================================================================) restarts : 1 conflicts : 12 (3 /sec) decisions : 269 (73 /sec) propagations : 276762 (75421 /sec) inspects : 2650717 (722351 /sec) conflict literals : 86 (2.27 % deleted) CPU time : 3.66957 s SATISFIABLE VERIFY_CNF 1106 END : (5 seconds) [Thu Jun 1 16:55:16 2006] VERIFY_CNF 1106 CPU : 4.66 = 0 + 0.00999999999999995 + 4.59 + 0.06 # RESULT : makespan 1106 SATISFIABLE SHOW_RESULT 1106 BEGIN : [Thu Jun 1 16:55:16 2006] # ASSIGN : makespan 1106 # ASSIGN : s_0_0 15 # ASSIGN : s_0_1 84 # ASSIGN : s_0_2 159 # ASSIGN : s_0_3 231 # ASSIGN : s_0_4 358 # ASSIGN : s_0_5 388 # ASSIGN : s_0_6 589 # ASSIGN : s_0_7 768 # ASSIGN : s_0_8 866 # ASSIGN : s_0_9 892 # ASSIGN : s_1_0 44 # ASSIGN : s_1_1 107 # ASSIGN : s_1_2 219 # ASSIGN : s_1_3 262 # ASSIGN : s_1_4 285 # ASSIGN : s_1_5 494 # ASSIGN : s_1_6 755 # ASSIGN : s_1_7 803 # ASSIGN : s_1_8 927 # ASSIGN : s_1_9 994 # ASSIGN : s_2_0 98 # ASSIGN : s_2_1 289 # ASSIGN : s_2_2 405 # ASSIGN : s_2_3 533 # ASSIGN : s_2_4 540 # ASSIGN : s_2_5 627 # ASSIGN : s_2_6 889 # ASSIGN : s_2_7 946 # ASSIGN : s_2_8 1018 # ASSIGN : s_2_9 1060 # ASSIGN : s_3_0 148 # ASSIGN : s_3_1 216 # ASSIGN : s_3_2 259 # ASSIGN : s_3_3 373 # ASSIGN : s_3_4 485 # ASSIGN : s_3_5 595 # ASSIGN : s_3_6 717 # ASSIGN : s_3_7 911 # ASSIGN : s_3_8 1007 # ASSIGN : s_3_9 1025 # ASSIGN : s_4_0 122 # ASSIGN : s_4_1 314 # ASSIGN : s_4_2 348 # ASSIGN : s_4_3 398 # ASSIGN : s_4_4 411 # ASSIGN : s_4_5 523 # ASSIGN : s_4_6 724 # ASSIGN : s_4_7 768 # ASSIGN : s_4_8 829 # ASSIGN : s_4_9 902 # ASSIGN : s_5_0 11 # ASSIGN : s_5_1 71 # ASSIGN : s_5_2 167 # ASSIGN : s_5_3 326 # ASSIGN : s_5_4 485 # ASSIGN : s_5_5 681 # ASSIGN : s_5_6 895 # ASSIGN : s_5_7 1012 # ASSIGN : s_5_8 1062 # ASSIGN : s_5_9 1097 # ASSIGN : s_6_0 63 # ASSIGN : s_6_1 375 # ASSIGN : s_6_2 493 # ASSIGN : s_6_3 565 # ASSIGN : s_6_4 655 # ASSIGN : s_6_5 753 # ASSIGN : s_6_6 761 # ASSIGN : s_6_7 811 # ASSIGN : s_6_8 889 # ASSIGN : s_6_9 1089 # ASSIGN : s_7_0 431 # ASSIGN : s_7_1 548 # ASSIGN : s_7_2 638 # ASSIGN : s_7_3 736 # ASSIGN : s_7_4 767 # ASSIGN : s_7_5 860 # ASSIGN : s_7_6 898 # ASSIGN : s_7_7 970 # ASSIGN : s_7_8 985 # ASSIGN : s_7_9 1057 # ASSIGN : s_8_0 85 # ASSIGN : s_8_1 120 # ASSIGN : s_8_2 162 # ASSIGN : s_8_3 236 # ASSIGN : s_8_4 263 # ASSIGN : s_8_5 414 # ASSIGN : s_8_6 466 # ASSIGN : s_8_7 558 # ASSIGN : s_8_8 698 # ASSIGN : s_8_9 1026 # ASSIGN : s_9_0 237 # ASSIGN : s_9_1 338 # ASSIGN : s_9_2 491 # ASSIGN : s_9_3 579 # ASSIGN : s_9_4 750 # ASSIGN : s_9_5 838 # ASSIGN : s_9_6 858 # ASSIGN : s_9_7 926 # ASSIGN : s_9_8 950 # ASSIGN : s_9_9 1003 # ASSIGN : s_10_0 23 # ASSIGN : s_10_1 128 # ASSIGN : s_10_2 226 # ASSIGN : s_10_3 261 # ASSIGN : s_10_4 287 # ASSIGN : s_10_5 305 # ASSIGN : s_10_6 343 # ASSIGN : s_10_7 367 # ASSIGN : s_10_8 921 # ASSIGN : s_10_9 1097 # ASSIGN : s_11_0 0 # ASSIGN : s_11_1 68 # ASSIGN : s_11_2 129 # ASSIGN : s_11_3 206 # ASSIGN : s_11_4 220 # ASSIGN : s_11_5 280 # ASSIGN : s_11_6 295 # ASSIGN : s_11_7 370 # ASSIGN : s_11_8 433 # ASSIGN : s_11_9 932 # ASSIGN : s_12_0 402 # ASSIGN : s_12_1 481 # ASSIGN : s_12_2 541 # ASSIGN : s_12_3 597 # ASSIGN : s_12_4 688 # ASSIGN : s_12_5 728 # ASSIGN : s_12_6 814 # ASSIGN : s_12_7 886 # ASSIGN : s_12_8 966 # ASSIGN : s_12_9 1055 # ASSIGN : s_13_0 9 # ASSIGN : s_13_1 19 # ASSIGN : s_13_2 111 # ASSIGN : s_13_3 134 # ASSIGN : s_13_4 180 # ASSIGN : s_13_5 310 # ASSIGN : s_13_6 382 # ASSIGN : s_13_7 388 # ASSIGN : s_13_8 445 # ASSIGN : s_13_9 548 # ASSIGN : s_14_0 529 # ASSIGN : s_14_1 553 # ASSIGN : s_14_2 582 # ASSIGN : s_14_3 631 # ASSIGN : s_14_4 686 # ASSIGN : s_14_5 733 # ASSIGN : s_14_6 810 # ASSIGN : s_14_7 887 # ASSIGN : s_14_8 979 # ASSIGN : s_14_9 1007 SHOW_RESULT 1106 END : 1106 (1 seconds) [Thu Jun 1 16:55:17 2006] SHOW_RESULT 1106 CPU : 0.569999999999993 = 0.569999999999993 + 0 + 0 + 0 # BOUND : makespan 857 1106 MODIFY_CNF 981 BEGIN : [Thu Jun 1 16:55:17 2006] MODIFY_CNF 981 END : 73284018 bytes (0 seconds) [Thu Jun 1 16:55:17 2006] MODIFY_CNF 981 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 981 BEGIN : [Thu Jun 1 16:55:17 2006] CMD : minisat /work/tamura/csp2sat62102.cnf /work/tamura/csp2sat62102.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1242638 3656838 | 414212 0 0 NaNQ | 0.000 % | | 100 | 1242638 3656838 | 455633 100 1040 10.4 | 65.171 % | | 253 | 1242638 3656838 | 501196 253 4349 17.2 | 65.171 % | | 478 | 1242638 3656838 | 551316 478 7983 16.7 | 65.171 % | | 816 | 1242638 3656838 | 606447 816 14007 17.2 | 65.171 % | ==============================================================================) restarts : 5 conflicts : 944 (120 /sec) decisions : 1875 (239 /sec) propagations : 7525669 (958056 /sec) inspects : 76248384 (9706807 /sec) conflict literals : 16264 (24.72 % deleted) CPU time : 7.85515 s SATISFIABLE VERIFY_CNF 981 END : (9 seconds) [Thu Jun 1 16:55:26 2006] VERIFY_CNF 981 CPU : 8.95999999999999 = 0.00999999999999091 + 0.01 + 8.67 + 0.27 # RESULT : makespan 981 SATISFIABLE SHOW_RESULT 981 BEGIN : [Thu Jun 1 16:55:26 2006] # ASSIGN : makespan 981 # ASSIGN : s_0_0 5 # ASSIGN : s_0_1 162 # ASSIGN : s_0_2 237 # ASSIGN : s_0_3 309 # ASSIGN : s_0_4 527 # ASSIGN : s_0_5 659 # ASSIGN : s_0_6 702 # ASSIGN : s_0_7 740 # ASSIGN : s_0_8 892 # ASSIGN : s_0_9 918 # ASSIGN : s_1_0 65 # ASSIGN : s_1_1 366 # ASSIGN : s_1_2 476 # ASSIGN : s_1_3 519 # ASSIGN : s_1_4 579 # ASSIGN : s_1_5 664 # ASSIGN : s_1_6 703 # ASSIGN : s_1_7 739 # ASSIGN : s_1_8 802 # ASSIGN : s_1_9 869 # ASSIGN : s_2_0 19 # ASSIGN : s_2_1 69 # ASSIGN : s_2_2 230 # ASSIGN : s_2_3 310 # ASSIGN : s_2_4 317 # ASSIGN : s_2_5 573 # ASSIGN : s_2_6 667 # ASSIGN : s_2_7 774 # ASSIGN : s_2_8 846 # ASSIGN : s_2_9 935 # ASSIGN : s_3_0 173 # ASSIGN : s_3_1 264 # ASSIGN : s_3_2 358 # ASSIGN : s_3_3 457 # ASSIGN : s_3_4 517 # ASSIGN : s_3_5 585 # ASSIGN : s_3_6 728 # ASSIGN : s_3_7 739 # ASSIGN : s_3_8 835 # ASSIGN : s_3_9 900 # ASSIGN : s_4_0 13 # ASSIGN : s_4_1 121 # ASSIGN : s_4_2 166 # ASSIGN : s_4_3 223 # ASSIGN : s_4_4 241 # ASSIGN : s_4_5 383 # ASSIGN : s_4_6 528 # ASSIGN : s_4_7 542 # ASSIGN : s_4_8 765 # ASSIGN : s_4_9 834 # ASSIGN : s_5_0 106 # ASSIGN : s_5_1 188 # ASSIGN : s_5_2 251 # ASSIGN : s_5_3 445 # ASSIGN : s_5_4 532 # ASSIGN : s_5_5 682 # ASSIGN : s_5_6 770 # ASSIGN : s_5_7 887 # ASSIGN : s_5_8 937 # ASSIGN : s_5_9 972 # ASSIGN : s_6_0 84 # ASSIGN : s_6_1 155 # ASSIGN : s_6_2 246 # ASSIGN : s_6_3 311 # ASSIGN : s_6_4 434 # ASSIGN : s_6_5 613 # ASSIGN : s_6_6 621 # ASSIGN : s_6_7 852 # ASSIGN : s_6_8 927 # ASSIGN : s_6_9 964 # ASSIGN : s_7_0 35 # ASSIGN : s_7_1 97 # ASSIGN : s_7_2 337 # ASSIGN : s_7_3 435 # ASSIGN : s_7_4 466 # ASSIGN : s_7_5 557 # ASSIGN : s_7_6 595 # ASSIGN : s_7_7 667 # ASSIGN : s_7_8 676 # ASSIGN : s_7_9 932 # ASSIGN : s_8_0 14 # ASSIGN : s_8_1 49 # ASSIGN : s_8_2 88 # ASSIGN : s_8_3 162 # ASSIGN : s_8_4 187 # ASSIGN : s_8_5 234 # ASSIGN : s_8_6 286 # ASSIGN : s_8_7 703 # ASSIGN : s_8_8 724 # ASSIGN : s_8_9 812 # ASSIGN : s_9_0 314 # ASSIGN : s_9_1 372 # ASSIGN : s_9_2 385 # ASSIGN : s_9_3 439 # ASSIGN : s_9_4 491 # ASSIGN : s_9_5 614 # ASSIGN : s_9_6 634 # ASSIGN : s_9_7 716 # ASSIGN : s_9_8 781 # ASSIGN : s_9_9 878 # ASSIGN : s_10_0 441 # ASSIGN : s_10_1 540 # ASSIGN : s_10_2 631 # ASSIGN : s_10_3 684 # ASSIGN : s_10_4 741 # ASSIGN : s_10_5 759 # ASSIGN : s_10_6 828 # ASSIGN : s_10_7 888 # ASSIGN : s_10_8 923 # ASSIGN : s_10_9 972 # ASSIGN : s_11_0 120 # ASSIGN : s_11_1 289 # ASSIGN : s_11_2 349 # ASSIGN : s_11_3 431 # ASSIGN : s_11_4 513 # ASSIGN : s_11_5 652 # ASSIGN : s_11_6 667 # ASSIGN : s_11_7 779 # ASSIGN : s_11_8 797 # ASSIGN : s_11_9 912 # ASSIGN : s_12_0 9 # ASSIGN : s_12_1 102 # ASSIGN : s_12_2 162 # ASSIGN : s_12_3 218 # ASSIGN : s_12_4 426 # ASSIGN : s_12_5 573 # ASSIGN : s_12_6 671 # ASSIGN : s_12_7 748 # ASSIGN : s_12_8 838 # ASSIGN : s_12_9 930 # ASSIGN : s_13_0 4 # ASSIGN : s_13_1 29 # ASSIGN : s_13_2 137 # ASSIGN : s_13_3 160 # ASSIGN : s_13_4 206 # ASSIGN : s_13_5 307 # ASSIGN : s_13_6 379 # ASSIGN : s_13_7 401 # ASSIGN : s_13_8 424 # ASSIGN : s_13_9 947 # ASSIGN : s_14_0 5 # ASSIGN : s_14_1 194 # ASSIGN : s_14_2 262 # ASSIGN : s_14_3 311 # ASSIGN : s_14_4 377 # ASSIGN : s_14_5 537 # ASSIGN : s_14_6 662 # ASSIGN : s_14_7 743 # ASSIGN : s_14_8 751 # ASSIGN : s_14_9 864 SHOW_RESULT 981 END : 981 (0 seconds) [Thu Jun 1 16:55:26 2006] SHOW_RESULT 981 CPU : 0.570000000000002 = 0.560000000000002 + 0.01 + 0 + 0 # BOUND : makespan 857 981 MODIFY_CNF 919 BEGIN : [Thu Jun 1 16:55:26 2006] MODIFY_CNF 919 END : 73284017 bytes (0 seconds) [Thu Jun 1 16:55:26 2006] MODIFY_CNF 919 CPU : 0.0100000000000193 = 0.0100000000000193 + 0 + 0 + 0 VERIFY_CNF 919 BEGIN : [Thu Jun 1 16:55:26 2006] CMD : minisat /work/tamura/csp2sat62102.cnf /work/tamura/csp2sat62102.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1064356 3131447 | 354785 0 0 NaNQ | 0.000 % | | 100 | 1064356 3131447 | 390263 99 741 7.5 | 69.768 % | | 250 | 1064356 3131447 | 429289 248 2451 9.9 | 69.769 % | | 475 | 1064356 3131447 | 472218 473 5845 12.4 | 69.769 % | | 812 | 1062866 3126979 | 519440 767 10537 13.7 | 69.769 % | | 1319 | 1058743 3114760 | 571384 1128 15900 14.1 | 69.844 % | | 2078 | 1058743 3114760 | 628523 1887 28647 15.2 | 69.844 % | | 3217 | 1053329 3098705 | 691375 2916 49337 16.9 | 69.936 % | | 4926 | 1013192 2979784 | 760513 4477 76002 17.0 | 70.663 % | ==============================================================================) restarts : 9 conflicts : 7273 (229 /sec) decisions : 10502 (330 /sec) propagations : 56012683 (1760171 /sec) inspects : 514359736 (16163503 /sec) conflict literals : 130695 (35.38 % deleted) CPU time : 31.8223 s UNSATISFIABLE VERIFY_CNF 919 END : (33 seconds) [Thu Jun 1 16:55:59 2006] VERIFY_CNF 919 CPU : 32.7 = 0 + 0.01 + 32.43 + 0.26 # RESULT : makespan 919 UNSATISFIABLE # BOUND : makespan 920 981 MODIFY_CNF 950 BEGIN : [Thu Jun 1 16:55:59 2006] MODIFY_CNF 950 END : 73284017 bytes (0 seconds) [Thu Jun 1 16:55:59 2006] MODIFY_CNF 950 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 950 BEGIN : [Thu Jun 1 16:55:59 2006] CMD : minisat /work/tamura/csp2sat62102.cnf /work/tamura/csp2sat62102.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1153094 3392934 | 384364 0 0 NaNQ | 0.000 % | | 102 | 1153094 3392934 | 422800 102 954 9.4 | 67.468 % | | 252 | 1153094 3392934 | 465080 252 3677 14.6 | 67.468 % | | 477 | 1153094 3392934 | 511588 477 5710 12.0 | 67.468 % | | 814 | 1153094 3392934 | 562747 814 12127 14.9 | 67.468 % | | 1320 | 1153094 3392934 | 619022 1320 17967 13.6 | 67.468 % | ==============================================================================) restarts : 6 conflicts : 1578 (169 /sec) decisions : 2842 (305 /sec) propagations : 10826236 (1160117 /sec) inspects : 103693817 (11111611 /sec) conflict literals : 22821 (24.80 % deleted) CPU time : 9.33202 s SATISFIABLE VERIFY_CNF 950 END : (11 seconds) [Thu Jun 1 16:56:10 2006] VERIFY_CNF 950 CPU : 10.18 = 0 + 0.01 + 10.09 + 0.0800000000000001 # RESULT : makespan 950 SATISFIABLE SHOW_RESULT 950 BEGIN : [Thu Jun 1 16:56:10 2006] # ASSIGN : makespan 950 # ASSIGN : s_0_0 7 # ASSIGN : s_0_1 15 # ASSIGN : s_0_2 110 # ASSIGN : s_0_3 182 # ASSIGN : s_0_4 471 # ASSIGN : s_0_5 517 # ASSIGN : s_0_6 641 # ASSIGN : s_0_7 679 # ASSIGN : s_0_8 777 # ASSIGN : s_0_9 887 # ASSIGN : s_1_0 44 # ASSIGN : s_1_1 63 # ASSIGN : s_1_2 177 # ASSIGN : s_1_3 241 # ASSIGN : s_1_4 489 # ASSIGN : s_1_5 581 # ASSIGN : s_1_6 620 # ASSIGN : s_1_7 633 # ASSIGN : s_1_8 771 # ASSIGN : s_1_9 838 # ASSIGN : s_2_0 34 # ASSIGN : s_2_1 84 # ASSIGN : s_2_2 183 # ASSIGN : s_2_3 263 # ASSIGN : s_2_4 313 # ASSIGN : s_2_5 368 # ASSIGN : s_2_6 520 # ASSIGN : s_2_7 667 # ASSIGN : s_2_8 804 # ASSIGN : s_2_9 847 # ASSIGN : s_3_0 115 # ASSIGN : s_3_1 215 # ASSIGN : s_3_2 270 # ASSIGN : s_3_3 369 # ASSIGN : s_3_4 552 # ASSIGN : s_3_5 634 # ASSIGN : s_3_6 739 # ASSIGN : s_3_7 750 # ASSIGN : s_3_8 846 # ASSIGN : s_3_9 869 # ASSIGN : s_4_0 18 # ASSIGN : s_4_1 102 # ASSIGN : s_4_2 136 # ASSIGN : s_4_3 176 # ASSIGN : s_4_4 183 # ASSIGN : s_4_5 256 # ASSIGN : s_4_6 330 # ASSIGN : s_4_7 374 # ASSIGN : s_4_8 564 # ASSIGN : s_4_9 750 # ASSIGN : s_5_0 185 # ASSIGN : s_5_1 264 # ASSIGN : s_5_2 370 # ASSIGN : s_5_3 429 # ASSIGN : s_5_4 501 # ASSIGN : s_5_5 662 # ASSIGN : s_5_6 739 # ASSIGN : s_5_7 856 # ASSIGN : s_5_8 906 # ASSIGN : s_5_9 941 # ASSIGN : s_6_0 65 # ASSIGN : s_6_1 154 # ASSIGN : s_6_2 245 # ASSIGN : s_6_3 313 # ASSIGN : s_6_4 403 # ASSIGN : s_6_5 501 # ASSIGN : s_6_6 509 # ASSIGN : s_6_7 559 # ASSIGN : s_6_8 896 # ASSIGN : s_6_9 933 # ASSIGN : s_7_0 1 # ASSIGN : s_7_1 125 # ASSIGN : s_7_2 300 # ASSIGN : s_7_3 398 # ASSIGN : s_7_4 429 # ASSIGN : s_7_5 693 # ASSIGN : s_7_6 731 # ASSIGN : s_7_7 803 # ASSIGN : s_7_8 829 # ASSIGN : s_7_9 901 # ASSIGN : s_8_0 153 # ASSIGN : s_8_1 188 # ASSIGN : s_8_2 227 # ASSIGN : s_8_3 404 # ASSIGN : s_8_4 462 # ASSIGN : s_8_5 526 # ASSIGN : s_8_6 578 # ASSIGN : s_8_7 646 # ASSIGN : s_8_8 693 # ASSIGN : s_8_9 812 # ASSIGN : s_9_0 90 # ASSIGN : s_9_1 236 # ASSIGN : s_9_2 280 # ASSIGN : s_9_3 405 # ASSIGN : s_9_4 574 # ASSIGN : s_9_5 673 # ASSIGN : s_9_6 703 # ASSIGN : s_9_7 783 # ASSIGN : s_9_8 828 # ASSIGN : s_9_9 893 # ASSIGN : s_10_0 258 # ASSIGN : s_10_1 435 # ASSIGN : s_10_2 627 # ASSIGN : s_10_3 660 # ASSIGN : s_10_4 685 # ASSIGN : s_10_5 728 # ASSIGN : s_10_6 805 # ASSIGN : s_10_7 857 # ASSIGN : s_10_8 892 # ASSIGN : s_10_9 941 # ASSIGN : s_11_0 42 # ASSIGN : s_11_1 220 # ASSIGN : s_11_2 291 # ASSIGN : s_11_3 447 # ASSIGN : s_11_4 457 # ASSIGN : s_11_5 537 # ASSIGN : s_11_6 659 # ASSIGN : s_11_7 731 # ASSIGN : s_11_8 766 # ASSIGN : s_11_9 881 # ASSIGN : s_12_0 148 # ASSIGN : s_12_1 253 # ASSIGN : s_12_2 342 # ASSIGN : s_12_3 429 # ASSIGN : s_12_4 520 # ASSIGN : s_12_5 560 # ASSIGN : s_12_6 653 # ASSIGN : s_12_7 725 # ASSIGN : s_12_8 807 # ASSIGN : s_12_9 899 # ASSIGN : s_13_0 0 # ASSIGN : s_13_1 10 # ASSIGN : s_13_2 113 # ASSIGN : s_13_3 136 # ASSIGN : s_13_4 310 # ASSIGN : s_13_5 357 # ASSIGN : s_13_6 429 # ASSIGN : s_13_7 441 # ASSIGN : s_13_8 464 # ASSIGN : s_13_9 916 # ASSIGN : s_14_0 247 # ASSIGN : s_14_1 271 # ASSIGN : s_14_2 301 # ASSIGN : s_14_3 350 # ASSIGN : s_14_4 417 # ASSIGN : s_14_5 577 # ASSIGN : s_14_6 654 # ASSIGN : s_14_7 731 # ASSIGN : s_14_8 749 # ASSIGN : s_14_9 780 SHOW_RESULT 950 END : 950 (0 seconds) [Thu Jun 1 16:56:10 2006] SHOW_RESULT 950 CPU : 0.599999999999994 = 0.599999999999994 + 0 + 0 + 0 # BOUND : makespan 920 950 MODIFY_CNF 935 BEGIN : [Thu Jun 1 16:56:10 2006] MODIFY_CNF 935 END : 73284017 bytes (0 seconds) [Thu Jun 1 16:56:10 2006] MODIFY_CNF 935 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 935 BEGIN : [Thu Jun 1 16:56:10 2006] CMD : minisat /work/tamura/csp2sat62102.cnf /work/tamura/csp2sat62102.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1109155 3263406 | 369718 0 0 NaNQ | 0.000 % | | 101 | 1109155 3263406 | 406689 101 965 9.6 | 68.581 % | | 251 | 1109155 3263406 | 447358 251 3369 13.4 | 68.581 % | | 476 | 1109155 3263406 | 492094 476 7134 15.0 | 68.581 % | | 814 | 1109155 3263406 | 541304 814 11481 14.1 | 68.581 % | | 1323 | 1109155 3263406 | 595434 1323 24036 18.2 | 68.581 % | | 2083 | 1109155 3263406 | 654977 2083 42139 20.2 | 68.581 % | | 3224 | 1109155 3263406 | 720475 3224 68999 21.4 | 68.581 % | | 4934 | 1109155 3263406 | 792523 4934 107274 21.7 | 68.581 % | | 7496 | 1109155 3263406 | 871775 7496 156310 20.9 | 68.581 % | | 11340 | 1109155 3263406 | 958953 11340 242331 21.4 | 68.581 % | | 17106 | 1109155 3263406 | 1054848 17106 383686 22.4 | 68.581 % | | 25757 | 1099078 3233570 | 1160333 22530 511257 22.7 | 68.775 % | ==============================================================================) restarts : 13 conflicts : 34815 (244 /sec) decisions : 50187 (351 /sec) propagations : 253546170 (1775107 /sec) inspects : 2564222963 (17952430 /sec) conflict literals : 823074 (38.08 % deleted) CPU time : 142.834 s SATISFIABLE VERIFY_CNF 935 END : (144 seconds) [Thu Jun 1 16:58:34 2006] VERIFY_CNF 935 CPU : 143.66 = 0 + 0.01 + 143.57 + 0.08 # RESULT : makespan 935 SATISFIABLE SHOW_RESULT 935 BEGIN : [Thu Jun 1 16:58:34 2006] # ASSIGN : makespan 935 # ASSIGN : s_0_0 88 # ASSIGN : s_0_1 96 # ASSIGN : s_0_2 171 # ASSIGN : s_0_3 299 # ASSIGN : s_0_4 486 # ASSIGN : s_0_5 539 # ASSIGN : s_0_6 586 # ASSIGN : s_0_7 657 # ASSIGN : s_0_8 762 # ASSIGN : s_0_9 872 # ASSIGN : s_1_0 107 # ASSIGN : s_1_1 126 # ASSIGN : s_1_2 200 # ASSIGN : s_1_3 243 # ASSIGN : s_1_4 266 # ASSIGN : s_1_5 447 # ASSIGN : s_1_6 536 # ASSIGN : s_1_7 562 # ASSIGN : s_1_8 756 # ASSIGN : s_1_9 823 # ASSIGN : s_2_0 1 # ASSIGN : s_2_1 51 # ASSIGN : s_2_2 151 # ASSIGN : s_2_3 267 # ASSIGN : s_2_4 284 # ASSIGN : s_2_5 339 # ASSIGN : s_2_6 449 # ASSIGN : s_2_7 775 # ASSIGN : s_2_8 847 # ASSIGN : s_2_9 889 # ASSIGN : s_3_0 143 # ASSIGN : s_3_1 211 # ASSIGN : s_3_2 274 # ASSIGN : s_3_3 373 # ASSIGN : s_3_4 433 # ASSIGN : s_3_5 501 # ASSIGN : s_3_6 729 # ASSIGN : s_3_7 740 # ASSIGN : s_3_8 836 # ASSIGN : s_3_9 854 # ASSIGN : s_4_0 4 # ASSIGN : s_4_1 265 # ASSIGN : s_4_2 361 # ASSIGN : s_4_3 426 # ASSIGN : s_4_4 476 # ASSIGN : s_4_5 583 # ASSIGN : s_4_6 660 # ASSIGN : s_4_7 672 # ASSIGN : s_4_8 732 # ASSIGN : s_4_9 836 # ASSIGN : s_5_0 62 # ASSIGN : s_5_1 122 # ASSIGN : s_5_2 208 # ASSIGN : s_5_3 329 # ASSIGN : s_5_4 401 # ASSIGN : s_5_5 634 # ASSIGN : s_5_6 724 # ASSIGN : s_5_7 841 # ASSIGN : s_5_8 891 # ASSIGN : s_5_9 926 # ASSIGN : s_6_0 36 # ASSIGN : s_6_1 148 # ASSIGN : s_6_2 239 # ASSIGN : s_6_3 374 # ASSIGN : s_6_4 464 # ASSIGN : s_6_5 666 # ASSIGN : s_6_6 674 # ASSIGN : s_6_7 739 # ASSIGN : s_6_8 881 # ASSIGN : s_6_9 918 # ASSIGN : s_7_0 0 # ASSIGN : s_7_1 121 # ASSIGN : s_7_2 231 # ASSIGN : s_7_3 344 # ASSIGN : s_7_4 400 # ASSIGN : s_7_5 550 # ASSIGN : s_7_6 588 # ASSIGN : s_7_7 788 # ASSIGN : s_7_8 814 # ASSIGN : s_7_9 886 # ASSIGN : s_8_0 48 # ASSIGN : s_8_1 83 # ASSIGN : s_8_2 222 # ASSIGN : s_8_3 401 # ASSIGN : s_8_4 453 # ASSIGN : s_8_5 531 # ASSIGN : s_8_6 624 # ASSIGN : s_8_7 695 # ASSIGN : s_8_8 716 # ASSIGN : s_8_9 797 # ASSIGN : s_9_0 296 # ASSIGN : s_9_1 354 # ASSIGN : s_9_2 375 # ASSIGN : s_9_3 487 # ASSIGN : s_9_4 546 # ASSIGN : s_9_5 657 # ASSIGN : s_9_6 687 # ASSIGN : s_9_7 755 # ASSIGN : s_9_8 779 # ASSIGN : s_9_9 832 # ASSIGN : s_10_0 326 # ASSIGN : s_10_1 425 # ASSIGN : s_10_2 516 # ASSIGN : s_10_3 549 # ASSIGN : s_10_4 568 # ASSIGN : s_10_5 677 # ASSIGN : s_10_6 715 # ASSIGN : s_10_7 801 # ASSIGN : s_10_8 877 # ASSIGN : s_10_9 926 # ASSIGN : s_11_0 15 # ASSIGN : s_11_1 278 # ASSIGN : s_11_2 491 # ASSIGN : s_11_3 572 # ASSIGN : s_11_4 582 # ASSIGN : s_11_5 642 # ASSIGN : s_11_6 660 # ASSIGN : s_11_7 733 # ASSIGN : s_11_8 751 # ASSIGN : s_11_9 866 # ASSIGN : s_12_0 4 # ASSIGN : s_12_1 83 # ASSIGN : s_12_2 144 # ASSIGN : s_12_3 208 # ASSIGN : s_12_4 299 # ASSIGN : s_12_5 401 # ASSIGN : s_12_6 500 # ASSIGN : s_12_7 592 # ASSIGN : s_12_8 792 # ASSIGN : s_12_9 884 # ASSIGN : s_13_0 26 # ASSIGN : s_13_1 36 # ASSIGN : s_13_2 128 # ASSIGN : s_13_3 153 # ASSIGN : s_13_4 199 # ASSIGN : s_13_5 254 # ASSIGN : s_13_6 338 # ASSIGN : s_13_7 351 # ASSIGN : s_13_8 406 # ASSIGN : s_13_9 901 # ASSIGN : s_14_0 12 # ASSIGN : s_14_1 99 # ASSIGN : s_14_2 173 # ASSIGN : s_14_3 304 # ASSIGN : s_14_4 359 # ASSIGN : s_14_5 506 # ASSIGN : s_14_6 583 # ASSIGN : s_14_7 666 # ASSIGN : s_14_8 703 # ASSIGN : s_14_9 731 SHOW_RESULT 935 END : 935 (1 seconds) [Thu Jun 1 16:58:35 2006] SHOW_RESULT 935 CPU : 0.589999999999984 = 0.579999999999984 + 0.00999999999999995 + 0 + 0 # BOUND : makespan 920 935 MODIFY_CNF 927 BEGIN : [Thu Jun 1 16:58:35 2006] MODIFY_CNF 927 END : 73284017 bytes (0 seconds) [Thu Jun 1 16:58:35 2006] MODIFY_CNF 927 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 927 BEGIN : [Thu Jun 1 16:58:35 2006] CMD : minisat /work/tamura/csp2sat62102.cnf /work/tamura/csp2sat62102.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1084241 3189888 | 361413 0 0 NaNQ | 0.000 % | | 100 | 1084241 3189888 | 397554 100 908 9.1 | 69.177 % | | 251 | 1084241 3189888 | 437309 251 2376 9.5 | 69.177 % | | 476 | 1084241 3189888 | 481040 476 5232 11.0 | 69.177 % | | 814 | 1083593 3187946 | 529144 813 11045 13.6 | 69.178 % | | 1320 | 1083593 3187946 | 582059 1319 19602 14.9 | 69.178 % | | 2079 | 1083593 3187946 | 640265 2078 33132 15.9 | 69.178 % | | 3218 | 1083593 3187946 | 704291 3217 54060 16.8 | 69.178 % | | 4926 | 1083593 3187946 | 774720 4925 82693 16.8 | 69.178 % | | 7489 | 1083593 3187946 | 852192 7488 150097 20.0 | 69.178 % | | 11335 | 1083593 3187946 | 937412 11334 261659 23.1 | 69.178 % | | 17102 | 1070976 3150547 | 1031153 16023 409259 25.5 | 69.401 % | ==============================================================================) restarts : 12 conflicts : 21180 (249 /sec) decisions : 29907 (352 /sec) propagations : 154475908 (1818870 /sec) inspects : 1495242864 (17605671 /sec) conflict literals : 538189 (36.81 % deleted) CPU time : 84.9296 s UNSATISFIABLE VERIFY_CNF 927 END : (86 seconds) [Thu Jun 1 17:00:01 2006] VERIFY_CNF 927 CPU : 85.88 = 0.0100000000000193 + 0.01 + 85.6 + 0.26 # RESULT : makespan 927 UNSATISFIABLE # BOUND : makespan 928 935 MODIFY_CNF 931 BEGIN : [Thu Jun 1 17:00:01 2006] MODIFY_CNF 931 END : 73284017 bytes (0 seconds) [Thu Jun 1 17:00:01 2006] MODIFY_CNF 931 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 931 BEGIN : [Thu Jun 1 17:00:01 2006] CMD : minisat /work/tamura/csp2sat62102.cnf /work/tamura/csp2sat62102.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1097973 3230471 | 365991 0 0 NaNQ | 0.000 % | | 101 | 1097973 3230471 | 402590 101 936 9.3 | 68.878 % | | 251 | 1097973 3230471 | 442849 250 2077 8.3 | 68.879 % | | 476 | 1097973 3230471 | 487134 475 5523 11.6 | 68.879 % | | 813 | 1097338 3228567 | 535847 792 9522 12.0 | 68.927 % | | 1319 | 1097338 3228567 | 589432 1298 15989 12.3 | 68.927 % | | 2078 | 1095898 3224347 | 648375 2056 27698 13.5 | 68.927 % | | 3217 | 1095898 3224347 | 713212 3195 48676 15.2 | 68.927 % | | 4925 | 1095898 3224347 | 784534 4903 77950 15.9 | 68.927 % | | 7489 | 1084661 3191084 | 862987 6640 112214 16.9 | 69.147 % | | 11333 | 1084661 3191084 | 949286 10484 182625 17.4 | 69.147 % | | 17100 | 1084009 3189130 | 1044215 16249 321244 19.8 | 69.148 % | | 25749 | 1004215 2952378 | 1148636 16836 300274 17.8 | 70.437 % | ==============================================================================) restarts : 13 conflicts : 28952 (251 /sec) decisions : 40598 (352 /sec) propagations : 215010258 (1863643 /sec) inspects : 2028965643 (17586456 /sec) conflict literals : 575434 (39.56 % deleted) CPU time : 115.371 s UNSATISFIABLE VERIFY_CNF 931 END : (116 seconds) [Thu Jun 1 17:01:57 2006] VERIFY_CNF 931 CPU : 116.05 = 0 + 0.01 + 115.96 + 0.0800000000000001 # RESULT : makespan 931 UNSATISFIABLE # BOUND : makespan 932 935 MODIFY_CNF 933 BEGIN : [Thu Jun 1 17:01:57 2006] MODIFY_CNF 933 END : 73284017 bytes (0 seconds) [Thu Jun 1 17:01:57 2006] MODIFY_CNF 933 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 933 BEGIN : [Thu Jun 1 17:01:57 2006] CMD : minisat /work/tamura/csp2sat62102.cnf /work/tamura/csp2sat62102.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1102025 3242325 | 367341 0 0 NaNQ | 0.000 % | | 101 | 1102025 3242325 | 404075 101 1004 9.9 | 68.732 % | | 251 | 1102025 3242325 | 444482 251 2064 8.2 | 68.732 % | | 477 | 1102025 3242325 | 488930 477 5883 12.3 | 68.732 % | | 815 | 1102025 3242325 | 537823 815 10892 13.4 | 68.732 % | | 1322 | 1102025 3242325 | 591606 1322 16539 12.5 | 68.732 % | | 2083 | 1102025 3242325 | 650766 2083 28765 13.8 | 68.732 % | | 3222 | 1102025 3242325 | 715843 3222 49607 15.4 | 68.732 % | | 4931 | 1102025 3242325 | 787428 4931 89022 18.1 | 68.732 % | | 7493 | 1102025 3242325 | 866170 7493 141496 18.9 | 68.732 % | | 11337 | 1098438 3231713 | 952787 10366 200059 19.3 | 68.805 % | | 17103 | 1098438 3231713 | 1048066 16132 350745 21.7 | 68.805 % | | 25752 | 1090726 3208766 | 1152873 23391 525781 22.5 | 68.900 % | ==============================================================================) restarts : 13 conflicts : 35001 (252 /sec) decisions : 48786 (351 /sec) propagations : 253503416 (1823172 /sec) inspects : 2485998778 (17879057 /sec) conflict literals : 792680 (38.85 % deleted) CPU time : 139.045 s UNSATISFIABLE VERIFY_CNF 933 END : (140 seconds) [Thu Jun 1 17:04:17 2006] VERIFY_CNF 933 CPU : 139.73 = 0 + 0.01 + 139.65 + 0.0699999999999998 # RESULT : makespan 933 UNSATISFIABLE # BOUND : makespan 934 935 MODIFY_CNF 934 BEGIN : [Thu Jun 1 17:04:17 2006] MODIFY_CNF 934 END : 73284017 bytes (0 seconds) [Thu Jun 1 17:04:17 2006] MODIFY_CNF 934 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 934 BEGIN : [Thu Jun 1 17:04:17 2006] CMD : minisat /work/tamura/csp2sat62102.cnf /work/tamura/csp2sat62102.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1106407 3255315 | 368802 0 0 NaNQ | 0.000 % | | 100 | 1106407 3255315 | 405682 100 1143 11.4 | 68.656 % | | 250 | 1106407 3255315 | 446250 250 3326 13.3 | 68.656 % | | 475 | 1106407 3255315 | 490875 475 6802 14.3 | 68.656 % | | 812 | 1106407 3255315 | 539963 812 10946 13.5 | 68.656 % | | 1318 | 1106407 3255315 | 593959 1318 18764 14.2 | 68.656 % | | 2077 | 1106407 3255315 | 653355 2077 26048 12.5 | 68.656 % | | 3216 | 1105859 3253672 | 718690 3173 45199 14.2 | 68.656 % | | 4924 | 1105859 3253672 | 790559 4881 70561 14.5 | 68.656 % | | 7486 | 1105859 3253672 | 869615 7443 122144 16.4 | 68.656 % | | 11330 | 1105859 3253672 | 956577 11287 189740 16.8 | 68.657 % | | 17096 | 1096216 3225025 | 1052235 12258 211392 17.2 | 68.797 % | | 25745 | 1096216 3225025 | 1157458 20907 420295 20.1 | 68.797 % | ==============================================================================) restarts : 13 conflicts : 37983 (260 /sec) decisions : 52526 (360 /sec) propagations : 269261990 (1846104 /sec) inspects : 2593775117 (17783344 /sec) conflict literals : 796330 (40.71 % deleted) CPU time : 145.854 s UNSATISFIABLE VERIFY_CNF 934 END : (147 seconds) [Thu Jun 1 17:06:44 2006] VERIFY_CNF 934 CPU : 146.6 = 0 + 0.01 + 146.51 + 0.0800000000000001 # RESULT : makespan 934 UNSATISFIABLE # BOUND : makespan 935 935 MAIN END : (849 seconds) [Thu Jun 1 17:06:44 2006] MAIN CPU : 847.16 = 158.52 + 0.33 + 687.07 + 1.24