# TIMEOUT 18000 MAIN BEGIN : [Sun Jun 18 16:14:03 2006] READ BEGIN : csp/gp05-10.csp [Sun Jun 18 16:14:03 2006] READ END : csp/gp05-10.csp (0 seconds) [Sun Jun 18 16:14:03 2006] READ CPU : 0.23 = 0.23 + 0 + 0 + 0 # BOUND : makespan 1000 2682 GENERATE_CNF 2682 BEGIN : [Sun Jun 18 16:14:03 2006] GENERATE_CNF 2682 END : 69009 variables 607810 clauses 12668042 bytes (24 seconds) [Sun Jun 18 16:14:27 2006] GENERATE_CNF 2682 CPU : 22.53 = 22.43 + 0.1 + 0 + 0 MODIFY_CNF 1841 BEGIN : [Sun Jun 18 16:14:27 2006] MODIFY_CNF 1841 END : 12668048 bytes (0 seconds) [Sun Jun 18 16:14:27 2006] MODIFY_CNF 1841 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1841 BEGIN : [Sun Jun 18 16:14:27 2006] CMD : minisat /tmp/csp2sat9282.cnf /tmp/csp2sat9282.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 439230 1249264 | 146410 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 1 (1 /sec) decisions : 105 (140 /sec) propagations : 75679 (100905 /sec) conflict literals : 5 (0.00 % deleted) Memory used : 28.46 MB CPU time : 0.75 s SATISFIABLE VERIFY_CNF 1841 END : (1 seconds) [Sun Jun 18 16:14:28 2006] VERIFY_CNF 1841 CPU : 0.9 = 0 + 0 + 0.79 + 0.11 # RESULT : makespan 1841 SATISFIABLE SHOW_RESULT 1841 BEGIN : [Sun Jun 18 16:14:28 2006] # ASSIGN : makespan 1841 # ASSIGN : s_0_0 401 # ASSIGN : s_0_1 402 # ASSIGN : s_0_2 786 # ASSIGN : s_0_3 787 # ASSIGN : s_0_4 841 # ASSIGN : s_1_0 488 # ASSIGN : s_1_1 764 # ASSIGN : s_1_2 839 # ASSIGN : s_1_3 814 # ASSIGN : s_1_4 1450 # ASSIGN : s_2_0 787 # ASSIGN : s_2_1 788 # ASSIGN : s_2_2 1126 # ASSIGN : s_2_3 868 # ASSIGN : s_2_4 1838 # ASSIGN : s_3_0 810 # ASSIGN : s_3_1 855 # ASSIGN : s_3_2 1814 # ASSIGN : s_3_3 1111 # ASSIGN : s_3_4 1839 # ASSIGN : s_4_0 841 # ASSIGN : s_4_1 1532 # ASSIGN : s_4_2 1823 # ASSIGN : s_4_3 1838 # ASSIGN : s_4_4 1840 SHOW_RESULT 1841 END : 1841 (0 seconds) [Sun Jun 18 16:14:28 2006] SHOW_RESULT 1841 CPU : 0.110000000000001 = 0.100000000000001 + 0.01 + 0 + 0 # BOUND : makespan 1000 1841 MODIFY_CNF 1420 BEGIN : [Sun Jun 18 16:14:28 2006] MODIFY_CNF 1420 END : 12668048 bytes (0 seconds) [Sun Jun 18 16:14:28 2006] MODIFY_CNF 1420 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1420 BEGIN : [Sun Jun 18 16:14:28 2006] CMD : minisat /tmp/csp2sat9282.cnf /tmp/csp2sat9282.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 355030 996664 | 118343 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 81 (100 /sec) propagations : 69009 (85196 /sec) conflict literals : 0 ( nan % deleted) Memory used : 28.46 MB CPU time : 0.81 s SATISFIABLE VERIFY_CNF 1420 END : (1 seconds) [Sun Jun 18 16:14:29 2006] VERIFY_CNF 1420 CPU : 0.91 = 0 + 0 + 0.84 + 0.07 # RESULT : makespan 1420 SATISFIABLE SHOW_RESULT 1420 BEGIN : [Sun Jun 18 16:14:29 2006] # ASSIGN : makespan 1420 # ASSIGN : s_0_0 66 # ASSIGN : s_0_1 749 # ASSIGN : s_0_2 112 # ASSIGN : s_0_3 113 # ASSIGN : s_0_4 140 # ASSIGN : s_1_0 67 # ASSIGN : s_1_1 343 # ASSIGN : s_1_2 418 # ASSIGN : s_1_3 393 # ASSIGN : s_1_4 1029 # ASSIGN : s_2_0 366 # ASSIGN : s_2_1 367 # ASSIGN : s_2_2 705 # ASSIGN : s_2_3 447 # ASSIGN : s_2_4 1417 # ASSIGN : s_3_0 389 # ASSIGN : s_3_1 434 # ASSIGN : s_3_2 1393 # ASSIGN : s_3_3 690 # ASSIGN : s_3_4 1418 # ASSIGN : s_4_0 420 # ASSIGN : s_4_1 1111 # ASSIGN : s_4_2 1402 # ASSIGN : s_4_3 1417 # ASSIGN : s_4_4 1419 SHOW_RESULT 1420 END : 1420 (0 seconds) [Sun Jun 18 16:14:29 2006] SHOW_RESULT 1420 CPU : 0.109999999999999 = 0.109999999999999 + 0 + 0 + 0 # BOUND : makespan 1000 1420 MODIFY_CNF 1210 BEGIN : [Sun Jun 18 16:14:29 2006] MODIFY_CNF 1210 END : 12668048 bytes (0 seconds) [Sun Jun 18 16:14:29 2006] MODIFY_CNF 1210 CPU : 0.00999999999999801 = 0.00999999999999801 + 0 + 0 + 0 VERIFY_CNF 1210 BEGIN : [Sun Jun 18 16:14:29 2006] CMD : minisat /tmp/csp2sat9282.cnf /tmp/csp2sat9282.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 313030 870664 | 104343 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (3 /sec) decisions : 10 (13 /sec) propagations : 49885 (66513 /sec) conflict literals : 1 (0.00 % deleted) Memory used : 28.12 MB CPU time : 0.75 s UNSATISFIABLE VERIFY_CNF 1210 END : (1 seconds) [Sun Jun 18 16:14:30 2006] VERIFY_CNF 1210 CPU : 0.87 = 0 + 0 + 0.75 + 0.12 # RESULT : makespan 1210 UNSATISFIABLE # BOUND : makespan 1211 1420 MODIFY_CNF 1315 BEGIN : [Sun Jun 18 16:14:30 2006] MODIFY_CNF 1315 END : 12668048 bytes (0 seconds) [Sun Jun 18 16:14:30 2006] MODIFY_CNF 1315 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1315 BEGIN : [Sun Jun 18 16:14:30 2006] CMD : minisat /tmp/csp2sat9282.cnf /tmp/csp2sat9282.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 334030 933664 | 111343 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 1 (1 /sec) decisions : 69 (82 /sec) propagations : 72995 (86899 /sec) conflict literals : 7 (0.00 % deleted) Memory used : 28.46 MB CPU time : 0.84 s SATISFIABLE VERIFY_CNF 1315 END : (0 seconds) [Sun Jun 18 16:14:30 2006] VERIFY_CNF 1315 CPU : 0.91 = 0 + 0 + 0.88 + 0.03 # RESULT : makespan 1315 SATISFIABLE SHOW_RESULT 1315 BEGIN : [Sun Jun 18 16:14:30 2006] # ASSIGN : makespan 1315 # ASSIGN : s_0_0 6 # ASSIGN : s_0_1 644 # ASSIGN : s_0_2 7 # ASSIGN : s_0_3 8 # ASSIGN : s_0_4 35 # ASSIGN : s_1_0 1039 # ASSIGN : s_1_1 6 # ASSIGN : s_1_2 30 # ASSIGN : s_1_3 317 # ASSIGN : s_1_4 651 # ASSIGN : s_2_0 5 # ASSIGN : s_2_1 262 # ASSIGN : s_2_2 600 # ASSIGN : s_2_3 342 # ASSIGN : s_2_4 1312 # ASSIGN : s_3_0 284 # ASSIGN : s_3_1 329 # ASSIGN : s_3_2 1288 # ASSIGN : s_3_3 585 # ASSIGN : s_3_4 1313 # ASSIGN : s_4_0 315 # ASSIGN : s_4_1 1006 # ASSIGN : s_4_2 1297 # ASSIGN : s_4_3 1312 # ASSIGN : s_4_4 1314 SHOW_RESULT 1315 END : 1315 (1 seconds) [Sun Jun 18 16:14:31 2006] SHOW_RESULT 1315 CPU : 0.110000000000001 = 0.100000000000001 + 0.01 + 0 + 0 # BOUND : makespan 1211 1315 MODIFY_CNF 1263 BEGIN : [Sun Jun 18 16:14:31 2006] MODIFY_CNF 1263 END : 12668048 bytes (0 seconds) [Sun Jun 18 16:14:31 2006] MODIFY_CNF 1263 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1263 BEGIN : [Sun Jun 18 16:14:31 2006] CMD : minisat /tmp/csp2sat9282.cnf /tmp/csp2sat9282.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 323630 902464 | 107876 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (2 /sec) decisions : 58 (72 /sec) propagations : 78648 (97096 /sec) conflict literals : 6 (0.00 % deleted) Memory used : 28.46 MB CPU time : 0.81 s SATISFIABLE VERIFY_CNF 1263 END : (1 seconds) [Sun Jun 18 16:14:32 2006] VERIFY_CNF 1263 CPU : 0.93 = 0 + 0 + 0.850000000000001 + 0.08 # RESULT : makespan 1263 SATISFIABLE SHOW_RESULT 1263 BEGIN : [Sun Jun 18 16:14:32 2006] # ASSIGN : makespan 1263 # ASSIGN : s_0_0 4 # ASSIGN : s_0_1 634 # ASSIGN : s_0_2 5 # ASSIGN : s_0_3 1208 # ASSIGN : s_0_4 25 # ASSIGN : s_1_0 293 # ASSIGN : s_1_1 610 # ASSIGN : s_1_2 6 # ASSIGN : s_1_3 1235 # ASSIGN : s_1_4 847 # ASSIGN : s_2_0 49 # ASSIGN : s_2_1 497 # ASSIGN : s_2_2 564 # ASSIGN : s_2_3 50 # ASSIGN : s_2_4 1260 # ASSIGN : s_3_0 262 # ASSIGN : s_3_1 996 # ASSIGN : s_3_2 1252 # ASSIGN : s_3_3 293 # ASSIGN : s_3_4 1261 # ASSIGN : s_4_0 569 # ASSIGN : s_4_1 206 # ASSIGN : s_4_2 549 # ASSIGN : s_4_3 1260 # ASSIGN : s_4_4 1262 SHOW_RESULT 1263 END : 1263 (0 seconds) [Sun Jun 18 16:14:32 2006] SHOW_RESULT 1263 CPU : 0.110000000000001 = 0.100000000000001 + 0.00999999999999998 + 0 + 0 # BOUND : makespan 1211 1263 MODIFY_CNF 1237 BEGIN : [Sun Jun 18 16:14:32 2006] MODIFY_CNF 1237 END : 12668048 bytes (0 seconds) [Sun Jun 18 16:14:32 2006] MODIFY_CNF 1237 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1237 BEGIN : [Sun Jun 18 16:14:32 2006] CMD : minisat /tmp/csp2sat9282.cnf /tmp/csp2sat9282.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 318430 886864 | 106143 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (2 /sec) decisions : 10 (12 /sec) propagations : 48815 (60265 /sec) conflict literals : 1 (0.00 % deleted) Memory used : 28.12 MB CPU time : 0.81 s UNSATISFIABLE VERIFY_CNF 1237 END : (0 seconds) [Sun Jun 18 16:14:32 2006] VERIFY_CNF 1237 CPU : 0.87 = 0 + 0 + 0.81 + 0.06 # RESULT : makespan 1237 UNSATISFIABLE # BOUND : makespan 1238 1263 MODIFY_CNF 1250 BEGIN : [Sun Jun 18 16:14:32 2006] MODIFY_CNF 1250 END : 12668048 bytes (0 seconds) [Sun Jun 18 16:14:32 2006] MODIFY_CNF 1250 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1250 BEGIN : [Sun Jun 18 16:14:32 2006] CMD : minisat /tmp/csp2sat9282.cnf /tmp/csp2sat9282.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 321030 894664 | 107010 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (3 /sec) decisions : 10 (13 /sec) propagations : 48472 (62144 /sec) conflict literals : 1 (0.00 % deleted) Memory used : 28.12 MB CPU time : 0.78 s UNSATISFIABLE VERIFY_CNF 1250 END : (1 seconds) [Sun Jun 18 16:14:33 2006] VERIFY_CNF 1250 CPU : 0.86 = 0 + 0 + 0.78 + 0.0800000000000001 # RESULT : makespan 1250 UNSATISFIABLE # BOUND : makespan 1251 1263 MODIFY_CNF 1257 BEGIN : [Sun Jun 18 16:14:33 2006] MODIFY_CNF 1257 END : 12668048 bytes (0 seconds) [Sun Jun 18 16:14:33 2006] MODIFY_CNF 1257 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1257 BEGIN : [Sun Jun 18 16:14:33 2006] CMD : minisat /tmp/csp2sat9282.cnf /tmp/csp2sat9282.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 322430 898864 | 107476 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 3 (4 /sec) decisions : 40 (49 /sec) propagations : 77151 (94087 /sec) conflict literals : 12 (14.29 % deleted) Memory used : 28.47 MB CPU time : 0.82 s SATISFIABLE VERIFY_CNF 1257 END : (1 seconds) [Sun Jun 18 16:14:34 2006] VERIFY_CNF 1257 CPU : 0.94 = 0 + 0.01 + 0.84 + 0.09 # RESULT : makespan 1257 SATISFIABLE SHOW_RESULT 1257 BEGIN : [Sun Jun 18 16:14:34 2006] # ASSIGN : makespan 1257 # ASSIGN : s_0_0 0 # ASSIGN : s_0_1 637 # ASSIGN : s_0_2 1256 # ASSIGN : s_0_3 1 # ASSIGN : s_0_4 28 # ASSIGN : s_1_0 287 # ASSIGN : s_1_1 613 # ASSIGN : s_1_2 0 # ASSIGN : s_1_3 1229 # ASSIGN : s_1_4 841 # ASSIGN : s_2_0 52 # ASSIGN : s_2_1 499 # ASSIGN : s_2_2 566 # ASSIGN : s_2_3 53 # ASSIGN : s_2_4 1254 # ASSIGN : s_3_0 256 # ASSIGN : s_3_1 999 # ASSIGN : s_3_2 287 # ASSIGN : s_3_3 296 # ASSIGN : s_3_4 1255 # ASSIGN : s_4_0 563 # ASSIGN : s_4_1 208 # ASSIGN : s_4_2 548 # ASSIGN : s_4_3 1254 # ASSIGN : s_4_4 1256 SHOW_RESULT 1257 END : 1257 (0 seconds) [Sun Jun 18 16:14:34 2006] SHOW_RESULT 1257 CPU : 0.109999999999998 = 0.0999999999999979 + 0.01 + 0 + 0 # BOUND : makespan 1251 1257 MODIFY_CNF 1254 BEGIN : [Sun Jun 18 16:14:34 2006] MODIFY_CNF 1254 END : 12668048 bytes (0 seconds) [Sun Jun 18 16:14:34 2006] MODIFY_CNF 1254 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1254 BEGIN : [Sun Jun 18 16:14:34 2006] CMD : minisat /tmp/csp2sat9282.cnf /tmp/csp2sat9282.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 321830 897064 | 107276 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 3 (4 /sec) decisions : 38 (47 /sec) propagations : 93064 (114894 /sec) conflict literals : 12 (14.29 % deleted) Memory used : 28.47 MB CPU time : 0.81 s SATISFIABLE VERIFY_CNF 1254 END : (1 seconds) [Sun Jun 18 16:14:35 2006] VERIFY_CNF 1254 CPU : 0.94 = 0 + 0 + 0.84 + 0.1 # RESULT : makespan 1254 SATISFIABLE SHOW_RESULT 1254 BEGIN : [Sun Jun 18 16:14:35 2006] # ASSIGN : makespan 1254 # ASSIGN : s_0_0 1253 # ASSIGN : s_0_1 280 # ASSIGN : s_0_2 201 # ASSIGN : s_0_3 202 # ASSIGN : s_0_4 642 # ASSIGN : s_1_0 691 # ASSIGN : s_1_1 0 # ASSIGN : s_1_2 967 # ASSIGN : s_1_3 229 # ASSIGN : s_1_4 254 # ASSIGN : s_2_0 1007 # ASSIGN : s_2_1 893 # ASSIGN : s_2_2 205 # ASSIGN : s_2_3 1008 # ASSIGN : s_2_4 1251 # ASSIGN : s_3_0 1221 # ASSIGN : s_3_1 24 # ASSIGN : s_3_2 15 # ASSIGN : s_3_3 305 # ASSIGN : s_3_4 1252 # ASSIGN : s_4_0 0 # ASSIGN : s_4_1 960 # ASSIGN : s_4_2 945 # ASSIGN : s_4_3 1251 # ASSIGN : s_4_4 1253 SHOW_RESULT 1254 END : 1254 (0 seconds) [Sun Jun 18 16:14:35 2006] SHOW_RESULT 1254 CPU : 0.109999999999999 = 0.109999999999999 + 0 + 0 + 0 # BOUND : makespan 1251 1254 MODIFY_CNF 1252 BEGIN : [Sun Jun 18 16:14:35 2006] MODIFY_CNF 1252 END : 12668048 bytes (0 seconds) [Sun Jun 18 16:14:35 2006] MODIFY_CNF 1252 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1252 BEGIN : [Sun Jun 18 16:14:35 2006] CMD : minisat /tmp/csp2sat9282.cnf /tmp/csp2sat9282.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 321430 895864 | 107143 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 5 (6 /sec) decisions : 18 (22 /sec) propagations : 79584 (97054 /sec) conflict literals : 8 (0.00 % deleted) Memory used : 28.18 MB CPU time : 0.82 s UNSATISFIABLE VERIFY_CNF 1252 END : (1 seconds) [Sun Jun 18 16:14:36 2006] VERIFY_CNF 1252 CPU : 0.889999999999999 = 0 + 0 + 0.819999999999999 + 0.0700000000000001 # RESULT : makespan 1252 UNSATISFIABLE # BOUND : makespan 1253 1254 MODIFY_CNF 1253 BEGIN : [Sun Jun 18 16:14:36 2006] MODIFY_CNF 1253 END : 12668048 bytes (0 seconds) [Sun Jun 18 16:14:36 2006] MODIFY_CNF 1253 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1253 BEGIN : [Sun Jun 18 16:14:36 2006] CMD : minisat /tmp/csp2sat9282.cnf /tmp/csp2sat9282.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 321630 896464 | 107210 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 5 (6 /sec) decisions : 18 (22 /sec) propagations : 78264 (95444 /sec) conflict literals : 8 (0.00 % deleted) Memory used : 28.17 MB CPU time : 0.82 s UNSATISFIABLE VERIFY_CNF 1253 END : (1 seconds) [Sun Jun 18 16:14:37 2006] VERIFY_CNF 1253 CPU : 0.89 = 0 + 0 + 0.82 + 0.07 # RESULT : makespan 1253 UNSATISFIABLE # BOUND : makespan 1254 1254 MAIN END : (34 seconds) [Sun Jun 18 16:14:37 2006] MAIN CPU : 33.37 = 23.32 + 0.15 + 9.02 + 0.88