# TIMEOUT 18000 MAIN BEGIN : [Sun Jun 18 17:31:29 2006] READ BEGIN : csp/gp09-03.csp [Sun Jun 18 17:31:29 2006] READ END : csp/gp09-03.csp (2 seconds) [Sun Jun 18 17:31:31 2006] READ CPU : 1.34 = 1.33 + 0.01 + 0 + 0 # BOUND : makespan 1000 4348 GENERATE_CNF 4348 BEGIN : [Sun Jun 18 17:31:31 2006] GENERATE_CNF 4348 END : 357077 variables 6121380 clauses 146022716 bytes (235 seconds) [Sun Jun 18 17:35:26 2006] GENERATE_CNF 4348 CPU : 234.46 = 233.21 + 1.25 + 0 + 0 MODIFY_CNF 2674 BEGIN : [Sun Jun 18 17:35:26 2006] MODIFY_CNF 2674 END : 146022723 bytes (0 seconds) [Sun Jun 18 17:35:26 2006] MODIFY_CNF 2674 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 2674 BEGIN : [Sun Jun 18 17:35:26 2006] CMD : minisat /tmp/csp2sat11196.cnf /tmp/csp2sat11196.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 3950008 11495790 | 1316669 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 1 (0 /sec) decisions : 600 (62 /sec) propagations : 374338 (38832 /sec) conflict literals : 9 (0.00 % deleted) Memory used : 240.46 MB CPU time : 9.64 s SATISFIABLE VERIFY_CNF 2674 END : (10 seconds) [Sun Jun 18 17:35:36 2006] VERIFY_CNF 2674 CPU : 10.54 = 0 + 0 + 9.81 + 0.73 # RESULT : makespan 2674 SATISFIABLE SHOW_RESULT 2674 BEGIN : [Sun Jun 18 17:35:36 2006] # ASSIGN : makespan 2674 # ASSIGN : s_0_0 860 # ASSIGN : s_0_1 76 # ASSIGN : s_0_2 31 # ASSIGN : s_0_3 32 # ASSIGN : s_0_4 66 # ASSIGN : s_0_5 68 # ASSIGN : s_0_6 973 # ASSIGN : s_0_7 1277 # ASSIGN : s_0_8 1556 # ASSIGN : s_1_0 935 # ASSIGN : s_1_1 267 # ASSIGN : s_1_2 268 # ASSIGN : s_1_3 33 # ASSIGN : s_1_4 241 # ASSIGN : s_1_5 242 # ASSIGN : s_1_6 974 # ASSIGN : s_1_7 1278 # ASSIGN : s_1_8 2276 # ASSIGN : s_2_0 974 # ASSIGN : s_2_1 300 # ASSIGN : s_2_2 957 # ASSIGN : s_2_3 813 # ASSIGN : s_2_4 958 # ASSIGN : s_2_5 972 # ASSIGN : s_2_6 975 # ASSIGN : s_2_7 1335 # ASSIGN : s_2_8 2277 # ASSIGN : s_3_0 1603 # ASSIGN : s_3_1 305 # ASSIGN : s_3_2 1071 # ASSIGN : s_3_3 1073 # ASSIGN : s_3_4 1075 # ASSIGN : s_3_5 1080 # ASSIGN : s_3_6 1730 # ASSIGN : s_3_7 1807 # ASSIGN : s_3_8 2278 # ASSIGN : s_4_0 1909 # ASSIGN : s_4_1 990 # ASSIGN : s_4_2 1072 # ASSIGN : s_4_3 1074 # ASSIGN : s_4_4 1076 # ASSIGN : s_4_5 1081 # ASSIGN : s_4_6 1905 # ASSIGN : s_4_7 1906 # ASSIGN : s_4_8 2286 # ASSIGN : s_5_0 2288 # ASSIGN : s_5_1 1022 # ASSIGN : s_5_2 1105 # ASSIGN : s_5_3 1122 # ASSIGN : s_5_4 1134 # ASSIGN : s_5_5 1658 # ASSIGN : s_5_6 1923 # ASSIGN : s_5_7 1925 # ASSIGN : s_5_8 2287 # ASSIGN : s_6_0 2291 # ASSIGN : s_6_1 1170 # ASSIGN : s_6_2 1171 # ASSIGN : s_6_3 1179 # ASSIGN : s_6_4 1519 # ASSIGN : s_6_5 1990 # ASSIGN : s_6_6 2110 # ASSIGN : s_6_7 2157 # ASSIGN : s_6_8 2288 # ASSIGN : s_7_0 2667 # ASSIGN : s_7_1 1378 # ASSIGN : s_7_2 1379 # ASSIGN : s_7_3 1538 # ASSIGN : s_7_4 1539 # ASSIGN : s_7_5 2110 # ASSIGN : s_7_6 2111 # ASSIGN : s_7_7 2402 # ASSIGN : s_7_8 2403 # ASSIGN : s_8_0 2668 # ASSIGN : s_8_1 1674 # ASSIGN : s_8_2 1675 # ASSIGN : s_8_3 1819 # ASSIGN : s_8_4 2110 # ASSIGN : s_8_5 2111 # ASSIGN : s_8_6 2112 # ASSIGN : s_8_7 2669 # ASSIGN : s_8_8 2673 SHOW_RESULT 2674 END : 2674 (2 seconds) [Sun Jun 18 17:35:38 2006] SHOW_RESULT 2674 CPU : 1.39999999999998 = 1.33999999999997 + 0.0600000000000001 + 0 + 0 # BOUND : makespan 1000 2674 MODIFY_CNF 1837 BEGIN : [Sun Jun 18 17:35:38 2006] MODIFY_CNF 1837 END : 146022722 bytes (0 seconds) [Sun Jun 18 17:35:38 2006] MODIFY_CNF 1837 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1837 BEGIN : [Sun Jun 18 17:35:38 2006] CMD : minisat /tmp/csp2sat11196.cnf /tmp/csp2sat11196.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 2865256 8241534 | 955085 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (0 /sec) decisions : 476 (40 /sec) propagations : 418546 (35231 /sec) conflict literals : 17 (0.00 % deleted) Memory used : 240.46 MB CPU time : 11.88 s SATISFIABLE VERIFY_CNF 1837 END : (13 seconds) [Sun Jun 18 17:35:51 2006] VERIFY_CNF 1837 CPU : 12.81 = 0 + 0 + 12.05 + 0.76 # RESULT : makespan 1837 SATISFIABLE SHOW_RESULT 1837 BEGIN : [Sun Jun 18 17:35:51 2006] # ASSIGN : makespan 1837 # ASSIGN : s_0_0 1054 # ASSIGN : s_0_1 78 # ASSIGN : s_0_2 7 # ASSIGN : s_0_3 0 # ASSIGN : s_0_4 1 # ASSIGN : s_0_5 8 # ASSIGN : s_0_6 16 # ASSIGN : s_0_7 294 # ASSIGN : s_0_8 299 # ASSIGN : s_1_0 22 # ASSIGN : s_1_1 269 # ASSIGN : s_1_2 352 # ASSIGN : s_1_3 61 # ASSIGN : s_1_4 3 # ASSIGN : s_1_5 270 # ASSIGN : s_1_6 17 # ASSIGN : s_1_7 295 # ASSIGN : s_1_8 1019 # ASSIGN : s_2_0 2 # ASSIGN : s_2_1 399 # ASSIGN : s_2_2 3 # ASSIGN : s_2_3 876 # ASSIGN : s_2_4 4 # ASSIGN : s_2_5 378 # ASSIGN : s_2_6 18 # ASSIGN : s_2_7 404 # ASSIGN : s_2_8 1020 # ASSIGN : s_3_0 537 # ASSIGN : s_3_1 1029 # ASSIGN : s_3_2 73 # ASSIGN : s_3_3 1020 # ASSIGN : s_3_4 75 # ASSIGN : s_3_5 380 # ASSIGN : s_3_6 381 # ASSIGN : s_3_7 921 # ASSIGN : s_3_8 1021 # ASSIGN : s_4_0 81 # ASSIGN : s_4_1 1714 # ASSIGN : s_4_2 74 # ASSIGN : s_4_3 1036 # ASSIGN : s_4_4 76 # ASSIGN : s_4_5 459 # ASSIGN : s_4_6 458 # ASSIGN : s_4_7 1046 # ASSIGN : s_4_8 1049 # ASSIGN : s_5_0 664 # ASSIGN : s_5_1 1746 # ASSIGN : s_5_2 1021 # ASSIGN : s_5_3 1038 # ASSIGN : s_5_4 169 # ASSIGN : s_5_5 1203 # ASSIGN : s_5_6 554 # ASSIGN : s_5_7 1468 # ASSIGN : s_5_8 1050 # ASSIGN : s_6_0 667 # ASSIGN : s_6_1 1836 # ASSIGN : s_6_2 1043 # ASSIGN : s_6_3 1054 # ASSIGN : s_6_4 1560 # ASSIGN : s_6_5 1580 # ASSIGN : s_6_6 556 # ASSIGN : s_6_7 1700 # ASSIGN : s_6_8 1051 # ASSIGN : s_7_0 1129 # ASSIGN : s_7_1 1829 # ASSIGN : s_7_2 1527 # ASSIGN : s_7_3 1394 # ASSIGN : s_7_4 558 # ASSIGN : s_7_5 1830 # ASSIGN : s_7_6 557 # ASSIGN : s_7_7 1831 # ASSIGN : s_7_8 1130 # ASSIGN : s_8_0 1394 # ASSIGN : s_8_1 837 # ASSIGN : s_8_2 1686 # ASSIGN : s_8_3 1395 # ASSIGN : s_8_4 1830 # ASSIGN : s_8_5 1831 # ASSIGN : s_8_6 838 # ASSIGN : s_8_7 1832 # ASSIGN : s_8_8 1836 SHOW_RESULT 1837 END : 1837 (1 seconds) [Sun Jun 18 17:35:52 2006] SHOW_RESULT 1837 CPU : 1.57 = 1.56 + 0.01 + 0 + 0 # BOUND : makespan 1000 1837 MODIFY_CNF 1418 BEGIN : [Sun Jun 18 17:35:52 2006] MODIFY_CNF 1418 END : 146022722 bytes (0 seconds) [Sun Jun 18 17:35:52 2006] MODIFY_CNF 1418 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1418 BEGIN : [Sun Jun 18 17:35:52 2006] CMD : minisat /tmp/csp2sat11196.cnf /tmp/csp2sat11196.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 2322232 6612462 | 774077 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (0 /sec) decisions : 322 (30 /sec) propagations : 368048 (34494 /sec) conflict literals : 14 (0.00 % deleted) Memory used : 240.46 MB CPU time : 10.67 s SATISFIABLE VERIFY_CNF 1418 END : (12 seconds) [Sun Jun 18 17:36:04 2006] VERIFY_CNF 1418 CPU : 11.73 = 0 + 0 + 10.84 + 0.89 # RESULT : makespan 1418 SATISFIABLE SHOW_RESULT 1418 BEGIN : [Sun Jun 18 17:36:04 2006] # ASSIGN : makespan 1418 # ASSIGN : s_0_0 878 # ASSIGN : s_0_1 953 # ASSIGN : s_0_2 0 # ASSIGN : s_0_3 1 # ASSIGN : s_0_4 20 # ASSIGN : s_0_5 28 # ASSIGN : s_0_6 2 # ASSIGN : s_0_7 157 # ASSIGN : s_0_8 158 # ASSIGN : s_1_0 7 # ASSIGN : s_1_1 6 # ASSIGN : s_1_2 320 # ASSIGN : s_1_3 55 # ASSIGN : s_1_4 54 # ASSIGN : s_1_5 1392 # ASSIGN : s_1_6 1417 # ASSIGN : s_1_7 263 # ASSIGN : s_1_8 1009 # ASSIGN : s_2_0 46 # ASSIGN : s_2_1 10 # ASSIGN : s_2_2 1 # ASSIGN : s_2_3 1247 # ASSIGN : s_2_4 22 # ASSIGN : s_2_5 36 # ASSIGN : s_2_6 80 # ASSIGN : s_2_7 440 # ASSIGN : s_2_8 1010 # ASSIGN : s_3_0 1019 # ASSIGN : s_3_1 227 # ASSIGN : s_3_2 2 # ASSIGN : s_3_3 1405 # ASSIGN : s_3_4 0 # ASSIGN : s_3_5 1 # ASSIGN : s_3_6 3 # ASSIGN : s_3_7 912 # ASSIGN : s_3_8 1011 # ASSIGN : s_4_0 47 # ASSIGN : s_4_1 15 # ASSIGN : s_4_2 12 # ASSIGN : s_4_3 1391 # ASSIGN : s_4_4 1393 # ASSIGN : s_4_5 453 # ASSIGN : s_4_6 452 # ASSIGN : s_4_7 1030 # ASSIGN : s_4_8 1033 # ASSIGN : s_5_0 424 # ASSIGN : s_5_1 76 # ASSIGN : s_5_2 14 # ASSIGN : s_5_3 1406 # ASSIGN : s_5_4 649 # ASSIGN : s_5_5 159 # ASSIGN : s_5_6 647 # ASSIGN : s_5_7 1035 # ASSIGN : s_5_8 1034 # ASSIGN : s_6_0 427 # ASSIGN : s_6_1 1144 # ASSIGN : s_6_2 31 # ASSIGN : s_6_3 804 # ASSIGN : s_6_4 1398 # ASSIGN : s_6_5 39 # ASSIGN : s_6_6 803 # ASSIGN : s_6_7 1267 # ASSIGN : s_6_8 1145 # ASSIGN : s_7_0 1146 # ASSIGN : s_7_1 1147 # ASSIGN : s_7_2 987 # ASSIGN : s_7_3 803 # ASSIGN : s_7_4 78 # ASSIGN : s_7_5 38 # ASSIGN : s_7_6 854 # ASSIGN : s_7_7 1412 # ASSIGN : s_7_8 1148 # ASSIGN : s_8_0 1411 # ASSIGN : s_8_1 1412 # ASSIGN : s_8_2 176 # ASSIGN : s_8_3 512 # ASSIGN : s_8_4 77 # ASSIGN : s_8_5 452 # ASSIGN : s_8_6 855 # ASSIGN : s_8_7 1413 # ASSIGN : s_8_8 1417 SHOW_RESULT 1418 END : 1418 (1 seconds) [Sun Jun 18 17:36:05 2006] SHOW_RESULT 1418 CPU : 1.53000000000002 = 1.51000000000002 + 0.02 + 0 + 0 # BOUND : makespan 1000 1418 MODIFY_CNF 1209 BEGIN : [Sun Jun 18 17:36:06 2006] MODIFY_CNF 1209 END : 146022722 bytes (0 seconds) [Sun Jun 18 17:36:06 2006] MODIFY_CNF 1209 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1209 BEGIN : [Sun Jun 18 17:36:06 2006] CMD : minisat /tmp/csp2sat11196.cnf /tmp/csp2sat11196.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 2051368 5799870 | 683789 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 1 (0 /sec) decisions : 268 (24 /sec) propagations : 374060 (34005 /sec) conflict literals : 5 (0.00 % deleted) Memory used : 240.46 MB CPU time : 11 s SATISFIABLE VERIFY_CNF 1209 END : (12 seconds) [Sun Jun 18 17:36:18 2006] VERIFY_CNF 1209 CPU : 11.98 = 0 + 0 + 11.19 + 0.79 # RESULT : makespan 1209 SATISFIABLE SHOW_RESULT 1209 BEGIN : [Sun Jun 18 17:36:18 2006] # ASSIGN : makespan 1209 # ASSIGN : s_0_0 1125 # ASSIGN : s_0_1 934 # ASSIGN : s_0_2 5 # ASSIGN : s_0_3 763 # ASSIGN : s_0_4 6 # ASSIGN : s_0_5 35 # ASSIGN : s_0_6 8 # ASSIGN : s_0_7 9 # ASSIGN : s_0_8 43 # ASSIGN : s_1_0 959 # ASSIGN : s_1_1 3 # ASSIGN : s_1_2 292 # ASSIGN : s_1_3 12 # ASSIGN : s_1_4 10 # ASSIGN : s_1_5 1178 # ASSIGN : s_1_6 11 # ASSIGN : s_1_7 1016 # ASSIGN : s_1_8 0 # ASSIGN : s_2_0 3 # ASSIGN : s_2_1 4 # ASSIGN : s_2_2 0 # ASSIGN : s_2_3 619 # ASSIGN : s_2_4 34 # ASSIGN : s_2_5 48 # ASSIGN : s_2_6 849 # ASSIGN : s_2_7 109 # ASSIGN : s_2_8 1 # ASSIGN : s_3_0 998 # ASSIGN : s_3_1 248 # ASSIGN : s_3_2 1 # ASSIGN : s_3_3 1176 # ASSIGN : s_3_4 111 # ASSIGN : s_3_5 1177 # ASSIGN : s_3_6 112 # ASSIGN : s_3_7 10 # ASSIGN : s_3_8 2 # ASSIGN : s_4_0 180 # ASSIGN : s_4_1 9 # ASSIGN : s_4_2 6 # ASSIGN : s_4_3 579 # ASSIGN : s_4_4 166 # ASSIGN : s_4_5 600 # ASSIGN : s_4_6 41 # ASSIGN : s_4_7 581 # ASSIGN : s_4_8 42 # ASSIGN : s_5_0 557 # ASSIGN : s_5_1 87 # ASSIGN : s_5_2 16 # ASSIGN : s_5_3 0 # ASSIGN : s_5_4 817 # ASSIGN : s_5_5 292 # ASSIGN : s_5_6 189 # ASSIGN : s_5_7 584 # ASSIGN : s_5_8 816 # ASSIGN : s_6_0 560 # ASSIGN : s_6_1 170 # ASSIGN : s_6_2 8 # ASSIGN : s_6_3 220 # ASSIGN : s_6_4 171 # ASSIGN : s_6_5 50 # ASSIGN : s_6_6 191 # ASSIGN : s_6_7 1073 # ASSIGN : s_6_8 936 # ASSIGN : s_7_0 938 # ASSIGN : s_7_1 933 # ASSIGN : s_7_2 33 # ASSIGN : s_7_3 764 # ASSIGN : s_7_4 193 # ASSIGN : s_7_5 1203 # ASSIGN : s_7_6 192 # ASSIGN : s_7_7 1204 # ASSIGN : s_7_8 939 # ASSIGN : s_8_0 1200 # ASSIGN : s_8_1 1201 # ASSIGN : s_8_2 1056 # ASSIGN : s_8_3 765 # ASSIGN : s_8_4 1202 # ASSIGN : s_8_5 1204 # ASSIGN : s_8_6 209 # ASSIGN : s_8_7 1205 # ASSIGN : s_8_8 1203 SHOW_RESULT 1209 END : 1209 (1 seconds) [Sun Jun 18 17:36:19 2006] SHOW_RESULT 1209 CPU : 1.53 = 1.53 + 0 + 0 + 0 # BOUND : makespan 1000 1209 MODIFY_CNF 1104 BEGIN : [Sun Jun 18 17:36:19 2006] MODIFY_CNF 1104 END : 146022722 bytes (0 seconds) [Sun Jun 18 17:36:19 2006] MODIFY_CNF 1104 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1104 BEGIN : [Sun Jun 18 17:36:19 2006] CMD : minisat /tmp/csp2sat11196.cnf /tmp/csp2sat11196.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1915288 5391630 | 638429 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 6 (1 /sec) decisions : 32 (3 /sec) propagations : 366959 (31634 /sec) conflict literals : 20 (9.09 % deleted) Memory used : 238.88 MB CPU time : 11.6 s UNSATISFIABLE VERIFY_CNF 1104 END : (12 seconds) [Sun Jun 18 17:36:31 2006] VERIFY_CNF 1104 CPU : 12.37 = 0 + 0.01 + 11.6 + 0.76 # RESULT : makespan 1104 UNSATISFIABLE # BOUND : makespan 1105 1209 MODIFY_CNF 1157 BEGIN : [Sun Jun 18 17:36:31 2006] MODIFY_CNF 1157 END : 146022722 bytes (0 seconds) [Sun Jun 18 17:36:31 2006] MODIFY_CNF 1157 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1157 BEGIN : [Sun Jun 18 17:36:31 2006] CMD : minisat /tmp/csp2sat11196.cnf /tmp/csp2sat11196.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1983976 5597694 | 661325 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 6 (1 /sec) decisions : 293 (25 /sec) propagations : 398650 (34545 /sec) conflict literals : 34 (5.56 % deleted) Memory used : 240.46 MB CPU time : 11.54 s SATISFIABLE VERIFY_CNF 1157 END : (13 seconds) [Sun Jun 18 17:36:44 2006] VERIFY_CNF 1157 CPU : 12.47 = 0.0100000000000193 + 0 + 11.73 + 0.73 # RESULT : makespan 1157 SATISFIABLE SHOW_RESULT 1157 BEGIN : [Sun Jun 18 17:36:44 2006] # ASSIGN : makespan 1157 # ASSIGN : s_0_0 881 # ASSIGN : s_0_1 956 # ASSIGN : s_0_2 880 # ASSIGN : s_0_3 6 # ASSIGN : s_0_4 17 # ASSIGN : s_0_5 20 # ASSIGN : s_0_6 14 # ASSIGN : s_0_7 16 # ASSIGN : s_0_8 28 # ASSIGN : s_1_0 89 # ASSIGN : s_1_1 88 # ASSIGN : s_1_2 213 # ASSIGN : s_1_3 949 # ASSIGN : s_1_4 2 # ASSIGN : s_1_5 188 # ASSIGN : s_1_6 0 # ASSIGN : s_1_7 26 # ASSIGN : s_1_8 1 # ASSIGN : s_2_0 1 # ASSIGN : s_2_1 227 # ASSIGN : s_2_2 17 # ASSIGN : s_2_3 21 # ASSIGN : s_2_4 3 # ASSIGN : s_2_5 18 # ASSIGN : s_2_6 791 # ASSIGN : s_2_7 319 # ASSIGN : s_2_8 2 # ASSIGN : s_3_0 1022 # ASSIGN : s_3_1 232 # ASSIGN : s_3_2 16 # ASSIGN : s_3_3 7 # ASSIGN : s_3_4 19 # ASSIGN : s_3_5 231 # ASSIGN : s_3_6 25 # ASSIGN : s_3_7 917 # ASSIGN : s_3_8 8 # ASSIGN : s_4_0 128 # ASSIGN : s_4_1 96 # ASSIGN : s_4_2 11 # ASSIGN : s_4_3 13 # ASSIGN : s_4_4 20 # ASSIGN : s_4_5 580 # ASSIGN : s_4_6 15 # ASSIGN : s_4_7 17 # ASSIGN : s_4_8 27 # ASSIGN : s_5_0 1153 # ASSIGN : s_5_1 0 # ASSIGN : s_5_2 1134 # ASSIGN : s_5_3 646 # ASSIGN : s_5_4 749 # ASSIGN : s_5_5 315 # ASSIGN : s_5_6 1151 # ASSIGN : s_5_7 83 # ASSIGN : s_5_8 748 # ASSIGN : s_6_0 505 # ASSIGN : s_6_1 1147 # ASSIGN : s_6_2 3 # ASSIGN : s_6_3 165 # ASSIGN : s_6_4 25 # ASSIGN : s_6_5 45 # ASSIGN : s_6_6 16 # ASSIGN : s_6_7 1016 # ASSIGN : s_6_8 881 # ASSIGN : s_7_0 1149 # ASSIGN : s_7_1 1148 # ASSIGN : s_7_2 18 # ASSIGN : s_7_3 16 # ASSIGN : s_7_4 178 # ASSIGN : s_7_5 177 # ASSIGN : s_7_6 17 # ASSIGN : s_7_7 1150 # ASSIGN : s_7_8 884 # ASSIGN : s_8_0 1156 # ASSIGN : s_8_1 1149 # ASSIGN : s_8_2 990 # ASSIGN : s_8_3 658 # ASSIGN : s_8_4 1150 # ASSIGN : s_8_5 44 # ASSIGN : s_8_6 102 # ASSIGN : s_8_7 1151 # ASSIGN : s_8_8 1155 SHOW_RESULT 1157 END : 1157 (1 seconds) [Sun Jun 18 17:36:45 2006] SHOW_RESULT 1157 CPU : 1.50999999999999 = 1.50999999999999 + 0 + 0 + 0 # BOUND : makespan 1105 1157 MODIFY_CNF 1131 BEGIN : [Sun Jun 18 17:36:45 2006] MODIFY_CNF 1131 END : 146022722 bytes (0 seconds) [Sun Jun 18 17:36:45 2006] MODIFY_CNF 1131 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1131 BEGIN : [Sun Jun 18 17:36:45 2006] CMD : minisat /tmp/csp2sat11196.cnf /tmp/csp2sat11196.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1950280 5496606 | 650093 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 9 (1 /sec) decisions : 260 (23 /sec) propagations : 400318 (34780 /sec) conflict literals : 83 (5.68 % deleted) Memory used : 240.46 MB CPU time : 11.51 s SATISFIABLE VERIFY_CNF 1131 END : (13 seconds) [Sun Jun 18 17:36:58 2006] VERIFY_CNF 1131 CPU : 12.51 = 0 + 0.00999999999999979 + 11.68 + 0.82 # RESULT : makespan 1131 SATISFIABLE SHOW_RESULT 1131 BEGIN : [Sun Jun 18 17:36:58 2006] # ASSIGN : makespan 1131 # ASSIGN : s_0_0 1047 # ASSIGN : s_0_1 805 # ASSIGN : s_0_2 0 # ASSIGN : s_0_3 1 # ASSIGN : s_0_4 734 # ASSIGN : s_0_5 996 # ASSIGN : s_0_6 13 # ASSIGN : s_0_7 3 # ASSIGN : s_0_8 14 # ASSIGN : s_1_0 783 # ASSIGN : s_1_1 1130 # ASSIGN : s_1_2 32 # ASSIGN : s_1_3 915 # ASSIGN : s_1_4 725 # ASSIGN : s_1_5 6 # ASSIGN : s_1_6 31 # ASSIGN : s_1_7 726 # ASSIGN : s_1_8 1 # ASSIGN : s_2_0 1 # ASSIGN : s_2_1 1125 # ASSIGN : s_2_2 3 # ASSIGN : s_2_3 476 # ASSIGN : s_2_4 620 # ASSIGN : s_2_5 994 # ASSIGN : s_2_6 634 # ASSIGN : s_2_7 4 # ASSIGN : s_2_8 2 # ASSIGN : s_3_0 822 # ASSIGN : s_3_1 120 # ASSIGN : s_3_2 4 # ASSIGN : s_3_3 2 # ASSIGN : s_3_4 3 # ASSIGN : s_3_5 1130 # ASSIGN : s_3_6 1048 # ASSIGN : s_3_7 949 # ASSIGN : s_3_8 5 # ASSIGN : s_4_0 27 # ASSIGN : s_4_1 1089 # ASSIGN : s_4_2 5 # ASSIGN : s_4_3 11 # ASSIGN : s_4_4 1121 # ASSIGN : s_4_5 417 # ASSIGN : s_4_6 1129 # ASSIGN : s_4_7 0 # ASSIGN : s_4_8 13 # ASSIGN : s_5_0 404 # ASSIGN : s_5_1 37 # ASSIGN : s_5_2 7 # ASSIGN : s_5_3 25 # ASSIGN : s_5_4 736 # ASSIGN : s_5_5 139 # ASSIGN : s_5_6 1127 # ASSIGN : s_5_7 494 # ASSIGN : s_5_8 735 # ASSIGN : s_6_0 407 # ASSIGN : s_6_1 3 # ASSIGN : s_6_2 24 # ASSIGN : s_6_3 67 # ASSIGN : s_6_4 4 # ASSIGN : s_6_5 1004 # ASSIGN : s_6_6 1130 # ASSIGN : s_6_7 818 # ASSIGN : s_6_8 815 # ASSIGN : s_7_0 1122 # ASSIGN : s_7_1 36 # ASSIGN : s_7_2 699 # ASSIGN : s_7_3 1123 # ASSIGN : s_7_4 49 # ASSIGN : s_7_5 1124 # ASSIGN : s_7_6 1125 # ASSIGN : s_7_7 1126 # ASSIGN : s_7_8 858 # ASSIGN : s_8_0 1123 # ASSIGN : s_8_1 1124 # ASSIGN : s_8_2 978 # ASSIGN : s_8_3 624 # ASSIGN : s_8_4 1126 # ASSIGN : s_8_5 1125 # ASSIGN : s_8_6 68 # ASSIGN : s_8_7 1127 # ASSIGN : s_8_8 1122 SHOW_RESULT 1131 END : 1131 (2 seconds) [Sun Jun 18 17:37:00 2006] SHOW_RESULT 1131 CPU : 1.55000000000002 = 1.54000000000002 + 0.01 + 0 + 0 # BOUND : makespan 1105 1131 MODIFY_CNF 1118 BEGIN : [Sun Jun 18 17:37:00 2006] MODIFY_CNF 1118 END : 146022722 bytes (0 seconds) [Sun Jun 18 17:37:00 2006] MODIFY_CNF 1118 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1118 BEGIN : [Sun Jun 18 17:37:00 2006] CMD : minisat /tmp/csp2sat11196.cnf /tmp/csp2sat11196.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1933432 5446062 | 644477 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 3 (0 /sec) decisions : 126 (11 /sec) propagations : 386064 (32745 /sec) conflict literals : 22 (15.38 % deleted) Memory used : 240.46 MB CPU time : 11.79 s SATISFIABLE VERIFY_CNF 1118 END : (12 seconds) [Sun Jun 18 17:37:12 2006] VERIFY_CNF 1118 CPU : 12.88 = 0 + 0 + 11.97 + 0.909999999999999 # RESULT : makespan 1118 SATISFIABLE SHOW_RESULT 1118 BEGIN : [Sun Jun 18 17:37:12 2006] # ASSIGN : makespan 1118 # ASSIGN : s_0_0 1031 # ASSIGN : s_0_1 840 # ASSIGN : s_0_2 1116 # ASSIGN : s_0_3 0 # ASSIGN : s_0_4 8 # ASSIGN : s_0_5 1106 # ASSIGN : s_0_6 10 # ASSIGN : s_0_7 1 # ASSIGN : s_0_8 11 # ASSIGN : s_1_0 775 # ASSIGN : s_1_1 839 # ASSIGN : s_1_2 26 # ASSIGN : s_1_3 909 # ASSIGN : s_1_4 717 # ASSIGN : s_1_5 1 # ASSIGN : s_1_6 1117 # ASSIGN : s_1_7 718 # ASSIGN : s_1_8 0 # ASSIGN : s_2_0 0 # ASSIGN : s_2_1 1077 # ASSIGN : s_2_2 1117 # ASSIGN : s_2_3 474 # ASSIGN : s_2_4 666 # ASSIGN : s_2_5 1114 # ASSIGN : s_2_6 680 # ASSIGN : s_2_7 2 # ASSIGN : s_2_8 1 # ASSIGN : s_3_0 814 # ASSIGN : s_3_1 129 # ASSIGN : s_3_2 0 # ASSIGN : s_3_3 1 # ASSIGN : s_3_4 10 # ASSIGN : s_3_5 127 # ASSIGN : s_3_6 1040 # ASSIGN : s_3_7 941 # ASSIGN : s_3_8 2 # ASSIGN : s_4_0 16 # ASSIGN : s_4_1 1082 # ASSIGN : s_4_2 970 # ASSIGN : s_4_3 7 # ASSIGN : s_4_4 11 # ASSIGN : s_4_5 393 # ASSIGN : s_4_6 9 # ASSIGN : s_4_7 1114 # ASSIGN : s_4_8 10 # ASSIGN : s_5_0 396 # ASSIGN : s_5_1 45 # ASSIGN : s_5_2 1 # ASSIGN : s_5_3 31 # ASSIGN : s_5_4 732 # ASSIGN : s_5_5 128 # ASSIGN : s_5_6 43 # ASSIGN : s_5_7 486 # ASSIGN : s_5_8 731 # ASSIGN : s_6_0 399 # ASSIGN : s_6_1 17 # ASSIGN : s_6_2 18 # ASSIGN : s_6_3 59 # ASSIGN : s_6_4 38 # ASSIGN : s_6_5 986 # ASSIGN : s_6_6 58 # ASSIGN : s_6_7 806 # ASSIGN : s_6_8 803 # ASSIGN : s_7_0 15 # ASSIGN : s_7_1 43 # ASSIGN : s_7_2 693 # ASSIGN : s_7_3 58 # ASSIGN : s_7_4 95 # ASSIGN : s_7_5 1116 # ASSIGN : s_7_6 679 # ASSIGN : s_7_7 1117 # ASSIGN : s_7_8 852 # ASSIGN : s_8_0 971 # ASSIGN : s_8_1 44 # ASSIGN : s_8_2 972 # ASSIGN : s_8_3 618 # ASSIGN : s_8_4 1117 # ASSIGN : s_8_5 61 # ASSIGN : s_8_6 62 # ASSIGN : s_8_7 937 # ASSIGN : s_8_8 1116 SHOW_RESULT 1118 END : 1118 (2 seconds) [Sun Jun 18 17:37:14 2006] SHOW_RESULT 1118 CPU : 1.53 = 1.5 + 0.03 + 0 + 0 # BOUND : makespan 1105 1118 MODIFY_CNF 1111 BEGIN : [Sun Jun 18 17:37:14 2006] MODIFY_CNF 1111 END : 146022722 bytes (0 seconds) [Sun Jun 18 17:37:14 2006] MODIFY_CNF 1111 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1111 BEGIN : [Sun Jun 18 17:37:14 2006] CMD : minisat /tmp/csp2sat11196.cnf /tmp/csp2sat11196.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1924360 5418846 | 641453 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 7 (1 /sec) decisions : 34 (3 /sec) propagations : 346028 (29677 /sec) conflict literals : 24 (7.69 % deleted) Memory used : 238.90 MB CPU time : 11.66 s UNSATISFIABLE VERIFY_CNF 1111 END : (12 seconds) [Sun Jun 18 17:37:26 2006] VERIFY_CNF 1111 CPU : 12.29 = 0 + 0 + 11.66 + 0.63 # RESULT : makespan 1111 UNSATISFIABLE # BOUND : makespan 1112 1118 MODIFY_CNF 1115 BEGIN : [Sun Jun 18 17:37:26 2006] MODIFY_CNF 1115 END : 146022722 bytes (0 seconds) [Sun Jun 18 17:37:26 2006] MODIFY_CNF 1115 CPU : 0.01 = 0 + 0.01 + 0 + 0 VERIFY_CNF 1115 BEGIN : [Sun Jun 18 17:37:26 2006] CMD : minisat /tmp/csp2sat11196.cnf /tmp/csp2sat11196.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1929544 5434398 | 643181 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 12 (1 /sec) decisions : 164 (14 /sec) propagations : 422010 (36412 /sec) conflict literals : 64 (12.33 % deleted) Memory used : 240.46 MB CPU time : 11.59 s SATISFIABLE VERIFY_CNF 1115 END : (13 seconds) [Sun Jun 18 17:37:39 2006] VERIFY_CNF 1115 CPU : 12.63 = 0 + 0 + 11.76 + 0.87 # RESULT : makespan 1115 SATISFIABLE SHOW_RESULT 1115 BEGIN : [Sun Jun 18 17:37:39 2006] # ASSIGN : makespan 1115 # ASSIGN : s_0_0 1034 # ASSIGN : s_0_1 843 # ASSIGN : s_0_2 1112 # ASSIGN : s_0_3 7 # ASSIGN : s_0_4 22 # ASSIGN : s_0_5 12 # ASSIGN : s_0_6 24 # ASSIGN : s_0_7 25 # ASSIGN : s_0_8 123 # ASSIGN : s_1_0 995 # ASSIGN : s_1_1 20 # ASSIGN : s_1_2 256 # ASSIGN : s_1_3 48 # ASSIGN : s_1_4 21 # ASSIGN : s_1_5 23 # ASSIGN : s_1_6 22 # ASSIGN : s_1_7 923 # ASSIGN : s_1_8 0 # ASSIGN : s_2_0 0 # ASSIGN : s_2_1 2 # ASSIGN : s_2_2 964 # ASSIGN : s_2_3 968 # ASSIGN : s_2_4 7 # ASSIGN : s_2_5 21 # ASSIGN : s_2_6 604 # ASSIGN : s_2_7 26 # ASSIGN : s_2_8 1 # ASSIGN : s_3_0 10 # ASSIGN : s_3_1 137 # ASSIGN : s_3_2 963 # ASSIGN : s_3_3 967 # ASSIGN : s_3_4 0 # ASSIGN : s_3_5 1 # ASSIGN : s_3_6 1037 # ASSIGN : s_3_7 824 # ASSIGN : s_3_8 2 # ASSIGN : s_4_0 159 # ASSIGN : s_4_1 105 # ASSIGN : s_4_2 1113 # ASSIGN : s_4_3 0 # ASSIGN : s_4_4 2 # ASSIGN : s_4_5 536 # ASSIGN : s_4_6 19 # ASSIGN : s_4_7 22 # ASSIGN : s_4_8 104 # ASSIGN : s_5_0 156 # ASSIGN : s_5_1 22 # ASSIGN : s_5_2 216 # ASSIGN : s_5_3 8 # ASSIGN : s_5_4 730 # ASSIGN : s_5_5 233 # ASSIGN : s_5_6 20 # ASSIGN : s_5_7 498 # ASSIGN : s_5_8 109 # ASSIGN : s_6_0 604 # ASSIGN : s_6_1 21 # ASSIGN : s_6_2 248 # ASSIGN : s_6_3 264 # ASSIGN : s_6_4 27 # ASSIGN : s_6_5 113 # ASSIGN : s_6_6 47 # ASSIGN : s_6_7 980 # ASSIGN : s_6_8 110 # ASSIGN : s_7_0 1111 # ASSIGN : s_7_1 822 # ASSIGN : s_7_2 0 # ASSIGN : s_7_3 1112 # ASSIGN : s_7_4 159 # ASSIGN : s_7_5 1113 # ASSIGN : s_7_6 1114 # ASSIGN : s_7_7 823 # ASSIGN : s_7_8 846 # ASSIGN : s_8_0 1109 # ASSIGN : s_8_1 0 # ASSIGN : s_8_2 965 # ASSIGN : s_8_3 674 # ASSIGN : s_8_4 1 # ASSIGN : s_8_5 20 # ASSIGN : s_8_6 48 # ASSIGN : s_8_7 1111 # ASSIGN : s_8_8 1110 SHOW_RESULT 1115 END : 1115 (1 seconds) [Sun Jun 18 17:37:40 2006] SHOW_RESULT 1115 CPU : 1.55 = 1.53 + 0.02 + 0 + 0 # BOUND : makespan 1112 1115 MODIFY_CNF 1113 BEGIN : [Sun Jun 18 17:37:41 2006] MODIFY_CNF 1113 END : 146022722 bytes (0 seconds) [Sun Jun 18 17:37:41 2006] MODIFY_CNF 1113 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1113 BEGIN : [Sun Jun 18 17:37:41 2006] CMD : minisat /tmp/csp2sat11196.cnf /tmp/csp2sat11196.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1926952 5426622 | 642317 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 7 (1 /sec) decisions : 34 (3 /sec) propagations : 347332 (30150 /sec) conflict literals : 16 (5.88 % deleted) Memory used : 238.89 MB CPU time : 11.52 s UNSATISFIABLE VERIFY_CNF 1113 END : (12 seconds) [Sun Jun 18 17:37:53 2006] VERIFY_CNF 1113 CPU : 12.23 = 0 + 0 + 11.52 + 0.71 # RESULT : makespan 1113 UNSATISFIABLE # BOUND : makespan 1114 1115 MODIFY_CNF 1114 BEGIN : [Sun Jun 18 17:37:53 2006] MODIFY_CNF 1114 END : 146022722 bytes (0 seconds) [Sun Jun 18 17:37:53 2006] MODIFY_CNF 1114 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1114 BEGIN : [Sun Jun 18 17:37:53 2006] CMD : minisat /tmp/csp2sat11196.cnf /tmp/csp2sat11196.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1928248 5430510 | 642749 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 10 (1 /sec) decisions : 37 (3 /sec) propagations : 392044 (33855 /sec) conflict literals : 31 (8.82 % deleted) Memory used : 238.90 MB CPU time : 11.58 s UNSATISFIABLE VERIFY_CNF 1114 END : (12 seconds) [Sun Jun 18 17:38:05 2006] VERIFY_CNF 1114 CPU : 12.35 = 0.00999999999999091 + 0 + 11.58 + 0.76 # RESULT : makespan 1114 UNSATISFIABLE # BOUND : makespan 1115 1115 MAIN END : (396 seconds) [Sun Jun 18 17:38:05 2006] MAIN CPU : 395.07 = 246.87 + 1.45 + 137.39 + 9.36