# TIMEOUT 18000 MAIN BEGIN : [Sun Jun 18 16:18:57 2006] READ BEGIN : csp/gp06-05.csp [Sun Jun 18 16:18:57 2006] READ END : csp/gp06-05.csp (1 seconds) [Sun Jun 18 16:18:58 2006] READ CPU : 0.4 = 0.4 + 0 + 0 + 0 # BOUND : makespan 1000 2928 GENERATE_CNF 2928 BEGIN : [Sun Jun 18 16:18:58 2006] GENERATE_CNF 2928 END : 107806 variables 1171907 clauses 25963496 bytes (44 seconds) [Sun Jun 18 16:19:42 2006] GENERATE_CNF 2928 CPU : 43.63 = 43.47 + 0.16 + 0 + 0 MODIFY_CNF 1964 BEGIN : [Sun Jun 18 16:19:42 2006] MODIFY_CNF 1964 END : 25963502 bytes (0 seconds) [Sun Jun 18 16:19:42 2006] MODIFY_CNF 1964 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1964 BEGIN : [Sun Jun 18 16:19:42 2006] CMD : minisat /tmp/csp2sat9729.cnf /tmp/csp2sat9729.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 824250 2365888 | 274750 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 4 (3 /sec) decisions : 147 (93 /sec) propagations : 127091 (80437 /sec) conflict literals : 22 (15.38 % deleted) Memory used : 50.08 MB CPU time : 1.58 s SATISFIABLE VERIFY_CNF 1964 END : (2 seconds) [Sun Jun 18 16:19:44 2006] VERIFY_CNF 1964 CPU : 1.78 = 0 + 0 + 1.65 + 0.13 # RESULT : makespan 1964 SATISFIABLE SHOW_RESULT 1964 BEGIN : [Sun Jun 18 16:19:44 2006] # ASSIGN : makespan 1964 # ASSIGN : s_0_0 5 # ASSIGN : s_0_1 466 # ASSIGN : s_0_2 113 # ASSIGN : s_0_3 6 # ASSIGN : s_0_4 9 # ASSIGN : s_0_5 114 # ASSIGN : s_1_0 18 # ASSIGN : s_1_1 1110 # ASSIGN : s_1_2 937 # ASSIGN : s_1_3 7 # ASSIGN : s_1_4 10 # ASSIGN : s_1_5 822 # ASSIGN : s_2_0 965 # ASSIGN : s_2_1 1121 # ASSIGN : s_2_2 1136 # ASSIGN : s_2_3 171 # ASSIGN : s_2_4 170 # ASSIGN : s_2_5 823 # ASSIGN : s_3_0 1275 # ASSIGN : s_3_1 1312 # ASSIGN : s_3_2 1320 # ASSIGN : s_3_3 814 # ASSIGN : s_3_4 312 # ASSIGN : s_3_5 824 # ASSIGN : s_4_0 1612 # ASSIGN : s_4_1 1613 # ASSIGN : s_4_2 1813 # ASSIGN : s_4_3 963 # ASSIGN : s_4_4 313 # ASSIGN : s_4_5 1619 # ASSIGN : s_5_0 1962 # ASSIGN : s_5_1 1645 # ASSIGN : s_5_2 1961 # ASSIGN : s_5_3 964 # ASSIGN : s_5_4 1306 # ASSIGN : s_5_5 1963 SHOW_RESULT 1964 END : 1964 (0 seconds) [Sun Jun 18 16:19:44 2006] SHOW_RESULT 1964 CPU : 0.190000000000004 = 0.160000000000004 + 0.03 + 0 + 0 # BOUND : makespan 1000 1964 MODIFY_CNF 1482 BEGIN : [Sun Jun 18 16:19:44 2006] MODIFY_CNF 1482 END : 25963502 bytes (0 seconds) [Sun Jun 18 16:19:44 2006] MODIFY_CNF 1482 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1482 BEGIN : [Sun Jun 18 16:19:44 2006] CMD : minisat /tmp/csp2sat9729.cnf /tmp/csp2sat9729.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 650730 1845328 | 216910 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 1 (1 /sec) decisions : 120 (75 /sec) propagations : 117511 (73444 /sec) conflict literals : 6 (0.00 % deleted) Memory used : 50.08 MB CPU time : 1.6 s SATISFIABLE VERIFY_CNF 1482 END : (2 seconds) [Sun Jun 18 16:19:46 2006] VERIFY_CNF 1482 CPU : 1.79 = 0 + 0 + 1.65 + 0.14 # RESULT : makespan 1482 SATISFIABLE SHOW_RESULT 1482 BEGIN : [Sun Jun 18 16:19:46 2006] # ASSIGN : makespan 1482 # ASSIGN : s_0_0 7 # ASSIGN : s_0_1 838 # ASSIGN : s_0_2 8 # ASSIGN : s_0_3 104 # ASSIGN : s_0_4 0 # ASSIGN : s_0_5 105 # ASSIGN : s_1_0 482 # ASSIGN : s_1_1 443 # ASSIGN : s_1_2 9 # ASSIGN : s_1_3 454 # ASSIGN : s_1_4 1 # ASSIGN : s_1_5 457 # ASSIGN : s_2_0 1286 # ASSIGN : s_2_1 119 # ASSIGN : s_2_2 1102 # ASSIGN : s_2_3 459 # ASSIGN : s_2_4 146 # ASSIGN : s_2_5 458 # ASSIGN : s_3_0 1442 # ASSIGN : s_3_1 134 # ASSIGN : s_3_2 182 # ASSIGN : s_3_3 1126 # ASSIGN : s_3_4 147 # ASSIGN : s_3_5 675 # ASSIGN : s_4_0 1479 # ASSIGN : s_4_1 142 # ASSIGN : s_4_2 1331 # ASSIGN : s_4_3 1136 # ASSIGN : s_4_4 148 # ASSIGN : s_4_5 1137 # ASSIGN : s_5_0 1480 # ASSIGN : s_5_1 482 # ASSIGN : s_5_2 1479 # ASSIGN : s_5_3 1137 # ASSIGN : s_5_4 798 # ASSIGN : s_5_5 1481 SHOW_RESULT 1482 END : 1482 (0 seconds) [Sun Jun 18 16:19:46 2006] SHOW_RESULT 1482 CPU : 0.199999999999996 = 0.199999999999996 + 0 + 0 + 0 # BOUND : makespan 1000 1482 MODIFY_CNF 1241 BEGIN : [Sun Jun 18 16:19:46 2006] MODIFY_CNF 1241 END : 25963502 bytes (0 seconds) [Sun Jun 18 16:19:46 2006] MODIFY_CNF 1241 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1241 BEGIN : [Sun Jun 18 16:19:46 2006] CMD : minisat /tmp/csp2sat9729.cnf /tmp/csp2sat9729.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 563970 1585048 | 187990 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 3 (2 /sec) decisions : 13 (8 /sec) propagations : 79494 (50313 /sec) conflict literals : 3 (25.00 % deleted) Memory used : 49.54 MB CPU time : 1.58 s UNSATISFIABLE VERIFY_CNF 1241 END : (2 seconds) [Sun Jun 18 16:19:48 2006] VERIFY_CNF 1241 CPU : 1.73 = 0 + 0 + 1.58 + 0.15 # RESULT : makespan 1241 UNSATISFIABLE # BOUND : makespan 1242 1482 MODIFY_CNF 1362 BEGIN : [Sun Jun 18 16:19:48 2006] MODIFY_CNF 1362 END : 25963502 bytes (0 seconds) [Sun Jun 18 16:19:48 2006] MODIFY_CNF 1362 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1362 BEGIN : [Sun Jun 18 16:19:48 2006] CMD : minisat /tmp/csp2sat9729.cnf /tmp/csp2sat9729.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 607530 1715728 | 202510 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 3 (2 /sec) decisions : 109 (70 /sec) propagations : 115987 (74351 /sec) conflict literals : 12 (0.00 % deleted) Memory used : 50.08 MB CPU time : 1.56 s SATISFIABLE VERIFY_CNF 1362 END : (2 seconds) [Sun Jun 18 16:19:50 2006] VERIFY_CNF 1362 CPU : 1.76 = 0 + 0 + 1.62 + 0.14 # RESULT : makespan 1362 SATISFIABLE SHOW_RESULT 1362 BEGIN : [Sun Jun 18 16:19:50 2006] # ASSIGN : makespan 1362 # ASSIGN : s_0_0 3 # ASSIGN : s_0_1 718 # ASSIGN : s_0_2 4 # ASSIGN : s_0_3 5 # ASSIGN : s_0_4 6 # ASSIGN : s_0_5 7 # ASSIGN : s_1_0 384 # ASSIGN : s_1_1 348 # ASSIGN : s_1_2 1188 # ASSIGN : s_1_3 16 # ASSIGN : s_1_4 19 # ASSIGN : s_1_5 359 # ASSIGN : s_2_0 204 # ASSIGN : s_2_1 0 # ASSIGN : s_2_2 1004 # ASSIGN : s_2_3 361 # ASSIGN : s_2_4 27 # ASSIGN : s_2_5 360 # ASSIGN : s_3_0 1325 # ASSIGN : s_3_1 15 # ASSIGN : s_3_2 63 # ASSIGN : s_3_3 1007 # ASSIGN : s_3_4 28 # ASSIGN : s_3_5 556 # ASSIGN : s_4_0 22 # ASSIGN : s_4_1 23 # ASSIGN : s_4_2 856 # ASSIGN : s_4_3 1017 # ASSIGN : s_4_4 29 # ASSIGN : s_4_5 1166 # ASSIGN : s_5_0 362 # ASSIGN : s_5_1 363 # ASSIGN : s_5_2 1361 # ASSIGN : s_5_3 1018 # ASSIGN : s_5_4 679 # ASSIGN : s_5_5 1360 SHOW_RESULT 1362 END : 1362 (0 seconds) [Sun Jun 18 16:19:50 2006] SHOW_RESULT 1362 CPU : 0.200000000000005 = 0.190000000000005 + 0.00999999999999998 + 0 + 0 # BOUND : makespan 1242 1362 MODIFY_CNF 1302 BEGIN : [Sun Jun 18 16:19:50 2006] MODIFY_CNF 1302 END : 25963502 bytes (0 seconds) [Sun Jun 18 16:19:50 2006] MODIFY_CNF 1302 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1302 BEGIN : [Sun Jun 18 16:19:50 2006] CMD : minisat /tmp/csp2sat9729.cnf /tmp/csp2sat9729.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 585930 1650928 | 195310 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 4 (3 /sec) decisions : 87 (56 /sec) propagations : 111969 (72707 /sec) conflict literals : 22 (0.00 % deleted) Memory used : 50.08 MB CPU time : 1.54 s SATISFIABLE VERIFY_CNF 1302 END : (2 seconds) [Sun Jun 18 16:19:52 2006] VERIFY_CNF 1302 CPU : 1.79 = 0 + 0 + 1.58 + 0.21 # RESULT : makespan 1302 SATISFIABLE SHOW_RESULT 1302 BEGIN : [Sun Jun 18 16:19:52 2006] # ASSIGN : makespan 1302 # ASSIGN : s_0_0 454 # ASSIGN : s_0_1 455 # ASSIGN : s_0_2 1 # ASSIGN : s_0_3 0 # ASSIGN : s_0_4 2 # ASSIGN : s_0_5 3 # ASSIGN : s_1_0 496 # ASSIGN : s_1_1 323 # ASSIGN : s_1_2 150 # ASSIGN : s_1_3 139 # ASSIGN : s_1_4 142 # ASSIGN : s_1_5 355 # ASSIGN : s_2_0 106 # ASSIGN : s_2_1 334 # ASSIGN : s_2_2 475 # ASSIGN : s_2_3 659 # ASSIGN : s_2_4 308 # ASSIGN : s_2_5 356 # ASSIGN : s_3_0 262 # ASSIGN : s_3_1 349 # ASSIGN : s_3_2 808 # ASSIGN : s_3_3 299 # ASSIGN : s_3_4 309 # ASSIGN : s_3_5 357 # ASSIGN : s_4_0 1 # ASSIGN : s_4_1 1099 # ASSIGN : s_4_2 2 # ASSIGN : s_4_3 309 # ASSIGN : s_4_4 310 # ASSIGN : s_4_5 1105 # ASSIGN : s_5_0 1300 # ASSIGN : s_5_1 1 # ASSIGN : s_5_2 1301 # ASSIGN : s_5_3 317 # ASSIGN : s_5_4 960 # ASSIGN : s_5_5 1299 SHOW_RESULT 1302 END : 1302 (0 seconds) [Sun Jun 18 16:19:52 2006] SHOW_RESULT 1302 CPU : 0.189999999999998 = 0.189999999999998 + 0 + 0 + 0 # BOUND : makespan 1242 1302 MODIFY_CNF 1272 BEGIN : [Sun Jun 18 16:19:52 2006] MODIFY_CNF 1272 END : 25963502 bytes (0 seconds) [Sun Jun 18 16:19:52 2006] MODIFY_CNF 1272 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1272 BEGIN : [Sun Jun 18 16:19:52 2006] CMD : minisat /tmp/csp2sat9729.cnf /tmp/csp2sat9729.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 575130 1618528 | 191710 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 3 (2 /sec) decisions : 13 (8 /sec) propagations : 78347 (50875 /sec) conflict literals : 3 (25.00 % deleted) Memory used : 49.54 MB CPU time : 1.54 s UNSATISFIABLE VERIFY_CNF 1272 END : (1 seconds) [Sun Jun 18 16:19:53 2006] VERIFY_CNF 1272 CPU : 1.7 = 0 + 0 + 1.54 + 0.16 # RESULT : makespan 1272 UNSATISFIABLE # BOUND : makespan 1273 1302 MODIFY_CNF 1287 BEGIN : [Sun Jun 18 16:19:53 2006] MODIFY_CNF 1287 END : 25963502 bytes (0 seconds) [Sun Jun 18 16:19:53 2006] MODIFY_CNF 1287 CPU : 0.00999999999999801 = 0.00999999999999801 + 0 + 0 + 0 VERIFY_CNF 1287 BEGIN : [Sun Jun 18 16:19:53 2006] CMD : minisat /tmp/csp2sat9729.cnf /tmp/csp2sat9729.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 580530 1634728 | 193510 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (1 /sec) decisions : 13 (8 /sec) propagations : 75399 (48333 /sec) conflict literals : 1 (0.00 % deleted) Memory used : 49.54 MB CPU time : 1.56 s UNSATISFIABLE VERIFY_CNF 1287 END : (2 seconds) [Sun Jun 18 16:19:55 2006] VERIFY_CNF 1287 CPU : 1.69 = 0 + 0 + 1.56 + 0.13 # RESULT : makespan 1287 UNSATISFIABLE # BOUND : makespan 1288 1302 MODIFY_CNF 1295 BEGIN : [Sun Jun 18 16:19:55 2006] MODIFY_CNF 1295 END : 25963502 bytes (0 seconds) [Sun Jun 18 16:19:55 2006] MODIFY_CNF 1295 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1295 BEGIN : [Sun Jun 18 16:19:55 2006] CMD : minisat /tmp/csp2sat9729.cnf /tmp/csp2sat9729.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 583410 1643368 | 194470 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (1 /sec) decisions : 13 (8 /sec) propagations : 74914 (47716 /sec) conflict literals : 1 (0.00 % deleted) Memory used : 49.54 MB CPU time : 1.57 s UNSATISFIABLE VERIFY_CNF 1295 END : (2 seconds) [Sun Jun 18 16:19:57 2006] VERIFY_CNF 1295 CPU : 1.71 = 0 + 0.01 + 1.57 + 0.13 # RESULT : makespan 1295 UNSATISFIABLE # BOUND : makespan 1296 1302 MODIFY_CNF 1299 BEGIN : [Sun Jun 18 16:19:57 2006] MODIFY_CNF 1299 END : 25963502 bytes (0 seconds) [Sun Jun 18 16:19:57 2006] MODIFY_CNF 1299 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1299 BEGIN : [Sun Jun 18 16:19:57 2006] CMD : minisat /tmp/csp2sat9729.cnf /tmp/csp2sat9729.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 584850 1647688 | 194950 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 1 (1 /sec) decisions : 76 (47 /sec) propagations : 114031 (69958 /sec) conflict literals : 4 (0.00 % deleted) Memory used : 50.09 MB CPU time : 1.63 s SATISFIABLE VERIFY_CNF 1299 END : (2 seconds) [Sun Jun 18 16:19:59 2006] VERIFY_CNF 1299 CPU : 1.82 = 0 + 0 + 1.69 + 0.13 # RESULT : makespan 1299 SATISFIABLE SHOW_RESULT 1299 BEGIN : [Sun Jun 18 16:19:59 2006] # ASSIGN : makespan 1299 # ASSIGN : s_0_0 7 # ASSIGN : s_0_1 655 # ASSIGN : s_0_2 8 # ASSIGN : s_0_3 92 # ASSIGN : s_0_4 450 # ASSIGN : s_0_5 98 # ASSIGN : s_1_0 136 # ASSIGN : s_1_1 71 # ASSIGN : s_1_2 940 # ASSIGN : s_1_3 93 # ASSIGN : s_1_4 1289 # ASSIGN : s_1_5 96 # ASSIGN : s_2_0 957 # ASSIGN : s_2_1 82 # ASSIGN : s_2_2 1113 # ASSIGN : s_2_3 311 # ASSIGN : s_2_4 1297 # ASSIGN : s_2_5 97 # ASSIGN : s_3_0 1258 # ASSIGN : s_3_1 139 # ASSIGN : s_3_2 157 # ASSIGN : s_3_3 147 # ASSIGN : s_3_4 1298 # ASSIGN : s_3_5 650 # ASSIGN : s_4_0 1295 # ASSIGN : s_4_1 304 # ASSIGN : s_4_2 9 # ASSIGN : s_4_3 310 # ASSIGN : s_4_4 451 # ASSIGN : s_4_5 1101 # ASSIGN : s_5_0 1296 # ASSIGN : s_5_1 339 # ASSIGN : s_5_2 1297 # ASSIGN : s_5_3 954 # ASSIGN : s_5_4 0 # ASSIGN : s_5_5 1298 SHOW_RESULT 1299 END : 1299 (0 seconds) [Sun Jun 18 16:19:59 2006] SHOW_RESULT 1299 CPU : 0.190000000000005 = 0.190000000000005 + 0 + 0 + 0 # BOUND : makespan 1296 1299 MODIFY_CNF 1297 BEGIN : [Sun Jun 18 16:19:59 2006] MODIFY_CNF 1297 END : 25963502 bytes (0 seconds) [Sun Jun 18 16:19:59 2006] MODIFY_CNF 1297 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1297 BEGIN : [Sun Jun 18 16:19:59 2006] CMD : minisat /tmp/csp2sat9729.cnf /tmp/csp2sat9729.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 584130 1645528 | 194710 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (1 /sec) decisions : 13 (8 /sec) propagations : 73375 (44202 /sec) conflict literals : 1 (0.00 % deleted) Memory used : 49.53 MB CPU time : 1.66 s UNSATISFIABLE VERIFY_CNF 1297 END : (2 seconds) [Sun Jun 18 16:20:01 2006] VERIFY_CNF 1297 CPU : 1.78 = 0 + 0 + 1.66 + 0.12 # RESULT : makespan 1297 UNSATISFIABLE # BOUND : makespan 1298 1299 MODIFY_CNF 1298 BEGIN : [Sun Jun 18 16:20:01 2006] MODIFY_CNF 1298 END : 25963502 bytes (0 seconds) [Sun Jun 18 16:20:01 2006] MODIFY_CNF 1298 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1298 BEGIN : [Sun Jun 18 16:20:01 2006] CMD : minisat /tmp/csp2sat9729.cnf /tmp/csp2sat9729.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 584490 1646608 | 194830 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (1 /sec) decisions : 13 (6 /sec) propagations : 73338 (34923 /sec) conflict literals : 1 (0.00 % deleted) Memory used : 49.53 MB CPU time : 2.1 s UNSATISFIABLE VERIFY_CNF 1298 END : (2 seconds) [Sun Jun 18 16:20:03 2006] VERIFY_CNF 1298 CPU : 2.24 = 0 + 0 + 2.1 + 0.14 # RESULT : makespan 1298 UNSATISFIABLE # BOUND : makespan 1299 1299 MAIN END : (66 seconds) [Sun Jun 18 16:20:03 2006] MAIN CPU : 64.81 = 44.82 + 0.21 + 18.2 + 1.58