# TIMEOUT 18000 MAIN BEGIN : [Sun Jun 18 16:17:54 2006] READ BEGIN : csp/gp06-04.csp [Sun Jun 18 16:17:54 2006] READ END : csp/gp06-04.csp (1 seconds) [Sun Jun 18 16:17:55 2006] READ CPU : 0.41 = 0.4 + 0.01 + 0 + 0 # BOUND : makespan 1000 2851 GENERATE_CNF 2851 BEGIN : [Sun Jun 18 16:17:55 2006] GENERATE_CNF 2851 END : 104957 variables 1138566 clauses 25161803 bytes (44 seconds) [Sun Jun 18 16:18:39 2006] GENERATE_CNF 2851 CPU : 43.98 = 43.79 + 0.19 + 0 + 0 MODIFY_CNF 1925 BEGIN : [Sun Jun 18 16:18:39 2006] MODIFY_CNF 1925 END : 25161809 bytes (0 seconds) [Sun Jun 18 16:18:39 2006] MODIFY_CNF 1925 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1925 BEGIN : [Sun Jun 18 16:18:39 2006] CMD : minisat /tmp/csp2sat9709.cnf /tmp/csp2sat9709.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 804589 2309754 | 268196 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (1 /sec) decisions : 171 (119 /sec) propagations : 117201 (81390 /sec) conflict literals : 10 (0.00 % deleted) Memory used : 48.79 MB CPU time : 1.44 s SATISFIABLE VERIFY_CNF 1925 END : (2 seconds) [Sun Jun 18 16:18:41 2006] VERIFY_CNF 1925 CPU : 1.68 = 0 + 0 + 1.49 + 0.19 # RESULT : makespan 1925 SATISFIABLE SHOW_RESULT 1925 BEGIN : [Sun Jun 18 16:18:41 2006] # ASSIGN : makespan 1925 # ASSIGN : s_0_0 512 # ASSIGN : s_0_1 197 # ASSIGN : s_0_2 198 # ASSIGN : s_0_3 218 # ASSIGN : s_0_4 880 # ASSIGN : s_0_5 846 # ASSIGN : s_1_0 883 # ASSIGN : s_1_1 549 # ASSIGN : s_1_2 244 # ASSIGN : s_1_3 1198 # ASSIGN : s_1_4 1197 # ASSIGN : s_1_5 884 # ASSIGN : s_2_0 885 # ASSIGN : s_2_1 901 # ASSIGN : s_2_2 270 # ASSIGN : s_2_3 1834 # ASSIGN : s_2_4 1227 # ASSIGN : s_2_5 886 # ASSIGN : s_3_0 888 # ASSIGN : s_3_1 1227 # ASSIGN : s_3_2 889 # ASSIGN : s_3_3 1886 # ASSIGN : s_3_4 1228 # ASSIGN : s_3_5 891 # ASSIGN : s_4_0 905 # ASSIGN : s_4_1 1239 # ASSIGN : s_4_2 917 # ASSIGN : s_4_3 1888 # ASSIGN : s_4_4 1901 # ASSIGN : s_4_5 1266 # ASSIGN : s_5_0 925 # ASSIGN : s_5_1 1576 # ASSIGN : s_5_2 1887 # ASSIGN : s_5_3 1902 # ASSIGN : s_5_4 1905 # ASSIGN : s_5_5 1924 SHOW_RESULT 1925 END : 1925 (0 seconds) [Sun Jun 18 16:18:41 2006] SHOW_RESULT 1925 CPU : 0.180000000000002 = 0.170000000000002 + 0.01 + 0 + 0 # BOUND : makespan 1000 1925 MODIFY_CNF 1462 BEGIN : [Sun Jun 18 16:18:41 2006] MODIFY_CNF 1462 END : 25161809 bytes (0 seconds) [Sun Jun 18 16:18:41 2006] MODIFY_CNF 1462 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1462 BEGIN : [Sun Jun 18 16:18:41 2006] CMD : minisat /tmp/csp2sat9709.cnf /tmp/csp2sat9709.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 637909 1809714 | 212636 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 1 (1 /sec) decisions : 123 (84 /sec) propagations : 108508 (74321 /sec) conflict literals : 6 (0.00 % deleted) Memory used : 48.79 MB CPU time : 1.46 s SATISFIABLE VERIFY_CNF 1462 END : (2 seconds) [Sun Jun 18 16:18:43 2006] VERIFY_CNF 1462 CPU : 1.7 = 0 + 0 + 1.51 + 0.19 # RESULT : makespan 1462 SATISFIABLE SHOW_RESULT 1462 BEGIN : [Sun Jun 18 16:18:43 2006] # ASSIGN : makespan 1462 # ASSIGN : s_0_0 1128 # ASSIGN : s_0_1 400 # ASSIGN : s_0_2 2 # ASSIGN : s_0_3 441 # ASSIGN : s_0_4 83 # ASSIGN : s_0_5 22 # ASSIGN : s_1_0 29 # ASSIGN : s_1_1 401 # ASSIGN : s_1_2 30 # ASSIGN : s_1_3 735 # ASSIGN : s_1_4 400 # ASSIGN : s_1_5 56 # ASSIGN : s_2_0 57 # ASSIGN : s_2_1 73 # ASSIGN : s_2_2 485 # ASSIGN : s_2_3 1371 # ASSIGN : s_2_4 441 # ASSIGN : s_2_5 58 # ASSIGN : s_3_0 62 # ASSIGN : s_3_1 399 # ASSIGN : s_3_2 1100 # ASSIGN : s_3_3 1423 # ASSIGN : s_3_4 442 # ASSIGN : s_3_5 63 # ASSIGN : s_4_0 441 # ASSIGN : s_4_1 1075 # ASSIGN : s_4_2 1102 # ASSIGN : s_4_3 1425 # ASSIGN : s_4_4 1438 # ASSIGN : s_4_5 453 # ASSIGN : s_5_0 462 # ASSIGN : s_5_1 1113 # ASSIGN : s_5_2 1424 # ASSIGN : s_5_3 1439 # ASSIGN : s_5_4 1442 # ASSIGN : s_5_5 1461 SHOW_RESULT 1462 END : 1462 (0 seconds) [Sun Jun 18 16:18:43 2006] SHOW_RESULT 1462 CPU : 0.179999999999995 = 0.169999999999995 + 0.01 + 0 + 0 # BOUND : makespan 1000 1462 MODIFY_CNF 1231 BEGIN : [Sun Jun 18 16:18:43 2006] MODIFY_CNF 1231 END : 25161809 bytes (0 seconds) [Sun Jun 18 16:18:43 2006] MODIFY_CNF 1231 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1231 BEGIN : [Sun Jun 18 16:18:43 2006] CMD : minisat /tmp/csp2sat9709.cnf /tmp/csp2sat9709.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 554749 1560234 | 184916 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (1 /sec) decisions : 3 (2 /sec) propagations : 72015 (46763 /sec) conflict literals : 1 (0.00 % deleted) Memory used : 48.26 MB CPU time : 1.54 s UNSATISFIABLE VERIFY_CNF 1231 END : (1 seconds) [Sun Jun 18 16:18:44 2006] VERIFY_CNF 1231 CPU : 1.64 = 0 + 0 + 1.54 + 0.1 # RESULT : makespan 1231 UNSATISFIABLE # BOUND : makespan 1232 1462 MODIFY_CNF 1347 BEGIN : [Sun Jun 18 16:18:44 2006] MODIFY_CNF 1347 END : 25161809 bytes (0 seconds) [Sun Jun 18 16:18:44 2006] MODIFY_CNF 1347 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1347 BEGIN : [Sun Jun 18 16:18:44 2006] CMD : minisat /tmp/csp2sat9709.cnf /tmp/csp2sat9709.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 596509 1685514 | 198836 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 1 (1 /sec) decisions : 108 (64 /sec) propagations : 109018 (64892 /sec) conflict literals : 11 (15.38 % deleted) Memory used : 48.79 MB CPU time : 1.68 s SATISFIABLE VERIFY_CNF 1347 END : (2 seconds) [Sun Jun 18 16:18:46 2006] VERIFY_CNF 1347 CPU : 1.85 = 0 + 0 + 1.73 + 0.12 # RESULT : makespan 1347 SATISFIABLE SHOW_RESULT 1347 BEGIN : [Sun Jun 18 16:18:46 2006] # ASSIGN : makespan 1347 # ASSIGN : s_0_0 680 # ASSIGN : s_0_1 4 # ASSIGN : s_0_2 5 # ASSIGN : s_0_3 1014 # ASSIGN : s_0_4 59 # ASSIGN : s_0_5 25 # ASSIGN : s_1_0 14 # ASSIGN : s_1_1 1013 # ASSIGN : s_1_2 280 # ASSIGN : s_1_3 377 # ASSIGN : s_1_4 376 # ASSIGN : s_1_5 306 # ASSIGN : s_2_0 15 # ASSIGN : s_2_1 323 # ASSIGN : s_2_2 694 # ASSIGN : s_2_3 256 # ASSIGN : s_2_4 649 # ASSIGN : s_2_5 308 # ASSIGN : s_3_0 16 # ASSIGN : s_3_1 649 # ASSIGN : s_3_2 311 # ASSIGN : s_3_3 1308 # ASSIGN : s_3_4 650 # ASSIGN : s_3_5 313 # ASSIGN : s_4_0 17 # ASSIGN : s_4_1 661 # ASSIGN : s_4_2 339 # ASSIGN : s_4_3 1310 # ASSIGN : s_4_4 1323 # ASSIGN : s_4_5 688 # ASSIGN : s_5_0 29 # ASSIGN : s_5_1 702 # ASSIGN : s_5_2 1309 # ASSIGN : s_5_3 1324 # ASSIGN : s_5_4 1327 # ASSIGN : s_5_5 1346 SHOW_RESULT 1347 END : 1347 (0 seconds) [Sun Jun 18 16:18:46 2006] SHOW_RESULT 1347 CPU : 0.18 = 0.18 + 0 + 0 + 0 # BOUND : makespan 1232 1347 MODIFY_CNF 1289 BEGIN : [Sun Jun 18 16:18:46 2006] MODIFY_CNF 1289 END : 25161809 bytes (0 seconds) [Sun Jun 18 16:18:46 2006] MODIFY_CNF 1289 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1289 BEGIN : [Sun Jun 18 16:18:46 2006] CMD : minisat /tmp/csp2sat9709.cnf /tmp/csp2sat9709.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 575629 1622874 | 191876 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 56 (33 /sec) propagations : 104957 (61739 /sec) conflict literals : 0 ( nan % deleted) Memory used : 48.79 MB CPU time : 1.7 s SATISFIABLE VERIFY_CNF 1289 END : (2 seconds) [Sun Jun 18 16:18:48 2006] VERIFY_CNF 1289 CPU : 1.9 = 0 + 0 + 1.74 + 0.16 # RESULT : makespan 1289 SATISFIABLE SHOW_RESULT 1289 BEGIN : [Sun Jun 18 16:18:48 2006] # ASSIGN : makespan 1289 # ASSIGN : s_0_0 895 # ASSIGN : s_0_1 3 # ASSIGN : s_0_2 1229 # ASSIGN : s_0_3 355 # ASSIGN : s_0_4 38 # ASSIGN : s_0_5 4 # ASSIGN : s_1_0 1288 # ASSIGN : s_1_1 255 # ASSIGN : s_1_2 0 # ASSIGN : s_1_3 649 # ASSIGN : s_1_4 36 # ASSIGN : s_1_5 246 # ASSIGN : s_2_0 0 # ASSIGN : s_2_1 963 # ASSIGN : s_2_2 348 # ASSIGN : s_2_3 196 # ASSIGN : s_2_4 37 # ASSIGN : s_2_5 248 # ASSIGN : s_3_0 1248 # ASSIGN : s_3_1 589 # ASSIGN : s_3_2 1249 # ASSIGN : s_3_3 11 # ASSIGN : s_3_4 590 # ASSIGN : s_3_5 253 # ASSIGN : s_4_0 1250 # ASSIGN : s_4_1 601 # ASSIGN : s_4_2 26 # ASSIGN : s_4_3 13 # ASSIGN : s_4_4 1262 # ASSIGN : s_4_5 628 # ASSIGN : s_5_0 1 # ASSIGN : s_5_1 652 # ASSIGN : s_5_2 1251 # ASSIGN : s_5_3 1285 # ASSIGN : s_5_4 1266 # ASSIGN : s_5_5 1288 SHOW_RESULT 1289 END : 1289 (0 seconds) [Sun Jun 18 16:18:48 2006] SHOW_RESULT 1289 CPU : 0.170000000000004 = 0.160000000000004 + 0.00999999999999998 + 0 + 0 # BOUND : makespan 1232 1289 MODIFY_CNF 1260 BEGIN : [Sun Jun 18 16:18:48 2006] MODIFY_CNF 1260 END : 25161809 bytes (0 seconds) [Sun Jun 18 16:18:48 2006] MODIFY_CNF 1260 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1260 BEGIN : [Sun Jun 18 16:18:48 2006] CMD : minisat /tmp/csp2sat9709.cnf /tmp/csp2sat9709.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 565189 1591554 | 188396 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (1 /sec) decisions : 3 (2 /sec) propagations : 72722 (43808 /sec) conflict literals : 1 (0.00 % deleted) Memory used : 48.25 MB CPU time : 1.66 s UNSATISFIABLE VERIFY_CNF 1260 END : (2 seconds) [Sun Jun 18 16:18:50 2006] VERIFY_CNF 1260 CPU : 1.79 = 0 + 0 + 1.66 + 0.13 # RESULT : makespan 1260 UNSATISFIABLE # BOUND : makespan 1261 1289 MODIFY_CNF 1275 BEGIN : [Sun Jun 18 16:18:50 2006] MODIFY_CNF 1275 END : 25161809 bytes (0 seconds) [Sun Jun 18 16:18:50 2006] MODIFY_CNF 1275 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1275 BEGIN : [Sun Jun 18 16:18:50 2006] CMD : minisat /tmp/csp2sat9709.cnf /tmp/csp2sat9709.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 570589 1607754 | 190196 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 63 (36 /sec) propagations : 104957 (59975 /sec) conflict literals : 0 ( nan % deleted) Memory used : 48.79 MB CPU time : 1.75 s SATISFIABLE VERIFY_CNF 1275 END : (2 seconds) [Sun Jun 18 16:18:52 2006] VERIFY_CNF 1275 CPU : 1.94 = 0 + 0 + 1.81 + 0.13 # RESULT : makespan 1275 SATISFIABLE SHOW_RESULT 1275 BEGIN : [Sun Jun 18 16:18:52 2006] # ASSIGN : makespan 1275 # ASSIGN : s_0_0 906 # ASSIGN : s_0_1 905 # ASSIGN : s_0_2 640 # ASSIGN : s_0_3 326 # ASSIGN : s_0_4 9 # ASSIGN : s_0_5 1240 # ASSIGN : s_1_0 1274 # ASSIGN : s_1_1 0 # ASSIGN : s_1_2 535 # ASSIGN : s_1_3 620 # ASSIGN : s_1_4 561 # ASSIGN : s_1_5 597 # ASSIGN : s_2_0 168 # ASSIGN : s_2_1 334 # ASSIGN : s_2_2 660 # ASSIGN : s_2_3 169 # ASSIGN : s_2_4 333 # ASSIGN : s_2_5 221 # ASSIGN : s_3_0 195 # ASSIGN : s_3_1 1220 # ASSIGN : s_3_2 196 # ASSIGN : s_3_3 1256 # ASSIGN : s_3_4 562 # ASSIGN : s_3_5 226 # ASSIGN : s_4_0 201 # ASSIGN : s_4_1 1221 # ASSIGN : s_4_2 213 # ASSIGN : s_4_3 1258 # ASSIGN : s_4_4 1248 # ASSIGN : s_4_5 599 # ASSIGN : s_5_0 255 # ASSIGN : s_5_1 909 # ASSIGN : s_5_2 198 # ASSIGN : s_5_3 1271 # ASSIGN : s_5_4 1252 # ASSIGN : s_5_5 1274 SHOW_RESULT 1275 END : 1275 (0 seconds) [Sun Jun 18 16:18:52 2006] SHOW_RESULT 1275 CPU : 0.18 = 0.18 + 0 + 0 + 0 # BOUND : makespan 1261 1275 MODIFY_CNF 1268 BEGIN : [Sun Jun 18 16:18:52 2006] MODIFY_CNF 1268 END : 25161809 bytes (0 seconds) [Sun Jun 18 16:18:52 2006] MODIFY_CNF 1268 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1268 BEGIN : [Sun Jun 18 16:18:52 2006] CMD : minisat /tmp/csp2sat9709.cnf /tmp/csp2sat9709.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 568069 1600194 | 189356 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (1 /sec) decisions : 3 (2 /sec) propagations : 72568 (46518 /sec) conflict literals : 1 (0.00 % deleted) Memory used : 48.25 MB CPU time : 1.56 s UNSATISFIABLE VERIFY_CNF 1268 END : (2 seconds) [Sun Jun 18 16:18:54 2006] VERIFY_CNF 1268 CPU : 1.66 = 0 + 0 + 1.56 + 0.1 # RESULT : makespan 1268 UNSATISFIABLE # BOUND : makespan 1269 1275 MODIFY_CNF 1272 BEGIN : [Sun Jun 18 16:18:54 2006] MODIFY_CNF 1272 END : 25161809 bytes (0 seconds) [Sun Jun 18 16:18:54 2006] MODIFY_CNF 1272 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1272 BEGIN : [Sun Jun 18 16:18:54 2006] CMD : minisat /tmp/csp2sat9709.cnf /tmp/csp2sat9709.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 569509 1604514 | 189836 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (1 /sec) decisions : 3 (2 /sec) propagations : 72046 (46183 /sec) conflict literals : 1 (0.00 % deleted) Memory used : 48.25 MB CPU time : 1.56 s UNSATISFIABLE VERIFY_CNF 1272 END : (2 seconds) [Sun Jun 18 16:18:56 2006] VERIFY_CNF 1272 CPU : 1.64 = 0 + 0 + 1.56 + 0.0799999999999998 # RESULT : makespan 1272 UNSATISFIABLE # BOUND : makespan 1273 1275 MODIFY_CNF 1274 BEGIN : [Sun Jun 18 16:18:56 2006] MODIFY_CNF 1274 END : 25161809 bytes (0 seconds) [Sun Jun 18 16:18:56 2006] MODIFY_CNF 1274 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1274 BEGIN : [Sun Jun 18 16:18:56 2006] CMD : minisat /tmp/csp2sat9709.cnf /tmp/csp2sat9709.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 570229 1606674 | 190076 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (1 /sec) decisions : 3 (2 /sec) propagations : 71962 (48954 /sec) conflict literals : 1 (0.00 % deleted) Memory used : 48.25 MB CPU time : 1.47 s UNSATISFIABLE VERIFY_CNF 1274 END : (1 seconds) [Sun Jun 18 16:18:57 2006] VERIFY_CNF 1274 CPU : 1.69 = 0 + 0 + 1.47 + 0.22 # RESULT : makespan 1274 UNSATISFIABLE # BOUND : makespan 1275 1275 MAIN END : (63 seconds) [Sun Jun 18 16:18:57 2006] MAIN CPU : 62.78 = 45.06 + 0.23 + 16.07 + 1.42