MAIN BEGIN : [Fri Jun 2 08:35:24 2006] READ BEGIN : csp/orb05.csp [Fri Jun 2 08:35:24 2006] READ END : csp/orb05.csp (2 seconds) [Fri Jun 2 08:35:26 2006] READ CPU : 1.35 = 1.35 + 0 + 0 + 0 # BOUND : makespan 630 1116 GENERATE_CNF 1116 BEGIN : [Fri Jun 2 08:35:26 2006] GENERATE_CNF 1116 END : 113288 variables 1175978 clauses 26178226 bytes (57 seconds) [Fri Jun 2 08:36:23 2006] GENERATE_CNF 1116 CPU : 57.11 = 57.03 + 0.08 + 0 + 0 MODIFY_CNF 873 BEGIN : [Fri Jun 2 08:36:23 2006] MODIFY_CNF 873 END : 26178232 bytes (0 seconds) [Fri Jun 2 08:36:23 2006] MODIFY_CNF 873 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 873 BEGIN : [Fri Jun 2 08:36:23 2006] CMD : minisat /work/tamura/csp2sat54964.cnf /work/tamura/csp2sat54964.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 464824 1355619 | 154941 0 0 NaNQ | 0.000 % | | 100 | 464824 1355619 | 170435 100 624 6.2 | 65.383 % | | 253 | 464824 1355619 | 187478 253 1675 6.6 | 65.383 % | | 478 | 464824 1355619 | 206226 478 4059 8.5 | 65.383 % | | 815 | 464824 1355619 | 226849 815 7242 8.9 | 65.383 % | ==============================================================================) restarts : 5 conflicts : 1172 (299 /sec) decisions : 1597 (407 /sec) propagations : 6733826 (1717113 /sec) inspects : 41392339 (10554967 /sec) conflict literals : 10048 (32.43 % deleted) CPU time : 3.9216 s UNSATISFIABLE VERIFY_CNF 873 END : (4 seconds) [Fri Jun 2 08:36:27 2006] VERIFY_CNF 873 CPU : 4.21 = 0.00999999999999801 + 0.01 + 4.17 + 0.02 # RESULT : makespan 873 UNSATISFIABLE # BOUND : makespan 874 1116 MODIFY_CNF 995 BEGIN : [Fri Jun 2 08:36:27 2006] MODIFY_CNF 995 END : 26178232 bytes (0 seconds) [Fri Jun 2 08:36:27 2006] MODIFY_CNF 995 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 995 BEGIN : [Fri Jun 2 08:36:27 2006] CMD : minisat /work/tamura/csp2sat54964.cnf /work/tamura/csp2sat54964.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 625873 1826350 | 208624 0 0 NaNQ | 0.000 % | ==============================================================================) restarts : 1 conflicts : 7 (5 /sec) decisions : 131 (97 /sec) propagations : 162824 (120975 /sec) inspects : 1124039 (835140 /sec) conflict literals : 98 (14.04 % deleted) CPU time : 1.34593 s SATISFIABLE VERIFY_CNF 995 END : (2 seconds) [Fri Jun 2 08:36:29 2006] VERIFY_CNF 995 CPU : 1.83 = 0 + 0 + 1.71 + 0.12 # RESULT : makespan 995 SATISFIABLE SHOW_RESULT 995 BEGIN : [Fri Jun 2 08:36:29 2006] # ASSIGN : makespan 995 # ASSIGN : s_0_0 41 # ASSIGN : s_0_1 62 # ASSIGN : s_0_2 172 # ASSIGN : s_0_3 220 # ASSIGN : s_0_4 305 # ASSIGN : s_0_5 318 # ASSIGN : s_0_6 391 # ASSIGN : s_0_7 450 # ASSIGN : s_0_8 545 # ASSIGN : s_0_9 626 # ASSIGN : s_1_0 0 # ASSIGN : s_1_1 52 # ASSIGN : s_1_2 302 # ASSIGN : s_1_3 386 # ASSIGN : s_1_4 530 # ASSIGN : s_1_5 586 # ASSIGN : s_1_6 596 # ASSIGN : s_1_7 622 # ASSIGN : s_1_8 672 # ASSIGN : s_1_9 711 # ASSIGN : s_2_0 128 # ASSIGN : s_2_1 178 # ASSIGN : s_2_2 296 # ASSIGN : s_2_3 322 # ASSIGN : s_2_4 388 # ASSIGN : s_2_5 456 # ASSIGN : s_2_6 623 # ASSIGN : s_2_7 737 # ASSIGN : s_2_8 760 # ASSIGN : s_2_9 848 # ASSIGN : s_3_0 10 # ASSIGN : s_3_1 37 # ASSIGN : s_3_2 95 # ASSIGN : s_3_3 157 # ASSIGN : s_3_4 203 # ASSIGN : s_3_5 252 # ASSIGN : s_3_6 258 # ASSIGN : s_3_7 721 # ASSIGN : s_3_8 749 # ASSIGN : s_3_9 829 # ASSIGN : s_4_0 28 # ASSIGN : s_4_1 106 # ASSIGN : s_4_2 153 # ASSIGN : s_4_3 182 # ASSIGN : s_4_4 199 # ASSIGN : s_4_5 228 # ASSIGN : s_4_6 285 # ASSIGN : s_4_7 363 # ASSIGN : s_4_8 710 # ASSIGN : s_4_9 859 # ASSIGN : s_5_0 156 # ASSIGN : s_5_1 222 # ASSIGN : s_5_2 273 # ASSIGN : s_5_3 322 # ASSIGN : s_5_4 389 # ASSIGN : s_5_5 458 # ASSIGN : s_5_6 473 # ASSIGN : s_5_7 665 # ASSIGN : s_5_8 691 # ASSIGN : s_5_9 750 # ASSIGN : s_6_0 155 # ASSIGN : s_6_1 244 # ASSIGN : s_6_2 428 # ASSIGN : s_6_3 541 # ASSIGN : s_6_4 616 # ASSIGN : s_6_5 650 # ASSIGN : s_6_6 668 # ASSIGN : s_6_7 751 # ASSIGN : s_6_8 766 # ASSIGN : s_6_9 869 # ASSIGN : s_7_0 320 # ASSIGN : s_7_1 376 # ASSIGN : s_7_2 459 # ASSIGN : s_7_3 539 # ASSIGN : s_7_4 555 # ASSIGN : s_7_5 702 # ASSIGN : s_7_6 795 # ASSIGN : s_7_7 825 # ASSIGN : s_7_8 854 # ASSIGN : s_7_9 967 # ASSIGN : s_8_0 392 # ASSIGN : s_8_1 471 # ASSIGN : s_8_2 540 # ASSIGN : s_8_3 624 # ASSIGN : s_8_4 640 # ASSIGN : s_8_5 719 # ASSIGN : s_8_6 760 # ASSIGN : s_8_7 851 # ASSIGN : s_8_8 886 # ASSIGN : s_8_9 920 # ASSIGN : s_9_0 5 # ASSIGN : s_9_1 18 # ASSIGN : s_9_2 63 # ASSIGN : s_9_3 83 # ASSIGN : s_9_4 104 # ASSIGN : s_9_5 198 # ASSIGN : s_9_6 661 # ASSIGN : s_9_7 805 # ASSIGN : s_9_8 836 # ASSIGN : s_9_9 932 SHOW_RESULT 995 END : 995 (0 seconds) [Fri Jun 2 08:36:29 2006] SHOW_RESULT 995 CPU : 0.32 = 0.32 + 0 + 0 + 0 # BOUND : makespan 874 995 MODIFY_CNF 934 BEGIN : [Fri Jun 2 08:36:29 2006] MODIFY_CNF 934 END : 26178232 bytes (0 seconds) [Fri Jun 2 08:36:29 2006] MODIFY_CNF 934 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 934 BEGIN : [Fri Jun 2 08:36:29 2006] CMD : minisat /work/tamura/csp2sat54964.cnf /work/tamura/csp2sat54964.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 546894 1595614 | 182298 0 0 NaNQ | 0.000 % | ==============================================================================) restarts : 1 conflicts : 16 (11 /sec) decisions : 122 (86 /sec) propagations : 201493 (141677 /sec) inspects : 1452981 (1021647 /sec) conflict literals : 282 (13.50 % deleted) CPU time : 1.42219 s SATISFIABLE VERIFY_CNF 934 END : (2 seconds) [Fri Jun 2 08:36:31 2006] VERIFY_CNF 934 CPU : 1.87 = 0 + 0.01 + 1.75 + 0.11 # RESULT : makespan 934 SATISFIABLE SHOW_RESULT 934 BEGIN : [Fri Jun 2 08:36:31 2006] # ASSIGN : makespan 934 # ASSIGN : s_0_0 180 # ASSIGN : s_0_1 230 # ASSIGN : s_0_2 354 # ASSIGN : s_0_3 402 # ASSIGN : s_0_4 479 # ASSIGN : s_0_5 492 # ASSIGN : s_0_6 563 # ASSIGN : s_0_7 622 # ASSIGN : s_0_8 712 # ASSIGN : s_0_9 722 # ASSIGN : s_1_0 42 # ASSIGN : s_1_1 94 # ASSIGN : s_1_2 170 # ASSIGN : s_1_3 254 # ASSIGN : s_1_4 340 # ASSIGN : s_1_5 396 # ASSIGN : s_1_6 406 # ASSIGN : s_1_7 432 # ASSIGN : s_1_8 524 # ASSIGN : s_1_9 565 # ASSIGN : s_2_0 0 # ASSIGN : s_2_1 186 # ASSIGN : s_2_2 478 # ASSIGN : s_2_3 518 # ASSIGN : s_2_4 644 # ASSIGN : s_2_5 738 # ASSIGN : s_2_6 812 # ASSIGN : s_2_7 839 # ASSIGN : s_2_8 853 # ASSIGN : s_2_9 868 # ASSIGN : s_3_0 129 # ASSIGN : s_3_1 147 # ASSIGN : s_3_2 205 # ASSIGN : s_3_3 269 # ASSIGN : s_3_4 315 # ASSIGN : s_3_5 426 # ASSIGN : s_3_6 432 # ASSIGN : s_3_7 660 # ASSIGN : s_3_8 688 # ASSIGN : s_3_9 768 # ASSIGN : s_4_0 11 # ASSIGN : s_4_1 89 # ASSIGN : s_4_2 136 # ASSIGN : s_4_3 165 # ASSIGN : s_4_4 181 # ASSIGN : s_4_5 210 # ASSIGN : s_4_6 267 # ASSIGN : s_4_7 345 # ASSIGN : s_4_8 649 # ASSIGN : s_4_9 798 # ASSIGN : s_5_0 28 # ASSIGN : s_5_1 112 # ASSIGN : s_5_2 178 # ASSIGN : s_5_3 190 # ASSIGN : s_5_4 258 # ASSIGN : s_5_5 325 # ASSIGN : s_5_6 340 # ASSIGN : s_5_7 596 # ASSIGN : s_5_8 702 # ASSIGN : s_5_9 727 # ASSIGN : s_6_0 163 # ASSIGN : s_6_1 191 # ASSIGN : s_6_2 270 # ASSIGN : s_6_3 327 # ASSIGN : s_6_4 408 # ASSIGN : s_6_5 456 # ASSIGN : s_6_6 474 # ASSIGN : s_6_7 581 # ASSIGN : s_6_8 614 # ASSIGN : s_6_9 889 # ASSIGN : s_7_0 267 # ASSIGN : s_7_1 323 # ASSIGN : s_7_2 504 # ASSIGN : s_7_3 584 # ASSIGN : s_7_4 604 # ASSIGN : s_7_5 635 # ASSIGN : s_7_6 728 # ASSIGN : s_7_7 758 # ASSIGN : s_7_8 787 # ASSIGN : s_7_9 906 # ASSIGN : s_8_0 327 # ASSIGN : s_8_1 406 # ASSIGN : s_8_2 475 # ASSIGN : s_8_3 557 # ASSIGN : s_8_4 573 # ASSIGN : s_8_5 658 # ASSIGN : s_8_6 699 # ASSIGN : s_8_7 790 # ASSIGN : s_8_8 825 # ASSIGN : s_8_9 859 # ASSIGN : s_9_0 6 # ASSIGN : s_9_1 36 # ASSIGN : s_9_2 55 # ASSIGN : s_9_3 75 # ASSIGN : s_9_4 87 # ASSIGN : s_9_5 198 # ASSIGN : s_9_6 600 # ASSIGN : s_9_7 744 # ASSIGN : s_9_8 775 # ASSIGN : s_9_9 871 SHOW_RESULT 934 END : 934 (1 seconds) [Fri Jun 2 08:36:32 2006] SHOW_RESULT 934 CPU : 0.310000000000002 = 0.310000000000002 + 0 + 0 + 0 # BOUND : makespan 874 934 MODIFY_CNF 904 BEGIN : [Fri Jun 2 08:36:32 2006] MODIFY_CNF 904 END : 26178232 bytes (0 seconds) [Fri Jun 2 08:36:32 2006] MODIFY_CNF 904 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 904 BEGIN : [Fri Jun 2 08:36:32 2006] CMD : minisat /work/tamura/csp2sat54964.cnf /work/tamura/csp2sat54964.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 508594 1483764 | 169531 0 0 NaNQ | 0.000 % | | 100 | 508594 1483764 | 186484 100 1240 12.4 | 62.584 % | | 250 | 508594 1483764 | 205132 250 2530 10.1 | 62.584 % | ==============================================================================) restarts : 3 conflicts : 364 (157 /sec) decisions : 767 (331 /sec) propagations : 2404085 (1038561 /sec) inspects : 17024488 (7354556 /sec) conflict literals : 3669 (29.43 % deleted) CPU time : 2.31482 s SATISFIABLE VERIFY_CNF 904 END : (2 seconds) [Fri Jun 2 08:36:34 2006] VERIFY_CNF 904 CPU : 2.67 = 0.00999999999999801 + 0 + 2.62 + 0.04 # RESULT : makespan 904 SATISFIABLE SHOW_RESULT 904 BEGIN : [Fri Jun 2 08:36:34 2006] # ASSIGN : makespan 904 # ASSIGN : s_0_0 10 # ASSIGN : s_0_1 30 # ASSIGN : s_0_2 133 # ASSIGN : s_0_3 181 # ASSIGN : s_0_4 331 # ASSIGN : s_0_5 356 # ASSIGN : s_0_6 464 # ASSIGN : s_0_7 523 # ASSIGN : s_0_8 613 # ASSIGN : s_0_9 623 # ASSIGN : s_1_0 174 # ASSIGN : s_1_1 424 # ASSIGN : s_1_2 500 # ASSIGN : s_1_3 584 # ASSIGN : s_1_4 659 # ASSIGN : s_1_5 737 # ASSIGN : s_1_6 747 # ASSIGN : s_1_7 773 # ASSIGN : s_1_8 816 # ASSIGN : s_1_9 855 # ASSIGN : s_2_0 163 # ASSIGN : s_2_1 226 # ASSIGN : s_2_2 337 # ASSIGN : s_2_3 443 # ASSIGN : s_2_4 647 # ASSIGN : s_2_5 715 # ASSIGN : s_2_6 789 # ASSIGN : s_2_7 835 # ASSIGN : s_2_8 849 # ASSIGN : s_2_9 883 # ASSIGN : s_3_0 9 # ASSIGN : s_3_1 47 # ASSIGN : s_3_2 109 # ASSIGN : s_3_3 171 # ASSIGN : s_3_4 217 # ASSIGN : s_3_5 266 # ASSIGN : s_3_6 272 # ASSIGN : s_3_7 766 # ASSIGN : s_3_8 794 # ASSIGN : s_3_9 874 # ASSIGN : s_4_0 27 # ASSIGN : s_4_1 105 # ASSIGN : s_4_2 152 # ASSIGN : s_4_3 196 # ASSIGN : s_4_4 213 # ASSIGN : s_4_5 242 # ASSIGN : s_4_6 299 # ASSIGN : s_4_7 421 # ASSIGN : s_4_8 659 # ASSIGN : s_4_9 738 # ASSIGN : s_5_0 21 # ASSIGN : s_5_1 123 # ASSIGN : s_5_2 287 # ASSIGN : s_5_3 363 # ASSIGN : s_5_4 427 # ASSIGN : s_5_5 510 # ASSIGN : s_5_6 531 # ASSIGN : s_5_7 653 # ASSIGN : s_5_8 688 # ASSIGN : s_5_9 757 # ASSIGN : s_6_0 7 # ASSIGN : s_6_1 87 # ASSIGN : s_6_2 172 # ASSIGN : s_6_3 257 # ASSIGN : s_6_4 332 # ASSIGN : s_6_5 377 # ASSIGN : s_6_6 395 # ASSIGN : s_6_7 508 # ASSIGN : s_6_8 535 # ASSIGN : s_6_9 706 # ASSIGN : s_7_0 290 # ASSIGN : s_7_1 346 # ASSIGN : s_7_2 429 # ASSIGN : s_7_3 509 # ASSIGN : s_7_4 525 # ASSIGN : s_7_5 556 # ASSIGN : s_7_6 649 # ASSIGN : s_7_7 679 # ASSIGN : s_7_8 708 # ASSIGN : s_7_9 855 # ASSIGN : s_8_0 191 # ASSIGN : s_8_1 270 # ASSIGN : s_8_2 339 # ASSIGN : s_8_3 478 # ASSIGN : s_8_4 494 # ASSIGN : s_8_5 556 # ASSIGN : s_8_6 597 # ASSIGN : s_8_7 688 # ASSIGN : s_8_8 723 # ASSIGN : s_8_9 774 # ASSIGN : s_9_0 4 # ASSIGN : s_9_1 28 # ASSIGN : s_9_2 77 # ASSIGN : s_9_3 97 # ASSIGN : s_9_4 118 # ASSIGN : s_9_5 212 # ASSIGN : s_9_6 344 # ASSIGN : s_9_7 657 # ASSIGN : s_9_8 698 # ASSIGN : s_9_9 811 SHOW_RESULT 904 END : 904 (1 seconds) [Fri Jun 2 08:36:35 2006] SHOW_RESULT 904 CPU : 0.33 = 0.32 + 0.01 + 0 + 0 # BOUND : makespan 874 904 MODIFY_CNF 889 BEGIN : [Fri Jun 2 08:36:35 2006] MODIFY_CNF 889 END : 26178232 bytes (0 seconds) [Fri Jun 2 08:36:35 2006] MODIFY_CNF 889 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 889 BEGIN : [Fri Jun 2 08:36:35 2006] CMD : minisat /work/tamura/csp2sat54964.cnf /work/tamura/csp2sat54964.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 484580 1413260 | 161526 0 0 NaNQ | 0.000 % | | 100 | 484580 1413260 | 177678 100 880 8.8 | 63.944 % | | 251 | 484580 1413260 | 195446 251 2411 9.6 | 63.944 % | | 477 | 484580 1413260 | 214991 477 4361 9.1 | 63.944 % | ==============================================================================) restarts : 4 conflicts : 679 (241 /sec) decisions : 1197 (424 /sec) propagations : 3764319 (1333796 /sec) inspects : 23730631 (8408379 /sec) conflict literals : 6318 (26.04 % deleted) CPU time : 2.82226 s SATISFIABLE VERIFY_CNF 889 END : (3 seconds) [Fri Jun 2 08:36:38 2006] VERIFY_CNF 889 CPU : 3.18 = 0.00999999999999801 + 0 + 3.14 + 0.03 # RESULT : makespan 889 SATISFIABLE SHOW_RESULT 889 BEGIN : [Fri Jun 2 08:36:38 2006] # ASSIGN : makespan 889 # ASSIGN : s_0_0 12 # ASSIGN : s_0_1 23 # ASSIGN : s_0_2 116 # ASSIGN : s_0_3 164 # ASSIGN : s_0_4 240 # ASSIGN : s_0_5 253 # ASSIGN : s_0_6 324 # ASSIGN : s_0_7 394 # ASSIGN : s_0_8 484 # ASSIGN : s_0_9 494 # ASSIGN : s_1_0 117 # ASSIGN : s_1_1 241 # ASSIGN : s_1_2 317 # ASSIGN : s_1_3 401 # ASSIGN : s_1_4 483 # ASSIGN : s_1_5 722 # ASSIGN : s_1_6 732 # ASSIGN : s_1_7 758 # ASSIGN : s_1_8 801 # ASSIGN : s_1_9 840 # ASSIGN : s_2_0 317 # ASSIGN : s_2_1 494 # ASSIGN : s_2_2 538 # ASSIGN : s_2_3 564 # ASSIGN : s_2_4 632 # ASSIGN : s_2_5 700 # ASSIGN : s_2_6 774 # ASSIGN : s_2_7 820 # ASSIGN : s_2_8 834 # ASSIGN : s_2_9 868 # ASSIGN : s_3_0 186 # ASSIGN : s_3_1 204 # ASSIGN : s_3_2 262 # ASSIGN : s_3_3 324 # ASSIGN : s_3_4 370 # ASSIGN : s_3_5 395 # ASSIGN : s_3_6 423 # ASSIGN : s_3_7 751 # ASSIGN : s_3_8 779 # ASSIGN : s_3_9 859 # ASSIGN : s_4_0 10 # ASSIGN : s_4_1 88 # ASSIGN : s_4_2 135 # ASSIGN : s_4_3 237 # ASSIGN : s_4_4 366 # ASSIGN : s_4_5 400 # ASSIGN : s_4_6 479 # ASSIGN : s_4_7 557 # ASSIGN : s_4_8 644 # ASSIGN : s_4_9 723 # ASSIGN : s_5_0 345 # ASSIGN : s_5_1 411 # ASSIGN : s_5_2 462 # ASSIGN : s_5_3 474 # ASSIGN : s_5_4 539 # ASSIGN : s_5_5 615 # ASSIGN : s_5_6 630 # ASSIGN : s_5_7 696 # ASSIGN : s_5_8 722 # ASSIGN : s_5_9 742 # ASSIGN : s_6_0 0 # ASSIGN : s_6_1 106 # ASSIGN : s_6_2 195 # ASSIGN : s_6_3 246 # ASSIGN : s_6_4 330 # ASSIGN : s_6_5 383 # ASSIGN : s_6_6 401 # ASSIGN : s_6_7 542 # ASSIGN : s_6_8 559 # ASSIGN : s_6_9 725 # ASSIGN : s_7_0 182 # ASSIGN : s_7_1 238 # ASSIGN : s_7_2 321 # ASSIGN : s_7_3 548 # ASSIGN : s_7_4 575 # ASSIGN : s_7_5 606 # ASSIGN : s_7_6 699 # ASSIGN : s_7_7 729 # ASSIGN : s_7_8 768 # ASSIGN : s_7_9 840 # ASSIGN : s_8_0 27 # ASSIGN : s_8_1 169 # ASSIGN : s_8_2 242 # ASSIGN : s_8_3 338 # ASSIGN : s_8_4 354 # ASSIGN : s_8_5 416 # ASSIGN : s_8_6 457 # ASSIGN : s_8_7 578 # ASSIGN : s_8_8 613 # ASSIGN : s_8_9 647 # ASSIGN : s_9_0 5 # ASSIGN : s_9_1 32 # ASSIGN : s_9_2 51 # ASSIGN : s_9_3 71 # ASSIGN : s_9_4 83 # ASSIGN : s_9_5 177 # ASSIGN : s_9_6 271 # ASSIGN : s_9_7 652 # ASSIGN : s_9_8 683 # ASSIGN : s_9_9 796 SHOW_RESULT 889 END : 889 (0 seconds) [Fri Jun 2 08:36:38 2006] SHOW_RESULT 889 CPU : 0.32 = 0.32 + 0 + 0 + 0 # BOUND : makespan 874 889 MODIFY_CNF 881 BEGIN : [Fri Jun 2 08:36:38 2006] MODIFY_CNF 881 END : 26178232 bytes (0 seconds) [Fri Jun 2 08:36:38 2006] MODIFY_CNF 881 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 881 BEGIN : [Fri Jun 2 08:36:38 2006] CMD : minisat /work/tamura/csp2sat54964.cnf /work/tamura/csp2sat54964.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 475199 1385929 | 158399 0 0 NaNQ | 0.000 % | | 100 | 475199 1385929 | 174238 100 680 6.8 | 64.663 % | | 250 | 475199 1385929 | 191662 250 2375 9.5 | 64.663 % | | 478 | 475199 1385929 | 210829 478 4270 8.9 | 64.663 % | | 815 | 475199 1385929 | 231911 815 8207 10.1 | 64.663 % | | 1321 | 465286 1356808 | 255103 752 7003 9.3 | 65.428 % | ==============================================================================) restarts : 6 conflicts : 1770 (349 /sec) decisions : 2416 (476 /sec) propagations : 9715764 (1913663 /sec) inspects : 62073840 (12226360 /sec) conflict literals : 16164 (35.74 % deleted) CPU time : 5.07705 s UNSATISFIABLE VERIFY_CNF 881 END : (6 seconds) [Fri Jun 2 08:36:44 2006] VERIFY_CNF 881 CPU : 5.46 = 0.00999999999999801 + 0.01 + 5.33 + 0.11 # RESULT : makespan 881 UNSATISFIABLE # BOUND : makespan 882 889 MODIFY_CNF 885 BEGIN : [Fri Jun 2 08:36:44 2006] MODIFY_CNF 885 END : 26178232 bytes (0 seconds) [Fri Jun 2 08:36:44 2006] MODIFY_CNF 885 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 885 BEGIN : [Fri Jun 2 08:36:44 2006] CMD : minisat /work/tamura/csp2sat54964.cnf /work/tamura/csp2sat54964.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 479448 1398271 | 159816 0 0 NaNQ | 0.000 % | | 100 | 479448 1398271 | 175797 100 970 9.7 | 64.304 % | | 250 | 479448 1398271 | 193377 250 2652 10.6 | 64.304 % | | 475 | 479448 1398271 | 212715 475 4628 9.7 | 64.304 % | | 812 | 479448 1398271 | 233986 812 7497 9.2 | 64.304 % | | 1318 | 479448 1398271 | 257385 1318 13393 10.2 | 64.304 % | | 2077 | 479448 1398271 | 283123 2077 22446 10.8 | 64.304 % | ==============================================================================) restarts : 7 conflicts : 2602 (380 /sec) decisions : 3489 (509 /sec) propagations : 14232575 (2076984 /sec) inspects : 94215054 (13748964 /sec) conflict literals : 28146 (34.09 % deleted) CPU time : 6.85252 s UNSATISFIABLE VERIFY_CNF 885 END : (7 seconds) [Fri Jun 2 08:36:51 2006] VERIFY_CNF 885 CPU : 7.16 = 0 + 0.01 + 7.12 + 0.03 # RESULT : makespan 885 UNSATISFIABLE # BOUND : makespan 886 889 MODIFY_CNF 887 BEGIN : [Fri Jun 2 08:36:51 2006] MODIFY_CNF 887 END : 26178232 bytes (0 seconds) [Fri Jun 2 08:36:51 2006] MODIFY_CNF 887 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 887 BEGIN : [Fri Jun 2 08:36:51 2006] CMD : minisat /work/tamura/csp2sat54964.cnf /work/tamura/csp2sat54964.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 481278 1403559 | 160426 0 0 NaNQ | 0.000 % | | 103 | 481278 1403559 | 176468 103 852 8.3 | 64.126 % | | 253 | 481278 1403559 | 194115 253 2081 8.2 | 64.126 % | | 480 | 481278 1403559 | 213527 480 4271 8.9 | 64.126 % | | 817 | 481278 1403559 | 234879 817 7532 9.2 | 64.126 % | | 1323 | 481278 1403559 | 258367 1323 12762 9.6 | 64.126 % | ==============================================================================) restarts : 6 conflicts : 2034 (349 /sec) decisions : 3106 (533 /sec) propagations : 11698640 (2008742 /sec) inspects : 76892958 (13203085 /sec) conflict literals : 21587 (34.51 % deleted) CPU time : 5.82386 s SATISFIABLE VERIFY_CNF 887 END : (6 seconds) [Fri Jun 2 08:36:57 2006] VERIFY_CNF 887 CPU : 6.15 = 0 + 0 + 6.12 + 0.03 # RESULT : makespan 887 SATISFIABLE SHOW_RESULT 887 BEGIN : [Fri Jun 2 08:36:57 2006] # ASSIGN : makespan 887 # ASSIGN : s_0_0 1 # ASSIGN : s_0_1 23 # ASSIGN : s_0_2 116 # ASSIGN : s_0_3 164 # ASSIGN : s_0_4 240 # ASSIGN : s_0_5 253 # ASSIGN : s_0_6 326 # ASSIGN : s_0_7 385 # ASSIGN : s_0_8 475 # ASSIGN : s_0_9 518 # ASSIGN : s_1_0 352 # ASSIGN : s_1_1 409 # ASSIGN : s_1_2 485 # ASSIGN : s_1_3 569 # ASSIGN : s_1_4 642 # ASSIGN : s_1_5 720 # ASSIGN : s_1_6 730 # ASSIGN : s_1_7 756 # ASSIGN : s_1_8 799 # ASSIGN : s_1_9 838 # ASSIGN : s_2_0 12 # ASSIGN : s_2_1 198 # ASSIGN : s_2_2 242 # ASSIGN : s_2_3 274 # ASSIGN : s_2_4 371 # ASSIGN : s_2_5 698 # ASSIGN : s_2_6 772 # ASSIGN : s_2_7 818 # ASSIGN : s_2_8 832 # ASSIGN : s_2_9 866 # ASSIGN : s_3_0 98 # ASSIGN : s_3_1 174 # ASSIGN : s_3_2 232 # ASSIGN : s_3_3 294 # ASSIGN : s_3_4 340 # ASSIGN : s_3_5 365 # ASSIGN : s_3_6 410 # ASSIGN : s_3_7 643 # ASSIGN : s_3_8 777 # ASSIGN : s_3_9 857 # ASSIGN : s_4_0 10 # ASSIGN : s_4_1 88 # ASSIGN : s_4_2 135 # ASSIGN : s_4_3 237 # ASSIGN : s_4_4 336 # ASSIGN : s_4_5 366 # ASSIGN : s_4_6 487 # ASSIGN : s_4_7 624 # ASSIGN : s_4_8 738 # ASSIGN : s_4_9 784 # ASSIGN : s_5_0 338 # ASSIGN : s_5_1 404 # ASSIGN : s_5_2 455 # ASSIGN : s_5_3 474 # ASSIGN : s_5_4 563 # ASSIGN : s_5_5 630 # ASSIGN : s_5_6 645 # ASSIGN : s_5_7 711 # ASSIGN : s_5_8 737 # ASSIGN : s_5_9 768 # ASSIGN : s_6_0 0 # ASSIGN : s_6_1 119 # ASSIGN : s_6_2 195 # ASSIGN : s_6_3 268 # ASSIGN : s_6_4 386 # ASSIGN : s_6_5 467 # ASSIGN : s_6_6 485 # ASSIGN : s_6_7 568 # ASSIGN : s_6_8 583 # ASSIGN : s_6_9 689 # ASSIGN : s_7_0 204 # ASSIGN : s_7_1 260 # ASSIGN : s_7_2 343 # ASSIGN : s_7_3 423 # ASSIGN : s_7_4 439 # ASSIGN : s_7_5 470 # ASSIGN : s_7_6 565 # ASSIGN : s_7_7 595 # ASSIGN : s_7_8 671 # ASSIGN : s_7_9 740 # ASSIGN : s_8_0 40 # ASSIGN : s_8_1 129 # ASSIGN : s_8_2 212 # ASSIGN : s_8_3 308 # ASSIGN : s_8_4 324 # ASSIGN : s_8_5 414 # ASSIGN : s_8_6 554 # ASSIGN : s_8_7 671 # ASSIGN : s_8_8 706 # ASSIGN : s_8_9 757 # ASSIGN : s_9_0 5 # ASSIGN : s_9_1 32 # ASSIGN : s_9_2 51 # ASSIGN : s_9_3 71 # ASSIGN : s_9_4 83 # ASSIGN : s_9_5 177 # ASSIGN : s_9_6 439 # ASSIGN : s_9_7 538 # ASSIGN : s_9_8 625 # ASSIGN : s_9_9 721 SHOW_RESULT 887 END : 887 (1 seconds) [Fri Jun 2 08:36:58 2006] SHOW_RESULT 887 CPU : 0.330000000000005 = 0.330000000000005 + 0 + 0 + 0 # BOUND : makespan 886 887 MODIFY_CNF 886 BEGIN : [Fri Jun 2 08:36:58 2006] MODIFY_CNF 886 END : 26178232 bytes (0 seconds) [Fri Jun 2 08:36:58 2006] MODIFY_CNF 886 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 886 BEGIN : [Fri Jun 2 08:36:58 2006] CMD : minisat /work/tamura/csp2sat54964.cnf /work/tamura/csp2sat54964.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 480362 1400912 | 160120 0 0 NaNQ | 0.000 % | | 101 | 480362 1400912 | 176132 101 984 9.7 | 64.215 % | | 251 | 480362 1400912 | 193745 251 2311 9.2 | 64.215 % | | 476 | 480362 1400912 | 213119 476 4789 10.1 | 64.215 % | | 813 | 480362 1400912 | 234431 813 7465 9.2 | 64.215 % | | 1319 | 480362 1400912 | 257874 1319 11950 9.1 | 64.215 % | | 2078 | 480362 1400912 | 283662 2078 20813 10.0 | 64.215 % | ==============================================================================) restarts : 7 conflicts : 3066 (392 /sec) decisions : 4188 (536 /sec) propagations : 16901961 (2163094 /sec) inspects : 110206995 (14104168 /sec) conflict literals : 30993 (34.19 % deleted) CPU time : 7.81379 s UNSATISFIABLE VERIFY_CNF 886 END : (8 seconds) [Fri Jun 2 08:37:06 2006] VERIFY_CNF 886 CPU : 8.21 = 0.00999999999999801 + 0.00999999999999998 + 8.08 + 0.11 # RESULT : makespan 886 UNSATISFIABLE # BOUND : makespan 887 887 MAIN END : (102 seconds) [Fri Jun 2 08:37:06 2006] MAIN CPU : 100.82 = 60.04 + 0.14 + 40.04 + 0.6