MAIN BEGIN : [Thu Jun 1 17:06:45 2006] READ BEGIN : csp/la25.csp [Thu Jun 1 17:06:45 2006] READ END : csp/la25.csp (3 seconds) [Thu Jun 1 17:06:48 2006] READ CPU : 3.07 = 3.07 + 0 + 0 + 0 # BOUND : makespan 864 1383 GENERATE_CNF 1383 BEGIN : [Thu Jun 1 17:06:48 2006] GENERATE_CNF 1383 END : 210521 variables 3200825 clauses 74948742 bytes (157 seconds) [Thu Jun 1 17:09:25 2006] GENERATE_CNF 1383 CPU : 156.78 = 156.56 + 0.22 + 0 + 0 MODIFY_CNF 1123 BEGIN : [Thu Jun 1 17:09:25 2006] MODIFY_CNF 1123 END : 74948748 bytes (0 seconds) [Thu Jun 1 17:09:25 2006] MODIFY_CNF 1123 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1123 BEGIN : [Thu Jun 1 17:09:25 2006] CMD : minisat /work/tamura/csp2sat62104.cnf /work/tamura/csp2sat62104.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1661933 4890949 | 553977 0 0 NaNQ | 0.000 % | ==============================================================================) restarts : 1 conflicts : 31 (8 /sec) decisions : 306 (81 /sec) propagations : 381608 (101467 /sec) inspects : 3789063 (1007486 /sec) conflict literals : 333 (10.72 % deleted) CPU time : 3.76091 s SATISFIABLE VERIFY_CNF 1123 END : (5 seconds) [Thu Jun 1 17:09:30 2006] VERIFY_CNF 1123 CPU : 4.75000000000002 = 0.0100000000000193 + 0.01 + 4.66 + 0.07 # RESULT : makespan 1123 SATISFIABLE SHOW_RESULT 1123 BEGIN : [Thu Jun 1 17:09:30 2006] # ASSIGN : makespan 1123 # ASSIGN : s_0_0 54 # ASSIGN : s_0_1 68 # ASSIGN : s_0_2 240 # ASSIGN : s_0_3 525 # ASSIGN : s_0_4 620 # ASSIGN : s_0_5 696 # ASSIGN : s_0_6 933 # ASSIGN : s_0_7 954 # ASSIGN : s_0_8 1013 # ASSIGN : s_0_9 1057 # ASSIGN : s_1_0 194 # ASSIGN : s_1_1 252 # ASSIGN : s_1_2 397 # ASSIGN : s_1_3 563 # ASSIGN : s_1_4 621 # ASSIGN : s_1_5 708 # ASSIGN : s_1_6 798 # ASSIGN : s_1_7 841 # ASSIGN : s_1_8 944 # ASSIGN : s_1_9 1031 # ASSIGN : s_2_0 48 # ASSIGN : s_2_1 53 # ASSIGN : s_2_2 137 # ASSIGN : s_2_3 180 # ASSIGN : s_2_4 242 # ASSIGN : s_2_5 456 # ASSIGN : s_2_6 576 # ASSIGN : s_2_7 635 # ASSIGN : s_2_8 888 # ASSIGN : s_2_9 1109 # ASSIGN : s_3_0 55 # ASSIGN : s_3_1 139 # ASSIGN : s_3_2 194 # ASSIGN : s_3_3 351 # ASSIGN : s_3_4 403 # ASSIGN : s_3_5 470 # ASSIGN : s_3_6 567 # ASSIGN : s_3_7 840 # ASSIGN : s_3_8 883 # ASSIGN : s_3_9 957 # ASSIGN : s_4_0 72 # ASSIGN : s_4_1 235 # ASSIGN : s_4_2 368 # ASSIGN : s_4_3 455 # ASSIGN : s_4_4 709 # ASSIGN : s_4_5 746 # ASSIGN : s_4_6 793 # ASSIGN : s_4_7 1065 # ASSIGN : s_4_8 1070 # ASSIGN : s_4_9 1108 # ASSIGN : s_5_0 154 # ASSIGN : s_5_1 163 # ASSIGN : s_5_2 257 # ASSIGN : s_5_3 290 # ASSIGN : s_5_4 370 # ASSIGN : s_5_5 443 # ASSIGN : s_5_6 538 # ASSIGN : s_5_7 881 # ASSIGN : s_5_8 1007 # ASSIGN : s_5_9 1067 # ASSIGN : s_6_0 0 # ASSIGN : s_6_1 97 # ASSIGN : s_6_2 161 # ASSIGN : s_6_3 239 # ASSIGN : s_6_4 260 # ASSIGN : s_6_5 354 # ASSIGN : s_6_6 402 # ASSIGN : s_6_7 596 # ASSIGN : s_6_8 612 # ASSIGN : s_6_9 786 # ASSIGN : s_7_0 5 # ASSIGN : s_7_1 91 # ASSIGN : s_7_2 385 # ASSIGN : s_7_3 542 # ASSIGN : s_7_4 790 # ASSIGN : s_7_5 859 # ASSIGN : s_7_6 889 # ASSIGN : s_7_7 921 # ASSIGN : s_7_8 954 # ASSIGN : s_7_9 998 # ASSIGN : s_8_0 11 # ASSIGN : s_8_1 127 # ASSIGN : s_8_2 143 # ASSIGN : s_8_3 228 # ASSIGN : s_8_4 418 # ASSIGN : s_8_5 448 # ASSIGN : s_8_6 606 # ASSIGN : s_8_7 699 # ASSIGN : s_8_8 793 # ASSIGN : s_8_9 854 # ASSIGN : s_9_0 288 # ASSIGN : s_9_1 324 # ASSIGN : s_9_2 355 # ASSIGN : s_9_3 402 # ASSIGN : s_9_4 454 # ASSIGN : s_9_5 486 # ASSIGN : s_9_6 497 # ASSIGN : s_9_7 532 # ASSIGN : s_9_8 617 # ASSIGN : s_9_9 637 # ASSIGN : s_10_0 107 # ASSIGN : s_10_1 127 # ASSIGN : s_10_2 176 # ASSIGN : s_10_3 250 # ASSIGN : s_10_4 317 # ASSIGN : s_10_5 334 # ASSIGN : s_10_6 369 # ASSIGN : s_10_7 563 # ASSIGN : s_10_8 640 # ASSIGN : s_10_9 983 # ASSIGN : s_11_0 147 # ASSIGN : s_11_1 232 # ASSIGN : s_11_2 253 # ASSIGN : s_11_3 343 # ASSIGN : s_11_4 462 # ASSIGN : s_11_5 603 # ASSIGN : s_11_6 652 # ASSIGN : s_11_7 681 # ASSIGN : s_11_8 698 # ASSIGN : s_11_9 797 # ASSIGN : s_12_0 482 # ASSIGN : s_12_1 500 # ASSIGN : s_12_2 587 # ASSIGN : s_12_3 598 # ASSIGN : s_12_4 670 # ASSIGN : s_12_5 716 # ASSIGN : s_12_6 759 # ASSIGN : s_12_7 778 # ASSIGN : s_12_8 810 # ASSIGN : s_12_9 957 # ASSIGN : s_13_0 273 # ASSIGN : s_13_1 305 # ASSIGN : s_13_2 453 # ASSIGN : s_13_3 524 # ASSIGN : s_13_4 686 # ASSIGN : s_13_5 769 # ASSIGN : s_13_6 826 # ASSIGN : s_13_7 925 # ASSIGN : s_13_8 1016 # ASSIGN : s_13_9 1115 # ASSIGN : s_14_0 154 # ASSIGN : s_14_1 463 # ASSIGN : s_14_2 497 # ASSIGN : s_14_3 560 # ASSIGN : s_14_4 687 # ASSIGN : s_14_5 855 # ASSIGN : s_14_6 924 # ASSIGN : s_14_7 945 # ASSIGN : s_14_8 1021 # ASSIGN : s_14_9 1060 SHOW_RESULT 1123 END : 1123 (1 seconds) [Thu Jun 1 17:09:31 2006] SHOW_RESULT 1123 CPU : 0.590000000000003 = 0.590000000000003 + 0 + 0 + 0 # BOUND : makespan 864 1123 MODIFY_CNF 993 BEGIN : [Thu Jun 1 17:09:31 2006] MODIFY_CNF 993 END : 74948748 bytes (0 seconds) [Thu Jun 1 17:09:31 2006] MODIFY_CNF 993 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 993 BEGIN : [Thu Jun 1 17:09:31 2006] CMD : minisat /work/tamura/csp2sat62104.cnf /work/tamura/csp2sat62104.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1326409 3904092 | 442136 0 0 NaNQ | 0.000 % | | 101 | 1326409 3904092 | 486349 101 1547 15.3 | 63.926 % | | 251 | 1326409 3904092 | 534984 251 2905 11.6 | 63.926 % | | 477 | 1326409 3904092 | 588483 477 6079 12.7 | 63.926 % | | 815 | 1326409 3904092 | 647331 815 9914 12.2 | 63.926 % | | 1321 | 1326409 3904092 | 712064 1321 15468 11.7 | 63.926 % | | 2082 | 1326409 3904092 | 783270 2082 25811 12.4 | 63.926 % | | 3222 | 1326409 3904092 | 861597 3222 43425 13.5 | 63.926 % | | 4930 | 1326409 3904092 | 947757 4930 63156 12.8 | 63.926 % | | 7492 | 1326409 3904092 | 1042533 7492 102556 13.7 | 63.926 % | | 11336 | 1326409 3904092 | 1146786 11336 171971 15.2 | 63.926 % | | 17102 | 1326409 3904092 | 1261465 17102 293442 17.2 | 63.926 % | ==============================================================================) restarts : 12 conflicts : 22300 (231 /sec) decisions : 31237 (324 /sec) propagations : 174423499 (1807529 /sec) inspects : 1679173427 (17401068 /sec) conflict literals : 421763 (36.07 % deleted) CPU time : 96.4983 s SATISFIABLE VERIFY_CNF 993 END : (97 seconds) [Thu Jun 1 17:11:08 2006] VERIFY_CNF 993 CPU : 97.6 = 0 + 0.01 + 97.31 + 0.28 # RESULT : makespan 993 SATISFIABLE SHOW_RESULT 993 BEGIN : [Thu Jun 1 17:11:08 2006] # ASSIGN : makespan 993 # ASSIGN : s_0_0 6 # ASSIGN : s_0_1 30 # ASSIGN : s_0_2 105 # ASSIGN : s_0_3 138 # ASSIGN : s_0_4 176 # ASSIGN : s_0_5 280 # ASSIGN : s_0_6 380 # ASSIGN : s_0_7 397 # ASSIGN : s_0_8 426 # ASSIGN : s_0_9 636 # ASSIGN : s_1_0 99 # ASSIGN : s_1_1 160 # ASSIGN : s_1_2 242 # ASSIGN : s_1_3 346 # ASSIGN : s_1_4 404 # ASSIGN : s_1_5 491 # ASSIGN : s_1_6 580 # ASSIGN : s_1_7 636 # ASSIGN : s_1_8 832 # ASSIGN : s_1_9 901 # ASSIGN : s_2_0 40 # ASSIGN : s_2_1 45 # ASSIGN : s_2_2 133 # ASSIGN : s_2_3 189 # ASSIGN : s_2_4 291 # ASSIGN : s_2_5 307 # ASSIGN : s_2_6 316 # ASSIGN : s_2_7 377 # ASSIGN : s_2_8 569 # ASSIGN : s_2_9 901 # ASSIGN : s_3_0 200 # ASSIGN : s_3_1 244 # ASSIGN : s_3_2 313 # ASSIGN : s_3_3 438 # ASSIGN : s_3_4 457 # ASSIGN : s_3_5 536 # ASSIGN : s_3_6 650 # ASSIGN : s_3_7 737 # ASSIGN : s_3_8 780 # ASSIGN : s_3_9 952 # ASSIGN : s_4_0 89 # ASSIGN : s_4_1 476 # ASSIGN : s_4_2 560 # ASSIGN : s_4_3 635 # ASSIGN : s_4_4 686 # ASSIGN : s_4_5 723 # ASSIGN : s_4_6 765 # ASSIGN : s_4_7 924 # ASSIGN : s_4_8 940 # ASSIGN : s_4_9 978 # ASSIGN : s_5_0 312 # ASSIGN : s_5_1 398 # ASSIGN : s_5_2 470 # ASSIGN : s_5_3 501 # ASSIGN : s_5_4 583 # ASSIGN : s_5_5 656 # ASSIGN : s_5_6 770 # ASSIGN : s_5_7 810 # ASSIGN : s_5_8 853 # ASSIGN : s_5_9 937 # ASSIGN : s_6_0 36 # ASSIGN : s_6_1 327 # ASSIGN : s_6_2 391 # ASSIGN : s_6_3 490 # ASSIGN : s_6_4 516 # ASSIGN : s_6_5 619 # ASSIGN : s_6_6 677 # ASSIGN : s_6_7 730 # ASSIGN : s_6_8 746 # ASSIGN : s_6_9 846 # ASSIGN : s_7_0 8 # ASSIGN : s_7_1 94 # ASSIGN : s_7_2 189 # ASSIGN : s_7_3 252 # ASSIGN : s_7_4 643 # ASSIGN : s_7_5 740 # ASSIGN : s_7_6 781 # ASSIGN : s_7_7 813 # ASSIGN : s_7_8 849 # ASSIGN : s_7_9 893 # ASSIGN : s_8_0 1 # ASSIGN : s_8_1 117 # ASSIGN : s_8_2 133 # ASSIGN : s_8_3 144 # ASSIGN : s_8_4 214 # ASSIGN : s_8_5 264 # ASSIGN : s_8_6 348 # ASSIGN : s_8_7 441 # ASSIGN : s_8_8 522 # ASSIGN : s_8_9 633 # ASSIGN : s_9_0 58 # ASSIGN : s_9_1 268 # ASSIGN : s_9_2 299 # ASSIGN : s_9_3 352 # ASSIGN : s_9_4 409 # ASSIGN : s_9_5 511 # ASSIGN : s_9_6 546 # ASSIGN : s_9_7 584 # ASSIGN : s_9_8 636 # ASSIGN : s_9_9 716 # ASSIGN : s_10_0 20 # ASSIGN : s_10_1 40 # ASSIGN : s_10_2 179 # ASSIGN : s_10_3 253 # ASSIGN : s_10_4 263 # ASSIGN : s_10_5 357 # ASSIGN : s_10_6 623 # ASSIGN : s_10_7 708 # ASSIGN : s_10_8 785 # ASSIGN : s_10_9 853 # ASSIGN : s_11_0 129 # ASSIGN : s_11_1 473 # ASSIGN : s_11_2 480 # ASSIGN : s_11_3 551 # ASSIGN : s_11_4 610 # ASSIGN : s_11_5 734 # ASSIGN : s_11_6 751 # ASSIGN : s_11_7 915 # ASSIGN : s_11_8 932 # ASSIGN : s_11_9 980 # ASSIGN : s_12_0 185 # ASSIGN : s_12_1 237 # ASSIGN : s_12_2 324 # ASSIGN : s_12_3 358 # ASSIGN : s_12_4 418 # ASSIGN : s_12_5 792 # ASSIGN : s_12_6 835 # ASSIGN : s_12_7 854 # ASSIGN : s_12_8 913 # ASSIGN : s_12_9 929 # ASSIGN : s_13_0 8 # ASSIGN : s_13_1 45 # ASSIGN : s_13_2 137 # ASSIGN : s_13_3 170 # ASSIGN : s_13_4 252 # ASSIGN : s_13_5 335 # ASSIGN : s_13_6 392 # ASSIGN : s_13_7 795 # ASSIGN : s_13_8 886 # ASSIGN : s_13_9 985 # ASSIGN : s_14_0 165 # ASSIGN : s_14_1 314 # ASSIGN : s_14_2 321 # ASSIGN : s_14_3 431 # ASSIGN : s_14_4 469 # ASSIGN : s_14_5 574 # ASSIGN : s_14_6 702 # ASSIGN : s_14_7 723 # ASSIGN : s_14_8 885 # ASSIGN : s_14_9 930 SHOW_RESULT 993 END : 993 (1 seconds) [Thu Jun 1 17:11:09 2006] SHOW_RESULT 993 CPU : 0.609999999999994 = 0.599999999999994 + 0.01 + 0 + 0 # BOUND : makespan 864 993 MODIFY_CNF 928 BEGIN : [Thu Jun 1 17:11:09 2006] MODIFY_CNF 928 END : 74948747 bytes (0 seconds) [Thu Jun 1 17:11:09 2006] MODIFY_CNF 928 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 928 BEGIN : [Thu Jun 1 17:11:09 2006] CMD : minisat /work/tamura/csp2sat62104.cnf /work/tamura/csp2sat62104.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1144885 3369416 | 381628 0 0 NaNQ | 0.000 % | | 100 | 1144885 3369416 | 419790 100 874 8.7 | 68.642 % | | 250 | 1144885 3369416 | 461769 249 2213 8.9 | 68.798 % | | 475 | 1144885 3369416 | 507946 471 3828 8.1 | 69.053 % | | 814 | 1144885 3369416 | 558741 810 7790 9.6 | 69.053 % | ==============================================================================) restarts : 5 conflicts : 901 (126 /sec) decisions : 1341 (187 /sec) propagations : 6700046 (935316 /sec) inspects : 51346960 (7167958 /sec) conflict literals : 8283 (33.19 % deleted) CPU time : 7.1634 s UNSATISFIABLE VERIFY_CNF 928 END : (8 seconds) [Thu Jun 1 17:11:17 2006] VERIFY_CNF 928 CPU : 8.12 = 0 + 0.01 + 7.84 + 0.27 # RESULT : makespan 928 UNSATISFIABLE # BOUND : makespan 929 993 MODIFY_CNF 961 BEGIN : [Thu Jun 1 17:11:17 2006] MODIFY_CNF 961 END : 74948747 bytes (0 seconds) [Thu Jun 1 17:11:17 2006] MODIFY_CNF 961 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 961 BEGIN : [Thu Jun 1 17:11:17 2006] CMD : minisat /work/tamura/csp2sat62104.cnf /work/tamura/csp2sat62104.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1234992 3634714 | 411664 0 0 NaNQ | 0.000 % | | 101 | 1234992 3634714 | 452830 101 1080 10.7 | 66.249 % | | 251 | 1234992 3634714 | 498113 251 2563 10.2 | 66.249 % | | 476 | 1234992 3634714 | 547924 476 5290 11.1 | 66.249 % | | 813 | 1234992 3634714 | 602717 813 8948 11.0 | 66.249 % | | 1320 | 1234992 3634714 | 662988 1320 16552 12.5 | 66.249 % | | 2079 | 1234992 3634714 | 729287 2079 26817 12.9 | 66.249 % | | 3218 | 1234992 3634714 | 802216 3218 39666 12.3 | 66.249 % | | 4926 | 1234992 3634714 | 882438 4926 66335 13.5 | 66.249 % | | 7488 | 1227018 3611116 | 970682 6225 84207 13.5 | 66.406 % | ==============================================================================) restarts : 10 conflicts : 11013 (247 /sec) decisions : 15428 (346 /sec) propagations : 83388014 (1869628 /sec) inspects : 729232259 (16349988 /sec) conflict literals : 173306 (35.42 % deleted) CPU time : 44.6014 s UNSATISFIABLE VERIFY_CNF 961 END : (46 seconds) [Thu Jun 1 17:12:03 2006] VERIFY_CNF 961 CPU : 45.37 = 0 + 0.00999999999999995 + 45.28 + 0.08 # RESULT : makespan 961 UNSATISFIABLE # BOUND : makespan 962 993 MODIFY_CNF 977 BEGIN : [Thu Jun 1 17:12:03 2006] MODIFY_CNF 977 END : 74948748 bytes (0 seconds) [Thu Jun 1 17:12:03 2006] MODIFY_CNF 977 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 977 BEGIN : [Thu Jun 1 17:12:03 2006] CMD : minisat /work/tamura/csp2sat62104.cnf /work/tamura/csp2sat62104.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1280517 3768854 | 426839 0 0 NaNQ | 0.000 % | | 100 | 1280517 3768854 | 469522 100 1478 14.8 | 65.088 % | | 250 | 1280517 3768854 | 516475 250 2726 10.9 | 65.088 % | | 475 | 1280517 3768854 | 568122 474 5446 11.5 | 65.089 % | | 812 | 1280517 3768854 | 624934 811 9677 11.9 | 65.089 % | | 1319 | 1279883 3766953 | 687428 1305 15435 11.8 | 65.089 % | | 2078 | 1279883 3766953 | 756171 2064 24265 11.8 | 65.089 % | | 3217 | 1279883 3766953 | 831788 3203 39286 12.3 | 65.089 % | | 4925 | 1279883 3766953 | 914967 4911 61357 12.5 | 65.089 % | | 7488 | 1279883 3766953 | 1006464 7474 101059 13.5 | 65.089 % | | 11332 | 1279223 3765021 | 1107110 11315 164879 14.6 | 65.112 % | | 17099 | 1279223 3765021 | 1217821 17082 307702 18.0 | 65.112 % | ==============================================================================) restarts : 12 conflicts : 21394 (244 /sec) decisions : 29777 (339 /sec) propagations : 163037430 (1857731 /sec) inspects : 1538910690 (17535123 /sec) conflict literals : 404665 (33.92 % deleted) CPU time : 87.7616 s SATISFIABLE VERIFY_CNF 977 END : (89 seconds) [Thu Jun 1 17:13:32 2006] VERIFY_CNF 977 CPU : 88.7 = 0 + 0.01 + 88.61 + 0.0800000000000001 # RESULT : makespan 977 SATISFIABLE SHOW_RESULT 977 BEGIN : [Thu Jun 1 17:13:32 2006] # ASSIGN : makespan 977 # ASSIGN : s_0_0 0 # ASSIGN : s_0_1 14 # ASSIGN : s_0_2 89 # ASSIGN : s_0_3 101 # ASSIGN : s_0_4 251 # ASSIGN : s_0_5 352 # ASSIGN : s_0_6 449 # ASSIGN : s_0_7 533 # ASSIGN : s_0_8 585 # ASSIGN : s_0_9 696 # ASSIGN : s_1_0 70 # ASSIGN : s_1_1 108 # ASSIGN : s_1_2 231 # ASSIGN : s_1_3 316 # ASSIGN : s_1_4 374 # ASSIGN : s_1_5 461 # ASSIGN : s_1_6 569 # ASSIGN : s_1_7 620 # ASSIGN : s_1_8 732 # ASSIGN : s_1_9 885 # ASSIGN : s_2_0 119 # ASSIGN : s_2_1 124 # ASSIGN : s_2_2 208 # ASSIGN : s_2_3 267 # ASSIGN : s_2_4 376 # ASSIGN : s_2_5 578 # ASSIGN : s_2_6 603 # ASSIGN : s_2_7 655 # ASSIGN : s_2_8 775 # ASSIGN : s_2_9 963 # ASSIGN : s_3_0 0 # ASSIGN : s_3_1 97 # ASSIGN : s_3_2 105 # ASSIGN : s_3_3 201 # ASSIGN : s_3_4 220 # ASSIGN : s_3_5 279 # ASSIGN : s_3_6 376 # ASSIGN : s_3_7 462 # ASSIGN : s_3_8 771 # ASSIGN : s_3_9 877 # ASSIGN : s_4_0 101 # ASSIGN : s_4_1 452 # ASSIGN : s_4_2 523 # ASSIGN : s_4_3 598 # ASSIGN : s_4_4 640 # ASSIGN : s_4_5 677 # ASSIGN : s_4_6 700 # ASSIGN : s_4_7 908 # ASSIGN : s_4_8 924 # ASSIGN : s_4_9 962 # ASSIGN : s_5_0 319 # ASSIGN : s_5_1 380 # ASSIGN : s_5_2 459 # ASSIGN : s_5_3 490 # ASSIGN : s_5_4 571 # ASSIGN : s_5_5 644 # ASSIGN : s_5_6 754 # ASSIGN : s_5_7 818 # ASSIGN : s_5_8 861 # ASSIGN : s_5_9 921 # ASSIGN : s_6_0 8 # ASSIGN : s_6_1 316 # ASSIGN : s_6_2 408 # ASSIGN : s_6_3 486 # ASSIGN : s_6_4 507 # ASSIGN : s_6_5 649 # ASSIGN : s_6_6 709 # ASSIGN : s_6_7 762 # ASSIGN : s_6_8 801 # ASSIGN : s_6_9 914 # ASSIGN : s_7_0 3 # ASSIGN : s_7_1 105 # ASSIGN : s_7_2 229 # ASSIGN : s_7_3 327 # ASSIGN : s_7_4 616 # ASSIGN : s_7_5 686 # ASSIGN : s_7_6 716 # ASSIGN : s_7_7 748 # ASSIGN : s_7_8 841 # ASSIGN : s_7_9 918 # ASSIGN : s_8_0 57 # ASSIGN : s_8_1 190 # ASSIGN : s_8_2 206 # ASSIGN : s_8_3 217 # ASSIGN : s_8_4 262 # ASSIGN : s_8_5 292 # ASSIGN : s_8_6 505 # ASSIGN : s_8_7 748 # ASSIGN : s_8_8 808 # ASSIGN : s_8_9 887 # ASSIGN : s_9_0 69 # ASSIGN : s_9_1 429 # ASSIGN : s_9_2 460 # ASSIGN : s_9_3 560 # ASSIGN : s_9_4 612 # ASSIGN : s_9_5 644 # ASSIGN : s_9_6 681 # ASSIGN : s_9_7 748 # ASSIGN : s_9_8 845 # ASSIGN : s_9_9 865 # ASSIGN : s_10_0 136 # ASSIGN : s_10_1 156 # ASSIGN : s_10_2 205 # ASSIGN : s_10_3 306 # ASSIGN : s_10_4 335 # ASSIGN : s_10_5 354 # ASSIGN : s_10_6 388 # ASSIGN : s_10_7 522 # ASSIGN : s_10_8 680 # ASSIGN : s_10_9 781 # ASSIGN : s_11_0 12 # ASSIGN : s_11_1 237 # ASSIGN : s_11_2 244 # ASSIGN : s_11_3 315 # ASSIGN : s_11_4 384 # ASSIGN : s_11_5 473 # ASSIGN : s_11_6 494 # ASSIGN : s_11_7 599 # ASSIGN : s_11_8 629 # ASSIGN : s_11_9 964 # ASSIGN : s_12_0 42 # ASSIGN : s_12_1 464 # ASSIGN : s_12_2 551 # ASSIGN : s_12_3 562 # ASSIGN : s_12_4 601 # ASSIGN : s_12_5 666 # ASSIGN : s_12_6 720 # ASSIGN : s_12_7 739 # ASSIGN : s_12_8 783 # ASSIGN : s_12_9 913 # ASSIGN : s_13_0 69 # ASSIGN : s_13_1 139 # ASSIGN : s_13_2 295 # ASSIGN : s_13_3 328 # ASSIGN : s_13_4 410 # ASSIGN : s_13_5 493 # ASSIGN : s_13_6 550 # ASSIGN : s_13_7 779 # ASSIGN : s_13_8 870 # ASSIGN : s_13_9 969 # ASSIGN : s_14_0 102 # ASSIGN : s_14_1 190 # ASSIGN : s_14_2 197 # ASSIGN : s_14_3 224 # ASSIGN : s_14_4 263 # ASSIGN : s_14_5 709 # ASSIGN : s_14_6 778 # ASSIGN : s_14_7 799 # ASSIGN : s_14_8 869 # ASSIGN : s_14_9 914 SHOW_RESULT 977 END : 977 (0 seconds) [Thu Jun 1 17:13:32 2006] SHOW_RESULT 977 CPU : 0.629999999999995 = 0.629999999999995 + 0 + 0 + 0 # BOUND : makespan 962 977 MODIFY_CNF 969 BEGIN : [Thu Jun 1 17:13:32 2006] MODIFY_CNF 969 END : 74948748 bytes (0 seconds) [Thu Jun 1 17:13:32 2006] MODIFY_CNF 969 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 969 BEGIN : [Thu Jun 1 17:13:32 2006] CMD : minisat /work/tamura/csp2sat62104.cnf /work/tamura/csp2sat62104.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1260157 3708987 | 420052 0 0 NaNQ | 0.000 % | | 100 | 1260157 3708987 | 462057 100 1330 13.3 | 65.666 % | | 250 | 1260157 3708987 | 508262 250 2714 10.9 | 65.666 % | | 475 | 1260157 3708987 | 559089 475 5858 12.3 | 65.666 % | | 812 | 1260157 3708987 | 614998 812 10265 12.6 | 65.666 % | | 1318 | 1260157 3708987 | 676497 1318 17711 13.4 | 65.666 % | | 2077 | 1260157 3708987 | 744147 2077 25620 12.3 | 65.666 % | | 3216 | 1260157 3708987 | 818562 3216 38177 11.9 | 65.666 % | | 4924 | 1260157 3708987 | 900418 4924 63997 13.0 | 65.666 % | | 7486 | 1260157 3708987 | 990460 7486 114609 15.3 | 65.666 % | | 11330 | 1260157 3708987 | 1089506 11330 175620 15.5 | 65.666 % | | 17096 | 1259477 3706948 | 1198457 16398 286118 17.4 | 65.667 % | ==============================================================================) restarts : 12 conflicts : 22420 (242 /sec) decisions : 30824 (333 /sec) propagations : 175110686 (1891973 /sec) inspects : 1572153824 (16986242 /sec) conflict literals : 394073 (38.56 % deleted) CPU time : 92.5545 s UNSATISFIABLE VERIFY_CNF 969 END : (94 seconds) [Thu Jun 1 17:15:06 2006] VERIFY_CNF 969 CPU : 93.3 = 0 + 0.02 + 93.2 + 0.08 # RESULT : makespan 969 UNSATISFIABLE # BOUND : makespan 970 977 MODIFY_CNF 973 BEGIN : [Thu Jun 1 17:15:06 2006] MODIFY_CNF 973 END : 74948748 bytes (0 seconds) [Thu Jun 1 17:15:06 2006] MODIFY_CNF 973 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 973 BEGIN : [Thu Jun 1 17:15:06 2006] CMD : minisat /work/tamura/csp2sat62104.cnf /work/tamura/csp2sat62104.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1270379 3739046 | 423459 0 0 NaNQ | 0.000 % | | 100 | 1270379 3739046 | 465804 100 1359 13.6 | 65.377 % | | 253 | 1270379 3739046 | 512385 253 3007 11.9 | 65.377 % | | 479 | 1270379 3739046 | 563623 479 5391 11.3 | 65.377 % | | 817 | 1270379 3739046 | 619986 817 9681 11.8 | 65.377 % | | 1325 | 1270379 3739046 | 681984 1325 16328 12.3 | 65.377 % | | 2084 | 1270379 3739046 | 750183 2084 29593 14.2 | 65.377 % | | 3223 | 1270379 3739046 | 825201 3223 45263 14.0 | 65.377 % | | 4931 | 1270379 3739046 | 907721 4931 72972 14.8 | 65.377 % | | 7493 | 1270379 3739046 | 998494 7493 109540 14.6 | 65.377 % | | 11337 | 1243370 3659014 | 1098343 9225 137043 14.9 | 65.855 % | | 17103 | 1243370 3659014 | 1208177 14991 277865 18.5 | 65.855 % | | 25752 | 1193341 3510727 | 1328995 15932 286278 18.0 | 66.719 % | ==============================================================================) restarts : 13 conflicts : 30296 (249 /sec) decisions : 41352 (340 /sec) propagations : 228593494 (1878205 /sec) inspects : 2092143238 (17189784 /sec) conflict literals : 557995 (38.93 % deleted) CPU time : 121.709 s UNSATISFIABLE VERIFY_CNF 973 END : (123 seconds) [Thu Jun 1 17:17:09 2006] VERIFY_CNF 973 CPU : 122.48 = 0 + 0.01 + 122.39 + 0.08 # RESULT : makespan 973 UNSATISFIABLE # BOUND : makespan 974 977 MODIFY_CNF 975 BEGIN : [Thu Jun 1 17:17:09 2006] MODIFY_CNF 975 END : 74948748 bytes (0 seconds) [Thu Jun 1 17:17:09 2006] MODIFY_CNF 975 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 975 BEGIN : [Thu Jun 1 17:17:09 2006] CMD : minisat /work/tamura/csp2sat62104.cnf /work/tamura/csp2sat62104.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1275368 3753710 | 425122 0 0 NaNQ | 0.000 % | | 100 | 1275368 3753710 | 467634 100 1179 11.8 | 65.232 % | | 250 | 1275368 3753710 | 514397 250 2924 11.7 | 65.232 % | | 475 | 1275368 3753710 | 565837 474 5766 12.2 | 65.233 % | | 812 | 1275368 3753710 | 622421 810 10382 12.8 | 65.234 % | | 1318 | 1274032 3749704 | 684663 1293 16421 12.7 | 65.234 % | | 2078 | 1274032 3749704 | 753129 2053 25130 12.2 | 65.234 % | | 3219 | 1274032 3749704 | 828442 3194 38999 12.2 | 65.234 % | | 4929 | 1274032 3749704 | 911286 4904 74805 15.3 | 65.234 % | | 7492 | 1274032 3749704 | 1002415 7467 132877 17.8 | 65.234 % | | 11336 | 1272486 3745115 | 1102656 11309 211909 18.7 | 65.258 % | | 17102 | 1272486 3745115 | 1212922 17075 345423 20.2 | 65.258 % | | 25751 | 1268496 3733378 | 1334214 24771 534184 21.6 | 65.369 % | ==============================================================================) restarts : 13 conflicts : 35641 (246 /sec) decisions : 48849 (337 /sec) propagations : 263014522 (1815191 /sec) inspects : 2524993653 (17426210 /sec) conflict literals : 783074 (37.93 % deleted) CPU time : 144.896 s UNSATISFIABLE VERIFY_CNF 975 END : (146 seconds) [Thu Jun 1 17:19:35 2006] VERIFY_CNF 975 CPU : 145.71 = 0 + 0.01 + 145.63 + 0.0700000000000001 # RESULT : makespan 975 UNSATISFIABLE # BOUND : makespan 976 977 MODIFY_CNF 976 BEGIN : [Thu Jun 1 17:19:35 2006] MODIFY_CNF 976 END : 74948748 bytes (0 seconds) [Thu Jun 1 17:19:35 2006] MODIFY_CNF 976 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 976 BEGIN : [Thu Jun 1 17:19:35 2006] CMD : minisat /work/tamura/csp2sat62104.cnf /work/tamura/csp2sat62104.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1277505 3759970 | 425835 0 0 NaNQ | 0.000 % | | 101 | 1277505 3759970 | 468418 101 1666 16.5 | 65.161 % | | 251 | 1277505 3759970 | 515260 251 3146 12.5 | 65.161 % | | 476 | 1277505 3759970 | 566786 476 6669 14.0 | 65.161 % | | 813 | 1277505 3759970 | 623465 813 10532 13.0 | 65.161 % | | 1319 | 1277505 3759970 | 685811 1319 17983 13.6 | 65.161 % | | 2078 | 1277505 3759970 | 754392 2078 29128 14.0 | 65.161 % | | 3217 | 1277505 3759970 | 829831 3217 46308 14.4 | 65.161 % | | 4925 | 1277505 3759970 | 912815 4925 80372 16.3 | 65.161 % | | 7487 | 1277505 3759970 | 1004096 7487 121394 16.2 | 65.161 % | | 11332 | 1277505 3759970 | 1104506 11332 181087 16.0 | 65.161 % | | 17098 | 1277505 3759970 | 1214956 17098 298065 17.4 | 65.161 % | | 25747 | 1277505 3759970 | 1336452 25747 474344 18.4 | 65.161 % | ==============================================================================) restarts : 13 conflicts : 38501 (246 /sec) decisions : 53025 (338 /sec) propagations : 286595839 (1829401 /sec) inspects : 2756311010 (17594104 /sec) conflict literals : 803498 (37.74 % deleted) CPU time : 156.661 s UNSATISFIABLE VERIFY_CNF 976 END : (158 seconds) [Thu Jun 1 17:22:13 2006] VERIFY_CNF 976 CPU : 157.5 = 0.0100000000000193 + 0.00999999999999995 + 157.4 + 0.0800000000000001 # RESULT : makespan 976 UNSATISFIABLE # BOUND : makespan 977 977 MAIN END : (928 seconds) [Thu Jun 1 17:22:13 2006] MAIN CPU : 925.23 = 161.49 + 0.33 + 762.32 + 1.09