Termination Competition 2015
General Information wc = 300 a = 1 b = 1 c = 0.1 ( 2015-08-05 18:48:18.60928 UTC ) 51787 pairs, 12024641.5 / 6232857.3 s finished in 399686h 5m 50s
Termination of Term Rewriting (and Transition Systems)
finished in 399686h 5m 50s, 33684 pairs, 6726808.6 / 3493948.5 s
Combined Ranking (Rules):
- 1. AProVE 2015 (20)
- 2. TTT2 (10)
- NaTT 1.3 (10)
- 4. matchbox2015-07-26.1 (7)
- 5. muterm 5.17 (6)
- 6. AProVE certified (3)
- 7. T2 - 2015-07-09 - 13745bd6 (2)
- Wanda (2)
- 9. AProVE certified TRS Standard (1)
- 10. cycsrs-29-07-2015.5 (0)
- AutoNon 1.21 (0)
- Ctrl (0)
| category | post-proc | rankings | statistics |
|---|---|---|---|
| TRS Standard | plain.3 | AProVE 2015 (1310), NaTT 1.3 (1023), TTT2 (989), muterm 5.17 (834), Wanda (636), matchbox2015-07-26.1 (524), AutoNon 1.21 (228), | 10486 pairs, 1666958.3 / 824051.3 s |
| SRS Standard | plain.3 | AProVE 2015 (832), TTT2 (598), matchbox2015-07-26.1 (365), NaTT 1.3 (202), muterm 5.17 (135), AutoNon 1.21 (58), | 7890 pairs, 2570235.3 / 1324912.6 s |
| Cycles | plain.3 | matchbox2015-07-26.1 (646), cycsrs-29-07-2015.5 (422), | 2630 pairs, 950125.9 / 453572.0 s |
| TRS Relative | plain.3 | NaTT 1.3 (70), AProVE 2015 (55), TTT2 (41), matchbox2015-07-26.1 (40), | 392 pairs, 77146.9 / 34711.5 s |
| SRS Relative | plain.3 | AProVE 2015 (88), matchbox2015-07-26.1 (32), TTT2 (24), NaTT 1.3 (17), | 820 pairs, 274225.6 / 145649.5 s |
| TRS Standard certified | ceta-2.20-2 | AProVE certified TRS Standard (1223), TTT2 (962), | 2996 pairs, 251319.4 / 124453.7 s |
| SRS Standard certified | ceta-2.20-2 | AProVE certified (816), TTT2 (570), | 2630 pairs, 486311.2 / 223843.9 s |
| TRS Relative certified | ceta-2.20-2 | AProVE certified (51), TTT2 (41), | 196 pairs, 29112.5 / 17898.6 s |
| SRS Relative certified | ceta-2.20-2 | AProVE certified (88), TTT2 (20), | 410 pairs, 76372.8 / 46591.8 s |
| TRS Equational | plain.3 | AProVE 2015 (67), muterm 5.17 (63), | 152 pairs, 3067.0 / 3466.0 s |
| TRS Conditional | plain.3 | muterm 5.17 (101), AProVE 2015 (85), | 234 pairs, 5576.4 / 5099.8 s |
| TRS Context Sensitive | plain.3 | muterm 5.17 (98), AProVE 2015 (97), | 216 pairs, 7100.2 / 5007.1 s |
| TRS Innermost | plain.3 | AProVE 2015 (273), muterm 5.17 (203), | 732 pairs, 102735.3 / 77628.8 s |
| Integer Transition Systems | plain.3 | T2 - 2015-07-09 - 13745bd6 (1061), AProVE 2015 (1034), Ctrl (423), | 3666 pairs, 212567.8 / 200512.7 s |
| Integer TRS | plain.3 | AProVE 2015 (102), Ctrl (85), | 234 pairs, 13954.0 / 6549.1 s |
Complexity Analysis of Term Rewriting
finished in 399683h 19m 8s, 14796 pairs, 5140915.1 / 2607632.9 s
Combined Ranking (Rules):
- 1. TCT3_2015 (6)
- 2. AProVE 2015 (4)
- 3. AProVE certified (1)
- matchbox2015-07-26.1 (1)
- 5. TCT2_20150725 (0)
| category | post-proc | rankings | statistics |
|---|---|---|---|
| Derivational Complexity - Full Rewriting | plain.3 | TCT3_2015 (853), matchbox2015-07-26.1 (369), TCT2_20150725 (0), | 5427 pairs, 2534205.9 / 1205378.3 s |
| Runtime Complexity - Full Rewriting | plain.3 | AProVE 2015 (1218), TCT3_2015 (414), TCT2_20150725 (0), | 2877 pairs, 791627.1 / 439245.3 s |
| Runtime Complexity - Innermost Rewriting | plain.3 | AProVE 2015 (2102), TCT3_2015 (769), TCT2_20150725 (0), | 3246 pairs, 916945.1 / 491516.2 s |
| Runtime Complexity - Innermost Rewriting certified | ceta-2.20-2 | TCT3_2015 (689), AProVE certified (495), TCT2_20150725 (0), | 3246 pairs, 898136.9 / 471493.2 s |
Termination of Programming Languages
finished in 399683h 22m 25s, 3307 pairs, 156917.9 / 131275.9 s
Combined Ranking (Rules):
- 1. UltimateBuchiAutomizer (3)
- 2. HipTNT+ v3 (2)
- AProVE 2015 (2)
| category | post-proc | rankings | statistics |
|---|---|---|---|
| C | plain.3 | UltimateBuchiAutomizer (277), AProVE 2015 (252), HipTNT+ v3 (249), | 1416 pairs, 84389.0 / 85616.8 s |
| C Integer Programs | plain.3 | HipTNT+ v3 (305), UltimateBuchiAutomizer (295), AProVE 2015 (289), | 1005 pairs, 40026.8 / 22753.0 s |
| Java Bytecode | plain.3 | AProVE 2015 (410), UltimateBuchiAutomizer (141), | 886 pairs, 32502.0 / 22906.2 s |