# TIMEOUT 18000 MAIN BEGIN : [Sun Jun 18 18:53:25 2006] READ BEGIN : csp/gp10-05.csp [Sun Jun 18 18:53:25 2006] READ END : csp/gp10-05.csp (2 seconds) [Sun Jun 18 18:53:27 2006] READ CPU : 1.87 = 1.84 + 0.03 + 0 + 0 # BOUND : makespan 1000 3541 GENERATE_CNF 3541 BEGIN : [Sun Jun 18 18:53:27 2006] GENERATE_CNF 3541 END : 358743 variables 6809544 clauses 162791329 bytes (263 seconds) [Sun Jun 18 18:57:50 2006] GENERATE_CNF 3541 CPU : 261.12 = 259.92 + 1.2 + 0 + 0 MODIFY_CNF 2270 BEGIN : [Sun Jun 18 18:57:50 2006] MODIFY_CNF 2270 END : 162791336 bytes (0 seconds) [Sun Jun 18 18:57:50 2006] MODIFY_CNF 2270 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 2270 BEGIN : [Sun Jun 18 18:57:50 2006] CMD : minisat /tmp/csp2sat12671.cnf /tmp/csp2sat12671.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 4519239 13202782 | 1506413 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 43 (4 /sec) decisions : 748 (64 /sec) propagations : 817223 (69551 /sec) conflict literals : 675 (3.57 % deleted) Memory used : 280.53 MB CPU time : 11.75 s SATISFIABLE VERIFY_CNF 2270 END : (12 seconds) [Sun Jun 18 18:58:02 2006] VERIFY_CNF 2270 CPU : 12.85 = 0 + 0 + 11.91 + 0.94 # RESULT : makespan 2270 SATISFIABLE SHOW_RESULT 2270 BEGIN : [Sun Jun 18 18:58:02 2006] # ASSIGN : makespan 2270 # ASSIGN : s_0_0 13 # ASSIGN : s_0_1 596 # ASSIGN : s_0_2 295 # ASSIGN : s_0_3 290 # ASSIGN : s_0_4 108 # ASSIGN : s_0_5 589 # ASSIGN : s_0_6 171 # ASSIGN : s_0_7 1203 # ASSIGN : s_0_8 206 # ASSIGN : s_0_9 783 # ASSIGN : s_1_0 17 # ASSIGN : s_1_1 737 # ASSIGN : s_1_2 705 # ASSIGN : s_1_3 381 # ASSIGN : s_1_4 176 # ASSIGN : s_1_5 902 # ASSIGN : s_1_6 172 # ASSIGN : s_1_7 1204 # ASSIGN : s_1_8 270 # ASSIGN : s_1_9 1355 # ASSIGN : s_2_0 448 # ASSIGN : s_2_1 867 # ASSIGN : s_2_2 763 # ASSIGN : s_2_3 868 # ASSIGN : s_2_4 463 # ASSIGN : s_2_5 903 # ASSIGN : s_2_6 173 # ASSIGN : s_2_7 1355 # ASSIGN : s_2_8 449 # ASSIGN : s_2_9 1356 # ASSIGN : s_3_0 456 # ASSIGN : s_3_1 869 # ASSIGN : s_3_2 1059 # ASSIGN : s_3_3 871 # ASSIGN : s_3_4 997 # ASSIGN : s_3_5 1410 # ASSIGN : s_3_6 300 # ASSIGN : s_3_7 1411 # ASSIGN : s_3_8 459 # ASSIGN : s_3_9 1357 # ASSIGN : s_4_0 608 # ASSIGN : s_4_1 870 # ASSIGN : s_4_2 1376 # ASSIGN : s_4_3 1186 # ASSIGN : s_4_4 1377 # ASSIGN : s_4_5 1590 # ASSIGN : s_4_6 301 # ASSIGN : s_4_7 1884 # ASSIGN : s_4_8 470 # ASSIGN : s_4_9 1381 # ASSIGN : s_5_0 1065 # ASSIGN : s_5_1 917 # ASSIGN : s_5_2 1624 # ASSIGN : s_5_3 1229 # ASSIGN : s_5_4 1398 # ASSIGN : s_5_5 1841 # ASSIGN : s_5_6 306 # ASSIGN : s_5_7 2061 # ASSIGN : s_5_8 471 # ASSIGN : s_5_9 1751 # ASSIGN : s_6_0 1227 # ASSIGN : s_6_1 1043 # ASSIGN : s_6_2 1625 # ASSIGN : s_6_3 1230 # ASSIGN : s_6_4 1407 # ASSIGN : s_6_5 1865 # ASSIGN : s_6_6 914 # ASSIGN : s_6_7 2126 # ASSIGN : s_6_8 917 # ASSIGN : s_6_9 1752 # ASSIGN : s_7_0 1264 # ASSIGN : s_7_1 1300 # ASSIGN : s_7_2 1664 # ASSIGN : s_7_3 1867 # ASSIGN : s_7_4 1899 # ASSIGN : s_7_5 2183 # ASSIGN : s_7_6 917 # ASSIGN : s_7_7 2127 # ASSIGN : s_7_8 918 # ASSIGN : s_7_9 1901 # ASSIGN : s_8_0 2260 # ASSIGN : s_8_1 1655 # ASSIGN : s_8_2 1669 # ASSIGN : s_8_3 1869 # ASSIGN : s_8_4 1937 # ASSIGN : s_8_5 2184 # ASSIGN : s_8_6 960 # ASSIGN : s_8_7 2185 # ASSIGN : s_8_8 2259 # ASSIGN : s_8_9 2265 # ASSIGN : s_9_0 1270 # ASSIGN : s_9_1 1669 # ASSIGN : s_9_2 1670 # ASSIGN : s_9_3 1895 # ASSIGN : s_9_4 2188 # ASSIGN : s_9_5 2189 # ASSIGN : s_9_6 2190 # ASSIGN : s_9_7 2191 # ASSIGN : s_9_8 2260 # ASSIGN : s_9_9 2269 SHOW_RESULT 2270 END : 2270 (2 seconds) [Sun Jun 18 18:58:04 2006] SHOW_RESULT 2270 CPU : 1.25999999999996 = 1.22999999999996 + 0.03 + 0 + 0 # BOUND : makespan 1000 2270 MODIFY_CNF 1635 BEGIN : [Sun Jun 18 18:58:04 2006] MODIFY_CNF 1635 END : 162791335 bytes (0 seconds) [Sun Jun 18 18:58:04 2006] MODIFY_CNF 1635 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1635 BEGIN : [Sun Jun 18 18:58:04 2006] CMD : minisat /tmp/csp2sat12671.cnf /tmp/csp2sat12671.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 3376239 9773782 | 1125413 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 30 (2 /sec) decisions : 793 (56 /sec) propagations : 698373 (49285 /sec) conflict literals : 568 (8.24 % deleted) Memory used : 280.53 MB CPU time : 14.17 s SATISFIABLE VERIFY_CNF 1635 END : (15 seconds) [Sun Jun 18 18:58:19 2006] VERIFY_CNF 1635 CPU : 15.27 = 0 + 0.01 + 14.34 + 0.92 # RESULT : makespan 1635 SATISFIABLE SHOW_RESULT 1635 BEGIN : [Sun Jun 18 18:58:19 2006] # ASSIGN : makespan 1635 # ASSIGN : s_0_0 2 # ASSIGN : s_0_1 901 # ASSIGN : s_0_2 1042 # ASSIGN : s_0_3 15 # ASSIGN : s_0_4 20 # ASSIGN : s_0_5 83 # ASSIGN : s_0_6 0 # ASSIGN : s_0_7 1 # ASSIGN : s_0_8 90 # ASSIGN : s_0_9 307 # ASSIGN : s_1_0 778 # ASSIGN : s_1_1 368 # ASSIGN : s_1_2 511 # ASSIGN : s_1_3 1281 # ASSIGN : s_1_4 543 # ASSIGN : s_1_5 1 # ASSIGN : s_1_6 2 # ASSIGN : s_1_7 3 # ASSIGN : s_1_8 154 # ASSIGN : s_1_9 727 # ASSIGN : s_2_0 6 # ASSIGN : s_2_1 9 # ASSIGN : s_2_2 26 # ASSIGN : s_2_3 130 # ASSIGN : s_2_4 1333 # ASSIGN : s_2_5 275 # ASSIGN : s_2_6 138 # ASSIGN : s_2_7 727 # ASSIGN : s_2_8 265 # ASSIGN : s_2_9 728 # ASSIGN : s_3_0 7 # ASSIGN : s_3_1 10 # ASSIGN : s_3_2 1336 # ASSIGN : s_3_3 603 # ASSIGN : s_3_4 1270 # ASSIGN : s_3_5 786 # ASSIGN : s_3_6 307 # ASSIGN : s_3_7 787 # ASSIGN : s_3_8 466 # ASSIGN : s_3_9 729 # ASSIGN : s_4_0 491 # ASSIGN : s_4_1 137 # ASSIGN : s_4_2 307 # ASSIGN : s_4_3 1213 # ASSIGN : s_4_4 1256 # ASSIGN : s_4_5 962 # ASSIGN : s_4_6 308 # ASSIGN : s_4_7 1260 # ASSIGN : s_4_8 477 # ASSIGN : s_4_9 753 # ASSIGN : s_5_0 151 # ASSIGN : s_5_1 11 # ASSIGN : s_5_2 150 # ASSIGN : s_5_3 1126 # ASSIGN : s_5_4 1208 # ASSIGN : s_5_5 1217 # ASSIGN : s_5_6 313 # ASSIGN : s_5_7 1437 # ASSIGN : s_5_8 478 # ASSIGN : s_5_9 1127 # ASSIGN : s_6_0 148 # ASSIGN : s_6_1 184 # ASSIGN : s_6_2 387 # ASSIGN : s_6_3 426 # ASSIGN : s_6_4 637 # ASSIGN : s_6_5 1241 # ASSIGN : s_6_6 855 # ASSIGN : s_6_7 1502 # ASSIGN : s_6_8 924 # ASSIGN : s_6_9 1128 # ASSIGN : s_7_0 1497 # ASSIGN : s_7_1 498 # ASSIGN : s_7_2 853 # ASSIGN : s_7_3 1605 # ASSIGN : s_7_4 1633 # ASSIGN : s_7_5 1632 # ASSIGN : s_7_6 858 # ASSIGN : s_7_7 1503 # ASSIGN : s_7_8 925 # ASSIGN : s_7_9 1271 # ASSIGN : s_8_0 1588 # ASSIGN : s_8_1 1593 # ASSIGN : s_8_2 1634 # ASSIGN : s_8_3 1607 # ASSIGN : s_8_4 296 # ASSIGN : s_8_5 1633 # ASSIGN : s_8_6 859 # ASSIGN : s_8_7 1559 # ASSIGN : s_8_8 1554 # ASSIGN : s_8_9 1555 # ASSIGN : s_9_0 933 # ASSIGN : s_9_1 1553 # ASSIGN : s_9_2 628 # ASSIGN : s_9_3 133 # ASSIGN : s_9_4 1332 # ASSIGN : s_9_5 1634 # ASSIGN : s_9_6 1554 # ASSIGN : s_9_7 1565 # ASSIGN : s_9_8 1555 # ASSIGN : s_9_9 1564 SHOW_RESULT 1635 END : 1635 (1 seconds) [Sun Jun 18 18:58:20 2006] SHOW_RESULT 1635 CPU : 1.37000000000001 = 1.36000000000001 + 0.01 + 0 + 0 # BOUND : makespan 1000 1635 MODIFY_CNF 1317 BEGIN : [Sun Jun 18 18:58:20 2006] MODIFY_CNF 1317 END : 162791335 bytes (0 seconds) [Sun Jun 18 18:58:20 2006] MODIFY_CNF 1317 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1317 BEGIN : [Sun Jun 18 18:58:20 2006] CMD : minisat /tmp/csp2sat12671.cnf /tmp/csp2sat12671.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 2803839 8056582 | 934613 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 8 (1 /sec) decisions : 518 (38 /sec) propagations : 454524 (33569 /sec) conflict literals : 42 (2.33 % deleted) Memory used : 280.52 MB CPU time : 13.54 s SATISFIABLE VERIFY_CNF 1317 END : (15 seconds) [Sun Jun 18 18:58:35 2006] VERIFY_CNF 1317 CPU : 14.56 = 0 + 0 + 13.71 + 0.85 # RESULT : makespan 1317 SATISFIABLE SHOW_RESULT 1317 BEGIN : [Sun Jun 18 18:58:35 2006] # ASSIGN : makespan 1317 # ASSIGN : s_0_0 589 # ASSIGN : s_0_1 824 # ASSIGN : s_0_2 1018 # ASSIGN : s_0_3 1 # ASSIGN : s_0_4 71 # ASSIGN : s_0_5 136 # ASSIGN : s_0_6 0 # ASSIGN : s_0_7 6 # ASSIGN : s_0_8 7 # ASSIGN : s_0_9 143 # ASSIGN : s_1_0 593 # ASSIGN : s_1_1 193 # ASSIGN : s_1_2 39 # ASSIGN : s_1_3 993 # ASSIGN : s_1_4 899 # ASSIGN : s_1_5 562 # ASSIGN : s_1_6 5 # ASSIGN : s_1_7 748 # ASSIGN : s_1_8 71 # ASSIGN : s_1_9 563 # ASSIGN : s_2_0 1 # ASSIGN : s_2_1 4 # ASSIGN : s_2_2 75 # ASSIGN : s_2_3 179 # ASSIGN : s_2_4 1017 # ASSIGN : s_2_5 565 # ASSIGN : s_2_6 192 # ASSIGN : s_2_7 11 # ASSIGN : s_2_8 182 # ASSIGN : s_2_9 564 # ASSIGN : s_3_0 2 # ASSIGN : s_3_1 5 # ASSIGN : s_3_2 720 # ASSIGN : s_3_3 8 # ASSIGN : s_3_4 134 # ASSIGN : s_3_5 1316 # ASSIGN : s_3_6 6 # ASSIGN : s_3_7 207 # ASSIGN : s_3_8 196 # ASSIGN : s_3_9 680 # ASSIGN : s_4_0 1055 # ASSIGN : s_4_1 965 # ASSIGN : s_4_2 189 # ASSIGN : s_4_3 190 # ASSIGN : s_4_4 1012 # ASSIGN : s_4_5 311 # ASSIGN : s_4_6 7 # ASSIGN : s_4_7 12 # ASSIGN : s_4_8 233 # ASSIGN : s_4_9 704 # ASSIGN : s_5_0 751 # ASSIGN : s_5_1 1091 # ASSIGN : s_5_2 208 # ASSIGN : s_5_3 233 # ASSIGN : s_5_4 18 # ASSIGN : s_5_5 209 # ASSIGN : s_5_6 27 # ASSIGN : s_5_7 962 # ASSIGN : s_5_8 234 # ASSIGN : s_5_9 913 # ASSIGN : s_6_0 6 # ASSIGN : s_6_1 9 # ASSIGN : s_6_2 209 # ASSIGN : s_6_3 503 # ASSIGN : s_6_4 681 # ASSIGN : s_6_5 1050 # ASSIGN : s_6_6 319 # ASSIGN : s_6_7 1027 # ASSIGN : s_6_8 680 # ASSIGN : s_6_9 914 # ASSIGN : s_7_0 65 # ASSIGN : s_7_1 323 # ASSIGN : s_7_2 1312 # ASSIGN : s_7_3 680 # ASSIGN : s_7_4 678 # ASSIGN : s_7_5 1311 # ASSIGN : s_7_6 322 # ASSIGN : s_7_7 1028 # ASSIGN : s_7_8 682 # ASSIGN : s_7_9 1084 # ASSIGN : s_8_0 71 # ASSIGN : s_8_1 1217 # ASSIGN : s_8_2 248 # ASSIGN : s_8_3 249 # ASSIGN : s_8_4 275 # ASSIGN : s_8_5 1314 # ASSIGN : s_8_6 522 # ASSIGN : s_8_7 1231 # ASSIGN : s_8_8 1305 # ASSIGN : s_8_9 1310 # ASSIGN : s_9_0 76 # ASSIGN : s_9_1 1235 # ASSIGN : s_9_2 475 # ASSIGN : s_9_3 700 # ASSIGN : s_9_4 1016 # ASSIGN : s_9_5 1315 # ASSIGN : s_9_6 1236 # ASSIGN : s_9_7 1237 # ASSIGN : s_9_8 1306 # ASSIGN : s_9_9 1316 SHOW_RESULT 1317 END : 1317 (1 seconds) [Sun Jun 18 18:58:36 2006] SHOW_RESULT 1317 CPU : 1.33999999999998 = 1.32999999999998 + 0.01 + 0 + 0 # BOUND : makespan 1000 1317 MODIFY_CNF 1158 BEGIN : [Sun Jun 18 18:58:36 2006] MODIFY_CNF 1158 END : 162791335 bytes (0 seconds) [Sun Jun 18 18:58:36 2006] MODIFY_CNF 1158 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1158 BEGIN : [Sun Jun 18 18:58:36 2006] CMD : minisat /tmp/csp2sat12671.cnf /tmp/csp2sat12671.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 2517639 7197982 | 839213 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 6 (0 /sec) decisions : 277 (19 /sec) propagations : 400355 (27573 /sec) conflict literals : 132 (4.35 % deleted) Memory used : 280.52 MB CPU time : 14.52 s SATISFIABLE VERIFY_CNF 1158 END : (16 seconds) [Sun Jun 18 18:58:52 2006] VERIFY_CNF 1158 CPU : 15.56 = 0 + 0 + 14.72 + 0.84 # RESULT : makespan 1158 SATISFIABLE SHOW_RESULT 1158 BEGIN : [Sun Jun 18 18:58:52 2006] # ASSIGN : makespan 1158 # ASSIGN : s_0_0 14 # ASSIGN : s_0_1 581 # ASSIGN : s_0_2 722 # ASSIGN : s_0_3 4 # ASSIGN : s_0_4 1020 # ASSIGN : s_0_5 18 # ASSIGN : s_0_6 25 # ASSIGN : s_0_7 26 # ASSIGN : s_0_8 1083 # ASSIGN : s_0_9 27 # ASSIGN : s_1_0 741 # ASSIGN : s_1_1 990 # ASSIGN : s_1_2 1120 # ASSIGN : s_1_3 123 # ASSIGN : s_1_4 896 # ASSIGN : s_1_5 1157 # ASSIGN : s_1_6 122 # ASSIGN : s_1_7 448 # ASSIGN : s_1_8 0 # ASSIGN : s_1_9 447 # ASSIGN : s_2_0 0 # ASSIGN : s_2_1 23 # ASSIGN : s_2_2 1016 # ASSIGN : s_2_3 64 # ASSIGN : s_2_4 263 # ASSIGN : s_2_5 564 # ASSIGN : s_2_6 133 # ASSIGN : s_2_7 67 # ASSIGN : s_2_8 111 # ASSIGN : s_2_9 563 # ASSIGN : s_3_0 21 # ASSIGN : s_3_1 24 # ASSIGN : s_3_2 139 # ASSIGN : s_3_3 449 # ASSIGN : s_3_4 1096 # ASSIGN : s_3_5 25 # ASSIGN : s_3_6 120 # ASSIGN : s_3_7 599 # ASSIGN : s_3_8 121 # ASSIGN : s_3_9 575 # ASSIGN : s_4_0 896 # ASSIGN : s_4_1 817 # ASSIGN : s_4_2 0 # ASSIGN : s_4_3 80 # ASSIGN : s_4_4 591 # ASSIGN : s_4_5 313 # ASSIGN : s_4_6 127 # ASSIGN : s_4_7 136 # ASSIGN : s_4_8 132 # ASSIGN : s_4_9 603 # ASSIGN : s_5_0 579 # ASSIGN : s_5_1 864 # ASSIGN : s_5_2 1 # ASSIGN : s_5_3 0 # ASSIGN : s_5_4 2 # ASSIGN : s_5_5 28 # ASSIGN : s_5_6 993 # ASSIGN : s_5_7 68 # ASSIGN : s_5_8 133 # ASSIGN : s_5_9 812 # ASSIGN : s_6_0 576 # ASSIGN : s_6_1 392 # ASSIGN : s_6_2 10 # ASSIGN : s_6_3 981 # ASSIGN : s_6_4 595 # ASSIGN : s_6_5 52 # ASSIGN : s_6_6 49 # ASSIGN : s_6_7 391 # ASSIGN : s_6_8 579 # ASSIGN : s_6_9 813 # ASSIGN : s_7_0 1 # ASSIGN : s_7_1 37 # ASSIGN : s_7_2 1152 # ASSIGN : s_7_3 9 # ASSIGN : s_7_4 11 # ASSIGN : s_7_5 26 # ASSIGN : s_7_6 36 # ASSIGN : s_7_7 392 # ASSIGN : s_7_8 580 # ASSIGN : s_7_9 926 # ASSIGN : s_8_0 7 # ASSIGN : s_8_1 1133 # ASSIGN : s_8_2 1157 # ASSIGN : s_8_3 955 # ASSIGN : s_8_4 13 # ASSIGN : s_8_5 12 # ASSIGN : s_8_6 260 # ASSIGN : s_8_7 1072 # ASSIGN : s_8_8 1147 # ASSIGN : s_8_9 1153 # ASSIGN : s_9_0 38 # ASSIGN : s_9_1 1147 # ASSIGN : s_9_2 437 # ASSIGN : s_9_3 662 # ASSIGN : s_9_4 1 # ASSIGN : s_9_5 27 # ASSIGN : s_9_6 992 # ASSIGN : s_9_7 1078 # ASSIGN : s_9_8 1148 # ASSIGN : s_9_9 1157 SHOW_RESULT 1158 END : 1158 (1 seconds) [Sun Jun 18 18:58:53 2006] SHOW_RESULT 1158 CPU : 1.34000000000004 = 1.33000000000004 + 0.01 + 0 + 0 # BOUND : makespan 1000 1158 MODIFY_CNF 1079 BEGIN : [Sun Jun 18 18:58:53 2006] MODIFY_CNF 1079 END : 162791334 bytes (0 seconds) [Sun Jun 18 18:58:53 2006] MODIFY_CNF 1079 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1079 BEGIN : [Sun Jun 18 18:58:53 2006] CMD : minisat /tmp/csp2sat12671.cnf /tmp/csp2sat12671.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 2375439 6771382 | 791813 0 0 nan | 0.000 % | | 100 | 2375440 6771382 | 870994 99 2364 23.9 | 72.186 % | ============================================================================== restarts : 2 conflicts : 204 (12 /sec) decisions : 536 (31 /sec) propagations : 2284028 (130740 /sec) conflict literals : 3984 (21.87 % deleted) Memory used : 280.54 MB CPU time : 17.47 s SATISFIABLE VERIFY_CNF 1079 END : (19 seconds) [Sun Jun 18 18:59:12 2006] VERIFY_CNF 1079 CPU : 18.47 = 0 + 0 + 17.67 + 0.8 # RESULT : makespan 1079 SATISFIABLE SHOW_RESULT 1079 BEGIN : [Sun Jun 18 18:59:12 2006] # ASSIGN : makespan 1079 # ASSIGN : s_0_0 353 # ASSIGN : s_0_1 873 # ASSIGN : s_0_2 42 # ASSIGN : s_0_3 867 # ASSIGN : s_0_4 357 # ASSIGN : s_0_5 25 # ASSIGN : s_0_6 32 # ASSIGN : s_0_7 41 # ASSIGN : s_0_8 1014 # ASSIGN : s_0_9 444 # ASSIGN : s_1_0 162 # ASSIGN : s_1_1 742 # ASSIGN : s_1_2 1046 # ASSIGN : s_1_3 317 # ASSIGN : s_1_4 648 # ASSIGN : s_1_5 49 # ASSIGN : s_1_6 50 # ASSIGN : s_1_7 872 # ASSIGN : s_1_8 51 # ASSIGN : s_1_9 1078 # ASSIGN : s_2_0 330 # ASSIGN : s_2_1 1044 # ASSIGN : s_2_2 912 # ASSIGN : s_2_3 1045 # ASSIGN : s_2_4 30 # ASSIGN : s_2_5 331 # ASSIGN : s_2_6 785 # ASSIGN : s_2_7 19 # ASSIGN : s_2_8 20 # ASSIGN : s_2_9 1074 # ASSIGN : s_3_0 1071 # ASSIGN : s_3_1 1078 # ASSIGN : s_3_2 574 # ASSIGN : s_3_3 872 # ASSIGN : s_3_4 1009 # ASSIGN : s_3_5 79 # ASSIGN : s_3_6 33 # ASSIGN : s_3_7 88 # ASSIGN : s_3_8 998 # ASSIGN : s_3_9 7 # ASSIGN : s_4_0 368 # ASSIGN : s_4_1 30 # ASSIGN : s_4_2 2 # ASSIGN : s_4_3 821 # ASSIGN : s_4_4 1073 # ASSIGN : s_4_5 80 # ASSIGN : s_4_6 25 # ASSIGN : s_4_7 630 # ASSIGN : s_4_8 1078 # ASSIGN : s_4_9 864 # ASSIGN : s_5_0 0 # ASSIGN : s_5_1 616 # ASSIGN : s_5_2 911 # ASSIGN : s_5_3 1078 # ASSIGN : s_5_4 753 # ASSIGN : s_5_5 783 # ASSIGN : s_5_6 912 # ASSIGN : s_5_7 807 # ASSIGN : s_5_8 170 # ASSIGN : s_5_9 1077 # ASSIGN : s_6_0 638 # ASSIGN : s_6_1 77 # ASSIGN : s_6_2 3 # ASSIGN : s_6_3 641 # ASSIGN : s_6_4 420 # ASSIGN : s_6_5 818 # ASSIGN : s_6_6 64 # ASSIGN : s_6_7 76 # ASSIGN : s_6_8 2 # ASSIGN : s_6_9 307 # ASSIGN : s_7_0 646 # ASSIGN : s_7_1 261 # ASSIGN : s_7_2 1016 # ASSIGN : s_7_3 1021 # ASSIGN : s_7_4 644 # ASSIGN : s_7_5 33 # ASSIGN : s_7_6 34 # ASSIGN : s_7_7 1023 # ASSIGN : s_7_8 652 # ASSIGN : s_7_9 35 # ASSIGN : s_8_0 1074 # ASSIGN : s_8_1 16 # ASSIGN : s_8_2 1045 # ASSIGN : s_8_3 1048 # ASSIGN : s_8_4 762 # ASSIGN : s_8_5 60 # ASSIGN : s_8_6 67 # ASSIGN : s_8_7 61 # ASSIGN : s_8_8 1013 # ASSIGN : s_8_9 31 # ASSIGN : s_9_0 672 # ASSIGN : s_9_1 1076 # ASSIGN : s_9_2 336 # ASSIGN : s_9_3 24 # ASSIGN : s_9_4 1077 # ASSIGN : s_9_5 23 # ASSIGN : s_9_6 1078 # ASSIGN : s_9_7 561 # ASSIGN : s_9_8 643 # ASSIGN : s_9_9 1075 SHOW_RESULT 1079 END : 1079 (1 seconds) [Sun Jun 18 18:59:13 2006] SHOW_RESULT 1079 CPU : 1.35000000000004 = 1.33000000000004 + 0.02 + 0 + 0 # BOUND : makespan 1000 1079 MODIFY_CNF 1039 BEGIN : [Sun Jun 18 18:59:13 2006] MODIFY_CNF 1039 END : 162791334 bytes (0 seconds) [Sun Jun 18 18:59:13 2006] MODIFY_CNF 1039 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1039 BEGIN : [Sun Jun 18 18:59:13 2006] CMD : minisat /tmp/csp2sat12671.cnf /tmp/csp2sat12671.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 2303439 6555382 | 767813 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 41 (3 /sec) decisions : 105 (7 /sec) propagations : 528940 (34191 /sec) conflict literals : 229 (23.15 % deleted) Memory used : 278.92 MB CPU time : 15.47 s UNSATISFIABLE VERIFY_CNF 1039 END : (16 seconds) [Sun Jun 18 18:59:29 2006] VERIFY_CNF 1039 CPU : 16.24 = 0 + 0 + 15.47 + 0.77 # RESULT : makespan 1039 UNSATISFIABLE # BOUND : makespan 1040 1079 MODIFY_CNF 1059 BEGIN : [Sun Jun 18 18:59:29 2006] MODIFY_CNF 1059 END : 162791334 bytes (0 seconds) [Sun Jun 18 18:59:29 2006] MODIFY_CNF 1059 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1059 BEGIN : [Sun Jun 18 18:59:29 2006] CMD : minisat /tmp/csp2sat12671.cnf /tmp/csp2sat12671.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 2339439 6663382 | 779813 0 0 nan | 0.000 % | | 101 | 2339439 6663382 | 857794 101 1566 15.5 | 72.750 % | | 251 | 2339443 6663382 | 943573 246 3120 12.7 | 72.845 % | ============================================================================== restarts : 3 conflicts : 368 (19 /sec) decisions : 525 (28 /sec) propagations : 4119390 (216241 /sec) conflict literals : 4091 (32.87 % deleted) Memory used : 278.99 MB CPU time : 19.05 s UNSATISFIABLE VERIFY_CNF 1059 END : (20 seconds) [Sun Jun 18 18:59:49 2006] VERIFY_CNF 1059 CPU : 20 = 0 + 0 + 19.05 + 0.95 # RESULT : makespan 1059 UNSATISFIABLE # BOUND : makespan 1060 1079 MODIFY_CNF 1069 BEGIN : [Sun Jun 18 18:59:49 2006] MODIFY_CNF 1069 END : 162791334 bytes (0 seconds) [Sun Jun 18 18:59:49 2006] MODIFY_CNF 1069 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1069 BEGIN : [Sun Jun 18 18:59:49 2006] CMD : minisat /tmp/csp2sat12671.cnf /tmp/csp2sat12671.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 2357439 6717382 | 785813 0 0 nan | 0.000 % | | 100 | 2357439 6717382 | 864394 100 1711 17.1 | 72.468 % | | 250 | 2357439 6717382 | 950833 250 3645 14.6 | 72.468 % | | 475 | 2357440 6717382 | 1045917 474 6830 14.4 | 72.468 % | | 812 | 2357442 6717382 | 1150508 809 10976 13.6 | 72.468 % | ============================================================================== restarts : 5 conflicts : 1312 (43 /sec) decisions : 1678 (55 /sec) propagations : 13768695 (453067 /sec) conflict literals : 16648 (32.77 % deleted) Memory used : 279.04 MB CPU time : 30.39 s UNSATISFIABLE VERIFY_CNF 1069 END : (32 seconds) [Sun Jun 18 19:00:21 2006] VERIFY_CNF 1069 CPU : 31.42 = 0 + 0 + 30.39 + 1.03 # RESULT : makespan 1069 UNSATISFIABLE # BOUND : makespan 1070 1079 MODIFY_CNF 1074 BEGIN : [Sun Jun 18 19:00:21 2006] MODIFY_CNF 1074 END : 162791334 bytes (0 seconds) [Sun Jun 18 19:00:21 2006] MODIFY_CNF 1074 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1074 BEGIN : [Sun Jun 18 19:00:21 2006] CMD : minisat /tmp/csp2sat12671.cnf /tmp/csp2sat12671.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 2366439 6744382 | 788813 0 0 nan | 0.000 % | | 101 | 2366439 6744382 | 867694 101 1940 19.2 | 72.327 % | | 252 | 2366439 6744382 | 954463 252 4026 16.0 | 72.327 % | ============================================================================== restarts : 3 conflicts : 383 (19 /sec) decisions : 710 (36 /sec) propagations : 4185938 (210137 /sec) conflict literals : 5652 (32.66 % deleted) Memory used : 280.55 MB CPU time : 19.92 s SATISFIABLE VERIFY_CNF 1074 END : (20 seconds) [Sun Jun 18 19:00:41 2006] VERIFY_CNF 1074 CPU : 20.81 = 0 + 0 + 20.11 + 0.7 # RESULT : makespan 1074 SATISFIABLE SHOW_RESULT 1074 BEGIN : [Sun Jun 18 19:00:41 2006] # ASSIGN : makespan 1074 # ASSIGN : s_0_0 1070 # ASSIGN : s_0_1 929 # ASSIGN : s_0_2 635 # ASSIGN : s_0_3 11 # ASSIGN : s_0_4 572 # ASSIGN : s_0_5 27 # ASSIGN : s_0_6 10 # ASSIGN : s_0_7 16 # ASSIGN : s_0_8 34 # ASSIGN : s_0_9 152 # ASSIGN : s_1_0 1 # ASSIGN : s_1_1 799 # ASSIGN : s_1_2 1040 # ASSIGN : s_1_3 311 # ASSIGN : s_1_4 658 # ASSIGN : s_1_5 798 # ASSIGN : s_1_6 1073 # ASSIGN : s_1_7 160 # ASSIGN : s_1_8 929 # ASSIGN : s_1_9 1072 # ASSIGN : s_2_0 1050 # ASSIGN : s_2_1 1070 # ASSIGN : s_2_2 935 # ASSIGN : s_2_3 1071 # ASSIGN : s_2_4 28 # ASSIGN : s_2_5 329 # ASSIGN : s_2_6 781 # ASSIGN : s_2_7 328 # ASSIGN : s_2_8 1051 # ASSIGN : s_2_9 1067 # ASSIGN : s_3_0 338 # ASSIGN : s_3_1 1072 # ASSIGN : s_3_2 17 # ASSIGN : s_3_3 873 # ASSIGN : s_3_4 999 # ASSIGN : s_3_5 1073 # ASSIGN : s_3_6 13 # ASSIGN : s_3_7 341 # ASSIGN : s_3_8 1061 # ASSIGN : s_3_9 814 # ASSIGN : s_4_0 341 # ASSIGN : s_4_1 31 # ASSIGN : s_4_2 11 # ASSIGN : s_4_3 1025 # ASSIGN : s_4_4 1068 # ASSIGN : s_4_5 78 # ASSIGN : s_4_6 26 # ASSIGN : s_4_7 828 # ASSIGN : s_4_8 10 # ASSIGN : s_4_9 605 # ASSIGN : s_5_0 156 # ASSIGN : s_5_1 318 # ASSIGN : s_5_2 7 # ASSIGN : s_5_3 17 # ASSIGN : s_5_4 8 # ASSIGN : s_5_5 54 # ASSIGN : s_5_6 908 # ASSIGN : s_5_7 91 # ASSIGN : s_5_8 462 # ASSIGN : s_5_9 1073 # ASSIGN : s_6_0 603 # ASSIGN : s_6_1 131 # ASSIGN : s_6_2 315 # ASSIGN : s_6_3 635 # ASSIGN : s_6_4 354 # ASSIGN : s_6_5 812 # ASSIGN : s_6_6 14 # ASSIGN : s_6_7 17 # ASSIGN : s_6_8 1073 # ASSIGN : s_6_9 18 # ASSIGN : s_7_0 1064 # ASSIGN : s_7_1 444 # ASSIGN : s_7_2 12 # ASSIGN : s_7_3 836 # ASSIGN : s_7_4 1072 # ASSIGN : s_7_5 811 # ASSIGN : s_7_6 34 # ASSIGN : s_7_7 35 # ASSIGN : s_7_8 98 # ASSIGN : s_7_9 838 # ASSIGN : s_8_0 1059 # ASSIGN : s_8_1 15 # ASSIGN : s_8_2 1039 # ASSIGN : s_8_3 999 # ASSIGN : s_8_4 752 # ASSIGN : s_8_5 14 # ASSIGN : s_8_6 57 # ASSIGN : s_8_7 29 # ASSIGN : s_8_8 1072 # ASSIGN : s_8_9 1068 # ASSIGN : s_9_0 606 # ASSIGN : s_9_1 317 # ASSIGN : s_9_2 381 # ASSIGN : s_9_3 18 # ASSIGN : s_9_4 353 # ASSIGN : s_9_5 16 # ASSIGN : s_9_6 17 # ASSIGN : s_9_7 1005 # ASSIGN : s_9_8 1 # ASSIGN : s_9_9 15 SHOW_RESULT 1074 END : 1074 (2 seconds) [Sun Jun 18 19:00:43 2006] SHOW_RESULT 1074 CPU : 1.55000000000002 = 1.54000000000002 + 0.01 + 0 + 0 # BOUND : makespan 1070 1074 MODIFY_CNF 1072 BEGIN : [Sun Jun 18 19:00:43 2006] MODIFY_CNF 1072 END : 162791334 bytes (0 seconds) [Sun Jun 18 19:00:43 2006] MODIFY_CNF 1072 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1072 BEGIN : [Sun Jun 18 19:00:43 2006] CMD : minisat /tmp/csp2sat12671.cnf /tmp/csp2sat12671.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 2362839 6733582 | 787613 0 0 nan | 0.000 % | | 103 | 2362839 6733582 | 866374 103 1888 18.3 | 72.384 % | | 255 | 2362839 6733582 | 953011 255 4295 16.8 | 72.384 % | ============================================================================== restarts : 3 conflicts : 330 (18 /sec) decisions : 753 (40 /sec) propagations : 3426021 (182041 /sec) conflict literals : 5267 (28.26 % deleted) Memory used : 280.55 MB CPU time : 18.82 s SATISFIABLE VERIFY_CNF 1072 END : (20 seconds) [Sun Jun 18 19:01:03 2006] VERIFY_CNF 1072 CPU : 19.84 = 0 + 0.01 + 18.96 + 0.87 # RESULT : makespan 1072 SATISFIABLE SHOW_RESULT 1072 BEGIN : [Sun Jun 18 19:01:03 2006] # ASSIGN : makespan 1072 # ASSIGN : s_0_0 472 # ASSIGN : s_0_1 3 # ASSIGN : s_0_2 178 # ASSIGN : s_0_3 1067 # ASSIGN : s_0_4 476 # ASSIGN : s_0_5 1060 # ASSIGN : s_0_6 177 # ASSIGN : s_0_7 2 # ASSIGN : s_0_8 996 # ASSIGN : s_0_9 539 # ASSIGN : s_1_0 917 # ASSIGN : s_1_1 144 # ASSIGN : s_1_2 1 # ASSIGN : s_1_3 442 # ASSIGN : s_1_4 348 # ASSIGN : s_1_5 0 # ASSIGN : s_1_6 347 # ASSIGN : s_1_7 766 # ASSIGN : s_1_8 33 # ASSIGN : s_1_9 283 # ASSIGN : s_2_0 72 # ASSIGN : s_2_1 765 # ASSIGN : s_2_2 74 # ASSIGN : s_2_3 61 # ASSIGN : s_2_4 766 # ASSIGN : s_2_5 306 # ASSIGN : s_2_6 179 # ASSIGN : s_2_7 0 # ASSIGN : s_2_8 23 # ASSIGN : s_2_9 1 # ASSIGN : s_3_0 9 # ASSIGN : s_3_1 1070 # ASSIGN : s_3_2 768 # ASSIGN : s_3_3 133 # ASSIGN : s_3_4 39 # ASSIGN : s_3_5 1068 # ASSIGN : s_3_6 1071 # ASSIGN : s_3_7 292 # ASSIGN : s_3_8 12 # ASSIGN : s_3_9 259 # ASSIGN : s_4_0 493 # ASSIGN : s_4_1 1009 # ASSIGN : s_4_2 63 # ASSIGN : s_4_3 64 # ASSIGN : s_4_4 1066 # ASSIGN : s_4_5 758 # ASSIGN : s_4_6 6 # ASSIGN : s_4_7 107 # ASSIGN : s_4_8 5 # ASSIGN : s_4_9 284 # ASSIGN : s_5_0 755 # ASSIGN : s_5_1 629 # ASSIGN : s_5_2 1071 # ASSIGN : s_5_3 1066 # ASSIGN : s_5_4 2 # ASSIGN : s_5_5 1036 # ASSIGN : s_5_6 12 # ASSIGN : s_5_7 945 # ASSIGN : s_5_8 183 # ASSIGN : s_5_9 11 # ASSIGN : s_6_0 490 # ASSIGN : s_6_1 775 # ASSIGN : s_6_2 503 # ASSIGN : s_6_3 265 # ASSIGN : s_6_4 547 # ASSIGN : s_6_5 4 # ASSIGN : s_6_6 0 # ASSIGN : s_6_7 765 # ASSIGN : s_6_8 3 # ASSIGN : s_6_9 959 # ASSIGN : s_7_0 25 # ASSIGN : s_7_1 274 # ASSIGN : s_7_2 1066 # ASSIGN : s_7_3 23 # ASSIGN : s_7_4 31 # ASSIGN : s_7_5 1071 # ASSIGN : s_7_6 11 # ASSIGN : s_7_7 1010 # ASSIGN : s_7_8 650 # ASSIGN : s_7_9 33 # ASSIGN : s_8_0 20 # ASSIGN : s_8_1 1056 # ASSIGN : s_8_2 0 # ASSIGN : s_8_3 35 # ASSIGN : s_8_4 101 # ASSIGN : s_8_5 1070 # ASSIGN : s_8_6 361 # ASSIGN : s_8_7 95 # ASSIGN : s_8_8 1071 # ASSIGN : s_8_9 29 # ASSIGN : s_9_0 73 # ASSIGN : s_9_1 1071 # ASSIGN : s_9_2 542 # ASSIGN : s_9_3 767 # ASSIGN : s_9_4 1070 # ASSIGN : s_9_5 1069 # ASSIGN : s_9_6 3 # ASSIGN : s_9_7 4 # ASSIGN : s_9_8 1060 # ASSIGN : s_9_9 2 SHOW_RESULT 1072 END : 1072 (1 seconds) [Sun Jun 18 19:01:04 2006] SHOW_RESULT 1072 CPU : 1.33 = 1.31 + 0.02 + 0 + 0 # BOUND : makespan 1070 1072 MODIFY_CNF 1071 BEGIN : [Sun Jun 18 19:01:04 2006] MODIFY_CNF 1071 END : 162791334 bytes (0 seconds) [Sun Jun 18 19:01:04 2006] MODIFY_CNF 1071 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1071 BEGIN : [Sun Jun 18 19:01:04 2006] CMD : minisat /tmp/csp2sat12671.cnf /tmp/csp2sat12671.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 2361039 6728182 | 787013 0 0 nan | 0.000 % | | 103 | 2361039 6728182 | 865714 103 1820 17.7 | 72.412 % | | 253 | 2361039 6728182 | 952285 253 3695 14.6 | 72.412 % | | 478 | 2361039 6728182 | 1047514 478 6674 14.0 | 72.412 % | | 819 | 2361040 6728182 | 1152265 818 11501 14.1 | 72.412 % | ============================================================================== restarts : 5 conflicts : 1144 (42 /sec) decisions : 1662 (62 /sec) propagations : 11249038 (416940 /sec) conflict literals : 14983 (33.99 % deleted) Memory used : 280.55 MB CPU time : 26.98 s SATISFIABLE VERIFY_CNF 1071 END : (28 seconds) [Sun Jun 18 19:01:32 2006] VERIFY_CNF 1071 CPU : 28.05 = 0 + 0.01 + 27.16 + 0.880000000000001 # RESULT : makespan 1071 SATISFIABLE SHOW_RESULT 1071 BEGIN : [Sun Jun 18 19:01:32 2006] # ASSIGN : makespan 1071 # ASSIGN : s_0_0 632 # ASSIGN : s_0_1 930 # ASSIGN : s_0_2 636 # ASSIGN : s_0_3 10 # ASSIGN : s_0_4 569 # ASSIGN : s_0_5 25 # ASSIGN : s_0_6 32 # ASSIGN : s_0_7 148 # ASSIGN : s_0_8 33 # ASSIGN : s_0_9 149 # ASSIGN : s_1_0 0 # ASSIGN : s_1_1 798 # ASSIGN : s_1_2 1039 # ASSIGN : s_1_3 309 # ASSIGN : s_1_4 644 # ASSIGN : s_1_5 796 # ASSIGN : s_1_6 778 # ASSIGN : s_1_7 158 # ASSIGN : s_1_8 928 # ASSIGN : s_1_9 797 # ASSIGN : s_2_0 1064 # ASSIGN : s_2_1 929 # ASSIGN : s_2_2 935 # ASSIGN : s_2_3 1068 # ASSIGN : s_2_4 27 # ASSIGN : s_2_5 327 # ASSIGN : s_2_6 779 # ASSIGN : s_2_7 26 # ASSIGN : s_2_8 918 # ASSIGN : s_2_9 1046 # ASSIGN : s_3_0 323 # ASSIGN : s_3_1 1 # ASSIGN : s_3_2 14 # ASSIGN : s_3_3 859 # ASSIGN : s_3_4 985 # ASSIGN : s_3_5 0 # ASSIGN : s_3_6 2 # ASSIGN : s_3_7 386 # ASSIGN : s_3_8 3 # ASSIGN : s_3_9 1047 # ASSIGN : s_4_0 326 # ASSIGN : s_4_1 28 # ASSIGN : s_4_2 12 # ASSIGN : s_4_3 816 # ASSIGN : s_4_4 1065 # ASSIGN : s_4_5 75 # ASSIGN : s_4_6 21 # ASSIGN : s_4_7 887 # ASSIGN : s_4_8 1069 # ASSIGN : s_4_9 588 # ASSIGN : s_5_0 155 # ASSIGN : s_5_1 317 # ASSIGN : s_5_2 13 # ASSIGN : s_5_3 15 # ASSIGN : s_5_4 4 # ASSIGN : s_5_5 51 # ASSIGN : s_5_6 906 # ASSIGN : s_5_7 83 # ASSIGN : s_5_8 460 # ASSIGN : s_5_9 148 # ASSIGN : s_6_0 629 # ASSIGN : s_6_1 128 # ASSIGN : s_6_2 312 # ASSIGN : s_6_3 633 # ASSIGN : s_6_4 351 # ASSIGN : s_6_5 810 # ASSIGN : s_6_6 10 # ASSIGN : s_6_7 13 # ASSIGN : s_6_8 14 # ASSIGN : s_6_9 15 # ASSIGN : s_7_0 1065 # ASSIGN : s_7_1 443 # ASSIGN : s_7_2 4 # ASSIGN : s_7_3 1061 # ASSIGN : s_7_4 1063 # ASSIGN : s_7_5 809 # ASSIGN : s_7_6 26 # ASSIGN : s_7_7 27 # ASSIGN : s_7_8 97 # ASSIGN : s_7_9 820 # ASSIGN : s_8_0 1059 # ASSIGN : s_8_1 14 # ASSIGN : s_8_2 9 # ASSIGN : s_8_3 1033 # ASSIGN : s_8_4 738 # ASSIGN : s_8_5 42 # ASSIGN : s_8_6 43 # ASSIGN : s_8_7 1064 # ASSIGN : s_8_8 1070 # ASSIGN : s_8_9 10 # ASSIGN : s_9_0 660 # ASSIGN : s_9_1 316 # ASSIGN : s_9_2 411 # ASSIGN : s_9_3 16 # ASSIGN : s_9_4 1070 # ASSIGN : s_9_5 8 # ASSIGN : s_9_6 15 # ASSIGN : s_9_7 317 # ASSIGN : s_9_8 1060 # ASSIGN : s_9_9 9 SHOW_RESULT 1071 END : 1071 (2 seconds) [Sun Jun 18 19:01:34 2006] SHOW_RESULT 1071 CPU : 1.32999999999999 = 1.31999999999999 + 0.00999999999999979 + 0 + 0 # BOUND : makespan 1070 1071 MODIFY_CNF 1070 BEGIN : [Sun Jun 18 19:01:34 2006] MODIFY_CNF 1070 END : 162791334 bytes (0 seconds) [Sun Jun 18 19:01:34 2006] MODIFY_CNF 1070 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1070 BEGIN : [Sun Jun 18 19:01:34 2006] CMD : minisat /tmp/csp2sat12671.cnf /tmp/csp2sat12671.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 2359239 6722782 | 786413 0 0 nan | 0.000 % | | 100 | 2359239 6722782 | 865054 100 1636 16.4 | 72.440 % | | 250 | 2359239 6722782 | 951559 250 3924 15.7 | 72.440 % | | 475 | 2359239 6722782 | 1046715 475 6861 14.4 | 72.440 % | | 813 | 2359242 6722782 | 1151387 810 12602 15.6 | 72.440 % | ============================================================================== restarts : 5 conflicts : 1218 (45 /sec) decisions : 1559 (58 /sec) propagations : 11580253 (427789 /sec) conflict literals : 17201 (31.10 % deleted) Memory used : 278.99 MB CPU time : 27.07 s UNSATISFIABLE VERIFY_CNF 1070 END : (28 seconds) [Sun Jun 18 19:02:02 2006] VERIFY_CNF 1070 CPU : 27.96 = 0 + 0.01 + 27.07 + 0.879999999999999 # RESULT : makespan 1070 UNSATISFIABLE # BOUND : makespan 1071 1071 MAIN END : (517 seconds) [Sun Jun 18 19:02:02 2006] MAIN CPU : 515.14 = 272.76 + 1.39 + 230.56 + 10.43