Summary

We first present the results where we compare CeTA with TTT2 as termination prover against the other combinations that have participated in the termination competition. The column TC+ represents the combination of TTT2 and CeTA, where all methods that are supported in version 1.03 of CeTA are used in the strategy of TTT2. In TC only those methods are used that are described in the TPHOLs 2009 paper (dependency graph decomposition and linear polynomial orders) have been used. In both combinations TC and TC+ coefficients where chosen between 0 and 3.
Note that the time for proof generation was not explicitly measured during the last certified termination competition, but was just added to the termination prover time. This is the reason for the question marks in the table below. (detailed results)

Whereas in the table above, for each TRS each configuration may have produced and certified a different proof, we also made an experiment where every time the same proof has to be certified. To this end we used AProVE with only those techniques that are supported by all three certifiers (EDG Dependency Graph estimation and linear polynomials), and then converted each of these proofs in the corresponding input formats for each of the certifiers. This resulted in 358 termination proofs which had to be certified by each of the certifiers. In this way we now compare only the execution time for checking a certificate of the same set of proofs.
We again used CeTA version 1.03 and for the other certifiers we took the most recent versions which were available to download on June 3, 2009 (CoLoR_090311.tgz, Rainbow_090318.tgz, coccinelle-1.5-8.2-1.tgz, CiME v3.02 built on 30/04/2009). All experiments have been performed on a standard PC equipped with a 2.4GHz CPU and 2GB RAM. (detailed results)

Within the columns of TC and TC+, click on the individual results to see the proof and the output of CeTA. For all other configurations we refer to the result table of the certified termination competition.