YES(?,O(n^1))
* Step 1: UnsatPaths WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          0. start(A,B,C) -> eval(A,B,C)      True                       (1,1)
          1. eval(A,B,C)  -> eval(A,B,-1 + C) [C >= 1 + B && B >= A]     (?,1)
          2. eval(A,B,C)  -> eval(-1 + A,B,C) [C >= 1 + B && A >= 1 + B] (?,1)
          3. eval(A,B,C)  -> eval(-1 + A,B,C) [A >= 1 + B]               (?,1)
        Signature:
          {(eval,3);(start,3)}
        Flow Graph:
          [0->{1,2,3},1->{1,2,3},2->{1,2,3},3->{1,2,3}]
        
    + Applied Processor:
        UnsatPaths
    + Details:
        We remove following edges from the transition graph: [(1,2),(1,3)]
* Step 2: PolyRank WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          0. start(A,B,C) -> eval(A,B,C)      True                       (1,1)
          1. eval(A,B,C)  -> eval(A,B,-1 + C) [C >= 1 + B && B >= A]     (?,1)
          2. eval(A,B,C)  -> eval(-1 + A,B,C) [C >= 1 + B && A >= 1 + B] (?,1)
          3. eval(A,B,C)  -> eval(-1 + A,B,C) [A >= 1 + B]               (?,1)
        Signature:
          {(eval,3);(start,3)}
        Flow Graph:
          [0->{1,2,3},1->{1},2->{1,2,3},3->{1,2,3}]
        
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
           p(eval) = x1 + -1*x2
          p(start) = x1 + -1*x2
        
        Following rules are strictly oriented:
         [A >= 1 + B] ==>                 
          eval(A,B,C)   = A + -1*B        
                        > -1 + A + -1*B   
                        = eval(-1 + A,B,C)
        
        
        Following rules are weakly oriented:
                              True ==>                 
                      start(A,B,C)   = A + -1*B        
                                    >= A + -1*B        
                                     = eval(A,B,C)     
        
            [C >= 1 + B && B >= A] ==>                 
                       eval(A,B,C)   = A + -1*B        
                                    >= A + -1*B        
                                     = eval(A,B,-1 + C)
        
        [C >= 1 + B && A >= 1 + B] ==>                 
                       eval(A,B,C)   = A + -1*B        
                                    >= -1 + A + -1*B   
                                     = eval(-1 + A,B,C)
        
        
* Step 3: PolyRank WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          0. start(A,B,C) -> eval(A,B,C)      True                       (1,1)    
          1. eval(A,B,C)  -> eval(A,B,-1 + C) [C >= 1 + B && B >= A]     (?,1)    
          2. eval(A,B,C)  -> eval(-1 + A,B,C) [C >= 1 + B && A >= 1 + B] (?,1)    
          3. eval(A,B,C)  -> eval(-1 + A,B,C) [A >= 1 + B]               (A + B,1)
        Signature:
          {(eval,3);(start,3)}
        Flow Graph:
          [0->{1,2,3},1->{1},2->{1,2,3},3->{1,2,3}]
        
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
           p(eval) = x1 + -1*x2
          p(start) = x1 + -1*x2
        
        Following rules are strictly oriented:
        [C >= 1 + B && A >= 1 + B] ==>                 
                       eval(A,B,C)   = A + -1*B        
                                     > -1 + A + -1*B   
                                     = eval(-1 + A,B,C)
        
                      [A >= 1 + B] ==>                 
                       eval(A,B,C)   = A + -1*B        
                                     > -1 + A + -1*B   
                                     = eval(-1 + A,B,C)
        
        
        Following rules are weakly oriented:
                          True ==>                 
                  start(A,B,C)   = A + -1*B        
                                >= A + -1*B        
                                 = eval(A,B,C)     
        
        [C >= 1 + B && B >= A] ==>                 
                   eval(A,B,C)   = A + -1*B        
                                >= A + -1*B        
                                 = eval(A,B,-1 + C)
        
        
* Step 4: PolyRank WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          0. start(A,B,C) -> eval(A,B,C)      True                       (1,1)    
          1. eval(A,B,C)  -> eval(A,B,-1 + C) [C >= 1 + B && B >= A]     (?,1)    
          2. eval(A,B,C)  -> eval(-1 + A,B,C) [C >= 1 + B && A >= 1 + B] (A + B,1)
          3. eval(A,B,C)  -> eval(-1 + A,B,C) [A >= 1 + B]               (A + B,1)
        Signature:
          {(eval,3);(start,3)}
        Flow Graph:
          [0->{1,2,3},1->{1},2->{1,2,3},3->{1,2,3}]
        
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
           p(eval) = -1*x2 + x3
          p(start) = -1*x2 + x3
        
        Following rules are strictly oriented:
        [C >= 1 + B && B >= A] ==>                 
                   eval(A,B,C)   = -1*B + C        
                                 > -1 + -1*B + C   
                                 = eval(A,B,-1 + C)
        
        
        Following rules are weakly oriented:
                              True ==>                 
                      start(A,B,C)   = -1*B + C        
                                    >= -1*B + C        
                                     = eval(A,B,C)     
        
        [C >= 1 + B && A >= 1 + B] ==>                 
                       eval(A,B,C)   = -1*B + C        
                                    >= -1*B + C        
                                     = eval(-1 + A,B,C)
        
                      [A >= 1 + B] ==>                 
                       eval(A,B,C)   = -1*B + C        
                                    >= -1*B + C        
                                     = eval(-1 + A,B,C)
        
        
* Step 5: KnowledgePropagation WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          0. start(A,B,C) -> eval(A,B,C)      True                       (1,1)    
          1. eval(A,B,C)  -> eval(A,B,-1 + C) [C >= 1 + B && B >= A]     (B + C,1)
          2. eval(A,B,C)  -> eval(-1 + A,B,C) [C >= 1 + B && A >= 1 + B] (A + B,1)
          3. eval(A,B,C)  -> eval(-1 + A,B,C) [A >= 1 + B]               (A + B,1)
        Signature:
          {(eval,3);(start,3)}
        Flow Graph:
          [0->{1,2,3},1->{1},2->{1,2,3},3->{1,2,3}]
        
    + Applied Processor:
        KnowledgePropagation
    + Details:
        The problem is already solved.

YES(?,O(n^1))