YES(?,ELEMENTARY)

'epo* (timeout of 60.0 seconds)'
--------------------------------
Answer:           YES(?,ELEMENTARY)
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  dx(X()) -> 1()
     , dx(0()) -> 0()
     , dx(1()) -> 0()
     , dx(a()) -> 0()
     , dx(+(f, g)) -> +(dx(f), dx(g))
     , dx(*(f, g)) -> +(*(dx(f), g), *(dx(g), f))
     , dx(-(f, g)) -> -(dx(f), dx(g))
     , dx(neg(f)) -> neg(dx(f))
     , dx(/(f, g)) -> -(/(dx(f), g), /(*(dx(g), f), exp(g, 2())))
     , dx(ln(f)) -> /(dx(f), f)
     , dx(exp(f, g)) ->
       +(*(dx(f), *(exp(f, -(g, 1())), g)),
         *(dx(g), *(exp(f, g), ln(f))))}

Proof Output:    
  Strict Rules in Predicative Notation:
   {  dx(X();) -> 1()
    , dx(0();) -> 0()
    , dx(1();) -> 0()
    , dx(a();) -> 0()
    , dx(+(; f, g);) -> +(; dx(f;), dx(g;))
    , dx(*(; f, g);) -> +(; *(; dx(f;), g), *(; dx(g;), f))
    , dx(-(; f, g);) -> -(; dx(f;), dx(g;))
    , dx(neg(; f);) -> neg(; dx(f;))
    , dx(/(; f, g);) ->
      -(; /(; dx(f;), g), /(; *(; dx(g;), f), exp(; g, 2())))
    , dx(ln(; f);) -> /(; dx(f;), f)
    , dx(exp(; f, g);) ->
      +(; *(; dx(f;), *(; exp(; f, -(; g, 1())), g)),
          *(; dx(g;), *(; exp(; f, g), ln(; f))))}
  Safe Mapping:
   safe(dx) = {}, safe(X) = {}, safe(1) = {}, safe(0) = {},
   safe(a) = {}, safe(+) = {1, 2}, safe(*) = {1, 2}, safe(-) = {1, 2},
   safe(neg) = {1}, safe(/) = {1, 2}, safe(exp) = {1, 2},
   safe(2) = {}, safe(ln) = {1}
  Argument Permutation:
   mu(dx) = [1]
  Precedence:
   dx ~ dx