MAIN BEGIN : [Thu Jun 1 16:35:57 2006] READ BEGIN : csp/la22.csp [Thu Jun 1 16:35:57 2006] READ END : csp/la22.csp (3 seconds) [Thu Jun 1 16:36:00 2006] READ CPU : 2.97 = 2.97 + 0 + 0 + 0 # BOUND : makespan 830 1294 GENERATE_CNF 1294 BEGIN : [Thu Jun 1 16:36:00 2006] GENERATE_CNF 1294 END : 197116 variables 2990547 clauses 69802278 bytes (146 seconds) [Thu Jun 1 16:38:26 2006] GENERATE_CNF 1294 CPU : 145.7 = 145.49 + 0.21 + 0 + 0 MODIFY_CNF 1062 BEGIN : [Thu Jun 1 16:38:26 2006] MODIFY_CNF 1062 END : 69802284 bytes (0 seconds) [Thu Jun 1 16:38:26 2006] MODIFY_CNF 1062 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1062 BEGIN : [Thu Jun 1 16:38:26 2006] CMD : minisat /work/tamura/csp2sat95922.cnf /work/tamura/csp2sat95922.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1544206 4545088 | 514735 0 0 NaNQ | 0.000 % | ==============================================================================) restarts : 1 conflicts : 36 (10 /sec) decisions : 380 (106 /sec) propagations : 380945 (106446 /sec) inspects : 4053185 (1132567 /sec) conflict literals : 338 (21.40 % deleted) CPU time : 3.57876 s SATISFIABLE VERIFY_CNF 1062 END : (5 seconds) [Thu Jun 1 16:38:31 2006] VERIFY_CNF 1062 CPU : 4.54999999999999 = 0.00999999999999091 + 0.01 + 4.47 + 0.06 # RESULT : makespan 1062 SATISFIABLE SHOW_RESULT 1062 BEGIN : [Thu Jun 1 16:38:31 2006] # ASSIGN : makespan 1062 # ASSIGN : s_0_0 56 # ASSIGN : s_0_1 122 # ASSIGN : s_0_2 213 # ASSIGN : s_0_3 466 # ASSIGN : s_0_4 611 # ASSIGN : s_0_5 795 # ASSIGN : s_0_6 887 # ASSIGN : s_0_7 894 # ASSIGN : s_0_8 906 # ASSIGN : s_0_9 976 # ASSIGN : s_1_0 5 # ASSIGN : s_1_1 60 # ASSIGN : s_1_2 80 # ASSIGN : s_1_3 284 # ASSIGN : s_1_4 298 # ASSIGN : s_1_5 377 # ASSIGN : s_1_6 554 # ASSIGN : s_1_7 659 # ASSIGN : s_1_8 761 # ASSIGN : s_1_9 899 # ASSIGN : s_2_0 1 # ASSIGN : s_2_1 127 # ASSIGN : s_2_2 294 # ASSIGN : s_2_3 349 # ASSIGN : s_2_4 364 # ASSIGN : s_2_5 509 # ASSIGN : s_2_6 713 # ASSIGN : s_2_7 789 # ASSIGN : s_2_8 842 # ASSIGN : s_2_9 915 # ASSIGN : s_3_0 18 # ASSIGN : s_3_1 137 # ASSIGN : s_3_2 211 # ASSIGN : s_3_3 300 # ASSIGN : s_3_4 443 # ASSIGN : s_3_5 517 # ASSIGN : s_3_6 598 # ASSIGN : s_3_7 802 # ASSIGN : s_3_8 916 # ASSIGN : s_3_9 968 # ASSIGN : s_4_0 87 # ASSIGN : s_4_1 187 # ASSIGN : s_4_2 202 # ASSIGN : s_4_3 328 # ASSIGN : s_4_4 389 # ASSIGN : s_4_5 750 # ASSIGN : s_4_6 812 # ASSIGN : s_4_7 901 # ASSIGN : s_4_8 912 # ASSIGN : s_4_9 1057 # ASSIGN : s_5_0 38 # ASSIGN : s_5_1 122 # ASSIGN : s_5_2 175 # ASSIGN : s_5_3 247 # ASSIGN : s_5_4 495 # ASSIGN : s_5_5 586 # ASSIGN : s_5_6 654 # ASSIGN : s_5_7 704 # ASSIGN : s_5_8 823 # ASSIGN : s_5_9 985 # ASSIGN : s_6_0 300 # ASSIGN : s_6_1 452 # ASSIGN : s_6_2 488 # ASSIGN : s_6_3 607 # ASSIGN : s_6_4 675 # ASSIGN : s_6_5 950 # ASSIGN : s_6_6 991 # ASSIGN : s_6_7 1014 # ASSIGN : s_6_8 1039 # ASSIGN : s_6_9 1056 # ASSIGN : s_7_0 5 # ASSIGN : s_7_1 70 # ASSIGN : s_7_2 78 # ASSIGN : s_7_3 163 # ASSIGN : s_7_4 234 # ASSIGN : s_7_5 299 # ASSIGN : s_7_6 327 # ASSIGN : s_7_7 415 # ASSIGN : s_7_8 491 # ASSIGN : s_7_9 846 # ASSIGN : s_8_0 518 # ASSIGN : s_8_1 555 # ASSIGN : s_8_2 592 # ASSIGN : s_8_3 620 # ASSIGN : s_8_4 671 # ASSIGN : s_8_5 757 # ASSIGN : s_8_6 766 # ASSIGN : s_8_7 821 # ASSIGN : s_8_8 921 # ASSIGN : s_8_9 972 # ASSIGN : s_9_0 45 # ASSIGN : s_9_1 390 # ASSIGN : s_9_2 405 # ASSIGN : s_9_3 582 # ASSIGN : s_9_4 632 # ASSIGN : s_9_5 720 # ASSIGN : s_9_6 736 # ASSIGN : s_9_7 782 # ASSIGN : s_9_8 943 # ASSIGN : s_9_9 980 # ASSIGN : s_10_0 84 # ASSIGN : s_10_1 362 # ASSIGN : s_10_2 452 # ASSIGN : s_10_3 560 # ASSIGN : s_10_4 626 # ASSIGN : s_10_5 631 # ASSIGN : s_10_6 685 # ASSIGN : s_10_7 758 # ASSIGN : s_10_8 806 # ASSIGN : s_10_9 1002 # ASSIGN : s_11_0 156 # ASSIGN : s_11_1 395 # ASSIGN : s_11_2 539 # ASSIGN : s_11_3 636 # ASSIGN : s_11_4 678 # ASSIGN : s_11_5 724 # ASSIGN : s_11_6 793 # ASSIGN : s_11_7 817 # ASSIGN : s_11_8 876 # ASSIGN : s_11_9 910 # ASSIGN : s_12_0 61 # ASSIGN : s_12_1 84 # ASSIGN : s_12_2 109 # ASSIGN : s_12_3 254 # ASSIGN : s_12_4 278 # ASSIGN : s_12_5 306 # ASSIGN : s_12_6 871 # ASSIGN : s_12_7 900 # ASSIGN : s_12_8 941 # ASSIGN : s_12_9 1017 # ASSIGN : s_13_0 32 # ASSIGN : s_13_1 69 # ASSIGN : s_13_2 147 # ASSIGN : s_13_3 511 # ASSIGN : s_13_4 549 # ASSIGN : s_13_5 675 # ASSIGN : s_13_6 905 # ASSIGN : s_13_7 917 # ASSIGN : s_13_8 995 # ASSIGN : s_13_9 1050 # ASSIGN : s_14_0 410 # ASSIGN : s_14_1 500 # ASSIGN : s_14_2 657 # ASSIGN : s_14_3 706 # ASSIGN : s_14_4 793 # ASSIGN : s_14_5 833 # ASSIGN : s_14_6 856 # ASSIGN : s_14_7 938 # ASSIGN : s_14_8 965 # ASSIGN : s_14_9 1014 SHOW_RESULT 1062 END : 1062 (1 seconds) [Thu Jun 1 16:38:32 2006] SHOW_RESULT 1062 CPU : 0.54000000000002 = 0.54000000000002 + 0 + 0 + 0 # BOUND : makespan 830 1062 MODIFY_CNF 946 BEGIN : [Thu Jun 1 16:38:32 2006] MODIFY_CNF 946 END : 69802284 bytes (0 seconds) [Thu Jun 1 16:38:32 2006] MODIFY_CNF 946 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 946 BEGIN : [Thu Jun 1 16:38:32 2006] CMD : minisat /work/tamura/csp2sat95922.cnf /work/tamura/csp2sat95922.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1239892 3649750 | 413297 0 0 NaNQ | 0.000 % | | 100 | 1239892 3649750 | 454626 100 2086 20.9 | 64.101 % | | 250 | 1239892 3649750 | 500089 250 5147 20.6 | 64.101 % | | 475 | 1239892 3649750 | 550098 475 8087 17.0 | 64.101 % | | 813 | 1239892 3649750 | 605108 813 12097 14.9 | 64.101 % | | 1319 | 1239892 3649750 | 665618 1319 23164 17.6 | 64.101 % | | 2078 | 1239892 3649750 | 732180 2078 34930 16.8 | 64.101 % | | 3217 | 1239892 3649750 | 805398 3217 63989 19.9 | 64.101 % | | 4925 | 1239892 3649750 | 885938 4925 94365 19.2 | 64.101 % | | 7487 | 1239892 3649750 | 974532 7487 140479 18.8 | 64.101 % | ==============================================================================) restarts : 10 conflicts : 8560 (228 /sec) decisions : 12604 (336 /sec) propagations : 64027083 (1704414 /sec) inspects : 635434274 (16915389 /sec) conflict literals : 156735 (30.20 % deleted) CPU time : 37.5655 s SATISFIABLE VERIFY_CNF 946 END : (38 seconds) [Thu Jun 1 16:39:10 2006] VERIFY_CNF 946 CPU : 38.6 = 0 + 0.02 + 38.33 + 0.25 # RESULT : makespan 946 SATISFIABLE SHOW_RESULT 946 BEGIN : [Thu Jun 1 16:39:10 2006] # ASSIGN : makespan 946 # ASSIGN : s_0_0 4 # ASSIGN : s_0_1 184 # ASSIGN : s_0_2 275 # ASSIGN : s_0_3 386 # ASSIGN : s_0_4 480 # ASSIGN : s_0_5 689 # ASSIGN : s_0_6 781 # ASSIGN : s_0_7 788 # ASSIGN : s_0_8 846 # ASSIGN : s_0_9 927 # ASSIGN : s_1_0 13 # ASSIGN : s_1_1 45 # ASSIGN : s_1_2 65 # ASSIGN : s_1_3 93 # ASSIGN : s_1_4 107 # ASSIGN : s_1_5 237 # ASSIGN : s_1_6 556 # ASSIGN : s_1_7 653 # ASSIGN : s_1_8 828 # ASSIGN : s_1_9 939 # ASSIGN : s_2_0 4 # ASSIGN : s_2_1 97 # ASSIGN : s_2_2 117 # ASSIGN : s_2_3 151 # ASSIGN : s_2_4 217 # ASSIGN : s_2_5 305 # ASSIGN : s_2_6 503 # ASSIGN : s_2_7 600 # ASSIGN : s_2_8 655 # ASSIGN : s_2_9 722 # ASSIGN : s_3_0 104 # ASSIGN : s_3_1 182 # ASSIGN : s_3_2 256 # ASSIGN : s_3_3 490 # ASSIGN : s_3_4 552 # ASSIGN : s_3_5 606 # ASSIGN : s_3_6 693 # ASSIGN : s_3_7 702 # ASSIGN : s_3_8 800 # ASSIGN : s_3_9 852 # ASSIGN : s_4_0 72 # ASSIGN : s_4_1 163 # ASSIGN : s_4_2 236 # ASSIGN : s_4_3 302 # ASSIGN : s_4_4 426 # ASSIGN : s_4_5 613 # ASSIGN : s_4_6 675 # ASSIGN : s_4_7 780 # ASSIGN : s_4_8 796 # ASSIGN : s_4_9 941 # ASSIGN : s_5_0 9 # ASSIGN : s_5_1 110 # ASSIGN : s_5_2 160 # ASSIGN : s_5_3 282 # ASSIGN : s_5_4 335 # ASSIGN : s_5_5 472 # ASSIGN : s_5_6 605 # ASSIGN : s_5_7 702 # ASSIGN : s_5_8 802 # ASSIGN : s_5_9 869 # ASSIGN : s_6_0 131 # ASSIGN : s_6_1 401 # ASSIGN : s_6_2 437 # ASSIGN : s_6_3 511 # ASSIGN : s_6_4 743 # ASSIGN : s_6_5 816 # ASSIGN : s_6_6 875 # ASSIGN : s_6_7 898 # ASSIGN : s_6_8 923 # ASSIGN : s_6_9 940 # ASSIGN : s_7_0 0 # ASSIGN : s_7_1 73 # ASSIGN : s_7_2 81 # ASSIGN : s_7_3 166 # ASSIGN : s_7_4 270 # ASSIGN : s_7_5 344 # ASSIGN : s_7_6 394 # ASSIGN : s_7_7 524 # ASSIGN : s_7_8 601 # ASSIGN : s_7_9 707 # ASSIGN : s_8_0 70 # ASSIGN : s_8_1 118 # ASSIGN : s_8_2 198 # ASSIGN : s_8_3 226 # ASSIGN : s_8_4 277 # ASSIGN : s_8_5 363 # ASSIGN : s_8_6 372 # ASSIGN : s_8_7 427 # ASSIGN : s_8_8 501 # ASSIGN : s_8_9 563 # ASSIGN : s_9_0 26 # ASSIGN : s_9_1 65 # ASSIGN : s_9_2 80 # ASSIGN : s_9_3 173 # ASSIGN : s_9_4 217 # ASSIGN : s_9_5 500 # ASSIGN : s_9_6 623 # ASSIGN : s_9_7 669 # ASSIGN : s_9_8 827 # ASSIGN : s_9_9 857 # ASSIGN : s_10_0 155 # ASSIGN : s_10_1 227 # ASSIGN : s_10_2 340 # ASSIGN : s_10_3 491 # ASSIGN : s_10_4 628 # ASSIGN : s_10_5 633 # ASSIGN : s_10_6 687 # ASSIGN : s_10_7 734 # ASSIGN : s_10_8 789 # ASSIGN : s_10_9 886 # ASSIGN : s_11_0 450 # ASSIGN : s_11_1 496 # ASSIGN : s_11_2 516 # ASSIGN : s_11_3 635 # ASSIGN : s_11_4 656 # ASSIGN : s_11_5 726 # ASSIGN : s_11_6 769 # ASSIGN : s_11_7 798 # ASSIGN : s_11_8 857 # ASSIGN : s_11_9 891 # ASSIGN : s_12_0 56 # ASSIGN : s_12_1 79 # ASSIGN : s_12_2 178 # ASSIGN : s_12_3 288 # ASSIGN : s_12_4 312 # ASSIGN : s_12_5 604 # ASSIGN : s_12_6 788 # ASSIGN : s_12_7 820 # ASSIGN : s_12_8 825 # ASSIGN : s_12_9 901 # ASSIGN : s_13_0 20 # ASSIGN : s_13_1 57 # ASSIGN : s_13_2 130 # ASSIGN : s_13_3 362 # ASSIGN : s_13_4 411 # ASSIGN : s_13_5 482 # ASSIGN : s_13_6 561 # ASSIGN : s_13_7 573 # ASSIGN : s_13_8 802 # ASSIGN : s_13_9 934 # ASSIGN : s_14_0 400 # ASSIGN : s_14_1 540 # ASSIGN : s_14_2 557 # ASSIGN : s_14_3 606 # ASSIGN : s_14_4 700 # ASSIGN : s_14_5 740 # ASSIGN : s_14_6 763 # ASSIGN : s_14_7 842 # ASSIGN : s_14_8 884 # ASSIGN : s_14_9 898 SHOW_RESULT 946 END : 946 (1 seconds) [Thu Jun 1 16:39:11 2006] SHOW_RESULT 946 CPU : 0.530000000000001 = 0.530000000000001 + 0 + 0 + 0 # BOUND : makespan 830 946 MODIFY_CNF 888 BEGIN : [Thu Jun 1 16:39:11 2006] MODIFY_CNF 888 END : 69802283 bytes (0 seconds) [Thu Jun 1 16:39:11 2006] MODIFY_CNF 888 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 888 BEGIN : [Thu Jun 1 16:39:11 2006] CMD : minisat /work/tamura/csp2sat95922.cnf /work/tamura/csp2sat95922.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1073424 3159188 | 357808 0 0 NaNQ | 0.000 % | | 100 | 1073424 3159188 | 393588 100 994 9.9 | 68.601 % | | 252 | 1073424 3159188 | 432947 252 2396 9.5 | 68.601 % | | 477 | 1073424 3159188 | 476242 477 4458 9.3 | 68.601 % | | 814 | 1073424 3159188 | 523866 814 7897 9.7 | 68.601 % | | 1320 | 1073424 3159188 | 576253 1320 13505 10.2 | 68.601 % | | 2079 | 1072976 3157845 | 633878 1900 19594 10.3 | 69.321 % | ==============================================================================) restarts : 7 conflicts : 2823 (222 /sec) decisions : 3877 (305 /sec) propagations : 18029453 (1420148 /sec) inspects : 152200649 (11988578 /sec) conflict literals : 28789 (34.39 % deleted) CPU time : 12.6955 s UNSATISFIABLE VERIFY_CNF 888 END : (13 seconds) [Thu Jun 1 16:39:24 2006] VERIFY_CNF 888 CPU : 13.59 = 0.00999999999999091 + 0.01 + 13.32 + 0.25 # RESULT : makespan 888 UNSATISFIABLE # BOUND : makespan 889 946 MODIFY_CNF 917 BEGIN : [Thu Jun 1 16:39:24 2006] MODIFY_CNF 917 END : 69802283 bytes (0 seconds) [Thu Jun 1 16:39:24 2006] MODIFY_CNF 917 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 917 BEGIN : [Thu Jun 1 16:39:24 2006] CMD : minisat /work/tamura/csp2sat95922.cnf /work/tamura/csp2sat95922.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1161668 3419485 | 387222 0 0 NaNQ | 0.000 % | | 103 | 1161668 3419485 | 425944 103 990 9.6 | 66.343 % | | 253 | 1161668 3419485 | 468538 253 2468 9.8 | 66.343 % | | 478 | 1161668 3419485 | 515392 478 4601 9.6 | 66.343 % | | 816 | 1161668 3419485 | 566931 816 8834 10.8 | 66.343 % | | 1322 | 1161668 3419485 | 623624 1322 13598 10.3 | 66.343 % | | 2085 | 1161668 3419485 | 685987 2085 21063 10.1 | 66.343 % | | 3224 | 1161668 3419485 | 754586 3224 37613 11.7 | 66.343 % | | 4933 | 1161668 3419485 | 830044 4933 61681 12.5 | 66.343 % | | 7495 | 1161668 3419485 | 913049 7495 100347 13.4 | 66.343 % | | 11339 | 1161668 3419485 | 1004354 11339 156413 13.8 | 66.343 % | | 17105 | 1115165 3281773 | 1104789 11456 145694 12.7 | 67.263 % | ==============================================================================) restarts : 12 conflicts : 17926 (290 /sec) decisions : 24372 (394 /sec) propagations : 115637899 (1867772 /sec) inspects : 1059469463 (17112446 /sec) conflict literals : 251215 (36.26 % deleted) CPU time : 61.9122 s UNSATISFIABLE VERIFY_CNF 917 END : (63 seconds) [Thu Jun 1 16:40:27 2006] VERIFY_CNF 917 CPU : 62.66 = 0 + 0.01 + 62.58 + 0.07 # RESULT : makespan 917 UNSATISFIABLE # BOUND : makespan 918 946 MODIFY_CNF 932 BEGIN : [Thu Jun 1 16:40:27 2006] MODIFY_CNF 932 END : 69802284 bytes (0 seconds) [Thu Jun 1 16:40:27 2006] MODIFY_CNF 932 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 932 BEGIN : [Thu Jun 1 16:40:27 2006] CMD : minisat /work/tamura/csp2sat95922.cnf /work/tamura/csp2sat95922.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1203251 3541951 | 401083 0 0 NaNQ | 0.000 % | | 100 | 1203251 3541951 | 441191 100 1385 13.8 | 65.182 % | | 250 | 1203251 3541951 | 485310 250 2950 11.8 | 65.182 % | | 475 | 1203251 3541951 | 533841 475 4844 10.2 | 65.182 % | | 812 | 1203251 3541951 | 587225 812 8297 10.2 | 65.182 % | | 1318 | 1203251 3541951 | 645948 1318 13521 10.3 | 65.182 % | | 2077 | 1203251 3541951 | 710543 2077 22590 10.9 | 65.182 % | | 3218 | 1203251 3541951 | 781597 3218 33790 10.5 | 65.182 % | | 4926 | 1203251 3541951 | 859757 4926 55779 11.3 | 65.182 % | | 7491 | 1203251 3541951 | 945732 7491 104639 14.0 | 65.182 % | ==============================================================================) restarts : 10 conflicts : 7885 (275 /sec) decisions : 11460 (399 /sec) propagations : 50102941 (1744695 /sec) inspects : 475534491 (16559159 /sec) conflict literals : 111967 (28.65 % deleted) CPU time : 28.7173 s SATISFIABLE VERIFY_CNF 932 END : (30 seconds) [Thu Jun 1 16:40:57 2006] VERIFY_CNF 932 CPU : 29.58 = 0.0100000000000193 + 0.01 + 29.48 + 0.08 # RESULT : makespan 932 SATISFIABLE SHOW_RESULT 932 BEGIN : [Thu Jun 1 16:40:57 2006] # ASSIGN : makespan 932 # ASSIGN : s_0_0 52 # ASSIGN : s_0_1 200 # ASSIGN : s_0_2 510 # ASSIGN : s_0_3 597 # ASSIGN : s_0_4 691 # ASSIGN : s_0_5 739 # ASSIGN : s_0_6 831 # ASSIGN : s_0_7 872 # ASSIGN : s_0_8 902 # ASSIGN : s_0_9 913 # ASSIGN : s_1_0 95 # ASSIGN : s_1_1 335 # ASSIGN : s_1_2 395 # ASSIGN : s_1_3 412 # ASSIGN : s_1_4 426 # ASSIGN : s_1_5 492 # ASSIGN : s_1_6 600 # ASSIGN : s_1_7 677 # ASSIGN : s_1_8 814 # ASSIGN : s_1_9 925 # ASSIGN : s_2_0 15 # ASSIGN : s_2_1 92 # ASSIGN : s_2_2 132 # ASSIGN : s_2_3 166 # ASSIGN : s_2_4 203 # ASSIGN : s_2_5 291 # ASSIGN : s_2_6 547 # ASSIGN : s_2_7 635 # ASSIGN : s_2_8 641 # ASSIGN : s_2_9 708 # ASSIGN : s_3_0 68 # ASSIGN : s_3_1 182 # ASSIGN : s_3_2 256 # ASSIGN : s_3_3 448 # ASSIGN : s_3_4 534 # ASSIGN : s_3_5 599 # ASSIGN : s_3_6 668 # ASSIGN : s_3_7 688 # ASSIGN : s_3_8 786 # ASSIGN : s_3_9 838 # ASSIGN : s_4_0 65 # ASSIGN : s_4_1 163 # ASSIGN : s_4_2 360 # ASSIGN : s_4_3 442 # ASSIGN : s_4_4 586 # ASSIGN : s_4_5 644 # ASSIGN : s_4_6 706 # ASSIGN : s_4_7 771 # ASSIGN : s_4_8 837 # ASSIGN : s_4_9 927 # ASSIGN : s_5_0 1 # ASSIGN : s_5_1 112 # ASSIGN : s_5_2 153 # ASSIGN : s_5_3 228 # ASSIGN : s_5_4 321 # ASSIGN : s_5_5 418 # ASSIGN : s_5_6 591 # ASSIGN : s_5_7 693 # ASSIGN : s_5_8 788 # ASSIGN : s_5_9 855 # ASSIGN : s_6_0 133 # ASSIGN : s_6_1 336 # ASSIGN : s_6_2 372 # ASSIGN : s_6_3 521 # ASSIGN : s_6_4 741 # ASSIGN : s_6_5 790 # ASSIGN : s_6_6 861 # ASSIGN : s_6_7 884 # ASSIGN : s_6_8 909 # ASSIGN : s_6_9 926 # ASSIGN : s_7_0 0 # ASSIGN : s_7_1 76 # ASSIGN : s_7_2 96 # ASSIGN : s_7_3 181 # ASSIGN : s_7_4 256 # ASSIGN : s_7_5 344 # ASSIGN : s_7_6 380 # ASSIGN : s_7_7 476 # ASSIGN : s_7_8 615 # ASSIGN : s_7_9 693 # ASSIGN : s_8_0 118 # ASSIGN : s_8_1 202 # ASSIGN : s_8_2 239 # ASSIGN : s_8_3 281 # ASSIGN : s_8_4 332 # ASSIGN : s_8_5 433 # ASSIGN : s_8_6 492 # ASSIGN : s_8_7 567 # ASSIGN : s_8_8 640 # ASSIGN : s_8_9 780 # ASSIGN : s_9_0 18 # ASSIGN : s_9_1 57 # ASSIGN : s_9_2 72 # ASSIGN : s_9_3 155 # ASSIGN : s_9_4 199 # ASSIGN : s_9_5 252 # ASSIGN : s_9_6 402 # ASSIGN : s_9_7 468 # ASSIGN : s_9_8 795 # ASSIGN : s_9_9 820 # ASSIGN : s_10_0 84 # ASSIGN : s_10_1 191 # ASSIGN : s_10_2 268 # ASSIGN : s_10_3 355 # ASSIGN : s_10_4 421 # ASSIGN : s_10_5 438 # ASSIGN : s_10_6 495 # ASSIGN : s_10_7 536 # ASSIGN : s_10_8 573 # ASSIGN : s_10_9 679 # ASSIGN : s_11_0 156 # ASSIGN : s_11_1 375 # ASSIGN : s_11_2 395 # ASSIGN : s_11_3 576 # ASSIGN : s_11_4 642 # ASSIGN : s_11_5 712 # ASSIGN : s_11_6 765 # ASSIGN : s_11_7 784 # ASSIGN : s_11_8 843 # ASSIGN : s_11_9 877 # ASSIGN : s_12_0 85 # ASSIGN : s_12_1 108 # ASSIGN : s_12_2 178 # ASSIGN : s_12_3 336 # ASSIGN : s_12_4 367 # ASSIGN : s_12_5 412 # ASSIGN : s_12_6 571 # ASSIGN : s_12_7 806 # ASSIGN : s_12_8 811 # ASSIGN : s_12_9 887 # ASSIGN : s_13_0 22 # ASSIGN : s_13_1 59 # ASSIGN : s_13_2 112 # ASSIGN : s_13_3 357 # ASSIGN : s_13_4 405 # ASSIGN : s_13_5 492 # ASSIGN : s_13_6 603 # ASSIGN : s_13_7 673 # ASSIGN : s_13_8 788 # ASSIGN : s_13_9 920 # ASSIGN : s_14_0 267 # ASSIGN : s_14_1 486 # ASSIGN : s_14_2 503 # ASSIGN : s_14_3 552 # ASSIGN : s_14_4 686 # ASSIGN : s_14_5 726 # ASSIGN : s_14_6 749 # ASSIGN : s_14_7 828 # ASSIGN : s_14_8 870 # ASSIGN : s_14_9 884 SHOW_RESULT 932 END : 932 (1 seconds) [Thu Jun 1 16:40:58 2006] SHOW_RESULT 932 CPU : 0.569999999999993 = 0.569999999999993 + 0 + 0 + 0 # BOUND : makespan 918 932 MODIFY_CNF 925 BEGIN : [Thu Jun 1 16:40:58 2006] MODIFY_CNF 925 END : 69802283 bytes (0 seconds) [Thu Jun 1 16:40:58 2006] MODIFY_CNF 925 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 925 BEGIN : [Thu Jun 1 16:40:58 2006] CMD : minisat /work/tamura/csp2sat95922.cnf /work/tamura/csp2sat95922.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1184972 3488178 | 394990 0 0 NaNQ | 0.000 % | | 101 | 1184972 3488178 | 434489 101 1290 12.8 | 65.722 % | | 251 | 1184972 3488178 | 477937 251 2521 10.0 | 65.722 % | | 476 | 1184972 3488178 | 525731 476 4589 9.6 | 65.722 % | | 813 | 1184972 3488178 | 578304 813 7973 9.8 | 65.722 % | | 1319 | 1184972 3488178 | 636135 1319 13952 10.6 | 65.722 % | | 2078 | 1184972 3488178 | 699748 2078 23195 11.2 | 65.722 % | | 3217 | 1184972 3488178 | 769723 3217 37053 11.5 | 65.722 % | | 4927 | 1184465 3486658 | 846696 4054 45881 11.3 | 65.723 % | | 7490 | 1184465 3486658 | 931365 6617 73819 11.2 | 65.723 % | | 11336 | 1184465 3486658 | 1024502 10463 126195 12.1 | 65.723 % | | 17102 | 1168469 3439209 | 1126952 13139 159547 12.1 | 65.999 % | ==============================================================================) restarts : 12 conflicts : 24838 (310 /sec) decisions : 32593 (407 /sec) propagations : 152921184 (1909565 /sec) inspects : 1407030573 (17569946 /sec) conflict literals : 316108 (36.28 % deleted) CPU time : 80.0817 s UNSATISFIABLE VERIFY_CNF 925 END : (81 seconds) [Thu Jun 1 16:42:19 2006] VERIFY_CNF 925 CPU : 81.03 = 0 + 0.02 + 80.76 + 0.25 # RESULT : makespan 925 UNSATISFIABLE # BOUND : makespan 926 932 MODIFY_CNF 929 BEGIN : [Thu Jun 1 16:42:19 2006] MODIFY_CNF 929 END : 69802284 bytes (0 seconds) [Thu Jun 1 16:42:19 2006] MODIFY_CNF 929 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 929 BEGIN : [Thu Jun 1 16:42:19 2006] CMD : minisat /work/tamura/csp2sat95922.cnf /work/tamura/csp2sat95922.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1195250 3518405 | 398416 0 0 NaNQ | 0.000 % | | 100 | 1195250 3518405 | 438257 100 1607 16.1 | 65.414 % | | 251 | 1195250 3518405 | 482083 251 2925 11.7 | 65.414 % | | 477 | 1195250 3518405 | 530291 477 4889 10.2 | 65.414 % | | 815 | 1195250 3518405 | 583320 815 9503 11.7 | 65.414 % | | 1322 | 1195250 3518405 | 641652 1322 15117 11.4 | 65.414 % | | 2082 | 1194631 3516549 | 705818 1803 19932 11.1 | 65.415 % | | 3224 | 1193716 3513864 | 776400 2944 31831 10.8 | 65.445 % | | 4932 | 1193716 3513864 | 854040 4652 72123 15.5 | 65.445 % | | 7494 | 1193716 3513864 | 939444 7214 117826 16.3 | 65.445 % | | 11338 | 1193716 3513864 | 1033388 11058 172166 15.6 | 65.445 % | | 17104 | 1193128 3512102 | 1136727 14939 233713 15.6 | 65.446 % | | 25755 | 1193128 3512102 | 1250400 23590 423603 18.0 | 65.446 % | ==============================================================================) restarts : 13 conflicts : 37984 (264 /sec) decisions : 52659 (366 /sec) propagations : 254465827 (1769718 /sec) inspects : 2518102667 (17512500 /sec) conflict literals : 776993 (33.74 % deleted) CPU time : 143.789 s SATISFIABLE VERIFY_CNF 929 END : (145 seconds) [Thu Jun 1 16:44:44 2006] VERIFY_CNF 929 CPU : 144.67 = 0.00999999999999091 + 0.01 + 144.57 + 0.0800000000000001 # RESULT : makespan 929 SATISFIABLE SHOW_RESULT 929 BEGIN : [Thu Jun 1 16:44:44 2006] # ASSIGN : makespan 929 # ASSIGN : s_0_0 1 # ASSIGN : s_0_1 197 # ASSIGN : s_0_2 468 # ASSIGN : s_0_3 555 # ASSIGN : s_0_4 649 # ASSIGN : s_0_5 687 # ASSIGN : s_0_6 810 # ASSIGN : s_0_7 817 # ASSIGN : s_0_8 829 # ASSIGN : s_0_9 910 # ASSIGN : s_1_0 2 # ASSIGN : s_1_1 320 # ASSIGN : s_1_2 361 # ASSIGN : s_1_3 370 # ASSIGN : s_1_4 384 # ASSIGN : s_1_5 450 # ASSIGN : s_1_6 539 # ASSIGN : s_1_7 624 # ASSIGN : s_1_8 811 # ASSIGN : s_1_9 922 # ASSIGN : s_2_0 5 # ASSIGN : s_2_1 93 # ASSIGN : s_2_2 118 # ASSIGN : s_2_3 152 # ASSIGN : s_2_4 200 # ASSIGN : s_2_5 288 # ASSIGN : s_2_6 486 # ASSIGN : s_2_7 575 # ASSIGN : s_2_8 581 # ASSIGN : s_2_9 626 # ASSIGN : s_3_0 79 # ASSIGN : s_3_1 175 # ASSIGN : s_3_2 249 # ASSIGN : s_3_3 406 # ASSIGN : s_3_4 492 # ASSIGN : s_3_5 566 # ASSIGN : s_3_6 640 # ASSIGN : s_3_7 661 # ASSIGN : s_3_8 765 # ASSIGN : s_3_9 835 # ASSIGN : s_4_0 67 # ASSIGN : s_4_1 156 # ASSIGN : s_4_2 259 # ASSIGN : s_4_3 361 # ASSIGN : s_4_4 544 # ASSIGN : s_4_5 606 # ASSIGN : s_4_6 668 # ASSIGN : s_4_7 739 # ASSIGN : s_4_8 779 # ASSIGN : s_4_9 924 # ASSIGN : s_5_0 2 # ASSIGN : s_5_1 111 # ASSIGN : s_5_2 183 # ASSIGN : s_5_3 221 # ASSIGN : s_5_4 318 # ASSIGN : s_5_5 428 # ASSIGN : s_5_6 496 # ASSIGN : s_5_7 546 # ASSIGN : s_5_8 763 # ASSIGN : s_5_9 852 # ASSIGN : s_6_0 106 # ASSIGN : s_6_1 329 # ASSIGN : s_6_2 365 # ASSIGN : s_6_3 465 # ASSIGN : s_6_4 720 # ASSIGN : s_6_5 799 # ASSIGN : s_6_6 858 # ASSIGN : s_6_7 881 # ASSIGN : s_6_8 906 # ASSIGN : s_6_9 923 # ASSIGN : s_7_0 2 # ASSIGN : s_7_1 74 # ASSIGN : s_7_2 82 # ASSIGN : s_7_3 167 # ASSIGN : s_7_4 253 # ASSIGN : s_7_5 337 # ASSIGN : s_7_6 377 # ASSIGN : s_7_7 611 # ASSIGN : s_7_8 759 # ASSIGN : s_7_9 786 # ASSIGN : s_8_0 67 # ASSIGN : s_8_1 104 # ASSIGN : s_8_2 155 # ASSIGN : s_8_3 274 # ASSIGN : s_8_4 325 # ASSIGN : s_8_5 422 # ASSIGN : s_8_6 431 # ASSIGN : s_8_7 525 # ASSIGN : s_8_8 598 # ASSIGN : s_8_9 649 # ASSIGN : s_9_0 15 # ASSIGN : s_9_1 58 # ASSIGN : s_9_2 73 # ASSIGN : s_9_3 156 # ASSIGN : s_9_4 200 # ASSIGN : s_9_5 686 # ASSIGN : s_9_6 702 # ASSIGN : s_9_7 748 # ASSIGN : s_9_8 785 # ASSIGN : s_9_9 840 # ASSIGN : s_10_0 187 # ASSIGN : s_10_1 313 # ASSIGN : s_10_2 363 # ASSIGN : s_10_3 489 # ASSIGN : s_10_4 605 # ASSIGN : s_10_5 616 # ASSIGN : s_10_6 670 # ASSIGN : s_10_7 727 # ASSIGN : s_10_8 772 # ASSIGN : s_10_9 869 # ASSIGN : s_11_0 141 # ASSIGN : s_11_1 201 # ASSIGN : s_11_2 238 # ASSIGN : s_11_3 340 # ASSIGN : s_11_4 610 # ASSIGN : s_11_5 709 # ASSIGN : s_11_6 762 # ASSIGN : s_11_7 781 # ASSIGN : s_11_8 840 # ASSIGN : s_11_9 874 # ASSIGN : s_12_0 31 # ASSIGN : s_12_1 54 # ASSIGN : s_12_2 171 # ASSIGN : s_12_3 311 # ASSIGN : s_12_4 335 # ASSIGN : s_12_5 409 # ASSIGN : s_12_6 538 # ASSIGN : s_12_7 656 # ASSIGN : s_12_8 690 # ASSIGN : s_12_9 884 # ASSIGN : s_13_0 21 # ASSIGN : s_13_1 58 # ASSIGN : s_13_2 113 # ASSIGN : s_13_3 368 # ASSIGN : s_13_4 421 # ASSIGN : s_13_5 517 # ASSIGN : s_13_6 593 # ASSIGN : s_13_7 635 # ASSIGN : s_13_8 785 # ASSIGN : s_13_9 917 # ASSIGN : s_14_0 223 # ASSIGN : s_14_1 411 # ASSIGN : s_14_2 440 # ASSIGN : s_14_3 492 # ASSIGN : s_14_4 683 # ASSIGN : s_14_5 723 # ASSIGN : s_14_6 746 # ASSIGN : s_14_7 825 # ASSIGN : s_14_8 867 # ASSIGN : s_14_9 881 SHOW_RESULT 929 END : 929 (0 seconds) [Thu Jun 1 16:44:44 2006] SHOW_RESULT 929 CPU : 0.569999999999993 = 0.569999999999993 + 0 + 0 + 0 # BOUND : makespan 926 929 MODIFY_CNF 927 BEGIN : [Thu Jun 1 16:44:44 2006] MODIFY_CNF 927 END : 69802283 bytes (0 seconds) [Thu Jun 1 16:44:44 2006] MODIFY_CNF 927 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 927 BEGIN : [Thu Jun 1 16:44:44 2006] CMD : minisat /work/tamura/csp2sat95922.cnf /work/tamura/csp2sat95922.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1190048 3503103 | 396682 0 0 NaNQ | 0.000 % | | 100 | 1190048 3503103 | 436350 100 1442 14.4 | 65.568 % | | 250 | 1190048 3503103 | 479985 250 2639 10.6 | 65.568 % | | 475 | 1190048 3503103 | 527983 475 4507 9.5 | 65.568 % | | 812 | 1190048 3503103 | 580782 812 8273 10.2 | 65.568 % | | 1318 | 1190048 3503103 | 638860 1318 14370 10.9 | 65.568 % | | 2077 | 1190048 3503103 | 702746 2077 23279 11.2 | 65.568 % | | 3216 | 1190048 3503103 | 773020 3216 38368 11.9 | 65.568 % | | 4924 | 1190048 3503103 | 850323 4924 60368 12.3 | 65.568 % | | 7486 | 1190048 3503103 | 935355 7486 99116 13.2 | 65.568 % | | 11330 | 1190048 3503103 | 1028890 11330 158111 14.0 | 65.568 % | | 17096 | 1190048 3503103 | 1131780 17096 258233 15.1 | 65.568 % | | 25745 | 1190048 3503103 | 1244958 25745 418529 16.3 | 65.568 % | ==============================================================================) restarts : 13 conflicts : 32657 (259 /sec) decisions : 44277 (351 /sec) propagations : 229785856 (1823902 /sec) inspects : 2188284494 (17369285 /sec) conflict literals : 560131 (36.09 % deleted) CPU time : 125.986 s SATISFIABLE VERIFY_CNF 927 END : (127 seconds) [Thu Jun 1 16:46:51 2006] VERIFY_CNF 927 CPU : 126.84 = 0 + 0.02 + 126.74 + 0.0800000000000001 # RESULT : makespan 927 SATISFIABLE SHOW_RESULT 927 BEGIN : [Thu Jun 1 16:46:51 2006] # ASSIGN : makespan 927 # ASSIGN : s_0_0 88 # ASSIGN : s_0_1 195 # ASSIGN : s_0_2 466 # ASSIGN : s_0_3 553 # ASSIGN : s_0_4 647 # ASSIGN : s_0_5 685 # ASSIGN : s_0_6 826 # ASSIGN : s_0_7 867 # ASSIGN : s_0_8 897 # ASSIGN : s_0_9 908 # ASSIGN : s_1_0 47 # ASSIGN : s_1_1 153 # ASSIGN : s_1_2 359 # ASSIGN : s_1_3 368 # ASSIGN : s_1_4 382 # ASSIGN : s_1_5 448 # ASSIGN : s_1_6 537 # ASSIGN : s_1_7 622 # ASSIGN : s_1_8 809 # ASSIGN : s_1_9 920 # ASSIGN : s_2_0 3 # ASSIGN : s_2_1 91 # ASSIGN : s_2_2 116 # ASSIGN : s_2_3 150 # ASSIGN : s_2_4 198 # ASSIGN : s_2_5 286 # ASSIGN : s_2_6 484 # ASSIGN : s_2_7 564 # ASSIGN : s_2_8 570 # ASSIGN : s_2_9 615 # ASSIGN : s_3_0 85 # ASSIGN : s_3_1 173 # ASSIGN : s_3_2 247 # ASSIGN : s_3_3 404 # ASSIGN : s_3_4 490 # ASSIGN : s_3_5 564 # ASSIGN : s_3_6 638 # ASSIGN : s_3_7 659 # ASSIGN : s_3_8 781 # ASSIGN : s_3_9 833 # ASSIGN : s_4_0 66 # ASSIGN : s_4_1 154 # ASSIGN : s_4_2 257 # ASSIGN : s_4_3 426 # ASSIGN : s_4_4 542 # ASSIGN : s_4_5 604 # ASSIGN : s_4_6 666 # ASSIGN : s_4_7 761 # ASSIGN : s_4_8 777 # ASSIGN : s_4_9 922 # ASSIGN : s_5_0 0 # ASSIGN : s_5_1 109 # ASSIGN : s_5_2 183 # ASSIGN : s_5_3 227 # ASSIGN : s_5_4 316 # ASSIGN : s_5_5 426 # ASSIGN : s_5_6 494 # ASSIGN : s_5_7 544 # ASSIGN : s_5_8 761 # ASSIGN : s_5_9 850 # ASSIGN : s_6_0 112 # ASSIGN : s_6_1 327 # ASSIGN : s_6_2 363 # ASSIGN : s_6_3 463 # ASSIGN : s_6_4 736 # ASSIGN : s_6_5 785 # ASSIGN : s_6_6 856 # ASSIGN : s_6_7 879 # ASSIGN : s_6_8 904 # ASSIGN : s_6_9 921 # ASSIGN : s_7_0 1 # ASSIGN : s_7_1 72 # ASSIGN : s_7_2 80 # ASSIGN : s_7_3 165 # ASSIGN : s_7_4 251 # ASSIGN : s_7_5 335 # ASSIGN : s_7_6 375 # ASSIGN : s_7_7 609 # ASSIGN : s_7_8 757 # ASSIGN : s_7_9 784 # ASSIGN : s_8_0 51 # ASSIGN : s_8_1 102 # ASSIGN : s_8_2 155 # ASSIGN : s_8_3 280 # ASSIGN : s_8_4 331 # ASSIGN : s_8_5 417 # ASSIGN : s_8_6 429 # ASSIGN : s_8_7 523 # ASSIGN : s_8_8 596 # ASSIGN : s_8_9 647 # ASSIGN : s_9_0 8 # ASSIGN : s_9_1 56 # ASSIGN : s_9_2 71 # ASSIGN : s_9_3 154 # ASSIGN : s_9_4 198 # ASSIGN : s_9_5 675 # ASSIGN : s_9_6 691 # ASSIGN : s_9_7 737 # ASSIGN : s_9_8 790 # ASSIGN : s_9_9 815 # ASSIGN : s_10_0 185 # ASSIGN : s_10_1 311 # ASSIGN : s_10_2 361 # ASSIGN : s_10_3 487 # ASSIGN : s_10_4 608 # ASSIGN : s_10_5 614 # ASSIGN : s_10_6 668 # ASSIGN : s_10_7 725 # ASSIGN : s_10_8 770 # ASSIGN : s_10_9 867 # ASSIGN : s_11_0 139 # ASSIGN : s_11_1 207 # ASSIGN : s_11_2 236 # ASSIGN : s_11_3 347 # ASSIGN : s_11_4 613 # ASSIGN : s_11_5 707 # ASSIGN : s_11_6 760 # ASSIGN : s_11_7 779 # ASSIGN : s_11_8 838 # ASSIGN : s_11_9 872 # ASSIGN : s_12_0 37 # ASSIGN : s_12_1 60 # ASSIGN : s_12_2 169 # ASSIGN : s_12_3 309 # ASSIGN : s_12_4 333 # ASSIGN : s_12_5 407 # ASSIGN : s_12_6 536 # ASSIGN : s_12_7 591 # ASSIGN : s_12_8 688 # ASSIGN : s_12_9 882 # ASSIGN : s_13_0 19 # ASSIGN : s_13_1 56 # ASSIGN : s_13_2 111 # ASSIGN : s_13_3 366 # ASSIGN : s_13_4 410 # ASSIGN : s_13_5 515 # ASSIGN : s_13_6 596 # ASSIGN : s_13_7 633 # ASSIGN : s_13_8 783 # ASSIGN : s_13_9 915 # ASSIGN : s_14_0 221 # ASSIGN : s_14_1 314 # ASSIGN : s_14_2 368 # ASSIGN : s_14_3 481 # ASSIGN : s_14_4 681 # ASSIGN : s_14_5 721 # ASSIGN : s_14_6 744 # ASSIGN : s_14_7 823 # ASSIGN : s_14_8 865 # ASSIGN : s_14_9 879 SHOW_RESULT 927 END : 927 (1 seconds) [Thu Jun 1 16:46:52 2006] SHOW_RESULT 927 CPU : 0.570000000000022 = 0.570000000000022 + 0 + 0 + 0 # BOUND : makespan 926 927 MODIFY_CNF 926 BEGIN : [Thu Jun 1 16:46:52 2006] MODIFY_CNF 926 END : 69802283 bytes (0 seconds) [Thu Jun 1 16:46:52 2006] MODIFY_CNF 926 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 926 BEGIN : [Thu Jun 1 16:46:52 2006] CMD : minisat /work/tamura/csp2sat95922.cnf /work/tamura/csp2sat95922.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1187895 3496795 | 395965 0 0 NaNQ | 0.000 % | | 100 | 1187895 3496795 | 435561 100 1415 14.2 | 65.645 % | | 251 | 1187895 3496795 | 479117 251 3397 13.5 | 65.645 % | | 476 | 1187895 3496795 | 527029 476 5533 11.6 | 65.645 % | | 813 | 1187895 3496795 | 579732 813 9614 11.8 | 65.645 % | | 1320 | 1187895 3496795 | 637705 1320 15999 12.1 | 65.645 % | | 2080 | 1187895 3496795 | 701476 2080 27008 13.0 | 65.645 % | | 3220 | 1187895 3496795 | 771623 3220 40173 12.5 | 65.645 % | | 4928 | 1187895 3496795 | 848786 4928 61390 12.5 | 65.645 % | | 7490 | 1187895 3496795 | 933664 7490 98714 13.2 | 65.645 % | | 11337 | 1187895 3496795 | 1027031 11337 147901 13.0 | 65.645 % | | 17104 | 1187895 3496795 | 1129734 17104 239318 14.0 | 65.645 % | | 25753 | 1187895 3496795 | 1242707 25753 383196 14.9 | 65.645 % | ==============================================================================) restarts : 13 conflicts : 28413 (292 /sec) decisions : 37651 (387 /sec) propagations : 180978262 (1862058 /sec) inspects : 1704327745 (17535575 /sec) conflict literals : 420765 (35.37 % deleted) CPU time : 97.1926 s UNSATISFIABLE VERIFY_CNF 926 END : (98 seconds) [Thu Jun 1 16:48:30 2006] VERIFY_CNF 926 CPU : 97.99 = 0 + 0.01 + 97.91 + 0.0699999999999998 # RESULT : makespan 926 UNSATISFIABLE # BOUND : makespan 927 927 MAIN END : (753 seconds) [Thu Jun 1 16:48:30 2006] MAIN CPU : 750.99 = 151.31 + 0.33 + 598.16 + 1.19