# TIMEOUT 18000 MAIN BEGIN : [Mon Jun 19 23:13:46 2006] READ BEGIN : csp/tai_4x4_7.csp [Mon Jun 19 23:13:46 2006] READ END : csp/tai_4x4_7.csp (0 seconds) [Mon Jun 19 23:13:46 2006] READ CPU : 0.11 = 0.11 + 0 + 0 + 0 # BOUND : makespan 197 282 GENERATE_CNF 282 BEGIN : [Mon Jun 19 23:13:46 2006] GENERATE_CNF 282 END : 4743 variables 29188 clauses 511204 bytes (1 seconds) [Mon Jun 19 23:13:47 2006] GENERATE_CNF 282 CPU : 1.07 = 1.07 + 0 + 0 + 0 MODIFY_CNF 239 BEGIN : [Mon Jun 19 23:13:47 2006] MODIFY_CNF 239 END : 511209 bytes (0 seconds) [Mon Jun 19 23:13:47 2006] MODIFY_CNF 239 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 239 BEGIN : [Mon Jun 19 23:13:47 2006] CMD : minisat /tmp/csp2sat13824.cnf /tmp/csp2sat13824.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 24847 70126 | 8282 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 33 (1100 /sec) propagations : 4743 (158100 /sec) conflict literals : 0 ( nan % deleted) Memory used : 2.52 MB CPU time : 0.03 s SATISFIABLE VERIFY_CNF 239 END : (0 seconds) [Mon Jun 19 23:13:47 2006] VERIFY_CNF 239 CPU : 0.04 = 0 + 0 + 0.04 + 0 # RESULT : makespan 239 SATISFIABLE SHOW_RESULT 239 BEGIN : [Mon Jun 19 23:13:47 2006] # ASSIGN : makespan 239 # ASSIGN : s_0_0 152 # ASSIGN : s_0_1 222 # ASSIGN : s_0_2 46 # ASSIGN : s_0_3 55 # ASSIGN : s_1_0 209 # ASSIGN : s_1_1 8 # ASSIGN : s_1_2 60 # ASSIGN : s_1_3 138 # ASSIGN : s_2_0 34 # ASSIGN : s_2_1 51 # ASSIGN : s_2_2 153 # ASSIGN : s_2_3 178 # ASSIGN : s_3_0 42 # ASSIGN : s_3_1 108 # ASSIGN : s_3_2 172 # ASSIGN : s_3_3 234 SHOW_RESULT 239 END : 239 (0 seconds) [Mon Jun 19 23:13:47 2006] SHOW_RESULT 239 CPU : 0.01 = 0.01 + 0 + 0 + 0 # BOUND : makespan 197 239 MODIFY_CNF 218 BEGIN : [Mon Jun 19 23:13:47 2006] MODIFY_CNF 218 END : 511209 bytes (0 seconds) [Mon Jun 19 23:13:47 2006] MODIFY_CNF 218 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 218 BEGIN : [Mon Jun 19 23:13:47 2006] CMD : minisat /tmp/csp2sat13824.cnf /tmp/csp2sat13824.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 22831 64078 | 7610 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 1 (33 /sec) decisions : 30 (1000 /sec) propagations : 5211 (173700 /sec) conflict literals : 6 (14.29 % deleted) Memory used : 2.52 MB CPU time : 0.03 s SATISFIABLE VERIFY_CNF 218 END : (0 seconds) [Mon Jun 19 23:13:47 2006] VERIFY_CNF 218 CPU : 0.04 = 0 + 0 + 0.04 + 0 # RESULT : makespan 218 SATISFIABLE SHOW_RESULT 218 BEGIN : [Mon Jun 19 23:13:47 2006] # ASSIGN : makespan 218 # ASSIGN : s_0_0 161 # ASSIGN : s_0_1 13 # ASSIGN : s_0_2 0 # ASSIGN : s_0_3 34 # ASSIGN : s_1_0 87 # ASSIGN : s_1_1 175 # ASSIGN : s_1_2 9 # ASSIGN : s_1_3 117 # ASSIGN : s_2_0 13 # ASSIGN : s_2_1 30 # ASSIGN : s_2_2 132 # ASSIGN : s_2_3 157 # ASSIGN : s_3_0 21 # ASSIGN : s_3_1 87 # ASSIGN : s_3_2 151 # ASSIGN : s_3_3 213 SHOW_RESULT 218 END : 218 (0 seconds) [Mon Jun 19 23:13:47 2006] SHOW_RESULT 218 CPU : 0.01 = 0.01 + 0 + 0 + 0 # BOUND : makespan 197 218 MODIFY_CNF 207 BEGIN : [Mon Jun 19 23:13:47 2006] MODIFY_CNF 207 END : 511209 bytes (0 seconds) [Mon Jun 19 23:13:47 2006] MODIFY_CNF 207 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 207 BEGIN : [Mon Jun 19 23:13:47 2006] CMD : minisat /tmp/csp2sat13824.cnf /tmp/csp2sat13824.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 21775 60910 | 7258 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 26 (650 /sec) propagations : 4743 (118575 /sec) conflict literals : 0 ( nan % deleted) Memory used : 2.52 MB CPU time : 0.04 s SATISFIABLE VERIFY_CNF 207 END : (0 seconds) [Mon Jun 19 23:13:47 2006] VERIFY_CNF 207 CPU : 0.04 = 0 + 0 + 0.04 + 0 # RESULT : makespan 207 SATISFIABLE SHOW_RESULT 207 BEGIN : [Mon Jun 19 23:13:47 2006] # ASSIGN : makespan 207 # ASSIGN : s_0_0 120 # ASSIGN : s_0_1 190 # ASSIGN : s_0_2 2 # ASSIGN : s_0_3 11 # ASSIGN : s_1_0 177 # ASSIGN : s_1_1 134 # ASSIGN : s_1_2 16 # ASSIGN : s_1_3 94 # ASSIGN : s_2_0 112 # ASSIGN : s_2_1 13 # ASSIGN : s_2_2 121 # ASSIGN : s_2_3 146 # ASSIGN : s_3_0 4 # ASSIGN : s_3_1 70 # ASSIGN : s_3_2 140 # ASSIGN : s_3_3 202 SHOW_RESULT 207 END : 207 (0 seconds) [Mon Jun 19 23:13:47 2006] SHOW_RESULT 207 CPU : 0.01 = 0.01 + 0 + 0 + 0 # BOUND : makespan 197 207 MODIFY_CNF 202 BEGIN : [Mon Jun 19 23:13:47 2006] MODIFY_CNF 202 END : 511208 bytes (0 seconds) [Mon Jun 19 23:13:47 2006] MODIFY_CNF 202 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 202 BEGIN : [Mon Jun 19 23:13:47 2006] CMD : minisat /tmp/csp2sat13824.cnf /tmp/csp2sat13824.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 21295 59470 | 7098 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (67 /sec) decisions : 23 (767 /sec) propagations : 6661 (222033 /sec) conflict literals : 8 (38.46 % deleted) Memory used : 2.52 MB CPU time : 0.03 s SATISFIABLE VERIFY_CNF 202 END : (0 seconds) [Mon Jun 19 23:13:47 2006] VERIFY_CNF 202 CPU : 0.04 = 0 + 0 + 0.03 + 0.01 # RESULT : makespan 202 SATISFIABLE SHOW_RESULT 202 BEGIN : [Mon Jun 19 23:13:47 2006] # ASSIGN : makespan 202 # ASSIGN : s_0_0 1 # ASSIGN : s_0_1 176 # ASSIGN : s_0_2 193 # ASSIGN : s_0_3 58 # ASSIGN : s_1_0 172 # ASSIGN : s_1_1 129 # ASSIGN : s_1_2 51 # ASSIGN : s_1_3 11 # ASSIGN : s_2_0 133 # ASSIGN : s_2_1 72 # ASSIGN : s_2_2 32 # ASSIGN : s_2_3 141 # ASSIGN : s_3_0 65 # ASSIGN : s_3_1 1 # ASSIGN : s_3_2 131 # ASSIGN : s_3_3 197 SHOW_RESULT 202 END : 202 (0 seconds) [Mon Jun 19 23:13:47 2006] SHOW_RESULT 202 CPU : 0.01 = 0.01 + 0 + 0 + 0 # BOUND : makespan 197 202 MODIFY_CNF 199 BEGIN : [Mon Jun 19 23:13:47 2006] MODIFY_CNF 199 END : 511208 bytes (0 seconds) [Mon Jun 19 23:13:47 2006] MODIFY_CNF 199 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 199 BEGIN : [Mon Jun 19 23:13:47 2006] CMD : minisat /tmp/csp2sat13824.cnf /tmp/csp2sat13824.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 21007 58606 | 7002 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 21 (525 /sec) decisions : 22 (550 /sec) propagations : 17893 (447325 /sec) conflict literals : 67 (25.56 % deleted) Memory used : 2.50 MB CPU time : 0.04 s UNSATISFIABLE VERIFY_CNF 199 END : (0 seconds) [Mon Jun 19 23:13:47 2006] VERIFY_CNF 199 CPU : 0.05 = 0 + 0 + 0.04 + 0.01 # RESULT : makespan 199 UNSATISFIABLE # BOUND : makespan 200 202 MODIFY_CNF 201 BEGIN : [Mon Jun 19 23:13:47 2006] MODIFY_CNF 201 END : 511208 bytes (0 seconds) [Mon Jun 19 23:13:47 2006] MODIFY_CNF 201 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 201 BEGIN : [Mon Jun 19 23:13:47 2006] CMD : minisat /tmp/csp2sat13824.cnf /tmp/csp2sat13824.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 21199 59182 | 7066 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (67 /sec) decisions : 18 (600 /sec) propagations : 6839 (227967 /sec) conflict literals : 7 (41.67 % deleted) Memory used : 2.52 MB CPU time : 0.03 s SATISFIABLE VERIFY_CNF 201 END : (0 seconds) [Mon Jun 19 23:13:47 2006] VERIFY_CNF 201 CPU : 0.04 = 0 + 0 + 0.03 + 0.01 # RESULT : makespan 201 SATISFIABLE SHOW_RESULT 201 BEGIN : [Mon Jun 19 23:13:47 2006] # ASSIGN : makespan 201 # ASSIGN : s_0_0 0 # ASSIGN : s_0_1 175 # ASSIGN : s_0_2 192 # ASSIGN : s_0_3 57 # ASSIGN : s_1_0 171 # ASSIGN : s_1_1 128 # ASSIGN : s_1_2 50 # ASSIGN : s_1_3 10 # ASSIGN : s_2_0 132 # ASSIGN : s_2_1 71 # ASSIGN : s_2_2 31 # ASSIGN : s_2_3 140 # ASSIGN : s_3_0 64 # ASSIGN : s_3_1 0 # ASSIGN : s_3_2 130 # ASSIGN : s_3_3 196 SHOW_RESULT 201 END : 201 (0 seconds) [Mon Jun 19 23:13:47 2006] SHOW_RESULT 201 CPU : 0.01 = 0.01 + 0 + 0 + 0 # BOUND : makespan 200 201 MODIFY_CNF 200 BEGIN : [Mon Jun 19 23:13:47 2006] MODIFY_CNF 200 END : 511208 bytes (0 seconds) [Mon Jun 19 23:13:47 2006] MODIFY_CNF 200 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 200 BEGIN : [Mon Jun 19 23:13:47 2006] CMD : minisat /tmp/csp2sat13824.cnf /tmp/csp2sat13824.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 21103 58894 | 7034 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 22 (550 /sec) decisions : 25 (625 /sec) propagations : 19265 (481625 /sec) conflict literals : 68 (22.73 % deleted) Memory used : 2.50 MB CPU time : 0.04 s UNSATISFIABLE VERIFY_CNF 200 END : (0 seconds) [Mon Jun 19 23:13:47 2006] VERIFY_CNF 200 CPU : 0.04 = 0 + 0 + 0.04 + 0 # RESULT : makespan 200 UNSATISFIABLE # BOUND : makespan 201 201 MAIN END : (1 seconds) [Mon Jun 19 23:13:47 2006] MAIN CPU : 1.52 = 1.23 + 0 + 0.26 + 0.03