# TIMEOUT 18000 MAIN BEGIN : [Mon Jun 19 23:18:27 2006] READ BEGIN : csp/tai_7x7_8.csp [Mon Jun 19 23:18:27 2006] READ END : csp/tai_7x7_8.csp (0 seconds) [Mon Jun 19 23:18:27 2006] READ CPU : 0.63 = 0.63 + 0 + 0 + 0 # BOUND : makespan 424 611 GENERATE_CNF 611 BEGIN : [Mon Jun 19 23:18:27 2006] GENERATE_CNF 611 END : 30863 variables 370287 clauses 7648724 bytes (15 seconds) [Mon Jun 19 23:18:42 2006] GENERATE_CNF 611 CPU : 14.03 = 13.96 + 0.07 + 0 + 0 MODIFY_CNF 517 BEGIN : [Mon Jun 19 23:18:42 2006] MODIFY_CNF 517 END : 7648729 bytes (0 seconds) [Mon Jun 19 23:18:42 2006] MODIFY_CNF 517 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 517 BEGIN : [Mon Jun 19 23:18:42 2006] CMD : minisat /tmp/csp2sat14064.cnf /tmp/csp2sat14064.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 314079 912803 | 104693 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 1 (2 /sec) decisions : 144 (320 /sec) propagations : 34083 (75740 /sec) conflict literals : 4 (0.00 % deleted) Memory used : 18.01 MB CPU time : 0.45 s SATISFIABLE VERIFY_CNF 517 END : (0 seconds) [Mon Jun 19 23:18:42 2006] VERIFY_CNF 517 CPU : 0.54 = 0 + 0 + 0.46 + 0.08 # RESULT : makespan 517 SATISFIABLE SHOW_RESULT 517 BEGIN : [Mon Jun 19 23:18:42 2006] # ASSIGN : makespan 517 # ASSIGN : s_0_0 237 # ASSIGN : s_0_1 380 # ASSIGN : s_0_2 400 # ASSIGN : s_0_3 420 # ASSIGN : s_0_4 107 # ASSIGN : s_0_5 15 # ASSIGN : s_0_6 1 # ASSIGN : s_1_0 334 # ASSIGN : s_1_1 242 # ASSIGN : s_1_2 419 # ASSIGN : s_1_3 456 # ASSIGN : s_1_4 190 # ASSIGN : s_1_5 107 # ASSIGN : s_1_6 22 # ASSIGN : s_2_0 9 # ASSIGN : s_2_1 188 # ASSIGN : s_2_2 14 # ASSIGN : s_2_3 25 # ASSIGN : s_2_4 238 # ASSIGN : s_2_5 187 # ASSIGN : s_2_6 77 # ASSIGN : s_3_0 136 # ASSIGN : s_3_1 284 # ASSIGN : s_3_2 29 # ASSIGN : s_3_3 97 # ASSIGN : s_3_4 380 # ASSIGN : s_3_5 201 # ASSIGN : s_3_6 174 # ASSIGN : s_4_0 78 # ASSIGN : s_4_1 17 # ASSIGN : s_4_2 147 # ASSIGN : s_4_3 130 # ASSIGN : s_4_4 459 # ASSIGN : s_4_5 309 # ASSIGN : s_4_6 243 # ASSIGN : s_5_0 419 # ASSIGN : s_5_1 78 # ASSIGN : s_5_2 219 # ASSIGN : s_5_3 147 # ASSIGN : s_5_4 295 # ASSIGN : s_5_5 390 # ASSIGN : s_5_6 297 # ASSIGN : s_6_0 388 # ASSIGN : s_6_1 95 # ASSIGN : s_6_2 237 # ASSIGN : s_6_3 153 # ASSIGN : s_6_4 299 # ASSIGN : s_6_5 411 # ASSIGN : s_6_6 437 SHOW_RESULT 517 END : 517 (0 seconds) [Mon Jun 19 23:18:42 2006] SHOW_RESULT 517 CPU : 0.0500000000000009 = 0.0400000000000009 + 0.01 + 0 + 0 # BOUND : makespan 424 517 MODIFY_CNF 470 BEGIN : [Mon Jun 19 23:18:42 2006] MODIFY_CNF 470 END : 7648729 bytes (0 seconds) [Mon Jun 19 23:18:42 2006] MODIFY_CNF 470 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 470 BEGIN : [Mon Jun 19 23:18:42 2006] CMD : minisat /tmp/csp2sat14064.cnf /tmp/csp2sat14064.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 286443 829895 | 95481 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 5 (12 /sec) decisions : 117 (272 /sec) propagations : 38115 (88640 /sec) conflict literals : 45 (2.17 % deleted) Memory used : 18.03 MB CPU time : 0.43 s SATISFIABLE VERIFY_CNF 470 END : (1 seconds) [Mon Jun 19 23:18:43 2006] VERIFY_CNF 470 CPU : 0.53 = 0 + 0 + 0.44 + 0.09 # RESULT : makespan 470 SATISFIABLE SHOW_RESULT 470 BEGIN : [Mon Jun 19 23:18:43 2006] # ASSIGN : makespan 470 # ASSIGN : s_0_0 193 # ASSIGN : s_0_1 137 # ASSIGN : s_0_2 118 # ASSIGN : s_0_3 157 # ASSIGN : s_0_4 387 # ASSIGN : s_0_5 26 # ASSIGN : s_0_6 3 # ASSIGN : s_1_0 416 # ASSIGN : s_1_1 264 # ASSIGN : s_1_2 365 # ASSIGN : s_1_3 72 # ASSIGN : s_1_4 216 # ASSIGN : s_1_5 133 # ASSIGN : s_1_6 17 # ASSIGN : s_2_0 411 # ASSIGN : s_2_1 214 # ASSIGN : s_2_2 82 # ASSIGN : s_2_3 418 # ASSIGN : s_2_4 16 # ASSIGN : s_2_5 213 # ASSIGN : s_2_6 93 # ASSIGN : s_3_0 152 # ASSIGN : s_3_1 306 # ASSIGN : s_3_2 402 # ASSIGN : s_3_3 39 # ASSIGN : s_3_4 73 # ASSIGN : s_3_5 223 # ASSIGN : s_3_6 190 # ASSIGN : s_4_0 290 # ASSIGN : s_4_1 76 # ASSIGN : s_4_2 4 # ASSIGN : s_4_3 140 # ASSIGN : s_4_4 158 # ASSIGN : s_4_5 342 # ASSIGN : s_4_6 217 # ASSIGN : s_5_0 2 # ASSIGN : s_5_1 176 # ASSIGN : s_5_2 100 # ASSIGN : s_5_3 193 # ASSIGN : s_5_4 269 # ASSIGN : s_5_5 423 # ASSIGN : s_5_6 271 # ASSIGN : s_6_0 114 # ASSIGN : s_6_1 18 # ASSIGN : s_6_2 137 # ASSIGN : s_6_3 199 # ASSIGN : s_6_4 283 # ASSIGN : s_6_5 444 # ASSIGN : s_6_6 364 SHOW_RESULT 470 END : 470 (0 seconds) [Mon Jun 19 23:18:43 2006] SHOW_RESULT 470 CPU : 0.0399999999999991 = 0.0399999999999991 + 0 + 0 + 0 # BOUND : makespan 424 470 MODIFY_CNF 447 BEGIN : [Mon Jun 19 23:18:43 2006] MODIFY_CNF 447 END : 7648729 bytes (0 seconds) [Mon Jun 19 23:18:43 2006] MODIFY_CNF 447 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 447 BEGIN : [Mon Jun 19 23:18:43 2006] CMD : minisat /tmp/csp2sat14064.cnf /tmp/csp2sat14064.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 272919 789323 | 90973 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 7 (15 /sec) decisions : 133 (277 /sec) propagations : 46977 (97869 /sec) conflict literals : 44 (12.00 % deleted) Memory used : 18.03 MB CPU time : 0.48 s SATISFIABLE VERIFY_CNF 447 END : (0 seconds) [Mon Jun 19 23:18:43 2006] VERIFY_CNF 447 CPU : 0.54 = 0 + 0 + 0.5 + 0.04 # RESULT : makespan 447 SATISFIABLE SHOW_RESULT 447 BEGIN : [Mon Jun 19 23:18:43 2006] # ASSIGN : makespan 447 # ASSIGN : s_0_0 267 # ASSIGN : s_0_1 235 # ASSIGN : s_0_2 180 # ASSIGN : s_0_3 199 # ASSIGN : s_0_4 364 # ASSIGN : s_0_5 46 # ASSIGN : s_0_6 1 # ASSIGN : s_1_0 393 # ASSIGN : s_1_1 78 # ASSIGN : s_1_2 218 # ASSIGN : s_1_3 255 # ASSIGN : s_1_4 316 # ASSIGN : s_1_5 138 # ASSIGN : s_1_6 15 # ASSIGN : s_2_0 39 # ASSIGN : s_2_1 182 # ASSIGN : s_2_2 1 # ASSIGN : s_2_3 345 # ASSIGN : s_2_4 259 # ASSIGN : s_2_5 232 # ASSIGN : s_2_6 70 # ASSIGN : s_3_0 195 # ASSIGN : s_3_1 318 # ASSIGN : s_3_2 84 # ASSIGN : s_3_3 414 # ASSIGN : s_3_4 5 # ASSIGN : s_3_5 233 # ASSIGN : s_3_6 167 # ASSIGN : s_4_0 142 # ASSIGN : s_4_1 255 # ASSIGN : s_4_2 12 # ASSIGN : s_4_3 397 # ASSIGN : s_4_4 84 # ASSIGN : s_4_5 316 # ASSIGN : s_4_6 194 # ASSIGN : s_5_0 44 # ASSIGN : s_5_1 27 # ASSIGN : s_5_2 152 # ASSIGN : s_5_3 170 # ASSIGN : s_5_4 176 # ASSIGN : s_5_5 400 # ASSIGN : s_5_6 248 # ASSIGN : s_6_0 13 # ASSIGN : s_6_1 120 # ASSIGN : s_6_2 279 # ASSIGN : s_6_3 36 # ASSIGN : s_6_4 178 # ASSIGN : s_6_5 421 # ASSIGN : s_6_6 341 SHOW_RESULT 447 END : 447 (0 seconds) [Mon Jun 19 23:18:43 2006] SHOW_RESULT 447 CPU : 0.0399999999999991 = 0.0399999999999991 + 0 + 0 + 0 # BOUND : makespan 424 447 MODIFY_CNF 435 BEGIN : [Mon Jun 19 23:18:43 2006] MODIFY_CNF 435 END : 7648729 bytes (0 seconds) [Mon Jun 19 23:18:43 2006] MODIFY_CNF 435 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 435 BEGIN : [Mon Jun 19 23:18:43 2006] CMD : minisat /tmp/csp2sat14064.cnf /tmp/csp2sat14064.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 265863 768155 | 88621 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 11 (23 /sec) decisions : 102 (212 /sec) propagations : 53134 (110696 /sec) conflict literals : 276 (1.43 % deleted) Memory used : 18.03 MB CPU time : 0.48 s SATISFIABLE VERIFY_CNF 435 END : (1 seconds) [Mon Jun 19 23:18:44 2006] VERIFY_CNF 435 CPU : 0.54 = 0 + 0 + 0.5 + 0.04 # RESULT : makespan 435 SATISFIABLE SHOW_RESULT 435 BEGIN : [Mon Jun 19 23:18:44 2006] # ASSIGN : makespan 435 # ASSIGN : s_0_0 103 # ASSIGN : s_0_1 25 # ASSIGN : s_0_2 225 # ASSIGN : s_0_3 45 # ASSIGN : s_0_4 247 # ASSIGN : s_0_5 343 # ASSIGN : s_0_6 7 # ASSIGN : s_1_0 381 # ASSIGN : s_1_1 123 # ASSIGN : s_1_2 86 # ASSIGN : s_1_3 165 # ASSIGN : s_1_4 330 # ASSIGN : s_1_5 226 # ASSIGN : s_1_6 21 # ASSIGN : s_2_0 321 # ASSIGN : s_2_1 177 # ASSIGN : s_2_2 8 # ASSIGN : s_2_3 326 # ASSIGN : s_2_4 378 # ASSIGN : s_2_5 1 # ASSIGN : s_2_6 76 # ASSIGN : s_3_0 200 # ASSIGN : s_3_1 339 # ASSIGN : s_3_2 271 # ASSIGN : s_3_3 238 # ASSIGN : s_3_4 85 # ASSIGN : s_3_5 2 # ASSIGN : s_3_6 173 # ASSIGN : s_4_0 269 # ASSIGN : s_4_1 62 # ASSIGN : s_4_2 346 # ASSIGN : s_4_3 418 # ASSIGN : s_4_4 4 # ASSIGN : s_4_5 124 # ASSIGN : s_4_6 208 # ASSIGN : s_5_0 5 # ASSIGN : s_5_1 227 # ASSIGN : s_5_2 244 # ASSIGN : s_5_3 412 # ASSIGN : s_5_4 164 # ASSIGN : s_5_5 205 # ASSIGN : s_5_6 262 # ASSIGN : s_6_0 332 # ASSIGN : s_6_1 248 # ASSIGN : s_6_2 19 # ASSIGN : s_6_3 81 # ASSIGN : s_6_4 166 # ASSIGN : s_6_5 306 # ASSIGN : s_6_6 355 SHOW_RESULT 435 END : 435 (0 seconds) [Mon Jun 19 23:18:44 2006] SHOW_RESULT 435 CPU : 0.0399999999999991 = 0.0399999999999991 + 0 + 0 + 0 # BOUND : makespan 424 435 MODIFY_CNF 429 BEGIN : [Mon Jun 19 23:18:44 2006] MODIFY_CNF 429 END : 7648728 bytes (0 seconds) [Mon Jun 19 23:18:44 2006] MODIFY_CNF 429 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 429 BEGIN : [Mon Jun 19 23:18:44 2006] CMD : minisat /tmp/csp2sat14064.cnf /tmp/csp2sat14064.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 262335 757571 | 87445 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 15 (29 /sec) decisions : 112 (215 /sec) propagations : 52866 (101665 /sec) conflict literals : 156 (7.69 % deleted) Memory used : 18.03 MB CPU time : 0.52 s SATISFIABLE VERIFY_CNF 429 END : (0 seconds) [Mon Jun 19 23:18:44 2006] VERIFY_CNF 429 CPU : 0.59 = 0 + 0 + 0.53 + 0.06 # RESULT : makespan 429 SATISFIABLE SHOW_RESULT 429 BEGIN : [Mon Jun 19 23:18:44 2006] # ASSIGN : makespan 429 # ASSIGN : s_0_0 105 # ASSIGN : s_0_1 216 # ASSIGN : s_0_2 21 # ASSIGN : s_0_3 40 # ASSIGN : s_0_4 236 # ASSIGN : s_0_5 336 # ASSIGN : s_0_6 1 # ASSIGN : s_1_0 202 # ASSIGN : s_1_1 160 # ASSIGN : s_1_2 344 # ASSIGN : s_1_3 76 # ASSIGN : s_1_4 381 # ASSIGN : s_1_5 256 # ASSIGN : s_1_6 15 # ASSIGN : s_2_0 2 # ASSIGN : s_2_1 20 # ASSIGN : s_2_2 9 # ASSIGN : s_2_3 376 # ASSIGN : s_2_4 179 # ASSIGN : s_2_5 428 # ASSIGN : s_2_6 70 # ASSIGN : s_3_0 295 # ASSIGN : s_3_1 333 # ASSIGN : s_3_2 194 # ASSIGN : s_3_3 262 # ASSIGN : s_3_4 88 # ASSIGN : s_3_5 5 # ASSIGN : s_3_6 167 # ASSIGN : s_4_0 377 # ASSIGN : s_4_1 258 # ASSIGN : s_4_2 47 # ASSIGN : s_4_3 23 # ASSIGN : s_4_4 319 # ASSIGN : s_4_5 121 # ASSIGN : s_4_6 202 # ASSIGN : s_5_0 7 # ASSIGN : s_5_1 143 # ASSIGN : s_5_2 119 # ASSIGN : s_5_3 137 # ASSIGN : s_5_4 177 # ASSIGN : s_5_5 209 # ASSIGN : s_5_6 256 # ASSIGN : s_6_0 259 # ASSIGN : s_6_1 85 # ASSIGN : s_6_2 282 # ASSIGN : s_6_3 146 # ASSIGN : s_6_4 4 # ASSIGN : s_6_5 230 # ASSIGN : s_6_6 349 SHOW_RESULT 429 END : 429 (1 seconds) [Mon Jun 19 23:18:45 2006] SHOW_RESULT 429 CPU : 0.0700000000000003 = 0.0700000000000003 + 0 + 0 + 0 # BOUND : makespan 424 429 MODIFY_CNF 426 BEGIN : [Mon Jun 19 23:18:45 2006] MODIFY_CNF 426 END : 7648728 bytes (0 seconds) [Mon Jun 19 23:18:45 2006] MODIFY_CNF 426 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 426 BEGIN : [Mon Jun 19 23:18:45 2006] CMD : minisat /tmp/csp2sat14064.cnf /tmp/csp2sat14064.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 260571 752279 | 86857 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 82 (137 /sec) decisions : 195 (325 /sec) propagations : 144243 (240405 /sec) conflict literals : 1058 (5.79 % deleted) Memory used : 18.03 MB CPU time : 0.6 s SATISFIABLE VERIFY_CNF 426 END : (0 seconds) [Mon Jun 19 23:18:45 2006] VERIFY_CNF 426 CPU : 0.68 = 0 + 0 + 0.62 + 0.06 # RESULT : makespan 426 SATISFIABLE SHOW_RESULT 426 BEGIN : [Mon Jun 19 23:18:45 2006] # ASSIGN : makespan 426 # ASSIGN : s_0_0 329 # ASSIGN : s_0_1 213 # ASSIGN : s_0_2 64 # ASSIGN : s_0_3 177 # ASSIGN : s_0_4 246 # ASSIGN : s_0_5 83 # ASSIGN : s_0_6 3 # ASSIGN : s_1_0 275 # ASSIGN : s_1_1 233 # ASSIGN : s_1_2 196 # ASSIGN : s_1_3 75 # ASSIGN : s_1_4 141 # ASSIGN : s_1_5 346 # ASSIGN : s_1_6 17 # ASSIGN : s_2_0 263 # ASSIGN : s_2_1 353 # ASSIGN : s_2_2 268 # ASSIGN : s_2_3 20 # ASSIGN : s_2_4 189 # ASSIGN : s_2_5 319 # ASSIGN : s_2_6 72 # ASSIGN : s_3_0 98 # ASSIGN : s_3_1 2 # ASSIGN : s_3_2 279 # ASSIGN : s_3_3 136 # ASSIGN : s_3_4 347 # ASSIGN : s_3_5 196 # ASSIGN : s_3_6 169 # ASSIGN : s_4_0 146 # ASSIGN : s_4_1 276 # ASSIGN : s_4_2 354 # ASSIGN : s_4_3 337 # ASSIGN : s_4_4 83 # ASSIGN : s_4_5 2 # ASSIGN : s_4_6 198 # ASSIGN : s_5_0 0 # ASSIGN : s_5_1 403 # ASSIGN : s_5_2 234 # ASSIGN : s_5_3 420 # ASSIGN : s_5_4 345 # ASSIGN : s_5_5 175 # ASSIGN : s_5_6 252 # ASSIGN : s_6_0 213 # ASSIGN : s_6_1 155 # ASSIGN : s_6_2 93 # ASSIGN : s_6_3 236 # ASSIGN : s_6_4 2 # ASSIGN : s_6_5 320 # ASSIGN : s_6_6 346 SHOW_RESULT 426 END : 426 (0 seconds) [Mon Jun 19 23:18:45 2006] SHOW_RESULT 426 CPU : 0.0400000000000009 = 0.0400000000000009 + 0 + 0 + 0 # BOUND : makespan 424 426 MODIFY_CNF 425 BEGIN : [Mon Jun 19 23:18:45 2006] MODIFY_CNF 425 END : 7648728 bytes (0 seconds) [Mon Jun 19 23:18:45 2006] MODIFY_CNF 425 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 425 BEGIN : [Mon Jun 19 23:18:45 2006] CMD : minisat /tmp/csp2sat14064.cnf /tmp/csp2sat14064.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 259983 750515 | 86661 0 0 nan | 0.000 % | | 100 | 259983 750515 | 95327 100 1521 15.2 | 38.713 % | ============================================================================== restarts : 2 conflicts : 152 (227 /sec) decisions : 332 (496 /sec) propagations : 264428 (394669 /sec) conflict literals : 2348 (10.55 % deleted) Memory used : 18.05 MB CPU time : 0.67 s SATISFIABLE VERIFY_CNF 425 END : (1 seconds) [Mon Jun 19 23:18:46 2006] VERIFY_CNF 425 CPU : 0.77 = 0 + 0 + 0.68 + 0.09 # RESULT : makespan 425 SATISFIABLE SHOW_RESULT 425 BEGIN : [Mon Jun 19 23:18:46 2006] # ASSIGN : makespan 425 # ASSIGN : s_0_0 127 # ASSIGN : s_0_1 87 # ASSIGN : s_0_2 406 # ASSIGN : s_0_3 35 # ASSIGN : s_0_4 224 # ASSIGN : s_0_5 307 # ASSIGN : s_0_6 109 # ASSIGN : s_1_0 258 # ASSIGN : s_1_1 215 # ASSIGN : s_1_2 117 # ASSIGN : s_1_3 154 # ASSIGN : s_1_4 320 # ASSIGN : s_1_5 1 # ASSIGN : s_1_6 370 # ASSIGN : s_2_0 253 # ASSIGN : s_2_1 21 # ASSIGN : s_2_2 357 # ASSIGN : s_2_3 71 # ASSIGN : s_2_4 368 # ASSIGN : s_2_5 0 # ASSIGN : s_2_6 123 # ASSIGN : s_3_0 387 # ASSIGN : s_3_1 107 # ASSIGN : s_3_2 286 # ASSIGN : s_3_3 354 # ASSIGN : s_3_4 1 # ASSIGN : s_3_5 203 # ASSIGN : s_3_6 80 # ASSIGN : s_4_0 335 # ASSIGN : s_4_1 274 # ASSIGN : s_4_2 9 # ASSIGN : s_4_3 402 # ASSIGN : s_4_4 162 # ASSIGN : s_4_5 81 # ASSIGN : s_4_6 220 # ASSIGN : s_5_0 29 # ASSIGN : s_5_1 257 # ASSIGN : s_5_2 388 # ASSIGN : s_5_3 419 # ASSIGN : s_5_4 222 # ASSIGN : s_5_5 182 # ASSIGN : s_5_6 277 # ASSIGN : s_6_0 312 # ASSIGN : s_6_1 341 # ASSIGN : s_6_2 166 # ASSIGN : s_6_3 228 # ASSIGN : s_6_4 81 # ASSIGN : s_6_5 399 # ASSIGN : s_6_6 0 SHOW_RESULT 425 END : 425 (0 seconds) [Mon Jun 19 23:18:46 2006] SHOW_RESULT 425 CPU : 0.0399999999999991 = 0.0399999999999991 + 0 + 0 + 0 # BOUND : makespan 424 425 MODIFY_CNF 424 BEGIN : [Mon Jun 19 23:18:46 2006] MODIFY_CNF 424 END : 7648728 bytes (0 seconds) [Mon Jun 19 23:18:46 2006] MODIFY_CNF 424 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 424 BEGIN : [Mon Jun 19 23:18:46 2006] CMD : minisat /tmp/csp2sat14064.cnf /tmp/csp2sat14064.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 259396 748751 | 86465 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 69 (121 /sec) decisions : 175 (307 /sec) propagations : 118781 (208388 /sec) conflict literals : 867 (6.47 % deleted) Memory used : 18.03 MB CPU time : 0.57 s SATISFIABLE VERIFY_CNF 424 END : (1 seconds) [Mon Jun 19 23:18:47 2006] VERIFY_CNF 424 CPU : 0.62 = 0 + 0 + 0.59 + 0.03 # RESULT : makespan 424 SATISFIABLE SHOW_RESULT 424 BEGIN : [Mon Jun 19 23:18:47 2006] # ASSIGN : makespan 424 # ASSIGN : s_0_0 236 # ASSIGN : s_0_1 18 # ASSIGN : s_0_2 65 # ASSIGN : s_0_3 200 # ASSIGN : s_0_4 341 # ASSIGN : s_0_5 108 # ASSIGN : s_0_6 1 # ASSIGN : s_1_0 333 # ASSIGN : s_1_1 211 # ASSIGN : s_1_2 387 # ASSIGN : s_1_3 73 # ASSIGN : s_1_4 157 # ASSIGN : s_1_5 253 # ASSIGN : s_1_6 15 # ASSIGN : s_2_0 419 # ASSIGN : s_2_1 351 # ASSIGN : s_2_2 304 # ASSIGN : s_2_3 18 # ASSIGN : s_2_4 205 # ASSIGN : s_2_5 340 # ASSIGN : s_2_6 70 # ASSIGN : s_3_0 0 # ASSIGN : s_3_1 38 # ASSIGN : s_3_2 194 # ASSIGN : s_3_3 134 # ASSIGN : s_3_4 262 # ASSIGN : s_3_5 341 # ASSIGN : s_3_6 167 # ASSIGN : s_4_0 145 # ASSIGN : s_4_1 254 # ASSIGN : s_4_2 315 # ASSIGN : s_4_3 401 # ASSIGN : s_4_4 87 # ASSIGN : s_4_5 6 # ASSIGN : s_4_6 197 # ASSIGN : s_5_0 47 # ASSIGN : s_5_1 401 # ASSIGN : s_5_2 176 # ASSIGN : s_5_3 418 # ASSIGN : s_5_4 1 # ASSIGN : s_5_5 206 # ASSIGN : s_5_6 251 # ASSIGN : s_6_0 204 # ASSIGN : s_6_1 146 # ASSIGN : s_6_2 84 # ASSIGN : s_6_3 260 # ASSIGN : s_6_4 3 # ASSIGN : s_6_5 227 # ASSIGN : s_6_6 344 SHOW_RESULT 424 END : 424 (0 seconds) [Mon Jun 19 23:18:47 2006] SHOW_RESULT 424 CPU : 0.0500000000000007 = 0.0500000000000007 + 0 + 0 + 0 # BOUND : makespan 424 424 MAIN END : (20 seconds) [Mon Jun 19 23:18:47 2006] MAIN CPU : 19.86 = 14.97 + 0.08 + 4.32 + 0.49