MAIN BEGIN : [Sat Jun 3 12:47:44 2006] READ BEGIN : csp/tai10.csp [Sat Jun 3 12:47:44 2006] READ END : csp/tai10.csp (5 seconds) [Sat Jun 3 12:47:49 2006] READ CPU : 4.5 = 4.5 + 0 + 0 + 0 # BOUND : makespan 911 1699 GENERATE_CNF 1699 BEGIN : [Sat Jun 3 12:47:49 2006] GENERATE_CNF 1699 END : 386890 variables 5942909 clauses 142077914 bytes (292 seconds) [Sat Jun 3 12:52:41 2006] GENERATE_CNF 1699 CPU : 291.73 = 291.34 + 0.39 + 0 + 0 MODIFY_CNF 1305 BEGIN : [Sat Jun 3 12:52:41 2006] MODIFY_CNF 1305 END : 142077920 bytes (0 seconds) [Sat Jun 3 12:52:41 2006] MODIFY_CNF 1305 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1305 BEGIN : [Sat Jun 3 12:52:41 2006] CMD : minisat /work/tamura/csp2sat118832.cnf /work/tamura/csp2sat118832.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 2124208 6247566 | 708069 0 0 NaNQ | 0.000 % | | 100 | 2124208 6247566 | 778875 100 1698 17.0 | 67.329 % | | 251 | 2124208 6247566 | 856763 251 5441 21.7 | 67.329 % | | 478 | 2124208 6247566 | 942439 478 10176 21.3 | 67.329 % | | 816 | 2124208 6247566 | 1036683 816 15705 19.2 | 67.329 % | ==============================================================================) restarts : 5 conflicts : 925 (60 /sec) decisions : 1762 (115 /sec) propagations : 12154146 (794364 /sec) inspects : 111992050 (7319516 /sec) conflict literals : 17316 (22.63 % deleted) CPU time : 15.3005 s SATISFIABLE VERIFY_CNF 1305 END : (17 seconds) [Sat Jun 3 12:52:58 2006] VERIFY_CNF 1305 CPU : 16.96 = 0.00999999999999091 + 0.02 + 16.8 + 0.13 # RESULT : makespan 1305 SATISFIABLE SHOW_RESULT 1305 BEGIN : [Sat Jun 3 12:52:58 2006] # ASSIGN : makespan 1305 # ASSIGN : s_0_0 254 # ASSIGN : s_0_1 290 # ASSIGN : s_0_2 368 # ASSIGN : s_0_3 454 # ASSIGN : s_0_4 676 # ASSIGN : s_0_5 751 # ASSIGN : s_0_6 765 # ASSIGN : s_0_7 859 # ASSIGN : s_0_8 929 # ASSIGN : s_0_9 943 # ASSIGN : s_0_10 1039 # ASSIGN : s_0_11 1134 # ASSIGN : s_0_12 1183 # ASSIGN : s_0_13 1219 # ASSIGN : s_0_14 1304 # ASSIGN : s_1_0 111 # ASSIGN : s_1_1 211 # ASSIGN : s_1_2 252 # ASSIGN : s_1_3 274 # ASSIGN : s_1_4 473 # ASSIGN : s_1_5 525 # ASSIGN : s_1_6 596 # ASSIGN : s_1_7 612 # ASSIGN : s_1_8 706 # ASSIGN : s_1_9 777 # ASSIGN : s_1_10 907 # ASSIGN : s_1_11 919 # ASSIGN : s_1_12 1074 # ASSIGN : s_1_13 1230 # ASSIGN : s_1_14 1275 # ASSIGN : s_2_0 37 # ASSIGN : s_2_1 97 # ASSIGN : s_2_2 140 # ASSIGN : s_2_3 254 # ASSIGN : s_2_4 312 # ASSIGN : s_2_5 392 # ASSIGN : s_2_6 429 # ASSIGN : s_2_7 515 # ASSIGN : s_2_8 599 # ASSIGN : s_2_9 711 # ASSIGN : s_2_10 769 # ASSIGN : s_2_11 898 # ASSIGN : s_2_12 922 # ASSIGN : s_2_13 1039 # ASSIGN : s_2_14 1131 # ASSIGN : s_3_0 112 # ASSIGN : s_3_1 137 # ASSIGN : s_3_2 429 # ASSIGN : s_3_3 469 # ASSIGN : s_3_4 475 # ASSIGN : s_3_5 525 # ASSIGN : s_3_6 582 # ASSIGN : s_3_7 583 # ASSIGN : s_3_8 627 # ASSIGN : s_3_9 721 # ASSIGN : s_3_10 751 # ASSIGN : s_3_11 846 # ASSIGN : s_3_12 947 # ASSIGN : s_3_13 998 # ASSIGN : s_3_14 1115 # ASSIGN : s_4_0 44 # ASSIGN : s_4_1 174 # ASSIGN : s_4_2 213 # ASSIGN : s_4_3 288 # ASSIGN : s_4_4 594 # ASSIGN : s_4_5 596 # ASSIGN : s_4_6 689 # ASSIGN : s_4_7 774 # ASSIGN : s_4_8 844 # ASSIGN : s_4_9 939 # ASSIGN : s_4_10 1005 # ASSIGN : s_4_11 1009 # ASSIGN : s_4_12 1020 # ASSIGN : s_4_13 1070 # ASSIGN : s_4_14 1227 # ASSIGN : s_5_0 121 # ASSIGN : s_5_1 194 # ASSIGN : s_5_2 286 # ASSIGN : s_5_3 329 # ASSIGN : s_5_4 376 # ASSIGN : s_5_5 519 # ASSIGN : s_5_6 675 # ASSIGN : s_5_7 739 # ASSIGN : s_5_8 752 # ASSIGN : s_5_9 798 # ASSIGN : s_5_10 847 # ASSIGN : s_5_11 870 # ASSIGN : s_5_12 908 # ASSIGN : s_5_13 932 # ASSIGN : s_5_14 1203 # ASSIGN : s_6_0 5 # ASSIGN : s_6_1 16 # ASSIGN : s_6_2 96 # ASSIGN : s_6_3 163 # ASSIGN : s_6_4 256 # ASSIGN : s_6_5 746 # ASSIGN : s_6_6 806 # ASSIGN : s_6_7 858 # ASSIGN : s_6_8 922 # ASSIGN : s_6_9 1033 # ASSIGN : s_6_10 1046 # ASSIGN : s_6_11 1136 # ASSIGN : s_6_12 1200 # ASSIGN : s_6_13 1262 # ASSIGN : s_6_14 1280 # ASSIGN : s_7_0 52 # ASSIGN : s_7_1 75 # ASSIGN : s_7_2 236 # ASSIGN : s_7_3 258 # ASSIGN : s_7_4 349 # ASSIGN : s_7_5 447 # ASSIGN : s_7_6 662 # ASSIGN : s_7_7 760 # ASSIGN : s_7_8 1034 # ASSIGN : s_7_9 1050 # ASSIGN : s_7_10 1087 # ASSIGN : s_7_11 1092 # ASSIGN : s_7_12 1148 # ASSIGN : s_7_13 1165 # ASSIGN : s_7_14 1259 # ASSIGN : s_8_0 0 # ASSIGN : s_8_1 46 # ASSIGN : s_8_2 105 # ASSIGN : s_8_3 305 # ASSIGN : s_8_4 367 # ASSIGN : s_8_5 418 # ASSIGN : s_8_6 497 # ASSIGN : s_8_7 500 # ASSIGN : s_8_8 540 # ASSIGN : s_8_9 566 # ASSIGN : s_8_10 584 # ASSIGN : s_8_11 609 # ASSIGN : s_8_12 634 # ASSIGN : s_8_13 1164 # ASSIGN : s_8_14 1199 # ASSIGN : s_9_0 8 # ASSIGN : s_9_1 35 # ASSIGN : s_9_2 49 # ASSIGN : s_9_3 126 # ASSIGN : s_9_4 464 # ASSIGN : s_9_5 685 # ASSIGN : s_9_6 781 # ASSIGN : s_9_7 840 # ASSIGN : s_9_8 879 # ASSIGN : s_9_9 965 # ASSIGN : s_9_10 1004 # ASSIGN : s_9_11 1095 # ASSIGN : s_9_12 1125 # ASSIGN : s_9_13 1216 # ASSIGN : s_9_14 1294 # ASSIGN : s_10_0 125 # ASSIGN : s_10_1 192 # ASSIGN : s_10_2 377 # ASSIGN : s_10_3 427 # ASSIGN : s_10_4 433 # ASSIGN : s_10_5 516 # ASSIGN : s_10_6 535 # ASSIGN : s_10_7 564 # ASSIGN : s_10_8 604 # ASSIGN : s_10_9 676 # ASSIGN : s_10_10 708 # ASSIGN : s_10_11 756 # ASSIGN : s_10_12 855 # ASSIGN : s_10_13 954 # ASSIGN : s_10_14 1235 # ASSIGN : s_11_0 289 # ASSIGN : s_11_1 355 # ASSIGN : s_11_2 362 # ASSIGN : s_11_3 443 # ASSIGN : s_11_4 554 # ASSIGN : s_11_5 659 # ASSIGN : s_11_6 742 # ASSIGN : s_11_7 758 # ASSIGN : s_11_8 759 # ASSIGN : s_11_9 828 # ASSIGN : s_11_10 835 # ASSIGN : s_11_11 838 # ASSIGN : s_11_12 1105 # ASSIGN : s_11_13 1113 # ASSIGN : s_11_14 1138 # ASSIGN : s_12_0 196 # ASSIGN : s_12_1 347 # ASSIGN : s_12_2 428 # ASSIGN : s_12_3 432 # ASSIGN : s_12_4 510 # ASSIGN : s_12_5 519 # ASSIGN : s_12_6 601 # ASSIGN : s_12_7 760 # ASSIGN : s_12_8 765 # ASSIGN : s_12_9 839 # ASSIGN : s_12_10 863 # ASSIGN : s_12_11 1031 # ASSIGN : s_12_12 1035 # ASSIGN : s_12_13 1137 # ASSIGN : s_12_14 1231 # ASSIGN : s_13_0 5 # ASSIGN : s_13_1 37 # ASSIGN : s_13_2 132 # ASSIGN : s_13_3 222 # ASSIGN : s_13_4 386 # ASSIGN : s_13_5 417 # ASSIGN : s_13_6 474 # ASSIGN : s_13_7 519 # ASSIGN : s_13_8 607 # ASSIGN : s_13_9 705 # ASSIGN : s_13_10 768 # ASSIGN : s_13_11 823 # ASSIGN : s_13_12 1002 # ASSIGN : s_13_13 1199 # ASSIGN : s_13_14 1283 # ASSIGN : s_14_0 0 # ASSIGN : s_14_1 12 # ASSIGN : s_14_2 47 # ASSIGN : s_14_3 133 # ASSIGN : s_14_4 150 # ASSIGN : s_14_5 192 # ASSIGN : s_14_6 238 # ASSIGN : s_14_7 303 # ASSIGN : s_14_8 597 # ASSIGN : s_14_9 693 # ASSIGN : s_14_10 729 # ASSIGN : s_14_11 815 # ASSIGN : s_14_12 910 # ASSIGN : s_14_13 1003 # ASSIGN : s_14_14 1248 SHOW_RESULT 1305 END : 1305 (1 seconds) [Sat Jun 3 12:52:59 2006] SHOW_RESULT 1305 CPU : 1.06999999999999 = 1.06999999999999 + 0 + 0 + 0 # BOUND : makespan 911 1305 MODIFY_CNF 1108 BEGIN : [Sat Jun 3 12:52:59 2006] MODIFY_CNF 1108 END : 142077920 bytes (0 seconds) [Sat Jun 3 12:52:59 2006] MODIFY_CNF 1108 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1108 BEGIN : [Sat Jun 3 12:52:59 2006] CMD : minisat /work/tamura/csp2sat118832.cnf /work/tamura/csp2sat118832.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1278604 3755703 | 426201 0 0 NaNQ | 0.000 % | ==============================================================================) restarts : 1 conflicts : 42 (4 /sec) decisions : 56 (6 /sec) propagations : 709128 (74672 /sec) inspects : 4885644 (514466 /sec) conflict literals : 204 (29.66 % deleted) CPU time : 9.49653 s UNSATISFIABLE VERIFY_CNF 1108 END : (12 seconds) [Sat Jun 3 12:53:11 2006] VERIFY_CNF 1108 CPU : 10.7 = 0.00999999999999091 + 0.03 + 10.52 + 0.14 # RESULT : makespan 1108 UNSATISFIABLE # BOUND : makespan 1109 1305 MODIFY_CNF 1207 BEGIN : [Sat Jun 3 12:53:11 2006] MODIFY_CNF 1207 END : 142077920 bytes (0 seconds) [Sat Jun 3 12:53:11 2006] MODIFY_CNF 1207 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1207 BEGIN : [Sat Jun 3 12:53:11 2006] CMD : minisat /work/tamura/csp2sat118832.cnf /work/tamura/csp2sat118832.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1704043 5009388 | 568014 0 0 NaNQ | 0.000 % | | 101 | 1704043 5009388 | 624815 101 767 7.6 | 73.125 % | | 251 | 1704043 5009388 | 687296 251 1795 7.2 | 73.125 % | | 477 | 1704043 5009388 | 756026 477 3714 7.8 | 73.125 % | | 814 | 1677986 4932153 | 831629 708 5972 8.4 | 73.828 % | ==============================================================================) restarts : 5 conflicts : 1144 (79 /sec) decisions : 1653 (114 /sec) propagations : 11631063 (804457 /sec) inspects : 81218260 (5617420 /sec) conflict literals : 9600 (31.23 % deleted) CPU time : 14.4583 s UNSATISFIABLE VERIFY_CNF 1207 END : (16 seconds) [Sat Jun 3 12:53:27 2006] VERIFY_CNF 1207 CPU : 15.71 = 0 + 0.01 + 15.56 + 0.14 # RESULT : makespan 1207 UNSATISFIABLE # BOUND : makespan 1208 1305 MODIFY_CNF 1256 BEGIN : [Sat Jun 3 12:53:27 2006] MODIFY_CNF 1256 END : 142077920 bytes (0 seconds) [Sat Jun 3 12:53:27 2006] MODIFY_CNF 1256 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1256 BEGIN : [Sat Jun 3 12:53:27 2006] CMD : minisat /work/tamura/csp2sat118832.cnf /work/tamura/csp2sat118832.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1912782 5624446 | 637594 0 0 NaNQ | 0.000 % | | 100 | 1912782 5624446 | 701353 100 1047 10.5 | 70.225 % | | 250 | 1912782 5624446 | 771488 250 3085 12.3 | 70.225 % | | 475 | 1912782 5624446 | 848637 475 6115 12.9 | 70.225 % | | 812 | 1912782 5624446 | 933501 812 9822 12.1 | 70.225 % | | 1319 | 1912782 5624446 | 1026851 1319 20009 15.2 | 70.225 % | | 2078 | 1912782 5624446 | 1129536 2078 37783 18.2 | 70.225 % | | 3217 | 1912782 5624446 | 1242490 3217 57654 17.9 | 70.225 % | | 4926 | 1912782 5624446 | 1366739 4926 89722 18.2 | 70.225 % | | 7488 | 1912782 5624446 | 1503413 7488 165369 22.1 | 70.225 % | | 11332 | 1912782 5624446 | 1653754 11332 243191 21.5 | 70.225 % | | 17098 | 1912782 5624446 | 1819130 17098 376709 22.0 | 70.225 % | ==============================================================================) restarts : 12 conflicts : 17694 (140 /sec) decisions : 26197 (208 /sec) propagations : 209853314 (1662860 /sec) inspects : 1859649546 (14735708 /sec) conflict literals : 394113 (30.71 % deleted) CPU time : 126.2 s SATISFIABLE VERIFY_CNF 1256 END : (128 seconds) [Sat Jun 3 12:55:35 2006] VERIFY_CNF 1256 CPU : 128.16 = 0 + 0.02 + 127.6 + 0.54 # RESULT : makespan 1256 SATISFIABLE SHOW_RESULT 1256 BEGIN : [Sat Jun 3 12:55:35 2006] # ASSIGN : makespan 1256 # ASSIGN : s_0_0 8 # ASSIGN : s_0_1 43 # ASSIGN : s_0_2 133 # ASSIGN : s_0_3 212 # ASSIGN : s_0_4 277 # ASSIGN : s_0_5 335 # ASSIGN : s_0_6 349 # ASSIGN : s_0_7 486 # ASSIGN : s_0_8 570 # ASSIGN : s_0_9 584 # ASSIGN : s_0_10 674 # ASSIGN : s_0_11 769 # ASSIGN : s_0_12 824 # ASSIGN : s_0_13 860 # ASSIGN : s_0_14 1199 # ASSIGN : s_1_0 121 # ASSIGN : s_1_1 204 # ASSIGN : s_1_2 246 # ASSIGN : s_1_3 268 # ASSIGN : s_1_4 297 # ASSIGN : s_1_5 349 # ASSIGN : s_1_6 420 # ASSIGN : s_1_7 437 # ASSIGN : s_1_8 530 # ASSIGN : s_1_9 594 # ASSIGN : s_1_10 657 # ASSIGN : s_1_11 669 # ASSIGN : s_1_12 881 # ASSIGN : s_1_13 1181 # ASSIGN : s_1_14 1226 # ASSIGN : s_2_0 5 # ASSIGN : s_2_1 65 # ASSIGN : s_2_2 282 # ASSIGN : s_2_3 353 # ASSIGN : s_2_4 355 # ASSIGN : s_2_5 405 # ASSIGN : s_2_6 442 # ASSIGN : s_2_7 528 # ASSIGN : s_2_8 609 # ASSIGN : s_2_9 696 # ASSIGN : s_2_10 753 # ASSIGN : s_2_11 819 # ASSIGN : s_2_12 843 # ASSIGN : s_2_13 941 # ASSIGN : s_2_14 1050 # ASSIGN : s_3_0 87 # ASSIGN : s_3_1 172 # ASSIGN : s_3_2 247 # ASSIGN : s_3_3 324 # ASSIGN : s_3_4 330 # ASSIGN : s_3_5 366 # ASSIGN : s_3_6 423 # ASSIGN : s_3_7 424 # ASSIGN : s_3_8 468 # ASSIGN : s_3_9 562 # ASSIGN : s_3_10 592 # ASSIGN : s_3_11 687 # ASSIGN : s_3_12 1112 # ASSIGN : s_3_13 1166 # ASSIGN : s_3_14 1218 # ASSIGN : s_4_0 108 # ASSIGN : s_4_1 229 # ASSIGN : s_4_2 268 # ASSIGN : s_4_3 343 # ASSIGN : s_4_4 441 # ASSIGN : s_4_5 492 # ASSIGN : s_4_6 547 # ASSIGN : s_4_7 653 # ASSIGN : s_4_8 685 # ASSIGN : s_4_9 780 # ASSIGN : s_4_10 920 # ASSIGN : s_4_11 933 # ASSIGN : s_4_12 944 # ASSIGN : s_4_13 994 # ASSIGN : s_4_14 1119 # ASSIGN : s_5_0 257 # ASSIGN : s_5_1 330 # ASSIGN : s_5_2 377 # ASSIGN : s_5_3 445 # ASSIGN : s_5_4 502 # ASSIGN : s_5_5 690 # ASSIGN : s_5_6 797 # ASSIGN : s_5_7 830 # ASSIGN : s_5_8 843 # ASSIGN : s_5_9 861 # ASSIGN : s_5_10 910 # ASSIGN : s_5_11 934 # ASSIGN : s_5_12 972 # ASSIGN : s_5_13 993 # ASSIGN : s_5_14 1154 # ASSIGN : s_6_0 34 # ASSIGN : s_6_1 37 # ASSIGN : s_6_2 117 # ASSIGN : s_6_3 184 # ASSIGN : s_6_4 501 # ASSIGN : s_6_5 704 # ASSIGN : s_6_6 735 # ASSIGN : s_6_7 860 # ASSIGN : s_6_8 924 # ASSIGN : s_6_9 1014 # ASSIGN : s_6_10 1016 # ASSIGN : s_6_11 1133 # ASSIGN : s_6_12 1197 # ASSIGN : s_6_13 1213 # ASSIGN : s_6_14 1231 # ASSIGN : s_7_0 16 # ASSIGN : s_7_1 78 # ASSIGN : s_7_2 108 # ASSIGN : s_7_3 130 # ASSIGN : s_7_4 437 # ASSIGN : s_7_5 697 # ASSIGN : s_7_6 830 # ASSIGN : s_7_7 919 # ASSIGN : s_7_8 1033 # ASSIGN : s_7_9 1055 # ASSIGN : s_7_10 1092 # ASSIGN : s_7_11 1097 # ASSIGN : s_7_12 1139 # ASSIGN : s_7_13 1156 # ASSIGN : s_7_14 1210 # ASSIGN : s_8_0 56 # ASSIGN : s_8_1 100 # ASSIGN : s_8_2 159 # ASSIGN : s_8_3 375 # ASSIGN : s_8_4 448 # ASSIGN : s_8_5 499 # ASSIGN : s_8_6 554 # ASSIGN : s_8_7 557 # ASSIGN : s_8_8 710 # ASSIGN : s_8_9 736 # ASSIGN : s_8_10 754 # ASSIGN : s_8_11 812 # ASSIGN : s_8_12 1041 # ASSIGN : s_8_13 1115 # ASSIGN : s_8_14 1150 # ASSIGN : s_9_0 7 # ASSIGN : s_9_1 39 # ASSIGN : s_9_2 53 # ASSIGN : s_9_3 504 # ASSIGN : s_9_4 565 # ASSIGN : s_9_5 620 # ASSIGN : s_9_6 753 # ASSIGN : s_9_7 922 # ASSIGN : s_9_8 943 # ASSIGN : s_9_9 976 # ASSIGN : s_9_10 1009 # ASSIGN : s_9_11 1113 # ASSIGN : s_9_12 1143 # ASSIGN : s_9_13 1234 # ASSIGN : s_9_14 1245 # ASSIGN : s_10_0 34 # ASSIGN : s_10_1 101 # ASSIGN : s_10_2 195 # ASSIGN : s_10_3 245 # ASSIGN : s_10_4 275 # ASSIGN : s_10_5 358 # ASSIGN : s_10_6 377 # ASSIGN : s_10_7 406 # ASSIGN : s_10_8 443 # ASSIGN : s_10_9 524 # ASSIGN : s_10_10 556 # ASSIGN : s_10_11 598 # ASSIGN : s_10_12 831 # ASSIGN : s_10_13 945 # ASSIGN : s_10_14 1063 # ASSIGN : s_11_0 505 # ASSIGN : s_11_1 590 # ASSIGN : s_11_2 597 # ASSIGN : s_11_3 678 # ASSIGN : s_11_4 760 # ASSIGN : s_11_5 818 # ASSIGN : s_11_6 904 # ASSIGN : s_11_7 943 # ASSIGN : s_11_8 944 # ASSIGN : s_11_9 1013 # ASSIGN : s_11_10 1020 # ASSIGN : s_11_11 1023 # ASSIGN : s_11_12 1107 # ASSIGN : s_11_13 1131 # ASSIGN : s_11_14 1163 # ASSIGN : s_12_0 39 # ASSIGN : s_12_1 131 # ASSIGN : s_12_2 262 # ASSIGN : s_12_3 272 # ASSIGN : s_12_4 350 # ASSIGN : s_12_5 359 # ASSIGN : s_12_6 443 # ASSIGN : s_12_7 542 # ASSIGN : s_12_8 559 # ASSIGN : s_12_9 679 # ASSIGN : s_12_10 687 # ASSIGN : s_12_11 731 # ASSIGN : s_12_12 771 # ASSIGN : s_12_13 850 # ASSIGN : s_12_14 1038 # ASSIGN : s_13_0 215 # ASSIGN : s_13_1 247 # ASSIGN : s_13_2 518 # ASSIGN : s_13_3 549 # ASSIGN : s_13_4 617 # ASSIGN : s_13_5 648 # ASSIGN : s_13_6 658 # ASSIGN : s_13_7 703 # ASSIGN : s_13_8 778 # ASSIGN : s_13_9 901 # ASSIGN : s_13_10 952 # ASSIGN : s_13_11 1007 # ASSIGN : s_13_12 1106 # ASSIGN : s_13_13 1150 # ASSIGN : s_13_14 1234 # ASSIGN : s_14_0 219 # ASSIGN : s_14_1 231 # ASSIGN : s_14_2 266 # ASSIGN : s_14_3 349 # ASSIGN : s_14_4 436 # ASSIGN : s_14_5 478 # ASSIGN : s_14_6 533 # ASSIGN : s_14_7 616 # ASSIGN : s_14_8 691 # ASSIGN : s_14_9 787 # ASSIGN : s_14_10 815 # ASSIGN : s_14_11 901 # ASSIGN : s_14_12 996 # ASSIGN : s_14_13 1089 # ASSIGN : s_14_14 1200 SHOW_RESULT 1256 END : 1256 (1 seconds) [Sat Jun 3 12:55:36 2006] SHOW_RESULT 1256 CPU : 1.14 = 1.13 + 0.01 + 0 + 0 # BOUND : makespan 1208 1256 MODIFY_CNF 1232 BEGIN : [Sat Jun 3 12:55:36 2006] MODIFY_CNF 1232 END : 142077920 bytes (0 seconds) [Sat Jun 3 12:55:36 2006] MODIFY_CNF 1232 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1232 BEGIN : [Sat Jun 3 12:55:36 2006] CMD : minisat /work/tamura/csp2sat118832.cnf /work/tamura/csp2sat118832.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1806831 5312064 | 602277 0 0 NaNQ | 0.000 % | | 102 | 1806831 5312064 | 662504 102 1179 11.6 | 71.647 % | | 252 | 1806831 5312064 | 728755 252 3082 12.2 | 71.647 % | | 478 | 1806831 5312064 | 801630 478 7562 15.8 | 71.647 % | | 815 | 1806831 5312064 | 881793 815 12467 15.3 | 71.647 % | | 1321 | 1806831 5312064 | 969973 1321 18988 14.4 | 71.647 % | | 2081 | 1806831 5312064 | 1066970 2081 31827 15.3 | 71.647 % | | 3221 | 1806831 5312064 | 1173667 3221 49925 15.5 | 71.647 % | | 4929 | 1805557 5308285 | 1291034 4614 74739 16.2 | 71.658 % | | 7491 | 1748045 5138208 | 1420137 6314 100935 16.0 | 73.248 % | ==============================================================================) restarts : 10 conflicts : 8866 (139 /sec) decisions : 13249 (208 /sec) propagations : 103646399 (1627714 /sec) inspects : 832843547 (13079383 /sec) conflict literals : 144170 (32.30 % deleted) CPU time : 63.6761 s UNSATISFIABLE VERIFY_CNF 1232 END : (66 seconds) [Sat Jun 3 12:56:42 2006] VERIFY_CNF 1232 CPU : 64.95 = 0.0100000000000477 + 0.02 + 64.78 + 0.14 # RESULT : makespan 1232 UNSATISFIABLE # BOUND : makespan 1233 1256 MODIFY_CNF 1244 BEGIN : [Sat Jun 3 12:56:42 2006] MODIFY_CNF 1244 END : 142077920 bytes (0 seconds) [Sat Jun 3 12:56:42 2006] MODIFY_CNF 1244 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1244 BEGIN : [Sat Jun 3 12:56:42 2006] CMD : minisat /work/tamura/csp2sat118832.cnf /work/tamura/csp2sat118832.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1858638 5464749 | 619546 0 0 NaNQ | 0.000 % | | 101 | 1858638 5464749 | 681500 101 2207 21.9 | 70.936 % | | 251 | 1858638 5464749 | 749650 251 4387 17.5 | 70.936 % | | 476 | 1858638 5464749 | 824615 476 8705 18.3 | 70.936 % | | 813 | 1858638 5464749 | 907077 813 13230 16.3 | 70.936 % | | 1319 | 1858638 5464749 | 997785 1319 25230 19.1 | 70.936 % | | 2078 | 1858638 5464749 | 1097563 2078 38762 18.7 | 70.936 % | | 3219 | 1858638 5464749 | 1207319 3219 59311 18.4 | 70.936 % | ==============================================================================) restarts : 8 conflicts : 4138 (121 /sec) decisions : 6736 (197 /sec) propagations : 46809062 (1371498 /sec) inspects : 398472421 (11675174 /sec) conflict literals : 73250 (25.78 % deleted) CPU time : 34.1299 s SATISFIABLE VERIFY_CNF 1244 END : (36 seconds) [Sat Jun 3 12:57:18 2006] VERIFY_CNF 1244 CPU : 35.65 = 0 + 0.02 + 35.47 + 0.16 # RESULT : makespan 1244 SATISFIABLE SHOW_RESULT 1244 BEGIN : [Sat Jun 3 12:57:18 2006] # ASSIGN : makespan 1244 # ASSIGN : s_0_0 60 # ASSIGN : s_0_1 100 # ASSIGN : s_0_2 194 # ASSIGN : s_0_3 273 # ASSIGN : s_0_4 338 # ASSIGN : s_0_5 414 # ASSIGN : s_0_6 428 # ASSIGN : s_0_7 521 # ASSIGN : s_0_8 613 # ASSIGN : s_0_9 627 # ASSIGN : s_0_10 717 # ASSIGN : s_0_11 812 # ASSIGN : s_0_12 861 # ASSIGN : s_0_13 897 # ASSIGN : s_0_14 1187 # ASSIGN : s_1_0 17 # ASSIGN : s_1_1 139 # ASSIGN : s_1_2 180 # ASSIGN : s_1_3 248 # ASSIGN : s_1_4 277 # ASSIGN : s_1_5 329 # ASSIGN : s_1_6 400 # ASSIGN : s_1_7 416 # ASSIGN : s_1_8 509 # ASSIGN : s_1_9 629 # ASSIGN : s_1_10 702 # ASSIGN : s_1_11 727 # ASSIGN : s_1_12 1059 # ASSIGN : s_1_13 1169 # ASSIGN : s_1_14 1214 # ASSIGN : s_2_0 77 # ASSIGN : s_2_1 137 # ASSIGN : s_2_2 180 # ASSIGN : s_2_3 253 # ASSIGN : s_2_4 255 # ASSIGN : s_2_5 305 # ASSIGN : s_2_6 342 # ASSIGN : s_2_7 435 # ASSIGN : s_2_8 516 # ASSIGN : s_2_9 687 # ASSIGN : s_2_10 744 # ASSIGN : s_2_11 810 # ASSIGN : s_2_12 834 # ASSIGN : s_2_13 946 # ASSIGN : s_2_14 1038 # ASSIGN : s_3_0 77 # ASSIGN : s_3_1 291 # ASSIGN : s_3_2 350 # ASSIGN : s_3_3 385 # ASSIGN : s_3_4 391 # ASSIGN : s_3_5 424 # ASSIGN : s_3_6 481 # ASSIGN : s_3_7 482 # ASSIGN : s_3_8 526 # ASSIGN : s_3_9 620 # ASSIGN : s_3_10 650 # ASSIGN : s_3_11 745 # ASSIGN : s_3_12 895 # ASSIGN : s_3_13 1154 # ASSIGN : s_3_14 1206 # ASSIGN : s_4_0 253 # ASSIGN : s_4_1 349 # ASSIGN : s_4_2 388 # ASSIGN : s_4_3 463 # ASSIGN : s_4_4 561 # ASSIGN : s_4_5 563 # ASSIGN : s_4_6 601 # ASSIGN : s_4_7 676 # ASSIGN : s_4_8 708 # ASSIGN : s_4_9 845 # ASSIGN : s_4_10 908 # ASSIGN : s_4_11 921 # ASSIGN : s_4_12 932 # ASSIGN : s_4_13 982 # ASSIGN : s_4_14 1107 # ASSIGN : s_5_0 121 # ASSIGN : s_5_1 306 # ASSIGN : s_5_2 334 # ASSIGN : s_5_3 377 # ASSIGN : s_5_4 424 # ASSIGN : s_5_5 678 # ASSIGN : s_5_6 784 # ASSIGN : s_5_7 817 # ASSIGN : s_5_8 838 # ASSIGN : s_5_9 849 # ASSIGN : s_5_10 898 # ASSIGN : s_5_11 922 # ASSIGN : s_5_12 960 # ASSIGN : s_5_13 981 # ASSIGN : s_5_14 1142 # ASSIGN : s_6_0 12 # ASSIGN : s_6_1 15 # ASSIGN : s_6_2 95 # ASSIGN : s_6_3 162 # ASSIGN : s_6_4 410 # ASSIGN : s_6_5 692 # ASSIGN : s_6_6 723 # ASSIGN : s_6_7 848 # ASSIGN : s_6_8 912 # ASSIGN : s_6_9 1002 # ASSIGN : s_6_10 1004 # ASSIGN : s_6_11 1121 # ASSIGN : s_6_12 1185 # ASSIGN : s_6_13 1201 # ASSIGN : s_6_14 1219 # ASSIGN : s_7_0 268 # ASSIGN : s_7_1 487 # ASSIGN : s_7_2 517 # ASSIGN : s_7_3 539 # ASSIGN : s_7_4 611 # ASSIGN : s_7_5 755 # ASSIGN : s_7_6 818 # ASSIGN : s_7_7 907 # ASSIGN : s_7_8 1038 # ASSIGN : s_7_9 1043 # ASSIGN : s_7_10 1080 # ASSIGN : s_7_11 1085 # ASSIGN : s_7_12 1127 # ASSIGN : s_7_13 1144 # ASSIGN : s_7_14 1198 # ASSIGN : s_8_0 95 # ASSIGN : s_8_1 139 # ASSIGN : s_8_2 202 # ASSIGN : s_8_3 289 # ASSIGN : s_8_4 503 # ASSIGN : s_8_5 554 # ASSIGN : s_8_6 665 # ASSIGN : s_8_7 668 # ASSIGN : s_8_8 808 # ASSIGN : s_8_9 846 # ASSIGN : s_8_10 864 # ASSIGN : s_8_11 879 # ASSIGN : s_8_12 1029 # ASSIGN : s_8_13 1103 # ASSIGN : s_8_14 1138 # ASSIGN : s_9_0 264 # ASSIGN : s_9_1 291 # ASSIGN : s_9_2 453 # ASSIGN : s_9_3 530 # ASSIGN : s_9_4 554 # ASSIGN : s_9_5 609 # ASSIGN : s_9_6 714 # ASSIGN : s_9_7 827 # ASSIGN : s_9_8 861 # ASSIGN : s_9_9 964 # ASSIGN : s_9_10 997 # ASSIGN : s_9_11 1101 # ASSIGN : s_9_12 1131 # ASSIGN : s_9_13 1222 # ASSIGN : s_9_14 1233 # ASSIGN : s_10_0 24 # ASSIGN : s_10_1 91 # ASSIGN : s_10_2 198 # ASSIGN : s_10_3 251 # ASSIGN : s_10_4 262 # ASSIGN : s_10_5 345 # ASSIGN : s_10_6 387 # ASSIGN : s_10_7 416 # ASSIGN : s_10_8 501 # ASSIGN : s_10_9 559 # ASSIGN : s_10_10 591 # ASSIGN : s_10_11 643 # ASSIGN : s_10_12 742 # ASSIGN : s_10_13 830 # ASSIGN : s_10_14 890 # ASSIGN : s_11_0 0 # ASSIGN : s_11_1 74 # ASSIGN : s_11_2 81 # ASSIGN : s_11_3 295 # ASSIGN : s_11_4 518 # ASSIGN : s_11_5 576 # ASSIGN : s_11_6 659 # ASSIGN : s_11_7 675 # ASSIGN : s_11_8 676 # ASSIGN : s_11_9 1001 # ASSIGN : s_11_10 1008 # ASSIGN : s_11_11 1011 # ASSIGN : s_11_12 1095 # ASSIGN : s_11_13 1119 # ASSIGN : s_11_14 1151 # ASSIGN : s_12_0 5 # ASSIGN : s_12_1 97 # ASSIGN : s_12_2 178 # ASSIGN : s_12_3 185 # ASSIGN : s_12_4 280 # ASSIGN : s_12_5 476 # ASSIGN : s_12_6 593 # ASSIGN : s_12_7 670 # ASSIGN : s_12_8 677 # ASSIGN : s_12_9 765 # ASSIGN : s_12_10 773 # ASSIGN : s_12_11 843 # ASSIGN : s_12_12 847 # ASSIGN : s_12_13 910 # ASSIGN : s_12_14 1077 # ASSIGN : s_13_0 187 # ASSIGN : s_13_1 219 # ASSIGN : s_13_2 307 # ASSIGN : s_13_3 364 # ASSIGN : s_13_4 432 # ASSIGN : s_13_5 466 # ASSIGN : s_13_6 476 # ASSIGN : s_13_7 575 # ASSIGN : s_13_8 766 # ASSIGN : s_13_9 889 # ASSIGN : s_13_10 940 # ASSIGN : s_13_11 995 # ASSIGN : s_13_12 1094 # ASSIGN : s_13_13 1138 # ASSIGN : s_13_14 1222 # ASSIGN : s_14_0 135 # ASSIGN : s_14_1 147 # ASSIGN : s_14_2 182 # ASSIGN : s_14_3 246 # ASSIGN : s_14_4 263 # ASSIGN : s_14_5 305 # ASSIGN : s_14_6 351 # ASSIGN : s_14_7 527 # ASSIGN : s_14_8 679 # ASSIGN : s_14_9 775 # ASSIGN : s_14_10 803 # ASSIGN : s_14_11 889 # ASSIGN : s_14_12 984 # ASSIGN : s_14_13 1077 # ASSIGN : s_14_14 1188 SHOW_RESULT 1244 END : 1244 (1 seconds) [Sat Jun 3 12:57:19 2006] SHOW_RESULT 1244 CPU : 1.14999999999999 = 1.13999999999999 + 0.01 + 0 + 0 # BOUND : makespan 1233 1244 MODIFY_CNF 1238 BEGIN : [Sat Jun 3 12:57:19 2006] MODIFY_CNF 1238 END : 142077920 bytes (0 seconds) [Sat Jun 3 12:57:19 2006] MODIFY_CNF 1238 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1238 BEGIN : [Sat Jun 3 12:57:19 2006] CMD : minisat /work/tamura/csp2sat118832.cnf /work/tamura/csp2sat118832.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1832404 5387415 | 610801 0 0 NaNQ | 0.000 % | | 101 | 1832404 5387415 | 671881 101 1129 11.2 | 71.292 % | | 251 | 1832404 5387415 | 739069 251 2052 8.2 | 71.292 % | | 477 | 1832404 5387415 | 812976 477 3895 8.2 | 71.292 % | | 814 | 1831766 5385502 | 894273 741 8516 11.5 | 71.292 % | | 1320 | 1831766 5385502 | 983701 1247 20172 16.2 | 71.292 % | | 2080 | 1831766 5385502 | 1082071 2007 34642 17.3 | 71.292 % | | 3222 | 1831766 5385502 | 1190278 3149 49685 15.8 | 71.292 % | | 4931 | 1831766 5385502 | 1309306 4858 83271 17.1 | 71.292 % | | 7493 | 1822324 5357558 | 1440236 5992 99327 16.6 | 71.392 % | | 11338 | 1815631 5337724 | 1584260 9428 188237 20.0 | 71.585 % | ==============================================================================) restarts : 11 conflicts : 15842 (149 /sec) decisions : 23557 (222 /sec) propagations : 181918343 (1711397 /sec) inspects : 1528618788 (14380486 /sec) conflict literals : 335528 (31.64 % deleted) CPU time : 106.298 s UNSATISFIABLE VERIFY_CNF 1238 END : (108 seconds) [Sat Jun 3 12:59:07 2006] VERIFY_CNF 1238 CPU : 107.99 = 0.00999999999999091 + 0.0299999999999999 + 107.42 + 0.53 # RESULT : makespan 1238 UNSATISFIABLE # BOUND : makespan 1239 1244 MODIFY_CNF 1241 BEGIN : [Sat Jun 3 12:59:07 2006] MODIFY_CNF 1241 END : 142077920 bytes (0 seconds) [Sat Jun 3 12:59:07 2006] MODIFY_CNF 1241 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1241 BEGIN : [Sat Jun 3 12:59:07 2006] CMD : minisat /work/tamura/csp2sat118832.cnf /work/tamura/csp2sat118832.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1847426 5431795 | 615808 0 0 NaNQ | 0.000 % | | 101 | 1847426 5431795 | 677388 101 851 8.4 | 71.113 % | | 252 | 1847426 5431795 | 745127 252 2516 10.0 | 71.113 % | | 477 | 1847426 5431795 | 819640 477 5289 11.1 | 71.113 % | | 814 | 1847426 5431795 | 901604 814 10668 13.1 | 71.113 % | | 1321 | 1847426 5431795 | 991764 1321 19201 14.5 | 71.113 % | ==============================================================================) restarts : 6 conflicts : 1710 (91 /sec) decisions : 2948 (156 /sec) propagations : 19880981 (1053108 /sec) inspects : 164245143 (8700165 /sec) conflict literals : 24997 (25.56 % deleted) CPU time : 18.8784 s SATISFIABLE VERIFY_CNF 1241 END : (21 seconds) [Sat Jun 3 12:59:28 2006] VERIFY_CNF 1241 CPU : 20.39 = 0 + 0.02 + 20.21 + 0.16 # RESULT : makespan 1241 SATISFIABLE SHOW_RESULT 1241 BEGIN : [Sat Jun 3 12:59:28 2006] # ASSIGN : makespan 1241 # ASSIGN : s_0_0 1 # ASSIGN : s_0_1 46 # ASSIGN : s_0_2 124 # ASSIGN : s_0_3 203 # ASSIGN : s_0_4 268 # ASSIGN : s_0_5 331 # ASSIGN : s_0_6 345 # ASSIGN : s_0_7 518 # ASSIGN : s_0_8 630 # ASSIGN : s_0_9 644 # ASSIGN : s_0_10 734 # ASSIGN : s_0_11 837 # ASSIGN : s_0_12 901 # ASSIGN : s_0_13 989 # ASSIGN : s_0_14 1240 # ASSIGN : s_1_0 138 # ASSIGN : s_1_1 238 # ASSIGN : s_1_2 284 # ASSIGN : s_1_3 306 # ASSIGN : s_1_4 335 # ASSIGN : s_1_5 387 # ASSIGN : s_1_6 458 # ASSIGN : s_1_7 474 # ASSIGN : s_1_8 572 # ASSIGN : s_1_9 626 # ASSIGN : s_1_10 725 # ASSIGN : s_1_11 737 # ASSIGN : s_1_12 1056 # ASSIGN : s_1_13 1166 # ASSIGN : s_1_14 1211 # ASSIGN : s_2_0 89 # ASSIGN : s_2_1 149 # ASSIGN : s_2_2 279 # ASSIGN : s_2_3 350 # ASSIGN : s_2_4 352 # ASSIGN : s_2_5 402 # ASSIGN : s_2_6 439 # ASSIGN : s_2_7 546 # ASSIGN : s_2_8 627 # ASSIGN : s_2_9 776 # ASSIGN : s_2_10 833 # ASSIGN : s_2_11 899 # ASSIGN : s_2_12 923 # ASSIGN : s_2_13 1021 # ASSIGN : s_2_14 1113 # ASSIGN : s_3_0 254 # ASSIGN : s_3_1 268 # ASSIGN : s_3_2 353 # ASSIGN : s_3_3 397 # ASSIGN : s_3_4 403 # ASSIGN : s_3_5 428 # ASSIGN : s_3_6 527 # ASSIGN : s_3_7 528 # ASSIGN : s_3_8 572 # ASSIGN : s_3_9 689 # ASSIGN : s_3_10 719 # ASSIGN : s_3_11 814 # ASSIGN : s_3_12 1116 # ASSIGN : s_3_13 1173 # ASSIGN : s_3_14 1225 # ASSIGN : s_4_0 96 # ASSIGN : s_4_1 199 # ASSIGN : s_4_2 252 # ASSIGN : s_4_3 327 # ASSIGN : s_4_4 463 # ASSIGN : s_4_5 485 # ASSIGN : s_4_6 525 # ASSIGN : s_4_7 597 # ASSIGN : s_4_8 643 # ASSIGN : s_4_9 744 # ASSIGN : s_4_10 829 # ASSIGN : s_4_11 833 # ASSIGN : s_4_12 844 # ASSIGN : s_4_13 894 # ASSIGN : s_4_14 1035 # ASSIGN : s_5_0 208 # ASSIGN : s_5_1 449 # ASSIGN : s_5_2 477 # ASSIGN : s_5_3 523 # ASSIGN : s_5_4 570 # ASSIGN : s_5_5 673 # ASSIGN : s_5_6 761 # ASSIGN : s_5_7 794 # ASSIGN : s_5_8 807 # ASSIGN : s_5_9 829 # ASSIGN : s_5_10 878 # ASSIGN : s_5_11 919 # ASSIGN : s_5_12 957 # ASSIGN : s_5_13 978 # ASSIGN : s_5_14 1139 # ASSIGN : s_6_0 43 # ASSIGN : s_6_1 119 # ASSIGN : s_6_2 335 # ASSIGN : s_6_3 475 # ASSIGN : s_6_4 598 # ASSIGN : s_6_5 689 # ASSIGN : s_6_6 720 # ASSIGN : s_6_7 845 # ASSIGN : s_6_8 909 # ASSIGN : s_6_9 999 # ASSIGN : s_6_10 1001 # ASSIGN : s_6_11 1118 # ASSIGN : s_6_12 1182 # ASSIGN : s_6_13 1198 # ASSIGN : s_6_14 1216 # ASSIGN : s_7_0 139 # ASSIGN : s_7_1 162 # ASSIGN : s_7_2 192 # ASSIGN : s_7_3 214 # ASSIGN : s_7_4 388 # ASSIGN : s_7_5 752 # ASSIGN : s_7_6 815 # ASSIGN : s_7_7 904 # ASSIGN : s_7_8 1016 # ASSIGN : s_7_9 1040 # ASSIGN : s_7_10 1077 # ASSIGN : s_7_11 1082 # ASSIGN : s_7_12 1124 # ASSIGN : s_7_13 1141 # ASSIGN : s_7_14 1195 # ASSIGN : s_8_0 192 # ASSIGN : s_8_1 247 # ASSIGN : s_8_2 469 # ASSIGN : s_8_3 567 # ASSIGN : s_8_4 629 # ASSIGN : s_8_5 680 # ASSIGN : s_8_6 735 # ASSIGN : s_8_7 738 # ASSIGN : s_8_8 778 # ASSIGN : s_8_9 804 # ASSIGN : s_8_10 822 # ASSIGN : s_8_11 876 # ASSIGN : s_8_12 1021 # ASSIGN : s_8_13 1100 # ASSIGN : s_8_14 1135 # ASSIGN : s_9_0 0 # ASSIGN : s_9_1 27 # ASSIGN : s_9_2 41 # ASSIGN : s_9_3 520 # ASSIGN : s_9_4 544 # ASSIGN : s_9_5 599 # ASSIGN : s_9_6 666 # ASSIGN : s_9_7 904 # ASSIGN : s_9_8 928 # ASSIGN : s_9_9 961 # ASSIGN : s_9_10 994 # ASSIGN : s_9_11 1093 # ASSIGN : s_9_12 1123 # ASSIGN : s_9_13 1214 # ASSIGN : s_9_14 1230 # ASSIGN : s_10_0 25 # ASSIGN : s_10_1 92 # ASSIGN : s_10_2 186 # ASSIGN : s_10_3 236 # ASSIGN : s_10_4 238 # ASSIGN : s_10_5 321 # ASSIGN : s_10_6 399 # ASSIGN : s_10_7 428 # ASSIGN : s_10_8 465 # ASSIGN : s_10_9 556 # ASSIGN : s_10_10 588 # ASSIGN : s_10_11 640 # ASSIGN : s_10_12 739 # ASSIGN : s_10_13 827 # ASSIGN : s_10_14 986 # ASSIGN : s_11_0 36 # ASSIGN : s_11_1 111 # ASSIGN : s_11_2 118 # ASSIGN : s_11_3 199 # ASSIGN : s_11_4 281 # ASSIGN : s_11_5 339 # ASSIGN : s_11_6 422 # ASSIGN : s_11_7 438 # ASSIGN : s_11_8 530 # ASSIGN : s_11_9 617 # ASSIGN : s_11_10 624 # ASSIGN : s_11_11 627 # ASSIGN : s_11_12 711 # ASSIGN : s_11_13 887 # ASSIGN : s_11_14 923 # ASSIGN : s_12_0 30 # ASSIGN : s_12_1 122 # ASSIGN : s_12_2 340 # ASSIGN : s_12_3 344 # ASSIGN : s_12_4 457 # ASSIGN : s_12_5 466 # ASSIGN : s_12_6 568 # ASSIGN : s_12_7 668 # ASSIGN : s_12_8 687 # ASSIGN : s_12_9 742 # ASSIGN : s_12_10 750 # ASSIGN : s_12_11 840 # ASSIGN : s_12_12 844 # ASSIGN : s_12_13 907 # ASSIGN : s_12_14 1167 # ASSIGN : s_13_0 201 # ASSIGN : s_13_1 233 # ASSIGN : s_13_2 321 # ASSIGN : s_13_3 357 # ASSIGN : s_13_4 425 # ASSIGN : s_13_5 456 # ASSIGN : s_13_6 473 # ASSIGN : s_13_7 523 # ASSIGN : s_13_8 763 # ASSIGN : s_13_9 886 # ASSIGN : s_13_10 937 # ASSIGN : s_13_11 992 # ASSIGN : s_13_12 1091 # ASSIGN : s_13_13 1135 # ASSIGN : s_13_14 1219 # ASSIGN : s_14_0 174 # ASSIGN : s_14_1 186 # ASSIGN : s_14_2 221 # ASSIGN : s_14_3 285 # ASSIGN : s_14_4 302 # ASSIGN : s_14_5 346 # ASSIGN : s_14_6 392 # ASSIGN : s_14_7 594 # ASSIGN : s_14_8 676 # ASSIGN : s_14_9 772 # ASSIGN : s_14_10 800 # ASSIGN : s_14_11 886 # ASSIGN : s_14_12 981 # ASSIGN : s_14_13 1074 # ASSIGN : s_14_14 1184 SHOW_RESULT 1241 END : 1241 (1 seconds) [Sat Jun 3 12:59:29 2006] SHOW_RESULT 1241 CPU : 1.12 = 1.12 + 0 + 0 + 0 # BOUND : makespan 1239 1241 MODIFY_CNF 1240 BEGIN : [Sat Jun 3 12:59:29 2006] MODIFY_CNF 1240 END : 142077920 bytes (0 seconds) [Sat Jun 3 12:59:29 2006] MODIFY_CNF 1240 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1240 BEGIN : [Sat Jun 3 12:59:29 2006] CMD : minisat /work/tamura/csp2sat118832.cnf /work/tamura/csp2sat118832.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1841899 5415444 | 613966 0 0 NaNQ | 0.000 % | | 100 | 1841899 5415444 | 675362 100 1057 10.6 | 71.173 % | | 252 | 1841899 5415444 | 742898 252 2189 8.7 | 71.173 % | | 479 | 1841899 5415444 | 817188 479 4031 8.4 | 71.173 % | | 818 | 1841899 5415444 | 898907 818 7697 9.4 | 71.173 % | | 1324 | 1841294 5413630 | 988798 1165 11511 9.9 | 71.173 % | | 2084 | 1841294 5413630 | 1087678 1925 23206 12.1 | 71.173 % | | 3223 | 1840632 5411645 | 1196446 3015 43265 14.3 | 71.174 % | | 4931 | 1837591 5402636 | 1316090 4717 72720 15.4 | 71.204 % | | 7494 | 1837591 5402636 | 1447699 7280 130568 17.9 | 71.204 % | | 11343 | 1818412 5345917 | 1592469 10072 210389 20.9 | 71.418 % | | 17111 | 1733863 5095250 | 1751716 10723 228594 21.3 | 72.212 % | ==============================================================================) restarts : 12 conflicts : 18386 (147 /sec) decisions : 27031 (217 /sec) propagations : 213193764 (1708900 /sec) inspects : 1800837105 (14434992 /sec) conflict literals : 418151 (32.81 % deleted) CPU time : 124.755 s UNSATISFIABLE VERIFY_CNF 1240 END : (126 seconds) [Sat Jun 3 13:01:35 2006] VERIFY_CNF 1240 CPU : 125.95 = 0.00999999999999091 + 0.03 + 125.77 + 0.14 # RESULT : makespan 1240 UNSATISFIABLE # BOUND : makespan 1241 1241 MAIN END : (831 seconds) [Sat Jun 3 13:01:35 2006] MAIN CPU : 827.17 = 300.35 + 0.61 + 524.13 + 2.08