MAYBE
* Step 1: WeightGap MAYBE
    + Considered Problem:
        - Strict TRS:
            add(0(),X) -> X
            add(s(X),Y) -> s(add(X,Y))
            and(false(),Y) -> false()
            and(true(),X) -> X
            first(0(),X) -> nil()
            first(s(X),cons(Y,Z)) -> cons(Y,first(X,Z))
            from(X) -> cons(X,from(s(X)))
            if(false(),X,Y) -> Y
            if(true(),X,Y) -> X
        - Signature:
            {add/2,and/2,first/2,from/1,if/3} / {0/0,cons/2,false/0,nil/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {add,and,first,from,if} 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) = [1]                  
              p(add) = [9] x1 + [2] x2 + [0]
              p(and) = [3] x1 + [2] x2 + [1]
             p(cons) = [1] x2 + [0]         
            p(false) = [1]                  
            p(first) = [8] x1 + [8]         
             p(from) = [1]                  
               p(if) = [2] x2 + [2] x3 + [4]
              p(nil) = [1]                  
                p(s) = [1] x1 + [1]         
             p(true) = [0]                  
          
          Following rules are strictly oriented:
                     add(0(),X) = [2] X + [9]        
                                > [1] X + [0]        
                                = X                  
          
                    add(s(X),Y) = [9] X + [2] Y + [9]
                                > [9] X + [2] Y + [1]
                                = s(add(X,Y))        
          
                 and(false(),Y) = [2] Y + [4]        
                                > [1]                
                                = false()            
          
                  and(true(),X) = [2] X + [1]        
                                > [1] X + [0]        
                                = X                  
          
                   first(0(),X) = [16]               
                                > [1]                
                                = nil()              
          
          first(s(X),cons(Y,Z)) = [8] X + [16]       
                                > [8] X + [8]        
                                = cons(Y,first(X,Z)) 
          
                if(false(),X,Y) = [2] X + [2] Y + [4]
                                > [1] Y + [0]        
                                = Y                  
          
                 if(true(),X,Y) = [2] X + [2] Y + [4]
                                > [1] X + [0]        
                                = X                  
          
          
          Following rules are (at-least) weakly oriented:
          from(X) =  [1]               
                  >= [1]               
                  =  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:
          add(0(),X) -> X
          add(s(X),Y) -> s(add(X,Y))
          and(false(),Y) -> false()
          and(true(),X) -> X
          first(0(),X) -> nil()
          first(s(X),cons(Y,Z)) -> cons(Y,first(X,Z))
          if(false(),X,Y) -> Y
          if(true(),X,Y) -> X
      - Signature:
          {add/2,and/2,first/2,from/1,if/3} / {0/0,cons/2,false/0,nil/0,s/1,true/0}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {add,and,first,from,if} and constructors {0,cons,false,nil
          ,s,true}
  + Applied Processor:
      EmptyProcessor
  + Details:
      The problem is still open.
MAYBE