# TIMEOUT 18000 MAIN BEGIN : [Sun Jun 18 19:47:50 2006] READ BEGIN : csp/j3-per10-2.csp [Sun Jun 18 19:47:50 2006] READ END : csp/j3-per10-2.csp (0 seconds) [Sun Jun 18 19:47:50 2006] READ CPU : 0.05 = 0.05 + 0 + 0 + 0 # BOUND : makespan 1000 1629 GENERATE_CNF 1629 BEGIN : [Sun Jun 18 19:47:50 2006] GENERATE_CNF 1629 END : 15355 variables 68341 clauses 1294291 bytes (3 seconds) [Sun Jun 18 19:47:53 2006] GENERATE_CNF 1629 CPU : 2.39 = 2.39 + 0 + 0 + 0 MODIFY_CNF 1314 BEGIN : [Sun Jun 18 19:47:53 2006] MODIFY_CNF 1314 END : 1294297 bytes (0 seconds) [Sun Jun 18 19:47:53 2006] MODIFY_CNF 1314 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1314 BEGIN : [Sun Jun 18 19:47:53 2006] CMD : minisat /tmp/csp2sat13582.cnf /tmp/csp2sat13582.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 56897 155497 | 18965 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 17 (212 /sec) propagations : 15355 (191938 /sec) conflict literals : 0 ( nan % deleted) Memory used : 5.04 MB CPU time : 0.08 s SATISFIABLE VERIFY_CNF 1314 END : (0 seconds) [Sun Jun 18 19:47:53 2006] VERIFY_CNF 1314 CPU : 0.11 = 0.0100000000000002 + 0 + 0.08 + 0.02 # RESULT : makespan 1314 SATISFIABLE SHOW_RESULT 1314 BEGIN : [Sun Jun 18 19:47:53 2006] # ASSIGN : makespan 1314 # ASSIGN : s_0_0 821 # ASSIGN : s_0_1 198 # ASSIGN : s_0_2 414 # ASSIGN : s_1_0 275 # ASSIGN : s_1_1 394 # ASSIGN : s_1_2 646 # ASSIGN : s_2_0 387 # ASSIGN : s_2_1 782 # ASSIGN : s_2_2 1282 SHOW_RESULT 1314 END : 1314 (0 seconds) [Sun Jun 18 19:47:53 2006] SHOW_RESULT 1314 CPU : 0.0199999999999996 = 0.0199999999999996 + 0 + 0 + 0 # BOUND : makespan 1000 1314 MODIFY_CNF 1157 BEGIN : [Sun Jun 18 19:47:53 2006] MODIFY_CNF 1157 END : 1294297 bytes (0 seconds) [Sun Jun 18 19:47:53 2006] MODIFY_CNF 1157 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1157 BEGIN : [Sun Jun 18 19:47:53 2006] CMD : minisat /tmp/csp2sat13582.cnf /tmp/csp2sat13582.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 51245 138541 | 17081 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 16 (178 /sec) propagations : 15355 (170611 /sec) conflict literals : 0 ( nan % deleted) Memory used : 5.03 MB CPU time : 0.09 s SATISFIABLE VERIFY_CNF 1157 END : (0 seconds) [Sun Jun 18 19:47:53 2006] VERIFY_CNF 1157 CPU : 0.11 = 0 + 0 + 0.1 + 0.01 # RESULT : makespan 1157 SATISFIABLE SHOW_RESULT 1157 BEGIN : [Sun Jun 18 19:47:53 2006] # ASSIGN : makespan 1157 # ASSIGN : s_0_0 664 # ASSIGN : s_0_1 41 # ASSIGN : s_0_2 257 # ASSIGN : s_1_0 118 # ASSIGN : s_1_1 237 # ASSIGN : s_1_2 489 # ASSIGN : s_2_0 230 # ASSIGN : s_2_1 625 # ASSIGN : s_2_2 1125 SHOW_RESULT 1157 END : 1157 (0 seconds) [Sun Jun 18 19:47:53 2006] SHOW_RESULT 1157 CPU : 0.02 = 0.02 + 0 + 0 + 0 # BOUND : makespan 1000 1157 MODIFY_CNF 1078 BEGIN : [Sun Jun 18 19:47:53 2006] MODIFY_CNF 1078 END : 1294296 bytes (0 seconds) [Sun Jun 18 19:47:53 2006] MODIFY_CNF 1078 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1078 BEGIN : [Sun Jun 18 19:47:53 2006] CMD : minisat /tmp/csp2sat13582.cnf /tmp/csp2sat13582.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 48401 130009 | 16133 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 10 (100 /sec) propagations : 15355 (153550 /sec) conflict literals : 0 ( nan % deleted) Memory used : 4.99 MB CPU time : 0.1 s SATISFIABLE VERIFY_CNF 1078 END : (0 seconds) [Sun Jun 18 19:47:53 2006] VERIFY_CNF 1078 CPU : 0.11 = 0 + 0 + 0.11 + 0 # RESULT : makespan 1078 SATISFIABLE SHOW_RESULT 1078 BEGIN : [Sun Jun 18 19:47:53 2006] # ASSIGN : makespan 1078 # ASSIGN : s_0_0 473 # ASSIGN : s_0_1 277 # ASSIGN : s_0_2 45 # ASSIGN : s_1_0 966 # ASSIGN : s_1_1 25 # ASSIGN : s_1_2 330 # ASSIGN : s_2_0 78 # ASSIGN : s_2_1 546 # ASSIGN : s_2_2 1046 SHOW_RESULT 1078 END : 1078 (0 seconds) [Sun Jun 18 19:47:53 2006] SHOW_RESULT 1078 CPU : 0.02 = 0.02 + 0 + 0 + 0 # BOUND : makespan 1000 1078 MODIFY_CNF 1039 BEGIN : [Sun Jun 18 19:47:53 2006] MODIFY_CNF 1039 END : 1294296 bytes (0 seconds) [Sun Jun 18 19:47:53 2006] MODIFY_CNF 1039 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1039 BEGIN : [Sun Jun 18 19:47:53 2006] CMD : minisat /tmp/csp2sat13582.cnf /tmp/csp2sat13582.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 46997 125797 | 15665 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (22 /sec) decisions : 3 (33 /sec) propagations : 14639 (162656 /sec) conflict literals : 1 (0.00 % deleted) Memory used : 5.00 MB CPU time : 0.09 s UNSATISFIABLE VERIFY_CNF 1039 END : (0 seconds) [Sun Jun 18 19:47:53 2006] VERIFY_CNF 1039 CPU : 0.1 = 0 + 0 + 0.09 + 0.01 # RESULT : makespan 1039 UNSATISFIABLE # BOUND : makespan 1040 1078 MODIFY_CNF 1059 BEGIN : [Sun Jun 18 19:47:53 2006] MODIFY_CNF 1059 END : 1294296 bytes (0 seconds) [Sun Jun 18 19:47:53 2006] MODIFY_CNF 1059 CPU : 0.0100000000000002 = 0.0100000000000002 + 0 + 0 + 0 VERIFY_CNF 1059 BEGIN : [Sun Jun 18 19:47:53 2006] CMD : minisat /tmp/csp2sat13582.cnf /tmp/csp2sat13582.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 47717 127957 | 15905 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 10 (143 /sec) propagations : 15355 (219357 /sec) conflict literals : 0 ( nan % deleted) Memory used : 4.99 MB CPU time : 0.07 s SATISFIABLE VERIFY_CNF 1059 END : (0 seconds) [Sun Jun 18 19:47:53 2006] VERIFY_CNF 1059 CPU : 0.11 = 0 + 0 + 0.08 + 0.03 # RESULT : makespan 1059 SATISFIABLE SHOW_RESULT 1059 BEGIN : [Sun Jun 18 19:47:53 2006] # ASSIGN : makespan 1059 # ASSIGN : s_0_0 454 # ASSIGN : s_0_1 258 # ASSIGN : s_0_2 26 # ASSIGN : s_1_0 947 # ASSIGN : s_1_1 6 # ASSIGN : s_1_2 311 # ASSIGN : s_2_0 59 # ASSIGN : s_2_1 527 # ASSIGN : s_2_2 1027 SHOW_RESULT 1059 END : 1059 (0 seconds) [Sun Jun 18 19:47:53 2006] SHOW_RESULT 1059 CPU : 0.02 = 0.02 + 0 + 0 + 0 # BOUND : makespan 1040 1059 MODIFY_CNF 1049 BEGIN : [Sun Jun 18 19:47:53 2006] MODIFY_CNF 1049 END : 1294296 bytes (0 seconds) [Sun Jun 18 19:47:53 2006] MODIFY_CNF 1049 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1049 BEGIN : [Sun Jun 18 19:47:53 2006] CMD : minisat /tmp/csp2sat13582.cnf /tmp/csp2sat13582.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 47357 126877 | 15785 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (25 /sec) decisions : 3 (38 /sec) propagations : 14529 (181612 /sec) conflict literals : 1 (0.00 % deleted) Memory used : 4.99 MB CPU time : 0.08 s UNSATISFIABLE VERIFY_CNF 1049 END : (0 seconds) [Sun Jun 18 19:47:53 2006] VERIFY_CNF 1049 CPU : 0.1 = 0 + 0 + 0.08 + 0.02 # RESULT : makespan 1049 UNSATISFIABLE # BOUND : makespan 1050 1059 MODIFY_CNF 1054 BEGIN : [Sun Jun 18 19:47:53 2006] MODIFY_CNF 1054 END : 1294296 bytes (0 seconds) [Sun Jun 18 19:47:53 2006] MODIFY_CNF 1054 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1054 BEGIN : [Sun Jun 18 19:47:53 2006] CMD : minisat /tmp/csp2sat13582.cnf /tmp/csp2sat13582.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 47537 127417 | 15845 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 10 (111 /sec) propagations : 15355 (170611 /sec) conflict literals : 0 ( nan % deleted) Memory used : 4.99 MB CPU time : 0.09 s SATISFIABLE VERIFY_CNF 1054 END : (0 seconds) [Sun Jun 18 19:47:53 2006] VERIFY_CNF 1054 CPU : 0.11 = 0 + 0 + 0.1 + 0.01 # RESULT : makespan 1054 SATISFIABLE SHOW_RESULT 1054 BEGIN : [Sun Jun 18 19:47:53 2006] # ASSIGN : makespan 1054 # ASSIGN : s_0_0 449 # ASSIGN : s_0_1 253 # ASSIGN : s_0_2 21 # ASSIGN : s_1_0 942 # ASSIGN : s_1_1 1 # ASSIGN : s_1_2 306 # ASSIGN : s_2_0 54 # ASSIGN : s_2_1 522 # ASSIGN : s_2_2 1022 SHOW_RESULT 1054 END : 1054 (0 seconds) [Sun Jun 18 19:47:53 2006] SHOW_RESULT 1054 CPU : 0.02 = 0.02 + 0 + 0 + 0 # BOUND : makespan 1050 1054 MODIFY_CNF 1052 BEGIN : [Sun Jun 18 19:47:53 2006] MODIFY_CNF 1052 END : 1294296 bytes (0 seconds) [Sun Jun 18 19:47:53 2006] MODIFY_CNF 1052 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1052 BEGIN : [Sun Jun 18 19:47:53 2006] CMD : minisat /tmp/csp2sat13582.cnf /tmp/csp2sat13582.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 47465 127201 | 15821 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (20 /sec) decisions : 3 (30 /sec) propagations : 14419 (144190 /sec) conflict literals : 1 (0.00 % deleted) Memory used : 4.99 MB CPU time : 0.1 s UNSATISFIABLE VERIFY_CNF 1052 END : (0 seconds) [Sun Jun 18 19:47:53 2006] VERIFY_CNF 1052 CPU : 0.1 = 0 + 0 + 0.1 + 0 # RESULT : makespan 1052 UNSATISFIABLE # BOUND : makespan 1053 1054 MODIFY_CNF 1053 BEGIN : [Sun Jun 18 19:47:53 2006] MODIFY_CNF 1053 END : 1294296 bytes (0 seconds) [Sun Jun 18 19:47:53 2006] MODIFY_CNF 1053 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1053 BEGIN : [Sun Jun 18 19:47:53 2006] CMD : minisat /tmp/csp2sat13582.cnf /tmp/csp2sat13582.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 47501 127309 | 15833 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 9 (90 /sec) propagations : 15355 (153550 /sec) conflict literals : 0 ( nan % deleted) Memory used : 4.99 MB CPU time : 0.1 s SATISFIABLE VERIFY_CNF 1053 END : (1 seconds) [Sun Jun 18 19:47:54 2006] VERIFY_CNF 1053 CPU : 0.11 = 0 + 0 + 0.11 + 0 # RESULT : makespan 1053 SATISFIABLE SHOW_RESULT 1053 BEGIN : [Sun Jun 18 19:47:54 2006] # ASSIGN : makespan 1053 # ASSIGN : s_0_0 448 # ASSIGN : s_0_1 252 # ASSIGN : s_0_2 20 # ASSIGN : s_1_0 941 # ASSIGN : s_1_1 0 # ASSIGN : s_1_2 305 # ASSIGN : s_2_0 53 # ASSIGN : s_2_1 521 # ASSIGN : s_2_2 1021 SHOW_RESULT 1053 END : 1053 (0 seconds) [Sun Jun 18 19:47:54 2006] SHOW_RESULT 1053 CPU : 0.0200000000000002 = 0.0100000000000002 + 0.01 + 0 + 0 # BOUND : makespan 1053 1053 MAIN END : (4 seconds) [Sun Jun 18 19:47:54 2006] MAIN CPU : 3.54 = 2.58 + 0.01 + 0.85 + 0.1