# TIMEOUT 18000 MAIN BEGIN : [Mon Jun 19 23:16:25 2006] READ BEGIN : csp/tai_7x7_4.csp [Mon Jun 19 23:16:25 2006] READ END : csp/tai_7x7_4.csp (1 seconds) [Mon Jun 19 23:16:26 2006] READ CPU : 0.65 = 0.64 + 0.01 + 0 + 0 # BOUND : makespan 463 619 GENERATE_CNF 619 BEGIN : [Mon Jun 19 23:16:26 2006] GENERATE_CNF 619 END : 31224 variables 370305 clauses 7651018 bytes (14 seconds) [Mon Jun 19 23:16:40 2006] GENERATE_CNF 619 CPU : 14.11 = 14.07 + 0.04 + 0 + 0 MODIFY_CNF 541 BEGIN : [Mon Jun 19 23:16:40 2006] MODIFY_CNF 541 END : 7651023 bytes (0 seconds) [Mon Jun 19 23:16:40 2006] MODIFY_CNF 541 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 541 BEGIN : [Mon Jun 19 23:16:40 2006] CMD : minisat /tmp/csp2sat14006.cnf /tmp/csp2sat14006.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 323505 940720 | 107835 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 3 (6 /sec) decisions : 148 (285 /sec) propagations : 36279 (69767 /sec) conflict literals : 20 (0.00 % deleted) Memory used : 18.05 MB CPU time : 0.52 s SATISFIABLE VERIFY_CNF 541 END : (1 seconds) [Mon Jun 19 23:16:41 2006] VERIFY_CNF 541 CPU : 0.55 = 0 + 0 + 0.54 + 0.01 # RESULT : makespan 541 SATISFIABLE SHOW_RESULT 541 BEGIN : [Mon Jun 19 23:16:41 2006] # ASSIGN : makespan 541 # ASSIGN : s_0_0 414 # ASSIGN : s_0_1 299 # ASSIGN : s_0_2 230 # ASSIGN : s_0_3 340 # ASSIGN : s_0_4 144 # ASSIGN : s_0_5 96 # ASSIGN : s_0_6 1 # ASSIGN : s_1_0 335 # ASSIGN : s_1_1 1 # ASSIGN : s_1_2 395 # ASSIGN : s_1_3 444 # ASSIGN : s_1_4 49 # ASSIGN : s_1_5 146 # ASSIGN : s_1_6 96 # ASSIGN : s_2_0 464 # ASSIGN : s_2_1 344 # ASSIGN : s_2_2 85 # ASSIGN : s_2_3 1 # ASSIGN : s_2_4 400 # ASSIGN : s_2_5 207 # ASSIGN : s_2_6 147 # ASSIGN : s_3_0 378 # ASSIGN : s_3_1 459 # ASSIGN : s_3_2 14 # ASSIGN : s_3_3 79 # ASSIGN : s_3_4 450 # ASSIGN : s_3_5 289 # ASSIGN : s_3_6 165 # ASSIGN : s_4_0 18 # ASSIGN : s_4_1 174 # ASSIGN : s_4_2 416 # ASSIGN : s_4_3 147 # ASSIGN : s_4_4 493 # ASSIGN : s_4_5 339 # ASSIGN : s_4_6 252 # ASSIGN : s_5_0 257 # ASSIGN : s_5_1 54 # ASSIGN : s_5_2 187 # ASSIGN : s_5_3 201 # ASSIGN : s_5_4 261 # ASSIGN : s_5_5 409 # ASSIGN : s_5_6 298 # ASSIGN : s_6_0 116 # ASSIGN : s_6_1 86 # ASSIGN : s_6_2 193 # ASSIGN : s_6_3 257 # ASSIGN : s_6_4 311 # ASSIGN : s_6_5 459 # ASSIGN : s_6_6 384 SHOW_RESULT 541 END : 541 (0 seconds) [Mon Jun 19 23:16:41 2006] SHOW_RESULT 541 CPU : 0.0399999999999994 = 0.0299999999999994 + 0.01 + 0 + 0 # BOUND : makespan 463 541 MODIFY_CNF 502 BEGIN : [Mon Jun 19 23:16:41 2006] MODIFY_CNF 502 END : 7651023 bytes (0 seconds) [Mon Jun 19 23:16:41 2006] MODIFY_CNF 502 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 502 BEGIN : [Mon Jun 19 23:16:41 2006] CMD : minisat /tmp/csp2sat14006.cnf /tmp/csp2sat14006.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 300573 871924 | 100191 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 4 (9 /sec) decisions : 122 (260 /sec) propagations : 40499 (86168 /sec) conflict literals : 77 (2.53 % deleted) Memory used : 18.11 MB CPU time : 0.47 s SATISFIABLE VERIFY_CNF 502 END : (1 seconds) [Mon Jun 19 23:16:42 2006] VERIFY_CNF 502 CPU : 0.55 = 0.00999999999999979 + 0 + 0.49 + 0.05 # RESULT : makespan 502 SATISFIABLE SHOW_RESULT 502 BEGIN : [Mon Jun 19 23:16:42 2006] # ASSIGN : makespan 502 # ASSIGN : s_0_0 186 # ASSIGN : s_0_1 327 # ASSIGN : s_0_2 117 # ASSIGN : s_0_3 253 # ASSIGN : s_0_4 368 # ASSIGN : s_0_5 454 # ASSIGN : s_0_6 22 # ASSIGN : s_1_0 236 # ASSIGN : s_1_1 279 # ASSIGN : s_1_2 384 # ASSIGN : s_1_3 405 # ASSIGN : s_1_4 71 # ASSIGN : s_1_5 1 # ASSIGN : s_1_6 118 # ASSIGN : s_2_0 425 # ASSIGN : s_2_1 186 # ASSIGN : s_2_2 257 # ASSIGN : s_2_3 327 # ASSIGN : s_2_4 12 # ASSIGN : s_2_5 62 # ASSIGN : s_2_6 168 # ASSIGN : s_3_0 1 # ASSIGN : s_3_1 420 # ASSIGN : s_3_2 319 # ASSIGN : s_3_3 37 # ASSIGN : s_3_4 135 # ASSIGN : s_3_5 144 # ASSIGN : s_3_6 194 # ASSIGN : s_4_0 327 # ASSIGN : s_4_1 1 # ASSIGN : s_4_2 425 # ASSIGN : s_4_3 105 # ASSIGN : s_4_4 163 # ASSIGN : s_4_5 211 # ASSIGN : s_4_6 281 # ASSIGN : s_5_0 75 # ASSIGN : s_5_1 79 # ASSIGN : s_5_2 111 # ASSIGN : s_5_3 132 # ASSIGN : s_5_4 235 # ASSIGN : s_5_5 291 # ASSIGN : s_5_6 341 # ASSIGN : s_6_0 109 # ASSIGN : s_6_1 242 # ASSIGN : s_6_2 72 # ASSIGN : s_6_3 188 # ASSIGN : s_6_4 272 # ASSIGN : s_6_5 345 # ASSIGN : s_6_6 427 SHOW_RESULT 502 END : 502 (0 seconds) [Mon Jun 19 23:16:42 2006] SHOW_RESULT 502 CPU : 0.0400000000000011 = 0.0300000000000011 + 0.01 + 0 + 0 # BOUND : makespan 463 502 MODIFY_CNF 482 BEGIN : [Mon Jun 19 23:16:42 2006] MODIFY_CNF 482 END : 7651023 bytes (0 seconds) [Mon Jun 19 23:16:42 2006] MODIFY_CNF 482 CPU : 0.00999999999999979 = 0.00999999999999979 + 0 + 0 + 0 VERIFY_CNF 482 BEGIN : [Mon Jun 19 23:16:42 2006] CMD : minisat /tmp/csp2sat14006.cnf /tmp/csp2sat14006.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 288813 836644 | 96271 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 8 (18 /sec) decisions : 114 (259 /sec) propagations : 42875 (97443 /sec) conflict literals : 100 (1.96 % deleted) Memory used : 18.11 MB CPU time : 0.44 s SATISFIABLE VERIFY_CNF 482 END : (0 seconds) [Mon Jun 19 23:16:42 2006] VERIFY_CNF 482 CPU : 0.53 = 0 + 0 + 0.46 + 0.07 # RESULT : makespan 482 SATISFIABLE SHOW_RESULT 482 BEGIN : [Mon Jun 19 23:16:42 2006] # ASSIGN : makespan 482 # ASSIGN : s_0_0 180 # ASSIGN : s_0_1 307 # ASSIGN : s_0_2 111 # ASSIGN : s_0_3 233 # ASSIGN : s_0_4 348 # ASSIGN : s_0_5 434 # ASSIGN : s_0_6 2 # ASSIGN : s_1_0 439 # ASSIGN : s_1_1 162 # ASSIGN : s_1_2 9 # ASSIGN : s_1_3 307 # ASSIGN : s_1_4 30 # ASSIGN : s_1_5 210 # ASSIGN : s_1_6 97 # ASSIGN : s_2_0 230 # ASSIGN : s_2_1 91 # ASSIGN : s_2_2 342 # ASSIGN : s_2_3 404 # ASSIGN : s_2_4 165 # ASSIGN : s_2_5 4 # ASSIGN : s_2_6 147 # ASSIGN : s_3_0 138 # ASSIGN : s_3_1 368 # ASSIGN : s_3_2 277 # ASSIGN : s_3_3 9 # ASSIGN : s_3_4 77 # ASSIGN : s_3_5 86 # ASSIGN : s_3_6 174 # ASSIGN : s_4_0 307 # ASSIGN : s_4_1 10 # ASSIGN : s_4_2 405 # ASSIGN : s_4_3 206 # ASSIGN : s_4_4 88 # ASSIGN : s_4_5 136 # ASSIGN : s_4_6 261 # ASSIGN : s_5_0 101 # ASSIGN : s_5_1 450 # ASSIGN : s_5_2 105 # ASSIGN : s_5_3 150 # ASSIGN : s_5_4 215 # ASSIGN : s_5_5 271 # ASSIGN : s_5_6 321 # ASSIGN : s_6_0 19 # ASSIGN : s_6_1 222 # ASSIGN : s_6_2 185 # ASSIGN : s_6_3 96 # ASSIGN : s_6_4 252 # ASSIGN : s_6_5 325 # ASSIGN : s_6_6 407 SHOW_RESULT 482 END : 482 (0 seconds) [Mon Jun 19 23:16:42 2006] SHOW_RESULT 482 CPU : 0.0499999999999994 = 0.0299999999999994 + 0.02 + 0 + 0 # BOUND : makespan 463 482 MODIFY_CNF 472 BEGIN : [Mon Jun 19 23:16:42 2006] MODIFY_CNF 472 END : 7651023 bytes (0 seconds) [Mon Jun 19 23:16:42 2006] MODIFY_CNF 472 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 472 BEGIN : [Mon Jun 19 23:16:42 2006] CMD : minisat /tmp/csp2sat14006.cnf /tmp/csp2sat14006.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 282933 819004 | 94311 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (4 /sec) decisions : 83 (184 /sec) propagations : 33495 (74433 /sec) conflict literals : 17 (0.00 % deleted) Memory used : 18.11 MB CPU time : 0.45 s SATISFIABLE VERIFY_CNF 472 END : (1 seconds) [Mon Jun 19 23:16:43 2006] VERIFY_CNF 472 CPU : 0.55 = 0 + 0 + 0.47 + 0.08 # RESULT : makespan 472 SATISFIABLE SHOW_RESULT 472 BEGIN : [Mon Jun 19 23:16:43 2006] # ASSIGN : makespan 472 # ASSIGN : s_0_0 210 # ASSIGN : s_0_1 95 # ASSIGN : s_0_2 264 # ASSIGN : s_0_3 136 # ASSIGN : s_0_4 338 # ASSIGN : s_0_5 424 # ASSIGN : s_0_6 0 # ASSIGN : s_1_0 167 # ASSIGN : s_1_1 47 # ASSIGN : s_1_2 26 # ASSIGN : s_1_3 319 # ASSIGN : s_1_4 425 # ASSIGN : s_1_5 254 # ASSIGN : s_1_6 95 # ASSIGN : s_2_0 395 # ASSIGN : s_2_1 185 # ASSIGN : s_2_2 333 # ASSIGN : s_2_3 241 # ASSIGN : s_2_4 95 # ASSIGN : s_2_5 2 # ASSIGN : s_2_6 145 # ASSIGN : s_3_0 260 # ASSIGN : s_3_1 312 # ASSIGN : s_3_2 407 # ASSIGN : s_3_3 14 # ASSIGN : s_3_4 0 # ASSIGN : s_3_5 84 # ASSIGN : s_3_6 163 # ASSIGN : s_4_0 296 # ASSIGN : s_4_1 394 # ASSIGN : s_4_2 57 # ASSIGN : s_4_3 214 # ASSIGN : s_4_4 9 # ASSIGN : s_4_5 134 # ASSIGN : s_4_6 250 # ASSIGN : s_5_0 1 # ASSIGN : s_5_1 15 # ASSIGN : s_5_2 161 # ASSIGN : s_5_3 416 # ASSIGN : s_5_4 167 # ASSIGN : s_5_5 204 # ASSIGN : s_5_6 311 # ASSIGN : s_6_0 5 # ASSIGN : s_6_1 282 # ASSIGN : s_6_2 172 # ASSIGN : s_6_3 82 # ASSIGN : s_6_4 209 # ASSIGN : s_6_5 315 # ASSIGN : s_6_6 397 SHOW_RESULT 472 END : 472 (0 seconds) [Mon Jun 19 23:16:43 2006] SHOW_RESULT 472 CPU : 0.0500000000000007 = 0.0500000000000007 + 0 + 0 + 0 # BOUND : makespan 463 472 MODIFY_CNF 467 BEGIN : [Mon Jun 19 23:16:43 2006] MODIFY_CNF 467 END : 7651022 bytes (0 seconds) [Mon Jun 19 23:16:43 2006] MODIFY_CNF 467 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 467 BEGIN : [Mon Jun 19 23:16:43 2006] CMD : minisat /tmp/csp2sat14006.cnf /tmp/csp2sat14006.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 279993 810184 | 93331 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 50 (88 /sec) decisions : 164 (288 /sec) propagations : 144659 (253788 /sec) conflict literals : 1307 (7.11 % deleted) Memory used : 18.11 MB CPU time : 0.57 s SATISFIABLE VERIFY_CNF 467 END : (0 seconds) [Mon Jun 19 23:16:43 2006] VERIFY_CNF 467 CPU : 0.63 = 0 + 0 + 0.59 + 0.04 # RESULT : makespan 467 SATISFIABLE SHOW_RESULT 467 BEGIN : [Mon Jun 19 23:16:43 2006] # ASSIGN : makespan 467 # ASSIGN : s_0_0 340 # ASSIGN : s_0_1 96 # ASSIGN : s_0_2 185 # ASSIGN : s_0_3 393 # ASSIGN : s_0_4 254 # ASSIGN : s_0_5 137 # ASSIGN : s_0_6 1 # ASSIGN : s_1_0 297 # ASSIGN : s_1_1 341 # ASSIGN : s_1_2 32 # ASSIGN : s_1_3 150 # ASSIGN : s_1_4 53 # ASSIGN : s_1_5 406 # ASSIGN : s_1_6 100 # ASSIGN : s_2_0 390 # ASSIGN : s_2_1 168 # ASSIGN : s_2_2 88 # ASSIGN : s_2_3 247 # ASSIGN : s_2_4 340 # ASSIGN : s_2_5 5 # ASSIGN : s_2_6 150 # ASSIGN : s_3_0 261 # ASSIGN : s_3_1 5 # ASSIGN : s_3_2 402 # ASSIGN : s_3_3 325 # ASSIGN : s_3_4 393 # ASSIGN : s_3_5 87 # ASSIGN : s_3_6 173 # ASSIGN : s_4_0 88 # ASSIGN : s_4_1 389 # ASSIGN : s_4_2 312 # ASSIGN : s_4_3 57 # ASSIGN : s_4_4 5 # ASSIGN : s_4_5 186 # ASSIGN : s_4_6 260 # ASSIGN : s_5_0 84 # ASSIGN : s_5_1 224 # ASSIGN : s_5_2 78 # ASSIGN : s_5_3 1 # ASSIGN : s_5_4 144 # ASSIGN : s_5_5 256 # ASSIGN : s_5_6 306 # ASSIGN : s_6_0 7 # ASSIGN : s_6_1 138 # ASSIGN : s_6_2 273 # ASSIGN : s_6_3 84 # ASSIGN : s_6_4 181 # ASSIGN : s_6_5 310 # ASSIGN : s_6_6 392 SHOW_RESULT 467 END : 467 (0 seconds) [Mon Jun 19 23:16:43 2006] SHOW_RESULT 467 CPU : 0.0399999999999991 = 0.0399999999999991 + 0 + 0 + 0 # BOUND : makespan 463 467 MODIFY_CNF 465 BEGIN : [Mon Jun 19 23:16:43 2006] MODIFY_CNF 465 END : 7651022 bytes (0 seconds) [Mon Jun 19 23:16:43 2006] MODIFY_CNF 465 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 465 BEGIN : [Mon Jun 19 23:16:43 2006] CMD : minisat /tmp/csp2sat14006.cnf /tmp/csp2sat14006.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 278817 806656 | 92939 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 35 (66 /sec) decisions : 143 (270 /sec) propagations : 120759 (227847 /sec) conflict literals : 887 (7.12 % deleted) Memory used : 18.11 MB CPU time : 0.53 s SATISFIABLE VERIFY_CNF 465 END : (1 seconds) [Mon Jun 19 23:16:44 2006] VERIFY_CNF 465 CPU : 0.61 = 0 + 0 + 0.55 + 0.06 # RESULT : makespan 465 SATISFIABLE SHOW_RESULT 465 BEGIN : [Mon Jun 19 23:16:44 2006] # ASSIGN : makespan 465 # ASSIGN : s_0_0 186 # ASSIGN : s_0_1 95 # ASSIGN : s_0_2 236 # ASSIGN : s_0_3 391 # ASSIGN : s_0_4 305 # ASSIGN : s_0_5 136 # ASSIGN : s_0_6 0 # ASSIGN : s_1_0 341 # ASSIGN : s_1_1 280 # ASSIGN : s_1_2 30 # ASSIGN : s_1_3 148 # ASSIGN : s_1_4 51 # ASSIGN : s_1_5 404 # ASSIGN : s_1_6 98 # ASSIGN : s_2_0 384 # ASSIGN : s_2_1 328 # ASSIGN : s_2_2 174 # ASSIGN : s_2_3 245 # ASSIGN : s_2_4 103 # ASSIGN : s_2_5 4 # ASSIGN : s_2_6 153 # ASSIGN : s_3_0 287 # ASSIGN : s_3_1 4 # ASSIGN : s_3_2 400 # ASSIGN : s_3_3 323 # ASSIGN : s_3_4 391 # ASSIGN : s_3_5 86 # ASSIGN : s_3_6 171 # ASSIGN : s_4_0 86 # ASSIGN : s_4_1 387 # ASSIGN : s_4_2 310 # ASSIGN : s_4_3 56 # ASSIGN : s_4_4 3 # ASSIGN : s_4_5 184 # ASSIGN : s_4_6 258 # ASSIGN : s_5_0 461 # ASSIGN : s_5_1 163 # ASSIGN : s_5_2 394 # ASSIGN : s_5_3 0 # ASSIGN : s_5_4 195 # ASSIGN : s_5_5 254 # ASSIGN : s_5_6 304 # ASSIGN : s_6_0 6 # ASSIGN : s_6_1 202 # ASSIGN : s_6_2 137 # ASSIGN : s_6_3 83 # ASSIGN : s_6_4 232 # ASSIGN : s_6_5 308 # ASSIGN : s_6_6 390 SHOW_RESULT 465 END : 465 (0 seconds) [Mon Jun 19 23:16:44 2006] SHOW_RESULT 465 CPU : 0.0400000000000009 = 0.0400000000000009 + 0 + 0 + 0 # BOUND : makespan 463 465 MODIFY_CNF 464 BEGIN : [Mon Jun 19 23:16:44 2006] MODIFY_CNF 464 END : 7651022 bytes (0 seconds) [Mon Jun 19 23:16:44 2006] MODIFY_CNF 464 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 464 BEGIN : [Mon Jun 19 23:16:44 2006] CMD : minisat /tmp/csp2sat14006.cnf /tmp/csp2sat14006.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 278229 804892 | 92743 0 0 nan | 0.000 % | | 103 | 278229 804892 | 102017 103 1698 16.5 | 34.243 % | ============================================================================== restarts : 2 conflicts : 183 (238 /sec) decisions : 402 (522 /sec) propagations : 358239 (465245 /sec) conflict literals : 2570 (12.70 % deleted) Memory used : 18.13 MB CPU time : 0.77 s SATISFIABLE VERIFY_CNF 464 END : (1 seconds) [Mon Jun 19 23:16:45 2006] VERIFY_CNF 464 CPU : 0.82 = 0.00999999999999979 + 0 + 0.79 + 0.02 # RESULT : makespan 464 SATISFIABLE SHOW_RESULT 464 BEGIN : [Mon Jun 19 23:16:45 2006] # ASSIGN : makespan 464 # ASSIGN : s_0_0 0 # ASSIGN : s_0_1 50 # ASSIGN : s_0_2 395 # ASSIGN : s_0_3 91 # ASSIGN : s_0_4 260 # ASSIGN : s_0_5 346 # ASSIGN : s_0_6 165 # ASSIGN : s_1_0 56 # ASSIGN : s_1_1 2 # ASSIGN : s_1_2 224 # ASSIGN : s_1_3 245 # ASSIGN : s_1_4 367 # ASSIGN : s_1_5 99 # ASSIGN : s_1_6 414 # ASSIGN : s_2_0 256 # ASSIGN : s_2_1 111 # ASSIGN : s_2_2 333 # ASSIGN : s_2_3 167 # ASSIGN : s_2_4 414 # ASSIGN : s_2_5 17 # ASSIGN : s_2_6 396 # ASSIGN : s_3_0 428 # ASSIGN : s_3_1 184 # ASSIGN : s_3_2 13 # ASSIGN : s_3_3 342 # ASSIGN : s_3_4 175 # ASSIGN : s_3_5 292 # ASSIGN : s_3_6 78 # ASSIGN : s_4_0 158 # ASSIGN : s_4_1 316 # ASSIGN : s_4_2 81 # ASSIGN : s_4_3 6 # ASSIGN : s_4_4 33 # ASSIGN : s_4_5 394 # ASSIGN : s_4_6 264 # ASSIGN : s_5_0 154 # ASSIGN : s_5_1 432 # ASSIGN : s_5_2 7 # ASSIGN : s_5_3 35 # ASSIGN : s_5_4 205 # ASSIGN : s_5_5 242 # ASSIGN : s_5_6 310 # ASSIGN : s_6_0 333 # ASSIGN : s_6_1 266 # ASSIGN : s_6_2 296 # ASSIGN : s_6_3 410 # ASSIGN : s_6_4 87 # ASSIGN : s_6_5 160 # ASSIGN : s_6_6 3 SHOW_RESULT 464 END : 464 (0 seconds) [Mon Jun 19 23:16:45 2006] SHOW_RESULT 464 CPU : 0.0399999999999991 = 0.0399999999999991 + 0 + 0 + 0 # BOUND : makespan 463 464 MODIFY_CNF 463 BEGIN : [Mon Jun 19 23:16:45 2006] MODIFY_CNF 463 END : 7651022 bytes (0 seconds) [Mon Jun 19 23:16:45 2006] MODIFY_CNF 463 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 463 BEGIN : [Mon Jun 19 23:16:45 2006] CMD : minisat /tmp/csp2sat14006.cnf /tmp/csp2sat14006.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 277642 803128 | 92547 0 0 nan | 0.000 % | | 101 | 277642 803128 | 101801 101 1809 17.9 | 34.403 % | ============================================================================== restarts : 2 conflicts : 245 (285 /sec) decisions : 442 (514 /sec) propagations : 434351 (505059 /sec) conflict literals : 4887 (8.12 % deleted) Memory used : 18.13 MB CPU time : 0.86 s SATISFIABLE VERIFY_CNF 463 END : (1 seconds) [Mon Jun 19 23:16:46 2006] VERIFY_CNF 463 CPU : 0.919999999999999 = 0 + 0 + 0.879999999999999 + 0.04 # RESULT : makespan 463 SATISFIABLE SHOW_RESULT 463 BEGIN : [Mon Jun 19 23:16:46 2006] # ASSIGN : makespan 463 # ASSIGN : s_0_0 212 # ASSIGN : s_0_1 336 # ASSIGN : s_0_2 143 # ASSIGN : s_0_3 262 # ASSIGN : s_0_4 377 # ASSIGN : s_0_5 0 # ASSIGN : s_0_6 48 # ASSIGN : s_1_0 3 # ASSIGN : s_1_1 218 # ASSIGN : s_1_2 340 # ASSIGN : s_1_3 366 # ASSIGN : s_1_4 49 # ASSIGN : s_1_5 266 # ASSIGN : s_1_6 147 # ASSIGN : s_2_0 272 # ASSIGN : s_2_1 162 # ASSIGN : s_2_2 0 # ASSIGN : s_2_3 62 # ASSIGN : s_2_4 222 # ASSIGN : s_2_5 381 # ASSIGN : s_2_6 359 # ASSIGN : s_3_0 427 # ASSIGN : s_3_1 51 # ASSIGN : s_3_2 361 # ASSIGN : s_3_3 194 # ASSIGN : s_3_4 133 # ASSIGN : s_3_5 142 # ASSIGN : s_3_6 272 # ASSIGN : s_4_0 46 # ASSIGN : s_4_1 385 # ASSIGN : s_4_2 262 # ASSIGN : s_4_3 339 # ASSIGN : s_4_4 144 # ASSIGN : s_4_5 192 # ASSIGN : s_4_6 0 # ASSIGN : s_5_0 268 # ASSIGN : s_5_1 295 # ASSIGN : s_5_2 256 # ASSIGN : s_5_3 6 # ASSIGN : s_5_4 96 # ASSIGN : s_5_5 327 # ASSIGN : s_5_6 377 # ASSIGN : s_6_0 349 # ASSIGN : s_6_1 21 # ASSIGN : s_6_2 426 # ASSIGN : s_6_3 140 # ASSIGN : s_6_4 276 # ASSIGN : s_6_5 58 # ASSIGN : s_6_6 197 SHOW_RESULT 463 END : 463 (0 seconds) [Mon Jun 19 23:16:46 2006] SHOW_RESULT 463 CPU : 0.0400000000000009 = 0.0400000000000009 + 0 + 0 + 0 # BOUND : makespan 463 463 MAIN END : (21 seconds) [Mon Jun 19 23:16:46 2006] MAIN CPU : 20.28 = 15.05 + 0.09 + 4.77 + 0.37