# TIMEOUT 18000 MAIN BEGIN : [Sun Jun 18 16:47:33 2006] READ BEGIN : csp/gp08-01.csp [Sun Jun 18 16:47:33 2006] READ END : csp/gp08-01.csp (1 seconds) [Sun Jun 18 16:47:34 2006] READ CPU : 0.99 = 0.97 + 0.02 + 0 + 0 # BOUND : makespan 1000 2865 GENERATE_CNF 2865 BEGIN : [Sun Jun 18 16:47:34 2006] GENERATE_CNF 2865 END : 186315 variables 2762188 clauses 64120056 bytes (105 seconds) [Sun Jun 18 16:49:19 2006] GENERATE_CNF 2865 CPU : 105.48 = 105.11 + 0.37 + 0 + 0 MODIFY_CNF 1932 BEGIN : [Sun Jun 18 16:49:19 2006] MODIFY_CNF 1932 END : 64120062 bytes (0 seconds) [Sun Jun 18 16:49:19 2006] MODIFY_CNF 1932 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1932 BEGIN : [Sun Jun 18 16:49:19 2006] CMD : minisat /tmp/csp2sat10312.cnf /tmp/csp2sat10312.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1924871 5590354 | 641623 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (1 /sec) decisions : 336 (86 /sec) propagations : 227047 (57920 /sec) conflict literals : 25 (7.41 % deleted) Memory used : 115.16 MB CPU time : 3.92 s SATISFIABLE VERIFY_CNF 1932 END : (5 seconds) [Sun Jun 18 16:49:24 2006] VERIFY_CNF 1932 CPU : 4.29 = 0 + 0 + 4.01 + 0.28 # RESULT : makespan 1932 SATISFIABLE SHOW_RESULT 1932 BEGIN : [Sun Jun 18 16:49:24 2006] # ASSIGN : makespan 1932 # ASSIGN : s_0_0 8 # ASSIGN : s_0_1 483 # ASSIGN : s_0_2 887 # ASSIGN : s_0_3 160 # ASSIGN : s_0_4 731 # ASSIGN : s_0_5 285 # ASSIGN : s_0_6 292 # ASSIGN : s_0_7 291 # ASSIGN : s_1_0 9 # ASSIGN : s_1_1 160 # ASSIGN : s_1_2 1325 # ASSIGN : s_1_3 161 # ASSIGN : s_1_4 1082 # ASSIGN : s_1_5 442 # ASSIGN : s_1_6 441 # ASSIGN : s_1_7 298 # ASSIGN : s_2_0 13 # ASSIGN : s_2_1 317 # ASSIGN : s_2_2 1422 # ASSIGN : s_2_3 321 # ASSIGN : s_2_4 1215 # ASSIGN : s_2_5 1041 # ASSIGN : s_2_6 531 # ASSIGN : s_2_7 326 # ASSIGN : s_3_0 1009 # ASSIGN : s_3_1 321 # ASSIGN : s_3_2 1817 # ASSIGN : s_3_3 322 # ASSIGN : s_3_4 1216 # ASSIGN : s_3_5 1128 # ASSIGN : s_3_6 1130 # ASSIGN : s_3_7 327 # ASSIGN : s_4_0 505 # ASSIGN : s_4_1 887 # ASSIGN : s_4_2 1831 # ASSIGN : s_4_3 1931 # ASSIGN : s_4_4 1466 # ASSIGN : s_4_5 1163 # ASSIGN : s_4_6 1162 # ASSIGN : s_4_7 904 # ASSIGN : s_5_0 14 # ASSIGN : s_5_1 888 # ASSIGN : s_5_2 1884 # ASSIGN : s_5_3 708 # ASSIGN : s_5_4 1467 # ASSIGN : s_5_5 1466 # ASSIGN : s_5_6 1301 # ASSIGN : s_5_7 1333 # ASSIGN : s_6_0 15 # ASSIGN : s_6_1 1561 # ASSIGN : s_6_2 1885 # ASSIGN : s_6_3 710 # ASSIGN : s_6_4 1886 # ASSIGN : s_6_5 1611 # ASSIGN : s_6_6 1612 # ASSIGN : s_6_7 1927 # ASSIGN : s_7_0 932 # ASSIGN : s_7_1 1563 # ASSIGN : s_7_2 1893 # ASSIGN : s_7_3 934 # ASSIGN : s_7_4 1894 # ASSIGN : s_7_5 1929 # ASSIGN : s_7_6 1930 # ASSIGN : s_7_7 1928 SHOW_RESULT 1932 END : 1932 (0 seconds) [Sun Jun 18 16:49:24 2006] SHOW_RESULT 1932 CPU : 0.389999999999999 = 0.359999999999999 + 0.03 + 0 + 0 # BOUND : makespan 1000 1932 MODIFY_CNF 1466 BEGIN : [Sun Jun 18 16:49:24 2006] MODIFY_CNF 1466 END : 64120062 bytes (0 seconds) [Sun Jun 18 16:49:24 2006] MODIFY_CNF 1466 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1466 BEGIN : [Sun Jun 18 16:49:24 2006] CMD : minisat /tmp/csp2sat10312.cnf /tmp/csp2sat10312.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1507335 4337746 | 502445 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 6 (2 /sec) decisions : 359 (90 /sec) propagations : 242510 (61086 /sec) conflict literals : 44 (0.00 % deleted) Memory used : 115.15 MB CPU time : 3.97 s SATISFIABLE VERIFY_CNF 1466 END : (5 seconds) [Sun Jun 18 16:49:29 2006] VERIFY_CNF 1466 CPU : 4.38 = 0 + 0 + 4.05 + 0.33 # RESULT : makespan 1466 SATISFIABLE SHOW_RESULT 1466 BEGIN : [Sun Jun 18 16:49:29 2006] # ASSIGN : makespan 1466 # ASSIGN : s_0_0 18 # ASSIGN : s_0_1 780 # ASSIGN : s_0_2 1028 # ASSIGN : s_0_3 570 # ASSIGN : s_0_4 583 # ASSIGN : s_0_5 29 # ASSIGN : s_0_6 182 # ASSIGN : s_0_7 35 # ASSIGN : s_1_0 19 # ASSIGN : s_1_1 30 # ASSIGN : s_1_2 931 # ASSIGN : s_1_3 178 # ASSIGN : s_1_4 1295 # ASSIGN : s_1_5 332 # ASSIGN : s_1_6 331 # ASSIGN : s_1_7 36 # ASSIGN : s_2_0 23 # ASSIGN : s_2_1 31 # ASSIGN : s_2_2 65 # ASSIGN : s_2_3 62 # ASSIGN : s_2_4 63 # ASSIGN : s_2_5 1034 # ASSIGN : s_2_6 524 # ASSIGN : s_2_7 64 # ASSIGN : s_3_0 1002 # ASSIGN : s_3_1 35 # ASSIGN : s_3_2 51 # ASSIGN : s_3_3 315 # ASSIGN : s_3_4 65 # ASSIGN : s_3_5 1121 # ASSIGN : s_3_6 1123 # ASSIGN : s_3_7 320 # ASSIGN : s_4_0 515 # ASSIGN : s_4_1 36 # ASSIGN : s_4_2 460 # ASSIGN : s_4_3 513 # ASSIGN : s_4_4 514 # ASSIGN : s_4_5 1157 # ASSIGN : s_4_6 1155 # ASSIGN : s_4_7 897 # ASSIGN : s_5_0 24 # ASSIGN : s_5_1 37 # ASSIGN : s_5_2 36 # ASSIGN : s_5_3 571 # ASSIGN : s_5_4 739 # ASSIGN : s_5_5 1460 # ASSIGN : s_5_6 1156 # ASSIGN : s_5_7 1327 # ASSIGN : s_6_0 25 # ASSIGN : s_6_1 1178 # ASSIGN : s_6_2 572 # ASSIGN : s_6_3 573 # ASSIGN : s_6_4 1180 # ASSIGN : s_6_5 1461 # ASSIGN : s_6_6 1188 # ASSIGN : s_6_7 1464 # ASSIGN : s_7_0 1426 # ASSIGN : s_7_1 450 # ASSIGN : s_7_2 796 # ASSIGN : s_7_3 797 # ASSIGN : s_7_4 1428 # ASSIGN : s_7_5 1462 # ASSIGN : s_7_6 1463 # ASSIGN : s_7_7 1465 SHOW_RESULT 1466 END : 1466 (0 seconds) [Sun Jun 18 16:49:29 2006] SHOW_RESULT 1466 CPU : 0.460000000000003 = 0.450000000000003 + 0.01 + 0 + 0 # BOUND : makespan 1000 1466 MODIFY_CNF 1233 BEGIN : [Sun Jun 18 16:49:29 2006] MODIFY_CNF 1233 END : 64120062 bytes (0 seconds) [Sun Jun 18 16:49:29 2006] MODIFY_CNF 1233 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1233 BEGIN : [Sun Jun 18 16:49:29 2006] CMD : minisat /tmp/csp2sat10312.cnf /tmp/csp2sat10312.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1298567 3711442 | 432855 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 6 (1 /sec) decisions : 191 (44 /sec) propagations : 220813 (50529 /sec) conflict literals : 95 (14.41 % deleted) Memory used : 115.15 MB CPU time : 4.37 s SATISFIABLE VERIFY_CNF 1233 END : (5 seconds) [Sun Jun 18 16:49:34 2006] VERIFY_CNF 1233 CPU : 4.79 = 0 + 0 + 4.47 + 0.32 # RESULT : makespan 1233 SATISFIABLE SHOW_RESULT 1233 BEGIN : [Sun Jun 18 16:49:34 2006] # ASSIGN : makespan 1233 # ASSIGN : s_0_0 1 # ASSIGN : s_0_1 152 # ASSIGN : s_0_2 400 # ASSIGN : s_0_3 1220 # ASSIGN : s_0_4 1039 # ASSIGN : s_0_5 1221 # ASSIGN : s_0_6 3 # ASSIGN : s_0_7 2 # ASSIGN : s_1_0 23 # ASSIGN : s_1_1 27 # ASSIGN : s_1_2 138 # ASSIGN : s_1_3 1083 # ASSIGN : s_1_4 906 # ASSIGN : s_1_5 307 # ASSIGN : s_1_6 306 # ASSIGN : s_1_7 28 # ASSIGN : s_2_0 3 # ASSIGN : s_2_1 4 # ASSIGN : s_2_2 838 # ASSIGN : s_2_3 8 # ASSIGN : s_2_4 34 # ASSIGN : s_2_5 220 # ASSIGN : s_2_6 328 # ASSIGN : s_2_7 56 # ASSIGN : s_3_0 1114 # ASSIGN : s_3_1 2 # ASSIGN : s_3_2 16 # ASSIGN : s_3_3 3 # ASSIGN : s_3_4 634 # ASSIGN : s_3_5 916 # ASSIGN : s_3_6 884 # ASSIGN : s_3_7 57 # ASSIGN : s_4_0 83 # ASSIGN : s_4_1 8 # ASSIGN : s_4_2 30 # ASSIGN : s_4_3 9 # ASSIGN : s_4_4 633 # ASSIGN : s_4_5 918 # ASSIGN : s_4_6 917 # ASSIGN : s_4_7 659 # ASSIGN : s_5_0 8 # ASSIGN : s_5_1 452 # ASSIGN : s_5_2 9 # ASSIGN : s_5_3 10 # ASSIGN : s_5_4 35 # ASSIGN : s_5_5 1227 # ASSIGN : s_5_6 923 # ASSIGN : s_5_7 1094 # ASSIGN : s_6_0 465 # ASSIGN : s_6_1 9 # ASSIGN : s_6_2 11 # ASSIGN : s_6_3 12 # ASSIGN : s_6_4 457 # ASSIGN : s_6_5 1228 # ASSIGN : s_6_6 955 # ASSIGN : s_6_7 1231 # ASSIGN : s_7_0 81 # ASSIGN : s_7_1 865 # ASSIGN : s_7_2 235 # ASSIGN : s_7_3 236 # ASSIGN : s_7_4 1195 # ASSIGN : s_7_5 1229 # ASSIGN : s_7_6 1230 # ASSIGN : s_7_7 1232 SHOW_RESULT 1233 END : 1233 (0 seconds) [Sun Jun 18 16:49:34 2006] SHOW_RESULT 1233 CPU : 0.409999999999991 = 0.399999999999991 + 0.01 + 0 + 0 # BOUND : makespan 1000 1233 MODIFY_CNF 1116 BEGIN : [Sun Jun 18 16:49:34 2006] MODIFY_CNF 1116 END : 64120062 bytes (0 seconds) [Sun Jun 18 16:49:34 2006] MODIFY_CNF 1116 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1116 BEGIN : [Sun Jun 18 16:49:34 2006] CMD : minisat /tmp/csp2sat10312.cnf /tmp/csp2sat10312.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1193735 3396946 | 397911 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (0 /sec) decisions : 10 (2 /sec) propagations : 127305 (30025 /sec) conflict literals : 1 (0.00 % deleted) Memory used : 114.21 MB CPU time : 4.24 s UNSATISFIABLE VERIFY_CNF 1116 END : (5 seconds) [Sun Jun 18 16:49:39 2006] VERIFY_CNF 1116 CPU : 4.62000000000001 = 0.0100000000000051 + 0 + 4.24 + 0.37 # RESULT : makespan 1116 UNSATISFIABLE # BOUND : makespan 1117 1233 MODIFY_CNF 1175 BEGIN : [Sun Jun 18 16:49:39 2006] MODIFY_CNF 1175 END : 64120062 bytes (0 seconds) [Sun Jun 18 16:49:39 2006] MODIFY_CNF 1175 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1175 BEGIN : [Sun Jun 18 16:49:39 2006] CMD : minisat /tmp/csp2sat10312.cnf /tmp/csp2sat10312.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1246599 3555538 | 415533 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 1 (0 /sec) decisions : 178 (41 /sec) propagations : 193494 (44481 /sec) conflict literals : 10 (16.67 % deleted) Memory used : 115.15 MB CPU time : 4.35 s SATISFIABLE VERIFY_CNF 1175 END : (5 seconds) [Sun Jun 18 16:49:44 2006] VERIFY_CNF 1175 CPU : 4.81 = 0 + 0 + 4.48 + 0.33 # RESULT : makespan 1175 SATISFIABLE SHOW_RESULT 1175 BEGIN : [Sun Jun 18 16:49:44 2006] # ASSIGN : makespan 1175 # ASSIGN : s_0_0 12 # ASSIGN : s_0_1 927 # ASSIGN : s_0_2 97 # ASSIGN : s_0_3 17 # ASSIGN : s_0_4 535 # ASSIGN : s_0_5 56 # ASSIGN : s_0_6 716 # ASSIGN : s_0_7 0 # ASSIGN : s_1_0 937 # ASSIGN : s_1_1 0 # ASSIGN : s_1_2 1074 # ASSIGN : s_1_3 47 # ASSIGN : s_1_4 941 # ASSIGN : s_1_5 266 # ASSIGN : s_1_6 1174 # ASSIGN : s_1_7 1 # ASSIGN : s_2_0 13 # ASSIGN : s_2_1 14 # ASSIGN : s_2_2 679 # ASSIGN : s_2_3 18 # ASSIGN : s_2_4 24 # ASSIGN : s_2_5 62 # ASSIGN : s_2_6 149 # ASSIGN : s_2_7 29 # ASSIGN : s_3_0 1015 # ASSIGN : s_3_1 18 # ASSIGN : s_3_2 4 # ASSIGN : s_3_3 19 # ASSIGN : s_3_4 691 # ASSIGN : s_3_5 1173 # ASSIGN : s_3_6 659 # ASSIGN : s_3_7 30 # ASSIGN : s_4_0 26 # ASSIGN : s_4_1 23 # ASSIGN : s_4_2 554 # ASSIGN : s_4_3 24 # ASSIGN : s_4_4 25 # ASSIGN : s_4_5 867 # ASSIGN : s_4_6 865 # ASSIGN : s_4_7 607 # ASSIGN : s_5_0 25 # ASSIGN : s_5_1 452 # ASSIGN : s_5_2 1171 # ASSIGN : s_5_3 33 # ASSIGN : s_5_4 35 # ASSIGN : s_5_5 865 # ASSIGN : s_5_6 866 # ASSIGN : s_5_7 1038 # ASSIGN : s_6_0 408 # ASSIGN : s_6_1 25 # ASSIGN : s_6_2 1172 # ASSIGN : s_6_3 184 # ASSIGN : s_6_4 27 # ASSIGN : s_6_5 1171 # ASSIGN : s_6_6 898 # ASSIGN : s_6_7 1173 # ASSIGN : s_7_0 1134 # ASSIGN : s_7_1 122 # ASSIGN : s_7_2 1173 # ASSIGN : s_7_3 505 # ASSIGN : s_7_4 1136 # ASSIGN : s_7_5 1170 # ASSIGN : s_7_6 1171 # ASSIGN : s_7_7 1174 SHOW_RESULT 1175 END : 1175 (0 seconds) [Sun Jun 18 16:49:44 2006] SHOW_RESULT 1175 CPU : 0.409999999999991 = 0.399999999999991 + 0.01 + 0 + 0 # BOUND : makespan 1117 1175 MODIFY_CNF 1146 BEGIN : [Sun Jun 18 16:49:44 2006] MODIFY_CNF 1146 END : 64120062 bytes (0 seconds) [Sun Jun 18 16:49:44 2006] MODIFY_CNF 1146 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1146 BEGIN : [Sun Jun 18 16:49:44 2006] CMD : minisat /tmp/csp2sat10312.cnf /tmp/csp2sat10312.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1220615 3477586 | 406871 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 5 (1 /sec) decisions : 227 (52 /sec) propagations : 248291 (57210 /sec) conflict literals : 21 (8.70 % deleted) Memory used : 115.15 MB CPU time : 4.34 s SATISFIABLE VERIFY_CNF 1146 END : (5 seconds) [Sun Jun 18 16:49:49 2006] VERIFY_CNF 1146 CPU : 4.88 = 0 + 0 + 4.43 + 0.45 # RESULT : makespan 1146 SATISFIABLE SHOW_RESULT 1146 BEGIN : [Sun Jun 18 16:49:49 2006] # ASSIGN : makespan 1146 # ASSIGN : s_0_0 4 # ASSIGN : s_0_1 345 # ASSIGN : s_0_2 701 # ASSIGN : s_0_3 9 # ASSIGN : s_0_4 20 # ASSIGN : s_0_5 14 # ASSIGN : s_0_6 196 # ASSIGN : s_0_7 1142 # ASSIGN : s_1_0 5 # ASSIGN : s_1_1 0 # ASSIGN : s_1_2 25 # ASSIGN : s_1_3 1006 # ASSIGN : s_1_4 722 # ASSIGN : s_1_5 123 # ASSIGN : s_1_6 122 # ASSIGN : s_1_7 978 # ASSIGN : s_2_0 9 # ASSIGN : s_2_1 1 # ASSIGN : s_2_2 238 # ASSIGN : s_2_3 10 # ASSIGN : s_2_4 11 # ASSIGN : s_2_5 34 # ASSIGN : s_2_6 633 # ASSIGN : s_2_7 1143 # ASSIGN : s_3_0 12 # ASSIGN : s_3_1 5 # ASSIGN : s_3_2 150 # ASSIGN : s_3_3 131 # ASSIGN : s_3_4 855 # ASSIGN : s_3_5 10 # ASSIGN : s_3_6 164 # ASSIGN : s_3_7 278 # ASSIGN : s_4_0 266 # ASSIGN : s_4_1 6 # ASSIGN : s_4_2 648 # ASSIGN : s_4_3 1143 # ASSIGN : s_4_4 1142 # ASSIGN : s_4_5 839 # ASSIGN : s_4_6 7 # ASSIGN : s_4_7 8 # ASSIGN : s_5_0 131 # ASSIGN : s_5_1 593 # ASSIGN : s_5_2 1139 # ASSIGN : s_5_3 1144 # ASSIGN : s_5_4 176 # ASSIGN : s_5_5 121 # ASSIGN : s_5_6 132 # ASSIGN : s_5_7 1006 # ASSIGN : s_6_0 649 # ASSIGN : s_6_1 10 # ASSIGN : s_6_2 1140 # ASSIGN : s_6_3 136 # ASSIGN : s_6_4 12 # ASSIGN : s_6_5 122 # ASSIGN : s_6_6 360 # ASSIGN : s_6_7 1144 # ASSIGN : s_7_0 1139 # ASSIGN : s_7_1 15 # ASSIGN : s_7_2 1141 # ASSIGN : s_7_3 377 # ASSIGN : s_7_4 1105 # ASSIGN : s_7_5 1142 # ASSIGN : s_7_6 1143 # ASSIGN : s_7_7 1145 SHOW_RESULT 1146 END : 1146 (0 seconds) [Sun Jun 18 16:49:49 2006] SHOW_RESULT 1146 CPU : 0.419999999999997 = 0.409999999999997 + 0.01 + 0 + 0 # BOUND : makespan 1117 1146 MODIFY_CNF 1131 BEGIN : [Sun Jun 18 16:49:49 2006] MODIFY_CNF 1131 END : 64120062 bytes (0 seconds) [Sun Jun 18 16:49:49 2006] MODIFY_CNF 1131 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1131 BEGIN : [Sun Jun 18 16:49:49 2006] CMD : minisat /tmp/csp2sat10312.cnf /tmp/csp2sat10312.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1207175 3437266 | 402391 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 6 (1 /sec) decisions : 169 (39 /sec) propagations : 226388 (52894 /sec) conflict literals : 31 (3.12 % deleted) Memory used : 115.15 MB CPU time : 4.28 s SATISFIABLE VERIFY_CNF 1131 END : (5 seconds) [Sun Jun 18 16:49:54 2006] VERIFY_CNF 1131 CPU : 4.8 = 0 + 0 + 4.36 + 0.44 # RESULT : makespan 1131 SATISFIABLE SHOW_RESULT 1131 BEGIN : [Sun Jun 18 16:49:54 2006] # ASSIGN : makespan 1131 # ASSIGN : s_0_0 964 # ASSIGN : s_0_1 549 # ASSIGN : s_0_2 111 # ASSIGN : s_0_3 23 # ASSIGN : s_0_4 965 # ASSIGN : s_0_5 31 # ASSIGN : s_0_6 815 # ASSIGN : s_0_7 0 # ASSIGN : s_1_0 1123 # ASSIGN : s_1_1 5 # ASSIGN : s_1_2 1021 # ASSIGN : s_1_3 31 # ASSIGN : s_1_4 289 # ASSIGN : s_1_5 422 # ASSIGN : s_1_6 30 # ASSIGN : s_1_7 261 # ASSIGN : s_2_0 979 # ASSIGN : s_2_1 6 # ASSIGN : s_2_2 584 # ASSIGN : s_2_3 24 # ASSIGN : s_2_4 0 # ASSIGN : s_2_5 1033 # ASSIGN : s_2_6 32 # ASSIGN : s_2_7 1 # ASSIGN : s_3_0 980 # ASSIGN : s_3_1 10 # ASSIGN : s_3_2 11 # ASSIGN : s_3_3 25 # ASSIGN : s_3_4 39 # ASSIGN : s_3_5 37 # ASSIGN : s_3_6 1099 # ASSIGN : s_3_7 294 # ASSIGN : s_4_0 490 # ASSIGN : s_4_1 29 # ASSIGN : s_4_2 57 # ASSIGN : s_4_3 30 # ASSIGN : s_4_4 4 # ASSIGN : s_4_5 119 # ASSIGN : s_4_6 31 # ASSIGN : s_4_7 872 # ASSIGN : s_5_0 1127 # ASSIGN : s_5_1 135 # ASSIGN : s_5_2 1118 # ASSIGN : s_5_3 0 # ASSIGN : s_5_4 548 # ASSIGN : s_5_5 1032 # ASSIGN : s_5_6 1067 # ASSIGN : s_5_7 2 # ASSIGN : s_6_0 0 # ASSIGN : s_6_1 1129 # ASSIGN : s_6_2 1119 # ASSIGN : s_6_3 895 # ASSIGN : s_6_4 1121 # ASSIGN : s_6_5 1120 # ASSIGN : s_6_6 542 # ASSIGN : s_6_7 871 # ASSIGN : s_7_0 1128 # ASSIGN : s_7_1 797 # ASSIGN : s_7_2 110 # ASSIGN : s_7_3 168 # ASSIGN : s_7_4 5 # ASSIGN : s_7_5 1127 # ASSIGN : s_7_6 3 # ASSIGN : s_7_7 1130 SHOW_RESULT 1131 END : 1131 (1 seconds) [Sun Jun 18 16:49:55 2006] SHOW_RESULT 1131 CPU : 0.409999999999997 = 0.409999999999997 + 0 + 0 + 0 # BOUND : makespan 1117 1131 MODIFY_CNF 1124 BEGIN : [Sun Jun 18 16:49:55 2006] MODIFY_CNF 1124 END : 64120062 bytes (0 seconds) [Sun Jun 18 16:49:55 2006] MODIFY_CNF 1124 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1124 BEGIN : [Sun Jun 18 16:49:55 2006] CMD : minisat /tmp/csp2sat10312.cnf /tmp/csp2sat10312.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1200903 3418450 | 400301 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (0 /sec) decisions : 10 (2 /sec) propagations : 126785 (30773 /sec) conflict literals : 1 (0.00 % deleted) Memory used : 114.21 MB CPU time : 4.12 s UNSATISFIABLE VERIFY_CNF 1124 END : (4 seconds) [Sun Jun 18 16:49:59 2006] VERIFY_CNF 1124 CPU : 4.49 = 0 + 0 + 4.12 + 0.37 # RESULT : makespan 1124 UNSATISFIABLE # BOUND : makespan 1125 1131 MODIFY_CNF 1128 BEGIN : [Sun Jun 18 16:49:59 2006] MODIFY_CNF 1128 END : 64120062 bytes (0 seconds) [Sun Jun 18 16:49:59 2006] MODIFY_CNF 1128 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1128 BEGIN : [Sun Jun 18 16:49:59 2006] CMD : minisat /tmp/csp2sat10312.cnf /tmp/csp2sat10312.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1204487 3429202 | 401495 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (0 /sec) decisions : 10 (2 /sec) propagations : 126525 (30785 /sec) conflict literals : 1 (0.00 % deleted) Memory used : 114.21 MB CPU time : 4.11 s UNSATISFIABLE VERIFY_CNF 1128 END : (5 seconds) [Sun Jun 18 16:50:04 2006] VERIFY_CNF 1128 CPU : 4.52000000000001 = 0 + 0.00999999999999995 + 4.11000000000001 + 0.4 # RESULT : makespan 1128 UNSATISFIABLE # BOUND : makespan 1129 1131 MODIFY_CNF 1130 BEGIN : [Sun Jun 18 16:50:04 2006] MODIFY_CNF 1130 END : 64120062 bytes (0 seconds) [Sun Jun 18 16:50:04 2006] MODIFY_CNF 1130 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1130 BEGIN : [Sun Jun 18 16:50:04 2006] CMD : minisat /tmp/csp2sat10312.cnf /tmp/csp2sat10312.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1206279 3434578 | 402093 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 5 (1 /sec) decisions : 149 (34 /sec) propagations : 239136 (54597 /sec) conflict literals : 17 (0.00 % deleted) Memory used : 115.15 MB CPU time : 4.38 s SATISFIABLE VERIFY_CNF 1130 END : (5 seconds) [Sun Jun 18 16:50:09 2006] VERIFY_CNF 1130 CPU : 4.79 = 0 + 0 + 4.47 + 0.32 # RESULT : makespan 1130 SATISFIABLE SHOW_RESULT 1130 BEGIN : [Sun Jun 18 16:50:09 2006] # ASSIGN : makespan 1130 # ASSIGN : s_0_0 5 # ASSIGN : s_0_1 334 # ASSIGN : s_0_2 635 # ASSIGN : s_0_3 6 # ASSIGN : s_0_4 7 # ASSIGN : s_0_5 1122 # ASSIGN : s_0_6 185 # ASSIGN : s_0_7 1128 # ASSIGN : s_1_0 10 # ASSIGN : s_1_1 0 # ASSIGN : s_1_2 14 # ASSIGN : s_1_3 990 # ASSIGN : s_1_4 711 # ASSIGN : s_1_5 112 # ASSIGN : s_1_6 111 # ASSIGN : s_1_7 962 # ASSIGN : s_2_0 0 # ASSIGN : s_2_1 1122 # ASSIGN : s_2_2 186 # ASSIGN : s_2_3 13 # ASSIGN : s_2_4 163 # ASSIGN : s_2_5 23 # ASSIGN : s_2_6 612 # ASSIGN : s_2_7 1129 # ASSIGN : s_3_0 139 # ASSIGN : s_3_1 1 # ASSIGN : s_3_2 125 # ASSIGN : s_3_3 14 # ASSIGN : s_3_4 844 # ASSIGN : s_3_5 110 # ASSIGN : s_3_6 78 # ASSIGN : s_3_7 267 # ASSIGN : s_4_0 258 # ASSIGN : s_4_1 1126 # ASSIGN : s_4_2 1073 # ASSIGN : s_4_3 1127 # ASSIGN : s_4_4 1128 # ASSIGN : s_4_5 770 # ASSIGN : s_4_6 1129 # ASSIGN : s_4_7 0 # ASSIGN : s_5_0 1 # ASSIGN : s_5_1 582 # ASSIGN : s_5_2 581 # ASSIGN : s_5_3 19 # ASSIGN : s_5_4 164 # ASSIGN : s_5_5 21 # ASSIGN : s_5_6 132 # ASSIGN : s_5_7 995 # ASSIGN : s_6_0 640 # ASSIGN : s_6_1 2 # ASSIGN : s_6_2 631 # ASSIGN : s_6_3 42 # ASSIGN : s_6_4 632 # ASSIGN : s_6_5 22 # ASSIGN : s_6_6 339 # ASSIGN : s_6_7 266 # ASSIGN : s_7_0 2 # ASSIGN : s_7_1 4 # ASSIGN : s_7_2 1129 # ASSIGN : s_7_3 361 # ASSIGN : s_7_4 1094 # ASSIGN : s_7_5 1 # ASSIGN : s_7_6 337 # ASSIGN : s_7_7 994 SHOW_RESULT 1130 END : 1130 (0 seconds) [Sun Jun 18 16:50:09 2006] SHOW_RESULT 1130 CPU : 0.410000000000011 = 0.410000000000011 + 0 + 0 + 0 # BOUND : makespan 1129 1130 MODIFY_CNF 1129 BEGIN : [Sun Jun 18 16:50:09 2006] MODIFY_CNF 1129 END : 64120062 bytes (0 seconds) [Sun Jun 18 16:50:09 2006] MODIFY_CNF 1129 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1129 BEGIN : [Sun Jun 18 16:50:09 2006] CMD : minisat /tmp/csp2sat10312.cnf /tmp/csp2sat10312.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1205383 3431890 | 401794 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (0 /sec) decisions : 10 (2 /sec) propagations : 126460 (30110 /sec) conflict literals : 1 (0.00 % deleted) Memory used : 114.21 MB CPU time : 4.2 s UNSATISFIABLE VERIFY_CNF 1129 END : (4 seconds) [Sun Jun 18 16:50:13 2006] VERIFY_CNF 1129 CPU : 4.52 = 0 + 0.01 + 4.2 + 0.31 # RESULT : makespan 1129 UNSATISFIABLE # BOUND : makespan 1130 1130 MAIN END : (160 seconds) [Sun Jun 18 16:50:13 2006] MAIN CPU : 160.32 = 108.98 + 0.48 + 46.94 + 3.92