# TIMEOUT 18000 MAIN BEGIN : [Sun Jun 18 17:04:38 2006] READ BEGIN : csp/gp08-06.csp [Sun Jun 18 17:04:38 2006] READ END : csp/gp08-06.csp (1 seconds) [Sun Jun 18 17:04:39 2006] READ CPU : 0.93 = 0.92 + 0.01 + 0 + 0 # BOUND : makespan 1000 3123 GENERATE_CNF 3123 BEGIN : [Sun Jun 18 17:04:39 2006] GENERATE_CNF 3123 END : 203085 variables 3026638 clauses 70570913 bytes (114 seconds) [Sun Jun 18 17:06:33 2006] GENERATE_CNF 3123 CPU : 113.43 = 112.94 + 0.49 + 0 + 0 MODIFY_CNF 2061 BEGIN : [Sun Jun 18 17:06:33 2006] MODIFY_CNF 2061 END : 70570920 bytes (0 seconds) [Sun Jun 18 17:06:33 2006] MODIFY_CNF 2061 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 2061 BEGIN : [Sun Jun 18 17:06:33 2006] CMD : minisat /tmp/csp2sat10676.cnf /tmp/csp2sat10676.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 2073737 6020182 | 691245 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 3 (1 /sec) decisions : 348 (83 /sec) propagations : 243352 (57941 /sec) conflict literals : 34 (2.86 % deleted) Memory used : 125.86 MB CPU time : 4.2 s SATISFIABLE VERIFY_CNF 2061 END : (5 seconds) [Sun Jun 18 17:06:38 2006] VERIFY_CNF 2061 CPU : 4.71 = 0 + 0 + 4.29 + 0.42 # RESULT : makespan 2061 SATISFIABLE SHOW_RESULT 2061 BEGIN : [Sun Jun 18 17:06:38 2006] # ASSIGN : makespan 2061 # ASSIGN : s_0_0 783 # ASSIGN : s_0_1 29 # ASSIGN : s_0_2 372 # ASSIGN : s_0_3 486 # ASSIGN : s_0_4 25 # ASSIGN : s_0_5 26 # ASSIGN : s_0_6 371 # ASSIGN : s_0_7 698 # ASSIGN : s_1_0 2060 # ASSIGN : s_1_1 371 # ASSIGN : s_1_2 531 # ASSIGN : s_1_3 717 # ASSIGN : s_1_4 981 # ASSIGN : s_1_5 208 # ASSIGN : s_1_6 372 # ASSIGN : s_1_7 966 # ASSIGN : s_2_0 1025 # ASSIGN : s_2_1 394 # ASSIGN : s_2_2 699 # ASSIGN : s_2_3 900 # ASSIGN : s_2_4 1584 # ASSIGN : s_2_5 211 # ASSIGN : s_2_6 398 # ASSIGN : s_2_7 1026 # ASSIGN : s_3_0 1240 # ASSIGN : s_3_1 562 # ASSIGN : s_3_2 700 # ASSIGN : s_3_3 901 # ASSIGN : s_3_4 1878 # ASSIGN : s_3_5 950 # ASSIGN : s_3_6 1246 # ASSIGN : s_3_7 1241 # ASSIGN : s_4_0 112 # ASSIGN : s_4_1 563 # ASSIGN : s_4_2 725 # ASSIGN : s_4_3 2034 # ASSIGN : s_4_4 1879 # ASSIGN : s_4_5 1395 # ASSIGN : s_4_6 2012 # ASSIGN : s_4_7 1242 # ASSIGN : s_5_0 239 # ASSIGN : s_5_1 863 # ASSIGN : s_5_2 890 # ASSIGN : s_5_3 1274 # ASSIGN : s_5_4 1880 # ASSIGN : s_5_5 1978 # ASSIGN : s_5_6 2013 # ASSIGN : s_5_7 1275 # ASSIGN : s_6_0 245 # ASSIGN : s_6_1 864 # ASSIGN : s_6_2 1352 # ASSIGN : s_6_3 1494 # ASSIGN : s_6_4 1881 # ASSIGN : s_6_5 1979 # ASSIGN : s_6_6 2014 # ASSIGN : s_6_7 2015 # ASSIGN : s_7_0 1061 # ASSIGN : s_7_1 1145 # ASSIGN : s_7_2 1353 # ASSIGN : s_7_3 1495 # ASSIGN : s_7_4 2021 # ASSIGN : s_7_5 2022 # ASSIGN : s_7_6 2023 # ASSIGN : s_7_7 2060 SHOW_RESULT 2061 END : 2061 (0 seconds) [Sun Jun 18 17:06:38 2006] SHOW_RESULT 2061 CPU : 0.410000000000001 = 0.390000000000001 + 0.02 + 0 + 0 # BOUND : makespan 1000 2061 MODIFY_CNF 1530 BEGIN : [Sun Jun 18 17:06:38 2006] MODIFY_CNF 1530 END : 70570919 bytes (0 seconds) [Sun Jun 18 17:06:38 2006] MODIFY_CNF 1530 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1530 BEGIN : [Sun Jun 18 17:06:38 2006] CMD : minisat /tmp/csp2sat10676.cnf /tmp/csp2sat10676.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1597961 4592854 | 532653 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 4 (1 /sec) decisions : 345 (77 /sec) propagations : 257592 (57756 /sec) conflict literals : 24 (0.00 % deleted) Memory used : 125.87 MB CPU time : 4.46 s SATISFIABLE VERIFY_CNF 1530 END : (5 seconds) [Sun Jun 18 17:06:43 2006] VERIFY_CNF 1530 CPU : 4.97 = 0 + 0 + 4.57 + 0.4 # RESULT : makespan 1530 SATISFIABLE SHOW_RESULT 1530 BEGIN : [Sun Jun 18 17:06:43 2006] # ASSIGN : makespan 1530 # ASSIGN : s_0_0 493 # ASSIGN : s_0_1 1074 # ASSIGN : s_0_2 1416 # ASSIGN : s_0_3 97 # ASSIGN : s_0_4 10 # ASSIGN : s_0_5 0 # ASSIGN : s_0_6 11 # ASSIGN : s_0_7 12 # ASSIGN : s_1_0 2 # ASSIGN : s_1_1 0 # ASSIGN : s_1_2 1105 # ASSIGN : s_1_3 309 # ASSIGN : s_1_4 492 # ASSIGN : s_1_5 3 # ASSIGN : s_1_6 148 # ASSIGN : s_1_7 174 # ASSIGN : s_2_0 5 # ASSIGN : s_2_1 1 # ASSIGN : s_2_2 0 # ASSIGN : s_2_3 705 # ASSIGN : s_2_4 1095 # ASSIGN : s_2_5 6 # ASSIGN : s_2_6 404 # ASSIGN : s_2_7 189 # ASSIGN : s_3_0 59 # ASSIGN : s_3_1 60 # ASSIGN : s_3_2 61 # ASSIGN : s_3_3 1340 # ASSIGN : s_3_4 1389 # ASSIGN : s_3_5 383 # ASSIGN : s_3_6 708 # ASSIGN : s_3_7 673 # ASSIGN : s_4_0 251 # ASSIGN : s_4_1 378 # ASSIGN : s_4_2 86 # ASSIGN : s_4_3 1503 # ASSIGN : s_4_4 1390 # ASSIGN : s_4_5 872 # ASSIGN : s_4_6 1490 # ASSIGN : s_4_7 674 # ASSIGN : s_5_0 245 # ASSIGN : s_5_1 96 # ASSIGN : s_5_2 322 # ASSIGN : s_5_3 706 # ASSIGN : s_5_4 1391 # ASSIGN : s_5_5 1356 # ASSIGN : s_5_6 1491 # ASSIGN : s_5_7 707 # ASSIGN : s_6_0 735 # ASSIGN : s_6_1 97 # ASSIGN : s_6_2 1273 # ASSIGN : s_6_3 1311 # ASSIGN : s_6_4 1392 # ASSIGN : s_6_5 1357 # ASSIGN : s_6_6 1492 # ASSIGN : s_6_7 1312 # ASSIGN : s_7_0 409 # ASSIGN : s_7_1 540 # ASSIGN : s_7_2 1274 # ASSIGN : s_7_3 748 # ASSIGN : s_7_4 1490 # ASSIGN : s_7_5 1491 # ASSIGN : s_7_6 1493 # ASSIGN : s_7_7 1492 SHOW_RESULT 1530 END : 1530 (1 seconds) [Sun Jun 18 17:06:44 2006] SHOW_RESULT 1530 CPU : 0.399999999999991 = 0.399999999999991 + 0 + 0 + 0 # BOUND : makespan 1000 1530 MODIFY_CNF 1265 BEGIN : [Sun Jun 18 17:06:44 2006] MODIFY_CNF 1265 END : 70570919 bytes (0 seconds) [Sun Jun 18 17:06:44 2006] MODIFY_CNF 1265 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1265 BEGIN : [Sun Jun 18 17:06:44 2006] CMD : minisat /tmp/csp2sat10676.cnf /tmp/csp2sat10676.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1360521 3880534 | 453507 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 3 (1 /sec) decisions : 193 (40 /sec) propagations : 217901 (45491 /sec) conflict literals : 23 (4.17 % deleted) Memory used : 125.87 MB CPU time : 4.79 s SATISFIABLE VERIFY_CNF 1265 END : (5 seconds) [Sun Jun 18 17:06:49 2006] VERIFY_CNF 1265 CPU : 5.28 = 0 + 0 + 4.9 + 0.38 # RESULT : makespan 1265 SATISFIABLE SHOW_RESULT 1265 BEGIN : [Sun Jun 18 17:06:49 2006] # ASSIGN : makespan 1265 # ASSIGN : s_0_0 123 # ASSIGN : s_0_1 365 # ASSIGN : s_0_2 707 # ASSIGN : s_0_3 821 # ASSIGN : s_0_4 1 # ASSIGN : s_0_5 35 # ASSIGN : s_0_6 0 # ASSIGN : s_0_7 38 # ASSIGN : s_1_0 41 # ASSIGN : s_1_1 0 # ASSIGN : s_1_2 832 # ASSIGN : s_1_3 1033 # ASSIGN : s_1_4 185 # ASSIGN : s_1_5 167 # ASSIGN : s_1_6 1 # ASSIGN : s_1_7 170 # ASSIGN : s_2_0 0 # ASSIGN : s_2_1 23 # ASSIGN : s_2_2 1 # ASSIGN : s_2_3 787 # ASSIGN : s_2_4 788 # ASSIGN : s_2_5 1082 # ASSIGN : s_2_6 27 # ASSIGN : s_2_7 328 # ASSIGN : s_3_0 42 # ASSIGN : s_3_1 48 # ASSIGN : s_3_2 3 # ASSIGN : s_3_3 1216 # ASSIGN : s_3_4 2 # ASSIGN : s_3_5 221 # ASSIGN : s_3_6 584 # ASSIGN : s_3_7 543 # ASSIGN : s_4_0 417 # ASSIGN : s_4_1 1063 # ASSIGN : s_4_2 28 # ASSIGN : s_4_3 0 # ASSIGN : s_4_4 27 # ASSIGN : s_4_5 579 # ASSIGN : s_4_6 1225 # ASSIGN : s_4_7 544 # ASSIGN : s_5_0 43 # ASSIGN : s_5_1 49 # ASSIGN : s_5_2 193 # ASSIGN : s_5_3 50 # ASSIGN : s_5_4 184 # ASSIGN : s_5_5 192 # ASSIGN : s_5_6 1226 # ASSIGN : s_5_7 577 # ASSIGN : s_6_0 546 # ASSIGN : s_6_1 84 # ASSIGN : s_6_2 2 # ASSIGN : s_6_3 51 # ASSIGN : s_6_4 1084 # ASSIGN : s_6_5 511 # ASSIGN : s_6_6 1227 # ASSIGN : s_6_7 1182 # ASSIGN : s_7_0 1142 # ASSIGN : s_7_1 792 # ASSIGN : s_7_2 1000 # ASSIGN : s_7_3 52 # ASSIGN : s_7_4 1226 # ASSIGN : s_7_5 578 # ASSIGN : s_7_6 1228 # ASSIGN : s_7_7 1227 SHOW_RESULT 1265 END : 1265 (0 seconds) [Sun Jun 18 17:06:49 2006] SHOW_RESULT 1265 CPU : 0.379999999999999 = 0.359999999999999 + 0.02 + 0 + 0 # BOUND : makespan 1000 1265 MODIFY_CNF 1132 BEGIN : [Sun Jun 18 17:06:49 2006] MODIFY_CNF 1132 END : 70570919 bytes (0 seconds) [Sun Jun 18 17:06:49 2006] MODIFY_CNF 1132 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1132 BEGIN : [Sun Jun 18 17:06:49 2006] CMD : minisat /tmp/csp2sat10676.cnf /tmp/csp2sat10676.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1241353 3523030 | 413784 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 43 (8 /sec) decisions : 170 (32 /sec) propagations : 514432 (95797 /sec) conflict literals : 614 (34.33 % deleted) Memory used : 125.87 MB CPU time : 5.37 s SATISFIABLE VERIFY_CNF 1132 END : (6 seconds) [Sun Jun 18 17:06:55 2006] VERIFY_CNF 1132 CPU : 5.83 = 0 + 0.01 + 5.47 + 0.35 # RESULT : makespan 1132 SATISFIABLE SHOW_RESULT 1132 BEGIN : [Sun Jun 18 17:06:55 2006] # ASSIGN : makespan 1132 # ASSIGN : s_0_0 137 # ASSIGN : s_0_1 628 # ASSIGN : s_0_2 4 # ASSIGN : s_0_3 393 # ASSIGN : s_0_4 1131 # ASSIGN : s_0_5 1127 # ASSIGN : s_0_6 3 # ASSIGN : s_0_7 986 # ASSIGN : s_1_0 2 # ASSIGN : s_1_1 42 # ASSIGN : s_1_2 295 # ASSIGN : s_1_3 112 # ASSIGN : s_1_4 513 # ASSIGN : s_1_5 31 # ASSIGN : s_1_6 86 # ASSIGN : s_1_7 1116 # ASSIGN : s_2_0 1131 # ASSIGN : s_2_1 609 # ASSIGN : s_2_2 613 # ASSIGN : s_2_3 33 # ASSIGN : s_2_4 219 # ASSIGN : s_2_5 34 # ASSIGN : s_2_6 829 # ASSIGN : s_2_7 614 # ASSIGN : s_3_0 1 # ASSIGN : s_3_1 43 # ASSIGN : s_3_2 1107 # ASSIGN : s_3_3 63 # ASSIGN : s_3_4 118 # ASSIGN : s_3_5 817 # ASSIGN : s_3_6 185 # ASSIGN : s_3_7 8 # ASSIGN : s_4_0 3 # ASSIGN : s_4_1 970 # ASSIGN : s_4_2 130 # ASSIGN : s_4_3 306 # ASSIGN : s_4_4 2 # ASSIGN : s_4_5 333 # ASSIGN : s_4_6 828 # ASSIGN : s_4_7 937 # ASSIGN : s_5_0 1123 # ASSIGN : s_5_1 627 # ASSIGN : s_5_2 723 # ASSIGN : s_5_3 8 # ASSIGN : s_5_4 1129 # ASSIGN : s_5_5 1130 # ASSIGN : s_5_6 1131 # ASSIGN : s_5_7 9 # ASSIGN : s_6_0 533 # ASSIGN : s_6_1 252 # ASSIGN : s_6_2 118 # ASSIGN : s_6_3 1131 # ASSIGN : s_6_4 119 # ASSIGN : s_6_5 217 # ASSIGN : s_6_6 1130 # ASSIGN : s_6_7 1071 # ASSIGN : s_7_0 379 # ASSIGN : s_7_1 44 # ASSIGN : s_7_2 463 # ASSIGN : s_7_3 605 # ASSIGN : s_7_4 6 # ASSIGN : s_7_5 332 # ASSIGN : s_7_6 7 # ASSIGN : s_7_7 1131 SHOW_RESULT 1132 END : 1132 (1 seconds) [Sun Jun 18 17:06:56 2006] SHOW_RESULT 1132 CPU : 0.39000000000001 = 0.38000000000001 + 0.0099999999999999 + 0 + 0 # BOUND : makespan 1000 1132 MODIFY_CNF 1066 BEGIN : [Sun Jun 18 17:06:56 2006] MODIFY_CNF 1066 END : 70570918 bytes (0 seconds) [Sun Jun 18 17:06:56 2006] MODIFY_CNF 1066 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1066 BEGIN : [Sun Jun 18 17:06:56 2006] CMD : minisat /tmp/csp2sat10676.cnf /tmp/csp2sat10676.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1182217 3345622 | 394072 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (0 /sec) decisions : 13 (3 /sec) propagations : 150770 (32847 /sec) conflict literals : 1 (0.00 % deleted) Memory used : 124.88 MB CPU time : 4.59 s UNSATISFIABLE VERIFY_CNF 1066 END : (5 seconds) [Sun Jun 18 17:07:01 2006] VERIFY_CNF 1066 CPU : 4.99 = 0 + 0 + 4.59 + 0.4 # RESULT : makespan 1066 UNSATISFIABLE # BOUND : makespan 1067 1132 MODIFY_CNF 1099 BEGIN : [Sun Jun 18 17:07:01 2006] MODIFY_CNF 1099 END : 70570919 bytes (0 seconds) [Sun Jun 18 17:07:01 2006] MODIFY_CNF 1099 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1099 BEGIN : [Sun Jun 18 17:07:01 2006] CMD : minisat /tmp/csp2sat10676.cnf /tmp/csp2sat10676.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1211785 3434326 | 403928 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (0 /sec) decisions : 13 (3 /sec) propagations : 147955 (28618 /sec) conflict literals : 1 (0.00 % deleted) Memory used : 124.87 MB CPU time : 5.17 s UNSATISFIABLE VERIFY_CNF 1099 END : (5 seconds) [Sun Jun 18 17:07:06 2006] VERIFY_CNF 1099 CPU : 5.49 = 0 + 0 + 5.17 + 0.32 # RESULT : makespan 1099 UNSATISFIABLE # BOUND : makespan 1100 1132 MODIFY_CNF 1116 BEGIN : [Sun Jun 18 17:07:06 2006] MODIFY_CNF 1116 END : 70570919 bytes (0 seconds) [Sun Jun 18 17:07:06 2006] MODIFY_CNF 1116 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1116 BEGIN : [Sun Jun 18 17:07:06 2006] CMD : minisat /tmp/csp2sat10676.cnf /tmp/csp2sat10676.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1227017 3480022 | 409005 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 6 (1 /sec) decisions : 160 (31 /sec) propagations : 253280 (48896 /sec) conflict literals : 59 (11.94 % deleted) Memory used : 125.87 MB CPU time : 5.18 s SATISFIABLE VERIFY_CNF 1116 END : (6 seconds) [Sun Jun 18 17:07:12 2006] VERIFY_CNF 1116 CPU : 5.59 = 0 + 0 + 5.27 + 0.32 # RESULT : makespan 1116 SATISFIABLE SHOW_RESULT 1116 BEGIN : [Sun Jun 18 17:07:12 2006] # ASSIGN : makespan 1116 # ASSIGN : s_0_0 290 # ASSIGN : s_0_1 565 # ASSIGN : s_0_2 1001 # ASSIGN : s_0_3 78 # ASSIGN : s_0_4 10 # ASSIGN : s_0_5 11 # ASSIGN : s_0_6 14 # ASSIGN : s_0_7 916 # ASSIGN : s_1_0 2 # ASSIGN : s_1_1 217 # ASSIGN : s_1_2 33 # ASSIGN : s_1_3 869 # ASSIGN : s_1_4 218 # ASSIGN : s_1_5 1052 # ASSIGN : s_1_6 1088 # ASSIGN : s_1_7 1055 # ASSIGN : s_2_0 3 # ASSIGN : s_2_1 561 # ASSIGN : s_2_2 4 # ASSIGN : s_2_3 5 # ASSIGN : s_2_4 821 # ASSIGN : s_2_5 354 # ASSIGN : s_2_6 53 # ASSIGN : s_2_7 606 # ASSIGN : s_3_0 6 # ASSIGN : s_3_1 1115 # ASSIGN : s_3_2 347 # ASSIGN : s_3_3 7 # ASSIGN : s_3_4 56 # ASSIGN : s_3_5 57 # ASSIGN : s_3_6 389 # ASSIGN : s_3_7 1021 # ASSIGN : s_4_0 163 # ASSIGN : s_4_1 1 # ASSIGN : s_4_2 372 # ASSIGN : s_4_3 316 # ASSIGN : s_4_4 0 # ASSIGN : s_4_5 537 # ASSIGN : s_4_6 1021 # ASSIGN : s_4_7 1022 # ASSIGN : s_5_0 1106 # ASSIGN : s_5_1 0 # ASSIGN : s_5_2 617 # ASSIGN : s_5_3 1112 # ASSIGN : s_5_4 1115 # ASSIGN : s_5_5 1113 # ASSIGN : s_5_6 1114 # ASSIGN : s_5_7 1 # ASSIGN : s_6_0 532 # ASSIGN : s_6_1 251 # ASSIGN : s_6_2 1115 # ASSIGN : s_6_3 6 # ASSIGN : s_6_4 120 # ASSIGN : s_6_5 17 # ASSIGN : s_6_6 52 # ASSIGN : s_6_7 1070 # ASSIGN : s_7_0 79 # ASSIGN : s_7_1 907 # ASSIGN : s_7_2 201 # ASSIGN : s_7_3 343 # ASSIGN : s_7_4 13 # ASSIGN : s_7_5 14 # ASSIGN : s_7_6 15 # ASSIGN : s_7_7 1115 SHOW_RESULT 1116 END : 1116 (0 seconds) [Sun Jun 18 17:07:12 2006] SHOW_RESULT 1116 CPU : 0.36999999999999 = 0.36999999999999 + 0 + 0 + 0 # BOUND : makespan 1100 1116 MODIFY_CNF 1108 BEGIN : [Sun Jun 18 17:07:12 2006] MODIFY_CNF 1108 END : 70570919 bytes (0 seconds) [Sun Jun 18 17:07:12 2006] MODIFY_CNF 1108 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1108 BEGIN : [Sun Jun 18 17:07:12 2006] CMD : minisat /tmp/csp2sat10676.cnf /tmp/csp2sat10676.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1219849 3458518 | 406616 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (0 /sec) decisions : 13 (3 /sec) propagations : 146983 (29338 /sec) conflict literals : 1 (0.00 % deleted) Memory used : 124.87 MB CPU time : 5.01 s UNSATISFIABLE VERIFY_CNF 1108 END : (6 seconds) [Sun Jun 18 17:07:18 2006] VERIFY_CNF 1108 CPU : 5.40000000000001 = 0 + 0.01 + 5.01000000000001 + 0.38 # RESULT : makespan 1108 UNSATISFIABLE # BOUND : makespan 1109 1116 MODIFY_CNF 1112 BEGIN : [Sun Jun 18 17:07:18 2006] MODIFY_CNF 1112 END : 70570919 bytes (0 seconds) [Sun Jun 18 17:07:18 2006] MODIFY_CNF 1112 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1112 BEGIN : [Sun Jun 18 17:07:18 2006] CMD : minisat /tmp/csp2sat10676.cnf /tmp/csp2sat10676.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1223433 3469270 | 407811 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (0 /sec) decisions : 13 (3 /sec) propagations : 148626 (30025 /sec) conflict literals : 1 (0.00 % deleted) Memory used : 124.87 MB CPU time : 4.95 s UNSATISFIABLE VERIFY_CNF 1112 END : (5 seconds) [Sun Jun 18 17:07:23 2006] VERIFY_CNF 1112 CPU : 5.35 = 0 + 0 + 4.95 + 0.4 # RESULT : makespan 1112 UNSATISFIABLE # BOUND : makespan 1113 1116 MODIFY_CNF 1114 BEGIN : [Sun Jun 18 17:07:23 2006] MODIFY_CNF 1114 END : 70570919 bytes (0 seconds) [Sun Jun 18 17:07:23 2006] MODIFY_CNF 1114 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1114 BEGIN : [Sun Jun 18 17:07:23 2006] CMD : minisat /tmp/csp2sat10676.cnf /tmp/csp2sat10676.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1225225 3474646 | 408408 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 3 (1 /sec) decisions : 13 (3 /sec) propagations : 166859 (32911 /sec) conflict literals : 3 (0.00 % deleted) Memory used : 124.89 MB CPU time : 5.07 s UNSATISFIABLE VERIFY_CNF 1114 END : (5 seconds) [Sun Jun 18 17:07:28 2006] VERIFY_CNF 1114 CPU : 5.43 = 0 + 0 + 5.07 + 0.36 # RESULT : makespan 1114 UNSATISFIABLE # BOUND : makespan 1115 1116 MODIFY_CNF 1115 BEGIN : [Sun Jun 18 17:07:28 2006] MODIFY_CNF 1115 END : 70570919 bytes (0 seconds) [Sun Jun 18 17:07:28 2006] MODIFY_CNF 1115 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1115 BEGIN : [Sun Jun 18 17:07:28 2006] CMD : minisat /tmp/csp2sat10676.cnf /tmp/csp2sat10676.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1226121 3477334 | 408707 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 7 (1 /sec) decisions : 125 (23 /sec) propagations : 284719 (53418 /sec) conflict literals : 44 (13.73 % deleted) Memory used : 125.87 MB CPU time : 5.33 s SATISFIABLE VERIFY_CNF 1115 END : (6 seconds) [Sun Jun 18 17:07:34 2006] VERIFY_CNF 1115 CPU : 5.73 = 0 + 0 + 5.43 + 0.3 # RESULT : makespan 1115 SATISFIABLE SHOW_RESULT 1115 BEGIN : [Sun Jun 18 17:07:34 2006] # ASSIGN : makespan 1115 # ASSIGN : s_0_0 583 # ASSIGN : s_0_1 241 # ASSIGN : s_0_2 3 # ASSIGN : s_0_3 899 # ASSIGN : s_0_4 1111 # ASSIGN : s_0_5 117 # ASSIGN : s_0_6 1113 # ASSIGN : s_0_7 140 # ASSIGN : s_1_0 1114 # ASSIGN : s_1_1 240 # ASSIGN : s_1_2 922 # ASSIGN : s_1_3 30 # ASSIGN : s_1_4 319 # ASSIGN : s_1_5 1 # ASSIGN : s_1_6 4 # ASSIGN : s_1_7 225 # ASSIGN : s_2_0 1113 # ASSIGN : s_2_1 600 # ASSIGN : s_2_2 604 # ASSIGN : s_2_3 1114 # ASSIGN : s_2_4 0 # ASSIGN : s_2_5 605 # ASSIGN : s_2_6 812 # ASSIGN : s_2_7 294 # ASSIGN : s_3_0 38 # ASSIGN : s_3_1 3 # ASSIGN : s_3_2 1090 # ASSIGN : s_3_3 739 # ASSIGN : s_3_4 1089 # ASSIGN : s_3_5 788 # ASSIGN : s_3_6 107 # ASSIGN : s_3_7 87 # ASSIGN : s_4_0 825 # ASSIGN : s_4_1 953 # ASSIGN : s_4_2 615 # ASSIGN : s_4_3 2 # ASSIGN : s_4_4 952 # ASSIGN : s_4_5 121 # ASSIGN : s_4_6 811 # ASSIGN : s_4_7 88 # ASSIGN : s_5_0 39 # ASSIGN : s_5_1 4 # ASSIGN : s_5_2 125 # ASSIGN : s_5_3 29 # ASSIGN : s_5_4 1114 # ASSIGN : s_5_5 120 # ASSIGN : s_5_6 106 # ASSIGN : s_5_7 509 # ASSIGN : s_6_0 45 # ASSIGN : s_6_1 672 # ASSIGN : s_6_2 614 # ASSIGN : s_6_3 1113 # ASSIGN : s_6_4 980 # ASSIGN : s_6_5 1078 # ASSIGN : s_6_6 1114 # ASSIGN : s_6_7 0 # ASSIGN : s_7_0 1028 # ASSIGN : s_7_1 5 # ASSIGN : s_7_2 780 # ASSIGN : s_7_3 213 # ASSIGN : s_7_4 1112 # ASSIGN : s_7_5 1113 # ASSIGN : s_7_6 743 # ASSIGN : s_7_7 1114 SHOW_RESULT 1115 END : 1115 (1 seconds) [Sun Jun 18 17:07:35 2006] SHOW_RESULT 1115 CPU : 0.380000000000005 = 0.370000000000005 + 0.01 + 0 + 0 # BOUND : makespan 1115 1115 MAIN END : (177 seconds) [Sun Jun 18 17:07:35 2006] MAIN CPU : 175.48 = 116.15 + 0.58 + 54.72 + 4.03