# TIMEOUT 18000 MAIN BEGIN : [Sun Jun 18 19:48:28 2006] READ BEGIN : csp/j4-per10-0.csp [Sun Jun 18 19:48:28 2006] READ END : csp/j4-per10-0.csp (0 seconds) [Sun Jun 18 19:48:28 2006] READ CPU : 0.11 = 0.11 + 0 + 0 + 0 # BOUND : makespan 1000 1783 GENERATE_CNF 1783 BEGIN : [Sun Jun 18 19:48:28 2006] GENERATE_CNF 1783 END : 29457 variables 190740 clauses 3838917 bytes (7 seconds) [Sun Jun 18 19:48:35 2006] GENERATE_CNF 1783 CPU : 6.75 = 6.71 + 0.04 + 0 + 0 MODIFY_CNF 1391 BEGIN : [Sun Jun 18 19:48:35 2006] MODIFY_CNF 1391 END : 3838923 bytes (0 seconds) [Sun Jun 18 19:48:35 2006] MODIFY_CNF 1391 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1391 BEGIN : [Sun Jun 18 19:48:35 2006] CMD : minisat /tmp/csp2sat13650.cnf /tmp/csp2sat13650.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 152895 429556 | 50965 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 1 (4 /sec) decisions : 42 (175 /sec) propagations : 32035 (133479 /sec) conflict literals : 5 (0.00 % deleted) Memory used : 10.17 MB CPU time : 0.24 s SATISFIABLE VERIFY_CNF 1391 END : (1 seconds) [Sun Jun 18 19:48:36 2006] VERIFY_CNF 1391 CPU : 0.27 = 0 + 0 + 0.26 + 0.01 # RESULT : makespan 1391 SATISFIABLE SHOW_RESULT 1391 BEGIN : [Sun Jun 18 19:48:36 2006] # ASSIGN : makespan 1391 # ASSIGN : s_0_0 34 # ASSIGN : s_0_1 2 # ASSIGN : s_0_2 832 # ASSIGN : s_0_3 491 # ASSIGN : s_1_0 460 # ASSIGN : s_1_1 830 # ASSIGN : s_1_2 177 # ASSIGN : s_1_3 659 # ASSIGN : s_2_0 519 # ASSIGN : s_2_1 383 # ASSIGN : s_2_2 595 # ASSIGN : s_2_3 712 # ASSIGN : s_3_0 704 # ASSIGN : s_3_1 466 # ASSIGN : s_3_2 1143 # ASSIGN : s_3_3 1383 SHOW_RESULT 1391 END : 1391 (0 seconds) [Sun Jun 18 19:48:36 2006] SHOW_RESULT 1391 CPU : 0.0399999999999994 = 0.0299999999999994 + 0.01 + 0 + 0 # BOUND : makespan 1000 1391 MODIFY_CNF 1195 BEGIN : [Sun Jun 18 19:48:36 2006] MODIFY_CNF 1195 END : 3838923 bytes (0 seconds) [Sun Jun 18 19:48:36 2006] MODIFY_CNF 1195 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1195 BEGIN : [Sun Jun 18 19:48:36 2006] CMD : minisat /tmp/csp2sat13650.cnf /tmp/csp2sat13650.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 134079 373108 | 44693 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 1 (4 /sec) decisions : 31 (124 /sec) propagations : 33037 (132148 /sec) conflict literals : 8 (11.11 % deleted) Memory used : 10.24 MB CPU time : 0.25 s SATISFIABLE VERIFY_CNF 1195 END : (0 seconds) [Sun Jun 18 19:48:36 2006] VERIFY_CNF 1195 CPU : 0.3 = 0 + 0.01 + 0.27 + 0.02 # RESULT : makespan 1195 SATISFIABLE SHOW_RESULT 1195 BEGIN : [Sun Jun 18 19:48:36 2006] # ASSIGN : makespan 1195 # ASSIGN : s_0_0 271 # ASSIGN : s_0_1 71 # ASSIGN : s_0_2 884 # ASSIGN : s_0_3 103 # ASSIGN : s_1_0 1136 # ASSIGN : s_1_1 575 # ASSIGN : s_1_2 57 # ASSIGN : s_1_3 463 # ASSIGN : s_2_0 60 # ASSIGN : s_2_1 136 # ASSIGN : s_2_2 340 # ASSIGN : s_2_3 516 # ASSIGN : s_3_0 697 # ASSIGN : s_3_1 219 # ASSIGN : s_3_2 457 # ASSIGN : s_3_3 1187 SHOW_RESULT 1195 END : 1195 (0 seconds) [Sun Jun 18 19:48:36 2006] SHOW_RESULT 1195 CPU : 0.04 = 0.04 + 0 + 0 + 0 # BOUND : makespan 1000 1195 MODIFY_CNF 1097 BEGIN : [Sun Jun 18 19:48:36 2006] MODIFY_CNF 1097 END : 3838922 bytes (0 seconds) [Sun Jun 18 19:48:36 2006] MODIFY_CNF 1097 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1097 BEGIN : [Sun Jun 18 19:48:36 2006] CMD : minisat /tmp/csp2sat13650.cnf /tmp/csp2sat13650.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 124671 344884 | 41557 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 4 (15 /sec) decisions : 35 (135 /sec) propagations : 41914 (161208 /sec) conflict literals : 18 (0.00 % deleted) Memory used : 10.27 MB CPU time : 0.26 s SATISFIABLE VERIFY_CNF 1097 END : (0 seconds) [Sun Jun 18 19:48:36 2006] VERIFY_CNF 1097 CPU : 0.31 = 0 + 0.01 + 0.28 + 0.02 # RESULT : makespan 1097 SATISFIABLE SHOW_RESULT 1097 BEGIN : [Sun Jun 18 19:48:36 2006] # ASSIGN : makespan 1097 # ASSIGN : s_0_0 595 # ASSIGN : s_0_1 221 # ASSIGN : s_0_2 263 # ASSIGN : s_0_3 32 # ASSIGN : s_1_0 76 # ASSIGN : s_1_1 253 # ASSIGN : s_1_2 814 # ASSIGN : s_1_3 200 # ASSIGN : s_2_0 1021 # ASSIGN : s_2_1 63 # ASSIGN : s_2_2 146 # ASSIGN : s_2_3 350 # ASSIGN : s_3_0 135 # ASSIGN : s_3_1 851 # ASSIGN : s_3_2 574 # ASSIGN : s_3_3 1089 SHOW_RESULT 1097 END : 1097 (0 seconds) [Sun Jun 18 19:48:36 2006] SHOW_RESULT 1097 CPU : 0.04 = 0.04 + 0 + 0 + 0 # BOUND : makespan 1000 1097 MODIFY_CNF 1048 BEGIN : [Sun Jun 18 19:48:36 2006] MODIFY_CNF 1048 END : 3838922 bytes (0 seconds) [Sun Jun 18 19:48:36 2006] MODIFY_CNF 1048 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1048 BEGIN : [Sun Jun 18 19:48:36 2006] CMD : minisat /tmp/csp2sat13650.cnf /tmp/csp2sat13650.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 119967 330772 | 39989 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 7 (27 /sec) decisions : 23 (88 /sec) propagations : 44089 (169573 /sec) conflict literals : 23 (11.54 % deleted) Memory used : 10.27 MB CPU time : 0.26 s SATISFIABLE VERIFY_CNF 1048 END : (1 seconds) [Sun Jun 18 19:48:37 2006] VERIFY_CNF 1048 CPU : 0.3 = 0 + 0 + 0.28 + 0.02 # RESULT : makespan 1048 SATISFIABLE SHOW_RESULT 1048 BEGIN : [Sun Jun 18 19:48:37 2006] # ASSIGN : makespan 1048 # ASSIGN : s_0_0 446 # ASSIGN : s_0_1 103 # ASSIGN : s_0_2 135 # ASSIGN : s_0_3 872 # ASSIGN : s_1_0 989 # ASSIGN : s_1_1 145 # ASSIGN : s_1_2 706 # ASSIGN : s_1_3 92 # ASSIGN : s_2_0 889 # ASSIGN : s_2_1 965 # ASSIGN : s_2_2 18 # ASSIGN : s_2_3 201 # ASSIGN : s_3_0 7 # ASSIGN : s_3_1 727 # ASSIGN : s_3_2 466 # ASSIGN : s_3_3 1040 SHOW_RESULT 1048 END : 1048 (0 seconds) [Sun Jun 18 19:48:37 2006] SHOW_RESULT 1048 CPU : 0.04 = 0.04 + 0 + 0 + 0 # BOUND : makespan 1000 1048 MODIFY_CNF 1024 BEGIN : [Sun Jun 18 19:48:37 2006] MODIFY_CNF 1024 END : 3838922 bytes (0 seconds) [Sun Jun 18 19:48:37 2006] MODIFY_CNF 1024 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1024 BEGIN : [Sun Jun 18 19:48:37 2006] CMD : minisat /tmp/csp2sat13650.cnf /tmp/csp2sat13650.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 117663 323860 | 39221 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 8 (33 /sec) decisions : 9 (38 /sec) propagations : 41112 (171300 /sec) conflict literals : 12 (7.69 % deleted) Memory used : 10.13 MB CPU time : 0.24 s UNSATISFIABLE VERIFY_CNF 1024 END : (0 seconds) [Sun Jun 18 19:48:37 2006] VERIFY_CNF 1024 CPU : 0.28 = 0 + 0 + 0.24 + 0.04 # RESULT : makespan 1024 UNSATISFIABLE # BOUND : makespan 1025 1048 MODIFY_CNF 1036 BEGIN : [Sun Jun 18 19:48:37 2006] MODIFY_CNF 1036 END : 3838922 bytes (0 seconds) [Sun Jun 18 19:48:37 2006] MODIFY_CNF 1036 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1036 BEGIN : [Sun Jun 18 19:48:37 2006] CMD : minisat /tmp/csp2sat13650.cnf /tmp/csp2sat13650.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 118815 327316 | 39605 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 9 (33 /sec) decisions : 10 (37 /sec) propagations : 54601 (202226 /sec) conflict literals : 21 (12.50 % deleted) Memory used : 10.15 MB CPU time : 0.27 s UNSATISFIABLE VERIFY_CNF 1036 END : (0 seconds) [Sun Jun 18 19:48:37 2006] VERIFY_CNF 1036 CPU : 0.3 = 0.00999999999999979 + 0 + 0.27 + 0.02 # RESULT : makespan 1036 UNSATISFIABLE # BOUND : makespan 1037 1048 MODIFY_CNF 1042 BEGIN : [Sun Jun 18 19:48:37 2006] MODIFY_CNF 1042 END : 3838922 bytes (0 seconds) [Sun Jun 18 19:48:37 2006] MODIFY_CNF 1042 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1042 BEGIN : [Sun Jun 18 19:48:37 2006] CMD : minisat /tmp/csp2sat13650.cnf /tmp/csp2sat13650.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 119391 329044 | 39797 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 7 (25 /sec) decisions : 23 (82 /sec) propagations : 44662 (159507 /sec) conflict literals : 23 (11.54 % deleted) Memory used : 10.27 MB CPU time : 0.28 s SATISFIABLE VERIFY_CNF 1042 END : (1 seconds) [Sun Jun 18 19:48:38 2006] VERIFY_CNF 1042 CPU : 0.31 = 0 + 0 + 0.3 + 0.01 # RESULT : makespan 1042 SATISFIABLE SHOW_RESULT 1042 BEGIN : [Sun Jun 18 19:48:38 2006] # ASSIGN : makespan 1042 # ASSIGN : s_0_0 440 # ASSIGN : s_0_1 97 # ASSIGN : s_0_2 129 # ASSIGN : s_0_3 866 # ASSIGN : s_1_0 983 # ASSIGN : s_1_1 139 # ASSIGN : s_1_2 700 # ASSIGN : s_1_3 86 # ASSIGN : s_2_0 883 # ASSIGN : s_2_1 959 # ASSIGN : s_2_2 12 # ASSIGN : s_2_3 195 # ASSIGN : s_3_0 1 # ASSIGN : s_3_1 721 # ASSIGN : s_3_2 460 # ASSIGN : s_3_3 1034 SHOW_RESULT 1042 END : 1042 (0 seconds) [Sun Jun 18 19:48:38 2006] SHOW_RESULT 1042 CPU : 0.0500000000000007 = 0.0500000000000007 + 0 + 0 + 0 # BOUND : makespan 1037 1042 MODIFY_CNF 1039 BEGIN : [Sun Jun 18 19:48:38 2006] MODIFY_CNF 1039 END : 3838922 bytes (0 seconds) [Sun Jun 18 19:48:38 2006] MODIFY_CNF 1039 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1039 BEGIN : [Sun Jun 18 19:48:38 2006] CMD : minisat /tmp/csp2sat13650.cnf /tmp/csp2sat13650.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 119103 328180 | 39701 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 9 (33 /sec) decisions : 10 (37 /sec) propagations : 53741 (199041 /sec) conflict literals : 20 (13.04 % deleted) Memory used : 10.15 MB CPU time : 0.27 s UNSATISFIABLE VERIFY_CNF 1039 END : (0 seconds) [Sun Jun 18 19:48:38 2006] VERIFY_CNF 1039 CPU : 0.29 = 0 + 0 + 0.27 + 0.02 # RESULT : makespan 1039 UNSATISFIABLE # BOUND : makespan 1040 1042 MODIFY_CNF 1041 BEGIN : [Sun Jun 18 19:48:38 2006] MODIFY_CNF 1041 END : 3838922 bytes (0 seconds) [Sun Jun 18 19:48:38 2006] MODIFY_CNF 1041 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1041 BEGIN : [Sun Jun 18 19:48:38 2006] CMD : minisat /tmp/csp2sat13650.cnf /tmp/csp2sat13650.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 119295 328756 | 39765 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 7 (26 /sec) decisions : 21 (78 /sec) propagations : 44661 (165411 /sec) conflict literals : 23 (11.54 % deleted) Memory used : 10.27 MB CPU time : 0.27 s SATISFIABLE VERIFY_CNF 1041 END : (0 seconds) [Sun Jun 18 19:48:38 2006] VERIFY_CNF 1041 CPU : 0.3 = 0 + 0 + 0.28 + 0.02 # RESULT : makespan 1041 SATISFIABLE SHOW_RESULT 1041 BEGIN : [Sun Jun 18 19:48:38 2006] # ASSIGN : makespan 1041 # ASSIGN : s_0_0 439 # ASSIGN : s_0_1 96 # ASSIGN : s_0_2 128 # ASSIGN : s_0_3 865 # ASSIGN : s_1_0 982 # ASSIGN : s_1_1 138 # ASSIGN : s_1_2 699 # ASSIGN : s_1_3 85 # ASSIGN : s_2_0 882 # ASSIGN : s_2_1 958 # ASSIGN : s_2_2 11 # ASSIGN : s_2_3 194 # ASSIGN : s_3_0 0 # ASSIGN : s_3_1 720 # ASSIGN : s_3_2 459 # ASSIGN : s_3_3 1033 SHOW_RESULT 1041 END : 1041 (0 seconds) [Sun Jun 18 19:48:38 2006] SHOW_RESULT 1041 CPU : 0.04 = 0.04 + 0 + 0 + 0 # BOUND : makespan 1040 1041 MODIFY_CNF 1040 BEGIN : [Sun Jun 18 19:48:38 2006] MODIFY_CNF 1040 END : 3838922 bytes (0 seconds) [Sun Jun 18 19:48:38 2006] MODIFY_CNF 1040 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1040 BEGIN : [Sun Jun 18 19:48:38 2006] CMD : minisat /tmp/csp2sat13650.cnf /tmp/csp2sat13650.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 119199 328468 | 39733 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 9 (36 /sec) decisions : 10 (40 /sec) propagations : 53489 (213956 /sec) conflict literals : 20 (13.04 % deleted) Memory used : 10.14 MB CPU time : 0.25 s UNSATISFIABLE VERIFY_CNF 1040 END : (1 seconds) [Sun Jun 18 19:48:39 2006] VERIFY_CNF 1040 CPU : 0.29 = 0 + 0 + 0.26 + 0.03 # RESULT : makespan 1040 UNSATISFIABLE # BOUND : makespan 1041 1041 MAIN END : (11 seconds) [Sun Jun 18 19:48:39 2006] MAIN CPU : 10.06 = 7.07 + 0.07 + 2.71 + 0.21