# TIMEOUT 18000 MAIN BEGIN : [Sun Jun 18 20:10:52 2006] READ BEGIN : csp/j6-per20-0.csp [Sun Jun 18 20:10:52 2006] READ END : csp/j6-per20-0.csp (1 seconds) [Sun Jun 18 20:10:53 2006] READ CPU : 0.42 = 0.42 + 0 + 0 + 0 # BOUND : makespan 1000 1890 GENERATE_CNF 1890 BEGIN : [Sun Jun 18 20:10:53 2006] GENERATE_CNF 1890 END : 69400 variables 727773 clauses 15263169 bytes (26 seconds) [Sun Jun 18 20:11:19 2006] GENERATE_CNF 1890 CPU : 26.73 = 26.62 + 0.11 + 0 + 0 MODIFY_CNF 1445 BEGIN : [Sun Jun 18 20:11:19 2006] MODIFY_CNF 1445 END : 15263175 bytes (0 seconds) [Sun Jun 18 20:11:19 2006] MODIFY_CNF 1445 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1445 BEGIN : [Sun Jun 18 20:11:19 2006] CMD : minisat /tmp/csp2sat14244.cnf /tmp/csp2sat14244.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 566956 1632412 | 188985 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 13 (14 /sec) decisions : 157 (164 /sec) propagations : 155175 (161641 /sec) conflict literals : 281 (11.64 % deleted) Memory used : 32.14 MB CPU time : 0.96 s SATISFIABLE VERIFY_CNF 1445 END : (2 seconds) [Sun Jun 18 20:11:21 2006] VERIFY_CNF 1445 CPU : 1.08 = 0 + 0 + 1 + 0.08 # RESULT : makespan 1445 SATISFIABLE SHOW_RESULT 1445 BEGIN : [Sun Jun 18 20:11:21 2006] # ASSIGN : makespan 1445 # ASSIGN : s_0_0 1079 # ASSIGN : s_0_1 1319 # ASSIGN : s_0_2 13 # ASSIGN : s_0_3 131 # ASSIGN : s_0_4 82 # ASSIGN : s_0_5 645 # ASSIGN : s_1_0 714 # ASSIGN : s_1_1 1087 # ASSIGN : s_1_2 38 # ASSIGN : s_1_3 569 # ASSIGN : s_1_4 198 # ASSIGN : s_1_5 839 # ASSIGN : s_2_0 1234 # ASSIGN : s_2_1 780 # ASSIGN : s_2_2 180 # ASSIGN : s_2_3 574 # ASSIGN : s_2_4 372 # ASSIGN : s_2_5 998 # ASSIGN : s_3_0 909 # ASSIGN : s_3_1 538 # ASSIGN : s_3_2 251 # ASSIGN : s_3_3 843 # ASSIGN : s_3_4 563 # ASSIGN : s_3_5 1028 # ASSIGN : s_4_0 849 # ASSIGN : s_4_1 489 # ASSIGN : s_4_2 508 # ASSIGN : s_4_3 926 # ASSIGN : s_4_4 973 # ASSIGN : s_4_5 1153 # ASSIGN : s_5_0 384 # ASSIGN : s_5_1 92 # ASSIGN : s_5_2 1251 # ASSIGN : s_5_3 1347 # ASSIGN : s_5_4 1150 # ASSIGN : s_5_5 1437 SHOW_RESULT 1445 END : 1445 (0 seconds) [Sun Jun 18 20:11:21 2006] SHOW_RESULT 1445 CPU : 0.120000000000003 = 0.0900000000000034 + 0.03 + 0 + 0 # BOUND : makespan 1000 1445 MODIFY_CNF 1222 BEGIN : [Sun Jun 18 20:11:21 2006] MODIFY_CNF 1222 END : 15263175 bytes (0 seconds) [Sun Jun 18 20:11:21 2006] MODIFY_CNF 1222 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1222 BEGIN : [Sun Jun 18 20:11:21 2006] CMD : minisat /tmp/csp2sat14244.cnf /tmp/csp2sat14244.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 486676 1391572 | 162225 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 1 (1 /sec) decisions : 84 (94 /sec) propagations : 73501 (82585 /sec) conflict literals : 10 (0.00 % deleted) Memory used : 32.14 MB CPU time : 0.89 s SATISFIABLE VERIFY_CNF 1222 END : (1 seconds) [Sun Jun 18 20:11:22 2006] VERIFY_CNF 1222 CPU : 1.04 = 0 + 0 + 0.93 + 0.11 # RESULT : makespan 1222 SATISFIABLE SHOW_RESULT 1222 BEGIN : [Sun Jun 18 20:11:22 2006] # ASSIGN : makespan 1222 # ASSIGN : s_0_0 709 # ASSIGN : s_0_1 864 # ASSIGN : s_0_2 684 # ASSIGN : s_0_3 246 # ASSIGN : s_0_4 1 # ASSIGN : s_0_5 52 # ASSIGN : s_1_0 865 # ASSIGN : s_1_1 990 # ASSIGN : s_1_2 723 # ASSIGN : s_1_3 688 # ASSIGN : s_1_4 50 # ASSIGN : s_1_5 256 # ASSIGN : s_2_0 1011 # ASSIGN : s_2_1 475 # ASSIGN : s_2_2 153 # ASSIGN : s_2_3 693 # ASSIGN : s_2_4 224 # ASSIGN : s_2_5 415 # ASSIGN : s_3_0 50 # ASSIGN : s_3_1 420 # ASSIGN : s_3_2 965 # ASSIGN : s_3_3 899 # ASSIGN : s_3_4 574 # ASSIGN : s_3_5 445 # ASSIGN : s_4_0 169 # ASSIGN : s_4_1 68 # ASSIGN : s_4_2 229 # ASSIGN : s_4_3 1085 # ASSIGN : s_4_4 854 # ASSIGN : s_4_5 570 # ASSIGN : s_5_0 379 # ASSIGN : s_5_1 87 # ASSIGN : s_5_2 869 # ASSIGN : s_5_3 1132 # ASSIGN : s_5_4 1031 # ASSIGN : s_5_5 1023 SHOW_RESULT 1222 END : 1222 (0 seconds) [Sun Jun 18 20:11:22 2006] SHOW_RESULT 1222 CPU : 0.110000000000001 = 0.100000000000001 + 0.00999999999999998 + 0 + 0 # BOUND : makespan 1000 1222 MODIFY_CNF 1111 BEGIN : [Sun Jun 18 20:11:22 2006] MODIFY_CNF 1111 END : 15263175 bytes (0 seconds) [Sun Jun 18 20:11:22 2006] MODIFY_CNF 1111 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1111 BEGIN : [Sun Jun 18 20:11:22 2006] CMD : minisat /tmp/csp2sat14244.cnf /tmp/csp2sat14244.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 446716 1271692 | 148905 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (2 /sec) decisions : 71 (76 /sec) propagations : 71644 (77037 /sec) conflict literals : 10 (0.00 % deleted) Memory used : 32.14 MB CPU time : 0.93 s SATISFIABLE VERIFY_CNF 1111 END : (1 seconds) [Sun Jun 18 20:11:23 2006] VERIFY_CNF 1111 CPU : 1.06 = 0 + 0.01 + 0.97 + 0.08 # RESULT : makespan 1111 SATISFIABLE SHOW_RESULT 1111 BEGIN : [Sun Jun 18 20:11:23 2006] # ASSIGN : makespan 1111 # ASSIGN : s_0_0 269 # ASSIGN : s_0_1 500 # ASSIGN : s_0_2 12 # ASSIGN : s_0_3 626 # ASSIGN : s_0_4 451 # ASSIGN : s_0_5 37 # ASSIGN : s_1_0 754 # ASSIGN : s_1_1 879 # ASSIGN : s_1_2 612 # ASSIGN : s_1_3 20 # ASSIGN : s_1_4 25 # ASSIGN : s_1_5 231 # ASSIGN : s_2_0 900 # ASSIGN : s_2_1 661 # ASSIGN : s_2_2 128 # ASSIGN : s_2_3 420 # ASSIGN : s_2_4 199 # ASSIGN : s_2_5 390 # ASSIGN : s_3_0 29 # ASSIGN : s_3_1 4 # ASSIGN : s_3_2 854 # ASSIGN : s_3_3 354 # ASSIGN : s_3_4 553 # ASSIGN : s_3_5 424 # ASSIGN : s_4_0 148 # ASSIGN : s_4_1 113 # ASSIGN : s_4_2 208 # ASSIGN : s_4_3 1064 # ASSIGN : s_4_4 833 # ASSIGN : s_4_5 549 # ASSIGN : s_5_0 424 # ASSIGN : s_5_1 132 # ASSIGN : s_5_2 758 # ASSIGN : s_5_3 42 # ASSIGN : s_5_4 1010 # ASSIGN : s_5_5 1002 SHOW_RESULT 1111 END : 1111 (0 seconds) [Sun Jun 18 20:11:23 2006] SHOW_RESULT 1111 CPU : 0.109999999999999 = 0.109999999999999 + 0 + 0 + 0 # BOUND : makespan 1000 1111 MODIFY_CNF 1055 BEGIN : [Sun Jun 18 20:11:23 2006] MODIFY_CNF 1055 END : 15263174 bytes (0 seconds) [Sun Jun 18 20:11:23 2006] MODIFY_CNF 1055 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1055 BEGIN : [Sun Jun 18 20:11:23 2006] CMD : minisat /tmp/csp2sat14244.cnf /tmp/csp2sat14244.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 426556 1211212 | 142185 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 11 (11 /sec) decisions : 88 (86 /sec) propagations : 130364 (127808 /sec) conflict literals : 190 (9.09 % deleted) Memory used : 32.14 MB CPU time : 1.02 s SATISFIABLE VERIFY_CNF 1055 END : (1 seconds) [Sun Jun 18 20:11:24 2006] VERIFY_CNF 1055 CPU : 1.12 = 0 + 0.01 + 1.05 + 0.06 # RESULT : makespan 1055 SATISFIABLE SHOW_RESULT 1055 BEGIN : [Sun Jun 18 20:11:24 2006] # ASSIGN : makespan 1055 # ASSIGN : s_0_0 900 # ASSIGN : s_0_1 774 # ASSIGN : s_0_2 748 # ASSIGN : s_0_3 274 # ASSIGN : s_0_4 15 # ASSIGN : s_0_5 80 # ASSIGN : s_1_0 183 # ASSIGN : s_1_1 540 # ASSIGN : s_1_2 33 # ASSIGN : s_1_3 178 # ASSIGN : s_1_4 772 # ASSIGN : s_1_5 381 # ASSIGN : s_2_0 638 # ASSIGN : s_2_1 298 # ASSIGN : s_2_2 537 # ASSIGN : s_2_3 849 # ASSIGN : s_2_4 64 # ASSIGN : s_2_5 608 # ASSIGN : s_3_0 64 # ASSIGN : s_3_1 1030 # ASSIGN : s_3_2 773 # ASSIGN : s_3_3 189 # ASSIGN : s_3_4 255 # ASSIGN : s_3_5 638 # ASSIGN : s_4_0 4 # ASSIGN : s_4_1 516 # ASSIGN : s_4_2 175 # ASSIGN : s_4_3 712 # ASSIGN : s_4_4 535 # ASSIGN : s_4_5 763 # ASSIGN : s_5_0 308 # ASSIGN : s_5_1 6 # ASSIGN : s_5_2 652 # ASSIGN : s_5_3 759 # ASSIGN : s_5_4 946 # ASSIGN : s_5_5 1047 SHOW_RESULT 1055 END : 1055 (0 seconds) [Sun Jun 18 20:11:24 2006] SHOW_RESULT 1055 CPU : 0.109999999999999 = 0.109999999999999 + 0 + 0 + 0 # BOUND : makespan 1000 1055 MODIFY_CNF 1027 BEGIN : [Sun Jun 18 20:11:24 2006] MODIFY_CNF 1027 END : 15263174 bytes (0 seconds) [Sun Jun 18 20:11:24 2006] MODIFY_CNF 1027 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1027 BEGIN : [Sun Jun 18 20:11:24 2006] CMD : minisat /tmp/csp2sat14244.cnf /tmp/csp2sat14244.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 416476 1180972 | 138825 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 5 (5 /sec) decisions : 81 (84 /sec) propagations : 96095 (100099 /sec) conflict literals : 73 (9.88 % deleted) Memory used : 32.14 MB CPU time : 0.96 s SATISFIABLE VERIFY_CNF 1027 END : (1 seconds) [Sun Jun 18 20:11:25 2006] VERIFY_CNF 1027 CPU : 1.08 = 0 + 0 + 0.99 + 0.09 # RESULT : makespan 1027 SATISFIABLE SHOW_RESULT 1027 BEGIN : [Sun Jun 18 20:11:25 2006] # ASSIGN : makespan 1027 # ASSIGN : s_0_0 746 # ASSIGN : s_0_1 901 # ASSIGN : s_0_2 6 # ASSIGN : s_0_3 308 # ASSIGN : s_0_4 31 # ASSIGN : s_0_5 114 # ASSIGN : s_1_0 902 # ASSIGN : s_1_1 55 # ASSIGN : s_1_2 557 # ASSIGN : s_1_3 303 # ASSIGN : s_1_4 728 # ASSIGN : s_1_5 346 # ASSIGN : s_2_0 535 # ASSIGN : s_2_1 287 # ASSIGN : s_2_2 956 # ASSIGN : s_2_3 750 # ASSIGN : s_2_4 80 # ASSIGN : s_2_5 505 # ASSIGN : s_3_0 86 # ASSIGN : s_3_1 30 # ASSIGN : s_3_2 699 # ASSIGN : s_3_3 961 # ASSIGN : s_3_4 271 # ASSIGN : s_3_5 574 # ASSIGN : s_4_0 26 # ASSIGN : s_4_1 7 # ASSIGN : s_4_2 210 # ASSIGN : s_4_3 163 # ASSIGN : s_4_4 551 # ASSIGN : s_4_5 735 # ASSIGN : s_5_0 205 # ASSIGN : s_5_1 609 # ASSIGN : s_5_2 109 # ASSIGN : s_5_3 19 # ASSIGN : s_5_4 918 # ASSIGN : s_5_5 1019 SHOW_RESULT 1027 END : 1027 (0 seconds) [Sun Jun 18 20:11:25 2006] SHOW_RESULT 1027 CPU : 0.109999999999999 = 0.109999999999999 + 0 + 0 + 0 # BOUND : makespan 1000 1027 MODIFY_CNF 1013 BEGIN : [Sun Jun 18 20:11:25 2006] MODIFY_CNF 1013 END : 15263174 bytes (0 seconds) [Sun Jun 18 20:11:25 2006] MODIFY_CNF 1013 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1013 BEGIN : [Sun Jun 18 20:11:25 2006] CMD : minisat /tmp/csp2sat14244.cnf /tmp/csp2sat14244.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 411436 1165852 | 137145 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 11 (10 /sec) decisions : 88 (84 /sec) propagations : 116559 (111009 /sec) conflict literals : 191 (16.59 % deleted) Memory used : 32.14 MB CPU time : 1.05 s SATISFIABLE VERIFY_CNF 1013 END : (2 seconds) [Sun Jun 18 20:11:27 2006] VERIFY_CNF 1013 CPU : 1.23 = 0 + 0 + 1.08 + 0.15 # RESULT : makespan 1013 SATISFIABLE SHOW_RESULT 1013 BEGIN : [Sun Jun 18 20:11:27 2006] # ASSIGN : makespan 1013 # ASSIGN : s_0_0 732 # ASSIGN : s_0_1 887 # ASSIGN : s_0_2 640 # ASSIGN : s_0_3 202 # ASSIGN : s_0_4 665 # ASSIGN : s_0_5 8 # ASSIGN : s_1_0 888 # ASSIGN : s_1_1 19 # ASSIGN : s_1_2 498 # ASSIGN : s_1_3 1 # ASSIGN : s_1_4 714 # ASSIGN : s_1_5 332 # ASSIGN : s_2_0 521 # ASSIGN : s_2_1 251 # ASSIGN : s_2_2 942 # ASSIGN : s_2_3 736 # ASSIGN : s_2_4 17 # ASSIGN : s_2_5 491 # ASSIGN : s_3_0 72 # ASSIGN : s_3_1 532 # ASSIGN : s_3_2 685 # ASSIGN : s_3_3 6 # ASSIGN : s_3_4 208 # ASSIGN : s_3_5 557 # ASSIGN : s_4_0 12 # ASSIGN : s_4_1 469 # ASSIGN : s_4_2 128 # ASSIGN : s_4_3 966 # ASSIGN : s_4_4 488 # ASSIGN : s_4_5 682 # ASSIGN : s_5_0 191 # ASSIGN : s_5_1 595 # ASSIGN : s_5_2 5 # ASSIGN : s_5_3 101 # ASSIGN : s_5_4 904 # ASSIGN : s_5_5 1005 SHOW_RESULT 1013 END : 1013 (0 seconds) [Sun Jun 18 20:11:27 2006] SHOW_RESULT 1013 CPU : 0.109999999999999 = 0.109999999999999 + 0 + 0 + 0 # BOUND : makespan 1000 1013 MODIFY_CNF 1006 BEGIN : [Sun Jun 18 20:11:27 2006] MODIFY_CNF 1006 END : 15263173 bytes (0 seconds) [Sun Jun 18 20:11:27 2006] MODIFY_CNF 1006 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1006 BEGIN : [Sun Jun 18 20:11:27 2006] CMD : minisat /tmp/csp2sat14244.cnf /tmp/csp2sat14244.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 408916 1158292 | 136305 0 0 nan | 0.000 % | | 101 | 408916 1158292 | 149935 101 1349 13.4 | 55.167 % | | 252 | 408916 1158292 | 164929 252 3295 13.1 | 55.167 % | ============================================================================== restarts : 3 conflicts : 464 (155 /sec) decisions : 676 (225 /sec) propagations : 2685814 (895271 /sec) conflict literals : 5735 (32.56 % deleted) Memory used : 32.16 MB CPU time : 3 s SATISFIABLE VERIFY_CNF 1006 END : (3 seconds) [Sun Jun 18 20:11:30 2006] VERIFY_CNF 1006 CPU : 3.11 = 0 + 0 + 3.04 + 0.0700000000000001 # RESULT : makespan 1006 SATISFIABLE SHOW_RESULT 1006 BEGIN : [Sun Jun 18 20:11:30 2006] # ASSIGN : makespan 1006 # ASSIGN : s_0_0 851 # ASSIGN : s_0_1 0 # ASSIGN : s_0_2 628 # ASSIGN : s_0_3 126 # ASSIGN : s_0_4 564 # ASSIGN : s_0_5 653 # ASSIGN : s_1_0 722 # ASSIGN : s_1_1 414 # ASSIGN : s_1_2 41 # ASSIGN : s_1_3 31 # ASSIGN : s_1_4 213 # ASSIGN : s_1_5 847 # ASSIGN : s_2_0 511 # ASSIGN : s_2_1 192 # ASSIGN : s_2_2 440 # ASSIGN : s_2_3 800 # ASSIGN : s_2_4 1 # ASSIGN : s_2_5 410 # ASSIGN : s_3_0 62 # ASSIGN : s_3_1 689 # ASSIGN : s_3_2 183 # ASSIGN : s_3_3 623 # ASSIGN : s_3_4 726 # ASSIGN : s_3_5 498 # ASSIGN : s_4_0 2 # ASSIGN : s_4_1 646 # ASSIGN : s_4_2 665 # ASSIGN : s_4_3 576 # ASSIGN : s_4_4 387 # ASSIGN : s_4_5 103 # ASSIGN : s_5_0 181 # ASSIGN : s_5_1 714 # ASSIGN : s_5_2 517 # ASSIGN : s_5_3 36 # ASSIGN : s_5_4 613 # ASSIGN : s_5_5 28 SHOW_RESULT 1006 END : 1006 (0 seconds) [Sun Jun 18 20:11:30 2006] SHOW_RESULT 1006 CPU : 0.109999999999999 = 0.109999999999999 + 0 + 0 + 0 # BOUND : makespan 1000 1006 MODIFY_CNF 1003 BEGIN : [Sun Jun 18 20:11:30 2006] MODIFY_CNF 1003 END : 15263173 bytes (0 seconds) [Sun Jun 18 20:11:30 2006] MODIFY_CNF 1003 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1003 BEGIN : [Sun Jun 18 20:11:30 2006] CMD : minisat /tmp/csp2sat14244.cnf /tmp/csp2sat14244.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 407836 1155052 | 135945 0 0 nan | 0.000 % | | 102 | 407836 1155052 | 149539 102 1476 14.5 | 55.327 % | | 252 | 407836 1155052 | 164493 252 3223 12.8 | 55.327 % | | 477 | 407836 1155052 | 180942 477 6068 12.7 | 55.327 % | ============================================================================== restarts : 4 conflicts : 627 (173 /sec) decisions : 858 (236 /sec) propagations : 3473583 (956910 /sec) conflict literals : 7902 (32.38 % deleted) Memory used : 32.16 MB CPU time : 3.63 s SATISFIABLE VERIFY_CNF 1003 END : (4 seconds) [Sun Jun 18 20:11:34 2006] VERIFY_CNF 1003 CPU : 3.75 = 0 + 0 + 3.66 + 0.09 # RESULT : makespan 1003 SATISFIABLE SHOW_RESULT 1003 BEGIN : [Sun Jun 18 20:11:34 2006] # ASSIGN : makespan 1003 # ASSIGN : s_0_0 788 # ASSIGN : s_0_1 30 # ASSIGN : s_0_2 5 # ASSIGN : s_0_3 156 # ASSIGN : s_0_4 954 # ASSIGN : s_0_5 594 # ASSIGN : s_1_0 663 # ASSIGN : s_1_1 431 # ASSIGN : s_1_2 60 # ASSIGN : s_1_3 998 # ASSIGN : s_1_4 204 # ASSIGN : s_1_5 814 # ASSIGN : s_2_0 452 # ASSIGN : s_2_1 213 # ASSIGN : s_2_2 902 # ASSIGN : s_2_3 690 # ASSIGN : s_2_4 13 # ASSIGN : s_2_5 973 # ASSIGN : s_3_0 3 # ASSIGN : s_3_1 177 # ASSIGN : s_3_2 202 # ASSIGN : s_3_3 608 # ASSIGN : s_3_4 674 # ASSIGN : s_3_5 469 # ASSIGN : s_4_0 943 # ASSIGN : s_4_1 11 # ASSIGN : s_4_2 555 # ASSIGN : s_4_3 896 # ASSIGN : s_4_4 378 # ASSIGN : s_4_5 94 # ASSIGN : s_5_0 122 # ASSIGN : s_5_1 711 # ASSIGN : s_5_2 459 # ASSIGN : s_5_3 32 # ASSIGN : s_5_4 573 # ASSIGN : s_5_5 24 SHOW_RESULT 1003 END : 1003 (0 seconds) [Sun Jun 18 20:11:34 2006] SHOW_RESULT 1003 CPU : 0.110000000000003 = 0.110000000000003 + 0 + 0 + 0 # BOUND : makespan 1000 1003 MODIFY_CNF 1001 BEGIN : [Sun Jun 18 20:11:34 2006] MODIFY_CNF 1001 END : 15263173 bytes (0 seconds) [Sun Jun 18 20:11:34 2006] MODIFY_CNF 1001 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1001 BEGIN : [Sun Jun 18 20:11:34 2006] CMD : minisat /tmp/csp2sat14244.cnf /tmp/csp2sat14244.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 407116 1152892 | 135705 0 0 nan | 0.000 % | | 100 | 407116 1152892 | 149275 100 1431 14.3 | 55.434 % | | 250 | 407116 1152892 | 164203 250 3403 13.6 | 55.434 % | | 475 | 407116 1152892 | 180623 475 6331 13.3 | 55.434 % | | 812 | 407116 1152892 | 198685 812 10254 12.6 | 55.434 % | | 1320 | 407116 1152892 | 218554 1320 16278 12.3 | 55.434 % | ============================================================================== restarts : 6 conflicts : 1458 (185 /sec) decisions : 1934 (246 /sec) propagations : 8488654 (1078609 /sec) conflict literals : 17772 (35.53 % deleted) Memory used : 32.16 MB CPU time : 7.87 s SATISFIABLE VERIFY_CNF 1001 END : (8 seconds) [Sun Jun 18 20:11:42 2006] VERIFY_CNF 1001 CPU : 8.05 = 0 + 0 + 7.91 + 0.14 # RESULT : makespan 1001 SATISFIABLE SHOW_RESULT 1001 BEGIN : [Sun Jun 18 20:11:42 2006] # ASSIGN : makespan 1001 # ASSIGN : s_0_0 786 # ASSIGN : s_0_1 28 # ASSIGN : s_0_2 3 # ASSIGN : s_0_3 154 # ASSIGN : s_0_4 952 # ASSIGN : s_0_5 592 # ASSIGN : s_1_0 661 # ASSIGN : s_1_1 429 # ASSIGN : s_1_2 58 # ASSIGN : s_1_3 996 # ASSIGN : s_1_4 202 # ASSIGN : s_1_5 812 # ASSIGN : s_2_0 450 # ASSIGN : s_2_1 211 # ASSIGN : s_2_2 900 # ASSIGN : s_2_3 688 # ASSIGN : s_2_4 11 # ASSIGN : s_2_5 971 # ASSIGN : s_3_0 1 # ASSIGN : s_3_1 175 # ASSIGN : s_3_2 200 # ASSIGN : s_3_3 606 # ASSIGN : s_3_4 672 # ASSIGN : s_3_5 467 # ASSIGN : s_4_0 941 # ASSIGN : s_4_1 9 # ASSIGN : s_4_2 553 # ASSIGN : s_4_3 894 # ASSIGN : s_4_4 376 # ASSIGN : s_4_5 92 # ASSIGN : s_5_0 120 # ASSIGN : s_5_1 709 # ASSIGN : s_5_2 457 # ASSIGN : s_5_3 30 # ASSIGN : s_5_4 571 # ASSIGN : s_5_5 22 SHOW_RESULT 1001 END : 1001 (0 seconds) [Sun Jun 18 20:11:42 2006] SHOW_RESULT 1001 CPU : 0.109999999999999 = 0.109999999999999 + 0 + 0 + 0 # BOUND : makespan 1000 1001 MODIFY_CNF 1000 BEGIN : [Sun Jun 18 20:11:42 2006] MODIFY_CNF 1000 END : 15263173 bytes (0 seconds) [Sun Jun 18 20:11:42 2006] MODIFY_CNF 1000 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1000 BEGIN : [Sun Jun 18 20:11:42 2006] CMD : minisat /tmp/csp2sat14244.cnf /tmp/csp2sat14244.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 406757 1151812 | 135585 0 0 nan | 0.000 % | | 101 | 406757 1151812 | 149143 101 1371 13.6 | 55.487 % | | 251 | 406757 1151812 | 164057 251 3302 13.2 | 55.487 % | | 477 | 406757 1151812 | 180463 477 5646 11.8 | 55.487 % | | 814 | 406757 1151812 | 198509 814 9637 11.8 | 55.487 % | | 1320 | 406757 1151812 | 218360 1320 15170 11.5 | 55.487 % | ============================================================================== restarts : 6 conflicts : 2047 (197 /sec) decisions : 2616 (252 /sec) propagations : 11862349 (1141708 /sec) conflict literals : 23609 (36.19 % deleted) Memory used : 32.16 MB CPU time : 10.39 s SATISFIABLE VERIFY_CNF 1000 END : (11 seconds) [Sun Jun 18 20:11:53 2006] VERIFY_CNF 1000 CPU : 10.53 = 0 + 0.01 + 10.42 + 0.1 # RESULT : makespan 1000 SATISFIABLE SHOW_RESULT 1000 BEGIN : [Sun Jun 18 20:11:53 2006] # ASSIGN : makespan 1000 # ASSIGN : s_0_0 845 # ASSIGN : s_0_1 12 # ASSIGN : s_0_2 820 # ASSIGN : s_0_3 138 # ASSIGN : s_0_4 771 # ASSIGN : s_0_5 577 # ASSIGN : s_1_0 179 # ASSIGN : s_1_1 550 # ASSIGN : s_1_2 853 # ASSIGN : s_1_3 995 # ASSIGN : s_1_4 317 # ASSIGN : s_1_5 20 # ASSIGN : s_2_0 304 # ASSIGN : s_2_1 782 # ASSIGN : s_2_2 42 # ASSIGN : s_2_3 576 # ASSIGN : s_2_4 113 # ASSIGN : s_2_5 546 # ASSIGN : s_3_0 60 # ASSIGN : s_3_1 197 # ASSIGN : s_3_2 222 # ASSIGN : s_3_3 809 # ASSIGN : s_3_4 491 # ASSIGN : s_3_5 875 # ASSIGN : s_4_0 0 # ASSIGN : s_4_1 176 # ASSIGN : s_4_2 479 # ASSIGN : s_4_3 91 # ASSIGN : s_4_4 823 # ASSIGN : s_4_5 195 # ASSIGN : s_5_0 515 # ASSIGN : s_5_1 223 # ASSIGN : s_5_2 126 # ASSIGN : s_5_3 905 # ASSIGN : s_5_4 12 # ASSIGN : s_5_5 4 SHOW_RESULT 1000 END : 1000 (0 seconds) [Sun Jun 18 20:11:53 2006] SHOW_RESULT 1000 CPU : 0.110000000000001 = 0.100000000000001 + 0.01 + 0 + 0 # BOUND : makespan 1000 1000 MAIN END : (61 seconds) [Sun Jun 18 20:11:53 2006] MAIN CPU : 60.35 = 28.13 + 0.2 + 31.05 + 0.97