MAIN BEGIN : [Fri Jun 2 05:54:08 2006] READ BEGIN : csp/la36.csp [Fri Jun 2 05:54:08 2006] READ END : csp/la36.csp (4 seconds) [Fri Jun 2 05:54:12 2006] READ CPU : 4.58 = 4.58 + 0 + 0 + 0 # BOUND : makespan 1028 1676 GENERATE_CNF 1676 BEGIN : [Fri Jun 2 05:54:12 2006] GENERATE_CNF 1676 END : 381575 variables 5852465 clauses 139857437 bytes (287 seconds) [Fri Jun 2 05:58:59 2006] GENERATE_CNF 1676 CPU : 286.84 = 286.42 + 0.42 + 0 + 0 MODIFY_CNF 1352 BEGIN : [Fri Jun 2 05:58:59 2006] MODIFY_CNF 1352 END : 139857443 bytes (0 seconds) [Fri Jun 2 05:58:59 2006] MODIFY_CNF 1352 CPU : 0.00999999999999091 = 0.00999999999999091 + 0 + 0 + 0 VERIFY_CNF 1352 BEGIN : [Fri Jun 2 05:58:59 2006] CMD : minisat /work/tamura/csp2sat103986.cnf /work/tamura/csp2sat103986.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 2213971 6512084 | 737990 0 0 NaNQ | 0.000 % | | 100 | 2213971 6512084 | 811789 100 1207 12.1 | 65.614 % | | 251 | 2213971 6512084 | 892967 251 3644 14.5 | 65.614 % | ==============================================================================) restarts : 3 conflicts : 407 (37 /sec) decisions : 958 (87 /sec) propagations : 5480238 (497703 /sec) inspects : 53675995 (4874731 /sec) conflict literals : 7836 (21.80 % deleted) CPU time : 11.0111 s SATISFIABLE VERIFY_CNF 1352 END : (14 seconds) [Fri Jun 2 05:59:13 2006] VERIFY_CNF 1352 CPU : 12.66 = 0 + 0.00999999999999995 + 12.52 + 0.13 # RESULT : makespan 1352 SATISFIABLE SHOW_RESULT 1352 BEGIN : [Fri Jun 2 05:59:13 2006] # ASSIGN : makespan 1352 # ASSIGN : s_0_0 6 # ASSIGN : s_0_1 170 # ASSIGN : s_0_2 225 # ASSIGN : s_0_3 338 # ASSIGN : s_0_4 436 # ASSIGN : s_0_5 502 # ASSIGN : s_0_6 536 # ASSIGN : s_0_7 552 # ASSIGN : s_0_8 573 # ASSIGN : s_0_9 626 # ASSIGN : s_0_10 755 # ASSIGN : s_0_11 807 # ASSIGN : s_0_12 1193 # ASSIGN : s_0_13 1271 # ASSIGN : s_0_14 1313 # ASSIGN : s_1_0 102 # ASSIGN : s_1_1 364 # ASSIGN : s_1_2 462 # ASSIGN : s_1_3 539 # ASSIGN : s_1_4 663 # ASSIGN : s_1_5 697 # ASSIGN : s_1_6 800 # ASSIGN : s_1_7 843 # ASSIGN : s_1_8 898 # ASSIGN : s_1_9 994 # ASSIGN : s_1_10 1013 # ASSIGN : s_1_11 1053 # ASSIGN : s_1_12 1132 # ASSIGN : s_1_13 1224 # ASSIGN : s_1_14 1286 # ASSIGN : s_2_0 9 # ASSIGN : s_2_1 92 # ASSIGN : s_2_2 169 # ASSIGN : s_2_3 256 # ASSIGN : s_2_4 304 # ASSIGN : s_2_5 377 # ASSIGN : s_2_6 480 # ASSIGN : s_2_7 596 # ASSIGN : s_2_8 613 # ASSIGN : s_2_9 654 # ASSIGN : s_2_10 761 # ASSIGN : s_2_11 991 # ASSIGN : s_2_12 1148 # ASSIGN : s_2_13 1202 # ASSIGN : s_2_14 1289 # ASSIGN : s_3_0 1 # ASSIGN : s_3_1 78 # ASSIGN : s_3_2 174 # ASSIGN : s_3_3 202 # ASSIGN : s_3_4 209 # ASSIGN : s_3_5 312 # ASSIGN : s_3_6 347 # ASSIGN : s_3_7 390 # ASSIGN : s_3_8 466 # ASSIGN : s_3_9 475 # ASSIGN : s_3_10 631 # ASSIGN : s_3_11 674 # ASSIGN : s_3_12 750 # ASSIGN : s_3_13 1193 # ASSIGN : s_3_14 1203 # ASSIGN : s_4_0 94 # ASSIGN : s_4_1 181 # ASSIGN : s_4_2 245 # ASSIGN : s_4_3 295 # ASSIGN : s_4_4 354 # ASSIGN : s_4_5 531 # ASSIGN : s_4_6 576 # ASSIGN : s_4_7 585 # ASSIGN : s_4_8 672 # ASSIGN : s_4_9 793 # ASSIGN : s_4_10 820 # ASSIGN : s_4_11 911 # ASSIGN : s_4_12 1120 # ASSIGN : s_4_13 1165 # ASSIGN : s_4_14 1224 # ASSIGN : s_5_0 460 # ASSIGN : s_5_1 560 # ASSIGN : s_5_2 686 # ASSIGN : s_5_3 764 # ASSIGN : s_5_4 830 # ASSIGN : s_5_5 844 # ASSIGN : s_5_6 852 # ASSIGN : s_5_7 948 # ASSIGN : s_5_8 976 # ASSIGN : s_5_9 1050 # ASSIGN : s_5_10 1083 # ASSIGN : s_5_11 1172 # ASSIGN : s_5_12 1198 # ASSIGN : s_5_13 1235 # ASSIGN : s_5_14 1268 # ASSIGN : s_6_0 16 # ASSIGN : s_6_1 85 # ASSIGN : s_6_2 208 # ASSIGN : s_6_3 225 # ASSIGN : s_6_4 294 # ASSIGN : s_6_5 339 # ASSIGN : s_6_6 370 # ASSIGN : s_6_7 448 # ASSIGN : s_6_8 468 # ASSIGN : s_6_9 495 # ASSIGN : s_6_10 582 # ASSIGN : s_6_11 692 # ASSIGN : s_6_12 776 # ASSIGN : s_6_13 1071 # ASSIGN : s_6_14 1173 # ASSIGN : s_7_0 27 # ASSIGN : s_7_1 222 # ASSIGN : s_7_2 390 # ASSIGN : s_7_3 522 # ASSIGN : s_7_4 603 # ASSIGN : s_7_5 628 # ASSIGN : s_7_6 656 # ASSIGN : s_7_7 682 # ASSIGN : s_7_8 714 # ASSIGN : s_7_9 809 # ASSIGN : s_7_10 966 # ASSIGN : s_7_11 1063 # ASSIGN : s_7_12 1087 # ASSIGN : s_7_13 1239 # ASSIGN : s_7_14 1311 # ASSIGN : s_8_0 223 # ASSIGN : s_8_1 250 # ASSIGN : s_8_2 296 # ASSIGN : s_8_3 363 # ASSIGN : s_8_4 476 # ASSIGN : s_8_5 574 # ASSIGN : s_8_6 803 # ASSIGN : s_8_7 850 # ASSIGN : s_8_8 978 # ASSIGN : s_8_9 1040 # ASSIGN : s_8_10 1086 # ASSIGN : s_8_11 1114 # ASSIGN : s_8_12 1212 # ASSIGN : s_8_13 1254 # ASSIGN : s_8_14 1302 # ASSIGN : s_9_0 156 # ASSIGN : s_9_1 442 # ASSIGN : s_9_2 522 # ASSIGN : s_9_3 597 # ASSIGN : s_9_4 652 # ASSIGN : s_9_5 740 # ASSIGN : s_9_6 834 # ASSIGN : s_9_7 853 # ASSIGN : s_9_8 894 # ASSIGN : s_9_9 975 # ASSIGN : s_9_10 1025 # ASSIGN : s_9_11 1086 # ASSIGN : s_9_12 1165 # ASSIGN : s_9_13 1263 # ASSIGN : s_9_14 1289 # ASSIGN : s_10_0 191 # ASSIGN : s_10_1 304 # ASSIGN : s_10_2 400 # ASSIGN : s_10_3 447 # ASSIGN : s_10_4 570 # ASSIGN : s_10_5 639 # ASSIGN : s_10_6 716 # ASSIGN : s_10_7 749 # ASSIGN : s_10_8 848 # ASSIGN : s_10_9 870 # ASSIGN : s_10_10 902 # ASSIGN : s_10_11 959 # ASSIGN : s_10_12 1038 # ASSIGN : s_10_13 1052 # ASSIGN : s_10_14 1126 # ASSIGN : s_11_0 329 # ASSIGN : s_11_1 363 # ASSIGN : s_11_2 410 # ASSIGN : s_11_3 573 # ASSIGN : s_11_4 624 # ASSIGN : s_11_5 724 # ASSIGN : s_11_6 768 # ASSIGN : s_11_7 776 # ASSIGN : s_11_8 811 # ASSIGN : s_11_9 908 # ASSIGN : s_11_10 937 # ASSIGN : s_11_11 952 # ASSIGN : s_11_12 1128 # ASSIGN : s_11_13 1168 # ASSIGN : s_11_14 1314 # ASSIGN : s_12_0 5 # ASSIGN : s_12_1 55 # ASSIGN : s_12_2 112 # ASSIGN : s_12_3 173 # ASSIGN : s_12_4 193 # ASSIGN : s_12_5 287 # ASSIGN : s_12_6 820 # ASSIGN : s_12_7 878 # ASSIGN : s_12_8 941 # ASSIGN : s_12_9 1030 # ASSIGN : s_12_10 1086 # ASSIGN : s_12_11 1186 # ASSIGN : s_12_12 1207 # ASSIGN : s_12_13 1263 # ASSIGN : s_12_14 1295 # ASSIGN : s_13_0 298 # ASSIGN : s_13_1 382 # ASSIGN : s_13_2 427 # ASSIGN : s_13_3 442 # ASSIGN : s_13_4 698 # ASSIGN : s_13_5 796 # ASSIGN : s_13_6 881 # ASSIGN : s_13_7 910 # ASSIGN : s_13_8 1069 # ASSIGN : s_13_9 1136 # ASSIGN : s_13_10 1166 # ASSIGN : s_13_11 1216 # ASSIGN : s_13_12 1261 # ASSIGN : s_13_13 1281 # ASSIGN : s_13_14 1314 # ASSIGN : s_14_0 137 # ASSIGN : s_14_1 197 # ASSIGN : s_14_2 278 # ASSIGN : s_14_3 483 # ASSIGN : s_14_4 540 # ASSIGN : s_14_5 650 # ASSIGN : s_14_6 702 # ASSIGN : s_14_7 791 # ASSIGN : s_14_8 894 # ASSIGN : s_14_9 924 # ASSIGN : s_14_10 980 # ASSIGN : s_14_11 1018 # ASSIGN : s_14_12 1228 # ASSIGN : s_14_13 1282 # ASSIGN : s_14_14 1336 SHOW_RESULT 1352 END : 1352 (1 seconds) [Fri Jun 2 05:59:14 2006] SHOW_RESULT 1352 CPU : 1.07 = 1.06 + 0.01 + 0 + 0 # BOUND : makespan 1028 1352 MODIFY_CNF 1190 BEGIN : [Fri Jun 2 05:59:14 2006] MODIFY_CNF 1190 END : 139857443 bytes (0 seconds) [Fri Jun 2 05:59:14 2006] MODIFY_CNF 1190 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1190 BEGIN : [Fri Jun 2 05:59:14 2006] CMD : minisat /work/tamura/csp2sat103986.cnf /work/tamura/csp2sat103986.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1500818 4409577 | 500272 0 0 NaNQ | 0.000 % | | 100 | 1500818 4409577 | 550299 100 877 8.8 | 75.350 % | | 250 | 1500818 4409577 | 605329 250 2109 8.4 | 75.350 % | | 476 | 1456952 4279794 | 665862 398 3358 8.4 | 75.865 % | | 814 | 1456952 4279794 | 732448 735 5996 8.2 | 76.248 % | ==============================================================================) restarts : 5 conflicts : 909 (69 /sec) decisions : 1172 (89 /sec) propagations : 9903718 (748341 /sec) inspects : 63119384 (4769402 /sec) conflict literals : 6811 (36.62 % deleted) CPU time : 13.2342 s UNSATISFIABLE VERIFY_CNF 1190 END : (14 seconds) [Fri Jun 2 05:59:28 2006] VERIFY_CNF 1190 CPU : 14.8 = 0 + 0.03 + 14.28 + 0.49 # RESULT : makespan 1190 UNSATISFIABLE # BOUND : makespan 1191 1352 MODIFY_CNF 1271 BEGIN : [Fri Jun 2 05:59:28 2006] MODIFY_CNF 1271 END : 139857443 bytes (0 seconds) [Fri Jun 2 05:59:28 2006] MODIFY_CNF 1271 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1271 BEGIN : [Fri Jun 2 05:59:28 2006] CMD : minisat /work/tamura/csp2sat103986.cnf /work/tamura/csp2sat103986.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1848535 5434231 | 616178 0 0 NaNQ | 0.000 % | | 103 | 1848535 5434231 | 677795 102 1342 13.2 | 70.477 % | | 254 | 1848535 5434231 | 745575 253 2628 10.4 | 70.477 % | | 479 | 1848535 5434231 | 820132 478 5078 10.6 | 70.477 % | | 816 | 1847442 5430953 | 902146 815 8564 10.5 | 70.477 % | | 1322 | 1847442 5430953 | 992360 1321 14431 10.9 | 70.477 % | | 2081 | 1847442 5430953 | 1091596 2080 25915 12.5 | 70.477 % | | 3220 | 1847442 5430953 | 1200756 3219 40734 12.7 | 70.477 % | | 4930 | 1847442 5430953 | 1320832 4929 59412 12.1 | 70.477 % | | 7493 | 1846365 5427745 | 1452915 6698 81183 12.1 | 70.483 % | ==============================================================================) restarts : 10 conflicts : 10859 (157 /sec) decisions : 14998 (216 /sec) propagations : 121723348 (1756093 /sec) inspects : 990873977 (14295262 /sec) conflict literals : 137810 (34.83 % deleted) CPU time : 69.3149 s SATISFIABLE VERIFY_CNF 1271 END : (72 seconds) [Fri Jun 2 06:00:40 2006] VERIFY_CNF 1271 CPU : 70.88 = 0 + 0.01 + 70.71 + 0.16 # RESULT : makespan 1271 SATISFIABLE SHOW_RESULT 1271 BEGIN : [Fri Jun 2 06:00:40 2006] # ASSIGN : makespan 1271 # ASSIGN : s_0_0 62 # ASSIGN : s_0_1 261 # ASSIGN : s_0_2 316 # ASSIGN : s_0_3 387 # ASSIGN : s_0_4 659 # ASSIGN : s_0_5 724 # ASSIGN : s_0_6 758 # ASSIGN : s_0_7 774 # ASSIGN : s_0_8 849 # ASSIGN : s_0_9 902 # ASSIGN : s_0_10 928 # ASSIGN : s_0_11 1033 # ASSIGN : s_0_12 1130 # ASSIGN : s_0_13 1190 # ASSIGN : s_0_14 1232 # ASSIGN : s_1_0 66 # ASSIGN : s_1_1 357 # ASSIGN : s_1_2 462 # ASSIGN : s_1_3 539 # ASSIGN : s_1_4 603 # ASSIGN : s_1_5 637 # ASSIGN : s_1_6 716 # ASSIGN : s_1_7 759 # ASSIGN : s_1_8 814 # ASSIGN : s_1_9 894 # ASSIGN : s_1_10 913 # ASSIGN : s_1_11 950 # ASSIGN : s_1_12 1029 # ASSIGN : s_1_13 1143 # ASSIGN : s_1_14 1205 # ASSIGN : s_2_0 93 # ASSIGN : s_2_1 238 # ASSIGN : s_2_2 315 # ASSIGN : s_2_3 402 # ASSIGN : s_2_4 440 # ASSIGN : s_2_5 502 # ASSIGN : s_2_6 622 # ASSIGN : s_2_7 715 # ASSIGN : s_2_8 773 # ASSIGN : s_2_9 839 # ASSIGN : s_2_10 891 # ASSIGN : s_2_11 960 # ASSIGN : s_2_12 1029 # ASSIGN : s_2_13 1121 # ASSIGN : s_2_14 1246 # ASSIGN : s_3_0 16 # ASSIGN : s_3_1 93 # ASSIGN : s_3_2 466 # ASSIGN : s_3_3 571 # ASSIGN : s_3_4 578 # ASSIGN : s_3_5 680 # ASSIGN : s_3_6 733 # ASSIGN : s_3_7 795 # ASSIGN : s_3_8 871 # ASSIGN : s_3_9 908 # ASSIGN : s_3_10 1003 # ASSIGN : s_3_11 1046 # ASSIGN : s_3_12 1121 # ASSIGN : s_3_13 1182 # ASSIGN : s_3_14 1192 # ASSIGN : s_4_0 242 # ASSIGN : s_4_1 329 # ASSIGN : s_4_2 428 # ASSIGN : s_4_3 478 # ASSIGN : s_4_4 537 # ASSIGN : s_4_5 583 # ASSIGN : s_4_6 628 # ASSIGN : s_4_7 673 # ASSIGN : s_4_8 716 # ASSIGN : s_4_9 768 # ASSIGN : s_4_10 795 # ASSIGN : s_4_11 915 # ASSIGN : s_4_12 1153 # ASSIGN : s_4_13 1169 # ASSIGN : s_4_14 1232 # ASSIGN : s_5_0 73 # ASSIGN : s_5_1 197 # ASSIGN : s_5_2 500 # ASSIGN : s_5_3 614 # ASSIGN : s_5_4 794 # ASSIGN : s_5_5 808 # ASSIGN : s_5_6 816 # ASSIGN : s_5_7 858 # ASSIGN : s_5_8 886 # ASSIGN : s_5_9 985 # ASSIGN : s_5_10 1043 # ASSIGN : s_5_11 1132 # ASSIGN : s_5_12 1158 # ASSIGN : s_5_13 1195 # ASSIGN : s_5_14 1228 # ASSIGN : s_6_0 14 # ASSIGN : s_6_1 83 # ASSIGN : s_6_2 219 # ASSIGN : s_6_3 236 # ASSIGN : s_6_4 305 # ASSIGN : s_6_5 371 # ASSIGN : s_6_6 402 # ASSIGN : s_6_7 480 # ASSIGN : s_6_8 500 # ASSIGN : s_6_9 527 # ASSIGN : s_6_10 647 # ASSIGN : s_6_11 809 # ASSIGN : s_6_12 975 # ASSIGN : s_6_13 1051 # ASSIGN : s_6_14 1190 # ASSIGN : s_7_0 4 # ASSIGN : s_7_1 67 # ASSIGN : s_7_2 210 # ASSIGN : s_7_3 361 # ASSIGN : s_7_4 442 # ASSIGN : s_7_5 522 # ASSIGN : s_7_6 550 # ASSIGN : s_7_7 568 # ASSIGN : s_7_8 600 # ASSIGN : s_7_9 696 # ASSIGN : s_7_10 863 # ASSIGN : s_7_11 960 # ASSIGN : s_7_12 984 # ASSIGN : s_7_13 1033 # ASSIGN : s_7_14 1128 # ASSIGN : s_8_0 176 # ASSIGN : s_8_1 203 # ASSIGN : s_8_2 249 # ASSIGN : s_8_3 354 # ASSIGN : s_8_4 381 # ASSIGN : s_8_5 400 # ASSIGN : s_8_6 551 # ASSIGN : s_8_7 573 # ASSIGN : s_8_8 671 # ASSIGN : s_8_9 776 # ASSIGN : s_8_10 788 # ASSIGN : s_8_11 947 # ASSIGN : s_8_12 1071 # ASSIGN : s_8_13 1113 # ASSIGN : s_8_14 1161 # ASSIGN : s_9_0 29 # ASSIGN : s_9_1 96 # ASSIGN : s_9_2 179 # ASSIGN : s_9_3 295 # ASSIGN : s_9_4 350 # ASSIGN : s_9_5 400 # ASSIGN : s_9_6 494 # ASSIGN : s_9_7 508 # ASSIGN : s_9_8 549 # ASSIGN : s_9_9 621 # ASSIGN : s_9_10 671 # ASSIGN : s_9_11 732 # ASSIGN : s_9_12 811 # ASSIGN : s_9_13 1072 # ASSIGN : s_9_14 1208 # ASSIGN : s_10_0 28 # ASSIGN : s_10_1 93 # ASSIGN : s_10_2 189 # ASSIGN : s_10_3 254 # ASSIGN : s_10_4 343 # ASSIGN : s_10_5 485 # ASSIGN : s_10_6 543 # ASSIGN : s_10_7 576 # ASSIGN : s_10_8 836 # ASSIGN : s_10_9 861 # ASSIGN : s_10_10 893 # ASSIGN : s_10_11 1053 # ASSIGN : s_10_12 1145 # ASSIGN : s_10_13 1159 # ASSIGN : s_10_14 1211 # ASSIGN : s_11_0 169 # ASSIGN : s_11_1 268 # ASSIGN : s_11_2 442 # ASSIGN : s_11_3 685 # ASSIGN : s_11_4 736 # ASSIGN : s_11_5 814 # ASSIGN : s_11_6 858 # ASSIGN : s_11_7 866 # ASSIGN : s_11_8 883 # ASSIGN : s_11_9 980 # ASSIGN : s_11_10 1009 # ASSIGN : s_11_11 1024 # ASSIGN : s_11_12 1090 # ASSIGN : s_11_13 1147 # ASSIGN : s_11_14 1208 # ASSIGN : s_12_0 43 # ASSIGN : s_12_1 100 # ASSIGN : s_12_2 157 # ASSIGN : s_12_3 218 # ASSIGN : s_12_4 286 # ASSIGN : s_12_5 412 # ASSIGN : s_12_6 615 # ASSIGN : s_12_7 673 # ASSIGN : s_12_8 755 # ASSIGN : s_12_9 940 # ASSIGN : s_12_10 1018 # ASSIGN : s_12_11 1105 # ASSIGN : s_12_12 1126 # ASSIGN : s_12_13 1182 # ASSIGN : s_12_14 1214 # ASSIGN : s_13_0 176 # ASSIGN : s_13_1 260 # ASSIGN : s_13_2 331 # ASSIGN : s_13_3 346 # ASSIGN : s_13_4 737 # ASSIGN : s_13_5 798 # ASSIGN : s_13_6 880 # ASSIGN : s_13_7 909 # ASSIGN : s_13_8 979 # ASSIGN : s_13_9 1063 # ASSIGN : s_13_10 1093 # ASSIGN : s_13_11 1168 # ASSIGN : s_13_12 1191 # ASSIGN : s_13_13 1211 # ASSIGN : s_13_14 1233 # ASSIGN : s_14_0 2 # ASSIGN : s_14_1 39 # ASSIGN : s_14_2 120 # ASSIGN : s_14_3 181 # ASSIGN : s_14_4 238 # ASSIGN : s_14_5 348 # ASSIGN : s_14_6 465 # ASSIGN : s_14_7 624 # ASSIGN : s_14_8 686 # ASSIGN : s_14_9 721 # ASSIGN : s_14_10 773 # ASSIGN : s_14_11 956 # ASSIGN : s_14_12 1045 # ASSIGN : s_14_13 1099 # ASSIGN : s_14_14 1153 SHOW_RESULT 1271 END : 1271 (1 seconds) [Fri Jun 2 06:00:41 2006] SHOW_RESULT 1271 CPU : 1.08999999999997 = 1.08999999999997 + 0 + 0 + 0 # BOUND : makespan 1191 1271 MODIFY_CNF 1231 BEGIN : [Fri Jun 2 06:00:41 2006] MODIFY_CNF 1231 END : 139857443 bytes (0 seconds) [Fri Jun 2 06:00:41 2006] MODIFY_CNF 1231 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1231 BEGIN : [Fri Jun 2 06:00:41 2006] CMD : minisat /work/tamura/csp2sat103986.cnf /work/tamura/csp2sat103986.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1691632 4972626 | 563877 0 0 NaNQ | 0.000 % | | 100 | 1691632 4972626 | 620264 100 810 8.1 | 72.871 % | | 250 | 1691632 4972626 | 682291 250 2438 9.8 | 72.871 % | | 476 | 1691632 4972626 | 750520 476 4495 9.4 | 72.871 % | | 813 | 1691016 4970779 | 825572 812 7478 9.2 | 72.871 % | | 1319 | 1691016 4970779 | 908129 1318 12675 9.6 | 72.871 % | | 2079 | 1668826 4905186 | 998942 2036 20766 10.2 | 73.128 % | | 3218 | 1611267 4735334 | 1098836 2268 22523 9.9 | 78.357 % | ==============================================================================) restarts : 8 conflicts : 3245 (134 /sec) decisions : 4473 (185 /sec) propagations : 33458248 (1382473 /sec) inspects : 256257083 (10588376 /sec) conflict literals : 32369 (35.09 % deleted) CPU time : 24.2017 s UNSATISFIABLE VERIFY_CNF 1231 END : (26 seconds) [Fri Jun 2 06:01:07 2006] VERIFY_CNF 1231 CPU : 25.58 = 0.0100000000000477 + 0.03 + 25.4 + 0.14 # RESULT : makespan 1231 UNSATISFIABLE # BOUND : makespan 1232 1271 MODIFY_CNF 1251 BEGIN : [Fri Jun 2 06:01:07 2006] MODIFY_CNF 1251 END : 139857443 bytes (0 seconds) [Fri Jun 2 06:01:07 2006] MODIFY_CNF 1251 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1251 BEGIN : [Fri Jun 2 06:01:07 2006] CMD : minisat /work/tamura/csp2sat103986.cnf /work/tamura/csp2sat103986.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1766100 5191483 | 588700 0 0 NaNQ | 0.000 % | | 100 | 1766100 5191483 | 647570 100 883 8.8 | 71.675 % | | 252 | 1766100 5191483 | 712327 251 2479 9.9 | 71.676 % | | 477 | 1766100 5191483 | 783559 476 4261 9.0 | 71.676 % | | 814 | 1765448 5189529 | 861915 792 7464 9.4 | 71.676 % | | 1320 | 1765448 5189529 | 948107 1298 12883 9.9 | 71.676 % | | 2080 | 1765448 5189529 | 1042917 2058 22201 10.8 | 71.676 % | | 3219 | 1765448 5189529 | 1147209 3197 35673 11.2 | 71.676 % | | 4927 | 1765448 5189529 | 1261930 4905 54387 11.1 | 71.676 % | | 7490 | 1448308 4252147 | 1388123 1903 17778 9.3 | 75.399 % | ==============================================================================) restarts : 10 conflicts : 7565 (160 /sec) decisions : 10238 (217 /sec) propagations : 80423857 (1705307 /sec) inspects : 627995090 (13316008 /sec) conflict literals : 84360 (35.17 % deleted) CPU time : 47.1609 s UNSATISFIABLE VERIFY_CNF 1251 END : (49 seconds) [Fri Jun 2 06:01:56 2006] VERIFY_CNF 1251 CPU : 48.42 = 0 + 0.0199999999999999 + 48.26 + 0.14 # RESULT : makespan 1251 UNSATISFIABLE # BOUND : makespan 1252 1271 MODIFY_CNF 1261 BEGIN : [Fri Jun 2 06:01:56 2006] MODIFY_CNF 1261 END : 139857443 bytes (0 seconds) [Fri Jun 2 06:01:56 2006] MODIFY_CNF 1261 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1261 BEGIN : [Fri Jun 2 06:01:56 2006] CMD : minisat /work/tamura/csp2sat103986.cnf /work/tamura/csp2sat103986.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1813134 5330296 | 604378 0 0 NaNQ | 0.000 % | | 101 | 1813134 5330296 | 664815 101 1296 12.8 | 71.072 % | | 251 | 1813134 5330296 | 731297 251 3188 12.7 | 71.072 % | | 476 | 1813134 5330296 | 804427 475 4989 10.5 | 71.073 % | | 814 | 1812478 5328330 | 884869 801 8416 10.5 | 71.073 % | | 1321 | 1812478 5328330 | 973356 1308 12692 9.7 | 71.073 % | | 2080 | 1812478 5328330 | 1070692 2067 22129 10.7 | 71.073 % | | 3219 | 1812478 5328330 | 1177761 3206 36160 11.3 | 71.073 % | | 4927 | 1812478 5328330 | 1295537 4914 58061 11.8 | 71.073 % | | 7489 | 1736353 5103325 | 1425091 5430 65400 12.0 | 71.962 % | | 11334 | 1734318 5097278 | 1567600 8778 107768 12.3 | 71.977 % | ==============================================================================) restarts : 11 conflicts : 12844 (172 /sec) decisions : 17026 (228 /sec) propagations : 136595542 (1827270 /sec) inspects : 1079841140 (14445280 /sec) conflict literals : 160705 (37.35 % deleted) CPU time : 74.7539 s UNSATISFIABLE VERIFY_CNF 1261 END : (76 seconds) [Fri Jun 2 06:03:12 2006] VERIFY_CNF 1261 CPU : 76.12 = 0 + 0.02 + 75.96 + 0.14 # RESULT : makespan 1261 UNSATISFIABLE # BOUND : makespan 1262 1271 MODIFY_CNF 1266 BEGIN : [Fri Jun 2 06:03:12 2006] MODIFY_CNF 1266 END : 139857443 bytes (0 seconds) [Fri Jun 2 06:03:12 2006] MODIFY_CNF 1266 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1266 BEGIN : [Fri Jun 2 06:03:12 2006] CMD : minisat /work/tamura/csp2sat103986.cnf /work/tamura/csp2sat103986.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1831345 5383794 | 610448 0 0 NaNQ | 0.000 % | | 100 | 1831345 5383794 | 671492 99 1130 11.4 | 70.775 % | | 250 | 1831345 5383794 | 738642 249 2639 10.6 | 70.775 % | | 477 | 1831345 5383794 | 812506 476 5142 10.8 | 70.775 % | | 814 | 1830257 5380531 | 893756 813 8927 11.0 | 70.775 % | | 1320 | 1830257 5380531 | 983132 1319 13561 10.3 | 70.775 % | | 2081 | 1830257 5380531 | 1081445 2080 22718 10.9 | 70.775 % | | 3222 | 1830257 5380531 | 1189590 3221 39204 12.2 | 70.775 % | | 4930 | 1830257 5380531 | 1308549 4929 61247 12.4 | 70.775 % | | 7492 | 1815371 5336584 | 1439404 6182 76437 12.4 | 70.962 % | | 11336 | 1815371 5336584 | 1583344 10026 126700 12.6 | 70.962 % | ==============================================================================) restarts : 11 conflicts : 14858 (178 /sec) decisions : 19929 (239 /sec) propagations : 149070278 (1790145 /sec) inspects : 1227416168 (14739712 /sec) conflict literals : 187346 (34.78 % deleted) CPU time : 83.2727 s UNSATISFIABLE VERIFY_CNF 1266 END : (85 seconds) [Fri Jun 2 06:04:37 2006] VERIFY_CNF 1266 CPU : 84.63 = 0.00999999999999091 + 0.01 + 84.47 + 0.14 # RESULT : makespan 1266 UNSATISFIABLE # BOUND : makespan 1267 1271 MODIFY_CNF 1269 BEGIN : [Fri Jun 2 06:04:37 2006] MODIFY_CNF 1269 END : 139857443 bytes (0 seconds) [Fri Jun 2 06:04:37 2006] MODIFY_CNF 1269 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1269 BEGIN : [Fri Jun 2 06:04:37 2006] CMD : minisat /work/tamura/csp2sat103986.cnf /work/tamura/csp2sat103986.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1841969 5414986 | 613989 0 0 NaNQ | 0.000 % | | 100 | 1841969 5414986 | 675387 99 1388 14.0 | 70.596 % | | 250 | 1841969 5414986 | 742926 249 3466 13.9 | 70.596 % | | 475 | 1841969 5414986 | 817219 474 6129 12.9 | 70.596 % | | 812 | 1840878 5411714 | 898941 811 8940 11.0 | 70.596 % | | 1319 | 1840878 5411714 | 988835 1318 15449 11.7 | 70.596 % | | 2078 | 1840878 5411714 | 1087718 2077 24910 12.0 | 70.596 % | | 3218 | 1840878 5411714 | 1196490 3217 38268 11.9 | 70.596 % | | 4926 | 1840243 5409810 | 1316139 4357 51684 11.9 | 70.596 % | | 7488 | 1840243 5409810 | 1447753 6919 86402 12.5 | 70.596 % | ==============================================================================) restarts : 10 conflicts : 8308 (148 /sec) decisions : 11893 (211 /sec) propagations : 95434870 (1695616 /sec) inspects : 780759283 (13871954 /sec) conflict literals : 104313 (34.67 % deleted) CPU time : 56.2833 s SATISFIABLE VERIFY_CNF 1269 END : (59 seconds) [Fri Jun 2 06:05:36 2006] VERIFY_CNF 1269 CPU : 57.83 = 0 + 0.02 + 57.65 + 0.16 # RESULT : makespan 1269 SATISFIABLE SHOW_RESULT 1269 BEGIN : [Fri Jun 2 06:05:36 2006] # ASSIGN : makespan 1269 # ASSIGN : s_0_0 2 # ASSIGN : s_0_1 178 # ASSIGN : s_0_2 233 # ASSIGN : s_0_3 304 # ASSIGN : s_0_4 402 # ASSIGN : s_0_5 414 # ASSIGN : s_0_6 486 # ASSIGN : s_0_7 530 # ASSIGN : s_0_8 553 # ASSIGN : s_0_9 606 # ASSIGN : s_0_10 632 # ASSIGN : s_0_11 712 # ASSIGN : s_0_12 1063 # ASSIGN : s_0_13 1136 # ASSIGN : s_0_14 1230 # ASSIGN : s_1_0 64 # ASSIGN : s_1_1 355 # ASSIGN : s_1_2 453 # ASSIGN : s_1_3 534 # ASSIGN : s_1_4 598 # ASSIGN : s_1_5 638 # ASSIGN : s_1_6 717 # ASSIGN : s_1_7 760 # ASSIGN : s_1_8 815 # ASSIGN : s_1_9 892 # ASSIGN : s_1_10 911 # ASSIGN : s_1_11 948 # ASSIGN : s_1_12 1027 # ASSIGN : s_1_13 1141 # ASSIGN : s_1_14 1203 # ASSIGN : s_2_0 75 # ASSIGN : s_2_1 158 # ASSIGN : s_2_2 312 # ASSIGN : s_2_3 399 # ASSIGN : s_2_4 438 # ASSIGN : s_2_5 503 # ASSIGN : s_2_6 661 # ASSIGN : s_2_7 754 # ASSIGN : s_2_8 771 # ASSIGN : s_2_9 840 # ASSIGN : s_2_10 892 # ASSIGN : s_2_11 961 # ASSIGN : s_2_12 1095 # ASSIGN : s_2_13 1119 # ASSIGN : s_2_14 1244 # ASSIGN : s_3_0 1 # ASSIGN : s_3_1 92 # ASSIGN : s_3_2 458 # ASSIGN : s_3_3 491 # ASSIGN : s_3_4 498 # ASSIGN : s_3_5 614 # ASSIGN : s_3_6 649 # ASSIGN : s_3_7 684 # ASSIGN : s_3_8 760 # ASSIGN : s_3_9 769 # ASSIGN : s_3_10 864 # ASSIGN : s_3_11 1044 # ASSIGN : s_3_12 1119 # ASSIGN : s_3_13 1180 # ASSIGN : s_3_14 1190 # ASSIGN : s_4_0 165 # ASSIGN : s_4_1 252 # ASSIGN : s_4_2 398 # ASSIGN : s_4_3 448 # ASSIGN : s_4_4 507 # ASSIGN : s_4_5 584 # ASSIGN : s_4_6 629 # ASSIGN : s_4_7 671 # ASSIGN : s_4_8 714 # ASSIGN : s_4_9 766 # ASSIGN : s_4_10 793 # ASSIGN : s_4_11 984 # ASSIGN : s_4_12 1045 # ASSIGN : s_4_13 1082 # ASSIGN : s_4_14 1141 # ASSIGN : s_5_0 72 # ASSIGN : s_5_1 241 # ASSIGN : s_5_2 593 # ASSIGN : s_5_3 681 # ASSIGN : s_5_4 747 # ASSIGN : s_5_5 761 # ASSIGN : s_5_6 814 # ASSIGN : s_5_7 856 # ASSIGN : s_5_8 884 # ASSIGN : s_5_9 983 # ASSIGN : s_5_10 1041 # ASSIGN : s_5_11 1130 # ASSIGN : s_5_12 1156 # ASSIGN : s_5_13 1193 # ASSIGN : s_5_14 1226 # ASSIGN : s_6_0 12 # ASSIGN : s_6_1 81 # ASSIGN : s_6_2 218 # ASSIGN : s_6_3 235 # ASSIGN : s_6_4 304 # ASSIGN : s_6_5 371 # ASSIGN : s_6_6 402 # ASSIGN : s_6_7 480 # ASSIGN : s_6_8 500 # ASSIGN : s_6_9 527 # ASSIGN : s_6_10 667 # ASSIGN : s_6_11 864 # ASSIGN : s_6_12 1018 # ASSIGN : s_6_13 1094 # ASSIGN : s_6_14 1188 # ASSIGN : s_7_0 23 # ASSIGN : s_7_1 84 # ASSIGN : s_7_2 179 # ASSIGN : s_7_3 356 # ASSIGN : s_7_4 437 # ASSIGN : s_7_5 523 # ASSIGN : s_7_6 551 # ASSIGN : s_7_7 569 # ASSIGN : s_7_8 601 # ASSIGN : s_7_9 760 # ASSIGN : s_7_10 859 # ASSIGN : s_7_11 958 # ASSIGN : s_7_12 982 # ASSIGN : s_7_13 1031 # ASSIGN : s_7_14 1185 # ASSIGN : s_8_0 262 # ASSIGN : s_8_1 289 # ASSIGN : s_8_2 335 # ASSIGN : s_8_3 481 # ASSIGN : s_8_4 508 # ASSIGN : s_8_5 597 # ASSIGN : s_8_6 682 # ASSIGN : s_8_7 699 # ASSIGN : s_8_8 805 # ASSIGN : s_8_9 944 # ASSIGN : s_8_10 956 # ASSIGN : s_8_11 984 # ASSIGN : s_8_12 1092 # ASSIGN : s_8_13 1140 # ASSIGN : s_8_14 1219 # ASSIGN : s_9_0 27 # ASSIGN : s_9_1 78 # ASSIGN : s_9_2 177 # ASSIGN : s_9_3 294 # ASSIGN : s_9_4 349 # ASSIGN : s_9_5 408 # ASSIGN : s_9_6 502 # ASSIGN : s_9_7 516 # ASSIGN : s_9_8 557 # ASSIGN : s_9_9 645 # ASSIGN : s_9_10 695 # ASSIGN : s_9_11 905 # ASSIGN : s_9_12 996 # ASSIGN : s_9_13 1180 # ASSIGN : s_9_14 1206 # ASSIGN : s_10_0 17 # ASSIGN : s_10_1 82 # ASSIGN : s_10_2 188 # ASSIGN : s_10_3 280 # ASSIGN : s_10_4 430 # ASSIGN : s_10_5 499 # ASSIGN : s_10_6 563 # ASSIGN : s_10_7 596 # ASSIGN : s_10_8 753 # ASSIGN : s_10_9 775 # ASSIGN : s_10_10 807 # ASSIGN : s_10_11 902 # ASSIGN : s_10_12 982 # ASSIGN : s_10_13 1178 # ASSIGN : s_10_14 1209 # ASSIGN : s_11_0 160 # ASSIGN : s_11_1 194 # ASSIGN : s_11_2 587 # ASSIGN : s_11_3 661 # ASSIGN : s_11_4 734 # ASSIGN : s_11_5 812 # ASSIGN : s_11_6 859 # ASSIGN : s_11_7 867 # ASSIGN : s_11_8 884 # ASSIGN : s_11_9 981 # ASSIGN : s_11_10 1010 # ASSIGN : s_11_11 1025 # ASSIGN : s_11_12 1094 # ASSIGN : s_11_13 1134 # ASSIGN : s_11_14 1206 # ASSIGN : s_12_0 32 # ASSIGN : s_12_1 117 # ASSIGN : s_12_2 174 # ASSIGN : s_12_3 235 # ASSIGN : s_12_4 255 # ASSIGN : s_12_5 340 # ASSIGN : s_12_6 613 # ASSIGN : s_12_7 671 # ASSIGN : s_12_8 756 # ASSIGN : s_12_9 938 # ASSIGN : s_12_10 1016 # ASSIGN : s_12_11 1103 # ASSIGN : s_12_12 1124 # ASSIGN : s_12_13 1180 # ASSIGN : s_12_14 1212 # ASSIGN : s_13_0 175 # ASSIGN : s_13_1 259 # ASSIGN : s_13_2 443 # ASSIGN : s_13_3 458 # ASSIGN : s_13_4 677 # ASSIGN : s_13_5 796 # ASSIGN : s_13_6 878 # ASSIGN : s_13_7 907 # ASSIGN : s_13_8 977 # ASSIGN : s_13_9 1061 # ASSIGN : s_13_10 1091 # ASSIGN : s_13_11 1155 # ASSIGN : s_13_12 1178 # ASSIGN : s_13_13 1198 # ASSIGN : s_13_14 1231 # ASSIGN : s_14_0 0 # ASSIGN : s_14_1 37 # ASSIGN : s_14_2 118 # ASSIGN : s_14_3 180 # ASSIGN : s_14_4 237 # ASSIGN : s_14_5 356 # ASSIGN : s_14_6 460 # ASSIGN : s_14_7 625 # ASSIGN : s_14_8 687 # ASSIGN : s_14_9 741 # ASSIGN : s_14_10 799 # ASSIGN : s_14_11 837 # ASSIGN : s_14_12 1082 # ASSIGN : s_14_13 1136 # ASSIGN : s_14_14 1210 SHOW_RESULT 1269 END : 1269 (1 seconds) [Fri Jun 2 06:05:37 2006] SHOW_RESULT 1269 CPU : 1.08999999999998 = 1.07999999999998 + 0.01 + 0 + 0 # BOUND : makespan 1267 1269 MODIFY_CNF 1268 BEGIN : [Fri Jun 2 06:05:37 2006] MODIFY_CNF 1268 END : 139857443 bytes (0 seconds) [Fri Jun 2 06:05:37 2006] MODIFY_CNF 1268 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1268 BEGIN : [Fri Jun 2 06:05:37 2006] CMD : minisat /work/tamura/csp2sat103986.cnf /work/tamura/csp2sat103986.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1837100 5400607 | 612366 0 0 NaNQ | 0.000 % | | 102 | 1837100 5400607 | 673602 101 1912 18.9 | 70.656 % | | 252 | 1837100 5400607 | 740962 251 3962 15.8 | 70.656 % | | 477 | 1837100 5400607 | 815059 476 7133 15.0 | 70.656 % | | 815 | 1836010 5397338 | 896565 814 10316 12.7 | 70.656 % | | 1321 | 1836010 5397338 | 986221 1320 16599 12.6 | 70.656 % | | 2080 | 1836010 5397338 | 1084843 2079 24652 11.9 | 70.656 % | | 3219 | 1836010 5397338 | 1193328 3218 38587 12.0 | 70.656 % | | 4927 | 1836010 5397338 | 1312660 4926 58130 11.8 | 70.656 % | | 7489 | 1835341 5395333 | 1443926 7370 93731 12.7 | 70.657 % | ==============================================================================) restarts : 10 conflicts : 10152 (166 /sec) decisions : 14186 (231 /sec) propagations : 106338015 (1735076 /sec) inspects : 887760647 (14485245 /sec) conflict literals : 134767 (31.60 % deleted) CPU time : 61.2872 s SATISFIABLE VERIFY_CNF 1268 END : (63 seconds) [Fri Jun 2 06:06:40 2006] VERIFY_CNF 1268 CPU : 63.2 = 0.00999999999999091 + 0.03 + 62.66 + 0.5 # RESULT : makespan 1268 SATISFIABLE SHOW_RESULT 1268 BEGIN : [Fri Jun 2 06:06:40 2006] # ASSIGN : makespan 1268 # ASSIGN : s_0_0 1 # ASSIGN : s_0_1 176 # ASSIGN : s_0_2 231 # ASSIGN : s_0_3 302 # ASSIGN : s_0_4 400 # ASSIGN : s_0_5 412 # ASSIGN : s_0_6 446 # ASSIGN : s_0_7 529 # ASSIGN : s_0_8 552 # ASSIGN : s_0_9 605 # ASSIGN : s_0_10 631 # ASSIGN : s_0_11 711 # ASSIGN : s_0_12 1062 # ASSIGN : s_0_13 1135 # ASSIGN : s_0_14 1229 # ASSIGN : s_1_0 64 # ASSIGN : s_1_1 354 # ASSIGN : s_1_2 452 # ASSIGN : s_1_3 533 # ASSIGN : s_1_4 597 # ASSIGN : s_1_5 637 # ASSIGN : s_1_6 716 # ASSIGN : s_1_7 759 # ASSIGN : s_1_8 814 # ASSIGN : s_1_9 891 # ASSIGN : s_1_10 910 # ASSIGN : s_1_11 947 # ASSIGN : s_1_12 1026 # ASSIGN : s_1_13 1140 # ASSIGN : s_1_14 1202 # ASSIGN : s_2_0 91 # ASSIGN : s_2_1 188 # ASSIGN : s_2_2 311 # ASSIGN : s_2_3 398 # ASSIGN : s_2_4 437 # ASSIGN : s_2_5 502 # ASSIGN : s_2_6 654 # ASSIGN : s_2_7 747 # ASSIGN : s_2_8 764 # ASSIGN : s_2_9 830 # ASSIGN : s_2_10 891 # ASSIGN : s_2_11 960 # ASSIGN : s_2_12 1094 # ASSIGN : s_2_13 1118 # ASSIGN : s_2_14 1243 # ASSIGN : s_3_0 4 # ASSIGN : s_3_1 91 # ASSIGN : s_3_2 462 # ASSIGN : s_3_3 490 # ASSIGN : s_3_4 497 # ASSIGN : s_3_5 613 # ASSIGN : s_3_6 648 # ASSIGN : s_3_7 683 # ASSIGN : s_3_8 759 # ASSIGN : s_3_9 768 # ASSIGN : s_3_10 863 # ASSIGN : s_3_11 1043 # ASSIGN : s_3_12 1118 # ASSIGN : s_3_13 1179 # ASSIGN : s_3_14 1189 # ASSIGN : s_4_0 239 # ASSIGN : s_4_1 326 # ASSIGN : s_4_2 397 # ASSIGN : s_4_3 447 # ASSIGN : s_4_4 506 # ASSIGN : s_4_5 583 # ASSIGN : s_4_6 628 # ASSIGN : s_4_7 669 # ASSIGN : s_4_8 712 # ASSIGN : s_4_9 765 # ASSIGN : s_4_10 792 # ASSIGN : s_4_11 915 # ASSIGN : s_4_12 1044 # ASSIGN : s_4_13 1099 # ASSIGN : s_4_14 1158 # ASSIGN : s_5_0 71 # ASSIGN : s_5_1 193 # ASSIGN : s_5_2 592 # ASSIGN : s_5_3 680 # ASSIGN : s_5_4 746 # ASSIGN : s_5_5 760 # ASSIGN : s_5_6 816 # ASSIGN : s_5_7 863 # ASSIGN : s_5_8 922 # ASSIGN : s_5_9 982 # ASSIGN : s_5_10 1040 # ASSIGN : s_5_11 1129 # ASSIGN : s_5_12 1155 # ASSIGN : s_5_13 1192 # ASSIGN : s_5_14 1225 # ASSIGN : s_6_0 11 # ASSIGN : s_6_1 80 # ASSIGN : s_6_2 217 # ASSIGN : s_6_3 234 # ASSIGN : s_6_4 303 # ASSIGN : s_6_5 370 # ASSIGN : s_6_6 401 # ASSIGN : s_6_7 479 # ASSIGN : s_6_8 499 # ASSIGN : s_6_9 526 # ASSIGN : s_6_10 666 # ASSIGN : s_6_11 806 # ASSIGN : s_6_12 1017 # ASSIGN : s_6_13 1093 # ASSIGN : s_6_14 1187 # ASSIGN : s_7_0 22 # ASSIGN : s_7_1 114 # ASSIGN : s_7_2 209 # ASSIGN : s_7_3 355 # ASSIGN : s_7_4 436 # ASSIGN : s_7_5 522 # ASSIGN : s_7_6 550 # ASSIGN : s_7_7 568 # ASSIGN : s_7_8 600 # ASSIGN : s_7_9 759 # ASSIGN : s_7_10 858 # ASSIGN : s_7_11 957 # ASSIGN : s_7_12 981 # ASSIGN : s_7_13 1030 # ASSIGN : s_7_14 1184 # ASSIGN : s_8_0 161 # ASSIGN : s_8_1 288 # ASSIGN : s_8_2 334 # ASSIGN : s_8_3 480 # ASSIGN : s_8_4 507 # ASSIGN : s_8_5 605 # ASSIGN : s_8_6 749 # ASSIGN : s_8_7 766 # ASSIGN : s_8_8 881 # ASSIGN : s_8_9 943 # ASSIGN : s_8_10 955 # ASSIGN : s_8_11 983 # ASSIGN : s_8_12 1091 # ASSIGN : s_8_13 1139 # ASSIGN : s_8_14 1218 # ASSIGN : s_9_0 27 # ASSIGN : s_9_1 81 # ASSIGN : s_9_2 176 # ASSIGN : s_9_3 293 # ASSIGN : s_9_4 348 # ASSIGN : s_9_5 407 # ASSIGN : s_9_6 501 # ASSIGN : s_9_7 515 # ASSIGN : s_9_8 556 # ASSIGN : s_9_9 635 # ASSIGN : s_9_10 685 # ASSIGN : s_9_11 836 # ASSIGN : s_9_12 981 # ASSIGN : s_9_13 1140 # ASSIGN : s_9_14 1205 # ASSIGN : s_10_0 15 # ASSIGN : s_10_1 80 # ASSIGN : s_10_2 187 # ASSIGN : s_10_3 251 # ASSIGN : s_10_4 343 # ASSIGN : s_10_5 498 # ASSIGN : s_10_6 562 # ASSIGN : s_10_7 595 # ASSIGN : s_10_8 782 # ASSIGN : s_10_9 804 # ASSIGN : s_10_10 890 # ASSIGN : s_10_11 1000 # ASSIGN : s_10_12 1079 # ASSIGN : s_10_13 1177 # ASSIGN : s_10_14 1208 # ASSIGN : s_11_0 230 # ASSIGN : s_11_1 264 # ASSIGN : s_11_2 441 # ASSIGN : s_11_3 660 # ASSIGN : s_11_4 733 # ASSIGN : s_11_5 805 # ASSIGN : s_11_6 849 # ASSIGN : s_11_7 857 # ASSIGN : s_11_8 874 # ASSIGN : s_11_9 971 # ASSIGN : s_11_10 1009 # ASSIGN : s_11_11 1024 # ASSIGN : s_11_12 1093 # ASSIGN : s_11_13 1133 # ASSIGN : s_11_14 1205 # ASSIGN : s_12_0 30 # ASSIGN : s_12_1 147 # ASSIGN : s_12_2 204 # ASSIGN : s_12_3 265 # ASSIGN : s_12_4 285 # ASSIGN : s_12_5 412 # ASSIGN : s_12_6 612 # ASSIGN : s_12_7 670 # ASSIGN : s_12_8 746 # ASSIGN : s_12_9 883 # ASSIGN : s_12_10 1015 # ASSIGN : s_12_11 1102 # ASSIGN : s_12_12 1123 # ASSIGN : s_12_13 1179 # ASSIGN : s_12_14 1211 # ASSIGN : s_13_0 174 # ASSIGN : s_13_1 258 # ASSIGN : s_13_2 442 # ASSIGN : s_13_3 457 # ASSIGN : s_13_4 544 # ASSIGN : s_13_5 795 # ASSIGN : s_13_6 877 # ASSIGN : s_13_7 906 # ASSIGN : s_13_8 976 # ASSIGN : s_13_9 1060 # ASSIGN : s_13_10 1090 # ASSIGN : s_13_11 1154 # ASSIGN : s_13_12 1177 # ASSIGN : s_13_13 1197 # ASSIGN : s_13_14 1230 # ASSIGN : s_14_0 0 # ASSIGN : s_14_1 37 # ASSIGN : s_14_2 118 # ASSIGN : s_14_3 179 # ASSIGN : s_14_4 236 # ASSIGN : s_14_5 355 # ASSIGN : s_14_6 459 # ASSIGN : s_14_7 624 # ASSIGN : s_14_8 686 # ASSIGN : s_14_9 740 # ASSIGN : s_14_10 825 # ASSIGN : s_14_11 956 # ASSIGN : s_14_12 1081 # ASSIGN : s_14_13 1135 # ASSIGN : s_14_14 1209 SHOW_RESULT 1268 END : 1268 (1 seconds) [Fri Jun 2 06:06:41 2006] SHOW_RESULT 1268 CPU : 1.10000000000002 = 1.10000000000002 + 0 + 0 + 0 # BOUND : makespan 1267 1268 MODIFY_CNF 1267 BEGIN : [Fri Jun 2 06:06:41 2006] MODIFY_CNF 1267 END : 139857443 bytes (0 seconds) [Fri Jun 2 06:06:41 2006] MODIFY_CNF 1267 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1267 BEGIN : [Fri Jun 2 06:06:41 2006] CMD : minisat /work/tamura/csp2sat103986.cnf /work/tamura/csp2sat103986.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1834233 5392232 | 611411 0 0 NaNQ | 0.000 % | | 102 | 1834233 5392232 | 672552 101 1537 15.2 | 70.715 % | | 252 | 1834233 5392232 | 739807 251 3333 13.3 | 70.715 % | | 477 | 1834233 5392232 | 813788 476 5512 11.6 | 70.715 % | | 815 | 1833144 5388966 | 895166 813 8307 10.2 | 70.716 % | | 1321 | 1833144 5388966 | 984683 1319 14166 10.7 | 70.716 % | | 2080 | 1832476 5386964 | 1083151 1900 19305 10.2 | 70.716 % | | 3221 | 1832476 5386964 | 1191467 3041 33405 11.0 | 70.716 % | | 4929 | 1832476 5386964 | 1310613 4749 50868 10.7 | 70.716 % | | 7491 | 1832476 5386964 | 1441675 7311 85545 11.7 | 70.716 % | | 11336 | 1832476 5386964 | 1585842 11156 134068 12.0 | 70.716 % | ==============================================================================) restarts : 11 conflicts : 16210 (176 /sec) decisions : 21215 (230 /sec) propagations : 166716616 (1809020 /sec) inspects : 1370501832 (14871133 /sec) conflict literals : 201061 (33.80 % deleted) CPU time : 92.1585 s UNSATISFIABLE VERIFY_CNF 1267 END : (94 seconds) [Fri Jun 2 06:08:15 2006] VERIFY_CNF 1267 CPU : 93.51 = 0 + 0.0299999999999999 + 93.33 + 0.15 # RESULT : makespan 1267 UNSATISFIABLE # BOUND : makespan 1268 1268 MAIN END : (847 seconds) [Fri Jun 2 06:08:15 2006] MAIN CPU : 843.44 = 295.4 + 0.65 + 545.24 + 2.15