WORST_CASE(?,O(n^1))
* Step 1: Ara WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            dx(X) -> one()
            dx(a()) -> zero()
            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)
            dx(minus(ALPHA,BETA)) -> minus(dx(ALPHA),dx(BETA))
            dx(neg(ALPHA)) -> neg(dx(ALPHA))
            dx(plus(ALPHA,BETA)) -> plus(dx(ALPHA),dx(BETA))
            dx(times(ALPHA,BETA)) -> plus(times(BETA,dx(ALPHA)),times(ALPHA,dx(BETA)))
        - Signature:
            {dx/1} / {a/0,div/2,exp/2,ln/1,minus/2,neg/1,one/0,plus/2,times/2,two/0,zero/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {dx} and constructors {a,div,exp,ln,minus,neg,one,plus
            ,times,two,zero}
    + Applied Processor:
        Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 3, araTimeout = 60, araFindStrictRules = Nothing, araSmtSolver = MiniSMT}
    + Details:
        Signatures used:
        ----------------
          a :: [] -(0)-> A(4)
          div :: [A(4) x A(4)] -(4)-> A(4)
          div :: [A(0) x A(0)] -(0)-> A(0)
          dx :: [A(4)] -(1)-> A(0)
          exp :: [A(4) x A(4)] -(4)-> A(4)
          exp :: [A(0) x A(0)] -(0)-> A(0)
          ln :: [A(4)] -(4)-> A(4)
          ln :: [A(0)] -(0)-> A(0)
          minus :: [A(4) x A(4)] -(4)-> A(4)
          minus :: [A(0) x A(0)] -(0)-> A(0)
          neg :: [A(4)] -(4)-> A(4)
          neg :: [A(0)] -(0)-> A(0)
          one :: [] -(0)-> A(1)
          plus :: [A(4) x A(4)] -(4)-> A(4)
          plus :: [A(0) x A(0)] -(0)-> A(0)
          times :: [A(4) x A(4)] -(4)-> A(4)
          times :: [A(0) x A(0)] -(0)-> A(0)
          two :: [] -(0)-> A(4)
          zero :: [] -(0)-> A(0)
        
        
        Cost-free Signatures used:
        --------------------------
          a :: [] -(0)-> A_cf(0)
          div :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
          dx :: [A_cf(0)] -(0)-> A_cf(0)
          exp :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
          ln :: [A_cf(0)] -(0)-> A_cf(0)
          minus :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
          neg :: [A_cf(0)] -(0)-> A_cf(0)
          one :: [] -(0)-> A_cf(0)
          plus :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
          times :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
          two :: [] -(0)-> A_cf(0)
          zero :: [] -(0)-> A_cf(0)
        
        
        Base Constructor Signatures used:
        ---------------------------------
          a_A :: [] -(0)-> A(1)
          div_A :: [A(1) x A(1)] -(1)-> A(1)
          exp_A :: [A(1) x A(1)] -(1)-> A(1)
          ln_A :: [A(1)] -(1)-> A(1)
          minus_A :: [A(1) x A(1)] -(1)-> A(1)
          neg_A :: [A(1)] -(1)-> A(1)
          one_A :: [] -(0)-> A(1)
          plus_A :: [A(1) x A(1)] -(1)-> A(1)
          times_A :: [A(1) x A(1)] -(1)-> A(1)
          two_A :: [] -(0)-> A(1)
          zero_A :: [] -(0)-> A(1)
        
* Step 2: Open MAYBE
    - Strict TRS:
        dx(X) -> one()
        dx(a()) -> zero()
        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)
        dx(minus(ALPHA,BETA)) -> minus(dx(ALPHA),dx(BETA))
        dx(neg(ALPHA)) -> neg(dx(ALPHA))
        dx(plus(ALPHA,BETA)) -> plus(dx(ALPHA),dx(BETA))
        dx(times(ALPHA,BETA)) -> plus(times(BETA,dx(ALPHA)),times(ALPHA,dx(BETA)))
    - Signature:
        {dx/1} / {a/0,div/2,exp/2,ln/1,minus/2,neg/1,one/0,plus/2,times/2,two/0,zero/0}
    - Obligation:
        innermost runtime complexity wrt. defined symbols {dx} and constructors {a,div,exp,ln,minus,neg,one,plus
        ,times,two,zero}
Following problems could not be solved:
  - Strict TRS:
      dx(X) -> one()
      dx(a()) -> zero()
      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)
      dx(minus(ALPHA,BETA)) -> minus(dx(ALPHA),dx(BETA))
      dx(neg(ALPHA)) -> neg(dx(ALPHA))
      dx(plus(ALPHA,BETA)) -> plus(dx(ALPHA),dx(BETA))
      dx(times(ALPHA,BETA)) -> plus(times(BETA,dx(ALPHA)),times(ALPHA,dx(BETA)))
  - Signature:
      {dx/1} / {a/0,div/2,exp/2,ln/1,minus/2,neg/1,one/0,plus/2,times/2,two/0,zero/0}
  - Obligation:
      innermost runtime complexity wrt. defined symbols {dx} and constructors {a,div,exp,ln,minus,neg,one,plus
      ,times,two,zero}
WORST_CASE(?,O(n^1))