# TIMEOUT 18000 MAIN BEGIN : [Mon Jun 19 23:13:47 2006] READ BEGIN : csp/tai_4x4_8.csp [Mon Jun 19 23:13:47 2006] READ END : csp/tai_4x4_8.csp (1 seconds) [Mon Jun 19 23:13:48 2006] READ CPU : 0.12 = 0.11 + 0.01 + 0 + 0 # BOUND : makespan 212 335 GENERATE_CNF 335 BEGIN : [Mon Jun 19 23:13:48 2006] GENERATE_CNF 335 END : 5629 variables 35110 clauses 618206 bytes (1 seconds) [Mon Jun 19 23:13:49 2006] GENERATE_CNF 335 CPU : 1.3 = 1.3 + 0 + 0 + 0 MODIFY_CNF 273 BEGIN : [Mon Jun 19 23:13:49 2006] MODIFY_CNF 273 END : 618211 bytes (0 seconds) [Mon Jun 19 23:13:49 2006] MODIFY_CNF 273 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 273 BEGIN : [Mon Jun 19 23:13:49 2006] CMD : minisat /tmp/csp2sat13832.cnf /tmp/csp2sat13832.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 28945 81534 | 9648 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 1 (20 /sec) decisions : 35 (700 /sec) propagations : 7084 (141680 /sec) conflict literals : 6 (0.00 % deleted) Memory used : 2.94 MB CPU time : 0.05 s SATISFIABLE VERIFY_CNF 273 END : (0 seconds) [Mon Jun 19 23:13:49 2006] VERIFY_CNF 273 CPU : 0.05 = 0 + 0 + 0.05 + 0 # RESULT : makespan 273 SATISFIABLE SHOW_RESULT 273 BEGIN : [Mon Jun 19 23:13:49 2006] # ASSIGN : makespan 273 # ASSIGN : s_0_0 115 # ASSIGN : s_0_1 176 # ASSIGN : s_0_2 259 # ASSIGN : s_0_3 15 # ASSIGN : s_1_0 131 # ASSIGN : s_1_1 20 # ASSIGN : s_1_2 1 # ASSIGN : s_1_3 110 # ASSIGN : s_2_0 212 # ASSIGN : s_2_1 143 # ASSIGN : s_2_2 29 # ASSIGN : s_2_3 168 # ASSIGN : s_3_0 64 # ASSIGN : s_3_1 264 # ASSIGN : s_3_2 125 # ASSIGN : s_3_3 172 SHOW_RESULT 273 END : 273 (0 seconds) [Mon Jun 19 23:13:49 2006] SHOW_RESULT 273 CPU : 0.01 = 0.01 + 0 + 0 + 0 # BOUND : makespan 212 273 MODIFY_CNF 242 BEGIN : [Mon Jun 19 23:13:49 2006] MODIFY_CNF 242 END : 618211 bytes (0 seconds) [Mon Jun 19 23:13:49 2006] MODIFY_CNF 242 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 242 BEGIN : [Mon Jun 19 23:13:49 2006] CMD : minisat /tmp/csp2sat13832.cnf /tmp/csp2sat13832.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 25969 72606 | 8656 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 26 (1300 /sec) propagations : 5629 (281450 /sec) conflict literals : 0 ( nan % deleted) Memory used : 2.94 MB CPU time : 0.02 s SATISFIABLE VERIFY_CNF 242 END : (0 seconds) [Mon Jun 19 23:13:49 2006] VERIFY_CNF 242 CPU : 0.05 = 0 + 0 + 0.02 + 0.03 # RESULT : makespan 242 SATISFIABLE SHOW_RESULT 242 BEGIN : [Mon Jun 19 23:13:49 2006] # ASSIGN : makespan 242 # ASSIGN : s_0_0 5 # ASSIGN : s_0_1 150 # ASSIGN : s_0_2 132 # ASSIGN : s_0_3 21 # ASSIGN : s_1_0 161 # ASSIGN : s_1_1 22 # ASSIGN : s_1_2 3 # ASSIGN : s_1_3 116 # ASSIGN : s_2_0 29 # ASSIGN : s_2_1 112 # ASSIGN : s_2_2 146 # ASSIGN : s_2_3 137 # ASSIGN : s_3_0 90 # ASSIGN : s_3_1 233 # ASSIGN : s_3_2 43 # ASSIGN : s_3_3 141 SHOW_RESULT 242 END : 242 (0 seconds) [Mon Jun 19 23:13:49 2006] SHOW_RESULT 242 CPU : 0 = 0 + 0 + 0 + 0 # BOUND : makespan 212 242 MODIFY_CNF 227 BEGIN : [Mon Jun 19 23:13:49 2006] MODIFY_CNF 227 END : 618211 bytes (0 seconds) [Mon Jun 19 23:13:49 2006] MODIFY_CNF 227 CPU : 0.01 = 0.01 + 0 + 0 + 0 VERIFY_CNF 227 BEGIN : [Mon Jun 19 23:13:49 2006] CMD : minisat /tmp/csp2sat13832.cnf /tmp/csp2sat13832.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 24529 68286 | 8176 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 1 (33 /sec) decisions : 19 (633 /sec) propagations : 6209 (206967 /sec) conflict literals : 4 (20.00 % deleted) Memory used : 2.95 MB CPU time : 0.03 s SATISFIABLE VERIFY_CNF 227 END : (0 seconds) [Mon Jun 19 23:13:49 2006] VERIFY_CNF 227 CPU : 0.05 = 0 + 0 + 0.03 + 0.02 # RESULT : makespan 227 SATISFIABLE SHOW_RESULT 227 BEGIN : [Mon Jun 19 23:13:49 2006] # ASSIGN : makespan 227 # ASSIGN : s_0_0 211 # ASSIGN : s_0_1 128 # ASSIGN : s_0_2 17 # ASSIGN : s_0_3 31 # ASSIGN : s_1_0 127 # ASSIGN : s_1_1 37 # ASSIGN : s_1_2 208 # ASSIGN : s_1_3 6 # ASSIGN : s_2_0 51 # ASSIGN : s_2_1 2 # ASSIGN : s_2_2 112 # ASSIGN : s_2_3 27 # ASSIGN : s_3_0 0 # ASSIGN : s_3_1 218 # ASSIGN : s_3_2 65 # ASSIGN : s_3_3 126 SHOW_RESULT 227 END : 227 (0 seconds) [Mon Jun 19 23:13:49 2006] SHOW_RESULT 227 CPU : 0.01 = 0.01 + 0 + 0 + 0 # BOUND : makespan 212 227 MODIFY_CNF 219 BEGIN : [Mon Jun 19 23:13:49 2006] MODIFY_CNF 219 END : 618210 bytes (0 seconds) [Mon Jun 19 23:13:49 2006] MODIFY_CNF 219 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 219 BEGIN : [Mon Jun 19 23:13:49 2006] CMD : minisat /tmp/csp2sat13832.cnf /tmp/csp2sat13832.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 23761 65982 | 7920 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 5 (125 /sec) decisions : 24 (600 /sec) propagations : 10972 (274300 /sec) conflict literals : 21 (25.00 % deleted) Memory used : 2.95 MB CPU time : 0.04 s SATISFIABLE VERIFY_CNF 219 END : (0 seconds) [Mon Jun 19 23:13:49 2006] VERIFY_CNF 219 CPU : 0.05 = 0 + 0 + 0.04 + 0.01 # RESULT : makespan 219 SATISFIABLE SHOW_RESULT 219 BEGIN : [Mon Jun 19 23:13:49 2006] # ASSIGN : makespan 219 # ASSIGN : s_0_0 6 # ASSIGN : s_0_1 41 # ASSIGN : s_0_2 27 # ASSIGN : s_0_3 124 # ASSIGN : s_1_0 22 # ASSIGN : s_1_1 129 # ASSIGN : s_1_2 3 # ASSIGN : s_1_3 103 # ASSIGN : s_2_0 158 # ASSIGN : s_2_1 16 # ASSIGN : s_2_2 62 # ASSIGN : s_2_3 7 # ASSIGN : s_3_0 107 # ASSIGN : s_3_1 2 # ASSIGN : s_3_2 172 # ASSIGN : s_3_3 11 SHOW_RESULT 219 END : 219 (0 seconds) [Mon Jun 19 23:13:49 2006] SHOW_RESULT 219 CPU : 0.01 = 0.01 + 0 + 0 + 0 # BOUND : makespan 212 219 MODIFY_CNF 215 BEGIN : [Mon Jun 19 23:13:49 2006] MODIFY_CNF 215 END : 618210 bytes (0 seconds) [Mon Jun 19 23:13:49 2006] MODIFY_CNF 215 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 215 BEGIN : [Mon Jun 19 23:13:49 2006] CMD : minisat /tmp/csp2sat13832.cnf /tmp/csp2sat13832.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 23377 64830 | 7792 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 14 (350 /sec) decisions : 13 (325 /sec) propagations : 17111 (427775 /sec) conflict literals : 30 (30.23 % deleted) Memory used : 2.91 MB CPU time : 0.04 s UNSATISFIABLE VERIFY_CNF 215 END : (0 seconds) [Mon Jun 19 23:13:49 2006] VERIFY_CNF 215 CPU : 0.05 = 0 + 0 + 0.04 + 0.01 # RESULT : makespan 215 UNSATISFIABLE # BOUND : makespan 216 219 MODIFY_CNF 217 BEGIN : [Mon Jun 19 23:13:49 2006] MODIFY_CNF 217 END : 618210 bytes (0 seconds) [Mon Jun 19 23:13:49 2006] MODIFY_CNF 217 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 217 BEGIN : [Mon Jun 19 23:13:49 2006] CMD : minisat /tmp/csp2sat13832.cnf /tmp/csp2sat13832.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 23569 65406 | 7856 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 5 (125 /sec) decisions : 22 (550 /sec) propagations : 10971 (274275 /sec) conflict literals : 20 (20.00 % deleted) Memory used : 2.95 MB CPU time : 0.04 s SATISFIABLE VERIFY_CNF 217 END : (0 seconds) [Mon Jun 19 23:13:49 2006] VERIFY_CNF 217 CPU : 0.06 = 0 + 0 + 0.05 + 0.01 # RESULT : makespan 217 SATISFIABLE SHOW_RESULT 217 BEGIN : [Mon Jun 19 23:13:49 2006] # ASSIGN : makespan 217 # ASSIGN : s_0_0 4 # ASSIGN : s_0_1 39 # ASSIGN : s_0_2 25 # ASSIGN : s_0_3 122 # ASSIGN : s_1_0 20 # ASSIGN : s_1_1 127 # ASSIGN : s_1_2 1 # ASSIGN : s_1_3 101 # ASSIGN : s_2_0 156 # ASSIGN : s_2_1 14 # ASSIGN : s_2_2 60 # ASSIGN : s_2_3 5 # ASSIGN : s_3_0 105 # ASSIGN : s_3_1 0 # ASSIGN : s_3_2 170 # ASSIGN : s_3_3 9 SHOW_RESULT 217 END : 217 (0 seconds) [Mon Jun 19 23:13:49 2006] SHOW_RESULT 217 CPU : 0.01 = 0.01 + 0 + 0 + 0 # BOUND : makespan 216 217 MODIFY_CNF 216 BEGIN : [Mon Jun 19 23:13:49 2006] MODIFY_CNF 216 END : 618210 bytes (0 seconds) [Mon Jun 19 23:13:49 2006] MODIFY_CNF 216 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 216 BEGIN : [Mon Jun 19 23:13:49 2006] CMD : minisat /tmp/csp2sat13832.cnf /tmp/csp2sat13832.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 23473 65118 | 7824 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 22 (440 /sec) decisions : 24 (480 /sec) propagations : 23590 (471800 /sec) conflict literals : 79 (17.71 % deleted) Memory used : 2.92 MB CPU time : 0.05 s UNSATISFIABLE VERIFY_CNF 216 END : (0 seconds) [Mon Jun 19 23:13:49 2006] VERIFY_CNF 216 CPU : 0.06 = 0 + 0 + 0.05 + 0.01 # RESULT : makespan 216 UNSATISFIABLE # BOUND : makespan 217 217 MAIN END : (2 seconds) [Mon Jun 19 23:13:49 2006] MAIN CPU : 1.84 = 1.46 + 0.01 + 0.28 + 0.09