# TIMEOUT 18000 MAIN BEGIN : [Mon Jun 19 23:14:43 2006] READ BEGIN : csp/tai_5x5_9.csp [Mon Jun 19 23:14:43 2006] READ END : csp/tai_5x5_9.csp (1 seconds) [Mon Jun 19 23:14:44 2006] READ CPU : 0.23 = 0.23 + 0 + 0 + 0 # BOUND : makespan 349 462 GENERATE_CNF 462 BEGIN : [Mon Jun 19 23:14:44 2006] GENERATE_CNF 462 END : 11940 variables 94884 clauses 1820831 bytes (3 seconds) [Mon Jun 19 23:14:47 2006] GENERATE_CNF 462 CPU : 3.48 = 3.47 + 0.01 + 0 + 0 MODIFY_CNF 405 BEGIN : [Mon Jun 19 23:14:47 2006] MODIFY_CNF 405 END : 1820836 bytes (0 seconds) [Mon Jun 19 23:14:47 2006] MODIFY_CNF 405 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 405 BEGIN : [Mon Jun 19 23:14:47 2006] CMD : minisat /tmp/csp2sat13923.cnf /tmp/csp2sat13923.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 83104 237955 | 27701 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 6 (50 /sec) decisions : 51 (425 /sec) propagations : 19252 (160433 /sec) conflict literals : 57 (1.72 % deleted) Memory used : 5.95 MB CPU time : 0.12 s SATISFIABLE VERIFY_CNF 405 END : (0 seconds) [Mon Jun 19 23:14:47 2006] VERIFY_CNF 405 CPU : 0.13 = 0 + 0 + 0.13 + 0 # RESULT : makespan 405 SATISFIABLE SHOW_RESULT 405 BEGIN : [Mon Jun 19 23:14:47 2006] # ASSIGN : makespan 405 # ASSIGN : s_0_0 266 # ASSIGN : s_0_1 142 # ASSIGN : s_0_2 288 # ASSIGN : s_0_3 2 # ASSIGN : s_0_4 52 # ASSIGN : s_1_0 332 # ASSIGN : s_1_1 239 # ASSIGN : s_1_2 63 # ASSIGN : s_1_3 40 # ASSIGN : s_1_4 147 # ASSIGN : s_2_0 6 # ASSIGN : s_2_1 177 # ASSIGN : s_2_2 371 # ASSIGN : s_2_3 83 # ASSIGN : s_2_4 215 # ASSIGN : s_3_0 93 # ASSIGN : s_3_1 333 # ASSIGN : s_3_2 8 # ASSIGN : s_3_3 189 # ASSIGN : s_3_4 256 # ASSIGN : s_4_0 250 # ASSIGN : s_4_1 49 # ASSIGN : s_4_2 161 # ASSIGN : s_4_3 266 # ASSIGN : s_4_4 315 SHOW_RESULT 405 END : 405 (0 seconds) [Mon Jun 19 23:14:47 2006] SHOW_RESULT 405 CPU : 0.02 = 0.02 + 0 + 0 + 0 # BOUND : makespan 349 405 MODIFY_CNF 377 BEGIN : [Mon Jun 19 23:14:47 2006] MODIFY_CNF 377 END : 1820836 bytes (0 seconds) [Mon Jun 19 23:14:47 2006] MODIFY_CNF 377 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 377 BEGIN : [Mon Jun 19 23:14:47 2006] CMD : minisat /tmp/csp2sat13923.cnf /tmp/csp2sat13923.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 77504 221155 | 25834 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 8 (67 /sec) decisions : 49 (408 /sec) propagations : 19989 (166575 /sec) conflict literals : 73 (6.41 % deleted) Memory used : 5.98 MB CPU time : 0.12 s SATISFIABLE VERIFY_CNF 377 END : (0 seconds) [Mon Jun 19 23:14:47 2006] VERIFY_CNF 377 CPU : 0.13 = 0 + 0 + 0.12 + 0.01 # RESULT : makespan 377 SATISFIABLE SHOW_RESULT 377 BEGIN : [Mon Jun 19 23:14:47 2006] # ASSIGN : makespan 377 # ASSIGN : s_0_0 165 # ASSIGN : s_0_1 270 # ASSIGN : s_0_2 187 # ASSIGN : s_0_3 123 # ASSIGN : s_0_4 29 # ASSIGN : s_1_0 220 # ASSIGN : s_1_1 26 # ASSIGN : s_1_2 293 # ASSIGN : s_1_3 3 # ASSIGN : s_1_4 119 # ASSIGN : s_2_0 300 # ASSIGN : s_2_1 232 # ASSIGN : s_2_2 153 # ASSIGN : s_2_3 29 # ASSIGN : s_2_4 187 # ASSIGN : s_3_0 2 # ASSIGN : s_3_1 305 # ASSIGN : s_3_2 98 # ASSIGN : s_3_3 161 # ASSIGN : s_3_4 228 # ASSIGN : s_4_0 123 # ASSIGN : s_4_1 139 # ASSIGN : s_4_2 9 # ASSIGN : s_4_3 238 # ASSIGN : s_4_4 287 SHOW_RESULT 377 END : 377 (0 seconds) [Mon Jun 19 23:14:47 2006] SHOW_RESULT 377 CPU : 0.00999999999999979 = 0.00999999999999979 + 0 + 0 + 0 # BOUND : makespan 349 377 MODIFY_CNF 363 BEGIN : [Mon Jun 19 23:14:47 2006] MODIFY_CNF 363 END : 1820836 bytes (0 seconds) [Mon Jun 19 23:14:47 2006] MODIFY_CNF 363 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 363 BEGIN : [Mon Jun 19 23:14:47 2006] CMD : minisat /tmp/csp2sat13923.cnf /tmp/csp2sat13923.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 74704 212755 | 24901 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 10 (83 /sec) decisions : 52 (433 /sec) propagations : 22072 (183933 /sec) conflict literals : 90 (4.26 % deleted) Memory used : 6.02 MB CPU time : 0.12 s SATISFIABLE VERIFY_CNF 363 END : (0 seconds) [Mon Jun 19 23:14:47 2006] VERIFY_CNF 363 CPU : 0.15 = 0.0100000000000002 + 0 + 0.13 + 0.01 # RESULT : makespan 363 SATISFIABLE SHOW_RESULT 363 BEGIN : [Mon Jun 19 23:14:47 2006] # ASSIGN : makespan 363 # ASSIGN : s_0_0 245 # ASSIGN : s_0_1 101 # ASSIGN : s_0_2 280 # ASSIGN : s_0_3 182 # ASSIGN : s_0_4 1 # ASSIGN : s_1_0 17 # ASSIGN : s_1_1 270 # ASSIGN : s_1_2 186 # ASSIGN : s_1_3 159 # ASSIGN : s_1_4 91 # ASSIGN : s_2_0 90 # ASSIGN : s_2_1 231 # ASSIGN : s_2_2 56 # ASSIGN : s_2_3 269 # ASSIGN : s_2_4 167 # ASSIGN : s_3_0 267 # ASSIGN : s_3_1 136 # ASSIGN : s_3_2 1 # ASSIGN : s_3_3 69 # ASSIGN : s_3_4 208 # ASSIGN : s_4_0 204 # ASSIGN : s_4_1 4 # ASSIGN : s_4_2 97 # ASSIGN : s_4_3 220 # ASSIGN : s_4_4 273 SHOW_RESULT 363 END : 363 (1 seconds) [Mon Jun 19 23:14:48 2006] SHOW_RESULT 363 CPU : 0.02 = 0.02 + 0 + 0 + 0 # BOUND : makespan 349 363 MODIFY_CNF 356 BEGIN : [Mon Jun 19 23:14:48 2006] MODIFY_CNF 356 END : 1820835 bytes (0 seconds) [Mon Jun 19 23:14:48 2006] MODIFY_CNF 356 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 356 BEGIN : [Mon Jun 19 23:14:48 2006] CMD : minisat /tmp/csp2sat13923.cnf /tmp/csp2sat13923.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 73304 208555 | 24434 0 0 nan | 0.000 % | | 100 | 73304 208555 | 26877 100 797 8.0 | 36.952 % | ============================================================================== restarts : 2 conflicts : 174 (725 /sec) decisions : 268 (1117 /sec) propagations : 252970 (1054042 /sec) conflict literals : 1417 (26.66 % deleted) Memory used : 6.04 MB CPU time : 0.24 s SATISFIABLE VERIFY_CNF 356 END : (0 seconds) [Mon Jun 19 23:14:48 2006] VERIFY_CNF 356 CPU : 0.28 = 0 + 0 + 0.25 + 0.03 # RESULT : makespan 356 SATISFIABLE SHOW_RESULT 356 BEGIN : [Mon Jun 19 23:14:48 2006] # ASSIGN : makespan 356 # ASSIGN : s_0_0 113 # ASSIGN : s_0_1 135 # ASSIGN : s_0_2 183 # ASSIGN : s_0_3 67 # ASSIGN : s_0_4 266 # ASSIGN : s_1_0 26 # ASSIGN : s_1_1 263 # ASSIGN : s_1_2 99 # ASSIGN : s_1_3 3 # ASSIGN : s_1_4 195 # ASSIGN : s_2_0 183 # ASSIGN : s_2_1 21 # ASSIGN : s_2_2 59 # ASSIGN : s_2_3 262 # ASSIGN : s_2_4 93 # ASSIGN : s_3_0 260 # ASSIGN : s_3_1 62 # ASSIGN : s_3_2 4 # ASSIGN : s_3_3 193 # ASSIGN : s_3_4 134 # ASSIGN : s_4_0 154 # ASSIGN : s_4_1 170 # ASSIGN : s_4_2 267 # ASSIGN : s_4_3 105 # ASSIGN : s_4_4 3 SHOW_RESULT 356 END : 356 (0 seconds) [Mon Jun 19 23:14:48 2006] SHOW_RESULT 356 CPU : 0.02 = 0.02 + 0 + 0 + 0 # BOUND : makespan 349 356 MODIFY_CNF 352 BEGIN : [Mon Jun 19 23:14:48 2006] MODIFY_CNF 352 END : 1820835 bytes (0 seconds) [Mon Jun 19 23:14:48 2006] MODIFY_CNF 352 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 352 BEGIN : [Mon Jun 19 23:14:48 2006] CMD : minisat /tmp/csp2sat13923.cnf /tmp/csp2sat13923.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 72504 206155 | 24168 0 0 nan | 0.000 % | | 100 | 72506 206155 | 26584 98 700 7.1 | 37.823 % | | 250 | 72507 206155 | 29243 247 1862 7.5 | 37.823 % | ============================================================================== restarts : 3 conflicts : 458 (916 /sec) decisions : 584 (1168 /sec) propagations : 651303 (1302606 /sec) conflict literals : 3204 (33.03 % deleted) Memory used : 5.99 MB CPU time : 0.5 s UNSATISFIABLE VERIFY_CNF 352 END : (0 seconds) [Mon Jun 19 23:14:48 2006] VERIFY_CNF 352 CPU : 0.52 = 0 + 0 + 0.5 + 0.02 # RESULT : makespan 352 UNSATISFIABLE # BOUND : makespan 353 356 MODIFY_CNF 354 BEGIN : [Mon Jun 19 23:14:48 2006] MODIFY_CNF 354 END : 1820835 bytes (0 seconds) [Mon Jun 19 23:14:48 2006] MODIFY_CNF 354 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 354 BEGIN : [Mon Jun 19 23:14:48 2006] CMD : minisat /tmp/csp2sat13923.cnf /tmp/csp2sat13923.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 72904 207355 | 24301 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 79 (465 /sec) decisions : 134 (788 /sec) propagations : 113375 (666912 /sec) conflict literals : 588 (27.94 % deleted) Memory used : 6.02 MB CPU time : 0.17 s SATISFIABLE VERIFY_CNF 354 END : (1 seconds) [Mon Jun 19 23:14:49 2006] VERIFY_CNF 354 CPU : 0.19 = 0 + 0 + 0.18 + 0.01 # RESULT : makespan 354 SATISFIABLE SHOW_RESULT 354 BEGIN : [Mon Jun 19 23:14:49 2006] # ASSIGN : makespan 354 # ASSIGN : s_0_0 259 # ASSIGN : s_0_1 281 # ASSIGN : s_0_2 8 # ASSIGN : s_0_3 316 # ASSIGN : s_0_4 133 # ASSIGN : s_1_0 281 # ASSIGN : s_1_1 188 # ASSIGN : s_1_2 91 # ASSIGN : s_1_3 68 # ASSIGN : s_1_4 0 # ASSIGN : s_2_0 52 # ASSIGN : s_2_1 316 # ASSIGN : s_2_2 265 # ASSIGN : s_2_3 129 # ASSIGN : s_2_4 223 # ASSIGN : s_3_0 136 # ASSIGN : s_3_1 2 # ASSIGN : s_3_2 299 # ASSIGN : s_3_3 232 # ASSIGN : s_3_4 74 # ASSIGN : s_4_0 3 # ASSIGN : s_4_1 82 # ASSIGN : s_4_2 175 # ASSIGN : s_4_3 19 # ASSIGN : s_4_4 264 SHOW_RESULT 354 END : 354 (0 seconds) [Mon Jun 19 23:14:49 2006] SHOW_RESULT 354 CPU : 0.00999999999999979 = 0.00999999999999979 + 0 + 0 + 0 # BOUND : makespan 353 354 MODIFY_CNF 353 BEGIN : [Mon Jun 19 23:14:49 2006] MODIFY_CNF 353 END : 1820835 bytes (0 seconds) [Mon Jun 19 23:14:49 2006] MODIFY_CNF 353 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 353 BEGIN : [Mon Jun 19 23:14:49 2006] CMD : minisat /tmp/csp2sat13923.cnf /tmp/csp2sat13923.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 72704 206755 | 24234 0 0 nan | 0.000 % | | 100 | 72706 206755 | 26657 98 586 6.0 | 37.605 % | ============================================================================== restarts : 2 conflicts : 195 (696 /sec) decisions : 300 (1071 /sec) propagations : 289112 (1032543 /sec) conflict literals : 1288 (30.27 % deleted) Memory used : 6.04 MB CPU time : 0.28 s SATISFIABLE VERIFY_CNF 353 END : (0 seconds) [Mon Jun 19 23:14:49 2006] VERIFY_CNF 353 CPU : 0.29 = 0 + 0 + 0.28 + 0.01 # RESULT : makespan 353 SATISFIABLE SHOW_RESULT 353 BEGIN : [Mon Jun 19 23:14:49 2006] # ASSIGN : makespan 353 # ASSIGN : s_0_0 225 # ASSIGN : s_0_1 190 # ASSIGN : s_0_2 90 # ASSIGN : s_0_3 315 # ASSIGN : s_0_4 0 # ASSIGN : s_1_0 280 # ASSIGN : s_1_1 2 # ASSIGN : s_1_2 173 # ASSIGN : s_1_3 257 # ASSIGN : s_1_4 95 # ASSIGN : s_2_0 145 # ASSIGN : s_2_1 315 # ASSIGN : s_2_2 264 # ASSIGN : s_2_3 2 # ASSIGN : s_2_4 222 # ASSIGN : s_3_0 0 # ASSIGN : s_3_1 226 # ASSIGN : s_3_2 298 # ASSIGN : s_3_3 96 # ASSIGN : s_3_4 163 # ASSIGN : s_4_0 247 # ASSIGN : s_4_1 97 # ASSIGN : s_4_2 1 # ASSIGN : s_4_3 198 # ASSIGN : s_4_4 263 SHOW_RESULT 353 END : 353 (0 seconds) [Mon Jun 19 23:14:49 2006] SHOW_RESULT 353 CPU : 0.02 = 0.02 + 0 + 0 + 0 # BOUND : makespan 353 353 MAIN END : (6 seconds) [Mon Jun 19 23:14:49 2006] MAIN CPU : 5.5 = 3.81 + 0.01 + 1.59 + 0.09