# TIMEOUT 18000 MAIN BEGIN : [Mon Jun 19 07:22:46 2006] READ BEGIN : csp/j8-per10-0.csp [Mon Jun 19 07:22:46 2006] READ END : csp/j8-per10-0.csp (1 seconds) [Mon Jun 19 07:22:47 2006] READ CPU : 0.94 = 0.92 + 0.02 + 0 + 0 # BOUND : makespan 1000 2588 GENERATE_CNF 2588 BEGIN : [Mon Jun 19 07:22:47 2006] GENERATE_CNF 2588 END : 168310 variables 2481679 clauses 57280792 bytes (93 seconds) [Mon Jun 19 07:24:20 2006] GENERATE_CNF 2588 CPU : 92.77 = 92.33 + 0.44 + 0 + 0 MODIFY_CNF 1794 BEGIN : [Mon Jun 19 07:24:20 2006] MODIFY_CNF 1794 END : 57280798 bytes (0 seconds) [Mon Jun 19 07:24:20 2006] MODIFY_CNF 1794 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1794 BEGIN : [Mon Jun 19 07:24:20 2006] CMD : minisat /tmp/csp2sat23155.cnf /tmp/csp2sat23155.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1768906 5140464 | 589635 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 39 (10 /sec) decisions : 403 (107 /sec) propagations : 556723 (147672 /sec) conflict literals : 1006 (10.02 % deleted) Memory used : 103.78 MB CPU time : 3.77 s SATISFIABLE VERIFY_CNF 1794 END : (4 seconds) [Mon Jun 19 07:24:24 2006] VERIFY_CNF 1794 CPU : 4.15 = 0 + 0 + 3.85 + 0.3 # RESULT : makespan 1794 SATISFIABLE SHOW_RESULT 1794 BEGIN : [Mon Jun 19 07:24:24 2006] # ASSIGN : makespan 1794 # ASSIGN : s_0_0 1643 # ASSIGN : s_0_1 1429 # ASSIGN : s_0_2 431 # ASSIGN : s_0_3 702 # ASSIGN : s_0_4 69 # ASSIGN : s_0_5 805 # ASSIGN : s_0_6 22 # ASSIGN : s_0_7 100 # ASSIGN : s_1_0 1633 # ASSIGN : s_1_1 362 # ASSIGN : s_1_2 518 # ASSIGN : s_1_3 910 # ASSIGN : s_1_4 105 # ASSIGN : s_1_5 1005 # ASSIGN : s_1_6 41 # ASSIGN : s_1_7 542 # ASSIGN : s_2_0 1019 # ASSIGN : s_2_1 222 # ASSIGN : s_2_2 543 # ASSIGN : s_2_3 924 # ASSIGN : s_2_4 224 # ASSIGN : s_2_5 1369 # ASSIGN : s_2_6 86 # ASSIGN : s_2_7 783 # ASSIGN : s_3_0 825 # ASSIGN : s_3_1 1622 # ASSIGN : s_3_2 836 # ASSIGN : s_3_3 968 # ASSIGN : s_3_4 377 # ASSIGN : s_3_5 1565 # ASSIGN : s_3_6 101 # ASSIGN : s_3_7 890 # ASSIGN : s_4_0 330 # ASSIGN : s_4_1 1607 # ASSIGN : s_4_2 1014 # ASSIGN : s_4_3 1176 # ASSIGN : s_4_4 470 # ASSIGN : s_4_5 1604 # ASSIGN : s_4_6 564 # ASSIGN : s_4_7 1093 # ASSIGN : s_5_0 239 # ASSIGN : s_5_1 1484 # ASSIGN : s_5_2 1098 # ASSIGN : s_5_3 1306 # ASSIGN : s_5_4 637 # ASSIGN : s_5_5 1613 # ASSIGN : s_5_6 1000 # ASSIGN : s_5_7 1273 # ASSIGN : s_6_0 221 # ASSIGN : s_6_1 750 # ASSIGN : s_6_2 1175 # ASSIGN : s_6_3 1445 # ASSIGN : s_6_4 865 # ASSIGN : s_6_5 1771 # ASSIGN : s_6_6 1106 # ASSIGN : s_6_7 1434 # ASSIGN : s_7_0 1224 # ASSIGN : s_7_1 794 # ASSIGN : s_7_2 1598 # ASSIGN : s_7_3 1783 # ASSIGN : s_7_4 1688 # ASSIGN : s_7_5 1789 # ASSIGN : s_7_6 1741 # ASSIGN : s_7_7 1725 SHOW_RESULT 1794 END : 1794 (0 seconds) [Mon Jun 19 07:24:24 2006] SHOW_RESULT 1794 CPU : 0.330000000000002 = 0.310000000000002 + 0.02 + 0 + 0 # BOUND : makespan 1000 1794 MODIFY_CNF 1397 BEGIN : [Mon Jun 19 07:24:24 2006] MODIFY_CNF 1397 END : 57280798 bytes (0 seconds) [Mon Jun 19 07:24:24 2006] MODIFY_CNF 1397 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1397 BEGIN : [Mon Jun 19 07:24:24 2006] CMD : minisat /tmp/csp2sat23155.cnf /tmp/csp2sat23155.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1413194 4073328 | 471064 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 7 (2 /sec) decisions : 298 (78 /sec) propagations : 226429 (59430 /sec) conflict literals : 62 (1.59 % deleted) Memory used : 103.78 MB CPU time : 3.81 s SATISFIABLE VERIFY_CNF 1397 END : (5 seconds) [Mon Jun 19 07:24:29 2006] VERIFY_CNF 1397 CPU : 4.19 = 0 + 0 + 3.89 + 0.3 # RESULT : makespan 1397 SATISFIABLE SHOW_RESULT 1397 BEGIN : [Mon Jun 19 07:24:29 2006] # ASSIGN : makespan 1397 # ASSIGN : s_0_0 683 # ASSIGN : s_0_1 97 # ASSIGN : s_0_2 834 # ASSIGN : s_0_3 921 # ASSIGN : s_0_4 44 # ASSIGN : s_0_5 152 # ASSIGN : s_0_6 0 # ASSIGN : s_0_7 352 # ASSIGN : s_1_0 4 # ASSIGN : s_1_1 194 # ASSIGN : s_1_2 1373 # ASSIGN : s_1_3 350 # ASSIGN : s_1_4 75 # ASSIGN : s_1_5 364 # ASSIGN : s_1_6 19 # ASSIGN : s_1_7 728 # ASSIGN : s_2_0 1151 # ASSIGN : s_2_1 352 # ASSIGN : s_2_2 503 # ASSIGN : s_2_3 459 # ASSIGN : s_2_4 199 # ASSIGN : s_2_5 743 # ASSIGN : s_2_6 64 # ASSIGN : s_2_7 969 # ASSIGN : s_3_0 14 # ASSIGN : s_3_1 537 # ASSIGN : s_3_2 25 # ASSIGN : s_3_3 1189 # ASSIGN : s_3_4 355 # ASSIGN : s_3_5 939 # ASSIGN : s_3_6 79 # ASSIGN : s_3_7 1076 # ASSIGN : s_4_0 61 # ASSIGN : s_4_1 354 # ASSIGN : s_4_2 369 # ASSIGN : s_4_3 1024 # ASSIGN : s_4_4 448 # ASSIGN : s_4_5 978 # ASSIGN : s_4_6 542 # ASSIGN : s_4_7 1154 # ASSIGN : s_5_0 201 # ASSIGN : s_5_1 414 # ASSIGN : s_5_2 292 # ASSIGN : s_5_3 782 # ASSIGN : s_5_4 542 # ASSIGN : s_5_5 981 # ASSIGN : s_5_6 1139 # ASSIGN : s_5_7 1237 # ASSIGN : s_6_0 1356 # ASSIGN : s_6_1 709 # ASSIGN : s_6_2 1011 # ASSIGN : s_6_3 24 # ASSIGN : s_6_4 770 # ASSIGN : s_6_5 1374 # ASSIGN : s_6_6 1281 # ASSIGN : s_6_7 1270 # ASSIGN : s_7_0 309 # ASSIGN : s_7_1 753 # ASSIGN : s_7_2 202 # ASSIGN : s_7_3 1183 # ASSIGN : s_7_4 1297 # ASSIGN : s_7_5 1392 # ASSIGN : s_7_6 1350 # ASSIGN : s_7_7 1334 SHOW_RESULT 1397 END : 1397 (0 seconds) [Mon Jun 19 07:24:29 2006] SHOW_RESULT 1397 CPU : 0.320000000000007 = 0.320000000000007 + 0 + 0 + 0 # BOUND : makespan 1000 1397 MODIFY_CNF 1198 BEGIN : [Mon Jun 19 07:24:29 2006] MODIFY_CNF 1198 END : 57280798 bytes (0 seconds) [Mon Jun 19 07:24:29 2006] MODIFY_CNF 1198 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1198 BEGIN : [Mon Jun 19 07:24:29 2006] CMD : minisat /tmp/csp2sat23155.cnf /tmp/csp2sat23155.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1234890 3538416 | 411630 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (1 /sec) decisions : 226 (66 /sec) propagations : 200486 (58451 /sec) conflict literals : 7 (0.00 % deleted) Memory used : 103.78 MB CPU time : 3.43 s SATISFIABLE VERIFY_CNF 1198 END : (4 seconds) [Mon Jun 19 07:24:33 2006] VERIFY_CNF 1198 CPU : 3.92 = 0 + 0 + 3.49 + 0.43 # RESULT : makespan 1198 SATISFIABLE SHOW_RESULT 1198 BEGIN : [Mon Jun 19 07:24:33 2006] # ASSIGN : makespan 1198 # ASSIGN : s_0_0 838 # ASSIGN : s_0_1 687 # ASSIGN : s_0_2 751 # ASSIGN : s_0_3 989 # ASSIGN : s_0_4 29 # ASSIGN : s_0_5 60 # ASSIGN : s_0_6 10 # ASSIGN : s_0_7 293 # ASSIGN : s_1_0 14 # ASSIGN : s_1_1 865 # ASSIGN : s_1_2 1174 # ASSIGN : s_1_3 24 # ASSIGN : s_1_4 1021 # ASSIGN : s_1_5 260 # ASSIGN : s_1_6 110 # ASSIGN : s_1_7 624 # ASSIGN : s_2_0 993 # ASSIGN : s_2_1 17 # ASSIGN : s_2_2 434 # ASSIGN : s_2_3 38 # ASSIGN : s_2_4 199 # ASSIGN : s_2_5 674 # ASSIGN : s_2_6 155 # ASSIGN : s_2_7 870 # ASSIGN : s_3_0 66 # ASSIGN : s_3_1 515 # ASSIGN : s_3_2 12 # ASSIGN : s_3_3 730 # ASSIGN : s_3_4 77 # ASSIGN : s_3_5 938 # ASSIGN : s_3_6 170 # ASSIGN : s_3_7 977 # ASSIGN : s_4_0 212 # ASSIGN : s_4_1 19 # ASSIGN : s_4_2 898 # ASSIGN : s_4_3 82 # ASSIGN : s_4_4 352 # ASSIGN : s_4_5 977 # ASSIGN : s_4_6 446 # ASSIGN : s_4_7 1055 # ASSIGN : s_5_0 373 # ASSIGN : s_5_1 742 # ASSIGN : s_5_2 68 # ASSIGN : s_5_3 234 # ASSIGN : s_5_4 514 # ASSIGN : s_5_5 980 # ASSIGN : s_5_6 882 # ASSIGN : s_5_7 1138 # ASSIGN : s_6_0 127 # ASSIGN : s_6_1 1109 # ASSIGN : s_6_2 145 # ASSIGN : s_6_3 404 # ASSIGN : s_6_4 780 # ASSIGN : s_6_5 1153 # ASSIGN : s_6_6 1029 # ASSIGN : s_6_7 1171 # ASSIGN : s_7_0 464 # ASSIGN : s_7_1 34 # ASSIGN : s_7_2 1002 # ASSIGN : s_7_3 1092 # ASSIGN : s_7_4 1140 # ASSIGN : s_7_5 1177 # ASSIGN : s_7_6 1098 # ASSIGN : s_7_7 1182 SHOW_RESULT 1198 END : 1198 (0 seconds) [Mon Jun 19 07:24:33 2006] SHOW_RESULT 1198 CPU : 0.319999999999993 = 0.319999999999993 + 0 + 0 + 0 # BOUND : makespan 1000 1198 MODIFY_CNF 1099 BEGIN : [Mon Jun 19 07:24:33 2006] MODIFY_CNF 1099 END : 57280798 bytes (0 seconds) [Mon Jun 19 07:24:33 2006] MODIFY_CNF 1099 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1099 BEGIN : [Mon Jun 19 07:24:33 2006] CMD : minisat /tmp/csp2sat23155.cnf /tmp/csp2sat23155.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1146186 3272304 | 382062 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 52 (13 /sec) decisions : 210 (52 /sec) propagations : 444942 (110407 /sec) conflict literals : 1172 (9.92 % deleted) Memory used : 103.78 MB CPU time : 4.03 s SATISFIABLE VERIFY_CNF 1099 END : (4 seconds) [Mon Jun 19 07:24:37 2006] VERIFY_CNF 1099 CPU : 4.36 = 0 + 0 + 4.11 + 0.25 # RESULT : makespan 1099 SATISFIABLE SHOW_RESULT 1099 BEGIN : [Mon Jun 19 07:24:37 2006] # ASSIGN : makespan 1099 # ASSIGN : s_0_0 808 # ASSIGN : s_0_1 1044 # ASSIGN : s_0_2 618 # ASSIGN : s_0_3 705 # ASSIGN : s_0_4 581 # ASSIGN : s_0_5 354 # ASSIGN : s_0_6 4 # ASSIGN : s_0_7 23 # ASSIGN : s_1_0 677 # ASSIGN : s_1_1 202 # ASSIGN : s_1_2 14 # ASSIGN : s_1_3 1085 # ASSIGN : s_1_4 83 # ASSIGN : s_1_5 712 # ASSIGN : s_1_6 38 # ASSIGN : s_1_7 358 # ASSIGN : s_2_0 394 # ASSIGN : s_2_1 52 # ASSIGN : s_2_2 706 # ASSIGN : s_2_3 317 # ASSIGN : s_2_4 946 # ASSIGN : s_2_5 111 # ASSIGN : s_2_6 96 # ASSIGN : s_2_7 599 # ASSIGN : s_3_0 706 # ASSIGN : s_3_1 434 # ASSIGN : s_3_2 1045 # ASSIGN : s_3_3 837 # ASSIGN : s_3_4 612 # ASSIGN : s_3_5 72 # ASSIGN : s_3_6 113 # ASSIGN : s_3_7 759 # ASSIGN : s_4_0 959 # ASSIGN : s_4_1 187 # ASSIGN : s_4_2 310 # ASSIGN : s_4_3 47 # ASSIGN : s_4_4 213 # ASSIGN : s_4_5 307 # ASSIGN : s_4_6 389 # ASSIGN : s_4_7 840 # ASSIGN : s_5_0 717 # ASSIGN : s_5_1 54 # ASSIGN : s_5_2 968 # ASSIGN : s_5_3 177 # ASSIGN : s_5_4 316 # ASSIGN : s_5_5 554 # ASSIGN : s_5_6 825 # ASSIGN : s_5_7 923 # ASSIGN : s_6_0 687 # ASSIGN : s_6_1 7 # ASSIGN : s_6_2 51 # ASSIGN : s_6_3 361 # ASSIGN : s_6_4 705 # ASSIGN : s_6_5 1076 # ASSIGN : s_6_6 967 # ASSIGN : s_6_7 956 # ASSIGN : s_7_0 20 # ASSIGN : s_7_1 606 # ASSIGN : s_7_2 454 # ASSIGN : s_7_3 14 # ASSIGN : s_7_4 544 # ASSIGN : s_7_5 1094 # ASSIGN : s_7_6 1036 # ASSIGN : s_7_7 1078 SHOW_RESULT 1099 END : 1099 (1 seconds) [Mon Jun 19 07:24:38 2006] SHOW_RESULT 1099 CPU : 0.310000000000002 = 0.310000000000002 + 0 + 0 + 0 # BOUND : makespan 1000 1099 MODIFY_CNF 1049 BEGIN : [Mon Jun 19 07:24:38 2006] MODIFY_CNF 1049 END : 57280797 bytes (0 seconds) [Mon Jun 19 07:24:38 2006] MODIFY_CNF 1049 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1049 BEGIN : [Mon Jun 19 07:24:38 2006] CMD : minisat /tmp/csp2sat23155.cnf /tmp/csp2sat23155.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1101386 3137904 | 367128 0 0 nan | 0.000 % | | 101 | 1101386 3137904 | 403840 101 2163 21.4 | 64.158 % | ============================================================================== restarts : 2 conflicts : 148 (30 /sec) decisions : 414 (83 /sec) propagations : 1244714 (250950 /sec) conflict literals : 3027 (18.23 % deleted) Memory used : 103.80 MB CPU time : 4.96 s SATISFIABLE VERIFY_CNF 1049 END : (5 seconds) [Mon Jun 19 07:24:43 2006] VERIFY_CNF 1049 CPU : 5.39 = 0 + 0 + 5.02 + 0.37 # RESULT : makespan 1049 SATISFIABLE SHOW_RESULT 1049 BEGIN : [Mon Jun 19 07:24:43 2006] # ASSIGN : makespan 1049 # ASSIGN : s_0_0 723 # ASSIGN : s_0_1 977 # ASSIGN : s_0_2 36 # ASSIGN : s_0_3 874 # ASSIGN : s_0_4 5 # ASSIGN : s_0_5 123 # ASSIGN : s_0_6 704 # ASSIGN : s_0_7 373 # ASSIGN : s_1_0 1039 # ASSIGN : s_1_1 167 # ASSIGN : s_1_2 687 # ASSIGN : s_1_3 1025 # ASSIGN : s_1_4 48 # ASSIGN : s_1_5 323 # ASSIGN : s_1_6 3 # ASSIGN : s_1_7 744 # ASSIGN : s_2_0 427 # ASSIGN : s_2_1 1047 # ASSIGN : s_2_2 180 # ASSIGN : s_2_3 136 # ASSIGN : s_2_4 894 # ASSIGN : s_2_5 692 # ASSIGN : s_2_6 121 # ASSIGN : s_2_7 14 # ASSIGN : s_3_0 35 # ASSIGN : s_3_1 351 # ASSIGN : s_3_2 126 # ASSIGN : s_3_3 523 # ASSIGN : s_3_4 180 # ASSIGN : s_3_5 84 # ASSIGN : s_3_6 731 # ASSIGN : s_3_7 273 # ASSIGN : s_4_0 892 # ASSIGN : s_4_1 1032 # ASSIGN : s_4_2 711 # ASSIGN : s_4_3 6 # ASSIGN : s_4_4 794 # ASSIGN : s_4_5 888 # ASSIGN : s_4_6 268 # ASSIGN : s_4_7 185 # ASSIGN : s_5_0 632 # ASSIGN : s_5_1 0 # ASSIGN : s_5_2 555 # ASSIGN : s_5_3 735 # ASSIGN : s_5_4 282 # ASSIGN : s_5_5 891 # ASSIGN : s_5_6 170 # ASSIGN : s_5_7 137 # ASSIGN : s_6_0 5 # ASSIGN : s_6_1 123 # ASSIGN : s_6_2 790 # ASSIGN : s_6_3 197 # ASSIGN : s_6_4 549 # ASSIGN : s_6_5 23 # ASSIGN : s_6_6 52 # ASSIGN : s_6_7 174 # ASSIGN : s_7_0 46 # ASSIGN : s_7_1 547 # ASSIGN : s_7_2 420 # ASSIGN : s_7_3 1001 # ASSIGN : s_7_4 510 # ASSIGN : s_7_5 41 # ASSIGN : s_7_6 1007 # ASSIGN : s_7_7 985 SHOW_RESULT 1049 END : 1049 (0 seconds) [Mon Jun 19 07:24:43 2006] SHOW_RESULT 1049 CPU : 0.300000000000001 = 0.280000000000001 + 0.02 + 0 + 0 # BOUND : makespan 1000 1049 MODIFY_CNF 1024 BEGIN : [Mon Jun 19 07:24:44 2006] MODIFY_CNF 1024 END : 57280797 bytes (0 seconds) [Mon Jun 19 07:24:44 2006] MODIFY_CNF 1024 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1024 BEGIN : [Mon Jun 19 07:24:44 2006] CMD : minisat /tmp/csp2sat23155.cnf /tmp/csp2sat23155.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1078986 3070704 | 359662 0 0 nan | 0.000 % | | 100 | 1078986 3070704 | 395628 100 2851 28.5 | 65.124 % | | 252 | 1078986 3070704 | 435191 252 5573 22.1 | 65.124 % | | 479 | 1078986 3070704 | 478710 479 10255 21.4 | 65.124 % | | 816 | 1078986 3070704 | 526581 816 15423 18.9 | 65.124 % | | 1323 | 1078986 3070704 | 579239 1323 25093 19.0 | 65.124 % | | 2082 | 1078986 3070704 | 637163 2082 38463 18.5 | 65.124 % | | 3222 | 1078986 3070704 | 700879 3222 59215 18.4 | 65.124 % | | 4930 | 1078986 3070704 | 770967 4930 95064 19.3 | 65.124 % | | 7492 | 1078986 3070704 | 848064 7492 149827 20.0 | 65.124 % | | 11336 | 1078986 3070704 | 932870 11336 238181 21.0 | 65.124 % | ============================================================================== restarts : 11 conflicts : 12147 (111 /sec) decisions : 15300 (140 /sec) propagations : 98623647 (899358 /sec) conflict literals : 255185 (34.97 % deleted) Memory used : 103.80 MB CPU time : 109.66 s SATISFIABLE VERIFY_CNF 1024 END : (110 seconds) [Mon Jun 19 07:26:34 2006] VERIFY_CNF 1024 CPU : 110.03 = 0.0100000000000051 + 0.01 + 109.74 + 0.27 # RESULT : makespan 1024 SATISFIABLE SHOW_RESULT 1024 BEGIN : [Mon Jun 19 07:26:34 2006] # ASSIGN : makespan 1024 # ASSIGN : s_0_0 770 # ASSIGN : s_0_1 27 # ASSIGN : s_0_2 82 # ASSIGN : s_0_3 921 # ASSIGN : s_0_4 534 # ASSIGN : s_0_5 565 # ASSIGN : s_0_6 0 # ASSIGN : s_0_7 203 # ASSIGN : s_1_0 20 # ASSIGN : s_1_1 427 # ASSIGN : s_1_2 714 # ASSIGN : s_1_3 6 # ASSIGN : s_1_4 583 # ASSIGN : s_1_5 43 # ASSIGN : s_1_6 979 # ASSIGN : s_1_7 738 # ASSIGN : s_2_0 409 # ASSIGN : s_2_1 1022 # ASSIGN : s_2_2 169 # ASSIGN : s_2_3 724 # ASSIGN : s_2_4 4 # ASSIGN : s_2_5 768 # ASSIGN : s_2_6 964 # ASSIGN : s_2_7 617 # ASSIGN : s_3_0 614 # ASSIGN : s_3_1 255 # ASSIGN : s_3_2 634 # ASSIGN : s_3_3 47 # ASSIGN : s_3_4 441 # ASSIGN : s_3_5 4 # ASSIGN : s_3_6 688 # ASSIGN : s_3_7 536 # ASSIGN : s_4_0 625 # ASSIGN : s_4_1 1 # ASSIGN : s_4_2 546 # ASSIGN : s_4_3 791 # ASSIGN : s_4_4 930 # ASSIGN : s_4_5 765 # ASSIGN : s_4_6 110 # ASSIGN : s_4_7 16 # ASSIGN : s_5_0 933 # ASSIGN : s_5_1 132 # ASSIGN : s_5_2 5 # ASSIGN : s_5_3 259 # ASSIGN : s_5_4 702 # ASSIGN : s_5_5 407 # ASSIGN : s_5_6 590 # ASSIGN : s_5_7 99 # ASSIGN : s_6_0 1 # ASSIGN : s_6_1 88 # ASSIGN : s_6_2 742 # ASSIGN : s_6_3 398 # ASSIGN : s_6_4 157 # ASSIGN : s_6_5 1001 # ASSIGN : s_6_6 19 # ASSIGN : s_6_7 146 # ASSIGN : s_7_0 30 # ASSIGN : s_7_1 589 # ASSIGN : s_7_2 456 # ASSIGN : s_7_3 24 # ASSIGN : s_7_4 404 # ASSIGN : s_7_5 1019 # ASSIGN : s_7_6 547 # ASSIGN : s_7_7 0 SHOW_RESULT 1024 END : 1024 (0 seconds) [Mon Jun 19 07:26:34 2006] SHOW_RESULT 1024 CPU : 0.300000000000006 = 0.290000000000006 + 0.01 + 0 + 0 # BOUND : makespan 1000 1024 MODIFY_CNF 1012 BEGIN : [Mon Jun 19 07:26:34 2006] MODIFY_CNF 1012 END : 57280797 bytes (0 seconds) [Mon Jun 19 07:26:34 2006] MODIFY_CNF 1012 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1012 BEGIN : [Mon Jun 19 07:26:34 2006] CMD : minisat /tmp/csp2sat23155.cnf /tmp/csp2sat23155.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1068234 3038448 | 356078 0 0 nan | 0.000 % | | 102 | 1068234 3038448 | 391685 102 2525 24.8 | 65.587 % | | 253 | 1068234 3038448 | 430854 253 5214 20.6 | 65.587 % | | 480 | 1068234 3038448 | 473939 480 8635 18.0 | 65.587 % | | 817 | 1068234 3038448 | 521333 817 14529 17.8 | 65.587 % | | 1323 | 1068234 3038448 | 573467 1323 23611 17.8 | 65.587 % | | 2083 | 1068234 3038448 | 630813 2083 39897 19.2 | 65.587 % | | 3222 | 1068234 3038448 | 693895 3222 67397 20.9 | 65.587 % | | 4932 | 1068234 3038448 | 763284 4932 98207 19.9 | 65.587 % | | 7495 | 1068234 3038448 | 839613 7495 151081 20.2 | 65.587 % | | 11339 | 1068234 3038448 | 923574 11339 232638 20.5 | 65.587 % | | 17105 | 1068234 3038448 | 1015932 17105 356218 20.8 | 65.587 % | | 25757 | 1068235 3038448 | 1117525 25756 533800 20.7 | 65.587 % | | 38732 | 1043496 2964306 | 1229277 23190 420256 18.1 | 66.683 % | ============================================================================== restarts : 14 conflicts : 40909 (108 /sec) decisions : 47697 (125 /sec) propagations : 326568394 (858487 /sec) conflict literals : 837323 (38.94 % deleted) Memory used : 103.13 MB CPU time : 380.4 s UNSATISFIABLE VERIFY_CNF 1012 END : (381 seconds) [Mon Jun 19 07:32:55 2006] VERIFY_CNF 1012 CPU : 380.79 = 0 + 0.01 + 380.4 + 0.38 # RESULT : makespan 1012 UNSATISFIABLE # BOUND : makespan 1013 1024 MODIFY_CNF 1018 BEGIN : [Mon Jun 19 07:32:55 2006] MODIFY_CNF 1018 END : 57280797 bytes (0 seconds) [Mon Jun 19 07:32:55 2006] MODIFY_CNF 1018 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1018 BEGIN : [Mon Jun 19 07:32:55 2006] CMD : minisat /tmp/csp2sat23155.cnf /tmp/csp2sat23155.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1073610 3054576 | 357870 0 0 nan | 0.000 % | | 100 | 1073610 3054576 | 393657 100 2340 23.4 | 65.356 % | | 253 | 1073610 3054576 | 433022 253 5184 20.5 | 65.356 % | | 478 | 1073610 3054576 | 476324 478 9240 19.3 | 65.356 % | | 816 | 1073610 3054576 | 523957 816 15359 18.8 | 65.356 % | | 1322 | 1073610 3054576 | 576353 1322 24977 18.9 | 65.356 % | | 2082 | 1073610 3054576 | 633988 2082 41312 19.8 | 65.356 % | | 3221 | 1073610 3054576 | 697387 3221 60113 18.7 | 65.356 % | | 4931 | 1073610 3054576 | 767126 4931 92108 18.7 | 65.356 % | | 7493 | 1073610 3054576 | 843838 7493 141038 18.8 | 65.356 % | | 11337 | 1073610 3054576 | 928222 11337 225472 19.9 | 65.356 % | | 17104 | 1073610 3054576 | 1021044 17104 357073 20.9 | 65.356 % | | 25753 | 1073611 3054576 | 1123149 25752 538932 20.9 | 65.356 % | ============================================================================== restarts : 13 conflicts : 26031 (107 /sec) decisions : 31797 (131 /sec) propagations : 213313518 (879172 /sec) conflict literals : 544251 (36.14 % deleted) Memory used : 103.80 MB CPU time : 242.63 s SATISFIABLE VERIFY_CNF 1018 END : (243 seconds) [Mon Jun 19 07:36:58 2006] VERIFY_CNF 1018 CPU : 243.33 = 0 + 0 + 242.71 + 0.62 # RESULT : makespan 1018 SATISFIABLE SHOW_RESULT 1018 BEGIN : [Mon Jun 19 07:36:58 2006] # ASSIGN : makespan 1018 # ASSIGN : s_0_0 466 # ASSIGN : s_0_1 948 # ASSIGN : s_0_2 129 # ASSIGN : s_0_3 9 # ASSIGN : s_0_4 435 # ASSIGN : s_0_5 216 # ASSIGN : s_0_6 416 # ASSIGN : s_0_7 617 # ASSIGN : s_1_0 456 # ASSIGN : s_1_1 1 # ASSIGN : s_1_2 418 # ASSIGN : s_1_3 442 # ASSIGN : s_1_4 468 # ASSIGN : s_1_5 604 # ASSIGN : s_1_6 973 # ASSIGN : s_1_7 177 # ASSIGN : s_2_0 233 # ASSIGN : s_2_1 607 # ASSIGN : s_2_2 778 # ASSIGN : s_2_3 456 # ASSIGN : s_2_4 624 # ASSIGN : s_2_5 20 # ASSIGN : s_2_6 5 # ASSIGN : s_2_7 500 # ASSIGN : s_3_0 1007 # ASSIGN : s_3_1 776 # ASSIGN : s_3_2 722 # ASSIGN : s_3_3 514 # ASSIGN : s_3_4 19 # ASSIGN : s_3_5 968 # ASSIGN : s_3_6 140 # ASSIGN : s_3_7 422 # ASSIGN : s_4_0 93 # ASSIGN : s_4_1 1003 # ASSIGN : s_4_2 261 # ASSIGN : s_4_3 873 # ASSIGN : s_4_4 340 # ASSIGN : s_4_5 434 # ASSIGN : s_4_6 437 # ASSIGN : s_4_7 10 # ASSIGN : s_5_0 2 # ASSIGN : s_5_1 609 # ASSIGN : s_5_2 341 # ASSIGN : s_5_3 734 # ASSIGN : s_5_4 112 # ASSIGN : s_5_5 446 # ASSIGN : s_5_6 875 # ASSIGN : s_5_7 985 # ASSIGN : s_6_0 438 # ASSIGN : s_6_1 732 # ASSIGN : s_6_2 463 # ASSIGN : s_6_3 112 # ASSIGN : s_6_4 777 # ASSIGN : s_6_5 2 # ASSIGN : s_6_6 29 # ASSIGN : s_6_7 101 # ASSIGN : s_7_0 633 # ASSIGN : s_7_1 157 # ASSIGN : s_7_2 8 # ASSIGN : s_7_3 2 # ASSIGN : s_7_4 587 # ASSIGN : s_7_5 1013 # ASSIGN : s_7_6 98 # ASSIGN : s_7_7 141 SHOW_RESULT 1018 END : 1018 (0 seconds) [Mon Jun 19 07:36:58 2006] SHOW_RESULT 1018 CPU : 0.299999999999997 = 0.299999999999997 + 0 + 0 + 0 # BOUND : makespan 1013 1018 MODIFY_CNF 1015 BEGIN : [Mon Jun 19 07:36:58 2006] MODIFY_CNF 1015 END : 57280797 bytes (0 seconds) [Mon Jun 19 07:36:58 2006] MODIFY_CNF 1015 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1015 BEGIN : [Mon Jun 19 07:36:58 2006] CMD : minisat /tmp/csp2sat23155.cnf /tmp/csp2sat23155.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1070922 3046512 | 356974 0 0 nan | 0.000 % | | 101 | 1070922 3046512 | 392671 101 2608 25.8 | 65.471 % | | 252 | 1070922 3046512 | 431938 252 5305 21.1 | 65.471 % | | 478 | 1070922 3046512 | 475132 478 9646 20.2 | 65.471 % | | 815 | 1070922 3046512 | 522645 815 14627 17.9 | 65.471 % | | 1322 | 1070922 3046512 | 574910 1322 23164 17.5 | 65.471 % | | 2082 | 1070922 3046512 | 632401 2082 38106 18.3 | 65.471 % | | 3223 | 1070922 3046512 | 695641 3223 61353 19.0 | 65.471 % | | 4934 | 1070922 3046512 | 765205 4934 94004 19.1 | 65.471 % | | 7497 | 1070922 3046512 | 841726 7497 140748 18.8 | 65.471 % | | 11341 | 1070923 3046512 | 925898 11340 219714 19.4 | 65.471 % | | 17108 | 1070923 3046512 | 1018488 17107 344205 20.1 | 65.471 % | | 25758 | 1070923 3046512 | 1120337 25757 524497 20.4 | 65.471 % | | 38732 | 1070927 3046512 | 1232371 38727 785696 20.3 | 65.471 % | ============================================================================== restarts : 14 conflicts : 56313 (99 /sec) decisions : 65364 (115 /sec) propagations : 470436776 (829110 /sec) conflict literals : 1140280 (40.53 % deleted) Memory used : 103.12 MB CPU time : 567.4 s UNSATISFIABLE VERIFY_CNF 1015 END : (568 seconds) [Mon Jun 19 07:46:26 2006] VERIFY_CNF 1015 CPU : 567.64 = 0 + 0 + 567.4 + 0.24 # RESULT : makespan 1015 UNSATISFIABLE # BOUND : makespan 1016 1018 MODIFY_CNF 1017 BEGIN : [Mon Jun 19 07:46:26 2006] MODIFY_CNF 1017 END : 57280797 bytes (0 seconds) [Mon Jun 19 07:46:26 2006] MODIFY_CNF 1017 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1017 BEGIN : [Mon Jun 19 07:46:26 2006] CMD : minisat /tmp/csp2sat23155.cnf /tmp/csp2sat23155.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1072714 3051888 | 357571 0 0 nan | 0.000 % | | 100 | 1072714 3051888 | 393328 100 2465 24.6 | 65.394 % | | 250 | 1072714 3051888 | 432660 250 4574 18.3 | 65.394 % | | 475 | 1072714 3051888 | 475927 475 9628 20.3 | 65.394 % | | 812 | 1072714 3051888 | 523519 812 14630 18.0 | 65.394 % | | 1318 | 1072714 3051888 | 575871 1318 22611 17.2 | 65.394 % | | 2080 | 1072714 3051888 | 633458 2080 35969 17.3 | 65.394 % | | 3219 | 1072714 3051888 | 696804 3219 58675 18.2 | 65.394 % | | 4927 | 1072714 3051888 | 766485 4927 88662 18.0 | 65.394 % | ============================================================================== restarts : 9 conflicts : 6613 (115 /sec) decisions : 8425 (147 /sec) propagations : 52085910 (908845 /sec) conflict literals : 123121 (35.05 % deleted) Memory used : 103.80 MB CPU time : 57.31 s SATISFIABLE VERIFY_CNF 1017 END : (58 seconds) [Mon Jun 19 07:47:24 2006] VERIFY_CNF 1017 CPU : 57.7400000000001 = 0 + 0 + 57.3900000000001 + 0.35 # RESULT : makespan 1017 SATISFIABLE SHOW_RESULT 1017 BEGIN : [Mon Jun 19 07:47:24 2006] # ASSIGN : makespan 1017 # ASSIGN : s_0_0 402 # ASSIGN : s_0_1 16 # ASSIGN : s_0_2 827 # ASSIGN : s_0_3 914 # ASSIGN : s_0_4 553 # ASSIGN : s_0_5 603 # ASSIGN : s_0_6 584 # ASSIGN : s_0_7 71 # ASSIGN : s_1_0 553 # ASSIGN : s_1_1 861 # ASSIGN : s_1_2 595 # ASSIGN : s_1_3 574 # ASSIGN : s_1_4 434 # ASSIGN : s_1_5 70 # ASSIGN : s_1_6 5 # ASSIGN : s_1_7 620 # ASSIGN : s_2_0 581 # ASSIGN : s_2_1 421 # ASSIGN : s_2_2 1 # ASSIGN : s_2_3 530 # ASSIGN : s_2_4 241 # ASSIGN : s_2_5 803 # ASSIGN : s_2_6 1002 # ASSIGN : s_2_7 423 # ASSIGN : s_3_0 9 # ASSIGN : s_3_1 78 # ASSIGN : s_3_2 250 # ASSIGN : s_3_3 322 # ASSIGN : s_3_4 924 # ASSIGN : s_3_5 31 # ASSIGN : s_3_6 609 # ASSIGN : s_3_7 531 # ASSIGN : s_4_0 786 # ASSIGN : s_4_1 0 # ASSIGN : s_4_2 707 # ASSIGN : s_4_3 18 # ASSIGN : s_4_4 602 # ASSIGN : s_4_5 15 # ASSIGN : s_4_6 148 # ASSIGN : s_4_7 934 # ASSIGN : s_5_0 926 # ASSIGN : s_5_1 298 # ASSIGN : s_5_2 619 # ASSIGN : s_5_3 159 # ASSIGN : s_5_4 696 # ASSIGN : s_5_5 445 # ASSIGN : s_5_6 50 # ASSIGN : s_5_7 17 # ASSIGN : s_6_0 563 # ASSIGN : s_6_1 254 # ASSIGN : s_6_2 304 # ASSIGN : s_6_3 588 # ASSIGN : s_6_4 0 # ASSIGN : s_6_5 999 # ASSIGN : s_6_6 930 # ASSIGN : s_6_7 919 # ASSIGN : s_7_0 20 # ASSIGN : s_7_1 431 # ASSIGN : s_7_2 927 # ASSIGN : s_7_3 12 # ASSIGN : s_7_4 394 # ASSIGN : s_7_5 7 # ASSIGN : s_7_6 885 # ASSIGN : s_7_7 869 SHOW_RESULT 1017 END : 1017 (0 seconds) [Mon Jun 19 07:47:24 2006] SHOW_RESULT 1017 CPU : 0.310000000000002 = 0.310000000000002 + 0 + 0 + 0 # BOUND : makespan 1016 1017 MODIFY_CNF 1016 BEGIN : [Mon Jun 19 07:47:24 2006] MODIFY_CNF 1016 END : 57280797 bytes (0 seconds) [Mon Jun 19 07:47:24 2006] MODIFY_CNF 1016 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1016 BEGIN : [Mon Jun 19 07:47:24 2006] CMD : minisat /tmp/csp2sat23155.cnf /tmp/csp2sat23155.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1071818 3049200 | 357272 0 0 nan | 0.000 % | | 100 | 1071818 3049200 | 392999 100 2297 23.0 | 65.433 % | | 250 | 1071818 3049200 | 432299 250 5117 20.5 | 65.433 % | | 478 | 1071818 3049200 | 475529 478 9080 19.0 | 65.433 % | | 815 | 1071818 3049200 | 523081 815 14338 17.6 | 65.433 % | | 1323 | 1071818 3049200 | 575390 1323 24626 18.6 | 65.433 % | | 2084 | 1071818 3049200 | 632929 2084 39345 18.9 | 65.433 % | | 3223 | 1071818 3049200 | 696222 3223 59418 18.4 | 65.433 % | | 4931 | 1071818 3049200 | 765844 4931 88641 18.0 | 65.433 % | | 7494 | 1071818 3049200 | 842428 7494 138224 18.4 | 65.433 % | | 11339 | 1071818 3049200 | 926671 11339 212814 18.8 | 65.433 % | | 17106 | 1071818 3049200 | 1019338 17106 334246 19.5 | 65.433 % | | 25757 | 1071818 3049200 | 1121272 25757 499556 19.4 | 65.433 % | | 38732 | 1071819 3049200 | 1233399 38731 762321 19.7 | 65.433 % | | 58194 | 1059598 3012615 | 1356739 41507 780259 18.8 | 66.015 % | ============================================================================== restarts : 15 conflicts : 61145 (97 /sec) decisions : 70604 (112 /sec) propagations : 520326691 (828190 /sec) conflict literals : 1243902 (40.29 % deleted) Memory used : 103.12 MB CPU time : 628.27 s UNSATISFIABLE VERIFY_CNF 1016 END : (629 seconds) [Mon Jun 19 07:57:53 2006] VERIFY_CNF 1016 CPU : 628.96 = 0 + 0 + 628.27 + 0.69 # RESULT : makespan 1016 UNSATISFIABLE # BOUND : makespan 1017 1017 MAIN END : (2107 seconds) [Mon Jun 19 07:57:53 2006] MAIN CPU : 2106.73 = 95.73 + 0.53 + 2006.27 + 4.2