WORST_CASE(?,O(n^2))
* Step 1: LocalSizeboundsProc WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0. evalaxstart(A,B,C)    -> evalaxentryin(A,B,C)   True                       (1,1)
          1. evalaxentryin(A,B,C)  -> evalaxbbin(0,B,C)      True                       (?,1)
          2. evalaxbbin(A,B,C)     -> evalaxbb2in(A,0,C)     True                       (?,1)
          3. evalaxbb2in(A,B,C)    -> evalaxbb1in(A,B,C)     [C >= 2 + B]               (?,1)
          4. evalaxbb2in(A,B,C)    -> evalaxbb3in(A,B,C)     [1 + B >= C]               (?,1)
          5. evalaxbb1in(A,B,C)    -> evalaxbb2in(A,1 + B,C) True                       (?,1)
          6. evalaxbb3in(A,B,C)    -> evalaxbbin(1 + A,B,C)  [1 + B >= C && C >= 3 + A] (?,1)
          7. evalaxbb3in(A,B,C)    -> evalaxreturnin(A,B,C)  [C >= 2 + B]               (?,1)
          8. evalaxbb3in(A,B,C)    -> evalaxreturnin(A,B,C)  [2 + A >= C]               (?,1)
          9. evalaxreturnin(A,B,C) -> evalaxstop(A,B,C)      True                       (?,1)
        Signature:
          {(evalaxbb1in,3)
          ;(evalaxbb2in,3)
          ;(evalaxbb3in,3)
          ;(evalaxbbin,3)
          ;(evalaxentryin,3)
          ;(evalaxreturnin,3)
          ;(evalaxstart,3)
          ;(evalaxstop,3)}
        Flow Graph:
          [0->{1},1->{2},2->{3,4},3->{5},4->{6,7,8},5->{3,4},6->{2},7->{9},8->{9},9->{}]
        
    + Applied Processor:
        LocalSizeboundsProc
    + Details:
        LocalSizebounds generated; rvgraph
          (<0,0,A>,     A, .= 0) (<0,0,B>,     B, .= 0) (<0,0,C>, C, .= 0) 
          (<1,0,A>,     0, .= 0) (<1,0,B>,     B, .= 0) (<1,0,C>, C, .= 0) 
          (<2,0,A>,     A, .= 0) (<2,0,B>,     0, .= 0) (<2,0,C>, C, .= 0) 
          (<3,0,A>,     A, .= 0) (<3,0,B>,     B, .= 0) (<3,0,C>, C, .= 0) 
          (<4,0,A>,     A, .= 0) (<4,0,B>,     B, .= 0) (<4,0,C>, C, .= 0) 
          (<5,0,A>,     A, .= 0) (<5,0,B>, 1 + B, .+ 1) (<5,0,C>, C, .= 0) 
          (<6,0,A>, 1 + A, .+ 1) (<6,0,B>,     B, .= 0) (<6,0,C>, C, .= 0) 
          (<7,0,A>,     A, .= 0) (<7,0,B>,     B, .= 0) (<7,0,C>, C, .= 0) 
          (<8,0,A>,     A, .= 0) (<8,0,B>,     B, .= 0) (<8,0,C>, C, .= 0) 
          (<9,0,A>,     A, .= 0) (<9,0,B>,     B, .= 0) (<9,0,C>, C, .= 0) 
* Step 2: SizeboundsProc WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0. evalaxstart(A,B,C)    -> evalaxentryin(A,B,C)   True                       (1,1)
          1. evalaxentryin(A,B,C)  -> evalaxbbin(0,B,C)      True                       (?,1)
          2. evalaxbbin(A,B,C)     -> evalaxbb2in(A,0,C)     True                       (?,1)
          3. evalaxbb2in(A,B,C)    -> evalaxbb1in(A,B,C)     [C >= 2 + B]               (?,1)
          4. evalaxbb2in(A,B,C)    -> evalaxbb3in(A,B,C)     [1 + B >= C]               (?,1)
          5. evalaxbb1in(A,B,C)    -> evalaxbb2in(A,1 + B,C) True                       (?,1)
          6. evalaxbb3in(A,B,C)    -> evalaxbbin(1 + A,B,C)  [1 + B >= C && C >= 3 + A] (?,1)
          7. evalaxbb3in(A,B,C)    -> evalaxreturnin(A,B,C)  [C >= 2 + B]               (?,1)
          8. evalaxbb3in(A,B,C)    -> evalaxreturnin(A,B,C)  [2 + A >= C]               (?,1)
          9. evalaxreturnin(A,B,C) -> evalaxstop(A,B,C)      True                       (?,1)
        Signature:
          {(evalaxbb1in,3)
          ;(evalaxbb2in,3)
          ;(evalaxbb3in,3)
          ;(evalaxbbin,3)
          ;(evalaxentryin,3)
          ;(evalaxreturnin,3)
          ;(evalaxstart,3)
          ;(evalaxstop,3)}
        Flow Graph:
          [0->{1},1->{2},2->{3,4},3->{5},4->{6,7,8},5->{3,4},6->{2},7->{9},8->{9},9->{}]
        Sizebounds:
          (<0,0,A>, ?) (<0,0,B>, ?) (<0,0,C>, ?) 
          (<1,0,A>, ?) (<1,0,B>, ?) (<1,0,C>, ?) 
          (<2,0,A>, ?) (<2,0,B>, ?) (<2,0,C>, ?) 
          (<3,0,A>, ?) (<3,0,B>, ?) (<3,0,C>, ?) 
          (<4,0,A>, ?) (<4,0,B>, ?) (<4,0,C>, ?) 
          (<5,0,A>, ?) (<5,0,B>, ?) (<5,0,C>, ?) 
          (<6,0,A>, ?) (<6,0,B>, ?) (<6,0,C>, ?) 
          (<7,0,A>, ?) (<7,0,B>, ?) (<7,0,C>, ?) 
          (<8,0,A>, ?) (<8,0,B>, ?) (<8,0,C>, ?) 
          (<9,0,A>, ?) (<9,0,B>, ?) (<9,0,C>, ?) 
    + Applied Processor:
        SizeboundsProc
    + Details:
        Sizebounds computed:
          (<0,0,A>, A) (<0,0,B>, B) (<0,0,C>, C) 
          (<1,0,A>, 0) (<1,0,B>, B) (<1,0,C>, C) 
          (<2,0,A>, C) (<2,0,B>, 0) (<2,0,C>, C) 
          (<3,0,A>, ?) (<3,0,B>, C) (<3,0,C>, C) 
          (<4,0,A>, ?) (<4,0,B>, C) (<4,0,C>, C) 
          (<5,0,A>, ?) (<5,0,B>, C) (<5,0,C>, C) 
          (<6,0,A>, C) (<6,0,B>, C) (<6,0,C>, C) 
          (<7,0,A>, ?) (<7,0,B>, C) (<7,0,C>, C) 
          (<8,0,A>, ?) (<8,0,B>, C) (<8,0,C>, C) 
          (<9,0,A>, ?) (<9,0,B>, C) (<9,0,C>, C) 
* Step 3: UnsatPaths WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0. evalaxstart(A,B,C)    -> evalaxentryin(A,B,C)   True                       (1,1)
          1. evalaxentryin(A,B,C)  -> evalaxbbin(0,B,C)      True                       (?,1)
          2. evalaxbbin(A,B,C)     -> evalaxbb2in(A,0,C)     True                       (?,1)
          3. evalaxbb2in(A,B,C)    -> evalaxbb1in(A,B,C)     [C >= 2 + B]               (?,1)
          4. evalaxbb2in(A,B,C)    -> evalaxbb3in(A,B,C)     [1 + B >= C]               (?,1)
          5. evalaxbb1in(A,B,C)    -> evalaxbb2in(A,1 + B,C) True                       (?,1)
          6. evalaxbb3in(A,B,C)    -> evalaxbbin(1 + A,B,C)  [1 + B >= C && C >= 3 + A] (?,1)
          7. evalaxbb3in(A,B,C)    -> evalaxreturnin(A,B,C)  [C >= 2 + B]               (?,1)
          8. evalaxbb3in(A,B,C)    -> evalaxreturnin(A,B,C)  [2 + A >= C]               (?,1)
          9. evalaxreturnin(A,B,C) -> evalaxstop(A,B,C)      True                       (?,1)
        Signature:
          {(evalaxbb1in,3)
          ;(evalaxbb2in,3)
          ;(evalaxbb3in,3)
          ;(evalaxbbin,3)
          ;(evalaxentryin,3)
          ;(evalaxreturnin,3)
          ;(evalaxstart,3)
          ;(evalaxstop,3)}
        Flow Graph:
          [0->{1},1->{2},2->{3,4},3->{5},4->{6,7,8},5->{3,4},6->{2},7->{9},8->{9},9->{}]
        Sizebounds:
          (<0,0,A>, A) (<0,0,B>, B) (<0,0,C>, C) 
          (<1,0,A>, 0) (<1,0,B>, B) (<1,0,C>, C) 
          (<2,0,A>, C) (<2,0,B>, 0) (<2,0,C>, C) 
          (<3,0,A>, ?) (<3,0,B>, C) (<3,0,C>, C) 
          (<4,0,A>, ?) (<4,0,B>, C) (<4,0,C>, C) 
          (<5,0,A>, ?) (<5,0,B>, C) (<5,0,C>, C) 
          (<6,0,A>, C) (<6,0,B>, C) (<6,0,C>, C) 
          (<7,0,A>, ?) (<7,0,B>, C) (<7,0,C>, C) 
          (<8,0,A>, ?) (<8,0,B>, C) (<8,0,C>, C) 
          (<9,0,A>, ?) (<9,0,B>, C) (<9,0,C>, C) 
    + Applied Processor:
        UnsatPaths
    + Details:
        We remove following edges from the transition graph: [(4,7)]
* Step 4: UnreachableRules WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0. evalaxstart(A,B,C)    -> evalaxentryin(A,B,C)   True                       (1,1)
          1. evalaxentryin(A,B,C)  -> evalaxbbin(0,B,C)      True                       (?,1)
          2. evalaxbbin(A,B,C)     -> evalaxbb2in(A,0,C)     True                       (?,1)
          3. evalaxbb2in(A,B,C)    -> evalaxbb1in(A,B,C)     [C >= 2 + B]               (?,1)
          4. evalaxbb2in(A,B,C)    -> evalaxbb3in(A,B,C)     [1 + B >= C]               (?,1)
          5. evalaxbb1in(A,B,C)    -> evalaxbb2in(A,1 + B,C) True                       (?,1)
          6. evalaxbb3in(A,B,C)    -> evalaxbbin(1 + A,B,C)  [1 + B >= C && C >= 3 + A] (?,1)
          7. evalaxbb3in(A,B,C)    -> evalaxreturnin(A,B,C)  [C >= 2 + B]               (?,1)
          8. evalaxbb3in(A,B,C)    -> evalaxreturnin(A,B,C)  [2 + A >= C]               (?,1)
          9. evalaxreturnin(A,B,C) -> evalaxstop(A,B,C)      True                       (?,1)
        Signature:
          {(evalaxbb1in,3)
          ;(evalaxbb2in,3)
          ;(evalaxbb3in,3)
          ;(evalaxbbin,3)
          ;(evalaxentryin,3)
          ;(evalaxreturnin,3)
          ;(evalaxstart,3)
          ;(evalaxstop,3)}
        Flow Graph:
          [0->{1},1->{2},2->{3,4},3->{5},4->{6,8},5->{3,4},6->{2},7->{9},8->{9},9->{}]
        Sizebounds:
          (<0,0,A>, A) (<0,0,B>, B) (<0,0,C>, C) 
          (<1,0,A>, 0) (<1,0,B>, B) (<1,0,C>, C) 
          (<2,0,A>, C) (<2,0,B>, 0) (<2,0,C>, C) 
          (<3,0,A>, ?) (<3,0,B>, C) (<3,0,C>, C) 
          (<4,0,A>, ?) (<4,0,B>, C) (<4,0,C>, C) 
          (<5,0,A>, ?) (<5,0,B>, C) (<5,0,C>, C) 
          (<6,0,A>, C) (<6,0,B>, C) (<6,0,C>, C) 
          (<7,0,A>, ?) (<7,0,B>, C) (<7,0,C>, C) 
          (<8,0,A>, ?) (<8,0,B>, C) (<8,0,C>, C) 
          (<9,0,A>, ?) (<9,0,B>, C) (<9,0,C>, C) 
    + Applied Processor:
        UnreachableRules
    + Details:
        The following transitions are not reachable from the starting states and are removed: [7]
* Step 5: LeafRules WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0. evalaxstart(A,B,C)    -> evalaxentryin(A,B,C)   True                       (1,1)
          1. evalaxentryin(A,B,C)  -> evalaxbbin(0,B,C)      True                       (?,1)
          2. evalaxbbin(A,B,C)     -> evalaxbb2in(A,0,C)     True                       (?,1)
          3. evalaxbb2in(A,B,C)    -> evalaxbb1in(A,B,C)     [C >= 2 + B]               (?,1)
          4. evalaxbb2in(A,B,C)    -> evalaxbb3in(A,B,C)     [1 + B >= C]               (?,1)
          5. evalaxbb1in(A,B,C)    -> evalaxbb2in(A,1 + B,C) True                       (?,1)
          6. evalaxbb3in(A,B,C)    -> evalaxbbin(1 + A,B,C)  [1 + B >= C && C >= 3 + A] (?,1)
          8. evalaxbb3in(A,B,C)    -> evalaxreturnin(A,B,C)  [2 + A >= C]               (?,1)
          9. evalaxreturnin(A,B,C) -> evalaxstop(A,B,C)      True                       (?,1)
        Signature:
          {(evalaxbb1in,3)
          ;(evalaxbb2in,3)
          ;(evalaxbb3in,3)
          ;(evalaxbbin,3)
          ;(evalaxentryin,3)
          ;(evalaxreturnin,3)
          ;(evalaxstart,3)
          ;(evalaxstop,3)}
        Flow Graph:
          [0->{1},1->{2},2->{3,4},3->{5},4->{6,8},5->{3,4},6->{2},8->{9},9->{}]
        Sizebounds:
          (<0,0,A>, A) (<0,0,B>, B) (<0,0,C>, C) 
          (<1,0,A>, 0) (<1,0,B>, B) (<1,0,C>, C) 
          (<2,0,A>, C) (<2,0,B>, 0) (<2,0,C>, C) 
          (<3,0,A>, ?) (<3,0,B>, C) (<3,0,C>, C) 
          (<4,0,A>, ?) (<4,0,B>, C) (<4,0,C>, C) 
          (<5,0,A>, ?) (<5,0,B>, C) (<5,0,C>, C) 
          (<6,0,A>, C) (<6,0,B>, C) (<6,0,C>, C) 
          (<8,0,A>, ?) (<8,0,B>, C) (<8,0,C>, C) 
          (<9,0,A>, ?) (<9,0,B>, C) (<9,0,C>, C) 
    + Applied Processor:
        LeafRules
    + Details:
        The following transitions are estimated by its predecessors and are removed [8,9]
* Step 6: PolyRank WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0. evalaxstart(A,B,C)   -> evalaxentryin(A,B,C)   True                       (1,1)
          1. evalaxentryin(A,B,C) -> evalaxbbin(0,B,C)      True                       (?,1)
          2. evalaxbbin(A,B,C)    -> evalaxbb2in(A,0,C)     True                       (?,1)
          3. evalaxbb2in(A,B,C)   -> evalaxbb1in(A,B,C)     [C >= 2 + B]               (?,1)
          4. evalaxbb2in(A,B,C)   -> evalaxbb3in(A,B,C)     [1 + B >= C]               (?,1)
          5. evalaxbb1in(A,B,C)   -> evalaxbb2in(A,1 + B,C) True                       (?,1)
          6. evalaxbb3in(A,B,C)   -> evalaxbbin(1 + A,B,C)  [1 + B >= C && C >= 3 + A] (?,1)
        Signature:
          {(evalaxbb1in,3)
          ;(evalaxbb2in,3)
          ;(evalaxbb3in,3)
          ;(evalaxbbin,3)
          ;(evalaxentryin,3)
          ;(evalaxreturnin,3)
          ;(evalaxstart,3)
          ;(evalaxstop,3)}
        Flow Graph:
          [0->{1},1->{2},2->{3,4},3->{5},4->{6},5->{3,4},6->{2}]
        Sizebounds:
          (<0,0,A>, A) (<0,0,B>, B) (<0,0,C>, C) 
          (<1,0,A>, 0) (<1,0,B>, B) (<1,0,C>, C) 
          (<2,0,A>, C) (<2,0,B>, 0) (<2,0,C>, C) 
          (<3,0,A>, ?) (<3,0,B>, C) (<3,0,C>, C) 
          (<4,0,A>, ?) (<4,0,B>, C) (<4,0,C>, C) 
          (<5,0,A>, ?) (<5,0,B>, C) (<5,0,C>, C) 
          (<6,0,A>, C) (<6,0,B>, C) (<6,0,C>, C) 
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
            p(evalaxbb1in) = -2 + -1*x1 + x3
            p(evalaxbb2in) = -2 + -1*x1 + x3
            p(evalaxbb3in) = -2 + -1*x1 + x3
             p(evalaxbbin) = -2 + -1*x1 + x3
          p(evalaxentryin) = 1 + x3         
            p(evalaxstart) = 1 + x3         
        
        The following rules are strictly oriented:
        [1 + B >= C && C >= 3 + A] ==>                      
                evalaxbb3in(A,B,C)   = -2 + -1*A + C        
                                     > -3 + -1*A + C        
                                     = evalaxbbin(1 + A,B,C)
        
        
        The following rules are weakly oriented:
                          True ==>                       
            evalaxstart(A,B,C)   = 1 + C                 
                                >= 1 + C                 
                                 = evalaxentryin(A,B,C)  
        
                          True ==>                       
          evalaxentryin(A,B,C)   = 1 + C                 
                                >= -2 + C                
                                 = evalaxbbin(0,B,C)     
        
                          True ==>                       
             evalaxbbin(A,B,C)   = -2 + -1*A + C         
                                >= -2 + -1*A + C         
                                 = evalaxbb2in(A,0,C)    
        
                  [C >= 2 + B] ==>                       
            evalaxbb2in(A,B,C)   = -2 + -1*A + C         
                                >= -2 + -1*A + C         
                                 = evalaxbb1in(A,B,C)    
        
                  [1 + B >= C] ==>                       
            evalaxbb2in(A,B,C)   = -2 + -1*A + C         
                                >= -2 + -1*A + C         
                                 = evalaxbb3in(A,B,C)    
        
                          True ==>                       
            evalaxbb1in(A,B,C)   = -2 + -1*A + C         
                                >= -2 + -1*A + C         
                                 = evalaxbb2in(A,1 + B,C)
        
        
* Step 7: KnowledgePropagation WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0. evalaxstart(A,B,C)   -> evalaxentryin(A,B,C)   True                       (1,1)    
          1. evalaxentryin(A,B,C) -> evalaxbbin(0,B,C)      True                       (?,1)    
          2. evalaxbbin(A,B,C)    -> evalaxbb2in(A,0,C)     True                       (?,1)    
          3. evalaxbb2in(A,B,C)   -> evalaxbb1in(A,B,C)     [C >= 2 + B]               (?,1)    
          4. evalaxbb2in(A,B,C)   -> evalaxbb3in(A,B,C)     [1 + B >= C]               (?,1)    
          5. evalaxbb1in(A,B,C)   -> evalaxbb2in(A,1 + B,C) True                       (?,1)    
          6. evalaxbb3in(A,B,C)   -> evalaxbbin(1 + A,B,C)  [1 + B >= C && C >= 3 + A] (1 + C,1)
        Signature:
          {(evalaxbb1in,3)
          ;(evalaxbb2in,3)
          ;(evalaxbb3in,3)
          ;(evalaxbbin,3)
          ;(evalaxentryin,3)
          ;(evalaxreturnin,3)
          ;(evalaxstart,3)
          ;(evalaxstop,3)}
        Flow Graph:
          [0->{1},1->{2},2->{3,4},3->{5},4->{6},5->{3,4},6->{2}]
        Sizebounds:
          (<0,0,A>, A) (<0,0,B>, B) (<0,0,C>, C) 
          (<1,0,A>, 0) (<1,0,B>, B) (<1,0,C>, C) 
          (<2,0,A>, C) (<2,0,B>, 0) (<2,0,C>, C) 
          (<3,0,A>, ?) (<3,0,B>, C) (<3,0,C>, C) 
          (<4,0,A>, ?) (<4,0,B>, C) (<4,0,C>, C) 
          (<5,0,A>, ?) (<5,0,B>, C) (<5,0,C>, C) 
          (<6,0,A>, C) (<6,0,B>, C) (<6,0,C>, C) 
    + Applied Processor:
        KnowledgePropagation
    + Details:
        We propagate bounds from predecessors.
* Step 8: PolyRank WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0. evalaxstart(A,B,C)   -> evalaxentryin(A,B,C)   True                       (1,1)    
          1. evalaxentryin(A,B,C) -> evalaxbbin(0,B,C)      True                       (1,1)    
          2. evalaxbbin(A,B,C)    -> evalaxbb2in(A,0,C)     True                       (2 + C,1)
          3. evalaxbb2in(A,B,C)   -> evalaxbb1in(A,B,C)     [C >= 2 + B]               (?,1)    
          4. evalaxbb2in(A,B,C)   -> evalaxbb3in(A,B,C)     [1 + B >= C]               (?,1)    
          5. evalaxbb1in(A,B,C)   -> evalaxbb2in(A,1 + B,C) True                       (?,1)    
          6. evalaxbb3in(A,B,C)   -> evalaxbbin(1 + A,B,C)  [1 + B >= C && C >= 3 + A] (1 + C,1)
        Signature:
          {(evalaxbb1in,3)
          ;(evalaxbb2in,3)
          ;(evalaxbb3in,3)
          ;(evalaxbbin,3)
          ;(evalaxentryin,3)
          ;(evalaxreturnin,3)
          ;(evalaxstart,3)
          ;(evalaxstop,3)}
        Flow Graph:
          [0->{1},1->{2},2->{3,4},3->{5},4->{6},5->{3,4},6->{2}]
        Sizebounds:
          (<0,0,A>, A) (<0,0,B>, B) (<0,0,C>, C) 
          (<1,0,A>, 0) (<1,0,B>, B) (<1,0,C>, C) 
          (<2,0,A>, C) (<2,0,B>, 0) (<2,0,C>, C) 
          (<3,0,A>, ?) (<3,0,B>, C) (<3,0,C>, C) 
          (<4,0,A>, ?) (<4,0,B>, C) (<4,0,C>, C) 
          (<5,0,A>, ?) (<5,0,B>, C) (<5,0,C>, C) 
          (<6,0,A>, C) (<6,0,B>, C) (<6,0,C>, C) 
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [4,5,3], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
          p(evalaxbb1in) = 1
          p(evalaxbb2in) = 1
          p(evalaxbb3in) = 0
        
        The following rules are strictly oriented:
                [1 + B >= C] ==>                   
          evalaxbb2in(A,B,C)   = 1                 
                               > 0                 
                               = evalaxbb3in(A,B,C)
        
        
        The following rules are weakly oriented:
                [C >= 2 + B] ==>                       
          evalaxbb2in(A,B,C)   = 1                     
                              >= 1                     
                               = evalaxbb1in(A,B,C)    
        
                        True ==>                       
          evalaxbb1in(A,B,C)   = 1                     
                              >= 1                     
                               = evalaxbb2in(A,1 + B,C)
        
        We use the following global sizebounds:
        (<0,0,A>, A) (<0,0,B>, B) (<0,0,C>, C) 
        (<1,0,A>, 0) (<1,0,B>, B) (<1,0,C>, C) 
        (<2,0,A>, C) (<2,0,B>, 0) (<2,0,C>, C) 
        (<3,0,A>, ?) (<3,0,B>, C) (<3,0,C>, C) 
        (<4,0,A>, ?) (<4,0,B>, C) (<4,0,C>, C) 
        (<5,0,A>, ?) (<5,0,B>, C) (<5,0,C>, C) 
        (<6,0,A>, C) (<6,0,B>, C) (<6,0,C>, C) 
* Step 9: PolyRank WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0. evalaxstart(A,B,C)   -> evalaxentryin(A,B,C)   True                       (1,1)    
          1. evalaxentryin(A,B,C) -> evalaxbbin(0,B,C)      True                       (1,1)    
          2. evalaxbbin(A,B,C)    -> evalaxbb2in(A,0,C)     True                       (2 + C,1)
          3. evalaxbb2in(A,B,C)   -> evalaxbb1in(A,B,C)     [C >= 2 + B]               (?,1)    
          4. evalaxbb2in(A,B,C)   -> evalaxbb3in(A,B,C)     [1 + B >= C]               (2 + C,1)
          5. evalaxbb1in(A,B,C)   -> evalaxbb2in(A,1 + B,C) True                       (?,1)    
          6. evalaxbb3in(A,B,C)   -> evalaxbbin(1 + A,B,C)  [1 + B >= C && C >= 3 + A] (1 + C,1)
        Signature:
          {(evalaxbb1in,3)
          ;(evalaxbb2in,3)
          ;(evalaxbb3in,3)
          ;(evalaxbbin,3)
          ;(evalaxentryin,3)
          ;(evalaxreturnin,3)
          ;(evalaxstart,3)
          ;(evalaxstop,3)}
        Flow Graph:
          [0->{1},1->{2},2->{3,4},3->{5},4->{6},5->{3,4},6->{2}]
        Sizebounds:
          (<0,0,A>, A) (<0,0,B>, B) (<0,0,C>, C) 
          (<1,0,A>, 0) (<1,0,B>, B) (<1,0,C>, C) 
          (<2,0,A>, C) (<2,0,B>, 0) (<2,0,C>, C) 
          (<3,0,A>, ?) (<3,0,B>, C) (<3,0,C>, C) 
          (<4,0,A>, ?) (<4,0,B>, C) (<4,0,C>, C) 
          (<5,0,A>, ?) (<5,0,B>, C) (<5,0,C>, C) 
          (<6,0,A>, C) (<6,0,B>, C) (<6,0,C>, C) 
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [6,4,5,3], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
          p(evalaxbb1in) = 1 + -1*x2 + x3
          p(evalaxbb2in) = 2 + -1*x2 + x3
          p(evalaxbb3in) = 2 + -1*x2 + x3
           p(evalaxbbin) = 2 + -1*x2 + x3
        
        The following rules are strictly oriented:
                [C >= 2 + B] ==>                   
          evalaxbb2in(A,B,C)   = 2 + -1*B + C      
                               > 1 + -1*B + C      
                               = evalaxbb1in(A,B,C)
        
        
        The following rules are weakly oriented:
                      [1 + B >= C] ==>                       
                evalaxbb2in(A,B,C)   = 2 + -1*B + C          
                                    >= 2 + -1*B + C          
                                     = evalaxbb3in(A,B,C)    
        
                              True ==>                       
                evalaxbb1in(A,B,C)   = 1 + -1*B + C          
                                    >= 1 + -1*B + C          
                                     = evalaxbb2in(A,1 + B,C)
        
        [1 + B >= C && C >= 3 + A] ==>                       
                evalaxbb3in(A,B,C)   = 2 + -1*B + C          
                                    >= 2 + -1*B + C          
                                     = evalaxbbin(1 + A,B,C) 
        
        We use the following global sizebounds:
        (<0,0,A>, A) (<0,0,B>, B) (<0,0,C>, C) 
        (<1,0,A>, 0) (<1,0,B>, B) (<1,0,C>, C) 
        (<2,0,A>, C) (<2,0,B>, 0) (<2,0,C>, C) 
        (<3,0,A>, ?) (<3,0,B>, C) (<3,0,C>, C) 
        (<4,0,A>, ?) (<4,0,B>, C) (<4,0,C>, C) 
        (<5,0,A>, ?) (<5,0,B>, C) (<5,0,C>, C) 
        (<6,0,A>, C) (<6,0,B>, C) (<6,0,C>, C) 
* Step 10: KnowledgePropagation WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0. evalaxstart(A,B,C)   -> evalaxentryin(A,B,C)   True                       (1,1)            
          1. evalaxentryin(A,B,C) -> evalaxbbin(0,B,C)      True                       (1,1)            
          2. evalaxbbin(A,B,C)    -> evalaxbb2in(A,0,C)     True                       (2 + C,1)        
          3. evalaxbb2in(A,B,C)   -> evalaxbb1in(A,B,C)     [C >= 2 + B]               (4 + 4*C + C^2,1)
          4. evalaxbb2in(A,B,C)   -> evalaxbb3in(A,B,C)     [1 + B >= C]               (2 + C,1)        
          5. evalaxbb1in(A,B,C)   -> evalaxbb2in(A,1 + B,C) True                       (?,1)            
          6. evalaxbb3in(A,B,C)   -> evalaxbbin(1 + A,B,C)  [1 + B >= C && C >= 3 + A] (1 + C,1)        
        Signature:
          {(evalaxbb1in,3)
          ;(evalaxbb2in,3)
          ;(evalaxbb3in,3)
          ;(evalaxbbin,3)
          ;(evalaxentryin,3)
          ;(evalaxreturnin,3)
          ;(evalaxstart,3)
          ;(evalaxstop,3)}
        Flow Graph:
          [0->{1},1->{2},2->{3,4},3->{5},4->{6},5->{3,4},6->{2}]
        Sizebounds:
          (<0,0,A>, A) (<0,0,B>, B) (<0,0,C>, C) 
          (<1,0,A>, 0) (<1,0,B>, B) (<1,0,C>, C) 
          (<2,0,A>, C) (<2,0,B>, 0) (<2,0,C>, C) 
          (<3,0,A>, ?) (<3,0,B>, C) (<3,0,C>, C) 
          (<4,0,A>, ?) (<4,0,B>, C) (<4,0,C>, C) 
          (<5,0,A>, ?) (<5,0,B>, C) (<5,0,C>, C) 
          (<6,0,A>, C) (<6,0,B>, C) (<6,0,C>, C) 
    + Applied Processor:
        KnowledgePropagation
    + Details:
        We propagate bounds from predecessors.
* Step 11: LocalSizeboundsProc WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0. evalaxstart(A,B,C)   -> evalaxentryin(A,B,C)   True                       (1,1)            
          1. evalaxentryin(A,B,C) -> evalaxbbin(0,B,C)      True                       (1,1)            
          2. evalaxbbin(A,B,C)    -> evalaxbb2in(A,0,C)     True                       (2 + C,1)        
          3. evalaxbb2in(A,B,C)   -> evalaxbb1in(A,B,C)     [C >= 2 + B]               (4 + 4*C + C^2,1)
          4. evalaxbb2in(A,B,C)   -> evalaxbb3in(A,B,C)     [1 + B >= C]               (2 + C,1)        
          5. evalaxbb1in(A,B,C)   -> evalaxbb2in(A,1 + B,C) True                       (4 + 4*C + C^2,1)
          6. evalaxbb3in(A,B,C)   -> evalaxbbin(1 + A,B,C)  [1 + B >= C && C >= 3 + A] (1 + C,1)        
        Signature:
          {(evalaxbb1in,3)
          ;(evalaxbb2in,3)
          ;(evalaxbb3in,3)
          ;(evalaxbbin,3)
          ;(evalaxentryin,3)
          ;(evalaxreturnin,3)
          ;(evalaxstart,3)
          ;(evalaxstop,3)}
        Flow Graph:
          [0->{1},1->{2},2->{3,4},3->{5},4->{6},5->{3,4},6->{2}]
        Sizebounds:
          (<0,0,A>, A) (<0,0,B>, B) (<0,0,C>, C) 
          (<1,0,A>, 0) (<1,0,B>, B) (<1,0,C>, C) 
          (<2,0,A>, C) (<2,0,B>, 0) (<2,0,C>, C) 
          (<3,0,A>, ?) (<3,0,B>, C) (<3,0,C>, C) 
          (<4,0,A>, ?) (<4,0,B>, C) (<4,0,C>, C) 
          (<5,0,A>, ?) (<5,0,B>, C) (<5,0,C>, C) 
          (<6,0,A>, C) (<6,0,B>, C) (<6,0,C>, C) 
    + Applied Processor:
        LocalSizeboundsProc
    + Details:
        The problem is already solved.

WORST_CASE(?,O(n^2))