YES(?,ELEMENTARY)

'epo* (timeout of 60.0 seconds)'
--------------------------------
Answer:           YES(?,ELEMENTARY)
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  a__eq(0(), 0()) -> true()
     , a__eq(s(X), s(Y)) -> a__eq(X, Y)
     , a__eq(X, Y) -> false()
     , a__inf(X) -> cons(X, inf(s(X)))
     , a__take(0(), X) -> nil()
     , a__take(s(X), cons(Y, L)) -> cons(Y, take(X, L))
     , a__length(nil()) -> 0()
     , a__length(cons(X, L)) -> s(length(L))
     , mark(eq(X1, X2)) -> a__eq(X1, X2)
     , mark(inf(X)) -> a__inf(mark(X))
     , mark(take(X1, X2)) -> a__take(mark(X1), mark(X2))
     , mark(length(X)) -> a__length(mark(X))
     , mark(0()) -> 0()
     , mark(true()) -> true()
     , mark(s(X)) -> s(X)
     , mark(false()) -> false()
     , mark(cons(X1, X2)) -> cons(X1, X2)
     , mark(nil()) -> nil()
     , a__eq(X1, X2) -> eq(X1, X2)
     , a__inf(X) -> inf(X)
     , a__take(X1, X2) -> take(X1, X2)
     , a__length(X) -> length(X)}

Proof Output:    
  Strict Rules in Predicative Notation:
   {  a__eq(0(); 0()) -> true()
    , a__eq(s(; Y); s(; X)) -> a__eq(Y; X)
    , a__eq(Y; X) -> false()
    , a__inf(; X) -> cons(; X, inf(; s(; X)))
    , a__take(; 0(), X) -> nil()
    , a__take(; s(; X), cons(; Y, L)) -> cons(; Y, take(; X, L))
    , a__length(; nil()) -> 0()
    , a__length(; cons(; X, L)) -> s(; length(; L))
    , mark(eq(; X1, X2);) -> a__eq(X2; X1)
    , mark(inf(; X);) -> a__inf(; mark(X;))
    , mark(take(; X1, X2);) -> a__take(; mark(X1;), mark(X2;))
    , mark(length(; X);) -> a__length(; mark(X;))
    , mark(0();) -> 0()
    , mark(true();) -> true()
    , mark(s(; X);) -> s(; X)
    , mark(false();) -> false()
    , mark(cons(; X1, X2);) -> cons(; X1, X2)
    , mark(nil();) -> nil()
    , a__eq(X2; X1) -> eq(; X1, X2)
    , a__inf(; X) -> inf(; X)
    , a__take(; X1, X2) -> take(; X1, X2)
    , a__length(; X) -> length(; X)}
  Safe Mapping:
   safe(a__eq) = {1}, safe(0) = {}, safe(true) = {}, safe(s) = {1},
   safe(false) = {}, safe(a__inf) = {1}, safe(cons) = {1, 2},
   safe(inf) = {1}, safe(a__take) = {1, 2}, safe(nil) = {},
   safe(take) = {1, 2}, safe(a__length) = {1}, safe(length) = {1},
   safe(mark) = {}, safe(eq) = {1, 2}
  Argument Permutation:
   mu(a__eq) = [1, 2], mu(a__inf) = [1], mu(a__take) = [1, 2],
   mu(a__length) = [1], mu(mark) = [1]
  Precedence:
   mark ~ mark, mark > a__length, mark > a__take, mark > a__inf,
   mark > a__eq, a__length ~ a__length, a__length ~ a__take,
   a__length > a__inf, a__length > a__eq, a__take ~ a__length,
   a__take ~ a__take, a__take > a__inf, a__take > a__eq,
   a__inf ~ a__inf, a__eq > a__inf, a__eq ~ a__eq