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