# TIMEOUT 18000 MAIN BEGIN : [Sun Jun 18 19:50:47 2006] READ BEGIN : csp/j5-per10-0.csp [Sun Jun 18 19:50:47 2006] READ END : csp/j5-per10-0.csp (0 seconds) [Sun Jun 18 19:50:47 2006] READ CPU : 0.23 = 0.23 + 0 + 0 + 0 # BOUND : makespan 1000 1565 GENERATE_CNF 1565 BEGIN : [Sun Jun 18 19:50:47 2006] GENERATE_CNF 1565 END : 39967 variables 329523 clauses 6777003 bytes (12 seconds) [Sun Jun 18 19:50:59 2006] GENERATE_CNF 1565 CPU : 12.43 = 12.35 + 0.08 + 0 + 0 MODIFY_CNF 1282 BEGIN : [Sun Jun 18 19:50:59 2006] MODIFY_CNF 1282 END : 6777009 bytes (0 seconds) [Sun Jun 18 19:50:59 2006] MODIFY_CNF 1282 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1282 BEGIN : [Sun Jun 18 19:50:59 2006] CMD : minisat /tmp/csp2sat13764.cnf /tmp/csp2sat13764.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 272543 778245 | 90847 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (5 /sec) decisions : 62 (148 /sec) propagations : 44883 (106864 /sec) conflict literals : 18 (0.00 % deleted) Memory used : 16.47 MB CPU time : 0.42 s SATISFIABLE VERIFY_CNF 1282 END : (1 seconds) [Sun Jun 18 19:51:00 2006] VERIFY_CNF 1282 CPU : 0.5 = 0 + 0 + 0.44 + 0.06 # RESULT : makespan 1282 SATISFIABLE SHOW_RESULT 1282 BEGIN : [Sun Jun 18 19:51:00 2006] # ASSIGN : makespan 1282 # ASSIGN : s_0_0 17 # ASSIGN : s_0_1 477 # ASSIGN : s_0_2 722 # ASSIGN : s_0_3 142 # ASSIGN : s_0_4 143 # ASSIGN : s_1_0 747 # ASSIGN : s_1_1 1051 # ASSIGN : s_1_2 34 # ASSIGN : s_1_3 166 # ASSIGN : s_1_4 716 # ASSIGN : s_2_0 146 # ASSIGN : s_2_1 6 # ASSIGN : s_2_2 341 # ASSIGN : s_2_3 472 # ASSIGN : s_2_4 743 # ASSIGN : s_3_0 38 # ASSIGN : s_3_1 201 # ASSIGN : s_3_2 343 # ASSIGN : s_3_3 745 # ASSIGN : s_3_4 1086 # ASSIGN : s_4_0 375 # ASSIGN : s_4_1 754 # ASSIGN : s_4_2 1110 # ASSIGN : s_4_3 944 # ASSIGN : s_4_4 1158 SHOW_RESULT 1282 END : 1282 (0 seconds) [Sun Jun 18 19:51:00 2006] SHOW_RESULT 1282 CPU : 0.0600000000000005 = 0.0600000000000005 + 0 + 0 + 0 # BOUND : makespan 1000 1282 MODIFY_CNF 1141 BEGIN : [Sun Jun 18 19:51:00 2006] MODIFY_CNF 1141 END : 6777009 bytes (0 seconds) [Sun Jun 18 19:51:00 2006] MODIFY_CNF 1141 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1141 BEGIN : [Sun Jun 18 19:51:00 2006] CMD : minisat /tmp/csp2sat13764.cnf /tmp/csp2sat13764.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 244343 693645 | 81447 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 4 (9 /sec) decisions : 48 (109 /sec) propagations : 53796 (122264 /sec) conflict literals : 33 (15.38 % deleted) Memory used : 16.73 MB CPU time : 0.44 s SATISFIABLE VERIFY_CNF 1141 END : (0 seconds) [Sun Jun 18 19:51:00 2006] VERIFY_CNF 1141 CPU : 0.5 = 0 + 0 + 0.46 + 0.04 # RESULT : makespan 1141 SATISFIABLE SHOW_RESULT 1141 BEGIN : [Sun Jun 18 19:51:00 2006] # ASSIGN : makespan 1141 # ASSIGN : s_0_0 1120 # ASSIGN : s_0_1 343 # ASSIGN : s_0_2 621 # ASSIGN : s_0_3 2 # ASSIGN : s_0_4 9 # ASSIGN : s_1_0 474 # ASSIGN : s_1_1 778 # ASSIGN : s_1_2 1009 # ASSIGN : s_1_3 3 # ASSIGN : s_1_4 447 # ASSIGN : s_2_0 925 # ASSIGN : s_2_1 169 # ASSIGN : s_2_2 580 # ASSIGN : s_2_3 309 # ASSIGN : s_2_4 582 # ASSIGN : s_3_0 817 # ASSIGN : s_3_1 11 # ASSIGN : s_3_2 153 # ASSIGN : s_3_3 618 # ASSIGN : s_3_4 945 # ASSIGN : s_4_0 102 # ASSIGN : s_4_1 588 # ASSIGN : s_4_2 532 # ASSIGN : s_4_3 851 # ASSIGN : s_4_4 1017 SHOW_RESULT 1141 END : 1141 (0 seconds) [Sun Jun 18 19:51:00 2006] SHOW_RESULT 1141 CPU : 0.0700000000000005 = 0.0600000000000005 + 0.01 + 0 + 0 # BOUND : makespan 1000 1141 MODIFY_CNF 1070 BEGIN : [Sun Jun 18 19:51:00 2006] MODIFY_CNF 1070 END : 6777008 bytes (0 seconds) [Sun Jun 18 19:51:00 2006] MODIFY_CNF 1070 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1070 BEGIN : [Sun Jun 18 19:51:00 2006] CMD : minisat /tmp/csp2sat13764.cnf /tmp/csp2sat13764.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 230143 651045 | 76714 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 5 (10 /sec) decisions : 46 (96 /sec) propagations : 56980 (118708 /sec) conflict literals : 32 (13.51 % deleted) Memory used : 16.73 MB CPU time : 0.48 s SATISFIABLE VERIFY_CNF 1070 END : (1 seconds) [Sun Jun 18 19:51:01 2006] VERIFY_CNF 1070 CPU : 0.56 = 0 + 0 + 0.5 + 0.06 # RESULT : makespan 1070 SATISFIABLE SHOW_RESULT 1070 BEGIN : [Sun Jun 18 19:51:01 2006] # ASSIGN : makespan 1070 # ASSIGN : s_0_0 1049 # ASSIGN : s_0_1 415 # ASSIGN : s_0_2 661 # ASSIGN : s_0_3 660 # ASSIGN : s_0_4 81 # ASSIGN : s_1_0 442 # ASSIGN : s_1_1 184 # ASSIGN : s_1_2 52 # ASSIGN : s_1_3 764 # ASSIGN : s_1_4 415 # ASSIGN : s_2_0 854 # ASSIGN : s_2_1 44 # ASSIGN : s_2_2 1068 # ASSIGN : s_2_3 223 # ASSIGN : s_2_4 511 # ASSIGN : s_3_0 746 # ASSIGN : s_3_1 928 # ASSIGN : s_3_2 282 # ASSIGN : s_3_3 24 # ASSIGN : s_3_4 856 # ASSIGN : s_4_0 70 # ASSIGN : s_4_1 738 # ASSIGN : s_4_2 4 # ASSIGN : s_4_3 494 # ASSIGN : s_4_4 946 SHOW_RESULT 1070 END : 1070 (0 seconds) [Sun Jun 18 19:51:01 2006] SHOW_RESULT 1070 CPU : 0.0599999999999989 = 0.0499999999999989 + 0.01 + 0 + 0 # BOUND : makespan 1000 1070 MODIFY_CNF 1035 BEGIN : [Sun Jun 18 19:51:01 2006] MODIFY_CNF 1035 END : 6777008 bytes (0 seconds) [Sun Jun 18 19:51:01 2006] MODIFY_CNF 1035 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1035 BEGIN : [Sun Jun 18 19:51:01 2006] CMD : minisat /tmp/csp2sat13764.cnf /tmp/csp2sat13764.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 223143 630045 | 74381 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (4 /sec) decisions : 34 (74 /sec) propagations : 48465 (105359 /sec) conflict literals : 17 (15.00 % deleted) Memory used : 16.73 MB CPU time : 0.46 s SATISFIABLE VERIFY_CNF 1035 END : (1 seconds) [Sun Jun 18 19:51:02 2006] VERIFY_CNF 1035 CPU : 0.5 = 0 + 0 + 0.48 + 0.02 # RESULT : makespan 1035 SATISFIABLE SHOW_RESULT 1035 BEGIN : [Sun Jun 18 19:51:02 2006] # ASSIGN : makespan 1035 # ASSIGN : s_0_0 1014 # ASSIGN : s_0_1 769 # ASSIGN : s_0_2 381 # ASSIGN : s_0_3 4 # ASSIGN : s_0_4 5 # ASSIGN : s_1_0 597 # ASSIGN : s_1_1 366 # ASSIGN : s_1_2 901 # ASSIGN : s_1_3 33 # ASSIGN : s_1_4 339 # ASSIGN : s_2_0 29 # ASSIGN : s_2_1 226 # ASSIGN : s_2_2 1033 # ASSIGN : s_2_3 762 # ASSIGN : s_2_4 419 # ASSIGN : s_3_0 906 # ASSIGN : s_3_1 627 # ASSIGN : s_3_2 2 # ASSIGN : s_3_3 397 # ASSIGN : s_3_4 834 # ASSIGN : s_4_0 224 # ASSIGN : s_4_1 34 # ASSIGN : s_4_2 853 # ASSIGN : s_4_3 596 # ASSIGN : s_4_4 911 SHOW_RESULT 1035 END : 1035 (0 seconds) [Sun Jun 18 19:51:02 2006] SHOW_RESULT 1035 CPU : 0.0600000000000005 = 0.0600000000000005 + 0 + 0 + 0 # BOUND : makespan 1000 1035 MODIFY_CNF 1017 BEGIN : [Sun Jun 18 19:51:02 2006] MODIFY_CNF 1017 END : 6777008 bytes (0 seconds) [Sun Jun 18 19:51:02 2006] MODIFY_CNF 1017 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1017 BEGIN : [Sun Jun 18 19:51:02 2006] CMD : minisat /tmp/csp2sat13764.cnf /tmp/csp2sat13764.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 219543 619245 | 73181 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 18 (38 /sec) decisions : 62 (132 /sec) propagations : 107107 (227887 /sec) conflict literals : 226 (15.36 % deleted) Memory used : 16.73 MB CPU time : 0.47 s SATISFIABLE VERIFY_CNF 1017 END : (0 seconds) [Sun Jun 18 19:51:02 2006] VERIFY_CNF 1017 CPU : 0.55 = 0 + 0 + 0.49 + 0.06 # RESULT : makespan 1017 SATISFIABLE SHOW_RESULT 1017 BEGIN : [Sun Jun 18 19:51:02 2006] # ASSIGN : makespan 1017 # ASSIGN : s_0_0 996 # ASSIGN : s_0_1 416 # ASSIGN : s_0_2 28 # ASSIGN : s_0_3 27 # ASSIGN : s_0_4 662 # ASSIGN : s_1_0 579 # ASSIGN : s_1_1 42 # ASSIGN : s_1_2 883 # ASSIGN : s_1_3 273 # ASSIGN : s_1_4 14 # ASSIGN : s_2_0 384 # ASSIGN : s_2_1 875 # ASSIGN : s_2_2 1015 # ASSIGN : s_2_3 580 # ASSIGN : s_2_4 41 # ASSIGN : s_3_0 888 # ASSIGN : s_3_1 274 # ASSIGN : s_3_2 504 # ASSIGN : s_3_3 74 # ASSIGN : s_3_4 432 # ASSIGN : s_4_0 12 # ASSIGN : s_4_1 661 # ASSIGN : s_4_2 456 # ASSIGN : s_4_3 851 # ASSIGN : s_4_4 537 SHOW_RESULT 1017 END : 1017 (0 seconds) [Sun Jun 18 19:51:02 2006] SHOW_RESULT 1017 CPU : 0.0600000000000005 = 0.0600000000000005 + 0 + 0 + 0 # BOUND : makespan 1000 1017 MODIFY_CNF 1008 BEGIN : [Sun Jun 18 19:51:02 2006] MODIFY_CNF 1008 END : 6777008 bytes (0 seconds) [Sun Jun 18 19:51:02 2006] MODIFY_CNF 1008 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1008 BEGIN : [Sun Jun 18 19:51:02 2006] CMD : minisat /tmp/csp2sat13764.cnf /tmp/csp2sat13764.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 217743 613845 | 72581 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 13 (28 /sec) decisions : 42 (89 /sec) propagations : 103152 (219472 /sec) conflict literals : 127 (25.29 % deleted) Memory used : 16.73 MB CPU time : 0.47 s SATISFIABLE VERIFY_CNF 1008 END : (1 seconds) [Sun Jun 18 19:51:03 2006] VERIFY_CNF 1008 CPU : 0.55 = 0 + 0 + 0.5 + 0.05 # RESULT : makespan 1008 SATISFIABLE SHOW_RESULT 1008 BEGIN : [Sun Jun 18 19:51:03 2006] # ASSIGN : makespan 1008 # ASSIGN : s_0_0 987 # ASSIGN : s_0_1 407 # ASSIGN : s_0_2 19 # ASSIGN : s_0_3 18 # ASSIGN : s_0_4 653 # ASSIGN : s_1_0 572 # ASSIGN : s_1_1 34 # ASSIGN : s_1_2 876 # ASSIGN : s_1_3 265 # ASSIGN : s_1_4 6 # ASSIGN : s_2_0 376 # ASSIGN : s_2_1 868 # ASSIGN : s_2_2 866 # ASSIGN : s_2_3 571 # ASSIGN : s_2_4 33 # ASSIGN : s_3_0 879 # ASSIGN : s_3_1 265 # ASSIGN : s_3_2 487 # ASSIGN : s_3_3 66 # ASSIGN : s_3_4 415 # ASSIGN : s_4_0 4 # ASSIGN : s_4_1 652 # ASSIGN : s_4_2 439 # ASSIGN : s_4_3 842 # ASSIGN : s_4_4 528 SHOW_RESULT 1008 END : 1008 (0 seconds) [Sun Jun 18 19:51:03 2006] SHOW_RESULT 1008 CPU : 0.0600000000000005 = 0.0600000000000005 + 0 + 0 + 0 # BOUND : makespan 1000 1008 MODIFY_CNF 1004 BEGIN : [Sun Jun 18 19:51:03 2006] MODIFY_CNF 1004 END : 6777007 bytes (0 seconds) [Sun Jun 18 19:51:03 2006] MODIFY_CNF 1004 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1004 BEGIN : [Sun Jun 18 19:51:03 2006] CMD : minisat /tmp/csp2sat13764.cnf /tmp/csp2sat13764.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 216943 611445 | 72314 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 13 (27 /sec) decisions : 44 (92 /sec) propagations : 90482 (188504 /sec) conflict literals : 105 (18.60 % deleted) Memory used : 16.73 MB CPU time : 0.48 s SATISFIABLE VERIFY_CNF 1004 END : (0 seconds) [Sun Jun 18 19:51:03 2006] VERIFY_CNF 1004 CPU : 0.56 = 0 + 0 + 0.49 + 0.07 # RESULT : makespan 1004 SATISFIABLE SHOW_RESULT 1004 BEGIN : [Sun Jun 18 19:51:03 2006] # ASSIGN : makespan 1004 # ASSIGN : s_0_0 983 # ASSIGN : s_0_1 403 # ASSIGN : s_0_2 15 # ASSIGN : s_0_3 14 # ASSIGN : s_0_4 649 # ASSIGN : s_1_0 568 # ASSIGN : s_1_1 30 # ASSIGN : s_1_2 872 # ASSIGN : s_1_3 261 # ASSIGN : s_1_4 2 # ASSIGN : s_2_0 372 # ASSIGN : s_2_1 864 # ASSIGN : s_2_2 862 # ASSIGN : s_2_3 567 # ASSIGN : s_2_4 29 # ASSIGN : s_3_0 875 # ASSIGN : s_3_1 261 # ASSIGN : s_3_2 483 # ASSIGN : s_3_3 62 # ASSIGN : s_3_4 411 # ASSIGN : s_4_0 0 # ASSIGN : s_4_1 648 # ASSIGN : s_4_2 435 # ASSIGN : s_4_3 838 # ASSIGN : s_4_4 524 SHOW_RESULT 1004 END : 1004 (0 seconds) [Sun Jun 18 19:51:03 2006] SHOW_RESULT 1004 CPU : 0.0499999999999989 = 0.0499999999999989 + 0 + 0 + 0 # BOUND : makespan 1000 1004 MODIFY_CNF 1002 BEGIN : [Sun Jun 18 19:51:03 2006] MODIFY_CNF 1002 END : 6777007 bytes (0 seconds) [Sun Jun 18 19:51:03 2006] MODIFY_CNF 1002 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1002 BEGIN : [Sun Jun 18 19:51:03 2006] CMD : minisat /tmp/csp2sat13764.cnf /tmp/csp2sat13764.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 216543 610245 | 72181 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 52 (104 /sec) decisions : 65 (130 /sec) propagations : 228341 (456682 /sec) conflict literals : 212 (33.12 % deleted) Memory used : 16.54 MB CPU time : 0.5 s UNSATISFIABLE VERIFY_CNF 1002 END : (1 seconds) [Sun Jun 18 19:51:04 2006] VERIFY_CNF 1002 CPU : 0.6 = 0 + 0 + 0.5 + 0.1 # RESULT : makespan 1002 UNSATISFIABLE # BOUND : makespan 1003 1004 MODIFY_CNF 1003 BEGIN : [Sun Jun 18 19:51:04 2006] MODIFY_CNF 1003 END : 6777007 bytes (0 seconds) [Sun Jun 18 19:51:04 2006] MODIFY_CNF 1003 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1003 BEGIN : [Sun Jun 18 19:51:04 2006] CMD : minisat /tmp/csp2sat13764.cnf /tmp/csp2sat13764.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 216743 610845 | 72247 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 49 (84 /sec) decisions : 59 (102 /sec) propagations : 236005 (406905 /sec) conflict literals : 210 (38.60 % deleted) Memory used : 16.55 MB CPU time : 0.58 s UNSATISFIABLE VERIFY_CNF 1003 END : (1 seconds) [Sun Jun 18 19:51:05 2006] VERIFY_CNF 1003 CPU : 0.600000000000001 = 0 + 0 + 0.580000000000001 + 0.02 # RESULT : makespan 1003 UNSATISFIABLE # BOUND : makespan 1004 1004 MAIN END : (18 seconds) [Sun Jun 18 19:51:05 2006] MAIN CPU : 18.01 = 12.99 + 0.1 + 4.44 + 0.48