# TIMEOUT 18000 MAIN BEGIN : [Sun Jun 18 19:48:20 2006] READ BEGIN : csp/j4-per0-2.csp [Sun Jun 18 19:48:20 2006] READ END : csp/j4-per0-2.csp (0 seconds) [Sun Jun 18 19:48:20 2006] READ CPU : 0.12 = 0.12 + 0 + 0 + 0 # BOUND : makespan 1000 1583 GENERATE_CNF 1583 BEGIN : [Sun Jun 18 19:48:20 2006] GENERATE_CNF 1583 END : 26057 variables 163530 clauses 3270138 bytes (6 seconds) [Sun Jun 18 19:48:26 2006] GENERATE_CNF 1583 CPU : 5.92 = 5.87 + 0.05 + 0 + 0 MODIFY_CNF 1291 BEGIN : [Sun Jun 18 19:48:26 2006] MODIFY_CNF 1291 END : 3270144 bytes (0 seconds) [Sun Jun 18 19:48:26 2006] MODIFY_CNF 1291 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1291 BEGIN : [Sun Jun 18 19:48:26 2006] CMD : minisat /tmp/csp2sat13640.cnf /tmp/csp2sat13640.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 135285 380126 | 45095 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (11 /sec) decisions : 36 (189 /sec) propagations : 35223 (185384 /sec) conflict literals : 11 (8.33 % deleted) Memory used : 9.01 MB CPU time : 0.19 s SATISFIABLE VERIFY_CNF 1291 END : (0 seconds) [Sun Jun 18 19:48:26 2006] VERIFY_CNF 1291 CPU : 0.23 = 0 + 0 + 0.2 + 0.03 # RESULT : makespan 1291 SATISFIABLE SHOW_RESULT 1291 BEGIN : [Sun Jun 18 19:48:26 2006] # ASSIGN : makespan 1291 # ASSIGN : s_0_0 153 # ASSIGN : s_0_1 651 # ASSIGN : s_0_2 204 # ASSIGN : s_0_3 184 # ASSIGN : s_1_0 958 # ASSIGN : s_1_1 474 # ASSIGN : s_1_2 619 # ASSIGN : s_1_3 291 # ASSIGN : s_2_0 322 # ASSIGN : s_2_1 1185 # ASSIGN : s_2_2 12 # ASSIGN : s_2_3 494 # ASSIGN : s_3_0 381 # ASSIGN : s_3_1 166 # ASSIGN : s_3_2 1083 # ASSIGN : s_3_3 1137 SHOW_RESULT 1291 END : 1291 (0 seconds) [Sun Jun 18 19:48:26 2006] SHOW_RESULT 1291 CPU : 0.04 = 0.04 + 0 + 0 + 0 # BOUND : makespan 1000 1291 MODIFY_CNF 1145 BEGIN : [Sun Jun 18 19:48:26 2006] MODIFY_CNF 1145 END : 3270144 bytes (0 seconds) [Sun Jun 18 19:48:26 2006] MODIFY_CNF 1145 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1145 BEGIN : [Sun Jun 18 19:48:26 2006] CMD : minisat /tmp/csp2sat13640.cnf /tmp/csp2sat13640.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 121269 338078 | 40423 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 20 (100 /sec) propagations : 26057 (130285 /sec) conflict literals : 0 ( nan % deleted) Memory used : 9.07 MB CPU time : 0.2 s SATISFIABLE VERIFY_CNF 1145 END : (0 seconds) [Sun Jun 18 19:48:26 2006] VERIFY_CNF 1145 CPU : 0.23 = 0 + 0 + 0.21 + 0.02 # RESULT : makespan 1145 SATISFIABLE SHOW_RESULT 1145 BEGIN : [Sun Jun 18 19:48:26 2006] # ASSIGN : makespan 1145 # ASSIGN : s_0_0 27 # ASSIGN : s_0_1 505 # ASSIGN : s_0_2 58 # ASSIGN : s_0_3 1 # ASSIGN : s_1_0 812 # ASSIGN : s_1_1 328 # ASSIGN : s_1_2 473 # ASSIGN : s_1_3 21 # ASSIGN : s_2_0 145 # ASSIGN : s_2_1 1039 # ASSIGN : s_2_2 847 # ASSIGN : s_2_3 204 # ASSIGN : s_3_0 235 # ASSIGN : s_3_1 20 # ASSIGN : s_3_2 1091 # ASSIGN : s_3_3 937 SHOW_RESULT 1145 END : 1145 (0 seconds) [Sun Jun 18 19:48:26 2006] SHOW_RESULT 1145 CPU : 0.0300000000000002 = 0.0300000000000002 + 0 + 0 + 0 # BOUND : makespan 1000 1145 MODIFY_CNF 1072 BEGIN : [Sun Jun 18 19:48:26 2006] MODIFY_CNF 1072 END : 3270143 bytes (0 seconds) [Sun Jun 18 19:48:26 2006] MODIFY_CNF 1072 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1072 BEGIN : [Sun Jun 18 19:48:26 2006] CMD : minisat /tmp/csp2sat13640.cnf /tmp/csp2sat13640.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 114261 317054 | 38087 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 14 (74 /sec) propagations : 26057 (137142 /sec) conflict literals : 0 ( nan % deleted) Memory used : 9.05 MB CPU time : 0.19 s SATISFIABLE VERIFY_CNF 1072 END : (1 seconds) [Sun Jun 18 19:48:27 2006] VERIFY_CNF 1072 CPU : 0.24 = 0 + 0 + 0.21 + 0.03 # RESULT : makespan 1072 SATISFIABLE SHOW_RESULT 1072 BEGIN : [Sun Jun 18 19:48:27 2006] # ASSIGN : makespan 1072 # ASSIGN : s_0_0 606 # ASSIGN : s_0_1 1 # ASSIGN : s_0_2 637 # ASSIGN : s_0_3 1052 # ASSIGN : s_1_0 680 # ASSIGN : s_1_1 535 # ASSIGN : s_1_2 196 # ASSIGN : s_1_3 13 # ASSIGN : s_2_0 1013 # ASSIGN : s_2_1 907 # ASSIGN : s_2_2 4 # ASSIGN : s_2_3 255 # ASSIGN : s_3_0 6 # ASSIGN : s_3_1 683 # ASSIGN : s_3_2 583 # ASSIGN : s_3_3 898 SHOW_RESULT 1072 END : 1072 (0 seconds) [Sun Jun 18 19:48:27 2006] SHOW_RESULT 1072 CPU : 0.04 = 0.04 + 0 + 0 + 0 # BOUND : makespan 1000 1072 MODIFY_CNF 1036 BEGIN : [Sun Jun 18 19:48:27 2006] MODIFY_CNF 1036 END : 3270143 bytes (0 seconds) [Sun Jun 18 19:48:27 2006] MODIFY_CNF 1036 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1036 BEGIN : [Sun Jun 18 19:48:27 2006] CMD : minisat /tmp/csp2sat13640.cnf /tmp/csp2sat13640.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 110805 306686 | 36935 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (11 /sec) decisions : 1 (5 /sec) propagations : 19375 (101974 /sec) conflict literals : 1 (0.00 % deleted) Memory used : 8.93 MB CPU time : 0.19 s UNSATISFIABLE VERIFY_CNF 1036 END : (0 seconds) [Sun Jun 18 19:48:27 2006] VERIFY_CNF 1036 CPU : 0.22 = 0 + 0 + 0.19 + 0.03 # RESULT : makespan 1036 UNSATISFIABLE # BOUND : makespan 1037 1072 MODIFY_CNF 1054 BEGIN : [Sun Jun 18 19:48:27 2006] MODIFY_CNF 1054 END : 3270143 bytes (0 seconds) [Sun Jun 18 19:48:27 2006] MODIFY_CNF 1054 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1054 BEGIN : [Sun Jun 18 19:48:27 2006] CMD : minisat /tmp/csp2sat13640.cnf /tmp/csp2sat13640.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 112533 311870 | 37511 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (10 /sec) decisions : 1 (5 /sec) propagations : 24303 (121515 /sec) conflict literals : 1 (0.00 % deleted) Memory used : 8.94 MB CPU time : 0.2 s UNSATISFIABLE VERIFY_CNF 1054 END : (0 seconds) [Sun Jun 18 19:48:27 2006] VERIFY_CNF 1054 CPU : 0.22 = 0 + 0 + 0.2 + 0.02 # RESULT : makespan 1054 UNSATISFIABLE # BOUND : makespan 1055 1072 MODIFY_CNF 1063 BEGIN : [Sun Jun 18 19:48:27 2006] MODIFY_CNF 1063 END : 3270143 bytes (0 seconds) [Sun Jun 18 19:48:27 2006] MODIFY_CNF 1063 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1063 BEGIN : [Sun Jun 18 19:48:27 2006] CMD : minisat /tmp/csp2sat13640.cnf /tmp/csp2sat13640.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 113397 314462 | 37799 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (10 /sec) decisions : 1 (5 /sec) propagations : 24434 (116352 /sec) conflict literals : 1 (0.00 % deleted) Memory used : 8.94 MB CPU time : 0.21 s UNSATISFIABLE VERIFY_CNF 1063 END : (0 seconds) [Sun Jun 18 19:48:27 2006] VERIFY_CNF 1063 CPU : 0.22 = 0 + 0 + 0.21 + 0.01 # RESULT : makespan 1063 UNSATISFIABLE # BOUND : makespan 1064 1072 MODIFY_CNF 1068 BEGIN : [Sun Jun 18 19:48:27 2006] MODIFY_CNF 1068 END : 3270143 bytes (0 seconds) [Sun Jun 18 19:48:27 2006] MODIFY_CNF 1068 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1068 BEGIN : [Sun Jun 18 19:48:27 2006] CMD : minisat /tmp/csp2sat13640.cnf /tmp/csp2sat13640.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 113877 315902 | 37959 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 4 (19 /sec) decisions : 4 (19 /sec) propagations : 32608 (155276 /sec) conflict literals : 4 (33.33 % deleted) Memory used : 8.94 MB CPU time : 0.21 s UNSATISFIABLE VERIFY_CNF 1068 END : (1 seconds) [Sun Jun 18 19:48:28 2006] VERIFY_CNF 1068 CPU : 0.24 = 0 + 0.01 + 0.21 + 0.02 # RESULT : makespan 1068 UNSATISFIABLE # BOUND : makespan 1069 1072 MODIFY_CNF 1070 BEGIN : [Sun Jun 18 19:48:28 2006] MODIFY_CNF 1070 END : 3270143 bytes (0 seconds) [Sun Jun 18 19:48:28 2006] MODIFY_CNF 1070 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1070 BEGIN : [Sun Jun 18 19:48:28 2006] CMD : minisat /tmp/csp2sat13640.cnf /tmp/csp2sat13640.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 114069 316478 | 38023 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 4 (19 /sec) decisions : 4 (19 /sec) propagations : 32570 (155095 /sec) conflict literals : 4 (33.33 % deleted) Memory used : 8.92 MB CPU time : 0.21 s UNSATISFIABLE VERIFY_CNF 1070 END : (0 seconds) [Sun Jun 18 19:48:28 2006] VERIFY_CNF 1070 CPU : 0.22 = 0 + 0 + 0.21 + 0.01 # RESULT : makespan 1070 UNSATISFIABLE # BOUND : makespan 1071 1072 MODIFY_CNF 1071 BEGIN : [Sun Jun 18 19:48:28 2006] MODIFY_CNF 1071 END : 3270143 bytes (0 seconds) [Sun Jun 18 19:48:28 2006] MODIFY_CNF 1071 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1071 BEGIN : [Sun Jun 18 19:48:28 2006] CMD : minisat /tmp/csp2sat13640.cnf /tmp/csp2sat13640.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 114165 316766 | 38055 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 13 (65 /sec) propagations : 26057 (130285 /sec) conflict literals : 0 ( nan % deleted) Memory used : 9.06 MB CPU time : 0.2 s SATISFIABLE VERIFY_CNF 1071 END : (0 seconds) [Sun Jun 18 19:48:28 2006] VERIFY_CNF 1071 CPU : 0.24 = 0 + 0 + 0.21 + 0.03 # RESULT : makespan 1071 SATISFIABLE SHOW_RESULT 1071 BEGIN : [Sun Jun 18 19:48:28 2006] # ASSIGN : makespan 1071 # ASSIGN : s_0_0 605 # ASSIGN : s_0_1 0 # ASSIGN : s_0_2 636 # ASSIGN : s_0_3 1051 # ASSIGN : s_1_0 679 # ASSIGN : s_1_1 534 # ASSIGN : s_1_2 195 # ASSIGN : s_1_3 12 # ASSIGN : s_2_0 1012 # ASSIGN : s_2_1 906 # ASSIGN : s_2_2 3 # ASSIGN : s_2_3 254 # ASSIGN : s_3_0 5 # ASSIGN : s_3_1 682 # ASSIGN : s_3_2 582 # ASSIGN : s_3_3 897 SHOW_RESULT 1071 END : 1071 (0 seconds) [Sun Jun 18 19:48:28 2006] SHOW_RESULT 1071 CPU : 0.04 = 0.04 + 0 + 0 + 0 # BOUND : makespan 1071 1071 MAIN END : (8 seconds) [Sun Jun 18 19:48:28 2006] MAIN CPU : 8.25 = 6.14 + 0.06 + 1.85 + 0.2