Our test suite consists of those 600 TRSs from the termination problem database 8.0, for which a nontermination proof was found by at least one tool in the termination competitions 2008-2011 (in most of these nontermination proofs, the evaluation strategy for the TRS is not restricted). For all of these 600 TRSs we called the termination tool AProVE to investigate innermost termination. To this end, we configured AProVE in a way similar to the termination competition 2011, but dropped some of the time-intensive techniques for proving termination, and increased the amount of nontermination techniques. The detailed configuration can be found in this file. Note that in the generated nontermination proofs, many techniques (e.g., reduction pair processor, usable rules, dependency graph, ...), are just printed as Pair and Rule Removal.

In the first run AProVE delivered several wrong answers and proofs, where the bug was in one of its two loop-finding methods: it completely ignored the innermost strategy. After this bug was fixed, AProVE detected 352 innermost nontermination proofs (and 103 innermost termination proofs) which could all be certified by CeTA.

Our experiments have been performed on a machine with two 2.8 GHz Quad-Core Intel Xeon processors and 6 GB of main memory using a 60 seconds timeout. In the result table one can click on the execution times to see the proofs and answers of CeTA (version 2.3).