YES(?,POLY) 'Pop* with parameter subtitution (timeout of 60.0 seconds)' ----------------------------------------------------------- Answer: YES(?,POLY) Input Problem: innermost runtime-complexity with respect to Rules: { from(X) -> cons(X, n__from(s(X))) , sel(0(), cons(X, Y)) -> X , sel(s(X), cons(Y, Z)) -> sel(X, activate(Z)) , from(X) -> n__from(X) , activate(n__from(X)) -> from(X) , activate(X) -> X} Proof Output: The input was oriented with the instance of POP* as induced by the precedence sel > from, sel > activate, activate > from and safe mapping safe(from) = {1}, safe(cons) = {1, 2}, safe(n__from) = {1}, safe(s) = {1}, safe(sel) = {2}, safe(0) = {}, safe(activate) = {1} . For your convenience, here is the input in predicative notation: Rules: { from(; X) -> cons(; X, n__from(; s(; X))) , sel(0(); cons(; X, Y)) -> X , sel(s(; X); cons(; Y, Z)) -> sel(X; activate(; Z)) , from(; X) -> n__from(; X) , activate(; n__from(; X)) -> from(; X) , activate(; X) -> X}