MAIN BEGIN : [Thu Jun 1 16:04:29 2006] READ BEGIN : csp/la20.csp [Thu Jun 1 16:04:29 2006] READ END : csp/la20.csp (1 seconds) [Thu Jun 1 16:04:30 2006] READ CPU : 1.38 = 1.38 + 0 + 0 + 0 # BOUND : makespan 756 1210 GENERATE_CNF 1210 BEGIN : [Thu Jun 1 16:04:30 2006] GENERATE_CNF 1210 END : 122656 variables 1272661 clauses 28522282 bytes (62 seconds) [Thu Jun 1 16:05:32 2006] GENERATE_CNF 1210 CPU : 61.33 = 61.25 + 0.08 + 0 + 0 MODIFY_CNF 983 BEGIN : [Thu Jun 1 16:05:32 2006] MODIFY_CNF 983 END : 28522288 bytes (0 seconds) [Thu Jun 1 16:05:32 2006] MODIFY_CNF 983 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 983 BEGIN : [Thu Jun 1 16:05:32 2006] CMD : minisat /work/tamura/csp2sat66112.cnf /work/tamura/csp2sat66112.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 549411 1603737 | 183137 0 0 NaNQ | 0.000 % | ==============================================================================) restarts : 1 conflicts : 74 (43 /sec) decisions : 259 (152 /sec) propagations : 486707 (285360 /sec) inspects : 3655220 (2143082 /sec) conflict literals : 1288 (9.17 % deleted) CPU time : 1.70559 s SATISFIABLE VERIFY_CNF 983 END : (2 seconds) [Thu Jun 1 16:05:34 2006] VERIFY_CNF 983 CPU : 2.09 = 0 + 0.01 + 2.05 + 0.03 # RESULT : makespan 983 SATISFIABLE SHOW_RESULT 983 BEGIN : [Thu Jun 1 16:05:34 2006] # ASSIGN : makespan 983 # ASSIGN : s_0_0 298 # ASSIGN : s_0_1 450 # ASSIGN : s_0_2 548 # ASSIGN : s_0_3 706 # ASSIGN : s_0_4 768 # ASSIGN : s_0_5 800 # ASSIGN : s_0_6 837 # ASSIGN : s_0_7 843 # ASSIGN : s_0_8 862 # ASSIGN : s_0_9 943 # ASSIGN : s_1_0 118 # ASSIGN : s_1_1 139 # ASSIGN : s_1_2 209 # ASSIGN : s_1_3 274 # ASSIGN : s_1_4 404 # ASSIGN : s_1_5 477 # ASSIGN : s_1_6 542 # ASSIGN : s_1_7 610 # ASSIGN : s_1_8 886 # ASSIGN : s_1_9 941 # ASSIGN : s_2_0 19 # ASSIGN : s_2_1 104 # ASSIGN : s_2_2 141 # ASSIGN : s_2_3 229 # ASSIGN : s_2_4 263 # ASSIGN : s_2_5 307 # ASSIGN : s_2_6 603 # ASSIGN : s_2_7 692 # ASSIGN : s_2_8 782 # ASSIGN : s_2_9 954 # ASSIGN : s_3_0 77 # ASSIGN : s_3_1 157 # ASSIGN : s_3_2 234 # ASSIGN : s_3_3 290 # ASSIGN : s_3_4 298 # ASSIGN : s_3_5 418 # ASSIGN : s_3_6 493 # ASSIGN : s_3_7 531 # ASSIGN : s_3_8 611 # ASSIGN : s_3_9 886 # ASSIGN : s_4_0 17 # ASSIGN : s_4_1 108 # ASSIGN : s_4_2 186 # ASSIGN : s_4_3 323 # ASSIGN : s_4_4 340 # ASSIGN : s_4_5 411 # ASSIGN : s_4_6 461 # ASSIGN : s_4_7 800 # ASSIGN : s_4_8 880 # ASSIGN : s_4_9 936 # ASSIGN : s_5_0 131 # ASSIGN : s_5_1 148 # ASSIGN : s_5_2 171 # ASSIGN : s_5_3 232 # ASSIGN : s_5_4 350 # ASSIGN : s_5_5 379 # ASSIGN : s_5_6 475 # ASSIGN : s_5_7 520 # ASSIGN : s_5_8 713 # ASSIGN : s_5_9 900 # ASSIGN : s_6_0 3 # ASSIGN : s_6_1 73 # ASSIGN : s_6_2 165 # ASSIGN : s_6_3 309 # ASSIGN : s_6_4 471 # ASSIGN : s_6_5 579 # ASSIGN : s_6_6 606 # ASSIGN : s_6_7 766 # ASSIGN : s_6_8 882 # ASSIGN : s_6_9 910 # ASSIGN : s_7_0 47 # ASSIGN : s_7_1 142 # ASSIGN : s_7_2 253 # ASSIGN : s_7_3 338 # ASSIGN : s_7_4 390 # ASSIGN : s_7_5 530 # ASSIGN : s_7_6 567 # ASSIGN : s_7_7 687 # ASSIGN : s_7_8 746 # ASSIGN : s_7_9 787 # ASSIGN : s_8_0 13 # ASSIGN : s_8_1 157 # ASSIGN : s_8_2 202 # ASSIGN : s_8_3 328 # ASSIGN : s_8_4 389 # ASSIGN : s_8_5 396 # ASSIGN : s_8_6 455 # ASSIGN : s_8_7 562 # ASSIGN : s_8_8 713 # ASSIGN : s_8_9 956 # ASSIGN : s_9_0 181 # ASSIGN : s_9_1 237 # ASSIGN : s_9_2 343 # ASSIGN : s_9_3 544 # ASSIGN : s_9_4 570 # ASSIGN : s_9_5 652 # ASSIGN : s_9_6 723 # ASSIGN : s_9_7 767 # ASSIGN : s_9_8 866 # ASSIGN : s_9_9 899 SHOW_RESULT 983 END : 983 (0 seconds) [Thu Jun 1 16:05:34 2006] SHOW_RESULT 983 CPU : 0.350000000000001 = 0.350000000000001 + 0 + 0 + 0 # BOUND : makespan 756 983 MODIFY_CNF 869 BEGIN : [Thu Jun 1 16:05:34 2006] MODIFY_CNF 869 END : 28522288 bytes (0 seconds) [Thu Jun 1 16:05:34 2006] MODIFY_CNF 869 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 869 BEGIN : [Thu Jun 1 16:05:34 2006] CMD : minisat /work/tamura/csp2sat66112.cnf /work/tamura/csp2sat66112.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 398106 1161509 | 132702 0 0 NaNQ | 0.000 % | ==============================================================================) restarts : 1 conflicts : 22 (13 /sec) decisions : 30 (17 /sec) propagations : 234119 (136458 /sec) inspects : 1263019 (736159 /sec) conflict literals : 62 (31.11 % deleted) CPU time : 1.71569 s UNSATISFIABLE VERIFY_CNF 869 END : (2 seconds) [Thu Jun 1 16:05:36 2006] VERIFY_CNF 869 CPU : 2.02 = 0 + 0.01 + 1.98 + 0.03 # RESULT : makespan 869 UNSATISFIABLE # BOUND : makespan 870 983 MODIFY_CNF 926 BEGIN : [Thu Jun 1 16:05:36 2006] MODIFY_CNF 926 END : 28522288 bytes (0 seconds) [Thu Jun 1 16:05:36 2006] MODIFY_CNF 926 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 926 BEGIN : [Thu Jun 1 16:05:36 2006] CMD : minisat /work/tamura/csp2sat66112.cnf /work/tamura/csp2sat66112.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 476550 1390950 | 158850 0 0 NaNQ | 0.000 % | ==============================================================================) restarts : 1 conflicts : 52 (30 /sec) decisions : 223 (129 /sec) propagations : 381047 (220254 /sec) inspects : 2583275 (1493191 /sec) conflict literals : 443 (11.93 % deleted) CPU time : 1.73004 s SATISFIABLE VERIFY_CNF 926 END : (2 seconds) [Thu Jun 1 16:05:38 2006] VERIFY_CNF 926 CPU : 2.09 = 0 + 0 + 2.05 + 0.04 # RESULT : makespan 926 SATISFIABLE SHOW_RESULT 926 BEGIN : [Thu Jun 1 16:05:38 2006] # ASSIGN : makespan 926 # ASSIGN : s_0_0 24 # ASSIGN : s_0_1 33 # ASSIGN : s_0_2 164 # ASSIGN : s_0_3 270 # ASSIGN : s_0_4 310 # ASSIGN : s_0_5 342 # ASSIGN : s_0_6 449 # ASSIGN : s_0_7 497 # ASSIGN : s_0_8 516 # ASSIGN : s_0_9 635 # ASSIGN : s_1_0 63 # ASSIGN : s_1_1 84 # ASSIGN : s_1_2 154 # ASSIGN : s_1_3 219 # ASSIGN : s_1_4 518 # ASSIGN : s_1_5 612 # ASSIGN : s_1_6 677 # ASSIGN : s_1_7 748 # ASSIGN : s_1_8 829 # ASSIGN : s_1_9 884 # ASSIGN : s_2_0 375 # ASSIGN : s_2_1 460 # ASSIGN : s_2_2 500 # ASSIGN : s_2_3 540 # ASSIGN : s_2_4 564 # ASSIGN : s_2_5 610 # ASSIGN : s_2_6 693 # ASSIGN : s_2_7 782 # ASSIGN : s_2_8 813 # ASSIGN : s_2_9 897 # ASSIGN : s_3_0 74 # ASSIGN : s_3_1 154 # ASSIGN : s_3_2 231 # ASSIGN : s_3_3 337 # ASSIGN : s_3_4 345 # ASSIGN : s_3_5 401 # ASSIGN : s_3_6 502 # ASSIGN : s_3_7 608 # ASSIGN : s_3_8 688 # ASSIGN : s_3_9 829 # ASSIGN : s_4_0 204 # ASSIGN : s_4_1 295 # ASSIGN : s_4_2 376 # ASSIGN : s_4_3 491 # ASSIGN : s_4_4 508 # ASSIGN : s_4_5 579 # ASSIGN : s_4_6 629 # ASSIGN : s_4_7 702 # ASSIGN : s_4_8 814 # ASSIGN : s_4_9 919 # ASSIGN : s_5_0 15 # ASSIGN : s_5_1 57 # ASSIGN : s_5_2 66 # ASSIGN : s_5_3 184 # ASSIGN : s_5_4 330 # ASSIGN : s_5_5 359 # ASSIGN : s_5_6 455 # ASSIGN : s_5_7 506 # ASSIGN : s_5_8 540 # ASSIGN : s_5_9 675 # ASSIGN : s_6_0 4 # ASSIGN : s_6_1 124 # ASSIGN : s_6_2 216 # ASSIGN : s_6_3 314 # ASSIGN : s_6_4 417 # ASSIGN : s_6_5 525 # ASSIGN : s_6_6 552 # ASSIGN : s_6_7 729 # ASSIGN : s_6_8 825 # ASSIGN : s_6_9 853 # ASSIGN : s_7_0 114 # ASSIGN : s_7_1 287 # ASSIGN : s_7_2 379 # ASSIGN : s_7_3 464 # ASSIGN : s_7_4 516 # ASSIGN : s_7_5 597 # ASSIGN : s_7_6 638 # ASSIGN : s_7_7 689 # ASSIGN : s_7_8 812 # ASSIGN : s_7_9 870 # ASSIGN : s_8_0 4 # ASSIGN : s_8_1 64 # ASSIGN : s_8_2 109 # ASSIGN : s_8_3 197 # ASSIGN : s_8_4 209 # ASSIGN : s_8_5 261 # ASSIGN : s_8_6 283 # ASSIGN : s_8_7 386 # ASSIGN : s_8_8 711 # ASSIGN : s_8_9 899 # ASSIGN : s_9_0 2 # ASSIGN : s_9_1 23 # ASSIGN : s_9_2 220 # ASSIGN : s_9_3 288 # ASSIGN : s_9_4 335 # ASSIGN : s_9_5 435 # ASSIGN : s_9_6 508 # ASSIGN : s_9_7 594 # ASSIGN : s_9_8 780 # ASSIGN : s_9_9 842 SHOW_RESULT 926 END : 926 (1 seconds) [Thu Jun 1 16:05:39 2006] SHOW_RESULT 926 CPU : 0.340000000000003 = 0.340000000000003 + 0 + 0 + 0 # BOUND : makespan 870 926 MODIFY_CNF 898 BEGIN : [Thu Jun 1 16:05:39 2006] MODIFY_CNF 898 END : 28522288 bytes (0 seconds) [Thu Jun 1 16:05:39 2006] MODIFY_CNF 898 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 898 BEGIN : [Thu Jun 1 16:05:39 2006] CMD : minisat /work/tamura/csp2sat66112.cnf /work/tamura/csp2sat66112.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 439750 1283403 | 146583 0 0 NaNQ | 0.000 % | | 100 | 439750 1283403 | 161241 99 885 8.9 | 70.491 % | ==============================================================================) restarts : 2 conflicts : 241 (107 /sec) decisions : 338 (150 /sec) propagations : 1644666 (728163 /sec) inspects : 10465955 (4633719 /sec) conflict literals : 2004 (33.44 % deleted) CPU time : 2.25865 s UNSATISFIABLE VERIFY_CNF 898 END : (2 seconds) [Thu Jun 1 16:05:41 2006] VERIFY_CNF 898 CPU : 2.57 = 0.00999999999999801 + 0.01 + 2.52 + 0.03 # RESULT : makespan 898 UNSATISFIABLE # BOUND : makespan 899 926 MODIFY_CNF 912 BEGIN : [Thu Jun 1 16:05:41 2006] MODIFY_CNF 912 END : 28522288 bytes (0 seconds) [Thu Jun 1 16:05:41 2006] MODIFY_CNF 912 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 912 BEGIN : [Thu Jun 1 16:05:41 2006] CMD : minisat /work/tamura/csp2sat66112.cnf /work/tamura/csp2sat66112.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 459157 1340195 | 153052 0 0 NaNQ | 0.000 % | ==============================================================================) restarts : 1 conflicts : 68 (38 /sec) decisions : 229 (127 /sec) propagations : 587381 (325085 /sec) inspects : 3816635 (2112312 /sec) conflict literals : 593 (26.70 % deleted) CPU time : 1.80685 s SATISFIABLE VERIFY_CNF 912 END : (3 seconds) [Thu Jun 1 16:05:44 2006] VERIFY_CNF 912 CPU : 2.25 = 0 + 0.01 + 2.12 + 0.12 # RESULT : makespan 912 SATISFIABLE SHOW_RESULT 912 BEGIN : [Thu Jun 1 16:05:44 2006] # ASSIGN : makespan 912 # ASSIGN : s_0_0 30 # ASSIGN : s_0_1 39 # ASSIGN : s_0_2 150 # ASSIGN : s_0_3 314 # ASSIGN : s_0_4 354 # ASSIGN : s_0_5 411 # ASSIGN : s_0_6 448 # ASSIGN : s_0_7 454 # ASSIGN : s_0_8 496 # ASSIGN : s_0_9 621 # ASSIGN : s_1_0 49 # ASSIGN : s_1_1 70 # ASSIGN : s_1_2 140 # ASSIGN : s_1_3 205 # ASSIGN : s_1_4 427 # ASSIGN : s_1_5 473 # ASSIGN : s_1_6 538 # ASSIGN : s_1_7 662 # ASSIGN : s_1_8 815 # ASSIGN : s_1_9 870 # ASSIGN : s_2_0 229 # ASSIGN : s_2_1 417 # ASSIGN : s_2_2 488 # ASSIGN : s_2_3 528 # ASSIGN : s_2_4 552 # ASSIGN : s_2_5 596 # ASSIGN : s_2_6 679 # ASSIGN : s_2_7 768 # ASSIGN : s_2_8 799 # ASSIGN : s_2_9 883 # ASSIGN : s_3_0 70 # ASSIGN : s_3_1 208 # ASSIGN : s_3_2 404 # ASSIGN : s_3_3 460 # ASSIGN : s_3_4 468 # ASSIGN : s_3_5 597 # ASSIGN : s_3_6 656 # ASSIGN : s_3_7 694 # ASSIGN : s_3_8 774 # ASSIGN : s_3_9 815 # ASSIGN : s_4_0 3 # ASSIGN : s_4_1 285 # ASSIGN : s_4_2 366 # ASSIGN : s_4_3 481 # ASSIGN : s_4_4 498 # ASSIGN : s_4_5 569 # ASSIGN : s_4_6 619 # ASSIGN : s_4_7 688 # ASSIGN : s_4_8 800 # ASSIGN : s_4_9 905 # ASSIGN : s_5_0 13 # ASSIGN : s_5_1 21 # ASSIGN : s_5_2 72 # ASSIGN : s_5_3 170 # ASSIGN : s_5_4 357 # ASSIGN : s_5_5 386 # ASSIGN : s_5_6 532 # ASSIGN : s_5_7 577 # ASSIGN : s_5_8 625 # ASSIGN : s_5_9 730 # ASSIGN : s_6_0 0 # ASSIGN : s_6_1 130 # ASSIGN : s_6_2 222 # ASSIGN : s_6_3 320 # ASSIGN : s_6_4 407 # ASSIGN : s_6_5 536 # ASSIGN : s_6_6 563 # ASSIGN : s_6_7 678 # ASSIGN : s_6_8 811 # ASSIGN : s_6_9 839 # ASSIGN : s_7_0 120 # ASSIGN : s_7_1 234 # ASSIGN : s_7_2 326 # ASSIGN : s_7_3 454 # ASSIGN : s_7_4 506 # ASSIGN : s_7_5 587 # ASSIGN : s_7_6 649 # ASSIGN : s_7_7 739 # ASSIGN : s_7_8 798 # ASSIGN : s_7_9 856 # ASSIGN : s_8_0 10 # ASSIGN : s_8_1 70 # ASSIGN : s_8_2 115 # ASSIGN : s_8_3 203 # ASSIGN : s_8_4 215 # ASSIGN : s_8_5 247 # ASSIGN : s_8_6 269 # ASSIGN : s_8_7 362 # ASSIGN : s_8_8 661 # ASSIGN : s_8_9 885 # ASSIGN : s_9_0 94 # ASSIGN : s_9_1 142 # ASSIGN : s_9_2 226 # ASSIGN : s_9_3 294 # ASSIGN : s_9_4 325 # ASSIGN : s_9_5 411 # ASSIGN : s_9_6 482 # ASSIGN : s_9_7 526 # ASSIGN : s_9_8 766 # ASSIGN : s_9_9 828 SHOW_RESULT 912 END : 912 (0 seconds) [Thu Jun 1 16:05:44 2006] SHOW_RESULT 912 CPU : 0.359999999999999 = 0.359999999999999 + 0 + 0 + 0 # BOUND : makespan 899 912 MODIFY_CNF 905 BEGIN : [Thu Jun 1 16:05:44 2006] MODIFY_CNF 905 END : 28522288 bytes (0 seconds) [Thu Jun 1 16:05:44 2006] MODIFY_CNF 905 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 905 BEGIN : [Thu Jun 1 16:05:44 2006] CMD : minisat /work/tamura/csp2sat66112.cnf /work/tamura/csp2sat66112.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 450969 1316343 | 150323 0 0 NaNQ | 0.000 % | | 100 | 450969 1316343 | 165355 97 643 6.6 | 71.008 % | ==============================================================================) restarts : 2 conflicts : 161 (79 /sec) decisions : 354 (174 /sec) propagations : 1200119 (590203 /sec) inspects : 7641747 (3758111 /sec) conflict literals : 1042 (36.66 % deleted) CPU time : 2.0334 s SATISFIABLE VERIFY_CNF 905 END : (2 seconds) [Thu Jun 1 16:05:46 2006] VERIFY_CNF 905 CPU : 2.39 = 0 + 0 + 2.35 + 0.04 # RESULT : makespan 905 SATISFIABLE SHOW_RESULT 905 BEGIN : [Thu Jun 1 16:05:46 2006] # ASSIGN : makespan 905 # ASSIGN : s_0_0 0 # ASSIGN : s_0_1 14 # ASSIGN : s_0_2 172 # ASSIGN : s_0_3 227 # ASSIGN : s_0_4 267 # ASSIGN : s_0_5 299 # ASSIGN : s_0_6 338 # ASSIGN : s_0_7 395 # ASSIGN : s_0_8 415 # ASSIGN : s_0_9 738 # ASSIGN : s_1_0 136 # ASSIGN : s_1_1 157 # ASSIGN : s_1_2 279 # ASSIGN : s_1_3 357 # ASSIGN : s_1_4 476 # ASSIGN : s_1_5 522 # ASSIGN : s_1_6 588 # ASSIGN : s_1_7 655 # ASSIGN : s_1_8 808 # ASSIGN : s_1_9 863 # ASSIGN : s_2_0 276 # ASSIGN : s_2_1 414 # ASSIGN : s_2_2 474 # ASSIGN : s_2_3 514 # ASSIGN : s_2_4 538 # ASSIGN : s_2_5 582 # ASSIGN : s_2_6 665 # ASSIGN : s_2_7 754 # ASSIGN : s_2_8 785 # ASSIGN : s_2_9 876 # ASSIGN : s_3_0 92 # ASSIGN : s_3_1 185 # ASSIGN : s_3_2 419 # ASSIGN : s_3_3 549 # ASSIGN : s_3_4 557 # ASSIGN : s_3_5 587 # ASSIGN : s_3_6 646 # ASSIGN : s_3_7 684 # ASSIGN : s_3_8 764 # ASSIGN : s_3_9 808 # ASSIGN : s_4_0 54 # ASSIGN : s_4_1 145 # ASSIGN : s_4_2 256 # ASSIGN : s_4_3 344 # ASSIGN : s_4_4 361 # ASSIGN : s_4_5 446 # ASSIGN : s_4_6 496 # ASSIGN : s_4_7 613 # ASSIGN : s_4_8 722 # ASSIGN : s_4_9 778 # ASSIGN : s_5_0 1 # ASSIGN : s_5_1 9 # ASSIGN : s_5_2 18 # ASSIGN : s_5_3 159 # ASSIGN : s_5_4 315 # ASSIGN : s_5_5 362 # ASSIGN : s_5_6 610 # ASSIGN : s_5_7 805 # ASSIGN : s_5_8 815 # ASSIGN : s_5_9 869 # ASSIGN : s_6_0 6 # ASSIGN : s_6_1 76 # ASSIGN : s_6_2 190 # ASSIGN : s_6_3 288 # ASSIGN : s_6_4 375 # ASSIGN : s_6_5 475 # ASSIGN : s_6_6 502 # ASSIGN : s_6_7 668 # ASSIGN : s_6_8 804 # ASSIGN : s_6_9 832 # ASSIGN : s_7_0 95 # ASSIGN : s_7_1 244 # ASSIGN : s_7_2 336 # ASSIGN : s_7_3 421 # ASSIGN : s_7_4 474 # ASSIGN : s_7_5 555 # ASSIGN : s_7_6 693 # ASSIGN : s_7_7 732 # ASSIGN : s_7_8 791 # ASSIGN : s_7_9 849 # ASSIGN : s_8_0 239 # ASSIGN : s_8_1 299 # ASSIGN : s_8_2 344 # ASSIGN : s_8_3 432 # ASSIGN : s_8_4 444 # ASSIGN : s_8_5 451 # ASSIGN : s_8_6 473 # ASSIGN : s_8_7 587 # ASSIGN : s_8_8 636 # ASSIGN : s_8_9 878 # ASSIGN : s_9_0 33 # ASSIGN : s_9_1 96 # ASSIGN : s_9_2 168 # ASSIGN : s_9_3 236 # ASSIGN : s_9_4 262 # ASSIGN : s_9_5 344 # ASSIGN : s_9_6 458 # ASSIGN : s_9_7 566 # ASSIGN : s_9_8 705 # ASSIGN : s_9_9 821 SHOW_RESULT 905 END : 905 (1 seconds) [Thu Jun 1 16:05:47 2006] SHOW_RESULT 905 CPU : 0.359999999999994 = 0.349999999999994 + 0.01 + 0 + 0 # BOUND : makespan 899 905 MODIFY_CNF 902 BEGIN : [Thu Jun 1 16:05:47 2006] MODIFY_CNF 902 END : 28522288 bytes (0 seconds) [Thu Jun 1 16:05:47 2006] MODIFY_CNF 902 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 902 BEGIN : [Thu Jun 1 16:05:47 2006] CMD : minisat /work/tamura/csp2sat66112.cnf /work/tamura/csp2sat66112.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 446604 1303555 | 148868 0 0 NaNQ | 0.000 % | | 100 | 446604 1303555 | 163754 98 592 6.0 | 70.566 % | | 251 | 446604 1303555 | 180130 249 2292 9.2 | 70.566 % | ==============================================================================) restarts : 3 conflicts : 287 (122 /sec) decisions : 586 (248 /sec) propagations : 2033592 (861312 /sec) inspects : 13211464 (5595614 /sec) conflict literals : 2616 (30.67 % deleted) CPU time : 2.36104 s SATISFIABLE VERIFY_CNF 902 END : (3 seconds) [Thu Jun 1 16:05:50 2006] VERIFY_CNF 902 CPU : 2.70000000000001 = 0.0100000000000051 + 0 + 2.66 + 0.03 # RESULT : makespan 902 SATISFIABLE SHOW_RESULT 902 BEGIN : [Thu Jun 1 16:05:50 2006] # ASSIGN : makespan 902 # ASSIGN : s_0_0 0 # ASSIGN : s_0_1 12 # ASSIGN : s_0_2 160 # ASSIGN : s_0_3 224 # ASSIGN : s_0_4 264 # ASSIGN : s_0_5 441 # ASSIGN : s_0_6 478 # ASSIGN : s_0_7 484 # ASSIGN : s_0_8 503 # ASSIGN : s_0_9 633 # ASSIGN : s_1_0 133 # ASSIGN : s_1_1 154 # ASSIGN : s_1_2 289 # ASSIGN : s_1_3 354 # ASSIGN : s_1_4 473 # ASSIGN : s_1_5 519 # ASSIGN : s_1_6 585 # ASSIGN : s_1_7 652 # ASSIGN : s_1_8 805 # ASSIGN : s_1_9 860 # ASSIGN : s_2_0 8 # ASSIGN : s_2_1 146 # ASSIGN : s_2_2 438 # ASSIGN : s_2_3 511 # ASSIGN : s_2_4 535 # ASSIGN : s_2_5 579 # ASSIGN : s_2_6 662 # ASSIGN : s_2_7 751 # ASSIGN : s_2_8 782 # ASSIGN : s_2_9 873 # ASSIGN : s_3_0 80 # ASSIGN : s_3_1 214 # ASSIGN : s_3_2 416 # ASSIGN : s_3_3 546 # ASSIGN : s_3_4 554 # ASSIGN : s_3_5 584 # ASSIGN : s_3_6 643 # ASSIGN : s_3_7 681 # ASSIGN : s_3_8 761 # ASSIGN : s_3_9 805 # ASSIGN : s_4_0 83 # ASSIGN : s_4_1 174 # ASSIGN : s_4_2 215 # ASSIGN : s_4_3 303 # ASSIGN : s_4_4 320 # ASSIGN : s_4_5 391 # ASSIGN : s_4_6 444 # ASSIGN : s_4_7 610 # ASSIGN : s_4_8 719 # ASSIGN : s_4_9 775 # ASSIGN : s_5_0 0 # ASSIGN : s_5_1 9 # ASSIGN : s_5_2 18 # ASSIGN : s_5_3 183 # ASSIGN : s_5_4 330 # ASSIGN : s_5_5 359 # ASSIGN : s_5_6 607 # ASSIGN : s_5_7 802 # ASSIGN : s_5_8 812 # ASSIGN : s_5_9 866 # ASSIGN : s_6_0 6 # ASSIGN : s_6_1 76 # ASSIGN : s_6_2 188 # ASSIGN : s_6_3 286 # ASSIGN : s_6_4 373 # ASSIGN : s_6_5 472 # ASSIGN : s_6_6 499 # ASSIGN : s_6_7 665 # ASSIGN : s_6_8 801 # ASSIGN : s_6_9 829 # ASSIGN : s_7_0 93 # ASSIGN : s_7_1 214 # ASSIGN : s_7_2 306 # ASSIGN : s_7_3 418 # ASSIGN : s_7_4 498 # ASSIGN : s_7_5 584 # ASSIGN : s_7_6 690 # ASSIGN : s_7_7 729 # ASSIGN : s_7_8 788 # ASSIGN : s_7_9 846 # ASSIGN : s_8_0 236 # ASSIGN : s_8_1 296 # ASSIGN : s_8_2 341 # ASSIGN : s_8_3 429 # ASSIGN : s_8_4 441 # ASSIGN : s_8_5 448 # ASSIGN : s_8_6 470 # ASSIGN : s_8_7 616 # ASSIGN : s_8_8 706 # ASSIGN : s_8_9 875 # ASSIGN : s_9_0 62 # ASSIGN : s_9_1 93 # ASSIGN : s_9_2 168 # ASSIGN : s_9_3 260 # ASSIGN : s_9_4 291 # ASSIGN : s_9_5 373 # ASSIGN : s_9_6 455 # ASSIGN : s_9_7 563 # ASSIGN : s_9_8 673 # ASSIGN : s_9_9 818 SHOW_RESULT 902 END : 902 (0 seconds) [Thu Jun 1 16:05:50 2006] SHOW_RESULT 902 CPU : 0.340000000000003 = 0.340000000000003 + 0 + 0 + 0 # BOUND : makespan 899 902 MODIFY_CNF 900 BEGIN : [Thu Jun 1 16:05:50 2006] MODIFY_CNF 900 END : 28522288 bytes (0 seconds) [Thu Jun 1 16:05:50 2006] MODIFY_CNF 900 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 900 BEGIN : [Thu Jun 1 16:05:50 2006] CMD : minisat /work/tamura/csp2sat66112.cnf /work/tamura/csp2sat66112.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 443570 1294658 | 147856 0 0 NaNQ | 0.000 % | | 102 | 443570 1294658 | 162641 100 747 7.5 | 70.733 % | | 252 | 406958 1186934 | 178905 148 1176 7.9 | 74.226 % | ==============================================================================) restarts : 3 conflicts : 264 (115 /sec) decisions : 395 (173 /sec) propagations : 1789791 (782769 /sec) inspects : 11543466 (5048560 /sec) conflict literals : 2159 (39.99 % deleted) CPU time : 2.28649 s UNSATISFIABLE VERIFY_CNF 900 END : (3 seconds) [Thu Jun 1 16:05:53 2006] VERIFY_CNF 900 CPU : 2.68000000000001 = 0.0100000000000051 + 0.00999999999999998 + 2.55 + 0.11 # RESULT : makespan 900 UNSATISFIABLE # BOUND : makespan 901 902 MODIFY_CNF 901 BEGIN : [Thu Jun 1 16:05:53 2006] MODIFY_CNF 901 END : 28522288 bytes (0 seconds) [Thu Jun 1 16:05:53 2006] MODIFY_CNF 901 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 901 BEGIN : [Thu Jun 1 16:05:53 2006] CMD : minisat /work/tamura/csp2sat66112.cnf /work/tamura/csp2sat66112.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 445037 1298956 | 148345 0 0 NaNQ | 0.000 % | | 101 | 445037 1298956 | 163179 100 793 7.9 | 70.238 % | | 251 | 445037 1298956 | 179497 247 2389 9.7 | 71.984 % | ==============================================================================) restarts : 3 conflicts : 279 (117 /sec) decisions : 392 (164 /sec) propagations : 1949771 (817570 /sec) inspects : 12593029 (5280459 /sec) conflict literals : 2515 (33.62 % deleted) CPU time : 2.38484 s UNSATISFIABLE VERIFY_CNF 901 END : (2 seconds) [Thu Jun 1 16:05:55 2006] VERIFY_CNF 901 CPU : 2.78 = 0 + 0.01 + 2.65 + 0.12 # RESULT : makespan 901 UNSATISFIABLE # BOUND : makespan 902 902 MAIN END : (86 seconds) [Thu Jun 1 16:05:55 2006] MAIN CPU : 86.03 = 64.4 + 0.15 + 20.93 + 0.55