YES(?,ELEMENTARY) 'epo* (timeout of 60.0 seconds)' -------------------------------- Answer: YES(?,ELEMENTARY) Input Problem: innermost runtime-complexity with respect to Rules: { filter(cons(X), 0(), M) -> cons(0()) , filter(cons(X), s(N), M) -> cons(X) , sieve(cons(0())) -> cons(0()) , sieve(cons(s(N))) -> cons(s(N)) , nats(N) -> cons(N) , zprimes() -> sieve(nats(s(s(0()))))} Proof Output: Strict Rules in Predicative Notation: { filter(; cons(; X), 0(), M) -> cons(; 0()) , filter(; cons(; X), s(; N), M) -> cons(; X) , sieve(; cons(; 0())) -> cons(; 0()) , sieve(; cons(; s(; N))) -> cons(; s(; N)) , nats(; N) -> cons(; N) , zprimes() -> sieve(; nats(; s(; s(; 0()))))} Safe Mapping: safe(filter) = {1, 2, 3}, safe(cons) = {1}, safe(0) = {}, safe(s) = {1}, safe(sieve) = {1}, safe(nats) = {1}, safe(zprimes) = {} Argument Permutation: mu(filter) = [3, 1, 2], mu(sieve) = [1], mu(nats) = [1], mu(zprimes) = [] Precedence: zprimes ~ zprimes, zprimes > nats, zprimes > sieve, zprimes > filter, nats ~ nats, nats ~ sieve, nats > filter, sieve ~ nats, sieve ~ sieve, sieve > filter, filter ~ filter