MAIN BEGIN : [Fri Jun 2 08:25:53 2006] READ BEGIN : csp/orb02.csp [Fri Jun 2 08:25:53 2006] READ END : csp/orb02.csp (2 seconds) [Fri Jun 2 08:25:55 2006] READ CPU : 1.39 = 1.39 + 0 + 0 + 0 # BOUND : makespan 671 1157 GENERATE_CNF 1157 BEGIN : [Fri Jun 2 08:25:55 2006] GENERATE_CNF 1157 END : 117388 variables 1217188 clauses 27179168 bytes (59 seconds) [Fri Jun 2 08:26:54 2006] GENERATE_CNF 1157 CPU : 58.9 = 58.82 + 0.08 + 0 + 0 MODIFY_CNF 914 BEGIN : [Fri Jun 2 08:26:54 2006] MODIFY_CNF 914 END : 27179174 bytes (0 seconds) [Fri Jun 2 08:26:54 2006] MODIFY_CNF 914 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 914 BEGIN : [Fri Jun 2 08:26:54 2006] CMD : minisat /work/tamura/csp2sat45900.cnf /work/tamura/csp2sat45900.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 478840 1397034 | 159613 0 0 NaNQ | 0.000 % | ==============================================================================) restarts : 1 conflicts : 23 (15 /sec) decisions : 143 (91 /sec) propagations : 191674 (121779 /sec) inspects : 1272839 (808694 /sec) conflict literals : 305 (6.44 % deleted) CPU time : 1.57394 s SATISFIABLE VERIFY_CNF 914 END : (2 seconds) [Fri Jun 2 08:26:56 2006] VERIFY_CNF 914 CPU : 1.92 = 0 + 0 + 1.9 + 0.02 # RESULT : makespan 914 SATISFIABLE SHOW_RESULT 914 BEGIN : [Fri Jun 2 08:26:56 2006] # ASSIGN : makespan 914 # ASSIGN : s_0_0 142 # ASSIGN : s_0_1 214 # ASSIGN : s_0_2 283 # ASSIGN : s_0_3 316 # ASSIGN : s_0_4 402 # ASSIGN : s_0_5 477 # ASSIGN : s_0_6 493 # ASSIGN : s_0_7 589 # ASSIGN : s_0_8 617 # ASSIGN : s_0_9 751 # ASSIGN : s_1_0 1 # ASSIGN : s_1_1 36 # ASSIGN : s_1_2 126 # ASSIGN : s_1_3 174 # ASSIGN : s_1_4 226 # ASSIGN : s_1_5 286 # ASSIGN : s_1_6 341 # ASSIGN : s_1_7 388 # ASSIGN : s_1_8 481 # ASSIGN : s_1_9 561 # ASSIGN : s_2_0 72 # ASSIGN : s_2_1 173 # ASSIGN : s_2_2 184 # ASSIGN : s_2_3 198 # ASSIGN : s_2_4 254 # ASSIGN : s_2_5 319 # ASSIGN : s_2_6 510 # ASSIGN : s_2_7 520 # ASSIGN : s_2_8 802 # ASSIGN : s_2_9 827 # ASSIGN : s_3_0 219 # ASSIGN : s_3_1 268 # ASSIGN : s_3_2 299 # ASSIGN : s_3_3 481 # ASSIGN : s_3_4 581 # ASSIGN : s_3_5 644 # ASSIGN : s_3_6 692 # ASSIGN : s_3_7 757 # ASSIGN : s_3_8 780 # ASSIGN : s_3_9 885 # ASSIGN : s_4_0 17 # ASSIGN : s_4_1 166 # ASSIGN : s_4_2 172 # ASSIGN : s_4_3 200 # ASSIGN : s_4_4 296 # ASSIGN : s_4_5 382 # ASSIGN : s_4_6 497 # ASSIGN : s_4_7 519 # ASSIGN : s_4_8 826 # ASSIGN : s_4_9 890 # ASSIGN : s_5_0 2 # ASSIGN : s_5_1 119 # ASSIGN : s_5_2 184 # ASSIGN : s_5_3 262 # ASSIGN : s_5_4 328 # ASSIGN : s_5_5 412 # ASSIGN : s_5_6 511 # ASSIGN : s_5_7 596 # ASSIGN : s_5_8 683 # ASSIGN : s_5_9 774 # ASSIGN : s_6_0 48 # ASSIGN : s_6_1 124 # ASSIGN : s_6_2 323 # ASSIGN : s_6_3 399 # ASSIGN : s_6_4 561 # ASSIGN : s_6_5 637 # ASSIGN : s_6_6 716 # ASSIGN : s_6_7 816 # ASSIGN : s_6_8 830 # ASSIGN : s_6_9 857 # ASSIGN : s_7_0 222 # ASSIGN : s_7_1 315 # ASSIGN : s_7_2 342 # ASSIGN : s_7_3 444 # ASSIGN : s_7_4 531 # ASSIGN : s_7_5 679 # ASSIGN : s_7_6 733 # ASSIGN : s_7_7 762 # ASSIGN : s_7_8 845 # ASSIGN : s_7_9 867 # ASSIGN : s_8_0 34 # ASSIGN : s_8_1 270 # ASSIGN : s_8_2 281 # ASSIGN : s_8_3 359 # ASSIGN : s_8_4 531 # ASSIGN : s_8_5 596 # ASSIGN : s_8_6 677 # ASSIGN : s_8_7 687 # ASSIGN : s_8_8 811 # ASSIGN : s_8_9 865 # ASSIGN : s_9_0 62 # ASSIGN : s_9_1 84 # ASSIGN : s_9_2 160 # ASSIGN : s_9_3 249 # ASSIGN : s_9_4 346 # ASSIGN : s_9_5 434 # ASSIGN : s_9_6 444 # ASSIGN : s_9_7 594 # ASSIGN : s_9_8 696 # ASSIGN : s_9_9 897 SHOW_RESULT 914 END : 914 (0 seconds) [Fri Jun 2 08:26:56 2006] SHOW_RESULT 914 CPU : 0.329999999999998 = 0.329999999999998 + 0 + 0 + 0 # BOUND : makespan 671 914 MODIFY_CNF 792 BEGIN : [Fri Jun 2 08:26:56 2006] MODIFY_CNF 792 END : 27179174 bytes (0 seconds) [Fri Jun 2 08:26:56 2006] MODIFY_CNF 792 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 792 BEGIN : [Fri Jun 2 08:26:56 2006] CMD : minisat /work/tamura/csp2sat45900.cnf /work/tamura/csp2sat45900.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 327419 955205 | 109139 0 0 NaNQ | 0.000 % | ==============================================================================) restarts : 1 conflicts : 4 (2 /sec) decisions : 3 (2 /sec) propagations : 116578 (71692 /sec) inspects : 633068 (389316 /sec) conflict literals : 3 (0.00 % deleted) CPU time : 1.6261 s UNSATISFIABLE VERIFY_CNF 792 END : (2 seconds) [Fri Jun 2 08:26:58 2006] VERIFY_CNF 792 CPU : 1.9 = 0 + 0.01 + 1.85 + 0.04 # RESULT : makespan 792 UNSATISFIABLE # BOUND : makespan 793 914 MODIFY_CNF 853 BEGIN : [Fri Jun 2 08:26:58 2006] MODIFY_CNF 853 END : 27179174 bytes (0 seconds) [Fri Jun 2 08:26:58 2006] MODIFY_CNF 853 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 853 BEGIN : [Fri Jun 2 08:26:58 2006] CMD : minisat /work/tamura/csp2sat45900.cnf /work/tamura/csp2sat45900.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 402700 1174822 | 134233 0 0 NaNQ | 0.000 % | | 100 | 402700 1174822 | 147656 95 480 5.1 | 72.260 % | ==============================================================================) restarts : 2 conflicts : 132 (70 /sec) decisions : 176 (94 /sec) propagations : 892286 (474067 /sec) inspects : 4745592 (2521310 /sec) conflict literals : 677 (28.28 % deleted) CPU time : 1.88219 s UNSATISFIABLE VERIFY_CNF 853 END : (2 seconds) [Fri Jun 2 08:27:00 2006] VERIFY_CNF 853 CPU : 2.19 = 0.0100000000000051 + 0.00999999999999998 + 2.14 + 0.03 # RESULT : makespan 853 UNSATISFIABLE # BOUND : makespan 854 914 MODIFY_CNF 884 BEGIN : [Fri Jun 2 08:27:00 2006] MODIFY_CNF 884 END : 27179174 bytes (0 seconds) [Fri Jun 2 08:27:00 2006] MODIFY_CNF 884 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 884 BEGIN : [Fri Jun 2 08:27:00 2006] CMD : minisat /work/tamura/csp2sat45900.cnf /work/tamura/csp2sat45900.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 439537 1282179 | 146512 0 0 NaNQ | 0.000 % | | 100 | 439537 1282179 | 161163 98 709 7.2 | 68.672 % | | 250 | 439537 1282179 | 177279 247 1907 7.7 | 68.674 % | | 475 | 438013 1277612 | 195007 449 3637 8.1 | 69.963 % | ==============================================================================) restarts : 4 conflicts : 614 (211 /sec) decisions : 894 (308 /sec) propagations : 3759920 (1294021 /sec) inspects : 22382807 (7703307 /sec) conflict literals : 5145 (29.58 % deleted) CPU time : 2.90561 s UNSATISFIABLE VERIFY_CNF 884 END : (4 seconds) [Fri Jun 2 08:27:04 2006] VERIFY_CNF 884 CPU : 3.19 = 0 + 0 + 3.16 + 0.03 # RESULT : makespan 884 UNSATISFIABLE # BOUND : makespan 885 914 MODIFY_CNF 899 BEGIN : [Fri Jun 2 08:27:04 2006] MODIFY_CNF 899 END : 27179174 bytes (0 seconds) [Fri Jun 2 08:27:04 2006] MODIFY_CNF 899 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 899 BEGIN : [Fri Jun 2 08:27:04 2006] CMD : minisat /work/tamura/csp2sat45900.cnf /work/tamura/csp2sat45900.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 458961 1338923 | 152987 0 0 NaNQ | 0.000 % | ==============================================================================) restarts : 1 conflicts : 32 (20 /sec) decisions : 139 (85 /sec) propagations : 269813 (164826 /sec) inspects : 1765458 (1078503 /sec) conflict literals : 279 (14.94 % deleted) CPU time : 1.63695 s SATISFIABLE VERIFY_CNF 899 END : (2 seconds) [Fri Jun 2 08:27:06 2006] VERIFY_CNF 899 CPU : 2.08 = 0 + 0.01 + 1.96 + 0.11 # RESULT : makespan 899 SATISFIABLE SHOW_RESULT 899 BEGIN : [Fri Jun 2 08:27:06 2006] # ASSIGN : makespan 899 # ASSIGN : s_0_0 194 # ASSIGN : s_0_1 266 # ASSIGN : s_0_2 320 # ASSIGN : s_0_3 417 # ASSIGN : s_0_4 503 # ASSIGN : s_0_5 578 # ASSIGN : s_0_6 594 # ASSIGN : s_0_7 690 # ASSIGN : s_0_8 724 # ASSIGN : s_0_9 823 # ASSIGN : s_1_0 4 # ASSIGN : s_1_1 21 # ASSIGN : s_1_2 224 # ASSIGN : s_1_3 272 # ASSIGN : s_1_4 324 # ASSIGN : s_1_5 427 # ASSIGN : s_1_6 456 # ASSIGN : s_1_7 474 # ASSIGN : s_1_8 563 # ASSIGN : s_1_9 674 # ASSIGN : s_2_0 147 # ASSIGN : s_2_1 213 # ASSIGN : s_2_2 224 # ASSIGN : s_2_3 248 # ASSIGN : s_2_4 304 # ASSIGN : s_2_5 320 # ASSIGN : s_2_6 403 # ASSIGN : s_2_7 413 # ASSIGN : s_2_8 550 # ASSIGN : s_2_9 601 # ASSIGN : s_3_0 98 # ASSIGN : s_3_1 174 # ASSIGN : s_3_2 205 # ASSIGN : s_3_3 222 # ASSIGN : s_3_4 350 # ASSIGN : s_3_5 452 # ASSIGN : s_3_6 656 # ASSIGN : s_3_7 721 # ASSIGN : s_3_8 744 # ASSIGN : s_3_9 794 # ASSIGN : s_4_0 20 # ASSIGN : s_4_1 75 # ASSIGN : s_4_2 81 # ASSIGN : s_4_3 109 # ASSIGN : s_4_4 264 # ASSIGN : s_4_5 353 # ASSIGN : s_4_6 482 # ASSIGN : s_4_7 504 # ASSIGN : s_4_8 574 # ASSIGN : s_4_9 875 # ASSIGN : s_5_0 9 # ASSIGN : s_5_1 75 # ASSIGN : s_5_2 105 # ASSIGN : s_5_3 175 # ASSIGN : s_5_4 194 # ASSIGN : s_5_5 298 # ASSIGN : s_5_6 496 # ASSIGN : s_5_7 581 # ASSIGN : s_5_8 668 # ASSIGN : s_5_9 759 # ASSIGN : s_6_0 148 # ASSIGN : s_6_1 238 # ASSIGN : s_6_2 308 # ASSIGN : s_6_3 384 # ASSIGN : s_6_4 487 # ASSIGN : s_6_5 588 # ASSIGN : s_6_6 638 # ASSIGN : s_6_7 801 # ASSIGN : s_6_8 815 # ASSIGN : s_6_9 842 # ASSIGN : s_7_0 55 # ASSIGN : s_7_1 189 # ASSIGN : s_7_2 267 # ASSIGN : s_7_3 330 # ASSIGN : s_7_4 464 # ASSIGN : s_7_5 643 # ASSIGN : s_7_6 697 # ASSIGN : s_7_7 747 # ASSIGN : s_7_8 830 # ASSIGN : s_7_9 852 # ASSIGN : s_8_0 58 # ASSIGN : s_8_1 86 # ASSIGN : s_8_2 97 # ASSIGN : s_8_3 245 # ASSIGN : s_8_4 593 # ASSIGN : s_8_5 659 # ASSIGN : s_8_6 740 # ASSIGN : s_8_7 750 # ASSIGN : s_8_8 796 # ASSIGN : s_8_9 850 # ASSIGN : s_9_0 16 # ASSIGN : s_9_1 38 # ASSIGN : s_9_2 114 # ASSIGN : s_9_3 203 # ASSIGN : s_9_4 216 # ASSIGN : s_9_5 320 # ASSIGN : s_9_6 330 # ASSIGN : s_9_7 405 # ASSIGN : s_9_8 510 # ASSIGN : s_9_9 882 SHOW_RESULT 899 END : 899 (0 seconds) [Fri Jun 2 08:27:06 2006] SHOW_RESULT 899 CPU : 0.329999999999998 = 0.329999999999998 + 0 + 0 + 0 # BOUND : makespan 885 899 MODIFY_CNF 892 BEGIN : [Fri Jun 2 08:27:06 2006] MODIFY_CNF 892 END : 27179174 bytes (0 seconds) [Fri Jun 2 08:27:06 2006] MODIFY_CNF 892 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 892 BEGIN : [Fri Jun 2 08:27:06 2006] CMD : minisat /work/tamura/csp2sat45900.cnf /work/tamura/csp2sat45900.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 450817 1315202 | 150272 0 0 NaNQ | 0.000 % | ==============================================================================) restarts : 1 conflicts : 54 (32 /sec) decisions : 203 (121 /sec) propagations : 360951 (215305 /sec) inspects : 2486823 (1483372 /sec) conflict literals : 575 (11.67 % deleted) CPU time : 1.67647 s SATISFIABLE VERIFY_CNF 892 END : (2 seconds) [Fri Jun 2 08:27:08 2006] VERIFY_CNF 892 CPU : 2.11 = 0.00999999999999801 + 0.01 + 1.98 + 0.11 # RESULT : makespan 892 SATISFIABLE SHOW_RESULT 892 BEGIN : [Fri Jun 2 08:27:08 2006] # ASSIGN : makespan 892 # ASSIGN : s_0_0 120 # ASSIGN : s_0_1 192 # ASSIGN : s_0_2 246 # ASSIGN : s_0_3 279 # ASSIGN : s_0_4 371 # ASSIGN : s_0_5 455 # ASSIGN : s_0_6 471 # ASSIGN : s_0_7 567 # ASSIGN : s_0_8 587 # ASSIGN : s_0_9 729 # ASSIGN : s_1_0 3 # ASSIGN : s_1_1 21 # ASSIGN : s_1_2 151 # ASSIGN : s_1_3 207 # ASSIGN : s_1_4 259 # ASSIGN : s_1_5 319 # ASSIGN : s_1_6 348 # ASSIGN : s_1_7 366 # ASSIGN : s_1_8 459 # ASSIGN : s_1_9 539 # ASSIGN : s_2_0 207 # ASSIGN : s_2_1 254 # ASSIGN : s_2_2 265 # ASSIGN : s_2_3 304 # ASSIGN : s_2_4 430 # ASSIGN : s_2_5 446 # ASSIGN : s_2_6 529 # ASSIGN : s_2_7 600 # ASSIGN : s_2_8 780 # ASSIGN : s_2_9 805 # ASSIGN : s_3_0 266 # ASSIGN : s_3_1 334 # ASSIGN : s_3_2 365 # ASSIGN : s_3_3 451 # ASSIGN : s_3_4 537 # ASSIGN : s_3_5 690 # ASSIGN : s_3_6 725 # ASSIGN : s_3_7 790 # ASSIGN : s_3_8 813 # ASSIGN : s_3_9 863 # ASSIGN : s_4_0 19 # ASSIGN : s_4_1 74 # ASSIGN : s_4_2 81 # ASSIGN : s_4_3 109 # ASSIGN : s_4_4 274 # ASSIGN : s_4_5 360 # ASSIGN : s_4_6 634 # ASSIGN : s_4_7 702 # ASSIGN : s_4_8 804 # ASSIGN : s_4_9 868 # ASSIGN : s_5_0 29 # ASSIGN : s_5_1 79 # ASSIGN : s_5_2 102 # ASSIGN : s_5_3 172 # ASSIGN : s_5_4 192 # ASSIGN : s_5_5 392 # ASSIGN : s_5_6 489 # ASSIGN : s_5_7 574 # ASSIGN : s_5_8 661 # ASSIGN : s_5_9 752 # ASSIGN : s_6_0 75 # ASSIGN : s_6_1 205 # ASSIGN : s_6_2 315 # ASSIGN : s_6_3 391 # ASSIGN : s_6_4 539 # ASSIGN : s_6_5 615 # ASSIGN : s_6_6 686 # ASSIGN : s_6_7 772 # ASSIGN : s_6_8 786 # ASSIGN : s_6_9 835 # ASSIGN : s_7_0 199 # ASSIGN : s_7_1 292 # ASSIGN : s_7_2 334 # ASSIGN : s_7_3 414 # ASSIGN : s_7_4 501 # ASSIGN : s_7_5 624 # ASSIGN : s_7_6 678 # ASSIGN : s_7_7 740 # ASSIGN : s_7_8 825 # ASSIGN : s_7_9 845 # ASSIGN : s_8_0 52 # ASSIGN : s_8_1 80 # ASSIGN : s_8_2 91 # ASSIGN : s_8_3 169 # ASSIGN : s_8_4 308 # ASSIGN : s_8_5 648 # ASSIGN : s_8_6 733 # ASSIGN : s_8_7 743 # ASSIGN : s_8_8 789 # ASSIGN : s_8_9 860 # ASSIGN : s_9_0 4 # ASSIGN : s_9_1 26 # ASSIGN : s_9_2 102 # ASSIGN : s_9_3 191 # ASSIGN : s_9_4 204 # ASSIGN : s_9_5 382 # ASSIGN : s_9_6 492 # ASSIGN : s_9_7 567 # ASSIGN : s_9_8 665 # ASSIGN : s_9_9 808 SHOW_RESULT 892 END : 892 (1 seconds) [Fri Jun 2 08:27:09 2006] SHOW_RESULT 892 CPU : 0.340000000000003 = 0.340000000000003 + 0 + 0 + 0 # BOUND : makespan 885 892 MODIFY_CNF 888 BEGIN : [Fri Jun 2 08:27:09 2006] MODIFY_CNF 888 END : 27179174 bytes (0 seconds) [Fri Jun 2 08:27:09 2006] MODIFY_CNF 888 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 888 BEGIN : [Fri Jun 2 08:27:09 2006] CMD : minisat /work/tamura/csp2sat45900.cnf /work/tamura/csp2sat45900.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 445139 1298576 | 148379 0 0 NaNQ | 0.000 % | | 101 | 445139 1298576 | 163216 100 881 8.8 | 68.321 % | | 253 | 445139 1298576 | 179538 252 2407 9.6 | 68.321 % | | 478 | 444673 1297180 | 197492 456 4764 10.4 | 68.414 % | ==============================================================================) restarts : 4 conflicts : 545 (205 /sec) decisions : 947 (356 /sec) propagations : 3135121 (1177656 /sec) inspects : 19122633 (7183100 /sec) conflict literals : 5407 (25.39 % deleted) CPU time : 2.66217 s SATISFIABLE VERIFY_CNF 888 END : (3 seconds) [Fri Jun 2 08:27:12 2006] VERIFY_CNF 888 CPU : 3 = 0 + 0 + 2.96 + 0.04 # RESULT : makespan 888 SATISFIABLE SHOW_RESULT 888 BEGIN : [Fri Jun 2 08:27:12 2006] # ASSIGN : makespan 888 # ASSIGN : s_0_0 122 # ASSIGN : s_0_1 194 # ASSIGN : s_0_2 248 # ASSIGN : s_0_3 281 # ASSIGN : s_0_4 367 # ASSIGN : s_0_5 451 # ASSIGN : s_0_6 467 # ASSIGN : s_0_7 563 # ASSIGN : s_0_8 591 # ASSIGN : s_0_9 725 # ASSIGN : s_1_0 2 # ASSIGN : s_1_1 23 # ASSIGN : s_1_2 147 # ASSIGN : s_1_3 203 # ASSIGN : s_1_4 255 # ASSIGN : s_1_5 315 # ASSIGN : s_1_6 344 # ASSIGN : s_1_7 362 # ASSIGN : s_1_8 455 # ASSIGN : s_1_9 535 # ASSIGN : s_2_0 201 # ASSIGN : s_2_1 256 # ASSIGN : s_2_2 267 # ASSIGN : s_2_3 300 # ASSIGN : s_2_4 426 # ASSIGN : s_2_5 442 # ASSIGN : s_2_6 525 # ASSIGN : s_2_7 596 # ASSIGN : s_2_8 776 # ASSIGN : s_2_9 830 # ASSIGN : s_3_0 248 # ASSIGN : s_3_1 338 # ASSIGN : s_3_2 369 # ASSIGN : s_3_3 455 # ASSIGN : s_3_4 533 # ASSIGN : s_3_5 615 # ASSIGN : s_3_6 663 # ASSIGN : s_3_7 728 # ASSIGN : s_3_8 751 # ASSIGN : s_3_9 801 # ASSIGN : s_4_0 18 # ASSIGN : s_4_1 73 # ASSIGN : s_4_2 83 # ASSIGN : s_4_3 111 # ASSIGN : s_4_4 270 # ASSIGN : s_4_5 356 # ASSIGN : s_4_6 471 # ASSIGN : s_4_7 493 # ASSIGN : s_4_8 800 # ASSIGN : s_4_9 864 # ASSIGN : s_5_0 25 # ASSIGN : s_5_1 75 # ASSIGN : s_5_2 98 # ASSIGN : s_5_3 168 # ASSIGN : s_5_4 194 # ASSIGN : s_5_5 386 # ASSIGN : s_5_6 485 # ASSIGN : s_5_7 570 # ASSIGN : s_5_8 657 # ASSIGN : s_5_9 748 # ASSIGN : s_6_0 71 # ASSIGN : s_6_1 207 # ASSIGN : s_6_2 297 # ASSIGN : s_6_3 373 # ASSIGN : s_6_4 535 # ASSIGN : s_6_5 611 # ASSIGN : s_6_6 690 # ASSIGN : s_6_7 790 # ASSIGN : s_6_8 804 # ASSIGN : s_6_9 831 # ASSIGN : s_7_0 195 # ASSIGN : s_7_1 288 # ASSIGN : s_7_2 316 # ASSIGN : s_7_3 418 # ASSIGN : s_7_4 505 # ASSIGN : s_7_5 650 # ASSIGN : s_7_6 704 # ASSIGN : s_7_7 736 # ASSIGN : s_7_8 821 # ASSIGN : s_7_9 841 # ASSIGN : s_8_0 51 # ASSIGN : s_8_1 79 # ASSIGN : s_8_2 90 # ASSIGN : s_8_3 171 # ASSIGN : s_8_4 304 # ASSIGN : s_8_5 644 # ASSIGN : s_8_6 729 # ASSIGN : s_8_7 739 # ASSIGN : s_8_8 785 # ASSIGN : s_8_9 856 # ASSIGN : s_9_0 0 # ASSIGN : s_9_1 22 # ASSIGN : s_9_2 98 # ASSIGN : s_9_3 187 # ASSIGN : s_9_4 200 # ASSIGN : s_9_5 408 # ASSIGN : s_9_6 418 # ASSIGN : s_9_7 563 # ASSIGN : s_9_8 661 # ASSIGN : s_9_9 804 SHOW_RESULT 888 END : 888 (0 seconds) [Fri Jun 2 08:27:12 2006] SHOW_RESULT 888 CPU : 0.349999999999996 = 0.339999999999996 + 0.00999999999999998 + 0 + 0 # BOUND : makespan 885 888 MODIFY_CNF 886 BEGIN : [Fri Jun 2 08:27:12 2006] MODIFY_CNF 886 END : 27179174 bytes (0 seconds) [Fri Jun 2 08:27:12 2006] MODIFY_CNF 886 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 886 BEGIN : [Fri Jun 2 08:27:12 2006] CMD : minisat /work/tamura/csp2sat45900.cnf /work/tamura/csp2sat45900.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 442651 1291316 | 147550 0 0 NaNQ | 0.000 % | | 100 | 442651 1291316 | 162305 99 619 6.3 | 68.495 % | | 250 | 442651 1291316 | 178535 249 2447 9.8 | 68.495 % | | 475 | 442187 1289926 | 196389 455 4911 10.8 | 68.495 % | ==============================================================================) restarts : 4 conflicts : 708 (236 /sec) decisions : 962 (320 /sec) propagations : 4134754 (1376809 /sec) inspects : 25093763 (8355834 /sec) conflict literals : 6593 (28.49 % deleted) CPU time : 3.00314 s UNSATISFIABLE VERIFY_CNF 886 END : (3 seconds) [Fri Jun 2 08:27:15 2006] VERIFY_CNF 886 CPU : 3.37 = 0 + 0 + 3.27 + 0.1 # RESULT : makespan 886 UNSATISFIABLE # BOUND : makespan 887 888 MODIFY_CNF 887 BEGIN : [Fri Jun 2 08:27:15 2006] MODIFY_CNF 887 END : 27179174 bytes (0 seconds) [Fri Jun 2 08:27:15 2006] MODIFY_CNF 887 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 887 BEGIN : [Fri Jun 2 08:27:15 2006] CMD : minisat /work/tamura/csp2sat45900.cnf /work/tamura/csp2sat45900.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 443529 1293849 | 147843 0 0 NaNQ | 0.000 % | | 100 | 443529 1293849 | 162627 99 597 6.0 | 68.409 % | | 251 | 443529 1293849 | 178890 249 2026 8.1 | 68.738 % | | 476 | 437990 1277618 | 196779 424 4426 10.4 | 68.738 % | ==============================================================================) restarts : 4 conflicts : 792 (238 /sec) decisions : 1146 (345 /sec) propagations : 4908736 (1476201 /sec) inspects : 29536614 (8882530 /sec) conflict literals : 7684 (30.49 % deleted) CPU time : 3.32525 s UNSATISFIABLE VERIFY_CNF 887 END : (4 seconds) [Fri Jun 2 08:27:19 2006] VERIFY_CNF 887 CPU : 3.69 = 0 + 0.01 + 3.57 + 0.11 # RESULT : makespan 887 UNSATISFIABLE # BOUND : makespan 888 888 MAIN END : (86 seconds) [Fri Jun 2 08:27:19 2006] MAIN CPU : 85.1 = 61.58 + 0.14 + 22.79 + 0.59