YES(?,ELEMENTARY) 'epo* (timeout of 60.0 seconds)' -------------------------------- Answer: YES(?,ELEMENTARY) Input Problem: innermost runtime-complexity with respect to Rules: { f(g(x)) -> g(g(f(x))) , f(g(x)) -> g(g(g(x)))} Proof Output: Strict Rules in Predicative Notation: { f(g(; x);) -> g(; g(; f(x;))) , f(g(; x);) -> g(; g(; g(; x)))} Safe Mapping: safe(f) = {}, safe(g) = {1} Argument Permutation: mu(f) = [1] Precedence: f ~ f