MAIN BEGIN : [Thu Jun 1 04:18:31 2006] READ BEGIN : csp/abz5.csp [Thu Jun 1 04:18:31 2006] READ END : csp/abz5.csp (2 seconds) [Thu Jun 1 04:18:33 2006] READ CPU : 1.41 = 1.4 + 0.01 + 0 + 0 # BOUND : makespan 868 1370 GENERATE_CNF 1370 BEGIN : [Thu Jun 1 04:18:33 2006] GENERATE_CNF 1370 END : 138704 variables 1424661 clauses 32221853 bytes (68 seconds) [Thu Jun 1 04:19:41 2006] GENERATE_CNF 1370 CPU : 68.69 = 68.6 + 0.09 + 0 + 0 MODIFY_CNF 1119 BEGIN : [Thu Jun 1 04:19:41 2006] MODIFY_CNF 1119 END : 32221859 bytes (0 seconds) [Thu Jun 1 04:19:41 2006] MODIFY_CNF 1119 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1119 BEGIN : [Thu Jun 1 04:19:41 2006] CMD : minisat /work/tamura/csp2sat99940.cnf /work/tamura/csp2sat99940.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 384042 1117488 | 128014 0 0 NaNQ | 0.000 % | ==============================================================================) restarts : 1 conflicts : 97 (44 /sec) decisions : 123 (56 /sec) propagations : 684131 (313236 /sec) inspects : 3566699 (1633046 /sec) conflict literals : 440 (20.43 % deleted) CPU time : 2.18408 s UNSATISFIABLE VERIFY_CNF 1119 END : (3 seconds) [Thu Jun 1 04:19:44 2006] VERIFY_CNF 1119 CPU : 2.49 = 0 + 0.01 + 2.46 + 0.02 # RESULT : makespan 1119 UNSATISFIABLE # BOUND : makespan 1120 1370 MODIFY_CNF 1245 BEGIN : [Thu Jun 1 04:19:44 2006] MODIFY_CNF 1245 END : 32221859 bytes (0 seconds) [Thu Jun 1 04:19:44 2006] MODIFY_CNF 1245 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1245 BEGIN : [Thu Jun 1 04:19:44 2006] CMD : minisat /work/tamura/csp2sat99940.cnf /work/tamura/csp2sat99940.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 541614 1577385 | 180538 0 0 NaNQ | 0.000 % | | 100 | 541614 1577385 | 198591 100 974 9.7 | 65.520 % | | 250 | 541614 1577385 | 218450 250 2463 9.9 | 65.520 % | | 475 | 541614 1577385 | 240296 475 4611 9.7 | 65.520 % | | 813 | 541614 1577385 | 264325 813 8352 10.3 | 65.520 % | ==============================================================================) restarts : 5 conflicts : 1288 (265 /sec) decisions : 2096 (432 /sec) propagations : 8339682 (1718756 /sec) inspects : 54140693 (11158053 /sec) conflict literals : 13828 (24.62 % deleted) CPU time : 4.85216 s SATISFIABLE VERIFY_CNF 1245 END : (5 seconds) [Thu Jun 1 04:19:49 2006] VERIFY_CNF 1245 CPU : 5.27 = 0 + 0 + 5.23 + 0.04 # RESULT : makespan 1245 SATISFIABLE SHOW_RESULT 1245 BEGIN : [Thu Jun 1 04:19:49 2006] # ASSIGN : makespan 1245 # ASSIGN : s_0_0 274 # ASSIGN : s_0_1 366 # ASSIGN : s_0_2 441 # ASSIGN : s_0_3 535 # ASSIGN : s_0_4 634 # ASSIGN : s_0_5 701 # ASSIGN : s_0_6 795 # ASSIGN : s_0_7 899 # ASSIGN : s_0_8 1067 # ASSIGN : s_0_9 1153 # ASSIGN : s_1_0 76 # ASSIGN : s_1_1 148 # ASSIGN : s_1_2 293 # ASSIGN : s_1_3 362 # ASSIGN : s_1_4 437 # ASSIGN : s_1_5 599 # ASSIGN : s_1_6 783 # ASSIGN : s_1_7 916 # ASSIGN : s_1_8 998 # ASSIGN : s_1_9 1111 # ASSIGN : s_2_0 106 # ASSIGN : s_2_1 210 # ASSIGN : s_2_2 336 # ASSIGN : s_2_3 419 # ASSIGN : s_2_4 648 # ASSIGN : s_2_5 712 # ASSIGN : s_2_6 821 # ASSIGN : s_2_7 924 # ASSIGN : s_2_8 1021 # ASSIGN : s_2_9 1076 # ASSIGN : s_3_0 19 # ASSIGN : s_3_1 369 # ASSIGN : s_3_2 484 # ASSIGN : s_3_3 569 # ASSIGN : s_3_4 668 # ASSIGN : s_3_5 722 # ASSIGN : s_3_6 797 # ASSIGN : s_3_7 875 # ASSIGN : s_3_8 951 # ASSIGN : s_3_9 1178 # ASSIGN : s_4_0 29 # ASSIGN : s_4_1 101 # ASSIGN : s_4_2 189 # ASSIGN : s_4_3 271 # ASSIGN : s_4_4 504 # ASSIGN : s_4_5 790 # ASSIGN : s_4_6 927 # ASSIGN : s_4_7 1022 # ASSIGN : s_4_8 1092 # ASSIGN : s_4_9 1159 # ASSIGN : s_5_0 64 # ASSIGN : s_5_1 193 # ASSIGN : s_5_2 304 # ASSIGN : s_5_3 368 # ASSIGN : s_5_4 434 # ASSIGN : s_5_5 531 # ASSIGN : s_5_6 664 # ASSIGN : s_5_7 733 # ASSIGN : s_5_8 997 # ASSIGN : s_5_9 1157 # ASSIGN : s_6_0 113 # ASSIGN : s_6_1 163 # ASSIGN : s_6_2 472 # ASSIGN : s_6_3 569 # ASSIGN : s_6_4 665 # ASSIGN : s_6_5 760 # ASSIGN : s_6_6 857 # ASSIGN : s_6_7 923 # ASSIGN : s_6_8 1122 # ASSIGN : s_6_9 1174 # ASSIGN : s_7_0 3 # ASSIGN : s_7_1 125 # ASSIGN : s_7_2 198 # ASSIGN : s_7_3 280 # ASSIGN : s_7_4 331 # ASSIGN : s_7_5 402 # ASSIGN : s_7_6 496 # ASSIGN : s_7_7 603 # ASSIGN : s_7_8 665 # ASSIGN : s_7_9 872 # ASSIGN : s_8_0 96 # ASSIGN : s_8_1 222 # ASSIGN : s_8_2 330 # ASSIGN : s_8_3 411 # ASSIGN : s_8_4 545 # ASSIGN : s_8_5 611 # ASSIGN : s_8_6 787 # ASSIGN : s_8_7 863 # ASSIGN : s_8_8 921 # ASSIGN : s_8_9 1014 # ASSIGN : s_9_0 98 # ASSIGN : s_9_1 190 # ASSIGN : s_9_2 249 # ASSIGN : s_9_3 514 # ASSIGN : s_9_4 581 # ASSIGN : s_9_5 637 # ASSIGN : s_9_6 869 # ASSIGN : s_9_7 1009 # ASSIGN : s_9_8 1090 # ASSIGN : s_9_9 1149 SHOW_RESULT 1245 END : 1245 (1 seconds) [Thu Jun 1 04:19:50 2006] SHOW_RESULT 1245 CPU : 0.399999999999991 = 0.399999999999991 + 0 + 0 + 0 # BOUND : makespan 1120 1245 MODIFY_CNF 1182 BEGIN : [Thu Jun 1 04:19:50 2006] MODIFY_CNF 1182 END : 32221859 bytes (0 seconds) [Thu Jun 1 04:19:50 2006] MODIFY_CNF 1182 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1182 BEGIN : [Thu Jun 1 04:19:50 2006] CMD : minisat /work/tamura/csp2sat99940.cnf /work/tamura/csp2sat99940.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 462865 1347539 | 154288 0 0 NaNQ | 0.000 % | | 100 | 462865 1347539 | 169716 99 652 6.6 | 70.154 % | | 250 | 462865 1347539 | 186688 249 2185 8.8 | 70.154 % | | 476 | 461996 1344933 | 205357 474 3802 8.0 | 70.155 % | ==============================================================================) restarts : 4 conflicts : 620 (185 /sec) decisions : 808 (241 /sec) propagations : 4075350 (1215674 /sec) inspects : 23244027 (6933674 /sec) conflict literals : 4844 (27.54 % deleted) CPU time : 3.35234 s UNSATISFIABLE VERIFY_CNF 1182 END : (3 seconds) [Thu Jun 1 04:19:53 2006] VERIFY_CNF 1182 CPU : 3.7 = 0 + 0.00999999999999998 + 3.65 + 0.04 # RESULT : makespan 1182 UNSATISFIABLE # BOUND : makespan 1183 1245 MODIFY_CNF 1214 BEGIN : [Thu Jun 1 04:19:53 2006] MODIFY_CNF 1214 END : 32221859 bytes (0 seconds) [Thu Jun 1 04:19:53 2006] MODIFY_CNF 1214 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1214 BEGIN : [Thu Jun 1 04:19:53 2006] CMD : minisat /work/tamura/csp2sat99940.cnf /work/tamura/csp2sat99940.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 500779 1458032 | 166926 0 0 NaNQ | 0.000 % | | 100 | 500779 1458032 | 183618 99 947 9.6 | 67.803 % | | 251 | 500779 1458032 | 201980 250 2319 9.3 | 67.803 % | | 477 | 499878 1455330 | 222178 476 4401 9.2 | 67.803 % | | 815 | 499878 1455330 | 244396 814 7486 9.2 | 67.803 % | | 1321 | 497049 1447166 | 268835 1162 10419 9.0 | 68.419 % | ==============================================================================) restarts : 6 conflicts : 1345 (263 /sec) decisions : 1800 (352 /sec) propagations : 9127453 (1782783 /sec) inspects : 54105313 (10567900 /sec) conflict literals : 11918 (29.39 % deleted) CPU time : 5.11978 s UNSATISFIABLE VERIFY_CNF 1214 END : (6 seconds) [Thu Jun 1 04:19:59 2006] VERIFY_CNF 1214 CPU : 5.57 = 0 + 0 + 5.44 + 0.13 # RESULT : makespan 1214 UNSATISFIABLE # BOUND : makespan 1215 1245 MODIFY_CNF 1230 BEGIN : [Thu Jun 1 04:19:59 2006] MODIFY_CNF 1230 END : 32221859 bytes (0 seconds) [Thu Jun 1 04:19:59 2006] MODIFY_CNF 1230 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1230 BEGIN : [Thu Jun 1 04:19:59 2006] CMD : minisat /work/tamura/csp2sat99940.cnf /work/tamura/csp2sat99940.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 521961 1519952 | 173987 0 0 NaNQ | 0.000 % | | 100 | 521961 1519952 | 191385 99 971 9.8 | 66.625 % | | 252 | 521961 1519952 | 210524 251 2096 8.4 | 66.625 % | | 477 | 521044 1517202 | 231576 469 4373 9.3 | 66.625 % | | 814 | 521044 1517202 | 254734 806 7340 9.1 | 66.625 % | | 1320 | 521044 1517202 | 280207 1312 12830 9.8 | 66.625 % | | 2079 | 521044 1517202 | 308228 2071 21014 10.1 | 66.625 % | ==============================================================================) restarts : 7 conflicts : 2496 (331 /sec) decisions : 3486 (462 /sec) propagations : 16046622 (2125121 /sec) inspects : 97522324 (12915290 /sec) conflict literals : 24750 (30.78 % deleted) CPU time : 7.55092 s UNSATISFIABLE VERIFY_CNF 1230 END : (8 seconds) [Thu Jun 1 04:20:07 2006] VERIFY_CNF 1230 CPU : 7.92 = 0.0100000000000051 + 0.01 + 7.87 + 0.03 # RESULT : makespan 1230 UNSATISFIABLE # BOUND : makespan 1231 1245 MODIFY_CNF 1238 BEGIN : [Thu Jun 1 04:20:07 2006] MODIFY_CNF 1238 END : 32221859 bytes (0 seconds) [Thu Jun 1 04:20:07 2006] MODIFY_CNF 1238 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1238 BEGIN : [Thu Jun 1 04:20:07 2006] CMD : minisat /work/tamura/csp2sat99940.cnf /work/tamura/csp2sat99940.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 532186 1549814 | 177395 0 0 NaNQ | 0.000 % | | 100 | 532186 1549814 | 195134 99 998 10.1 | 66.037 % | | 250 | 532186 1549814 | 214647 249 2594 10.4 | 66.037 % | | 477 | 532186 1549814 | 236112 476 4500 9.5 | 66.037 % | | 814 | 531261 1547040 | 259724 798 8966 11.2 | 66.037 % | | 1321 | 531261 1547040 | 285696 1305 14269 10.9 | 66.037 % | ==============================================================================) restarts : 6 conflicts : 1848 (285 /sec) decisions : 2719 (420 /sec) propagations : 12883655 (1988824 /sec) inspects : 81998432 (12657935 /sec) conflict literals : 20008 (29.78 % deleted) CPU time : 6.47803 s SATISFIABLE VERIFY_CNF 1238 END : (7 seconds) [Thu Jun 1 04:20:14 2006] VERIFY_CNF 1238 CPU : 6.92 = 0 + 0.01 + 6.86 + 0.05 # RESULT : makespan 1238 SATISFIABLE SHOW_RESULT 1238 BEGIN : [Thu Jun 1 04:20:14 2006] # ASSIGN : makespan 1238 # ASSIGN : s_0_0 271 # ASSIGN : s_0_1 393 # ASSIGN : s_0_2 501 # ASSIGN : s_0_3 598 # ASSIGN : s_0_4 711 # ASSIGN : s_0_5 778 # ASSIGN : s_0_6 867 # ASSIGN : s_0_7 961 # ASSIGN : s_0_8 1060 # ASSIGN : s_0_9 1146 # ASSIGN : s_1_0 53 # ASSIGN : s_1_1 125 # ASSIGN : s_1_2 178 # ASSIGN : s_1_3 359 # ASSIGN : s_1_4 434 # ASSIGN : s_1_5 841 # ASSIGN : s_1_6 907 # ASSIGN : s_1_7 999 # ASSIGN : s_1_8 1081 # ASSIGN : s_1_9 1175 # ASSIGN : s_2_0 16 # ASSIGN : s_2_1 99 # ASSIGN : s_2_2 160 # ASSIGN : s_2_3 243 # ASSIGN : s_2_4 371 # ASSIGN : s_2_5 513 # ASSIGN : s_2_6 816 # ASSIGN : s_2_7 917 # ASSIGN : s_2_8 1014 # ASSIGN : s_2_9 1069 # ASSIGN : s_3_0 272 # ASSIGN : s_3_1 366 # ASSIGN : s_3_2 476 # ASSIGN : s_3_3 537 # ASSIGN : s_3_4 636 # ASSIGN : s_3_5 690 # ASSIGN : s_3_6 765 # ASSIGN : s_3_7 831 # ASSIGN : s_3_8 944 # ASSIGN : s_3_9 1171 # ASSIGN : s_4_0 33 # ASSIGN : s_4_1 102 # ASSIGN : s_4_2 216 # ASSIGN : s_4_3 298 # ASSIGN : s_4_4 429 # ASSIGN : s_4_5 528 # ASSIGN : s_4_6 595 # ASSIGN : s_4_7 697 # ASSIGN : s_4_8 894 # ASSIGN : s_4_9 1152 # ASSIGN : s_5_0 58 # ASSIGN : s_5_1 190 # ASSIGN : s_5_2 326 # ASSIGN : s_5_3 435 # ASSIGN : s_5_4 528 # ASSIGN : s_5_5 608 # ASSIGN : s_5_6 736 # ASSIGN : s_5_7 805 # ASSIGN : s_5_8 990 # ASSIGN : s_5_9 1150 # ASSIGN : s_6_0 107 # ASSIGN : s_6_1 157 # ASSIGN : s_6_2 440 # ASSIGN : s_6_3 540 # ASSIGN : s_6_4 649 # ASSIGN : s_6_5 744 # ASSIGN : s_6_6 887 # ASSIGN : s_6_7 953 # ASSIGN : s_6_8 1052 # ASSIGN : s_6_9 1104 # ASSIGN : s_7_0 4 # ASSIGN : s_7_1 102 # ASSIGN : s_7_2 175 # ASSIGN : s_7_3 257 # ASSIGN : s_7_4 308 # ASSIGN : s_7_5 390 # ASSIGN : s_7_6 484 # ASSIGN : s_7_7 569 # ASSIGN : s_7_8 631 # ASSIGN : s_7_9 726 # ASSIGN : s_8_0 66 # ASSIGN : s_8_1 247 # ASSIGN : s_8_2 318 # ASSIGN : s_8_3 399 # ASSIGN : s_8_4 622 # ASSIGN : s_8_5 688 # ASSIGN : s_8_6 780 # ASSIGN : s_8_7 856 # ASSIGN : s_8_8 914 # ASSIGN : s_8_9 1007 # ASSIGN : s_9_0 268 # ASSIGN : s_9_1 320 # ASSIGN : s_9_2 379 # ASSIGN : s_9_3 461 # ASSIGN : s_9_4 574 # ASSIGN : s_9_5 630 # ASSIGN : s_9_6 944 # ASSIGN : s_9_7 1002 # ASSIGN : s_9_8 1083 # ASSIGN : s_9_9 1142 SHOW_RESULT 1238 END : 1238 (0 seconds) [Thu Jun 1 04:20:14 2006] SHOW_RESULT 1238 CPU : 0.390000000000001 = 0.390000000000001 + 0 + 0 + 0 # BOUND : makespan 1231 1238 MODIFY_CNF 1234 BEGIN : [Thu Jun 1 04:20:14 2006] MODIFY_CNF 1234 END : 32221859 bytes (0 seconds) [Thu Jun 1 04:20:14 2006] MODIFY_CNF 1234 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1234 BEGIN : [Thu Jun 1 04:20:14 2006] CMD : minisat /work/tamura/csp2sat99940.cnf /work/tamura/csp2sat99940.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 526180 1532204 | 175393 0 0 NaNQ | 0.000 % | | 102 | 526180 1532204 | 192932 101 1095 10.8 | 66.333 % | | 252 | 526180 1532204 | 212225 251 2456 9.8 | 66.333 % | | 477 | 525259 1529442 | 233448 476 4612 9.7 | 66.333 % | | 814 | 525259 1529442 | 256792 813 7763 9.5 | 66.333 % | | 1320 | 525259 1529442 | 282472 1319 13252 10.0 | 66.333 % | | 2079 | 521474 1518411 | 310719 1808 18344 10.1 | 66.563 % | ==============================================================================) restarts : 7 conflicts : 2956 (341 /sec) decisions : 4206 (485 /sec) propagations : 19172826 (2213098 /sec) inspects : 120391280 (13896631 /sec) conflict literals : 31194 (30.38 % deleted) CPU time : 8.66334 s SATISFIABLE VERIFY_CNF 1234 END : (10 seconds) [Thu Jun 1 04:20:24 2006] VERIFY_CNF 1234 CPU : 9.07 = 0 + 0 + 9.03 + 0.04 # RESULT : makespan 1234 SATISFIABLE SHOW_RESULT 1234 BEGIN : [Thu Jun 1 04:20:24 2006] # ASSIGN : makespan 1234 # ASSIGN : s_0_0 267 # ASSIGN : s_0_1 389 # ASSIGN : s_0_2 497 # ASSIGN : s_0_3 594 # ASSIGN : s_0_4 707 # ASSIGN : s_0_5 774 # ASSIGN : s_0_6 863 # ASSIGN : s_0_7 957 # ASSIGN : s_0_8 1056 # ASSIGN : s_0_9 1142 # ASSIGN : s_1_0 49 # ASSIGN : s_1_1 121 # ASSIGN : s_1_2 174 # ASSIGN : s_1_3 355 # ASSIGN : s_1_4 430 # ASSIGN : s_1_5 837 # ASSIGN : s_1_6 903 # ASSIGN : s_1_7 995 # ASSIGN : s_1_8 1077 # ASSIGN : s_1_9 1171 # ASSIGN : s_2_0 12 # ASSIGN : s_2_1 95 # ASSIGN : s_2_2 156 # ASSIGN : s_2_3 239 # ASSIGN : s_2_4 367 # ASSIGN : s_2_5 509 # ASSIGN : s_2_6 812 # ASSIGN : s_2_7 913 # ASSIGN : s_2_8 1010 # ASSIGN : s_2_9 1065 # ASSIGN : s_3_0 268 # ASSIGN : s_3_1 362 # ASSIGN : s_3_2 472 # ASSIGN : s_3_3 533 # ASSIGN : s_3_4 632 # ASSIGN : s_3_5 686 # ASSIGN : s_3_6 761 # ASSIGN : s_3_7 827 # ASSIGN : s_3_8 940 # ASSIGN : s_3_9 1167 # ASSIGN : s_4_0 29 # ASSIGN : s_4_1 98 # ASSIGN : s_4_2 212 # ASSIGN : s_4_3 294 # ASSIGN : s_4_4 425 # ASSIGN : s_4_5 524 # ASSIGN : s_4_6 591 # ASSIGN : s_4_7 693 # ASSIGN : s_4_8 890 # ASSIGN : s_4_9 1148 # ASSIGN : s_5_0 54 # ASSIGN : s_5_1 186 # ASSIGN : s_5_2 322 # ASSIGN : s_5_3 431 # ASSIGN : s_5_4 524 # ASSIGN : s_5_5 604 # ASSIGN : s_5_6 732 # ASSIGN : s_5_7 801 # ASSIGN : s_5_8 986 # ASSIGN : s_5_9 1146 # ASSIGN : s_6_0 103 # ASSIGN : s_6_1 153 # ASSIGN : s_6_2 436 # ASSIGN : s_6_3 536 # ASSIGN : s_6_4 645 # ASSIGN : s_6_5 740 # ASSIGN : s_6_6 883 # ASSIGN : s_6_7 949 # ASSIGN : s_6_8 1048 # ASSIGN : s_6_9 1100 # ASSIGN : s_7_0 0 # ASSIGN : s_7_1 98 # ASSIGN : s_7_2 171 # ASSIGN : s_7_3 253 # ASSIGN : s_7_4 304 # ASSIGN : s_7_5 386 # ASSIGN : s_7_6 480 # ASSIGN : s_7_7 565 # ASSIGN : s_7_8 627 # ASSIGN : s_7_9 722 # ASSIGN : s_8_0 62 # ASSIGN : s_8_1 243 # ASSIGN : s_8_2 314 # ASSIGN : s_8_3 395 # ASSIGN : s_8_4 618 # ASSIGN : s_8_5 684 # ASSIGN : s_8_6 776 # ASSIGN : s_8_7 852 # ASSIGN : s_8_8 910 # ASSIGN : s_8_9 1003 # ASSIGN : s_9_0 264 # ASSIGN : s_9_1 316 # ASSIGN : s_9_2 375 # ASSIGN : s_9_3 457 # ASSIGN : s_9_4 570 # ASSIGN : s_9_5 626 # ASSIGN : s_9_6 940 # ASSIGN : s_9_7 998 # ASSIGN : s_9_8 1079 # ASSIGN : s_9_9 1138 SHOW_RESULT 1234 END : 1234 (0 seconds) [Thu Jun 1 04:20:24 2006] SHOW_RESULT 1234 CPU : 0.410000000000006 = 0.400000000000006 + 0.00999999999999998 + 0 + 0 # BOUND : makespan 1231 1234 MODIFY_CNF 1232 BEGIN : [Thu Jun 1 04:20:24 2006] MODIFY_CNF 1232 END : 32221859 bytes (0 seconds) [Thu Jun 1 04:20:24 2006] MODIFY_CNF 1232 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1232 BEGIN : [Thu Jun 1 04:20:24 2006] CMD : minisat /work/tamura/csp2sat99940.cnf /work/tamura/csp2sat99940.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 524512 1527402 | 174837 0 0 NaNQ | 0.000 % | | 101 | 524512 1527402 | 192320 101 1101 10.9 | 66.477 % | | 251 | 524512 1527402 | 211552 251 2631 10.5 | 66.477 % | | 479 | 524512 1527402 | 232708 479 4845 10.1 | 66.477 % | | 816 | 524512 1527402 | 255978 816 8779 10.8 | 66.477 % | | 1322 | 524512 1527402 | 281576 1322 14134 10.7 | 66.477 % | | 2083 | 518606 1510230 | 309734 1657 18948 11.4 | 66.870 % | ==============================================================================) restarts : 7 conflicts : 3217 (331 /sec) decisions : 4289 (442 /sec) propagations : 22082528 (2275081 /sec) inspects : 136304423 (14042938 /sec) conflict literals : 35134 (31.60 % deleted) CPU time : 9.70626 s UNSATISFIABLE VERIFY_CNF 1232 END : (10 seconds) [Thu Jun 1 04:20:34 2006] VERIFY_CNF 1232 CPU : 10.11 = 0.0100000000000051 + 0 + 9.98 + 0.12 # RESULT : makespan 1232 UNSATISFIABLE # BOUND : makespan 1233 1234 MODIFY_CNF 1233 BEGIN : [Thu Jun 1 04:20:34 2006] MODIFY_CNF 1233 END : 32221859 bytes (0 seconds) [Thu Jun 1 04:20:34 2006] MODIFY_CNF 1233 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1233 BEGIN : [Thu Jun 1 04:20:34 2006] CMD : minisat /work/tamura/csp2sat99940.cnf /work/tamura/csp2sat99940.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 525346 1529803 | 175115 0 0 NaNQ | 0.000 % | | 100 | 525346 1529803 | 192626 100 1116 11.2 | 66.404 % | | 250 | 525346 1529803 | 211889 250 2522 10.1 | 66.404 % | | 475 | 525346 1529803 | 233078 475 4392 9.2 | 66.404 % | | 814 | 525346 1529803 | 256385 814 7636 9.4 | 66.404 % | | 1320 | 524750 1528016 | 282024 1201 11308 9.4 | 66.405 % | | 2080 | 524750 1528016 | 310226 1961 20445 10.4 | 66.405 % | | 3220 | 484628 1410113 | 341249 2526 25653 10.2 | 68.395 % | ==============================================================================) restarts : 8 conflicts : 3368 (343 /sec) decisions : 4587 (467 /sec) propagations : 22753133 (2315444 /sec) inspects : 138952577 (14140337 /sec) conflict literals : 33388 (33.57 % deleted) CPU time : 9.82668 s UNSATISFIABLE VERIFY_CNF 1233 END : (10 seconds) [Thu Jun 1 04:20:44 2006] VERIFY_CNF 1233 CPU : 10.29 = 0 + 0.01 + 10.16 + 0.12 # RESULT : makespan 1233 UNSATISFIABLE # BOUND : makespan 1234 1234 MAIN END : (133 seconds) [Thu Jun 1 04:20:44 2006] MAIN CPU : 132.66 = 71.23 + 0.16 + 60.68 + 0.59