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):
- 1. AProVE_JRE2 (19)
- 2. TTT2 (5)
- 3. NaTT (4)
- 4. CppInv (3)
- mu-term 5.13 (3)
- 6. T2 - 2014-07-06v1 (2)
- 7. matchbox2014.07.08 (1)
- Wanda (1)
- 9. THOR (0)
- Ctrl (0)
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):
- 1. TCT (2)
- 2. AProVE_JRE2 (1)
- 3. CaT (0)
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):
- 1. AProVE_JRE2 (2)
- 2. UltimateBuchiAutomizer (1)
- 3. T2 - 2014-07-06v1 (0)
category | post-proc | rankings | statistics |
---|---|---|---|
C | plain | AProVE_JRE2 (296), UltimateBuchiAutomizer (271), T2 - 2014-07-06v1 (183), | 1293 pairs, 71980.7 / 43108.1 s |