Setup
Experiments have been run on the 2132 TRSs of TPDB version 7.0.2.
All of the proofs have been generated with TTT2 (changeset
a5b22ac1840e of the mercurial repository). Then, the generated proofs have
been certified using CeTA v1.10.
All Experiments have been performed on a machine with 8 Dual Core AMD
Opteron 885 processors and 64GB RAM running Linux.
- basic uses the dependency graph and the reduction pair processor with linear polynomial orders. Furthermore, some fast methods for finding nontermination are used: check whether the lhs is a variable, check whether the rhs contains a free variable, check whether the rhs contains a substitution instance of the lhs.
- sc is like basic where additionally the subterm criterion is used.
- ur is like basic where the reduction pair processor in combination with usable rules is added.
- sc_ur is simply the combination of sc and ur.
- full uses a combination of all techniques that are available in TTT2 and supported by CeTA.
Statistics
problem | basic_ttt2 | ceta1 | sc_ttt2 | ceta2 | ur_ttt2 | ceta3 | scur_ttt2 | ceta4 | full_ttt2 | ceta5 | ||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
#yes | 439 | 439 | 553 | 553 | 663 | 663 | 669 | 669 | 1223 | 1223 | ||||
total time | 1459.054 | 25.696 | 993.434 | 26.399 | 1390.208 | 43.379 | 1305.547 | 41.212 | 4247.826 | 90.385 | ||||
average time | 3.324 | 0.059 | 1.796 | 0.048 | 2.097 | 0.065 | 1.951 | 0.062 | 3.473 | 0.074 | ||||
#no | 125 | 125 | 125 | 125 | 125 | 125 | 125 | 125 | 221 | 221 | ||||
total time | 17.517 | 2.51 | 17.459 | 2.502 | 17.672 | 2.5 | 17.587 | 2.505 | 233.776 | 4.627 | ||||
average time | 0.14 | 0.02 | 0.14 | 0.02 | 0.141 | 0.02 | 0.141 | 0.02 | 1.058 | 0.021 | ||||
#maybe | 1406 | 0 | 1336 | 0 | 1215 | 0 | 1209 | 0 | 440 | 0 | ||||
total time | 5452.061 | 0.0 | 5078.596 | 0.0 | 5343.288 | 0.0 | 5212.156 | 0.0 | 16221.683 | 0.0 | ||||
average time | 3.878 | - | 3.801 | - | 4.398 | - | 4.311 | - | 36.867 | - | ||||
#timeout | 162 | 0 | 118 | 0 | 129 | 0 | 129 | 0 | 248 | 0 | ||||
total time | 9720.0 | 0.0 | 7080.0 | 0.0 | 7740.0 | 0.0 | 7740.0 | 0.0 | 14880.0 | 0.0 | ||||
average time | 60.0 | - | 60.0 | - | 60.0 | - | 60.0 | - | 60.0 | - | ||||
total time | 16648.631 | 28.206 | 13169.489 | 28.901 | 14491.167 | 45.879 | 14275.29 | 43.717 | 35583.286 | 95.011 | ||||
|