# TIMEOUT 18000 MAIN BEGIN : [Sun Jun 18 18:44:50 2006] READ BEGIN : csp/gp10-04.csp [Sun Jun 18 18:44:50 2006] READ END : csp/gp10-04.csp (2 seconds) [Sun Jun 18 18:44:52 2006] READ CPU : 1.91 = 1.88 + 0.03 + 0 + 0 # BOUND : makespan 1000 3736 GENERATE_CNF 3736 BEGIN : [Sun Jun 18 18:44:52 2006] GENERATE_CNF 3736 END : 378438 variables 7199739 clauses 172353154 bytes (287 seconds) [Sun Jun 18 18:49:39 2006] GENERATE_CNF 3736 CPU : 286.26 = 284.75 + 1.51 + 0 + 0 MODIFY_CNF 2368 BEGIN : [Sun Jun 18 18:49:39 2006] MODIFY_CNF 2368 END : 172353161 bytes (0 seconds) [Sun Jun 18 18:49:39 2006] MODIFY_CNF 2368 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 2368 BEGIN : [Sun Jun 18 18:49:39 2006] CMD : minisat /tmp/csp2sat12447.cnf /tmp/csp2sat12447.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 4734834 13829872 | 1578278 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 3 (0 /sec) decisions : 641 (61 /sec) propagations : 445666 (42163 /sec) conflict literals : 73 (0.00 % deleted) Memory used : 296.33 MB CPU time : 10.57 s SATISFIABLE VERIFY_CNF 2368 END : (11 seconds) [Sun Jun 18 18:49:50 2006] VERIFY_CNF 2368 CPU : 11.79 = 0 + 0 + 10.76 + 1.03 # RESULT : makespan 2368 SATISFIABLE SHOW_RESULT 2368 BEGIN : [Sun Jun 18 18:49:50 2006] # ASSIGN : makespan 2368 # ASSIGN : s_0_0 11 # ASSIGN : s_0_1 12 # ASSIGN : s_0_2 640 # ASSIGN : s_0_3 204 # ASSIGN : s_0_4 13 # ASSIGN : s_0_5 38 # ASSIGN : s_0_6 39 # ASSIGN : s_0_7 144 # ASSIGN : s_0_8 44 # ASSIGN : s_0_9 202 # ASSIGN : s_1_0 38 # ASSIGN : s_1_1 559 # ASSIGN : s_1_2 1114 # ASSIGN : s_1_3 801 # ASSIGN : s_1_4 48 # ASSIGN : s_1_5 237 # ASSIGN : s_1_6 40 # ASSIGN : s_1_7 221 # ASSIGN : s_1_8 45 # ASSIGN : s_1_9 222 # ASSIGN : s_2_0 303 # ASSIGN : s_2_1 788 # ASSIGN : s_2_2 1374 # ASSIGN : s_2_3 803 # ASSIGN : s_2_4 223 # ASSIGN : s_2_5 701 # ASSIGN : s_2_6 111 # ASSIGN : s_2_7 224 # ASSIGN : s_2_8 112 # ASSIGN : s_2_9 225 # ASSIGN : s_3_0 1180 # ASSIGN : s_3_1 819 # ASSIGN : s_3_2 1528 # ASSIGN : s_3_3 1037 # ASSIGN : s_3_4 231 # ASSIGN : s_3_5 781 # ASSIGN : s_3_6 225 # ASSIGN : s_3_7 228 # ASSIGN : s_3_8 229 # ASSIGN : s_3_9 230 # ASSIGN : s_4_0 1605 # ASSIGN : s_4_1 820 # ASSIGN : s_4_2 1609 # ASSIGN : s_4_3 1048 # ASSIGN : s_4_4 783 # ASSIGN : s_4_5 784 # ASSIGN : s_4_6 240 # ASSIGN : s_4_7 417 # ASSIGN : s_4_8 1142 # ASSIGN : s_4_9 294 # ASSIGN : s_5_0 1606 # ASSIGN : s_5_1 821 # ASSIGN : s_5_2 1610 # ASSIGN : s_5_3 1103 # ASSIGN : s_5_4 819 # ASSIGN : s_5_5 820 # ASSIGN : s_5_6 420 # ASSIGN : s_5_7 1104 # ASSIGN : s_5_8 1946 # ASSIGN : s_5_9 316 # ASSIGN : s_6_0 1607 # ASSIGN : s_6_1 1105 # ASSIGN : s_6_2 1611 # ASSIGN : s_6_3 1108 # ASSIGN : s_6_4 1366 # ASSIGN : s_6_5 825 # ASSIGN : s_6_6 502 # ASSIGN : s_6_7 1873 # ASSIGN : s_6_8 1971 # ASSIGN : s_6_9 503 # ASSIGN : s_7_0 1611 # ASSIGN : s_7_1 1119 # ASSIGN : s_7_2 1612 # ASSIGN : s_7_3 1634 # ASSIGN : s_7_4 1609 # ASSIGN : s_7_5 1334 # ASSIGN : s_7_6 722 # ASSIGN : s_7_7 1880 # ASSIGN : s_7_8 2054 # ASSIGN : s_7_9 625 # ASSIGN : s_8_0 1939 # ASSIGN : s_8_1 1365 # ASSIGN : s_8_2 1617 # ASSIGN : s_8_3 1635 # ASSIGN : s_8_4 1636 # ASSIGN : s_8_5 1641 # ASSIGN : s_8_6 1408 # ASSIGN : s_8_7 1889 # ASSIGN : s_8_8 2068 # ASSIGN : s_8_9 706 # ASSIGN : s_9_0 1944 # ASSIGN : s_9_1 1368 # ASSIGN : s_9_2 1618 # ASSIGN : s_9_3 1640 # ASSIGN : s_9_4 1641 # ASSIGN : s_9_5 1642 # ASSIGN : s_9_6 1643 # ASSIGN : s_9_7 1890 # ASSIGN : s_9_8 2183 # ASSIGN : s_9_9 2367 SHOW_RESULT 2368 END : 2368 (2 seconds) [Sun Jun 18 18:49:52 2006] SHOW_RESULT 2368 CPU : 1.38999999999998 = 1.33999999999997 + 0.05 + 0 + 0 # BOUND : makespan 1000 2368 MODIFY_CNF 1684 BEGIN : [Sun Jun 18 18:49:52 2006] MODIFY_CNF 1684 END : 172353160 bytes (0 seconds) [Sun Jun 18 18:49:52 2006] MODIFY_CNF 1684 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1684 BEGIN : [Sun Jun 18 18:49:52 2006] CMD : minisat /tmp/csp2sat12447.cnf /tmp/csp2sat12447.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 3503634 10136272 | 1167878 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 18 (1 /sec) decisions : 657 (51 /sec) propagations : 592966 (46145 /sec) conflict literals : 257 (8.21 % deleted) Memory used : 296.33 MB CPU time : 12.85 s SATISFIABLE VERIFY_CNF 1684 END : (14 seconds) [Sun Jun 18 18:50:06 2006] VERIFY_CNF 1684 CPU : 13.85 = 0 + 0 + 13.02 + 0.83 # RESULT : makespan 1684 SATISFIABLE SHOW_RESULT 1684 BEGIN : [Sun Jun 18 18:50:06 2006] # ASSIGN : makespan 1684 # ASSIGN : s_0_0 3 # ASSIGN : s_0_1 5 # ASSIGN : s_0_2 1209 # ASSIGN : s_0_3 606 # ASSIGN : s_0_4 333 # ASSIGN : s_0_5 35 # ASSIGN : s_0_6 0 # ASSIGN : s_0_7 488 # ASSIGN : s_0_8 4 # ASSIGN : s_0_9 6 # ASSIGN : s_1_0 1682 # ASSIGN : s_1_1 1451 # ASSIGN : s_1_2 568 # ASSIGN : s_1_3 1042 # ASSIGN : s_1_4 358 # ASSIGN : s_1_5 36 # ASSIGN : s_1_6 1 # ASSIGN : s_1_7 546 # ASSIGN : s_1_8 13 # ASSIGN : s_1_9 8 # ASSIGN : s_2_0 629 # ASSIGN : s_2_1 532 # ASSIGN : s_2_2 1027 # ASSIGN : s_2_3 217 # ASSIGN : s_2_4 531 # ASSIGN : s_2_5 451 # ASSIGN : s_2_6 6 # ASSIGN : s_2_7 547 # ASSIGN : s_2_8 16 # ASSIGN : s_2_9 11 # ASSIGN : s_3_0 186 # ASSIGN : s_3_1 6 # ASSIGN : s_3_2 24 # ASSIGN : s_3_3 534 # ASSIGN : s_3_4 549 # ASSIGN : s_3_5 545 # ASSIGN : s_3_6 7 # ASSIGN : s_3_7 548 # ASSIGN : s_3_8 127 # ASSIGN : s_3_9 105 # ASSIGN : s_4_0 7 # ASSIGN : s_4_1 8 # ASSIGN : s_4_2 9 # ASSIGN : s_4_3 1044 # ASSIGN : s_4_4 1099 # ASSIGN : s_4_5 642 # ASSIGN : s_4_6 10 # ASSIGN : s_4_7 678 # ASSIGN : s_4_8 128 # ASSIGN : s_4_9 106 # ASSIGN : s_5_0 18 # ASSIGN : s_5_1 250 # ASSIGN : s_5_2 23 # ASSIGN : s_5_3 1099 # ASSIGN : s_5_4 1100 # ASSIGN : s_5_5 820 # ASSIGN : s_5_6 64 # ASSIGN : s_5_7 1111 # ASSIGN : s_5_8 591 # ASSIGN : s_5_9 146 # ASSIGN : s_6_0 19 # ASSIGN : s_6_1 23 # ASSIGN : s_6_2 239 # ASSIGN : s_6_3 1355 # ASSIGN : s_6_4 1101 # ASSIGN : s_6_5 821 # ASSIGN : s_6_6 240 # ASSIGN : s_6_7 1613 # ASSIGN : s_6_8 616 # ASSIGN : s_6_9 699 # ASSIGN : s_7_0 25 # ASSIGN : s_7_1 26 # ASSIGN : s_7_2 828 # ASSIGN : s_7_3 1619 # ASSIGN : s_7_4 1342 # ASSIGN : s_7_5 1344 # ASSIGN : s_7_6 241 # ASSIGN : s_7_7 1620 # ASSIGN : s_7_8 833 # ASSIGN : s_7_9 881 # ASSIGN : s_8_0 624 # ASSIGN : s_8_1 1680 # ASSIGN : s_8_2 1683 # ASSIGN : s_8_3 1628 # ASSIGN : s_8_4 1621 # ASSIGN : s_8_5 1626 # ASSIGN : s_8_6 638 # ASSIGN : s_8_7 1629 # ASSIGN : s_8_8 847 # ASSIGN : s_8_9 962 # ASSIGN : s_9_0 1203 # ASSIGN : s_9_1 684 # ASSIGN : s_9_2 1181 # ASSIGN : s_9_3 1629 # ASSIGN : s_9_4 1626 # ASSIGN : s_9_5 1627 # ASSIGN : s_9_6 934 # ASSIGN : s_9_7 1630 # ASSIGN : s_9_8 1442 # ASSIGN : s_9_9 1628 SHOW_RESULT 1684 END : 1684 (1 seconds) [Sun Jun 18 18:50:07 2006] SHOW_RESULT 1684 CPU : 1.76 = 1.75 + 0.01 + 0 + 0 # BOUND : makespan 1000 1684 MODIFY_CNF 1342 BEGIN : [Sun Jun 18 18:50:08 2006] MODIFY_CNF 1342 END : 172353160 bytes (0 seconds) [Sun Jun 18 18:50:08 2006] MODIFY_CNF 1342 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1342 BEGIN : [Sun Jun 18 18:50:08 2006] CMD : minisat /tmp/csp2sat12447.cnf /tmp/csp2sat12447.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 2888034 8289472 | 962678 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 7 (0 /sec) decisions : 496 (32 /sec) propagations : 448848 (29108 /sec) conflict literals : 93 (3.12 % deleted) Memory used : 296.34 MB CPU time : 15.42 s SATISFIABLE VERIFY_CNF 1342 END : (16 seconds) [Sun Jun 18 18:50:24 2006] VERIFY_CNF 1342 CPU : 16.73 = 0 + 0 + 15.61 + 1.12 # RESULT : makespan 1342 SATISFIABLE SHOW_RESULT 1342 BEGIN : [Sun Jun 18 18:50:24 2006] # ASSIGN : makespan 1342 # ASSIGN : s_0_0 2 # ASSIGN : s_0_1 0 # ASSIGN : s_0_2 56 # ASSIGN : s_0_3 530 # ASSIGN : s_0_4 11 # ASSIGN : s_0_5 4 # ASSIGN : s_0_6 5 # ASSIGN : s_0_7 966 # ASSIGN : s_0_8 6 # ASSIGN : s_0_9 7 # ASSIGN : s_1_0 3 # ASSIGN : s_1_1 702 # ASSIGN : s_1_2 987 # ASSIGN : s_1_3 0 # ASSIGN : s_1_4 369 # ASSIGN : s_1_5 47 # ASSIGN : s_1_6 32 # ASSIGN : s_1_7 8 # ASSIGN : s_1_8 29 # ASSIGN : s_1_9 9 # ASSIGN : s_2_0 944 # ASSIGN : s_2_1 21 # ASSIGN : s_2_2 710 # ASSIGN : s_2_3 38 # ASSIGN : s_2_4 36 # ASSIGN : s_2_5 864 # ASSIGN : s_2_6 37 # ASSIGN : s_2_7 11 # ASSIGN : s_2_8 334 # ASSIGN : s_2_9 12 # ASSIGN : s_3_0 97 # ASSIGN : s_3_1 1 # ASSIGN : s_3_2 1247 # ASSIGN : s_3_3 2 # ASSIGN : s_3_4 542 # ASSIGN : s_3_5 13 # ASSIGN : s_3_6 94 # ASSIGN : s_3_7 16 # ASSIGN : s_3_8 445 # ASSIGN : s_3_9 17 # ASSIGN : s_4_0 5 # ASSIGN : s_4_1 9 # ASSIGN : s_4_2 10 # ASSIGN : s_4_3 1150 # ASSIGN : s_4_4 40 # ASSIGN : s_4_5 410 # ASSIGN : s_4_6 1205 # ASSIGN : s_4_7 41 # ASSIGN : s_4_8 446 # ASSIGN : s_4_9 18 # ASSIGN : s_5_0 6 # ASSIGN : s_5_1 977 # ASSIGN : s_5_2 36 # ASSIGN : s_5_3 37 # ASSIGN : s_5_4 44 # ASSIGN : s_5_5 45 # ASSIGN : s_5_6 1259 # ASSIGN : s_5_7 407 # ASSIGN : s_5_8 909 # ASSIGN : s_5_9 46 # ASSIGN : s_6_0 7 # ASSIGN : s_6_1 931 # ASSIGN : s_6_2 11 # ASSIGN : s_6_3 272 # ASSIGN : s_6_4 1092 # ASSIGN : s_6_5 584 # ASSIGN : s_6_6 1341 # ASSIGN : s_6_7 1024 # ASSIGN : s_6_8 934 # ASSIGN : s_6_9 150 # ASSIGN : s_7_0 28 # ASSIGN : s_7_1 85 # ASSIGN : s_7_2 1328 # ASSIGN : s_7_3 1016 # ASSIGN : s_7_4 1333 # ASSIGN : s_7_5 1053 # ASSIGN : s_7_6 457 # ASSIGN : s_7_7 1031 # ASSIGN : s_7_8 1017 # ASSIGN : s_7_9 300 # ASSIGN : s_8_0 29 # ASSIGN : s_8_1 1332 # ASSIGN : s_8_2 34 # ASSIGN : s_8_3 35 # ASSIGN : s_8_4 1335 # ASSIGN : s_8_5 1340 # ASSIGN : s_8_6 172 # ASSIGN : s_8_7 1040 # ASSIGN : s_8_8 1041 # ASSIGN : s_8_9 381 # ASSIGN : s_9_0 615 # ASSIGN : s_9_1 365 # ASSIGN : s_9_2 12 # ASSIGN : s_9_3 36 # ASSIGN : s_9_4 1340 # ASSIGN : s_9_5 1341 # ASSIGN : s_9_6 854 # ASSIGN : s_9_7 1101 # ASSIGN : s_9_8 1156 # ASSIGN : s_9_9 1155 SHOW_RESULT 1342 END : 1342 (2 seconds) [Sun Jun 18 18:50:26 2006] SHOW_RESULT 1342 CPU : 1.71999999999999 = 1.69999999999999 + 0.0199999999999998 + 0 + 0 # BOUND : makespan 1000 1342 MODIFY_CNF 1171 BEGIN : [Sun Jun 18 18:50:26 2006] MODIFY_CNF 1171 END : 172353160 bytes (0 seconds) [Sun Jun 18 18:50:26 2006] MODIFY_CNF 1171 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1171 BEGIN : [Sun Jun 18 18:50:26 2006] CMD : minisat /tmp/csp2sat12447.cnf /tmp/csp2sat12447.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 2580234 7366072 | 860078 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 12 (1 /sec) decisions : 340 (21 /sec) propagations : 486811 (29540 /sec) conflict literals : 118 (7.09 % deleted) Memory used : 296.34 MB CPU time : 16.48 s SATISFIABLE VERIFY_CNF 1171 END : (18 seconds) [Sun Jun 18 18:50:44 2006] VERIFY_CNF 1171 CPU : 17.75 = 0 + 0.02 + 16.66 + 1.07 # RESULT : makespan 1171 SATISFIABLE SHOW_RESULT 1171 BEGIN : [Sun Jun 18 18:50:44 2006] # ASSIGN : makespan 1171 # ASSIGN : s_0_0 3 # ASSIGN : s_0_1 4 # ASSIGN : s_0_2 697 # ASSIGN : s_0_3 122 # ASSIGN : s_0_4 97 # ASSIGN : s_0_5 5 # ASSIGN : s_0_6 2 # ASSIGN : s_0_7 39 # ASSIGN : s_0_8 6 # ASSIGN : s_0_9 0 # ASSIGN : s_1_0 11 # ASSIGN : s_1_1 21 # ASSIGN : s_1_2 380 # ASSIGN : s_1_3 5 # ASSIGN : s_1_4 993 # ASSIGN : s_1_5 671 # ASSIGN : s_1_6 1166 # ASSIGN : s_1_7 1 # ASSIGN : s_1_8 7 # ASSIGN : s_1_9 2 # ASSIGN : s_2_0 280 # ASSIGN : s_2_1 941 # ASSIGN : s_2_2 126 # ASSIGN : s_2_3 678 # ASSIGN : s_2_4 0 # ASSIGN : s_2_5 1091 # ASSIGN : s_2_6 1 # ASSIGN : s_2_7 4 # ASSIGN : s_2_8 10 # ASSIGN : s_2_9 5 # ASSIGN : s_3_0 823 # ASSIGN : s_3_1 19 # ASSIGN : s_3_2 21 # ASSIGN : s_3_3 7 # ASSIGN : s_3_4 122 # ASSIGN : s_3_5 0 # ASSIGN : s_3_6 3 # ASSIGN : s_3_7 6 # ASSIGN : s_3_8 121 # ASSIGN : s_3_9 18 # ASSIGN : s_4_0 13 # ASSIGN : s_4_1 20 # ASSIGN : s_4_2 102 # ASSIGN : s_4_3 47 # ASSIGN : s_4_4 24 # ASSIGN : s_4_5 994 # ASSIGN : s_4_6 1030 # ASSIGN : s_4_7 103 # ASSIGN : s_4_8 469 # ASSIGN : s_4_9 25 # ASSIGN : s_5_0 14 # ASSIGN : s_5_1 299 # ASSIGN : s_5_2 123 # ASSIGN : s_5_3 581 # ASSIGN : s_5_4 29 # ASSIGN : s_5_5 34 # ASSIGN : s_5_6 1084 # ASSIGN : s_5_7 582 # ASSIGN : s_5_8 124 # ASSIGN : s_5_9 149 # ASSIGN : s_6_0 15 # ASSIGN : s_6_1 250 # ASSIGN : s_6_2 125 # ASSIGN : s_6_3 913 # ASSIGN : s_6_4 672 # ASSIGN : s_6_5 391 # ASSIGN : s_6_6 19 # ASSIGN : s_6_7 20 # ASSIGN : s_6_8 167 # ASSIGN : s_6_9 253 # ASSIGN : s_7_0 23 # ASSIGN : s_7_1 956 # ASSIGN : s_7_2 322 # ASSIGN : s_7_3 558 # ASSIGN : s_7_4 25 # ASSIGN : s_7_5 36 # ASSIGN : s_7_6 559 # ASSIGN : s_7_7 27 # ASSIGN : s_7_8 327 # ASSIGN : s_7_9 375 # ASSIGN : s_8_0 24 # ASSIGN : s_8_1 296 # ASSIGN : s_8_2 340 # ASSIGN : s_8_3 29 # ASSIGN : s_8_4 30 # ASSIGN : s_8_5 35 # ASSIGN : s_8_6 87 # ASSIGN : s_8_7 1115 # ASSIGN : s_8_8 341 # ASSIGN : s_8_9 456 # ASSIGN : s_9_0 41 # ASSIGN : s_9_1 662 # ASSIGN : s_9_2 640 # ASSIGN : s_9_3 912 # ASSIGN : s_9_4 40 # ASSIGN : s_9_5 311 # ASSIGN : s_9_6 312 # ASSIGN : s_9_7 1116 # ASSIGN : s_9_8 932 # ASSIGN : s_9_9 1170 SHOW_RESULT 1171 END : 1171 (2 seconds) [Sun Jun 18 18:50:46 2006] SHOW_RESULT 1171 CPU : 1.71999999999999 = 1.69999999999999 + 0.02 + 0 + 0 # BOUND : makespan 1000 1171 MODIFY_CNF 1085 BEGIN : [Sun Jun 18 18:50:46 2006] MODIFY_CNF 1085 END : 172353159 bytes (0 seconds) [Sun Jun 18 18:50:46 2006] MODIFY_CNF 1085 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1085 BEGIN : [Sun Jun 18 18:50:46 2006] CMD : minisat /tmp/csp2sat12447.cnf /tmp/csp2sat12447.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 2425434 6901672 | 808478 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 34 (2 /sec) decisions : 247 (14 /sec) propagations : 705973 (40480 /sec) conflict literals : 465 (23.52 % deleted) Memory used : 296.34 MB CPU time : 17.44 s SATISFIABLE VERIFY_CNF 1085 END : (18 seconds) [Sun Jun 18 18:51:04 2006] VERIFY_CNF 1085 CPU : 18.49 = 0 + 0.01 + 17.62 + 0.86 # RESULT : makespan 1085 SATISFIABLE SHOW_RESULT 1085 BEGIN : [Sun Jun 18 18:51:04 2006] # ASSIGN : makespan 1085 # ASSIGN : s_0_0 2 # ASSIGN : s_0_1 1 # ASSIGN : s_0_2 457 # ASSIGN : s_0_3 3 # ASSIGN : s_0_4 1000 # ASSIGN : s_0_5 448 # ASSIGN : s_0_6 0 # ASSIGN : s_0_7 1027 # ASSIGN : s_0_8 999 # ASSIGN : s_0_9 1025 # ASSIGN : s_1_0 0 # ASSIGN : s_1_1 842 # ASSIGN : s_1_2 197 # ASSIGN : s_1_3 1071 # ASSIGN : s_1_4 3 # ASSIGN : s_1_5 485 # ASSIGN : s_1_6 1080 # ASSIGN : s_1_7 470 # ASSIGN : s_1_8 482 # ASSIGN : s_1_9 1077 # ASSIGN : s_2_0 299 # ASSIGN : s_2_1 12 # ASSIGN : s_2_2 931 # ASSIGN : s_2_3 697 # ASSIGN : s_2_4 0 # ASSIGN : s_2_5 72 # ASSIGN : s_2_6 152 # ASSIGN : s_2_7 9 # ASSIGN : s_2_8 160 # ASSIGN : s_2_9 280 # ASSIGN : s_3_0 726 # ASSIGN : s_3_1 27 # ASSIGN : s_3_2 72 # ASSIGN : s_3_3 1074 # ASSIGN : s_3_4 176 # ASSIGN : s_3_5 156 # ASSIGN : s_3_6 153 # ASSIGN : s_3_7 8 # ASSIGN : s_3_8 159 # ASSIGN : s_3_9 16 # ASSIGN : s_4_0 1082 # ASSIGN : s_4_1 2 # ASSIGN : s_4_2 71 # ASSIGN : s_4_3 999 # ASSIGN : s_4_4 1076 # ASSIGN : s_4_5 449 # ASSIGN : s_4_6 3 # ASSIGN : s_4_7 83 # ASSIGN : s_4_8 536 # ASSIGN : s_4_9 1054 # ASSIGN : s_5_0 1083 # ASSIGN : s_5_1 243 # ASSIGN : s_5_2 13 # ASSIGN : s_5_3 1 # ASSIGN : s_5_4 1084 # ASSIGN : s_5_5 1082 # ASSIGN : s_5_6 57 # ASSIGN : s_5_7 525 # ASSIGN : s_5_8 17 # ASSIGN : s_5_9 139 # ASSIGN : s_6_0 722 # ASSIGN : s_6_1 7 # ASSIGN : s_6_2 158 # ASSIGN : s_6_3 439 # ASSIGN : s_6_4 759 # ASSIGN : s_6_5 159 # ASSIGN : s_6_6 156 # ASSIGN : s_6_7 10 # ASSIGN : s_6_8 1002 # ASSIGN : s_6_9 17 # ASSIGN : s_7_0 1084 # ASSIGN : s_7_1 28 # ASSIGN : s_7_2 14 # ASSIGN : s_7_3 0 # ASSIGN : s_7_4 1 # ASSIGN : s_7_5 807 # ASSIGN : s_7_6 410 # ASSIGN : s_7_7 19 # ASSIGN : s_7_8 271 # ASSIGN : s_7_9 285 # ASSIGN : s_8_0 36 # ASSIGN : s_8_1 1074 # ASSIGN : s_8_2 25 # ASSIGN : s_8_3 1073 # ASSIGN : s_8_4 1077 # ASSIGN : s_8_5 1083 # ASSIGN : s_8_6 157 # ASSIGN : s_8_7 41 # ASSIGN : s_8_8 42 # ASSIGN : s_8_9 366 # ASSIGN : s_9_0 48 # ASSIGN : s_9_1 583 # ASSIGN : s_9_2 26 # ASSIGN : s_9_3 2 # ASSIGN : s_9_4 1082 # ASSIGN : s_9_5 1084 # ASSIGN : s_9_6 833 # ASSIGN : s_9_7 471 # ASSIGN : s_9_8 287 # ASSIGN : s_9_9 1083 SHOW_RESULT 1085 END : 1085 (2 seconds) [Sun Jun 18 18:51:06 2006] SHOW_RESULT 1085 CPU : 1.74000000000002 = 1.73000000000002 + 0.01 + 0 + 0 # BOUND : makespan 1000 1085 MODIFY_CNF 1042 BEGIN : [Sun Jun 18 18:51:06 2006] MODIFY_CNF 1042 END : 172353159 bytes (0 seconds) [Sun Jun 18 18:51:06 2006] MODIFY_CNF 1042 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1042 BEGIN : [Sun Jun 18 18:51:06 2006] CMD : minisat /tmp/csp2sat12447.cnf /tmp/csp2sat12447.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 2348034 6669472 | 782678 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 43 (3 /sec) decisions : 89 (5 /sec) propagations : 526469 (30680 /sec) conflict literals : 174 (23.35 % deleted) Memory used : 294.61 MB CPU time : 17.16 s UNSATISFIABLE VERIFY_CNF 1042 END : (18 seconds) [Sun Jun 18 18:51:24 2006] VERIFY_CNF 1042 CPU : 18.14 = 0 + 0 + 17.16 + 0.98 # RESULT : makespan 1042 UNSATISFIABLE # BOUND : makespan 1043 1085 MODIFY_CNF 1064 BEGIN : [Sun Jun 18 18:51:24 2006] MODIFY_CNF 1064 END : 172353159 bytes (0 seconds) [Sun Jun 18 18:51:24 2006] MODIFY_CNF 1064 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1064 BEGIN : [Sun Jun 18 18:51:24 2006] CMD : minisat /tmp/csp2sat12447.cnf /tmp/csp2sat12447.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 2387634 6788272 | 795878 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 61 (4 /sec) decisions : 115 (7 /sec) propagations : 734157 (42560 /sec) conflict literals : 354 (31.66 % deleted) Memory used : 294.66 MB CPU time : 17.25 s UNSATISFIABLE VERIFY_CNF 1064 END : (18 seconds) [Sun Jun 18 18:51:42 2006] VERIFY_CNF 1064 CPU : 18.29 = 0 + 0 + 17.25 + 1.04 # RESULT : makespan 1064 UNSATISFIABLE # BOUND : makespan 1065 1085 MODIFY_CNF 1075 BEGIN : [Sun Jun 18 18:51:42 2006] MODIFY_CNF 1075 END : 172353159 bytes (0 seconds) [Sun Jun 18 18:51:42 2006] MODIFY_CNF 1075 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1075 BEGIN : [Sun Jun 18 18:51:42 2006] CMD : minisat /tmp/csp2sat12447.cnf /tmp/csp2sat12447.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 2407434 6847672 | 802478 0 0 nan | 0.000 % | | 103 | 2407435 6847672 | 882725 102 1213 11.9 | 73.741 % | ============================================================================== restarts : 2 conflicts : 164 (8 /sec) decisions : 233 (12 /sec) propagations : 1945354 (98003 /sec) conflict literals : 1563 (28.27 % deleted) Memory used : 294.73 MB CPU time : 19.85 s UNSATISFIABLE VERIFY_CNF 1075 END : (21 seconds) [Sun Jun 18 18:52:03 2006] VERIFY_CNF 1075 CPU : 20.74 = 0 + 0 + 19.85 + 0.890000000000001 # RESULT : makespan 1075 UNSATISFIABLE # BOUND : makespan 1076 1085 MODIFY_CNF 1080 BEGIN : [Sun Jun 18 18:52:03 2006] MODIFY_CNF 1080 END : 172353159 bytes (0 seconds) [Sun Jun 18 18:52:03 2006] MODIFY_CNF 1080 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1080 BEGIN : [Sun Jun 18 18:52:03 2006] CMD : minisat /tmp/csp2sat12447.cnf /tmp/csp2sat12447.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 2416434 6874672 | 805478 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 63 (4 /sec) decisions : 269 (15 /sec) propagations : 900462 (50418 /sec) conflict literals : 752 (20.00 % deleted) Memory used : 296.34 MB CPU time : 17.86 s SATISFIABLE VERIFY_CNF 1080 END : (19 seconds) [Sun Jun 18 18:52:22 2006] VERIFY_CNF 1080 CPU : 18.99 = 0 + 0 + 18.06 + 0.93 # RESULT : makespan 1080 SATISFIABLE SHOW_RESULT 1080 BEGIN : [Sun Jun 18 18:52:22 2006] # ASSIGN : makespan 1080 # ASSIGN : s_0_0 1079 # ASSIGN : s_0_1 1078 # ASSIGN : s_0_2 604 # ASSIGN : s_0_3 2 # ASSIGN : s_0_4 505 # ASSIGN : s_0_5 441 # ASSIGN : s_0_6 603 # ASSIGN : s_0_7 447 # ASSIGN : s_0_8 561 # ASSIGN : s_0_9 0 # ASSIGN : s_1_0 10 # ASSIGN : s_1_1 844 # ASSIGN : s_1_2 189 # ASSIGN : s_1_3 834 # ASSIGN : s_1_4 16 # ASSIGN : s_1_5 478 # ASSIGN : s_1_6 5 # ASSIGN : s_1_7 15 # ASSIGN : s_1_8 1073 # ASSIGN : s_1_9 1076 # ASSIGN : s_2_0 438 # ASSIGN : s_2_1 343 # ASSIGN : s_2_2 32 # ASSIGN : s_2_3 836 # ASSIGN : s_2_4 10 # ASSIGN : s_2_5 358 # ASSIGN : s_2_6 29 # ASSIGN : s_2_7 9 # ASSIGN : s_2_8 186 # ASSIGN : s_2_9 1071 # ASSIGN : s_3_0 26 # ASSIGN : s_3_1 374 # ASSIGN : s_3_2 449 # ASSIGN : s_3_3 438 # ASSIGN : s_3_4 530 # ASSIGN : s_3_5 20 # ASSIGN : s_3_6 23 # ASSIGN : s_3_7 8 # ASSIGN : s_3_8 1 # ASSIGN : s_3_9 389 # ASSIGN : s_4_0 437 # ASSIGN : s_4_1 1079 # ASSIGN : s_4_2 561 # ASSIGN : s_4_3 487 # ASSIGN : s_4_4 485 # ASSIGN : s_4_5 442 # ASSIGN : s_4_6 1025 # ASSIGN : s_4_7 24 # ASSIGN : s_4_8 562 # ASSIGN : s_4_9 390 # ASSIGN : s_5_0 433 # ASSIGN : s_5_1 3 # ASSIGN : s_5_2 1079 # ASSIGN : s_5_3 1078 # ASSIGN : s_5_4 486 # ASSIGN : s_5_5 2 # ASSIGN : s_5_6 487 # ASSIGN : s_5_7 569 # ASSIGN : s_5_8 434 # ASSIGN : s_5_9 285 # ASSIGN : s_6_0 12 # ASSIGN : s_6_1 0 # ASSIGN : s_6_2 31 # ASSIGN : s_6_3 542 # ASSIGN : s_6_4 218 # ASSIGN : s_6_5 800 # ASSIGN : s_6_6 30 # ASSIGN : s_6_7 16 # ASSIGN : s_6_8 459 # ASSIGN : s_6_9 96 # ASSIGN : s_7_0 374 # ASSIGN : s_7_1 375 # ASSIGN : s_7_2 599 # ASSIGN : s_7_3 1070 # ASSIGN : s_7_4 0 # ASSIGN : s_7_5 83 # ASSIGN : s_7_6 628 # ASSIGN : s_7_7 1071 # ASSIGN : s_7_8 1056 # ASSIGN : s_7_9 2 # ASSIGN : s_8_0 18 # ASSIGN : s_8_1 1075 # ASSIGN : s_8_2 1078 # ASSIGN : s_8_3 1079 # ASSIGN : s_8_4 11 # ASSIGN : s_8_5 30 # ASSIGN : s_8_6 31 # ASSIGN : s_8_7 23 # ASSIGN : s_8_8 297 # ASSIGN : s_8_9 412 # ASSIGN : s_9_0 840 # ASSIGN : s_9_1 590 # ASSIGN : s_9_2 568 # ASSIGN : s_9_3 0 # ASSIGN : s_9_4 504 # ASSIGN : s_9_5 1 # ASSIGN : s_9_6 240 # ASSIGN : s_9_7 514 # ASSIGN : s_9_8 2 # ASSIGN : s_9_9 1079 SHOW_RESULT 1080 END : 1080 (2 seconds) [Sun Jun 18 18:52:24 2006] SHOW_RESULT 1080 CPU : 1.74000000000001 = 1.74000000000001 + 0 + 0 + 0 # BOUND : makespan 1076 1080 MODIFY_CNF 1078 BEGIN : [Sun Jun 18 18:52:24 2006] MODIFY_CNF 1078 END : 172353159 bytes (0 seconds) [Sun Jun 18 18:52:24 2006] MODIFY_CNF 1078 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1078 BEGIN : [Sun Jun 18 18:52:24 2006] CMD : minisat /tmp/csp2sat12447.cnf /tmp/csp2sat12447.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 2412834 6863872 | 804278 0 0 nan | 0.000 % | | 102 | 2412834 6863872 | 884705 102 1334 13.1 | 73.661 % | ============================================================================== restarts : 2 conflicts : 133 (7 /sec) decisions : 392 (21 /sec) propagations : 1666388 (90466 /sec) conflict literals : 1557 (28.81 % deleted) Memory used : 296.36 MB CPU time : 18.42 s SATISFIABLE VERIFY_CNF 1078 END : (19 seconds) [Sun Jun 18 18:52:43 2006] VERIFY_CNF 1078 CPU : 19.5 = 0 + 0 + 18.62 + 0.880000000000001 # RESULT : makespan 1078 SATISFIABLE SHOW_RESULT 1078 BEGIN : [Sun Jun 18 18:52:43 2006] # ASSIGN : makespan 1078 # ASSIGN : s_0_0 437 # ASSIGN : s_0_1 1074 # ASSIGN : s_0_2 600 # ASSIGN : s_0_3 0 # ASSIGN : s_0_4 503 # ASSIGN : s_0_5 439 # ASSIGN : s_0_6 1075 # ASSIGN : s_0_7 445 # ASSIGN : s_0_8 599 # ASSIGN : s_0_9 1076 # ASSIGN : s_1_0 837 # ASSIGN : s_1_1 841 # ASSIGN : s_1_2 184 # ASSIGN : s_1_3 474 # ASSIGN : s_1_4 11 # ASSIGN : s_1_5 476 # ASSIGN : s_1_6 1070 # ASSIGN : s_1_7 444 # ASSIGN : s_1_8 454 # ASSIGN : s_1_9 0 # ASSIGN : s_2_0 439 # ASSIGN : s_2_1 344 # ASSIGN : s_2_2 30 # ASSIGN : s_2_3 837 # ASSIGN : s_2_4 185 # ASSIGN : s_2_5 359 # ASSIGN : s_2_6 12 # ASSIGN : s_2_7 15 # ASSIGN : s_2_8 186 # ASSIGN : s_2_9 1071 # ASSIGN : s_3_0 88 # ASSIGN : s_3_1 0 # ASSIGN : s_3_2 447 # ASSIGN : s_3_3 436 # ASSIGN : s_3_4 528 # ASSIGN : s_3_5 10 # ASSIGN : s_3_6 13 # ASSIGN : s_3_7 16 # ASSIGN : s_3_8 1 # ASSIGN : s_3_9 87 # ASSIGN : s_4_0 438 # ASSIGN : s_4_1 1077 # ASSIGN : s_4_2 23 # ASSIGN : s_4_3 485 # ASSIGN : s_4_4 5 # ASSIGN : s_4_5 440 # ASSIGN : s_4_6 560 # ASSIGN : s_4_7 24 # ASSIGN : s_4_8 614 # ASSIGN : s_4_9 390 # ASSIGN : s_5_0 1 # ASSIGN : s_5_1 4 # ASSIGN : s_5_2 1077 # ASSIGN : s_5_3 1075 # ASSIGN : s_5_4 477 # ASSIGN : s_5_5 3 # ASSIGN : s_5_6 478 # ASSIGN : s_5_7 566 # ASSIGN : s_5_8 429 # ASSIGN : s_5_9 286 # ASSIGN : s_6_0 84 # ASSIGN : s_6_1 1 # ASSIGN : s_6_2 29 # ASSIGN : s_6_3 540 # ASSIGN : s_6_4 216 # ASSIGN : s_6_5 798 # ASSIGN : s_6_6 16 # ASSIGN : s_6_7 17 # ASSIGN : s_6_8 457 # ASSIGN : s_6_9 94 # ASSIGN : s_7_0 2 # ASSIGN : s_7_1 374 # ASSIGN : s_7_2 595 # ASSIGN : s_7_3 1077 # ASSIGN : s_7_4 0 # ASSIGN : s_7_5 84 # ASSIGN : s_7_6 671 # ASSIGN : s_7_7 1068 # ASSIGN : s_7_8 600 # ASSIGN : s_7_9 3 # ASSIGN : s_8_0 16 # ASSIGN : s_8_1 294 # ASSIGN : s_8_2 1075 # ASSIGN : s_8_3 1076 # ASSIGN : s_8_4 6 # ASSIGN : s_8_5 21 # ASSIGN : s_8_6 22 # ASSIGN : s_8_7 1077 # ASSIGN : s_8_8 297 # ASSIGN : s_8_9 412 # ASSIGN : s_9_0 839 # ASSIGN : s_9_1 589 # ASSIGN : s_9_2 567 # ASSIGN : s_9_3 484 # ASSIGN : s_9_4 502 # ASSIGN : s_9_5 1 # ASSIGN : s_9_6 231 # ASSIGN : s_9_7 512 # ASSIGN : s_9_8 2 # ASSIGN : s_9_9 230 SHOW_RESULT 1078 END : 1078 (2 seconds) [Sun Jun 18 18:52:45 2006] SHOW_RESULT 1078 CPU : 1.72 = 1.69 + 0.03 + 0 + 0 # BOUND : makespan 1076 1078 MODIFY_CNF 1077 BEGIN : [Sun Jun 18 18:52:45 2006] MODIFY_CNF 1077 END : 172353159 bytes (0 seconds) [Sun Jun 18 18:52:45 2006] MODIFY_CNF 1077 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1077 BEGIN : [Sun Jun 18 18:52:45 2006] CMD : minisat /tmp/csp2sat12447.cnf /tmp/csp2sat12447.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 2411034 6858472 | 803678 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 88 (5 /sec) decisions : 293 (16 /sec) propagations : 1155721 (65038 /sec) conflict literals : 1109 (25.32 % deleted) Memory used : 296.34 MB CPU time : 17.77 s SATISFIABLE VERIFY_CNF 1077 END : (19 seconds) [Sun Jun 18 18:53:04 2006] VERIFY_CNF 1077 CPU : 18.92 = 0 + 0.01 + 17.94 + 0.969999999999999 # RESULT : makespan 1077 SATISFIABLE SHOW_RESULT 1077 BEGIN : [Sun Jun 18 18:53:04 2006] # ASSIGN : makespan 1077 # ASSIGN : s_0_0 1076 # ASSIGN : s_0_1 1075 # ASSIGN : s_0_2 517 # ASSIGN : s_0_3 18 # ASSIGN : s_0_4 1027 # ASSIGN : s_0_5 17 # ASSIGN : s_0_6 1074 # ASSIGN : s_0_7 454 # ASSIGN : s_0_8 1026 # ASSIGN : s_0_9 0 # ASSIGN : s_1_0 12 # ASSIGN : s_1_1 838 # ASSIGN : s_1_2 215 # ASSIGN : s_1_3 1072 # ASSIGN : s_1_4 31 # ASSIGN : s_1_5 475 # ASSIGN : s_1_6 1067 # ASSIGN : s_1_7 21 # ASSIGN : s_1_8 1074 # ASSIGN : s_1_9 212 # ASSIGN : s_2_0 439 # ASSIGN : s_2_1 344 # ASSIGN : s_2_2 32 # ASSIGN : s_2_3 837 # ASSIGN : s_2_4 30 # ASSIGN : s_2_5 359 # ASSIGN : s_2_6 26 # ASSIGN : s_2_7 22 # ASSIGN : s_2_8 186 # ASSIGN : s_2_9 1071 # ASSIGN : s_3_0 23 # ASSIGN : s_3_1 371 # ASSIGN : s_3_2 996 # ASSIGN : s_3_3 3 # ASSIGN : s_3_4 446 # ASSIGN : s_3_5 14 # ASSIGN : s_3_6 20 # ASSIGN : s_3_7 444 # ASSIGN : s_3_8 445 # ASSIGN : s_3_9 389 # ASSIGN : s_4_0 438 # ASSIGN : s_4_1 1076 # ASSIGN : s_4_2 482 # ASSIGN : s_4_3 484 # ASSIGN : s_4_4 1070 # ASSIGN : s_4_5 439 # ASSIGN : s_4_6 1013 # ASSIGN : s_4_7 24 # ASSIGN : s_4_8 550 # ASSIGN : s_4_9 390 # ASSIGN : s_5_0 419 # ASSIGN : s_5_1 3 # ASSIGN : s_5_2 483 # ASSIGN : s_5_3 1076 # ASSIGN : s_5_4 1071 # ASSIGN : s_5_5 2 # ASSIGN : s_5_6 484 # ASSIGN : s_5_7 566 # ASSIGN : s_5_8 420 # ASSIGN : s_5_9 285 # ASSIGN : s_6_0 14 # ASSIGN : s_6_1 0 # ASSIGN : s_6_2 31 # ASSIGN : s_6_3 539 # ASSIGN : s_6_4 205 # ASSIGN : s_6_5 797 # ASSIGN : s_6_6 27 # ASSIGN : s_6_7 447 # ASSIGN : s_6_8 456 # ASSIGN : s_6_9 83 # ASSIGN : s_7_0 371 # ASSIGN : s_7_1 372 # ASSIGN : s_7_2 991 # ASSIGN : s_7_3 1 # ASSIGN : s_7_4 1052 # ASSIGN : s_7_5 84 # ASSIGN : s_7_6 594 # ASSIGN : s_7_7 1068 # ASSIGN : s_7_8 1054 # ASSIGN : s_7_9 2 # ASSIGN : s_8_0 18 # ASSIGN : s_8_1 294 # ASSIGN : s_8_2 26 # ASSIGN : s_8_3 1071 # ASSIGN : s_8_4 1072 # ASSIGN : s_8_5 27 # ASSIGN : s_8_6 28 # ASSIGN : s_8_7 23 # ASSIGN : s_8_8 297 # ASSIGN : s_8_9 412 # ASSIGN : s_9_0 837 # ASSIGN : s_9_1 587 # ASSIGN : s_9_2 490 # ASSIGN : s_9_3 0 # ASSIGN : s_9_4 204 # ASSIGN : s_9_5 1 # ASSIGN : s_9_6 237 # ASSIGN : s_9_7 512 # ASSIGN : s_9_8 2 # ASSIGN : s_9_9 1076 SHOW_RESULT 1077 END : 1077 (2 seconds) [Sun Jun 18 18:53:06 2006] SHOW_RESULT 1077 CPU : 1.75000000000002 = 1.73000000000002 + 0.02 + 0 + 0 # BOUND : makespan 1076 1077 MODIFY_CNF 1076 BEGIN : [Sun Jun 18 18:53:06 2006] MODIFY_CNF 1076 END : 172353159 bytes (0 seconds) [Sun Jun 18 18:53:06 2006] MODIFY_CNF 1076 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1076 BEGIN : [Sun Jun 18 18:53:06 2006] CMD : minisat /tmp/csp2sat12447.cnf /tmp/csp2sat12447.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 2409234 6853072 | 803078 0 0 nan | 0.000 % | | 102 | 2409234 6853072 | 883385 102 1119 11.0 | 73.714 % | ============================================================================== restarts : 2 conflicts : 190 (10 /sec) decisions : 278 (15 /sec) propagations : 1898782 (103195 /sec) conflict literals : 1552 (30.65 % deleted) Memory used : 294.73 MB CPU time : 18.4 s UNSATISFIABLE VERIFY_CNF 1076 END : (19 seconds) [Sun Jun 18 18:53:25 2006] VERIFY_CNF 1076 CPU : 19.38 = 0.0100000000000477 + 0 + 18.4 + 0.970000000000001 # RESULT : makespan 1076 UNSATISFIABLE # BOUND : makespan 1077 1077 MAIN END : (515 seconds) [Sun Jun 18 18:53:25 2006] MAIN CPU : 514.58 = 300.32 + 1.74 + 200.95 + 11.57