# TIMEOUT 18000 MAIN BEGIN : [Sun Jun 18 16:32:08 2006] READ BEGIN : csp/gp07-04.csp [Sun Jun 18 16:32:08 2006] READ END : csp/gp07-04.csp (1 seconds) [Sun Jun 18 16:32:09 2006] READ CPU : 0.64 = 0.62 + 0.02 + 0 + 0 # BOUND : makespan 1000 3534 GENERATE_CNF 3534 BEGIN : [Sun Jun 18 16:32:09 2006] GENERATE_CNF 3534 END : 176437 variables 2295576 clauses 52962656 bytes (87 seconds) [Sun Jun 18 16:33:36 2006] GENERATE_CNF 3534 CPU : 86.97 = 86.56 + 0.41 + 0 + 0 MODIFY_CNF 2267 BEGIN : [Sun Jun 18 16:33:36 2006] MODIFY_CNF 2267 END : 52962663 bytes (0 seconds) [Sun Jun 18 16:33:36 2006] MODIFY_CNF 2267 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 2267 BEGIN : [Sun Jun 18 16:33:36 2006] CMD : minisat /tmp/csp2sat10026.cnf /tmp/csp2sat10026.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1549644 4473924 | 516548 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (1 /sec) decisions : 255 (81 /sec) propagations : 181581 (57462 /sec) conflict literals : 20 (0.00 % deleted) Memory used : 100.32 MB CPU time : 3.16 s SATISFIABLE VERIFY_CNF 2267 END : (4 seconds) [Sun Jun 18 16:33:40 2006] VERIFY_CNF 2267 CPU : 3.48 = 0 + 0 + 3.25 + 0.23 # RESULT : makespan 2267 SATISFIABLE SHOW_RESULT 2267 BEGIN : [Sun Jun 18 16:33:40 2006] # ASSIGN : makespan 2267 # ASSIGN : s_0_0 20 # ASSIGN : s_0_1 79 # ASSIGN : s_0_2 80 # ASSIGN : s_0_3 450 # ASSIGN : s_0_4 455 # ASSIGN : s_0_5 1266 # ASSIGN : s_0_6 1267 # ASSIGN : s_1_0 21 # ASSIGN : s_1_1 82 # ASSIGN : s_1_2 81 # ASSIGN : s_1_3 881 # ASSIGN : s_1_4 754 # ASSIGN : s_1_5 1267 # ASSIGN : s_1_6 1959 # ASSIGN : s_2_0 49 # ASSIGN : s_2_1 793 # ASSIGN : s_2_2 267 # ASSIGN : s_2_3 1086 # ASSIGN : s_2_4 756 # ASSIGN : s_2_5 1358 # ASSIGN : s_2_6 1960 # ASSIGN : s_3_0 60 # ASSIGN : s_3_1 979 # ASSIGN : s_3_2 732 # ASSIGN : s_3_3 1114 # ASSIGN : s_3_4 763 # ASSIGN : s_3_5 1360 # ASSIGN : s_3_6 2261 # ASSIGN : s_4_0 426 # ASSIGN : s_4_1 1251 # ASSIGN : s_4_2 733 # ASSIGN : s_4_3 1252 # ASSIGN : s_4_4 1502 # ASSIGN : s_4_5 1503 # ASSIGN : s_4_6 2262 # ASSIGN : s_5_0 1415 # ASSIGN : s_5_1 1264 # ASSIGN : s_5_2 734 # ASSIGN : s_5_3 1267 # ASSIGN : s_5_4 1701 # ASSIGN : s_5_5 2175 # ASSIGN : s_5_6 2265 # ASSIGN : s_6_0 1876 # ASSIGN : s_6_1 1267 # ASSIGN : s_6_2 1269 # ASSIGN : s_6_3 1270 # ASSIGN : s_6_4 1877 # ASSIGN : s_6_5 2176 # ASSIGN : s_6_6 2266 SHOW_RESULT 2267 END : 2267 (0 seconds) [Sun Jun 18 16:33:40 2006] SHOW_RESULT 2267 CPU : 0.349999999999998 = 0.329999999999998 + 0.02 + 0 + 0 # BOUND : makespan 1000 2267 MODIFY_CNF 1633 BEGIN : [Sun Jun 18 16:33:40 2006] MODIFY_CNF 1633 END : 52962662 bytes (0 seconds) [Sun Jun 18 16:33:40 2006] MODIFY_CNF 1633 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1633 BEGIN : [Sun Jun 18 16:33:40 2006] CMD : minisat /tmp/csp2sat10026.cnf /tmp/csp2sat10026.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1176852 3355548 | 392284 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 5 (1 /sec) decisions : 221 (64 /sec) propagations : 214543 (62549 /sec) conflict literals : 81 (11.96 % deleted) Memory used : 100.32 MB CPU time : 3.43 s SATISFIABLE VERIFY_CNF 1633 END : (4 seconds) [Sun Jun 18 16:33:44 2006] VERIFY_CNF 1633 CPU : 3.89 = 0 + 0 + 3.52 + 0.37 # RESULT : makespan 1633 SATISFIABLE SHOW_RESULT 1633 BEGIN : [Sun Jun 18 16:33:44 2006] # ASSIGN : makespan 1633 # ASSIGN : s_0_0 1604 # ASSIGN : s_0_1 467 # ASSIGN : s_0_2 15 # ASSIGN : s_0_3 16 # ASSIGN : s_0_4 22 # ASSIGN : s_0_5 21 # ASSIGN : s_0_6 633 # ASSIGN : s_1_0 1605 # ASSIGN : s_1_1 468 # ASSIGN : s_1_2 24 # ASSIGN : s_1_3 25 # ASSIGN : s_1_4 321 # ASSIGN : s_1_5 230 # ASSIGN : s_1_6 1325 # ASSIGN : s_2_0 27 # ASSIGN : s_2_1 1140 # ASSIGN : s_2_2 396 # ASSIGN : s_2_3 295 # ASSIGN : s_2_4 323 # ASSIGN : s_2_5 330 # ASSIGN : s_2_6 1326 # ASSIGN : s_3_0 1034 # ASSIGN : s_3_1 1400 # ASSIGN : s_3_2 861 # ASSIGN : s_3_3 475 # ASSIGN : s_3_4 613 # ASSIGN : s_3_5 332 # ASSIGN : s_3_6 1627 # ASSIGN : s_4_0 38 # ASSIGN : s_4_1 1535 # ASSIGN : s_4_2 862 # ASSIGN : s_4_3 616 # ASSIGN : s_4_4 829 # ASSIGN : s_4_5 863 # ASSIGN : s_4_6 1628 # ASSIGN : s_5_0 345 # ASSIGN : s_5_1 1536 # ASSIGN : s_5_2 1006 # ASSIGN : s_5_3 631 # ASSIGN : s_5_4 830 # ASSIGN : s_5_5 1541 # ASSIGN : s_5_6 1631 # ASSIGN : s_6_0 633 # ASSIGN : s_6_1 1539 # ASSIGN : s_6_2 1541 # ASSIGN : s_6_3 634 # ASSIGN : s_6_4 1240 # ASSIGN : s_6_5 1542 # ASSIGN : s_6_6 1632 SHOW_RESULT 1633 END : 1633 (0 seconds) [Sun Jun 18 16:33:44 2006] SHOW_RESULT 1633 CPU : 0.370000000000005 = 0.370000000000005 + 0 + 0 + 0 # BOUND : makespan 1000 1633 MODIFY_CNF 1316 BEGIN : [Sun Jun 18 16:33:44 2006] MODIFY_CNF 1316 END : 52962662 bytes (0 seconds) [Sun Jun 18 16:33:44 2006] MODIFY_CNF 1316 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1316 BEGIN : [Sun Jun 18 16:33:44 2006] CMD : minisat /tmp/csp2sat10026.cnf /tmp/csp2sat10026.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 990456 2796360 | 330152 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 162 (48 /sec) propagations : 176437 (51741 /sec) conflict literals : 0 ( nan % deleted) Memory used : 100.32 MB CPU time : 3.41 s SATISFIABLE VERIFY_CNF 1316 END : (4 seconds) [Sun Jun 18 16:33:48 2006] VERIFY_CNF 1316 CPU : 3.86 = 0 + 0 + 3.47 + 0.39 # RESULT : makespan 1316 SATISFIABLE SHOW_RESULT 1316 BEGIN : [Sun Jun 18 16:33:48 2006] # ASSIGN : makespan 1316 # ASSIGN : s_0_0 3 # ASSIGN : s_0_1 4 # ASSIGN : s_0_2 5 # ASSIGN : s_0_3 6 # ASSIGN : s_0_4 17 # ASSIGN : s_0_5 16 # ASSIGN : s_0_6 316 # ASSIGN : s_1_0 15 # ASSIGN : s_1_1 336 # ASSIGN : s_1_2 11 # ASSIGN : s_1_3 1111 # ASSIGN : s_1_4 320 # ASSIGN : s_1_5 43 # ASSIGN : s_1_6 1008 # ASSIGN : s_2_0 123 # ASSIGN : s_2_1 136 # ASSIGN : s_2_2 544 # ASSIGN : s_2_3 20 # ASSIGN : s_2_4 322 # ASSIGN : s_2_5 134 # ASSIGN : s_2_6 1009 # ASSIGN : s_3_0 567 # ASSIGN : s_3_1 1083 # ASSIGN : s_3_2 12 # ASSIGN : s_3_3 48 # ASSIGN : s_3_4 329 # ASSIGN : s_3_5 186 # ASSIGN : s_3_6 1310 # ASSIGN : s_4_0 238 # ASSIGN : s_4_1 1218 # ASSIGN : s_4_2 13 # ASSIGN : s_4_3 223 # ASSIGN : s_4_4 545 # ASSIGN : s_4_5 546 # ASSIGN : s_4_6 1311 # ASSIGN : s_5_0 933 # ASSIGN : s_5_1 1219 # ASSIGN : s_5_2 14 # ASSIGN : s_5_3 11 # ASSIGN : s_5_4 746 # ASSIGN : s_5_5 1224 # ASSIGN : s_5_6 1314 # ASSIGN : s_6_0 1221 # ASSIGN : s_6_1 1222 # ASSIGN : s_6_2 1224 # ASSIGN : s_6_3 316 # ASSIGN : s_6_4 922 # ASSIGN : s_6_5 1225 # ASSIGN : s_6_6 1315 SHOW_RESULT 1316 END : 1316 (1 seconds) [Sun Jun 18 16:33:49 2006] SHOW_RESULT 1316 CPU : 0.350000000000003 = 0.340000000000003 + 0.01 + 0 + 0 # BOUND : makespan 1000 1316 MODIFY_CNF 1158 BEGIN : [Sun Jun 18 16:33:49 2006] MODIFY_CNF 1158 END : 52962662 bytes (0 seconds) [Sun Jun 18 16:33:49 2006] MODIFY_CNF 1158 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1158 BEGIN : [Sun Jun 18 16:33:49 2006] CMD : minisat /tmp/csp2sat10026.cnf /tmp/csp2sat10026.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 897552 2517648 | 299184 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (1 /sec) decisions : 20 (6 /sec) propagations : 133721 (40277 /sec) conflict literals : 1 (0.00 % deleted) Memory used : 99.47 MB CPU time : 3.32 s UNSATISFIABLE VERIFY_CNF 1158 END : (3 seconds) [Sun Jun 18 16:33:52 2006] VERIFY_CNF 1158 CPU : 3.7 = 0 + 0 + 3.32 + 0.38 # RESULT : makespan 1158 UNSATISFIABLE # BOUND : makespan 1159 1316 MODIFY_CNF 1237 BEGIN : [Sun Jun 18 16:33:52 2006] MODIFY_CNF 1237 END : 52962662 bytes (0 seconds) [Sun Jun 18 16:33:52 2006] MODIFY_CNF 1237 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1237 BEGIN : [Sun Jun 18 16:33:52 2006] CMD : minisat /tmp/csp2sat10026.cnf /tmp/csp2sat10026.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 944004 2657004 | 314668 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 1 (0 /sec) decisions : 161 (48 /sec) propagations : 178551 (53780 /sec) conflict literals : 4 (0.00 % deleted) Memory used : 100.32 MB CPU time : 3.32 s SATISFIABLE VERIFY_CNF 1237 END : (4 seconds) [Sun Jun 18 16:33:56 2006] VERIFY_CNF 1237 CPU : 3.71 = 0 + 0 + 3.39 + 0.32 # RESULT : makespan 1237 SATISFIABLE SHOW_RESULT 1237 BEGIN : [Sun Jun 18 16:33:56 2006] # ASSIGN : makespan 1237 # ASSIGN : s_0_0 7 # ASSIGN : s_0_1 8 # ASSIGN : s_0_2 9 # ASSIGN : s_0_3 10 # ASSIGN : s_0_4 938 # ASSIGN : s_0_5 76 # ASSIGN : s_0_6 237 # ASSIGN : s_1_0 895 # ASSIGN : s_1_1 18 # ASSIGN : s_1_2 12 # ASSIGN : s_1_3 690 # ASSIGN : s_1_4 16 # ASSIGN : s_1_5 1051 # ASSIGN : s_1_6 929 # ASSIGN : s_2_0 129 # ASSIGN : s_2_1 716 # ASSIGN : s_2_2 147 # ASSIGN : s_2_3 902 # ASSIGN : s_2_4 140 # ASSIGN : s_2_5 1235 # ASSIGN : s_2_6 930 # ASSIGN : s_3_0 529 # ASSIGN : s_3_1 958 # ASSIGN : s_3_2 13 # ASSIGN : s_3_3 1093 # ASSIGN : s_3_4 220 # ASSIGN : s_3_5 77 # ASSIGN : s_3_6 1231 # ASSIGN : s_4_0 923 # ASSIGN : s_4_1 1230 # ASSIGN : s_4_2 14 # ASSIGN : s_4_3 15 # ASSIGN : s_4_4 219 # ASSIGN : s_4_5 251 # ASSIGN : s_4_6 1232 # ASSIGN : s_5_0 150 # ASSIGN : s_5_1 1231 # ASSIGN : s_5_2 612 # ASSIGN : s_5_3 30 # ASSIGN : s_5_4 436 # ASSIGN : s_5_5 1142 # ASSIGN : s_5_6 1235 # ASSIGN : s_6_0 1233 # ASSIGN : s_6_1 1234 # ASSIGN : s_6_2 1142 # ASSIGN : s_6_3 33 # ASSIGN : s_6_4 639 # ASSIGN : s_6_5 1143 # ASSIGN : s_6_6 1236 SHOW_RESULT 1237 END : 1237 (0 seconds) [Sun Jun 18 16:33:56 2006] SHOW_RESULT 1237 CPU : 0.359999999999999 = 0.359999999999999 + 0 + 0 + 0 # BOUND : makespan 1159 1237 MODIFY_CNF 1198 BEGIN : [Sun Jun 18 16:33:56 2006] MODIFY_CNF 1198 END : 52962662 bytes (0 seconds) [Sun Jun 18 16:33:56 2006] MODIFY_CNF 1198 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1198 BEGIN : [Sun Jun 18 16:33:56 2006] CMD : minisat /tmp/csp2sat10026.cnf /tmp/csp2sat10026.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 921072 2588208 | 307024 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (1 /sec) decisions : 133 (39 /sec) propagations : 194519 (57380 /sec) conflict literals : 20 (28.57 % deleted) Memory used : 100.32 MB CPU time : 3.39 s SATISFIABLE VERIFY_CNF 1198 END : (4 seconds) [Sun Jun 18 16:34:00 2006] VERIFY_CNF 1198 CPU : 3.76 = 0 + 0 + 3.49 + 0.27 # RESULT : makespan 1198 SATISFIABLE SHOW_RESULT 1198 BEGIN : [Sun Jun 18 16:34:00 2006] # ASSIGN : makespan 1198 # ASSIGN : s_0_0 0 # ASSIGN : s_0_1 9 # ASSIGN : s_0_2 10 # ASSIGN : s_0_3 1 # ASSIGN : s_0_4 899 # ASSIGN : s_0_5 6 # ASSIGN : s_0_6 11 # ASSIGN : s_1_0 1166 # ASSIGN : s_1_1 31 # ASSIGN : s_1_2 28 # ASSIGN : s_1_3 961 # ASSIGN : s_1_4 29 # ASSIGN : s_1_5 870 # ASSIGN : s_1_6 703 # ASSIGN : s_2_0 693 # ASSIGN : s_2_1 1005 # ASSIGN : s_2_2 108 # ASSIGN : s_2_3 80 # ASSIGN : s_2_4 647 # ASSIGN : s_2_5 4 # ASSIGN : s_2_6 704 # ASSIGN : s_3_0 288 # ASSIGN : s_3_1 870 # ASSIGN : s_3_2 1191 # ASSIGN : s_3_3 150 # ASSIGN : s_3_4 654 # ASSIGN : s_3_5 7 # ASSIGN : s_3_6 1192 # ASSIGN : s_4_0 859 # ASSIGN : s_4_1 1191 # ASSIGN : s_4_2 54 # ASSIGN : s_4_3 1176 # ASSIGN : s_4_4 55 # ASSIGN : s_4_5 187 # ASSIGN : s_4_6 1193 # ASSIGN : s_5_0 2 # ASSIGN : s_5_1 1192 # ASSIGN : s_5_2 573 # ASSIGN : s_5_3 352 # ASSIGN : s_5_4 397 # ASSIGN : s_5_5 1103 # ASSIGN : s_5_6 1196 # ASSIGN : s_6_0 1194 # ASSIGN : s_6_1 1195 # ASSIGN : s_6_2 55 # ASSIGN : s_6_3 355 # ASSIGN : s_6_4 56 # ASSIGN : s_6_5 1104 # ASSIGN : s_6_6 1197 SHOW_RESULT 1198 END : 1198 (1 seconds) [Sun Jun 18 16:34:01 2006] SHOW_RESULT 1198 CPU : 0.359999999999999 = 0.359999999999999 + 0 + 0 + 0 # BOUND : makespan 1159 1198 MODIFY_CNF 1178 BEGIN : [Sun Jun 18 16:34:01 2006] MODIFY_CNF 1178 END : 52962662 bytes (0 seconds) [Sun Jun 18 16:34:01 2006] MODIFY_CNF 1178 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1178 BEGIN : [Sun Jun 18 16:34:01 2006] CMD : minisat /tmp/csp2sat10026.cnf /tmp/csp2sat10026.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 909312 2552928 | 303104 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 129 (40 /sec) propagations : 176437 (54288 /sec) conflict literals : 0 ( nan % deleted) Memory used : 100.32 MB CPU time : 3.25 s SATISFIABLE VERIFY_CNF 1178 END : (3 seconds) [Sun Jun 18 16:34:04 2006] VERIFY_CNF 1178 CPU : 3.75 = 0 + 0 + 3.35 + 0.4 # RESULT : makespan 1178 SATISFIABLE SHOW_RESULT 1178 BEGIN : [Sun Jun 18 16:34:04 2006] # ASSIGN : makespan 1178 # ASSIGN : s_0_0 835 # ASSIGN : s_0_1 6 # ASSIGN : s_0_2 7 # ASSIGN : s_0_3 8 # ASSIGN : s_0_4 879 # ASSIGN : s_0_5 13 # ASSIGN : s_0_6 143 # ASSIGN : s_1_0 836 # ASSIGN : s_1_1 13 # ASSIGN : s_1_2 10 # ASSIGN : s_1_3 973 # ASSIGN : s_1_4 11 # ASSIGN : s_1_5 882 # ASSIGN : s_1_6 870 # ASSIGN : s_2_0 0 # ASSIGN : s_2_1 685 # ASSIGN : s_2_2 88 # ASSIGN : s_2_3 24 # ASSIGN : s_2_4 60 # ASSIGN : s_2_5 14 # ASSIGN : s_2_6 871 # ASSIGN : s_3_0 297 # ASSIGN : s_3_1 1036 # ASSIGN : s_3_2 15 # ASSIGN : s_3_3 159 # ASSIGN : s_3_4 663 # ASSIGN : s_3_5 16 # ASSIGN : s_3_6 1172 # ASSIGN : s_4_0 864 # ASSIGN : s_4_1 1171 # ASSIGN : s_4_2 51 # ASSIGN : s_4_3 52 # ASSIGN : s_4_4 67 # ASSIGN : s_4_5 192 # ASSIGN : s_4_6 1173 # ASSIGN : s_5_0 11 # ASSIGN : s_5_1 1172 # ASSIGN : s_5_2 553 # ASSIGN : s_5_3 364 # ASSIGN : s_5_4 377 # ASSIGN : s_5_5 1083 # ASSIGN : s_5_6 1176 # ASSIGN : s_6_0 1174 # ASSIGN : s_6_1 1175 # ASSIGN : s_6_2 1083 # ASSIGN : s_6_3 367 # ASSIGN : s_6_4 68 # ASSIGN : s_6_5 1084 # ASSIGN : s_6_6 1177 SHOW_RESULT 1178 END : 1178 (1 seconds) [Sun Jun 18 16:34:05 2006] SHOW_RESULT 1178 CPU : 0.359999999999998 = 0.329999999999998 + 0.03 + 0 + 0 # BOUND : makespan 1159 1178 MODIFY_CNF 1168 BEGIN : [Sun Jun 18 16:34:05 2006] MODIFY_CNF 1168 END : 52962662 bytes (0 seconds) [Sun Jun 18 16:34:05 2006] MODIFY_CNF 1168 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1168 BEGIN : [Sun Jun 18 16:34:05 2006] CMD : minisat /tmp/csp2sat10026.cnf /tmp/csp2sat10026.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 903432 2535288 | 301144 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 92 (27 /sec) propagations : 176437 (51893 /sec) conflict literals : 0 ( nan % deleted) Memory used : 100.32 MB CPU time : 3.4 s SATISFIABLE VERIFY_CNF 1168 END : (3 seconds) [Sun Jun 18 16:34:08 2006] VERIFY_CNF 1168 CPU : 3.76 = 0 + 0 + 3.48 + 0.28 # RESULT : makespan 1168 SATISFIABLE SHOW_RESULT 1168 BEGIN : [Sun Jun 18 16:34:08 2006] # ASSIGN : makespan 1168 # ASSIGN : s_0_0 0 # ASSIGN : s_0_1 2 # ASSIGN : s_0_2 1 # ASSIGN : s_0_3 9 # ASSIGN : s_0_4 869 # ASSIGN : s_0_5 3 # ASSIGN : s_0_6 168 # ASSIGN : s_1_0 826 # ASSIGN : s_1_1 3 # ASSIGN : s_1_2 2 # ASSIGN : s_1_3 963 # ASSIGN : s_1_4 0 # ASSIGN : s_1_5 872 # ASSIGN : s_1_6 860 # ASSIGN : s_2_0 664 # ASSIGN : s_2_1 675 # ASSIGN : s_2_2 78 # ASSIGN : s_2_3 14 # ASSIGN : s_2_4 50 # ASSIGN : s_2_5 4 # ASSIGN : s_2_6 861 # ASSIGN : s_3_0 287 # ASSIGN : s_3_1 1026 # ASSIGN : s_3_2 5 # ASSIGN : s_3_3 149 # ASSIGN : s_3_4 653 # ASSIGN : s_3_5 6 # ASSIGN : s_3_6 1162 # ASSIGN : s_4_0 854 # ASSIGN : s_4_1 1161 # ASSIGN : s_4_2 41 # ASSIGN : s_4_3 42 # ASSIGN : s_4_4 57 # ASSIGN : s_4_5 182 # ASSIGN : s_4_6 1163 # ASSIGN : s_5_0 1 # ASSIGN : s_5_1 1162 # ASSIGN : s_5_2 543 # ASSIGN : s_5_3 354 # ASSIGN : s_5_4 367 # ASSIGN : s_5_5 1073 # ASSIGN : s_5_6 1166 # ASSIGN : s_6_0 1164 # ASSIGN : s_6_1 1165 # ASSIGN : s_6_2 1073 # ASSIGN : s_6_3 357 # ASSIGN : s_6_4 58 # ASSIGN : s_6_5 1074 # ASSIGN : s_6_6 1167 SHOW_RESULT 1168 END : 1168 (1 seconds) [Sun Jun 18 16:34:09 2006] SHOW_RESULT 1168 CPU : 0.360000000000009 = 0.350000000000009 + 0.01 + 0 + 0 # BOUND : makespan 1159 1168 MODIFY_CNF 1163 BEGIN : [Sun Jun 18 16:34:09 2006] MODIFY_CNF 1163 END : 52962662 bytes (0 seconds) [Sun Jun 18 16:34:09 2006] MODIFY_CNF 1163 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1163 BEGIN : [Sun Jun 18 16:34:09 2006] CMD : minisat /tmp/csp2sat10026.cnf /tmp/csp2sat10026.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 900492 2526468 | 300164 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 3 (1 /sec) decisions : 20 (6 /sec) propagations : 147316 (44913 /sec) conflict literals : 3 (0.00 % deleted) Memory used : 99.49 MB CPU time : 3.28 s UNSATISFIABLE VERIFY_CNF 1163 END : (3 seconds) [Sun Jun 18 16:34:12 2006] VERIFY_CNF 1163 CPU : 3.6 = 0 + 0 + 3.28 + 0.32 # RESULT : makespan 1163 UNSATISFIABLE # BOUND : makespan 1164 1168 MODIFY_CNF 1166 BEGIN : [Sun Jun 18 16:34:12 2006] MODIFY_CNF 1166 END : 52962662 bytes (0 seconds) [Sun Jun 18 16:34:12 2006] MODIFY_CNF 1166 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1166 BEGIN : [Sun Jun 18 16:34:12 2006] CMD : minisat /tmp/csp2sat10026.cnf /tmp/csp2sat10026.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 902256 2531760 | 300752 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (1 /sec) decisions : 20 (6 /sec) propagations : 144621 (44092 /sec) conflict literals : 1 (0.00 % deleted) Memory used : 99.50 MB CPU time : 3.28 s UNSATISFIABLE VERIFY_CNF 1166 END : (4 seconds) [Sun Jun 18 16:34:16 2006] VERIFY_CNF 1166 CPU : 3.59 = 0 + 0 + 3.28 + 0.31 # RESULT : makespan 1166 UNSATISFIABLE # BOUND : makespan 1167 1168 MODIFY_CNF 1167 BEGIN : [Sun Jun 18 16:34:16 2006] MODIFY_CNF 1167 END : 52962662 bytes (0 seconds) [Sun Jun 18 16:34:16 2006] MODIFY_CNF 1167 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1167 BEGIN : [Sun Jun 18 16:34:16 2006] CMD : minisat /tmp/csp2sat10026.cnf /tmp/csp2sat10026.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 902844 2533524 | 300948 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 82 (25 /sec) propagations : 176437 (53304 /sec) conflict literals : 0 ( nan % deleted) Memory used : 100.32 MB CPU time : 3.31 s SATISFIABLE VERIFY_CNF 1167 END : (4 seconds) [Sun Jun 18 16:34:20 2006] VERIFY_CNF 1167 CPU : 3.75 = 0 + 0 + 3.4 + 0.35 # RESULT : makespan 1167 SATISFIABLE SHOW_RESULT 1167 BEGIN : [Sun Jun 18 16:34:20 2006] # ASSIGN : makespan 1167 # ASSIGN : s_0_0 823 # ASSIGN : s_0_1 0 # ASSIGN : s_0_2 1 # ASSIGN : s_0_3 5 # ASSIGN : s_0_4 868 # ASSIGN : s_0_5 2 # ASSIGN : s_0_6 131 # ASSIGN : s_1_0 824 # ASSIGN : s_1_1 2 # ASSIGN : s_1_2 1164 # ASSIGN : s_1_3 959 # ASSIGN : s_1_4 0 # ASSIGN : s_1_5 868 # ASSIGN : s_1_6 859 # ASSIGN : s_2_0 663 # ASSIGN : s_2_1 674 # ASSIGN : s_2_2 76 # ASSIGN : s_2_3 10 # ASSIGN : s_2_4 46 # ASSIGN : s_2_5 3 # ASSIGN : s_2_6 860 # ASSIGN : s_3_0 286 # ASSIGN : s_3_1 1024 # ASSIGN : s_3_2 4 # ASSIGN : s_3_3 148 # ASSIGN : s_3_4 652 # ASSIGN : s_3_5 5 # ASSIGN : s_3_6 1161 # ASSIGN : s_4_0 852 # ASSIGN : s_4_1 1159 # ASSIGN : s_4_2 37 # ASSIGN : s_4_3 38 # ASSIGN : s_4_4 53 # ASSIGN : s_4_5 180 # ASSIGN : s_4_6 1162 # ASSIGN : s_5_0 0 # ASSIGN : s_5_1 1160 # ASSIGN : s_5_2 541 # ASSIGN : s_5_3 350 # ASSIGN : s_5_4 365 # ASSIGN : s_5_5 1071 # ASSIGN : s_5_6 1165 # ASSIGN : s_6_0 1162 # ASSIGN : s_6_1 1163 # ASSIGN : s_6_2 1165 # ASSIGN : s_6_3 353 # ASSIGN : s_6_4 54 # ASSIGN : s_6_5 1072 # ASSIGN : s_6_6 1166 SHOW_RESULT 1167 END : 1167 (0 seconds) [Sun Jun 18 16:34:20 2006] SHOW_RESULT 1167 CPU : 0.450000000000003 = 0.450000000000003 + 0 + 0 + 0 # BOUND : makespan 1167 1167 MAIN END : (132 seconds) [Sun Jun 18 16:34:20 2006] MAIN CPU : 131.47 = 90.11 + 0.51 + 37.23 + 3.62