WORST_CASE(?,O(n^2))
* Step 1: NaturalMI WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            choice(cons(x,xs)) -> x
            choice(cons(x,xs)) -> choice(xs)
            eq(0(x),1(y)) -> false()
            eq(1(x),0(y)) -> false()
            eq(1(x),1(y)) -> eq(x,y)
            eq(O(x),0(y)) -> eq(x,y)
            eq(nil(),nil()) -> true()
            guess(cons(clause,cnf)) -> cons(choice(clause),guess(cnf))
            guess(nil()) -> nil()
            if(false(),t,e) -> e
            if(true(),t,e) -> t
            member(x,cons(y,ys)) -> if(eq(x,y),true(),member(x,ys))
            member(x,nil()) -> false()
            negate(0(x)) -> 1(x)
            negate(1(x)) -> 0(x)
            sat(cnf) -> satck(cnf,guess(cnf))
            satck(cnf,assign) -> if(verify(assign),assign,unsat())
            verify(cons(l,ls)) -> if(member(negate(l),ls),false(),verify(ls))
            verify(nil()) -> true()
        - Signature:
            {choice/1,eq/2,guess/1,if/3,member/2,negate/1,sat/1,satck/2,verify/1} / {0/1,1/1,O/1,cons/2,false/0,nil/0
            ,true/0,unsat/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {choice,eq,guess,if,member,negate,sat,satck
            ,verify} and constructors {0,1,O,cons,false,nil,true,unsat}
    + Applied Processor:
        NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}
    + Details:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(cons) = {1,2},
          uargs(if) = {1,3},
          uargs(member) = {1},
          uargs(satck) = {2}
        
        Following symbols are considered usable:
          {choice,eq,guess,if,member,negate,sat,satck,verify}
        TcT has computed the following interpretation:
               p(0) = [0 0] x1 + [0]                      
                      [0 1]      [4]                      
               p(1) = [0 0] x1 + [0]                      
                      [0 1]      [6]                      
               p(O) = [1 1] x1 + [0]                      
                      [0 1]      [0]                      
          p(choice) = [1 1] x1 + [1]                      
                      [0 2]      [2]                      
            p(cons) = [1 0] x1 + [1 4] x2 + [2]           
                      [0 1]      [0 1]      [3]           
              p(eq) = [0 1] x2 + [0]                      
                      [0 0]      [2]                      
           p(false) = [1]                                 
                      [0]                                 
           p(guess) = [2 1] x1 + [0]                      
                      [0 2]      [0]                      
              p(if) = [1 1] x1 + [1 0] x2 + [1 0] x3 + [0]
                      [0 0]      [0 1]      [0 1]      [0]
          p(member) = [2 0] x1 + [0 1] x2 + [0]           
                      [0 0]      [0 1]      [0]           
          p(negate) = [0 0] x1 + [1]                      
                      [0 2]      [0]                      
             p(nil) = [0]                                 
                      [4]                                 
             p(sat) = [7 5] x1 + [6]                      
                      [2 4]      [3]                      
           p(satck) = [1 0] x1 + [3 1] x2 + [4]           
                      [0 2]      [0 1]      [3]           
            p(true) = [0]                                 
                      [2]                                 
           p(unsat) = [0]                                 
                      [0]                                 
          p(verify) = [2 0] x1 + [2]                      
                      [0 1]      [0]                      
        
        Following rules are strictly oriented:
             choice(cons(x,xs)) = [1 1] x + [1 5] xs + [6]                   
                                  [0 2]     [0 2]      [8]                   
                                > [1 0] x + [0]                              
                                  [0 1]     [0]                              
                                = x                                          
        
             choice(cons(x,xs)) = [1 1] x + [1 5] xs + [6]                   
                                  [0 2]     [0 2]      [8]                   
                                > [1 1] xs + [1]                             
                                  [0 2]      [2]                             
                                = choice(xs)                                 
        
                  eq(0(x),1(y)) = [0 1] y + [6]                              
                                  [0 0]     [2]                              
                                > [1]                                        
                                  [0]                                        
                                = false()                                    
        
                  eq(1(x),0(y)) = [0 1] y + [4]                              
                                  [0 0]     [2]                              
                                > [1]                                        
                                  [0]                                        
                                = false()                                    
        
                  eq(1(x),1(y)) = [0 1] y + [6]                              
                                  [0 0]     [2]                              
                                > [0 1] y + [0]                              
                                  [0 0]     [2]                              
                                = eq(x,y)                                    
        
                  eq(O(x),0(y)) = [0 1] y + [4]                              
                                  [0 0]     [2]                              
                                > [0 1] y + [0]                              
                                  [0 0]     [2]                              
                                = eq(x,y)                                    
        
                eq(nil(),nil()) = [4]                                        
                                  [2]                                        
                                > [0]                                        
                                  [2]                                        
                                = true()                                     
        
        guess(cons(clause,cnf)) = [2 1] clause + [2 9] cnf + [7]             
                                  [0 2]          [0 2]       [6]             
                                > [1 1] clause + [2 9] cnf + [3]             
                                  [0 2]          [0 2]       [5]             
                                = cons(choice(clause),guess(cnf))            
        
                   guess(nil()) = [4]                                        
                                  [8]                                        
                                > [0]                                        
                                  [4]                                        
                                = nil()                                      
        
                if(false(),t,e) = [1 0] e + [1 0] t + [1]                    
                                  [0 1]     [0 1]     [0]                    
                                > [1 0] e + [0]                              
                                  [0 1]     [0]                              
                                = e                                          
        
                 if(true(),t,e) = [1 0] e + [1 0] t + [2]                    
                                  [0 1]     [0 1]     [0]                    
                                > [1 0] t + [0]                              
                                  [0 1]     [0]                              
                                = t                                          
        
           member(x,cons(y,ys)) = [2 0] x + [0 1] y + [0 1] ys + [3]         
                                  [0 0]     [0 1]     [0 1]      [3]         
                                > [2 0] x + [0 1] y + [0 1] ys + [2]         
                                  [0 0]     [0 0]     [0 1]      [2]         
                                = if(eq(x,y),true(),member(x,ys))            
        
                member(x,nil()) = [2 0] x + [4]                              
                                  [0 0]     [4]                              
                                > [1]                                        
                                  [0]                                        
                                = false()                                    
        
                   negate(0(x)) = [0 0] x + [1]                              
                                  [0 2]     [8]                              
                                > [0 0] x + [0]                              
                                  [0 1]     [6]                              
                                = 1(x)                                       
        
                   negate(1(x)) = [0 0] x + [1]                              
                                  [0 2]     [12]                             
                                > [0 0] x + [0]                              
                                  [0 1]     [4]                              
                                = 0(x)                                       
        
                       sat(cnf) = [7 5] cnf + [6]                            
                                  [2 4]       [3]                            
                                > [7 5] cnf + [4]                            
                                  [0 4]       [3]                            
                                = satck(cnf,guess(cnf))                      
        
              satck(cnf,assign) = [3 1] assign + [1 0] cnf + [4]             
                                  [0 1]          [0 2]       [3]             
                                > [3 1] assign + [2]                         
                                  [0 1]          [0]                         
                                = if(verify(assign),assign,unsat())          
        
             verify(cons(l,ls)) = [2 0] l + [2 8] ls + [6]                   
                                  [0 1]     [0 1]      [3]                   
                                > [2 2] ls + [5]                             
                                  [0 1]      [0]                             
                                = if(member(negate(l),ls),false(),verify(ls))
        
                  verify(nil()) = [2]                                        
                                  [4]                                        
                                > [0]                                        
                                  [2]                                        
                                = true()                                     
        
        
        Following rules are (at-least) weakly oriented:
        

WORST_CASE(?,O(n^2))