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