WORST_CASE(?,O(n^2))
* Step 1: LocalSizeboundsProc WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0. evalfstart(A,B,C,D)    -> evalfentryin(A,B,C,D)   True         (1,1)
          1. evalfentryin(A,B,C,D)  -> evalfbb4in(1,B,C,D)     True         (?,1)
          2. evalfbb4in(A,B,C,D)    -> evalfbb2in(A,B,1,D)     [B >= A]     (?,1)
          3. evalfbb4in(A,B,C,D)    -> evalfreturnin(A,B,C,D)  [A >= 1 + B] (?,1)
          4. evalfbb2in(A,B,C,D)    -> evalfbb1in(A,B,C,D)     [D >= C]     (?,1)
          5. evalfbb2in(A,B,C,D)    -> evalfbb3in(A,B,C,D)     [C >= 1 + D] (?,1)
          6. evalfbb1in(A,B,C,D)    -> evalfbb2in(A,B,1 + C,D) True         (?,1)
          7. evalfbb3in(A,B,C,D)    -> evalfbb4in(1 + A,B,C,D) True         (?,1)
          8. evalfreturnin(A,B,C,D) -> evalfstop(A,B,C,D)      True         (?,1)
        Signature:
          {(evalfbb1in,4)
          ;(evalfbb2in,4)
          ;(evalfbb3in,4)
          ;(evalfbb4in,4)
          ;(evalfentryin,4)
          ;(evalfreturnin,4)
          ;(evalfstart,4)
          ;(evalfstop,4)}
        Flow Graph:
          [0->{1},1->{2,3},2->{4,5},3->{8},4->{6},5->{7},6->{4,5},7->{2,3},8->{}]
        
    + Applied Processor:
        LocalSizeboundsProc
    + Details:
        LocalSizebounds generated; rvgraph
          (<0,0,A>,     A, .= 0) (<0,0,B>, B, .= 0) (<0,0,C>,     C, .= 0) (<0,0,D>, D, .= 0) 
          (<1,0,A>,     1, .= 1) (<1,0,B>, B, .= 0) (<1,0,C>,     C, .= 0) (<1,0,D>, D, .= 0) 
          (<2,0,A>,     A, .= 0) (<2,0,B>, B, .= 0) (<2,0,C>,     1, .= 1) (<2,0,D>, D, .= 0) 
          (<3,0,A>,     A, .= 0) (<3,0,B>, B, .= 0) (<3,0,C>,     C, .= 0) (<3,0,D>, D, .= 0) 
          (<4,0,A>,     A, .= 0) (<4,0,B>, B, .= 0) (<4,0,C>,     C, .= 0) (<4,0,D>, D, .= 0) 
          (<5,0,A>,     A, .= 0) (<5,0,B>, B, .= 0) (<5,0,C>,     C, .= 0) (<5,0,D>, D, .= 0) 
          (<6,0,A>,     A, .= 0) (<6,0,B>, B, .= 0) (<6,0,C>, 1 + C, .+ 1) (<6,0,D>, D, .= 0) 
          (<7,0,A>, 1 + A, .+ 1) (<7,0,B>, B, .= 0) (<7,0,C>,     C, .= 0) (<7,0,D>, D, .= 0) 
          (<8,0,A>,     A, .= 0) (<8,0,B>, B, .= 0) (<8,0,C>,     C, .= 0) (<8,0,D>, D, .= 0) 
* Step 2: SizeboundsProc WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0. evalfstart(A,B,C,D)    -> evalfentryin(A,B,C,D)   True         (1,1)
          1. evalfentryin(A,B,C,D)  -> evalfbb4in(1,B,C,D)     True         (?,1)
          2. evalfbb4in(A,B,C,D)    -> evalfbb2in(A,B,1,D)     [B >= A]     (?,1)
          3. evalfbb4in(A,B,C,D)    -> evalfreturnin(A,B,C,D)  [A >= 1 + B] (?,1)
          4. evalfbb2in(A,B,C,D)    -> evalfbb1in(A,B,C,D)     [D >= C]     (?,1)
          5. evalfbb2in(A,B,C,D)    -> evalfbb3in(A,B,C,D)     [C >= 1 + D] (?,1)
          6. evalfbb1in(A,B,C,D)    -> evalfbb2in(A,B,1 + C,D) True         (?,1)
          7. evalfbb3in(A,B,C,D)    -> evalfbb4in(1 + A,B,C,D) True         (?,1)
          8. evalfreturnin(A,B,C,D) -> evalfstop(A,B,C,D)      True         (?,1)
        Signature:
          {(evalfbb1in,4)
          ;(evalfbb2in,4)
          ;(evalfbb3in,4)
          ;(evalfbb4in,4)
          ;(evalfentryin,4)
          ;(evalfreturnin,4)
          ;(evalfstart,4)
          ;(evalfstop,4)}
        Flow Graph:
          [0->{1},1->{2,3},2->{4,5},3->{8},4->{6},5->{7},6->{4,5},7->{2,3},8->{}]
        Sizebounds:
          (<0,0,A>, ?) (<0,0,B>, ?) (<0,0,C>, ?) (<0,0,D>, ?) 
          (<1,0,A>, ?) (<1,0,B>, ?) (<1,0,C>, ?) (<1,0,D>, ?) 
          (<2,0,A>, ?) (<2,0,B>, ?) (<2,0,C>, ?) (<2,0,D>, ?) 
          (<3,0,A>, ?) (<3,0,B>, ?) (<3,0,C>, ?) (<3,0,D>, ?) 
          (<4,0,A>, ?) (<4,0,B>, ?) (<4,0,C>, ?) (<4,0,D>, ?) 
          (<5,0,A>, ?) (<5,0,B>, ?) (<5,0,C>, ?) (<5,0,D>, ?) 
          (<6,0,A>, ?) (<6,0,B>, ?) (<6,0,C>, ?) (<6,0,D>, ?) 
          (<7,0,A>, ?) (<7,0,B>, ?) (<7,0,C>, ?) (<7,0,D>, ?) 
          (<8,0,A>, ?) (<8,0,B>, ?) (<8,0,C>, ?) (<8,0,D>, ?) 
    + Applied Processor:
        SizeboundsProc
    + Details:
        Sizebounds computed:
          (<0,0,A>, A) (<0,0,B>, B) (<0,0,C>,         C) (<0,0,D>, D) 
          (<1,0,A>, 1) (<1,0,B>, B) (<1,0,C>,         C) (<1,0,D>, D) 
          (<2,0,A>, B) (<2,0,B>, B) (<2,0,C>,         1) (<2,0,D>, D) 
          (<3,0,A>, ?) (<3,0,B>, B) (<3,0,C>, 1 + C + D) (<3,0,D>, D) 
          (<4,0,A>, ?) (<4,0,B>, B) (<4,0,C>,         D) (<4,0,D>, D) 
          (<5,0,A>, ?) (<5,0,B>, B) (<5,0,C>,     1 + D) (<5,0,D>, D) 
          (<6,0,A>, ?) (<6,0,B>, B) (<6,0,C>,         D) (<6,0,D>, D) 
          (<7,0,A>, ?) (<7,0,B>, B) (<7,0,C>,     1 + D) (<7,0,D>, D) 
          (<8,0,A>, ?) (<8,0,B>, B) (<8,0,C>, 1 + C + D) (<8,0,D>, D) 
* Step 3: LeafRules WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0. evalfstart(A,B,C,D)    -> evalfentryin(A,B,C,D)   True         (1,1)
          1. evalfentryin(A,B,C,D)  -> evalfbb4in(1,B,C,D)     True         (?,1)
          2. evalfbb4in(A,B,C,D)    -> evalfbb2in(A,B,1,D)     [B >= A]     (?,1)
          3. evalfbb4in(A,B,C,D)    -> evalfreturnin(A,B,C,D)  [A >= 1 + B] (?,1)
          4. evalfbb2in(A,B,C,D)    -> evalfbb1in(A,B,C,D)     [D >= C]     (?,1)
          5. evalfbb2in(A,B,C,D)    -> evalfbb3in(A,B,C,D)     [C >= 1 + D] (?,1)
          6. evalfbb1in(A,B,C,D)    -> evalfbb2in(A,B,1 + C,D) True         (?,1)
          7. evalfbb3in(A,B,C,D)    -> evalfbb4in(1 + A,B,C,D) True         (?,1)
          8. evalfreturnin(A,B,C,D) -> evalfstop(A,B,C,D)      True         (?,1)
        Signature:
          {(evalfbb1in,4)
          ;(evalfbb2in,4)
          ;(evalfbb3in,4)
          ;(evalfbb4in,4)
          ;(evalfentryin,4)
          ;(evalfreturnin,4)
          ;(evalfstart,4)
          ;(evalfstop,4)}
        Flow Graph:
          [0->{1},1->{2,3},2->{4,5},3->{8},4->{6},5->{7},6->{4,5},7->{2,3},8->{}]
        Sizebounds:
          (<0,0,A>, A) (<0,0,B>, B) (<0,0,C>,         C) (<0,0,D>, D) 
          (<1,0,A>, 1) (<1,0,B>, B) (<1,0,C>,         C) (<1,0,D>, D) 
          (<2,0,A>, B) (<2,0,B>, B) (<2,0,C>,         1) (<2,0,D>, D) 
          (<3,0,A>, ?) (<3,0,B>, B) (<3,0,C>, 1 + C + D) (<3,0,D>, D) 
          (<4,0,A>, ?) (<4,0,B>, B) (<4,0,C>,         D) (<4,0,D>, D) 
          (<5,0,A>, ?) (<5,0,B>, B) (<5,0,C>,     1 + D) (<5,0,D>, D) 
          (<6,0,A>, ?) (<6,0,B>, B) (<6,0,C>,         D) (<6,0,D>, D) 
          (<7,0,A>, ?) (<7,0,B>, B) (<7,0,C>,     1 + D) (<7,0,D>, D) 
          (<8,0,A>, ?) (<8,0,B>, B) (<8,0,C>, 1 + C + D) (<8,0,D>, D) 
    + Applied Processor:
        LeafRules
    + Details:
        The following transitions are estimated by its predecessors and are removed [3,8]
* Step 4: PolyRank WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0. evalfstart(A,B,C,D)   -> evalfentryin(A,B,C,D)   True         (1,1)
          1. evalfentryin(A,B,C,D) -> evalfbb4in(1,B,C,D)     True         (?,1)
          2. evalfbb4in(A,B,C,D)   -> evalfbb2in(A,B,1,D)     [B >= A]     (?,1)
          4. evalfbb2in(A,B,C,D)   -> evalfbb1in(A,B,C,D)     [D >= C]     (?,1)
          5. evalfbb2in(A,B,C,D)   -> evalfbb3in(A,B,C,D)     [C >= 1 + D] (?,1)
          6. evalfbb1in(A,B,C,D)   -> evalfbb2in(A,B,1 + C,D) True         (?,1)
          7. evalfbb3in(A,B,C,D)   -> evalfbb4in(1 + A,B,C,D) True         (?,1)
        Signature:
          {(evalfbb1in,4)
          ;(evalfbb2in,4)
          ;(evalfbb3in,4)
          ;(evalfbb4in,4)
          ;(evalfentryin,4)
          ;(evalfreturnin,4)
          ;(evalfstart,4)
          ;(evalfstop,4)}
        Flow Graph:
          [0->{1},1->{2},2->{4,5},4->{6},5->{7},6->{4,5},7->{2}]
        Sizebounds:
          (<0,0,A>, A) (<0,0,B>, B) (<0,0,C>,     C) (<0,0,D>, D) 
          (<1,0,A>, 1) (<1,0,B>, B) (<1,0,C>,     C) (<1,0,D>, D) 
          (<2,0,A>, B) (<2,0,B>, B) (<2,0,C>,     1) (<2,0,D>, D) 
          (<4,0,A>, ?) (<4,0,B>, B) (<4,0,C>,     D) (<4,0,D>, D) 
          (<5,0,A>, ?) (<5,0,B>, B) (<5,0,C>, 1 + D) (<5,0,D>, D) 
          (<6,0,A>, ?) (<6,0,B>, B) (<6,0,C>,     D) (<6,0,D>, D) 
          (<7,0,A>, ?) (<7,0,B>, B) (<7,0,C>, 1 + D) (<7,0,D>, D) 
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
            p(evalfbb1in) = 1
            p(evalfbb2in) = 1
            p(evalfbb3in) = 1
            p(evalfbb4in) = 1
          p(evalfentryin) = 2
            p(evalfstart) = 2
        
        The following rules are strictly oriented:
                           True ==>                    
          evalfentryin(A,B,C,D)   = 2                  
                                  > 1                  
                                  = evalfbb4in(1,B,C,D)
        
        
        The following rules are weakly oriented:
                         True ==>                        
          evalfstart(A,B,C,D)   = 2                      
                               >= 2                      
                                = evalfentryin(A,B,C,D)  
        
                     [B >= A] ==>                        
          evalfbb4in(A,B,C,D)   = 1                      
                               >= 1                      
                                = evalfbb2in(A,B,1,D)    
        
                     [D >= C] ==>                        
          evalfbb2in(A,B,C,D)   = 1                      
                               >= 1                      
                                = evalfbb1in(A,B,C,D)    
        
                 [C >= 1 + D] ==>                        
          evalfbb2in(A,B,C,D)   = 1                      
                               >= 1                      
                                = evalfbb3in(A,B,C,D)    
        
                         True ==>                        
          evalfbb1in(A,B,C,D)   = 1                      
                               >= 1                      
                                = evalfbb2in(A,B,1 + C,D)
        
                         True ==>                        
          evalfbb3in(A,B,C,D)   = 1                      
                               >= 1                      
                                = evalfbb4in(1 + A,B,C,D)
        
        
* Step 5: PolyRank WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0. evalfstart(A,B,C,D)   -> evalfentryin(A,B,C,D)   True         (1,1)
          1. evalfentryin(A,B,C,D) -> evalfbb4in(1,B,C,D)     True         (2,1)
          2. evalfbb4in(A,B,C,D)   -> evalfbb2in(A,B,1,D)     [B >= A]     (?,1)
          4. evalfbb2in(A,B,C,D)   -> evalfbb1in(A,B,C,D)     [D >= C]     (?,1)
          5. evalfbb2in(A,B,C,D)   -> evalfbb3in(A,B,C,D)     [C >= 1 + D] (?,1)
          6. evalfbb1in(A,B,C,D)   -> evalfbb2in(A,B,1 + C,D) True         (?,1)
          7. evalfbb3in(A,B,C,D)   -> evalfbb4in(1 + A,B,C,D) True         (?,1)
        Signature:
          {(evalfbb1in,4)
          ;(evalfbb2in,4)
          ;(evalfbb3in,4)
          ;(evalfbb4in,4)
          ;(evalfentryin,4)
          ;(evalfreturnin,4)
          ;(evalfstart,4)
          ;(evalfstop,4)}
        Flow Graph:
          [0->{1},1->{2},2->{4,5},4->{6},5->{7},6->{4,5},7->{2}]
        Sizebounds:
          (<0,0,A>, A) (<0,0,B>, B) (<0,0,C>,     C) (<0,0,D>, D) 
          (<1,0,A>, 1) (<1,0,B>, B) (<1,0,C>,     C) (<1,0,D>, D) 
          (<2,0,A>, B) (<2,0,B>, B) (<2,0,C>,     1) (<2,0,D>, D) 
          (<4,0,A>, ?) (<4,0,B>, B) (<4,0,C>,     D) (<4,0,D>, D) 
          (<5,0,A>, ?) (<5,0,B>, B) (<5,0,C>, 1 + D) (<5,0,D>, D) 
          (<6,0,A>, ?) (<6,0,B>, B) (<6,0,C>,     D) (<6,0,D>, D) 
          (<7,0,A>, ?) (<7,0,B>, B) (<7,0,C>, 1 + D) (<7,0,D>, D) 
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
            p(evalfbb1in) = -1*x1 + x2    
            p(evalfbb2in) = -1*x1 + x2    
            p(evalfbb3in) = -1*x1 + x2    
            p(evalfbb4in) = 1 + -1*x1 + x2
          p(evalfentryin) = x2            
            p(evalfstart) = x2            
        
        The following rules are strictly oriented:
                     [B >= A] ==>                    
          evalfbb4in(A,B,C,D)   = 1 + -1*A + B       
                                > -1*A + B           
                                = evalfbb2in(A,B,1,D)
        
        
        The following rules are weakly oriented:
                           True ==>                        
            evalfstart(A,B,C,D)   = B                      
                                 >= B                      
                                  = evalfentryin(A,B,C,D)  
        
                           True ==>                        
          evalfentryin(A,B,C,D)   = B                      
                                 >= B                      
                                  = evalfbb4in(1,B,C,D)    
        
                       [D >= C] ==>                        
            evalfbb2in(A,B,C,D)   = -1*A + B               
                                 >= -1*A + B               
                                  = evalfbb1in(A,B,C,D)    
        
                   [C >= 1 + D] ==>                        
            evalfbb2in(A,B,C,D)   = -1*A + B               
                                 >= -1*A + B               
                                  = evalfbb3in(A,B,C,D)    
        
                           True ==>                        
            evalfbb1in(A,B,C,D)   = -1*A + B               
                                 >= -1*A + B               
                                  = evalfbb2in(A,B,1 + C,D)
        
                           True ==>                        
            evalfbb3in(A,B,C,D)   = -1*A + B               
                                 >= -1*A + B               
                                  = evalfbb4in(1 + A,B,C,D)
        
        
* Step 6: PolyRank WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0. evalfstart(A,B,C,D)   -> evalfentryin(A,B,C,D)   True         (1,1)
          1. evalfentryin(A,B,C,D) -> evalfbb4in(1,B,C,D)     True         (2,1)
          2. evalfbb4in(A,B,C,D)   -> evalfbb2in(A,B,1,D)     [B >= A]     (B,1)
          4. evalfbb2in(A,B,C,D)   -> evalfbb1in(A,B,C,D)     [D >= C]     (?,1)
          5. evalfbb2in(A,B,C,D)   -> evalfbb3in(A,B,C,D)     [C >= 1 + D] (?,1)
          6. evalfbb1in(A,B,C,D)   -> evalfbb2in(A,B,1 + C,D) True         (?,1)
          7. evalfbb3in(A,B,C,D)   -> evalfbb4in(1 + A,B,C,D) True         (?,1)
        Signature:
          {(evalfbb1in,4)
          ;(evalfbb2in,4)
          ;(evalfbb3in,4)
          ;(evalfbb4in,4)
          ;(evalfentryin,4)
          ;(evalfreturnin,4)
          ;(evalfstart,4)
          ;(evalfstop,4)}
        Flow Graph:
          [0->{1},1->{2},2->{4,5},4->{6},5->{7},6->{4,5},7->{2}]
        Sizebounds:
          (<0,0,A>, A) (<0,0,B>, B) (<0,0,C>,     C) (<0,0,D>, D) 
          (<1,0,A>, 1) (<1,0,B>, B) (<1,0,C>,     C) (<1,0,D>, D) 
          (<2,0,A>, B) (<2,0,B>, B) (<2,0,C>,     1) (<2,0,D>, D) 
          (<4,0,A>, ?) (<4,0,B>, B) (<4,0,C>,     D) (<4,0,D>, D) 
          (<5,0,A>, ?) (<5,0,B>, B) (<5,0,C>, 1 + D) (<5,0,D>, D) 
          (<6,0,A>, ?) (<6,0,B>, B) (<6,0,C>,     D) (<6,0,D>, D) 
          (<7,0,A>, ?) (<7,0,B>, B) (<7,0,C>, 1 + D) (<7,0,D>, D) 
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [7,5,6,4], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
          p(evalfbb1in) = 1
          p(evalfbb2in) = 1
          p(evalfbb3in) = 1
          p(evalfbb4in) = 0
        
        The following rules are strictly oriented:
                         True ==>                        
          evalfbb3in(A,B,C,D)   = 1                      
                                > 0                      
                                = evalfbb4in(1 + A,B,C,D)
        
        
        The following rules are weakly oriented:
                     [D >= C] ==>                        
          evalfbb2in(A,B,C,D)   = 1                      
                               >= 1                      
                                = evalfbb1in(A,B,C,D)    
        
                 [C >= 1 + D] ==>                        
          evalfbb2in(A,B,C,D)   = 1                      
                               >= 1                      
                                = evalfbb3in(A,B,C,D)    
        
                         True ==>                        
          evalfbb1in(A,B,C,D)   = 1                      
                               >= 1                      
                                = evalfbb2in(A,B,1 + C,D)
        
        We use the following global sizebounds:
        (<0,0,A>, A) (<0,0,B>, B) (<0,0,C>,     C) (<0,0,D>, D) 
        (<1,0,A>, 1) (<1,0,B>, B) (<1,0,C>,     C) (<1,0,D>, D) 
        (<2,0,A>, B) (<2,0,B>, B) (<2,0,C>,     1) (<2,0,D>, D) 
        (<4,0,A>, ?) (<4,0,B>, B) (<4,0,C>,     D) (<4,0,D>, D) 
        (<5,0,A>, ?) (<5,0,B>, B) (<5,0,C>, 1 + D) (<5,0,D>, D) 
        (<6,0,A>, ?) (<6,0,B>, B) (<6,0,C>,     D) (<6,0,D>, D) 
        (<7,0,A>, ?) (<7,0,B>, B) (<7,0,C>, 1 + D) (<7,0,D>, D) 
* Step 7: PolyRank WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0. evalfstart(A,B,C,D)   -> evalfentryin(A,B,C,D)   True         (1,1)
          1. evalfentryin(A,B,C,D) -> evalfbb4in(1,B,C,D)     True         (2,1)
          2. evalfbb4in(A,B,C,D)   -> evalfbb2in(A,B,1,D)     [B >= A]     (B,1)
          4. evalfbb2in(A,B,C,D)   -> evalfbb1in(A,B,C,D)     [D >= C]     (?,1)
          5. evalfbb2in(A,B,C,D)   -> evalfbb3in(A,B,C,D)     [C >= 1 + D] (?,1)
          6. evalfbb1in(A,B,C,D)   -> evalfbb2in(A,B,1 + C,D) True         (?,1)
          7. evalfbb3in(A,B,C,D)   -> evalfbb4in(1 + A,B,C,D) True         (B,1)
        Signature:
          {(evalfbb1in,4)
          ;(evalfbb2in,4)
          ;(evalfbb3in,4)
          ;(evalfbb4in,4)
          ;(evalfentryin,4)
          ;(evalfreturnin,4)
          ;(evalfstart,4)
          ;(evalfstop,4)}
        Flow Graph:
          [0->{1},1->{2},2->{4,5},4->{6},5->{7},6->{4,5},7->{2}]
        Sizebounds:
          (<0,0,A>, A) (<0,0,B>, B) (<0,0,C>,     C) (<0,0,D>, D) 
          (<1,0,A>, 1) (<1,0,B>, B) (<1,0,C>,     C) (<1,0,D>, D) 
          (<2,0,A>, B) (<2,0,B>, B) (<2,0,C>,     1) (<2,0,D>, D) 
          (<4,0,A>, ?) (<4,0,B>, B) (<4,0,C>,     D) (<4,0,D>, D) 
          (<5,0,A>, ?) (<5,0,B>, B) (<5,0,C>, 1 + D) (<5,0,D>, D) 
          (<6,0,A>, ?) (<6,0,B>, B) (<6,0,C>,     D) (<6,0,D>, D) 
          (<7,0,A>, ?) (<7,0,B>, B) (<7,0,C>, 1 + D) (<7,0,D>, D) 
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [7,5,6,4], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
          p(evalfbb1in) = 1
          p(evalfbb2in) = 1
          p(evalfbb3in) = 0
          p(evalfbb4in) = 0
        
        The following rules are strictly oriented:
                 [C >= 1 + D] ==>                    
          evalfbb2in(A,B,C,D)   = 1                  
                                > 0                  
                                = evalfbb3in(A,B,C,D)
        
        
        The following rules are weakly oriented:
                     [D >= C] ==>                        
          evalfbb2in(A,B,C,D)   = 1                      
                               >= 1                      
                                = evalfbb1in(A,B,C,D)    
        
                         True ==>                        
          evalfbb1in(A,B,C,D)   = 1                      
                               >= 1                      
                                = evalfbb2in(A,B,1 + C,D)
        
                         True ==>                        
          evalfbb3in(A,B,C,D)   = 0                      
                               >= 0                      
                                = evalfbb4in(1 + A,B,C,D)
        
        We use the following global sizebounds:
        (<0,0,A>, A) (<0,0,B>, B) (<0,0,C>,     C) (<0,0,D>, D) 
        (<1,0,A>, 1) (<1,0,B>, B) (<1,0,C>,     C) (<1,0,D>, D) 
        (<2,0,A>, B) (<2,0,B>, B) (<2,0,C>,     1) (<2,0,D>, D) 
        (<4,0,A>, ?) (<4,0,B>, B) (<4,0,C>,     D) (<4,0,D>, D) 
        (<5,0,A>, ?) (<5,0,B>, B) (<5,0,C>, 1 + D) (<5,0,D>, D) 
        (<6,0,A>, ?) (<6,0,B>, B) (<6,0,C>,     D) (<6,0,D>, D) 
        (<7,0,A>, ?) (<7,0,B>, B) (<7,0,C>, 1 + D) (<7,0,D>, D) 
* Step 8: PolyRank WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0. evalfstart(A,B,C,D)   -> evalfentryin(A,B,C,D)   True         (1,1)
          1. evalfentryin(A,B,C,D) -> evalfbb4in(1,B,C,D)     True         (2,1)
          2. evalfbb4in(A,B,C,D)   -> evalfbb2in(A,B,1,D)     [B >= A]     (B,1)
          4. evalfbb2in(A,B,C,D)   -> evalfbb1in(A,B,C,D)     [D >= C]     (?,1)
          5. evalfbb2in(A,B,C,D)   -> evalfbb3in(A,B,C,D)     [C >= 1 + D] (B,1)
          6. evalfbb1in(A,B,C,D)   -> evalfbb2in(A,B,1 + C,D) True         (?,1)
          7. evalfbb3in(A,B,C,D)   -> evalfbb4in(1 + A,B,C,D) True         (B,1)
        Signature:
          {(evalfbb1in,4)
          ;(evalfbb2in,4)
          ;(evalfbb3in,4)
          ;(evalfbb4in,4)
          ;(evalfentryin,4)
          ;(evalfreturnin,4)
          ;(evalfstart,4)
          ;(evalfstop,4)}
        Flow Graph:
          [0->{1},1->{2},2->{4,5},4->{6},5->{7},6->{4,5},7->{2}]
        Sizebounds:
          (<0,0,A>, A) (<0,0,B>, B) (<0,0,C>,     C) (<0,0,D>, D) 
          (<1,0,A>, 1) (<1,0,B>, B) (<1,0,C>,     C) (<1,0,D>, D) 
          (<2,0,A>, B) (<2,0,B>, B) (<2,0,C>,     1) (<2,0,D>, D) 
          (<4,0,A>, ?) (<4,0,B>, B) (<4,0,C>,     D) (<4,0,D>, D) 
          (<5,0,A>, ?) (<5,0,B>, B) (<5,0,C>, 1 + D) (<5,0,D>, D) 
          (<6,0,A>, ?) (<6,0,B>, B) (<6,0,C>,     D) (<6,0,D>, D) 
          (<7,0,A>, ?) (<7,0,B>, B) (<7,0,C>, 1 + D) (<7,0,D>, D) 
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [7,5,6,4], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
          p(evalfbb1in) = 1 + -1*x3 + x4
          p(evalfbb2in) = 2 + -1*x3 + x4
          p(evalfbb3in) = 2 + -1*x3 + x4
          p(evalfbb4in) = 2 + -1*x3 + x4
        
        The following rules are strictly oriented:
                     [D >= C] ==>                    
          evalfbb2in(A,B,C,D)   = 2 + -1*C + D       
                                > 1 + -1*C + D       
                                = evalfbb1in(A,B,C,D)
        
        
        The following rules are weakly oriented:
                 [C >= 1 + D] ==>                        
          evalfbb2in(A,B,C,D)   = 2 + -1*C + D           
                               >= 2 + -1*C + D           
                                = evalfbb3in(A,B,C,D)    
        
                         True ==>                        
          evalfbb1in(A,B,C,D)   = 1 + -1*C + D           
                               >= 1 + -1*C + D           
                                = evalfbb2in(A,B,1 + C,D)
        
                         True ==>                        
          evalfbb3in(A,B,C,D)   = 2 + -1*C + D           
                               >= 2 + -1*C + D           
                                = evalfbb4in(1 + A,B,C,D)
        
        We use the following global sizebounds:
        (<0,0,A>, A) (<0,0,B>, B) (<0,0,C>,     C) (<0,0,D>, D) 
        (<1,0,A>, 1) (<1,0,B>, B) (<1,0,C>,     C) (<1,0,D>, D) 
        (<2,0,A>, B) (<2,0,B>, B) (<2,0,C>,     1) (<2,0,D>, D) 
        (<4,0,A>, ?) (<4,0,B>, B) (<4,0,C>,     D) (<4,0,D>, D) 
        (<5,0,A>, ?) (<5,0,B>, B) (<5,0,C>, 1 + D) (<5,0,D>, D) 
        (<6,0,A>, ?) (<6,0,B>, B) (<6,0,C>,     D) (<6,0,D>, D) 
        (<7,0,A>, ?) (<7,0,B>, B) (<7,0,C>, 1 + D) (<7,0,D>, D) 
* Step 9: KnowledgePropagation WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0. evalfstart(A,B,C,D)   -> evalfentryin(A,B,C,D)   True         (1,1)        
          1. evalfentryin(A,B,C,D) -> evalfbb4in(1,B,C,D)     True         (2,1)        
          2. evalfbb4in(A,B,C,D)   -> evalfbb2in(A,B,1,D)     [B >= A]     (B,1)        
          4. evalfbb2in(A,B,C,D)   -> evalfbb1in(A,B,C,D)     [D >= C]     (3*B + B*D,1)
          5. evalfbb2in(A,B,C,D)   -> evalfbb3in(A,B,C,D)     [C >= 1 + D] (B,1)        
          6. evalfbb1in(A,B,C,D)   -> evalfbb2in(A,B,1 + C,D) True         (?,1)        
          7. evalfbb3in(A,B,C,D)   -> evalfbb4in(1 + A,B,C,D) True         (B,1)        
        Signature:
          {(evalfbb1in,4)
          ;(evalfbb2in,4)
          ;(evalfbb3in,4)
          ;(evalfbb4in,4)
          ;(evalfentryin,4)
          ;(evalfreturnin,4)
          ;(evalfstart,4)
          ;(evalfstop,4)}
        Flow Graph:
          [0->{1},1->{2},2->{4,5},4->{6},5->{7},6->{4,5},7->{2}]
        Sizebounds:
          (<0,0,A>, A) (<0,0,B>, B) (<0,0,C>,     C) (<0,0,D>, D) 
          (<1,0,A>, 1) (<1,0,B>, B) (<1,0,C>,     C) (<1,0,D>, D) 
          (<2,0,A>, B) (<2,0,B>, B) (<2,0,C>,     1) (<2,0,D>, D) 
          (<4,0,A>, ?) (<4,0,B>, B) (<4,0,C>,     D) (<4,0,D>, D) 
          (<5,0,A>, ?) (<5,0,B>, B) (<5,0,C>, 1 + D) (<5,0,D>, D) 
          (<6,0,A>, ?) (<6,0,B>, B) (<6,0,C>,     D) (<6,0,D>, D) 
          (<7,0,A>, ?) (<7,0,B>, B) (<7,0,C>, 1 + D) (<7,0,D>, D) 
    + Applied Processor:
        KnowledgePropagation
    + Details:
        We propagate bounds from predecessors.
* Step 10: LocalSizeboundsProc WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0. evalfstart(A,B,C,D)   -> evalfentryin(A,B,C,D)   True         (1,1)        
          1. evalfentryin(A,B,C,D) -> evalfbb4in(1,B,C,D)     True         (2,1)        
          2. evalfbb4in(A,B,C,D)   -> evalfbb2in(A,B,1,D)     [B >= A]     (B,1)        
          4. evalfbb2in(A,B,C,D)   -> evalfbb1in(A,B,C,D)     [D >= C]     (3*B + B*D,1)
          5. evalfbb2in(A,B,C,D)   -> evalfbb3in(A,B,C,D)     [C >= 1 + D] (B,1)        
          6. evalfbb1in(A,B,C,D)   -> evalfbb2in(A,B,1 + C,D) True         (3*B + B*D,1)
          7. evalfbb3in(A,B,C,D)   -> evalfbb4in(1 + A,B,C,D) True         (B,1)        
        Signature:
          {(evalfbb1in,4)
          ;(evalfbb2in,4)
          ;(evalfbb3in,4)
          ;(evalfbb4in,4)
          ;(evalfentryin,4)
          ;(evalfreturnin,4)
          ;(evalfstart,4)
          ;(evalfstop,4)}
        Flow Graph:
          [0->{1},1->{2},2->{4,5},4->{6},5->{7},6->{4,5},7->{2}]
        Sizebounds:
          (<0,0,A>, A) (<0,0,B>, B) (<0,0,C>,     C) (<0,0,D>, D) 
          (<1,0,A>, 1) (<1,0,B>, B) (<1,0,C>,     C) (<1,0,D>, D) 
          (<2,0,A>, B) (<2,0,B>, B) (<2,0,C>,     1) (<2,0,D>, D) 
          (<4,0,A>, ?) (<4,0,B>, B) (<4,0,C>,     D) (<4,0,D>, D) 
          (<5,0,A>, ?) (<5,0,B>, B) (<5,0,C>, 1 + D) (<5,0,D>, D) 
          (<6,0,A>, ?) (<6,0,B>, B) (<6,0,C>,     D) (<6,0,D>, D) 
          (<7,0,A>, ?) (<7,0,B>, B) (<7,0,C>, 1 + D) (<7,0,D>, D) 
    + Applied Processor:
        LocalSizeboundsProc
    + Details:
        The problem is already solved.

WORST_CASE(?,O(n^2))