# TIMEOUT 18000 MAIN BEGIN : [Mon Jun 19 23:13:44 2006] READ BEGIN : csp/tai_4x4_6.csp [Mon Jun 19 23:13:44 2006] READ END : csp/tai_4x4_6.csp (0 seconds) [Mon Jun 19 23:13:44 2006] READ CPU : 0.12 = 0.12 + 0 + 0 + 0 # BOUND : makespan 185 280 GENERATE_CNF 280 BEGIN : [Mon Jun 19 23:13:44 2006] GENERATE_CNF 280 END : 4721 variables 29194 clauses 511801 bytes (1 seconds) [Mon Jun 19 23:13:45 2006] GENERATE_CNF 280 CPU : 1.08 = 1.08 + 0 + 0 + 0 MODIFY_CNF 232 BEGIN : [Mon Jun 19 23:13:45 2006] MODIFY_CNF 232 END : 511806 bytes (0 seconds) [Mon Jun 19 23:13:45 2006] MODIFY_CNF 232 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 232 BEGIN : [Mon Jun 19 23:13:45 2006] CMD : minisat /tmp/csp2sat13816.cnf /tmp/csp2sat13816.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 24373 68726 | 8124 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 1 (33 /sec) decisions : 40 (1333 /sec) propagations : 6281 (209367 /sec) conflict literals : 5 (0.00 % deleted) Memory used : 2.52 MB CPU time : 0.03 s SATISFIABLE VERIFY_CNF 232 END : (1 seconds) [Mon Jun 19 23:13:46 2006] VERIFY_CNF 232 CPU : 0.05 = 0 + 0 + 0.04 + 0.01 # RESULT : makespan 232 SATISFIABLE SHOW_RESULT 232 BEGIN : [Mon Jun 19 23:13:46 2006] # ASSIGN : makespan 232 # ASSIGN : s_0_0 28 # ASSIGN : s_0_1 186 # ASSIGN : s_0_2 65 # ASSIGN : s_0_3 8 # ASSIGN : s_1_0 134 # ASSIGN : s_1_1 3 # ASSIGN : s_1_2 9 # ASSIGN : s_1_3 19 # ASSIGN : s_2_0 225 # ASSIGN : s_2_1 4 # ASSIGN : s_2_2 156 # ASSIGN : s_2_3 95 # ASSIGN : s_3_0 74 # ASSIGN : s_3_1 124 # ASSIGN : s_3_2 160 # ASSIGN : s_3_3 202 SHOW_RESULT 232 END : 232 (0 seconds) [Mon Jun 19 23:13:46 2006] SHOW_RESULT 232 CPU : 0.01 = 0.01 + 0 + 0 + 0 # BOUND : makespan 185 232 MODIFY_CNF 208 BEGIN : [Mon Jun 19 23:13:46 2006] MODIFY_CNF 208 END : 511806 bytes (0 seconds) [Mon Jun 19 23:13:46 2006] MODIFY_CNF 208 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 208 BEGIN : [Mon Jun 19 23:13:46 2006] CMD : minisat /tmp/csp2sat13816.cnf /tmp/csp2sat13816.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 22069 61814 | 7356 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 27 (675 /sec) propagations : 4721 (118025 /sec) conflict literals : 0 ( nan % deleted) Memory used : 2.52 MB CPU time : 0.04 s SATISFIABLE VERIFY_CNF 208 END : (0 seconds) [Mon Jun 19 23:13:46 2006] VERIFY_CNF 208 CPU : 0.05 = 0 + 0 + 0.04 + 0.01 # RESULT : makespan 208 SATISFIABLE SHOW_RESULT 208 BEGIN : [Mon Jun 19 23:13:46 2006] # ASSIGN : makespan 208 # ASSIGN : s_0_0 30 # ASSIGN : s_0_1 162 # ASSIGN : s_0_2 71 # ASSIGN : s_0_3 19 # ASSIGN : s_1_0 117 # ASSIGN : s_1_1 10 # ASSIGN : s_1_2 11 # ASSIGN : s_1_3 41 # ASSIGN : s_2_0 14 # ASSIGN : s_2_1 26 # ASSIGN : s_2_2 21 # ASSIGN : s_2_3 117 # ASSIGN : s_3_0 67 # ASSIGN : s_3_1 126 # ASSIGN : s_3_2 25 # ASSIGN : s_3_3 178 SHOW_RESULT 208 END : 208 (0 seconds) [Mon Jun 19 23:13:46 2006] SHOW_RESULT 208 CPU : 0.01 = 0.01 + 0 + 0 + 0 # BOUND : makespan 185 208 MODIFY_CNF 196 BEGIN : [Mon Jun 19 23:13:46 2006] MODIFY_CNF 196 END : 511806 bytes (0 seconds) [Mon Jun 19 23:13:46 2006] MODIFY_CNF 196 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 196 BEGIN : [Mon Jun 19 23:13:46 2006] CMD : minisat /tmp/csp2sat13816.cnf /tmp/csp2sat13816.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 20917 58358 | 6972 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 19 (475 /sec) propagations : 4721 (118025 /sec) conflict literals : 0 ( nan % deleted) Memory used : 2.53 MB CPU time : 0.04 s SATISFIABLE VERIFY_CNF 196 END : (0 seconds) [Mon Jun 19 23:13:46 2006] VERIFY_CNF 196 CPU : 0.04 = 0 + 0 + 0.04 + 0 # RESULT : makespan 196 SATISFIABLE SHOW_RESULT 196 BEGIN : [Mon Jun 19 23:13:46 2006] # ASSIGN : makespan 196 # ASSIGN : s_0_0 18 # ASSIGN : s_0_1 150 # ASSIGN : s_0_2 59 # ASSIGN : s_0_3 7 # ASSIGN : s_1_0 105 # ASSIGN : s_1_1 2 # ASSIGN : s_1_2 3 # ASSIGN : s_1_3 29 # ASSIGN : s_2_0 7 # ASSIGN : s_2_1 14 # ASSIGN : s_2_2 192 # ASSIGN : s_2_3 105 # ASSIGN : s_3_0 55 # ASSIGN : s_3_1 114 # ASSIGN : s_3_2 13 # ASSIGN : s_3_3 166 SHOW_RESULT 196 END : 196 (0 seconds) [Mon Jun 19 23:13:46 2006] SHOW_RESULT 196 CPU : 0.01 = 0.01 + 0 + 0 + 0 # BOUND : makespan 185 196 MODIFY_CNF 190 BEGIN : [Mon Jun 19 23:13:46 2006] MODIFY_CNF 190 END : 511805 bytes (0 seconds) [Mon Jun 19 23:13:46 2006] MODIFY_CNF 190 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 190 BEGIN : [Mon Jun 19 23:13:46 2006] CMD : minisat /tmp/csp2sat13816.cnf /tmp/csp2sat13816.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 20341 56630 | 6780 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 1 (33 /sec) decisions : 12 (400 /sec) propagations : 6016 (200533 /sec) conflict literals : 2 (0.00 % deleted) Memory used : 2.53 MB CPU time : 0.03 s SATISFIABLE VERIFY_CNF 190 END : (0 seconds) [Mon Jun 19 23:13:46 2006] VERIFY_CNF 190 CPU : 0.04 = 0 + 0 + 0.03 + 0.01 # RESULT : makespan 190 SATISFIABLE SHOW_RESULT 190 BEGIN : [Mon Jun 19 23:13:46 2006] # ASSIGN : makespan 190 # ASSIGN : s_0_0 142 # ASSIGN : s_0_1 5 # ASSIGN : s_0_2 51 # ASSIGN : s_0_3 179 # ASSIGN : s_1_0 1 # ASSIGN : s_1_1 189 # ASSIGN : s_1_2 176 # ASSIGN : s_1_3 100 # ASSIGN : s_2_0 179 # ASSIGN : s_2_1 62 # ASSIGN : s_2_2 186 # ASSIGN : s_2_3 1 # ASSIGN : s_3_0 92 # ASSIGN : s_3_1 153 # ASSIGN : s_3_2 9 # ASSIGN : s_3_3 62 SHOW_RESULT 190 END : 190 (0 seconds) [Mon Jun 19 23:13:46 2006] SHOW_RESULT 190 CPU : 0.01 = 0.01 + 0 + 0 + 0 # BOUND : makespan 185 190 MODIFY_CNF 187 BEGIN : [Mon Jun 19 23:13:46 2006] MODIFY_CNF 187 END : 511805 bytes (0 seconds) [Mon Jun 19 23:13:46 2006] MODIFY_CNF 187 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 187 BEGIN : [Mon Jun 19 23:13:46 2006] CMD : minisat /tmp/csp2sat13816.cnf /tmp/csp2sat13816.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 20053 55766 | 6684 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 4 (100 /sec) decisions : 3 (75 /sec) propagations : 5770 (144250 /sec) conflict literals : 4 (20.00 % deleted) Memory used : 2.50 MB CPU time : 0.04 s UNSATISFIABLE VERIFY_CNF 187 END : (0 seconds) [Mon Jun 19 23:13:46 2006] VERIFY_CNF 187 CPU : 0.04 = 0 + 0 + 0.04 + 0 # RESULT : makespan 187 UNSATISFIABLE # BOUND : makespan 188 190 MODIFY_CNF 189 BEGIN : [Mon Jun 19 23:13:46 2006] MODIFY_CNF 189 END : 511805 bytes (0 seconds) [Mon Jun 19 23:13:46 2006] MODIFY_CNF 189 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 189 BEGIN : [Mon Jun 19 23:13:46 2006] CMD : minisat /tmp/csp2sat13816.cnf /tmp/csp2sat13816.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 20245 56342 | 6748 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 1 (25 /sec) decisions : 7 (175 /sec) propagations : 6113 (152825 /sec) conflict literals : 2 (0.00 % deleted) Memory used : 2.53 MB CPU time : 0.04 s SATISFIABLE VERIFY_CNF 189 END : (0 seconds) [Mon Jun 19 23:13:46 2006] VERIFY_CNF 189 CPU : 0.04 = 0 + 0 + 0.04 + 0 # RESULT : makespan 189 SATISFIABLE SHOW_RESULT 189 BEGIN : [Mon Jun 19 23:13:46 2006] # ASSIGN : makespan 189 # ASSIGN : s_0_0 141 # ASSIGN : s_0_1 4 # ASSIGN : s_0_2 50 # ASSIGN : s_0_3 178 # ASSIGN : s_1_0 0 # ASSIGN : s_1_1 188 # ASSIGN : s_1_2 175 # ASSIGN : s_1_3 99 # ASSIGN : s_2_0 178 # ASSIGN : s_2_1 61 # ASSIGN : s_2_2 185 # ASSIGN : s_2_3 0 # ASSIGN : s_3_0 91 # ASSIGN : s_3_1 152 # ASSIGN : s_3_2 8 # ASSIGN : s_3_3 61 SHOW_RESULT 189 END : 189 (0 seconds) [Mon Jun 19 23:13:46 2006] SHOW_RESULT 189 CPU : 0.01 = 0.01 + 0 + 0 + 0 # BOUND : makespan 188 189 MODIFY_CNF 188 BEGIN : [Mon Jun 19 23:13:46 2006] MODIFY_CNF 188 END : 511805 bytes (0 seconds) [Mon Jun 19 23:13:46 2006] MODIFY_CNF 188 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 188 BEGIN : [Mon Jun 19 23:13:46 2006] CMD : minisat /tmp/csp2sat13816.cnf /tmp/csp2sat13816.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 20149 56054 | 6716 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 5 (167 /sec) decisions : 5 (167 /sec) propagations : 6888 (229600 /sec) conflict literals : 6 (14.29 % deleted) Memory used : 2.51 MB CPU time : 0.03 s UNSATISFIABLE VERIFY_CNF 188 END : (0 seconds) [Mon Jun 19 23:13:46 2006] VERIFY_CNF 188 CPU : 0.04 = 0 + 0 + 0.03 + 0.01 # RESULT : makespan 188 UNSATISFIABLE # BOUND : makespan 189 189 MAIN END : (2 seconds) [Mon Jun 19 23:13:46 2006] MAIN CPU : 1.55 = 1.25 + 0 + 0.26 + 0.04