# TIMEOUT 18000 MAIN BEGIN : [Mon Jun 19 23:13:51 2006] READ BEGIN : csp/tai_5x5_1.csp [Mon Jun 19 23:13:51 2006] READ END : csp/tai_5x5_1.csp (0 seconds) [Mon Jun 19 23:13:51 2006] READ CPU : 0.23 = 0.23 + 0 + 0 + 0 # BOUND : makespan 295 444 GENERATE_CNF 444 BEGIN : [Mon Jun 19 23:13:51 2006] GENERATE_CNF 444 END : 11526 variables 94098 clauses 1802732 bytes (4 seconds) [Mon Jun 19 23:13:55 2006] GENERATE_CNF 444 CPU : 3.5 = 3.49 + 0.01 + 0 + 0 MODIFY_CNF 369 BEGIN : [Mon Jun 19 23:13:55 2006] MODIFY_CNF 369 END : 1802737 bytes (0 seconds) [Mon Jun 19 23:13:55 2006] MODIFY_CNF 369 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 369 BEGIN : [Mon Jun 19 23:13:55 2006] CMD : minisat /tmp/csp2sat13847.cnf /tmp/csp2sat13847.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 78718 225211 | 26239 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (17 /sec) decisions : 71 (592 /sec) propagations : 12727 (106058 /sec) conflict literals : 9 (0.00 % deleted) Memory used : 5.91 MB CPU time : 0.12 s SATISFIABLE VERIFY_CNF 369 END : (0 seconds) [Mon Jun 19 23:13:55 2006] VERIFY_CNF 369 CPU : 0.13 = 0 + 0 + 0.13 + 0 # RESULT : makespan 369 SATISFIABLE SHOW_RESULT 369 BEGIN : [Mon Jun 19 23:13:55 2006] # ASSIGN : makespan 369 # ASSIGN : s_0_0 170 # ASSIGN : s_0_1 234 # ASSIGN : s_0_2 46 # ASSIGN : s_0_3 77 # ASSIGN : s_0_4 2 # ASSIGN : s_1_0 29 # ASSIGN : s_1_1 300 # ASSIGN : s_1_2 94 # ASSIGN : s_1_3 162 # ASSIGN : s_1_4 56 # ASSIGN : s_2_0 295 # ASSIGN : s_2_1 4 # ASSIGN : s_2_2 201 # ASSIGN : s_2_3 176 # ASSIGN : s_2_4 74 # ASSIGN : s_3_0 36 # ASSIGN : s_3_1 119 # ASSIGN : s_3_2 261 # ASSIGN : s_3_3 177 # ASSIGN : s_3_4 164 # ASSIGN : s_4_0 90 # ASSIGN : s_4_1 189 # ASSIGN : s_4_2 359 # ASSIGN : s_4_3 253 # ASSIGN : s_4_4 268 SHOW_RESULT 369 END : 369 (0 seconds) [Mon Jun 19 23:13:55 2006] SHOW_RESULT 369 CPU : 0.02 = 0.02 + 0 + 0 + 0 # BOUND : makespan 295 369 MODIFY_CNF 332 BEGIN : [Mon Jun 19 23:13:55 2006] MODIFY_CNF 332 END : 1802737 bytes (0 seconds) [Mon Jun 19 23:13:55 2006] MODIFY_CNF 332 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 332 BEGIN : [Mon Jun 19 23:13:55 2006] CMD : minisat /tmp/csp2sat13847.cnf /tmp/csp2sat13847.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 71318 203011 | 23772 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (17 /sec) decisions : 58 (483 /sec) propagations : 14106 (117550 /sec) conflict literals : 6 (0.00 % deleted) Memory used : 5.94 MB CPU time : 0.12 s SATISFIABLE VERIFY_CNF 332 END : (0 seconds) [Mon Jun 19 23:13:55 2006] VERIFY_CNF 332 CPU : 0.13 = 0 + 0 + 0.12 + 0.01 # RESULT : makespan 332 SATISFIABLE SHOW_RESULT 332 BEGIN : [Mon Jun 19 23:13:55 2006] # ASSIGN : makespan 332 # ASSIGN : s_0_0 268 # ASSIGN : s_0_1 196 # ASSIGN : s_0_2 4 # ASSIGN : s_0_3 88 # ASSIGN : s_0_4 35 # ASSIGN : s_1_0 44 # ASSIGN : s_1_1 104 # ASSIGN : s_1_2 239 # ASSIGN : s_1_3 173 # ASSIGN : s_1_4 79 # ASSIGN : s_2_0 188 # ASSIGN : s_2_1 262 # ASSIGN : s_2_2 37 # ASSIGN : s_2_3 187 # ASSIGN : s_2_4 97 # ASSIGN : s_3_0 51 # ASSIGN : s_3_1 6 # ASSIGN : s_3_2 105 # ASSIGN : s_3_3 241 # ASSIGN : s_3_4 203 # ASSIGN : s_4_0 108 # ASSIGN : s_4_1 59 # ASSIGN : s_4_2 307 # ASSIGN : s_4_3 317 # ASSIGN : s_4_4 216 SHOW_RESULT 332 END : 332 (0 seconds) [Mon Jun 19 23:13:55 2006] SHOW_RESULT 332 CPU : 0.00999999999999979 = 0.00999999999999979 + 0 + 0 + 0 # BOUND : makespan 295 332 MODIFY_CNF 313 BEGIN : [Mon Jun 19 23:13:55 2006] MODIFY_CNF 313 END : 1802737 bytes (0 seconds) [Mon Jun 19 23:13:55 2006] MODIFY_CNF 313 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 313 BEGIN : [Mon Jun 19 23:13:55 2006] CMD : minisat /tmp/csp2sat13847.cnf /tmp/csp2sat13847.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 67518 191611 | 22506 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 11 (100 /sec) decisions : 64 (582 /sec) propagations : 23036 (209418 /sec) conflict literals : 124 (12.06 % deleted) Memory used : 5.94 MB CPU time : 0.11 s SATISFIABLE VERIFY_CNF 313 END : (0 seconds) [Mon Jun 19 23:13:55 2006] VERIFY_CNF 313 CPU : 0.14 = 0 + 0 + 0.12 + 0.02 # RESULT : makespan 313 SATISFIABLE SHOW_RESULT 313 BEGIN : [Mon Jun 19 23:13:55 2006] # ASSIGN : makespan 313 # ASSIGN : s_0_0 249 # ASSIGN : s_0_1 133 # ASSIGN : s_0_2 218 # ASSIGN : s_0_3 48 # ASSIGN : s_0_4 4 # ASSIGN : s_1_0 114 # ASSIGN : s_1_1 199 # ASSIGN : s_1_2 129 # ASSIGN : s_1_3 34 # ASSIGN : s_1_4 66 # ASSIGN : s_2_0 175 # ASSIGN : s_2_1 14 # ASSIGN : s_2_2 253 # ASSIGN : s_2_3 174 # ASSIGN : s_2_4 84 # ASSIGN : s_3_0 121 # ASSIGN : s_3_1 268 # ASSIGN : s_3_2 23 # ASSIGN : s_3_3 192 # ASSIGN : s_3_4 179 # ASSIGN : s_4_0 8 # ASSIGN : s_4_1 88 # ASSIGN : s_4_2 197 # ASSIGN : s_4_3 298 # ASSIGN : s_4_4 207 SHOW_RESULT 313 END : 313 (0 seconds) [Mon Jun 19 23:13:55 2006] SHOW_RESULT 313 CPU : 0.02 = 0.02 + 0 + 0 + 0 # BOUND : makespan 295 313 MODIFY_CNF 304 BEGIN : [Mon Jun 19 23:13:55 2006] MODIFY_CNF 304 END : 1802737 bytes (0 seconds) [Mon Jun 19 23:13:55 2006] MODIFY_CNF 304 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 304 BEGIN : [Mon Jun 19 23:13:55 2006] CMD : minisat /tmp/csp2sat13847.cnf /tmp/csp2sat13847.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 65718 186211 | 21906 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 25 (250 /sec) decisions : 83 (830 /sec) propagations : 36609 (366090 /sec) conflict literals : 233 (17.38 % deleted) Memory used : 5.94 MB CPU time : 0.1 s SATISFIABLE VERIFY_CNF 304 END : (1 seconds) [Mon Jun 19 23:13:56 2006] VERIFY_CNF 304 CPU : 0.14 = 0 + 0 + 0.11 + 0.03 # RESULT : makespan 304 SATISFIABLE SHOW_RESULT 304 BEGIN : [Mon Jun 19 23:13:56 2006] # ASSIGN : makespan 304 # ASSIGN : s_0_0 155 # ASSIGN : s_0_1 54 # ASSIGN : s_0_2 124 # ASSIGN : s_0_3 219 # ASSIGN : s_0_4 10 # ASSIGN : s_1_0 229 # ASSIGN : s_1_1 120 # ASSIGN : s_1_2 236 # ASSIGN : s_1_3 86 # ASSIGN : s_1_4 66 # ASSIGN : s_2_0 1 # ASSIGN : s_2_1 234 # ASSIGN : s_2_2 174 # ASSIGN : s_2_3 83 # ASSIGN : s_2_4 84 # ASSIGN : s_3_0 250 # ASSIGN : s_3_1 189 # ASSIGN : s_3_2 2 # ASSIGN : s_3_3 100 # ASSIGN : s_3_4 176 # ASSIGN : s_4_0 75 # ASSIGN : s_4_1 9 # ASSIGN : s_4_2 164 # ASSIGN : s_4_3 198 # ASSIGN : s_4_4 213 SHOW_RESULT 304 END : 304 (0 seconds) [Mon Jun 19 23:13:56 2006] SHOW_RESULT 304 CPU : 0.0100000000000002 = 0.0100000000000002 + 0 + 0 + 0 # BOUND : makespan 295 304 MODIFY_CNF 299 BEGIN : [Mon Jun 19 23:13:56 2006] MODIFY_CNF 299 END : 1802736 bytes (0 seconds) [Mon Jun 19 23:13:56 2006] MODIFY_CNF 299 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 299 BEGIN : [Mon Jun 19 23:13:56 2006] CMD : minisat /tmp/csp2sat13847.cnf /tmp/csp2sat13847.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 64718 183211 | 21572 0 0 nan | 0.000 % | | 101 | 64718 183211 | 23729 101 1003 9.9 | 44.552 % | | 252 | 64377 182191 | 26102 251 2600 10.4 | 44.916 % | ============================================================================== restarts : 3 conflicts : 446 (1088 /sec) decisions : 547 (1334 /sec) propagations : 534155 (1302817 /sec) conflict literals : 3717 (27.03 % deleted) Memory used : 5.91 MB CPU time : 0.41 s UNSATISFIABLE VERIFY_CNF 299 END : (0 seconds) [Mon Jun 19 23:13:56 2006] VERIFY_CNF 299 CPU : 0.42 = 0 + 0 + 0.41 + 0.01 # RESULT : makespan 299 UNSATISFIABLE # BOUND : makespan 300 304 MODIFY_CNF 302 BEGIN : [Mon Jun 19 23:13:56 2006] MODIFY_CNF 302 END : 1802736 bytes (0 seconds) [Mon Jun 19 23:13:56 2006] MODIFY_CNF 302 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 302 BEGIN : [Mon Jun 19 23:13:56 2006] CMD : minisat /tmp/csp2sat13847.cnf /tmp/csp2sat13847.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 65318 185011 | 21772 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 45 (346 /sec) decisions : 109 (838 /sec) propagations : 69221 (532469 /sec) conflict literals : 473 (25.16 % deleted) Memory used : 5.94 MB CPU time : 0.13 s SATISFIABLE VERIFY_CNF 302 END : (0 seconds) [Mon Jun 19 23:13:56 2006] VERIFY_CNF 302 CPU : 0.17 = 0 + 0 + 0.14 + 0.03 # RESULT : makespan 302 SATISFIABLE SHOW_RESULT 302 BEGIN : [Mon Jun 19 23:13:56 2006] # ASSIGN : makespan 302 # ASSIGN : s_0_0 238 # ASSIGN : s_0_1 46 # ASSIGN : s_0_2 203 # ASSIGN : s_0_3 118 # ASSIGN : s_0_4 2 # ASSIGN : s_1_0 71 # ASSIGN : s_1_1 112 # ASSIGN : s_1_2 234 # ASSIGN : s_1_3 212 # ASSIGN : s_1_4 50 # ASSIGN : s_2_0 158 # ASSIGN : s_2_1 232 # ASSIGN : s_2_2 2 # ASSIGN : s_2_3 62 # ASSIGN : s_2_4 68 # ASSIGN : s_3_0 16 # ASSIGN : s_3_1 181 # ASSIGN : s_3_2 70 # ASSIGN : s_3_3 226 # ASSIGN : s_3_4 168 # ASSIGN : s_4_0 78 # ASSIGN : s_4_1 1 # ASSIGN : s_4_2 193 # ASSIGN : s_4_3 63 # ASSIGN : s_4_4 211 SHOW_RESULT 302 END : 302 (0 seconds) [Mon Jun 19 23:13:56 2006] SHOW_RESULT 302 CPU : 0.02 = 0.02 + 0 + 0 + 0 # BOUND : makespan 300 302 MODIFY_CNF 301 BEGIN : [Mon Jun 19 23:13:56 2006] MODIFY_CNF 301 END : 1802736 bytes (0 seconds) [Mon Jun 19 23:13:56 2006] MODIFY_CNF 301 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 301 BEGIN : [Mon Jun 19 23:13:56 2006] CMD : minisat /tmp/csp2sat13847.cnf /tmp/csp2sat13847.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 65118 184411 | 21706 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 68 (378 /sec) decisions : 121 (672 /sec) propagations : 105521 (586228 /sec) conflict literals : 878 (25.40 % deleted) Memory used : 5.94 MB CPU time : 0.18 s SATISFIABLE VERIFY_CNF 301 END : (0 seconds) [Mon Jun 19 23:13:56 2006] VERIFY_CNF 301 CPU : 0.18 = 0 + 0 + 0.18 + 0 # RESULT : makespan 301 SATISFIABLE SHOW_RESULT 301 BEGIN : [Mon Jun 19 23:13:56 2006] # ASSIGN : makespan 301 # ASSIGN : s_0_0 237 # ASSIGN : s_0_1 45 # ASSIGN : s_0_2 202 # ASSIGN : s_0_3 117 # ASSIGN : s_0_4 1 # ASSIGN : s_1_0 70 # ASSIGN : s_1_1 111 # ASSIGN : s_1_2 233 # ASSIGN : s_1_3 211 # ASSIGN : s_1_4 49 # ASSIGN : s_2_0 157 # ASSIGN : s_2_1 231 # ASSIGN : s_2_2 6 # ASSIGN : s_2_3 66 # ASSIGN : s_2_4 67 # ASSIGN : s_3_0 15 # ASSIGN : s_3_1 180 # ASSIGN : s_3_2 69 # ASSIGN : s_3_3 225 # ASSIGN : s_3_4 167 # ASSIGN : s_4_0 77 # ASSIGN : s_4_1 0 # ASSIGN : s_4_2 192 # ASSIGN : s_4_3 51 # ASSIGN : s_4_4 210 SHOW_RESULT 301 END : 301 (0 seconds) [Mon Jun 19 23:13:56 2006] SHOW_RESULT 301 CPU : 0.00999999999999979 = 0.00999999999999979 + 0 + 0 + 0 # BOUND : makespan 300 301 MODIFY_CNF 300 BEGIN : [Mon Jun 19 23:13:56 2006] MODIFY_CNF 300 END : 1802736 bytes (0 seconds) [Mon Jun 19 23:13:56 2006] MODIFY_CNF 300 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 300 BEGIN : [Mon Jun 19 23:13:56 2006] CMD : minisat /tmp/csp2sat13847.cnf /tmp/csp2sat13847.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 64918 183811 | 21639 0 0 nan | 0.000 % | | 100 | 64918 183811 | 23802 100 1024 10.2 | 44.326 % | | 250 | 64919 183811 | 26183 249 2237 9.0 | 44.326 % | ============================================================================== restarts : 3 conflicts : 362 (1006 /sec) decisions : 539 (1497 /sec) propagations : 431423 (1198397 /sec) conflict literals : 2997 (29.13 % deleted) Memory used : 5.96 MB CPU time : 0.36 s SATISFIABLE VERIFY_CNF 300 END : (1 seconds) [Mon Jun 19 23:13:57 2006] VERIFY_CNF 300 CPU : 0.37 = 0 + 0 + 0.37 + 0 # RESULT : makespan 300 SATISFIABLE SHOW_RESULT 300 BEGIN : [Mon Jun 19 23:13:57 2006] # ASSIGN : makespan 300 # ASSIGN : s_0_0 169 # ASSIGN : s_0_1 234 # ASSIGN : s_0_2 9 # ASSIGN : s_0_3 40 # ASSIGN : s_0_4 125 # ASSIGN : s_1_0 293 # ASSIGN : s_1_1 48 # ASSIGN : s_1_2 172 # ASSIGN : s_1_3 255 # ASSIGN : s_1_4 269 # ASSIGN : s_2_0 90 # ASSIGN : s_2_1 164 # ASSIGN : s_2_2 240 # ASSIGN : s_2_3 239 # ASSIGN : s_2_4 0 # ASSIGN : s_3_0 233 # ASSIGN : s_3_1 3 # ASSIGN : s_3_2 59 # ASSIGN : s_3_3 157 # ASSIGN : s_3_4 287 # ASSIGN : s_4_0 10 # ASSIGN : s_4_1 117 # ASSIGN : s_4_2 162 # ASSIGN : s_4_3 285 # ASSIGN : s_4_4 178 SHOW_RESULT 300 END : 300 (0 seconds) [Mon Jun 19 23:13:57 2006] SHOW_RESULT 300 CPU : 0.0100000000000002 = 0.0100000000000002 + 0 + 0 + 0 # BOUND : makespan 300 300 MAIN END : (6 seconds) [Mon Jun 19 23:13:57 2006] MAIN CPU : 5.53 = 3.84 + 0.01 + 1.58 + 0.1