# TIMEOUT 18000 MAIN BEGIN : [Sun Jun 18 16:11:18 2006] READ BEGIN : csp/gp05-05.csp [Sun Jun 18 16:11:18 2006] READ END : csp/gp05-05.csp (0 seconds) [Sun Jun 18 16:11:18 2006] READ CPU : 0.23 = 0.23 + 0 + 0 + 0 # BOUND : makespan 1000 2649 GENERATE_CNF 2649 BEGIN : [Sun Jun 18 16:11:18 2006] GENERATE_CNF 2649 END : 68151 variables 599527 clauses 12493859 bytes (23 seconds) [Sun Jun 18 16:11:41 2006] GENERATE_CNF 2649 CPU : 22.45 = 22.39 + 0.06 + 0 + 0 MODIFY_CNF 1824 BEGIN : [Sun Jun 18 16:11:41 2006] MODIFY_CNF 1824 END : 12493865 bytes (0 seconds) [Sun Jun 18 16:11:41 2006] MODIFY_CNF 1824 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1824 BEGIN : [Sun Jun 18 16:11:41 2006] CMD : minisat /tmp/csp2sat9179.cnf /tmp/csp2sat9179.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 434147 1234873 | 144715 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 1 (1 /sec) decisions : 95 (116 /sec) propagations : 73298 (89388 /sec) conflict literals : 9 (0.00 % deleted) Memory used : 28.11 MB CPU time : 0.82 s SATISFIABLE VERIFY_CNF 1824 END : (0 seconds) [Sun Jun 18 16:11:41 2006] VERIFY_CNF 1824 CPU : 0.89 = 0 + 0 + 0.84 + 0.05 # RESULT : makespan 1824 SATISFIABLE SHOW_RESULT 1824 BEGIN : [Sun Jun 18 16:11:41 2006] # ASSIGN : makespan 1824 # ASSIGN : s_0_0 86 # ASSIGN : s_0_1 93 # ASSIGN : s_0_2 417 # ASSIGN : s_0_3 94 # ASSIGN : s_0_4 408 # ASSIGN : s_1_0 102 # ASSIGN : s_1_1 487 # ASSIGN : s_1_2 1086 # ASSIGN : s_1_3 1087 # ASSIGN : s_1_4 488 # ASSIGN : s_2_0 533 # ASSIGN : s_2_1 785 # ASSIGN : s_2_2 1103 # ASSIGN : s_2_3 1102 # ASSIGN : s_2_4 1431 # ASSIGN : s_3_0 534 # ASSIGN : s_3_1 1113 # ASSIGN : s_3_2 1783 # ASSIGN : s_3_3 1114 # ASSIGN : s_3_4 1784 # ASSIGN : s_4_0 824 # ASSIGN : s_4_1 1141 # ASSIGN : s_4_2 1821 # ASSIGN : s_4_3 1822 # ASSIGN : s_4_4 1823 SHOW_RESULT 1824 END : 1824 (1 seconds) [Sun Jun 18 16:11:42 2006] SHOW_RESULT 1824 CPU : 0.120000000000003 = 0.110000000000003 + 0.01 + 0 + 0 # BOUND : makespan 1000 1824 MODIFY_CNF 1412 BEGIN : [Sun Jun 18 16:11:42 2006] MODIFY_CNF 1412 END : 12493865 bytes (0 seconds) [Sun Jun 18 16:11:42 2006] MODIFY_CNF 1412 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1412 BEGIN : [Sun Jun 18 16:11:42 2006] CMD : minisat /tmp/csp2sat9179.cnf /tmp/csp2sat9179.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 351747 987673 | 117249 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 73 (96 /sec) propagations : 68151 (89672 /sec) conflict literals : 0 ( nan % deleted) Memory used : 28.11 MB CPU time : 0.76 s SATISFIABLE VERIFY_CNF 1412 END : (0 seconds) [Sun Jun 18 16:11:42 2006] VERIFY_CNF 1412 CPU : 0.9 = 0 + 0 + 0.8 + 0.1 # RESULT : makespan 1412 SATISFIABLE SHOW_RESULT 1412 BEGIN : [Sun Jun 18 16:11:42 2006] # ASSIGN : makespan 1412 # ASSIGN : s_0_0 27 # ASSIGN : s_0_1 34 # ASSIGN : s_0_2 373 # ASSIGN : s_0_3 59 # ASSIGN : s_0_4 35 # ASSIGN : s_1_0 657 # ASSIGN : s_1_1 43 # ASSIGN : s_1_2 1042 # ASSIGN : s_1_3 642 # ASSIGN : s_1_4 44 # ASSIGN : s_2_0 93 # ASSIGN : s_2_1 94 # ASSIGN : s_2_2 1043 # ASSIGN : s_2_3 689 # ASSIGN : s_2_4 690 # ASSIGN : s_3_0 121 # ASSIGN : s_3_1 411 # ASSIGN : s_3_2 1371 # ASSIGN : s_3_3 702 # ASSIGN : s_3_4 1372 # ASSIGN : s_4_0 1092 # ASSIGN : s_4_1 412 # ASSIGN : s_4_2 1409 # ASSIGN : s_4_3 1410 # ASSIGN : s_4_4 1411 SHOW_RESULT 1412 END : 1412 (1 seconds) [Sun Jun 18 16:11:43 2006] SHOW_RESULT 1412 CPU : 0.0999999999999979 = 0.0999999999999979 + 0 + 0 + 0 # BOUND : makespan 1000 1412 MODIFY_CNF 1206 BEGIN : [Sun Jun 18 16:11:43 2006] MODIFY_CNF 1206 END : 12493865 bytes (0 seconds) [Sun Jun 18 16:11:43 2006] MODIFY_CNF 1206 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1206 BEGIN : [Sun Jun 18 16:11:43 2006] CMD : minisat /tmp/csp2sat9179.cnf /tmp/csp2sat9179.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 310547 864073 | 103515 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (3 /sec) decisions : 6 (8 /sec) propagations : 48546 (64728 /sec) conflict literals : 1 (0.00 % deleted) Memory used : 27.76 MB CPU time : 0.75 s UNSATISFIABLE VERIFY_CNF 1206 END : (0 seconds) [Sun Jun 18 16:11:43 2006] VERIFY_CNF 1206 CPU : 0.85 = 0 + 0 + 0.75 + 0.1 # RESULT : makespan 1206 UNSATISFIABLE # BOUND : makespan 1207 1412 MODIFY_CNF 1309 BEGIN : [Sun Jun 18 16:11:43 2006] MODIFY_CNF 1309 END : 12493865 bytes (0 seconds) [Sun Jun 18 16:11:43 2006] MODIFY_CNF 1309 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1309 BEGIN : [Sun Jun 18 16:11:43 2006] CMD : minisat /tmp/csp2sat9179.cnf /tmp/csp2sat9179.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 331147 925873 | 110382 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 57 (75 /sec) propagations : 68151 (89672 /sec) conflict literals : 0 ( nan % deleted) Memory used : 28.11 MB CPU time : 0.76 s SATISFIABLE VERIFY_CNF 1309 END : (1 seconds) [Sun Jun 18 16:11:44 2006] VERIFY_CNF 1309 CPU : 0.91 = 0 + 0 + 0.79 + 0.12 # RESULT : makespan 1309 SATISFIABLE SHOW_RESULT 1309 BEGIN : [Sun Jun 18 16:11:44 2006] # ASSIGN : makespan 1309 # ASSIGN : s_0_0 10 # ASSIGN : s_0_1 4 # ASSIGN : s_0_2 254 # ASSIGN : s_0_3 993 # ASSIGN : s_0_4 17 # ASSIGN : s_1_0 924 # ASSIGN : s_1_1 5 # ASSIGN : s_1_2 923 # ASSIGN : s_1_3 11 # ASSIGN : s_1_4 26 # ASSIGN : s_2_0 5 # ASSIGN : s_2_1 6 # ASSIGN : s_2_2 977 # ASSIGN : s_2_3 323 # ASSIGN : s_2_4 624 # ASSIGN : s_3_0 19 # ASSIGN : s_3_1 323 # ASSIGN : s_3_2 1305 # ASSIGN : s_3_3 324 # ASSIGN : s_3_4 1266 # ASSIGN : s_4_0 309 # ASSIGN : s_4_1 626 # ASSIGN : s_4_2 1306 # ASSIGN : s_4_3 1307 # ASSIGN : s_4_4 1308 SHOW_RESULT 1309 END : 1309 (0 seconds) [Sun Jun 18 16:11:44 2006] SHOW_RESULT 1309 CPU : 0.0999999999999999 = 0.0899999999999999 + 0.01 + 0 + 0 # BOUND : makespan 1207 1309 MODIFY_CNF 1258 BEGIN : [Sun Jun 18 16:11:44 2006] MODIFY_CNF 1258 END : 12493865 bytes (0 seconds) [Sun Jun 18 16:11:44 2006] MODIFY_CNF 1258 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1258 BEGIN : [Sun Jun 18 16:11:44 2006] CMD : minisat /tmp/csp2sat9179.cnf /tmp/csp2sat9179.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 320947 895273 | 106982 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (3 /sec) decisions : 6 (8 /sec) propagations : 47194 (59739 /sec) conflict literals : 1 (0.00 % deleted) Memory used : 27.76 MB CPU time : 0.79 s UNSATISFIABLE VERIFY_CNF 1258 END : (1 seconds) [Sun Jun 18 16:11:45 2006] VERIFY_CNF 1258 CPU : 0.84 = 0 + 0 + 0.79 + 0.05 # RESULT : makespan 1258 UNSATISFIABLE # BOUND : makespan 1259 1309 MODIFY_CNF 1284 BEGIN : [Sun Jun 18 16:11:45 2006] MODIFY_CNF 1284 END : 12493865 bytes (0 seconds) [Sun Jun 18 16:11:45 2006] MODIFY_CNF 1284 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1284 BEGIN : [Sun Jun 18 16:11:45 2006] CMD : minisat /tmp/csp2sat9179.cnf /tmp/csp2sat9179.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 326147 910873 | 108715 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 41 (53 /sec) propagations : 68151 (88508 /sec) conflict literals : 0 ( nan % deleted) Memory used : 28.11 MB CPU time : 0.77 s SATISFIABLE VERIFY_CNF 1284 END : (1 seconds) [Sun Jun 18 16:11:46 2006] VERIFY_CNF 1284 CPU : 0.9 = 0 + 0 + 0.81 + 0.09 # RESULT : makespan 1284 SATISFIABLE SHOW_RESULT 1284 BEGIN : [Sun Jun 18 16:11:46 2006] # ASSIGN : makespan 1284 # ASSIGN : s_0_0 274 # ASSIGN : s_0_1 0 # ASSIGN : s_0_2 283 # ASSIGN : s_0_3 952 # ASSIGN : s_0_4 1273 # ASSIGN : s_1_0 607 # ASSIGN : s_1_1 1 # ASSIGN : s_1_2 0 # ASSIGN : s_1_3 1266 # ASSIGN : s_1_4 2 # ASSIGN : s_2_0 281 # ASSIGN : s_2_1 283 # ASSIGN : s_2_2 954 # ASSIGN : s_2_3 282 # ASSIGN : s_2_4 600 # ASSIGN : s_3_0 992 # ASSIGN : s_3_1 282 # ASSIGN : s_3_2 1282 # ASSIGN : s_3_3 283 # ASSIGN : s_3_4 953 # ASSIGN : s_4_0 284 # ASSIGN : s_4_1 601 # ASSIGN : s_4_2 1283 # ASSIGN : s_4_3 1281 # ASSIGN : s_4_4 1282 SHOW_RESULT 1284 END : 1284 (0 seconds) [Sun Jun 18 16:11:46 2006] SHOW_RESULT 1284 CPU : 0.100000000000001 = 0.100000000000001 + 0 + 0 + 0 # BOUND : makespan 1259 1284 MODIFY_CNF 1271 BEGIN : [Sun Jun 18 16:11:46 2006] MODIFY_CNF 1271 END : 12493865 bytes (0 seconds) [Sun Jun 18 16:11:46 2006] MODIFY_CNF 1271 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1271 BEGIN : [Sun Jun 18 16:11:46 2006] CMD : minisat /tmp/csp2sat9179.cnf /tmp/csp2sat9179.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 323547 903073 | 107849 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (3 /sec) decisions : 6 (8 /sec) propagations : 48136 (64181 /sec) conflict literals : 1 (0.00 % deleted) Memory used : 27.76 MB CPU time : 0.75 s UNSATISFIABLE VERIFY_CNF 1271 END : (1 seconds) [Sun Jun 18 16:11:47 2006] VERIFY_CNF 1271 CPU : 0.85 = 0 + 0 + 0.75 + 0.1 # RESULT : makespan 1271 UNSATISFIABLE # BOUND : makespan 1272 1284 MODIFY_CNF 1278 BEGIN : [Sun Jun 18 16:11:47 2006] MODIFY_CNF 1278 END : 12493865 bytes (0 seconds) [Sun Jun 18 16:11:47 2006] MODIFY_CNF 1278 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1278 BEGIN : [Sun Jun 18 16:11:47 2006] CMD : minisat /tmp/csp2sat9179.cnf /tmp/csp2sat9179.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 324947 907273 | 108315 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (3 /sec) decisions : 6 (8 /sec) propagations : 47330 (60679 /sec) conflict literals : 1 (0.00 % deleted) Memory used : 27.76 MB CPU time : 0.78 s UNSATISFIABLE VERIFY_CNF 1278 END : (1 seconds) [Sun Jun 18 16:11:48 2006] VERIFY_CNF 1278 CPU : 0.849999999999999 = 0 + 0 + 0.779999999999999 + 0.0700000000000001 # RESULT : makespan 1278 UNSATISFIABLE # BOUND : makespan 1279 1284 MODIFY_CNF 1281 BEGIN : [Sun Jun 18 16:11:48 2006] MODIFY_CNF 1281 END : 12493865 bytes (0 seconds) [Sun Jun 18 16:11:48 2006] MODIFY_CNF 1281 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1281 BEGIN : [Sun Jun 18 16:11:48 2006] CMD : minisat /tmp/csp2sat9179.cnf /tmp/csp2sat9179.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 325547 909073 | 108515 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 39 (51 /sec) propagations : 68151 (89672 /sec) conflict literals : 0 ( nan % deleted) Memory used : 28.11 MB CPU time : 0.76 s SATISFIABLE VERIFY_CNF 1281 END : (1 seconds) [Sun Jun 18 16:11:49 2006] VERIFY_CNF 1281 CPU : 0.9 = 0 + 0 + 0.79 + 0.11 # RESULT : makespan 1281 SATISFIABLE SHOW_RESULT 1281 BEGIN : [Sun Jun 18 16:11:49 2006] # ASSIGN : makespan 1281 # ASSIGN : s_0_0 256 # ASSIGN : s_0_1 263 # ASSIGN : s_0_2 280 # ASSIGN : s_0_3 949 # ASSIGN : s_0_4 1270 # ASSIGN : s_1_0 606 # ASSIGN : s_1_1 1262 # ASSIGN : s_1_2 0 # ASSIGN : s_1_3 1263 # ASSIGN : s_1_4 1 # ASSIGN : s_2_0 263 # ASSIGN : s_2_1 265 # ASSIGN : s_2_2 952 # ASSIGN : s_2_3 264 # ASSIGN : s_2_4 599 # ASSIGN : s_3_0 991 # ASSIGN : s_3_1 264 # ASSIGN : s_3_2 951 # ASSIGN : s_3_3 280 # ASSIGN : s_3_4 952 # ASSIGN : s_4_0 265 # ASSIGN : s_4_1 582 # ASSIGN : s_4_2 1280 # ASSIGN : s_4_3 1278 # ASSIGN : s_4_4 1279 SHOW_RESULT 1281 END : 1281 (0 seconds) [Sun Jun 18 16:11:49 2006] SHOW_RESULT 1281 CPU : 0.0999999999999979 = 0.0999999999999979 + 0 + 0 + 0 # BOUND : makespan 1279 1281 MODIFY_CNF 1280 BEGIN : [Sun Jun 18 16:11:49 2006] MODIFY_CNF 1280 END : 12493865 bytes (0 seconds) [Sun Jun 18 16:11:49 2006] MODIFY_CNF 1280 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1280 BEGIN : [Sun Jun 18 16:11:49 2006] CMD : minisat /tmp/csp2sat9179.cnf /tmp/csp2sat9179.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 325347 908473 | 108449 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 1 (1 /sec) decisions : 39 (52 /sec) propagations : 71356 (95141 /sec) conflict literals : 3 (0.00 % deleted) Memory used : 28.10 MB CPU time : 0.75 s SATISFIABLE VERIFY_CNF 1280 END : (1 seconds) [Sun Jun 18 16:11:50 2006] VERIFY_CNF 1280 CPU : 0.91 = 0 + 0 + 0.79 + 0.12 # RESULT : makespan 1280 SATISFIABLE SHOW_RESULT 1280 BEGIN : [Sun Jun 18 16:11:50 2006] # ASSIGN : makespan 1280 # ASSIGN : s_0_0 254 # ASSIGN : s_0_1 261 # ASSIGN : s_0_2 280 # ASSIGN : s_0_3 949 # ASSIGN : s_0_4 1270 # ASSIGN : s_1_0 605 # ASSIGN : s_1_1 1262 # ASSIGN : s_1_2 1279 # ASSIGN : s_1_3 1263 # ASSIGN : s_1_4 0 # ASSIGN : s_2_0 263 # ASSIGN : s_2_1 265 # ASSIGN : s_2_2 951 # ASSIGN : s_2_3 264 # ASSIGN : s_2_4 598 # ASSIGN : s_3_0 990 # ASSIGN : s_3_1 262 # ASSIGN : s_3_2 263 # ASSIGN : s_3_3 280 # ASSIGN : s_3_4 951 # ASSIGN : s_4_0 265 # ASSIGN : s_4_1 582 # ASSIGN : s_4_2 264 # ASSIGN : s_4_3 1278 # ASSIGN : s_4_4 1279 SHOW_RESULT 1280 END : 1280 (0 seconds) [Sun Jun 18 16:11:50 2006] SHOW_RESULT 1280 CPU : 0.0999999999999999 = 0.0899999999999999 + 0.01 + 0 + 0 # BOUND : makespan 1279 1280 MODIFY_CNF 1279 BEGIN : [Sun Jun 18 16:11:50 2006] MODIFY_CNF 1279 END : 12493865 bytes (0 seconds) [Sun Jun 18 16:11:50 2006] MODIFY_CNF 1279 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1279 BEGIN : [Sun Jun 18 16:11:50 2006] CMD : minisat /tmp/csp2sat9179.cnf /tmp/csp2sat9179.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 325147 907873 | 108382 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 7 (9 /sec) decisions : 8 (10 /sec) propagations : 65249 (82594 /sec) conflict literals : 11 (8.33 % deleted) Memory used : 27.77 MB CPU time : 0.79 s UNSATISFIABLE VERIFY_CNF 1279 END : (1 seconds) [Sun Jun 18 16:11:51 2006] VERIFY_CNF 1279 CPU : 0.87 = 0 + 0.01 + 0.79 + 0.07 # RESULT : makespan 1279 UNSATISFIABLE # BOUND : makespan 1280 1280 MAIN END : (33 seconds) [Sun Jun 18 16:11:51 2006] MAIN CPU : 32.97 = 23.21 + 0.1 + 8.68 + 0.98