# TIMEOUT 18000 MAIN BEGIN : [Sun Jun 18 18:35:53 2006] READ BEGIN : csp/gp10-03.csp [Sun Jun 18 18:35:53 2006] READ END : csp/gp10-03.csp (2 seconds) [Sun Jun 18 18:35:55 2006] READ CPU : 1.87 = 1.85 + 0.02 + 0 + 0 # BOUND : makespan 1000 3715 GENERATE_CNF 3715 BEGIN : [Sun Jun 18 18:35:55 2006] GENERATE_CNF 3715 END : 376317 variables 7157718 clauses 171321061 bytes (278 seconds) [Sun Jun 18 18:40:33 2006] GENERATE_CNF 3715 CPU : 276.38 = 275.18 + 1.2 + 0 + 0 MODIFY_CNF 2357 BEGIN : [Sun Jun 18 18:40:33 2006] MODIFY_CNF 2357 END : 171321068 bytes (0 seconds) [Sun Jun 18 18:40:33 2006] MODIFY_CNF 2357 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 2357 BEGIN : [Sun Jun 18 18:40:33 2006] CMD : minisat /tmp/csp2sat12297.cnf /tmp/csp2sat12297.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 4710813 13759930 | 1570271 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 12 (1 /sec) decisions : 692 (58 /sec) propagations : 510149 (42406 /sec) conflict literals : 267 (2.20 % deleted) Memory used : 294.60 MB CPU time : 12.03 s SATISFIABLE VERIFY_CNF 2357 END : (13 seconds) [Sun Jun 18 18:40:46 2006] VERIFY_CNF 2357 CPU : 13.17 = 0 + 0 + 12.22 + 0.95 # RESULT : makespan 2357 SATISFIABLE SHOW_RESULT 2357 BEGIN : [Sun Jun 18 18:40:46 2006] # ASSIGN : makespan 2357 # ASSIGN : s_0_0 56 # ASSIGN : s_0_1 1 # ASSIGN : s_0_2 116 # ASSIGN : s_0_3 88 # ASSIGN : s_0_4 4 # ASSIGN : s_0_5 44 # ASSIGN : s_0_6 97 # ASSIGN : s_0_7 1083 # ASSIGN : s_0_8 280 # ASSIGN : s_0_9 528 # ASSIGN : s_1_0 373 # ASSIGN : s_1_1 48 # ASSIGN : s_1_2 254 # ASSIGN : s_1_3 585 # ASSIGN : s_1_4 52 # ASSIGN : s_1_5 55 # ASSIGN : s_1_6 146 # ASSIGN : s_1_7 1617 # ASSIGN : s_1_8 371 # ASSIGN : s_1_9 651 # ASSIGN : s_2_0 534 # ASSIGN : s_2_1 426 # ASSIGN : s_2_2 427 # ASSIGN : s_2_3 616 # ASSIGN : s_2_4 169 # ASSIGN : s_2_5 183 # ASSIGN : s_2_6 246 # ASSIGN : s_2_7 1618 # ASSIGN : s_2_8 449 # ASSIGN : s_2_9 1141 # ASSIGN : s_3_0 862 # ASSIGN : s_3_1 427 # ASSIGN : s_3_2 428 # ASSIGN : s_3_3 1141 # ASSIGN : s_3_4 268 # ASSIGN : s_3_5 269 # ASSIGN : s_3_6 709 # ASSIGN : s_3_7 1666 # ASSIGN : s_3_8 914 # ASSIGN : s_3_9 1142 # ASSIGN : s_4_0 1049 # ASSIGN : s_4_1 490 # ASSIGN : s_4_2 709 # ASSIGN : s_4_3 1259 # ASSIGN : s_4_4 392 # ASSIGN : s_4_5 509 # ASSIGN : s_4_6 710 # ASSIGN : s_4_7 1810 # ASSIGN : s_4_8 1277 # ASSIGN : s_4_9 1276 # ASSIGN : s_5_0 1363 # ASSIGN : s_5_1 530 # ASSIGN : s_5_2 738 # ASSIGN : s_5_3 1465 # ASSIGN : s_5_4 741 # ASSIGN : s_5_5 663 # ASSIGN : s_5_6 1466 # ASSIGN : s_5_7 1877 # ASSIGN : s_5_8 1371 # ASSIGN : s_5_9 1332 # ASSIGN : s_6_0 1486 # ASSIGN : s_6_1 532 # ASSIGN : s_6_2 1182 # ASSIGN : s_6_3 1517 # ASSIGN : s_6_4 1519 # ASSIGN : s_6_5 667 # ASSIGN : s_6_6 1761 # ASSIGN : s_6_7 1878 # ASSIGN : s_6_8 1522 # ASSIGN : s_6_9 1333 # ASSIGN : s_7_0 1704 # ASSIGN : s_7_1 695 # ASSIGN : s_7_2 1246 # ASSIGN : s_7_3 1581 # ASSIGN : s_7_4 1767 # ASSIGN : s_7_5 1768 # ASSIGN : s_7_6 1769 # ASSIGN : s_7_7 1880 # ASSIGN : s_7_8 1825 # ASSIGN : s_7_9 1334 # ASSIGN : s_8_0 1993 # ASSIGN : s_8_1 1210 # ASSIGN : s_8_2 1247 # ASSIGN : s_8_3 1640 # ASSIGN : s_8_4 1768 # ASSIGN : s_8_5 1769 # ASSIGN : s_8_6 1770 # ASSIGN : s_8_7 1991 # ASSIGN : s_8_8 1826 # ASSIGN : s_8_9 2355 # ASSIGN : s_9_0 2336 # ASSIGN : s_9_1 1357 # ASSIGN : s_9_2 1640 # ASSIGN : s_9_3 1641 # ASSIGN : s_9_4 1995 # ASSIGN : s_9_5 2243 # ASSIGN : s_9_6 2245 # ASSIGN : s_9_7 2246 # ASSIGN : s_9_8 2354 # ASSIGN : s_9_9 2356 SHOW_RESULT 2357 END : 2357 (1 seconds) [Sun Jun 18 18:40:47 2006] SHOW_RESULT 2357 CPU : 1.26000000000002 = 1.17000000000002 + 0.0900000000000001 + 0 + 0 # BOUND : makespan 1000 2357 MODIFY_CNF 1678 BEGIN : [Sun Jun 18 18:40:47 2006] MODIFY_CNF 1678 END : 171321067 bytes (0 seconds) [Sun Jun 18 18:40:47 2006] MODIFY_CNF 1678 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1678 BEGIN : [Sun Jun 18 18:40:47 2006] CMD : minisat /tmp/csp2sat12297.cnf /tmp/csp2sat12297.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 3488613 10093330 | 1162871 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 27 (2 /sec) decisions : 672 (45 /sec) propagations : 859751 (57240 /sec) conflict literals : 575 (8.29 % deleted) Memory used : 294.60 MB CPU time : 15.02 s SATISFIABLE VERIFY_CNF 1678 END : (16 seconds) [Sun Jun 18 18:41:03 2006] VERIFY_CNF 1678 CPU : 16.02 = 0 + 0.01 + 15.21 + 0.8 # RESULT : makespan 1678 SATISFIABLE SHOW_RESULT 1678 BEGIN : [Sun Jun 18 18:41:03 2006] # ASSIGN : makespan 1678 # ASSIGN : s_0_0 1317 # ASSIGN : s_0_1 0 # ASSIGN : s_0_2 1473 # ASSIGN : s_0_3 1618 # ASSIGN : s_0_4 1635 # ASSIGN : s_0_5 3 # ASSIGN : s_0_6 105 # ASSIGN : s_0_7 247 # ASSIGN : s_0_8 14 # ASSIGN : s_0_9 124 # ASSIGN : s_1_0 1483 # ASSIGN : s_1_1 21 # ASSIGN : s_1_2 1356 # ASSIGN : s_1_3 1644 # ASSIGN : s_1_4 1675 # ASSIGN : s_1_5 25 # ASSIGN : s_1_6 148 # ASSIGN : s_1_7 781 # ASSIGN : s_1_8 116 # ASSIGN : s_1_9 248 # ASSIGN : s_2_0 1401 # ASSIGN : s_2_1 41 # ASSIGN : s_2_2 1355 # ASSIGN : s_2_3 830 # ASSIGN : s_2_4 48 # ASSIGN : s_2_5 280 # ASSIGN : s_2_6 343 # ASSIGN : s_2_7 782 # ASSIGN : s_2_8 118 # ASSIGN : s_2_9 738 # ASSIGN : s_3_0 1349 # ASSIGN : s_3_1 42 # ASSIGN : s_3_2 1052 # ASSIGN : s_3_3 61 # ASSIGN : s_3_4 62 # ASSIGN : s_3_5 581 # ASSIGN : s_3_6 523 # ASSIGN : s_3_7 873 # ASSIGN : s_3_8 203 # ASSIGN : s_3_9 739 # ASSIGN : s_4_0 1090 # ASSIGN : s_4_1 43 # ASSIGN : s_4_2 62 # ASSIGN : s_4_3 1627 # ASSIGN : s_4_4 63 # ASSIGN : s_4_5 863 # ASSIGN : s_4_6 524 # ASSIGN : s_4_7 1017 # ASSIGN : s_4_8 430 # ASSIGN : s_4_9 1085 # ASSIGN : s_5_0 1300 # ASSIGN : s_5_1 141 # ASSIGN : s_5_2 1675 # ASSIGN : s_5_3 160 # ASSIGN : s_5_4 161 # ASSIGN : s_5_5 1080 # ASSIGN : s_5_6 1308 # ASSIGN : s_5_7 1084 # ASSIGN : s_5_8 752 # ASSIGN : s_5_9 1086 # ASSIGN : s_6_0 812 # ASSIGN : s_6_1 677 # ASSIGN : s_6_2 1611 # ASSIGN : s_6_3 158 # ASSIGN : s_6_4 843 # ASSIGN : s_6_5 1088 # ASSIGN : s_6_6 1603 # ASSIGN : s_6_7 1085 # ASSIGN : s_6_8 846 # ASSIGN : s_6_9 1087 # ASSIGN : s_7_0 969 # ASSIGN : s_7_1 143 # ASSIGN : s_7_2 658 # ASSIGN : s_7_3 1555 # ASSIGN : s_7_4 1195 # ASSIGN : s_7_5 1670 # ASSIGN : s_7_6 1614 # ASSIGN : s_7_7 1196 # ASSIGN : s_7_8 1307 # ASSIGN : s_7_9 1308 # ASSIGN : s_8_0 316 # ASSIGN : s_8_1 1411 # ASSIGN : s_8_2 659 # ASSIGN : s_8_3 1677 # ASSIGN : s_8_4 1333 # ASSIGN : s_8_5 1671 # ASSIGN : s_8_6 1615 # ASSIGN : s_8_7 1448 # ASSIGN : s_8_8 1450 # ASSIGN : s_8_9 1676 # ASSIGN : s_9_0 1032 # ASSIGN : s_9_1 1050 # ASSIGN : s_9_2 1333 # ASSIGN : s_9_3 476 # ASSIGN : s_9_4 1334 # ASSIGN : s_9_5 1672 # ASSIGN : s_9_6 1674 # ASSIGN : s_9_7 1582 # ASSIGN : s_9_8 1675 # ASSIGN : s_9_9 1677 SHOW_RESULT 1678 END : 1678 (2 seconds) [Sun Jun 18 18:41:05 2006] SHOW_RESULT 1678 CPU : 1.91999999999998 = 1.89999999999998 + 0.02 + 0 + 0 # BOUND : makespan 1000 1678 MODIFY_CNF 1339 BEGIN : [Sun Jun 18 18:41:05 2006] MODIFY_CNF 1339 END : 171321067 bytes (0 seconds) [Sun Jun 18 18:41:05 2006] MODIFY_CNF 1339 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1339 BEGIN : [Sun Jun 18 18:41:05 2006] CMD : minisat /tmp/csp2sat12297.cnf /tmp/csp2sat12297.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 2878413 8262730 | 959471 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 4 (0 /sec) decisions : 509 (34 /sec) propagations : 431978 (28608 /sec) conflict literals : 30 (3.23 % deleted) Memory used : 294.60 MB CPU time : 15.1 s SATISFIABLE VERIFY_CNF 1339 END : (16 seconds) [Sun Jun 18 18:41:21 2006] VERIFY_CNF 1339 CPU : 16.38 = 0 + 0.01 + 15.29 + 1.08 # RESULT : makespan 1339 SATISFIABLE SHOW_RESULT 1339 BEGIN : [Sun Jun 18 18:41:21 2006] # ASSIGN : makespan 1339 # ASSIGN : s_0_0 948 # ASSIGN : s_0_1 0 # ASSIGN : s_0_2 1079 # ASSIGN : s_0_3 115 # ASSIGN : s_0_4 980 # ASSIGN : s_0_5 7 # ASSIGN : s_0_6 18 # ASSIGN : s_0_7 352 # ASSIGN : s_0_8 124 # ASSIGN : s_0_9 229 # ASSIGN : s_1_0 981 # ASSIGN : s_1_1 3 # ASSIGN : s_1_2 1217 # ASSIGN : s_1_3 184 # ASSIGN : s_1_4 8 # ASSIGN : s_1_5 68 # ASSIGN : s_1_6 217 # ASSIGN : s_1_7 980 # ASSIGN : s_1_8 215 # ASSIGN : s_1_9 357 # ASSIGN : s_2_0 1142 # ASSIGN : s_2_1 7 # ASSIGN : s_2_2 8 # ASSIGN : s_2_3 302 # ASSIGN : s_2_4 11 # ASSIGN : s_2_5 909 # ASSIGN : s_2_6 37 # ASSIGN : s_2_7 1224 # ASSIGN : s_2_8 217 # ASSIGN : s_2_9 847 # ASSIGN : s_3_0 28 # ASSIGN : s_3_1 9 # ASSIGN : s_3_2 546 # ASSIGN : s_3_3 827 # ASSIGN : s_3_4 25 # ASSIGN : s_3_5 159 # ASSIGN : s_3_6 317 # ASSIGN : s_3_7 1080 # ASSIGN : s_3_8 319 # ASSIGN : s_3_9 848 # ASSIGN : s_4_0 80 # ASSIGN : s_4_1 10 # ASSIGN : s_4_2 9 # ASSIGN : s_4_3 828 # ASSIGN : s_4_4 1020 # ASSIGN : s_4_5 1118 # ASSIGN : s_4_6 318 # ASSIGN : s_4_7 1272 # ASSIGN : s_4_8 657 # ASSIGN : s_4_9 982 # ASSIGN : s_5_0 18 # ASSIGN : s_5_1 29 # ASSIGN : s_5_2 26 # ASSIGN : s_5_3 845 # ASSIGN : s_5_4 31 # ASSIGN : s_5_5 972 # ASSIGN : s_5_6 984 # ASSIGN : s_5_7 982 # ASSIGN : s_5_8 751 # ASSIGN : s_5_9 983 # ASSIGN : s_6_0 290 # ASSIGN : s_6_1 1204 # ASSIGN : s_6_2 69 # ASSIGN : s_6_3 846 # ASSIGN : s_6_4 26 # ASSIGN : s_6_5 323 # ASSIGN : s_6_6 838 # ASSIGN : s_6_7 321 # ASSIGN : s_6_8 848 # ASSIGN : s_6_9 1087 # ASSIGN : s_7_0 339 # ASSIGN : s_7_1 402 # ASSIGN : s_7_2 133 # ASSIGN : s_7_3 917 # ASSIGN : s_7_4 29 # ASSIGN : s_7_5 976 # ASSIGN : s_7_6 983 # ASSIGN : s_7_7 210 # ASSIGN : s_7_8 1087 # ASSIGN : s_7_9 1088 # ASSIGN : s_8_0 527 # ASSIGN : s_8_1 82 # ASSIGN : s_8_2 134 # ASSIGN : s_8_3 976 # ASSIGN : s_8_4 30 # ASSIGN : s_8_5 977 # ASSIGN : s_8_6 1279 # ASSIGN : s_8_7 886 # ASSIGN : s_8_8 1114 # ASSIGN : s_8_9 1335 # ASSIGN : s_9_0 870 # ASSIGN : s_9_1 119 # ASSIGN : s_9_2 1334 # ASSIGN : s_9_3 980 # ASSIGN : s_9_4 622 # ASSIGN : s_9_5 978 # ASSIGN : s_9_6 1335 # ASSIGN : s_9_7 888 # ASSIGN : s_9_8 1337 # ASSIGN : s_9_9 1336 SHOW_RESULT 1339 END : 1339 (2 seconds) [Sun Jun 18 18:41:23 2006] SHOW_RESULT 1339 CPU : 1.82999999999999 = 1.81999999999999 + 0.01 + 0 + 0 # BOUND : makespan 1000 1339 MODIFY_CNF 1169 BEGIN : [Sun Jun 18 18:41:23 2006] MODIFY_CNF 1169 END : 171321067 bytes (0 seconds) [Sun Jun 18 18:41:23 2006] MODIFY_CNF 1169 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1169 BEGIN : [Sun Jun 18 18:41:23 2006] CMD : minisat /tmp/csp2sat12297.cnf /tmp/csp2sat12297.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 2572413 7344730 | 857471 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 11 (1 /sec) decisions : 253 (15 /sec) propagations : 452475 (26758 /sec) conflict literals : 107 (7.76 % deleted) Memory used : 294.60 MB CPU time : 16.91 s SATISFIABLE VERIFY_CNF 1169 END : (18 seconds) [Sun Jun 18 18:41:41 2006] VERIFY_CNF 1169 CPU : 18.02 = 0 + 0 + 17.11 + 0.91 # RESULT : makespan 1169 SATISFIABLE SHOW_RESULT 1169 BEGIN : [Sun Jun 18 18:41:41 2006] # ASSIGN : makespan 1169 # ASSIGN : s_0_0 491 # ASSIGN : s_0_1 1126 # ASSIGN : s_0_2 349 # ASSIGN : s_0_3 125 # ASSIGN : s_0_4 1129 # ASSIGN : s_0_5 225 # ASSIGN : s_0_6 1107 # ASSIGN : s_0_7 523 # ASSIGN : s_0_8 134 # ASSIGN : s_0_9 0 # ASSIGN : s_1_0 987 # ASSIGN : s_1_1 892 # ASSIGN : s_1_2 3 # ASSIGN : s_1_3 613 # ASSIGN : s_1_4 648 # ASSIGN : s_1_5 896 # ASSIGN : s_1_6 652 # ASSIGN : s_1_7 120 # ASSIGN : s_1_8 121 # ASSIGN : s_1_9 123 # ASSIGN : s_2_0 62 # ASSIGN : s_2_1 38 # ASSIGN : s_2_2 161 # ASSIGN : s_2_3 644 # ASSIGN : s_2_4 630 # ASSIGN : s_2_5 162 # ASSIGN : s_2_6 434 # ASSIGN : s_2_7 386 # ASSIGN : s_2_8 245 # ASSIGN : s_2_9 614 # ASSIGN : s_3_0 563 # ASSIGN : s_3_1 0 # ASSIGN : s_3_2 884 # ASSIGN : s_3_3 2 # ASSIGN : s_3_4 1 # ASSIGN : s_3_5 4 # ASSIGN : s_3_6 3 # ASSIGN : s_3_7 186 # ASSIGN : s_3_8 330 # ASSIGN : s_3_9 615 # ASSIGN : s_4_0 762 # ASSIGN : s_4_1 972 # ASSIGN : s_4_2 2 # ASSIGN : s_4_3 537 # ASSIGN : s_4_4 651 # ASSIGN : s_4_5 1015 # ASSIGN : s_4_6 95 # ASSIGN : s_4_7 456 # ASSIGN : s_4_8 557 # ASSIGN : s_4_9 749 # ASSIGN : s_5_0 648 # ASSIGN : s_5_1 596 # ASSIGN : s_5_2 1165 # ASSIGN : s_5_3 3 # ASSIGN : s_5_4 5 # ASSIGN : s_5_5 808 # ASSIGN : s_5_6 812 # ASSIGN : s_5_7 4 # ASSIGN : s_5_8 656 # ASSIGN : s_5_9 750 # ASSIGN : s_6_0 31 # ASSIGN : s_6_1 991 # ASSIGN : s_6_2 172 # ASSIGN : s_6_3 0 # ASSIGN : s_6_4 2 # ASSIGN : s_6_5 236 # ASSIGN : s_6_6 21 # ASSIGN : s_6_7 170 # ASSIGN : s_6_8 752 # ASSIGN : s_6_9 751 # ASSIGN : s_7_0 687 # ASSIGN : s_7_1 39 # ASSIGN : s_7_2 1168 # ASSIGN : s_7_3 554 # ASSIGN : s_7_4 750 # ASSIGN : s_7_5 751 # ASSIGN : s_7_6 752 # ASSIGN : s_7_7 1057 # ASSIGN : s_7_8 1000 # ASSIGN : s_7_9 753 # ASSIGN : s_8_0 144 # ASSIGN : s_8_1 1 # ASSIGN : s_8_2 487 # ASSIGN : s_8_3 38 # ASSIGN : s_8_4 880 # ASSIGN : s_8_5 0 # ASSIGN : s_8_6 39 # ASSIGN : s_8_7 142 # ASSIGN : s_8_8 1001 # ASSIGN : s_8_9 1167 # ASSIGN : s_9_0 1148 # ASSIGN : s_9_1 598 # ASSIGN : s_9_2 160 # ASSIGN : s_9_3 183 # ASSIGN : s_9_4 881 # ASSIGN : s_9_5 2 # ASSIGN : s_9_6 29 # ASSIGN : s_9_7 30 # ASSIGN : s_9_8 1166 # ASSIGN : s_9_9 1168 SHOW_RESULT 1169 END : 1169 (2 seconds) [Sun Jun 18 18:41:43 2006] SHOW_RESULT 1169 CPU : 1.81000000000001 = 1.80000000000001 + 0.00999999999999979 + 0 + 0 # BOUND : makespan 1000 1169 MODIFY_CNF 1084 BEGIN : [Sun Jun 18 18:41:43 2006] MODIFY_CNF 1084 END : 171321066 bytes (0 seconds) [Sun Jun 18 18:41:43 2006] MODIFY_CNF 1084 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1084 BEGIN : [Sun Jun 18 18:41:43 2006] CMD : minisat /tmp/csp2sat12297.cnf /tmp/csp2sat12297.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 2419413 6885730 | 806471 0 0 nan | 0.000 % | | 100 | 2419415 6885730 | 887118 98 1580 16.1 | 73.351 % | | 251 | 2419416 6885730 | 975829 248 4343 17.5 | 73.351 % | ============================================================================== restarts : 3 conflicts : 417 (19 /sec) decisions : 750 (35 /sec) propagations : 4027575 (188029 /sec) conflict literals : 7147 (36.56 % deleted) Memory used : 294.62 MB CPU time : 21.42 s SATISFIABLE VERIFY_CNF 1084 END : (23 seconds) [Sun Jun 18 18:42:06 2006] VERIFY_CNF 1084 CPU : 22.54 = 0 + 0 + 21.59 + 0.95 # RESULT : makespan 1084 SATISFIABLE SHOW_RESULT 1084 BEGIN : [Sun Jun 18 18:42:06 2006] # ASSIGN : makespan 1084 # ASSIGN : s_0_0 54 # ASSIGN : s_0_1 114 # ASSIGN : s_0_2 117 # ASSIGN : s_0_3 105 # ASSIGN : s_0_4 296 # ASSIGN : s_0_5 269 # ASSIGN : s_0_6 1 # ASSIGN : s_0_7 336 # ASSIGN : s_0_8 870 # ASSIGN : s_0_9 961 # ASSIGN : s_1_0 119 # ASSIGN : s_1_1 1079 # ASSIGN : s_1_2 0 # ASSIGN : s_1_3 1033 # ASSIGN : s_1_4 1065 # ASSIGN : s_1_5 280 # ASSIGN : s_1_6 371 # ASSIGN : s_1_7 1083 # ASSIGN : s_1_8 976 # ASSIGN : s_1_9 471 # ASSIGN : s_2_0 650 # ASSIGN : s_2_1 1083 # ASSIGN : s_2_2 784 # ASSIGN : s_2_3 114 # ASSIGN : s_2_4 1069 # ASSIGN : s_2_5 51 # ASSIGN : s_2_6 889 # ASSIGN : s_2_7 3 # ASSIGN : s_2_8 785 # ASSIGN : s_2_9 2 # ASSIGN : s_3_0 2 # ASSIGN : s_3_1 0 # ASSIGN : s_3_2 787 # ASSIGN : s_3_3 1 # ASSIGN : s_3_4 1068 # ASSIGN : s_3_5 398 # ASSIGN : s_3_6 1082 # ASSIGN : s_3_7 192 # ASSIGN : s_3_8 558 # ASSIGN : s_3_9 58 # ASSIGN : s_4_0 291 # ASSIGN : s_4_1 1 # ASSIGN : s_4_2 1082 # ASSIGN : s_4_3 1064 # ASSIGN : s_4_4 966 # ASSIGN : s_4_5 115 # ASSIGN : s_4_6 550 # ASSIGN : s_4_7 899 # ASSIGN : s_4_8 21 # ASSIGN : s_4_9 20 # ASSIGN : s_5_0 1075 # ASSIGN : s_5_1 74 # ASSIGN : s_5_2 1072 # ASSIGN : s_5_3 1083 # ASSIGN : s_5_4 375 # ASSIGN : s_5_5 371 # ASSIGN : s_5_6 76 # ASSIGN : s_5_7 0 # ASSIGN : s_5_8 978 # ASSIGN : s_5_9 18 # ASSIGN : s_6_0 86 # ASSIGN : s_6_1 117 # ASSIGN : s_6_2 255 # ASSIGN : s_6_3 1081 # ASSIGN : s_6_4 252 # ASSIGN : s_6_5 558 # ASSIGN : s_6_6 1073 # ASSIGN : s_6_7 79 # ASSIGN : s_6_8 319 # ASSIGN : s_6_9 17 # ASSIGN : s_7_0 501 # ASSIGN : s_7_1 564 # ASSIGN : s_7_2 1081 # ASSIGN : s_7_3 22 # ASSIGN : s_7_4 3 # ASSIGN : s_7_5 1082 # ASSIGN : s_7_6 1083 # ASSIGN : s_7_7 81 # ASSIGN : s_7_8 20 # ASSIGN : s_7_9 224 # ASSIGN : s_8_0 732 # ASSIGN : s_8_1 77 # ASSIGN : s_8_2 339 # ASSIGN : s_8_3 18 # ASSIGN : s_8_4 338 # ASSIGN : s_8_5 1083 # ASSIGN : s_8_6 20 # ASSIGN : s_8_7 1 # ASSIGN : s_8_8 154 # ASSIGN : s_8_9 19 # ASSIGN : s_9_0 621 # ASSIGN : s_9_1 266 # ASSIGN : s_9_2 1083 # ASSIGN : s_9_3 639 # ASSIGN : s_9_4 4 # ASSIGN : s_9_5 556 # ASSIGN : s_9_6 549 # ASSIGN : s_9_7 993 # ASSIGN : s_9_8 1 # ASSIGN : s_9_9 3 SHOW_RESULT 1084 END : 1084 (2 seconds) [Sun Jun 18 18:42:08 2006] SHOW_RESULT 1084 CPU : 1.78999999999997 = 1.77999999999997 + 0.01 + 0 + 0 # BOUND : makespan 1000 1084 MODIFY_CNF 1042 BEGIN : [Sun Jun 18 18:42:08 2006] MODIFY_CNF 1042 END : 171321066 bytes (0 seconds) [Sun Jun 18 18:42:08 2006] MODIFY_CNF 1042 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1042 BEGIN : [Sun Jun 18 18:42:08 2006] CMD : minisat /tmp/csp2sat12297.cnf /tmp/csp2sat12297.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 2343813 6658930 | 781271 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (0 /sec) decisions : 31 (2 /sec) propagations : 286716 (16945 /sec) conflict literals : 1 (0.00 % deleted) Memory used : 292.82 MB CPU time : 16.92 s UNSATISFIABLE VERIFY_CNF 1042 END : (17 seconds) [Sun Jun 18 18:42:25 2006] VERIFY_CNF 1042 CPU : 17.79 = 0 + 0.01 + 16.92 + 0.859999999999999 # RESULT : makespan 1042 UNSATISFIABLE # BOUND : makespan 1043 1084 MODIFY_CNF 1063 BEGIN : [Sun Jun 18 18:42:25 2006] MODIFY_CNF 1063 END : 171321066 bytes (0 seconds) [Sun Jun 18 18:42:25 2006] MODIFY_CNF 1063 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1063 BEGIN : [Sun Jun 18 18:42:25 2006] CMD : minisat /tmp/csp2sat12297.cnf /tmp/csp2sat12297.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 2381613 6772330 | 793871 0 0 nan | 0.000 % | | 102 | 2381615 6772330 | 873258 100 1429 14.3 | 73.915 % | | 252 | 2381619 6772330 | 960583 245 2768 11.3 | 74.116 % | ============================================================================== restarts : 3 conflicts : 401 (19 /sec) decisions : 551 (26 /sec) propagations : 4190219 (197652 /sec) conflict literals : 4031 (37.29 % deleted) Memory used : 292.99 MB CPU time : 21.2 s UNSATISFIABLE VERIFY_CNF 1063 END : (22 seconds) [Sun Jun 18 18:42:47 2006] VERIFY_CNF 1063 CPU : 22.05 = 0 + 0 + 21.2 + 0.850000000000001 # RESULT : makespan 1063 UNSATISFIABLE # BOUND : makespan 1064 1084 MODIFY_CNF 1074 BEGIN : [Sun Jun 18 18:42:47 2006] MODIFY_CNF 1074 END : 171321066 bytes (0 seconds) [Sun Jun 18 18:42:47 2006] MODIFY_CNF 1074 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1074 BEGIN : [Sun Jun 18 18:42:47 2006] CMD : minisat /tmp/csp2sat12297.cnf /tmp/csp2sat12297.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 2401413 6831730 | 800471 0 0 nan | 0.000 % | | 101 | 2401414 6831730 | 880518 100 1530 15.3 | 73.620 % | | 251 | 2401415 6831730 | 968569 249 3059 12.3 | 73.620 % | | 477 | 2401425 6831730 | 1065426 464 5902 12.7 | 73.766 % | ============================================================================== restarts : 4 conflicts : 523 (24 /sec) decisions : 700 (32 /sec) propagations : 4605556 (211555 /sec) conflict literals : 6205 (40.41 % deleted) Memory used : 293.01 MB CPU time : 21.77 s UNSATISFIABLE VERIFY_CNF 1074 END : (23 seconds) [Sun Jun 18 18:43:10 2006] VERIFY_CNF 1074 CPU : 22.77 = 0 + 0 + 21.77 + 1 # RESULT : makespan 1074 UNSATISFIABLE # BOUND : makespan 1075 1084 MODIFY_CNF 1079 BEGIN : [Sun Jun 18 18:43:10 2006] MODIFY_CNF 1079 END : 171321066 bytes (0 seconds) [Sun Jun 18 18:43:10 2006] MODIFY_CNF 1079 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1079 BEGIN : [Sun Jun 18 18:43:10 2006] CMD : minisat /tmp/csp2sat12297.cnf /tmp/csp2sat12297.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 2410413 6858730 | 803471 0 0 nan | 0.000 % | | 101 | 2410414 6858730 | 883818 100 1507 15.1 | 73.485 % | | 252 | 2410418 6858730 | 972199 247 3285 13.3 | 73.485 % | | 478 | 2410419 6858730 | 1069419 472 7044 14.9 | 73.485 % | ============================================================================== restarts : 4 conflicts : 657 (27 /sec) decisions : 889 (36 /sec) propagations : 5849035 (238541 /sec) conflict literals : 9308 (39.52 % deleted) Memory used : 293.02 MB CPU time : 24.52 s UNSATISFIABLE VERIFY_CNF 1079 END : (26 seconds) [Sun Jun 18 18:43:36 2006] VERIFY_CNF 1079 CPU : 25.46 = 0 + 0.01 + 24.52 + 0.93 # RESULT : makespan 1079 UNSATISFIABLE # BOUND : makespan 1080 1084 MODIFY_CNF 1082 BEGIN : [Sun Jun 18 18:43:36 2006] MODIFY_CNF 1082 END : 171321066 bytes (0 seconds) [Sun Jun 18 18:43:36 2006] MODIFY_CNF 1082 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1082 BEGIN : [Sun Jun 18 18:43:36 2006] CMD : minisat /tmp/csp2sat12297.cnf /tmp/csp2sat12297.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 2415813 6874930 | 805271 0 0 nan | 0.000 % | | 101 | 2415814 6874930 | 885798 100 1635 16.4 | 73.405 % | | 251 | 2415815 6874930 | 974377 249 3893 15.6 | 73.405 % | ============================================================================== restarts : 3 conflicts : 454 (21 /sec) decisions : 821 (37 /sec) propagations : 4594624 (207902 /sec) conflict literals : 6499 (36.61 % deleted) Memory used : 294.62 MB CPU time : 22.1 s SATISFIABLE VERIFY_CNF 1082 END : (23 seconds) [Sun Jun 18 18:43:59 2006] VERIFY_CNF 1082 CPU : 23.19 = 0 + 0.01 + 22.27 + 0.91 # RESULT : makespan 1082 SATISFIABLE SHOW_RESULT 1082 BEGIN : [Sun Jun 18 18:43:59 2006] # ASSIGN : makespan 1082 # ASSIGN : s_0_0 55 # ASSIGN : s_0_1 900 # ASSIGN : s_0_2 103 # ASSIGN : s_0_3 1073 # ASSIGN : s_0_4 15 # ASSIGN : s_0_5 87 # ASSIGN : s_0_6 1054 # ASSIGN : s_0_7 366 # ASSIGN : s_0_8 268 # ASSIGN : s_0_9 931 # ASSIGN : s_1_0 808 # ASSIGN : s_1_1 1075 # ASSIGN : s_1_2 528 # ASSIGN : s_1_3 1 # ASSIGN : s_1_4 805 # ASSIGN : s_1_5 984 # ASSIGN : s_1_6 659 # ASSIGN : s_1_7 1081 # ASSIGN : s_1_8 1079 # ASSIGN : s_1_9 32 # ASSIGN : s_2_0 969 # ASSIGN : s_2_1 0 # ASSIGN : s_2_2 1066 # ASSIGN : s_2_3 444 # ASSIGN : s_2_4 1068 # ASSIGN : s_2_5 16 # ASSIGN : s_2_6 79 # ASSIGN : s_2_7 311 # ASSIGN : s_2_8 359 # ASSIGN : s_2_9 1067 # ASSIGN : s_3_0 3 # ASSIGN : s_3_1 851 # ASSIGN : s_3_2 241 # ASSIGN : s_3_3 88 # ASSIGN : s_3_4 2 # ASSIGN : s_3_5 672 # ASSIGN : s_3_6 1079 # ASSIGN : s_3_7 97 # ASSIGN : s_3_8 852 # ASSIGN : s_3_9 522 # ASSIGN : s_4_0 598 # ASSIGN : s_4_1 1 # ASSIGN : s_4_2 33 # ASSIGN : s_4_3 997 # ASSIGN : s_4_4 67 # ASSIGN : s_4_5 830 # ASSIGN : s_4_6 259 # ASSIGN : s_4_7 1014 # ASSIGN : s_4_8 165 # ASSIGN : s_4_9 1081 # ASSIGN : s_5_0 97 # ASSIGN : s_5_1 1080 # ASSIGN : s_5_2 1072 # ASSIGN : s_5_3 0 # ASSIGN : s_5_4 168 # ASSIGN : s_5_5 1075 # ASSIGN : s_5_6 759 # ASSIGN : s_5_7 96 # ASSIGN : s_5_8 2 # ASSIGN : s_5_9 1 # ASSIGN : s_6_0 1051 # ASSIGN : s_6_1 903 # ASSIGN : s_6_2 34 # ASSIGN : s_6_3 32 # ASSIGN : s_6_4 10 # ASSIGN : s_6_5 98 # ASSIGN : s_6_6 15 # ASSIGN : s_6_7 901 # ASSIGN : s_6_8 613 # ASSIGN : s_6_9 31 # ASSIGN : s_7_0 535 # ASSIGN : s_7_1 20 # ASSIGN : s_7_2 1081 # ASSIGN : s_7_3 1014 # ASSIGN : s_7_4 13 # ASSIGN : s_7_5 15 # ASSIGN : s_7_6 1080 # ASSIGN : s_7_7 903 # ASSIGN : s_7_8 1 # ASSIGN : s_7_9 656 # ASSIGN : s_8_0 105 # ASSIGN : s_8_1 1038 # ASSIGN : s_8_2 645 # ASSIGN : s_8_3 89 # ASSIGN : s_8_4 14 # ASSIGN : s_8_5 1081 # ASSIGN : s_8_6 23 # ASSIGN : s_8_7 94 # ASSIGN : s_8_8 448 # ASSIGN : s_8_9 1080 # ASSIGN : s_9_0 517 # ASSIGN : s_9_1 537 # ASSIGN : s_9_2 1078 # ASSIGN : s_9_3 90 # ASSIGN : s_9_4 820 # ASSIGN : s_9_5 1079 # ASSIGN : s_9_6 1081 # ASSIGN : s_9_7 0 # ASSIGN : s_9_8 446 # ASSIGN : s_9_9 1077 SHOW_RESULT 1082 END : 1082 (2 seconds) [Sun Jun 18 18:44:01 2006] SHOW_RESULT 1082 CPU : 1.81000000000001 = 1.80000000000001 + 0.01 + 0 + 0 # BOUND : makespan 1080 1082 MODIFY_CNF 1081 BEGIN : [Sun Jun 18 18:44:01 2006] MODIFY_CNF 1081 END : 171321066 bytes (0 seconds) [Sun Jun 18 18:44:01 2006] MODIFY_CNF 1081 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1081 BEGIN : [Sun Jun 18 18:44:01 2006] CMD : minisat /tmp/csp2sat12297.cnf /tmp/csp2sat12297.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 2414013 6869530 | 804671 0 0 nan | 0.000 % | | 101 | 2414014 6869530 | 885138 100 1591 15.9 | 73.432 % | ============================================================================== restarts : 2 conflicts : 170 (9 /sec) decisions : 374 (20 /sec) propagations : 1730380 (92090 /sec) conflict literals : 2505 (28.43 % deleted) Memory used : 294.62 MB CPU time : 18.79 s SATISFIABLE VERIFY_CNF 1081 END : (19 seconds) [Sun Jun 18 18:44:20 2006] VERIFY_CNF 1081 CPU : 19.78 = 0 + 0 + 18.97 + 0.81 # RESULT : makespan 1081 SATISFIABLE SHOW_RESULT 1081 BEGIN : [Sun Jun 18 18:44:20 2006] # ASSIGN : makespan 1081 # ASSIGN : s_0_0 178 # ASSIGN : s_0_1 26 # ASSIGN : s_0_2 778 # ASSIGN : s_0_3 981 # ASSIGN : s_0_4 926 # ASSIGN : s_0_5 6 # ASSIGN : s_0_6 759 # ASSIGN : s_0_7 221 # ASSIGN : s_0_8 990 # ASSIGN : s_0_9 55 # ASSIGN : s_1_0 12 # ASSIGN : s_1_1 277 # ASSIGN : s_1_2 916 # ASSIGN : s_1_3 1033 # ASSIGN : s_1_4 1076 # ASSIGN : s_1_5 173 # ASSIGN : s_1_6 320 # ASSIGN : s_1_7 1080 # ASSIGN : s_1_8 10 # ASSIGN : s_1_9 426 # ASSIGN : s_2_0 599 # ASSIGN : s_2_1 73 # ASSIGN : s_2_2 776 # ASSIGN : s_2_3 74 # ASSIGN : s_2_4 0 # ASSIGN : s_2_5 1018 # ASSIGN : s_2_6 838 # ASSIGN : s_2_7 18 # ASSIGN : s_2_8 691 # ASSIGN : s_2_9 17 # ASSIGN : s_3_0 422 # ASSIGN : s_3_1 263 # ASSIGN : s_3_2 474 # ASSIGN : s_3_3 7 # ASSIGN : s_3_4 1079 # ASSIGN : s_3_5 264 # ASSIGN : s_3_6 9 # ASSIGN : s_3_7 755 # ASSIGN : s_3_8 33 # ASSIGN : s_3_9 943 # ASSIGN : s_4_0 210 # ASSIGN : s_4_1 0 # ASSIGN : s_4_2 777 # ASSIGN : s_4_3 1064 # ASSIGN : s_4_4 966 # ASSIGN : s_4_5 19 # ASSIGN : s_4_6 420 # ASSIGN : s_4_7 899 # ASSIGN : s_4_8 802 # ASSIGN : s_4_9 178 # ASSIGN : s_5_0 0 # ASSIGN : s_5_1 1079 # ASSIGN : s_5_2 1075 # ASSIGN : s_5_3 8 # ASSIGN : s_5_4 305 # ASSIGN : s_5_5 1014 # ASSIGN : s_5_6 10 # ASSIGN : s_5_7 9 # ASSIGN : s_5_8 896 # ASSIGN : s_5_9 1078 # ASSIGN : s_6_0 1046 # ASSIGN : s_6_1 84 # ASSIGN : s_6_2 17 # ASSIGN : s_6_3 1031 # ASSIGN : s_6_4 14 # ASSIGN : s_6_5 499 # ASSIGN : s_6_6 0 # ASSIGN : s_6_7 219 # ASSIGN : s_6_8 260 # ASSIGN : s_6_9 1077 # ASSIGN : s_7_0 501 # ASSIGN : s_7_1 564 # ASSIGN : s_7_2 1079 # ASSIGN : s_7_3 9 # ASSIGN : s_7_4 1080 # ASSIGN : s_7_5 497 # ASSIGN : s_7_6 8 # ASSIGN : s_7_7 68 # ASSIGN : s_7_8 7 # ASSIGN : s_7_9 179 # ASSIGN : s_8_0 681 # ASSIGN : s_8_1 29 # ASSIGN : s_8_2 81 # ASSIGN : s_8_3 73 # ASSIGN : s_8_4 28 # ASSIGN : s_8_5 498 # ASSIGN : s_8_6 1024 # ASSIGN : s_8_7 66 # ASSIGN : s_8_8 516 # ASSIGN : s_8_9 1080 # ASSIGN : s_9_0 581 # ASSIGN : s_9_1 281 # ASSIGN : s_9_2 16 # ASSIGN : s_9_3 627 # ASSIGN : s_9_4 33 # ASSIGN : s_9_5 17 # ASSIGN : s_9_6 1080 # ASSIGN : s_9_7 989 # ASSIGN : s_9_8 31 # ASSIGN : s_9_9 1079 SHOW_RESULT 1081 END : 1081 (2 seconds) [Sun Jun 18 18:44:22 2006] SHOW_RESULT 1081 CPU : 1.82 = 1.81 + 0.01 + 0 + 0 # BOUND : makespan 1080 1081 MODIFY_CNF 1080 BEGIN : [Sun Jun 18 18:44:22 2006] MODIFY_CNF 1080 END : 171321066 bytes (0 seconds) [Sun Jun 18 18:44:22 2006] MODIFY_CNF 1080 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1080 BEGIN : [Sun Jun 18 18:44:22 2006] CMD : minisat /tmp/csp2sat12297.cnf /tmp/csp2sat12297.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 2412213 6864130 | 804071 0 0 nan | 0.000 % | | 100 | 2412214 6864130 | 884478 99 1393 14.1 | 73.459 % | | 250 | 2412214 6864130 | 972925 249 3570 14.3 | 73.459 % | | 475 | 2412215 6864130 | 1070218 473 6475 13.7 | 73.459 % | | 812 | 2412220 6864130 | 1177240 803 11117 13.8 | 76.828 % | ============================================================================== restarts : 5 conflicts : 860 (33 /sec) decisions : 1161 (44 /sec) propagations : 7788912 (297514 /sec) conflict literals : 11426 (39.67 % deleted) Memory used : 293.04 MB CPU time : 26.18 s UNSATISFIABLE VERIFY_CNF 1080 END : (27 seconds) [Sun Jun 18 18:44:49 2006] VERIFY_CNF 1080 CPU : 27.16 = 0 + 0.01 + 26.18 + 0.969999999999999 # RESULT : makespan 1080 UNSATISFIABLE # BOUND : makespan 1081 1081 MAIN END : (536 seconds) [Sun Jun 18 18:44:49 2006] MAIN CPU : 535.08 = 289.37 + 1.44 + 233.25 + 11.02