MAYBE

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict Trs:
  { dx(X) -> one()
  , dx(a()) -> zero()
  , dx(plus(ALPHA, BETA)) -> plus(dx(ALPHA), dx(BETA))
  , dx(times(ALPHA, BETA)) ->
    plus(times(BETA, dx(ALPHA)), times(ALPHA, dx(BETA)))
  , dx(minus(ALPHA, BETA)) -> minus(dx(ALPHA), dx(BETA))
  , dx(neg(ALPHA)) -> neg(dx(ALPHA))
  , dx(div(ALPHA, BETA)) ->
    minus(div(dx(ALPHA), BETA),
          times(ALPHA, div(dx(BETA), exp(BETA, two()))))
  , dx(exp(ALPHA, BETA)) ->
    plus(times(BETA, times(exp(ALPHA, minus(BETA, one())), dx(ALPHA))),
         times(exp(ALPHA, BETA), times(ln(ALPHA), dx(BETA))))
  , dx(ln(ALPHA)) -> div(dx(ALPHA), ALPHA) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..