# TIMEOUT 18000 MAIN BEGIN : [Mon Jun 19 14:13:33 2006] READ BEGIN : csp/tai_15x15_9.csp [Mon Jun 19 14:13:33 2006] READ END : csp/tai_15x15_9.csp (7 seconds) [Mon Jun 19 14:13:40 2006] READ CPU : 6.29 = 6.24 + 0.05 + 0 + 0 # BOUND : makespan 899 1407 GENERATE_CNF 1407 BEGIN : [Mon Jun 19 14:13:40 2006] GENERATE_CNF 1407 END : 324060 variables 8998985 clauses 215840562 bytes (348 seconds) [Mon Jun 19 14:19:28 2006] GENERATE_CNF 1407 CPU : 346.98 = 345.53 + 1.45 + 0 + 0 MODIFY_CNF 1153 BEGIN : [Mon Jun 19 14:19:28 2006] MODIFY_CNF 1153 END : 215840568 bytes (0 seconds) [Mon Jun 19 14:19:28 2006] MODIFY_CNF 1153 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1153 BEGIN : [Mon Jun 19 14:19:28 2006] CMD : minisat /tmp/csp2sat32182.cnf /tmp/csp2sat32182.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 7390905 21860588 | 2463635 0 0 nan | 0.000 % | | 100 | 7390905 21860588 | 2709998 100 2032 20.3 | 21.377 % | ============================================================================== restarts : 2 conflicts : 130 (8 /sec) decisions : 2164 (127 /sec) propagations : 1033950 (60821 /sec) conflict literals : 2251 (8.20 % deleted) Memory used : 365.48 MB CPU time : 17 s SATISFIABLE VERIFY_CNF 1153 END : (19 seconds) [Mon Jun 19 14:19:47 2006] VERIFY_CNF 1153 CPU : 18.44 = 0 + 0.01 + 17.17 + 1.26 # RESULT : makespan 1153 SATISFIABLE SHOW_RESULT 1153 BEGIN : [Mon Jun 19 14:19:47 2006] # ASSIGN : makespan 1153 # ASSIGN : s_0_0 428 # ASSIGN : s_0_1 1138 # ASSIGN : s_0_2 752 # ASSIGN : s_0_3 294 # ASSIGN : s_0_4 881 # ASSIGN : s_0_5 1055 # ASSIGN : s_0_6 1144 # ASSIGN : s_0_7 1031 # ASSIGN : s_0_8 368 # ASSIGN : s_0_9 828 # ASSIGN : s_0_10 526 # ASSIGN : s_0_11 489 # ASSIGN : s_0_12 926 # ASSIGN : s_0_13 655 # ASSIGN : s_0_14 493 # ASSIGN : s_1_0 542 # ASSIGN : s_1_1 840 # ASSIGN : s_1_2 654 # ASSIGN : s_1_3 326 # ASSIGN : s_1_4 926 # ASSIGN : s_1_5 379 # ASSIGN : s_1_6 1143 # ASSIGN : s_1_7 13 # ASSIGN : s_1_8 434 # ASSIGN : s_1_9 135 # ASSIGN : s_1_10 1018 # ASSIGN : s_1_11 200 # ASSIGN : s_1_12 284 # ASSIGN : s_1_13 584 # ASSIGN : s_1_14 73 # ASSIGN : s_2_0 1124 # ASSIGN : s_2_1 247 # ASSIGN : s_2_2 728 # ASSIGN : s_2_3 578 # ASSIGN : s_2_4 948 # ASSIGN : s_2_5 153 # ASSIGN : s_2_6 1027 # ASSIGN : s_2_7 51 # ASSIGN : s_2_8 404 # ASSIGN : s_2_9 733 # ASSIGN : s_2_10 868 # ASSIGN : s_2_11 170 # ASSIGN : s_2_12 258 # ASSIGN : s_2_13 513 # ASSIGN : s_2_14 267 # ASSIGN : s_3_0 611 # ASSIGN : s_3_1 797 # ASSIGN : s_3_2 875 # ASSIGN : s_3_3 663 # ASSIGN : s_3_4 312 # ASSIGN : s_3_5 98 # ASSIGN : s_3_6 26 # ASSIGN : s_3_7 912 # ASSIGN : s_3_8 1058 # ASSIGN : s_3_9 189 # ASSIGN : s_3_10 813 # ASSIGN : s_3_11 1001 # ASSIGN : s_3_12 402 # ASSIGN : s_3_13 418 # ASSIGN : s_3_14 599 # ASSIGN : s_4_0 845 # ASSIGN : s_4_1 7 # ASSIGN : s_4_2 9 # ASSIGN : s_4_3 1139 # ASSIGN : s_4_4 48 # ASSIGN : s_4_5 132 # ASSIGN : s_4_6 168 # ASSIGN : s_4_7 902 # ASSIGN : s_4_8 983 # ASSIGN : s_4_9 267 # ASSIGN : s_4_10 462 # ASSIGN : s_4_11 1057 # ASSIGN : s_4_12 937 # ASSIGN : s_4_13 411 # ASSIGN : s_4_14 598 # ASSIGN : s_5_0 1059 # ASSIGN : s_5_1 89 # ASSIGN : s_5_2 322 # ASSIGN : s_5_3 962 # ASSIGN : s_5_4 693 # ASSIGN : s_5_5 834 # ASSIGN : s_5_6 739 # ASSIGN : s_5_7 125 # ASSIGN : s_5_8 916 # ASSIGN : s_5_9 415 # ASSIGN : s_5_10 1122 # ASSIGN : s_5_11 517 # ASSIGN : s_5_12 791 # ASSIGN : s_5_13 1144 # ASSIGN : s_5_14 421 # ASSIGN : s_6_0 28 # ASSIGN : s_6_1 415 # ASSIGN : s_6_2 431 # ASSIGN : s_6_3 809 # ASSIGN : s_6_4 167 # ASSIGN : s_6_5 927 # ASSIGN : s_6_6 521 # ASSIGN : s_6_7 621 # ASSIGN : s_6_8 850 # ASSIGN : s_6_9 1012 # ASSIGN : s_6_10 715 # ASSIGN : s_6_11 515 # ASSIGN : s_6_12 1073 # ASSIGN : s_6_13 342 # ASSIGN : s_6_14 1091 # ASSIGN : s_7_0 898 # ASSIGN : s_7_1 897 # ASSIGN : s_7_2 557 # ASSIGN : s_7_3 758 # ASSIGN : s_7_4 257 # ASSIGN : s_7_5 2 # ASSIGN : s_7_6 87 # ASSIGN : s_7_7 342 # ASSIGN : s_7_8 818 # ASSIGN : s_7_9 635 # ASSIGN : s_7_10 470 # ASSIGN : s_7_11 853 # ASSIGN : s_7_12 699 # ASSIGN : s_7_13 955 # ASSIGN : s_7_14 1027 # ASSIGN : s_8_0 436 # ASSIGN : s_8_1 1052 # ASSIGN : s_8_2 37 # ASSIGN : s_8_3 517 # ASSIGN : s_8_4 790 # ASSIGN : s_8_5 109 # ASSIGN : s_8_6 314 # ASSIGN : s_8_7 154 # ASSIGN : s_8_8 681 # ASSIGN : s_8_9 565 # ASSIGN : s_8_10 913 # ASSIGN : s_8_11 547 # ASSIGN : s_8_12 587 # ASSIGN : s_8_13 873 # ASSIGN : s_8_14 994 # ASSIGN : s_9_0 974 # ASSIGN : s_9_1 106 # ASSIGN : s_9_2 96 # ASSIGN : s_9_3 892 # ASSIGN : s_9_4 391 # ASSIGN : s_9_5 354 # ASSIGN : s_9_6 181 # ASSIGN : s_9_7 253 # ASSIGN : s_9_8 615 # ASSIGN : s_9_9 483 # ASSIGN : s_9_10 1079 # ASSIGN : s_9_11 485 # ASSIGN : s_9_12 490 # ASSIGN : s_9_13 810 # ASSIGN : s_9_14 724 # ASSIGN : s_10_0 41 # ASSIGN : s_10_1 905 # ASSIGN : s_10_2 112 # ASSIGN : s_10_3 887 # ASSIGN : s_10_4 1036 # ASSIGN : s_10_5 176 # ASSIGN : s_10_6 254 # ASSIGN : s_10_7 813 # ASSIGN : s_10_8 526 # ASSIGN : s_10_9 402 # ASSIGN : s_10_10 956 # ASSIGN : s_10_11 473 # ASSIGN : s_10_12 414 # ASSIGN : s_10_13 777 # ASSIGN : s_10_14 645 # ASSIGN : s_11_0 87 # ASSIGN : s_11_1 12 # ASSIGN : s_11_2 162 # ASSIGN : s_11_3 460 # ASSIGN : s_11_4 1133 # ASSIGN : s_11_5 1050 # ASSIGN : s_11_6 1111 # ASSIGN : s_11_7 147 # ASSIGN : s_11_8 237 # ASSIGN : s_11_9 382 # ASSIGN : s_11_10 440 # ASSIGN : s_11_11 358 # ASSIGN : s_11_12 298 # ASSIGN : s_11_13 193 # ASSIGN : s_11_14 611 # ASSIGN : s_12_0 887 # ASSIGN : s_12_1 2 # ASSIGN : s_12_2 813 # ASSIGN : s_12_3 528 # ASSIGN : s_12_4 752 # ASSIGN : s_12_5 578 # ASSIGN : s_12_6 387 # ASSIGN : s_12_7 432 # ASSIGN : s_12_8 191 # ASSIGN : s_12_9 343 # ASSIGN : s_12_10 625 # ASSIGN : s_12_11 225 # ASSIGN : s_12_12 5 # ASSIGN : s_12_13 96 # ASSIGN : s_12_14 305 # ASSIGN : s_13_0 828 # ASSIGN : s_13_1 630 # ASSIGN : s_13_2 945 # ASSIGN : s_13_3 1055 # ASSIGN : s_13_4 13 # ASSIGN : s_13_5 279 # ASSIGN : s_13_6 422 # ASSIGN : s_13_7 528 # ASSIGN : s_13_8 720 # ASSIGN : s_13_9 871 # ASSIGN : s_13_10 364 # ASSIGN : s_13_11 892 # ASSIGN : s_13_12 972 # ASSIGN : s_13_13 59 # ASSIGN : s_13_14 842 # ASSIGN : s_14_0 708 # ASSIGN : s_14_1 93 # ASSIGN : s_14_2 994 # ASSIGN : s_14_3 846 # ASSIGN : s_14_4 206 # ASSIGN : s_14_5 542 # ASSIGN : s_14_6 620 # ASSIGN : s_14_7 328 # ASSIGN : s_14_8 394 # ASSIGN : s_14_9 898 # ASSIGN : s_14_10 261 # ASSIGN : s_14_11 137 # ASSIGN : s_14_12 1101 # ASSIGN : s_14_13 1071 # ASSIGN : s_14_14 796 SHOW_RESULT 1153 END : 1153 (1 seconds) [Mon Jun 19 14:19:48 2006] SHOW_RESULT 1153 CPU : 1.04000000000001 = 0.990000000000009 + 0.05 + 0 + 0 # BOUND : makespan 899 1153 MODIFY_CNF 1026 BEGIN : [Mon Jun 19 14:19:48 2006] MODIFY_CNF 1026 END : 215840568 bytes (0 seconds) [Mon Jun 19 14:19:48 2006] MODIFY_CNF 1026 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1026 BEGIN : [Mon Jun 19 14:19:48 2006] CMD : minisat /tmp/csp2sat32182.cnf /tmp/csp2sat32182.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 6590805 19460288 | 2196935 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 18 (1 /sec) decisions : 1346 (81 /sec) propagations : 465240 (27892 /sec) conflict literals : 224 (1.75 % deleted) Memory used : 365.45 MB CPU time : 16.68 s SATISFIABLE VERIFY_CNF 1026 END : (18 seconds) [Mon Jun 19 14:20:06 2006] VERIFY_CNF 1026 CPU : 17.82 = 0.0100000000000477 + 0 + 16.83 + 0.98 # RESULT : makespan 1026 SATISFIABLE SHOW_RESULT 1026 BEGIN : [Mon Jun 19 14:20:06 2006] # ASSIGN : makespan 1026 # ASSIGN : s_0_0 583 # ASSIGN : s_0_1 388 # ASSIGN : s_0_2 471 # ASSIGN : s_0_3 394 # ASSIGN : s_0_4 426 # ASSIGN : s_0_5 299 # ASSIGN : s_0_6 591 # ASSIGN : s_0_7 275 # ASSIGN : s_0_8 245 # ASSIGN : s_0_9 805 # ASSIGN : s_0_10 49 # ASSIGN : s_0_11 1 # ASSIGN : s_0_12 38 # ASSIGN : s_0_13 148 # ASSIGN : s_0_14 5 # ASSIGN : s_1_0 932 # ASSIGN : s_1_1 732 # ASSIGN : s_1_2 620 # ASSIGN : s_1_3 789 # ASSIGN : s_1_4 598 # ASSIGN : s_1_5 509 # ASSIGN : s_1_6 0 # ASSIGN : s_1_7 316 # ASSIGN : s_1_8 360 # ASSIGN : s_1_9 452 # ASSIGN : s_1_10 167 # ASSIGN : s_1_11 13 # ASSIGN : s_1_12 153 # ASSIGN : s_1_13 246 # ASSIGN : s_1_14 38 # ASSIGN : s_2_0 179 # ASSIGN : s_2_1 208 # ASSIGN : s_2_2 95 # ASSIGN : s_2_3 941 # ASSIGN : s_2_4 764 # ASSIGN : s_2_5 35 # ASSIGN : s_2_6 843 # ASSIGN : s_2_7 660 # ASSIGN : s_2_8 5 # ASSIGN : s_2_9 543 # ASSIGN : s_2_10 228 # ASSIGN : s_2_11 52 # ASSIGN : s_2_12 219 # ASSIGN : s_2_13 343 # ASSIGN : s_2_14 100 # ASSIGN : s_3_0 974 # ASSIGN : s_3_1 257 # ASSIGN : s_3_2 937 # ASSIGN : s_3_3 842 # ASSIGN : s_3_4 685 # ASSIGN : s_3_5 67 # ASSIGN : s_3_6 510 # ASSIGN : s_3_7 571 # ASSIGN : s_3_8 150 # ASSIGN : s_3_9 330 # ASSIGN : s_3_10 273 # ASSIGN : s_3_11 82 # ASSIGN : s_3_12 245 # ASSIGN : s_3_13 408 # ASSIGN : s_3_14 138 # ASSIGN : s_4_0 640 # ASSIGN : s_4_1 395 # ASSIGN : s_4_2 354 # ASSIGN : s_4_3 431 # ASSIGN : s_4_4 845 # ASSIGN : s_4_5 151 # ASSIGN : s_4_6 445 # ASSIGN : s_4_7 299 # ASSIGN : s_4_8 76 # ASSIGN : s_4_9 0 # ASSIGN : s_4_10 328 # ASSIGN : s_4_11 176 # ASSIGN : s_4_12 258 # ASSIGN : s_4_13 503 # ASSIGN : s_4_14 150 # ASSIGN : s_5_0 79 # ASSIGN : s_5_1 142 # ASSIGN : s_5_2 694 # ASSIGN : s_5_3 519 # ASSIGN : s_5_4 380 # ASSIGN : s_5_5 612 # ASSIGN : s_5_6 458 # ASSIGN : s_5_7 1 # ASSIGN : s_5_8 787 # ASSIGN : s_5_9 147 # ASSIGN : s_5_10 336 # ASSIGN : s_5_11 263 # ASSIGN : s_5_12 293 # ASSIGN : s_5_13 510 # ASSIGN : s_5_14 153 # ASSIGN : s_6_0 210 # ASSIGN : s_6_1 1 # ASSIGN : s_6_2 113 # ASSIGN : s_6_3 633 # ASSIGN : s_6_4 17 # ASSIGN : s_6_5 842 # ASSIGN : s_6_6 927 # ASSIGN : s_6_7 748 # ASSIGN : s_6_8 475 # ASSIGN : s_6_9 670 # ASSIGN : s_6_10 358 # ASSIGN : s_6_11 338 # ASSIGN : s_6_12 340 # ASSIGN : s_6_13 541 # ASSIGN : s_6_14 225 # ASSIGN : s_7_0 682 # ASSIGN : s_7_1 22 # ASSIGN : s_7_2 532 # ASSIGN : s_7_3 236 # ASSIGN : s_7_4 56 # ASSIGN : s_7_5 748 # ASSIGN : s_7_6 133 # ASSIGN : s_7_7 872 # ASSIGN : s_7_8 833 # ASSIGN : s_7_9 962 # ASSIGN : s_7_10 452 # ASSIGN : s_7_11 354 # ASSIGN : s_7_12 393 # ASSIGN : s_7_13 610 # ASSIGN : s_7_14 287 # ASSIGN : s_8_0 739 # ASSIGN : s_8_1 559 # ASSIGN : s_8_2 820 # ASSIGN : s_8_3 297 # ASSIGN : s_8_4 131 # ASSIGN : s_8_5 0 # ASSIGN : s_8_6 214 # ASSIGN : s_8_7 23 # ASSIGN : s_8_8 645 # ASSIGN : s_8_9 308 # ASSIGN : s_8_10 983 # ASSIGN : s_8_11 438 # ASSIGN : s_8_12 458 # ASSIGN : s_8_13 684 # ASSIGN : s_8_14 351 # ASSIGN : s_9_0 841 # ASSIGN : s_9_1 649 # ASSIGN : s_9_2 103 # ASSIGN : s_9_3 314 # ASSIGN : s_9_4 219 # ASSIGN : s_9_5 78 # ASSIGN : s_9_6 1 # ASSIGN : s_9_7 122 # ASSIGN : s_9_8 926 # ASSIGN : s_9_9 506 # ASSIGN : s_9_10 508 # ASSIGN : s_9_11 456 # ASSIGN : s_9_12 552 # ASSIGN : s_9_13 724 # ASSIGN : s_9_14 384 # ASSIGN : s_10_0 27 # ASSIGN : s_10_1 146 # ASSIGN : s_10_2 879 # ASSIGN : s_10_3 1 # ASSIGN : s_10_4 929 # ASSIGN : s_10_5 382 # ASSIGN : s_10_6 73 # ASSIGN : s_10_7 197 # ASSIGN : s_10_8 271 # ASSIGN : s_10_9 638 # ASSIGN : s_10_10 551 # ASSIGN : s_10_11 460 # ASSIGN : s_10_12 651 # ASSIGN : s_10_13 787 # ASSIGN : s_10_14 472 # ASSIGN : s_11_0 223 # ASSIGN : s_11_1 397 # ASSIGN : s_11_2 64 # ASSIGN : s_11_3 6 # ASSIGN : s_11_4 111 # ASSIGN : s_11_5 172 # ASSIGN : s_11_6 287 # ASSIGN : s_11_7 309 # ASSIGN : s_11_8 865 # ASSIGN : s_11_9 650 # ASSIGN : s_11_10 613 # ASSIGN : s_11_11 491 # ASSIGN : s_11_12 710 # ASSIGN : s_11_13 820 # ASSIGN : s_11_14 561 # ASSIGN : s_12_0 283 # ASSIGN : s_12_1 472 # ASSIGN : s_12_2 1 # ASSIGN : s_12_3 63 # ASSIGN : s_12_4 475 # ASSIGN : s_12_5 177 # ASSIGN : s_12_6 311 # ASSIGN : s_12_7 354 # ASSIGN : s_12_8 992 # ASSIGN : s_12_9 731 # ASSIGN : s_12_10 633 # ASSIGN : s_12_11 515 # ASSIGN : s_12_12 770 # ASSIGN : s_12_13 864 # ASSIGN : s_12_14 595 # ASSIGN : s_13_0 9 # ASSIGN : s_13_1 23 # ASSIGN : s_13_2 197 # ASSIGN : s_13_3 113 # ASSIGN : s_13_4 311 # ASSIGN : s_13_5 224 # ASSIGN : s_13_6 346 # ASSIGN : s_13_7 450 # ASSIGN : s_13_8 543 # ASSIGN : s_13_9 784 # ASSIGN : s_13_10 723 # ASSIGN : s_13_11 670 # ASSIGN : s_13_12 861 # ASSIGN : s_13_13 959 # ASSIGN : s_13_14 641 # ASSIGN : s_14_0 294 # ASSIGN : s_14_1 500 # ASSIGN : s_14_2 382 # ASSIGN : s_14_3 459 # ASSIGN : s_14_4 513 # ASSIGN : s_14_5 564 # ASSIGN : s_14_6 600 # ASSIGN : s_14_7 734 # ASSIGN : s_14_8 66 # ASSIGN : s_14_9 848 # ASSIGN : s_14_10 781 # ASSIGN : s_14_11 748 # ASSIGN : s_14_12 944 # ASSIGN : s_14_13 996 # ASSIGN : s_14_14 688 SHOW_RESULT 1026 END : 1026 (1 seconds) [Mon Jun 19 14:20:07 2006] SHOW_RESULT 1026 CPU : 1.17 = 1.13 + 0.04 + 0 + 0 # BOUND : makespan 899 1026 MODIFY_CNF 962 BEGIN : [Mon Jun 19 14:20:07 2006] MODIFY_CNF 962 END : 215840567 bytes (0 seconds) [Mon Jun 19 14:20:07 2006] MODIFY_CNF 962 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 962 BEGIN : [Mon Jun 19 14:20:07 2006] CMD : minisat /tmp/csp2sat32182.cnf /tmp/csp2sat32182.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 6187605 18250688 | 2062535 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 48 (3 /sec) decisions : 1688 (95 /sec) propagations : 699588 (39237 /sec) conflict literals : 619 (3.73 % deleted) Memory used : 365.45 MB CPU time : 17.83 s SATISFIABLE VERIFY_CNF 962 END : (19 seconds) [Mon Jun 19 14:20:26 2006] VERIFY_CNF 962 CPU : 19.14 = 0 + 0 + 17.99 + 1.15 # RESULT : makespan 962 SATISFIABLE SHOW_RESULT 962 BEGIN : [Mon Jun 19 14:20:26 2006] # ASSIGN : makespan 962 # ASSIGN : s_0_0 321 # ASSIGN : s_0_1 4 # ASSIGN : s_0_2 360 # ASSIGN : s_0_3 568 # ASSIGN : s_0_4 421 # ASSIGN : s_0_5 600 # ASSIGN : s_0_6 236 # ASSIGN : s_0_7 10 # ASSIGN : s_0_8 245 # ASSIGN : s_0_9 466 # ASSIGN : s_0_10 820 # ASSIGN : s_0_11 0 # ASSIGN : s_0_12 89 # ASSIGN : s_0_13 100 # ASSIGN : s_0_14 34 # ASSIGN : s_1_0 403 # ASSIGN : s_1_1 558 # ASSIGN : s_1_2 676 # ASSIGN : s_1_3 7 # ASSIGN : s_1_4 381 # ASSIGN : s_1_5 492 # ASSIGN : s_1_6 6 # ASSIGN : s_1_7 615 # ASSIGN : s_1_8 870 # ASSIGN : s_1_9 143 # ASSIGN : s_1_10 759 # ASSIGN : s_1_11 355 # ASSIGN : s_1_12 129 # ASSIGN : s_1_13 197 # ASSIGN : s_1_14 67 # ASSIGN : s_2_0 81 # ASSIGN : s_2_1 256 # ASSIGN : s_2_2 355 # ASSIGN : s_2_3 616 # ASSIGN : s_2_4 537 # ASSIGN : s_2_5 475 # ASSIGN : s_2_6 384 # ASSIGN : s_2_7 746 # ASSIGN : s_2_8 835 # ASSIGN : s_2_9 865 # ASSIGN : s_2_10 701 # ASSIGN : s_2_11 51 # ASSIGN : s_2_12 152 # ASSIGN : s_2_13 267 # ASSIGN : s_2_14 202 # ASSIGN : s_3_0 173 # ASSIGN : s_3_1 618 # ASSIGN : s_3_2 551 # ASSIGN : s_3_3 60 # ASSIGN : s_3_4 252 # ASSIGN : s_3_5 589 # ASSIGN : s_3_6 490 # ASSIGN : s_3_7 873 # ASSIGN : s_3_8 691 # ASSIGN : s_3_9 787 # ASSIGN : s_3_10 636 # ASSIGN : s_3_11 434 # ASSIGN : s_3_12 161 # ASSIGN : s_3_13 332 # ASSIGN : s_3_14 240 # ASSIGN : s_4_0 329 # ASSIGN : s_4_1 277 # ASSIGN : s_4_2 279 # ASSIGN : s_4_3 315 # ASSIGN : s_4_4 878 # ASSIGN : s_4_5 155 # ASSIGN : s_4_6 371 # ASSIGN : s_4_7 34 # ASSIGN : s_4_8 554 # ASSIGN : s_4_9 711 # ASSIGN : s_4_10 628 # ASSIGN : s_4_11 796 # ASSIGN : s_4_12 176 # ASSIGN : s_4_13 427 # ASSIGN : s_4_14 307 # ASSIGN : s_5_0 445 # ASSIGN : s_5_1 10 # ASSIGN : s_5_2 72 # ASSIGN : s_5_3 869 # ASSIGN : s_5_4 165 # ASSIGN : s_5_5 768 # ASSIGN : s_5_6 662 # ASSIGN : s_5_7 44 # ASSIGN : s_5_8 508 # ASSIGN : s_5_9 580 # ASSIGN : s_5_10 606 # ASSIGN : s_5_11 380 # ASSIGN : s_5_12 211 # ASSIGN : s_5_13 434 # ASSIGN : s_5_14 308 # ASSIGN : s_6_0 621 # ASSIGN : s_6_1 634 # ASSIGN : s_6_2 750 # ASSIGN : s_6_3 713 # ASSIGN : s_6_4 213 # ASSIGN : s_6_5 850 # ASSIGN : s_6_6 272 # ASSIGN : s_6_7 66 # ASSIGN : s_6_8 0 # ASSIGN : s_6_9 650 # ASSIGN : s_6_10 512 # ASSIGN : s_6_11 211 # ASSIGN : s_6_12 254 # ASSIGN : s_6_13 443 # ASSIGN : s_6_14 381 # ASSIGN : s_7_0 777 # ASSIGN : s_7_1 0 # ASSIGN : s_7_2 834 # ASSIGN : s_7_3 343 # ASSIGN : s_7_4 105 # ASSIGN : s_7_5 683 # ASSIGN : s_7_6 24 # ASSIGN : s_7_7 160 # ASSIGN : s_7_8 651 # ASSIGN : s_7_9 586 # ASSIGN : s_7_10 394 # ASSIGN : s_7_11 923 # ASSIGN : s_7_12 284 # ASSIGN : s_7_13 514 # ASSIGN : s_7_14 450 # ASSIGN : s_8_0 0 # ASSIGN : s_8_1 164 # ASSIGN : s_8_2 466 # ASSIGN : s_8_3 600 # ASSIGN : s_8_4 703 # ASSIGN : s_8_5 443 # ASSIGN : s_8_6 846 # ASSIGN : s_8_7 250 # ASSIGN : s_8_8 796 # ASSIGN : s_8_9 558 # ASSIGN : s_8_10 919 # ASSIGN : s_8_11 128 # ASSIGN : s_8_12 349 # ASSIGN : s_8_13 611 # ASSIGN : s_8_14 525 # ASSIGN : s_9_0 225 # ASSIGN : s_9_1 14 # ASSIGN : s_9_2 0 # ASSIGN : s_9_3 155 # ASSIGN : s_9_4 786 # ASSIGN : s_9_5 935 # ASSIGN : s_9_6 714 # ASSIGN : s_9_7 353 # ASSIGN : s_9_8 89 # ASSIGN : s_9_9 960 # ASSIGN : s_9_10 310 # ASSIGN : s_9_11 10 # ASSIGN : s_9_12 444 # ASSIGN : s_9_13 651 # ASSIGN : s_9_14 571 # ASSIGN : s_10_0 110 # ASSIGN : s_10_1 861 # ASSIGN : s_10_2 912 # ASSIGN : s_10_3 338 # ASSIGN : s_10_4 8 # ASSIGN : s_10_5 350 # ASSIGN : s_10_6 786 # ASSIGN : s_10_7 428 # ASSIGN : s_10_8 156 # ASSIGN : s_10_9 529 # ASSIGN : s_10_10 248 # ASSIGN : s_10_11 517 # ASSIGN : s_10_12 541 # ASSIGN : s_10_13 723 # ASSIGN : s_10_14 643 # ASSIGN : s_11_0 902 # ASSIGN : s_11_1 89 # ASSIGN : s_11_2 435 # ASSIGN : s_11_3 812 # ASSIGN : s_11_4 683 # ASSIGN : s_11_5 547 # ASSIGN : s_11_6 468 # ASSIGN : s_11_7 502 # ASSIGN : s_11_8 271 # ASSIGN : s_11_9 509 # ASSIGN : s_11_10 228 # ASSIGN : s_11_11 410 # ASSIGN : s_11_12 600 # ASSIGN : s_11_13 756 # ASSIGN : s_11_14 722 # ASSIGN : s_12_0 310 # ASSIGN : s_12_1 1 # ASSIGN : s_12_2 10 # ASSIGN : s_12_3 469 # ASSIGN : s_12_4 622 # ASSIGN : s_12_5 91 # ASSIGN : s_12_6 927 # ASSIGN : s_12_7 519 # ASSIGN : s_12_8 332 # ASSIGN : s_12_9 427 # ASSIGN : s_12_10 138 # ASSIGN : s_12_11 230 # ASSIGN : s_12_12 660 # ASSIGN : s_12_13 800 # ASSIGN : s_12_14 762 # ASSIGN : s_13_0 843 # ASSIGN : s_13_1 464 # ASSIGN : s_13_2 199 # ASSIGN : s_13_3 226 # ASSIGN : s_13_4 331 # ASSIGN : s_13_5 5 # ASSIGN : s_13_6 554 # ASSIGN : s_13_7 653 # ASSIGN : s_13_8 366 # ASSIGN : s_13_9 310 # ASSIGN : s_13_10 80 # ASSIGN : s_13_11 146 # ASSIGN : s_13_12 751 # ASSIGN : s_13_13 895 # ASSIGN : s_13_14 857 # ASSIGN : s_14_0 665 # ASSIGN : s_14_1 807 # ASSIGN : s_14_2 588 # ASSIGN : s_14_3 428 # ASSIGN : s_14_4 486 # ASSIGN : s_14_5 552 # ASSIGN : s_14_6 148 # ASSIGN : s_14_7 820 # ASSIGN : s_14_8 786 # ASSIGN : s_14_9 331 # ASSIGN : s_14_10 13 # ASSIGN : s_14_11 753 # ASSIGN : s_14_12 834 # ASSIGN : s_14_13 932 # ASSIGN : s_14_14 886 SHOW_RESULT 962 END : 962 (1 seconds) [Mon Jun 19 14:20:27 2006] SHOW_RESULT 962 CPU : 1.17 = 1.12 + 0.0499999999999998 + 0 + 0 # BOUND : makespan 899 962 MODIFY_CNF 930 BEGIN : [Mon Jun 19 14:20:27 2006] MODIFY_CNF 930 END : 215840567 bytes (0 seconds) [Mon Jun 19 14:20:27 2006] MODIFY_CNF 930 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 930 BEGIN : [Mon Jun 19 14:20:27 2006] CMD : minisat /tmp/csp2sat32182.cnf /tmp/csp2sat32182.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 5986005 17645888 | 1995335 0 0 nan | 0.000 % | | 101 | 5986005 17645888 | 2194868 101 1548 15.3 | 36.929 % | ============================================================================== restarts : 2 conflicts : 196 (10 /sec) decisions : 2051 (102 /sec) propagations : 958923 (47542 /sec) conflict literals : 3157 (7.82 % deleted) Memory used : 365.47 MB CPU time : 20.17 s SATISFIABLE VERIFY_CNF 930 END : (21 seconds) [Mon Jun 19 14:20:48 2006] VERIFY_CNF 930 CPU : 21.34 = 0.00999999999999091 + 0 + 20.32 + 1.01 # RESULT : makespan 930 SATISFIABLE SHOW_RESULT 930 BEGIN : [Mon Jun 19 14:20:48 2006] # ASSIGN : makespan 930 # ASSIGN : s_0_0 144 # ASSIGN : s_0_1 728 # ASSIGN : s_0_2 520 # ASSIGN : s_0_3 445 # ASSIGN : s_0_4 350 # ASSIGN : s_0_5 602 # ASSIGN : s_0_6 62 # ASSIGN : s_0_7 793 # ASSIGN : s_0_8 767 # ASSIGN : s_0_9 685 # ASSIGN : s_0_10 180 # ASSIGN : s_0_11 926 # ASSIGN : s_0_12 818 # ASSIGN : s_0_13 829 # ASSIGN : s_0_14 734 # ASSIGN : s_1_0 814 # ASSIGN : s_1_1 120 # ASSIGN : s_1_2 856 # ASSIGN : s_1_3 223 # ASSIGN : s_1_4 395 # ASSIGN : s_1_5 759 # ASSIGN : s_1_6 341 # ASSIGN : s_1_7 82 # ASSIGN : s_1_8 468 # ASSIGN : s_1_9 28 # ASSIGN : s_1_10 279 # ASSIGN : s_1_11 443 # ASSIGN : s_1_12 381 # ASSIGN : s_1_13 585 # ASSIGN : s_1_14 672 # ASSIGN : s_2_0 332 # ASSIGN : s_2_1 361 # ASSIGN : s_2_2 3 # ASSIGN : s_2_3 720 # ASSIGN : s_2_4 90 # ASSIGN : s_2_5 828 # ASSIGN : s_2_6 170 # ASSIGN : s_2_7 8 # ASSIGN : s_2_8 560 # ASSIGN : s_2_9 385 # ASSIGN : s_2_10 863 # ASSIGN : s_2_11 599 # ASSIGN : s_2_12 372 # ASSIGN : s_2_13 480 # ASSIGN : s_2_14 634 # ASSIGN : s_3_0 277 # ASSIGN : s_3_1 261 # ASSIGN : s_3_2 581 # ASSIGN : s_3_3 61 # ASSIGN : s_3_4 169 # ASSIGN : s_3_5 158 # ASSIGN : s_3_6 0 # ASSIGN : s_3_7 630 # ASSIGN : s_3_8 835 # ASSIGN : s_3_9 728 # ASSIGN : s_3_10 497 # ASSIGN : s_3_11 329 # ASSIGN : s_3_12 806 # ASSIGN : s_3_13 385 # ASSIGN : s_3_14 618 # ASSIGN : s_4_0 235 # ASSIGN : s_4_1 4 # ASSIGN : s_4_2 478 # ASSIGN : s_4_3 156 # ASSIGN : s_4_4 6 # ASSIGN : s_4_5 506 # ASSIGN : s_4_6 562 # ASSIGN : s_4_7 120 # ASSIGN : s_4_8 693 # ASSIGN : s_4_9 609 # ASSIGN : s_4_10 340 # ASSIGN : s_4_11 844 # ASSIGN : s_4_12 771 # ASSIGN : s_4_13 378 # ASSIGN : s_4_14 929 # ASSIGN : s_5_0 13 # ASSIGN : s_5_1 9 # ASSIGN : s_5_2 625 # ASSIGN : s_5_3 276 # ASSIGN : s_5_4 500 # ASSIGN : s_5_5 173 # ASSIGN : s_5_6 415 # ASSIGN : s_5_7 393 # ASSIGN : s_5_8 76 # ASSIGN : s_5_9 270 # ASSIGN : s_5_10 908 # ASSIGN : s_5_11 814 # ASSIGN : s_5_12 728 # ASSIGN : s_5_13 369 # ASSIGN : s_5_14 546 # ASSIGN : s_6_0 720 # ASSIGN : s_6_1 740 # ASSIGN : s_6_2 394 # ASSIGN : s_6_3 170 # ASSIGN : s_6_4 549 # ASSIGN : s_6_5 845 # ASSIGN : s_6_6 71 # ASSIGN : s_6_7 224 # ASSIGN : s_6_8 5 # ASSIGN : s_6_9 324 # ASSIGN : s_6_10 608 # ASSIGN : s_6_11 482 # ASSIGN : s_6_12 702 # ASSIGN : s_6_13 760 # ASSIGN : s_6_14 484 # ASSIGN : s_7_0 873 # ASSIGN : s_7_1 0 # ASSIGN : s_7_2 52 # ASSIGN : s_7_3 1 # ASSIGN : s_7_4 818 # ASSIGN : s_7_5 335 # ASSIGN : s_7_6 254 # ASSIGN : s_7_7 130 # ASSIGN : s_7_8 220 # ASSIGN : s_7_9 488 # ASSIGN : s_7_10 552 # ASSIGN : s_7_11 770 # ASSIGN : s_7_12 629 # ASSIGN : s_7_13 688 # ASSIGN : s_7_14 420 # ASSIGN : s_8_0 733 # ASSIGN : s_8_1 629 # ASSIGN : s_8_2 243 # ASSIGN : s_8_3 207 # ASSIGN : s_8_4 417 # ASSIGN : s_8_5 312 # ASSIGN : s_8_6 342 # ASSIGN : s_8_7 817 # ASSIGN : s_8_8 590 # ASSIGN : s_8_9 98 # ASSIGN : s_8_10 131 # ASSIGN : s_8_11 715 # ASSIGN : s_8_12 4 # ASSIGN : s_8_13 545 # ASSIGN : s_8_14 174 # ASSIGN : s_9_0 393 # ASSIGN : s_9_1 177 # ASSIGN : s_9_2 9 # ASSIGN : s_9_3 647 # ASSIGN : s_9_4 717 # ASSIGN : s_9_5 19 # ASSIGN : s_9_6 575 # ASSIGN : s_9_7 318 # ASSIGN : s_9_8 252 # ASSIGN : s_9_9 928 # ASSIGN : s_9_10 813 # ASSIGN : s_9_11 809 # ASSIGN : s_9_12 478 # ASSIGN : s_9_13 114 # ASSIGN : s_9_14 856 # ASSIGN : s_10_0 508 # ASSIGN : s_10_1 578 # ASSIGN : s_10_2 162 # ASSIGN : s_10_3 218 # ASSIGN : s_10_4 248 # ASSIGN : s_10_5 80 # ASSIGN : s_10_6 797 # ASSIGN : s_10_7 719 # ASSIGN : s_10_8 345 # ASSIGN : s_10_9 554 # ASSIGN : s_10_10 435 # ASSIGN : s_10_11 566 # ASSIGN : s_10_12 871 # ASSIGN : s_10_13 655 # ASSIGN : s_10_14 1 # ASSIGN : s_11_0 152 # ASSIGN : s_11_1 45 # ASSIGN : s_11_2 212 # ASSIGN : s_11_3 388 # ASSIGN : s_11_4 588 # ASSIGN : s_11_5 3 # ASSIGN : s_11_6 908 # ASSIGN : s_11_7 623 # ASSIGN : s_11_8 632 # ASSIGN : s_11_9 8 # ASSIGN : s_11_10 703 # ASSIGN : s_11_11 244 # ASSIGN : s_11_12 312 # ASSIGN : s_11_13 268 # ASSIGN : s_11_14 784 # ASSIGN : s_12_0 709 # ASSIGN : s_12_1 16 # ASSIGN : s_12_2 302 # ASSIGN : s_12_3 477 # ASSIGN : s_12_4 892 # ASSIGN : s_12_5 255 # ASSIGN : s_12_6 857 # ASSIGN : s_12_7 527 # ASSIGN : s_12_8 434 # ASSIGN : s_12_9 216 # ASSIGN : s_12_10 723 # ASSIGN : s_12_11 629 # ASSIGN : s_12_12 125 # ASSIGN : s_12_13 19 # ASSIGN : s_12_14 818 # ASSIGN : s_13_0 643 # ASSIGN : s_13_1 756 # ASSIGN : s_13_2 364 # ASSIGN : s_13_3 846 # ASSIGN : s_13_4 608 # ASSIGN : s_13_5 527 # ASSIGN : s_13_6 657 # ASSIGN : s_13_7 434 # ASSIGN : s_13_8 122 # ASSIGN : s_13_9 303 # ASSIGN : s_13_10 64 # ASSIGN : s_13_11 11 # ASSIGN : s_13_12 220 # ASSIGN : s_13_13 327 # ASSIGN : s_13_14 391 # ASSIGN : s_14_0 555 # ASSIGN : s_14_1 31 # ASSIGN : s_14_2 718 # ASSIGN : s_14_3 805 # ASSIGN : s_14_4 666 # ASSIGN : s_14_5 44 # ASSIGN : s_14_6 467 # ASSIGN : s_14_7 916 # ASSIGN : s_14_8 795 # ASSIGN : s_14_9 120 # ASSIGN : s_14_10 348 # ASSIGN : s_14_11 269 # ASSIGN : s_14_12 415 # ASSIGN : s_14_13 238 # ASSIGN : s_14_14 302 SHOW_RESULT 930 END : 930 (2 seconds) [Mon Jun 19 14:20:50 2006] SHOW_RESULT 930 CPU : 1.14999999999999 = 1.13999999999999 + 0.01 + 0 + 0 # BOUND : makespan 899 930 MODIFY_CNF 914 BEGIN : [Mon Jun 19 14:20:50 2006] MODIFY_CNF 914 END : 215840567 bytes (0 seconds) [Mon Jun 19 14:20:50 2006] MODIFY_CNF 914 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 914 BEGIN : [Mon Jun 19 14:20:50 2006] CMD : minisat /tmp/csp2sat32182.cnf /tmp/csp2sat32182.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 5885205 17343488 | 1961735 0 0 nan | 0.000 % | | 100 | 5885205 17343488 | 2157908 100 3224 32.2 | 38.044 % | ============================================================================== restarts : 2 conflicts : 170 (8 /sec) decisions : 1788 (82 /sec) propagations : 1277417 (58597 /sec) conflict literals : 4285 (6.58 % deleted) Memory used : 365.47 MB CPU time : 21.8 s SATISFIABLE VERIFY_CNF 914 END : (23 seconds) [Mon Jun 19 14:21:13 2006] VERIFY_CNF 914 CPU : 23.11 = 0 + 0.01 + 21.98 + 1.12 # RESULT : makespan 914 SATISFIABLE SHOW_RESULT 914 BEGIN : [Mon Jun 19 14:21:13 2006] # ASSIGN : makespan 914 # ASSIGN : s_0_0 11 # ASSIGN : s_0_1 207 # ASSIGN : s_0_2 19 # ASSIGN : s_0_3 311 # ASSIGN : s_0_4 213 # ASSIGN : s_0_5 742 # ASSIGN : s_0_6 554 # ASSIGN : s_0_7 500 # ASSIGN : s_0_8 842 # ASSIGN : s_0_9 604 # ASSIGN : s_0_10 383 # ASSIGN : s_0_11 106 # ASSIGN : s_0_12 530 # ASSIGN : s_0_13 110 # ASSIGN : s_0_14 880 # ASSIGN : s_1_0 710 # ASSIGN : s_1_1 488 # ASSIGN : s_1_2 325 # ASSIGN : s_1_3 9 # ASSIGN : s_1_4 640 # ASSIGN : s_1_5 399 # ASSIGN : s_1_6 167 # ASSIGN : s_1_7 599 # ASSIGN : s_1_8 62 # ASSIGN : s_1_9 545 # ASSIGN : s_1_10 183 # ASSIGN : s_1_11 752 # ASSIGN : s_1_12 668 # ASSIGN : s_1_13 255 # ASSIGN : s_1_14 818 # ASSIGN : s_2_0 425 # ASSIGN : s_2_1 19 # ASSIGN : s_2_2 4 # ASSIGN : s_2_3 226 # ASSIGN : s_2_4 40 # ASSIGN : s_2_5 454 # ASSIGN : s_2_6 830 # ASSIGN : s_2_7 741 # ASSIGN : s_2_8 317 # ASSIGN : s_2_9 119 # ASSIGN : s_2_10 525 # ASSIGN : s_2_11 629 # ASSIGN : s_2_12 659 # ASSIGN : s_2_13 348 # ASSIGN : s_2_14 471 # ASSIGN : s_3_0 263 # ASSIGN : s_3_1 3 # ASSIGN : s_3_2 225 # ASSIGN : s_3_3 398 # ASSIGN : s_3_4 835 # ASSIGN : s_3_5 140 # ASSIGN : s_3_6 493 # ASSIGN : s_3_7 651 # ASSIGN : s_3_8 740 # ASSIGN : s_3_9 318 # ASSIGN : s_3_10 80 # ASSIGN : s_3_11 153 # ASSIGN : s_3_12 209 # ASSIGN : s_3_13 556 # ASSIGN : s_3_14 20 # ASSIGN : s_4_0 580 # ASSIGN : s_4_1 30 # ASSIGN : s_4_2 262 # ASSIGN : s_4_3 343 # ASSIGN : s_4_4 747 # ASSIGN : s_4_5 9 # ASSIGN : s_4_6 563 # ASSIGN : s_4_7 290 # ASSIGN : s_4_8 154 # ASSIGN : s_4_9 43 # ASSIGN : s_4_10 35 # ASSIGN : s_4_11 831 # ASSIGN : s_4_12 392 # ASSIGN : s_4_13 676 # ASSIGN : s_4_14 913 # ASSIGN : s_5_0 36 # ASSIGN : s_5_1 317 # ASSIGN : s_5_2 709 # ASSIGN : s_5_3 553 # ASSIGN : s_5_4 662 # ASSIGN : s_5_5 151 # ASSIGN : s_5_6 99 # ASSIGN : s_5_7 471 # ASSIGN : s_5_8 868 # ASSIGN : s_5_9 7 # ASSIGN : s_5_10 13 # ASSIGN : s_5_11 523 # ASSIGN : s_5_12 349 # ASSIGN : s_5_13 339 # ASSIGN : s_5_14 399 # ASSIGN : s_6_0 398 # ASSIGN : s_6_1 217 # ASSIGN : s_6_2 482 # ASSIGN : s_6_3 877 # ASSIGN : s_6_4 708 # ASSIGN : s_6_5 233 # ASSIGN : s_6_6 0 # ASSIGN : s_6_7 103 # ASSIGN : s_6_8 566 # ASSIGN : s_6_9 647 # ASSIGN : s_6_10 764 # ASSIGN : s_6_11 411 # ASSIGN : s_6_12 318 # ASSIGN : s_6_13 413 # ASSIGN : s_6_14 336 # ASSIGN : s_7_0 801 # ASSIGN : s_7_1 0 # ASSIGN : s_7_2 404 # ASSIGN : s_7_3 730 # ASSIGN : s_7_4 278 # ASSIGN : s_7_5 564 # ASSIGN : s_7_6 649 # ASSIGN : s_7_7 1 # ASSIGN : s_7_8 372 # ASSIGN : s_7_9 214 # ASSIGN : s_7_10 858 # ASSIGN : s_7_11 333 # ASSIGN : s_7_12 91 # ASSIGN : s_7_13 484 # ASSIGN : s_7_14 150 # ASSIGN : s_8_0 315 # ASSIGN : s_8_1 396 # ASSIGN : s_8_2 650 # ASSIGN : s_8_3 532 # ASSIGN : s_8_4 130 # ASSIGN : s_8_5 87 # ASSIGN : s_8_6 576 # ASSIGN : s_8_7 815 # ASSIGN : s_8_8 23 # ASSIGN : s_8_9 775 # ASSIGN : s_8_10 482 # ASSIGN : s_8_11 797 # ASSIGN : s_8_12 221 # ASSIGN : s_8_13 716 # ASSIGN : s_8_14 543 # ASSIGN : s_9_0 178 # ASSIGN : s_9_1 32 # ASSIGN : s_9_2 9 # ASSIGN : s_9_3 781 # ASSIGN : s_9_4 335 # ASSIGN : s_9_5 110 # ASSIGN : s_9_6 263 # ASSIGN : s_9_7 524 # ASSIGN : s_9_8 674 # ASSIGN : s_9_9 773 # ASSIGN : s_9_10 135 # ASSIGN : s_9_11 777 # ASSIGN : s_9_12 427 # ASSIGN : s_9_13 851 # ASSIGN : s_9_14 602 # ASSIGN : s_10_0 122 # ASSIGN : s_10_1 632 # ASSIGN : s_10_2 802 # ASSIGN : s_10_3 105 # ASSIGN : s_10_4 473 # ASSIGN : s_10_5 319 # ASSIGN : s_10_6 168 # ASSIGN : s_10_7 397 # ASSIGN : s_10_8 228 # ASSIGN : s_10_9 31 # ASSIGN : s_10_10 570 # ASSIGN : s_10_11 110 # ASSIGN : s_10_12 855 # ASSIGN : s_10_13 683 # ASSIGN : s_10_14 723 # ASSIGN : s_11_0 622 # ASSIGN : s_11_1 321 # ASSIGN : s_11_2 588 # ASSIGN : s_11_3 119 # ASSIGN : s_11_4 258 # ASSIGN : s_11_5 909 # ASSIGN : s_11_6 471 # ASSIGN : s_11_7 493 # ASSIGN : s_11_8 407 # ASSIGN : s_11_9 798 # ASSIGN : s_11_10 60 # ASSIGN : s_11_11 82 # ASSIGN : s_11_12 682 # ASSIGN : s_11_13 211 # ASSIGN : s_11_14 509 # ASSIGN : s_12_0 101 # ASSIGN : s_12_1 485 # ASSIGN : s_12_2 852 # ASSIGN : s_12_3 176 # ASSIGN : s_12_4 435 # ASSIGN : s_12_5 494 # ASSIGN : s_12_6 228 # ASSIGN : s_12_7 300 # ASSIGN : s_12_8 632 # ASSIGN : s_12_9 396 # ASSIGN : s_12_10 666 # ASSIGN : s_12_11 2 # ASSIGN : s_12_12 541 # ASSIGN : s_12_13 756 # ASSIGN : s_12_14 112 # ASSIGN : s_13_0 900 # ASSIGN : s_13_1 107 # ASSIGN : s_13_2 619 # ASSIGN : s_13_3 646 # ASSIGN : s_13_4 5 # ASSIGN : s_13_5 825 # ASSIGN : s_13_6 369 # ASSIGN : s_13_7 197 # ASSIGN : s_13_8 468 # ASSIGN : s_13_9 290 # ASSIGN : s_13_10 311 # ASSIGN : s_13_11 566 # ASSIGN : s_13_12 742 # ASSIGN : s_13_13 41 # ASSIGN : s_13_14 78 # ASSIGN : s_14_0 485 # ASSIGN : s_14_1 573 # ASSIGN : s_14_2 80 # ASSIGN : s_14_3 357 # ASSIGN : s_14_4 586 # ASSIGN : s_14_5 661 # ASSIGN : s_14_6 730 # ASSIGN : s_14_7 637 # ASSIGN : s_14_8 347 # ASSIGN : s_14_9 818 # ASSIGN : s_14_10 244 # ASSIGN : s_14_11 697 # ASSIGN : s_14_12 157 # ASSIGN : s_14_13 2 # ASSIGN : s_14_14 32 SHOW_RESULT 914 END : 914 (1 seconds) [Mon Jun 19 14:21:14 2006] SHOW_RESULT 914 CPU : 1.17000000000002 = 1.17000000000002 + 0 + 0 + 0 # BOUND : makespan 899 914 MODIFY_CNF 906 BEGIN : [Mon Jun 19 14:21:14 2006] MODIFY_CNF 906 END : 215840566 bytes (0 seconds) [Mon Jun 19 14:21:14 2006] MODIFY_CNF 906 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 906 BEGIN : [Mon Jun 19 14:21:14 2006] CMD : minisat /tmp/csp2sat32182.cnf /tmp/csp2sat32182.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 5834805 17192288 | 1944935 0 0 nan | 0.000 % | | 100 | 5834805 17192288 | 2139428 100 3717 37.2 | 38.602 % | ============================================================================== restarts : 2 conflicts : 221 (10 /sec) decisions : 1782 (79 /sec) propagations : 1234266 (54710 /sec) conflict literals : 6045 (5.27 % deleted) Memory used : 365.48 MB CPU time : 22.56 s SATISFIABLE VERIFY_CNF 906 END : (24 seconds) [Mon Jun 19 14:21:38 2006] VERIFY_CNF 906 CPU : 23.81 = 0 + 0 + 22.7 + 1.11 # RESULT : makespan 906 SATISFIABLE SHOW_RESULT 906 BEGIN : [Mon Jun 19 14:21:38 2006] # ASSIGN : makespan 906 # ASSIGN : s_0_0 2 # ASSIGN : s_0_1 95 # ASSIGN : s_0_2 443 # ASSIGN : s_0_3 784 # ASSIGN : s_0_4 50 # ASSIGN : s_0_5 823 # ASSIGN : s_0_6 15 # ASSIGN : s_0_7 366 # ASSIGN : s_0_8 271 # ASSIGN : s_0_9 323 # ASSIGN : s_0_10 577 # ASSIGN : s_0_11 116 # ASSIGN : s_0_12 260 # ASSIGN : s_0_13 158 # ASSIGN : s_0_14 736 # ASSIGN : s_1_0 424 # ASSIGN : s_1_1 715 # ASSIGN : s_1_2 628 # ASSIGN : s_1_3 362 # ASSIGN : s_1_4 2 # ASSIGN : s_1_5 150 # ASSIGN : s_1_6 24 # ASSIGN : s_1_7 772 # ASSIGN : s_1_8 505 # ASSIGN : s_1_9 96 # ASSIGN : s_1_10 299 # ASSIGN : s_1_11 480 # ASSIGN : s_1_12 614 # ASSIGN : s_1_13 836 # ASSIGN : s_1_14 221 # ASSIGN : s_2_0 330 # ASSIGN : s_2_1 122 # ASSIGN : s_2_2 166 # ASSIGN : s_2_3 816 # ASSIGN : s_2_4 735 # ASSIGN : s_2_5 133 # ASSIGN : s_2_6 463 # ASSIGN : s_2_7 599 # ASSIGN : s_2_8 209 # ASSIGN : s_2_9 1 # ASSIGN : s_2_10 360 # ASSIGN : s_2_11 433 # ASSIGN : s_2_12 246 # ASSIGN : s_2_13 255 # ASSIGN : s_2_14 171 # ASSIGN : s_3_0 604 # ASSIGN : s_3_1 106 # ASSIGN : s_3_2 122 # ASSIGN : s_3_3 415 # ASSIGN : s_3_4 656 # ASSIGN : s_3_5 296 # ASSIGN : s_3_6 823 # ASSIGN : s_3_7 510 # ASSIGN : s_3_8 11 # ASSIGN : s_3_9 745 # ASSIGN : s_3_10 241 # ASSIGN : s_3_11 173 # ASSIGN : s_3_12 229 # ASSIGN : s_3_13 320 # ASSIGN : s_3_14 159 # ASSIGN : s_4_0 23 # ASSIGN : s_4_1 101 # ASSIGN : s_4_2 65 # ASSIGN : s_4_3 1 # ASSIGN : s_4_4 199 # ASSIGN : s_4_5 103 # ASSIGN : s_4_6 124 # ASSIGN : s_4_7 486 # ASSIGN : s_4_8 331 # ASSIGN : s_4_9 405 # ASSIGN : s_4_10 137 # ASSIGN : s_4_11 681 # ASSIGN : s_4_12 164 # ASSIGN : s_4_13 820 # ASSIGN : s_4_14 905 # ASSIGN : s_5_0 359 # ASSIGN : s_5_1 0 # ASSIGN : s_5_2 504 # ASSIGN : s_5_3 678 # ASSIGN : s_5_4 153 # ASSIGN : s_5_5 422 # ASSIGN : s_5_6 771 # ASSIGN : s_5_7 884 # ASSIGN : s_5_8 597 # ASSIGN : s_5_9 861 # ASSIGN : s_5_10 13 # ASSIGN : s_5_11 648 # ASSIGN : s_5_12 110 # ASSIGN : s_5_13 827 # ASSIGN : s_5_14 38 # ASSIGN : s_6_0 10 # ASSIGN : s_6_1 796 # ASSIGN : s_6_2 338 # ASSIGN : s_6_3 136 # ASSIGN : s_6_4 283 # ASSIGN : s_6_5 645 # ASSIGN : s_6_6 25 # ASSIGN : s_6_7 178 # ASSIGN : s_6_8 730 # ASSIGN : s_6_9 582 # ASSIGN : s_6_10 812 # ASSIGN : s_6_11 643 # ASSIGN : s_6_12 422 # ASSIGN : s_6_13 440 # ASSIGN : s_6_14 509 # ASSIGN : s_7_0 732 # ASSIGN : s_7_1 156 # ASSIGN : s_7_2 789 # ASSIGN : s_7_3 85 # ASSIGN : s_7_4 426 # ASSIGN : s_7_5 0 # ASSIGN : s_7_6 157 # ASSIGN : s_7_7 272 # ASSIGN : s_7_8 239 # ASSIGN : s_7_9 481 # ASSIGN : s_7_10 676 # ASSIGN : s_7_11 867 # ASSIGN : s_7_12 545 # ASSIGN : s_7_13 604 # ASSIGN : s_7_14 362 # ASSIGN : s_8_0 90 # ASSIGN : s_8_1 4 # ASSIGN : s_8_2 176 # ASSIGN : s_8_3 311 # ASSIGN : s_8_4 322 # ASSIGN : s_8_5 622 # ASSIGN : s_8_6 238 # ASSIGN : s_8_7 673 # ASSIGN : s_8_8 405 # ASSIGN : s_8_9 651 # ASSIGN : s_8_10 534 # ASSIGN : s_8_11 604 # ASSIGN : s_8_12 812 # ASSIGN : s_8_13 772 # ASSIGN : s_8_14 476 # ASSIGN : s_9_0 171 # ASSIGN : s_9_1 256 # ASSIGN : s_9_2 779 # ASSIGN : s_9_3 15 # ASSIGN : s_9_4 814 # ASSIGN : s_9_5 789 # ASSIGN : s_9_6 331 # ASSIGN : s_9_7 96 # ASSIGN : s_9_8 643 # ASSIGN : s_9_9 565 # ASSIGN : s_9_10 405 # ASSIGN : s_9_11 567 # ASSIGN : s_9_12 448 # ASSIGN : s_9_13 709 # ASSIGN : s_9_14 571 # ASSIGN : s_10_0 466 # ASSIGN : s_10_1 625 # ASSIGN : s_10_2 1 # ASSIGN : s_10_3 901 # ASSIGN : s_10_4 524 # ASSIGN : s_10_5 205 # ASSIGN : s_10_6 403 # ASSIGN : s_10_7 810 # ASSIGN : s_10_8 116 # ASSIGN : s_10_9 733 # ASSIGN : s_10_10 748 # ASSIGN : s_10_11 512 # ASSIGN : s_10_12 51 # ASSIGN : s_10_13 676 # ASSIGN : s_10_14 283 # ASSIGN : s_11_0 672 # ASSIGN : s_11_1 181 # ASSIGN : s_11_2 307 # ASSIGN : s_11_3 554 # ASSIGN : s_11_4 406 # ASSIGN : s_11_5 818 # ASSIGN : s_11_6 884 # ASSIGN : s_11_7 171 # ASSIGN : s_11_8 444 # ASSIGN : s_11_9 823 # ASSIGN : s_11_10 514 # ASSIGN : s_11_11 843 # ASSIGN : s_11_12 752 # ASSIGN : s_11_13 6 # ASSIGN : s_11_14 125 # ASSIGN : s_12_0 593 # ASSIGN : s_12_1 864 # ASSIGN : s_12_2 235 # ASSIGN : s_12_3 611 # ASSIGN : s_12_4 486 # ASSIGN : s_12_5 343 # ASSIGN : s_12_6 547 # ASSIGN : s_12_7 390 # ASSIGN : s_12_8 297 # ASSIGN : s_12_9 867 # ASSIGN : s_12_10 145 # ASSIGN : s_12_11 763 # ASSIGN : s_12_12 661 # ASSIGN : s_12_13 50 # ASSIGN : s_12_14 0 # ASSIGN : s_13_0 656 # ASSIGN : s_13_1 361 # ASSIGN : s_13_2 93 # ASSIGN : s_13_3 173 # ASSIGN : s_13_4 621 # ASSIGN : s_13_5 546 # ASSIGN : s_13_6 670 # ASSIGN : s_13_7 0 # ASSIGN : s_13_8 798 # ASSIGN : s_13_9 257 # ASSIGN : s_13_10 451 # ASSIGN : s_13_11 120 # ASSIGN : s_13_12 278 # ASSIGN : s_13_13 509 # ASSIGN : s_13_14 769 # ASSIGN : s_14_0 795 # ASSIGN : s_14_1 883 # ASSIGN : s_14_2 702 # ASSIGN : s_14_3 511 # ASSIGN : s_14_4 102 # ASSIGN : s_14_5 307 # ASSIGN : s_14_6 582 # ASSIGN : s_14_7 496 # ASSIGN : s_14_8 896 # ASSIGN : s_14_9 161 # ASSIGN : s_14_10 35 # ASSIGN : s_14_11 274 # ASSIGN : s_14_12 370 # ASSIGN : s_14_13 552 # ASSIGN : s_14_14 430 SHOW_RESULT 906 END : 906 (1 seconds) [Mon Jun 19 14:21:39 2006] SHOW_RESULT 906 CPU : 1.18000000000001 = 1.18000000000001 + 0 + 0 + 0 # BOUND : makespan 899 906 MODIFY_CNF 902 BEGIN : [Mon Jun 19 14:21:39 2006] MODIFY_CNF 902 END : 215840566 bytes (0 seconds) [Mon Jun 19 14:21:39 2006] MODIFY_CNF 902 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 902 BEGIN : [Mon Jun 19 14:21:39 2006] CMD : minisat /tmp/csp2sat32182.cnf /tmp/csp2sat32182.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 5809605 17116688 | 1936535 0 0 nan | 0.000 % | | 100 | 5809605 17116688 | 2130188 100 2990 29.9 | 38.881 % | | 250 | 5809605 17116688 | 2343207 250 9262 37.0 | 38.881 % | ============================================================================== restarts : 3 conflicts : 419 (18 /sec) decisions : 2539 (107 /sec) propagations : 1916968 (80477 /sec) conflict literals : 13094 (5.34 % deleted) Memory used : 365.48 MB CPU time : 23.82 s SATISFIABLE VERIFY_CNF 902 END : (25 seconds) [Mon Jun 19 14:22:04 2006] VERIFY_CNF 902 CPU : 25.21 = 0 + 0 + 23.99 + 1.22 # RESULT : makespan 902 SATISFIABLE SHOW_RESULT 902 BEGIN : [Mon Jun 19 14:22:04 2006] # ASSIGN : makespan 902 # ASSIGN : s_0_0 762 # ASSIGN : s_0_1 770 # ASSIGN : s_0_2 776 # ASSIGN : s_0_3 7 # ASSIGN : s_0_4 274 # ASSIGN : s_0_5 191 # ASSIGN : s_0_6 138 # ASSIGN : s_0_7 541 # ASSIGN : s_0_8 699 # ASSIGN : s_0_9 837 # ASSIGN : s_0_10 442 # ASSIGN : s_0_11 92 # ASSIGN : s_0_12 127 # ASSIGN : s_0_13 602 # ASSIGN : s_0_14 158 # ASSIGN : s_1_0 200 # ASSIGN : s_1_1 397 # ASSIGN : s_1_2 516 # ASSIGN : s_1_3 849 # ASSIGN : s_1_4 173 # ASSIGN : s_1_5 794 # ASSIGN : s_1_6 705 # ASSIGN : s_1_7 601 # ASSIGN : s_1_8 43 # ASSIGN : s_1_9 318 # ASSIGN : s_1_10 706 # ASSIGN : s_1_11 372 # ASSIGN : s_1_12 159 # ASSIGN : s_1_13 248 # ASSIGN : s_1_14 454 # ASSIGN : s_2_0 242 # ASSIGN : s_2_1 826 # ASSIGN : s_2_2 93 # ASSIGN : s_2_3 376 # ASSIGN : s_2_4 731 # ASSIGN : s_2_5 874 # ASSIGN : s_2_6 291 # ASSIGN : s_2_7 639 # ASSIGN : s_2_8 204 # ASSIGN : s_2_9 461 # ASSIGN : s_2_10 556 # ASSIGN : s_2_11 169 # ASSIGN : s_2_12 150 # ASSIGN : s_2_13 0 # ASSIGN : s_2_14 601 # ASSIGN : s_3_0 139 # ASSIGN : s_3_1 563 # ASSIGN : s_3_2 7 # ASSIGN : s_3_3 44 # ASSIGN : s_3_4 591 # ASSIGN : s_3_5 891 # ASSIGN : s_3_6 375 # ASSIGN : s_3_7 191 # ASSIGN : s_3_8 280 # ASSIGN : s_3_9 679 # ASSIGN : s_3_10 836 # ASSIGN : s_3_11 780 # ASSIGN : s_3_12 760 # ASSIGN : s_3_13 468 # ASSIGN : s_3_14 579 # ASSIGN : s_4_0 718 # ASSIGN : s_4_1 467 # ASSIGN : s_4_2 98 # ASSIGN : s_4_3 828 # ASSIGN : s_4_4 4 # ASSIGN : s_4_5 358 # ASSIGN : s_4_6 147 # ASSIGN : s_4_7 281 # ASSIGN : s_4_8 475 # ASSIGN : s_4_9 379 # ASSIGN : s_4_10 894 # ASSIGN : s_4_11 199 # ASSIGN : s_4_12 772 # ASSIGN : s_4_13 842 # ASSIGN : s_4_14 760 # ASSIGN : s_5_0 25 # ASSIGN : s_5_1 469 # ASSIGN : s_5_2 590 # ASSIGN : s_5_3 283 # ASSIGN : s_5_4 88 # ASSIGN : s_5_5 712 # ASSIGN : s_5_6 513 # ASSIGN : s_5_7 565 # ASSIGN : s_5_8 234 # ASSIGN : s_5_9 455 # ASSIGN : s_5_10 814 # ASSIGN : s_5_11 483 # ASSIGN : s_5_12 859 # ASSIGN : s_5_13 849 # ASSIGN : s_5_14 382 # ASSIGN : s_6_0 4 # ASSIGN : s_6_1 357 # ASSIGN : s_6_2 273 # ASSIGN : s_6_3 471 # ASSIGN : s_6_4 134 # ASSIGN : s_6_5 620 # ASSIGN : s_6_6 35 # ASSIGN : s_6_7 373 # ASSIGN : s_6_8 774 # ASSIGN : s_6_9 559 # ASSIGN : s_6_10 179 # ASSIGN : s_6_11 549 # ASSIGN : s_6_12 17 # ASSIGN : s_6_13 705 # ASSIGN : s_6_14 840 # ASSIGN : s_7_0 436 # ASSIGN : s_7_1 579 # ASSIGN : s_7_2 358 # ASSIGN : s_7_3 580 # ASSIGN : s_7_4 670 # ASSIGN : s_7_5 493 # ASSIGN : s_7_6 821 # ASSIGN : s_7_7 2 # ASSIGN : s_7_8 725 # ASSIGN : s_7_9 757 # ASSIGN : s_7_10 107 # ASSIGN : s_7_11 631 # ASSIGN : s_7_12 299 # ASSIGN : s_7_13 163 # ASSIGN : s_7_14 235 # ASSIGN : s_8_0 285 # ASSIGN : s_8_1 199 # ASSIGN : s_8_2 717 # ASSIGN : s_8_3 688 # ASSIGN : s_8_4 485 # ASSIGN : s_8_5 462 # ASSIGN : s_8_6 568 # ASSIGN : s_8_7 92 # ASSIGN : s_8_8 841 # ASSIGN : s_8_9 880 # ASSIGN : s_8_10 2 # ASSIGN : s_8_11 699 # ASSIGN : s_8_12 366 # ASSIGN : s_8_13 801 # ASSIGN : s_8_14 642 # ASSIGN : s_9_0 603 # ASSIGN : s_9_1 692 # ASSIGN : s_9_2 53 # ASSIGN : s_9_3 508 # ASSIGN : s_9_4 810 # ASSIGN : s_9_5 578 # ASSIGN : s_9_6 436 # ASSIGN : s_9_7 298 # ASSIGN : s_9_8 135 # ASSIGN : s_9_9 28 # ASSIGN : s_9_10 767 # ASSIGN : s_9_11 688 # ASSIGN : s_9_12 201 # ASSIGN : s_9_13 373 # ASSIGN : s_9_14 63 # ASSIGN : s_10_0 856 # ASSIGN : s_10_1 286 # ASSIGN : s_10_2 223 # ASSIGN : s_10_3 39 # ASSIGN : s_10_4 370 # ASSIGN : s_10_5 113 # ASSIGN : s_10_6 641 # ASSIGN : s_10_7 467 # ASSIGN : s_10_8 549 # ASSIGN : s_10_9 274 # ASSIGN : s_10_10 45 # ASSIGN : s_10_11 844 # ASSIGN : s_10_12 701 # ASSIGN : s_10_13 337 # ASSIGN : s_10_14 761 # ASSIGN : s_11_0 376 # ASSIGN : s_11_1 124 # ASSIGN : s_11_2 485 # ASSIGN : s_11_3 699 # ASSIGN : s_11_4 571 # ASSIGN : s_11_5 853 # ASSIGN : s_11_6 13 # ASSIGN : s_11_7 291 # ASSIGN : s_11_8 638 # ASSIGN : s_11_9 298 # ASSIGN : s_11_10 618 # ASSIGN : s_11_11 756 # ASSIGN : s_11_12 64 # ASSIGN : s_11_13 858 # ASSIGN : s_11_14 537 # ASSIGN : s_12_0 826 # ASSIGN : s_12_1 837 # ASSIGN : s_12_2 840 # ASSIGN : s_12_3 233 # ASSIGN : s_12_4 195 # ASSIGN : s_12_5 305 # ASSIGN : s_12_6 160 # ASSIGN : s_12_7 713 # ASSIGN : s_12_8 9 # ASSIGN : s_12_9 636 # ASSIGN : s_12_10 352 # ASSIGN : s_12_11 551 # ASSIGN : s_12_12 460 # ASSIGN : s_12_13 65 # ASSIGN : s_12_14 675 # ASSIGN : s_13_0 271 # ASSIGN : s_13_1 473 # ASSIGN : s_13_2 683 # ASSIGN : s_13_3 149 # ASSIGN : s_13_4 236 # ASSIGN : s_13_5 21 # ASSIGN : s_13_6 710 # ASSIGN : s_13_7 809 # ASSIGN : s_13_8 375 # ASSIGN : s_13_9 0 # ASSIGN : s_13_10 288 # ASSIGN : s_13_11 96 # ASSIGN : s_13_12 600 # ASSIGN : s_13_13 563 # ASSIGN : s_13_14 346 # ASSIGN : s_14_0 499 # ASSIGN : s_14_1 626 # ASSIGN : s_14_2 126 # ASSIGN : s_14_3 766 # ASSIGN : s_14_4 319 # ASSIGN : s_14_5 402 # ASSIGN : s_14_6 203 # ASSIGN : s_14_7 587 # ASSIGN : s_14_8 892 # ASSIGN : s_14_9 30 # ASSIGN : s_14_10 639 # ASSIGN : s_14_11 859 # ASSIGN : s_14_12 807 # ASSIGN : s_14_13 438 # ASSIGN : s_14_14 714 SHOW_RESULT 902 END : 902 (1 seconds) [Mon Jun 19 14:22:05 2006] SHOW_RESULT 902 CPU : 1.22999999999998 = 1.20999999999998 + 0.02 + 0 + 0 # BOUND : makespan 899 902 MODIFY_CNF 900 BEGIN : [Mon Jun 19 14:22:06 2006] MODIFY_CNF 900 END : 215840566 bytes (0 seconds) [Mon Jun 19 14:22:06 2006] MODIFY_CNF 900 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 900 BEGIN : [Mon Jun 19 14:22:06 2006] CMD : minisat /tmp/csp2sat32182.cnf /tmp/csp2sat32182.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 5797005 17078888 | 1932335 0 0 nan | 0.000 % | | 100 | 5797005 17078888 | 2125568 100 2225 22.2 | 39.021 % | | 250 | 5797005 17078888 | 2338125 250 5418 21.7 | 39.021 % | | 475 | 5797005 17078888 | 2571937 475 11792 24.8 | 39.021 % | ============================================================================== restarts : 4 conflicts : 691 (27 /sec) decisions : 3896 (153 /sec) propagations : 2537900 (99604 /sec) conflict literals : 15543 (5.95 % deleted) Memory used : 365.48 MB CPU time : 25.48 s SATISFIABLE VERIFY_CNF 900 END : (26 seconds) [Mon Jun 19 14:22:32 2006] VERIFY_CNF 900 CPU : 26.57 = 0 + 0 + 25.66 + 0.91 # RESULT : makespan 900 SATISFIABLE SHOW_RESULT 900 BEGIN : [Mon Jun 19 14:22:32 2006] # ASSIGN : makespan 900 # ASSIGN : s_0_0 656 # ASSIGN : s_0_1 490 # ASSIGN : s_0_2 496 # ASSIGN : s_0_3 854 # ASSIGN : s_0_4 675 # ASSIGN : s_0_5 566 # ASSIGN : s_0_6 792 # ASSIGN : s_0_7 172 # ASSIGN : s_0_8 730 # ASSIGN : s_0_9 83 # ASSIGN : s_0_10 226 # ASSIGN : s_0_11 486 # ASSIGN : s_0_12 772 # ASSIGN : s_0_13 332 # ASSIGN : s_0_14 49 # ASSIGN : s_1_0 664 # ASSIGN : s_1_1 500 # ASSIGN : s_1_2 557 # ASSIGN : s_1_3 706 # ASSIGN : s_1_4 878 # ASSIGN : s_1_5 769 # ASSIGN : s_1_6 649 # ASSIGN : s_1_7 40 # ASSIGN : s_1_8 193 # ASSIGN : s_1_9 824 # ASSIGN : s_1_10 325 # ASSIGN : s_1_11 106 # ASSIGN : s_1_12 311 # ASSIGN : s_1_13 429 # ASSIGN : s_1_14 131 # ASSIGN : s_2_0 528 # ASSIGN : s_2_1 859 # ASSIGN : s_2_2 387 # ASSIGN : s_2_3 252 # ASSIGN : s_2_4 557 # ASSIGN : s_2_5 235 # ASSIGN : s_2_6 650 # ASSIGN : s_2_7 392 # ASSIGN : s_2_8 756 # ASSIGN : s_2_9 126 # ASSIGN : s_2_10 480 # ASSIGN : s_2_11 870 # ASSIGN : s_2_12 90 # ASSIGN : s_2_13 13 # ASSIGN : s_2_14 795 # ASSIGN : s_3_0 46 # ASSIGN : s_3_1 595 # ASSIGN : s_3_2 786 # ASSIGN : s_3_3 611 # ASSIGN : s_3_4 420 # ASSIGN : s_3_5 23 # ASSIGN : s_3_6 298 # ASSIGN : s_3_7 196 # ASSIGN : s_3_8 98 # ASSIGN : s_3_9 708 # ASSIGN : s_3_10 845 # ASSIGN : s_3_11 364 # ASSIGN : s_3_12 34 # ASSIGN : s_3_13 499 # ASSIGN : s_3_14 833 # ASSIGN : s_4_0 590 # ASSIGN : s_4_1 588 # ASSIGN : s_4_2 185 # ASSIGN : s_4_3 886 # ASSIGN : s_4_4 336 # ASSIGN : s_4_5 545 # ASSIGN : s_4_6 213 # ASSIGN : s_4_7 8 # ASSIGN : s_4_8 24 # ASSIGN : s_4_9 632 # ASSIGN : s_4_10 0 # ASSIGN : s_4_11 724 # ASSIGN : s_4_12 806 # ASSIGN : s_4_13 717 # ASSIGN : s_4_14 710 # ASSIGN : s_5_0 262 # ASSIGN : s_5_1 881 # ASSIGN : s_5_2 631 # ASSIGN : s_5_3 382 # ASSIGN : s_5_4 832 # ASSIGN : s_5_5 55 # ASSIGN : s_5_6 734 # ASSIGN : s_5_7 18 # ASSIGN : s_5_8 786 # ASSIGN : s_5_9 885 # ASSIGN : s_5_10 137 # ASSIGN : s_5_11 601 # ASSIGN : s_5_12 339 # ASSIGN : s_5_13 891 # ASSIGN : s_5_14 502 # ASSIGN : s_6_0 2 # ASSIGN : s_6_1 558 # ASSIGN : s_6_2 302 # ASSIGN : s_6_3 195 # ASSIGN : s_6_4 636 # ASSIGN : s_6_5 684 # ASSIGN : s_6_6 801 # ASSIGN : s_6_7 78 # ASSIGN : s_6_8 482 # ASSIGN : s_6_9 17 # ASSIGN : s_6_10 386 # ASSIGN : s_6_11 15 # ASSIGN : s_6_12 783 # ASSIGN : s_6_13 233 # ASSIGN : s_6_14 574 # ASSIGN : s_7_0 371 # ASSIGN : s_7_1 285 # ASSIGN : s_7_2 71 # ASSIGN : s_7_3 759 # ASSIGN : s_7_4 1 # ASSIGN : s_7_5 286 # ASSIGN : s_7_6 467 # ASSIGN : s_7_7 810 # ASSIGN : s_7_8 548 # ASSIGN : s_7_9 221 # ASSIGN : s_7_10 703 # ASSIGN : s_7_11 428 # ASSIGN : s_7_12 580 # ASSIGN : s_7_13 149 # ASSIGN : s_7_14 639 # ASSIGN : s_8_0 819 # ASSIGN : s_8_1 8 # ASSIGN : s_8_2 243 # ASSIGN : s_8_3 232 # ASSIGN : s_8_4 145 # ASSIGN : s_8_5 649 # ASSIGN : s_8_6 359 # ASSIGN : s_8_7 711 # ASSIGN : s_8_8 672 # ASSIGN : s_8_9 337 # ASSIGN : s_8_10 94 # ASSIGN : s_8_11 319 # ASSIGN : s_8_12 486 # ASSIGN : s_8_13 594 # ASSIGN : s_8_14 453 # ASSIGN : s_9_0 141 # ASSIGN : s_9_1 665 # ASSIGN : s_9_2 483 # ASSIGN : s_9_3 8 # ASSIGN : s_9_4 740 # ASSIGN : s_9_5 515 # ASSIGN : s_9_6 226 # ASSIGN : s_9_7 540 # ASSIGN : s_9_8 832 # ASSIGN : s_9_9 898 # ASSIGN : s_9_10 622 # ASSIGN : s_9_11 493 # ASSIGN : s_9_12 386 # ASSIGN : s_9_13 78 # ASSIGN : s_9_14 314 # ASSIGN : s_10_0 325 # ASSIGN : s_10_1 790 # ASSIGN : s_10_2 416 # ASSIGN : s_10_3 549 # ASSIGN : s_10_4 228 # ASSIGN : s_10_5 150 # ASSIGN : s_10_6 90 # ASSIGN : s_10_7 466 # ASSIGN : s_10_8 583 # ASSIGN : s_10_9 5 # ASSIGN : s_10_10 28 # ASSIGN : s_10_11 571 # ASSIGN : s_10_12 841 # ASSIGN : s_10_13 678 # ASSIGN : s_10_14 711 # ASSIGN : s_11_0 439 # ASSIGN : s_11_1 364 # ASSIGN : s_11_2 40 # ASSIGN : s_11_3 554 # ASSIGN : s_11_4 720 # ASSIGN : s_11_5 679 # ASSIGN : s_11_6 168 # ASSIGN : s_11_7 1 # ASSIGN : s_11_8 285 # ASSIGN : s_11_9 804 # ASSIGN : s_11_10 825 # ASSIGN : s_11_11 530 # ASSIGN : s_11_12 190 # ASSIGN : s_11_13 634 # ASSIGN : s_11_14 866 # ASSIGN : s_12_0 713 # ASSIGN : s_12_1 897 # ASSIGN : s_12_2 724 # ASSIGN : s_12_3 475 # ASSIGN : s_12_4 56 # ASSIGN : s_12_5 385 # ASSIGN : s_12_6 432 # ASSIGN : s_12_7 615 # ASSIGN : s_12_8 346 # ASSIGN : s_12_9 298 # ASSIGN : s_12_10 525 # ASSIGN : s_12_11 218 # ASSIGN : s_12_12 99 # ASSIGN : s_12_13 796 # ASSIGN : s_12_14 11 # ASSIGN : s_13_0 499 # ASSIGN : s_13_1 195 # ASSIGN : s_13_2 2 # ASSIGN : s_13_3 111 # ASSIGN : s_13_4 513 # ASSIGN : s_13_5 825 # ASSIGN : s_13_6 548 # ASSIGN : s_13_7 285 # ASSIGN : s_13_8 380 # ASSIGN : s_13_9 478 # ASSIGN : s_13_10 767 # ASSIGN : s_13_11 29 # ASSIGN : s_13_12 647 # ASSIGN : s_13_13 730 # ASSIGN : s_13_14 82 # ASSIGN : s_14_0 731 # ASSIGN : s_14_1 652 # ASSIGN : s_14_2 823 # ASSIGN : s_14_3 337 # ASSIGN : s_14_4 94 # ASSIGN : s_14_5 461 # ASSIGN : s_14_6 2 # ASSIGN : s_14_7 378 # ASSIGN : s_14_8 720 # ASSIGN : s_14_9 536 # ASSIGN : s_14_10 159 # ASSIGN : s_14_11 497 # ASSIGN : s_14_12 250 # ASSIGN : s_14_13 302 # ASSIGN : s_14_14 407 SHOW_RESULT 900 END : 900 (1 seconds) [Mon Jun 19 14:22:33 2006] SHOW_RESULT 900 CPU : 1.16999999999999 = 1.13999999999999 + 0.03 + 0 + 0 # BOUND : makespan 899 900 MODIFY_CNF 899 BEGIN : [Mon Jun 19 14:22:33 2006] MODIFY_CNF 899 END : 215840566 bytes (0 seconds) [Mon Jun 19 14:22:33 2006] MODIFY_CNF 899 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 899 BEGIN : [Mon Jun 19 14:22:33 2006] CMD : minisat /tmp/csp2sat32182.cnf /tmp/csp2sat32182.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 5790706 17059988 | 1930235 0 0 nan | 0.000 % | | 100 | 5790706 17059988 | 2123258 100 3675 36.8 | 39.091 % | | 252 | 5790706 17059988 | 2335584 252 8028 31.9 | 39.091 % | | 478 | 5790706 17059988 | 2569142 478 14187 29.7 | 39.091 % | | 815 | 5790706 17059988 | 2826057 815 18180 22.3 | 39.091 % | ============================================================================== restarts : 5 conflicts : 1281 (48 /sec) decisions : 4185 (157 /sec) propagations : 3264429 (122677 /sec) conflict literals : 25360 (9.98 % deleted) Memory used : 365.48 MB CPU time : 26.61 s SATISFIABLE VERIFY_CNF 899 END : (28 seconds) [Mon Jun 19 14:23:01 2006] VERIFY_CNF 899 CPU : 28 = 0 + 0.01 + 26.78 + 1.21 # RESULT : makespan 899 SATISFIABLE SHOW_RESULT 899 BEGIN : [Mon Jun 19 14:23:01 2006] # ASSIGN : makespan 899 # ASSIGN : s_0_0 726 # ASSIGN : s_0_1 720 # ASSIGN : s_0_2 226 # ASSIGN : s_0_3 112 # ASSIGN : s_0_4 315 # ASSIGN : s_0_5 816 # ASSIGN : s_0_6 26 # ASSIGN : s_0_7 372 # ASSIGN : s_0_8 415 # ASSIGN : s_0_9 734 # ASSIGN : s_0_10 499 # ASSIGN : s_0_11 811 # ASSIGN : s_0_12 791 # ASSIGN : s_0_13 623 # ASSIGN : s_0_14 76 # ASSIGN : s_1_0 202 # ASSIGN : s_1_1 145 # ASSIGN : s_1_2 59 # ASSIGN : s_1_3 498 # ASSIGN : s_1_4 794 # ASSIGN : s_1_5 738 # ASSIGN : s_1_6 35 # ASSIGN : s_1_7 396 # ASSIGN : s_1_8 621 # ASSIGN : s_1_9 845 # ASSIGN : s_1_10 437 # ASSIGN : s_1_11 713 # ASSIGN : s_1_12 286 # ASSIGN : s_1_13 551 # ASSIGN : s_1_14 300 # ASSIGN : s_2_0 634 # ASSIGN : s_2_1 887 # ASSIGN : s_2_2 622 # ASSIGN : s_2_3 712 # ASSIGN : s_2_4 415 # ASSIGN : s_2_5 353 # ASSIGN : s_2_6 131 # ASSIGN : s_2_7 528 # ASSIGN : s_2_8 385 # ASSIGN : s_2_9 32 # ASSIGN : s_2_10 665 # ASSIGN : s_2_11 323 # ASSIGN : s_2_12 277 # ASSIGN : s_2_13 797 # ASSIGN : s_2_14 220 # ASSIGN : s_3_0 304 # ASSIGN : s_3_1 364 # ASSIGN : s_3_2 655 # ASSIGN : s_3_3 14 # ASSIGN : s_3_4 109 # ASSIGN : s_3_5 793 # ASSIGN : s_3_6 475 # ASSIGN : s_3_7 692 # ASSIGN : s_3_8 804 # ASSIGN : s_3_9 577 # ASSIGN : s_3_10 249 # ASSIGN : s_3_11 193 # ASSIGN : s_3_12 2 # ASSIGN : s_3_13 380 # ASSIGN : s_3_14 781 # ASSIGN : s_4_0 62 # ASSIGN : s_4_1 143 # ASSIGN : s_4_2 627 # ASSIGN : s_4_3 613 # ASSIGN : s_4_4 188 # ASSIGN : s_4_5 332 # ASSIGN : s_4_6 536 # ASSIGN : s_4_7 0 # ASSIGN : s_4_8 720 # ASSIGN : s_4_9 390 # ASSIGN : s_4_10 381 # ASSIGN : s_4_11 815 # ASSIGN : s_4_12 153 # ASSIGN : s_4_13 104 # ASSIGN : s_4_14 717 # ASSIGN : s_5_0 663 # ASSIGN : s_5_1 18 # ASSIGN : s_5_2 133 # ASSIGN : s_5_3 806 # ASSIGN : s_5_4 494 # ASSIGN : s_5_5 249 # ASSIGN : s_5_6 331 # ASSIGN : s_5_7 781 # ASSIGN : s_5_8 441 # ASSIGN : s_5_9 22 # ASSIGN : s_5_10 389 # ASSIGN : s_5_11 411 # ASSIGN : s_5_12 28 # ASSIGN : s_5_13 111 # ASSIGN : s_5_14 576 # ASSIGN : s_6_0 29 # ASSIGN : s_6_1 2 # ASSIGN : s_6_2 813 # ASSIGN : s_6_3 397 # ASSIGN : s_6_4 272 # ASSIGN : s_6_5 42 # ASSIGN : s_6_6 549 # ASSIGN : s_6_7 434 # ASSIGN : s_6_8 206 # ASSIGN : s_6_9 127 # ASSIGN : s_6_10 710 # ASSIGN : s_6_11 897 # ASSIGN : s_6_12 188 # ASSIGN : s_6_13 311 # ASSIGN : s_6_14 648 # ASSIGN : s_7_0 841 # ASSIGN : s_7_1 898 # ASSIGN : s_7_2 695 # ASSIGN : s_7_3 551 # ASSIGN : s_7_4 360 # ASSIGN : s_7_5 130 # ASSIGN : s_7_6 215 # ASSIGN : s_7_7 602 # ASSIGN : s_7_8 0 # ASSIGN : s_7_9 777 # ASSIGN : s_7_10 304 # ASSIGN : s_7_11 32 # ASSIGN : s_7_12 71 # ASSIGN : s_7_13 479 # ASSIGN : s_7_14 415 # ASSIGN : s_8_0 735 # ASSIGN : s_8_1 395 # ASSIGN : s_8_2 303 # ASSIGN : s_8_3 3 # ASSIGN : s_8_4 816 # ASSIGN : s_8_5 672 # ASSIGN : s_8_6 58 # ASSIGN : s_8_7 198 # ASSIGN : s_8_8 521 # ASSIGN : s_8_9 499 # ASSIGN : s_8_10 144 # ASSIGN : s_8_11 481 # ASSIGN : s_8_12 571 # ASSIGN : s_8_13 18 # ASSIGN : s_8_14 362 # ASSIGN : s_9_0 455 # ASSIGN : s_9_1 727 # ASSIGN : s_9_2 287 # ASSIGN : s_9_3 632 # ASSIGN : s_9_4 540 # ASSIGN : s_9_5 702 # ASSIGN : s_9_6 383 # ASSIGN : s_9_7 297 # ASSIGN : s_9_8 32 # ASSIGN : s_9_9 377 # ASSIGN : s_9_10 100 # ASSIGN : s_9_11 379 # ASSIGN : s_9_12 802 # ASSIGN : s_9_13 215 # ASSIGN : s_9_14 143 # ASSIGN : s_10_0 557 # ASSIGN : s_10_1 603 # ASSIGN : s_10_2 448 # ASSIGN : s_10_3 331 # ASSIGN : s_10_4 654 # ASSIGN : s_10_5 370 # ASSIGN : s_10_6 751 # ASSIGN : s_10_7 17 # ASSIGN : s_10_8 98 # ASSIGN : s_10_9 5 # ASSIGN : s_10_10 187 # ASSIGN : s_10_11 358 # ASSIGN : s_10_12 498 # ASSIGN : s_10_13 278 # ASSIGN : s_10_14 820 # ASSIGN : s_11_0 244 # ASSIGN : s_11_1 804 # ASSIGN : s_11_2 773 # ASSIGN : s_11_3 144 # ASSIGN : s_11_4 634 # ASSIGN : s_11_5 695 # ASSIGN : s_11_6 36 # ASSIGN : s_11_7 10 # ASSIGN : s_11_8 560 # ASSIGN : s_11_9 700 # ASSIGN : s_11_10 879 # ASSIGN : s_11_11 536 # ASSIGN : s_11_12 323 # ASSIGN : s_11_13 720 # ASSIGN : s_11_14 109 # ASSIGN : s_12_0 109 # ASSIGN : s_12_1 582 # ASSIGN : s_12_2 386 # ASSIGN : s_12_3 336 # ASSIGN : s_12_4 756 # ASSIGN : s_12_5 530 # ASSIGN : s_12_6 296 # ASSIGN : s_12_7 803 # ASSIGN : s_12_8 487 # ASSIGN : s_12_9 219 # ASSIGN : s_12_10 10 # ASSIGN : s_12_11 585 # ASSIGN : s_12_12 665 # ASSIGN : s_12_13 120 # ASSIGN : s_12_14 258 # ASSIGN : s_13_0 0 # ASSIGN : s_13_1 487 # ASSIGN : s_13_2 14 # ASSIGN : s_13_3 201 # ASSIGN : s_13_4 70 # ASSIGN : s_13_5 577 # ASSIGN : s_13_6 652 # ASSIGN : s_13_7 105 # ASSIGN : s_13_8 285 # ASSIGN : s_13_9 466 # ASSIGN : s_13_10 804 # ASSIGN : s_13_11 751 # ASSIGN : s_13_12 383 # ASSIGN : s_13_13 862 # ASSIGN : s_13_14 41 # ASSIGN : s_14_0 356 # ASSIGN : s_14_1 705 # ASSIGN : s_14_2 521 # ASSIGN : s_14_3 444 # ASSIGN : s_14_4 19 # ASSIGN : s_14_5 485 # ASSIGN : s_14_6 811 # ASSIGN : s_14_7 91 # ASSIGN : s_14_8 794 # ASSIGN : s_14_9 260 # ASSIGN : s_14_10 598 # ASSIGN : s_14_11 160 # ASSIGN : s_14_12 208 # ASSIGN : s_14_13 764 # ASSIGN : s_14_14 718 SHOW_RESULT 899 END : 899 (2 seconds) [Mon Jun 19 14:23:03 2006] SHOW_RESULT 899 CPU : 1.16000000000003 = 1.15000000000003 + 0.01 + 0 + 0 # BOUND : makespan 899 899 MAIN END : (570 seconds) [Mon Jun 19 14:23:03 2006] MAIN CPU : 567.62 = 362.49 + 1.74 + 193.42 + 9.97