WORST_CASE(?,O(1))
* Step 1: RestrictVarsProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        Rules:
          0.  f0(A,B,C)  -> f8(0,B,C)      True                   (1,1)
          1.  f8(A,B,C)  -> f14(A,A,C)     [0 >= A && 0 >= D]     (?,1)
          2.  f8(A,B,C)  -> f14(A,A,C)     [0 >= A]               (?,1)
          3.  f23(A,B,C) -> f28(A,B,D)     [0 >= A && 0 >= 1 + E] (?,1)
          4.  f23(A,B,C) -> f28(A,B,D)     [0 >= A]               (?,1)
          5.  f23(A,B,C) -> f23(1 + A,B,C) [0 >= A]               (?,1)
          6.  f28(A,B,C) -> f23(1 + A,B,C) True                   (?,1)
          7.  f28(A,B,C) -> f23(1 + A,B,C) [0 >= 1 + D]           (?,1)
          8.  f23(A,B,C) -> f38(A,B,C)     [A >= 1]               (?,1)
          9.  f8(A,B,C)  -> f8(1 + A,A,C)  [0 >= A]               (?,1)
          10. f14(A,B,C) -> f8(1 + A,B,C)  True                   (?,1)
          11. f14(A,B,C) -> f8(1 + A,B,C)  [0 >= 1 + D]           (?,1)
          12. f8(A,B,C)  -> f23(0,B,C)     [A >= 1]               (?,1)
        Signature:
          {(f0,3);(f14,3);(f23,3);(f28,3);(f38,3);(f8,3)}
        Flow Graph:
          [0->{1,2,9,12},1->{10,11},2->{10,11},3->{6,7},4->{6,7},5->{3,4,5,8},6->{3,4,5,8},7->{3,4,5,8},8->{},9->{1
          ,2,9,12},10->{1,2,9,12},11->{1,2,9,12},12->{3,4,5,8}]
        
    + Applied Processor:
        RestrictVarsProcessor
    + Details:
        We removed the arguments [B,C] .
* Step 2: LocalSizeboundsProc WORST_CASE(?,O(1))
    + Considered Problem:
        Rules:
          0.  f0(A)  -> f8(0)      True                   (1,1)
          1.  f8(A)  -> f14(A)     [0 >= A && 0 >= D]     (?,1)
          2.  f8(A)  -> f14(A)     [0 >= A]               (?,1)
          3.  f23(A) -> f28(A)     [0 >= A && 0 >= 1 + E] (?,1)
          4.  f23(A) -> f28(A)     [0 >= A]               (?,1)
          5.  f23(A) -> f23(1 + A) [0 >= A]               (?,1)
          6.  f28(A) -> f23(1 + A) True                   (?,1)
          7.  f28(A) -> f23(1 + A) [0 >= 1 + D]           (?,1)
          8.  f23(A) -> f38(A)     [A >= 1]               (?,1)
          9.  f8(A)  -> f8(1 + A)  [0 >= A]               (?,1)
          10. f14(A) -> f8(1 + A)  True                   (?,1)
          11. f14(A) -> f8(1 + A)  [0 >= 1 + D]           (?,1)
          12. f8(A)  -> f23(0)     [A >= 1]               (?,1)
        Signature:
          {(f0,1);(f14,1);(f23,1);(f28,1);(f38,1);(f8,1)}
        Flow Graph:
          [0->{1,2,9,12},1->{10,11},2->{10,11},3->{6,7},4->{6,7},5->{3,4,5,8},6->{3,4,5,8},7->{3,4,5,8},8->{},9->{1
          ,2,9,12},10->{1,2,9,12},11->{1,2,9,12},12->{3,4,5,8}]
        
    + Applied Processor:
        LocalSizeboundsProc
    + Details:
        LocalSizebounds generated; rvgraph
          (< 0,0,A>,     0, .= 0) 
          (< 1,0,A>,     A, .= 0) 
          (< 2,0,A>,     A, .= 0) 
          (< 3,0,A>,     A, .= 0) 
          (< 4,0,A>,     A, .= 0) 
          (< 5,0,A>, 1 + A, .+ 1) 
          (< 6,0,A>, 1 + A, .+ 1) 
          (< 7,0,A>, 1 + A, .+ 1) 
          (< 8,0,A>,     A, .= 0) 
          (< 9,0,A>, 1 + A, .+ 1) 
          (<10,0,A>, 1 + A, .+ 1) 
          (<11,0,A>, 1 + A, .+ 1) 
          (<12,0,A>,     0, .= 0) 
* Step 3: SizeboundsProc WORST_CASE(?,O(1))
    + Considered Problem:
        Rules:
          0.  f0(A)  -> f8(0)      True                   (1,1)
          1.  f8(A)  -> f14(A)     [0 >= A && 0 >= D]     (?,1)
          2.  f8(A)  -> f14(A)     [0 >= A]               (?,1)
          3.  f23(A) -> f28(A)     [0 >= A && 0 >= 1 + E] (?,1)
          4.  f23(A) -> f28(A)     [0 >= A]               (?,1)
          5.  f23(A) -> f23(1 + A) [0 >= A]               (?,1)
          6.  f28(A) -> f23(1 + A) True                   (?,1)
          7.  f28(A) -> f23(1 + A) [0 >= 1 + D]           (?,1)
          8.  f23(A) -> f38(A)     [A >= 1]               (?,1)
          9.  f8(A)  -> f8(1 + A)  [0 >= A]               (?,1)
          10. f14(A) -> f8(1 + A)  True                   (?,1)
          11. f14(A) -> f8(1 + A)  [0 >= 1 + D]           (?,1)
          12. f8(A)  -> f23(0)     [A >= 1]               (?,1)
        Signature:
          {(f0,1);(f14,1);(f23,1);(f28,1);(f38,1);(f8,1)}
        Flow Graph:
          [0->{1,2,9,12},1->{10,11},2->{10,11},3->{6,7},4->{6,7},5->{3,4,5,8},6->{3,4,5,8},7->{3,4,5,8},8->{},9->{1
          ,2,9,12},10->{1,2,9,12},11->{1,2,9,12},12->{3,4,5,8}]
        Sizebounds:
          (< 0,0,A>, ?) 
          (< 1,0,A>, ?) 
          (< 2,0,A>, ?) 
          (< 3,0,A>, ?) 
          (< 4,0,A>, ?) 
          (< 5,0,A>, ?) 
          (< 6,0,A>, ?) 
          (< 7,0,A>, ?) 
          (< 8,0,A>, ?) 
          (< 9,0,A>, ?) 
          (<10,0,A>, ?) 
          (<11,0,A>, ?) 
          (<12,0,A>, ?) 
    + Applied Processor:
        SizeboundsProc
    + Details:
        Sizebounds computed:
          (< 0,0,A>, 0) 
          (< 1,0,A>, 0) 
          (< 2,0,A>, 0) 
          (< 3,0,A>, 0) 
          (< 4,0,A>, 0) 
          (< 5,0,A>, 1) 
          (< 6,0,A>, 0) 
          (< 7,0,A>, 0) 
          (< 8,0,A>, 1) 
          (< 9,0,A>, 1) 
          (<10,0,A>, 0) 
          (<11,0,A>, 0) 
          (<12,0,A>, 0) 
* Step 4: UnsatPaths WORST_CASE(?,O(1))
    + Considered Problem:
        Rules:
          0.  f0(A)  -> f8(0)      True                   (1,1)
          1.  f8(A)  -> f14(A)     [0 >= A && 0 >= D]     (?,1)
          2.  f8(A)  -> f14(A)     [0 >= A]               (?,1)
          3.  f23(A) -> f28(A)     [0 >= A && 0 >= 1 + E] (?,1)
          4.  f23(A) -> f28(A)     [0 >= A]               (?,1)
          5.  f23(A) -> f23(1 + A) [0 >= A]               (?,1)
          6.  f28(A) -> f23(1 + A) True                   (?,1)
          7.  f28(A) -> f23(1 + A) [0 >= 1 + D]           (?,1)
          8.  f23(A) -> f38(A)     [A >= 1]               (?,1)
          9.  f8(A)  -> f8(1 + A)  [0 >= A]               (?,1)
          10. f14(A) -> f8(1 + A)  True                   (?,1)
          11. f14(A) -> f8(1 + A)  [0 >= 1 + D]           (?,1)
          12. f8(A)  -> f23(0)     [A >= 1]               (?,1)
        Signature:
          {(f0,1);(f14,1);(f23,1);(f28,1);(f38,1);(f8,1)}
        Flow Graph:
          [0->{1,2,9,12},1->{10,11},2->{10,11},3->{6,7},4->{6,7},5->{3,4,5,8},6->{3,4,5,8},7->{3,4,5,8},8->{},9->{1
          ,2,9,12},10->{1,2,9,12},11->{1,2,9,12},12->{3,4,5,8}]
        Sizebounds:
          (< 0,0,A>, 0) 
          (< 1,0,A>, 0) 
          (< 2,0,A>, 0) 
          (< 3,0,A>, 0) 
          (< 4,0,A>, 0) 
          (< 5,0,A>, 1) 
          (< 6,0,A>, 0) 
          (< 7,0,A>, 0) 
          (< 8,0,A>, 1) 
          (< 9,0,A>, 1) 
          (<10,0,A>, 0) 
          (<11,0,A>, 0) 
          (<12,0,A>, 0) 
    + Applied Processor:
        UnsatPaths
    + Details:
        We remove following edges from the transition graph: [(0,12),(12,8)]
* Step 5: LeafRules WORST_CASE(?,O(1))
    + Considered Problem:
        Rules:
          0.  f0(A)  -> f8(0)      True                   (1,1)
          1.  f8(A)  -> f14(A)     [0 >= A && 0 >= D]     (?,1)
          2.  f8(A)  -> f14(A)     [0 >= A]               (?,1)
          3.  f23(A) -> f28(A)     [0 >= A && 0 >= 1 + E] (?,1)
          4.  f23(A) -> f28(A)     [0 >= A]               (?,1)
          5.  f23(A) -> f23(1 + A) [0 >= A]               (?,1)
          6.  f28(A) -> f23(1 + A) True                   (?,1)
          7.  f28(A) -> f23(1 + A) [0 >= 1 + D]           (?,1)
          8.  f23(A) -> f38(A)     [A >= 1]               (?,1)
          9.  f8(A)  -> f8(1 + A)  [0 >= A]               (?,1)
          10. f14(A) -> f8(1 + A)  True                   (?,1)
          11. f14(A) -> f8(1 + A)  [0 >= 1 + D]           (?,1)
          12. f8(A)  -> f23(0)     [A >= 1]               (?,1)
        Signature:
          {(f0,1);(f14,1);(f23,1);(f28,1);(f38,1);(f8,1)}
        Flow Graph:
          [0->{1,2,9},1->{10,11},2->{10,11},3->{6,7},4->{6,7},5->{3,4,5,8},6->{3,4,5,8},7->{3,4,5,8},8->{},9->{1,2,9
          ,12},10->{1,2,9,12},11->{1,2,9,12},12->{3,4,5}]
        Sizebounds:
          (< 0,0,A>, 0) 
          (< 1,0,A>, 0) 
          (< 2,0,A>, 0) 
          (< 3,0,A>, 0) 
          (< 4,0,A>, 0) 
          (< 5,0,A>, 1) 
          (< 6,0,A>, 0) 
          (< 7,0,A>, 0) 
          (< 8,0,A>, 1) 
          (< 9,0,A>, 1) 
          (<10,0,A>, 0) 
          (<11,0,A>, 0) 
          (<12,0,A>, 0) 
    + Applied Processor:
        LeafRules
    + Details:
        The following transitions are estimated by its predecessors and are removed [8]
* Step 6: PolyRank WORST_CASE(?,O(1))
    + Considered Problem:
        Rules:
          0.  f0(A)  -> f8(0)      True                   (1,1)
          1.  f8(A)  -> f14(A)     [0 >= A && 0 >= D]     (?,1)
          2.  f8(A)  -> f14(A)     [0 >= A]               (?,1)
          3.  f23(A) -> f28(A)     [0 >= A && 0 >= 1 + E] (?,1)
          4.  f23(A) -> f28(A)     [0 >= A]               (?,1)
          5.  f23(A) -> f23(1 + A) [0 >= A]               (?,1)
          6.  f28(A) -> f23(1 + A) True                   (?,1)
          7.  f28(A) -> f23(1 + A) [0 >= 1 + D]           (?,1)
          9.  f8(A)  -> f8(1 + A)  [0 >= A]               (?,1)
          10. f14(A) -> f8(1 + A)  True                   (?,1)
          11. f14(A) -> f8(1 + A)  [0 >= 1 + D]           (?,1)
          12. f8(A)  -> f23(0)     [A >= 1]               (?,1)
        Signature:
          {(f0,1);(f14,1);(f23,1);(f28,1);(f38,1);(f8,1)}
        Flow Graph:
          [0->{1,2,9},1->{10,11},2->{10,11},3->{6,7},4->{6,7},5->{3,4,5},6->{3,4,5},7->{3,4,5},9->{1,2,9,12},10->{1
          ,2,9,12},11->{1,2,9,12},12->{3,4,5}]
        Sizebounds:
          (< 0,0,A>, 0) 
          (< 1,0,A>, 0) 
          (< 2,0,A>, 0) 
          (< 3,0,A>, 0) 
          (< 4,0,A>, 0) 
          (< 5,0,A>, 1) 
          (< 6,0,A>, 0) 
          (< 7,0,A>, 0) 
          (< 9,0,A>, 1) 
          (<10,0,A>, 0) 
          (<11,0,A>, 0) 
          (<12,0,A>, 0) 
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
           p(f0) = 1
          p(f14) = 1
          p(f23) = 0
          p(f28) = 0
           p(f8) = 1
        
        The following rules are strictly oriented:
        [A >= 1] ==>       
           f8(A)   = 1     
                   > 0     
                   = f23(0)
        
        
        The following rules are weakly oriented:
                          True ==>           
                         f0(A)   = 1         
                                >= 1         
                                 = f8(0)     
        
            [0 >= A && 0 >= D] ==>           
                         f8(A)   = 1         
                                >= 1         
                                 = f14(A)    
        
                      [0 >= A] ==>           
                         f8(A)   = 1         
                                >= 1         
                                 = f14(A)    
        
        [0 >= A && 0 >= 1 + E] ==>           
                        f23(A)   = 0         
                                >= 0         
                                 = f28(A)    
        
                      [0 >= A] ==>           
                        f23(A)   = 0         
                                >= 0         
                                 = f28(A)    
        
                      [0 >= A] ==>           
                        f23(A)   = 0         
                                >= 0         
                                 = f23(1 + A)
        
                          True ==>           
                        f28(A)   = 0         
                                >= 0         
                                 = f23(1 + A)
        
                  [0 >= 1 + D] ==>           
                        f28(A)   = 0         
                                >= 0         
                                 = f23(1 + A)
        
                      [0 >= A] ==>           
                         f8(A)   = 1         
                                >= 1         
                                 = f8(1 + A) 
        
                          True ==>           
                        f14(A)   = 1         
                                >= 1         
                                 = f8(1 + A) 
        
                  [0 >= 1 + D] ==>           
                        f14(A)   = 1         
                                >= 1         
                                 = f8(1 + A) 
        
        
* Step 7: PolyRank WORST_CASE(?,O(1))
    + Considered Problem:
        Rules:
          0.  f0(A)  -> f8(0)      True                   (1,1)
          1.  f8(A)  -> f14(A)     [0 >= A && 0 >= D]     (?,1)
          2.  f8(A)  -> f14(A)     [0 >= A]               (?,1)
          3.  f23(A) -> f28(A)     [0 >= A && 0 >= 1 + E] (?,1)
          4.  f23(A) -> f28(A)     [0 >= A]               (?,1)
          5.  f23(A) -> f23(1 + A) [0 >= A]               (?,1)
          6.  f28(A) -> f23(1 + A) True                   (?,1)
          7.  f28(A) -> f23(1 + A) [0 >= 1 + D]           (?,1)
          9.  f8(A)  -> f8(1 + A)  [0 >= A]               (?,1)
          10. f14(A) -> f8(1 + A)  True                   (?,1)
          11. f14(A) -> f8(1 + A)  [0 >= 1 + D]           (?,1)
          12. f8(A)  -> f23(0)     [A >= 1]               (1,1)
        Signature:
          {(f0,1);(f14,1);(f23,1);(f28,1);(f38,1);(f8,1)}
        Flow Graph:
          [0->{1,2,9},1->{10,11},2->{10,11},3->{6,7},4->{6,7},5->{3,4,5},6->{3,4,5},7->{3,4,5},9->{1,2,9,12},10->{1
          ,2,9,12},11->{1,2,9,12},12->{3,4,5}]
        Sizebounds:
          (< 0,0,A>, 0) 
          (< 1,0,A>, 0) 
          (< 2,0,A>, 0) 
          (< 3,0,A>, 0) 
          (< 4,0,A>, 0) 
          (< 5,0,A>, 1) 
          (< 6,0,A>, 0) 
          (< 7,0,A>, 0) 
          (< 9,0,A>, 1) 
          (<10,0,A>, 0) 
          (<11,0,A>, 0) 
          (<12,0,A>, 0) 
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
           p(f0) = 2        
          p(f14) = 2        
          p(f23) = 2 + -1*x1
          p(f28) = 1 + -1*x1
           p(f8) = 2        
        
        The following rules are strictly oriented:
        [0 >= A] ==>           
          f23(A)   = 2 + -1*A  
                   > 1 + -1*A  
                   = f28(A)    
        
        [0 >= A] ==>           
          f23(A)   = 2 + -1*A  
                   > 1 + -1*A  
                   = f23(1 + A)
        
        
        The following rules are weakly oriented:
                          True ==>           
                         f0(A)   = 2         
                                >= 2         
                                 = f8(0)     
        
            [0 >= A && 0 >= D] ==>           
                         f8(A)   = 2         
                                >= 2         
                                 = f14(A)    
        
                      [0 >= A] ==>           
                         f8(A)   = 2         
                                >= 2         
                                 = f14(A)    
        
        [0 >= A && 0 >= 1 + E] ==>           
                        f23(A)   = 2 + -1*A  
                                >= 1 + -1*A  
                                 = f28(A)    
        
                          True ==>           
                        f28(A)   = 1 + -1*A  
                                >= 1 + -1*A  
                                 = f23(1 + A)
        
                  [0 >= 1 + D] ==>           
                        f28(A)   = 1 + -1*A  
                                >= 1 + -1*A  
                                 = f23(1 + A)
        
                      [0 >= A] ==>           
                         f8(A)   = 2         
                                >= 2         
                                 = f8(1 + A) 
        
                          True ==>           
                        f14(A)   = 2         
                                >= 2         
                                 = f8(1 + A) 
        
                  [0 >= 1 + D] ==>           
                        f14(A)   = 2         
                                >= 2         
                                 = f8(1 + A) 
        
                      [A >= 1] ==>           
                         f8(A)   = 2         
                                >= 2         
                                 = f23(0)    
        
        
* Step 8: PolyRank WORST_CASE(?,O(1))
    + Considered Problem:
        Rules:
          0.  f0(A)  -> f8(0)      True                   (1,1)
          1.  f8(A)  -> f14(A)     [0 >= A && 0 >= D]     (?,1)
          2.  f8(A)  -> f14(A)     [0 >= A]               (?,1)
          3.  f23(A) -> f28(A)     [0 >= A && 0 >= 1 + E] (?,1)
          4.  f23(A) -> f28(A)     [0 >= A]               (2,1)
          5.  f23(A) -> f23(1 + A) [0 >= A]               (2,1)
          6.  f28(A) -> f23(1 + A) True                   (?,1)
          7.  f28(A) -> f23(1 + A) [0 >= 1 + D]           (?,1)
          9.  f8(A)  -> f8(1 + A)  [0 >= A]               (?,1)
          10. f14(A) -> f8(1 + A)  True                   (?,1)
          11. f14(A) -> f8(1 + A)  [0 >= 1 + D]           (?,1)
          12. f8(A)  -> f23(0)     [A >= 1]               (1,1)
        Signature:
          {(f0,1);(f14,1);(f23,1);(f28,1);(f38,1);(f8,1)}
        Flow Graph:
          [0->{1,2,9},1->{10,11},2->{10,11},3->{6,7},4->{6,7},5->{3,4,5},6->{3,4,5},7->{3,4,5},9->{1,2,9,12},10->{1
          ,2,9,12},11->{1,2,9,12},12->{3,4,5}]
        Sizebounds:
          (< 0,0,A>, 0) 
          (< 1,0,A>, 0) 
          (< 2,0,A>, 0) 
          (< 3,0,A>, 0) 
          (< 4,0,A>, 0) 
          (< 5,0,A>, 1) 
          (< 6,0,A>, 0) 
          (< 7,0,A>, 0) 
          (< 9,0,A>, 1) 
          (<10,0,A>, 0) 
          (<11,0,A>, 0) 
          (<12,0,A>, 0) 
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
           p(f0) = 1        
          p(f14) = 1        
          p(f23) = 1 + -1*x1
          p(f28) = -1*x1    
           p(f8) = 1        
        
        The following rules are strictly oriented:
        [0 >= A && 0 >= 1 + E] ==>           
                        f23(A)   = 1 + -1*A  
                                 > -1*A      
                                 = f28(A)    
        
                      [0 >= A] ==>           
                        f23(A)   = 1 + -1*A  
                                 > -1*A      
                                 = f28(A)    
        
                      [0 >= A] ==>           
                        f23(A)   = 1 + -1*A  
                                 > -1*A      
                                 = f23(1 + A)
        
        
        The following rules are weakly oriented:
                      True ==>           
                     f0(A)   = 1         
                            >= 1         
                             = f8(0)     
        
        [0 >= A && 0 >= D] ==>           
                     f8(A)   = 1         
                            >= 1         
                             = f14(A)    
        
                  [0 >= A] ==>           
                     f8(A)   = 1         
                            >= 1         
                             = f14(A)    
        
                      True ==>           
                    f28(A)   = -1*A      
                            >= -1*A      
                             = f23(1 + A)
        
              [0 >= 1 + D] ==>           
                    f28(A)   = -1*A      
                            >= -1*A      
                             = f23(1 + A)
        
                  [0 >= A] ==>           
                     f8(A)   = 1         
                            >= 1         
                             = f8(1 + A) 
        
                      True ==>           
                    f14(A)   = 1         
                            >= 1         
                             = f8(1 + A) 
        
              [0 >= 1 + D] ==>           
                    f14(A)   = 1         
                            >= 1         
                             = f8(1 + A) 
        
                  [A >= 1] ==>           
                     f8(A)   = 1         
                            >= 1         
                             = f23(0)    
        
        
* Step 9: KnowledgePropagation WORST_CASE(?,O(1))
    + Considered Problem:
        Rules:
          0.  f0(A)  -> f8(0)      True                   (1,1)
          1.  f8(A)  -> f14(A)     [0 >= A && 0 >= D]     (?,1)
          2.  f8(A)  -> f14(A)     [0 >= A]               (?,1)
          3.  f23(A) -> f28(A)     [0 >= A && 0 >= 1 + E] (1,1)
          4.  f23(A) -> f28(A)     [0 >= A]               (1,1)
          5.  f23(A) -> f23(1 + A) [0 >= A]               (1,1)
          6.  f28(A) -> f23(1 + A) True                   (?,1)
          7.  f28(A) -> f23(1 + A) [0 >= 1 + D]           (?,1)
          9.  f8(A)  -> f8(1 + A)  [0 >= A]               (?,1)
          10. f14(A) -> f8(1 + A)  True                   (?,1)
          11. f14(A) -> f8(1 + A)  [0 >= 1 + D]           (?,1)
          12. f8(A)  -> f23(0)     [A >= 1]               (1,1)
        Signature:
          {(f0,1);(f14,1);(f23,1);(f28,1);(f38,1);(f8,1)}
        Flow Graph:
          [0->{1,2,9},1->{10,11},2->{10,11},3->{6,7},4->{6,7},5->{3,4,5},6->{3,4,5},7->{3,4,5},9->{1,2,9,12},10->{1
          ,2,9,12},11->{1,2,9,12},12->{3,4,5}]
        Sizebounds:
          (< 0,0,A>, 0) 
          (< 1,0,A>, 0) 
          (< 2,0,A>, 0) 
          (< 3,0,A>, 0) 
          (< 4,0,A>, 0) 
          (< 5,0,A>, 1) 
          (< 6,0,A>, 0) 
          (< 7,0,A>, 0) 
          (< 9,0,A>, 1) 
          (<10,0,A>, 0) 
          (<11,0,A>, 0) 
          (<12,0,A>, 0) 
    + Applied Processor:
        KnowledgePropagation
    + Details:
        We propagate bounds from predecessors.
* Step 10: PolyRank WORST_CASE(?,O(1))
    + Considered Problem:
        Rules:
          0.  f0(A)  -> f8(0)      True                   (1,1)
          1.  f8(A)  -> f14(A)     [0 >= A && 0 >= D]     (?,1)
          2.  f8(A)  -> f14(A)     [0 >= A]               (?,1)
          3.  f23(A) -> f28(A)     [0 >= A && 0 >= 1 + E] (1,1)
          4.  f23(A) -> f28(A)     [0 >= A]               (1,1)
          5.  f23(A) -> f23(1 + A) [0 >= A]               (1,1)
          6.  f28(A) -> f23(1 + A) True                   (2,1)
          7.  f28(A) -> f23(1 + A) [0 >= 1 + D]           (2,1)
          9.  f8(A)  -> f8(1 + A)  [0 >= A]               (?,1)
          10. f14(A) -> f8(1 + A)  True                   (?,1)
          11. f14(A) -> f8(1 + A)  [0 >= 1 + D]           (?,1)
          12. f8(A)  -> f23(0)     [A >= 1]               (1,1)
        Signature:
          {(f0,1);(f14,1);(f23,1);(f28,1);(f38,1);(f8,1)}
        Flow Graph:
          [0->{1,2,9},1->{10,11},2->{10,11},3->{6,7},4->{6,7},5->{3,4,5},6->{3,4,5},7->{3,4,5},9->{1,2,9,12},10->{1
          ,2,9,12},11->{1,2,9,12},12->{3,4,5}]
        Sizebounds:
          (< 0,0,A>, 0) 
          (< 1,0,A>, 0) 
          (< 2,0,A>, 0) 
          (< 3,0,A>, 0) 
          (< 4,0,A>, 0) 
          (< 5,0,A>, 1) 
          (< 6,0,A>, 0) 
          (< 7,0,A>, 0) 
          (< 9,0,A>, 1) 
          (<10,0,A>, 0) 
          (<11,0,A>, 0) 
          (<12,0,A>, 0) 
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [1,9,10,2,11], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
          p(f14) = 1 + -1*x1
           p(f8) = 2 + -1*x1
        
        The following rules are strictly oriented:
        [0 >= A] ==>          
           f8(A)   = 2 + -1*A 
                   > 1 + -1*A 
                   = f14(A)   
        
        [0 >= A] ==>          
           f8(A)   = 2 + -1*A 
                   > 1 + -1*A 
                   = f8(1 + A)
        
        
        The following rules are weakly oriented:
        [0 >= A && 0 >= D] ==>          
                     f8(A)   = 2 + -1*A 
                            >= 1 + -1*A 
                             = f14(A)   
        
                      True ==>          
                    f14(A)   = 1 + -1*A 
                            >= 1 + -1*A 
                             = f8(1 + A)
        
              [0 >= 1 + D] ==>          
                    f14(A)   = 1 + -1*A 
                            >= 1 + -1*A 
                             = f8(1 + A)
        
        We use the following global sizebounds:
        (< 0,0,A>, 0) 
        (< 1,0,A>, 0) 
        (< 2,0,A>, 0) 
        (< 3,0,A>, 0) 
        (< 4,0,A>, 0) 
        (< 5,0,A>, 1) 
        (< 6,0,A>, 0) 
        (< 7,0,A>, 0) 
        (< 9,0,A>, 1) 
        (<10,0,A>, 0) 
        (<11,0,A>, 0) 
        (<12,0,A>, 0) 
* Step 11: PolyRank WORST_CASE(?,O(1))
    + Considered Problem:
        Rules:
          0.  f0(A)  -> f8(0)      True                   (1,1)
          1.  f8(A)  -> f14(A)     [0 >= A && 0 >= D]     (?,1)
          2.  f8(A)  -> f14(A)     [0 >= A]               (2,1)
          3.  f23(A) -> f28(A)     [0 >= A && 0 >= 1 + E] (1,1)
          4.  f23(A) -> f28(A)     [0 >= A]               (1,1)
          5.  f23(A) -> f23(1 + A) [0 >= A]               (1,1)
          6.  f28(A) -> f23(1 + A) True                   (2,1)
          7.  f28(A) -> f23(1 + A) [0 >= 1 + D]           (2,1)
          9.  f8(A)  -> f8(1 + A)  [0 >= A]               (2,1)
          10. f14(A) -> f8(1 + A)  True                   (?,1)
          11. f14(A) -> f8(1 + A)  [0 >= 1 + D]           (?,1)
          12. f8(A)  -> f23(0)     [A >= 1]               (1,1)
        Signature:
          {(f0,1);(f14,1);(f23,1);(f28,1);(f38,1);(f8,1)}
        Flow Graph:
          [0->{1,2,9},1->{10,11},2->{10,11},3->{6,7},4->{6,7},5->{3,4,5},6->{3,4,5},7->{3,4,5},9->{1,2,9,12},10->{1
          ,2,9,12},11->{1,2,9,12},12->{3,4,5}]
        Sizebounds:
          (< 0,0,A>, 0) 
          (< 1,0,A>, 0) 
          (< 2,0,A>, 0) 
          (< 3,0,A>, 0) 
          (< 4,0,A>, 0) 
          (< 5,0,A>, 1) 
          (< 6,0,A>, 0) 
          (< 7,0,A>, 0) 
          (< 9,0,A>, 1) 
          (<10,0,A>, 0) 
          (<11,0,A>, 0) 
          (<12,0,A>, 0) 
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [1,10,2,11], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
          p(f14) = 1 + -1*x1
           p(f8) = 2 + -1*x1
        
        The following rules are strictly oriented:
        [0 >= A && 0 >= D] ==>         
                     f8(A)   = 2 + -1*A
                             > 1 + -1*A
                             = f14(A)  
        
                  [0 >= A] ==>         
                     f8(A)   = 2 + -1*A
                             > 1 + -1*A
                             = f14(A)  
        
        
        The following rules are weakly oriented:
                True ==>          
              f14(A)   = 1 + -1*A 
                      >= 1 + -1*A 
                       = f8(1 + A)
        
        [0 >= 1 + D] ==>          
              f14(A)   = 1 + -1*A 
                      >= 1 + -1*A 
                       = f8(1 + A)
        
        We use the following global sizebounds:
        (< 0,0,A>, 0) 
        (< 1,0,A>, 0) 
        (< 2,0,A>, 0) 
        (< 3,0,A>, 0) 
        (< 4,0,A>, 0) 
        (< 5,0,A>, 1) 
        (< 6,0,A>, 0) 
        (< 7,0,A>, 0) 
        (< 9,0,A>, 1) 
        (<10,0,A>, 0) 
        (<11,0,A>, 0) 
        (<12,0,A>, 0) 
* Step 12: KnowledgePropagation WORST_CASE(?,O(1))
    + Considered Problem:
        Rules:
          0.  f0(A)  -> f8(0)      True                   (1,1)
          1.  f8(A)  -> f14(A)     [0 >= A && 0 >= D]     (8,1)
          2.  f8(A)  -> f14(A)     [0 >= A]               (2,1)
          3.  f23(A) -> f28(A)     [0 >= A && 0 >= 1 + E] (1,1)
          4.  f23(A) -> f28(A)     [0 >= A]               (1,1)
          5.  f23(A) -> f23(1 + A) [0 >= A]               (1,1)
          6.  f28(A) -> f23(1 + A) True                   (2,1)
          7.  f28(A) -> f23(1 + A) [0 >= 1 + D]           (2,1)
          9.  f8(A)  -> f8(1 + A)  [0 >= A]               (2,1)
          10. f14(A) -> f8(1 + A)  True                   (?,1)
          11. f14(A) -> f8(1 + A)  [0 >= 1 + D]           (?,1)
          12. f8(A)  -> f23(0)     [A >= 1]               (1,1)
        Signature:
          {(f0,1);(f14,1);(f23,1);(f28,1);(f38,1);(f8,1)}
        Flow Graph:
          [0->{1,2,9},1->{10,11},2->{10,11},3->{6,7},4->{6,7},5->{3,4,5},6->{3,4,5},7->{3,4,5},9->{1,2,9,12},10->{1
          ,2,9,12},11->{1,2,9,12},12->{3,4,5}]
        Sizebounds:
          (< 0,0,A>, 0) 
          (< 1,0,A>, 0) 
          (< 2,0,A>, 0) 
          (< 3,0,A>, 0) 
          (< 4,0,A>, 0) 
          (< 5,0,A>, 1) 
          (< 6,0,A>, 0) 
          (< 7,0,A>, 0) 
          (< 9,0,A>, 1) 
          (<10,0,A>, 0) 
          (<11,0,A>, 0) 
          (<12,0,A>, 0) 
    + Applied Processor:
        KnowledgePropagation
    + Details:
        We propagate bounds from predecessors.
* Step 13: LocalSizeboundsProc WORST_CASE(?,O(1))
    + Considered Problem:
        Rules:
          0.  f0(A)  -> f8(0)      True                   (1,1) 
          1.  f8(A)  -> f14(A)     [0 >= A && 0 >= D]     (8,1) 
          2.  f8(A)  -> f14(A)     [0 >= A]               (2,1) 
          3.  f23(A) -> f28(A)     [0 >= A && 0 >= 1 + E] (1,1) 
          4.  f23(A) -> f28(A)     [0 >= A]               (1,1) 
          5.  f23(A) -> f23(1 + A) [0 >= A]               (1,1) 
          6.  f28(A) -> f23(1 + A) True                   (2,1) 
          7.  f28(A) -> f23(1 + A) [0 >= 1 + D]           (2,1) 
          9.  f8(A)  -> f8(1 + A)  [0 >= A]               (2,1) 
          10. f14(A) -> f8(1 + A)  True                   (10,1)
          11. f14(A) -> f8(1 + A)  [0 >= 1 + D]           (10,1)
          12. f8(A)  -> f23(0)     [A >= 1]               (1,1) 
        Signature:
          {(f0,1);(f14,1);(f23,1);(f28,1);(f38,1);(f8,1)}
        Flow Graph:
          [0->{1,2,9},1->{10,11},2->{10,11},3->{6,7},4->{6,7},5->{3,4,5},6->{3,4,5},7->{3,4,5},9->{1,2,9,12},10->{1
          ,2,9,12},11->{1,2,9,12},12->{3,4,5}]
        Sizebounds:
          (< 0,0,A>, 0) 
          (< 1,0,A>, 0) 
          (< 2,0,A>, 0) 
          (< 3,0,A>, 0) 
          (< 4,0,A>, 0) 
          (< 5,0,A>, 1) 
          (< 6,0,A>, 0) 
          (< 7,0,A>, 0) 
          (< 9,0,A>, 1) 
          (<10,0,A>, 0) 
          (<11,0,A>, 0) 
          (<12,0,A>, 0) 
    + Applied Processor:
        LocalSizeboundsProc
    + Details:
        The problem is already solved.

WORST_CASE(?,O(1))