First we performed three series of experiments: one with benchmarks from the paper and other LC(S)TRS examples we have collected, one with higher-order benchmarks from the termination problem database, and one with integer TRSs from the termination problem database. All experiments were performed using Z3 as a backend, and a 60 second timeout.
In addition, we have tested the effect of disabling one or more processors from the paper. This can be found in disable experiments.