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

WORST_CASE(?,O(n^2))