MAIN BEGIN : [Thu Jun 1 20:15:13 2006] READ BEGIN : csp/la28.csp [Thu Jun 1 20:15:13 2006] READ END : csp/la28.csp (5 seconds) [Thu Jun 1 20:15:18 2006] READ CPU : 5.35 = 5.35 + 0 + 0 + 0 # BOUND : makespan 1216 1670 GENERATE_CNF 1670 BEGIN : [Thu Jun 1 20:15:18 2006] GENERATE_CNF 1670 END : 338856 variables 6788057 clauses 162515793 bytes (334 seconds) [Thu Jun 1 20:20:52 2006] GENERATE_CNF 1670 CPU : 333.66 = 333.19 + 0.47 + 0 + 0 MODIFY_CNF 1443 BEGIN : [Thu Jun 1 20:20:52 2006] MODIFY_CNF 1443 END : 162515799 bytes (0 seconds) [Thu Jun 1 20:20:52 2006] MODIFY_CNF 1443 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1443 BEGIN : [Thu Jun 1 20:20:52 2006] CMD : minisat /work/tamura/csp2sat70812.cnf /work/tamura/csp2sat70812.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 4115608 12162555 | 1371869 0 0 NaNQ | 0.000 % | ==============================================================================) restarts : 1 conflicts : 38 (5 /sec) decisions : 1504 (179 /sec) propagations : 630379 (75178 /sec) inspects : 9236609 (1101539 /sec) conflict literals : 354 (3.54 % deleted) CPU time : 8.38518 s SATISFIABLE VERIFY_CNF 1443 END : (12 seconds) [Thu Jun 1 20:21:04 2006] VERIFY_CNF 1443 CPU : 10.71 = 0 + 0.01 + 10.55 + 0.15 # RESULT : makespan 1443 SATISFIABLE SHOW_RESULT 1443 BEGIN : [Thu Jun 1 20:21:04 2006] # ASSIGN : makespan 1443 # ASSIGN : s_0_0 119 # ASSIGN : s_0_1 151 # ASSIGN : s_0_2 281 # ASSIGN : s_0_3 768 # ASSIGN : s_0_4 808 # ASSIGN : s_0_5 829 # ASSIGN : s_0_6 1273 # ASSIGN : s_0_7 1354 # ASSIGN : s_0_8 1391 # ASSIGN : s_0_9 1434 # ASSIGN : s_1_0 497 # ASSIGN : s_1_1 567 # ASSIGN : s_1_2 622 # ASSIGN : s_1_3 643 # ASSIGN : s_1_4 716 # ASSIGN : s_1_5 835 # ASSIGN : s_1_6 1008 # ASSIGN : s_1_7 1158 # ASSIGN : s_1_8 1242 # ASSIGN : s_1_9 1362 # ASSIGN : s_2_0 315 # ASSIGN : s_2_1 402 # ASSIGN : s_2_2 491 # ASSIGN : s_2_3 581 # ASSIGN : s_2_4 625 # ASSIGN : s_2_5 804 # ASSIGN : s_2_6 1073 # ASSIGN : s_2_7 1102 # ASSIGN : s_2_8 1205 # ASSIGN : s_2_9 1403 # ASSIGN : s_3_0 24 # ASSIGN : s_3_1 492 # ASSIGN : s_3_2 551 # ASSIGN : s_3_3 595 # ASSIGN : s_3_4 674 # ASSIGN : s_3_5 846 # ASSIGN : s_3_6 979 # ASSIGN : s_3_7 1061 # ASSIGN : s_3_8 1232 # ASSIGN : s_3_9 1286 # ASSIGN : s_4_0 76 # ASSIGN : s_4_1 116 # ASSIGN : s_4_2 187 # ASSIGN : s_4_3 278 # ASSIGN : s_4_4 285 # ASSIGN : s_4_5 367 # ASSIGN : s_4_6 1099 # ASSIGN : s_4_7 1149 # ASSIGN : s_4_8 1247 # ASSIGN : s_4_9 1264 # ASSIGN : s_5_0 143 # ASSIGN : s_5_1 275 # ASSIGN : s_5_2 506 # ASSIGN : s_5_3 638 # ASSIGN : s_5_4 806 # ASSIGN : s_5_5 860 # ASSIGN : s_5_6 956 # ASSIGN : s_5_7 972 # ASSIGN : s_5_8 1149 # ASSIGN : s_5_9 1216 # ASSIGN : s_6_0 217 # ASSIGN : s_6_1 513 # ASSIGN : s_6_2 754 # ASSIGN : s_6_3 853 # ASSIGN : s_6_4 881 # ASSIGN : s_6_5 979 # ASSIGN : s_6_6 1049 # ASSIGN : s_6_7 1136 # ASSIGN : s_6_8 1280 # ASSIGN : s_6_9 1416 # ASSIGN : s_7_0 36 # ASSIGN : s_7_1 131 # ASSIGN : s_7_2 331 # ASSIGN : s_7_3 498 # ASSIGN : s_7_4 608 # ASSIGN : s_7_5 710 # ASSIGN : s_7_6 751 # ASSIGN : s_7_7 964 # ASSIGN : s_7_8 1104 # ASSIGN : s_7_9 1324 # ASSIGN : s_8_0 144 # ASSIGN : s_8_1 399 # ASSIGN : s_8_2 550 # ASSIGN : s_8_3 647 # ASSIGN : s_8_4 950 # ASSIGN : s_8_5 989 # ASSIGN : s_8_6 1229 # ASSIGN : s_8_7 1274 # ASSIGN : s_8_8 1382 # ASSIGN : s_8_9 1431 # ASSIGN : s_9_0 22 # ASSIGN : s_9_1 55 # ASSIGN : s_9_2 162 # ASSIGN : s_9_3 206 # ASSIGN : s_9_4 232 # ASSIGN : s_9_5 316 # ASSIGN : s_9_6 398 # ASSIGN : s_9_7 466 # ASSIGN : s_9_8 487 # ASSIGN : s_9_9 707 # ASSIGN : s_10_0 72 # ASSIGN : s_10_1 115 # ASSIGN : s_10_2 203 # ASSIGN : s_10_3 233 # ASSIGN : s_10_4 344 # ASSIGN : s_10_5 555 # ASSIGN : s_10_6 969 # ASSIGN : s_10_7 1008 # ASSIGN : s_10_8 1334 # ASSIGN : s_10_9 1353 # ASSIGN : s_11_0 175 # ASSIGN : s_11_1 194 # ASSIGN : s_11_2 261 # ASSIGN : s_11_3 334 # ASSIGN : s_11_4 419 # ASSIGN : s_11_5 878 # ASSIGN : s_11_6 917 # ASSIGN : s_11_7 1113 # ASSIGN : s_11_8 1136 # ASSIGN : s_11_9 1400 # ASSIGN : s_12_0 0 # ASSIGN : s_12_1 80 # ASSIGN : s_12_2 126 # ASSIGN : s_12_3 216 # ASSIGN : s_12_4 334 # ASSIGN : s_12_5 395 # ASSIGN : s_12_6 445 # ASSIGN : s_12_7 505 # ASSIGN : s_12_8 1322 # ASSIGN : s_12_9 1377 # ASSIGN : s_13_0 104 # ASSIGN : s_13_1 375 # ASSIGN : s_13_2 558 # ASSIGN : s_13_3 848 # ASSIGN : s_13_4 926 # ASSIGN : s_13_5 1003 # ASSIGN : s_13_6 1203 # ASSIGN : s_13_7 1275 # ASSIGN : s_13_8 1302 # ASSIGN : s_13_9 1375 # ASSIGN : s_14_0 569 # ASSIGN : s_14_1 667 # ASSIGN : s_14_2 710 # ASSIGN : s_14_3 722 # ASSIGN : s_14_4 762 # ASSIGN : s_14_5 832 # ASSIGN : s_14_6 906 # ASSIGN : s_14_7 940 # ASSIGN : s_14_8 947 # ASSIGN : s_14_9 977 # ASSIGN : s_15_0 179 # ASSIGN : s_15_1 309 # ASSIGN : s_15_2 336 # ASSIGN : s_15_3 416 # ASSIGN : s_15_4 488 # ASSIGN : s_15_5 514 # ASSIGN : s_15_6 559 # ASSIGN : s_15_7 638 # ASSIGN : s_15_8 1178 # ASSIGN : s_15_9 1383 # ASSIGN : s_16_0 300 # ASSIGN : s_16_1 380 # ASSIGN : s_16_2 397 # ASSIGN : s_16_3 549 # ASSIGN : s_16_4 599 # ASSIGN : s_16_5 664 # ASSIGN : s_16_6 701 # ASSIGN : s_16_7 1059 # ASSIGN : s_16_8 1185 # ASSIGN : s_16_9 1256 # ASSIGN : s_17_0 799 # ASSIGN : s_17_1 872 # ASSIGN : s_17_2 884 # ASSIGN : s_17_3 915 # ASSIGN : s_17_4 964 # ASSIGN : s_17_5 1055 # ASSIGN : s_17_6 1117 # ASSIGN : s_17_7 1235 # ASSIGN : s_17_8 1307 # ASSIGN : s_17_9 1405 # ASSIGN : s_18_0 236 # ASSIGN : s_18_1 271 # ASSIGN : s_18_2 387 # ASSIGN : s_18_3 412 # ASSIGN : s_18_4 447 # ASSIGN : s_18_5 468 # ASSIGN : s_18_6 515 # ASSIGN : s_18_7 636 # ASSIGN : s_18_8 814 # ASSIGN : s_18_9 871 # ASSIGN : s_19_0 838 # ASSIGN : s_19_1 916 # ASSIGN : s_19_2 945 # ASSIGN : s_19_3 1003 # ASSIGN : s_19_4 1077 # ASSIGN : s_19_5 1082 # ASSIGN : s_19_6 1157 # ASSIGN : s_19_7 1207 # ASSIGN : s_19_8 1264 # ASSIGN : s_19_9 1352 SHOW_RESULT 1443 END : 1443 (0 seconds) [Thu Jun 1 20:21:04 2006] SHOW_RESULT 1443 CPU : 0.949999999999998 = 0.939999999999998 + 0.01 + 0 + 0 # BOUND : makespan 1216 1443 MODIFY_CNF 1329 BEGIN : [Thu Jun 1 20:21:04 2006] MODIFY_CNF 1329 END : 162515799 bytes (0 seconds) [Thu Jun 1 20:21:04 2006] MODIFY_CNF 1329 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1329 BEGIN : [Thu Jun 1 20:21:04 2006] CMD : minisat /work/tamura/csp2sat70812.cnf /work/tamura/csp2sat70812.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 3656931 10809442 | 1218977 0 0 NaNQ | 0.000 % | | 100 | 3656931 10809442 | 1340874 100 1929 19.3 | 51.930 % | | 250 | 3656931 10809442 | 1474962 250 4269 17.1 | 51.930 % | | 477 | 3656931 10809442 | 1622458 477 7574 15.9 | 51.930 % | | 814 | 3656931 10809442 | 1784704 814 18785 23.1 | 51.930 % | | 1320 | 3656931 10809442 | 1963174 1320 28843 21.9 | 51.930 % | ==============================================================================) restarts : 6 conflicts : 1419 (74 /sec) decisions : 3117 (163 /sec) propagations : 11580671 (604172 /sec) inspects : 164360120 (8574786 /sec) conflict literals : 31495 (14.27 % deleted) CPU time : 19.1678 s SATISFIABLE VERIFY_CNF 1329 END : (22 seconds) [Thu Jun 1 20:21:26 2006] VERIFY_CNF 1329 CPU : 21.83 = 0 + 0.02 + 21.17 + 0.64 # RESULT : makespan 1329 SATISFIABLE SHOW_RESULT 1329 BEGIN : [Thu Jun 1 20:21:26 2006] # ASSIGN : makespan 1329 # ASSIGN : s_0_0 75 # ASSIGN : s_0_1 107 # ASSIGN : s_0_2 244 # ASSIGN : s_0_3 370 # ASSIGN : s_0_4 410 # ASSIGN : s_0_5 453 # ASSIGN : s_0_6 491 # ASSIGN : s_0_7 1192 # ASSIGN : s_0_8 1239 # ASSIGN : s_0_9 1305 # ASSIGN : s_1_0 641 # ASSIGN : s_1_1 711 # ASSIGN : s_1_2 889 # ASSIGN : s_1_3 910 # ASSIGN : s_1_4 974 # ASSIGN : s_1_5 1031 # ASSIGN : s_1_6 1070 # ASSIGN : s_1_7 1172 # ASSIGN : s_1_8 1249 # ASSIGN : s_1_9 1314 # ASSIGN : s_2_0 286 # ASSIGN : s_2_1 551 # ASSIGN : s_2_2 640 # ASSIGN : s_2_3 664 # ASSIGN : s_2_4 829 # ASSIGN : s_2_5 914 # ASSIGN : s_2_6 945 # ASSIGN : s_2_7 984 # ASSIGN : s_2_8 1212 # ASSIGN : s_2_9 1289 # ASSIGN : s_3_0 6 # ASSIGN : s_3_1 104 # ASSIGN : s_3_2 163 # ASSIGN : s_3_3 175 # ASSIGN : s_3_4 281 # ASSIGN : s_3_5 358 # ASSIGN : s_3_6 436 # ASSIGN : s_3_7 516 # ASSIGN : s_3_8 572 # ASSIGN : s_3_9 1172 # ASSIGN : s_4_0 241 # ASSIGN : s_4_1 294 # ASSIGN : s_4_2 615 # ASSIGN : s_4_3 706 # ASSIGN : s_4_4 713 # ASSIGN : s_4_5 772 # ASSIGN : s_4_6 914 # ASSIGN : s_4_7 964 # ASSIGN : s_4_8 1020 # ASSIGN : s_4_9 1096 # ASSIGN : s_5_0 250 # ASSIGN : s_5_1 296 # ASSIGN : s_5_2 306 # ASSIGN : s_5_3 379 # ASSIGN : s_5_4 388 # ASSIGN : s_5_5 471 # ASSIGN : s_5_6 567 # ASSIGN : s_5_7 700 # ASSIGN : s_5_8 777 # ASSIGN : s_5_9 1074 # ASSIGN : s_6_0 142 # ASSIGN : s_6_1 310 # ASSIGN : s_6_2 396 # ASSIGN : s_6_3 488 # ASSIGN : s_6_4 516 # ASSIGN : s_6_5 712 # ASSIGN : s_6_6 817 # ASSIGN : s_6_7 974 # ASSIGN : s_6_8 1137 # ASSIGN : s_6_9 1210 # ASSIGN : s_7_0 5 # ASSIGN : s_7_1 129 # ASSIGN : s_7_2 243 # ASSIGN : s_7_3 299 # ASSIGN : s_7_4 351 # ASSIGN : s_7_5 435 # ASSIGN : s_7_6 489 # ASSIGN : s_7_7 574 # ASSIGN : s_7_8 613 # ASSIGN : s_7_9 1237 # ASSIGN : s_8_0 100 # ASSIGN : s_8_1 447 # ASSIGN : s_8_2 782 # ASSIGN : s_8_3 875 # ASSIGN : s_8_4 904 # ASSIGN : s_8_5 926 # ASSIGN : s_8_6 1087 # ASSIGN : s_8_7 1132 # ASSIGN : s_8_8 1206 # ASSIGN : s_8_9 1279 # ASSIGN : s_9_0 172 # ASSIGN : s_9_1 205 # ASSIGN : s_9_2 266 # ASSIGN : s_9_3 326 # ASSIGN : s_9_4 352 # ASSIGN : s_9_5 902 # ASSIGN : s_9_6 1006 # ASSIGN : s_9_7 1089 # ASSIGN : s_9_8 1135 # ASSIGN : s_9_9 1230 # ASSIGN : s_10_0 183 # ASSIGN : s_10_1 416 # ASSIGN : s_10_2 510 # ASSIGN : s_10_3 540 # ASSIGN : s_10_4 772 # ASSIGN : s_10_5 1164 # ASSIGN : s_10_6 1190 # ASSIGN : s_10_7 1198 # ASSIGN : s_10_8 1272 # ASSIGN : s_10_9 1291 # ASSIGN : s_11_0 21 # ASSIGN : s_11_1 40 # ASSIGN : s_11_2 110 # ASSIGN : s_11_3 188 # ASSIGN : s_11_4 412 # ASSIGN : s_11_5 1057 # ASSIGN : s_11_6 1140 # ASSIGN : s_11_7 1149 # ASSIGN : s_11_8 1199 # ASSIGN : s_11_9 1229 # ASSIGN : s_12_0 3 # ASSIGN : s_12_1 117 # ASSIGN : s_12_2 163 # ASSIGN : s_12_3 248 # ASSIGN : s_12_4 365 # ASSIGN : s_12_5 442 # ASSIGN : s_12_6 449 # ASSIGN : s_12_7 614 # ASSIGN : s_12_8 763 # ASSIGN : s_12_9 818 # ASSIGN : s_13_0 86 # ASSIGN : s_13_1 215 # ASSIGN : s_13_2 438 # ASSIGN : s_13_3 472 # ASSIGN : s_13_4 775 # ASSIGN : s_13_5 818 # ASSIGN : s_13_6 984 # ASSIGN : s_13_7 1056 # ASSIGN : s_13_8 1067 # ASSIGN : s_13_9 1261 # ASSIGN : s_14_0 102 # ASSIGN : s_14_1 171 # ASSIGN : s_14_2 214 # ASSIGN : s_14_3 226 # ASSIGN : s_14_4 273 # ASSIGN : s_14_5 744 # ASSIGN : s_14_6 923 # ASSIGN : s_14_7 957 # ASSIGN : s_14_8 974 # ASSIGN : s_14_9 1056 # ASSIGN : s_15_0 3 # ASSIGN : s_15_1 102 # ASSIGN : s_15_2 185 # ASSIGN : s_15_3 354 # ASSIGN : s_15_4 426 # ASSIGN : s_15_5 444 # ASSIGN : s_15_6 566 # ASSIGN : s_15_7 645 # ASSIGN : s_15_8 708 # ASSIGN : s_15_9 1269 # ASSIGN : s_16_0 88 # ASSIGN : s_16_1 341 # ASSIGN : s_16_2 476 # ASSIGN : s_16_3 583 # ASSIGN : s_16_4 633 # ASSIGN : s_16_5 780 # ASSIGN : s_16_6 847 # ASSIGN : s_16_7 1037 # ASSIGN : s_16_8 1127 # ASSIGN : s_16_9 1222 # ASSIGN : s_17_0 224 # ASSIGN : s_17_1 343 # ASSIGN : s_17_2 559 # ASSIGN : s_17_3 614 # ASSIGN : s_17_4 738 # ASSIGN : s_17_5 852 # ASSIGN : s_17_6 924 # ASSIGN : s_17_7 1014 # ASSIGN : s_17_8 1086 # ASSIGN : s_17_9 1184 # ASSIGN : s_18_0 475 # ASSIGN : s_18_1 575 # ASSIGN : s_18_2 638 # ASSIGN : s_18_3 663 # ASSIGN : s_18_4 698 # ASSIGN : s_18_5 719 # ASSIGN : s_18_6 766 # ASSIGN : s_18_7 894 # ASSIGN : s_18_8 1110 # ASSIGN : s_18_9 1255 # ASSIGN : s_19_0 107 # ASSIGN : s_19_1 302 # ASSIGN : s_19_2 354 # ASSIGN : s_19_3 419 # ASSIGN : s_19_4 561 # ASSIGN : s_19_5 570 # ASSIGN : s_19_6 590 # ASSIGN : s_19_7 649 # ASSIGN : s_19_8 806 # ASSIGN : s_19_9 1004 SHOW_RESULT 1329 END : 1329 (1 seconds) [Thu Jun 1 20:21:27 2006] SHOW_RESULT 1329 CPU : 0.930000000000016 = 0.920000000000016 + 0.01 + 0 + 0 # BOUND : makespan 1216 1329 MODIFY_CNF 1272 BEGIN : [Thu Jun 1 20:21:27 2006] MODIFY_CNF 1272 END : 162515798 bytes (0 seconds) [Thu Jun 1 20:21:27 2006] MODIFY_CNF 1272 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1272 BEGIN : [Thu Jun 1 20:21:27 2006] CMD : minisat /work/tamura/csp2sat70812.cnf /work/tamura/csp2sat70812.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 3422951 10118969 | 1140983 0 0 NaNQ | 0.000 % | | 100 | 3422951 10118969 | 1255081 100 1273 12.7 | 55.314 % | | 250 | 3422951 10118969 | 1380589 250 3403 13.6 | 55.314 % | | 475 | 3422951 10118969 | 1518648 475 6223 13.1 | 55.314 % | | 812 | 3422951 10118969 | 1670513 812 18537 22.8 | 55.314 % | | 1318 | 3422951 10118969 | 1837564 1318 28511 21.6 | 55.314 % | | 2077 | 3422951 10118969 | 2021320 2077 44256 21.3 | 55.314 % | | 3216 | 3422951 10118969 | 2223453 3216 90655 28.2 | 55.314 % | | 4924 | 3422951 10118969 | 2445798 4924 153252 31.1 | 55.314 % | | 7486 | 3422951 10118969 | 2690378 7486 218890 29.2 | 55.314 % | ==============================================================================) restarts : 10 conflicts : 10465 (123 /sec) decisions : 17703 (207 /sec) propagations : 83224019 (975109 /sec) inspects : 1226094731 (14365757 /sec) conflict literals : 384965 (18.73 % deleted) CPU time : 85.3484 s SATISFIABLE VERIFY_CNF 1272 END : (88 seconds) [Thu Jun 1 20:22:55 2006] VERIFY_CNF 1272 CPU : 87.52 = 0.00999999999999091 + 0.02 + 87.32 + 0.17 # RESULT : makespan 1272 SATISFIABLE SHOW_RESULT 1272 BEGIN : [Thu Jun 1 20:22:55 2006] # ASSIGN : makespan 1272 # ASSIGN : s_0_0 2 # ASSIGN : s_0_1 34 # ASSIGN : s_0_2 115 # ASSIGN : s_0_3 203 # ASSIGN : s_0_4 245 # ASSIGN : s_0_5 252 # ASSIGN : s_0_6 305 # ASSIGN : s_0_7 1003 # ASSIGN : s_0_8 1040 # ASSIGN : s_0_9 1132 # ASSIGN : s_1_0 258 # ASSIGN : s_1_1 458 # ASSIGN : s_1_2 556 # ASSIGN : s_1_3 588 # ASSIGN : s_1_4 652 # ASSIGN : s_1_5 698 # ASSIGN : s_1_6 723 # ASSIGN : s_1_7 788 # ASSIGN : s_1_8 898 # ASSIGN : s_1_9 963 # ASSIGN : s_2_0 83 # ASSIGN : s_2_1 170 # ASSIGN : s_2_2 791 # ASSIGN : s_2_3 815 # ASSIGN : s_2_4 859 # ASSIGN : s_2_5 952 # ASSIGN : s_2_6 983 # ASSIGN : s_2_7 1049 # ASSIGN : s_2_8 1195 # ASSIGN : s_2_9 1232 # ASSIGN : s_3_0 3 # ASSIGN : s_3_1 83 # ASSIGN : s_3_2 142 # ASSIGN : s_3_3 150 # ASSIGN : s_3_4 200 # ASSIGN : s_3_5 277 # ASSIGN : s_3_6 389 # ASSIGN : s_3_7 500 # ASSIGN : s_3_8 611 # ASSIGN : s_3_9 1115 # ASSIGN : s_4_0 140 # ASSIGN : s_4_1 180 # ASSIGN : s_4_2 251 # ASSIGN : s_4_3 342 # ASSIGN : s_4_4 386 # ASSIGN : s_4_5 551 # ASSIGN : s_4_6 641 # ASSIGN : s_4_7 733 # ASSIGN : s_4_8 869 # ASSIGN : s_4_9 1138 # ASSIGN : s_5_0 167 # ASSIGN : s_5_1 295 # ASSIGN : s_5_2 379 # ASSIGN : s_5_3 472 # ASSIGN : s_5_4 482 # ASSIGN : s_5_5 741 # ASSIGN : s_5_6 1012 # ASSIGN : s_5_7 1020 # ASSIGN : s_5_8 1106 # ASSIGN : s_5_9 1157 # ASSIGN : s_6_0 0 # ASSIGN : s_6_1 99 # ASSIGN : s_6_2 185 # ASSIGN : s_6_3 526 # ASSIGN : s_6_4 554 # ASSIGN : s_6_5 686 # ASSIGN : s_6_6 789 # ASSIGN : s_6_7 887 # ASSIGN : s_6_8 1080 # ASSIGN : s_6_9 1153 # ASSIGN : s_7_0 124 # ASSIGN : s_7_1 373 # ASSIGN : s_7_2 475 # ASSIGN : s_7_3 536 # ASSIGN : s_7_4 668 # ASSIGN : s_7_5 727 # ASSIGN : s_7_6 768 # ASSIGN : s_7_7 1076 # ASSIGN : s_7_8 1117 # ASSIGN : s_7_9 1180 # ASSIGN : s_8_0 228 # ASSIGN : s_8_1 431 # ASSIGN : s_8_2 756 # ASSIGN : s_8_3 849 # ASSIGN : s_8_4 876 # ASSIGN : s_8_5 937 # ASSIGN : s_8_6 1031 # ASSIGN : s_8_7 1089 # ASSIGN : s_8_8 1149 # ASSIGN : s_8_9 1222 # ASSIGN : s_9_0 50 # ASSIGN : s_9_1 89 # ASSIGN : s_9_2 227 # ASSIGN : s_9_3 271 # ASSIGN : s_9_4 305 # ASSIGN : s_9_5 481 # ASSIGN : s_9_6 563 # ASSIGN : s_9_7 631 # ASSIGN : s_9_8 652 # ASSIGN : s_9_9 1039 # ASSIGN : s_10_0 56 # ASSIGN : s_10_1 173 # ASSIGN : s_10_2 259 # ASSIGN : s_10_3 297 # ASSIGN : s_10_4 445 # ASSIGN : s_10_5 701 # ASSIGN : s_10_6 1133 # ASSIGN : s_10_7 1141 # ASSIGN : s_10_8 1215 # ASSIGN : s_10_9 1234 # ASSIGN : s_11_0 309 # ASSIGN : s_11_1 328 # ASSIGN : s_11_2 396 # ASSIGN : s_11_3 469 # ASSIGN : s_11_4 585 # ASSIGN : s_11_5 866 # ASSIGN : s_11_6 905 # ASSIGN : s_11_7 914 # ASSIGN : s_11_8 1007 # ASSIGN : s_11_9 1046 # ASSIGN : s_12_0 272 # ASSIGN : s_12_1 349 # ASSIGN : s_12_2 395 # ASSIGN : s_12_3 831 # ASSIGN : s_12_4 944 # ASSIGN : s_12_5 1005 # ASSIGN : s_12_6 1012 # ASSIGN : s_12_7 1056 # ASSIGN : s_12_8 1160 # ASSIGN : s_12_9 1215 # ASSIGN : s_13_0 324 # ASSIGN : s_13_1 429 # ASSIGN : s_13_2 520 # ASSIGN : s_13_3 531 # ASSIGN : s_13_4 627 # ASSIGN : s_13_5 691 # ASSIGN : s_13_6 787 # ASSIGN : s_13_7 862 # ASSIGN : s_13_8 903 # ASSIGN : s_13_9 1204 # ASSIGN : s_14_0 30 # ASSIGN : s_14_1 99 # ASSIGN : s_14_2 156 # ASSIGN : s_14_3 187 # ASSIGN : s_14_4 235 # ASSIGN : s_14_5 614 # ASSIGN : s_14_6 693 # ASSIGN : s_14_7 968 # ASSIGN : s_14_8 975 # ASSIGN : s_14_9 1049 # ASSIGN : s_15_0 243 # ASSIGN : s_15_1 346 # ASSIGN : s_15_2 423 # ASSIGN : s_15_3 599 # ASSIGN : s_15_4 679 # ASSIGN : s_15_5 688 # ASSIGN : s_15_6 865 # ASSIGN : s_15_7 1054 # ASSIGN : s_15_8 1135 # ASSIGN : s_15_9 1212 # ASSIGN : s_16_0 24 # ASSIGN : s_16_1 168 # ASSIGN : s_16_2 486 # ASSIGN : s_16_3 577 # ASSIGN : s_16_4 631 # ASSIGN : s_16_5 696 # ASSIGN : s_16_6 788 # ASSIGN : s_16_7 886 # ASSIGN : s_16_8 978 # ASSIGN : s_16_9 1226 # ASSIGN : s_17_0 147 # ASSIGN : s_17_1 219 # ASSIGN : s_17_2 315 # ASSIGN : s_17_3 346 # ASSIGN : s_17_4 395 # ASSIGN : s_17_5 873 # ASSIGN : s_17_6 935 # ASSIGN : s_17_7 1025 # ASSIGN : s_17_8 1097 # ASSIGN : s_17_9 1234 # ASSIGN : s_18_0 289 # ASSIGN : s_18_1 608 # ASSIGN : s_18_2 671 # ASSIGN : s_18_3 733 # ASSIGN : s_18_4 837 # ASSIGN : s_18_5 858 # ASSIGN : s_18_6 924 # ASSIGN : s_18_7 976 # ASSIGN : s_18_8 1121 # ASSIGN : s_18_9 1198 # ASSIGN : s_19_0 21 # ASSIGN : s_19_1 213 # ASSIGN : s_19_2 237 # ASSIGN : s_19_3 344 # ASSIGN : s_19_4 424 # ASSIGN : s_19_5 452 # ASSIGN : s_19_6 513 # ASSIGN : s_19_7 670 # ASSIGN : s_19_8 727 # ASSIGN : s_19_9 922 SHOW_RESULT 1272 END : 1272 (1 seconds) [Thu Jun 1 20:22:56 2006] SHOW_RESULT 1272 CPU : 0.949999999999998 = 0.939999999999998 + 0.0099999999999999 + 0 + 0 # BOUND : makespan 1216 1272 MODIFY_CNF 1244 BEGIN : [Thu Jun 1 20:22:56 2006] MODIFY_CNF 1244 END : 162515798 bytes (0 seconds) [Thu Jun 1 20:22:56 2006] MODIFY_CNF 1244 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1244 BEGIN : [Thu Jun 1 20:22:56 2006] CMD : minisat /work/tamura/csp2sat70812.cnf /work/tamura/csp2sat70812.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 3305324 9771725 | 1101774 0 0 NaNQ | 0.000 % | | 100 | 3305324 9771725 | 1211951 100 1308 13.1 | 56.978 % | | 250 | 3305324 9771725 | 1333146 250 3257 13.0 | 56.978 % | | 475 | 3305324 9771725 | 1466461 475 6769 14.3 | 56.978 % | | 812 | 3305324 9771725 | 1613107 812 15393 19.0 | 56.978 % | | 1318 | 3305324 9771725 | 1774418 1318 20968 15.9 | 56.978 % | | 2077 | 3305324 9771725 | 1951859 2077 31116 15.0 | 56.978 % | | 3216 | 3305324 9771725 | 2147045 3216 50679 15.8 | 56.978 % | | 4924 | 3305324 9771725 | 2361750 4924 97608 19.8 | 56.978 % | | 7486 | 3305324 9771725 | 2597925 7486 190004 25.4 | 56.978 % | | 11331 | 3305324 9771725 | 2857718 11331 278079 24.5 | 56.978 % | | 17097 | 3305324 9771725 | 3143489 17097 468512 27.4 | 56.978 % | | 25746 | 3305324 9771725 | 3457838 25746 926752 36.0 | 56.978 % | ==============================================================================) restarts : 13 conflicts : 27774 (141 /sec) decisions : 42357 (214 /sec) propagations : 207272992 (1049016 /sec) inspects : 2950939866 (14934813 /sec) conflict literals : 1005167 (20.78 % deleted) CPU time : 197.588 s SATISFIABLE VERIFY_CNF 1244 END : (201 seconds) [Thu Jun 1 20:26:17 2006] VERIFY_CNF 1244 CPU : 199.66 = 0 + 0.02 + 199.47 + 0.17 # RESULT : makespan 1244 SATISFIABLE SHOW_RESULT 1244 BEGIN : [Thu Jun 1 20:26:17 2006] # ASSIGN : makespan 1244 # ASSIGN : s_0_0 44 # ASSIGN : s_0_1 123 # ASSIGN : s_0_2 298 # ASSIGN : s_0_3 353 # ASSIGN : s_0_4 393 # ASSIGN : s_0_5 424 # ASSIGN : s_0_6 445 # ASSIGN : s_0_7 846 # ASSIGN : s_0_8 989 # ASSIGN : s_0_9 1103 # ASSIGN : s_1_0 557 # ASSIGN : s_1_1 627 # ASSIGN : s_1_2 682 # ASSIGN : s_1_3 703 # ASSIGN : s_1_4 787 # ASSIGN : s_1_5 895 # ASSIGN : s_1_6 965 # ASSIGN : s_1_7 1030 # ASSIGN : s_1_8 1107 # ASSIGN : s_1_9 1172 # ASSIGN : s_2_0 1 # ASSIGN : s_2_1 85 # ASSIGN : s_2_2 180 # ASSIGN : s_2_3 204 # ASSIGN : s_2_4 248 # ASSIGN : s_2_5 385 # ASSIGN : s_2_6 416 # ASSIGN : s_2_7 539 # ASSIGN : s_2_8 909 # ASSIGN : s_2_9 1204 # ASSIGN : s_3_0 0 # ASSIGN : s_3_1 80 # ASSIGN : s_3_2 139 # ASSIGN : s_3_3 147 # ASSIGN : s_3_4 192 # ASSIGN : s_3_5 269 # ASSIGN : s_3_6 348 # ASSIGN : s_3_7 470 # ASSIGN : s_3_8 526 # ASSIGN : s_3_9 920 # ASSIGN : s_4_0 21 # ASSIGN : s_4_1 177 # ASSIGN : s_4_2 427 # ASSIGN : s_4_3 583 # ASSIGN : s_4_4 630 # ASSIGN : s_4_5 803 # ASSIGN : s_4_6 883 # ASSIGN : s_4_7 1051 # ASSIGN : s_4_8 1130 # ASSIGN : s_4_9 1156 # ASSIGN : s_5_0 211 # ASSIGN : s_5_1 247 # ASSIGN : s_5_2 268 # ASSIGN : s_5_3 464 # ASSIGN : s_5_4 481 # ASSIGN : s_5_5 544 # ASSIGN : s_5_6 734 # ASSIGN : s_5_7 742 # ASSIGN : s_5_8 1147 # ASSIGN : s_5_9 1186 # ASSIGN : s_6_0 93 # ASSIGN : s_6_1 221 # ASSIGN : s_6_2 307 # ASSIGN : s_6_3 399 # ASSIGN : s_6_4 428 # ASSIGN : s_6_5 535 # ASSIGN : s_6_6 605 # ASSIGN : s_6_7 700 # ASSIGN : s_6_8 1144 # ASSIGN : s_6_9 1217 # ASSIGN : s_7_0 0 # ASSIGN : s_7_1 95 # ASSIGN : s_7_2 549 # ASSIGN : s_7_3 651 # ASSIGN : s_7_4 790 # ASSIGN : s_7_5 871 # ASSIGN : s_7_6 936 # ASSIGN : s_7_7 1017 # ASSIGN : s_7_8 1077 # ASSIGN : s_7_9 1125 # ASSIGN : s_8_0 256 # ASSIGN : s_8_1 284 # ASSIGN : s_8_2 767 # ASSIGN : s_8_3 860 # ASSIGN : s_8_4 887 # ASSIGN : s_8_5 942 # ASSIGN : s_8_6 1056 # ASSIGN : s_8_7 1123 # ASSIGN : s_8_8 1183 # ASSIGN : s_8_9 1232 # ASSIGN : s_9_0 251 # ASSIGN : s_9_1 396 # ASSIGN : s_9_2 479 # ASSIGN : s_9_3 523 # ASSIGN : s_9_4 552 # ASSIGN : s_9_5 696 # ASSIGN : s_9_6 778 # ASSIGN : s_9_7 849 # ASSIGN : s_9_8 894 # ASSIGN : s_9_9 1011 # ASSIGN : s_10_0 1 # ASSIGN : s_10_1 67 # ASSIGN : s_10_2 174 # ASSIGN : s_10_3 217 # ASSIGN : s_10_4 315 # ASSIGN : s_10_5 526 # ASSIGN : s_10_6 575 # ASSIGN : s_10_7 622 # ASSIGN : s_10_8 1061 # ASSIGN : s_10_9 1106 # ASSIGN : s_11_0 61 # ASSIGN : s_11_1 80 # ASSIGN : s_11_2 148 # ASSIGN : s_11_3 263 # ASSIGN : s_11_4 390 # ASSIGN : s_11_5 612 # ASSIGN : s_11_6 660 # ASSIGN : s_11_7 669 # ASSIGN : s_11_8 692 # ASSIGN : s_11_9 1080 # ASSIGN : s_12_0 76 # ASSIGN : s_12_1 397 # ASSIGN : s_12_2 443 # ASSIGN : s_12_3 685 # ASSIGN : s_12_4 810 # ASSIGN : s_12_5 974 # ASSIGN : s_12_6 1035 # ASSIGN : s_12_7 1080 # ASSIGN : s_12_8 1132 # ASSIGN : s_12_9 1187 # ASSIGN : s_13_0 382 # ASSIGN : s_13_1 578 # ASSIGN : s_13_2 689 # ASSIGN : s_13_3 819 # ASSIGN : s_13_4 890 # ASSIGN : s_13_5 933 # ASSIGN : s_13_6 1029 # ASSIGN : s_13_7 1101 # ASSIGN : s_13_8 1112 # ASSIGN : s_13_9 1176 # ASSIGN : s_14_0 156 # ASSIGN : s_14_1 225 # ASSIGN : s_14_2 406 # ASSIGN : s_14_3 418 # ASSIGN : s_14_4 716 # ASSIGN : s_14_5 786 # ASSIGN : s_14_6 912 # ASSIGN : s_14_7 946 # ASSIGN : s_14_8 981 # ASSIGN : s_14_9 1041 # ASSIGN : s_15_0 112 # ASSIGN : s_15_1 211 # ASSIGN : s_15_2 239 # ASSIGN : s_15_3 326 # ASSIGN : s_15_4 457 # ASSIGN : s_15_5 473 # ASSIGN : s_15_6 518 # ASSIGN : s_15_7 567 # ASSIGN : s_15_8 1011 # ASSIGN : s_15_9 1184 # ASSIGN : s_16_0 313 # ASSIGN : s_16_1 449 # ASSIGN : s_16_2 466 # ASSIGN : s_16_3 590 # ASSIGN : s_16_4 640 # ASSIGN : s_16_5 705 # ASSIGN : s_16_6 796 # ASSIGN : s_16_7 921 # ASSIGN : s_16_8 1032 # ASSIGN : s_16_9 1110 # ASSIGN : s_17_0 42 # ASSIGN : s_17_1 114 # ASSIGN : s_17_2 238 # ASSIGN : s_17_3 354 # ASSIGN : s_17_4 627 # ASSIGN : s_17_5 718 # ASSIGN : s_17_6 780 # ASSIGN : s_17_7 870 # ASSIGN : s_17_8 953 # ASSIGN : s_17_9 1118 # ASSIGN : s_18_0 204 # ASSIGN : s_18_1 333 # ASSIGN : s_18_2 398 # ASSIGN : s_18_3 423 # ASSIGN : s_18_4 458 # ASSIGN : s_18_5 528 # ASSIGN : s_18_6 575 # ASSIGN : s_18_7 636 # ASSIGN : s_18_8 751 # ASSIGN : s_18_9 1109 # ASSIGN : s_19_0 12 # ASSIGN : s_19_1 193 # ASSIGN : s_19_2 257 # ASSIGN : s_19_3 333 # ASSIGN : s_19_4 388 # ASSIGN : s_19_5 403 # ASSIGN : s_19_6 525 # ASSIGN : s_19_7 723 # ASSIGN : s_19_8 833 # ASSIGN : s_19_9 921 SHOW_RESULT 1244 END : 1244 (1 seconds) [Thu Jun 1 20:26:18 2006] SHOW_RESULT 1244 CPU : 0.96999999999998 = 0.95999999999998 + 0.01 + 0 + 0 # BOUND : makespan 1216 1244 MODIFY_CNF 1230 BEGIN : [Thu Jun 1 20:26:18 2006] MODIFY_CNF 1230 END : 162515798 bytes (0 seconds) [Thu Jun 1 20:26:18 2006] MODIFY_CNF 1230 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1230 BEGIN : [Thu Jun 1 20:26:18 2006] CMD : minisat /work/tamura/csp2sat70812.cnf /work/tamura/csp2sat70812.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 3246056 9596740 | 1082018 0 0 NaNQ | 0.000 % | | 101 | 3246056 9596740 | 1190219 101 1906 18.9 | 57.810 % | | 252 | 3246056 9596740 | 1309241 252 4579 18.2 | 57.810 % | | 479 | 3246056 9596740 | 1440165 479 9947 20.8 | 57.810 % | | 816 | 3246056 9596740 | 1584182 816 15686 19.2 | 57.810 % | | 1323 | 3246056 9596740 | 1742600 1323 27674 20.9 | 57.810 % | | 2083 | 3246056 9596740 | 1916860 2083 41239 19.8 | 57.810 % | | 3222 | 3246056 9596740 | 2108546 3222 57396 17.8 | 57.810 % | | 4930 | 3246056 9596740 | 2319401 4930 115466 23.4 | 57.810 % | | 7492 | 3246056 9596740 | 2551341 7492 189174 25.3 | 57.810 % | | 11336 | 3246056 9596740 | 2806476 11336 301985 26.6 | 57.810 % | | 17102 | 3246056 9596740 | 3087123 17102 453184 26.5 | 57.810 % | | 25752 | 3246056 9596740 | 3395835 25752 676459 26.3 | 57.810 % | ==============================================================================) restarts : 13 conflicts : 31135 (123 /sec) decisions : 48729 (192 /sec) propagations : 262782784 (1037560 /sec) inspects : 3540717535 (13980020 /sec) conflict literals : 833303 (28.18 % deleted) CPU time : 253.27 s SATISFIABLE VERIFY_CNF 1230 END : (256 seconds) [Thu Jun 1 20:30:34 2006] VERIFY_CNF 1230 CPU : 255.85 = 0 + 0.02 + 255.21 + 0.62 # RESULT : makespan 1230 SATISFIABLE SHOW_RESULT 1230 BEGIN : [Thu Jun 1 20:30:34 2006] # ASSIGN : makespan 1230 # ASSIGN : s_0_0 8 # ASSIGN : s_0_1 120 # ASSIGN : s_0_2 277 # ASSIGN : s_0_3 332 # ASSIGN : s_0_4 372 # ASSIGN : s_0_5 385 # ASSIGN : s_0_6 404 # ASSIGN : s_0_7 832 # ASSIGN : s_0_8 1124 # ASSIGN : s_0_9 1164 # ASSIGN : s_1_0 0 # ASSIGN : s_1_1 77 # ASSIGN : s_1_2 191 # ASSIGN : s_1_3 213 # ASSIGN : s_1_4 290 # ASSIGN : s_1_5 535 # ASSIGN : s_1_6 615 # ASSIGN : s_1_7 749 # ASSIGN : s_1_8 1084 # ASSIGN : s_1_9 1149 # ASSIGN : s_2_0 248 # ASSIGN : s_2_1 382 # ASSIGN : s_2_2 482 # ASSIGN : s_2_3 610 # ASSIGN : s_2_4 660 # ASSIGN : s_2_5 745 # ASSIGN : s_2_6 776 # ASSIGN : s_2_7 935 # ASSIGN : s_2_8 1153 # ASSIGN : s_2_9 1190 # ASSIGN : s_3_0 4 # ASSIGN : s_3_1 116 # ASSIGN : s_3_2 198 # ASSIGN : s_3_3 206 # ASSIGN : s_3_4 367 # ASSIGN : s_3_5 444 # ASSIGN : s_3_6 530 # ASSIGN : s_3_7 983 # ASSIGN : s_3_8 1066 # ASSIGN : s_3_9 1133 # ASSIGN : s_4_0 147 # ASSIGN : s_4_1 327 # ASSIGN : s_4_2 458 # ASSIGN : s_4_3 549 # ASSIGN : s_4_4 556 # ASSIGN : s_4_5 873 # ASSIGN : s_4_6 965 # ASSIGN : s_4_7 1015 # ASSIGN : s_4_8 1116 # ASSIGN : s_4_9 1142 # ASSIGN : s_5_0 212 # ASSIGN : s_5_1 308 # ASSIGN : s_5_2 632 # ASSIGN : s_5_3 685 # ASSIGN : s_5_4 694 # ASSIGN : s_5_5 777 # ASSIGN : s_5_6 923 # ASSIGN : s_5_7 931 # ASSIGN : s_5_8 1133 # ASSIGN : s_5_9 1172 # ASSIGN : s_6_0 48 # ASSIGN : s_6_1 176 # ASSIGN : s_6_2 277 # ASSIGN : s_6_3 378 # ASSIGN : s_6_4 406 # ASSIGN : s_6_5 523 # ASSIGN : s_6_6 593 # ASSIGN : s_6_7 680 # ASSIGN : s_6_8 850 # ASSIGN : s_6_9 956 # ASSIGN : s_7_0 16 # ASSIGN : s_7_1 163 # ASSIGN : s_7_2 329 # ASSIGN : s_7_3 471 # ASSIGN : s_7_4 560 # ASSIGN : s_7_5 619 # ASSIGN : s_7_6 739 # ASSIGN : s_7_7 953 # ASSIGN : s_7_8 992 # ASSIGN : s_7_9 1054 # ASSIGN : s_8_0 9 # ASSIGN : s_8_1 679 # ASSIGN : s_8_2 748 # ASSIGN : s_8_3 865 # ASSIGN : s_8_4 892 # ASSIGN : s_8_5 914 # ASSIGN : s_8_6 1002 # ASSIGN : s_8_7 1047 # ASSIGN : s_8_8 1107 # ASSIGN : s_8_9 1180 # ASSIGN : s_9_0 37 # ASSIGN : s_9_1 70 # ASSIGN : s_9_2 131 # ASSIGN : s_9_3 175 # ASSIGN : s_9_4 201 # ASSIGN : s_9_5 285 # ASSIGN : s_9_6 369 # ASSIGN : s_9_7 437 # ASSIGN : s_9_8 485 # ASSIGN : s_9_9 841 # ASSIGN : s_10_0 40 # ASSIGN : s_10_1 83 # ASSIGN : s_10_2 183 # ASSIGN : s_10_3 231 # ASSIGN : s_10_4 329 # ASSIGN : s_10_5 504 # ASSIGN : s_10_6 574 # ASSIGN : s_10_7 611 # ASSIGN : s_10_8 1153 # ASSIGN : s_10_9 1192 # ASSIGN : s_11_0 266 # ASSIGN : s_11_1 461 # ASSIGN : s_11_2 581 # ASSIGN : s_11_3 654 # ASSIGN : s_11_4 903 # ASSIGN : s_11_5 1000 # ASSIGN : s_11_6 1039 # ASSIGN : s_11_7 1048 # ASSIGN : s_11_8 1071 # ASSIGN : s_11_9 1110 # ASSIGN : s_12_0 302 # ASSIGN : s_12_1 374 # ASSIGN : s_12_2 420 # ASSIGN : s_12_3 506 # ASSIGN : s_12_4 750 # ASSIGN : s_12_5 993 # ASSIGN : s_12_6 1024 # ASSIGN : s_12_7 1066 # ASSIGN : s_12_8 1118 # ASSIGN : s_12_9 1173 # ASSIGN : s_13_0 84 # ASSIGN : s_13_1 227 # ASSIGN : s_13_2 318 # ASSIGN : s_13_3 525 # ASSIGN : s_13_4 826 # ASSIGN : s_13_5 869 # ASSIGN : s_13_6 990 # ASSIGN : s_13_7 1062 # ASSIGN : s_13_8 1089 # ASSIGN : s_13_9 1162 # ASSIGN : s_14_0 86 # ASSIGN : s_14_1 155 # ASSIGN : s_14_2 248 # ASSIGN : s_14_3 262 # ASSIGN : s_14_4 336 # ASSIGN : s_14_5 451 # ASSIGN : s_14_6 956 # ASSIGN : s_14_7 1008 # ASSIGN : s_14_8 1104 # ASSIGN : s_14_9 1146 # ASSIGN : s_15_0 92 # ASSIGN : s_15_1 599 # ASSIGN : s_15_2 626 # ASSIGN : s_15_3 685 # ASSIGN : s_15_4 811 # ASSIGN : s_15_5 820 # ASSIGN : s_15_6 865 # ASSIGN : s_15_7 929 # ASSIGN : s_15_8 997 # ASSIGN : s_15_9 1073 # ASSIGN : s_16_0 8 # ASSIGN : s_16_1 260 # ASSIGN : s_16_2 528 # ASSIGN : s_16_3 629 # ASSIGN : s_16_4 680 # ASSIGN : s_16_5 757 # ASSIGN : s_16_6 805 # ASSIGN : s_16_7 907 # ASSIGN : s_16_8 1018 # ASSIGN : s_16_9 1134 # ASSIGN : s_17_0 14 # ASSIGN : s_17_1 111 # ASSIGN : s_17_2 132 # ASSIGN : s_17_3 187 # ASSIGN : s_17_4 236 # ASSIGN : s_17_5 397 # ASSIGN : s_17_6 459 # ASSIGN : s_17_7 677 # ASSIGN : s_17_8 794 # ASSIGN : s_17_9 1066 # ASSIGN : s_18_0 347 # ASSIGN : s_18_1 398 # ASSIGN : s_18_2 500 # ASSIGN : s_18_3 525 # ASSIGN : s_18_4 560 # ASSIGN : s_18_5 582 # ASSIGN : s_18_6 687 # ASSIGN : s_18_7 739 # ASSIGN : s_18_8 826 # ASSIGN : s_18_9 1156 # ASSIGN : s_19_0 138 # ASSIGN : s_19_1 207 # ASSIGN : s_19_2 250 # ASSIGN : s_19_3 483 # ASSIGN : s_19_4 555 # ASSIGN : s_19_5 591 # ASSIGN : s_19_6 637 # ASSIGN : s_19_7 762 # ASSIGN : s_19_8 819 # ASSIGN : s_19_9 940 SHOW_RESULT 1230 END : 1230 (1 seconds) [Thu Jun 1 20:30:35 2006] SHOW_RESULT 1230 CPU : 0.970000000000036 = 0.960000000000036 + 0.01 + 0 + 0 # BOUND : makespan 1216 1230 MODIFY_CNF 1223 BEGIN : [Thu Jun 1 20:30:35 2006] MODIFY_CNF 1223 END : 162515797 bytes (0 seconds) [Thu Jun 1 20:30:35 2006] MODIFY_CNF 1223 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1223 BEGIN : [Thu Jun 1 20:30:35 2006] CMD : minisat /work/tamura/csp2sat70812.cnf /work/tamura/csp2sat70812.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 3216078 9508217 | 1072026 0 0 NaNQ | 0.000 % | | 100 | 3216078 9508217 | 1179228 100 1275 12.8 | 58.226 % | | 250 | 3216078 9508217 | 1297151 250 2962 11.8 | 58.226 % | | 475 | 3216078 9508217 | 1426866 475 7120 15.0 | 58.226 % | | 813 | 3216078 9508217 | 1569553 813 12696 15.6 | 58.226 % | | 1320 | 3216078 9508217 | 1726508 1320 21279 16.1 | 58.226 % | | 2079 | 3216078 9508217 | 1899159 2079 42011 20.2 | 58.226 % | | 3218 | 3216078 9508217 | 2089075 3218 67804 21.1 | 58.226 % | | 4926 | 3216078 9508217 | 2297982 4926 139499 28.3 | 58.226 % | | 7489 | 3216078 9508217 | 2527781 7489 193689 25.9 | 58.226 % | | 11333 | 3216078 9508217 | 2780559 11333 307042 27.1 | 58.226 % | | 17099 | 3216078 9508217 | 3058615 17099 465981 27.3 | 58.226 % | | 25748 | 3216078 9508217 | 3364476 25748 700375 27.2 | 58.226 % | | 38722 | 3216078 9508217 | 3700924 38722 1182103 30.5 | 58.226 % | | 58183 | 3216078 9508217 | 4071016 58183 1708146 29.4 | 58.226 % | | 87376 | 3216078 9508217 | 4478118 87376 3782564 43.3 | 58.226 % | | 131165 | 3216078 9508217 | 4925930 131165 5287607 40.3 | 58.226 % | | 196849 | 3216078 9508217 | 5418523 196849 12089257 61.4 | 58.226 % | | 295375 | 3216078 9508217 | 5960375 295375 16397678 55.5 | 58.226 % | | 443164 | 3216078 9508217 | 6556413 443164 21434210 48.4 | 58.226 % | | 664849 | 3216078 9508217 | 7212054 664849 31149199 46.9 | 58.226 % | ==============================================================================) restarts : 21 conflicts : 774776 (90 /sec) decisions : 1041500 (121 /sec) propagations : 5926259204 (690356 /sec) inspects : 90360386265 (10526175 /sec) conflict literals : 40332356 (29.41 % deleted) CPU time : 8584.35 s SATISFIABLE VERIFY_CNF 1223 END : (8596 seconds) [Thu Jun 1 22:53:51 2006] VERIFY_CNF 1223 CPU : 8587.16 = 0.00999999999999091 + 0.02 + 8586.96 + 0.17 # RESULT : makespan 1223 SATISFIABLE SHOW_RESULT 1223 BEGIN : [Thu Jun 1 22:53:51 2006] # ASSIGN : makespan 1223 # ASSIGN : s_0_0 70 # ASSIGN : s_0_1 109 # ASSIGN : s_0_2 219 # ASSIGN : s_0_3 291 # ASSIGN : s_0_4 377 # ASSIGN : s_0_5 383 # ASSIGN : s_0_6 402 # ASSIGN : s_0_7 811 # ASSIGN : s_0_8 888 # ASSIGN : s_0_9 928 # ASSIGN : s_1_0 445 # ASSIGN : s_1_1 515 # ASSIGN : s_1_2 742 # ASSIGN : s_1_3 763 # ASSIGN : s_1_4 843 # ASSIGN : s_1_5 914 # ASSIGN : s_1_6 939 # ASSIGN : s_1_7 1033 # ASSIGN : s_1_8 1143 # ASSIGN : s_1_9 1208 # ASSIGN : s_2_0 190 # ASSIGN : s_2_1 274 # ASSIGN : s_2_2 429 # ASSIGN : s_2_3 729 # ASSIGN : s_2_4 792 # ASSIGN : s_2_5 877 # ASSIGN : s_2_6 908 # ASSIGN : s_2_7 937 # ASSIGN : s_2_8 1106 # ASSIGN : s_2_9 1183 # ASSIGN : s_3_0 0 # ASSIGN : s_3_1 86 # ASSIGN : s_3_2 153 # ASSIGN : s_3_3 161 # ASSIGN : s_3_4 191 # ASSIGN : s_3_5 268 # ASSIGN : s_3_6 366 # ASSIGN : s_3_7 446 # ASSIGN : s_3_8 554 # ASSIGN : s_3_9 1126 # ASSIGN : s_4_0 314 # ASSIGN : s_4_1 374 # ASSIGN : s_4_2 486 # ASSIGN : s_4_3 577 # ASSIGN : s_4_4 595 # ASSIGN : s_4_5 757 # ASSIGN : s_4_6 848 # ASSIGN : s_4_7 928 # ASSIGN : s_4_8 1109 # ASSIGN : s_4_9 1127 # ASSIGN : s_5_0 154 # ASSIGN : s_5_1 233 # ASSIGN : s_5_2 289 # ASSIGN : s_5_3 354 # ASSIGN : s_5_4 363 # ASSIGN : s_5_5 456 # ASSIGN : s_5_6 591 # ASSIGN : s_5_7 674 # ASSIGN : s_5_8 1126 # ASSIGN : s_5_9 1165 # ASSIGN : s_6_0 92 # ASSIGN : s_6_1 219 # ASSIGN : s_6_2 306 # ASSIGN : s_6_3 401 # ASSIGN : s_6_4 448 # ASSIGN : s_6_5 693 # ASSIGN : s_6_6 841 # ASSIGN : s_6_7 1004 # ASSIGN : s_6_8 1123 # ASSIGN : s_6_9 1196 # ASSIGN : s_7_0 5 # ASSIGN : s_7_1 166 # ASSIGN : s_7_2 454 # ASSIGN : s_7_3 510 # ASSIGN : s_7_4 581 # ASSIGN : s_7_5 690 # ASSIGN : s_7_6 756 # ASSIGN : s_7_7 837 # ASSIGN : s_7_8 876 # ASSIGN : s_7_9 1020 # ASSIGN : s_8_0 275 # ASSIGN : s_8_1 331 # ASSIGN : s_8_2 417 # ASSIGN : s_8_3 724 # ASSIGN : s_8_4 751 # ASSIGN : s_8_5 795 # ASSIGN : s_8_6 961 # ASSIGN : s_8_7 1040 # ASSIGN : s_8_8 1100 # ASSIGN : s_8_9 1211 # ASSIGN : s_9_0 1 # ASSIGN : s_9_1 100 # ASSIGN : s_9_2 175 # ASSIGN : s_9_3 243 # ASSIGN : s_9_4 282 # ASSIGN : s_9_5 468 # ASSIGN : s_9_6 570 # ASSIGN : s_9_7 640 # ASSIGN : s_9_8 763 # ASSIGN : s_9_9 863 # ASSIGN : s_10_0 0 # ASSIGN : s_10_1 43 # ASSIGN : s_10_2 115 # ASSIGN : s_10_3 145 # ASSIGN : s_10_4 243 # ASSIGN : s_10_5 615 # ASSIGN : s_10_6 642 # ASSIGN : s_10_7 650 # ASSIGN : s_10_8 1021 # ASSIGN : s_10_9 1085 # ASSIGN : s_11_0 14 # ASSIGN : s_11_1 33 # ASSIGN : s_11_2 102 # ASSIGN : s_11_3 190 # ASSIGN : s_11_4 376 # ASSIGN : s_11_5 962 # ASSIGN : s_11_6 1001 # ASSIGN : s_11_7 1010 # ASSIGN : s_11_8 1093 # ASSIGN : s_11_9 1122 # ASSIGN : s_12_0 305 # ASSIGN : s_12_1 400 # ASSIGN : s_12_2 510 # ASSIGN : s_12_3 638 # ASSIGN : s_12_4 731 # ASSIGN : s_12_5 827 # ASSIGN : s_12_6 834 # ASSIGN : s_12_7 889 # ASSIGN : s_12_8 955 # ASSIGN : s_12_9 1020 # ASSIGN : s_13_0 562 # ASSIGN : s_13_1 661 # ASSIGN : s_13_2 752 # ASSIGN : s_13_3 773 # ASSIGN : s_13_4 855 # ASSIGN : s_13_5 898 # ASSIGN : s_13_6 994 # ASSIGN : s_13_7 1066 # ASSIGN : s_13_8 1077 # ASSIGN : s_13_9 1155 # ASSIGN : s_14_0 164 # ASSIGN : s_14_1 334 # ASSIGN : s_14_2 453 # ASSIGN : s_14_3 634 # ASSIGN : s_14_4 773 # ASSIGN : s_14_5 854 # ASSIGN : s_14_6 950 # ASSIGN : s_14_7 984 # ASSIGN : s_14_8 1059 # ASSIGN : s_14_9 1112 # ASSIGN : s_15_0 34 # ASSIGN : s_15_1 133 # ASSIGN : s_15_2 160 # ASSIGN : s_15_3 293 # ASSIGN : s_15_4 365 # ASSIGN : s_15_5 389 # ASSIGN : s_15_6 434 # ASSIGN : s_15_7 483 # ASSIGN : s_15_8 546 # ASSIGN : s_15_9 1006 # ASSIGN : s_16_0 176 # ASSIGN : s_16_1 251 # ASSIGN : s_16_2 274 # ASSIGN : s_16_3 502 # ASSIGN : s_16_4 552 # ASSIGN : s_16_5 617 # ASSIGN : s_16_6 654 # ASSIGN : s_16_7 1019 # ASSIGN : s_16_8 1137 # ASSIGN : s_16_9 1215 # ASSIGN : s_17_0 28 # ASSIGN : s_17_1 100 # ASSIGN : s_17_2 398 # ASSIGN : s_17_3 550 # ASSIGN : s_17_4 599 # ASSIGN : s_17_5 695 # ASSIGN : s_17_6 765 # ASSIGN : s_17_7 883 # ASSIGN : s_17_8 991 # ASSIGN : s_17_9 1089 # ASSIGN : s_18_0 80 # ASSIGN : s_18_1 527 # ASSIGN : s_18_2 590 # ASSIGN : s_18_3 615 # ASSIGN : s_18_4 674 # ASSIGN : s_18_5 695 # ASSIGN : s_18_6 759 # ASSIGN : s_18_7 939 # ASSIGN : s_18_8 1110 # ASSIGN : s_18_9 1149 # ASSIGN : s_19_0 201 # ASSIGN : s_19_1 269 # ASSIGN : s_19_2 318 # ASSIGN : s_19_3 377 # ASSIGN : s_19_4 429 # ASSIGN : s_19_5 445 # ASSIGN : s_19_6 465 # ASSIGN : s_19_7 584 # ASSIGN : s_19_8 641 # ASSIGN : s_19_9 1006 SHOW_RESULT 1223 END : 1223 (1 seconds) [Thu Jun 1 22:53:52 2006] SHOW_RESULT 1223 CPU : 0.97999999999997 = 0.96999999999997 + 0.01 + 0 + 0 # BOUND : makespan 1216 1223 MODIFY_CNF 1219 BEGIN : [Thu Jun 1 22:53:52 2006] MODIFY_CNF 1219 END : 162515797 bytes (0 seconds) [Thu Jun 1 22:53:52 2006] MODIFY_CNF 1219 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1219 BEGIN : [Thu Jun 1 22:53:52 2006] CMD : minisat /work/tamura/csp2sat70812.cnf /work/tamura/csp2sat70812.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 3195464 9447186 | 1065154 0 0 NaNQ | 0.000 % | | 100 | 3195464 9447186 | 1171669 100 1963 19.6 | 58.466 % | | 251 | 3195464 9447186 | 1288836 251 4109 16.4 | 58.466 % | | 477 | 3195464 9447186 | 1417719 477 8156 17.1 | 58.466 % | | 815 | 3195464 9447186 | 1559491 815 14323 17.6 | 58.466 % | | 1322 | 3195464 9447186 | 1715441 1322 21758 16.5 | 58.466 % | | 2082 | 3195464 9447186 | 1886985 2082 36349 17.5 | 58.466 % | | 3222 | 3195464 9447186 | 2075683 3222 85246 26.5 | 58.466 % | | 4930 | 3195464 9447186 | 2283252 4930 112156 22.7 | 58.466 % | | 7492 | 3195464 9447186 | 2511577 7492 153728 20.5 | 58.466 % | | 11336 | 3195464 9447186 | 2762735 11336 315404 27.8 | 58.466 % | | 17102 | 3195464 9447186 | 3039008 17102 469739 27.5 | 58.466 % | | 25751 | 3195464 9447186 | 3342909 25751 642883 25.0 | 58.466 % | | 38725 | 3195464 9447186 | 3677200 38725 1189428 30.7 | 58.466 % | ==============================================================================) restarts : 14 conflicts : 43763 (144 /sec) decisions : 66231 (218 /sec) propagations : 334369857 (1102087 /sec) inspects : 4547892150 (14989907 /sec) conflict literals : 1351067 (21.11 % deleted) CPU time : 303.397 s SATISFIABLE VERIFY_CNF 1219 END : (306 seconds) [Thu Jun 1 22:58:58 2006] VERIFY_CNF 1219 CPU : 305.43 = 0 + 0.02 + 305.23 + 0.18 # RESULT : makespan 1219 SATISFIABLE SHOW_RESULT 1219 BEGIN : [Thu Jun 1 22:58:58 2006] # ASSIGN : makespan 1219 # ASSIGN : s_0_0 12 # ASSIGN : s_0_1 95 # ASSIGN : s_0_2 176 # ASSIGN : s_0_3 231 # ASSIGN : s_0_4 271 # ASSIGN : s_0_5 278 # ASSIGN : s_0_6 297 # ASSIGN : s_0_7 829 # ASSIGN : s_0_8 866 # ASSIGN : s_0_9 931 # ASSIGN : s_1_0 548 # ASSIGN : s_1_1 643 # ASSIGN : s_1_2 698 # ASSIGN : s_1_3 719 # ASSIGN : s_1_4 813 # ASSIGN : s_1_5 870 # ASSIGN : s_1_6 909 # ASSIGN : s_1_7 974 # ASSIGN : s_1_8 1139 # ASSIGN : s_1_9 1204 # ASSIGN : s_2_0 3 # ASSIGN : s_2_1 87 # ASSIGN : s_2_2 191 # ASSIGN : s_2_3 272 # ASSIGN : s_2_4 316 # ASSIGN : s_2_5 414 # ASSIGN : s_2_6 447 # ASSIGN : s_2_7 714 # ASSIGN : s_2_8 803 # ASSIGN : s_2_9 1179 # ASSIGN : s_3_0 7 # ASSIGN : s_3_1 87 # ASSIGN : s_3_2 146 # ASSIGN : s_3_3 154 # ASSIGN : s_3_4 202 # ASSIGN : s_3_5 279 # ASSIGN : s_3_6 317 # ASSIGN : s_3_7 397 # ASSIGN : s_3_8 476 # ASSIGN : s_3_9 1122 # ASSIGN : s_4_0 144 # ASSIGN : s_4_1 184 # ASSIGN : s_4_2 277 # ASSIGN : s_4_3 371 # ASSIGN : s_4_4 378 # ASSIGN : s_4_5 445 # ASSIGN : s_4_6 525 # ASSIGN : s_4_7 581 # ASSIGN : s_4_8 1105 # ASSIGN : s_4_9 1131 # ASSIGN : s_5_0 289 # ASSIGN : s_5_1 437 # ASSIGN : s_5_2 509 # ASSIGN : s_5_3 594 # ASSIGN : s_5_4 626 # ASSIGN : s_5_5 895 # ASSIGN : s_5_6 1037 # ASSIGN : s_5_7 1045 # ASSIGN : s_5_8 1122 # ASSIGN : s_5_9 1161 # ASSIGN : s_6_0 45 # ASSIGN : s_6_1 160 # ASSIGN : s_6_2 340 # ASSIGN : s_6_3 432 # ASSIGN : s_6_4 488 # ASSIGN : s_6_5 783 # ASSIGN : s_6_6 853 # ASSIGN : s_6_7 1000 # ASSIGN : s_6_8 1096 # ASSIGN : s_6_9 1192 # ASSIGN : s_7_0 0 # ASSIGN : s_7_1 106 # ASSIGN : s_7_2 222 # ASSIGN : s_7_3 301 # ASSIGN : s_7_4 368 # ASSIGN : s_7_5 507 # ASSIGN : s_7_6 603 # ASSIGN : s_7_7 684 # ASSIGN : s_7_8 737 # ASSIGN : s_7_9 1016 # ASSIGN : s_8_0 397 # ASSIGN : s_8_1 453 # ASSIGN : s_8_2 533 # ASSIGN : s_8_3 687 # ASSIGN : s_8_4 750 # ASSIGN : s_8_5 787 # ASSIGN : s_8_6 991 # ASSIGN : s_8_7 1036 # ASSIGN : s_8_8 1096 # ASSIGN : s_8_9 1207 # ASSIGN : s_9_0 198 # ASSIGN : s_9_1 255 # ASSIGN : s_9_2 318 # ASSIGN : s_9_3 376 # ASSIGN : s_9_4 404 # ASSIGN : s_9_5 493 # ASSIGN : s_9_6 575 # ASSIGN : s_9_7 645 # ASSIGN : s_9_8 666 # ASSIGN : s_9_9 956 # ASSIGN : s_10_0 44 # ASSIGN : s_10_1 156 # ASSIGN : s_10_2 452 # ASSIGN : s_10_3 482 # ASSIGN : s_10_4 580 # ASSIGN : s_10_5 859 # ASSIGN : s_10_6 918 # ASSIGN : s_10_7 940 # ASSIGN : s_10_8 1099 # ASSIGN : s_10_9 1169 # ASSIGN : s_11_0 0 # ASSIGN : s_11_1 19 # ASSIGN : s_11_2 87 # ASSIGN : s_11_3 186 # ASSIGN : s_11_4 271 # ASSIGN : s_11_5 680 # ASSIGN : s_11_6 733 # ASSIGN : s_11_7 764 # ASSIGN : s_11_8 840 # ASSIGN : s_11_9 1118 # ASSIGN : s_12_0 246 # ASSIGN : s_12_1 325 # ASSIGN : s_12_2 402 # ASSIGN : s_12_3 706 # ASSIGN : s_12_4 799 # ASSIGN : s_12_5 860 # ASSIGN : s_12_6 867 # ASSIGN : s_12_7 975 # ASSIGN : s_12_8 1051 # ASSIGN : s_12_9 1147 # ASSIGN : s_13_0 353 # ASSIGN : s_13_1 554 # ASSIGN : s_13_2 655 # ASSIGN : s_13_3 674 # ASSIGN : s_13_4 742 # ASSIGN : s_13_5 869 # ASSIGN : s_13_6 965 # ASSIGN : s_13_7 1051 # ASSIGN : s_13_8 1087 # ASSIGN : s_13_9 1151 # ASSIGN : s_14_0 144 # ASSIGN : s_14_1 228 # ASSIGN : s_14_2 463 # ASSIGN : s_14_3 532 # ASSIGN : s_14_4 586 # ASSIGN : s_14_5 832 # ASSIGN : s_14_6 906 # ASSIGN : s_14_7 940 # ASSIGN : s_14_8 1055 # ASSIGN : s_14_9 1108 # ASSIGN : s_15_0 99 # ASSIGN : s_15_1 215 # ASSIGN : s_15_2 242 # ASSIGN : s_15_3 304 # ASSIGN : s_15_4 401 # ASSIGN : s_15_5 410 # ASSIGN : s_15_6 460 # ASSIGN : s_15_7 517 # ASSIGN : s_15_8 744 # ASSIGN : s_15_9 1062 # ASSIGN : s_16_0 71 # ASSIGN : s_16_1 323 # ASSIGN : s_16_2 416 # ASSIGN : s_16_3 522 # ASSIGN : s_16_4 572 # ASSIGN : s_16_5 637 # ASSIGN : s_16_6 769 # ASSIGN : s_16_7 885 # ASSIGN : s_16_8 1014 # ASSIGN : s_16_9 1085 # ASSIGN : s_17_0 72 # ASSIGN : s_17_1 177 # ASSIGN : s_17_2 248 # ASSIGN : s_17_3 361 # ASSIGN : s_17_4 618 # ASSIGN : s_17_5 723 # ASSIGN : s_17_6 785 # ASSIGN : s_17_7 875 # ASSIGN : s_17_8 947 # ASSIGN : s_17_9 1093 # ASSIGN : s_18_0 498 # ASSIGN : s_18_1 709 # ASSIGN : s_18_2 772 # ASSIGN : s_18_3 797 # ASSIGN : s_18_4 849 # ASSIGN : s_18_5 926 # ASSIGN : s_18_6 973 # ASSIGN : s_18_7 1025 # ASSIGN : s_18_8 1106 # ASSIGN : s_18_9 1145 # ASSIGN : s_19_0 86 # ASSIGN : s_19_1 189 # ASSIGN : s_19_2 213 # ASSIGN : s_19_3 362 # ASSIGN : s_19_4 427 # ASSIGN : s_19_5 455 # ASSIGN : s_19_6 475 # ASSIGN : s_19_7 599 # ASSIGN : s_19_8 656 # ASSIGN : s_19_9 903 SHOW_RESULT 1219 END : 1219 (1 seconds) [Thu Jun 1 22:58:59 2006] SHOW_RESULT 1219 CPU : 0.970000000000036 = 0.960000000000036 + 0.0099999999999999 + 0 + 0 # BOUND : makespan 1216 1219 MODIFY_CNF 1217 BEGIN : [Thu Jun 1 22:58:59 2006] MODIFY_CNF 1217 END : 162515797 bytes (0 seconds) [Thu Jun 1 22:58:59 2006] MODIFY_CNF 1217 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1217 BEGIN : [Thu Jun 1 22:58:59 2006] CMD : minisat /work/tamura/csp2sat70812.cnf /work/tamura/csp2sat70812.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 3187506 9423714 | 1062502 0 0 NaNQ | 0.000 % | | 101 | 3187506 9423714 | 1168752 101 1790 17.7 | 58.584 % | | 252 | 3187506 9423714 | 1285627 252 3488 13.8 | 58.584 % | | 477 | 3187506 9423714 | 1414190 477 6915 14.5 | 58.584 % | | 814 | 3187506 9423714 | 1555609 814 11943 14.7 | 58.584 % | | 1320 | 3187506 9423714 | 1711170 1320 17815 13.5 | 58.584 % | | 2080 | 3187506 9423714 | 1882287 2080 26353 12.7 | 58.584 % | | 3219 | 3187506 9423714 | 2070515 3219 41459 12.9 | 58.584 % | | 4927 | 3187506 9423714 | 2277567 4927 84440 17.1 | 58.584 % | | 7489 | 3187506 9423714 | 2505324 7489 171682 22.9 | 58.584 % | | 11333 | 3187506 9423714 | 2755856 11333 242103 21.4 | 58.584 % | | 17099 | 3187506 9423714 | 3031442 17099 359268 21.0 | 58.584 % | | 25749 | 3187506 9423714 | 3334586 25749 643619 25.0 | 58.584 % | | 38723 | 3187506 9423714 | 3668045 38723 1022229 26.4 | 58.584 % | | 58184 | 3187506 9423714 | 4034849 58184 1833219 31.5 | 58.584 % | | 87377 | 3187506 9423714 | 4438334 87377 4411177 50.5 | 58.584 % | | 131168 | 3187506 9423714 | 4882167 131168 6192039 47.2 | 58.584 % | ==============================================================================) restarts : 17 conflicts : 147816 (141 /sec) decisions : 209255 (199 /sec) propagations : 1043014697 (994039 /sec) inspects : 14879050808 (14180394 /sec) conflict literals : 7008987 (22.32 % deleted) CPU time : 1049.27 s SATISFIABLE VERIFY_CNF 1217 END : (1053 seconds) [Thu Jun 1 23:16:32 2006] VERIFY_CNF 1217 CPU : 1051.9 = 0.00999999999999091 + 0.03 + 1051.24 + 0.62 # RESULT : makespan 1217 SATISFIABLE SHOW_RESULT 1217 BEGIN : [Thu Jun 1 23:16:32 2006] # ASSIGN : makespan 1217 # ASSIGN : s_0_0 9 # ASSIGN : s_0_1 105 # ASSIGN : s_0_2 218 # ASSIGN : s_0_3 273 # ASSIGN : s_0_4 313 # ASSIGN : s_0_5 319 # ASSIGN : s_0_6 384 # ASSIGN : s_0_7 568 # ASSIGN : s_0_8 1008 # ASSIGN : s_0_9 1048 # ASSIGN : s_1_0 304 # ASSIGN : s_1_1 437 # ASSIGN : s_1_2 492 # ASSIGN : s_1_3 525 # ASSIGN : s_1_4 595 # ASSIGN : s_1_5 650 # ASSIGN : s_1_6 675 # ASSIGN : s_1_7 775 # ASSIGN : s_1_8 982 # ASSIGN : s_1_9 1145 # ASSIGN : s_2_0 54 # ASSIGN : s_2_1 314 # ASSIGN : s_2_2 527 # ASSIGN : s_2_3 551 # ASSIGN : s_2_4 710 # ASSIGN : s_2_5 866 # ASSIGN : s_2_6 1028 # ASSIGN : s_2_7 1057 # ASSIGN : s_2_8 1140 # ASSIGN : s_2_9 1177 # ASSIGN : s_3_0 2 # ASSIGN : s_3_1 97 # ASSIGN : s_3_2 156 # ASSIGN : s_3_3 180 # ASSIGN : s_3_4 210 # ASSIGN : s_3_5 331 # ASSIGN : s_3_6 471 # ASSIGN : s_3_7 556 # ASSIGN : s_3_8 634 # ASSIGN : s_3_9 1120 # ASSIGN : s_4_0 466 # ASSIGN : s_4_1 532 # ASSIGN : s_4_2 611 # ASSIGN : s_4_3 741 # ASSIGN : s_4_4 836 # ASSIGN : s_4_5 897 # ASSIGN : s_4_6 984 # ASSIGN : s_4_7 1047 # ASSIGN : s_4_8 1103 # ASSIGN : s_4_9 1129 # ASSIGN : s_5_0 138 # ASSIGN : s_5_1 230 # ASSIGN : s_5_2 488 # ASSIGN : s_5_3 580 # ASSIGN : s_5_4 589 # ASSIGN : s_5_5 688 # ASSIGN : s_5_6 838 # ASSIGN : s_5_7 905 # ASSIGN : s_5_8 1120 # ASSIGN : s_5_9 1159 # ASSIGN : s_6_0 42 # ASSIGN : s_6_1 141 # ASSIGN : s_6_2 227 # ASSIGN : s_6_3 319 # ASSIGN : s_6_4 347 # ASSIGN : s_6_5 455 # ASSIGN : s_6_6 579 # ASSIGN : s_6_7 740 # ASSIGN : s_6_8 1094 # ASSIGN : s_6_9 1190 # ASSIGN : s_7_0 1 # ASSIGN : s_7_1 99 # ASSIGN : s_7_2 338 # ASSIGN : s_7_3 403 # ASSIGN : s_7_4 533 # ASSIGN : s_7_5 669 # ASSIGN : s_7_6 726 # ASSIGN : s_7_7 827 # ASSIGN : s_7_8 1062 # ASSIGN : s_7_9 1098 # ASSIGN : s_8_0 340 # ASSIGN : s_8_1 415 # ASSIGN : s_8_2 757 # ASSIGN : s_8_3 852 # ASSIGN : s_8_4 879 # ASSIGN : s_8_5 901 # ASSIGN : s_8_6 989 # ASSIGN : s_8_7 1034 # ASSIGN : s_8_8 1094 # ASSIGN : s_8_9 1205 # ASSIGN : s_9_0 3 # ASSIGN : s_9_1 36 # ASSIGN : s_9_2 97 # ASSIGN : s_9_3 160 # ASSIGN : s_9_4 186 # ASSIGN : s_9_5 287 # ASSIGN : s_9_6 369 # ASSIGN : s_9_7 444 # ASSIGN : s_9_8 465 # ASSIGN : s_9_9 850 # ASSIGN : s_10_0 41 # ASSIGN : s_10_1 84 # ASSIGN : s_10_2 181 # ASSIGN : s_10_3 211 # ASSIGN : s_10_4 309 # ASSIGN : s_10_5 445 # ASSIGN : s_10_6 484 # ASSIGN : s_10_7 506 # ASSIGN : s_10_8 1097 # ASSIGN : s_10_9 1167 # ASSIGN : s_11_0 23 # ASSIGN : s_11_1 374 # ASSIGN : s_11_2 477 # ASSIGN : s_11_3 731 # ASSIGN : s_11_4 895 # ASSIGN : s_11_5 1032 # ASSIGN : s_11_6 1071 # ASSIGN : s_11_7 1080 # ASSIGN : s_11_8 1103 # ASSIGN : s_11_9 1116 # ASSIGN : s_12_0 273 # ASSIGN : s_12_1 369 # ASSIGN : s_12_2 499 # ASSIGN : s_12_3 605 # ASSIGN : s_12_4 918 # ASSIGN : s_12_5 979 # ASSIGN : s_12_6 986 # ASSIGN : s_12_7 1053 # ASSIGN : s_12_8 1105 # ASSIGN : s_12_9 1160 # ASSIGN : s_13_0 82 # ASSIGN : s_13_1 207 # ASSIGN : s_13_2 298 # ASSIGN : s_13_3 394 # ASSIGN : s_13_4 513 # ASSIGN : s_13_5 750 # ASSIGN : s_13_6 846 # ASSIGN : s_13_7 977 # ASSIGN : s_13_8 988 # ASSIGN : s_13_9 1149 # ASSIGN : s_14_0 95 # ASSIGN : s_14_1 164 # ASSIGN : s_14_2 215 # ASSIGN : s_14_3 230 # ASSIGN : s_14_4 270 # ASSIGN : s_14_5 617 # ASSIGN : s_14_6 804 # ASSIGN : s_14_7 872 # ASSIGN : s_14_8 949 # ASSIGN : s_14_9 987 # ASSIGN : s_15_0 174 # ASSIGN : s_15_1 500 # ASSIGN : s_15_2 643 # ASSIGN : s_15_3 702 # ASSIGN : s_15_4 795 # ASSIGN : s_15_5 807 # ASSIGN : s_15_6 852 # ASSIGN : s_15_7 921 # ASSIGN : s_15_8 984 # ASSIGN : s_15_9 1060 # ASSIGN : s_16_0 7 # ASSIGN : s_16_1 82 # ASSIGN : s_16_2 213 # ASSIGN : s_16_3 319 # ASSIGN : s_16_4 397 # ASSIGN : s_16_5 462 # ASSIGN : s_16_6 536 # ASSIGN : s_16_7 641 # ASSIGN : s_16_8 917 # ASSIGN : s_16_9 1024 # ASSIGN : s_17_0 23 # ASSIGN : s_17_1 96 # ASSIGN : s_17_2 184 # ASSIGN : s_17_3 392 # ASSIGN : s_17_4 441 # ASSIGN : s_17_5 550 # ASSIGN : s_17_6 612 # ASSIGN : s_17_7 702 # ASSIGN : s_17_8 774 # ASSIGN : s_17_9 986 # ASSIGN : s_18_0 279 # ASSIGN : s_18_1 603 # ASSIGN : s_18_2 666 # ASSIGN : s_18_3 691 # ASSIGN : s_18_4 784 # ASSIGN : s_18_5 805 # ASSIGN : s_18_6 852 # ASSIGN : s_18_7 904 # ASSIGN : s_18_8 1041 # ASSIGN : s_18_9 1143 # ASSIGN : s_19_0 112 # ASSIGN : s_19_1 187 # ASSIGN : s_19_2 240 # ASSIGN : s_19_3 345 # ASSIGN : s_19_4 592 # ASSIGN : s_19_5 597 # ASSIGN : s_19_6 698 # ASSIGN : s_19_7 748 # ASSIGN : s_19_8 816 # ASSIGN : s_19_9 1076 SHOW_RESULT 1217 END : 1217 (1 seconds) [Thu Jun 1 23:16:33 2006] SHOW_RESULT 1217 CPU : 0.939999999999998 = 0.939999999999998 + 0 + 0 + 0 # BOUND : makespan 1216 1217 MODIFY_CNF 1216 BEGIN : [Thu Jun 1 23:16:33 2006] MODIFY_CNF 1216 END : 162515797 bytes (0 seconds) [Thu Jun 1 23:16:33 2006] MODIFY_CNF 1216 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1216 BEGIN : [Thu Jun 1 23:16:33 2006] CMD : minisat /work/tamura/csp2sat70812.cnf /work/tamura/csp2sat70812.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 3183528 9411980 | 1061176 0 0 NaNQ | 0.000 % | | 101 | 3183528 9411980 | 1167293 101 1947 19.3 | 58.644 % | | 252 | 3183528 9411980 | 1284022 252 3837 15.2 | 58.644 % | | 477 | 3183528 9411980 | 1412425 477 7580 15.9 | 58.644 % | | 815 | 3183528 9411980 | 1553667 815 12427 15.2 | 58.644 % | | 1321 | 3183528 9411980 | 1709034 1321 19967 15.1 | 58.644 % | | 2080 | 3183528 9411980 | 1879938 2080 29126 14.0 | 58.644 % | | 3220 | 3183528 9411980 | 2067931 3220 44482 13.8 | 58.644 % | | 4929 | 3183528 9411980 | 2274724 4929 81313 16.5 | 58.644 % | | 7491 | 3183528 9411980 | 2502197 7491 116628 15.6 | 58.644 % | | 11335 | 3183528 9411980 | 2752417 11335 220735 19.5 | 58.644 % | | 17101 | 3183528 9411980 | 3027658 17101 373843 21.9 | 58.644 % | | 25751 | 3183528 9411980 | 3330424 25751 906903 35.2 | 58.644 % | | 38725 | 3183528 9411980 | 3663467 38725 1189898 30.7 | 58.644 % | | 58186 | 3183528 9411980 | 4029814 58186 1551143 26.7 | 58.644 % | | 87378 | 3183528 9411980 | 4432795 87378 2453044 28.1 | 58.644 % | | 131167 | 3183528 9411980 | 4876075 131167 3153746 24.0 | 58.644 % | | 196853 | 3183528 9411980 | 5363682 196853 4496714 22.8 | 58.644 % | ==============================================================================) restarts : 18 conflicts : 215183 (125 /sec) decisions : 298886 (173 /sec) propagations : 1814040427 (1049595 /sec) inspects : 22877944776 (13237066 /sec) conflict literals : 5477350 (29.76 % deleted) CPU time : 1728.32 s SATISFIABLE VERIFY_CNF 1216 END : (1732 seconds) [Thu Jun 1 23:45:25 2006] VERIFY_CNF 1216 CPU : 1730.92 = 0.00999999999999091 + 0.03 + 1730.25 + 0.63 # RESULT : makespan 1216 SATISFIABLE SHOW_RESULT 1216 BEGIN : [Thu Jun 1 23:45:25 2006] # ASSIGN : makespan 1216 # ASSIGN : s_0_0 69 # ASSIGN : s_0_1 102 # ASSIGN : s_0_2 239 # ASSIGN : s_0_3 303 # ASSIGN : s_0_4 343 # ASSIGN : s_0_5 349 # ASSIGN : s_0_6 368 # ASSIGN : s_0_7 778 # ASSIGN : s_0_8 856 # ASSIGN : s_0_9 1004 # ASSIGN : s_1_0 578 # ASSIGN : s_1_1 660 # ASSIGN : s_1_2 752 # ASSIGN : s_1_3 783 # ASSIGN : s_1_4 847 # ASSIGN : s_1_5 969 # ASSIGN : s_1_6 994 # ASSIGN : s_1_7 1059 # ASSIGN : s_1_8 1136 # ASSIGN : s_1_9 1201 # ASSIGN : s_2_0 33 # ASSIGN : s_2_1 150 # ASSIGN : s_2_2 243 # ASSIGN : s_2_3 267 # ASSIGN : s_2_4 350 # ASSIGN : s_2_5 442 # ASSIGN : s_2_6 520 # ASSIGN : s_2_7 862 # ASSIGN : s_2_8 945 # ASSIGN : s_2_9 1176 # ASSIGN : s_3_0 5 # ASSIGN : s_3_1 86 # ASSIGN : s_3_2 221 # ASSIGN : s_3_3 229 # ASSIGN : s_3_4 380 # ASSIGN : s_3_5 467 # ASSIGN : s_3_6 529 # ASSIGN : s_3_7 612 # ASSIGN : s_3_8 684 # ASSIGN : s_3_9 1059 # ASSIGN : s_4_0 238 # ASSIGN : s_4_1 435 # ASSIGN : s_4_2 627 # ASSIGN : s_4_3 718 # ASSIGN : s_4_4 725 # ASSIGN : s_4_5 844 # ASSIGN : s_4_6 932 # ASSIGN : s_4_7 982 # ASSIGN : s_4_8 1062 # ASSIGN : s_4_9 1082 # ASSIGN : s_5_0 247 # ASSIGN : s_5_1 283 # ASSIGN : s_5_2 298 # ASSIGN : s_5_3 371 # ASSIGN : s_5_4 504 # ASSIGN : s_5_5 684 # ASSIGN : s_5_6 787 # ASSIGN : s_5_7 816 # ASSIGN : s_5_8 893 # ASSIGN : s_5_9 1115 # ASSIGN : s_6_0 47 # ASSIGN : s_6_1 146 # ASSIGN : s_6_2 268 # ASSIGN : s_6_3 400 # ASSIGN : s_6_4 431 # ASSIGN : s_6_5 558 # ASSIGN : s_6_6 628 # ASSIGN : s_6_7 784 # ASSIGN : s_6_8 1024 # ASSIGN : s_6_9 1097 # ASSIGN : s_7_0 7 # ASSIGN : s_7_1 114 # ASSIGN : s_7_2 293 # ASSIGN : s_7_3 353 # ASSIGN : s_7_4 477 # ASSIGN : s_7_5 648 # ASSIGN : s_7_6 781 # ASSIGN : s_7_7 1020 # ASSIGN : s_7_8 1061 # ASSIGN : s_7_9 1124 # ASSIGN : s_8_0 0 # ASSIGN : s_8_1 486 # ASSIGN : s_8_2 641 # ASSIGN : s_8_3 754 # ASSIGN : s_8_4 783 # ASSIGN : s_8_5 805 # ASSIGN : s_8_6 924 # ASSIGN : s_8_7 1033 # ASSIGN : s_8_8 1093 # ASSIGN : s_8_9 1166 # ASSIGN : s_9_0 0 # ASSIGN : s_9_1 33 # ASSIGN : s_9_2 101 # ASSIGN : s_9_3 145 # ASSIGN : s_9_4 183 # ASSIGN : s_9_5 278 # ASSIGN : s_9_6 360 # ASSIGN : s_9_7 428 # ASSIGN : s_9_8 449 # ASSIGN : s_9_9 884 # ASSIGN : s_10_0 5 # ASSIGN : s_10_1 48 # ASSIGN : s_10_2 120 # ASSIGN : s_10_3 195 # ASSIGN : s_10_4 293 # ASSIGN : s_10_5 396 # ASSIGN : s_10_6 478 # ASSIGN : s_10_7 526 # ASSIGN : s_10_8 815 # ASSIGN : s_10_9 1178 # ASSIGN : s_11_0 28 # ASSIGN : s_11_1 162 # ASSIGN : s_11_2 232 # ASSIGN : s_11_3 311 # ASSIGN : s_11_4 549 # ASSIGN : s_11_5 734 # ASSIGN : s_11_6 773 # ASSIGN : s_11_7 782 # ASSIGN : s_11_8 925 # ASSIGN : s_11_9 1173 # ASSIGN : s_12_0 305 # ASSIGN : s_12_1 377 # ASSIGN : s_12_2 458 # ASSIGN : s_12_3 567 # ASSIGN : s_12_4 795 # ASSIGN : s_12_5 873 # ASSIGN : s_12_6 880 # ASSIGN : s_12_7 922 # ASSIGN : s_12_8 1004 # ASSIGN : s_12_9 1073 # ASSIGN : s_13_0 405 # ASSIGN : s_13_1 536 # ASSIGN : s_13_2 673 # ASSIGN : s_13_3 715 # ASSIGN : s_13_4 791 # ASSIGN : s_13_5 834 # ASSIGN : s_13_6 930 # ASSIGN : s_13_7 1002 # ASSIGN : s_13_8 1013 # ASSIGN : s_13_9 1148 # ASSIGN : s_14_0 156 # ASSIGN : s_14_1 255 # ASSIGN : s_14_2 555 # ASSIGN : s_14_3 569 # ASSIGN : s_14_4 609 # ASSIGN : s_14_5 680 # ASSIGN : s_14_6 896 # ASSIGN : s_14_7 938 # ASSIGN : s_14_8 983 # ASSIGN : s_14_9 1013 # ASSIGN : s_15_0 117 # ASSIGN : s_15_1 216 # ASSIGN : s_15_2 294 # ASSIGN : s_15_3 386 # ASSIGN : s_15_4 569 # ASSIGN : s_15_5 635 # ASSIGN : s_15_6 733 # ASSIGN : s_15_7 931 # ASSIGN : s_15_8 1079 # ASSIGN : s_15_9 1156 # ASSIGN : s_16_0 124 # ASSIGN : s_16_1 199 # ASSIGN : s_16_2 259 # ASSIGN : s_16_3 423 # ASSIGN : s_16_4 473 # ASSIGN : s_16_5 538 # ASSIGN : s_16_6 575 # ASSIGN : s_16_7 972 # ASSIGN : s_16_8 1130 # ASSIGN : s_16_9 1208 # ASSIGN : s_17_0 84 # ASSIGN : s_17_1 422 # ASSIGN : s_17_2 436 # ASSIGN : s_17_3 477 # ASSIGN : s_17_4 689 # ASSIGN : s_17_5 780 # ASSIGN : s_17_6 842 # ASSIGN : s_17_7 932 # ASSIGN : s_17_8 1038 # ASSIGN : s_17_9 1170 # ASSIGN : s_18_0 85 # ASSIGN : s_18_1 506 # ASSIGN : s_18_2 575 # ASSIGN : s_18_3 600 # ASSIGN : s_18_4 647 # ASSIGN : s_18_5 668 # ASSIGN : s_18_6 715 # ASSIGN : s_18_7 767 # ASSIGN : s_18_8 893 # ASSIGN : s_18_9 1142 # ASSIGN : s_19_0 94 # ASSIGN : s_19_1 171 # ASSIGN : s_19_2 225 # ASSIGN : s_19_3 390 # ASSIGN : s_19_4 452 # ASSIGN : s_19_5 457 # ASSIGN : s_19_6 505 # ASSIGN : s_19_7 555 # ASSIGN : s_19_8 679 # ASSIGN : s_19_9 1029 SHOW_RESULT 1216 END : 1216 (1 seconds) [Thu Jun 1 23:45:26 2006] SHOW_RESULT 1216 CPU : 0.960000000000036 = 0.960000000000036 + 0 + 0 + 0 # BOUND : makespan 1216 1216 MAIN END : (12613 seconds) [Thu Jun 1 23:45:26 2006] MAIN CPU : 12598.61 = 347.13 + 0.73 + 12247.4 + 3.35