MAYBE
* Step 1: WeightGap MAYBE
    + Considered Problem:
        - Strict TRS:
            eq(X,Y) -> false()
            eq(0(),0()) -> true()
            eq(s(X),s(Y)) -> eq(X,Y)
            inf(X) -> cons(X,inf(s(X)))
            length(cons(X,L)) -> s(length(L))
            length(nil()) -> 0()
            take(0(),X) -> nil()
            take(s(X),cons(Y,L)) -> cons(Y,take(X,L))
        - Signature:
            {eq/2,inf/1,length/1,take/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {eq,inf,length,take} and constructors {0,cons,false,nil,s
            ,true}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following nonconstant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(cons) = {2},
            uargs(s) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                 p(0) = [0]         
              p(cons) = [1] x2 + [4]
                p(eq) = [0]         
             p(false) = [0]         
               p(inf) = [0]         
            p(length) = [6] x1 + [0]
               p(nil) = [4]         
                 p(s) = [1] x1 + [7]
              p(take) = [3] x1 + [8]
              p(true) = [0]         
          
          Following rules are strictly oriented:
             length(cons(X,L)) = [6] L + [24]     
                               > [6] L + [7]      
                               = s(length(L))     
          
                 length(nil()) = [24]             
                               > [0]              
                               = 0()              
          
                   take(0(),X) = [8]              
                               > [4]              
                               = nil()            
          
          take(s(X),cons(Y,L)) = [3] X + [29]     
                               > [3] X + [12]     
                               = cons(Y,take(X,L))
          
          
          Following rules are (at-least) weakly oriented:
                eq(X,Y) =  [0]              
                        >= [0]              
                        =  false()          
          
            eq(0(),0()) =  [0]              
                        >= [0]              
                        =  true()           
          
          eq(s(X),s(Y)) =  [0]              
                        >= [0]              
                        =  eq(X,Y)          
          
                 inf(X) =  [0]              
                        >= [4]              
                        =  cons(X,inf(s(X)))
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 2: WeightGap MAYBE
    + Considered Problem:
        - Strict TRS:
            eq(X,Y) -> false()
            eq(0(),0()) -> true()
            eq(s(X),s(Y)) -> eq(X,Y)
            inf(X) -> cons(X,inf(s(X)))
        - Weak TRS:
            length(cons(X,L)) -> s(length(L))
            length(nil()) -> 0()
            take(0(),X) -> nil()
            take(s(X),cons(Y,L)) -> cons(Y,take(X,L))
        - Signature:
            {eq/2,inf/1,length/1,take/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {eq,inf,length,take} and constructors {0,cons,false,nil,s
            ,true}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following nonconstant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(cons) = {2},
            uargs(s) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                 p(0) = [0]          
              p(cons) = [1] x2 + [2] 
                p(eq) = [2] x1 + [9] 
             p(false) = [2]          
               p(inf) = [2] x1 + [8] 
            p(length) = [5] x1 + [15]
               p(nil) = [1]          
                 p(s) = [1] x1 + [8] 
              p(take) = [3] x2 + [2] 
              p(true) = [0]          
          
          Following rules are strictly oriented:
                eq(X,Y) = [2] X + [9] 
                        > [2]         
                        = false()     
          
            eq(0(),0()) = [9]         
                        > [0]         
                        = true()      
          
          eq(s(X),s(Y)) = [2] X + [25]
                        > [2] X + [9] 
                        = eq(X,Y)     
          
          
          Following rules are (at-least) weakly oriented:
                        inf(X) =  [2] X + [8]      
                               >= [2] X + [26]     
                               =  cons(X,inf(s(X)))
          
             length(cons(X,L)) =  [5] L + [25]     
                               >= [5] L + [23]     
                               =  s(length(L))     
          
                 length(nil()) =  [20]             
                               >= [0]              
                               =  0()              
          
                   take(0(),X) =  [3] X + [2]      
                               >= [1]              
                               =  nil()            
          
          take(s(X),cons(Y,L)) =  [3] L + [8]      
                               >= [3] L + [4]      
                               =  cons(Y,take(X,L))
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 3: Failure MAYBE
  + Considered Problem:
      - Strict TRS:
          inf(X) -> cons(X,inf(s(X)))
      - Weak TRS:
          eq(X,Y) -> false()
          eq(0(),0()) -> true()
          eq(s(X),s(Y)) -> eq(X,Y)
          length(cons(X,L)) -> s(length(L))
          length(nil()) -> 0()
          take(0(),X) -> nil()
          take(s(X),cons(Y,L)) -> cons(Y,take(X,L))
      - Signature:
          {eq/2,inf/1,length/1,take/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {eq,inf,length,take} and constructors {0,cons,false,nil,s
          ,true}
  + Applied Processor:
      EmptyProcessor
  + Details:
      The problem is still open.
MAYBE