MAIN BEGIN : [Thu Jun 1 17:22:13 2006] READ BEGIN : csp/la26.csp [Thu Jun 1 17:22:13 2006] READ END : csp/la26.csp (6 seconds) [Thu Jun 1 17:22:19 2006] READ CPU : 5.41 = 5.4 + 0.00999999999999998 + 0 + 0 # BOUND : makespan 1218 1479 GENERATE_CNF 1479 BEGIN : [Thu Jun 1 17:22:19 2006] GENERATE_CNF 1479 END : 300463 variables 5988807 clauses 142852033 bytes (295 seconds) [Thu Jun 1 17:27:14 2006] GENERATE_CNF 1479 CPU : 294.92 = 294.51 + 0.41 + 0 + 0 MODIFY_CNF 1348 BEGIN : [Thu Jun 1 17:27:14 2006] MODIFY_CNF 1348 END : 142852039 bytes (0 seconds) [Thu Jun 1 17:27:14 2006] MODIFY_CNF 1348 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1348 BEGIN : [Thu Jun 1 17:27:14 2006] CMD : minisat /work/tamura/csp2sat78524.cnf /work/tamura/csp2sat78524.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 3725970 11011026 | 1241990 0 0 NaNQ | 0.000 % | | 100 | 3725970 11011026 | 1366189 100 2091 20.9 | 43.960 % | | 250 | 3725970 11011026 | 1502807 250 5257 21.0 | 43.960 % | ==============================================================================) restarts : 3 conflicts : 350 (35 /sec) decisions : 1296 (128 /sec) propagations : 3134676 (309953 /sec) inspects : 47625327 (4709130 /sec) conflict literals : 6872 (13.37 % deleted) CPU time : 10.1134 s SATISFIABLE VERIFY_CNF 1348 END : (13 seconds) [Thu Jun 1 17:27:27 2006] VERIFY_CNF 1348 CPU : 12.47 = 0.00999999999999091 + 0.01 + 12.32 + 0.13 # RESULT : makespan 1348 SATISFIABLE SHOW_RESULT 1348 BEGIN : [Thu Jun 1 17:27:27 2006] # ASSIGN : makespan 1348 # ASSIGN : s_0_0 33 # ASSIGN : s_0_1 97 # ASSIGN : s_0_2 229 # ASSIGN : s_0_3 402 # ASSIGN : s_0_4 424 # ASSIGN : s_0_5 512 # ASSIGN : s_0_6 533 # ASSIGN : s_0_7 759 # ASSIGN : s_0_8 1099 # ASSIGN : s_0_9 1293 # ASSIGN : s_1_0 537 # ASSIGN : s_1_1 628 # ASSIGN : s_1_2 726 # ASSIGN : s_1_3 765 # ASSIGN : s_1_4 844 # ASSIGN : s_1_5 856 # ASSIGN : s_1_6 933 # ASSIGN : s_1_7 1011 # ASSIGN : s_1_8 1275 # ASSIGN : s_1_9 1306 # ASSIGN : s_2_0 393 # ASSIGN : s_2_1 445 # ASSIGN : s_2_2 546 # ASSIGN : s_2_3 656 # ASSIGN : s_2_4 729 # ASSIGN : s_2_5 751 # ASSIGN : s_2_6 857 # ASSIGN : s_2_7 1008 # ASSIGN : s_2_8 1067 # ASSIGN : s_2_9 1201 # ASSIGN : s_3_0 36 # ASSIGN : s_3_1 123 # ASSIGN : s_3_2 534 # ASSIGN : s_3_3 630 # ASSIGN : s_3_4 700 # ASSIGN : s_3_5 794 # ASSIGN : s_3_6 832 # ASSIGN : s_3_7 892 # ASSIGN : s_3_8 942 # ASSIGN : s_3_9 1042 # ASSIGN : s_4_0 87 # ASSIGN : s_4_1 200 # ASSIGN : s_4_2 300 # ASSIGN : s_4_3 418 # ASSIGN : s_4_4 535 # ASSIGN : s_4_5 584 # ASSIGN : s_4_6 626 # ASSIGN : s_4_7 705 # ASSIGN : s_4_8 950 # ASSIGN : s_4_9 1102 # ASSIGN : s_5_0 681 # ASSIGN : s_5_1 688 # ASSIGN : s_5_2 749 # ASSIGN : s_5_3 874 # ASSIGN : s_5_4 931 # ASSIGN : s_5_5 941 # ASSIGN : s_5_6 1014 # ASSIGN : s_5_7 1042 # ASSIGN : s_5_8 1139 # ASSIGN : s_5_9 1339 # ASSIGN : s_6_0 15 # ASSIGN : s_6_1 74 # ASSIGN : s_6_2 121 # ASSIGN : s_6_3 303 # ASSIGN : s_6_4 375 # ASSIGN : s_6_5 465 # ASSIGN : s_6_6 487 # ASSIGN : s_6_7 748 # ASSIGN : s_6_8 1263 # ASSIGN : s_6_9 1313 # ASSIGN : s_7_0 108 # ASSIGN : s_7_1 117 # ASSIGN : s_7_2 261 # ASSIGN : s_7_3 301 # ASSIGN : s_7_4 425 # ASSIGN : s_7_5 490 # ASSIGN : s_7_6 809 # ASSIGN : s_7_7 940 # ASSIGN : s_7_8 1027 # ASSIGN : s_7_9 1309 # ASSIGN : s_8_0 272 # ASSIGN : s_8_1 333 # ASSIGN : s_8_2 627 # ASSIGN : s_8_3 787 # ASSIGN : s_8_4 1025 # ASSIGN : s_8_5 1118 # ASSIGN : s_8_6 1144 # ASSIGN : s_8_7 1177 # ASSIGN : s_8_8 1295 # ASSIGN : s_8_9 1340 # ASSIGN : s_9_0 592 # ASSIGN : s_9_1 699 # ASSIGN : s_9_2 747 # ASSIGN : s_9_3 825 # ASSIGN : s_9_4 909 # ASSIGN : s_9_5 1003 # ASSIGN : s_9_6 1072 # ASSIGN : s_9_7 1146 # ASSIGN : s_9_8 1234 # ASSIGN : s_9_9 1279 # ASSIGN : s_10_0 99 # ASSIGN : s_10_1 123 # ASSIGN : s_10_2 160 # ASSIGN : s_10_3 185 # ASSIGN : s_10_4 202 # ASSIGN : s_10_5 751 # ASSIGN : s_10_6 938 # ASSIGN : s_10_7 1159 # ASSIGN : s_10_8 1228 # ASSIGN : s_10_9 1259 # ASSIGN : s_11_0 135 # ASSIGN : s_11_1 225 # ASSIGN : s_11_2 300 # ASSIGN : s_11_3 372 # ASSIGN : s_11_4 458 # ASSIGN : s_11_5 481 # ASSIGN : s_11_6 580 # ASSIGN : s_11_7 668 # ASSIGN : s_11_8 878 # ASSIGN : s_11_9 1041 # ASSIGN : s_12_0 368 # ASSIGN : s_12_1 780 # ASSIGN : s_12_2 882 # ASSIGN : s_12_3 930 # ASSIGN : s_12_4 976 # ASSIGN : s_12_5 1010 # ASSIGN : s_12_6 1077 # ASSIGN : s_12_7 1185 # ASSIGN : s_12_8 1227 # ASSIGN : s_12_9 1301 # ASSIGN : s_13_0 5 # ASSIGN : s_13_1 85 # ASSIGN : s_13_2 136 # ASSIGN : s_13_3 155 # ASSIGN : s_13_4 253 # ASSIGN : s_13_5 281 # ASSIGN : s_13_6 331 # ASSIGN : s_13_7 427 # ASSIGN : s_13_8 839 # ASSIGN : s_13_9 851 # ASSIGN : s_14_0 2 # ASSIGN : s_14_1 167 # ASSIGN : s_14_2 242 # ASSIGN : s_14_3 399 # ASSIGN : s_14_4 710 # ASSIGN : s_14_5 824 # ASSIGN : s_14_6 924 # ASSIGN : s_14_7 938 # ASSIGN : s_14_8 993 # ASSIGN : s_14_9 1265 # ASSIGN : s_15_0 289 # ASSIGN : s_15_1 385 # ASSIGN : s_15_2 430 # ASSIGN : s_15_3 487 # ASSIGN : s_15_4 885 # ASSIGN : s_15_5 967 # ASSIGN : s_15_6 1078 # ASSIGN : s_15_7 1157 # ASSIGN : s_15_8 1266 # ASSIGN : s_15_9 1326 # ASSIGN : s_16_0 5 # ASSIGN : s_16_1 50 # ASSIGN : s_16_2 275 # ASSIGN : s_16_3 850 # ASSIGN : s_16_4 923 # ASSIGN : s_16_5 1060 # ASSIGN : s_16_6 1118 # ASSIGN : s_16_7 1152 # ASSIGN : s_16_8 1206 # ASSIGN : s_16_9 1275 # ASSIGN : s_17_0 124 # ASSIGN : s_17_1 261 # ASSIGN : s_17_2 399 # ASSIGN : s_17_3 416 # ASSIGN : s_17_4 478 # ASSIGN : s_17_5 544 # ASSIGN : s_17_6 601 # ASSIGN : s_17_7 630 # ASSIGN : s_17_8 1190 # ASSIGN : s_17_9 1198 # ASSIGN : s_18_0 28 # ASSIGN : s_18_1 86 # ASSIGN : s_18_2 179 # ASSIGN : s_18_3 272 # ASSIGN : s_18_4 359 # ASSIGN : s_18_5 559 # ASSIGN : s_18_6 662 # ASSIGN : s_18_7 719 # ASSIGN : s_18_8 988 # ASSIGN : s_18_9 1328 # ASSIGN : s_19_0 168 # ASSIGN : s_19_1 253 # ASSIGN : s_19_2 337 # ASSIGN : s_19_3 404 # ASSIGN : s_19_4 495 # ASSIGN : s_19_5 510 # ASSIGN : s_19_6 580 # ASSIGN : s_19_7 610 # ASSIGN : s_19_8 825 # ASSIGN : s_19_9 1328 SHOW_RESULT 1348 END : 1348 (1 seconds) [Thu Jun 1 17:27:28 2006] SHOW_RESULT 1348 CPU : 0.839999999999984 = 0.829999999999984 + 0.01 + 0 + 0 # BOUND : makespan 1218 1348 MODIFY_CNF 1283 BEGIN : [Thu Jun 1 17:27:28 2006] MODIFY_CNF 1283 END : 142852038 bytes (0 seconds) [Thu Jun 1 17:27:28 2006] MODIFY_CNF 1283 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1283 BEGIN : [Thu Jun 1 17:27:28 2006] CMD : minisat /work/tamura/csp2sat78524.cnf /work/tamura/csp2sat78524.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 3461049 10229336 | 1153683 0 0 NaNQ | 0.000 % | | 101 | 3461049 10229336 | 1269051 101 1151 11.4 | 48.311 % | | 252 | 3461049 10229336 | 1395956 252 3082 12.2 | 48.311 % | | 477 | 3461049 10229336 | 1535552 477 8393 17.6 | 48.311 % | | 814 | 3461049 10229336 | 1689107 814 13946 17.1 | 48.311 % | | 1321 | 3461049 10229336 | 1858018 1321 29106 22.0 | 48.311 % | ==============================================================================) restarts : 6 conflicts : 1784 (91 /sec) decisions : 3989 (203 /sec) propagations : 13267321 (675940 /sec) inspects : 195158948 (9942909 /sec) conflict literals : 41914 (12.22 % deleted) CPU time : 19.628 s SATISFIABLE VERIFY_CNF 1283 END : (22 seconds) [Thu Jun 1 17:27:50 2006] VERIFY_CNF 1283 CPU : 22.19 = 0.0100000000000477 + 0.02 + 21.62 + 0.54 # RESULT : makespan 1283 SATISFIABLE SHOW_RESULT 1283 BEGIN : [Thu Jun 1 17:27:50 2006] # ASSIGN : makespan 1283 # ASSIGN : s_0_0 8 # ASSIGN : s_0_1 192 # ASSIGN : s_0_2 218 # ASSIGN : s_0_3 291 # ASSIGN : s_0_4 664 # ASSIGN : s_0_5 698 # ASSIGN : s_0_6 777 # ASSIGN : s_0_7 944 # ASSIGN : s_0_8 1172 # ASSIGN : s_0_9 1228 # ASSIGN : s_1_0 260 # ASSIGN : s_1_1 389 # ASSIGN : s_1_2 487 # ASSIGN : s_1_3 611 # ASSIGN : s_1_4 708 # ASSIGN : s_1_5 941 # ASSIGN : s_1_6 1018 # ASSIGN : s_1_7 1095 # ASSIGN : s_1_8 1210 # ASSIGN : s_1_9 1241 # ASSIGN : s_2_0 14 # ASSIGN : s_2_1 96 # ASSIGN : s_2_2 188 # ASSIGN : s_2_3 289 # ASSIGN : s_2_4 350 # ASSIGN : s_2_5 369 # ASSIGN : s_2_6 412 # ASSIGN : s_2_7 526 # ASSIGN : s_2_8 789 # ASSIGN : s_2_9 1144 # ASSIGN : s_3_0 263 # ASSIGN : s_3_1 536 # ASSIGN : s_3_2 614 # ASSIGN : s_3_3 707 # ASSIGN : s_3_4 776 # ASSIGN : s_3_5 863 # ASSIGN : s_3_6 917 # ASSIGN : s_3_7 977 # ASSIGN : s_3_8 1072 # ASSIGN : s_3_9 1203 # ASSIGN : s_4_0 1 # ASSIGN : s_4_1 119 # ASSIGN : s_4_2 413 # ASSIGN : s_4_3 690 # ASSIGN : s_4_4 772 # ASSIGN : s_4_5 821 # ASSIGN : s_4_6 838 # ASSIGN : s_4_7 919 # ASSIGN : s_4_8 963 # ASSIGN : s_4_9 1010 # ASSIGN : s_5_0 719 # ASSIGN : s_5_1 743 # ASSIGN : s_5_2 804 # ASSIGN : s_5_3 977 # ASSIGN : s_5_4 1012 # ASSIGN : s_5_5 1022 # ASSIGN : s_5_6 1057 # ASSIGN : s_5_7 1085 # ASSIGN : s_5_8 1161 # ASSIGN : s_5_9 1274 # ASSIGN : s_6_0 60 # ASSIGN : s_6_1 223 # ASSIGN : s_6_2 331 # ASSIGN : s_6_3 460 # ASSIGN : s_6_4 488 # ASSIGN : s_6_5 850 # ASSIGN : s_6_6 866 # ASSIGN : s_6_7 1013 # ASSIGN : s_6_8 1206 # ASSIGN : s_6_9 1256 # ASSIGN : s_7_0 51 # ASSIGN : s_7_1 349 # ASSIGN : s_7_2 633 # ASSIGN : s_7_3 682 # ASSIGN : s_7_4 903 # ASSIGN : s_7_5 923 # ASSIGN : s_7_6 1044 # ASSIGN : s_7_7 1085 # ASSIGN : s_7_8 1196 # ASSIGN : s_7_9 1244 # ASSIGN : s_8_0 32 # ASSIGN : s_8_1 60 # ASSIGN : s_8_2 174 # ASSIGN : s_8_3 252 # ASSIGN : s_8_4 307 # ASSIGN : s_8_5 355 # ASSIGN : s_8_6 503 # ASSIGN : s_8_7 540 # ASSIGN : s_8_8 710 # ASSIGN : s_8_9 798 # ASSIGN : s_9_0 0 # ASSIGN : s_9_1 96 # ASSIGN : s_9_2 123 # ASSIGN : s_9_3 201 # ASSIGN : s_9_4 289 # ASSIGN : s_9_5 384 # ASSIGN : s_9_6 456 # ASSIGN : s_9_7 530 # ASSIGN : s_9_8 753 # ASSIGN : s_9_9 974 # ASSIGN : s_10_0 192 # ASSIGN : s_10_1 234 # ASSIGN : s_10_2 266 # ASSIGN : s_10_3 383 # ASSIGN : s_10_4 400 # ASSIGN : s_10_5 532 # ASSIGN : s_10_6 613 # ASSIGN : s_10_7 689 # ASSIGN : s_10_8 868 # ASSIGN : s_10_9 899 # ASSIGN : s_11_0 241 # ASSIGN : s_11_1 351 # ASSIGN : s_11_2 379 # ASSIGN : s_11_3 451 # ASSIGN : s_11_4 537 # ASSIGN : s_11_5 560 # ASSIGN : s_11_6 707 # ASSIGN : s_11_7 868 # ASSIGN : s_11_8 965 # ASSIGN : s_11_9 1225 # ASSIGN : s_12_0 520 # ASSIGN : s_12_1 561 # ASSIGN : s_12_2 659 # ASSIGN : s_12_3 726 # ASSIGN : s_12_4 792 # ASSIGN : s_12_5 819 # ASSIGN : s_12_6 901 # ASSIGN : s_12_7 1043 # ASSIGN : s_12_8 1155 # ASSIGN : s_12_9 1236 # ASSIGN : s_13_0 19 # ASSIGN : s_13_1 331 # ASSIGN : s_13_2 381 # ASSIGN : s_13_3 584 # ASSIGN : s_13_4 698 # ASSIGN : s_13_5 726 # ASSIGN : s_13_6 809 # ASSIGN : s_13_7 1121 # ASSIGN : s_13_8 1184 # ASSIGN : s_13_9 1203 # ASSIGN : s_14_0 27 # ASSIGN : s_14_1 99 # ASSIGN : s_14_2 500 # ASSIGN : s_14_3 713 # ASSIGN : s_14_4 886 # ASSIGN : s_14_5 925 # ASSIGN : s_14_6 975 # ASSIGN : s_14_7 989 # ASSIGN : s_14_8 1077 # ASSIGN : s_14_9 1104 # ASSIGN : s_15_0 0 # ASSIGN : s_15_1 99 # ASSIGN : s_15_2 144 # ASSIGN : s_15_3 257 # ASSIGN : s_15_4 304 # ASSIGN : s_15_5 378 # ASSIGN : s_15_6 453 # ASSIGN : s_15_7 558 # ASSIGN : s_15_8 629 # ASSIGN : s_15_9 767 # ASSIGN : s_16_0 1 # ASSIGN : s_16_1 79 # ASSIGN : s_16_2 126 # ASSIGN : s_16_3 184 # ASSIGN : s_16_4 216 # ASSIGN : s_16_5 285 # ASSIGN : s_16_6 343 # ASSIGN : s_16_7 377 # ASSIGN : s_16_8 410 # ASSIGN : s_16_9 479 # ASSIGN : s_17_0 87 # ASSIGN : s_17_1 131 # ASSIGN : s_17_2 171 # ASSIGN : s_17_3 495 # ASSIGN : s_17_4 647 # ASSIGN : s_17_5 804 # ASSIGN : s_17_6 899 # ASSIGN : s_17_7 1034 # ASSIGN : s_17_8 1098 # ASSIGN : s_17_9 1106 # ASSIGN : s_18_0 113 # ASSIGN : s_18_1 265 # ASSIGN : s_18_2 315 # ASSIGN : s_18_3 392 # ASSIGN : s_18_4 557 # ASSIGN : s_18_5 783 # ASSIGN : s_18_6 806 # ASSIGN : s_18_7 1112 # ASSIGN : s_18_8 1145 # ASSIGN : s_18_9 1263 # ASSIGN : s_19_0 178 # ASSIGN : s_19_1 720 # ASSIGN : s_19_2 872 # ASSIGN : s_19_3 928 # ASSIGN : s_19_4 991 # ASSIGN : s_19_5 1006 # ASSIGN : s_19_6 1076 # ASSIGN : s_19_7 1106 # ASSIGN : s_19_8 1196 # ASSIGN : s_19_9 1263 SHOW_RESULT 1283 END : 1283 (1 seconds) [Thu Jun 1 17:27:51 2006] SHOW_RESULT 1283 CPU : 0.829999999999984 = 0.829999999999984 + 0 + 0 + 0 # BOUND : makespan 1218 1283 MODIFY_CNF 1250 BEGIN : [Thu Jun 1 17:27:51 2006] MODIFY_CNF 1250 END : 142852038 bytes (0 seconds) [Thu Jun 1 17:27:51 2006] MODIFY_CNF 1250 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1250 BEGIN : [Thu Jun 1 17:27:51 2006] CMD : minisat /work/tamura/csp2sat78524.cnf /work/tamura/csp2sat78524.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 3329194 9840404 | 1109731 0 0 NaNQ | 0.000 % | | 101 | 3329194 9840404 | 1220704 101 1337 13.2 | 50.519 % | | 252 | 3329194 9840404 | 1342774 252 4015 15.9 | 50.519 % | | 478 | 3329194 9840404 | 1477051 478 7885 16.5 | 50.519 % | | 816 | 3329194 9840404 | 1624757 816 13268 16.3 | 50.519 % | | 1322 | 3329194 9840404 | 1787232 1322 28485 21.5 | 50.519 % | | 2081 | 3329194 9840404 | 1965956 2081 43301 20.8 | 50.519 % | | 3220 | 3329194 9840404 | 2162551 3220 79487 24.7 | 50.519 % | | 4930 | 3329194 9840404 | 2378806 4930 116732 23.7 | 50.519 % | | 7492 | 3329194 9840404 | 2616687 7492 200857 26.8 | 50.519 % | | 11336 | 3329194 9840404 | 2878356 11336 382588 33.7 | 50.519 % | ==============================================================================) restarts : 11 conflicts : 15030 (103 /sec) decisions : 25058 (171 /sec) propagations : 143612989 (981394 /sec) inspects : 2042960292 (13960779 /sec) conflict literals : 541168 (21.04 % deleted) CPU time : 146.336 s SATISFIABLE VERIFY_CNF 1250 END : (149 seconds) [Thu Jun 1 17:30:20 2006] VERIFY_CNF 1250 CPU : 148.6 = 0 + 0.0299999999999999 + 148.42 + 0.15 # RESULT : makespan 1250 SATISFIABLE SHOW_RESULT 1250 BEGIN : [Thu Jun 1 17:30:20 2006] # ASSIGN : makespan 1250 # ASSIGN : s_0_0 0 # ASSIGN : s_0_1 69 # ASSIGN : s_0_2 132 # ASSIGN : s_0_3 638 # ASSIGN : s_0_4 843 # ASSIGN : s_0_5 877 # ASSIGN : s_0_6 898 # ASSIGN : s_0_7 1019 # ASSIGN : s_0_8 1050 # ASSIGN : s_0_9 1195 # ASSIGN : s_1_0 638 # ASSIGN : s_1_1 693 # ASSIGN : s_1_2 791 # ASSIGN : s_1_3 830 # ASSIGN : s_1_4 909 # ASSIGN : s_1_5 926 # ASSIGN : s_1_6 1003 # ASSIGN : s_1_7 1080 # ASSIGN : s_1_8 1177 # ASSIGN : s_1_9 1208 # ASSIGN : s_2_0 17 # ASSIGN : s_2_1 60 # ASSIGN : s_2_2 275 # ASSIGN : s_2_3 506 # ASSIGN : s_2_4 565 # ASSIGN : s_2_5 584 # ASSIGN : s_2_6 627 # ASSIGN : s_2_7 717 # ASSIGN : s_2_8 751 # ASSIGN : s_2_9 1188 # ASSIGN : s_3_0 308 # ASSIGN : s_3_1 411 # ASSIGN : s_3_2 490 # ASSIGN : s_3_3 595 # ASSIGN : s_3_4 666 # ASSIGN : s_3_5 753 # ASSIGN : s_3_6 791 # ASSIGN : s_3_7 962 # ASSIGN : s_3_8 1039 # ASSIGN : s_3_9 1170 # ASSIGN : s_4_0 80 # ASSIGN : s_4_1 178 # ASSIGN : s_4_2 203 # ASSIGN : s_4_3 318 # ASSIGN : s_4_4 395 # ASSIGN : s_4_5 444 # ASSIGN : s_4_6 481 # ASSIGN : s_4_7 583 # ASSIGN : s_4_8 816 # ASSIGN : s_4_9 923 # ASSIGN : s_5_0 57 # ASSIGN : s_5_1 703 # ASSIGN : s_5_2 796 # ASSIGN : s_5_3 891 # ASSIGN : s_5_4 926 # ASSIGN : s_5_5 1006 # ASSIGN : s_5_6 1041 # ASSIGN : s_5_7 1070 # ASSIGN : s_5_8 1146 # ASSIGN : s_5_9 1241 # ASSIGN : s_6_0 54 # ASSIGN : s_6_1 113 # ASSIGN : s_6_2 156 # ASSIGN : s_6_3 215 # ASSIGN : s_6_4 278 # ASSIGN : s_6_5 346 # ASSIGN : s_6_6 362 # ASSIGN : s_6_7 474 # ASSIGN : s_6_8 639 # ASSIGN : s_6_9 726 # ASSIGN : s_7_0 141 # ASSIGN : s_7_1 188 # ASSIGN : s_7_2 250 # ASSIGN : s_7_3 655 # ASSIGN : s_7_4 809 # ASSIGN : s_7_5 852 # ASSIGN : s_7_6 922 # ASSIGN : s_7_7 963 # ASSIGN : s_7_8 1072 # ASSIGN : s_7_9 1211 # ASSIGN : s_8_0 280 # ASSIGN : s_8_1 334 # ASSIGN : s_8_2 412 # ASSIGN : s_8_3 490 # ASSIGN : s_8_4 527 # ASSIGN : s_8_5 569 # ASSIGN : s_8_6 603 # ASSIGN : s_8_7 636 # ASSIGN : s_8_8 1040 # ASSIGN : s_8_9 1242 # ASSIGN : s_9_0 287 # ASSIGN : s_9_1 383 # ASSIGN : s_9_2 410 # ASSIGN : s_9_3 488 # ASSIGN : s_9_4 572 # ASSIGN : s_9_5 689 # ASSIGN : s_9_6 803 # ASSIGN : s_9_7 936 # ASSIGN : s_9_8 1017 # ASSIGN : s_9_9 1103 # ASSIGN : s_10_0 13 # ASSIGN : s_10_1 37 # ASSIGN : s_10_2 88 # ASSIGN : s_10_3 241 # ASSIGN : s_10_4 259 # ASSIGN : s_10_5 400 # ASSIGN : s_10_6 1069 # ASSIGN : s_10_7 1145 # ASSIGN : s_10_8 1177 # ASSIGN : s_10_9 1230 # ASSIGN : s_11_0 52 # ASSIGN : s_11_1 150 # ASSIGN : s_11_2 181 # ASSIGN : s_11_3 253 # ASSIGN : s_11_4 339 # ASSIGN : s_11_5 461 # ASSIGN : s_11_6 560 # ASSIGN : s_11_7 654 # ASSIGN : s_11_8 764 # ASSIGN : s_11_9 1172 # ASSIGN : s_12_0 258 # ASSIGN : s_12_1 540 # ASSIGN : s_12_2 664 # ASSIGN : s_12_3 712 # ASSIGN : s_12_4 758 # ASSIGN : s_12_5 785 # ASSIGN : s_12_6 859 # ASSIGN : s_12_7 921 # ASSIGN : s_12_8 1122 # ASSIGN : s_12_9 1223 # ASSIGN : s_13_0 1 # ASSIGN : s_13_1 200 # ASSIGN : s_13_2 364 # ASSIGN : s_13_3 486 # ASSIGN : s_13_4 665 # ASSIGN : s_13_5 779 # ASSIGN : s_13_6 829 # ASSIGN : s_13_7 1082 # ASSIGN : s_13_8 1158 # ASSIGN : s_13_9 1170 # ASSIGN : s_14_0 9 # ASSIGN : s_14_1 81 # ASSIGN : s_14_2 479 # ASSIGN : s_14_3 815 # ASSIGN : s_14_4 906 # ASSIGN : s_14_5 943 # ASSIGN : s_14_6 993 # ASSIGN : s_14_7 1007 # ASSIGN : s_14_8 1062 # ASSIGN : s_14_9 1117 # ASSIGN : s_15_0 6 # ASSIGN : s_15_1 204 # ASSIGN : s_15_2 218 # ASSIGN : s_15_3 275 # ASSIGN : s_15_4 339 # ASSIGN : s_15_5 404 # ASSIGN : s_15_6 560 # ASSIGN : s_15_7 641 # ASSIGN : s_15_8 725 # ASSIGN : s_15_9 1017 # ASSIGN : s_16_0 64 # ASSIGN : s_16_1 95 # ASSIGN : s_16_2 142 # ASSIGN : s_16_3 211 # ASSIGN : s_16_4 243 # ASSIGN : s_16_5 287 # ASSIGN : s_16_6 345 # ASSIGN : s_16_7 379 # ASSIGN : s_16_8 421 # ASSIGN : s_16_9 587 # ASSIGN : s_17_0 13 # ASSIGN : s_17_1 145 # ASSIGN : s_17_2 185 # ASSIGN : s_17_3 202 # ASSIGN : s_17_4 264 # ASSIGN : s_17_5 330 # ASSIGN : s_17_6 415 # ASSIGN : s_17_7 489 # ASSIGN : s_17_8 1033 # ASSIGN : s_17_9 1073 # ASSIGN : s_18_0 22 # ASSIGN : s_18_1 102 # ASSIGN : s_18_2 152 # ASSIGN : s_18_3 231 # ASSIGN : s_18_4 322 # ASSIGN : s_18_5 389 # ASSIGN : s_18_6 429 # ASSIGN : s_18_7 894 # ASSIGN : s_18_8 1033 # ASSIGN : s_18_9 1203 # ASSIGN : s_19_0 96 # ASSIGN : s_19_1 710 # ASSIGN : s_19_2 794 # ASSIGN : s_19_3 850 # ASSIGN : s_19_4 911 # ASSIGN : s_19_5 947 # ASSIGN : s_19_6 1043 # ASSIGN : s_19_7 1073 # ASSIGN : s_19_8 1163 # ASSIGN : s_19_9 1230 SHOW_RESULT 1250 END : 1250 (1 seconds) [Thu Jun 1 17:30:21 2006] SHOW_RESULT 1250 CPU : 0.810000000000002 = 0.810000000000002 + 0 + 0 + 0 # BOUND : makespan 1218 1250 MODIFY_CNF 1234 BEGIN : [Thu Jun 1 17:30:21 2006] MODIFY_CNF 1234 END : 142852038 bytes (0 seconds) [Thu Jun 1 17:30:21 2006] MODIFY_CNF 1234 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1234 BEGIN : [Thu Jun 1 17:30:21 2006] CMD : minisat /work/tamura/csp2sat78524.cnf /work/tamura/csp2sat78524.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 3260494 9637528 | 1086831 0 0 NaNQ | 0.000 % | | 100 | 3260494 9637528 | 1195514 100 1243 12.4 | 51.592 % | | 250 | 3260494 9637528 | 1315065 250 4962 19.8 | 51.592 % | | 475 | 3260494 9637528 | 1446572 475 12048 25.4 | 51.592 % | | 813 | 3260494 9637528 | 1591229 813 20673 25.4 | 51.592 % | | 1319 | 3260494 9637528 | 1750352 1319 33033 25.0 | 51.592 % | | 2079 | 3260494 9637528 | 1925387 2079 47603 22.9 | 51.592 % | | 3219 | 3260494 9637528 | 2117926 3219 80649 25.1 | 51.592 % | | 4929 | 3260494 9637528 | 2329718 4929 145512 29.5 | 51.592 % | | 7492 | 3260494 9637528 | 2562690 7492 218196 29.1 | 51.592 % | | 11336 | 3260494 9637528 | 2818959 11336 293898 25.9 | 51.592 % | | 17102 | 3260494 9637528 | 3100855 17102 468774 27.4 | 51.592 % | ==============================================================================) restarts : 12 conflicts : 20076 (103 /sec) decisions : 31469 (161 /sec) propagations : 194219138 (994924 /sec) inspects : 2699818988 (13830335 /sec) conflict literals : 650277 (25.12 % deleted) CPU time : 195.21 s SATISFIABLE VERIFY_CNF 1234 END : (198 seconds) [Thu Jun 1 17:33:39 2006] VERIFY_CNF 1234 CPU : 197.39 = 0.00999999999999091 + 0.02 + 197.21 + 0.15 # RESULT : makespan 1234 SATISFIABLE SHOW_RESULT 1234 BEGIN : [Thu Jun 1 17:33:39 2006] # ASSIGN : makespan 1234 # ASSIGN : s_0_0 101 # ASSIGN : s_0_1 169 # ASSIGN : s_0_2 280 # ASSIGN : s_0_3 396 # ASSIGN : s_0_4 715 # ASSIGN : s_0_5 808 # ASSIGN : s_0_6 829 # ASSIGN : s_0_7 1037 # ASSIGN : s_0_8 1092 # ASSIGN : s_0_9 1179 # ASSIGN : s_1_0 381 # ASSIGN : s_1_1 436 # ASSIGN : s_1_2 547 # ASSIGN : s_1_3 586 # ASSIGN : s_1_4 666 # ASSIGN : s_1_5 678 # ASSIGN : s_1_6 907 # ASSIGN : s_1_7 1064 # ASSIGN : s_1_8 1161 # ASSIGN : s_1_9 1192 # ASSIGN : s_2_0 238 # ASSIGN : s_2_1 449 # ASSIGN : s_2_2 541 # ASSIGN : s_2_3 605 # ASSIGN : s_2_4 659 # ASSIGN : s_2_5 678 # ASSIGN : s_2_6 721 # ASSIGN : s_2_7 804 # ASSIGN : s_2_8 838 # ASSIGN : s_2_9 1172 # ASSIGN : s_3_0 272 # ASSIGN : s_3_1 359 # ASSIGN : s_3_2 526 # ASSIGN : s_3_3 654 # ASSIGN : s_3_4 749 # ASSIGN : s_3_5 836 # ASSIGN : s_3_6 953 # ASSIGN : s_3_7 984 # ASSIGN : s_3_8 1078 # ASSIGN : s_3_9 1174 # ASSIGN : s_4_0 59 # ASSIGN : s_4_1 157 # ASSIGN : s_4_2 205 # ASSIGN : s_4_3 319 # ASSIGN : s_4_4 430 # ASSIGN : s_4_5 479 # ASSIGN : s_4_6 498 # ASSIGN : s_4_7 870 # ASSIGN : s_4_8 958 # ASSIGN : s_4_9 1058 # ASSIGN : s_5_0 116 # ASSIGN : s_5_1 201 # ASSIGN : s_5_2 369 # ASSIGN : s_5_3 506 # ASSIGN : s_5_4 576 # ASSIGN : s_5_5 643 # ASSIGN : s_5_6 1026 # ASSIGN : s_5_7 1054 # ASSIGN : s_5_8 1130 # ASSIGN : s_5_9 1225 # ASSIGN : s_6_0 36 # ASSIGN : s_6_1 202 # ASSIGN : s_6_2 245 # ASSIGN : s_6_3 323 # ASSIGN : s_6_4 351 # ASSIGN : s_6_5 612 # ASSIGN : s_6_6 656 # ASSIGN : s_6_7 717 # ASSIGN : s_6_8 824 # ASSIGN : s_6_9 874 # ASSIGN : s_7_0 27 # ASSIGN : s_7_1 55 # ASSIGN : s_7_2 153 # ASSIGN : s_7_3 545 # ASSIGN : s_7_4 654 # ASSIGN : s_7_5 674 # ASSIGN : s_7_6 763 # ASSIGN : s_7_7 972 # ASSIGN : s_7_8 1077 # ASSIGN : s_7_9 1195 # ASSIGN : s_8_0 197 # ASSIGN : s_8_1 225 # ASSIGN : s_8_2 291 # ASSIGN : s_8_3 375 # ASSIGN : s_8_4 412 # ASSIGN : s_8_5 628 # ASSIGN : s_8_6 695 # ASSIGN : s_8_7 728 # ASSIGN : s_8_8 863 # ASSIGN : s_8_9 1226 # ASSIGN : s_9_0 1 # ASSIGN : s_9_1 100 # ASSIGN : s_9_2 127 # ASSIGN : s_9_3 275 # ASSIGN : s_9_4 412 # ASSIGN : s_9_5 755 # ASSIGN : s_9_6 843 # ASSIGN : s_9_7 917 # ASSIGN : s_9_8 1019 # ASSIGN : s_9_9 1145 # ASSIGN : s_10_0 357 # ASSIGN : s_10_1 404 # ASSIGN : s_10_2 454 # ASSIGN : s_10_3 842 # ASSIGN : s_10_4 859 # ASSIGN : s_10_5 977 # ASSIGN : s_10_6 1058 # ASSIGN : s_10_7 1134 # ASSIGN : s_10_8 1161 # ASSIGN : s_10_9 1214 # ASSIGN : s_11_0 5 # ASSIGN : s_11_1 95 # ASSIGN : s_11_2 123 # ASSIGN : s_11_3 195 # ASSIGN : s_11_4 281 # ASSIGN : s_11_5 304 # ASSIGN : s_11_6 403 # ASSIGN : s_11_7 479 # ASSIGN : s_11_8 609 # ASSIGN : s_11_9 914 # ASSIGN : s_12_0 42 # ASSIGN : s_12_1 97 # ASSIGN : s_12_2 195 # ASSIGN : s_12_3 384 # ASSIGN : s_12_4 471 # ASSIGN : s_12_5 538 # ASSIGN : s_12_6 616 # ASSIGN : s_12_7 679 # ASSIGN : s_12_8 790 # ASSIGN : s_12_9 1187 # ASSIGN : s_13_0 6 # ASSIGN : s_13_1 312 # ASSIGN : s_13_2 417 # ASSIGN : s_13_3 436 # ASSIGN : s_13_4 534 # ASSIGN : s_13_5 606 # ASSIGN : s_13_6 694 # ASSIGN : s_13_7 817 # ASSIGN : s_13_8 953 # ASSIGN : s_13_9 998 # ASSIGN : s_14_0 98 # ASSIGN : s_14_1 170 # ASSIGN : s_14_2 262 # ASSIGN : s_14_3 362 # ASSIGN : s_14_4 501 # ASSIGN : s_14_5 882 # ASSIGN : s_14_6 932 # ASSIGN : s_14_7 946 # ASSIGN : s_14_8 1001 # ASSIGN : s_14_9 1036 # ASSIGN : s_15_0 4 # ASSIGN : s_15_1 209 # ASSIGN : s_15_2 562 # ASSIGN : s_15_3 619 # ASSIGN : s_15_4 723 # ASSIGN : s_15_5 788 # ASSIGN : s_15_6 874 # ASSIGN : s_15_7 965 # ASSIGN : s_15_8 1152 # ASSIGN : s_15_9 1212 # ASSIGN : s_16_0 85 # ASSIGN : s_16_1 120 # ASSIGN : s_16_2 167 # ASSIGN : s_16_3 447 # ASSIGN : s_16_4 896 # ASSIGN : s_16_5 967 # ASSIGN : s_16_6 1025 # ASSIGN : s_16_7 1059 # ASSIGN : s_16_8 1092 # ASSIGN : s_16_9 1161 # ASSIGN : s_17_0 228 # ASSIGN : s_17_1 294 # ASSIGN : s_17_2 358 # ASSIGN : s_17_3 464 # ASSIGN : s_17_4 577 # ASSIGN : s_17_5 659 # ASSIGN : s_17_6 723 # ASSIGN : s_17_7 752 # ASSIGN : s_17_8 924 # ASSIGN : s_17_9 940 # ASSIGN : s_18_0 223 # ASSIGN : s_18_1 496 # ASSIGN : s_18_2 546 # ASSIGN : s_18_3 665 # ASSIGN : s_18_4 813 # ASSIGN : s_18_5 880 # ASSIGN : s_18_6 901 # ASSIGN : s_18_7 1090 # ASSIGN : s_18_8 1122 # ASSIGN : s_18_9 1214 # ASSIGN : s_19_0 0 # ASSIGN : s_19_1 86 # ASSIGN : s_19_2 182 # ASSIGN : s_19_3 243 # ASSIGN : s_19_4 304 # ASSIGN : s_19_5 334 # ASSIGN : s_19_6 441 # ASSIGN : s_19_7 977 # ASSIGN : s_19_8 1067 # ASSIGN : s_19_9 1154 SHOW_RESULT 1234 END : 1234 (1 seconds) [Thu Jun 1 17:33:40 2006] SHOW_RESULT 1234 CPU : 0.829999999999993 = 0.819999999999993 + 0.01 + 0 + 0 # BOUND : makespan 1218 1234 MODIFY_CNF 1226 BEGIN : [Thu Jun 1 17:33:40 2006] MODIFY_CNF 1226 END : 142852038 bytes (0 seconds) [Thu Jun 1 17:33:40 2006] MODIFY_CNF 1226 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1226 BEGIN : [Thu Jun 1 17:33:40 2006] CMD : minisat /work/tamura/csp2sat78524.cnf /work/tamura/csp2sat78524.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 3228558 9543328 | 1076186 0 0 NaNQ | 0.000 % | | 100 | 3228558 9543328 | 1183804 100 2279 22.8 | 52.127 % | | 250 | 3228558 9543328 | 1302185 250 4423 17.7 | 52.127 % | | 475 | 3228558 9543328 | 1432403 475 11039 23.2 | 52.127 % | | 812 | 3228558 9543328 | 1575643 812 17542 21.6 | 52.127 % | | 1318 | 3228558 9543328 | 1733208 1318 34457 26.1 | 52.127 % | | 2077 | 3228558 9543328 | 1906529 2077 57766 27.8 | 52.127 % | | 3216 | 3228558 9543328 | 2097182 3216 91369 28.4 | 52.127 % | | 4925 | 3228558 9543328 | 2306900 4925 139261 28.3 | 52.127 % | | 7487 | 3228558 9543328 | 2537590 7487 219345 29.3 | 52.127 % | | 11332 | 3228558 9543328 | 2791349 11332 332144 29.3 | 52.127 % | | 17099 | 3228558 9543328 | 3070484 17099 582453 34.1 | 52.127 % | | 25749 | 3228558 9543328 | 3377532 25749 921346 35.8 | 52.127 % | ==============================================================================) restarts : 13 conflicts : 33799 (109 /sec) decisions : 53956 (174 /sec) propagations : 310104543 (997761 /sec) inspects : 4476488064 (14403100 /sec) conflict literals : 1142173 (25.97 % deleted) CPU time : 310.8 s SATISFIABLE VERIFY_CNF 1226 END : (314 seconds) [Thu Jun 1 17:38:54 2006] VERIFY_CNF 1226 CPU : 313.25 = 0 + 0.02 + 312.68 + 0.55 # RESULT : makespan 1226 SATISFIABLE SHOW_RESULT 1226 BEGIN : [Thu Jun 1 17:38:54 2006] # ASSIGN : makespan 1226 # ASSIGN : s_0_0 297 # ASSIGN : s_0_1 349 # ASSIGN : s_0_2 375 # ASSIGN : s_0_3 452 # ASSIGN : s_0_4 519 # ASSIGN : s_0_5 738 # ASSIGN : s_0_6 759 # ASSIGN : s_0_7 854 # ASSIGN : s_0_8 993 # ASSIGN : s_0_9 1171 # ASSIGN : s_1_0 96 # ASSIGN : s_1_1 180 # ASSIGN : s_1_2 282 # ASSIGN : s_1_3 373 # ASSIGN : s_1_4 655 # ASSIGN : s_1_5 724 # ASSIGN : s_1_6 941 # ASSIGN : s_1_7 1038 # ASSIGN : s_1_8 1153 # ASSIGN : s_1_9 1184 # ASSIGN : s_2_0 2 # ASSIGN : s_2_1 151 # ASSIGN : s_2_2 252 # ASSIGN : s_2_3 316 # ASSIGN : s_2_4 370 # ASSIGN : s_2_5 389 # ASSIGN : s_2_6 432 # ASSIGN : s_2_7 516 # ASSIGN : s_2_8 550 # ASSIGN : s_2_9 1164 # ASSIGN : s_3_0 283 # ASSIGN : s_3_1 436 # ASSIGN : s_3_2 515 # ASSIGN : s_3_3 611 # ASSIGN : s_3_4 814 # ASSIGN : s_3_5 901 # ASSIGN : s_3_6 945 # ASSIGN : s_3_7 1018 # ASSIGN : s_3_8 1070 # ASSIGN : s_3_9 1166 # ASSIGN : s_4_0 41 # ASSIGN : s_4_1 155 # ASSIGN : s_4_2 221 # ASSIGN : s_4_3 296 # ASSIGN : s_4_4 506 # ASSIGN : s_4_5 594 # ASSIGN : s_4_6 645 # ASSIGN : s_4_7 805 # ASSIGN : s_4_8 858 # ASSIGN : s_4_9 908 # ASSIGN : s_5_0 16 # ASSIGN : s_5_1 341 # ASSIGN : s_5_2 667 # ASSIGN : s_5_3 762 # ASSIGN : s_5_4 797 # ASSIGN : s_5_5 831 # ASSIGN : s_5_6 1000 # ASSIGN : s_5_7 1028 # ASSIGN : s_5_8 1104 # ASSIGN : s_5_9 1217 # ASSIGN : s_6_0 39 # ASSIGN : s_6_1 253 # ASSIGN : s_6_2 386 # ASSIGN : s_6_3 451 # ASSIGN : s_6_4 500 # ASSIGN : s_6_5 552 # ASSIGN : s_6_6 576 # ASSIGN : s_6_7 854 # ASSIGN : s_6_8 1114 # ASSIGN : s_6_9 1199 # ASSIGN : s_7_0 146 # ASSIGN : s_7_1 174 # ASSIGN : s_7_2 217 # ASSIGN : s_7_3 278 # ASSIGN : s_7_4 426 # ASSIGN : s_7_5 446 # ASSIGN : s_7_6 841 # ASSIGN : s_7_7 906 # ASSIGN : s_7_8 998 # ASSIGN : s_7_9 1187 # ASSIGN : s_8_0 67 # ASSIGN : s_8_1 151 # ASSIGN : s_8_2 218 # ASSIGN : s_8_3 456 # ASSIGN : s_8_4 493 # ASSIGN : s_8_5 568 # ASSIGN : s_8_6 657 # ASSIGN : s_8_7 690 # ASSIGN : s_8_8 875 # ASSIGN : s_8_9 973 # ASSIGN : s_9_0 0 # ASSIGN : s_9_1 116 # ASSIGN : s_9_2 143 # ASSIGN : s_9_3 278 # ASSIGN : s_9_4 362 # ASSIGN : s_9_5 471 # ASSIGN : s_9_6 555 # ASSIGN : s_9_7 629 # ASSIGN : s_9_8 813 # ASSIGN : s_9_9 1137 # ASSIGN : s_10_0 402 # ASSIGN : s_10_1 435 # ASSIGN : s_10_2 468 # ASSIGN : s_10_3 797 # ASSIGN : s_10_4 882 # ASSIGN : s_10_5 969 # ASSIGN : s_10_6 1050 # ASSIGN : s_10_7 1126 # ASSIGN : s_10_8 1153 # ASSIGN : s_10_9 1206 # ASSIGN : s_11_0 8 # ASSIGN : s_11_1 98 # ASSIGN : s_11_2 126 # ASSIGN : s_11_3 467 # ASSIGN : s_11_4 553 # ASSIGN : s_11_5 680 # ASSIGN : s_11_6 779 # ASSIGN : s_11_7 855 # ASSIGN : s_11_8 1004 # ASSIGN : s_11_9 1079 # ASSIGN : s_12_0 157 # ASSIGN : s_12_1 243 # ASSIGN : s_12_2 350 # ASSIGN : s_12_3 398 # ASSIGN : s_12_4 444 # ASSIGN : s_12_5 552 # ASSIGN : s_12_6 652 # ASSIGN : s_12_7 763 # ASSIGN : s_12_8 807 # ASSIGN : s_12_9 1199 # ASSIGN : s_13_0 1 # ASSIGN : s_13_1 101 # ASSIGN : s_13_2 161 # ASSIGN : s_13_3 180 # ASSIGN : s_13_4 570 # ASSIGN : s_13_5 635 # ASSIGN : s_13_6 685 # ASSIGN : s_13_7 857 # ASSIGN : s_13_8 945 # ASSIGN : s_13_9 990 # ASSIGN : s_14_0 9 # ASSIGN : s_14_1 81 # ASSIGN : s_14_2 479 # ASSIGN : s_14_3 540 # ASSIGN : s_14_4 619 # ASSIGN : s_14_5 695 # ASSIGN : s_14_6 745 # ASSIGN : s_14_7 786 # ASSIGN : s_14_8 939 # ASSIGN : s_14_9 957 # ASSIGN : s_15_0 20 # ASSIGN : s_15_1 499 # ASSIGN : s_15_2 513 # ASSIGN : s_15_3 608 # ASSIGN : s_15_4 714 # ASSIGN : s_15_5 779 # ASSIGN : s_15_6 866 # ASSIGN : s_15_7 1043 # ASSIGN : s_15_8 1144 # ASSIGN : s_15_9 1204 # ASSIGN : s_16_0 95 # ASSIGN : s_16_1 133 # ASSIGN : s_16_2 365 # ASSIGN : s_16_3 423 # ASSIGN : s_16_4 554 # ASSIGN : s_16_5 598 # ASSIGN : s_16_6 656 # ASSIGN : s_16_7 1046 # ASSIGN : s_16_8 1084 # ASSIGN : s_16_9 1153 # ASSIGN : s_17_0 23 # ASSIGN : s_17_1 93 # ASSIGN : s_17_2 139 # ASSIGN : s_17_3 156 # ASSIGN : s_17_4 231 # ASSIGN : s_17_5 301 # ASSIGN : s_17_6 321 # ASSIGN : s_17_7 952 # ASSIGN : s_17_8 1041 # ASSIGN : s_17_9 1049 # ASSIGN : s_18_0 174 # ASSIGN : s_18_1 232 # ASSIGN : s_18_2 622 # ASSIGN : s_18_3 710 # ASSIGN : s_18_4 849 # ASSIGN : s_18_5 920 # ASSIGN : s_18_6 981 # ASSIGN : s_18_7 1082 # ASSIGN : s_18_8 1114 # ASSIGN : s_18_9 1179 # ASSIGN : s_19_0 198 # ASSIGN : s_19_1 296 # ASSIGN : s_19_2 380 # ASSIGN : s_19_3 455 # ASSIGN : s_19_4 535 # ASSIGN : s_19_5 582 # ASSIGN : s_19_6 801 # ASSIGN : s_19_7 969 # ASSIGN : s_19_8 1059 # ASSIGN : s_19_9 1146 SHOW_RESULT 1226 END : 1226 (0 seconds) [Thu Jun 1 17:38:54 2006] SHOW_RESULT 1226 CPU : 0.819999999999993 = 0.819999999999993 + 0 + 0 + 0 # BOUND : makespan 1218 1226 MODIFY_CNF 1222 BEGIN : [Thu Jun 1 17:38:54 2006] MODIFY_CNF 1222 END : 142852037 bytes (0 seconds) [Thu Jun 1 17:38:54 2006] MODIFY_CNF 1222 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1222 BEGIN : [Thu Jun 1 17:38:54 2006] CMD : minisat /work/tamura/csp2sat78524.cnf /work/tamura/csp2sat78524.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 3212590 9496228 | 1070863 0 0 NaNQ | 0.000 % | | 100 | 3212590 9496228 | 1177949 100 1169 11.7 | 52.395 % | | 250 | 3212590 9496228 | 1295744 250 4833 19.3 | 52.395 % | | 476 | 3212590 9496228 | 1425318 476 8808 18.5 | 52.395 % | | 814 | 3212590 9496228 | 1567850 814 14674 18.0 | 52.395 % | | 1320 | 3212590 9496228 | 1724635 1320 25795 19.5 | 52.395 % | | 2079 | 3212590 9496228 | 1897099 2079 37637 18.1 | 52.395 % | | 3220 | 3212590 9496228 | 2086809 3220 63593 19.7 | 52.395 % | | 4928 | 3212590 9496228 | 2295489 4928 113338 23.0 | 52.395 % | | 7491 | 3212590 9496228 | 2525038 7491 178402 23.8 | 52.395 % | | 11336 | 3212590 9496228 | 2777542 11336 286198 25.2 | 52.395 % | | 17103 | 3212590 9496228 | 3055297 17103 527683 30.9 | 52.395 % | | 25752 | 3212590 9496228 | 3360826 25752 758287 29.4 | 52.395 % | | 38726 | 3212590 9496228 | 3696909 38726 2079978 53.7 | 52.395 % | | 58187 | 3212590 9496228 | 4066600 58187 2938993 50.5 | 52.395 % | | 87381 | 3212590 9496228 | 4473260 87381 4124611 47.2 | 52.395 % | | 131170 | 3212590 9496228 | 4920586 131170 5663024 43.2 | 52.395 % | ==============================================================================) restarts : 17 conflicts : 162166 (101 /sec) decisions : 241010 (150 /sec) propagations : 1452660279 (901873 /sec) inspects : 22184954141 (13773366 /sec) conflict literals : 8888271 (26.32 % deleted) CPU time : 1610.71 s SATISFIABLE VERIFY_CNF 1222 END : (1616 seconds) [Thu Jun 1 18:05:50 2006] VERIFY_CNF 1222 CPU : 1613.31 = 0 + 0.02 + 1612.74 + 0.55 # RESULT : makespan 1222 SATISFIABLE SHOW_RESULT 1222 BEGIN : [Thu Jun 1 18:05:50 2006] # ASSIGN : makespan 1222 # ASSIGN : s_0_0 207 # ASSIGN : s_0_1 259 # ASSIGN : s_0_2 369 # ASSIGN : s_0_3 476 # ASSIGN : s_0_4 503 # ASSIGN : s_0_5 537 # ASSIGN : s_0_6 564 # ASSIGN : s_0_7 659 # ASSIGN : s_0_8 720 # ASSIGN : s_0_9 1167 # ASSIGN : s_1_0 0 # ASSIGN : s_1_1 164 # ASSIGN : s_1_2 276 # ASSIGN : s_1_3 351 # ASSIGN : s_1_4 430 # ASSIGN : s_1_5 448 # ASSIGN : s_1_6 579 # ASSIGN : s_1_7 663 # ASSIGN : s_1_8 729 # ASSIGN : s_1_9 855 # ASSIGN : s_2_0 6 # ASSIGN : s_2_1 55 # ASSIGN : s_2_2 154 # ASSIGN : s_2_3 218 # ASSIGN : s_2_4 518 # ASSIGN : s_2_5 555 # ASSIGN : s_2_6 905 # ASSIGN : s_2_7 1034 # ASSIGN : s_2_8 1068 # ASSIGN : s_2_9 1160 # ASSIGN : s_3_0 260 # ASSIGN : s_3_1 347 # ASSIGN : s_3_2 442 # ASSIGN : s_3_3 691 # ASSIGN : s_3_4 760 # ASSIGN : s_3_5 861 # ASSIGN : s_3_6 899 # ASSIGN : s_3_7 927 # ASSIGN : s_3_8 985 # ASSIGN : s_3_9 1109 # ASSIGN : s_4_0 4 # ASSIGN : s_4_1 102 # ASSIGN : s_4_2 143 # ASSIGN : s_4_3 274 # ASSIGN : s_4_4 444 # ASSIGN : s_4_5 493 # ASSIGN : s_4_6 525 # ASSIGN : s_4_7 676 # ASSIGN : s_4_8 923 # ASSIGN : s_4_9 1013 # ASSIGN : s_5_0 498 # ASSIGN : s_5_1 520 # ASSIGN : s_5_2 581 # ASSIGN : s_5_3 694 # ASSIGN : s_5_4 751 # ASSIGN : s_5_5 783 # ASSIGN : s_5_6 930 # ASSIGN : s_5_7 958 # ASSIGN : s_5_8 1068 # ASSIGN : s_5_9 1213 # ASSIGN : s_6_0 43 # ASSIGN : s_6_1 188 # ASSIGN : s_6_2 535 # ASSIGN : s_6_3 820 # ASSIGN : s_6_4 848 # ASSIGN : s_6_5 900 # ASSIGN : s_6_6 916 # ASSIGN : s_6_7 975 # ASSIGN : s_6_8 1110 # ASSIGN : s_6_9 1187 # ASSIGN : s_7_0 155 # ASSIGN : s_7_1 231 # ASSIGN : s_7_2 375 # ASSIGN : s_7_3 389 # ASSIGN : s_7_4 595 # ASSIGN : s_7_5 794 # ASSIGN : s_7_6 917 # ASSIGN : s_7_7 988 # ASSIGN : s_7_8 1105 # ASSIGN : s_7_9 1183 # ASSIGN : s_8_0 0 # ASSIGN : s_8_1 141 # ASSIGN : s_8_2 221 # ASSIGN : s_8_3 546 # ASSIGN : s_8_4 694 # ASSIGN : s_8_5 787 # ASSIGN : s_8_6 897 # ASSIGN : s_8_7 1028 # ASSIGN : s_8_8 1169 # ASSIGN : s_8_9 1214 # ASSIGN : s_9_0 147 # ASSIGN : s_9_1 245 # ASSIGN : s_9_2 272 # ASSIGN : s_9_3 480 # ASSIGN : s_9_4 600 # ASSIGN : s_9_5 710 # ASSIGN : s_9_6 779 # ASSIGN : s_9_7 853 # ASSIGN : s_9_8 1023 # ASSIGN : s_9_9 1075 # ASSIGN : s_10_0 435 # ASSIGN : s_10_1 460 # ASSIGN : s_10_2 492 # ASSIGN : s_10_3 583 # ASSIGN : s_10_4 813 # ASSIGN : s_10_5 923 # ASSIGN : s_10_6 1018 # ASSIGN : s_10_7 1117 # ASSIGN : s_10_8 1150 # ASSIGN : s_10_9 1202 # ASSIGN : s_11_0 1 # ASSIGN : s_11_1 127 # ASSIGN : s_11_2 188 # ASSIGN : s_11_3 285 # ASSIGN : s_11_4 371 # ASSIGN : s_11_5 394 # ASSIGN : s_11_6 503 # ASSIGN : s_11_7 597 # ASSIGN : s_11_8 968 # ASSIGN : s_11_9 1144 # ASSIGN : s_12_0 120 # ASSIGN : s_12_1 243 # ASSIGN : s_12_2 510 # ASSIGN : s_12_3 558 # ASSIGN : s_12_4 604 # ASSIGN : s_12_5 656 # ASSIGN : s_12_6 729 # ASSIGN : s_12_7 806 # ASSIGN : s_12_8 1147 # ASSIGN : s_12_9 1195 # ASSIGN : s_13_0 4 # ASSIGN : s_13_1 91 # ASSIGN : s_13_2 142 # ASSIGN : s_13_3 161 # ASSIGN : s_13_4 262 # ASSIGN : s_13_5 291 # ASSIGN : s_13_6 341 # ASSIGN : s_13_7 440 # ASSIGN : s_13_8 505 # ASSIGN : s_13_9 517 # ASSIGN : s_14_0 12 # ASSIGN : s_14_1 84 # ASSIGN : s_14_2 459 # ASSIGN : s_14_3 631 # ASSIGN : s_14_4 757 # ASSIGN : s_14_5 995 # ASSIGN : s_14_6 1094 # ASSIGN : s_14_7 1108 # ASSIGN : s_14_8 1163 # ASSIGN : s_14_9 1181 # ASSIGN : s_15_0 46 # ASSIGN : s_15_1 276 # ASSIGN : s_15_2 290 # ASSIGN : s_15_3 383 # ASSIGN : s_15_4 598 # ASSIGN : s_15_5 743 # ASSIGN : s_15_6 818 # ASSIGN : s_15_7 897 # ASSIGN : s_15_8 968 # ASSIGN : s_15_9 1200 # ASSIGN : s_16_0 72 # ASSIGN : s_16_1 114 # ASSIGN : s_16_2 390 # ASSIGN : s_16_3 583 # ASSIGN : s_16_4 615 # ASSIGN : s_16_5 665 # ASSIGN : s_16_6 723 # ASSIGN : s_16_7 773 # ASSIGN : s_16_8 847 # ASSIGN : s_16_9 934 # ASSIGN : s_17_0 28 # ASSIGN : s_17_1 74 # ASSIGN : s_17_2 137 # ASSIGN : s_17_3 159 # ASSIGN : s_17_4 284 # ASSIGN : s_17_5 350 # ASSIGN : s_17_6 365 # ASSIGN : s_17_7 438 # ASSIGN : s_17_8 863 # ASSIGN : s_17_9 871 # ASSIGN : s_18_0 218 # ASSIGN : s_18_1 315 # ASSIGN : s_18_2 680 # ASSIGN : s_18_3 761 # ASSIGN : s_18_4 848 # ASSIGN : s_18_5 906 # ASSIGN : s_18_6 966 # ASSIGN : s_18_7 1034 # ASSIGN : s_18_8 1066 # ASSIGN : s_18_9 1175 # ASSIGN : s_19_0 103 # ASSIGN : s_19_1 299 # ASSIGN : s_19_2 424 # ASSIGN : s_19_3 630 # ASSIGN : s_19_4 736 # ASSIGN : s_19_5 791 # ASSIGN : s_19_6 1004 # ASSIGN : s_19_7 1045 # ASSIGN : s_19_8 1135 # ASSIGN : s_19_9 1202 SHOW_RESULT 1222 END : 1222 (1 seconds) [Thu Jun 1 18:05:51 2006] SHOW_RESULT 1222 CPU : 0.829999999999993 = 0.819999999999993 + 0.01 + 0 + 0 # BOUND : makespan 1218 1222 MODIFY_CNF 1220 BEGIN : [Thu Jun 1 18:05:51 2006] MODIFY_CNF 1220 END : 142852037 bytes (0 seconds) [Thu Jun 1 18:05:51 2006] MODIFY_CNF 1220 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1220 BEGIN : [Thu Jun 1 18:05:51 2006] CMD : minisat /work/tamura/csp2sat78524.cnf /work/tamura/csp2sat78524.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 3204606 9472678 | 1068202 0 0 NaNQ | 0.000 % | | 100 | 3204606 9472678 | 1175022 100 1608 16.1 | 52.529 % | | 250 | 3204606 9472678 | 1292524 250 4453 17.8 | 52.529 % | | 475 | 3204606 9472678 | 1421776 475 8752 18.4 | 52.529 % | | 812 | 3204606 9472678 | 1563954 812 16609 20.5 | 52.529 % | | 1320 | 3204606 9472678 | 1720350 1320 27415 20.8 | 52.529 % | | 2079 | 3204606 9472678 | 1892385 2079 48971 23.6 | 52.529 % | | 3219 | 3204606 9472678 | 2081623 3219 77880 24.2 | 52.529 % | | 4928 | 3204606 9472678 | 2289785 4928 122332 24.8 | 52.529 % | | 7490 | 3204606 9472678 | 2518764 7490 162674 21.7 | 52.529 % | | 11335 | 3204606 9472678 | 2770640 11335 281514 24.8 | 52.529 % | | 17101 | 3204606 9472678 | 3047704 17101 522587 30.6 | 52.529 % | | 25751 | 3204606 9472678 | 3352475 25751 771147 29.9 | 52.529 % | | 38725 | 3204606 9472678 | 3687723 38725 1152789 29.8 | 52.529 % | | 58186 | 3204606 9472678 | 4056495 58186 1964959 33.8 | 52.529 % | | 87378 | 3204606 9472678 | 4462144 87378 3366347 38.5 | 52.529 % | | 131167 | 3204606 9472678 | 4908359 131167 6110699 46.6 | 52.529 % | | 196853 | 3204606 9472678 | 5399195 196853 10099047 51.3 | 52.529 % | | 295379 | 3204606 9472678 | 5939114 295379 14183227 48.0 | 52.529 % | | 443168 | 3204606 9472678 | 6533026 443168 18193878 41.1 | 52.529 % | | 664852 | 3204606 9472678 | 7186328 664852 30498527 45.9 | 52.529 % | ==============================================================================) restarts : 21 conflicts : 985382 (70 /sec) decisions : 1382851 (98 /sec) propagations : 8732956799 (620806 /sec) inspects : 138515840651 (9846772 /sec) conflict literals : 51449172 (35.75 % deleted) CPU time : 14067.1 s SATISFIABLE VERIFY_CNF 1220 END : (14086 seconds) [Thu Jun 1 22:00:37 2006] VERIFY_CNF 1220 CPU : 14069.58 = 0 + 0.02 + 14069.41 + 0.15 # RESULT : makespan 1220 SATISFIABLE SHOW_RESULT 1220 BEGIN : [Thu Jun 1 22:00:37 2006] # ASSIGN : makespan 1220 # ASSIGN : s_0_0 9 # ASSIGN : s_0_1 61 # ASSIGN : s_0_2 87 # ASSIGN : s_0_3 336 # ASSIGN : s_0_4 448 # ASSIGN : s_0_5 664 # ASSIGN : s_0_6 685 # ASSIGN : s_0_7 851 # ASSIGN : s_0_8 953 # ASSIGN : s_0_9 1165 # ASSIGN : s_1_0 319 # ASSIGN : s_1_1 387 # ASSIGN : s_1_2 485 # ASSIGN : s_1_3 524 # ASSIGN : s_1_4 691 # ASSIGN : s_1_5 703 # ASSIGN : s_1_6 809 # ASSIGN : s_1_7 914 # ASSIGN : s_1_8 1147 # ASSIGN : s_1_9 1178 # ASSIGN : s_2_0 28 # ASSIGN : s_2_1 131 # ASSIGN : s_2_2 236 # ASSIGN : s_2_3 300 # ASSIGN : s_2_4 359 # ASSIGN : s_2_5 378 # ASSIGN : s_2_6 441 # ASSIGN : s_2_7 542 # ASSIGN : s_2_8 603 # ASSIGN : s_2_9 1158 # ASSIGN : s_3_0 138 # ASSIGN : s_3_1 225 # ASSIGN : s_3_2 302 # ASSIGN : s_3_3 413 # ASSIGN : s_3_4 482 # ASSIGN : s_3_5 579 # ASSIGN : s_3_6 621 # ASSIGN : s_3_7 653 # ASSIGN : s_3_8 903 # ASSIGN : s_3_9 1044 # ASSIGN : s_4_0 27 # ASSIGN : s_4_1 133 # ASSIGN : s_4_2 158 # ASSIGN : s_4_3 233 # ASSIGN : s_4_4 310 # ASSIGN : s_4_5 375 # ASSIGN : s_4_6 392 # ASSIGN : s_4_7 876 # ASSIGN : s_4_8 980 # ASSIGN : s_4_9 1104 # ASSIGN : s_5_0 641 # ASSIGN : s_5_1 648 # ASSIGN : s_5_2 761 # ASSIGN : s_5_3 858 # ASSIGN : s_5_4 893 # ASSIGN : s_5_5 928 # ASSIGN : s_5_6 1012 # ASSIGN : s_5_7 1040 # ASSIGN : s_5_8 1116 # ASSIGN : s_5_9 1211 # ASSIGN : s_6_0 74 # ASSIGN : s_6_1 352 # ASSIGN : s_6_2 395 # ASSIGN : s_6_3 442 # ASSIGN : s_6_4 510 # ASSIGN : s_6_5 576 # ASSIGN : s_6_6 746 # ASSIGN : s_6_7 805 # ASSIGN : s_6_8 963 # ASSIGN : s_6_9 1044 # ASSIGN : s_7_0 65 # ASSIGN : s_7_1 93 # ASSIGN : s_7_2 154 # ASSIGN : s_7_3 260 # ASSIGN : s_7_4 531 # ASSIGN : s_7_5 562 # ASSIGN : s_7_6 821 # ASSIGN : s_7_7 1006 # ASSIGN : s_7_8 1133 # ASSIGN : s_7_9 1181 # ASSIGN : s_8_0 383 # ASSIGN : s_8_1 471 # ASSIGN : s_8_2 613 # ASSIGN : s_8_3 693 # ASSIGN : s_8_4 730 # ASSIGN : s_8_5 862 # ASSIGN : s_8_6 888 # ASSIGN : s_8_7 921 # ASSIGN : s_8_8 1011 # ASSIGN : s_8_9 1212 # ASSIGN : s_9_0 223 # ASSIGN : s_9_1 319 # ASSIGN : s_9_2 432 # ASSIGN : s_9_3 515 # ASSIGN : s_9_4 599 # ASSIGN : s_9_5 780 # ASSIGN : s_9_6 896 # ASSIGN : s_9_7 986 # ASSIGN : s_9_8 1071 # ASSIGN : s_9_9 1151 # ASSIGN : s_10_0 5 # ASSIGN : s_10_1 29 # ASSIGN : s_10_2 136 # ASSIGN : s_10_3 161 # ASSIGN : s_10_4 182 # ASSIGN : s_10_5 311 # ASSIGN : s_10_6 609 # ASSIGN : s_10_7 694 # ASSIGN : s_10_8 774 # ASSIGN : s_10_9 856 # ASSIGN : s_11_0 64 # ASSIGN : s_11_1 359 # ASSIGN : s_11_2 411 # ASSIGN : s_11_3 483 # ASSIGN : s_11_4 569 # ASSIGN : s_11_5 592 # ASSIGN : s_11_6 712 # ASSIGN : s_11_7 796 # ASSIGN : s_11_8 966 # ASSIGN : s_11_9 1093 # ASSIGN : s_12_0 10 # ASSIGN : s_12_1 33 # ASSIGN : s_12_2 134 # ASSIGN : s_12_3 233 # ASSIGN : s_12_4 284 # ASSIGN : s_12_5 354 # ASSIGN : s_12_6 421 # ASSIGN : s_12_7 524 # ASSIGN : s_12_8 682 # ASSIGN : s_12_9 1173 # ASSIGN : s_13_0 1 # ASSIGN : s_13_1 168 # ASSIGN : s_13_2 394 # ASSIGN : s_13_3 682 # ASSIGN : s_13_4 780 # ASSIGN : s_13_5 808 # ASSIGN : s_13_6 872 # ASSIGN : s_13_7 1010 # ASSIGN : s_13_8 1082 # ASSIGN : s_13_9 1118 # ASSIGN : s_14_0 9 # ASSIGN : s_14_1 81 # ASSIGN : s_14_2 470 # ASSIGN : s_14_3 537 # ASSIGN : s_14_4 616 # ASSIGN : s_14_5 904 # ASSIGN : s_14_6 954 # ASSIGN : s_14_7 968 # ASSIGN : s_14_8 1023 # ASSIGN : s_14_9 1041 # ASSIGN : s_15_0 29 # ASSIGN : s_15_1 125 # ASSIGN : s_15_2 168 # ASSIGN : s_15_3 566 # ASSIGN : s_15_4 617 # ASSIGN : s_15_5 709 # ASSIGN : s_15_6 849 # ASSIGN : s_15_7 970 # ASSIGN : s_15_8 1073 # ASSIGN : s_15_9 1198 # ASSIGN : s_16_0 279 # ASSIGN : s_16_1 331 # ASSIGN : s_16_2 645 # ASSIGN : s_16_3 752 # ASSIGN : s_16_4 784 # ASSIGN : s_16_5 828 # ASSIGN : s_16_6 886 # ASSIGN : s_16_7 920 # ASSIGN : s_16_8 974 # ASSIGN : s_16_9 1067 # ASSIGN : s_17_0 9 # ASSIGN : s_17_1 99 # ASSIGN : s_17_2 139 # ASSIGN : s_17_3 156 # ASSIGN : s_17_4 218 # ASSIGN : s_17_5 285 # ASSIGN : s_17_6 346 # ASSIGN : s_17_7 399 # ASSIGN : s_17_8 507 # ASSIGN : s_17_9 551 # ASSIGN : s_18_0 178 # ASSIGN : s_18_1 269 # ASSIGN : s_18_2 374 # ASSIGN : s_18_3 437 # ASSIGN : s_18_4 704 # ASSIGN : s_18_5 788 # ASSIGN : s_18_6 857 # ASSIGN : s_18_7 1062 # ASSIGN : s_18_8 1094 # ASSIGN : s_18_9 1200 # ASSIGN : s_19_0 53 # ASSIGN : s_19_1 218 # ASSIGN : s_19_2 303 # ASSIGN : s_19_3 691 # ASSIGN : s_19_4 772 # ASSIGN : s_19_5 787 # ASSIGN : s_19_6 1013 # ASSIGN : s_19_7 1043 # ASSIGN : s_19_8 1133 # ASSIGN : s_19_9 1200 SHOW_RESULT 1220 END : 1220 (1 seconds) [Thu Jun 1 22:00:38 2006] SHOW_RESULT 1220 CPU : 0.829999999999984 = 0.829999999999984 + 0 + 0 + 0 # BOUND : makespan 1218 1220 MODIFY_CNF 1219 BEGIN : [Thu Jun 1 22:00:38 2006] MODIFY_CNF 1219 END : 142852037 bytes (0 seconds) [Thu Jun 1 22:00:38 2006] MODIFY_CNF 1219 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1219 BEGIN : [Thu Jun 1 22:00:38 2006] CMD : minisat /work/tamura/csp2sat78524.cnf /work/tamura/csp2sat78524.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 3200650 9461011 | 1066883 0 0 NaNQ | 0.000 % | | 101 | 3200650 9461011 | 1173571 101 1632 16.2 | 52.595 % | | 251 | 3200650 9461011 | 1290928 251 6317 25.2 | 52.595 % | | 476 | 3200650 9461011 | 1420021 476 11352 23.8 | 52.595 % | | 814 | 3200650 9461011 | 1562023 814 21399 26.3 | 52.595 % | | 1321 | 3200650 9461011 | 1718225 1321 28442 21.5 | 52.596 % | | 2081 | 3200650 9461011 | 1890048 2081 46411 22.3 | 52.595 % | | 3220 | 3200650 9461011 | 2079053 3220 67912 21.1 | 52.595 % | | 4928 | 3200650 9461011 | 2286958 4928 104111 21.1 | 52.595 % | | 7492 | 3200650 9461011 | 2515654 7492 145494 19.4 | 52.595 % | | 11336 | 3200650 9461011 | 2767219 11336 290495 25.6 | 52.595 % | | 17103 | 3200650 9461011 | 3043941 17103 482506 28.2 | 52.595 % | | 25752 | 3200650 9461011 | 3348335 25752 895918 34.8 | 52.595 % | | 38726 | 3200650 9461011 | 3683169 38726 1460105 37.7 | 52.595 % | | 58188 | 3200650 9461011 | 4051486 58188 2236500 38.4 | 52.595 % | | 87381 | 3200650 9461011 | 4456635 87381 4412357 50.5 | 52.595 % | | 131170 | 3200650 9461011 | 4902298 131170 6876955 52.4 | 52.595 % | | 196854 | 3200650 9461011 | 5392528 196854 11191376 56.9 | 52.595 % | | 295380 | 3200650 9461011 | 5931781 295380 16763242 56.8 | 52.595 % | ==============================================================================) restarts : 19 conflicts : 301802 (93 /sec) decisions : 441716 (136 /sec) propagations : 2696952628 (828929 /sec) inspects : 41615731721 (12790915 /sec) conflict literals : 17044694 (32.06 % deleted) CPU time : 3253.54 s SATISFIABLE VERIFY_CNF 1219 END : (3259 seconds) [Thu Jun 1 22:54:57 2006] VERIFY_CNF 1219 CPU : 3255.86 = 0 + 0.0299999999999999 + 3255.68 + 0.15 # RESULT : makespan 1219 SATISFIABLE SHOW_RESULT 1219 BEGIN : [Thu Jun 1 22:54:57 2006] # ASSIGN : makespan 1219 # ASSIGN : s_0_0 1 # ASSIGN : s_0_1 53 # ASSIGN : s_0_2 79 # ASSIGN : s_0_3 209 # ASSIGN : s_0_4 260 # ASSIGN : s_0_5 697 # ASSIGN : s_0_6 844 # ASSIGN : s_0_7 939 # ASSIGN : s_0_8 1019 # ASSIGN : s_0_9 1164 # ASSIGN : s_1_0 404 # ASSIGN : s_1_1 540 # ASSIGN : s_1_2 750 # ASSIGN : s_1_3 797 # ASSIGN : s_1_4 876 # ASSIGN : s_1_5 895 # ASSIGN : s_1_6 972 # ASSIGN : s_1_7 1049 # ASSIGN : s_1_8 1146 # ASSIGN : s_1_9 1177 # ASSIGN : s_2_0 11 # ASSIGN : s_2_1 197 # ASSIGN : s_2_2 294 # ASSIGN : s_2_3 358 # ASSIGN : s_2_4 412 # ASSIGN : s_2_5 431 # ASSIGN : s_2_6 519 # ASSIGN : s_2_7 674 # ASSIGN : s_2_8 708 # ASSIGN : s_2_9 1157 # ASSIGN : s_3_0 50 # ASSIGN : s_3_1 141 # ASSIGN : s_3_2 218 # ASSIGN : s_3_3 317 # ASSIGN : s_3_4 387 # ASSIGN : s_3_5 474 # ASSIGN : s_3_6 512 # ASSIGN : s_3_7 536 # ASSIGN : s_3_8 577 # ASSIGN : s_3_9 960 # ASSIGN : s_4_0 18 # ASSIGN : s_4_1 116 # ASSIGN : s_4_2 150 # ASSIGN : s_4_3 225 # ASSIGN : s_4_4 337 # ASSIGN : s_4_5 386 # ASSIGN : s_4_6 433 # ASSIGN : s_4_7 888 # ASSIGN : s_4_8 961 # ASSIGN : s_4_9 1020 # ASSIGN : s_5_0 544 # ASSIGN : s_5_1 568 # ASSIGN : s_5_2 644 # ASSIGN : s_5_3 745 # ASSIGN : s_5_4 787 # ASSIGN : s_5_5 860 # ASSIGN : s_5_6 1011 # ASSIGN : s_5_7 1039 # ASSIGN : s_5_8 1115 # ASSIGN : s_5_9 1210 # ASSIGN : s_6_0 57 # ASSIGN : s_6_1 302 # ASSIGN : s_6_2 473 # ASSIGN : s_6_3 540 # ASSIGN : s_6_4 582 # ASSIGN : s_6_5 643 # ASSIGN : s_6_6 659 # ASSIGN : s_6_7 718 # ASSIGN : s_6_8 809 # ASSIGN : s_6_9 859 # ASSIGN : s_7_0 48 # ASSIGN : s_7_1 154 # ASSIGN : s_7_2 197 # ASSIGN : s_7_3 360 # ASSIGN : s_7_4 459 # ASSIGN : s_7_5 482 # ASSIGN : s_7_6 709 # ASSIGN : s_7_7 932 # ASSIGN : s_7_8 1021 # ASSIGN : s_7_9 1180 # ASSIGN : s_8_0 178 # ASSIGN : s_8_1 211 # ASSIGN : s_8_2 395 # ASSIGN : s_8_3 478 # ASSIGN : s_8_4 520 # ASSIGN : s_8_5 612 # ASSIGN : s_8_6 638 # ASSIGN : s_8_7 671 # ASSIGN : s_8_8 1166 # ASSIGN : s_8_9 1211 # ASSIGN : s_9_0 3 # ASSIGN : s_9_1 169 # ASSIGN : s_9_2 246 # ASSIGN : s_9_3 324 # ASSIGN : s_9_4 515 # ASSIGN : s_9_5 710 # ASSIGN : s_9_6 813 # ASSIGN : s_9_7 887 # ASSIGN : s_9_8 1004 # ASSIGN : s_9_9 1072 # ASSIGN : s_10_0 289 # ASSIGN : s_10_1 313 # ASSIGN : s_10_2 345 # ASSIGN : s_10_3 370 # ASSIGN : s_10_4 525 # ASSIGN : s_10_5 629 # ASSIGN : s_10_6 754 # ASSIGN : s_10_7 878 # ASSIGN : s_10_8 937 # ASSIGN : s_10_9 1141 # ASSIGN : s_11_0 56 # ASSIGN : s_11_1 484 # ASSIGN : s_11_2 551 # ASSIGN : s_11_3 623 # ASSIGN : s_11_4 722 # ASSIGN : s_11_5 789 # ASSIGN : s_11_6 896 # ASSIGN : s_11_7 1019 # ASSIGN : s_11_8 1116 # ASSIGN : s_11_9 1161 # ASSIGN : s_12_0 1 # ASSIGN : s_12_1 99 # ASSIGN : s_12_2 219 # ASSIGN : s_12_3 291 # ASSIGN : s_12_4 347 # ASSIGN : s_12_5 415 # ASSIGN : s_12_6 540 # ASSIGN : s_12_7 602 # ASSIGN : s_12_8 660 # ASSIGN : s_12_9 1172 # ASSIGN : s_13_0 1 # ASSIGN : s_13_1 146 # ASSIGN : s_13_2 196 # ASSIGN : s_13_3 215 # ASSIGN : s_13_4 512 # ASSIGN : s_13_5 609 # ASSIGN : s_13_6 673 # ASSIGN : s_13_7 794 # ASSIGN : s_13_8 1009 # ASSIGN : s_13_9 1117 # ASSIGN : s_14_0 9 # ASSIGN : s_14_1 81 # ASSIGN : s_14_2 479 # ASSIGN : s_14_3 550 # ASSIGN : s_14_4 634 # ASSIGN : s_14_5 780 # ASSIGN : s_14_6 830 # ASSIGN : s_14_7 888 # ASSIGN : s_14_8 943 # ASSIGN : s_14_9 968 # ASSIGN : s_15_0 73 # ASSIGN : s_15_1 188 # ASSIGN : s_15_2 267 # ASSIGN : s_15_3 739 # ASSIGN : s_15_4 794 # ASSIGN : s_15_5 864 # ASSIGN : s_15_6 987 # ASSIGN : s_15_7 1066 # ASSIGN : s_15_8 1137 # ASSIGN : s_15_9 1197 # ASSIGN : s_16_0 137 # ASSIGN : s_16_1 168 # ASSIGN : s_16_2 374 # ASSIGN : s_16_3 432 # ASSIGN : s_16_4 629 # ASSIGN : s_16_5 696 # ASSIGN : s_16_6 760 # ASSIGN : s_16_7 843 # ASSIGN : s_16_8 899 # ASSIGN : s_16_9 968 # ASSIGN : s_17_0 6 # ASSIGN : s_17_1 99 # ASSIGN : s_17_2 139 # ASSIGN : s_17_3 156 # ASSIGN : s_17_4 277 # ASSIGN : s_17_5 343 # ASSIGN : s_17_6 403 # ASSIGN : s_17_7 482 # ASSIGN : s_17_8 688 # ASSIGN : s_17_9 767 # ASSIGN : s_18_0 202 # ASSIGN : s_18_1 267 # ASSIGN : s_18_2 332 # ASSIGN : s_18_3 395 # ASSIGN : s_18_4 786 # ASSIGN : s_18_5 857 # ASSIGN : s_18_6 886 # ASSIGN : s_18_7 1106 # ASSIGN : s_18_8 1138 # ASSIGN : s_18_9 1199 # ASSIGN : s_19_0 206 # ASSIGN : s_19_1 311 # ASSIGN : s_19_2 408 # ASSIGN : s_19_3 464 # ASSIGN : s_19_4 562 # ASSIGN : s_19_5 709 # ASSIGN : s_19_6 779 # ASSIGN : s_19_7 980 # ASSIGN : s_19_8 1070 # ASSIGN : s_19_9 1199 SHOW_RESULT 1219 END : 1219 (1 seconds) [Thu Jun 1 22:54:58 2006] SHOW_RESULT 1219 CPU : 0.829999999999984 = 0.829999999999984 + 0 + 0 + 0 # BOUND : makespan 1218 1219 MODIFY_CNF 1218 BEGIN : [Thu Jun 1 22:54:58 2006] MODIFY_CNF 1218 END : 142852037 bytes (0 seconds) [Thu Jun 1 22:54:58 2006] MODIFY_CNF 1218 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1218 BEGIN : [Thu Jun 1 22:54:58 2006] CMD : minisat /work/tamura/csp2sat78524.cnf /work/tamura/csp2sat78524.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 3196660 9449241 | 1065553 0 0 NaNQ | 0.000 % | | 100 | 3196660 9449241 | 1172108 100 1812 18.1 | 52.662 % | | 251 | 3196660 9449241 | 1289319 251 5134 20.5 | 52.662 % | | 476 | 3196660 9449241 | 1418251 476 11110 23.3 | 52.662 % | | 813 | 3196660 9449241 | 1560076 813 22599 27.8 | 52.662 % | | 1319 | 3196660 9449241 | 1716083 1319 38308 29.0 | 52.662 % | | 2079 | 3196660 9449241 | 1887692 2079 57406 27.6 | 52.662 % | | 3219 | 3196660 9449241 | 2076461 3219 77313 24.0 | 52.662 % | | 4928 | 3196660 9449241 | 2284107 4928 112565 22.8 | 52.662 % | | 7490 | 3196660 9449241 | 2512518 7490 176440 23.6 | 52.662 % | | 11335 | 3196660 9449241 | 2763770 11335 351890 31.0 | 52.662 % | | 17102 | 3196660 9449241 | 3040147 17102 507177 29.7 | 52.662 % | | 25751 | 3196660 9449241 | 3344161 25751 775511 30.1 | 52.662 % | | 38725 | 3196660 9449241 | 3678577 38725 1425950 36.8 | 52.662 % | | 58187 | 3196660 9449241 | 4046435 58187 2409608 41.4 | 52.662 % | | 87379 | 3196660 9449241 | 4451079 87379 3253813 37.2 | 52.662 % | | 131169 | 3196660 9449241 | 4896187 131169 5045352 38.5 | 52.662 % | | 196853 | 3196660 9449241 | 5385805 196853 8412450 42.7 | 52.662 % | | 295379 | 3196660 9449241 | 5924386 295379 11488999 38.9 | 52.662 % | | 443169 | 3196660 9449241 | 6516825 443169 18223355 41.1 | 52.662 % | | 664853 | 3196660 9449241 | 7168507 664853 24971244 37.6 | 52.662 % | | 997379 | 3196660 9449241 | 7885358 997379 34825827 34.9 | 52.662 % | ==============================================================================) restarts : 22 conflicts : 1093813 (83 /sec) decisions : 1476574 (113 /sec) propagations : 8528224830 (650577 /sec) inspects : 134582708410 (10266658 /sec) conflict literals : 41411019 (36.16 % deleted) CPU time : 13108.7 s SATISFIABLE VERIFY_CNF 1218 END : (13126 seconds) [Fri Jun 2 02:33:44 2006] VERIFY_CNF 1218 CPU : 13112.05 = 0.0100000000000477 + 0.03 + 13111.45 + 0.56 # RESULT : makespan 1218 SATISFIABLE SHOW_RESULT 1218 BEGIN : [Fri Jun 2 02:33:44 2006] # ASSIGN : makespan 1218 # ASSIGN : s_0_0 28 # ASSIGN : s_0_1 165 # ASSIGN : s_0_2 261 # ASSIGN : s_0_3 422 # ASSIGN : s_0_4 452 # ASSIGN : s_0_5 583 # ASSIGN : s_0_6 604 # ASSIGN : s_0_7 699 # ASSIGN : s_0_8 1076 # ASSIGN : s_0_9 1163 # ASSIGN : s_1_0 79 # ASSIGN : s_1_1 134 # ASSIGN : s_1_2 240 # ASSIGN : s_1_3 300 # ASSIGN : s_1_4 408 # ASSIGN : s_1_5 455 # ASSIGN : s_1_6 557 # ASSIGN : s_1_7 651 # ASSIGN : s_1_8 725 # ASSIGN : s_1_9 903 # ASSIGN : s_2_0 70 # ASSIGN : s_2_1 284 # ASSIGN : s_2_2 376 # ASSIGN : s_2_3 440 # ASSIGN : s_2_4 673 # ASSIGN : s_2_5 760 # ASSIGN : s_2_6 803 # ASSIGN : s_2_7 901 # ASSIGN : s_2_8 935 # ASSIGN : s_2_9 1079 # ASSIGN : s_3_0 422 # ASSIGN : s_3_1 509 # ASSIGN : s_3_2 586 # ASSIGN : s_3_3 687 # ASSIGN : s_3_4 756 # ASSIGN : s_3_5 843 # ASSIGN : s_3_6 901 # ASSIGN : s_3_7 988 # ASSIGN : s_3_8 1062 # ASSIGN : s_3_9 1158 # ASSIGN : s_4_0 2 # ASSIGN : s_4_1 107 # ASSIGN : s_4_2 132 # ASSIGN : s_4_3 219 # ASSIGN : s_4_4 296 # ASSIGN : s_4_5 359 # ASSIGN : s_4_6 376 # ASSIGN : s_4_7 467 # ASSIGN : s_4_8 717 # ASSIGN : s_4_9 1029 # ASSIGN : s_5_0 3 # ASSIGN : s_5_1 18 # ASSIGN : s_5_2 80 # ASSIGN : s_5_3 274 # ASSIGN : s_5_4 538 # ASSIGN : s_5_5 925 # ASSIGN : s_5_6 960 # ASSIGN : s_5_7 988 # ASSIGN : s_5_8 1064 # ASSIGN : s_5_9 1209 # ASSIGN : s_6_0 11 # ASSIGN : s_6_1 379 # ASSIGN : s_6_2 679 # ASSIGN : s_6_3 839 # ASSIGN : s_6_4 881 # ASSIGN : s_6_5 941 # ASSIGN : s_6_6 957 # ASSIGN : s_6_7 1016 # ASSIGN : s_6_8 1141 # ASSIGN : s_6_9 1191 # ASSIGN : s_7_0 2 # ASSIGN : s_7_1 37 # ASSIGN : s_7_2 80 # ASSIGN : s_7_3 94 # ASSIGN : s_7_4 168 # ASSIGN : s_7_5 207 # ASSIGN : s_7_6 279 # ASSIGN : s_7_7 321 # ASSIGN : s_7_8 858 # ASSIGN : s_7_9 1179 # ASSIGN : s_8_0 237 # ASSIGN : s_8_1 310 # ASSIGN : s_8_2 725 # ASSIGN : s_8_3 856 # ASSIGN : s_8_4 893 # ASSIGN : s_8_5 962 # ASSIGN : s_8_6 995 # ASSIGN : s_8_7 1029 # ASSIGN : s_8_8 1125 # ASSIGN : s_8_9 1183 # ASSIGN : s_9_0 188 # ASSIGN : s_9_1 320 # ASSIGN : s_9_2 347 # ASSIGN : s_9_3 425 # ASSIGN : s_9_4 526 # ASSIGN : s_9_5 629 # ASSIGN : s_9_6 738 # ASSIGN : s_9_7 812 # ASSIGN : s_9_8 945 # ASSIGN : s_9_9 1129 # ASSIGN : s_10_0 144 # ASSIGN : s_10_1 385 # ASSIGN : s_10_2 438 # ASSIGN : s_10_3 486 # ASSIGN : s_10_4 814 # ASSIGN : s_10_5 961 # ASSIGN : s_10_6 1042 # ASSIGN : s_10_7 1118 # ASSIGN : s_10_8 1146 # ASSIGN : s_10_9 1198 # ASSIGN : s_11_0 154 # ASSIGN : s_11_1 317 # ASSIGN : s_11_2 345 # ASSIGN : s_11_3 417 # ASSIGN : s_11_4 503 # ASSIGN : s_11_5 535 # ASSIGN : s_11_6 634 # ASSIGN : s_11_7 715 # ASSIGN : s_11_8 867 # ASSIGN : s_11_9 985 # ASSIGN : s_12_0 309 # ASSIGN : s_12_1 539 # ASSIGN : s_12_2 639 # ASSIGN : s_12_3 692 # ASSIGN : s_12_4 787 # ASSIGN : s_12_5 814 # ASSIGN : s_12_6 881 # ASSIGN : s_12_7 943 # ASSIGN : s_12_8 1014 # ASSIGN : s_12_9 1191 # ASSIGN : s_13_0 0 # ASSIGN : s_13_1 104 # ASSIGN : s_13_2 171 # ASSIGN : s_13_3 191 # ASSIGN : s_13_4 289 # ASSIGN : s_13_5 326 # ASSIGN : s_13_6 382 # ASSIGN : s_13_7 494 # ASSIGN : s_13_8 623 # ASSIGN : s_13_9 635 # ASSIGN : s_14_0 147 # ASSIGN : s_14_1 511 # ASSIGN : s_14_2 637 # ASSIGN : s_14_3 698 # ASSIGN : s_14_4 777 # ASSIGN : s_14_5 907 # ASSIGN : s_14_6 1028 # ASSIGN : s_14_7 1104 # ASSIGN : s_14_8 1159 # ASSIGN : s_14_9 1177 # ASSIGN : s_15_0 75 # ASSIGN : s_15_1 218 # ASSIGN : s_15_2 232 # ASSIGN : s_15_3 420 # ASSIGN : s_15_4 586 # ASSIGN : s_15_5 720 # ASSIGN : s_15_6 822 # ASSIGN : s_15_7 945 # ASSIGN : s_15_8 1136 # ASSIGN : s_15_9 1196 # ASSIGN : s_16_0 265 # ASSIGN : s_16_1 338 # ASSIGN : s_16_2 532 # ASSIGN : s_16_3 763 # ASSIGN : s_16_4 795 # ASSIGN : s_16_5 846 # ASSIGN : s_16_6 933 # ASSIGN : s_16_7 1043 # ASSIGN : s_16_8 1076 # ASSIGN : s_16_9 1145 # ASSIGN : s_17_0 10 # ASSIGN : s_17_1 54 # ASSIGN : s_17_2 158 # ASSIGN : s_17_3 175 # ASSIGN : s_17_4 244 # ASSIGN : s_17_5 332 # ASSIGN : s_17_6 411 # ASSIGN : s_17_7 463 # ASSIGN : s_17_8 904 # ASSIGN : s_17_9 912 # ASSIGN : s_18_0 100 # ASSIGN : s_18_1 190 # ASSIGN : s_18_2 476 # ASSIGN : s_18_3 548 # ASSIGN : s_18_4 886 # ASSIGN : s_18_5 967 # ASSIGN : s_18_6 990 # ASSIGN : s_18_7 1047 # ASSIGN : s_18_8 1107 # ASSIGN : s_18_9 1171 # ASSIGN : s_19_0 152 # ASSIGN : s_19_1 237 # ASSIGN : s_19_2 369 # ASSIGN : s_19_3 440 # ASSIGN : s_19_4 501 # ASSIGN : s_19_5 516 # ASSIGN : s_19_6 590 # ASSIGN : s_19_7 620 # ASSIGN : s_19_8 710 # ASSIGN : s_19_9 1009 SHOW_RESULT 1218 END : 1218 (1 seconds) [Fri Jun 2 02:33:45 2006] SHOW_RESULT 1218 CPU : 0.829999999999984 = 0.829999999999984 + 0 + 0 + 0 # BOUND : makespan 1218 1218 MAIN END : (33092 seconds) [Fri Jun 2 02:33:45 2006] MAIN CPU : 33052.51 = 307.4 + 0.65 + 32741.53 + 2.93