WORST_CASE(?,O(n^2))
* Step 1: RestrictVarsProcessor WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0. l0(A,B) -> l1(0,B)             True         (1,1)
          1. l1(A,B) -> c2(l2(A,B),l3(A,B)) [B >= 0]     (?,1)
          2. l1(A,B) -> l4(A,B)             [0 >= 1 + B] (?,1)
          3. l2(A,B) -> l1(C,-1 + B)        [B >= 0]     (?,1)
          4. l3(A,B) -> l5(C,B)             True         (?,1)
          5. l5(A,B) -> l6(1,B)             True         (?,1)
          6. l6(A,B) -> c2(l7(A,B),l8(A,B)) [B >= 1]     (?,1)
          7. l6(A,B) -> l9(A,B)             [0 >= B]     (?,1)
          8. l7(A,B) -> l9(C,B)             True         (?,1)
          9. l8(A,B) -> l8(C,-1 + B)        [B >= 1]     (?,1)
        Signature:
          {(l0,2);(l1,2);(l2,2);(l3,2);(l4,2);(l5,2);(l6,2);(l7,2);(l8,2);(l9,2)}
        Flow Graph:
          [0->{1,2},1->{3,4},2->{},3->{1,2},4->{5},5->{6,7},6->{8,9},7->{},8->{},9->{9}]
        
    + Applied Processor:
        RestrictVarsProcessor
    + Details:
        We removed the arguments [A] .
* Step 2: LocalSizeboundsProc WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0. l0(B) -> l1(B)           True         (1,1)
          1. l1(B) -> c2(l2(B),l3(B)) [B >= 0]     (?,1)
          2. l1(B) -> l4(B)           [0 >= 1 + B] (?,1)
          3. l2(B) -> l1(-1 + B)      [B >= 0]     (?,1)
          4. l3(B) -> l5(B)           True         (?,1)
          5. l5(B) -> l6(B)           True         (?,1)
          6. l6(B) -> c2(l7(B),l8(B)) [B >= 1]     (?,1)
          7. l6(B) -> l9(B)           [0 >= B]     (?,1)
          8. l7(B) -> l9(B)           True         (?,1)
          9. l8(B) -> l8(-1 + B)      [B >= 1]     (?,1)
        Signature:
          {(l0,1);(l1,1);(l2,1);(l3,1);(l4,1);(l5,1);(l6,1);(l7,1);(l8,1);(l9,1)}
        Flow Graph:
          [0->{1,2},1->{3,4},2->{},3->{1,2},4->{5},5->{6,7},6->{8,9},7->{},8->{},9->{9}]
        
    + Applied Processor:
        LocalSizeboundsProc
    + Details:
        LocalSizebounds generated; rvgraph
          (<0,0,B>,     B, .= 0) 
          (<1,0,B>,     B, .= 0) 
          (<1,1,B>,     B, .= 0) 
          (<2,0,B>,     B, .= 0) 
          (<3,0,B>, 1 + B, .+ 1) 
          (<4,0,B>,     B, .= 0) 
          (<5,0,B>,     B, .= 0) 
          (<6,0,B>,     B, .= 0) 
          (<6,1,B>,     B, .= 0) 
          (<7,0,B>,     B, .= 0) 
          (<8,0,B>,     B, .= 0) 
          (<9,0,B>, 1 + B, .+ 1) 
* Step 3: SizeboundsProc WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0. l0(B) -> l1(B)           True         (1,1)
          1. l1(B) -> c2(l2(B),l3(B)) [B >= 0]     (?,1)
          2. l1(B) -> l4(B)           [0 >= 1 + B] (?,1)
          3. l2(B) -> l1(-1 + B)      [B >= 0]     (?,1)
          4. l3(B) -> l5(B)           True         (?,1)
          5. l5(B) -> l6(B)           True         (?,1)
          6. l6(B) -> c2(l7(B),l8(B)) [B >= 1]     (?,1)
          7. l6(B) -> l9(B)           [0 >= B]     (?,1)
          8. l7(B) -> l9(B)           True         (?,1)
          9. l8(B) -> l8(-1 + B)      [B >= 1]     (?,1)
        Signature:
          {(l0,1);(l1,1);(l2,1);(l3,1);(l4,1);(l5,1);(l6,1);(l7,1);(l8,1);(l9,1)}
        Flow Graph:
          [0->{1,2},1->{3,4},2->{},3->{1,2},4->{5},5->{6,7},6->{8,9},7->{},8->{},9->{9}]
        Sizebounds:
          (<0,0,B>, ?) 
          (<1,0,B>, ?) 
          (<1,1,B>, ?) 
          (<2,0,B>, ?) 
          (<3,0,B>, ?) 
          (<4,0,B>, ?) 
          (<5,0,B>, ?) 
          (<6,0,B>, ?) 
          (<6,1,B>, ?) 
          (<7,0,B>, ?) 
          (<8,0,B>, ?) 
          (<9,0,B>, ?) 
    + Applied Processor:
        SizeboundsProc
    + Details:
        Sizebounds computed:
          (<0,0,B>, B) 
          (<1,0,B>, ?) 
          (<1,1,B>, ?) 
          (<2,0,B>, ?) 
          (<3,0,B>, ?) 
          (<4,0,B>, ?) 
          (<5,0,B>, ?) 
          (<6,0,B>, ?) 
          (<6,1,B>, ?) 
          (<7,0,B>, ?) 
          (<8,0,B>, ?) 
          (<9,0,B>, ?) 
* Step 4: LeafRules WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0. l0(B) -> l1(B)           True         (1,1)
          1. l1(B) -> c2(l2(B),l3(B)) [B >= 0]     (?,1)
          2. l1(B) -> l4(B)           [0 >= 1 + B] (?,1)
          3. l2(B) -> l1(-1 + B)      [B >= 0]     (?,1)
          4. l3(B) -> l5(B)           True         (?,1)
          5. l5(B) -> l6(B)           True         (?,1)
          6. l6(B) -> c2(l7(B),l8(B)) [B >= 1]     (?,1)
          7. l6(B) -> l9(B)           [0 >= B]     (?,1)
          8. l7(B) -> l9(B)           True         (?,1)
          9. l8(B) -> l8(-1 + B)      [B >= 1]     (?,1)
        Signature:
          {(l0,1);(l1,1);(l2,1);(l3,1);(l4,1);(l5,1);(l6,1);(l7,1);(l8,1);(l9,1)}
        Flow Graph:
          [0->{1,2},1->{3,4},2->{},3->{1,2},4->{5},5->{6,7},6->{8,9},7->{},8->{},9->{9}]
        Sizebounds:
          (<0,0,B>, B) 
          (<1,0,B>, ?) 
          (<1,1,B>, ?) 
          (<2,0,B>, ?) 
          (<3,0,B>, ?) 
          (<4,0,B>, ?) 
          (<5,0,B>, ?) 
          (<6,0,B>, ?) 
          (<6,1,B>, ?) 
          (<7,0,B>, ?) 
          (<8,0,B>, ?) 
          (<9,0,B>, ?) 
    + Applied Processor:
        LeafRules
    + Details:
        The following transitions are estimated by its predecessors and are removed [2,7,8]
* Step 5: PolyRank WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0. l0(B) -> l1(B)           True     (1,1)
          1. l1(B) -> c2(l2(B),l3(B)) [B >= 0] (?,1)
          3. l2(B) -> l1(-1 + B)      [B >= 0] (?,1)
          4. l3(B) -> l5(B)           True     (?,1)
          5. l5(B) -> l6(B)           True     (?,1)
          6. l6(B) -> c2(l7(B),l8(B)) [B >= 1] (?,1)
          9. l8(B) -> l8(-1 + B)      [B >= 1] (?,1)
        Signature:
          {(l0,1);(l1,1);(l2,1);(l3,1);(l4,1);(l5,1);(l6,1);(l7,1);(l8,1);(l9,1)}
        Flow Graph:
          [0->{1},1->{3,4},3->{1},4->{5},5->{6},6->{9},9->{9}]
        Sizebounds:
          (<0,0,B>, B) 
          (<1,0,B>, ?) 
          (<1,1,B>, ?) 
          (<3,0,B>, ?) 
          (<4,0,B>, ?) 
          (<5,0,B>, ?) 
          (<6,0,B>, ?) 
          (<6,1,B>, ?) 
          (<9,0,B>, ?) 
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [1,3], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
          p(l1) = 1 + x1
          p(l2) = 1 + x1
          p(l3) = 0     
        
        The following rules are strictly oriented:
        [B >= 0] ==>           
           l2(B)   = 1 + B     
                   > B         
                   = l1(-1 + B)
        
        
        The following rules are weakly oriented:
        [B >= 0] ==>                
           l1(B)   = 1 + B          
                  >= 1 + B          
                   = c2(l2(B),l3(B))
        
        We use the following global sizebounds:
        (<0,0,B>, B) 
        (<1,0,B>, ?) 
        (<1,1,B>, ?) 
        (<3,0,B>, ?) 
        (<4,0,B>, ?) 
        (<5,0,B>, ?) 
        (<6,0,B>, ?) 
        (<6,1,B>, ?) 
        (<9,0,B>, ?) 
* Step 6: KnowledgePropagation WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0. l0(B) -> l1(B)           True     (1,1)    
          1. l1(B) -> c2(l2(B),l3(B)) [B >= 0] (?,1)    
          3. l2(B) -> l1(-1 + B)      [B >= 0] (1 + B,1)
          4. l3(B) -> l5(B)           True     (?,1)    
          5. l5(B) -> l6(B)           True     (?,1)    
          6. l6(B) -> c2(l7(B),l8(B)) [B >= 1] (?,1)    
          9. l8(B) -> l8(-1 + B)      [B >= 1] (?,1)    
        Signature:
          {(l0,1);(l1,1);(l2,1);(l3,1);(l4,1);(l5,1);(l6,1);(l7,1);(l8,1);(l9,1)}
        Flow Graph:
          [0->{1},1->{3,4},3->{1},4->{5},5->{6},6->{9},9->{9}]
        Sizebounds:
          (<0,0,B>, B) 
          (<1,0,B>, ?) 
          (<1,1,B>, ?) 
          (<3,0,B>, ?) 
          (<4,0,B>, ?) 
          (<5,0,B>, ?) 
          (<6,0,B>, ?) 
          (<6,1,B>, ?) 
          (<9,0,B>, ?) 
    + Applied Processor:
        KnowledgePropagation
    + Details:
        We propagate bounds from predecessors.
* Step 7: ChainProcessor WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0. l0(B) -> l1(B)           True     (1,1)    
          1. l1(B) -> c2(l2(B),l3(B)) [B >= 0] (2 + B,1)
          3. l2(B) -> l1(-1 + B)      [B >= 0] (1 + B,1)
          4. l3(B) -> l5(B)           True     (2 + B,1)
          5. l5(B) -> l6(B)           True     (2 + B,1)
          6. l6(B) -> c2(l7(B),l8(B)) [B >= 1] (2 + B,1)
          9. l8(B) -> l8(-1 + B)      [B >= 1] (?,1)    
        Signature:
          {(l0,1);(l1,1);(l2,1);(l3,1);(l4,1);(l5,1);(l6,1);(l7,1);(l8,1);(l9,1)}
        Flow Graph:
          [0->{1},1->{3,4},3->{1},4->{5},5->{6},6->{9},9->{9}]
        Sizebounds:
          (<0,0,B>, B) 
          (<1,0,B>, ?) 
          (<1,1,B>, ?) 
          (<3,0,B>, ?) 
          (<4,0,B>, ?) 
          (<5,0,B>, ?) 
          (<6,0,B>, ?) 
          (<6,1,B>, ?) 
          (<9,0,B>, ?) 
    + Applied Processor:
        ChainProcessor False [0,1,3,4,5,6,9]
    + Details:
        We chained rule 1 to obtain the rules [10] .
* Step 8: UnreachableRules WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0.  l0(B) -> l1(B)                True               (1,1)    
          3.  l2(B) -> l1(-1 + B)           [B >= 0]           (1 + B,1)
          4.  l3(B) -> l5(B)                True               (2 + B,1)
          5.  l5(B) -> l6(B)                True               (2 + B,1)
          6.  l6(B) -> c2(l7(B),l8(B))      [B >= 1]           (2 + B,1)
          9.  l8(B) -> l8(-1 + B)           [B >= 1]           (?,1)    
          10. l1(B) -> c2(l1(-1 + B),l3(B)) [B >= 0 && B >= 0] (2 + B,2)
        Signature:
          {(l0,1);(l1,1);(l2,1);(l3,1);(l4,1);(l5,1);(l6,1);(l7,1);(l8,1);(l9,1)}
        Flow Graph:
          [0->{10},3->{10},4->{5},5->{6},6->{9},9->{9},10->{4,10}]
        Sizebounds:
          (< 0,0,B>, B) 
          (< 3,0,B>, ?) 
          (< 4,0,B>, ?) 
          (< 5,0,B>, ?) 
          (< 6,0,B>, ?) 
          (< 6,1,B>, ?) 
          (< 9,0,B>, ?) 
          (<10,0,B>, ?) 
    + Applied Processor:
        UnreachableRules
    + Details:
        The following transitions are not reachable from the starting states and are removed: [3]
* Step 9: ChainProcessor WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0.  l0(B) -> l1(B)                True               (1,1)    
          4.  l3(B) -> l5(B)                True               (2 + B,1)
          5.  l5(B) -> l6(B)                True               (2 + B,1)
          6.  l6(B) -> c2(l7(B),l8(B))      [B >= 1]           (2 + B,1)
          9.  l8(B) -> l8(-1 + B)           [B >= 1]           (?,1)    
          10. l1(B) -> c2(l1(-1 + B),l3(B)) [B >= 0 && B >= 0] (2 + B,2)
        Signature:
          {(l0,1);(l1,1);(l2,1);(l3,1);(l4,1);(l5,1);(l6,1);(l7,1);(l8,1);(l9,1)}
        Flow Graph:
          [0->{10},4->{5},5->{6},6->{9},9->{9},10->{4,10}]
        Sizebounds:
          (< 0,0,B>, B) 
          (< 4,0,B>, ?) 
          (< 5,0,B>, ?) 
          (< 6,0,B>, ?) 
          (< 6,1,B>, ?) 
          (< 9,0,B>, ?) 
          (<10,0,B>, ?) 
    + Applied Processor:
        ChainProcessor False [0,4,5,6,9,10]
    + Details:
        We chained rule 4 to obtain the rules [11] .
* Step 10: UnreachableRules WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0.  l0(B) -> l1(B)                True               (1,1)    
          5.  l5(B) -> l6(B)                True               (2 + B,1)
          6.  l6(B) -> c2(l7(B),l8(B))      [B >= 1]           (2 + B,1)
          9.  l8(B) -> l8(-1 + B)           [B >= 1]           (?,1)    
          10. l1(B) -> c2(l1(-1 + B),l3(B)) [B >= 0 && B >= 0] (2 + B,2)
          11. l3(B) -> l6(B)                True               (2 + B,2)
        Signature:
          {(l0,1);(l1,1);(l2,1);(l3,1);(l4,1);(l5,1);(l6,1);(l7,1);(l8,1);(l9,1)}
        Flow Graph:
          [0->{10},5->{6},6->{9},9->{9},10->{10,11},11->{6}]
        Sizebounds:
          (< 0,0,B>, B) 
          (< 5,0,B>, ?) 
          (< 6,0,B>, ?) 
          (< 6,1,B>, ?) 
          (< 9,0,B>, ?) 
          (<10,0,B>, ?) 
          (<11,0,B>, ?) 
    + Applied Processor:
        UnreachableRules
    + Details:
        The following transitions are not reachable from the starting states and are removed: [5]
* Step 11: ChainProcessor WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0.  l0(B) -> l1(B)                True               (1,1)    
          6.  l6(B) -> c2(l7(B),l8(B))      [B >= 1]           (2 + B,1)
          9.  l8(B) -> l8(-1 + B)           [B >= 1]           (?,1)    
          10. l1(B) -> c2(l1(-1 + B),l3(B)) [B >= 0 && B >= 0] (2 + B,2)
          11. l3(B) -> l6(B)                True               (2 + B,2)
        Signature:
          {(l0,1);(l1,1);(l2,1);(l3,1);(l4,1);(l5,1);(l6,1);(l7,1);(l8,1);(l9,1)}
        Flow Graph:
          [0->{10},6->{9},9->{9},10->{10,11},11->{6}]
        Sizebounds:
          (< 0,0,B>, B) 
          (< 6,0,B>, ?) 
          (< 6,1,B>, ?) 
          (< 9,0,B>, ?) 
          (<10,0,B>, ?) 
          (<11,0,B>, ?) 
    + Applied Processor:
        ChainProcessor False [0,6,9,10,11]
    + Details:
        We chained rule 10 to obtain the rules [12] .
* Step 12: UnreachableRules WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0.  l0(B) -> l1(B)                     True               (1,1)    
          6.  l6(B) -> c2(l7(B),l8(B))           [B >= 1]           (2 + B,1)
          9.  l8(B) -> l8(-1 + B)                [B >= 1]           (?,1)    
          11. l3(B) -> l6(B)                     True               (2 + B,2)
          12. l1(B) -> c2(l1(-1 + B),l6(-1 + B)) [B >= 0 && B >= 0] (2 + B,4)
        Signature:
          {(l0,1);(l1,1);(l2,1);(l3,1);(l4,1);(l5,1);(l6,1);(l7,1);(l8,1);(l9,1)}
        Flow Graph:
          [0->{12},6->{9},9->{9},11->{6},12->{6,12}]
        Sizebounds:
          (< 0,0,B>, B) 
          (< 6,0,B>, ?) 
          (< 6,1,B>, ?) 
          (< 9,0,B>, ?) 
          (<11,0,B>, ?) 
          (<12,0,B>, ?) 
    + Applied Processor:
        UnreachableRules
    + Details:
        The following transitions are not reachable from the starting states and are removed: [11]
* Step 13: LocalSizeboundsProc WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0.  l0(B) -> l1(B)                     True               (1,1)    
          6.  l6(B) -> c2(l7(B),l8(B))           [B >= 1]           (2 + B,1)
          9.  l8(B) -> l8(-1 + B)                [B >= 1]           (?,1)    
          12. l1(B) -> c2(l1(-1 + B),l6(-1 + B)) [B >= 0 && B >= 0] (2 + B,4)
        Signature:
          {(l0,1);(l1,1);(l2,1);(l3,1);(l4,1);(l5,1);(l6,1);(l7,1);(l8,1);(l9,1)}
        Flow Graph:
          [0->{12},6->{9},9->{9},12->{6,12}]
        Sizebounds:
          (< 0,0,B>, B) 
          (< 6,0,B>, ?) 
          (< 6,1,B>, ?) 
          (< 9,0,B>, ?) 
          (<12,0,B>, ?) 
    + Applied Processor:
        LocalSizeboundsProc
    + Details:
        LocalSizebounds generated; rvgraph
          (< 0,0,B>,     B, .= 0) 
          (< 6,0,B>,     B, .= 0) 
          (< 6,1,B>,     B, .= 0) 
          (< 9,0,B>, 1 + B, .+ 1) 
          (<12,0,B>, 1 + B, .+ 1) 
          (<12,1,B>, 1 + B, .+ 1) 
* Step 14: SizeboundsProc WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0.  l0(B) -> l1(B)                     True               (1,1)    
          6.  l6(B) -> c2(l7(B),l8(B))           [B >= 1]           (2 + B,1)
          9.  l8(B) -> l8(-1 + B)                [B >= 1]           (?,1)    
          12. l1(B) -> c2(l1(-1 + B),l6(-1 + B)) [B >= 0 && B >= 0] (2 + B,4)
        Signature:
          {(l0,1);(l1,1);(l2,1);(l3,1);(l4,1);(l5,1);(l6,1);(l7,1);(l8,1);(l9,1)}
        Flow Graph:
          [0->{12},6->{9},9->{9},12->{6,12}]
        Sizebounds:
          (< 0,0,B>, ?) 
          (< 6,0,B>, ?) 
          (< 6,1,B>, ?) 
          (< 9,0,B>, ?) 
          (<12,0,B>, ?) 
          (<12,1,B>, ?) 
    + Applied Processor:
        SizeboundsProc
    + Details:
        Sizebounds computed:
          (< 0,0,B>,       B) 
          (< 6,0,B>, 4 + 3*B) 
          (< 6,1,B>, 4 + 3*B) 
          (< 9,0,B>,       ?) 
          (<12,0,B>, 4 + 3*B) 
          (<12,1,B>, 4 + 3*B) 
* Step 15: LocationConstraintsProc WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0.  l0(B) -> l1(B)                     True               (1,1)    
          6.  l6(B) -> c2(l7(B),l8(B))           [B >= 1]           (2 + B,1)
          9.  l8(B) -> l8(-1 + B)                [B >= 1]           (?,1)    
          12. l1(B) -> c2(l1(-1 + B),l6(-1 + B)) [B >= 0 && B >= 0] (2 + B,4)
        Signature:
          {(l0,1);(l1,1);(l2,1);(l3,1);(l4,1);(l5,1);(l6,1);(l7,1);(l8,1);(l9,1)}
        Flow Graph:
          [0->{12},6->{9},9->{9},12->{6,12}]
        Sizebounds:
          (< 0,0,B>,       B) 
          (< 6,0,B>, 4 + 3*B) 
          (< 6,1,B>, 4 + 3*B) 
          (< 9,0,B>,       ?) 
          (<12,0,B>, 4 + 3*B) 
          (<12,1,B>, 4 + 3*B) 
    + Applied Processor:
        LocationConstraintsProc
    + Details:
        We computed the location constraints  0 :  True 6 :  True 9 :  True 12 :  True .
* Step 16: LoopRecurrenceProcessor WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0.  l0(B) -> l1(B)                     True               (1,1)    
          6.  l6(B) -> c2(l7(B),l8(B))           [B >= 1]           (2 + B,1)
          9.  l8(B) -> l8(-1 + B)                [B >= 1]           (?,1)    
          12. l1(B) -> c2(l1(-1 + B),l6(-1 + B)) [B >= 0 && B >= 0] (2 + B,4)
        Signature:
          {(l0,1);(l1,1);(l2,1);(l3,1);(l4,1);(l5,1);(l6,1);(l7,1);(l8,1);(l9,1)}
        Flow Graph:
          [0->{12},6->{9},9->{9},12->{6,12}]
        Sizebounds:
          (< 0,0,B>,       B) 
          (< 6,0,B>, 4 + 3*B) 
          (< 6,1,B>, 4 + 3*B) 
          (< 9,0,B>,       ?) 
          (<12,0,B>, 4 + 3*B) 
          (<12,1,B>, 4 + 3*B) 
    + Applied Processor:
        LoopRecurrenceProcessor [12]
    + Details:
        Applying the recurrence pattern linear * f to the expression B yields the solution 2*B + B^2 .
* Step 17: LoopRecurrenceProcessor WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0.  l0(B) -> l1(B)                     True               (1,1)        
          6.  l6(B) -> c2(l7(B),l8(B))           [B >= 1]           (2 + B,1)    
          9.  l8(B) -> l8(-1 + B)                [B >= 1]           (2*B + B^2,1)
          12. l1(B) -> c2(l1(-1 + B),l6(-1 + B)) [B >= 0 && B >= 0] (2 + B,4)    
        Signature:
          {(l0,1);(l1,1);(l2,1);(l3,1);(l4,1);(l5,1);(l6,1);(l7,1);(l8,1);(l9,1)}
        Flow Graph:
          [0->{12},6->{9},9->{9},12->{6,12}]
        Sizebounds:
          (< 0,0,B>,       B) 
          (< 6,0,B>, 4 + 3*B) 
          (< 6,1,B>, 4 + 3*B) 
          (< 9,0,B>,       ?) 
          (<12,0,B>, 4 + 3*B) 
          (<12,1,B>, 4 + 3*B) 
    + Applied Processor:
        LoopRecurrenceProcessor [9]
    + Details:
        Applying the recurrence pattern linear * f to the expression B yields the solution B .
* Step 18: UnsatPaths WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0.  l0(B) -> l1(B)                     True               (1,1)        
          6.  l6(B) -> c2(l7(B),l8(B))           [B >= 1]           (2 + B,1)    
          9.  l8(B) -> l8(-1 + B)                [B >= 1]           (2*B + B^2,1)
          12. l1(B) -> c2(l1(-1 + B),l6(-1 + B)) [B >= 0 && B >= 0] (2 + B,4)    
        Signature:
          {(l0,1);(l1,1);(l2,1);(l3,1);(l4,1);(l5,1);(l6,1);(l7,1);(l8,1);(l9,1)}
        Flow Graph:
          [0->{12},6->{9},9->{9},12->{6,12}]
        Sizebounds:
          (< 0,0,B>,       B) 
          (< 6,0,B>, 4 + 3*B) 
          (< 6,1,B>, 4 + 3*B) 
          (< 9,0,B>,       ?) 
          (<12,0,B>, 4 + 3*B) 
          (<12,1,B>, 4 + 3*B) 
    + Applied Processor:
        UnsatPaths
    + Details:
        The problem is already solved.

WORST_CASE(?,O(n^2))