MAIN BEGIN : [Sat Jun 3 12:46:54 2006] READ BEGIN : csp/tai09.csp [Sat Jun 3 12:46:54 2006] READ END : csp/tai09.csp (4 seconds) [Sat Jun 3 12:46:58 2006] READ CPU : 4.47 = 4.47 + 0 + 0 + 0 # BOUND : makespan 982 1709 GENERATE_CNF 1709 BEGIN : [Sat Jun 3 12:46:58 2006] GENERATE_CNF 1709 END : 389079 variables 5970771 clauses 142757213 bytes (293 seconds) [Sat Jun 3 12:51:51 2006] GENERATE_CNF 1709 CPU : 292.51 = 292.09 + 0.42 + 0 + 0 MODIFY_CNF 1345 BEGIN : [Sat Jun 3 12:51:51 2006] MODIFY_CNF 1345 END : 142757219 bytes (0 seconds) [Sat Jun 3 12:51:51 2006] MODIFY_CNF 1345 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1345 BEGIN : [Sat Jun 3 12:51:51 2006] CMD : minisat /work/tamura/csp2sat69982.cnf /work/tamura/csp2sat69982.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 2148102 6317451 | 716034 0 0 NaNQ | 0.000 % | | 101 | 2148102 6317451 | 787637 101 1163 11.5 | 67.058 % | | 251 | 2148102 6317451 | 866401 251 3673 14.6 | 67.058 % | | 476 | 2148102 6317451 | 953041 476 8518 17.9 | 67.058 % | ==============================================================================) restarts : 4 conflicts : 763 (53 /sec) decisions : 1652 (114 /sec) propagations : 10266763 (709450 /sec) inspects : 100104423 (6917379 /sec) conflict literals : 15325 (29.55 % deleted) CPU time : 14.4714 s SATISFIABLE VERIFY_CNF 1345 END : (17 seconds) [Sat Jun 3 12:52:08 2006] VERIFY_CNF 1345 CPU : 16.04 = 0.00999999999999091 + 0.01 + 15.89 + 0.13 # RESULT : makespan 1345 SATISFIABLE SHOW_RESULT 1345 BEGIN : [Sat Jun 3 12:52:08 2006] # ASSIGN : makespan 1345 # ASSIGN : s_0_0 26 # ASSIGN : s_0_1 117 # ASSIGN : s_0_2 233 # ASSIGN : s_0_3 418 # ASSIGN : s_0_4 444 # ASSIGN : s_0_5 534 # ASSIGN : s_0_6 587 # ASSIGN : s_0_7 594 # ASSIGN : s_0_8 672 # ASSIGN : s_0_9 821 # ASSIGN : s_0_10 829 # ASSIGN : s_0_11 848 # ASSIGN : s_0_12 904 # ASSIGN : s_0_13 1032 # ASSIGN : s_0_14 1098 # ASSIGN : s_1_0 19 # ASSIGN : s_1_1 90 # ASSIGN : s_1_2 93 # ASSIGN : s_1_3 301 # ASSIGN : s_1_4 375 # ASSIGN : s_1_5 425 # ASSIGN : s_1_6 498 # ASSIGN : s_1_7 603 # ASSIGN : s_1_8 774 # ASSIGN : s_1_9 895 # ASSIGN : s_1_10 973 # ASSIGN : s_1_11 1103 # ASSIGN : s_1_12 1193 # ASSIGN : s_1_13 1257 # ASSIGN : s_1_14 1342 # ASSIGN : s_2_0 87 # ASSIGN : s_2_1 363 # ASSIGN : s_2_2 461 # ASSIGN : s_2_3 543 # ASSIGN : s_2_4 599 # ASSIGN : s_2_5 678 # ASSIGN : s_2_6 747 # ASSIGN : s_2_7 842 # ASSIGN : s_2_8 883 # ASSIGN : s_2_9 922 # ASSIGN : s_2_10 938 # ASSIGN : s_2_11 940 # ASSIGN : s_2_12 1011 # ASSIGN : s_2_13 1038 # ASSIGN : s_2_14 1158 # ASSIGN : s_3_0 133 # ASSIGN : s_3_1 183 # ASSIGN : s_3_2 188 # ASSIGN : s_3_3 287 # ASSIGN : s_3_4 386 # ASSIGN : s_3_5 601 # ASSIGN : s_3_6 621 # ASSIGN : s_3_7 683 # ASSIGN : s_3_8 716 # ASSIGN : s_3_9 795 # ASSIGN : s_3_10 851 # ASSIGN : s_3_11 963 # ASSIGN : s_3_12 1073 # ASSIGN : s_3_13 1129 # ASSIGN : s_3_14 1196 # ASSIGN : s_4_0 46 # ASSIGN : s_4_1 192 # ASSIGN : s_4_2 207 # ASSIGN : s_4_3 419 # ASSIGN : s_4_4 545 # ASSIGN : s_4_5 553 # ASSIGN : s_4_6 634 # ASSIGN : s_4_7 720 # ASSIGN : s_4_8 772 # ASSIGN : s_4_9 854 # ASSIGN : s_4_10 1003 # ASSIGN : s_4_11 1115 # ASSIGN : s_4_12 1203 # ASSIGN : s_4_13 1247 # ASSIGN : s_4_14 1327 # ASSIGN : s_5_0 1 # ASSIGN : s_5_1 80 # ASSIGN : s_5_2 184 # ASSIGN : s_5_3 278 # ASSIGN : s_5_4 287 # ASSIGN : s_5_5 660 # ASSIGN : s_5_6 765 # ASSIGN : s_5_7 777 # ASSIGN : s_5_8 861 # ASSIGN : s_5_9 916 # ASSIGN : s_5_10 986 # ASSIGN : s_5_11 1025 # ASSIGN : s_5_12 1039 # ASSIGN : s_5_13 1042 # ASSIGN : s_5_14 1096 # ASSIGN : s_6_0 359 # ASSIGN : s_6_1 401 # ASSIGN : s_6_2 492 # ASSIGN : s_6_3 534 # ASSIGN : s_6_4 626 # ASSIGN : s_6_5 663 # ASSIGN : s_6_6 688 # ASSIGN : s_6_7 766 # ASSIGN : s_6_8 886 # ASSIGN : s_6_9 902 # ASSIGN : s_6_10 1068 # ASSIGN : s_6_11 1110 # ASSIGN : s_6_12 1190 # ASSIGN : s_6_13 1224 # ASSIGN : s_6_14 1316 # ASSIGN : s_7_0 464 # ASSIGN : s_7_1 560 # ASSIGN : s_7_2 585 # ASSIGN : s_7_3 652 # ASSIGN : s_7_4 719 # ASSIGN : s_7_5 823 # ASSIGN : s_7_6 843 # ASSIGN : s_7_7 895 # ASSIGN : s_7_8 981 # ASSIGN : s_7_9 1067 # ASSIGN : s_7_10 1102 # ASSIGN : s_7_11 1140 # ASSIGN : s_7_12 1158 # ASSIGN : s_7_13 1201 # ASSIGN : s_7_14 1247 # ASSIGN : s_8_0 214 # ASSIGN : s_8_1 292 # ASSIGN : s_8_2 376 # ASSIGN : s_8_3 379 # ASSIGN : s_8_4 477 # ASSIGN : s_8_5 545 # ASSIGN : s_8_6 570 # ASSIGN : s_8_7 599 # ASSIGN : s_8_8 749 # ASSIGN : s_8_9 898 # ASSIGN : s_8_10 918 # ASSIGN : s_8_11 1018 # ASSIGN : s_8_12 1173 # ASSIGN : s_8_13 1241 # ASSIGN : s_8_14 1304 # ASSIGN : s_9_0 61 # ASSIGN : s_9_1 91 # ASSIGN : s_9_2 143 # ASSIGN : s_9_3 223 # ASSIGN : s_9_4 392 # ASSIGN : s_9_5 406 # ASSIGN : s_9_6 412 # ASSIGN : s_9_7 448 # ASSIGN : s_9_8 536 # ASSIGN : s_9_9 621 # ASSIGN : s_9_10 683 # ASSIGN : s_9_11 1029 # ASSIGN : s_9_12 1061 # ASSIGN : s_9_13 1077 # ASSIGN : s_9_14 1338 # ASSIGN : s_10_0 21 # ASSIGN : s_10_1 39 # ASSIGN : s_10_2 129 # ASSIGN : s_10_3 184 # ASSIGN : s_10_4 209 # ASSIGN : s_10_5 281 # ASSIGN : s_10_6 373 # ASSIGN : s_10_7 467 # ASSIGN : s_10_8 589 # ASSIGN : s_10_9 748 # ASSIGN : s_10_10 831 # ASSIGN : s_10_11 889 # ASSIGN : s_10_12 924 # ASSIGN : s_10_13 1198 # ASSIGN : s_10_14 1259 # ASSIGN : s_11_0 3 # ASSIGN : s_11_1 53 # ASSIGN : s_11_2 126 # ASSIGN : s_11_3 221 # ASSIGN : s_11_4 278 # ASSIGN : s_11_5 303 # ASSIGN : s_11_6 376 # ASSIGN : s_11_7 394 # ASSIGN : s_11_8 398 # ASSIGN : s_11_9 680 # ASSIGN : s_11_10 874 # ASSIGN : s_11_11 942 # ASSIGN : s_11_12 979 # ASSIGN : s_11_13 1021 # ASSIGN : s_11_14 1221 # ASSIGN : s_12_0 78 # ASSIGN : s_12_1 134 # ASSIGN : s_12_2 175 # ASSIGN : s_12_3 188 # ASSIGN : s_12_4 263 # ASSIGN : s_12_5 294 # ASSIGN : s_12_6 360 # ASSIGN : s_12_7 432 # ASSIGN : s_12_8 505 # ASSIGN : s_12_9 607 # ASSIGN : s_12_10 687 # ASSIGN : s_12_11 746 # ASSIGN : s_12_12 799 # ASSIGN : s_12_13 1257 # ASSIGN : s_12_14 1307 # ASSIGN : s_13_0 7 # ASSIGN : s_13_1 98 # ASSIGN : s_13_2 217 # ASSIGN : s_13_3 253 # ASSIGN : s_13_4 303 # ASSIGN : s_13_5 452 # ASSIGN : s_13_6 467 # ASSIGN : s_13_7 498 # ASSIGN : s_13_8 678 # ASSIGN : s_13_9 934 # ASSIGN : s_13_10 989 # ASSIGN : s_13_11 1167 # ASSIGN : s_13_12 1190 # ASSIGN : s_13_13 1209 # ASSIGN : s_13_14 1252 # ASSIGN : s_14_0 132 # ASSIGN : s_14_1 247 # ASSIGN : s_14_2 293 # ASSIGN : s_14_3 368 # ASSIGN : s_14_4 440 # ASSIGN : s_14_5 512 # ASSIGN : s_14_6 518 # ASSIGN : s_14_7 723 # ASSIGN : s_14_8 939 # ASSIGN : s_14_9 963 # ASSIGN : s_14_10 1007 # ASSIGN : s_14_11 1020 # ASSIGN : s_14_12 1133 # ASSIGN : s_14_13 1232 # ASSIGN : s_14_14 1242 SHOW_RESULT 1345 END : 1345 (1 seconds) [Sat Jun 3 12:52:09 2006] SHOW_RESULT 1345 CPU : 1.06 = 1.06 + 0 + 0 + 0 # BOUND : makespan 982 1345 MODIFY_CNF 1163 BEGIN : [Sat Jun 3 12:52:09 2006] MODIFY_CNF 1163 END : 142757219 bytes (0 seconds) [Sat Jun 3 12:52:09 2006] MODIFY_CNF 1163 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1163 BEGIN : [Sat Jun 3 12:52:09 2006] CMD : minisat /work/tamura/csp2sat69982.cnf /work/tamura/csp2sat69982.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1364852 4009221 | 454950 0 0 NaNQ | 0.000 % | | 100 | 1364852 4009221 | 500445 92 539 5.9 | 80.906 % | ==============================================================================) restarts : 2 conflicts : 102 (11 /sec) decisions : 131 (14 /sec) propagations : 1467521 (154216 /sec) inspects : 8936806 (939136 /sec) conflict literals : 548 (24.62 % deleted) CPU time : 9.51599 s UNSATISFIABLE VERIFY_CNF 1163 END : (11 seconds) [Sat Jun 3 12:52:20 2006] VERIFY_CNF 1163 CPU : 11.06 = 0 + 0.03 + 10.51 + 0.52 # RESULT : makespan 1163 UNSATISFIABLE # BOUND : makespan 1164 1345 MODIFY_CNF 1254 BEGIN : [Sat Jun 3 12:52:20 2006] MODIFY_CNF 1254 END : 142757219 bytes (0 seconds) [Sat Jun 3 12:52:20 2006] MODIFY_CNF 1254 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1254 BEGIN : [Sat Jun 3 12:52:20 2006] CMD : minisat /work/tamura/csp2sat69982.cnf /work/tamura/csp2sat69982.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1762919 5182614 | 587639 0 0 NaNQ | 0.000 % | | 101 | 1762919 5182614 | 646402 101 1275 12.6 | 72.406 % | | 252 | 1762919 5182614 | 711043 250 2483 9.9 | 72.445 % | | 479 | 1762919 5182614 | 782147 477 6923 14.5 | 72.445 % | | 817 | 1757964 5167898 | 860362 755 10619 14.1 | 72.445 % | | 1325 | 1757964 5167898 | 946398 1263 17684 14.0 | 72.445 % | | 2085 | 1757964 5167898 | 1041038 2023 30472 15.1 | 72.445 % | | 3226 | 1757964 5167898 | 1145142 3164 46733 14.8 | 72.445 % | | 4934 | 1756756 5164276 | 1259656 4166 60489 14.5 | 72.449 % | | 7496 | 1755887 5161680 | 1385622 6727 105100 15.6 | 72.449 % | ==============================================================================) restarts : 10 conflicts : 8691 (121 /sec) decisions : 12110 (169 /sec) propagations : 117361909 (1636514 /sec) inspects : 909827890 (12686790 /sec) conflict literals : 140570 (37.32 % deleted) CPU time : 71.7146 s UNSATISFIABLE VERIFY_CNF 1254 END : (73 seconds) [Sat Jun 3 12:53:33 2006] VERIFY_CNF 1254 CPU : 72.92 = 0 + 0.02 + 72.76 + 0.14 # RESULT : makespan 1254 UNSATISFIABLE # BOUND : makespan 1255 1345 MODIFY_CNF 1300 BEGIN : [Sat Jun 3 12:53:33 2006] MODIFY_CNF 1300 END : 142757219 bytes (0 seconds) [Sat Jun 3 12:53:33 2006] MODIFY_CNF 1300 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1300 BEGIN : [Sat Jun 3 12:53:33 2006] CMD : minisat /work/tamura/csp2sat69982.cnf /work/tamura/csp2sat69982.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1960681 5765423 | 653560 0 0 NaNQ | 0.000 % | | 100 | 1960681 5765423 | 718916 100 1442 14.4 | 69.698 % | | 250 | 1960681 5765423 | 790807 250 3442 13.8 | 69.698 % | | 475 | 1960681 5765423 | 869888 475 6529 13.7 | 69.698 % | | 813 | 1960681 5765423 | 956877 813 13093 16.1 | 69.698 % | | 1320 | 1960681 5765423 | 1052564 1320 23721 18.0 | 69.698 % | | 2079 | 1960681 5765423 | 1157821 2079 36036 17.3 | 69.698 % | | 3218 | 1960681 5765423 | 1273603 3218 56620 17.6 | 69.698 % | | 4926 | 1960030 5763471 | 1400963 4323 74388 17.2 | 69.699 % | | 7489 | 1960030 5763471 | 1541060 6886 118184 17.2 | 69.699 % | ==============================================================================) restarts : 10 conflicts : 10056 (119 /sec) decisions : 14996 (178 /sec) propagations : 134251540 (1595008 /sec) inspects : 1171982016 (13924020 /sec) conflict literals : 193789 (35.62 % deleted) CPU time : 84.1698 s SATISFIABLE VERIFY_CNF 1300 END : (86 seconds) [Sat Jun 3 12:54:59 2006] VERIFY_CNF 1300 CPU : 86.05 = 0 + 0.02 + 85.51 + 0.52 # RESULT : makespan 1300 SATISFIABLE SHOW_RESULT 1300 BEGIN : [Sat Jun 3 12:54:59 2006] # ASSIGN : makespan 1300 # ASSIGN : s_0_0 24 # ASSIGN : s_0_1 115 # ASSIGN : s_0_2 132 # ASSIGN : s_0_3 177 # ASSIGN : s_0_4 251 # ASSIGN : s_0_5 400 # ASSIGN : s_0_6 453 # ASSIGN : s_0_7 460 # ASSIGN : s_0_8 538 # ASSIGN : s_0_9 632 # ASSIGN : s_0_10 710 # ASSIGN : s_0_11 729 # ASSIGN : s_0_12 785 # ASSIGN : s_0_13 1043 # ASSIGN : s_0_14 1109 # ASSIGN : s_1_0 230 # ASSIGN : s_1_1 346 # ASSIGN : s_1_2 372 # ASSIGN : s_1_3 412 # ASSIGN : s_1_4 487 # ASSIGN : s_1_5 530 # ASSIGN : s_1_6 603 # ASSIGN : s_1_7 699 # ASSIGN : s_1_8 779 # ASSIGN : s_1_9 866 # ASSIGN : s_1_10 985 # ASSIGN : s_1_11 1073 # ASSIGN : s_1_12 1163 # ASSIGN : s_1_13 1212 # ASSIGN : s_1_14 1297 # ASSIGN : s_2_0 92 # ASSIGN : s_2_1 180 # ASSIGN : s_2_2 280 # ASSIGN : s_2_3 362 # ASSIGN : s_2_4 476 # ASSIGN : s_2_5 555 # ASSIGN : s_2_6 624 # ASSIGN : s_2_7 719 # ASSIGN : s_2_8 760 # ASSIGN : s_2_9 799 # ASSIGN : s_2_10 811 # ASSIGN : s_2_11 813 # ASSIGN : s_2_12 885 # ASSIGN : s_2_13 944 # ASSIGN : s_2_14 1051 # ASSIGN : s_3_0 19 # ASSIGN : s_3_1 230 # ASSIGN : s_3_2 275 # ASSIGN : s_3_3 326 # ASSIGN : s_3_4 398 # ASSIGN : s_3_5 447 # ASSIGN : s_3_6 467 # ASSIGN : s_3_7 529 # ASSIGN : s_3_8 563 # ASSIGN : s_3_9 729 # ASSIGN : s_3_10 790 # ASSIGN : s_3_11 857 # ASSIGN : s_3_12 885 # ASSIGN : s_3_13 941 # ASSIGN : s_3_14 1053 # ASSIGN : s_4_0 69 # ASSIGN : s_4_1 205 # ASSIGN : s_4_2 264 # ASSIGN : s_4_3 284 # ASSIGN : s_4_4 363 # ASSIGN : s_4_5 371 # ASSIGN : s_4_6 444 # ASSIGN : s_4_7 570 # ASSIGN : s_4_8 622 # ASSIGN : s_4_9 721 # ASSIGN : s_4_10 783 # ASSIGN : s_4_11 1070 # ASSIGN : s_4_12 1158 # ASSIGN : s_4_13 1202 # ASSIGN : s_4_14 1282 # ASSIGN : s_5_0 136 # ASSIGN : s_5_1 215 # ASSIGN : s_5_2 278 # ASSIGN : s_5_3 444 # ASSIGN : s_5_4 457 # ASSIGN : s_5_5 543 # ASSIGN : s_5_6 646 # ASSIGN : s_5_7 658 # ASSIGN : s_5_8 724 # ASSIGN : s_5_9 953 # ASSIGN : s_5_10 1038 # ASSIGN : s_5_11 1079 # ASSIGN : s_5_12 1093 # ASSIGN : s_5_13 1096 # ASSIGN : s_5_14 1150 # ASSIGN : s_6_0 207 # ASSIGN : s_6_1 249 # ASSIGN : s_6_2 288 # ASSIGN : s_6_3 353 # ASSIGN : s_6_4 450 # ASSIGN : s_6_5 597 # ASSIGN : s_6_6 632 # ASSIGN : s_6_7 781 # ASSIGN : s_6_8 941 # ASSIGN : s_6_9 957 # ASSIGN : s_6_10 1023 # ASSIGN : s_6_11 1065 # ASSIGN : s_6_12 1145 # ASSIGN : s_6_13 1179 # ASSIGN : s_6_14 1271 # ASSIGN : s_7_0 84 # ASSIGN : s_7_1 205 # ASSIGN : s_7_2 231 # ASSIGN : s_7_3 280 # ASSIGN : s_7_4 347 # ASSIGN : s_7_5 408 # ASSIGN : s_7_6 446 # ASSIGN : s_7_7 712 # ASSIGN : s_7_8 893 # ASSIGN : s_7_9 960 # ASSIGN : s_7_10 995 # ASSIGN : s_7_11 1060 # ASSIGN : s_7_12 1113 # ASSIGN : s_7_13 1156 # ASSIGN : s_7_14 1202 # ASSIGN : s_8_0 253 # ASSIGN : s_8_1 341 # ASSIGN : s_8_2 409 # ASSIGN : s_8_3 431 # ASSIGN : s_8_4 564 # ASSIGN : s_8_5 683 # ASSIGN : s_8_6 691 # ASSIGN : s_8_7 706 # ASSIGN : s_8_8 794 # ASSIGN : s_8_9 880 # ASSIGN : s_8_10 912 # ASSIGN : s_8_11 1001 # ASSIGN : s_8_12 1118 # ASSIGN : s_8_13 1196 # ASSIGN : s_8_14 1259 # ASSIGN : s_9_0 489 # ASSIGN : s_9_1 519 # ASSIGN : s_9_2 562 # ASSIGN : s_9_3 642 # ASSIGN : s_9_4 710 # ASSIGN : s_9_5 741 # ASSIGN : s_9_6 747 # ASSIGN : s_9_7 794 # ASSIGN : s_9_8 882 # ASSIGN : s_9_9 982 # ASSIGN : s_9_10 1033 # ASSIGN : s_9_11 1147 # ASSIGN : s_9_12 1186 # ASSIGN : s_9_13 1219 # ASSIGN : s_9_14 1293 # ASSIGN : s_10_0 1 # ASSIGN : s_10_1 24 # ASSIGN : s_10_2 114 # ASSIGN : s_10_3 169 # ASSIGN : s_10_4 203 # ASSIGN : s_10_5 277 # ASSIGN : s_10_6 369 # ASSIGN : s_10_7 486 # ASSIGN : s_10_8 557 # ASSIGN : s_10_9 649 # ASSIGN : s_10_10 736 # ASSIGN : s_10_11 841 # ASSIGN : s_10_12 876 # ASSIGN : s_10_13 1153 # ASSIGN : s_10_14 1214 # ASSIGN : s_11_0 1 # ASSIGN : s_11_1 51 # ASSIGN : s_11_2 119 # ASSIGN : s_11_3 220 # ASSIGN : s_11_4 330 # ASSIGN : s_11_5 428 # ASSIGN : s_11_6 501 # ASSIGN : s_11_7 539 # ASSIGN : s_11_8 555 # ASSIGN : s_11_9 745 # ASSIGN : s_11_10 785 # ASSIGN : s_11_11 821 # ASSIGN : s_11_12 858 # ASSIGN : s_11_13 900 # ASSIGN : s_11_14 1176 # ASSIGN : s_12_0 93 # ASSIGN : s_12_1 95 # ASSIGN : s_12_2 192 # ASSIGN : s_12_3 257 # ASSIGN : s_12_4 332 # ASSIGN : s_12_5 423 # ASSIGN : s_12_6 498 # ASSIGN : s_12_7 574 # ASSIGN : s_12_8 640 # ASSIGN : s_12_9 832 # ASSIGN : s_12_10 877 # ASSIGN : s_12_11 906 # ASSIGN : s_12_12 955 # ASSIGN : s_12_13 1212 # ASSIGN : s_12_14 1262 # ASSIGN : s_13_0 7 # ASSIGN : s_13_1 87 # ASSIGN : s_13_2 194 # ASSIGN : s_13_3 234 # ASSIGN : s_13_4 355 # ASSIGN : s_13_5 686 # ASSIGN : s_13_6 701 # ASSIGN : s_13_7 732 # ASSIGN : s_13_8 854 # ASSIGN : s_13_9 966 # ASSIGN : s_13_10 1021 # ASSIGN : s_13_11 1122 # ASSIGN : s_13_12 1145 # ASSIGN : s_13_13 1164 # ASSIGN : s_13_14 1207 # ASSIGN : s_14_0 130 # ASSIGN : s_14_1 206 # ASSIGN : s_14_2 296 # ASSIGN : s_14_3 402 # ASSIGN : s_14_4 474 # ASSIGN : s_14_5 741 # ASSIGN : s_14_6 769 # ASSIGN : s_14_7 788 # ASSIGN : s_14_8 812 # ASSIGN : s_14_9 836 # ASSIGN : s_14_10 880 # ASSIGN : s_14_11 884 # ASSIGN : s_14_12 944 # ASSIGN : s_14_13 1068 # ASSIGN : s_14_14 1078 SHOW_RESULT 1300 END : 1300 (1 seconds) [Sat Jun 3 12:55:00 2006] SHOW_RESULT 1300 CPU : 1.08999999999997 = 1.08999999999997 + 0 + 0 + 0 # BOUND : makespan 1255 1300 MODIFY_CNF 1277 BEGIN : [Sat Jun 3 12:55:00 2006] MODIFY_CNF 1277 END : 142757219 bytes (0 seconds) [Sat Jun 3 12:55:00 2006] MODIFY_CNF 1277 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1277 BEGIN : [Sat Jun 3 12:55:00 2006] CMD : minisat /work/tamura/csp2sat69982.cnf /work/tamura/csp2sat69982.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1860991 5471591 | 620330 0 0 NaNQ | 0.000 % | | 102 | 1860991 5471591 | 682363 102 1211 11.9 | 71.052 % | | 253 | 1860991 5471591 | 750599 253 2521 10.0 | 71.052 % | | 478 | 1860991 5471591 | 825659 478 5311 11.1 | 71.052 % | | 816 | 1860991 5471591 | 908225 816 10905 13.4 | 71.052 % | | 1322 | 1860991 5471591 | 999047 1322 23836 18.0 | 71.052 % | | 2081 | 1860991 5471591 | 1098952 2081 36945 17.8 | 71.052 % | | 3220 | 1860991 5471591 | 1208847 3220 57443 17.8 | 71.052 % | | 4929 | 1860991 5471591 | 1329732 4929 94054 19.1 | 71.052 % | ==============================================================================) restarts : 9 conflicts : 5959 (110 /sec) decisions : 9236 (171 /sec) propagations : 82758734 (1531153 /sec) inspects : 701984125 (12987694 /sec) conflict literals : 116858 (31.01 % deleted) CPU time : 54.0499 s SATISFIABLE VERIFY_CNF 1277 END : (56 seconds) [Sat Jun 3 12:55:56 2006] VERIFY_CNF 1277 CPU : 55.54 = 0.00999999999999091 + 0.0299999999999999 + 55.34 + 0.16 # RESULT : makespan 1277 SATISFIABLE SHOW_RESULT 1277 BEGIN : [Sat Jun 3 12:55:56 2006] # ASSIGN : makespan 1277 # ASSIGN : s_0_0 42 # ASSIGN : s_0_1 133 # ASSIGN : s_0_2 189 # ASSIGN : s_0_3 348 # ASSIGN : s_0_4 433 # ASSIGN : s_0_5 523 # ASSIGN : s_0_6 576 # ASSIGN : s_0_7 583 # ASSIGN : s_0_8 661 # ASSIGN : s_0_9 782 # ASSIGN : s_0_10 820 # ASSIGN : s_0_11 839 # ASSIGN : s_0_12 895 # ASSIGN : s_0_13 964 # ASSIGN : s_0_14 1030 # ASSIGN : s_1_0 9 # ASSIGN : s_1_1 43 # ASSIGN : s_1_2 44 # ASSIGN : s_1_3 101 # ASSIGN : s_1_4 175 # ASSIGN : s_1_5 250 # ASSIGN : s_1_6 323 # ASSIGN : s_1_7 419 # ASSIGN : s_1_8 499 # ASSIGN : s_1_9 615 # ASSIGN : s_1_10 708 # ASSIGN : s_1_11 806 # ASSIGN : s_1_12 903 # ASSIGN : s_1_13 952 # ASSIGN : s_1_14 1274 # ASSIGN : s_2_0 150 # ASSIGN : s_2_1 365 # ASSIGN : s_2_2 475 # ASSIGN : s_2_3 557 # ASSIGN : s_2_4 628 # ASSIGN : s_2_5 732 # ASSIGN : s_2_6 801 # ASSIGN : s_2_7 896 # ASSIGN : s_2_8 938 # ASSIGN : s_2_9 977 # ASSIGN : s_2_10 990 # ASSIGN : s_2_11 991 # ASSIGN : s_2_12 1074 # ASSIGN : s_2_13 1101 # ASSIGN : s_2_14 1178 # ASSIGN : s_3_0 276 # ASSIGN : s_3_1 326 # ASSIGN : s_3_2 327 # ASSIGN : s_3_3 350 # ASSIGN : s_3_4 422 # ASSIGN : s_3_5 530 # ASSIGN : s_3_6 586 # ASSIGN : s_3_7 648 # ASSIGN : s_3_8 681 # ASSIGN : s_3_9 765 # ASSIGN : s_3_10 886 # ASSIGN : s_3_11 966 # ASSIGN : s_3_12 989 # ASSIGN : s_3_13 1045 # ASSIGN : s_3_14 1128 # ASSIGN : s_4_0 29 # ASSIGN : s_4_1 133 # ASSIGN : s_4_2 148 # ASSIGN : s_4_3 194 # ASSIGN : s_4_4 441 # ASSIGN : s_4_5 449 # ASSIGN : s_4_6 522 # ASSIGN : s_4_7 608 # ASSIGN : s_4_8 660 # ASSIGN : s_4_9 739 # ASSIGN : s_4_10 859 # ASSIGN : s_4_11 1015 # ASSIGN : s_4_12 1135 # ASSIGN : s_4_13 1179 # ASSIGN : s_4_14 1259 # ASSIGN : s_5_0 47 # ASSIGN : s_5_1 126 # ASSIGN : s_5_2 463 # ASSIGN : s_5_3 557 # ASSIGN : s_5_4 566 # ASSIGN : s_5_5 693 # ASSIGN : s_5_6 796 # ASSIGN : s_5_7 809 # ASSIGN : s_5_8 875 # ASSIGN : s_5_9 930 # ASSIGN : s_5_10 1010 # ASSIGN : s_5_11 1045 # ASSIGN : s_5_12 1059 # ASSIGN : s_5_13 1062 # ASSIGN : s_5_14 1116 # ASSIGN : s_6_0 0 # ASSIGN : s_6_1 45 # ASSIGN : s_6_2 84 # ASSIGN : s_6_3 281 # ASSIGN : s_6_4 290 # ASSIGN : s_6_5 387 # ASSIGN : s_6_6 421 # ASSIGN : s_6_7 585 # ASSIGN : s_6_8 843 # ASSIGN : s_6_9 868 # ASSIGN : s_6_10 1000 # ASSIGN : s_6_11 1042 # ASSIGN : s_6_12 1122 # ASSIGN : s_6_13 1156 # ASSIGN : s_6_14 1248 # ASSIGN : s_7_0 114 # ASSIGN : s_7_1 298 # ASSIGN : s_7_2 342 # ASSIGN : s_7_3 391 # ASSIGN : s_7_4 470 # ASSIGN : s_7_5 536 # ASSIGN : s_7_6 556 # ASSIGN : s_7_7 706 # ASSIGN : s_7_8 735 # ASSIGN : s_7_9 786 # ASSIGN : s_7_10 821 # ASSIGN : s_7_11 859 # ASSIGN : s_7_12 877 # ASSIGN : s_7_13 920 # ASSIGN : s_7_14 1179 # ASSIGN : s_8_0 277 # ASSIGN : s_8_1 365 # ASSIGN : s_8_2 527 # ASSIGN : s_8_3 550 # ASSIGN : s_8_4 656 # ASSIGN : s_8_5 724 # ASSIGN : s_8_6 745 # ASSIGN : s_8_7 760 # ASSIGN : s_8_8 848 # ASSIGN : s_8_9 937 # ASSIGN : s_8_10 957 # ASSIGN : s_8_11 1046 # ASSIGN : s_8_12 1105 # ASSIGN : s_8_13 1173 # ASSIGN : s_8_14 1236 # ASSIGN : s_9_0 84 # ASSIGN : s_9_1 191 # ASSIGN : s_9_2 234 # ASSIGN : s_9_3 323 # ASSIGN : s_9_4 407 # ASSIGN : s_9_5 514 # ASSIGN : s_9_6 520 # ASSIGN : s_9_7 556 # ASSIGN : s_9_8 644 # ASSIGN : s_9_9 755 # ASSIGN : s_9_10 906 # ASSIGN : s_9_11 1057 # ASSIGN : s_9_12 1089 # ASSIGN : s_9_13 1111 # ASSIGN : s_9_14 1270 # ASSIGN : s_10_0 11 # ASSIGN : s_10_1 44 # ASSIGN : s_10_2 134 # ASSIGN : s_10_3 189 # ASSIGN : s_10_4 218 # ASSIGN : s_10_5 295 # ASSIGN : s_10_6 387 # ASSIGN : s_10_7 530 # ASSIGN : s_10_8 603 # ASSIGN : s_10_9 707 # ASSIGN : s_10_10 790 # ASSIGN : s_10_11 1002 # ASSIGN : s_10_12 1037 # ASSIGN : s_10_13 1130 # ASSIGN : s_10_14 1191 # ASSIGN : s_11_0 19 # ASSIGN : s_11_1 69 # ASSIGN : s_11_2 150 # ASSIGN : s_11_3 238 # ASSIGN : s_11_4 314 # ASSIGN : s_11_5 339 # ASSIGN : s_11_6 412 # ASSIGN : s_11_7 430 # ASSIGN : s_11_8 458 # ASSIGN : s_11_9 697 # ASSIGN : s_11_10 737 # ASSIGN : s_11_11 966 # ASSIGN : s_11_12 1003 # ASSIGN : s_11_13 1059 # ASSIGN : s_11_14 1153 # ASSIGN : s_12_0 0 # ASSIGN : s_12_1 2 # ASSIGN : s_12_2 91 # ASSIGN : s_12_3 104 # ASSIGN : s_12_4 179 # ASSIGN : s_12_5 210 # ASSIGN : s_12_6 284 # ASSIGN : s_12_7 356 # ASSIGN : s_12_8 434 # ASSIGN : s_12_9 599 # ASSIGN : s_12_10 652 # ASSIGN : s_12_11 688 # ASSIGN : s_12_12 763 # ASSIGN : s_12_13 1072 # ASSIGN : s_12_14 1239 # ASSIGN : s_13_0 5 # ASSIGN : s_13_1 85 # ASSIGN : s_13_2 214 # ASSIGN : s_13_3 273 # ASSIGN : s_13_4 343 # ASSIGN : s_13_5 422 # ASSIGN : s_13_6 437 # ASSIGN : s_13_7 468 # ASSIGN : s_13_8 808 # ASSIGN : s_13_9 911 # ASSIGN : s_13_10 966 # ASSIGN : s_13_11 1099 # ASSIGN : s_13_12 1122 # ASSIGN : s_13_13 1141 # ASSIGN : s_13_14 1184 # ASSIGN : s_14_0 164 # ASSIGN : s_14_1 239 # ASSIGN : s_14_2 374 # ASSIGN : s_14_3 478 # ASSIGN : s_14_4 550 # ASSIGN : s_14_5 686 # ASSIGN : s_14_6 692 # ASSIGN : s_14_7 715 # ASSIGN : s_14_8 885 # ASSIGN : s_14_9 909 # ASSIGN : s_14_10 953 # ASSIGN : s_14_11 969 # ASSIGN : s_14_12 1065 # ASSIGN : s_14_13 1164 # ASSIGN : s_14_14 1174 SHOW_RESULT 1277 END : 1277 (1 seconds) [Sat Jun 3 12:55:57 2006] SHOW_RESULT 1277 CPU : 1.11000000000001 = 1.11000000000001 + 0 + 0 + 0 # BOUND : makespan 1255 1277 MODIFY_CNF 1266 BEGIN : [Sat Jun 3 12:55:57 2006] MODIFY_CNF 1266 END : 142757219 bytes (0 seconds) [Sat Jun 3 12:55:57 2006] MODIFY_CNF 1266 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1266 BEGIN : [Sat Jun 3 12:55:57 2006] CMD : minisat /work/tamura/csp2sat69982.cnf /work/tamura/csp2sat69982.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1807231 5312826 | 602410 0 0 NaNQ | 0.000 % | | 100 | 1807231 5312826 | 662651 100 1030 10.3 | 71.703 % | | 250 | 1807231 5312826 | 728916 250 3556 14.2 | 71.703 % | | 475 | 1807231 5312826 | 801807 475 6213 13.1 | 71.703 % | | 812 | 1807231 5312826 | 881988 812 11425 14.1 | 71.703 % | | 1319 | 1807231 5312826 | 970187 1319 18442 14.0 | 71.703 % | | 2078 | 1807231 5312826 | 1067206 2078 32460 15.6 | 71.703 % | | 3218 | 1807231 5312826 | 1173926 3218 50929 15.8 | 71.703 % | | 4926 | 1807231 5312826 | 1291319 4926 78252 15.9 | 71.703 % | | 7488 | 1807231 5312826 | 1420451 7488 125720 16.8 | 71.703 % | | 11332 | 1807231 5312826 | 1562496 11332 206114 18.2 | 71.703 % | | 17098 | 1804771 5305477 | 1718746 16608 341496 20.6 | 71.712 % | ==============================================================================) restarts : 12 conflicts : 19309 (127 /sec) decisions : 26765 (176 /sec) propagations : 259622452 (1703847 /sec) inspects : 2100406212 (13784521 /sec) conflict literals : 390074 (36.83 % deleted) CPU time : 152.374 s UNSATISFIABLE VERIFY_CNF 1266 END : (155 seconds) [Sat Jun 3 12:58:32 2006] VERIFY_CNF 1266 CPU : 153.78 = 0 + 0.04 + 153.6 + 0.14 # RESULT : makespan 1266 UNSATISFIABLE # BOUND : makespan 1267 1277 MODIFY_CNF 1272 BEGIN : [Sat Jun 3 12:58:32 2006] MODIFY_CNF 1272 END : 142757219 bytes (0 seconds) [Sat Jun 3 12:58:32 2006] MODIFY_CNF 1272 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1272 BEGIN : [Sat Jun 3 12:58:32 2006] CMD : minisat /work/tamura/csp2sat69982.cnf /work/tamura/csp2sat69982.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1830867 5382369 | 610289 0 0 NaNQ | 0.000 % | | 100 | 1830867 5382369 | 671317 100 1357 13.6 | 71.351 % | | 252 | 1830867 5382369 | 738449 251 3013 12.0 | 71.352 % | | 477 | 1830867 5382369 | 812294 476 7023 14.8 | 71.352 % | | 815 | 1830207 5380390 | 893524 741 10932 14.8 | 71.352 % | | 1324 | 1830207 5380390 | 982876 1250 17328 13.9 | 71.352 % | | 2085 | 1830207 5380390 | 1081164 2011 33532 16.7 | 71.352 % | | 3225 | 1830207 5380390 | 1189280 3151 49835 15.8 | 71.352 % | | 4933 | 1830207 5380390 | 1308208 4859 82167 16.9 | 71.352 % | | 7495 | 1830207 5380390 | 1439029 7421 128937 17.4 | 71.352 % | | 11339 | 1829705 5378885 | 1582932 9880 176610 17.9 | 71.352 % | | 17106 | 1829705 5378885 | 1741225 15647 293165 18.7 | 71.352 % | | 25755 | 1829705 5378885 | 1915348 24296 497720 20.5 | 71.352 % | ==============================================================================) restarts : 13 conflicts : 36222 (128 /sec) decisions : 50064 (177 /sec) propagations : 482878334 (1705081 /sec) inspects : 4027357653 (14220914 /sec) conflict literals : 778689 (40.78 % deleted) CPU time : 283.2 s UNSATISFIABLE VERIFY_CNF 1272 END : (285 seconds) [Sat Jun 3 13:03:17 2006] VERIFY_CNF 1272 CPU : 284.59 = 0.00999999999999091 + 0.02 + 284.41 + 0.15 # RESULT : makespan 1272 UNSATISFIABLE # BOUND : makespan 1273 1277 MODIFY_CNF 1275 BEGIN : [Sat Jun 3 13:03:17 2006] MODIFY_CNF 1275 END : 142757219 bytes (0 seconds) [Sat Jun 3 13:03:17 2006] MODIFY_CNF 1275 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1275 BEGIN : [Sat Jun 3 13:03:17 2006] CMD : minisat /work/tamura/csp2sat69982.cnf /work/tamura/csp2sat69982.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1849840 5438597 | 616613 0 0 NaNQ | 0.000 % | | 100 | 1849840 5438597 | 678274 100 1065 10.7 | 71.171 % | | 250 | 1849840 5438597 | 746101 250 2802 11.2 | 71.171 % | | 478 | 1849840 5438597 | 820711 478 5879 12.3 | 71.171 % | | 816 | 1849840 5438597 | 902783 816 11661 14.3 | 71.171 % | | 1322 | 1849840 5438597 | 993061 1322 18779 14.2 | 71.171 % | | 2084 | 1849840 5438597 | 1092367 2084 31537 15.1 | 71.171 % | | 3223 | 1849840 5438597 | 1201604 3223 51390 15.9 | 71.171 % | | 4931 | 1849840 5438597 | 1321764 4931 86752 17.6 | 71.171 % | | 7494 | 1849840 5438597 | 1453941 7494 140079 18.7 | 71.171 % | | 11338 | 1849840 5438597 | 1599335 11338 216606 19.1 | 71.171 % | ==============================================================================) restarts : 11 conflicts : 12433 (124 /sec) decisions : 18474 (184 /sec) propagations : 166478995 (1658786 /sec) inspects : 1369055156 (13641175 /sec) conflict literals : 239671 (34.07 % deleted) CPU time : 100.362 s SATISFIABLE VERIFY_CNF 1275 END : (102 seconds) [Sat Jun 3 13:04:59 2006] VERIFY_CNF 1275 CPU : 101.87 = 0 + 0.02 + 101.7 + 0.15 # RESULT : makespan 1275 SATISFIABLE SHOW_RESULT 1275 BEGIN : [Sat Jun 3 13:04:59 2006] # ASSIGN : makespan 1275 # ASSIGN : s_0_0 56 # ASSIGN : s_0_1 147 # ASSIGN : s_0_2 187 # ASSIGN : s_0_3 346 # ASSIGN : s_0_4 431 # ASSIGN : s_0_5 521 # ASSIGN : s_0_6 574 # ASSIGN : s_0_7 581 # ASSIGN : s_0_8 659 # ASSIGN : s_0_9 780 # ASSIGN : s_0_10 818 # ASSIGN : s_0_11 837 # ASSIGN : s_0_12 893 # ASSIGN : s_0_13 962 # ASSIGN : s_0_14 1028 # ASSIGN : s_1_0 10 # ASSIGN : s_1_1 44 # ASSIGN : s_1_2 57 # ASSIGN : s_1_3 99 # ASSIGN : s_1_4 173 # ASSIGN : s_1_5 248 # ASSIGN : s_1_6 321 # ASSIGN : s_1_7 417 # ASSIGN : s_1_8 497 # ASSIGN : s_1_9 613 # ASSIGN : s_1_10 706 # ASSIGN : s_1_11 804 # ASSIGN : s_1_12 901 # ASSIGN : s_1_13 950 # ASSIGN : s_1_14 1272 # ASSIGN : s_2_0 148 # ASSIGN : s_2_1 363 # ASSIGN : s_2_2 473 # ASSIGN : s_2_3 555 # ASSIGN : s_2_4 610 # ASSIGN : s_2_5 730 # ASSIGN : s_2_6 799 # ASSIGN : s_2_7 894 # ASSIGN : s_2_8 936 # ASSIGN : s_2_9 975 # ASSIGN : s_2_10 988 # ASSIGN : s_2_11 989 # ASSIGN : s_2_12 1072 # ASSIGN : s_2_13 1099 # ASSIGN : s_2_14 1176 # ASSIGN : s_3_0 274 # ASSIGN : s_3_1 324 # ASSIGN : s_3_2 325 # ASSIGN : s_3_3 348 # ASSIGN : s_3_4 420 # ASSIGN : s_3_5 528 # ASSIGN : s_3_6 584 # ASSIGN : s_3_7 646 # ASSIGN : s_3_8 679 # ASSIGN : s_3_9 832 # ASSIGN : s_3_10 888 # ASSIGN : s_3_11 964 # ASSIGN : s_3_12 987 # ASSIGN : s_3_13 1043 # ASSIGN : s_3_14 1126 # ASSIGN : s_4_0 97 # ASSIGN : s_4_1 116 # ASSIGN : s_4_2 131 # ASSIGN : s_4_3 192 # ASSIGN : s_4_4 439 # ASSIGN : s_4_5 447 # ASSIGN : s_4_6 520 # ASSIGN : s_4_7 606 # ASSIGN : s_4_8 658 # ASSIGN : s_4_9 737 # ASSIGN : s_4_10 825 # ASSIGN : s_4_11 918 # ASSIGN : s_4_12 1133 # ASSIGN : s_4_13 1177 # ASSIGN : s_4_14 1257 # ASSIGN : s_5_0 45 # ASSIGN : s_5_1 124 # ASSIGN : s_5_2 461 # ASSIGN : s_5_3 555 # ASSIGN : s_5_4 564 # ASSIGN : s_5_5 691 # ASSIGN : s_5_6 794 # ASSIGN : s_5_7 817 # ASSIGN : s_5_8 883 # ASSIGN : s_5_9 938 # ASSIGN : s_5_10 1008 # ASSIGN : s_5_11 1043 # ASSIGN : s_5_12 1057 # ASSIGN : s_5_13 1060 # ASSIGN : s_5_14 1114 # ASSIGN : s_6_0 1 # ASSIGN : s_6_1 43 # ASSIGN : s_6_2 82 # ASSIGN : s_6_3 279 # ASSIGN : s_6_4 288 # ASSIGN : s_6_5 385 # ASSIGN : s_6_6 419 # ASSIGN : s_6_7 583 # ASSIGN : s_6_8 689 # ASSIGN : s_6_9 744 # ASSIGN : s_6_10 908 # ASSIGN : s_6_11 1040 # ASSIGN : s_6_12 1120 # ASSIGN : s_6_13 1154 # ASSIGN : s_6_14 1246 # ASSIGN : s_7_0 112 # ASSIGN : s_7_1 296 # ASSIGN : s_7_2 340 # ASSIGN : s_7_3 389 # ASSIGN : s_7_4 468 # ASSIGN : s_7_5 534 # ASSIGN : s_7_6 554 # ASSIGN : s_7_7 700 # ASSIGN : s_7_8 802 # ASSIGN : s_7_9 853 # ASSIGN : s_7_10 888 # ASSIGN : s_7_11 992 # ASSIGN : s_7_12 1010 # ASSIGN : s_7_13 1053 # ASSIGN : s_7_14 1177 # ASSIGN : s_8_0 275 # ASSIGN : s_8_1 363 # ASSIGN : s_8_2 525 # ASSIGN : s_8_3 548 # ASSIGN : s_8_4 654 # ASSIGN : s_8_5 722 # ASSIGN : s_8_6 743 # ASSIGN : s_8_7 758 # ASSIGN : s_8_8 846 # ASSIGN : s_8_9 935 # ASSIGN : s_8_10 955 # ASSIGN : s_8_11 1044 # ASSIGN : s_8_12 1103 # ASSIGN : s_8_13 1171 # ASSIGN : s_8_14 1234 # ASSIGN : s_9_0 27 # ASSIGN : s_9_1 189 # ASSIGN : s_9_2 232 # ASSIGN : s_9_3 321 # ASSIGN : s_9_4 405 # ASSIGN : s_9_5 512 # ASSIGN : s_9_6 518 # ASSIGN : s_9_7 554 # ASSIGN : s_9_8 642 # ASSIGN : s_9_9 753 # ASSIGN : s_9_10 926 # ASSIGN : s_9_11 1055 # ASSIGN : s_9_12 1087 # ASSIGN : s_9_13 1109 # ASSIGN : s_9_14 1268 # ASSIGN : s_10_0 9 # ASSIGN : s_10_1 42 # ASSIGN : s_10_2 132 # ASSIGN : s_10_3 187 # ASSIGN : s_10_4 216 # ASSIGN : s_10_5 293 # ASSIGN : s_10_6 385 # ASSIGN : s_10_7 528 # ASSIGN : s_10_8 601 # ASSIGN : s_10_9 705 # ASSIGN : s_10_10 788 # ASSIGN : s_10_11 1000 # ASSIGN : s_10_12 1035 # ASSIGN : s_10_13 1128 # ASSIGN : s_10_14 1189 # ASSIGN : s_11_0 17 # ASSIGN : s_11_1 67 # ASSIGN : s_11_2 148 # ASSIGN : s_11_3 236 # ASSIGN : s_11_4 312 # ASSIGN : s_11_5 337 # ASSIGN : s_11_6 410 # ASSIGN : s_11_7 428 # ASSIGN : s_11_8 456 # ASSIGN : s_11_9 742 # ASSIGN : s_11_10 782 # ASSIGN : s_11_11 864 # ASSIGN : s_11_12 1001 # ASSIGN : s_11_13 1057 # ASSIGN : s_11_14 1151 # ASSIGN : s_12_0 1 # ASSIGN : s_12_1 3 # ASSIGN : s_12_2 89 # ASSIGN : s_12_3 102 # ASSIGN : s_12_4 177 # ASSIGN : s_12_5 208 # ASSIGN : s_12_6 282 # ASSIGN : s_12_7 354 # ASSIGN : s_12_8 432 # ASSIGN : s_12_9 597 # ASSIGN : s_12_10 650 # ASSIGN : s_12_11 680 # ASSIGN : s_12_12 729 # ASSIGN : s_12_13 886 # ASSIGN : s_12_14 972 # ASSIGN : s_13_0 3 # ASSIGN : s_13_1 83 # ASSIGN : s_13_2 212 # ASSIGN : s_13_3 271 # ASSIGN : s_13_4 341 # ASSIGN : s_13_5 420 # ASSIGN : s_13_6 435 # ASSIGN : s_13_7 466 # ASSIGN : s_13_8 806 # ASSIGN : s_13_9 920 # ASSIGN : s_13_10 1004 # ASSIGN : s_13_11 1097 # ASSIGN : s_13_12 1120 # ASSIGN : s_13_13 1139 # ASSIGN : s_13_14 1182 # ASSIGN : s_14_0 162 # ASSIGN : s_14_1 237 # ASSIGN : s_14_2 372 # ASSIGN : s_14_3 476 # ASSIGN : s_14_4 548 # ASSIGN : s_14_5 684 # ASSIGN : s_14_6 690 # ASSIGN : s_14_7 713 # ASSIGN : s_14_8 738 # ASSIGN : s_14_9 762 # ASSIGN : s_14_10 806 # ASSIGN : s_14_11 810 # ASSIGN : s_14_12 1063 # ASSIGN : s_14_13 1162 # ASSIGN : s_14_14 1172 SHOW_RESULT 1275 END : 1275 (1 seconds) [Sat Jun 3 13:05:00 2006] SHOW_RESULT 1275 CPU : 1.08000000000004 = 1.08000000000004 + 0 + 0 + 0 # BOUND : makespan 1273 1275 MODIFY_CNF 1274 BEGIN : [Sat Jun 3 13:05:00 2006] MODIFY_CNF 1274 END : 142757219 bytes (0 seconds) [Sat Jun 3 13:05:00 2006] MODIFY_CNF 1274 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1274 BEGIN : [Sat Jun 3 13:05:00 2006] CMD : minisat /work/tamura/csp2sat69982.cnf /work/tamura/csp2sat69982.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1841441 5413632 | 613813 0 0 NaNQ | 0.000 % | | 101 | 1841441 5413632 | 675194 101 1190 11.8 | 71.232 % | | 251 | 1841441 5413632 | 742713 251 2737 10.9 | 71.232 % | | 476 | 1841441 5413632 | 816985 476 7777 16.3 | 71.232 % | | 814 | 1841441 5413632 | 898683 814 13219 16.2 | 71.232 % | | 1320 | 1841441 5413632 | 988551 1320 21587 16.4 | 71.232 % | | 2079 | 1841441 5413632 | 1087407 2079 33215 16.0 | 71.232 % | | 3218 | 1841441 5413632 | 1196147 3218 53250 16.5 | 71.232 % | | 4926 | 1841441 5413632 | 1315762 4926 81894 16.6 | 71.232 % | | 7488 | 1841441 5413632 | 1447338 7488 127614 17.0 | 71.232 % | | 11332 | 1840937 5412121 | 1592072 9729 167164 17.2 | 71.233 % | | 17099 | 1840937 5412121 | 1751280 15496 288034 18.6 | 71.233 % | ==============================================================================) restarts : 12 conflicts : 19305 (126 /sec) decisions : 27400 (179 /sec) propagations : 261408985 (1710763 /sec) inspects : 2134110467 (13966454 /sec) conflict literals : 377592 (36.69 % deleted) CPU time : 152.803 s SATISFIABLE VERIFY_CNF 1274 END : (155 seconds) [Sat Jun 3 13:07:35 2006] VERIFY_CNF 1274 CPU : 154.3 = 0.00999999999999091 + 0.0299999999999999 + 154.1 + 0.16 # RESULT : makespan 1274 SATISFIABLE SHOW_RESULT 1274 BEGIN : [Sat Jun 3 13:07:35 2006] # ASSIGN : makespan 1274 # ASSIGN : s_0_0 56 # ASSIGN : s_0_1 251 # ASSIGN : s_0_2 266 # ASSIGN : s_0_3 345 # ASSIGN : s_0_4 430 # ASSIGN : s_0_5 520 # ASSIGN : s_0_6 573 # ASSIGN : s_0_7 580 # ASSIGN : s_0_8 658 # ASSIGN : s_0_9 779 # ASSIGN : s_0_10 817 # ASSIGN : s_0_11 836 # ASSIGN : s_0_12 892 # ASSIGN : s_0_13 961 # ASSIGN : s_0_14 1027 # ASSIGN : s_1_0 9 # ASSIGN : s_1_1 43 # ASSIGN : s_1_2 56 # ASSIGN : s_1_3 98 # ASSIGN : s_1_4 172 # ASSIGN : s_1_5 247 # ASSIGN : s_1_6 320 # ASSIGN : s_1_7 416 # ASSIGN : s_1_8 496 # ASSIGN : s_1_9 612 # ASSIGN : s_1_10 705 # ASSIGN : s_1_11 803 # ASSIGN : s_1_12 900 # ASSIGN : s_1_13 949 # ASSIGN : s_1_14 1271 # ASSIGN : s_2_0 147 # ASSIGN : s_2_1 362 # ASSIGN : s_2_2 472 # ASSIGN : s_2_3 554 # ASSIGN : s_2_4 609 # ASSIGN : s_2_5 729 # ASSIGN : s_2_6 798 # ASSIGN : s_2_7 893 # ASSIGN : s_2_8 935 # ASSIGN : s_2_9 974 # ASSIGN : s_2_10 987 # ASSIGN : s_2_11 988 # ASSIGN : s_2_12 1071 # ASSIGN : s_2_13 1098 # ASSIGN : s_2_14 1175 # ASSIGN : s_3_0 273 # ASSIGN : s_3_1 323 # ASSIGN : s_3_2 324 # ASSIGN : s_3_3 347 # ASSIGN : s_3_4 419 # ASSIGN : s_3_5 527 # ASSIGN : s_3_6 583 # ASSIGN : s_3_7 645 # ASSIGN : s_3_8 678 # ASSIGN : s_3_9 831 # ASSIGN : s_3_10 887 # ASSIGN : s_3_11 963 # ASSIGN : s_3_12 986 # ASSIGN : s_3_13 1042 # ASSIGN : s_3_14 1125 # ASSIGN : s_4_0 96 # ASSIGN : s_4_1 130 # ASSIGN : s_4_2 145 # ASSIGN : s_4_3 191 # ASSIGN : s_4_4 438 # ASSIGN : s_4_5 446 # ASSIGN : s_4_6 519 # ASSIGN : s_4_7 605 # ASSIGN : s_4_8 657 # ASSIGN : s_4_9 736 # ASSIGN : s_4_10 824 # ASSIGN : s_4_11 917 # ASSIGN : s_4_12 1132 # ASSIGN : s_4_13 1176 # ASSIGN : s_4_14 1256 # ASSIGN : s_5_0 44 # ASSIGN : s_5_1 123 # ASSIGN : s_5_2 460 # ASSIGN : s_5_3 554 # ASSIGN : s_5_4 563 # ASSIGN : s_5_5 690 # ASSIGN : s_5_6 793 # ASSIGN : s_5_7 816 # ASSIGN : s_5_8 882 # ASSIGN : s_5_9 937 # ASSIGN : s_5_10 1007 # ASSIGN : s_5_11 1042 # ASSIGN : s_5_12 1056 # ASSIGN : s_5_13 1059 # ASSIGN : s_5_14 1113 # ASSIGN : s_6_0 0 # ASSIGN : s_6_1 42 # ASSIGN : s_6_2 81 # ASSIGN : s_6_3 278 # ASSIGN : s_6_4 287 # ASSIGN : s_6_5 379 # ASSIGN : s_6_6 404 # ASSIGN : s_6_7 582 # ASSIGN : s_6_8 688 # ASSIGN : s_6_9 771 # ASSIGN : s_6_10 907 # ASSIGN : s_6_11 1039 # ASSIGN : s_6_12 1119 # ASSIGN : s_6_13 1153 # ASSIGN : s_6_14 1245 # ASSIGN : s_7_0 111 # ASSIGN : s_7_1 295 # ASSIGN : s_7_2 339 # ASSIGN : s_7_3 388 # ASSIGN : s_7_4 467 # ASSIGN : s_7_5 533 # ASSIGN : s_7_6 553 # ASSIGN : s_7_7 699 # ASSIGN : s_7_8 831 # ASSIGN : s_7_9 915 # ASSIGN : s_7_10 950 # ASSIGN : s_7_11 991 # ASSIGN : s_7_12 1009 # ASSIGN : s_7_13 1052 # ASSIGN : s_7_14 1176 # ASSIGN : s_8_0 274 # ASSIGN : s_8_1 362 # ASSIGN : s_8_2 524 # ASSIGN : s_8_3 547 # ASSIGN : s_8_4 653 # ASSIGN : s_8_5 721 # ASSIGN : s_8_6 742 # ASSIGN : s_8_7 757 # ASSIGN : s_8_8 845 # ASSIGN : s_8_9 934 # ASSIGN : s_8_10 954 # ASSIGN : s_8_11 1043 # ASSIGN : s_8_12 1102 # ASSIGN : s_8_13 1170 # ASSIGN : s_8_14 1233 # ASSIGN : s_9_0 26 # ASSIGN : s_9_1 143 # ASSIGN : s_9_2 186 # ASSIGN : s_9_3 320 # ASSIGN : s_9_4 482 # ASSIGN : s_9_5 511 # ASSIGN : s_9_6 517 # ASSIGN : s_9_7 553 # ASSIGN : s_9_8 641 # ASSIGN : s_9_9 752 # ASSIGN : s_9_10 887 # ASSIGN : s_9_11 1054 # ASSIGN : s_9_12 1086 # ASSIGN : s_9_13 1108 # ASSIGN : s_9_14 1267 # ASSIGN : s_10_0 8 # ASSIGN : s_10_1 41 # ASSIGN : s_10_2 131 # ASSIGN : s_10_3 186 # ASSIGN : s_10_4 215 # ASSIGN : s_10_5 292 # ASSIGN : s_10_6 384 # ASSIGN : s_10_7 527 # ASSIGN : s_10_8 600 # ASSIGN : s_10_9 704 # ASSIGN : s_10_10 787 # ASSIGN : s_10_11 999 # ASSIGN : s_10_12 1034 # ASSIGN : s_10_13 1127 # ASSIGN : s_10_14 1188 # ASSIGN : s_11_0 31 # ASSIGN : s_11_1 81 # ASSIGN : s_11_2 147 # ASSIGN : s_11_3 235 # ASSIGN : s_11_4 311 # ASSIGN : s_11_5 336 # ASSIGN : s_11_6 409 # ASSIGN : s_11_7 427 # ASSIGN : s_11_8 455 # ASSIGN : s_11_9 703 # ASSIGN : s_11_10 743 # ASSIGN : s_11_11 954 # ASSIGN : s_11_12 1000 # ASSIGN : s_11_13 1056 # ASSIGN : s_11_14 1150 # ASSIGN : s_12_0 0 # ASSIGN : s_12_1 2 # ASSIGN : s_12_2 88 # ASSIGN : s_12_3 101 # ASSIGN : s_12_4 176 # ASSIGN : s_12_5 207 # ASSIGN : s_12_6 281 # ASSIGN : s_12_7 353 # ASSIGN : s_12_8 431 # ASSIGN : s_12_9 596 # ASSIGN : s_12_10 649 # ASSIGN : s_12_11 679 # ASSIGN : s_12_12 728 # ASSIGN : s_12_13 885 # ASSIGN : s_12_14 1236 # ASSIGN : s_13_0 2 # ASSIGN : s_13_1 82 # ASSIGN : s_13_2 211 # ASSIGN : s_13_3 270 # ASSIGN : s_13_4 340 # ASSIGN : s_13_5 419 # ASSIGN : s_13_6 434 # ASSIGN : s_13_7 465 # ASSIGN : s_13_8 805 # ASSIGN : s_13_9 919 # ASSIGN : s_13_10 1003 # ASSIGN : s_13_11 1096 # ASSIGN : s_13_12 1119 # ASSIGN : s_13_13 1138 # ASSIGN : s_13_14 1181 # ASSIGN : s_14_0 161 # ASSIGN : s_14_1 236 # ASSIGN : s_14_2 371 # ASSIGN : s_14_3 475 # ASSIGN : s_14_4 547 # ASSIGN : s_14_5 683 # ASSIGN : s_14_6 689 # ASSIGN : s_14_7 712 # ASSIGN : s_14_8 737 # ASSIGN : s_14_9 761 # ASSIGN : s_14_10 805 # ASSIGN : s_14_11 809 # ASSIGN : s_14_12 1062 # ASSIGN : s_14_13 1161 # ASSIGN : s_14_14 1171 SHOW_RESULT 1274 END : 1274 (1 seconds) [Sat Jun 3 13:07:36 2006] SHOW_RESULT 1274 CPU : 1.10000000000002 = 1.10000000000002 + 0 + 0 + 0 # BOUND : makespan 1273 1274 MODIFY_CNF 1273 BEGIN : [Sat Jun 3 13:07:36 2006] MODIFY_CNF 1273 END : 142757219 bytes (0 seconds) [Sat Jun 3 13:07:36 2006] MODIFY_CNF 1273 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1273 BEGIN : [Sat Jun 3 13:07:36 2006] CMD : minisat /work/tamura/csp2sat69982.cnf /work/tamura/csp2sat69982.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1836605 5399353 | 612201 0 0 NaNQ | 0.000 % | | 100 | 1836605 5399353 | 673421 100 1083 10.8 | 71.291 % | | 252 | 1836605 5399353 | 740763 252 2879 11.4 | 71.291 % | | 483 | 1836605 5399353 | 814839 483 6502 13.5 | 71.291 % | | 820 | 1836605 5399353 | 896323 820 13482 16.4 | 71.291 % | | 1327 | 1836605 5399353 | 985955 1327 20737 15.6 | 71.291 % | | 2086 | 1836605 5399353 | 1084551 2086 35817 17.2 | 71.291 % | | 3225 | 1836605 5399353 | 1193006 3225 58478 18.1 | 71.291 % | | 4933 | 1836605 5399353 | 1312307 4933 93514 19.0 | 71.291 % | | 7495 | 1836605 5399353 | 1443537 7495 139727 18.6 | 71.291 % | | 11339 | 1836605 5399353 | 1587891 11339 210581 18.6 | 71.291 % | | 17105 | 1836605 5399353 | 1746680 17105 374658 21.9 | 71.291 % | | 25754 | 1817306 5342247 | 1921348 24595 556615 22.6 | 71.496 % | ==============================================================================) restarts : 13 conflicts : 37456 (123 /sec) decisions : 51861 (170 /sec) propagations : 510712825 (1671582 /sec) inspects : 4323635403 (14151415 /sec) conflict literals : 860447 (40.68 % deleted) CPU time : 305.527 s UNSATISFIABLE VERIFY_CNF 1273 END : (308 seconds) [Sat Jun 3 13:12:44 2006] VERIFY_CNF 1273 CPU : 306.84 = 0.00999999999999091 + 0.03 + 306.66 + 0.14 # RESULT : makespan 1273 UNSATISFIABLE # BOUND : makespan 1274 1274 MAIN END : (1550 seconds) [Sat Jun 3 13:12:44 2006] MAIN CPU : 1545.44 = 302.08 + 0.67 + 1240.48 + 2.21