# TIMEOUT 18000 MAIN BEGIN : [Mon Jun 19 23:14:20 2006] READ BEGIN : csp/tai_5x5_5.csp [Mon Jun 19 23:14:20 2006] READ END : csp/tai_5x5_5.csp (0 seconds) [Mon Jun 19 23:14:20 2006] READ CPU : 0.23 = 0.23 + 0 + 0 + 0 # BOUND : makespan 321 400 GENERATE_CNF 400 BEGIN : [Mon Jun 19 23:14:20 2006] GENERATE_CNF 400 END : 10356 variables 80906 clauses 1528755 bytes (3 seconds) [Mon Jun 19 23:14:23 2006] GENERATE_CNF 400 CPU : 2.97 = 2.96 + 0.01 + 0 + 0 MODIFY_CNF 360 BEGIN : [Mon Jun 19 23:14:23 2006] MODIFY_CNF 360 END : 1528760 bytes (0 seconds) [Mon Jun 19 23:14:23 2006] MODIFY_CNF 360 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 360 BEGIN : [Mon Jun 19 23:14:23 2006] CMD : minisat /tmp/csp2sat13890.cnf /tmp/csp2sat13890.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 72526 207805 | 24175 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 1 (11 /sec) decisions : 42 (467 /sec) propagations : 12703 (141144 /sec) conflict literals : 19 (0.00 % deleted) Memory used : 5.36 MB CPU time : 0.09 s SATISFIABLE VERIFY_CNF 360 END : (0 seconds) [Mon Jun 19 23:14:23 2006] VERIFY_CNF 360 CPU : 0.11 = 0 + 0 + 0.09 + 0.02 # RESULT : makespan 360 SATISFIABLE SHOW_RESULT 360 BEGIN : [Mon Jun 19 23:14:23 2006] # ASSIGN : makespan 360 # ASSIGN : s_0_0 141 # ASSIGN : s_0_1 308 # ASSIGN : s_0_2 202 # ASSIGN : s_0_3 1 # ASSIGN : s_0_4 62 # ASSIGN : s_1_0 227 # ASSIGN : s_1_1 260 # ASSIGN : s_1_2 15 # ASSIGN : s_1_3 61 # ASSIGN : s_1_4 135 # ASSIGN : s_2_0 27 # ASSIGN : s_2_1 176 # ASSIGN : s_2_2 280 # ASSIGN : s_2_3 113 # ASSIGN : s_2_4 235 # ASSIGN : s_3_0 268 # ASSIGN : s_3_1 91 # ASSIGN : s_3_2 86 # ASSIGN : s_3_3 177 # ASSIGN : s_3_4 266 # ASSIGN : s_4_0 199 # ASSIGN : s_4_1 16 # ASSIGN : s_4_2 108 # ASSIGN : s_4_3 233 # ASSIGN : s_4_4 282 SHOW_RESULT 360 END : 360 (1 seconds) [Mon Jun 19 23:14:24 2006] SHOW_RESULT 360 CPU : 0.02 = 0.02 + 0 + 0 + 0 # BOUND : makespan 321 360 MODIFY_CNF 340 BEGIN : [Mon Jun 19 23:14:24 2006] MODIFY_CNF 340 END : 1528760 bytes (0 seconds) [Mon Jun 19 23:14:24 2006] MODIFY_CNF 340 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 340 BEGIN : [Mon Jun 19 23:14:24 2006] CMD : minisat /tmp/csp2sat13890.cnf /tmp/csp2sat13890.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 68526 195805 | 22842 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 8 (80 /sec) decisions : 73 (730 /sec) propagations : 16645 (166450 /sec) conflict literals : 101 (8.18 % deleted) Memory used : 5.38 MB CPU time : 0.1 s SATISFIABLE VERIFY_CNF 340 END : (0 seconds) [Mon Jun 19 23:14:24 2006] VERIFY_CNF 340 CPU : 0.11 = 0 + 0 + 0.1 + 0.01 # RESULT : makespan 340 SATISFIABLE SHOW_RESULT 340 BEGIN : [Mon Jun 19 23:14:24 2006] # ASSIGN : makespan 340 # ASSIGN : s_0_0 282 # ASSIGN : s_0_1 229 # ASSIGN : s_0_2 91 # ASSIGN : s_0_3 169 # ASSIGN : s_0_4 5 # ASSIGN : s_1_0 249 # ASSIGN : s_1_1 181 # ASSIGN : s_1_2 289 # ASSIGN : s_1_3 26 # ASSIGN : s_1_4 78 # ASSIGN : s_2_0 7 # ASSIGN : s_2_1 281 # ASSIGN : s_2_2 201 # ASSIGN : s_2_3 106 # ASSIGN : s_2_4 170 # ASSIGN : s_3_0 93 # ASSIGN : s_3_1 8 # ASSIGN : s_3_2 335 # ASSIGN : s_3_3 235 # ASSIGN : s_3_4 211 # ASSIGN : s_4_0 185 # ASSIGN : s_4_1 106 # ASSIGN : s_4_2 0 # ASSIGN : s_4_3 291 # ASSIGN : s_4_4 213 SHOW_RESULT 340 END : 340 (0 seconds) [Mon Jun 19 23:14:24 2006] SHOW_RESULT 340 CPU : 0.0100000000000002 = 0.0100000000000002 + 0 + 0 + 0 # BOUND : makespan 321 340 MODIFY_CNF 330 BEGIN : [Mon Jun 19 23:14:24 2006] MODIFY_CNF 330 END : 1528760 bytes (0 seconds) [Mon Jun 19 23:14:24 2006] MODIFY_CNF 330 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 330 BEGIN : [Mon Jun 19 23:14:24 2006] CMD : minisat /tmp/csp2sat13890.cnf /tmp/csp2sat13890.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 66526 189805 | 22175 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 69 (383 /sec) decisions : 123 (683 /sec) propagations : 119340 (663000 /sec) conflict literals : 993 (26.99 % deleted) Memory used : 5.38 MB CPU time : 0.18 s SATISFIABLE VERIFY_CNF 330 END : (0 seconds) [Mon Jun 19 23:14:24 2006] VERIFY_CNF 330 CPU : 0.18 = 0 + 0 + 0.18 + 0 # RESULT : makespan 330 SATISFIABLE SHOW_RESULT 330 BEGIN : [Mon Jun 19 23:14:24 2006] # ASSIGN : makespan 330 # ASSIGN : s_0_0 272 # ASSIGN : s_0_1 220 # ASSIGN : s_0_2 142 # ASSIGN : s_0_3 82 # ASSIGN : s_0_4 9 # ASSIGN : s_1_0 94 # ASSIGN : s_1_1 282 # ASSIGN : s_1_2 5 # ASSIGN : s_1_3 222 # ASSIGN : s_1_4 127 # ASSIGN : s_2_0 0 # ASSIGN : s_2_1 86 # ASSIGN : s_2_2 250 # ASSIGN : s_2_3 156 # ASSIGN : s_2_4 219 # ASSIGN : s_3_0 132 # ASSIGN : s_3_1 1 # ASSIGN : s_3_2 245 # ASSIGN : s_3_3 274 # ASSIGN : s_3_4 250 # ASSIGN : s_4_0 224 # ASSIGN : s_4_1 145 # ASSIGN : s_4_2 51 # ASSIGN : s_4_3 2 # ASSIGN : s_4_4 252 SHOW_RESULT 330 END : 330 (0 seconds) [Mon Jun 19 23:14:24 2006] SHOW_RESULT 330 CPU : 0.00999999999999979 = 0.00999999999999979 + 0 + 0 + 0 # BOUND : makespan 321 330 MODIFY_CNF 325 BEGIN : [Mon Jun 19 23:14:24 2006] MODIFY_CNF 325 END : 1528759 bytes (0 seconds) [Mon Jun 19 23:14:24 2006] MODIFY_CNF 325 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 325 BEGIN : [Mon Jun 19 23:14:24 2006] CMD : minisat /tmp/csp2sat13890.cnf /tmp/csp2sat13890.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 65526 186805 | 21842 0 0 nan | 0.000 % | | 100 | 65526 186805 | 24026 100 1126 11.3 | 33.787 % | | 253 | 65526 186805 | 26428 253 2360 9.3 | 33.787 % | | 479 | 65528 186805 | 29071 477 4791 10.0 | 33.787 % | | 816 | 63507 180796 | 31978 585 5537 9.5 | 36.868 % | ============================================================================== restarts : 5 conflicts : 930 (949 /sec) decisions : 1133 (1156 /sec) propagations : 1329554 (1356688 /sec) conflict literals : 8167 (32.13 % deleted) Memory used : 5.36 MB CPU time : 0.98 s UNSATISFIABLE VERIFY_CNF 325 END : (1 seconds) [Mon Jun 19 23:14:25 2006] VERIFY_CNF 325 CPU : 1 = 0 + 0 + 0.98 + 0.02 # RESULT : makespan 325 UNSATISFIABLE # BOUND : makespan 326 330 MODIFY_CNF 328 BEGIN : [Mon Jun 19 23:14:25 2006] MODIFY_CNF 328 END : 1528759 bytes (0 seconds) [Mon Jun 19 23:14:25 2006] MODIFY_CNF 328 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 328 BEGIN : [Mon Jun 19 23:14:25 2006] CMD : minisat /tmp/csp2sat13890.cnf /tmp/csp2sat13890.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 66126 188605 | 22042 0 0 nan | 0.000 % | | 100 | 66126 188605 | 24246 100 1217 12.2 | 33.034 % | | 251 | 66126 188605 | 26670 251 2596 10.3 | 33.034 % | | 476 | 66126 188605 | 29337 476 4756 10.0 | 33.034 % | ============================================================================== restarts : 4 conflicts : 572 (908 /sec) decisions : 788 (1251 /sec) propagations : 876479 (1391237 /sec) conflict literals : 5630 (32.36 % deleted) Memory used : 5.39 MB CPU time : 0.63 s SATISFIABLE VERIFY_CNF 328 END : (1 seconds) [Mon Jun 19 23:14:26 2006] VERIFY_CNF 328 CPU : 0.65 = 0 + 0 + 0.63 + 0.02 # RESULT : makespan 328 SATISFIABLE SHOW_RESULT 328 BEGIN : [Mon Jun 19 23:14:26 2006] # ASSIGN : makespan 328 # ASSIGN : s_0_0 55 # ASSIGN : s_0_1 3 # ASSIGN : s_0_2 113 # ASSIGN : s_0_3 195 # ASSIGN : s_0_4 255 # ASSIGN : s_1_0 6 # ASSIGN : s_1_1 135 # ASSIGN : s_1_2 191 # ASSIGN : s_1_3 276 # ASSIGN : s_1_4 39 # ASSIGN : s_2_0 242 # ASSIGN : s_2_1 183 # ASSIGN : s_2_2 33 # ASSIGN : s_2_3 120 # ASSIGN : s_2_4 2 # ASSIGN : s_3_0 117 # ASSIGN : s_3_1 243 # ASSIGN : s_3_2 28 # ASSIGN : s_3_3 61 # ASSIGN : s_3_4 0 # ASSIGN : s_4_0 209 # ASSIGN : s_4_1 56 # ASSIGN : s_4_2 237 # ASSIGN : s_4_3 7 # ASSIGN : s_4_4 131 SHOW_RESULT 328 END : 328 (0 seconds) [Mon Jun 19 23:14:26 2006] SHOW_RESULT 328 CPU : 0.00999999999999979 = 0.00999999999999979 + 0 + 0 + 0 # BOUND : makespan 326 328 MODIFY_CNF 327 BEGIN : [Mon Jun 19 23:14:26 2006] MODIFY_CNF 327 END : 1528759 bytes (0 seconds) [Mon Jun 19 23:14:26 2006] MODIFY_CNF 327 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 327 BEGIN : [Mon Jun 19 23:14:26 2006] CMD : minisat /tmp/csp2sat13890.cnf /tmp/csp2sat13890.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 65926 188005 | 21975 0 0 nan | 0.000 % | | 101 | 65926 188005 | 24172 101 1316 13.0 | 33.285 % | ============================================================================== restarts : 2 conflicts : 140 (636 /sec) decisions : 225 (1023 /sec) propagations : 211185 (959932 /sec) conflict literals : 1664 (27.72 % deleted) Memory used : 5.41 MB CPU time : 0.22 s SATISFIABLE VERIFY_CNF 327 END : (0 seconds) [Mon Jun 19 23:14:26 2006] VERIFY_CNF 327 CPU : 0.24 = 0 + 0 + 0.23 + 0.01 # RESULT : makespan 327 SATISFIABLE SHOW_RESULT 327 BEGIN : [Mon Jun 19 23:14:26 2006] # ASSIGN : makespan 327 # ASSIGN : s_0_0 54 # ASSIGN : s_0_1 2 # ASSIGN : s_0_2 112 # ASSIGN : s_0_3 192 # ASSIGN : s_0_4 252 # ASSIGN : s_1_0 5 # ASSIGN : s_1_1 133 # ASSIGN : s_1_2 190 # ASSIGN : s_1_3 275 # ASSIGN : s_1_4 38 # ASSIGN : s_2_0 241 # ASSIGN : s_2_1 181 # ASSIGN : s_2_2 32 # ASSIGN : s_2_3 118 # ASSIGN : s_2_4 1 # ASSIGN : s_3_0 116 # ASSIGN : s_3_1 240 # ASSIGN : s_3_2 27 # ASSIGN : s_3_3 60 # ASSIGN : s_3_4 325 # ASSIGN : s_4_0 208 # ASSIGN : s_4_1 55 # ASSIGN : s_4_2 236 # ASSIGN : s_4_3 6 # ASSIGN : s_4_4 130 SHOW_RESULT 327 END : 327 (0 seconds) [Mon Jun 19 23:14:26 2006] SHOW_RESULT 327 CPU : 0.02 = 0.02 + 0 + 0 + 0 # BOUND : makespan 326 327 MODIFY_CNF 326 BEGIN : [Mon Jun 19 23:14:26 2006] MODIFY_CNF 326 END : 1528759 bytes (0 seconds) [Mon Jun 19 23:14:26 2006] MODIFY_CNF 326 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 326 BEGIN : [Mon Jun 19 23:14:26 2006] CMD : minisat /tmp/csp2sat13890.cnf /tmp/csp2sat13890.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 65726 187405 | 21908 0 0 nan | 0.000 % | | 101 | 65726 187405 | 24098 101 1388 13.7 | 33.536 % | ============================================================================== restarts : 2 conflicts : 232 (859 /sec) decisions : 343 (1270 /sec) propagations : 310966 (1151726 /sec) conflict literals : 2417 (30.49 % deleted) Memory used : 5.40 MB CPU time : 0.27 s SATISFIABLE VERIFY_CNF 326 END : (0 seconds) [Mon Jun 19 23:14:26 2006] VERIFY_CNF 326 CPU : 0.3 = 0 + 0 + 0.28 + 0.02 # RESULT : makespan 326 SATISFIABLE SHOW_RESULT 326 BEGIN : [Mon Jun 19 23:14:26 2006] # ASSIGN : makespan 326 # ASSIGN : s_0_0 53 # ASSIGN : s_0_1 1 # ASSIGN : s_0_2 111 # ASSIGN : s_0_3 193 # ASSIGN : s_0_4 253 # ASSIGN : s_1_0 4 # ASSIGN : s_1_1 133 # ASSIGN : s_1_2 189 # ASSIGN : s_1_3 274 # ASSIGN : s_1_4 37 # ASSIGN : s_2_0 240 # ASSIGN : s_2_1 181 # ASSIGN : s_2_2 31 # ASSIGN : s_2_3 118 # ASSIGN : s_2_4 0 # ASSIGN : s_3_0 115 # ASSIGN : s_3_1 241 # ASSIGN : s_3_2 26 # ASSIGN : s_3_3 59 # ASSIGN : s_3_4 239 # ASSIGN : s_4_0 207 # ASSIGN : s_4_1 54 # ASSIGN : s_4_2 235 # ASSIGN : s_4_3 5 # ASSIGN : s_4_4 129 SHOW_RESULT 326 END : 326 (0 seconds) [Mon Jun 19 23:14:26 2006] SHOW_RESULT 326 CPU : 0.02 = 0.02 + 0 + 0 + 0 # BOUND : makespan 326 326 MAIN END : (6 seconds) [Mon Jun 19 23:14:26 2006] MAIN CPU : 5.88 = 3.28 + 0.01 + 2.49 + 0.1