# TIMEOUT 18000 MAIN BEGIN : [Sun Jun 18 19:47:44 2006] READ BEGIN : csp/j3-per10-0.csp [Sun Jun 18 19:47:44 2006] READ END : csp/j3-per10-0.csp (0 seconds) [Sun Jun 18 19:47:44 2006] READ CPU : 0.05 = 0.05 + 0 + 0 + 0 # BOUND : makespan 1000 1361 GENERATE_CNF 1361 BEGIN : [Sun Jun 18 19:47:44 2006] GENERATE_CNF 1361 END : 12675 variables 53453 clauses 992405 bytes (2 seconds) [Sun Jun 18 19:47:46 2006] GENERATE_CNF 1361 CPU : 1.86 = 1.85 + 0.01 + 0 + 0 MODIFY_CNF 1180 BEGIN : [Sun Jun 18 19:47:46 2006] MODIFY_CNF 1180 END : 992411 bytes (0 seconds) [Sun Jun 18 19:47:46 2006] MODIFY_CNF 1180 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1180 BEGIN : [Sun Jun 18 19:47:46 2006] CMD : minisat /tmp/csp2sat13562.cnf /tmp/csp2sat13562.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 46833 127985 | 15611 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 12 (200 /sec) propagations : 12675 (211250 /sec) conflict literals : 0 ( nan % deleted) Memory used : 4.34 MB CPU time : 0.06 s SATISFIABLE VERIFY_CNF 1180 END : (0 seconds) [Sun Jun 18 19:47:46 2006] VERIFY_CNF 1180 CPU : 0.08 = 0 + 0 + 0.07 + 0.01 # RESULT : makespan 1180 SATISFIABLE SHOW_RESULT 1180 BEGIN : [Sun Jun 18 19:47:46 2006] # ASSIGN : makespan 1180 # ASSIGN : s_0_0 606 # ASSIGN : s_0_1 997 # ASSIGN : s_0_2 246 # ASSIGN : s_1_0 976 # ASSIGN : s_1_1 43 # ASSIGN : s_1_2 640 # ASSIGN : s_2_0 180 # ASSIGN : s_2_1 618 # ASSIGN : s_2_2 845 SHOW_RESULT 1180 END : 1180 (0 seconds) [Sun Jun 18 19:47:46 2006] SHOW_RESULT 1180 CPU : 0.02 = 0.01 + 0.01 + 0 + 0 # BOUND : makespan 1000 1180 MODIFY_CNF 1090 BEGIN : [Sun Jun 18 19:47:46 2006] MODIFY_CNF 1090 END : 992410 bytes (0 seconds) [Sun Jun 18 19:47:46 2006] MODIFY_CNF 1090 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1090 BEGIN : [Sun Jun 18 19:47:46 2006] CMD : minisat /tmp/csp2sat13562.cnf /tmp/csp2sat13562.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 43593 118265 | 14531 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 6 (100 /sec) decisions : 5 (83 /sec) propagations : 18818 (313633 /sec) conflict literals : 8 (11.11 % deleted) Memory used : 4.28 MB CPU time : 0.06 s UNSATISFIABLE VERIFY_CNF 1090 END : (0 seconds) [Sun Jun 18 19:47:46 2006] VERIFY_CNF 1090 CPU : 0.07 = 0 + 0 + 0.06 + 0.01 # RESULT : makespan 1090 UNSATISFIABLE # BOUND : makespan 1091 1180 MODIFY_CNF 1135 BEGIN : [Sun Jun 18 19:47:46 2006] MODIFY_CNF 1135 END : 992411 bytes (0 seconds) [Sun Jun 18 19:47:46 2006] MODIFY_CNF 1135 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1135 BEGIN : [Sun Jun 18 19:47:46 2006] CMD : minisat /tmp/csp2sat13562.cnf /tmp/csp2sat13562.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 45213 123125 | 15071 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (29 /sec) decisions : 13 (186 /sec) propagations : 17409 (248700 /sec) conflict literals : 5 (28.57 % deleted) Memory used : 4.34 MB CPU time : 0.07 s SATISFIABLE VERIFY_CNF 1135 END : (0 seconds) [Sun Jun 18 19:47:46 2006] VERIFY_CNF 1135 CPU : 0.08 = 0 + 0 + 0.07 + 0.01 # RESULT : makespan 1135 SATISFIABLE SHOW_RESULT 1135 BEGIN : [Sun Jun 18 19:47:46 2006] # ASSIGN : makespan 1135 # ASSIGN : s_0_0 4 # ASSIGN : s_0_1 952 # ASSIGN : s_0_2 440 # ASSIGN : s_1_0 931 # ASSIGN : s_1_1 356 # ASSIGN : s_1_2 151 # ASSIGN : s_2_0 374 # ASSIGN : s_2_1 129 # ASSIGN : s_2_2 800 SHOW_RESULT 1135 END : 1135 (0 seconds) [Sun Jun 18 19:47:46 2006] SHOW_RESULT 1135 CPU : 0.01 = 0.01 + 0 + 0 + 0 # BOUND : makespan 1091 1135 MODIFY_CNF 1113 BEGIN : [Sun Jun 18 19:47:46 2006] MODIFY_CNF 1113 END : 992411 bytes (0 seconds) [Sun Jun 18 19:47:46 2006] MODIFY_CNF 1113 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1113 BEGIN : [Sun Jun 18 19:47:46 2006] CMD : minisat /tmp/csp2sat13562.cnf /tmp/csp2sat13562.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 44421 120749 | 14807 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 4 (67 /sec) decisions : 3 (50 /sec) propagations : 15384 (256400 /sec) conflict literals : 4 (20.00 % deleted) Memory used : 4.30 MB CPU time : 0.06 s UNSATISFIABLE VERIFY_CNF 1113 END : (0 seconds) [Sun Jun 18 19:47:46 2006] VERIFY_CNF 1113 CPU : 0.08 = 0 + 0 + 0.06 + 0.02 # RESULT : makespan 1113 UNSATISFIABLE # BOUND : makespan 1114 1135 MODIFY_CNF 1124 BEGIN : [Sun Jun 18 19:47:46 2006] MODIFY_CNF 1124 END : 992411 bytes (0 seconds) [Sun Jun 18 19:47:46 2006] MODIFY_CNF 1124 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1124 BEGIN : [Sun Jun 18 19:47:46 2006] CMD : minisat /tmp/csp2sat13562.cnf /tmp/csp2sat13562.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 44817 121937 | 14939 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 7 (117 /sec) decisions : 7 (117 /sec) propagations : 21940 (365667 /sec) conflict literals : 11 (35.29 % deleted) Memory used : 4.29 MB CPU time : 0.06 s UNSATISFIABLE VERIFY_CNF 1124 END : (0 seconds) [Sun Jun 18 19:47:46 2006] VERIFY_CNF 1124 CPU : 0.07 = 0 + 0 + 0.06 + 0.01 # RESULT : makespan 1124 UNSATISFIABLE # BOUND : makespan 1125 1135 MODIFY_CNF 1130 BEGIN : [Sun Jun 18 19:47:46 2006] MODIFY_CNF 1130 END : 992411 bytes (0 seconds) [Sun Jun 18 19:47:46 2006] MODIFY_CNF 1130 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1130 BEGIN : [Sun Jun 18 19:47:46 2006] CMD : minisat /tmp/csp2sat13562.cnf /tmp/csp2sat13562.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 45033 122585 | 15011 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 8 (100 /sec) decisions : 8 (100 /sec) propagations : 25213 (315162 /sec) conflict literals : 15 (16.67 % deleted) Memory used : 4.29 MB CPU time : 0.08 s UNSATISFIABLE VERIFY_CNF 1130 END : (0 seconds) [Sun Jun 18 19:47:46 2006] VERIFY_CNF 1130 CPU : 0.08 = 0 + 0 + 0.08 + 0 # RESULT : makespan 1130 UNSATISFIABLE # BOUND : makespan 1131 1135 MODIFY_CNF 1133 BEGIN : [Sun Jun 18 19:47:46 2006] MODIFY_CNF 1133 END : 992411 bytes (0 seconds) [Sun Jun 18 19:47:46 2006] MODIFY_CNF 1133 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1133 BEGIN : [Sun Jun 18 19:47:46 2006] CMD : minisat /tmp/csp2sat13562.cnf /tmp/csp2sat13562.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 45141 122909 | 15047 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (33 /sec) decisions : 13 (217 /sec) propagations : 17409 (290150 /sec) conflict literals : 5 (28.57 % deleted) Memory used : 4.35 MB CPU time : 0.06 s SATISFIABLE VERIFY_CNF 1133 END : (0 seconds) [Sun Jun 18 19:47:46 2006] VERIFY_CNF 1133 CPU : 0.08 = 0 + 0 + 0.07 + 0.01 # RESULT : makespan 1133 SATISFIABLE SHOW_RESULT 1133 BEGIN : [Sun Jun 18 19:47:46 2006] # ASSIGN : makespan 1133 # ASSIGN : s_0_0 2 # ASSIGN : s_0_1 950 # ASSIGN : s_0_2 438 # ASSIGN : s_1_0 929 # ASSIGN : s_1_1 354 # ASSIGN : s_1_2 149 # ASSIGN : s_2_0 372 # ASSIGN : s_2_1 127 # ASSIGN : s_2_2 798 SHOW_RESULT 1133 END : 1133 (0 seconds) [Sun Jun 18 19:47:46 2006] SHOW_RESULT 1133 CPU : 0.02 = 0.02 + 0 + 0 + 0 # BOUND : makespan 1131 1133 MODIFY_CNF 1132 BEGIN : [Sun Jun 18 19:47:46 2006] MODIFY_CNF 1132 END : 992411 bytes (0 seconds) [Sun Jun 18 19:47:46 2006] MODIFY_CNF 1132 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1132 BEGIN : [Sun Jun 18 19:47:46 2006] CMD : minisat /tmp/csp2sat13562.cnf /tmp/csp2sat13562.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 45105 122801 | 15035 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (29 /sec) decisions : 13 (186 /sec) propagations : 17409 (248700 /sec) conflict literals : 5 (28.57 % deleted) Memory used : 4.35 MB CPU time : 0.07 s SATISFIABLE VERIFY_CNF 1132 END : (0 seconds) [Sun Jun 18 19:47:46 2006] VERIFY_CNF 1132 CPU : 0.0800000000000001 = 0 + 0 + 0.0700000000000001 + 0.01 # RESULT : makespan 1132 SATISFIABLE SHOW_RESULT 1132 BEGIN : [Sun Jun 18 19:47:46 2006] # ASSIGN : makespan 1132 # ASSIGN : s_0_0 1 # ASSIGN : s_0_1 949 # ASSIGN : s_0_2 437 # ASSIGN : s_1_0 928 # ASSIGN : s_1_1 353 # ASSIGN : s_1_2 148 # ASSIGN : s_2_0 371 # ASSIGN : s_2_1 126 # ASSIGN : s_2_2 797 SHOW_RESULT 1132 END : 1132 (0 seconds) [Sun Jun 18 19:47:46 2006] SHOW_RESULT 1132 CPU : 0.02 = 0.01 + 0.01 + 0 + 0 # BOUND : makespan 1131 1132 MODIFY_CNF 1131 BEGIN : [Sun Jun 18 19:47:46 2006] MODIFY_CNF 1131 END : 992411 bytes (0 seconds) [Sun Jun 18 19:47:46 2006] MODIFY_CNF 1131 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1131 BEGIN : [Sun Jun 18 19:47:46 2006] CMD : minisat /tmp/csp2sat13562.cnf /tmp/csp2sat13562.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 45069 122693 | 15023 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (40 /sec) decisions : 10 (200 /sec) propagations : 17409 (348180 /sec) conflict literals : 5 (28.57 % deleted) Memory used : 4.35 MB CPU time : 0.05 s SATISFIABLE VERIFY_CNF 1131 END : (0 seconds) [Sun Jun 18 19:47:46 2006] VERIFY_CNF 1131 CPU : 0.0799999999999999 = 0 + 0 + 0.0599999999999999 + 0.02 # RESULT : makespan 1131 SATISFIABLE SHOW_RESULT 1131 BEGIN : [Sun Jun 18 19:47:46 2006] # ASSIGN : makespan 1131 # ASSIGN : s_0_0 0 # ASSIGN : s_0_1 948 # ASSIGN : s_0_2 436 # ASSIGN : s_1_0 927 # ASSIGN : s_1_1 352 # ASSIGN : s_1_2 147 # ASSIGN : s_2_0 370 # ASSIGN : s_2_1 125 # ASSIGN : s_2_2 796 SHOW_RESULT 1131 END : 1131 (0 seconds) [Sun Jun 18 19:47:46 2006] SHOW_RESULT 1131 CPU : 0.02 = 0.02 + 0 + 0 + 0 # BOUND : makespan 1131 1131 MAIN END : (2 seconds) [Sun Jun 18 19:47:46 2006] MAIN CPU : 2.7 = 1.97 + 0.03 + 0.6 + 0.1