MAYBE
* Step 1: NaturalPI MAYBE
    + Considered Problem:
        - Strict TRS:
            d(0()) -> 0()
            d(s(x)) -> s(s(d(x)))
            exp(0()) -> s(0())
            exp(s(x)) -> d(exp(x))
        - Signature:
            {d/1,exp/1} / {0/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {d,exp} and constructors {0,s}
    + Applied Processor:
        NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a polynomial interpretation of kind constructor-based(mixed(2)):
        The following argument positions are considered usable:
          uargs(d) = {1},
          uargs(s) = {1}
        
        Following symbols are considered usable:
          {d,exp}
        TcT has computed the following interpretation:
            p(0) = 2                
            p(d) = x1               
          p(exp) = 1 + 2*x1 + 5*x1^2
            p(s) = x1               
        
        Following rules are strictly oriented:
        exp(0()) = 25    
                 > 2     
                 = s(0())
        
        
        Following rules are (at-least) weakly oriented:
           d(0()) =  2              
                  >= 2              
                  =  0()            
        
          d(s(x)) =  x              
                  >= x              
                  =  s(s(d(x)))     
        
        exp(s(x)) =  1 + 2*x + 5*x^2
                  >= 1 + 2*x + 5*x^2
                  =  d(exp(x))      
        
* Step 2: Failure MAYBE
  + Considered Problem:
      - Strict TRS:
          d(0()) -> 0()
          d(s(x)) -> s(s(d(x)))
          exp(s(x)) -> d(exp(x))
      - Weak TRS:
          exp(0()) -> s(0())
      - Signature:
          {d/1,exp/1} / {0/0,s/1}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {d,exp} and constructors {0,s}
  + Applied Processor:
      EmptyProcessor
  + Details:
      The problem is still open.
MAYBE