YES(?,O(n^1))
* Step 1: TrivialSCCs WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          0. evalexministart(A,B,C)    -> evalexminientryin(A,B,C)        True                               (1,1)
          1. evalexminientryin(A,B,C)  -> evalexminibb1in(B,A,C)          True                               (?,1)
          2. evalexminibb1in(A,B,C)    -> evalexminibbin(A,B,C)           [100 >= B && A >= C]               (?,1)
          3. evalexminibb1in(A,B,C)    -> evalexminireturnin(A,B,C)       [B >= 101]                         (?,1)
          4. evalexminibb1in(A,B,C)    -> evalexminireturnin(A,B,C)       [C >= 1 + A]                       (?,1)
          5. evalexminibbin(A,B,C)     -> evalexminibb1in(-1 + A,C,1 + B) [A + -1*C >= 0 && 100 + -1*B >= 0] (?,1)
          6. evalexminireturnin(A,B,C) -> evalexministop(A,B,C)           True                               (?,1)
        Signature:
          {(evalexminibb1in,3)
          ;(evalexminibbin,3)
          ;(evalexminientryin,3)
          ;(evalexminireturnin,3)
          ;(evalexministart,3)
          ;(evalexministop,3)}
        Flow Graph:
          [0->{1},1->{2,3,4},2->{5},3->{6},4->{6},5->{2,3,4},6->{}]
        
    + Applied Processor:
        TrivialSCCs
    + Details:
        All trivial SCCs of the transition graph admit timebound 1.
* Step 2: PolyRank WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          0. evalexministart(A,B,C)    -> evalexminientryin(A,B,C)        True                               (1,1)
          1. evalexminientryin(A,B,C)  -> evalexminibb1in(B,A,C)          True                               (1,1)
          2. evalexminibb1in(A,B,C)    -> evalexminibbin(A,B,C)           [100 >= B && A >= C]               (?,1)
          3. evalexminibb1in(A,B,C)    -> evalexminireturnin(A,B,C)       [B >= 101]                         (1,1)
          4. evalexminibb1in(A,B,C)    -> evalexminireturnin(A,B,C)       [C >= 1 + A]                       (1,1)
          5. evalexminibbin(A,B,C)     -> evalexminibb1in(-1 + A,C,1 + B) [A + -1*C >= 0 && 100 + -1*B >= 0] (?,1)
          6. evalexminireturnin(A,B,C) -> evalexministop(A,B,C)           True                               (1,1)
        Signature:
          {(evalexminibb1in,3)
          ;(evalexminibbin,3)
          ;(evalexminientryin,3)
          ;(evalexminireturnin,3)
          ;(evalexministart,3)
          ;(evalexministop,3)}
        Flow Graph:
          [0->{1},1->{2,3,4},2->{5},3->{6},4->{6},5->{2,3,4},6->{}]
        
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
             p(evalexminibb1in) = 101 + x1 + -1*x2 + -1*x3
              p(evalexminibbin) = 101 + x1 + -1*x2 + -1*x3
           p(evalexminientryin) = 101 + -1*x1 + x2 + -1*x3
          p(evalexminireturnin) = x1 + -1*x2 + -1*x3      
             p(evalexministart) = 101 + -1*x1 + x2 + -1*x3
              p(evalexministop) = x1 + -1*x2 + -1*x3      
        
        Following rules are strictly oriented:
        [A + -1*C >= 0 && 100 + -1*B >= 0] ==>                                
                     evalexminibbin(A,B,C)   = 101 + A + -1*B + -1*C          
                                             > 99 + A + -1*B + -1*C           
                                             = evalexminibb1in(-1 + A,C,1 + B)
        
        
        Following rules are weakly oriented:
                               True ==>                          
             evalexministart(A,B,C)   = 101 + -1*A + B + -1*C    
                                     >= 101 + -1*A + B + -1*C    
                                      = evalexminientryin(A,B,C) 
        
                               True ==>                          
           evalexminientryin(A,B,C)   = 101 + -1*A + B + -1*C    
                                     >= 101 + -1*A + B + -1*C    
                                      = evalexminibb1in(B,A,C)   
        
               [100 >= B && A >= C] ==>                          
             evalexminibb1in(A,B,C)   = 101 + A + -1*B + -1*C    
                                     >= 101 + A + -1*B + -1*C    
                                      = evalexminibbin(A,B,C)    
        
                         [B >= 101] ==>                          
             evalexminibb1in(A,B,C)   = 101 + A + -1*B + -1*C    
                                     >= A + -1*B + -1*C          
                                      = evalexminireturnin(A,B,C)
        
                       [C >= 1 + A] ==>                          
             evalexminibb1in(A,B,C)   = 101 + A + -1*B + -1*C    
                                     >= A + -1*B + -1*C          
                                      = evalexminireturnin(A,B,C)
        
                               True ==>                          
          evalexminireturnin(A,B,C)   = A + -1*B + -1*C          
                                     >= A + -1*B + -1*C          
                                      = evalexministop(A,B,C)    
        
        
* Step 3: KnowledgePropagation WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          0. evalexministart(A,B,C)    -> evalexminientryin(A,B,C)        True                               (1,1)              
          1. evalexminientryin(A,B,C)  -> evalexminibb1in(B,A,C)          True                               (1,1)              
          2. evalexminibb1in(A,B,C)    -> evalexminibbin(A,B,C)           [100 >= B && A >= C]               (?,1)              
          3. evalexminibb1in(A,B,C)    -> evalexminireturnin(A,B,C)       [B >= 101]                         (1,1)              
          4. evalexminibb1in(A,B,C)    -> evalexminireturnin(A,B,C)       [C >= 1 + A]                       (1,1)              
          5. evalexminibbin(A,B,C)     -> evalexminibb1in(-1 + A,C,1 + B) [A + -1*C >= 0 && 100 + -1*B >= 0] (101 + A + B + C,1)
          6. evalexminireturnin(A,B,C) -> evalexministop(A,B,C)           True                               (1,1)              
        Signature:
          {(evalexminibb1in,3)
          ;(evalexminibbin,3)
          ;(evalexminientryin,3)
          ;(evalexminireturnin,3)
          ;(evalexministart,3)
          ;(evalexministop,3)}
        Flow Graph:
          [0->{1},1->{2,3,4},2->{5},3->{6},4->{6},5->{2,3,4},6->{}]
        
    + Applied Processor:
        KnowledgePropagation
    + Details:
        We propagate bounds from predecessors.
* Step 4: PolyRank WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          0. evalexministart(A,B,C)    -> evalexminientryin(A,B,C)        True                               (1,1)              
          1. evalexminientryin(A,B,C)  -> evalexminibb1in(B,A,C)          True                               (1,1)              
          2. evalexminibb1in(A,B,C)    -> evalexminibbin(A,B,C)           [100 >= B && A >= C]               (102 + A + B + C,1)
          3. evalexminibb1in(A,B,C)    -> evalexminireturnin(A,B,C)       [B >= 101]                         (1,1)              
          4. evalexminibb1in(A,B,C)    -> evalexminireturnin(A,B,C)       [C >= 1 + A]                       (1,1)              
          5. evalexminibbin(A,B,C)     -> evalexminibb1in(-1 + A,C,1 + B) [A + -1*C >= 0 && 100 + -1*B >= 0] (101 + A + B + C,1)
          6. evalexminireturnin(A,B,C) -> evalexministop(A,B,C)           True                               (1,1)              
        Signature:
          {(evalexminibb1in,3)
          ;(evalexminibbin,3)
          ;(evalexminientryin,3)
          ;(evalexminireturnin,3)
          ;(evalexministart,3)
          ;(evalexministop,3)}
        Flow Graph:
          [0->{1},1->{2,3,4},2->{5},3->{6},4->{6},5->{2,3,4},6->{}]
        
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
    + Details:
        The problem is already solved.

YES(?,O(n^1))