This page collects experimental results conducted with small polynomial path orders as implemented in our complexity analyser TcT, version 2.0 (executable, config, test-file). All Experiments were conducted on a computer with 8 Dual Core AMD Opteron™ 885 processors, with a timeout of 10 seconds.

Experiments cover the following techniques:

MPO	multiset path orders over quasi precedences
LMPO	lightweight multiset path orders over quasi precedences
POP*	polynomial path orders over quasi precedences
sPOP*	small polynomial path orders over quasi precedences
sPOP* (PS)	small polynomial path orders with parameter substitution, over quasi precedences
semantic (rel)	matrix and polynomial interpretations used iteratively in a relative setting, compare ZK'10. The degree and dimension of matrices is gradually increased.
semantic + sPOP* (rel)	as above, but including small polynomial path orders with parameter substitution

In Table TC we collect experimental data on a testbed which collects a subset of 597 examples from the termination problem database, version 8.0. This subset was obtained by restricting the runtime complexity problem set to constructor TRSs that are known to be terminating.

In Table TCO we compare small polynomial path orders to various similar techniques as in Table TC, but the testbed has been restricted additionally to orthogonal systems. Conclusively this testbed allows us to conclude polytime computability from polynomially bounded runtime complexity.