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