MAIN BEGIN : [Sat Jun 3 11:14:03 2006] READ BEGIN : csp/tai03.csp [Sat Jun 3 11:14:03 2006] READ END : csp/tai03.csp (5 seconds) [Sat Jun 3 11:14:08 2006] READ CPU : 4.52 = 4.52 + 0 + 0 + 0 # BOUND : makespan 921 1711 GENERATE_CNF 1711 BEGIN : [Sat Jun 3 11:14:08 2006] GENERATE_CNF 1711 END : 389592 variables 5988519 clauses 143193212 bytes (294 seconds) [Sat Jun 3 11:19:02 2006] GENERATE_CNF 1711 CPU : 292.29 = 291.88 + 0.41 + 0 + 0 MODIFY_CNF 1316 BEGIN : [Sat Jun 3 11:19:02 2006] MODIFY_CNF 1316 END : 143193218 bytes (0 seconds) [Sat Jun 3 11:19:02 2006] MODIFY_CNF 1316 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1316 BEGIN : [Sat Jun 3 11:19:02 2006] CMD : minisat /work/tamura/csp2sat54214.cnf /work/tamura/csp2sat54214.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 2218785 6526163 | 739595 0 0 NaNQ | 0.000 % | ==============================================================================) restarts : 1 conflicts : 65 (7 /sec) decisions : 356 (40 /sec) propagations : 986210 (110448 /sec) inspects : 9382037 (1050720 /sec) conflict literals : 871 (19.94 % deleted) CPU time : 8.92915 s SATISFIABLE VERIFY_CNF 1316 END : (11 seconds) [Sat Jun 3 11:19:13 2006] VERIFY_CNF 1316 CPU : 10.59 = 0.00999999999999091 + 0.01 + 10.44 + 0.13 # RESULT : makespan 1316 SATISFIABLE SHOW_RESULT 1316 BEGIN : [Sat Jun 3 11:19:13 2006] # ASSIGN : makespan 1316 # ASSIGN : s_0_0 277 # ASSIGN : s_0_1 374 # ASSIGN : s_0_2 455 # ASSIGN : s_0_3 536 # ASSIGN : s_0_4 659 # ASSIGN : s_0_5 739 # ASSIGN : s_0_6 742 # ASSIGN : s_0_7 815 # ASSIGN : s_0_8 922 # ASSIGN : s_0_9 976 # ASSIGN : s_0_10 1042 # ASSIGN : s_0_11 1130 # ASSIGN : s_0_12 1212 # ASSIGN : s_0_13 1216 # ASSIGN : s_0_14 1228 # ASSIGN : s_1_0 29 # ASSIGN : s_1_1 112 # ASSIGN : s_1_2 170 # ASSIGN : s_1_3 280 # ASSIGN : s_1_4 295 # ASSIGN : s_1_5 388 # ASSIGN : s_1_6 486 # ASSIGN : s_1_7 538 # ASSIGN : s_1_8 841 # ASSIGN : s_1_9 906 # ASSIGN : s_1_10 1003 # ASSIGN : s_1_11 1041 # ASSIGN : s_1_12 1071 # ASSIGN : s_1_13 1076 # ASSIGN : s_1_14 1277 # ASSIGN : s_2_0 276 # ASSIGN : s_2_1 364 # ASSIGN : s_2_2 411 # ASSIGN : s_2_3 530 # ASSIGN : s_2_4 598 # ASSIGN : s_2_5 668 # ASSIGN : s_2_6 746 # ASSIGN : s_2_7 879 # ASSIGN : s_2_8 994 # ASSIGN : s_2_9 1013 # ASSIGN : s_2_10 1046 # ASSIGN : s_2_11 1094 # ASSIGN : s_2_12 1187 # ASSIGN : s_2_13 1286 # ASSIGN : s_2_14 1295 # ASSIGN : s_3_0 40 # ASSIGN : s_3_1 469 # ASSIGN : s_3_2 552 # ASSIGN : s_3_3 711 # ASSIGN : s_3_4 741 # ASSIGN : s_3_5 837 # ASSIGN : s_3_6 868 # ASSIGN : s_3_7 888 # ASSIGN : s_3_8 934 # ASSIGN : s_3_9 975 # ASSIGN : s_3_10 1030 # ASSIGN : s_3_11 1057 # ASSIGN : s_3_12 1131 # ASSIGN : s_3_13 1223 # ASSIGN : s_3_14 1241 # ASSIGN : s_4_0 76 # ASSIGN : s_4_1 124 # ASSIGN : s_4_2 173 # ASSIGN : s_4_3 183 # ASSIGN : s_4_4 226 # ASSIGN : s_4_5 445 # ASSIGN : s_4_6 517 # ASSIGN : s_4_7 549 # ASSIGN : s_4_8 614 # ASSIGN : s_4_9 651 # ASSIGN : s_4_10 710 # ASSIGN : s_4_11 752 # ASSIGN : s_4_12 914 # ASSIGN : s_4_13 987 # ASSIGN : s_4_14 1090 # ASSIGN : s_5_0 68 # ASSIGN : s_5_1 151 # ASSIGN : s_5_2 231 # ASSIGN : s_5_3 261 # ASSIGN : s_5_4 339 # ASSIGN : s_5_5 426 # ASSIGN : s_5_6 520 # ASSIGN : s_5_7 556 # ASSIGN : s_5_8 632 # ASSIGN : s_5_9 694 # ASSIGN : s_5_10 724 # ASSIGN : s_5_11 780 # ASSIGN : s_5_12 870 # ASSIGN : s_5_13 902 # ASSIGN : s_5_14 954 # ASSIGN : s_6_0 24 # ASSIGN : s_6_1 53 # ASSIGN : s_6_2 145 # ASSIGN : s_6_3 166 # ASSIGN : s_6_4 247 # ASSIGN : s_6_5 264 # ASSIGN : s_6_6 310 # ASSIGN : s_6_7 324 # ASSIGN : s_6_8 346 # ASSIGN : s_6_9 362 # ASSIGN : s_6_10 480 # ASSIGN : s_6_11 640 # ASSIGN : s_6_12 665 # ASSIGN : s_6_13 955 # ASSIGN : s_6_14 993 # ASSIGN : s_7_0 73 # ASSIGN : s_7_1 85 # ASSIGN : s_7_2 159 # ASSIGN : s_7_3 163 # ASSIGN : s_7_4 170 # ASSIGN : s_7_5 185 # ASSIGN : s_7_6 257 # ASSIGN : s_7_7 307 # ASSIGN : s_7_8 1018 # ASSIGN : s_7_9 1067 # ASSIGN : s_7_10 1092 # ASSIGN : s_7_11 1110 # ASSIGN : s_7_12 1165 # ASSIGN : s_7_13 1170 # ASSIGN : s_7_14 1289 # ASSIGN : s_8_0 345 # ASSIGN : s_8_1 458 # ASSIGN : s_8_2 471 # ASSIGN : s_8_3 504 # ASSIGN : s_8_4 551 # ASSIGN : s_8_5 637 # ASSIGN : s_8_6 672 # ASSIGN : s_8_7 769 # ASSIGN : s_8_8 817 # ASSIGN : s_8_9 842 # ASSIGN : s_8_10 882 # ASSIGN : s_8_11 1004 # ASSIGN : s_8_12 1026 # ASSIGN : s_8_13 1215 # ASSIGN : s_8_14 1300 # ASSIGN : s_9_0 13 # ASSIGN : s_9_1 40 # ASSIGN : s_9_2 44 # ASSIGN : s_9_3 79 # ASSIGN : s_9_4 159 # ASSIGN : s_9_5 208 # ASSIGN : s_9_6 254 # ASSIGN : s_9_7 338 # ASSIGN : s_9_8 384 # ASSIGN : s_9_9 481 # ASSIGN : s_9_10 574 # ASSIGN : s_9_11 592 # ASSIGN : s_9_12 615 # ASSIGN : s_9_13 763 # ASSIGN : s_9_14 1107 # ASSIGN : s_10_0 0 # ASSIGN : s_10_1 36 # ASSIGN : s_10_2 193 # ASSIGN : s_10_3 274 # ASSIGN : s_10_4 341 # ASSIGN : s_10_5 414 # ASSIGN : s_10_6 487 # ASSIGN : s_10_7 678 # ASSIGN : s_10_8 758 # ASSIGN : s_10_9 840 # ASSIGN : s_10_10 991 # ASSIGN : s_10_11 1087 # ASSIGN : s_10_12 1111 # ASSIGN : s_10_13 1165 # ASSIGN : s_10_14 1257 # ASSIGN : s_11_0 235 # ASSIGN : s_11_1 313 # ASSIGN : s_11_2 419 # ASSIGN : s_11_3 537 # ASSIGN : s_11_4 580 # ASSIGN : s_11_5 581 # ASSIGN : s_11_6 712 # ASSIGN : s_11_7 825 # ASSIGN : s_11_8 874 # ASSIGN : s_11_9 1112 # ASSIGN : s_11_10 1138 # ASSIGN : s_11_11 1217 # ASSIGN : s_11_12 1226 # ASSIGN : s_11_13 1250 # ASSIGN : s_11_14 1274 # ASSIGN : s_12_0 275 # ASSIGN : s_12_1 345 # ASSIGN : s_12_2 431 # ASSIGN : s_12_3 482 # ASSIGN : s_12_4 553 # ASSIGN : s_12_5 636 # ASSIGN : s_12_6 701 # ASSIGN : s_12_7 747 # ASSIGN : s_12_8 764 # ASSIGN : s_12_9 863 # ASSIGN : s_12_10 877 # ASSIGN : s_12_11 965 # ASSIGN : s_12_12 1029 # ASSIGN : s_12_13 1116 # ASSIGN : s_12_14 1299 # ASSIGN : s_13_0 121 # ASSIGN : s_13_1 131 # ASSIGN : s_13_2 217 # ASSIGN : s_13_3 584 # ASSIGN : s_13_4 647 # ASSIGN : s_13_5 708 # ASSIGN : s_13_6 770 # ASSIGN : s_13_7 845 # ASSIGN : s_13_8 935 # ASSIGN : s_13_9 975 # ASSIGN : s_13_10 1052 # ASSIGN : s_13_11 1060 # ASSIGN : s_13_12 1087 # ASSIGN : s_13_13 1183 # ASSIGN : s_13_14 1252 # ASSIGN : s_14_0 0 # ASSIGN : s_14_1 73 # ASSIGN : s_14_2 85 # ASSIGN : s_14_3 99 # ASSIGN : s_14_4 237 # ASSIGN : s_14_5 240 # ASSIGN : s_14_6 287 # ASSIGN : s_14_7 371 # ASSIGN : s_14_8 464 # ASSIGN : s_14_9 523 # ASSIGN : s_14_10 657 # ASSIGN : s_14_11 788 # ASSIGN : s_14_12 875 # ASSIGN : s_14_13 1102 # ASSIGN : s_14_14 1241 SHOW_RESULT 1316 END : 1316 (1 seconds) [Sat Jun 3 11:19:14 2006] SHOW_RESULT 1316 CPU : 1.06999999999999 = 1.06999999999999 + 0 + 0 + 0 # BOUND : makespan 921 1316 MODIFY_CNF 1118 BEGIN : [Sat Jun 3 11:19:14 2006] MODIFY_CNF 1118 END : 143193218 bytes (0 seconds) [Sat Jun 3 11:19:14 2006] MODIFY_CNF 1118 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1118 BEGIN : [Sat Jun 3 11:19:14 2006] CMD : minisat /work/tamura/csp2sat54214.cnf /work/tamura/csp2sat54214.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1363576 4005718 | 454525 0 0 NaNQ | 0.000 % | | 100 | 1363576 4005718 | 499977 95 499 5.3 | 78.198 % | ==============================================================================) restarts : 2 conflicts : 108 (11 /sec) decisions : 142 (15 /sec) propagations : 1331117 (140054 /sec) inspects : 8041045 (846044 /sec) conflict literals : 533 (26.99 % deleted) CPU time : 9.50428 s UNSATISFIABLE VERIFY_CNF 1118 END : (11 seconds) [Sat Jun 3 11:19:25 2006] VERIFY_CNF 1118 CPU : 11.08 = 0.00999999999999091 + 0.03 + 10.53 + 0.51 # RESULT : makespan 1118 UNSATISFIABLE # BOUND : makespan 1119 1316 MODIFY_CNF 1217 BEGIN : [Sat Jun 3 11:19:25 2006] MODIFY_CNF 1217 END : 143193218 bytes (0 seconds) [Sat Jun 3 11:19:25 2006] MODIFY_CNF 1217 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1217 BEGIN : [Sat Jun 3 11:19:25 2006] CMD : minisat /work/tamura/csp2sat54214.cnf /work/tamura/csp2sat54214.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1790431 5263663 | 596810 0 0 NaNQ | 0.000 % | | 101 | 1790431 5263663 | 656491 101 1145 11.3 | 72.050 % | | 251 | 1790431 5263663 | 722140 251 2497 9.9 | 72.050 % | | 477 | 1790431 5263663 | 794354 477 5816 12.2 | 72.050 % | | 815 | 1790431 5263663 | 873789 815 9347 11.5 | 72.050 % | | 1323 | 1790431 5263663 | 961168 1323 15747 11.9 | 72.050 % | | 2083 | 1790431 5263663 | 1057285 2083 26716 12.8 | 72.050 % | | 3222 | 1790431 5263663 | 1163013 3222 43015 13.4 | 72.050 % | | 4930 | 1790431 5263663 | 1279315 4930 66485 13.5 | 72.050 % | | 7492 | 1790431 5263663 | 1407246 7492 117622 15.7 | 72.050 % | | 11336 | 1790431 5263663 | 1547971 11336 186216 16.4 | 72.050 % | | 17105 | 1790431 5263663 | 1702768 17105 296617 17.3 | 72.050 % | ==============================================================================) restarts : 12 conflicts : 17742 (149 /sec) decisions : 24967 (209 /sec) propagations : 216807063 (1816845 /sec) inspects : 1686574419 (14133506 /sec) conflict literals : 303482 (35.25 % deleted) CPU time : 119.332 s UNSATISFIABLE VERIFY_CNF 1217 END : (121 seconds) [Sat Jun 3 11:21:26 2006] VERIFY_CNF 1217 CPU : 120.75 = 0 + 0.02 + 120.5 + 0.23 # RESULT : makespan 1217 UNSATISFIABLE # BOUND : makespan 1218 1316 MODIFY_CNF 1267 BEGIN : [Sat Jun 3 11:21:26 2006] MODIFY_CNF 1267 END : 143193218 bytes (0 seconds) [Sat Jun 3 11:21:26 2006] MODIFY_CNF 1267 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1267 BEGIN : [Sat Jun 3 11:21:26 2006] CMD : minisat /work/tamura/csp2sat54214.cnf /work/tamura/csp2sat54214.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 2009658 5909942 | 669886 0 0 NaNQ | 0.000 % | | 102 | 2009658 5909942 | 736874 102 1368 13.4 | 69.109 % | | 252 | 2009658 5909942 | 810562 252 3985 15.8 | 69.109 % | | 478 | 2009658 5909942 | 891618 478 7218 15.1 | 69.109 % | | 815 | 2009658 5909942 | 980780 815 14054 17.2 | 69.109 % | | 1321 | 2009658 5909942 | 1078858 1321 22995 17.4 | 69.109 % | | 2080 | 2009658 5909942 | 1186743 2080 38397 18.5 | 69.109 % | ==============================================================================) restarts : 7 conflicts : 2644 (105 /sec) decisions : 4803 (191 /sec) propagations : 29415428 (1169071 /sec) inspects : 274960137 (10927871 /sec) conflict literals : 53215 (20.82 % deleted) CPU time : 25.1614 s SATISFIABLE VERIFY_CNF 1267 END : (27 seconds) [Sat Jun 3 11:21:53 2006] VERIFY_CNF 1267 CPU : 26.76 = 0 + 0.01 + 26.59 + 0.16 # RESULT : makespan 1267 SATISFIABLE SHOW_RESULT 1267 BEGIN : [Sat Jun 3 11:21:53 2006] # ASSIGN : makespan 1267 # ASSIGN : s_0_0 24 # ASSIGN : s_0_1 93 # ASSIGN : s_0_2 223 # ASSIGN : s_0_3 316 # ASSIGN : s_0_4 486 # ASSIGN : s_0_5 566 # ASSIGN : s_0_6 569 # ASSIGN : s_0_7 607 # ASSIGN : s_0_8 724 # ASSIGN : s_0_9 780 # ASSIGN : s_0_10 880 # ASSIGN : s_0_11 984 # ASSIGN : s_0_12 1093 # ASSIGN : s_0_13 1167 # ASSIGN : s_0_14 1179 # ASSIGN : s_1_0 69 # ASSIGN : s_1_1 179 # ASSIGN : s_1_2 257 # ASSIGN : s_1_3 317 # ASSIGN : s_1_4 332 # ASSIGN : s_1_5 535 # ASSIGN : s_1_6 640 # ASSIGN : s_1_7 780 # ASSIGN : s_1_8 983 # ASSIGN : s_1_9 1005 # ASSIGN : s_1_10 1090 # ASSIGN : s_1_11 1116 # ASSIGN : s_1_12 1146 # ASSIGN : s_1_13 1151 # ASSIGN : s_1_14 1245 # ASSIGN : s_2_0 115 # ASSIGN : s_2_1 177 # ASSIGN : s_2_2 224 # ASSIGN : s_2_3 324 # ASSIGN : s_2_4 378 # ASSIGN : s_2_5 477 # ASSIGN : s_2_6 611 # ASSIGN : s_2_7 682 # ASSIGN : s_2_8 778 # ASSIGN : s_2_9 797 # ASSIGN : s_2_10 830 # ASSIGN : s_2_11 874 # ASSIGN : s_2_12 945 # ASSIGN : s_2_13 1199 # ASSIGN : s_2_14 1208 # ASSIGN : s_3_0 115 # ASSIGN : s_3_1 166 # ASSIGN : s_3_2 252 # ASSIGN : s_3_3 334 # ASSIGN : s_3_4 364 # ASSIGN : s_3_5 582 # ASSIGN : s_3_6 671 # ASSIGN : s_3_7 746 # ASSIGN : s_3_8 772 # ASSIGN : s_3_9 813 # ASSIGN : s_3_10 868 # ASSIGN : s_3_11 1087 # ASSIGN : s_3_12 1097 # ASSIGN : s_3_13 1189 # ASSIGN : s_3_14 1192 # ASSIGN : s_4_0 6 # ASSIGN : s_4_1 47 # ASSIGN : s_4_2 96 # ASSIGN : s_4_3 140 # ASSIGN : s_4_4 183 # ASSIGN : s_4_5 344 # ASSIGN : s_4_6 416 # ASSIGN : s_4_7 575 # ASSIGN : s_4_8 703 # ASSIGN : s_4_9 740 # ASSIGN : s_4_10 830 # ASSIGN : s_4_11 862 # ASSIGN : s_4_12 897 # ASSIGN : s_4_13 970 # ASSIGN : s_4_14 1112 # ASSIGN : s_5_0 144 # ASSIGN : s_5_1 227 # ASSIGN : s_5_2 281 # ASSIGN : s_5_3 287 # ASSIGN : s_5_4 300 # ASSIGN : s_5_5 387 # ASSIGN : s_5_6 481 # ASSIGN : s_5_7 517 # ASSIGN : s_5_8 593 # ASSIGN : s_5_9 639 # ASSIGN : s_5_10 669 # ASSIGN : s_5_11 725 # ASSIGN : s_5_12 787 # ASSIGN : s_5_13 819 # ASSIGN : s_5_14 873 # ASSIGN : s_6_0 70 # ASSIGN : s_6_1 99 # ASSIGN : s_6_2 209 # ASSIGN : s_6_3 230 # ASSIGN : s_6_4 304 # ASSIGN : s_6_5 321 # ASSIGN : s_6_6 467 # ASSIGN : s_6_7 496 # ASSIGN : s_6_8 566 # ASSIGN : s_6_9 590 # ASSIGN : s_6_10 697 # ASSIGN : s_6_11 1022 # ASSIGN : s_6_12 1066 # ASSIGN : s_6_13 1165 # ASSIGN : s_6_14 1203 # ASSIGN : s_7_0 106 # ASSIGN : s_7_1 118 # ASSIGN : s_7_2 296 # ASSIGN : s_7_3 338 # ASSIGN : s_7_4 405 # ASSIGN : s_7_5 463 # ASSIGN : s_7_6 525 # ASSIGN : s_7_7 686 # ASSIGN : s_7_8 821 # ASSIGN : s_7_9 871 # ASSIGN : s_7_10 915 # ASSIGN : s_7_11 933 # ASSIGN : s_7_12 993 # ASSIGN : s_7_13 1041 # ASSIGN : s_7_14 1240 # ASSIGN : s_8_0 11 # ASSIGN : s_8_1 80 # ASSIGN : s_8_2 127 # ASSIGN : s_8_3 177 # ASSIGN : s_8_4 410 # ASSIGN : s_8_5 684 # ASSIGN : s_8_6 722 # ASSIGN : s_8_7 880 # ASSIGN : s_8_8 928 # ASSIGN : s_8_9 953 # ASSIGN : s_8_10 1015 # ASSIGN : s_8_11 1109 # ASSIGN : s_8_12 1131 # ASSIGN : s_8_13 1192 # ASSIGN : s_8_14 1251 # ASSIGN : s_9_0 6 # ASSIGN : s_9_1 33 # ASSIGN : s_9_2 37 # ASSIGN : s_9_3 72 # ASSIGN : s_9_4 152 # ASSIGN : s_9_5 211 # ASSIGN : s_9_6 257 # ASSIGN : s_9_7 341 # ASSIGN : s_9_8 421 # ASSIGN : s_9_9 521 # ASSIGN : s_9_10 593 # ASSIGN : s_9_11 669 # ASSIGN : s_9_12 692 # ASSIGN : s_9_13 788 # ASSIGN : s_9_14 1228 # ASSIGN : s_10_0 192 # ASSIGN : s_10_1 228 # ASSIGN : s_10_2 257 # ASSIGN : s_10_3 368 # ASSIGN : s_10_4 435 # ASSIGN : s_10_5 598 # ASSIGN : s_10_6 620 # ASSIGN : s_10_7 674 # ASSIGN : s_10_8 715 # ASSIGN : s_10_9 797 # ASSIGN : s_10_10 832 # ASSIGN : s_10_11 998 # ASSIGN : s_10_12 1005 # ASSIGN : s_10_13 1059 # ASSIGN : s_10_14 1229 # ASSIGN : s_11_0 49 # ASSIGN : s_11_1 165 # ASSIGN : s_11_2 259 # ASSIGN : s_11_3 325 # ASSIGN : s_11_4 420 # ASSIGN : s_11_5 421 # ASSIGN : s_11_6 517 # ASSIGN : s_11_7 659 # ASSIGN : s_11_8 708 # ASSIGN : s_11_9 870 # ASSIGN : s_11_10 896 # ASSIGN : s_11_11 975 # ASSIGN : s_11_12 984 # ASSIGN : s_11_13 1008 # ASSIGN : s_11_14 1051 # ASSIGN : s_12_0 127 # ASSIGN : s_12_1 201 # ASSIGN : s_12_2 511 # ASSIGN : s_12_3 565 # ASSIGN : s_12_4 603 # ASSIGN : s_12_5 686 # ASSIGN : s_12_6 769 # ASSIGN : s_12_7 781 # ASSIGN : s_12_8 798 # ASSIGN : s_12_9 897 # ASSIGN : s_12_10 911 # ASSIGN : s_12_11 968 # ASSIGN : s_12_12 1032 # ASSIGN : s_12_13 1096 # ASSIGN : s_12_14 1228 # ASSIGN : s_13_0 3 # ASSIGN : s_13_1 13 # ASSIGN : s_13_2 304 # ASSIGN : s_13_3 397 # ASSIGN : s_13_4 460 # ASSIGN : s_13_5 549 # ASSIGN : s_13_6 611 # ASSIGN : s_13_7 691 # ASSIGN : s_13_8 790 # ASSIGN : s_13_9 898 # ASSIGN : s_13_10 975 # ASSIGN : s_13_11 988 # ASSIGN : s_13_12 1035 # ASSIGN : s_13_13 1134 # ASSIGN : s_13_14 1203 # ASSIGN : s_14_0 42 # ASSIGN : s_14_1 148 # ASSIGN : s_14_2 160 # ASSIGN : s_14_3 174 # ASSIGN : s_14_4 245 # ASSIGN : s_14_5 248 # ASSIGN : s_14_6 295 # ASSIGN : s_14_7 379 # ASSIGN : s_14_8 482 # ASSIGN : s_14_9 555 # ASSIGN : s_14_10 613 # ASSIGN : s_14_11 846 # ASSIGN : s_14_12 1034 # ASSIGN : s_14_13 1124 # ASSIGN : s_14_14 1192 SHOW_RESULT 1267 END : 1267 (1 seconds) [Sat Jun 3 11:21:54 2006] SHOW_RESULT 1267 CPU : 1.11000000000002 = 1.10000000000002 + 0.01 + 0 + 0 # BOUND : makespan 1218 1267 MODIFY_CNF 1242 BEGIN : [Sat Jun 3 11:21:54 2006] MODIFY_CNF 1242 END : 143193218 bytes (0 seconds) [Sat Jun 3 11:21:54 2006] MODIFY_CNF 1242 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1242 BEGIN : [Sat Jun 3 11:21:54 2006] CMD : minisat /work/tamura/csp2sat54214.cnf /work/tamura/csp2sat54214.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1899410 5584896 | 633136 0 0 NaNQ | 0.000 % | | 101 | 1899410 5584896 | 696449 101 1192 11.8 | 70.578 % | | 252 | 1899410 5584896 | 766094 252 3047 12.1 | 70.578 % | | 478 | 1899410 5584896 | 842704 478 5732 12.0 | 70.578 % | | 816 | 1899410 5584896 | 926974 816 11433 14.0 | 70.578 % | | 1322 | 1899410 5584896 | 1019671 1322 17699 13.4 | 70.578 % | | 2082 | 1899410 5584896 | 1121639 2082 29925 14.4 | 70.578 % | | 3222 | 1899410 5584896 | 1233802 3222 47374 14.7 | 70.578 % | | 4930 | 1899410 5584896 | 1357183 4930 83294 16.9 | 70.578 % | | 7492 | 1899410 5584896 | 1492901 7492 120491 16.1 | 70.578 % | | 11336 | 1899410 5584896 | 1642191 11336 196404 17.3 | 70.578 % | | 17102 | 1899410 5584896 | 1806410 17102 312153 18.3 | 70.578 % | | 25751 | 1899410 5584896 | 1987051 25751 497783 19.3 | 70.578 % | ==============================================================================) restarts : 13 conflicts : 27842 (137 /sec) decisions : 39322 (194 /sec) propagations : 352337080 (1739261 /sec) inspects : 2993347815 (14776228 /sec) conflict literals : 533842 (35.85 % deleted) CPU time : 202.579 s SATISFIABLE VERIFY_CNF 1242 END : (205 seconds) [Sat Jun 3 11:25:19 2006] VERIFY_CNF 1242 CPU : 204.57 = 0.00999999999999091 + 0.03 + 203.97 + 0.56 # RESULT : makespan 1242 SATISFIABLE SHOW_RESULT 1242 BEGIN : [Sat Jun 3 11:25:19 2006] # ASSIGN : makespan 1242 # ASSIGN : s_0_0 16 # ASSIGN : s_0_1 88 # ASSIGN : s_0_2 260 # ASSIGN : s_0_3 442 # ASSIGN : s_0_4 538 # ASSIGN : s_0_5 618 # ASSIGN : s_0_6 643 # ASSIGN : s_0_7 681 # ASSIGN : s_0_8 743 # ASSIGN : s_0_9 797 # ASSIGN : s_0_10 952 # ASSIGN : s_0_11 1040 # ASSIGN : s_0_12 1122 # ASSIGN : s_0_13 1142 # ASSIGN : s_0_14 1154 # ASSIGN : s_1_0 151 # ASSIGN : s_1_1 272 # ASSIGN : s_1_2 324 # ASSIGN : s_1_3 398 # ASSIGN : s_1_4 413 # ASSIGN : s_1_5 574 # ASSIGN : s_1_6 659 # ASSIGN : s_1_7 761 # ASSIGN : s_1_8 817 # ASSIGN : s_1_9 839 # ASSIGN : s_1_10 924 # ASSIGN : s_1_11 960 # ASSIGN : s_1_12 990 # ASSIGN : s_1_13 995 # ASSIGN : s_1_14 1084 # ASSIGN : s_2_0 54 # ASSIGN : s_2_1 138 # ASSIGN : s_2_2 185 # ASSIGN : s_2_3 301 # ASSIGN : s_2_4 357 # ASSIGN : s_2_5 465 # ASSIGN : s_2_6 547 # ASSIGN : s_2_7 618 # ASSIGN : s_2_8 714 # ASSIGN : s_2_9 733 # ASSIGN : s_2_10 766 # ASSIGN : s_2_11 810 # ASSIGN : s_2_12 881 # ASSIGN : s_2_13 1174 # ASSIGN : s_2_14 1183 # ASSIGN : s_3_0 16 # ASSIGN : s_3_1 49 # ASSIGN : s_3_2 246 # ASSIGN : s_3_3 336 # ASSIGN : s_3_4 366 # ASSIGN : s_3_5 462 # ASSIGN : s_3_6 740 # ASSIGN : s_3_7 751 # ASSIGN : s_3_8 809 # ASSIGN : s_3_9 885 # ASSIGN : s_3_10 940 # ASSIGN : s_3_11 964 # ASSIGN : s_3_12 974 # ASSIGN : s_3_13 1066 # ASSIGN : s_3_14 1069 # ASSIGN : s_4_0 2 # ASSIGN : s_4_1 38 # ASSIGN : s_4_2 87 # ASSIGN : s_4_3 97 # ASSIGN : s_4_4 140 # ASSIGN : s_4_5 209 # ASSIGN : s_4_6 338 # ASSIGN : s_4_7 487 # ASSIGN : s_4_8 552 # ASSIGN : s_4_9 663 # ASSIGN : s_4_10 720 # ASSIGN : s_4_11 766 # ASSIGN : s_4_12 777 # ASSIGN : s_4_13 850 # ASSIGN : s_4_14 1230 # ASSIGN : s_5_0 126 # ASSIGN : s_5_1 334 # ASSIGN : s_5_2 452 # ASSIGN : s_5_3 458 # ASSIGN : s_5_4 471 # ASSIGN : s_5_5 621 # ASSIGN : s_5_6 715 # ASSIGN : s_5_7 779 # ASSIGN : s_5_8 863 # ASSIGN : s_5_9 909 # ASSIGN : s_5_10 939 # ASSIGN : s_5_11 1015 # ASSIGN : s_5_12 1086 # ASSIGN : s_5_13 1118 # ASSIGN : s_5_14 1170 # ASSIGN : s_6_0 14 # ASSIGN : s_6_1 43 # ASSIGN : s_6_2 355 # ASSIGN : s_6_3 376 # ASSIGN : s_6_4 403 # ASSIGN : s_6_5 479 # ASSIGN : s_6_6 544 # ASSIGN : s_6_7 558 # ASSIGN : s_6_8 573 # ASSIGN : s_6_9 589 # ASSIGN : s_6_10 638 # ASSIGN : s_6_11 858 # ASSIGN : s_6_12 932 # ASSIGN : s_6_13 1101 # ASSIGN : s_6_14 1178 # ASSIGN : s_7_0 75 # ASSIGN : s_7_1 211 # ASSIGN : s_7_2 285 # ASSIGN : s_7_3 323 # ASSIGN : s_7_4 326 # ASSIGN : s_7_5 341 # ASSIGN : s_7_6 825 # ASSIGN : s_7_7 922 # ASSIGN : s_7_8 992 # ASSIGN : s_7_9 1041 # ASSIGN : s_7_10 1066 # ASSIGN : s_7_11 1084 # ASSIGN : s_7_12 1139 # ASSIGN : s_7_13 1144 # ASSIGN : s_7_14 1215 # ASSIGN : s_8_0 6 # ASSIGN : s_8_1 75 # ASSIGN : s_8_2 246 # ASSIGN : s_8_3 279 # ASSIGN : s_8_4 336 # ASSIGN : s_8_5 749 # ASSIGN : s_8_6 780 # ASSIGN : s_8_7 877 # ASSIGN : s_8_8 925 # ASSIGN : s_8_9 950 # ASSIGN : s_8_10 990 # ASSIGN : s_8_11 1084 # ASSIGN : s_8_12 1106 # ASSIGN : s_8_13 1167 # ASSIGN : s_8_14 1226 # ASSIGN : s_9_0 131 # ASSIGN : s_9_1 158 # ASSIGN : s_9_2 162 # ASSIGN : s_9_3 197 # ASSIGN : s_9_4 277 # ASSIGN : s_9_5 326 # ASSIGN : s_9_6 372 # ASSIGN : s_9_7 456 # ASSIGN : s_9_8 502 # ASSIGN : s_9_9 598 # ASSIGN : s_9_10 670 # ASSIGN : s_9_11 688 # ASSIGN : s_9_12 711 # ASSIGN : s_9_13 807 # ASSIGN : s_9_14 1203 # ASSIGN : s_10_0 85 # ASSIGN : s_10_1 121 # ASSIGN : s_10_2 191 # ASSIGN : s_10_3 328 # ASSIGN : s_10_4 395 # ASSIGN : s_10_5 522 # ASSIGN : s_10_6 552 # ASSIGN : s_10_7 603 # ASSIGN : s_10_8 626 # ASSIGN : s_10_9 708 # ASSIGN : s_10_10 743 # ASSIGN : s_10_11 1008 # ASSIGN : s_10_12 1058 # ASSIGN : s_10_13 1112 # ASSIGN : s_10_14 1204 # ASSIGN : s_11_0 9 # ASSIGN : s_11_1 87 # ASSIGN : s_11_2 145 # ASSIGN : s_11_3 234 # ASSIGN : s_11_4 278 # ASSIGN : s_11_5 281 # ASSIGN : s_11_6 337 # ASSIGN : s_11_7 422 # ASSIGN : s_11_8 493 # ASSIGN : s_11_9 859 # ASSIGN : s_11_10 885 # ASSIGN : s_11_11 1031 # ASSIGN : s_11_12 1042 # ASSIGN : s_11_13 1077 # ASSIGN : s_11_14 1125 # ASSIGN : s_12_0 0 # ASSIGN : s_12_1 45 # ASSIGN : s_12_2 131 # ASSIGN : s_12_3 169 # ASSIGN : s_12_4 207 # ASSIGN : s_12_5 290 # ASSIGN : s_12_6 326 # ASSIGN : s_12_7 427 # ASSIGN : s_12_8 444 # ASSIGN : s_12_9 543 # ASSIGN : s_12_10 587 # ASSIGN : s_12_11 644 # ASSIGN : s_12_12 752 # ASSIGN : s_12_13 875 # ASSIGN : s_12_14 971 # ASSIGN : s_13_0 179 # ASSIGN : s_13_1 200 # ASSIGN : s_13_2 371 # ASSIGN : s_13_3 464 # ASSIGN : s_13_4 527 # ASSIGN : s_13_5 588 # ASSIGN : s_13_6 650 # ASSIGN : s_13_7 725 # ASSIGN : s_13_8 815 # ASSIGN : s_13_9 855 # ASSIGN : s_13_10 953 # ASSIGN : s_13_11 961 # ASSIGN : s_13_12 988 # ASSIGN : s_13_13 1109 # ASSIGN : s_13_14 1178 # ASSIGN : s_14_0 116 # ASSIGN : s_14_1 189 # ASSIGN : s_14_2 201 # ASSIGN : s_14_3 215 # ASSIGN : s_14_4 286 # ASSIGN : s_14_5 289 # ASSIGN : s_14_6 336 # ASSIGN : s_14_7 420 # ASSIGN : s_14_8 504 # ASSIGN : s_14_9 557 # ASSIGN : s_14_10 615 # ASSIGN : s_14_11 710 # ASSIGN : s_14_12 819 # ASSIGN : s_14_13 1001 # ASSIGN : s_14_14 1167 SHOW_RESULT 1242 END : 1242 (1 seconds) [Sat Jun 3 11:25:20 2006] SHOW_RESULT 1242 CPU : 1.10000000000002 = 1.10000000000002 + 0 + 0 + 0 # BOUND : makespan 1218 1242 MODIFY_CNF 1230 BEGIN : [Sat Jun 3 11:25:20 2006] MODIFY_CNF 1230 END : 143193218 bytes (0 seconds) [Sat Jun 3 11:25:20 2006] MODIFY_CNF 1230 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1230 BEGIN : [Sat Jun 3 11:25:20 2006] CMD : minisat /work/tamura/csp2sat54214.cnf /work/tamura/csp2sat54214.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1845092 5424680 | 615030 0 0 NaNQ | 0.000 % | | 100 | 1845092 5424680 | 676533 100 1200 12.0 | 71.285 % | | 250 | 1845092 5424680 | 744186 250 3207 12.8 | 71.285 % | | 475 | 1845092 5424680 | 818604 475 5010 10.5 | 71.285 % | | 812 | 1845092 5424680 | 900465 812 9029 11.1 | 71.285 % | | 1318 | 1845092 5424680 | 990511 1318 15472 11.7 | 71.285 % | | 2077 | 1845092 5424680 | 1089563 2077 27528 13.3 | 71.285 % | | 3217 | 1845092 5424680 | 1198519 3217 45103 14.0 | 71.285 % | | 4927 | 1845092 5424680 | 1318371 4927 74457 15.1 | 71.285 % | | 7489 | 1835535 5396299 | 1450208 6603 100792 15.3 | 71.361 % | ==============================================================================) restarts : 10 conflicts : 8622 (138 /sec) decisions : 12905 (207 /sec) propagations : 104987318 (1684419 /sec) inspects : 831814380 (13345652 /sec) conflict literals : 139931 (31.53 % deleted) CPU time : 62.3285 s SATISFIABLE VERIFY_CNF 1230 END : (65 seconds) [Sat Jun 3 11:26:25 2006] VERIFY_CNF 1230 CPU : 63.9 = 0 + 0.03 + 63.71 + 0.16 # RESULT : makespan 1230 SATISFIABLE SHOW_RESULT 1230 BEGIN : [Sat Jun 3 11:26:25 2006] # ASSIGN : makespan 1230 # ASSIGN : s_0_0 12 # ASSIGN : s_0_1 81 # ASSIGN : s_0_2 229 # ASSIGN : s_0_3 310 # ASSIGN : s_0_4 619 # ASSIGN : s_0_5 699 # ASSIGN : s_0_6 702 # ASSIGN : s_0_7 767 # ASSIGN : s_0_8 829 # ASSIGN : s_0_9 883 # ASSIGN : s_0_10 957 # ASSIGN : s_0_11 1045 # ASSIGN : s_0_12 1127 # ASSIGN : s_0_13 1130 # ASSIGN : s_0_14 1142 # ASSIGN : s_1_0 26 # ASSIGN : s_1_1 244 # ASSIGN : s_1_2 295 # ASSIGN : s_1_3 342 # ASSIGN : s_1_4 357 # ASSIGN : s_1_5 559 # ASSIGN : s_1_6 635 # ASSIGN : s_1_7 687 # ASSIGN : s_1_8 713 # ASSIGN : s_1_9 735 # ASSIGN : s_1_10 911 # ASSIGN : s_1_11 948 # ASSIGN : s_1_12 978 # ASSIGN : s_1_13 983 # ASSIGN : s_1_14 1072 # ASSIGN : s_2_0 116 # ASSIGN : s_2_1 178 # ASSIGN : s_2_2 225 # ASSIGN : s_2_3 318 # ASSIGN : s_2_4 372 # ASSIGN : s_2_5 413 # ASSIGN : s_2_6 520 # ASSIGN : s_2_7 591 # ASSIGN : s_2_8 702 # ASSIGN : s_2_9 721 # ASSIGN : s_2_10 754 # ASSIGN : s_2_11 798 # ASSIGN : s_2_12 869 # ASSIGN : s_2_13 1162 # ASSIGN : s_2_14 1171 # ASSIGN : s_3_0 0 # ASSIGN : s_3_1 33 # ASSIGN : s_3_2 244 # ASSIGN : s_3_3 324 # ASSIGN : s_3_4 354 # ASSIGN : s_3_5 450 # ASSIGN : s_3_6 481 # ASSIGN : s_3_7 552 # ASSIGN : s_3_8 578 # ASSIGN : s_3_9 658 # ASSIGN : s_3_10 743 # ASSIGN : s_3_11 755 # ASSIGN : s_3_12 820 # ASSIGN : s_3_13 986 # ASSIGN : s_3_14 989 # ASSIGN : s_4_0 7 # ASSIGN : s_4_1 48 # ASSIGN : s_4_2 97 # ASSIGN : s_4_3 107 # ASSIGN : s_4_4 150 # ASSIGN : s_4_5 219 # ASSIGN : s_4_6 291 # ASSIGN : s_4_7 388 # ASSIGN : s_4_8 453 # ASSIGN : s_4_9 492 # ASSIGN : s_4_10 563 # ASSIGN : s_4_11 595 # ASSIGN : s_4_12 759 # ASSIGN : s_4_13 832 # ASSIGN : s_4_14 1218 # ASSIGN : s_5_0 94 # ASSIGN : s_5_1 177 # ASSIGN : s_5_2 229 # ASSIGN : s_5_3 306 # ASSIGN : s_5_4 319 # ASSIGN : s_5_5 605 # ASSIGN : s_5_6 720 # ASSIGN : s_5_7 756 # ASSIGN : s_5_8 832 # ASSIGN : s_5_9 878 # ASSIGN : s_5_10 921 # ASSIGN : s_5_11 977 # ASSIGN : s_5_12 1074 # ASSIGN : s_5_13 1106 # ASSIGN : s_5_14 1158 # ASSIGN : s_6_0 54 # ASSIGN : s_6_1 83 # ASSIGN : s_6_2 196 # ASSIGN : s_6_3 217 # ASSIGN : s_6_4 393 # ASSIGN : s_6_5 481 # ASSIGN : s_6_6 535 # ASSIGN : s_6_7 549 # ASSIGN : s_6_8 564 # ASSIGN : s_6_9 580 # ASSIGN : s_6_10 629 # ASSIGN : s_6_11 910 # ASSIGN : s_6_12 929 # ASSIGN : s_6_13 1089 # ASSIGN : s_6_14 1166 # ASSIGN : s_7_0 182 # ASSIGN : s_7_1 194 # ASSIGN : s_7_2 268 # ASSIGN : s_7_3 296 # ASSIGN : s_7_4 565 # ASSIGN : s_7_5 596 # ASSIGN : s_7_6 813 # ASSIGN : s_7_7 910 # ASSIGN : s_7_8 980 # ASSIGN : s_7_9 1029 # ASSIGN : s_7_10 1054 # ASSIGN : s_7_11 1072 # ASSIGN : s_7_12 1127 # ASSIGN : s_7_13 1132 # ASSIGN : s_7_14 1203 # ASSIGN : s_8_0 38 # ASSIGN : s_8_1 272 # ASSIGN : s_8_2 285 # ASSIGN : s_8_3 359 # ASSIGN : s_8_4 406 # ASSIGN : s_8_5 627 # ASSIGN : s_8_6 765 # ASSIGN : s_8_7 862 # ASSIGN : s_8_8 912 # ASSIGN : s_8_9 937 # ASSIGN : s_8_10 978 # ASSIGN : s_8_11 1072 # ASSIGN : s_8_12 1094 # ASSIGN : s_8_13 1155 # ASSIGN : s_8_14 1214 # ASSIGN : s_9_0 39 # ASSIGN : s_9_1 66 # ASSIGN : s_9_2 80 # ASSIGN : s_9_3 115 # ASSIGN : s_9_4 232 # ASSIGN : s_9_5 281 # ASSIGN : s_9_6 327 # ASSIGN : s_9_7 411 # ASSIGN : s_9_8 457 # ASSIGN : s_9_9 586 # ASSIGN : s_9_10 658 # ASSIGN : s_9_11 676 # ASSIGN : s_9_12 699 # ASSIGN : s_9_13 795 # ASSIGN : s_9_14 1191 # ASSIGN : s_10_0 125 # ASSIGN : s_10_1 161 # ASSIGN : s_10_2 299 # ASSIGN : s_10_3 380 # ASSIGN : s_10_4 447 # ASSIGN : s_10_5 697 # ASSIGN : s_10_6 705 # ASSIGN : s_10_7 803 # ASSIGN : s_10_8 826 # ASSIGN : s_10_9 908 # ASSIGN : s_10_10 943 # ASSIGN : s_10_11 1039 # ASSIGN : s_10_12 1046 # ASSIGN : s_10_13 1100 # ASSIGN : s_10_14 1192 # ASSIGN : s_11_0 70 # ASSIGN : s_11_1 151 # ASSIGN : s_11_2 209 # ASSIGN : s_11_3 447 # ASSIGN : s_11_4 490 # ASSIGN : s_11_5 491 # ASSIGN : s_11_6 553 # ASSIGN : s_11_7 666 # ASSIGN : s_11_8 715 # ASSIGN : s_11_9 923 # ASSIGN : s_11_10 949 # ASSIGN : s_11_11 1028 # ASSIGN : s_11_12 1037 # ASSIGN : s_11_13 1061 # ASSIGN : s_11_14 1085 # ASSIGN : s_12_0 10 # ASSIGN : s_12_1 109 # ASSIGN : s_12_2 195 # ASSIGN : s_12_3 233 # ASSIGN : s_12_4 271 # ASSIGN : s_12_5 410 # ASSIGN : s_12_6 446 # ASSIGN : s_12_7 475 # ASSIGN : s_12_8 492 # ASSIGN : s_12_9 605 # ASSIGN : s_12_10 619 # ASSIGN : s_12_11 676 # ASSIGN : s_12_12 740 # ASSIGN : s_12_13 863 # ASSIGN : s_12_14 959 # ASSIGN : s_13_0 228 # ASSIGN : s_13_1 238 # ASSIGN : s_13_2 368 # ASSIGN : s_13_3 461 # ASSIGN : s_13_4 524 # ASSIGN : s_13_5 585 # ASSIGN : s_13_6 647 # ASSIGN : s_13_7 722 # ASSIGN : s_13_8 812 # ASSIGN : s_13_9 852 # ASSIGN : s_13_10 941 # ASSIGN : s_13_11 949 # ASSIGN : s_13_12 976 # ASSIGN : s_13_13 1097 # ASSIGN : s_13_14 1166 # ASSIGN : s_14_0 43 # ASSIGN : s_14_1 136 # ASSIGN : s_14_2 148 # ASSIGN : s_14_3 162 # ASSIGN : s_14_4 235 # ASSIGN : s_14_5 272 # ASSIGN : s_14_6 326 # ASSIGN : s_14_7 410 # ASSIGN : s_14_8 494 # ASSIGN : s_14_9 547 # ASSIGN : s_14_10 606 # ASSIGN : s_14_11 701 # ASSIGN : s_14_12 788 # ASSIGN : s_14_13 1064 # ASSIGN : s_14_14 1155 SHOW_RESULT 1230 END : 1230 (1 seconds) [Sat Jun 3 11:26:26 2006] SHOW_RESULT 1230 CPU : 1.09999999999997 = 1.09999999999997 + 0 + 0 + 0 # BOUND : makespan 1218 1230 MODIFY_CNF 1224 BEGIN : [Sat Jun 3 11:26:26 2006] MODIFY_CNF 1224 END : 143193218 bytes (0 seconds) [Sat Jun 3 11:26:26 2006] MODIFY_CNF 1224 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1224 BEGIN : [Sat Jun 3 11:26:26 2006] CMD : minisat /work/tamura/csp2sat54214.cnf /work/tamura/csp2sat54214.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1820600 5352571 | 606866 0 0 NaNQ | 0.000 % | | 101 | 1820600 5352571 | 667552 101 886 8.8 | 71.638 % | | 251 | 1820600 5352571 | 734307 251 1952 7.8 | 71.638 % | | 478 | 1820600 5352571 | 807738 478 5463 11.4 | 71.638 % | | 815 | 1820600 5352571 | 888512 815 10258 12.6 | 71.638 % | | 1321 | 1820600 5352571 | 977363 1321 17159 13.0 | 71.638 % | | 2082 | 1820600 5352571 | 1075100 2082 29143 14.0 | 71.638 % | | 3221 | 1820077 5351003 | 1182610 2829 41263 14.6 | 71.662 % | | 4929 | 1807670 5314175 | 1300871 4524 65144 14.4 | 71.741 % | | 7492 | 1807670 5314175 | 1430958 7087 118154 16.7 | 71.741 % | | 11337 | 1807670 5314175 | 1574054 10932 181019 16.6 | 71.741 % | ==============================================================================) restarts : 11 conflicts : 14202 (144 /sec) decisions : 20495 (208 /sec) propagations : 174927968 (1772620 /sec) inspects : 1370542291 (13888288 /sec) conflict literals : 236106 (33.80 % deleted) CPU time : 98.6833 s SATISFIABLE VERIFY_CNF 1224 END : (100 seconds) [Sat Jun 3 11:28:06 2006] VERIFY_CNF 1224 CPU : 100.23 = 0.0100000000000477 + 0.0299999999999999 + 100.04 + 0.15 # RESULT : makespan 1224 SATISFIABLE SHOW_RESULT 1224 BEGIN : [Sat Jun 3 11:28:06 2006] # ASSIGN : makespan 1224 # ASSIGN : s_0_0 1 # ASSIGN : s_0_1 76 # ASSIGN : s_0_2 157 # ASSIGN : s_0_3 238 # ASSIGN : s_0_4 602 # ASSIGN : s_0_5 682 # ASSIGN : s_0_6 685 # ASSIGN : s_0_7 723 # ASSIGN : s_0_8 823 # ASSIGN : s_0_9 877 # ASSIGN : s_0_10 951 # ASSIGN : s_0_11 1039 # ASSIGN : s_0_12 1121 # ASSIGN : s_0_13 1124 # ASSIGN : s_0_14 1136 # ASSIGN : s_1_0 34 # ASSIGN : s_1_1 252 # ASSIGN : s_1_2 303 # ASSIGN : s_1_3 350 # ASSIGN : s_1_4 365 # ASSIGN : s_1_5 557 # ASSIGN : s_1_6 633 # ASSIGN : s_1_7 685 # ASSIGN : s_1_8 703 # ASSIGN : s_1_9 725 # ASSIGN : s_1_10 905 # ASSIGN : s_1_11 942 # ASSIGN : s_1_12 972 # ASSIGN : s_1_13 977 # ASSIGN : s_1_14 1066 # ASSIGN : s_2_0 109 # ASSIGN : s_2_1 201 # ASSIGN : s_2_2 255 # ASSIGN : s_2_3 348 # ASSIGN : s_2_4 402 # ASSIGN : s_2_5 440 # ASSIGN : s_2_6 518 # ASSIGN : s_2_7 589 # ASSIGN : s_2_8 696 # ASSIGN : s_2_9 715 # ASSIGN : s_2_10 748 # ASSIGN : s_2_11 792 # ASSIGN : s_2_12 863 # ASSIGN : s_2_13 1156 # ASSIGN : s_2_14 1165 # ASSIGN : s_3_0 8 # ASSIGN : s_3_1 41 # ASSIGN : s_3_2 265 # ASSIGN : s_3_3 345 # ASSIGN : s_3_4 422 # ASSIGN : s_3_5 678 # ASSIGN : s_3_6 744 # ASSIGN : s_3_7 759 # ASSIGN : s_3_8 785 # ASSIGN : s_3_9 859 # ASSIGN : s_3_10 914 # ASSIGN : s_3_11 926 # ASSIGN : s_3_12 936 # ASSIGN : s_3_13 1028 # ASSIGN : s_3_14 1051 # ASSIGN : s_4_0 0 # ASSIGN : s_4_1 50 # ASSIGN : s_4_2 106 # ASSIGN : s_4_3 116 # ASSIGN : s_4_4 159 # ASSIGN : s_4_5 228 # ASSIGN : s_4_6 300 # ASSIGN : s_4_7 375 # ASSIGN : s_4_8 440 # ASSIGN : s_4_9 477 # ASSIGN : s_4_10 534 # ASSIGN : s_4_11 566 # ASSIGN : s_4_12 597 # ASSIGN : s_4_13 826 # ASSIGN : s_4_14 1039 # ASSIGN : s_5_0 11 # ASSIGN : s_5_1 189 # ASSIGN : s_5_2 253 # ASSIGN : s_5_3 327 # ASSIGN : s_5_4 390 # ASSIGN : s_5_5 588 # ASSIGN : s_5_6 719 # ASSIGN : s_5_7 755 # ASSIGN : s_5_8 831 # ASSIGN : s_5_9 884 # ASSIGN : s_5_10 915 # ASSIGN : s_5_11 971 # ASSIGN : s_5_12 1068 # ASSIGN : s_5_13 1100 # ASSIGN : s_5_14 1152 # ASSIGN : s_6_0 94 # ASSIGN : s_6_1 123 # ASSIGN : s_6_2 309 # ASSIGN : s_6_3 330 # ASSIGN : s_6_4 357 # ASSIGN : s_6_5 374 # ASSIGN : s_6_6 521 # ASSIGN : s_6_7 535 # ASSIGN : s_6_8 550 # ASSIGN : s_6_9 621 # ASSIGN : s_6_10 759 # ASSIGN : s_6_11 904 # ASSIGN : s_6_12 923 # ASSIGN : s_6_13 1083 # ASSIGN : s_6_14 1160 # ASSIGN : s_7_0 427 # ASSIGN : s_7_1 476 # ASSIGN : s_7_2 568 # ASSIGN : s_7_3 572 # ASSIGN : s_7_4 575 # ASSIGN : s_7_5 590 # ASSIGN : s_7_6 807 # ASSIGN : s_7_7 904 # ASSIGN : s_7_8 974 # ASSIGN : s_7_9 1023 # ASSIGN : s_7_10 1048 # ASSIGN : s_7_11 1066 # ASSIGN : s_7_12 1121 # ASSIGN : s_7_13 1126 # ASSIGN : s_7_14 1197 # ASSIGN : s_8_0 47 # ASSIGN : s_8_1 161 # ASSIGN : s_8_2 175 # ASSIGN : s_8_3 208 # ASSIGN : s_8_4 304 # ASSIGN : s_8_5 728 # ASSIGN : s_8_6 759 # ASSIGN : s_8_7 856 # ASSIGN : s_8_8 906 # ASSIGN : s_8_9 931 # ASSIGN : s_8_10 972 # ASSIGN : s_8_11 1066 # ASSIGN : s_8_12 1088 # ASSIGN : s_8_13 1149 # ASSIGN : s_8_14 1208 # ASSIGN : s_9_0 57 # ASSIGN : s_9_1 84 # ASSIGN : s_9_2 88 # ASSIGN : s_9_3 123 # ASSIGN : s_9_4 203 # ASSIGN : s_9_5 254 # ASSIGN : s_9_6 300 # ASSIGN : s_9_7 419 # ASSIGN : s_9_8 465 # ASSIGN : s_9_9 580 # ASSIGN : s_9_10 652 # ASSIGN : s_9_11 670 # ASSIGN : s_9_12 693 # ASSIGN : s_9_13 789 # ASSIGN : s_9_14 1185 # ASSIGN : s_10_0 70 # ASSIGN : s_10_1 106 # ASSIGN : s_10_2 171 # ASSIGN : s_10_3 252 # ASSIGN : s_10_4 319 # ASSIGN : s_10_5 417 # ASSIGN : s_10_6 439 # ASSIGN : s_10_7 561 # ASSIGN : s_10_8 621 # ASSIGN : s_10_9 759 # ASSIGN : s_10_10 810 # ASSIGN : s_10_11 1033 # ASSIGN : s_10_12 1040 # ASSIGN : s_10_13 1094 # ASSIGN : s_10_14 1186 # ASSIGN : s_11_0 6 # ASSIGN : s_11_1 99 # ASSIGN : s_11_2 221 # ASSIGN : s_11_3 340 # ASSIGN : s_11_4 383 # ASSIGN : s_11_5 384 # ASSIGN : s_11_6 584 # ASSIGN : s_11_7 660 # ASSIGN : s_11_8 709 # ASSIGN : s_11_9 917 # ASSIGN : s_11_10 943 # ASSIGN : s_11_11 1022 # ASSIGN : s_11_12 1031 # ASSIGN : s_11_13 1055 # ASSIGN : s_11_14 1079 # ASSIGN : s_12_0 12 # ASSIGN : s_12_1 117 # ASSIGN : s_12_2 207 # ASSIGN : s_12_3 245 # ASSIGN : s_12_4 283 # ASSIGN : s_12_5 366 # ASSIGN : s_12_6 454 # ASSIGN : s_12_7 473 # ASSIGN : s_12_8 490 # ASSIGN : s_12_9 599 # ASSIGN : s_12_10 613 # ASSIGN : s_12_11 670 # ASSIGN : s_12_12 734 # ASSIGN : s_12_13 857 # ASSIGN : s_12_14 953 # ASSIGN : s_13_0 138 # ASSIGN : s_13_1 259 # ASSIGN : s_13_2 362 # ASSIGN : s_13_3 455 # ASSIGN : s_13_4 518 # ASSIGN : s_13_5 579 # ASSIGN : s_13_6 641 # ASSIGN : s_13_7 716 # ASSIGN : s_13_8 806 # ASSIGN : s_13_9 846 # ASSIGN : s_13_10 935 # ASSIGN : s_13_11 943 # ASSIGN : s_13_12 970 # ASSIGN : s_13_13 1091 # ASSIGN : s_13_14 1160 # ASSIGN : s_14_0 36 # ASSIGN : s_14_1 148 # ASSIGN : s_14_2 160 # ASSIGN : s_14_3 174 # ASSIGN : s_14_4 248 # ASSIGN : s_14_5 251 # ASSIGN : s_14_6 298 # ASSIGN : s_14_7 382 # ASSIGN : s_14_8 466 # ASSIGN : s_14_9 519 # ASSIGN : s_14_10 577 # ASSIGN : s_14_11 672 # ASSIGN : s_14_12 794 # ASSIGN : s_14_13 971 # ASSIGN : s_14_14 1149 SHOW_RESULT 1224 END : 1224 (2 seconds) [Sat Jun 3 11:28:08 2006] SHOW_RESULT 1224 CPU : 1.09999999999997 = 1.08999999999997 + 0.01 + 0 + 0 # BOUND : makespan 1218 1224 MODIFY_CNF 1221 BEGIN : [Sat Jun 3 11:28:08 2006] MODIFY_CNF 1221 END : 143193218 bytes (0 seconds) [Sat Jun 3 11:28:08 2006] MODIFY_CNF 1221 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1221 BEGIN : [Sat Jun 3 11:28:08 2006] CMD : minisat /work/tamura/csp2sat54214.cnf /work/tamura/csp2sat54214.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1808462 5316842 | 602820 0 0 NaNQ | 0.000 % | | 100 | 1808462 5316842 | 663102 100 1081 10.8 | 71.814 % | | 250 | 1808462 5316842 | 729412 250 3123 12.5 | 71.814 % | | 475 | 1808462 5316842 | 802353 475 7010 14.8 | 71.814 % | | 812 | 1808462 5316842 | 882588 812 10824 13.3 | 71.814 % | | 1320 | 1808462 5316842 | 970847 1320 17922 13.6 | 71.814 % | | 2080 | 1807872 5315073 | 1067932 2069 28619 13.8 | 71.814 % | | 3219 | 1807872 5315073 | 1174725 3208 42414 13.2 | 71.814 % | | 4927 | 1807872 5315073 | 1292198 4916 70883 14.4 | 71.814 % | | 7489 | 1807872 5315073 | 1421418 7478 107018 14.3 | 71.814 % | | 11333 | 1807872 5315073 | 1563559 11322 183565 16.2 | 71.814 % | | 17099 | 1807872 5315073 | 1719915 17088 287290 16.8 | 71.814 % | ==============================================================================) restarts : 12 conflicts : 23180 (147 /sec) decisions : 32206 (205 /sec) propagations : 286310462 (1821064 /sec) inspects : 2236135562 (14222834 /sec) conflict literals : 408386 (37.07 % deleted) CPU time : 157.222 s SATISFIABLE VERIFY_CNF 1221 END : (159 seconds) [Sat Jun 3 11:30:47 2006] VERIFY_CNF 1221 CPU : 159.1 = 0.00999999999999091 + 0.03 + 158.53 + 0.53 # RESULT : makespan 1221 SATISFIABLE SHOW_RESULT 1221 BEGIN : [Sat Jun 3 11:30:47 2006] # ASSIGN : makespan 1221 # ASSIGN : s_0_0 8 # ASSIGN : s_0_1 77 # ASSIGN : s_0_2 235 # ASSIGN : s_0_3 316 # ASSIGN : s_0_4 378 # ASSIGN : s_0_5 458 # ASSIGN : s_0_6 493 # ASSIGN : s_0_7 531 # ASSIGN : s_0_8 593 # ASSIGN : s_0_9 647 # ASSIGN : s_0_10 713 # ASSIGN : s_0_11 1036 # ASSIGN : s_0_12 1118 # ASSIGN : s_0_13 1121 # ASSIGN : s_0_14 1133 # ASSIGN : s_1_0 30 # ASSIGN : s_1_1 179 # ASSIGN : s_1_2 280 # ASSIGN : s_1_3 327 # ASSIGN : s_1_4 342 # ASSIGN : s_1_5 434 # ASSIGN : s_1_6 510 # ASSIGN : s_1_7 562 # ASSIGN : s_1_8 600 # ASSIGN : s_1_9 654 # ASSIGN : s_1_10 796 # ASSIGN : s_1_11 822 # ASSIGN : s_1_12 852 # ASSIGN : s_1_13 857 # ASSIGN : s_1_14 950 # ASSIGN : s_2_0 0 # ASSIGN : s_2_1 67 # ASSIGN : s_2_2 114 # ASSIGN : s_2_3 207 # ASSIGN : s_2_4 261 # ASSIGN : s_2_5 299 # ASSIGN : s_2_6 395 # ASSIGN : s_2_7 466 # ASSIGN : s_2_8 574 # ASSIGN : s_2_9 627 # ASSIGN : s_2_10 660 # ASSIGN : s_2_11 704 # ASSIGN : s_2_12 775 # ASSIGN : s_2_13 1153 # ASSIGN : s_2_14 1162 # ASSIGN : s_3_0 9 # ASSIGN : s_3_1 42 # ASSIGN : s_3_2 129 # ASSIGN : s_3_3 209 # ASSIGN : s_3_4 277 # ASSIGN : s_3_5 422 # ASSIGN : s_3_6 453 # ASSIGN : s_3_7 464 # ASSIGN : s_3_8 490 # ASSIGN : s_3_9 545 # ASSIGN : s_3_10 664 # ASSIGN : s_3_11 720 # ASSIGN : s_3_12 783 # ASSIGN : s_3_13 977 # ASSIGN : s_3_14 980 # ASSIGN : s_4_0 135 # ASSIGN : s_4_1 171 # ASSIGN : s_4_2 220 # ASSIGN : s_4_3 230 # ASSIGN : s_4_4 273 # ASSIGN : s_4_5 473 # ASSIGN : s_4_6 550 # ASSIGN : s_4_7 611 # ASSIGN : s_4_8 676 # ASSIGN : s_4_9 776 # ASSIGN : s_4_10 833 # ASSIGN : s_4_11 865 # ASSIGN : s_4_12 929 # ASSIGN : s_4_13 1002 # ASSIGN : s_4_14 1209 # ASSIGN : s_5_0 2 # ASSIGN : s_5_1 105 # ASSIGN : s_5_2 239 # ASSIGN : s_5_3 249 # ASSIGN : s_5_4 409 # ASSIGN : s_5_5 520 # ASSIGN : s_5_6 697 # ASSIGN : s_5_7 733 # ASSIGN : s_5_8 809 # ASSIGN : s_5_9 916 # ASSIGN : s_5_10 946 # ASSIGN : s_5_11 1003 # ASSIGN : s_5_12 1065 # ASSIGN : s_5_13 1097 # ASSIGN : s_5_14 1149 # ASSIGN : s_6_0 85 # ASSIGN : s_6_1 114 # ASSIGN : s_6_2 308 # ASSIGN : s_6_3 329 # ASSIGN : s_6_4 356 # ASSIGN : s_6_5 373 # ASSIGN : s_6_6 450 # ASSIGN : s_6_7 496 # ASSIGN : s_6_8 584 # ASSIGN : s_6_9 615 # ASSIGN : s_6_10 737 # ASSIGN : s_6_11 918 # ASSIGN : s_6_12 937 # ASSIGN : s_6_13 1080 # ASSIGN : s_6_14 1157 # ASSIGN : s_7_0 186 # ASSIGN : s_7_1 198 # ASSIGN : s_7_2 272 # ASSIGN : s_7_3 455 # ASSIGN : s_7_4 577 # ASSIGN : s_7_5 592 # ASSIGN : s_7_6 730 # ASSIGN : s_7_7 784 # ASSIGN : s_7_8 880 # ASSIGN : s_7_9 1020 # ASSIGN : s_7_10 1045 # ASSIGN : s_7_11 1063 # ASSIGN : s_7_12 1118 # ASSIGN : s_7_13 1123 # ASSIGN : s_7_14 1194 # ASSIGN : s_8_0 36 # ASSIGN : s_8_1 158 # ASSIGN : s_8_2 174 # ASSIGN : s_8_3 276 # ASSIGN : s_8_4 323 # ASSIGN : s_8_5 699 # ASSIGN : s_8_6 730 # ASSIGN : s_8_7 827 # ASSIGN : s_8_8 875 # ASSIGN : s_8_9 929 # ASSIGN : s_8_10 969 # ASSIGN : s_8_11 1063 # ASSIGN : s_8_12 1085 # ASSIGN : s_8_13 1146 # ASSIGN : s_8_14 1205 # ASSIGN : s_9_0 58 # ASSIGN : s_9_1 85 # ASSIGN : s_9_2 89 # ASSIGN : s_9_3 124 # ASSIGN : s_9_4 262 # ASSIGN : s_9_5 331 # ASSIGN : s_9_6 377 # ASSIGN : s_9_7 461 # ASSIGN : s_9_8 507 # ASSIGN : s_9_9 667 # ASSIGN : s_9_10 739 # ASSIGN : s_9_11 757 # ASSIGN : s_9_12 780 # ASSIGN : s_9_13 876 # ASSIGN : s_9_14 1182 # ASSIGN : s_10_0 156 # ASSIGN : s_10_1 192 # ASSIGN : s_10_2 230 # ASSIGN : s_10_3 311 # ASSIGN : s_10_4 387 # ASSIGN : s_10_5 569 # ASSIGN : s_10_6 580 # ASSIGN : s_10_7 714 # ASSIGN : s_10_8 783 # ASSIGN : s_10_9 865 # ASSIGN : s_10_10 900 # ASSIGN : s_10_11 996 # ASSIGN : s_10_12 1037 # ASSIGN : s_10_13 1091 # ASSIGN : s_10_14 1183 # ASSIGN : s_11_0 1 # ASSIGN : s_11_1 79 # ASSIGN : s_11_2 137 # ASSIGN : s_11_3 199 # ASSIGN : s_11_4 242 # ASSIGN : s_11_5 243 # ASSIGN : s_11_6 431 # ASSIGN : s_11_7 511 # ASSIGN : s_11_8 600 # ASSIGN : s_11_9 823 # ASSIGN : s_11_10 849 # ASSIGN : s_11_11 928 # ASSIGN : s_11_12 948 # ASSIGN : s_11_13 972 # ASSIGN : s_11_14 1076 # ASSIGN : s_12_0 41 # ASSIGN : s_12_1 113 # ASSIGN : s_12_2 204 # ASSIGN : s_12_3 242 # ASSIGN : s_12_4 416 # ASSIGN : s_12_5 514 # ASSIGN : s_12_6 603 # ASSIGN : s_12_7 614 # ASSIGN : s_12_8 631 # ASSIGN : s_12_9 730 # ASSIGN : s_12_10 744 # ASSIGN : s_12_11 801 # ASSIGN : s_12_12 871 # ASSIGN : s_12_13 972 # ASSIGN : s_12_14 1068 # ASSIGN : s_13_0 135 # ASSIGN : s_13_1 248 # ASSIGN : s_13_2 334 # ASSIGN : s_13_3 427 # ASSIGN : s_13_4 499 # ASSIGN : s_13_5 560 # ASSIGN : s_13_6 622 # ASSIGN : s_13_7 697 # ASSIGN : s_13_8 787 # ASSIGN : s_13_9 851 # ASSIGN : s_13_10 934 # ASSIGN : s_13_11 942 # ASSIGN : s_13_12 972 # ASSIGN : s_13_13 1088 # ASSIGN : s_13_14 1157 # ASSIGN : s_14_0 62 # ASSIGN : s_14_1 145 # ASSIGN : s_14_2 157 # ASSIGN : s_14_3 171 # ASSIGN : s_14_4 245 # ASSIGN : s_14_5 276 # ASSIGN : s_14_6 369 # ASSIGN : s_14_7 485 # ASSIGN : s_14_8 569 # ASSIGN : s_14_9 622 # ASSIGN : s_14_10 680 # ASSIGN : s_14_11 855 # ASSIGN : s_14_12 965 # ASSIGN : s_14_13 1055 # ASSIGN : s_14_14 1146 SHOW_RESULT 1221 END : 1221 (1 seconds) [Sat Jun 3 11:30:48 2006] SHOW_RESULT 1221 CPU : 1.10000000000002 = 1.10000000000002 + 0 + 0 + 0 # BOUND : makespan 1218 1221 MODIFY_CNF 1219 BEGIN : [Sat Jun 3 11:30:48 2006] MODIFY_CNF 1219 END : 143193218 bytes (0 seconds) [Sat Jun 3 11:30:48 2006] MODIFY_CNF 1219 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1219 BEGIN : [Sat Jun 3 11:30:48 2006] CMD : minisat /work/tamura/csp2sat54214.cnf /work/tamura/csp2sat54214.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1799676 5290941 | 599892 0 0 NaNQ | 0.000 % | | 100 | 1799676 5290941 | 659881 100 1177 11.8 | 71.932 % | | 251 | 1799676 5290941 | 725869 251 2909 11.6 | 71.932 % | | 476 | 1799676 5290941 | 798456 476 5727 12.0 | 71.932 % | | 813 | 1799676 5290941 | 878301 813 10489 12.9 | 71.932 % | | 1319 | 1799676 5290941 | 966132 1319 17358 13.2 | 71.932 % | | 2078 | 1799676 5290941 | 1062745 2078 28843 13.9 | 71.932 % | | 3218 | 1799676 5290941 | 1169019 3218 45393 14.1 | 71.932 % | | 4926 | 1799676 5290941 | 1285921 4926 75544 15.3 | 71.932 % | | 7489 | 1799676 5290941 | 1414513 7489 116342 15.5 | 71.932 % | | 11334 | 1799676 5290941 | 1555965 11334 201625 17.8 | 71.932 % | ==============================================================================) restarts : 11 conflicts : 14211 (143 /sec) decisions : 20696 (208 /sec) propagations : 176831843 (1777633 /sec) inspects : 1392222974 (13995568 /sec) conflict literals : 259594 (33.64 % deleted) CPU time : 99.476 s SATISFIABLE VERIFY_CNF 1219 END : (101 seconds) [Sat Jun 3 11:32:29 2006] VERIFY_CNF 1219 CPU : 101.39 = 0.00999999999999091 + 0.03 + 100.82 + 0.53 # RESULT : makespan 1219 SATISFIABLE SHOW_RESULT 1219 BEGIN : [Sat Jun 3 11:32:29 2006] # ASSIGN : makespan 1219 # ASSIGN : s_0_0 7 # ASSIGN : s_0_1 85 # ASSIGN : s_0_2 241 # ASSIGN : s_0_3 322 # ASSIGN : s_0_4 390 # ASSIGN : s_0_5 470 # ASSIGN : s_0_6 491 # ASSIGN : s_0_7 529 # ASSIGN : s_0_8 591 # ASSIGN : s_0_9 695 # ASSIGN : s_0_10 761 # ASSIGN : s_0_11 921 # ASSIGN : s_0_12 1003 # ASSIGN : s_0_13 1119 # ASSIGN : s_0_14 1131 # ASSIGN : s_1_0 31 # ASSIGN : s_1_1 185 # ASSIGN : s_1_2 280 # ASSIGN : s_1_3 327 # ASSIGN : s_1_4 342 # ASSIGN : s_1_5 431 # ASSIGN : s_1_6 639 # ASSIGN : s_1_7 691 # ASSIGN : s_1_8 709 # ASSIGN : s_1_9 735 # ASSIGN : s_1_10 820 # ASSIGN : s_1_11 876 # ASSIGN : s_1_12 906 # ASSIGN : s_1_13 911 # ASSIGN : s_1_14 1047 # ASSIGN : s_2_0 0 # ASSIGN : s_2_1 65 # ASSIGN : s_2_2 115 # ASSIGN : s_2_3 208 # ASSIGN : s_2_4 262 # ASSIGN : s_2_5 300 # ASSIGN : s_2_6 378 # ASSIGN : s_2_7 449 # ASSIGN : s_2_8 572 # ASSIGN : s_2_9 628 # ASSIGN : s_2_10 661 # ASSIGN : s_2_11 705 # ASSIGN : s_2_12 776 # ASSIGN : s_2_13 1151 # ASSIGN : s_2_14 1160 # ASSIGN : s_3_0 9 # ASSIGN : s_3_1 42 # ASSIGN : s_3_2 127 # ASSIGN : s_3_3 207 # ASSIGN : s_3_4 283 # ASSIGN : s_3_5 407 # ASSIGN : s_3_6 438 # ASSIGN : s_3_7 462 # ASSIGN : s_3_8 488 # ASSIGN : s_3_9 548 # ASSIGN : s_3_10 603 # ASSIGN : s_3_11 615 # ASSIGN : s_3_12 625 # ASSIGN : s_3_13 921 # ASSIGN : s_3_14 924 # ASSIGN : s_4_0 135 # ASSIGN : s_4_1 171 # ASSIGN : s_4_2 220 # ASSIGN : s_4_3 230 # ASSIGN : s_4_4 273 # ASSIGN : s_4_5 471 # ASSIGN : s_4_6 543 # ASSIGN : s_4_7 574 # ASSIGN : s_4_8 694 # ASSIGN : s_4_9 731 # ASSIGN : s_4_10 788 # ASSIGN : s_4_11 866 # ASSIGN : s_4_12 892 # ASSIGN : s_4_13 1000 # ASSIGN : s_4_14 1207 # ASSIGN : s_5_0 115 # ASSIGN : s_5_1 198 # ASSIGN : s_5_2 240 # ASSIGN : s_5_3 255 # ASSIGN : s_5_4 289 # ASSIGN : s_5_5 376 # ASSIGN : s_5_6 509 # ASSIGN : s_5_7 545 # ASSIGN : s_5_8 626 # ASSIGN : s_5_9 731 # ASSIGN : s_5_10 771 # ASSIGN : s_5_11 846 # ASSIGN : s_5_12 1063 # ASSIGN : s_5_13 1095 # ASSIGN : s_5_14 1147 # ASSIGN : s_6_0 86 # ASSIGN : s_6_1 129 # ASSIGN : s_6_2 313 # ASSIGN : s_6_3 334 # ASSIGN : s_6_4 361 # ASSIGN : s_6_5 379 # ASSIGN : s_6_6 448 # ASSIGN : s_6_7 502 # ASSIGN : s_6_8 585 # ASSIGN : s_6_9 645 # ASSIGN : s_6_10 765 # ASSIGN : s_6_11 999 # ASSIGN : s_6_12 1018 # ASSIGN : s_6_13 1117 # ASSIGN : s_6_14 1155 # ASSIGN : s_7_0 321 # ASSIGN : s_7_1 333 # ASSIGN : s_7_2 412 # ASSIGN : s_7_3 545 # ASSIGN : s_7_4 548 # ASSIGN : s_7_5 563 # ASSIGN : s_7_6 877 # ASSIGN : s_7_7 927 # ASSIGN : s_7_8 965 # ASSIGN : s_7_9 1014 # ASSIGN : s_7_10 1039 # ASSIGN : s_7_11 1057 # ASSIGN : s_7_12 1112 # ASSIGN : s_7_13 1121 # ASSIGN : s_7_14 1192 # ASSIGN : s_8_0 3 # ASSIGN : s_8_1 72 # ASSIGN : s_8_2 175 # ASSIGN : s_8_3 369 # ASSIGN : s_8_4 416 # ASSIGN : s_8_5 678 # ASSIGN : s_8_6 738 # ASSIGN : s_8_7 835 # ASSIGN : s_8_8 883 # ASSIGN : s_8_9 908 # ASSIGN : s_8_10 953 # ASSIGN : s_8_11 1047 # ASSIGN : s_8_12 1069 # ASSIGN : s_8_13 1144 # ASSIGN : s_8_14 1203 # ASSIGN : s_9_0 58 # ASSIGN : s_9_1 85 # ASSIGN : s_9_2 89 # ASSIGN : s_9_3 124 # ASSIGN : s_9_4 268 # ASSIGN : s_9_5 341 # ASSIGN : s_9_6 387 # ASSIGN : s_9_7 473 # ASSIGN : s_9_8 519 # ASSIGN : s_9_9 645 # ASSIGN : s_9_10 717 # ASSIGN : s_9_11 758 # ASSIGN : s_9_12 781 # ASSIGN : s_9_13 877 # ASSIGN : s_9_14 1180 # ASSIGN : s_10_0 76 # ASSIGN : s_10_1 112 # ASSIGN : s_10_2 236 # ASSIGN : s_10_3 317 # ASSIGN : s_10_4 384 # ASSIGN : s_10_5 567 # ASSIGN : s_10_6 621 # ASSIGN : s_10_7 672 # ASSIGN : s_10_8 731 # ASSIGN : s_10_9 849 # ASSIGN : s_10_10 932 # ASSIGN : s_10_11 1028 # ASSIGN : s_10_12 1035 # ASSIGN : s_10_13 1089 # ASSIGN : s_10_14 1181 # ASSIGN : s_11_0 0 # ASSIGN : s_11_1 78 # ASSIGN : s_11_2 136 # ASSIGN : s_11_3 200 # ASSIGN : s_11_4 243 # ASSIGN : s_11_5 244 # ASSIGN : s_11_6 441 # ASSIGN : s_11_7 517 # ASSIGN : s_11_8 601 # ASSIGN : s_11_9 866 # ASSIGN : s_11_10 930 # ASSIGN : s_11_11 1009 # ASSIGN : s_11_12 1023 # ASSIGN : s_11_13 1078 # ASSIGN : s_11_14 1102 # ASSIGN : s_12_0 40 # ASSIGN : s_12_1 114 # ASSIGN : s_12_2 204 # ASSIGN : s_12_3 242 # ASSIGN : s_12_4 422 # ASSIGN : s_12_5 507 # ASSIGN : s_12_6 615 # ASSIGN : s_12_7 688 # ASSIGN : s_12_8 714 # ASSIGN : s_12_9 813 # ASSIGN : s_12_10 827 # ASSIGN : s_12_11 884 # ASSIGN : s_12_12 948 # ASSIGN : s_12_13 1006 # ASSIGN : s_12_14 1130 # ASSIGN : s_13_0 236 # ASSIGN : s_13_1 246 # ASSIGN : s_13_2 332 # ASSIGN : s_13_3 425 # ASSIGN : s_13_4 505 # ASSIGN : s_13_5 566 # ASSIGN : s_13_6 630 # ASSIGN : s_13_7 705 # ASSIGN : s_13_8 795 # ASSIGN : s_13_9 839 # ASSIGN : s_13_10 916 # ASSIGN : s_13_11 924 # ASSIGN : s_13_12 951 # ASSIGN : s_13_13 1086 # ASSIGN : s_13_14 1155 # ASSIGN : s_14_0 62 # ASSIGN : s_14_1 140 # ASSIGN : s_14_2 152 # ASSIGN : s_14_3 166 # ASSIGN : s_14_4 237 # ASSIGN : s_14_5 242 # ASSIGN : s_14_6 354 # ASSIGN : s_14_7 478 # ASSIGN : s_14_8 562 # ASSIGN : s_14_9 620 # ASSIGN : s_14_10 681 # ASSIGN : s_14_11 837 # ASSIGN : s_14_12 963 # ASSIGN : s_14_13 1053 # ASSIGN : s_14_14 1144 SHOW_RESULT 1219 END : 1219 (2 seconds) [Sat Jun 3 11:32:31 2006] SHOW_RESULT 1219 CPU : 1.11000000000001 = 1.11000000000001 + 0 + 0 + 0 # BOUND : makespan 1218 1219 MODIFY_CNF 1218 BEGIN : [Sat Jun 3 11:32:31 2006] MODIFY_CNF 1218 END : 143193218 bytes (0 seconds) [Sat Jun 3 11:32:31 2006] MODIFY_CNF 1218 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1218 BEGIN : [Sat Jun 3 11:32:31 2006] CMD : minisat /work/tamura/csp2sat54214.cnf /work/tamura/csp2sat54214.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1795016 5277189 | 598338 0 0 NaNQ | 0.000 % | | 100 | 1795016 5277189 | 658171 100 881 8.8 | 71.991 % | | 250 | 1795016 5277189 | 723988 250 2903 11.6 | 71.991 % | | 477 | 1795016 5277189 | 796387 477 5449 11.4 | 71.991 % | | 815 | 1795016 5277189 | 876026 815 10058 12.3 | 71.991 % | | 1321 | 1795016 5277189 | 963629 1321 16103 12.2 | 71.991 % | | 2080 | 1795016 5277189 | 1059992 2080 25835 12.4 | 71.991 % | | 3219 | 1794371 5275255 | 1165991 2630 31627 12.0 | 71.991 % | | 4927 | 1794371 5275255 | 1282590 4338 60505 13.9 | 71.991 % | | 7489 | 1794371 5275255 | 1410849 6900 107641 15.6 | 71.991 % | | 11335 | 1787073 5253655 | 1551934 10066 167702 16.7 | 72.068 % | ==============================================================================) restarts : 11 conflicts : 16795 (146 /sec) decisions : 23787 (207 /sec) propagations : 210124166 (1828354 /sec) inspects : 1621485008 (14109030 /sec) conflict literals : 305607 (34.16 % deleted) CPU time : 114.925 s SATISFIABLE VERIFY_CNF 1218 END : (117 seconds) [Sat Jun 3 11:34:28 2006] VERIFY_CNF 1218 CPU : 116.49 = 0 + 0.0299999999999999 + 116.31 + 0.15 # RESULT : makespan 1218 SATISFIABLE SHOW_RESULT 1218 BEGIN : [Sat Jun 3 11:34:28 2006] # ASSIGN : makespan 1218 # ASSIGN : s_0_0 15 # ASSIGN : s_0_1 84 # ASSIGN : s_0_2 244 # ASSIGN : s_0_3 325 # ASSIGN : s_0_4 389 # ASSIGN : s_0_5 469 # ASSIGN : s_0_6 490 # ASSIGN : s_0_7 528 # ASSIGN : s_0_8 590 # ASSIGN : s_0_9 694 # ASSIGN : s_0_10 760 # ASSIGN : s_0_11 920 # ASSIGN : s_0_12 1002 # ASSIGN : s_0_13 1118 # ASSIGN : s_0_14 1130 # ASSIGN : s_1_0 29 # ASSIGN : s_1_1 188 # ASSIGN : s_1_2 246 # ASSIGN : s_1_3 330 # ASSIGN : s_1_4 345 # ASSIGN : s_1_5 434 # ASSIGN : s_1_6 576 # ASSIGN : s_1_7 690 # ASSIGN : s_1_8 708 # ASSIGN : s_1_9 734 # ASSIGN : s_1_10 819 # ASSIGN : s_1_11 875 # ASSIGN : s_1_12 905 # ASSIGN : s_1_13 910 # ASSIGN : s_1_14 1046 # ASSIGN : s_2_0 2 # ASSIGN : s_2_1 64 # ASSIGN : s_2_2 113 # ASSIGN : s_2_3 206 # ASSIGN : s_2_4 260 # ASSIGN : s_2_5 298 # ASSIGN : s_2_6 377 # ASSIGN : s_2_7 448 # ASSIGN : s_2_8 571 # ASSIGN : s_2_9 627 # ASSIGN : s_2_10 660 # ASSIGN : s_2_11 704 # ASSIGN : s_2_12 775 # ASSIGN : s_2_13 1150 # ASSIGN : s_2_14 1159 # ASSIGN : s_3_0 8 # ASSIGN : s_3_1 41 # ASSIGN : s_3_2 126 # ASSIGN : s_3_3 206 # ASSIGN : s_3_4 282 # ASSIGN : s_3_5 406 # ASSIGN : s_3_6 437 # ASSIGN : s_3_7 461 # ASSIGN : s_3_8 487 # ASSIGN : s_3_9 532 # ASSIGN : s_3_10 587 # ASSIGN : s_3_11 599 # ASSIGN : s_3_12 624 # ASSIGN : s_3_13 974 # ASSIGN : s_3_14 977 # ASSIGN : s_4_0 138 # ASSIGN : s_4_1 174 # ASSIGN : s_4_2 223 # ASSIGN : s_4_3 233 # ASSIGN : s_4_4 276 # ASSIGN : s_4_5 460 # ASSIGN : s_4_6 609 # ASSIGN : s_4_7 628 # ASSIGN : s_4_8 693 # ASSIGN : s_4_9 730 # ASSIGN : s_4_10 787 # ASSIGN : s_4_11 865 # ASSIGN : s_4_12 891 # ASSIGN : s_4_13 999 # ASSIGN : s_4_14 1206 # ASSIGN : s_5_0 118 # ASSIGN : s_5_1 201 # ASSIGN : s_5_2 239 # ASSIGN : s_5_3 258 # ASSIGN : s_5_4 288 # ASSIGN : s_5_5 375 # ASSIGN : s_5_6 508 # ASSIGN : s_5_7 544 # ASSIGN : s_5_8 625 # ASSIGN : s_5_9 730 # ASSIGN : s_5_10 770 # ASSIGN : s_5_11 845 # ASSIGN : s_5_12 1045 # ASSIGN : s_5_13 1077 # ASSIGN : s_5_14 1129 # ASSIGN : s_6_0 82 # ASSIGN : s_6_1 111 # ASSIGN : s_6_2 312 # ASSIGN : s_6_3 333 # ASSIGN : s_6_4 360 # ASSIGN : s_6_5 378 # ASSIGN : s_6_6 487 # ASSIGN : s_6_7 501 # ASSIGN : s_6_8 584 # ASSIGN : s_6_9 644 # ASSIGN : s_6_10 764 # ASSIGN : s_6_11 958 # ASSIGN : s_6_12 1017 # ASSIGN : s_6_13 1116 # ASSIGN : s_6_14 1154 # ASSIGN : s_7_0 320 # ASSIGN : s_7_1 332 # ASSIGN : s_7_2 411 # ASSIGN : s_7_3 544 # ASSIGN : s_7_4 547 # ASSIGN : s_7_5 562 # ASSIGN : s_7_6 876 # ASSIGN : s_7_7 926 # ASSIGN : s_7_8 964 # ASSIGN : s_7_9 1013 # ASSIGN : s_7_10 1038 # ASSIGN : s_7_11 1056 # ASSIGN : s_7_12 1111 # ASSIGN : s_7_13 1120 # ASSIGN : s_7_14 1191 # ASSIGN : s_8_0 2 # ASSIGN : s_8_1 71 # ASSIGN : s_8_2 335 # ASSIGN : s_8_3 368 # ASSIGN : s_8_4 415 # ASSIGN : s_8_5 591 # ASSIGN : s_8_6 737 # ASSIGN : s_8_7 834 # ASSIGN : s_8_8 882 # ASSIGN : s_8_9 907 # ASSIGN : s_8_10 952 # ASSIGN : s_8_11 1046 # ASSIGN : s_8_12 1068 # ASSIGN : s_8_13 1143 # ASSIGN : s_8_14 1202 # ASSIGN : s_9_0 57 # ASSIGN : s_9_1 84 # ASSIGN : s_9_2 88 # ASSIGN : s_9_3 123 # ASSIGN : s_9_4 271 # ASSIGN : s_9_5 330 # ASSIGN : s_9_6 376 # ASSIGN : s_9_7 472 # ASSIGN : s_9_8 518 # ASSIGN : s_9_9 644 # ASSIGN : s_9_10 716 # ASSIGN : s_9_11 757 # ASSIGN : s_9_12 780 # ASSIGN : s_9_13 876 # ASSIGN : s_9_14 1179 # ASSIGN : s_10_0 153 # ASSIGN : s_10_1 189 # ASSIGN : s_10_2 239 # ASSIGN : s_10_3 320 # ASSIGN : s_10_4 387 # ASSIGN : s_10_5 566 # ASSIGN : s_10_6 620 # ASSIGN : s_10_7 671 # ASSIGN : s_10_8 730 # ASSIGN : s_10_9 848 # ASSIGN : s_10_10 931 # ASSIGN : s_10_11 1027 # ASSIGN : s_10_12 1034 # ASSIGN : s_10_13 1088 # ASSIGN : s_10_14 1180 # ASSIGN : s_11_0 0 # ASSIGN : s_11_1 78 # ASSIGN : s_11_2 136 # ASSIGN : s_11_3 198 # ASSIGN : s_11_4 241 # ASSIGN : s_11_5 242 # ASSIGN : s_11_6 440 # ASSIGN : s_11_7 516 # ASSIGN : s_11_8 600 # ASSIGN : s_11_9 865 # ASSIGN : s_11_10 929 # ASSIGN : s_11_11 1008 # ASSIGN : s_11_12 1022 # ASSIGN : s_11_13 1077 # ASSIGN : s_11_14 1101 # ASSIGN : s_12_0 40 # ASSIGN : s_12_1 112 # ASSIGN : s_12_2 203 # ASSIGN : s_12_3 293 # ASSIGN : s_12_4 421 # ASSIGN : s_12_5 510 # ASSIGN : s_12_6 614 # ASSIGN : s_12_7 687 # ASSIGN : s_12_8 713 # ASSIGN : s_12_9 812 # ASSIGN : s_12_10 826 # ASSIGN : s_12_11 883 # ASSIGN : s_12_12 947 # ASSIGN : s_12_13 1005 # ASSIGN : s_12_14 1201 # ASSIGN : s_13_0 235 # ASSIGN : s_13_1 245 # ASSIGN : s_13_2 331 # ASSIGN : s_13_3 424 # ASSIGN : s_13_4 504 # ASSIGN : s_13_5 565 # ASSIGN : s_13_6 629 # ASSIGN : s_13_7 704 # ASSIGN : s_13_8 794 # ASSIGN : s_13_9 838 # ASSIGN : s_13_10 915 # ASSIGN : s_13_11 923 # ASSIGN : s_13_12 950 # ASSIGN : s_13_13 1085 # ASSIGN : s_13_14 1154 # ASSIGN : s_14_0 65 # ASSIGN : s_14_1 139 # ASSIGN : s_14_2 151 # ASSIGN : s_14_3 165 # ASSIGN : s_14_4 236 # ASSIGN : s_14_5 241 # ASSIGN : s_14_6 353 # ASSIGN : s_14_7 462 # ASSIGN : s_14_8 546 # ASSIGN : s_14_9 622 # ASSIGN : s_14_10 680 # ASSIGN : s_14_11 836 # ASSIGN : s_14_12 962 # ASSIGN : s_14_13 1052 # ASSIGN : s_14_14 1143 SHOW_RESULT 1218 END : 1218 (1 seconds) [Sat Jun 3 11:34:29 2006] SHOW_RESULT 1218 CPU : 1.09999999999997 = 1.09999999999997 + 0 + 0 + 0 # BOUND : makespan 1218 1218 MAIN END : (1226 seconds) [Sat Jun 3 11:34:29 2006] MAIN CPU : 1220.47 = 305.24 + 0.68 + 911.44 + 3.11