| 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 |
|---|---|---|---|
| ped2.B.recomb1-0.01-1.wcnf | O = 7 T = 5.29 |
O = 7 T = 5.29 (out)(err) |
O = 1350 T = 179.44 (out)(err) |
| ped2.B.recomb1-0.01-2.wcnf | O = 7 T = 5.65 |
O = 7 T = 5.65 (out)(err) |
O = 155499436 T = 199.73 (out)(err) |
| ped2.B.recomb1-0.01-3.wcnf | O = 6 T = 4.22 |
O = 6 T = 4.22 (out)(err) |
O = 131 T = 195.86 (out)(err) |
| ped2.B.recomb1-0.01-4.wcnf | O = 7 T = 4.09 |
O = 7 T = 4.09 (out)(err) |
O = 1397043 T = 169.41 (out)(err) |
| ped2.B.recomb1-0.01-5.wcnf | O = 7 T = 5.41 |
O = 7 T = 5.41 (out)(err) |
O = 143453563 T = 156.56 (out)(err) |
| ped2.B.recomb1-0.10-10.wcnf | O = 6 T = 5.10 |
O = 6 T = 5.10 (out)(err) |
O = 1573708 T = 195.94 (out)(err) |
| ped2.B.recomb1-0.10-6.wcnf | O = 7 T = 6.04 |
O = 7 T = 6.04 (out)(err) |
O = 183464708 T = 150.77 (out)(err) |
| ped2.B.recomb1-0.10-7.wcnf | O = 588 T = 5.91 |
O = 588 T = 5.91 (out)(err) |
O = 17880566 T = 151.76 (out)(err) |
| ped2.B.recomb1-0.10-8.wcnf | O = 589 T = 4.58 |
O = 589 T = 4.58 (out)(err) |
O = 148141070 T = 144.49 (out)(err) |
| ped2.B.recomb1-0.10-9.wcnf | O = 7 T = 7.69 |
O = 7 T = 7.69 (out)(err) |
O = 152761760 T = 163.21 (out)(err) |
| ped2.B.recomb1-0.20-11.wcnf | O = 7 T = 8.47 |
O = 7 T = 8.47 (out)(err) |
O = 143 T = 209.43 (out)(err) |
| ped2.B.recomb1-0.20-12.wcnf | O = 7 T = 12.01 |
O = 7 T = 12.01 (out)(err) |
O = 157376063 T = 166.10 (out)(err) |
| ped2.B.recomb1-0.20-13.wcnf | O = 7 T = 7.63 |
O = 7 T = 7.63 (out)(err) |
O = 1 T = 158.16 (out)(err) |
| ped2.B.recomb1-0.20-14.wcnf | O = 7 T = 7.10 |
O = 7 T = 7.10 (out)(err) |
O = 12947 T = 189.24 (out)(err) |
| ped2.B.recomb1-0.20-15.wcnf | O = 7 T = 14.23 |
O = 7 T = 14.23 (out)(err) |
O = 182527556 T = 141.18 (out)(err) |
| ped2.G.recomb1-0.01-1.wcnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = 11 T = 190.83 (out)(err) |
| ped2.G.recomb1-0.01-2.wcnf | O = 8771 T = 12.14 |
O = 8771 T = 12.14 (out)(err) |
O = 93594155389 T = 194.37 (out)(err) |
| ped2.G.recomb1-0.01-3.wcnf | O = 11672 T = 29.15 |
O = 11672 T = 29.15 (out)(err) |
O = 15268 T = 194.39 (out)(err) |
| ped2.G.recomb1-0.01-4.wcnf | O = 11665 T = 204.52 |
O = 11665 T = 204.52 (out)(err) |
O = 85779 T = 191.56 (out)(err) |
| ped2.G.recomb1-0.01-5.wcnf | O = 3525 T = 179.34 |
O = 3525 T = 179.34 (out)(err) |
O = 112805820349 T = 190.35 (out)(err) |
| ped2.G.recomb1-0.10-10.wcnf | O = N/A T = TO |
O = 5272 T = 218.36 (out)(err) |
O = 8413269181 T = 190.45 (out)(err) |
| ped2.G.recomb1-0.10-6.wcnf | O = N/A T = TO |
O = 9928 T = 16.38 (out)(err) |
O = 106690637347 T = 190.84 (out)(err) |
| ped2.G.recomb1-0.10-7.wcnf | O = N/A T = TO |
O = 4694 T = 158.60 (out)(err) |
O = 1309484737 T = 191.74 (out)(err) |
| ped2.G.recomb1-0.10-8.wcnf | O = N/A T = TO |
O = 23891 T = 63.05 (out)(err) |
O = N/A T = TO (out)(err) |
| ped2.G.recomb1-0.10-9.wcnf | O = N/A T = TO |
O = 7023 T = 199.10 (out)(err) |
O = 153527834978 T = 193.83 (out)(err) |
| ped2.G.recomb1-0.20-11.wcnf | O = N/A T = TO |
O = 8760 T = 19.43 (out)(err) |
O = N/A T = TO (out)(err) |
| ped2.G.recomb1-0.20-12.wcnf | O = N/A T = TO |
O = 63996 T = 22.86 (out)(err) |
O = N/A T = TO (out)(err) |
| ped2.G.recomb1-0.20-13.wcnf | O = N/A T = TO |
O = 42489 T = 21.05 (out)(err) |
O = N/A T = TO (out)(err) |
| ped2.G.recomb1-0.20-14.wcnf | O = N/A T = TO |
O = 20399 T = 21.97 (out)(err) |
O = 8045545872000 T = 6.83 (out)(err) |
| ped2.G.recomb1-0.20-15.wcnf | O = N/A T = TO |
O = 29109 T = 22.77 (out)(err) |
O = N/A T = TO (out)(err) |
| ped2.G.recomb10-0.01-1.wcnf | O = 143075 T = 18.16 |
O = 143075 T = 18.16 (out)(err) |
O = 84806182 T = 190.14 (out)(err) |
| ped2.G.recomb10-0.01-2.wcnf | O = 90175 T = 15.83 |
O = 90175 T = 15.83 (out)(err) |
O = 121797021973 T = 190.91 (out)(err) |
| ped2.G.recomb10-0.01-3.wcnf | O = 122732 T = 224.42 |
O = 122732 T = 224.42 (out)(err) |
O = 93957 T = 190.13 (out)(err) |
| ped2.G.recomb10-0.01-4.wcnf | O = 127985 T = 13.88 |
O = 127985 T = 13.88 (out)(err) |
O = 112324758735 T = 189.21 (out)(err) |
| ped2.G.recomb10-0.01-5.wcnf | O = 138432 T = 13.07 |
O = 138432 T = 13.07 (out)(err) |
O = 121208938958 T = 193.76 (out)(err) |
| ped2.G.recomb10-0.10-10.wcnf | O = N/A T = TO |
O = 154729 T = 18.27 (out)(err) |
O = 114 T = 192.17 (out)(err) |
| ped2.G.recomb10-0.10-6.wcnf | O = N/A T = TO |
O = 142512 T = 20.95 (out)(err) |
O = 1585846 T = 190.43 (out)(err) |
| ped2.G.recomb10-0.10-7.wcnf | O = N/A T = TO |
O = 104727 T = 18.97 (out)(err) |
O = 161481935294 T = 193.51 (out)(err) |
| ped2.G.recomb10-0.10-8.wcnf | O = N/A T = TO |
O = 129148 T = 21.30 (out)(err) |
O = 153196372153 T = 196.38 (out)(err) |
| ped2.G.recomb10-0.10-9.wcnf | O = N/A T = TO |
O = 139598 T = 17.14 (out)(err) |
O = 195158506861 T = 199.93 (out)(err) |
| ped2.G.recomb10-0.20-11.wcnf | O = N/A T = TO |
O = 152394 T = 23.39 (out)(err) |
O = N/A T = TO (out)(err) |
| ped2.G.recomb10-0.20-12.wcnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
| ped2.G.recomb10-0.20-13.wcnf | O = N/A T = TO |
O = 111703 T = 25.32 (out)(err) |
O = N/A T = TO (out)(err) |
| ped2.G.recomb10-0.20-14.wcnf | O = N/A T = TO |
O = 112284 T = 29.65 (out)(err) |
O = N/A T = TO (out)(err) |
| ped2.G.recomb10-0.20-15.wcnf | O = N/A T = TO |
O = 144261 T = 25.58 (out)(err) |
O = N/A T = TO (out)(err) |
| ped2.G.recomb5-0.01-1.wcnf | O = 59357 T = 14.39 |
O = 59357 T = 14.39 (out)(err) |
O = 106017096246 T = 199.05 (out)(err) |
| ped2.G.recomb5-0.01-2.wcnf | O = 89010 T = 15.18 |
O = 89010 T = 15.18 (out)(err) |
O = 162401371851 T = 197.51 (out)(err) |
| ped2.G.recomb5-0.01-3.wcnf | O = 69238 T = 14.60 |
O = 69238 T = 14.60 (out)(err) |
O = 127954942753 T = 198.95 (out)(err) |
| ped2.G.recomb5-0.01-4.wcnf | O = 42494 T = 12.61 |
O = 42494 T = 12.61 (out)(err) |
O = 114078061625 T = 187.29 (out)(err) |
| ped2.G.recomb5-0.01-5.wcnf | O = 65762 T = 10.94 |
O = 65762 T = 10.94 (out)(err) |
O = 91680444224 T = 192.90 (out)(err) |
| ped2.G.recomb5-0.10-10.wcnf | O = N/A T = TO |
O = 66914 T = 50.63 (out)(err) |
O = 127377722184 T = 195.83 (out)(err) |
| ped2.G.recomb5-0.10-6.wcnf | O = 61125 T = 16.62 |
O = 61125 T = 16.62 (out)(err) |
O = 148535189824 T = 190.84 (out)(err) |
| ped2.G.recomb5-0.10-7.wcnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = 116387359995 T = 192.75 (out)(err) |
| ped2.G.recomb5-0.10-8.wcnf | O = N/A T = TO |
O = 64596 T = 20.79 (out)(err) |
O = 151443139 T = 197.23 (out)(err) |
| ped2.G.recomb5-0.10-9.wcnf | O = N/A T = TO |
O = 70991 T = 17.49 (out)(err) |
O = 1620 T = 196.08 (out)(err) |
| ped2.G.recomb5-0.20-11.wcnf | O = N/A T = TO |
O = 73908 T = 22.38 (out)(err) |
O = N/A T = TO (out)(err) |
| ped2.G.recomb5-0.20-12.wcnf | O = N/A T = TO |
O = 57040 T = 23.27 (out)(err) |
O = 7513851317440 T = 6.52 (out)(err) |
| ped2.G.recomb5-0.20-13.wcnf | O = N/A T = TO |
O = 97752 T = 24.75 (out)(err) |
O = N/A T = TO (out)(err) |
| ped2.G.recomb5-0.20-14.wcnf | O = N/A T = TO |
O = 64600 T = 32.76 (out)(err) |
O = N/A T = TO (out)(err) |
| ped2.G.recomb5-0.20-15.wcnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
| ped3.D.recomb10-0.20-11.wcnf | O = 690 T = 7.32 |
O = 690 T = 7.32 (out)(err) |
O = 57346327 T = 69.19 (out)(err) |
| ped3.D.recomb10-0.20-12.wcnf | O = 349 T = 3.95 |
O = 349 T = 3.95 (out)(err) |
O = 59442118 T = 164.93 (out)(err) |
| ped3.D.recomb10-0.20-13.wcnf | O = 350 T = 56.26 |
O = 350 T = 56.26 (out)(err) |
O = 47358438 T = 178.68 (out)(err) |
| ped3.D.recomb10-0.20-14.wcnf | O = 7 T = 5.58 |
O = 7 T = 5.58 (out)(err) |
O = 41058803 T = 106.05 (out)(err) |
| ped3.D.recomb10-0.20-15.wcnf | O = 689 T = 5.04 |
O = 689 T = 5.04 (out)(err) |
O = 48419626 T = 81.91 (out)(err) |
| ped3.E.recomb10-0.20-11.wcnf | O = 20869 T = 7.48 |
O = 20869 T = 7.48 (out)(err) |
O = 563057235 T = 145.00 (out)(err) |
| ped3.E.recomb10-0.20-12.wcnf | O = 20869 T = 37.15 |
O = 20869 T = 37.15 (out)(err) |
O = 568705554 T = 233.66 (out)(err) |
| ped3.E.recomb10-0.20-13.wcnf | O = 11647 T = 282.24 |
O = 11647 T = 282.24 (out)(err) |
O = 499287846 T = 147.64 (out)(err) |
| ped3.E.recomb10-0.20-14.wcnf | O = 19838 T = 8.07 |
O = 19838 T = 8.07 (out)(err) |
O = 632477997 T = 139.37 (out)(err) |
| ped3.E.recomb10-0.20-15.wcnf | O = 8570 T = 199.23 |
O = 8570 T = 199.23 (out)(err) |
O = 546169178 T = 180.96 (out)(err) |
| ped3.F.recomb10-0.01-1.wcnf | O = 14374 T = 5.23 |
O = 14374 T = 5.23 (out)(err) |
O = 559646186 T = 123.94 (out)(err) |
| ped3.F.recomb10-0.01-2.wcnf | O = 19832 T = 99.36 |
O = 19832 T = 99.36 (out)(err) |
O = 499759421 T = 66.24 (out)(err) |
| ped3.F.recomb10-0.01-3.wcnf | O = 8571 T = 5.51 |
O = 8571 T = 5.51 (out)(err) |
O = 510793169 T = 83.29 (out)(err) |
| ped3.F.recomb10-0.01-4.wcnf | O = 7207 T = 219.26 |
O = 7207 T = 219.26 (out)(err) |
O = 484003165 T = 43.77 (out)(err) |
| ped3.F.recomb10-0.01-5.wcnf | O = 9598 T = 216.89 |
O = 9598 T = 216.89 (out)(err) |
O = 518675722 T = 58.28 (out)(err) |
| ped3.F.recomb10-0.10-10.wcnf | O = 11304 T = 5.93 |
O = 11304 T = 5.93 (out)(err) |
O = 621106688 T = 192.70 (out)(err) |
| ped3.F.recomb10-0.10-6.wcnf | O = 8921 T = 7.19 |
O = 8921 T = 7.19 (out)(err) |
O = 547031942 T = 92.94 (out)(err) |
| ped3.F.recomb10-0.10-7.wcnf | O = 11654 T = 9.27 |
O = 11654 T = 9.27 (out)(err) |
O = 537575663 T = 115.42 (out)(err) |
| ped3.F.recomb10-0.10-8.wcnf | O = 20196 T = 7.06 |
O = 20196 T = 7.06 (out)(err) |
O = 452492415 T = 192.49 (out)(err) |
| ped3.F.recomb10-0.10-9.wcnf | O = 6871 T = 5.47 |
O = 6871 T = 5.47 (out)(err) |
O = 479292958 T = 189.93 (out)(err) |
| ped3.F.recomb10-0.20-11.wcnf | O = 9268 T = 178.71 |
O = 9268 T = 178.71 (out)(err) |
O = 386301259 T = 179.14 (out)(err) |
| ped3.F.recomb10-0.20-12.wcnf | O = 15406 T = 31.55 |
O = 15406 T = 31.55 (out)(err) |
O = 365790478 T = 192.55 (out)(err) |
| ped3.F.recomb10-0.20-13.wcnf | O = 2416 T = 44.89 |
O = 2416 T = 44.89 (out)(err) |
O = 490313752 T = 207.73 (out)(err) |
| ped3.F.recomb10-0.20-14.wcnf | O = 8234 T = 6.75 |
O = 8234 T = 6.75 (out)(err) |
O = 405167776 T = 126.19 (out)(err) |
| ped3.F.recomb10-0.20-15.wcnf | O = 8574 T = 132.40 |
O = 8574 T = 132.40 (out)(err) |
O = 658931794 T = 194.73 (out)(err) |
| ped3.G.recomb10-0.01-1.wcnf | O = 27022 T = 7.05 |
O = 27022 T = 7.05 (out)(err) |
O = 7355 T = 225.63 (out)(err) |
| ped3.G.recomb10-0.01-2.wcnf | O = 21572 T = 7.40 |
O = 21572 T = 7.40 (out)(err) |
O = 984110 T = 174.22 (out)(err) |
| ped3.G.recomb10-0.01-3.wcnf | O = 23955 T = 7.33 |
O = 23955 T = 7.33 (out)(err) |
O = 1249890626 T = 233.52 (out)(err) |
| ped3.G.recomb10-0.01-4.wcnf | O = 30775 T = 7.45 |
O = 30775 T = 7.45 (out)(err) |
O = 8806 T = 222.20 (out)(err) |
| ped3.G.recomb10-0.01-5.wcnf | O = 20207 T = 6.79 |
O = 20207 T = 6.79 (out)(err) |
O = 1346523555 T = 238.63 (out)(err) |
| ped3.G.recomb10-0.10-10.wcnf | O = 31133 T = 9.33 |
O = 31133 T = 9.33 (out)(err) |
O = 925448212 T = 197.61 (out)(err) |
| ped3.G.recomb10-0.10-6.wcnf | O = 29775 T = 7.67 |
O = 29775 T = 7.67 (out)(err) |
O = 8599387 T = 217.12 (out)(err) |
| ped3.G.recomb10-0.10-7.wcnf | O = 29758 T = 7.56 |
O = 29758 T = 7.56 (out)(err) |
O = 991023561 T = 216.31 (out)(err) |
| ped3.G.recomb10-0.10-8.wcnf | O = 28058 T = 98.09 |
O = 28058 T = 98.09 (out)(err) |
O = 939196002 T = 225.44 (out)(err) |
| ped3.G.recomb10-0.10-9.wcnf | O = 25325 T = 7.66 |
O = 25325 T = 7.66 (out)(err) |
O = 91 T = 231.50 (out)(err) |
| ped3.G.recomb10-0.20-11.wcnf | O = 22950 T = 196.33 |
O = 22950 T = 196.33 (out)(err) |
O = 860005239 T = 205.88 (out)(err) |
| ped3.G.recomb10-0.20-12.wcnf | O = 28411 T = 8.98 |
O = 28411 T = 8.98 (out)(err) |
O = 1298170423 T = 211.13 (out)(err) |
| ped3.G.recomb10-0.20-13.wcnf | O = 35588 T = 13.85 |
O = 35588 T = 13.85 (out)(err) |
O = 870376430 T = 224.39 (out)(err) |
| ped3.G.recomb10-0.20-14.wcnf | O = 24992 T = 9.76 |
O = 24992 T = 9.76 (out)(err) |
O = 1139494922 T = 208.43 (out)(err) |
| ped3.G.recomb10-0.20-15.wcnf | O = 28747 T = 9.09 |
O = 28747 T = 9.09 (out)(err) |
O = 1015463719 T = 204.17 (out)(err) |
| comp01.wcnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = 31292 T = 14.86 (out)(err) |
| comp02.wcnf | O = N/A T = TO |
O = 135 T = 284.41 (out)(err) |
O = 1687811 T = 238.98 (out)(err) |
| comp03.wcnf | O = N/A T = TO |
O = 349 T = 5.31 (out)(err) |
O = 786258 T = 238.66 (out)(err) |
| comp04.wcnf | O = N/A T = TO |
O = 66 T = 205.62 (out)(err) |
O = 943924 T = 254.31 (out)(err) |
| comp05.wcnf | O = N/A T = TO |
O = 1062 T = 5.30 (out)(err) |
O = 2203447 T = 91.74 (out)(err) |
| comp06.wcnf | O = N/A T = TO |
O = 247 T = 264.45 (out)(err) |
O = 1684307 T = 238.06 (out)(err) |
| comp07.wcnf | O = N/A T = TO |
O = 799 T = 244.25 (out)(err) |
O = 502 T = 223.02 (out)(err) |
| comp08.wcnf | O = N/A T = TO |
O = 91 T = 27.88 (out)(err) |
O = 2190589 T = 242.70 (out)(err) |
| comp09.wcnf | O = N/A T = TO |
O = 218 T = 248.04 (out)(err) |
O = 1785767 T = 244.97 (out)(err) |
| comp10.wcnf | O = N/A T = TO |
O = 190 T = 280.13 (out)(err) |
O = 6901735 T = 230.33 (out)(err) |
| comp12.wcnf | O = N/A T = TO |
O = 1299 T = 5.48 (out)(err) |
O = 4462285 T = 234.81 (out)(err) |
| comp13.wcnf | O = N/A T = TO |
O = 180 T = 77.46 (out)(err) |
O = 1564936 T = 238.95 (out)(err) |
| comp14.wcnf | O = N/A T = TO |
O = 138 T = 240.10 (out)(err) |
O = 1536729 T = 238.94 (out)(err) |
| comp15.wcnf | O = N/A T = TO |
O = 349 T = 5.68 (out)(err) |
O = 718172 T = 234.76 (out)(err) |
| comp16.wcnf | O = N/A T = TO |
O = 99 T = 221.97 (out)(err) |
O = 7675777 T = 227.98 (out)(err) |
| comp17.wcnf | O = N/A T = TO |
O = 280 T = 281.99 (out)(err) |
O = 5870274 T = 238.99 (out)(err) |
| comp18.wcnf | O = N/A T = TO |
O = 293 T = 5.25 (out)(err) |
O = 708255 T = 111.16 (out)(err) |
| comp19.wcnf | O = N/A T = TO |
O = 218 T = 32.86 (out)(err) |
O = 1782698 T = 239.04 (out)(err) |
| comp20.wcnf | O = N/A T = TO |
O = 544 T = 26.66 (out)(err) |
O = 2500754 T = 238.00 (out)(err) |
| comp21.wcnf | O = N/A T = TO |
O = 281 T = 166.27 (out)(err) |
O = 57416 T = 239.44 (out)(err) |
| dds1.wcnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
| dds4.wcnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
| test1.wcnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = 66831 T = 27.72 (out)(err) |
| test2.wcnf | O = N/A T = TO |
O = 274 T = 194.13 (out)(err) |
O = 103615 T = 87.31 (out)(err) |
| test3.wcnf | O = N/A T = TO |
O = 414 T = 161.46 (out)(err) |
O = 456173 T = 237.67 (out)(err) |
| test4.wcnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = 726685 T = 239.06 (out)(err) |
| mancoosi-test-i1000d0u98-0.wcnf | O = 107076495 T = 45.51 |
O = 107076495 T = 45.51 (out)(err) |
O = 68012273556 T = 148.36 (out)(err) |
| mancoosi-test-i1000d0u98-1.wcnf | O = 122084955 T = 63.77 |
O = 122084955 T = 63.77 (out)(err) |
O = 52008391880 T = 156.34 (out)(err) |
| mancoosi-test-i1000d0u98-10.wcnf | O = 152083527 T = 34.20 |
O = 152083527 T = 34.20 (out)(err) |
O = 18424944401 T = 97.55 (out)(err) |
| mancoosi-test-i1000d0u98-11.wcnf | O = 122139402 T = 4.22 |
O = 122139402 T = 4.22 (out)(err) |
O = 51662799212 T = 152.06 (out)(err) |
| mancoosi-test-i1000d0u98-12.wcnf | O = 77077762 T = 249.64 |
O = 77077762 T = 249.64 (out)(err) |
O = 35509978 T = 260.68 (out)(err) |
| mancoosi-test-i1000d0u98-13.wcnf | O = 182245730 T = 6.81 |
O = 182245730 T = 6.81 (out)(err) |
O = 84316232889 T = 150.33 (out)(err) |
| mancoosi-test-i1000d0u98-14.wcnf | O = 137147806 T = 170.12 |
O = 137147806 T = 170.12 (out)(err) |
O = 51513095810 T = 217.52 (out)(err) |
| mancoosi-test-i1000d0u98-15.wcnf | O = 92031744 T = 23.87 |
O = 92031744 T = 23.87 (out)(err) |
O = 51798474712 T = 123.65 (out)(err) |
| mancoosi-test-i1000d0u98-16.wcnf | O = 137075245 T = 26.44 |
O = 137075245 T = 26.44 (out)(err) |
O = 51888343070 T = 121.49 (out)(err) |
| mancoosi-test-i1000d0u98-17.wcnf | O = 152192544 T = 98.36 |
O = 152192544 T = 98.36 (out)(err) |
O = 84706651795 T = 243.00 (out)(err) |
| mancoosi-test-i1000d0u98-18.wcnf | O = 152228825 T = 6.46 |
O = 152228825 T = 6.46 (out)(err) |
O = 67621455055 T = 140.22 (out)(err) |
| mancoosi-test-i1000d0u98-19.wcnf | O = 92049939 T = 47.26 |
O = 92049939 T = 47.26 (out)(err) |
O = 18484487630 T = 151.92 (out)(err) |
| mancoosi-test-i1000d0u98-2.wcnf | O = 77059701 T = 6.44 |
O = 77059701 T = 6.44 (out)(err) |
O = 68282 T = 149.24 (out)(err) |
| mancoosi-test-i1000d0u98-20.wcnf | O = 122103134 T = 278.08 |
O = 122103134 T = 278.08 (out)(err) |
O = 84736378017 T = 124.29 (out)(err) |
| mancoosi-test-i1000d0u98-21.wcnf | O = 77041487 T = 70.66 |
O = 77041487 T = 70.66 (out)(err) |
O = 18514741284 T = 200.21 (out)(err) |
| mancoosi-test-i1000d0u98-22.wcnf | O = 92086312 T = 35.39 |
O = 92086312 T = 35.39 (out)(err) |
O = 51498232797 T = 156.91 (out)(err) |
| mancoosi-test-i1000d0u98-23.wcnf | O = 62014822 T = 6.73 |
O = 62014822 T = 6.73 (out)(err) |
O = 68312 T = 180.26 (out)(err) |
| mancoosi-test-i1000d0u98-24.wcnf | O = 167273676 T = 32.64 |
O = 167273676 T = 32.64 (out)(err) |
O = 51482715596 T = 182.40 (out)(err) |
| mancoosi-test-i1000d0u98-3.wcnf | O = 91959146 T = 50.21 |
O = 91959146 T = 50.21 (out)(err) |
O = 67967303338 T = 217.37 (out)(err) |
| mancoosi-test-i1000d0u98-4.wcnf | O = 122175781 T = 8.99 |
O = 122175781 T = 8.99 (out)(err) |
O = 67921896016 T = 216.74 (out)(err) |
| mancoosi-test-i1000d0u98-5.wcnf | O = 107058295 T = 80.17 |
O = 107058295 T = 80.17 (out)(err) |
O = 83895815318 T = 36.91 (out)(err) |
| mancoosi-test-i1000d0u98-6.wcnf | O = 137093314 T = 7.14 |
O = 137093314 T = 7.14 (out)(err) |
O = 51558339522 T = 104.44 (out)(err) |
| mancoosi-test-i1000d0u98-7.wcnf | O = 92104395 T = 14.03 |
O = 92104395 T = 14.03 (out)(err) |
O = 843915482 T = 93.25 (out)(err) |
| mancoosi-test-i1000d0u98-8.wcnf | O = 137057008 T = 148.68 |
O = 137057008 T = 148.68 (out)(err) |
O = 51618245 T = 208.31 (out)(err) |
| mancoosi-test-i1000d0u98-9.wcnf | O = 167164758 T = 6.38 |
O = 167164758 T = 6.38 (out)(err) |
O = 18379374068 T = 218.72 (out)(err) |
| mancoosi-test-i2000d0u98-25.wcnf | O = 332548069 T = 154.03 |
O = 332548069 T = 154.03 (out)(err) |
O = 224078437 T = 89.17 (out)(err) |
| mancoosi-test-i2000d0u98-26.wcnf | O = 302513043 T = 142.14 |
O = 302513043 T = 142.14 (out)(err) |
O = 255018186 T = 134.94 (out)(err) |
| mancoosi-test-i2000d0u98-27.wcnf | O = 317557787 T = 279.34 |
O = 317557787 T = 279.34 (out)(err) |
O = 66584748641 T = 99.49 (out)(err) |
| mancoosi-test-i2000d0u98-28.wcnf | O = 287468291 T = 203.04 |
O = 287468291 T = 203.04 (out)(err) |
O = 192747978917 T = 126.70 (out)(err) |
| mancoosi-test-i2000d0u98-29.wcnf | O = 332675238 T = 278.10 |
O = 332675238 T = 278.10 (out)(err) |
O = 35674761396 T = 232.21 (out)(err) |
| mancoosi-test-i2000d0u98-30.wcnf | O = 212389892 T = 14.91 |
O = 212389892 T = 14.91 (out)(err) |
O = 224243276002 T = 180.98 (out)(err) |
| mancoosi-test-i2000d0u98-31.wcnf | O = 302585711 T = 159.75 |
O = 302585711 T = 159.75 (out)(err) |
O = 192507935805 T = 95.21 (out)(err) |
| mancoosi-test-i2000d0u98-32.wcnf | O = 422762096 T = 80.13 |
O = 422762096 T = 80.13 (out)(err) |
O = 161267054 T = 217.35 (out)(err) |
| mancoosi-test-i2000d0u98-33.wcnf | O = 347574599 T = 279.98 |
O = 347574599 T = 279.98 (out)(err) |
O = 224123080905 T = 213.46 (out)(err) |
| mancoosi-test-i2000d0u98-34.wcnf | O = 317448770 T = 261.07 |
O = 317448770 T = 261.07 (out)(err) |
O = 2567 T = 228.94 (out)(err) |
| mancoosi-test-i2000d0u98-35.wcnf | O = 407608342 T = 242.98 |
O = 407608342 T = 242.98 (out)(err) |
O = 224198740860 T = 70.28 (out)(err) |
| mancoosi-test-i2000d0u98-36.wcnf | O = 332566184 T = 6.19 |
O = 332566184 T = 6.19 (out)(err) |
O = 192402859440 T = 83.28 (out)(err) |
| mancoosi-test-i2000d0u98-37.wcnf | O = 437697880 T = 289.55 |
O = 437697880 T = 289.55 (out)(err) |
O = 254897955323 T = 63.25 (out)(err) |
| mancoosi-test-i2000d0u98-38.wcnf | O = 332620778 T = 83.84 |
O = 332620778 T = 83.84 (out)(err) |
O = 1 T = 149.36 (out)(err) |
| mancoosi-test-i2000d0u98-39.wcnf | O = 392636177 T = 256.11 |
O = 392636177 T = 256.11 (out)(err) |
O = 129440810002 T = 98.07 (out)(err) |
| mancoosi-test-i2000d0u98-40.wcnf | O = 197399502 T = 3.72 |
O = 197399502 T = 3.72 (out)(err) |
O = 1 T = 204.13 (out)(err) |
| mancoosi-test-i2000d0u98-41.wcnf | O = 422780296 T = 16.58 |
O = 422780296 T = 16.58 (out)(err) |
O = 98020156146 T = 217.17 (out)(err) |
| mancoosi-test-i2000d0u98-42.wcnf | O = 317539561 T = 213.09 |
O = 317539561 T = 213.09 (out)(err) |
O = 129605921266 T = 220.99 (out)(err) |
| mancoosi-test-i2000d0u98-43.wcnf | O = 242443033 T = 140.66 |
O = 242443033 T = 140.66 (out)(err) |
O = 128479272192 T = 68.19 (out)(err) |
| mancoosi-test-i2000d0u98-44.wcnf | O = 227380053 T = 57.88 |
O = 227380053 T = 57.88 (out)(err) |
O = 160996486363 T = 157.76 (out)(err) |
| mancoosi-test-i2000d0u98-45.wcnf | O = 227398249 T = 152.62 |
O = 227398249 T = 152.62 (out)(err) |
O = 160019956980 T = 39.03 (out)(err) |
| mancoosi-test-i2000d0u98-46.wcnf | O = 422707588 T = 244.68 |
O = 422707588 T = 244.68 (out)(err) |
O = 129365895340 T = 238.13 (out)(err) |
| mancoosi-test-i2000d0u98-47.wcnf | O = 332566202 T = 98.79 |
O = 332566202 T = 98.79 (out)(err) |
O = 98275771762 T = 147.99 (out)(err) |
| mancoosi-test-i2000d0u98-48.wcnf | O = 377773202 T = 82.34 |
O = 377773202 T = 82.34 (out)(err) |
O = 98305751725 T = 222.94 (out)(err) |
| mancoosi-test-i2000d0u98-49.wcnf | O = 212353539 T = 124.88 |
O = 212353539 T = 124.88 (out)(err) |
O = 97929796878 T = 137.76 (out)(err) |
| mancoosi-test-i3000d0u98-50.wcnf | O = 527911892 T = 287.14 |
O = 527911892 T = 287.14 (out)(err) |
O = 283 T = 184.31 (out)(err) |
| mancoosi-test-i3000d0u98-51.wcnf | O = 618162431 T = 226.96 |
O = 618162431 T = 226.96 (out)(err) |
O = 191785768488 T = 139.74 (out)(err) |
| mancoosi-test-i3000d0u98-52.wcnf | O = 798463185 T = 249.13 |
O = 798463185 T = 249.13 (out)(err) |
O = 1907943 T = 85.64 (out)(err) |
| mancoosi-test-i3000d0u98-53.wcnf | O = 588163614 T = 227.21 |
O = 588163614 T = 227.21 (out)(err) |
O = 143475735873 T = 42.96 (out)(err) |
| mancoosi-test-i3000d0u98-54.wcnf | O = 738429559 T = 273.62 |
O = 738429559 T = 273.62 (out)(err) |
O = 144136906036 T = 145.87 (out)(err) |
| mancoosi-test-i3000d0u98-55.wcnf | O = 542992950 T = 225.46 |
O = 542992950 T = 225.46 (out)(err) |
O = 236610250984 T = 151.54 (out)(err) |
| mancoosi-test-i3000d0u98-56.wcnf | O = 648160920 T = 76.46 |
O = 648160920 T = 76.46 (out)(err) |
O = 2373471 T = 94.09 (out)(err) |
| mancoosi-test-i3000d0u98-57.wcnf | O = 437806859 T = 278.52 |
O = 437806859 T = 278.52 (out)(err) |
O = 19085 T = 91.16 (out)(err) |
| mancoosi-test-i3000d0u98-58.wcnf | O = 648142814 T = 264.97 |
O = 648142814 T = 264.97 (out)(err) |
O = 237467056655 T = 141.49 (out)(err) |
| mancoosi-test-i3000d0u98-59.wcnf | O = 588127263 T = 257.03 |
O = 588127263 T = 257.03 (out)(err) |
O = 97163895044 T = 89.93 (out)(err) |
| mancoosi-test-i3000d0u98-60.wcnf | O = 768373654 T = 259.59 |
O = 768373654 T = 259.59 (out)(err) |
O = 330496566741 T = 193.50 (out)(err) |
| mancoosi-test-i3000d0u98-61.wcnf | O = 678323157 T = 180.47 |
O = 678323157 T = 180.47 (out)(err) |
O = 9737434 T = 209.32 (out)(err) |
| mancoosi-test-i3000d0u98-62.wcnf | O = 542956700 T = 190.08 |
O = 542956700 T = 190.08 (out)(err) |
O = 97960177139 T = 90.35 (out)(err) |
| mancoosi-test-i3000d0u98-63.wcnf | O = 528002753 T = 234.82 |
O = 528002753 T = 234.82 (out)(err) |
O = 143896516802 T = 103.29 (out)(err) |
| mancoosi-test-i3000d0u98-64.wcnf | O = 723257578 T = 213.99 |
O = 723257578 T = 213.99 (out)(err) |
O = 283343235470 T = 222.32 (out)(err) |
| mancoosi-test-i3000d0u98-65.wcnf | O = 738356811 T = 242.57 |
O = 738356811 T = 242.57 (out)(err) |
O = 237421649746 T = 178.25 (out)(err) |
| mancoosi-test-i3000d0u98-66.wcnf | O = 573046158 T = 273.96 |
O = 573046158 T = 273.96 (out)(err) |
O = 470874970235 T = 145.86 (out)(err) |
| mancoosi-test-i3000d0u98-67.wcnf | O = 678214110 T = 127.86 |
O = 678214110 T = 127.86 (out)(err) |
O = 23761774029 T = 95.43 (out)(err) |
| mancoosi-test-i3000d0u98-68.wcnf | O = 573064364 T = 283.63 |
O = 573064364 T = 283.63 (out)(err) |
O = 330211024377 T = 189.02 (out)(err) |
| mancoosi-test-i3000d0u98-69.wcnf | O = 813453413 T = 236.14 |
O = 813453413 T = 236.14 (out)(err) |
O = 2839 T = 99.00 (out)(err) |
| mancoosi-test-i3000d0u98-70.wcnf | O = 588163640 T = 251.71 |
O = 588163640 T = 251.71 (out)(err) |
O = 144061991609 T = 95.53 (out)(err) |
| mancoosi-test-i3000d0u98-71.wcnf | O = 482995744 T = 211.91 |
O = 482995744 T = 211.91 (out)(err) |
O = 236911 T = 86.15 (out)(err) |
| mancoosi-test-i3000d0u98-72.wcnf | O = 633043474 T = 122.00 |
O = 633043474 T = 122.00 (out)(err) |
O = 236956134266 T = 167.86 (out)(err) |
| mancoosi-test-i3000d0u98-73.wcnf | O = 648160983 T = 121.51 |
O = 648160983 T = 121.51 (out)(err) |
O = 377770272684 T = 233.14 (out)(err) |
| mancoosi-test-i3000d0u98-74.wcnf | O = 708376403 T = 3.85 |
O = 708376403 T = 3.85 (out)(err) |
O = 144903316433 T = 100.25 (out)(err) |
| mancoosi-test-i4000d0u98-75.wcnf | O = 963701214 T = 194.43 |
O = 963701214 T = 194.43 (out)(err) |
O = 251907554841 T = 155.09 (out)(err) |
| mancoosi-test-i4000d0u98-76.wcnf | O = 963810321 T = 149.83 |
O = 963810321 T = 149.83 (out)(err) |
O = 621967314147 T = 153.89 (out)(err) |
| mancoosi-test-i4000d0u98-77.wcnf | O = 993917895 T = 208.46 |
O = 993917895 T = 208.46 (out)(err) |
O = 37463006 T = 160.85 (out)(err) |
| mancoosi-test-i4000d0u98-78.wcnf | O = 1144092925 T = 211.40 |
O = 1144092925 T = 211.40 (out)(err) |
O = 37805 T = 91.58 (out)(err) |
| mancoosi-test-i4000d0u98-79.wcnf | O = 978854921 T = 4.53 |
O = 978854921 T = 4.53 (out)(err) |
O = 4367 T = 162.89 (out)(err) |
| mancoosi-test-i4000d0u98-80.wcnf | O = 1053915295 T = 222.74 |
O = 1053915295 T = 222.74 (out)(err) |
O = 254327163 T = 79.46 (out)(err) |
| mancoosi-test-i4000d0u98-81.wcnf | O = 1264360186 T = 223.84 |
O = 1264360186 T = 223.84 (out)(err) |
O = 37572674728 T = 221.12 (out)(err) |
| mancoosi-test-i4000d0u98-82.wcnf | O = 1174164208 T = 281.38 |
O = 1174164208 T = 281.38 (out)(err) |
O = 375606443532 T = 160.61 (out)(err) |
| mancoosi-test-i4000d0u98-83.wcnf | O = 1069032771 T = 54.04 |
O = 1069032771 T = 54.04 (out)(err) |
O = 190103081502 T = 130.86 (out)(err) |
| mancoosi-test-i4000d0u98-84.wcnf | O = 1069069040 T = 240.59 |
O = 1069069040 T = 240.59 (out)(err) |
O = 376087331068 T = 181.82 (out)(err) |
| mancoosi-test-i4000d0u98-85.wcnf | O = 903703949 T = 270.00 |
O = 903703949 T = 270.00 (out)(err) |
O = 313727364494 T = 84.58 (out)(err) |
| mancoosi-test-i4000d0u98-86.wcnf | O = 963773861 T = 92.62 |
O = 963773861 T = 92.62 (out)(err) |
O = 250810922648 T = 50.30 (out)(err) |
| mancoosi-test-i4000d0u98-87.wcnf | O = 1038852305 T = 278.58 |
O = 1038852305 T = 278.58 (out)(err) |
O = 190478891409 T = 158.68 (out)(err) |
| mancoosi-test-i4000d0u98-88.wcnf | O = 768428227 T = 24.49 |
O = 768428227 T = 24.49 (out)(err) |
O = 2 T = 156.19 (out)(err) |
| mancoosi-test-i4000d0u98-89.wcnf | O = 963791998 T = 254.13 |
O = 963791998 T = 254.13 (out)(err) |
O = 374840487510 T = 96.85 (out)(err) |
| mancoosi-test-i4000d0u98-90.wcnf | O = 858624129 T = 213.13 |
O = 858624129 T = 213.13 (out)(err) |
O = 37 T = 87.30 (out)(err) |
| mancoosi-test-i4000d0u98-91.wcnf | O = 1008889969 T = 100.80 |
O = 1008889969 T = 100.80 (out)(err) |
O = 497 T = 82.68 (out)(err) |
| mancoosi-test-i4000d0u98-92.wcnf | O = 723402935 T = 44.31 |
O = 723402935 T = 44.31 (out)(err) |
O = 499019936243 T = 123.79 (out)(err) |
| mancoosi-test-i4000d0u98-93.wcnf | O = 888640890 T = 25.88 |
O = 888640890 T = 25.88 (out)(err) |
O = 18984775 T = 140.68 (out)(err) |
| mancoosi-test-i4000d0u98-94.wcnf | O = 1084041090 T = 259.55 |
O = 1084041090 T = 259.55 (out)(err) |
O = 375501 T = 177.34 (out)(err) |
| mancoosi-test-i4000d0u98-95.wcnf | O = 1068996342 T = 39.64 |
O = 1068996342 T = 39.64 (out)(err) |
O = 375 T = 104.96 (out)(err) |
| mancoosi-test-i4000d0u98-96.wcnf | O = 1099031365 T = 241.93 |
O = 1099031365 T = 241.93 (out)(err) |
O = 43658 T = 188.22 (out)(err) |
| mancoosi-test-i4000d0u98-97.wcnf | O = 1159174032 T = 244.86 |
O = 1159174032 T = 244.86 (out)(err) |
O = 3760 T = 183.84 (out)(err) |
| mancoosi-test-i4000d0u98-98.wcnf | O = 1038834155 T = 227.04 |
O = 1038834155 T = 227.04 (out)(err) |
O = 2523 T = 180.03 (out)(err) |
| mancoosi-test-i4000d0u98-99.wcnf | O = 873650677 T = 39.95 |
O = 873650677 T = 39.95 (out)(err) |
O = 313186298280 T = 194.32 (out)(err) |