| 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 |
|---|---|---|---|
| frb20-11-1.partial.wcnf | O = 200 T = 9.99 |
O = 204 T = 4.45 (out)(err) |
O = 200 T = 9.99 (out)(err) |
| frb20-11-2.partial.wcnf | O = 200 T = 8.86 |
O = 204 T = 5.06 (out)(err) |
O = 200 T = 8.86 (out)(err) |
| frb20-11-3.partial.wcnf | O = 200 T = 11.70 |
O = 204 T = 1.73 (out)(err) |
O = 200 T = 11.70 (out)(err) |
| frb20-11-4.partial.wcnf | O = 200 T = 54.04 |
O = 204 T = 24.42 (out)(err) |
O = 200 T = 54.04 (out)(err) |
| frb20-11-5.partial.wcnf | O = 200 T = 91.72 |
O = 204 T = 3.73 (out)(err) |
O = 200 T = 91.72 (out)(err) |
| frb25-13-1.partial.wcnf | O = 301 T = 54.52 |
O = 306 T = 4.08 (out)(err) |
O = 301 T = 54.52 (out)(err) |
| frb25-13-2.partial.wcnf | O = 301 T = 112.77 |
O = 305 T = 10.62 (out)(err) |
O = 301 T = 112.77 (out)(err) |
| frb25-13-3.partial.wcnf | O = 301 T = 29.34 |
O = 305 T = 2.27 (out)(err) |
O = 301 T = 29.34 (out)(err) |
| frb25-13-4.partial.wcnf | O = 301 T = 19.99 |
O = 306 T = 2.95 (out)(err) |
O = 301 T = 19.99 (out)(err) |
| frb25-13-5.partial.wcnf | O = 302 T = 14.26 |
O = 307 T = 2.08 (out)(err) |
O = 302 T = 14.26 (out)(err) |
| frb30-15-1.partial.wcnf | O = 423 T = 20.06 |
O = 426 T = 71.91 (out)(err) |
O = 423 T = 20.06 (out)(err) |
| frb30-15-2.partial.wcnf | O = 422 T = 199.41 |
O = 429 T = 4.56 (out)(err) |
O = 422 T = 199.41 (out)(err) |
| frb30-15-3.partial.wcnf | O = 423 T = 35.40 |
O = 426 T = 4.86 (out)(err) |
O = 423 T = 35.40 (out)(err) |
| frb30-15-4.partial.wcnf | O = 423 T = 19.14 |
O = 427 T = 5.94 (out)(err) |
O = 423 T = 19.14 (out)(err) |
| frb30-15-5.partial.wcnf | O = 423 T = 20.38 |
O = 426 T = 4.26 (out)(err) |
O = 423 T = 20.38 (out)(err) |
| frb35-17-1.partial.wcnf | O = 564 T = 192.58 |
O = 570 T = 4.01 (out)(err) |
O = 564 T = 192.58 (out)(err) |
| frb35-17-2.partial.wcnf | O = 565 T = 27.48 |
O = 568 T = 4.81 (out)(err) |
O = 565 T = 27.48 (out)(err) |
| frb35-17-3.partial.wcnf | O = 563 T = 105.62 |
O = 567 T = 4.12 (out)(err) |
O = 563 T = 105.62 (out)(err) |
| frb35-17-4.partial.wcnf | O = 565 T = 23.29 |
O = 566 T = 3.67 (out)(err) |
O = 565 T = 23.29 (out)(err) |
| frb35-17-5.partial.wcnf | O = 564 T = 128.80 |
O = 568 T = 4.74 (out)(err) |
O = 564 T = 128.80 (out)(err) |
| frb40-19-1.partial.wcnf | O = 726 T = 77.54 |
O = 730 T = 3.86 (out)(err) |
O = 726 T = 77.54 (out)(err) |
| frb40-19-2.partial.wcnf | O = 726 T = 138.49 |
O = 729 T = 5.23 (out)(err) |
O = 726 T = 138.49 (out)(err) |
| frb40-19-3.partial.wcnf | O = 726 T = 43.28 |
O = 731 T = 4.29 (out)(err) |
O = 726 T = 43.28 (out)(err) |
| frb40-19-4.partial.wcnf | O = 726 T = 236.79 |
O = 730 T = 5.20 (out)(err) |
O = 726 T = 236.79 (out)(err) |
| frb40-19-5.partial.wcnf | O = 726 T = 13.67 |
O = 730 T = 2.80 (out)(err) |
O = 726 T = 13.67 (out)(err) |
| ft10-808-1090.wcnf | O = 192 T = 287.41 |
O = 192 T = 287.41 (out)(err) |
O = 75844 T = 147.13 (out)(err) |
| la04-567-0696.wcnf | O = 23 T = 37.47 |
O = 23 T = 37.47 (out)(err) |
O = 130 T = 31.81 (out)(err) |
| orb08-894-1058.wcnf | O = 72 T = 282.46 |
O = 72 T = 282.46 (out)(err) |
O = 8745 T = 169.17 (out)(err) |
| max_clq_150-0-447-1.clq.wcnf | O = 147 T = 1.99 |
O = 147 T = 1.99 (out)(err) |
O = 147 T = 6.55 (out)(err) |
| max_clq_150-0-447-2.clq.wcnf | O = 147 T = 1.80 |
O = 147 T = 1.80 (out)(err) |
O = 147 T = 6.28 (out)(err) |
| max_clq_150-0-447-3.clq.wcnf | O = 147 T = 2.04 |
O = 147 T = 2.04 (out)(err) |
O = 147 T = 7.69 (out)(err) |
| max_clq_150-0-447-4.clq.wcnf | O = 147 T = 2.29 |
O = 147 T = 2.29 (out)(err) |
O = 147 T = 6.90 (out)(err) |
| max_clq_150-1-894-1.clq.wcnf | O = 146 T = 1.76 |
O = 146 T = 1.76 (out)(err) |
O = 146 T = 6.83 (out)(err) |
| max_clq_150-1-894-2.clq.wcnf | O = 146 T = 1.86 |
O = 146 T = 1.86 (out)(err) |
O = 146 T = 7.59 (out)(err) |
| max_clq_150-1-894-3.clq.wcnf | O = 146 T = 2.12 |
O = 146 T = 2.12 (out)(err) |
O = 146 T = 7.33 (out)(err) |
| max_clq_150-1-894-4.clq.wcnf | O = 146 T = 2.00 |
O = 146 T = 2.00 (out)(err) |
O = 146 T = 6.65 (out)(err) |
| max_clq_150-10-4917-1.clq.wcnf | O = 141 T = 5.84 |
O = 141 T = 35.04 (out)(err) |
O = 141 T = 5.84 (out)(err) |
| max_clq_150-10-4917-2.clq.wcnf | O = 141 T = 4.12 |
O = 141 T = 4.12 (out)(err) |
O = 141 T = 5.00 (out)(err) |
| max_clq_150-10-4917-3.clq.wcnf | O = 141 T = 1.32 |
O = 141 T = 13.53 (out)(err) |
O = 141 T = 1.32 (out)(err) |
| max_clq_150-10-4917-4.clq.wcnf | O = 141 T = 8.11 |
O = 141 T = 22.90 (out)(err) |
O = 141 T = 8.11 (out)(err) |
| max_clq_150-11-5364-1.clq.wcnf | O = 140 T = 6.88 |
O = 140 T = 12.77 (out)(err) |
O = 140 T = 6.88 (out)(err) |
| max_clq_150-11-5364-2.clq.wcnf | O = 141 T = 2.79 |
O = 141 T = 2.79 (out)(err) |
O = 141 T = 6.26 (out)(err) |
| max_clq_150-11-5364-3.clq.wcnf | O = 140 T = 7.89 |
O = 140 T = 12.00 (out)(err) |
O = 140 T = 7.89 (out)(err) |
| max_clq_150-11-5364-4.clq.wcnf | O = 140 T = 1.47 |
O = 140 T = 25.22 (out)(err) |
O = 140 T = 1.47 (out)(err) |
| max_clq_150-12-5811-1.clq.wcnf | O = 140 T = 1.47 |
O = 140 T = 1.47 (out)(err) |
O = 140 T = 6.28 (out)(err) |
| max_clq_150-12-5811-2.clq.wcnf | O = 140 T = 4.84 |
O = 140 T = 4.84 (out)(err) |
O = 140 T = 6.62 (out)(err) |
| max_clq_150-12-5811-3.clq.wcnf | O = 139 T = 4.23 |
O = 139 T = 90.67 (out)(err) |
O = 139 T = 4.23 (out)(err) |
| max_clq_150-12-5811-4.clq.wcnf | O = 140 T = 4.44 |
O = 140 T = 4.44 (out)(err) |
O = 140 T = 5.13 (out)(err) |
| max_clq_150-13-6258-1.clq.wcnf | O = 138 T = 5.65 |
O = 138 T = 55.44 (out)(err) |
O = 138 T = 5.65 (out)(err) |
| max_clq_150-13-6258-2.clq.wcnf | O = 139 T = 4.54 |
O = 139 T = 5.58 (out)(err) |
O = 139 T = 4.54 (out)(err) |
| max_clq_150-13-6258-3.clq.wcnf | O = 138 T = 3.69 |
O = 138 T = 22.30 (out)(err) |
O = 138 T = 3.69 (out)(err) |
| max_clq_150-13-6258-4.clq.wcnf | O = 138 T = 4.81 |
O = 138 T = 4.81 (out)(err) |
O = 138 T = 5.95 (out)(err) |
| max_clq_150-14-6705-1.clq.wcnf | O = 138 T = 7.04 |
O = 138 T = 23.23 (out)(err) |
O = 138 T = 7.04 (out)(err) |
| max_clq_150-14-6705-2.clq.wcnf | O = 137 T = 5.10 |
O = 138 T = 59.77 (out)(err) |
O = 137 T = 5.10 (out)(err) |
| max_clq_150-14-6705-3.clq.wcnf | O = 137 T = 4.29 |
O = 137 T = 247.09 (out)(err) |
O = 137 T = 4.29 (out)(err) |
| max_clq_150-14-6705-4.clq.wcnf | O = 137 T = 0.70 |
O = 138 T = 5.41 (out)(err) |
O = 137 T = 0.70 (out)(err) |
| max_clq_150-15-7152-1.clq.wcnf | O = 135 T = 6.60 |
O = 136 T = 48.70 (out)(err) |
O = 135 T = 6.60 (out)(err) |
| max_clq_150-15-7152-2.clq.wcnf | O = 136 T = 7.60 |
O = 137 T = 45.91 (out)(err) |
O = 136 T = 7.60 (out)(err) |
| max_clq_150-15-7152-3.clq.wcnf | O = 135 T = 1.57 |
O = 136 T = 183.72 (out)(err) |
O = 135 T = 1.57 (out)(err) |
| max_clq_150-15-7152-4.clq.wcnf | O = 136 T = 6.09 |
O = 137 T = 32.98 (out)(err) |
O = 136 T = 6.09 (out)(err) |
| max_clq_150-16-7599-1.clq.wcnf | O = 134 T = 5.86 |
O = 136 T = 62.93 (out)(err) |
O = 134 T = 5.86 (out)(err) |
| max_clq_150-16-7599-2.clq.wcnf | O = 135 T = 0.64 |
O = 136 T = 2.30 (out)(err) |
O = 135 T = 0.64 (out)(err) |
| max_clq_150-16-7599-3.clq.wcnf | O = 134 T = 3.55 |
O = 135 T = 191.30 (out)(err) |
O = 134 T = 3.55 (out)(err) |
| max_clq_150-16-7599-4.clq.wcnf | O = 135 T = 3.03 |
O = 135 T = 275.83 (out)(err) |
O = 135 T = 3.03 (out)(err) |
| max_clq_150-17-8046-1.clq.wcnf | O = 132 T = 2.04 |
O = 134 T = 4.62 (out)(err) |
O = 132 T = 2.04 (out)(err) |
| max_clq_150-17-8046-2.clq.wcnf | O = 133 T = 6.44 |
O = 134 T = 4.98 (out)(err) |
O = 133 T = 6.44 (out)(err) |
| max_clq_150-17-8046-3.clq.wcnf | O = 132 T = 5.74 |
O = 134 T = 130.86 (out)(err) |
O = 132 T = 5.74 (out)(err) |
| max_clq_150-17-8046-4.clq.wcnf | O = 132 T = 5.35 |
O = 134 T = 95.03 (out)(err) |
O = 132 T = 5.35 (out)(err) |
| max_clq_150-18-8493-1.clq.wcnf | O = 130 T = 7.04 |
O = 133 T = 4.72 (out)(err) |
O = 130 T = 7.04 (out)(err) |
| max_clq_150-18-8493-2.clq.wcnf | O = 130 T = 5.26 |
O = 132 T = 8.79 (out)(err) |
O = 130 T = 5.26 (out)(err) |
| max_clq_150-18-8493-3.clq.wcnf | O = 129 T = 8.94 |
O = 133 T = 5.18 (out)(err) |
O = 129 T = 8.94 (out)(err) |
| max_clq_150-18-8493-4.clq.wcnf | O = 129 T = 5.97 |
O = 133 T = 149.51 (out)(err) |
O = 129 T = 5.97 (out)(err) |
| max_clq_150-19-8940-1.clq.wcnf | O = 127 T = 5.87 |
O = 132 T = 2.44 (out)(err) |
O = 127 T = 5.87 (out)(err) |
| max_clq_150-19-8940-2.clq.wcnf | O = 126 T = 5.22 |
O = 130 T = 24.28 (out)(err) |
O = 126 T = 5.22 (out)(err) |
| max_clq_150-19-8940-3.clq.wcnf | O = 127 T = 2.79 |
O = 131 T = 11.40 (out)(err) |
O = 127 T = 2.79 (out)(err) |
| max_clq_150-19-8940-4.clq.wcnf | O = 127 T = 11.24 |
O = 132 T = 1.41 (out)(err) |
O = 127 T = 11.24 (out)(err) |
| max_clq_150-2-1341-1.clq.wcnf | O = 146 T = 1.79 |
O = 146 T = 1.79 (out)(err) |
O = 146 T = 8.36 (out)(err) |
| max_clq_150-2-1341-2.clq.wcnf | O = 146 T = 1.73 |
O = 146 T = 1.73 (out)(err) |
O = 146 T = 3.83 (out)(err) |
| max_clq_150-2-1341-3.clq.wcnf | O = 146 T = 2.55 |
O = 146 T = 2.55 (out)(err) |
O = 146 T = 7.92 (out)(err) |
| max_clq_150-2-1341-4.clq.wcnf | O = 145 T = 1.93 |
O = 145 T = 1.93 (out)(err) |
O = 145 T = 6.22 (out)(err) |
| max_clq_150-20-9387-1.clq.wcnf | O = 123 T = 5.64 |
O = 129 T = 4.81 (out)(err) |
O = 123 T = 5.64 (out)(err) |
| max_clq_150-20-9387-2.clq.wcnf | O = 124 T = 5.10 |
O = 129 T = 4.23 (out)(err) |
O = 124 T = 5.10 (out)(err) |
| max_clq_150-20-9387-3.clq.wcnf | O = 123 T = 5.28 |
O = 127 T = 12.86 (out)(err) |
O = 123 T = 5.28 (out)(err) |
| max_clq_150-20-9387-4.clq.wcnf | O = 123 T = 4.83 |
O = 127 T = 2.00 (out)(err) |
O = 123 T = 4.83 (out)(err) |
| max_clq_150-21-9834-1.clq.wcnf | O = 117 T = 4.56 |
O = 123 T = 2.73 (out)(err) |
O = 117 T = 4.56 (out)(err) |
| max_clq_150-21-9834-2.clq.wcnf | O = 118 T = 5.60 |
O = 119 T = 287.14 (out)(err) |
O = 118 T = 5.60 (out)(err) |
| max_clq_150-21-9834-3.clq.wcnf | O = 116 T = 14.59 |
O = 127 T = 3.39 (out)(err) |
O = 116 T = 14.59 (out)(err) |
| max_clq_150-21-9834-4.clq.wcnf | O = 118 T = 5.73 |
O = 123 T = 5.26 (out)(err) |
O = 118 T = 5.73 (out)(err) |
| max_clq_150-22-10281-1.clq.wcnf | O = 108 T = 18.47 |
O = 115 T = 5.84 (out)(err) |
O = 108 T = 18.47 (out)(err) |
| max_clq_150-22-10281-2.clq.wcnf | O = 107 T = 55.11 |
O = 117 T = 3.89 (out)(err) |
O = 107 T = 55.11 (out)(err) |
| max_clq_150-22-10281-3.clq.wcnf | O = 108 T = 69.13 |
O = 114 T = 3.64 (out)(err) |
O = 108 T = 69.13 (out)(err) |
| max_clq_150-22-10281-4.clq.wcnf | O = 108 T = 10.36 |
O = 114 T = 2.08 (out)(err) |
O = 108 T = 10.36 (out)(err) |
| max_clq_150-23-10728-1.clq.wcnf | O = 91 T = 5.82 |
O = 102 T = 3.63 (out)(err) |
O = 91 T = 5.82 (out)(err) |
| max_clq_150-23-10728-2.clq.wcnf | O = 89 T = 5.50 |
O = 104 T = 5.87 (out)(err) |
O = 89 T = 5.50 (out)(err) |
| max_clq_150-23-10728-3.clq.wcnf | O = 92 T = 4.17 |
O = 98 T = 5.50 (out)(err) |
O = 92 T = 4.17 (out)(err) |
| max_clq_150-23-10728-4.clq.wcnf | O = 90 T = 4.70 |
O = 101 T = 4.76 (out)(err) |
O = 90 T = 4.70 (out)(err) |
| max_clq_150-3-1788-1.clq.wcnf | O = 145 T = 1.85 |
O = 145 T = 1.85 (out)(err) |
O = 145 T = 7.17 (out)(err) |
| max_clq_150-3-1788-2.clq.wcnf | O = 145 T = 1.85 |
O = 145 T = 1.85 (out)(err) |
O = 145 T = 7.08 (out)(err) |
| max_clq_150-3-1788-3.clq.wcnf | O = 145 T = 2.03 |
O = 145 T = 2.03 (out)(err) |
O = 145 T = 7.97 (out)(err) |
| max_clq_150-3-1788-4.clq.wcnf | O = 145 T = 1.81 |
O = 145 T = 1.81 (out)(err) |
O = 145 T = 7.53 (out)(err) |
| max_clq_150-4-2235-1.clq.wcnf | O = 144 T = 1.99 |
O = 144 T = 1.99 (out)(err) |
O = 144 T = 6.90 (out)(err) |
| max_clq_150-4-2235-2.clq.wcnf | O = 145 T = 2.32 |
O = 145 T = 2.32 (out)(err) |
O = 145 T = 6.74 (out)(err) |
| max_clq_150-4-2235-3.clq.wcnf | O = 144 T = 2.71 |
O = 144 T = 2.71 (out)(err) |
O = 144 T = 7.38 (out)(err) |
| max_clq_150-4-2235-4.clq.wcnf | O = 145 T = 2.40 |
O = 145 T = 2.40 (out)(err) |
O = 145 T = 5.37 (out)(err) |
| max_clq_150-5-2682-1.clq.wcnf | O = 144 T = 2.81 |
O = 144 T = 2.81 (out)(err) |
O = 144 T = 6.46 (out)(err) |
| max_clq_150-5-2682-2.clq.wcnf | O = 144 T = 2.20 |
O = 144 T = 2.20 (out)(err) |
O = 144 T = 7.12 (out)(err) |
| max_clq_150-5-2682-3.clq.wcnf | O = 144 T = 2.89 |
O = 144 T = 2.89 (out)(err) |
O = 144 T = 7.97 (out)(err) |
| max_clq_150-5-2682-4.clq.wcnf | O = 144 T = 2.42 |
O = 144 T = 2.42 (out)(err) |
O = 144 T = 4.13 (out)(err) |
| max_clq_150-6-3129-1.clq.wcnf | O = 144 T = 3.41 |
O = 144 T = 3.94 (out)(err) |
O = 144 T = 3.41 (out)(err) |
| max_clq_150-6-3129-2.clq.wcnf | O = 143 T = 4.17 |
O = 143 T = 4.17 (out)(err) |
O = 143 T = 6.74 (out)(err) |
| max_clq_150-6-3129-3.clq.wcnf | O = 143 T = 2.39 |
O = 143 T = 2.39 (out)(err) |
O = 143 T = 4.15 (out)(err) |
| max_clq_150-6-3129-4.clq.wcnf | O = 144 T = 4.06 |
O = 144 T = 4.06 (out)(err) |
O = 144 T = 6.25 (out)(err) |
| max_clq_150-7-3576-1.clq.wcnf | O = 144 T = 1.83 |
O = 144 T = 1.83 (out)(err) |
O = 144 T = 6.36 (out)(err) |
| max_clq_150-7-3576-2.clq.wcnf | O = 143 T = 1.12 |
O = 143 T = 1.81 (out)(err) |
O = 143 T = 1.12 (out)(err) |
| max_clq_150-7-3576-3.clq.wcnf | O = 143 T = 5.68 |
O = 143 T = 5.68 (out)(err) |
O = 143 T = 5.88 (out)(err) |
| max_clq_150-7-3576-4.clq.wcnf | O = 143 T = 1.42 |
O = 143 T = 4.52 (out)(err) |
O = 143 T = 1.42 (out)(err) |
| max_clq_150-8-4023-1.clq.wcnf | O = 143 T = 3.59 |
O = 143 T = 4.40 (out)(err) |
O = 143 T = 3.59 (out)(err) |
| max_clq_150-8-4023-2.clq.wcnf | O = 142 T = 4.63 |
O = 142 T = 4.63 (out)(err) |
O = 142 T = 6.93 (out)(err) |
| max_clq_150-8-4023-3.clq.wcnf | O = 143 T = 4.88 |
O = 143 T = 4.88 (out)(err) |
O = 143 T = 6.68 (out)(err) |
| max_clq_150-8-4023-4.clq.wcnf | O = 142 T = 5.11 |
O = 142 T = 5.11 (out)(err) |
O = 142 T = 5.68 (out)(err) |
| max_clq_150-9-4470-1.clq.wcnf | O = 142 T = 5.26 |
O = 142 T = 5.61 (out)(err) |
O = 142 T = 5.26 (out)(err) |
| max_clq_150-9-4470-2.clq.wcnf | O = 142 T = 6.55 |
O = 142 T = 6.55 (out)(err) |
O = 142 T = 6.72 (out)(err) |
| max_clq_150-9-4470-3.clq.wcnf | O = 142 T = 4.54 |
O = 142 T = 4.54 (out)(err) |
O = 142 T = 7.00 (out)(err) |
| max_clq_150-9-4470-4.clq.wcnf | O = 142 T = 0.65 |
O = 142 T = 4.57 (out)(err) |
O = 142 T = 0.65 (out)(err) |
| MANN_a27.clq.wcnf | O = 253 T = 4.01 |
O = 253 T = 4.01 (out)(err) |
O = 253 T = 8.77 (out)(err) |
| MANN_a45.clq.wcnf | O = 694 T = 20.29 |
O = 695 T = 3.13 (out)(err) |
O = 694 T = 20.29 (out)(err) |
| MANN_a81.clq.wcnf | O = 2225 T = 4.85 |
O = 2225 T = 4.85 (out)(err) |
O = 2237 T = 176.67 (out)(err) |
| MANN_a9.clq.wcnf | O = 29 T = 0.14 |
O = 29 T = 1.86 (out)(err) |
O = 29 T = 0.14 (out)(err) |
| brock200_1.clq.wcnf | O = 179 T = 8.62 |
O = 182 T = 29.42 (out)(err) |
O = 179 T = 8.62 (out)(err) |
| brock200_2.clq.wcnf | O = 188 T = 7.76 |
O = 190 T = 5.71 (out)(err) |
O = 188 T = 7.76 (out)(err) |
| brock200_3.clq.wcnf | O = 185 T = 9.05 |
O = 188 T = 3.73 (out)(err) |
O = 185 T = 9.05 (out)(err) |
| brock200_4.clq.wcnf | O = 183 T = 22.18 |
O = 187 T = 4.36 (out)(err) |
O = 183 T = 22.18 (out)(err) |
| brock400_1.clq.wcnf | O = 376 T = 18.21 |
O = 382 T = 5.06 (out)(err) |
O = 376 T = 18.21 (out)(err) |
| brock400_2.clq.wcnf | O = 377 T = 16.36 |
O = 382 T = 132.14 (out)(err) |
O = 377 T = 16.36 (out)(err) |
| brock400_3.clq.wcnf | O = 376 T = 98.25 |
O = 382 T = 6.66 (out)(err) |
O = 376 T = 98.25 (out)(err) |
| brock400_4.clq.wcnf | O = 367 T = 81.36 |
O = 380 T = 4.20 (out)(err) |
O = 367 T = 81.36 (out)(err) |
| brock800_1.clq.wcnf | O = 781 T = 182.18 |
O = 784 T = 4.22 (out)(err) |
O = 781 T = 182.18 (out)(err) |
| brock800_2.clq.wcnf | O = 781 T = 42.91 |
O = 784 T = 87.00 (out)(err) |
O = 781 T = 42.91 (out)(err) |
| brock800_3.clq.wcnf | O = 782 T = 40.68 |
O = 783 T = 2.48 (out)(err) |
O = 782 T = 40.68 (out)(err) |
| brock800_4.clq.wcnf | O = 782 T = 42.04 |
O = 784 T = 2.75 (out)(err) |
O = 782 T = 42.04 (out)(err) |
| c-fat200-1.clq.wcnf | O = 188 T = 2.39 |
O = 188 T = 2.39 (out)(err) |
O = 188 T = 8.02 (out)(err) |
| c-fat200-2.clq.wcnf | O = 176 T = 2.95 |
O = 176 T = 2.95 (out)(err) |
O = 176 T = 9.46 (out)(err) |
| c-fat200-5.clq.wcnf | O = 142 T = 2.15 |
O = 142 T = 2.15 (out)(err) |
O = 142 T = 8.36 (out)(err) |
| c-fat500-1.clq.wcnf | O = 486 T = 2.19 |
O = 486 T = 2.19 (out)(err) |
O = 486 T = 15.08 (out)(err) |
| c-fat500-10.clq.wcnf | O = 374 T = 3.02 |
O = 374 T = 3.02 (out)(err) |
O = 374 T = 25.46 (out)(err) |
| c-fat500-2.clq.wcnf | O = 474 T = 2.90 |
O = 474 T = 2.90 (out)(err) |
O = 474 T = 25.89 (out)(err) |
| c-fat500-5.clq.wcnf | O = 436 T = 1.85 |
O = 436 T = 1.85 (out)(err) |
O = 436 T = 5.70 (out)(err) |
| hamming10-2.clq.wcnf | O = 512 T = 5.01 |
O = 512 T = 5.01 (out)(err) |
O = 512 T = 60.23 (out)(err) |
| hamming10-4.clq.wcnf | O = 990 T = 167.61 |
O = 996 T = 3.95 (out)(err) |
O = 990 T = 167.61 (out)(err) |
| hamming6-2.clq.wcnf | O = 32 T = 2.28 |
O = 32 T = 2.28 (out)(err) |
O = 32 T = 2.77 (out)(err) |
| hamming6-4.clq.wcnf | O = 60 T = 0.52 |
O = 60 T = 0.52 (out)(err) |
O = 60 T = 3.05 (out)(err) |
| hamming8-2.clq.wcnf | O = 128 T = 3.50 |
O = 128 T = 3.50 (out)(err) |
O = 128 T = 13.13 (out)(err) |
| hamming8-4.clq.wcnf | O = 240 T = 3.66 |
O = 240 T = 3.66 (out)(err) |
O = 240 T = 10.74 (out)(err) |
| johnson16-2-4.clq.wcnf | O = 112 T = 0.55 |
O = 112 T = 0.55 (out)(err) |
O = 112 T = 3.50 (out)(err) |
| johnson32-2-4.clq.wcnf | O = 480 T = 3.85 |
O = 480 T = 3.85 (out)(err) |
O = 480 T = 20.58 (out)(err) |
| johnson8-2-4.clq.wcnf | O = 24 T = 0.51 |
O = 24 T = 0.51 (out)(err) |
O = 24 T = 1.68 (out)(err) |
| johnson8-4-4.clq.wcnf | O = 56 T = 2.24 |
O = 56 T = 4.45 (out)(err) |
O = 56 T = 2.24 (out)(err) |
| keller4.clq.wcnf | O = 160 T = 1.06 |
O = 160 T = 145.18 (out)(err) |
O = 160 T = 1.06 (out)(err) |
| keller5.clq.wcnf | O = 753 T = 195.95 |
O = 756 T = 3.93 (out)(err) |
O = 753 T = 195.95 (out)(err) |
| p_hat1000-1.clq.wcnf | O = 990 T = 97.83 |
O = 991 T = 147.67 (out)(err) |
O = 990 T = 97.83 (out)(err) |
| p_hat1000-2.clq.wcnf | O = 957 T = 123.05 |
O = 973 T = 15.60 (out)(err) |
O = 957 T = 123.05 (out)(err) |
| p_hat1000-3.clq.wcnf | O = 941 T = 88.46 |
O = 963 T = 4.13 (out)(err) |
O = 941 T = 88.46 (out)(err) |
| p_hat300-1.clq.wcnf | O = 292 T = 5.72 |
O = 292 T = 5.72 (out)(err) |
O = 292 T = 15.15 (out)(err) |
| p_hat300-2.clq.wcnf | O = 275 T = 12.71 |
O = 280 T = 122.13 (out)(err) |
O = 275 T = 12.71 (out)(err) |
| p_hat300-3.clq.wcnf | O = 264 T = 12.39 |
O = 275 T = 45.29 (out)(err) |
O = 264 T = 12.39 (out)(err) |
| p_hat500-1.clq.wcnf | O = 491 T = 3.23 |
O = 491 T = 3.23 (out)(err) |
O = 491 T = 20.85 (out)(err) |
| p_hat500-2.clq.wcnf | O = 465 T = 16.69 |
O = 474 T = 12.93 (out)(err) |
O = 465 T = 16.69 (out)(err) |
| p_hat500-3.clq.wcnf | O = 452 T = 90.94 |
O = 464 T = 5.26 (out)(err) |
O = 452 T = 90.94 (out)(err) |
| p_hat700-1.clq.wcnf | O = 689 T = 182.26 |
O = 691 T = 251.01 (out)(err) |
O = 689 T = 182.26 (out)(err) |
| p_hat700-2.clq.wcnf | O = 659 T = 72.98 |
O = 675 T = 287.99 (out)(err) |
O = 659 T = 72.98 (out)(err) |
| p_hat700-3.clq.wcnf | O = 643 T = 103.87 |
O = 665 T = 3.83 (out)(err) |
O = 643 T = 103.87 (out)(err) |
| san1000.clq.wcnf | O = 991 T = 17.83 |
O = 992 T = 51.83 (out)(err) |
O = 991 T = 17.83 (out)(err) |
| san200_0.7_1.clq.wcnf | O = 170 T = 7.72 |
O = 185 T = 3.94 (out)(err) |
O = 170 T = 7.72 (out)(err) |
| san200_0.7_2.clq.wcnf | O = 182 T = 31.26 |
O = 187 T = 253.79 (out)(err) |
O = 182 T = 31.26 (out)(err) |
| san200_0.9_1.clq.wcnf | O = 130 T = 6.97 |
O = 161 T = 3.98 (out)(err) |
O = 130 T = 6.97 (out)(err) |
| san200_0.9_2.clq.wcnf | O = 140 T = 3.11 |
O = 169 T = 3.35 (out)(err) |
O = 140 T = 3.11 (out)(err) |
| san200_0.9_3.clq.wcnf | O = 156 T = 81.70 |
O = 174 T = 3.97 (out)(err) |
O = 156 T = 81.70 (out)(err) |
| san400_0.5_1.clq.wcnf | O = 387 T = 152.11 |
O = 393 T = 1.74 (out)(err) |
O = 387 T = 152.11 (out)(err) |
| san400_0.7_1.clq.wcnf | O = 360 T = 73.30 |
O = 380 T = 2.01 (out)(err) |
O = 360 T = 73.30 (out)(err) |
| san400_0.7_2.clq.wcnf | O = 380 T = 221.13 |
O = 384 T = 2.22 (out)(err) |
O = 380 T = 221.13 (out)(err) |
| san400_0.7_3.clq.wcnf | O = 384 T = 8.38 |
O = 384 T = 8.38 (out)(err) |
O = 384 T = 17.28 (out)(err) |
| san400_0.9_1.clq.wcnf | O = 300 T = 48.20 |
O = 357 T = 4.15 (out)(err) |
O = 300 T = 48.20 (out)(err) |
| sanr200_0.7.clq.wcnf | O = 182 T = 7.51 |
O = 184 T = 3.87 (out)(err) |
O = 182 T = 7.51 (out)(err) |
| sanr200_0.9.clq.wcnf | O = 158 T = 10.59 |
O = 170 T = 3.89 (out)(err) |
O = 158 T = 10.59 (out)(err) |
| sanr400_0.5.clq.wcnf | O = 387 T = 14.35 |
O = 389 T = 4.55 (out)(err) |
O = 387 T = 14.35 (out)(err) |
| sanr400_0.7.clq.wcnf | O = 379 T = 61.33 |
O = 383 T = 16.93 (out)(err) |
O = 379 T = 61.33 (out)(err) |
| cnf3.150.250.832706.cnf.wcnf | O = 15 T = 5.59 |
O = 15 T = 28.86 (out)(err) |
O = 15 T = 5.59 (out)(err) |
| cnf3.150.250.832707.cnf.wcnf | O = 18 T = 6.08 |
O = 21 T = 30.06 (out)(err) |
O = 18 T = 6.08 (out)(err) |
| cnf3.150.250.832708.cnf.wcnf | O = 20 T = 6.87 |
O = 27 T = 60.61 (out)(err) |
O = 20 T = 6.87 (out)(err) |
| cnf3.150.250.832709.cnf.wcnf | O = 24 T = 6.74 |
O = 28 T = 42.43 (out)(err) |
O = 24 T = 6.74 (out)(err) |
| cnf3.150.250.832710.cnf.wcnf | O = 24 T = 5.68 |
O = 32 T = 0.47 (out)(err) |
O = 24 T = 5.68 (out)(err) |
| cnf3.150.250.832711.cnf.wcnf | O = 20 T = 5.28 |
O = 23 T = 4.24 (out)(err) |
O = 20 T = 5.28 (out)(err) |
| cnf3.150.250.832712.cnf.wcnf | O = 23 T = 6.36 |
O = 24 T = 177.52 (out)(err) |
O = 23 T = 6.36 (out)(err) |
| cnf3.150.250.832713.cnf.wcnf | O = 16 T = 5.80 |
O = 16 T = 286.48 (out)(err) |
O = 16 T = 5.80 (out)(err) |
| cnf3.150.250.832714.cnf.wcnf | O = 23 T = 7.45 |
O = 27 T = 32.79 (out)(err) |
O = 23 T = 7.45 (out)(err) |
| cnf3.150.250.832715.cnf.wcnf | O = 24 T = 4.81 |
O = 28 T = 5.55 (out)(err) |
O = 24 T = 4.81 (out)(err) |
| cnf3.150.300.195561.cnf.wcnf | O = 22 T = 4.95 |
O = 24 T = 4.24 (out)(err) |
O = 22 T = 4.95 (out)(err) |
| cnf3.150.300.195562.cnf.wcnf | O = 22 T = 6.93 |
O = 23 T = 257.59 (out)(err) |
O = 22 T = 6.93 (out)(err) |
| cnf3.150.300.195563.cnf.wcnf | O = 20 T = 5.83 |
O = 22 T = 3.41 (out)(err) |
O = 20 T = 5.83 (out)(err) |
| cnf3.150.300.195564.cnf.wcnf | O = 26 T = 0.39 |
O = 30 T = 15.77 (out)(err) |
O = 26 T = 0.39 (out)(err) |
| cnf3.150.300.195565.cnf.wcnf | O = 27 T = 5.13 |
O = 36 T = 121.31 (out)(err) |
O = 27 T = 5.13 (out)(err) |
| cnf3.150.300.195566.cnf.wcnf | O = 21 T = 7.43 |
O = 30 T = 0.81 (out)(err) |
O = 21 T = 7.43 (out)(err) |
| cnf3.150.300.195567.cnf.wcnf | O = 26 T = 5.62 |
O = 38 T = 3.19 (out)(err) |
O = 26 T = 5.62 (out)(err) |
| cnf3.150.300.195568.cnf.wcnf | O = 25 T = 4.87 |
O = 28 T = 215.18 (out)(err) |
O = 25 T = 4.87 (out)(err) |
| cnf3.150.300.195569.cnf.wcnf | O = 27 T = 5.26 |
O = 29 T = 68.79 (out)(err) |
O = 27 T = 5.26 (out)(err) |
| cnf3.150.300.195570.cnf.wcnf | O = 20 T = 5.40 |
O = 20 T = 64.48 (out)(err) |
O = 20 T = 5.40 (out)(err) |
| cnf3.150.350.558416.cnf.wcnf | O = 32 T = 5.82 |
O = 41 T = 150.99 (out)(err) |
O = 32 T = 5.82 (out)(err) |
| cnf3.150.350.558417.cnf.wcnf | O = 30 T = 5.35 |
O = 32 T = 185.04 (out)(err) |
O = 30 T = 5.35 (out)(err) |
| cnf3.150.350.558418.cnf.wcnf | O = 29 T = 4.62 |
O = 41 T = 64.30 (out)(err) |
O = 29 T = 4.62 (out)(err) |
| cnf3.150.350.558419.cnf.wcnf | O = 29 T = 5.34 |
O = 35 T = 268.41 (out)(err) |
O = 29 T = 5.34 (out)(err) |
| cnf3.150.350.558420.cnf.wcnf | O = 32 T = 5.21 |
O = 38 T = 4.92 (out)(err) |
O = 32 T = 5.21 (out)(err) |
| cnf3.150.350.558421.cnf.wcnf | O = 30 T = 6.14 |
O = 34 T = 130.85 (out)(err) |
O = 30 T = 6.14 (out)(err) |
| cnf3.150.350.558422.cnf.wcnf | O = 30 T = 5.58 |
O = 38 T = 4.96 (out)(err) |
O = 30 T = 5.58 (out)(err) |
| cnf3.150.350.558423.cnf.wcnf | O = 26 T = 6.65 |
O = 33 T = 6.76 (out)(err) |
O = 26 T = 6.65 (out)(err) |
| cnf3.150.350.558424.cnf.wcnf | O = 24 T = 4.70 |
O = 27 T = 149.79 (out)(err) |
O = 24 T = 4.70 (out)(err) |
| cnf3.150.350.558425.cnf.wcnf | O = 27 T = 0.56 |
O = 34 T = 231.67 (out)(err) |
O = 27 T = 0.56 (out)(err) |
| cnf3.150.400.921271.cnf.wcnf | O = 38 T = 6.82 |
O = 42 T = 112.71 (out)(err) |
O = 38 T = 6.82 (out)(err) |
| cnf3.150.400.921272.cnf.wcnf | O = 33 T = 7.33 |
O = 34 T = 5.13 (out)(err) |
O = 33 T = 7.33 (out)(err) |
| cnf3.150.400.921273.cnf.wcnf | O = 31 T = 5.72 |
O = 36 T = 7.37 (out)(err) |
O = 31 T = 5.72 (out)(err) |
| cnf3.150.400.921274.cnf.wcnf | O = 34 T = 5.44 |
O = 35 T = 129.67 (out)(err) |
O = 34 T = 5.44 (out)(err) |
| cnf3.150.400.921275.cnf.wcnf | O = 37 T = 5.85 |
O = 48 T = 2.78 (out)(err) |
O = 37 T = 5.85 (out)(err) |
| cnf3.150.400.921276.cnf.wcnf | O = 34 T = 5.28 |
O = 38 T = 6.20 (out)(err) |
O = 34 T = 5.28 (out)(err) |
| cnf3.150.400.921277.cnf.wcnf | O = 33 T = 6.84 |
O = 38 T = 5.66 (out)(err) |
O = 33 T = 6.84 (out)(err) |
| cnf3.150.400.921278.cnf.wcnf | O = 31 T = 4.70 |
O = 35 T = 5.46 (out)(err) |
O = 31 T = 4.70 (out)(err) |
| cnf3.150.400.921279.cnf.wcnf | O = 28 T = 4.21 |
O = 31 T = 268.96 (out)(err) |
O = 28 T = 4.21 (out)(err) |
| cnf3.150.400.921280.cnf.wcnf | O = 30 T = 7.18 |
O = 41 T = 34.50 (out)(err) |
O = 30 T = 7.18 (out)(err) |
| cnf3.150.450.284126.cnf.wcnf | O = 43 T = 8.37 |
O = 44 T = 138.88 (out)(err) |
O = 43 T = 8.37 (out)(err) |
| cnf3.150.450.284127.cnf.wcnf | O = 34 T = 6.89 |
O = 34 T = 271.75 (out)(err) |
O = 34 T = 6.89 (out)(err) |
| cnf3.150.450.284128.cnf.wcnf | O = 34 T = 9.33 |
O = 36 T = 73.83 (out)(err) |
O = 34 T = 9.33 (out)(err) |
| cnf3.150.450.284129.cnf.wcnf | O = 33 T = 5.62 |
O = 34 T = 219.21 (out)(err) |
O = 33 T = 5.62 (out)(err) |
| cnf3.150.450.284130.cnf.wcnf | O = 36 T = 1.08 |
O = 42 T = 14.20 (out)(err) |
O = 36 T = 1.08 (out)(err) |
| cnf3.150.450.284131.cnf.wcnf | O = 31 T = 7.00 |
O = 38 T = 21.20 (out)(err) |
O = 31 T = 7.00 (out)(err) |
| cnf3.150.450.284132.cnf.wcnf | O = 31 T = 7.09 |
O = 36 T = 104.69 (out)(err) |
O = 31 T = 7.09 (out)(err) |
| cnf3.150.450.284133.cnf.wcnf | O = 39 T = 7.33 |
O = 41 T = 5.84 (out)(err) |
O = 39 T = 7.33 (out)(err) |
| cnf3.150.450.284134.cnf.wcnf | O = 39 T = 4.93 |
O = 42 T = 141.57 (out)(err) |
O = 39 T = 4.93 (out)(err) |
| cnf3.150.450.284135.cnf.wcnf | O = 35 T = 5.82 |
O = 42 T = 4.09 (out)(err) |
O = 35 T = 5.82 (out)(err) |
| cnf3.150.500.646981.cnf.wcnf | O = 47 T = 6.35 |
O = 47 T = 37.89 (out)(err) |
O = 47 T = 6.35 (out)(err) |
| cnf3.150.500.646982.cnf.wcnf | O = 46 T = 6.82 |
O = 46 T = 38.22 (out)(err) |
O = 46 T = 6.82 (out)(err) |
| cnf3.150.500.646983.cnf.wcnf | O = 47 T = 6.13 |
O = 48 T = 101.39 (out)(err) |
O = 47 T = 6.13 (out)(err) |
| cnf3.150.500.646984.cnf.wcnf | O = 42 T = 6.72 |
O = 42 T = 17.61 (out)(err) |
O = 42 T = 6.72 (out)(err) |
| cnf3.150.500.646985.cnf.wcnf | O = 53 T = 7.37 |
O = 53 T = 29.49 (out)(err) |
O = 53 T = 7.37 (out)(err) |
| cnf3.150.500.646986.cnf.wcnf | O = 47 T = 6.49 |
O = 47 T = 23.45 (out)(err) |
O = 47 T = 6.49 (out)(err) |
| cnf3.150.500.646987.cnf.wcnf | O = 43 T = 6.57 |
O = 43 T = 15.75 (out)(err) |
O = 43 T = 6.57 (out)(err) |
| cnf3.150.500.646988.cnf.wcnf | O = 41 T = 7.51 |
O = 41 T = 20.65 (out)(err) |
O = 41 T = 7.51 (out)(err) |
| cnf3.150.500.646989.cnf.wcnf | O = 49 T = 8.67 |
O = 49 T = 10.46 (out)(err) |
O = 49 T = 8.67 (out)(err) |
| cnf3.150.500.646990.cnf.wcnf | O = 44 T = 6.93 |
O = 44 T = 21.68 (out)(err) |
O = 44 T = 6.93 (out)(err) |
| cnf3.150.550.009836.cnf.wcnf | O = 54 T = 3.39 |
O = 54 T = 3.39 (out)(err) |
O = 54 T = 7.90 (out)(err) |
| cnf3.150.550.009837.cnf.wcnf | O = 52 T = 8.60 |
O = 52 T = 8.60 (out)(err) |
O = 52 T = 10.18 (out)(err) |
| cnf3.150.550.009838.cnf.wcnf | O = 45 T = 8.99 |
O = 45 T = 11.33 (out)(err) |
O = 45 T = 8.99 (out)(err) |
| cnf3.150.550.009839.cnf.wcnf | O = 39 T = 6.53 |
O = 39 T = 7.02 (out)(err) |
O = 39 T = 6.53 (out)(err) |
| cnf3.150.550.009840.cnf.wcnf | O = 52 T = 7.13 |
O = 52 T = 7.95 (out)(err) |
O = 52 T = 7.13 (out)(err) |
| cnf3.150.550.009841.cnf.wcnf | O = 57 T = 9.34 |
O = 57 T = 9.34 (out)(err) |
O = 57 T = 10.24 (out)(err) |
| cnf3.150.550.009842.cnf.wcnf | O = 45 T = 7.12 |
O = 45 T = 7.12 (out)(err) |
O = 45 T = 7.46 (out)(err) |
| cnf3.150.550.009843.cnf.wcnf | O = 40 T = 7.60 |
O = 40 T = 7.60 (out)(err) |
O = 40 T = 11.65 (out)(err) |
| cnf3.150.550.009844.cnf.wcnf | O = 47 T = 6.98 |
O = 47 T = 15.63 (out)(err) |
O = 47 T = 6.98 (out)(err) |
| cnf3.150.550.009845.cnf.wcnf | O = 50 T = 4.75 |
O = 50 T = 4.75 (out)(err) |
O = 50 T = 9.93 (out)(err) |
| cnf3.150.600.372691.cnf.wcnf | O = 63 T = 2.60 |
O = 63 T = 2.60 (out)(err) |
O = 63 T = 10.16 (out)(err) |
| cnf3.150.600.372692.cnf.wcnf | O = 49 T = 3.58 |
O = 49 T = 3.58 (out)(err) |
O = 49 T = 9.60 (out)(err) |
| cnf3.150.600.372693.cnf.wcnf | O = 69 T = 1.64 |
O = 69 T = 1.64 (out)(err) |
O = 69 T = 65.52 (out)(err) |
| cnf3.150.600.372694.cnf.wcnf | O = 62 T = 2.61 |
O = 62 T = 2.61 (out)(err) |
O = 62 T = 10.94 (out)(err) |
| cnf3.150.600.372695.cnf.wcnf | O = 53 T = 3.23 |
O = 53 T = 3.23 (out)(err) |
O = 53 T = 10.49 (out)(err) |
| cnf3.150.600.372696.cnf.wcnf | O = 53 T = 2.45 |
O = 53 T = 2.45 (out)(err) |
O = 53 T = 11.01 (out)(err) |
| cnf3.150.600.372697.cnf.wcnf | O = 46 T = 5.02 |
O = 46 T = 5.02 (out)(err) |
O = 46 T = 9.44 (out)(err) |
| cnf3.150.600.372698.cnf.wcnf | O = 57 T = 4.22 |
O = 57 T = 4.22 (out)(err) |
O = 57 T = 7.86 (out)(err) |
| cnf3.150.600.372699.cnf.wcnf | O = 65 T = 2.23 |
O = 65 T = 2.23 (out)(err) |
O = 65 T = 9.13 (out)(err) |
| cnf3.150.600.372700.cnf.wcnf | O = 60 T = 3.45 |
O = 60 T = 3.45 (out)(err) |
O = 60 T = 8.37 (out)(err) |
| 3col100_5_1.shuffled.cnf.wcnf | O = 100 T = 2.43 |
O = 100 T = 2.43 (out)(err) |
O = 100 T = 105.77 (out)(err) |
| 3col100_5_10.shuffled.cnf.wcnf | O = 94 T = 2.06 |
O = 94 T = 2.06 (out)(err) |
O = 94 T = 18.39 (out)(err) |
| 3col100_5_2.shuffled.cnf.wcnf | O = 104 T = 2.22 |
O = 104 T = 2.22 (out)(err) |
O = 1142 T = 10.09 (out)(err) |
| 3col100_5_3.shuffled.cnf.wcnf | O = 92 T = 1.80 |
O = 92 T = 1.80 (out)(err) |
O = 93 T = 14.45 (out)(err) |
| 3col100_5_4.shuffled.cnf.wcnf | O = 97 T = 2.20 |
O = 97 T = 2.20 (out)(err) |
O = 102 T = 54.42 (out)(err) |
| 3col100_5_5.shuffled.cnf.wcnf | O = 86 T = 1.92 |
O = 86 T = 1.92 (out)(err) |
O = 86 T = 9.86 (out)(err) |
| 3col100_5_6.shuffled.cnf.wcnf | O = 90 T = 1.81 |
O = 90 T = 1.81 (out)(err) |
O = 90 T = 20.61 (out)(err) |
| 3col100_5_7.shuffled.cnf.wcnf | O = 85 T = 1.79 |
O = 85 T = 1.79 (out)(err) |
O = 85 T = 11.34 (out)(err) |
| 3col100_5_8.shuffled.cnf.wcnf | O = 94 T = 1.93 |
O = 94 T = 1.93 (out)(err) |
O = 95 T = 17.28 (out)(err) |
| 3col100_5_9.shuffled.cnf.wcnf | O = 94 T = 2.08 |
O = 94 T = 2.08 (out)(err) |
O = 94 T = 23.81 (out)(err) |
| 3col120_5_1.shuffled.cnf.wcnf | O = 123 T = 5.45 |
O = 123 T = 5.45 (out)(err) |
O = 1362 T = 107.47 (out)(err) |
| 3col120_5_10.shuffled.cnf.wcnf | O = 125 T = 4.60 |
O = 125 T = 4.60 (out)(err) |
O = 1363 T = 26.98 (out)(err) |
| 3col120_5_2.shuffled.cnf.wcnf | O = 124 T = 5.39 |
O = 124 T = 5.39 (out)(err) |
O = 1365 T = 12.94 (out)(err) |
| 3col120_5_3.shuffled.cnf.wcnf | O = 119 T = 4.82 |
O = 119 T = 4.82 (out)(err) |
O = 1370 T = 16.54 (out)(err) |
| 3col120_5_4.shuffled.cnf.wcnf | O = 122 T = 5.11 |
O = 122 T = 5.11 (out)(err) |
O = 122 T = 122.19 (out)(err) |
| 3col120_5_5.shuffled.cnf.wcnf | O = 112 T = 4.78 |
O = 112 T = 4.78 (out)(err) |
O = 114 T = 56.88 (out)(err) |
| 3col120_5_6.shuffled.cnf.wcnf | O = 121 T = 5.75 |
O = 121 T = 5.75 (out)(err) |
O = 121 T = 141.21 (out)(err) |
| 3col120_5_7.shuffled.cnf.wcnf | O = 120 T = 5.29 |
O = 120 T = 5.29 (out)(err) |
O = 1363 T = 12.35 (out)(err) |
| 3col120_5_8.shuffled.cnf.wcnf | O = 110 T = 4.27 |
O = 110 T = 4.27 (out)(err) |
O = 1359 T = 15.23 (out)(err) |
| 3col120_5_9.shuffled.cnf.wcnf | O = 117 T = 4.83 |
O = 117 T = 4.83 (out)(err) |
O = 1360 T = 28.94 (out)(err) |
| 3col140_5_1.shuffled.cnf.wcnf | O = 121 T = 7.86 |
O = 121 T = 7.86 (out)(err) |
O = 127 T = 171.21 (out)(err) |
| 3col140_5_10.shuffled.cnf.wcnf | O = 122 T = 12.61 |
O = 122 T = 12.61 (out)(err) |
O = 123 T = 92.84 (out)(err) |
| 3col140_5_2.shuffled.cnf.wcnf | O = 131 T = 8.14 |
O = 131 T = 8.14 (out)(err) |
O = 1596 T = 140.86 (out)(err) |
| 3col140_5_3.shuffled.cnf.wcnf | O = 128 T = 6.20 |
O = 128 T = 6.20 (out)(err) |
O = 1598 T = 18.36 (out)(err) |
| 3col140_5_4.shuffled.cnf.wcnf | O = 128 T = 6.75 |
O = 128 T = 6.75 (out)(err) |
O = 138 T = 224.60 (out)(err) |
| 3col140_5_5.shuffled.cnf.wcnf | O = 124 T = 9.88 |
O = 124 T = 9.88 (out)(err) |
O = 124 T = 97.84 (out)(err) |
| 3col140_5_6.shuffled.cnf.wcnf | O = 120 T = 8.08 |
O = 120 T = 8.08 (out)(err) |
O = 120 T = 80.30 (out)(err) |
| 3col140_5_7.shuffled.cnf.wcnf | O = 119 T = 10.95 |
O = 119 T = 10.95 (out)(err) |
O = 121 T = 45.12 (out)(err) |
| 3col140_5_8.shuffled.cnf.wcnf | O = 123 T = 4.92 |
O = 123 T = 4.92 (out)(err) |
O = 1599 T = 76.91 (out)(err) |
| 3col140_5_9.shuffled.cnf.wcnf | O = 134 T = 10.38 |
O = 134 T = 10.38 (out)(err) |
O = 1601 T = 84.30 (out)(err) |
| 3col80_5_1.shuffled.cnf.wcnf | O = 79 T = 1.36 |
O = 79 T = 1.36 (out)(err) |
O = 79 T = 7.07 (out)(err) |
| 3col80_5_10.shuffled.cnf.wcnf | O = 75 T = 1.14 |
O = 75 T = 1.14 (out)(err) |
O = 75 T = 8.11 (out)(err) |
| 3col80_5_2.shuffled.cnf.wcnf | O = 71 T = 1.24 |
O = 71 T = 1.24 (out)(err) |
O = 71 T = 8.38 (out)(err) |
| 3col80_5_3.shuffled.cnf.wcnf | O = 88 T = 1.27 |
O = 88 T = 1.27 (out)(err) |
O = 88 T = 7.87 (out)(err) |
| 3col80_5_4.shuffled.cnf.wcnf | O = 73 T = 1.07 |
O = 73 T = 1.07 (out)(err) |
O = 73 T = 7.83 (out)(err) |
| 3col80_5_5.shuffled.cnf.wcnf | O = 78 T = 1.53 |
O = 78 T = 1.53 (out)(err) |
O = 78 T = 8.73 (out)(err) |
| 3col80_5_6.shuffled.cnf.wcnf | O = 76 T = 1.42 |
O = 76 T = 1.42 (out)(err) |
O = 76 T = 8.83 (out)(err) |
| 3col80_5_7.shuffled.cnf.wcnf | O = 80 T = 1.15 |
O = 80 T = 1.15 (out)(err) |
O = 80 T = 5.15 (out)(err) |
| 3col80_5_8.shuffled.cnf.wcnf | O = 82 T = 1.23 |
O = 82 T = 1.23 (out)(err) |
O = 82 T = 8.87 (out)(err) |
| 3col80_5_9.shuffled.cnf.wcnf | O = 79 T = 1.00 |
O = 79 T = 1.00 (out)(err) |
O = 79 T = 12.40 (out)(err) |
| cnt05.shuffled.cnf.wcnf | O = 174 T = 0.93 |
O = 174 T = 0.93 (out)(err) |
O = 1451 T = 18.40 (out)(err) |
| cnt06.shuffled.cnf.wcnf | O = 365 T = 1.69 |
O = 365 T = 1.69 (out)(err) |
O = 6782 T = 28.69 (out)(err) |
| cnt07.shuffled.cnf.wcnf | O = 877 T = 2.89 |
O = 877 T = 2.89 (out)(err) |
O = 123058 T = 97.12 (out)(err) |
| dp02s02.shuffled.cnf.wcnf | O = 100 T = 0.60 |
O = 100 T = 0.60 (out)(err) |
O = 103 T = 25.76 (out)(err) |
| dp03s03.shuffled.cnf.wcnf | O = 254 T = 1.27 |
O = 254 T = 1.27 (out)(err) |
O = 12868 T = 44.35 (out)(err) |
| dp04s04.shuffled.cnf.wcnf | O = 533 T = 2.15 |
O = 533 T = 2.15 (out)(err) |
O = 71277 T = 231.78 (out)(err) |
| dp05s05.shuffled.cnf.wcnf | O = 765 T = 2.84 |
O = 765 T = 2.84 (out)(err) |
O = 201865 T = 53.27 (out)(err) |
| dp06s06.shuffled.cnf.wcnf | O = 1164 T = 5.70 |
O = 1164 T = 5.70 (out)(err) |
O = 488933 T = 13.33 (out)(err) |
| dp07s07.shuffled.cnf.wcnf | O = 1563 T = 41.90 |
O = 1563 T = 41.90 (out)(err) |
O = 878812 T = 172.23 (out)(err) |
| ezfact32_1.shuffled.cnf.wcnf | O = 400 T = 2.08 |
O = 400 T = 2.08 (out)(err) |
O = 111250 T = 157.60 (out)(err) |
| ezfact32_10.shuffled.cnf.wcnf | O = 389 T = 2.07 |
O = 389 T = 2.07 (out)(err) |
O = 122344 T = 149.72 (out)(err) |
| ezfact32_2.shuffled.cnf.wcnf | O = 364 T = 2.01 |
O = 364 T = 2.01 (out)(err) |
O = 116786 T = 38.71 (out)(err) |
| ezfact32_3.shuffled.cnf.wcnf | O = 397 T = 12.87 |
O = 397 T = 12.87 (out)(err) |
O = 105715 T = 23.69 (out)(err) |
| ezfact32_4.shuffled.cnf.wcnf | O = 379 T = 1.82 |
O = 379 T = 1.82 (out)(err) |
O = 116797 T = 53.11 (out)(err) |
| ezfact32_5.shuffled.cnf.wcnf | O = 394 T = 2.11 |
O = 394 T = 2.11 (out)(err) |
O = 105686 T = 190.01 (out)(err) |
| ezfact32_6.shuffled.cnf.wcnf | O = 382 T = 2.56 |
O = 382 T = 2.56 (out)(err) |
O = 122326 T = 80.59 (out)(err) |
| ezfact32_7.shuffled.cnf.wcnf | O = 394 T = 1.48 |
O = 394 T = 1.48 (out)(err) |
O = 127876 T = 237.77 (out)(err) |
| ezfact32_8.shuffled.cnf.wcnf | O = 392 T = 1.82 |
O = 392 T = 1.82 (out)(err) |
O = 127849 T = 25.79 (out)(err) |
| ezfact32_9.shuffled.cnf.wcnf | O = 382 T = 1.87 |
O = 382 T = 1.87 (out)(err) |
O = 111220 T = 86.00 (out)(err) |
| med11.shuffled.cnf.wcnf | O = 164 T = 4.48 |
O = 164 T = 4.48 (out)(err) |
O = 164 T = 12.04 (out)(err) |
| kbtree9_7_3_5_30_1.wcsp.wcnf | O = 9 T = 137.38 |
O = 16 T = 1.12 (out)(err) |
O = 9 T = 137.38 (out)(err) |
| kbtree9_7_3_5_30_2.wcsp.wcnf | O = 7 T = 4.21 |
O = 25 T = 2.09 (out)(err) |
O = 7 T = 4.21 (out)(err) |
| kbtree9_7_3_5_30_3.wcsp.wcnf | O = 9 T = 1.17 |
O = 17 T = 5.76 (out)(err) |
O = 9 T = 1.17 (out)(err) |
| kbtree9_7_3_5_30_4.wcsp.wcnf | O = 6 T = 7.78 |
O = 22 T = 1.46 (out)(err) |
O = 6 T = 7.78 (out)(err) |
| kbtree9_7_3_5_30_5.wcsp.wcnf | O = 6 T = 3.91 |
O = 9 T = 280.70 (out)(err) |
O = 6 T = 3.91 (out)(err) |
| kbtree9_7_3_5_30_6.wcsp.wcnf | O = 9 T = 189.08 |
O = 20 T = 4.26 (out)(err) |
O = 9 T = 189.08 (out)(err) |
| kbtree9_7_3_5_40_1.wcsp.wcnf | O = 27 T = 6.86 |
O = 48 T = 5.06 (out)(err) |
O = 27 T = 6.86 (out)(err) |
| kbtree9_7_3_5_40_2.wcsp.wcnf | O = 26 T = 9.85 |
O = 53 T = 2.18 (out)(err) |
O = 26 T = 9.85 (out)(err) |
| kbtree9_7_3_5_40_3.wcsp.wcnf | O = 22 T = 5.00 |
O = 39 T = 4.48 (out)(err) |
O = 22 T = 5.00 (out)(err) |
| kbtree9_7_3_5_40_4.wcsp.wcnf | O = 22 T = 8.00 |
O = 41 T = 5.60 (out)(err) |
O = 22 T = 8.00 (out)(err) |
| kbtree9_7_3_5_40_5.wcsp.wcnf | O = 23 T = 25.98 |
O = 41 T = 5.79 (out)(err) |
O = 23 T = 25.98 (out)(err) |
| kbtree9_7_3_5_40_6.wcsp.wcnf | O = 26 T = 8.46 |
O = 51 T = 3.13 (out)(err) |
O = 26 T = 8.46 (out)(err) |
| kbtree9_7_3_5_50_1.wcsp.wcnf | O = 36 T = 9.72 |
O = 56 T = 2.39 (out)(err) |
O = 36 T = 9.72 (out)(err) |
| kbtree9_7_3_5_50_2.wcsp.wcnf | O = 37 T = 11.29 |
O = 67 T = 1.89 (out)(err) |
O = 37 T = 11.29 (out)(err) |
| kbtree9_7_3_5_50_3.wcsp.wcnf | O = 37 T = 9.35 |
O = 52 T = 6.53 (out)(err) |
O = 37 T = 9.35 (out)(err) |
| kbtree9_7_3_5_50_4.wcsp.wcnf | O = 38 T = 11.40 |
O = 61 T = 1.79 (out)(err) |
O = 38 T = 11.40 (out)(err) |
| kbtree9_7_3_5_50_5.wcsp.wcnf | O = 37 T = 9.33 |
O = 60 T = 4.68 (out)(err) |
O = 37 T = 9.33 (out)(err) |
| kbtree9_7_3_5_50_6.wcsp.wcnf | O = 38 T = 5.30 |
O = 58 T = 2.15 (out)(err) |
O = 38 T = 5.30 (out)(err) |
| kbtree9_7_3_5_60_1.wcsp.wcnf | O = 54 T = 8.56 |
O = 87 T = 4.59 (out)(err) |
O = 54 T = 8.56 (out)(err) |
| kbtree9_7_3_5_60_2.wcsp.wcnf | O = 59 T = 14.14 |
O = 73 T = 4.64 (out)(err) |
O = 59 T = 14.14 (out)(err) |
| kbtree9_7_3_5_60_3.wcsp.wcnf | O = 59 T = 8.30 |
O = 85 T = 4.96 (out)(err) |
O = 59 T = 8.30 (out)(err) |
| kbtree9_7_3_5_60_4.wcsp.wcnf | O = 59 T = 12.58 |
O = 83 T = 5.24 (out)(err) |
O = 59 T = 12.58 (out)(err) |
| kbtree9_7_3_5_60_5.wcsp.wcnf | O = 56 T = 43.03 |
O = 86 T = 2.39 (out)(err) |
O = 56 T = 43.03 (out)(err) |
| kbtree9_7_3_5_60_6.wcsp.wcnf | O = 57 T = 7.41 |
O = 90 T = 3.81 (out)(err) |
O = 57 T = 7.41 (out)(err) |
| kbtree9_7_3_5_70_1.wcsp.wcnf | O = 75 T = 19.64 |
O = 106 T = 5.16 (out)(err) |
O = 75 T = 19.64 (out)(err) |
| kbtree9_7_3_5_70_2.wcsp.wcnf | O = 72 T = 9.72 |
O = 107 T = 1.75 (out)(err) |
O = 72 T = 9.72 (out)(err) |
| kbtree9_7_3_5_70_3.wcsp.wcnf | O = 76 T = 35.75 |
O = 102 T = 6.37 (out)(err) |
O = 76 T = 35.75 (out)(err) |
| kbtree9_7_3_5_70_4.wcsp.wcnf | O = 74 T = 9.23 |
O = 111 T = 2.13 (out)(err) |
O = 74 T = 9.23 (out)(err) |
| kbtree9_7_3_5_70_5.wcsp.wcnf | O = 72 T = 6.94 |
O = 103 T = 2.35 (out)(err) |
O = 72 T = 6.94 (out)(err) |
| kbtree9_7_3_5_70_6.wcsp.wcnf | O = 75 T = 17.44 |
O = 105 T = 3.86 (out)(err) |
O = 75 T = 17.44 (out)(err) |
| kbtree9_7_3_5_80_1.wcsp.wcnf | O = 98 T = 8.76 |
O = 124 T = 5.75 (out)(err) |
O = 98 T = 8.76 (out)(err) |
| kbtree9_7_3_5_80_2.wcsp.wcnf | O = 104 T = 121.61 |
O = 131 T = 5.88 (out)(err) |
O = 104 T = 121.61 (out)(err) |
| kbtree9_7_3_5_80_3.wcsp.wcnf | O = 105 T = 157.46 |
O = 132 T = 0.52 (out)(err) |
O = 105 T = 157.46 (out)(err) |
| kbtree9_7_3_5_80_4.wcsp.wcnf | O = 101 T = 174.32 |
O = 124 T = 2.13 (out)(err) |
O = 101 T = 174.32 (out)(err) |
| kbtree9_7_3_5_80_5.wcsp.wcnf | O = 107 T = 18.51 |
O = 127 T = 5.00 (out)(err) |
O = 107 T = 18.51 (out)(err) |
| kbtree9_7_3_5_80_6.wcsp.wcnf | O = 106 T = 140.18 |
O = 128 T = 2.66 (out)(err) |
O = 106 T = 140.18 (out)(err) |
| kbtree9_7_3_5_90_1.wcsp.wcnf | O = 126 T = 48.98 |
O = 142 T = 3.24 (out)(err) |
O = 126 T = 48.98 (out)(err) |
| kbtree9_7_3_5_90_2.wcsp.wcnf | O = 127 T = 91.11 |
O = 149 T = 5.41 (out)(err) |
O = 127 T = 91.11 (out)(err) |
| kbtree9_7_3_5_90_3.wcsp.wcnf | O = 126 T = 59.60 |
O = 146 T = 4.10 (out)(err) |
O = 126 T = 59.60 (out)(err) |
| kbtree9_7_3_5_90_4.wcsp.wcnf | O = 131 T = 18.91 |
O = 144 T = 2.40 (out)(err) |
O = 131 T = 18.91 (out)(err) |
| kbtree9_7_3_5_90_5.wcsp.wcnf | O = 128 T = 188.01 |
O = 140 T = 47.11 (out)(err) |
O = 128 T = 188.01 (out)(err) |
| kbtree9_7_3_5_90_6.wcsp.wcnf | O = 133 T = 50.08 |
O = 147 T = 147.79 (out)(err) |
O = 133 T = 50.08 (out)(err) |
| normalized-mps-v2-20-10-stein15.opb.msat.wcnf | O = 9 T = 0.62 |
O = 9 T = 0.62 (out)(err) |
O = 9 T = 1.78 (out)(err) |
| normalized-mps-v2-20-10-stein27.opb.msat.wcnf | O = 18 T = 1.87 |
O = 18 T = 1.87 (out)(err) |
O = 18 T = 5.13 (out)(err) |
| normalized-mps-v2-20-10-stein45.opb.msat.wcnf | O = 30 T = 17.75 |
O = 30 T = 17.75 (out)(err) |
O = 30 T = 115.41 (out)(err) |
| normalized-mps-v2-20-10-stein9.opb.msat.wcnf | O = 5 T = 0.36 |
O = 5 T = 0.36 (out)(err) |
O = 5 T = 0.81 (out)(err) |