# TIMEOUT 18000 MAIN BEGIN : [Sun Jun 18 19:51:57 2006] READ BEGIN : csp/j5-per20-1.csp [Sun Jun 18 19:51:57 2006] READ END : csp/j5-per20-1.csp (0 seconds) [Sun Jun 18 19:51:57 2006] READ CPU : 0.23 = 0.23 + 0 + 0 + 0 # BOUND : makespan 1000 2205 GENERATE_CNF 2205 BEGIN : [Sun Jun 18 19:51:57 2006] GENERATE_CNF 2205 END : 56607 variables 492707 clauses 10230832 bytes (18 seconds) [Sun Jun 18 19:52:15 2006] GENERATE_CNF 2205 CPU : 17.77 = 17.71 + 0.06 + 0 + 0 MODIFY_CNF 1602 BEGIN : [Sun Jun 18 19:52:15 2006] MODIFY_CNF 1602 END : 10230838 bytes (0 seconds) [Sun Jun 18 19:52:15 2006] MODIFY_CNF 1602 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1602 BEGIN : [Sun Jun 18 19:52:15 2006] CMD : minisat /tmp/csp2sat13822.cnf /tmp/csp2sat13822.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 371727 1059157 | 123909 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 86 (134 /sec) propagations : 56607 (88448 /sec) conflict literals : 0 ( nan % deleted) Memory used : 23.55 MB CPU time : 0.64 s SATISFIABLE VERIFY_CNF 1602 END : (1 seconds) [Sun Jun 18 19:52:16 2006] VERIFY_CNF 1602 CPU : 0.72 = 0 + 0 + 0.67 + 0.05 # RESULT : makespan 1602 SATISFIABLE SHOW_RESULT 1602 BEGIN : [Sun Jun 18 19:52:16 2006] # ASSIGN : makespan 1602 # ASSIGN : s_0_0 111 # ASSIGN : s_0_1 224 # ASSIGN : s_0_2 26 # ASSIGN : s_0_3 553 # ASSIGN : s_0_4 544 # ASSIGN : s_1_0 240 # ASSIGN : s_1_1 797 # ASSIGN : s_1_2 179 # ASSIGN : s_1_3 995 # ASSIGN : s_1_4 577 # ASSIGN : s_2_0 635 # ASSIGN : s_2_1 1162 # ASSIGN : s_2_2 432 # ASSIGN : s_2_3 1223 # ASSIGN : s_2_4 647 # ASSIGN : s_3_0 684 # ASSIGN : s_3_1 1281 # ASSIGN : s_3_2 729 # ASSIGN : s_3_3 1330 # ASSIGN : s_3_4 1396 # ASSIGN : s_4_0 790 # ASSIGN : s_4_1 1283 # ASSIGN : s_4_2 1566 # ASSIGN : s_4_3 1576 # ASSIGN : s_4_4 1580 SHOW_RESULT 1602 END : 1602 (0 seconds) [Sun Jun 18 19:52:16 2006] SHOW_RESULT 1602 CPU : 0.0899999999999983 = 0.0799999999999983 + 0.01 + 0 + 0 # BOUND : makespan 1000 1602 MODIFY_CNF 1301 BEGIN : [Sun Jun 18 19:52:16 2006] MODIFY_CNF 1301 END : 10230838 bytes (0 seconds) [Sun Jun 18 19:52:16 2006] MODIFY_CNF 1301 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1301 BEGIN : [Sun Jun 18 19:52:16 2006] CMD : minisat /tmp/csp2sat13822.cnf /tmp/csp2sat13822.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 311527 878557 | 103842 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 3 (5 /sec) decisions : 84 (129 /sec) propagations : 70665 (108715 /sec) conflict literals : 29 (19.44 % deleted) Memory used : 23.55 MB CPU time : 0.65 s SATISFIABLE VERIFY_CNF 1301 END : (0 seconds) [Sun Jun 18 19:52:16 2006] VERIFY_CNF 1301 CPU : 0.74 = 0 + 0 + 0.68 + 0.06 # RESULT : makespan 1301 SATISFIABLE SHOW_RESULT 1301 BEGIN : [Sun Jun 18 19:52:16 2006] # ASSIGN : makespan 1301 # ASSIGN : s_0_0 1188 # ASSIGN : s_0_1 868 # ASSIGN : s_0_2 146 # ASSIGN : s_0_3 426 # ASSIGN : s_0_4 417 # ASSIGN : s_1_0 559 # ASSIGN : s_1_1 33 # ASSIGN : s_1_2 231 # ASSIGN : s_1_3 896 # ASSIGN : s_1_4 462 # ASSIGN : s_2_0 1112 # ASSIGN : s_2_1 231 # ASSIGN : s_2_2 292 # ASSIGN : s_2_3 1124 # ASSIGN : s_2_4 532 # ASSIGN : s_3_0 21 # ASSIGN : s_3_1 493 # ASSIGN : s_3_2 495 # ASSIGN : s_3_3 1231 # ASSIGN : s_3_4 1047 # ASSIGN : s_4_0 66 # ASSIGN : s_4_1 585 # ASSIGN : s_4_2 1287 # ASSIGN : s_4_3 1297 # ASSIGN : s_4_4 1265 SHOW_RESULT 1301 END : 1301 (1 seconds) [Sun Jun 18 19:52:17 2006] SHOW_RESULT 1301 CPU : 0.0899999999999999 = 0.0899999999999999 + 0 + 0 + 0 # BOUND : makespan 1000 1301 MODIFY_CNF 1150 BEGIN : [Sun Jun 18 19:52:17 2006] MODIFY_CNF 1150 END : 10230838 bytes (0 seconds) [Sun Jun 18 19:52:17 2006] MODIFY_CNF 1150 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1150 BEGIN : [Sun Jun 18 19:52:17 2006] CMD : minisat /tmp/csp2sat13822.cnf /tmp/csp2sat13822.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 281327 787957 | 93775 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 1 (2 /sec) decisions : 69 (106 /sec) propagations : 65798 (101228 /sec) conflict literals : 3 (0.00 % deleted) Memory used : 23.55 MB CPU time : 0.65 s SATISFIABLE VERIFY_CNF 1150 END : (0 seconds) [Sun Jun 18 19:52:17 2006] VERIFY_CNF 1150 CPU : 0.74 = 0 + 0 + 0.69 + 0.05 # RESULT : makespan 1150 SATISFIABLE SHOW_RESULT 1150 BEGIN : [Sun Jun 18 19:52:17 2006] # ASSIGN : makespan 1150 # ASSIGN : s_0_0 1037 # ASSIGN : s_0_1 453 # ASSIGN : s_0_2 952 # ASSIGN : s_0_3 11 # ASSIGN : s_0_4 2 # ASSIGN : s_1_0 700 # ASSIGN : s_1_1 89 # ASSIGN : s_1_2 28 # ASSIGN : s_1_3 472 # ASSIGN : s_1_4 287 # ASSIGN : s_2_0 105 # ASSIGN : s_2_1 1089 # ASSIGN : s_2_2 117 # ASSIGN : s_2_3 951 # ASSIGN : s_2_4 357 # ASSIGN : s_3_0 162 # ASSIGN : s_3_1 1056 # ASSIGN : s_3_2 320 # ASSIGN : s_3_3 1058 # ASSIGN : s_3_4 872 # ASSIGN : s_4_0 207 # ASSIGN : s_4_1 773 # ASSIGN : s_4_2 1114 # ASSIGN : s_4_3 1124 # ASSIGN : s_4_4 1128 SHOW_RESULT 1150 END : 1150 (0 seconds) [Sun Jun 18 19:52:17 2006] SHOW_RESULT 1150 CPU : 0.0899999999999999 = 0.0899999999999999 + 0 + 0 + 0 # BOUND : makespan 1000 1150 MODIFY_CNF 1075 BEGIN : [Sun Jun 18 19:52:17 2006] MODIFY_CNF 1075 END : 10230837 bytes (0 seconds) [Sun Jun 18 19:52:17 2006] MODIFY_CNF 1075 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1075 BEGIN : [Sun Jun 18 19:52:17 2006] CMD : minisat /tmp/csp2sat13822.cnf /tmp/csp2sat13822.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 266327 742957 | 88775 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 48 (75 /sec) propagations : 56607 (88448 /sec) conflict literals : 0 ( nan % deleted) Memory used : 23.55 MB CPU time : 0.64 s SATISFIABLE VERIFY_CNF 1075 END : (1 seconds) [Sun Jun 18 19:52:18 2006] VERIFY_CNF 1075 CPU : 0.75 = 0 + 0 + 0.67 + 0.08 # RESULT : makespan 1075 SATISFIABLE SHOW_RESULT 1075 BEGIN : [Sun Jun 18 19:52:18 2006] # ASSIGN : makespan 1075 # ASSIGN : s_0_0 962 # ASSIGN : s_0_1 496 # ASSIGN : s_0_2 877 # ASSIGN : s_0_3 54 # ASSIGN : s_0_4 45 # ASSIGN : s_1_0 132 # ASSIGN : s_1_1 816 # ASSIGN : s_1_2 1 # ASSIGN : s_1_3 588 # ASSIGN : s_1_4 62 # ASSIGN : s_2_0 54 # ASSIGN : s_2_1 1014 # ASSIGN : s_2_2 66 # ASSIGN : s_2_3 898 # ASSIGN : s_2_4 306 # ASSIGN : s_3_0 87 # ASSIGN : s_3_1 184 # ASSIGN : s_3_2 269 # ASSIGN : s_3_3 1005 # ASSIGN : s_3_4 821 # ASSIGN : s_4_0 469 # ASSIGN : s_4_1 186 # ASSIGN : s_4_2 1039 # ASSIGN : s_4_3 1071 # ASSIGN : s_4_4 1049 SHOW_RESULT 1075 END : 1075 (0 seconds) [Sun Jun 18 19:52:18 2006] SHOW_RESULT 1075 CPU : 0.0899999999999999 = 0.0899999999999999 + 0 + 0 + 0 # BOUND : makespan 1000 1075 MODIFY_CNF 1037 BEGIN : [Sun Jun 18 19:52:18 2006] MODIFY_CNF 1037 END : 10230837 bytes (0 seconds) [Sun Jun 18 19:52:18 2006] MODIFY_CNF 1037 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1037 BEGIN : [Sun Jun 18 19:52:18 2006] CMD : minisat /tmp/csp2sat13822.cnf /tmp/csp2sat13822.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 258727 720157 | 86242 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 1 (2 /sec) decisions : 41 (68 /sec) propagations : 56937 (94895 /sec) conflict literals : 5 (16.67 % deleted) Memory used : 23.55 MB CPU time : 0.6 s SATISFIABLE VERIFY_CNF 1037 END : (1 seconds) [Sun Jun 18 19:52:19 2006] VERIFY_CNF 1037 CPU : 0.74 = 0 + 0 + 0.63 + 0.11 # RESULT : makespan 1037 SATISFIABLE SHOW_RESULT 1037 BEGIN : [Sun Jun 18 19:52:19 2006] # ASSIGN : makespan 1037 # ASSIGN : s_0_0 924 # ASSIGN : s_0_1 456 # ASSIGN : s_0_2 839 # ASSIGN : s_0_3 14 # ASSIGN : s_0_4 5 # ASSIGN : s_1_0 94 # ASSIGN : s_1_1 839 # ASSIGN : s_1_2 778 # ASSIGN : s_1_3 550 # ASSIGN : s_1_4 24 # ASSIGN : s_2_0 9 # ASSIGN : s_2_1 778 # ASSIGN : s_2_2 21 # ASSIGN : s_2_3 860 # ASSIGN : s_2_4 263 # ASSIGN : s_3_0 49 # ASSIGN : s_3_1 776 # ASSIGN : s_3_2 224 # ASSIGN : s_3_3 967 # ASSIGN : s_3_4 783 # ASSIGN : s_4_0 431 # ASSIGN : s_4_1 148 # ASSIGN : s_4_2 1001 # ASSIGN : s_4_3 1033 # ASSIGN : s_4_4 1011 SHOW_RESULT 1037 END : 1037 (0 seconds) [Sun Jun 18 19:52:19 2006] SHOW_RESULT 1037 CPU : 0.0900000000000018 = 0.0800000000000018 + 0.01 + 0 + 0 # BOUND : makespan 1000 1037 MODIFY_CNF 1018 BEGIN : [Sun Jun 18 19:52:19 2006] MODIFY_CNF 1018 END : 10230837 bytes (0 seconds) [Sun Jun 18 19:52:19 2006] MODIFY_CNF 1018 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1018 BEGIN : [Sun Jun 18 19:52:19 2006] CMD : minisat /tmp/csp2sat13822.cnf /tmp/csp2sat13822.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 254927 708757 | 84975 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 1 (2 /sec) decisions : 42 (68 /sec) propagations : 60107 (96947 /sec) conflict literals : 4 (20.00 % deleted) Memory used : 23.55 MB CPU time : 0.62 s SATISFIABLE VERIFY_CNF 1018 END : (1 seconds) [Sun Jun 18 19:52:20 2006] VERIFY_CNF 1018 CPU : 0.74 = 0 + 0 + 0.65 + 0.09 # RESULT : makespan 1018 SATISFIABLE SHOW_RESULT 1018 BEGIN : [Sun Jun 18 19:52:20 2006] # ASSIGN : makespan 1018 # ASSIGN : s_0_0 905 # ASSIGN : s_0_1 50 # ASSIGN : s_0_2 820 # ASSIGN : s_0_3 377 # ASSIGN : s_0_4 22 # ASSIGN : s_1_0 568 # ASSIGN : s_1_1 370 # ASSIGN : s_1_2 921 # ASSIGN : s_1_3 142 # ASSIGN : s_1_4 31 # ASSIGN : s_2_0 7 # ASSIGN : s_2_1 957 # ASSIGN : s_2_2 616 # ASSIGN : s_2_3 819 # ASSIGN : s_2_4 101 # ASSIGN : s_3_0 19 # ASSIGN : s_3_1 17 # ASSIGN : s_3_2 64 # ASSIGN : s_3_3 926 # ASSIGN : s_3_4 742 # ASSIGN : s_4_0 75 # ASSIGN : s_4_1 674 # ASSIGN : s_4_2 982 # ASSIGN : s_4_3 992 # ASSIGN : s_4_4 996 SHOW_RESULT 1018 END : 1018 (0 seconds) [Sun Jun 18 19:52:20 2006] SHOW_RESULT 1018 CPU : 0.0900000000000003 = 0.0700000000000003 + 0.02 + 0 + 0 # BOUND : makespan 1000 1018 MODIFY_CNF 1009 BEGIN : [Sun Jun 18 19:52:20 2006] MODIFY_CNF 1009 END : 10230837 bytes (0 seconds) [Sun Jun 18 19:52:20 2006] MODIFY_CNF 1009 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1009 BEGIN : [Sun Jun 18 19:52:20 2006] CMD : minisat /tmp/csp2sat13822.cnf /tmp/csp2sat13822.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 253127 703357 | 84375 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (3 /sec) decisions : 35 (54 /sec) propagations : 60935 (93746 /sec) conflict literals : 13 (7.14 % deleted) Memory used : 23.55 MB CPU time : 0.65 s SATISFIABLE VERIFY_CNF 1009 END : (1 seconds) [Sun Jun 18 19:52:21 2006] VERIFY_CNF 1009 CPU : 0.74 = 0 + 0 + 0.69 + 0.05 # RESULT : makespan 1009 SATISFIABLE SHOW_RESULT 1009 BEGIN : [Sun Jun 18 19:52:21 2006] # ASSIGN : makespan 1009 # ASSIGN : s_0_0 896 # ASSIGN : s_0_1 15 # ASSIGN : s_0_2 811 # ASSIGN : s_0_3 335 # ASSIGN : s_0_4 6 # ASSIGN : s_1_0 547 # ASSIGN : s_1_1 349 # ASSIGN : s_1_2 912 # ASSIGN : s_1_3 107 # ASSIGN : s_1_4 37 # ASSIGN : s_2_0 884 # ASSIGN : s_2_1 948 # ASSIGN : s_2_2 0 # ASSIGN : s_2_3 777 # ASSIGN : s_2_4 240 # ASSIGN : s_3_0 9 # ASSIGN : s_3_1 7 # ASSIGN : s_3_2 203 # ASSIGN : s_3_3 939 # ASSIGN : s_3_4 755 # ASSIGN : s_4_0 54 # ASSIGN : s_4_1 665 # ASSIGN : s_4_2 973 # ASSIGN : s_4_3 1005 # ASSIGN : s_4_4 983 SHOW_RESULT 1009 END : 1009 (0 seconds) [Sun Jun 18 19:52:21 2006] SHOW_RESULT 1009 CPU : 0.0799999999999983 = 0.0799999999999983 + 0 + 0 + 0 # BOUND : makespan 1000 1009 MODIFY_CNF 1004 BEGIN : [Sun Jun 18 19:52:21 2006] MODIFY_CNF 1004 END : 10230836 bytes (0 seconds) [Sun Jun 18 19:52:21 2006] MODIFY_CNF 1004 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1004 BEGIN : [Sun Jun 18 19:52:21 2006] CMD : minisat /tmp/csp2sat13822.cnf /tmp/csp2sat13822.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 252127 700357 | 84042 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 1 (1 /sec) decisions : 38 (57 /sec) propagations : 60167 (89801 /sec) conflict literals : 5 (16.67 % deleted) Memory used : 23.55 MB CPU time : 0.67 s SATISFIABLE VERIFY_CNF 1004 END : (0 seconds) [Sun Jun 18 19:52:21 2006] VERIFY_CNF 1004 CPU : 0.74 = 0 + 0 + 0.69 + 0.05 # RESULT : makespan 1004 SATISFIABLE SHOW_RESULT 1004 BEGIN : [Sun Jun 18 19:52:21 2006] # ASSIGN : makespan 1004 # ASSIGN : s_0_0 891 # ASSIGN : s_0_1 36 # ASSIGN : s_0_2 806 # ASSIGN : s_0_3 363 # ASSIGN : s_0_4 8 # ASSIGN : s_1_0 554 # ASSIGN : s_1_1 356 # ASSIGN : s_1_2 907 # ASSIGN : s_1_3 128 # ASSIGN : s_1_4 17 # ASSIGN : s_2_0 49 # ASSIGN : s_2_1 943 # ASSIGN : s_2_2 602 # ASSIGN : s_2_3 805 # ASSIGN : s_2_4 87 # ASSIGN : s_3_0 4 # ASSIGN : s_3_1 2 # ASSIGN : s_3_2 50 # ASSIGN : s_3_3 912 # ASSIGN : s_3_4 728 # ASSIGN : s_4_0 61 # ASSIGN : s_4_1 660 # ASSIGN : s_4_2 968 # ASSIGN : s_4_3 978 # ASSIGN : s_4_4 982 SHOW_RESULT 1004 END : 1004 (1 seconds) [Sun Jun 18 19:52:22 2006] SHOW_RESULT 1004 CPU : 0.0799999999999983 = 0.0799999999999983 + 0 + 0 + 0 # BOUND : makespan 1000 1004 MODIFY_CNF 1002 BEGIN : [Sun Jun 18 19:52:22 2006] MODIFY_CNF 1002 END : 10230836 bytes (0 seconds) [Sun Jun 18 19:52:22 2006] MODIFY_CNF 1002 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1002 BEGIN : [Sun Jun 18 19:52:22 2006] CMD : minisat /tmp/csp2sat13822.cnf /tmp/csp2sat13822.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 251727 699157 | 83909 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 1 (2 /sec) decisions : 36 (55 /sec) propagations : 60167 (92565 /sec) conflict literals : 6 (14.29 % deleted) Memory used : 23.55 MB CPU time : 0.65 s SATISFIABLE VERIFY_CNF 1002 END : (0 seconds) [Sun Jun 18 19:52:22 2006] VERIFY_CNF 1002 CPU : 0.75 = 0 + 0 + 0.67 + 0.08 # RESULT : makespan 1002 SATISFIABLE SHOW_RESULT 1002 BEGIN : [Sun Jun 18 19:52:22 2006] # ASSIGN : makespan 1002 # ASSIGN : s_0_0 889 # ASSIGN : s_0_1 34 # ASSIGN : s_0_2 804 # ASSIGN : s_0_3 361 # ASSIGN : s_0_4 6 # ASSIGN : s_1_0 552 # ASSIGN : s_1_1 354 # ASSIGN : s_1_2 905 # ASSIGN : s_1_3 126 # ASSIGN : s_1_4 15 # ASSIGN : s_2_0 47 # ASSIGN : s_2_1 941 # ASSIGN : s_2_2 600 # ASSIGN : s_2_3 803 # ASSIGN : s_2_4 85 # ASSIGN : s_3_0 2 # ASSIGN : s_3_1 0 # ASSIGN : s_3_2 48 # ASSIGN : s_3_3 910 # ASSIGN : s_3_4 726 # ASSIGN : s_4_0 59 # ASSIGN : s_4_1 658 # ASSIGN : s_4_2 966 # ASSIGN : s_4_3 976 # ASSIGN : s_4_4 980 SHOW_RESULT 1002 END : 1002 (0 seconds) [Sun Jun 18 19:52:22 2006] SHOW_RESULT 1002 CPU : 0.0899999999999999 = 0.0899999999999999 + 0 + 0 + 0 # BOUND : makespan 1000 1002 MODIFY_CNF 1001 BEGIN : [Sun Jun 18 19:52:22 2006] MODIFY_CNF 1001 END : 10230836 bytes (0 seconds) [Sun Jun 18 19:52:22 2006] MODIFY_CNF 1001 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1001 BEGIN : [Sun Jun 18 19:52:22 2006] CMD : minisat /tmp/csp2sat13822.cnf /tmp/csp2sat13822.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 251527 698557 | 83842 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 1 (1 /sec) decisions : 38 (54 /sec) propagations : 60167 (84742 /sec) conflict literals : 6 (14.29 % deleted) Memory used : 23.55 MB CPU time : 0.71 s SATISFIABLE VERIFY_CNF 1001 END : (1 seconds) [Sun Jun 18 19:52:23 2006] VERIFY_CNF 1001 CPU : 0.83 = 0 + 0 + 0.74 + 0.09 # RESULT : makespan 1001 SATISFIABLE SHOW_RESULT 1001 BEGIN : [Sun Jun 18 19:52:23 2006] # ASSIGN : makespan 1001 # ASSIGN : s_0_0 888 # ASSIGN : s_0_1 33 # ASSIGN : s_0_2 803 # ASSIGN : s_0_3 360 # ASSIGN : s_0_4 5 # ASSIGN : s_1_0 551 # ASSIGN : s_1_1 353 # ASSIGN : s_1_2 904 # ASSIGN : s_1_3 125 # ASSIGN : s_1_4 14 # ASSIGN : s_2_0 46 # ASSIGN : s_2_1 940 # ASSIGN : s_2_2 599 # ASSIGN : s_2_3 802 # ASSIGN : s_2_4 84 # ASSIGN : s_3_0 1 # ASSIGN : s_3_1 655 # ASSIGN : s_3_2 47 # ASSIGN : s_3_3 909 # ASSIGN : s_3_4 725 # ASSIGN : s_4_0 58 # ASSIGN : s_4_1 657 # ASSIGN : s_4_2 965 # ASSIGN : s_4_3 975 # ASSIGN : s_4_4 979 SHOW_RESULT 1001 END : 1001 (0 seconds) [Sun Jun 18 19:52:23 2006] SHOW_RESULT 1001 CPU : 0.0900000000000003 = 0.0700000000000003 + 0.02 + 0 + 0 # BOUND : makespan 1000 1001 MODIFY_CNF 1000 BEGIN : [Sun Jun 18 19:52:23 2006] MODIFY_CNF 1000 END : 10230836 bytes (0 seconds) [Sun Jun 18 19:52:23 2006] MODIFY_CNF 1000 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1000 BEGIN : [Sun Jun 18 19:52:23 2006] CMD : minisat /tmp/csp2sat13822.cnf /tmp/csp2sat13822.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 251328 697957 | 83776 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 1 (2 /sec) decisions : 36 (58 /sec) propagations : 60167 (97044 /sec) conflict literals : 6 (14.29 % deleted) Memory used : 23.55 MB CPU time : 0.62 s SATISFIABLE VERIFY_CNF 1000 END : (1 seconds) [Sun Jun 18 19:52:24 2006] VERIFY_CNF 1000 CPU : 0.74 = 0 + 0 + 0.649999999999999 + 0.0900000000000001 # RESULT : makespan 1000 SATISFIABLE SHOW_RESULT 1000 BEGIN : [Sun Jun 18 19:52:24 2006] # ASSIGN : makespan 1000 # ASSIGN : s_0_0 887 # ASSIGN : s_0_1 32 # ASSIGN : s_0_2 802 # ASSIGN : s_0_3 359 # ASSIGN : s_0_4 4 # ASSIGN : s_1_0 550 # ASSIGN : s_1_1 352 # ASSIGN : s_1_2 903 # ASSIGN : s_1_3 124 # ASSIGN : s_1_4 13 # ASSIGN : s_2_0 45 # ASSIGN : s_2_1 939 # ASSIGN : s_2_2 598 # ASSIGN : s_2_3 801 # ASSIGN : s_2_4 83 # ASSIGN : s_3_0 0 # ASSIGN : s_3_1 654 # ASSIGN : s_3_2 46 # ASSIGN : s_3_3 908 # ASSIGN : s_3_4 724 # ASSIGN : s_4_0 57 # ASSIGN : s_4_1 656 # ASSIGN : s_4_2 964 # ASSIGN : s_4_3 974 # ASSIGN : s_4_4 978 SHOW_RESULT 1000 END : 1000 (0 seconds) [Sun Jun 18 19:52:24 2006] SHOW_RESULT 1000 CPU : 0.0800000000000018 = 0.0800000000000018 + 0 + 0 + 0 # BOUND : makespan 1000 1000 MAIN END : (27 seconds) [Sun Jun 18 19:52:24 2006] MAIN CPU : 27.2 = 18.85 + 0.12 + 7.43 + 0.8