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))) , after(0(), XS) -> XS , after(s(N), cons(X, XS)) -> after(N, activate(XS)) , 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 after > from, after > activate, activate > from and safe mapping safe(from) = {1}, safe(cons) = {1, 2}, safe(n__from) = {1}, safe(s) = {1}, safe(after) = {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))) , after(0(); XS) -> XS , after(s(; N); cons(; X, XS)) -> after(N; activate(; XS)) , from(; X) -> n__from(; X) , activate(; n__from(; X)) -> from(; X) , activate(; X) -> X}