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