Label | Meaning |
---|---|
S | Solution {OPTIMUM FOUND or OPT | UNSATISFIABLE or UNSAT | UNKNOWN | Not available or N/A} |
O | Best solution found |
T | CPU time (TO for Time Out) |
(out)(err) | Standard output and standard error for each solver |
Color | Meaning for Complete Solvers | Meaning for Incomplete Solvers |
---|---|---|
Text | Best solver column | Best solver column |
Text | Optimal solution with the best CPU time | Best solution with the best CPU time |
Text | Optimal solution and finished within the Time Out | Best solution without the best CPU time |
Text | Optimal solution and did not finish within the Time Out | Solution found but not the best |
Text | Time Out | Time Out |
Text | Buggy solution | Buggy solution |
Instance file name | Best solver | Sat4j-i | ubcsat-irots |
---|---|---|---|
clq1-cv160c800l2g1.wcnf | O = 75 T = 46.93 |
O = 112 T = 4.99 (out)(err) |
O = 75 T = 46.93 (out)(err) |
clq1-cv160c800l2g10.wcnf | O = 68 T = 190.03 |
O = 86 T = 25.77 (out)(err) |
O = 68 T = 190.03 (out)(err) |
clq1-cv160c800l2g11.wcnf | O = 83 T = 202.24 |
O = 111 T = 117.11 (out)(err) |
O = 83 T = 202.24 (out)(err) |
clq1-cv160c800l2g12.wcnf | O = 75 T = 30.86 |
O = 101 T = 4.52 (out)(err) |
O = 75 T = 30.86 (out)(err) |
clq1-cv160c800l2g13.wcnf | O = 67 T = 89.85 |
O = 90 T = 1.95 (out)(err) |
O = 67 T = 89.85 (out)(err) |
clq1-cv160c800l2g14.wcnf | O = 55 T = 30.84 |
O = 85 T = 4.55 (out)(err) |
O = 55 T = 30.84 (out)(err) |
clq1-cv160c800l2g15.wcnf | O = 80 T = 134.13 |
O = 95 T = 5.45 (out)(err) |
O = 80 T = 134.13 (out)(err) |
clq1-cv160c800l2g16.wcnf | O = 68 T = 32.72 |
O = 104 T = 5.32 (out)(err) |
O = 68 T = 32.72 (out)(err) |
clq1-cv160c800l2g17.wcnf | O = 72 T = 203.21 |
O = 97 T = 1.91 (out)(err) |
O = 72 T = 203.21 (out)(err) |
clq1-cv160c800l2g18.wcnf | O = 67 T = 30.49 |
O = 99 T = 85.83 (out)(err) |
O = 67 T = 30.49 (out)(err) |
clq1-cv160c800l2g19.wcnf | O = 87 T = 44.23 |
O = 119 T = 5.34 (out)(err) |
O = 87 T = 44.23 (out)(err) |
clq1-cv160c800l2g2.wcnf | O = 67 T = 29.33 |
O = 87 T = 54.64 (out)(err) |
O = 67 T = 29.33 (out)(err) |
clq1-cv160c800l2g20.wcnf | O = 61 T = 36.40 |
O = 91 T = 2.73 (out)(err) |
O = 61 T = 36.40 (out)(err) |
clq1-cv160c800l2g21.wcnf | O = 73 T = 58.02 |
O = 90 T = 2.12 (out)(err) |
O = 73 T = 58.02 (out)(err) |
clq1-cv160c800l2g22.wcnf | O = 70 T = 155.45 |
O = 111 T = 5.46 (out)(err) |
O = 70 T = 155.45 (out)(err) |
clq1-cv160c800l2g23.wcnf | O = 63 T = 191.73 |
O = 99 T = 2.24 (out)(err) |
O = 63 T = 191.73 (out)(err) |
clq1-cv160c800l2g24.wcnf | O = 70 T = 31.85 |
O = 81 T = 147.58 (out)(err) |
O = 70 T = 31.85 (out)(err) |
clq1-cv160c800l2g25.wcnf | O = 68 T = 29.78 |
O = 106 T = 3.75 (out)(err) |
O = 68 T = 29.78 (out)(err) |
clq1-cv160c800l2g26.wcnf | O = 67 T = 114.27 |
O = 90 T = 5.12 (out)(err) |
O = 67 T = 114.27 (out)(err) |
clq1-cv160c800l2g27.wcnf | O = 73 T = 252.69 |
O = 108 T = 1.09 (out)(err) |
O = 73 T = 252.69 (out)(err) |
clq1-cv160c800l2g28.wcnf | O = 63 T = 45.30 |
O = 98 T = 4.97 (out)(err) |
O = 63 T = 45.30 (out)(err) |
clq1-cv160c800l2g29.wcnf | O = 58 T = 32.33 |
O = 82 T = 5.13 (out)(err) |
O = 58 T = 32.33 (out)(err) |
clq1-cv160c800l2g3.wcnf | O = 75 T = 189.11 |
O = 107 T = 3.67 (out)(err) |
O = 75 T = 189.11 (out)(err) |
clq1-cv160c800l2g30.wcnf | O = 78 T = 103.45 |
O = 122 T = 3.67 (out)(err) |
O = 78 T = 103.45 (out)(err) |
clq1-cv160c800l2g4.wcnf | O = 68 T = 130.27 |
O = 99 T = 4.45 (out)(err) |
O = 68 T = 130.27 (out)(err) |
clq1-cv160c800l2g5.wcnf | O = 62 T = 100.47 |
O = 87 T = 3.81 (out)(err) |
O = 62 T = 100.47 (out)(err) |
clq1-cv160c800l2g6.wcnf | O = 79 T = 93.31 |
O = 102 T = 4.75 (out)(err) |
O = 79 T = 93.31 (out)(err) |
clq1-cv160c800l2g7.wcnf | O = 83 T = 127.25 |
O = 94 T = 2.98 (out)(err) |
O = 83 T = 127.25 (out)(err) |
clq1-cv160c800l2g8.wcnf | O = 65 T = 80.32 |
O = 79 T = 29.96 (out)(err) |
O = 65 T = 80.32 (out)(err) |
clq1-cv160c800l2g9.wcnf | O = 70 T = 106.15 |
O = 87 T = 151.98 (out)(err) |
O = 70 T = 106.15 (out)(err) |
clq1-cv260c1040l2g1.wcnf | O = 96 T = 42.62 |
O = 100 T = 1.72 (out)(err) |
O = 96 T = 42.62 (out)(err) |
clq1-cv260c1040l2g10.wcnf | O = 93 T = 37.70 |
O = 94 T = 4.59 (out)(err) |
O = 93 T = 37.70 (out)(err) |
clq1-cv260c1040l2g11.wcnf | O = 50 T = 2.33 |
O = 50 T = 2.33 (out)(err) |
O = 71 T = 67.27 (out)(err) |
clq1-cv260c1040l2g12.wcnf | O = 84 T = 184.39 |
O = 88 T = 3.22 (out)(err) |
O = 84 T = 184.39 (out)(err) |
clq1-cv260c1040l2g13.wcnf | O = 56 T = 3.57 |
O = 56 T = 3.57 (out)(err) |
O = 70 T = 16.20 (out)(err) |
clq1-cv260c1040l2g14.wcnf | O = 84 T = 37.59 |
O = 104 T = 5.22 (out)(err) |
O = 84 T = 37.59 (out)(err) |
clq1-cv260c1040l2g15.wcnf | O = 64 T = 1.83 |
O = 64 T = 1.83 (out)(err) |
O = 80 T = 176.11 (out)(err) |
clq1-cv260c1040l2g16.wcnf | O = 82 T = 4.36 |
O = 82 T = 4.36 (out)(err) |
O = 82 T = 39.31 (out)(err) |
clq1-cv260c1040l2g17.wcnf | O = 78 T = 36.66 |
O = 80 T = 3.88 (out)(err) |
O = 78 T = 36.66 (out)(err) |
clq1-cv260c1040l2g18.wcnf | O = 66 T = 39.62 |
O = 70 T = 5.66 (out)(err) |
O = 66 T = 39.62 (out)(err) |
clq1-cv260c1040l2g19.wcnf | O = 91 T = 3.78 |
O = 91 T = 3.78 (out)(err) |
O = 95 T = 121.16 (out)(err) |
clq1-cv260c1040l2g2.wcnf | O = 86 T = 11.29 |
O = 86 T = 176.45 (out)(err) |
O = 86 T = 11.29 (out)(err) |
clq1-cv260c1040l2g20.wcnf | O = 82 T = 3.01 |
O = 82 T = 3.01 (out)(err) |
O = 84 T = 43.56 (out)(err) |
clq1-cv260c1040l2g21.wcnf | O = 83 T = 42.17 |
O = 90 T = 1.37 (out)(err) |
O = 83 T = 42.17 (out)(err) |
clq1-cv260c1040l2g22.wcnf | O = 91 T = 40.30 |
O = 115 T = 3.57 (out)(err) |
O = 91 T = 40.30 (out)(err) |
clq1-cv260c1040l2g23.wcnf | O = 82 T = 37.78 |
O = 98 T = 4.89 (out)(err) |
O = 82 T = 37.78 (out)(err) |
clq1-cv260c1040l2g24.wcnf | O = 62 T = 2.02 |
O = 62 T = 2.02 (out)(err) |
O = 77 T = 30.75 (out)(err) |
clq1-cv260c1040l2g25.wcnf | O = 66 T = 155.53 |
O = 91 T = 1.71 (out)(err) |
O = 66 T = 155.53 (out)(err) |
clq1-cv260c1040l2g26.wcnf | O = 73 T = 41.21 |
O = 82 T = 4.36 (out)(err) |
O = 73 T = 41.21 (out)(err) |
clq1-cv260c1040l2g27.wcnf | O = 99 T = 38.06 |
O = 130 T = 3.87 (out)(err) |
O = 99 T = 38.06 (out)(err) |
clq1-cv260c1040l2g28.wcnf | O = 94 T = 252.99 |
O = 100 T = 4.02 (out)(err) |
O = 94 T = 252.99 (out)(err) |
clq1-cv260c1040l2g29.wcnf | O = 81 T = 20.13 |
O = 105 T = 2.50 (out)(err) |
O = 81 T = 20.13 (out)(err) |
clq1-cv260c1040l2g3.wcnf | O = 75 T = 76.40 |
O = 89 T = 2.55 (out)(err) |
O = 75 T = 76.40 (out)(err) |
clq1-cv260c1040l2g30.wcnf | O = 86 T = 37.19 |
O = 101 T = 4.00 (out)(err) |
O = 86 T = 37.19 (out)(err) |
clq1-cv260c1040l2g4.wcnf | O = 75 T = 193.94 |
O = 79 T = 1.31 (out)(err) |
O = 75 T = 193.94 (out)(err) |
clq1-cv260c1040l2g5.wcnf | O = 89 T = 2.70 |
O = 89 T = 2.70 (out)(err) |
O = 90 T = 173.03 (out)(err) |
clq1-cv260c1040l2g6.wcnf | O = 86 T = 26.97 |
O = 90 T = 2.90 (out)(err) |
O = 86 T = 26.97 (out)(err) |
clq1-cv260c1040l2g7.wcnf | O = 76 T = 42.44 |
O = 82 T = 3.55 (out)(err) |
O = 76 T = 42.44 (out)(err) |
clq1-cv260c1040l2g8.wcnf | O = 74 T = 262.74 |
O = 82 T = 3.35 (out)(err) |
O = 74 T = 262.74 (out)(err) |
clq1-cv260c1040l2g9.wcnf | O = 64 T = 4.01 |
O = 64 T = 4.01 (out)(err) |
O = 80 T = 110.47 (out)(err) |
clq1-c2mv70c350l3g1.wcnf | O = 57 T = 28.31 |
O = 72 T = 3.96 (out)(err) |
O = 57 T = 28.31 (out)(err) |
clq1-c2mv70c350l3g10.wcnf | O = 43 T = 80.61 |
O = 59 T = 2.05 (out)(err) |
O = 43 T = 80.61 (out)(err) |
clq1-c2mv70c350l3g11.wcnf | O = 50 T = 11.98 |
O = 67 T = 67.64 (out)(err) |
O = 50 T = 11.98 (out)(err) |
clq1-c2mv70c350l3g12.wcnf | O = 52 T = 13.62 |
O = 66 T = 1.99 (out)(err) |
O = 52 T = 13.62 (out)(err) |
clq1-c2mv70c350l3g13.wcnf | O = 47 T = 198.87 |
O = 69 T = 8.18 (out)(err) |
O = 47 T = 198.87 (out)(err) |
clq1-c2mv70c350l3g14.wcnf | O = 51 T = 131.40 |
O = 73 T = 2.76 (out)(err) |
O = 51 T = 131.40 (out)(err) |
clq1-c2mv70c350l3g15.wcnf | O = 53 T = 229.61 |
O = 81 T = 4.66 (out)(err) |
O = 53 T = 229.61 (out)(err) |
clq1-c2mv70c350l3g16.wcnf | O = 52 T = 193.45 |
O = 70 T = 4.80 (out)(err) |
O = 52 T = 193.45 (out)(err) |
clq1-c2mv70c350l3g17.wcnf | O = 47 T = 11.66 |
O = 62 T = 5.03 (out)(err) |
O = 47 T = 11.66 (out)(err) |
clq1-c2mv70c350l3g18.wcnf | O = 52 T = 83.02 |
O = 67 T = 4.10 (out)(err) |
O = 52 T = 83.02 (out)(err) |
clq1-c2mv70c350l3g19.wcnf | O = 56 T = 41.68 |
O = 75 T = 4.75 (out)(err) |
O = 56 T = 41.68 (out)(err) |
clq1-c2mv70c350l3g2.wcnf | O = 48 T = 181.84 |
O = 70 T = 1.60 (out)(err) |
O = 48 T = 181.84 (out)(err) |
clq1-c2mv70c350l3g20.wcnf | O = 52 T = 16.38 |
O = 69 T = 65.61 (out)(err) |
O = 52 T = 16.38 (out)(err) |
clq1-c2mv70c350l3g21.wcnf | O = 40 T = 184.87 |
O = 62 T = 4.60 (out)(err) |
O = 40 T = 184.87 (out)(err) |
clq1-c2mv70c350l3g22.wcnf | O = 51 T = 100.08 |
O = 71 T = 1.72 (out)(err) |
O = 51 T = 100.08 (out)(err) |
clq1-c2mv70c350l3g23.wcnf | O = 53 T = 65.54 |
O = 69 T = 3.03 (out)(err) |
O = 53 T = 65.54 (out)(err) |
clq1-c2mv70c350l3g24.wcnf | O = 53 T = 150.62 |
O = 69 T = 20.93 (out)(err) |
O = 53 T = 150.62 (out)(err) |
clq1-c2mv70c350l3g25.wcnf | O = 45 T = 29.20 |
O = 70 T = 2.88 (out)(err) |
O = 45 T = 29.20 (out)(err) |
clq1-c2mv70c350l3g26.wcnf | O = 51 T = 35.24 |
O = 74 T = 2.07 (out)(err) |
O = 51 T = 35.24 (out)(err) |
clq1-c2mv70c350l3g27.wcnf | O = 58 T = 132.35 |
O = 71 T = 4.29 (out)(err) |
O = 58 T = 132.35 (out)(err) |
clq1-c2mv70c350l3g28.wcnf | O = 54 T = 12.41 |
O = 71 T = 3.93 (out)(err) |
O = 54 T = 12.41 (out)(err) |
clq1-c2mv70c350l3g29.wcnf | O = 55 T = 161.92 |
O = 80 T = 8.59 (out)(err) |
O = 55 T = 161.92 (out)(err) |
clq1-c2mv70c350l3g3.wcnf | O = 51 T = 52.76 |
O = 76 T = 3.32 (out)(err) |
O = 51 T = 52.76 (out)(err) |
clq1-c2mv70c350l3g30.wcnf | O = 55 T = 14.67 |
O = 72 T = 2.28 (out)(err) |
O = 55 T = 14.67 (out)(err) |
clq1-c2mv70c350l3g4.wcnf | O = 50 T = 220.85 |
O = 61 T = 4.19 (out)(err) |
O = 50 T = 220.85 (out)(err) |
clq1-c2mv70c350l3g5.wcnf | O = 48 T = 13.57 |
O = 66 T = 3.25 (out)(err) |
O = 48 T = 13.57 (out)(err) |
clq1-c2mv70c350l3g6.wcnf | O = 51 T = 26.45 |
O = 72 T = 2.56 (out)(err) |
O = 51 T = 26.45 (out)(err) |
clq1-c2mv70c350l3g7.wcnf | O = 55 T = 218.49 |
O = 72 T = 3.72 (out)(err) |
O = 55 T = 218.49 (out)(err) |
clq1-c2mv70c350l3g8.wcnf | O = 50 T = 162.76 |
O = 58 T = 5.03 (out)(err) |
O = 50 T = 162.76 (out)(err) |
clq1-c2mv70c350l3g9.wcnf | O = 52 T = 129.06 |
O = 68 T = 4.84 (out)(err) |
O = 52 T = 129.06 (out)(err) |
clq1-c2mv80c400l3g1.wcnf | O = 59 T = 152.79 |
O = 95 T = 2.39 (out)(err) |
O = 59 T = 152.79 (out)(err) |
clq1-c2mv80c400l3g10.wcnf | O = 60 T = 11.55 |
O = 85 T = 8.91 (out)(err) |
O = 60 T = 11.55 (out)(err) |
clq1-c2mv80c400l3g11.wcnf | O = 59 T = 16.85 |
O = 84 T = 3.94 (out)(err) |
O = 59 T = 16.85 (out)(err) |
clq1-c2mv80c400l3g12.wcnf | O = 66 T = 61.03 |
O = 86 T = 6.82 (out)(err) |
O = 66 T = 61.03 (out)(err) |
clq1-c2mv80c400l3g13.wcnf | O = 62 T = 31.45 |
O = 88 T = 3.74 (out)(err) |
O = 62 T = 31.45 (out)(err) |
clq1-c2mv80c400l3g14.wcnf | O = 61 T = 152.29 |
O = 83 T = 4.55 (out)(err) |
O = 61 T = 152.29 (out)(err) |
clq1-c2mv80c400l3g15.wcnf | O = 62 T = 15.25 |
O = 92 T = 5.44 (out)(err) |
O = 62 T = 15.25 (out)(err) |
clq1-c2mv80c400l3g16.wcnf | O = 65 T = 14.98 |
O = 89 T = 5.03 (out)(err) |
O = 65 T = 14.98 (out)(err) |
clq1-c2mv80c400l3g17.wcnf | O = 68 T = 79.46 |
O = 83 T = 6.01 (out)(err) |
O = 68 T = 79.46 (out)(err) |
clq1-c2mv80c400l3g18.wcnf | O = 59 T = 15.50 |
O = 89 T = 4.96 (out)(err) |
O = 59 T = 15.50 (out)(err) |
clq1-c2mv80c400l3g19.wcnf | O = 57 T = 212.64 |
O = 82 T = 4.25 (out)(err) |
O = 57 T = 212.64 (out)(err) |
clq1-c2mv80c400l3g2.wcnf | O = 68 T = 207.69 |
O = 94 T = 3.98 (out)(err) |
O = 68 T = 207.69 (out)(err) |
clq1-c2mv80c400l3g20.wcnf | O = 58 T = 202.68 |
O = 95 T = 6.51 (out)(err) |
O = 58 T = 202.68 (out)(err) |
clq1-c2mv80c400l3g21.wcnf | O = 67 T = 188.58 |
O = 91 T = 6.11 (out)(err) |
O = 67 T = 188.58 (out)(err) |
clq1-c2mv80c400l3g22.wcnf | O = 68 T = 30.31 |
O = 97 T = 3.45 (out)(err) |
O = 68 T = 30.31 (out)(err) |
clq1-c2mv80c400l3g23.wcnf | O = 58 T = 52.38 |
O = 92 T = 4.85 (out)(err) |
O = 58 T = 52.38 (out)(err) |
clq1-c2mv80c400l3g24.wcnf | O = 54 T = 16.67 |
O = 90 T = 4.64 (out)(err) |
O = 54 T = 16.67 (out)(err) |
clq1-c2mv80c400l3g25.wcnf | O = 58 T = 15.01 |
O = 98 T = 4.70 (out)(err) |
O = 58 T = 15.01 (out)(err) |
clq1-c2mv80c400l3g26.wcnf | O = 59 T = 113.07 |
O = 97 T = 2.38 (out)(err) |
O = 59 T = 113.07 (out)(err) |
clq1-c2mv80c400l3g27.wcnf | O = 62 T = 17.23 |
O = 88 T = 1.72 (out)(err) |
O = 62 T = 17.23 (out)(err) |
clq1-c2mv80c400l3g28.wcnf | O = 60 T = 162.71 |
O = 89 T = 5.16 (out)(err) |
O = 60 T = 162.71 (out)(err) |
clq1-c2mv80c400l3g29.wcnf | O = 66 T = 10.27 |
O = 90 T = 5.00 (out)(err) |
O = 66 T = 10.27 (out)(err) |
clq1-c2mv80c400l3g3.wcnf | O = 64 T = 44.87 |
O = 96 T = 3.02 (out)(err) |
O = 64 T = 44.87 (out)(err) |
clq1-c2mv80c400l3g30.wcnf | O = 60 T = 181.55 |
O = 93 T = 3.91 (out)(err) |
O = 60 T = 181.55 (out)(err) |
clq1-c2mv80c400l3g4.wcnf | O = 63 T = 16.15 |
O = 95 T = 3.92 (out)(err) |
O = 63 T = 16.15 (out)(err) |
clq1-c2mv80c400l3g5.wcnf | O = 67 T = 15.45 |
O = 87 T = 2.56 (out)(err) |
O = 67 T = 15.45 (out)(err) |
clq1-c2mv80c400l3g6.wcnf | O = 63 T = 35.36 |
O = 91 T = 5.96 (out)(err) |
O = 63 T = 35.36 (out)(err) |
clq1-c2mv80c400l3g7.wcnf | O = 66 T = 43.71 |
O = 92 T = 3.64 (out)(err) |
O = 66 T = 43.71 (out)(err) |
clq1-c2mv80c400l3g8.wcnf | O = 68 T = 13.35 |
O = 86 T = 5.17 (out)(err) |
O = 68 T = 13.35 (out)(err) |
clq1-c2mv80c400l3g9.wcnf | O = 63 T = 31.04 |
O = 86 T = 4.42 (out)(err) |
O = 63 T = 31.04 (out)(err) |
file_rpms_wcnf_L2_V150_C4000_H150_0.wcnf | O = 802 T = 9.28 |
O = 930 T = 5.60 (out)(err) |
O = 802 T = 9.28 (out)(err) |
file_rpms_wcnf_L2_V150_C4000_H150_1.wcnf | O = 4802 T = 7.75 |
O = N/A T = TO (out)(err) |
O = 4802 T = 7.75 (out)(err) |
file_rpms_wcnf_L2_V150_C4000_H150_2.wcnf | O = 805 T = 10.03 |
O = 934 T = 6.06 (out)(err) |
O = 805 T = 10.03 (out)(err) |
file_rpms_wcnf_L2_V150_C4000_H150_3.wcnf | O = 752 T = 8.69 |
O = 909 T = 7.65 (out)(err) |
O = 752 T = 8.69 (out)(err) |
file_rpms_wcnf_L2_V150_C4000_H150_4.wcnf | O = 750 T = 10.32 |
O = 896 T = 4.62 (out)(err) |
O = 750 T = 10.32 (out)(err) |
file_rpms_wcnf_L2_V150_C4000_H150_5.wcnf | O = 756 T = 3.95 |
O = 879 T = 4.36 (out)(err) |
O = 756 T = 3.95 (out)(err) |
file_rpms_wcnf_L2_V150_C4000_H150_6.wcnf | O = 782 T = 7.26 |
O = 880 T = 5.50 (out)(err) |
O = 782 T = 7.26 (out)(err) |
file_rpms_wcnf_L2_V150_C4000_H150_7.wcnf | O = 755 T = 7.09 |
O = 920 T = 5.74 (out)(err) |
O = 755 T = 7.09 (out)(err) |
file_rpms_wcnf_L2_V150_C4000_H150_8.wcnf | O = 764 T = 12.31 |
O = 909 T = 4.98 (out)(err) |
O = 764 T = 12.31 (out)(err) |
file_rpms_wcnf_L2_V150_C4000_H150_9.wcnf | O = 792 T = 9.07 |
O = 948 T = 3.24 (out)(err) |
O = 792 T = 9.07 (out)(err) |
file_rpms_wcnf_L2_V150_C4500_H150_0.wcnf | O = 867 T = 10.10 |
O = 1047 T = 5.27 (out)(err) |
O = 867 T = 10.10 (out)(err) |
file_rpms_wcnf_L2_V150_C4500_H150_1.wcnf | O = 905 T = 8.34 |
O = 1021 T = 4.71 (out)(err) |
O = 905 T = 8.34 (out)(err) |
file_rpms_wcnf_L2_V150_C4500_H150_2.wcnf | O = 912 T = 7.52 |
O = 1007 T = 7.09 (out)(err) |
O = 912 T = 7.52 (out)(err) |
file_rpms_wcnf_L2_V150_C4500_H150_3.wcnf | O = 878 T = 8.03 |
O = 1053 T = 8.87 (out)(err) |
O = 878 T = 8.03 (out)(err) |
file_rpms_wcnf_L2_V150_C4500_H150_4.wcnf | O = 890 T = 10.47 |
O = 1066 T = 6.19 (out)(err) |
O = 890 T = 10.47 (out)(err) |
file_rpms_wcnf_L2_V150_C4500_H150_5.wcnf | O = 881 T = 9.41 |
O = 1099 T = 4.44 (out)(err) |
O = 881 T = 9.41 (out)(err) |
file_rpms_wcnf_L2_V150_C4500_H150_6.wcnf | O = 856 T = 8.25 |
O = 985 T = 4.40 (out)(err) |
O = 856 T = 8.25 (out)(err) |
file_rpms_wcnf_L2_V150_C4500_H150_7.wcnf | O = 875 T = 9.79 |
O = 1034 T = 3.93 (out)(err) |
O = 875 T = 9.79 (out)(err) |
file_rpms_wcnf_L2_V150_C4500_H150_8.wcnf | O = 908 T = 8.18 |
O = 1048 T = 5.26 (out)(err) |
O = 908 T = 8.18 (out)(err) |
file_rpms_wcnf_L2_V150_C4500_H150_9.wcnf | O = 898 T = 11.06 |
O = 1048 T = 3.48 (out)(err) |
O = 898 T = 11.06 (out)(err) |
file_rpms_wcnf_L2_V150_C5000_H150_0.wcnf | O = 1018 T = 11.80 |
O = 1178 T = 7.03 (out)(err) |
O = 1018 T = 11.80 (out)(err) |
file_rpms_wcnf_L2_V150_C5000_H150_1.wcnf | O = 1015 T = 9.85 |
O = 1198 T = 5.41 (out)(err) |
O = 1015 T = 9.85 (out)(err) |
file_rpms_wcnf_L2_V150_C5000_H150_2.wcnf | O = 979 T = 9.59 |
O = 1120 T = 4.52 (out)(err) |
O = 979 T = 9.59 (out)(err) |
file_rpms_wcnf_L2_V150_C5000_H150_3.wcnf | O = 1032 T = 9.89 |
O = 1164 T = 4.25 (out)(err) |
O = 1032 T = 9.89 (out)(err) |
file_rpms_wcnf_L2_V150_C5000_H150_4.wcnf | O = 1018 T = 7.36 |
O = 1155 T = 5.73 (out)(err) |
O = 1018 T = 7.36 (out)(err) |
file_rpms_wcnf_L2_V150_C5000_H150_5.wcnf | O = 991 T = 7.27 |
O = 1130 T = 3.17 (out)(err) |
O = 991 T = 7.27 (out)(err) |
file_rpms_wcnf_L2_V150_C5000_H150_6.wcnf | O = 1005 T = 7.93 |
O = 1129 T = 5.29 (out)(err) |
O = 1005 T = 7.93 (out)(err) |
file_rpms_wcnf_L2_V150_C5000_H150_7.wcnf | O = 991 T = 9.46 |
O = 1132 T = 5.54 (out)(err) |
O = 991 T = 9.46 (out)(err) |
file_rpms_wcnf_L2_V150_C5000_H150_8.wcnf | O = 999 T = 10.81 |
O = 1151 T = 3.80 (out)(err) |
O = 999 T = 10.81 (out)(err) |
file_rpms_wcnf_L2_V150_C5000_H150_9.wcnf | O = 993 T = 5.40 |
O = 1140 T = 4.17 (out)(err) |
O = 993 T = 5.40 (out)(err) |
file_rpms_wcnf_L2_V150_C2500_H150_0.wcnf | O = 464 T = 9.29 |
O = 536 T = 5.17 (out)(err) |
O = 464 T = 9.29 (out)(err) |
file_rpms_wcnf_L2_V150_C2500_H150_1.wcnf | O = 454 T = 9.63 |
O = 575 T = 2.80 (out)(err) |
O = 454 T = 9.63 (out)(err) |
file_rpms_wcnf_L2_V150_C2500_H150_2.wcnf | O = 423 T = 5.91 |
O = 543 T = 4.99 (out)(err) |
O = 423 T = 5.91 (out)(err) |
file_rpms_wcnf_L2_V150_C2500_H150_3.wcnf | O = 442 T = 7.42 |
O = 551 T = 2.38 (out)(err) |
O = 442 T = 7.42 (out)(err) |
file_rpms_wcnf_L2_V150_C2500_H150_4.wcnf | O = 447 T = 8.18 |
O = 535 T = 5.45 (out)(err) |
O = 447 T = 8.18 (out)(err) |
file_rpms_wcnf_L2_V150_C2500_H150_5.wcnf | O = 433 T = 7.28 |
O = 521 T = 4.34 (out)(err) |
O = 433 T = 7.28 (out)(err) |
file_rpms_wcnf_L2_V150_C2500_H150_6.wcnf | O = 461 T = 8.47 |
O = 523 T = 3.65 (out)(err) |
O = 461 T = 8.47 (out)(err) |
file_rpms_wcnf_L2_V150_C2500_H150_7.wcnf | O = 434 T = 8.58 |
O = 549 T = 5.45 (out)(err) |
O = 434 T = 8.58 (out)(err) |
file_rpms_wcnf_L2_V150_C2500_H150_8.wcnf | O = 456 T = 0.87 |
O = 531 T = 3.51 (out)(err) |
O = 456 T = 0.87 (out)(err) |
file_rpms_wcnf_L2_V150_C2500_H150_9.wcnf | O = 470 T = 7.77 |
O = 566 T = 2.18 (out)(err) |
O = 470 T = 7.77 (out)(err) |
file_rpms_wcnf_L2_V150_C3000_H150_0.wcnf | O = 539 T = 8.72 |
O = 694 T = 3.10 (out)(err) |
O = 539 T = 8.72 (out)(err) |
file_rpms_wcnf_L2_V150_C3000_H150_1.wcnf | O = 560 T = 7.14 |
O = 699 T = 5.55 (out)(err) |
O = 560 T = 7.14 (out)(err) |
file_rpms_wcnf_L2_V150_C3000_H150_2.wcnf | O = 531 T = 1.17 |
O = 662 T = 5.26 (out)(err) |
O = 531 T = 1.17 (out)(err) |
file_rpms_wcnf_L2_V150_C3000_H150_3.wcnf | O = 555 T = 9.76 |
O = 652 T = 3.00 (out)(err) |
O = 555 T = 9.76 (out)(err) |
file_rpms_wcnf_L2_V150_C3000_H150_4.wcnf | O = 556 T = 9.52 |
O = 626 T = 1.98 (out)(err) |
O = 556 T = 9.52 (out)(err) |
file_rpms_wcnf_L2_V150_C3000_H150_5.wcnf | O = 538 T = 6.90 |
O = 679 T = 3.01 (out)(err) |
O = 538 T = 6.90 (out)(err) |
file_rpms_wcnf_L2_V150_C3000_H150_6.wcnf | O = 537 T = 7.81 |
O = 663 T = 1.22 (out)(err) |
O = 537 T = 7.81 (out)(err) |
file_rpms_wcnf_L2_V150_C3000_H150_7.wcnf | O = 527 T = 8.10 |
O = 648 T = 3.27 (out)(err) |
O = 527 T = 8.10 (out)(err) |
file_rpms_wcnf_L2_V150_C3000_H150_8.wcnf | O = 564 T = 3.53 |
O = 649 T = 2.34 (out)(err) |
O = 564 T = 3.53 (out)(err) |
file_rpms_wcnf_L2_V150_C3000_H150_9.wcnf | O = 552 T = 9.08 |
O = 652 T = 5.02 (out)(err) |
O = 552 T = 9.08 (out)(err) |
file_rpms_wcnf_L2_V150_C3500_H150_0.wcnf | O = 680 T = 8.12 |
O = 790 T = 5.60 (out)(err) |
O = 680 T = 8.12 (out)(err) |
file_rpms_wcnf_L2_V150_C3500_H150_1.wcnf | O = 679 T = 8.12 |
O = 802 T = 5.99 (out)(err) |
O = 679 T = 8.12 (out)(err) |
file_rpms_wcnf_L2_V150_C3500_H150_2.wcnf | O = 716 T = 7.52 |
O = 796 T = 2.89 (out)(err) |
O = 716 T = 7.52 (out)(err) |
file_rpms_wcnf_L2_V150_C3500_H150_3.wcnf | O = 669 T = 7.33 |
O = 776 T = 5.11 (out)(err) |
O = 669 T = 7.33 (out)(err) |
file_rpms_wcnf_L2_V150_C3500_H150_4.wcnf | O = 627 T = 6.98 |
O = 754 T = 3.70 (out)(err) |
O = 627 T = 6.98 (out)(err) |
file_rpms_wcnf_L2_V150_C3500_H150_5.wcnf | O = 667 T = 6.04 |
O = 809 T = 5.79 (out)(err) |
O = 667 T = 6.04 (out)(err) |
file_rpms_wcnf_L2_V150_C3500_H150_6.wcnf | O = 688 T = 9.18 |
O = 819 T = 1.99 (out)(err) |
O = 688 T = 9.18 (out)(err) |
file_rpms_wcnf_L2_V150_C3500_H150_7.wcnf | O = 675 T = 7.71 |
O = 808 T = 3.74 (out)(err) |
O = 675 T = 7.71 (out)(err) |
file_rpms_wcnf_L2_V150_C3500_H150_8.wcnf | O = 675 T = 10.68 |
O = 823 T = 5.59 (out)(err) |
O = 675 T = 10.68 (out)(err) |
file_rpms_wcnf_L2_V150_C3500_H150_9.wcnf | O = 638 T = 8.71 |
O = 794 T = 3.57 (out)(err) |
O = 638 T = 8.71 (out)(err) |
file_rpms_wcnf_L3_V100_C600_H100_0.wcnf | O = 8 T = 3.51 |
O = 15 T = 21.39 (out)(err) |
O = 8 T = 3.51 (out)(err) |
file_rpms_wcnf_L3_V100_C600_H100_1.wcnf | O = 8 T = 3.36 |
O = 21 T = 4.81 (out)(err) |
O = 8 T = 3.36 (out)(err) |
file_rpms_wcnf_L3_V100_C600_H100_2.wcnf | O = 8 T = 3.03 |
O = 36 T = 5.14 (out)(err) |
O = 8 T = 3.03 (out)(err) |
file_rpms_wcnf_L3_V100_C600_H100_3.wcnf | O = 9 T = 2.60 |
O = 35 T = 3.92 (out)(err) |
O = 9 T = 2.60 (out)(err) |
file_rpms_wcnf_L3_V100_C600_H100_4.wcnf | O = 7 T = 3.16 |
O = 28 T = 4.82 (out)(err) |
O = 7 T = 3.16 (out)(err) |
file_rpms_wcnf_L3_V100_C600_H100_5.wcnf | O = 8 T = 3.99 |
O = 34 T = 4.32 (out)(err) |
O = 8 T = 3.99 (out)(err) |
file_rpms_wcnf_L3_V100_C600_H100_6.wcnf | O = 7 T = 3.22 |
O = 15 T = 5.09 (out)(err) |
O = 7 T = 3.22 (out)(err) |
file_rpms_wcnf_L3_V100_C600_H100_7.wcnf | O = 8 T = 3.36 |
O = 26 T = 2.62 (out)(err) |
O = 8 T = 3.36 (out)(err) |
file_rpms_wcnf_L3_V100_C600_H100_8.wcnf | O = 5 T = 2.23 |
O = 23 T = 3.75 (out)(err) |
O = 5 T = 2.23 (out)(err) |
file_rpms_wcnf_L3_V100_C600_H100_9.wcnf | O = 9 T = 2.87 |
O = 41 T = 1.04 (out)(err) |
O = 9 T = 2.87 (out)(err) |
file_rpms_wcnf_L3_V100_C700_H100_0.wcnf | O = 18 T = 2.61 |
O = 48 T = 2.82 (out)(err) |
O = 18 T = 2.61 (out)(err) |
file_rpms_wcnf_L3_V100_C700_H100_1.wcnf | O = 14 T = 3.23 |
O = 47 T = 4.43 (out)(err) |
O = 14 T = 3.23 (out)(err) |
file_rpms_wcnf_L3_V100_C700_H100_2.wcnf | O = 15 T = 3.78 |
O = 42 T = 4.98 (out)(err) |
O = 15 T = 3.78 (out)(err) |
file_rpms_wcnf_L3_V100_C700_H100_3.wcnf | O = 12 T = 3.10 |
O = 46 T = 5.28 (out)(err) |
O = 12 T = 3.10 (out)(err) |
file_rpms_wcnf_L3_V100_C700_H100_4.wcnf | O = 11 T = 3.98 |
O = 44 T = 6.46 (out)(err) |
O = 11 T = 3.98 (out)(err) |
file_rpms_wcnf_L3_V100_C700_H100_5.wcnf | O = 14 T = 4.58 |
O = 50 T = 5.20 (out)(err) |
O = 14 T = 4.58 (out)(err) |
file_rpms_wcnf_L3_V100_C700_H100_6.wcnf | O = 12 T = 3.46 |
O = 37 T = 3.68 (out)(err) |
O = 12 T = 3.46 (out)(err) |
file_rpms_wcnf_L3_V100_C700_H100_7.wcnf | O = 17 T = 3.45 |
O = 47 T = 4.56 (out)(err) |
O = 17 T = 3.45 (out)(err) |
file_rpms_wcnf_L3_V100_C700_H100_8.wcnf | O = 16 T = 2.97 |
O = 48 T = 5.76 (out)(err) |
O = 16 T = 2.97 (out)(err) |
file_rpms_wcnf_L3_V100_C700_H100_9.wcnf | O = 12 T = 3.51 |
O = 50 T = 5.31 (out)(err) |
O = 12 T = 3.51 (out)(err) |
file_rpms_wcnf_L3_V100_C800_H100_0.wcnf | O = 21 T = 4.22 |
O = 58 T = 3.57 (out)(err) |
O = 21 T = 4.22 (out)(err) |
file_rpms_wcnf_L3_V100_C800_H100_1.wcnf | O = 21 T = 3.97 |
O = 62 T = 3.82 (out)(err) |
O = 21 T = 3.97 (out)(err) |
file_rpms_wcnf_L3_V100_C800_H100_2.wcnf | O = 20 T = 0.48 |
O = 53 T = 2.44 (out)(err) |
O = 20 T = 0.48 (out)(err) |
file_rpms_wcnf_L3_V100_C800_H100_3.wcnf | O = 22 T = 4.13 |
O = 44 T = 4.53 (out)(err) |
O = 22 T = 4.13 (out)(err) |
file_rpms_wcnf_L3_V100_C800_H100_4.wcnf | O = 18 T = 0.42 |
O = 61 T = 5.46 (out)(err) |
O = 18 T = 0.42 (out)(err) |
file_rpms_wcnf_L3_V100_C800_H100_5.wcnf | O = 20 T = 3.33 |
O = 41 T = 8.57 (out)(err) |
O = 20 T = 3.33 (out)(err) |
file_rpms_wcnf_L3_V100_C800_H100_6.wcnf | O = 17 T = 3.48 |
O = 60 T = 4.78 (out)(err) |
O = 17 T = 3.48 (out)(err) |
file_rpms_wcnf_L3_V100_C800_H100_7.wcnf | O = 23 T = 4.03 |
O = 50 T = 2.21 (out)(err) |
O = 23 T = 4.03 (out)(err) |
file_rpms_wcnf_L3_V100_C800_H100_8.wcnf | O = 25 T = 3.41 |
O = 56 T = 1.94 (out)(err) |
O = 25 T = 3.41 (out)(err) |
file_rpms_wcnf_L3_V100_C800_H100_9.wcnf | O = 20 T = 3.72 |
O = 40 T = 4.97 (out)(err) |
O = 20 T = 3.72 (out)(err) |