MAIN BEGIN : [Thu Jun 1 15:35:08 2006] READ BEGIN : csp/la08.csp [Thu Jun 1 15:35:08 2006] READ END : csp/la08.csp (2 seconds) [Thu Jun 1 15:35:10 2006] READ CPU : 1.55 = 1.55 + 0 + 0 + 0 # BOUND : makespan 863 966 GENERATE_CNF 966 BEGIN : [Thu Jun 1 15:35:10 2006] GENERATE_CNF 966 END : 73830 variables 1092621 clauses 23193285 bytes (53 seconds) [Thu Jun 1 15:36:03 2006] GENERATE_CNF 966 CPU : 53.18 = 53.11 + 0.07 + 0 + 0 MODIFY_CNF 914 BEGIN : [Thu Jun 1 15:36:03 2006] MODIFY_CNF 914 END : 23193290 bytes (0 seconds) [Thu Jun 1 15:36:03 2006] MODIFY_CNF 914 CPU : 0.0100000000000051 = 0.0100000000000051 + 0 + 0 + 0 VERIFY_CNF 914 BEGIN : [Thu Jun 1 15:36:03 2006] CMD : minisat /work/tamura/csp2sat98504.cnf /work/tamura/csp2sat98504.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 836262 2458514 | 278754 0 0 NaNQ | 0.000 % | ==============================================================================) restarts : 1 conflicts : 15 (15 /sec) decisions : 197 (203 /sec) propagations : 117668 (121368 /sec) inspects : 1188510 (1225885 /sec) conflict literals : 138 (21.59 % deleted) CPU time : 0.969512 s SATISFIABLE VERIFY_CNF 914 END : (1 seconds) [Thu Jun 1 15:36:04 2006] VERIFY_CNF 914 CPU : 1.39 = 0 + 0 + 1.37 + 0.02 # RESULT : makespan 914 SATISFIABLE SHOW_RESULT 914 BEGIN : [Thu Jun 1 15:36:04 2006] # ASSIGN : makespan 914 # ASSIGN : s_0_0 112 # ASSIGN : s_0_1 204 # ASSIGN : s_0_2 298 # ASSIGN : s_0_3 310 # ASSIGN : s_0_4 414 # ASSIGN : s_1_0 36 # ASSIGN : s_1_1 103 # ASSIGN : s_1_2 122 # ASSIGN : s_1_3 209 # ASSIGN : s_1_4 848 # ASSIGN : s_2_0 16 # ASSIGN : s_2_1 30 # ASSIGN : s_2_2 47 # ASSIGN : s_2_3 140 # ASSIGN : s_2_4 540 # ASSIGN : s_3_0 57 # ASSIGN : s_3_1 156 # ASSIGN : s_3_2 229 # ASSIGN : s_3_3 238 # ASSIGN : s_3_4 315 # ASSIGN : s_4_0 2 # ASSIGN : s_4_1 51 # ASSIGN : s_4_2 413 # ASSIGN : s_4_3 421 # ASSIGN : s_4_4 899 # ASSIGN : s_5_0 222 # ASSIGN : s_5_1 419 # ASSIGN : s_5_2 496 # ASSIGN : s_5_3 516 # ASSIGN : s_5_4 658 # ASSIGN : s_6_0 401 # ASSIGN : s_6_1 512 # ASSIGN : s_6_2 583 # ASSIGN : s_6_3 664 # ASSIGN : s_6_4 775 # ASSIGN : s_7_0 43 # ASSIGN : s_7_1 152 # ASSIGN : s_7_2 236 # ASSIGN : s_7_3 322 # ASSIGN : s_7_4 410 # ASSIGN : s_8_0 322 # ASSIGN : s_8_1 412 # ASSIGN : s_8_2 508 # ASSIGN : s_8_3 560 # ASSIGN : s_8_4 770 # ASSIGN : s_9_0 517 # ASSIGN : s_9_1 621 # ASSIGN : s_9_2 675 # ASSIGN : s_9_3 734 # ASSIGN : s_9_4 822 # ASSIGN : s_10_0 371 # ASSIGN : s_10_1 466 # ASSIGN : s_10_2 522 # ASSIGN : s_10_3 838 # ASSIGN : s_10_4 891 # ASSIGN : s_11_0 474 # ASSIGN : s_11_1 600 # ASSIGN : s_11_2 678 # ASSIGN : s_11_3 769 # ASSIGN : s_11_4 837 # ASSIGN : s_12_0 2 # ASSIGN : s_12_1 220 # ASSIGN : s_12_2 672 # ASSIGN : s_12_3 866 # ASSIGN : s_12_4 908 # ASSIGN : s_13_0 539 # ASSIGN : s_13_1 569 # ASSIGN : s_13_2 635 # ASSIGN : s_13_3 724 # ASSIGN : s_13_4 849 # ASSIGN : s_14_0 401 # ASSIGN : s_14_1 512 # ASSIGN : s_14_2 599 # ASSIGN : s_14_3 752 # ASSIGN : s_14_4 760 SHOW_RESULT 914 END : 914 (0 seconds) [Thu Jun 1 15:36:04 2006] SHOW_RESULT 914 CPU : 0.209999999999994 = 0.209999999999994 + 0 + 0 + 0 # BOUND : makespan 863 914 MODIFY_CNF 888 BEGIN : [Thu Jun 1 15:36:04 2006] MODIFY_CNF 888 END : 23193290 bytes (0 seconds) [Thu Jun 1 15:36:04 2006] MODIFY_CNF 888 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 888 BEGIN : [Thu Jun 1 15:36:04 2006] CMD : minisat /work/tamura/csp2sat98504.cnf /work/tamura/csp2sat98504.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 806986 2372662 | 268995 0 0 NaNQ | 0.000 % | | 100 | 806986 2372662 | 295894 100 1256 12.6 | 34.241 % | ==============================================================================) restarts : 2 conflicts : 105 (89 /sec) decisions : 315 (266 /sec) propagations : 463287 (391764 /sec) inspects : 5110430 (4321476 /sec) conflict literals : 1313 (22.58 % deleted) CPU time : 1.18257 s SATISFIABLE VERIFY_CNF 888 END : (2 seconds) [Thu Jun 1 15:36:06 2006] VERIFY_CNF 888 CPU : 1.7 = 0 + 0.00999999999999995 + 1.66 + 0.03 # RESULT : makespan 888 SATISFIABLE SHOW_RESULT 888 BEGIN : [Thu Jun 1 15:36:06 2006] # ASSIGN : makespan 888 # ASSIGN : s_0_0 73 # ASSIGN : s_0_1 206 # ASSIGN : s_0_2 300 # ASSIGN : s_0_3 312 # ASSIGN : s_0_4 422 # ASSIGN : s_1_0 56 # ASSIGN : s_1_1 194 # ASSIGN : s_1_2 213 # ASSIGN : s_1_3 547 # ASSIGN : s_1_4 558 # ASSIGN : s_2_0 2 # ASSIGN : s_2_1 16 # ASSIGN : s_2_2 29 # ASSIGN : s_2_3 110 # ASSIGN : s_2_4 310 # ASSIGN : s_3_0 382 # ASSIGN : s_3_1 731 # ASSIGN : s_3_2 797 # ASSIGN : s_3_3 804 # ASSIGN : s_3_4 881 # ASSIGN : s_4_0 77 # ASSIGN : s_4_1 126 # ASSIGN : s_4_2 344 # ASSIGN : s_4_3 377 # ASSIGN : s_4_4 547 # ASSIGN : s_5_0 22 # ASSIGN : s_5_1 380 # ASSIGN : s_5_2 568 # ASSIGN : s_5_3 605 # ASSIGN : s_5_4 812 # ASSIGN : s_6_0 215 # ASSIGN : s_6_1 350 # ASSIGN : s_6_2 377 # ASSIGN : s_6_3 429 # ASSIGN : s_6_4 749 # ASSIGN : s_7_0 261 # ASSIGN : s_7_1 330 # ASSIGN : s_7_2 455 # ASSIGN : s_7_3 517 # ASSIGN : s_7_4 633 # ASSIGN : s_8_0 457 # ASSIGN : s_8_1 562 # ASSIGN : s_8_2 624 # ASSIGN : s_8_3 668 # ASSIGN : s_8_4 729 # ASSIGN : s_9_0 553 # ASSIGN : s_9_1 588 # ASSIGN : s_9_2 642 # ASSIGN : s_9_3 701 # ASSIGN : s_9_4 789 # ASSIGN : s_10_0 149 # ASSIGN : s_10_1 327 # ASSIGN : s_10_2 475 # ASSIGN : s_10_3 795 # ASSIGN : s_10_4 848 # ASSIGN : s_11_0 339 # ASSIGN : s_11_1 403 # ASSIGN : s_11_2 477 # ASSIGN : s_11_3 574 # ASSIGN : s_11_4 658 # ASSIGN : s_12_0 104 # ASSIGN : s_12_1 165 # ASSIGN : s_12_2 260 # ASSIGN : s_12_3 823 # ASSIGN : s_12_4 882 # ASSIGN : s_13_0 43 # ASSIGN : s_13_1 124 # ASSIGN : s_13_2 190 # ASSIGN : s_13_3 224 # ASSIGN : s_13_4 871 # ASSIGN : s_14_0 111 # ASSIGN : s_14_1 630 # ASSIGN : s_14_2 705 # ASSIGN : s_14_3 781 # ASSIGN : s_14_4 800 SHOW_RESULT 888 END : 888 (0 seconds) [Thu Jun 1 15:36:06 2006] SHOW_RESULT 888 CPU : 0.200000000000003 = 0.200000000000003 + 0 + 0 + 0 # BOUND : makespan 863 888 MODIFY_CNF 875 BEGIN : [Thu Jun 1 15:36:06 2006] MODIFY_CNF 875 END : 23193290 bytes (0 seconds) [Thu Jun 1 15:36:06 2006] MODIFY_CNF 875 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 875 BEGIN : [Thu Jun 1 15:36:06 2006] CMD : minisat /work/tamura/csp2sat98504.cnf /work/tamura/csp2sat98504.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 792348 2329736 | 264116 0 0 NaNQ | 0.000 % | ==============================================================================) restarts : 1 conflicts : 6 (6 /sec) decisions : 158 (159 /sec) propagations : 97132 (97817 /sec) inspects : 945425 (952091 /sec) conflict literals : 56 (20.00 % deleted) CPU time : 0.992999 s SATISFIABLE VERIFY_CNF 875 END : (2 seconds) [Thu Jun 1 15:36:08 2006] VERIFY_CNF 875 CPU : 1.5 = 0.00999999999999801 + 0 + 1.4 + 0.09 # RESULT : makespan 875 SATISFIABLE SHOW_RESULT 875 BEGIN : [Thu Jun 1 15:36:08 2006] # ASSIGN : makespan 875 # ASSIGN : s_0_0 82 # ASSIGN : s_0_1 174 # ASSIGN : s_0_2 268 # ASSIGN : s_0_3 280 # ASSIGN : s_0_4 376 # ASSIGN : s_1_0 4 # ASSIGN : s_1_1 25 # ASSIGN : s_1_2 44 # ASSIGN : s_1_3 178 # ASSIGN : s_1_4 189 # ASSIGN : s_2_0 55 # ASSIGN : s_2_1 69 # ASSIGN : s_2_2 131 # ASSIGN : s_2_3 264 # ASSIGN : s_2_4 364 # ASSIGN : s_3_0 269 # ASSIGN : s_3_1 633 # ASSIGN : s_3_2 708 # ASSIGN : s_3_3 715 # ASSIGN : s_3_4 792 # ASSIGN : s_4_0 66 # ASSIGN : s_4_1 100 # ASSIGN : s_4_2 200 # ASSIGN : s_4_3 238 # ASSIGN : s_4_4 295 # ASSIGN : s_5_0 12 # ASSIGN : s_5_1 206 # ASSIGN : s_5_2 384 # ASSIGN : s_5_3 433 # ASSIGN : s_5_4 799 # ASSIGN : s_6_0 255 # ASSIGN : s_6_1 283 # ASSIGN : s_6_2 310 # ASSIGN : s_6_3 486 # ASSIGN : s_6_4 736 # ASSIGN : s_7_0 0 # ASSIGN : s_7_1 122 # ASSIGN : s_7_2 206 # ASSIGN : s_7_3 283 # ASSIGN : s_7_4 371 # ASSIGN : s_8_0 317 # ASSIGN : s_8_1 407 # ASSIGN : s_8_2 469 # ASSIGN : s_8_3 572 # ASSIGN : s_8_4 640 # ASSIGN : s_9_0 478 # ASSIGN : s_9_1 499 # ASSIGN : s_9_2 553 # ASSIGN : s_9_3 612 # ASSIGN : s_9_4 700 # ASSIGN : s_10_0 3 # ASSIGN : s_10_1 383 # ASSIGN : s_10_2 483 # ASSIGN : s_10_3 799 # ASSIGN : s_10_4 852 # ASSIGN : s_11_0 503 # ASSIGN : s_11_1 561 # ASSIGN : s_11_2 633 # ASSIGN : s_11_3 724 # ASSIGN : s_11_4 798 # ASSIGN : s_12_0 362 # ASSIGN : s_12_1 428 # ASSIGN : s_12_2 699 # ASSIGN : s_12_3 810 # ASSIGN : s_12_4 869 # ASSIGN : s_13_0 523 # ASSIGN : s_13_1 574 # ASSIGN : s_13_2 728 # ASSIGN : s_13_3 751 # ASSIGN : s_13_4 835 # ASSIGN : s_14_0 404 # ASSIGN : s_14_1 541 # ASSIGN : s_14_2 616 # ASSIGN : s_14_3 692 # ASSIGN : s_14_4 787 SHOW_RESULT 875 END : 875 (0 seconds) [Thu Jun 1 15:36:08 2006] SHOW_RESULT 875 CPU : 0.200000000000003 = 0.200000000000003 + 0 + 0 + 0 # BOUND : makespan 863 875 MODIFY_CNF 869 BEGIN : [Thu Jun 1 15:36:08 2006] MODIFY_CNF 869 END : 23193289 bytes (0 seconds) [Thu Jun 1 15:36:08 2006] MODIFY_CNF 869 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 869 BEGIN : [Thu Jun 1 15:36:08 2006] CMD : minisat /work/tamura/csp2sat98504.cnf /work/tamura/csp2sat98504.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 785592 2309924 | 261864 0 0 NaNQ | 0.000 % | ==============================================================================) restarts : 1 conflicts : 95 (84 /sec) decisions : 325 (288 /sec) propagations : 365681 (324312 /sec) inspects : 3982964 (3532374 /sec) conflict literals : 1091 (19.84 % deleted) CPU time : 1.12756 s SATISFIABLE VERIFY_CNF 869 END : (2 seconds) [Thu Jun 1 15:36:10 2006] VERIFY_CNF 869 CPU : 1.55 = 0.00999999999999801 + 0.01 + 1.51 + 0.02 # RESULT : makespan 869 SATISFIABLE SHOW_RESULT 869 BEGIN : [Thu Jun 1 15:36:10 2006] # ASSIGN : makespan 869 # ASSIGN : s_0_0 99 # ASSIGN : s_0_1 274 # ASSIGN : s_0_2 590 # ASSIGN : s_0_3 602 # ASSIGN : s_0_4 762 # ASSIGN : s_1_0 39 # ASSIGN : s_1_1 84 # ASSIGN : s_1_2 103 # ASSIGN : s_1_3 197 # ASSIGN : s_1_4 208 # ASSIGN : s_2_0 1 # ASSIGN : s_2_1 15 # ASSIGN : s_2_2 28 # ASSIGN : s_2_3 183 # ASSIGN : s_2_4 368 # ASSIGN : s_3_0 179 # ASSIGN : s_3_1 274 # ASSIGN : s_3_2 344 # ASSIGN : s_3_3 685 # ASSIGN : s_3_4 862 # ASSIGN : s_4_0 60 # ASSIGN : s_4_1 94 # ASSIGN : s_4_2 191 # ASSIGN : s_4_3 207 # ASSIGN : s_4_4 854 # ASSIGN : s_5_0 6 # ASSIGN : s_5_1 309 # ASSIGN : s_5_2 388 # ASSIGN : s_5_3 426 # ASSIGN : s_5_4 646 # ASSIGN : s_6_0 199 # ASSIGN : s_6_1 386 # ASSIGN : s_6_2 413 # ASSIGN : s_6_3 479 # ASSIGN : s_6_4 730 # ASSIGN : s_7_0 30 # ASSIGN : s_7_1 127 # ASSIGN : s_7_2 190 # ASSIGN : s_7_3 252 # ASSIGN : s_7_4 340 # ASSIGN : s_8_0 219 # ASSIGN : s_8_1 351 # ASSIGN : s_8_2 438 # ASSIGN : s_8_3 503 # ASSIGN : s_8_4 567 # ASSIGN : s_9_0 447 # ASSIGN : s_9_1 564 # ASSIGN : s_9_2 650 # ASSIGN : s_9_3 760 # ASSIGN : s_9_4 848 # ASSIGN : s_10_0 303 # ASSIGN : s_10_1 376 # ASSIGN : s_10_2 452 # ASSIGN : s_10_3 793 # ASSIGN : s_10_4 846 # ASSIGN : s_11_0 465 # ASSIGN : s_11_1 530 # ASSIGN : s_11_2 618 # ASSIGN : s_11_3 709 # ASSIGN : s_11_4 777 # ASSIGN : s_12_0 258 # ASSIGN : s_12_1 449 # ASSIGN : s_12_2 693 # ASSIGN : s_12_3 804 # ASSIGN : s_12_4 863 # ASSIGN : s_13_0 544 # ASSIGN : s_13_1 619 # ASSIGN : s_13_2 722 # ASSIGN : s_13_3 745 # ASSIGN : s_13_4 829 # ASSIGN : s_14_0 408 # ASSIGN : s_14_1 503 # ASSIGN : s_14_2 574 # ASSIGN : s_14_3 769 # ASSIGN : s_14_4 781 SHOW_RESULT 869 END : 869 (0 seconds) [Thu Jun 1 15:36:10 2006] SHOW_RESULT 869 CPU : 0.200000000000003 = 0.200000000000003 + 0 + 0 + 0 # BOUND : makespan 863 869 MODIFY_CNF 866 BEGIN : [Thu Jun 1 15:36:10 2006] MODIFY_CNF 866 END : 23193289 bytes (0 seconds) [Thu Jun 1 15:36:10 2006] MODIFY_CNF 866 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 866 BEGIN : [Thu Jun 1 15:36:10 2006] CMD : minisat /work/tamura/csp2sat98504.cnf /work/tamura/csp2sat98504.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 782214 2300018 | 260738 0 0 NaNQ | 0.000 % | | 100 | 782214 2300018 | 286811 100 1068 10.7 | 36.505 % | | 251 | 782214 2300018 | 315492 251 4410 17.6 | 36.505 % | | 476 | 782214 2300018 | 347042 476 11424 24.0 | 36.505 % | | 813 | 782214 2300018 | 381746 813 15407 19.0 | 36.505 % | ==============================================================================) restarts : 5 conflicts : 975 (413 /sec) decisions : 1779 (753 /sec) propagations : 2586951 (1094987 /sec) inspects : 31843997 (13478707 /sec) conflict literals : 19284 (13.38 % deleted) CPU time : 2.36254 s SATISFIABLE VERIFY_CNF 866 END : (3 seconds) [Thu Jun 1 15:36:13 2006] VERIFY_CNF 866 CPU : 2.86 = 0 + 0 + 2.77 + 0.09 # RESULT : makespan 866 SATISFIABLE SHOW_RESULT 866 BEGIN : [Thu Jun 1 15:36:13 2006] # ASSIGN : makespan 866 # ASSIGN : s_0_0 1 # ASSIGN : s_0_1 95 # ASSIGN : s_0_2 229 # ASSIGN : s_0_3 255 # ASSIGN : s_0_4 807 # ASSIGN : s_1_0 314 # ASSIGN : s_1_1 447 # ASSIGN : s_1_2 564 # ASSIGN : s_1_3 651 # ASSIGN : s_1_4 667 # ASSIGN : s_2_0 276 # ASSIGN : s_2_1 290 # ASSIGN : s_2_2 303 # ASSIGN : s_2_3 599 # ASSIGN : s_2_4 677 # ASSIGN : s_3_0 0 # ASSIGN : s_3_1 346 # ASSIGN : s_3_2 474 # ASSIGN : s_3_3 481 # ASSIGN : s_3_4 859 # ASSIGN : s_4_0 430 # ASSIGN : s_4_1 510 # ASSIGN : s_4_2 662 # ASSIGN : s_4_3 677 # ASSIGN : s_4_4 775 # ASSIGN : s_5_0 17 # ASSIGN : s_5_1 373 # ASSIGN : s_5_2 538 # ASSIGN : s_5_3 558 # ASSIGN : s_5_4 790 # ASSIGN : s_6_0 3 # ASSIGN : s_6_1 93 # ASSIGN : s_6_2 132 # ASSIGN : s_6_3 188 # ASSIGN : s_6_4 464 # ASSIGN : s_7_0 120 # ASSIGN : s_7_1 189 # ASSIGN : s_7_2 241 # ASSIGN : s_7_3 324 # ASSIGN : s_7_4 412 # ASSIGN : s_8_0 200 # ASSIGN : s_8_1 657 # ASSIGN : s_8_2 733 # ASSIGN : s_8_3 753 # ASSIGN : s_8_4 814 # ASSIGN : s_9_0 12 # ASSIGN : s_9_1 260 # ASSIGN : s_9_2 314 # ASSIGN : s_9_3 378 # ASSIGN : s_9_4 466 # ASSIGN : s_10_0 26 # ASSIGN : s_10_1 127 # ASSIGN : s_10_2 177 # ASSIGN : s_10_3 790 # ASSIGN : s_10_4 843 # ASSIGN : s_11_0 67 # ASSIGN : s_11_1 105 # ASSIGN : s_11_2 577 # ASSIGN : s_11_3 668 # ASSIGN : s_11_4 736 # ASSIGN : s_12_0 184 # ASSIGN : s_12_1 450 # ASSIGN : s_12_2 615 # ASSIGN : s_12_3 697 # ASSIGN : s_12_4 722 # ASSIGN : s_13_0 545 # ASSIGN : s_13_1 611 # ASSIGN : s_13_2 719 # ASSIGN : s_13_3 742 # ASSIGN : s_13_4 826 # ASSIGN : s_14_0 335 # ASSIGN : s_14_1 493 # ASSIGN : s_14_2 575 # ASSIGN : s_14_3 728 # ASSIGN : s_14_4 778 SHOW_RESULT 866 END : 866 (0 seconds) [Thu Jun 1 15:36:13 2006] SHOW_RESULT 866 CPU : 0.209999999999996 = 0.199999999999996 + 0.01 + 0 + 0 # BOUND : makespan 863 866 MODIFY_CNF 864 BEGIN : [Thu Jun 1 15:36:13 2006] MODIFY_CNF 864 END : 23193289 bytes (0 seconds) [Thu Jun 1 15:36:13 2006] MODIFY_CNF 864 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 864 BEGIN : [Thu Jun 1 15:36:13 2006] CMD : minisat /work/tamura/csp2sat98504.cnf /work/tamura/csp2sat98504.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 779962 2293414 | 259987 0 0 NaNQ | 0.000 % | ==============================================================================) restarts : 1 conflicts : 73 (65 /sec) decisions : 297 (266 /sec) propagations : 315880 (282747 /sec) inspects : 3356112 (3004087 /sec) conflict literals : 697 (24.32 % deleted) CPU time : 1.11718 s SATISFIABLE VERIFY_CNF 864 END : (2 seconds) [Thu Jun 1 15:36:15 2006] VERIFY_CNF 864 CPU : 1.63 = 0 + 0 + 1.54 + 0.09 # RESULT : makespan 864 SATISFIABLE SHOW_RESULT 864 BEGIN : [Thu Jun 1 15:36:15 2006] # ASSIGN : makespan 864 # ASSIGN : s_0_0 71 # ASSIGN : s_0_1 266 # ASSIGN : s_0_2 601 # ASSIGN : s_0_3 685 # ASSIGN : s_0_4 780 # ASSIGN : s_1_0 33 # ASSIGN : s_1_1 54 # ASSIGN : s_1_2 73 # ASSIGN : s_1_3 163 # ASSIGN : s_1_4 178 # ASSIGN : s_2_0 158 # ASSIGN : s_2_1 174 # ASSIGN : s_2_2 233 # ASSIGN : s_2_3 408 # ASSIGN : s_2_4 614 # ASSIGN : s_3_0 149 # ASSIGN : s_3_1 244 # ASSIGN : s_3_2 462 # ASSIGN : s_3_3 588 # ASSIGN : s_3_4 857 # ASSIGN : s_4_0 55 # ASSIGN : s_4_1 89 # ASSIGN : s_4_2 277 # ASSIGN : s_4_3 343 # ASSIGN : s_4_4 849 # ASSIGN : s_5_0 1 # ASSIGN : s_5_1 283 # ASSIGN : s_5_2 360 # ASSIGN : s_5_3 388 # ASSIGN : s_5_4 773 # ASSIGN : s_6_0 424 # ASSIGN : s_6_1 510 # ASSIGN : s_6_2 613 # ASSIGN : s_6_3 665 # ASSIGN : s_6_4 773 # ASSIGN : s_7_0 2 # ASSIGN : s_7_1 97 # ASSIGN : s_7_2 160 # ASSIGN : s_7_3 222 # ASSIGN : s_7_4 310 # ASSIGN : s_8_0 187 # ASSIGN : s_8_1 308 # ASSIGN : s_8_2 433 # ASSIGN : s_8_3 475 # ASSIGN : s_8_4 536 # ASSIGN : s_9_0 442 # ASSIGN : s_9_1 536 # ASSIGN : s_9_2 590 # ASSIGN : s_9_3 665 # ASSIGN : s_9_4 753 # ASSIGN : s_10_0 32 # ASSIGN : s_10_1 172 # ASSIGN : s_10_2 447 # ASSIGN : s_10_3 537 # ASSIGN : s_10_4 725 # ASSIGN : s_11_0 469 # ASSIGN : s_11_1 525 # ASSIGN : s_11_2 634 # ASSIGN : s_11_3 725 # ASSIGN : s_11_4 793 # ASSIGN : s_12_0 370 # ASSIGN : s_12_1 415 # ASSIGN : s_12_2 597 # ASSIGN : s_12_3 748 # ASSIGN : s_12_4 787 # ASSIGN : s_13_0 385 # ASSIGN : s_13_1 441 # ASSIGN : s_13_2 507 # ASSIGN : s_13_3 649 # ASSIGN : s_13_4 847 # ASSIGN : s_14_0 380 # ASSIGN : s_14_1 530 # ASSIGN : s_14_2 649 # ASSIGN : s_14_3 768 # ASSIGN : s_14_4 776 SHOW_RESULT 864 END : 864 (0 seconds) [Thu Jun 1 15:36:15 2006] SHOW_RESULT 864 CPU : 0.210000000000001 = 0.210000000000001 + 0 + 0 + 0 # BOUND : makespan 863 864 MODIFY_CNF 863 BEGIN : [Thu Jun 1 15:36:15 2006] MODIFY_CNF 863 END : 23193289 bytes (0 seconds) [Thu Jun 1 15:36:15 2006] MODIFY_CNF 863 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 863 BEGIN : [Thu Jun 1 15:36:15 2006] CMD : minisat /work/tamura/csp2sat98504.cnf /work/tamura/csp2sat98504.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 778837 2290114 | 259612 0 0 NaNQ | 0.000 % | ==============================================================================) restarts : 1 conflicts : 61 (56 /sec) decisions : 315 (288 /sec) propagations : 265249 (242200 /sec) inspects : 2894997 (2643435 /sec) conflict literals : 669 (25.25 % deleted) CPU time : 1.09516 s SATISFIABLE VERIFY_CNF 863 END : (1 seconds) [Thu Jun 1 15:36:16 2006] VERIFY_CNF 863 CPU : 1.56 = 0 + 0.01 + 1.46 + 0.09 # RESULT : makespan 863 SATISFIABLE SHOW_RESULT 863 BEGIN : [Thu Jun 1 15:36:16 2006] # ASSIGN : makespan 863 # ASSIGN : s_0_0 283 # ASSIGN : s_0_1 375 # ASSIGN : s_0_2 637 # ASSIGN : s_0_3 684 # ASSIGN : s_0_4 779 # ASSIGN : s_1_0 22 # ASSIGN : s_1_1 43 # ASSIGN : s_1_2 69 # ASSIGN : s_1_3 166 # ASSIGN : s_1_4 177 # ASSIGN : s_2_0 62 # ASSIGN : s_2_1 76 # ASSIGN : s_2_2 218 # ASSIGN : s_2_3 309 # ASSIGN : s_2_4 608 # ASSIGN : s_3_0 148 # ASSIGN : s_3_1 243 # ASSIGN : s_3_2 484 # ASSIGN : s_3_3 587 # ASSIGN : s_3_4 856 # ASSIGN : s_4_0 54 # ASSIGN : s_4_1 88 # ASSIGN : s_4_2 187 # ASSIGN : s_4_3 201 # ASSIGN : s_4_4 649 # ASSIGN : s_5_0 0 # ASSIGN : s_5_1 89 # ASSIGN : s_5_2 260 # ASSIGN : s_5_3 343 # ASSIGN : s_5_4 787 # ASSIGN : s_6_0 325 # ASSIGN : s_6_1 412 # ASSIGN : s_6_2 491 # ASSIGN : s_6_3 664 # ASSIGN : s_6_4 766 # ASSIGN : s_7_0 7 # ASSIGN : s_7_1 96 # ASSIGN : s_7_2 156 # ASSIGN : s_7_3 246 # ASSIGN : s_7_4 334 # ASSIGN : s_8_0 193 # ASSIGN : s_8_1 293 # ASSIGN : s_8_2 432 # ASSIGN : s_8_3 469 # ASSIGN : s_8_4 535 # ASSIGN : s_9_0 441 # ASSIGN : s_9_1 530 # ASSIGN : s_9_2 584 # ASSIGN : s_9_3 664 # ASSIGN : s_9_4 752 # ASSIGN : s_10_0 355 # ASSIGN : s_10_1 396 # ASSIGN : s_10_2 446 # ASSIGN : s_10_3 787 # ASSIGN : s_10_4 840 # ASSIGN : s_11_0 401 # ASSIGN : s_11_1 524 # ASSIGN : s_11_2 628 # ASSIGN : s_11_3 719 # ASSIGN : s_11_4 792 # ASSIGN : s_12_0 439 # ASSIGN : s_12_1 489 # ASSIGN : s_12_2 596 # ASSIGN : s_12_3 724 # ASSIGN : s_12_4 786 # ASSIGN : s_13_0 439 # ASSIGN : s_13_1 469 # ASSIGN : s_13_2 543 # ASSIGN : s_13_3 648 # ASSIGN : s_13_4 749 # ASSIGN : s_14_0 280 # ASSIGN : s_14_1 566 # ASSIGN : s_14_2 643 # ASSIGN : s_14_3 767 # ASSIGN : s_14_4 775 SHOW_RESULT 863 END : 863 (1 seconds) [Thu Jun 1 15:36:17 2006] SHOW_RESULT 863 CPU : 0.199999999999996 = 0.199999999999996 + 0 + 0 + 0 # BOUND : makespan 863 863 MAIN END : (69 seconds) [Thu Jun 1 15:36:17 2006] MAIN CPU : 68.38 = 56.13 + 0.11 + 11.71 + 0.43