René Thiemann noticed a serious bug in the implementation of KBO, which affects columns (4), (5), and KBO in Table 2. The new data is given below. Consequently, the claim in Section 5 that the termination of Example 33 (Battle of Hydra and Hercules) in [6] can be proved by TTT has to be retracted. (The bug has been corrected in the meantime.)
The data in column (6) is obtained with all argument filterings and the other options the same as for columns (4) and (5).
| (4) | (5) | KBO | (6) | ||
|---|---|---|---|---|---|
| [3, Example 3.3] | 129.57 | 0.00 | ?
| ||
| [3, Example 3.4] | 1.12 | 16.80 | 0.00 | 0.72 | |
| [3, Example 3.9] | 398.94 | ? | 0.00 | 6.66 | |
| [3, Example 3.11] | 2.25 | 33.92 | 0.00 | ? | |
| [3, Example 3.15] | 0.38 | 0.39 | 0.06 | 0.38 | |
| [3, Example 3.38] | 0.02 | 7.73 | 0.00 | 1.01 | |
| [3, Example 3.44] | 0.84 | 3.53 | 0.10 | 0.34 | |
| [4, Example 6] | 0.08 | 280.04 | 0.00 | 8.81 | |
| [6, Example 11] | 0.39 | 5.63 | 0.00 | 46.74 | |
| [6, Example 33] | 0.20 | 31.21 | 0.00 | 17.98 | |
| [15, Example 17] | 22.23 | ? | 0.00 | ? | |
| [16, Example 4.27] | 2.40 | 8.29 | 0.16 | 239.21 | |
| [16, Example 4.60] | 0.33 | 102.50 | 0.00 | 587.39 | |
| [17, Example 58] | 0.48 | 0.47 | 0.07 | 0.05 |