Termination Competition 2014

General Information wc = 300 a = 100 b = 1000 c = 1.0 ( 2014-07-20 02:25:05.328531 UTC ) 37880 pairs, 7806889.5 / 3143466.2 s finished in 11h 41m 27s

Termination of Term Rewriting (and Transition Systems)

finished in 11h 41m 27s, 27599 pairs, 4280960.8 / 2004985.2 s

Combined Ranking (Rules):
category post-proc rankings statistics
TRS Standard plain AProVE_JRE2 (1312), NaTT (1024), TTT2 (997), mu-term 5.13 (856), Wanda (636), 7405 pairs, 416831.1 / 247239.1 s
SRS Standard plain AProVE_JRE2 (839), TTT2 (607), NaTT (204), mu-term 5.13 (139), 5260 pairs, 1078452.9 / 683824.1 s
TRS Relative plain AProVE_JRE2 (35), TTT2 (24), 88 pairs, 13062.8 / 4027.5 s
SRS Relative plain AProVE_JRE2 (89), TTT2 (25), 410 pairs, 106678.3 / 45449.7 s
TRS Standard certified ceta AProVE_JRE2 (1222), TTT2 (966), matchbox2014.07.08 (714), 4443 pairs, 774987.2 / 331790.1 s
SRS Standard certified ceta AProVE_JRE2 (819), matchbox2014.07.08 (584), TTT2 (572), 3945 pairs, 1465907.9 / 437506.9 s
TRS Relative certified ceta AProVE_JRE2 (31), TTT2 (24), 88 pairs, 13971.7 / 4898.0 s
SRS Relative certified ceta AProVE_JRE2 (89), TTT2 (23), 410 pairs, 96316.9 / 45322.1 s
TRS Equational plain AProVE_JRE2 (62), mu-term 5.13 (59), 142 pairs, 2898.8 / 2661.4 s
TRS Conditional plain mu-term 5.13 (25), AProVE_JRE2 (18), 64 pairs, 4401.4 / 2887.3 s
TRS Context Sensitive plain mu-term 5.13 (101), AProVE_JRE2 (98), 216 pairs, 8366.2 / 5349.0 s
TRS Innermost plain AProVE_JRE2 (273), mu-term 5.13 (211), 732 pairs, 124684.1 / 75201.2 s
Higher-Order rewriting (union beta) plain Wanda (152), THOR (121), 350 pairs, 3875.1 / 1409.1 s
Integer Transition Systems plain CppInv (747), T2 - 2014-07-06v1 (562), AProVE_JRE2 (217), Ctrl (184).

The results of CppInv and T2 are incomparable with those of AProVE and Ctrl, since they ran on different sets of examples. This is due to bugs in the translator from the SMTLIB-format to the formats of the tools.

3812 pairs, 156180.8 / 112903.0 s
Integer TRS plain AProVE_JRE2 (104), Ctrl (80), 234 pairs, 14345.7 / 4516.8 s

Complexity Analysis of Term Rewriting

finished in 10h 38m 43s, 8988 pairs, 3453948.0 / 1095372.9 s

Combined Ranking (Rules):
category post-proc rankings statistics
Derivational Complexity - Full Rewriting plain TCT (1575), CaT (1108), 3618 pairs, 1611245.4 / 474675.2 s
Runtime Complexity - Full Rewriting plain TCT (1505), CaT (889), 2578 pairs, 722622.5 / 236598.8 s
Runtime Complexity - Innermost Rewriting plain AProVE_JRE2 (2179), TCT (2082), 2792 pairs, 1120080.1 / 384098.9 s

Termination of Programming Languages

finished in 5h 26m 50s, 1293 pairs, 71980.7 / 43108.1 s

Combined Ranking (Rules):
category post-proc rankings statistics
C plain AProVE_JRE2 (296), UltimateBuchiAutomizer (271), T2 - 2014-07-06v1 (183), 1293 pairs, 71980.7 / 43108.1 s

General Information