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