# TIMEOUT 18000 MAIN BEGIN : [Sun Jun 18 17:10:59 2006] READ BEGIN : csp/gp08-08.csp [Sun Jun 18 17:10:59 2006] READ END : csp/gp08-08.csp (1 seconds) [Sun Jun 18 17:11:00 2006] READ CPU : 0.93 = 0.93 + 0 + 0 + 0 # BOUND : makespan 1000 3187 GENERATE_CNF 3187 BEGIN : [Sun Jun 18 17:11:00 2006] GENERATE_CNF 3187 END : 207245 variables 3092238 clauses 72162000 bytes (116 seconds) [Sun Jun 18 17:12:56 2006] GENERATE_CNF 3187 CPU : 116.03 = 115.56 + 0.47 + 0 + 0 MODIFY_CNF 2093 BEGIN : [Sun Jun 18 17:12:56 2006] MODIFY_CNF 2093 END : 72162007 bytes (0 seconds) [Sun Jun 18 17:12:56 2006] MODIFY_CNF 2093 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 2093 BEGIN : [Sun Jun 18 17:12:56 2006] CMD : minisat /tmp/csp2sat10787.cnf /tmp/csp2sat10787.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 2110665 6126806 | 703555 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 4 (1 /sec) decisions : 352 (77 /sec) propagations : 259304 (56370 /sec) conflict literals : 52 (0.00 % deleted) Memory used : 128.43 MB CPU time : 4.6 s SATISFIABLE VERIFY_CNF 2093 END : (5 seconds) [Sun Jun 18 17:13:01 2006] VERIFY_CNF 2093 CPU : 5.11 = 0 + 0 + 4.71 + 0.4 # RESULT : makespan 2093 SATISFIABLE SHOW_RESULT 2093 BEGIN : [Sun Jun 18 17:13:01 2006] # ASSIGN : makespan 2093 # ASSIGN : s_0_0 199 # ASSIGN : s_0_1 50 # ASSIGN : s_0_2 9 # ASSIGN : s_0_3 19 # ASSIGN : s_0_4 20 # ASSIGN : s_0_5 171 # ASSIGN : s_0_6 445 # ASSIGN : s_0_7 1086 # ASSIGN : s_1_0 394 # ASSIGN : s_1_1 385 # ASSIGN : s_1_2 417 # ASSIGN : s_1_3 70 # ASSIGN : s_1_4 173 # ASSIGN : s_1_5 172 # ASSIGN : s_1_6 1509 # ASSIGN : s_1_7 1087 # ASSIGN : s_2_0 566 # ASSIGN : s_2_1 565 # ASSIGN : s_2_2 1072 # ASSIGN : s_2_3 72 # ASSIGN : s_2_4 1087 # ASSIGN : s_2_5 318 # ASSIGN : s_2_6 1606 # ASSIGN : s_2_7 1088 # ASSIGN : s_3_0 1020 # ASSIGN : s_3_1 570 # ASSIGN : s_3_2 1092 # ASSIGN : s_3_3 81 # ASSIGN : s_3_4 1330 # ASSIGN : s_3_5 319 # ASSIGN : s_3_6 1607 # ASSIGN : s_3_7 1613 # ASSIGN : s_4_0 1023 # ASSIGN : s_4_1 1028 # ASSIGN : s_4_2 1129 # ASSIGN : s_4_3 83 # ASSIGN : s_4_4 1400 # ASSIGN : s_4_5 320 # ASSIGN : s_4_6 1834 # ASSIGN : s_4_7 2044 # ASSIGN : s_5_0 1028 # ASSIGN : s_5_1 1029 # ASSIGN : s_5_2 1130 # ASSIGN : s_5_3 501 # ASSIGN : s_5_4 1410 # ASSIGN : s_5_5 1550 # ASSIGN : s_5_6 1840 # ASSIGN : s_5_7 2081 # ASSIGN : s_6_0 1038 # ASSIGN : s_6_1 1195 # ASSIGN : s_6_2 1395 # ASSIGN : s_6_3 611 # ASSIGN : s_6_4 1411 # ASSIGN : s_6_5 2066 # ASSIGN : s_6_6 2068 # ASSIGN : s_6_7 2085 # ASSIGN : s_7_0 1093 # ASSIGN : s_7_1 1357 # ASSIGN : s_7_2 1512 # ASSIGN : s_7_3 1513 # ASSIGN : s_7_4 1725 # ASSIGN : s_7_5 2087 # ASSIGN : s_7_6 2088 # ASSIGN : s_7_7 2092 SHOW_RESULT 2093 END : 2093 (1 seconds) [Sun Jun 18 17:13:02 2006] SHOW_RESULT 2093 CPU : 0.42000000000001 = 0.38000000000001 + 0.04 + 0 + 0 # BOUND : makespan 1000 2093 MODIFY_CNF 1546 BEGIN : [Sun Jun 18 17:13:02 2006] MODIFY_CNF 1546 END : 72162006 bytes (0 seconds) [Sun Jun 18 17:13:02 2006] MODIFY_CNF 1546 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1546 BEGIN : [Sun Jun 18 17:13:02 2006] CMD : minisat /tmp/csp2sat10787.cnf /tmp/csp2sat10787.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1620553 4656470 | 540184 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 4 (1 /sec) decisions : 353 (76 /sec) propagations : 256825 (55470 /sec) conflict literals : 31 (6.06 % deleted) Memory used : 128.43 MB CPU time : 4.63 s SATISFIABLE VERIFY_CNF 1546 END : (5 seconds) [Sun Jun 18 17:13:07 2006] VERIFY_CNF 1546 CPU : 5.18 = 0 + 0.01 + 4.74 + 0.43 # RESULT : makespan 1546 SATISFIABLE SHOW_RESULT 1546 BEGIN : [Sun Jun 18 17:13:07 2006] # ASSIGN : makespan 1546 # ASSIGN : s_0_0 50 # ASSIGN : s_0_1 1425 # ASSIGN : s_0_2 2 # ASSIGN : s_0_3 1 # ASSIGN : s_0_4 20 # ASSIGN : s_0_5 12 # ASSIGN : s_0_6 321 # ASSIGN : s_0_7 305 # ASSIGN : s_1_0 27 # ASSIGN : s_1_1 4 # ASSIGN : s_1_2 307 # ASSIGN : s_1_3 2 # ASSIGN : s_1_4 94 # ASSIGN : s_1_5 13 # ASSIGN : s_1_6 962 # ASSIGN : s_1_7 306 # ASSIGN : s_2_0 1092 # ASSIGN : s_2_1 13 # ASSIGN : s_2_2 292 # ASSIGN : s_2_3 4 # ASSIGN : s_2_4 540 # ASSIGN : s_2_5 14 # ASSIGN : s_2_6 1059 # ASSIGN : s_2_7 541 # ASSIGN : s_3_0 6 # ASSIGN : s_3_1 186 # ASSIGN : s_3_2 96 # ASSIGN : s_3_3 133 # ASSIGN : s_3_4 648 # ASSIGN : s_3_5 1059 # ASSIGN : s_3_6 1060 # ASSIGN : s_3_7 1066 # ASSIGN : s_4_0 9 # ASSIGN : s_4_1 14 # ASSIGN : s_4_2 1027 # ASSIGN : s_4_3 728 # ASSIGN : s_4_4 718 # ASSIGN : s_4_5 15 # ASSIGN : s_4_6 1287 # ASSIGN : s_4_7 1497 # ASSIGN : s_5_0 245 # ASSIGN : s_5_1 636 # ASSIGN : s_5_2 1028 # ASSIGN : s_5_3 135 # ASSIGN : s_5_4 737 # ASSIGN : s_5_5 738 # ASSIGN : s_5_6 1293 # ASSIGN : s_5_7 1534 # ASSIGN : s_6_0 246 # ASSIGN : s_6_1 1263 # ASSIGN : s_6_2 1503 # ASSIGN : s_6_3 301 # ASSIGN : s_6_4 863 # ASSIGN : s_6_5 1519 # ASSIGN : s_6_6 1521 # ASSIGN : s_6_7 1538 # ASSIGN : s_7_0 546 # ASSIGN : s_7_1 810 # ASSIGN : s_7_2 1539 # ASSIGN : s_7_3 965 # ASSIGN : s_7_4 1177 # ASSIGN : s_7_5 1540 # ASSIGN : s_7_6 1541 # ASSIGN : s_7_7 1545 SHOW_RESULT 1546 END : 1546 (0 seconds) [Sun Jun 18 17:13:07 2006] SHOW_RESULT 1546 CPU : 0.529999999999996 = 0.519999999999996 + 0.01 + 0 + 0 # BOUND : makespan 1000 1546 MODIFY_CNF 1273 BEGIN : [Sun Jun 18 17:13:07 2006] MODIFY_CNF 1273 END : 72162006 bytes (0 seconds) [Sun Jun 18 17:13:07 2006] MODIFY_CNF 1273 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1273 BEGIN : [Sun Jun 18 17:13:07 2006] CMD : minisat /tmp/csp2sat10787.cnf /tmp/csp2sat10787.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1375945 3922646 | 458648 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 1 (0 /sec) decisions : 199 (39 /sec) propagations : 208984 (40817 /sec) conflict literals : 3 (0.00 % deleted) Memory used : 128.43 MB CPU time : 5.12 s SATISFIABLE VERIFY_CNF 1273 END : (6 seconds) [Sun Jun 18 17:13:13 2006] VERIFY_CNF 1273 CPU : 5.63 = 0 + 0 + 5.24 + 0.39 # RESULT : makespan 1273 SATISFIABLE SHOW_RESULT 1273 BEGIN : [Sun Jun 18 17:13:13 2006] # ASSIGN : makespan 1273 # ASSIGN : s_0_0 1078 # ASSIGN : s_0_1 947 # ASSIGN : s_0_2 745 # ASSIGN : s_0_3 0 # ASSIGN : s_0_4 4 # ASSIGN : s_0_5 2 # ASSIGN : s_0_6 104 # ASSIGN : s_0_7 3 # ASSIGN : s_1_0 14 # ASSIGN : s_1_1 3 # ASSIGN : s_1_2 37 # ASSIGN : s_1_3 1 # ASSIGN : s_1_4 692 # ASSIGN : s_1_5 12 # ASSIGN : s_1_6 910 # ASSIGN : s_1_7 13 # ASSIGN : s_2_0 553 # ASSIGN : s_2_1 17 # ASSIGN : s_2_2 19 # ASSIGN : s_2_3 8 # ASSIGN : s_2_4 34 # ASSIGN : s_2_5 18 # ASSIGN : s_2_6 1007 # ASSIGN : s_2_7 35 # ASSIGN : s_3_0 5 # ASSIGN : s_3_1 127 # ASSIGN : s_3_2 1193 # ASSIGN : s_3_3 18 # ASSIGN : s_3_4 57 # ASSIGN : s_3_5 20 # ASSIGN : s_3_6 1008 # ASSIGN : s_3_7 577 # ASSIGN : s_4_0 8 # ASSIGN : s_4_1 35 # ASSIGN : s_4_2 36 # ASSIGN : s_4_3 64 # ASSIGN : s_4_4 301 # ASSIGN : s_4_5 311 # ASSIGN : s_4_6 1014 # ASSIGN : s_4_7 1224 # ASSIGN : s_5_0 13 # ASSIGN : s_5_1 648 # ASSIGN : s_5_2 755 # ASSIGN : s_5_3 319 # ASSIGN : s_5_4 318 # ASSIGN : s_5_5 21 # ASSIGN : s_5_6 1020 # ASSIGN : s_5_7 1261 # ASSIGN : s_6_0 110 # ASSIGN : s_6_1 1068 # ASSIGN : s_6_2 1230 # ASSIGN : s_6_3 641 # ASSIGN : s_6_4 327 # ASSIGN : s_6_5 1246 # ASSIGN : s_6_6 1248 # ASSIGN : s_6_7 1265 # ASSIGN : s_7_0 165 # ASSIGN : s_7_1 749 # ASSIGN : s_7_2 1266 # ASSIGN : s_7_3 429 # ASSIGN : s_7_4 904 # ASSIGN : s_7_5 1267 # ASSIGN : s_7_6 1268 # ASSIGN : s_7_7 1272 SHOW_RESULT 1273 END : 1273 (1 seconds) [Sun Jun 18 17:13:14 2006] SHOW_RESULT 1273 CPU : 0.51 = 0.5 + 0.01 + 0 + 0 # BOUND : makespan 1000 1273 MODIFY_CNF 1136 BEGIN : [Sun Jun 18 17:13:14 2006] MODIFY_CNF 1136 END : 72162006 bytes (0 seconds) [Sun Jun 18 17:13:14 2006] MODIFY_CNF 1136 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1136 BEGIN : [Sun Jun 18 17:13:14 2006] CMD : minisat /tmp/csp2sat10787.cnf /tmp/csp2sat10787.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1253193 3554390 | 417731 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 19 (4 /sec) decisions : 71 (14 /sec) propagations : 422154 (80564 /sec) conflict literals : 64 (7.25 % deleted) Memory used : 127.52 MB CPU time : 5.24 s UNSATISFIABLE VERIFY_CNF 1136 END : (5 seconds) [Sun Jun 18 17:13:19 2006] VERIFY_CNF 1136 CPU : 5.57 = 0 + 0 + 5.24 + 0.33 # RESULT : makespan 1136 UNSATISFIABLE # BOUND : makespan 1137 1273 MODIFY_CNF 1205 BEGIN : [Sun Jun 18 17:13:19 2006] MODIFY_CNF 1205 END : 72162006 bytes (0 seconds) [Sun Jun 18 17:13:19 2006] MODIFY_CNF 1205 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1205 BEGIN : [Sun Jun 18 17:13:19 2006] CMD : minisat /tmp/csp2sat10787.cnf /tmp/csp2sat10787.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1315017 3739862 | 438339 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (0 /sec) decisions : 219 (42 /sec) propagations : 215288 (41642 /sec) conflict literals : 7 (0.00 % deleted) Memory used : 128.43 MB CPU time : 5.17 s SATISFIABLE VERIFY_CNF 1205 END : (6 seconds) [Sun Jun 18 17:13:25 2006] VERIFY_CNF 1205 CPU : 5.7 = 0 + 0 + 5.28 + 0.42 # RESULT : makespan 1205 SATISFIABLE SHOW_RESULT 1205 BEGIN : [Sun Jun 18 17:13:25 2006] # ASSIGN : makespan 1205 # ASSIGN : s_0_0 364 # ASSIGN : s_0_1 33 # ASSIGN : s_0_2 154 # ASSIGN : s_0_3 1 # ASSIGN : s_0_4 3 # ASSIGN : s_0_5 2 # ASSIGN : s_0_6 559 # ASSIGN : s_0_7 205 # ASSIGN : s_1_0 22 # ASSIGN : s_1_1 1 # ASSIGN : s_1_2 273 # ASSIGN : s_1_3 10 # ASSIGN : s_1_4 982 # ASSIGN : s_1_5 21 # ASSIGN : s_1_6 52 # ASSIGN : s_1_7 206 # ASSIGN : s_2_0 751 # ASSIGN : s_2_1 154 # ASSIGN : s_2_2 28 # ASSIGN : s_2_3 12 # ASSIGN : s_2_4 79 # ASSIGN : s_2_5 22 # ASSIGN : s_2_6 149 # ASSIGN : s_2_7 207 # ASSIGN : s_3_0 13 # ASSIGN : s_3_1 156 # ASSIGN : s_3_2 43 # ASSIGN : s_3_3 21 # ASSIGN : s_3_4 80 # ASSIGN : s_3_5 23 # ASSIGN : s_3_6 150 # ASSIGN : s_3_7 725 # ASSIGN : s_4_0 16 # ASSIGN : s_4_1 155 # ASSIGN : s_4_2 164 # ASSIGN : s_4_3 171 # ASSIGN : s_4_4 1194 # ASSIGN : s_4_5 453 # ASSIGN : s_4_6 165 # ASSIGN : s_4_7 1156 # ASSIGN : s_5_0 21 # ASSIGN : s_5_1 827 # ASSIGN : s_5_2 928 # ASSIGN : s_5_3 658 # ASSIGN : s_5_4 1204 # ASSIGN : s_5_5 24 # ASSIGN : s_5_6 314 # ASSIGN : s_5_7 1193 # ASSIGN : s_6_0 45 # ASSIGN : s_6_1 606 # ASSIGN : s_6_2 212 # ASSIGN : s_6_3 768 # ASSIGN : s_6_4 228 # ASSIGN : s_6_5 1195 # ASSIGN : s_6_6 542 # ASSIGN : s_6_7 1197 # ASSIGN : s_7_0 100 # ASSIGN : s_7_1 1043 # ASSIGN : s_7_2 1198 # ASSIGN : s_7_3 408 # ASSIGN : s_7_4 620 # ASSIGN : s_7_5 1199 # ASSIGN : s_7_6 1200 # ASSIGN : s_7_7 1204 SHOW_RESULT 1205 END : 1205 (0 seconds) [Sun Jun 18 17:13:25 2006] SHOW_RESULT 1205 CPU : 0.519999999999996 = 0.519999999999996 + 0 + 0 + 0 # BOUND : makespan 1137 1205 MODIFY_CNF 1171 BEGIN : [Sun Jun 18 17:13:25 2006] MODIFY_CNF 1171 END : 72162006 bytes (0 seconds) [Sun Jun 18 17:13:25 2006] MODIFY_CNF 1171 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1171 BEGIN : [Sun Jun 18 17:13:25 2006] CMD : minisat /tmp/csp2sat10787.cnf /tmp/csp2sat10787.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1284553 3648470 | 428184 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 4 (1 /sec) decisions : 192 (37 /sec) propagations : 238901 (46031 /sec) conflict literals : 37 (7.50 % deleted) Memory used : 128.43 MB CPU time : 5.19 s SATISFIABLE VERIFY_CNF 1171 END : (6 seconds) [Sun Jun 18 17:13:31 2006] VERIFY_CNF 1171 CPU : 5.73 = 0 + 0.01 + 5.29 + 0.43 # RESULT : makespan 1171 SATISFIABLE SHOW_RESULT 1171 BEGIN : [Sun Jun 18 17:13:31 2006] # ASSIGN : makespan 1171 # ASSIGN : s_0_0 331 # ASSIGN : s_0_1 17 # ASSIGN : s_0_2 293 # ASSIGN : s_0_3 16 # ASSIGN : s_0_4 238 # ASSIGN : s_0_5 138 # ASSIGN : s_0_6 526 # ASSIGN : s_0_7 139 # ASSIGN : s_1_0 280 # ASSIGN : s_1_1 8 # ASSIGN : s_1_2 303 # ASSIGN : s_1_3 40 # ASSIGN : s_1_4 958 # ASSIGN : s_1_5 42 # ASSIGN : s_1_6 43 # ASSIGN : s_1_7 140 # ASSIGN : s_2_0 659 # ASSIGN : s_2_1 138 # ASSIGN : s_2_2 0 # ASSIGN : s_2_3 65 # ASSIGN : s_2_4 1170 # ASSIGN : s_2_5 139 # ASSIGN : s_2_6 140 # ASSIGN : s_2_7 141 # ASSIGN : s_3_0 0 # ASSIGN : s_3_1 237 # ASSIGN : s_3_2 1127 # ASSIGN : s_3_3 74 # ASSIGN : s_3_4 76 # ASSIGN : s_3_5 149 # ASSIGN : s_3_6 150 # ASSIGN : s_3_7 687 # ASSIGN : s_4_0 1113 # ASSIGN : s_4_1 145 # ASSIGN : s_4_2 15 # ASSIGN : s_4_3 876 # ASSIGN : s_4_4 146 # ASSIGN : s_4_5 162 # ASSIGN : s_4_6 156 # ASSIGN : s_4_7 1118 # ASSIGN : s_5_0 3 # ASSIGN : s_5_1 741 # ASSIGN : s_5_2 16 # ASSIGN : s_5_3 520 # ASSIGN : s_5_4 15 # ASSIGN : s_5_5 865 # ASSIGN : s_5_6 281 # ASSIGN : s_5_7 1155 # ASSIGN : s_6_0 589 # ASSIGN : s_6_1 997 # ASSIGN : s_6_2 981 # ASSIGN : s_6_3 82 # ASSIGN : s_6_4 644 # ASSIGN : s_6_5 80 # ASSIGN : s_6_6 509 # ASSIGN : s_6_7 1159 # ASSIGN : s_7_0 4 # ASSIGN : s_7_1 842 # ASSIGN : s_7_2 1164 # ASSIGN : s_7_3 630 # ASSIGN : s_7_4 268 # ASSIGN : s_7_5 1165 # ASSIGN : s_7_6 1167 # ASSIGN : s_7_7 1166 SHOW_RESULT 1171 END : 1171 (1 seconds) [Sun Jun 18 17:13:32 2006] SHOW_RESULT 1171 CPU : 0.510000000000005 = 0.510000000000005 + 0 + 0 + 0 # BOUND : makespan 1137 1171 MODIFY_CNF 1154 BEGIN : [Sun Jun 18 17:13:32 2006] MODIFY_CNF 1154 END : 72162006 bytes (0 seconds) [Sun Jun 18 17:13:32 2006] MODIFY_CNF 1154 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1154 BEGIN : [Sun Jun 18 17:13:32 2006] CMD : minisat /tmp/csp2sat10787.cnf /tmp/csp2sat10787.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1269321 3602774 | 423107 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 4 (1 /sec) decisions : 163 (30 /sec) propagations : 233896 (43556 /sec) conflict literals : 15 (6.25 % deleted) Memory used : 128.43 MB CPU time : 5.37 s SATISFIABLE VERIFY_CNF 1154 END : (6 seconds) [Sun Jun 18 17:13:38 2006] VERIFY_CNF 1154 CPU : 5.9 = 0 + 0.0099999999999999 + 5.46 + 0.43 # RESULT : makespan 1154 SATISFIABLE SHOW_RESULT 1154 BEGIN : [Sun Jun 18 17:13:38 2006] # ASSIGN : makespan 1154 # ASSIGN : s_0_0 55 # ASSIGN : s_0_1 1033 # ASSIGN : s_0_2 8 # ASSIGN : s_0_3 0 # ASSIGN : s_0_4 362 # ASSIGN : s_0_5 2 # ASSIGN : s_0_6 392 # ASSIGN : s_0_7 54 # ASSIGN : s_1_0 16 # ASSIGN : s_1_1 7 # ASSIGN : s_1_2 499 # ASSIGN : s_1_3 39 # ASSIGN : s_1_4 83 # ASSIGN : s_1_5 3 # ASSIGN : s_1_6 295 # ASSIGN : s_1_7 82 # ASSIGN : s_2_0 616 # ASSIGN : s_2_1 17 # ASSIGN : s_2_2 18 # ASSIGN : s_2_3 41 # ASSIGN : s_2_4 1 # ASSIGN : s_2_5 4 # ASSIGN : s_2_6 5 # ASSIGN : s_2_7 98 # ASSIGN : s_3_0 1070 # ASSIGN : s_3_1 175 # ASSIGN : s_3_2 95 # ASSIGN : s_3_3 1 # ASSIGN : s_3_4 3 # ASSIGN : s_3_5 132 # ASSIGN : s_3_6 1077 # ASSIGN : s_3_7 639 # ASSIGN : s_4_0 0 # ASSIGN : s_4_1 19 # ASSIGN : s_4_2 33 # ASSIGN : s_4_3 846 # ASSIGN : s_4_4 73 # ASSIGN : s_4_5 133 # ASSIGN : s_4_6 1083 # ASSIGN : s_4_7 1089 # ASSIGN : s_5_0 5 # ASSIGN : s_5_1 625 # ASSIGN : s_5_2 234 # ASSIGN : s_5_3 726 # ASSIGN : s_5_4 2 # ASSIGN : s_5_5 836 # ASSIGN : s_5_6 6 # ASSIGN : s_5_7 1126 # ASSIGN : s_6_0 1073 # ASSIGN : s_6_1 871 # ASSIGN : s_6_2 34 # ASSIGN : s_6_3 50 # ASSIGN : s_6_4 477 # ASSIGN : s_6_5 1128 # ASSIGN : s_6_6 1137 # ASSIGN : s_6_7 1130 # ASSIGN : s_7_0 250 # ASSIGN : s_7_1 20 # ASSIGN : s_7_2 233 # ASSIGN : s_7_3 514 # ASSIGN : s_7_4 791 # ASSIGN : s_7_5 19 # ASSIGN : s_7_6 246 # ASSIGN : s_7_7 1153 SHOW_RESULT 1154 END : 1154 (0 seconds) [Sun Jun 18 17:13:38 2006] SHOW_RESULT 1154 CPU : 0.509999999999991 = 0.509999999999991 + 0 + 0 + 0 # BOUND : makespan 1137 1154 MODIFY_CNF 1145 BEGIN : [Sun Jun 18 17:13:38 2006] MODIFY_CNF 1145 END : 72162006 bytes (0 seconds) [Sun Jun 18 17:13:38 2006] MODIFY_CNF 1145 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1145 BEGIN : [Sun Jun 18 17:13:38 2006] CMD : minisat /tmp/csp2sat10787.cnf /tmp/csp2sat10787.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1261257 3578582 | 420419 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 42 (7 /sec) decisions : 93 (16 /sec) propagations : 650216 (113081 /sec) conflict literals : 248 (21.27 % deleted) Memory used : 127.52 MB CPU time : 5.75 s UNSATISFIABLE VERIFY_CNF 1145 END : (6 seconds) [Sun Jun 18 17:13:44 2006] VERIFY_CNF 1145 CPU : 6.08 = 0 + 0.01 + 5.75 + 0.32 # RESULT : makespan 1145 UNSATISFIABLE # BOUND : makespan 1146 1154 MODIFY_CNF 1150 BEGIN : [Sun Jun 18 17:13:44 2006] MODIFY_CNF 1150 END : 72162006 bytes (0 seconds) [Sun Jun 18 17:13:44 2006] MODIFY_CNF 1150 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1150 BEGIN : [Sun Jun 18 17:13:44 2006] CMD : minisat /tmp/csp2sat10787.cnf /tmp/csp2sat10787.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1265737 3592022 | 421912 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 4 (1 /sec) decisions : 194 (37 /sec) propagations : 235373 (45004 /sec) conflict literals : 14 (0.00 % deleted) Memory used : 128.43 MB CPU time : 5.23 s SATISFIABLE VERIFY_CNF 1150 END : (6 seconds) [Sun Jun 18 17:13:50 2006] VERIFY_CNF 1150 CPU : 5.75 = 0 + 0 + 5.34 + 0.41 # RESULT : makespan 1150 SATISFIABLE SHOW_RESULT 1150 BEGIN : [Sun Jun 18 17:13:50 2006] # ASSIGN : makespan 1150 # ASSIGN : s_0_0 111 # ASSIGN : s_0_1 1029 # ASSIGN : s_0_2 5 # ASSIGN : s_0_3 1 # ASSIGN : s_0_4 358 # ASSIGN : s_0_5 2 # ASSIGN : s_0_6 388 # ASSIGN : s_0_7 95 # ASSIGN : s_1_0 55 # ASSIGN : s_1_1 12 # ASSIGN : s_1_2 495 # ASSIGN : s_1_3 4 # ASSIGN : s_1_4 79 # ASSIGN : s_1_5 3 # ASSIGN : s_1_6 291 # ASSIGN : s_1_7 78 # ASSIGN : s_2_0 614 # ASSIGN : s_2_1 21 # ASSIGN : s_2_2 81 # ASSIGN : s_2_3 22 # ASSIGN : s_2_4 0 # ASSIGN : s_2_5 7 # ASSIGN : s_2_6 1 # ASSIGN : s_2_7 96 # ASSIGN : s_3_0 3 # ASSIGN : s_3_1 187 # ASSIGN : s_3_2 150 # ASSIGN : s_3_3 6 # ASSIGN : s_3_4 9 # ASSIGN : s_3_5 8 # ASSIGN : s_3_6 1089 # ASSIGN : s_3_7 658 # ASSIGN : s_4_0 26 # ASSIGN : s_4_1 31 # ASSIGN : s_4_2 34 # ASSIGN : s_4_3 791 # ASSIGN : s_4_4 772 # ASSIGN : s_4_5 35 # ASSIGN : s_4_6 1095 # ASSIGN : s_4_7 1101 # ASSIGN : s_5_0 0 # ASSIGN : s_5_1 637 # ASSIGN : s_5_2 230 # ASSIGN : s_5_3 1028 # ASSIGN : s_5_4 1 # ASSIGN : s_5_5 738 # ASSIGN : s_5_6 2 # ASSIGN : s_5_7 1138 # ASSIGN : s_6_0 1068 # ASSIGN : s_6_1 867 # ASSIGN : s_6_2 15 # ASSIGN : s_6_3 31 # ASSIGN : s_6_4 458 # ASSIGN : s_6_5 1123 # ASSIGN : s_6_6 1125 # ASSIGN : s_6_7 1142 # ASSIGN : s_7_0 306 # ASSIGN : s_7_1 32 # ASSIGN : s_7_2 229 # ASSIGN : s_7_3 570 # ASSIGN : s_7_4 782 # ASSIGN : s_7_5 1144 # ASSIGN : s_7_6 1145 # ASSIGN : s_7_7 1149 SHOW_RESULT 1150 END : 1150 (0 seconds) [Sun Jun 18 17:13:50 2006] SHOW_RESULT 1150 CPU : 0.51 = 0.5 + 0.01 + 0 + 0 # BOUND : makespan 1146 1150 MODIFY_CNF 1148 BEGIN : [Sun Jun 18 17:13:50 2006] MODIFY_CNF 1148 END : 72162006 bytes (0 seconds) [Sun Jun 18 17:13:50 2006] MODIFY_CNF 1148 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1148 BEGIN : [Sun Jun 18 17:13:50 2006] CMD : minisat /tmp/csp2sat10787.cnf /tmp/csp2sat10787.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1263945 3586646 | 421315 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 3 (1 /sec) decisions : 180 (34 /sec) propagations : 224739 (42971 /sec) conflict literals : 13 (0.00 % deleted) Memory used : 128.43 MB CPU time : 5.23 s SATISFIABLE VERIFY_CNF 1148 END : (6 seconds) [Sun Jun 18 17:13:56 2006] VERIFY_CNF 1148 CPU : 5.76 = 0 + 0.01 + 5.31 + 0.44 # RESULT : makespan 1148 SATISFIABLE SHOW_RESULT 1148 BEGIN : [Sun Jun 18 17:13:56 2006] # ASSIGN : makespan 1148 # ASSIGN : s_0_0 64 # ASSIGN : s_0_1 1025 # ASSIGN : s_0_2 53 # ASSIGN : s_0_3 0 # ASSIGN : s_0_4 354 # ASSIGN : s_0_5 63 # ASSIGN : s_0_6 384 # ASSIGN : s_0_7 1146 # ASSIGN : s_1_0 36 # ASSIGN : s_1_1 15 # ASSIGN : s_1_2 493 # ASSIGN : s_1_3 1 # ASSIGN : s_1_4 75 # ASSIGN : s_1_5 73 # ASSIGN : s_1_6 287 # ASSIGN : s_1_7 74 # ASSIGN : s_2_0 611 # ASSIGN : s_2_1 24 # ASSIGN : s_2_2 2 # ASSIGN : s_2_3 25 # ASSIGN : s_2_4 1 # ASSIGN : s_2_5 92 # ASSIGN : s_2_6 1085 # ASSIGN : s_2_7 93 # ASSIGN : s_3_0 0 # ASSIGN : s_3_1 184 # ASSIGN : s_3_2 104 # ASSIGN : s_3_3 3 # ASSIGN : s_3_4 5 # ASSIGN : s_3_5 141 # ASSIGN : s_3_6 1086 # ASSIGN : s_3_7 655 # ASSIGN : s_4_0 59 # ASSIGN : s_4_1 28 # ASSIGN : s_4_2 17 # ASSIGN : s_4_3 855 # ASSIGN : s_4_4 1137 # ASSIGN : s_4_5 142 # ASSIGN : s_4_6 1092 # ASSIGN : s_4_7 1098 # ASSIGN : s_5_0 610 # ASSIGN : s_5_1 634 # ASSIGN : s_5_2 228 # ASSIGN : s_5_3 735 # ASSIGN : s_5_4 1147 # ASSIGN : s_5_5 845 # ASSIGN : s_5_6 0 # ASSIGN : s_5_7 1135 # ASSIGN : s_6_0 1065 # ASSIGN : s_6_1 863 # ASSIGN : s_6_2 18 # ASSIGN : s_6_3 34 # ASSIGN : s_6_4 461 # ASSIGN : s_6_5 1137 # ASSIGN : s_6_6 1120 # ASSIGN : s_6_7 1139 # ASSIGN : s_7_0 259 # ASSIGN : s_7_1 29 # ASSIGN : s_7_2 227 # ASSIGN : s_7_3 523 # ASSIGN : s_7_4 775 # ASSIGN : s_7_5 1142 # ASSIGN : s_7_6 1143 # ASSIGN : s_7_7 1147 SHOW_RESULT 1148 END : 1148 (1 seconds) [Sun Jun 18 17:13:57 2006] SHOW_RESULT 1148 CPU : 0.510000000000005 = 0.510000000000005 + 0 + 0 + 0 # BOUND : makespan 1146 1148 MODIFY_CNF 1147 BEGIN : [Sun Jun 18 17:13:57 2006] MODIFY_CNF 1147 END : 72162006 bytes (0 seconds) [Sun Jun 18 17:13:57 2006] MODIFY_CNF 1147 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1147 BEGIN : [Sun Jun 18 17:13:57 2006] CMD : minisat /tmp/csp2sat10787.cnf /tmp/csp2sat10787.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1263049 3583958 | 421016 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 29 (5 /sec) decisions : 84 (16 /sec) propagations : 410965 (76388 /sec) conflict literals : 132 (16.46 % deleted) Memory used : 127.52 MB CPU time : 5.38 s UNSATISFIABLE VERIFY_CNF 1147 END : (5 seconds) [Sun Jun 18 17:14:02 2006] VERIFY_CNF 1147 CPU : 5.77 = 0 + 0 + 5.38 + 0.39 # RESULT : makespan 1147 UNSATISFIABLE # BOUND : makespan 1148 1148 MAIN END : (183 seconds) [Sun Jun 18 17:14:02 2006] MAIN CPU : 183.21 = 120.49 + 0.59 + 57.74 + 4.39