YES(?,ELEMENTARY)

'epo* (timeout of 60.0 seconds)'
--------------------------------
Answer:           YES(?,ELEMENTARY)
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  D(t()) -> 1()
     , D(constant()) -> 0()
     , D(+(x, y)) -> +(D(x), D(y))
     , D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
     , D(-(x, y)) -> -(D(x), D(y))
     , D(minus(x)) -> minus(D(x))
     , D(div(x, y)) -> -(div(D(x), y), div(*(x, D(y)), pow(y, 2())))
     , D(ln(x)) -> div(D(x), x)
     , D(pow(x, y)) ->
       +(*(*(y, pow(x, -(y, 1()))), D(x)), *(*(pow(x, y), ln(x)), D(y)))}

Proof Output:    
  Strict Rules in Predicative Notation:
   {  D(t();) -> 1()
    , D(constant();) -> 0()
    , D(+(; x, y);) -> +(; D(x;), D(y;))
    , D(*(; x, y);) -> +(; *(; y, D(x;)), *(; x, D(y;)))
    , D(-(; x, y);) -> -(; D(x;), D(y;))
    , D(minus(; x);) -> minus(; D(x;))
    , D(div(; x, y);) ->
      -(; div(; D(x;), y), div(; *(; x, D(y;)), pow(; y, 2())))
    , D(ln(; x);) -> div(; D(x;), x)
    , D(pow(; x, y);) ->
      +(; *(; *(; y, pow(; x, -(; y, 1()))), D(x;)),
          *(; *(; pow(; x, y), ln(; x)), D(y;)))}
  Safe Mapping:
   safe(D) = {}, safe(t) = {}, safe(1) = {}, safe(constant) = {},
   safe(0) = {}, safe(+) = {1, 2}, safe(*) = {1, 2}, safe(-) = {1, 2},
   safe(minus) = {1}, safe(div) = {1, 2}, safe(pow) = {1, 2},
   safe(2) = {}, safe(ln) = {1}
  Argument Permutation:
   mu(D) = [1]
  Precedence:
   D ~ D