# TIMEOUT 18000 MAIN BEGIN : [Sun Jun 18 16:13:01 2006] READ BEGIN : csp/gp05-08.csp [Sun Jun 18 16:13:01 2006] READ END : csp/gp05-08.csp (0 seconds) [Sun Jun 18 16:13:01 2006] READ CPU : 0.24 = 0.24 + 0 + 0 + 0 # BOUND : makespan 1000 2162 GENERATE_CNF 2162 BEGIN : [Sun Jun 18 16:13:01 2006] GENERATE_CNF 2162 END : 55489 variables 477290 clauses 9901763 bytes (20 seconds) [Sun Jun 18 16:13:21 2006] GENERATE_CNF 2162 CPU : 19.98 = 19.89 + 0.09 + 0 + 0 MODIFY_CNF 1581 BEGIN : [Sun Jun 18 16:13:21 2006] MODIFY_CNF 1581 END : 9901769 bytes (0 seconds) [Sun Jun 18 16:13:21 2006] MODIFY_CNF 1581 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1581 BEGIN : [Sun Jun 18 16:13:21 2006] CMD : minisat /tmp/csp2sat9233.cnf /tmp/csp2sat9233.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 360710 1027224 | 120236 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 75 (123 /sec) propagations : 55489 (90966 /sec) conflict literals : 0 ( nan % deleted) Memory used : 22.84 MB CPU time : 0.61 s SATISFIABLE VERIFY_CNF 1581 END : (1 seconds) [Sun Jun 18 16:13:22 2006] VERIFY_CNF 1581 CPU : 0.71 = 0 + 0 + 0.64 + 0.07 # RESULT : makespan 1581 SATISFIABLE SHOW_RESULT 1581 BEGIN : [Sun Jun 18 16:13:22 2006] # ASSIGN : makespan 1581 # ASSIGN : s_0_0 12 # ASSIGN : s_0_1 578 # ASSIGN : s_0_2 568 # ASSIGN : s_0_3 2 # ASSIGN : s_0_4 3 # ASSIGN : s_1_0 335 # ASSIGN : s_1_1 1235 # ASSIGN : s_1_2 579 # ASSIGN : s_1_3 25 # ASSIGN : s_1_4 26 # ASSIGN : s_2_0 341 # ASSIGN : s_2_1 1557 # ASSIGN : s_2_2 941 # ASSIGN : s_2_3 210 # ASSIGN : s_2_4 877 # ASSIGN : s_3_0 579 # ASSIGN : s_3_1 1558 # ASSIGN : s_3_2 1568 # ASSIGN : s_3_3 580 # ASSIGN : s_3_4 891 # ASSIGN : s_4_0 581 # ASSIGN : s_4_1 1569 # ASSIGN : s_4_2 1579 # ASSIGN : s_4_3 1013 # ASSIGN : s_4_4 1580 SHOW_RESULT 1581 END : 1581 (0 seconds) [Sun Jun 18 16:13:22 2006] SHOW_RESULT 1581 CPU : 0.0900000000000018 = 0.0800000000000018 + 0.01 + 0 + 0 # BOUND : makespan 1000 1581 MODIFY_CNF 1290 BEGIN : [Sun Jun 18 16:13:22 2006] MODIFY_CNF 1290 END : 9901769 bytes (0 seconds) [Sun Jun 18 16:13:22 2006] MODIFY_CNF 1290 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1290 BEGIN : [Sun Jun 18 16:13:22 2006] CMD : minisat /tmp/csp2sat9233.cnf /tmp/csp2sat9233.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 302510 852624 | 100836 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 41 (65 /sec) propagations : 55489 (88078 /sec) conflict literals : 0 ( nan % deleted) Memory used : 22.93 MB CPU time : 0.63 s SATISFIABLE VERIFY_CNF 1290 END : (1 seconds) [Sun Jun 18 16:13:23 2006] VERIFY_CNF 1290 CPU : 0.73 = 0 + 0 + 0.65 + 0.08 # RESULT : makespan 1290 SATISFIABLE SHOW_RESULT 1290 BEGIN : [Sun Jun 18 16:13:23 2006] # ASSIGN : makespan 1290 # ASSIGN : s_0_0 956 # ASSIGN : s_0_1 15 # ASSIGN : s_0_2 5 # ASSIGN : s_0_3 0 # ASSIGN : s_0_4 1279 # ASSIGN : s_1_0 1284 # ASSIGN : s_1_1 946 # ASSIGN : s_1_2 311 # ASSIGN : s_1_3 1 # ASSIGN : s_1_4 2 # ASSIGN : s_2_0 434 # ASSIGN : s_2_1 672 # ASSIGN : s_2_2 673 # ASSIGN : s_2_3 159 # ASSIGN : s_2_4 420 # ASSIGN : s_3_0 1 # ASSIGN : s_3_1 1268 # ASSIGN : s_3_2 279 # ASSIGN : s_3_3 290 # ASSIGN : s_3_4 601 # ASSIGN : s_4_0 2 # ASSIGN : s_4_1 1278 # ASSIGN : s_4_2 1289 # ASSIGN : s_4_3 722 # ASSIGN : s_4_4 1288 SHOW_RESULT 1290 END : 1290 (0 seconds) [Sun Jun 18 16:13:23 2006] SHOW_RESULT 1290 CPU : 0.0899999999999999 = 0.0899999999999999 + 0 + 0 + 0 # BOUND : makespan 1000 1290 MODIFY_CNF 1145 BEGIN : [Sun Jun 18 16:13:23 2006] MODIFY_CNF 1145 END : 9901769 bytes (0 seconds) [Sun Jun 18 16:13:23 2006] MODIFY_CNF 1145 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1145 BEGIN : [Sun Jun 18 16:13:23 2006] CMD : minisat /tmp/csp2sat9233.cnf /tmp/csp2sat9233.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 273510 765624 | 91170 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (3 /sec) decisions : 5 (8 /sec) propagations : 36933 (61555 /sec) conflict literals : 1 (0.00 % deleted) Memory used : 22.63 MB CPU time : 0.6 s UNSATISFIABLE VERIFY_CNF 1145 END : (0 seconds) [Sun Jun 18 16:13:23 2006] VERIFY_CNF 1145 CPU : 0.69 = 0 + 0 + 0.6 + 0.09 # RESULT : makespan 1145 UNSATISFIABLE # BOUND : makespan 1146 1290 MODIFY_CNF 1218 BEGIN : [Sun Jun 18 16:13:23 2006] MODIFY_CNF 1218 END : 9901769 bytes (0 seconds) [Sun Jun 18 16:13:23 2006] MODIFY_CNF 1218 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1218 BEGIN : [Sun Jun 18 16:13:23 2006] CMD : minisat /tmp/csp2sat9233.cnf /tmp/csp2sat9233.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 288110 809424 | 96036 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (3 /sec) decisions : 5 (8 /sec) propagations : 35035 (54742 /sec) conflict literals : 1 (0.00 % deleted) Memory used : 22.62 MB CPU time : 0.64 s UNSATISFIABLE VERIFY_CNF 1218 END : (1 seconds) [Sun Jun 18 16:13:24 2006] VERIFY_CNF 1218 CPU : 0.68 = 0 + 0 + 0.64 + 0.04 # RESULT : makespan 1218 UNSATISFIABLE # BOUND : makespan 1219 1290 MODIFY_CNF 1254 BEGIN : [Sun Jun 18 16:13:24 2006] MODIFY_CNF 1254 END : 9901769 bytes (0 seconds) [Sun Jun 18 16:13:24 2006] MODIFY_CNF 1254 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1254 BEGIN : [Sun Jun 18 16:13:24 2006] CMD : minisat /tmp/csp2sat9233.cnf /tmp/csp2sat9233.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 295310 831024 | 98436 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (3 /sec) decisions : 5 (8 /sec) propagations : 34099 (54125 /sec) conflict literals : 1 (0.00 % deleted) Memory used : 22.62 MB CPU time : 0.63 s UNSATISFIABLE VERIFY_CNF 1254 END : (1 seconds) [Sun Jun 18 16:13:25 2006] VERIFY_CNF 1254 CPU : 0.68 = 0 + 0 + 0.63 + 0.05 # RESULT : makespan 1254 UNSATISFIABLE # BOUND : makespan 1255 1290 MODIFY_CNF 1272 BEGIN : [Sun Jun 18 16:13:25 2006] MODIFY_CNF 1272 END : 9901769 bytes (0 seconds) [Sun Jun 18 16:13:25 2006] MODIFY_CNF 1272 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1272 BEGIN : [Sun Jun 18 16:13:25 2006] CMD : minisat /tmp/csp2sat9233.cnf /tmp/csp2sat9233.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 298910 841824 | 99636 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (3 /sec) decisions : 5 (8 /sec) propagations : 33631 (53383 /sec) conflict literals : 1 (0.00 % deleted) Memory used : 22.62 MB CPU time : 0.63 s UNSATISFIABLE VERIFY_CNF 1272 END : (0 seconds) [Sun Jun 18 16:13:25 2006] VERIFY_CNF 1272 CPU : 0.67 = 0 + 0 + 0.63 + 0.04 # RESULT : makespan 1272 UNSATISFIABLE # BOUND : makespan 1273 1290 MODIFY_CNF 1281 BEGIN : [Sun Jun 18 16:13:25 2006] MODIFY_CNF 1281 END : 9901769 bytes (0 seconds) [Sun Jun 18 16:13:25 2006] MODIFY_CNF 1281 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1281 BEGIN : [Sun Jun 18 16:13:25 2006] CMD : minisat /tmp/csp2sat9233.cnf /tmp/csp2sat9233.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 300710 847224 | 100236 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (3 /sec) decisions : 5 (9 /sec) propagations : 33397 (57581 /sec) conflict literals : 1 (0.00 % deleted) Memory used : 22.62 MB CPU time : 0.58 s UNSATISFIABLE VERIFY_CNF 1281 END : (1 seconds) [Sun Jun 18 16:13:26 2006] VERIFY_CNF 1281 CPU : 0.67 = 0 + 0 + 0.58 + 0.09 # RESULT : makespan 1281 UNSATISFIABLE # BOUND : makespan 1282 1290 MODIFY_CNF 1286 BEGIN : [Sun Jun 18 16:13:26 2006] MODIFY_CNF 1286 END : 9901769 bytes (0 seconds) [Sun Jun 18 16:13:26 2006] MODIFY_CNF 1286 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1286 BEGIN : [Sun Jun 18 16:13:26 2006] CMD : minisat /tmp/csp2sat9233.cnf /tmp/csp2sat9233.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 301710 850224 | 100570 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (3 /sec) decisions : 5 (8 /sec) propagations : 33267 (53656 /sec) conflict literals : 1 (0.00 % deleted) Memory used : 22.62 MB CPU time : 0.62 s UNSATISFIABLE VERIFY_CNF 1286 END : (1 seconds) [Sun Jun 18 16:13:27 2006] VERIFY_CNF 1286 CPU : 0.67 = 0 + 0 + 0.62 + 0.05 # RESULT : makespan 1286 UNSATISFIABLE # BOUND : makespan 1287 1290 MODIFY_CNF 1288 BEGIN : [Sun Jun 18 16:13:27 2006] MODIFY_CNF 1288 END : 9901769 bytes (0 seconds) [Sun Jun 18 16:13:27 2006] MODIFY_CNF 1288 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1288 BEGIN : [Sun Jun 18 16:13:27 2006] CMD : minisat /tmp/csp2sat9233.cnf /tmp/csp2sat9233.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 302110 851424 | 100703 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 37 (62 /sec) propagations : 55489 (92482 /sec) conflict literals : 0 ( nan % deleted) Memory used : 22.93 MB CPU time : 0.6 s SATISFIABLE VERIFY_CNF 1288 END : (1 seconds) [Sun Jun 18 16:13:28 2006] VERIFY_CNF 1288 CPU : 0.74 = 0 + 0 + 0.62 + 0.12 # RESULT : makespan 1288 SATISFIABLE SHOW_RESULT 1288 BEGIN : [Sun Jun 18 16:13:28 2006] # ASSIGN : makespan 1288 # ASSIGN : s_0_0 955 # ASSIGN : s_0_1 14 # ASSIGN : s_0_2 3 # ASSIGN : s_0_3 13 # ASSIGN : s_0_4 1278 # ASSIGN : s_1_0 1282 # ASSIGN : s_1_1 945 # ASSIGN : s_1_2 310 # ASSIGN : s_1_3 0 # ASSIGN : s_1_4 1 # ASSIGN : s_2_0 433 # ASSIGN : s_2_1 671 # ASSIGN : s_2_2 672 # ASSIGN : s_2_3 158 # ASSIGN : s_2_4 419 # ASSIGN : s_3_0 0 # ASSIGN : s_3_1 1267 # ASSIGN : s_3_2 278 # ASSIGN : s_3_3 289 # ASSIGN : s_3_4 600 # ASSIGN : s_4_0 1 # ASSIGN : s_4_1 1277 # ASSIGN : s_4_2 0 # ASSIGN : s_4_3 721 # ASSIGN : s_4_4 1287 SHOW_RESULT 1288 END : 1288 (0 seconds) [Sun Jun 18 16:13:28 2006] SHOW_RESULT 1288 CPU : 0.110000000000001 = 0.100000000000001 + 0.01 + 0 + 0 # BOUND : makespan 1287 1288 MODIFY_CNF 1287 BEGIN : [Sun Jun 18 16:13:28 2006] MODIFY_CNF 1287 END : 9901769 bytes (0 seconds) [Sun Jun 18 16:13:28 2006] MODIFY_CNF 1287 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1287 BEGIN : [Sun Jun 18 16:13:28 2006] CMD : minisat /tmp/csp2sat9233.cnf /tmp/csp2sat9233.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 301910 850824 | 100636 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 38 (58 /sec) propagations : 55489 (84074 /sec) conflict literals : 0 ( nan % deleted) Memory used : 22.93 MB CPU time : 0.66 s SATISFIABLE VERIFY_CNF 1287 END : (0 seconds) [Sun Jun 18 16:13:28 2006] VERIFY_CNF 1287 CPU : 0.73 = 0 + 0 + 0.69 + 0.04 # RESULT : makespan 1287 SATISFIABLE SHOW_RESULT 1287 BEGIN : [Sun Jun 18 16:13:28 2006] # ASSIGN : makespan 1287 # ASSIGN : s_0_0 954 # ASSIGN : s_0_1 287 # ASSIGN : s_0_2 146 # ASSIGN : s_0_3 156 # ASSIGN : s_0_4 1277 # ASSIGN : s_1_0 1281 # ASSIGN : s_1_1 944 # ASSIGN : s_1_2 309 # ASSIGN : s_1_3 719 # ASSIGN : s_1_4 0 # ASSIGN : s_2_0 433 # ASSIGN : s_2_1 156 # ASSIGN : s_2_2 671 # ASSIGN : s_2_3 157 # ASSIGN : s_2_4 419 # ASSIGN : s_3_0 0 # ASSIGN : s_3_1 1266 # ASSIGN : s_3_2 277 # ASSIGN : s_3_3 288 # ASSIGN : s_3_4 599 # ASSIGN : s_4_0 1 # ASSIGN : s_4_1 1276 # ASSIGN : s_4_2 0 # ASSIGN : s_4_3 720 # ASSIGN : s_4_4 1286 SHOW_RESULT 1287 END : 1287 (0 seconds) [Sun Jun 18 16:13:28 2006] SHOW_RESULT 1287 CPU : 0.0800000000000018 = 0.0800000000000018 + 0 + 0 + 0 # BOUND : makespan 1287 1287 MAIN END : (27 seconds) [Sun Jun 18 16:13:28 2006] MAIN CPU : 27.58 = 20.49 + 0.12 + 6.3 + 0.67