WORST_CASE(?,O(n^2))
* Step 1: LocalSizeboundsProc WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0. l0(A,B,C,D) -> l1(0,B,C,D)          True               (1,1)
          1. l1(A,B,C,D) -> l1(1 + A,-1 + B,C,D) [B >= 1]           (?,1)
          2. l1(A,B,C,D) -> l2(A,B,A,D)          [0 >= B]           (?,1)
          3. l2(A,B,C,D) -> l3(A,B,C,C)          [C >= 1]           (?,1)
          4. l3(A,B,C,D) -> l3(A,B,C,-1 + D)     [D >= 1 && C >= 1] (?,1)
          5. l3(A,B,C,D) -> l2(A,B,-1 + C,D)     [0 >= D && C >= 1] (?,1)
        Signature:
          {(l0,4);(l1,4);(l2,4);(l3,4)}
        Flow Graph:
          [0->{1,2},1->{1,2},2->{3},3->{4,5},4->{4,5},5->{3}]
        
    + Applied Processor:
        LocalSizeboundsProc
    + Details:
        LocalSizebounds generated; rvgraph
          (<0,0,A>,     0, .= 0) (<0,0,B>,     B, .= 0) (<0,0,C>,     C, .= 0) (<0,0,D>,     D, .= 0) 
          (<1,0,A>, 1 + A, .+ 1) (<1,0,B>, 1 + B, .+ 1) (<1,0,C>,     C, .= 0) (<1,0,D>,     D, .= 0) 
          (<2,0,A>,     A, .= 0) (<2,0,B>,     B, .= 0) (<2,0,C>,     A, .= 0) (<2,0,D>,     D, .= 0) 
          (<3,0,A>,     A, .= 0) (<3,0,B>,     B, .= 0) (<3,0,C>,     C, .= 0) (<3,0,D>,     C, .= 0) 
          (<4,0,A>,     A, .= 0) (<4,0,B>,     B, .= 0) (<4,0,C>,     C, .= 0) (<4,0,D>, 1 + D, .+ 1) 
          (<5,0,A>,     A, .= 0) (<5,0,B>,     B, .= 0) (<5,0,C>, 1 + C, .+ 1) (<5,0,D>,     D, .= 0) 
* Step 2: SizeboundsProc WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0. l0(A,B,C,D) -> l1(0,B,C,D)          True               (1,1)
          1. l1(A,B,C,D) -> l1(1 + A,-1 + B,C,D) [B >= 1]           (?,1)
          2. l1(A,B,C,D) -> l2(A,B,A,D)          [0 >= B]           (?,1)
          3. l2(A,B,C,D) -> l3(A,B,C,C)          [C >= 1]           (?,1)
          4. l3(A,B,C,D) -> l3(A,B,C,-1 + D)     [D >= 1 && C >= 1] (?,1)
          5. l3(A,B,C,D) -> l2(A,B,-1 + C,D)     [0 >= D && C >= 1] (?,1)
        Signature:
          {(l0,4);(l1,4);(l2,4);(l3,4)}
        Flow Graph:
          [0->{1,2},1->{1,2},2->{3},3->{4,5},4->{4,5},5->{3}]
        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>, ?) 
    + Applied Processor:
        SizeboundsProc
    + Details:
        Sizebounds computed:
          (<0,0,A>, 0) (<0,0,B>, B) (<0,0,C>, C) (<0,0,D>, D) 
          (<1,0,A>, ?) (<1,0,B>, ?) (<1,0,C>, C) (<1,0,D>, D) 
          (<2,0,A>, ?) (<2,0,B>, ?) (<2,0,C>, ?) (<2,0,D>, 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>, ?) 
* Step 3: UnsatPaths WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0. l0(A,B,C,D) -> l1(0,B,C,D)          True               (1,1)
          1. l1(A,B,C,D) -> l1(1 + A,-1 + B,C,D) [B >= 1]           (?,1)
          2. l1(A,B,C,D) -> l2(A,B,A,D)          [0 >= B]           (?,1)
          3. l2(A,B,C,D) -> l3(A,B,C,C)          [C >= 1]           (?,1)
          4. l3(A,B,C,D) -> l3(A,B,C,-1 + D)     [D >= 1 && C >= 1] (?,1)
          5. l3(A,B,C,D) -> l2(A,B,-1 + C,D)     [0 >= D && C >= 1] (?,1)
        Signature:
          {(l0,4);(l1,4);(l2,4);(l3,4)}
        Flow Graph:
          [0->{1,2},1->{1,2},2->{3},3->{4,5},4->{4,5},5->{3}]
        Sizebounds:
          (<0,0,A>, 0) (<0,0,B>, B) (<0,0,C>, C) (<0,0,D>, D) 
          (<1,0,A>, ?) (<1,0,B>, ?) (<1,0,C>, C) (<1,0,D>, D) 
          (<2,0,A>, ?) (<2,0,B>, ?) (<2,0,C>, ?) (<2,0,D>, 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>, ?) 
    + Applied Processor:
        UnsatPaths
    + Details:
        We remove following edges from the transition graph: [(3,5)]
* Step 4: PolyRank WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0. l0(A,B,C,D) -> l1(0,B,C,D)          True               (1,1)
          1. l1(A,B,C,D) -> l1(1 + A,-1 + B,C,D) [B >= 1]           (?,1)
          2. l1(A,B,C,D) -> l2(A,B,A,D)          [0 >= B]           (?,1)
          3. l2(A,B,C,D) -> l3(A,B,C,C)          [C >= 1]           (?,1)
          4. l3(A,B,C,D) -> l3(A,B,C,-1 + D)     [D >= 1 && C >= 1] (?,1)
          5. l3(A,B,C,D) -> l2(A,B,-1 + C,D)     [0 >= D && C >= 1] (?,1)
        Signature:
          {(l0,4);(l1,4);(l2,4);(l3,4)}
        Flow Graph:
          [0->{1,2},1->{1,2},2->{3},3->{4},4->{4,5},5->{3}]
        Sizebounds:
          (<0,0,A>, 0) (<0,0,B>, B) (<0,0,C>, C) (<0,0,D>, D) 
          (<1,0,A>, ?) (<1,0,B>, ?) (<1,0,C>, C) (<1,0,D>, D) 
          (<2,0,A>, ?) (<2,0,B>, ?) (<2,0,C>, ?) (<2,0,D>, 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>, ?) 
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
          p(l0) = 2
          p(l1) = 2
          p(l2) = 1
          p(l3) = 1
        
        The following rules are strictly oriented:
             [0 >= B] ==>            
          l1(A,B,C,D)   = 2          
                        > 1          
                        = l2(A,B,A,D)
        
        
        The following rules are weakly oriented:
                      True ==>                     
               l0(A,B,C,D)   = 2                   
                            >= 2                   
                             = l1(0,B,C,D)         
        
                  [B >= 1] ==>                     
               l1(A,B,C,D)   = 2                   
                            >= 2                   
                             = l1(1 + A,-1 + B,C,D)
        
                  [C >= 1] ==>                     
               l2(A,B,C,D)   = 1                   
                            >= 1                   
                             = l3(A,B,C,C)         
        
        [D >= 1 && C >= 1] ==>                     
               l3(A,B,C,D)   = 1                   
                            >= 1                   
                             = l3(A,B,C,-1 + D)    
        
        [0 >= D && C >= 1] ==>                     
               l3(A,B,C,D)   = 1                   
                            >= 1                   
                             = l2(A,B,-1 + C,D)    
        
        
* Step 5: PolyRank WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0. l0(A,B,C,D) -> l1(0,B,C,D)          True               (1,1)
          1. l1(A,B,C,D) -> l1(1 + A,-1 + B,C,D) [B >= 1]           (?,1)
          2. l1(A,B,C,D) -> l2(A,B,A,D)          [0 >= B]           (2,1)
          3. l2(A,B,C,D) -> l3(A,B,C,C)          [C >= 1]           (?,1)
          4. l3(A,B,C,D) -> l3(A,B,C,-1 + D)     [D >= 1 && C >= 1] (?,1)
          5. l3(A,B,C,D) -> l2(A,B,-1 + C,D)     [0 >= D && C >= 1] (?,1)
        Signature:
          {(l0,4);(l1,4);(l2,4);(l3,4)}
        Flow Graph:
          [0->{1,2},1->{1,2},2->{3},3->{4},4->{4,5},5->{3}]
        Sizebounds:
          (<0,0,A>, 0) (<0,0,B>, B) (<0,0,C>, C) (<0,0,D>, D) 
          (<1,0,A>, ?) (<1,0,B>, ?) (<1,0,C>, C) (<1,0,D>, D) 
          (<2,0,A>, ?) (<2,0,B>, ?) (<2,0,C>, ?) (<2,0,D>, 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>, ?) 
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
          p(l0) = x2
          p(l1) = x2
          p(l2) = x2
          p(l3) = x2
        
        The following rules are strictly oriented:
             [B >= 1] ==>                     
          l1(A,B,C,D)   = B                   
                        > -1 + B              
                        = l1(1 + A,-1 + B,C,D)
        
        
        The following rules are weakly oriented:
                      True ==>                 
               l0(A,B,C,D)   = B               
                            >= B               
                             = l1(0,B,C,D)     
        
                  [0 >= B] ==>                 
               l1(A,B,C,D)   = B               
                            >= B               
                             = l2(A,B,A,D)     
        
                  [C >= 1] ==>                 
               l2(A,B,C,D)   = B               
                            >= B               
                             = l3(A,B,C,C)     
        
        [D >= 1 && C >= 1] ==>                 
               l3(A,B,C,D)   = B               
                            >= B               
                             = l3(A,B,C,-1 + D)
        
        [0 >= D && C >= 1] ==>                 
               l3(A,B,C,D)   = B               
                            >= B               
                             = l2(A,B,-1 + C,D)
        
        
* Step 6: SizeboundsProc WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0. l0(A,B,C,D) -> l1(0,B,C,D)          True               (1,1)
          1. l1(A,B,C,D) -> l1(1 + A,-1 + B,C,D) [B >= 1]           (B,1)
          2. l1(A,B,C,D) -> l2(A,B,A,D)          [0 >= B]           (2,1)
          3. l2(A,B,C,D) -> l3(A,B,C,C)          [C >= 1]           (?,1)
          4. l3(A,B,C,D) -> l3(A,B,C,-1 + D)     [D >= 1 && C >= 1] (?,1)
          5. l3(A,B,C,D) -> l2(A,B,-1 + C,D)     [0 >= D && C >= 1] (?,1)
        Signature:
          {(l0,4);(l1,4);(l2,4);(l3,4)}
        Flow Graph:
          [0->{1,2},1->{1,2},2->{3},3->{4},4->{4,5},5->{3}]
        Sizebounds:
          (<0,0,A>, 0) (<0,0,B>, B) (<0,0,C>, C) (<0,0,D>, D) 
          (<1,0,A>, ?) (<1,0,B>, ?) (<1,0,C>, C) (<1,0,D>, D) 
          (<2,0,A>, ?) (<2,0,B>, ?) (<2,0,C>, ?) (<2,0,D>, 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>, ?) 
    + Applied Processor:
        SizeboundsProc
    + Details:
        Sizebounds computed:
          (<0,0,A>, 0) (<0,0,B>,   B) (<0,0,C>, C) (<0,0,D>, D) 
          (<1,0,A>, B) (<1,0,B>, 2*B) (<1,0,C>, C) (<1,0,D>, D) 
          (<2,0,A>, B) (<2,0,B>, 2*B) (<2,0,C>, B) (<2,0,D>, D) 
          (<3,0,A>, B) (<3,0,B>, 2*B) (<3,0,C>, ?) (<3,0,D>, ?) 
          (<4,0,A>, B) (<4,0,B>, 2*B) (<4,0,C>, ?) (<4,0,D>, ?) 
          (<5,0,A>, B) (<5,0,B>, 2*B) (<5,0,C>, ?) (<5,0,D>, ?) 
* Step 7: PolyRank WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0. l0(A,B,C,D) -> l1(0,B,C,D)          True               (1,1)
          1. l1(A,B,C,D) -> l1(1 + A,-1 + B,C,D) [B >= 1]           (B,1)
          2. l1(A,B,C,D) -> l2(A,B,A,D)          [0 >= B]           (2,1)
          3. l2(A,B,C,D) -> l3(A,B,C,C)          [C >= 1]           (?,1)
          4. l3(A,B,C,D) -> l3(A,B,C,-1 + D)     [D >= 1 && C >= 1] (?,1)
          5. l3(A,B,C,D) -> l2(A,B,-1 + C,D)     [0 >= D && C >= 1] (?,1)
        Signature:
          {(l0,4);(l1,4);(l2,4);(l3,4)}
        Flow Graph:
          [0->{1,2},1->{1,2},2->{3},3->{4},4->{4,5},5->{3}]
        Sizebounds:
          (<0,0,A>, 0) (<0,0,B>,   B) (<0,0,C>, C) (<0,0,D>, D) 
          (<1,0,A>, B) (<1,0,B>, 2*B) (<1,0,C>, C) (<1,0,D>, D) 
          (<2,0,A>, B) (<2,0,B>, 2*B) (<2,0,C>, B) (<2,0,D>, D) 
          (<3,0,A>, B) (<3,0,B>, 2*B) (<3,0,C>, ?) (<3,0,D>, ?) 
          (<4,0,A>, B) (<4,0,B>, 2*B) (<4,0,C>, ?) (<4,0,D>, ?) 
          (<5,0,A>, B) (<5,0,B>, 2*B) (<5,0,C>, ?) (<5,0,D>, ?) 
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [3,5,4], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
          p(l2) = x3
          p(l3) = x3
        
        The following rules are strictly oriented:
        [0 >= D && C >= 1] ==>                 
               l3(A,B,C,D)   = C               
                             > -1 + C          
                             = l2(A,B,-1 + C,D)
        
        
        The following rules are weakly oriented:
                  [C >= 1] ==>                 
               l2(A,B,C,D)   = C               
                            >= C               
                             = l3(A,B,C,C)     
        
        [D >= 1 && C >= 1] ==>                 
               l3(A,B,C,D)   = C               
                            >= C               
                             = l3(A,B,C,-1 + D)
        
        We use the following global sizebounds:
        (<0,0,A>, 0) (<0,0,B>,   B) (<0,0,C>, C) (<0,0,D>, D) 
        (<1,0,A>, B) (<1,0,B>, 2*B) (<1,0,C>, C) (<1,0,D>, D) 
        (<2,0,A>, B) (<2,0,B>, 2*B) (<2,0,C>, B) (<2,0,D>, D) 
        (<3,0,A>, B) (<3,0,B>, 2*B) (<3,0,C>, ?) (<3,0,D>, ?) 
        (<4,0,A>, B) (<4,0,B>, 2*B) (<4,0,C>, ?) (<4,0,D>, ?) 
        (<5,0,A>, B) (<5,0,B>, 2*B) (<5,0,C>, ?) (<5,0,D>, ?) 
* Step 8: KnowledgePropagation WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0. l0(A,B,C,D) -> l1(0,B,C,D)          True               (1,1)  
          1. l1(A,B,C,D) -> l1(1 + A,-1 + B,C,D) [B >= 1]           (B,1)  
          2. l1(A,B,C,D) -> l2(A,B,A,D)          [0 >= B]           (2,1)  
          3. l2(A,B,C,D) -> l3(A,B,C,C)          [C >= 1]           (?,1)  
          4. l3(A,B,C,D) -> l3(A,B,C,-1 + D)     [D >= 1 && C >= 1] (?,1)  
          5. l3(A,B,C,D) -> l2(A,B,-1 + C,D)     [0 >= D && C >= 1] (2*B,1)
        Signature:
          {(l0,4);(l1,4);(l2,4);(l3,4)}
        Flow Graph:
          [0->{1,2},1->{1,2},2->{3},3->{4},4->{4,5},5->{3}]
        Sizebounds:
          (<0,0,A>, 0) (<0,0,B>,   B) (<0,0,C>, C) (<0,0,D>, D) 
          (<1,0,A>, B) (<1,0,B>, 2*B) (<1,0,C>, C) (<1,0,D>, D) 
          (<2,0,A>, B) (<2,0,B>, 2*B) (<2,0,C>, B) (<2,0,D>, D) 
          (<3,0,A>, B) (<3,0,B>, 2*B) (<3,0,C>, ?) (<3,0,D>, ?) 
          (<4,0,A>, B) (<4,0,B>, 2*B) (<4,0,C>, ?) (<4,0,D>, ?) 
          (<5,0,A>, B) (<5,0,B>, 2*B) (<5,0,C>, ?) (<5,0,D>, ?) 
    + Applied Processor:
        KnowledgePropagation
    + Details:
        We propagate bounds from predecessors.
* Step 9: SizeboundsProc WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0. l0(A,B,C,D) -> l1(0,B,C,D)          True               (1,1)      
          1. l1(A,B,C,D) -> l1(1 + A,-1 + B,C,D) [B >= 1]           (B,1)      
          2. l1(A,B,C,D) -> l2(A,B,A,D)          [0 >= B]           (2,1)      
          3. l2(A,B,C,D) -> l3(A,B,C,C)          [C >= 1]           (2 + 2*B,1)
          4. l3(A,B,C,D) -> l3(A,B,C,-1 + D)     [D >= 1 && C >= 1] (?,1)      
          5. l3(A,B,C,D) -> l2(A,B,-1 + C,D)     [0 >= D && C >= 1] (2*B,1)    
        Signature:
          {(l0,4);(l1,4);(l2,4);(l3,4)}
        Flow Graph:
          [0->{1,2},1->{1,2},2->{3},3->{4},4->{4,5},5->{3}]
        Sizebounds:
          (<0,0,A>, 0) (<0,0,B>,   B) (<0,0,C>, C) (<0,0,D>, D) 
          (<1,0,A>, B) (<1,0,B>, 2*B) (<1,0,C>, C) (<1,0,D>, D) 
          (<2,0,A>, B) (<2,0,B>, 2*B) (<2,0,C>, B) (<2,0,D>, D) 
          (<3,0,A>, B) (<3,0,B>, 2*B) (<3,0,C>, ?) (<3,0,D>, ?) 
          (<4,0,A>, B) (<4,0,B>, 2*B) (<4,0,C>, ?) (<4,0,D>, ?) 
          (<5,0,A>, B) (<5,0,B>, 2*B) (<5,0,C>, ?) (<5,0,D>, ?) 
    + Applied Processor:
        SizeboundsProc
    + Details:
        Sizebounds computed:
          (<0,0,A>, 0) (<0,0,B>,   B) (<0,0,C>,   C) (<0,0,D>,   D) 
          (<1,0,A>, B) (<1,0,B>, 2*B) (<1,0,C>,   C) (<1,0,D>,   D) 
          (<2,0,A>, B) (<2,0,B>, 2*B) (<2,0,C>,   B) (<2,0,D>,   D) 
          (<3,0,A>, B) (<3,0,B>, 2*B) (<3,0,C>, 3*B) (<3,0,D>, 3*B) 
          (<4,0,A>, B) (<4,0,B>, 2*B) (<4,0,C>, 3*B) (<4,0,D>,   ?) 
          (<5,0,A>, B) (<5,0,B>, 2*B) (<5,0,C>, 3*B) (<5,0,D>,   ?) 
* Step 10: PolyRank WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0. l0(A,B,C,D) -> l1(0,B,C,D)          True               (1,1)      
          1. l1(A,B,C,D) -> l1(1 + A,-1 + B,C,D) [B >= 1]           (B,1)      
          2. l1(A,B,C,D) -> l2(A,B,A,D)          [0 >= B]           (2,1)      
          3. l2(A,B,C,D) -> l3(A,B,C,C)          [C >= 1]           (2 + 2*B,1)
          4. l3(A,B,C,D) -> l3(A,B,C,-1 + D)     [D >= 1 && C >= 1] (?,1)      
          5. l3(A,B,C,D) -> l2(A,B,-1 + C,D)     [0 >= D && C >= 1] (2*B,1)    
        Signature:
          {(l0,4);(l1,4);(l2,4);(l3,4)}
        Flow Graph:
          [0->{1,2},1->{1,2},2->{3},3->{4},4->{4,5},5->{3}]
        Sizebounds:
          (<0,0,A>, 0) (<0,0,B>,   B) (<0,0,C>,   C) (<0,0,D>,   D) 
          (<1,0,A>, B) (<1,0,B>, 2*B) (<1,0,C>,   C) (<1,0,D>,   D) 
          (<2,0,A>, B) (<2,0,B>, 2*B) (<2,0,C>,   B) (<2,0,D>,   D) 
          (<3,0,A>, B) (<3,0,B>, 2*B) (<3,0,C>, 3*B) (<3,0,D>, 3*B) 
          (<4,0,A>, B) (<4,0,B>, 2*B) (<4,0,C>, 3*B) (<4,0,D>,   ?) 
          (<5,0,A>, B) (<5,0,B>, 2*B) (<5,0,C>, 3*B) (<5,0,D>,   ?) 
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [4], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
          p(l3) = x4
        
        The following rules are strictly oriented:
        [D >= 1 && C >= 1] ==>                 
               l3(A,B,C,D)   = D               
                             > -1 + D          
                             = l3(A,B,C,-1 + D)
        
        
        The following rules are weakly oriented:
        
        We use the following global sizebounds:
        (<0,0,A>, 0) (<0,0,B>,   B) (<0,0,C>,   C) (<0,0,D>,   D) 
        (<1,0,A>, B) (<1,0,B>, 2*B) (<1,0,C>,   C) (<1,0,D>,   D) 
        (<2,0,A>, B) (<2,0,B>, 2*B) (<2,0,C>,   B) (<2,0,D>,   D) 
        (<3,0,A>, B) (<3,0,B>, 2*B) (<3,0,C>, 3*B) (<3,0,D>, 3*B) 
        (<4,0,A>, B) (<4,0,B>, 2*B) (<4,0,C>, 3*B) (<4,0,D>,   ?) 
        (<5,0,A>, B) (<5,0,B>, 2*B) (<5,0,C>, 3*B) (<5,0,D>,   ?) 
* Step 11: KnowledgePropagation WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0. l0(A,B,C,D) -> l1(0,B,C,D)          True               (1,1)          
          1. l1(A,B,C,D) -> l1(1 + A,-1 + B,C,D) [B >= 1]           (B,1)          
          2. l1(A,B,C,D) -> l2(A,B,A,D)          [0 >= B]           (2,1)          
          3. l2(A,B,C,D) -> l3(A,B,C,C)          [C >= 1]           (2 + 2*B,1)    
          4. l3(A,B,C,D) -> l3(A,B,C,-1 + D)     [D >= 1 && C >= 1] (6*B + 6*B^2,1)
          5. l3(A,B,C,D) -> l2(A,B,-1 + C,D)     [0 >= D && C >= 1] (2*B,1)        
        Signature:
          {(l0,4);(l1,4);(l2,4);(l3,4)}
        Flow Graph:
          [0->{1,2},1->{1,2},2->{3},3->{4},4->{4,5},5->{3}]
        Sizebounds:
          (<0,0,A>, 0) (<0,0,B>,   B) (<0,0,C>,   C) (<0,0,D>,   D) 
          (<1,0,A>, B) (<1,0,B>, 2*B) (<1,0,C>,   C) (<1,0,D>,   D) 
          (<2,0,A>, B) (<2,0,B>, 2*B) (<2,0,C>,   B) (<2,0,D>,   D) 
          (<3,0,A>, B) (<3,0,B>, 2*B) (<3,0,C>, 3*B) (<3,0,D>, 3*B) 
          (<4,0,A>, B) (<4,0,B>, 2*B) (<4,0,C>, 3*B) (<4,0,D>,   ?) 
          (<5,0,A>, B) (<5,0,B>, 2*B) (<5,0,C>, 3*B) (<5,0,D>,   ?) 
    + Applied Processor:
        KnowledgePropagation
    + Details:
        The problem is already solved.

WORST_CASE(?,O(n^2))