# TIMEOUT 18000 MAIN BEGIN : [Sun Jun 18 20:06:27 2006] READ BEGIN : csp/j6-per0-1.csp [Sun Jun 18 20:06:27 2006] READ END : csp/j6-per0-1.csp (1 seconds) [Sun Jun 18 20:06:28 2006] READ CPU : 0.4 = 0.4 + 0 + 0 + 0 # BOUND : makespan 1000 2510 GENERATE_CNF 2510 BEGIN : [Sun Jun 18 20:06:28 2006] GENERATE_CNF 2510 END : 92340 variables 990913 clauses 20874467 bytes (37 seconds) [Sun Jun 18 20:07:05 2006] GENERATE_CNF 2510 CPU : 37.03 = 36.83 + 0.2 + 0 + 0 MODIFY_CNF 1755 BEGIN : [Sun Jun 18 20:07:05 2006] MODIFY_CNF 1755 END : 20874473 bytes (0 seconds) [Sun Jun 18 20:07:05 2006] MODIFY_CNF 1755 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1755 BEGIN : [Sun Jun 18 20:07:05 2006] CMD : minisat /tmp/csp2sat14133.cnf /tmp/csp2sat14133.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 718496 2064092 | 239498 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 19 (15 /sec) decisions : 202 (155 /sec) propagations : 238416 (183397 /sec) conflict literals : 330 (13.84 % deleted) Memory used : 42.81 MB CPU time : 1.3 s SATISFIABLE VERIFY_CNF 1755 END : (1 seconds) [Sun Jun 18 20:07:06 2006] VERIFY_CNF 1755 CPU : 1.53 = 0 + 0 + 1.34 + 0.19 # RESULT : makespan 1755 SATISFIABLE SHOW_RESULT 1755 BEGIN : [Sun Jun 18 20:07:06 2006] # ASSIGN : makespan 1755 # ASSIGN : s_0_0 1503 # ASSIGN : s_0_1 1672 # ASSIGN : s_0_2 364 # ASSIGN : s_0_3 7 # ASSIGN : s_0_4 754 # ASSIGN : s_0_5 180 # ASSIGN : s_1_0 1539 # ASSIGN : s_1_1 1734 # ASSIGN : s_1_2 799 # ASSIGN : s_1_3 483 # ASSIGN : s_1_4 1110 # ASSIGN : s_1_5 198 # ASSIGN : s_2_0 1504 # ASSIGN : s_2_1 1497 # ASSIGN : s_2_2 1067 # ASSIGN : s_2_3 1166 # ASSIGN : s_2_4 1207 # ASSIGN : s_2_5 302 # ASSIGN : s_3_0 1733 # ASSIGN : s_3_1 748 # ASSIGN : s_3_2 1102 # ASSIGN : s_3_3 1193 # ASSIGN : s_3_4 1436 # ASSIGN : s_3_5 969 # ASSIGN : s_4_0 1198 # ASSIGN : s_4_1 302 # ASSIGN : s_4_2 1289 # ASSIGN : s_4_3 1458 # ASSIGN : s_4_4 1726 # ASSIGN : s_4_5 1121 # ASSIGN : s_5_0 541 # ASSIGN : s_5_1 59 # ASSIGN : s_5_2 1699 # ASSIGN : s_5_3 1655 # ASSIGN : s_5_4 1746 # ASSIGN : s_5_5 1754 SHOW_RESULT 1755 END : 1755 (1 seconds) [Sun Jun 18 20:07:07 2006] SHOW_RESULT 1755 CPU : 0.169999999999999 = 0.149999999999999 + 0.02 + 0 + 0 # BOUND : makespan 1000 1755 MODIFY_CNF 1377 BEGIN : [Sun Jun 18 20:07:07 2006] MODIFY_CNF 1377 END : 20874473 bytes (0 seconds) [Sun Jun 18 20:07:07 2006] MODIFY_CNF 1377 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1377 BEGIN : [Sun Jun 18 20:07:07 2006] CMD : minisat /tmp/csp2sat14133.cnf /tmp/csp2sat14133.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 582416 1655852 | 194138 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (1 /sec) decisions : 115 (85 /sec) propagations : 99999 (73529 /sec) conflict literals : 12 (0.00 % deleted) Memory used : 42.81 MB CPU time : 1.36 s SATISFIABLE VERIFY_CNF 1377 END : (1 seconds) [Sun Jun 18 20:07:08 2006] VERIFY_CNF 1377 CPU : 1.57 = 0 + 0 + 1.41 + 0.16 # RESULT : makespan 1377 SATISFIABLE SHOW_RESULT 1377 BEGIN : [Sun Jun 18 20:07:08 2006] # ASSIGN : makespan 1377 # ASSIGN : s_0_0 18 # ASSIGN : s_0_1 869 # ASSIGN : s_0_2 931 # ASSIGN : s_0_3 37 # ASSIGN : s_0_4 210 # ASSIGN : s_0_5 19 # ASSIGN : s_1_0 1183 # ASSIGN : s_1_1 37 # ASSIGN : s_1_2 663 # ASSIGN : s_1_3 250 # ASSIGN : s_1_4 566 # ASSIGN : s_1_5 58 # ASSIGN : s_2_0 92 # ASSIGN : s_2_1 1370 # ASSIGN : s_2_2 127 # ASSIGN : s_2_3 10 # ASSIGN : s_2_4 829 # ASSIGN : s_2_5 162 # ASSIGN : s_3_0 141 # ASSIGN : s_3_1 202 # ASSIGN : s_3_2 572 # ASSIGN : s_3_3 682 # ASSIGN : s_3_4 1058 # ASSIGN : s_3_5 925 # ASSIGN : s_4_0 163 # ASSIGN : s_4_1 423 # ASSIGN : s_4_2 254 # ASSIGN : s_4_3 1074 # ASSIGN : s_4_4 1348 # ASSIGN : s_4_5 1271 # ASSIGN : s_5_0 377 # ASSIGN : s_5_1 1034 # ASSIGN : s_5_2 1321 # ASSIGN : s_5_3 1277 # ASSIGN : s_5_4 1368 # ASSIGN : s_5_5 1376 SHOW_RESULT 1377 END : 1377 (0 seconds) [Sun Jun 18 20:07:08 2006] SHOW_RESULT 1377 CPU : 0.160000000000004 = 0.160000000000004 + 0 + 0 + 0 # BOUND : makespan 1000 1377 MODIFY_CNF 1188 BEGIN : [Sun Jun 18 20:07:08 2006] MODIFY_CNF 1188 END : 20874473 bytes (0 seconds) [Sun Jun 18 20:07:08 2006] MODIFY_CNF 1188 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1188 BEGIN : [Sun Jun 18 20:07:08 2006] CMD : minisat /tmp/csp2sat14133.cnf /tmp/csp2sat14133.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 514376 1451732 | 171458 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 3 (2 /sec) decisions : 82 (55 /sec) propagations : 112505 (76017 /sec) conflict literals : 22 (4.35 % deleted) Memory used : 42.81 MB CPU time : 1.48 s SATISFIABLE VERIFY_CNF 1188 END : (2 seconds) [Sun Jun 18 20:07:10 2006] VERIFY_CNF 1188 CPU : 1.67 = 0 + 0 + 1.53 + 0.14 # RESULT : makespan 1188 SATISFIABLE SHOW_RESULT 1188 BEGIN : [Sun Jun 18 20:07:10 2006] # ASSIGN : makespan 1188 # ASSIGN : s_0_0 11 # ASSIGN : s_0_1 27 # ASSIGN : s_0_2 798 # ASSIGN : s_0_3 591 # ASSIGN : s_0_4 234 # ASSIGN : s_0_5 188 # ASSIGN : s_1_0 12 # ASSIGN : s_1_1 1080 # ASSIGN : s_1_2 322 # ASSIGN : s_1_3 764 # ASSIGN : s_1_4 590 # ASSIGN : s_1_5 206 # ASSIGN : s_2_0 240 # ASSIGN : s_2_1 1101 # ASSIGN : s_2_2 275 # ASSIGN : s_2_3 1108 # ASSIGN : s_2_4 5 # ASSIGN : s_2_5 310 # ASSIGN : s_3_0 310 # ASSIGN : s_3_1 332 # ASSIGN : s_3_2 596 # ASSIGN : s_3_3 67 # ASSIGN : s_3_4 687 # ASSIGN : s_3_5 977 # ASSIGN : s_4_0 999 # ASSIGN : s_4_1 553 # ASSIGN : s_4_2 106 # ASSIGN : s_4_3 356 # ASSIGN : s_4_4 1090 # ASSIGN : s_4_5 1110 # ASSIGN : s_5_0 342 # ASSIGN : s_5_1 89 # ASSIGN : s_5_2 42 # ASSIGN : s_5_3 1135 # ASSIGN : s_5_4 1179 # ASSIGN : s_5_5 1187 SHOW_RESULT 1188 END : 1188 (0 seconds) [Sun Jun 18 20:07:10 2006] SHOW_RESULT 1188 CPU : 0.150000000000001 = 0.140000000000001 + 0.01 + 0 + 0 # BOUND : makespan 1000 1188 MODIFY_CNF 1094 BEGIN : [Sun Jun 18 20:07:10 2006] MODIFY_CNF 1094 END : 20874472 bytes (0 seconds) [Sun Jun 18 20:07:10 2006] MODIFY_CNF 1094 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1094 BEGIN : [Sun Jun 18 20:07:10 2006] CMD : minisat /tmp/csp2sat14133.cnf /tmp/csp2sat14133.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 480536 1350212 | 160178 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 5 (4 /sec) decisions : 76 (54 /sec) propagations : 115763 (81523 /sec) conflict literals : 60 (4.76 % deleted) Memory used : 42.81 MB CPU time : 1.42 s SATISFIABLE VERIFY_CNF 1094 END : (2 seconds) [Sun Jun 18 20:07:12 2006] VERIFY_CNF 1094 CPU : 1.59 = 0 + 0 + 1.46 + 0.13 # RESULT : makespan 1094 SATISFIABLE SHOW_RESULT 1094 BEGIN : [Sun Jun 18 20:07:12 2006] # ASSIGN : makespan 1094 # ASSIGN : s_0_0 3 # ASSIGN : s_0_1 1032 # ASSIGN : s_0_2 429 # ASSIGN : s_0_3 850 # ASSIGN : s_0_4 73 # ASSIGN : s_0_5 39 # ASSIGN : s_1_0 900 # ASSIGN : s_1_1 33 # ASSIGN : s_1_2 161 # ASSIGN : s_1_3 534 # ASSIGN : s_1_4 437 # ASSIGN : s_1_5 57 # ASSIGN : s_2_0 4 # ASSIGN : s_2_1 54 # ASSIGN : s_2_2 126 # ASSIGN : s_2_3 1067 # ASSIGN : s_2_4 836 # ASSIGN : s_2_5 169 # ASSIGN : s_3_0 39 # ASSIGN : s_3_1 61 # ASSIGN : s_3_2 1003 # ASSIGN : s_3_3 291 # ASSIGN : s_3_4 546 # ASSIGN : s_3_5 855 # ASSIGN : s_4_0 728 # ASSIGN : s_4_1 282 # ASSIGN : s_4_2 819 # ASSIGN : s_4_3 85 # ASSIGN : s_4_4 1065 # ASSIGN : s_4_5 988 # ASSIGN : s_5_0 71 # ASSIGN : s_5_1 780 # ASSIGN : s_5_2 24 # ASSIGN : s_5_3 1023 # ASSIGN : s_5_4 1085 # ASSIGN : s_5_5 1093 SHOW_RESULT 1094 END : 1094 (0 seconds) [Sun Jun 18 20:07:12 2006] SHOW_RESULT 1094 CPU : 0.159999999999999 = 0.149999999999999 + 0.00999999999999998 + 0 + 0 # BOUND : makespan 1000 1094 MODIFY_CNF 1047 BEGIN : [Sun Jun 18 20:07:12 2006] MODIFY_CNF 1047 END : 20874472 bytes (0 seconds) [Sun Jun 18 20:07:12 2006] MODIFY_CNF 1047 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1047 BEGIN : [Sun Jun 18 20:07:12 2006] CMD : minisat /tmp/csp2sat14133.cnf /tmp/csp2sat14133.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 463616 1299452 | 154538 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 39 (25 /sec) decisions : 107 (68 /sec) propagations : 353424 (225111 /sec) conflict literals : 321 (28.35 % deleted) Memory used : 42.81 MB CPU time : 1.57 s SATISFIABLE VERIFY_CNF 1047 END : (2 seconds) [Sun Jun 18 20:07:14 2006] VERIFY_CNF 1047 CPU : 1.74 = 0 + 0 + 1.62 + 0.12 # RESULT : makespan 1047 SATISFIABLE SHOW_RESULT 1047 BEGIN : [Sun Jun 18 20:07:14 2006] # ASSIGN : makespan 1047 # ASSIGN : s_0_0 1046 # ASSIGN : s_0_1 23 # ASSIGN : s_0_2 281 # ASSIGN : s_0_3 85 # ASSIGN : s_0_4 671 # ASSIGN : s_0_5 5 # ASSIGN : s_1_0 57 # ASSIGN : s_1_1 2 # ASSIGN : s_1_2 674 # ASSIGN : s_1_3 258 # ASSIGN : s_1_4 574 # ASSIGN : s_1_5 942 # ASSIGN : s_2_0 1005 # ASSIGN : s_2_1 1040 # ASSIGN : s_2_2 964 # ASSIGN : s_2_3 14 # ASSIGN : s_2_4 46 # ASSIGN : s_2_5 275 # ASSIGN : s_3_0 19 # ASSIGN : s_3_1 819 # ASSIGN : s_3_2 190 # ASSIGN : s_3_3 576 # ASSIGN : s_3_4 284 # ASSIGN : s_3_5 41 # ASSIGN : s_4_0 251 # ASSIGN : s_4_1 373 # ASSIGN : s_4_2 5 # ASSIGN : s_4_3 830 # ASSIGN : s_4_4 1027 # ASSIGN : s_4_5 174 # ASSIGN : s_5_0 342 # ASSIGN : s_5_1 99 # ASSIGN : s_5_2 999 # ASSIGN : s_5_3 41 # ASSIGN : s_5_4 33 # ASSIGN : s_5_5 1046 SHOW_RESULT 1047 END : 1047 (0 seconds) [Sun Jun 18 20:07:14 2006] SHOW_RESULT 1047 CPU : 0.150000000000006 = 0.150000000000006 + 0 + 0 + 0 # BOUND : makespan 1000 1047 MODIFY_CNF 1023 BEGIN : [Sun Jun 18 20:07:14 2006] MODIFY_CNF 1023 END : 20874472 bytes (0 seconds) [Sun Jun 18 20:07:14 2006] MODIFY_CNF 1023 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1023 BEGIN : [Sun Jun 18 20:07:14 2006] CMD : minisat /tmp/csp2sat14133.cnf /tmp/csp2sat14133.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 454976 1273532 | 151658 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 48 (30 /sec) decisions : 61 (38 /sec) propagations : 394350 (246469 /sec) conflict literals : 276 (34.44 % deleted) Memory used : 42.41 MB CPU time : 1.6 s UNSATISFIABLE VERIFY_CNF 1023 END : (2 seconds) [Sun Jun 18 20:07:16 2006] VERIFY_CNF 1023 CPU : 1.76 = 0.00999999999999801 + 0 + 1.6 + 0.15 # RESULT : makespan 1023 UNSATISFIABLE # BOUND : makespan 1024 1047 MODIFY_CNF 1035 BEGIN : [Sun Jun 18 20:07:16 2006] MODIFY_CNF 1035 END : 20874472 bytes (0 seconds) [Sun Jun 18 20:07:16 2006] MODIFY_CNF 1035 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1035 BEGIN : [Sun Jun 18 20:07:16 2006] CMD : minisat /tmp/csp2sat14133.cnf /tmp/csp2sat14133.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 459296 1286492 | 153098 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 68 (41 /sec) decisions : 85 (51 /sec) propagations : 490960 (295759 /sec) conflict literals : 459 (31.08 % deleted) Memory used : 42.41 MB CPU time : 1.66 s UNSATISFIABLE VERIFY_CNF 1035 END : (1 seconds) [Sun Jun 18 20:07:17 2006] VERIFY_CNF 1035 CPU : 1.81 = 0 + 0 + 1.66 + 0.15 # RESULT : makespan 1035 UNSATISFIABLE # BOUND : makespan 1036 1047 MODIFY_CNF 1041 BEGIN : [Sun Jun 18 20:07:17 2006] MODIFY_CNF 1041 END : 20874472 bytes (0 seconds) [Sun Jun 18 20:07:17 2006] MODIFY_CNF 1041 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1041 BEGIN : [Sun Jun 18 20:07:17 2006] CMD : minisat /tmp/csp2sat14133.cnf /tmp/csp2sat14133.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 461456 1292972 | 153818 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 76 (44 /sec) decisions : 91 (52 /sec) propagations : 566797 (325745 /sec) conflict literals : 509 (28.31 % deleted) Memory used : 42.42 MB CPU time : 1.74 s UNSATISFIABLE VERIFY_CNF 1041 END : (2 seconds) [Sun Jun 18 20:07:19 2006] VERIFY_CNF 1041 CPU : 1.83 = 0 + 0 + 1.74 + 0.0899999999999999 # RESULT : makespan 1041 UNSATISFIABLE # BOUND : makespan 1042 1047 MODIFY_CNF 1044 BEGIN : [Sun Jun 18 20:07:19 2006] MODIFY_CNF 1044 END : 20874472 bytes (0 seconds) [Sun Jun 18 20:07:19 2006] MODIFY_CNF 1044 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1044 BEGIN : [Sun Jun 18 20:07:19 2006] CMD : minisat /tmp/csp2sat14133.cnf /tmp/csp2sat14133.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 462536 1296212 | 154178 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 90 (49 /sec) decisions : 110 (60 /sec) propagations : 663911 (362793 /sec) conflict literals : 493 (36.96 % deleted) Memory used : 42.43 MB CPU time : 1.83 s UNSATISFIABLE VERIFY_CNF 1044 END : (2 seconds) [Sun Jun 18 20:07:21 2006] VERIFY_CNF 1044 CPU : 1.91 = 0 + 0 + 1.83 + 0.0800000000000001 # RESULT : makespan 1044 UNSATISFIABLE # BOUND : makespan 1045 1047 MODIFY_CNF 1046 BEGIN : [Sun Jun 18 20:07:21 2006] MODIFY_CNF 1046 END : 20874472 bytes (0 seconds) [Sun Jun 18 20:07:21 2006] MODIFY_CNF 1046 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1046 BEGIN : [Sun Jun 18 20:07:21 2006] CMD : minisat /tmp/csp2sat14133.cnf /tmp/csp2sat14133.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 463256 1298372 | 154418 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 40 (27 /sec) decisions : 94 (64 /sec) propagations : 343674 (233792 /sec) conflict literals : 323 (30.69 % deleted) Memory used : 42.81 MB CPU time : 1.47 s SATISFIABLE VERIFY_CNF 1046 END : (2 seconds) [Sun Jun 18 20:07:23 2006] VERIFY_CNF 1046 CPU : 1.67 = 0 + 0 + 1.52 + 0.15 # RESULT : makespan 1046 SATISFIABLE SHOW_RESULT 1046 BEGIN : [Sun Jun 18 20:07:23 2006] # ASSIGN : makespan 1046 # ASSIGN : s_0_0 1045 # ASSIGN : s_0_1 21 # ASSIGN : s_0_2 280 # ASSIGN : s_0_3 83 # ASSIGN : s_0_4 670 # ASSIGN : s_0_5 256 # ASSIGN : s_1_0 56 # ASSIGN : s_1_1 0 # ASSIGN : s_1_2 673 # ASSIGN : s_1_3 257 # ASSIGN : s_1_4 573 # ASSIGN : s_1_5 941 # ASSIGN : s_2_0 1004 # ASSIGN : s_2_1 1039 # ASSIGN : s_2_2 963 # ASSIGN : s_2_3 12 # ASSIGN : s_2_4 45 # ASSIGN : s_2_5 274 # ASSIGN : s_3_0 18 # ASSIGN : s_3_1 818 # ASSIGN : s_3_2 189 # ASSIGN : s_3_3 575 # ASSIGN : s_3_4 283 # ASSIGN : s_3_5 40 # ASSIGN : s_4_0 250 # ASSIGN : s_4_1 372 # ASSIGN : s_4_2 4 # ASSIGN : s_4_3 829 # ASSIGN : s_4_4 1026 # ASSIGN : s_4_5 173 # ASSIGN : s_5_0 341 # ASSIGN : s_5_1 98 # ASSIGN : s_5_2 998 # ASSIGN : s_5_3 39 # ASSIGN : s_5_4 31 # ASSIGN : s_5_5 1045 SHOW_RESULT 1046 END : 1046 (0 seconds) [Sun Jun 18 20:07:23 2006] SHOW_RESULT 1046 CPU : 0.150000000000001 = 0.140000000000001 + 0.01 + 0 + 0 # BOUND : makespan 1045 1046 MODIFY_CNF 1045 BEGIN : [Sun Jun 18 20:07:23 2006] MODIFY_CNF 1045 END : 20874472 bytes (0 seconds) [Sun Jun 18 20:07:23 2006] MODIFY_CNF 1045 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1045 BEGIN : [Sun Jun 18 20:07:23 2006] CMD : minisat /tmp/csp2sat14133.cnf /tmp/csp2sat14133.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 462896 1297292 | 154298 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 35 (23 /sec) decisions : 85 (56 /sec) propagations : 320375 (210773 /sec) conflict literals : 269 (30.49 % deleted) Memory used : 42.81 MB CPU time : 1.52 s SATISFIABLE VERIFY_CNF 1045 END : (2 seconds) [Sun Jun 18 20:07:25 2006] VERIFY_CNF 1045 CPU : 1.69 = 0 + 0 + 1.57 + 0.12 # RESULT : makespan 1045 SATISFIABLE SHOW_RESULT 1045 BEGIN : [Sun Jun 18 20:07:25 2006] # ASSIGN : makespan 1045 # ASSIGN : s_0_0 1044 # ASSIGN : s_0_1 21 # ASSIGN : s_0_2 279 # ASSIGN : s_0_3 83 # ASSIGN : s_0_4 669 # ASSIGN : s_0_5 3 # ASSIGN : s_1_0 55 # ASSIGN : s_1_1 0 # ASSIGN : s_1_2 672 # ASSIGN : s_1_3 256 # ASSIGN : s_1_4 572 # ASSIGN : s_1_5 940 # ASSIGN : s_2_0 1003 # ASSIGN : s_2_1 1038 # ASSIGN : s_2_2 962 # ASSIGN : s_2_3 12 # ASSIGN : s_2_4 44 # ASSIGN : s_2_5 273 # ASSIGN : s_3_0 17 # ASSIGN : s_3_1 817 # ASSIGN : s_3_2 188 # ASSIGN : s_3_3 574 # ASSIGN : s_3_4 282 # ASSIGN : s_3_5 39 # ASSIGN : s_4_0 249 # ASSIGN : s_4_1 371 # ASSIGN : s_4_2 3 # ASSIGN : s_4_3 828 # ASSIGN : s_4_4 1025 # ASSIGN : s_4_5 172 # ASSIGN : s_5_0 340 # ASSIGN : s_5_1 97 # ASSIGN : s_5_2 997 # ASSIGN : s_5_3 39 # ASSIGN : s_5_4 31 # ASSIGN : s_5_5 1044 SHOW_RESULT 1045 END : 1045 (0 seconds) [Sun Jun 18 20:07:25 2006] SHOW_RESULT 1045 CPU : 0.149999999999999 = 0.149999999999999 + 0 + 0 + 0 # BOUND : makespan 1045 1045 MAIN END : (58 seconds) [Sun Jun 18 20:07:25 2006] MAIN CPU : 57.31 = 38.3 + 0.25 + 17.28 + 1.48