# TIMEOUT 18000 MAIN BEGIN : [Sun Jun 18 17:00:30 2006] READ BEGIN : csp/gp08-05.csp [Sun Jun 18 17:00:30 2006] READ END : csp/gp08-05.csp (1 seconds) [Sun Jun 18 17:00:31 2006] READ CPU : 1 = 1 + 0 + 0 + 0 # BOUND : makespan 1000 3996 GENERATE_CNF 3996 BEGIN : [Sun Jun 18 17:00:31 2006] GENERATE_CNF 3996 END : 259830 variables 3921463 clauses 92383807 bytes (158 seconds) [Sun Jun 18 17:03:09 2006] GENERATE_CNF 3996 CPU : 157.52 = 156.96 + 0.56 + 0 + 0 MODIFY_CNF 2498 BEGIN : [Sun Jun 18 17:03:09 2006] MODIFY_CNF 2498 END : 92383814 bytes (0 seconds) [Sun Jun 18 17:03:09 2006] MODIFY_CNF 2498 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 2498 BEGIN : [Sun Jun 18 17:03:09 2006] CMD : minisat /tmp/csp2sat10588.cnf /tmp/csp2sat10588.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 2577906 7475944 | 859302 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 379 (69 /sec) propagations : 259830 (46986 /sec) conflict literals : 0 ( nan % deleted) Memory used : 161.91 MB CPU time : 5.53 s SATISFIABLE VERIFY_CNF 2498 END : (6 seconds) [Sun Jun 18 17:03:15 2006] VERIFY_CNF 2498 CPU : 6.12 = 0 + 0.0099999999999999 + 5.66 + 0.45 # RESULT : makespan 2498 SATISFIABLE SHOW_RESULT 2498 BEGIN : [Sun Jun 18 17:03:15 2006] # ASSIGN : makespan 2498 # ASSIGN : s_0_0 17 # ASSIGN : s_0_1 18 # ASSIGN : s_0_2 19 # ASSIGN : s_0_3 223 # ASSIGN : s_0_4 204 # ASSIGN : s_0_5 845 # ASSIGN : s_0_6 846 # ASSIGN : s_0_7 1498 # ASSIGN : s_1_0 37 # ASSIGN : s_1_1 25 # ASSIGN : s_1_2 26 # ASSIGN : s_1_3 825 # ASSIGN : s_1_4 502 # ASSIGN : s_1_5 959 # ASSIGN : s_1_6 966 # ASSIGN : s_1_7 1747 # ASSIGN : s_2_0 486 # ASSIGN : s_2_1 130 # ASSIGN : s_2_2 232 # ASSIGN : s_2_3 855 # ASSIGN : s_2_4 503 # ASSIGN : s_2_5 1222 # ASSIGN : s_2_6 1465 # ASSIGN : s_2_7 1749 # ASSIGN : s_3_0 722 # ASSIGN : s_3_1 159 # ASSIGN : s_3_2 855 # ASSIGN : s_3_3 856 # ASSIGN : s_3_4 857 # ASSIGN : s_3_5 1480 # ASSIGN : s_3_6 1481 # ASSIGN : s_3_7 1837 # ASSIGN : s_4_0 723 # ASSIGN : s_4_1 175 # ASSIGN : s_4_2 901 # ASSIGN : s_4_3 2257 # ASSIGN : s_4_4 1745 # ASSIGN : s_4_5 1747 # ASSIGN : s_4_6 1837 # ASSIGN : s_4_7 1838 # ASSIGN : s_5_0 887 # ASSIGN : s_5_1 638 # ASSIGN : s_5_2 902 # ASSIGN : s_5_3 1626 # ASSIGN : s_5_4 1749 # ASSIGN : s_5_5 1750 # ASSIGN : s_5_6 1958 # ASSIGN : s_5_7 1963 # ASSIGN : s_6_0 1161 # ASSIGN : s_6_1 1386 # ASSIGN : s_6_2 1626 # ASSIGN : s_6_3 1627 # ASSIGN : s_6_4 1750 # ASSIGN : s_6_5 1751 # ASSIGN : s_6_6 1966 # ASSIGN : s_6_7 1967 # ASSIGN : s_7_0 1498 # ASSIGN : s_7_1 1626 # ASSIGN : s_7_2 1627 # ASSIGN : s_7_3 1628 # ASSIGN : s_7_4 1751 # ASSIGN : s_7_5 1752 # ASSIGN : s_7_6 2495 # ASSIGN : s_7_7 2497 SHOW_RESULT 2498 END : 2498 (1 seconds) [Sun Jun 18 17:03:16 2006] SHOW_RESULT 2498 CPU : 0.559999999999982 = 0.519999999999982 + 0.04 + 0 + 0 # BOUND : makespan 1000 2498 MODIFY_CNF 1749 BEGIN : [Sun Jun 18 17:03:16 2006] MODIFY_CNF 1749 END : 92383813 bytes (0 seconds) [Sun Jun 18 17:03:16 2006] MODIFY_CNF 1749 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1749 BEGIN : [Sun Jun 18 17:03:16 2006] CMD : minisat /tmp/csp2sat10588.cnf /tmp/csp2sat10588.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1906802 5462632 | 635600 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 13 (2 /sec) decisions : 389 (61 /sec) propagations : 420569 (66441 /sec) conflict literals : 201 (2.90 % deleted) Memory used : 161.91 MB CPU time : 6.33 s SATISFIABLE VERIFY_CNF 1749 END : (7 seconds) [Sun Jun 18 17:03:23 2006] VERIFY_CNF 1749 CPU : 6.9 = 0 + 0 + 6.47 + 0.43 # RESULT : makespan 1749 SATISFIABLE SHOW_RESULT 1749 BEGIN : [Sun Jun 18 17:03:23 2006] # ASSIGN : makespan 1749 # ASSIGN : s_0_0 16 # ASSIGN : s_0_1 17 # ASSIGN : s_0_2 19 # ASSIGN : s_0_3 474 # ASSIGN : s_0_4 206 # ASSIGN : s_0_5 18 # ASSIGN : s_0_6 26 # ASSIGN : s_0_7 225 # ASSIGN : s_1_0 1118 # ASSIGN : s_1_1 16 # ASSIGN : s_1_2 128 # ASSIGN : s_1_3 1076 # ASSIGN : s_1_4 753 # ASSIGN : s_1_5 139 # ASSIGN : s_1_6 146 # ASSIGN : s_1_7 645 # ASSIGN : s_2_0 1732 # ASSIGN : s_2_1 108 # ASSIGN : s_2_2 393 # ASSIGN : s_2_3 1106 # ASSIGN : s_2_4 754 # ASSIGN : s_2_5 150 # ASSIGN : s_2_6 735 # ASSIGN : s_2_7 647 # ASSIGN : s_3_0 1731 # ASSIGN : s_3_1 1733 # ASSIGN : s_3_2 748 # ASSIGN : s_3_3 1107 # ASSIGN : s_3_4 1108 # ASSIGN : s_3_5 749 # ASSIGN : s_3_6 751 # ASSIGN : s_3_7 750 # ASSIGN : s_4_0 1567 # ASSIGN : s_4_1 137 # ASSIGN : s_4_2 896 # ASSIGN : s_4_3 1326 # ASSIGN : s_4_4 1744 # ASSIGN : s_4_5 750 # ASSIGN : s_4_6 1739 # ASSIGN : s_4_7 753 # ASSIGN : s_5_0 882 # ASSIGN : s_5_1 600 # ASSIGN : s_5_2 897 # ASSIGN : s_5_3 1621 # ASSIGN : s_5_4 1746 # ASSIGN : s_5_5 849 # ASSIGN : s_5_6 1740 # ASSIGN : s_5_7 878 # ASSIGN : s_6_0 625 # ASSIGN : s_6_1 851 # ASSIGN : s_6_2 1621 # ASSIGN : s_6_3 1622 # ASSIGN : s_6_4 1747 # ASSIGN : s_6_5 850 # ASSIGN : s_6_6 1745 # ASSIGN : s_6_7 1091 # ASSIGN : s_7_0 497 # ASSIGN : s_7_1 1620 # ASSIGN : s_7_2 1622 # ASSIGN : s_7_3 1623 # ASSIGN : s_7_4 1748 # ASSIGN : s_7_5 877 # ASSIGN : s_7_6 1746 # ASSIGN : s_7_7 1621 SHOW_RESULT 1749 END : 1749 (1 seconds) [Sun Jun 18 17:03:24 2006] SHOW_RESULT 1749 CPU : 1.04 = 1.03 + 0.01 + 0 + 0 # BOUND : makespan 1000 1749 MODIFY_CNF 1374 BEGIN : [Sun Jun 18 17:03:24 2006] MODIFY_CNF 1374 END : 92383813 bytes (0 seconds) [Sun Jun 18 17:03:24 2006] MODIFY_CNF 1374 CPU : 0.00999999999999091 = 0.00999999999999091 + 0 + 0 + 0 VERIFY_CNF 1374 BEGIN : [Sun Jun 18 17:03:24 2006] CMD : minisat /tmp/csp2sat10588.cnf /tmp/csp2sat10588.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1570802 4454632 | 523600 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 8 (1 /sec) decisions : 304 (45 /sec) propagations : 289609 (42842 /sec) conflict literals : 41 (2.38 % deleted) Memory used : 161.91 MB CPU time : 6.76 s SATISFIABLE VERIFY_CNF 1374 END : (7 seconds) [Sun Jun 18 17:03:31 2006] VERIFY_CNF 1374 CPU : 7.39 = 0 + 0 + 6.88 + 0.51 # RESULT : makespan 1374 SATISFIABLE SHOW_RESULT 1374 BEGIN : [Sun Jun 18 17:03:31 2006] # ASSIGN : makespan 1374 # ASSIGN : s_0_0 5 # ASSIGN : s_0_1 631 # ASSIGN : s_0_2 632 # ASSIGN : s_0_3 644 # ASSIGN : s_0_4 6 # ASSIGN : s_0_5 25 # ASSIGN : s_0_6 275 # ASSIGN : s_0_7 26 # ASSIGN : s_1_0 925 # ASSIGN : s_1_1 894 # ASSIGN : s_1_2 277 # ASSIGN : s_1_3 9 # ASSIGN : s_1_4 39 # ASSIGN : s_1_5 40 # ASSIGN : s_1_6 395 # ASSIGN : s_1_7 288 # ASSIGN : s_2_0 29 # ASSIGN : s_2_1 865 # ASSIGN : s_2_2 378 # ASSIGN : s_2_3 46 # ASSIGN : s_2_4 1010 # ASSIGN : s_2_5 47 # ASSIGN : s_2_6 986 # ASSIGN : s_2_7 290 # ASSIGN : s_3_0 242 # ASSIGN : s_3_1 1358 # ASSIGN : s_3_2 243 # ASSIGN : s_3_3 244 # ASSIGN : s_3_4 379 # ASSIGN : s_3_5 377 # ASSIGN : s_3_6 1002 # ASSIGN : s_3_7 378 # ASSIGN : s_4_0 731 # ASSIGN : s_4_1 895 # ASSIGN : s_4_2 639 # ASSIGN : s_4_3 245 # ASSIGN : s_4_4 1362 # ASSIGN : s_4_5 486 # ASSIGN : s_4_6 1364 # ASSIGN : s_4_7 511 # ASSIGN : s_5_0 225 # ASSIGN : s_5_1 240 # ASSIGN : s_5_2 640 # ASSIGN : s_5_3 635 # ASSIGN : s_5_4 1364 # ASSIGN : s_5_5 489 # ASSIGN : s_5_6 1365 # ASSIGN : s_5_7 636 # ASSIGN : s_6_0 491 # ASSIGN : s_6_1 0 # ASSIGN : s_6_2 1368 # ASSIGN : s_6_3 1246 # ASSIGN : s_6_4 1369 # ASSIGN : s_6_5 490 # ASSIGN : s_6_6 1370 # ASSIGN : s_6_7 716 # ASSIGN : s_7_0 363 # ASSIGN : s_7_1 502 # ASSIGN : s_7_2 1370 # ASSIGN : s_7_3 1247 # ASSIGN : s_7_4 1373 # ASSIGN : s_7_5 503 # ASSIGN : s_7_6 1371 # ASSIGN : s_7_7 1246 SHOW_RESULT 1374 END : 1374 (1 seconds) [Sun Jun 18 17:03:32 2006] SHOW_RESULT 1374 CPU : 1.00000000000002 = 0.980000000000018 + 0.02 + 0 + 0 # BOUND : makespan 1000 1374 MODIFY_CNF 1187 BEGIN : [Sun Jun 18 17:03:32 2006] MODIFY_CNF 1187 END : 92383813 bytes (0 seconds) [Sun Jun 18 17:03:32 2006] MODIFY_CNF 1187 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1187 BEGIN : [Sun Jun 18 17:03:32 2006] CMD : minisat /tmp/csp2sat10588.cnf /tmp/csp2sat10588.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1403250 3951976 | 467750 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 3 (1 /sec) decisions : 15 (3 /sec) propagations : 201122 (33859 /sec) conflict literals : 4 (20.00 % deleted) Memory used : 160.69 MB CPU time : 5.94 s UNSATISFIABLE VERIFY_CNF 1187 END : (7 seconds) [Sun Jun 18 17:03:39 2006] VERIFY_CNF 1187 CPU : 6.33 = 0 + 0 + 5.94 + 0.39 # RESULT : makespan 1187 UNSATISFIABLE # BOUND : makespan 1188 1374 MODIFY_CNF 1281 BEGIN : [Sun Jun 18 17:03:39 2006] MODIFY_CNF 1281 END : 92383813 bytes (0 seconds) [Sun Jun 18 17:03:39 2006] MODIFY_CNF 1281 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1281 BEGIN : [Sun Jun 18 17:03:39 2006] CMD : minisat /tmp/csp2sat10588.cnf /tmp/csp2sat10588.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1487474 4204648 | 495824 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 1 (0 /sec) decisions : 161 (23 /sec) propagations : 268268 (38600 /sec) conflict literals : 10 (9.09 % deleted) Memory used : 161.91 MB CPU time : 6.95 s SATISFIABLE VERIFY_CNF 1281 END : (7 seconds) [Sun Jun 18 17:03:46 2006] VERIFY_CNF 1281 CPU : 7.61 = 0 + 0 + 7.08 + 0.53 # RESULT : makespan 1281 SATISFIABLE SHOW_RESULT 1281 BEGIN : [Sun Jun 18 17:03:46 2006] # ASSIGN : makespan 1281 # ASSIGN : s_0_0 48 # ASSIGN : s_0_1 49 # ASSIGN : s_0_2 1 # ASSIGN : s_0_3 553 # ASSIGN : s_0_4 414 # ASSIGN : s_0_5 0 # ASSIGN : s_0_6 433 # ASSIGN : s_0_7 50 # ASSIGN : s_1_0 301 # ASSIGN : s_1_1 57 # ASSIGN : s_1_2 8 # ASSIGN : s_1_3 170 # ASSIGN : s_1_4 1275 # ASSIGN : s_1_5 1 # ASSIGN : s_1_6 765 # ASSIGN : s_1_7 299 # ASSIGN : s_2_0 750 # ASSIGN : s_2_1 522 # ASSIGN : s_2_2 767 # ASSIGN : s_2_3 551 # ASSIGN : s_2_4 0 # ASSIGN : s_2_5 1021 # ASSIGN : s_2_6 1264 # ASSIGN : s_2_7 352 # ASSIGN : s_3_0 2 # ASSIGN : s_3_1 58 # ASSIGN : s_3_2 0 # ASSIGN : s_3_3 14 # ASSIGN : s_3_4 652 # ASSIGN : s_3_5 15 # ASSIGN : s_3_6 77 # ASSIGN : s_3_7 440 # ASSIGN : s_4_0 1112 # ASSIGN : s_4_1 566 # ASSIGN : s_4_2 19 # ASSIGN : s_4_3 200 # ASSIGN : s_4_4 1276 # ASSIGN : s_4_5 16 # ASSIGN : s_4_6 1280 # ASSIGN : s_4_7 441 # ASSIGN : s_5_0 3 # ASSIGN : s_5_1 1029 # ASSIGN : s_5_2 20 # ASSIGN : s_5_3 18 # ASSIGN : s_5_4 1278 # ASSIGN : s_5_5 19 # ASSIGN : s_5_6 760 # ASSIGN : s_5_7 744 # ASSIGN : s_6_0 57 # ASSIGN : s_6_1 282 # ASSIGN : s_6_2 1278 # ASSIGN : s_6_3 552 # ASSIGN : s_6_4 1279 # ASSIGN : s_6_5 56 # ASSIGN : s_6_6 747 # ASSIGN : s_6_7 748 # ASSIGN : s_7_0 984 # ASSIGN : s_7_1 74 # ASSIGN : s_7_2 1279 # ASSIGN : s_7_3 1155 # ASSIGN : s_7_4 1280 # ASSIGN : s_7_5 241 # ASSIGN : s_7_6 75 # ASSIGN : s_7_7 1278 SHOW_RESULT 1281 END : 1281 (1 seconds) [Sun Jun 18 17:03:47 2006] SHOW_RESULT 1281 CPU : 1.01000000000002 = 1.01000000000002 + 0 + 0 + 0 # BOUND : makespan 1188 1281 MODIFY_CNF 1234 BEGIN : [Sun Jun 18 17:03:47 2006] MODIFY_CNF 1234 END : 92383813 bytes (0 seconds) [Sun Jun 18 17:03:47 2006] MODIFY_CNF 1234 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1234 BEGIN : [Sun Jun 18 17:03:47 2006] CMD : minisat /tmp/csp2sat10588.cnf /tmp/csp2sat10588.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1445362 4078312 | 481787 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 3 (1 /sec) decisions : 196 (33 /sec) propagations : 272109 (46042 /sec) conflict literals : 12 (0.00 % deleted) Memory used : 161.91 MB CPU time : 5.91 s SATISFIABLE VERIFY_CNF 1234 END : (7 seconds) [Sun Jun 18 17:03:54 2006] VERIFY_CNF 1234 CPU : 6.64 = 0 + 0 + 6.04 + 0.6 # RESULT : makespan 1234 SATISFIABLE SHOW_RESULT 1234 BEGIN : [Sun Jun 18 17:03:54 2006] # ASSIGN : makespan 1234 # ASSIGN : s_0_0 0 # ASSIGN : s_0_1 1 # ASSIGN : s_0_2 6 # ASSIGN : s_0_3 493 # ASSIGN : s_0_4 1095 # ASSIGN : s_0_5 13 # ASSIGN : s_0_6 1114 # ASSIGN : s_0_7 44 # ASSIGN : s_1_0 782 # ASSIGN : s_1_1 2 # ASSIGN : s_1_2 20 # ASSIGN : s_1_3 31 # ASSIGN : s_1_4 12 # ASSIGN : s_1_5 61 # ASSIGN : s_1_6 77 # ASSIGN : s_1_7 1231 # ASSIGN : s_2_0 6 # ASSIGN : s_2_1 610 # ASSIGN : s_2_2 39 # ASSIGN : s_2_3 5 # ASSIGN : s_2_4 639 # ASSIGN : s_2_5 991 # ASSIGN : s_2_6 23 # ASSIGN : s_2_7 293 # ASSIGN : s_3_0 5 # ASSIGN : s_3_1 734 # ASSIGN : s_3_2 0 # ASSIGN : s_3_3 13 # ASSIGN : s_3_4 16 # ASSIGN : s_3_5 14 # ASSIGN : s_3_6 750 # ASSIGN : s_3_7 15 # ASSIGN : s_4_0 604 # ASSIGN : s_4_1 768 # ASSIGN : s_4_2 1 # ASSIGN : s_4_3 140 # ASSIGN : s_4_4 13 # ASSIGN : s_4_5 68 # ASSIGN : s_4_6 71 # ASSIGN : s_4_7 381 # ASSIGN : s_5_0 56 # ASSIGN : s_5_1 243 # ASSIGN : s_5_2 510 # ASSIGN : s_5_3 492 # ASSIGN : s_5_4 15 # ASSIGN : s_5_5 71 # ASSIGN : s_5_6 72 # ASSIGN : s_5_7 506 # ASSIGN : s_6_0 351 # ASSIGN : s_6_1 3 # ASSIGN : s_6_2 2 # ASSIGN : s_6_3 1107 # ASSIGN : s_6_4 1231 # ASSIGN : s_6_5 247 # ASSIGN : s_6_6 576 # ASSIGN : s_6_7 577 # ASSIGN : s_7_0 120 # ASSIGN : s_7_1 1231 # ASSIGN : s_7_2 38 # ASSIGN : s_7_3 1108 # ASSIGN : s_7_4 1232 # ASSIGN : s_7_5 248 # ASSIGN : s_7_6 1106 # ASSIGN : s_7_7 1233 SHOW_RESULT 1234 END : 1234 (1 seconds) [Sun Jun 18 17:03:55 2006] SHOW_RESULT 1234 CPU : 0.989999999999999 = 0.969999999999999 + 0.02 + 0 + 0 # BOUND : makespan 1188 1234 MODIFY_CNF 1211 BEGIN : [Sun Jun 18 17:03:55 2006] MODIFY_CNF 1211 END : 92383813 bytes (0 seconds) [Sun Jun 18 17:03:55 2006] MODIFY_CNF 1211 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1211 BEGIN : [Sun Jun 18 17:03:55 2006] CMD : minisat /tmp/csp2sat10588.cnf /tmp/csp2sat10588.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1424754 4016488 | 474918 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (0 /sec) decisions : 24 (4 /sec) propagations : 200790 (34679 /sec) conflict literals : 1 (0.00 % deleted) Memory used : 160.69 MB CPU time : 5.79 s UNSATISFIABLE VERIFY_CNF 1211 END : (6 seconds) [Sun Jun 18 17:04:01 2006] VERIFY_CNF 1211 CPU : 6.3 = 0 + 0 + 5.79 + 0.51 # RESULT : makespan 1211 UNSATISFIABLE # BOUND : makespan 1212 1234 MODIFY_CNF 1223 BEGIN : [Sun Jun 18 17:04:01 2006] MODIFY_CNF 1223 END : 92383813 bytes (0 seconds) [Sun Jun 18 17:04:01 2006] MODIFY_CNF 1223 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1223 BEGIN : [Sun Jun 18 17:04:01 2006] CMD : minisat /tmp/csp2sat10588.cnf /tmp/csp2sat10588.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1435506 4048744 | 478502 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 5 (1 /sec) decisions : 253 (43 /sec) propagations : 294774 (49625 /sec) conflict literals : 21 (16.00 % deleted) Memory used : 161.91 MB CPU time : 5.94 s SATISFIABLE VERIFY_CNF 1223 END : (7 seconds) [Sun Jun 18 17:04:08 2006] VERIFY_CNF 1223 CPU : 6.64 = 0 + 0 + 6.05 + 0.59 # RESULT : makespan 1223 SATISFIABLE SHOW_RESULT 1223 BEGIN : [Sun Jun 18 17:04:08 2006] # ASSIGN : makespan 1223 # ASSIGN : s_0_0 0 # ASSIGN : s_0_1 1 # ASSIGN : s_0_2 58 # ASSIGN : s_0_3 474 # ASSIGN : s_0_4 1076 # ASSIGN : s_0_5 2 # ASSIGN : s_0_6 1095 # ASSIGN : s_0_7 146 # ASSIGN : s_1_0 771 # ASSIGN : s_1_1 3 # ASSIGN : s_1_2 65 # ASSIGN : s_1_3 83 # ASSIGN : s_1_4 4 # ASSIGN : s_1_5 76 # ASSIGN : s_1_6 113 # ASSIGN : s_1_7 1220 # ASSIGN : s_2_0 60 # ASSIGN : s_2_1 112 # ASSIGN : s_2_2 141 # ASSIGN : s_2_3 1 # ASSIGN : s_2_4 628 # ASSIGN : s_2_5 980 # ASSIGN : s_2_6 612 # ASSIGN : s_2_7 395 # ASSIGN : s_3_0 1 # ASSIGN : s_3_1 723 # ASSIGN : s_3_2 0 # ASSIGN : s_3_3 2 # ASSIGN : s_3_4 5 # ASSIGN : s_3_5 3 # ASSIGN : s_3_6 739 # ASSIGN : s_3_7 4 # ASSIGN : s_4_0 584 # ASSIGN : s_4_1 748 # ASSIGN : s_4_2 1211 # ASSIGN : s_4_3 204 # ASSIGN : s_4_4 1212 # ASSIGN : s_4_5 192 # ASSIGN : s_4_6 1222 # ASSIGN : s_4_7 21 # ASSIGN : s_5_0 77 # ASSIGN : s_5_1 196 # ASSIGN : s_5_2 487 # ASSIGN : s_5_3 445 # ASSIGN : s_5_4 1214 # ASSIGN : s_5_5 195 # ASSIGN : s_5_6 1215 # ASSIGN : s_5_7 483 # ASSIGN : s_6_0 220 # ASSIGN : s_6_1 447 # ASSIGN : s_6_2 445 # ASSIGN : s_6_3 446 # ASSIGN : s_6_4 1218 # ASSIGN : s_6_5 219 # ASSIGN : s_6_6 687 # ASSIGN : s_6_7 688 # ASSIGN : s_7_0 92 # ASSIGN : s_7_1 1217 # ASSIGN : s_7_2 1218 # ASSIGN : s_7_3 1094 # ASSIGN : s_7_4 1219 # ASSIGN : s_7_5 237 # ASSIGN : s_7_6 1220 # ASSIGN : s_7_7 1222 SHOW_RESULT 1223 END : 1223 (1 seconds) [Sun Jun 18 17:04:09 2006] SHOW_RESULT 1223 CPU : 1.00000000000001 = 0.990000000000009 + 0.01 + 0 + 0 # BOUND : makespan 1212 1223 MODIFY_CNF 1217 BEGIN : [Sun Jun 18 17:04:09 2006] MODIFY_CNF 1217 END : 92383813 bytes (0 seconds) [Sun Jun 18 17:04:09 2006] MODIFY_CNF 1217 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1217 BEGIN : [Sun Jun 18 17:04:09 2006] CMD : minisat /tmp/csp2sat10588.cnf /tmp/csp2sat10588.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1430130 4032616 | 476710 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (0 /sec) decisions : 24 (4 /sec) propagations : 200141 (34507 /sec) conflict literals : 1 (0.00 % deleted) Memory used : 160.69 MB CPU time : 5.8 s UNSATISFIABLE VERIFY_CNF 1217 END : (6 seconds) [Sun Jun 18 17:04:15 2006] VERIFY_CNF 1217 CPU : 6.26 = 0 + 0 + 5.8 + 0.46 # RESULT : makespan 1217 UNSATISFIABLE # BOUND : makespan 1218 1223 MODIFY_CNF 1220 BEGIN : [Sun Jun 18 17:04:15 2006] MODIFY_CNF 1220 END : 92383813 bytes (0 seconds) [Sun Jun 18 17:04:15 2006] MODIFY_CNF 1220 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1220 BEGIN : [Sun Jun 18 17:04:15 2006] CMD : minisat /tmp/csp2sat10588.cnf /tmp/csp2sat10588.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1432818 4040680 | 477606 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 4 (1 /sec) decisions : 215 (36 /sec) propagations : 306942 (50818 /sec) conflict literals : 11 (0.00 % deleted) Memory used : 161.91 MB CPU time : 6.04 s SATISFIABLE VERIFY_CNF 1220 END : (7 seconds) [Sun Jun 18 17:04:22 2006] VERIFY_CNF 1220 CPU : 6.64 = 0 + 0 + 6.18 + 0.46 # RESULT : makespan 1220 SATISFIABLE SHOW_RESULT 1220 BEGIN : [Sun Jun 18 17:04:22 2006] # ASSIGN : makespan 1220 # ASSIGN : s_0_0 11 # ASSIGN : s_0_1 1 # ASSIGN : s_0_2 34 # ASSIGN : s_0_3 128 # ASSIGN : s_0_4 1195 # ASSIGN : s_0_5 0 # ASSIGN : s_0_6 730 # ASSIGN : s_0_7 946 # ASSIGN : s_1_0 597 # ASSIGN : s_1_1 2 # ASSIGN : s_1_2 1195 # ASSIGN : s_1_3 10 # ASSIGN : s_1_4 1 # ASSIGN : s_1_5 3 # ASSIGN : s_1_6 98 # ASSIGN : s_1_7 1217 # ASSIGN : s_2_0 12 # ASSIGN : s_2_1 295 # ASSIGN : s_2_2 41 # ASSIGN : s_2_3 40 # ASSIGN : s_2_4 625 # ASSIGN : s_2_5 977 # ASSIGN : s_2_6 609 # ASSIGN : s_2_7 324 # ASSIGN : s_3_0 1219 # ASSIGN : s_3_1 788 # ASSIGN : s_3_2 1206 # ASSIGN : s_3_3 804 # ASSIGN : s_3_4 2 # ASSIGN : s_3_5 1 # ASSIGN : s_3_6 850 # ASSIGN : s_3_7 0 # ASSIGN : s_4_0 1046 # ASSIGN : s_4_1 325 # ASSIGN : s_4_2 324 # ASSIGN : s_4_3 805 # ASSIGN : s_4_4 1214 # ASSIGN : s_4_5 42 # ASSIGN : s_4_6 1210 # ASSIGN : s_4_7 199 # ASSIGN : s_5_0 29 # ASSIGN : s_5_1 46 # ASSIGN : s_5_2 471 # ASSIGN : s_5_3 44 # ASSIGN : s_5_4 1216 # ASSIGN : s_5_5 45 # ASSIGN : s_5_6 1211 # ASSIGN : s_5_7 412 # ASSIGN : s_6_0 191 # ASSIGN : s_6_1 966 # ASSIGN : s_6_2 1216 # ASSIGN : s_6_3 127 # ASSIGN : s_6_4 1217 # ASSIGN : s_6_5 190 # ASSIGN : s_6_6 1219 # ASSIGN : s_6_7 416 # ASSIGN : s_7_0 63 # ASSIGN : s_7_1 1206 # ASSIGN : s_7_2 1207 # ASSIGN : s_7_3 1083 # ASSIGN : s_7_4 1218 # ASSIGN : s_7_5 234 # ASSIGN : s_7_6 1208 # ASSIGN : s_7_7 1219 SHOW_RESULT 1220 END : 1220 (1 seconds) [Sun Jun 18 17:04:23 2006] SHOW_RESULT 1220 CPU : 1 = 1 + 0 + 0 + 0 # BOUND : makespan 1218 1220 MODIFY_CNF 1219 BEGIN : [Sun Jun 18 17:04:23 2006] MODIFY_CNF 1219 END : 92383813 bytes (0 seconds) [Sun Jun 18 17:04:23 2006] MODIFY_CNF 1219 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1219 BEGIN : [Sun Jun 18 17:04:23 2006] CMD : minisat /tmp/csp2sat10588.cnf /tmp/csp2sat10588.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1431922 4037992 | 477307 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (0 /sec) decisions : 168 (29 /sec) propagations : 270106 (46093 /sec) conflict literals : 5 (0.00 % deleted) Memory used : 161.91 MB CPU time : 5.86 s SATISFIABLE VERIFY_CNF 1219 END : (6 seconds) [Sun Jun 18 17:04:29 2006] VERIFY_CNF 1219 CPU : 6.5 = 0 + 0 + 5.98999999999999 + 0.510000000000001 # RESULT : makespan 1219 SATISFIABLE SHOW_RESULT 1219 BEGIN : [Sun Jun 18 17:04:29 2006] # ASSIGN : makespan 1219 # ASSIGN : s_0_0 4 # ASSIGN : s_0_1 5 # ASSIGN : s_0_2 57 # ASSIGN : s_0_3 132 # ASSIGN : s_0_4 1189 # ASSIGN : s_0_5 6 # ASSIGN : s_0_6 734 # ASSIGN : s_0_7 940 # ASSIGN : s_1_0 513 # ASSIGN : s_1_1 6 # ASSIGN : s_1_2 1201 # ASSIGN : s_1_3 1060 # ASSIGN : s_1_4 0 # ASSIGN : s_1_5 7 # ASSIGN : s_1_6 14 # ASSIGN : s_1_7 1216 # ASSIGN : s_2_0 496 # ASSIGN : s_2_1 34 # ASSIGN : s_2_2 64 # ASSIGN : s_2_3 63 # ASSIGN : s_2_4 624 # ASSIGN : s_2_5 976 # ASSIGN : s_2_6 608 # ASSIGN : s_2_7 318 # ASSIGN : s_3_0 1211 # ASSIGN : s_3_1 802 # ASSIGN : s_3_2 1212 # ASSIGN : s_3_3 818 # ASSIGN : s_3_4 1 # ASSIGN : s_3_5 853 # ASSIGN : s_3_6 854 # ASSIGN : s_3_7 0 # ASSIGN : s_4_0 21 # ASSIGN : s_4_1 339 # ASSIGN : s_4_2 338 # ASSIGN : s_4_3 819 # ASSIGN : s_4_4 1208 # ASSIGN : s_4_5 18 # ASSIGN : s_4_6 1210 # ASSIGN : s_4_7 193 # ASSIGN : s_5_0 6 # ASSIGN : s_5_1 90 # ASSIGN : s_5_2 477 # ASSIGN : s_5_3 88 # ASSIGN : s_5_4 1210 # ASSIGN : s_5_5 89 # ASSIGN : s_5_6 1211 # ASSIGN : s_5_7 406 # ASSIGN : s_6_0 185 # ASSIGN : s_6_1 973 # ASSIGN : s_6_2 1213 # ASSIGN : s_6_3 108 # ASSIGN : s_6_4 1214 # ASSIGN : s_6_5 109 # ASSIGN : s_6_6 1218 # ASSIGN : s_6_7 410 # ASSIGN : s_7_0 962 # ASSIGN : s_7_1 1213 # ASSIGN : s_7_2 1214 # ASSIGN : s_7_3 1090 # ASSIGN : s_7_4 1215 # ASSIGN : s_7_5 110 # ASSIGN : s_7_6 1216 # ASSIGN : s_7_7 1218 SHOW_RESULT 1219 END : 1219 (1 seconds) [Sun Jun 18 17:04:30 2006] SHOW_RESULT 1219 CPU : 1.00999999999999 = 1.00999999999999 + 0 + 0 + 0 # BOUND : makespan 1218 1219 MODIFY_CNF 1218 BEGIN : [Sun Jun 18 17:04:30 2006] MODIFY_CNF 1218 END : 92383813 bytes (0 seconds) [Sun Jun 18 17:04:30 2006] MODIFY_CNF 1218 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1218 BEGIN : [Sun Jun 18 17:04:30 2006] CMD : minisat /tmp/csp2sat10588.cnf /tmp/csp2sat10588.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1431026 4035304 | 477008 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 8 (1 /sec) decisions : 234 (38 /sec) propagations : 380334 (61843 /sec) conflict literals : 28 (20.00 % deleted) Memory used : 161.91 MB CPU time : 6.15 s SATISFIABLE VERIFY_CNF 1218 END : (7 seconds) [Sun Jun 18 17:04:37 2006] VERIFY_CNF 1218 CPU : 6.76 = 0 + 0.01 + 6.26000000000001 + 0.489999999999999 # RESULT : makespan 1218 SATISFIABLE SHOW_RESULT 1218 BEGIN : [Sun Jun 18 17:04:37 2006] # ASSIGN : makespan 1218 # ASSIGN : s_0_0 4 # ASSIGN : s_0_1 7 # ASSIGN : s_0_2 8 # ASSIGN : s_0_3 250 # ASSIGN : s_0_4 1190 # ASSIGN : s_0_5 15 # ASSIGN : s_0_6 16 # ASSIGN : s_0_7 941 # ASSIGN : s_1_0 636 # ASSIGN : s_1_1 14 # ASSIGN : s_1_2 48 # ASSIGN : s_1_3 59 # ASSIGN : s_1_4 1213 # ASSIGN : s_1_5 89 # ASSIGN : s_1_6 137 # ASSIGN : s_1_7 1215 # ASSIGN : s_2_0 606 # ASSIGN : s_2_1 16 # ASSIGN : s_2_2 231 # ASSIGN : s_2_3 95 # ASSIGN : s_2_4 623 # ASSIGN : s_2_5 975 # ASSIGN : s_2_6 0 # ASSIGN : s_2_7 96 # ASSIGN : s_3_0 635 # ASSIGN : s_3_1 1200 # ASSIGN : s_3_2 1216 # ASSIGN : s_3_3 1217 # ASSIGN : s_3_4 0 # ASSIGN : s_3_5 842 # ASSIGN : s_3_6 844 # ASSIGN : s_3_7 843 # ASSIGN : s_4_0 333 # ASSIGN : s_4_1 497 # ASSIGN : s_4_2 95 # ASSIGN : s_4_3 975 # ASSIGN : s_4_4 1216 # ASSIGN : s_4_5 96 # ASSIGN : s_4_6 136 # ASSIGN : s_4_7 184 # ASSIGN : s_5_0 294 # ASSIGN : s_5_1 45 # ASSIGN : s_5_2 485 # ASSIGN : s_5_3 43 # ASSIGN : s_5_4 1209 # ASSIGN : s_5_5 44 # ASSIGN : s_5_6 1210 # ASSIGN : s_5_7 309 # ASSIGN : s_6_0 5 # ASSIGN : s_6_1 960 # ASSIGN : s_6_2 230 # ASSIGN : s_6_3 1216 # ASSIGN : s_6_4 1215 # ASSIGN : s_6_5 959 # ASSIGN : s_6_6 1217 # ASSIGN : s_6_7 313 # ASSIGN : s_7_0 1085 # ASSIGN : s_7_1 15 # ASSIGN : s_7_2 1213 # ASSIGN : s_7_3 852 # ASSIGN : s_7_4 1214 # ASSIGN : s_7_5 99 # ASSIGN : s_7_6 1215 # ASSIGN : s_7_7 1217 SHOW_RESULT 1218 END : 1218 (1 seconds) [Sun Jun 18 17:04:38 2006] SHOW_RESULT 1218 CPU : 1.01000000000001 = 0.990000000000009 + 0.0199999999999999 + 0 + 0 # BOUND : makespan 1218 1218 MAIN END : (248 seconds) [Sun Jun 18 17:04:38 2006] MAIN CPU : 247.41 = 166.64 + 0.7 + 74.14 + 5.93