MAIN BEGIN : [Fri Jun 2 08:33:18 2006] READ BEGIN : csp/orb04.csp [Fri Jun 2 08:33:18 2006] READ END : csp/orb04.csp (1 seconds) [Fri Jun 2 08:33:19 2006] READ CPU : 1.39 = 1.39 + 0 + 0 + 0 # BOUND : makespan 759 1356 GENERATE_CNF 1356 BEGIN : [Fri Jun 2 08:33:19 2006] GENERATE_CNF 1356 END : 137399 variables 1431686 clauses 32373746 bytes (70 seconds) [Fri Jun 2 08:34:29 2006] GENERATE_CNF 1356 CPU : 69.16 = 69.06 + 0.1 + 0 + 0 MODIFY_CNF 1057 BEGIN : [Fri Jun 2 08:34:29 2006] MODIFY_CNF 1057 END : 32373752 bytes (0 seconds) [Fri Jun 2 08:34:29 2006] MODIFY_CNF 1057 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1057 BEGIN : [Fri Jun 2 08:34:29 2006] CMD : minisat /work/tamura/csp2sat54962.cnf /work/tamura/csp2sat54962.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 639987 1869759 | 213329 0 0 NaNQ | 0.000 % | ==============================================================================) restarts : 1 conflicts : 2 (1 /sec) decisions : 129 (73 /sec) propagations : 142303 (80587 /sec) inspects : 857914 (485842 /sec) conflict literals : 12 (0.00 % deleted) CPU time : 1.76583 s SATISFIABLE VERIFY_CNF 1057 END : (2 seconds) [Fri Jun 2 08:34:31 2006] VERIFY_CNF 1057 CPU : 2.19999999999999 = 0.00999999999999091 + 0 + 2.16 + 0.03 # RESULT : makespan 1057 SATISFIABLE SHOW_RESULT 1057 BEGIN : [Fri Jun 2 08:34:31 2006] # ASSIGN : makespan 1057 # ASSIGN : s_0_0 34 # ASSIGN : s_0_1 130 # ASSIGN : s_0_2 245 # ASSIGN : s_0_3 280 # ASSIGN : s_0_4 414 # ASSIGN : s_0_5 429 # ASSIGN : s_0_6 566 # ASSIGN : s_0_7 743 # ASSIGN : s_0_8 911 # ASSIGN : s_0_9 961 # ASSIGN : s_1_0 242 # ASSIGN : s_1_1 353 # ASSIGN : s_1_2 441 # ASSIGN : s_1_3 521 # ASSIGN : s_1_4 581 # ASSIGN : s_1_5 680 # ASSIGN : s_1_6 719 # ASSIGN : s_1_7 804 # ASSIGN : s_1_8 832 # ASSIGN : s_1_9 907 # ASSIGN : s_2_0 190 # ASSIGN : s_2_1 269 # ASSIGN : s_2_2 291 # ASSIGN : s_2_3 324 # ASSIGN : s_2_4 392 # ASSIGN : s_2_5 461 # ASSIGN : s_2_6 543 # ASSIGN : s_2_7 578 # ASSIGN : s_2_8 906 # ASSIGN : s_2_9 973 # ASSIGN : s_3_0 3 # ASSIGN : s_3_1 36 # ASSIGN : s_3_2 121 # ASSIGN : s_3_3 176 # ASSIGN : s_3_4 307 # ASSIGN : s_3_5 365 # ASSIGN : s_3_6 376 # ASSIGN : s_3_7 445 # ASSIGN : s_3_8 629 # ASSIGN : s_3_9 1032 # ASSIGN : s_4_0 42 # ASSIGN : s_4_1 139 # ASSIGN : s_4_2 262 # ASSIGN : s_4_3 419 # ASSIGN : s_4_4 472 # ASSIGN : s_4_5 612 # ASSIGN : s_4_6 702 # ASSIGN : s_4_7 800 # ASSIGN : s_4_8 967 # ASSIGN : s_4_9 1017 # ASSIGN : s_5_0 140 # ASSIGN : s_5_1 237 # ASSIGN : s_5_2 305 # ASSIGN : s_5_3 349 # ASSIGN : s_5_4 417 # ASSIGN : s_5_5 466 # ASSIGN : s_5_6 551 # ASSIGN : s_5_7 636 # ASSIGN : s_5_8 930 # ASSIGN : s_5_9 976 # ASSIGN : s_6_0 146 # ASSIGN : s_6_1 180 # ASSIGN : s_6_2 256 # ASSIGN : s_6_3 304 # ASSIGN : s_6_4 416 # ASSIGN : s_6_5 669 # ASSIGN : s_6_6 767 # ASSIGN : s_6_7 908 # ASSIGN : s_6_8 1006 # ASSIGN : s_6_9 1013 # ASSIGN : s_7_0 370 # ASSIGN : s_7_1 427 # ASSIGN : s_7_2 432 # ASSIGN : s_7_3 517 # ASSIGN : s_7_4 568 # ASSIGN : s_7_5 626 # ASSIGN : s_7_6 705 # ASSIGN : s_7_7 831 # ASSIGN : s_7_8 887 # ASSIGN : s_7_9 984 # ASSIGN : s_8_0 414 # ASSIGN : s_8_1 438 # ASSIGN : s_8_2 501 # ASSIGN : s_8_3 549 # ASSIGN : s_8_4 653 # ASSIGN : s_8_5 726 # ASSIGN : s_8_6 800 # ASSIGN : s_8_7 863 # ASSIGN : s_8_8 880 # ASSIGN : s_8_9 973 # ASSIGN : s_9_0 478 # ASSIGN : s_9_1 529 # ASSIGN : s_9_2 534 # ASSIGN : s_9_3 574 # ASSIGN : s_9_4 634 # ASSIGN : s_9_5 695 # ASSIGN : s_9_6 753 # ASSIGN : s_9_7 807 # ASSIGN : s_9_8 879 # ASSIGN : s_9_9 963 SHOW_RESULT 1057 END : 1057 (0 seconds) [Fri Jun 2 08:34:31 2006] SHOW_RESULT 1057 CPU : 0.370000000000005 = 0.370000000000005 + 0 + 0 + 0 # BOUND : makespan 759 1057 MODIFY_CNF 908 BEGIN : [Fri Jun 2 08:34:31 2006] MODIFY_CNF 908 END : 32373752 bytes (0 seconds) [Fri Jun 2 08:34:31 2006] MODIFY_CNF 908 CPU : 0.0100000000000051 = 0.0100000000000051 + 0 + 0 + 0 VERIFY_CNF 908 BEGIN : [Fri Jun 2 08:34:31 2006] CMD : minisat /work/tamura/csp2sat54962.cnf /work/tamura/csp2sat54962.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 445857 1302515 | 148619 0 0 NaNQ | 0.000 % | ==============================================================================) restarts : 1 conflicts : 20 (10 /sec) decisions : 29 (15 /sec) propagations : 243642 (124098 /sec) inspects : 1271548 (647657 /sec) conflict literals : 51 (30.14 % deleted) CPU time : 1.9633 s UNSATISFIABLE VERIFY_CNF 908 END : (3 seconds) [Fri Jun 2 08:34:34 2006] VERIFY_CNF 908 CPU : 2.32 = 0 + 0.01 + 2.27 + 0.04 # RESULT : makespan 908 UNSATISFIABLE # BOUND : makespan 909 1057 MODIFY_CNF 983 BEGIN : [Fri Jun 2 08:34:34 2006] MODIFY_CNF 983 END : 32373752 bytes (0 seconds) [Fri Jun 2 08:34:34 2006] MODIFY_CNF 983 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 983 BEGIN : [Fri Jun 2 08:34:34 2006] CMD : minisat /work/tamura/csp2sat54962.cnf /work/tamura/csp2sat54962.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 544019 1589370 | 181339 0 0 NaNQ | 0.000 % | | 100 | 544019 1589370 | 199472 100 827 8.3 | 68.681 % | | 250 | 519357 1516730 | 219420 156 1104 7.1 | 69.793 % | ==============================================================================) restarts : 3 conflicts : 386 (132 /sec) decisions : 575 (197 /sec) propagations : 2902306 (996055 /sec) inspects : 17049310 (5851229 /sec) conflict literals : 2668 (34.72 % deleted) CPU time : 2.9138 s UNSATISFIABLE VERIFY_CNF 983 END : (3 seconds) [Fri Jun 2 08:34:37 2006] VERIFY_CNF 983 CPU : 3.29 = 0 + 0.01 + 3.24 + 0.04 # RESULT : makespan 983 UNSATISFIABLE # BOUND : makespan 984 1057 MODIFY_CNF 1020 BEGIN : [Fri Jun 2 08:34:37 2006] MODIFY_CNF 1020 END : 32373752 bytes (0 seconds) [Fri Jun 2 08:34:37 2006] MODIFY_CNF 1020 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1020 BEGIN : [Fri Jun 2 08:34:37 2006] CMD : minisat /work/tamura/csp2sat54962.cnf /work/tamura/csp2sat54962.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 596164 1742040 | 198721 0 0 NaNQ | 0.000 % | | 100 | 596164 1742040 | 218593 100 1387 13.9 | 65.931 % | | 250 | 596164 1742040 | 240452 250 3383 13.5 | 65.931 % | | 475 | 596164 1742040 | 264497 475 6110 12.9 | 65.931 % | | 813 | 596164 1742040 | 290947 813 9727 12.0 | 65.931 % | | 1320 | 596164 1742040 | 320042 1320 17883 13.5 | 65.931 % | ==============================================================================) restarts : 6 conflicts : 1766 (277 /sec) decisions : 2826 (444 /sec) propagations : 11865171 (1863986 /sec) inspects : 85940092 (13500952 /sec) conflict literals : 24967 (29.13 % deleted) CPU time : 6.36548 s SATISFIABLE VERIFY_CNF 1020 END : (7 seconds) [Fri Jun 2 08:34:44 2006] VERIFY_CNF 1020 CPU : 6.88 = 0 + 0 + 6.76 + 0.12 # RESULT : makespan 1020 SATISFIABLE SHOW_RESULT 1020 BEGIN : [Fri Jun 2 08:34:44 2006] # ASSIGN : makespan 1020 # ASSIGN : s_0_0 1 # ASSIGN : s_0_1 193 # ASSIGN : s_0_2 203 # ASSIGN : s_0_3 238 # ASSIGN : s_0_4 282 # ASSIGN : s_0_5 340 # ASSIGN : s_0_6 460 # ASSIGN : s_0_7 763 # ASSIGN : s_0_8 897 # ASSIGN : s_0_9 1008 # ASSIGN : s_1_0 171 # ASSIGN : s_1_1 266 # ASSIGN : s_1_2 373 # ASSIGN : s_1_3 490 # ASSIGN : s_1_4 512 # ASSIGN : s_1_5 691 # ASSIGN : s_1_6 730 # ASSIGN : s_1_7 815 # ASSIGN : s_1_8 852 # ASSIGN : s_1_9 951 # ASSIGN : s_2_0 346 # ASSIGN : s_2_1 398 # ASSIGN : s_2_2 420 # ASSIGN : s_2_3 453 # ASSIGN : s_2_4 573 # ASSIGN : s_2_5 600 # ASSIGN : s_2_6 680 # ASSIGN : s_2_7 705 # ASSIGN : s_2_8 739 # ASSIGN : s_2_9 924 # ASSIGN : s_3_0 140 # ASSIGN : s_3_1 212 # ASSIGN : s_3_2 297 # ASSIGN : s_3_3 352 # ASSIGN : s_3_4 432 # ASSIGN : s_3_5 501 # ASSIGN : s_3_6 530 # ASSIGN : s_3_7 641 # ASSIGN : s_3_8 697 # ASSIGN : s_3_9 995 # ASSIGN : s_4_0 9 # ASSIGN : s_4_1 112 # ASSIGN : s_4_2 218 # ASSIGN : s_4_3 305 # ASSIGN : s_4_4 424 # ASSIGN : s_4_5 509 # ASSIGN : s_4_6 599 # ASSIGN : s_4_7 763 # ASSIGN : s_4_8 930 # ASSIGN : s_4_9 980 # ASSIGN : s_5_0 96 # ASSIGN : s_5_1 210 # ASSIGN : s_5_2 278 # ASSIGN : s_5_3 325 # ASSIGN : s_5_4 392 # ASSIGN : s_5_5 436 # ASSIGN : s_5_6 521 # ASSIGN : s_5_7 599 # ASSIGN : s_5_8 706 # ASSIGN : s_5_9 870 # ASSIGN : s_6_0 106 # ASSIGN : s_6_1 142 # ASSIGN : s_6_2 218 # ASSIGN : s_6_3 363 # ASSIGN : s_6_4 453 # ASSIGN : s_6_5 476 # ASSIGN : s_6_6 837 # ASSIGN : s_6_7 871 # ASSIGN : s_6_8 969 # ASSIGN : s_6_9 976 # ASSIGN : s_7_0 234 # ASSIGN : s_7_1 320 # ASSIGN : s_7_2 384 # ASSIGN : s_7_3 480 # ASSIGN : s_7_4 531 # ASSIGN : s_7_5 589 # ASSIGN : s_7_6 668 # ASSIGN : s_7_7 767 # ASSIGN : s_7_8 850 # ASSIGN : s_7_9 947 # ASSIGN : s_8_0 322 # ASSIGN : s_8_1 357 # ASSIGN : s_8_2 464 # ASSIGN : s_8_3 512 # ASSIGN : s_8_4 616 # ASSIGN : s_8_5 689 # ASSIGN : s_8_6 763 # ASSIGN : s_8_7 826 # ASSIGN : s_8_8 843 # ASSIGN : s_8_9 936 # ASSIGN : s_9_0 413 # ASSIGN : s_9_1 464 # ASSIGN : s_9_2 469 # ASSIGN : s_9_3 516 # ASSIGN : s_9_4 576 # ASSIGN : s_9_5 622 # ASSIGN : s_9_6 716 # ASSIGN : s_9_7 770 # ASSIGN : s_9_8 842 # ASSIGN : s_9_9 926 SHOW_RESULT 1020 END : 1020 (0 seconds) [Fri Jun 2 08:34:44 2006] SHOW_RESULT 1020 CPU : 0.379999999999995 = 0.379999999999995 + 0 + 0 + 0 # BOUND : makespan 984 1020 MODIFY_CNF 1002 BEGIN : [Fri Jun 2 08:34:44 2006] MODIFY_CNF 1002 END : 32373752 bytes (0 seconds) [Fri Jun 2 08:34:44 2006] MODIFY_CNF 1002 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1002 BEGIN : [Fri Jun 2 08:34:44 2006] CMD : minisat /work/tamura/csp2sat54962.cnf /work/tamura/csp2sat54962.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 572454 1672739 | 190818 0 0 NaNQ | 0.000 % | | 101 | 572454 1672739 | 209899 101 919 9.1 | 67.265 % | | 251 | 572454 1672739 | 230889 251 2497 9.9 | 67.265 % | | 476 | 572454 1672739 | 253978 476 5112 10.7 | 67.265 % | | 813 | 572454 1672739 | 279376 813 9223 11.3 | 67.265 % | | 1319 | 569991 1665452 | 307314 1175 12781 10.9 | 67.343 % | ==============================================================================) restarts : 6 conflicts : 2062 (285 /sec) decisions : 2911 (402 /sec) propagations : 14278749 (1973853 /sec) inspects : 94141914 (13013903 /sec) conflict literals : 22594 (33.69 % deleted) CPU time : 7.23395 s UNSATISFIABLE VERIFY_CNF 1002 END : (8 seconds) [Fri Jun 2 08:34:52 2006] VERIFY_CNF 1002 CPU : 7.61000000000001 = 0.0100000000000051 + 0.01 + 7.55 + 0.04 # RESULT : makespan 1002 UNSATISFIABLE # BOUND : makespan 1003 1020 MODIFY_CNF 1011 BEGIN : [Fri Jun 2 08:34:52 2006] MODIFY_CNF 1011 END : 32373752 bytes (0 seconds) [Fri Jun 2 08:34:52 2006] MODIFY_CNF 1011 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1011 BEGIN : [Fri Jun 2 08:34:52 2006] CMD : minisat /work/tamura/csp2sat54962.cnf /work/tamura/csp2sat54962.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 584102 1706769 | 194700 0 0 NaNQ | 0.000 % | | 101 | 584102 1706769 | 214170 101 1318 13.0 | 66.598 % | | 253 | 584102 1706769 | 235587 253 3574 14.1 | 66.598 % | | 480 | 584102 1706769 | 259145 480 5909 12.3 | 66.598 % | | 820 | 584102 1706769 | 285060 820 9858 12.0 | 66.598 % | | 1329 | 584102 1706769 | 313566 1329 17945 13.5 | 66.598 % | | 2088 | 583534 1705066 | 344922 1850 24757 13.4 | 66.599 % | ==============================================================================) restarts : 7 conflicts : 2377 (308 /sec) decisions : 3672 (475 /sec) propagations : 15320773 (1982804 /sec) inspects : 109593903 (14183571 /sec) conflict literals : 32220 (28.20 % deleted) CPU time : 7.72682 s SATISFIABLE VERIFY_CNF 1011 END : (8 seconds) [Fri Jun 2 08:35:00 2006] VERIFY_CNF 1011 CPU : 8.17 = 0 + 0.00999999999999998 + 8.11 + 0.05 # RESULT : makespan 1011 SATISFIABLE SHOW_RESULT 1011 BEGIN : [Fri Jun 2 08:35:00 2006] # ASSIGN : makespan 1011 # ASSIGN : s_0_0 60 # ASSIGN : s_0_1 127 # ASSIGN : s_0_2 154 # ASSIGN : s_0_3 189 # ASSIGN : s_0_4 358 # ASSIGN : s_0_5 422 # ASSIGN : s_0_6 551 # ASSIGN : s_0_7 697 # ASSIGN : s_0_8 888 # ASSIGN : s_0_9 999 # ASSIGN : s_1_0 199 # ASSIGN : s_1_1 270 # ASSIGN : s_1_2 313 # ASSIGN : s_1_3 393 # ASSIGN : s_1_4 415 # ASSIGN : s_1_5 572 # ASSIGN : s_1_6 634 # ASSIGN : s_1_7 719 # ASSIGN : s_1_8 786 # ASSIGN : s_1_9 861 # ASSIGN : s_2_0 262 # ASSIGN : s_2_1 314 # ASSIGN : s_2_2 419 # ASSIGN : s_2_3 452 # ASSIGN : s_2_4 556 # ASSIGN : s_2_5 583 # ASSIGN : s_2_6 801 # ASSIGN : s_2_7 826 # ASSIGN : s_2_8 860 # ASSIGN : s_2_9 915 # ASSIGN : s_3_0 5 # ASSIGN : s_3_1 42 # ASSIGN : s_3_2 132 # ASSIGN : s_3_3 187 # ASSIGN : s_3_4 267 # ASSIGN : s_3_5 325 # ASSIGN : s_3_6 336 # ASSIGN : s_3_7 405 # ASSIGN : s_3_8 520 # ASSIGN : s_3_9 986 # ASSIGN : s_4_0 68 # ASSIGN : s_4_1 169 # ASSIGN : s_4_2 270 # ASSIGN : s_4_3 357 # ASSIGN : s_4_4 421 # ASSIGN : s_4_5 498 # ASSIGN : s_4_6 593 # ASSIGN : s_4_7 852 # ASSIGN : s_4_8 932 # ASSIGN : s_4_9 971 # ASSIGN : s_5_0 228 # ASSIGN : s_5_1 325 # ASSIGN : s_5_2 428 # ASSIGN : s_5_3 472 # ASSIGN : s_5_4 539 # ASSIGN : s_5_5 606 # ASSIGN : s_5_6 691 # ASSIGN : s_5_7 794 # ASSIGN : s_5_8 884 # ASSIGN : s_5_9 930 # ASSIGN : s_6_0 165 # ASSIGN : s_6_1 233 # ASSIGN : s_6_2 309 # ASSIGN : s_6_3 360 # ASSIGN : s_6_4 461 # ASSIGN : s_6_5 503 # ASSIGN : s_6_6 588 # ASSIGN : s_6_7 621 # ASSIGN : s_6_8 925 # ASSIGN : s_6_9 967 # ASSIGN : s_7_0 315 # ASSIGN : s_7_1 368 # ASSIGN : s_7_2 373 # ASSIGN : s_7_3 463 # ASSIGN : s_7_4 514 # ASSIGN : s_7_5 572 # ASSIGN : s_7_6 651 # ASSIGN : s_7_7 746 # ASSIGN : s_7_8 841 # ASSIGN : s_7_9 938 # ASSIGN : s_8_0 36 # ASSIGN : s_8_1 137 # ASSIGN : s_8_2 200 # ASSIGN : s_8_3 248 # ASSIGN : s_8_4 404 # ASSIGN : s_8_5 477 # ASSIGN : s_8_6 679 # ASSIGN : s_8_7 742 # ASSIGN : s_8_8 759 # ASSIGN : s_8_9 927 # ASSIGN : s_9_0 359 # ASSIGN : s_9_1 410 # ASSIGN : s_9_2 458 # ASSIGN : s_9_3 551 # ASSIGN : s_9_4 611 # ASSIGN : s_9_5 657 # ASSIGN : s_9_6 715 # ASSIGN : s_9_7 769 # ASSIGN : s_9_8 888 # ASSIGN : s_9_9 917 SHOW_RESULT 1011 END : 1011 (1 seconds) [Fri Jun 2 08:35:01 2006] SHOW_RESULT 1011 CPU : 0.379999999999995 = 0.379999999999995 + 0 + 0 + 0 # BOUND : makespan 1003 1011 MODIFY_CNF 1007 BEGIN : [Fri Jun 2 08:35:01 2006] MODIFY_CNF 1007 END : 32373752 bytes (0 seconds) [Fri Jun 2 08:35:01 2006] MODIFY_CNF 1007 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1007 BEGIN : [Fri Jun 2 08:35:01 2006] CMD : minisat /work/tamura/csp2sat54962.cnf /work/tamura/csp2sat54962.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 579548 1693513 | 193182 0 0 NaNQ | 0.000 % | | 100 | 579548 1693513 | 212500 100 1209 12.1 | 66.894 % | | 250 | 579548 1693513 | 233750 250 2818 11.3 | 66.893 % | | 476 | 579548 1693513 | 257125 476 5694 12.0 | 66.894 % | | 814 | 579548 1693513 | 282837 814 10692 13.1 | 66.894 % | ==============================================================================) restarts : 5 conflicts : 1218 (248 /sec) decisions : 1954 (397 /sec) propagations : 8211627 (1670132 /sec) inspects : 57639791 (11723141 /sec) conflict literals : 17068 (26.85 % deleted) CPU time : 4.91675 s SATISFIABLE VERIFY_CNF 1007 END : (5 seconds) [Fri Jun 2 08:35:06 2006] VERIFY_CNF 1007 CPU : 5.36 = 0 + 0.01 + 5.31 + 0.04 # RESULT : makespan 1007 SATISFIABLE SHOW_RESULT 1007 BEGIN : [Fri Jun 2 08:35:06 2006] # ASSIGN : makespan 1007 # ASSIGN : s_0_0 1 # ASSIGN : s_0_1 24 # ASSIGN : s_0_2 34 # ASSIGN : s_0_3 69 # ASSIGN : s_0_4 113 # ASSIGN : s_0_5 418 # ASSIGN : s_0_6 547 # ASSIGN : s_0_7 693 # ASSIGN : s_0_8 884 # ASSIGN : s_0_9 995 # ASSIGN : s_1_0 195 # ASSIGN : s_1_1 266 # ASSIGN : s_1_2 309 # ASSIGN : s_1_3 389 # ASSIGN : s_1_4 411 # ASSIGN : s_1_5 568 # ASSIGN : s_1_6 630 # ASSIGN : s_1_7 715 # ASSIGN : s_1_8 782 # ASSIGN : s_1_9 857 # ASSIGN : s_2_0 258 # ASSIGN : s_2_1 310 # ASSIGN : s_2_2 415 # ASSIGN : s_2_3 448 # ASSIGN : s_2_4 552 # ASSIGN : s_2_5 579 # ASSIGN : s_2_6 797 # ASSIGN : s_2_7 822 # ASSIGN : s_2_8 856 # ASSIGN : s_2_9 911 # ASSIGN : s_3_0 9 # ASSIGN : s_3_1 43 # ASSIGN : s_3_2 128 # ASSIGN : s_3_3 183 # ASSIGN : s_3_4 263 # ASSIGN : s_3_5 321 # ASSIGN : s_3_6 332 # ASSIGN : s_3_7 401 # ASSIGN : s_3_8 516 # ASSIGN : s_3_9 982 # ASSIGN : s_4_0 64 # ASSIGN : s_4_1 165 # ASSIGN : s_4_2 266 # ASSIGN : s_4_3 353 # ASSIGN : s_4_4 417 # ASSIGN : s_4_5 494 # ASSIGN : s_4_6 589 # ASSIGN : s_4_7 837 # ASSIGN : s_4_8 917 # ASSIGN : s_4_9 967 # ASSIGN : s_5_0 224 # ASSIGN : s_5_1 321 # ASSIGN : s_5_2 424 # ASSIGN : s_5_3 468 # ASSIGN : s_5_4 535 # ASSIGN : s_5_5 602 # ASSIGN : s_5_6 687 # ASSIGN : s_5_7 790 # ASSIGN : s_5_8 880 # ASSIGN : s_5_9 926 # ASSIGN : s_6_0 161 # ASSIGN : s_6_1 229 # ASSIGN : s_6_2 305 # ASSIGN : s_6_3 356 # ASSIGN : s_6_4 457 # ASSIGN : s_6_5 499 # ASSIGN : s_6_6 584 # ASSIGN : s_6_7 617 # ASSIGN : s_6_8 956 # ASSIGN : s_6_9 963 # ASSIGN : s_7_0 311 # ASSIGN : s_7_1 364 # ASSIGN : s_7_2 369 # ASSIGN : s_7_3 459 # ASSIGN : s_7_4 510 # ASSIGN : s_7_5 568 # ASSIGN : s_7_6 647 # ASSIGN : s_7_7 742 # ASSIGN : s_7_8 837 # ASSIGN : s_7_9 934 # ASSIGN : s_8_0 40 # ASSIGN : s_8_1 133 # ASSIGN : s_8_2 196 # ASSIGN : s_8_3 244 # ASSIGN : s_8_4 400 # ASSIGN : s_8_5 473 # ASSIGN : s_8_6 664 # ASSIGN : s_8_7 727 # ASSIGN : s_8_8 744 # ASSIGN : s_8_9 923 # ASSIGN : s_9_0 355 # ASSIGN : s_9_1 406 # ASSIGN : s_9_2 454 # ASSIGN : s_9_3 547 # ASSIGN : s_9_4 607 # ASSIGN : s_9_5 653 # ASSIGN : s_9_6 711 # ASSIGN : s_9_7 765 # ASSIGN : s_9_8 884 # ASSIGN : s_9_9 913 SHOW_RESULT 1007 END : 1007 (1 seconds) [Fri Jun 2 08:35:07 2006] SHOW_RESULT 1007 CPU : 0.379999999999995 = 0.379999999999995 + 0 + 0 + 0 # BOUND : makespan 1003 1007 MODIFY_CNF 1005 BEGIN : [Fri Jun 2 08:35:07 2006] MODIFY_CNF 1005 END : 32373752 bytes (0 seconds) [Fri Jun 2 08:35:07 2006] MODIFY_CNF 1005 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1005 BEGIN : [Fri Jun 2 08:35:07 2006] CMD : minisat /work/tamura/csp2sat54962.cnf /work/tamura/csp2sat54962.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 576975 1685997 | 192325 0 0 NaNQ | 0.000 % | | 100 | 576975 1685997 | 211557 100 999 10.0 | 67.042 % | | 250 | 576975 1685997 | 232713 250 2584 10.3 | 67.042 % | | 475 | 576283 1683922 | 255984 465 5606 12.1 | 67.043 % | | 812 | 576283 1683922 | 281583 802 9162 11.4 | 67.043 % | | 1320 | 576283 1683922 | 309741 1310 15755 12.0 | 67.043 % | | 2079 | 575409 1681346 | 340715 1742 21085 12.1 | 67.078 % | ==============================================================================) restarts : 7 conflicts : 2504 (301 /sec) decisions : 3676 (441 /sec) propagations : 17004110 (2042175 /sec) inspects : 117728536 (14139069 /sec) conflict literals : 31161 (31.91 % deleted) CPU time : 8.32647 s SATISFIABLE VERIFY_CNF 1005 END : (9 seconds) [Fri Jun 2 08:35:16 2006] VERIFY_CNF 1005 CPU : 8.76 = 0 + 0.01 + 8.71 + 0.04 # RESULT : makespan 1005 SATISFIABLE SHOW_RESULT 1005 BEGIN : [Fri Jun 2 08:35:16 2006] # ASSIGN : makespan 1005 # ASSIGN : s_0_0 186 # ASSIGN : s_0_1 212 # ASSIGN : s_0_2 228 # ASSIGN : s_0_3 263 # ASSIGN : s_0_4 352 # ASSIGN : s_0_5 416 # ASSIGN : s_0_6 545 # ASSIGN : s_0_7 691 # ASSIGN : s_0_8 882 # ASSIGN : s_0_9 993 # ASSIGN : s_1_0 194 # ASSIGN : s_1_1 264 # ASSIGN : s_1_2 307 # ASSIGN : s_1_3 387 # ASSIGN : s_1_4 409 # ASSIGN : s_1_5 566 # ASSIGN : s_1_6 628 # ASSIGN : s_1_7 713 # ASSIGN : s_1_8 780 # ASSIGN : s_1_9 855 # ASSIGN : s_2_0 257 # ASSIGN : s_2_1 391 # ASSIGN : s_2_2 413 # ASSIGN : s_2_3 446 # ASSIGN : s_2_4 550 # ASSIGN : s_2_5 577 # ASSIGN : s_2_6 786 # ASSIGN : s_2_7 820 # ASSIGN : s_2_8 854 # ASSIGN : s_2_9 909 # ASSIGN : s_3_0 0 # ASSIGN : s_3_1 33 # ASSIGN : s_3_2 118 # ASSIGN : s_3_3 173 # ASSIGN : s_3_4 253 # ASSIGN : s_3_5 311 # ASSIGN : s_3_6 322 # ASSIGN : s_3_7 399 # ASSIGN : s_3_8 514 # ASSIGN : s_3_9 980 # ASSIGN : s_4_0 55 # ASSIGN : s_4_1 155 # ASSIGN : s_4_2 264 # ASSIGN : s_4_3 351 # ASSIGN : s_4_4 415 # ASSIGN : s_4_5 492 # ASSIGN : s_4_6 587 # ASSIGN : s_4_7 748 # ASSIGN : s_4_8 926 # ASSIGN : s_4_9 965 # ASSIGN : s_5_0 222 # ASSIGN : s_5_1 319 # ASSIGN : s_5_2 422 # ASSIGN : s_5_3 466 # ASSIGN : s_5_4 533 # ASSIGN : s_5_5 600 # ASSIGN : s_5_6 685 # ASSIGN : s_5_7 788 # ASSIGN : s_5_8 878 # ASSIGN : s_5_9 924 # ASSIGN : s_6_0 152 # ASSIGN : s_6_1 187 # ASSIGN : s_6_2 303 # ASSIGN : s_6_3 354 # ASSIGN : s_6_4 455 # ASSIGN : s_6_5 497 # ASSIGN : s_6_6 582 # ASSIGN : s_6_7 615 # ASSIGN : s_6_8 919 # ASSIGN : s_6_9 961 # ASSIGN : s_7_0 309 # ASSIGN : s_7_1 362 # ASSIGN : s_7_2 367 # ASSIGN : s_7_3 457 # ASSIGN : s_7_4 508 # ASSIGN : s_7_5 566 # ASSIGN : s_7_6 645 # ASSIGN : s_7_7 740 # ASSIGN : s_7_8 835 # ASSIGN : s_7_9 932 # ASSIGN : s_8_0 31 # ASSIGN : s_8_1 123 # ASSIGN : s_8_2 186 # ASSIGN : s_8_3 234 # ASSIGN : s_8_4 398 # ASSIGN : s_8_5 471 # ASSIGN : s_8_6 748 # ASSIGN : s_8_7 811 # ASSIGN : s_8_8 828 # ASSIGN : s_8_9 921 # ASSIGN : s_9_0 353 # ASSIGN : s_9_1 404 # ASSIGN : s_9_2 452 # ASSIGN : s_9_3 545 # ASSIGN : s_9_4 605 # ASSIGN : s_9_5 651 # ASSIGN : s_9_6 709 # ASSIGN : s_9_7 763 # ASSIGN : s_9_8 882 # ASSIGN : s_9_9 911 SHOW_RESULT 1005 END : 1005 (0 seconds) [Fri Jun 2 08:35:16 2006] SHOW_RESULT 1005 CPU : 0.38000000000001 = 0.38000000000001 + 0 + 0 + 0 # BOUND : makespan 1003 1005 MODIFY_CNF 1004 BEGIN : [Fri Jun 2 08:35:16 2006] MODIFY_CNF 1004 END : 32373752 bytes (0 seconds) [Fri Jun 2 08:35:16 2006] MODIFY_CNF 1004 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1004 BEGIN : [Fri Jun 2 08:35:16 2006] CMD : minisat /work/tamura/csp2sat54962.cnf /work/tamura/csp2sat54962.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 575065 1680369 | 191688 0 0 NaNQ | 0.000 % | | 100 | 575065 1680369 | 210856 100 1144 11.4 | 67.117 % | | 251 | 575065 1680369 | 231942 251 3276 13.1 | 67.117 % | | 476 | 575065 1680369 | 255136 476 5514 11.6 | 67.117 % | | 813 | 575065 1680369 | 280650 813 9753 12.0 | 67.117 % | | 1319 | 575065 1680369 | 308715 1319 17977 13.6 | 67.117 % | | 2078 | 540513 1578683 | 339586 1558 19689 12.6 | 68.637 % | ==============================================================================) restarts : 7 conflicts : 2179 (290 /sec) decisions : 3057 (406 /sec) propagations : 14976475 (1989975 /sec) inspects : 102563234 (13627925 /sec) conflict literals : 28254 (30.74 % deleted) CPU time : 7.52596 s UNSATISFIABLE VERIFY_CNF 1004 END : (8 seconds) [Fri Jun 2 08:35:24 2006] VERIFY_CNF 1004 CPU : 8.01 = 0 + 0.00999999999999998 + 7.86 + 0.14 # RESULT : makespan 1004 UNSATISFIABLE # BOUND : makespan 1005 1005 MAIN END : (126 seconds) [Fri Jun 2 08:35:24 2006] MAIN CPU : 125.05 = 72.37 + 0.17 + 51.97 + 0.54