MAIN BEGIN : [Fri Jun 2 08:41:03 2006] READ BEGIN : csp/orb08.csp [Fri Jun 2 08:41:03 2006] READ END : csp/orb08.csp (2 seconds) [Fri Jun 2 08:41:05 2006] READ CPU : 1.41 = 1.41 + 0 + 0 + 0 # BOUND : makespan 585 1139 GENERATE_CNF 1139 BEGIN : [Fri Jun 2 08:41:05 2006] GENERATE_CNF 1139 END : 115656 variables 1205211 clauses 26883971 bytes (58 seconds) [Fri Jun 2 08:42:03 2006] GENERATE_CNF 1139 CPU : 58.61 = 58.53 + 0.08 + 0 + 0 MODIFY_CNF 862 BEGIN : [Fri Jun 2 08:42:03 2006] MODIFY_CNF 862 END : 26883977 bytes (0 seconds) [Fri Jun 2 08:42:03 2006] MODIFY_CNF 862 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 862 BEGIN : [Fri Jun 2 08:42:03 2006] CMD : minisat /work/tamura/csp2sat29442.cnf /work/tamura/csp2sat29442.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 545531 1595202 | 181843 0 0 NaNQ | 0.000 % | | 100 | 545531 1595202 | 200027 100 930 9.3 | 63.878 % | | 251 | 545531 1595202 | 220030 251 1810 7.2 | 63.878 % | ==============================================================================) restarts : 3 conflicts : 406 (200 /sec) decisions : 556 (274 /sec) propagations : 1934980 (952983 /sec) inspects : 11298029 (5564309 /sec) conflict literals : 2558 (27.74 % deleted) CPU time : 2.03045 s UNSATISFIABLE VERIFY_CNF 862 END : (3 seconds) [Fri Jun 2 08:42:06 2006] VERIFY_CNF 862 CPU : 2.34 = 0 + 0.01 + 2.31 + 0.02 # RESULT : makespan 862 UNSATISFIABLE # BOUND : makespan 863 1139 MODIFY_CNF 1001 BEGIN : [Fri Jun 2 08:42:06 2006] MODIFY_CNF 1001 END : 26883977 bytes (0 seconds) [Fri Jun 2 08:42:06 2006] MODIFY_CNF 1001 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1001 BEGIN : [Fri Jun 2 08:42:06 2006] CMD : minisat /work/tamura/csp2sat29442.cnf /work/tamura/csp2sat29442.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 684670 1998580 | 228223 0 0 NaNQ | 0.000 % | | 101 | 684670 1998580 | 251045 101 1732 17.1 | 51.740 % | ==============================================================================) restarts : 2 conflicts : 193 (109 /sec) decisions : 513 (289 /sec) propagations : 1192876 (670989 /sec) inspects : 10322732 (5806503 /sec) conflict literals : 3039 (13.62 % deleted) CPU time : 1.77779 s SATISFIABLE VERIFY_CNF 1001 END : (2 seconds) [Fri Jun 2 08:42:08 2006] VERIFY_CNF 1001 CPU : 2.18 = 0 + 0 + 2.15 + 0.03 # RESULT : makespan 1001 SATISFIABLE SHOW_RESULT 1001 BEGIN : [Fri Jun 2 08:42:08 2006] # ASSIGN : makespan 1001 # ASSIGN : s_0_0 148 # ASSIGN : s_0_1 204 # ASSIGN : s_0_2 278 # ASSIGN : s_0_3 323 # ASSIGN : s_0_4 381 # ASSIGN : s_0_5 468 # ASSIGN : s_0_6 673 # ASSIGN : s_0_7 881 # ASSIGN : s_0_8 942 # ASSIGN : s_0_9 990 # ASSIGN : s_1_0 4 # ASSIGN : s_1_1 129 # ASSIGN : s_1_2 192 # ASSIGN : s_1_3 243 # ASSIGN : s_1_4 334 # ASSIGN : s_1_5 376 # ASSIGN : s_1_6 387 # ASSIGN : s_1_7 416 # ASSIGN : s_1_8 530 # ASSIGN : s_1_9 559 # ASSIGN : s_2_0 84 # ASSIGN : s_2_1 172 # ASSIGN : s_2_2 203 # ASSIGN : s_2_3 250 # ASSIGN : s_2_4 261 # ASSIGN : s_2_5 487 # ASSIGN : s_2_6 691 # ASSIGN : s_2_7 749 # ASSIGN : s_2_8 830 # ASSIGN : s_2_9 898 # ASSIGN : s_3_0 24 # ASSIGN : s_3_1 58 # ASSIGN : s_3_2 357 # ASSIGN : s_3_3 457 # ASSIGN : s_3_4 512 # ASSIGN : s_3_5 541 # ASSIGN : s_3_6 590 # ASSIGN : s_3_7 704 # ASSIGN : s_3_8 758 # ASSIGN : s_3_9 773 # ASSIGN : s_4_0 4 # ASSIGN : s_4_1 67 # ASSIGN : s_4_2 158 # ASSIGN : s_4_3 346 # ASSIGN : s_4_4 465 # ASSIGN : s_4_5 511 # ASSIGN : s_4_6 608 # ASSIGN : s_4_7 645 # ASSIGN : s_4_8 700 # ASSIGN : s_4_9 731 # ASSIGN : s_5_0 484 # ASSIGN : s_5_1 509 # ASSIGN : s_5_2 514 # ASSIGN : s_5_3 653 # ASSIGN : s_5_4 747 # ASSIGN : s_5_5 761 # ASSIGN : s_5_6 855 # ASSIGN : s_5_7 875 # ASSIGN : s_5_8 898 # ASSIGN : s_5_9 962 # ASSIGN : s_6_0 16 # ASSIGN : s_6_1 40 # ASSIGN : s_6_2 61 # ASSIGN : s_6_3 108 # ASSIGN : s_6_4 149 # ASSIGN : s_6_5 316 # ASSIGN : s_6_6 452 # ASSIGN : s_6_7 683 # ASSIGN : s_6_8 758 # ASSIGN : s_6_9 986 # ASSIGN : s_7_0 11 # ASSIGN : s_7_1 253 # ASSIGN : s_7_2 260 # ASSIGN : s_7_3 412 # ASSIGN : s_7_4 440 # ASSIGN : s_7_5 547 # ASSIGN : s_7_6 638 # ASSIGN : s_7_7 647 # ASSIGN : s_7_8 765 # ASSIGN : s_7_9 883 # ASSIGN : s_8_0 530 # ASSIGN : s_8_1 564 # ASSIGN : s_8_2 616 # ASSIGN : s_8_3 655 # ASSIGN : s_8_4 661 # ASSIGN : s_8_5 755 # ASSIGN : s_8_6 778 # ASSIGN : s_8_7 834 # ASSIGN : s_8_8 877 # ASSIGN : s_8_9 882 # ASSIGN : s_9_0 280 # ASSIGN : s_9_1 391 # ASSIGN : s_9_2 521 # ASSIGN : s_9_3 603 # ASSIGN : s_9_4 613 # ASSIGN : s_9_5 642 # ASSIGN : s_9_6 657 # ASSIGN : s_9_7 708 # ASSIGN : s_9_8 797 # ASSIGN : s_9_9 980 SHOW_RESULT 1001 END : 1001 (0 seconds) [Fri Jun 2 08:42:08 2006] SHOW_RESULT 1001 CPU : 0.310000000000002 = 0.310000000000002 + 0 + 0 + 0 # BOUND : makespan 863 1001 MODIFY_CNF 932 BEGIN : [Fri Jun 2 08:42:08 2006] MODIFY_CNF 932 END : 26883977 bytes (0 seconds) [Fri Jun 2 08:42:08 2006] MODIFY_CNF 932 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 932 BEGIN : [Fri Jun 2 08:42:08 2006] CMD : minisat /work/tamura/csp2sat29442.cnf /work/tamura/csp2sat29442.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 615601 1798342 | 205200 0 0 NaNQ | 0.000 % | | 100 | 615601 1798342 | 225720 100 1192 11.9 | 57.765 % | ==============================================================================) restarts : 2 conflicts : 120 (74 /sec) decisions : 418 (257 /sec) propagations : 768546 (472620 /sec) inspects : 5485369 (3373249 /sec) conflict literals : 1394 (19.14 % deleted) CPU time : 1.62614 s SATISFIABLE VERIFY_CNF 932 END : (2 seconds) [Fri Jun 2 08:42:10 2006] VERIFY_CNF 932 CPU : 2.12 = 0.00999999999999801 + 0.01 + 1.99 + 0.11 # RESULT : makespan 932 SATISFIABLE SHOW_RESULT 932 BEGIN : [Fri Jun 2 08:42:10 2006] # ASSIGN : makespan 932 # ASSIGN : s_0_0 400 # ASSIGN : s_0_1 456 # ASSIGN : s_0_2 623 # ASSIGN : s_0_3 668 # ASSIGN : s_0_4 691 # ASSIGN : s_0_5 767 # ASSIGN : s_0_6 794 # ASSIGN : s_0_7 812 # ASSIGN : s_0_8 873 # ASSIGN : s_0_9 921 # ASSIGN : s_1_0 40 # ASSIGN : s_1_1 106 # ASSIGN : s_1_2 186 # ASSIGN : s_1_3 237 # ASSIGN : s_1_4 343 # ASSIGN : s_1_5 385 # ASSIGN : s_1_6 396 # ASSIGN : s_1_7 425 # ASSIGN : s_1_8 477 # ASSIGN : s_1_9 506 # ASSIGN : s_2_0 264 # ASSIGN : s_2_1 424 # ASSIGN : s_2_2 455 # ASSIGN : s_2_3 502 # ASSIGN : s_2_4 512 # ASSIGN : s_2_5 574 # ASSIGN : s_2_6 634 # ASSIGN : s_2_7 748 # ASSIGN : s_2_8 777 # ASSIGN : s_2_9 829 # ASSIGN : s_3_0 133 # ASSIGN : s_3_1 149 # ASSIGN : s_3_2 220 # ASSIGN : s_3_3 288 # ASSIGN : s_3_4 421 # ASSIGN : s_3_5 502 # ASSIGN : s_3_6 551 # ASSIGN : s_3_7 638 # ASSIGN : s_3_8 692 # ASSIGN : s_3_9 712 # ASSIGN : s_4_0 94 # ASSIGN : s_4_1 151 # ASSIGN : s_4_2 196 # ASSIGN : s_4_3 327 # ASSIGN : s_4_4 426 # ASSIGN : s_4_5 472 # ASSIGN : s_4_6 697 # ASSIGN : s_4_7 731 # ASSIGN : s_4_8 769 # ASSIGN : s_4_9 875 # ASSIGN : s_5_0 370 # ASSIGN : s_5_1 395 # ASSIGN : s_5_2 413 # ASSIGN : s_5_3 574 # ASSIGN : s_5_4 678 # ASSIGN : s_5_5 692 # ASSIGN : s_5_6 786 # ASSIGN : s_5_7 806 # ASSIGN : s_5_8 829 # ASSIGN : s_5_9 893 # ASSIGN : s_6_0 9 # ASSIGN : s_6_1 33 # ASSIGN : s_6_2 56 # ASSIGN : s_6_3 103 # ASSIGN : s_6_4 143 # ASSIGN : s_6_5 325 # ASSIGN : s_6_6 413 # ASSIGN : s_6_7 617 # ASSIGN : s_6_8 820 # ASSIGN : s_6_9 917 # ASSIGN : s_7_0 101 # ASSIGN : s_7_1 109 # ASSIGN : s_7_2 116 # ASSIGN : s_7_3 192 # ASSIGN : s_7_4 255 # ASSIGN : s_7_5 364 # ASSIGN : s_7_6 585 # ASSIGN : s_7_7 594 # ASSIGN : s_7_8 699 # ASSIGN : s_7_9 814 # ASSIGN : s_8_0 6 # ASSIGN : s_8_1 54 # ASSIGN : s_8_2 106 # ASSIGN : s_8_3 190 # ASSIGN : s_8_4 225 # ASSIGN : s_8_5 319 # ASSIGN : s_8_6 329 # ASSIGN : s_8_7 436 # ASSIGN : s_8_8 485 # ASSIGN : s_8_9 490 # ASSIGN : s_9_0 275 # ASSIGN : s_9_1 352 # ASSIGN : s_9_2 430 # ASSIGN : s_9_3 520 # ASSIGN : s_9_4 530 # ASSIGN : s_9_5 559 # ASSIGN : s_9_6 596 # ASSIGN : s_9_7 647 # ASSIGN : s_9_8 769 # ASSIGN : s_9_9 911 SHOW_RESULT 932 END : 932 (1 seconds) [Fri Jun 2 08:42:11 2006] SHOW_RESULT 932 CPU : 0.32 = 0.32 + 0 + 0 + 0 # BOUND : makespan 863 932 MODIFY_CNF 897 BEGIN : [Fri Jun 2 08:42:11 2006] MODIFY_CNF 897 END : 26883977 bytes (0 seconds) [Fri Jun 2 08:42:11 2006] MODIFY_CNF 897 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 897 BEGIN : [Fri Jun 2 08:42:11 2006] CMD : minisat /work/tamura/csp2sat29442.cnf /work/tamura/csp2sat29442.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 580566 1696772 | 193522 0 0 NaNQ | 0.000 % | | 100 | 580566 1696772 | 212874 100 875 8.8 | 60.822 % | | 250 | 580566 1696772 | 234161 250 2121 8.5 | 60.822 % | | 476 | 580566 1696772 | 257577 476 3967 8.3 | 60.822 % | | 813 | 580566 1696772 | 283335 813 7022 8.6 | 60.822 % | | 1319 | 580566 1696772 | 311669 1319 10681 8.1 | 60.822 % | | 2078 | 580566 1696772 | 342836 2078 17008 8.2 | 60.822 % | | 3217 | 562535 1644250 | 377119 2607 21918 8.4 | 63.985 % | ==============================================================================) restarts : 8 conflicts : 3678 (405 /sec) decisions : 4994 (549 /sec) propagations : 20734121 (2280989 /sec) inspects : 141488649 (15565359 /sec) conflict literals : 30776 (31.58 % deleted) CPU time : 9.08997 s UNSATISFIABLE VERIFY_CNF 897 END : (9 seconds) [Fri Jun 2 08:42:20 2006] VERIFY_CNF 897 CPU : 9.41 = 0.00999999999999801 + 0 + 9.36 + 0.04 # RESULT : makespan 897 UNSATISFIABLE # BOUND : makespan 898 932 MODIFY_CNF 915 BEGIN : [Fri Jun 2 08:42:20 2006] MODIFY_CNF 915 END : 26883977 bytes (0 seconds) [Fri Jun 2 08:42:20 2006] MODIFY_CNF 915 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 915 BEGIN : [Fri Jun 2 08:42:20 2006] CMD : minisat /work/tamura/csp2sat29442.cnf /work/tamura/csp2sat29442.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 598584 1749008 | 199528 0 0 NaNQ | 0.000 % | | 101 | 598584 1749008 | 219480 101 1041 10.3 | 59.250 % | | 251 | 598584 1749008 | 241428 251 2526 10.1 | 59.250 % | | 477 | 598584 1749008 | 265571 477 4780 10.0 | 59.250 % | | 814 | 598584 1749008 | 292128 814 8309 10.2 | 59.250 % | ==============================================================================) restarts : 5 conflicts : 873 (246 /sec) decisions : 1396 (394 /sec) propagations : 5594697 (1579514 /sec) inspects : 40568200 (11453356 /sec) conflict literals : 8802 (29.07 % deleted) CPU time : 3.54204 s SATISFIABLE VERIFY_CNF 915 END : (4 seconds) [Fri Jun 2 08:42:24 2006] VERIFY_CNF 915 CPU : 4 = 0 + 0.01 + 3.89 + 0.1 # RESULT : makespan 915 SATISFIABLE SHOW_RESULT 915 BEGIN : [Fri Jun 2 08:42:24 2006] # ASSIGN : makespan 915 # ASSIGN : s_0_0 290 # ASSIGN : s_0_1 384 # ASSIGN : s_0_2 458 # ASSIGN : s_0_3 573 # ASSIGN : s_0_4 602 # ASSIGN : s_0_5 750 # ASSIGN : s_0_6 777 # ASSIGN : s_0_7 795 # ASSIGN : s_0_8 856 # ASSIGN : s_0_9 904 # ASSIGN : s_1_0 115 # ASSIGN : s_1_1 207 # ASSIGN : s_1_2 252 # ASSIGN : s_1_3 303 # ASSIGN : s_1_4 348 # ASSIGN : s_1_5 422 # ASSIGN : s_1_6 433 # ASSIGN : s_1_7 532 # ASSIGN : s_1_8 584 # ASSIGN : s_1_9 651 # ASSIGN : s_2_0 88 # ASSIGN : s_2_1 176 # ASSIGN : s_2_2 241 # ASSIGN : s_2_3 288 # ASSIGN : s_2_4 321 # ASSIGN : s_2_5 383 # ASSIGN : s_2_6 462 # ASSIGN : s_2_7 532 # ASSIGN : s_2_8 561 # ASSIGN : s_2_9 613 # ASSIGN : s_3_0 20 # ASSIGN : s_3_1 81 # ASSIGN : s_3_2 178 # ASSIGN : s_3_3 233 # ASSIGN : s_3_4 292 # ASSIGN : s_3_5 301 # ASSIGN : s_3_6 350 # ASSIGN : s_3_7 443 # ASSIGN : s_3_8 497 # ASSIGN : s_3_9 504 # ASSIGN : s_4_0 39 # ASSIGN : s_4_1 46 # ASSIGN : s_4_2 106 # ASSIGN : s_4_3 198 # ASSIGN : s_4_4 644 # ASSIGN : s_4_5 690 # ASSIGN : s_4_6 769 # ASSIGN : s_4_7 810 # ASSIGN : s_4_8 848 # ASSIGN : s_4_9 897 # ASSIGN : s_5_0 359 # ASSIGN : s_5_1 385 # ASSIGN : s_5_2 390 # ASSIGN : s_5_3 479 # ASSIGN : s_5_4 577 # ASSIGN : s_5_5 591 # ASSIGN : s_5_6 685 # ASSIGN : s_5_7 705 # ASSIGN : s_5_8 739 # ASSIGN : s_5_9 858 # ASSIGN : s_6_0 152 # ASSIGN : s_6_1 231 # ASSIGN : s_6_2 298 # ASSIGN : s_6_3 345 # ASSIGN : s_6_4 385 # ASSIGN : s_6_5 520 # ASSIGN : s_6_6 639 # ASSIGN : s_6_7 728 # ASSIGN : s_6_8 803 # ASSIGN : s_6_9 900 # ASSIGN : s_7_0 1 # ASSIGN : s_7_1 6 # ASSIGN : s_7_2 13 # ASSIGN : s_7_3 87 # ASSIGN : s_7_4 126 # ASSIGN : s_7_5 322 # ASSIGN : s_7_6 403 # ASSIGN : s_7_7 412 # ASSIGN : s_7_8 465 # ASSIGN : s_7_9 797 # ASSIGN : s_8_0 2 # ASSIGN : s_8_1 36 # ASSIGN : s_8_2 89 # ASSIGN : s_8_3 227 # ASSIGN : s_8_4 250 # ASSIGN : s_8_5 344 # ASSIGN : s_8_6 476 # ASSIGN : s_8_7 543 # ASSIGN : s_8_8 630 # ASSIGN : s_8_9 635 # ASSIGN : s_9_0 426 # ASSIGN : s_9_1 503 # ASSIGN : s_9_2 596 # ASSIGN : s_9_3 678 # ASSIGN : s_9_4 688 # ASSIGN : s_9_5 717 # ASSIGN : s_9_6 732 # ASSIGN : s_9_7 783 # ASSIGN : s_9_8 857 # ASSIGN : s_9_9 894 SHOW_RESULT 915 END : 915 (1 seconds) [Fri Jun 2 08:42:25 2006] SHOW_RESULT 915 CPU : 0.330000000000005 = 0.330000000000005 + 0 + 0 + 0 # BOUND : makespan 898 915 MODIFY_CNF 906 BEGIN : [Fri Jun 2 08:42:25 2006] MODIFY_CNF 906 END : 26883977 bytes (0 seconds) [Fri Jun 2 08:42:25 2006] MODIFY_CNF 906 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 906 BEGIN : [Fri Jun 2 08:42:25 2006] CMD : minisat /work/tamura/csp2sat29442.cnf /work/tamura/csp2sat29442.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 589575 1722890 | 196525 0 0 NaNQ | 0.000 % | | 102 | 589575 1722890 | 216177 102 1274 12.5 | 60.036 % | | 252 | 589575 1722890 | 237795 252 2679 10.6 | 60.036 % | | 479 | 589575 1722890 | 261574 479 4844 10.1 | 60.036 % | ==============================================================================) restarts : 4 conflicts : 681 (246 /sec) decisions : 1084 (392 /sec) propagations : 3704389 (1340070 /sec) inspects : 26385613 (9545047 /sec) conflict literals : 6580 (22.92 % deleted) CPU time : 2.76432 s SATISFIABLE VERIFY_CNF 906 END : (3 seconds) [Fri Jun 2 08:42:28 2006] VERIFY_CNF 906 CPU : 3.24 = 0 + 0.01 + 3.12 + 0.11 # RESULT : makespan 906 SATISFIABLE SHOW_RESULT 906 BEGIN : [Fri Jun 2 08:42:28 2006] # ASSIGN : makespan 906 # ASSIGN : s_0_0 318 # ASSIGN : s_0_1 447 # ASSIGN : s_0_2 521 # ASSIGN : s_0_3 566 # ASSIGN : s_0_4 616 # ASSIGN : s_0_5 692 # ASSIGN : s_0_6 711 # ASSIGN : s_0_7 775 # ASSIGN : s_0_8 836 # ASSIGN : s_0_9 895 # ASSIGN : s_1_0 215 # ASSIGN : s_1_1 299 # ASSIGN : s_1_2 361 # ASSIGN : s_1_3 412 # ASSIGN : s_1_4 470 # ASSIGN : s_1_5 512 # ASSIGN : s_1_6 580 # ASSIGN : s_1_7 640 # ASSIGN : s_1_8 719 # ASSIGN : s_1_9 748 # ASSIGN : s_2_0 254 # ASSIGN : s_2_1 342 # ASSIGN : s_2_2 373 # ASSIGN : s_2_3 420 # ASSIGN : s_2_4 430 # ASSIGN : s_2_5 504 # ASSIGN : s_2_6 609 # ASSIGN : s_2_7 667 # ASSIGN : s_2_8 696 # ASSIGN : s_2_9 750 # ASSIGN : s_3_0 10 # ASSIGN : s_3_1 26 # ASSIGN : s_3_2 119 # ASSIGN : s_3_3 189 # ASSIGN : s_3_4 309 # ASSIGN : s_3_5 318 # ASSIGN : s_3_6 367 # ASSIGN : s_3_7 450 # ASSIGN : s_3_8 568 # ASSIGN : s_3_9 577 # ASSIGN : s_4_0 140 # ASSIGN : s_4_1 174 # ASSIGN : s_4_2 244 # ASSIGN : s_4_3 589 # ASSIGN : s_4_4 683 # ASSIGN : s_4_5 729 # ASSIGN : s_4_6 808 # ASSIGN : s_4_7 842 # ASSIGN : s_4_8 880 # ASSIGN : s_4_9 888 # ASSIGN : s_5_0 1 # ASSIGN : s_5_1 37 # ASSIGN : s_5_2 44 # ASSIGN : s_5_3 133 # ASSIGN : s_5_4 233 # ASSIGN : s_5_5 252 # ASSIGN : s_5_6 346 # ASSIGN : s_5_7 366 # ASSIGN : s_5_8 450 # ASSIGN : s_5_9 849 # ASSIGN : s_6_0 97 # ASSIGN : s_6_1 121 # ASSIGN : s_6_2 142 # ASSIGN : s_6_3 278 # ASSIGN : s_6_4 318 # ASSIGN : s_6_5 452 # ASSIGN : s_6_6 523 # ASSIGN : s_6_7 612 # ASSIGN : s_6_8 711 # ASSIGN : s_6_9 891 # ASSIGN : s_7_0 147 # ASSIGN : s_7_1 247 # ASSIGN : s_7_2 346 # ASSIGN : s_7_3 464 # ASSIGN : s_7_4 492 # ASSIGN : s_7_5 564 # ASSIGN : s_7_6 625 # ASSIGN : s_7_7 634 # ASSIGN : s_7_8 687 # ASSIGN : s_7_9 809 # ASSIGN : s_8_0 3 # ASSIGN : s_8_1 44 # ASSIGN : s_8_2 96 # ASSIGN : s_8_3 136 # ASSIGN : s_8_4 152 # ASSIGN : s_8_5 246 # ASSIGN : s_8_6 262 # ASSIGN : s_8_7 389 # ASSIGN : s_8_8 430 # ASSIGN : s_8_9 494 # ASSIGN : s_9_0 42 # ASSIGN : s_9_1 153 # ASSIGN : s_9_2 227 # ASSIGN : s_9_3 336 # ASSIGN : s_9_4 406 # ASSIGN : s_9_5 435 # ASSIGN : s_9_6 459 # ASSIGN : s_9_7 510 # ASSIGN : s_9_8 575 # ASSIGN : s_9_9 690 SHOW_RESULT 906 END : 906 (0 seconds) [Fri Jun 2 08:42:28 2006] SHOW_RESULT 906 CPU : 0.309999999999995 = 0.309999999999995 + 0 + 0 + 0 # BOUND : makespan 898 906 MODIFY_CNF 902 BEGIN : [Fri Jun 2 08:42:28 2006] MODIFY_CNF 902 END : 26883977 bytes (0 seconds) [Fri Jun 2 08:42:28 2006] MODIFY_CNF 902 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 902 BEGIN : [Fri Jun 2 08:42:28 2006] CMD : minisat /work/tamura/csp2sat29442.cnf /work/tamura/csp2sat29442.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 585571 1711282 | 195190 0 0 NaNQ | 0.000 % | | 101 | 585571 1711282 | 214709 101 1029 10.2 | 60.385 % | | 251 | 585571 1711282 | 236179 251 2156 8.6 | 60.385 % | ==============================================================================) restarts : 3 conflicts : 472 (198 /sec) decisions : 869 (364 /sec) propagations : 2845072 (1191415 /sec) inspects : 18988248 (7951601 /sec) conflict literals : 3918 (25.89 % deleted) CPU time : 2.38798 s SATISFIABLE VERIFY_CNF 902 END : (3 seconds) [Fri Jun 2 08:42:31 2006] VERIFY_CNF 902 CPU : 2.84 = 0.0100000000000051 + 0.01 + 2.72 + 0.1 # RESULT : makespan 902 SATISFIABLE SHOW_RESULT 902 BEGIN : [Fri Jun 2 08:42:31 2006] # ASSIGN : makespan 902 # ASSIGN : s_0_0 316 # ASSIGN : s_0_1 443 # ASSIGN : s_0_2 517 # ASSIGN : s_0_3 562 # ASSIGN : s_0_4 612 # ASSIGN : s_0_5 688 # ASSIGN : s_0_6 707 # ASSIGN : s_0_7 771 # ASSIGN : s_0_8 832 # ASSIGN : s_0_9 891 # ASSIGN : s_1_0 213 # ASSIGN : s_1_1 297 # ASSIGN : s_1_2 359 # ASSIGN : s_1_3 410 # ASSIGN : s_1_4 451 # ASSIGN : s_1_5 510 # ASSIGN : s_1_6 576 # ASSIGN : s_1_7 633 # ASSIGN : s_1_8 685 # ASSIGN : s_1_9 744 # ASSIGN : s_2_0 252 # ASSIGN : s_2_1 340 # ASSIGN : s_2_2 371 # ASSIGN : s_2_3 418 # ASSIGN : s_2_4 428 # ASSIGN : s_2_5 509 # ASSIGN : s_2_6 605 # ASSIGN : s_2_7 663 # ASSIGN : s_2_8 692 # ASSIGN : s_2_9 746 # ASSIGN : s_3_0 26 # ASSIGN : s_3_1 48 # ASSIGN : s_3_2 119 # ASSIGN : s_3_3 174 # ASSIGN : s_3_4 307 # ASSIGN : s_3_5 318 # ASSIGN : s_3_6 367 # ASSIGN : s_3_7 455 # ASSIGN : s_3_8 528 # ASSIGN : s_3_9 538 # ASSIGN : s_4_0 414 # ASSIGN : s_4_1 421 # ASSIGN : s_4_2 493 # ASSIGN : s_4_3 585 # ASSIGN : s_4_4 679 # ASSIGN : s_4_5 725 # ASSIGN : s_4_6 804 # ASSIGN : s_4_7 838 # ASSIGN : s_4_8 876 # ASSIGN : s_4_9 884 # ASSIGN : s_5_0 12 # ASSIGN : s_5_1 37 # ASSIGN : s_5_2 42 # ASSIGN : s_5_3 131 # ASSIGN : s_5_4 231 # ASSIGN : s_5_5 273 # ASSIGN : s_5_6 429 # ASSIGN : s_5_7 572 # ASSIGN : s_5_8 595 # ASSIGN : s_5_9 845 # ASSIGN : s_6_0 133 # ASSIGN : s_6_1 208 # ASSIGN : s_6_2 229 # ASSIGN : s_6_3 276 # ASSIGN : s_6_4 316 # ASSIGN : s_6_5 450 # ASSIGN : s_6_6 521 # ASSIGN : s_6_7 610 # ASSIGN : s_6_8 707 # ASSIGN : s_6_9 887 # ASSIGN : s_7_0 157 # ASSIGN : s_7_1 245 # ASSIGN : s_7_2 344 # ASSIGN : s_7_3 462 # ASSIGN : s_7_4 490 # ASSIGN : s_7_5 569 # ASSIGN : s_7_6 630 # ASSIGN : s_7_7 639 # ASSIGN : s_7_8 714 # ASSIGN : s_7_9 805 # ASSIGN : s_8_0 3 # ASSIGN : s_8_1 42 # ASSIGN : s_8_2 94 # ASSIGN : s_8_3 156 # ASSIGN : s_8_4 162 # ASSIGN : s_8_5 256 # ASSIGN : s_8_6 262 # ASSIGN : s_8_7 408 # ASSIGN : s_8_8 449 # ASSIGN : s_8_9 454 # ASSIGN : s_9_0 42 # ASSIGN : s_9_1 134 # ASSIGN : s_9_2 225 # ASSIGN : s_9_3 334 # ASSIGN : s_9_4 375 # ASSIGN : s_9_5 404 # ASSIGN : s_9_6 419 # ASSIGN : s_9_7 470 # ASSIGN : s_9_8 535 # ASSIGN : s_9_9 686 SHOW_RESULT 902 END : 902 (0 seconds) [Fri Jun 2 08:42:31 2006] SHOW_RESULT 902 CPU : 0.309999999999995 = 0.309999999999995 + 0 + 0 + 0 # BOUND : makespan 898 902 MODIFY_CNF 900 BEGIN : [Fri Jun 2 08:42:31 2006] MODIFY_CNF 900 END : 26883977 bytes (0 seconds) [Fri Jun 2 08:42:31 2006] MODIFY_CNF 900 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 900 BEGIN : [Fri Jun 2 08:42:31 2006] CMD : minisat /work/tamura/csp2sat29442.cnf /work/tamura/csp2sat29442.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 583569 1705478 | 194523 0 0 NaNQ | 0.000 % | | 100 | 583569 1705478 | 213975 100 1131 11.3 | 60.560 % | | 250 | 583569 1705478 | 235372 250 2383 9.5 | 60.560 % | | 476 | 583569 1705478 | 258910 476 4440 9.3 | 60.560 % | | 813 | 583569 1705478 | 284801 813 7482 9.2 | 60.560 % | ==============================================================================) restarts : 5 conflicts : 827 (257 /sec) decisions : 1328 (413 /sec) propagations : 4972582 (1547243 /sec) inspects : 33174777 (10322492 /sec) conflict literals : 7665 (26.59 % deleted) CPU time : 3.21383 s SATISFIABLE VERIFY_CNF 900 END : (4 seconds) [Fri Jun 2 08:42:35 2006] VERIFY_CNF 900 CPU : 3.67 = 0.00999999999999801 + 0 + 3.55 + 0.11 # RESULT : makespan 900 SATISFIABLE SHOW_RESULT 900 BEGIN : [Fri Jun 2 08:42:35 2006] # ASSIGN : makespan 900 # ASSIGN : s_0_0 314 # ASSIGN : s_0_1 441 # ASSIGN : s_0_2 515 # ASSIGN : s_0_3 560 # ASSIGN : s_0_4 610 # ASSIGN : s_0_5 686 # ASSIGN : s_0_6 705 # ASSIGN : s_0_7 769 # ASSIGN : s_0_8 830 # ASSIGN : s_0_9 889 # ASSIGN : s_1_0 132 # ASSIGN : s_1_1 283 # ASSIGN : s_1_2 357 # ASSIGN : s_1_3 408 # ASSIGN : s_1_4 449 # ASSIGN : s_1_5 508 # ASSIGN : s_1_6 574 # ASSIGN : s_1_7 631 # ASSIGN : s_1_8 683 # ASSIGN : s_1_9 742 # ASSIGN : s_2_0 238 # ASSIGN : s_2_1 326 # ASSIGN : s_2_2 369 # ASSIGN : s_2_3 416 # ASSIGN : s_2_4 426 # ASSIGN : s_2_5 502 # ASSIGN : s_2_6 603 # ASSIGN : s_2_7 661 # ASSIGN : s_2_8 690 # ASSIGN : s_2_9 744 # ASSIGN : s_3_0 102 # ASSIGN : s_3_1 118 # ASSIGN : s_3_2 195 # ASSIGN : s_3_3 250 # ASSIGN : s_3_4 305 # ASSIGN : s_3_5 316 # ASSIGN : s_3_6 365 # ASSIGN : s_3_7 448 # ASSIGN : s_3_8 514 # ASSIGN : s_3_9 564 # ASSIGN : s_4_0 434 # ASSIGN : s_4_1 450 # ASSIGN : s_4_2 491 # ASSIGN : s_4_3 583 # ASSIGN : s_4_4 677 # ASSIGN : s_4_5 723 # ASSIGN : s_4_6 802 # ASSIGN : s_4_7 836 # ASSIGN : s_4_8 874 # ASSIGN : s_4_9 882 # ASSIGN : s_5_0 10 # ASSIGN : s_5_1 35 # ASSIGN : s_5_2 40 # ASSIGN : s_5_3 129 # ASSIGN : s_5_4 224 # ASSIGN : s_5_5 265 # ASSIGN : s_5_6 412 # ASSIGN : s_5_7 432 # ASSIGN : s_5_8 455 # ASSIGN : s_5_9 843 # ASSIGN : s_6_0 89 # ASSIGN : s_6_1 121 # ASSIGN : s_6_2 203 # ASSIGN : s_6_3 274 # ASSIGN : s_6_4 314 # ASSIGN : s_6_5 448 # ASSIGN : s_6_6 519 # ASSIGN : s_6_7 608 # ASSIGN : s_6_8 705 # ASSIGN : s_6_9 885 # ASSIGN : s_7_0 113 # ASSIGN : s_7_1 142 # ASSIGN : s_7_2 342 # ASSIGN : s_7_3 422 # ASSIGN : s_7_4 488 # ASSIGN : s_7_5 567 # ASSIGN : s_7_6 628 # ASSIGN : s_7_7 637 # ASSIGN : s_7_8 712 # ASSIGN : s_7_9 803 # ASSIGN : s_8_0 1 # ASSIGN : s_8_1 40 # ASSIGN : s_8_2 92 # ASSIGN : s_8_3 183 # ASSIGN : s_8_4 189 # ASSIGN : s_8_5 359 # ASSIGN : s_8_6 452 # ASSIGN : s_8_7 521 # ASSIGN : s_8_8 562 # ASSIGN : s_8_9 621 # ASSIGN : s_9_0 55 # ASSIGN : s_9_1 149 # ASSIGN : s_9_2 223 # ASSIGN : s_9_3 332 # ASSIGN : s_9_4 357 # ASSIGN : s_9_5 386 # ASSIGN : s_9_6 401 # ASSIGN : s_9_7 499 # ASSIGN : s_9_8 571 # ASSIGN : s_9_9 684 SHOW_RESULT 900 END : 900 (0 seconds) [Fri Jun 2 08:42:35 2006] SHOW_RESULT 900 CPU : 0.319999999999995 = 0.309999999999995 + 0.00999999999999998 + 0 + 0 # BOUND : makespan 898 900 MODIFY_CNF 899 BEGIN : [Fri Jun 2 08:42:35 2006] MODIFY_CNF 899 END : 26883977 bytes (0 seconds) [Fri Jun 2 08:42:35 2006] MODIFY_CNF 899 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 899 BEGIN : [Fri Jun 2 08:42:35 2006] CMD : minisat /work/tamura/csp2sat29442.cnf /work/tamura/csp2sat29442.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 582568 1702576 | 194189 0 0 NaNQ | 0.000 % | | 100 | 582568 1702576 | 213607 100 1161 11.6 | 60.647 % | | 251 | 582568 1702576 | 234968 251 2405 9.6 | 60.647 % | | 476 | 582568 1702576 | 258465 476 3979 8.4 | 60.647 % | ==============================================================================) restarts : 4 conflicts : 675 (246 /sec) decisions : 1088 (396 /sec) propagations : 3792312 (1380006 /sec) inspects : 25372498 (9232940 /sec) conflict literals : 5609 (26.63 % deleted) CPU time : 2.74804 s SATISFIABLE VERIFY_CNF 899 END : (3 seconds) [Fri Jun 2 08:42:38 2006] VERIFY_CNF 899 CPU : 3.14000000000001 = 0.0100000000000051 + 0 + 3.09 + 0.04 # RESULT : makespan 899 SATISFIABLE SHOW_RESULT 899 BEGIN : [Fri Jun 2 08:42:38 2006] # ASSIGN : makespan 899 # ASSIGN : s_0_0 303 # ASSIGN : s_0_1 358 # ASSIGN : s_0_2 432 # ASSIGN : s_0_3 477 # ASSIGN : s_0_4 609 # ASSIGN : s_0_5 685 # ASSIGN : s_0_6 704 # ASSIGN : s_0_7 768 # ASSIGN : s_0_8 829 # ASSIGN : s_0_9 888 # ASSIGN : s_1_0 40 # ASSIGN : s_1_1 106 # ASSIGN : s_1_2 171 # ASSIGN : s_1_3 222 # ASSIGN : s_1_4 292 # ASSIGN : s_1_5 334 # ASSIGN : s_1_6 345 # ASSIGN : s_1_7 374 # ASSIGN : s_1_8 520 # ASSIGN : s_1_9 550 # ASSIGN : s_2_0 239 # ASSIGN : s_2_1 327 # ASSIGN : s_2_2 358 # ASSIGN : s_2_3 405 # ASSIGN : s_2_4 415 # ASSIGN : s_2_5 489 # ASSIGN : s_2_6 549 # ASSIGN : s_2_7 625 # ASSIGN : s_2_8 654 # ASSIGN : s_2_9 706 # ASSIGN : s_3_0 133 # ASSIGN : s_3_1 149 # ASSIGN : s_3_2 220 # ASSIGN : s_3_3 350 # ASSIGN : s_3_4 406 # ASSIGN : s_3_5 417 # ASSIGN : s_3_6 466 # ASSIGN : s_3_7 568 # ASSIGN : s_3_8 622 # ASSIGN : s_3_9 772 # ASSIGN : s_4_0 442 # ASSIGN : s_4_1 449 # ASSIGN : s_4_2 490 # ASSIGN : s_4_3 582 # ASSIGN : s_4_4 676 # ASSIGN : s_4_5 722 # ASSIGN : s_4_6 801 # ASSIGN : s_4_7 835 # ASSIGN : s_4_8 873 # ASSIGN : s_4_9 881 # ASSIGN : s_5_0 9 # ASSIGN : s_5_1 34 # ASSIGN : s_5_2 39 # ASSIGN : s_5_3 128 # ASSIGN : s_5_4 225 # ASSIGN : s_5_5 245 # ASSIGN : s_5_6 354 # ASSIGN : s_5_7 429 # ASSIGN : s_5_8 452 # ASSIGN : s_5_9 497 # ASSIGN : s_6_0 82 # ASSIGN : s_6_1 112 # ASSIGN : s_6_2 133 # ASSIGN : s_6_3 180 # ASSIGN : s_6_4 240 # ASSIGN : s_6_5 395 # ASSIGN : s_6_6 536 # ASSIGN : s_6_7 629 # ASSIGN : s_6_8 704 # ASSIGN : s_6_9 884 # ASSIGN : s_7_0 77 # ASSIGN : s_7_1 164 # ASSIGN : s_7_2 201 # ASSIGN : s_7_3 275 # ASSIGN : s_7_4 334 # ASSIGN : s_7_5 426 # ASSIGN : s_7_6 487 # ASSIGN : s_7_7 496 # ASSIGN : s_7_8 549 # ASSIGN : s_7_9 607 # ASSIGN : s_8_0 0 # ASSIGN : s_8_1 39 # ASSIGN : s_8_2 91 # ASSIGN : s_8_3 195 # ASSIGN : s_8_4 233 # ASSIGN : s_8_5 339 # ASSIGN : s_8_6 361 # ASSIGN : s_8_7 581 # ASSIGN : s_8_8 633 # ASSIGN : s_8_9 638 # ASSIGN : s_9_0 103 # ASSIGN : s_9_1 358 # ASSIGN : s_9_2 500 # ASSIGN : s_9_3 599 # ASSIGN : s_9_4 612 # ASSIGN : s_9_5 641 # ASSIGN : s_9_6 656 # ASSIGN : s_9_7 707 # ASSIGN : s_9_8 798 # ASSIGN : s_9_9 878 SHOW_RESULT 899 END : 899 (1 seconds) [Fri Jun 2 08:42:39 2006] SHOW_RESULT 899 CPU : 0.309999999999995 = 0.309999999999995 + 0 + 0 + 0 # BOUND : makespan 898 899 MODIFY_CNF 898 BEGIN : [Fri Jun 2 08:42:39 2006] MODIFY_CNF 898 END : 26883977 bytes (0 seconds) [Fri Jun 2 08:42:39 2006] MODIFY_CNF 898 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 898 BEGIN : [Fri Jun 2 08:42:39 2006] CMD : minisat /work/tamura/csp2sat29442.cnf /work/tamura/csp2sat29442.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 581567 1699674 | 193855 0 0 NaNQ | 0.000 % | | 100 | 581567 1699674 | 213240 100 1078 10.8 | 60.734 % | | 250 | 581567 1699674 | 234564 250 2114 8.5 | 60.734 % | | 476 | 581567 1699674 | 258021 476 3925 8.2 | 60.734 % | | 815 | 581567 1699674 | 283823 815 7513 9.2 | 60.734 % | | 1322 | 581567 1699674 | 312205 1322 11617 8.8 | 60.734 % | | 2081 | 581567 1699674 | 343425 2081 20391 9.8 | 60.734 % | | 3220 | 581567 1699674 | 377768 3220 31745 9.9 | 60.734 % | ==============================================================================) restarts : 8 conflicts : 3665 (423 /sec) decisions : 5015 (579 /sec) propagations : 19148377 (2208860 /sec) inspects : 135818213 (15667302 /sec) conflict literals : 35186 (29.80 % deleted) CPU time : 8.6689 s UNSATISFIABLE VERIFY_CNF 898 END : (9 seconds) [Fri Jun 2 08:42:48 2006] VERIFY_CNF 898 CPU : 9.06 = 0.0100000000000051 + 0.01 + 8.93 + 0.11 # RESULT : makespan 898 UNSATISFIABLE # BOUND : makespan 899 899 MAIN END : (105 seconds) [Fri Jun 2 08:42:48 2006] MAIN CPU : 104.24 = 62.21 + 0.15 + 41.11 + 0.77