# TIMEOUT 18000 MAIN BEGIN : [Sun Jun 18 16:07:10 2006] READ BEGIN : csp/gp03-07.csp [Sun Jun 18 16:07:10 2006] READ END : csp/gp03-07.csp (1 seconds) [Sun Jun 18 16:07:11 2006] READ CPU : 0.05 = 0.04 + 0.01 + 0 + 0 # BOUND : makespan 1000 1486 GENERATE_CNF 1486 BEGIN : [Sun Jun 18 16:07:11 2006] GENERATE_CNF 1486 END : 13925 variables 59868 clauses 1122938 bytes (2 seconds) [Sun Jun 18 16:07:13 2006] GENERATE_CNF 1486 CPU : 2.09 = 2.08 + 0.01 + 0 + 0 MODIFY_CNF 1243 BEGIN : [Sun Jun 18 16:07:13 2006] MODIFY_CNF 1243 END : 1122944 bytes (0 seconds) [Sun Jun 18 16:07:13 2006] MODIFY_CNF 1243 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1243 BEGIN : [Sun Jun 18 16:07:13 2006] CMD : minisat /tmp/csp2sat8611.cnf /tmp/csp2sat8611.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 51016 139284 | 17005 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 13 (162 /sec) propagations : 13925 (174062 /sec) conflict literals : 0 ( nan % deleted) Memory used : 4.69 MB CPU time : 0.08 s SATISFIABLE VERIFY_CNF 1243 END : (0 seconds) [Sun Jun 18 16:07:13 2006] VERIFY_CNF 1243 CPU : 0.08 = 0 + 0 + 0.08 + 0 # RESULT : makespan 1243 SATISFIABLE SHOW_RESULT 1243 BEGIN : [Sun Jun 18 16:07:13 2006] # ASSIGN : makespan 1243 # ASSIGN : s_0_0 1078 # ASSIGN : s_0_1 65 # ASSIGN : s_0_2 243 # ASSIGN : s_1_0 568 # ASSIGN : s_1_1 242 # ASSIGN : s_1_2 901 # ASSIGN : s_2_0 66 # ASSIGN : s_2_1 745 # ASSIGN : s_2_2 1242 SHOW_RESULT 1243 END : 1243 (0 seconds) [Sun Jun 18 16:07:13 2006] SHOW_RESULT 1243 CPU : 0.02 = 0.02 + 0 + 0 + 0 # BOUND : makespan 1000 1243 MODIFY_CNF 1121 BEGIN : [Sun Jun 18 16:07:13 2006] MODIFY_CNF 1121 END : 1122944 bytes (0 seconds) [Sun Jun 18 16:07:13 2006] MODIFY_CNF 1121 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1121 BEGIN : [Sun Jun 18 16:07:13 2006] CMD : minisat /tmp/csp2sat8611.cnf /tmp/csp2sat8611.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 46624 126108 | 15541 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (29 /sec) decisions : 3 (43 /sec) propagations : 11789 (168414 /sec) conflict literals : 1 (0.00 % deleted) Memory used : 4.62 MB CPU time : 0.07 s UNSATISFIABLE VERIFY_CNF 1121 END : (0 seconds) [Sun Jun 18 16:07:13 2006] VERIFY_CNF 1121 CPU : 0.08 = 0 + 0 + 0.07 + 0.01 # RESULT : makespan 1121 UNSATISFIABLE # BOUND : makespan 1122 1243 MODIFY_CNF 1182 BEGIN : [Sun Jun 18 16:07:13 2006] MODIFY_CNF 1182 END : 1122944 bytes (0 seconds) [Sun Jun 18 16:07:13 2006] MODIFY_CNF 1182 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1182 BEGIN : [Sun Jun 18 16:07:13 2006] CMD : minisat /tmp/csp2sat8611.cnf /tmp/csp2sat8611.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 48820 132696 | 16273 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 13 (186 /sec) propagations : 13925 (198929 /sec) conflict literals : 0 ( nan % deleted) Memory used : 4.68 MB CPU time : 0.07 s SATISFIABLE VERIFY_CNF 1182 END : (0 seconds) [Sun Jun 18 16:07:13 2006] VERIFY_CNF 1182 CPU : 0.09 = 0 + 0 + 0.08 + 0.01 # RESULT : makespan 1182 SATISFIABLE SHOW_RESULT 1182 BEGIN : [Sun Jun 18 16:07:13 2006] # ASSIGN : makespan 1182 # ASSIGN : s_0_0 1017 # ASSIGN : s_0_1 4 # ASSIGN : s_0_2 182 # ASSIGN : s_1_0 507 # ASSIGN : s_1_1 181 # ASSIGN : s_1_2 840 # ASSIGN : s_2_0 5 # ASSIGN : s_2_1 684 # ASSIGN : s_2_2 1181 SHOW_RESULT 1182 END : 1182 (0 seconds) [Sun Jun 18 16:07:13 2006] SHOW_RESULT 1182 CPU : 0.02 = 0.02 + 0 + 0 + 0 # BOUND : makespan 1122 1182 MODIFY_CNF 1152 BEGIN : [Sun Jun 18 16:07:13 2006] MODIFY_CNF 1152 END : 1122944 bytes (0 seconds) [Sun Jun 18 16:07:13 2006] MODIFY_CNF 1152 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1152 BEGIN : [Sun Jun 18 16:07:13 2006] CMD : minisat /tmp/csp2sat8611.cnf /tmp/csp2sat8611.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 47740 129456 | 15913 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (29 /sec) decisions : 3 (43 /sec) propagations : 11479 (163986 /sec) conflict literals : 1 (0.00 % deleted) Memory used : 4.63 MB CPU time : 0.07 s UNSATISFIABLE VERIFY_CNF 1152 END : (0 seconds) [Sun Jun 18 16:07:13 2006] VERIFY_CNF 1152 CPU : 0.08 = 0 + 0 + 0.07 + 0.01 # RESULT : makespan 1152 UNSATISFIABLE # BOUND : makespan 1153 1182 MODIFY_CNF 1167 BEGIN : [Sun Jun 18 16:07:13 2006] MODIFY_CNF 1167 END : 1122944 bytes (0 seconds) [Sun Jun 18 16:07:13 2006] MODIFY_CNF 1167 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1167 BEGIN : [Sun Jun 18 16:07:13 2006] CMD : minisat /tmp/csp2sat8611.cnf /tmp/csp2sat8611.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 48280 131076 | 16093 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 12 (171 /sec) propagations : 13925 (198929 /sec) conflict literals : 0 ( nan % deleted) Memory used : 4.68 MB CPU time : 0.07 s SATISFIABLE VERIFY_CNF 1167 END : (0 seconds) [Sun Jun 18 16:07:13 2006] VERIFY_CNF 1167 CPU : 0.09 = 0 + 0 + 0.08 + 0.01 # RESULT : makespan 1167 SATISFIABLE SHOW_RESULT 1167 BEGIN : [Sun Jun 18 16:07:13 2006] # ASSIGN : makespan 1167 # ASSIGN : s_0_0 1 # ASSIGN : s_0_1 990 # ASSIGN : s_0_2 167 # ASSIGN : s_1_0 166 # ASSIGN : s_1_1 499 # ASSIGN : s_1_2 825 # ASSIGN : s_2_0 664 # ASSIGN : s_2_1 2 # ASSIGN : s_2_2 1166 SHOW_RESULT 1167 END : 1167 (0 seconds) [Sun Jun 18 16:07:13 2006] SHOW_RESULT 1167 CPU : 0.02 = 0.02 + 0 + 0 + 0 # BOUND : makespan 1153 1167 MODIFY_CNF 1160 BEGIN : [Sun Jun 18 16:07:13 2006] MODIFY_CNF 1160 END : 1122944 bytes (0 seconds) [Sun Jun 18 16:07:13 2006] MODIFY_CNF 1160 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1160 BEGIN : [Sun Jun 18 16:07:13 2006] CMD : minisat /tmp/csp2sat8611.cnf /tmp/csp2sat8611.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 48028 130320 | 16009 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (29 /sec) decisions : 3 (43 /sec) propagations : 11398 (162829 /sec) conflict literals : 1 (0.00 % deleted) Memory used : 4.61 MB CPU time : 0.07 s UNSATISFIABLE VERIFY_CNF 1160 END : (0 seconds) [Sun Jun 18 16:07:13 2006] VERIFY_CNF 1160 CPU : 0.08 = 0 + 0 + 0.07 + 0.01 # RESULT : makespan 1160 UNSATISFIABLE # BOUND : makespan 1161 1167 MODIFY_CNF 1164 BEGIN : [Sun Jun 18 16:07:13 2006] MODIFY_CNF 1164 END : 1122944 bytes (0 seconds) [Sun Jun 18 16:07:13 2006] MODIFY_CNF 1164 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1164 BEGIN : [Sun Jun 18 16:07:13 2006] CMD : minisat /tmp/csp2sat8611.cnf /tmp/csp2sat8611.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 48172 130752 | 16057 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 3 (38 /sec) decisions : 3 (38 /sec) propagations : 16406 (205075 /sec) conflict literals : 3 (0.00 % deleted) Memory used : 4.62 MB CPU time : 0.08 s UNSATISFIABLE VERIFY_CNF 1164 END : (0 seconds) [Sun Jun 18 16:07:13 2006] VERIFY_CNF 1164 CPU : 0.0900000000000002 = 0.0100000000000002 + 0 + 0.08 + 0 # RESULT : makespan 1164 UNSATISFIABLE # BOUND : makespan 1165 1167 MODIFY_CNF 1166 BEGIN : [Sun Jun 18 16:07:13 2006] MODIFY_CNF 1166 END : 1122944 bytes (0 seconds) [Sun Jun 18 16:07:13 2006] MODIFY_CNF 1166 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1166 BEGIN : [Sun Jun 18 16:07:13 2006] CMD : minisat /tmp/csp2sat8611.cnf /tmp/csp2sat8611.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 48244 130968 | 16081 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 9 (112 /sec) propagations : 13925 (174062 /sec) conflict literals : 0 ( nan % deleted) Memory used : 4.68 MB CPU time : 0.08 s SATISFIABLE VERIFY_CNF 1166 END : (0 seconds) [Sun Jun 18 16:07:13 2006] VERIFY_CNF 1166 CPU : 0.09 = 0 + 0 + 0.09 + 0 # RESULT : makespan 1166 SATISFIABLE SHOW_RESULT 1166 BEGIN : [Sun Jun 18 16:07:13 2006] # ASSIGN : makespan 1166 # ASSIGN : s_0_0 0 # ASSIGN : s_0_1 989 # ASSIGN : s_0_2 166 # ASSIGN : s_1_0 165 # ASSIGN : s_1_1 498 # ASSIGN : s_1_2 824 # ASSIGN : s_2_0 663 # ASSIGN : s_2_1 1 # ASSIGN : s_2_2 1165 SHOW_RESULT 1166 END : 1166 (0 seconds) [Sun Jun 18 16:07:13 2006] SHOW_RESULT 1166 CPU : 0.02 = 0.02 + 0 + 0 + 0 # BOUND : makespan 1165 1166 MODIFY_CNF 1165 BEGIN : [Sun Jun 18 16:07:13 2006] MODIFY_CNF 1165 END : 1122944 bytes (0 seconds) [Sun Jun 18 16:07:13 2006] MODIFY_CNF 1165 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1165 BEGIN : [Sun Jun 18 16:07:13 2006] CMD : minisat /tmp/csp2sat8611.cnf /tmp/csp2sat8611.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 48208 130860 | 16069 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 7 (117 /sec) propagations : 13925 (232083 /sec) conflict literals : 0 ( nan % deleted) Memory used : 4.68 MB CPU time : 0.06 s SATISFIABLE VERIFY_CNF 1165 END : (0 seconds) [Sun Jun 18 16:07:13 2006] VERIFY_CNF 1165 CPU : 0.0800000000000001 = 0 + 0 + 0.0600000000000001 + 0.02 # RESULT : makespan 1165 SATISFIABLE SHOW_RESULT 1165 BEGIN : [Sun Jun 18 16:07:13 2006] # ASSIGN : makespan 1165 # ASSIGN : s_0_0 1000 # ASSIGN : s_0_1 823 # ASSIGN : s_0_2 165 # ASSIGN : s_1_0 164 # ASSIGN : s_1_1 497 # ASSIGN : s_1_2 823 # ASSIGN : s_2_0 498 # ASSIGN : s_2_1 0 # ASSIGN : s_2_2 1164 SHOW_RESULT 1165 END : 1165 (1 seconds) [Sun Jun 18 16:07:14 2006] SHOW_RESULT 1165 CPU : 0.0199999999999996 = 0.0199999999999996 + 0 + 0 + 0 # BOUND : makespan 1165 1165 MAIN END : (4 seconds) [Sun Jun 18 16:07:14 2006] MAIN CPU : 3 = 2.23 + 0.02 + 0.68 + 0.07