MAIN BEGIN : [Fri Jun 2 07:40:17 2006] READ BEGIN : csp/la40.csp [Fri Jun 2 07:40:17 2006] READ END : csp/la40.csp (4 seconds) [Fri Jun 2 07:40:21 2006] READ CPU : 4.56 = 4.56 + 0 + 0 + 0 # BOUND : makespan 1027 1778 GENERATE_CNF 1778 BEGIN : [Fri Jun 2 07:40:21 2006] GENERATE_CNF 1778 END : 404628 variables 6224041 clauses 148956405 bytes (306 seconds) [Fri Jun 2 07:45:27 2006] GENERATE_CNF 1778 CPU : 305.28 = 304.84 + 0.44 + 0 + 0 MODIFY_CNF 1402 BEGIN : [Fri Jun 2 07:45:27 2006] MODIFY_CNF 1402 END : 148956411 bytes (0 seconds) [Fri Jun 2 07:45:27 2006] MODIFY_CNF 1402 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1402 BEGIN : [Fri Jun 2 07:45:27 2006] CMD : minisat /work/tamura/csp2sat29478.cnf /work/tamura/csp2sat29478.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 2536457 7464148 | 845485 0 0 NaNQ | 0.000 % | ==============================================================================) restarts : 1 conflicts : 24 (3 /sec) decisions : 320 (37 /sec) propagations : 616261 (72130 /sec) inspects : 5783157 (676888 /sec) conflict literals : 465 (11.43 % deleted) CPU time : 8.54375 s SATISFIABLE VERIFY_CNF 1402 END : (10 seconds) [Fri Jun 2 07:45:37 2006] VERIFY_CNF 1402 CPU : 10.28 = 0.00999999999999091 + 0.01 + 10.13 + 0.13 # RESULT : makespan 1402 SATISFIABLE SHOW_RESULT 1402 BEGIN : [Fri Jun 2 07:45:37 2006] # ASSIGN : makespan 1402 # ASSIGN : s_0_0 0 # ASSIGN : s_0_1 65 # ASSIGN : s_0_2 93 # ASSIGN : s_0_3 167 # ASSIGN : s_0_4 214 # ASSIGN : s_0_5 265 # ASSIGN : s_0_6 406 # ASSIGN : s_0_7 479 # ASSIGN : s_0_8 532 # ASSIGN : s_0_9 545 # ASSIGN : s_0_10 653 # ASSIGN : s_0_11 688 # ASSIGN : s_0_12 747 # ASSIGN : s_0_13 1042 # ASSIGN : s_0_14 1192 # ASSIGN : s_1_0 94 # ASSIGN : s_1_1 158 # ASSIGN : s_1_2 219 # ASSIGN : s_1_3 302 # ASSIGN : s_1_4 346 # ASSIGN : s_1_5 352 # ASSIGN : s_1_6 413 # ASSIGN : s_1_7 586 # ASSIGN : s_1_8 593 # ASSIGN : s_1_9 887 # ASSIGN : s_1_10 908 # ASSIGN : s_1_11 931 # ASSIGN : s_1_12 941 # ASSIGN : s_1_13 1020 # ASSIGN : s_1_14 1330 # ASSIGN : s_2_0 56 # ASSIGN : s_2_1 129 # ASSIGN : s_2_2 211 # ASSIGN : s_2_3 234 # ASSIGN : s_2_4 296 # ASSIGN : s_2_5 384 # ASSIGN : s_2_6 405 # ASSIGN : s_2_7 470 # ASSIGN : s_2_8 558 # ASSIGN : s_2_9 611 # ASSIGN : s_2_10 692 # ASSIGN : s_2_11 785 # ASSIGN : s_2_12 946 # ASSIGN : s_2_13 1291 # ASSIGN : s_2_14 1324 # ASSIGN : s_3_0 8 # ASSIGN : s_3_1 20 # ASSIGN : s_3_2 71 # ASSIGN : s_3_3 178 # ASSIGN : s_3_4 193 # ASSIGN : s_3_5 306 # ASSIGN : s_3_6 404 # ASSIGN : s_3_7 498 # ASSIGN : s_3_8 540 # ASSIGN : s_3_9 648 # ASSIGN : s_3_10 683 # ASSIGN : s_3_11 754 # ASSIGN : s_3_12 782 # ASSIGN : s_3_13 788 # ASSIGN : s_3_14 1219 # ASSIGN : s_4_0 12 # ASSIGN : s_4_1 109 # ASSIGN : s_4_2 201 # ASSIGN : s_4_3 325 # ASSIGN : s_4_4 340 # ASSIGN : s_4_5 550 # ASSIGN : s_4_6 695 # ASSIGN : s_4_7 727 # ASSIGN : s_4_8 749 # ASSIGN : s_4_9 811 # ASSIGN : s_4_10 1009 # ASSIGN : s_4_11 1032 # ASSIGN : s_4_12 1218 # ASSIGN : s_4_13 1347 # ASSIGN : s_4_14 1371 # ASSIGN : s_5_0 86 # ASSIGN : s_5_1 247 # ASSIGN : s_5_2 335 # ASSIGN : s_5_3 428 # ASSIGN : s_5_4 441 # ASSIGN : s_5_5 485 # ASSIGN : s_5_6 566 # ASSIGN : s_5_7 658 # ASSIGN : s_5_8 672 # ASSIGN : s_5_9 774 # ASSIGN : s_5_10 791 # ASSIGN : s_5_11 1007 # ASSIGN : s_5_12 1211 # ASSIGN : s_5_13 1321 # ASSIGN : s_5_14 1353 # ASSIGN : s_6_0 297 # ASSIGN : s_6_1 312 # ASSIGN : s_6_2 394 # ASSIGN : s_6_3 551 # ASSIGN : s_6_4 626 # ASSIGN : s_6_5 698 # ASSIGN : s_6_6 791 # ASSIGN : s_6_7 890 # ASSIGN : s_6_8 916 # ASSIGN : s_6_9 972 # ASSIGN : s_6_10 1017 # ASSIGN : s_6_11 1085 # ASSIGN : s_6_12 1260 # ASSIGN : s_6_13 1279 # ASSIGN : s_6_14 1306 # ASSIGN : s_7_0 50 # ASSIGN : s_7_1 104 # ASSIGN : s_7_2 194 # ASSIGN : s_7_3 310 # ASSIGN : s_7_4 348 # ASSIGN : s_7_5 552 # ASSIGN : s_7_6 604 # ASSIGN : s_7_7 664 # ASSIGN : s_7_8 701 # ASSIGN : s_7_9 1042 # ASSIGN : s_7_10 1135 # ASSIGN : s_7_11 1195 # ASSIGN : s_7_12 1273 # ASSIGN : s_7_13 1296 # ASSIGN : s_7_14 1319 # ASSIGN : s_8_0 117 # ASSIGN : s_8_1 140 # ASSIGN : s_8_2 209 # ASSIGN : s_8_3 509 # ASSIGN : s_8_4 659 # ASSIGN : s_8_5 729 # ASSIGN : s_8_6 812 # ASSIGN : s_8_7 845 # ASSIGN : s_8_8 905 # ASSIGN : s_8_9 1017 # ASSIGN : s_8_10 1033 # ASSIGN : s_8_11 1063 # ASSIGN : s_8_12 1136 # ASSIGN : s_8_13 1231 # ASSIGN : s_8_14 1268 # ASSIGN : s_9_0 7 # ASSIGN : s_9_1 116 # ASSIGN : s_9_2 128 # ASSIGN : s_9_3 208 # ASSIGN : s_9_4 258 # ASSIGN : s_9_5 311 # ASSIGN : s_9_6 401 # ASSIGN : s_9_7 473 # ASSIGN : s_9_8 497 # ASSIGN : s_9_9 511 # ASSIGN : s_9_10 582 # ASSIGN : s_9_11 626 # ASSIGN : s_9_12 672 # ASSIGN : s_9_13 687 # ASSIGN : s_9_14 1279 # ASSIGN : s_10_0 134 # ASSIGN : s_10_1 188 # ASSIGN : s_10_2 235 # ASSIGN : s_10_3 369 # ASSIGN : s_10_4 433 # ASSIGN : s_10_5 510 # ASSIGN : s_10_6 526 # ASSIGN : s_10_7 532 # ASSIGN : s_10_8 876 # ASSIGN : s_10_9 969 # ASSIGN : s_10_10 1036 # ASSIGN : s_10_11 1118 # ASSIGN : s_10_12 1193 # ASSIGN : s_10_13 1265 # ASSIGN : s_10_14 1305 # ASSIGN : s_11_0 502 # ASSIGN : s_11_1 748 # ASSIGN : s_11_2 823 # ASSIGN : s_11_3 849 # ASSIGN : s_11_4 858 # ASSIGN : s_11_5 905 # ASSIGN : s_11_6 982 # ASSIGN : s_11_7 1061 # ASSIGN : s_11_8 1097 # ASSIGN : s_11_9 1127 # ASSIGN : s_11_10 1225 # ASSIGN : s_11_11 1304 # ASSIGN : s_11_12 1311 # ASSIGN : s_11_13 1366 # ASSIGN : s_11_14 1372 # ASSIGN : s_12_0 210 # ASSIGN : s_12_1 259 # ASSIGN : s_12_2 342 # ASSIGN : s_12_3 415 # ASSIGN : s_12_4 571 # ASSIGN : s_12_5 784 # ASSIGN : s_12_6 876 # ASSIGN : s_12_7 949 # ASSIGN : s_12_8 980 # ASSIGN : s_12_9 1015 # ASSIGN : s_12_10 1069 # ASSIGN : s_12_11 1090 # ASSIGN : s_12_12 1202 # ASSIGN : s_12_13 1274 # ASSIGN : s_12_14 1326 # ASSIGN : s_13_0 102 # ASSIGN : s_13_1 200 # ASSIGN : s_13_2 363 # ASSIGN : s_13_3 415 # ASSIGN : s_13_4 473 # ASSIGN : s_13_5 506 # ASSIGN : s_13_6 630 # ASSIGN : s_13_7 710 # ASSIGN : s_13_8 739 # ASSIGN : s_13_9 809 # ASSIGN : s_13_10 852 # ASSIGN : s_13_11 900 # ASSIGN : s_13_12 958 # ASSIGN : s_13_13 1003 # ASSIGN : s_13_14 1097 # ASSIGN : s_14_0 501 # ASSIGN : s_14_1 594 # ASSIGN : s_14_2 629 # ASSIGN : s_14_3 719 # ASSIGN : s_14_4 786 # ASSIGN : s_14_5 800 # ASSIGN : s_14_6 823 # ASSIGN : s_14_7 844 # ASSIGN : s_14_8 862 # ASSIGN : s_14_9 949 # ASSIGN : s_14_10 1076 # ASSIGN : s_14_11 1102 # ASSIGN : s_14_12 1138 # ASSIGN : s_14_13 1246 # ASSIGN : s_14_14 1330 SHOW_RESULT 1402 END : 1402 (2 seconds) [Fri Jun 2 07:45:39 2006] SHOW_RESULT 1402 CPU : 1.12000000000001 = 1.11000000000001 + 0.01 + 0 + 0 # BOUND : makespan 1027 1402 MODIFY_CNF 1214 BEGIN : [Fri Jun 2 07:45:39 2006] MODIFY_CNF 1214 END : 148956411 bytes (0 seconds) [Fri Jun 2 07:45:39 2006] MODIFY_CNF 1214 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1214 BEGIN : [Fri Jun 2 07:45:39 2006] CMD : minisat /work/tamura/csp2sat29478.cnf /work/tamura/csp2sat29478.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1709065 5024791 | 569688 0 0 NaNQ | 0.000 % | | 100 | 1709065 5024791 | 626656 100 1277 12.8 | 74.377 % | | 250 | 1709065 5024791 | 689322 250 2859 11.4 | 74.377 % | | 475 | 1709065 5024791 | 758254 475 5591 11.8 | 74.377 % | | 813 | 1709065 5024791 | 834080 813 11014 13.5 | 74.377 % | | 1320 | 1709065 5024791 | 917488 1320 17921 13.6 | 74.377 % | | 2079 | 1709065 5024791 | 1009237 2079 30455 14.6 | 74.377 % | | 3218 | 1709065 5024791 | 1110160 3218 46628 14.5 | 74.377 % | | 4927 | 1709065 5024791 | 1221176 4927 69757 14.2 | 74.377 % | | 7490 | 1709065 5024791 | 1343294 7490 111698 14.9 | 74.377 % | | 11334 | 1709065 5024791 | 1477623 11334 190345 16.8 | 74.377 % | | 17100 | 1709065 5024791 | 1625386 17100 323348 18.9 | 74.377 % | | 25749 | 1705784 5014992 | 1787924 18339 316207 17.2 | 74.389 % | | 38725 | 1596775 4692680 | 1966717 16473 246133 14.9 | 75.771 % | ==============================================================================) restarts : 14 conflicts : 42325 (184 /sec) decisions : 58356 (254 /sec) propagations : 423598113 (1840188 /sec) inspects : 3376328014 (14667390 /sec) conflict literals : 827441 (39.55 % deleted) CPU time : 230.193 s UNSATISFIABLE VERIFY_CNF 1214 END : (232 seconds) [Fri Jun 2 07:49:31 2006] VERIFY_CNF 1214 CPU : 231.89 = 0.00999999999999091 + 0.03 + 231.31 + 0.54 # RESULT : makespan 1214 UNSATISFIABLE # BOUND : makespan 1215 1402 MODIFY_CNF 1308 BEGIN : [Fri Jun 2 07:49:31 2006] MODIFY_CNF 1308 END : 148956411 bytes (0 seconds) [Fri Jun 2 07:49:31 2006] MODIFY_CNF 1308 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1308 BEGIN : [Fri Jun 2 07:49:31 2006] CMD : minisat /work/tamura/csp2sat29478.cnf /work/tamura/csp2sat29478.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 2115635 6223077 | 705211 0 0 NaNQ | 0.000 % | ==============================================================================) restarts : 1 conflicts : 11 (1 /sec) decisions : 231 (25 /sec) propagations : 457747 (50394 /sec) inspects : 3886986 (427928 /sec) conflict literals : 100 (6.54 % deleted) CPU time : 9.08328 s SATISFIABLE VERIFY_CNF 1308 END : (11 seconds) [Fri Jun 2 07:49:42 2006] VERIFY_CNF 1308 CPU : 10.77 = 0 + 0.02 + 10.59 + 0.16 # RESULT : makespan 1308 SATISFIABLE SHOW_RESULT 1308 BEGIN : [Fri Jun 2 07:49:42 2006] # ASSIGN : makespan 1308 # ASSIGN : s_0_0 55 # ASSIGN : s_0_1 253 # ASSIGN : s_0_2 421 # ASSIGN : s_0_3 554 # ASSIGN : s_0_4 587 # ASSIGN : s_0_5 638 # ASSIGN : s_0_6 745 # ASSIGN : s_0_7 818 # ASSIGN : s_0_8 850 # ASSIGN : s_0_9 863 # ASSIGN : s_0_10 944 # ASSIGN : s_0_11 979 # ASSIGN : s_0_12 1038 # ASSIGN : s_0_13 1076 # ASSIGN : s_0_14 1168 # ASSIGN : s_1_0 126 # ASSIGN : s_1_1 190 # ASSIGN : s_1_2 243 # ASSIGN : s_1_3 326 # ASSIGN : s_1_4 359 # ASSIGN : s_1_5 707 # ASSIGN : s_1_6 866 # ASSIGN : s_1_7 938 # ASSIGN : s_1_8 946 # ASSIGN : s_1_9 1036 # ASSIGN : s_1_10 1057 # ASSIGN : s_1_11 1080 # ASSIGN : s_1_12 1129 # ASSIGN : s_1_13 1168 # ASSIGN : s_1_14 1236 # ASSIGN : s_2_0 12 # ASSIGN : s_2_1 85 # ASSIGN : s_2_2 167 # ASSIGN : s_2_3 244 # ASSIGN : s_2_4 306 # ASSIGN : s_2_5 394 # ASSIGN : s_2_6 415 # ASSIGN : s_2_7 480 # ASSIGN : s_2_8 588 # ASSIGN : s_2_9 641 # ASSIGN : s_2_10 722 # ASSIGN : s_2_11 815 # ASSIGN : s_2_12 1045 # ASSIGN : s_2_13 1197 # ASSIGN : s_2_14 1230 # ASSIGN : s_3_0 13 # ASSIGN : s_3_1 32 # ASSIGN : s_3_2 112 # ASSIGN : s_3_3 145 # ASSIGN : s_3_4 160 # ASSIGN : s_3_5 388 # ASSIGN : s_3_6 486 # ASSIGN : s_3_7 661 # ASSIGN : s_3_8 735 # ASSIGN : s_3_9 868 # ASSIGN : s_3_10 892 # ASSIGN : s_3_11 945 # ASSIGN : s_3_12 1090 # ASSIGN : s_3_13 1096 # ASSIGN : s_3_14 1195 # ASSIGN : s_4_0 3 # ASSIGN : s_4_1 100 # ASSIGN : s_4_2 120 # ASSIGN : s_4_3 216 # ASSIGN : s_4_4 232 # ASSIGN : s_4_5 313 # ASSIGN : s_4_6 361 # ASSIGN : s_4_7 393 # ASSIGN : s_4_8 438 # ASSIGN : s_4_9 491 # ASSIGN : s_4_10 663 # ASSIGN : s_4_11 686 # ASSIGN : s_4_12 772 # ASSIGN : s_4_13 870 # ASSIGN : s_4_14 1117 # ASSIGN : s_5_0 25 # ASSIGN : s_5_1 119 # ASSIGN : s_5_2 207 # ASSIGN : s_5_3 300 # ASSIGN : s_5_4 315 # ASSIGN : s_5_5 360 # ASSIGN : s_5_6 455 # ASSIGN : s_5_7 549 # ASSIGN : s_5_8 580 # ASSIGN : s_5_9 760 # ASSIGN : s_5_10 777 # ASSIGN : s_5_11 910 # ASSIGN : s_5_12 1148 # ASSIGN : s_5_13 1227 # ASSIGN : s_5_14 1259 # ASSIGN : s_6_0 15 # ASSIGN : s_6_1 30 # ASSIGN : s_6_2 195 # ASSIGN : s_6_3 305 # ASSIGN : s_6_4 358 # ASSIGN : s_6_5 439 # ASSIGN : s_6_6 488 # ASSIGN : s_6_7 637 # ASSIGN : s_6_8 663 # ASSIGN : s_6_9 719 # ASSIGN : s_6_10 826 # ASSIGN : s_6_11 894 # ASSIGN : s_6_12 945 # ASSIGN : s_6_13 953 # ASSIGN : s_6_14 980 # ASSIGN : s_7_0 180 # ASSIGN : s_7_1 262 # ASSIGN : s_7_2 286 # ASSIGN : s_7_3 300 # ASSIGN : s_7_4 338 # ASSIGN : s_7_5 374 # ASSIGN : s_7_6 426 # ASSIGN : s_7_7 513 # ASSIGN : s_7_8 550 # ASSIGN : s_7_9 598 # ASSIGN : s_7_10 691 # ASSIGN : s_7_11 800 # ASSIGN : s_7_12 897 # ASSIGN : s_7_13 920 # ASSIGN : s_7_14 1225 # ASSIGN : s_8_0 2 # ASSIGN : s_8_1 14 # ASSIGN : s_8_2 83 # ASSIGN : s_8_3 369 # ASSIGN : s_8_4 481 # ASSIGN : s_8_5 585 # ASSIGN : s_8_6 673 # ASSIGN : s_8_7 706 # ASSIGN : s_8_8 751 # ASSIGN : s_8_9 831 # ASSIGN : s_8_10 862 # ASSIGN : s_8_11 937 # ASSIGN : s_8_12 1010 # ASSIGN : s_8_13 1069 # ASSIGN : s_8_14 1106 # ASSIGN : s_9_0 0 # ASSIGN : s_9_1 107 # ASSIGN : s_9_2 151 # ASSIGN : s_9_3 231 # ASSIGN : s_9_4 281 # ASSIGN : s_9_5 329 # ASSIGN : s_9_6 419 # ASSIGN : s_9_7 494 # ASSIGN : s_9_8 518 # ASSIGN : s_9_9 532 # ASSIGN : s_9_10 603 # ASSIGN : s_9_11 647 # ASSIGN : s_9_12 698 # ASSIGN : s_9_13 713 # ASSIGN : s_9_14 1216 # ASSIGN : s_10_0 33 # ASSIGN : s_10_1 87 # ASSIGN : s_10_2 109 # ASSIGN : s_10_3 170 # ASSIGN : s_10_4 234 # ASSIGN : s_10_5 307 # ASSIGN : s_10_6 323 # ASSIGN : s_10_7 392 # ASSIGN : s_10_8 509 # ASSIGN : s_10_9 624 # ASSIGN : s_10_10 764 # ASSIGN : s_10_11 846 # ASSIGN : s_10_12 948 # ASSIGN : s_10_13 1171 # ASSIGN : s_10_14 1211 # ASSIGN : s_11_0 9 # ASSIGN : s_11_1 602 # ASSIGN : s_11_2 671 # ASSIGN : s_11_3 693 # ASSIGN : s_11_4 702 # ASSIGN : s_11_5 749 # ASSIGN : s_11_6 828 # ASSIGN : s_11_7 907 # ASSIGN : s_11_8 943 # ASSIGN : s_11_9 973 # ASSIGN : s_11_10 1131 # ASSIGN : s_11_11 1210 # ASSIGN : s_11_12 1217 # ASSIGN : s_11_13 1272 # ASSIGN : s_11_14 1278 # ASSIGN : s_12_0 307 # ASSIGN : s_12_1 356 # ASSIGN : s_12_2 469 # ASSIGN : s_12_3 585 # ASSIGN : s_12_4 667 # ASSIGN : s_12_5 774 # ASSIGN : s_12_6 871 # ASSIGN : s_12_7 944 # ASSIGN : s_12_8 975 # ASSIGN : s_12_9 1010 # ASSIGN : s_12_10 1064 # ASSIGN : s_12_11 1071 # ASSIGN : s_12_12 1108 # ASSIGN : s_12_13 1180 # ASSIGN : s_12_14 1232 # ASSIGN : s_13_0 101 # ASSIGN : s_13_1 210 # ASSIGN : s_13_2 248 # ASSIGN : s_13_3 365 # ASSIGN : s_13_4 391 # ASSIGN : s_13_5 430 # ASSIGN : s_13_6 636 # ASSIGN : s_13_7 716 # ASSIGN : s_13_8 759 # ASSIGN : s_13_9 829 # ASSIGN : s_13_10 872 # ASSIGN : s_13_11 921 # ASSIGN : s_13_12 1013 # ASSIGN : s_13_13 1058 # ASSIGN : s_13_14 1212 # ASSIGN : s_14_0 97 # ASSIGN : s_14_1 199 # ASSIGN : s_14_2 216 # ASSIGN : s_14_3 428 # ASSIGN : s_14_4 495 # ASSIGN : s_14_5 509 # ASSIGN : s_14_6 542 # ASSIGN : s_14_7 563 # ASSIGN : s_14_8 581 # ASSIGN : s_14_9 651 # ASSIGN : s_14_10 858 # ASSIGN : s_14_11 884 # ASSIGN : s_14_12 920 # ASSIGN : s_14_13 1152 # ASSIGN : s_14_14 1236 SHOW_RESULT 1308 END : 1308 (1 seconds) [Fri Jun 2 07:49:43 2006] SHOW_RESULT 1308 CPU : 1.15000000000003 = 1.15000000000003 + 0 + 0 + 0 # BOUND : makespan 1215 1308 MODIFY_CNF 1261 BEGIN : [Fri Jun 2 07:49:43 2006] MODIFY_CNF 1261 END : 148956411 bytes (0 seconds) [Fri Jun 2 07:49:43 2006] MODIFY_CNF 1261 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1261 BEGIN : [Fri Jun 2 07:49:43 2006] CMD : minisat /work/tamura/csp2sat29478.cnf /work/tamura/csp2sat29478.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1921711 5651995 | 640570 0 0 NaNQ | 0.000 % | | 102 | 1921711 5651995 | 704627 102 2095 20.5 | 71.710 % | | 252 | 1921711 5651995 | 775089 252 4472 17.7 | 71.710 % | ==============================================================================) restarts : 3 conflicts : 393 (35 /sec) decisions : 991 (87 /sec) propagations : 4103559 (360880 /sec) inspects : 38718648 (3405041 /sec) conflict literals : 6314 (17.87 % deleted) CPU time : 11.371 s SATISFIABLE VERIFY_CNF 1261 END : (14 seconds) [Fri Jun 2 07:49:57 2006] VERIFY_CNF 1261 CPU : 12.98 = 0 + 0.0299999999999999 + 12.79 + 0.16 # RESULT : makespan 1261 SATISFIABLE SHOW_RESULT 1261 BEGIN : [Fri Jun 2 07:49:57 2006] # ASSIGN : makespan 1261 # ASSIGN : s_0_0 65 # ASSIGN : s_0_1 131 # ASSIGN : s_0_2 189 # ASSIGN : s_0_3 264 # ASSIGN : s_0_4 297 # ASSIGN : s_0_5 397 # ASSIGN : s_0_6 472 # ASSIGN : s_0_7 545 # ASSIGN : s_0_8 673 # ASSIGN : s_0_9 706 # ASSIGN : s_0_10 787 # ASSIGN : s_0_11 822 # ASSIGN : s_0_12 1072 # ASSIGN : s_0_13 1110 # ASSIGN : s_0_14 1204 # ASSIGN : s_1_0 148 # ASSIGN : s_1_1 212 # ASSIGN : s_1_2 265 # ASSIGN : s_1_3 348 # ASSIGN : s_1_4 474 # ASSIGN : s_1_5 525 # ASSIGN : s_1_6 834 # ASSIGN : s_1_7 906 # ASSIGN : s_1_8 938 # ASSIGN : s_1_9 1028 # ASSIGN : s_1_10 1049 # ASSIGN : s_1_11 1072 # ASSIGN : s_1_12 1082 # ASSIGN : s_1_13 1121 # ASSIGN : s_1_14 1189 # ASSIGN : s_2_0 24 # ASSIGN : s_2_1 97 # ASSIGN : s_2_2 179 # ASSIGN : s_2_3 202 # ASSIGN : s_2_4 268 # ASSIGN : s_2_5 356 # ASSIGN : s_2_6 377 # ASSIGN : s_2_7 453 # ASSIGN : s_2_8 542 # ASSIGN : s_2_9 595 # ASSIGN : s_2_10 676 # ASSIGN : s_2_11 769 # ASSIGN : s_2_12 1043 # ASSIGN : s_2_13 1150 # ASSIGN : s_2_14 1183 # ASSIGN : s_3_0 5 # ASSIGN : s_3_1 49 # ASSIGN : s_3_2 100 # ASSIGN : s_3_3 142 # ASSIGN : s_3_4 177 # ASSIGN : s_3_5 268 # ASSIGN : s_3_6 366 # ASSIGN : s_3_7 460 # ASSIGN : s_3_8 523 # ASSIGN : s_3_9 652 # ASSIGN : s_3_10 694 # ASSIGN : s_3_11 830 # ASSIGN : s_3_12 897 # ASSIGN : s_3_13 903 # ASSIGN : s_3_14 1002 # ASSIGN : s_4_0 26 # ASSIGN : s_4_1 123 # ASSIGN : s_4_2 130 # ASSIGN : s_4_3 459 # ASSIGN : s_4_4 491 # ASSIGN : s_4_5 564 # ASSIGN : s_4_6 607 # ASSIGN : s_4_7 639 # ASSIGN : s_4_8 872 # ASSIGN : s_4_9 925 # ASSIGN : s_4_10 1019 # ASSIGN : s_4_11 1042 # ASSIGN : s_4_12 1128 # ASSIGN : s_4_13 1206 # ASSIGN : s_4_14 1230 # ASSIGN : s_5_0 17 # ASSIGN : s_5_1 268 # ASSIGN : s_5_2 517 # ASSIGN : s_5_3 610 # ASSIGN : s_5_4 631 # ASSIGN : s_5_5 675 # ASSIGN : s_5_6 818 # ASSIGN : s_5_7 881 # ASSIGN : s_5_8 909 # ASSIGN : s_5_9 976 # ASSIGN : s_5_10 993 # ASSIGN : s_5_11 1104 # ASSIGN : s_5_12 1139 # ASSIGN : s_5_13 1207 # ASSIGN : s_5_14 1212 # ASSIGN : s_6_0 3 # ASSIGN : s_6_1 18 # ASSIGN : s_6_2 103 # ASSIGN : s_6_3 124 # ASSIGN : s_6_4 260 # ASSIGN : s_6_5 332 # ASSIGN : s_6_6 381 # ASSIGN : s_6_7 480 # ASSIGN : s_6_8 506 # ASSIGN : s_6_9 577 # ASSIGN : s_6_10 622 # ASSIGN : s_6_11 690 # ASSIGN : s_6_12 741 # ASSIGN : s_6_13 749 # ASSIGN : s_6_14 776 # ASSIGN : s_7_0 43 # ASSIGN : s_7_1 133 # ASSIGN : s_7_2 157 # ASSIGN : s_7_3 171 # ASSIGN : s_7_4 209 # ASSIGN : s_7_5 245 # ASSIGN : s_7_6 313 # ASSIGN : s_7_7 368 # ASSIGN : s_7_8 405 # ASSIGN : s_7_9 514 # ASSIGN : s_7_10 709 # ASSIGN : s_7_11 1012 # ASSIGN : s_7_12 1082 # ASSIGN : s_7_13 1105 # ASSIGN : s_7_14 1178 # ASSIGN : s_8_0 31 # ASSIGN : s_8_1 83 # ASSIGN : s_8_2 152 # ASSIGN : s_8_3 226 # ASSIGN : s_8_4 249 # ASSIGN : s_8_5 281 # ASSIGN : s_8_6 379 # ASSIGN : s_8_7 412 # ASSIGN : s_8_8 457 # ASSIGN : s_8_9 527 # ASSIGN : s_8_10 565 # ASSIGN : s_8_11 735 # ASSIGN : s_8_12 808 # ASSIGN : s_8_13 867 # ASSIGN : s_8_14 940 # ASSIGN : s_9_0 61 # ASSIGN : s_9_1 171 # ASSIGN : s_9_2 183 # ASSIGN : s_9_3 263 # ASSIGN : s_9_4 368 # ASSIGN : s_9_5 416 # ASSIGN : s_9_6 550 # ASSIGN : s_9_7 623 # ASSIGN : s_9_8 647 # ASSIGN : s_9_9 661 # ASSIGN : s_9_10 732 # ASSIGN : s_9_11 858 # ASSIGN : s_9_12 904 # ASSIGN : s_9_13 919 # ASSIGN : s_9_14 980 # ASSIGN : s_10_0 191 # ASSIGN : s_10_1 423 # ASSIGN : s_10_2 445 # ASSIGN : s_10_3 506 # ASSIGN : s_10_4 552 # ASSIGN : s_10_5 625 # ASSIGN : s_10_6 641 # ASSIGN : s_10_7 647 # ASSIGN : s_10_8 741 # ASSIGN : s_10_9 846 # ASSIGN : s_10_10 913 # ASSIGN : s_10_11 967 # ASSIGN : s_10_12 1078 # ASSIGN : s_10_13 1124 # ASSIGN : s_10_14 1164 # ASSIGN : s_11_0 176 # ASSIGN : s_11_1 277 # ASSIGN : s_11_2 313 # ASSIGN : s_11_3 335 # ASSIGN : s_11_4 344 # ASSIGN : s_11_5 391 # ASSIGN : s_11_6 562 # ASSIGN : s_11_7 650 # ASSIGN : s_11_8 686 # ASSIGN : s_11_9 732 # ASSIGN : s_11_10 914 # ASSIGN : s_11_11 1163 # ASSIGN : s_11_12 1170 # ASSIGN : s_11_13 1225 # ASSIGN : s_11_14 1231 # ASSIGN : s_12_0 12 # ASSIGN : s_12_1 104 # ASSIGN : s_12_2 187 # ASSIGN : s_12_3 363 # ASSIGN : s_12_4 468 # ASSIGN : s_12_5 566 # ASSIGN : s_12_6 658 # ASSIGN : s_12_7 731 # ASSIGN : s_12_8 762 # ASSIGN : s_12_9 797 # ASSIGN : s_12_10 851 # ASSIGN : s_12_11 858 # ASSIGN : s_12_12 895 # ASSIGN : s_12_13 1079 # ASSIGN : s_12_14 1131 # ASSIGN : s_13_0 33 # ASSIGN : s_13_1 168 # ASSIGN : s_13_2 280 # ASSIGN : s_13_3 337 # ASSIGN : s_13_4 363 # ASSIGN : s_13_5 426 # ASSIGN : s_13_6 465 # ASSIGN : s_13_7 548 # ASSIGN : s_13_8 577 # ASSIGN : s_13_9 673 # ASSIGN : s_13_10 716 # ASSIGN : s_13_11 764 # ASSIGN : s_13_12 822 # ASSIGN : s_13_13 984 # ASSIGN : s_13_14 1165 # ASSIGN : s_14_0 89 # ASSIGN : s_14_1 159 # ASSIGN : s_14_2 178 # ASSIGN : s_14_3 301 # ASSIGN : s_14_4 398 # ASSIGN : s_14_5 442 # ASSIGN : s_14_6 482 # ASSIGN : s_14_7 503 # ASSIGN : s_14_8 521 # ASSIGN : s_14_9 574 # ASSIGN : s_14_10 723 # ASSIGN : s_14_11 761 # ASSIGN : s_14_12 926 # ASSIGN : s_14_13 1078 # ASSIGN : s_14_14 1162 SHOW_RESULT 1261 END : 1261 (1 seconds) [Fri Jun 2 07:49:58 2006] SHOW_RESULT 1261 CPU : 1.14 = 1.13 + 0.01 + 0 + 0 # BOUND : makespan 1215 1261 MODIFY_CNF 1238 BEGIN : [Fri Jun 2 07:49:58 2006] MODIFY_CNF 1238 END : 148956411 bytes (0 seconds) [Fri Jun 2 07:49:58 2006] MODIFY_CNF 1238 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1238 BEGIN : [Fri Jun 2 07:49:58 2006] CMD : minisat /work/tamura/csp2sat29478.cnf /work/tamura/csp2sat29478.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1808764 5318418 | 602921 0 0 NaNQ | 0.000 % | | 102 | 1808764 5318418 | 663213 102 1769 17.3 | 73.018 % | | 252 | 1808764 5318418 | 729534 252 3050 12.1 | 73.018 % | | 477 | 1808764 5318418 | 802487 477 5603 11.7 | 73.018 % | | 814 | 1808764 5318418 | 882736 814 11756 14.4 | 73.018 % | | 1322 | 1808764 5318418 | 971010 1322 18983 14.4 | 73.018 % | | 2081 | 1808764 5318418 | 1068111 2081 28851 13.9 | 73.018 % | | 3220 | 1808764 5318418 | 1174922 3220 53969 16.8 | 73.018 % | | 4928 | 1808764 5318418 | 1292414 4928 80837 16.4 | 73.018 % | | 7490 | 1808764 5318418 | 1421656 7490 125128 16.7 | 73.018 % | ==============================================================================) restarts : 10 conflicts : 9002 (151 /sec) decisions : 14084 (237 /sec) propagations : 97656332 (1640346 /sec) inspects : 838656503 (14087021 /sec) conflict literals : 166938 (30.84 % deleted) CPU time : 59.534 s SATISFIABLE VERIFY_CNF 1238 END : (61 seconds) [Fri Jun 2 07:50:59 2006] VERIFY_CNF 1238 CPU : 61.5 = 0.00999999999999091 + 0.03 + 60.91 + 0.55 # RESULT : makespan 1238 SATISFIABLE SHOW_RESULT 1238 BEGIN : [Fri Jun 2 07:50:59 2006] # ASSIGN : makespan 1238 # ASSIGN : s_0_0 226 # ASSIGN : s_0_1 291 # ASSIGN : s_0_2 336 # ASSIGN : s_0_3 457 # ASSIGN : s_0_4 511 # ASSIGN : s_0_5 619 # ASSIGN : s_0_6 738 # ASSIGN : s_0_7 811 # ASSIGN : s_0_8 850 # ASSIGN : s_0_9 863 # ASSIGN : s_0_10 944 # ASSIGN : s_0_11 979 # ASSIGN : s_0_12 1049 # ASSIGN : s_0_13 1087 # ASSIGN : s_0_14 1211 # ASSIGN : s_1_0 183 # ASSIGN : s_1_1 247 # ASSIGN : s_1_2 300 # ASSIGN : s_1_3 478 # ASSIGN : s_1_4 655 # ASSIGN : s_1_5 734 # ASSIGN : s_1_6 786 # ASSIGN : s_1_7 911 # ASSIGN : s_1_8 918 # ASSIGN : s_1_9 1008 # ASSIGN : s_1_10 1029 # ASSIGN : s_1_11 1052 # ASSIGN : s_1_12 1062 # ASSIGN : s_1_13 1117 # ASSIGN : s_1_14 1166 # ASSIGN : s_2_0 7 # ASSIGN : s_2_1 80 # ASSIGN : s_2_2 170 # ASSIGN : s_2_3 193 # ASSIGN : s_2_4 257 # ASSIGN : s_2_5 345 # ASSIGN : s_2_6 366 # ASSIGN : s_2_7 431 # ASSIGN : s_2_8 561 # ASSIGN : s_2_9 614 # ASSIGN : s_2_10 695 # ASSIGN : s_2_11 826 # ASSIGN : s_2_12 967 # ASSIGN : s_2_13 1132 # ASSIGN : s_2_14 1160 # ASSIGN : s_3_0 16 # ASSIGN : s_3_1 29 # ASSIGN : s_3_2 87 # ASSIGN : s_3_3 120 # ASSIGN : s_3_4 135 # ASSIGN : s_3_5 367 # ASSIGN : s_3_6 465 # ASSIGN : s_3_7 573 # ASSIGN : s_3_8 585 # ASSIGN : s_3_9 671 # ASSIGN : s_3_10 903 # ASSIGN : s_3_11 973 # ASSIGN : s_3_12 1046 # ASSIGN : s_3_13 1063 # ASSIGN : s_3_14 1170 # ASSIGN : s_4_0 6 # ASSIGN : s_4_1 103 # ASSIGN : s_4_2 110 # ASSIGN : s_4_3 206 # ASSIGN : s_4_4 298 # ASSIGN : s_4_5 410 # ASSIGN : s_4_6 543 # ASSIGN : s_4_7 575 # ASSIGN : s_4_8 627 # ASSIGN : s_4_9 694 # ASSIGN : s_4_10 788 # ASSIGN : s_4_11 811 # ASSIGN : s_4_12 951 # ASSIGN : s_4_13 1183 # ASSIGN : s_4_14 1207 # ASSIGN : s_5_0 98 # ASSIGN : s_5_1 216 # ASSIGN : s_5_2 304 # ASSIGN : s_5_3 397 # ASSIGN : s_5_4 410 # ASSIGN : s_5_5 454 # ASSIGN : s_5_6 520 # ASSIGN : s_5_7 615 # ASSIGN : s_5_8 629 # ASSIGN : s_5_9 696 # ASSIGN : s_5_10 713 # ASSIGN : s_5_11 932 # ASSIGN : s_5_12 978 # ASSIGN : s_5_13 1058 # ASSIGN : s_5_14 1189 # ASSIGN : s_6_0 211 # ASSIGN : s_6_1 268 # ASSIGN : s_6_2 350 # ASSIGN : s_6_3 371 # ASSIGN : s_6_4 424 # ASSIGN : s_6_5 496 # ASSIGN : s_6_6 562 # ASSIGN : s_6_7 661 # ASSIGN : s_6_8 710 # ASSIGN : s_6_9 766 # ASSIGN : s_6_10 876 # ASSIGN : s_6_11 952 # ASSIGN : s_6_12 1028 # ASSIGN : s_6_13 1090 # ASSIGN : s_6_14 1142 # ASSIGN : s_7_0 9 # ASSIGN : s_7_1 63 # ASSIGN : s_7_2 88 # ASSIGN : s_7_3 102 # ASSIGN : s_7_4 140 # ASSIGN : s_7_5 191 # ASSIGN : s_7_6 243 # ASSIGN : s_7_7 330 # ASSIGN : s_7_8 383 # ASSIGN : s_7_9 450 # ASSIGN : s_7_10 605 # ASSIGN : s_7_11 783 # ASSIGN : s_7_12 853 # ASSIGN : s_7_13 928 # ASSIGN : s_7_14 1049 # ASSIGN : s_8_0 68 # ASSIGN : s_8_1 162 # ASSIGN : s_8_2 231 # ASSIGN : s_8_3 348 # ASSIGN : s_8_4 426 # ASSIGN : s_8_5 530 # ASSIGN : s_8_6 654 # ASSIGN : s_8_7 687 # ASSIGN : s_8_8 732 # ASSIGN : s_8_9 796 # ASSIGN : s_8_10 871 # ASSIGN : s_8_11 930 # ASSIGN : s_8_12 1003 # ASSIGN : s_8_13 1071 # ASSIGN : s_8_14 1108 # ASSIGN : s_9_0 89 # ASSIGN : s_9_1 176 # ASSIGN : s_9_2 188 # ASSIGN : s_9_3 269 # ASSIGN : s_9_4 319 # ASSIGN : s_9_5 367 # ASSIGN : s_9_6 458 # ASSIGN : s_9_7 545 # ASSIGN : s_9_8 583 # ASSIGN : s_9_9 597 # ASSIGN : s_9_10 669 # ASSIGN : s_9_11 894 # ASSIGN : s_9_12 1039 # ASSIGN : s_9_13 1054 # ASSIGN : s_9_14 1115 # ASSIGN : s_10_0 4 # ASSIGN : s_10_1 58 # ASSIGN : s_10_2 80 # ASSIGN : s_10_3 160 # ASSIGN : s_10_4 235 # ASSIGN : s_10_5 308 # ASSIGN : s_10_6 324 # ASSIGN : s_10_7 371 # ASSIGN : s_10_8 526 # ASSIGN : s_10_9 665 # ASSIGN : s_10_10 843 # ASSIGN : s_10_11 897 # ASSIGN : s_10_12 1055 # ASSIGN : s_10_13 1101 # ASSIGN : s_10_14 1141 # ASSIGN : s_11_0 115 # ASSIGN : s_11_1 207 # ASSIGN : s_11_2 247 # ASSIGN : s_11_3 308 # ASSIGN : s_11_4 317 # ASSIGN : s_11_5 381 # ASSIGN : s_11_6 490 # ASSIGN : s_11_7 569 # ASSIGN : s_11_8 638 # ASSIGN : s_11_9 668 # ASSIGN : s_11_10 880 # ASSIGN : s_11_11 972 # ASSIGN : s_11_12 1010 # ASSIGN : s_11_13 1065 # ASSIGN : s_11_14 1078 # ASSIGN : s_12_0 9 # ASSIGN : s_12_1 79 # ASSIGN : s_12_2 162 # ASSIGN : s_12_3 438 # ASSIGN : s_12_4 612 # ASSIGN : s_12_5 694 # ASSIGN : s_12_6 798 # ASSIGN : s_12_7 874 # ASSIGN : s_12_8 905 # ASSIGN : s_12_9 940 # ASSIGN : s_12_10 994 # ASSIGN : s_12_11 1001 # ASSIGN : s_12_12 1038 # ASSIGN : s_12_13 1110 # ASSIGN : s_12_14 1162 # ASSIGN : s_13_0 0 # ASSIGN : s_13_1 135 # ASSIGN : s_13_2 169 # ASSIGN : s_13_3 221 # ASSIGN : s_13_4 336 # ASSIGN : s_13_5 364 # ASSIGN : s_13_6 450 # ASSIGN : s_13_7 530 # ASSIGN : s_13_8 559 # ASSIGN : s_13_9 647 # ASSIGN : s_13_10 690 # ASSIGN : s_13_11 738 # ASSIGN : s_13_12 813 # ASSIGN : s_13_13 858 # ASSIGN : s_13_14 959 # ASSIGN : s_14_0 28 # ASSIGN : s_14_1 98 # ASSIGN : s_14_2 141 # ASSIGN : s_14_3 255 # ASSIGN : s_14_4 322 # ASSIGN : s_14_5 343 # ASSIGN : s_14_6 403 # ASSIGN : s_14_7 435 # ASSIGN : s_14_8 453 # ASSIGN : s_14_9 501 # ASSIGN : s_14_10 712 # ASSIGN : s_14_11 823 # ASSIGN : s_14_12 859 # ASSIGN : s_14_13 952 # ASSIGN : s_14_14 1036 SHOW_RESULT 1238 END : 1238 (1 seconds) [Fri Jun 2 07:51:00 2006] SHOW_RESULT 1238 CPU : 1.13 = 1.13 + 0 + 0 + 0 # BOUND : makespan 1215 1238 MODIFY_CNF 1226 BEGIN : [Fri Jun 2 07:51:00 2006] MODIFY_CNF 1226 END : 148956411 bytes (0 seconds) [Fri Jun 2 07:51:00 2006] MODIFY_CNF 1226 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1226 BEGIN : [Fri Jun 2 07:51:00 2006] CMD : minisat /work/tamura/csp2sat29478.cnf /work/tamura/csp2sat29478.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1759659 5173838 | 586553 0 0 NaNQ | 0.000 % | | 101 | 1759659 5173838 | 645208 101 993 9.8 | 73.697 % | | 251 | 1759659 5173838 | 709729 251 2920 11.6 | 73.697 % | | 477 | 1759659 5173838 | 780702 477 5493 11.5 | 73.697 % | | 814 | 1759659 5173838 | 858772 814 9468 11.6 | 73.697 % | | 1320 | 1759659 5173838 | 944649 1320 16233 12.3 | 73.697 % | | 2080 | 1759659 5173838 | 1039114 2080 26690 12.8 | 73.697 % | | 3219 | 1759659 5173838 | 1143025 3219 48165 15.0 | 73.697 % | | 4929 | 1759659 5173838 | 1257328 4929 75739 15.4 | 73.697 % | | 7491 | 1759659 5173838 | 1383061 7491 137153 18.3 | 73.697 % | | 11335 | 1759659 5173838 | 1521367 11335 190829 16.8 | 73.697 % | | 17101 | 1759659 5173838 | 1673504 17101 309235 18.1 | 73.697 % | | 25751 | 1759659 5173838 | 1840854 25751 484134 18.8 | 73.697 % | ==============================================================================) restarts : 13 conflicts : 38383 (183 /sec) decisions : 53160 (253 /sec) propagations : 379173880 (1805664 /sec) inspects : 3199576623 (15236707 /sec) conflict literals : 768929 (35.81 % deleted) CPU time : 209.991 s SATISFIABLE VERIFY_CNF 1226 END : (213 seconds) [Fri Jun 2 07:54:33 2006] VERIFY_CNF 1226 CPU : 211.59 = 0 + 0.03 + 211.4 + 0.16 # RESULT : makespan 1226 SATISFIABLE SHOW_RESULT 1226 BEGIN : [Fri Jun 2 07:54:33 2006] # ASSIGN : makespan 1226 # ASSIGN : s_0_0 41 # ASSIGN : s_0_1 218 # ASSIGN : s_0_2 297 # ASSIGN : s_0_3 371 # ASSIGN : s_0_4 404 # ASSIGN : s_0_5 455 # ASSIGN : s_0_6 642 # ASSIGN : s_0_7 715 # ASSIGN : s_0_8 763 # ASSIGN : s_0_9 776 # ASSIGN : s_0_10 857 # ASSIGN : s_0_11 892 # ASSIGN : s_0_12 1037 # ASSIGN : s_0_13 1075 # ASSIGN : s_0_14 1157 # ASSIGN : s_1_0 60 # ASSIGN : s_1_1 166 # ASSIGN : s_1_2 288 # ASSIGN : s_1_3 595 # ASSIGN : s_1_4 689 # ASSIGN : s_1_5 695 # ASSIGN : s_1_6 781 # ASSIGN : s_1_7 863 # ASSIGN : s_1_8 870 # ASSIGN : s_1_9 981 # ASSIGN : s_1_10 1002 # ASSIGN : s_1_11 1025 # ASSIGN : s_1_12 1050 # ASSIGN : s_1_13 1105 # ASSIGN : s_1_14 1154 # ASSIGN : s_2_0 46 # ASSIGN : s_2_1 165 # ASSIGN : s_2_2 249 # ASSIGN : s_2_3 272 # ASSIGN : s_2_4 344 # ASSIGN : s_2_5 450 # ASSIGN : s_2_6 480 # ASSIGN : s_2_7 545 # ASSIGN : s_2_8 674 # ASSIGN : s_2_9 733 # ASSIGN : s_2_10 854 # ASSIGN : s_2_11 960 # ASSIGN : s_2_12 1054 # ASSIGN : s_2_13 1115 # ASSIGN : s_2_14 1148 # ASSIGN : s_3_0 3 # ASSIGN : s_3_1 15 # ASSIGN : s_3_2 66 # ASSIGN : s_3_3 104 # ASSIGN : s_3_4 119 # ASSIGN : s_3_5 246 # ASSIGN : s_3_6 344 # ASSIGN : s_3_7 438 # ASSIGN : s_3_8 503 # ASSIGN : s_3_9 571 # ASSIGN : s_3_10 672 # ASSIGN : s_3_11 687 # ASSIGN : s_3_12 770 # ASSIGN : s_3_13 809 # ASSIGN : s_3_14 908 # ASSIGN : s_4_0 10 # ASSIGN : s_4_1 137 # ASSIGN : s_4_2 144 # ASSIGN : s_4_3 240 # ASSIGN : s_4_4 377 # ASSIGN : s_4_5 450 # ASSIGN : s_4_6 514 # ASSIGN : s_4_7 546 # ASSIGN : s_4_8 615 # ASSIGN : s_4_9 689 # ASSIGN : s_4_10 783 # ASSIGN : s_4_11 806 # ASSIGN : s_4_12 1042 # ASSIGN : s_4_13 1171 # ASSIGN : s_4_14 1195 # ASSIGN : s_5_0 94 # ASSIGN : s_5_1 223 # ASSIGN : s_5_2 311 # ASSIGN : s_5_3 437 # ASSIGN : s_5_4 486 # ASSIGN : s_5_5 530 # ASSIGN : s_5_6 622 # ASSIGN : s_5_7 727 # ASSIGN : s_5_8 747 # ASSIGN : s_5_9 814 # ASSIGN : s_5_10 862 # ASSIGN : s_5_11 949 # ASSIGN : s_5_12 1035 # ASSIGN : s_5_13 1145 # ASSIGN : s_5_14 1177 # ASSIGN : s_6_0 106 # ASSIGN : s_6_1 180 # ASSIGN : s_6_2 262 # ASSIGN : s_6_3 324 # ASSIGN : s_6_4 427 # ASSIGN : s_6_5 529 # ASSIGN : s_6_6 628 # ASSIGN : s_6_7 727 # ASSIGN : s_6_8 753 # ASSIGN : s_6_9 818 # ASSIGN : s_6_10 927 # ASSIGN : s_6_11 995 # ASSIGN : s_6_12 1046 # ASSIGN : s_6_13 1078 # ASSIGN : s_6_14 1130 # ASSIGN : s_7_0 45 # ASSIGN : s_7_1 99 # ASSIGN : s_7_2 123 # ASSIGN : s_7_3 137 # ASSIGN : s_7_4 175 # ASSIGN : s_7_5 217 # ASSIGN : s_7_6 269 # ASSIGN : s_7_7 334 # ASSIGN : s_7_8 371 # ASSIGN : s_7_9 549 # ASSIGN : s_7_10 743 # ASSIGN : s_7_11 925 # ASSIGN : s_7_12 1097 # ASSIGN : s_7_13 1120 # ASSIGN : s_7_14 1143 # ASSIGN : s_8_0 8 # ASSIGN : s_8_1 20 # ASSIGN : s_8_2 89 # ASSIGN : s_8_3 121 # ASSIGN : s_8_4 191 # ASSIGN : s_8_5 418 # ASSIGN : s_8_6 500 # ASSIGN : s_8_7 533 # ASSIGN : s_8_8 578 # ASSIGN : s_8_9 642 # ASSIGN : s_8_10 657 # ASSIGN : s_8_11 680 # ASSIGN : s_8_12 831 # ASSIGN : s_8_13 947 # ASSIGN : s_8_14 984 # ASSIGN : s_9_0 124 # ASSIGN : s_9_1 211 # ASSIGN : s_9_2 278 # ASSIGN : s_9_3 390 # ASSIGN : s_9_4 450 # ASSIGN : s_9_5 498 # ASSIGN : s_9_6 617 # ASSIGN : s_9_7 709 # ASSIGN : s_9_8 733 # ASSIGN : s_9_9 747 # ASSIGN : s_9_10 818 # ASSIGN : s_9_11 882 # ASSIGN : s_9_12 990 # ASSIGN : s_9_13 1039 # ASSIGN : s_9_14 1103 # ASSIGN : s_10_0 163 # ASSIGN : s_10_1 261 # ASSIGN : s_10_2 283 # ASSIGN : s_10_3 440 # ASSIGN : s_10_4 499 # ASSIGN : s_10_5 572 # ASSIGN : s_10_6 588 # ASSIGN : s_10_7 594 # ASSIGN : s_10_8 688 # ASSIGN : s_10_9 803 # ASSIGN : s_10_10 897 # ASSIGN : s_10_11 951 # ASSIGN : s_10_12 1043 # ASSIGN : s_10_13 1089 # ASSIGN : s_10_14 1129 # ASSIGN : s_11_0 126 # ASSIGN : s_11_1 219 # ASSIGN : s_11_2 255 # ASSIGN : s_11_3 277 # ASSIGN : s_11_4 286 # ASSIGN : s_11_5 337 # ASSIGN : s_11_6 414 # ASSIGN : s_11_7 493 # ASSIGN : s_11_8 538 # ASSIGN : s_11_9 568 # ASSIGN : s_11_10 666 # ASSIGN : s_11_11 799 # ASSIGN : s_11_12 927 # ASSIGN : s_11_13 984 # ASSIGN : s_11_14 1127 # ASSIGN : s_12_0 212 # ASSIGN : s_12_1 271 # ASSIGN : s_12_2 354 # ASSIGN : s_12_3 432 # ASSIGN : s_12_4 514 # ASSIGN : s_12_5 596 # ASSIGN : s_12_6 745 # ASSIGN : s_12_7 859 # ASSIGN : s_12_8 890 # ASSIGN : s_12_9 928 # ASSIGN : s_12_10 982 # ASSIGN : s_12_11 989 # ASSIGN : s_12_12 1026 # ASSIGN : s_12_13 1098 # ASSIGN : s_12_14 1150 # ASSIGN : s_13_0 0 # ASSIGN : s_13_1 107 # ASSIGN : s_13_2 141 # ASSIGN : s_13_3 193 # ASSIGN : s_13_4 219 # ASSIGN : s_13_5 247 # ASSIGN : s_13_6 391 # ASSIGN : s_13_7 471 # ASSIGN : s_13_8 524 # ASSIGN : s_13_9 642 # ASSIGN : s_13_10 685 # ASSIGN : s_13_11 741 # ASSIGN : s_13_12 808 # ASSIGN : s_13_13 853 # ASSIGN : s_13_14 947 # ASSIGN : s_14_0 24 # ASSIGN : s_14_1 98 # ASSIGN : s_14_2 115 # ASSIGN : s_14_3 205 # ASSIGN : s_14_4 283 # ASSIGN : s_14_5 310 # ASSIGN : s_14_6 333 # ASSIGN : s_14_7 358 # ASSIGN : s_14_8 376 # ASSIGN : s_14_9 419 # ASSIGN : s_14_10 820 # ASSIGN : s_14_11 846 # ASSIGN : s_14_12 1005 # ASSIGN : s_14_13 1100 # ASSIGN : s_14_14 1184 SHOW_RESULT 1226 END : 1226 (1 seconds) [Fri Jun 2 07:54:34 2006] SHOW_RESULT 1226 CPU : 1.14 = 1.13 + 0.01 + 0 + 0 # BOUND : makespan 1215 1226 MODIFY_CNF 1220 BEGIN : [Fri Jun 2 07:54:34 2006] MODIFY_CNF 1220 END : 148956411 bytes (0 seconds) [Fri Jun 2 07:54:34 2006] MODIFY_CNF 1220 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1220 BEGIN : [Fri Jun 2 07:54:34 2006] CMD : minisat /work/tamura/csp2sat29478.cnf /work/tamura/csp2sat29478.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1735490 5102698 | 578496 0 0 NaNQ | 0.000 % | | 100 | 1735490 5102698 | 636345 100 1553 15.5 | 74.036 % | | 250 | 1735490 5102698 | 699980 250 3746 15.0 | 74.036 % | | 475 | 1735490 5102698 | 769978 475 6527 13.7 | 74.036 % | | 813 | 1735490 5102698 | 846975 813 11914 14.7 | 74.036 % | | 1319 | 1735490 5102698 | 931673 1319 18343 13.9 | 74.036 % | | 2078 | 1735490 5102698 | 1024840 2078 30091 14.5 | 74.036 % | | 3217 | 1735490 5102698 | 1127325 3217 44729 13.9 | 74.036 % | | 4927 | 1735490 5102698 | 1240057 4927 75184 15.3 | 74.036 % | | 7491 | 1735490 5102698 | 1364063 7491 111092 14.8 | 74.036 % | | 11337 | 1735490 5102698 | 1500469 11337 186243 16.4 | 74.036 % | | 17103 | 1735490 5102698 | 1650516 17103 294231 17.2 | 74.036 % | | 25752 | 1735490 5102698 | 1815568 25752 458199 17.8 | 74.036 % | | 38728 | 1717403 5049233 | 1997125 33315 597492 17.9 | 74.236 % | ==============================================================================) restarts : 14 conflicts : 52280 (183 /sec) decisions : 70400 (246 /sec) propagations : 518720269 (1813477 /sec) inspects : 4192607200 (14657608 /sec) conflict literals : 1001535 (41.36 % deleted) CPU time : 286.036 s UNSATISFIABLE VERIFY_CNF 1220 END : (288 seconds) [Fri Jun 2 07:59:22 2006] VERIFY_CNF 1220 CPU : 287.31 = 0 + 0.0299999999999999 + 287.12 + 0.16 # RESULT : makespan 1220 UNSATISFIABLE # BOUND : makespan 1221 1226 MODIFY_CNF 1223 BEGIN : [Fri Jun 2 07:59:22 2006] MODIFY_CNF 1223 END : 148956411 bytes (0 seconds) [Fri Jun 2 07:59:22 2006] MODIFY_CNF 1223 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1223 BEGIN : [Fri Jun 2 07:59:22 2006] CMD : minisat /work/tamura/csp2sat29478.cnf /work/tamura/csp2sat29478.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1749251 5143296 | 583083 0 0 NaNQ | 0.000 % | | 103 | 1749251 5143296 | 641391 103 1123 10.9 | 73.866 % | | 253 | 1749251 5143296 | 705530 253 2278 9.0 | 73.866 % | | 478 | 1749251 5143296 | 776083 478 5406 11.3 | 73.866 % | | 816 | 1749251 5143296 | 853691 816 9810 12.0 | 73.866 % | | 1323 | 1749251 5143296 | 939061 1323 17121 12.9 | 73.866 % | | 2082 | 1749251 5143296 | 1032967 2082 29517 14.2 | 73.866 % | | 3221 | 1749251 5143296 | 1136263 3221 52877 16.4 | 73.866 % | | 4929 | 1749251 5143296 | 1249890 4929 85118 17.3 | 73.866 % | | 7492 | 1749251 5143296 | 1374879 7492 123391 16.5 | 73.866 % | ==============================================================================) restarts : 10 conflicts : 9087 (161 /sec) decisions : 13801 (245 /sec) propagations : 94821616 (1679885 /sec) inspects : 773937582 (13711282 /sec) conflict literals : 160408 (30.02 % deleted) CPU time : 56.4453 s SATISFIABLE VERIFY_CNF 1223 END : (58 seconds) [Fri Jun 2 08:00:20 2006] VERIFY_CNF 1223 CPU : 57.97 = 0.00999999999999091 + 0.02 + 57.79 + 0.15 # RESULT : makespan 1223 SATISFIABLE SHOW_RESULT 1223 BEGIN : [Fri Jun 2 08:00:20 2006] # ASSIGN : makespan 1223 # ASSIGN : s_0_0 32 # ASSIGN : s_0_1 126 # ASSIGN : s_0_2 199 # ASSIGN : s_0_3 480 # ASSIGN : s_0_4 513 # ASSIGN : s_0_5 564 # ASSIGN : s_0_6 639 # ASSIGN : s_0_7 712 # ASSIGN : s_0_8 760 # ASSIGN : s_0_9 773 # ASSIGN : s_0_10 854 # ASSIGN : s_0_11 889 # ASSIGN : s_0_12 1034 # ASSIGN : s_0_13 1072 # ASSIGN : s_0_14 1154 # ASSIGN : s_1_0 90 # ASSIGN : s_1_1 179 # ASSIGN : s_1_2 232 # ASSIGN : s_1_3 315 # ASSIGN : s_1_4 364 # ASSIGN : s_1_5 370 # ASSIGN : s_1_6 426 # ASSIGN : s_1_7 705 # ASSIGN : s_1_8 737 # ASSIGN : s_1_9 862 # ASSIGN : s_1_10 893 # ASSIGN : s_1_11 916 # ASSIGN : s_1_12 926 # ASSIGN : s_1_13 1102 # ASSIGN : s_1_14 1151 # ASSIGN : s_2_0 1 # ASSIGN : s_2_1 74 # ASSIGN : s_2_2 156 # ASSIGN : s_2_3 179 # ASSIGN : s_2_4 241 # ASSIGN : s_2_5 329 # ASSIGN : s_2_6 350 # ASSIGN : s_2_7 416 # ASSIGN : s_2_8 649 # ASSIGN : s_2_9 702 # ASSIGN : s_2_10 857 # ASSIGN : s_2_11 954 # ASSIGN : s_2_12 1031 # ASSIGN : s_2_13 1112 # ASSIGN : s_2_14 1145 # ASSIGN : s_3_0 2 # ASSIGN : s_3_1 35 # ASSIGN : s_3_2 93 # ASSIGN : s_3_3 131 # ASSIGN : s_3_4 163 # ASSIGN : s_3_5 324 # ASSIGN : s_3_6 422 # ASSIGN : s_3_7 516 # ASSIGN : s_3_8 528 # ASSIGN : s_3_9 644 # ASSIGN : s_3_10 691 # ASSIGN : s_3_11 821 # ASSIGN : s_3_12 877 # ASSIGN : s_3_13 883 # ASSIGN : s_3_14 982 # ASSIGN : s_4_0 43 # ASSIGN : s_4_1 140 # ASSIGN : s_4_2 177 # ASSIGN : s_4_3 273 # ASSIGN : s_4_4 290 # ASSIGN : s_4_5 363 # ASSIGN : s_4_6 406 # ASSIGN : s_4_7 438 # ASSIGN : s_4_8 486 # ASSIGN : s_4_9 686 # ASSIGN : s_4_10 780 # ASSIGN : s_4_11 803 # ASSIGN : s_4_12 1039 # ASSIGN : s_4_13 1168 # ASSIGN : s_4_14 1192 # ASSIGN : s_5_0 84 # ASSIGN : s_5_1 241 # ASSIGN : s_5_2 348 # ASSIGN : s_5_3 441 # ASSIGN : s_5_4 454 # ASSIGN : s_5_5 498 # ASSIGN : s_5_6 619 # ASSIGN : s_5_7 717 # ASSIGN : s_5_8 775 # ASSIGN : s_5_9 842 # ASSIGN : s_5_10 859 # ASSIGN : s_5_11 947 # ASSIGN : s_5_12 1032 # ASSIGN : s_5_13 1142 # ASSIGN : s_5_14 1174 # ASSIGN : s_6_0 97 # ASSIGN : s_6_1 126 # ASSIGN : s_6_2 220 # ASSIGN : s_6_3 373 # ASSIGN : s_6_4 547 # ASSIGN : s_6_5 619 # ASSIGN : s_6_6 668 # ASSIGN : s_6_7 767 # ASSIGN : s_6_8 793 # ASSIGN : s_6_9 849 # ASSIGN : s_6_10 897 # ASSIGN : s_6_11 965 # ASSIGN : s_6_12 1023 # ASSIGN : s_6_13 1075 # ASSIGN : s_6_14 1127 # ASSIGN : s_7_0 15 # ASSIGN : s_7_1 69 # ASSIGN : s_7_2 95 # ASSIGN : s_7_3 109 # ASSIGN : s_7_4 147 # ASSIGN : s_7_5 183 # ASSIGN : s_7_6 235 # ASSIGN : s_7_7 290 # ASSIGN : s_7_8 368 # ASSIGN : s_7_9 546 # ASSIGN : s_7_10 894 # ASSIGN : s_7_11 1016 # ASSIGN : s_7_12 1094 # ASSIGN : s_7_13 1117 # ASSIGN : s_7_14 1140 # ASSIGN : s_8_0 3 # ASSIGN : s_8_1 17 # ASSIGN : s_8_2 86 # ASSIGN : s_8_3 112 # ASSIGN : s_8_4 135 # ASSIGN : s_8_5 395 # ASSIGN : s_8_6 477 # ASSIGN : s_8_7 510 # ASSIGN : s_8_8 555 # ASSIGN : s_8_9 634 # ASSIGN : s_8_10 654 # ASSIGN : s_8_11 710 # ASSIGN : s_8_12 783 # ASSIGN : s_8_13 965 # ASSIGN : s_8_14 1092 # ASSIGN : s_9_0 3 # ASSIGN : s_9_1 196 # ASSIGN : s_9_2 208 # ASSIGN : s_9_3 288 # ASSIGN : s_9_4 476 # ASSIGN : s_9_5 524 # ASSIGN : s_9_6 614 # ASSIGN : s_9_7 706 # ASSIGN : s_9_8 730 # ASSIGN : s_9_9 744 # ASSIGN : s_9_10 815 # ASSIGN : s_9_11 879 # ASSIGN : s_9_12 950 # ASSIGN : s_9_13 1036 # ASSIGN : s_9_14 1100 # ASSIGN : s_10_0 261 # ASSIGN : s_10_1 325 # ASSIGN : s_10_2 347 # ASSIGN : s_10_3 408 # ASSIGN : s_10_4 474 # ASSIGN : s_10_5 618 # ASSIGN : s_10_6 634 # ASSIGN : s_10_7 640 # ASSIGN : s_10_8 734 # ASSIGN : s_10_9 827 # ASSIGN : s_10_10 894 # ASSIGN : s_10_11 948 # ASSIGN : s_10_12 1040 # ASSIGN : s_10_13 1086 # ASSIGN : s_10_14 1126 # ASSIGN : s_11_0 7 # ASSIGN : s_11_1 99 # ASSIGN : s_11_2 146 # ASSIGN : s_11_3 168 # ASSIGN : s_11_4 243 # ASSIGN : s_11_5 290 # ASSIGN : s_11_6 397 # ASSIGN : s_11_7 476 # ASSIGN : s_11_8 535 # ASSIGN : s_11_9 565 # ASSIGN : s_11_10 663 # ASSIGN : s_11_11 789 # ASSIGN : s_11_12 796 # ASSIGN : s_11_13 851 # ASSIGN : s_11_14 917 # ASSIGN : s_12_0 154 # ASSIGN : s_12_1 203 # ASSIGN : s_12_2 341 # ASSIGN : s_12_3 450 # ASSIGN : s_12_4 532 # ASSIGN : s_12_5 642 # ASSIGN : s_12_6 742 # ASSIGN : s_12_7 859 # ASSIGN : s_12_8 890 # ASSIGN : s_12_9 925 # ASSIGN : s_12_10 979 # ASSIGN : s_12_11 986 # ASSIGN : s_12_12 1023 # ASSIGN : s_12_13 1095 # ASSIGN : s_12_14 1147 # ASSIGN : s_13_0 154 # ASSIGN : s_13_1 252 # ASSIGN : s_13_2 286 # ASSIGN : s_13_3 338 # ASSIGN : s_13_4 367 # ASSIGN : s_13_5 414 # ASSIGN : s_13_6 460 # ASSIGN : s_13_7 540 # ASSIGN : s_13_8 569 # ASSIGN : s_13_9 639 # ASSIGN : s_13_10 682 # ASSIGN : s_13_11 731 # ASSIGN : s_13_12 805 # ASSIGN : s_13_13 850 # ASSIGN : s_13_14 944 # ASSIGN : s_14_0 14 # ASSIGN : s_14_1 109 # ASSIGN : s_14_2 130 # ASSIGN : s_14_3 327 # ASSIGN : s_14_4 394 # ASSIGN : s_14_5 415 # ASSIGN : s_14_6 453 # ASSIGN : s_14_7 494 # ASSIGN : s_14_8 512 # ASSIGN : s_14_9 570 # ASSIGN : s_14_10 770 # ASSIGN : s_14_11 843 # ASSIGN : s_14_12 1002 # ASSIGN : s_14_13 1097 # ASSIGN : s_14_14 1181 SHOW_RESULT 1223 END : 1223 (1 seconds) [Fri Jun 2 08:00:21 2006] SHOW_RESULT 1223 CPU : 1.13 = 1.13 + 0 + 0 + 0 # BOUND : makespan 1221 1223 MODIFY_CNF 1222 BEGIN : [Fri Jun 2 08:00:21 2006] MODIFY_CNF 1222 END : 148956411 bytes (0 seconds) [Fri Jun 2 08:00:21 2006] MODIFY_CNF 1222 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1222 BEGIN : [Fri Jun 2 08:00:21 2006] CMD : minisat /work/tamura/csp2sat29478.cnf /work/tamura/csp2sat29478.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1745526 5132348 | 581842 0 0 NaNQ | 0.000 % | | 100 | 1745526 5132348 | 640026 100 1563 15.6 | 73.922 % | | 251 | 1745526 5132348 | 704028 251 2880 11.5 | 73.922 % | | 476 | 1745526 5132348 | 774431 476 5978 12.6 | 73.922 % | | 813 | 1745526 5132348 | 851874 813 11391 14.0 | 73.922 % | | 1319 | 1745526 5132348 | 937062 1319 16435 12.5 | 73.922 % | | 2079 | 1745526 5132348 | 1030768 2079 24721 11.9 | 73.922 % | | 3218 | 1745526 5132348 | 1133845 3218 39332 12.2 | 73.922 % | | 4926 | 1745526 5132348 | 1247230 4926 70875 14.4 | 73.922 % | | 7489 | 1744791 5130144 | 1371953 7226 101847 14.1 | 73.922 % | | 11333 | 1744791 5130144 | 1509148 11070 172475 15.6 | 73.922 % | | 17099 | 1744791 5130144 | 1660063 16836 284223 16.9 | 73.922 % | | 25749 | 1744791 5130144 | 1826069 25486 477117 18.7 | 73.922 % | | 38723 | 1744791 5130144 | 2008676 38460 775291 20.2 | 73.922 % | ==============================================================================) restarts : 14 conflicts : 40780 (191 /sec) decisions : 55160 (258 /sec) propagations : 388417685 (1819723 /sec) inspects : 3200863528 (14995928 /sec) conflict literals : 817776 (36.50 % deleted) CPU time : 213.449 s SATISFIABLE VERIFY_CNF 1222 END : (216 seconds) [Fri Jun 2 08:03:57 2006] VERIFY_CNF 1222 CPU : 215.01 = 0.0100000000000477 + 0.03 + 214.8 + 0.17 # RESULT : makespan 1222 SATISFIABLE SHOW_RESULT 1222 BEGIN : [Fri Jun 2 08:03:57 2006] # ASSIGN : makespan 1222 # ASSIGN : s_0_0 31 # ASSIGN : s_0_1 125 # ASSIGN : s_0_2 198 # ASSIGN : s_0_3 479 # ASSIGN : s_0_4 512 # ASSIGN : s_0_5 563 # ASSIGN : s_0_6 638 # ASSIGN : s_0_7 711 # ASSIGN : s_0_8 759 # ASSIGN : s_0_9 772 # ASSIGN : s_0_10 853 # ASSIGN : s_0_11 888 # ASSIGN : s_0_12 1033 # ASSIGN : s_0_13 1071 # ASSIGN : s_0_14 1153 # ASSIGN : s_1_0 89 # ASSIGN : s_1_1 178 # ASSIGN : s_1_2 231 # ASSIGN : s_1_3 314 # ASSIGN : s_1_4 363 # ASSIGN : s_1_5 369 # ASSIGN : s_1_6 425 # ASSIGN : s_1_7 557 # ASSIGN : s_1_8 736 # ASSIGN : s_1_9 861 # ASSIGN : s_1_10 892 # ASSIGN : s_1_11 915 # ASSIGN : s_1_12 925 # ASSIGN : s_1_13 1101 # ASSIGN : s_1_14 1150 # ASSIGN : s_2_0 0 # ASSIGN : s_2_1 73 # ASSIGN : s_2_2 155 # ASSIGN : s_2_3 178 # ASSIGN : s_2_4 240 # ASSIGN : s_2_5 328 # ASSIGN : s_2_6 349 # ASSIGN : s_2_7 415 # ASSIGN : s_2_8 648 # ASSIGN : s_2_9 701 # ASSIGN : s_2_10 856 # ASSIGN : s_2_11 953 # ASSIGN : s_2_12 1030 # ASSIGN : s_2_13 1111 # ASSIGN : s_2_14 1144 # ASSIGN : s_3_0 1 # ASSIGN : s_3_1 34 # ASSIGN : s_3_2 92 # ASSIGN : s_3_3 147 # ASSIGN : s_3_4 162 # ASSIGN : s_3_5 323 # ASSIGN : s_3_6 421 # ASSIGN : s_3_7 515 # ASSIGN : s_3_8 527 # ASSIGN : s_3_9 643 # ASSIGN : s_3_10 668 # ASSIGN : s_3_11 683 # ASSIGN : s_3_12 876 # ASSIGN : s_3_13 882 # ASSIGN : s_3_14 981 # ASSIGN : s_4_0 33 # ASSIGN : s_4_1 130 # ASSIGN : s_4_2 137 # ASSIGN : s_4_3 272 # ASSIGN : s_4_4 289 # ASSIGN : s_4_5 362 # ASSIGN : s_4_6 405 # ASSIGN : s_4_7 437 # ASSIGN : s_4_8 485 # ASSIGN : s_4_9 685 # ASSIGN : s_4_10 779 # ASSIGN : s_4_11 802 # ASSIGN : s_4_12 1038 # ASSIGN : s_4_13 1167 # ASSIGN : s_4_14 1191 # ASSIGN : s_5_0 83 # ASSIGN : s_5_1 240 # ASSIGN : s_5_2 347 # ASSIGN : s_5_3 440 # ASSIGN : s_5_4 453 # ASSIGN : s_5_5 497 # ASSIGN : s_5_6 618 # ASSIGN : s_5_7 716 # ASSIGN : s_5_8 774 # ASSIGN : s_5_9 841 # ASSIGN : s_5_10 858 # ASSIGN : s_5_11 946 # ASSIGN : s_5_12 1031 # ASSIGN : s_5_13 1141 # ASSIGN : s_5_14 1173 # ASSIGN : s_6_0 96 # ASSIGN : s_6_1 125 # ASSIGN : s_6_2 219 # ASSIGN : s_6_3 372 # ASSIGN : s_6_4 472 # ASSIGN : s_6_5 618 # ASSIGN : s_6_6 667 # ASSIGN : s_6_7 766 # ASSIGN : s_6_8 792 # ASSIGN : s_6_9 848 # ASSIGN : s_6_10 896 # ASSIGN : s_6_11 964 # ASSIGN : s_6_12 1022 # ASSIGN : s_6_13 1074 # ASSIGN : s_6_14 1126 # ASSIGN : s_7_0 14 # ASSIGN : s_7_1 68 # ASSIGN : s_7_2 94 # ASSIGN : s_7_3 108 # ASSIGN : s_7_4 146 # ASSIGN : s_7_5 182 # ASSIGN : s_7_6 234 # ASSIGN : s_7_7 289 # ASSIGN : s_7_8 367 # ASSIGN : s_7_9 545 # ASSIGN : s_7_10 893 # ASSIGN : s_7_11 1015 # ASSIGN : s_7_12 1093 # ASSIGN : s_7_13 1116 # ASSIGN : s_7_14 1139 # ASSIGN : s_8_0 2 # ASSIGN : s_8_1 16 # ASSIGN : s_8_2 85 # ASSIGN : s_8_3 111 # ASSIGN : s_8_4 134 # ASSIGN : s_8_5 394 # ASSIGN : s_8_6 476 # ASSIGN : s_8_7 509 # ASSIGN : s_8_8 554 # ASSIGN : s_8_9 633 # ASSIGN : s_8_10 653 # ASSIGN : s_8_11 709 # ASSIGN : s_8_12 782 # ASSIGN : s_8_13 949 # ASSIGN : s_8_14 1091 # ASSIGN : s_9_0 2 # ASSIGN : s_9_1 195 # ASSIGN : s_9_2 207 # ASSIGN : s_9_3 287 # ASSIGN : s_9_4 475 # ASSIGN : s_9_5 523 # ASSIGN : s_9_6 613 # ASSIGN : s_9_7 705 # ASSIGN : s_9_8 729 # ASSIGN : s_9_9 743 # ASSIGN : s_9_10 814 # ASSIGN : s_9_11 878 # ASSIGN : s_9_12 986 # ASSIGN : s_9_13 1035 # ASSIGN : s_9_14 1099 # ASSIGN : s_10_0 260 # ASSIGN : s_10_1 324 # ASSIGN : s_10_2 346 # ASSIGN : s_10_3 407 # ASSIGN : s_10_4 544 # ASSIGN : s_10_5 617 # ASSIGN : s_10_6 633 # ASSIGN : s_10_7 639 # ASSIGN : s_10_8 733 # ASSIGN : s_10_9 826 # ASSIGN : s_10_10 893 # ASSIGN : s_10_11 947 # ASSIGN : s_10_12 1039 # ASSIGN : s_10_13 1085 # ASSIGN : s_10_14 1125 # ASSIGN : s_11_0 6 # ASSIGN : s_11_1 98 # ASSIGN : s_11_2 176 # ASSIGN : s_11_3 233 # ASSIGN : s_11_4 242 # ASSIGN : s_11_5 289 # ASSIGN : s_11_6 396 # ASSIGN : s_11_7 475 # ASSIGN : s_11_8 534 # ASSIGN : s_11_9 564 # ASSIGN : s_11_10 662 # ASSIGN : s_11_11 788 # ASSIGN : s_11_12 795 # ASSIGN : s_11_13 850 # ASSIGN : s_11_14 916 # ASSIGN : s_12_0 153 # ASSIGN : s_12_1 202 # ASSIGN : s_12_2 339 # ASSIGN : s_12_3 449 # ASSIGN : s_12_4 531 # ASSIGN : s_12_5 641 # ASSIGN : s_12_6 741 # ASSIGN : s_12_7 858 # ASSIGN : s_12_8 889 # ASSIGN : s_12_9 924 # ASSIGN : s_12_10 978 # ASSIGN : s_12_11 985 # ASSIGN : s_12_12 1022 # ASSIGN : s_12_13 1094 # ASSIGN : s_12_14 1146 # ASSIGN : s_13_0 153 # ASSIGN : s_13_1 251 # ASSIGN : s_13_2 285 # ASSIGN : s_13_3 337 # ASSIGN : s_13_4 366 # ASSIGN : s_13_5 412 # ASSIGN : s_13_6 459 # ASSIGN : s_13_7 539 # ASSIGN : s_13_8 568 # ASSIGN : s_13_9 638 # ASSIGN : s_13_10 681 # ASSIGN : s_13_11 730 # ASSIGN : s_13_12 804 # ASSIGN : s_13_13 849 # ASSIGN : s_13_14 943 # ASSIGN : s_14_0 13 # ASSIGN : s_14_1 108 # ASSIGN : s_14_2 129 # ASSIGN : s_14_3 326 # ASSIGN : s_14_4 393 # ASSIGN : s_14_5 414 # ASSIGN : s_14_6 451 # ASSIGN : s_14_7 493 # ASSIGN : s_14_8 511 # ASSIGN : s_14_9 569 # ASSIGN : s_14_10 769 # ASSIGN : s_14_11 842 # ASSIGN : s_14_12 1001 # ASSIGN : s_14_13 1096 # ASSIGN : s_14_14 1180 SHOW_RESULT 1222 END : 1222 (1 seconds) [Fri Jun 2 08:03:58 2006] SHOW_RESULT 1222 CPU : 1.14999999999999 = 1.13999999999999 + 0.01 + 0 + 0 # BOUND : makespan 1221 1222 MODIFY_CNF 1221 BEGIN : [Fri Jun 2 08:03:58 2006] MODIFY_CNF 1221 END : 148956411 bytes (0 seconds) [Fri Jun 2 08:03:58 2006] MODIFY_CNF 1221 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1221 BEGIN : [Fri Jun 2 08:03:58 2006] CMD : minisat /work/tamura/csp2sat29478.cnf /work/tamura/csp2sat29478.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1742682 5124042 | 580894 0 0 NaNQ | 0.000 % | | 100 | 1742682 5124042 | 638983 100 1555 15.6 | 73.978 % | | 250 | 1742682 5124042 | 702881 250 2763 11.1 | 73.978 % | | 476 | 1742682 5124042 | 773169 476 4577 9.6 | 73.978 % | | 814 | 1742682 5124042 | 850486 814 8446 10.4 | 73.978 % | | 1320 | 1742682 5124042 | 935535 1320 16449 12.5 | 73.978 % | | 2079 | 1742682 5124042 | 1029089 2079 27016 13.0 | 73.978 % | | 3219 | 1742682 5124042 | 1131998 3219 45957 14.3 | 73.978 % | | 4927 | 1742682 5124042 | 1245197 4927 68483 13.9 | 73.978 % | | 7489 | 1742682 5124042 | 1369717 7489 108253 14.5 | 73.978 % | | 11333 | 1742682 5124042 | 1506689 11333 176910 15.6 | 73.978 % | | 17100 | 1742682 5124042 | 1657358 17100 274778 16.1 | 73.978 % | | 25749 | 1742682 5124042 | 1823094 25749 478469 18.6 | 73.978 % | | 38723 | 1742682 5124042 | 2005403 38723 800431 20.7 | 73.978 % | | 58184 | 1604570 4715102 | 2205943 30900 589904 19.1 | 75.332 % | ==============================================================================) restarts : 15 conflicts : 59907 (175 /sec) decisions : 80423 (235 /sec) propagations : 615067858 (1795156 /sec) inspects : 5004646302 (14606713 /sec) conflict literals : 1286292 (38.99 % deleted) CPU time : 342.626 s UNSATISFIABLE VERIFY_CNF 1221 END : (345 seconds) [Fri Jun 2 08:09:43 2006] VERIFY_CNF 1221 CPU : 343.85 = 0.00999999999999091 + 0.03 + 343.66 + 0.15 # RESULT : makespan 1221 UNSATISFIABLE # BOUND : makespan 1222 1222 MAIN END : (1766 seconds) [Fri Jun 2 08:09:43 2006] MAIN CPU : 1760.98 = 317.41 + 0.74 + 1440.5 + 2.33