# TIMEOUT 18000 MAIN BEGIN : [Sun Jun 18 17:20:37 2006] READ BEGIN : csp/gp09-01.csp [Sun Jun 18 17:20:37 2006] READ END : csp/gp09-01.csp (1 seconds) [Sun Jun 18 17:20:38 2006] READ CPU : 1.37 = 1.36 + 0.01 + 0 + 0 # BOUND : makespan 1000 3870 GENERATE_CNF 3870 BEGIN : [Sun Jun 18 17:20:38 2006] GENERATE_CNF 3870 END : 317881 variables 5423978 clauses 128965150 bytes (208 seconds) [Sun Jun 18 17:24:06 2006] GENERATE_CNF 3870 CPU : 206.39 = 205.5 + 0.89 + 0 + 0 MODIFY_CNF 2435 BEGIN : [Sun Jun 18 17:24:06 2006] MODIFY_CNF 2435 END : 128965157 bytes (0 seconds) [Sun Jun 18 17:24:06 2006] MODIFY_CNF 2435 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 2435 BEGIN : [Sun Jun 18 17:24:06 2006] CMD : minisat /tmp/csp2sat10989.cnf /tmp/csp2sat10989.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 3562350 10372012 | 1187450 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 4 (1 /sec) decisions : 483 (62 /sec) propagations : 389138 (49698 /sec) conflict literals : 112 (3.45 % deleted) Memory used : 213.50 MB CPU time : 7.83 s SATISFIABLE VERIFY_CNF 2435 END : (8 seconds) [Sun Jun 18 17:24:14 2006] VERIFY_CNF 2435 CPU : 8.73 = 0 + 0 + 7.98 + 0.75 # RESULT : makespan 2435 SATISFIABLE SHOW_RESULT 2435 BEGIN : [Sun Jun 18 17:24:14 2006] # ASSIGN : makespan 2435 # ASSIGN : s_0_0 1 # ASSIGN : s_0_1 148 # ASSIGN : s_0_2 637 # ASSIGN : s_0_3 1001 # ASSIGN : s_0_4 12 # ASSIGN : s_0_5 13 # ASSIGN : s_0_6 146 # ASSIGN : s_0_7 147 # ASSIGN : s_0_8 916 # ASSIGN : s_1_0 3 # ASSIGN : s_1_1 751 # ASSIGN : s_1_2 781 # ASSIGN : s_1_3 1249 # ASSIGN : s_1_4 18 # ASSIGN : s_1_5 126 # ASSIGN : s_1_6 260 # ASSIGN : s_1_7 580 # ASSIGN : s_1_8 917 # ASSIGN : s_2_0 18 # ASSIGN : s_2_1 785 # ASSIGN : s_2_2 783 # ASSIGN : s_2_3 1255 # ASSIGN : s_2_4 19 # ASSIGN : s_2_5 570 # ASSIGN : s_2_6 569 # ASSIGN : s_2_7 784 # ASSIGN : s_2_8 1256 # ASSIGN : s_3_0 440 # ASSIGN : s_3_1 1031 # ASSIGN : s_3_2 825 # ASSIGN : s_3_3 1260 # ASSIGN : s_3_4 1522 # ASSIGN : s_3_5 768 # ASSIGN : s_3_6 603 # ASSIGN : s_3_7 826 # ASSIGN : s_3_8 1257 # ASSIGN : s_4_0 2010 # ASSIGN : s_4_1 1240 # ASSIGN : s_4_2 923 # ASSIGN : s_4_3 1261 # ASSIGN : s_4_4 1953 # ASSIGN : s_4_5 817 # ASSIGN : s_4_6 682 # ASSIGN : s_4_7 1050 # ASSIGN : s_4_8 1260 # ASSIGN : s_5_0 462 # ASSIGN : s_5_1 1285 # ASSIGN : s_5_2 1286 # ASSIGN : s_5_3 1898 # ASSIGN : s_5_4 1958 # ASSIGN : s_5_5 835 # ASSIGN : s_5_6 683 # ASSIGN : s_5_7 1315 # ASSIGN : s_5_8 1743 # ASSIGN : s_6_0 514 # ASSIGN : s_6_1 1286 # ASSIGN : s_6_2 1287 # ASSIGN : s_6_3 1941 # ASSIGN : s_6_4 1959 # ASSIGN : s_6_5 1730 # ASSIGN : s_6_6 684 # ASSIGN : s_6_7 1765 # ASSIGN : s_6_8 1766 # ASSIGN : s_7_0 928 # ASSIGN : s_7_1 1294 # ASSIGN : s_7_2 1297 # ASSIGN : s_7_3 1942 # ASSIGN : s_7_4 1964 # ASSIGN : s_7_5 1966 # ASSIGN : s_7_6 1968 # ASSIGN : s_7_7 1969 # ASSIGN : s_7_8 1971 # ASSIGN : s_8_0 2011 # ASSIGN : s_8_1 1435 # ASSIGN : s_8_2 1436 # ASSIGN : s_8_3 2382 # ASSIGN : s_8_4 2423 # ASSIGN : s_8_5 2427 # ASSIGN : s_8_6 2428 # ASSIGN : s_8_7 2433 # ASSIGN : s_8_8 2434 SHOW_RESULT 2435 END : 2435 (1 seconds) [Sun Jun 18 17:24:15 2006] SHOW_RESULT 2435 CPU : 0.810000000000009 = 0.740000000000009 + 0.07 + 0 + 0 # BOUND : makespan 1000 2435 MODIFY_CNF 1717 BEGIN : [Sun Jun 18 17:24:15 2006] MODIFY_CNF 1717 END : 128965156 bytes (0 seconds) [Sun Jun 18 17:24:15 2006] MODIFY_CNF 1717 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1717 BEGIN : [Sun Jun 18 17:24:15 2006] CMD : minisat /tmp/csp2sat10989.cnf /tmp/csp2sat10989.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 2631822 7580428 | 877274 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 25 (3 /sec) decisions : 503 (54 /sec) propagations : 619605 (66056 /sec) conflict literals : 404 (7.97 % deleted) Memory used : 213.50 MB CPU time : 9.38 s SATISFIABLE VERIFY_CNF 1717 END : (10 seconds) [Sun Jun 18 17:24:25 2006] VERIFY_CNF 1717 CPU : 10.2 = 0 + 0 + 9.54 + 0.66 # RESULT : makespan 1717 SATISFIABLE SHOW_RESULT 1717 BEGIN : [Sun Jun 18 17:24:25 2006] # ASSIGN : makespan 1717 # ASSIGN : s_0_0 0 # ASSIGN : s_0_1 1216 # ASSIGN : s_0_2 258 # ASSIGN : s_0_3 647 # ASSIGN : s_0_4 1716 # ASSIGN : s_0_5 61 # ASSIGN : s_0_6 2 # ASSIGN : s_0_7 3 # ASSIGN : s_0_8 174 # ASSIGN : s_1_0 1702 # ASSIGN : s_1_1 511 # ASSIGN : s_1_2 1 # ASSIGN : s_1_3 541 # ASSIGN : s_1_4 3 # ASSIGN : s_1_5 547 # ASSIGN : s_1_6 681 # ASSIGN : s_1_7 4 # ASSIGN : s_1_8 175 # ASSIGN : s_2_0 13 # ASSIGN : s_2_1 261 # ASSIGN : s_2_2 1716 # ASSIGN : s_2_3 217 # ASSIGN : s_2_4 1124 # ASSIGN : s_2_5 744 # ASSIGN : s_2_6 990 # ASSIGN : s_2_7 218 # ASSIGN : s_2_8 507 # ASSIGN : s_3_0 424 # ASSIGN : s_3_1 8 # ASSIGN : s_3_2 217 # ASSIGN : s_3_3 218 # ASSIGN : s_3_4 511 # ASSIGN : s_3_5 942 # ASSIGN : s_3_6 991 # ASSIGN : s_3_7 219 # ASSIGN : s_3_8 508 # ASSIGN : s_4_0 14 # ASSIGN : s_4_1 240 # ASSIGN : s_4_2 758 # ASSIGN : s_4_3 1080 # ASSIGN : s_4_4 1047 # ASSIGN : s_4_5 1052 # ASSIGN : s_4_6 1070 # ASSIGN : s_4_7 429 # ASSIGN : s_4_8 619 # ASSIGN : s_5_0 446 # ASSIGN : s_5_1 260 # ASSIGN : s_5_2 402 # ASSIGN : s_5_3 403 # ASSIGN : s_5_4 510 # ASSIGN : s_5_5 1229 # ASSIGN : s_5_6 1071 # ASSIGN : s_5_7 643 # ASSIGN : s_5_8 620 # ASSIGN : s_6_0 498 # ASSIGN : s_6_1 884 # ASSIGN : s_6_2 885 # ASSIGN : s_6_3 895 # ASSIGN : s_6_4 1674 # ASSIGN : s_6_5 1679 # ASSIGN : s_6_6 1072 # ASSIGN : s_6_7 1071 # ASSIGN : s_6_8 896 # ASSIGN : s_7_0 15 # ASSIGN : s_7_1 1705 # ASSIGN : s_7_2 991 # ASSIGN : s_7_3 381 # ASSIGN : s_7_4 1710 # ASSIGN : s_7_5 1714 # ASSIGN : s_7_6 1704 # ASSIGN : s_7_7 1708 # ASSIGN : s_7_8 1241 # ASSIGN : s_8_0 668 # ASSIGN : s_8_1 1129 # ASSIGN : s_8_2 1130 # ASSIGN : s_8_3 1039 # ASSIGN : s_8_4 1712 # ASSIGN : s_8_5 1716 # ASSIGN : s_8_6 1705 # ASSIGN : s_8_7 1710 # ASSIGN : s_8_8 1711 SHOW_RESULT 1717 END : 1717 (1 seconds) [Sun Jun 18 17:24:26 2006] SHOW_RESULT 1717 CPU : 0.82000000000001 = 0.77000000000001 + 0.05 + 0 + 0 # BOUND : makespan 1000 1717 MODIFY_CNF 1358 BEGIN : [Sun Jun 18 17:24:26 2006] MODIFY_CNF 1358 END : 128965156 bytes (0 seconds) [Sun Jun 18 17:24:26 2006] MODIFY_CNF 1358 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1358 BEGIN : [Sun Jun 18 17:24:26 2006] CMD : minisat /tmp/csp2sat10989.cnf /tmp/csp2sat10989.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 2166558 6184636 | 722186 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 6 (1 /sec) decisions : 435 (40 /sec) propagations : 371999 (34097 /sec) conflict literals : 32 (5.88 % deleted) Memory used : 213.50 MB CPU time : 10.91 s SATISFIABLE VERIFY_CNF 1358 END : (12 seconds) [Sun Jun 18 17:24:38 2006] VERIFY_CNF 1358 CPU : 11.75 = 0.0100000000000193 + 0 + 11.07 + 0.67 # RESULT : makespan 1358 SATISFIABLE SHOW_RESULT 1358 BEGIN : [Sun Jun 18 17:24:38 2006] # ASSIGN : makespan 1358 # ASSIGN : s_0_0 1 # ASSIGN : s_0_1 202 # ASSIGN : s_0_2 56 # ASSIGN : s_0_3 1056 # ASSIGN : s_0_4 13 # ASSIGN : s_0_5 747 # ASSIGN : s_0_6 14 # ASSIGN : s_0_7 200 # ASSIGN : s_0_8 201 # ASSIGN : s_1_0 3 # ASSIGN : s_1_1 172 # ASSIGN : s_1_2 1 # ASSIGN : s_1_3 31 # ASSIGN : s_1_4 37 # ASSIGN : s_1_5 38 # ASSIGN : s_1_6 1040 # ASSIGN : s_1_7 539 # ASSIGN : s_1_8 207 # ASSIGN : s_2_0 18 # ASSIGN : s_2_1 1058 # ASSIGN : s_2_2 13 # ASSIGN : s_2_3 14 # ASSIGN : s_2_4 124 # ASSIGN : s_2_5 860 # ASSIGN : s_2_6 15 # ASSIGN : s_2_7 123 # ASSIGN : s_2_8 674 # ASSIGN : s_3_0 96 # ASSIGN : s_3_1 691 # ASSIGN : s_3_2 15 # ASSIGN : s_3_3 16 # ASSIGN : s_3_4 905 # ASSIGN : s_3_5 180 # ASSIGN : s_3_6 17 # ASSIGN : s_3_7 334 # ASSIGN : s_3_8 675 # ASSIGN : s_4_0 19 # ASSIGN : s_4_1 900 # ASSIGN : s_4_2 1209 # ASSIGN : s_4_3 41 # ASSIGN : s_4_4 1336 # ASSIGN : s_4_5 20 # ASSIGN : s_4_6 16 # ASSIGN : s_4_7 710 # ASSIGN : s_4_8 678 # ASSIGN : s_5_0 868 # ASSIGN : s_5_1 920 # ASSIGN : s_5_2 29 # ASSIGN : s_5_3 812 # ASSIGN : s_5_4 1357 # ASSIGN : s_5_5 229 # ASSIGN : s_5_6 99 # ASSIGN : s_5_7 921 # ASSIGN : s_5_8 679 # ASSIGN : s_6_0 1134 # ASSIGN : s_6_1 1304 # ASSIGN : s_6_2 30 # ASSIGN : s_6_3 40 # ASSIGN : s_6_4 1341 # ASSIGN : s_6_5 1305 # ASSIGN : s_6_6 100 # ASSIGN : s_6_7 1349 # ASSIGN : s_6_8 702 # ASSIGN : s_7_0 489 # ASSIGN : s_7_1 1342 # ASSIGN : s_7_2 350 # ASSIGN : s_7_3 855 # ASSIGN : s_7_4 1346 # ASSIGN : s_7_5 1340 # ASSIGN : s_7_6 1349 # ASSIGN : s_7_7 1350 # ASSIGN : s_7_8 877 # ASSIGN : s_8_0 118 # ASSIGN : s_8_1 1345 # ASSIGN : s_8_2 634 # ASSIGN : s_8_3 1304 # ASSIGN : s_8_4 1348 # ASSIGN : s_8_5 1346 # ASSIGN : s_8_6 1353 # ASSIGN : s_8_7 1352 # ASSIGN : s_8_8 1347 SHOW_RESULT 1358 END : 1358 (1 seconds) [Sun Jun 18 17:24:39 2006] SHOW_RESULT 1358 CPU : 0.799999999999983 = 0.799999999999983 + 0 + 0 + 0 # BOUND : makespan 1000 1358 MODIFY_CNF 1179 BEGIN : [Sun Jun 18 17:24:39 2006] MODIFY_CNF 1179 END : 128965156 bytes (0 seconds) [Sun Jun 18 17:24:39 2006] MODIFY_CNF 1179 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1179 BEGIN : [Sun Jun 18 17:24:39 2006] CMD : minisat /tmp/csp2sat10989.cnf /tmp/csp2sat10989.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1934574 5488684 | 644858 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (0 /sec) decisions : 190 (16 /sec) propagations : 323598 (27540 /sec) conflict literals : 10 (9.09 % deleted) Memory used : 213.50 MB CPU time : 11.75 s SATISFIABLE VERIFY_CNF 1179 END : (12 seconds) [Sun Jun 18 17:24:51 2006] VERIFY_CNF 1179 CPU : 12.49 = 0 + 0.01 + 11.91 + 0.57 # RESULT : makespan 1179 SATISFIABLE SHOW_RESULT 1179 BEGIN : [Sun Jun 18 17:24:51 2006] # ASSIGN : makespan 1179 # ASSIGN : s_0_0 3 # ASSIGN : s_0_1 287 # ASSIGN : s_0_2 1024 # ASSIGN : s_0_3 776 # ASSIGN : s_0_4 54 # ASSIGN : s_0_5 82 # ASSIGN : s_0_6 0 # ASSIGN : s_0_7 5 # ASSIGN : s_0_8 1 # ASSIGN : s_1_0 48 # ASSIGN : s_1_1 8 # ASSIGN : s_1_2 862 # ASSIGN : s_1_3 2 # ASSIGN : s_1_4 0 # ASSIGN : s_1_5 195 # ASSIGN : s_1_6 864 # ASSIGN : s_1_7 691 # ASSIGN : s_1_8 329 # ASSIGN : s_2_0 5 # ASSIGN : s_2_1 41 # ASSIGN : s_2_2 1168 # ASSIGN : s_2_3 11 # ASSIGN : s_2_4 612 # ASSIGN : s_2_5 376 # ASSIGN : s_2_6 1 # ASSIGN : s_2_7 6 # ASSIGN : s_2_8 2 # ASSIGN : s_3_0 1157 # ASSIGN : s_3_1 896 # ASSIGN : s_3_2 734 # ASSIGN : s_3_3 0 # ASSIGN : s_3_4 55 # ASSIGN : s_3_5 6 # ASSIGN : s_3_6 785 # ASSIGN : s_3_7 486 # ASSIGN : s_3_8 3 # ASSIGN : s_4_0 63 # ASSIGN : s_4_1 1105 # ASSIGN : s_4_2 735 # ASSIGN : s_4_3 98 # ASSIGN : s_4_4 1162 # ASSIGN : s_4_5 64 # ASSIGN : s_4_6 6 # ASSIGN : s_4_7 915 # ASSIGN : s_4_8 7 # ASSIGN : s_5_0 541 # ASSIGN : s_5_1 7 # ASSIGN : s_5_2 0 # ASSIGN : s_5_3 12 # ASSIGN : s_5_4 1 # ASSIGN : s_5_5 684 # ASSIGN : s_5_6 55 # ASSIGN : s_5_7 56 # ASSIGN : s_5_8 661 # ASSIGN : s_6_0 964 # ASSIGN : s_6_1 0 # ASSIGN : s_6_2 1169 # ASSIGN : s_6_3 1 # ASSIGN : s_6_4 2 # ASSIGN : s_6_5 1134 # ASSIGN : s_6_6 183 # ASSIGN : s_6_7 7 # ASSIGN : s_6_8 8 # ASSIGN : s_7_0 118 # ASSIGN : s_7_1 38 # ASSIGN : s_7_2 576 # ASSIGN : s_7_3 76 # ASSIGN : s_7_4 572 # ASSIGN : s_7_5 574 # ASSIGN : s_7_6 117 # ASSIGN : s_7_7 484 # ASSIGN : s_7_8 715 # ASSIGN : s_8_0 593 # ASSIGN : s_8_1 1125 # ASSIGN : s_8_2 1 # ASSIGN : s_8_3 1126 # ASSIGN : s_8_4 1167 # ASSIGN : s_8_5 1171 # ASSIGN : s_8_6 1173 # ASSIGN : s_8_7 1172 # ASSIGN : s_8_8 1178 SHOW_RESULT 1179 END : 1179 (1 seconds) [Sun Jun 18 17:24:52 2006] SHOW_RESULT 1179 CPU : 0.839999999999993 = 0.819999999999993 + 0.02 + 0 + 0 # BOUND : makespan 1000 1179 MODIFY_CNF 1089 BEGIN : [Sun Jun 18 17:24:52 2006] MODIFY_CNF 1089 END : 128965155 bytes (0 seconds) [Sun Jun 18 17:24:52 2006] MODIFY_CNF 1089 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1089 BEGIN : [Sun Jun 18 17:24:52 2006] CMD : minisat /tmp/csp2sat10989.cnf /tmp/csp2sat10989.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1817934 5138764 | 605978 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 5 (1 /sec) decisions : 8 (1 /sec) propagations : 253854 (26834 /sec) conflict literals : 6 (14.29 % deleted) Memory used : 212.00 MB CPU time : 9.46 s UNSATISFIABLE VERIFY_CNF 1089 END : (10 seconds) [Sun Jun 18 17:25:02 2006] VERIFY_CNF 1089 CPU : 10.15 = 0.00999999999999091 + 0 + 9.46 + 0.68 # RESULT : makespan 1089 UNSATISFIABLE # BOUND : makespan 1090 1179 MODIFY_CNF 1134 BEGIN : [Sun Jun 18 17:25:02 2006] MODIFY_CNF 1134 END : 128965156 bytes (0 seconds) [Sun Jun 18 17:25:02 2006] MODIFY_CNF 1134 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1134 BEGIN : [Sun Jun 18 17:25:02 2006] CMD : minisat /tmp/csp2sat10989.cnf /tmp/csp2sat10989.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1876254 5313724 | 625418 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 7 (1 /sec) decisions : 217 (24 /sec) propagations : 361430 (39805 /sec) conflict literals : 23 (4.17 % deleted) Memory used : 213.50 MB CPU time : 9.08 s SATISFIABLE VERIFY_CNF 1134 END : (10 seconds) [Sun Jun 18 17:25:12 2006] VERIFY_CNF 1134 CPU : 9.84 = 0 + 0 + 9.25 + 0.59 # RESULT : makespan 1134 SATISFIABLE SHOW_RESULT 1134 BEGIN : [Sun Jun 18 17:25:12 2006] # ASSIGN : makespan 1134 # ASSIGN : s_0_0 529 # ASSIGN : s_0_1 4 # ASSIGN : s_0_2 624 # ASSIGN : s_0_3 768 # ASSIGN : s_0_4 2 # ASSIGN : s_0_5 1016 # ASSIGN : s_0_6 3 # ASSIGN : s_0_7 1 # ASSIGN : s_0_8 1130 # ASSIGN : s_1_0 531 # ASSIGN : s_1_1 730 # ASSIGN : s_1_2 1131 # ASSIGN : s_1_3 5 # ASSIGN : s_1_4 3 # ASSIGN : s_1_5 546 # ASSIGN : s_1_6 816 # ASSIGN : s_1_7 20 # ASSIGN : s_1_8 191 # ASSIGN : s_2_0 0 # ASSIGN : s_2_1 878 # ASSIGN : s_2_2 1130 # ASSIGN : s_2_3 11 # ASSIGN : s_2_4 35 # ASSIGN : s_2_5 680 # ASSIGN : s_2_6 1 # ASSIGN : s_2_7 19 # ASSIGN : s_2_8 1131 # ASSIGN : s_3_0 113 # ASSIGN : s_3_1 493 # ASSIGN : s_3_2 1133 # ASSIGN : s_3_3 12 # ASSIGN : s_3_4 702 # ASSIGN : s_3_5 13 # ASSIGN : s_3_6 135 # ASSIGN : s_3_7 288 # ASSIGN : s_3_8 9 # ASSIGN : s_4_0 1 # ASSIGN : s_4_1 760 # ASSIGN : s_4_2 780 # ASSIGN : s_4_3 123 # ASSIGN : s_4_4 4 # ASSIGN : s_4_5 907 # ASSIGN : s_4_6 2 # ASSIGN : s_4_7 940 # ASSIGN : s_4_8 1133 # ASSIGN : s_5_0 10 # ASSIGN : s_5_1 1124 # ASSIGN : s_5_2 1129 # ASSIGN : s_5_3 1041 # ASSIGN : s_5_4 9 # ASSIGN : s_5_5 62 # ASSIGN : s_5_6 8 # ASSIGN : s_5_7 512 # ASSIGN : s_5_8 1101 # ASSIGN : s_6_0 960 # ASSIGN : s_6_1 877 # ASSIGN : s_6_2 0 # ASSIGN : s_6_3 15 # ASSIGN : s_6_4 10 # ASSIGN : s_6_5 925 # ASSIGN : s_6_6 214 # ASSIGN : s_6_7 1130 # ASSIGN : s_6_8 16 # ASSIGN : s_7_0 157 # ASSIGN : s_7_1 1126 # ASSIGN : s_7_2 986 # ASSIGN : s_7_3 101 # ASSIGN : s_7_4 33 # ASSIGN : s_7_5 1129 # ASSIGN : s_7_6 1125 # ASSIGN : s_7_7 1131 # ASSIGN : s_7_8 523 # ASSIGN : s_8_0 589 # ASSIGN : s_8_1 1125 # ASSIGN : s_8_2 10 # ASSIGN : s_8_3 1084 # ASSIGN : s_8_4 585 # ASSIGN : s_8_5 1131 # ASSIGN : s_8_6 1126 # ASSIGN : s_8_7 1133 # ASSIGN : s_8_8 1132 SHOW_RESULT 1134 END : 1134 (1 seconds) [Sun Jun 18 17:25:13 2006] SHOW_RESULT 1134 CPU : 0.959999999999989 = 0.949999999999989 + 0.01 + 0 + 0 # BOUND : makespan 1090 1134 MODIFY_CNF 1112 BEGIN : [Sun Jun 18 17:25:13 2006] MODIFY_CNF 1112 END : 128965156 bytes (0 seconds) [Sun Jun 18 17:25:13 2006] MODIFY_CNF 1112 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1112 BEGIN : [Sun Jun 18 17:25:13 2006] CMD : minisat /tmp/csp2sat10989.cnf /tmp/csp2sat10989.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1847742 5228188 | 615914 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 5 (1 /sec) decisions : 24 (3 /sec) propagations : 262465 (29792 /sec) conflict literals : 7 (0.00 % deleted) Memory used : 212.02 MB CPU time : 8.81 s UNSATISFIABLE VERIFY_CNF 1112 END : (10 seconds) [Sun Jun 18 17:25:23 2006] VERIFY_CNF 1112 CPU : 9.40999999999999 = 0 + 0 + 8.81 + 0.6 # RESULT : makespan 1112 UNSATISFIABLE # BOUND : makespan 1113 1134 MODIFY_CNF 1123 BEGIN : [Sun Jun 18 17:25:23 2006] MODIFY_CNF 1123 END : 128965156 bytes (0 seconds) [Sun Jun 18 17:25:23 2006] MODIFY_CNF 1123 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1123 BEGIN : [Sun Jun 18 17:25:23 2006] CMD : minisat /tmp/csp2sat10989.cnf /tmp/csp2sat10989.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1861998 5270956 | 620666 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 8 (1 /sec) decisions : 28 (3 /sec) propagations : 289925 (33325 /sec) conflict literals : 14 (17.65 % deleted) Memory used : 212.02 MB CPU time : 8.7 s UNSATISFIABLE VERIFY_CNF 1123 END : (9 seconds) [Sun Jun 18 17:25:32 2006] VERIFY_CNF 1123 CPU : 9.39 = 0 + 0 + 8.7 + 0.69 # RESULT : makespan 1123 UNSATISFIABLE # BOUND : makespan 1124 1134 MODIFY_CNF 1129 BEGIN : [Sun Jun 18 17:25:32 2006] MODIFY_CNF 1129 END : 128965156 bytes (0 seconds) [Sun Jun 18 17:25:32 2006] MODIFY_CNF 1129 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1129 BEGIN : [Sun Jun 18 17:25:32 2006] CMD : minisat /tmp/csp2sat10989.cnf /tmp/csp2sat10989.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1869774 5294284 | 623258 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 6 (1 /sec) decisions : 187 (21 /sec) propagations : 346953 (39382 /sec) conflict literals : 22 (4.35 % deleted) Memory used : 213.50 MB CPU time : 8.81 s SATISFIABLE VERIFY_CNF 1129 END : (10 seconds) [Sun Jun 18 17:25:42 2006] VERIFY_CNF 1129 CPU : 9.74000000000001 = 0 + 0.01 + 8.96000000000001 + 0.77 # RESULT : makespan 1129 SATISFIABLE SHOW_RESULT 1129 BEGIN : [Sun Jun 18 17:25:42 2006] # ASSIGN : makespan 1129 # ASSIGN : s_0_0 502 # ASSIGN : s_0_1 0 # ASSIGN : s_0_2 615 # ASSIGN : s_0_3 759 # ASSIGN : s_0_4 614 # ASSIGN : s_0_5 1007 # ASSIGN : s_0_6 1120 # ASSIGN : s_0_7 504 # ASSIGN : s_0_8 1127 # ASSIGN : s_1_0 526 # ASSIGN : s_1_1 712 # ASSIGN : s_1_2 1125 # ASSIGN : s_1_3 7 # ASSIGN : s_1_4 0 # ASSIGN : s_1_5 541 # ASSIGN : s_1_6 811 # ASSIGN : s_1_7 16 # ASSIGN : s_1_8 187 # ASSIGN : s_2_0 0 # ASSIGN : s_2_1 873 # ASSIGN : s_2_2 1127 # ASSIGN : s_2_3 13 # ASSIGN : s_2_4 27 # ASSIGN : s_2_5 675 # ASSIGN : s_2_6 14 # ASSIGN : s_2_7 15 # ASSIGN : s_2_8 1128 # ASSIGN : s_3_0 60 # ASSIGN : s_3_1 489 # ASSIGN : s_3_2 1 # ASSIGN : s_3_3 82 # ASSIGN : s_3_4 698 # ASSIGN : s_3_5 6 # ASSIGN : s_3_6 130 # ASSIGN : s_3_7 284 # ASSIGN : s_3_8 3 # ASSIGN : s_4_0 1 # ASSIGN : s_4_1 742 # ASSIGN : s_4_2 762 # ASSIGN : s_4_3 105 # ASSIGN : s_4_4 2 # ASSIGN : s_4_5 889 # ASSIGN : s_4_6 53 # ASSIGN : s_4_7 933 # ASSIGN : s_4_8 1126 # ASSIGN : s_5_0 2 # ASSIGN : s_5_1 1119 # ASSIGN : s_5_2 941 # ASSIGN : s_5_3 1036 # ASSIGN : s_5_4 1 # ASSIGN : s_5_5 55 # ASSIGN : s_5_6 54 # ASSIGN : s_5_7 505 # ASSIGN : s_5_8 1096 # ASSIGN : s_6_0 952 # ASSIGN : s_6_1 872 # ASSIGN : s_6_2 942 # ASSIGN : s_6_3 1122 # ASSIGN : s_6_4 7 # ASSIGN : s_6_5 907 # ASSIGN : s_6_6 209 # ASSIGN : s_6_7 1123 # ASSIGN : s_6_8 12 # ASSIGN : s_7_0 136 # ASSIGN : s_7_1 1126 # ASSIGN : s_7_2 982 # ASSIGN : s_7_3 83 # ASSIGN : s_7_4 25 # ASSIGN : s_7_5 1122 # ASSIGN : s_7_6 1121 # ASSIGN : s_7_7 1124 # ASSIGN : s_7_8 519 # ASSIGN : s_8_0 581 # ASSIGN : s_8_1 1120 # ASSIGN : s_8_2 2 # ASSIGN : s_8_3 1079 # ASSIGN : s_8_4 577 # ASSIGN : s_8_5 1128 # ASSIGN : s_8_6 1122 # ASSIGN : s_8_7 1127 # ASSIGN : s_8_8 1121 SHOW_RESULT 1129 END : 1129 (0 seconds) [Sun Jun 18 17:25:42 2006] SHOW_RESULT 1129 CPU : 0.799999999999992 = 0.789999999999992 + 0.01 + 0 + 0 # BOUND : makespan 1124 1129 MODIFY_CNF 1126 BEGIN : [Sun Jun 18 17:25:42 2006] MODIFY_CNF 1126 END : 128965156 bytes (0 seconds) [Sun Jun 18 17:25:42 2006] MODIFY_CNF 1126 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1126 BEGIN : [Sun Jun 18 17:25:42 2006] CMD : minisat /tmp/csp2sat10989.cnf /tmp/csp2sat10989.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1865886 5282620 | 621962 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 7 (1 /sec) decisions : 26 (3 /sec) propagations : 280182 (32131 /sec) conflict literals : 13 (27.78 % deleted) Memory used : 212.02 MB CPU time : 8.72 s UNSATISFIABLE VERIFY_CNF 1126 END : (10 seconds) [Sun Jun 18 17:25:52 2006] VERIFY_CNF 1126 CPU : 9.36 = 0 + 0 + 8.72 + 0.64 # RESULT : makespan 1126 UNSATISFIABLE # BOUND : makespan 1127 1129 MODIFY_CNF 1128 BEGIN : [Sun Jun 18 17:25:52 2006] MODIFY_CNF 1128 END : 128965156 bytes (0 seconds) [Sun Jun 18 17:25:52 2006] MODIFY_CNF 1128 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1128 BEGIN : [Sun Jun 18 17:25:52 2006] CMD : minisat /tmp/csp2sat10989.cnf /tmp/csp2sat10989.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1868478 5290396 | 622826 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 7 (1 /sec) decisions : 26 (3 /sec) propagations : 279710 (31967 /sec) conflict literals : 13 (27.78 % deleted) Memory used : 212.02 MB CPU time : 8.75 s UNSATISFIABLE VERIFY_CNF 1128 END : (9 seconds) [Sun Jun 18 17:26:01 2006] VERIFY_CNF 1128 CPU : 9.36 = 0 + 0 + 8.75 + 0.61 # RESULT : makespan 1128 UNSATISFIABLE # BOUND : makespan 1129 1129 MAIN END : (324 seconds) [Sun Jun 18 17:26:01 2006] MAIN CPU : 323.3 = 211.84 + 1.08 + 103.15 + 7.23