# TIMEOUT 18000 MAIN BEGIN : [Sun Jun 18 17:17:12 2006] READ BEGIN : csp/gp08-10.csp [Sun Jun 18 17:17:12 2006] READ END : csp/gp08-10.csp (1 seconds) [Sun Jun 18 17:17:13 2006] READ CPU : 0.98 = 0.98 + 0 + 0 + 0 # BOUND : makespan 1000 3506 GENERATE_CNF 3506 BEGIN : [Sun Jun 18 17:17:13 2006] GENERATE_CNF 3506 END : 227980 variables 3419213 clauses 80137825 bytes (131 seconds) [Sun Jun 18 17:19:24 2006] GENERATE_CNF 3506 CPU : 129.4 = 128.87 + 0.53 + 0 + 0 MODIFY_CNF 2253 BEGIN : [Sun Jun 18 17:19:24 2006] MODIFY_CNF 2253 END : 80137832 bytes (0 seconds) [Sun Jun 18 17:19:24 2006] MODIFY_CNF 2253 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 2253 BEGIN : [Sun Jun 18 17:19:24 2006] CMD : minisat /tmp/csp2sat10922.cnf /tmp/csp2sat10922.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 2295176 6659604 | 765058 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 297 (61 /sec) propagations : 227980 (46909 /sec) conflict literals : 0 ( nan % deleted) Memory used : 141.64 MB CPU time : 4.86 s SATISFIABLE VERIFY_CNF 2253 END : (5 seconds) [Sun Jun 18 17:19:29 2006] VERIFY_CNF 2253 CPU : 5.52 = 0 + 0.01 + 4.97 + 0.54 # RESULT : makespan 2253 SATISFIABLE SHOW_RESULT 2253 BEGIN : [Sun Jun 18 17:19:29 2006] # ASSIGN : makespan 2253 # ASSIGN : s_0_0 302 # ASSIGN : s_0_1 117 # ASSIGN : s_0_2 135 # ASSIGN : s_0_3 1251 # ASSIGN : s_0_4 136 # ASSIGN : s_0_5 190 # ASSIGN : s_0_6 0 # ASSIGN : s_0_7 1 # ASSIGN : s_1_0 692 # ASSIGN : s_1_1 743 # ASSIGN : s_1_2 931 # ASSIGN : s_1_3 1705 # ASSIGN : s_1_4 142 # ASSIGN : s_1_5 318 # ASSIGN : s_1_6 18 # ASSIGN : s_1_7 19 # ASSIGN : s_2_0 693 # ASSIGN : s_2_1 1088 # ASSIGN : s_2_2 1338 # ASSIGN : s_2_3 1708 # ASSIGN : s_2_4 452 # ASSIGN : s_2_5 453 # ASSIGN : s_2_6 94 # ASSIGN : s_2_7 108 # ASSIGN : s_3_0 694 # ASSIGN : s_3_1 1369 # ASSIGN : s_3_2 1829 # ASSIGN : s_3_3 2043 # ASSIGN : s_3_4 493 # ASSIGN : s_3_5 494 # ASSIGN : s_3_6 95 # ASSIGN : s_3_7 109 # ASSIGN : s_4_0 1090 # ASSIGN : s_4_1 1370 # ASSIGN : s_4_2 1832 # ASSIGN : s_4_3 2044 # ASSIGN : s_4_4 1065 # ASSIGN : s_4_5 741 # ASSIGN : s_4_6 351 # ASSIGN : s_4_7 1066 # ASSIGN : s_5_0 1091 # ASSIGN : s_5_1 1909 # ASSIGN : s_5_2 1963 # ASSIGN : s_5_3 2045 # ASSIGN : s_5_4 1096 # ASSIGN : s_5_5 745 # ASSIGN : s_5_6 1075 # ASSIGN : s_5_7 1076 # ASSIGN : s_6_0 1252 # ASSIGN : s_6_1 2023 # ASSIGN : s_6_2 2049 # ASSIGN : s_6_3 2050 # ASSIGN : s_6_4 2250 # ASSIGN : s_6_5 770 # ASSIGN : s_6_6 1458 # ASSIGN : s_6_7 1541 # ASSIGN : s_7_0 1253 # ASSIGN : s_7_1 2050 # ASSIGN : s_7_2 2051 # ASSIGN : s_7_3 2056 # ASSIGN : s_7_4 2251 # ASSIGN : s_7_5 1458 # ASSIGN : s_7_6 1459 # ASSIGN : s_7_7 2252 SHOW_RESULT 2253 END : 2253 (1 seconds) [Sun Jun 18 17:19:30 2006] SHOW_RESULT 2253 CPU : 0.490000000000008 = 0.460000000000008 + 0.0299999999999999 + 0 + 0 # BOUND : makespan 1000 2253 MODIFY_CNF 1626 BEGIN : [Sun Jun 18 17:19:30 2006] MODIFY_CNF 1626 END : 80137831 bytes (0 seconds) [Sun Jun 18 17:19:30 2006] MODIFY_CNF 1626 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1626 BEGIN : [Sun Jun 18 17:19:30 2006] CMD : minisat /tmp/csp2sat10922.cnf /tmp/csp2sat10922.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1733384 4974228 | 577794 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (0 /sec) decisions : 284 (53 /sec) propagations : 255717 (47887 /sec) conflict literals : 19 (9.52 % deleted) Memory used : 141.64 MB CPU time : 5.34 s SATISFIABLE VERIFY_CNF 1626 END : (6 seconds) [Sun Jun 18 17:19:36 2006] VERIFY_CNF 1626 CPU : 5.88 = 0 + 0 + 5.46 + 0.42 # RESULT : makespan 1626 SATISFIABLE SHOW_RESULT 1626 BEGIN : [Sun Jun 18 17:19:36 2006] # ASSIGN : makespan 1626 # ASSIGN : s_0_0 615 # ASSIGN : s_0_1 24 # ASSIGN : s_0_2 42 # ASSIGN : s_0_3 161 # ASSIGN : s_0_4 43 # ASSIGN : s_0_5 49 # ASSIGN : s_0_6 0 # ASSIGN : s_0_7 1 # ASSIGN : s_1_0 17 # ASSIGN : s_1_1 1403 # ASSIGN : s_1_2 625 # ASSIGN : s_1_3 622 # ASSIGN : s_1_4 446 # ASSIGN : s_1_5 311 # ASSIGN : s_1_6 18 # ASSIGN : s_1_7 19 # ASSIGN : s_2_0 92 # ASSIGN : s_2_1 203 # ASSIGN : s_2_2 1032 # ASSIGN : s_2_3 697 # ASSIGN : s_2_4 696 # ASSIGN : s_2_5 453 # ASSIGN : s_2_6 93 # ASSIGN : s_2_7 108 # ASSIGN : s_3_0 1006 # ASSIGN : s_3_1 493 # ASSIGN : s_3_2 1402 # ASSIGN : s_3_3 696 # ASSIGN : s_3_4 721 # ASSIGN : s_3_5 494 # ASSIGN : s_3_6 94 # ASSIGN : s_3_7 109 # ASSIGN : s_4_0 107 # ASSIGN : s_4_1 941 # ASSIGN : s_4_2 1405 # ASSIGN : s_4_3 690 # ASSIGN : s_4_4 722 # ASSIGN : s_4_5 694 # ASSIGN : s_4_6 108 # ASSIGN : s_4_7 498 # ASSIGN : s_5_0 502 # ASSIGN : s_5_1 637 # ASSIGN : s_5_2 1536 # ASSIGN : s_5_3 691 # ASSIGN : s_5_4 723 # ASSIGN : s_5_5 698 # ASSIGN : s_5_6 507 # ASSIGN : s_5_7 508 # ASSIGN : s_6_0 1005 # ASSIGN : s_6_1 1591 # ASSIGN : s_6_2 1618 # ASSIGN : s_6_3 1103 # ASSIGN : s_6_4 1617 # ASSIGN : s_6_5 1109 # ASSIGN : s_6_6 522 # ASSIGN : s_6_7 523 # ASSIGN : s_7_0 1412 # ASSIGN : s_7_1 1617 # ASSIGN : s_7_2 1619 # ASSIGN : s_7_3 1217 # ASSIGN : s_7_4 1618 # ASSIGN : s_7_5 1624 # ASSIGN : s_7_6 626 # ASSIGN : s_7_7 1625 SHOW_RESULT 1626 END : 1626 (0 seconds) [Sun Jun 18 17:19:36 2006] SHOW_RESULT 1626 CPU : 0.689999999999998 = 0.689999999999998 + 0 + 0 + 0 # BOUND : makespan 1000 1626 MODIFY_CNF 1313 BEGIN : [Sun Jun 18 17:19:36 2006] MODIFY_CNF 1313 END : 80137831 bytes (0 seconds) [Sun Jun 18 17:19:36 2006] MODIFY_CNF 1313 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1313 BEGIN : [Sun Jun 18 17:19:36 2006] CMD : minisat /tmp/csp2sat10922.cnf /tmp/csp2sat10922.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1452936 4132884 | 484312 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 4 (1 /sec) decisions : 224 (41 /sec) propagations : 303899 (55864 /sec) conflict literals : 23 (4.17 % deleted) Memory used : 141.64 MB CPU time : 5.44 s SATISFIABLE VERIFY_CNF 1313 END : (6 seconds) [Sun Jun 18 17:19:42 2006] VERIFY_CNF 1313 CPU : 6 = 0 + 0 + 5.55 + 0.45 # RESULT : makespan 1313 SATISFIABLE SHOW_RESULT 1313 BEGIN : [Sun Jun 18 17:19:42 2006] # ASSIGN : makespan 1313 # ASSIGN : s_0_0 85 # ASSIGN : s_0_1 1232 # ASSIGN : s_0_2 0 # ASSIGN : s_0_3 475 # ASSIGN : s_0_4 953 # ASSIGN : s_0_5 998 # ASSIGN : s_0_6 14 # ASSIGN : s_0_7 67 # ASSIGN : s_1_0 0 # ASSIGN : s_1_1 306 # ASSIGN : s_1_2 552 # ASSIGN : s_1_3 1307 # ASSIGN : s_1_4 959 # ASSIGN : s_1_5 1135 # ASSIGN : s_1_6 15 # ASSIGN : s_1_7 217 # ASSIGN : s_2_0 1 # ASSIGN : s_2_1 494 # ASSIGN : s_2_2 5 # ASSIGN : s_2_3 934 # ASSIGN : s_2_4 1269 # ASSIGN : s_2_5 1270 # ASSIGN : s_2_6 0 # ASSIGN : s_2_7 375 # ASSIGN : s_3_0 767 # ASSIGN : s_3_1 15 # ASSIGN : s_3_2 1 # ASSIGN : s_3_3 1312 # ASSIGN : s_3_4 0 # ASSIGN : s_3_5 30 # ASSIGN : s_3_6 16 # ASSIGN : s_3_7 376 # ASSIGN : s_4_0 2 # ASSIGN : s_4_1 770 # ASSIGN : s_4_2 421 # ASSIGN : s_4_3 1310 # ASSIGN : s_4_4 1311 # ASSIGN : s_4_5 26 # ASSIGN : s_4_6 31 # ASSIGN : s_4_7 760 # ASSIGN : s_5_0 1163 # ASSIGN : s_5_1 1250 # ASSIGN : s_5_2 1168 # ASSIGN : s_5_3 929 # ASSIGN : s_5_4 2 # ASSIGN : s_5_5 1110 # ASSIGN : s_5_6 1 # ASSIGN : s_5_7 815 # ASSIGN : s_6_0 3 # ASSIGN : s_6_1 744 # ASSIGN : s_6_2 4 # ASSIGN : s_6_3 224 # ASSIGN : s_6_4 1312 # ASSIGN : s_6_5 230 # ASSIGN : s_6_6 712 # ASSIGN : s_6_7 830 # ASSIGN : s_7_0 508 # ASSIGN : s_7_1 1304 # ASSIGN : s_7_2 1305 # ASSIGN : s_7_3 280 # ASSIGN : s_7_4 1310 # ASSIGN : s_7_5 1311 # ASSIGN : s_7_6 713 # ASSIGN : s_7_7 1312 SHOW_RESULT 1313 END : 1313 (1 seconds) [Sun Jun 18 17:19:43 2006] SHOW_RESULT 1313 CPU : 0.679999999999988 = 0.669999999999987 + 0.01 + 0 + 0 # BOUND : makespan 1000 1313 MODIFY_CNF 1156 BEGIN : [Sun Jun 18 17:19:43 2006] MODIFY_CNF 1156 END : 80137831 bytes (0 seconds) [Sun Jun 18 17:19:43 2006] MODIFY_CNF 1156 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1156 BEGIN : [Sun Jun 18 17:19:43 2006] CMD : minisat /tmp/csp2sat10922.cnf /tmp/csp2sat10922.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1312264 3710868 | 437421 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 5 (1 /sec) decisions : 28 (5 /sec) propagations : 194347 (35208 /sec) conflict literals : 8 (11.11 % deleted) Memory used : 140.59 MB CPU time : 5.52 s UNSATISFIABLE VERIFY_CNF 1156 END : (6 seconds) [Sun Jun 18 17:19:49 2006] VERIFY_CNF 1156 CPU : 6.07 = 0 + 0 + 5.52 + 0.55 # RESULT : makespan 1156 UNSATISFIABLE # BOUND : makespan 1157 1313 MODIFY_CNF 1235 BEGIN : [Sun Jun 18 17:19:49 2006] MODIFY_CNF 1235 END : 80137831 bytes (0 seconds) [Sun Jun 18 17:19:49 2006] MODIFY_CNF 1235 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1235 BEGIN : [Sun Jun 18 17:19:49 2006] CMD : minisat /tmp/csp2sat10922.cnf /tmp/csp2sat10922.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1383048 3923220 | 461016 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 4 (1 /sec) decisions : 168 (29 /sec) propagations : 243127 (41703 /sec) conflict literals : 31 (6.06 % deleted) Memory used : 141.64 MB CPU time : 5.83 s SATISFIABLE VERIFY_CNF 1235 END : (7 seconds) [Sun Jun 18 17:19:56 2006] VERIFY_CNF 1235 CPU : 6.51 = 0 + 0.01 + 5.94 + 0.56 # RESULT : makespan 1235 SATISFIABLE SHOW_RESULT 1235 BEGIN : [Sun Jun 18 17:19:56 2006] # ASSIGN : makespan 1235 # ASSIGN : s_0_0 28 # ASSIGN : s_0_1 4 # ASSIGN : s_0_2 0 # ASSIGN : s_0_3 780 # ASSIGN : s_0_4 22 # ASSIGN : s_0_5 668 # ASSIGN : s_0_6 1 # ASSIGN : s_0_7 616 # ASSIGN : s_1_0 1 # ASSIGN : s_1_1 1017 # ASSIGN : s_1_2 227 # ASSIGN : s_1_3 48 # ASSIGN : s_1_4 51 # ASSIGN : s_1_5 882 # ASSIGN : s_1_6 2 # ASSIGN : s_1_7 634 # ASSIGN : s_2_0 2 # ASSIGN : s_2_1 73 # ASSIGN : s_2_2 659 # ASSIGN : s_2_3 324 # ASSIGN : s_2_4 323 # ASSIGN : s_2_5 32 # ASSIGN : s_2_6 3 # ASSIGN : s_2_7 9 # ASSIGN : s_3_0 633 # ASSIGN : s_3_1 3 # ASSIGN : s_3_2 1029 # ASSIGN : s_3_3 9 # ASSIGN : s_3_4 404 # ASSIGN : s_3_5 1032 # ASSIGN : s_3_6 405 # ASSIGN : s_3_7 10 # ASSIGN : s_4_0 418 # ASSIGN : s_4_1 555 # ASSIGN : s_4_2 1103 # ASSIGN : s_4_3 1234 # ASSIGN : s_4_4 419 # ASSIGN : s_4_5 0 # ASSIGN : s_4_6 4 # ASSIGN : s_4_7 394 # ASSIGN : s_5_0 22 # ASSIGN : s_5_1 350 # ASSIGN : s_5_2 36 # ASSIGN : s_5_3 118 # ASSIGN : s_5_4 420 # ASSIGN : s_5_5 132 # ASSIGN : s_5_6 419 # ASSIGN : s_5_7 404 # ASSIGN : s_6_0 27 # ASSIGN : s_6_1 1205 # ASSIGN : s_6_2 122 # ASSIGN : s_6_3 123 # ASSIGN : s_6_4 1233 # ASSIGN : s_6_5 157 # ASSIGN : s_6_6 639 # ASSIGN : s_6_7 723 # ASSIGN : s_7_0 428 # ASSIGN : s_7_1 1231 # ASSIGN : s_7_2 124 # ASSIGN : s_7_3 129 # ASSIGN : s_7_4 1234 # ASSIGN : s_7_5 1232 # ASSIGN : s_7_6 640 # ASSIGN : s_7_7 1233 SHOW_RESULT 1235 END : 1235 (0 seconds) [Sun Jun 18 17:19:56 2006] SHOW_RESULT 1235 CPU : 0.670000000000006 = 0.650000000000006 + 0.02 + 0 + 0 # BOUND : makespan 1157 1235 MODIFY_CNF 1196 BEGIN : [Sun Jun 18 17:19:56 2006] MODIFY_CNF 1196 END : 80137831 bytes (0 seconds) [Sun Jun 18 17:19:56 2006] MODIFY_CNF 1196 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1196 BEGIN : [Sun Jun 18 17:19:56 2006] CMD : minisat /tmp/csp2sat10922.cnf /tmp/csp2sat10922.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1348104 3818388 | 449368 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 1 (0 /sec) decisions : 184 (32 /sec) propagations : 235491 (40672 /sec) conflict literals : 7 (0.00 % deleted) Memory used : 141.64 MB CPU time : 5.79 s SATISFIABLE VERIFY_CNF 1196 END : (7 seconds) [Sun Jun 18 17:20:03 2006] VERIFY_CNF 1196 CPU : 6.37 = 0 + 0 + 5.88 + 0.49 # RESULT : makespan 1196 SATISFIABLE SHOW_RESULT 1196 BEGIN : [Sun Jun 18 17:20:03 2006] # ASSIGN : makespan 1196 # ASSIGN : s_0_0 209 # ASSIGN : s_0_1 0 # ASSIGN : s_0_2 127 # ASSIGN : s_0_3 742 # ASSIGN : s_0_4 36 # ASSIGN : s_0_5 630 # ASSIGN : s_0_6 128 # ASSIGN : s_0_7 18 # ASSIGN : s_1_0 1011 # ASSIGN : s_1_1 537 # ASSIGN : s_1_2 130 # ASSIGN : s_1_3 37 # ASSIGN : s_1_4 1012 # ASSIGN : s_1_5 860 # ASSIGN : s_1_6 129 # ASSIGN : s_1_7 40 # ASSIGN : s_2_0 1190 # ASSIGN : s_2_1 152 # ASSIGN : s_2_2 737 # ASSIGN : s_2_3 402 # ASSIGN : s_2_4 42 # ASSIGN : s_2_5 43 # ASSIGN : s_2_6 150 # ASSIGN : s_2_7 151 # ASSIGN : s_3_0 599 # ASSIGN : s_3_1 25 # ASSIGN : s_3_2 591 # ASSIGN : s_3_3 81 # ASSIGN : s_3_4 111 # ASSIGN : s_3_5 995 # ASSIGN : s_3_6 169 # ASSIGN : s_3_7 207 # ASSIGN : s_4_0 0 # ASSIGN : s_4_1 725 # ASSIGN : s_4_2 594 # ASSIGN : s_4_3 82 # ASSIGN : s_4_4 1195 # ASSIGN : s_4_5 84 # ASSIGN : s_4_6 204 # ASSIGN : s_4_7 174 # ASSIGN : s_5_0 1191 # ASSIGN : s_5_1 26 # ASSIGN : s_5_2 1107 # ASSIGN : s_5_3 83 # ASSIGN : s_5_4 199 # ASSIGN : s_5_5 88 # ASSIGN : s_5_6 183 # ASSIGN : s_5_7 184 # ASSIGN : s_6_0 1 # ASSIGN : s_6_1 80 # ASSIGN : s_6_2 1189 # ASSIGN : s_6_3 106 # ASSIGN : s_6_4 112 # ASSIGN : s_6_5 113 # ASSIGN : s_6_6 595 # ASSIGN : s_6_7 707 # ASSIGN : s_7_0 2 # ASSIGN : s_7_1 1187 # ASSIGN : s_7_2 1190 # ASSIGN : s_7_3 207 # ASSIGN : s_7_4 1188 # ASSIGN : s_7_5 1195 # ASSIGN : s_7_6 596 # ASSIGN : s_7_7 1189 SHOW_RESULT 1196 END : 1196 (0 seconds) [Sun Jun 18 17:20:03 2006] SHOW_RESULT 1196 CPU : 0.669999999999987 = 0.669999999999987 + 0 + 0 + 0 # BOUND : makespan 1157 1196 MODIFY_CNF 1176 BEGIN : [Sun Jun 18 17:20:03 2006] MODIFY_CNF 1176 END : 80137831 bytes (0 seconds) [Sun Jun 18 17:20:03 2006] MODIFY_CNF 1176 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1176 BEGIN : [Sun Jun 18 17:20:03 2006] CMD : minisat /tmp/csp2sat10922.cnf /tmp/csp2sat10922.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1330184 3764628 | 443394 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 1 (0 /sec) decisions : 159 (28 /sec) propagations : 234712 (40962 /sec) conflict literals : 5 (0.00 % deleted) Memory used : 141.64 MB CPU time : 5.73 s SATISFIABLE VERIFY_CNF 1176 END : (7 seconds) [Sun Jun 18 17:20:10 2006] VERIFY_CNF 1176 CPU : 6.25 = 0 + 0 + 5.85 + 0.4 # RESULT : makespan 1176 SATISFIABLE SHOW_RESULT 1176 BEGIN : [Sun Jun 18 17:20:10 2006] # ASSIGN : makespan 1176 # ASSIGN : s_0_0 176 # ASSIGN : s_0_1 144 # ASSIGN : s_0_2 0 # ASSIGN : s_0_3 702 # ASSIGN : s_0_4 170 # ASSIGN : s_0_5 3 # ASSIGN : s_0_6 2 # ASSIGN : s_0_7 1156 # ASSIGN : s_1_0 1 # ASSIGN : s_1_1 650 # ASSIGN : s_1_2 140 # ASSIGN : s_1_3 562 # ASSIGN : s_1_4 998 # ASSIGN : s_1_5 838 # ASSIGN : s_1_6 24 # ASSIGN : s_1_7 25 # ASSIGN : s_2_0 2 # ASSIGN : s_2_1 917 # ASSIGN : s_2_2 547 # ASSIGN : s_2_3 212 # ASSIGN : s_2_4 179 # ASSIGN : s_2_5 115 # ASSIGN : s_2_6 113 # ASSIGN : s_2_7 114 # ASSIGN : s_3_0 566 # ASSIGN : s_3_1 0 # ASSIGN : s_3_2 1 # ASSIGN : s_3_3 565 # ASSIGN : s_3_4 180 # ASSIGN : s_3_5 973 # ASSIGN : s_3_6 130 # ASSIGN : s_3_7 181 # ASSIGN : s_4_0 3 # ASSIGN : s_4_1 188 # ASSIGN : s_4_2 4 # ASSIGN : s_4_3 701 # ASSIGN : s_4_4 184 # ASSIGN : s_4_5 156 # ASSIGN : s_4_6 786 # ASSIGN : s_4_7 135 # ASSIGN : s_5_0 85 # ASSIGN : s_5_1 90 # ASSIGN : s_5_2 1081 # ASSIGN : s_5_3 1163 # ASSIGN : s_5_4 185 # ASSIGN : s_5_5 160 # ASSIGN : s_5_6 144 # ASSIGN : s_5_7 145 # ASSIGN : s_6_0 161 # ASSIGN : s_6_1 162 # ASSIGN : s_6_2 1167 # ASSIGN : s_6_3 1168 # ASSIGN : s_6_4 1174 # ASSIGN : s_6_5 192 # ASSIGN : s_6_6 191 # ASSIGN : s_6_7 674 # ASSIGN : s_7_0 962 # ASSIGN : s_7_1 1167 # ASSIGN : s_7_2 1168 # ASSIGN : s_7_3 0 # ASSIGN : s_7_4 1175 # ASSIGN : s_7_5 1173 # ASSIGN : s_7_6 195 # ASSIGN : s_7_7 1174 SHOW_RESULT 1176 END : 1176 (0 seconds) [Sun Jun 18 17:20:10 2006] SHOW_RESULT 1176 CPU : 0.669999999999997 = 0.659999999999997 + 0.01 + 0 + 0 # BOUND : makespan 1157 1176 MODIFY_CNF 1166 BEGIN : [Sun Jun 18 17:20:10 2006] MODIFY_CNF 1166 END : 80137831 bytes (0 seconds) [Sun Jun 18 17:20:10 2006] MODIFY_CNF 1166 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1166 BEGIN : [Sun Jun 18 17:20:10 2006] CMD : minisat /tmp/csp2sat10922.cnf /tmp/csp2sat10922.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1321224 3737748 | 440408 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 13 (2 /sec) decisions : 212 (37 /sec) propagations : 280533 (48788 /sec) conflict literals : 65 (2.99 % deleted) Memory used : 141.64 MB CPU time : 5.75 s SATISFIABLE VERIFY_CNF 1166 END : (7 seconds) [Sun Jun 18 17:20:17 2006] VERIFY_CNF 1166 CPU : 6.31 = 0 + 0 + 5.86 + 0.45 # RESULT : makespan 1166 SATISFIABLE SHOW_RESULT 1166 BEGIN : [Sun Jun 18 17:20:17 2006] # ASSIGN : makespan 1166 # ASSIGN : s_0_0 207 # ASSIGN : s_0_1 31 # ASSIGN : s_0_2 5 # ASSIGN : s_0_3 597 # ASSIGN : s_0_4 6 # ASSIGN : s_0_5 1051 # ASSIGN : s_0_6 12 # ASSIGN : s_0_7 13 # ASSIGN : s_1_0 764 # ASSIGN : s_1_1 49 # ASSIGN : s_1_2 243 # ASSIGN : s_1_3 33 # ASSIGN : s_1_4 900 # ASSIGN : s_1_5 765 # ASSIGN : s_1_6 32 # ASSIGN : s_1_7 1076 # ASSIGN : s_2_0 649 # ASSIGN : s_2_1 390 # ASSIGN : s_2_2 650 # ASSIGN : s_2_3 42 # ASSIGN : s_2_4 1162 # ASSIGN : s_2_5 0 # ASSIGN : s_2_6 41 # ASSIGN : s_2_7 1075 # ASSIGN : s_3_0 765 # ASSIGN : s_3_1 4 # ASSIGN : s_3_2 32 # ASSIGN : s_3_3 1162 # ASSIGN : s_3_4 1163 # ASSIGN : s_3_5 565 # ASSIGN : s_3_6 57 # ASSIGN : s_3_7 181 # ASSIGN : s_4_0 0 # ASSIGN : s_4_1 640 # ASSIGN : s_4_2 50 # ASSIGN : s_4_3 1164 # ASSIGN : s_4_4 1165 # ASSIGN : s_4_5 42 # ASSIGN : s_4_6 181 # ASSIGN : s_4_7 32 # ASSIGN : s_5_0 1161 # ASSIGN : s_5_1 1102 # ASSIGN : s_5_2 1020 # ASSIGN : s_5_3 1156 # ASSIGN : s_5_4 87 # ASSIGN : s_5_5 46 # ASSIGN : s_5_6 71 # ASSIGN : s_5_7 72 # ASSIGN : s_6_0 1 # ASSIGN : s_6_1 5 # ASSIGN : s_6_2 35 # ASSIGN : s_6_3 36 # ASSIGN : s_6_4 82 # ASSIGN : s_6_5 83 # ASSIGN : s_6_6 571 # ASSIGN : s_6_7 593 # ASSIGN : s_7_0 2 # ASSIGN : s_7_1 237 # ASSIGN : s_7_2 238 # ASSIGN : s_7_3 377 # ASSIGN : s_7_4 1164 # ASSIGN : s_7_5 1163 # ASSIGN : s_7_6 572 # ASSIGN : s_7_7 1165 SHOW_RESULT 1166 END : 1166 (0 seconds) [Sun Jun 18 17:20:17 2006] SHOW_RESULT 1166 CPU : 0.669999999999997 = 0.659999999999997 + 0.01 + 0 + 0 # BOUND : makespan 1157 1166 MODIFY_CNF 1161 BEGIN : [Sun Jun 18 17:20:17 2006] MODIFY_CNF 1161 END : 80137831 bytes (0 seconds) [Sun Jun 18 17:20:17 2006] MODIFY_CNF 1161 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1161 BEGIN : [Sun Jun 18 17:20:17 2006] CMD : minisat /tmp/csp2sat10922.cnf /tmp/csp2sat10922.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1316744 3724308 | 438914 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 8 (1 /sec) decisions : 197 (33 /sec) propagations : 251260 (42659 /sec) conflict literals : 32 (8.57 % deleted) Memory used : 141.64 MB CPU time : 5.89 s SATISFIABLE VERIFY_CNF 1161 END : (7 seconds) [Sun Jun 18 17:20:24 2006] VERIFY_CNF 1161 CPU : 6.34 = 0 + 0 + 6 + 0.34 # RESULT : makespan 1161 SATISFIABLE SHOW_RESULT 1161 BEGIN : [Sun Jun 18 17:20:24 2006] # ASSIGN : makespan 1161 # ASSIGN : s_0_0 205 # ASSIGN : s_0_1 25 # ASSIGN : s_0_2 204 # ASSIGN : s_0_3 595 # ASSIGN : s_0_4 19 # ASSIGN : s_0_5 1049 # ASSIGN : s_0_6 18 # ASSIGN : s_0_7 0 # ASSIGN : s_1_0 757 # ASSIGN : s_1_1 43 # ASSIGN : s_1_2 231 # ASSIGN : s_1_3 11 # ASSIGN : s_1_4 894 # ASSIGN : s_1_5 759 # ASSIGN : s_1_6 25 # ASSIGN : s_1_7 1070 # ASSIGN : s_2_0 637 # ASSIGN : s_2_1 363 # ASSIGN : s_2_2 638 # ASSIGN : s_2_3 27 # ASSIGN : s_2_4 25 # ASSIGN : s_2_5 1008 # ASSIGN : s_2_6 26 # ASSIGN : s_2_7 1159 # ASSIGN : s_3_0 758 # ASSIGN : s_3_1 13 # ASSIGN : s_3_2 26 # ASSIGN : s_3_3 14 # ASSIGN : s_3_4 29 # ASSIGN : s_3_5 558 # ASSIGN : s_3_6 51 # ASSIGN : s_3_7 174 # ASSIGN : s_4_0 1154 # ASSIGN : s_4_1 613 # ASSIGN : s_4_2 41 # ASSIGN : s_4_3 15 # ASSIGN : s_4_4 30 # ASSIGN : s_4_5 26 # ASSIGN : s_4_6 172 # ASSIGN : s_4_7 31 # ASSIGN : s_5_0 1155 # ASSIGN : s_5_1 1101 # ASSIGN : s_5_2 1019 # ASSIGN : s_5_3 16 # ASSIGN : s_5_4 81 # ASSIGN : s_5_5 40 # ASSIGN : s_5_6 65 # ASSIGN : s_5_7 66 # ASSIGN : s_6_0 1160 # ASSIGN : s_6_1 1075 # ASSIGN : s_6_2 20 # ASSIGN : s_6_3 21 # ASSIGN : s_6_4 1158 # ASSIGN : s_6_5 75 # ASSIGN : s_6_6 562 # ASSIGN : s_6_7 588 # ASSIGN : s_7_0 0 # ASSIGN : s_7_1 361 # ASSIGN : s_7_2 1154 # ASSIGN : s_7_3 362 # ASSIGN : s_7_4 1159 # ASSIGN : s_7_5 557 # ASSIGN : s_7_6 563 # ASSIGN : s_7_7 1160 SHOW_RESULT 1161 END : 1161 (0 seconds) [Sun Jun 18 17:20:24 2006] SHOW_RESULT 1161 CPU : 0.670000000000025 = 0.660000000000025 + 0.01 + 0 + 0 # BOUND : makespan 1157 1161 MODIFY_CNF 1159 BEGIN : [Sun Jun 18 17:20:24 2006] MODIFY_CNF 1159 END : 80137831 bytes (0 seconds) [Sun Jun 18 17:20:24 2006] MODIFY_CNF 1159 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1159 BEGIN : [Sun Jun 18 17:20:24 2006] CMD : minisat /tmp/csp2sat10922.cnf /tmp/csp2sat10922.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1314952 3718932 | 438317 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 5 (1 /sec) decisions : 28 (5 /sec) propagations : 193205 (32526 /sec) conflict literals : 8 (11.11 % deleted) Memory used : 140.58 MB CPU time : 5.94 s UNSATISFIABLE VERIFY_CNF 1159 END : (7 seconds) [Sun Jun 18 17:20:31 2006] VERIFY_CNF 1159 CPU : 6.32 = 0 + 0 + 5.94 + 0.38 # RESULT : makespan 1159 UNSATISFIABLE # BOUND : makespan 1160 1161 MODIFY_CNF 1160 BEGIN : [Sun Jun 18 17:20:31 2006] MODIFY_CNF 1160 END : 80137831 bytes (0 seconds) [Sun Jun 18 17:20:31 2006] MODIFY_CNF 1160 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1160 BEGIN : [Sun Jun 18 17:20:31 2006] CMD : minisat /tmp/csp2sat10922.cnf /tmp/csp2sat10922.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1315848 3721620 | 438616 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 5 (1 /sec) decisions : 28 (5 /sec) propagations : 193142 (33825 /sec) conflict literals : 8 (11.11 % deleted) Memory used : 140.58 MB CPU time : 5.71 s UNSATISFIABLE VERIFY_CNF 1160 END : (6 seconds) [Sun Jun 18 17:20:37 2006] VERIFY_CNF 1160 CPU : 6.05 = 0 + 0 + 5.71 + 0.34 # RESULT : makespan 1160 UNSATISFIABLE # BOUND : makespan 1161 1161 MAIN END : (205 seconds) [Sun Jun 18 17:20:37 2006] MAIN CPU : 203.29 = 135.05 + 0.64 + 62.68 + 4.92