# TIMEOUT 18000 MAIN BEGIN : [Sun Jun 18 19:49:52 2006] READ BEGIN : csp/j5-per0-1.csp [Sun Jun 18 19:49:52 2006] READ END : csp/j5-per0-1.csp (0 seconds) [Sun Jun 18 19:49:52 2006] READ CPU : 0.23 = 0.21 + 0.02 + 0 + 0 # BOUND : makespan 1000 2285 GENERATE_CNF 2285 BEGIN : [Sun Jun 18 19:49:52 2006] GENERATE_CNF 2285 END : 58687 variables 508163 clauses 10552422 bytes (19 seconds) [Sun Jun 18 19:50:11 2006] GENERATE_CNF 2285 CPU : 18.98 = 18.94 + 0.04 + 0 + 0 MODIFY_CNF 1642 BEGIN : [Sun Jun 18 19:50:11 2006] MODIFY_CNF 1642 END : 10552428 bytes (0 seconds) [Sun Jun 18 19:50:11 2006] MODIFY_CNF 1642 CPU : 0.0100000000000016 = 0.0100000000000016 + 0 + 0 + 0 VERIFY_CNF 1642 BEGIN : [Sun Jun 18 19:50:11 2006] CMD : minisat /tmp/csp2sat13726.cnf /tmp/csp2sat13726.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 379183 1079445 | 126394 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 3 (5 /sec) decisions : 94 (142 /sec) propagations : 73988 (112103 /sec) conflict literals : 22 (12.00 % deleted) Memory used : 24.20 MB CPU time : 0.66 s SATISFIABLE VERIFY_CNF 1642 END : (1 seconds) [Sun Jun 18 19:50:12 2006] VERIFY_CNF 1642 CPU : 0.73 = 0 + 0 + 0.69 + 0.04 # RESULT : makespan 1642 SATISFIABLE SHOW_RESULT 1642 BEGIN : [Sun Jun 18 19:50:12 2006] # ASSIGN : makespan 1642 # ASSIGN : s_0_0 35 # ASSIGN : s_0_1 36 # ASSIGN : s_0_2 97 # ASSIGN : s_0_3 642 # ASSIGN : s_0_4 578 # ASSIGN : s_1_0 915 # ASSIGN : s_1_1 305 # ASSIGN : s_1_2 367 # ASSIGN : s_1_3 1246 # ASSIGN : s_1_4 704 # ASSIGN : s_2_0 247 # ASSIGN : s_2_1 628 # ASSIGN : s_2_2 649 # ASSIGN : s_2_3 1482 # ASSIGN : s_2_4 793 # ASSIGN : s_3_0 437 # ASSIGN : s_3_1 675 # ASSIGN : s_3_2 660 # ASSIGN : s_3_3 1594 # ASSIGN : s_3_4 1459 # ASSIGN : s_4_0 502 # ASSIGN : s_4_1 1477 # ASSIGN : s_4_2 1055 # ASSIGN : s_4_3 1640 # ASSIGN : s_4_4 1549 SHOW_RESULT 1642 END : 1642 (0 seconds) [Sun Jun 18 19:50:12 2006] SHOW_RESULT 1642 CPU : 0.0899999999999999 = 0.0899999999999999 + 0 + 0 + 0 # BOUND : makespan 1000 1642 MODIFY_CNF 1321 BEGIN : [Sun Jun 18 19:50:12 2006] MODIFY_CNF 1321 END : 10552428 bytes (0 seconds) [Sun Jun 18 19:50:12 2006] MODIFY_CNF 1321 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1321 BEGIN : [Sun Jun 18 19:50:12 2006] CMD : minisat /tmp/csp2sat13726.cnf /tmp/csp2sat13726.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 314983 886845 | 104994 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 1 (1 /sec) decisions : 56 (81 /sec) propagations : 64310 (93203 /sec) conflict literals : 12 (20.00 % deleted) Memory used : 24.23 MB CPU time : 0.69 s SATISFIABLE VERIFY_CNF 1321 END : (1 seconds) [Sun Jun 18 19:50:13 2006] VERIFY_CNF 1321 CPU : 0.76 = 0 + 0 + 0.72 + 0.04 # RESULT : makespan 1321 SATISFIABLE SHOW_RESULT 1321 BEGIN : [Sun Jun 18 19:50:13 2006] # ASSIGN : makespan 1321 # ASSIGN : s_0_0 70 # ASSIGN : s_0_1 105 # ASSIGN : s_0_2 1051 # ASSIGN : s_0_3 230 # ASSIGN : s_0_4 166 # ASSIGN : s_1_0 412 # ASSIGN : s_1_1 1259 # ASSIGN : s_1_2 0 # ASSIGN : s_1_3 834 # ASSIGN : s_1_4 315 # ASSIGN : s_2_0 71 # ASSIGN : s_2_1 261 # ASSIGN : s_2_2 282 # ASSIGN : s_2_3 1070 # ASSIGN : s_2_4 404 # ASSIGN : s_3_0 1256 # ASSIGN : s_3_1 308 # ASSIGN : s_3_2 293 # ASSIGN : s_3_3 1182 # ASSIGN : s_3_4 1092 # ASSIGN : s_4_0 743 # ASSIGN : s_4_1 1156 # ASSIGN : s_4_2 321 # ASSIGN : s_4_3 1228 # ASSIGN : s_4_4 1230 SHOW_RESULT 1321 END : 1321 (0 seconds) [Sun Jun 18 19:50:13 2006] SHOW_RESULT 1321 CPU : 0.0999999999999999 = 0.0899999999999999 + 0.01 + 0 + 0 # BOUND : makespan 1000 1321 MODIFY_CNF 1160 BEGIN : [Sun Jun 18 19:50:13 2006] MODIFY_CNF 1160 END : 10552428 bytes (0 seconds) [Sun Jun 18 19:50:13 2006] MODIFY_CNF 1160 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1160 BEGIN : [Sun Jun 18 19:50:13 2006] CMD : minisat /tmp/csp2sat13726.cnf /tmp/csp2sat13726.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 282783 790245 | 94261 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (3 /sec) decisions : 58 (85 /sec) propagations : 67928 (99894 /sec) conflict literals : 18 (0.00 % deleted) Memory used : 24.23 MB CPU time : 0.68 s SATISFIABLE VERIFY_CNF 1160 END : (1 seconds) [Sun Jun 18 19:50:14 2006] VERIFY_CNF 1160 CPU : 0.78 = 0 + 0 + 0.71 + 0.07 # RESULT : makespan 1160 SATISFIABLE SHOW_RESULT 1160 BEGIN : [Sun Jun 18 19:50:14 2006] # ASSIGN : makespan 1160 # ASSIGN : s_0_0 7 # ASSIGN : s_0_1 134 # ASSIGN : s_0_2 879 # ASSIGN : s_0_3 227 # ASSIGN : s_0_4 8 # ASSIGN : s_1_0 161 # ASSIGN : s_1_1 1098 # ASSIGN : s_1_2 549 # ASSIGN : s_1_3 831 # ASSIGN : s_1_4 72 # ASSIGN : s_2_0 905 # ASSIGN : s_2_1 16 # ASSIGN : s_2_2 1149 # ASSIGN : s_2_3 37 # ASSIGN : s_2_4 239 # ASSIGN : s_3_0 1095 # ASSIGN : s_3_1 195 # ASSIGN : s_3_2 55 # ASSIGN : s_3_3 149 # ASSIGN : s_3_4 979 # ASSIGN : s_4_0 492 # ASSIGN : s_4_1 995 # ASSIGN : s_4_2 70 # ASSIGN : s_4_3 1067 # ASSIGN : s_4_4 1069 SHOW_RESULT 1160 END : 1160 (0 seconds) [Sun Jun 18 19:50:14 2006] SHOW_RESULT 1160 CPU : 0.0899999999999999 = 0.0899999999999999 + 0 + 0 + 0 # BOUND : makespan 1000 1160 MODIFY_CNF 1080 BEGIN : [Sun Jun 18 19:50:14 2006] MODIFY_CNF 1080 END : 10552427 bytes (0 seconds) [Sun Jun 18 19:50:14 2006] MODIFY_CNF 1080 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1080 BEGIN : [Sun Jun 18 19:50:14 2006] CMD : minisat /tmp/csp2sat13726.cnf /tmp/csp2sat13726.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 266783 742245 | 88927 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 4 (6 /sec) decisions : 46 (68 /sec) propagations : 72153 (106107 /sec) conflict literals : 23 (4.17 % deleted) Memory used : 24.23 MB CPU time : 0.68 s SATISFIABLE VERIFY_CNF 1080 END : (1 seconds) [Sun Jun 18 19:50:15 2006] VERIFY_CNF 1080 CPU : 0.78 = 0 + 0 + 0.71 + 0.07 # RESULT : makespan 1080 SATISFIABLE SHOW_RESULT 1080 BEGIN : [Sun Jun 18 19:50:15 2006] # ASSIGN : makespan 1080 # ASSIGN : s_0_0 49 # ASSIGN : s_0_1 53 # ASSIGN : s_0_2 799 # ASSIGN : s_0_3 178 # ASSIGN : s_0_4 114 # ASSIGN : s_1_0 135 # ASSIGN : s_1_1 1018 # ASSIGN : s_1_2 500 # ASSIGN : s_1_3 782 # ASSIGN : s_1_4 25 # ASSIGN : s_2_0 879 # ASSIGN : s_2_1 32 # ASSIGN : s_2_2 1069 # ASSIGN : s_2_3 66 # ASSIGN : s_2_4 213 # ASSIGN : s_3_0 50 # ASSIGN : s_3_1 115 # ASSIGN : s_3_2 29 # ASSIGN : s_3_3 1034 # ASSIGN : s_3_4 899 # ASSIGN : s_4_0 466 # ASSIGN : s_4_1 917 # ASSIGN : s_4_2 44 # ASSIGN : s_4_3 42 # ASSIGN : s_4_4 989 SHOW_RESULT 1080 END : 1080 (0 seconds) [Sun Jun 18 19:50:15 2006] SHOW_RESULT 1080 CPU : 0.0899999999999999 = 0.0899999999999999 + 0 + 0 + 0 # BOUND : makespan 1000 1080 MODIFY_CNF 1040 BEGIN : [Sun Jun 18 19:50:15 2006] MODIFY_CNF 1040 END : 10552427 bytes (0 seconds) [Sun Jun 18 19:50:15 2006] MODIFY_CNF 1040 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1040 BEGIN : [Sun Jun 18 19:50:15 2006] CMD : minisat /tmp/csp2sat13726.cnf /tmp/csp2sat13726.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 258783 718245 | 86261 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 14 (21 /sec) decisions : 16 (24 /sec) propagations : 112000 (169697 /sec) conflict literals : 51 (19.05 % deleted) Memory used : 23.97 MB CPU time : 0.66 s UNSATISFIABLE VERIFY_CNF 1040 END : (1 seconds) [Sun Jun 18 19:50:16 2006] VERIFY_CNF 1040 CPU : 0.78 = 0 + 0 + 0.66 + 0.12 # RESULT : makespan 1040 UNSATISFIABLE # BOUND : makespan 1041 1080 MODIFY_CNF 1060 BEGIN : [Sun Jun 18 19:50:16 2006] MODIFY_CNF 1060 END : 10552427 bytes (0 seconds) [Sun Jun 18 19:50:16 2006] MODIFY_CNF 1060 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1060 BEGIN : [Sun Jun 18 19:50:16 2006] CMD : minisat /tmp/csp2sat13726.cnf /tmp/csp2sat13726.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 262783 730245 | 87594 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (3 /sec) decisions : 36 (47 /sec) propagations : 66372 (86197 /sec) conflict literals : 9 (0.00 % deleted) Memory used : 24.23 MB CPU time : 0.77 s SATISFIABLE VERIFY_CNF 1060 END : (1 seconds) [Sun Jun 18 19:50:17 2006] VERIFY_CNF 1060 CPU : 0.87 = 0 + 0 + 0.8 + 0.07 # RESULT : makespan 1060 SATISFIABLE SHOW_RESULT 1060 BEGIN : [Sun Jun 18 19:50:17 2006] # ASSIGN : makespan 1060 # ASSIGN : s_0_0 29 # ASSIGN : s_0_1 33 # ASSIGN : s_0_2 779 # ASSIGN : s_0_3 158 # ASSIGN : s_0_4 94 # ASSIGN : s_1_0 115 # ASSIGN : s_1_1 998 # ASSIGN : s_1_2 480 # ASSIGN : s_1_3 762 # ASSIGN : s_1_4 5 # ASSIGN : s_2_0 859 # ASSIGN : s_2_1 12 # ASSIGN : s_2_2 1049 # ASSIGN : s_2_3 46 # ASSIGN : s_2_4 193 # ASSIGN : s_3_0 30 # ASSIGN : s_3_1 95 # ASSIGN : s_3_2 9 # ASSIGN : s_3_3 1014 # ASSIGN : s_3_4 879 # ASSIGN : s_4_0 446 # ASSIGN : s_4_1 897 # ASSIGN : s_4_2 24 # ASSIGN : s_4_3 22 # ASSIGN : s_4_4 969 SHOW_RESULT 1060 END : 1060 (0 seconds) [Sun Jun 18 19:50:17 2006] SHOW_RESULT 1060 CPU : 0.0899999999999999 = 0.0899999999999999 + 0 + 0 + 0 # BOUND : makespan 1041 1060 MODIFY_CNF 1050 BEGIN : [Sun Jun 18 19:50:17 2006] MODIFY_CNF 1050 END : 10552427 bytes (0 seconds) [Sun Jun 18 19:50:17 2006] MODIFY_CNF 1050 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1050 BEGIN : [Sun Jun 18 19:50:17 2006] CMD : minisat /tmp/csp2sat13726.cnf /tmp/csp2sat13726.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 260783 724245 | 86927 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 14 (18 /sec) decisions : 16 (21 /sec) propagations : 119755 (155526 /sec) conflict literals : 52 (17.46 % deleted) Memory used : 23.97 MB CPU time : 0.77 s UNSATISFIABLE VERIFY_CNF 1050 END : (0 seconds) [Sun Jun 18 19:50:17 2006] VERIFY_CNF 1050 CPU : 0.82 = 0 + 0 + 0.77 + 0.05 # RESULT : makespan 1050 UNSATISFIABLE # BOUND : makespan 1051 1060 MODIFY_CNF 1055 BEGIN : [Sun Jun 18 19:50:17 2006] MODIFY_CNF 1055 END : 10552427 bytes (0 seconds) [Sun Jun 18 19:50:17 2006] MODIFY_CNF 1055 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1055 BEGIN : [Sun Jun 18 19:50:17 2006] CMD : minisat /tmp/csp2sat13726.cnf /tmp/csp2sat13726.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 261783 727245 | 87261 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (3 /sec) decisions : 34 (50 /sec) propagations : 66372 (97606 /sec) conflict literals : 9 (0.00 % deleted) Memory used : 24.23 MB CPU time : 0.68 s SATISFIABLE VERIFY_CNF 1055 END : (1 seconds) [Sun Jun 18 19:50:18 2006] VERIFY_CNF 1055 CPU : 0.82 = 0 + 0 + 0.71 + 0.11 # RESULT : makespan 1055 SATISFIABLE SHOW_RESULT 1055 BEGIN : [Sun Jun 18 19:50:18 2006] # ASSIGN : makespan 1055 # ASSIGN : s_0_0 24 # ASSIGN : s_0_1 28 # ASSIGN : s_0_2 774 # ASSIGN : s_0_3 153 # ASSIGN : s_0_4 89 # ASSIGN : s_1_0 110 # ASSIGN : s_1_1 993 # ASSIGN : s_1_2 475 # ASSIGN : s_1_3 757 # ASSIGN : s_1_4 0 # ASSIGN : s_2_0 854 # ASSIGN : s_2_1 7 # ASSIGN : s_2_2 1044 # ASSIGN : s_2_3 41 # ASSIGN : s_2_4 188 # ASSIGN : s_3_0 25 # ASSIGN : s_3_1 90 # ASSIGN : s_3_2 4 # ASSIGN : s_3_3 1009 # ASSIGN : s_3_4 874 # ASSIGN : s_4_0 441 # ASSIGN : s_4_1 892 # ASSIGN : s_4_2 19 # ASSIGN : s_4_3 17 # ASSIGN : s_4_4 964 SHOW_RESULT 1055 END : 1055 (0 seconds) [Sun Jun 18 19:50:18 2006] SHOW_RESULT 1055 CPU : 0.0899999999999999 = 0.0899999999999999 + 0 + 0 + 0 # BOUND : makespan 1051 1055 MODIFY_CNF 1053 BEGIN : [Sun Jun 18 19:50:18 2006] MODIFY_CNF 1053 END : 10552427 bytes (0 seconds) [Sun Jun 18 19:50:18 2006] MODIFY_CNF 1053 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1053 BEGIN : [Sun Jun 18 19:50:18 2006] CMD : minisat /tmp/csp2sat13726.cnf /tmp/csp2sat13726.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 261383 726045 | 87127 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 14 (19 /sec) decisions : 16 (22 /sec) propagations : 118408 (162203 /sec) conflict literals : 52 (18.75 % deleted) Memory used : 23.97 MB CPU time : 0.73 s UNSATISFIABLE VERIFY_CNF 1053 END : (1 seconds) [Sun Jun 18 19:50:19 2006] VERIFY_CNF 1053 CPU : 0.79 = 0 + 0 + 0.73 + 0.0600000000000001 # RESULT : makespan 1053 UNSATISFIABLE # BOUND : makespan 1054 1055 MODIFY_CNF 1054 BEGIN : [Sun Jun 18 19:50:19 2006] MODIFY_CNF 1054 END : 10552427 bytes (0 seconds) [Sun Jun 18 19:50:19 2006] MODIFY_CNF 1054 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1054 BEGIN : [Sun Jun 18 19:50:19 2006] CMD : minisat /tmp/csp2sat13726.cnf /tmp/csp2sat13726.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 261583 726645 | 87194 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 6 (9 /sec) decisions : 58 (83 /sec) propagations : 83991 (119987 /sec) conflict literals : 32 (5.88 % deleted) Memory used : 24.23 MB CPU time : 0.7 s SATISFIABLE VERIFY_CNF 1054 END : (1 seconds) [Sun Jun 18 19:50:20 2006] VERIFY_CNF 1054 CPU : 0.79 = 0 + 0 + 0.73 + 0.0599999999999999 # RESULT : makespan 1054 SATISFIABLE SHOW_RESULT 1054 BEGIN : [Sun Jun 18 19:50:20 2006] # ASSIGN : makespan 1054 # ASSIGN : s_0_0 1053 # ASSIGN : s_0_1 64 # ASSIGN : s_0_2 769 # ASSIGN : s_0_3 125 # ASSIGN : s_0_4 0 # ASSIGN : s_1_0 116 # ASSIGN : s_1_1 2 # ASSIGN : s_1_2 447 # ASSIGN : s_1_3 729 # ASSIGN : s_1_4 965 # ASSIGN : s_2_0 863 # ASSIGN : s_2_1 175 # ASSIGN : s_2_2 2 # ASSIGN : s_2_3 13 # ASSIGN : s_2_4 197 # ASSIGN : s_3_0 41 # ASSIGN : s_3_1 196 # ASSIGN : s_3_2 1039 # ASSIGN : s_3_3 993 # ASSIGN : s_3_4 106 # ASSIGN : s_4_0 450 # ASSIGN : s_4_1 980 # ASSIGN : s_4_2 25 # ASSIGN : s_4_3 1052 # ASSIGN : s_4_4 874 SHOW_RESULT 1054 END : 1054 (0 seconds) [Sun Jun 18 19:50:20 2006] SHOW_RESULT 1054 CPU : 0.0900000000000018 = 0.0800000000000018 + 0.01 + 0 + 0 # BOUND : makespan 1054 1054 MAIN END : (28 seconds) [Sun Jun 18 19:50:20 2006] MAIN CPU : 27.79 = 19.79 + 0.08 + 7.23 + 0.69