# TIMEOUT 18000 MAIN BEGIN : [Sun Jun 18 17:56:30 2006] READ BEGIN : csp/gp09-07.csp [Sun Jun 18 17:56:30 2006] READ END : csp/gp09-07.csp (2 seconds) [Sun Jun 18 17:56:32 2006] READ CPU : 1.34 = 1.32 + 0.02 + 0 + 0 # BOUND : makespan 1000 3963 GENERATE_CNF 3963 BEGIN : [Sun Jun 18 17:56:32 2006] GENERATE_CNF 3963 END : 325507 variables 5559665 clauses 132282767 bytes (214 seconds) [Sun Jun 18 18:00:06 2006] GENERATE_CNF 3963 CPU : 213.28 = 212.33 + 0.95 + 0 + 0 MODIFY_CNF 2481 BEGIN : [Sun Jun 18 18:00:06 2006] MODIFY_CNF 2481 END : 132282774 bytes (0 seconds) [Sun Jun 18 18:00:06 2006] MODIFY_CNF 2481 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 2481 BEGIN : [Sun Jun 18 18:00:06 2006] CMD : minisat /tmp/csp2sat11595.cnf /tmp/csp2sat11595.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 3637125 10588711 | 1212375 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 8 (1 /sec) decisions : 491 (59 /sec) propagations : 380716 (45814 /sec) conflict literals : 123 (3.15 % deleted) Memory used : 218.62 MB CPU time : 8.31 s SATISFIABLE VERIFY_CNF 2481 END : (9 seconds) [Sun Jun 18 18:00:15 2006] VERIFY_CNF 2481 CPU : 9.04 = 0 + 0 + 8.47 + 0.57 # RESULT : makespan 2481 SATISFIABLE SHOW_RESULT 2481 BEGIN : [Sun Jun 18 18:00:15 2006] # ASSIGN : makespan 2481 # ASSIGN : s_0_0 1318 # ASSIGN : s_0_1 275 # ASSIGN : s_0_2 0 # ASSIGN : s_0_3 1 # ASSIGN : s_0_4 44 # ASSIGN : s_0_5 37 # ASSIGN : s_0_6 373 # ASSIGN : s_0_7 38 # ASSIGN : s_0_8 43 # ASSIGN : s_1_0 1448 # ASSIGN : s_1_1 579 # ASSIGN : s_1_2 327 # ASSIGN : s_1_3 47 # ASSIGN : s_1_4 224 # ASSIGN : s_1_5 183 # ASSIGN : s_1_6 921 # ASSIGN : s_1_7 580 # ASSIGN : s_1_8 184 # ASSIGN : s_2_0 1627 # ASSIGN : s_2_1 720 # ASSIGN : s_2_2 721 # ASSIGN : s_2_3 153 # ASSIGN : s_2_4 225 # ASSIGN : s_2_5 226 # ASSIGN : s_2_6 1038 # ASSIGN : s_2_7 1087 # ASSIGN : s_2_8 186 # ASSIGN : s_3_0 1697 # ASSIGN : s_3_1 780 # ASSIGN : s_3_2 722 # ASSIGN : s_3_3 324 # ASSIGN : s_3_4 248 # ASSIGN : s_3_5 1066 # ASSIGN : s_3_6 1042 # ASSIGN : s_3_7 1482 # ASSIGN : s_3_8 187 # ASSIGN : s_4_0 1793 # ASSIGN : s_4_1 1088 # ASSIGN : s_4_2 817 # ASSIGN : s_4_3 1262 # ASSIGN : s_4_4 352 # ASSIGN : s_4_5 1090 # ASSIGN : s_4_6 1092 # ASSIGN : s_4_7 1483 # ASSIGN : s_4_8 279 # ASSIGN : s_5_0 2211 # ASSIGN : s_5_1 1090 # ASSIGN : s_5_2 1092 # ASSIGN : s_5_3 1483 # ASSIGN : s_5_4 364 # ASSIGN : s_5_5 1091 # ASSIGN : s_5_6 1093 # ASSIGN : s_5_7 1484 # ASSIGN : s_5_8 363 # ASSIGN : s_6_0 2212 # ASSIGN : s_6_1 1099 # ASSIGN : s_6_2 1114 # ASSIGN : s_6_3 1707 # ASSIGN : s_6_4 1711 # ASSIGN : s_6_5 1379 # ASSIGN : s_6_6 1123 # ASSIGN : s_6_7 1722 # ASSIGN : s_6_8 712 # ASSIGN : s_7_0 2213 # ASSIGN : s_7_1 1214 # ASSIGN : s_7_2 1460 # ASSIGN : s_7_3 1709 # ASSIGN : s_7_4 1712 # ASSIGN : s_7_5 1708 # ASSIGN : s_7_6 1714 # ASSIGN : s_7_7 1723 # ASSIGN : s_7_8 1740 # ASSIGN : s_8_0 2214 # ASSIGN : s_8_1 1481 # ASSIGN : s_8_2 1855 # ASSIGN : s_8_3 2014 # ASSIGN : s_8_4 2318 # ASSIGN : s_8_5 2319 # ASSIGN : s_8_6 2468 # ASSIGN : s_8_7 2479 # ASSIGN : s_8_8 2480 SHOW_RESULT 2481 END : 2481 (1 seconds) [Sun Jun 18 18:00:16 2006] SHOW_RESULT 2481 CPU : 1.00999999999999 = 0.919999999999987 + 0.0900000000000001 + 0 + 0 # BOUND : makespan 1000 2481 MODIFY_CNF 1740 BEGIN : [Sun Jun 18 18:00:16 2006] MODIFY_CNF 1740 END : 132282773 bytes (0 seconds) [Sun Jun 18 18:00:16 2006] MODIFY_CNF 1740 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1740 BEGIN : [Sun Jun 18 18:00:16 2006] CMD : minisat /tmp/csp2sat11595.cnf /tmp/csp2sat11595.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 2676789 7707703 | 892263 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 9 (1 /sec) decisions : 472 (49 /sec) propagations : 432730 (45217 /sec) conflict literals : 96 (2.04 % deleted) Memory used : 218.62 MB CPU time : 9.57 s SATISFIABLE VERIFY_CNF 1740 END : (10 seconds) [Sun Jun 18 18:00:26 2006] VERIFY_CNF 1740 CPU : 10.39 = 0 + 0 + 9.74 + 0.65 # RESULT : makespan 1740 SATISFIABLE SHOW_RESULT 1740 BEGIN : [Sun Jun 18 18:00:26 2006] # ASSIGN : makespan 1740 # ASSIGN : s_0_0 932 # ASSIGN : s_0_1 1641 # ASSIGN : s_0_2 28 # ASSIGN : s_0_3 255 # ASSIGN : s_0_4 75 # ASSIGN : s_0_5 29 # ASSIGN : s_0_6 369 # ASSIGN : s_0_7 30 # ASSIGN : s_0_8 35 # ASSIGN : s_1_0 738 # ASSIGN : s_1_1 34 # ASSIGN : s_1_2 38 # ASSIGN : s_1_3 291 # ASSIGN : s_1_4 290 # ASSIGN : s_1_5 35 # ASSIGN : s_1_6 917 # ASSIGN : s_1_7 397 # ASSIGN : s_1_8 36 # ASSIGN : s_2_0 1504 # ASSIGN : s_2_1 1739 # ASSIGN : s_2_2 383 # ASSIGN : s_2_3 409 # ASSIGN : s_2_4 300 # ASSIGN : s_2_5 520 # ASSIGN : s_2_6 1034 # ASSIGN : s_2_7 1085 # ASSIGN : s_2_8 171 # ASSIGN : s_3_0 1644 # ASSIGN : s_3_1 1218 # ASSIGN : s_3_2 384 # ASSIGN : s_3_3 442 # ASSIGN : s_3_4 301 # ASSIGN : s_3_5 1014 # ASSIGN : s_3_6 1038 # ASSIGN : s_3_7 1480 # ASSIGN : s_3_8 172 # ASSIGN : s_4_0 1063 # ASSIGN : s_4_1 57 # ASSIGN : s_4_2 569 # ASSIGN : s_4_3 840 # ASSIGN : s_4_4 377 # ASSIGN : s_4_5 1061 # ASSIGN : s_4_6 1062 # ASSIGN : s_4_7 1481 # ASSIGN : s_4_8 233 # ASSIGN : s_5_0 1481 # ASSIGN : s_5_1 1123 # ASSIGN : s_5_2 1115 # ASSIGN : s_5_3 1124 # ASSIGN : s_5_4 389 # ASSIGN : s_5_5 1126 # ASSIGN : s_5_6 1426 # ASSIGN : s_5_7 1482 # ASSIGN : s_5_8 306 # ASSIGN : s_6_0 1062 # ASSIGN : s_6_1 59 # ASSIGN : s_6_2 1116 # ASSIGN : s_6_3 1125 # ASSIGN : s_6_4 1455 # ASSIGN : s_6_5 1127 # ASSIGN : s_6_6 1456 # ASSIGN : s_6_7 1720 # ASSIGN : s_6_8 307 # ASSIGN : s_7_0 1574 # ASSIGN : s_7_1 448 # ASSIGN : s_7_2 1170 # ASSIGN : s_7_3 1167 # ASSIGN : s_7_4 1575 # ASSIGN : s_7_5 1577 # ASSIGN : s_7_6 1712 # ASSIGN : s_7_7 1721 # ASSIGN : s_7_8 694 # ASSIGN : s_8_0 634 # ASSIGN : s_8_1 74 # ASSIGN : s_8_2 1418 # ASSIGN : s_8_3 1218 # ASSIGN : s_8_4 1577 # ASSIGN : s_8_5 1578 # ASSIGN : s_8_6 1727 # ASSIGN : s_8_7 1738 # ASSIGN : s_8_8 1739 SHOW_RESULT 1740 END : 1740 (2 seconds) [Sun Jun 18 18:00:28 2006] SHOW_RESULT 1740 CPU : 1.26 = 1.25 + 0.01 + 0 + 0 # BOUND : makespan 1000 1740 MODIFY_CNF 1370 BEGIN : [Sun Jun 18 18:00:28 2006] MODIFY_CNF 1370 END : 132282773 bytes (0 seconds) [Sun Jun 18 18:00:28 2006] MODIFY_CNF 1370 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1370 BEGIN : [Sun Jun 18 18:00:28 2006] CMD : minisat /tmp/csp2sat11595.cnf /tmp/csp2sat11595.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 2197269 6269143 | 732423 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 8 (1 /sec) decisions : 360 (31 /sec) propagations : 407394 (35150 /sec) conflict literals : 111 (3.48 % deleted) Memory used : 218.62 MB CPU time : 11.59 s SATISFIABLE VERIFY_CNF 1370 END : (12 seconds) [Sun Jun 18 18:00:40 2006] VERIFY_CNF 1370 CPU : 12.43 = 0 + 0.01 + 11.75 + 0.67 # RESULT : makespan 1370 SATISFIABLE SHOW_RESULT 1370 BEGIN : [Sun Jun 18 18:00:40 2006] # ASSIGN : makespan 1370 # ASSIGN : s_0_0 644 # ASSIGN : s_0_1 1256 # ASSIGN : s_0_2 4 # ASSIGN : s_0_3 588 # ASSIGN : s_0_4 1076 # ASSIGN : s_0_5 5 # ASSIGN : s_0_6 40 # ASSIGN : s_0_7 10 # ASSIGN : s_0_8 15 # ASSIGN : s_1_0 465 # ASSIGN : s_1_1 0 # ASSIGN : s_1_2 946 # ASSIGN : s_1_3 359 # ASSIGN : s_1_4 5 # ASSIGN : s_1_5 6 # ASSIGN : s_1_6 727 # ASSIGN : s_1_7 18 # ASSIGN : s_1_8 16 # ASSIGN : s_2_0 774 # ASSIGN : s_2_1 1 # ASSIGN : s_2_2 193 # ASSIGN : s_2_3 2 # ASSIGN : s_2_4 194 # ASSIGN : s_2_5 848 # ASSIGN : s_2_6 844 # ASSIGN : s_2_7 379 # ASSIGN : s_2_8 195 # ASSIGN : s_3_0 100 # ASSIGN : s_3_1 562 # ASSIGN : s_3_2 271 # ASSIGN : s_3_3 884 # ASSIGN : s_3_4 1282 # ASSIGN : s_3_5 824 # ASSIGN : s_3_6 859 # ASSIGN : s_3_7 883 # ASSIGN : s_3_8 196 # ASSIGN : s_4_0 935 # ASSIGN : s_4_1 34 # ASSIGN : s_4_2 347 # ASSIGN : s_4_3 36 # ASSIGN : s_4_4 1358 # ASSIGN : s_4_5 7 # ASSIGN : s_4_6 933 # ASSIGN : s_4_7 934 # ASSIGN : s_4_8 257 # ASSIGN : s_5_0 1353 # ASSIGN : s_5_1 1354 # ASSIGN : s_5_2 329 # ASSIGN : s_5_3 35 # ASSIGN : s_5_4 331 # ASSIGN : s_5_5 8 # ASSIGN : s_5_6 1057 # ASSIGN : s_5_7 1113 # ASSIGN : s_5_8 330 # ASSIGN : s_6_0 337 # ASSIGN : s_6_1 1355 # ASSIGN : s_6_2 338 # ASSIGN : s_6_3 477 # ASSIGN : s_6_4 8 # ASSIGN : s_6_5 9 # ASSIGN : s_6_6 1087 # ASSIGN : s_6_7 1351 # ASSIGN : s_6_8 479 # ASSIGN : s_7_0 360 # ASSIGN : s_7_1 82 # ASSIGN : s_7_2 618 # ASSIGN : s_7_3 1339 # ASSIGN : s_7_4 328 # ASSIGN : s_7_5 1342 # ASSIGN : s_7_6 1343 # ASSIGN : s_7_7 1352 # ASSIGN : s_7_8 866 # ASSIGN : s_8_0 361 # ASSIGN : s_8_1 824 # ASSIGN : s_8_2 1198 # ASSIGN : s_8_3 624 # ASSIGN : s_8_4 330 # ASSIGN : s_8_5 475 # ASSIGN : s_8_6 1357 # ASSIGN : s_8_7 1369 # ASSIGN : s_8_8 1368 SHOW_RESULT 1370 END : 1370 (1 seconds) [Sun Jun 18 18:00:41 2006] SHOW_RESULT 1370 CPU : 1.15000000000001 = 1.15000000000001 + 0 + 0 + 0 # BOUND : makespan 1000 1370 MODIFY_CNF 1185 BEGIN : [Sun Jun 18 18:00:41 2006] MODIFY_CNF 1185 END : 132282773 bytes (0 seconds) [Sun Jun 18 18:00:41 2006] MODIFY_CNF 1185 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1185 BEGIN : [Sun Jun 18 18:00:41 2006] CMD : minisat /tmp/csp2sat11595.cnf /tmp/csp2sat11595.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1957509 5549863 | 652503 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 4 (0 /sec) decisions : 327 (35 /sec) propagations : 366605 (39762 /sec) conflict literals : 16 (0.00 % deleted) Memory used : 218.62 MB CPU time : 9.22 s SATISFIABLE VERIFY_CNF 1185 END : (10 seconds) [Sun Jun 18 18:00:51 2006] VERIFY_CNF 1185 CPU : 10.03 = 0.00999999999999091 + 0 + 9.35 + 0.67 # RESULT : makespan 1185 SATISFIABLE SHOW_RESULT 1185 BEGIN : [Sun Jun 18 18:00:51 2006] # ASSIGN : makespan 1185 # ASSIGN : s_0_0 1054 # ASSIGN : s_0_1 776 # ASSIGN : s_0_2 74 # ASSIGN : s_0_3 3 # ASSIGN : s_0_4 874 # ASSIGN : s_0_5 2 # ASSIGN : s_0_6 80 # ASSIGN : s_0_7 75 # ASSIGN : s_0_8 1 # ASSIGN : s_1_0 745 # ASSIGN : s_1_1 0 # ASSIGN : s_1_2 924 # ASSIGN : s_1_3 39 # ASSIGN : s_1_4 1 # ASSIGN : s_1_5 4 # ASSIGN : s_1_6 628 # ASSIGN : s_1_7 186 # ASSIGN : s_1_8 5 # ASSIGN : s_2_0 984 # ASSIGN : s_2_1 1 # ASSIGN : s_2_2 0 # ASSIGN : s_2_3 931 # ASSIGN : s_2_4 2 # ASSIGN : s_2_5 33 # ASSIGN : s_2_6 3 # ASSIGN : s_2_7 527 # ASSIGN : s_2_8 7 # ASSIGN : s_3_0 649 # ASSIGN : s_3_1 923 # ASSIGN : s_3_2 864 # ASSIGN : s_3_3 146 # ASSIGN : s_3_4 69 # ASSIGN : s_3_5 550 # ASSIGN : s_3_6 840 # ASSIGN : s_3_7 922 # ASSIGN : s_3_8 8 # ASSIGN : s_4_0 175 # ASSIGN : s_4_1 17 # ASSIGN : s_4_2 593 # ASSIGN : s_4_3 964 # ASSIGN : s_4_4 19 # ASSIGN : s_4_5 31 # ASSIGN : s_4_6 871 # ASSIGN : s_4_7 927 # ASSIGN : s_4_8 71 # ASSIGN : s_5_0 1184 # ASSIGN : s_5_1 31 # ASSIGN : s_5_2 923 # ASSIGN : s_5_3 145 # ASSIGN : s_5_4 146 # ASSIGN : s_5_5 32 # ASSIGN : s_5_6 872 # ASSIGN : s_5_7 928 # ASSIGN : s_5_8 144 # ASSIGN : s_6_0 33 # ASSIGN : s_6_1 37 # ASSIGN : s_6_2 1176 # ASSIGN : s_6_3 544 # ASSIGN : s_6_4 145 # ASSIGN : s_6_5 574 # ASSIGN : s_6_6 902 # ASSIGN : s_6_7 1166 # ASSIGN : s_6_8 157 # ASSIGN : s_7_0 34 # ASSIGN : s_7_1 52 # ASSIGN : s_7_2 298 # ASSIGN : s_7_3 546 # ASSIGN : s_7_4 1156 # ASSIGN : s_7_5 1022 # ASSIGN : s_7_6 1158 # ASSIGN : s_7_7 1167 # ASSIGN : s_7_8 549 # ASSIGN : s_8_0 35 # ASSIGN : s_8_1 357 # ASSIGN : s_8_2 139 # ASSIGN : s_8_3 731 # ASSIGN : s_8_4 1183 # ASSIGN : s_8_5 1023 # ASSIGN : s_8_6 1172 # ASSIGN : s_8_7 1184 # ASSIGN : s_8_8 1022 SHOW_RESULT 1185 END : 1185 (1 seconds) [Sun Jun 18 18:00:52 2006] SHOW_RESULT 1185 CPU : 1.14 = 1.13 + 0.01 + 0 + 0 # BOUND : makespan 1000 1185 MODIFY_CNF 1092 BEGIN : [Sun Jun 18 18:00:52 2006] MODIFY_CNF 1092 END : 132282772 bytes (0 seconds) [Sun Jun 18 18:00:52 2006] MODIFY_CNF 1092 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1092 BEGIN : [Sun Jun 18 18:00:52 2006] CMD : minisat /tmp/csp2sat11595.cnf /tmp/csp2sat11595.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1836981 5188279 | 612327 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (0 /sec) decisions : 210 (21 /sec) propagations : 345002 (35276 /sec) conflict literals : 6 (0.00 % deleted) Memory used : 218.62 MB CPU time : 9.78 s SATISFIABLE VERIFY_CNF 1092 END : (11 seconds) [Sun Jun 18 18:01:03 2006] VERIFY_CNF 1092 CPU : 10.64 = 0 + 0 + 9.93 + 0.71 # RESULT : makespan 1092 SATISFIABLE SHOW_RESULT 1092 BEGIN : [Sun Jun 18 18:01:03 2006] # ASSIGN : makespan 1092 # ASSIGN : s_0_0 842 # ASSIGN : s_0_1 993 # ASSIGN : s_0_2 8 # ASSIGN : s_0_3 14 # ASSIGN : s_0_4 108 # ASSIGN : s_0_5 0 # ASSIGN : s_0_6 288 # ASSIGN : s_0_7 2 # ASSIGN : s_0_8 1 # ASSIGN : s_1_0 661 # ASSIGN : s_1_1 2 # ASSIGN : s_1_2 840 # ASSIGN : s_1_3 53 # ASSIGN : s_1_4 318 # ASSIGN : s_1_5 4 # ASSIGN : s_1_6 171 # ASSIGN : s_1_7 320 # ASSIGN : s_1_8 5 # ASSIGN : s_2_0 591 # ASSIGN : s_2_1 1091 # ASSIGN : s_2_2 9 # ASSIGN : s_2_3 558 # ASSIGN : s_2_4 1090 # ASSIGN : s_2_5 14 # ASSIGN : s_2_6 2 # ASSIGN : s_2_7 695 # ASSIGN : s_2_8 7 # ASSIGN : s_3_0 972 # ASSIGN : s_3_1 710 # ASSIGN : s_3_2 77 # ASSIGN : s_3_3 159 # ASSIGN : s_3_4 1 # ASSIGN : s_3_5 1068 # ASSIGN : s_3_6 135 # ASSIGN : s_3_7 0 # ASSIGN : s_3_8 557 # ASSIGN : s_4_0 151 # ASSIGN : s_4_1 3 # ASSIGN : s_4_2 569 # ASSIGN : s_4_3 871 # ASSIGN : s_4_4 95 # ASSIGN : s_4_5 5 # ASSIGN : s_4_6 6 # ASSIGN : s_4_7 7 # ASSIGN : s_4_8 8 # ASSIGN : s_5_0 1091 # ASSIGN : s_5_1 9 # ASSIGN : s_5_2 10 # ASSIGN : s_5_3 50 # ASSIGN : s_5_4 364 # ASSIGN : s_5_5 11 # ASSIGN : s_5_6 12 # ASSIGN : s_5_7 82 # ASSIGN : s_5_8 81 # ASSIGN : s_6_0 11 # ASSIGN : s_6_1 36 # ASSIGN : s_6_2 15 # ASSIGN : s_6_3 51 # ASSIGN : s_6_4 107 # ASSIGN : s_6_5 508 # ASSIGN : s_6_6 836 # ASSIGN : s_6_7 24 # ASSIGN : s_6_8 121 # ASSIGN : s_7_0 12 # ASSIGN : s_7_1 51 # ASSIGN : s_7_2 321 # ASSIGN : s_7_3 615 # ASSIGN : s_7_4 319 # ASSIGN : s_7_5 13 # ASSIGN : s_7_6 42 # ASSIGN : s_7_7 25 # ASSIGN : s_7_8 618 # ASSIGN : s_8_0 20 # ASSIGN : s_8_1 297 # ASSIGN : s_8_2 138 # ASSIGN : s_8_3 671 # ASSIGN : s_8_4 0 # ASSIGN : s_8_5 919 # ASSIGN : s_8_6 124 # ASSIGN : s_8_7 1090 # ASSIGN : s_8_8 1091 SHOW_RESULT 1092 END : 1092 (1 seconds) [Sun Jun 18 18:01:04 2006] SHOW_RESULT 1092 CPU : 1.12000000000002 = 1.10000000000002 + 0.02 + 0 + 0 # BOUND : makespan 1000 1092 MODIFY_CNF 1046 BEGIN : [Sun Jun 18 18:01:04 2006] MODIFY_CNF 1046 END : 132282772 bytes (0 seconds) [Sun Jun 18 18:01:04 2006] MODIFY_CNF 1046 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1046 BEGIN : [Sun Jun 18 18:01:04 2006] CMD : minisat /tmp/csp2sat11595.cnf /tmp/csp2sat11595.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1777365 5009431 | 592455 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (0 /sec) decisions : 3 (0 /sec) propagations : 252711 (25578 /sec) conflict literals : 1 (0.00 % deleted) Memory used : 217.10 MB CPU time : 9.88 s UNSATISFIABLE VERIFY_CNF 1046 END : (11 seconds) [Sun Jun 18 18:01:15 2006] VERIFY_CNF 1046 CPU : 10.55 = 0 + 0.00999999999999979 + 9.88 + 0.66 # RESULT : makespan 1046 UNSATISFIABLE # BOUND : makespan 1047 1092 MODIFY_CNF 1069 BEGIN : [Sun Jun 18 18:01:15 2006] MODIFY_CNF 1069 END : 132282772 bytes (0 seconds) [Sun Jun 18 18:01:15 2006] MODIFY_CNF 1069 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1069 BEGIN : [Sun Jun 18 18:01:15 2006] CMD : minisat /tmp/csp2sat11595.cnf /tmp/csp2sat11595.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1807173 5098855 | 602391 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (0 /sec) decisions : 3 (0 /sec) propagations : 250822 (25699 /sec) conflict literals : 1 (0.00 % deleted) Memory used : 217.09 MB CPU time : 9.76 s UNSATISFIABLE VERIFY_CNF 1069 END : (10 seconds) [Sun Jun 18 18:01:25 2006] VERIFY_CNF 1069 CPU : 10.44 = 0 + 0 + 9.76 + 0.68 # RESULT : makespan 1069 UNSATISFIABLE # BOUND : makespan 1070 1092 MODIFY_CNF 1081 BEGIN : [Sun Jun 18 18:01:25 2006] MODIFY_CNF 1081 END : 132282772 bytes (0 seconds) [Sun Jun 18 18:01:25 2006] MODIFY_CNF 1081 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1081 BEGIN : [Sun Jun 18 18:01:25 2006] CMD : minisat /tmp/csp2sat11595.cnf /tmp/csp2sat11595.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1822725 5145511 | 607575 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (0 /sec) decisions : 3 (0 /sec) propagations : 260042 (23945 /sec) conflict literals : 1 (0.00 % deleted) Memory used : 217.12 MB CPU time : 10.86 s UNSATISFIABLE VERIFY_CNF 1081 END : (12 seconds) [Sun Jun 18 18:01:37 2006] VERIFY_CNF 1081 CPU : 11.42 = 0 + 0 + 10.86 + 0.56 # RESULT : makespan 1081 UNSATISFIABLE # BOUND : makespan 1082 1092 MODIFY_CNF 1087 BEGIN : [Sun Jun 18 18:01:37 2006] MODIFY_CNF 1087 END : 132282772 bytes (0 seconds) [Sun Jun 18 18:01:37 2006] MODIFY_CNF 1087 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1087 BEGIN : [Sun Jun 18 18:01:37 2006] CMD : minisat /tmp/csp2sat11595.cnf /tmp/csp2sat11595.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1830501 5168839 | 610167 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 17 (2 /sec) decisions : 25 (2 /sec) propagations : 411196 (38610 /sec) conflict literals : 175 (29.72 % deleted) Memory used : 217.21 MB CPU time : 10.65 s UNSATISFIABLE VERIFY_CNF 1087 END : (11 seconds) [Sun Jun 18 18:01:48 2006] VERIFY_CNF 1087 CPU : 11.45 = 0 + 0 + 10.65 + 0.8 # RESULT : makespan 1087 UNSATISFIABLE # BOUND : makespan 1088 1092 MODIFY_CNF 1090 BEGIN : [Sun Jun 18 18:01:48 2006] MODIFY_CNF 1090 END : 132282772 bytes (0 seconds) [Sun Jun 18 18:01:48 2006] MODIFY_CNF 1090 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1090 BEGIN : [Sun Jun 18 18:01:48 2006] CMD : minisat /tmp/csp2sat11595.cnf /tmp/csp2sat11595.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1834389 5180503 | 611463 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 30 (3 /sec) decisions : 148 (15 /sec) propagations : 522344 (51820 /sec) conflict literals : 512 (29.86 % deleted) Memory used : 218.62 MB CPU time : 10.08 s SATISFIABLE VERIFY_CNF 1090 END : (11 seconds) [Sun Jun 18 18:01:59 2006] VERIFY_CNF 1090 CPU : 10.83 = 0 + 0 + 10.25 + 0.58 # RESULT : makespan 1090 SATISFIABLE SHOW_RESULT 1090 BEGIN : [Sun Jun 18 18:01:59 2006] # ASSIGN : makespan 1090 # ASSIGN : s_0_0 137 # ASSIGN : s_0_1 39 # ASSIGN : s_0_2 1050 # ASSIGN : s_0_3 1051 # ASSIGN : s_0_4 821 # ASSIGN : s_0_5 38 # ASSIGN : s_0_6 267 # ASSIGN : s_0_7 816 # ASSIGN : s_0_8 1012 # ASSIGN : s_1_0 294 # ASSIGN : s_1_1 1085 # ASSIGN : s_1_2 26 # ASSIGN : s_1_3 945 # ASSIGN : s_1_4 814 # ASSIGN : s_1_5 1088 # ASSIGN : s_1_6 815 # ASSIGN : s_1_7 473 # ASSIGN : s_1_8 1086 # ASSIGN : s_2_0 498 # ASSIGN : s_2_1 1089 # ASSIGN : s_2_2 24 # ASSIGN : s_2_3 465 # ASSIGN : s_2_4 26 # ASSIGN : s_2_5 594 # ASSIGN : s_2_6 6 # ASSIGN : s_2_7 27 # ASSIGN : s_2_8 1088 # ASSIGN : s_3_0 41 # ASSIGN : s_3_1 161 # ASSIGN : s_3_2 956 # ASSIGN : s_3_3 534 # ASSIGN : s_3_4 1014 # ASSIGN : s_3_5 14 # ASSIGN : s_3_6 932 # ASSIGN : s_3_7 472 # ASSIGN : s_3_8 473 # ASSIGN : s_4_0 568 # ASSIGN : s_4_1 1087 # ASSIGN : s_4_2 278 # ASSIGN : s_4_3 1 # ASSIGN : s_4_4 1001 # ASSIGN : s_4_5 265 # ASSIGN : s_4_6 1089 # ASSIGN : s_4_7 0 # ASSIGN : s_4_8 1013 # ASSIGN : s_5_0 40 # ASSIGN : s_5_1 803 # ASSIGN : s_5_2 25 # ASSIGN : s_5_3 0 # ASSIGN : s_5_4 76 # ASSIGN : s_5_5 72 # ASSIGN : s_5_6 1059 # ASSIGN : s_5_7 821 # ASSIGN : s_5_8 1089 # ASSIGN : s_6_0 9 # ASSIGN : s_6_1 1063 # ASSIGN : s_6_2 1078 # ASSIGN : s_6_3 1087 # ASSIGN : s_6_4 1013 # ASSIGN : s_6_5 266 # ASSIGN : s_6_6 10 # ASSIGN : s_6_7 1089 # ASSIGN : s_6_8 598 # ASSIGN : s_7_0 497 # ASSIGN : s_7_1 804 # ASSIGN : s_7_2 549 # ASSIGN : s_7_3 531 # ASSIGN : s_7_4 802 # ASSIGN : s_7_5 1089 # ASSIGN : s_7_6 1050 # ASSIGN : s_7_7 1072 # ASSIGN : s_7_8 0 # ASSIGN : s_8_0 986 # ASSIGN : s_8_1 423 # ASSIGN : s_8_2 797 # ASSIGN : s_8_3 222 # ASSIGN : s_8_4 72 # ASSIGN : s_8_5 73 # ASSIGN : s_8_6 974 # ASSIGN : s_8_7 422 # ASSIGN : s_8_8 985 SHOW_RESULT 1090 END : 1090 (1 seconds) [Sun Jun 18 18:02:00 2006] SHOW_RESULT 1090 CPU : 1.14 = 1.13 + 0.01 + 0 + 0 # BOUND : makespan 1088 1090 MODIFY_CNF 1089 BEGIN : [Sun Jun 18 18:02:00 2006] MODIFY_CNF 1089 END : 132282772 bytes (0 seconds) [Sun Jun 18 18:02:00 2006] MODIFY_CNF 1089 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1089 BEGIN : [Sun Jun 18 18:02:00 2006] CMD : minisat /tmp/csp2sat11595.cnf /tmp/csp2sat11595.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1833093 5176615 | 611031 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 43 (4 /sec) decisions : 65 (6 /sec) propagations : 591151 (58821 /sec) conflict literals : 541 (33.70 % deleted) Memory used : 217.21 MB CPU time : 10.05 s UNSATISFIABLE VERIFY_CNF 1089 END : (11 seconds) [Sun Jun 18 18:02:11 2006] VERIFY_CNF 1089 CPU : 10.63 = 0 + 0 + 10.05 + 0.58 # RESULT : makespan 1089 UNSATISFIABLE # BOUND : makespan 1090 1090 MAIN END : (341 seconds) [Sun Jun 18 18:02:11 2006] MAIN CPU : 339.43 = 220.48 + 1.13 + 110.69 + 7.13