# TIMEOUT 18000 MAIN BEGIN : [Mon Jun 19 13:54:58 2006] READ BEGIN : csp/tai_15x15_7.csp [Mon Jun 19 13:54:58 2006] READ END : csp/tai_15x15_7.csp (7 seconds) [Mon Jun 19 13:55:05 2006] READ CPU : 6.77 = 6.68 + 0.09 + 0 + 0 # BOUND : makespan 891 1398 GENERATE_CNF 1398 BEGIN : [Mon Jun 19 13:55:05 2006] GENERATE_CNF 1398 END : 322034 variables 8943618 clauses 214486862 bytes (350 seconds) [Mon Jun 19 14:00:55 2006] GENERATE_CNF 1398 CPU : 349.04 = 347.35 + 1.69 + 0 + 0 MODIFY_CNF 1144 BEGIN : [Mon Jun 19 14:00:55 2006] MODIFY_CNF 1144 END : 214486868 bytes (0 seconds) [Mon Jun 19 14:00:55 2006] MODIFY_CNF 1144 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1144 BEGIN : [Mon Jun 19 14:00:55 2006] CMD : minisat /tmp/csp2sat31783.cnf /tmp/csp2sat31783.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 7335538 21696513 | 2445179 0 0 nan | 0.000 % | | 101 | 7335538 21696513 | 2689696 101 4105 40.6 | 21.471 % | ============================================================================== restarts : 2 conflicts : 122 (7 /sec) decisions : 2237 (130 /sec) propagations : 1458096 (84822 /sec) conflict literals : 4409 (11.98 % deleted) Memory used : 363.27 MB CPU time : 17.19 s SATISFIABLE VERIFY_CNF 1144 END : (18 seconds) [Mon Jun 19 14:01:13 2006] VERIFY_CNF 1144 CPU : 18.5 = 0 + 0 + 17.36 + 1.14 # RESULT : makespan 1144 SATISFIABLE SHOW_RESULT 1144 BEGIN : [Mon Jun 19 14:01:13 2006] # ASSIGN : makespan 1144 # ASSIGN : s_0_0 307 # ASSIGN : s_0_1 240 # ASSIGN : s_0_2 390 # ASSIGN : s_0_3 481 # ASSIGN : s_0_4 504 # ASSIGN : s_0_5 511 # ASSIGN : s_0_6 670 # ASSIGN : s_0_7 594 # ASSIGN : s_0_8 861 # ASSIGN : s_0_9 598 # ASSIGN : s_0_10 1093 # ASSIGN : s_0_11 1004 # ASSIGN : s_0_12 926 # ASSIGN : s_0_13 1136 # ASSIGN : s_0_14 799 # ASSIGN : s_1_0 5 # ASSIGN : s_1_1 134 # ASSIGN : s_1_2 175 # ASSIGN : s_1_3 261 # ASSIGN : s_1_4 6 # ASSIGN : s_1_5 233 # ASSIGN : s_1_6 588 # ASSIGN : s_1_7 354 # ASSIGN : s_1_8 831 # ASSIGN : s_1_9 452 # ASSIGN : s_1_10 875 # ASSIGN : s_1_11 964 # ASSIGN : s_1_12 787 # ASSIGN : s_1_13 1059 # ASSIGN : s_1_14 784 # ASSIGN : s_2_0 46 # ASSIGN : s_2_1 255 # ASSIGN : s_2_2 282 # ASSIGN : s_2_3 1012 # ASSIGN : s_2_4 368 # ASSIGN : s_2_5 490 # ASSIGN : s_2_6 497 # ASSIGN : s_2_7 653 # ASSIGN : s_2_8 797 # ASSIGN : s_2_9 1054 # ASSIGN : s_2_10 784 # ASSIGN : s_2_11 921 # ASSIGN : s_2_12 690 # ASSIGN : s_2_13 832 # ASSIGN : s_2_14 671 # ASSIGN : s_3_0 140 # ASSIGN : s_3_1 16 # ASSIGN : s_3_2 53 # ASSIGN : s_3_3 91 # ASSIGN : s_3_4 230 # ASSIGN : s_3_5 307 # ASSIGN : s_3_6 470 # ASSIGN : s_3_7 382 # ASSIGN : s_3_8 784 # ASSIGN : s_3_9 993 # ASSIGN : s_3_10 688 # ASSIGN : s_3_11 553 # ASSIGN : s_3_12 634 # ASSIGN : s_3_13 815 # ASSIGN : s_3_14 520 # ASSIGN : s_4_0 8 # ASSIGN : s_4_1 53 # ASSIGN : s_4_2 209 # ASSIGN : s_4_3 374 # ASSIGN : s_4_4 380 # ASSIGN : s_4_5 383 # ASSIGN : s_4_6 386 # ASSIGN : s_4_7 1087 # ASSIGN : s_4_8 772 # ASSIGN : s_4_9 944 # ASSIGN : s_4_10 506 # ASSIGN : s_4_11 447 # ASSIGN : s_4_12 602 # ASSIGN : s_4_13 795 # ASSIGN : s_4_14 1141 # ASSIGN : s_5_0 676 # ASSIGN : s_5_1 285 # ASSIGN : s_5_2 7 # ASSIGN : s_5_3 75 # ASSIGN : s_5_4 85 # ASSIGN : s_5_5 100 # ASSIGN : s_5_6 319 # ASSIGN : s_5_7 506 # ASSIGN : s_5_8 763 # ASSIGN : s_5_9 920 # ASSIGN : s_5_10 474 # ASSIGN : s_5_11 146 # ASSIGN : s_5_12 563 # ASSIGN : s_5_13 773 # ASSIGN : s_5_14 419 # ASSIGN : s_6_0 1007 # ASSIGN : s_6_1 922 # ASSIGN : s_6_2 807 # ASSIGN : s_6_3 1055 # ASSIGN : s_6_4 520 # ASSIGN : s_6_5 605 # ASSIGN : s_6_6 242 # ASSIGN : s_6_7 482 # ASSIGN : s_6_8 686 # ASSIGN : s_6_9 899 # ASSIGN : s_6_10 398 # ASSIGN : s_6_11 99 # ASSIGN : s_6_12 560 # ASSIGN : s_6_13 729 # ASSIGN : s_6_14 325 # ASSIGN : s_7_0 451 # ASSIGN : s_7_1 1082 # ASSIGN : s_7_2 295 # ASSIGN : s_7_3 971 # ASSIGN : s_7_4 3 # ASSIGN : s_7_5 1018 # ASSIGN : s_7_6 229 # ASSIGN : s_7_7 796 # ASSIGN : s_7_8 658 # ASSIGN : s_7_9 887 # ASSIGN : s_7_10 385 # ASSIGN : s_7_11 25 # ASSIGN : s_7_12 485 # ASSIGN : s_7_13 703 # ASSIGN : s_7_14 241 # ASSIGN : s_8_0 7 # ASSIGN : s_8_1 159 # ASSIGN : s_8_2 1001 # ASSIGN : s_8_3 552 # ASSIGN : s_8_4 717 # ASSIGN : s_8_5 1134 # ASSIGN : s_8_6 1056 # ASSIGN : s_8_7 1035 # ASSIGN : s_8_8 629 # ASSIGN : s_8_9 815 # ASSIGN : s_8_10 968 # ASSIGN : s_8_11 21 # ASSIGN : s_8_12 435 # ASSIGN : s_8_13 656 # ASSIGN : s_8_14 201 # ASSIGN : s_9_0 1060 # ASSIGN : s_9_1 858 # ASSIGN : s_9_2 1062 # ASSIGN : s_9_3 684 # ASSIGN : s_9_4 1120 # ASSIGN : s_9_5 12 # ASSIGN : s_9_6 976 # ASSIGN : s_9_7 947 # ASSIGN : s_9_8 477 # ASSIGN : s_9_9 756 # ASSIGN : s_9_10 305 # ASSIGN : s_9_11 1137 # ASSIGN : s_9_12 384 # ASSIGN : s_9_13 563 # ASSIGN : s_9_14 172 # ASSIGN : s_10_0 592 # ASSIGN : s_10_1 483 # ASSIGN : s_10_2 1034 # ASSIGN : s_10_3 790 # ASSIGN : s_10_4 864 # ASSIGN : s_10_5 931 # ASSIGN : s_10_6 902 # ASSIGN : s_10_7 1060 # ASSIGN : s_10_8 391 # ASSIGN : s_10_9 695 # ASSIGN : s_10_10 277 # ASSIGN : s_10_11 1094 # ASSIGN : s_10_12 303 # ASSIGN : s_10_13 561 # ASSIGN : s_10_14 99 # ASSIGN : s_11_0 1077 # ASSIGN : s_11_1 720 # ASSIGN : s_11_2 92 # ASSIGN : s_11_3 598 # ASSIGN : s_11_4 956 # ASSIGN : s_11_5 463 # ASSIGN : s_11_6 807 # ASSIGN : s_11_7 229 # ASSIGN : s_11_8 383 # ASSIGN : s_11_9 654 # ASSIGN : s_11_10 147 # ASSIGN : s_11_11 904 # ASSIGN : s_11_12 302 # ASSIGN : s_11_13 477 # ASSIGN : s_11_14 15 # ASSIGN : s_12_0 499 # ASSIGN : s_12_1 1058 # ASSIGN : s_12_2 1099 # ASSIGN : s_12_3 416 # ASSIGN : s_12_4 774 # ASSIGN : s_12_5 694 # ASSIGN : s_12_6 1134 # ASSIGN : s_12_7 209 # ASSIGN : s_12_8 311 # ASSIGN : s_12_9 614 # ASSIGN : s_12_10 60 # ASSIGN : s_12_11 843 # ASSIGN : s_12_12 238 # ASSIGN : s_12_13 471 # ASSIGN : s_12_14 1118 # ASSIGN : s_13_0 839 # ASSIGN : s_13_1 1037 # ASSIGN : s_13_2 485 # ASSIGN : s_13_3 887 # ASSIGN : s_13_4 1053 # ASSIGN : s_13_5 744 # ASSIGN : s_13_6 927 # ASSIGN : s_13_7 161 # ASSIGN : s_13_8 229 # ASSIGN : s_13_9 550 # ASSIGN : s_13_10 8 # ASSIGN : s_13_11 290 # ASSIGN : s_13_12 112 # ASSIGN : s_13_13 383 # ASSIGN : s_13_14 1119 # ASSIGN : s_14_0 908 # ASSIGN : s_14_1 600 # ASSIGN : s_14_2 649 # ASSIGN : s_14_3 711 # ASSIGN : s_14_4 1131 # ASSIGN : s_14_5 811 # ASSIGN : s_14_6 761 # ASSIGN : s_14_7 46 # ASSIGN : s_14_8 138 # ASSIGN : s_14_9 522 # ASSIGN : s_14_10 1055 # ASSIGN : s_14_11 229 # ASSIGN : s_14_12 9 # ASSIGN : s_14_13 293 # ASSIGN : s_14_14 1099 SHOW_RESULT 1144 END : 1144 (1 seconds) [Mon Jun 19 14:01:14 2006] SHOW_RESULT 1144 CPU : 1.04999999999997 = 0.96999999999997 + 0.0799999999999998 + 0 + 0 # BOUND : makespan 891 1144 MODIFY_CNF 1017 BEGIN : [Mon Jun 19 14:01:14 2006] MODIFY_CNF 1017 END : 214486868 bytes (0 seconds) [Mon Jun 19 14:01:14 2006] MODIFY_CNF 1017 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1017 BEGIN : [Mon Jun 19 14:01:14 2006] CMD : minisat /tmp/csp2sat31783.cnf /tmp/csp2sat31783.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 6535438 19296213 | 2178479 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 46 (3 /sec) decisions : 1692 (100 /sec) propagations : 694349 (40844 /sec) conflict literals : 1323 (7.29 % deleted) Memory used : 363.24 MB CPU time : 17 s SATISFIABLE VERIFY_CNF 1017 END : (19 seconds) [Mon Jun 19 14:01:33 2006] VERIFY_CNF 1017 CPU : 18.24 = 0 + 0 + 17.16 + 1.08 # RESULT : makespan 1017 SATISFIABLE SHOW_RESULT 1017 BEGIN : [Mon Jun 19 14:01:33 2006] # ASSIGN : makespan 1017 # ASSIGN : s_0_0 608 # ASSIGN : s_0_1 429 # ASSIGN : s_0_2 926 # ASSIGN : s_0_3 838 # ASSIGN : s_0_4 18 # ASSIGN : s_0_5 509 # ASSIGN : s_0_6 338 # ASSIGN : s_0_7 1 # ASSIGN : s_0_8 861 # ASSIGN : s_0_9 178 # ASSIGN : s_0_10 211 # ASSIGN : s_0_11 25 # ASSIGN : s_0_12 260 # ASSIGN : s_0_13 5 # ASSIGN : s_0_14 114 # ASSIGN : s_1_0 8 # ASSIGN : s_1_1 695 # ASSIGN : s_1_2 661 # ASSIGN : s_1_3 567 # ASSIGN : s_1_4 926 # ASSIGN : s_1_5 226 # ASSIGN : s_1_6 469 # ASSIGN : s_1_7 782 # ASSIGN : s_1_8 831 # ASSIGN : s_1_9 96 # ASSIGN : s_1_10 254 # ASSIGN : s_1_11 179 # ASSIGN : s_1_12 343 # ASSIGN : s_1_13 13 # ASSIGN : s_1_14 176 # ASSIGN : s_2_0 691 # ASSIGN : s_2_1 500 # ASSIGN : s_2_2 349 # ASSIGN : s_2_3 273 # ASSIGN : s_2_4 1005 # ASSIGN : s_2_5 380 # ASSIGN : s_2_6 563 # ASSIGN : s_2_7 673 # ASSIGN : s_2_8 797 # ASSIGN : s_2_9 0 # ASSIGN : s_2_10 198 # ASSIGN : s_2_11 219 # ASSIGN : s_2_12 387 # ASSIGN : s_2_13 90 # ASSIGN : s_2_14 179 # ASSIGN : s_3_0 785 # ASSIGN : s_3_1 444 # ASSIGN : s_3_2 549 # ASSIGN : s_3_3 24 # ASSIGN : s_3_4 708 # ASSIGN : s_3_5 592 # ASSIGN : s_3_6 990 # ASSIGN : s_3_7 343 # ASSIGN : s_3_8 690 # ASSIGN : s_3_9 875 # ASSIGN : s_3_10 102 # ASSIGN : s_3_11 262 # ASSIGN : s_3_12 481 # ASSIGN : s_3_13 201 # ASSIGN : s_3_14 224 # ASSIGN : s_4_0 570 # ASSIGN : s_4_1 720 # ASSIGN : s_4_2 853 # ASSIGN : s_4_3 73 # ASSIGN : s_4_4 850 # ASSIGN : s_4_5 926 # ASSIGN : s_4_6 7 # ASSIGN : s_4_7 963 # ASSIGN : s_4_8 678 # ASSIGN : s_4_9 801 # ASSIGN : s_4_10 437 # ASSIGN : s_4_11 345 # ASSIGN : s_4_12 535 # ASSIGN : s_4_13 218 # ASSIGN : s_4_14 257 # ASSIGN : s_5_0 882 # ASSIGN : s_5_1 204 # ASSIGN : s_5_2 10 # ASSIGN : s_5_3 79 # ASSIGN : s_5_4 867 # ASSIGN : s_5_5 667 # ASSIGN : s_5_6 737 # ASSIGN : s_5_7 810 # ASSIGN : s_5_8 554 # ASSIGN : s_5_9 713 # ASSIGN : s_5_10 372 # ASSIGN : s_5_11 404 # ASSIGN : s_5_12 567 # ASSIGN : s_5_13 238 # ASSIGN : s_5_14 260 # ASSIGN : s_6_0 969 # ASSIGN : s_6_1 884 # ASSIGN : s_6_2 179 # ASSIGN : s_6_3 89 # ASSIGN : s_6_4 609 # ASSIGN : s_6_5 723 # ASSIGN : s_6_6 804 # ASSIGN : s_6_7 649 # ASSIGN : s_6_8 563 # ASSIGN : s_6_9 692 # ASSIGN : s_6_10 13 # ASSIGN : s_6_11 487 # ASSIGN : s_6_12 606 # ASSIGN : s_6_13 271 # ASSIGN : s_6_14 315 # ASSIGN : s_7_0 220 # ASSIGN : s_7_1 264 # ASSIGN : s_7_2 56 # ASSIGN : s_7_3 178 # ASSIGN : s_7_4 151 # ASSIGN : s_7_5 442 # ASSIGN : s_7_6 154 # ASSIGN : s_7_7 872 # ASSIGN : s_7_8 506 # ASSIGN : s_7_9 166 # ASSIGN : s_7_10 0 # ASSIGN : s_7_11 534 # ASSIGN : s_7_12 609 # ASSIGN : s_7_13 326 # ASSIGN : s_7_14 388 # ASSIGN : s_8_0 9 # ASSIGN : s_8_1 10 # ASSIGN : s_8_2 146 # ASSIGN : s_8_3 219 # ASSIGN : s_8_4 265 # ASSIGN : s_8_5 52 # ASSIGN : s_8_6 68 # ASSIGN : s_8_7 322 # ASSIGN : s_8_8 425 # ASSIGN : s_8_9 612 # ASSIGN : s_8_10 909 # ASSIGN : s_8_11 608 # ASSIGN : s_8_12 684 # ASSIGN : s_8_13 352 # ASSIGN : s_8_14 452 # ASSIGN : s_9_0 254 # ASSIGN : s_9_1 52 # ASSIGN : s_9_2 362 # ASSIGN : s_9_3 315 # ASSIGN : s_9_4 128 # ASSIGN : s_9_5 929 # ASSIGN : s_9_6 654 # ASSIGN : s_9_7 139 # ASSIGN : s_9_8 168 # ASSIGN : s_9_9 256 # ASSIGN : s_9_10 533 # ASSIGN : s_9_11 612 # ASSIGN : s_9_12 734 # ASSIGN : s_9_13 399 # ASSIGN : s_9_14 492 # ASSIGN : s_10_0 32 # ASSIGN : s_10_1 116 # ASSIGN : s_10_2 418 # ASSIGN : s_10_3 342 # ASSIGN : s_10_4 888 # ASSIGN : s_10_5 255 # ASSIGN : s_10_6 444 # ASSIGN : s_10_7 5 # ASSIGN : s_10_8 931 # ASSIGN : s_10_9 194 # ASSIGN : s_10_10 662 # ASSIGN : s_10_11 619 # ASSIGN : s_10_12 785 # ASSIGN : s_10_13 495 # ASSIGN : s_10_14 521 # ASSIGN : s_11_0 262 # ASSIGN : s_11_1 329 # ASSIGN : s_11_2 798 # ASSIGN : s_11_3 416 # ASSIGN : s_11_4 165 # ASSIGN : s_11_5 38 # ASSIGN : s_11_6 881 # ASSIGN : s_11_7 66 # ASSIGN : s_11_8 489 # ASSIGN : s_11_9 976 # ASSIGN : s_11_10 688 # ASSIGN : s_11_11 671 # ASSIGN : s_11_12 866 # ASSIGN : s_11_13 497 # ASSIGN : s_11_14 594 # ASSIGN : s_12_0 127 # ASSIGN : s_12_1 527 # ASSIGN : s_12_2 587 # ASSIGN : s_12_3 472 # ASSIGN : s_12_4 323 # ASSIGN : s_12_5 392 # ASSIGN : s_12_6 551 # ASSIGN : s_12_7 561 # ASSIGN : s_12_8 606 # ASSIGN : s_12_9 936 # ASSIGN : s_12_10 770 # ASSIGN : s_12_11 703 # ASSIGN : s_12_12 867 # ASSIGN : s_12_13 581 # ASSIGN : s_12_14 680 # ASSIGN : s_13_0 383 # ASSIGN : s_13_1 577 # ASSIGN : s_13_2 284 # ASSIGN : s_13_3 527 # ASSIGN : s_13_4 62 # ASSIGN : s_13_5 159 # ASSIGN : s_13_6 235 # ASSIGN : s_13_7 431 # ASSIGN : s_13_8 703 # ASSIGN : s_13_9 479 # ASSIGN : s_13_10 857 # ASSIGN : s_13_11 764 # ASSIGN : s_13_12 931 # ASSIGN : s_13_13 593 # ASSIGN : s_13_14 681 # ASSIGN : s_14_0 471 # ASSIGN : s_14_1 611 # ASSIGN : s_14_2 710 # ASSIGN : s_14_3 660 # ASSIGN : s_14_4 49 # ASSIGN : s_14_5 62 # ASSIGN : s_14_6 184 # ASSIGN : s_14_7 230 # ASSIGN : s_14_8 334 # ASSIGN : s_14_9 583 # ASSIGN : s_14_10 942 # ASSIGN : s_14_11 881 # ASSIGN : s_14_12 980 # ASSIGN : s_14_13 791 # ASSIGN : s_14_14 772 SHOW_RESULT 1017 END : 1017 (1 seconds) [Mon Jun 19 14:01:34 2006] SHOW_RESULT 1017 CPU : 1.23000000000003 = 1.22000000000003 + 0.01 + 0 + 0 # BOUND : makespan 891 1017 MODIFY_CNF 954 BEGIN : [Mon Jun 19 14:01:34 2006] MODIFY_CNF 954 END : 214486867 bytes (0 seconds) [Mon Jun 19 14:01:34 2006] MODIFY_CNF 954 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 954 BEGIN : [Mon Jun 19 14:01:34 2006] CMD : minisat /tmp/csp2sat31783.cnf /tmp/csp2sat31783.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 6138538 18105513 | 2046179 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 35 (2 /sec) decisions : 1072 (67 /sec) propagations : 475787 (29718 /sec) conflict literals : 910 (7.99 % deleted) Memory used : 363.24 MB CPU time : 16.01 s SATISFIABLE VERIFY_CNF 954 END : (18 seconds) [Mon Jun 19 14:01:52 2006] VERIFY_CNF 954 CPU : 17.59 = 0 + 0 + 16.17 + 1.42 # RESULT : makespan 954 SATISFIABLE SHOW_RESULT 954 BEGIN : [Mon Jun 19 14:01:52 2006] # ASSIGN : makespan 954 # ASSIGN : s_0_0 251 # ASSIGN : s_0_1 484 # ASSIGN : s_0_2 660 # ASSIGN : s_0_3 521 # ASSIGN : s_0_4 2 # ASSIGN : s_0_5 388 # ASSIGN : s_0_6 569 # ASSIGN : s_0_7 549 # ASSIGN : s_0_8 800 # ASSIGN : s_0_9 553 # ASSIGN : s_0_10 757 # ASSIGN : s_0_11 865 # ASSIGN : s_0_12 71 # ASSIGN : s_0_13 185 # ASSIGN : s_0_14 9 # ASSIGN : s_1_0 1 # ASSIGN : s_1_1 386 # ASSIGN : s_1_2 270 # ASSIGN : s_1_3 711 # ASSIGN : s_1_4 632 # ASSIGN : s_1_5 42 # ASSIGN : s_1_6 487 # ASSIGN : s_1_7 804 # ASSIGN : s_1_8 457 # ASSIGN : s_1_9 316 # ASSIGN : s_1_10 832 # ASSIGN : s_1_11 2 # ASSIGN : s_1_12 149 # ASSIGN : s_1_13 193 # ASSIGN : s_1_14 82 # ASSIGN : s_2_0 692 # ASSIGN : s_2_1 499 # ASSIGN : s_2_2 463 # ASSIGN : s_2_3 389 # ASSIGN : s_2_4 20 # ASSIGN : s_2_5 32 # ASSIGN : s_2_6 104 # ASSIGN : s_2_7 786 # ASSIGN : s_2_8 526 # ASSIGN : s_2_9 864 # ASSIGN : s_2_10 819 # ASSIGN : s_2_11 42 # ASSIGN : s_2_12 195 # ASSIGN : s_2_13 289 # ASSIGN : s_2_14 85 # ASSIGN : s_3_0 864 # ASSIGN : s_3_1 54 # ASSIGN : s_3_2 751 # ASSIGN : s_3_3 472 # ASSIGN : s_3_4 299 # ASSIGN : s_3_5 224 # ASSIGN : s_3_6 9 # ASSIGN : s_3_7 567 # ASSIGN : s_3_8 36 # ASSIGN : s_3_9 803 # ASSIGN : s_3_10 655 # ASSIGN : s_3_11 137 # ASSIGN : s_3_12 402 # ASSIGN : s_3_13 378 # ASSIGN : s_3_14 104 # ASSIGN : s_4_0 418 # ASSIGN : s_4_1 873 # ASSIGN : s_4_2 789 # ASSIGN : s_4_3 4 # ASSIGN : s_4_4 36 # ASSIGN : s_4_5 39 # ASSIGN : s_4_6 43 # ASSIGN : s_4_7 341 # ASSIGN : s_4_8 120 # ASSIGN : s_4_9 504 # ASSIGN : s_4_10 559 # ASSIGN : s_4_11 218 # ASSIGN : s_4_12 456 # ASSIGN : s_4_13 395 # ASSIGN : s_4_14 138 # ASSIGN : s_5_0 560 # ASSIGN : s_5_1 20 # ASSIGN : s_5_2 369 # ASSIGN : s_5_3 10 # ASSIGN : s_5_4 55 # ASSIGN : s_5_5 70 # ASSIGN : s_5_6 838 # ASSIGN : s_5_7 196 # ASSIGN : s_5_8 132 # ASSIGN : s_5_9 253 # ASSIGN : s_5_10 527 # ASSIGN : s_5_11 277 # ASSIGN : s_5_12 488 # ASSIGN : s_5_13 415 # ASSIGN : s_5_14 141 # ASSIGN : s_6_0 483 # ASSIGN : s_6_1 633 # ASSIGN : s_6_2 862 # ASSIGN : s_6_3 544 # ASSIGN : s_6_4 76 # ASSIGN : s_6_5 116 # ASSIGN : s_6_6 761 # ASSIGN : s_6_7 52 # ASSIGN : s_6_8 718 # ASSIGN : s_6_9 416 # ASSIGN : s_6_10 284 # ASSIGN : s_6_11 360 # ASSIGN : s_6_12 531 # ASSIGN : s_6_13 437 # ASSIGN : s_6_14 197 # ASSIGN : s_7_0 647 # ASSIGN : s_7_1 811 # ASSIGN : s_7_2 96 # ASSIGN : s_7_3 22 # ASSIGN : s_7_4 192 # ASSIGN : s_7_5 324 # ASSIGN : s_7_6 195 # ASSIGN : s_7_7 681 # ASSIGN : s_7_8 772 # ASSIGN : s_7_9 207 # ASSIGN : s_7_10 219 # ASSIGN : s_7_11 407 # ASSIGN : s_7_12 534 # ASSIGN : s_7_13 481 # ASSIGN : s_7_14 270 # ASSIGN : s_8_0 109 # ASSIGN : s_8_1 178 # ASSIGN : s_8_2 0 # ASSIGN : s_8_3 63 # ASSIGN : s_8_4 242 # ASSIGN : s_8_5 807 # ASSIGN : s_8_6 409 # ASSIGN : s_8_7 860 # ASSIGN : s_8_8 320 # ASSIGN : s_8_9 731 # ASSIGN : s_8_10 921 # ASSIGN : s_8_11 503 # ASSIGN : s_8_12 609 # ASSIGN : s_8_13 507 # ASSIGN : s_8_14 347 # ASSIGN : s_9_0 3 # ASSIGN : s_9_1 298 # ASSIGN : s_9_2 33 # ASSIGN : s_9_3 111 # ASSIGN : s_9_4 376 # ASSIGN : s_9_5 719 # ASSIGN : s_9_6 217 # ASSIGN : s_9_7 416 # ASSIGN : s_9_8 868 # ASSIGN : s_9_9 445 # ASSIGN : s_9_10 138 # ASSIGN : s_9_11 510 # ASSIGN : s_9_12 659 # ASSIGN : s_9_13 554 # ASSIGN : s_9_14 387 # ASSIGN : s_10_0 334 # ASSIGN : s_10_1 220 # ASSIGN : s_10_2 70 # ASSIGN : s_10_3 146 # ASSIGN : s_10_4 916 # ASSIGN : s_10_5 817 # ASSIGN : s_10_6 663 # ASSIGN : s_10_7 307 # ASSIGN : s_10_8 560 # ASSIGN : s_10_9 9 # ASSIGN : s_10_10 112 # ASSIGN : s_10_11 517 # ASSIGN : s_10_12 710 # ASSIGN : s_10_13 647 # ASSIGN : s_10_14 418 # ASSIGN : s_11_0 797 # ASSIGN : s_11_1 91 # ASSIGN : s_11_2 186 # ASSIGN : s_11_3 241 # ASSIGN : s_11_4 392 # ASSIGN : s_11_5 635 # ASSIGN : s_11_6 297 # ASSIGN : s_11_7 881 # ASSIGN : s_11_8 1 # ASSIGN : s_11_9 594 # ASSIGN : s_11_10 9 # ASSIGN : s_11_11 568 # ASSIGN : s_11_12 791 # ASSIGN : s_11_13 649 # ASSIGN : s_11_14 491 # ASSIGN : s_12_0 158 # ASSIGN : s_12_1 362 # ASSIGN : s_12_2 251 # ASSIGN : s_12_3 307 # ASSIGN : s_12_4 489 # ASSIGN : s_12_5 904 # ASSIGN : s_12_6 392 # ASSIGN : s_12_7 84 # ASSIGN : s_12_8 646 # ASSIGN : s_12_9 118 # ASSIGN : s_12_10 402 # ASSIGN : s_12_11 585 # ASSIGN : s_12_12 792 # ASSIGN : s_12_13 733 # ASSIGN : s_12_14 584 # ASSIGN : s_13_0 110 # ASSIGN : s_13_1 411 # ASSIGN : s_13_2 304 # ASSIGN : s_13_3 431 # ASSIGN : s_13_4 558 # ASSIGN : s_13_5 471 # ASSIGN : s_13_6 905 # ASSIGN : s_13_7 1 # ASSIGN : s_13_8 49 # ASSIGN : s_13_9 159 # ASSIGN : s_13_10 232 # ASSIGN : s_13_11 646 # ASSIGN : s_13_12 856 # ASSIGN : s_13_13 739 # ASSIGN : s_13_14 624 # ASSIGN : s_14_0 5 # ASSIGN : s_14_1 427 # ASSIGN : s_14_2 476 # ASSIGN : s_14_3 638 # ASSIGN : s_14_4 734 # ASSIGN : s_14_5 538 # ASSIGN : s_14_6 688 # ASSIGN : s_14_7 104 # ASSIGN : s_14_8 197 # ASSIGN : s_14_9 288 # ASSIGN : s_14_10 364 # ASSIGN : s_14_11 747 # ASSIGN : s_14_12 917 # ASSIGN : s_14_13 827 # ASSIGN : s_14_14 808 SHOW_RESULT 954 END : 954 (1 seconds) [Mon Jun 19 14:01:53 2006] SHOW_RESULT 954 CPU : 1.20999999999999 = 1.19999999999999 + 0.01 + 0 + 0 # BOUND : makespan 891 954 MODIFY_CNF 922 BEGIN : [Mon Jun 19 14:01:53 2006] MODIFY_CNF 922 END : 214486867 bytes (0 seconds) [Mon Jun 19 14:01:53 2006] MODIFY_CNF 922 CPU : 0.01 = 0 + 0.01 + 0 + 0 VERIFY_CNF 922 BEGIN : [Mon Jun 19 14:01:53 2006] CMD : minisat /tmp/csp2sat31783.cnf /tmp/csp2sat31783.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 5936938 17500713 | 1978979 0 0 nan | 0.000 % | | 101 | 5936938 17500713 | 2176876 101 3466 34.3 | 37.051 % | ============================================================================== restarts : 2 conflicts : 125 (6 /sec) decisions : 1597 (78 /sec) propagations : 901963 (44084 /sec) conflict literals : 3678 (4.72 % deleted) Memory used : 363.27 MB CPU time : 20.46 s SATISFIABLE VERIFY_CNF 922 END : (22 seconds) [Mon Jun 19 14:02:15 2006] VERIFY_CNF 922 CPU : 21.75 = 0 + 0 + 20.6 + 1.15 # RESULT : makespan 922 SATISFIABLE SHOW_RESULT 922 BEGIN : [Mon Jun 19 14:02:15 2006] # ASSIGN : makespan 922 # ASSIGN : s_0_0 446 # ASSIGN : s_0_1 163 # ASSIGN : s_0_2 355 # ASSIGN : s_0_3 180 # ASSIGN : s_0_4 210 # ASSIGN : s_0_5 630 # ASSIGN : s_0_6 539 # ASSIGN : s_0_7 0 # ASSIGN : s_0_8 27 # ASSIGN : s_0_9 4 # ASSIGN : s_0_10 307 # ASSIGN : s_0_11 793 # ASSIGN : s_0_12 715 # ASSIGN : s_0_13 96 # ASSIGN : s_0_14 245 # ASSIGN : s_1_0 8 # ASSIGN : s_1_1 178 # ASSIGN : s_1_2 37 # ASSIGN : s_1_3 787 # ASSIGN : s_1_4 71 # ASSIGN : s_1_5 150 # ASSIGN : s_1_6 685 # ASSIGN : s_1_7 9 # ASSIGN : s_1_8 203 # ASSIGN : s_1_9 492 # ASSIGN : s_1_10 376 # ASSIGN : s_1_11 882 # ASSIGN : s_1_12 596 # ASSIGN : s_1_13 249 # ASSIGN : s_1_14 682 # ASSIGN : s_2_0 174 # ASSIGN : s_2_1 7 # ASSIGN : s_2_2 148 # ASSIGN : s_2_3 880 # ASSIGN : s_2_4 59 # ASSIGN : s_2_5 34 # ASSIGN : s_2_6 767 # ASSIGN : s_2_7 862 # ASSIGN : s_2_8 92 # ASSIGN : s_2_9 326 # ASSIGN : s_2_10 294 # ASSIGN : s_2_11 597 # ASSIGN : s_2_12 502 # ASSIGN : s_2_13 678 # ASSIGN : s_2_14 73 # ASSIGN : s_3_0 268 # ASSIGN : s_3_1 885 # ASSIGN : s_3_2 695 # ASSIGN : s_3_3 497 # ASSIGN : s_3_4 733 # ASSIGN : s_3_5 810 # ASSIGN : s_3_6 396 # ASSIGN : s_3_7 546 # ASSIGN : s_3_8 126 # ASSIGN : s_3_9 634 # ASSIGN : s_3_10 5 # ASSIGN : s_3_11 187 # ASSIGN : s_3_12 443 # ASSIGN : s_3_13 426 # ASSIGN : s_3_14 154 # ASSIGN : s_4_0 358 # ASSIGN : s_4_1 640 # ASSIGN : s_4_2 75 # ASSIGN : s_4_3 170 # ASSIGN : s_4_4 176 # ASSIGN : s_4_5 180 # ASSIGN : s_4_6 858 # ASSIGN : s_4_7 446 # ASSIGN : s_4_8 721 # ASSIGN : s_4_9 231 # ASSIGN : s_4_10 733 # ASSIGN : s_4_11 538 # ASSIGN : s_4_12 411 # ASSIGN : s_4_13 829 # ASSIGN : s_4_14 919 # ASSIGN : s_5_0 12 # ASSIGN : s_5_1 238 # ASSIGN : s_5_2 753 # ASSIGN : s_5_3 160 # ASSIGN : s_5_4 179 # ASSIGN : s_5_5 304 # ASSIGN : s_5_6 472 # ASSIGN : s_5_7 644 # ASSIGN : s_5_8 194 # ASSIGN : s_5_9 280 # ASSIGN : s_5_10 701 # ASSIGN : s_5_11 389 # ASSIGN : s_5_12 350 # ASSIGN : s_5_13 807 # ASSIGN : s_5_14 99 # ASSIGN : s_6_0 396 # ASSIGN : s_6_1 721 # ASSIGN : s_6_2 161 # ASSIGN : s_6_3 253 # ASSIGN : s_6_4 675 # ASSIGN : s_6_5 465 # ASSIGN : s_6_6 81 # ASSIGN : s_6_7 838 # ASSIGN : s_6_8 879 # ASSIGN : s_6_9 444 # ASSIGN : s_6_10 546 # ASSIGN : s_6_11 342 # ASSIGN : s_6_12 158 # ASSIGN : s_6_13 631 # ASSIGN : s_6_14 0 # ASSIGN : s_7_0 140 # ASSIGN : s_7_1 78 # ASSIGN : s_7_2 522 # ASSIGN : s_7_3 203 # ASSIGN : s_7_4 715 # ASSIGN : s_7_5 401 # ASSIGN : s_7_6 384 # ASSIGN : s_7_7 244 # ASSIGN : s_7_8 612 # ASSIGN : s_7_9 910 # ASSIGN : s_7_10 509 # ASSIGN : s_7_11 718 # ASSIGN : s_7_12 640 # ASSIGN : s_7_13 849 # ASSIGN : s_7_14 792 # ASSIGN : s_8_0 529 # ASSIGN : s_8_1 392 # ASSIGN : s_8_2 254 # ASSIGN : s_8_3 83 # ASSIGN : s_8_4 322 # ASSIGN : s_8_5 129 # ASSIGN : s_8_6 3 # ASSIGN : s_8_7 166 # ASSIGN : s_8_8 139 # ASSIGN : s_8_9 562 # ASSIGN : s_8_10 837 # ASSIGN : s_8_11 714 # ASSIGN : s_8_12 187 # ASSIGN : s_8_13 875 # ASSIGN : s_8_14 752 # ASSIGN : s_9_0 10 # ASSIGN : s_9_1 806 # ASSIGN : s_9_2 287 # ASSIGN : s_9_3 14 # ASSIGN : s_9_4 486 # ASSIGN : s_9_5 41 # ASSIGN : s_9_6 204 # ASSIGN : s_9_7 500 # ASSIGN : s_9_8 324 # ASSIGN : s_9_9 747 # ASSIGN : s_9_10 622 # ASSIGN : s_9_11 707 # ASSIGN : s_9_12 870 # ASSIGN : s_9_13 529 # ASSIGN : s_9_14 718 # ASSIGN : s_10_0 530 # ASSIGN : s_10_1 272 # ASSIGN : s_10_2 496 # ASSIGN : s_10_3 713 # ASSIGN : s_10_4 3 # ASSIGN : s_10_5 183 # ASSIGN : s_10_6 639 # ASSIGN : s_10_7 383 # ASSIGN : s_10_8 410 # ASSIGN : s_10_9 122 # ASSIGN : s_10_10 350 # ASSIGN : s_10_11 664 # ASSIGN : s_10_12 41 # ASSIGN : s_10_13 1 # ASSIGN : s_10_14 846 # ASSIGN : s_11_0 854 # ASSIGN : s_11_1 553 # ASSIGN : s_11_2 799 # ASSIGN : s_11_3 657 # ASSIGN : s_11_4 379 # ASSIGN : s_11_5 270 # ASSIGN : s_11_6 284 # ASSIGN : s_11_7 726 # ASSIGN : s_11_8 713 # ASSIGN : s_11_9 20 # ASSIGN : s_11_10 188 # ASSIGN : s_11_11 640 # ASSIGN : s_11_12 921 # ASSIGN : s_11_13 104 # ASSIGN : s_11_14 476 # ASSIGN : s_12_0 713 # ASSIGN : s_12_1 434 # ASSIGN : s_12_2 458 # ASSIGN : s_12_3 602 # ASSIGN : s_12_4 217 # ASSIGN : s_12_5 351 # ASSIGN : s_12_6 675 # ASSIGN : s_12_7 41 # ASSIGN : s_12_8 807 # ASSIGN : s_12_9 61 # ASSIGN : s_12_10 101 # ASSIGN : s_12_11 477 # ASSIGN : s_12_12 286 # ASSIGN : s_12_13 207 # ASSIGN : s_12_14 213 # ASSIGN : s_13_0 806 # ASSIGN : s_13_1 481 # ASSIGN : s_13_2 630 # ASSIGN : s_13_3 383 # ASSIGN : s_13_4 497 # ASSIGN : s_13_5 563 # ASSIGN : s_13_6 423 # ASSIGN : s_13_7 335 # ASSIGN : s_13_8 745 # ASSIGN : s_13_9 697 # ASSIGN : s_13_10 870 # ASSIGN : s_13_11 94 # ASSIGN : s_13_12 237 # ASSIGN : s_13_13 6 # ASSIGN : s_13_14 191 # ASSIGN : s_14_0 614 # ASSIGN : s_14_1 503 # ASSIGN : s_14_2 860 # ASSIGN : s_14_3 552 # ASSIGN : s_14_4 810 # ASSIGN : s_14_5 713 # ASSIGN : s_14_6 158 # ASSIGN : s_14_7 66 # ASSIGN : s_14_8 233 # ASSIGN : s_14_9 416 # ASSIGN : s_14_10 465 # ASSIGN : s_14_11 5 # ASSIGN : s_14_12 823 # ASSIGN : s_14_13 326 # ASSIGN : s_14_14 214 SHOW_RESULT 922 END : 922 (1 seconds) [Mon Jun 19 14:02:16 2006] SHOW_RESULT 922 CPU : 1.21999999999997 = 1.21999999999997 + 0 + 0 + 0 # BOUND : makespan 891 922 MODIFY_CNF 906 BEGIN : [Mon Jun 19 14:02:16 2006] MODIFY_CNF 906 END : 214486867 bytes (0 seconds) [Mon Jun 19 14:02:16 2006] MODIFY_CNF 906 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 906 BEGIN : [Mon Jun 19 14:02:16 2006] CMD : minisat /tmp/csp2sat31783.cnf /tmp/csp2sat31783.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 5836138 17198313 | 1945379 0 0 nan | 0.000 % | | 100 | 5836138 17198313 | 2139916 100 2041 20.4 | 38.174 % | ============================================================================== restarts : 2 conflicts : 142 (7 /sec) decisions : 1798 (84 /sec) propagations : 986001 (46204 /sec) conflict literals : 2469 (6.94 % deleted) Memory used : 363.27 MB CPU time : 21.34 s SATISFIABLE VERIFY_CNF 906 END : (22 seconds) [Mon Jun 19 14:02:38 2006] VERIFY_CNF 906 CPU : 22.58 = 0 + 0 + 21.51 + 1.07 # RESULT : makespan 906 SATISFIABLE SHOW_RESULT 906 BEGIN : [Mon Jun 19 14:02:38 2006] # ASSIGN : makespan 906 # ASSIGN : s_0_0 599 # ASSIGN : s_0_1 0 # ASSIGN : s_0_2 461 # ASSIGN : s_0_3 794 # ASSIGN : s_0_4 15 # ASSIGN : s_0_5 823 # ASSIGN : s_0_6 690 # ASSIGN : s_0_7 22 # ASSIGN : s_0_8 243 # ASSIGN : s_0_9 583 # ASSIGN : s_0_10 98 # ASSIGN : s_0_11 154 # ASSIGN : s_0_12 318 # ASSIGN : s_0_13 552 # ASSIGN : s_0_14 36 # ASSIGN : s_1_0 765 # ASSIGN : s_1_1 584 # ASSIGN : s_1_2 852 # ASSIGN : s_1_3 659 # ASSIGN : s_1_4 135 # ASSIGN : s_1_5 214 # ASSIGN : s_1_6 242 # ASSIGN : s_1_7 26 # ASSIGN : s_1_8 483 # ASSIGN : s_1_9 513 # ASSIGN : s_1_10 347 # ASSIGN : s_1_11 443 # ASSIGN : s_1_12 60 # ASSIGN : s_1_13 775 # ASSIGN : s_1_14 902 # ASSIGN : s_2_0 162 # ASSIGN : s_2_1 798 # ASSIGN : s_2_2 839 # ASSIGN : s_2_3 752 # ASSIGN : s_2_4 827 # ASSIGN : s_2_5 310 # ASSIGN : s_2_6 373 # ASSIGN : s_2_7 54 # ASSIGN : s_2_8 629 # ASSIGN : s_2_9 72 # ASSIGN : s_2_10 569 # ASSIGN : s_2_11 330 # ASSIGN : s_2_12 471 # ASSIGN : s_2_13 663 # ASSIGN : s_2_14 883 # ASSIGN : s_3_0 0 # ASSIGN : s_3_1 609 # ASSIGN : s_3_2 270 # ASSIGN : s_3_3 90 # ASSIGN : s_3_4 308 # ASSIGN : s_3_5 446 # ASSIGN : s_3_6 781 # ASSIGN : s_3_7 521 # ASSIGN : s_3_8 139 # ASSIGN : s_3_9 385 # ASSIGN : s_3_10 174 # ASSIGN : s_3_11 808 # ASSIGN : s_3_12 727 # ASSIGN : s_3_13 646 # ASSIGN : s_3_14 694 # ASSIGN : s_4_0 103 # ASSIGN : s_4_1 825 # ASSIGN : s_4_2 164 # ASSIGN : s_4_3 141 # ASSIGN : s_4_4 100 # ASSIGN : s_4_5 97 # ASSIGN : s_4_6 541 # ASSIGN : s_4_7 467 # ASSIGN : s_4_8 152 # ASSIGN : s_4_9 237 # ASSIGN : s_4_10 1 # ASSIGN : s_4_11 749 # ASSIGN : s_4_12 286 # ASSIGN : s_4_13 626 # ASSIGN : s_4_14 538 # ASSIGN : s_5_0 819 # ASSIGN : s_5_1 363 # ASSIGN : s_5_2 118 # ASSIGN : s_5_3 307 # ASSIGN : s_5_4 649 # ASSIGN : s_5_5 317 # ASSIGN : s_5_6 175 # ASSIGN : s_5_7 397 # ASSIGN : s_5_8 166 # ASSIGN : s_5_9 454 # ASSIGN : s_5_10 533 # ASSIGN : s_5_11 666 # ASSIGN : s_5_12 565 # ASSIGN : s_5_13 604 # ASSIGN : s_5_14 478 # ASSIGN : s_6_0 766 # ASSIGN : s_6_1 16 # ASSIGN : s_6_2 669 # ASSIGN : s_6_3 817 # ASSIGN : s_6_4 230 # ASSIGN : s_6_5 101 # ASSIGN : s_6_6 464 # ASSIGN : s_6_7 367 # ASSIGN : s_6_8 187 # ASSIGN : s_6_9 346 # ASSIGN : s_6_10 270 # ASSIGN : s_6_11 619 # ASSIGN : s_6_12 814 # ASSIGN : s_6_13 560 # ASSIGN : s_6_14 391 # ASSIGN : s_7_0 683 # ASSIGN : s_7_1 246 # ASSIGN : s_7_2 24 # ASSIGN : s_7_3 205 # ASSIGN : s_7_4 824 # ASSIGN : s_7_5 748 # ASSIGN : s_7_6 812 # ASSIGN : s_7_7 114 # ASSIGN : s_7_8 851 # ASSIGN : s_7_9 736 # ASSIGN : s_7_10 893 # ASSIGN : s_7_11 545 # ASSIGN : s_7_12 396 # ASSIGN : s_7_13 519 # ASSIGN : s_7_14 337 # ASSIGN : s_8_0 682 # ASSIGN : s_8_1 725 # ASSIGN : s_8_2 339 # ASSIGN : s_8_3 556 # ASSIGN : s_8_4 767 # ASSIGN : s_8_5 526 # ASSIGN : s_8_6 602 # ASSIGN : s_8_7 703 # ASSIGN : s_8_8 879 # ASSIGN : s_8_9 0 # ASSIGN : s_8_10 141 # ASSIGN : s_8_11 541 # ASSIGN : s_8_12 236 # ASSIGN : s_8_13 472 # ASSIGN : s_8_14 297 # ASSIGN : s_9_0 817 # ASSIGN : s_9_1 656 # ASSIGN : s_9_2 619 # ASSIGN : s_9_3 352 # ASSIGN : s_9_4 515 # ASSIGN : s_9_5 7 # ASSIGN : s_9_6 95 # ASSIGN : s_9_7 229 # ASSIGN : s_9_8 533 # ASSIGN : s_9_9 287 # ASSIGN : s_9_10 720 # ASSIGN : s_9_11 526 # ASSIGN : s_9_12 855 # ASSIGN : s_9_13 379 # ASSIGN : s_9_14 258 # ASSIGN : s_10_0 256 # ASSIGN : s_10_1 105 # ASSIGN : s_10_2 372 # ASSIGN : s_10_3 4 # ASSIGN : s_10_4 398 # ASSIGN : s_10_5 536 # ASSIGN : s_10_6 881 # ASSIGN : s_10_7 78 # ASSIGN : s_10_8 704 # ASSIGN : s_10_9 797 # ASSIGN : s_10_10 436 # ASSIGN : s_10_11 483 # ASSIGN : s_10_12 623 # ASSIGN : s_10_13 370 # ASSIGN : s_10_14 183 # ASSIGN : s_11_0 340 # ASSIGN : s_11_1 495 # ASSIGN : s_11_2 761 # ASSIGN : s_11_3 439 # ASSIGN : s_11_4 664 # ASSIGN : s_11_5 182 # ASSIGN : s_11_6 0 # ASSIGN : s_11_7 816 # ASSIGN : s_11_8 96 # ASSIGN : s_11_9 196 # ASSIGN : s_11_10 582 # ASSIGN : s_11_11 889 # ASSIGN : s_11_12 104 # ASSIGN : s_11_13 256 # ASSIGN : s_11_14 105 # ASSIGN : s_12_0 407 # ASSIGN : s_12_1 339 # ASSIGN : s_12_2 886 # ASSIGN : s_12_3 604 # ASSIGN : s_12_4 535 # ASSIGN : s_12_5 260 # ASSIGN : s_12_6 680 # ASSIGN : s_12_7 1 # ASSIGN : s_12_8 21 # ASSIGN : s_12_9 757 # ASSIGN : s_12_10 799 # ASSIGN : s_12_11 93 # ASSIGN : s_12_12 172 # ASSIGN : s_12_13 250 # ASSIGN : s_12_14 905 # ASSIGN : s_13_0 717 # ASSIGN : s_13_1 308 # ASSIGN : s_13_2 552 # ASSIGN : s_13_3 512 # ASSIGN : s_13_4 446 # ASSIGN : s_13_5 379 # ASSIGN : s_13_6 324 # ASSIGN : s_13_7 617 # ASSIGN : s_13_8 790 # ASSIGN : s_13_9 858 # ASSIGN : s_13_10 665 # ASSIGN : s_13_11 0 # ASSIGN : s_13_12 113 # ASSIGN : s_13_13 162 # ASSIGN : s_13_14 768 # ASSIGN : s_14_0 500 # ASSIGN : s_14_1 197 # ASSIGN : s_14_2 399 # ASSIGN : s_14_3 147 # ASSIGN : s_14_4 2 # ASSIGN : s_14_5 627 # ASSIGN : s_14_6 835 # ASSIGN : s_14_7 724 # ASSIGN : s_14_8 308 # ASSIGN : s_14_9 599 # ASSIGN : s_14_10 462 # ASSIGN : s_14_11 247 # ASSIGN : s_14_12 20 # ASSIGN : s_14_13 57 # ASSIGN : s_14_14 816 SHOW_RESULT 906 END : 906 (2 seconds) [Mon Jun 19 14:02:40 2006] SHOW_RESULT 906 CPU : 1.25000000000002 = 1.23000000000002 + 0.02 + 0 + 0 # BOUND : makespan 891 906 MODIFY_CNF 898 BEGIN : [Mon Jun 19 14:02:40 2006] MODIFY_CNF 898 END : 214486866 bytes (0 seconds) [Mon Jun 19 14:02:40 2006] MODIFY_CNF 898 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 898 BEGIN : [Mon Jun 19 14:02:40 2006] CMD : minisat /tmp/csp2sat31783.cnf /tmp/csp2sat31783.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 5785738 17047113 | 1928579 0 0 nan | 0.000 % | | 100 | 5785738 17047113 | 2121436 100 2597 26.0 | 38.735 % | ============================================================================== restarts : 2 conflicts : 185 (8 /sec) decisions : 2275 (103 /sec) propagations : 1158496 (52373 /sec) conflict literals : 3897 (5.25 % deleted) Memory used : 363.27 MB CPU time : 22.12 s SATISFIABLE VERIFY_CNF 898 END : (23 seconds) [Mon Jun 19 14:03:03 2006] VERIFY_CNF 898 CPU : 23.5 = 0 + 0 + 22.27 + 1.23 # RESULT : makespan 898 SATISFIABLE SHOW_RESULT 898 BEGIN : [Mon Jun 19 14:03:03 2006] # ASSIGN : makespan 898 # ASSIGN : s_0_0 565 # ASSIGN : s_0_1 101 # ASSIGN : s_0_2 10 # ASSIGN : s_0_3 753 # ASSIGN : s_0_4 306 # ASSIGN : s_0_5 116 # ASSIGN : s_0_6 199 # ASSIGN : s_0_7 6 # ASSIGN : s_0_8 833 # ASSIGN : s_0_9 320 # ASSIGN : s_0_10 776 # ASSIGN : s_0_11 362 # ASSIGN : s_0_12 648 # ASSIGN : s_0_13 490 # ASSIGN : s_0_14 503 # ASSIGN : s_1_0 649 # ASSIGN : s_1_1 335 # ASSIGN : s_1_2 301 # ASSIGN : s_1_3 133 # ASSIGN : s_1_4 29 # ASSIGN : s_1_5 870 # ASSIGN : s_1_6 788 # ASSIGN : s_1_7 671 # ASSIGN : s_1_8 266 # ASSIGN : s_1_9 360 # ASSIGN : s_1_10 445 # ASSIGN : s_1_11 226 # ASSIGN : s_1_12 604 # ASSIGN : s_1_13 711 # ASSIGN : s_1_14 699 # ASSIGN : s_2_0 291 # ASSIGN : s_2_1 226 # ASSIGN : s_2_2 552 # ASSIGN : s_2_3 704 # ASSIGN : s_2_4 17 # ASSIGN : s_2_5 219 # ASSIGN : s_2_6 47 # ASSIGN : s_2_7 566 # ASSIGN : s_2_8 394 # ASSIGN : s_2_9 765 # ASSIGN : s_2_10 34 # ASSIGN : s_2_11 855 # ASSIGN : s_2_12 428 # ASSIGN : s_2_13 615 # ASSIGN : s_2_14 746 # ASSIGN : s_3_0 69 # ASSIGN : s_3_1 32 # ASSIGN : s_3_2 336 # ASSIGN : s_3_3 549 # ASSIGN : s_3_4 161 # ASSIGN : s_3_5 699 # ASSIGN : s_3_6 871 # ASSIGN : s_3_7 461 # ASSIGN : s_3_8 2 # ASSIGN : s_3_9 638 # ASSIGN : s_3_10 238 # ASSIGN : s_3_11 774 # ASSIGN : s_3_12 374 # ASSIGN : s_3_13 598 # ASSIGN : s_3_14 428 # ASSIGN : s_4_0 651 # ASSIGN : s_4_1 253 # ASSIGN : s_4_2 479 # ASSIGN : s_4_3 13 # ASSIGN : s_4_4 3 # ASSIGN : s_4_5 113 # ASSIGN : s_4_6 138 # ASSIGN : s_4_7 844 # ASSIGN : s_4_8 560 # ASSIGN : s_4_9 430 # ASSIGN : s_4_10 334 # ASSIGN : s_4_11 715 # ASSIGN : s_4_12 572 # ASSIGN : s_4_13 801 # ASSIGN : s_4_14 821 # ASSIGN : s_5_0 385 # ASSIGN : s_5_1 116 # ASSIGN : s_5_2 797 # ASSIGN : s_5_3 3 # ASSIGN : s_5_4 370 # ASSIGN : s_5_5 67 # ASSIGN : s_5_6 290 # ASSIGN : s_5_7 210 # ASSIGN : s_5_8 490 # ASSIGN : s_5_9 543 # ASSIGN : s_5_10 692 # ASSIGN : s_5_11 589 # ASSIGN : s_5_12 726 # ASSIGN : s_5_13 567 # ASSIGN : s_5_14 155 # ASSIGN : s_6_0 689 # ASSIGN : s_6_1 740 # ASSIGN : s_6_2 149 # ASSIGN : s_6_3 600 # ASSIGN : s_6_4 458 # ASSIGN : s_6_5 241 # ASSIGN : s_6_6 357 # ASSIGN : s_6_7 434 # ASSIGN : s_6_8 15 # ASSIGN : s_6_9 336 # ASSIGN : s_6_10 73 # ASSIGN : s_6_11 542 # ASSIGN : s_6_12 322 # ASSIGN : s_6_13 498 # ASSIGN : s_6_14 825 # ASSIGN : s_7_0 864 # ASSIGN : s_7_1 556 # ASSIGN : s_7_2 647 # ASSIGN : s_7_3 92 # ASSIGN : s_7_4 0 # ASSIGN : s_7_5 3 # ASSIGN : s_7_6 741 # ASSIGN : s_7_7 753 # ASSIGN : s_7_8 618 # ASSIGN : s_7_9 134 # ASSIGN : s_7_10 432 # ASSIGN : s_7_11 468 # ASSIGN : s_7_12 155 # ASSIGN : s_7_13 341 # ASSIGN : s_7_14 374 # ASSIGN : s_8_0 650 # ASSIGN : s_8_1 183 # ASSIGN : s_8_2 116 # ASSIGN : s_8_3 46 # ASSIGN : s_8_4 313 # ASSIGN : s_8_5 841 # ASSIGN : s_8_6 663 # ASSIGN : s_8_7 162 # ASSIGN : s_8_8 463 # ASSIGN : s_8_9 225 # ASSIGN : s_8_10 572 # ASSIGN : s_8_11 297 # ASSIGN : s_8_12 522 # ASSIGN : s_8_13 851 # ASSIGN : s_8_14 781 # ASSIGN : s_9_0 0 # ASSIGN : s_9_1 393 # ASSIGN : s_9_2 264 # ASSIGN : s_9_3 19 # ASSIGN : s_9_4 6 # ASSIGN : s_9_5 457 # ASSIGN : s_9_6 583 # ASSIGN : s_9_7 364 # ASSIGN : s_9_8 58 # ASSIGN : s_9_9 706 # ASSIGN : s_9_10 819 # ASSIGN : s_9_11 51 # ASSIGN : s_9_12 765 # ASSIGN : s_9_13 144 # ASSIGN : s_9_14 670 # ASSIGN : s_10_0 207 # ASSIGN : s_10_1 467 # ASSIGN : s_10_2 737 # ASSIGN : s_10_3 382 # ASSIGN : s_10_4 108 # ASSIGN : s_10_5 545 # ASSIGN : s_10_6 763 # ASSIGN : s_10_7 644 # ASSIGN : s_10_8 296 # ASSIGN : s_10_9 146 # ASSIGN : s_10_10 8 # ASSIGN : s_10_11 672 # ASSIGN : s_10_12 817 # ASSIGN : s_10_13 6 # ASSIGN : s_10_14 35 # ASSIGN : s_11_0 2 # ASSIGN : s_11_1 632 # ASSIGN : s_11_2 843 # ASSIGN : s_11_3 311 # ASSIGN : s_11_4 719 # ASSIGN : s_11_5 827 # ASSIGN : s_11_6 488 # ASSIGN : s_11_7 71 # ASSIGN : s_11_8 144 # ASSIGN : s_11_9 591 # ASSIGN : s_11_10 152 # ASSIGN : s_11_11 451 # ASSIGN : s_11_12 816 # ASSIGN : s_11_13 367 # ASSIGN : s_11_14 234 # ASSIGN : s_12_0 472 # ASSIGN : s_12_1 150 # ASSIGN : s_12_2 565 # ASSIGN : s_12_3 246 # ASSIGN : s_12_4 389 # ASSIGN : s_12_5 774 # ASSIGN : s_12_6 753 # ASSIGN : s_12_7 10 # ASSIGN : s_12_8 174 # ASSIGN : s_12_9 94 # ASSIGN : s_12_10 605 # ASSIGN : s_12_11 301 # ASSIGN : s_12_12 30 # ASSIGN : s_12_13 845 # ASSIGN : s_12_14 824 # ASSIGN : s_13_0 159 # ASSIGN : s_13_1 2 # ASSIGN : s_13_2 374 # ASSIGN : s_13_3 779 # ASSIGN : s_13_4 819 # ASSIGN : s_13_5 632 # ASSIGN : s_13_6 439 # ASSIGN : s_13_7 584 # ASSIGN : s_13_8 499 # ASSIGN : s_13_9 18 # ASSIGN : s_13_10 724 # ASSIGN : s_13_11 66 # ASSIGN : s_13_12 325 # ASSIGN : s_13_13 237 # ASSIGN : s_13_14 702 # ASSIGN : s_14_0 737 # ASSIGN : s_14_1 836 # ASSIGN : s_14_2 584 # ASSIGN : s_14_3 456 # ASSIGN : s_14_4 885 # ASSIGN : s_14_5 359 # ASSIGN : s_14_6 0 # ASSIGN : s_14_7 267 # ASSIGN : s_14_8 646 # ASSIGN : s_14_9 506 # ASSIGN : s_14_10 534 # ASSIGN : s_14_11 165 # ASSIGN : s_14_12 230 # ASSIGN : s_14_13 46 # ASSIGN : s_14_14 136 SHOW_RESULT 898 END : 898 (1 seconds) [Mon Jun 19 14:03:04 2006] SHOW_RESULT 898 CPU : 1.22 = 1.19 + 0.03 + 0 + 0 # BOUND : makespan 891 898 MODIFY_CNF 894 BEGIN : [Mon Jun 19 14:03:05 2006] MODIFY_CNF 894 END : 214486866 bytes (0 seconds) [Mon Jun 19 14:03:05 2006] MODIFY_CNF 894 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 894 BEGIN : [Mon Jun 19 14:03:05 2006] CMD : minisat /tmp/csp2sat31783.cnf /tmp/csp2sat31783.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 5760538 16971513 | 1920179 0 0 nan | 0.000 % | | 100 | 5760538 16971513 | 2112196 100 3716 37.2 | 39.016 % | | 250 | 5760538 16971513 | 2323416 250 8521 34.1 | 39.016 % | | 475 | 5760538 16971513 | 2555758 475 12571 26.5 | 39.016 % | ============================================================================== restarts : 4 conflicts : 642 (26 /sec) decisions : 3232 (128 /sec) propagations : 2366922 (94075 /sec) conflict literals : 16223 (6.68 % deleted) Memory used : 363.27 MB CPU time : 25.16 s SATISFIABLE VERIFY_CNF 894 END : (26 seconds) [Mon Jun 19 14:03:31 2006] VERIFY_CNF 894 CPU : 26.34 = 0 + 0 + 25.32 + 1.02 # RESULT : makespan 894 SATISFIABLE SHOW_RESULT 894 BEGIN : [Mon Jun 19 14:03:31 2006] # ASSIGN : makespan 894 # ASSIGN : s_0_0 442 # ASSIGN : s_0_1 284 # ASSIGN : s_0_2 302 # ASSIGN : s_0_3 146 # ASSIGN : s_0_4 277 # ASSIGN : s_0_5 780 # ASSIGN : s_0_6 169 # ASSIGN : s_0_7 890 # ASSIGN : s_0_8 0 # ASSIGN : s_0_9 664 # ASSIGN : s_0_10 616 # ASSIGN : s_0_11 680 # ASSIGN : s_0_12 538 # ASSIGN : s_0_13 863 # ASSIGN : s_0_14 84 # ASSIGN : s_1_0 893 # ASSIGN : s_1_1 28 # ASSIGN : s_1_2 778 # ASSIGN : s_1_3 53 # ASSIGN : s_1_4 812 # ASSIGN : s_1_5 750 # ASSIGN : s_1_6 625 # ASSIGN : s_1_7 716 # ASSIGN : s_1_8 393 # ASSIGN : s_1_9 555 # ASSIGN : s_1_10 440 # ASSIGN : s_1_11 268 # ASSIGN : s_1_12 215 # ASSIGN : s_1_13 316 # ASSIGN : s_1_14 437 # ASSIGN : s_2_0 785 # ASSIGN : s_2_1 504 # ASSIGN : s_2_2 881 # ASSIGN : s_2_3 11 # ASSIGN : s_2_4 159 # ASSIGN : s_2_5 283 # ASSIGN : s_2_6 534 # ASSIGN : s_2_7 176 # ASSIGN : s_2_8 353 # ASSIGN : s_2_9 406 # ASSIGN : s_2_10 331 # ASSIGN : s_2_11 637 # ASSIGN : s_2_12 691 # ASSIGN : s_2_13 194 # ASSIGN : s_2_14 387 # ASSIGN : s_3_0 259 # ASSIGN : s_3_1 753 # ASSIGN : s_3_2 188 # ASSIGN : s_3_3 352 # ASSIGN : s_3_4 675 # ASSIGN : s_3_5 512 # ASSIGN : s_3_6 482 # ASSIGN : s_3_7 587 # ASSIGN : s_3_8 827 # ASSIGN : s_3_9 19 # ASSIGN : s_3_10 80 # ASSIGN : s_3_11 401 # ASSIGN : s_3_12 840 # ASSIGN : s_3_13 2 # ASSIGN : s_3_14 226 # ASSIGN : s_4_0 171 # ASSIGN : s_4_1 672 # ASSIGN : s_4_2 560 # ASSIGN : s_4_3 636 # ASSIGN : s_4_4 891 # ASSIGN : s_4_5 498 # ASSIGN : s_4_6 753 # ASSIGN : s_4_7 817 # ASSIGN : s_4_8 660 # ASSIGN : s_4_9 122 # ASSIGN : s_4_10 344 # ASSIGN : s_4_11 501 # ASSIGN : s_4_12 310 # ASSIGN : s_4_13 871 # ASSIGN : s_4_14 223 # ASSIGN : s_5_0 698 # ASSIGN : s_5_1 299 # ASSIGN : s_5_2 393 # ASSIGN : s_5_3 642 # ASSIGN : s_5_4 378 # ASSIGN : s_5_5 652 # ASSIGN : s_5_6 25 # ASSIGN : s_5_7 118 # ASSIGN : s_5_8 857 # ASSIGN : s_5_9 870 # ASSIGN : s_5_10 258 # ASSIGN : s_5_11 175 # ASSIGN : s_5_12 499 # ASSIGN : s_5_13 477 # ASSIGN : s_5_14 587 # ASSIGN : s_6_0 211 # ASSIGN : s_6_1 531 # ASSIGN : s_6_2 439 # ASSIGN : s_6_3 754 # ASSIGN : s_6_4 171 # ASSIGN : s_6_5 290 # ASSIGN : s_6_6 92 # ASSIGN : s_6_7 371 # ASSIGN : s_6_8 616 # ASSIGN : s_6_9 269 # ASSIGN : s_6_10 659 # ASSIGN : s_6_11 843 # ASSIGN : s_6_12 89 # ASSIGN : s_6_13 395 # ASSIGN : s_6_14 11 # ASSIGN : s_7_0 525 # ASSIGN : s_7_1 218 # ASSIGN : s_7_2 688 # ASSIGN : s_7_3 404 # ASSIGN : s_7_4 809 # ASSIGN : s_7_5 588 # ASSIGN : s_7_6 13 # ASSIGN : s_7_7 280 # ASSIGN : s_7_8 866 # ASSIGN : s_7_9 1 # ASSIGN : s_7_10 53 # ASSIGN : s_7_11 66 # ASSIGN : s_7_12 140 # ASSIGN : s_7_13 445 # ASSIGN : s_7_14 471 # ASSIGN : s_8_0 879 # ASSIGN : s_8_1 152 # ASSIGN : s_8_2 99 # ASSIGN : s_8_3 473 # ASSIGN : s_8_4 298 # ASSIGN : s_8_5 880 # ASSIGN : s_8_6 355 # ASSIGN : s_8_7 682 # ASSIGN : s_8_8 758 # ASSIGN : s_8_9 197 # ASSIGN : s_8_10 835 # ASSIGN : s_8_11 890 # ASSIGN : s_8_12 785 # ASSIGN : s_8_13 558 # ASSIGN : s_8_14 703 # ASSIGN : s_9_0 209 # ASSIGN : s_9_1 333 # ASSIGN : s_9_2 132 # ASSIGN : s_9_3 603 # ASSIGN : s_9_4 405 # ASSIGN : s_9_5 17 # ASSIGN : s_9_6 814 # ASSIGN : s_9_7 416 # ASSIGN : s_9_8 247 # ASSIGN : s_9_9 496 # ASSIGN : s_9_10 735 # ASSIGN : s_9_11 630 # ASSIGN : s_9_12 445 # ASSIGN : s_9_13 642 # ASSIGN : s_9_14 558 # ASSIGN : s_10_0 607 # ASSIGN : s_10_1 790 # ASSIGN : s_10_2 534 # ASSIGN : s_10_3 195 # ASSIGN : s_10_4 752 # ASSIGN : s_10_5 105 # ASSIGN : s_10_6 509 # ASSIGN : s_10_7 560 # ASSIGN : s_10_8 423 # ASSIGN : s_10_9 691 # ASSIGN : s_10_10 868 # ASSIGN : s_10_11 23 # ASSIGN : s_10_12 342 # ASSIGN : s_10_13 605 # ASSIGN : s_10_14 269 # ASSIGN : s_11_0 104 # ASSIGN : s_11_1 397 # ASSIGN : s_11_2 633 # ASSIGN : s_11_3 688 # ASSIGN : s_11_4 511 # ASSIGN : s_11_5 3 # ASSIGN : s_11_6 260 # ASSIGN : s_11_7 744 # ASSIGN : s_11_8 608 # ASSIGN : s_11_9 356 # ASSIGN : s_11_10 176 # ASSIGN : s_11_11 484 # ASSIGN : s_11_12 19 # ASSIGN : s_11_13 20 # ASSIGN : s_11_14 817 # ASSIGN : s_12_0 349 # ASSIGN : s_12_1 194 # ASSIGN : s_12_2 169 # ASSIGN : s_12_3 294 # ASSIGN : s_12_4 442 # ASSIGN : s_12_5 698 # ASSIGN : s_12_6 3 # ASSIGN : s_12_7 36 # ASSIGN : s_12_8 65 # ASSIGN : s_12_9 830 # ASSIGN : s_12_10 529 # ASSIGN : s_12_11 769 # ASSIGN : s_12_12 627 # ASSIGN : s_12_13 748 # ASSIGN : s_12_14 768 # ASSIGN : s_13_0 559 # ASSIGN : s_13_1 878 # ASSIGN : s_13_2 813 # ASSIGN : s_13_3 519 # ASSIGN : s_13_4 609 # ASSIGN : s_13_5 192 # ASSIGN : s_13_6 433 # ASSIGN : s_13_7 56 # ASSIGN : s_13_8 682 # ASSIGN : s_13_9 765 # ASSIGN : s_13_10 1 # ASSIGN : s_13_11 308 # ASSIGN : s_13_12 259 # ASSIGN : s_13_13 104 # ASSIGN : s_13_14 743 # ASSIGN : s_14_0 1 # ASSIGN : s_14_1 623 # ASSIGN : s_14_2 228 # ASSIGN : s_14_3 844 # ASSIGN : s_14_4 358 # ASSIGN : s_14_5 371 # ASSIGN : s_14_6 707 # ASSIGN : s_14_7 468 # ASSIGN : s_14_8 137 # ASSIGN : s_14_9 328 # ASSIGN : s_14_10 290 # ASSIGN : s_14_11 562 # ASSIGN : s_14_12 100 # ASSIGN : s_14_13 754 # ASSIGN : s_14_14 684 SHOW_RESULT 894 END : 894 (1 seconds) [Mon Jun 19 14:03:32 2006] SHOW_RESULT 894 CPU : 1.23999999999998 = 1.20999999999998 + 0.03 + 0 + 0 # BOUND : makespan 891 894 MODIFY_CNF 892 BEGIN : [Mon Jun 19 14:03:32 2006] MODIFY_CNF 892 END : 214486866 bytes (0 seconds) [Mon Jun 19 14:03:32 2006] MODIFY_CNF 892 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 892 BEGIN : [Mon Jun 19 14:03:32 2006] CMD : minisat /tmp/csp2sat31783.cnf /tmp/csp2sat31783.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 5747938 16933713 | 1915979 0 0 nan | 0.000 % | | 100 | 5747938 16933713 | 2107576 100 2698 27.0 | 39.156 % | | 250 | 5747938 16933713 | 2318334 250 8361 33.4 | 39.156 % | ============================================================================== restarts : 3 conflicts : 398 (16 /sec) decisions : 2835 (117 /sec) propagations : 1999414 (82213 /sec) conflict literals : 11248 (4.85 % deleted) Memory used : 363.27 MB CPU time : 24.32 s SATISFIABLE VERIFY_CNF 892 END : (26 seconds) [Mon Jun 19 14:03:58 2006] VERIFY_CNF 892 CPU : 25.44 = 0 + 0 + 24.46 + 0.98 # RESULT : makespan 892 SATISFIABLE SHOW_RESULT 892 BEGIN : [Mon Jun 19 14:03:58 2006] # ASSIGN : makespan 892 # ASSIGN : s_0_0 246 # ASSIGN : s_0_1 489 # ASSIGN : s_0_2 608 # ASSIGN : s_0_3 223 # ASSIGN : s_0_4 25 # ASSIGN : s_0_5 506 # ASSIGN : s_0_6 120 # ASSIGN : s_0_7 860 # ASSIGN : s_0_8 424 # ASSIGN : s_0_9 84 # ASSIGN : s_0_10 39 # ASSIGN : s_0_11 699 # ASSIGN : s_0_12 346 # ASSIGN : s_0_13 600 # ASSIGN : s_0_14 789 # ASSIGN : s_1_0 736 # ASSIGN : s_1_1 648 # ASSIGN : s_1_2 701 # ASSIGN : s_1_3 129 # ASSIGN : s_1_4 318 # ASSIGN : s_1_5 673 # ASSIGN : s_1_6 28 # ASSIGN : s_1_7 864 # ASSIGN : s_1_8 618 # ASSIGN : s_1_9 222 # ASSIGN : s_1_10 775 # ASSIGN : s_1_11 397 # ASSIGN : s_1_12 479 # ASSIGN : s_1_13 523 # ASSIGN : s_1_14 772 # ASSIGN : s_2_0 99 # ASSIGN : s_2_1 824 # ASSIGN : s_2_2 576 # ASSIGN : s_2_3 534 # ASSIGN : s_2_4 211 # ASSIGN : s_2_5 430 # ASSIGN : s_2_6 223 # ASSIGN : s_2_7 193 # ASSIGN : s_2_8 500 # ASSIGN : s_2_9 683 # ASSIGN : s_2_10 879 # ASSIGN : s_2_11 437 # ASSIGN : s_2_12 5 # ASSIGN : s_2_13 336 # ASSIGN : s_2_14 851 # ASSIGN : s_3_0 428 # ASSIGN : s_3_1 855 # ASSIGN : s_3_2 817 # ASSIGN : s_3_3 611 # ASSIGN : s_3_4 32 # ASSIGN : s_3_5 353 # ASSIGN : s_3_6 1 # ASSIGN : s_3_7 518 # ASSIGN : s_3_8 803 # ASSIGN : s_3_9 292 # ASSIGN : s_3_10 196 # ASSIGN : s_3_11 115 # ASSIGN : s_3_12 660 # ASSIGN : s_3_13 769 # ASSIGN : s_3_14 736 # ASSIGN : s_4_0 571 # ASSIGN : s_4_1 216 # ASSIGN : s_4_2 428 # ASSIGN : s_4_3 675 # ASSIGN : s_4_4 746 # ASSIGN : s_4_5 704 # ASSIGN : s_4_6 609 # ASSIGN : s_4_7 80 # ASSIGN : s_4_8 148 # ASSIGN : s_4_9 519 # ASSIGN : s_4_10 297 # ASSIGN : s_4_11 833 # ASSIGN : s_4_12 714 # ASSIGN : s_4_13 749 # ASSIGN : s_4_14 786 # ASSIGN : s_5_0 737 # ASSIGN : s_5_1 504 # ASSIGN : s_5_2 42 # ASSIGN : s_5_3 10 # ASSIGN : s_5_4 722 # ASSIGN : s_5_5 458 # ASSIGN : s_5_6 825 # ASSIGN : s_5_7 233 # ASSIGN : s_5_8 329 # ASSIGN : s_5_9 100 # ASSIGN : s_5_10 426 # ASSIGN : s_5_11 538 # ASSIGN : s_5_12 621 # ASSIGN : s_5_13 20 # ASSIGN : s_5_14 667 # ASSIGN : s_6_0 198 # ASSIGN : s_6_1 395 # ASSIGN : s_6_2 271 # ASSIGN : s_6_3 748 # ASSIGN : s_6_4 527 # ASSIGN : s_6_5 589 # ASSIGN : s_6_6 670 # ASSIGN : s_6_7 371 # ASSIGN : s_6_8 845 # ASSIGN : s_6_9 568 # ASSIGN : s_6_10 120 # ASSIGN : s_6_11 480 # ASSIGN : s_6_12 888 # ASSIGN : s_6_13 76 # ASSIGN : s_6_14 3 # ASSIGN : s_7_0 617 # ASSIGN : s_7_1 549 # ASSIGN : s_7_2 121 # ASSIGN : s_7_3 80 # ASSIGN : s_7_4 889 # ASSIGN : s_7_5 15 # ASSIGN : s_7_6 211 # ASSIGN : s_7_7 427 # ASSIGN : s_7_8 668 # ASSIGN : s_7_9 415 # ASSIGN : s_7_10 0 # ASSIGN : s_7_11 323 # ASSIGN : s_7_12 746 # ASSIGN : s_7_13 297 # ASSIGN : s_7_14 243 # ASSIGN : s_8_0 891 # ASSIGN : s_8_1 12 # ASSIGN : s_8_2 88 # ASSIGN : s_8_3 250 # ASSIGN : s_8_4 643 # ASSIGN : s_8_5 437 # ASSIGN : s_8_6 747 # ASSIGN : s_8_7 212 # ASSIGN : s_8_8 576 # ASSIGN : s_8_9 447 # ASSIGN : s_8_10 393 # ASSIGN : s_8_11 534 # ASSIGN : s_8_12 296 # ASSIGN : s_8_13 700 # ASSIGN : s_8_14 603 # ASSIGN : s_9_0 615 # ASSIGN : s_9_1 70 # ASSIGN : s_9_2 5 # ASSIGN : s_9_3 584 # ASSIGN : s_9_4 298 # ASSIGN : s_9_5 707 # ASSIGN : s_9_6 483 # ASSIGN : s_9_7 134 # ASSIGN : s_9_8 338 # ASSIGN : s_9_9 163 # ASSIGN : s_9_10 628 # ASSIGN : s_9_11 621 # ASSIGN : s_9_12 428 # ASSIGN : s_9_13 799 # ASSIGN : s_9_14 309 # ASSIGN : s_10_0 651 # ASSIGN : s_10_1 299 # ASSIGN : s_10_2 735 # ASSIGN : s_10_3 377 # ASSIGN : s_10_4 487 # ASSIGN : s_10_5 212 # ASSIGN : s_10_6 458 # ASSIGN : s_10_7 606 # ASSIGN : s_10_8 53 # ASSIGN : s_10_9 831 # ASSIGN : s_10_10 13 # ASSIGN : s_10_11 788 # ASSIGN : s_10_12 525 # ASSIGN : s_10_13 786 # ASSIGN : s_10_14 139 # ASSIGN : s_11_0 824 # ASSIGN : s_11_1 674 # ASSIGN : s_11_2 761 # ASSIGN : s_11_3 23 # ASSIGN : s_11_4 109 # ASSIGN : s_11_5 79 # ASSIGN : s_11_6 363 # ASSIGN : s_11_7 290 # ASSIGN : s_11_8 816 # ASSIGN : s_11_9 633 # ASSIGN : s_11_10 546 # ASSIGN : s_11_11 4 # ASSIGN : s_11_12 891 # ASSIGN : s_11_13 206 # ASSIGN : s_11_14 469 # ASSIGN : s_12_0 6 # ASSIGN : s_12_1 611 # ASSIGN : s_12_2 589 # ASSIGN : s_12_3 837 # ASSIGN : s_12_4 768 # ASSIGN : s_12_5 303 # ASSIGN : s_12_6 110 # ASSIGN : s_12_7 405 # ASSIGN : s_12_8 696 # ASSIGN : s_12_9 365 # ASSIGN : s_12_10 459 # ASSIGN : s_12_11 635 # ASSIGN : s_12_12 137 # ASSIGN : s_12_13 425 # ASSIGN : s_12_14 2 # ASSIGN : s_13_0 519 # ASSIGN : s_13_1 54 # ASSIGN : s_13_2 363 # ASSIGN : s_13_3 681 # ASSIGN : s_13_4 567 # ASSIGN : s_13_5 93 # ASSIGN : s_13_6 314 # ASSIGN : s_13_7 633 # ASSIGN : s_13_8 160 # ASSIGN : s_13_9 773 # ASSIGN : s_13_10 721 # ASSIGN : s_13_11 221 # ASSIGN : s_13_12 821 # ASSIGN : s_13_13 431 # ASSIGN : s_13_14 870 # ASSIGN : s_14_0 329 # ASSIGN : s_14_1 152 # ASSIGN : s_14_2 501 # ASSIGN : s_14_3 451 # ASSIGN : s_14_4 8 # ASSIGN : s_14_5 795 # ASSIGN : s_14_6 563 # ASSIGN : s_14_7 703 # ASSIGN : s_14_8 238 # ASSIGN : s_14_9 124 # ASSIGN : s_14_10 82 # ASSIGN : s_14_11 21 # ASSIGN : s_14_12 201 # ASSIGN : s_14_13 610 # ASSIGN : s_14_14 432 SHOW_RESULT 892 END : 892 (1 seconds) [Mon Jun 19 14:03:59 2006] SHOW_RESULT 892 CPU : 1.27 = 1.25 + 0.0199999999999998 + 0 + 0 # BOUND : makespan 891 892 MODIFY_CNF 891 BEGIN : [Mon Jun 19 14:03:59 2006] MODIFY_CNF 891 END : 214486866 bytes (0 seconds) [Mon Jun 19 14:03:59 2006] MODIFY_CNF 891 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 891 BEGIN : [Mon Jun 19 14:03:59 2006] CMD : minisat /tmp/csp2sat31783.cnf /tmp/csp2sat31783.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 5741639 16914813 | 1913879 0 0 nan | 0.000 % | | 100 | 5741639 16914813 | 2105266 100 1950 19.5 | 39.227 % | ============================================================================== restarts : 2 conflicts : 232 (10 /sec) decisions : 2190 (95 /sec) propagations : 1464650 (63542 /sec) conflict literals : 4201 (4.87 % deleted) Memory used : 363.27 MB CPU time : 23.05 s SATISFIABLE VERIFY_CNF 891 END : (24 seconds) [Mon Jun 19 14:04:23 2006] VERIFY_CNF 891 CPU : 24.46 = 0 + 0.0100000000000002 + 23.2 + 1.25 # RESULT : makespan 891 SATISFIABLE SHOW_RESULT 891 BEGIN : [Mon Jun 19 14:04:23 2006] # ASSIGN : makespan 891 # ASSIGN : s_0_0 259 # ASSIGN : s_0_1 348 # ASSIGN : s_0_2 363 # ASSIGN : s_0_3 231 # ASSIGN : s_0_4 489 # ASSIGN : s_0_5 749 # ASSIGN : s_0_6 140 # ASSIGN : s_0_7 1 # ASSIGN : s_0_8 75 # ASSIGN : s_0_9 832 # ASSIGN : s_0_10 848 # ASSIGN : s_0_11 578 # ASSIGN : s_0_12 671 # ASSIGN : s_0_13 5 # ASSIGN : s_0_14 13 # ASSIGN : s_1_0 746 # ASSIGN : s_1_1 597 # ASSIGN : s_1_2 661 # ASSIGN : s_1_3 397 # ASSIGN : s_1_4 496 # ASSIGN : s_1_5 622 # ASSIGN : s_1_6 308 # ASSIGN : s_1_7 863 # ASSIGN : s_1_8 44 # ASSIGN : s_1_9 74 # ASSIGN : s_1_10 211 # ASSIGN : s_1_11 156 # ASSIGN : s_1_12 0 # ASSIGN : s_1_13 783 # ASSIGN : s_1_14 860 # ASSIGN : s_2_0 747 # ASSIGN : s_2_1 377 # ASSIGN : s_2_2 454 # ASSIGN : s_2_3 568 # ASSIGN : s_2_4 345 # ASSIGN : s_2_5 437 # ASSIGN : s_2_6 0 # ASSIGN : s_2_7 357 # ASSIGN : s_2_8 478 # ASSIGN : s_2_9 255 # ASSIGN : s_2_10 99 # ASSIGN : s_2_11 113 # ASSIGN : s_2_12 158 # ASSIGN : s_2_13 648 # ASSIGN : s_2_14 610 # ASSIGN : s_3_0 439 # ASSIGN : s_3_1 542 # ASSIGN : s_3_2 208 # ASSIGN : s_3_3 623 # ASSIGN : s_3_4 672 # ASSIGN : s_3_5 282 # ASSIGN : s_3_6 596 # ASSIGN : s_3_7 749 # ASSIGN : s_3_8 18 # ASSIGN : s_3_9 376 # ASSIGN : s_3_10 112 # ASSIGN : s_3_11 31 # ASSIGN : s_3_12 837 # ASSIGN : s_3_13 579 # ASSIGN : s_3_14 249 # ASSIGN : s_4_0 1 # ASSIGN : s_4_1 267 # ASSIGN : s_4_2 818 # ASSIGN : s_4_3 90 # ASSIGN : s_4_4 85 # ASSIGN : s_4_5 96 # ASSIGN : s_4_6 535 # ASSIGN : s_4_7 213 # ASSIGN : s_4_8 167 # ASSIGN : s_4_9 690 # ASSIGN : s_4_10 395 # ASSIGN : s_4_11 739 # ASSIGN : s_4_12 639 # ASSIGN : s_4_13 348 # ASSIGN : s_4_14 803 # ASSIGN : s_5_0 39 # ASSIGN : s_5_1 632 # ASSIGN : s_5_2 246 # ASSIGN : s_5_3 164 # ASSIGN : s_5_4 126 # ASSIGN : s_5_5 835 # ASSIGN : s_5_6 390 # ASSIGN : s_5_7 300 # ASSIGN : s_5_8 179 # ASSIGN : s_5_9 666 # ASSIGN : s_5_10 3 # ASSIGN : s_5_11 495 # ASSIGN : s_5_12 593 # ASSIGN : s_5_13 368 # ASSIGN : s_5_14 191 # ASSIGN : s_6_0 843 # ASSIGN : s_6_1 103 # ASSIGN : s_6_2 569 # ASSIGN : s_6_3 714 # ASSIGN : s_6_4 803 # ASSIGN : s_6_5 15 # ASSIGN : s_6_6 231 # ASSIGN : s_6_7 498 # ASSIGN : s_6_8 188 # ASSIGN : s_6_9 477 # ASSIGN : s_6_10 313 # ASSIGN : s_6_11 667 # ASSIGN : s_6_12 566 # ASSIGN : s_6_13 522 # ASSIGN : s_6_14 389 # ASSIGN : s_7_0 134 # ASSIGN : s_7_1 41 # ASSIGN : s_7_2 695 # ASSIGN : s_7_3 174 # ASSIGN : s_7_4 215 # ASSIGN : s_7_5 218 # ASSIGN : s_7_6 879 # ASSIGN : s_7_7 576 # ASSIGN : s_7_8 667 # ASSIGN : s_7_9 867 # ASSIGN : s_7_10 300 # ASSIGN : s_7_11 417 # ASSIGN : s_7_12 491 # ASSIGN : s_7_13 391 # ASSIGN : s_7_14 806 # ASSIGN : s_8_0 841 # ASSIGN : s_8_1 670 # ASSIGN : s_8_2 785 # ASSIGN : s_8_3 118 # ASSIGN : s_8_4 288 # ASSIGN : s_8_5 881 # ASSIGN : s_8_6 457 # ASSIGN : s_8_7 842 # ASSIGN : s_8_8 349 # ASSIGN : s_8_9 2 # ASSIGN : s_8_10 712 # ASSIGN : s_8_11 383 # ASSIGN : s_8_12 407 # ASSIGN : s_8_13 601 # ASSIGN : s_8_14 745 # ASSIGN : s_9_0 342 # ASSIGN : s_9_1 203 # ASSIGN : s_9_2 532 # ASSIGN : s_9_3 315 # ASSIGN : s_9_4 433 # ASSIGN : s_9_5 444 # ASSIGN : s_9_6 704 # ASSIGN : s_9_7 271 # ASSIGN : s_9_8 797 # ASSIGN : s_9_9 144 # ASSIGN : s_9_10 625 # ASSIGN : s_9_11 410 # ASSIGN : s_9_12 356 # ASSIGN : s_9_13 51 # ASSIGN : s_9_14 581 # ASSIGN : s_10_0 168 # ASSIGN : s_10_1 739 # ASSIGN : s_10_2 142 # ASSIGN : s_10_3 817 # ASSIGN : s_10_4 88 # ASSIGN : s_10_5 650 # ASSIGN : s_10_6 623 # ASSIGN : s_10_7 535 # ASSIGN : s_10_8 376 # ASSIGN : s_10_9 562 # ASSIGN : s_10_10 35 # ASSIGN : s_10_11 333 # ASSIGN : s_10_12 252 # ASSIGN : s_10_13 737 # ASSIGN : s_10_14 462 # ASSIGN : s_11_0 676 # ASSIGN : s_11_1 404 # ASSIGN : s_11_2 19 # ASSIGN : s_11_3 254 # ASSIGN : s_11_4 575 # ASSIGN : s_11_5 1 # ASSIGN : s_11_6 784 # ASSIGN : s_11_7 84 # ASSIGN : s_11_8 883 # ASSIGN : s_11_9 743 # ASSIGN : s_11_10 491 # ASSIGN : s_11_11 387 # ASSIGN : s_11_12 157 # ASSIGN : s_11_13 170 # ASSIGN : s_11_14 310 # ASSIGN : s_12_0 344 # ASSIGN : s_12_1 715 # ASSIGN : s_12_2 74 # ASSIGN : s_12_3 490 # ASSIGN : s_12_4 5 # ASSIGN : s_12_5 545 # ASSIGN : s_12_6 694 # ASSIGN : s_12_7 674 # ASSIGN : s_12_8 595 # ASSIGN : s_12_9 437 # ASSIGN : s_12_10 761 # ASSIGN : s_12_11 272 # ASSIGN : s_12_12 93 # ASSIGN : s_12_13 884 # ASSIGN : s_12_14 890 # ASSIGN : s_13_0 628 # ASSIGN : s_13_1 25 # ASSIGN : s_13_2 292 # ASSIGN : s_13_3 50 # ASSIGN : s_13_4 141 # ASSIGN : s_13_5 357 # ASSIGN : s_13_6 91 # ASSIGN : s_13_7 701 # ASSIGN : s_13_8 512 # ASSIGN : s_13_9 207 # ASSIGN : s_13_10 573 # ASSIGN : s_13_11 798 # ASSIGN : s_13_12 749 # ASSIGN : s_13_13 424 # ASSIGN : s_13_14 679 # ASSIGN : s_14_0 529 # ASSIGN : s_14_1 842 # ASSIGN : s_14_2 467 # ASSIGN : s_14_3 0 # ASSIGN : s_14_4 787 # ASSIGN : s_14_5 99 # ASSIGN : s_14_6 648 # ASSIGN : s_14_7 375 # ASSIGN : s_14_8 696 # ASSIGN : s_14_9 347 # ASSIGN : s_14_10 61 # ASSIGN : s_14_11 196 # ASSIGN : s_14_12 800 # ASSIGN : s_14_13 257 # ASSIGN : s_14_14 629 SHOW_RESULT 891 END : 891 (2 seconds) [Mon Jun 19 14:04:25 2006] SHOW_RESULT 891 CPU : 1.24000000000002 = 1.23000000000002 + 0.00999999999999979 + 0 + 0 # BOUND : makespan 891 891 MAIN END : (567 seconds) [Mon Jun 19 14:04:25 2006] MAIN CPU : 565.68 = 365.28 + 2.01 + 188.05 + 10.34