MAIN BEGIN : [Thu Jun 1 14:12:09 2006] READ BEGIN : csp/la06.csp [Thu Jun 1 14:12:09 2006] READ END : csp/la06.csp (2 seconds) [Thu Jun 1 14:12:11 2006] READ CPU : 1.49 = 1.49 + 0 + 0 + 0 # BOUND : makespan 926 1078 GENERATE_CNF 1078 BEGIN : [Thu Jun 1 14:12:11 2006] GENERATE_CNF 1078 END : 82279 variables 1223769 clauses 26018469 bytes (60 seconds) [Thu Jun 1 14:13:11 2006] GENERATE_CNF 1078 CPU : 59.72 = 59.65 + 0.07 + 0 + 0 MODIFY_CNF 1002 BEGIN : [Thu Jun 1 14:13:11 2006] MODIFY_CNF 1002 END : 26018474 bytes (0 seconds) [Thu Jun 1 14:13:11 2006] MODIFY_CNF 1002 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1002 BEGIN : [Thu Jun 1 14:13:11 2006] CMD : minisat /work/tamura/csp2sat66598.cnf /work/tamura/csp2sat66598.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 933560 2744629 | 311186 0 0 NaNQ | 0.000 % | ==============================================================================) restarts : 1 conflicts : 16 (15 /sec) decisions : 193 (177 /sec) propagations : 122054 (111951 /sec) inspects : 1301855 (1194095 /sec) conflict literals : 176 (12.00 % deleted) CPU time : 1.09024 s SATISFIABLE VERIFY_CNF 1002 END : (1 seconds) [Thu Jun 1 14:13:12 2006] VERIFY_CNF 1002 CPU : 1.57 = 0.00999999999999801 + 0.01 + 1.53 + 0.02 # RESULT : makespan 1002 SATISFIABLE SHOW_RESULT 1002 BEGIN : [Thu Jun 1 14:13:12 2006] # ASSIGN : makespan 1002 # ASSIGN : s_0_0 31 # ASSIGN : s_0_1 54 # ASSIGN : s_0_2 88 # ASSIGN : s_0_3 219 # ASSIGN : s_0_4 392 # ASSIGN : s_1_0 289 # ASSIGN : s_1_1 341 # ASSIGN : s_1_2 548 # ASSIGN : s_1_3 702 # ASSIGN : s_1_4 935 # ASSIGN : s_2_0 241 # ASSIGN : s_2_1 272 # ASSIGN : s_2_2 422 # ASSIGN : s_2_3 464 # ASSIGN : s_2_4 904 # ASSIGN : s_3_0 29 # ASSIGN : s_3_1 106 # ASSIGN : s_3_2 183 # ASSIGN : s_3_3 344 # ASSIGN : s_3_4 601 # ASSIGN : s_4_0 51 # ASSIGN : s_4_1 503 # ASSIGN : s_4_2 537 # ASSIGN : s_4_3 619 # ASSIGN : s_4_4 814 # ASSIGN : s_5_0 9 # ASSIGN : s_5_1 52 # ASSIGN : s_5_2 108 # ASSIGN : s_5_3 200 # ASSIGN : s_5_4 262 # ASSIGN : s_6_0 15 # ASSIGN : s_6_1 131 # ASSIGN : s_6_2 268 # ASSIGN : s_6_3 357 # ASSIGN : s_6_4 450 # ASSIGN : s_7_0 284 # ASSIGN : s_7_1 355 # ASSIGN : s_7_2 396 # ASSIGN : s_7_3 434 # ASSIGN : s_7_4 776 # ASSIGN : s_8_0 298 # ASSIGN : s_8_1 447 # ASSIGN : s_8_2 517 # ASSIGN : s_8_3 556 # ASSIGN : s_8_4 638 # ASSIGN : s_9_0 399 # ASSIGN : s_9_1 542 # ASSIGN : s_9_2 637 # ASSIGN : s_9_3 884 # ASSIGN : s_9_4 959 # ASSIGN : s_10_0 619 # ASSIGN : s_10_1 667 # ASSIGN : s_10_2 705 # ASSIGN : s_10_3 800 # ASSIGN : s_10_4 995 # ASSIGN : s_11_0 495 # ASSIGN : s_11_1 647 # ASSIGN : s_11_2 728 # ASSIGN : s_11_3 823 # ASSIGN : s_11_4 917 # ASSIGN : s_12_0 657 # ASSIGN : s_12_1 716 # ASSIGN : s_12_2 732 # ASSIGN : s_12_3 866 # ASSIGN : s_12_4 956 # ASSIGN : s_13_0 789 # ASSIGN : s_13_1 832 # ASSIGN : s_13_2 897 # ASSIGN : s_13_3 925 # ASSIGN : s_13_4 952 # ASSIGN : s_14_0 600 # ASSIGN : s_14_1 687 # ASSIGN : s_14_2 827 # ASSIGN : s_14_3 867 # ASSIGN : s_14_4 876 SHOW_RESULT 1002 END : 1002 (1 seconds) [Thu Jun 1 14:13:13 2006] SHOW_RESULT 1002 CPU : 0.219999999999999 = 0.219999999999999 + 0 + 0 + 0 # BOUND : makespan 926 1002 MODIFY_CNF 964 BEGIN : [Thu Jun 1 14:13:13 2006] MODIFY_CNF 964 END : 26018474 bytes (0 seconds) [Thu Jun 1 14:13:13 2006] MODIFY_CNF 964 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 964 BEGIN : [Thu Jun 1 14:13:13 2006] CMD : minisat /work/tamura/csp2sat66598.cnf /work/tamura/csp2sat66598.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 890772 2619153 | 296924 0 0 NaNQ | 0.000 % | ==============================================================================) restarts : 1 conflicts : 4 (4 /sec) decisions : 171 (153 /sec) propagations : 101096 (90666 /sec) inspects : 968313 (868413 /sec) conflict literals : 26 (7.14 % deleted) CPU time : 1.11504 s SATISFIABLE VERIFY_CNF 964 END : (1 seconds) [Thu Jun 1 14:13:14 2006] VERIFY_CNF 964 CPU : 1.6 = 0.00999999999999801 + 0.01 + 1.55 + 0.03 # RESULT : makespan 964 SATISFIABLE SHOW_RESULT 964 BEGIN : [Thu Jun 1 14:13:14 2006] # ASSIGN : makespan 964 # ASSIGN : s_0_0 11 # ASSIGN : s_0_1 32 # ASSIGN : s_0_2 73 # ASSIGN : s_0_3 169 # ASSIGN : s_0_4 274 # ASSIGN : s_1_0 90 # ASSIGN : s_1_1 168 # ASSIGN : s_1_2 384 # ASSIGN : s_1_3 455 # ASSIGN : s_1_4 814 # ASSIGN : s_2_0 66 # ASSIGN : s_2_1 97 # ASSIGN : s_2_2 342 # ASSIGN : s_2_3 391 # ASSIGN : s_2_4 702 # ASSIGN : s_3_0 3 # ASSIGN : s_3_1 80 # ASSIGN : s_3_2 184 # ASSIGN : s_3_3 314 # ASSIGN : s_3_4 389 # ASSIGN : s_4_0 263 # ASSIGN : s_4_1 447 # ASSIGN : s_4_2 481 # ASSIGN : s_4_3 589 # ASSIGN : s_4_4 835 # ASSIGN : s_5_0 114 # ASSIGN : s_5_1 157 # ASSIGN : s_5_2 222 # ASSIGN : s_5_3 329 # ASSIGN : s_5_4 800 # ASSIGN : s_6_0 4 # ASSIGN : s_6_1 142 # ASSIGN : s_6_2 211 # ASSIGN : s_6_3 300 # ASSIGN : s_6_4 545 # ASSIGN : s_7_0 109 # ASSIGN : s_7_1 298 # ASSIGN : s_7_2 339 # ASSIGN : s_7_3 377 # ASSIGN : s_7_4 635 # ASSIGN : s_8_0 241 # ASSIGN : s_8_1 430 # ASSIGN : s_8_2 460 # ASSIGN : s_8_3 526 # ASSIGN : s_8_4 608 # ASSIGN : s_9_0 369 # ASSIGN : s_9_1 485 # ASSIGN : s_9_2 659 # ASSIGN : s_9_3 845 # ASSIGN : s_9_4 921 # ASSIGN : s_10_0 562 # ASSIGN : s_10_1 632 # ASSIGN : s_10_2 667 # ASSIGN : s_10_3 762 # ASSIGN : s_10_4 957 # ASSIGN : s_11_0 465 # ASSIGN : s_11_1 590 # ASSIGN : s_11_2 698 # ASSIGN : s_11_3 920 # ASSIGN : s_11_4 929 # ASSIGN : s_12_0 600 # ASSIGN : s_12_1 738 # ASSIGN : s_12_2 754 # ASSIGN : s_12_3 859 # ASSIGN : s_12_4 918 # ASSIGN : s_13_0 659 # ASSIGN : s_13_1 702 # ASSIGN : s_13_2 765 # ASSIGN : s_13_3 793 # ASSIGN : s_13_4 838 # ASSIGN : s_14_0 570 # ASSIGN : s_14_1 657 # ASSIGN : s_14_2 820 # ASSIGN : s_14_3 879 # ASSIGN : s_14_4 888 SHOW_RESULT 964 END : 964 (0 seconds) [Thu Jun 1 14:13:14 2006] SHOW_RESULT 964 CPU : 0.230000000000004 = 0.230000000000004 + 0 + 0 + 0 # BOUND : makespan 926 964 MODIFY_CNF 945 BEGIN : [Thu Jun 1 14:13:14 2006] MODIFY_CNF 945 END : 26018474 bytes (0 seconds) [Thu Jun 1 14:13:14 2006] MODIFY_CNF 945 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 945 BEGIN : [Thu Jun 1 14:13:14 2006] CMD : minisat /work/tamura/csp2sat66598.cnf /work/tamura/csp2sat66598.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 869378 2556415 | 289792 0 0 NaNQ | 0.000 % | | 100 | 869378 2556415 | 318771 100 1008 10.1 | 36.820 % | ==============================================================================) restarts : 2 conflicts : 115 (86 /sec) decisions : 434 (325 /sec) propagations : 449473 (336505 /sec) inspects : 5178335 (3876844 /sec) conflict literals : 1180 (15.89 % deleted) CPU time : 1.33571 s SATISFIABLE VERIFY_CNF 945 END : (2 seconds) [Thu Jun 1 14:13:16 2006] VERIFY_CNF 945 CPU : 1.89 = 0 + 0 + 1.79 + 0.1 # RESULT : makespan 945 SATISFIABLE SHOW_RESULT 945 BEGIN : [Thu Jun 1 14:13:16 2006] # ASSIGN : makespan 945 # ASSIGN : s_0_0 33 # ASSIGN : s_0_1 220 # ASSIGN : s_0_2 254 # ASSIGN : s_0_3 408 # ASSIGN : s_0_4 484 # ASSIGN : s_1_0 297 # ASSIGN : s_1_1 349 # ASSIGN : s_1_2 393 # ASSIGN : s_1_3 529 # ASSIGN : s_1_4 776 # ASSIGN : s_2_0 411 # ASSIGN : s_2_1 553 # ASSIGN : s_2_2 576 # ASSIGN : s_2_3 618 # ASSIGN : s_2_4 676 # ASSIGN : s_3_0 35 # ASSIGN : s_3_1 133 # ASSIGN : s_3_2 552 # ASSIGN : s_3_3 797 # ASSIGN : s_3_4 879 # ASSIGN : s_4_0 75 # ASSIGN : s_4_1 112 # ASSIGN : s_4_2 146 # ASSIGN : s_4_3 210 # ASSIGN : s_4_4 229 # ASSIGN : s_5_0 296 # ASSIGN : s_5_1 339 # ASSIGN : s_5_2 461 # ASSIGN : s_5_3 657 # ASSIGN : s_5_4 866 # ASSIGN : s_6_0 13 # ASSIGN : s_6_1 183 # ASSIGN : s_6_2 252 # ASSIGN : s_6_3 365 # ASSIGN : s_6_4 442 # ASSIGN : s_7_0 626 # ASSIGN : s_7_1 695 # ASSIGN : s_7_2 736 # ASSIGN : s_7_3 774 # ASSIGN : s_7_4 880 # ASSIGN : s_8_0 1 # ASSIGN : s_8_1 467 # ASSIGN : s_8_2 527 # ASSIGN : s_8_3 852 # ASSIGN : s_8_4 896 # ASSIGN : s_9_0 312 # ASSIGN : s_9_1 450 # ASSIGN : s_9_2 539 # ASSIGN : s_9_3 620 # ASSIGN : s_9_4 775 # ASSIGN : s_10_0 47 # ASSIGN : s_10_1 99 # ASSIGN : s_10_2 134 # ASSIGN : s_10_3 804 # ASSIGN : s_10_4 889 # ASSIGN : s_11_0 565 # ASSIGN : s_11_1 631 # ASSIGN : s_11_2 641 # ASSIGN : s_11_3 760 # ASSIGN : s_11_4 769 # ASSIGN : s_12_0 195 # ASSIGN : s_12_1 448 # ASSIGN : s_12_2 464 # ASSIGN : s_12_3 555 # ASSIGN : s_12_4 899 # ASSIGN : s_13_0 4 # ASSIGN : s_13_1 54 # ASSIGN : s_13_2 106 # ASSIGN : s_13_3 614 # ASSIGN : s_13_4 719 # ASSIGN : s_14_0 686 # ASSIGN : s_14_1 773 # ASSIGN : s_14_2 818 # ASSIGN : s_14_3 857 # ASSIGN : s_14_4 904 SHOW_RESULT 945 END : 945 (1 seconds) [Thu Jun 1 14:13:17 2006] SHOW_RESULT 945 CPU : 0.229999999999997 = 0.229999999999997 + 0 + 0 + 0 # BOUND : makespan 926 945 MODIFY_CNF 935 BEGIN : [Thu Jun 1 14:13:17 2006] MODIFY_CNF 935 END : 26018474 bytes (0 seconds) [Thu Jun 1 14:13:17 2006] MODIFY_CNF 935 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 935 BEGIN : [Thu Jun 1 14:13:17 2006] CMD : minisat /work/tamura/csp2sat66598.cnf /work/tamura/csp2sat66598.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 858118 2523395 | 286039 0 0 NaNQ | 0.000 % | ==============================================================================) restarts : 1 conflicts : 22 (19 /sec) decisions : 220 (189 /sec) propagations : 137478 (118028 /sec) inspects : 1424518 (1222984 /sec) conflict literals : 208 (2.80 % deleted) CPU time : 1.16479 s SATISFIABLE VERIFY_CNF 935 END : (1 seconds) [Thu Jun 1 14:13:18 2006] VERIFY_CNF 935 CPU : 1.74000000000001 = 0.0100000000000051 + 0.01 + 1.61 + 0.11 # RESULT : makespan 935 SATISFIABLE SHOW_RESULT 935 BEGIN : [Thu Jun 1 14:13:18 2006] # ASSIGN : makespan 935 # ASSIGN : s_0_0 5 # ASSIGN : s_0_1 26 # ASSIGN : s_0_2 60 # ASSIGN : s_0_3 232 # ASSIGN : s_0_4 312 # ASSIGN : s_1_0 79 # ASSIGN : s_1_1 155 # ASSIGN : s_1_2 343 # ASSIGN : s_1_3 414 # ASSIGN : s_1_4 615 # ASSIGN : s_2_0 138 # ASSIGN : s_2_1 220 # ASSIGN : s_2_2 301 # ASSIGN : s_2_3 367 # ASSIGN : s_2_4 787 # ASSIGN : s_3_0 2 # ASSIGN : s_3_1 82 # ASSIGN : s_3_2 171 # ASSIGN : s_3_3 285 # ASSIGN : s_3_4 348 # ASSIGN : s_4_0 250 # ASSIGN : s_4_1 406 # ASSIGN : s_4_2 440 # ASSIGN : s_4_3 539 # ASSIGN : s_4_4 759 # ASSIGN : s_5_0 267 # ASSIGN : s_5_1 469 # ASSIGN : s_5_2 523 # ASSIGN : s_5_3 621 # ASSIGN : s_5_4 683 # ASSIGN : s_6_0 6 # ASSIGN : s_6_1 131 # ASSIGN : s_6_2 200 # ASSIGN : s_6_3 287 # ASSIGN : s_6_4 504 # ASSIGN : s_7_0 99 # ASSIGN : s_7_1 159 # ASSIGN : s_7_2 310 # ASSIGN : s_7_3 364 # ASSIGN : s_7_4 483 # ASSIGN : s_8_0 169 # ASSIGN : s_8_1 507 # ASSIGN : s_8_2 762 # ASSIGN : s_8_3 842 # ASSIGN : s_8_4 886 # ASSIGN : s_9_0 340 # ASSIGN : s_9_1 447 # ASSIGN : s_9_2 524 # ASSIGN : s_9_3 603 # ASSIGN : s_9_4 721 # ASSIGN : s_10_0 538 # ASSIGN : s_10_1 591 # ASSIGN : s_10_2 636 # ASSIGN : s_10_3 733 # ASSIGN : s_10_4 879 # ASSIGN : s_11_0 159 # ASSIGN : s_11_1 566 # ASSIGN : s_11_2 626 # ASSIGN : s_11_3 730 # ASSIGN : s_11_4 809 # ASSIGN : s_12_0 576 # ASSIGN : s_12_1 717 # ASSIGN : s_12_2 739 # ASSIGN : s_12_3 830 # ASSIGN : s_12_4 889 # ASSIGN : s_13_0 635 # ASSIGN : s_13_1 678 # ASSIGN : s_13_2 731 # ASSIGN : s_13_3 764 # ASSIGN : s_13_4 844 # ASSIGN : s_14_0 436 # ASSIGN : s_14_1 558 # ASSIGN : s_14_2 791 # ASSIGN : s_14_3 885 # ASSIGN : s_14_4 894 SHOW_RESULT 935 END : 935 (1 seconds) [Thu Jun 1 14:13:19 2006] SHOW_RESULT 935 CPU : 0.219999999999999 = 0.219999999999999 + 0 + 0 + 0 # BOUND : makespan 926 935 MODIFY_CNF 930 BEGIN : [Thu Jun 1 14:13:19 2006] MODIFY_CNF 930 END : 26018473 bytes (0 seconds) [Thu Jun 1 14:13:19 2006] MODIFY_CNF 930 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 930 BEGIN : [Thu Jun 1 14:13:19 2006] CMD : minisat /work/tamura/csp2sat66598.cnf /work/tamura/csp2sat66598.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 852488 2506885 | 284162 0 0 NaNQ | 0.000 % | | 100 | 852488 2506885 | 312578 100 2494 24.9 | 38.205 % | ==============================================================================) restarts : 2 conflicts : 124 (91 /sec) decisions : 382 (280 /sec) propagations : 397293 (291647 /sec) inspects : 4813630 (3533622 /sec) conflict literals : 2751 (13.41 % deleted) CPU time : 1.36224 s SATISFIABLE VERIFY_CNF 930 END : (1 seconds) [Thu Jun 1 14:13:20 2006] VERIFY_CNF 930 CPU : 1.92 = 0.00999999999999801 + 0.01 + 1.81 + 0.09 # RESULT : makespan 930 SATISFIABLE SHOW_RESULT 930 BEGIN : [Thu Jun 1 14:13:20 2006] # ASSIGN : makespan 930 # ASSIGN : s_0_0 29 # ASSIGN : s_0_1 50 # ASSIGN : s_0_2 91 # ASSIGN : s_0_3 611 # ASSIGN : s_0_4 684 # ASSIGN : s_1_0 134 # ASSIGN : s_1_1 186 # ASSIGN : s_1_2 211 # ASSIGN : s_1_3 597 # ASSIGN : s_1_4 863 # ASSIGN : s_2_0 84 # ASSIGN : s_2_1 158 # ASSIGN : s_2_2 524 # ASSIGN : s_2_3 566 # ASSIGN : s_2_4 608 # ASSIGN : s_3_0 4 # ASSIGN : s_3_1 102 # ASSIGN : s_3_2 202 # ASSIGN : s_3_3 281 # ASSIGN : s_3_4 821 # ASSIGN : s_4_0 44 # ASSIGN : s_4_1 81 # ASSIGN : s_4_2 115 # ASSIGN : s_4_3 179 # ASSIGN : s_4_4 198 # ASSIGN : s_5_0 239 # ASSIGN : s_5_1 282 # ASSIGN : s_5_2 336 # ASSIGN : s_5_3 452 # ASSIGN : s_5_4 715 # ASSIGN : s_6_0 4 # ASSIGN : s_6_1 267 # ASSIGN : s_6_2 336 # ASSIGN : s_6_3 423 # ASSIGN : s_6_4 510 # ASSIGN : s_7_0 664 # ASSIGN : s_7_1 742 # ASSIGN : s_7_2 783 # ASSIGN : s_7_3 823 # ASSIGN : s_7_4 906 # ASSIGN : s_8_0 412 # ASSIGN : s_8_1 514 # ASSIGN : s_8_2 794 # ASSIGN : s_8_3 819 # ASSIGN : s_8_4 874 # ASSIGN : s_9_0 428 # ASSIGN : s_9_1 528 # ASSIGN : s_9_2 605 # ASSIGN : s_9_3 799 # ASSIGN : s_9_4 887 # ASSIGN : s_10_0 500 # ASSIGN : s_10_1 623 # ASSIGN : s_10_2 724 # ASSIGN : s_10_3 830 # ASSIGN : s_10_4 923 # ASSIGN : s_11_0 97 # ASSIGN : s_11_1 307 # ASSIGN : s_11_2 317 # ASSIGN : s_11_3 515 # ASSIGN : s_11_4 531 # ASSIGN : s_12_0 349 # ASSIGN : s_12_1 408 # ASSIGN : s_12_2 424 # ASSIGN : s_12_3 724 # ASSIGN : s_12_4 884 # ASSIGN : s_13_0 1 # ASSIGN : s_13_1 50 # ASSIGN : s_13_2 170 # ASSIGN : s_13_3 697 # ASSIGN : s_13_4 780 # ASSIGN : s_14_0 524 # ASSIGN : s_14_1 613 # ASSIGN : s_14_2 658 # ASSIGN : s_14_3 706 # ASSIGN : s_14_4 739 SHOW_RESULT 930 END : 930 (1 seconds) [Thu Jun 1 14:13:21 2006] SHOW_RESULT 930 CPU : 0.219999999999999 = 0.219999999999999 + 0 + 0 + 0 # BOUND : makespan 926 930 MODIFY_CNF 928 BEGIN : [Thu Jun 1 14:13:21 2006] MODIFY_CNF 928 END : 26018473 bytes (0 seconds) [Thu Jun 1 14:13:21 2006] MODIFY_CNF 928 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 928 BEGIN : [Thu Jun 1 14:13:21 2006] CMD : minisat /work/tamura/csp2sat66598.cnf /work/tamura/csp2sat66598.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 850236 2500281 | 283412 0 0 NaNQ | 0.000 % | | 101 | 850236 2500281 | 311753 101 1939 19.2 | 38.390 % | ==============================================================================) restarts : 2 conflicts : 142 (104 /sec) decisions : 440 (322 /sec) propagations : 430747 (315099 /sec) inspects : 5063042 (3703699 /sec) conflict literals : 2281 (12.03 % deleted) CPU time : 1.36702 s SATISFIABLE VERIFY_CNF 928 END : (2 seconds) [Thu Jun 1 14:13:23 2006] VERIFY_CNF 928 CPU : 1.88000000000001 = 0.0100000000000051 + 0 + 1.84 + 0.03 # RESULT : makespan 928 SATISFIABLE SHOW_RESULT 928 BEGIN : [Thu Jun 1 14:13:23 2006] # ASSIGN : makespan 928 # ASSIGN : s_0_0 67 # ASSIGN : s_0_1 98 # ASSIGN : s_0_2 201 # ASSIGN : s_0_3 397 # ASSIGN : s_0_4 493 # ASSIGN : s_1_0 3 # ASSIGN : s_1_1 55 # ASSIGN : s_1_2 493 # ASSIGN : s_1_3 696 # ASSIGN : s_1_4 861 # ASSIGN : s_2_0 14 # ASSIGN : s_2_1 95 # ASSIGN : s_2_2 215 # ASSIGN : s_2_3 257 # ASSIGN : s_2_4 296 # ASSIGN : s_3_0 317 # ASSIGN : s_3_1 394 # ASSIGN : s_3_2 471 # ASSIGN : s_3_3 762 # ASSIGN : s_3_4 819 # ASSIGN : s_4_0 18 # ASSIGN : s_4_1 98 # ASSIGN : s_4_2 132 # ASSIGN : s_4_3 196 # ASSIGN : s_4_4 222 # ASSIGN : s_5_0 45 # ASSIGN : s_5_1 88 # ASSIGN : s_5_2 305 # ASSIGN : s_5_3 431 # ASSIGN : s_5_4 849 # ASSIGN : s_6_0 2 # ASSIGN : s_6_1 188 # ASSIGN : s_6_2 307 # ASSIGN : s_6_3 394 # ASSIGN : s_6_4 473 # ASSIGN : s_7_0 607 # ASSIGN : s_7_1 681 # ASSIGN : s_7_2 722 # ASSIGN : s_7_3 766 # ASSIGN : s_7_4 904 # ASSIGN : s_8_0 301 # ASSIGN : s_8_1 606 # ASSIGN : s_8_2 741 # ASSIGN : s_8_3 817 # ASSIGN : s_8_4 872 # ASSIGN : s_9_0 511 # ASSIGN : s_9_1 622 # ASSIGN : s_9_2 699 # ASSIGN : s_9_3 797 # ASSIGN : s_9_4 885 # ASSIGN : s_10_0 173 # ASSIGN : s_10_1 399 # ASSIGN : s_10_2 667 # ASSIGN : s_10_3 828 # ASSIGN : s_10_4 921 # ASSIGN : s_11_0 450 # ASSIGN : s_11_1 550 # ASSIGN : s_11_2 560 # ASSIGN : s_11_3 655 # ASSIGN : s_11_4 664 # ASSIGN : s_12_0 114 # ASSIGN : s_12_1 548 # ASSIGN : s_12_2 564 # ASSIGN : s_12_3 760 # ASSIGN : s_12_4 882 # ASSIGN : s_13_0 71 # ASSIGN : s_13_1 142 # ASSIGN : s_13_2 194 # ASSIGN : s_13_3 669 # ASSIGN : s_13_4 778 # ASSIGN : s_14_0 107 # ASSIGN : s_14_1 262 # ASSIGN : s_14_2 434 # ASSIGN : s_14_3 613 # ASSIGN : s_14_4 623 SHOW_RESULT 928 END : 928 (0 seconds) [Thu Jun 1 14:13:23 2006] SHOW_RESULT 928 CPU : 0.219999999999999 = 0.219999999999999 + 0 + 0 + 0 # BOUND : makespan 926 928 MODIFY_CNF 927 BEGIN : [Thu Jun 1 14:13:23 2006] MODIFY_CNF 927 END : 26018473 bytes (0 seconds) [Thu Jun 1 14:13:23 2006] MODIFY_CNF 927 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 927 BEGIN : [Thu Jun 1 14:13:23 2006] CMD : minisat /work/tamura/csp2sat66598.cnf /work/tamura/csp2sat66598.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 849110 2496979 | 283036 0 0 NaNQ | 0.000 % | | 100 | 849110 2496979 | 311339 100 2026 20.3 | 38.482 % | ==============================================================================) restarts : 2 conflicts : 182 (122 /sec) decisions : 473 (316 /sec) propagations : 660391 (441544 /sec) inspects : 7702952 (5150275 /sec) conflict literals : 2840 (18.20 % deleted) CPU time : 1.49564 s SATISFIABLE VERIFY_CNF 927 END : (2 seconds) [Thu Jun 1 14:13:25 2006] VERIFY_CNF 927 CPU : 2.07 = 0.00999999999999801 + 0.01 + 1.95 + 0.1 # RESULT : makespan 927 SATISFIABLE SHOW_RESULT 927 BEGIN : [Thu Jun 1 14:13:25 2006] # ASSIGN : makespan 927 # ASSIGN : s_0_0 288 # ASSIGN : s_0_1 358 # ASSIGN : s_0_2 392 # ASSIGN : s_0_3 495 # ASSIGN : s_0_4 594 # ASSIGN : s_1_0 215 # ASSIGN : s_1_1 268 # ASSIGN : s_1_2 536 # ASSIGN : s_1_3 669 # ASSIGN : s_1_4 906 # ASSIGN : s_2_0 176 # ASSIGN : s_2_1 249 # ASSIGN : s_2_2 607 # ASSIGN : s_2_3 649 # ASSIGN : s_2_4 829 # ASSIGN : s_3_0 22 # ASSIGN : s_3_1 99 # ASSIGN : s_3_2 182 # ASSIGN : s_3_3 261 # ASSIGN : s_3_4 695 # ASSIGN : s_4_0 86 # ASSIGN : s_4_1 173 # ASSIGN : s_4_2 207 # ASSIGN : s_4_3 782 # ASSIGN : s_4_4 823 # ASSIGN : s_5_0 133 # ASSIGN : s_5_1 176 # ASSIGN : s_5_2 403 # ASSIGN : s_5_3 502 # ASSIGN : s_5_4 564 # ASSIGN : s_6_0 1 # ASSIGN : s_6_1 331 # ASSIGN : s_6_2 400 # ASSIGN : s_6_3 487 # ASSIGN : s_6_4 582 # ASSIGN : s_7_0 94 # ASSIGN : s_7_1 230 # ASSIGN : s_7_2 271 # ASSIGN : s_7_3 309 # ASSIGN : s_7_4 868 # ASSIGN : s_8_0 0 # ASSIGN : s_8_1 267 # ASSIGN : s_8_2 284 # ASSIGN : s_8_3 672 # ASSIGN : s_8_4 733 # ASSIGN : s_9_0 548 # ASSIGN : s_9_1 652 # ASSIGN : s_9_2 729 # ASSIGN : s_9_3 808 # ASSIGN : s_9_4 884 # ASSIGN : s_10_0 58 # ASSIGN : s_10_1 98 # ASSIGN : s_10_2 154 # ASSIGN : s_10_3 426 # ASSIGN : s_10_4 801 # ASSIGN : s_11_0 716 # ASSIGN : s_11_1 778 # ASSIGN : s_11_2 788 # ASSIGN : s_11_3 883 # ASSIGN : s_11_4 892 # ASSIGN : s_12_0 123 # ASSIGN : s_12_1 293 # ASSIGN : s_12_2 309 # ASSIGN : s_12_3 484 # ASSIGN : s_12_4 777 # ASSIGN : s_13_0 4 # ASSIGN : s_13_1 47 # ASSIGN : s_13_2 644 # ASSIGN : s_13_3 761 # ASSIGN : s_13_4 818 # ASSIGN : s_14_0 316 # ASSIGN : s_14_1 491 # ASSIGN : s_14_2 543 # ASSIGN : s_14_3 643 # ASSIGN : s_14_4 688 SHOW_RESULT 927 END : 927 (0 seconds) [Thu Jun 1 14:13:25 2006] SHOW_RESULT 927 CPU : 0.219999999999999 = 0.219999999999999 + 0 + 0 + 0 # BOUND : makespan 926 927 MODIFY_CNF 926 BEGIN : [Thu Jun 1 14:13:25 2006] MODIFY_CNF 926 END : 26018473 bytes (0 seconds) [Thu Jun 1 14:13:25 2006] MODIFY_CNF 926 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 926 BEGIN : [Thu Jun 1 14:13:25 2006] CMD : minisat /work/tamura/csp2sat66598.cnf /work/tamura/csp2sat66598.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 847985 2493679 | 282661 0 0 NaNQ | 0.000 % | | 100 | 847985 2493679 | 310927 100 1778 17.8 | 38.575 % | | 251 | 847985 2493679 | 342019 251 3311 13.2 | 38.575 % | | 477 | 847985 2493679 | 376221 477 5890 12.3 | 38.575 % | ==============================================================================) restarts : 4 conflicts : 581 (260 /sec) decisions : 1142 (511 /sec) propagations : 2163791 (967641 /sec) inspects : 23587730 (10548367 /sec) conflict literals : 7013 (22.40 % deleted) CPU time : 2.23615 s SATISFIABLE VERIFY_CNF 926 END : (3 seconds) [Thu Jun 1 14:13:28 2006] VERIFY_CNF 926 CPU : 2.81 = 0.00999999999999801 + 0.01 + 2.69 + 0.1 # RESULT : makespan 926 SATISFIABLE SHOW_RESULT 926 BEGIN : [Thu Jun 1 14:13:28 2006] # ASSIGN : makespan 926 # ASSIGN : s_0_0 50 # ASSIGN : s_0_1 125 # ASSIGN : s_0_2 264 # ASSIGN : s_0_3 426 # ASSIGN : s_0_4 550 # ASSIGN : s_1_0 55 # ASSIGN : s_1_1 107 # ASSIGN : s_1_2 123 # ASSIGN : s_1_3 194 # ASSIGN : s_1_4 220 # ASSIGN : s_2_0 368 # ASSIGN : s_2_1 479 # ASSIGN : s_2_2 609 # ASSIGN : s_2_3 690 # ASSIGN : s_2_4 828 # ASSIGN : s_3_0 126 # ASSIGN : s_3_1 203 # ASSIGN : s_3_2 359 # ASSIGN : s_3_3 693 # ASSIGN : s_3_4 817 # ASSIGN : s_4_0 217 # ASSIGN : s_4_1 270 # ASSIGN : s_4_2 304 # ASSIGN : s_4_3 740 # ASSIGN : s_4_4 843 # ASSIGN : s_5_0 237 # ASSIGN : s_5_1 280 # ASSIGN : s_5_2 334 # ASSIGN : s_5_3 488 # ASSIGN : s_5_4 573 # ASSIGN : s_6_0 241 # ASSIGN : s_6_1 340 # ASSIGN : s_6_2 409 # ASSIGN : s_6_3 496 # ASSIGN : s_6_4 730 # ASSIGN : s_7_0 491 # ASSIGN : s_7_1 651 # ASSIGN : s_7_2 692 # ASSIGN : s_7_3 736 # ASSIGN : s_7_4 819 # ASSIGN : s_8_0 11 # ASSIGN : s_8_1 109 # ASSIGN : s_8_2 151 # ASSIGN : s_8_3 176 # ASSIGN : s_8_4 759 # ASSIGN : s_9_0 551 # ASSIGN : s_9_1 652 # ASSIGN : s_9_2 729 # ASSIGN : s_9_3 808 # ASSIGN : s_9_4 883 # ASSIGN : s_10_0 123 # ASSIGN : s_10_1 159 # ASSIGN : s_10_2 748 # ASSIGN : s_10_3 843 # ASSIGN : s_10_4 919 # ASSIGN : s_11_0 0 # ASSIGN : s_11_1 254 # ASSIGN : s_11_2 466 # ASSIGN : s_11_3 596 # ASSIGN : s_11_4 605 # ASSIGN : s_12_0 48 # ASSIGN : s_12_1 431 # ASSIGN : s_12_2 497 # ASSIGN : s_12_3 588 # ASSIGN : s_12_4 647 # ASSIGN : s_13_0 5 # ASSIGN : s_13_1 71 # ASSIGN : s_13_2 148 # ASSIGN : s_13_3 561 # ASSIGN : s_13_4 640 # ASSIGN : s_14_0 61 # ASSIGN : s_14_1 354 # ASSIGN : s_14_2 399 # ASSIGN : s_14_3 438 # ASSIGN : s_14_4 447 SHOW_RESULT 926 END : 926 (0 seconds) [Thu Jun 1 14:13:28 2006] SHOW_RESULT 926 CPU : 0.220000000000006 = 0.220000000000006 + 0 + 0 + 0 # BOUND : makespan 926 926 MAIN END : (79 seconds) [Thu Jun 1 14:13:28 2006] MAIN CPU : 78.47 = 62.99 + 0.13 + 14.77 + 0.58