Data shown here is incomplete. This page will refresh with updates pulled from star-exec.

Termination Competition 2016

General Information wc_r = 30 wc_p = 300 a = 1 b = 1000 c = 1.0 ( 2016-09-05 22:36:25.176111 UTC ) 45112 of 45174 pairs, 1648726.1 / 678815.2 s

Termination of Term Rewriting (and Transition Systems)

34025 of 34083 pairs, 1196163.8 / 477503.2 s

Combined Ranking (Rules):
category post-proc rankings statistics
TRS Standard plain.4 AProVE standard f065806 (1272), NaTT 1.6 (1026), ttt2-v1.16 (1007), muterm 5.18 (827), Wanda (631), 7485 of 7490 pairs, 112229.9 / 51986.5 s
SRS Standard plain.4 AProVE standard f065806 (918), MultumNonMulta 3.6 (739), ttt2-v1.16 (722), pure-matchbox-2016-08-30.4 (558), NaTT 1.6 (185), muterm 5.18 (154), 9393 of 9414 pairs, 459082.1 / 178031.5 s
Cycles plain.4 pure-matchbox-2016-08-30.4 (733), cycsrs-100816 (627), CycNTA (104), 4068 pairs, 155110.2 / 75379.7 s
TRS Relative plain.4 NaTT 1.6 (71), AProVE standard f065806 (55), ttt2-v1.16 (41), 293 of 294 pairs, 10455.4 / 3247.1 s
SRS Relative plain.4 AProVE standard f065806 (78), MultumNonMulta 3.6 (52), ttt2-v1.16 (24), 614 of 615 pairs, 39262.8 / 14586.6 s
TRS Standard certified ceta-2.27.4 AProVE standard f065806 (1182), ttt2-v1.16 (937), 2992 of 2996 pairs, 84794.0 / 28525.2 s
SRS Standard certified ceta-2.27.4 AProVE standard f065806 (777), ttt2-v1.16 (605), 3114 of 3138 pairs, 222595.1 / 63881.4 s
TRS Relative certified ceta-2.27.4 AProVE standard f065806 (51), ttt2-v1.16 (44), 196 pairs, 6917.1 / 3218.1 s
SRS Relative certified ceta-2.27.4 AProVE standard f065806 (77), ttt2-v1.16 (27), 409 of 410 pairs, 28213.4 / 9718.3 s
TRS Equational plain.4 AProVE standard f065806 (64), muterm 5.18 (61), NaTT 1.6 (48), 228 pairs, 1509.3 / 1110.0 s
TRS Equational certified ceta-2.27.4 AProVE standard f065806 (62), NaTT 1.6 (13), 152 pairs, 927.4 / 542.9 s
TRS Conditional plain.4 muterm 5.18 (102), AProVE standard f065806 (84), 234 pairs, 1545.0 / 939.5 s
TRS Context Sensitive plain.4 muterm 5.18 (101), AProVE standard f065806 (97), 216 pairs, 1563.7 / 772.8 s
TRS Innermost plain.4 AProVE standard f065806 (260), muterm 5.18 (198), 731 of 732 pairs, 16616.2 / 9396.3 s
Integer Transition Systems plain.4 VeryMax-termCOMP16 (1034), AProVE standard f065806 (1009), Ctrl (348), 3666 pairs, 52910.8 / 35042.6 s
Integer TRS plain.4 AProVE standard f065806 (96), Ctrl (85), 234 pairs, 2431.3 / 1124.7 s

Complexity Analysis of Term Rewriting

9036 of 9038 pairs, 267544.1 / 102879.0 s

Combined Ranking (Rules):
category post-proc rankings statistics
Runtime Complexity - Full Rewriting plain.4 AProVE standard f065806 (2157), tct (1747), 1918 pairs, 63654.3 / 23924.6 s
Runtime Complexity - Innermost Rewriting plain.4 AProVE standard f065806 (2549), tct (2163), 2043 of 2044 pairs, 92266.1 / 32471.8 s
Runtime Complexity - Innermost Rewriting certified ceta-2.27.4 tct (669), AProVE standard f065806 (467), 2043 of 2044 pairs, 87941.8 / 31353.8 s
Complexity - Integer Transition Systems plain.4 AProVE standard f065806 (3533), CoFloCo+ ITS and C preprocessing final version (1693), tct (1428), Loopus (1323), 3032 pairs, 23681.9 / 15128.9 s

Termination of Programming Languages

1947 of 1949 pairs, 183197.1 / 96695.7 s

Combined Ranking (Rules):
category post-proc rankings statistics
C plain.4 AProVE llvm 5e5b89d (283), UltimateBuchiAutomizer (272), 943 of 944 pairs, 147983.3 / 82087.6 s
C Integer Programs plain.4 VeryMax-termCOMP16 (315), UltimateBuchiAutomizer (306), AProVE llvm 5e5b89d (283), 1004 of 1005 pairs, 35213.8 / 14608.1 s

Complexity Analysis of Programming Languages

finished in 417469h 4m 39s, 104 pairs, 1821.0 / 1737.3 s

Combined Ranking (Rules):
category post-proc rankings statistics
Complexity - C Integer Programs plain.4 Loopus (97), CoFloCo+ ITS and C preprocessing final version (81), AProVE c complexity (64), tct (13), 104 pairs, 1821.0 / 1737.3 s