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