MAIN BEGIN : [Thu Jun 1 16:48:31 2006] READ BEGIN : csp/la23.csp [Thu Jun 1 16:48:31 2006] READ END : csp/la23.csp (3 seconds) [Thu Jun 1 16:48:34 2006] READ CPU : 3.09 = 3.09 + 0 + 0 + 0 # BOUND : makespan 1032 1314 GENERATE_CNF 1314 BEGIN : [Thu Jun 1 16:48:34 2006] GENERATE_CNF 1314 END : 199934 variables 3023902 clauses 70616470 bytes (148 seconds) [Thu Jun 1 16:51:02 2006] GENERATE_CNF 1314 CPU : 147.52 = 147.31 + 0.21 + 0 + 0 MODIFY_CNF 1173 BEGIN : [Thu Jun 1 16:51:02 2006] MODIFY_CNF 1173 END : 70616476 bytes (0 seconds) [Thu Jun 1 16:51:02 2006] MODIFY_CNF 1173 CPU : 0.00999999999999091 = 0.00999999999999091 + 0 + 0 + 0 VERIFY_CNF 1173 BEGIN : [Thu Jun 1 16:51:02 2006] CMD : minisat /work/tamura/csp2sat33598.cnf /work/tamura/csp2sat33598.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1697182 4995026 | 565727 0 0 NaNQ | 0.000 % | | 100 | 1697182 4995026 | 622299 100 1457 14.6 | 51.314 % | | 250 | 1697182 4995026 | 684529 250 4197 16.8 | 51.314 % | ==============================================================================) restarts : 3 conflicts : 349 (71 /sec) decisions : 876 (179 /sec) propagations : 2643410 (540070 /sec) inspects : 30449217 (6221021 /sec) conflict literals : 6653 (17.43 % deleted) CPU time : 4.89457 s SATISFIABLE VERIFY_CNF 1173 END : (6 seconds) [Thu Jun 1 16:51:08 2006] VERIFY_CNF 1173 CPU : 5.99 = 0 + 0.01 + 5.92 + 0.06 # RESULT : makespan 1173 SATISFIABLE SHOW_RESULT 1173 BEGIN : [Thu Jun 1 16:51:08 2006] # ASSIGN : makespan 1173 # ASSIGN : s_0_0 8 # ASSIGN : s_0_1 92 # ASSIGN : s_0_2 150 # ASSIGN : s_0_3 245 # ASSIGN : s_0_4 289 # ASSIGN : s_0_5 387 # ASSIGN : s_0_6 516 # ASSIGN : s_0_7 521 # ASSIGN : s_0_8 661 # ASSIGN : s_0_9 868 # ASSIGN : s_1_0 19 # ASSIGN : s_1_1 178 # ASSIGN : s_1_2 437 # ASSIGN : s_1_3 452 # ASSIGN : s_1_4 491 # ASSIGN : s_1_5 572 # ASSIGN : s_1_6 767 # ASSIGN : s_1_7 802 # ASSIGN : s_1_8 859 # ASSIGN : s_1_9 932 # ASSIGN : s_2_0 167 # ASSIGN : s_2_1 290 # ASSIGN : s_2_2 361 # ASSIGN : s_2_3 462 # ASSIGN : s_2_4 829 # ASSIGN : s_2_5 909 # ASSIGN : s_2_6 931 # ASSIGN : s_2_7 941 # ASSIGN : s_2_8 1021 # ASSIGN : s_2_9 1124 # ASSIGN : s_3_0 152 # ASSIGN : s_3_1 227 # ASSIGN : s_3_2 244 # ASSIGN : s_3_3 251 # ASSIGN : s_3_4 386 # ASSIGN : s_3_5 397 # ASSIGN : s_3_6 459 # ASSIGN : s_3_7 544 # ASSIGN : s_3_8 579 # ASSIGN : s_3_9 877 # ASSIGN : s_4_0 8 # ASSIGN : s_4_1 28 # ASSIGN : s_4_2 40 # ASSIGN : s_4_3 224 # ASSIGN : s_4_4 292 # ASSIGN : s_4_5 356 # ASSIGN : s_4_6 506 # ASSIGN : s_4_7 554 # ASSIGN : s_4_8 754 # ASSIGN : s_4_9 1034 # ASSIGN : s_5_0 111 # ASSIGN : s_5_1 643 # ASSIGN : s_5_2 741 # ASSIGN : s_5_3 798 # ASSIGN : s_5_4 868 # ASSIGN : s_5_5 945 # ASSIGN : s_5_6 1009 # ASSIGN : s_5_7 1069 # ASSIGN : s_5_8 1098 # ASSIGN : s_5_9 1105 # ASSIGN : s_6_0 341 # ASSIGN : s_6_1 426 # ASSIGN : s_6_2 521 # ASSIGN : s_6_3 569 # ASSIGN : s_6_4 596 # ASSIGN : s_6_5 678 # ASSIGN : s_6_6 757 # ASSIGN : s_6_7 966 # ASSIGN : s_6_8 993 # ASSIGN : s_6_9 1167 # ASSIGN : s_7_0 168 # ASSIGN : s_7_1 437 # ASSIGN : s_7_2 583 # ASSIGN : s_7_3 670 # ASSIGN : s_7_4 718 # ASSIGN : s_7_5 759 # ASSIGN : s_7_6 795 # ASSIGN : s_7_7 825 # ASSIGN : s_7_8 1061 # ASSIGN : s_7_9 1097 # ASSIGN : s_8_0 58 # ASSIGN : s_8_1 133 # ASSIGN : s_8_2 146 # ASSIGN : s_8_3 332 # ASSIGN : s_8_4 461 # ASSIGN : s_8_5 630 # ASSIGN : s_8_6 736 # ASSIGN : s_8_7 824 # ASSIGN : s_8_8 947 # ASSIGN : s_8_9 1057 # ASSIGN : s_9_0 140 # ASSIGN : s_9_1 265 # ASSIGN : s_9_2 291 # ASSIGN : s_9_3 323 # ASSIGN : s_9_4 515 # ASSIGN : s_9_5 584 # ASSIGN : s_9_6 878 # ASSIGN : s_9_7 960 # ASSIGN : s_9_8 987 # ASSIGN : s_9_9 1119 # ASSIGN : s_10_0 227 # ASSIGN : s_10_1 289 # ASSIGN : s_10_2 604 # ASSIGN : s_10_3 636 # ASSIGN : s_10_4 698 # ASSIGN : s_10_5 899 # ASSIGN : s_10_6 968 # ASSIGN : s_10_7 1003 # ASSIGN : s_10_8 1075 # ASSIGN : s_10_9 1080 # ASSIGN : s_11_0 39 # ASSIGN : s_11_1 117 # ASSIGN : s_11_2 207 # ASSIGN : s_11_3 323 # ASSIGN : s_11_4 395 # ASSIGN : s_11_5 476 # ASSIGN : s_11_6 561 # ASSIGN : s_11_7 616 # ASSIGN : s_11_8 1078 # ASSIGN : s_11_9 1166 # ASSIGN : s_12_0 78 # ASSIGN : s_12_1 106 # ASSIGN : s_12_2 566 # ASSIGN : s_12_3 712 # ASSIGN : s_12_4 800 # ASSIGN : s_12_5 844 # ASSIGN : s_12_6 875 # ASSIGN : s_12_7 902 # ASSIGN : s_12_8 1001 # ASSIGN : s_12_9 1070 # ASSIGN : s_13_0 25 # ASSIGN : s_13_1 53 # ASSIGN : s_13_2 539 # ASSIGN : s_13_3 595 # ASSIGN : s_13_4 657 # ASSIGN : s_13_5 793 # ASSIGN : s_13_6 872 # ASSIGN : s_13_7 1027 # ASSIGN : s_13_8 1050 # ASSIGN : s_13_9 1097 # ASSIGN : s_14_0 35 # ASSIGN : s_14_1 53 # ASSIGN : s_14_2 146 # ASSIGN : s_14_3 204 # ASSIGN : s_14_4 324 # ASSIGN : s_14_5 393 # ASSIGN : s_14_6 450 # ASSIGN : s_14_7 501 # ASSIGN : s_14_8 657 # ASSIGN : s_14_9 736 SHOW_RESULT 1173 END : 1173 (1 seconds) [Thu Jun 1 16:51:09 2006] SHOW_RESULT 1173 CPU : 0.560000000000002 = 0.560000000000002 + 0 + 0 + 0 # BOUND : makespan 1032 1173 MODIFY_CNF 1102 BEGIN : [Thu Jun 1 16:51:09 2006] MODIFY_CNF 1102 END : 70616475 bytes (0 seconds) [Thu Jun 1 16:51:09 2006] MODIFY_CNF 1102 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1102 BEGIN : [Thu Jun 1 16:51:09 2006] CMD : minisat /work/tamura/csp2sat33598.cnf /work/tamura/csp2sat33598.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1520143 4474663 | 506714 0 0 NaNQ | 0.000 % | | 100 | 1520143 4474663 | 557385 100 1032 10.3 | 56.694 % | ==============================================================================) restarts : 2 conflicts : 133 (32 /sec) decisions : 554 (132 /sec) propagations : 1207886 (288492 /sec) inspects : 12796006 (3056205 /sec) conflict literals : 1387 (25.67 % deleted) CPU time : 4.18689 s SATISFIABLE VERIFY_CNF 1102 END : (5 seconds) [Thu Jun 1 16:51:14 2006] VERIFY_CNF 1102 CPU : 5.39 = 0 + 0.00999999999999998 + 5.11 + 0.27 # RESULT : makespan 1102 SATISFIABLE SHOW_RESULT 1102 BEGIN : [Thu Jun 1 16:51:14 2006] # ASSIGN : makespan 1102 # ASSIGN : s_0_0 110 # ASSIGN : s_0_1 419 # ASSIGN : s_0_2 477 # ASSIGN : s_0_3 604 # ASSIGN : s_0_4 665 # ASSIGN : s_0_5 762 # ASSIGN : s_0_6 900 # ASSIGN : s_0_7 905 # ASSIGN : s_0_8 997 # ASSIGN : s_0_9 1093 # ASSIGN : s_1_0 100 # ASSIGN : s_1_1 121 # ASSIGN : s_1_2 208 # ASSIGN : s_1_3 223 # ASSIGN : s_1_4 393 # ASSIGN : s_1_5 474 # ASSIGN : s_1_6 568 # ASSIGN : s_1_7 609 # ASSIGN : s_1_8 748 # ASSIGN : s_1_9 821 # ASSIGN : s_2_0 245 # ASSIGN : s_2_1 483 # ASSIGN : s_2_2 554 # ASSIGN : s_2_3 588 # ASSIGN : s_2_4 670 # ASSIGN : s_2_5 740 # ASSIGN : s_2_6 809 # ASSIGN : s_2_7 835 # ASSIGN : s_2_8 915 # ASSIGN : s_2_9 963 # ASSIGN : s_3_0 262 # ASSIGN : s_3_1 340 # ASSIGN : s_3_2 370 # ASSIGN : s_3_3 411 # ASSIGN : s_3_4 495 # ASSIGN : s_3_5 506 # ASSIGN : s_3_6 666 # ASSIGN : s_3_7 713 # ASSIGN : s_3_8 748 # ASSIGN : s_3_9 962 # ASSIGN : s_4_0 137 # ASSIGN : s_4_1 196 # ASSIGN : s_4_2 299 # ASSIGN : s_4_3 370 # ASSIGN : s_4_4 654 # ASSIGN : s_4_5 718 # ASSIGN : s_4_6 872 # ASSIGN : s_4_7 887 # ASSIGN : s_4_8 937 # ASSIGN : s_4_9 1012 # ASSIGN : s_5_0 5 # ASSIGN : s_5_1 98 # ASSIGN : s_5_2 243 # ASSIGN : s_5_3 300 # ASSIGN : s_5_4 400 # ASSIGN : s_5_5 538 # ASSIGN : s_5_6 596 # ASSIGN : s_5_7 648 # ASSIGN : s_5_8 825 # ASSIGN : s_5_9 832 # ASSIGN : s_6_0 9 # ASSIGN : s_6_1 150 # ASSIGN : s_6_2 323 # ASSIGN : s_6_3 403 # ASSIGN : s_6_4 475 # ASSIGN : s_6_5 557 # ASSIGN : s_6_6 677 # ASSIGN : s_6_7 799 # ASSIGN : s_6_8 922 # ASSIGN : s_6_9 1096 # ASSIGN : s_7_0 7 # ASSIGN : s_7_1 83 # ASSIGN : s_7_2 157 # ASSIGN : s_7_3 235 # ASSIGN : s_7_4 282 # ASSIGN : s_7_5 357 # ASSIGN : s_7_6 508 # ASSIGN : s_7_7 565 # ASSIGN : s_7_8 785 # ASSIGN : s_7_9 1026 # ASSIGN : s_8_0 22 # ASSIGN : s_8_1 97 # ASSIGN : s_8_2 259 # ASSIGN : s_8_3 371 # ASSIGN : s_8_4 429 # ASSIGN : s_8_5 483 # ASSIGN : s_8_6 567 # ASSIGN : s_8_7 655 # ASSIGN : s_8_8 952 # ASSIGN : s_8_9 1089 # ASSIGN : s_9_0 24 # ASSIGN : s_9_1 39 # ASSIGN : s_9_2 65 # ASSIGN : s_9_3 132 # ASSIGN : s_9_4 231 # ASSIGN : s_9_5 285 # ASSIGN : s_9_6 337 # ASSIGN : s_9_7 826 # ASSIGN : s_9_8 863 # ASSIGN : s_9_9 951 # ASSIGN : s_10_0 39 # ASSIGN : s_10_1 114 # ASSIGN : s_10_2 191 # ASSIGN : s_10_3 338 # ASSIGN : s_10_4 437 # ASSIGN : s_10_5 559 # ASSIGN : s_10_6 620 # ASSIGN : s_10_7 920 # ASSIGN : s_10_8 992 # ASSIGN : s_10_9 1009 # ASSIGN : s_11_0 181 # ASSIGN : s_11_1 310 # ASSIGN : s_11_2 400 # ASSIGN : s_11_3 485 # ASSIGN : s_11_4 787 # ASSIGN : s_11_5 851 # ASSIGN : s_11_6 914 # ASSIGN : s_11_7 925 # ASSIGN : s_11_8 1007 # ASSIGN : s_11_9 1095 # ASSIGN : s_12_0 287 # ASSIGN : s_12_1 577 # ASSIGN : s_12_2 599 # ASSIGN : s_12_3 649 # ASSIGN : s_12_4 737 # ASSIGN : s_12_5 781 # ASSIGN : s_12_6 812 # ASSIGN : s_12_7 839 # ASSIGN : s_12_8 1005 # ASSIGN : s_12_9 1054 # ASSIGN : s_13_0 30 # ASSIGN : s_13_1 44 # ASSIGN : s_13_2 196 # ASSIGN : s_13_3 315 # ASSIGN : s_13_4 377 # ASSIGN : s_13_5 511 # ASSIGN : s_13_6 664 # ASSIGN : s_13_7 733 # ASSIGN : s_13_8 740 # ASSIGN : s_13_9 1017 # ASSIGN : s_14_0 83 # ASSIGN : s_14_1 101 # ASSIGN : s_14_2 194 # ASSIGN : s_14_3 252 # ASSIGN : s_14_4 301 # ASSIGN : s_14_5 454 # ASSIGN : s_14_6 677 # ASSIGN : s_14_7 728 # ASSIGN : s_14_8 819 # ASSIGN : s_14_9 898 SHOW_RESULT 1102 END : 1102 (1 seconds) [Thu Jun 1 16:51:15 2006] SHOW_RESULT 1102 CPU : 0.539999999999992 = 0.539999999999992 + 0 + 0 + 0 # BOUND : makespan 1032 1102 MODIFY_CNF 1067 BEGIN : [Thu Jun 1 16:51:15 2006] MODIFY_CNF 1067 END : 70616475 bytes (0 seconds) [Thu Jun 1 16:51:15 2006] MODIFY_CNF 1067 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1067 BEGIN : [Thu Jun 1 16:51:15 2006] CMD : minisat /work/tamura/csp2sat33598.cnf /work/tamura/csp2sat33598.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1420505 4181072 | 473501 0 0 NaNQ | 0.000 % | | 100 | 1420505 4181072 | 520851 100 1170 11.7 | 59.359 % | | 250 | 1420505 4181072 | 572936 250 3593 14.4 | 59.359 % | | 475 | 1420505 4181072 | 630229 475 7216 15.2 | 59.359 % | | 812 | 1420505 4181072 | 693252 812 13196 16.3 | 59.359 % | | 1318 | 1420505 4181072 | 762578 1318 23035 17.5 | 59.359 % | | 2077 | 1420505 4181072 | 838835 2077 42741 20.6 | 59.359 % | ==============================================================================) restarts : 7 conflicts : 2350 (167 /sec) decisions : 4262 (303 /sec) propagations : 17848801 (1268769 /sec) inspects : 200340110 (14241029 /sec) conflict literals : 47271 (22.64 % deleted) CPU time : 14.0678 s SATISFIABLE VERIFY_CNF 1067 END : (15 seconds) [Thu Jun 1 16:51:30 2006] VERIFY_CNF 1067 CPU : 15.22 = 0 + 0.02 + 14.94 + 0.26 # RESULT : makespan 1067 SATISFIABLE SHOW_RESULT 1067 BEGIN : [Thu Jun 1 16:51:30 2006] # ASSIGN : makespan 1067 # ASSIGN : s_0_0 26 # ASSIGN : s_0_1 203 # ASSIGN : s_0_2 261 # ASSIGN : s_0_3 338 # ASSIGN : s_0_4 385 # ASSIGN : s_0_5 482 # ASSIGN : s_0_6 847 # ASSIGN : s_0_7 854 # ASSIGN : s_0_8 962 # ASSIGN : s_0_9 1058 # ASSIGN : s_1_0 0 # ASSIGN : s_1_1 21 # ASSIGN : s_1_2 108 # ASSIGN : s_1_3 123 # ASSIGN : s_1_4 163 # ASSIGN : s_1_5 567 # ASSIGN : s_1_6 658 # ASSIGN : s_1_7 732 # ASSIGN : s_1_8 789 # ASSIGN : s_1_9 862 # ASSIGN : s_2_0 12 # ASSIGN : s_2_1 52 # ASSIGN : s_2_2 134 # ASSIGN : s_2_3 173 # ASSIGN : s_2_4 255 # ASSIGN : s_2_5 325 # ASSIGN : s_2_6 375 # ASSIGN : s_2_7 386 # ASSIGN : s_2_8 970 # ASSIGN : s_2_9 1018 # ASSIGN : s_3_0 419 # ASSIGN : s_3_1 622 # ASSIGN : s_3_2 652 # ASSIGN : s_3_3 660 # ASSIGN : s_3_4 757 # ASSIGN : s_3_5 768 # ASSIGN : s_3_6 830 # ASSIGN : s_3_7 877 # ASSIGN : s_3_8 912 # ASSIGN : s_3_9 1003 # ASSIGN : s_4_0 5 # ASSIGN : s_4_1 25 # ASSIGN : s_4_2 37 # ASSIGN : s_4_3 110 # ASSIGN : s_4_4 180 # ASSIGN : s_4_5 244 # ASSIGN : s_4_6 349 # ASSIGN : s_4_7 369 # ASSIGN : s_4_8 423 # ASSIGN : s_4_9 515 # ASSIGN : s_5_0 108 # ASSIGN : s_5_1 261 # ASSIGN : s_5_2 366 # ASSIGN : s_5_3 466 # ASSIGN : s_5_4 544 # ASSIGN : s_5_5 644 # ASSIGN : s_5_6 774 # ASSIGN : s_5_7 841 # ASSIGN : s_5_8 870 # ASSIGN : s_5_9 999 # ASSIGN : s_6_0 272 # ASSIGN : s_6_1 331 # ASSIGN : s_6_2 426 # ASSIGN : s_6_3 491 # ASSIGN : s_6_4 530 # ASSIGN : s_6_5 612 # ASSIGN : s_6_6 753 # ASSIGN : s_6_7 852 # ASSIGN : s_6_8 887 # ASSIGN : s_6_9 1061 # ASSIGN : s_7_0 179 # ASSIGN : s_7_1 354 # ASSIGN : s_7_2 392 # ASSIGN : s_7_3 495 # ASSIGN : s_7_4 503 # ASSIGN : s_7_5 666 # ASSIGN : s_7_6 702 # ASSIGN : s_7_7 732 # ASSIGN : s_7_8 826 # ASSIGN : s_7_9 991 # ASSIGN : s_8_0 102 # ASSIGN : s_8_1 177 # ASSIGN : s_8_2 382 # ASSIGN : s_8_3 474 # ASSIGN : s_8_4 517 # ASSIGN : s_8_5 571 # ASSIGN : s_8_6 653 # ASSIGN : s_8_7 741 # ASSIGN : s_8_8 917 # ASSIGN : s_8_9 986 # ASSIGN : s_9_0 118 # ASSIGN : s_9_1 124 # ASSIGN : s_9_2 190 # ASSIGN : s_9_3 257 # ASSIGN : s_9_4 321 # ASSIGN : s_9_5 442 # ASSIGN : s_9_6 494 # ASSIGN : s_9_7 659 # ASSIGN : s_9_8 665 # ASSIGN : s_9_9 1013 # ASSIGN : s_10_0 364 # ASSIGN : s_10_1 463 # ASSIGN : s_10_2 576 # ASSIGN : s_10_3 627 # ASSIGN : s_10_4 689 # ASSIGN : s_10_5 758 # ASSIGN : s_10_6 819 # ASSIGN : s_10_7 885 # ASSIGN : s_10_8 957 # ASSIGN : s_10_9 974 # ASSIGN : s_11_0 5 # ASSIGN : s_11_1 83 # ASSIGN : s_11_2 246 # ASSIGN : s_11_3 423 # ASSIGN : s_11_4 668 # ASSIGN : s_11_5 816 # ASSIGN : s_11_6 879 # ASSIGN : s_11_7 890 # ASSIGN : s_11_8 972 # ASSIGN : s_11_9 1060 # ASSIGN : s_12_0 44 # ASSIGN : s_12_1 72 # ASSIGN : s_12_2 222 # ASSIGN : s_12_3 347 # ASSIGN : s_12_4 564 # ASSIGN : s_12_5 608 # ASSIGN : s_12_6 639 # ASSIGN : s_12_7 675 # ASSIGN : s_12_8 902 # ASSIGN : s_12_9 951 # ASSIGN : s_13_0 148 # ASSIGN : s_13_1 162 # ASSIGN : s_13_2 201 # ASSIGN : s_13_3 259 # ASSIGN : s_13_4 326 # ASSIGN : s_13_5 470 # ASSIGN : s_13_6 536 # ASSIGN : s_13_7 605 # ASSIGN : s_13_8 621 # ASSIGN : s_13_9 698 # ASSIGN : s_14_0 150 # ASSIGN : s_14_1 168 # ASSIGN : s_14_2 328 # ASSIGN : s_14_3 435 # ASSIGN : s_14_4 498 # ASSIGN : s_14_5 608 # ASSIGN : s_14_6 712 # ASSIGN : s_14_7 753 # ASSIGN : s_14_8 806 # ASSIGN : s_14_9 939 SHOW_RESULT 1067 END : 1067 (0 seconds) [Thu Jun 1 16:51:30 2006] SHOW_RESULT 1067 CPU : 0.539999999999992 = 0.539999999999992 + 0 + 0 + 0 # BOUND : makespan 1032 1067 MODIFY_CNF 1049 BEGIN : [Thu Jun 1 16:51:30 2006] MODIFY_CNF 1049 END : 70616475 bytes (0 seconds) [Thu Jun 1 16:51:30 2006] MODIFY_CNF 1049 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1049 BEGIN : [Thu Jun 1 16:51:30 2006] CMD : minisat /work/tamura/csp2sat33598.cnf /work/tamura/csp2sat33598.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1369963 4032183 | 456654 0 0 NaNQ | 0.000 % | | 100 | 1369963 4032183 | 502319 100 1297 13.0 | 60.731 % | | 250 | 1369963 4032183 | 552551 250 4515 18.1 | 60.731 % | | 476 | 1369963 4032183 | 607806 476 8008 16.8 | 60.731 % | | 814 | 1369963 4032183 | 668587 814 19669 24.2 | 60.731 % | | 1321 | 1369963 4032183 | 735445 1321 29774 22.5 | 60.731 % | ==============================================================================) restarts : 6 conflicts : 1363 (156 /sec) decisions : 2633 (301 /sec) propagations : 8866499 (1014493 /sec) inspects : 101274949 (11587744 /sec) conflict literals : 30362 (18.33 % deleted) CPU time : 8.73983 s SATISFIABLE VERIFY_CNF 1049 END : (10 seconds) [Thu Jun 1 16:51:40 2006] VERIFY_CNF 1049 CPU : 9.86999999999999 = 0.00999999999999091 + 0.01 + 9.59 + 0.26 # RESULT : makespan 1049 SATISFIABLE SHOW_RESULT 1049 BEGIN : [Thu Jun 1 16:51:40 2006] # ASSIGN : makespan 1049 # ASSIGN : s_0_0 179 # ASSIGN : s_0_1 263 # ASSIGN : s_0_2 323 # ASSIGN : s_0_3 405 # ASSIGN : s_0_4 449 # ASSIGN : s_0_5 696 # ASSIGN : s_0_6 840 # ASSIGN : s_0_7 845 # ASSIGN : s_0_8 944 # ASSIGN : s_0_9 1040 # ASSIGN : s_1_0 3 # ASSIGN : s_1_1 122 # ASSIGN : s_1_2 209 # ASSIGN : s_1_3 224 # ASSIGN : s_1_4 288 # ASSIGN : s_1_5 382 # ASSIGN : s_1_6 467 # ASSIGN : s_1_7 498 # ASSIGN : s_1_8 555 # ASSIGN : s_1_9 628 # ASSIGN : s_2_0 237 # ASSIGN : s_2_1 321 # ASSIGN : s_2_2 400 # ASSIGN : s_2_3 440 # ASSIGN : s_2_4 522 # ASSIGN : s_2_5 674 # ASSIGN : s_2_6 720 # ASSIGN : s_2_7 754 # ASSIGN : s_2_8 862 # ASSIGN : s_2_9 910 # ASSIGN : s_3_0 2 # ASSIGN : s_3_1 204 # ASSIGN : s_3_2 228 # ASSIGN : s_3_3 235 # ASSIGN : s_3_4 382 # ASSIGN : s_3_5 584 # ASSIGN : s_3_6 646 # ASSIGN : s_3_7 693 # ASSIGN : s_3_8 754 # ASSIGN : s_3_9 873 # ASSIGN : s_4_0 78 # ASSIGN : s_4_1 105 # ASSIGN : s_4_2 117 # ASSIGN : s_4_3 272 # ASSIGN : s_4_4 376 # ASSIGN : s_4_5 604 # ASSIGN : s_4_6 698 # ASSIGN : s_4_7 713 # ASSIGN : s_4_8 858 # ASSIGN : s_4_9 959 # ASSIGN : s_5_0 24 # ASSIGN : s_5_1 131 # ASSIGN : s_5_2 305 # ASSIGN : s_5_3 397 # ASSIGN : s_5_4 569 # ASSIGN : s_5_5 662 # ASSIGN : s_5_6 757 # ASSIGN : s_5_7 815 # ASSIGN : s_5_8 844 # ASSIGN : s_5_9 981 # ASSIGN : s_6_0 20 # ASSIGN : s_6_1 139 # ASSIGN : s_6_2 234 # ASSIGN : s_6_3 393 # ASSIGN : s_6_4 495 # ASSIGN : s_6_5 590 # ASSIGN : s_6_6 657 # ASSIGN : s_6_7 813 # ASSIGN : s_6_8 869 # ASSIGN : s_6_9 1043 # ASSIGN : s_7_0 1 # ASSIGN : s_7_1 77 # ASSIGN : s_7_2 98 # ASSIGN : s_7_3 274 # ASSIGN : s_7_4 282 # ASSIGN : s_7_5 369 # ASSIGN : s_7_6 419 # ASSIGN : s_7_7 785 # ASSIGN : s_7_8 928 # ASSIGN : s_7_9 973 # ASSIGN : s_8_0 1 # ASSIGN : s_8_1 76 # ASSIGN : s_8_2 123 # ASSIGN : s_8_3 205 # ASSIGN : s_8_4 253 # ASSIGN : s_8_5 307 # ASSIGN : s_8_6 424 # ASSIGN : s_8_7 512 # ASSIGN : s_8_8 728 # ASSIGN : s_8_9 968 # ASSIGN : s_9_0 39 # ASSIGN : s_9_1 63 # ASSIGN : s_9_2 89 # ASSIGN : s_9_3 477 # ASSIGN : s_9_4 546 # ASSIGN : s_9_5 705 # ASSIGN : s_9_6 763 # ASSIGN : s_9_7 845 # ASSIGN : s_9_8 851 # ASSIGN : s_9_9 995 # ASSIGN : s_10_0 143 # ASSIGN : s_10_1 221 # ASSIGN : s_10_2 392 # ASSIGN : s_10_3 440 # ASSIGN : s_10_4 515 # ASSIGN : s_10_5 592 # ASSIGN : s_10_6 653 # ASSIGN : s_10_7 867 # ASSIGN : s_10_8 939 # ASSIGN : s_10_9 956 # ASSIGN : s_11_0 45 # ASSIGN : s_11_1 187 # ASSIGN : s_11_2 277 # ASSIGN : s_11_3 362 # ASSIGN : s_11_4 434 # ASSIGN : s_11_5 597 # ASSIGN : s_11_6 660 # ASSIGN : s_11_7 672 # ASSIGN : s_11_8 954 # ASSIGN : s_11_9 1042 # ASSIGN : s_12_0 148 # ASSIGN : s_12_1 176 # ASSIGN : s_12_2 339 # ASSIGN : s_12_3 389 # ASSIGN : s_12_4 502 # ASSIGN : s_12_5 546 # ASSIGN : s_12_6 577 # ASSIGN : s_12_7 688 # ASSIGN : s_12_8 868 # ASSIGN : s_12_9 933 # ASSIGN : s_13_0 25 # ASSIGN : s_13_1 92 # ASSIGN : s_13_2 541 # ASSIGN : s_13_3 600 # ASSIGN : s_13_4 671 # ASSIGN : s_13_5 768 # ASSIGN : s_13_6 834 # ASSIGN : s_13_7 903 # ASSIGN : s_13_8 917 # ASSIGN : s_13_9 964 # ASSIGN : s_14_0 10 # ASSIGN : s_14_1 28 # ASSIGN : s_14_2 121 # ASSIGN : s_14_3 188 # ASSIGN : s_14_4 313 # ASSIGN : s_14_5 383 # ASSIGN : s_14_6 454 # ASSIGN : s_14_7 660 # ASSIGN : s_14_8 730 # ASSIGN : s_14_9 809 SHOW_RESULT 1049 END : 1049 (1 seconds) [Thu Jun 1 16:51:41 2006] SHOW_RESULT 1049 CPU : 0.539999999999992 = 0.539999999999992 + 0 + 0 + 0 # BOUND : makespan 1032 1049 MODIFY_CNF 1040 BEGIN : [Thu Jun 1 16:51:41 2006] MODIFY_CNF 1040 END : 70616475 bytes (0 seconds) [Thu Jun 1 16:51:41 2006] MODIFY_CNF 1040 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1040 BEGIN : [Thu Jun 1 16:51:41 2006] CMD : minisat /work/tamura/csp2sat33598.cnf /work/tamura/csp2sat33598.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1345565 3960357 | 448521 0 0 NaNQ | 0.000 % | | 101 | 1345565 3960357 | 493373 101 1014 10.0 | 61.415 % | | 251 | 1345565 3960357 | 542710 251 3861 15.4 | 61.415 % | | 476 | 1345565 3960357 | 596981 476 7924 16.6 | 61.415 % | | 813 | 1345565 3960357 | 656679 813 14745 18.1 | 61.415 % | ==============================================================================) restarts : 5 conflicts : 1203 (144 /sec) decisions : 2311 (276 /sec) propagations : 8437387 (1007881 /sec) inspects : 89898049 (10738699 /sec) conflict literals : 24817 (21.76 % deleted) CPU time : 8.37141 s SATISFIABLE VERIFY_CNF 1040 END : (9 seconds) [Thu Jun 1 16:51:50 2006] VERIFY_CNF 1040 CPU : 9.48 = 0 + 0.02 + 9.21 + 0.25 # RESULT : makespan 1040 SATISFIABLE SHOW_RESULT 1040 BEGIN : [Thu Jun 1 16:51:50 2006] # ASSIGN : makespan 1040 # ASSIGN : s_0_0 11 # ASSIGN : s_0_1 114 # ASSIGN : s_0_2 172 # ASSIGN : s_0_3 249 # ASSIGN : s_0_4 424 # ASSIGN : s_0_5 594 # ASSIGN : s_0_6 702 # ASSIGN : s_0_7 707 # ASSIGN : s_0_8 935 # ASSIGN : s_0_9 1031 # ASSIGN : s_1_0 0 # ASSIGN : s_1_1 244 # ASSIGN : s_1_2 371 # ASSIGN : s_1_3 404 # ASSIGN : s_1_4 536 # ASSIGN : s_1_5 617 # ASSIGN : s_1_6 729 # ASSIGN : s_1_7 760 # ASSIGN : s_1_8 817 # ASSIGN : s_1_9 890 # ASSIGN : s_2_0 111 # ASSIGN : s_2_1 186 # ASSIGN : s_2_2 346 # ASSIGN : s_2_3 380 # ASSIGN : s_2_4 486 # ASSIGN : s_2_5 683 # ASSIGN : s_2_6 734 # ASSIGN : s_2_7 783 # ASSIGN : s_2_8 943 # ASSIGN : s_2_9 991 # ASSIGN : s_3_0 0 # ASSIGN : s_3_1 151 # ASSIGN : s_3_2 281 # ASSIGN : s_3_3 288 # ASSIGN : s_3_4 386 # ASSIGN : s_3_5 397 # ASSIGN : s_3_6 494 # ASSIGN : s_3_7 581 # ASSIGN : s_3_8 616 # ASSIGN : s_3_9 747 # ASSIGN : s_4_0 85 # ASSIGN : s_4_1 105 # ASSIGN : s_4_2 170 # ASSIGN : s_4_3 248 # ASSIGN : s_4_4 333 # ASSIGN : s_4_5 442 # ASSIGN : s_4_6 541 # ASSIGN : s_4_7 587 # ASSIGN : s_4_8 725 # ASSIGN : s_4_9 800 # ASSIGN : s_5_0 21 # ASSIGN : s_5_1 272 # ASSIGN : s_5_2 411 # ASSIGN : s_5_3 597 # ASSIGN : s_5_4 667 # ASSIGN : s_5_5 744 # ASSIGN : s_5_6 802 # ASSIGN : s_5_7 899 # ASSIGN : s_5_8 928 # ASSIGN : s_5_9 937 # ASSIGN : s_6_0 95 # ASSIGN : s_6_1 151 # ASSIGN : s_6_2 286 # ASSIGN : s_6_3 334 # ASSIGN : s_6_4 360 # ASSIGN : s_6_5 468 # ASSIGN : s_6_6 545 # ASSIGN : s_6_7 825 # ASSIGN : s_6_8 860 # ASSIGN : s_6_9 1034 # ASSIGN : s_7_0 181 # ASSIGN : s_7_1 257 # ASSIGN : s_7_2 302 # ASSIGN : s_7_3 403 # ASSIGN : s_7_4 453 # ASSIGN : s_7_5 639 # ASSIGN : s_7_6 675 # ASSIGN : s_7_7 705 # ASSIGN : s_7_8 854 # ASSIGN : s_7_9 964 # ASSIGN : s_8_0 36 # ASSIGN : s_8_1 155 # ASSIGN : s_8_2 168 # ASSIGN : s_8_3 251 # ASSIGN : s_8_4 280 # ASSIGN : s_8_5 360 # ASSIGN : s_8_6 443 # ASSIGN : s_8_7 531 # ASSIGN : s_8_8 632 # ASSIGN : s_8_9 924 # ASSIGN : s_9_0 67 # ASSIGN : s_9_1 218 # ASSIGN : s_9_2 365 # ASSIGN : s_9_3 442 # ASSIGN : s_9_4 521 # ASSIGN : s_9_5 575 # ASSIGN : s_9_6 637 # ASSIGN : s_9_7 719 # ASSIGN : s_9_8 729 # ASSIGN : s_9_9 902 # ASSIGN : s_10_0 17 # ASSIGN : s_10_1 293 # ASSIGN : s_10_2 365 # ASSIGN : s_10_3 397 # ASSIGN : s_10_4 459 # ASSIGN : s_10_5 556 # ASSIGN : s_10_6 765 # ASSIGN : s_10_7 816 # ASSIGN : s_10_8 923 # ASSIGN : s_10_9 947 # ASSIGN : s_11_0 73 # ASSIGN : s_11_1 156 # ASSIGN : s_11_2 246 # ASSIGN : s_11_3 331 # ASSIGN : s_11_4 556 # ASSIGN : s_11_5 789 # ASSIGN : s_11_6 852 # ASSIGN : s_11_7 863 # ASSIGN : s_11_8 945 # ASSIGN : s_11_9 1033 # ASSIGN : s_12_0 117 # ASSIGN : s_12_1 145 # ASSIGN : s_12_2 315 # ASSIGN : s_12_3 506 # ASSIGN : s_12_4 627 # ASSIGN : s_12_5 832 # ASSIGN : s_12_6 863 # ASSIGN : s_12_7 890 # ASSIGN : s_12_8 956 # ASSIGN : s_12_9 1005 # ASSIGN : s_13_0 53 # ASSIGN : s_13_1 75 # ASSIGN : s_13_2 114 # ASSIGN : s_13_3 218 # ASSIGN : s_13_4 365 # ASSIGN : s_13_5 462 # ASSIGN : s_13_6 528 # ASSIGN : s_13_7 609 # ASSIGN : s_13_8 620 # ASSIGN : s_13_9 671 # ASSIGN : s_14_0 61 # ASSIGN : s_14_1 79 # ASSIGN : s_14_2 183 # ASSIGN : s_14_3 241 # ASSIGN : s_14_4 296 # ASSIGN : s_14_5 672 # ASSIGN : s_14_6 738 # ASSIGN : s_14_7 779 # ASSIGN : s_14_8 888 # ASSIGN : s_14_9 967 SHOW_RESULT 1040 END : 1040 (1 seconds) [Thu Jun 1 16:51:51 2006] SHOW_RESULT 1040 CPU : 0.54000000000002 = 0.54000000000002 + 0 + 0 + 0 # BOUND : makespan 1032 1040 MODIFY_CNF 1036 BEGIN : [Thu Jun 1 16:51:51 2006] MODIFY_CNF 1036 END : 70616474 bytes (0 seconds) [Thu Jun 1 16:51:51 2006] MODIFY_CNF 1036 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1036 BEGIN : [Thu Jun 1 16:51:51 2006] CMD : minisat /work/tamura/csp2sat33598.cnf /work/tamura/csp2sat33598.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1332107 3920595 | 444035 0 0 NaNQ | 0.000 % | | 100 | 1332107 3920595 | 488438 100 1188 11.9 | 61.722 % | | 252 | 1332107 3920595 | 537282 252 3097 12.3 | 61.722 % | | 478 | 1332107 3920595 | 591010 478 8170 17.1 | 61.722 % | ==============================================================================) restarts : 4 conflicts : 631 (104 /sec) decisions : 1236 (204 /sec) propagations : 4204368 (694296 /sec) inspects : 44173327 (7294645 /sec) conflict literals : 10314 (19.97 % deleted) CPU time : 6.05558 s SATISFIABLE VERIFY_CNF 1036 END : (7 seconds) [Thu Jun 1 16:51:58 2006] VERIFY_CNF 1036 CPU : 7.15999999999999 = 0 + 0.01 + 6.88999999999999 + 0.26 # RESULT : makespan 1036 SATISFIABLE SHOW_RESULT 1036 BEGIN : [Thu Jun 1 16:51:58 2006] # ASSIGN : makespan 1036 # ASSIGN : s_0_0 8 # ASSIGN : s_0_1 92 # ASSIGN : s_0_2 158 # ASSIGN : s_0_3 274 # ASSIGN : s_0_4 318 # ASSIGN : s_0_5 415 # ASSIGN : s_0_6 554 # ASSIGN : s_0_7 559 # ASSIGN : s_0_8 697 # ASSIGN : s_0_9 908 # ASSIGN : s_1_0 4 # ASSIGN : s_1_1 48 # ASSIGN : s_1_2 135 # ASSIGN : s_1_3 150 # ASSIGN : s_1_4 193 # ASSIGN : s_1_5 333 # ASSIGN : s_1_6 418 # ASSIGN : s_1_7 449 # ASSIGN : s_1_8 528 # ASSIGN : s_1_9 601 # ASSIGN : s_2_0 161 # ASSIGN : s_2_1 282 # ASSIGN : s_2_2 367 # ASSIGN : s_2_3 402 # ASSIGN : s_2_4 484 # ASSIGN : s_2_5 687 # ASSIGN : s_2_6 756 # ASSIGN : s_2_7 779 # ASSIGN : s_2_8 939 # ASSIGN : s_2_9 987 # ASSIGN : s_3_0 353 # ASSIGN : s_3_1 442 # ASSIGN : s_3_2 477 # ASSIGN : s_3_3 551 # ASSIGN : s_3_4 689 # ASSIGN : s_3_5 717 # ASSIGN : s_3_6 800 # ASSIGN : s_3_7 847 # ASSIGN : s_3_8 890 # ASSIGN : s_3_9 981 # ASSIGN : s_4_0 80 # ASSIGN : s_4_1 162 # ASSIGN : s_4_2 174 # ASSIGN : s_4_3 281 # ASSIGN : s_4_4 425 # ASSIGN : s_4_5 489 # ASSIGN : s_4_6 583 # ASSIGN : s_4_7 675 # ASSIGN : s_4_8 725 # ASSIGN : s_4_9 800 # ASSIGN : s_5_0 25 # ASSIGN : s_5_1 189 # ASSIGN : s_5_2 291 # ASSIGN : s_5_3 348 # ASSIGN : s_5_4 506 # ASSIGN : s_5_5 601 # ASSIGN : s_5_6 806 # ASSIGN : s_5_7 858 # ASSIGN : s_5_8 887 # ASSIGN : s_5_9 920 # ASSIGN : s_6_0 225 # ASSIGN : s_6_1 286 # ASSIGN : s_6_2 401 # ASSIGN : s_6_3 575 # ASSIGN : s_6_4 630 # ASSIGN : s_6_5 730 # ASSIGN : s_6_6 793 # ASSIGN : s_6_7 829 # ASSIGN : s_6_8 856 # ASSIGN : s_6_9 1030 # ASSIGN : s_7_0 1 # ASSIGN : s_7_1 77 # ASSIGN : s_7_2 205 # ASSIGN : s_7_3 283 # ASSIGN : s_7_4 326 # ASSIGN : s_7_5 594 # ASSIGN : s_7_6 659 # ASSIGN : s_7_7 772 # ASSIGN : s_7_8 872 # ASSIGN : s_7_9 960 # ASSIGN : s_8_0 24 # ASSIGN : s_8_1 99 # ASSIGN : s_8_2 112 # ASSIGN : s_8_3 235 # ASSIGN : s_8_4 264 # ASSIGN : s_8_5 333 # ASSIGN : s_8_6 529 # ASSIGN : s_8_7 617 # ASSIGN : s_8_8 983 # ASSIGN : s_8_9 1023 # ASSIGN : s_9_0 13 # ASSIGN : s_9_1 22 # ASSIGN : s_9_2 451 # ASSIGN : s_9_3 623 # ASSIGN : s_9_4 700 # ASSIGN : s_9_5 754 # ASSIGN : s_9_6 806 # ASSIGN : s_9_7 888 # ASSIGN : s_9_8 894 # ASSIGN : s_9_9 982 # ASSIGN : s_10_0 264 # ASSIGN : s_10_1 375 # ASSIGN : s_10_2 471 # ASSIGN : s_10_3 503 # ASSIGN : s_10_4 565 # ASSIGN : s_10_5 634 # ASSIGN : s_10_6 695 # ASSIGN : s_10_7 766 # ASSIGN : s_10_8 882 # ASSIGN : s_10_9 943 # ASSIGN : s_11_0 33 # ASSIGN : s_11_1 111 # ASSIGN : s_11_2 201 # ASSIGN : s_11_3 414 # ASSIGN : s_11_4 645 # ASSIGN : s_11_5 709 # ASSIGN : s_11_6 818 # ASSIGN : s_11_7 859 # ASSIGN : s_11_8 941 # ASSIGN : s_11_9 1029 # ASSIGN : s_12_0 72 # ASSIGN : s_12_1 100 # ASSIGN : s_12_2 175 # ASSIGN : s_12_3 245 # ASSIGN : s_12_4 381 # ASSIGN : s_12_5 428 # ASSIGN : s_12_6 459 # ASSIGN : s_12_7 486 # ASSIGN : s_12_8 933 # ASSIGN : s_12_9 988 # ASSIGN : s_13_0 19 # ASSIGN : s_13_1 38 # ASSIGN : s_13_2 118 # ASSIGN : s_13_3 174 # ASSIGN : s_13_4 236 # ASSIGN : s_13_5 336 # ASSIGN : s_13_6 483 # ASSIGN : s_13_7 552 # ASSIGN : s_13_8 598 # ASSIGN : s_13_9 678 # ASSIGN : s_14_0 4 # ASSIGN : s_14_1 24 # ASSIGN : s_14_2 117 # ASSIGN : s_14_3 504 # ASSIGN : s_14_4 565 # ASSIGN : s_14_5 640 # ASSIGN : s_14_6 712 # ASSIGN : s_14_7 753 # ASSIGN : s_14_8 838 # ASSIGN : s_14_9 917 SHOW_RESULT 1036 END : 1036 (1 seconds) [Thu Jun 1 16:51:59 2006] SHOW_RESULT 1036 CPU : 0.549999999999992 = 0.539999999999992 + 0.01 + 0 + 0 # BOUND : makespan 1032 1036 MODIFY_CNF 1034 BEGIN : [Thu Jun 1 16:51:59 2006] MODIFY_CNF 1034 END : 70616474 bytes (0 seconds) [Thu Jun 1 16:51:59 2006] MODIFY_CNF 1034 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1034 BEGIN : [Thu Jun 1 16:51:59 2006] CMD : minisat /work/tamura/csp2sat33598.cnf /work/tamura/csp2sat33598.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1326786 3904936 | 442262 0 0 NaNQ | 0.000 % | | 100 | 1326786 3904936 | 486488 100 1101 11.0 | 61.874 % | | 250 | 1326786 3904936 | 535137 250 4866 19.5 | 61.874 % | | 475 | 1326786 3904936 | 588650 475 7893 16.6 | 61.874 % | | 812 | 1326786 3904936 | 647515 812 15865 19.5 | 61.874 % | | 1318 | 1326786 3904936 | 712267 1318 28070 21.3 | 61.874 % | ==============================================================================) restarts : 6 conflicts : 1837 (179 /sec) decisions : 3186 (311 /sec) propagations : 11958126 (1165537 /sec) inspects : 128667196 (12540963 /sec) conflict literals : 36254 (14.20 % deleted) CPU time : 10.2598 s SATISFIABLE VERIFY_CNF 1034 END : (11 seconds) [Thu Jun 1 16:52:10 2006] VERIFY_CNF 1034 CPU : 11.36 = 0 + 0.01 + 11.09 + 0.26 # RESULT : makespan 1034 SATISFIABLE SHOW_RESULT 1034 BEGIN : [Thu Jun 1 16:52:10 2006] # ASSIGN : makespan 1034 # ASSIGN : s_0_0 169 # ASSIGN : s_0_1 253 # ASSIGN : s_0_2 311 # ASSIGN : s_0_3 395 # ASSIGN : s_0_4 439 # ASSIGN : s_0_5 536 # ASSIGN : s_0_6 681 # ASSIGN : s_0_7 686 # ASSIGN : s_0_8 752 # ASSIGN : s_0_9 856 # ASSIGN : s_1_0 2 # ASSIGN : s_1_1 84 # ASSIGN : s_1_2 171 # ASSIGN : s_1_3 186 # ASSIGN : s_1_4 237 # ASSIGN : s_1_5 318 # ASSIGN : s_1_6 403 # ASSIGN : s_1_7 435 # ASSIGN : s_1_8 492 # ASSIGN : s_1_9 565 # ASSIGN : s_2_0 75 # ASSIGN : s_2_1 115 # ASSIGN : s_2_2 229 # ASSIGN : s_2_3 318 # ASSIGN : s_2_4 423 # ASSIGN : s_2_5 514 # ASSIGN : s_2_6 672 # ASSIGN : s_2_7 682 # ASSIGN : s_2_8 762 # ASSIGN : s_2_9 810 # ASSIGN : s_3_0 1 # ASSIGN : s_3_1 203 # ASSIGN : s_3_2 220 # ASSIGN : s_3_3 227 # ASSIGN : s_3_4 315 # ASSIGN : s_3_5 326 # ASSIGN : s_3_6 388 # ASSIGN : s_3_7 457 # ASSIGN : s_3_8 497 # ASSIGN : s_3_9 737 # ASSIGN : s_4_0 119 # ASSIGN : s_4_1 159 # ASSIGN : s_4_2 355 # ASSIGN : s_4_3 434 # ASSIGN : s_4_4 501 # ASSIGN : s_4_5 619 # ASSIGN : s_4_6 713 # ASSIGN : s_4_7 728 # ASSIGN : s_4_8 843 # ASSIGN : s_4_9 944 # ASSIGN : s_5_0 23 # ASSIGN : s_5_1 314 # ASSIGN : s_5_2 440 # ASSIGN : s_5_3 612 # ASSIGN : s_5_4 729 # ASSIGN : s_5_5 806 # ASSIGN : s_5_6 865 # ASSIGN : s_5_7 917 # ASSIGN : s_5_8 946 # ASSIGN : s_5_9 953 # ASSIGN : s_6_0 10 # ASSIGN : s_6_1 168 # ASSIGN : s_6_2 263 # ASSIGN : s_6_3 351 # ASSIGN : s_6_4 460 # ASSIGN : s_6_5 588 # ASSIGN : s_6_6 716 # ASSIGN : s_6_7 810 # ASSIGN : s_6_8 854 # ASSIGN : s_6_9 1028 # ASSIGN : s_7_0 144 # ASSIGN : s_7_1 225 # ASSIGN : s_7_2 240 # ASSIGN : s_7_3 432 # ASSIGN : s_7_4 501 # ASSIGN : s_7_5 542 # ASSIGN : s_7_6 683 # ASSIGN : s_7_7 770 # ASSIGN : s_7_8 922 # ASSIGN : s_7_9 958 # ASSIGN : s_8_0 0 # ASSIGN : s_8_1 98 # ASSIGN : s_8_2 119 # ASSIGN : s_8_3 200 # ASSIGN : s_8_4 618 # ASSIGN : s_8_5 688 # ASSIGN : s_8_6 778 # ASSIGN : s_8_7 866 # ASSIGN : s_8_8 981 # ASSIGN : s_8_9 1021 # ASSIGN : s_9_0 34 # ASSIGN : s_9_1 40 # ASSIGN : s_9_2 66 # ASSIGN : s_9_3 116 # ASSIGN : s_9_4 261 # ASSIGN : s_9_5 387 # ASSIGN : s_9_6 551 # ASSIGN : s_9_7 837 # ASSIGN : s_9_8 848 # ASSIGN : s_9_9 980 # ASSIGN : s_10_0 138 # ASSIGN : s_10_1 328 # ASSIGN : s_10_2 407 # ASSIGN : s_10_3 439 # ASSIGN : s_10_4 521 # ASSIGN : s_10_5 590 # ASSIGN : s_10_6 651 # ASSIGN : s_10_7 864 # ASSIGN : s_10_8 936 # ASSIGN : s_10_9 941 # ASSIGN : s_11_0 41 # ASSIGN : s_11_1 150 # ASSIGN : s_11_2 275 # ASSIGN : s_11_3 360 # ASSIGN : s_11_4 561 # ASSIGN : s_11_5 625 # ASSIGN : s_11_6 799 # ASSIGN : s_11_7 857 # ASSIGN : s_11_8 939 # ASSIGN : s_11_9 1027 # ASSIGN : s_12_0 111 # ASSIGN : s_12_1 139 # ASSIGN : s_12_2 276 # ASSIGN : s_12_3 426 # ASSIGN : s_12_4 642 # ASSIGN : s_12_5 686 # ASSIGN : s_12_6 717 # ASSIGN : s_12_7 744 # ASSIGN : s_12_8 862 # ASSIGN : s_12_9 918 # ASSIGN : s_13_0 20 # ASSIGN : s_13_1 76 # ASSIGN : s_13_2 299 # ASSIGN : s_13_3 377 # ASSIGN : s_13_4 493 # ASSIGN : s_13_5 650 # ASSIGN : s_13_6 788 # ASSIGN : s_13_7 859 # ASSIGN : s_13_8 911 # ASSIGN : s_13_9 958 # ASSIGN : s_14_0 0 # ASSIGN : s_14_1 18 # ASSIGN : s_14_2 111 # ASSIGN : s_14_3 180 # ASSIGN : s_14_4 249 # ASSIGN : s_14_5 400 # ASSIGN : s_14_6 578 # ASSIGN : s_14_7 633 # ASSIGN : s_14_8 713 # ASSIGN : s_14_9 792 SHOW_RESULT 1034 END : 1034 (0 seconds) [Thu Jun 1 16:52:10 2006] SHOW_RESULT 1034 CPU : 0.54000000000002 = 0.54000000000002 + 0 + 0 + 0 # BOUND : makespan 1032 1034 MODIFY_CNF 1033 BEGIN : [Thu Jun 1 16:52:10 2006] MODIFY_CNF 1033 END : 70616474 bytes (0 seconds) [Thu Jun 1 16:52:10 2006] MODIFY_CNF 1033 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1033 BEGIN : [Thu Jun 1 16:52:10 2006] CMD : minisat /work/tamura/csp2sat33598.cnf /work/tamura/csp2sat33598.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1324606 3898547 | 441535 0 0 NaNQ | 0.000 % | | 100 | 1324606 3898547 | 485688 100 1089 10.9 | 61.950 % | | 250 | 1324606 3898547 | 534257 250 2849 11.4 | 61.950 % | | 475 | 1324606 3898547 | 587683 475 5429 11.4 | 61.950 % | | 812 | 1324606 3898547 | 646451 812 9312 11.5 | 61.950 % | | 1318 | 1324606 3898547 | 711096 1318 24040 18.2 | 61.950 % | | 2077 | 1324606 3898547 | 782206 2077 37202 17.9 | 61.950 % | | 3216 | 1324606 3898547 | 860426 3216 50083 15.6 | 61.950 % | ==============================================================================) restarts : 8 conflicts : 4039 (267 /sec) decisions : 6581 (436 /sec) propagations : 22264446 (1473473 /sec) inspects : 231044720 (15290665 /sec) conflict literals : 73773 (18.84 % deleted) CPU time : 15.1102 s SATISFIABLE VERIFY_CNF 1033 END : (17 seconds) [Thu Jun 1 16:52:27 2006] VERIFY_CNF 1033 CPU : 16.23 = 0.00999999999999091 + 0.01 + 15.95 + 0.26 # RESULT : makespan 1033 SATISFIABLE SHOW_RESULT 1033 BEGIN : [Thu Jun 1 16:52:27 2006] # ASSIGN : makespan 1033 # ASSIGN : s_0_0 15 # ASSIGN : s_0_1 131 # ASSIGN : s_0_2 241 # ASSIGN : s_0_3 318 # ASSIGN : s_0_4 362 # ASSIGN : s_0_5 459 # ASSIGN : s_0_6 576 # ASSIGN : s_0_7 581 # ASSIGN : s_0_8 790 # ASSIGN : s_0_9 905 # ASSIGN : s_1_0 1 # ASSIGN : s_1_1 71 # ASSIGN : s_1_2 158 # ASSIGN : s_1_3 189 # ASSIGN : s_1_4 237 # ASSIGN : s_1_5 380 # ASSIGN : s_1_6 474 # ASSIGN : s_1_7 525 # ASSIGN : s_1_8 591 # ASSIGN : s_1_9 664 # ASSIGN : s_2_0 146 # ASSIGN : s_2_1 324 # ASSIGN : s_2_2 414 # ASSIGN : s_2_3 452 # ASSIGN : s_2_4 632 # ASSIGN : s_2_5 747 # ASSIGN : s_2_6 804 # ASSIGN : s_2_7 856 # ASSIGN : s_2_8 936 # ASSIGN : s_2_9 984 # ASSIGN : s_3_0 1 # ASSIGN : s_3_1 214 # ASSIGN : s_3_2 541 # ASSIGN : s_3_3 548 # ASSIGN : s_3_4 635 # ASSIGN : s_3_5 646 # ASSIGN : s_3_6 708 # ASSIGN : s_3_7 755 # ASSIGN : s_3_8 803 # ASSIGN : s_3_9 914 # ASSIGN : s_4_0 25 # ASSIGN : s_4_1 45 # ASSIGN : s_4_2 218 # ASSIGN : s_4_3 308 # ASSIGN : s_4_4 375 # ASSIGN : s_4_5 439 # ASSIGN : s_4_6 582 # ASSIGN : s_4_7 700 # ASSIGN : s_4_8 810 # ASSIGN : s_4_9 894 # ASSIGN : s_5_0 22 # ASSIGN : s_5_1 228 # ASSIGN : s_5_2 321 # ASSIGN : s_5_3 378 # ASSIGN : s_5_4 448 # ASSIGN : s_5_5 554 # ASSIGN : s_5_6 612 # ASSIGN : s_5_7 719 # ASSIGN : s_5_8 748 # ASSIGN : s_5_9 930 # ASSIGN : s_6_0 170 # ASSIGN : s_6_1 271 # ASSIGN : s_6_2 366 # ASSIGN : s_6_3 507 # ASSIGN : s_6_4 533 # ASSIGN : s_6_5 639 # ASSIGN : s_6_6 712 # ASSIGN : s_6_7 783 # ASSIGN : s_6_8 853 # ASSIGN : s_6_9 1027 # ASSIGN : s_7_0 40 # ASSIGN : s_7_1 116 # ASSIGN : s_7_2 235 # ASSIGN : s_7_3 313 # ASSIGN : s_7_4 325 # ASSIGN : s_7_5 683 # ASSIGN : s_7_6 739 # ASSIGN : s_7_7 769 # ASSIGN : s_7_8 869 # ASSIGN : s_7_9 957 # ASSIGN : s_8_0 24 # ASSIGN : s_8_1 99 # ASSIGN : s_8_2 125 # ASSIGN : s_8_3 206 # ASSIGN : s_8_4 235 # ASSIGN : s_8_5 289 # ASSIGN : s_8_6 395 # ASSIGN : s_8_7 496 # ASSIGN : s_8_8 672 # ASSIGN : s_8_9 917 # ASSIGN : s_9_0 231 # ASSIGN : s_9_1 250 # ASSIGN : s_9_2 276 # ASSIGN : s_9_3 620 # ASSIGN : s_9_4 685 # ASSIGN : s_9_5 741 # ASSIGN : s_9_6 803 # ASSIGN : s_9_7 885 # ASSIGN : s_9_8 891 # ASSIGN : s_9_9 979 # ASSIGN : s_10_0 144 # ASSIGN : s_10_1 372 # ASSIGN : s_10_2 483 # ASSIGN : s_10_3 515 # ASSIGN : s_10_4 577 # ASSIGN : s_10_5 702 # ASSIGN : s_10_6 768 # ASSIGN : s_10_7 814 # ASSIGN : s_10_8 886 # ASSIGN : s_10_9 940 # ASSIGN : s_11_0 18 # ASSIGN : s_11_1 96 # ASSIGN : s_11_2 186 # ASSIGN : s_11_3 424 # ASSIGN : s_11_4 597 # ASSIGN : s_11_5 684 # ASSIGN : s_11_6 763 # ASSIGN : s_11_7 774 # ASSIGN : s_11_8 938 # ASSIGN : s_11_9 1026 # ASSIGN : s_12_0 57 # ASSIGN : s_12_1 85 # ASSIGN : s_12_2 226 # ASSIGN : s_12_3 371 # ASSIGN : s_12_4 471 # ASSIGN : s_12_5 584 # ASSIGN : s_12_6 615 # ASSIGN : s_12_7 702 # ASSIGN : s_12_8 930 # ASSIGN : s_12_9 998 # ASSIGN : s_13_0 4 # ASSIGN : s_13_1 76 # ASSIGN : s_13_2 115 # ASSIGN : s_13_3 173 # ASSIGN : s_13_4 283 # ASSIGN : s_13_5 386 # ASSIGN : s_13_6 505 # ASSIGN : s_13_7 574 # ASSIGN : s_13_8 661 # ASSIGN : s_13_9 793 # ASSIGN : s_14_0 1 # ASSIGN : s_14_1 19 # ASSIGN : s_14_2 112 # ASSIGN : s_14_3 171 # ASSIGN : s_14_4 465 # ASSIGN : s_14_5 534 # ASSIGN : s_14_6 642 # ASSIGN : s_14_7 750 # ASSIGN : s_14_8 890 # ASSIGN : s_14_9 969 SHOW_RESULT 1033 END : 1033 (0 seconds) [Thu Jun 1 16:52:27 2006] SHOW_RESULT 1033 CPU : 0.549999999999992 = 0.539999999999992 + 0.01 + 0 + 0 # BOUND : makespan 1032 1033 MODIFY_CNF 1032 BEGIN : [Thu Jun 1 16:52:27 2006] MODIFY_CNF 1032 END : 70616474 bytes (0 seconds) [Thu Jun 1 16:52:27 2006] MODIFY_CNF 1032 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1032 BEGIN : [Thu Jun 1 16:52:27 2006] CMD : minisat /work/tamura/csp2sat33598.cnf /work/tamura/csp2sat33598.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1321365 3888976 | 440455 0 0 NaNQ | 0.000 % | | 100 | 1321365 3888976 | 484500 100 1294 12.9 | 62.026 % | | 250 | 1321365 3888976 | 532950 250 3437 13.7 | 62.026 % | ==============================================================================) restarts : 3 conflicts : 460 (85 /sec) decisions : 1032 (191 /sec) propagations : 2964692 (547540 /sec) inspects : 31795326 (5872184 /sec) conflict literals : 8579 (11.47 % deleted) CPU time : 5.41457 s SATISFIABLE VERIFY_CNF 1032 END : (7 seconds) [Thu Jun 1 16:52:34 2006] VERIFY_CNF 1032 CPU : 6.50999999999999 = 0 + 0.00999999999999995 + 6.23999999999999 + 0.26 # RESULT : makespan 1032 SATISFIABLE SHOW_RESULT 1032 BEGIN : [Thu Jun 1 16:52:34 2006] # ASSIGN : makespan 1032 # ASSIGN : s_0_0 169 # ASSIGN : s_0_1 253 # ASSIGN : s_0_2 333 # ASSIGN : s_0_3 410 # ASSIGN : s_0_4 454 # ASSIGN : s_0_5 763 # ASSIGN : s_0_6 862 # ASSIGN : s_0_7 869 # ASSIGN : s_0_8 927 # ASSIGN : s_0_9 1023 # ASSIGN : s_1_0 0 # ASSIGN : s_1_1 26 # ASSIGN : s_1_2 113 # ASSIGN : s_1_3 128 # ASSIGN : s_1_4 211 # ASSIGN : s_1_5 295 # ASSIGN : s_1_6 380 # ASSIGN : s_1_7 411 # ASSIGN : s_1_8 468 # ASSIGN : s_1_9 541 # ASSIGN : s_2_0 75 # ASSIGN : s_2_1 182 # ASSIGN : s_2_2 258 # ASSIGN : s_2_3 322 # ASSIGN : s_2_4 404 # ASSIGN : s_2_5 474 # ASSIGN : s_2_6 551 # ASSIGN : s_2_7 576 # ASSIGN : s_2_8 656 # ASSIGN : s_2_9 766 # ASSIGN : s_3_0 8 # ASSIGN : s_3_1 83 # ASSIGN : s_3_2 107 # ASSIGN : s_3_3 114 # ASSIGN : s_3_4 401 # ASSIGN : s_3_5 412 # ASSIGN : s_3_6 494 # ASSIGN : s_3_7 640 # ASSIGN : s_3_8 675 # ASSIGN : s_3_9 792 # ASSIGN : s_4_0 85 # ASSIGN : s_4_1 200 # ASSIGN : s_4_2 233 # ASSIGN : s_4_3 313 # ASSIGN : s_4_4 433 # ASSIGN : s_4_5 704 # ASSIGN : s_4_6 802 # ASSIGN : s_4_7 817 # ASSIGN : s_4_8 867 # ASSIGN : s_4_9 942 # ASSIGN : s_5_0 21 # ASSIGN : s_5_1 350 # ASSIGN : s_5_2 449 # ASSIGN : s_5_3 506 # ASSIGN : s_5_4 605 # ASSIGN : s_5_5 682 # ASSIGN : s_5_6 740 # ASSIGN : s_5_7 798 # ASSIGN : s_5_8 827 # ASSIGN : s_5_9 951 # ASSIGN : s_6_0 31 # ASSIGN : s_6_1 115 # ASSIGN : s_6_2 210 # ASSIGN : s_6_3 266 # ASSIGN : s_6_4 292 # ASSIGN : s_6_5 386 # ASSIGN : s_6_6 604 # ASSIGN : s_6_7 722 # ASSIGN : s_6_8 852 # ASSIGN : s_6_9 1026 # ASSIGN : s_7_0 31 # ASSIGN : s_7_1 167 # ASSIGN : s_7_2 206 # ASSIGN : s_7_3 284 # ASSIGN : s_7_4 292 # ASSIGN : s_7_5 374 # ASSIGN : s_7_6 424 # ASSIGN : s_7_7 616 # ASSIGN : s_7_8 911 # ASSIGN : s_7_9 956 # ASSIGN : s_8_0 0 # ASSIGN : s_8_1 87 # ASSIGN : s_8_2 100 # ASSIGN : s_8_3 181 # ASSIGN : s_8_4 212 # ASSIGN : s_8_5 304 # ASSIGN : s_8_6 443 # ASSIGN : s_8_7 531 # ASSIGN : s_8_8 680 # ASSIGN : s_8_9 1019 # ASSIGN : s_9_0 191 # ASSIGN : s_9_1 258 # ASSIGN : s_9_2 474 # ASSIGN : s_9_3 552 # ASSIGN : s_9_4 628 # ASSIGN : s_9_5 683 # ASSIGN : s_9_6 735 # ASSIGN : s_9_7 821 # ASSIGN : s_9_8 834 # ASSIGN : s_9_9 978 # ASSIGN : s_10_0 119 # ASSIGN : s_10_1 515 # ASSIGN : s_10_2 586 # ASSIGN : s_10_3 618 # ASSIGN : s_10_4 680 # ASSIGN : s_10_5 749 # ASSIGN : s_10_6 815 # ASSIGN : s_10_7 850 # ASSIGN : s_10_8 922 # ASSIGN : s_10_9 939 # ASSIGN : s_11_0 5 # ASSIGN : s_11_1 105 # ASSIGN : s_11_2 229 # ASSIGN : s_11_3 314 # ASSIGN : s_11_4 541 # ASSIGN : s_11_5 700 # ASSIGN : s_11_6 810 # ASSIGN : s_11_7 855 # ASSIGN : s_11_8 937 # ASSIGN : s_11_9 1025 # ASSIGN : s_12_0 167 # ASSIGN : s_12_1 195 # ASSIGN : s_12_2 263 # ASSIGN : s_12_3 386 # ASSIGN : s_12_4 497 # ASSIGN : s_12_5 551 # ASSIGN : s_12_6 582 # ASSIGN : s_12_7 609 # ASSIGN : s_12_8 753 # ASSIGN : s_12_9 827 # ASSIGN : s_13_0 197 # ASSIGN : s_13_1 311 # ASSIGN : s_13_2 496 # ASSIGN : s_13_3 561 # ASSIGN : s_13_4 623 # ASSIGN : s_13_5 720 # ASSIGN : s_13_6 786 # ASSIGN : s_13_7 862 # ASSIGN : s_13_8 900 # ASSIGN : s_13_9 947 # ASSIGN : s_14_0 0 # ASSIGN : s_14_1 18 # ASSIGN : s_14_2 111 # ASSIGN : s_14_3 186 # ASSIGN : s_14_4 478 # ASSIGN : s_14_5 547 # ASSIGN : s_14_6 615 # ASSIGN : s_14_7 682 # ASSIGN : s_14_8 768 # ASSIGN : s_14_9 847 SHOW_RESULT 1032 END : 1032 (0 seconds) [Thu Jun 1 16:52:34 2006] SHOW_RESULT 1032 CPU : 0.530000000000001 = 0.530000000000001 + 0 + 0 + 0 # BOUND : makespan 1032 1032 MAIN END : (243 seconds) [Thu Jun 1 16:52:34 2006] MAIN CPU : 242.75 = 155.33 + 0.34 + 84.94 + 2.14