# TIMEOUT 18000 MAIN BEGIN : [Sun Jun 18 16:07:46 2006] READ BEGIN : csp/gp04-03.csp [Sun Jun 18 16:07:46 2006] READ END : csp/gp04-03.csp (0 seconds) [Sun Jun 18 16:07:46 2006] READ CPU : 0.12 = 0.11 + 0.01 + 0 + 0 # BOUND : makespan 1000 1708 GENERATE_CNF 1708 BEGIN : [Sun Jun 18 16:07:46 2006] GENERATE_CNF 1708 END : 28182 variables 179655 clauses 3605218 bytes (7 seconds) [Sun Jun 18 16:07:53 2006] GENERATE_CNF 1708 CPU : 6.68 = 6.67 + 0.01 + 0 + 0 MODIFY_CNF 1354 BEGIN : [Sun Jun 18 16:07:53 2006] MODIFY_CNF 1354 END : 3605224 bytes (0 seconds) [Sun Jun 18 16:07:53 2006] MODIFY_CNF 1354 CPU : 0.01 = 0 + 0.01 + 0 + 0 VERIFY_CNF 1354 BEGIN : [Sun Jun 18 16:07:53 2006] CMD : minisat /tmp/csp2sat8783.cnf /tmp/csp2sat8783.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 145458 408520 | 48486 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 34 (162 /sec) propagations : 28182 (134200 /sec) conflict literals : 0 ( nan % deleted) Memory used : 9.71 MB CPU time : 0.21 s SATISFIABLE VERIFY_CNF 1354 END : (0 seconds) [Sun Jun 18 16:07:53 2006] VERIFY_CNF 1354 CPU : 0.26 = 0 + 0 + 0.22 + 0.04 # RESULT : makespan 1354 SATISFIABLE SHOW_RESULT 1354 BEGIN : [Sun Jun 18 16:07:53 2006] # ASSIGN : makespan 1354 # ASSIGN : s_0_0 676 # ASSIGN : s_0_1 14 # ASSIGN : s_0_2 16 # ASSIGN : s_0_3 316 # ASSIGN : s_1_0 1312 # ASSIGN : s_1_1 30 # ASSIGN : s_1_2 18 # ASSIGN : s_1_3 714 # ASSIGN : s_2_0 324 # ASSIGN : s_2_1 28 # ASSIGN : s_2_2 358 # ASSIGN : s_2_3 1044 # ASSIGN : s_3_0 354 # ASSIGN : s_3_1 646 # ASSIGN : s_3_2 1026 # ASSIGN : s_3_3 1344 SHOW_RESULT 1354 END : 1354 (0 seconds) [Sun Jun 18 16:07:53 2006] SHOW_RESULT 1354 CPU : 0.04 = 0.04 + 0 + 0 + 0 # BOUND : makespan 1000 1354 MODIFY_CNF 1177 BEGIN : [Sun Jun 18 16:07:53 2006] MODIFY_CNF 1177 END : 3605224 bytes (0 seconds) [Sun Jun 18 16:07:53 2006] MODIFY_CNF 1177 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1177 BEGIN : [Sun Jun 18 16:07:53 2006] CMD : minisat /tmp/csp2sat8783.cnf /tmp/csp2sat8783.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 128466 357544 | 42822 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (9 /sec) decisions : 3 (14 /sec) propagations : 17487 (79486 /sec) conflict literals : 1 (0.00 % deleted) Memory used : 9.62 MB CPU time : 0.22 s UNSATISFIABLE VERIFY_CNF 1177 END : (1 seconds) [Sun Jun 18 16:07:54 2006] VERIFY_CNF 1177 CPU : 0.24 = 0 + 0 + 0.22 + 0.02 # RESULT : makespan 1177 UNSATISFIABLE # BOUND : makespan 1178 1354 MODIFY_CNF 1266 BEGIN : [Sun Jun 18 16:07:54 2006] MODIFY_CNF 1266 END : 3605224 bytes (0 seconds) [Sun Jun 18 16:07:54 2006] MODIFY_CNF 1266 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1266 BEGIN : [Sun Jun 18 16:07:54 2006] CMD : minisat /tmp/csp2sat8783.cnf /tmp/csp2sat8783.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 137010 383176 | 45670 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (10 /sec) decisions : 3 (14 /sec) propagations : 17102 (81438 /sec) conflict literals : 1 (0.00 % deleted) Memory used : 9.58 MB CPU time : 0.21 s UNSATISFIABLE VERIFY_CNF 1266 END : (0 seconds) [Sun Jun 18 16:07:54 2006] VERIFY_CNF 1266 CPU : 0.24 = 0 + 0 + 0.21 + 0.03 # RESULT : makespan 1266 UNSATISFIABLE # BOUND : makespan 1267 1354 MODIFY_CNF 1310 BEGIN : [Sun Jun 18 16:07:54 2006] MODIFY_CNF 1310 END : 3605224 bytes (0 seconds) [Sun Jun 18 16:07:54 2006] MODIFY_CNF 1310 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1310 BEGIN : [Sun Jun 18 16:07:54 2006] CMD : minisat /tmp/csp2sat8783.cnf /tmp/csp2sat8783.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 141234 395848 | 47078 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 1 (4 /sec) decisions : 27 (117 /sec) propagations : 30480 (132522 /sec) conflict literals : 5 (28.57 % deleted) Memory used : 9.73 MB CPU time : 0.23 s SATISFIABLE VERIFY_CNF 1310 END : (0 seconds) [Sun Jun 18 16:07:54 2006] VERIFY_CNF 1310 CPU : 0.27 = 0 + 0 + 0.25 + 0.02 # RESULT : makespan 1310 SATISFIABLE SHOW_RESULT 1310 BEGIN : [Sun Jun 18 16:07:54 2006] # ASSIGN : makespan 1310 # ASSIGN : s_0_0 644 # ASSIGN : s_0_1 0 # ASSIGN : s_0_2 2 # ASSIGN : s_0_3 4 # ASSIGN : s_1_0 322 # ASSIGN : s_1_1 694 # ASSIGN : s_1_2 300 # ASSIGN : s_1_3 364 # ASSIGN : s_2_0 1280 # ASSIGN : s_2_1 310 # ASSIGN : s_2_2 312 # ASSIGN : s_2_3 980 # ASSIGN : s_3_0 22 # ASSIGN : s_3_1 314 # ASSIGN : s_3_2 982 # ASSIGN : s_3_3 1300 SHOW_RESULT 1310 END : 1310 (0 seconds) [Sun Jun 18 16:07:54 2006] SHOW_RESULT 1310 CPU : 0.04 = 0.04 + 0 + 0 + 0 # BOUND : makespan 1267 1310 MODIFY_CNF 1288 BEGIN : [Sun Jun 18 16:07:54 2006] MODIFY_CNF 1288 END : 3605224 bytes (0 seconds) [Sun Jun 18 16:07:54 2006] MODIFY_CNF 1288 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1288 BEGIN : [Sun Jun 18 16:07:54 2006] CMD : minisat /tmp/csp2sat8783.cnf /tmp/csp2sat8783.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 139122 389512 | 46374 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 1 (5 /sec) decisions : 21 (100 /sec) propagations : 30244 (144019 /sec) conflict literals : 2 (0.00 % deleted) Memory used : 9.73 MB CPU time : 0.21 s SATISFIABLE VERIFY_CNF 1288 END : (0 seconds) [Sun Jun 18 16:07:54 2006] VERIFY_CNF 1288 CPU : 0.27 = 0 + 0 + 0.22 + 0.05 # RESULT : makespan 1288 SATISFIABLE SHOW_RESULT 1288 BEGIN : [Sun Jun 18 16:07:54 2006] # ASSIGN : makespan 1288 # ASSIGN : s_0_0 42 # ASSIGN : s_0_1 38 # ASSIGN : s_0_2 40 # ASSIGN : s_0_3 928 # ASSIGN : s_1_0 0 # ASSIGN : s_1_1 670 # ASSIGN : s_1_2 290 # ASSIGN : s_1_3 338 # ASSIGN : s_2_0 1256 # ASSIGN : s_2_1 1286 # ASSIGN : s_2_2 302 # ASSIGN : s_2_3 2 # ASSIGN : s_3_0 678 # ASSIGN : s_3_1 288 # ASSIGN : s_3_2 970 # ASSIGN : s_3_3 668 SHOW_RESULT 1288 END : 1288 (0 seconds) [Sun Jun 18 16:07:54 2006] SHOW_RESULT 1288 CPU : 0.04 = 0.04 + 0 + 0 + 0 # BOUND : makespan 1267 1288 MODIFY_CNF 1277 BEGIN : [Sun Jun 18 16:07:54 2006] MODIFY_CNF 1277 END : 3605224 bytes (0 seconds) [Sun Jun 18 16:07:54 2006] MODIFY_CNF 1277 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1277 BEGIN : [Sun Jun 18 16:07:54 2006] CMD : minisat /tmp/csp2sat8783.cnf /tmp/csp2sat8783.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 138066 386344 | 46022 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (9 /sec) decisions : 3 (14 /sec) propagations : 16915 (76886 /sec) conflict literals : 1 (0.00 % deleted) Memory used : 9.58 MB CPU time : 0.22 s UNSATISFIABLE VERIFY_CNF 1277 END : (1 seconds) [Sun Jun 18 16:07:55 2006] VERIFY_CNF 1277 CPU : 0.24 = 0 + 0 + 0.22 + 0.02 # RESULT : makespan 1277 UNSATISFIABLE # BOUND : makespan 1278 1288 MODIFY_CNF 1283 BEGIN : [Sun Jun 18 16:07:55 2006] MODIFY_CNF 1283 END : 3605224 bytes (0 seconds) [Sun Jun 18 16:07:55 2006] MODIFY_CNF 1283 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1283 BEGIN : [Sun Jun 18 16:07:55 2006] CMD : minisat /tmp/csp2sat8783.cnf /tmp/csp2sat8783.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 138642 388072 | 46214 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (8 /sec) decisions : 3 (12 /sec) propagations : 16799 (69996 /sec) conflict literals : 1 (0.00 % deleted) Memory used : 9.58 MB CPU time : 0.24 s UNSATISFIABLE VERIFY_CNF 1283 END : (0 seconds) [Sun Jun 18 16:07:55 2006] VERIFY_CNF 1283 CPU : 0.26 = 0 + 0 + 0.24 + 0.02 # RESULT : makespan 1283 UNSATISFIABLE # BOUND : makespan 1284 1288 MODIFY_CNF 1286 BEGIN : [Sun Jun 18 16:07:55 2006] MODIFY_CNF 1286 END : 3605224 bytes (0 seconds) [Sun Jun 18 16:07:55 2006] MODIFY_CNF 1286 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1286 BEGIN : [Sun Jun 18 16:07:55 2006] CMD : minisat /tmp/csp2sat8783.cnf /tmp/csp2sat8783.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 138930 388936 | 46310 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 3 (9 /sec) decisions : 3 (9 /sec) propagations : 23172 (72412 /sec) conflict literals : 3 (0.00 % deleted) Memory used : 9.59 MB CPU time : 0.32 s UNSATISFIABLE VERIFY_CNF 1286 END : (0 seconds) [Sun Jun 18 16:07:55 2006] VERIFY_CNF 1286 CPU : 0.33 = 0 + 0 + 0.32 + 0.00999999999999998 # RESULT : makespan 1286 UNSATISFIABLE # BOUND : makespan 1287 1288 MODIFY_CNF 1287 BEGIN : [Sun Jun 18 16:07:55 2006] MODIFY_CNF 1287 END : 3605224 bytes (0 seconds) [Sun Jun 18 16:07:55 2006] MODIFY_CNF 1287 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1287 BEGIN : [Sun Jun 18 16:07:55 2006] CMD : minisat /tmp/csp2sat8783.cnf /tmp/csp2sat8783.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 139026 389224 | 46342 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 3 (13 /sec) decisions : 3 (13 /sec) propagations : 23154 (100670 /sec) conflict literals : 3 (0.00 % deleted) Memory used : 9.59 MB CPU time : 0.23 s UNSATISFIABLE VERIFY_CNF 1287 END : (1 seconds) [Sun Jun 18 16:07:56 2006] VERIFY_CNF 1287 CPU : 0.280000000000001 = 0.0100000000000007 + 0 + 0.23 + 0.04 # RESULT : makespan 1287 UNSATISFIABLE # BOUND : makespan 1288 1288 MAIN END : (10 seconds) [Sun Jun 18 16:07:56 2006] MAIN CPU : 9.33 = 6.92 + 0.03 + 2.13 + 0.25