# TIMEOUT 18000 MAIN BEGIN : [Mon Jun 19 13:27:12 2006] READ BEGIN : csp/tai_15x15_4.csp [Mon Jun 19 13:27:12 2006] READ END : csp/tai_15x15_4.csp (6 seconds) [Mon Jun 19 13:27:18 2006] READ CPU : 6.34 = 6.24 + 0.1 + 0 + 0 # BOUND : makespan 934 1418 GENERATE_CNF 1418 BEGIN : [Mon Jun 19 13:27:18 2006] GENERATE_CNF 1418 END : 326511 variables 9067128 clauses 217539817 bytes (350 seconds) [Mon Jun 19 13:33:08 2006] GENERATE_CNF 1418 CPU : 348.48 = 346.93 + 1.55 + 0 + 0 MODIFY_CNF 1176 BEGIN : [Mon Jun 19 13:33:08 2006] MODIFY_CNF 1176 END : 217539823 bytes (0 seconds) [Mon Jun 19 13:33:08 2006] MODIFY_CNF 1176 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1176 BEGIN : [Mon Jun 19 13:33:08 2006] CMD : minisat /tmp/csp2sat30961.cnf /tmp/csp2sat30961.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 7534648 22289366 | 2511549 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 43 (3 /sec) decisions : 1628 (109 /sec) propagations : 649474 (43501 /sec) conflict literals : 1299 (9.22 % deleted) Memory used : 368.31 MB CPU time : 14.93 s SATISFIABLE VERIFY_CNF 1176 END : (16 seconds) [Mon Jun 19 13:33:24 2006] VERIFY_CNF 1176 CPU : 16.15 = 0 + 0 + 15.08 + 1.07 # RESULT : makespan 1176 SATISFIABLE SHOW_RESULT 1176 BEGIN : [Mon Jun 19 13:33:24 2006] # ASSIGN : makespan 1176 # ASSIGN : s_0_0 311 # ASSIGN : s_0_1 241 # ASSIGN : s_0_2 150 # ASSIGN : s_0_3 509 # ASSIGN : s_0_4 15 # ASSIGN : s_0_5 562 # ASSIGN : s_0_6 680 # ASSIGN : s_0_7 765 # ASSIGN : s_0_8 885 # ASSIGN : s_0_9 896 # ASSIGN : s_0_10 1073 # ASSIGN : s_0_11 254 # ASSIGN : s_0_12 66 # ASSIGN : s_0_13 30 # ASSIGN : s_0_14 175 # ASSIGN : s_1_0 89 # ASSIGN : s_1_1 1055 # ASSIGN : s_1_2 407 # ASSIGN : s_1_3 4 # ASSIGN : s_1_4 102 # ASSIGN : s_1_5 1102 # ASSIGN : s_1_6 1163 # ASSIGN : s_1_7 505 # ASSIGN : s_1_8 623 # ASSIGN : s_1_9 730 # ASSIGN : s_1_10 765 # ASSIGN : s_1_11 312 # ASSIGN : s_1_12 148 # ASSIGN : s_1_13 155 # ASSIGN : s_1_14 240 # ASSIGN : s_2_0 491 # ASSIGN : s_2_1 3 # ASSIGN : s_2_2 117 # ASSIGN : s_2_3 1164 # ASSIGN : s_2_4 578 # ASSIGN : s_2_5 646 # ASSIGN : s_2_6 735 # ASSIGN : s_2_7 1 # ASSIGN : s_2_8 94 # ASSIGN : s_2_9 1069 # ASSIGN : s_2_10 819 # ASSIGN : s_2_11 357 # ASSIGN : s_2_12 163 # ASSIGN : s_2_13 241 # ASSIGN : s_2_14 337 # ASSIGN : s_3_0 741 # ASSIGN : s_3_1 306 # ASSIGN : s_3_2 15 # ASSIGN : s_3_3 65 # ASSIGN : s_3_4 787 # ASSIGN : s_3_5 836 # ASSIGN : s_3_6 907 # ASSIGN : s_3_7 939 # ASSIGN : s_3_8 185 # ASSIGN : s_3_9 1008 # ASSIGN : s_3_10 162 # ASSIGN : s_3_11 444 # ASSIGN : s_3_12 221 # ASSIGN : s_3_13 343 # ASSIGN : s_3_14 361 # ASSIGN : s_4_0 104 # ASSIGN : s_4_1 56 # ASSIGN : s_4_2 144 # ASSIGN : s_4_3 165 # ASSIGN : s_4_4 829 # ASSIGN : s_4_5 883 # ASSIGN : s_4_6 252 # ASSIGN : s_4_7 264 # ASSIGN : s_4_8 921 # ASSIGN : s_4_9 967 # ASSIGN : s_4_10 286 # ASSIGN : s_4_11 507 # ASSIGN : s_4_12 291 # ASSIGN : s_4_13 375 # ASSIGN : s_4_14 413 # ASSIGN : s_5_0 181 # ASSIGN : s_5_1 79 # ASSIGN : s_5_2 195 # ASSIGN : s_5_3 244 # ASSIGN : s_5_4 683 # ASSIGN : s_5_5 400 # ASSIGN : s_5_6 776 # ASSIGN : s_5_7 849 # ASSIGN : s_5_8 995 # ASSIGN : s_5_9 492 # ASSIGN : s_5_10 1120 # ASSIGN : s_5_11 541 # ASSIGN : s_5_12 525 # ASSIGN : s_5_13 404 # ASSIGN : s_5_14 555 # ASSIGN : s_6_0 226 # ASSIGN : s_6_1 151 # ASSIGN : s_6_2 227 # ASSIGN : s_6_3 340 # ASSIGN : s_6_4 1019 # ASSIGN : s_6_5 1133 # ASSIGN : s_6_6 14 # ASSIGN : s_6_7 108 # ASSIGN : s_6_8 507 # ASSIGN : s_6_9 323 # ASSIGN : s_6_10 29 # ASSIGN : s_6_11 580 # ASSIGN : s_6_12 616 # ASSIGN : s_6_13 420 # ASSIGN : s_6_14 642 # ASSIGN : s_7_0 227 # ASSIGN : s_7_1 371 # ASSIGN : s_7_2 298 # ASSIGN : s_7_3 391 # ASSIGN : s_7_4 173 # ASSIGN : s_7_5 601 # ASSIGN : s_7_6 113 # ASSIGN : s_7_7 1126 # ASSIGN : s_7_8 1075 # ASSIGN : s_7_9 250 # ASSIGN : s_7_10 216 # ASSIGN : s_7_11 663 # ASSIGN : s_7_12 639 # ASSIGN : s_7_13 482 # ASSIGN : s_7_14 738 # ASSIGN : s_8_0 292 # ASSIGN : s_8_1 397 # ASSIGN : s_8_2 495 # ASSIGN : s_8_3 455 # ASSIGN : s_8_4 1070 # ASSIGN : s_8_5 318 # ASSIGN : s_8_6 978 # ASSIGN : s_8_7 39 # ASSIGN : s_8_8 110 # ASSIGN : s_8_9 192 # ASSIGN : s_8_10 1093 # ASSIGN : s_8_11 665 # ASSIGN : s_8_12 649 # ASSIGN : s_8_13 496 # ASSIGN : s_8_14 796 # ASSIGN : s_9_0 401 # ASSIGN : s_9_1 414 # ASSIGN : s_9_2 552 # ASSIGN : s_9_3 518 # ASSIGN : s_9_4 1150 # ASSIGN : s_9_5 464 # ASSIGN : s_9_6 1067 # ASSIGN : s_9_7 317 # ASSIGN : s_9_8 5 # ASSIGN : s_9_9 110 # ASSIGN : s_9_10 980 # ASSIGN : s_9_11 758 # ASSIGN : s_9_12 668 # ASSIGN : s_9_13 593 # ASSIGN : s_9_14 866 # ASSIGN : s_10_0 404 # ASSIGN : s_10_1 459 # ASSIGN : s_10_2 675 # ASSIGN : s_10_3 558 # ASSIGN : s_10_4 1121 # ASSIGN : s_10_5 107 # ASSIGN : s_10_6 142 # ASSIGN : s_10_7 6 # ASSIGN : s_10_8 239 # ASSIGN : s_10_9 30 # ASSIGN : s_10_10 328 # ASSIGN : s_10_11 837 # ASSIGN : s_10_12 767 # ASSIGN : s_10_13 800 # ASSIGN : s_10_14 955 # ASSIGN : s_11_0 551 # ASSIGN : s_11_1 577 # ASSIGN : s_11_2 748 # ASSIGN : s_11_3 614 # ASSIGN : s_11_4 210 # ASSIGN : s_11_5 251 # ASSIGN : s_11_6 362 # ASSIGN : s_11_7 1056 # ASSIGN : s_11_8 379 # ASSIGN : s_11_9 1123 # ASSIGN : s_11_10 454 # ASSIGN : s_11_11 932 # ASSIGN : s_11_12 785 # ASSIGN : s_11_13 921 # ASSIGN : s_11_14 999 # ASSIGN : s_12_0 552 # ASSIGN : s_12_1 608 # ASSIGN : s_12_2 837 # ASSIGN : s_12_3 682 # ASSIGN : s_12_4 255 # ASSIGN : s_12_5 30 # ASSIGN : s_12_6 135 # ASSIGN : s_12_7 223 # ASSIGN : s_12_8 352 # ASSIGN : s_12_9 384 # ASSIGN : s_12_10 459 # ASSIGN : s_12_11 1018 # ASSIGN : s_12_12 877 # ASSIGN : s_12_13 953 # ASSIGN : s_12_14 1033 # ASSIGN : s_13_0 575 # ASSIGN : s_13_1 661 # ASSIGN : s_13_2 864 # ASSIGN : s_13_3 774 # ASSIGN : s_13_4 46 # ASSIGN : s_13_5 161 # ASSIGN : s_13_6 322 # ASSIGN : s_13_7 345 # ASSIGN : s_13_8 408 # ASSIGN : s_13_9 450 # ASSIGN : s_13_10 522 # ASSIGN : s_13_11 1065 # ASSIGN : s_13_12 956 # ASSIGN : s_13_13 977 # ASSIGN : s_13_14 1080 # ASSIGN : s_14_0 653 # ASSIGN : s_14_1 755 # ASSIGN : s_14_2 979 # ASSIGN : s_14_3 869 # ASSIGN : s_14_4 438 # ASSIGN : s_14_5 516 # ASSIGN : s_14_6 538 # ASSIGN : s_14_7 582 # ASSIGN : s_14_8 659 # ASSIGN : s_14_9 836 # ASSIGN : s_14_10 901 # ASSIGN : s_14_11 1088 # ASSIGN : s_14_12 994 # ASSIGN : s_14_13 1065 # ASSIGN : s_14_14 1167 SHOW_RESULT 1176 END : 1176 (0 seconds) [Mon Jun 19 13:33:24 2006] SHOW_RESULT 1176 CPU : 0.720000000000043 = 0.640000000000043 + 0.0800000000000001 + 0 + 0 # BOUND : makespan 934 1176 MODIFY_CNF 1055 BEGIN : [Mon Jun 19 13:33:24 2006] MODIFY_CNF 1055 END : 217539823 bytes (0 seconds) [Mon Jun 19 13:33:24 2006] MODIFY_CNF 1055 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1055 BEGIN : [Mon Jun 19 13:33:24 2006] CMD : minisat /tmp/csp2sat30961.cnf /tmp/csp2sat30961.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 6772348 20002466 | 2257449 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 73 (5 /sec) decisions : 1571 (98 /sec) propagations : 700096 (43756 /sec) conflict literals : 2187 (10.88 % deleted) Memory used : 368.31 MB CPU time : 16 s SATISFIABLE VERIFY_CNF 1055 END : (18 seconds) [Mon Jun 19 13:33:42 2006] VERIFY_CNF 1055 CPU : 17.46 = 0 + 0.01 + 16.14 + 1.31 # RESULT : makespan 1055 SATISFIABLE SHOW_RESULT 1055 BEGIN : [Mon Jun 19 13:33:42 2006] # ASSIGN : makespan 1055 # ASSIGN : s_0_0 396 # ASSIGN : s_0_1 51 # ASSIGN : s_0_2 371 # ASSIGN : s_0_3 2 # ASSIGN : s_0_4 188 # ASSIGN : s_0_5 522 # ASSIGN : s_0_6 742 # ASSIGN : s_0_7 797 # ASSIGN : s_0_8 142 # ASSIGN : s_0_9 300 # ASSIGN : s_0_10 165 # ASSIGN : s_0_11 998 # ASSIGN : s_0_12 218 # ASSIGN : s_0_13 11 # ASSIGN : s_0_14 67 # ASSIGN : s_1_0 486 # ASSIGN : s_1_1 817 # ASSIGN : s_1_2 204 # ASSIGN : s_1_3 629 # ASSIGN : s_1_4 440 # ASSIGN : s_1_5 690 # ASSIGN : s_1_6 292 # ASSIGN : s_1_7 513 # ASSIGN : s_1_8 590 # ASSIGN : s_1_9 721 # ASSIGN : s_1_10 864 # ASSIGN : s_1_11 2 # ASSIGN : s_1_12 305 # ASSIGN : s_1_13 47 # ASSIGN : s_1_14 132 # ASSIGN : s_2_0 250 # ASSIGN : s_2_1 464 # ASSIGN : s_2_2 10 # ASSIGN : s_2_3 1043 # ASSIGN : s_2_4 800 # ASSIGN : s_2_5 561 # ASSIGN : s_2_6 423 # ASSIGN : s_2_7 45 # ASSIGN : s_2_8 523 # ASSIGN : s_2_9 650 # ASSIGN : s_2_10 918 # ASSIGN : s_2_11 47 # ASSIGN : s_2_12 312 # ASSIGN : s_2_13 134 # ASSIGN : s_2_14 230 # ASSIGN : s_3_0 127 # ASSIGN : s_3_1 0 # ASSIGN : s_3_2 37 # ASSIGN : s_3_3 726 # ASSIGN : s_3_4 921 # ASSIGN : s_3_5 440 # ASSIGN : s_3_6 338 # ASSIGN : s_3_7 963 # ASSIGN : s_3_8 487 # ASSIGN : s_3_9 536 # ASSIGN : s_3_10 1032 # ASSIGN : s_3_11 173 # ASSIGN : s_3_12 370 # ASSIGN : s_3_13 236 # ASSIGN : s_3_14 254 # ASSIGN : s_4_0 24 # ASSIGN : s_4_1 64 # ASSIGN : s_4_2 87 # ASSIGN : s_4_3 550 # ASSIGN : s_4_4 746 # ASSIGN : s_4_5 898 # ASSIGN : s_4_6 408 # ASSIGN : s_4_7 180 # ASSIGN : s_4_8 420 # ASSIGN : s_4_9 202 # ASSIGN : s_4_10 1000 # ASSIGN : s_4_11 243 # ASSIGN : s_4_12 466 # ASSIGN : s_4_13 277 # ASSIGN : s_4_14 306 # ASSIGN : s_5_0 79 # ASSIGN : s_5_1 125 # ASSIGN : s_5_2 93 # ASSIGN : s_5_3 823 # ASSIGN : s_5_4 203 # ASSIGN : s_5_5 1008 # ASSIGN : s_5_6 924 # ASSIGN : s_5_7 609 # ASSIGN : s_5_8 699 # ASSIGN : s_5_9 1022 # ASSIGN : s_5_10 10 # ASSIGN : s_5_11 319 # ASSIGN : s_5_12 567 # ASSIGN : s_5_13 372 # ASSIGN : s_5_14 400 # ASSIGN : s_6_0 196 # ASSIGN : s_6_1 197 # ASSIGN : s_6_2 125 # ASSIGN : s_6_3 919 # ASSIGN : s_6_4 868 # ASSIGN : s_6_5 1012 # ASSIGN : s_6_6 997 # ASSIGN : s_6_7 2 # ASSIGN : s_6_8 626 # ASSIGN : s_6_9 704 # ASSIGN : s_6_10 785 # ASSIGN : s_6_11 333 # ASSIGN : s_6_12 583 # ASSIGN : s_6_13 388 # ASSIGN : s_6_14 487 # ASSIGN : s_7_0 199 # ASSIGN : s_7_1 272 # ASSIGN : s_7_2 296 # ASSIGN : s_7_3 475 # ASSIGN : s_7_4 403 # ASSIGN : s_7_5 936 # ASSIGN : s_7_6 142 # ASSIGN : s_7_7 222 # ASSIGN : s_7_8 539 # ASSIGN : s_7_9 974 # ASSIGN : s_7_10 66 # ASSIGN : s_7_11 369 # ASSIGN : s_7_12 606 # ASSIGN : s_7_13 450 # ASSIGN : s_7_14 616 # ASSIGN : s_8_0 228 # ASSIGN : s_8_1 292 # ASSIGN : s_8_2 370 # ASSIGN : s_8_3 314 # ASSIGN : s_8_4 0 # ASSIGN : s_8_5 748 # ASSIGN : s_8_6 827 # ASSIGN : s_8_7 84 # ASSIGN : s_8_8 153 # ASSIGN : s_8_9 916 # ASSIGN : s_8_10 1005 # ASSIGN : s_8_11 371 # ASSIGN : s_8_12 620 # ASSIGN : s_8_13 464 # ASSIGN : s_8_14 674 # ASSIGN : s_9_0 247 # ASSIGN : s_9_1 309 # ASSIGN : s_9_2 441 # ASSIGN : s_9_3 354 # ASSIGN : s_9_4 23 # ASSIGN : s_9_5 388 # ASSIGN : s_9_6 164 # ASSIGN : s_9_7 49 # ASSIGN : s_9_8 966 # ASSIGN : s_9_9 834 # ASSIGN : s_9_10 77 # ASSIGN : s_9_11 482 # ASSIGN : s_9_12 636 # ASSIGN : s_9_13 561 # ASSIGN : s_9_14 744 # ASSIGN : s_10_0 310 # ASSIGN : s_10_1 365 # ASSIGN : s_10_2 487 # ASSIGN : s_10_3 970 # ASSIGN : s_10_4 1026 # ASSIGN : s_10_5 5 # ASSIGN : s_10_6 45 # ASSIGN : s_10_7 156 # ASSIGN : s_10_8 877 # ASSIGN : s_10_9 756 # ASSIGN : s_10_10 185 # ASSIGN : s_10_11 571 # ASSIGN : s_10_12 726 # ASSIGN : s_10_13 689 # ASSIGN : s_10_14 833 # ASSIGN : s_11_0 499 # ASSIGN : s_11_1 517 # ASSIGN : s_11_2 560 # ASSIGN : s_11_3 241 # ASSIGN : s_11_4 66 # ASSIGN : s_11_5 309 # ASSIGN : s_11_6 376 # ASSIGN : s_11_7 432 # ASSIGN : s_11_8 848 # ASSIGN : s_11_9 597 # ASSIGN : s_11_10 661 # ASSIGN : s_11_11 666 # ASSIGN : s_11_12 744 # ASSIGN : s_11_13 733 # ASSIGN : s_11_14 878 # ASSIGN : s_12_0 500 # ASSIGN : s_12_1 548 # ASSIGN : s_12_2 668 # ASSIGN : s_12_3 117 # ASSIGN : s_12_4 296 # ASSIGN : s_12_5 40 # ASSIGN : s_12_6 393 # ASSIGN : s_12_7 400 # ASSIGN : s_12_8 779 # ASSIGN : s_12_9 434 # ASSIGN : s_12_10 701 # ASSIGN : s_12_11 764 # ASSIGN : s_12_12 836 # ASSIGN : s_12_13 812 # ASSIGN : s_12_14 912 # ASSIGN : s_13_0 523 # ASSIGN : s_13_1 601 # ASSIGN : s_13_2 695 # ASSIGN : s_13_3 17 # ASSIGN : s_13_4 107 # ASSIGN : s_13_5 163 # ASSIGN : s_13_6 253 # ASSIGN : s_13_7 276 # ASSIGN : s_13_8 806 # ASSIGN : s_13_9 392 # ASSIGN : s_13_10 339 # ASSIGN : s_13_11 787 # ASSIGN : s_13_12 938 # ASSIGN : s_13_13 850 # ASSIGN : s_13_14 959 # ASSIGN : s_14_0 622 # ASSIGN : s_14_1 706 # ASSIGN : s_14_2 787 # ASSIGN : s_14_3 209 # ASSIGN : s_14_4 628 # ASSIGN : s_14_5 141 # ASSIGN : s_14_6 1 # ASSIGN : s_14_7 881 # ASSIGN : s_14_8 45 # ASSIGN : s_14_9 169 # ASSIGN : s_14_10 261 # ASSIGN : s_14_11 802 # ASSIGN : s_14_12 975 # ASSIGN : s_14_13 952 # ASSIGN : s_14_14 1046 SHOW_RESULT 1055 END : 1055 (1 seconds) [Mon Jun 19 13:33:43 2006] SHOW_RESULT 1055 CPU : 0.72999999999997 = 0.71999999999997 + 0.01 + 0 + 0 # BOUND : makespan 934 1055 MODIFY_CNF 994 BEGIN : [Mon Jun 19 13:33:43 2006] MODIFY_CNF 994 END : 217539822 bytes (0 seconds) [Mon Jun 19 13:33:43 2006] MODIFY_CNF 994 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 994 BEGIN : [Mon Jun 19 13:33:43 2006] CMD : minisat /tmp/csp2sat30961.cnf /tmp/csp2sat30961.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 6388048 18849566 | 2129349 0 0 nan | 0.000 % | | 100 | 6388048 18849566 | 2342283 100 2382 23.8 | 32.963 % | | 250 | 6388048 18849566 | 2576512 250 4332 17.3 | 32.963 % | ============================================================================== restarts : 3 conflicts : 263 (13 /sec) decisions : 2783 (137 /sec) propagations : 1358144 (66674 /sec) conflict literals : 4410 (5.67 % deleted) Memory used : 368.34 MB CPU time : 20.37 s SATISFIABLE VERIFY_CNF 994 END : (22 seconds) [Mon Jun 19 13:34:05 2006] VERIFY_CNF 994 CPU : 21.94 = 0 + 0.01 + 20.51 + 1.42 # RESULT : makespan 994 SATISFIABLE SHOW_RESULT 994 BEGIN : [Mon Jun 19 13:34:05 2006] # ASSIGN : makespan 994 # ASSIGN : s_0_0 107 # ASSIGN : s_0_1 961 # ASSIGN : s_0_2 1 # ASSIGN : s_0_3 423 # ASSIGN : s_0_4 468 # ASSIGN : s_0_5 26 # ASSIGN : s_0_6 368 # ASSIGN : s_0_7 279 # ASSIGN : s_0_8 483 # ASSIGN : s_0_9 501 # ASSIGN : s_0_10 974 # ASSIGN : s_0_11 669 # ASSIGN : s_0_12 197 # ASSIGN : s_0_13 65 # ASSIGN : s_0_14 835 # ASSIGN : s_1_0 1 # ASSIGN : s_1_1 690 # ASSIGN : s_1_2 28 # ASSIGN : s_1_3 225 # ASSIGN : s_1_4 948 # ASSIGN : s_1_5 658 # ASSIGN : s_1_6 116 # ASSIGN : s_1_7 767 # ASSIGN : s_1_8 494 # ASSIGN : s_1_9 365 # ASSIGN : s_1_10 428 # ASSIGN : s_1_11 613 # ASSIGN : s_1_12 21 # ASSIGN : s_1_13 140 # ASSIGN : s_1_14 541 # ASSIGN : s_2_0 934 # ASSIGN : s_2_1 436 # ASSIGN : s_2_2 165 # ASSIGN : s_2_3 2 # ASSIGN : s_2_4 489 # ASSIGN : s_2_5 569 # ASSIGN : s_2_6 192 # ASSIGN : s_2_7 434 # ASSIGN : s_2_8 16 # ASSIGN : s_2_9 233 # ASSIGN : s_2_10 346 # ASSIGN : s_2_11 814 # ASSIGN : s_2_12 32 # ASSIGN : s_2_13 702 # ASSIGN : s_2_14 287 # ASSIGN : s_3_0 495 # ASSIGN : s_3_1 843 # ASSIGN : s_3_2 541 # ASSIGN : s_3_3 128 # ASSIGN : s_3_4 236 # ASSIGN : s_3_5 784 # ASSIGN : s_3_6 5 # ASSIGN : s_3_7 627 # ASSIGN : s_3_8 591 # ASSIGN : s_3_9 37 # ASSIGN : s_3_10 321 # ASSIGN : s_3_11 362 # ASSIGN : s_3_12 425 # ASSIGN : s_3_13 344 # ASSIGN : s_3_14 696 # ASSIGN : s_4_0 455 # ASSIGN : s_4_1 280 # ASSIGN : s_4_2 666 # ASSIGN : s_4_3 576 # ASSIGN : s_4_4 182 # ASSIGN : s_4_5 303 # ASSIGN : s_4_6 859 # ASSIGN : s_4_7 44 # ASSIGN : s_4_8 530 # ASSIGN : s_4_9 98 # ASSIGN : s_4_10 139 # ASSIGN : s_4_11 148 # ASSIGN : s_4_12 341 # ASSIGN : s_4_13 871 # ASSIGN : s_4_14 900 # ASSIGN : s_5_0 641 # ASSIGN : s_5_1 364 # ASSIGN : s_5_2 878 # ASSIGN : s_5_3 14 # ASSIGN : s_5_4 655 # ASSIGN : s_5_5 990 # ASSIGN : s_5_6 480 # ASSIGN : s_5_7 110 # ASSIGN : s_5_8 910 # ASSIGN : s_5_9 845 # ASSIGN : s_5_10 585 # ASSIGN : s_5_11 448 # ASSIGN : s_5_12 553 # ASSIGN : s_5_13 569 # ASSIGN : s_5_14 748 # ASSIGN : s_6_0 640 # ASSIGN : s_6_1 562 # ASSIGN : s_6_2 470 # ASSIGN : s_6_3 655 # ASSIGN : s_6_4 417 # ASSIGN : s_6_5 354 # ASSIGN : s_6_6 51 # ASSIGN : s_6_7 66 # ASSIGN : s_6_8 109 # ASSIGN : s_6_9 400 # ASSIGN : s_6_10 714 # ASSIGN : s_6_11 318 # ASSIGN : s_6_12 295 # ASSIGN : s_6_13 809 # ASSIGN : s_6_14 191 # ASSIGN : s_7_0 598 # ASSIGN : s_7_1 118 # ASSIGN : s_7_2 771 # ASSIGN : s_7_3 706 # ASSIGN : s_7_4 557 # ASSIGN : s_7_5 942 # ASSIGN : s_7_6 346 # ASSIGN : s_7_7 844 # ASSIGN : s_7_8 644 # ASSIGN : s_7_9 894 # ASSIGN : s_7_10 144 # ASSIGN : s_7_11 596 # ASSIGN : s_7_12 621 # ASSIGN : s_7_13 980 # ASSIGN : s_7_14 396 # ASSIGN : s_8_0 574 # ASSIGN : s_8_1 138 # ASSIGN : s_8_2 593 # ASSIGN : s_8_3 432 # ASSIGN : s_8_4 594 # ASSIGN : s_8_5 689 # ASSIGN : s_8_6 236 # ASSIGN : s_8_7 363 # ASSIGN : s_8_8 826 # ASSIGN : s_8_9 768 # ASSIGN : s_8_10 155 # ASSIGN : s_8_11 901 # ASSIGN : s_8_12 325 # ASSIGN : s_8_13 472 # ASSIGN : s_8_14 617 # ASSIGN : s_9_0 569 # ASSIGN : s_9_1 155 # ASSIGN : s_9_2 919 # ASSIGN : s_9_3 960 # ASSIGN : s_9_4 2 # ASSIGN : s_9_5 103 # ASSIGN : s_9_6 654 # ASSIGN : s_9_7 200 # ASSIGN : s_9_8 737 # ASSIGN : s_9_9 572 # ASSIGN : s_9_10 482 # ASSIGN : s_9_11 228 # ASSIGN : s_9_12 829 # ASSIGN : s_9_13 397 # ASSIGN : s_9_14 307 # ASSIGN : s_10_0 841 # ASSIGN : s_10_1 2 # ASSIGN : s_10_2 389 # ASSIGN : s_10_3 896 # ASSIGN : s_10_4 812 # ASSIGN : s_10_5 265 # ASSIGN : s_10_6 557 # ASSIGN : s_10_7 970 # ASSIGN : s_10_8 300 # ASSIGN : s_10_9 691 # ASSIGN : s_10_10 182 # ASSIGN : s_10_11 462 # ASSIGN : s_10_12 952 # ASSIGN : s_10_13 101 # ASSIGN : s_10_14 138 # ASSIGN : s_11_0 568 # ASSIGN : s_11_1 531 # ASSIGN : s_11_2 594 # ASSIGN : s_11_3 828 # ASSIGN : s_11_4 356 # ASSIGN : s_11_5 397 # ASSIGN : s_11_6 977 # ASSIGN : s_11_7 464 # ASSIGN : s_11_8 75 # ASSIGN : s_11_9 303 # ASSIGN : s_11_10 793 # ASSIGN : s_11_11 726 # ASSIGN : s_11_12 631 # ASSIGN : s_11_13 798 # ASSIGN : s_11_14 104 # ASSIGN : s_12_0 14 # ASSIGN : s_12_1 637 # ASSIGN : s_12_2 967 # ASSIGN : s_12_3 484 # ASSIGN : s_12_4 84 # ASSIGN : s_12_5 181 # ASSIGN : s_12_6 904 # ASSIGN : s_12_7 911 # ASSIGN : s_12_8 391 # ASSIGN : s_12_9 418 # ASSIGN : s_12_10 258 # ASSIGN : s_12_11 799 # ASSIGN : s_12_12 723 # ASSIGN : s_12_13 943 # ASSIGN : s_12_14 37 # ASSIGN : s_13_0 376 # ASSIGN : s_13_1 737 # ASSIGN : s_13_2 194 # ASSIGN : s_13_3 286 # ASSIGN : s_13_4 28 # ASSIGN : s_13_5 831 # ASSIGN : s_13_6 129 # ASSIGN : s_13_7 544 # ASSIGN : s_13_8 695 # ASSIGN : s_13_9 152 # ASSIGN : s_13_10 921 # ASSIGN : s_13_11 114 # ASSIGN : s_13_12 90 # ASSIGN : s_13_13 607 # ASSIGN : s_13_14 454 # ASSIGN : s_14_0 666 # ASSIGN : s_14_1 880 # ASSIGN : s_14_2 672 # ASSIGN : s_14_3 770 # ASSIGN : s_14_4 278 # ASSIGN : s_14_5 547 # ASSIGN : s_14_6 436 # ASSIGN : s_14_7 696 # ASSIGN : s_14_8 182 # ASSIGN : s_14_9 961 # ASSIGN : s_14_10 802 # ASSIGN : s_14_11 32 # ASSIGN : s_14_12 111 # ASSIGN : s_14_13 374 # ASSIGN : s_14_14 687 SHOW_RESULT 994 END : 994 (0 seconds) [Mon Jun 19 13:34:05 2006] SHOW_RESULT 994 CPU : 0.680000000000007 = 0.680000000000007 + 0 + 0 + 0 # BOUND : makespan 934 994 MODIFY_CNF 964 BEGIN : [Mon Jun 19 13:34:05 2006] MODIFY_CNF 964 END : 217539822 bytes (0 seconds) [Mon Jun 19 13:34:05 2006] MODIFY_CNF 964 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 964 BEGIN : [Mon Jun 19 13:34:05 2006] CMD : minisat /tmp/csp2sat30961.cnf /tmp/csp2sat30961.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 6199048 18282566 | 2066349 0 0 nan | 0.000 % | | 101 | 6199048 18282566 | 2272983 101 1103 10.9 | 35.040 % | ============================================================================== restarts : 2 conflicts : 207 (10 /sec) decisions : 2038 (103 /sec) propagations : 1070788 (53917 /sec) conflict literals : 4268 (3.90 % deleted) Memory used : 368.34 MB CPU time : 19.86 s SATISFIABLE VERIFY_CNF 964 END : (21 seconds) [Mon Jun 19 13:34:26 2006] VERIFY_CNF 964 CPU : 21.16 = 0 + 0.01 + 20.02 + 1.13 # RESULT : makespan 964 SATISFIABLE SHOW_RESULT 964 BEGIN : [Mon Jun 19 13:34:26 2006] # ASSIGN : makespan 964 # ASSIGN : s_0_0 874 # ASSIGN : s_0_1 1 # ASSIGN : s_0_2 31 # ASSIGN : s_0_3 56 # ASSIGN : s_0_4 598 # ASSIGN : s_0_5 283 # ASSIGN : s_0_6 65 # ASSIGN : s_0_7 514 # ASSIGN : s_0_8 503 # ASSIGN : s_0_9 783 # ASSIGN : s_0_10 196 # ASSIGN : s_0_11 120 # ASSIGN : s_0_12 636 # ASSIGN : s_0_13 341 # ASSIGN : s_0_14 378 # ASSIGN : s_1_0 77 # ASSIGN : s_1_1 14 # ASSIGN : s_1_2 334 # ASSIGN : s_1_3 801 # ASSIGN : s_1_4 222 # ASSIGN : s_1_5 90 # ASSIGN : s_1_6 164 # ASSIGN : s_1_7 671 # ASSIGN : s_1_8 515 # ASSIGN : s_1_9 748 # ASSIGN : s_1_10 899 # ASSIGN : s_1_11 177 # ASSIGN : s_1_12 422 # ASSIGN : s_1_13 586 # ASSIGN : s_1_14 443 # ASSIGN : s_2_0 607 # ASSIGN : s_2_1 735 # ASSIGN : s_2_2 210 # ASSIGN : s_2_3 862 # ASSIGN : s_2_4 667 # ASSIGN : s_2_5 121 # ASSIGN : s_2_6 818 # ASSIGN : s_2_7 893 # ASSIGN : s_2_8 551 # ASSIGN : s_2_9 497 # ASSIGN : s_2_10 295 # ASSIGN : s_2_11 8 # ASSIGN : s_2_12 237 # ASSIGN : s_2_13 377 # ASSIGN : s_2_14 95 # ASSIGN : s_3_0 711 # ASSIGN : s_3_1 430 # ASSIGN : s_3_2 882 # ASSIGN : s_3_3 320 # ASSIGN : s_3_4 5 # ASSIGN : s_3_5 766 # ASSIGN : s_3_6 932 # ASSIGN : s_3_7 813 # ASSIGN : s_3_8 467 # ASSIGN : s_3_9 259 # ASSIGN : s_3_10 92 # ASSIGN : s_3_11 551 # ASSIGN : s_3_12 167 # ASSIGN : s_3_13 241 # ASSIGN : s_3_14 115 # ASSIGN : s_4_0 671 # ASSIGN : s_4_1 841 # ASSIGN : s_4_2 864 # ASSIGN : s_4_3 177 # ASSIGN : s_4_4 613 # ASSIGN : s_4_5 23 # ASSIGN : s_4_6 11 # ASSIGN : s_4_7 352 # ASSIGN : s_4_8 567 # ASSIGN : s_4_9 61 # ASSIGN : s_4_10 135 # ASSIGN : s_4_11 418 # ASSIGN : s_4_12 452 # ASSIGN : s_4_13 729 # ASSIGN : s_4_14 870 # ASSIGN : s_5_0 5 # ASSIGN : s_5_1 196 # ASSIGN : s_5_2 827 # ASSIGN : s_5_3 705 # ASSIGN : s_5_4 268 # ASSIGN : s_5_5 19 # ASSIGN : s_5_6 859 # ASSIGN : s_5_7 374 # ASSIGN : s_5_8 625 # ASSIGN : s_5_9 28 # ASSIGN : s_5_10 140 # ASSIGN : s_5_11 106 # ASSIGN : s_5_12 124 # ASSIGN : s_5_13 473 # ASSIGN : s_5_14 516 # ASSIGN : s_6_0 24 # ASSIGN : s_6_1 354 # ASSIGN : s_6_2 602 # ASSIGN : s_6_3 509 # ASSIGN : s_6_4 774 # ASSIGN : s_6_5 831 # ASSIGN : s_6_6 25 # ASSIGN : s_6_7 309 # ASSIGN : s_6_8 891 # ASSIGN : s_6_9 102 # ASSIGN : s_6_10 216 # ASSIGN : s_6_11 473 # ASSIGN : s_6_12 429 # ASSIGN : s_6_13 40 # ASSIGN : s_6_14 673 # ASSIGN : s_7_0 94 # ASSIGN : s_7_1 117 # ASSIGN : s_7_2 137 # ASSIGN : s_7_3 256 # ASSIGN : s_7_4 543 # ASSIGN : s_7_5 874 # ASSIGN : s_7_6 234 # ASSIGN : s_7_7 464 # ASSIGN : s_7_8 413 # ASSIGN : s_7_9 580 # ASSIGN : s_7_10 953 # ASSIGN : s_7_11 401 # ASSIGN : s_7_12 403 # ASSIGN : s_7_13 774 # ASSIGN : s_7_14 812 # ASSIGN : s_8_0 42 # ASSIGN : s_8_1 61 # ASSIGN : s_8_2 78 # ASSIGN : s_8_3 79 # ASSIGN : s_8_4 452 # ASSIGN : s_8_5 364 # ASSIGN : s_8_6 720 # ASSIGN : s_8_7 895 # ASSIGN : s_8_8 180 # ASSIGN : s_8_9 119 # ASSIGN : s_8_10 809 # ASSIGN : s_8_11 255 # ASSIGN : s_8_12 348 # ASSIGN : s_8_13 489 # ASSIGN : s_8_14 603 # ASSIGN : s_9_0 91 # ASSIGN : s_9_1 788 # ASSIGN : s_9_2 483 # ASSIGN : s_9_3 143 # ASSIGN : s_9_4 361 # ASSIGN : s_9_5 912 # ASSIGN : s_9_6 626 # ASSIGN : s_9_7 98 # ASSIGN : s_9_8 2 # ASSIGN : s_9_9 177 # ASSIGN : s_9_10 391 # ASSIGN : s_9_11 709 # ASSIGN : s_9_12 536 # ASSIGN : s_9_13 833 # ASSIGN : s_9_14 272 # ASSIGN : s_10_0 357 # ASSIGN : s_10_1 511 # ASSIGN : s_10_2 249 # ASSIGN : s_10_3 0 # ASSIGN : s_10_4 825 # ASSIGN : s_10_5 322 # ASSIGN : s_10_6 412 # ASSIGN : s_10_7 67 # ASSIGN : s_10_8 91 # ASSIGN : s_10_9 854 # ASSIGN : s_10_10 712 # ASSIGN : s_10_11 614 # ASSIGN : s_10_12 946 # ASSIGN : s_10_13 788 # ASSIGN : s_10_14 181 # ASSIGN : s_11_0 757 # ASSIGN : s_11_1 86 # ASSIGN : s_11_2 426 # ASSIGN : s_11_3 560 # ASSIGN : s_11_4 475 # ASSIGN : s_11_5 628 # ASSIGN : s_11_6 516 # ASSIGN : s_11_7 126 # ASSIGN : s_11_8 274 # ASSIGN : s_11_9 695 # ASSIGN : s_11_10 386 # ASSIGN : s_11_11 897 # ASSIGN : s_11_12 805 # ASSIGN : s_11_13 758 # ASSIGN : s_11_14 769 # ASSIGN : s_12_0 334 # ASSIGN : s_12_1 911 # ASSIGN : s_12_2 524 # ASSIGN : s_12_3 417 # ASSIGN : s_12_4 47 # ASSIGN : s_12_5 551 # ASSIGN : s_12_6 509 # ASSIGN : s_12_7 193 # ASSIGN : s_12_8 809 # ASSIGN : s_12_9 628 # ASSIGN : s_12_10 836 # ASSIGN : s_12_11 794 # ASSIGN : s_12_12 718 # ASSIGN : s_12_13 694 # ASSIGN : s_12_14 225 # ASSIGN : s_13_0 796 # ASSIGN : s_13_1 610 # ASSIGN : s_13_2 704 # ASSIGN : s_13_3 874 # ASSIGN : s_13_4 387 # ASSIGN : s_13_5 443 # ASSIGN : s_13_6 533 # ASSIGN : s_13_7 240 # ASSIGN : s_13_8 303 # ASSIGN : s_13_9 345 # ASSIGN : s_13_10 557 # ASSIGN : s_13_11 225 # ASSIGN : s_13_12 103 # ASSIGN : s_13_13 137 # ASSIGN : s_13_14 8 # ASSIGN : s_14_0 457 # ASSIGN : s_14_1 273 # ASSIGN : s_14_2 463 # ASSIGN : s_14_3 673 # ASSIGN : s_14_4 144 # ASSIGN : s_14_5 251 # ASSIGN : s_14_6 556 # ASSIGN : s_14_7 600 # ASSIGN : s_14_8 707 # ASSIGN : s_14_9 931 # ASSIGN : s_14_10 478 # ASSIGN : s_14_11 818 # ASSIGN : s_14_12 32 # ASSIGN : s_14_13 908 # ASSIGN : s_14_14 803 SHOW_RESULT 964 END : 964 (1 seconds) [Mon Jun 19 13:34:27 2006] SHOW_RESULT 964 CPU : 0.690000000000007 = 0.680000000000007 + 0.01 + 0 + 0 # BOUND : makespan 934 964 MODIFY_CNF 949 BEGIN : [Mon Jun 19 13:34:27 2006] MODIFY_CNF 949 END : 217539822 bytes (0 seconds) [Mon Jun 19 13:34:27 2006] MODIFY_CNF 949 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 949 BEGIN : [Mon Jun 19 13:34:27 2006] CMD : minisat /tmp/csp2sat30961.cnf /tmp/csp2sat30961.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 6104548 17999066 | 2034849 0 0 nan | 0.000 % | | 101 | 6104548 17999066 | 2238333 101 3306 32.7 | 36.078 % | | 252 | 6104548 17999066 | 2462167 252 6655 26.4 | 36.078 % | ============================================================================== restarts : 3 conflicts : 398 (18 /sec) decisions : 2793 (128 /sec) propagations : 1677403 (76839 /sec) conflict literals : 9860 (3.83 % deleted) Memory used : 368.34 MB CPU time : 21.83 s SATISFIABLE VERIFY_CNF 949 END : (23 seconds) [Mon Jun 19 13:34:50 2006] VERIFY_CNF 949 CPU : 23.18 = 0 + 0 + 21.99 + 1.19 # RESULT : makespan 949 SATISFIABLE SHOW_RESULT 949 BEGIN : [Mon Jun 19 13:34:50 2006] # ASSIGN : makespan 949 # ASSIGN : s_0_0 54 # ASSIGN : s_0_1 11 # ASSIGN : s_0_2 165 # ASSIGN : s_0_3 24 # ASSIGN : s_0_4 243 # ASSIGN : s_0_5 494 # ASSIGN : s_0_6 258 # ASSIGN : s_0_7 740 # ASSIGN : s_0_8 426 # ASSIGN : s_0_9 861 # ASSIGN : s_0_10 646 # ASSIGN : s_0_11 437 # ASSIGN : s_0_12 564 # ASSIGN : s_0_13 313 # ASSIGN : s_0_14 666 # ASSIGN : s_1_0 2 # ASSIGN : s_1_1 550 # ASSIGN : s_1_2 462 # ASSIGN : s_1_3 824 # ASSIGN : s_1_4 598 # ASSIGN : s_1_5 687 # ASSIGN : s_1_6 15 # ASSIGN : s_1_7 71 # ASSIGN : s_1_8 28 # ASSIGN : s_1_9 652 # ASSIGN : s_1_10 352 # ASSIGN : s_1_11 889 # ASSIGN : s_1_12 450 # ASSIGN : s_1_13 171 # ASSIGN : s_1_14 731 # ASSIGN : s_2_0 612 # ASSIGN : s_2_1 254 # ASSIGN : s_2_2 138 # ASSIGN : s_2_3 125 # ASSIGN : s_2_4 57 # ASSIGN : s_2_5 860 # ASSIGN : s_2_6 175 # ASSIGN : s_2_7 589 # ASSIGN : s_2_8 410 # ASSIGN : s_2_9 3 # ASSIGN : s_2_10 672 # ASSIGN : s_2_11 773 # ASSIGN : s_2_12 307 # ASSIGN : s_2_13 450 # ASSIGN : s_2_14 369 # ASSIGN : s_3_0 163 # ASSIGN : s_3_1 35 # ASSIGN : s_3_2 209 # ASSIGN : s_3_3 727 # ASSIGN : s_3_4 685 # ASSIGN : s_3_5 259 # ASSIGN : s_3_6 435 # ASSIGN : s_3_7 824 # ASSIGN : s_3_8 641 # ASSIGN : s_3_9 580 # ASSIGN : s_3_10 140 # ASSIGN : s_3_11 72 # ASSIGN : s_3_12 476 # ASSIGN : s_3_13 546 # ASSIGN : s_3_14 897 # ASSIGN : s_4_0 291 # ASSIGN : s_4_1 193 # ASSIGN : s_4_2 132 # ASSIGN : s_4_3 504 # ASSIGN : s_4_4 747 # ASSIGN : s_4_5 155 # ASSIGN : s_4_6 216 # ASSIGN : s_4_7 228 # ASSIGN : s_4_8 449 # ASSIGN : s_4_9 250 # ASSIGN : s_4_10 667 # ASSIGN : s_4_11 331 # ASSIGN : s_4_12 365 # ASSIGN : s_4_13 701 # ASSIGN : s_4_14 803 # ASSIGN : s_5_0 277 # ASSIGN : s_5_1 679 # ASSIGN : s_5_2 18 # ASSIGN : s_5_3 583 # ASSIGN : s_5_4 490 # ASSIGN : s_5_5 0 # ASSIGN : s_5_6 859 # ASSIGN : s_5_7 336 # ASSIGN : s_5_8 64 # ASSIGN : s_5_9 826 # ASSIGN : s_5_10 754 # ASSIGN : s_5_11 50 # ASSIGN : s_5_12 810 # ASSIGN : s_5_13 933 # ASSIGN : s_5_14 144 # ASSIGN : s_6_0 750 # ASSIGN : s_6_1 751 # ASSIGN : s_6_2 61 # ASSIGN : s_6_3 137 # ASSIGN : s_6_4 875 # ASSIGN : s_6_5 306 # ASSIGN : s_6_6 411 # ASSIGN : s_6_7 426 # ASSIGN : s_6_8 233 # ASSIGN : s_6_9 932 # ASSIGN : s_6_10 469 # ASSIGN : s_6_11 14 # ASSIGN : s_6_12 836 # ASSIGN : s_6_13 349 # ASSIGN : s_6_14 570 # ASSIGN : s_7_0 809 # ASSIGN : s_7_1 597 # ASSIGN : s_7_2 384 # ASSIGN : s_7_3 885 # ASSIGN : s_7_4 262 # ASSIGN : s_7_5 649 # ASSIGN : s_7_6 467 # ASSIGN : s_7_7 690 # ASSIGN : s_7_8 832 # ASSIGN : s_7_9 89 # ASSIGN : s_7_10 635 # ASSIGN : s_7_11 883 # ASSIGN : s_7_12 457 # ASSIGN : s_7_13 299 # ASSIGN : s_7_14 512 # ASSIGN : s_8_0 144 # ASSIGN : s_8_1 237 # ASSIGN : s_8_2 190 # ASSIGN : s_8_3 323 # ASSIGN : s_8_4 926 # ASSIGN : s_8_5 363 # ASSIGN : s_8_6 572 # ASSIGN : s_8_7 254 # ASSIGN : s_8_8 754 # ASSIGN : s_8_9 514 # ASSIGN : s_8_10 207 # ASSIGN : s_8_11 661 # ASSIGN : s_8_12 191 # ASSIGN : s_8_13 829 # ASSIGN : s_8_14 442 # ASSIGN : s_9_0 727 # ASSIGN : s_9_1 362 # ASSIGN : s_9_2 321 # ASSIGN : s_9_3 693 # ASSIGN : s_9_4 29 # ASSIGN : s_9_5 807 # ASSIGN : s_9_6 489 # ASSIGN : s_9_7 662 # ASSIGN : s_9_8 144 # ASSIGN : s_9_9 407 # ASSIGN : s_9_10 234 # ASSIGN : s_9_11 582 # ASSIGN : s_9_12 859 # ASSIGN : s_9_13 730 # ASSIGN : s_9_14 55 # ASSIGN : s_10_0 509 # ASSIGN : s_10_1 826 # ASSIGN : s_10_2 645 # ASSIGN : s_10_3 448 # ASSIGN : s_10_4 0 # ASSIGN : s_10_5 610 # ASSIGN : s_10_6 718 # ASSIGN : s_10_7 925 # ASSIGN : s_10_8 309 # ASSIGN : s_10_9 137 # ASSIGN : s_10_10 61 # ASSIGN : s_10_11 214 # ASSIGN : s_10_12 43 # ASSIGN : s_10_13 564 # ASSIGN : s_10_14 398 # ASSIGN : s_11_0 902 # ASSIGN : s_11_1 331 # ASSIGN : s_11_2 607 # ASSIGN : s_11_3 371 # ASSIGN : s_11_4 644 # ASSIGN : s_11_5 740 # ASSIGN : s_11_6 932 # ASSIGN : s_11_7 148 # ASSIGN : s_11_8 903 # ASSIGN : s_11_9 687 # ASSIGN : s_11_10 866 # ASSIGN : s_11_11 515 # ASSIGN : s_11_12 215 # ASSIGN : s_11_13 439 # ASSIGN : s_11_14 21 # ASSIGN : s_12_0 782 # ASSIGN : s_12_1 617 # ASSIGN : s_12_2 830 # ASSIGN : s_12_3 33 # ASSIGN : s_12_4 134 # ASSIGN : s_12_5 533 # ASSIGN : s_12_6 670 # ASSIGN : s_12_7 893 # ASSIGN : s_12_8 677 # ASSIGN : s_12_9 299 # ASSIGN : s_12_10 406 # ASSIGN : s_12_11 934 # ASSIGN : s_12_12 704 # ASSIGN : s_12_13 805 # ASSIGN : s_12_14 231 # ASSIGN : s_13_0 407 # ASSIGN : s_13_1 94 # ASSIGN : s_13_2 857 # ASSIGN : s_13_3 188 # ASSIGN : s_13_4 801 # ASSIGN : s_13_5 4 # ASSIGN : s_13_6 689 # ASSIGN : s_13_7 485 # ASSIGN : s_13_8 712 # ASSIGN : s_13_9 365 # ASSIGN : s_13_10 548 # ASSIGN : s_13_11 758 # ASSIGN : s_13_12 780 # ASSIGN : s_13_13 601 # ASSIGN : s_13_14 278 # ASSIGN : s_14_0 865 # ASSIGN : s_14_1 414 # ASSIGN : s_14_2 767 # ASSIGN : s_14_3 279 # ASSIGN : s_14_4 311 # ASSIGN : s_14_5 718 # ASSIGN : s_14_6 815 # ASSIGN : s_14_7 591 # ASSIGN : s_14_8 495 # ASSIGN : s_14_9 782 # ASSIGN : s_14_10 871 # ASSIGN : s_14_11 135 # ASSIGN : s_14_12 64 # ASSIGN : s_14_13 256 # ASSIGN : s_14_14 389 SHOW_RESULT 949 END : 949 (1 seconds) [Mon Jun 19 13:34:51 2006] SHOW_RESULT 949 CPU : 0.709999999999998 = 0.689999999999998 + 0.02 + 0 + 0 # BOUND : makespan 934 949 MODIFY_CNF 941 BEGIN : [Mon Jun 19 13:34:51 2006] MODIFY_CNF 941 END : 217539821 bytes (0 seconds) [Mon Jun 19 13:34:51 2006] MODIFY_CNF 941 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 941 BEGIN : [Mon Jun 19 13:34:51 2006] CMD : minisat /tmp/csp2sat30961.cnf /tmp/csp2sat30961.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 6054148 17847866 | 2018049 0 0 nan | 0.000 % | | 100 | 6054148 17847866 | 2219853 100 4168 41.7 | 36.632 % | | 250 | 6054148 17847866 | 2441839 250 5891 23.6 | 36.632 % | | 476 | 6054148 17847866 | 2686023 476 13158 27.6 | 36.632 % | | 814 | 6054148 17847866 | 2954625 814 28124 34.6 | 36.632 % | | 1320 | 6054148 17847866 | 3250088 1320 35532 26.9 | 36.632 % | ============================================================================== restarts : 6 conflicts : 1411 (54 /sec) decisions : 4810 (183 /sec) propagations : 3331585 (126918 /sec) conflict literals : 36549 (7.77 % deleted) Memory used : 368.34 MB CPU time : 26.25 s SATISFIABLE VERIFY_CNF 941 END : (28 seconds) [Mon Jun 19 13:35:19 2006] VERIFY_CNF 941 CPU : 27.55 = 0 + 0 + 26.41 + 1.14 # RESULT : makespan 941 SATISFIABLE SHOW_RESULT 941 BEGIN : [Mon Jun 19 13:35:19 2006] # ASSIGN : makespan 941 # ASSIGN : s_0_0 684 # ASSIGN : s_0_1 913 # ASSIGN : s_0_2 329 # ASSIGN : s_0_3 853 # ASSIGN : s_0_4 926 # ASSIGN : s_0_5 603 # ASSIGN : s_0_6 774 # ASSIGN : s_0_7 433 # ASSIGN : s_0_8 44 # ASSIGN : s_0_9 83 # ASSIGN : s_0_10 867 # ASSIGN : s_0_11 356 # ASSIGN : s_0_12 520 # ASSIGN : s_0_13 229 # ASSIGN : s_0_14 154 # ASSIGN : s_1_0 24 # ASSIGN : s_1_1 303 # ASSIGN : s_1_2 186 # ASSIGN : s_1_3 528 # ASSIGN : s_1_4 114 # ASSIGN : s_1_5 674 # ASSIGN : s_1_6 512 # ASSIGN : s_1_7 37 # ASSIGN : s_1_8 763 # ASSIGN : s_1_9 475 # ASSIGN : s_1_10 887 # ASSIGN : s_1_11 718 # ASSIGN : s_1_12 0 # ASSIGN : s_1_13 589 # ASSIGN : s_1_14 402 # ASSIGN : s_2_0 861 # ASSIGN : s_2_1 250 # ASSIGN : s_2_2 635 # ASSIGN : s_2_3 607 # ASSIGN : s_2_4 311 # ASSIGN : s_2_5 433 # ASSIGN : s_2_6 525 # ASSIGN : s_2_7 814 # ASSIGN : s_2_8 619 # ASSIGN : s_2_9 379 # ASSIGN : s_2_10 168 # ASSIGN : s_2_11 81 # ASSIGN : s_2_12 23 # ASSIGN : s_2_13 703 # ASSIGN : s_2_14 921 # ASSIGN : s_3_0 230 # ASSIGN : s_3_1 638 # ASSIGN : s_3_2 585 # ASSIGN : s_3_3 2 # ASSIGN : s_3_4 693 # ASSIGN : s_3_5 176 # ASSIGN : s_3_6 829 # ASSIGN : s_3_7 872 # ASSIGN : s_3_8 417 # ASSIGN : s_3_9 510 # ASSIGN : s_3_10 487 # ASSIGN : s_3_11 766 # ASSIGN : s_3_12 106 # ASSIGN : s_3_13 675 # ASSIGN : s_3_14 350 # ASSIGN : s_4_0 515 # ASSIGN : s_4_1 207 # ASSIGN : s_4_2 765 # ASSIGN : s_4_3 862 # ASSIGN : s_4_4 257 # ASSIGN : s_4_5 312 # ASSIGN : s_4_6 753 # ASSIGN : s_4_7 728 # ASSIGN : s_4_8 799 # ASSIGN : s_4_9 434 # ASSIGN : s_4_10 719 # ASSIGN : s_4_11 555 # ASSIGN : s_4_12 350 # ASSIGN : s_4_13 64 # ASSIGN : s_4_14 595 # ASSIGN : s_5_0 670 # ASSIGN : s_5_1 566 # ASSIGN : s_5_2 274 # ASSIGN : s_5_3 689 # ASSIGN : s_5_4 19 # ASSIGN : s_5_5 864 # ASSIGN : s_5_6 868 # ASSIGN : s_5_7 184 # ASSIGN : s_5_8 306 # ASSIGN : s_5_9 785 # ASSIGN : s_5_10 112 # ASSIGN : s_5_11 850 # ASSIGN : s_5_12 834 # ASSIGN : s_5_13 428 # ASSIGN : s_5_14 474 # ASSIGN : s_6_0 803 # ASSIGN : s_6_1 804 # ASSIGN : s_6_2 514 # ASSIGN : s_6_3 370 # ASSIGN : s_6_4 458 # ASSIGN : s_6_5 15 # ASSIGN : s_6_6 161 # ASSIGN : s_6_7 321 # ASSIGN : s_6_8 233 # ASSIGN : s_6_9 216 # ASSIGN : s_6_10 724 # ASSIGN : s_6_11 682 # ASSIGN : s_6_12 641 # ASSIGN : s_6_13 879 # ASSIGN : s_6_14 58 # ASSIGN : s_7_0 487 # ASSIGN : s_7_1 230 # ASSIGN : s_7_2 692 # ASSIGN : s_7_3 421 # ASSIGN : s_7_4 384 # ASSIGN : s_7_5 868 # ASSIGN : s_7_6 566 # ASSIGN : s_7_7 588 # ASSIGN : s_7_8 641 # ASSIGN : s_7_9 818 # ASSIGN : s_7_10 301 # ASSIGN : s_7_11 866 # ASSIGN : s_7_12 510 # ASSIGN : s_7_13 799 # ASSIGN : s_7_14 0 # ASSIGN : s_8_0 922 # ASSIGN : s_8_1 37 # ASSIGN : s_8_2 771 # ASSIGN : s_8_3 133 # ASSIGN : s_8_4 509 # ASSIGN : s_8_5 772 # ASSIGN : s_8_6 176 # ASSIGN : s_8_7 364 # ASSIGN : s_8_8 55 # ASSIGN : s_8_9 713 # ASSIGN : s_8_10 686 # ASSIGN : s_8_11 589 # ASSIGN : s_8_12 7 # ASSIGN : s_8_13 265 # ASSIGN : s_8_14 851 # ASSIGN : s_9_0 145 # ASSIGN : s_9_1 54 # ASSIGN : s_9_2 354 # ASSIGN : s_9_3 99 # ASSIGN : s_9_4 825 # ASSIGN : s_9_5 223 # ASSIGN : s_9_6 653 # ASSIGN : s_9_7 9 # ASSIGN : s_9_8 482 # ASSIGN : s_9_9 571 # ASSIGN : s_9_10 395 # ASSIGN : s_9_11 275 # ASSIGN : s_9_12 851 # ASSIGN : s_9_13 148 # ASSIGN : s_9_14 736 # ASSIGN : s_10_0 276 # ASSIGN : s_10_1 676 # ASSIGN : s_10_2 775 # ASSIGN : s_10_3 620 # ASSIGN : s_10_4 877 # ASSIGN : s_10_5 906 # ASSIGN : s_10_6 331 # ASSIGN : s_10_7 848 # ASSIGN : s_10_8 130 # ASSIGN : s_10_9 6 # ASSIGN : s_10_10 523 # ASSIGN : s_10_11 428 # ASSIGN : s_10_12 602 # ASSIGN : s_10_13 93 # ASSIGN : s_10_14 219 # ASSIGN : s_11_0 229 # ASSIGN : s_11_1 530 # ASSIGN : s_11_2 416 # ASSIGN : s_11_3 785 # ASSIGN : s_11_4 597 # ASSIGN : s_11_5 705 # ASSIGN : s_11_6 495 # ASSIGN : s_11_7 638 # ASSIGN : s_11_8 453 # ASSIGN : s_11_9 326 # ASSIGN : s_11_10 390 # ASSIGN : s_11_11 874 # ASSIGN : s_11_12 234 # ASSIGN : s_11_13 863 # ASSIGN : s_11_14 561 # ASSIGN : s_12_0 441 # ASSIGN : s_12_1 469 # ASSIGN : s_12_2 662 # ASSIGN : s_12_3 270 # ASSIGN : s_12_4 160 # ASSIGN : s_12_5 522 # ASSIGN : s_12_6 861 # ASSIGN : s_12_7 816 # ASSIGN : s_12_8 386 # ASSIGN : s_12_9 875 # ASSIGN : s_12_10 599 # ASSIGN : s_12_11 413 # ASSIGN : s_12_12 737 # ASSIGN : s_12_13 362 # ASSIGN : s_12_14 689 # ASSIGN : s_13_0 588 # ASSIGN : s_13_1 350 # ASSIGN : s_13_2 849 # ASSIGN : s_13_3 173 # ASSIGN : s_13_4 532 # ASSIGN : s_13_5 83 # ASSIGN : s_13_6 7 # ASSIGN : s_13_7 750 # ASSIGN : s_13_8 708 # ASSIGN : s_13_9 666 # ASSIGN : s_13_10 30 # ASSIGN : s_13_11 834 # ASSIGN : s_13_12 813 # ASSIGN : s_13_13 444 # ASSIGN : s_13_14 263 # ASSIGN : s_14_0 464 # ASSIGN : s_14_1 115 # ASSIGN : s_14_2 470 # ASSIGN : s_14_3 485 # ASSIGN : s_14_4 735 # ASSIGN : s_14_5 642 # ASSIGN : s_14_6 598 # ASSIGN : s_14_7 517 # ASSIGN : s_14_8 845 # ASSIGN : s_14_9 279 # ASSIGN : s_14_10 312 # ASSIGN : s_14_11 196 # ASSIGN : s_14_12 664 # ASSIGN : s_14_13 813 # ASSIGN : s_14_14 836 SHOW_RESULT 941 END : 941 (0 seconds) [Mon Jun 19 13:35:19 2006] SHOW_RESULT 941 CPU : 0.700000000000007 = 0.680000000000007 + 0.02 + 0 + 0 # BOUND : makespan 934 941 MODIFY_CNF 937 BEGIN : [Mon Jun 19 13:35:19 2006] MODIFY_CNF 937 END : 217539821 bytes (0 seconds) [Mon Jun 19 13:35:19 2006] MODIFY_CNF 937 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 937 BEGIN : [Mon Jun 19 13:35:19 2006] CMD : minisat /tmp/csp2sat30961.cnf /tmp/csp2sat30961.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 6028948 17772266 | 2009649 0 0 nan | 0.000 % | | 100 | 6028948 17772266 | 2210613 100 3858 38.6 | 36.909 % | | 250 | 6028948 17772266 | 2431675 250 6891 27.6 | 36.909 % | | 475 | 6028948 17772266 | 2674842 475 14895 31.4 | 36.909 % | ============================================================================== restarts : 4 conflicts : 621 (27 /sec) decisions : 3009 (129 /sec) propagations : 2496666 (107337 /sec) conflict literals : 20319 (5.68 % deleted) Memory used : 368.33 MB CPU time : 23.26 s SATISFIABLE VERIFY_CNF 937 END : (25 seconds) [Mon Jun 19 13:35:44 2006] VERIFY_CNF 937 CPU : 24.42 = 0 + 0 + 23.46 + 0.960000000000001 # RESULT : makespan 937 SATISFIABLE SHOW_RESULT 937 BEGIN : [Mon Jun 19 13:35:44 2006] # ASSIGN : makespan 937 # ASSIGN : s_0_0 577 # ASSIGN : s_0_1 924 # ASSIGN : s_0_2 473 # ASSIGN : s_0_3 443 # ASSIGN : s_0_4 4 # ASSIGN : s_0_5 677 # ASSIGN : s_0_6 25 # ASSIGN : s_0_7 286 # ASSIGN : s_0_8 80 # ASSIGN : s_0_9 800 # ASSIGN : s_0_10 91 # ASSIGN : s_0_11 111 # ASSIGN : s_0_12 168 # ASSIGN : s_0_13 250 # ASSIGN : s_0_14 377 # ASSIGN : s_1_0 6 # ASSIGN : s_1_1 704 # ASSIGN : s_1_2 296 # ASSIGN : s_1_3 19 # ASSIGN : s_1_4 95 # ASSIGN : s_1_5 521 # ASSIGN : s_1_6 141 # ASSIGN : s_1_7 552 # ASSIGN : s_1_8 154 # ASSIGN : s_1_9 200 # ASSIGN : s_1_10 235 # ASSIGN : s_1_11 384 # ASSIGN : s_1_12 429 # ASSIGN : s_1_13 436 # ASSIGN : s_1_14 751 # ASSIGN : s_2_0 667 # ASSIGN : s_2_1 489 # ASSIGN : s_2_2 542 # ASSIGN : s_2_3 7 # ASSIGN : s_2_4 19 # ASSIGN : s_2_5 87 # ASSIGN : s_2_6 176 # ASSIGN : s_2_7 217 # ASSIGN : s_2_8 219 # ASSIGN : s_2_9 235 # ASSIGN : s_2_10 289 # ASSIGN : s_2_11 569 # ASSIGN : s_2_12 371 # ASSIGN : s_2_13 727 # ASSIGN : s_2_14 823 # ASSIGN : s_3_0 53 # ASSIGN : s_3_1 165 # ASSIGN : s_3_2 246 # ASSIGN : s_3_3 724 # ASSIGN : s_3_4 381 # ASSIGN : s_3_5 436 # ASSIGN : s_3_6 619 # ASSIGN : s_3_7 483 # ASSIGN : s_3_8 568 # ASSIGN : s_3_9 651 # ASSIGN : s_3_10 909 # ASSIGN : s_3_11 836 # ASSIGN : s_3_12 301 # ASSIGN : s_3_13 228 # ASSIGN : s_3_14 1 # ASSIGN : s_4_0 443 # ASSIGN : s_4_1 544 # ASSIGN : s_4_2 574 # ASSIGN : s_4_3 858 # ASSIGN : s_4_4 639 # ASSIGN : s_4_5 483 # ASSIGN : s_4_6 607 # ASSIGN : s_4_7 195 # ASSIGN : s_4_8 253 # ASSIGN : s_4_9 341 # ASSIGN : s_4_10 797 # ASSIGN : s_4_11 802 # ASSIGN : s_4_12 693 # ASSIGN : s_4_13 299 # ASSIGN : s_4_14 60 # ASSIGN : s_5_0 246 # ASSIGN : s_5_1 632 # ASSIGN : s_5_2 391 # ASSIGN : s_5_3 516 # ASSIGN : s_5_4 423 # ASSIGN : s_5_5 860 # ASSIGN : s_5_6 864 # ASSIGN : s_5_7 105 # ASSIGN : s_5_8 768 # ASSIGN : s_5_9 72 # ASSIGN : s_5_10 712 # ASSIGN : s_5_11 276 # ASSIGN : s_5_12 260 # ASSIGN : s_5_13 616 # ASSIGN : s_5_14 290 # ASSIGN : s_6_0 836 # ASSIGN : s_6_1 761 # ASSIGN : s_6_2 156 # ASSIGN : s_6_3 351 # ASSIGN : s_6_4 227 # ASSIGN : s_6_5 716 # ASSIGN : s_6_6 309 # ASSIGN : s_6_7 62 # ASSIGN : s_6_8 439 # ASSIGN : s_6_9 324 # ASSIGN : s_6_10 633 # ASSIGN : s_6_11 899 # ASSIGN : s_6_12 278 # ASSIGN : s_6_13 837 # ASSIGN : s_6_14 512 # ASSIGN : s_7_0 734 # ASSIGN : s_7_1 857 # ASSIGN : s_7_2 580 # ASSIGN : s_7_3 452 # ASSIGN : s_7_4 757 # ASSIGN : s_7_5 398 # ASSIGN : s_7_6 119 # ASSIGN : s_7_7 236 # ASSIGN : s_7_8 517 # ASSIGN : s_7_9 152 # ASSIGN : s_7_10 813 # ASSIGN : s_7_11 935 # ASSIGN : s_7_12 667 # ASSIGN : s_7_13 328 # ASSIGN : s_7_14 877 # ASSIGN : s_8_0 272 # ASSIGN : s_8_1 9 # ASSIGN : s_8_2 867 # ASSIGN : s_8_3 402 # ASSIGN : s_8_4 575 # ASSIGN : s_8_5 598 # ASSIGN : s_8_6 775 # ASSIGN : s_8_7 868 # ASSIGN : s_8_8 693 # ASSIGN : s_8_9 517 # ASSIGN : s_8_10 208 # ASSIGN : s_8_11 291 # ASSIGN : s_8_12 677 # ASSIGN : s_8_13 111 # ASSIGN : s_8_14 442 # ASSIGN : s_9_0 301 # ASSIGN : s_9_1 439 # ASSIGN : s_9_2 653 # ASSIGN : s_9_3 80 # ASSIGN : s_9_4 794 # ASSIGN : s_9_5 304 # ASSIGN : s_9_6 356 # ASSIGN : s_9_7 820 # ASSIGN : s_9_8 848 # ASSIGN : s_9_9 712 # ASSIGN : s_9_10 114 # ASSIGN : s_9_11 484 # ASSIGN : s_9_12 563 # ASSIGN : s_9_13 5 # ASSIGN : s_9_14 201 # ASSIGN : s_10_0 99 # ASSIGN : s_10_1 283 # ASSIGN : s_10_2 694 # ASSIGN : s_10_3 227 # ASSIGN : s_10_4 198 # ASSIGN : s_10_5 563 # ASSIGN : s_10_6 466 # ASSIGN : s_10_7 796 # ASSIGN : s_10_8 604 # ASSIGN : s_10_9 382 # ASSIGN : s_10_10 824 # ASSIGN : s_10_11 4 # ASSIGN : s_10_12 777 # ASSIGN : s_10_13 900 # ASSIGN : s_10_14 154 # ASSIGN : s_11_0 842 # ASSIGN : s_11_1 567 # ASSIGN : s_11_2 895 # ASSIGN : s_11_3 283 # ASSIGN : s_11_4 598 # ASSIGN : s_11_5 759 # ASSIGN : s_11_6 742 # ASSIGN : s_11_7 370 # ASSIGN : s_11_8 190 # ASSIGN : s_11_9 19 # ASSIGN : s_11_10 932 # ASSIGN : s_11_11 656 # ASSIGN : s_11_12 76 # ASSIGN : s_11_13 826 # ASSIGN : s_11_14 843 # ASSIGN : s_12_0 772 # ASSIGN : s_12_1 384 # ASSIGN : s_12_2 498 # ASSIGN : s_12_3 612 # ASSIGN : s_12_4 284 # ASSIGN : s_12_5 10 # ASSIGN : s_12_6 765 # ASSIGN : s_12_7 437 # ASSIGN : s_12_8 127 # ASSIGN : s_12_9 871 # ASSIGN : s_12_10 549 # ASSIGN : s_12_11 469 # ASSIGN : s_12_12 795 # ASSIGN : s_12_13 525 # ASSIGN : s_12_14 704 # ASSIGN : s_13_0 859 # ASSIGN : s_13_1 26 # ASSIGN : s_13_2 767 # ASSIGN : s_13_3 120 # ASSIGN : s_13_4 519 # ASSIGN : s_13_5 210 # ASSIGN : s_13_6 2 # ASSIGN : s_13_7 704 # ASSIGN : s_13_8 300 # ASSIGN : s_13_9 575 # ASSIGN : s_13_10 466 # ASSIGN : s_13_11 430 # ASSIGN : s_13_12 445 # ASSIGN : s_13_13 342 # ASSIGN : s_13_14 617 # ASSIGN : s_14_0 853 # ASSIGN : s_14_1 202 # ASSIGN : s_14_2 444 # ASSIGN : s_14_3 821 # ASSIGN : s_14_4 859 # ASSIGN : s_14_5 180 # ASSIGN : s_14_6 563 # ASSIGN : s_14_7 629 # ASSIGN : s_14_8 343 # ASSIGN : s_14_9 459 # ASSIGN : s_14_10 13 # ASSIGN : s_14_11 723 # ASSIGN : s_14_12 492 # ASSIGN : s_14_13 700 # ASSIGN : s_14_14 608 SHOW_RESULT 937 END : 937 (1 seconds) [Mon Jun 19 13:35:45 2006] SHOW_RESULT 937 CPU : 0.729999999999989 = 0.699999999999989 + 0.03 + 0 + 0 # BOUND : makespan 934 937 MODIFY_CNF 935 BEGIN : [Mon Jun 19 13:35:45 2006] MODIFY_CNF 935 END : 217539821 bytes (0 seconds) [Mon Jun 19 13:35:45 2006] MODIFY_CNF 935 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 935 BEGIN : [Mon Jun 19 13:35:45 2006] CMD : minisat /tmp/csp2sat30961.cnf /tmp/csp2sat30961.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 6016348 17734466 | 2005449 0 0 nan | 0.000 % | | 100 | 6016348 17734466 | 2205993 100 3174 31.7 | 37.047 % | ============================================================================== restarts : 2 conflicts : 205 (10 /sec) decisions : 2689 (126 /sec) propagations : 1362230 (64015 /sec) conflict literals : 4607 (4.95 % deleted) Memory used : 368.33 MB CPU time : 21.28 s SATISFIABLE VERIFY_CNF 935 END : (22 seconds) [Mon Jun 19 13:36:07 2006] VERIFY_CNF 935 CPU : 22.6 = 0 + 0 + 21.45 + 1.15 # RESULT : makespan 935 SATISFIABLE SHOW_RESULT 935 BEGIN : [Mon Jun 19 13:36:07 2006] # ASSIGN : makespan 935 # ASSIGN : s_0_0 390 # ASSIGN : s_0_1 76 # ASSIGN : s_0_2 904 # ASSIGN : s_0_3 712 # ASSIGN : s_0_4 122 # ASSIGN : s_0_5 314 # ASSIGN : s_0_6 137 # ASSIGN : s_0_7 752 # ASSIGN : s_0_8 888 # ASSIGN : s_0_9 522 # ASSIGN : s_0_10 89 # ASSIGN : s_0_11 19 # ASSIGN : s_0_12 192 # ASSIGN : s_0_13 480 # ASSIGN : s_0_14 593 # ASSIGN : s_1_0 57 # ASSIGN : s_1_1 603 # ASSIGN : s_1_2 656 # ASSIGN : s_1_3 499 # ASSIGN : s_1_4 452 # ASSIGN : s_1_5 108 # ASSIGN : s_1_6 832 # ASSIGN : s_1_7 190 # ASSIGN : s_1_8 416 # ASSIGN : s_1_9 2 # ASSIGN : s_1_10 281 # ASSIGN : s_1_11 145 # ASSIGN : s_1_12 274 # ASSIGN : s_1_13 850 # ASSIGN : s_1_14 335 # ASSIGN : s_2_0 569 # ASSIGN : s_2_1 208 # ASSIGN : s_2_2 629 # ASSIGN : s_2_3 821 # ASSIGN : s_2_4 753 # ASSIGN : s_2_5 664 # ASSIGN : s_2_6 528 # ASSIGN : s_2_7 27 # ASSIGN : s_2_8 102 # ASSIGN : s_2_9 154 # ASSIGN : s_2_10 414 # ASSIGN : s_2_11 833 # ASSIGN : s_2_12 31 # ASSIGN : s_2_13 318 # ASSIGN : s_2_14 503 # ASSIGN : s_3_0 659 # ASSIGN : s_3_1 171 # ASSIGN : s_3_2 579 # ASSIGN : s_3_3 37 # ASSIGN : s_3_4 215 # ASSIGN : s_3_5 481 # ASSIGN : s_3_6 360 # ASSIGN : s_3_7 289 # ASSIGN : s_3_8 899 # ASSIGN : s_3_9 705 # ASSIGN : s_3_10 528 # ASSIGN : s_3_11 770 # ASSIGN : s_3_12 392 # ASSIGN : s_3_13 551 # ASSIGN : s_3_14 839 # ASSIGN : s_4_0 313 # ASSIGN : s_4_1 792 # ASSIGN : s_4_2 929 # ASSIGN : s_4_3 134 # ASSIGN : s_4_4 498 # ASSIGN : s_4_5 353 # ASSIGN : s_4_6 395 # ASSIGN : s_4_7 267 # ASSIGN : s_4_8 452 # ASSIGN : s_4_9 664 # ASSIGN : s_4_10 14 # ASSIGN : s_4_11 722 # ASSIGN : s_4_12 815 # ASSIGN : s_4_13 763 # ASSIGN : s_4_14 19 # ASSIGN : s_5_0 70 # ASSIGN : s_5_1 520 # ASSIGN : s_5_2 5 # ASSIGN : s_5_3 247 # ASSIGN : s_5_4 842 # ASSIGN : s_5_5 838 # ASSIGN : s_5_6 592 # ASSIGN : s_5_7 429 # ASSIGN : s_5_8 667 # ASSIGN : s_5_9 37 # ASSIGN : s_5_10 358 # ASSIGN : s_5_11 756 # ASSIGN : s_5_12 89 # ASSIGN : s_5_13 144 # ASSIGN : s_5_14 160 # ASSIGN : s_6_0 657 # ASSIGN : s_6_1 89 # ASSIGN : s_6_2 508 # ASSIGN : s_6_3 658 # ASSIGN : s_6_4 164 # ASSIGN : s_6_5 892 # ASSIGN : s_6_6 74 # ASSIGN : s_6_7 709 # ASSIGN : s_6_8 0 # ASSIGN : s_6_9 599 # ASSIGN : s_6_10 778 # ASSIGN : s_6_11 616 # ASSIGN : s_6_12 369 # ASSIGN : s_6_13 256 # ASSIGN : s_6_14 407 # ASSIGN : s_7_0 629 # ASSIGN : s_7_1 278 # ASSIGN : s_7_2 435 # ASSIGN : s_7_3 343 # ASSIGN : s_7_4 298 # ASSIGN : s_7_5 591 # ASSIGN : s_7_6 665 # ASSIGN : s_7_7 519 # ASSIGN : s_7_8 836 # ASSIGN : s_7_9 887 # ASSIGN : s_7_10 687 # ASSIGN : s_7_11 652 # ASSIGN : s_7_12 805 # ASSIGN : s_7_13 569 # ASSIGN : s_7_14 747 # ASSIGN : s_8_0 876 # ASSIGN : s_8_1 261 # ASSIGN : s_8_2 2 # ASSIGN : s_8_3 895 # ASSIGN : s_8_4 3 # ASSIGN : s_8_5 26 # ASSIGN : s_8_6 407 # ASSIGN : s_8_7 597 # ASSIGN : s_8_8 172 # ASSIGN : s_8_9 766 # ASSIGN : s_8_10 496 # ASSIGN : s_8_11 290 # ASSIGN : s_8_12 105 # ASSIGN : s_8_13 666 # ASSIGN : s_8_14 523 # ASSIGN : s_9_0 5 # ASSIGN : s_9_1 8 # ASSIGN : s_9_2 85 # ASSIGN : s_9_3 213 # ASSIGN : s_9_4 552 # ASSIGN : s_9_5 248 # ASSIGN : s_9_6 845 # ASSIGN : s_9_7 53 # ASSIGN : s_9_8 747 # ASSIGN : s_9_9 300 # ASSIGN : s_9_10 126 # ASSIGN : s_9_11 383 # ASSIGN : s_9_12 462 # ASSIGN : s_9_13 583 # ASSIGN : s_9_14 658 # ASSIGN : s_10_0 84 # ASSIGN : s_10_1 336 # ASSIGN : s_10_2 174 # ASSIGN : s_10_3 835 # ASSIGN : s_10_4 55 # ASSIGN : s_10_5 139 # ASSIGN : s_10_6 701 # ASSIGN : s_10_7 29 # ASSIGN : s_10_8 247 # ASSIGN : s_10_9 435 # ASSIGN : s_10_10 607 # ASSIGN : s_10_11 512 # ASSIGN : s_10_12 683 # ASSIGN : s_10_13 798 # ASSIGN : s_10_14 891 # ASSIGN : s_11_0 934 # ASSIGN : s_11_1 844 # ASSIGN : s_11_2 345 # ASSIGN : s_11_3 721 # ASSIGN : s_11_4 257 # ASSIGN : s_11_5 181 # ASSIGN : s_11_6 56 # ASSIGN : s_11_7 114 # ASSIGN : s_11_8 73 # ASSIGN : s_11_9 382 # ASSIGN : s_11_10 109 # ASSIGN : s_11_11 654 # ASSIGN : s_11_12 562 # ASSIGN : s_11_13 540 # ASSIGN : s_11_14 805 # ASSIGN : s_12_0 367 # ASSIGN : s_12_1 875 # ASSIGN : s_12_2 848 # ASSIGN : s_12_3 407 # ASSIGN : s_12_4 578 # ASSIGN : s_12_5 761 # ASSIGN : s_12_6 928 # ASSIGN : s_12_7 81 # ASSIGN : s_12_8 544 # ASSIGN : s_12_9 209 # ASSIGN : s_12_10 698 # ASSIGN : s_12_11 275 # ASSIGN : s_12_12 291 # ASSIGN : s_12_13 516 # ASSIGN : s_12_14 113 # ASSIGN : s_13_0 482 # ASSIGN : s_13_1 650 # ASSIGN : s_13_2 744 # ASSIGN : s_13_3 560 # ASSIGN : s_13_4 335 # ASSIGN : s_13_5 391 # ASSIGN : s_13_6 0 # ASSIGN : s_13_7 836 # ASSIGN : s_13_8 118 # ASSIGN : s_13_9 76 # ASSIGN : s_13_10 23 # ASSIGN : s_13_11 920 # ASSIGN : s_13_12 899 # ASSIGN : s_13_13 160 # ASSIGN : s_13_14 248 # ASSIGN : s_14_0 783 # ASSIGN : s_14_1 439 # ASSIGN : s_14_2 70 # ASSIGN : s_14_3 789 # ASSIGN : s_14_4 675 # ASSIGN : s_14_5 549 # ASSIGN : s_14_6 314 # ASSIGN : s_14_7 358 # ASSIGN : s_14_8 571 # ASSIGN : s_14_9 824 # ASSIGN : s_14_10 857 # ASSIGN : s_14_11 196 # ASSIGN : s_14_12 121 # ASSIGN : s_14_13 98 # ASSIGN : s_14_14 10 SHOW_RESULT 935 END : 935 (1 seconds) [Mon Jun 19 13:36:08 2006] SHOW_RESULT 935 CPU : 0.699999999999998 = 0.689999999999998 + 0.01 + 0 + 0 # BOUND : makespan 934 935 MODIFY_CNF 934 BEGIN : [Mon Jun 19 13:36:08 2006] MODIFY_CNF 934 END : 217539821 bytes (0 seconds) [Mon Jun 19 13:36:08 2006] MODIFY_CNF 934 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 934 BEGIN : [Mon Jun 19 13:36:08 2006] CMD : minisat /tmp/csp2sat30961.cnf /tmp/csp2sat30961.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 6010049 17715566 | 2003349 0 0 nan | 0.000 % | | 101 | 6010049 17715566 | 2203683 101 1033 10.2 | 37.116 % | | 251 | 6010049 17715566 | 2424052 251 3823 15.2 | 37.116 % | | 476 | 6010049 17715566 | 2666457 476 9971 20.9 | 37.116 % | ============================================================================== restarts : 4 conflicts : 514 (22 /sec) decisions : 3253 (142 /sec) propagations : 1922783 (84074 /sec) conflict literals : 10719 (11.02 % deleted) Memory used : 368.34 MB CPU time : 22.87 s SATISFIABLE VERIFY_CNF 934 END : (24 seconds) [Mon Jun 19 13:36:32 2006] VERIFY_CNF 934 CPU : 24.23 = 0 + 0 + 23.04 + 1.19 # RESULT : makespan 934 SATISFIABLE SHOW_RESULT 934 BEGIN : [Mon Jun 19 13:36:32 2006] # ASSIGN : makespan 934 # ASSIGN : s_0_0 552 # ASSIGN : s_0_1 288 # ASSIGN : s_0_2 301 # ASSIGN : s_0_3 841 # ASSIGN : s_0_4 36 # ASSIGN : s_0_5 131 # ASSIGN : s_0_6 642 # ASSIGN : s_0_7 190 # ASSIGN : s_0_8 489 # ASSIGN : s_0_9 697 # ASSIGN : s_0_10 170 # ASSIGN : s_0_11 432 # ASSIGN : s_0_12 326 # ASSIGN : s_0_13 0 # ASSIGN : s_0_14 53 # ASSIGN : s_1_0 277 # ASSIGN : s_1_1 4 # ASSIGN : s_1_2 426 # ASSIGN : s_1_3 678 # ASSIGN : s_1_4 51 # ASSIGN : s_1_5 290 # ASSIGN : s_1_6 100 # ASSIGN : s_1_7 113 # ASSIGN : s_1_8 200 # ASSIGN : s_1_9 643 # ASSIGN : s_1_10 797 # ASSIGN : s_1_11 514 # ASSIGN : s_1_12 790 # ASSIGN : s_1_13 341 # ASSIGN : s_1_14 571 # ASSIGN : s_2_0 719 # ASSIGN : s_2_1 492 # ASSIGN : s_2_2 241 # ASSIGN : s_2_3 14 # ASSIGN : s_2_4 627 # ASSIGN : s_2_5 807 # ASSIGN : s_2_6 200 # ASSIGN : s_2_7 490 # ASSIGN : s_2_8 918 # ASSIGN : s_2_9 132 # ASSIGN : s_2_10 545 # ASSIGN : s_2_11 345 # ASSIGN : s_2_12 268 # ASSIGN : s_2_13 36 # ASSIGN : s_2_14 695 # ASSIGN : s_3_0 856 # ASSIGN : s_3_1 455 # ASSIGN : s_3_2 139 # ASSIGN : s_3_3 341 # ASSIGN : s_3_4 97 # ASSIGN : s_3_5 189 # ASSIGN : s_3_6 902 # ASSIGN : s_3_7 697 # ASSIGN : s_3_8 236 # ASSIGN : s_3_9 768 # ASSIGN : s_3_10 522 # ASSIGN : s_3_11 278 # ASSIGN : s_3_12 555 # ASSIGN : s_3_13 625 # ASSIGN : s_3_14 643 # ASSIGN : s_4_0 788 # ASSIGN : s_4_1 173 # ASSIGN : s_4_2 200 # ASSIGN : s_4_3 850 # ASSIGN : s_4_4 206 # ASSIGN : s_4_5 1 # ASSIGN : s_4_6 260 # ASSIGN : s_4_7 828 # ASSIGN : s_4_8 272 # ASSIGN : s_4_9 91 # ASSIGN : s_4_10 929 # ASSIGN : s_4_11 57 # ASSIGN : s_4_12 704 # ASSIGN : s_4_13 444 # ASSIGN : s_4_14 477 # ASSIGN : s_5_0 174 # ASSIGN : s_5_1 101 # ASSIGN : s_5_2 902 # ASSIGN : s_5_3 438 # ASSIGN : s_5_4 534 # ASSIGN : s_5_5 434 # ASSIGN : s_5_6 712 # ASSIGN : s_5_7 11 # ASSIGN : s_5_8 318 # ASSIGN : s_5_9 285 # ASSIGN : s_5_10 634 # ASSIGN : s_5_11 888 # ASSIGN : s_5_12 842 # ASSIGN : s_5_13 798 # ASSIGN : s_5_14 188 # ASSIGN : s_6_0 933 # ASSIGN : s_6_1 213 # ASSIGN : s_6_2 350 # ASSIGN : s_6_3 75 # ASSIGN : s_6_4 710 # ASSIGN : s_6_5 761 # ASSIGN : s_6_6 544 # ASSIGN : s_6_7 500 # ASSIGN : s_6_8 1 # ASSIGN : s_6_9 186 # ASSIGN : s_6_10 421 # ASSIGN : s_6_11 559 # ASSIGN : s_6_12 625 # ASSIGN : s_6_13 648 # ASSIGN : s_6_14 804 # ASSIGN : s_7_0 833 # ASSIGN : s_7_1 81 # ASSIGN : s_7_2 760 # ASSIGN : s_7_3 126 # ASSIGN : s_7_4 419 # ASSIGN : s_7_5 896 # ASSIGN : s_7_6 874 # ASSIGN : s_7_7 343 # ASSIGN : s_7_8 529 # ASSIGN : s_7_9 595 # ASSIGN : s_7_10 511 # ASSIGN : s_7_11 872 # ASSIGN : s_7_12 694 # ASSIGN : s_7_13 581 # ASSIGN : s_7_14 275 # ASSIGN : s_8_0 649 # ASSIGN : s_8_1 196 # ASSIGN : s_8_2 668 # ASSIGN : s_8_3 570 # ASSIGN : s_8_4 375 # ASSIGN : s_8_5 39 # ASSIGN : s_8_6 785 # ASSIGN : s_8_7 274 # ASSIGN : s_8_8 398 # ASSIGN : s_8_9 876 # ASSIGN : s_8_10 12 # ASSIGN : s_8_11 692 # ASSIGN : s_8_12 676 # ASSIGN : s_8_13 473 # ASSIGN : s_8_14 118 # ASSIGN : s_9_0 95 # ASSIGN : s_9_1 889 # ASSIGN : s_9_2 669 # ASSIGN : s_9_3 536 # ASSIGN : s_9_4 177 # ASSIGN : s_9_5 373 # ASSIGN : s_9_6 453 # ASSIGN : s_9_7 425 # ASSIGN : s_9_8 580 # ASSIGN : s_9_9 203 # ASSIGN : s_9_10 286 # ASSIGN : s_9_11 98 # ASSIGN : s_9_12 2 # ASSIGN : s_9_13 814 # ASSIGN : s_9_14 715 # ASSIGN : s_10_0 301 # ASSIGN : s_10_1 790 # ASSIGN : s_10_2 522 # ASSIGN : s_10_3 190 # ASSIGN : s_10_4 905 # ASSIGN : s_10_5 478 # ASSIGN : s_10_6 3 # ASSIGN : s_10_7 766 # ASSIGN : s_10_8 101 # ASSIGN : s_10_9 356 # ASSIGN : s_10_10 690 # ASSIGN : s_10_11 595 # ASSIGN : s_10_12 246 # ASSIGN : s_10_13 264 # ASSIGN : s_10_14 433 # ASSIGN : s_11_0 779 # ASSIGN : s_11_1 303 # ASSIGN : s_11_2 863 # ASSIGN : s_11_3 610 # ASSIGN : s_11_4 334 # ASSIGN : s_11_5 694 # ASSIGN : s_11_6 391 # ASSIGN : s_11_7 543 # ASSIGN : s_11_8 500 # ASSIGN : s_11_9 5 # ASSIGN : s_11_10 780 # ASSIGN : s_11_11 796 # ASSIGN : s_11_12 408 # ASSIGN : s_11_13 785 # ASSIGN : s_11_14 900 # ASSIGN : s_12_0 527 # ASSIGN : s_12_1 550 # ASSIGN : s_12_2 710 # ASSIGN : s_12_3 249 # ASSIGN : s_12_4 761 # ASSIGN : s_12_5 617 # ASSIGN : s_12_6 703 # ASSIGN : s_12_7 393 # ASSIGN : s_12_8 74 # ASSIGN : s_12_9 461 # ASSIGN : s_12_10 107 # ASSIGN : s_12_11 184 # ASSIGN : s_12_12 858 # ASSIGN : s_12_13 737 # ASSIGN : s_12_14 6 # ASSIGN : s_13_0 420 # ASSIGN : s_13_1 603 # ASSIGN : s_13_2 0 # ASSIGN : s_13_3 739 # ASSIGN : s_13_4 277 # ASSIGN : s_13_5 513 # ASSIGN : s_13_6 113 # ASSIGN : s_13_7 871 # ASSIGN : s_13_8 697 # ASSIGN : s_13_9 829 # ASSIGN : s_13_10 224 # ASSIGN : s_13_11 498 # ASSIGN : s_13_12 92 # ASSIGN : s_13_13 136 # ASSIGN : s_13_14 333 # ASSIGN : s_14_0 708 # ASSIGN : s_14_1 343 # ASSIGN : s_14_2 740 # ASSIGN : s_14_3 26 # ASSIGN : s_14_4 456 # ASSIGN : s_14_5 321 # ASSIGN : s_14_6 582 # ASSIGN : s_14_7 626 # ASSIGN : s_14_8 755 # ASSIGN : s_14_9 58 # ASSIGN : s_14_10 851 # ASSIGN : s_14_11 199 # ASSIGN : s_14_12 128 # ASSIGN : s_14_13 714 # ASSIGN : s_14_14 424 SHOW_RESULT 934 END : 934 (1 seconds) [Mon Jun 19 13:36:33 2006] SHOW_RESULT 934 CPU : 0.680000000000016 = 0.670000000000016 + 0.01 + 0 + 0 # BOUND : makespan 934 934 MAIN END : (561 seconds) [Mon Jun 19 13:36:33 2006] MAIN CPU : 560.09 = 359.56 + 1.87 + 188.1 + 10.56