# TIMEOUT 18000 MAIN BEGIN : [Mon Jun 19 23:13:37 2006] READ BEGIN : csp/tai_4x4_2.csp [Mon Jun 19 23:13:37 2006] READ END : csp/tai_4x4_2.csp (1 seconds) [Mon Jun 19 23:13:38 2006] READ CPU : 0.12 = 0.12 + 0 + 0 + 0 # BOUND : makespan 229 278 GENERATE_CNF 278 BEGIN : [Mon Jun 19 23:13:38 2006] GENERATE_CNF 278 END : 4643 variables 27426 clauses 479764 bytes (1 seconds) [Mon Jun 19 23:13:39 2006] GENERATE_CNF 278 CPU : 1.01 = 1.01 + 0 + 0 + 0 MODIFY_CNF 253 BEGIN : [Mon Jun 19 23:13:39 2006] MODIFY_CNF 253 END : 479769 bytes (0 seconds) [Mon Jun 19 23:13:39 2006] MODIFY_CNF 253 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 253 BEGIN : [Mon Jun 19 23:13:39 2006] CMD : minisat /tmp/csp2sat13787.cnf /tmp/csp2sat13787.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 24813 70124 | 8271 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 21 (700 /sec) propagations : 4643 (154767 /sec) conflict literals : 0 ( nan % deleted) Memory used : 2.44 MB CPU time : 0.03 s SATISFIABLE VERIFY_CNF 253 END : (0 seconds) [Mon Jun 19 23:13:39 2006] VERIFY_CNF 253 CPU : 0.03 = 0 + 0 + 0.03 + 0 # RESULT : makespan 253 SATISFIABLE SHOW_RESULT 253 BEGIN : [Mon Jun 19 23:13:39 2006] # ASSIGN : makespan 253 # ASSIGN : s_0_0 86 # ASSIGN : s_0_1 170 # ASSIGN : s_0_2 16 # ASSIGN : s_0_3 11 # ASSIGN : s_1_0 173 # ASSIGN : s_1_1 56 # ASSIGN : s_1_2 102 # ASSIGN : s_1_3 32 # ASSIGN : s_2_0 131 # ASSIGN : s_2_1 0 # ASSIGN : s_2_2 160 # ASSIGN : s_2_3 70 # ASSIGN : s_3_0 12 # ASSIGN : s_3_1 101 # ASSIGN : s_3_2 189 # ASSIGN : s_3_3 146 SHOW_RESULT 253 END : 253 (0 seconds) [Mon Jun 19 23:13:39 2006] SHOW_RESULT 253 CPU : 0 = 0 + 0 + 0 + 0 # BOUND : makespan 229 253 MODIFY_CNF 241 BEGIN : [Mon Jun 19 23:13:39 2006] MODIFY_CNF 241 END : 479769 bytes (0 seconds) [Mon Jun 19 23:13:39 2006] MODIFY_CNF 241 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 241 BEGIN : [Mon Jun 19 23:13:39 2006] CMD : minisat /tmp/csp2sat13787.cnf /tmp/csp2sat13787.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 23661 66668 | 7887 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 5 (167 /sec) decisions : 25 (833 /sec) propagations : 9128 (304267 /sec) conflict literals : 30 (26.83 % deleted) Memory used : 2.44 MB CPU time : 0.03 s SATISFIABLE VERIFY_CNF 241 END : (0 seconds) [Mon Jun 19 23:13:39 2006] VERIFY_CNF 241 CPU : 0.04 = 0 + 0 + 0.03 + 0.01 # RESULT : makespan 241 SATISFIABLE SHOW_RESULT 241 BEGIN : [Mon Jun 19 23:13:39 2006] # ASSIGN : makespan 241 # ASSIGN : s_0_0 167 # ASSIGN : s_0_1 6 # ASSIGN : s_0_2 97 # ASSIGN : s_0_3 0 # ASSIGN : s_1_0 87 # ASSIGN : s_1_1 196 # ASSIGN : s_1_2 29 # ASSIGN : s_1_3 5 # ASSIGN : s_2_0 212 # ASSIGN : s_2_1 140 # ASSIGN : s_2_2 0 # ASSIGN : s_2_3 73 # ASSIGN : s_3_0 13 # ASSIGN : s_3_1 89 # ASSIGN : s_3_2 177 # ASSIGN : s_3_3 134 SHOW_RESULT 241 END : 241 (0 seconds) [Mon Jun 19 23:13:39 2006] SHOW_RESULT 241 CPU : 0 = 0 + 0 + 0 + 0 # BOUND : makespan 229 241 MODIFY_CNF 235 BEGIN : [Mon Jun 19 23:13:39 2006] MODIFY_CNF 235 END : 479768 bytes (0 seconds) [Mon Jun 19 23:13:39 2006] MODIFY_CNF 235 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 235 BEGIN : [Mon Jun 19 23:13:39 2006] CMD : minisat /tmp/csp2sat13787.cnf /tmp/csp2sat13787.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 23085 64940 | 7695 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 67 (1340 /sec) decisions : 75 (1500 /sec) propagations : 64161 (1283220 /sec) conflict literals : 276 (36.11 % deleted) Memory used : 2.43 MB CPU time : 0.05 s UNSATISFIABLE VERIFY_CNF 235 END : (0 seconds) [Mon Jun 19 23:13:39 2006] VERIFY_CNF 235 CPU : 0.06 = 0 + 0 + 0.05 + 0.01 # RESULT : makespan 235 UNSATISFIABLE # BOUND : makespan 236 241 MODIFY_CNF 238 BEGIN : [Mon Jun 19 23:13:39 2006] MODIFY_CNF 238 END : 479769 bytes (0 seconds) [Mon Jun 19 23:13:39 2006] MODIFY_CNF 238 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 238 BEGIN : [Mon Jun 19 23:13:39 2006] CMD : minisat /tmp/csp2sat13787.cnf /tmp/csp2sat13787.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 23373 65804 | 7791 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 13 (433 /sec) decisions : 36 (1200 /sec) propagations : 15843 (528100 /sec) conflict literals : 82 (22.64 % deleted) Memory used : 2.44 MB CPU time : 0.03 s SATISFIABLE VERIFY_CNF 238 END : (0 seconds) [Mon Jun 19 23:13:39 2006] VERIFY_CNF 238 CPU : 0.04 = 0 + 0 + 0.03 + 0.01 # RESULT : makespan 238 SATISFIABLE SHOW_RESULT 238 BEGIN : [Mon Jun 19 23:13:39 2006] # ASSIGN : makespan 238 # ASSIGN : s_0_0 2 # ASSIGN : s_0_1 54 # ASSIGN : s_0_2 139 # ASSIGN : s_0_3 47 # ASSIGN : s_1_0 158 # ASSIGN : s_1_1 7 # ASSIGN : s_1_2 81 # ASSIGN : s_1_3 52 # ASSIGN : s_2_0 47 # ASSIGN : s_2_1 137 # ASSIGN : s_2_2 209 # ASSIGN : s_2_3 76 # ASSIGN : s_3_0 76 # ASSIGN : s_3_1 193 # ASSIGN : s_3_2 12 # ASSIGN : s_3_3 150 SHOW_RESULT 238 END : 238 (0 seconds) [Mon Jun 19 23:13:39 2006] SHOW_RESULT 238 CPU : 0 = 0 + 0 + 0 + 0 # BOUND : makespan 236 238 MODIFY_CNF 237 BEGIN : [Mon Jun 19 23:13:39 2006] MODIFY_CNF 237 END : 479769 bytes (0 seconds) [Mon Jun 19 23:13:39 2006] MODIFY_CNF 237 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 237 BEGIN : [Mon Jun 19 23:13:39 2006] CMD : minisat /tmp/csp2sat13787.cnf /tmp/csp2sat13787.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 23277 65516 | 7759 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 13 (325 /sec) decisions : 35 (875 /sec) propagations : 15889 (397225 /sec) conflict literals : 81 (22.12 % deleted) Memory used : 2.44 MB CPU time : 0.04 s SATISFIABLE VERIFY_CNF 237 END : (0 seconds) [Mon Jun 19 23:13:39 2006] VERIFY_CNF 237 CPU : 0.04 = 0 + 0 + 0.04 + 0 # RESULT : makespan 237 SATISFIABLE SHOW_RESULT 237 BEGIN : [Mon Jun 19 23:13:39 2006] # ASSIGN : makespan 237 # ASSIGN : s_0_0 1 # ASSIGN : s_0_1 53 # ASSIGN : s_0_2 138 # ASSIGN : s_0_3 46 # ASSIGN : s_1_0 157 # ASSIGN : s_1_1 6 # ASSIGN : s_1_2 80 # ASSIGN : s_1_3 51 # ASSIGN : s_2_0 46 # ASSIGN : s_2_1 136 # ASSIGN : s_2_2 208 # ASSIGN : s_2_3 75 # ASSIGN : s_3_0 75 # ASSIGN : s_3_1 192 # ASSIGN : s_3_2 11 # ASSIGN : s_3_3 149 SHOW_RESULT 237 END : 237 (0 seconds) [Mon Jun 19 23:13:39 2006] SHOW_RESULT 237 CPU : 0.01 = 0.01 + 0 + 0 + 0 # BOUND : makespan 236 237 MODIFY_CNF 236 BEGIN : [Mon Jun 19 23:13:39 2006] MODIFY_CNF 236 END : 479768 bytes (0 seconds) [Mon Jun 19 23:13:39 2006] MODIFY_CNF 236 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 236 BEGIN : [Mon Jun 19 23:13:39 2006] CMD : minisat /tmp/csp2sat13787.cnf /tmp/csp2sat13787.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 23181 65228 | 7727 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 14 (467 /sec) decisions : 35 (1167 /sec) propagations : 18651 (621700 /sec) conflict literals : 83 (34.13 % deleted) Memory used : 2.44 MB CPU time : 0.03 s SATISFIABLE VERIFY_CNF 236 END : (0 seconds) [Mon Jun 19 23:13:39 2006] VERIFY_CNF 236 CPU : 0.04 = 0 + 0 + 0.03 + 0.01 # RESULT : makespan 236 SATISFIABLE SHOW_RESULT 236 BEGIN : [Mon Jun 19 23:13:39 2006] # ASSIGN : makespan 236 # ASSIGN : s_0_0 0 # ASSIGN : s_0_1 52 # ASSIGN : s_0_2 137 # ASSIGN : s_0_3 45 # ASSIGN : s_1_0 156 # ASSIGN : s_1_1 5 # ASSIGN : s_1_2 79 # ASSIGN : s_1_3 50 # ASSIGN : s_2_0 45 # ASSIGN : s_2_1 135 # ASSIGN : s_2_2 207 # ASSIGN : s_2_3 74 # ASSIGN : s_3_0 74 # ASSIGN : s_3_1 191 # ASSIGN : s_3_2 10 # ASSIGN : s_3_3 148 SHOW_RESULT 236 END : 236 (0 seconds) [Mon Jun 19 23:13:39 2006] SHOW_RESULT 236 CPU : 0 = 0 + 0 + 0 + 0 # BOUND : makespan 236 236 MAIN END : (2 seconds) [Mon Jun 19 23:13:39 2006] MAIN CPU : 1.41 = 1.16 + 0 + 0.21 + 0.04