# TIMEOUT 18000 MAIN BEGIN : [Mon Jun 19 12:26:50 2006] READ BEGIN : csp/j8-per20-0.csp [Mon Jun 19 12:26:50 2006] READ END : csp/j8-per20-0.csp (1 seconds) [Mon Jun 19 12:26:51 2006] READ CPU : 0.95 = 0.95 + 0 + 0 + 0 # BOUND : makespan 1000 2141 GENERATE_CNF 2141 BEGIN : [Mon Jun 19 12:26:51 2006] GENERATE_CNF 2141 END : 139255 variables 2030756 clauses 46301588 bytes (77 seconds) [Mon Jun 19 12:28:08 2006] GENERATE_CNF 2141 CPU : 76.43 = 76.09 + 0.34 + 0 + 0 MODIFY_CNF 1570 BEGIN : [Mon Jun 19 12:28:08 2006] MODIFY_CNF 1570 END : 46301594 bytes (0 seconds) [Mon Jun 19 12:28:08 2006] MODIFY_CNF 1570 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1570 BEGIN : [Mon Jun 19 12:28:08 2006] CMD : minisat /tmp/csp2sat29544.cnf /tmp/csp2sat29544.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1517791 4416174 | 505930 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 16 (5 /sec) decisions : 326 (102 /sec) propagations : 282530 (88567 /sec) conflict literals : 326 (6.05 % deleted) Memory used : 85.48 MB CPU time : 3.19 s SATISFIABLE VERIFY_CNF 1570 END : (3 seconds) [Mon Jun 19 12:28:11 2006] VERIFY_CNF 1570 CPU : 3.57 = 0 + 0 + 3.25 + 0.32 # RESULT : makespan 1570 SATISFIABLE SHOW_RESULT 1570 BEGIN : [Mon Jun 19 12:28:11 2006] # ASSIGN : makespan 1570 # ASSIGN : s_0_0 154 # ASSIGN : s_0_1 1354 # ASSIGN : s_0_2 337 # ASSIGN : s_0_3 33 # ASSIGN : s_0_4 273 # ASSIGN : s_0_5 442 # ASSIGN : s_0_6 9 # ASSIGN : s_0_7 473 # ASSIGN : s_1_0 1260 # ASSIGN : s_1_1 746 # ASSIGN : s_1_2 447 # ASSIGN : s_1_3 159 # ASSIGN : s_1_4 405 # ASSIGN : s_1_5 545 # ASSIGN : s_1_6 78 # ASSIGN : s_1_7 784 # ASSIGN : s_2_0 1349 # ASSIGN : s_2_1 602 # ASSIGN : s_2_2 661 # ASSIGN : s_2_3 377 # ASSIGN : s_2_4 448 # ASSIGN : s_2_5 869 # ASSIGN : s_2_6 148 # ASSIGN : s_2_7 840 # ASSIGN : s_3_0 1492 # ASSIGN : s_3_1 492 # ASSIGN : s_3_2 843 # ASSIGN : s_3_3 430 # ASSIGN : s_3_4 630 # ASSIGN : s_3_5 1067 # ASSIGN : s_3_6 261 # ASSIGN : s_3_7 914 # ASSIGN : s_4_0 805 # ASSIGN : s_4_1 421 # ASSIGN : s_4_2 968 # ASSIGN : s_4_3 455 # ASSIGN : s_4_4 1066 # ASSIGN : s_4_5 1247 # ASSIGN : s_4_6 314 # ASSIGN : s_4_7 998 # ASSIGN : s_5_0 559 # ASSIGN : s_5_1 354 # ASSIGN : s_5_2 1008 # ASSIGN : s_5_3 533 # ASSIGN : s_5_4 1262 # ASSIGN : s_5_5 1429 # ASSIGN : s_5_6 564 # ASSIGN : s_5_7 1134 # ASSIGN : s_6_0 688 # ASSIGN : s_6_1 810 # ASSIGN : s_6_2 1077 # ASSIGN : s_6_3 842 # ASSIGN : s_6_4 1377 # ASSIGN : s_6_5 1561 # ASSIGN : s_6_6 1075 # ASSIGN : s_6_7 1307 # ASSIGN : s_7_0 269 # ASSIGN : s_7_1 860 # ASSIGN : s_7_2 1319 # ASSIGN : s_7_3 1226 # ASSIGN : s_7_4 1555 # ASSIGN : s_7_5 1567 # ASSIGN : s_7_6 1273 # ASSIGN : s_7_7 1501 SHOW_RESULT 1570 END : 1570 (1 seconds) [Mon Jun 19 12:28:12 2006] SHOW_RESULT 1570 CPU : 0.25 = 0.25 + 0 + 0 + 0 # BOUND : makespan 1000 1570 MODIFY_CNF 1285 BEGIN : [Mon Jun 19 12:28:12 2006] MODIFY_CNF 1285 END : 46301594 bytes (0 seconds) [Mon Jun 19 12:28:12 2006] MODIFY_CNF 1285 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1285 BEGIN : [Mon Jun 19 12:28:12 2006] CMD : minisat /tmp/csp2sat29544.cnf /tmp/csp2sat29544.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1262431 3650094 | 420810 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 8 (3 /sec) decisions : 332 (116 /sec) propagations : 206253 (72369 /sec) conflict literals : 48 (4.00 % deleted) Memory used : 85.48 MB CPU time : 2.85 s SATISFIABLE VERIFY_CNF 1285 END : (3 seconds) [Mon Jun 19 12:28:15 2006] VERIFY_CNF 1285 CPU : 3.21 = 0 + 0 + 2.92 + 0.29 # RESULT : makespan 1285 SATISFIABLE SHOW_RESULT 1285 BEGIN : [Mon Jun 19 12:28:15 2006] # ASSIGN : makespan 1285 # ASSIGN : s_0_0 648 # ASSIGN : s_0_1 1005 # ASSIGN : s_0_2 858 # ASSIGN : s_0_3 73 # ASSIGN : s_0_4 1221 # ASSIGN : s_0_5 42 # ASSIGN : s_0_6 11 # ASSIGN : s_0_7 337 # ASSIGN : s_1_0 1053 # ASSIGN : s_1_1 741 # ASSIGN : s_1_2 483 # ASSIGN : s_1_3 835 # ASSIGN : s_1_4 145 # ASSIGN : s_1_5 187 # ASSIGN : s_1_6 35 # ASSIGN : s_1_7 779 # ASSIGN : s_2_0 1142 # ASSIGN : s_2_1 682 # ASSIGN : s_2_2 963 # ASSIGN : s_2_3 782 # ASSIGN : s_2_4 218 # ASSIGN : s_2_5 388 # ASSIGN : s_2_6 105 # ASSIGN : s_2_7 835 # ASSIGN : s_3_0 294 # ASSIGN : s_3_1 73 # ASSIGN : s_3_2 2 # ASSIGN : s_3_3 1260 # ASSIGN : s_3_4 372 # ASSIGN : s_3_5 586 # ASSIGN : s_3_6 219 # ASSIGN : s_3_7 864 # ASSIGN : s_4_0 422 # ASSIGN : s_4_1 39 # ASSIGN : s_4_2 154 # ASSIGN : s_4_3 194 # ASSIGN : s_4_4 585 # ASSIGN : s_4_5 766 # ASSIGN : s_4_6 272 # ASSIGN : s_4_7 948 # ASSIGN : s_5_0 61 # ASSIGN : s_5_1 938 # ASSIGN : s_5_2 184 # ASSIGN : s_5_3 353 # ASSIGN : s_5_4 823 # ASSIGN : s_5_5 1144 # ASSIGN : s_5_6 379 # ASSIGN : s_5_7 1016 # ASSIGN : s_6_0 66 # ASSIGN : s_6_1 183 # ASSIGN : s_6_2 253 # ASSIGN : s_6_3 549 # ASSIGN : s_6_4 945 # ASSIGN : s_6_5 1276 # ASSIGN : s_6_6 1133 # ASSIGN : s_6_7 1158 # ASSIGN : s_7_0 763 # ASSIGN : s_7_1 215 # ASSIGN : s_7_2 581 # ASSIGN : s_7_3 1181 # ASSIGN : s_7_4 1123 # ASSIGN : s_7_5 1282 # ASSIGN : s_7_6 1135 # ASSIGN : s_7_7 1228 SHOW_RESULT 1285 END : 1285 (0 seconds) [Mon Jun 19 12:28:15 2006] SHOW_RESULT 1285 CPU : 0.25 = 0.25 + 0 + 0 + 0 # BOUND : makespan 1000 1285 MODIFY_CNF 1142 BEGIN : [Mon Jun 19 12:28:15 2006] MODIFY_CNF 1142 END : 46301594 bytes (0 seconds) [Mon Jun 19 12:28:15 2006] MODIFY_CNF 1142 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1142 BEGIN : [Mon Jun 19 12:28:15 2006] CMD : minisat /tmp/csp2sat29544.cnf /tmp/csp2sat29544.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1134303 3265710 | 378101 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 1 (0 /sec) decisions : 181 (62 /sec) propagations : 142220 (49041 /sec) conflict literals : 19 (0.00 % deleted) Memory used : 85.48 MB CPU time : 2.9 s SATISFIABLE VERIFY_CNF 1142 END : (3 seconds) [Mon Jun 19 12:28:18 2006] VERIFY_CNF 1142 CPU : 3.22 = 0 + 0 + 2.97 + 0.25 # RESULT : makespan 1142 SATISFIABLE SHOW_RESULT 1142 BEGIN : [Mon Jun 19 12:28:18 2006] # ASSIGN : makespan 1142 # ASSIGN : s_0_0 705 # ASSIGN : s_0_1 926 # ASSIGN : s_0_2 497 # ASSIGN : s_0_3 376 # ASSIGN : s_0_4 602 # ASSIGN : s_0_5 2 # ASSIGN : s_0_6 33 # ASSIGN : s_0_7 65 # ASSIGN : s_1_0 453 # ASSIGN : s_1_1 359 # ASSIGN : s_1_2 664 # ASSIGN : s_1_3 762 # ASSIGN : s_1_4 4 # ASSIGN : s_1_5 127 # ASSIGN : s_1_6 57 # ASSIGN : s_1_7 397 # ASSIGN : s_2_0 820 # ASSIGN : s_2_1 269 # ASSIGN : s_2_2 963 # ASSIGN : s_2_3 103 # ASSIGN : s_2_4 666 # ASSIGN : s_2_5 328 # ASSIGN : s_2_6 156 # ASSIGN : s_2_7 526 # ASSIGN : s_3_0 1059 # ASSIGN : s_3_1 109 # ASSIGN : s_3_2 38 # ASSIGN : s_3_3 219 # ASSIGN : s_3_4 342 # ASSIGN : s_3_5 639 # ASSIGN : s_3_6 269 # ASSIGN : s_3_7 555 # ASSIGN : s_4_0 542 # ASSIGN : s_4_1 785 # ASSIGN : s_4_2 8 # ASSIGN : s_4_3 244 # ASSIGN : s_4_4 46 # ASSIGN : s_4_5 819 # ASSIGN : s_4_6 322 # ASSIGN : s_4_7 717 # ASSIGN : s_5_0 1137 # ASSIGN : s_5_1 42 # ASSIGN : s_5_2 158 # ASSIGN : s_5_3 350 # ASSIGN : s_5_4 227 # ASSIGN : s_5_5 1001 # ASSIGN : s_5_6 429 # ASSIGN : s_5_7 873 # ASSIGN : s_6_0 8 # ASSIGN : s_6_1 235 # ASSIGN : s_6_2 267 # ASSIGN : s_6_3 529 # ASSIGN : s_6_4 835 # ASSIGN : s_6_5 1133 # ASSIGN : s_6_6 1013 # ASSIGN : s_6_7 1015 # ASSIGN : s_7_0 125 # ASSIGN : s_7_1 415 # ASSIGN : s_7_2 781 # ASSIGN : s_7_3 980 # ASSIGN : s_7_4 1027 # ASSIGN : s_7_5 1139 # ASSIGN : s_7_6 1039 # ASSIGN : s_7_7 1085 SHOW_RESULT 1142 END : 1142 (1 seconds) [Mon Jun 19 12:28:19 2006] SHOW_RESULT 1142 CPU : 0.239999999999999 = 0.219999999999999 + 0.02 + 0 + 0 # BOUND : makespan 1000 1142 MODIFY_CNF 1071 BEGIN : [Mon Jun 19 12:28:19 2006] MODIFY_CNF 1071 END : 46301593 bytes (0 seconds) [Mon Jun 19 12:28:19 2006] MODIFY_CNF 1071 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1071 BEGIN : [Mon Jun 19 12:28:19 2006] CMD : minisat /tmp/csp2sat29544.cnf /tmp/csp2sat29544.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1070687 3074862 | 356895 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 3 (1 /sec) decisions : 147 (49 /sec) propagations : 146949 (48659 /sec) conflict literals : 38 (2.56 % deleted) Memory used : 85.48 MB CPU time : 3.02 s SATISFIABLE VERIFY_CNF 1071 END : (3 seconds) [Mon Jun 19 12:28:22 2006] VERIFY_CNF 1071 CPU : 3.37 = 0 + 0.01 + 3.09 + 0.27 # RESULT : makespan 1071 SATISFIABLE SHOW_RESULT 1071 BEGIN : [Mon Jun 19 12:28:22 2006] # ASSIGN : makespan 1071 # ASSIGN : s_0_0 555 # ASSIGN : s_0_1 791 # ASSIGN : s_0_2 450 # ASSIGN : s_0_3 670 # ASSIGN : s_0_4 1007 # ASSIGN : s_0_5 27 # ASSIGN : s_0_6 3 # ASSIGN : s_0_7 75 # ASSIGN : s_1_0 715 # ASSIGN : s_1_1 676 # ASSIGN : s_1_2 904 # ASSIGN : s_1_3 168 # ASSIGN : s_1_4 126 # ASSIGN : s_1_5 442 # ASSIGN : s_1_6 29 # ASSIGN : s_1_7 386 # ASSIGN : s_2_0 412 # ASSIGN : s_2_1 1012 # ASSIGN : s_2_2 233 # ASSIGN : s_2_3 46 # ASSIGN : s_2_4 841 # ASSIGN : s_2_5 643 # ASSIGN : s_2_6 99 # ASSIGN : s_2_7 614 # ASSIGN : s_3_0 804 # ASSIGN : s_3_1 7 # ASSIGN : s_3_2 593 # ASSIGN : s_3_3 117 # ASSIGN : s_3_4 269 # ASSIGN : s_3_5 882 # ASSIGN : s_3_6 212 # ASSIGN : s_3_7 664 # ASSIGN : s_4_0 908 # ASSIGN : s_4_1 714 # ASSIGN : s_4_2 420 # ASSIGN : s_4_3 824 # ASSIGN : s_4_4 482 # ASSIGN : s_4_5 58 # ASSIGN : s_4_6 265 # ASSIGN : s_4_7 748 # ASSIGN : s_5_0 0 # ASSIGN : s_5_1 173 # ASSIGN : s_5_2 1002 # ASSIGN : s_5_3 142 # ASSIGN : s_5_4 11 # ASSIGN : s_5_5 240 # ASSIGN : s_5_6 372 # ASSIGN : s_5_7 816 # ASSIGN : s_6_0 295 # ASSIGN : s_6_1 263 # ASSIGN : s_6_2 3 # ASSIGN : s_6_3 430 # ASSIGN : s_6_4 663 # ASSIGN : s_6_5 1062 # ASSIGN : s_6_6 942 # ASSIGN : s_6_7 944 # ASSIGN : s_7_0 5 # ASSIGN : s_7_1 310 # ASSIGN : s_7_2 720 # ASSIGN : s_7_3 902 # ASSIGN : s_7_4 995 # ASSIGN : s_7_5 1068 # ASSIGN : s_7_6 949 # ASSIGN : s_7_7 1014 SHOW_RESULT 1071 END : 1071 (0 seconds) [Mon Jun 19 12:28:22 2006] SHOW_RESULT 1071 CPU : 0.25 = 0.25 + 0 + 0 + 0 # BOUND : makespan 1000 1071 MODIFY_CNF 1035 BEGIN : [Mon Jun 19 12:28:22 2006] MODIFY_CNF 1035 END : 46301593 bytes (0 seconds) [Mon Jun 19 12:28:22 2006] MODIFY_CNF 1035 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1035 BEGIN : [Mon Jun 19 12:28:22 2006] CMD : minisat /tmp/csp2sat29544.cnf /tmp/csp2sat29544.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1038431 2978094 | 346143 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 60 (17 /sec) decisions : 200 (57 /sec) propagations : 552563 (157425 /sec) conflict literals : 2471 (11.31 % deleted) Memory used : 85.48 MB CPU time : 3.51 s SATISFIABLE VERIFY_CNF 1035 END : (4 seconds) [Mon Jun 19 12:28:26 2006] VERIFY_CNF 1035 CPU : 3.82 = 0 + 0 + 3.59 + 0.23 # RESULT : makespan 1035 SATISFIABLE SHOW_RESULT 1035 BEGIN : [Mon Jun 19 12:28:26 2006] # ASSIGN : makespan 1035 # ASSIGN : s_0_0 920 # ASSIGN : s_0_1 704 # ASSIGN : s_0_2 339 # ASSIGN : s_0_3 497 # ASSIGN : s_0_4 640 # ASSIGN : s_0_5 466 # ASSIGN : s_0_6 1 # ASSIGN : s_0_7 25 # ASSIGN : s_1_0 392 # ASSIGN : s_1_1 955 # ASSIGN : s_1_2 238 # ASSIGN : s_1_3 618 # ASSIGN : s_1_4 993 # ASSIGN : s_1_5 5 # ASSIGN : s_1_6 836 # ASSIGN : s_1_7 336 # ASSIGN : s_2_0 646 # ASSIGN : s_2_1 139 # ASSIGN : s_2_2 856 # ASSIGN : s_2_3 433 # ASSIGN : s_2_4 486 # ASSIGN : s_2_5 206 # ASSIGN : s_2_6 26 # ASSIGN : s_2_7 404 # ASSIGN : s_3_0 314 # ASSIGN : s_3_1 198 # ASSIGN : s_3_2 19 # ASSIGN : s_3_3 115 # ASSIGN : s_3_4 753 # ASSIGN : s_3_5 532 # ASSIGN : s_3_6 140 # ASSIGN : s_3_7 448 # ASSIGN : s_4_0 481 # ASSIGN : s_4_1 921 # ASSIGN : s_4_2 163 # ASSIGN : s_4_3 957 # ASSIGN : s_4_4 300 # ASSIGN : s_4_5 712 # ASSIGN : s_4_6 193 # ASSIGN : s_4_7 644 # ASSIGN : s_5_0 309 # ASSIGN : s_5_1 23 # ASSIGN : s_5_2 90 # ASSIGN : s_5_3 159 # ASSIGN : s_5_4 185 # ASSIGN : s_5_5 894 # ASSIGN : s_5_6 322 # ASSIGN : s_5_7 766 # ASSIGN : s_6_0 789 # ASSIGN : s_6_1 994 # ASSIGN : s_6_2 444 # ASSIGN : s_6_3 200 # ASSIGN : s_6_4 7 # ASSIGN : s_6_5 1026 # ASSIGN : s_6_6 906 # ASSIGN : s_6_7 908 # ASSIGN : s_7_0 18 # ASSIGN : s_7_1 308 # ASSIGN : s_7_2 674 # ASSIGN : s_7_3 873 # ASSIGN : s_7_4 966 # ASSIGN : s_7_5 1032 # ASSIGN : s_7_6 920 # ASSIGN : s_7_7 978 SHOW_RESULT 1035 END : 1035 (0 seconds) [Mon Jun 19 12:28:26 2006] SHOW_RESULT 1035 CPU : 0.240000000000004 = 0.230000000000004 + 0.01 + 0 + 0 # BOUND : makespan 1000 1035 MODIFY_CNF 1017 BEGIN : [Mon Jun 19 12:28:26 2006] MODIFY_CNF 1017 END : 46301593 bytes (0 seconds) [Mon Jun 19 12:28:26 2006] MODIFY_CNF 1017 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1017 BEGIN : [Mon Jun 19 12:28:26 2006] CMD : minisat /tmp/csp2sat29544.cnf /tmp/csp2sat29544.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1022303 2929710 | 340767 0 0 nan | 0.000 % | | 101 | 1022303 2929710 | 374843 101 3306 32.7 | 57.802 % | ============================================================================== restarts : 2 conflicts : 121 (32 /sec) decisions : 352 (92 /sec) propagations : 844191 (220415 /sec) conflict literals : 3627 (11.36 % deleted) Memory used : 85.50 MB CPU time : 3.83 s SATISFIABLE VERIFY_CNF 1017 END : (5 seconds) [Mon Jun 19 12:28:31 2006] VERIFY_CNF 1017 CPU : 4.18 = 0 + 0 + 3.9 + 0.28 # RESULT : makespan 1017 SATISFIABLE SHOW_RESULT 1017 BEGIN : [Mon Jun 19 12:28:31 2006] # ASSIGN : makespan 1017 # ASSIGN : s_0_0 4 # ASSIGN : s_0_1 689 # ASSIGN : s_0_2 454 # ASSIGN : s_0_3 559 # ASSIGN : s_0_4 922 # ASSIGN : s_0_5 986 # ASSIGN : s_0_6 119 # ASSIGN : s_0_7 143 # ASSIGN : s_1_0 542 # ASSIGN : s_1_1 979 # ASSIGN : s_1_2 356 # ASSIGN : s_1_3 746 # ASSIGN : s_1_4 489 # ASSIGN : s_1_5 0 # ASSIGN : s_1_6 207 # ASSIGN : s_1_7 670 # ASSIGN : s_2_0 399 # ASSIGN : s_2_1 905 # ASSIGN : s_2_2 608 # ASSIGN : s_2_3 964 # ASSIGN : s_2_4 8 # ASSIGN : s_2_5 201 # ASSIGN : s_2_6 792 # ASSIGN : s_2_7 573 # ASSIGN : s_3_0 631 # ASSIGN : s_3_1 175 # ASSIGN : s_3_2 285 # ASSIGN : s_3_3 426 # ASSIGN : s_3_4 709 # ASSIGN : s_3_5 451 # ASSIGN : s_3_6 4 # ASSIGN : s_3_7 933 # ASSIGN : s_4_0 119 # ASSIGN : s_4_1 61 # ASSIGN : s_4_2 572 # ASSIGN : s_4_3 481 # ASSIGN : s_4_4 300 # ASSIGN : s_4_5 672 # ASSIGN : s_4_6 910 # ASSIGN : s_4_7 602 # ASSIGN : s_5_0 721 # ASSIGN : s_5_1 95 # ASSIGN : s_5_2 26 # ASSIGN : s_5_3 0 # ASSIGN : s_5_4 162 # ASSIGN : s_5_5 854 # ASSIGN : s_5_6 277 # ASSIGN : s_5_7 726 # ASSIGN : s_6_0 282 # ASSIGN : s_6_1 17 # ASSIGN : s_6_2 787 # ASSIGN : s_6_3 49 # ASSIGN : s_6_4 531 # ASSIGN : s_6_5 445 # ASSIGN : s_6_6 2 # ASSIGN : s_6_7 461 # ASSIGN : s_7_0 727 # ASSIGN : s_7_1 303 # ASSIGN : s_7_2 103 # ASSIGN : s_7_3 680 # ASSIGN : s_7_4 288 # ASSIGN : s_7_5 669 # ASSIGN : s_7_6 57 # ASSIGN : s_7_7 3 SHOW_RESULT 1017 END : 1017 (0 seconds) [Mon Jun 19 12:28:31 2006] SHOW_RESULT 1017 CPU : 0.240000000000009 = 0.240000000000009 + 0 + 0 + 0 # BOUND : makespan 1000 1017 MODIFY_CNF 1008 BEGIN : [Mon Jun 19 12:28:31 2006] MODIFY_CNF 1008 END : 46301593 bytes (0 seconds) [Mon Jun 19 12:28:31 2006] MODIFY_CNF 1008 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1008 BEGIN : [Mon Jun 19 12:28:31 2006] CMD : minisat /tmp/csp2sat29544.cnf /tmp/csp2sat29544.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1014239 2905518 | 338079 0 0 nan | 0.000 % | | 100 | 1014239 2905518 | 371886 100 3382 33.8 | 58.222 % | ============================================================================== restarts : 2 conflicts : 198 (45 /sec) decisions : 463 (106 /sec) propagations : 1334087 (304586 /sec) conflict literals : 5137 (16.39 % deleted) Memory used : 85.50 MB CPU time : 4.38 s SATISFIABLE VERIFY_CNF 1008 END : (5 seconds) [Mon Jun 19 12:28:36 2006] VERIFY_CNF 1008 CPU : 4.73 = 0 + 0 + 4.46 + 0.27 # RESULT : makespan 1008 SATISFIABLE SHOW_RESULT 1008 BEGIN : [Mon Jun 19 12:28:36 2006] # ASSIGN : makespan 1008 # ASSIGN : s_0_0 509 # ASSIGN : s_0_1 792 # ASSIGN : s_0_2 659 # ASSIGN : s_0_3 388 # ASSIGN : s_0_4 13 # ASSIGN : s_0_5 628 # ASSIGN : s_0_6 764 # ASSIGN : s_0_7 77 # ASSIGN : s_1_0 624 # ASSIGN : s_1_1 752 # ASSIGN : s_1_2 283 # ASSIGN : s_1_3 790 # ASSIGN : s_1_4 433 # ASSIGN : s_1_5 44 # ASSIGN : s_1_6 498 # ASSIGN : s_1_7 568 # ASSIGN : s_2_0 2 # ASSIGN : s_2_1 198 # ASSIGN : s_2_2 411 # ASSIGN : s_2_3 145 # ASSIGN : s_2_4 257 # ASSIGN : s_2_5 668 # ASSIGN : s_2_6 895 # ASSIGN : s_2_7 866 # ASSIGN : s_3_0 431 # ASSIGN : s_3_1 88 # ASSIGN : s_3_2 1 # ASSIGN : s_3_3 765 # ASSIGN : s_3_4 795 # ASSIGN : s_3_5 245 # ASSIGN : s_3_6 601 # ASSIGN : s_3_7 654 # ASSIGN : s_4_0 151 # ASSIGN : s_4_1 13 # ASSIGN : s_4_2 381 # ASSIGN : s_4_3 67 # ASSIGN : s_4_4 607 # ASSIGN : s_4_5 425 # ASSIGN : s_4_6 788 # ASSIGN : s_4_7 940 # ASSIGN : s_5_0 1003 # ASSIGN : s_5_1 671 # ASSIGN : s_5_2 590 # ASSIGN : s_5_3 5 # ASSIGN : s_5_4 475 # ASSIGN : s_5_5 871 # ASSIGN : s_5_6 31 # ASSIGN : s_5_7 738 # ASSIGN : s_6_0 314 # ASSIGN : s_6_1 47 # ASSIGN : s_6_2 778 # ASSIGN : s_6_3 529 # ASSIGN : s_6_4 79 # ASSIGN : s_6_5 38 # ASSIGN : s_6_6 762 # ASSIGN : s_6_7 459 # ASSIGN : s_7_0 713 # ASSIGN : s_7_1 301 # ASSIGN : s_7_2 72 # ASSIGN : s_7_3 254 # ASSIGN : s_7_4 1 # ASSIGN : s_7_5 15 # ASSIGN : s_7_6 667 # ASSIGN : s_7_7 18 SHOW_RESULT 1008 END : 1008 (0 seconds) [Mon Jun 19 12:28:36 2006] SHOW_RESULT 1008 CPU : 0.239999999999999 = 0.219999999999999 + 0.02 + 0 + 0 # BOUND : makespan 1000 1008 MODIFY_CNF 1004 BEGIN : [Mon Jun 19 12:28:36 2006] MODIFY_CNF 1004 END : 46301592 bytes (0 seconds) [Mon Jun 19 12:28:36 2006] MODIFY_CNF 1004 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1004 BEGIN : [Mon Jun 19 12:28:36 2006] CMD : minisat /tmp/csp2sat29544.cnf /tmp/csp2sat29544.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1010655 2894766 | 336885 0 0 nan | 0.000 % | | 100 | 1010655 2894766 | 370573 100 4531 45.3 | 58.409 % | | 251 | 1010655 2894766 | 407630 251 8261 32.9 | 58.409 % | | 477 | 1010655 2894766 | 448393 477 15268 32.0 | 58.409 % | ============================================================================== restarts : 4 conflicts : 508 (77 /sec) decisions : 992 (150 /sec) propagations : 3547070 (535811 /sec) conflict literals : 16022 (22.16 % deleted) Memory used : 85.50 MB CPU time : 6.62 s SATISFIABLE VERIFY_CNF 1004 END : (7 seconds) [Mon Jun 19 12:28:43 2006] VERIFY_CNF 1004 CPU : 6.99 = 0 + 0 + 6.7 + 0.29 # RESULT : makespan 1004 SATISFIABLE SHOW_RESULT 1004 BEGIN : [Mon Jun 19 12:28:43 2006] # ASSIGN : makespan 1004 # ASSIGN : s_0_0 257 # ASSIGN : s_0_1 788 # ASSIGN : s_0_2 372 # ASSIGN : s_0_3 88 # ASSIGN : s_0_4 24 # ASSIGN : s_0_5 225 # ASSIGN : s_0_6 0 # ASSIGN : s_0_7 477 # ASSIGN : s_1_0 168 # ASSIGN : s_1_1 130 # ASSIGN : s_1_2 274 # ASSIGN : s_1_3 673 # ASSIGN : s_1_4 88 # ASSIGN : s_1_5 472 # ASSIGN : s_1_6 934 # ASSIGN : s_1_7 21 # ASSIGN : s_2_0 454 # ASSIGN : s_2_1 168 # ASSIGN : s_2_2 795 # ASSIGN : s_2_3 2 # ASSIGN : s_2_4 625 # ASSIGN : s_2_5 256 # ASSIGN : s_2_6 55 # ASSIGN : s_2_7 227 # ASSIGN : s_3_0 376 # ASSIGN : s_3_1 669 # ASSIGN : s_3_2 494 # ASSIGN : s_3_3 644 # ASSIGN : s_3_4 779 # ASSIGN : s_3_5 45 # ASSIGN : s_3_6 239 # ASSIGN : s_3_7 292 # ASSIGN : s_4_0 5 # ASSIGN : s_4_1 635 # ASSIGN : s_4_2 974 # ASSIGN : s_4_3 209 # ASSIGN : s_4_4 444 # ASSIGN : s_4_5 688 # ASSIGN : s_4_6 321 # ASSIGN : s_4_7 870 # ASSIGN : s_5_0 0 # ASSIGN : s_5_1 10 # ASSIGN : s_5_2 205 # ASSIGN : s_5_3 287 # ASSIGN : s_5_4 313 # ASSIGN : s_5_5 872 # ASSIGN : s_5_6 428 # ASSIGN : s_5_7 77 # ASSIGN : s_6_0 887 # ASSIGN : s_6_1 98 # ASSIGN : s_6_2 565 # ASSIGN : s_6_3 332 # ASSIGN : s_6_4 135 # ASSIGN : s_6_5 39 # ASSIGN : s_6_6 885 # ASSIGN : s_6_7 800 # ASSIGN : s_7_0 597 # ASSIGN : s_7_1 231 # ASSIGN : s_7_2 3 # ASSIGN : s_7_3 891 # ASSIGN : s_7_4 992 # ASSIGN : s_7_5 0 # ASSIGN : s_7_6 185 # ASSIGN : s_7_7 938 SHOW_RESULT 1004 END : 1004 (0 seconds) [Mon Jun 19 12:28:43 2006] SHOW_RESULT 1004 CPU : 0.23999999999999 = 0.22999999999999 + 0.01 + 0 + 0 # BOUND : makespan 1000 1004 MODIFY_CNF 1002 BEGIN : [Mon Jun 19 12:28:43 2006] MODIFY_CNF 1002 END : 46301592 bytes (0 seconds) [Mon Jun 19 12:28:43 2006] MODIFY_CNF 1002 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1002 BEGIN : [Mon Jun 19 12:28:43 2006] CMD : minisat /tmp/csp2sat29544.cnf /tmp/csp2sat29544.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1008863 2889390 | 336287 0 0 nan | 0.000 % | | 100 | 1008863 2889390 | 369915 100 3997 40.0 | 58.502 % | | 250 | 1008863 2889390 | 406907 250 9722 38.9 | 58.502 % | ============================================================================== restarts : 3 conflicts : 261 (54 /sec) decisions : 518 (107 /sec) propagations : 1591716 (328867 /sec) conflict literals : 9934 (10.68 % deleted) Memory used : 85.50 MB CPU time : 4.84 s SATISFIABLE VERIFY_CNF 1002 END : (5 seconds) [Mon Jun 19 12:28:48 2006] VERIFY_CNF 1002 CPU : 5.18000000000001 = 0.0100000000000051 + 0 + 4.9 + 0.27 # RESULT : makespan 1002 SATISFIABLE SHOW_RESULT 1002 BEGIN : [Mon Jun 19 12:28:48 2006] # ASSIGN : makespan 1002 # ASSIGN : s_0_0 635 # ASSIGN : s_0_1 419 # ASSIGN : s_0_2 3 # ASSIGN : s_0_3 786 # ASSIGN : s_0_4 938 # ASSIGN : s_0_5 907 # ASSIGN : s_0_6 762 # ASSIGN : s_0_7 108 # ASSIGN : s_1_0 913 # ASSIGN : s_1_1 98 # ASSIGN : s_1_2 355 # ASSIGN : s_1_3 137 # ASSIGN : s_1_4 16 # ASSIGN : s_1_5 574 # ASSIGN : s_1_6 843 # ASSIGN : s_1_7 518 # ASSIGN : s_2_0 202 # ASSIGN : s_2_1 360 # ASSIGN : s_2_2 453 # ASSIGN : s_2_3 949 # ASSIGN : s_2_4 784 # ASSIGN : s_2_5 4 # ASSIGN : s_2_6 649 # ASSIGN : s_2_7 424 # ASSIGN : s_3_0 124 # ASSIGN : s_3_1 250 # ASSIGN : s_3_2 862 # ASSIGN : s_3_3 360 # ASSIGN : s_3_4 565 # ASSIGN : s_3_5 385 # ASSIGN : s_3_6 947 # ASSIGN : s_3_7 778 # ASSIGN : s_4_0 750 # ASSIGN : s_4_1 168 # ASSIGN : s_4_2 133 # ASSIGN : s_4_3 672 # ASSIGN : s_4_4 384 # ASSIGN : s_4_5 202 # ASSIGN : s_4_6 10 # ASSIGN : s_4_7 934 # ASSIGN : s_5_0 2 # ASSIGN : s_5_1 21 # ASSIGN : s_5_2 933 # ASSIGN : s_5_3 907 # ASSIGN : s_5_4 88 # ASSIGN : s_5_5 775 # ASSIGN : s_5_6 203 # ASSIGN : s_5_7 647 # ASSIGN : s_6_0 7 # ASSIGN : s_6_1 136 # ASSIGN : s_6_2 632 # ASSIGN : s_6_3 399 # ASSIGN : s_6_4 206 # ASSIGN : s_6_5 994 # ASSIGN : s_6_6 1000 # ASSIGN : s_6_7 864 # ASSIGN : s_7_0 345 # ASSIGN : s_7_1 636 # ASSIGN : s_7_2 163 # ASSIGN : s_7_3 70 # ASSIGN : s_7_4 58 # ASSIGN : s_7_5 1 # ASSIGN : s_7_6 117 # ASSIGN : s_7_7 4 SHOW_RESULT 1002 END : 1002 (0 seconds) [Mon Jun 19 12:28:48 2006] SHOW_RESULT 1002 CPU : 0.23999999999999 = 0.22999999999999 + 0.01 + 0 + 0 # BOUND : makespan 1000 1002 MODIFY_CNF 1001 BEGIN : [Mon Jun 19 12:28:48 2006] MODIFY_CNF 1001 END : 46301592 bytes (0 seconds) [Mon Jun 19 12:28:48 2006] MODIFY_CNF 1001 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1001 BEGIN : [Mon Jun 19 12:28:48 2006] CMD : minisat /tmp/csp2sat29544.cnf /tmp/csp2sat29544.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1007967 2886702 | 335989 0 0 nan | 0.000 % | | 100 | 1007967 2886702 | 369587 100 3255 32.5 | 58.549 % | | 250 | 1007967 2886702 | 406546 250 6548 26.2 | 58.549 % | | 475 | 1007967 2886702 | 447201 475 12030 25.3 | 58.549 % | | 812 | 1007967 2886702 | 491921 812 19513 24.0 | 58.549 % | ============================================================================== restarts : 5 conflicts : 935 (101 /sec) decisions : 1568 (170 /sec) propagations : 5885374 (637635 /sec) conflict literals : 22109 (21.36 % deleted) Memory used : 85.50 MB CPU time : 9.23 s SATISFIABLE VERIFY_CNF 1001 END : (10 seconds) [Mon Jun 19 12:28:58 2006] VERIFY_CNF 1001 CPU : 9.51 = 0 + 0.01 + 9.29 + 0.21 # RESULT : makespan 1001 SATISFIABLE SHOW_RESULT 1001 BEGIN : [Mon Jun 19 12:28:58 2006] # ASSIGN : makespan 1001 # ASSIGN : s_0_0 548 # ASSIGN : s_0_1 785 # ASSIGN : s_0_2 77 # ASSIGN : s_0_3 664 # ASSIGN : s_0_4 3 # ASSIGN : s_0_5 182 # ASSIGN : s_0_6 213 # ASSIGN : s_0_7 237 # ASSIGN : s_1_0 5 # ASSIGN : s_1_1 164 # ASSIGN : s_1_2 257 # ASSIGN : s_1_3 446 # ASSIGN : s_1_4 755 # ASSIGN : s_1_5 797 # ASSIGN : s_1_6 376 # ASSIGN : s_1_7 694 # ASSIGN : s_2_0 858 # ASSIGN : s_2_1 36 # ASSIGN : s_2_2 625 # ASSIGN : s_2_3 805 # ASSIGN : s_2_4 257 # ASSIGN : s_2_5 411 # ASSIGN : s_2_6 95 # ASSIGN : s_2_7 208 # ASSIGN : s_3_0 780 # ASSIGN : s_3_1 274 # ASSIGN : s_3_2 186 # ASSIGN : s_3_3 892 # ASSIGN : s_3_4 542 # ASSIGN : s_3_5 2 # ASSIGN : s_3_6 489 # ASSIGN : s_3_7 917 # ASSIGN : s_4_0 385 # ASSIGN : s_4_1 2 # ASSIGN : s_4_2 355 # ASSIGN : s_4_3 923 # ASSIGN : s_4_4 67 # ASSIGN : s_4_5 609 # ASSIGN : s_4_6 248 # ASSIGN : s_4_7 849 # ASSIGN : s_5_0 0 # ASSIGN : s_5_1 202 # ASSIGN : s_5_2 5 # ASSIGN : s_5_3 401 # ASSIGN : s_5_4 427 # ASSIGN : s_5_5 269 # ASSIGN : s_5_6 557 # ASSIGN : s_5_7 74 # ASSIGN : s_6_0 663 # ASSIGN : s_6_1 130 # ASSIGN : s_6_2 395 # ASSIGN : s_6_3 162 # ASSIGN : s_6_4 808 # ASSIGN : s_6_5 791 # ASSIGN : s_6_6 93 # ASSIGN : s_6_7 4 # ASSIGN : s_7_0 94 # ASSIGN : s_7_1 384 # ASSIGN : s_7_2 804 # ASSIGN : s_7_3 47 # ASSIGN : s_7_4 986 # ASSIGN : s_7_5 998 # ASSIGN : s_7_6 1 # ASSIGN : s_7_7 750 SHOW_RESULT 1001 END : 1001 (0 seconds) [Mon Jun 19 12:28:58 2006] SHOW_RESULT 1001 CPU : 0.240000000000004 = 0.230000000000004 + 0.01 + 0 + 0 # BOUND : makespan 1000 1001 MODIFY_CNF 1000 BEGIN : [Mon Jun 19 12:28:58 2006] MODIFY_CNF 1000 END : 46301592 bytes (0 seconds) [Mon Jun 19 12:28:58 2006] MODIFY_CNF 1000 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1000 BEGIN : [Mon Jun 19 12:28:58 2006] CMD : minisat /tmp/csp2sat29544.cnf /tmp/csp2sat29544.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1007072 2884014 | 335690 0 0 nan | 0.000 % | | 101 | 1007072 2884014 | 369259 101 2957 29.3 | 58.595 % | | 251 | 1007072 2884014 | 406184 251 6700 26.7 | 58.595 % | | 476 | 1007072 2884014 | 446803 476 13003 27.3 | 58.595 % | | 813 | 1007072 2884014 | 491483 813 19139 23.5 | 58.595 % | | 1319 | 1007072 2884014 | 540632 1319 33680 25.5 | 58.595 % | | 2078 | 1007072 2884014 | 594695 2078 58300 28.1 | 58.595 % | ============================================================================== restarts : 7 conflicts : 2660 (137 /sec) decisions : 4211 (218 /sec) propagations : 16065040 (829806 /sec) conflict literals : 71129 (19.55 % deleted) Memory used : 85.50 MB CPU time : 19.36 s SATISFIABLE VERIFY_CNF 1000 END : (20 seconds) [Mon Jun 19 12:29:18 2006] VERIFY_CNF 1000 CPU : 19.74 = 0 + 0 + 19.42 + 0.32 # RESULT : makespan 1000 SATISFIABLE SHOW_RESULT 1000 BEGIN : [Mon Jun 19 12:29:18 2006] # ASSIGN : makespan 1000 # ASSIGN : s_0_0 453 # ASSIGN : s_0_1 696 # ASSIGN : s_0_2 348 # ASSIGN : s_0_3 575 # ASSIGN : s_0_4 912 # ASSIGN : s_0_5 6 # ASSIGN : s_0_6 976 # ASSIGN : s_0_7 37 # ASSIGN : s_1_0 568 # ASSIGN : s_1_1 658 # ASSIGN : s_1_2 250 # ASSIGN : s_1_3 32 # ASSIGN : s_1_4 407 # ASSIGN : s_1_5 796 # ASSIGN : s_1_6 711 # ASSIGN : s_1_7 450 # ASSIGN : s_2_0 657 # ASSIGN : s_2_1 12 # ASSIGN : s_2_2 71 # ASSIGN : s_2_3 947 # ASSIGN : s_2_4 449 # ASSIGN : s_2_5 251 # ASSIGN : s_2_6 834 # ASSIGN : s_2_7 805 # ASSIGN : s_3_0 917 # ASSIGN : s_3_1 84 # ASSIGN : s_3_2 0 # ASSIGN : s_3_3 877 # ASSIGN : s_3_4 194 # ASSIGN : s_3_5 601 # ASSIGN : s_3_6 781 # ASSIGN : s_3_7 506 # ASSIGN : s_4_0 290 # ASSIGN : s_4_1 256 # ASSIGN : s_4_2 458 # ASSIGN : s_4_3 784 # ASSIGN : s_4_4 603 # ASSIGN : s_4_5 69 # ASSIGN : s_4_6 496 # ASSIGN : s_4_7 862 # ASSIGN : s_5_0 995 # ASSIGN : s_5_1 928 # ASSIGN : s_5_2 718 # ASSIGN : s_5_3 902 # ASSIGN : s_5_4 787 # ASSIGN : s_5_5 458 # ASSIGN : s_5_6 14 # ASSIGN : s_5_7 590 # ASSIGN : s_6_0 800 # ASSIGN : s_6_1 223 # ASSIGN : s_6_2 488 # ASSIGN : s_6_3 255 # ASSIGN : s_6_4 16 # ASSIGN : s_6_5 790 # ASSIGN : s_6_6 12 # ASSIGN : s_6_7 930 # ASSIGN : s_7_0 0 # ASSIGN : s_7_1 290 # ASSIGN : s_7_2 803 # ASSIGN : s_7_3 702 # ASSIGN : s_7_4 985 # ASSIGN : s_7_5 997 # ASSIGN : s_7_6 656 # ASSIGN : s_7_7 749 SHOW_RESULT 1000 END : 1000 (0 seconds) [Mon Jun 19 12:29:18 2006] SHOW_RESULT 1000 CPU : 0.240000000000004 = 0.230000000000004 + 0.01 + 0 + 0 # BOUND : makespan 1000 1000 MAIN END : (148 seconds) [Mon Jun 19 12:29:18 2006] MAIN CPU : 147.61 = 79.67 + 0.45 + 64.49 + 3