# TIMEOUT 18000 MAIN BEGIN : [Sun Jun 18 19:49:24 2006] READ BEGIN : csp/j5-per0-0.csp [Sun Jun 18 19:49:24 2006] READ END : csp/j5-per0-0.csp (0 seconds) [Sun Jun 18 19:49:24 2006] READ CPU : 0.23 = 0.23 + 0 + 0 + 0 # BOUND : makespan 1000 1598 GENERATE_CNF 1598 BEGIN : [Sun Jun 18 19:49:24 2006] GENERATE_CNF 1598 END : 40825 variables 335726 clauses 6904614 bytes (13 seconds) [Sun Jun 18 19:49:37 2006] GENERATE_CNF 1598 CPU : 12.2 = 12.18 + 0.02 + 0 + 0 MODIFY_CNF 1299 BEGIN : [Sun Jun 18 19:49:37 2006] MODIFY_CNF 1299 END : 6904620 bytes (0 seconds) [Sun Jun 18 19:49:37 2006] MODIFY_CNF 1299 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1299 BEGIN : [Sun Jun 18 19:49:37 2006] CMD : minisat /tmp/csp2sat13715.cnf /tmp/csp2sat13715.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 275546 786396 | 91848 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 45 (118 /sec) propagations : 40825 (107434 /sec) conflict literals : 0 ( nan % deleted) Memory used : 16.82 MB CPU time : 0.38 s SATISFIABLE VERIFY_CNF 1299 END : (0 seconds) [Sun Jun 18 19:49:37 2006] VERIFY_CNF 1299 CPU : 0.48 = 0 + 0 + 0.4 + 0.08 # RESULT : makespan 1299 SATISFIABLE SHOW_RESULT 1299 BEGIN : [Sun Jun 18 19:49:37 2006] # ASSIGN : makespan 1299 # ASSIGN : s_0_0 400 # ASSIGN : s_0_1 511 # ASSIGN : s_0_2 1017 # ASSIGN : s_0_3 173 # ASSIGN : s_0_4 78 # ASSIGN : s_1_0 583 # ASSIGN : s_1_1 820 # ASSIGN : s_1_2 7 # ASSIGN : s_1_3 376 # ASSIGN : s_1_4 210 # ASSIGN : s_2_0 880 # ASSIGN : s_2_1 97 # ASSIGN : s_2_2 234 # ASSIGN : s_2_3 601 # ASSIGN : s_2_4 376 # ASSIGN : s_3_0 167 # ASSIGN : s_3_1 1007 # ASSIGN : s_3_2 336 # ASSIGN : s_3_3 800 # ASSIGN : s_3_4 519 # ASSIGN : s_4_0 240 # ASSIGN : s_4_1 436 # ASSIGN : s_4_2 534 # ASSIGN : s_4_3 1115 # ASSIGN : s_4_4 764 SHOW_RESULT 1299 END : 1299 (0 seconds) [Sun Jun 18 19:49:37 2006] SHOW_RESULT 1299 CPU : 0.0599999999999987 = 0.0599999999999987 + 0 + 0 + 0 # BOUND : makespan 1000 1299 MODIFY_CNF 1149 BEGIN : [Sun Jun 18 19:49:37 2006] MODIFY_CNF 1149 END : 6904620 bytes (0 seconds) [Sun Jun 18 19:49:37 2006] MODIFY_CNF 1149 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1149 BEGIN : [Sun Jun 18 19:49:37 2006] CMD : minisat /tmp/csp2sat13715.cnf /tmp/csp2sat13715.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 245546 696396 | 81848 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 19 (39 /sec) decisions : 71 (145 /sec) propagations : 106847 (218055 /sec) conflict literals : 261 (14.43 % deleted) Memory used : 16.86 MB CPU time : 0.49 s SATISFIABLE VERIFY_CNF 1149 END : (1 seconds) [Sun Jun 18 19:49:38 2006] VERIFY_CNF 1149 CPU : 0.55 = 0.00999999999999979 + 0 + 0.51 + 0.03 # RESULT : makespan 1149 SATISFIABLE SHOW_RESULT 1149 BEGIN : [Sun Jun 18 19:49:38 2006] # ASSIGN : makespan 1149 # ASSIGN : s_0_0 244 # ASSIGN : s_0_1 355 # ASSIGN : s_0_2 664 # ASSIGN : s_0_3 946 # ASSIGN : s_0_4 149 # ASSIGN : s_1_0 493 # ASSIGN : s_1_1 31 # ASSIGN : s_1_2 946 # ASSIGN : s_1_3 739 # ASSIGN : s_1_4 244 # ASSIGN : s_2_0 730 # ASSIGN : s_2_1 218 # ASSIGN : s_2_2 562 # ASSIGN : s_2_3 19 # ASSIGN : s_2_4 410 # ASSIGN : s_3_0 11 # ASSIGN : s_3_1 857 # ASSIGN : s_3_2 126 # ASSIGN : s_3_3 332 # ASSIGN : s_3_4 553 # ASSIGN : s_4_0 84 # ASSIGN : s_4_1 723 # ASSIGN : s_4_2 309 # ASSIGN : s_4_3 539 # ASSIGN : s_4_4 798 SHOW_RESULT 1149 END : 1149 (0 seconds) [Sun Jun 18 19:49:38 2006] SHOW_RESULT 1149 CPU : 0.0600000000000005 = 0.0600000000000005 + 0 + 0 + 0 # BOUND : makespan 1000 1149 MODIFY_CNF 1074 BEGIN : [Sun Jun 18 19:49:38 2006] MODIFY_CNF 1074 END : 6904619 bytes (0 seconds) [Sun Jun 18 19:49:38 2006] MODIFY_CNF 1074 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1074 BEGIN : [Sun Jun 18 19:49:38 2006] CMD : minisat /tmp/csp2sat13715.cnf /tmp/csp2sat13715.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 230546 651396 | 76848 0 0 nan | 0.000 % | | 100 | 230546 651396 | 84532 100 1173 11.7 | 45.808 % | | 250 | 230546 651396 | 92986 250 2704 10.8 | 45.808 % | | 475 | 230546 651396 | 102284 475 5048 10.6 | 45.808 % | ============================================================================== restarts : 4 conflicts : 559 (232 /sec) decisions : 797 (331 /sec) propagations : 2890133 (1199225 /sec) conflict literals : 6037 (35.24 % deleted) Memory used : 16.88 MB CPU time : 2.41 s SATISFIABLE VERIFY_CNF 1074 END : (2 seconds) [Sun Jun 18 19:49:40 2006] VERIFY_CNF 1074 CPU : 2.49 = 0 + 0 + 2.43 + 0.06 # RESULT : makespan 1074 SATISFIABLE SHOW_RESULT 1074 BEGIN : [Sun Jun 18 19:49:40 2006] # ASSIGN : makespan 1074 # ASSIGN : s_0_0 559 # ASSIGN : s_0_1 238 # ASSIGN : s_0_2 792 # ASSIGN : s_0_3 35 # ASSIGN : s_0_4 670 # ASSIGN : s_1_0 671 # ASSIGN : s_1_1 51 # ASSIGN : s_1_2 460 # ASSIGN : s_1_3 249 # ASSIGN : s_1_4 908 # ASSIGN : s_2_0 37 # ASSIGN : s_2_1 937 # ASSIGN : s_2_2 663 # ASSIGN : s_2_3 456 # ASSIGN : s_2_4 765 # ASSIGN : s_3_0 474 # ASSIGN : s_3_1 547 # ASSIGN : s_3_2 277 # ASSIGN : s_3_3 867 # ASSIGN : s_3_4 32 # ASSIGN : s_4_0 914 # ASSIGN : s_4_1 839 # ASSIGN : s_4_2 47 # ASSIGN : s_4_3 655 # ASSIGN : s_4_4 304 SHOW_RESULT 1074 END : 1074 (0 seconds) [Sun Jun 18 19:49:40 2006] SHOW_RESULT 1074 CPU : 0.0600000000000007 = 0.0500000000000007 + 0.01 + 0 + 0 # BOUND : makespan 1000 1074 MODIFY_CNF 1037 BEGIN : [Sun Jun 18 19:49:40 2006] MODIFY_CNF 1037 END : 6904619 bytes (0 seconds) [Sun Jun 18 19:49:40 2006] MODIFY_CNF 1037 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1037 BEGIN : [Sun Jun 18 19:49:40 2006] CMD : minisat /tmp/csp2sat13715.cnf /tmp/csp2sat13715.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 223146 629196 | 74382 0 0 nan | 0.000 % | | 100 | 223147 629196 | 81820 99 932 9.4 | 48.164 % | | 250 | 223150 629196 | 90002 246 2067 8.4 | 48.164 % | | 478 | 220057 619926 | 99002 403 3209 8.0 | 50.251 % | ============================================================================== restarts : 4 conflicts : 560 (248 /sec) decisions : 703 (311 /sec) propagations : 2685188 (1188136 /sec) conflict literals : 4071 (35.47 % deleted) Memory used : 16.71 MB CPU time : 2.26 s UNSATISFIABLE VERIFY_CNF 1037 END : (3 seconds) [Sun Jun 18 19:49:43 2006] VERIFY_CNF 1037 CPU : 2.29 = 0 + 0 + 2.26 + 0.03 # RESULT : makespan 1037 UNSATISFIABLE # BOUND : makespan 1038 1074 MODIFY_CNF 1056 BEGIN : [Sun Jun 18 19:49:43 2006] MODIFY_CNF 1056 END : 6904619 bytes (0 seconds) [Sun Jun 18 19:49:43 2006] MODIFY_CNF 1056 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1056 BEGIN : [Sun Jun 18 19:49:43 2006] CMD : minisat /tmp/csp2sat13715.cnf /tmp/csp2sat13715.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 226946 640596 | 75648 0 0 nan | 0.000 % | | 100 | 226946 640596 | 83212 100 1082 10.8 | 46.954 % | ============================================================================== restarts : 2 conflicts : 177 (172 /sec) decisions : 316 (307 /sec) propagations : 928347 (901308 /sec) conflict literals : 1870 (30.48 % deleted) Memory used : 16.88 MB CPU time : 1.03 s SATISFIABLE VERIFY_CNF 1056 END : (1 seconds) [Sun Jun 18 19:49:44 2006] VERIFY_CNF 1056 CPU : 1.13 = 0 + 0 + 1.05 + 0.08 # RESULT : makespan 1056 SATISFIABLE SHOW_RESULT 1056 BEGIN : [Sun Jun 18 19:49:44 2006] # ASSIGN : makespan 1056 # ASSIGN : s_0_0 945 # ASSIGN : s_0_1 39 # ASSIGN : s_0_2 663 # ASSIGN : s_0_3 459 # ASSIGN : s_0_4 348 # ASSIGN : s_1_0 192 # ASSIGN : s_1_1 869 # ASSIGN : s_1_2 459 # ASSIGN : s_1_3 662 # ASSIGN : s_1_4 26 # ASSIGN : s_2_0 526 # ASSIGN : s_2_1 365 # ASSIGN : s_2_2 954 # ASSIGN : s_2_3 6 # ASSIGN : s_2_4 205 # ASSIGN : s_3_0 429 # ASSIGN : s_3_1 502 # ASSIGN : s_3_2 30 # ASSIGN : s_3_3 222 # ASSIGN : s_3_4 811 # ASSIGN : s_4_0 32 # ASSIGN : s_4_1 794 # ASSIGN : s_4_2 213 # ASSIGN : s_4_3 872 # ASSIGN : s_4_4 443 SHOW_RESULT 1056 END : 1056 (0 seconds) [Sun Jun 18 19:49:44 2006] SHOW_RESULT 1056 CPU : 0.0599999999999987 = 0.0599999999999987 + 0 + 0 + 0 # BOUND : makespan 1038 1056 MODIFY_CNF 1047 BEGIN : [Sun Jun 18 19:49:44 2006] MODIFY_CNF 1047 END : 6904619 bytes (0 seconds) [Sun Jun 18 19:49:44 2006] MODIFY_CNF 1047 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1047 BEGIN : [Sun Jun 18 19:49:44 2006] CMD : minisat /tmp/csp2sat13715.cnf /tmp/csp2sat13715.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 225146 635196 | 75048 0 0 nan | 0.000 % | | 100 | 225146 635196 | 82552 100 981 9.8 | 47.527 % | | 250 | 225147 635196 | 90808 249 2167 8.7 | 47.527 % | ============================================================================== restarts : 3 conflicts : 452 (235 /sec) decisions : 610 (318 /sec) propagations : 2239666 (1166493 /sec) conflict literals : 3822 (35.97 % deleted) Memory used : 16.88 MB CPU time : 1.92 s SATISFIABLE VERIFY_CNF 1047 END : (2 seconds) [Sun Jun 18 19:49:46 2006] VERIFY_CNF 1047 CPU : 1.98 = 0 + 0 + 1.94 + 0.04 # RESULT : makespan 1047 SATISFIABLE SHOW_RESULT 1047 BEGIN : [Sun Jun 18 19:49:46 2006] # ASSIGN : makespan 1047 # ASSIGN : s_0_0 532 # ASSIGN : s_0_1 211 # ASSIGN : s_0_2 765 # ASSIGN : s_0_3 8 # ASSIGN : s_0_4 643 # ASSIGN : s_1_0 644 # ASSIGN : s_1_1 24 # ASSIGN : s_1_2 433 # ASSIGN : s_1_3 222 # ASSIGN : s_1_4 881 # ASSIGN : s_2_0 10 # ASSIGN : s_2_1 910 # ASSIGN : s_2_2 636 # ASSIGN : s_2_3 429 # ASSIGN : s_2_4 738 # ASSIGN : s_3_0 447 # ASSIGN : s_3_1 520 # ASSIGN : s_3_2 250 # ASSIGN : s_3_3 840 # ASSIGN : s_3_4 5 # ASSIGN : s_4_0 887 # ASSIGN : s_4_1 812 # ASSIGN : s_4_2 20 # ASSIGN : s_4_3 628 # ASSIGN : s_4_4 277 SHOW_RESULT 1047 END : 1047 (0 seconds) [Sun Jun 18 19:49:46 2006] SHOW_RESULT 1047 CPU : 0.0600000000000005 = 0.0600000000000005 + 0 + 0 + 0 # BOUND : makespan 1038 1047 MODIFY_CNF 1042 BEGIN : [Sun Jun 18 19:49:46 2006] MODIFY_CNF 1042 END : 6904619 bytes (0 seconds) [Sun Jun 18 19:49:46 2006] MODIFY_CNF 1042 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1042 BEGIN : [Sun Jun 18 19:49:46 2006] CMD : minisat /tmp/csp2sat13715.cnf /tmp/csp2sat13715.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 224146 632196 | 74715 0 0 nan | 0.000 % | | 100 | 224146 632196 | 82186 100 852 8.5 | 47.846 % | ============================================================================== restarts : 2 conflicts : 116 (143 /sec) decisions : 176 (217 /sec) propagations : 611828 (755343 /sec) conflict literals : 1010 (29.57 % deleted) Memory used : 16.88 MB CPU time : 0.81 s SATISFIABLE VERIFY_CNF 1042 END : (1 seconds) [Sun Jun 18 19:49:47 2006] VERIFY_CNF 1042 CPU : 0.9 = 0 + 0 + 0.83 + 0.07 # RESULT : makespan 1042 SATISFIABLE SHOW_RESULT 1042 BEGIN : [Sun Jun 18 19:49:47 2006] # ASSIGN : makespan 1042 # ASSIGN : s_0_0 419 # ASSIGN : s_0_1 530 # ASSIGN : s_0_2 27 # ASSIGN : s_0_3 839 # ASSIGN : s_0_4 324 # ASSIGN : s_1_0 174 # ASSIGN : s_1_1 855 # ASSIGN : s_1_2 411 # ASSIGN : s_1_3 632 # ASSIGN : s_1_4 0 # ASSIGN : s_2_0 623 # ASSIGN : s_2_1 26 # ASSIGN : s_2_2 309 # ASSIGN : s_2_3 424 # ASSIGN : s_2_4 166 # ASSIGN : s_3_0 541 # ASSIGN : s_3_1 238 # ASSIGN : s_3_2 614 # ASSIGN : s_3_3 31 # ASSIGN : s_3_4 797 # ASSIGN : s_4_0 3 # ASSIGN : s_4_1 163 # ASSIGN : s_4_2 812 # ASSIGN : s_4_3 240 # ASSIGN : s_4_4 446 SHOW_RESULT 1042 END : 1042 (0 seconds) [Sun Jun 18 19:49:47 2006] SHOW_RESULT 1042 CPU : 0.0600000000000005 = 0.0600000000000005 + 0 + 0 + 0 # BOUND : makespan 1038 1042 MODIFY_CNF 1040 BEGIN : [Sun Jun 18 19:49:47 2006] MODIFY_CNF 1040 END : 6904619 bytes (0 seconds) [Sun Jun 18 19:49:47 2006] MODIFY_CNF 1040 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1040 BEGIN : [Sun Jun 18 19:49:47 2006] CMD : minisat /tmp/csp2sat13715.cnf /tmp/csp2sat13715.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 223746 630996 | 74582 0 0 nan | 0.000 % | | 100 | 223747 630996 | 82040 99 836 8.4 | 47.973 % | | 250 | 223749 630996 | 90244 247 1856 7.5 | 47.973 % | | 476 | 223754 630996 | 99268 468 3613 7.7 | 47.973 % | ============================================================================== restarts : 4 conflicts : 596 (244 /sec) decisions : 750 (307 /sec) propagations : 2980972 (1221710 /sec) conflict literals : 4374 (36.86 % deleted) Memory used : 16.71 MB CPU time : 2.44 s UNSATISFIABLE VERIFY_CNF 1040 END : (2 seconds) [Sun Jun 18 19:49:49 2006] VERIFY_CNF 1040 CPU : 2.5 = 0 + 0 + 2.44 + 0.06 # RESULT : makespan 1040 UNSATISFIABLE # BOUND : makespan 1041 1042 MODIFY_CNF 1041 BEGIN : [Sun Jun 18 19:49:49 2006] MODIFY_CNF 1041 END : 6904619 bytes (0 seconds) [Sun Jun 18 19:49:49 2006] MODIFY_CNF 1041 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1041 BEGIN : [Sun Jun 18 19:49:49 2006] CMD : minisat /tmp/csp2sat13715.cnf /tmp/csp2sat13715.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 223946 631596 | 74648 0 0 nan | 0.000 % | | 100 | 223947 631596 | 82112 99 890 9.0 | 47.909 % | | 250 | 223949 631596 | 90324 247 2115 8.6 | 47.909 % | | 476 | 218989 616755 | 99356 348 2958 8.5 | 49.862 % | ============================================================================== restarts : 4 conflicts : 596 (233 /sec) decisions : 747 (292 /sec) propagations : 3061873 (1196044 /sec) conflict literals : 4408 (37.81 % deleted) Memory used : 16.72 MB CPU time : 2.56 s UNSATISFIABLE VERIFY_CNF 1041 END : (3 seconds) [Sun Jun 18 19:49:52 2006] VERIFY_CNF 1041 CPU : 2.6 = 0 + 0 + 2.56 + 0.04 # RESULT : makespan 1041 UNSATISFIABLE # BOUND : makespan 1042 1042 MAIN END : (28 seconds) [Sun Jun 18 19:49:52 2006] MAIN CPU : 27.72 = 12.78 + 0.03 + 14.42 + 0.49