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