MAYBE
* Step 1: WeightGap MAYBE
    + Considered Problem:
        - Strict TRS:
            2nd(cons(X,X1)) -> 2nd(cons1(X,X1))
            2nd(cons1(X,cons(Y,Z))) -> Y
            from(X) -> cons(X,from(s(X)))
        - Signature:
            {2nd/1,from/1} / {cons/2,cons1/2,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {2nd,from} and constructors {cons,cons1,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}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
              p(2nd) = [1] x1 + [3]          
             p(cons) = [1] x1 + [1] x2 + [11]
            p(cons1) = [1] x2 + [1]          
             p(from) = [8] x1 + [0]          
                p(s) = [1]                   
          
          Following rules are strictly oriented:
                  2nd(cons(X,X1)) = [1] X + [1] X1 + [14]
                                  > [1] X1 + [4]         
                                  = 2nd(cons1(X,X1))     
          
          2nd(cons1(X,cons(Y,Z))) = [1] Y + [1] Z + [15] 
                                  > [1] Y + [0]          
                                  = Y                    
          
          
          Following rules are (at-least) weakly oriented:
          from(X) =  [8] X + [0]       
                  >= [1] X + [19]      
                  =  cons(X,from(s(X)))
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 2: Failure MAYBE
  + Considered Problem:
      - Strict TRS:
          from(X) -> cons(X,from(s(X)))
      - Weak TRS:
          2nd(cons(X,X1)) -> 2nd(cons1(X,X1))
          2nd(cons1(X,cons(Y,Z))) -> Y
      - Signature:
          {2nd/1,from/1} / {cons/2,cons1/2,s/1}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {2nd,from} and constructors {cons,cons1,s}
  + Applied Processor:
      EmptyProcessor
  + Details:
      The problem is still open.
MAYBE