WORST_CASE(?,O(n^2))
* Step 1: RestrictVarsProcessor WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0. f0(A,B,C,D)  -> f4(0,B,C,D)         True                       (1,1)
          1. f4(A,B,C,D)  -> f8(1 + A,B,0,D)     [B >= 1 + A]               (?,1)
          2. f8(A,B,C,D)  -> f16(A,B,C,0)        [B >= 1 + A]               (?,1)
          3. f8(A,B,C,D)  -> f16(A,B,C,D)        [A >= B]                   (?,1)
          4. f8(A,B,C,D)  -> f8(1 + A,B,1 + C,E) [B >= 1 + A && 0 >= 1 + E] (?,1)
          5. f8(A,B,C,D)  -> f8(1 + A,B,1 + C,E) [B >= 1 + A && E >= 1]     (?,1)
          6. f16(A,B,C,D) -> f4(A,B,C,D)         [0 >= C]                   (?,1)
          7. f16(A,B,C,D) -> f4(-1 + A,B,C,D)    [C >= 1]                   (?,1)
          8. f4(A,B,C,D)  -> f20(A,B,C,D)        [A >= B]                   (?,1)
        Signature:
          {(f0,4);(f16,4);(f20,4);(f4,4);(f8,4)}
        Flow Graph:
          [0->{1,8},1->{2,3,4,5},2->{6,7},3->{6,7},4->{2,3,4,5},5->{2,3,4,5},6->{1,8},7->{1,8},8->{}]
        
    + Applied Processor:
        RestrictVarsProcessor
    + Details:
        We removed the arguments [D] .
* Step 2: LocalSizeboundsProc WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0. f0(A,B,C)  -> f4(0,B,C)         True                       (1,1)
          1. f4(A,B,C)  -> f8(1 + A,B,0)     [B >= 1 + A]               (?,1)
          2. f8(A,B,C)  -> f16(A,B,C)        [B >= 1 + A]               (?,1)
          3. f8(A,B,C)  -> f16(A,B,C)        [A >= B]                   (?,1)
          4. f8(A,B,C)  -> f8(1 + A,B,1 + C) [B >= 1 + A && 0 >= 1 + E] (?,1)
          5. f8(A,B,C)  -> f8(1 + A,B,1 + C) [B >= 1 + A && E >= 1]     (?,1)
          6. f16(A,B,C) -> f4(A,B,C)         [0 >= C]                   (?,1)
          7. f16(A,B,C) -> f4(-1 + A,B,C)    [C >= 1]                   (?,1)
          8. f4(A,B,C)  -> f20(A,B,C)        [A >= B]                   (?,1)
        Signature:
          {(f0,3);(f16,3);(f20,3);(f4,3);(f8,3)}
        Flow Graph:
          [0->{1,8},1->{2,3,4,5},2->{6,7},3->{6,7},4->{2,3,4,5},5->{2,3,4,5},6->{1,8},7->{1,8},8->{}]
        
    + Applied Processor:
        LocalSizeboundsProc
    + Details:
        LocalSizebounds generated; rvgraph
          (<0,0,A>,     0, .= 0) (<0,0,B>, B, .= 0) (<0,0,C>,     C, .= 0) 
          (<1,0,A>, 1 + A, .+ 1) (<1,0,B>, B, .= 0) (<1,0,C>,     0, .= 0) 
          (<2,0,A>,     A, .= 0) (<2,0,B>, B, .= 0) (<2,0,C>,     C, .= 0) 
          (<3,0,A>,     A, .= 0) (<3,0,B>, B, .= 0) (<3,0,C>,     C, .= 0) 
          (<4,0,A>, 1 + A, .+ 1) (<4,0,B>, B, .= 0) (<4,0,C>, 1 + C, .+ 1) 
          (<5,0,A>, 1 + A, .+ 1) (<5,0,B>, B, .= 0) (<5,0,C>, 1 + C, .+ 1) 
          (<6,0,A>,     A, .= 0) (<6,0,B>, B, .= 0) (<6,0,C>,     C, .= 0) 
          (<7,0,A>, 1 + A, .+ 1) (<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) 
* Step 3: SizeboundsProc WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0. f0(A,B,C)  -> f4(0,B,C)         True                       (1,1)
          1. f4(A,B,C)  -> f8(1 + A,B,0)     [B >= 1 + A]               (?,1)
          2. f8(A,B,C)  -> f16(A,B,C)        [B >= 1 + A]               (?,1)
          3. f8(A,B,C)  -> f16(A,B,C)        [A >= B]                   (?,1)
          4. f8(A,B,C)  -> f8(1 + A,B,1 + C) [B >= 1 + A && 0 >= 1 + E] (?,1)
          5. f8(A,B,C)  -> f8(1 + A,B,1 + C) [B >= 1 + A && E >= 1]     (?,1)
          6. f16(A,B,C) -> f4(A,B,C)         [0 >= C]                   (?,1)
          7. f16(A,B,C) -> f4(-1 + A,B,C)    [C >= 1]                   (?,1)
          8. f4(A,B,C)  -> f20(A,B,C)        [A >= B]                   (?,1)
        Signature:
          {(f0,3);(f16,3);(f20,3);(f4,3);(f8,3)}
        Flow Graph:
          [0->{1,8},1->{2,3,4,5},2->{6,7},3->{6,7},4->{2,3,4,5},5->{2,3,4,5},6->{1,8},7->{1,8},8->{}]
        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>, ?) 
    + Applied Processor:
        SizeboundsProc
    + Details:
        Sizebounds computed:
          (<0,0,A>, 0) (<0,0,B>, B) (<0,0,C>, C) 
          (<1,0,A>, B) (<1,0,B>, B) (<1,0,C>, 0) 
          (<2,0,A>, B) (<2,0,B>, B) (<2,0,C>, ?) 
          (<3,0,A>, B) (<3,0,B>, B) (<3,0,C>, ?) 
          (<4,0,A>, B) (<4,0,B>, B) (<4,0,C>, ?) 
          (<5,0,A>, B) (<5,0,B>, B) (<5,0,C>, ?) 
          (<6,0,A>, B) (<6,0,B>, B) (<6,0,C>, ?) 
          (<7,0,A>, B) (<7,0,B>, B) (<7,0,C>, ?) 
          (<8,0,A>, B) (<8,0,B>, B) (<8,0,C>, ?) 
* Step 4: LeafRules WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0. f0(A,B,C)  -> f4(0,B,C)         True                       (1,1)
          1. f4(A,B,C)  -> f8(1 + A,B,0)     [B >= 1 + A]               (?,1)
          2. f8(A,B,C)  -> f16(A,B,C)        [B >= 1 + A]               (?,1)
          3. f8(A,B,C)  -> f16(A,B,C)        [A >= B]                   (?,1)
          4. f8(A,B,C)  -> f8(1 + A,B,1 + C) [B >= 1 + A && 0 >= 1 + E] (?,1)
          5. f8(A,B,C)  -> f8(1 + A,B,1 + C) [B >= 1 + A && E >= 1]     (?,1)
          6. f16(A,B,C) -> f4(A,B,C)         [0 >= C]                   (?,1)
          7. f16(A,B,C) -> f4(-1 + A,B,C)    [C >= 1]                   (?,1)
          8. f4(A,B,C)  -> f20(A,B,C)        [A >= B]                   (?,1)
        Signature:
          {(f0,3);(f16,3);(f20,3);(f4,3);(f8,3)}
        Flow Graph:
          [0->{1,8},1->{2,3,4,5},2->{6,7},3->{6,7},4->{2,3,4,5},5->{2,3,4,5},6->{1,8},7->{1,8},8->{}]
        Sizebounds:
          (<0,0,A>, 0) (<0,0,B>, B) (<0,0,C>, C) 
          (<1,0,A>, B) (<1,0,B>, B) (<1,0,C>, 0) 
          (<2,0,A>, B) (<2,0,B>, B) (<2,0,C>, ?) 
          (<3,0,A>, B) (<3,0,B>, B) (<3,0,C>, ?) 
          (<4,0,A>, B) (<4,0,B>, B) (<4,0,C>, ?) 
          (<5,0,A>, B) (<5,0,B>, B) (<5,0,C>, ?) 
          (<6,0,A>, B) (<6,0,B>, B) (<6,0,C>, ?) 
          (<7,0,A>, B) (<7,0,B>, B) (<7,0,C>, ?) 
          (<8,0,A>, B) (<8,0,B>, B) (<8,0,C>, ?) 
    + Applied Processor:
        LeafRules
    + Details:
        The following transitions are estimated by its predecessors and are removed [8]
* Step 5: PolyRank WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0. f0(A,B,C)  -> f4(0,B,C)         True                       (1,1)
          1. f4(A,B,C)  -> f8(1 + A,B,0)     [B >= 1 + A]               (?,1)
          2. f8(A,B,C)  -> f16(A,B,C)        [B >= 1 + A]               (?,1)
          3. f8(A,B,C)  -> f16(A,B,C)        [A >= B]                   (?,1)
          4. f8(A,B,C)  -> f8(1 + A,B,1 + C) [B >= 1 + A && 0 >= 1 + E] (?,1)
          5. f8(A,B,C)  -> f8(1 + A,B,1 + C) [B >= 1 + A && E >= 1]     (?,1)
          6. f16(A,B,C) -> f4(A,B,C)         [0 >= C]                   (?,1)
          7. f16(A,B,C) -> f4(-1 + A,B,C)    [C >= 1]                   (?,1)
        Signature:
          {(f0,3);(f16,3);(f20,3);(f4,3);(f8,3)}
        Flow Graph:
          [0->{1},1->{2,3,4,5},2->{6,7},3->{6,7},4->{2,3,4,5},5->{2,3,4,5},6->{1},7->{1}]
        Sizebounds:
          (<0,0,A>, 0) (<0,0,B>, B) (<0,0,C>, C) 
          (<1,0,A>, B) (<1,0,B>, B) (<1,0,C>, 0) 
          (<2,0,A>, B) (<2,0,B>, B) (<2,0,C>, ?) 
          (<3,0,A>, B) (<3,0,B>, B) (<3,0,C>, ?) 
          (<4,0,A>, B) (<4,0,B>, B) (<4,0,C>, ?) 
          (<5,0,A>, B) (<5,0,B>, B) (<5,0,C>, ?) 
          (<6,0,A>, B) (<6,0,B>, B) (<6,0,C>, ?) 
          (<7,0,A>, B) (<7,0,B>, B) (<7,0,C>, ?) 
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
           p(f0) = x2            
          p(f16) = 1 + -1*x1 + x2
           p(f4) = -1*x1 + x2    
           p(f8) = 1 + -1*x1 + x2
        
        The following rules are strictly oriented:
        [B >= 1 + A && 0 >= 1 + E] ==>                  
                         f8(A,B,C)   = 1 + -1*A + B     
                                     > -1*A + B         
                                     = f8(1 + A,B,1 + C)
        
            [B >= 1 + A && E >= 1] ==>                  
                         f8(A,B,C)   = 1 + -1*A + B     
                                     > -1*A + B         
                                     = f8(1 + A,B,1 + C)
        
        
        The following rules are weakly oriented:
                True ==>               
           f0(A,B,C)   = B             
                      >= B             
                       = f4(0,B,C)     
        
        [B >= 1 + A] ==>               
           f4(A,B,C)   = -1*A + B      
                      >= -1*A + B      
                       = f8(1 + A,B,0) 
        
        [B >= 1 + A] ==>               
           f8(A,B,C)   = 1 + -1*A + B  
                      >= 1 + -1*A + B  
                       = f16(A,B,C)    
        
            [A >= B] ==>               
           f8(A,B,C)   = 1 + -1*A + B  
                      >= 1 + -1*A + B  
                       = f16(A,B,C)    
        
            [0 >= C] ==>               
          f16(A,B,C)   = 1 + -1*A + B  
                      >= -1*A + B      
                       = f4(A,B,C)     
        
            [C >= 1] ==>               
          f16(A,B,C)   = 1 + -1*A + B  
                      >= 1 + -1*A + B  
                       = f4(-1 + A,B,C)
        
        
* Step 6: ChainProcessor WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0. f0(A,B,C)  -> f4(0,B,C)         True                       (1,1)
          1. f4(A,B,C)  -> f8(1 + A,B,0)     [B >= 1 + A]               (?,1)
          2. f8(A,B,C)  -> f16(A,B,C)        [B >= 1 + A]               (?,1)
          3. f8(A,B,C)  -> f16(A,B,C)        [A >= B]                   (?,1)
          4. f8(A,B,C)  -> f8(1 + A,B,1 + C) [B >= 1 + A && 0 >= 1 + E] (B,1)
          5. f8(A,B,C)  -> f8(1 + A,B,1 + C) [B >= 1 + A && E >= 1]     (B,1)
          6. f16(A,B,C) -> f4(A,B,C)         [0 >= C]                   (?,1)
          7. f16(A,B,C) -> f4(-1 + A,B,C)    [C >= 1]                   (?,1)
        Signature:
          {(f0,3);(f16,3);(f20,3);(f4,3);(f8,3)}
        Flow Graph:
          [0->{1},1->{2,3,4,5},2->{6,7},3->{6,7},4->{2,3,4,5},5->{2,3,4,5},6->{1},7->{1}]
        Sizebounds:
          (<0,0,A>, 0) (<0,0,B>, B) (<0,0,C>, C) 
          (<1,0,A>, B) (<1,0,B>, B) (<1,0,C>, 0) 
          (<2,0,A>, B) (<2,0,B>, B) (<2,0,C>, ?) 
          (<3,0,A>, B) (<3,0,B>, B) (<3,0,C>, ?) 
          (<4,0,A>, B) (<4,0,B>, B) (<4,0,C>, ?) 
          (<5,0,A>, B) (<5,0,B>, B) (<5,0,C>, ?) 
          (<6,0,A>, B) (<6,0,B>, B) (<6,0,C>, ?) 
          (<7,0,A>, B) (<7,0,B>, B) (<7,0,C>, ?) 
    + Applied Processor:
        ChainProcessor False [0,1,2,3,4,5,6,7]
    + Details:
        We chained rule 0 to obtain the rules [8] .
* Step 7: ChainProcessor WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          1. f4(A,B,C)  -> f8(1 + A,B,0)     [B >= 1 + A]               (?,1)
          2. f8(A,B,C)  -> f16(A,B,C)        [B >= 1 + A]               (?,1)
          3. f8(A,B,C)  -> f16(A,B,C)        [A >= B]                   (?,1)
          4. f8(A,B,C)  -> f8(1 + A,B,1 + C) [B >= 1 + A && 0 >= 1 + E] (B,1)
          5. f8(A,B,C)  -> f8(1 + A,B,1 + C) [B >= 1 + A && E >= 1]     (B,1)
          6. f16(A,B,C) -> f4(A,B,C)         [0 >= C]                   (?,1)
          7. f16(A,B,C) -> f4(-1 + A,B,C)    [C >= 1]                   (?,1)
          8. f0(A,B,C)  -> f8(1,B,0)         [B >= 1]                   (1,2)
        Signature:
          {(f0,3);(f16,3);(f20,3);(f4,3);(f8,3)}
        Flow Graph:
          [1->{2,3,4,5},2->{6,7},3->{6,7},4->{2,3,4,5},5->{2,3,4,5},6->{1},7->{1},8->{2,3,4,5}]
        Sizebounds:
          (<1,0,A>, B) (<1,0,B>, B) (<1,0,C>, 0) 
          (<2,0,A>, B) (<2,0,B>, B) (<2,0,C>, ?) 
          (<3,0,A>, B) (<3,0,B>, B) (<3,0,C>, ?) 
          (<4,0,A>, B) (<4,0,B>, B) (<4,0,C>, ?) 
          (<5,0,A>, B) (<5,0,B>, B) (<5,0,C>, ?) 
          (<6,0,A>, B) (<6,0,B>, B) (<6,0,C>, ?) 
          (<7,0,A>, B) (<7,0,B>, B) (<7,0,C>, ?) 
          (<8,0,A>, B) (<8,0,B>, B) (<8,0,C>, 0) 
    + Applied Processor:
        ChainProcessor False [1,2,3,4,5,6,7,8]
    + Details:
        We chained rule 2 to obtain the rules [9,10] .
* Step 8: ChainProcessor WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          1.  f4(A,B,C)  -> f8(1 + A,B,0)     [B >= 1 + A]               (?,1)
          3.  f8(A,B,C)  -> f16(A,B,C)        [A >= B]                   (?,1)
          4.  f8(A,B,C)  -> f8(1 + A,B,1 + C) [B >= 1 + A && 0 >= 1 + E] (B,1)
          5.  f8(A,B,C)  -> f8(1 + A,B,1 + C) [B >= 1 + A && E >= 1]     (B,1)
          6.  f16(A,B,C) -> f4(A,B,C)         [0 >= C]                   (?,1)
          7.  f16(A,B,C) -> f4(-1 + A,B,C)    [C >= 1]                   (?,1)
          8.  f0(A,B,C)  -> f8(1,B,0)         [B >= 1]                   (1,2)
          9.  f8(A,B,C)  -> f4(A,B,C)         [B >= 1 + A && 0 >= C]     (?,2)
          10. f8(A,B,C)  -> f4(-1 + A,B,C)    [B >= 1 + A && C >= 1]     (?,2)
        Signature:
          {(f0,3);(f16,3);(f20,3);(f4,3);(f8,3)}
        Flow Graph:
          [1->{3,4,5,9,10},3->{6,7},4->{3,4,5,9,10},5->{3,4,5,9,10},6->{1},7->{1},8->{3,4,5,9,10},9->{1},10->{1}]
        Sizebounds:
          (< 1,0,A>, B) (< 1,0,B>, B) (< 1,0,C>, 0) 
          (< 3,0,A>, B) (< 3,0,B>, B) (< 3,0,C>, ?) 
          (< 4,0,A>, B) (< 4,0,B>, B) (< 4,0,C>, ?) 
          (< 5,0,A>, B) (< 5,0,B>, B) (< 5,0,C>, ?) 
          (< 6,0,A>, B) (< 6,0,B>, B) (< 6,0,C>, ?) 
          (< 7,0,A>, B) (< 7,0,B>, B) (< 7,0,C>, ?) 
          (< 8,0,A>, B) (< 8,0,B>, B) (< 8,0,C>, 0) 
          (< 9,0,A>, B) (< 9,0,B>, B) (< 9,0,C>, ?) 
          (<10,0,A>, B) (<10,0,B>, B) (<10,0,C>, ?) 
    + Applied Processor:
        ChainProcessor False [1,3,4,5,6,7,8,9,10]
    + Details:
        We chained rule 3 to obtain the rules [11,12] .
* Step 9: UnreachableRules WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          1.  f4(A,B,C)  -> f8(1 + A,B,0)     [B >= 1 + A]               (?,1)
          4.  f8(A,B,C)  -> f8(1 + A,B,1 + C) [B >= 1 + A && 0 >= 1 + E] (B,1)
          5.  f8(A,B,C)  -> f8(1 + A,B,1 + C) [B >= 1 + A && E >= 1]     (B,1)
          6.  f16(A,B,C) -> f4(A,B,C)         [0 >= C]                   (?,1)
          7.  f16(A,B,C) -> f4(-1 + A,B,C)    [C >= 1]                   (?,1)
          8.  f0(A,B,C)  -> f8(1,B,0)         [B >= 1]                   (1,2)
          9.  f8(A,B,C)  -> f4(A,B,C)         [B >= 1 + A && 0 >= C]     (?,2)
          10. f8(A,B,C)  -> f4(-1 + A,B,C)    [B >= 1 + A && C >= 1]     (?,2)
          11. f8(A,B,C)  -> f4(A,B,C)         [A >= B && 0 >= C]         (?,2)
          12. f8(A,B,C)  -> f4(-1 + A,B,C)    [A >= B && C >= 1]         (?,2)
        Signature:
          {(f0,3);(f16,3);(f20,3);(f4,3);(f8,3)}
        Flow Graph:
          [1->{4,5,9,10,11,12},4->{4,5,9,10,11,12},5->{4,5,9,10,11,12},6->{1},7->{1},8->{4,5,9,10,11,12},9->{1}
          ,10->{1},11->{1},12->{1}]
        Sizebounds:
          (< 1,0,A>, B) (< 1,0,B>, B) (< 1,0,C>, 0) 
          (< 4,0,A>, B) (< 4,0,B>, B) (< 4,0,C>, ?) 
          (< 5,0,A>, B) (< 5,0,B>, B) (< 5,0,C>, ?) 
          (< 6,0,A>, B) (< 6,0,B>, B) (< 6,0,C>, ?) 
          (< 7,0,A>, B) (< 7,0,B>, B) (< 7,0,C>, ?) 
          (< 8,0,A>, B) (< 8,0,B>, B) (< 8,0,C>, 0) 
          (< 9,0,A>, B) (< 9,0,B>, B) (< 9,0,C>, ?) 
          (<10,0,A>, B) (<10,0,B>, B) (<10,0,C>, ?) 
          (<11,0,A>, B) (<11,0,B>, B) (<11,0,C>, ?) 
          (<12,0,A>, B) (<12,0,B>, B) (<12,0,C>, ?) 
    + Applied Processor:
        UnreachableRules
    + Details:
        The following transitions are not reachable from the starting states and are removed: [6,7]
* Step 10: ChainProcessor WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          1.  f4(A,B,C) -> f8(1 + A,B,0)     [B >= 1 + A]               (?,1)
          4.  f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && 0 >= 1 + E] (B,1)
          5.  f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && E >= 1]     (B,1)
          8.  f0(A,B,C) -> f8(1,B,0)         [B >= 1]                   (1,2)
          9.  f8(A,B,C) -> f4(A,B,C)         [B >= 1 + A && 0 >= C]     (?,2)
          10. f8(A,B,C) -> f4(-1 + A,B,C)    [B >= 1 + A && C >= 1]     (?,2)
          11. f8(A,B,C) -> f4(A,B,C)         [A >= B && 0 >= C]         (?,2)
          12. f8(A,B,C) -> f4(-1 + A,B,C)    [A >= B && C >= 1]         (?,2)
        Signature:
          {(f0,3);(f16,3);(f20,3);(f4,3);(f8,3)}
        Flow Graph:
          [1->{4,5,9,10,11,12},4->{4,5,9,10,11,12},5->{4,5,9,10,11,12},8->{4,5,9,10,11,12},9->{1},10->{1},11->{1}
          ,12->{1}]
        Sizebounds:
          (< 1,0,A>, B) (< 1,0,B>, B) (< 1,0,C>, 0) 
          (< 4,0,A>, B) (< 4,0,B>, B) (< 4,0,C>, ?) 
          (< 5,0,A>, B) (< 5,0,B>, B) (< 5,0,C>, ?) 
          (< 8,0,A>, B) (< 8,0,B>, B) (< 8,0,C>, 0) 
          (< 9,0,A>, B) (< 9,0,B>, B) (< 9,0,C>, ?) 
          (<10,0,A>, B) (<10,0,B>, B) (<10,0,C>, ?) 
          (<11,0,A>, B) (<11,0,B>, B) (<11,0,C>, ?) 
          (<12,0,A>, B) (<12,0,B>, B) (<12,0,C>, ?) 
    + Applied Processor:
        ChainProcessor False [1,4,5,8,9,10,11,12]
    + Details:
        We chained rule 9 to obtain the rules [13] .
* Step 11: ChainProcessor WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          1.  f4(A,B,C) -> f8(1 + A,B,0)     [B >= 1 + A]                         (?,1)
          4.  f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && 0 >= 1 + E]           (B,1)
          5.  f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && E >= 1]               (B,1)
          8.  f0(A,B,C) -> f8(1,B,0)         [B >= 1]                             (1,2)
          10. f8(A,B,C) -> f4(-1 + A,B,C)    [B >= 1 + A && C >= 1]               (?,2)
          11. f8(A,B,C) -> f4(A,B,C)         [A >= B && 0 >= C]                   (?,2)
          12. f8(A,B,C) -> f4(-1 + A,B,C)    [A >= B && C >= 1]                   (?,2)
          13. f8(A,B,C) -> f8(1 + A,B,0)     [B >= 1 + A && 0 >= C && B >= 1 + A] (?,3)
        Signature:
          {(f0,3);(f16,3);(f20,3);(f4,3);(f8,3)}
        Flow Graph:
          [1->{4,5,10,11,12,13},4->{4,5,10,11,12,13},5->{4,5,10,11,12,13},8->{4,5,10,11,12,13},10->{1},11->{1}
          ,12->{1},13->{4,5,10,11,12,13}]
        Sizebounds:
          (< 1,0,A>, B) (< 1,0,B>, B) (< 1,0,C>, 0) 
          (< 4,0,A>, B) (< 4,0,B>, B) (< 4,0,C>, ?) 
          (< 5,0,A>, B) (< 5,0,B>, B) (< 5,0,C>, ?) 
          (< 8,0,A>, B) (< 8,0,B>, B) (< 8,0,C>, 0) 
          (<10,0,A>, B) (<10,0,B>, B) (<10,0,C>, ?) 
          (<11,0,A>, B) (<11,0,B>, B) (<11,0,C>, ?) 
          (<12,0,A>, B) (<12,0,B>, B) (<12,0,C>, ?) 
          (<13,0,A>, B) (<13,0,B>, B) (<13,0,C>, 0) 
    + Applied Processor:
        ChainProcessor False [1,4,5,8,10,11,12,13]
    + Details:
        We chained rule 10 to obtain the rules [14] .
* Step 12: ChainProcessor WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          1.  f4(A,B,C) -> f8(1 + A,B,0)     [B >= 1 + A]                         (?,1)
          4.  f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && 0 >= 1 + E]           (B,1)
          5.  f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && E >= 1]               (B,1)
          8.  f0(A,B,C) -> f8(1,B,0)         [B >= 1]                             (1,2)
          11. f8(A,B,C) -> f4(A,B,C)         [A >= B && 0 >= C]                   (?,2)
          12. f8(A,B,C) -> f4(-1 + A,B,C)    [A >= B && C >= 1]                   (?,2)
          13. f8(A,B,C) -> f8(1 + A,B,0)     [B >= 1 + A && 0 >= C && B >= 1 + A] (?,3)
          14. f8(A,B,C) -> f8(A,B,0)         [B >= 1 + A && C >= 1 && B >= A]     (?,3)
        Signature:
          {(f0,3);(f16,3);(f20,3);(f4,3);(f8,3)}
        Flow Graph:
          [1->{4,5,11,12,13,14},4->{4,5,11,12,13,14},5->{4,5,11,12,13,14},8->{4,5,11,12,13,14},11->{1},12->{1}
          ,13->{4,5,11,12,13,14},14->{4,5,11,12,13,14}]
        Sizebounds:
          (< 1,0,A>, B) (< 1,0,B>, B) (< 1,0,C>, 0) 
          (< 4,0,A>, B) (< 4,0,B>, B) (< 4,0,C>, ?) 
          (< 5,0,A>, B) (< 5,0,B>, B) (< 5,0,C>, ?) 
          (< 8,0,A>, B) (< 8,0,B>, B) (< 8,0,C>, 0) 
          (<11,0,A>, B) (<11,0,B>, B) (<11,0,C>, ?) 
          (<12,0,A>, B) (<12,0,B>, B) (<12,0,C>, ?) 
          (<13,0,A>, B) (<13,0,B>, B) (<13,0,C>, 0) 
          (<14,0,A>, B) (<14,0,B>, B) (<14,0,C>, 0) 
    + Applied Processor:
        ChainProcessor False [1,4,5,8,11,12,13,14]
    + Details:
        We chained rule 11 to obtain the rules [15] .
* Step 13: ChainProcessor WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          1.  f4(A,B,C) -> f8(1 + A,B,0)     [B >= 1 + A]                         (?,1)
          4.  f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && 0 >= 1 + E]           (B,1)
          5.  f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && E >= 1]               (B,1)
          8.  f0(A,B,C) -> f8(1,B,0)         [B >= 1]                             (1,2)
          12. f8(A,B,C) -> f4(-1 + A,B,C)    [A >= B && C >= 1]                   (?,2)
          13. f8(A,B,C) -> f8(1 + A,B,0)     [B >= 1 + A && 0 >= C && B >= 1 + A] (?,3)
          14. f8(A,B,C) -> f8(A,B,0)         [B >= 1 + A && C >= 1 && B >= A]     (?,3)
          15. f8(A,B,C) -> f8(1 + A,B,0)     [A >= B && 0 >= C && B >= 1 + A]     (?,3)
        Signature:
          {(f0,3);(f16,3);(f20,3);(f4,3);(f8,3)}
        Flow Graph:
          [1->{4,5,12,13,14,15},4->{4,5,12,13,14,15},5->{4,5,12,13,14,15},8->{4,5,12,13,14,15},12->{1},13->{4,5,12
          ,13,14,15},14->{4,5,12,13,14,15},15->{4,5,12,13,14,15}]
        Sizebounds:
          (< 1,0,A>, B) (< 1,0,B>, B) (< 1,0,C>, 0) 
          (< 4,0,A>, B) (< 4,0,B>, B) (< 4,0,C>, ?) 
          (< 5,0,A>, B) (< 5,0,B>, B) (< 5,0,C>, ?) 
          (< 8,0,A>, B) (< 8,0,B>, B) (< 8,0,C>, 0) 
          (<12,0,A>, B) (<12,0,B>, B) (<12,0,C>, ?) 
          (<13,0,A>, B) (<13,0,B>, B) (<13,0,C>, 0) 
          (<14,0,A>, B) (<14,0,B>, B) (<14,0,C>, 0) 
          (<15,0,A>, B) (<15,0,B>, B) (<15,0,C>, 0) 
    + Applied Processor:
        ChainProcessor False [1,4,5,8,12,13,14,15]
    + Details:
        We chained rule 12 to obtain the rules [16] .
* Step 14: UnreachableRules WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          1.  f4(A,B,C) -> f8(1 + A,B,0)     [B >= 1 + A]                         (?,1)
          4.  f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && 0 >= 1 + E]           (B,1)
          5.  f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && E >= 1]               (B,1)
          8.  f0(A,B,C) -> f8(1,B,0)         [B >= 1]                             (1,2)
          13. f8(A,B,C) -> f8(1 + A,B,0)     [B >= 1 + A && 0 >= C && B >= 1 + A] (?,3)
          14. f8(A,B,C) -> f8(A,B,0)         [B >= 1 + A && C >= 1 && B >= A]     (?,3)
          15. f8(A,B,C) -> f8(1 + A,B,0)     [A >= B && 0 >= C && B >= 1 + A]     (?,3)
          16. f8(A,B,C) -> f8(A,B,0)         [A >= B && C >= 1 && B >= A]         (?,3)
        Signature:
          {(f0,3);(f16,3);(f20,3);(f4,3);(f8,3)}
        Flow Graph:
          [1->{4,5,13,14,15,16},4->{4,5,13,14,15,16},5->{4,5,13,14,15,16},8->{4,5,13,14,15,16},13->{4,5,13,14,15,16}
          ,14->{4,5,13,14,15,16},15->{4,5,13,14,15,16},16->{4,5,13,14,15,16}]
        Sizebounds:
          (< 1,0,A>, B) (< 1,0,B>, B) (< 1,0,C>, 0) 
          (< 4,0,A>, B) (< 4,0,B>, B) (< 4,0,C>, ?) 
          (< 5,0,A>, B) (< 5,0,B>, B) (< 5,0,C>, ?) 
          (< 8,0,A>, B) (< 8,0,B>, B) (< 8,0,C>, 0) 
          (<13,0,A>, B) (<13,0,B>, B) (<13,0,C>, 0) 
          (<14,0,A>, B) (<14,0,B>, B) (<14,0,C>, 0) 
          (<15,0,A>, B) (<15,0,B>, B) (<15,0,C>, 0) 
          (<16,0,A>, B) (<16,0,B>, B) (<16,0,C>, 0) 
    + Applied Processor:
        UnreachableRules
    + Details:
        The following transitions are not reachable from the starting states and are removed: [1]
* Step 15: UnsatPaths WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          4.  f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && 0 >= 1 + E]           (B,1)
          5.  f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && E >= 1]               (B,1)
          8.  f0(A,B,C) -> f8(1,B,0)         [B >= 1]                             (1,2)
          13. f8(A,B,C) -> f8(1 + A,B,0)     [B >= 1 + A && 0 >= C && B >= 1 + A] (?,3)
          14. f8(A,B,C) -> f8(A,B,0)         [B >= 1 + A && C >= 1 && B >= A]     (?,3)
          15. f8(A,B,C) -> f8(1 + A,B,0)     [A >= B && 0 >= C && B >= 1 + A]     (?,3)
          16. f8(A,B,C) -> f8(A,B,0)         [A >= B && C >= 1 && B >= A]         (?,3)
        Signature:
          {(f0,3);(f16,3);(f20,3);(f4,3);(f8,3)}
        Flow Graph:
          [4->{4,5,13,14,15,16},5->{4,5,13,14,15,16},8->{4,5,13,14,15,16},13->{4,5,13,14,15,16},14->{4,5,13,14,15
          ,16},15->{4,5,13,14,15,16},16->{4,5,13,14,15,16}]
        Sizebounds:
          (< 4,0,A>, B) (< 4,0,B>, B) (< 4,0,C>, ?) 
          (< 5,0,A>, B) (< 5,0,B>, B) (< 5,0,C>, ?) 
          (< 8,0,A>, B) (< 8,0,B>, B) (< 8,0,C>, 0) 
          (<13,0,A>, B) (<13,0,B>, B) (<13,0,C>, 0) 
          (<14,0,A>, B) (<14,0,B>, B) (<14,0,C>, 0) 
          (<15,0,A>, B) (<15,0,B>, B) (<15,0,C>, 0) 
          (<16,0,A>, B) (<16,0,B>, B) (<16,0,C>, 0) 
    + Applied Processor:
        UnsatPaths
    + Details:
        We remove following edges from the transition graph: [(4,15)
                                                             ,(5,15)
                                                             ,(8,14)
                                                             ,(8,15)
                                                             ,(8,16)
                                                             ,(13,14)
                                                             ,(13,15)
                                                             ,(13,16)
                                                             ,(14,14)
                                                             ,(14,15)
                                                             ,(14,16)
                                                             ,(15,4)
                                                             ,(15,5)
                                                             ,(15,13)
                                                             ,(15,14)
                                                             ,(15,15)
                                                             ,(15,16)
                                                             ,(16,4)
                                                             ,(16,5)
                                                             ,(16,13)
                                                             ,(16,14)
                                                             ,(16,15)
                                                             ,(16,16)]
* Step 16: UnreachableRules WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          4.  f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && 0 >= 1 + E]           (B,1)
          5.  f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && E >= 1]               (B,1)
          8.  f0(A,B,C) -> f8(1,B,0)         [B >= 1]                             (1,2)
          13. f8(A,B,C) -> f8(1 + A,B,0)     [B >= 1 + A && 0 >= C && B >= 1 + A] (?,3)
          14. f8(A,B,C) -> f8(A,B,0)         [B >= 1 + A && C >= 1 && B >= A]     (?,3)
          15. f8(A,B,C) -> f8(1 + A,B,0)     [A >= B && 0 >= C && B >= 1 + A]     (?,3)
          16. f8(A,B,C) -> f8(A,B,0)         [A >= B && C >= 1 && B >= A]         (?,3)
        Signature:
          {(f0,3);(f16,3);(f20,3);(f4,3);(f8,3)}
        Flow Graph:
          [4->{4,5,13,14,16},5->{4,5,13,14,16},8->{4,5,13},13->{4,5,13},14->{4,5,13},15->{},16->{}]
        Sizebounds:
          (< 4,0,A>, B) (< 4,0,B>, B) (< 4,0,C>, ?) 
          (< 5,0,A>, B) (< 5,0,B>, B) (< 5,0,C>, ?) 
          (< 8,0,A>, B) (< 8,0,B>, B) (< 8,0,C>, 0) 
          (<13,0,A>, B) (<13,0,B>, B) (<13,0,C>, 0) 
          (<14,0,A>, B) (<14,0,B>, B) (<14,0,C>, 0) 
          (<15,0,A>, B) (<15,0,B>, B) (<15,0,C>, 0) 
          (<16,0,A>, B) (<16,0,B>, B) (<16,0,C>, 0) 
    + Applied Processor:
        UnreachableRules
    + Details:
        The following transitions are not reachable from the starting states and are removed: [15]
* Step 17: LeafRules WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          4.  f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && 0 >= 1 + E]           (B,1)
          5.  f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && E >= 1]               (B,1)
          8.  f0(A,B,C) -> f8(1,B,0)         [B >= 1]                             (1,2)
          13. f8(A,B,C) -> f8(1 + A,B,0)     [B >= 1 + A && 0 >= C && B >= 1 + A] (?,3)
          14. f8(A,B,C) -> f8(A,B,0)         [B >= 1 + A && C >= 1 && B >= A]     (?,3)
          16. f8(A,B,C) -> f8(A,B,0)         [A >= B && C >= 1 && B >= A]         (?,3)
        Signature:
          {(f0,3);(f16,3);(f20,3);(f4,3);(f8,3)}
        Flow Graph:
          [4->{4,5,13,14,16},5->{4,5,13,14,16},8->{4,5,13},13->{4,5,13},14->{4,5,13},16->{}]
        Sizebounds:
          (< 4,0,A>, B) (< 4,0,B>, B) (< 4,0,C>, ?) 
          (< 5,0,A>, B) (< 5,0,B>, B) (< 5,0,C>, ?) 
          (< 8,0,A>, B) (< 8,0,B>, B) (< 8,0,C>, 0) 
          (<13,0,A>, B) (<13,0,B>, B) (<13,0,C>, 0) 
          (<14,0,A>, B) (<14,0,B>, B) (<14,0,C>, 0) 
          (<16,0,A>, B) (<16,0,B>, B) (<16,0,C>, 0) 
    + Applied Processor:
        LeafRules
    + Details:
        The following transitions are estimated by its predecessors and are removed [16]
* Step 18: LocalSizeboundsProc WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          4.  f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && 0 >= 1 + E]           (B,1)
          5.  f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && E >= 1]               (B,1)
          8.  f0(A,B,C) -> f8(1,B,0)         [B >= 1]                             (1,2)
          13. f8(A,B,C) -> f8(1 + A,B,0)     [B >= 1 + A && 0 >= C && B >= 1 + A] (?,3)
          14. f8(A,B,C) -> f8(A,B,0)         [B >= 1 + A && C >= 1 && B >= A]     (?,3)
        Signature:
          {(f0,3);(f16,3);(f20,3);(f4,3);(f8,3)}
        Flow Graph:
          [4->{4,5,13,14},5->{4,5,13,14},8->{4,5,13},13->{4,5,13},14->{4,5,13}]
        Sizebounds:
          (< 4,0,A>, B) (< 4,0,B>, B) (< 4,0,C>, ?) 
          (< 5,0,A>, B) (< 5,0,B>, B) (< 5,0,C>, ?) 
          (< 8,0,A>, B) (< 8,0,B>, B) (< 8,0,C>, 0) 
          (<13,0,A>, B) (<13,0,B>, B) (<13,0,C>, 0) 
          (<14,0,A>, B) (<14,0,B>, B) (<14,0,C>, 0) 
    + Applied Processor:
        LocalSizeboundsProc
    + Details:
        LocalSizebounds generated; rvgraph
          (< 4,0,A>, 1 + A, .+ 1) (< 4,0,B>, B, .= 0) (< 4,0,C>, 1 + C, .+ 1) 
          (< 5,0,A>, 1 + A, .+ 1) (< 5,0,B>, B, .= 0) (< 5,0,C>, 1 + C, .+ 1) 
          (< 8,0,A>,     1, .= 1) (< 8,0,B>, B, .= 0) (< 8,0,C>,     0, .= 0) 
          (<13,0,A>, 1 + A, .+ 1) (<13,0,B>, B, .= 0) (<13,0,C>,     0, .= 0) 
          (<14,0,A>,     A, .= 0) (<14,0,B>, B, .= 0) (<14,0,C>,     0, .= 0) 
* Step 19: SizeboundsProc WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          4.  f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && 0 >= 1 + E]           (B,1)
          5.  f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && E >= 1]               (B,1)
          8.  f0(A,B,C) -> f8(1,B,0)         [B >= 1]                             (1,2)
          13. f8(A,B,C) -> f8(1 + A,B,0)     [B >= 1 + A && 0 >= C && B >= 1 + A] (?,3)
          14. f8(A,B,C) -> f8(A,B,0)         [B >= 1 + A && C >= 1 && B >= A]     (?,3)
        Signature:
          {(f0,3);(f16,3);(f20,3);(f4,3);(f8,3)}
        Flow Graph:
          [4->{4,5,13,14},5->{4,5,13,14},8->{4,5,13},13->{4,5,13},14->{4,5,13}]
        Sizebounds:
          (< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, ?) 
          (< 5,0,A>, ?) (< 5,0,B>, ?) (< 5,0,C>, ?) 
          (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?) 
          (<13,0,A>, ?) (<13,0,B>, ?) (<13,0,C>, ?) 
          (<14,0,A>, ?) (<14,0,B>, ?) (<14,0,C>, ?) 
    + Applied Processor:
        SizeboundsProc
    + Details:
        Sizebounds computed:
          (< 4,0,A>, B) (< 4,0,B>, B) (< 4,0,C>, 2*B) 
          (< 5,0,A>, B) (< 5,0,B>, B) (< 5,0,C>, 2*B) 
          (< 8,0,A>, 1) (< 8,0,B>, B) (< 8,0,C>,   0) 
          (<13,0,A>, B) (<13,0,B>, B) (<13,0,C>,   0) 
          (<14,0,A>, B) (<14,0,B>, B) (<14,0,C>,   0) 
* Step 20: LocationConstraintsProc WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          4.  f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && 0 >= 1 + E]           (B,1)
          5.  f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && E >= 1]               (B,1)
          8.  f0(A,B,C) -> f8(1,B,0)         [B >= 1]                             (1,2)
          13. f8(A,B,C) -> f8(1 + A,B,0)     [B >= 1 + A && 0 >= C && B >= 1 + A] (?,3)
          14. f8(A,B,C) -> f8(A,B,0)         [B >= 1 + A && C >= 1 && B >= A]     (?,3)
        Signature:
          {(f0,3);(f16,3);(f20,3);(f4,3);(f8,3)}
        Flow Graph:
          [4->{4,5,13,14},5->{4,5,13,14},8->{4,5,13},13->{4,5,13},14->{4,5,13}]
        Sizebounds:
          (< 4,0,A>, B) (< 4,0,B>, B) (< 4,0,C>, 2*B) 
          (< 5,0,A>, B) (< 5,0,B>, B) (< 5,0,C>, 2*B) 
          (< 8,0,A>, 1) (< 8,0,B>, B) (< 8,0,C>,   0) 
          (<13,0,A>, B) (<13,0,B>, B) (<13,0,C>,   0) 
          (<14,0,A>, B) (<14,0,B>, B) (<14,0,C>,   0) 
    + Applied Processor:
        LocationConstraintsProc
    + Details:
        We computed the location constraints  4 :  [B >= A] 5 :  [B >= A] 8 :  True 13 :  [B >= A] 14 :  [B >= A] .
* Step 21: PolyRank WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          4.  f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && 0 >= 1 + E]           (B,1)
          5.  f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && E >= 1]               (B,1)
          8.  f0(A,B,C) -> f8(1,B,0)         [B >= 1]                             (1,2)
          13. f8(A,B,C) -> f8(1 + A,B,0)     [B >= 1 + A && 0 >= C && B >= 1 + A] (?,3)
          14. f8(A,B,C) -> f8(A,B,0)         [B >= 1 + A && C >= 1 && B >= A]     (?,3)
        Signature:
          {(f0,3);(f16,3);(f20,3);(f4,3);(f8,3)}
        Flow Graph:
          [4->{4,5,13,14},5->{4,5,13,14},8->{4,5,13},13->{4,5,13},14->{4,5,13}]
        Sizebounds:
          (< 4,0,A>, B) (< 4,0,B>, B) (< 4,0,C>, 2*B) 
          (< 5,0,A>, B) (< 5,0,B>, B) (< 5,0,C>, 2*B) 
          (< 8,0,A>, 1) (< 8,0,B>, B) (< 8,0,C>,   0) 
          (<13,0,A>, B) (<13,0,B>, B) (<13,0,C>,   0) 
          (<14,0,A>, B) (<14,0,B>, B) (<14,0,C>,   0) 
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
          p(f0) = x2        
          p(f8) = -1*x1 + x2
        
        The following rules are strictly oriented:
                  [B >= 1 + A && 0 >= 1 + E] ==>                  
                                   f8(A,B,C)   = -1*A + B         
                                               > -1 + -1*A + B    
                                               = f8(1 + A,B,1 + C)
        
                      [B >= 1 + A && E >= 1] ==>                  
                                   f8(A,B,C)   = -1*A + B         
                                               > -1 + -1*A + B    
                                               = f8(1 + A,B,1 + C)
        
                                    [B >= 1] ==>                  
                                   f0(A,B,C)   = B                
                                               > -1 + B           
                                               = f8(1,B,0)        
        
        [B >= 1 + A && 0 >= C && B >= 1 + A] ==>                  
                                   f8(A,B,C)   = -1*A + B         
                                               > -1 + -1*A + B    
                                               = f8(1 + A,B,0)    
        
        
        The following rules are weakly oriented:
        [B >= 1 + A && C >= 1 && B >= A] ==>          
                               f8(A,B,C)   = -1*A + B 
                                          >= -1*A + B 
                                           = f8(A,B,0)
        
        
* Step 22: PolyRank WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          4.  f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && 0 >= 1 + E]           (B,1)
          5.  f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && E >= 1]               (B,1)
          8.  f0(A,B,C) -> f8(1,B,0)         [B >= 1]                             (1,2)
          13. f8(A,B,C) -> f8(1 + A,B,0)     [B >= 1 + A && 0 >= C && B >= 1 + A] (B,3)
          14. f8(A,B,C) -> f8(A,B,0)         [B >= 1 + A && C >= 1 && B >= A]     (?,3)
        Signature:
          {(f0,3);(f16,3);(f20,3);(f4,3);(f8,3)}
        Flow Graph:
          [4->{4,5,13,14},5->{4,5,13,14},8->{4,5,13},13->{4,5,13},14->{4,5,13}]
        Sizebounds:
          (< 4,0,A>, B) (< 4,0,B>, B) (< 4,0,C>, 2*B) 
          (< 5,0,A>, B) (< 5,0,B>, B) (< 5,0,C>, 2*B) 
          (< 8,0,A>, 1) (< 8,0,B>, B) (< 8,0,C>,   0) 
          (<13,0,A>, B) (<13,0,B>, B) (<13,0,C>,   0) 
          (<14,0,A>, B) (<14,0,B>, B) (<14,0,C>,   0) 
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [4,5,14], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
          p(f8) = -1*x1 + x2 + x3
        
        The following rules are strictly oriented:
        [B >= 1 + A && C >= 1 && B >= A] ==>             
                               f8(A,B,C)   = -1*A + B + C
                                           > -1*A + B    
                                           = f8(A,B,0)   
        
        
        The following rules are weakly oriented:
        [B >= 1 + A && 0 >= 1 + E] ==>                  
                         f8(A,B,C)   = -1*A + B + C     
                                    >= -1*A + B + C     
                                     = f8(1 + A,B,1 + C)
        
            [B >= 1 + A && E >= 1] ==>                  
                         f8(A,B,C)   = -1*A + B + C     
                                    >= -1*A + B + C     
                                     = f8(1 + A,B,1 + C)
        
        We use the following global sizebounds:
        (< 4,0,A>, B) (< 4,0,B>, B) (< 4,0,C>, 2*B) 
        (< 5,0,A>, B) (< 5,0,B>, B) (< 5,0,C>, 2*B) 
        (< 8,0,A>, 1) (< 8,0,B>, B) (< 8,0,C>,   0) 
        (<13,0,A>, B) (<13,0,B>, B) (<13,0,C>,   0) 
        (<14,0,A>, B) (<14,0,B>, B) (<14,0,C>,   0) 
* Step 23: KnowledgePropagation WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          4.  f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && 0 >= 1 + E]           (B,1)            
          5.  f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && E >= 1]               (B,1)            
          8.  f0(A,B,C) -> f8(1,B,0)         [B >= 1]                             (1,2)            
          13. f8(A,B,C) -> f8(1 + A,B,0)     [B >= 1 + A && 0 >= C && B >= 1 + A] (B,3)            
          14. f8(A,B,C) -> f8(A,B,0)         [B >= 1 + A && C >= 1 && B >= A]     (1 + B + 2*B^2,3)
        Signature:
          {(f0,3);(f16,3);(f20,3);(f4,3);(f8,3)}
        Flow Graph:
          [4->{4,5,13,14},5->{4,5,13,14},8->{4,5,13},13->{4,5,13},14->{4,5,13}]
        Sizebounds:
          (< 4,0,A>, B) (< 4,0,B>, B) (< 4,0,C>, 2*B) 
          (< 5,0,A>, B) (< 5,0,B>, B) (< 5,0,C>, 2*B) 
          (< 8,0,A>, 1) (< 8,0,B>, B) (< 8,0,C>,   0) 
          (<13,0,A>, B) (<13,0,B>, B) (<13,0,C>,   0) 
          (<14,0,A>, B) (<14,0,B>, B) (<14,0,C>,   0) 
    + Applied Processor:
        KnowledgePropagation
    + Details:
        The problem is already solved.

WORST_CASE(?,O(n^2))