# TIMEOUT 18000 MAIN BEGIN : [Sun Jun 18 19:47:38 2006] READ BEGIN : csp/j3-per0-2.csp [Sun Jun 18 19:47:38 2006] READ END : csp/j3-per0-2.csp (1 seconds) [Sun Jun 18 19:47:39 2006] READ CPU : 0.05 = 0.05 + 0 + 0 + 0 # BOUND : makespan 1000 2127 GENERATE_CNF 2127 BEGIN : [Sun Jun 18 19:47:39 2006] GENERATE_CNF 2127 END : 20335 variables 95123 clauses 1843704 bytes (3 seconds) [Sun Jun 18 19:47:42 2006] GENERATE_CNF 2127 CPU : 3.37 = 3.36 + 0.01 + 0 + 0 MODIFY_CNF 1563 BEGIN : [Sun Jun 18 19:47:42 2006] MODIFY_CNF 1563 END : 1843710 bytes (0 seconds) [Sun Jun 18 19:47:42 2006] MODIFY_CNF 1563 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1563 BEGIN : [Sun Jun 18 19:47:42 2006] CMD : minisat /tmp/csp2sat13549.cnf /tmp/csp2sat13549.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 74715 203971 | 24905 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 21 (175 /sec) propagations : 20335 (169458 /sec) conflict literals : 0 ( nan % deleted) Memory used : 6.25 MB CPU time : 0.12 s SATISFIABLE VERIFY_CNF 1563 END : (0 seconds) [Sun Jun 18 19:47:42 2006] VERIFY_CNF 1563 CPU : 0.14 = 0 + 0 + 0.13 + 0.01 # RESULT : makespan 1563 SATISFIABLE SHOW_RESULT 1563 BEGIN : [Sun Jun 18 19:47:42 2006] # ASSIGN : makespan 1563 # ASSIGN : s_0_0 193 # ASSIGN : s_0_1 479 # ASSIGN : s_0_2 563 # ASSIGN : s_1_0 290 # ASSIGN : s_1_1 551 # ASSIGN : s_1_2 1394 # ASSIGN : s_2_0 563 # ASSIGN : s_2_1 1205 # ASSIGN : s_2_2 1479 SHOW_RESULT 1563 END : 1563 (0 seconds) [Sun Jun 18 19:47:42 2006] SHOW_RESULT 1563 CPU : 0.0300000000000002 = 0.0300000000000002 + 0 + 0 + 0 # BOUND : makespan 1000 1563 MODIFY_CNF 1281 BEGIN : [Sun Jun 18 19:47:42 2006] MODIFY_CNF 1281 END : 1843710 bytes (0 seconds) [Sun Jun 18 19:47:42 2006] MODIFY_CNF 1281 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1281 BEGIN : [Sun Jun 18 19:47:42 2006] CMD : minisat /tmp/csp2sat13549.cnf /tmp/csp2sat13549.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 64563 173515 | 21521 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 17 (121 /sec) propagations : 20335 (145250 /sec) conflict literals : 0 ( nan % deleted) Memory used : 6.27 MB CPU time : 0.14 s SATISFIABLE VERIFY_CNF 1281 END : (0 seconds) [Sun Jun 18 19:47:42 2006] VERIFY_CNF 1281 CPU : 0.16 = 0 + 0 + 0.15 + 0.01 # RESULT : makespan 1281 SATISFIABLE SHOW_RESULT 1281 BEGIN : [Sun Jun 18 19:47:42 2006] # ASSIGN : makespan 1281 # ASSIGN : s_0_0 1184 # ASSIGN : s_0_1 197 # ASSIGN : s_0_2 281 # ASSIGN : s_1_0 8 # ASSIGN : s_1_1 269 # ASSIGN : s_1_2 1112 # ASSIGN : s_2_0 281 # ASSIGN : s_2_1 923 # ASSIGN : s_2_2 1197 SHOW_RESULT 1281 END : 1281 (0 seconds) [Sun Jun 18 19:47:42 2006] SHOW_RESULT 1281 CPU : 0.0299999999999998 = 0.0299999999999998 + 0 + 0 + 0 # BOUND : makespan 1000 1281 MODIFY_CNF 1140 BEGIN : [Sun Jun 18 19:47:42 2006] MODIFY_CNF 1140 END : 1843710 bytes (0 seconds) [Sun Jun 18 19:47:42 2006] MODIFY_CNF 1140 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1140 BEGIN : [Sun Jun 18 19:47:42 2006] CMD : minisat /tmp/csp2sat13549.cnf /tmp/csp2sat13549.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 59487 158287 | 19829 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 11 (79 /sec) propagations : 20335 (145250 /sec) conflict literals : 0 ( nan % deleted) Memory used : 6.27 MB CPU time : 0.14 s SATISFIABLE VERIFY_CNF 1140 END : (0 seconds) [Sun Jun 18 19:47:42 2006] VERIFY_CNF 1140 CPU : 0.16 = 0 + 0 + 0.15 + 0.01 # RESULT : makespan 1140 SATISFIABLE SHOW_RESULT 1140 BEGIN : [Sun Jun 18 19:47:42 2006] # ASSIGN : makespan 1140 # ASSIGN : s_0_0 971 # ASSIGN : s_0_1 1068 # ASSIGN : s_0_2 140 # ASSIGN : s_1_0 710 # ASSIGN : s_1_1 56 # ASSIGN : s_1_2 971 # ASSIGN : s_2_0 68 # ASSIGN : s_2_1 782 # ASSIGN : s_2_2 1056 SHOW_RESULT 1140 END : 1140 (0 seconds) [Sun Jun 18 19:47:42 2006] SHOW_RESULT 1140 CPU : 0.0299999999999998 = 0.0299999999999998 + 0 + 0 + 0 # BOUND : makespan 1000 1140 MODIFY_CNF 1070 BEGIN : [Sun Jun 18 19:47:42 2006] MODIFY_CNF 1070 END : 1843709 bytes (0 seconds) [Sun Jun 18 19:47:42 2006] MODIFY_CNF 1070 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1070 BEGIN : [Sun Jun 18 19:47:42 2006] CMD : minisat /tmp/csp2sat13549.cnf /tmp/csp2sat13549.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 56967 150727 | 18989 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 5 (36 /sec) decisions : 5 (36 /sec) propagations : 26895 (192107 /sec) conflict literals : 7 (0.00 % deleted) Memory used : 6.26 MB CPU time : 0.14 s UNSATISFIABLE VERIFY_CNF 1070 END : (1 seconds) [Sun Jun 18 19:47:43 2006] VERIFY_CNF 1070 CPU : 0.16 = 0 + 0 + 0.14 + 0.02 # RESULT : makespan 1070 UNSATISFIABLE # BOUND : makespan 1071 1140 MODIFY_CNF 1105 BEGIN : [Sun Jun 18 19:47:43 2006] MODIFY_CNF 1105 END : 1843710 bytes (0 seconds) [Sun Jun 18 19:47:43 2006] MODIFY_CNF 1105 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1105 BEGIN : [Sun Jun 18 19:47:43 2006] CMD : minisat /tmp/csp2sat13549.cnf /tmp/csp2sat13549.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 58227 154507 | 19409 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 11 (73 /sec) propagations : 20335 (135567 /sec) conflict literals : 0 ( nan % deleted) Memory used : 6.27 MB CPU time : 0.15 s SATISFIABLE VERIFY_CNF 1105 END : (0 seconds) [Sun Jun 18 19:47:43 2006] VERIFY_CNF 1105 CPU : 0.16 = 0 + 0 + 0.16 + 0 # RESULT : makespan 1105 SATISFIABLE SHOW_RESULT 1105 BEGIN : [Sun Jun 18 19:47:43 2006] # ASSIGN : makespan 1105 # ASSIGN : s_0_0 936 # ASSIGN : s_0_1 1033 # ASSIGN : s_0_2 105 # ASSIGN : s_1_0 675 # ASSIGN : s_1_1 21 # ASSIGN : s_1_2 936 # ASSIGN : s_2_0 33 # ASSIGN : s_2_1 747 # ASSIGN : s_2_2 1021 SHOW_RESULT 1105 END : 1105 (0 seconds) [Sun Jun 18 19:47:43 2006] SHOW_RESULT 1105 CPU : 0.0300000000000002 = 0.0300000000000002 + 0 + 0 + 0 # BOUND : makespan 1071 1105 MODIFY_CNF 1088 BEGIN : [Sun Jun 18 19:47:43 2006] MODIFY_CNF 1088 END : 1843709 bytes (0 seconds) [Sun Jun 18 19:47:43 2006] MODIFY_CNF 1088 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1088 BEGIN : [Sun Jun 18 19:47:43 2006] CMD : minisat /tmp/csp2sat13549.cnf /tmp/csp2sat13549.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 57615 152671 | 19205 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 9 (69 /sec) propagations : 20335 (156423 /sec) conflict literals : 0 ( nan % deleted) Memory used : 6.27 MB CPU time : 0.13 s SATISFIABLE VERIFY_CNF 1088 END : (0 seconds) [Sun Jun 18 19:47:43 2006] VERIFY_CNF 1088 CPU : 0.16 = 0 + 0 + 0.13 + 0.03 # RESULT : makespan 1088 SATISFIABLE SHOW_RESULT 1088 BEGIN : [Sun Jun 18 19:47:43 2006] # ASSIGN : makespan 1088 # ASSIGN : s_0_0 919 # ASSIGN : s_0_1 1016 # ASSIGN : s_0_2 88 # ASSIGN : s_1_0 658 # ASSIGN : s_1_1 4 # ASSIGN : s_1_2 919 # ASSIGN : s_2_0 16 # ASSIGN : s_2_1 730 # ASSIGN : s_2_2 1004 SHOW_RESULT 1088 END : 1088 (0 seconds) [Sun Jun 18 19:47:43 2006] SHOW_RESULT 1088 CPU : 0.0299999999999998 = 0.0299999999999998 + 0 + 0 + 0 # BOUND : makespan 1071 1088 MODIFY_CNF 1079 BEGIN : [Sun Jun 18 19:47:43 2006] MODIFY_CNF 1079 END : 1843709 bytes (0 seconds) [Sun Jun 18 19:47:43 2006] MODIFY_CNF 1079 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1079 BEGIN : [Sun Jun 18 19:47:43 2006] CMD : minisat /tmp/csp2sat13549.cnf /tmp/csp2sat13549.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 57291 151699 | 19097 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 5 (38 /sec) decisions : 5 (38 /sec) propagations : 25690 (197615 /sec) conflict literals : 7 (0.00 % deleted) Memory used : 6.26 MB CPU time : 0.13 s UNSATISFIABLE VERIFY_CNF 1079 END : (0 seconds) [Sun Jun 18 19:47:43 2006] VERIFY_CNF 1079 CPU : 0.15 = 0 + 0 + 0.13 + 0.02 # RESULT : makespan 1079 UNSATISFIABLE # BOUND : makespan 1080 1088 MODIFY_CNF 1084 BEGIN : [Sun Jun 18 19:47:43 2006] MODIFY_CNF 1084 END : 1843709 bytes (0 seconds) [Sun Jun 18 19:47:43 2006] MODIFY_CNF 1084 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1084 BEGIN : [Sun Jun 18 19:47:43 2006] CMD : minisat /tmp/csp2sat13549.cnf /tmp/csp2sat13549.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 57471 152239 | 19157 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 7 (64 /sec) propagations : 20335 (184864 /sec) conflict literals : 0 ( nan % deleted) Memory used : 6.27 MB CPU time : 0.11 s SATISFIABLE VERIFY_CNF 1084 END : (0 seconds) [Sun Jun 18 19:47:43 2006] VERIFY_CNF 1084 CPU : 0.16 = 0 + 0 + 0.12 + 0.04 # RESULT : makespan 1084 SATISFIABLE SHOW_RESULT 1084 BEGIN : [Sun Jun 18 19:47:43 2006] # ASSIGN : makespan 1084 # ASSIGN : s_0_0 915 # ASSIGN : s_0_1 1012 # ASSIGN : s_0_2 84 # ASSIGN : s_1_0 654 # ASSIGN : s_1_1 0 # ASSIGN : s_1_2 915 # ASSIGN : s_2_0 12 # ASSIGN : s_2_1 726 # ASSIGN : s_2_2 1000 SHOW_RESULT 1084 END : 1084 (0 seconds) [Sun Jun 18 19:47:43 2006] SHOW_RESULT 1084 CPU : 0.0300000000000002 = 0.0300000000000002 + 0 + 0 + 0 # BOUND : makespan 1080 1084 MODIFY_CNF 1082 BEGIN : [Sun Jun 18 19:47:43 2006] MODIFY_CNF 1082 END : 1843709 bytes (0 seconds) [Sun Jun 18 19:47:43 2006] MODIFY_CNF 1082 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1082 BEGIN : [Sun Jun 18 19:47:43 2006] CMD : minisat /tmp/csp2sat13549.cnf /tmp/csp2sat13549.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 57399 152023 | 19133 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 5 (38 /sec) decisions : 5 (38 /sec) propagations : 25657 (197362 /sec) conflict literals : 7 (0.00 % deleted) Memory used : 6.26 MB CPU time : 0.13 s UNSATISFIABLE VERIFY_CNF 1082 END : (0 seconds) [Sun Jun 18 19:47:43 2006] VERIFY_CNF 1082 CPU : 0.16 = 0 + 0 + 0.13 + 0.03 # RESULT : makespan 1082 UNSATISFIABLE # BOUND : makespan 1083 1084 MODIFY_CNF 1083 BEGIN : [Sun Jun 18 19:47:43 2006] MODIFY_CNF 1083 END : 1843709 bytes (0 seconds) [Sun Jun 18 19:47:43 2006] MODIFY_CNF 1083 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1083 BEGIN : [Sun Jun 18 19:47:43 2006] CMD : minisat /tmp/csp2sat13549.cnf /tmp/csp2sat13549.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 57435 152131 | 19145 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 5 (33 /sec) decisions : 5 (33 /sec) propagations : 25646 (170973 /sec) conflict literals : 7 (0.00 % deleted) Memory used : 6.26 MB CPU time : 0.15 s UNSATISFIABLE VERIFY_CNF 1083 END : (1 seconds) [Sun Jun 18 19:47:44 2006] VERIFY_CNF 1083 CPU : 0.16 = 0 + 0 + 0.15 + 0.00999999999999998 # RESULT : makespan 1083 UNSATISFIABLE # BOUND : makespan 1084 1084 MAIN END : (6 seconds) [Sun Jun 18 19:47:44 2006] MAIN CPU : 5.17 = 3.59 + 0.01 + 1.39 + 0.18