# TIMEOUT 18000 MAIN BEGIN : [Sun Jun 18 19:48:08 2006] READ BEGIN : csp/j4-per0-1.csp [Sun Jun 18 19:48:08 2006] READ END : csp/j4-per0-1.csp (0 seconds) [Sun Jun 18 19:48:08 2006] READ CPU : 0.12 = 0.12 + 0 + 0 + 0 # BOUND : makespan 1000 1942 GENERATE_CNF 1942 BEGIN : [Sun Jun 18 19:48:08 2006] GENERATE_CNF 1942 END : 32160 variables 209841 clauses 4237271 bytes (8 seconds) [Sun Jun 18 19:48:16 2006] GENERATE_CNF 1942 CPU : 7.53 = 7.5 + 0.03 + 0 + 0 MODIFY_CNF 1471 BEGIN : [Sun Jun 18 19:48:16 2006] MODIFY_CNF 1471 END : 4237277 bytes (0 seconds) [Sun Jun 18 19:48:16 2006] MODIFY_CNF 1471 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1471 BEGIN : [Sun Jun 18 19:48:16 2006] CMD : minisat /tmp/csp2sat13626.cnf /tmp/csp2sat13626.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 164412 461404 | 54804 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 3 (11 /sec) decisions : 56 (207 /sec) propagations : 51342 (190156 /sec) conflict literals : 13 (0.00 % deleted) Memory used : 10.98 MB CPU time : 0.27 s SATISFIABLE VERIFY_CNF 1471 END : (1 seconds) [Sun Jun 18 19:48:17 2006] VERIFY_CNF 1471 CPU : 0.32 = 0 + 0 + 0.28 + 0.04 # RESULT : makespan 1471 SATISFIABLE SHOW_RESULT 1471 BEGIN : [Sun Jun 18 19:48:17 2006] # ASSIGN : makespan 1471 # ASSIGN : s_0_0 470 # ASSIGN : s_0_1 138 # ASSIGN : s_0_2 200 # ASSIGN : s_0_3 471 # ASSIGN : s_1_0 167 # ASSIGN : s_1_1 846 # ASSIGN : s_1_2 676 # ASSIGN : s_1_3 1138 # ASSIGN : s_2_0 101 # ASSIGN : s_2_1 290 # ASSIGN : s_2_2 855 # ASSIGN : s_2_3 1410 # ASSIGN : s_3_0 471 # ASSIGN : s_3_1 1101 # ASSIGN : s_3_2 1228 # ASSIGN : s_3_3 1415 SHOW_RESULT 1471 END : 1471 (0 seconds) [Sun Jun 18 19:48:17 2006] SHOW_RESULT 1471 CPU : 0.05 = 0.04 + 0.01 + 0 + 0 # BOUND : makespan 1000 1471 MODIFY_CNF 1235 BEGIN : [Sun Jun 18 19:48:17 2006] MODIFY_CNF 1235 END : 4237277 bytes (0 seconds) [Sun Jun 18 19:48:17 2006] MODIFY_CNF 1235 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1235 BEGIN : [Sun Jun 18 19:48:17 2006] CMD : minisat /tmp/csp2sat13626.cnf /tmp/csp2sat13626.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 141756 393436 | 47252 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (8 /sec) decisions : 26 (100 /sec) propagations : 39558 (152146 /sec) conflict literals : 15 (11.76 % deleted) Memory used : 11.13 MB CPU time : 0.26 s SATISFIABLE VERIFY_CNF 1235 END : (0 seconds) [Sun Jun 18 19:48:17 2006] VERIFY_CNF 1235 CPU : 0.32 = 0 + 0 + 0.27 + 0.05 # RESULT : makespan 1235 SATISFIABLE SHOW_RESULT 1235 BEGIN : [Sun Jun 18 19:48:17 2006] # ASSIGN : makespan 1235 # ASSIGN : s_0_0 118 # ASSIGN : s_0_1 903 # ASSIGN : s_0_2 965 # ASSIGN : s_0_3 235 # ASSIGN : s_1_0 119 # ASSIGN : s_1_1 647 # ASSIGN : s_1_2 422 # ASSIGN : s_1_3 902 # ASSIGN : s_2_0 1108 # ASSIGN : s_2_1 36 # ASSIGN : s_2_2 592 # ASSIGN : s_2_3 1174 # ASSIGN : s_3_0 422 # ASSIGN : s_3_1 1052 # ASSIGN : s_3_2 235 # ASSIGN : s_3_3 1179 SHOW_RESULT 1235 END : 1235 (0 seconds) [Sun Jun 18 19:48:17 2006] SHOW_RESULT 1235 CPU : 0.0499999999999998 = 0.0499999999999998 + 0 + 0 + 0 # BOUND : makespan 1000 1235 MODIFY_CNF 1117 BEGIN : [Sun Jun 18 19:48:17 2006] MODIFY_CNF 1117 END : 4237277 bytes (0 seconds) [Sun Jun 18 19:48:17 2006] MODIFY_CNF 1117 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1117 BEGIN : [Sun Jun 18 19:48:17 2006] CMD : minisat /tmp/csp2sat13626.cnf /tmp/csp2sat13626.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 130428 359452 | 43476 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 7 (23 /sec) decisions : 7 (23 /sec) propagations : 43639 (145463 /sec) conflict literals : 12 (7.69 % deleted) Memory used : 10.98 MB CPU time : 0.3 s UNSATISFIABLE VERIFY_CNF 1117 END : (0 seconds) [Sun Jun 18 19:48:17 2006] VERIFY_CNF 1117 CPU : 0.32 = 0 + 0 + 0.3 + 0.02 # RESULT : makespan 1117 UNSATISFIABLE # BOUND : makespan 1118 1235 MODIFY_CNF 1176 BEGIN : [Sun Jun 18 19:48:17 2006] MODIFY_CNF 1176 END : 4237277 bytes (0 seconds) [Sun Jun 18 19:48:17 2006] MODIFY_CNF 1176 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1176 BEGIN : [Sun Jun 18 19:48:17 2006] CMD : minisat /tmp/csp2sat13626.cnf /tmp/csp2sat13626.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 136092 376444 | 45364 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 7 (25 /sec) decisions : 7 (25 /sec) propagations : 46387 (165668 /sec) conflict literals : 13 (7.14 % deleted) Memory used : 10.98 MB CPU time : 0.28 s UNSATISFIABLE VERIFY_CNF 1176 END : (1 seconds) [Sun Jun 18 19:48:18 2006] VERIFY_CNF 1176 CPU : 0.31 = 0 + 0 + 0.28 + 0.03 # RESULT : makespan 1176 UNSATISFIABLE # BOUND : makespan 1177 1235 MODIFY_CNF 1206 BEGIN : [Sun Jun 18 19:48:18 2006] MODIFY_CNF 1206 END : 4237277 bytes (0 seconds) [Sun Jun 18 19:48:18 2006] MODIFY_CNF 1206 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1206 BEGIN : [Sun Jun 18 19:48:18 2006] CMD : minisat /tmp/csp2sat13626.cnf /tmp/csp2sat13626.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 138972 385084 | 46324 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (7 /sec) decisions : 26 (87 /sec) propagations : 39558 (131860 /sec) conflict literals : 13 (23.53 % deleted) Memory used : 11.13 MB CPU time : 0.3 s SATISFIABLE VERIFY_CNF 1206 END : (0 seconds) [Sun Jun 18 19:48:18 2006] VERIFY_CNF 1206 CPU : 0.33 = 0 + 0 + 0.31 + 0.02 # RESULT : makespan 1206 SATISFIABLE SHOW_RESULT 1206 BEGIN : [Sun Jun 18 19:48:18 2006] # ASSIGN : makespan 1206 # ASSIGN : s_0_0 89 # ASSIGN : s_0_1 874 # ASSIGN : s_0_2 936 # ASSIGN : s_0_3 206 # ASSIGN : s_1_0 90 # ASSIGN : s_1_1 618 # ASSIGN : s_1_2 393 # ASSIGN : s_1_3 873 # ASSIGN : s_2_0 1079 # ASSIGN : s_2_1 7 # ASSIGN : s_2_2 563 # ASSIGN : s_2_3 1145 # ASSIGN : s_3_0 393 # ASSIGN : s_3_1 1023 # ASSIGN : s_3_2 206 # ASSIGN : s_3_3 1150 SHOW_RESULT 1206 END : 1206 (0 seconds) [Sun Jun 18 19:48:18 2006] SHOW_RESULT 1206 CPU : 0.0499999999999991 = 0.0399999999999991 + 0.01 + 0 + 0 # BOUND : makespan 1177 1206 MODIFY_CNF 1191 BEGIN : [Sun Jun 18 19:48:18 2006] MODIFY_CNF 1191 END : 4237277 bytes (0 seconds) [Sun Jun 18 19:48:18 2006] MODIFY_CNF 1191 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1191 BEGIN : [Sun Jun 18 19:48:18 2006] CMD : minisat /tmp/csp2sat13626.cnf /tmp/csp2sat13626.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 137532 380764 | 45844 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (7 /sec) decisions : 26 (87 /sec) propagations : 43489 (144963 /sec) conflict literals : 9 (25.00 % deleted) Memory used : 11.13 MB CPU time : 0.3 s SATISFIABLE VERIFY_CNF 1191 END : (0 seconds) [Sun Jun 18 19:48:18 2006] VERIFY_CNF 1191 CPU : 0.34 = 0 + 0 + 0.32 + 0.02 # RESULT : makespan 1191 SATISFIABLE SHOW_RESULT 1191 BEGIN : [Sun Jun 18 19:48:18 2006] # ASSIGN : makespan 1191 # ASSIGN : s_0_0 1124 # ASSIGN : s_0_1 1129 # ASSIGN : s_0_2 6 # ASSIGN : s_0_3 276 # ASSIGN : s_1_0 821 # ASSIGN : s_1_1 566 # ASSIGN : s_1_2 396 # ASSIGN : s_1_3 4 # ASSIGN : s_2_0 1125 # ASSIGN : s_2_1 10 # ASSIGN : s_2_2 570 # ASSIGN : s_2_3 943 # ASSIGN : s_3_0 191 # ASSIGN : s_3_1 821 # ASSIGN : s_3_2 1004 # ASSIGN : s_3_3 948 SHOW_RESULT 1191 END : 1191 (0 seconds) [Sun Jun 18 19:48:18 2006] SHOW_RESULT 1191 CPU : 0.04 = 0.04 + 0 + 0 + 0 # BOUND : makespan 1177 1191 MODIFY_CNF 1184 BEGIN : [Sun Jun 18 19:48:18 2006] MODIFY_CNF 1184 END : 4237277 bytes (0 seconds) [Sun Jun 18 19:48:18 2006] MODIFY_CNF 1184 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1184 BEGIN : [Sun Jun 18 19:48:18 2006] CMD : minisat /tmp/csp2sat13626.cnf /tmp/csp2sat13626.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 136860 378748 | 45620 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 1 (3 /sec) decisions : 25 (83 /sec) propagations : 36834 (122780 /sec) conflict literals : 4 (33.33 % deleted) Memory used : 11.13 MB CPU time : 0.3 s SATISFIABLE VERIFY_CNF 1184 END : (1 seconds) [Sun Jun 18 19:48:19 2006] VERIFY_CNF 1184 CPU : 0.33 = 0 + 0 + 0.32 + 0.01 # RESULT : makespan 1184 SATISFIABLE SHOW_RESULT 1184 BEGIN : [Sun Jun 18 19:48:19 2006] # ASSIGN : makespan 1184 # ASSIGN : s_0_0 175 # ASSIGN : s_0_1 1122 # ASSIGN : s_0_2 176 # ASSIGN : s_0_3 446 # ASSIGN : s_1_0 815 # ASSIGN : s_1_1 559 # ASSIGN : s_1_2 4 # ASSIGN : s_1_3 174 # ASSIGN : s_2_0 1118 # ASSIGN : s_2_1 3 # ASSIGN : s_2_2 568 # ASSIGN : s_2_3 1113 # ASSIGN : s_3_0 184 # ASSIGN : s_3_1 814 # ASSIGN : s_3_2 941 # ASSIGN : s_3_3 1128 SHOW_RESULT 1184 END : 1184 (0 seconds) [Sun Jun 18 19:48:19 2006] SHOW_RESULT 1184 CPU : 0.04 = 0.04 + 0 + 0 + 0 # BOUND : makespan 1177 1184 MODIFY_CNF 1180 BEGIN : [Sun Jun 18 19:48:19 2006] MODIFY_CNF 1180 END : 4237277 bytes (0 seconds) [Sun Jun 18 19:48:19 2006] MODIFY_CNF 1180 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1180 BEGIN : [Sun Jun 18 19:48:19 2006] CMD : minisat /tmp/csp2sat13626.cnf /tmp/csp2sat13626.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 136476 377596 | 45492 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 5 (18 /sec) decisions : 21 (75 /sec) propagations : 46573 (166332 /sec) conflict literals : 15 (16.67 % deleted) Memory used : 11.13 MB CPU time : 0.28 s SATISFIABLE VERIFY_CNF 1180 END : (0 seconds) [Sun Jun 18 19:48:19 2006] VERIFY_CNF 1180 CPU : 0.360000000000001 = 0.0100000000000007 + 0 + 0.29 + 0.06 # RESULT : makespan 1180 SATISFIABLE SHOW_RESULT 1180 BEGIN : [Sun Jun 18 19:48:19 2006] # ASSIGN : makespan 1180 # ASSIGN : s_0_0 1179 # ASSIGN : s_0_1 123 # ASSIGN : s_0_2 909 # ASSIGN : s_0_3 185 # ASSIGN : s_1_0 66 # ASSIGN : s_1_1 369 # ASSIGN : s_1_2 682 # ASSIGN : s_1_3 852 # ASSIGN : s_2_0 0 # ASSIGN : s_2_1 624 # ASSIGN : s_2_2 251 # ASSIGN : s_2_3 180 # ASSIGN : s_3_0 494 # ASSIGN : s_3_1 242 # ASSIGN : s_3_2 55 # ASSIGN : s_3_3 1124 SHOW_RESULT 1180 END : 1180 (0 seconds) [Sun Jun 18 19:48:19 2006] SHOW_RESULT 1180 CPU : 0.0499999999999998 = 0.0499999999999998 + 0 + 0 + 0 # BOUND : makespan 1177 1180 MODIFY_CNF 1178 BEGIN : [Sun Jun 18 19:48:19 2006] MODIFY_CNF 1178 END : 4237277 bytes (0 seconds) [Sun Jun 18 19:48:19 2006] MODIFY_CNF 1178 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1178 BEGIN : [Sun Jun 18 19:48:19 2006] CMD : minisat /tmp/csp2sat13626.cnf /tmp/csp2sat13626.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 136284 377020 | 45428 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 7 (23 /sec) decisions : 7 (23 /sec) propagations : 47978 (159927 /sec) conflict literals : 13 (7.14 % deleted) Memory used : 10.98 MB CPU time : 0.3 s UNSATISFIABLE VERIFY_CNF 1178 END : (0 seconds) [Sun Jun 18 19:48:19 2006] VERIFY_CNF 1178 CPU : 0.31 = 0 + 0 + 0.3 + 0.01 # RESULT : makespan 1178 UNSATISFIABLE # BOUND : makespan 1179 1180 MODIFY_CNF 1179 BEGIN : [Sun Jun 18 19:48:19 2006] MODIFY_CNF 1179 END : 4237277 bytes (0 seconds) [Sun Jun 18 19:48:19 2006] MODIFY_CNF 1179 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1179 BEGIN : [Sun Jun 18 19:48:19 2006] CMD : minisat /tmp/csp2sat13626.cnf /tmp/csp2sat13626.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 136380 377308 | 45460 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 7 (24 /sec) decisions : 7 (24 /sec) propagations : 47960 (165379 /sec) conflict literals : 13 (7.14 % deleted) Memory used : 10.98 MB CPU time : 0.29 s UNSATISFIABLE VERIFY_CNF 1179 END : (1 seconds) [Sun Jun 18 19:48:20 2006] VERIFY_CNF 1179 CPU : 0.31 = 0 + 0 + 0.29 + 0.02 # RESULT : makespan 1179 UNSATISFIABLE # BOUND : makespan 1180 1180 MAIN END : (12 seconds) [Sun Jun 18 19:48:20 2006] MAIN CPU : 11.19 = 7.9 + 0.05 + 2.96 + 0.28