# TIMEOUT 18000 MAIN BEGIN : [Sun Jun 18 16:08:18 2006] READ BEGIN : csp/gp04-06.csp [Sun Jun 18 16:08:18 2006] READ END : csp/gp04-06.csp (0 seconds) [Sun Jun 18 16:08:18 2006] READ CPU : 0.12 = 0.12 + 0 + 0 + 0 # BOUND : makespan 1000 1661 GENERATE_CNF 1661 BEGIN : [Sun Jun 18 16:08:18 2006] GENERATE_CNF 1661 END : 27383 variables 173592 clauses 3479879 bytes (7 seconds) [Sun Jun 18 16:08:25 2006] GENERATE_CNF 1661 CPU : 6.32 = 6.3 + 0.02 + 0 + 0 MODIFY_CNF 1330 BEGIN : [Sun Jun 18 16:08:25 2006] MODIFY_CNF 1330 END : 3479885 bytes (0 seconds) [Sun Jun 18 16:08:25 2006] MODIFY_CNF 1330 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1330 BEGIN : [Sun Jun 18 16:08:25 2006] CMD : minisat /tmp/csp2sat9031.cnf /tmp/csp2sat9031.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 141603 397754 | 47201 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (10 /sec) decisions : 29 (138 /sec) propagations : 32726 (155838 /sec) conflict literals : 9 (0.00 % deleted) Memory used : 9.46 MB CPU time : 0.21 s SATISFIABLE VERIFY_CNF 1330 END : (0 seconds) [Sun Jun 18 16:08:25 2006] VERIFY_CNF 1330 CPU : 0.25 = 0 + 0 + 0.22 + 0.03 # RESULT : makespan 1330 SATISFIABLE SHOW_RESULT 1330 BEGIN : [Sun Jun 18 16:08:25 2006] # ASSIGN : makespan 1330 # ASSIGN : s_0_0 0 # ASSIGN : s_0_1 607 # ASSIGN : s_0_2 245 # ASSIGN : s_0_3 7 # ASSIGN : s_1_0 3 # ASSIGN : s_1_1 1240 # ASSIGN : s_1_2 600 # ASSIGN : s_1_3 16 # ASSIGN : s_2_0 8 # ASSIGN : s_2_1 335 # ASSIGN : s_2_2 921 # ASSIGN : s_2_3 923 # ASSIGN : s_3_0 335 # ASSIGN : s_3_1 330 # ASSIGN : s_3_2 1000 # ASSIGN : s_3_3 1322 SHOW_RESULT 1330 END : 1330 (0 seconds) [Sun Jun 18 16:08:25 2006] SHOW_RESULT 1330 CPU : 0.04 = 0.04 + 0 + 0 + 0 # BOUND : makespan 1000 1330 MODIFY_CNF 1165 BEGIN : [Sun Jun 18 16:08:25 2006] MODIFY_CNF 1165 END : 3479885 bytes (0 seconds) [Sun Jun 18 16:08:25 2006] MODIFY_CNF 1165 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1165 BEGIN : [Sun Jun 18 16:08:25 2006] CMD : minisat /tmp/csp2sat9031.cnf /tmp/csp2sat9031.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 125763 350234 | 41921 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (11 /sec) decisions : 3 (17 /sec) propagations : 17400 (96667 /sec) conflict literals : 1 (0.00 % deleted) Memory used : 9.32 MB CPU time : 0.18 s UNSATISFIABLE VERIFY_CNF 1165 END : (0 seconds) [Sun Jun 18 16:08:25 2006] VERIFY_CNF 1165 CPU : 0.23 = 0 + 0 + 0.18 + 0.05 # RESULT : makespan 1165 UNSATISFIABLE # BOUND : makespan 1166 1330 MODIFY_CNF 1248 BEGIN : [Sun Jun 18 16:08:25 2006] MODIFY_CNF 1248 END : 3479885 bytes (0 seconds) [Sun Jun 18 16:08:25 2006] MODIFY_CNF 1248 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1248 BEGIN : [Sun Jun 18 16:08:25 2006] CMD : minisat /tmp/csp2sat9031.cnf /tmp/csp2sat9031.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 133731 374138 | 44577 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (10 /sec) decisions : 3 (14 /sec) propagations : 17368 (82705 /sec) conflict literals : 1 (0.00 % deleted) Memory used : 9.34 MB CPU time : 0.21 s UNSATISFIABLE VERIFY_CNF 1248 END : (0 seconds) [Sun Jun 18 16:08:25 2006] VERIFY_CNF 1248 CPU : 0.23 = 0 + 0 + 0.21 + 0.02 # RESULT : makespan 1248 UNSATISFIABLE # BOUND : makespan 1249 1330 MODIFY_CNF 1289 BEGIN : [Sun Jun 18 16:08:25 2006] MODIFY_CNF 1289 END : 3479885 bytes (0 seconds) [Sun Jun 18 16:08:25 2006] MODIFY_CNF 1289 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1289 BEGIN : [Sun Jun 18 16:08:25 2006] CMD : minisat /tmp/csp2sat9031.cnf /tmp/csp2sat9031.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 137667 385946 | 45889 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 1 (5 /sec) decisions : 32 (168 /sec) propagations : 27784 (146232 /sec) conflict literals : 8 (0.00 % deleted) Memory used : 9.46 MB CPU time : 0.19 s SATISFIABLE VERIFY_CNF 1289 END : (1 seconds) [Sun Jun 18 16:08:26 2006] VERIFY_CNF 1289 CPU : 0.24 = 0 + 0 + 0.2 + 0.04 # RESULT : makespan 1289 SATISFIABLE SHOW_RESULT 1289 BEGIN : [Sun Jun 18 16:08:26 2006] # ASSIGN : makespan 1289 # ASSIGN : s_0_0 5 # ASSIGN : s_0_1 289 # ASSIGN : s_0_2 934 # ASSIGN : s_0_3 8 # ASSIGN : s_1_0 12 # ASSIGN : s_1_1 922 # ASSIGN : s_1_2 601 # ASSIGN : s_1_3 17 # ASSIGN : s_2_0 284 # ASSIGN : s_2_1 1012 # ASSIGN : s_2_2 277 # ASSIGN : s_2_3 613 # ASSIGN : s_3_0 611 # ASSIGN : s_3_1 1284 # ASSIGN : s_3_2 279 # ASSIGN : s_3_3 1276 SHOW_RESULT 1289 END : 1289 (0 seconds) [Sun Jun 18 16:08:26 2006] SHOW_RESULT 1289 CPU : 0.04 = 0.04 + 0 + 0 + 0 # BOUND : makespan 1249 1289 MODIFY_CNF 1269 BEGIN : [Sun Jun 18 16:08:26 2006] MODIFY_CNF 1269 END : 3479885 bytes (0 seconds) [Sun Jun 18 16:08:26 2006] MODIFY_CNF 1269 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1269 BEGIN : [Sun Jun 18 16:08:26 2006] CMD : minisat /tmp/csp2sat9031.cnf /tmp/csp2sat9031.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 135747 380186 | 45249 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 15 (83 /sec) propagations : 27383 (152128 /sec) conflict literals : 0 ( nan % deleted) Memory used : 9.46 MB CPU time : 0.18 s SATISFIABLE VERIFY_CNF 1269 END : (0 seconds) [Sun Jun 18 16:08:26 2006] VERIFY_CNF 1269 CPU : 0.24 = 0 + 0 + 0.19 + 0.05 # RESULT : makespan 1269 SATISFIABLE SHOW_RESULT 1269 BEGIN : [Sun Jun 18 16:08:26 2006] # ASSIGN : makespan 1269 # ASSIGN : s_0_0 257 # ASSIGN : s_0_1 272 # ASSIGN : s_0_2 905 # ASSIGN : s_0_3 1260 # ASSIGN : s_1_0 1264 # ASSIGN : s_1_1 907 # ASSIGN : s_1_2 584 # ASSIGN : s_1_3 0 # ASSIGN : s_2_0 260 # ASSIGN : s_2_1 997 # ASSIGN : s_2_2 258 # ASSIGN : s_2_3 598 # ASSIGN : s_3_0 587 # ASSIGN : s_3_1 257 # ASSIGN : s_3_2 262 # ASSIGN : s_3_3 1252 SHOW_RESULT 1269 END : 1269 (0 seconds) [Sun Jun 18 16:08:26 2006] SHOW_RESULT 1269 CPU : 0.04 = 0.04 + 0 + 0 + 0 # BOUND : makespan 1249 1269 MODIFY_CNF 1259 BEGIN : [Sun Jun 18 16:08:26 2006] MODIFY_CNF 1259 END : 3479885 bytes (0 seconds) [Sun Jun 18 16:08:26 2006] MODIFY_CNF 1259 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1259 BEGIN : [Sun Jun 18 16:08:26 2006] CMD : minisat /tmp/csp2sat9031.cnf /tmp/csp2sat9031.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 134787 377306 | 44929 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (9 /sec) decisions : 3 (14 /sec) propagations : 16196 (73618 /sec) conflict literals : 1 (0.00 % deleted) Memory used : 9.33 MB CPU time : 0.22 s UNSATISFIABLE VERIFY_CNF 1259 END : (0 seconds) [Sun Jun 18 16:08:26 2006] VERIFY_CNF 1259 CPU : 0.22 = 0 + 0 + 0.22 + 0 # RESULT : makespan 1259 UNSATISFIABLE # BOUND : makespan 1260 1269 MODIFY_CNF 1264 BEGIN : [Sun Jun 18 16:08:26 2006] MODIFY_CNF 1264 END : 3479885 bytes (0 seconds) [Sun Jun 18 16:08:26 2006] MODIFY_CNF 1264 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1264 BEGIN : [Sun Jun 18 16:08:26 2006] CMD : minisat /tmp/csp2sat9031.cnf /tmp/csp2sat9031.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 135267 378746 | 45089 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 6 (25 /sec) decisions : 6 (25 /sec) propagations : 40141 (167254 /sec) conflict literals : 7 (0.00 % deleted) Memory used : 9.34 MB CPU time : 0.24 s UNSATISFIABLE VERIFY_CNF 1264 END : (1 seconds) [Sun Jun 18 16:08:27 2006] VERIFY_CNF 1264 CPU : 0.24 = 0 + 0 + 0.24 + 0 # RESULT : makespan 1264 UNSATISFIABLE # BOUND : makespan 1265 1269 MODIFY_CNF 1267 BEGIN : [Sun Jun 18 16:08:27 2006] MODIFY_CNF 1267 END : 3479885 bytes (0 seconds) [Sun Jun 18 16:08:27 2006] MODIFY_CNF 1267 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1267 BEGIN : [Sun Jun 18 16:08:27 2006] CMD : minisat /tmp/csp2sat9031.cnf /tmp/csp2sat9031.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 135555 379610 | 45185 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 3 (14 /sec) decisions : 3 (14 /sec) propagations : 25488 (115855 /sec) conflict literals : 3 (0.00 % deleted) Memory used : 9.33 MB CPU time : 0.22 s UNSATISFIABLE VERIFY_CNF 1267 END : (0 seconds) [Sun Jun 18 16:08:27 2006] VERIFY_CNF 1267 CPU : 0.23 = 0 + 0 + 0.22 + 0.01 # RESULT : makespan 1267 UNSATISFIABLE # BOUND : makespan 1268 1269 MODIFY_CNF 1268 BEGIN : [Sun Jun 18 16:08:27 2006] MODIFY_CNF 1268 END : 3479885 bytes (0 seconds) [Sun Jun 18 16:08:27 2006] MODIFY_CNF 1268 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1268 BEGIN : [Sun Jun 18 16:08:27 2006] CMD : minisat /tmp/csp2sat9031.cnf /tmp/csp2sat9031.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 135651 379898 | 45217 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 3 (14 /sec) decisions : 3 (14 /sec) propagations : 23868 (113657 /sec) conflict literals : 3 (0.00 % deleted) Memory used : 9.32 MB CPU time : 0.21 s UNSATISFIABLE VERIFY_CNF 1268 END : (0 seconds) [Sun Jun 18 16:08:27 2006] VERIFY_CNF 1268 CPU : 0.23 = 0 + 0 + 0.21 + 0.02 # RESULT : makespan 1268 UNSATISFIABLE # BOUND : makespan 1269 1269 MAIN END : (9 seconds) [Sun Jun 18 16:08:27 2006] MAIN CPU : 8.67 = 6.54 + 0.02 + 1.89 + 0.22