MAYBE
* Step 1: WeightGap MAYBE
    + Considered Problem:
        - Strict TRS:
            from(X) -> cons(X,from(s(X)))
            length(cons(X,Y)) -> s(length1(Y))
            length(nil()) -> 0()
            length1(X) -> length(X)
        - Signature:
            {from/1,length/1,length1/1} / {0/0,cons/2,nil/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {from,length,length1} and constructors {0,cons,nil,s}
    + 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) = [2]         
               p(cons) = [1] x2 + [1]
               p(from) = [8] x1 + [0]
             p(length) = [8] x1 + [8]
            p(length1) = [8] x1 + [0]
                p(nil) = [2]         
                  p(s) = [1] x1 + [1]
          
          Following rules are strictly oriented:
          length(cons(X,Y)) = [8] Y + [16] 
                            > [8] Y + [1]  
                            = s(length1(Y))
          
              length(nil()) = [24]         
                            > [2]          
                            = 0()          
          
          
          Following rules are (at-least) weakly oriented:
             from(X) =  [8] X + [0]       
                     >= [8] X + [9]       
                     =  cons(X,from(s(X)))
          
          length1(X) =  [8] X + [0]       
                     >= [8] X + [8]       
                     =  length(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:
            from(X) -> cons(X,from(s(X)))
            length1(X) -> length(X)
        - Weak TRS:
            length(cons(X,Y)) -> s(length1(Y))
            length(nil()) -> 0()
        - Signature:
            {from/1,length/1,length1/1} / {0/0,cons/2,nil/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {from,length,length1} and constructors {0,cons,nil,s}
    + 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 + [1]
               p(from) = [0]         
             p(length) = [1] x1 + [0]
            p(length1) = [1] x1 + [1]
                p(nil) = [0]         
                  p(s) = [1] x1 + [0]
          
          Following rules are strictly oriented:
          length1(X) = [1] X + [1]
                     > [1] X + [0]
                     = length(X)  
          
          
          Following rules are (at-least) weakly oriented:
                    from(X) =  [0]               
                            >= [1]               
                            =  cons(X,from(s(X)))
          
          length(cons(X,Y)) =  [1] Y + [1]       
                            >= [1] Y + [1]       
                            =  s(length1(Y))     
          
              length(nil()) =  [0]               
                            >= [0]               
                            =  0()               
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 3: Failure MAYBE
  + Considered Problem:
      - Strict TRS:
          from(X) -> cons(X,from(s(X)))
      - Weak TRS:
          length(cons(X,Y)) -> s(length1(Y))
          length(nil()) -> 0()
          length1(X) -> length(X)
      - Signature:
          {from/1,length/1,length1/1} / {0/0,cons/2,nil/0,s/1}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {from,length,length1} and constructors {0,cons,nil,s}
  + Applied Processor:
      EmptyProcessor
  + Details:
      The problem is still open.
MAYBE