# TIMEOUT 18000 MAIN BEGIN : [Mon Jun 19 23:15:56 2006] READ BEGIN : csp/tai_7x7_3.csp [Mon Jun 19 23:15:56 2006] READ END : csp/tai_7x7_3.csp (0 seconds) [Mon Jun 19 23:15:56 2006] READ CPU : 0.65 = 0.65 + 0 + 0 + 0 # BOUND : makespan 468 628 GENERATE_CNF 628 BEGIN : [Mon Jun 19 23:15:56 2006] GENERATE_CNF 628 END : 31669 variables 374258 clauses 7736436 bytes (14 seconds) [Mon Jun 19 23:16:10 2006] GENERATE_CNF 628 CPU : 14.06 = 14.01 + 0.05 + 0 + 0 MODIFY_CNF 548 BEGIN : [Mon Jun 19 23:16:10 2006] MODIFY_CNF 548 END : 7736441 bytes (0 seconds) [Mon Jun 19 23:16:10 2006] MODIFY_CNF 548 CPU : 0.00999999999999979 = 0.00999999999999979 + 0 + 0 + 0 VERIFY_CNF 548 BEGIN : [Mon Jun 19 23:16:10 2006] CMD : minisat /tmp/csp2sat13988.cnf /tmp/csp2sat13988.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 326282 948606 | 108760 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 8 (17 /sec) decisions : 130 (271 /sec) propagations : 52434 (109238 /sec) conflict literals : 223 (6.69 % deleted) Memory used : 18.22 MB CPU time : 0.48 s SATISFIABLE VERIFY_CNF 548 END : (1 seconds) [Mon Jun 19 23:16:11 2006] VERIFY_CNF 548 CPU : 0.53 = 0 + 0 + 0.5 + 0.03 # RESULT : makespan 548 SATISFIABLE SHOW_RESULT 548 BEGIN : [Mon Jun 19 23:16:11 2006] # ASSIGN : makespan 548 # ASSIGN : s_0_0 390 # ASSIGN : s_0_1 201 # ASSIGN : s_0_2 296 # ASSIGN : s_0_3 128 # ASSIGN : s_0_4 466 # ASSIGN : s_0_5 50 # ASSIGN : s_0_6 23 # ASSIGN : s_1_0 246 # ASSIGN : s_1_1 330 # ASSIGN : s_1_2 389 # ASSIGN : s_1_3 480 # ASSIGN : s_1_4 183 # ASSIGN : s_1_5 131 # ASSIGN : s_1_6 28 # ASSIGN : s_2_0 477 # ASSIGN : s_2_1 380 # ASSIGN : s_2_2 73 # ASSIGN : s_2_3 157 # ASSIGN : s_2_4 23 # ASSIGN : s_2_5 243 # ASSIGN : s_2_6 90 # ASSIGN : s_3_0 27 # ASSIGN : s_3_1 486 # ASSIGN : s_3_2 224 # ASSIGN : s_3_3 0 # ASSIGN : s_3_4 73 # ASSIGN : s_3_5 301 # ASSIGN : s_3_6 167 # ASSIGN : s_4_0 350 # ASSIGN : s_4_1 107 # ASSIGN : s_4_2 469 # ASSIGN : s_4_3 22 # ASSIGN : s_4_4 227 # ASSIGN : s_4_5 399 # ASSIGN : s_4_6 242 # ASSIGN : s_5_0 181 # ASSIGN : s_5_1 57 # ASSIGN : s_5_2 10 # ASSIGN : s_5_3 102 # ASSIGN : s_5_4 276 # ASSIGN : s_5_5 426 # ASSIGN : s_5_6 329 # ASSIGN : s_6_0 227 # ASSIGN : s_6_1 32 # ASSIGN : s_6_2 155 # ASSIGN : s_6_3 271 # ASSIGN : s_6_4 320 # ASSIGN : s_6_5 495 # ASSIGN : s_6_6 403 SHOW_RESULT 548 END : 548 (0 seconds) [Mon Jun 19 23:16:11 2006] SHOW_RESULT 548 CPU : 0.0500000000000009 = 0.0400000000000009 + 0.01 + 0 + 0 # BOUND : makespan 468 548 MODIFY_CNF 508 BEGIN : [Mon Jun 19 23:16:11 2006] MODIFY_CNF 508 END : 7736441 bytes (0 seconds) [Mon Jun 19 23:16:11 2006] MODIFY_CNF 508 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 508 BEGIN : [Mon Jun 19 23:16:11 2006] CMD : minisat /tmp/csp2sat13988.cnf /tmp/csp2sat13988.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 302762 878046 | 100920 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 13 (27 /sec) decisions : 134 (279 /sec) propagations : 72557 (151160 /sec) conflict literals : 294 (5.47 % deleted) Memory used : 18.29 MB CPU time : 0.48 s SATISFIABLE VERIFY_CNF 508 END : (0 seconds) [Mon Jun 19 23:16:11 2006] VERIFY_CNF 508 CPU : 0.56 = 0 + 0 + 0.49 + 0.07 # RESULT : makespan 508 SATISFIABLE SHOW_RESULT 508 BEGIN : [Mon Jun 19 23:16:11 2006] # ASSIGN : makespan 508 # ASSIGN : s_0_0 230 # ASSIGN : s_0_1 106 # ASSIGN : s_0_2 321 # ASSIGN : s_0_3 201 # ASSIGN : s_0_4 426 # ASSIGN : s_0_5 16 # ASSIGN : s_0_6 11 # ASSIGN : s_1_0 306 # ASSIGN : s_1_1 458 # ASSIGN : s_1_2 226 # ASSIGN : s_1_3 390 # ASSIGN : s_1_4 182 # ASSIGN : s_1_5 94 # ASSIGN : s_1_6 16 # ASSIGN : s_2_0 397 # ASSIGN : s_2_1 205 # ASSIGN : s_2_2 491 # ASSIGN : s_2_3 304 # ASSIGN : s_2_4 1 # ASSIGN : s_2_5 146 # ASSIGN : s_2_6 78 # ASSIGN : s_3_0 5 # ASSIGN : s_3_1 302 # ASSIGN : s_3_2 414 # ASSIGN : s_3_3 486 # ASSIGN : s_3_4 51 # ASSIGN : s_3_5 204 # ASSIGN : s_3_6 145 # ASSIGN : s_4_0 468 # ASSIGN : s_4_1 364 # ASSIGN : s_4_2 8 # ASSIGN : s_4_3 87 # ASSIGN : s_4_4 167 # ASSIGN : s_4_5 337 # ASSIGN : s_4_6 202 # ASSIGN : s_5_0 64 # ASSIGN : s_5_1 19 # ASSIGN : s_5_2 110 # ASSIGN : s_5_3 175 # ASSIGN : s_5_4 236 # ASSIGN : s_5_5 386 # ASSIGN : s_5_6 289 # ASSIGN : s_6_0 138 # ASSIGN : s_6_1 81 # ASSIGN : s_6_2 157 # ASSIGN : s_6_3 231 # ASSIGN : s_6_4 280 # ASSIGN : s_6_5 455 # ASSIGN : s_6_6 363 SHOW_RESULT 508 END : 508 (0 seconds) [Mon Jun 19 23:16:11 2006] SHOW_RESULT 508 CPU : 0.0499999999999989 = 0.0499999999999989 + 0 + 0 + 0 # BOUND : makespan 468 508 MODIFY_CNF 488 BEGIN : [Mon Jun 19 23:16:11 2006] MODIFY_CNF 488 END : 7736441 bytes (0 seconds) [Mon Jun 19 23:16:11 2006] MODIFY_CNF 488 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 488 BEGIN : [Mon Jun 19 23:16:11 2006] CMD : minisat /tmp/csp2sat13988.cnf /tmp/csp2sat13988.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 291002 842766 | 97000 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 49 (84 /sec) decisions : 158 (272 /sec) propagations : 116977 (201684 /sec) conflict literals : 884 (3.49 % deleted) Memory used : 18.29 MB CPU time : 0.58 s SATISFIABLE VERIFY_CNF 488 END : (1 seconds) [Mon Jun 19 23:16:12 2006] VERIFY_CNF 488 CPU : 0.61 = 0 + 0 + 0.59 + 0.02 # RESULT : makespan 488 SATISFIABLE SHOW_RESULT 488 BEGIN : [Mon Jun 19 23:16:12 2006] # ASSIGN : makespan 488 # ASSIGN : s_0_0 130 # ASSIGN : s_0_1 11 # ASSIGN : s_0_2 206 # ASSIGN : s_0_3 459 # ASSIGN : s_0_4 299 # ASSIGN : s_0_5 381 # ASSIGN : s_0_6 6 # ASSIGN : s_1_0 239 # ASSIGN : s_1_1 106 # ASSIGN : s_1_2 391 # ASSIGN : s_1_3 323 # ASSIGN : s_1_4 0 # ASSIGN : s_1_5 156 # ASSIGN : s_1_6 44 # ASSIGN : s_2_0 400 # ASSIGN : s_2_1 297 # ASSIGN : s_2_2 471 # ASSIGN : s_2_3 188 # ASSIGN : s_2_4 61 # ASSIGN : s_2_5 0 # ASSIGN : s_2_6 111 # ASSIGN : s_3_0 12 # ASSIGN : s_3_1 235 # ASSIGN : s_3_2 319 # ASSIGN : s_3_3 156 # ASSIGN : s_3_4 394 # ASSIGN : s_3_5 58 # ASSIGN : s_3_6 178 # ASSIGN : s_4_0 337 # ASSIGN : s_4_1 394 # ASSIGN : s_4_2 127 # ASSIGN : s_4_3 32 # ASSIGN : s_4_4 112 # ASSIGN : s_4_5 208 # ASSIGN : s_4_6 235 # ASSIGN : s_5_0 84 # ASSIGN : s_5_1 190 # ASSIGN : s_5_2 11 # ASSIGN : s_5_3 433 # ASSIGN : s_5_4 146 # ASSIGN : s_5_5 253 # ASSIGN : s_5_6 322 # ASSIGN : s_6_0 377 # ASSIGN : s_6_1 165 # ASSIGN : s_6_2 58 # ASSIGN : s_6_3 274 # ASSIGN : s_6_4 191 # ASSIGN : s_6_5 324 # ASSIGN : s_6_6 396 SHOW_RESULT 488 END : 488 (0 seconds) [Mon Jun 19 23:16:12 2006] SHOW_RESULT 488 CPU : 0.0500000000000007 = 0.0500000000000007 + 0 + 0 + 0 # BOUND : makespan 468 488 MODIFY_CNF 478 BEGIN : [Mon Jun 19 23:16:12 2006] MODIFY_CNF 478 END : 7736441 bytes (0 seconds) [Mon Jun 19 23:16:12 2006] MODIFY_CNF 478 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 478 BEGIN : [Mon Jun 19 23:16:12 2006] CMD : minisat /tmp/csp2sat13988.cnf /tmp/csp2sat13988.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 285122 825126 | 95040 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 14 (26 /sec) decisions : 96 (178 /sec) propagations : 72243 (133783 /sec) conflict literals : 364 (3.45 % deleted) Memory used : 18.29 MB CPU time : 0.54 s SATISFIABLE VERIFY_CNF 478 END : (1 seconds) [Mon Jun 19 23:16:13 2006] VERIFY_CNF 478 CPU : 0.57 = 0 + 0 + 0.55 + 0.02 # RESULT : makespan 478 SATISFIABLE SHOW_RESULT 478 BEGIN : [Mon Jun 19 23:16:13 2006] # ASSIGN : makespan 478 # ASSIGN : s_0_0 324 # ASSIGN : s_0_1 121 # ASSIGN : s_0_2 216 # ASSIGN : s_0_3 10 # ASSIGN : s_0_4 39 # ASSIGN : s_0_5 400 # ASSIGN : s_0_6 0 # ASSIGN : s_1_0 240 # ASSIGN : s_1_1 70 # ASSIGN : s_1_2 398 # ASSIGN : s_1_3 120 # ASSIGN : s_1_4 340 # ASSIGN : s_1_5 188 # ASSIGN : s_1_6 5 # ASSIGN : s_2_0 407 # ASSIGN : s_2_1 284 # ASSIGN : s_2_2 381 # ASSIGN : s_2_3 196 # ASSIGN : s_2_4 134 # ASSIGN : s_2_5 1 # ASSIGN : s_2_6 67 # ASSIGN : s_3_0 13 # ASSIGN : s_3_1 220 # ASSIGN : s_3_2 309 # ASSIGN : s_3_3 282 # ASSIGN : s_3_4 384 # ASSIGN : s_3_5 59 # ASSIGN : s_3_6 160 # ASSIGN : s_4_0 113 # ASSIGN : s_4_1 384 # ASSIGN : s_4_2 21 # ASSIGN : s_4_3 304 # ASSIGN : s_4_4 184 # ASSIGN : s_4_5 157 # ASSIGN : s_4_6 217 # ASSIGN : s_5_0 153 # ASSIGN : s_5_1 0 # ASSIGN : s_5_2 100 # ASSIGN : s_5_3 452 # ASSIGN : s_5_4 199 # ASSIGN : s_5_5 243 # ASSIGN : s_5_6 312 # ASSIGN : s_6_0 221 # ASSIGN : s_6_1 45 # ASSIGN : s_6_2 147 # ASSIGN : s_6_3 71 # ASSIGN : s_6_4 250 # ASSIGN : s_6_5 333 # ASSIGN : s_6_6 386 SHOW_RESULT 478 END : 478 (0 seconds) [Mon Jun 19 23:16:13 2006] SHOW_RESULT 478 CPU : 0.0500000000000007 = 0.0500000000000007 + 0 + 0 + 0 # BOUND : makespan 468 478 MODIFY_CNF 473 BEGIN : [Mon Jun 19 23:16:13 2006] MODIFY_CNF 473 END : 7736440 bytes (0 seconds) [Mon Jun 19 23:16:13 2006] MODIFY_CNF 473 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 473 BEGIN : [Mon Jun 19 23:16:13 2006] CMD : minisat /tmp/csp2sat13988.cnf /tmp/csp2sat13988.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 282182 816306 | 94060 0 0 nan | 0.000 % | | 100 | 282182 816306 | 103466 100 3145 31.4 | 34.283 % | ============================================================================== restarts : 2 conflicts : 244 (218 /sec) decisions : 461 (412 /sec) propagations : 717040 (640214 /sec) conflict literals : 8820 (16.29 % deleted) Memory used : 18.31 MB CPU time : 1.12 s SATISFIABLE VERIFY_CNF 473 END : (1 seconds) [Mon Jun 19 23:16:14 2006] VERIFY_CNF 473 CPU : 1.19 = 0 + 0 + 1.13 + 0.06 # RESULT : makespan 473 SATISFIABLE SHOW_RESULT 473 BEGIN : [Mon Jun 19 23:16:14 2006] # ASSIGN : makespan 473 # ASSIGN : s_0_0 270 # ASSIGN : s_0_1 349 # ASSIGN : s_0_2 172 # ASSIGN : s_0_3 444 # ASSIGN : s_0_4 7 # ASSIGN : s_0_5 89 # ASSIGN : s_0_6 2 # ASSIGN : s_1_0 163 # ASSIGN : s_1_1 299 # ASSIGN : s_1_2 8 # ASSIGN : s_1_3 361 # ASSIGN : s_1_4 429 # ASSIGN : s_1_5 247 # ASSIGN : s_1_6 100 # ASSIGN : s_2_0 402 # ASSIGN : s_2_1 63 # ASSIGN : s_2_2 315 # ASSIGN : s_2_3 229 # ASSIGN : s_2_4 352 # ASSIGN : s_2_5 5 # ASSIGN : s_2_6 162 # ASSIGN : s_3_0 77 # ASSIGN : s_3_1 1 # ASSIGN : s_3_2 401 # ASSIGN : s_3_3 123 # ASSIGN : s_3_4 152 # ASSIGN : s_3_5 303 # ASSIGN : s_3_6 246 # ASSIGN : s_4_0 346 # ASSIGN : s_4_1 205 # ASSIGN : s_4_2 88 # ASSIGN : s_4_3 2 # ASSIGN : s_4_4 331 # ASSIGN : s_4_5 167 # ASSIGN : s_4_6 386 # ASSIGN : s_5_0 31 # ASSIGN : s_5_1 160 # ASSIGN : s_5_2 265 # ASSIGN : s_5_3 82 # ASSIGN : s_5_4 108 # ASSIGN : s_5_5 404 # ASSIGN : s_5_6 312 # ASSIGN : s_6_0 126 # ASSIGN : s_6_1 448 # ASSIGN : s_6_2 332 # ASSIGN : s_6_3 145 # ASSIGN : s_6_4 248 # ASSIGN : s_6_5 194 # ASSIGN : s_6_6 8 SHOW_RESULT 473 END : 473 (0 seconds) [Mon Jun 19 23:16:14 2006] SHOW_RESULT 473 CPU : 0.0399999999999991 = 0.0399999999999991 + 0 + 0 + 0 # BOUND : makespan 468 473 MODIFY_CNF 470 BEGIN : [Mon Jun 19 23:16:14 2006] MODIFY_CNF 470 END : 7736440 bytes (0 seconds) [Mon Jun 19 23:16:14 2006] MODIFY_CNF 470 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 470 BEGIN : [Mon Jun 19 23:16:14 2006] CMD : minisat /tmp/csp2sat13988.cnf /tmp/csp2sat13988.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 280418 811014 | 93472 0 0 nan | 0.000 % | | 100 | 280418 811014 | 102819 100 2548 25.5 | 34.756 % | | 250 | 280418 811014 | 113101 250 6213 24.9 | 34.756 % | | 476 | 280418 811014 | 124411 476 12899 27.1 | 34.756 % | | 814 | 280418 811014 | 136852 814 20045 24.6 | 34.756 % | | 1321 | 280418 811014 | 150537 1321 35624 27.0 | 34.756 % | ============================================================================== restarts : 6 conflicts : 1647 (363 /sec) decisions : 2452 (540 /sec) propagations : 4147106 (913459 /sec) conflict literals : 47929 (19.26 % deleted) Memory used : 18.31 MB CPU time : 4.54 s SATISFIABLE VERIFY_CNF 470 END : (5 seconds) [Mon Jun 19 23:16:19 2006] VERIFY_CNF 470 CPU : 4.61 = 0 + 0 + 4.56 + 0.05 # RESULT : makespan 470 SATISFIABLE SHOW_RESULT 470 BEGIN : [Mon Jun 19 23:16:19 2006] # ASSIGN : makespan 470 # ASSIGN : s_0_0 98 # ASSIGN : s_0_1 281 # ASSIGN : s_0_2 377 # ASSIGN : s_0_3 174 # ASSIGN : s_0_4 3 # ASSIGN : s_0_5 203 # ASSIGN : s_0_6 93 # ASSIGN : s_1_0 1 # ASSIGN : s_1_1 231 # ASSIGN : s_1_2 129 # ASSIGN : s_1_3 402 # ASSIGN : s_1_4 85 # ASSIGN : s_1_5 350 # ASSIGN : s_1_6 283 # ASSIGN : s_2_0 207 # ASSIGN : s_2_1 89 # ASSIGN : s_2_2 278 # ASSIGN : s_2_3 3 # ASSIGN : s_2_4 295 # ASSIGN : s_2_5 412 # ASSIGN : s_2_6 345 # ASSIGN : s_3_0 367 # ASSIGN : s_3_1 2 # ASSIGN : s_3_2 295 # ASSIGN : s_3_3 273 # ASSIGN : s_3_4 179 # ASSIGN : s_3_5 71 # ASSIGN : s_3_6 413 # ASSIGN : s_4_0 321 # ASSIGN : s_4_1 376 # ASSIGN : s_4_2 3 # ASSIGN : s_4_3 89 # ASSIGN : s_4_4 361 # ASSIGN : s_4_5 169 # ASSIGN : s_4_6 196 # ASSIGN : s_5_0 424 # ASSIGN : s_5_1 186 # ASSIGN : s_5_2 82 # ASSIGN : s_5_3 247 # ASSIGN : s_5_4 135 # ASSIGN : s_5_5 281 # ASSIGN : s_5_6 8 # ASSIGN : s_6_0 302 # ASSIGN : s_6_1 64 # ASSIGN : s_6_2 209 # ASSIGN : s_6_3 338 # ASSIGN : s_6_4 387 # ASSIGN : s_6_5 11 # ASSIGN : s_6_6 104 SHOW_RESULT 470 END : 470 (0 seconds) [Mon Jun 19 23:16:19 2006] SHOW_RESULT 470 CPU : 0.0500000000000009 = 0.0400000000000009 + 0.01 + 0 + 0 # BOUND : makespan 468 470 MODIFY_CNF 469 BEGIN : [Mon Jun 19 23:16:19 2006] MODIFY_CNF 469 END : 7736440 bytes (0 seconds) [Mon Jun 19 23:16:19 2006] MODIFY_CNF 469 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 469 BEGIN : [Mon Jun 19 23:16:19 2006] CMD : minisat /tmp/csp2sat13988.cnf /tmp/csp2sat13988.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 279830 809250 | 93276 0 0 nan | 0.000 % | | 101 | 279830 809250 | 102603 101 3197 31.7 | 34.914 % | | 253 | 279830 809250 | 112863 253 8389 33.2 | 34.914 % | | 478 | 279830 809250 | 124150 478 15069 31.5 | 34.914 % | | 816 | 279830 809250 | 136565 816 30741 37.7 | 34.914 % | ============================================================================== restarts : 5 conflicts : 828 (327 /sec) decisions : 1375 (543 /sec) propagations : 2063072 (815443 /sec) conflict literals : 30974 (15.77 % deleted) Memory used : 18.31 MB CPU time : 2.53 s SATISFIABLE VERIFY_CNF 469 END : (2 seconds) [Mon Jun 19 23:16:21 2006] VERIFY_CNF 469 CPU : 2.59 = 0 + 0 + 2.54 + 0.05 # RESULT : makespan 469 SATISFIABLE SHOW_RESULT 469 BEGIN : [Mon Jun 19 23:16:21 2006] # ASSIGN : makespan 469 # ASSIGN : s_0_0 172 # ASSIGN : s_0_1 277 # ASSIGN : s_0_2 376 # ASSIGN : s_0_3 248 # ASSIGN : s_0_4 86 # ASSIGN : s_0_5 7 # ASSIGN : s_0_6 2 # ASSIGN : s_1_0 73 # ASSIGN : s_1_1 157 # ASSIGN : s_1_2 215 # ASSIGN : s_1_3 5 # ASSIGN : s_1_4 425 # ASSIGN : s_1_5 295 # ASSIGN : s_1_6 350 # ASSIGN : s_2_0 301 # ASSIGN : s_2_1 372 # ASSIGN : s_2_2 143 # ASSIGN : s_2_3 162 # ASSIGN : s_2_4 251 # ASSIGN : s_2_5 85 # ASSIGN : s_2_6 9 # ASSIGN : s_3_0 250 # ASSIGN : s_3_1 1 # ASSIGN : s_3_2 71 # ASSIGN : s_3_3 296 # ASSIGN : s_3_4 318 # ASSIGN : s_3_5 152 # ASSIGN : s_3_6 412 # ASSIGN : s_4_0 8 # ASSIGN : s_4_1 63 # ASSIGN : s_4_2 297 # ASSIGN : s_4_3 389 # ASSIGN : s_4_4 48 # ASSIGN : s_4_5 268 # ASSIGN : s_4_6 181 # ASSIGN : s_5_0 423 # ASSIGN : s_5_1 207 # ASSIGN : s_5_2 160 # ASSIGN : s_5_3 134 # ASSIGN : s_5_4 4 # ASSIGN : s_5_5 347 # ASSIGN : s_5_6 273 # ASSIGN : s_6_0 397 # ASSIGN : s_6_1 252 # ASSIGN : s_6_2 2 # ASSIGN : s_6_3 340 # ASSIGN : s_6_4 168 # ASSIGN : s_6_5 416 # ASSIGN : s_6_6 76 SHOW_RESULT 469 END : 469 (0 seconds) [Mon Jun 19 23:16:21 2006] SHOW_RESULT 469 CPU : 0.0499999999999989 = 0.0499999999999989 + 0 + 0 + 0 # BOUND : makespan 468 469 MODIFY_CNF 468 BEGIN : [Mon Jun 19 23:16:21 2006] MODIFY_CNF 468 END : 7736440 bytes (0 seconds) [Mon Jun 19 23:16:21 2006] MODIFY_CNF 468 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 468 BEGIN : [Mon Jun 19 23:16:21 2006] CMD : minisat /tmp/csp2sat13988.cnf /tmp/csp2sat13988.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 279243 807486 | 93081 0 0 nan | 0.000 % | | 100 | 279243 807486 | 102389 100 3127 31.3 | 35.072 % | | 250 | 279243 807486 | 112628 250 7133 28.5 | 35.072 % | | 475 | 279243 807486 | 123890 475 14187 29.9 | 35.072 % | | 815 | 279243 807486 | 136279 815 21321 26.2 | 35.072 % | ============================================================================== restarts : 5 conflicts : 1239 (331 /sec) decisions : 1942 (519 /sec) propagations : 3271554 (874747 /sec) conflict literals : 32234 (21.11 % deleted) Memory used : 18.31 MB CPU time : 3.74 s SATISFIABLE VERIFY_CNF 468 END : (4 seconds) [Mon Jun 19 23:16:25 2006] VERIFY_CNF 468 CPU : 3.78 = 0 + 0 + 3.76 + 0.02 # RESULT : makespan 468 SATISFIABLE SHOW_RESULT 468 BEGIN : [Mon Jun 19 23:16:25 2006] # ASSIGN : makespan 468 # ASSIGN : s_0_0 392 # ASSIGN : s_0_1 0 # ASSIGN : s_0_2 296 # ASSIGN : s_0_3 107 # ASSIGN : s_0_4 136 # ASSIGN : s_0_5 218 # ASSIGN : s_0_6 102 # ASSIGN : s_1_0 124 # ASSIGN : s_1_1 356 # ASSIGN : s_1_2 208 # ASSIGN : s_1_3 288 # ASSIGN : s_1_4 22 # ASSIGN : s_1_5 66 # ASSIGN : s_1_6 406 # ASSIGN : s_2_0 261 # ASSIGN : s_2_1 95 # ASSIGN : s_2_2 75 # ASSIGN : s_2_3 382 # ASSIGN : s_2_4 332 # ASSIGN : s_2_5 8 # ASSIGN : s_2_6 194 # ASSIGN : s_3_0 72 # ASSIGN : s_3_1 406 # ASSIGN : s_3_2 0 # ASSIGN : s_3_3 216 # ASSIGN : s_3_4 238 # ASSIGN : s_3_5 118 # ASSIGN : s_3_6 349 # ASSIGN : s_4_0 221 # ASSIGN : s_4_1 262 # ASSIGN : s_4_2 389 # ASSIGN : s_4_3 27 # ASSIGN : s_4_4 7 # ASSIGN : s_4_5 362 # ASSIGN : s_4_6 107 # ASSIGN : s_5_0 26 # ASSIGN : s_5_1 217 # ASSIGN : s_5_2 161 # ASSIGN : s_5_3 0 # ASSIGN : s_5_4 92 # ASSIGN : s_5_5 399 # ASSIGN : s_5_6 275 # ASSIGN : s_6_0 366 # ASSIGN : s_6_1 192 # ASSIGN : s_6_2 92 # ASSIGN : s_6_3 239 # ASSIGN : s_6_4 385 # ASSIGN : s_6_5 309 # ASSIGN : s_6_6 0 SHOW_RESULT 468 END : 468 (0 seconds) [Mon Jun 19 23:16:25 2006] SHOW_RESULT 468 CPU : 0.0400000000000009 = 0.0400000000000009 + 0 + 0 + 0 # BOUND : makespan 468 468 MAIN END : (29 seconds) [Mon Jun 19 23:16:25 2006] MAIN CPU : 29.54 = 15.03 + 0.07 + 14.12 + 0.32