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