# TIMEOUT 18000 MAIN BEGIN : [Mon Jun 19 23:18:47 2006] READ BEGIN : csp/tai_7x7_9.csp [Mon Jun 19 23:18:47 2006] READ END : csp/tai_7x7_9.csp (0 seconds) [Mon Jun 19 23:18:47 2006] READ CPU : 0.64 = 0.64 + 0 + 0 + 0 # BOUND : makespan 458 633 GENERATE_CNF 633 BEGIN : [Mon Jun 19 23:18:47 2006] GENERATE_CNF 633 END : 31929 variables 380761 clauses 7871394 bytes (15 seconds) [Mon Jun 19 23:19:02 2006] GENERATE_CNF 633 CPU : 14.44 = 14.42 + 0.02 + 0 + 0 MODIFY_CNF 545 BEGIN : [Mon Jun 19 23:19:02 2006] MODIFY_CNF 545 END : 7871399 bytes (0 seconds) [Mon Jun 19 23:19:02 2006] MODIFY_CNF 545 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 545 BEGIN : [Mon Jun 19 23:19:02 2006] CMD : minisat /tmp/csp2sat14077.cnf /tmp/csp2sat14077.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 328081 953743 | 109360 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 8 (16 /sec) decisions : 190 (388 /sec) propagations : 50259 (102569 /sec) conflict literals : 92 (4.17 % deleted) Memory used : 18.50 MB CPU time : 0.49 s SATISFIABLE VERIFY_CNF 545 END : (1 seconds) [Mon Jun 19 23:19:03 2006] VERIFY_CNF 545 CPU : 0.55 = 0 + 0 + 0.51 + 0.04 # RESULT : makespan 545 SATISFIABLE SHOW_RESULT 545 BEGIN : [Mon Jun 19 23:19:03 2006] # ASSIGN : makespan 545 # ASSIGN : s_0_0 404 # ASSIGN : s_0_1 231 # ASSIGN : s_0_2 335 # ASSIGN : s_0_3 436 # ASSIGN : s_0_4 0 # ASSIGN : s_0_5 106 # ASSIGN : s_0_6 75 # ASSIGN : s_1_0 466 # ASSIGN : s_1_1 394 # ASSIGN : s_1_2 300 # ASSIGN : s_1_3 479 # ASSIGN : s_1_4 71 # ASSIGN : s_1_5 178 # ASSIGN : s_1_6 118 # ASSIGN : s_2_0 144 # ASSIGN : s_2_1 298 # ASSIGN : s_2_2 202 # ASSIGN : s_2_3 392 # ASSIGN : s_2_4 112 # ASSIGN : s_2_5 225 # ASSIGN : s_2_6 190 # ASSIGN : s_3_0 3 # ASSIGN : s_3_1 495 # ASSIGN : s_3_2 367 # ASSIGN : s_3_3 216 # ASSIGN : s_3_4 127 # ASSIGN : s_3_5 311 # ASSIGN : s_3_6 196 # ASSIGN : s_4_0 93 # ASSIGN : s_4_1 194 # ASSIGN : s_4_2 459 # ASSIGN : s_4_3 8 # ASSIGN : s_4_4 272 # ASSIGN : s_4_5 353 # ASSIGN : s_4_6 285 # ASSIGN : s_5_0 192 # ASSIGN : s_5_1 145 # ASSIGN : s_5_2 1 # ASSIGN : s_5_3 83 # ASSIGN : s_5_4 311 # ASSIGN : s_5_5 446 # ASSIGN : s_5_6 409 # ASSIGN : s_6_0 281 # ASSIGN : s_6_1 35 # ASSIGN : s_6_2 66 # ASSIGN : s_6_3 152 # ASSIGN : s_6_4 374 # ASSIGN : s_6_5 528 # ASSIGN : s_6_6 436 SHOW_RESULT 545 END : 545 (0 seconds) [Mon Jun 19 23:19:03 2006] SHOW_RESULT 545 CPU : 0.0500000000000007 = 0.0500000000000007 + 0 + 0 + 0 # BOUND : makespan 458 545 MODIFY_CNF 501 BEGIN : [Mon Jun 19 23:19:03 2006] MODIFY_CNF 501 END : 7871399 bytes (0 seconds) [Mon Jun 19 23:19:03 2006] MODIFY_CNF 501 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 501 BEGIN : [Mon Jun 19 23:19:03 2006] CMD : minisat /tmp/csp2sat14077.cnf /tmp/csp2sat14077.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 302209 876127 | 100736 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 5 (11 /sec) decisions : 143 (304 /sec) propagations : 40212 (85557 /sec) conflict literals : 50 (0.00 % deleted) Memory used : 18.54 MB CPU time : 0.47 s SATISFIABLE VERIFY_CNF 501 END : (0 seconds) [Mon Jun 19 23:19:03 2006] VERIFY_CNF 501 CPU : 0.54 = 0 + 0 + 0.49 + 0.05 # RESULT : makespan 501 SATISFIABLE SHOW_RESULT 501 BEGIN : [Mon Jun 19 23:19:03 2006] # ASSIGN : makespan 501 # ASSIGN : s_0_0 360 # ASSIGN : s_0_1 218 # ASSIGN : s_0_2 305 # ASSIGN : s_0_3 392 # ASSIGN : s_0_4 113 # ASSIGN : s_0_5 3 # ASSIGN : s_0_6 82 # ASSIGN : s_1_0 2 # ASSIGN : s_1_1 285 # ASSIGN : s_1_2 250 # ASSIGN : s_1_3 435 # ASSIGN : s_1_4 184 # ASSIGN : s_1_5 75 # ASSIGN : s_1_6 124 # ASSIGN : s_2_0 455 # ASSIGN : s_2_1 357 # ASSIGN : s_2_2 0 # ASSIGN : s_2_3 313 # ASSIGN : s_2_4 225 # ASSIGN : s_2_5 122 # ASSIGN : s_2_6 195 # ASSIGN : s_3_0 263 # ASSIGN : s_3_1 451 # ASSIGN : s_3_2 109 # ASSIGN : s_3_3 8 # ASSIGN : s_3_4 353 # ASSIGN : s_3_5 221 # ASSIGN : s_3_6 201 # ASSIGN : s_4_0 15 # ASSIGN : s_4_1 66 # ASSIGN : s_4_2 402 # ASSIGN : s_4_3 103 # ASSIGN : s_4_4 488 # ASSIGN : s_4_5 309 # ASSIGN : s_4_6 235 # ASSIGN : s_5_0 67 # ASSIGN : s_5_1 19 # ASSIGN : s_5_2 337 # ASSIGN : s_5_3 178 # ASSIGN : s_5_4 240 # ASSIGN : s_5_5 402 # ASSIGN : s_5_6 303 # ASSIGN : s_6_0 156 # ASSIGN : s_6_1 125 # ASSIGN : s_6_2 23 # ASSIGN : s_6_3 249 # ASSIGN : s_6_4 422 # ASSIGN : s_6_5 484 # ASSIGN : s_6_6 330 SHOW_RESULT 501 END : 501 (0 seconds) [Mon Jun 19 23:19:03 2006] SHOW_RESULT 501 CPU : 0.0499999999999991 = 0.0399999999999991 + 0.01 + 0 + 0 # BOUND : makespan 458 501 MODIFY_CNF 479 BEGIN : [Mon Jun 19 23:19:03 2006] MODIFY_CNF 479 END : 7871399 bytes (0 seconds) [Mon Jun 19 23:19:03 2006] MODIFY_CNF 479 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 479 BEGIN : [Mon Jun 19 23:19:03 2006] CMD : minisat /tmp/csp2sat14077.cnf /tmp/csp2sat14077.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 289273 837319 | 96424 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 38 (68 /sec) decisions : 163 (291 /sec) propagations : 112579 (201034 /sec) conflict literals : 1081 (8.70 % deleted) Memory used : 18.54 MB CPU time : 0.56 s SATISFIABLE VERIFY_CNF 479 END : (1 seconds) [Mon Jun 19 23:19:04 2006] VERIFY_CNF 479 CPU : 0.61 = 0 + 0 + 0.58 + 0.03 # RESULT : makespan 479 SATISFIABLE SHOW_RESULT 479 BEGIN : [Mon Jun 19 23:19:04 2006] # ASSIGN : makespan 479 # ASSIGN : s_0_0 183 # ASSIGN : s_0_1 340 # ASSIGN : s_0_2 302 # ASSIGN : s_0_3 436 # ASSIGN : s_0_4 105 # ASSIGN : s_0_5 33 # ASSIGN : s_0_6 2 # ASSIGN : s_1_0 376 # ASSIGN : s_1_1 407 # ASSIGN : s_1_2 334 # ASSIGN : s_1_3 228 # ASSIGN : s_1_4 8 # ASSIGN : s_1_5 109 # ASSIGN : s_1_6 49 # ASSIGN : s_2_0 323 # ASSIGN : s_2_1 229 # ASSIGN : s_2_2 369 # ASSIGN : s_2_3 392 # ASSIGN : s_2_4 90 # ASSIGN : s_2_5 156 # ASSIGN : s_2_6 150 # ASSIGN : s_3_0 389 # ASSIGN : s_3_1 106 # ASSIGN : s_3_2 14 # ASSIGN : s_3_3 294 # ASSIGN : s_3_4 176 # ASSIGN : s_3_5 245 # ASSIGN : s_3_6 156 # ASSIGN : s_4_0 18 # ASSIGN : s_4_1 69 # ASSIGN : s_4_2 393 # ASSIGN : s_4_3 131 # ASSIGN : s_4_4 274 # ASSIGN : s_4_5 287 # ASSIGN : s_4_6 206 # ASSIGN : s_5_0 80 # ASSIGN : s_5_1 169 # ASSIGN : s_5_2 216 # ASSIGN : s_5_3 3 # ASSIGN : s_5_4 317 # ASSIGN : s_5_5 380 # ASSIGN : s_5_6 281 # ASSIGN : s_6_0 215 # ASSIGN : s_6_1 34 # ASSIGN : s_6_2 129 # ASSIGN : s_6_3 65 # ASSIGN : s_6_4 400 # ASSIGN : s_6_5 462 # ASSIGN : s_6_6 308 SHOW_RESULT 479 END : 479 (0 seconds) [Mon Jun 19 23:19:04 2006] SHOW_RESULT 479 CPU : 0.0500000000000007 = 0.0500000000000007 + 0 + 0 + 0 # BOUND : makespan 458 479 MODIFY_CNF 468 BEGIN : [Mon Jun 19 23:19:04 2006] MODIFY_CNF 468 END : 7871399 bytes (0 seconds) [Mon Jun 19 23:19:04 2006] MODIFY_CNF 468 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 468 BEGIN : [Mon Jun 19 23:19:04 2006] CMD : minisat /tmp/csp2sat14077.cnf /tmp/csp2sat14077.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 282805 817915 | 94268 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 24 (47 /sec) decisions : 162 (318 /sec) propagations : 74917 (146896 /sec) conflict literals : 490 (2.20 % deleted) Memory used : 18.54 MB CPU time : 0.51 s SATISFIABLE VERIFY_CNF 468 END : (1 seconds) [Mon Jun 19 23:19:05 2006] VERIFY_CNF 468 CPU : 0.59 = 0.00999999999999979 + 0 + 0.52 + 0.06 # RESULT : makespan 468 SATISFIABLE SHOW_RESULT 468 BEGIN : [Mon Jun 19 23:19:05 2006] # ASSIGN : makespan 468 # ASSIGN : s_0_0 160 # ASSIGN : s_0_1 329 # ASSIGN : s_0_2 297 # ASSIGN : s_0_3 425 # ASSIGN : s_0_4 192 # ASSIGN : s_0_5 42 # ASSIGN : s_0_6 11 # ASSIGN : s_1_0 319 # ASSIGN : s_1_1 396 # ASSIGN : s_1_2 347 # ASSIGN : s_1_3 217 # ASSIGN : s_1_4 13 # ASSIGN : s_1_5 114 # ASSIGN : s_1_6 54 # ASSIGN : s_2_0 332 # ASSIGN : s_2_1 235 # ASSIGN : s_2_2 95 # ASSIGN : s_2_3 381 # ASSIGN : s_2_4 80 # ASSIGN : s_2_5 161 # ASSIGN : s_2_6 155 # ASSIGN : s_3_0 378 # ASSIGN : s_3_1 184 # ASSIGN : s_3_2 3 # ASSIGN : s_3_3 283 # ASSIGN : s_3_4 95 # ASSIGN : s_3_5 234 # ASSIGN : s_3_6 164 # ASSIGN : s_4_0 3 # ASSIGN : s_4_1 147 # ASSIGN : s_4_2 382 # ASSIGN : s_4_3 68 # ASSIGN : s_4_4 263 # ASSIGN : s_4_5 276 # ASSIGN : s_4_6 195 # ASSIGN : s_5_0 54 # ASSIGN : s_5_1 7 # ASSIGN : s_5_2 205 # ASSIGN : s_5_3 143 # ASSIGN : s_5_4 306 # ASSIGN : s_5_5 369 # ASSIGN : s_5_6 270 # ASSIGN : s_6_0 204 # ASSIGN : s_6_1 87 # ASSIGN : s_6_2 118 # ASSIGN : s_6_3 4 # ASSIGN : s_6_4 389 # ASSIGN : s_6_5 451 # ASSIGN : s_6_6 297 SHOW_RESULT 468 END : 468 (0 seconds) [Mon Jun 19 23:19:05 2006] SHOW_RESULT 468 CPU : 0.0399999999999991 = 0.0399999999999991 + 0 + 0 + 0 # BOUND : makespan 458 468 MODIFY_CNF 463 BEGIN : [Mon Jun 19 23:19:05 2006] MODIFY_CNF 463 END : 7871398 bytes (0 seconds) [Mon Jun 19 23:19:05 2006] MODIFY_CNF 463 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 463 BEGIN : [Mon Jun 19 23:19:05 2006] CMD : minisat /tmp/csp2sat14077.cnf /tmp/csp2sat14077.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 279865 809095 | 93288 0 0 nan | 0.000 % | | 100 | 279865 809095 | 102616 100 2995 29.9 | 35.682 % | ============================================================================== restarts : 2 conflicts : 109 (160 /sec) decisions : 329 (484 /sec) propagations : 252459 (371263 /sec) conflict literals : 3068 (6.06 % deleted) Memory used : 18.56 MB CPU time : 0.68 s SATISFIABLE VERIFY_CNF 463 END : (1 seconds) [Mon Jun 19 23:19:06 2006] VERIFY_CNF 463 CPU : 0.75 = 0 + 0 + 0.69 + 0.06 # RESULT : makespan 463 SATISFIABLE SHOW_RESULT 463 BEGIN : [Mon Jun 19 23:19:06 2006] # ASSIGN : makespan 463 # ASSIGN : s_0_0 385 # ASSIGN : s_0_1 43 # ASSIGN : s_0_2 431 # ASSIGN : s_0_3 294 # ASSIGN : s_0_4 203 # ASSIGN : s_0_5 120 # ASSIGN : s_0_6 354 # ASSIGN : s_1_0 372 # ASSIGN : s_1_1 156 # ASSIGN : s_1_2 3 # ASSIGN : s_1_3 228 # ASSIGN : s_1_4 100 # ASSIGN : s_1_5 323 # ASSIGN : s_1_6 403 # ASSIGN : s_2_0 417 # ASSIGN : s_2_1 250 # ASSIGN : s_2_2 394 # ASSIGN : s_2_3 109 # ASSIGN : s_2_4 85 # ASSIGN : s_2_5 12 # ASSIGN : s_2_6 388 # ASSIGN : s_3_0 99 # ASSIGN : s_3_1 344 # ASSIGN : s_3_2 189 # ASSIGN : s_3_3 4 # ASSIGN : s_3_4 394 # ASSIGN : s_3_5 281 # ASSIGN : s_3_6 324 # ASSIGN : s_4_0 306 # ASSIGN : s_4_1 1 # ASSIGN : s_4_2 38 # ASSIGN : s_4_3 153 # ASSIGN : s_4_4 357 # ASSIGN : s_4_5 370 # ASSIGN : s_4_6 238 # ASSIGN : s_5_0 8 # ASSIGN : s_5_1 416 # ASSIGN : s_5_2 124 # ASSIGN : s_5_3 337 # ASSIGN : s_5_4 274 # ASSIGN : s_5_5 192 # ASSIGN : s_5_6 97 # ASSIGN : s_6_0 213 # ASSIGN : s_6_1 110 # ASSIGN : s_6_2 308 # ASSIGN : s_6_3 399 # ASSIGN : s_6_4 141 # ASSIGN : s_6_5 93 # ASSIGN : s_6_6 1 SHOW_RESULT 463 END : 463 (0 seconds) [Mon Jun 19 23:19:06 2006] SHOW_RESULT 463 CPU : 0.0499999999999991 = 0.0399999999999991 + 0.01 + 0 + 0 # BOUND : makespan 458 463 MODIFY_CNF 460 BEGIN : [Mon Jun 19 23:19:06 2006] MODIFY_CNF 460 END : 7871398 bytes (0 seconds) [Mon Jun 19 23:19:06 2006] MODIFY_CNF 460 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 460 BEGIN : [Mon Jun 19 23:19:06 2006] CMD : minisat /tmp/csp2sat14077.cnf /tmp/csp2sat14077.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 278101 803803 | 92700 0 0 nan | 0.000 % | | 103 | 278101 803803 | 101970 103 1794 17.4 | 36.152 % | ============================================================================== restarts : 2 conflicts : 117 (189 /sec) decisions : 343 (553 /sec) propagations : 168547 (271850 /sec) conflict literals : 1920 (4.57 % deleted) Memory used : 18.56 MB CPU time : 0.62 s SATISFIABLE VERIFY_CNF 460 END : (0 seconds) [Mon Jun 19 23:19:06 2006] VERIFY_CNF 460 CPU : 0.66 = 0 + 0 + 0.64 + 0.02 # RESULT : makespan 460 SATISFIABLE SHOW_RESULT 460 BEGIN : [Mon Jun 19 23:19:06 2006] # ASSIGN : makespan 460 # ASSIGN : s_0_0 288 # ASSIGN : s_0_1 216 # ASSIGN : s_0_2 342 # ASSIGN : s_0_3 135 # ASSIGN : s_0_4 23 # ASSIGN : s_0_5 388 # ASSIGN : s_0_6 185 # ASSIGN : s_1_0 271 # ASSIGN : s_1_1 144 # ASSIGN : s_1_2 284 # ASSIGN : s_1_3 69 # ASSIGN : s_1_4 230 # ASSIGN : s_1_5 341 # ASSIGN : s_1_6 400 # ASSIGN : s_2_0 4 # ASSIGN : s_2_1 50 # ASSIGN : s_2_2 319 # ASSIGN : s_2_3 416 # ASSIGN : s_2_4 379 # ASSIGN : s_2_5 183 # ASSIGN : s_2_6 394 # ASSIGN : s_3_0 163 # ASSIGN : s_3_1 410 # ASSIGN : s_3_2 2 # ASSIGN : s_3_3 315 # ASSIGN : s_3_4 94 # ASSIGN : s_3_5 273 # ASSIGN : s_3_6 253 # ASSIGN : s_4_0 320 # ASSIGN : s_4_1 283 # ASSIGN : s_4_2 374 # ASSIGN : s_4_3 178 # ASSIGN : s_4_4 4 # ASSIGN : s_4_5 85 # ASSIGN : s_4_6 17 # ASSIGN : s_5_0 371 # ASSIGN : s_5_1 320 # ASSIGN : s_5_2 98 # ASSIGN : s_5_3 253 # ASSIGN : s_5_4 163 # ASSIGN : s_5_5 3 # ASSIGN : s_5_6 226 # ASSIGN : s_6_0 70 # ASSIGN : s_6_1 367 # ASSIGN : s_6_2 170 # ASSIGN : s_6_3 5 # ASSIGN : s_6_4 398 # ASSIGN : s_6_5 256 # ASSIGN : s_6_6 275 SHOW_RESULT 460 END : 460 (0 seconds) [Mon Jun 19 23:19:06 2006] SHOW_RESULT 460 CPU : 0.0500000000000007 = 0.0500000000000007 + 0 + 0 + 0 # BOUND : makespan 458 460 MODIFY_CNF 459 BEGIN : [Mon Jun 19 23:19:06 2006] MODIFY_CNF 459 END : 7871398 bytes (0 seconds) [Mon Jun 19 23:19:06 2006] MODIFY_CNF 459 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 459 BEGIN : [Mon Jun 19 23:19:06 2006] CMD : minisat /tmp/csp2sat14077.cnf /tmp/csp2sat14077.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 277513 802039 | 92504 0 0 nan | 0.000 % | | 100 | 277513 802039 | 101754 100 2591 25.9 | 36.309 % | ============================================================================== restarts : 2 conflicts : 154 (200 /sec) decisions : 347 (451 /sec) propagations : 322045 (418240 /sec) conflict literals : 3583 (7.89 % deleted) Memory used : 18.56 MB CPU time : 0.77 s SATISFIABLE VERIFY_CNF 459 END : (1 seconds) [Mon Jun 19 23:19:07 2006] VERIFY_CNF 459 CPU : 0.82 = 0 + 0 + 0.79 + 0.03 # RESULT : makespan 459 SATISFIABLE SHOW_RESULT 459 BEGIN : [Mon Jun 19 23:19:07 2006] # ASSIGN : makespan 459 # ASSIGN : s_0_0 182 # ASSIGN : s_0_1 100 # ASSIGN : s_0_2 369 # ASSIGN : s_0_3 321 # ASSIGN : s_0_4 1 # ASSIGN : s_0_5 230 # ASSIGN : s_0_6 401 # ASSIGN : s_1_0 446 # ASSIGN : s_1_1 230 # ASSIGN : s_1_2 411 # ASSIGN : s_1_3 113 # ASSIGN : s_1_4 72 # ASSIGN : s_1_5 302 # ASSIGN : s_1_6 12 # ASSIGN : s_2_0 303 # ASSIGN : s_2_1 365 # ASSIGN : s_2_2 280 # ASSIGN : s_2_3 69 # ASSIGN : s_2_4 350 # ASSIGN : s_2_5 157 # ASSIGN : s_2_6 270 # ASSIGN : s_3_0 92 # ASSIGN : s_3_1 42 # ASSIGN : s_3_2 183 # ASSIGN : s_3_3 364 # ASSIGN : s_3_4 275 # ASSIGN : s_3_5 0 # ASSIGN : s_3_6 344 # ASSIGN : s_4_0 41 # ASSIGN : s_4_1 4 # ASSIGN : s_4_2 93 # ASSIGN : s_4_3 179 # ASSIGN : s_4_4 446 # ASSIGN : s_4_5 349 # ASSIGN : s_4_6 276 # ASSIGN : s_5_0 214 # ASSIGN : s_5_1 167 # ASSIGN : s_5_2 304 # ASSIGN : s_5_3 7 # ASSIGN : s_5_4 369 # ASSIGN : s_5_5 75 # ASSIGN : s_5_6 432 # ASSIGN : s_6_0 349 # ASSIGN : s_6_1 318 # ASSIGN : s_6_2 7 # ASSIGN : s_6_3 254 # ASSIGN : s_6_4 192 # ASSIGN : s_6_5 442 # ASSIGN : s_6_6 100 SHOW_RESULT 459 END : 459 (0 seconds) [Mon Jun 19 23:19:07 2006] SHOW_RESULT 459 CPU : 0.0499999999999989 = 0.0499999999999989 + 0 + 0 + 0 # BOUND : makespan 458 459 MODIFY_CNF 458 BEGIN : [Mon Jun 19 23:19:07 2006] MODIFY_CNF 458 END : 7871398 bytes (0 seconds) [Mon Jun 19 23:19:07 2006] MODIFY_CNF 458 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 458 BEGIN : [Mon Jun 19 23:19:07 2006] CMD : minisat /tmp/csp2sat14077.cnf /tmp/csp2sat14077.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 276926 800275 | 92308 0 0 nan | 0.000 % | | 100 | 276926 800275 | 101538 100 3081 30.8 | 36.465 % | | 250 | 276926 800275 | 111692 250 4712 18.8 | 36.465 % | ============================================================================== restarts : 3 conflicts : 333 (358 /sec) decisions : 603 (648 /sec) propagations : 571279 (614278 /sec) conflict literals : 5812 (9.61 % deleted) Memory used : 18.56 MB CPU time : 0.93 s SATISFIABLE VERIFY_CNF 458 END : (1 seconds) [Mon Jun 19 23:19:08 2006] VERIFY_CNF 458 CPU : 1.01 = 0 + 0 + 0.95 + 0.06 # RESULT : makespan 458 SATISFIABLE SHOW_RESULT 458 BEGIN : [Mon Jun 19 23:19:08 2006] # ASSIGN : makespan 458 # ASSIGN : s_0_0 342 # ASSIGN : s_0_1 3 # ASSIGN : s_0_2 187 # ASSIGN : s_0_3 71 # ASSIGN : s_0_4 374 # ASSIGN : s_0_5 260 # ASSIGN : s_0_6 127 # ASSIGN : s_1_0 379 # ASSIGN : s_1_1 140 # ASSIGN : s_1_2 219 # ASSIGN : s_1_3 392 # ASSIGN : s_1_4 291 # ASSIGN : s_1_5 332 # ASSIGN : s_1_6 67 # ASSIGN : s_2_0 23 # ASSIGN : s_2_1 252 # ASSIGN : s_2_2 435 # ASSIGN : s_2_3 114 # ASSIGN : s_2_4 164 # ASSIGN : s_2_5 179 # ASSIGN : s_2_6 158 # ASSIGN : s_3_0 69 # ASSIGN : s_3_1 346 # ASSIGN : s_3_2 254 # ASSIGN : s_3_3 159 # ASSIGN : s_3_4 0 # ASSIGN : s_3_5 396 # ASSIGN : s_3_6 438 # ASSIGN : s_4_0 394 # ASSIGN : s_4_1 212 # ASSIGN : s_4_2 0 # ASSIGN : s_4_3 317 # ASSIGN : s_4_4 445 # ASSIGN : s_4_5 86 # ASSIGN : s_4_6 249 # ASSIGN : s_5_0 160 # ASSIGN : s_5_1 411 # ASSIGN : s_5_2 346 # ASSIGN : s_5_3 255 # ASSIGN : s_5_4 97 # ASSIGN : s_5_5 4 # ASSIGN : s_5_6 319 # ASSIGN : s_6_0 249 # ASSIGN : s_6_1 70 # ASSIGN : s_6_2 101 # ASSIGN : s_6_3 6 # ASSIGN : s_6_4 187 # ASSIGN : s_6_5 441 # ASSIGN : s_6_6 346 SHOW_RESULT 458 END : 458 (0 seconds) [Mon Jun 19 23:19:08 2006] SHOW_RESULT 458 CPU : 0.0400000000000009 = 0.0400000000000009 + 0 + 0 + 0 # BOUND : makespan 458 458 MAIN END : (21 seconds) [Mon Jun 19 23:19:08 2006] MAIN CPU : 21 = 15.44 + 0.04 + 5.17 + 0.35