MAYBE
* Step 1: NaturalPI MAYBE
    + Considered Problem:
        - Strict TRS:
            ack(Cons(x,xs),Nil()) -> ack(xs,Cons(Nil(),Nil()))
            ack(Cons(x',xs'),Cons(x,xs)) -> ack(xs',ack(Cons(x',xs'),xs))
            ack(Nil(),n) -> Cons(Cons(Nil(),Nil()),n)
            goal(m,n) -> ack(m,n)
        - Signature:
            {ack/2,goal/2} / {Cons/2,Nil/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {ack,goal} and constructors {Cons,Nil}
    + 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(ack) = {2}
        
        Following symbols are considered usable:
          {ack,goal}
        TcT has computed the following interpretation:
          p(Cons) = x2      
           p(Nil) = 2       
           p(ack) = x2      
          p(goal) = 1 + 2*x2
        
        Following rules are strictly oriented:
        goal(m,n) = 1 + 2*n 
                  > n       
                  = ack(m,n)
        
        
        Following rules are (at-least) weakly oriented:
               ack(Cons(x,xs),Nil()) =  2                            
                                     >= 2                            
                                     =  ack(xs,Cons(Nil(),Nil()))    
        
        ack(Cons(x',xs'),Cons(x,xs)) =  xs                           
                                     >= xs                           
                                     =  ack(xs',ack(Cons(x',xs'),xs))
        
                        ack(Nil(),n) =  n                            
                                     >= n                            
                                     =  Cons(Cons(Nil(),Nil()),n)    
        
* Step 2: Failure MAYBE
  + Considered Problem:
      - Strict TRS:
          ack(Cons(x,xs),Nil()) -> ack(xs,Cons(Nil(),Nil()))
          ack(Cons(x',xs'),Cons(x,xs)) -> ack(xs',ack(Cons(x',xs'),xs))
          ack(Nil(),n) -> Cons(Cons(Nil(),Nil()),n)
      - Weak TRS:
          goal(m,n) -> ack(m,n)
      - Signature:
          {ack/2,goal/2} / {Cons/2,Nil/0}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {ack,goal} and constructors {Cons,Nil}
  + Applied Processor:
      EmptyProcessor
  + Details:
      The problem is still open.
MAYBE