YES(?,POLY) 'Pop* with parameter subtitution (timeout of 60.0 seconds)' ----------------------------------------------------------- Answer: YES(?,POLY) Input Problem: innermost runtime-complexity with respect to Rules: { first(0(), X) -> nil() , first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))) , from(X) -> cons(X, n__from(s(X))) , first(X1, X2) -> n__first(X1, X2) , from(X) -> n__from(X) , activate(n__first(X1, X2)) -> first(X1, X2) , 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 first > from, activate > from, first ~ activate and safe mapping safe(first) = {}, safe(0) = {}, safe(nil) = {}, safe(s) = {1}, safe(cons) = {1, 2}, safe(n__first) = {1, 2}, safe(activate) = {}, safe(from) = {1}, safe(n__from) = {1} . For your convenience, here is the input in predicative notation: Rules: { first(0(), X;) -> nil() , first(s(; X), cons(; Y, Z);) -> cons(; Y, n__first(; X, activate(Z;))) , from(; X) -> cons(; X, n__from(; s(; X))) , first(X1, X2;) -> n__first(; X1, X2) , from(; X) -> n__from(; X) , activate(n__first(; X1, X2);) -> first(X1, X2;) , activate(n__from(; X);) -> from(; X) , activate(X;) -> X}