# TIMEOUT 18000 MAIN BEGIN : [Mon Jun 19 14:04:25 2006] READ BEGIN : csp/tai_15x15_8.csp [Mon Jun 19 14:04:25 2006] READ END : csp/tai_15x15_8.csp (7 seconds) [Mon Jun 19 14:04:32 2006] READ CPU : 6.35 = 6.3 + 0.05 + 0 + 0 # BOUND : makespan 893 1386 GENERATE_CNF 1386 BEGIN : [Mon Jun 19 14:04:32 2006] GENERATE_CNF 1386 END : 319320 variables 8866998 clauses 212603891 bytes (340 seconds) [Mon Jun 19 14:10:12 2006] GENERATE_CNF 1386 CPU : 338.66 = 337.38 + 1.28 + 0 + 0 MODIFY_CNF 1139 BEGIN : [Mon Jun 19 14:10:12 2006] MODIFY_CNF 1139 END : 212603897 bytes (0 seconds) [Mon Jun 19 14:10:12 2006] MODIFY_CNF 1139 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1139 BEGIN : [Mon Jun 19 14:10:12 2006] CMD : minisat /tmp/csp2sat31997.cnf /tmp/csp2sat31997.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 7303018 21601667 | 2434339 0 0 nan | 0.000 % | | 100 | 7303018 21601667 | 2677772 100 3741 37.4 | 21.104 % | ============================================================================== restarts : 2 conflicts : 153 (9 /sec) decisions : 2793 (163 /sec) propagations : 1588438 (92512 /sec) conflict literals : 4802 (4.55 % deleted) Memory used : 360.14 MB CPU time : 17.17 s SATISFIABLE VERIFY_CNF 1139 END : (18 seconds) [Mon Jun 19 14:10:30 2006] VERIFY_CNF 1139 CPU : 18.47 = 0 + 0 + 17.34 + 1.13 # RESULT : makespan 1139 SATISFIABLE SHOW_RESULT 1139 BEGIN : [Mon Jun 19 14:10:30 2006] # ASSIGN : makespan 1139 # ASSIGN : s_0_0 922 # ASSIGN : s_0_1 556 # ASSIGN : s_0_2 488 # ASSIGN : s_0_3 658 # ASSIGN : s_0_4 237 # ASSIGN : s_0_5 413 # ASSIGN : s_0_6 1005 # ASSIGN : s_0_7 271 # ASSIGN : s_0_8 1127 # ASSIGN : s_0_9 1097 # ASSIGN : s_0_10 711 # ASSIGN : s_0_11 830 # ASSIGN : s_0_12 434 # ASSIGN : s_0_13 655 # ASSIGN : s_0_14 757 # ASSIGN : s_1_0 57 # ASSIGN : s_1_1 404 # ASSIGN : s_1_2 214 # ASSIGN : s_1_3 522 # ASSIGN : s_1_4 170 # ASSIGN : s_1_5 657 # ASSIGN : s_1_6 851 # ASSIGN : s_1_7 310 # ASSIGN : s_1_8 1077 # ASSIGN : s_1_9 947 # ASSIGN : s_1_10 592 # ASSIGN : s_1_11 978 # ASSIGN : s_1_12 529 # ASSIGN : s_1_13 706 # ASSIGN : s_1_14 519 # ASSIGN : s_2_0 173 # ASSIGN : s_2_1 1138 # ASSIGN : s_2_2 701 # ASSIGN : s_2_3 314 # ASSIGN : s_2_4 486 # ASSIGN : s_2_5 236 # ASSIGN : s_2_6 760 # ASSIGN : s_2_7 402 # ASSIGN : s_2_8 1001 # ASSIGN : s_2_9 836 # ASSIGN : s_2_10 913 # ASSIGN : s_2_11 646 # ASSIGN : s_2_12 1130 # ASSIGN : s_2_13 572 # ASSIGN : s_2_14 457 # ASSIGN : s_3_0 492 # ASSIGN : s_3_1 615 # ASSIGN : s_3_2 846 # ASSIGN : s_3_3 1004 # ASSIGN : s_3_4 1056 # ASSIGN : s_3_5 554 # ASSIGN : s_3_6 703 # ASSIGN : s_3_7 210 # ASSIGN : s_3_8 985 # ASSIGN : s_3_9 790 # ASSIGN : s_3_10 850 # ASSIGN : s_3_11 927 # ASSIGN : s_3_12 1089 # ASSIGN : s_3_13 249 # ASSIGN : s_3_14 359 # ASSIGN : s_4_0 125 # ASSIGN : s_4_1 181 # ASSIGN : s_4_2 796 # ASSIGN : s_4_3 610 # ASSIGN : s_4_4 403 # ASSIGN : s_4_5 540 # ASSIGN : s_4_6 618 # ASSIGN : s_4_7 280 # ASSIGN : s_4_8 833 # ASSIGN : s_4_9 714 # ASSIGN : s_4_10 803 # ASSIGN : s_4_11 706 # ASSIGN : s_4_12 1000 # ASSIGN : s_4_13 1083 # ASSIGN : s_4_14 912 # ASSIGN : s_5_0 317 # ASSIGN : s_5_1 475 # ASSIGN : s_5_2 1056 # ASSIGN : s_5_3 551 # ASSIGN : s_5_4 652 # ASSIGN : s_5_5 454 # ASSIGN : s_5_6 607 # ASSIGN : s_5_7 724 # ASSIGN : s_5_8 791 # ASSIGN : s_5_9 713 # ASSIGN : s_5_10 621 # ASSIGN : s_5_11 912 # ASSIGN : s_5_12 939 # ASSIGN : s_5_13 999 # ASSIGN : s_5_14 880 # ASSIGN : s_6_0 404 # ASSIGN : s_6_1 353 # ASSIGN : s_6_2 15 # ASSIGN : s_6_3 18 # ASSIGN : s_6_4 985 # ASSIGN : s_6_5 1090 # ASSIGN : s_6_6 572 # ASSIGN : s_6_7 477 # ASSIGN : s_6_8 774 # ASSIGN : s_6_9 696 # ASSIGN : s_6_10 1009 # ASSIGN : s_6_11 716 # ASSIGN : s_6_12 845 # ASSIGN : s_6_13 949 # ASSIGN : s_6_14 827 # ASSIGN : s_7_0 776 # ASSIGN : s_7_1 1024 # ASSIGN : s_7_2 858 # ASSIGN : s_7_3 1069 # ASSIGN : s_7_4 936 # ASSIGN : s_7_5 71 # ASSIGN : s_7_6 510 # ASSIGN : s_7_7 606 # ASSIGN : s_7_8 769 # ASSIGN : s_7_9 690 # ASSIGN : s_7_10 188 # ASSIGN : s_7_11 138 # ASSIGN : s_7_12 832 # ASSIGN : s_7_13 800 # ASSIGN : s_7_14 707 # ASSIGN : s_8_0 1057 # ASSIGN : s_8_1 8 # ASSIGN : s_8_2 932 # ASSIGN : s_8_3 165 # ASSIGN : s_8_4 833 # ASSIGN : s_8_5 59 # ASSIGN : s_8_6 401 # ASSIGN : s_8_7 1015 # ASSIGN : s_8_8 693 # ASSIGN : s_8_9 668 # ASSIGN : s_8_10 287 # ASSIGN : s_8_11 390 # ASSIGN : s_8_12 799 # ASSIGN : s_8_13 769 # ASSIGN : s_8_14 627 # ASSIGN : s_9_0 1136 # ASSIGN : s_9_1 942 # ASSIGN : s_9_2 369 # ASSIGN : s_9_3 216 # ASSIGN : s_9_4 35 # ASSIGN : s_9_5 2 # ASSIGN : s_9_6 206 # ASSIGN : s_9_7 1066 # ASSIGN : s_9_8 668 # ASSIGN : s_9_9 638 # ASSIGN : s_9_10 127 # ASSIGN : s_9_11 444 # ASSIGN : s_9_12 766 # ASSIGN : s_9_13 745 # ASSIGN : s_9_14 529 # ASSIGN : s_10_0 260 # ASSIGN : s_10_1 989 # ASSIGN : s_10_2 152 # ASSIGN : s_10_3 77 # ASSIGN : s_10_4 122 # ASSIGN : s_10_5 202 # ASSIGN : s_10_6 1057 # ASSIGN : s_10_7 458 # ASSIGN : s_10_8 664 # ASSIGN : s_10_9 590 # ASSIGN : s_10_10 321 # ASSIGN : s_10_11 232 # ASSIGN : s_10_12 696 # ASSIGN : s_10_13 480 # ASSIGN : s_10_14 416 # ASSIGN : s_11_0 1029 # ASSIGN : s_11_1 717 # ASSIGN : s_11_2 190 # ASSIGN : s_11_3 824 # ASSIGN : s_11_4 1 # ASSIGN : s_11_5 77 # ASSIGN : s_11_6 920 # ASSIGN : s_11_7 69 # ASSIGN : s_11_8 606 # ASSIGN : s_11_9 495 # ASSIGN : s_11_10 4 # ASSIGN : s_11_11 208 # ASSIGN : s_11_12 341 # ASSIGN : s_11_13 396 # ASSIGN : s_11_14 256 # ASSIGN : s_12_0 975 # ASSIGN : s_12_1 76 # ASSIGN : s_12_2 595 # ASSIGN : s_12_3 102 # ASSIGN : s_12_4 194 # ASSIGN : s_12_5 294 # ASSIGN : s_12_6 467 # ASSIGN : s_12_7 835 # ASSIGN : s_12_8 575 # ASSIGN : s_12_9 408 # ASSIGN : s_12_10 1113 # ASSIGN : s_12_11 266 # ASSIGN : s_12_12 314 # ASSIGN : s_12_13 368 # ASSIGN : s_12_14 231 # ASSIGN : s_13_0 997 # ASSIGN : s_13_1 809 # ASSIGN : s_13_2 26 # ASSIGN : s_13_3 905 # ASSIGN : s_13_4 32 # ASSIGN : s_13_5 159 # ASSIGN : s_13_6 54 # ASSIGN : s_13_7 786 # ASSIGN : s_13_8 517 # ASSIGN : s_13_9 199 # ASSIGN : s_13_10 66 # ASSIGN : s_13_11 309 # ASSIGN : s_13_12 232 # ASSIGN : s_13_13 333 # ASSIGN : s_13_14 1082 # ASSIGN : s_14_0 854 # ASSIGN : s_14_1 1085 # ASSIGN : s_14_2 656 # ASSIGN : s_14_3 818 # ASSIGN : s_14_4 1131 # ASSIGN : s_14_5 722 # ASSIGN : s_14_6 837 # ASSIGN : s_14_7 927 # ASSIGN : s_14_8 171 # ASSIGN : s_14_9 26 # ASSIGN : s_14_10 775 # ASSIGN : s_14_11 87 # ASSIGN : s_14_12 89 # ASSIGN : s_14_13 270 # ASSIGN : s_14_14 987 SHOW_RESULT 1139 END : 1139 (1 seconds) [Mon Jun 19 14:10:31 2006] SHOW_RESULT 1139 CPU : 0.869999999999975 = 0.839999999999975 + 0.03 + 0 + 0 # BOUND : makespan 893 1139 MODIFY_CNF 1016 BEGIN : [Mon Jun 19 14:10:31 2006] MODIFY_CNF 1016 END : 212603897 bytes (0 seconds) [Mon Jun 19 14:10:31 2006] MODIFY_CNF 1016 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1016 BEGIN : [Mon Jun 19 14:10:31 2006] CMD : minisat /tmp/csp2sat31997.cnf /tmp/csp2sat31997.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 6528118 19276967 | 2176039 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 35 (2 /sec) decisions : 1343 (84 /sec) propagations : 563596 (35357 /sec) conflict literals : 1036 (3.90 % deleted) Memory used : 360.11 MB CPU time : 15.94 s SATISFIABLE VERIFY_CNF 1016 END : (18 seconds) [Mon Jun 19 14:10:49 2006] VERIFY_CNF 1016 CPU : 17.38 = 0 + 0.01 + 16.12 + 1.25 # RESULT : makespan 1016 SATISFIABLE SHOW_RESULT 1016 BEGIN : [Mon Jun 19 14:10:49 2006] # ASSIGN : makespan 1016 # ASSIGN : s_0_0 799 # ASSIGN : s_0_1 737 # ASSIGN : s_0_2 948 # ASSIGN : s_0_3 655 # ASSIGN : s_0_4 442 # ASSIGN : s_0_5 201 # ASSIGN : s_0_6 533 # ASSIGN : s_0_7 180 # ASSIGN : s_0_8 5 # ASSIGN : s_0_9 17 # ASSIGN : s_0_10 603 # ASSIGN : s_0_11 239 # ASSIGN : s_0_12 126 # ASSIGN : s_0_13 47 # ASSIGN : s_0_14 56 # ASSIGN : s_1_0 245 # ASSIGN : s_1_1 796 # ASSIGN : s_1_2 591 # ASSIGN : s_1_3 708 # ASSIGN : s_1_4 1 # ASSIGN : s_1_5 876 # ASSIGN : s_1_6 947 # ASSIGN : s_1_7 420 # ASSIGN : s_1_8 512 # ASSIGN : s_1_9 129 # ASSIGN : s_1_10 562 # ASSIGN : s_1_11 321 # ASSIGN : s_1_12 182 # ASSIGN : s_1_13 50 # ASSIGN : s_1_14 160 # ASSIGN : s_2_0 358 # ASSIGN : s_2_1 0 # ASSIGN : s_2_2 290 # ASSIGN : s_2_3 715 # ASSIGN : s_2_4 476 # ASSIGN : s_2_5 813 # ASSIGN : s_2_6 871 # ASSIGN : s_2_7 562 # ASSIGN : s_2_8 199 # ASSIGN : s_2_9 638 # ASSIGN : s_2_10 1 # ASSIGN : s_2_11 421 # ASSIGN : s_2_12 275 # ASSIGN : s_2_13 89 # ASSIGN : s_2_14 163 # ASSIGN : s_3_0 10 # ASSIGN : s_3_1 867 # ASSIGN : s_3_2 3 # ASSIGN : s_3_3 448 # ASSIGN : s_3_4 566 # ASSIGN : s_3_5 955 # ASSIGN : s_3_6 345 # ASSIGN : s_3_7 523 # ASSIGN : s_3_8 72 # ASSIGN : s_3_9 402 # ASSIGN : s_3_10 93 # ASSIGN : s_3_11 599 # ASSIGN : s_3_12 283 # ASSIGN : s_3_13 165 # ASSIGN : s_3_14 192 # ASSIGN : s_4_0 108 # ASSIGN : s_4_1 466 # ASSIGN : s_4_2 242 # ASSIGN : s_4_3 0 # ASSIGN : s_4_4 25 # ASSIGN : s_4_5 603 # ASSIGN : s_4_6 765 # ASSIGN : s_4_7 617 # ASSIGN : s_4_8 850 # ASSIGN : s_4_9 940 # ASSIGN : s_4_10 156 # ASSIGN : s_4_11 650 # ASSIGN : s_4_12 324 # ASSIGN : s_4_13 186 # ASSIGN : s_4_14 249 # ASSIGN : s_5_0 852 # ASSIGN : s_5_1 565 # ASSIGN : s_5_2 474 # ASSIGN : s_5_3 8 # ASSIGN : s_5_4 108 # ASSIGN : s_5_5 222 # ASSIGN : s_5_6 182 # ASSIGN : s_5_7 746 # ASSIGN : s_5_8 808 # ASSIGN : s_5_9 939 # ASSIGN : s_5_10 300 # ASSIGN : s_5_11 658 # ASSIGN : s_5_12 407 # ASSIGN : s_5_13 243 # ASSIGN : s_5_14 331 # ASSIGN : s_6_0 943 # ASSIGN : s_6_1 244 # ASSIGN : s_6_2 7 # ASSIGN : s_6_3 64 # ASSIGN : s_6_4 169 # ASSIGN : s_6_5 742 # ASSIGN : s_6_6 193 # ASSIGN : s_6_7 826 # ASSIGN : s_6_8 791 # ASSIGN : s_6_9 922 # ASSIGN : s_6_10 381 # ASSIGN : s_6_11 673 # ASSIGN : s_6_12 467 # ASSIGN : s_6_13 327 # ASSIGN : s_6_14 363 # ASSIGN : s_7_0 84 # ASSIGN : s_7_1 295 # ASSIGN : s_7_2 10 # ASSIGN : s_7_3 123 # ASSIGN : s_7_4 196 # ASSIGN : s_7_5 363 # ASSIGN : s_7_6 585 # ASSIGN : s_7_7 647 # ASSIGN : s_7_8 786 # ASSIGN : s_7_9 916 # ASSIGN : s_7_10 462 # ASSIGN : s_7_11 731 # ASSIGN : s_7_12 561 # ASSIGN : s_7_13 369 # ASSIGN : s_7_14 403 # ASSIGN : s_8_0 494 # ASSIGN : s_8_1 3 # ASSIGN : s_8_2 84 # ASSIGN : s_8_3 193 # ASSIGN : s_8_4 245 # ASSIGN : s_8_5 347 # ASSIGN : s_8_6 693 # ASSIGN : s_8_7 359 # ASSIGN : s_8_8 615 # ASSIGN : s_8_9 759 # ASSIGN : s_8_10 954 # ASSIGN : s_8_11 781 # ASSIGN : s_8_12 574 # ASSIGN : s_8_13 401 # ASSIGN : s_8_14 453 # ASSIGN : s_9_0 164 # ASSIGN : s_9_1 54 # ASSIGN : s_9_2 167 # ASSIGN : s_9_3 244 # ASSIGN : s_9_4 344 # ASSIGN : s_9_5 468 # ASSIGN : s_9_6 154 # ASSIGN : s_9_7 921 # ASSIGN : s_9_8 991 # ASSIGN : s_9_9 729 # ASSIGN : s_9_10 649 # ASSIGN : s_9_11 792 # ASSIGN : s_9_12 607 # ASSIGN : s_9_13 431 # ASSIGN : s_9_14 501 # ASSIGN : s_10_0 188 # ASSIGN : s_10_1 101 # ASSIGN : s_10_2 252 # ASSIGN : s_10_3 342 # ASSIGN : s_10_4 957 # ASSIGN : s_10_5 925 # ASSIGN : s_10_6 17 # ASSIGN : s_10_7 401 # ASSIGN : s_10_8 987 # ASSIGN : s_10_9 551 # ASSIGN : s_10_10 710 # ASSIGN : s_10_11 877 # ASSIGN : s_10_12 640 # ASSIGN : s_10_13 452 # ASSIGN : s_10_14 599 # ASSIGN : s_11_0 313 # ASSIGN : s_11_1 136 # ASSIGN : s_11_2 349 # ASSIGN : s_11_3 367 # ASSIGN : s_11_4 639 # ASSIGN : s_11_5 20 # ASSIGN : s_11_6 228 # ASSIGN : s_11_7 341 # ASSIGN : s_11_8 929 # ASSIGN : s_11_9 449 # ASSIGN : s_11_10 805 # ASSIGN : s_11_11 905 # ASSIGN : s_11_12 734 # ASSIGN : s_11_13 544 # ASSIGN : s_11_14 642 # ASSIGN : s_12_0 440 # ASSIGN : s_12_1 340 # ASSIGN : s_12_2 379 # ASSIGN : s_12_3 500 # ASSIGN : s_12_4 690 # ASSIGN : s_12_5 0 # ASSIGN : s_12_6 99 # ASSIGN : s_12_7 189 # ASSIGN : s_12_8 766 # ASSIGN : s_12_9 281 # ASSIGN : s_12_10 867 # ASSIGN : s_12_11 934 # ASSIGN : s_12_12 789 # ASSIGN : s_12_13 628 # ASSIGN : s_12_14 727 # ASSIGN : s_13_0 462 # ASSIGN : s_13_1 366 # ASSIGN : s_13_2 557 # ASSIGN : s_13_3 563 # ASSIGN : s_13_4 749 # ASSIGN : s_13_5 102 # ASSIGN : s_13_6 142 # ASSIGN : s_13_7 157 # ASSIGN : s_13_8 691 # ASSIGN : s_13_9 248 # ASSIGN : s_13_10 893 # ASSIGN : s_13_11 962 # ASSIGN : s_13_12 816 # ASSIGN : s_13_13 656 # ASSIGN : s_13_14 752 # ASSIGN : s_14_0 573 # ASSIGN : s_14_1 641 # ASSIGN : s_14_2 687 # ASSIGN : s_14_3 803 # ASSIGN : s_14_4 795 # ASSIGN : s_14_5 520 # ASSIGN : s_14_6 3 # ASSIGN : s_14_7 28 # ASSIGN : s_14_8 88 # ASSIGN : s_14_9 187 # ASSIGN : s_14_10 988 # ASSIGN : s_14_11 986 # ASSIGN : s_14_12 904 # ASSIGN : s_14_13 732 # ASSIGN : s_14_14 809 SHOW_RESULT 1016 END : 1016 (1 seconds) [Mon Jun 19 14:10:50 2006] SHOW_RESULT 1016 CPU : 1.08 = 1.06 + 0.0199999999999998 + 0 + 0 # BOUND : makespan 893 1016 MODIFY_CNF 954 BEGIN : [Mon Jun 19 14:10:50 2006] MODIFY_CNF 954 END : 212603896 bytes (0 seconds) [Mon Jun 19 14:10:50 2006] MODIFY_CNF 954 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 954 BEGIN : [Mon Jun 19 14:10:50 2006] CMD : minisat /tmp/csp2sat31997.cnf /tmp/csp2sat31997.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 6137518 18105167 | 2045839 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 83 (5 /sec) decisions : 1682 (105 /sec) propagations : 599574 (37264 /sec) conflict literals : 932 (7.08 % deleted) Memory used : 360.11 MB CPU time : 16.09 s SATISFIABLE VERIFY_CNF 954 END : (17 seconds) [Mon Jun 19 14:11:07 2006] VERIFY_CNF 954 CPU : 17.3 = 0 + 0.01 + 16.26 + 1.03 # RESULT : makespan 954 SATISFIABLE SHOW_RESULT 954 BEGIN : [Mon Jun 19 14:11:07 2006] # ASSIGN : makespan 954 # ASSIGN : s_0_0 759 # ASSIGN : s_0_1 339 # ASSIGN : s_0_2 491 # ASSIGN : s_0_3 667 # ASSIGN : s_0_4 431 # ASSIGN : s_0_5 933 # ASSIGN : s_0_6 559 # ASSIGN : s_0_7 720 # ASSIGN : s_0_8 18 # ASSIGN : s_0_9 729 # ASSIGN : s_0_10 270 # ASSIGN : s_0_11 188 # ASSIGN : s_0_12 100 # ASSIGN : s_0_13 5 # ASSIGN : s_0_14 30 # ASSIGN : s_1_0 217 # ASSIGN : s_1_1 795 # ASSIGN : s_1_2 591 # ASSIGN : s_1_3 1 # ASSIGN : s_1_4 384 # ASSIGN : s_1_5 884 # ASSIGN : s_1_6 724 # ASSIGN : s_1_7 410 # ASSIGN : s_1_8 104 # ASSIGN : s_1_9 59 # ASSIGN : s_1_10 553 # ASSIGN : s_1_11 285 # ASSIGN : s_1_12 154 # ASSIGN : s_1_13 8 # ASSIGN : s_1_14 101 # ASSIGN : s_2_0 891 # ASSIGN : s_2_1 40 # ASSIGN : s_2_2 687 # ASSIGN : s_2_3 446 # ASSIGN : s_2_4 805 # ASSIGN : s_2_5 325 # ASSIGN : s_2_6 611 # ASSIGN : s_2_7 750 # ASSIGN : s_2_8 249 # ASSIGN : s_2_9 534 # ASSIGN : s_2_10 153 # ASSIGN : s_2_11 391 # ASSIGN : s_2_12 241 # ASSIGN : s_2_13 47 # ASSIGN : s_2_14 121 # ASSIGN : s_3_0 502 # ASSIGN : s_3_1 866 # ASSIGN : s_3_2 54 # ASSIGN : s_3_3 566 # ASSIGN : s_3_4 772 # ASSIGN : s_3_5 383 # ASSIGN : s_3_6 301 # ASSIGN : s_3_7 1 # ASSIGN : s_3_8 358 # ASSIGN : s_3_9 820 # ASSIGN : s_3_10 58 # ASSIGN : s_3_11 451 # ASSIGN : s_3_12 249 # ASSIGN : s_3_13 129 # ASSIGN : s_3_14 150 # ASSIGN : s_4_0 454 # ASSIGN : s_4_1 549 # ASSIGN : s_4_2 33 # ASSIGN : s_4_3 282 # ASSIGN : s_4_4 689 # ASSIGN : s_4_5 1 # ASSIGN : s_4_6 793 # ASSIGN : s_4_7 40 # ASSIGN : s_4_8 374 # ASSIGN : s_4_9 878 # ASSIGN : s_4_10 121 # ASSIGN : s_4_11 512 # ASSIGN : s_4_12 290 # ASSIGN : s_4_13 151 # ASSIGN : s_4_14 207 # ASSIGN : s_5_0 602 # ASSIGN : s_5_1 444 # ASSIGN : s_5_2 746 # ASSIGN : s_5_3 14 # ASSIGN : s_5_4 535 # ASSIGN : s_5_5 170 # ASSIGN : s_5_6 159 # ASSIGN : s_5_7 70 # ASSIGN : s_5_8 837 # ASSIGN : s_5_9 196 # ASSIGN : s_5_10 316 # ASSIGN : s_5_11 520 # ASSIGN : s_5_12 373 # ASSIGN : s_5_13 225 # ASSIGN : s_5_14 284 # ASSIGN : s_6_0 1 # ASSIGN : s_6_1 648 # ASSIGN : s_6_2 88 # ASSIGN : s_6_3 727 # ASSIGN : s_6_4 91 # ASSIGN : s_6_5 835 # ASSIGN : s_6_6 247 # ASSIGN : s_6_7 132 # ASSIGN : s_6_8 937 # ASSIGN : s_6_9 115 # ASSIGN : s_6_10 347 # ASSIGN : s_6_11 590 # ASSIGN : s_6_12 433 # ASSIGN : s_6_13 282 # ASSIGN : s_6_14 329 # ASSIGN : s_7_0 74 # ASSIGN : s_7_1 699 # ASSIGN : s_7_2 98 # ASSIGN : s_7_3 786 # ASSIGN : s_7_4 172 # ASSIGN : s_7_5 221 # ASSIGN : s_7_6 892 # ASSIGN : s_7_7 227 # ASSIGN : s_7_8 781 # ASSIGN : s_7_9 53 # ASSIGN : s_7_10 428 # ASSIGN : s_7_11 649 # ASSIGN : s_7_12 527 # ASSIGN : s_7_13 318 # ASSIGN : s_7_14 350 # ASSIGN : s_8_0 112 # ASSIGN : s_8_1 744 # ASSIGN : s_8_2 829 # ASSIGN : s_8_3 203 # ASSIGN : s_8_4 254 # ASSIGN : s_8_5 191 # ASSIGN : s_8_6 1 # ASSIGN : s_8_7 912 # ASSIGN : s_8_8 616 # ASSIGN : s_8_9 90 # ASSIGN : s_8_10 582 # ASSIGN : s_8_11 706 # ASSIGN : s_8_12 540 # ASSIGN : s_8_13 353 # ASSIGN : s_8_14 400 # ASSIGN : s_9_0 689 # ASSIGN : s_9_1 163 # ASSIGN : s_9_2 210 # ASSIGN : s_9_3 856 # ASSIGN : s_9_4 4 # ASSIGN : s_9_5 802 # ASSIGN : s_9_6 149 # ASSIGN : s_9_7 311 # ASSIGN : s_9_8 692 # ASSIGN : s_9_9 411 # ASSIGN : s_9_10 616 # ASSIGN : s_9_11 717 # ASSIGN : s_9_12 573 # ASSIGN : s_9_13 383 # ASSIGN : s_9_14 441 # ASSIGN : s_10_0 834 # ASSIGN : s_10_1 304 # ASSIGN : s_10_2 343 # ASSIGN : s_10_3 178 # ASSIGN : s_10_4 924 # ASSIGN : s_10_5 772 # ASSIGN : s_10_6 67 # ASSIGN : s_10_7 381 # ASSIGN : s_10_8 830 # ASSIGN : s_10_9 256 # ASSIGN : s_10_10 677 # ASSIGN : s_10_11 802 # ASSIGN : s_10_12 606 # ASSIGN : s_10_13 404 # ASSIGN : s_10_14 539 # ASSIGN : s_11_0 731 # ASSIGN : s_11_1 212 # ASSIGN : s_11_2 192 # ASSIGN : s_11_3 97 # ASSIGN : s_11_4 408 # ASSIGN : s_11_5 15 # ASSIGN : s_11_6 411 # ASSIGN : s_11_7 400 # ASSIGN : s_11_8 879 # ASSIGN : s_11_9 305 # ASSIGN : s_11_10 775 # ASSIGN : s_11_11 855 # ASSIGN : s_11_12 676 # ASSIGN : s_11_13 496 # ASSIGN : s_11_14 580 # ASSIGN : s_12_0 812 # ASSIGN : s_12_1 41 # ASSIGN : s_12_2 404 # ASSIGN : s_12_3 291 # ASSIGN : s_12_4 465 # ASSIGN : s_12_5 718 # ASSIGN : s_12_6 361 # ASSIGN : s_12_7 502 # ASSIGN : s_12_8 792 # ASSIGN : s_12_9 197 # ASSIGN : s_12_10 837 # ASSIGN : s_12_11 900 # ASSIGN : s_12_12 738 # ASSIGN : s_12_13 594 # ASSIGN : s_12_14 665 # ASSIGN : s_13_0 564 # ASSIGN : s_13_1 67 # ASSIGN : s_13_2 337 # ASSIGN : s_13_3 354 # ASSIGN : s_13_4 596 # ASSIGN : s_13_5 524 # ASSIGN : s_13_6 512 # ASSIGN : s_13_7 599 # ASSIGN : s_13_8 453 # ASSIGN : s_13_9 657 # ASSIGN : s_13_10 863 # ASSIGN : s_13_11 928 # ASSIGN : s_13_12 765 # ASSIGN : s_13_13 622 # ASSIGN : s_13_14 690 # ASSIGN : s_14_0 330 # ASSIGN : s_14_1 398 # ASSIGN : s_14_2 285 # ASSIGN : s_14_3 618 # ASSIGN : s_14_4 610 # ASSIGN : s_14_5 444 # ASSIGN : s_14_6 497 # ASSIGN : s_14_7 624 # ASSIGN : s_14_8 511 # ASSIGN : s_14_9 135 # ASSIGN : s_14_10 924 # ASSIGN : s_14_11 952 # ASSIGN : s_14_12 842 # ASSIGN : s_14_13 684 # ASSIGN : s_14_14 747 SHOW_RESULT 954 END : 954 (1 seconds) [Mon Jun 19 14:11:08 2006] SHOW_RESULT 954 CPU : 1.08999999999998 = 1.07999999999998 + 0.01 + 0 + 0 # BOUND : makespan 893 954 MODIFY_CNF 923 BEGIN : [Mon Jun 19 14:11:08 2006] MODIFY_CNF 923 END : 212603896 bytes (0 seconds) [Mon Jun 19 14:11:08 2006] MODIFY_CNF 923 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 923 BEGIN : [Mon Jun 19 14:11:08 2006] CMD : minisat /tmp/csp2sat31997.cnf /tmp/csp2sat31997.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 5942218 17519267 | 1980739 0 0 nan | 0.000 % | | 100 | 5942218 17519267 | 2178812 100 3121 31.2 | 36.392 % | ============================================================================== restarts : 2 conflicts : 158 (8 /sec) decisions : 1976 (100 /sec) propagations : 877761 (44287 /sec) conflict literals : 3682 (4.66 % deleted) Memory used : 360.14 MB CPU time : 19.82 s SATISFIABLE VERIFY_CNF 923 END : (21 seconds) [Mon Jun 19 14:11:29 2006] VERIFY_CNF 923 CPU : 20.88 = 0 + 0 + 19.97 + 0.91 # RESULT : makespan 923 SATISFIABLE SHOW_RESULT 923 BEGIN : [Mon Jun 19 14:11:29 2006] # ASSIGN : makespan 923 # ASSIGN : s_0_0 354 # ASSIGN : s_0_1 768 # ASSIGN : s_0_2 846 # ASSIGN : s_0_3 301 # ASSIGN : s_0_4 431 # ASSIGN : s_0_5 244 # ASSIGN : s_0_6 109 # ASSIGN : s_0_7 914 # ASSIGN : s_0_8 0 # ASSIGN : s_0_9 265 # ASSIGN : s_0_10 518 # ASSIGN : s_0_11 27 # ASSIGN : s_0_12 714 # ASSIGN : s_0_13 12 # ASSIGN : s_0_14 161 # ASSIGN : s_1_0 20 # ASSIGN : s_1_1 697 # ASSIGN : s_1_2 215 # ASSIGN : s_1_3 659 # ASSIGN : s_1_4 536 # ASSIGN : s_1_5 97 # ASSIGN : s_1_6 311 # ASSIGN : s_1_7 778 # ASSIGN : s_1_8 870 # ASSIGN : s_1_9 666 # ASSIGN : s_1_10 453 # ASSIGN : s_1_11 560 # ASSIGN : s_1_12 380 # ASSIGN : s_1_13 482 # ASSIGN : s_1_14 920 # ASSIGN : s_2_0 285 # ASSIGN : s_2_1 221 # ASSIGN : s_2_2 348 # ASSIGN : s_2_3 539 # ASSIGN : s_2_4 703 # ASSIGN : s_2_5 789 # ASSIGN : s_2_6 847 # ASSIGN : s_2_7 222 # ASSIGN : s_2_8 627 # ASSIGN : s_2_9 462 # ASSIGN : s_2_10 118 # ASSIGN : s_2_11 407 # ASSIGN : s_2_12 277 # ASSIGN : s_2_13 15 # ASSIGN : s_2_14 89 # ASSIGN : s_3_0 223 # ASSIGN : s_3_1 583 # ASSIGN : s_3_2 1 # ASSIGN : s_3_3 51 # ASSIGN : s_3_4 503 # ASSIGN : s_3_5 442 # ASSIGN : s_3_6 385 # ASSIGN : s_3_7 544 # ASSIGN : s_3_8 35 # ASSIGN : s_3_9 128 # ASSIGN : s_3_10 830 # ASSIGN : s_3_11 682 # ASSIGN : s_3_12 176 # ASSIGN : s_3_13 307 # ASSIGN : s_3_14 328 # ASSIGN : s_4_0 88 # ASSIGN : s_4_1 306 # ASSIGN : s_4_2 168 # ASSIGN : s_4_3 669 # ASSIGN : s_4_4 791 # ASSIGN : s_4_5 146 # ASSIGN : s_4_6 549 # ASSIGN : s_4_7 677 # ASSIGN : s_4_8 431 # ASSIGN : s_4_9 715 # ASSIGN : s_4_10 893 # ASSIGN : s_4_11 160 # ASSIGN : s_4_12 5 # ASSIGN : s_4_13 175 # ASSIGN : s_4_14 231 # ASSIGN : s_5_0 136 # ASSIGN : s_5_1 230 # ASSIGN : s_5_2 578 # ASSIGN : s_5_3 769 # ASSIGN : s_5_4 310 # ASSIGN : s_5_5 371 # ASSIGN : s_5_6 34 # ASSIGN : s_5_7 707 # ASSIGN : s_5_8 56 # ASSIGN : s_5_9 869 # ASSIGN : s_5_10 0 # ASSIGN : s_5_11 392 # ASSIGN : s_5_12 443 # ASSIGN : s_5_13 521 # ASSIGN : s_5_14 870 # ASSIGN : s_6_0 407 # ASSIGN : s_6_1 125 # ASSIGN : s_6_2 105 # ASSIGN : s_6_3 480 # ASSIGN : s_6_4 21 # ASSIGN : s_6_5 723 # ASSIGN : s_6_6 45 # ASSIGN : s_6_7 312 # ASSIGN : s_6_8 108 # ASSIGN : s_6_9 196 # ASSIGN : s_6_10 564 # ASSIGN : s_6_11 213 # ASSIGN : s_6_12 772 # ASSIGN : s_6_13 866 # ASSIGN : s_6_14 902 # ASSIGN : s_7_0 520 # ASSIGN : s_7_1 176 # ASSIGN : s_7_2 744 # ASSIGN : s_7_3 103 # ASSIGN : s_7_4 874 # ASSIGN : s_7_5 868 # ASSIGN : s_7_6 249 # ASSIGN : s_7_7 6 # ASSIGN : s_7_8 98 # ASSIGN : s_7_9 544 # ASSIGN : s_7_10 645 # ASSIGN : s_7_11 818 # ASSIGN : s_7_12 613 # ASSIGN : s_7_13 581 # ASSIGN : s_7_14 402 # ASSIGN : s_8_0 582 # ASSIGN : s_8_1 12 # ASSIGN : s_8_2 661 # ASSIGN : s_8_3 429 # ASSIGN : s_8_4 63 # ASSIGN : s_8_5 162 # ASSIGN : s_8_6 483 # ASSIGN : s_8_7 872 # ASSIGN : s_8_8 266 # ASSIGN : s_8_9 174 # ASSIGN : s_8_10 795 # ASSIGN : s_8_11 202 # ASSIGN : s_8_12 217 # ASSIGN : s_8_13 354 # ASSIGN : s_8_14 829 # ASSIGN : s_9_0 713 # ASSIGN : s_9_1 405 # ASSIGN : s_9_2 5 # ASSIGN : s_9_3 825 # ASSIGN : s_9_4 616 # ASSIGN : s_9_5 298 # ASSIGN : s_9_6 80 # ASSIGN : s_9_7 90 # ASSIGN : s_9_8 179 # ASSIGN : s_9_9 550 # ASSIGN : s_9_10 206 # ASSIGN : s_9_11 733 # ASSIGN : s_9_12 580 # ASSIGN : s_9_13 384 # ASSIGN : s_9_14 452 # ASSIGN : s_10_0 716 # ASSIGN : s_10_1 548 # ASSIGN : s_10_2 427 # ASSIGN : s_10_3 179 # ASSIGN : s_10_4 465 # ASSIGN : s_10_5 514 # ASSIGN : s_10_6 634 # ASSIGN : s_10_7 160 # ASSIGN : s_10_8 204 # ASSIGN : s_10_9 217 # ASSIGN : s_10_10 295 # ASSIGN : s_10_11 895 # ASSIGN : s_10_12 90 # ASSIGN : s_10_13 774 # ASSIGN : s_10_14 593 # ASSIGN : s_11_0 895 # ASSIGN : s_11_1 452 # ASSIGN : s_11_2 182 # ASSIGN : s_11_3 681 # ASSIGN : s_11_4 1 # ASSIGN : s_11_5 544 # ASSIGN : s_11_6 762 # ASSIGN : s_11_7 200 # ASSIGN : s_11_8 208 # ASSIGN : s_11_9 295 # ASSIGN : s_11_10 390 # ASSIGN : s_11_11 271 # ASSIGN : s_11_12 626 # ASSIGN : s_11_13 91 # ASSIGN : s_11_14 4 # ASSIGN : s_12_0 773 # ASSIGN : s_12_1 671 # ASSIGN : s_12_2 517 # ASSIGN : s_12_3 362 # ASSIGN : s_12_4 579 # ASSIGN : s_12_5 11 # ASSIGN : s_12_6 719 # ASSIGN : s_12_7 425 # ASSIGN : s_12_8 342 # ASSIGN : s_12_9 69 # ASSIGN : s_12_10 31 # ASSIGN : s_12_11 314 # ASSIGN : s_12_12 250 # ASSIGN : s_12_13 279 # ASSIGN : s_12_14 646 # ASSIGN : s_13_0 795 # ASSIGN : s_13_1 827 # ASSIGN : s_13_2 473 # ASSIGN : s_13_3 209 # ASSIGN : s_13_4 9 # ASSIGN : s_13_5 331 # ASSIGN : s_13_6 12 # ASSIGN : s_13_7 586 # ASSIGN : s_13_8 373 # ASSIGN : s_13_9 24 # ASSIGN : s_13_10 57 # ASSIGN : s_13_11 479 # ASSIGN : s_13_12 503 # ASSIGN : s_13_13 634 # ASSIGN : s_13_14 675 # ASSIGN : s_14_0 827 # ASSIGN : s_14_1 77 # ASSIGN : s_14_2 123 # ASSIGN : s_14_3 173 # ASSIGN : s_14_4 495 # ASSIGN : s_14_5 182 # ASSIGN : s_14_6 235 # ASSIGN : s_14_7 609 # ASSIGN : s_14_8 510 # ASSIGN : s_14_9 401 # ASSIGN : s_14_10 267 # ASSIGN : s_14_11 296 # ASSIGN : s_14_12 298 # ASSIGN : s_14_13 669 # ASSIGN : s_14_14 732 SHOW_RESULT 923 END : 923 (1 seconds) [Mon Jun 19 14:11:30 2006] SHOW_RESULT 923 CPU : 1.06 = 1.06 + 0 + 0 + 0 # BOUND : makespan 893 923 MODIFY_CNF 908 BEGIN : [Mon Jun 19 14:11:30 2006] MODIFY_CNF 908 END : 212603896 bytes (0 seconds) [Mon Jun 19 14:11:30 2006] MODIFY_CNF 908 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 908 BEGIN : [Mon Jun 19 14:11:30 2006] CMD : minisat /tmp/csp2sat31997.cnf /tmp/csp2sat31997.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 5847718 17235767 | 1949239 0 0 nan | 0.000 % | | 100 | 5847718 17235767 | 2144162 100 1769 17.7 | 37.453 % | | 251 | 5847718 17235767 | 2358579 251 7014 27.9 | 37.453 % | | 476 | 5847718 17235767 | 2594437 476 12013 25.2 | 37.453 % | ============================================================================== restarts : 4 conflicts : 505 (22 /sec) decisions : 3472 (151 /sec) propagations : 2333086 (101439 /sec) conflict literals : 12253 (6.36 % deleted) Memory used : 360.14 MB CPU time : 23 s SATISFIABLE VERIFY_CNF 908 END : (24 seconds) [Mon Jun 19 14:11:54 2006] VERIFY_CNF 908 CPU : 24.34 = 0 + 0 + 23.17 + 1.17 # RESULT : makespan 908 SATISFIABLE SHOW_RESULT 908 BEGIN : [Mon Jun 19 14:11:54 2006] # ASSIGN : makespan 908 # ASSIGN : s_0_0 31 # ASSIGN : s_0_1 533 # ASSIGN : s_0_2 662 # ASSIGN : s_0_3 597 # ASSIGN : s_0_4 232 # ASSIGN : s_0_5 751 # ASSIGN : s_0_6 845 # ASSIGN : s_0_7 22 # ASSIGN : s_0_8 650 # ASSIGN : s_0_9 777 # ASSIGN : s_0_10 381 # ASSIGN : s_0_11 133 # ASSIGN : s_0_12 287 # ASSIGN : s_0_13 772 # ASSIGN : s_0_14 463 # ASSIGN : s_1_0 220 # ASSIGN : s_1_1 144 # ASSIGN : s_1_2 288 # ASSIGN : s_1_3 584 # ASSIGN : s_1_4 703 # ASSIGN : s_1_5 591 # ASSIGN : s_1_6 513 # ASSIGN : s_1_7 766 # ASSIGN : s_1_8 858 # ASSIGN : s_1_9 645 # ASSIGN : s_1_10 484 # ASSIGN : s_1_11 384 # ASSIGN : s_1_12 58 # ASSIGN : s_1_13 727 # ASSIGN : s_1_14 141 # ASSIGN : s_2_0 489 # ASSIGN : s_2_1 0 # ASSIGN : s_2_2 849 # ASSIGN : s_2_3 270 # ASSIGN : s_2_4 129 # ASSIGN : s_2_5 640 # ASSIGN : s_2_6 1 # ASSIGN : s_2_7 434 # ASSIGN : s_2_8 358 # ASSIGN : s_2_9 698 # ASSIGN : s_2_10 552 # ASSIGN : s_2_11 215 # ASSIGN : s_2_12 121 # ASSIGN : s_2_13 775 # ASSIGN : s_2_14 92 # ASSIGN : s_3_0 598 # ASSIGN : s_3_1 349 # ASSIGN : s_3_2 183 # ASSIGN : s_3_3 793 # ASSIGN : s_3_4 760 # ASSIGN : s_3_5 847 # ASSIGN : s_3_6 291 # ASSIGN : s_3_7 138 # ASSIGN : s_3_8 464 # ASSIGN : s_3_9 49 # ASSIGN : s_3_10 674 # ASSIGN : s_3_11 483 # ASSIGN : s_3_12 246 # ASSIGN : s_3_13 225 # ASSIGN : s_3_14 536 # ASSIGN : s_4_0 334 # ASSIGN : s_4_1 215 # ASSIGN : s_4_2 804 # ASSIGN : s_4_3 476 # ASSIGN : s_4_4 817 # ASSIGN : s_4_5 554 # ASSIGN : s_4_6 644 # ASSIGN : s_4_7 106 # ASSIGN : s_4_8 136 # ASSIGN : s_4_9 568 # ASSIGN : s_4_10 522 # ASSIGN : s_4_11 326 # ASSIGN : s_4_12 382 # ASSIGN : s_4_13 39 # ASSIGN : s_4_14 729 # ASSIGN : s_5_0 84 # ASSIGN : s_5_1 736 # ASSIGN : s_5_2 187 # ASSIGN : s_5_3 397 # ASSIGN : s_5_4 23 # ASSIGN : s_5_5 826 # ASSIGN : s_5_6 897 # ASSIGN : s_5_7 608 # ASSIGN : s_5_8 505 # ASSIGN : s_5_9 504 # ASSIGN : s_5_10 453 # ASSIGN : s_5_11 852 # ASSIGN : s_5_12 547 # ASSIGN : s_5_13 670 # ASSIGN : s_5_14 279 # ASSIGN : s_6_0 660 # ASSIGN : s_6_1 592 # ASSIGN : s_6_2 74 # ASSIGN : s_6_3 14 # ASSIGN : s_6_4 266 # ASSIGN : s_6_5 290 # ASSIGN : s_6_6 77 # ASSIGN : s_6_7 339 # ASSIGN : s_6_8 447 # ASSIGN : s_6_9 176 # ASSIGN : s_6_10 827 # ASSIGN : s_6_11 534 # ASSIGN : s_6_12 733 # ASSIGN : s_6_13 498 # ASSIGN : s_6_14 220 # ASSIGN : s_7_0 171 # ASSIGN : s_7_1 863 # ASSIGN : s_7_2 730 # ASSIGN : s_7_3 73 # ASSIGN : s_7_4 431 # ASSIGN : s_7_5 820 # ASSIGN : s_7_6 582 # ASSIGN : s_7_7 195 # ASSIGN : s_7_8 815 # ASSIGN : s_7_9 807 # ASSIGN : s_7_10 282 # ASSIGN : s_7_11 23 # ASSIGN : s_7_12 665 # ASSIGN : s_7_13 546 # ASSIGN : s_7_14 679 # ASSIGN : s_8_0 394 # ASSIGN : s_8_1 812 # ASSIGN : s_8_2 473 # ASSIGN : s_8_3 742 # ASSIGN : s_8_4 295 # ASSIGN : s_8_5 700 # ASSIGN : s_8_6 112 # ASSIGN : s_8_7 565 # ASSIGN : s_8_8 219 # ASSIGN : s_8_9 676 # ASSIGN : s_8_10 640 # ASSIGN : s_8_11 867 # ASSIGN : s_8_12 607 # ASSIGN : s_8_13 878 # ASSIGN : s_8_14 178 # ASSIGN : s_9_0 739 # ASSIGN : s_9_1 689 # ASSIGN : s_9_2 398 # ASSIGN : s_9_3 172 # ASSIGN : s_9_4 517 # ASSIGN : s_9_5 777 # ASSIGN : s_9_6 760 # ASSIGN : s_9_7 36 # ASSIGN : s_9_8 480 # ASSIGN : s_9_9 338 # ASSIGN : s_9_10 111 # ASSIGN : s_9_11 604 # ASSIGN : s_9_12 3 # ASSIGN : s_9_13 377 # ASSIGN : s_9_14 810 # ASSIGN : s_10_0 742 # ASSIGN : s_10_1 314 # ASSIGN : s_10_2 811 # ASSIGN : s_10_3 143 # ASSIGN : s_10_4 673 # ASSIGN : s_10_5 712 # ASSIGN : s_10_6 431 # ASSIGN : s_10_7 861 # ASSIGN : s_10_8 854 # ASSIGN : s_10_9 95 # ASSIGN : s_10_10 0 # ASSIGN : s_10_11 880 # ASSIGN : s_10_12 168 # ASSIGN : s_10_13 578 # ASSIGN : s_10_14 238 # ASSIGN : s_11_0 565 # ASSIGN : s_11_1 3 # ASSIGN : s_11_2 270 # ASSIGN : s_11_3 484 # ASSIGN : s_11_4 810 # ASSIGN : s_11_5 95 # ASSIGN : s_11_6 185 # ASSIGN : s_11_7 177 # ASSIGN : s_11_8 300 # ASSIGN : s_11_9 813 # ASSIGN : s_11_10 737 # ASSIGN : s_11_11 360 # ASSIGN : s_11_12 678 # ASSIGN : s_11_13 400 # ASSIGN : s_11_14 593 # ASSIGN : s_12_0 312 # ASSIGN : s_12_1 118 # ASSIGN : s_12_2 601 # ASSIGN : s_12_3 845 # ASSIGN : s_12_4 480 # ASSIGN : s_12_5 571 # ASSIGN : s_12_6 782 # ASSIGN : s_12_7 674 # ASSIGN : s_12_8 825 # ASSIGN : s_12_9 368 # ASSIGN : s_12_10 427 # ASSIGN : s_12_11 90 # ASSIGN : s_12_12 341 # ASSIGN : s_12_13 284 # ASSIGN : s_12_14 153 # ASSIGN : s_13_0 799 # ASSIGN : s_13_1 437 # ASSIGN : s_13_2 391 # ASSIGN : s_13_3 650 # ASSIGN : s_13_4 796 # ASSIGN : s_13_5 397 # ASSIGN : s_13_6 770 # ASSIGN : s_13_7 542 # ASSIGN : s_13_8 592 # ASSIGN : s_13_9 254 # ASSIGN : s_13_10 193 # ASSIGN : s_13_11 287 # ASSIGN : s_13_12 831 # ASSIGN : s_13_13 95 # ASSIGN : s_13_14 311 # ASSIGN : s_14_0 832 # ASSIGN : s_14_1 643 # ASSIGN : s_14_2 556 # ASSIGN : s_14_3 362 # ASSIGN : s_14_4 900 # ASSIGN : s_14_5 42 # ASSIGN : s_14_6 348 # ASSIGN : s_14_7 279 # ASSIGN : s_14_8 700 # ASSIGN : s_14_9 193 # ASSIGN : s_14_10 799 # ASSIGN : s_14_11 128 # ASSIGN : s_14_12 465 # ASSIGN : s_14_13 130 # ASSIGN : s_14_14 368 SHOW_RESULT 908 END : 908 (2 seconds) [Mon Jun 19 14:11:56 2006] SHOW_RESULT 908 CPU : 1.07 = 1.06 + 0.01 + 0 + 0 # BOUND : makespan 893 908 MODIFY_CNF 900 BEGIN : [Mon Jun 19 14:11:56 2006] MODIFY_CNF 900 END : 212603895 bytes (0 seconds) [Mon Jun 19 14:11:56 2006] MODIFY_CNF 900 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 900 BEGIN : [Mon Jun 19 14:11:56 2006] CMD : minisat /tmp/csp2sat31997.cnf /tmp/csp2sat31997.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 5797318 17084567 | 1932439 0 0 nan | 0.000 % | | 100 | 5797318 17084567 | 2125682 100 5087 50.9 | 38.020 % | ============================================================================== restarts : 2 conflicts : 125 (6 /sec) decisions : 2411 (118 /sec) propagations : 1024216 (50011 /sec) conflict literals : 5248 (2.07 % deleted) Memory used : 360.14 MB CPU time : 20.48 s SATISFIABLE VERIFY_CNF 900 END : (21 seconds) [Mon Jun 19 14:12:17 2006] VERIFY_CNF 900 CPU : 21.7 = 0 + 0.01 + 20.63 + 1.06 # RESULT : makespan 900 SATISFIABLE SHOW_RESULT 900 BEGIN : [Mon Jun 19 14:12:17 2006] # ASSIGN : makespan 900 # ASSIGN : s_0_0 847 # ASSIGN : s_0_1 648 # ASSIGN : s_0_2 232 # ASSIGN : s_0_3 394 # ASSIGN : s_0_4 31 # ASSIGN : s_0_5 65 # ASSIGN : s_0_6 447 # ASSIGN : s_0_7 707 # ASSIGN : s_0_8 300 # ASSIGN : s_0_9 0 # ASSIGN : s_0_10 750 # ASSIGN : s_0_11 312 # ASSIGN : s_0_12 502 # ASSIGN : s_0_13 86 # ASSIGN : s_0_14 89 # ASSIGN : s_1_0 250 # ASSIGN : s_1_1 386 # ASSIGN : s_1_2 457 # ASSIGN : s_1_3 12 # ASSIGN : s_1_4 553 # ASSIGN : s_1_5 131 # ASSIGN : s_1_6 831 # ASSIGN : s_1_7 739 # ASSIGN : s_1_8 30 # ASSIGN : s_1_9 180 # ASSIGN : s_1_10 94 # ASSIGN : s_1_11 577 # ASSIGN : s_1_12 676 # ASSIGN : s_1_13 347 # ASSIGN : s_1_14 86 # ASSIGN : s_2_0 763 # ASSIGN : s_2_1 0 # ASSIGN : s_2_2 704 # ASSIGN : s_2_3 287 # ASSIGN : s_2_4 168 # ASSIGN : s_2_5 460 # ASSIGN : s_2_6 573 # ASSIGN : s_2_7 649 # ASSIGN : s_2_8 89 # ASSIGN : s_2_9 375 # ASSIGN : s_2_10 1 # ASSIGN : s_2_11 518 # ASSIGN : s_2_12 452 # ASSIGN : s_2_13 826 # ASSIGN : s_2_14 254 # ASSIGN : s_3_0 91 # ASSIGN : s_3_1 718 # ASSIGN : s_3_2 228 # ASSIGN : s_3_3 447 # ASSIGN : s_3_4 610 # ASSIGN : s_3_5 347 # ASSIGN : s_3_6 499 # ASSIGN : s_3_7 408 # ASSIGN : s_3_8 13 # ASSIGN : s_3_9 806 # ASSIGN : s_3_10 284 # ASSIGN : s_3_11 177 # ASSIGN : s_3_12 556 # ASSIGN : s_3_13 682 # ASSIGN : s_3_14 29 # ASSIGN : s_4_0 539 # ASSIGN : s_4_1 129 # ASSIGN : s_4_2 450 # ASSIGN : s_4_3 4 # ASSIGN : s_4_4 643 # ASSIGN : s_4_5 726 # ASSIGN : s_4_6 740 # ASSIGN : s_4_7 465 # ASSIGN : s_4_8 371 # ASSIGN : s_4_9 30 # ASSIGN : s_4_10 509 # ASSIGN : s_4_11 242 # ASSIGN : s_4_12 288 # ASSIGN : s_4_13 587 # ASSIGN : s_4_14 825 # ASSIGN : s_5_0 443 # ASSIGN : s_5_1 228 # ASSIGN : s_5_2 145 # ASSIGN : s_5_3 19 # ASSIGN : s_5_4 75 # ASSIGN : s_5_5 819 # ASSIGN : s_5_6 1 # ASSIGN : s_5_7 587 # ASSIGN : s_5_8 329 # ASSIGN : s_5_9 374 # ASSIGN : s_5_10 375 # ASSIGN : s_5_11 406 # ASSIGN : s_5_12 840 # ASSIGN : s_5_13 530 # ASSIGN : s_5_14 787 # ASSIGN : s_6_0 177 # ASSIGN : s_6_1 1 # ASSIGN : s_6_2 308 # ASSIGN : s_6_3 77 # ASSIGN : s_6_4 136 # ASSIGN : s_6_5 851 # ASSIGN : s_6_6 693 # ASSIGN : s_6_7 313 # ASSIGN : s_6_8 589 # ASSIGN : s_6_9 160 # ASSIGN : s_6_10 413 # ASSIGN : s_6_11 250 # ASSIGN : s_6_12 746 # ASSIGN : s_6_13 494 # ASSIGN : s_6_14 728 # ASSIGN : s_7_0 153 # ASSIGN : s_7_1 603 # ASSIGN : s_7_2 311 # ASSIGN : s_7_3 499 # ASSIGN : s_7_4 256 # ASSIGN : s_7_5 305 # ASSIGN : s_7_6 385 # ASSIGN : s_7_7 0 # ASSIGN : s_7_8 895 # ASSIGN : s_7_9 456 # ASSIGN : s_7_10 796 # ASSIGN : s_7_11 737 # ASSIGN : s_7_12 663 # ASSIGN : s_7_13 462 # ASSIGN : s_7_14 678 # ASSIGN : s_8_0 684 # ASSIGN : s_8_1 78 # ASSIGN : s_8_2 817 # ASSIGN : s_8_3 136 # ASSIGN : s_8_4 305 # ASSIGN : s_8_5 528 # ASSIGN : s_8_6 12 # ASSIGN : s_8_7 263 # ASSIGN : s_8_8 187 # ASSIGN : s_8_9 495 # ASSIGN : s_8_10 555 # ASSIGN : s_8_11 421 # ASSIGN : s_8_12 630 # ASSIGN : s_8_13 432 # ASSIGN : s_8_14 589 # ASSIGN : s_9_0 0 # ASSIGN : s_9_1 304 # ASSIGN : s_9_2 3 # ASSIGN : s_9_3 189 # ASSIGN : s_9_4 404 # ASSIGN : s_9_5 754 # ASSIGN : s_9_6 88 # ASSIGN : s_9_7 119 # ASSIGN : s_9_8 664 # ASSIGN : s_9_9 634 # ASSIGN : s_9_10 689 # ASSIGN : s_9_11 787 # ASSIGN : s_9_12 597 # ASSIGN : s_9_13 98 # ASSIGN : s_9_14 491 # ASSIGN : s_10_0 6 # ASSIGN : s_10_1 351 # ASSIGN : s_10_2 412 # ASSIGN : s_10_3 569 # ASSIGN : s_10_4 759 # ASSIGN : s_10_5 789 # ASSIGN : s_10_6 103 # ASSIGN : s_10_7 84 # ASSIGN : s_10_8 80 # ASSIGN : s_10_9 852 # ASSIGN : s_10_10 594 # ASSIGN : s_10_11 709 # ASSIGN : s_10_12 185 # ASSIGN : s_10_13 255 # ASSIGN : s_10_14 450 # ASSIGN : s_11_0 63 # ASSIGN : s_11_1 808 # ASSIGN : s_11_2 787 # ASSIGN : s_11_3 622 # ASSIGN : s_11_4 805 # ASSIGN : s_11_5 540 # ASSIGN : s_11_6 185 # ASSIGN : s_11_7 457 # ASSIGN : s_11_8 482 # ASSIGN : s_11_9 270 # ASSIGN : s_11_10 123 # ASSIGN : s_11_11 99 # ASSIGN : s_11_12 8 # ASSIGN : s_11_13 703 # ASSIGN : s_11_14 365 # ASSIGN : s_12_0 318 # ASSIGN : s_12_1 52 # ASSIGN : s_12_2 78 # ASSIGN : s_12_3 728 # ASSIGN : s_12_4 835 # ASSIGN : s_12_5 440 # ASSIGN : s_12_6 275 # ASSIGN : s_12_7 495 # ASSIGN : s_12_8 165 # ASSIGN : s_12_9 211 # ASSIGN : s_12_10 185 # ASSIGN : s_12_11 872 # ASSIGN : s_12_12 468 # ASSIGN : s_12_13 798 # ASSIGN : s_12_14 340 # ASSIGN : s_13_0 343 # ASSIGN : s_13_1 507 # ASSIGN : s_13_2 139 # ASSIGN : s_13_3 797 # ASSIGN : s_13_4 889 # ASSIGN : s_13_5 676 # ASSIGN : s_13_6 664 # ASSIGN : s_13_7 716 # ASSIGN : s_13_8 606 # ASSIGN : s_13_9 106 # ASSIGN : s_13_10 222 # ASSIGN : s_13_11 153 # ASSIGN : s_13_12 375 # ASSIGN : s_13_13 187 # ASSIGN : s_13_14 283 # ASSIGN : s_14_0 375 # ASSIGN : s_14_1 461 # ASSIGN : s_14_2 578 # ASSIGN : s_14_3 791 # ASSIGN : s_14_4 892 # ASSIGN : s_14_5 623 # ASSIGN : s_14_6 678 # ASSIGN : s_14_7 832 # ASSIGN : s_14_8 692 # ASSIGN : s_14_9 517 # ASSIGN : s_14_10 347 # ASSIGN : s_14_11 12 # ASSIGN : s_14_12 77 # ASSIGN : s_14_13 14 # ASSIGN : s_14_14 159 SHOW_RESULT 900 END : 900 (1 seconds) [Mon Jun 19 14:12:18 2006] SHOW_RESULT 900 CPU : 1.05999999999995 = 1.04999999999995 + 0.01 + 0 + 0 # BOUND : makespan 893 900 MODIFY_CNF 896 BEGIN : [Mon Jun 19 14:12:18 2006] MODIFY_CNF 896 END : 212603895 bytes (0 seconds) [Mon Jun 19 14:12:18 2006] MODIFY_CNF 896 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 896 BEGIN : [Mon Jun 19 14:12:18 2006] CMD : minisat /tmp/csp2sat31997.cnf /tmp/csp2sat31997.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 5772118 17008967 | 1924039 0 0 nan | 0.000 % | | 100 | 5772118 17008967 | 2116442 100 3642 36.4 | 38.303 % | ============================================================================== restarts : 2 conflicts : 147 (7 /sec) decisions : 2609 (118 /sec) propagations : 1213725 (54945 /sec) conflict literals : 3995 (3.06 % deleted) Memory used : 360.14 MB CPU time : 22.09 s SATISFIABLE VERIFY_CNF 896 END : (24 seconds) [Mon Jun 19 14:12:42 2006] VERIFY_CNF 896 CPU : 23.19 = 0 + 0 + 22.25 + 0.94 # RESULT : makespan 896 SATISFIABLE SHOW_RESULT 896 BEGIN : [Mon Jun 19 14:12:42 2006] # ASSIGN : makespan 896 # ASSIGN : s_0_0 330 # ASSIGN : s_0_1 436 # ASSIGN : s_0_2 825 # ASSIGN : s_0_3 593 # ASSIGN : s_0_4 122 # ASSIGN : s_0_5 495 # ASSIGN : s_0_6 172 # ASSIGN : s_0_7 9 # ASSIGN : s_0_8 110 # ASSIGN : s_0_9 516 # ASSIGN : s_0_10 547 # ASSIGN : s_0_11 691 # ASSIGN : s_0_12 25 # ASSIGN : s_0_13 893 # ASSIGN : s_0_14 224 # ASSIGN : s_1_0 262 # ASSIGN : s_1_1 556 # ASSIGN : s_1_2 335 # ASSIGN : s_1_3 431 # ASSIGN : s_1_4 5 # ASSIGN : s_1_5 199 # ASSIGN : s_1_6 728 # ASSIGN : s_1_7 636 # ASSIGN : s_1_8 142 # ASSIGN : s_1_9 48 # ASSIGN : s_1_10 457 # ASSIGN : s_1_11 797 # ASSIGN : s_1_12 79 # ASSIGN : s_1_13 517 # ASSIGN : s_1_14 196 # ASSIGN : s_2_0 678 # ASSIGN : s_2_1 0 # ASSIGN : s_2_2 181 # ASSIGN : s_2_3 314 # ASSIGN : s_2_4 460 # ASSIGN : s_2_5 402 # ASSIGN : s_2_6 820 # ASSIGN : s_2_7 89 # ASSIGN : s_2_8 741 # ASSIGN : s_2_9 546 # ASSIGN : s_2_10 1 # ASSIGN : s_2_11 623 # ASSIGN : s_2_12 144 # ASSIGN : s_2_13 240 # ASSIGN : s_2_14 152 # ASSIGN : s_3_0 140 # ASSIGN : s_3_1 808 # ASSIGN : s_3_2 248 # ASSIGN : s_3_3 646 # ASSIGN : s_3_4 29 # ASSIGN : s_3_5 295 # ASSIGN : s_3_6 372 # ASSIGN : s_3_7 597 # ASSIGN : s_3_8 356 # ASSIGN : s_3_9 202 # ASSIGN : s_3_10 698 # ASSIGN : s_3_11 544 # ASSIGN : s_3_12 761 # ASSIGN : s_3_13 62 # ASSIGN : s_3_14 83 # ASSIGN : s_4_0 383 # ASSIGN : s_4_1 627 # ASSIGN : s_4_2 241 # ASSIGN : s_4_3 104 # ASSIGN : s_4_4 726 # ASSIGN : s_4_5 129 # ASSIGN : s_4_6 534 # ASSIGN : s_4_7 154 # ASSIGN : s_4_8 817 # ASSIGN : s_4_9 250 # ASSIGN : s_4_10 346 # ASSIGN : s_4_11 526 # ASSIGN : s_4_12 431 # ASSIGN : s_4_13 184 # ASSIGN : s_4_14 8 # ASSIGN : s_5_0 741 # ASSIGN : s_5_1 28 # ASSIGN : s_5_2 252 # ASSIGN : s_5_3 840 # ASSIGN : s_5_4 665 # ASSIGN : s_5_5 1 # ASSIGN : s_5_6 523 # ASSIGN : s_5_7 190 # ASSIGN : s_5_8 428 # ASSIGN : s_5_9 27 # ASSIGN : s_5_10 596 # ASSIGN : s_5_11 508 # ASSIGN : s_5_12 368 # ASSIGN : s_5_13 127 # ASSIGN : s_5_14 476 # ASSIGN : s_6_0 546 # ASSIGN : s_6_1 495 # ASSIGN : s_6_2 1 # ASSIGN : s_6_3 32 # ASSIGN : s_6_4 156 # ASSIGN : s_6_5 753 # ASSIGN : s_6_6 619 # ASSIGN : s_6_7 256 # ASSIGN : s_6_8 719 # ASSIGN : s_6_9 10 # ASSIGN : s_6_10 376 # ASSIGN : s_6_11 180 # ASSIGN : s_6_12 802 # ASSIGN : s_6_13 91 # ASSIGN : s_6_14 458 # ASSIGN : s_7_0 6 # ASSIGN : s_7_1 763 # ASSIGN : s_7_2 439 # ASSIGN : s_7_3 112 # ASSIGN : s_7_4 599 # ASSIGN : s_7_5 648 # ASSIGN : s_7_6 654 # ASSIGN : s_7_7 513 # ASSIGN : s_7_8 736 # ASSIGN : s_7_9 0 # ASSIGN : s_7_10 247 # ASSIGN : s_7_11 62 # ASSIGN : s_7_12 748 # ASSIGN : s_7_13 30 # ASSIGN : s_7_14 389 # ASSIGN : s_8_0 457 # ASSIGN : s_8_1 289 # ASSIGN : s_8_2 536 # ASSIGN : s_8_3 182 # ASSIGN : s_8_4 341 # ASSIGN : s_8_5 248 # ASSIGN : s_8_6 106 # ASSIGN : s_8_7 762 # ASSIGN : s_8_8 30 # ASSIGN : s_8_9 840 # ASSIGN : s_8_10 862 # ASSIGN : s_8_11 446 # ASSIGN : s_8_12 715 # ASSIGN : s_8_13 0 # ASSIGN : s_8_14 672 # ASSIGN : s_9_0 57 # ASSIGN : s_9_1 196 # ASSIGN : s_9_2 88 # ASSIGN : s_9_3 701 # ASSIGN : s_9_4 809 # ASSIGN : s_9_5 163 # ASSIGN : s_9_6 799 # ASSIGN : s_9_7 351 # ASSIGN : s_9_8 5 # ASSIGN : s_9_9 456 # ASSIGN : s_9_10 486 # ASSIGN : s_9_11 266 # ASSIGN : s_9_12 668 # ASSIGN : s_9_13 647 # ASSIGN : s_9_14 549 # ASSIGN : s_10_0 60 # ASSIGN : s_10_1 728 # ASSIGN : s_10_2 22 # ASSIGN : s_10_3 406 # ASSIGN : s_10_4 230 # ASSIGN : s_10_5 260 # ASSIGN : s_10_6 290 # ASSIGN : s_10_7 459 # ASSIGN : s_10_8 1 # ASSIGN : s_10_9 680 # ASSIGN : s_10_10 117 # ASSIGN : s_10_11 480 # ASSIGN : s_10_12 598 # ASSIGN : s_10_13 801 # ASSIGN : s_10_14 508 # ASSIGN : s_11_0 202 # ASSIGN : s_11_1 104 # ASSIGN : s_11_2 4 # ASSIGN : s_11_3 233 # ASSIGN : s_11_4 1 # ASSIGN : s_11_5 22 # ASSIGN : s_11_6 429 # ASSIGN : s_11_7 421 # ASSIGN : s_11_8 569 # ASSIGN : s_11_9 326 # ASSIGN : s_11_10 627 # ASSIGN : s_11_11 773 # ASSIGN : s_11_12 514 # ASSIGN : s_11_13 689 # ASSIGN : s_11_14 811 # ASSIGN : s_12_0 118 # ASSIGN : s_12_1 2 # ASSIGN : s_12_2 652 # ASSIGN : s_12_3 438 # ASSIGN : s_12_4 304 # ASSIGN : s_12_5 143 # ASSIGN : s_12_6 43 # ASSIGN : s_12_7 804 # ASSIGN : s_12_8 192 # ASSIGN : s_12_9 745 # ASSIGN : s_12_10 212 # ASSIGN : s_12_11 238 # ASSIGN : s_12_12 341 # ASSIGN : s_12_13 556 # ASSIGN : s_12_14 713 # ASSIGN : s_13_0 230 # ASSIGN : s_13_1 340 # ASSIGN : s_13_2 619 # ASSIGN : s_13_3 501 # ASSIGN : s_13_4 440 # ASSIGN : s_13_5 856 # ASSIGN : s_13_6 716 # ASSIGN : s_13_7 478 # ASSIGN : s_13_8 658 # ASSIGN : s_13_9 625 # ASSIGN : s_13_10 795 # ASSIGN : s_13_11 595 # ASSIGN : s_13_12 263 # ASSIGN : s_13_13 443 # ASSIGN : s_13_14 738 # ASSIGN : s_14_0 828 # ASSIGN : s_14_1 243 # ASSIGN : s_14_2 722 # ASSIGN : s_14_3 10 # ASSIGN : s_14_4 78 # ASSIGN : s_14_5 669 # ASSIGN : s_14_6 86 # ASSIGN : s_14_7 18 # ASSIGN : s_14_8 470 # ASSIGN : s_14_9 100 # ASSIGN : s_14_10 767 # ASSIGN : s_14_11 16 # ASSIGN : s_14_12 161 # ASSIGN : s_14_13 584 # ASSIGN : s_14_14 294 SHOW_RESULT 896 END : 896 (1 seconds) [Mon Jun 19 14:12:43 2006] SHOW_RESULT 896 CPU : 1.06000000000001 = 1.05000000000001 + 0.01 + 0 + 0 # BOUND : makespan 893 896 MODIFY_CNF 894 BEGIN : [Mon Jun 19 14:12:43 2006] MODIFY_CNF 894 END : 212603895 bytes (0 seconds) [Mon Jun 19 14:12:43 2006] MODIFY_CNF 894 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 894 BEGIN : [Mon Jun 19 14:12:43 2006] CMD : minisat /tmp/csp2sat31997.cnf /tmp/csp2sat31997.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 5759518 16971167 | 1919839 0 0 nan | 0.000 % | | 102 | 5759518 16971167 | 2111822 102 3031 29.7 | 38.444 % | | 252 | 5759518 16971167 | 2323005 252 10409 41.3 | 38.444 % | ============================================================================== restarts : 3 conflicts : 311 (14 /sec) decisions : 2913 (128 /sec) propagations : 1702710 (75075 /sec) conflict literals : 10913 (4.73 % deleted) Memory used : 360.14 MB CPU time : 22.68 s SATISFIABLE VERIFY_CNF 894 END : (24 seconds) [Mon Jun 19 14:13:07 2006] VERIFY_CNF 894 CPU : 23.92 = 0 + 0 + 22.82 + 1.1 # RESULT : makespan 894 SATISFIABLE SHOW_RESULT 894 BEGIN : [Mon Jun 19 14:13:07 2006] # ASSIGN : makespan 894 # ASSIGN : s_0_0 481 # ASSIGN : s_0_1 753 # ASSIGN : s_0_2 19 # ASSIGN : s_0_3 235 # ASSIGN : s_0_4 537 # ASSIGN : s_0_5 99 # ASSIGN : s_0_6 429 # ASSIGN : s_0_7 708 # ASSIGN : s_0_8 120 # ASSIGN : s_0_9 205 # ASSIGN : s_0_10 321 # ASSIGN : s_0_11 626 # ASSIGN : s_0_12 840 # ASSIGN : s_0_13 132 # ASSIGN : s_0_14 135 # ASSIGN : s_1_0 534 # ASSIGN : s_1_1 348 # ASSIGN : s_1_2 438 # ASSIGN : s_1_3 108 # ASSIGN : s_1_4 161 # ASSIGN : s_1_5 185 # ASSIGN : s_1_6 633 # ASSIGN : s_1_7 234 # ASSIGN : s_1_8 844 # ASSIGN : s_1_9 602 # ASSIGN : s_1_10 702 # ASSIGN : s_1_11 745 # ASSIGN : s_1_12 0 # ASSIGN : s_1_13 63 # ASSIGN : s_1_14 345 # ASSIGN : s_2_0 754 # ASSIGN : s_2_1 1 # ASSIGN : s_2_2 270 # ASSIGN : s_2_3 2 # ASSIGN : s_2_4 668 # ASSIGN : s_2_5 481 # ASSIGN : s_2_6 329 # ASSIGN : s_2_7 613 # ASSIGN : s_2_8 405 # ASSIGN : s_2_9 817 # ASSIGN : s_2_10 182 # ASSIGN : s_2_11 119 # ASSIGN : s_2_12 174 # ASSIGN : s_2_13 539 # ASSIGN : s_2_14 90 # ASSIGN : s_3_0 692 # ASSIGN : s_3_1 569 # ASSIGN : s_3_2 890 # ASSIGN : s_3_3 183 # ASSIGN : s_3_4 754 # ASSIGN : s_3_5 122 # ASSIGN : s_3_6 269 # ASSIGN : s_3_7 326 # ASSIGN : s_3_8 6 # ASSIGN : s_3_9 22 # ASSIGN : s_3_10 827 # ASSIGN : s_3_11 518 # ASSIGN : s_3_12 382 # ASSIGN : s_3_13 425 # ASSIGN : s_3_14 446 # ASSIGN : s_4_0 422 # ASSIGN : s_4_1 470 # ASSIGN : s_4_2 160 # ASSIGN : s_4_3 171 # ASSIGN : s_4_4 571 # ASSIGN : s_4_5 312 # ASSIGN : s_4_6 809 # ASSIGN : s_4_7 187 # ASSIGN : s_4_8 326 # ASSIGN : s_4_9 68 # ASSIGN : s_4_10 731 # ASSIGN : s_4_11 179 # ASSIGN : s_4_12 217 # ASSIGN : s_4_13 7 # ASSIGN : s_4_14 654 # ASSIGN : s_5_0 303 # ASSIGN : s_5_1 2 # ASSIGN : s_5_2 779 # ASSIGN : s_5_3 115 # ASSIGN : s_5_4 391 # ASSIGN : s_5_5 78 # ASSIGN : s_5_6 104 # ASSIGN : s_5_7 551 # ASSIGN : s_5_8 509 # ASSIGN : s_5_9 249 # ASSIGN : s_5_10 272 # ASSIGN : s_5_11 255 # ASSIGN : s_5_12 672 # ASSIGN : s_5_13 452 # ASSIGN : s_5_14 862 # ASSIGN : s_6_0 201 # ASSIGN : s_6_1 657 # ASSIGN : s_6_2 2 # ASSIGN : s_6_3 288 # ASSIGN : s_6_4 466 # ASSIGN : s_6_5 29 # ASSIGN : s_6_6 598 # ASSIGN : s_6_7 92 # ASSIGN : s_6_8 640 # ASSIGN : s_6_9 5 # ASSIGN : s_6_10 490 # ASSIGN : s_6_11 370 # ASSIGN : s_6_12 732 # ASSIGN : s_6_13 826 # ASSIGN : s_6_14 428 # ASSIGN : s_7_0 274 # ASSIGN : s_7_1 708 # ASSIGN : s_7_2 568 # ASSIGN : s_7_3 755 # ASSIGN : s_7_4 225 # ASSIGN : s_7_5 557 # ASSIGN : s_7_6 163 # ASSIGN : s_7_7 407 # ASSIGN : s_7_8 563 # ASSIGN : s_7_9 694 # ASSIGN : s_7_10 64 # ASSIGN : s_7_11 298 # ASSIGN : s_7_12 659 # ASSIGN : s_7_13 862 # ASSIGN : s_7_14 348 # ASSIGN : s_8_0 613 # ASSIGN : s_8_1 419 # ASSIGN : s_8_2 167 # ASSIGN : s_8_3 549 # ASSIGN : s_8_4 795 # ASSIGN : s_8_5 749 # ASSIGN : s_8_6 3 # ASSIGN : s_8_7 365 # ASSIGN : s_8_8 250 # ASSIGN : s_8_9 700 # ASSIGN : s_8_10 761 # ASSIGN : s_8_11 734 # ASSIGN : s_8_12 69 # ASSIGN : s_8_13 102 # ASSIGN : s_8_14 503 # ASSIGN : s_9_0 106 # ASSIGN : s_9_1 812 # ASSIGN : s_9_2 642 # ASSIGN : s_9_3 446 # ASSIGN : s_9_4 280 # ASSIGN : s_9_5 861 # ASSIGN : s_9_6 140 # ASSIGN : s_9_7 717 # ASSIGN : s_9_8 787 # ASSIGN : s_9_9 250 # ASSIGN : s_9_10 367 # ASSIGN : s_9_11 1 # ASSIGN : s_9_12 184 # ASSIGN : s_9_13 150 # ASSIGN : s_9_14 544 # ASSIGN : s_10_0 109 # ASSIGN : s_10_1 859 # ASSIGN : s_10_2 345 # ASSIGN : s_10_3 692 # ASSIGN : s_10_4 497 # ASSIGN : s_10_5 391 # ASSIGN : s_10_6 717 # ASSIGN : s_10_7 799 # ASSIGN : s_10_8 167 # ASSIGN : s_10_9 421 # ASSIGN : s_10_10 597 # ASSIGN : s_10_11 469 # ASSIGN : s_10_12 527 # ASSIGN : s_10_13 171 # ASSIGN : s_10_14 818 # ASSIGN : s_11_0 834 # ASSIGN : s_11_1 160 # ASSIGN : s_11_2 87 # ASSIGN : s_11_3 347 # ASSIGN : s_11_4 494 # ASSIGN : s_11_5 640 # ASSIGN : s_11_6 497 # ASSIGN : s_11_7 886 # ASSIGN : s_11_8 582 # ASSIGN : s_11_9 722 # ASSIGN : s_11_10 428 # ASSIGN : s_11_11 862 # ASSIGN : s_11_12 105 # ASSIGN : s_11_13 263 # ASSIGN : s_11_14 2 # ASSIGN : s_12_0 166 # ASSIGN : s_12_1 134 # ASSIGN : s_12_2 718 # ASSIGN : s_12_3 825 # ASSIGN : s_12_4 188 # ASSIGN : s_12_5 801 # ASSIGN : s_12_6 226 # ASSIGN : s_12_7 0 # ASSIGN : s_12_8 668 # ASSIGN : s_12_9 484 # ASSIGN : s_12_10 571 # ASSIGN : s_12_11 270 # ASSIGN : s_12_12 423 # ASSIGN : s_12_13 690 # ASSIGN : s_12_14 398 # ASSIGN : s_13_0 390 # ASSIGN : s_13_1 252 # ASSIGN : s_13_2 537 # ASSIGN : s_13_3 600 # ASSIGN : s_13_4 534 # ASSIGN : s_13_5 821 # ASSIGN : s_13_6 705 # ASSIGN : s_13_7 863 # ASSIGN : s_13_8 192 # ASSIGN : s_13_9 543 # ASSIGN : s_13_10 3 # ASSIGN : s_13_11 576 # ASSIGN : s_13_12 450 # ASSIGN : s_13_13 786 # ASSIGN : s_13_14 729 # ASSIGN : s_14_0 18 # ASSIGN : s_14_1 88 # ASSIGN : s_14_2 383 # ASSIGN : s_14_3 888 # ASSIGN : s_14_4 787 # ASSIGN : s_14_5 428 # ASSIGN : s_14_6 584 # ASSIGN : s_14_7 491 # ASSIGN : s_14_8 688 # ASSIGN : s_14_9 144 # ASSIGN : s_14_10 799 # ASSIGN : s_14_11 86 # ASSIGN : s_14_12 300 # ASSIGN : s_14_13 625 # ASSIGN : s_14_14 205 SHOW_RESULT 894 END : 894 (1 seconds) [Mon Jun 19 14:13:08 2006] SHOW_RESULT 894 CPU : 1.06999999999995 = 1.04999999999995 + 0.02 + 0 + 0 # BOUND : makespan 893 894 MODIFY_CNF 893 BEGIN : [Mon Jun 19 14:13:08 2006] MODIFY_CNF 893 END : 212603895 bytes (0 seconds) [Mon Jun 19 14:13:08 2006] MODIFY_CNF 893 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 893 BEGIN : [Mon Jun 19 14:13:08 2006] CMD : minisat /tmp/csp2sat31997.cnf /tmp/csp2sat31997.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 5753219 16952267 | 1917739 0 0 nan | 0.000 % | | 100 | 5753219 16952267 | 2109512 100 1298 13.0 | 38.515 % | | 251 | 5753219 16952267 | 2320464 251 3827 15.2 | 38.515 % | | 476 | 5753219 16952267 | 2552510 476 5675 11.9 | 38.515 % | ============================================================================== restarts : 4 conflicts : 620 (28 /sec) decisions : 2888 (128 /sec) propagations : 1776729 (78931 /sec) conflict literals : 11841 (6.13 % deleted) Memory used : 360.14 MB CPU time : 22.51 s SATISFIABLE VERIFY_CNF 893 END : (24 seconds) [Mon Jun 19 14:13:32 2006] VERIFY_CNF 893 CPU : 23.93 = 0.00999999999999091 + 0.01 + 22.67 + 1.24 # RESULT : makespan 893 SATISFIABLE SHOW_RESULT 893 BEGIN : [Mon Jun 19 14:13:32 2006] # ASSIGN : makespan 893 # ASSIGN : s_0_0 316 # ASSIGN : s_0_1 789 # ASSIGN : s_0_2 74 # ASSIGN : s_0_3 150 # ASSIGN : s_0_4 40 # ASSIGN : s_0_5 687 # ASSIGN : s_0_6 370 # ASSIGN : s_0_7 31 # ASSIGN : s_0_8 222 # ASSIGN : s_0_9 426 # ASSIGN : s_0_10 546 # ASSIGN : s_0_11 234 # ASSIGN : s_0_12 456 # ASSIGN : s_0_13 598 # ASSIGN : s_0_14 719 # ASSIGN : s_1_0 825 # ASSIGN : s_1_1 7 # ASSIGN : s_1_2 215 # ASSIGN : s_1_3 0 # ASSIGN : s_1_4 507 # ASSIGN : s_1_5 534 # ASSIGN : s_1_6 79 # ASSIGN : s_1_7 646 # ASSIGN : s_1_8 767 # ASSIGN : s_1_9 474 # ASSIGN : s_1_10 148 # ASSIGN : s_1_11 324 # ASSIGN : s_1_12 583 # ASSIGN : s_1_13 423 # ASSIGN : s_1_14 531 # ASSIGN : s_2_0 463 # ASSIGN : s_2_1 0 # ASSIGN : s_2_2 349 # ASSIGN : s_2_3 717 # ASSIGN : s_2_4 631 # ASSIGN : s_2_5 83 # ASSIGN : s_2_6 196 # ASSIGN : s_2_7 408 # ASSIGN : s_2_8 526 # ASSIGN : s_2_9 272 # ASSIGN : s_2_10 805 # ASSIGN : s_2_11 141 # ASSIGN : s_2_12 1 # ASSIGN : s_2_13 9 # ASSIGN : s_2_14 602 # ASSIGN : s_3_0 401 # ASSIGN : s_3_1 297 # ASSIGN : s_3_2 541 # ASSIGN : s_3_3 63 # ASSIGN : s_3_4 264 # ASSIGN : s_3_5 203 # ASSIGN : s_3_6 672 # ASSIGN : s_3_7 479 # ASSIGN : s_3_8 877 # ASSIGN : s_3_9 817 # ASSIGN : s_3_10 0 # ASSIGN : s_3_11 621 # ASSIGN : s_3_12 736 # ASSIGN : s_3_13 520 # ASSIGN : s_3_14 545 # ASSIGN : s_4_0 190 # ASSIGN : s_4_1 635 # ASSIGN : s_4_2 4 # ASSIGN : s_4_3 142 # ASSIGN : s_4_4 548 # ASSIGN : s_4_5 21 # ASSIGN : s_4_6 272 # ASSIGN : s_4_7 518 # ASSIGN : s_4_8 63 # ASSIGN : s_4_9 734 # ASSIGN : s_4_10 242 # ASSIGN : s_4_11 454 # ASSIGN : s_4_12 810 # ASSIGN : s_4_13 462 # ASSIGN : s_4_14 357 # ASSIGN : s_5_0 90 # ASSIGN : s_5_1 420 # ASSIGN : s_5_2 740 # ASSIGN : s_5_3 7 # ASSIGN : s_5_4 359 # ASSIGN : s_5_5 708 # ASSIGN : s_5_6 729 # ASSIGN : s_5_7 823 # ASSIGN : s_5_8 622 # ASSIGN : s_5_9 89 # ASSIGN : s_5_10 177 # ASSIGN : s_5_11 677 # ASSIGN : s_5_12 510 # ASSIGN : s_5_13 302 # ASSIGN : s_5_14 224 # ASSIGN : s_6_0 618 # ASSIGN : s_6_1 738 # ASSIGN : s_6_2 538 # ASSIGN : s_6_3 834 # ASSIGN : s_6_4 433 # ASSIGN : s_6_5 485 # ASSIGN : s_6_6 32 # ASSIGN : s_6_7 313 # ASSIGN : s_6_8 817 # ASSIGN : s_6_9 457 # ASSIGN : s_6_10 67 # ASSIGN : s_6_11 560 # ASSIGN : s_6_12 219 # ASSIGN : s_6_13 164 # ASSIGN : s_6_14 201 # ASSIGN : s_7_0 691 # ASSIGN : s_7_1 848 # ASSIGN : s_7_2 425 # ASSIGN : s_7_3 328 # ASSIGN : s_7_4 745 # ASSIGN : s_7_5 739 # ASSIGN : s_7_6 504 # ASSIGN : s_7_7 208 # ASSIGN : s_7_8 499 # ASSIGN : s_7_9 113 # ASSIGN : s_7_10 592 # ASSIGN : s_7_11 798 # ASSIGN : s_7_12 570 # ASSIGN : s_7_13 119 # ASSIGN : s_7_14 151 # ASSIGN : s_8_0 715 # ASSIGN : s_8_1 150 # ASSIGN : s_8_2 632 # ASSIGN : s_8_3 266 # ASSIGN : s_8_4 794 # ASSIGN : s_8_5 35 # ASSIGN : s_8_6 566 # ASSIGN : s_8_7 58 # ASSIGN : s_8_8 317 # ASSIGN : s_8_9 505 # ASSIGN : s_8_10 208 # ASSIGN : s_8_11 47 # ASSIGN : s_8_12 423 # ASSIGN : s_8_13 393 # ASSIGN : s_8_14 109 # ASSIGN : s_9_0 369 # ASSIGN : s_9_1 496 # ASSIGN : s_9_2 551 # ASSIGN : s_9_3 398 # ASSIGN : s_9_4 170 # ASSIGN : s_9_5 629 # ASSIGN : s_9_6 662 # ASSIGN : s_9_7 100 # ASSIGN : s_9_8 257 # ASSIGN : s_9_9 863 # ASSIGN : s_9_10 282 # ASSIGN : s_9_11 692 # ASSIGN : s_9_12 777 # ASSIGN : s_9_13 372 # ASSIGN : s_9_14 2 # ASSIGN : s_10_0 561 # ASSIGN : s_10_1 385 # ASSIGN : s_10_2 311 # ASSIGN : s_10_3 115 # ASSIGN : s_10_4 140 # ASSIGN : s_10_5 170 # ASSIGN : s_10_6 422 # ASSIGN : s_10_7 292 # ASSIGN : s_10_8 4 # ASSIGN : s_10_9 621 # ASSIGN : s_10_10 710 # ASSIGN : s_10_11 8 # ASSIGN : s_10_12 36 # ASSIGN : s_10_13 200 # ASSIGN : s_10_14 669 # ASSIGN : s_11_0 8 # ASSIGN : s_11_1 543 # ASSIGN : s_11_2 56 # ASSIGN : s_11_3 635 # ASSIGN : s_11_4 79 # ASSIGN : s_11_5 341 # ASSIGN : s_11_6 800 # ASSIGN : s_11_7 885 # ASSIGN : s_11_8 423 # ASSIGN : s_11_9 161 # ASSIGN : s_11_10 481 # ASSIGN : s_11_11 82 # ASSIGN : s_11_12 106 # ASSIGN : s_11_13 716 # ASSIGN : s_11_14 256 # ASSIGN : s_12_0 36 # ASSIGN : s_12_1 78 # ASSIGN : s_12_2 142 # ASSIGN : s_12_3 203 # ASSIGN : s_12_4 322 # ASSIGN : s_12_5 810 # ASSIGN : s_12_6 757 # ASSIGN : s_12_7 554 # ASSIGN : s_12_8 506 # ASSIGN : s_12_9 675 # ASSIGN : s_12_10 455 # ASSIGN : s_12_11 526 # ASSIGN : s_12_12 396 # ASSIGN : s_12_13 830 # ASSIGN : s_12_14 868 # ASSIGN : s_13_0 58 # ASSIGN : s_13_1 201 # ASSIGN : s_13_2 626 # ASSIGN : s_13_3 496 # ASSIGN : s_13_4 469 # ASSIGN : s_13_5 761 # ASSIGN : s_13_6 647 # ASSIGN : s_13_7 738 # ASSIGN : s_13_8 143 # ASSIGN : s_13_9 588 # ASSIGN : s_13_10 343 # ASSIGN : s_13_11 472 # ASSIGN : s_13_12 659 # ASSIGN : s_13_13 858 # ASSIGN : s_13_14 801 # ASSIGN : s_14_0 238 # ASSIGN : s_14_1 104 # ASSIGN : s_14_2 11 # ASSIGN : s_14_3 828 # ASSIGN : s_14_4 306 # ASSIGN : s_14_5 838 # ASSIGN : s_14_6 182 # ASSIGN : s_14_7 763 # ASSIGN : s_14_8 664 # ASSIGN : s_14_9 527 # ASSIGN : s_14_10 404 # ASSIGN : s_14_11 891 # ASSIGN : s_14_12 314 # ASSIGN : s_14_13 601 # ASSIGN : s_14_14 432 SHOW_RESULT 893 END : 893 (1 seconds) [Mon Jun 19 14:13:33 2006] SHOW_RESULT 893 CPU : 1.05999999999997 = 1.02999999999997 + 0.03 + 0 + 0 # BOUND : makespan 893 893 MAIN END : (548 seconds) [Mon Jun 19 14:13:33 2006] MAIN CPU : 545.93 = 353.34 + 1.53 + 181.23 + 9.83