Hey Johannes, The "new results" from the demo categories are not due to new methods or implementation, but just due to the fact that, e.g., for complexity AProVE keeps trying to improve the result until the timeout strikes, so there are some examples, where something happens just before (or after) the timeout. Hence, there are always a few different results every year. There has been some work on termination of term rewriting in AProVE, but mainly in the area of probabilistic and relative termination. E.g., for relative termination we developed a new variant of DPs that I am going to present at IJCAR, which we use in our strategy for relative TRS and also showcase in the relative SRS strategy. Many thanks also from me to Florian for all the work! Kind regards, Jan-Christoph