MAYBE
* Step 1: UnsatPaths MAYBE
    + Considered Problem:
        Rules:
          0. evalcousot9start(A,B,C)    -> evalcousot9entryin(A,B,C)    True                                                                       (1,1)
          1. evalcousot9entryin(A,B,C)  -> evalcousot9bb3in(D,C,C)      True                                                                       (?,1)
          2. evalcousot9bb3in(A,B,C)    -> evalcousot9bbin(A,B,C)       [-1*B + C >= 0 && B >= 1]                                                  (?,1)
          3. evalcousot9bb3in(A,B,C)    -> evalcousot9returnin(A,B,C)   [-1*B + C >= 0 && 0 >= B]                                                  (?,1)
          4. evalcousot9bbin(A,B,C)     -> evalcousot9bb1in(A,B,C)      [-1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + B >= 0 && A >= 1] (?,1)
          5. evalcousot9bbin(A,B,C)     -> evalcousot9bb2in(A,B,C)      [-1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + B >= 0 && 0 >= A] (?,1)
          6. evalcousot9bb1in(A,B,C)    -> evalcousot9bb3in(-1 + A,B,C) [-1 + C >= 0                                                               (?,1)
                                                                         && -2 + B + C >= 0                                                             
                                                                         && -1*B + C >= 0                                                               
                                                                         && -2 + A + C >= 0                                                             
                                                                         && -1 + B >= 0                                                                 
                                                                         && -2 + A + B >= 0                                                             
                                                                         && -1 + A >= 0]                                                                
          7. evalcousot9bb2in(A,B,C)    -> evalcousot9bb3in(C,-1 + B,C) [-1 + C >= 0                                                               (?,1)
                                                                         && -2 + B + C >= 0                                                             
                                                                         && -1*B + C >= 0                                                               
                                                                         && -1 + -1*A + C >= 0                                                          
                                                                         && -1 + B >= 0                                                                 
                                                                         && -1 + -1*A + B >= 0                                                          
                                                                         && -1*A >= 0]                                                                  
          8. evalcousot9returnin(A,B,C) -> evalcousot9stop(A,B,C)       [-1*B + C >= 0 && -1*B >= 0]                                               (?,1)
        Signature:
          {(evalcousot9bb1in,3)
          ;(evalcousot9bb2in,3)
          ;(evalcousot9bb3in,3)
          ;(evalcousot9bbin,3)
          ;(evalcousot9entryin,3)
          ;(evalcousot9returnin,3)
          ;(evalcousot9start,3)
          ;(evalcousot9stop,3)}
        Flow Graph:
          [0->{1},1->{2,3},2->{4,5},3->{8},4->{6},5->{7},6->{2,3},7->{2,3},8->{}]
        
    + Applied Processor:
        UnsatPaths
    + Details:
        We remove following edges from the transition graph: [(6,3)]
* Step 2: TrivialSCCs MAYBE
    + Considered Problem:
        Rules:
          0. evalcousot9start(A,B,C)    -> evalcousot9entryin(A,B,C)    True                                                                       (1,1)
          1. evalcousot9entryin(A,B,C)  -> evalcousot9bb3in(D,C,C)      True                                                                       (?,1)
          2. evalcousot9bb3in(A,B,C)    -> evalcousot9bbin(A,B,C)       [-1*B + C >= 0 && B >= 1]                                                  (?,1)
          3. evalcousot9bb3in(A,B,C)    -> evalcousot9returnin(A,B,C)   [-1*B + C >= 0 && 0 >= B]                                                  (?,1)
          4. evalcousot9bbin(A,B,C)     -> evalcousot9bb1in(A,B,C)      [-1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + B >= 0 && A >= 1] (?,1)
          5. evalcousot9bbin(A,B,C)     -> evalcousot9bb2in(A,B,C)      [-1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + B >= 0 && 0 >= A] (?,1)
          6. evalcousot9bb1in(A,B,C)    -> evalcousot9bb3in(-1 + A,B,C) [-1 + C >= 0                                                               (?,1)
                                                                         && -2 + B + C >= 0                                                             
                                                                         && -1*B + C >= 0                                                               
                                                                         && -2 + A + C >= 0                                                             
                                                                         && -1 + B >= 0                                                                 
                                                                         && -2 + A + B >= 0                                                             
                                                                         && -1 + A >= 0]                                                                
          7. evalcousot9bb2in(A,B,C)    -> evalcousot9bb3in(C,-1 + B,C) [-1 + C >= 0                                                               (?,1)
                                                                         && -2 + B + C >= 0                                                             
                                                                         && -1*B + C >= 0                                                               
                                                                         && -1 + -1*A + C >= 0                                                          
                                                                         && -1 + B >= 0                                                                 
                                                                         && -1 + -1*A + B >= 0                                                          
                                                                         && -1*A >= 0]                                                                  
          8. evalcousot9returnin(A,B,C) -> evalcousot9stop(A,B,C)       [-1*B + C >= 0 && -1*B >= 0]                                               (?,1)
        Signature:
          {(evalcousot9bb1in,3)
          ;(evalcousot9bb2in,3)
          ;(evalcousot9bb3in,3)
          ;(evalcousot9bbin,3)
          ;(evalcousot9entryin,3)
          ;(evalcousot9returnin,3)
          ;(evalcousot9start,3)
          ;(evalcousot9stop,3)}
        Flow Graph:
          [0->{1},1->{2,3},2->{4,5},3->{8},4->{6},5->{7},6->{2},7->{2,3},8->{}]
        
    + Applied Processor:
        TrivialSCCs
    + Details:
        All trivial SCCs of the transition graph admit timebound 1.
* Step 3: PolyRank MAYBE
    + Considered Problem:
        Rules:
          0. evalcousot9start(A,B,C)    -> evalcousot9entryin(A,B,C)    True                                                                       (1,1)
          1. evalcousot9entryin(A,B,C)  -> evalcousot9bb3in(D,C,C)      True                                                                       (1,1)
          2. evalcousot9bb3in(A,B,C)    -> evalcousot9bbin(A,B,C)       [-1*B + C >= 0 && B >= 1]                                                  (?,1)
          3. evalcousot9bb3in(A,B,C)    -> evalcousot9returnin(A,B,C)   [-1*B + C >= 0 && 0 >= B]                                                  (1,1)
          4. evalcousot9bbin(A,B,C)     -> evalcousot9bb1in(A,B,C)      [-1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + B >= 0 && A >= 1] (?,1)
          5. evalcousot9bbin(A,B,C)     -> evalcousot9bb2in(A,B,C)      [-1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + B >= 0 && 0 >= A] (?,1)
          6. evalcousot9bb1in(A,B,C)    -> evalcousot9bb3in(-1 + A,B,C) [-1 + C >= 0                                                               (?,1)
                                                                         && -2 + B + C >= 0                                                             
                                                                         && -1*B + C >= 0                                                               
                                                                         && -2 + A + C >= 0                                                             
                                                                         && -1 + B >= 0                                                                 
                                                                         && -2 + A + B >= 0                                                             
                                                                         && -1 + A >= 0]                                                                
          7. evalcousot9bb2in(A,B,C)    -> evalcousot9bb3in(C,-1 + B,C) [-1 + C >= 0                                                               (?,1)
                                                                         && -2 + B + C >= 0                                                             
                                                                         && -1*B + C >= 0                                                               
                                                                         && -1 + -1*A + C >= 0                                                          
                                                                         && -1 + B >= 0                                                                 
                                                                         && -1 + -1*A + B >= 0                                                          
                                                                         && -1*A >= 0]                                                                  
          8. evalcousot9returnin(A,B,C) -> evalcousot9stop(A,B,C)       [-1*B + C >= 0 && -1*B >= 0]                                               (1,1)
        Signature:
          {(evalcousot9bb1in,3)
          ;(evalcousot9bb2in,3)
          ;(evalcousot9bb3in,3)
          ;(evalcousot9bbin,3)
          ;(evalcousot9entryin,3)
          ;(evalcousot9returnin,3)
          ;(evalcousot9start,3)
          ;(evalcousot9stop,3)}
        Flow Graph:
          [0->{1},1->{2,3},2->{4,5},3->{8},4->{6},5->{7},6->{2},7->{2,3},8->{}]
        
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
             p(evalcousot9bb1in) = x2
             p(evalcousot9bb2in) = x2
             p(evalcousot9bb3in) = x2
              p(evalcousot9bbin) = x2
           p(evalcousot9entryin) = x3
          p(evalcousot9returnin) = x2
             p(evalcousot9start) = x3
              p(evalcousot9stop) = x2
        
        Following rules are strictly oriented:
                     [-1 + C >= 0 ==>                             
               && -2 + B + C >= 0                                 
                 && -1*B + C >= 0                                 
            && -1 + -1*A + C >= 0                                 
                   && -1 + B >= 0                                 
            && -1 + -1*A + B >= 0                                 
                    && -1*A >= 0]                                 
          evalcousot9bb2in(A,B,C)   = B                           
                                    > -1 + B                      
                                    = evalcousot9bb3in(C,-1 + B,C)
        
        
        Following rules are weakly oriented:
                                                                              True ==>                             
                                                           evalcousot9start(A,B,C)   = C                           
                                                                                    >= C                           
                                                                                     = evalcousot9entryin(A,B,C)   
        
                                                                              True ==>                             
                                                         evalcousot9entryin(A,B,C)   = C                           
                                                                                    >= C                           
                                                                                     = evalcousot9bb3in(D,C,C)     
        
                                                         [-1*B + C >= 0 && B >= 1] ==>                             
                                                           evalcousot9bb3in(A,B,C)   = B                           
                                                                                    >= B                           
                                                                                     = evalcousot9bbin(A,B,C)      
        
                                                         [-1*B + C >= 0 && 0 >= B] ==>                             
                                                           evalcousot9bb3in(A,B,C)   = B                           
                                                                                    >= B                           
                                                                                     = evalcousot9returnin(A,B,C)  
        
        [-1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + B >= 0 && A >= 1] ==>                             
                                                            evalcousot9bbin(A,B,C)   = B                           
                                                                                    >= B                           
                                                                                     = evalcousot9bb1in(A,B,C)     
        
        [-1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + B >= 0 && 0 >= A] ==>                             
                                                            evalcousot9bbin(A,B,C)   = B                           
                                                                                    >= B                           
                                                                                     = evalcousot9bb2in(A,B,C)     
        
                                                                      [-1 + C >= 0 ==>                             
                                                                && -2 + B + C >= 0                                 
                                                                  && -1*B + C >= 0                                 
                                                                && -2 + A + C >= 0                                 
                                                                    && -1 + B >= 0                                 
                                                                && -2 + A + B >= 0                                 
                                                                   && -1 + A >= 0]                                 
                                                           evalcousot9bb1in(A,B,C)   = B                           
                                                                                    >= B                           
                                                                                     = evalcousot9bb3in(-1 + A,B,C)
        
                                                      [-1*B + C >= 0 && -1*B >= 0] ==>                             
                                                        evalcousot9returnin(A,B,C)   = B                           
                                                                                    >= B                           
                                                                                     = evalcousot9stop(A,B,C)      
        
        
* Step 4: PolyRank MAYBE
    + Considered Problem:
        Rules:
          0. evalcousot9start(A,B,C)    -> evalcousot9entryin(A,B,C)    True                                                                       (1,1)
          1. evalcousot9entryin(A,B,C)  -> evalcousot9bb3in(D,C,C)      True                                                                       (1,1)
          2. evalcousot9bb3in(A,B,C)    -> evalcousot9bbin(A,B,C)       [-1*B + C >= 0 && B >= 1]                                                  (?,1)
          3. evalcousot9bb3in(A,B,C)    -> evalcousot9returnin(A,B,C)   [-1*B + C >= 0 && 0 >= B]                                                  (1,1)
          4. evalcousot9bbin(A,B,C)     -> evalcousot9bb1in(A,B,C)      [-1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + B >= 0 && A >= 1] (?,1)
          5. evalcousot9bbin(A,B,C)     -> evalcousot9bb2in(A,B,C)      [-1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + B >= 0 && 0 >= A] (?,1)
          6. evalcousot9bb1in(A,B,C)    -> evalcousot9bb3in(-1 + A,B,C) [-1 + C >= 0                                                               (?,1)
                                                                         && -2 + B + C >= 0                                                             
                                                                         && -1*B + C >= 0                                                               
                                                                         && -2 + A + C >= 0                                                             
                                                                         && -1 + B >= 0                                                                 
                                                                         && -2 + A + B >= 0                                                             
                                                                         && -1 + A >= 0]                                                                
          7. evalcousot9bb2in(A,B,C)    -> evalcousot9bb3in(C,-1 + B,C) [-1 + C >= 0                                                               (C,1)
                                                                         && -2 + B + C >= 0                                                             
                                                                         && -1*B + C >= 0                                                               
                                                                         && -1 + -1*A + C >= 0                                                          
                                                                         && -1 + B >= 0                                                                 
                                                                         && -1 + -1*A + B >= 0                                                          
                                                                         && -1*A >= 0]                                                                  
          8. evalcousot9returnin(A,B,C) -> evalcousot9stop(A,B,C)       [-1*B + C >= 0 && -1*B >= 0]                                               (1,1)
        Signature:
          {(evalcousot9bb1in,3)
          ;(evalcousot9bb2in,3)
          ;(evalcousot9bb3in,3)
          ;(evalcousot9bbin,3)
          ;(evalcousot9entryin,3)
          ;(evalcousot9returnin,3)
          ;(evalcousot9start,3)
          ;(evalcousot9stop,3)}
        Flow Graph:
          [0->{1},1->{2,3},2->{4,5},3->{8},4->{6},5->{7},6->{2},7->{2,3},8->{}]
        
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
             p(evalcousot9bb1in) = x2     
             p(evalcousot9bb2in) = -1 + x2
             p(evalcousot9bb3in) = x2     
              p(evalcousot9bbin) = x2     
           p(evalcousot9entryin) = x3     
          p(evalcousot9returnin) = x2     
             p(evalcousot9start) = 1 + x3 
              p(evalcousot9stop) = x2     
        
        Following rules are strictly oriented:
        [-1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + B >= 0 && 0 >= A] ==>                        
                                                            evalcousot9bbin(A,B,C)   = B                      
                                                                                     > -1 + B                 
                                                                                     = evalcousot9bb2in(A,B,C)
        
        
        Following rules are weakly oriented:
                                                                              True ==>                             
                                                           evalcousot9start(A,B,C)   = 1 + C                       
                                                                                    >= C                           
                                                                                     = evalcousot9entryin(A,B,C)   
        
                                                                              True ==>                             
                                                         evalcousot9entryin(A,B,C)   = C                           
                                                                                    >= C                           
                                                                                     = evalcousot9bb3in(D,C,C)     
        
                                                         [-1*B + C >= 0 && B >= 1] ==>                             
                                                           evalcousot9bb3in(A,B,C)   = B                           
                                                                                    >= B                           
                                                                                     = evalcousot9bbin(A,B,C)      
        
                                                         [-1*B + C >= 0 && 0 >= B] ==>                             
                                                           evalcousot9bb3in(A,B,C)   = B                           
                                                                                    >= B                           
                                                                                     = evalcousot9returnin(A,B,C)  
        
        [-1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + B >= 0 && A >= 1] ==>                             
                                                            evalcousot9bbin(A,B,C)   = B                           
                                                                                    >= B                           
                                                                                     = evalcousot9bb1in(A,B,C)     
        
                                                                      [-1 + C >= 0 ==>                             
                                                                && -2 + B + C >= 0                                 
                                                                  && -1*B + C >= 0                                 
                                                                && -2 + A + C >= 0                                 
                                                                    && -1 + B >= 0                                 
                                                                && -2 + A + B >= 0                                 
                                                                   && -1 + A >= 0]                                 
                                                           evalcousot9bb1in(A,B,C)   = B                           
                                                                                    >= B                           
                                                                                     = evalcousot9bb3in(-1 + A,B,C)
        
                                                                      [-1 + C >= 0 ==>                             
                                                                && -2 + B + C >= 0                                 
                                                                  && -1*B + C >= 0                                 
                                                             && -1 + -1*A + C >= 0                                 
                                                                    && -1 + B >= 0                                 
                                                             && -1 + -1*A + B >= 0                                 
                                                                     && -1*A >= 0]                                 
                                                           evalcousot9bb2in(A,B,C)   = -1 + B                      
                                                                                    >= -1 + B                      
                                                                                     = evalcousot9bb3in(C,-1 + B,C)
        
                                                      [-1*B + C >= 0 && -1*B >= 0] ==>                             
                                                        evalcousot9returnin(A,B,C)   = B                           
                                                                                    >= B                           
                                                                                     = evalcousot9stop(A,B,C)      
        
        
* Step 5: Failure MAYBE
  + Considered Problem:
      Rules:
        0. evalcousot9start(A,B,C)    -> evalcousot9entryin(A,B,C)    True                                                                       (1,1)    
        1. evalcousot9entryin(A,B,C)  -> evalcousot9bb3in(D,C,C)      True                                                                       (1,1)    
        2. evalcousot9bb3in(A,B,C)    -> evalcousot9bbin(A,B,C)       [-1*B + C >= 0 && B >= 1]                                                  (?,1)    
        3. evalcousot9bb3in(A,B,C)    -> evalcousot9returnin(A,B,C)   [-1*B + C >= 0 && 0 >= B]                                                  (1,1)    
        4. evalcousot9bbin(A,B,C)     -> evalcousot9bb1in(A,B,C)      [-1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + B >= 0 && A >= 1] (?,1)    
        5. evalcousot9bbin(A,B,C)     -> evalcousot9bb2in(A,B,C)      [-1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + B >= 0 && 0 >= A] (1 + C,1)
        6. evalcousot9bb1in(A,B,C)    -> evalcousot9bb3in(-1 + A,B,C) [-1 + C >= 0                                                               (?,1)    
                                                                       && -2 + B + C >= 0                                                                 
                                                                       && -1*B + C >= 0                                                                   
                                                                       && -2 + A + C >= 0                                                                 
                                                                       && -1 + B >= 0                                                                     
                                                                       && -2 + A + B >= 0                                                                 
                                                                       && -1 + A >= 0]                                                                    
        7. evalcousot9bb2in(A,B,C)    -> evalcousot9bb3in(C,-1 + B,C) [-1 + C >= 0                                                               (C,1)    
                                                                       && -2 + B + C >= 0                                                                 
                                                                       && -1*B + C >= 0                                                                   
                                                                       && -1 + -1*A + C >= 0                                                              
                                                                       && -1 + B >= 0                                                                     
                                                                       && -1 + -1*A + B >= 0                                                              
                                                                       && -1*A >= 0]                                                                      
        8. evalcousot9returnin(A,B,C) -> evalcousot9stop(A,B,C)       [-1*B + C >= 0 && -1*B >= 0]                                               (1,1)    
      Signature:
        {(evalcousot9bb1in,3)
        ;(evalcousot9bb2in,3)
        ;(evalcousot9bb3in,3)
        ;(evalcousot9bbin,3)
        ;(evalcousot9entryin,3)
        ;(evalcousot9returnin,3)
        ;(evalcousot9start,3)
        ;(evalcousot9stop,3)}
      Flow Graph:
        [0->{1},1->{2,3},2->{4,5},3->{8},4->{6},5->{7},6->{2},7->{2,3},8->{}]
      
  + Applied Processor:
      Failing "Open problems left."
  + Details:
      Open problems left.
MAYBE