This page collects experimental results conducted with small polynomial path orders
as implemented in our complexity analyser TcT,
version 2.0 (executable, config, testfile).
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:
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.
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.