MAIN BEGIN : [Thu Jun 1 15:37:46 2006] READ BEGIN : csp/la10.csp [Thu Jun 1 15:37:46 2006] READ END : csp/la10.csp (2 seconds) [Thu Jun 1 15:37:48 2006] READ CPU : 1.53 = 1.53 + 0 + 0 + 0 # BOUND : makespan 958 1012 GENERATE_CNF 1012 BEGIN : [Thu Jun 1 15:37:48 2006] GENERATE_CNF 1012 END : 77231 variables 1143648 clauses 24290635 bytes (56 seconds) [Thu Jun 1 15:38:44 2006] GENERATE_CNF 1012 CPU : 55.73 = 55.66 + 0.07 + 0 + 0 MODIFY_CNF 985 BEGIN : [Thu Jun 1 15:38:44 2006] MODIFY_CNF 985 END : 24290640 bytes (0 seconds) [Thu Jun 1 15:38:44 2006] MODIFY_CNF 985 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 985 BEGIN : [Thu Jun 1 15:38:44 2006] CMD : minisat /work/tamura/csp2sat82106.cnf /work/tamura/csp2sat82106.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 908734 2671642 | 302911 0 0 NaNQ | 0.000 % | | 103 | 908734 2671642 | 333202 103 3037 29.5 | 28.977 % | ==============================================================================) restarts : 2 conflicts : 196 (148 /sec) decisions : 615 (465 /sec) propagations : 647038 (488924 /sec) inspects : 7548803 (5704137 /sec) conflict literals : 4346 (12.63 % deleted) CPU time : 1.32339 s SATISFIABLE VERIFY_CNF 985 END : (2 seconds) [Thu Jun 1 15:38:46 2006] VERIFY_CNF 985 CPU : 1.86 = 0.00999999999999801 + 0 + 1.83 + 0.02 # RESULT : makespan 985 SATISFIABLE SHOW_RESULT 985 BEGIN : [Thu Jun 1 15:38:46 2006] # ASSIGN : makespan 985 # ASSIGN : s_0_0 350 # ASSIGN : s_0_1 475 # ASSIGN : s_0_2 693 # ASSIGN : s_0_3 817 # ASSIGN : s_0_4 826 # ASSIGN : s_1_0 174 # ASSIGN : s_1_1 299 # ASSIGN : s_1_2 445 # ASSIGN : s_1_3 541 # ASSIGN : s_1_4 618 # ASSIGN : s_2_0 474 # ASSIGN : s_2_1 551 # ASSIGN : s_2_2 702 # ASSIGN : s_2_3 784 # ASSIGN : s_2_4 823 # ASSIGN : s_3_0 2 # ASSIGN : s_3_1 104 # ASSIGN : s_3_2 253 # ASSIGN : s_3_3 284 # ASSIGN : s_3_4 321 # ASSIGN : s_4_0 20 # ASSIGN : s_4_1 82 # ASSIGN : s_4_2 125 # ASSIGN : s_4_3 698 # ASSIGN : s_4_4 914 # ASSIGN : s_5_0 659 # ASSIGN : s_5_1 702 # ASSIGN : s_5_2 800 # ASSIGN : s_5_3 880 # ASSIGN : s_5_4 906 # ASSIGN : s_6_0 13 # ASSIGN : s_6_1 627 # ASSIGN : s_6_2 728 # ASSIGN : s_6_3 783 # ASSIGN : s_6_4 816 # ASSIGN : s_7_0 291 # ASSIGN : s_7_1 432 # ASSIGN : s_7_2 479 # ASSIGN : s_7_3 592 # ASSIGN : s_7_4 869 # ASSIGN : s_8_0 174 # ASSIGN : s_8_1 238 # ASSIGN : s_8_2 542 # ASSIGN : s_8_3 638 # ASSIGN : s_8_4 891 # ASSIGN : s_9_0 68 # ASSIGN : s_9_1 301 # ASSIGN : s_9_2 381 # ASSIGN : s_9_3 396 # ASSIGN : s_9_4 408 # ASSIGN : s_10_0 122 # ASSIGN : s_10_1 208 # ASSIGN : s_10_2 313 # ASSIGN : s_10_3 519 # ASSIGN : s_10_4 928 # ASSIGN : s_11_0 548 # ASSIGN : s_11_1 644 # ASSIGN : s_11_2 728 # ASSIGN : s_11_3 901 # ASSIGN : s_11_4 908 # ASSIGN : s_12_0 144 # ASSIGN : s_12_1 171 # ASSIGN : s_12_2 821 # ASSIGN : s_12_3 884 # ASSIGN : s_12_4 890 # ASSIGN : s_13_0 263 # ASSIGN : s_13_1 353 # ASSIGN : s_13_2 409 # ASSIGN : s_13_3 702 # ASSIGN : s_13_4 768 # ASSIGN : s_14_0 59 # ASSIGN : s_14_1 135 # ASSIGN : s_14_2 248 # ASSIGN : s_14_3 394 # ASSIGN : s_14_4 898 SHOW_RESULT 985 END : 985 (0 seconds) [Thu Jun 1 15:38:46 2006] SHOW_RESULT 985 CPU : 0.220000000000001 = 0.210000000000001 + 0.01 + 0 + 0 # BOUND : makespan 958 985 MODIFY_CNF 971 BEGIN : [Thu Jun 1 15:38:46 2006] MODIFY_CNF 971 END : 24290640 bytes (0 seconds) [Thu Jun 1 15:38:46 2006] MODIFY_CNF 971 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 971 BEGIN : [Thu Jun 1 15:38:46 2006] CMD : minisat /work/tamura/csp2sat82106.cnf /work/tamura/csp2sat82106.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 892970 2625414 | 297656 0 0 NaNQ | 0.000 % | ==============================================================================) restarts : 1 conflicts : 90 (78 /sec) decisions : 326 (281 /sec) propagations : 361273 (311579 /sec) inspects : 4142318 (3572534 /sec) conflict literals : 1061 (10.99 % deleted) CPU time : 1.15949 s SATISFIABLE VERIFY_CNF 971 END : (2 seconds) [Thu Jun 1 15:38:48 2006] VERIFY_CNF 971 CPU : 1.69000000000001 = 0.0100000000000051 + 0 + 1.65 + 0.03 # RESULT : makespan 971 SATISFIABLE SHOW_RESULT 971 BEGIN : [Thu Jun 1 15:38:48 2006] # ASSIGN : makespan 971 # ASSIGN : s_0_0 755 # ASSIGN : s_0_1 826 # ASSIGN : s_0_2 874 # ASSIGN : s_0_3 904 # ASSIGN : s_0_4 913 # ASSIGN : s_1_0 406 # ASSIGN : s_1_1 512 # ASSIGN : s_1_2 609 # ASSIGN : s_1_3 782 # ASSIGN : s_1_4 887 # ASSIGN : s_2_0 420 # ASSIGN : s_2_1 658 # ASSIGN : s_2_2 745 # ASSIGN : s_2_3 838 # ASSIGN : s_2_4 879 # ASSIGN : s_3_0 33 # ASSIGN : s_3_1 90 # ASSIGN : s_3_2 466 # ASSIGN : s_3_3 497 # ASSIGN : s_3_4 536 # ASSIGN : s_4_0 23 # ASSIGN : s_4_1 71 # ASSIGN : s_4_2 111 # ASSIGN : s_4_3 395 # ASSIGN : s_4_4 465 # ASSIGN : s_5_0 306 # ASSIGN : s_5_1 340 # ASSIGN : s_5_2 600 # ASSIGN : s_5_3 769 # ASSIGN : s_5_4 870 # ASSIGN : s_6_0 567 # ASSIGN : s_6_1 740 # ASSIGN : s_6_2 815 # ASSIGN : s_6_3 870 # ASSIGN : s_6_4 964 # ASSIGN : s_7_0 281 # ASSIGN : s_7_1 348 # ASSIGN : s_7_2 495 # ASSIGN : s_7_3 705 # ASSIGN : s_7_4 960 # ASSIGN : s_8_0 7 # ASSIGN : s_8_1 98 # ASSIGN : s_8_2 173 # ASSIGN : s_8_3 223 # ASSIGN : s_8_4 506 # ASSIGN : s_9_0 399 # ASSIGN : s_9_1 818 # ASSIGN : s_9_2 859 # ASSIGN : s_9_3 888 # ASSIGN : s_9_4 900 # ASSIGN : s_10_0 189 # ASSIGN : s_10_1 241 # ASSIGN : s_10_2 648 # ASSIGN : s_10_3 716 # ASSIGN : s_10_4 813 # ASSIGN : s_11_0 185 # ASSIGN : s_11_1 255 # ASSIGN : s_11_2 313 # ASSIGN : s_11_3 458 # ASSIGN : s_11_4 495 # ASSIGN : s_12_0 6 # ASSIGN : s_12_1 78 # ASSIGN : s_12_2 160 # ASSIGN : s_12_3 334 # ASSIGN : s_12_4 613 # ASSIGN : s_13_0 3 # ASSIGN : s_13_1 343 # ASSIGN : s_13_2 422 # ASSIGN : s_13_3 708 # ASSIGN : s_13_4 734 # ASSIGN : s_14_0 572 # ASSIGN : s_14_1 680 # ASSIGN : s_14_2 779 # ASSIGN : s_14_3 877 # ASSIGN : s_14_4 892 SHOW_RESULT 971 END : 971 (0 seconds) [Thu Jun 1 15:38:48 2006] SHOW_RESULT 971 CPU : 0.199999999999996 = 0.199999999999996 + 0 + 0 + 0 # BOUND : makespan 958 971 MODIFY_CNF 964 BEGIN : [Thu Jun 1 15:38:48 2006] MODIFY_CNF 964 END : 24290639 bytes (0 seconds) [Thu Jun 1 15:38:48 2006] MODIFY_CNF 964 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 964 BEGIN : [Thu Jun 1 15:38:48 2006] CMD : minisat /work/tamura/csp2sat82106.cnf /work/tamura/csp2sat82106.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 885088 2602300 | 295029 0 0 NaNQ | 0.000 % | | 100 | 885088 2602300 | 324531 100 1912 19.1 | 31.043 % | ==============================================================================) restarts : 2 conflicts : 114 (91 /sec) decisions : 419 (334 /sec) propagations : 471963 (376313 /sec) inspects : 5657638 (4511033 /sec) conflict literals : 2065 (6.48 % deleted) CPU time : 1.25418 s SATISFIABLE VERIFY_CNF 964 END : (2 seconds) [Thu Jun 1 15:38:50 2006] VERIFY_CNF 964 CPU : 1.87 = 0 + 0.01 + 1.77 + 0.09 # RESULT : makespan 964 SATISFIABLE SHOW_RESULT 964 BEGIN : [Thu Jun 1 15:38:50 2006] # ASSIGN : makespan 964 # ASSIGN : s_0_0 90 # ASSIGN : s_0_1 450 # ASSIGN : s_0_2 694 # ASSIGN : s_0_3 699 # ASSIGN : s_0_4 708 # ASSIGN : s_1_0 1 # ASSIGN : s_1_1 96 # ASSIGN : s_1_2 193 # ASSIGN : s_1_3 289 # ASSIGN : s_1_4 366 # ASSIGN : s_2_0 237 # ASSIGN : s_2_1 350 # ASSIGN : s_2_2 588 # ASSIGN : s_2_3 669 # ASSIGN : s_2_4 747 # ASSIGN : s_3_0 156 # ASSIGN : s_3_1 530 # ASSIGN : s_3_2 805 # ASSIGN : s_3_3 836 # ASSIGN : s_3_4 891 # ASSIGN : s_4_0 1 # ASSIGN : s_4_1 197 # ASSIGN : s_4_2 301 # ASSIGN : s_4_3 434 # ASSIGN : s_4_4 563 # ASSIGN : s_5_0 400 # ASSIGN : s_5_1 459 # ASSIGN : s_5_2 852 # ASSIGN : s_5_3 932 # ASSIGN : s_5_4 942 # ASSIGN : s_6_0 711 # ASSIGN : s_6_1 802 # ASSIGN : s_6_2 877 # ASSIGN : s_6_3 940 # ASSIGN : s_6_4 957 # ASSIGN : s_7_0 131 # ASSIGN : s_7_1 504 # ASSIGN : s_7_2 551 # ASSIGN : s_7_3 634 # ASSIGN : s_7_4 953 # ASSIGN : s_8_0 4 # ASSIGN : s_8_1 68 # ASSIGN : s_8_2 143 # ASSIGN : s_8_3 211 # ASSIGN : s_8_4 494 # ASSIGN : s_9_0 263 # ASSIGN : s_9_1 340 # ASSIGN : s_9_2 714 # ASSIGN : s_9_3 729 # ASSIGN : s_9_4 814 # ASSIGN : s_10_0 314 # ASSIGN : s_10_1 366 # ASSIGN : s_10_2 626 # ASSIGN : s_10_3 776 # ASSIGN : s_10_4 885 # ASSIGN : s_11_0 193 # ASSIGN : s_11_1 379 # ASSIGN : s_11_2 437 # ASSIGN : s_11_3 541 # ASSIGN : s_11_4 832 # ASSIGN : s_12_0 22 # ASSIGN : s_12_1 49 # ASSIGN : s_12_2 148 # ASSIGN : s_12_3 360 # ASSIGN : s_12_4 741 # ASSIGN : s_13_0 623 # ASSIGN : s_13_1 710 # ASSIGN : s_13_2 766 # ASSIGN : s_13_3 851 # ASSIGN : s_13_4 909 # ASSIGN : s_14_0 213 # ASSIGN : s_14_1 330 # ASSIGN : s_14_2 512 # ASSIGN : s_14_3 548 # ASSIGN : s_14_4 806 SHOW_RESULT 964 END : 964 (0 seconds) [Thu Jun 1 15:38:50 2006] SHOW_RESULT 964 CPU : 0.200000000000003 = 0.200000000000003 + 0 + 0 + 0 # BOUND : makespan 958 964 MODIFY_CNF 961 BEGIN : [Thu Jun 1 15:38:50 2006] MODIFY_CNF 961 END : 24290639 bytes (0 seconds) [Thu Jun 1 15:38:50 2006] MODIFY_CNF 961 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 961 BEGIN : [Thu Jun 1 15:38:50 2006] CMD : minisat /work/tamura/csp2sat82106.cnf /work/tamura/csp2sat82106.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 881710 2592394 | 293903 0 0 NaNQ | 0.000 % | | 100 | 881710 2592394 | 323293 100 1709 17.1 | 31.338 % | ==============================================================================) restarts : 2 conflicts : 150 (113 /sec) decisions : 545 (412 /sec) propagations : 627609 (474190 /sec) inspects : 7415042 (5602440 /sec) conflict literals : 2169 (14.00 % deleted) CPU time : 1.32354 s SATISFIABLE VERIFY_CNF 961 END : (2 seconds) [Thu Jun 1 15:38:52 2006] VERIFY_CNF 961 CPU : 1.94 = 0 + 0 + 1.85 + 0.09 # RESULT : makespan 961 SATISFIABLE SHOW_RESULT 961 BEGIN : [Thu Jun 1 15:38:52 2006] # ASSIGN : makespan 961 # ASSIGN : s_0_0 1 # ASSIGN : s_0_1 623 # ASSIGN : s_0_2 724 # ASSIGN : s_0_3 835 # ASSIGN : s_0_4 857 # ASSIGN : s_1_0 489 # ASSIGN : s_1_1 583 # ASSIGN : s_1_2 680 # ASSIGN : s_1_3 776 # ASSIGN : s_1_4 853 # ASSIGN : s_2_0 43 # ASSIGN : s_2_1 353 # ASSIGN : s_2_2 442 # ASSIGN : s_2_3 523 # ASSIGN : s_2_4 562 # ASSIGN : s_3_0 0 # ASSIGN : s_3_1 59 # ASSIGN : s_3_2 166 # ASSIGN : s_3_3 262 # ASSIGN : s_3_4 364 # ASSIGN : s_4_0 333 # ASSIGN : s_4_1 400 # ASSIGN : s_4_2 440 # ASSIGN : s_4_3 492 # ASSIGN : s_4_4 563 # ASSIGN : s_5_0 87 # ASSIGN : s_5_1 151 # ASSIGN : s_5_2 233 # ASSIGN : s_5_3 313 # ASSIGN : s_5_4 323 # ASSIGN : s_6_0 578 # ASSIGN : s_6_1 782 # ASSIGN : s_6_2 882 # ASSIGN : s_6_3 937 # ASSIGN : s_6_4 954 # ASSIGN : s_7_0 667 # ASSIGN : s_7_1 729 # ASSIGN : s_7_2 818 # ASSIGN : s_7_3 915 # ASSIGN : s_7_4 950 # ASSIGN : s_8_0 334 # ASSIGN : s_8_1 398 # ASSIGN : s_8_2 473 # ASSIGN : s_8_3 669 # ASSIGN : s_8_4 759 # ASSIGN : s_9_0 556 # ASSIGN : s_9_1 660 # ASSIGN : s_9_2 855 # ASSIGN : s_9_3 870 # ASSIGN : s_9_4 890 # ASSIGN : s_10_0 120 # ASSIGN : s_10_1 237 # ASSIGN : s_10_2 330 # ASSIGN : s_10_3 527 # ASSIGN : s_10_4 761 # ASSIGN : s_11_0 14 # ASSIGN : s_11_1 172 # ASSIGN : s_11_2 230 # ASSIGN : s_11_3 640 # ASSIGN : s_11_4 647 # ASSIGN : s_12_0 57 # ASSIGN : s_12_1 84 # ASSIGN : s_12_2 167 # ASSIGN : s_12_3 634 # ASSIGN : s_12_4 740 # ASSIGN : s_13_0 80 # ASSIGN : s_13_1 381 # ASSIGN : s_13_2 437 # ASSIGN : s_13_3 844 # ASSIGN : s_13_4 906 # ASSIGN : s_14_0 121 # ASSIGN : s_14_1 197 # ASSIGN : s_14_2 277 # ASSIGN : s_14_3 330 # ASSIGN : s_14_4 345 SHOW_RESULT 961 END : 961 (0 seconds) [Thu Jun 1 15:38:52 2006] SHOW_RESULT 961 CPU : 0.199999999999996 = 0.199999999999996 + 0 + 0 + 0 # BOUND : makespan 958 961 MODIFY_CNF 959 BEGIN : [Thu Jun 1 15:38:52 2006] MODIFY_CNF 959 END : 24290639 bytes (0 seconds) [Thu Jun 1 15:38:52 2006] MODIFY_CNF 959 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 959 BEGIN : [Thu Jun 1 15:38:52 2006] CMD : minisat /work/tamura/csp2sat82106.cnf /work/tamura/csp2sat82106.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 879458 2585790 | 293152 0 0 NaNQ | 0.000 % | | 100 | 879458 2585790 | 322467 100 1058 10.6 | 31.535 % | | 250 | 879458 2585790 | 354713 250 3732 14.9 | 31.535 % | | 475 | 879458 2585790 | 390185 475 6980 14.7 | 31.535 % | ==============================================================================) restarts : 4 conflicts : 634 (260 /sec) decisions : 1418 (581 /sec) propagations : 2514886 (1030698 /sec) inspects : 32810193 (13446889 /sec) conflict literals : 8913 (19.66 % deleted) CPU time : 2.43998 s SATISFIABLE VERIFY_CNF 959 END : (3 seconds) [Thu Jun 1 15:38:55 2006] VERIFY_CNF 959 CPU : 3.03 = 0.0100000000000051 + 0.01 + 2.93 + 0.08 # RESULT : makespan 959 SATISFIABLE SHOW_RESULT 959 BEGIN : [Thu Jun 1 15:38:55 2006] # ASSIGN : makespan 959 # ASSIGN : s_0_0 1 # ASSIGN : s_0_1 205 # ASSIGN : s_0_2 401 # ASSIGN : s_0_3 437 # ASSIGN : s_0_4 582 # ASSIGN : s_1_0 80 # ASSIGN : s_1_1 246 # ASSIGN : s_1_2 343 # ASSIGN : s_1_3 439 # ASSIGN : s_1_4 516 # ASSIGN : s_2_0 169 # ASSIGN : s_2_1 346 # ASSIGN : s_2_2 435 # ASSIGN : s_2_3 543 # ASSIGN : s_2_4 640 # ASSIGN : s_3_0 2 # ASSIGN : s_3_1 59 # ASSIGN : s_3_2 249 # ASSIGN : s_3_3 406 # ASSIGN : s_3_4 640 # ASSIGN : s_4_0 600 # ASSIGN : s_4_1 648 # ASSIGN : s_4_2 688 # ASSIGN : s_4_3 772 # ASSIGN : s_4_4 842 # ASSIGN : s_5_0 97 # ASSIGN : s_5_1 261 # ASSIGN : s_5_2 761 # ASSIGN : s_5_3 843 # ASSIGN : s_5_4 872 # ASSIGN : s_6_0 597 # ASSIGN : s_6_1 713 # ASSIGN : s_6_2 788 # ASSIGN : s_6_3 935 # ASSIGN : s_6_4 952 # ASSIGN : s_7_0 654 # ASSIGN : s_7_1 725 # ASSIGN : s_7_2 800 # ASSIGN : s_7_3 913 # ASSIGN : s_7_4 948 # ASSIGN : s_8_0 67 # ASSIGN : s_8_1 131 # ASSIGN : s_8_2 206 # ASSIGN : s_8_3 256 # ASSIGN : s_8_4 841 # ASSIGN : s_9_0 26 # ASSIGN : s_9_1 93 # ASSIGN : s_9_2 406 # ASSIGN : s_9_3 421 # ASSIGN : s_9_4 433 # ASSIGN : s_10_0 15 # ASSIGN : s_10_1 113 # ASSIGN : s_10_2 212 # ASSIGN : s_10_3 280 # ASSIGN : s_10_4 902 # ASSIGN : s_11_0 309 # ASSIGN : s_11_1 446 # ASSIGN : s_11_2 504 # ASSIGN : s_11_3 835 # ASSIGN : s_11_4 875 # ASSIGN : s_12_0 70 # ASSIGN : s_12_1 123 # ASSIGN : s_12_2 737 # ASSIGN : s_12_3 829 # ASSIGN : s_12_4 853 # ASSIGN : s_13_0 169 # ASSIGN : s_13_1 379 # ASSIGN : s_13_2 507 # ASSIGN : s_13_3 566 # ASSIGN : s_13_4 592 # ASSIGN : s_14_0 325 # ASSIGN : s_14_1 716 # ASSIGN : s_14_2 752 # ASSIGN : s_14_3 814 # ASSIGN : s_14_4 894 SHOW_RESULT 959 END : 959 (0 seconds) [Thu Jun 1 15:38:55 2006] SHOW_RESULT 959 CPU : 0.189999999999998 = 0.189999999999998 + 0 + 0 + 0 # BOUND : makespan 958 959 MODIFY_CNF 958 BEGIN : [Thu Jun 1 15:38:55 2006] MODIFY_CNF 958 END : 24290639 bytes (0 seconds) [Thu Jun 1 15:38:55 2006] MODIFY_CNF 958 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 958 BEGIN : [Thu Jun 1 15:38:55 2006] CMD : minisat /work/tamura/csp2sat82106.cnf /work/tamura/csp2sat82106.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 878333 2582490 | 292777 0 0 NaNQ | 0.000 % | | 100 | 878333 2582490 | 322054 100 1244 12.4 | 31.634 % | | 251 | 878333 2582490 | 354260 251 3430 13.7 | 31.634 % | ==============================================================================) restarts : 3 conflicts : 403 (210 /sec) decisions : 956 (499 /sec) propagations : 1714581 (894521 /sec) inspects : 19581775 (10216086 /sec) conflict literals : 4987 (25.88 % deleted) CPU time : 1.91676 s SATISFIABLE VERIFY_CNF 958 END : (3 seconds) [Thu Jun 1 15:38:58 2006] VERIFY_CNF 958 CPU : 2.46 = 0 + 0.01 + 2.41 + 0.04 # RESULT : makespan 958 SATISFIABLE SHOW_RESULT 958 BEGIN : [Thu Jun 1 15:38:58 2006] # ASSIGN : makespan 958 # ASSIGN : s_0_0 0 # ASSIGN : s_0_1 602 # ASSIGN : s_0_2 865 # ASSIGN : s_0_3 870 # ASSIGN : s_0_4 900 # ASSIGN : s_1_0 372 # ASSIGN : s_1_1 486 # ASSIGN : s_1_2 583 # ASSIGN : s_1_3 679 # ASSIGN : s_1_4 756 # ASSIGN : s_2_0 120 # ASSIGN : s_2_1 559 # ASSIGN : s_2_2 646 # ASSIGN : s_2_3 741 # ASSIGN : s_2_4 780 # ASSIGN : s_3_0 87 # ASSIGN : s_3_1 208 # ASSIGN : s_3_2 229 # ASSIGN : s_3_3 308 # ASSIGN : s_3_4 323 # ASSIGN : s_4_0 181 # ASSIGN : s_4_1 261 # ASSIGN : s_4_2 301 # ASSIGN : s_4_3 400 # ASSIGN : s_4_4 470 # ASSIGN : s_5_0 144 # ASSIGN : s_5_1 178 # ASSIGN : s_5_2 260 # ASSIGN : s_5_3 340 # ASSIGN : s_5_4 350 # ASSIGN : s_6_0 646 # ASSIGN : s_6_1 783 # ASSIGN : s_6_2 879 # ASSIGN : s_6_3 934 # ASSIGN : s_6_4 951 # ASSIGN : s_7_0 119 # ASSIGN : s_7_1 182 # ASSIGN : s_7_2 229 # ASSIGN : s_7_3 865 # ASSIGN : s_7_4 947 # ASSIGN : s_8_0 197 # ASSIGN : s_8_1 321 # ASSIGN : s_8_2 396 # ASSIGN : s_8_3 469 # ASSIGN : s_8_4 840 # ASSIGN : s_9_0 409 # ASSIGN : s_9_1 721 # ASSIGN : s_9_2 765 # ASSIGN : s_9_3 858 # ASSIGN : s_9_4 887 # ASSIGN : s_10_0 33 # ASSIGN : s_10_1 85 # ASSIGN : s_10_2 563 # ASSIGN : s_10_3 727 # ASSIGN : s_10_4 830 # ASSIGN : s_11_0 532 # ASSIGN : s_11_1 679 # ASSIGN : s_11_2 737 # ASSIGN : s_11_3 858 # ASSIGN : s_11_4 874 # ASSIGN : s_12_0 10 # ASSIGN : s_12_1 37 # ASSIGN : s_12_2 145 # ASSIGN : s_12_3 541 # ASSIGN : s_12_4 763 # ASSIGN : s_13_0 58 # ASSIGN : s_13_1 476 # ASSIGN : s_13_2 547 # ASSIGN : s_13_3 605 # ASSIGN : s_13_4 631 # ASSIGN : s_14_0 245 # ASSIGN : s_14_1 373 # ASSIGN : s_14_2 410 # ASSIGN : s_14_3 446 # ASSIGN : s_14_4 461 SHOW_RESULT 958 END : 958 (0 seconds) [Thu Jun 1 15:38:58 2006] SHOW_RESULT 958 CPU : 0.190000000000005 = 0.190000000000005 + 0 + 0 + 0 # BOUND : makespan 958 958 MAIN END : (72 seconds) [Thu Jun 1 15:38:58 2006] MAIN CPU : 71.32 = 58.42 + 0.11 + 12.44 + 0.35