WORST_CASE(?,O(n^2))
* Step 1: UnsatRules WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0. start(A,B,C,D,E,F)  -> stop(A,B,C,F,E,F)       [0 >= A && B = C && D = E && F = A]                          (?,1)
          1. start(A,B,C,D,E,F)  -> lbl52(A,-1 + B,C,F,E,F) [A >= 1 && C >= 1 && B = C && D = E && F = A]                (?,1)
          2. start(A,B,C,D,E,F)  -> lbl72(A,F,C,-1 + F,E,F) [A >= 1 && 0 >= C && B = C && D = E && F = A]                (?,1)
          3. lbl52(A,B,C,D,E,F)  -> stop(A,B,C,D,E,F)       [0 >= D && B >= 0 && D >= 1 && A >= D && F = A]              (?,1)
          4. lbl52(A,B,C,D,E,F)  -> lbl52(A,-1 + B,C,D,E,F) [D >= 1 && B >= 1 && B >= 0 && A >= D && F = A]              (?,1)
          5. lbl52(A,B,C,D,E,F)  -> lbl72(A,F,C,-1 + D,E,F) [D >= 1 && A >= D && B = 0 && F = A]                         (?,1)
          6. lbl72(A,B,C,D,E,F)  -> stop(A,B,C,D,E,F)       [A >= 1 && D = 0 && F = A && B = A]                          (?,1)
          7. lbl72(A,B,C,D,E,F)  -> lbl52(A,-1 + B,C,D,E,F) [D >= 1 && A >= 1 && D >= 0 && A >= 1 + D && F = A && B = A] (?,1)
          8. lbl72(A,B,C,D,E,F)  -> lbl72(A,F,C,-1 + D,E,F) [D >= 1 && 0 >= A && D >= 0 && A >= 1 + D && F = A && B = A] (?,1)
          9. start0(A,B,C,D,E,F) -> start(A,C,C,E,E,A)      True                                                         (1,1)
        Signature:
          {(lbl52,6);(lbl72,6);(start,6);(start0,6);(stop,6)}
        Flow Graph:
          [0->{},1->{3,4,5},2->{6,7,8},3->{},4->{3,4,5},5->{6,7,8},6->{},7->{3,4,5},8->{6,7,8},9->{0,1,2}]
        
    + Applied Processor:
        UnsatRules
    + Details:
        The following transitions have unsatisfiable constraints and are removed:  [3,8]
* Step 2: LocalSizeboundsProc WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0. start(A,B,C,D,E,F)  -> stop(A,B,C,F,E,F)       [0 >= A && B = C && D = E && F = A]                          (?,1)
          1. start(A,B,C,D,E,F)  -> lbl52(A,-1 + B,C,F,E,F) [A >= 1 && C >= 1 && B = C && D = E && F = A]                (?,1)
          2. start(A,B,C,D,E,F)  -> lbl72(A,F,C,-1 + F,E,F) [A >= 1 && 0 >= C && B = C && D = E && F = A]                (?,1)
          4. lbl52(A,B,C,D,E,F)  -> lbl52(A,-1 + B,C,D,E,F) [D >= 1 && B >= 1 && B >= 0 && A >= D && F = A]              (?,1)
          5. lbl52(A,B,C,D,E,F)  -> lbl72(A,F,C,-1 + D,E,F) [D >= 1 && A >= D && B = 0 && F = A]                         (?,1)
          6. lbl72(A,B,C,D,E,F)  -> stop(A,B,C,D,E,F)       [A >= 1 && D = 0 && F = A && B = A]                          (?,1)
          7. lbl72(A,B,C,D,E,F)  -> lbl52(A,-1 + B,C,D,E,F) [D >= 1 && A >= 1 && D >= 0 && A >= 1 + D && F = A && B = A] (?,1)
          9. start0(A,B,C,D,E,F) -> start(A,C,C,E,E,A)      True                                                         (1,1)
        Signature:
          {(lbl52,6);(lbl72,6);(start,6);(start0,6);(stop,6)}
        Flow Graph:
          [0->{},1->{4,5},2->{6,7},4->{4,5},5->{6,7},6->{},7->{4,5},9->{0,1,2}]
        
    + Applied Processor:
        LocalSizeboundsProc
    + Details:
        LocalSizebounds generated; rvgraph
          (<0,0,A>, A, .= 0) (<0,0,B>,     B, .= 0) (<0,0,C>, C, .= 0) (<0,0,D>,     F, .= 0) (<0,0,E>, E, .= 0) (<0,0,F>, F, .= 0) 
          (<1,0,A>, A, .= 0) (<1,0,B>, 1 + B, .+ 1) (<1,0,C>, C, .= 0) (<1,0,D>,     F, .= 0) (<1,0,E>, E, .= 0) (<1,0,F>, F, .= 0) 
          (<2,0,A>, A, .= 0) (<2,0,B>,     F, .= 0) (<2,0,C>, C, .= 0) (<2,0,D>, 1 + F, .+ 1) (<2,0,E>, E, .= 0) (<2,0,F>, F, .= 0) 
          (<4,0,A>, A, .= 0) (<4,0,B>, 1 + B, .+ 1) (<4,0,C>, C, .= 0) (<4,0,D>,     D, .= 0) (<4,0,E>, E, .= 0) (<4,0,F>, F, .= 0) 
          (<5,0,A>, A, .= 0) (<5,0,B>,     F, .= 0) (<5,0,C>, C, .= 0) (<5,0,D>, 1 + D, .+ 1) (<5,0,E>, E, .= 0) (<5,0,F>, F, .= 0) 
          (<6,0,A>, A, .= 0) (<6,0,B>,     B, .= 0) (<6,0,C>, C, .= 0) (<6,0,D>,     D, .= 0) (<6,0,E>, E, .= 0) (<6,0,F>, F, .= 0) 
          (<7,0,A>, A, .= 0) (<7,0,B>, 1 + B, .+ 1) (<7,0,C>, C, .= 0) (<7,0,D>,     D, .= 0) (<7,0,E>, E, .= 0) (<7,0,F>, F, .= 0) 
          (<9,0,A>, A, .= 0) (<9,0,B>,     C, .= 0) (<9,0,C>, C, .= 0) (<9,0,D>,     E, .= 0) (<9,0,E>, E, .= 0) (<9,0,F>, A, .= 0) 
* Step 3: SizeboundsProc WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0. start(A,B,C,D,E,F)  -> stop(A,B,C,F,E,F)       [0 >= A && B = C && D = E && F = A]                          (?,1)
          1. start(A,B,C,D,E,F)  -> lbl52(A,-1 + B,C,F,E,F) [A >= 1 && C >= 1 && B = C && D = E && F = A]                (?,1)
          2. start(A,B,C,D,E,F)  -> lbl72(A,F,C,-1 + F,E,F) [A >= 1 && 0 >= C && B = C && D = E && F = A]                (?,1)
          4. lbl52(A,B,C,D,E,F)  -> lbl52(A,-1 + B,C,D,E,F) [D >= 1 && B >= 1 && B >= 0 && A >= D && F = A]              (?,1)
          5. lbl52(A,B,C,D,E,F)  -> lbl72(A,F,C,-1 + D,E,F) [D >= 1 && A >= D && B = 0 && F = A]                         (?,1)
          6. lbl72(A,B,C,D,E,F)  -> stop(A,B,C,D,E,F)       [A >= 1 && D = 0 && F = A && B = A]                          (?,1)
          7. lbl72(A,B,C,D,E,F)  -> lbl52(A,-1 + B,C,D,E,F) [D >= 1 && A >= 1 && D >= 0 && A >= 1 + D && F = A && B = A] (?,1)
          9. start0(A,B,C,D,E,F) -> start(A,C,C,E,E,A)      True                                                         (1,1)
        Signature:
          {(lbl52,6);(lbl72,6);(start,6);(start0,6);(stop,6)}
        Flow Graph:
          [0->{},1->{4,5},2->{6,7},4->{4,5},5->{6,7},6->{},7->{4,5},9->{0,1,2}]
        Sizebounds:
          (<0,0,A>, ?) (<0,0,B>, ?) (<0,0,C>, ?) (<0,0,D>, ?) (<0,0,E>, ?) (<0,0,F>, ?) 
          (<1,0,A>, ?) (<1,0,B>, ?) (<1,0,C>, ?) (<1,0,D>, ?) (<1,0,E>, ?) (<1,0,F>, ?) 
          (<2,0,A>, ?) (<2,0,B>, ?) (<2,0,C>, ?) (<2,0,D>, ?) (<2,0,E>, ?) (<2,0,F>, ?) 
          (<4,0,A>, ?) (<4,0,B>, ?) (<4,0,C>, ?) (<4,0,D>, ?) (<4,0,E>, ?) (<4,0,F>, ?) 
          (<5,0,A>, ?) (<5,0,B>, ?) (<5,0,C>, ?) (<5,0,D>, ?) (<5,0,E>, ?) (<5,0,F>, ?) 
          (<6,0,A>, ?) (<6,0,B>, ?) (<6,0,C>, ?) (<6,0,D>, ?) (<6,0,E>, ?) (<6,0,F>, ?) 
          (<7,0,A>, ?) (<7,0,B>, ?) (<7,0,C>, ?) (<7,0,D>, ?) (<7,0,E>, ?) (<7,0,F>, ?) 
          (<9,0,A>, ?) (<9,0,B>, ?) (<9,0,C>, ?) (<9,0,D>, ?) (<9,0,E>, ?) (<9,0,F>, ?) 
    + Applied Processor:
        SizeboundsProc
    + Details:
        Sizebounds computed:
          (<0,0,A>, A) (<0,0,B>,     C) (<0,0,C>, C) (<0,0,D>,     A) (<0,0,E>, E) (<0,0,F>, A) 
          (<1,0,A>, A) (<1,0,B>, 1 + C) (<1,0,C>, C) (<1,0,D>,     A) (<1,0,E>, E) (<1,0,F>, A) 
          (<2,0,A>, A) (<2,0,B>,     A) (<2,0,C>, C) (<2,0,D>, 1 + A) (<2,0,E>, E) (<2,0,F>, A) 
          (<4,0,A>, A) (<4,0,B>,     ?) (<4,0,C>, C) (<4,0,D>,     A) (<4,0,E>, E) (<4,0,F>, A) 
          (<5,0,A>, A) (<5,0,B>,     A) (<5,0,C>, C) (<5,0,D>,     A) (<5,0,E>, E) (<5,0,F>, A) 
          (<6,0,A>, A) (<6,0,B>,     A) (<6,0,C>, C) (<6,0,D>, 1 + A) (<6,0,E>, E) (<6,0,F>, A) 
          (<7,0,A>, A) (<7,0,B>, 1 + A) (<7,0,C>, C) (<7,0,D>,     A) (<7,0,E>, E) (<7,0,F>, A) 
          (<9,0,A>, A) (<9,0,B>,     C) (<9,0,C>, C) (<9,0,D>,     E) (<9,0,E>, E) (<9,0,F>, A) 
* Step 4: UnsatPaths WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0. start(A,B,C,D,E,F)  -> stop(A,B,C,F,E,F)       [0 >= A && B = C && D = E && F = A]                          (?,1)
          1. start(A,B,C,D,E,F)  -> lbl52(A,-1 + B,C,F,E,F) [A >= 1 && C >= 1 && B = C && D = E && F = A]                (?,1)
          2. start(A,B,C,D,E,F)  -> lbl72(A,F,C,-1 + F,E,F) [A >= 1 && 0 >= C && B = C && D = E && F = A]                (?,1)
          4. lbl52(A,B,C,D,E,F)  -> lbl52(A,-1 + B,C,D,E,F) [D >= 1 && B >= 1 && B >= 0 && A >= D && F = A]              (?,1)
          5. lbl52(A,B,C,D,E,F)  -> lbl72(A,F,C,-1 + D,E,F) [D >= 1 && A >= D && B = 0 && F = A]                         (?,1)
          6. lbl72(A,B,C,D,E,F)  -> stop(A,B,C,D,E,F)       [A >= 1 && D = 0 && F = A && B = A]                          (?,1)
          7. lbl72(A,B,C,D,E,F)  -> lbl52(A,-1 + B,C,D,E,F) [D >= 1 && A >= 1 && D >= 0 && A >= 1 + D && F = A && B = A] (?,1)
          9. start0(A,B,C,D,E,F) -> start(A,C,C,E,E,A)      True                                                         (1,1)
        Signature:
          {(lbl52,6);(lbl72,6);(start,6);(start0,6);(stop,6)}
        Flow Graph:
          [0->{},1->{4,5},2->{6,7},4->{4,5},5->{6,7},6->{},7->{4,5},9->{0,1,2}]
        Sizebounds:
          (<0,0,A>, A) (<0,0,B>,     C) (<0,0,C>, C) (<0,0,D>,     A) (<0,0,E>, E) (<0,0,F>, A) 
          (<1,0,A>, A) (<1,0,B>, 1 + C) (<1,0,C>, C) (<1,0,D>,     A) (<1,0,E>, E) (<1,0,F>, A) 
          (<2,0,A>, A) (<2,0,B>,     A) (<2,0,C>, C) (<2,0,D>, 1 + A) (<2,0,E>, E) (<2,0,F>, A) 
          (<4,0,A>, A) (<4,0,B>,     ?) (<4,0,C>, C) (<4,0,D>,     A) (<4,0,E>, E) (<4,0,F>, A) 
          (<5,0,A>, A) (<5,0,B>,     A) (<5,0,C>, C) (<5,0,D>,     A) (<5,0,E>, E) (<5,0,F>, A) 
          (<6,0,A>, A) (<6,0,B>,     A) (<6,0,C>, C) (<6,0,D>, 1 + A) (<6,0,E>, E) (<6,0,F>, A) 
          (<7,0,A>, A) (<7,0,B>, 1 + A) (<7,0,C>, C) (<7,0,D>,     A) (<7,0,E>, E) (<7,0,F>, A) 
          (<9,0,A>, A) (<9,0,B>,     C) (<9,0,C>, C) (<9,0,D>,     E) (<9,0,E>, E) (<9,0,F>, A) 
    + Applied Processor:
        UnsatPaths
    + Details:
        We remove following edges from the transition graph: [(7,5)]
* Step 5: LeafRules WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0. start(A,B,C,D,E,F)  -> stop(A,B,C,F,E,F)       [0 >= A && B = C && D = E && F = A]                          (?,1)
          1. start(A,B,C,D,E,F)  -> lbl52(A,-1 + B,C,F,E,F) [A >= 1 && C >= 1 && B = C && D = E && F = A]                (?,1)
          2. start(A,B,C,D,E,F)  -> lbl72(A,F,C,-1 + F,E,F) [A >= 1 && 0 >= C && B = C && D = E && F = A]                (?,1)
          4. lbl52(A,B,C,D,E,F)  -> lbl52(A,-1 + B,C,D,E,F) [D >= 1 && B >= 1 && B >= 0 && A >= D && F = A]              (?,1)
          5. lbl52(A,B,C,D,E,F)  -> lbl72(A,F,C,-1 + D,E,F) [D >= 1 && A >= D && B = 0 && F = A]                         (?,1)
          6. lbl72(A,B,C,D,E,F)  -> stop(A,B,C,D,E,F)       [A >= 1 && D = 0 && F = A && B = A]                          (?,1)
          7. lbl72(A,B,C,D,E,F)  -> lbl52(A,-1 + B,C,D,E,F) [D >= 1 && A >= 1 && D >= 0 && A >= 1 + D && F = A && B = A] (?,1)
          9. start0(A,B,C,D,E,F) -> start(A,C,C,E,E,A)      True                                                         (1,1)
        Signature:
          {(lbl52,6);(lbl72,6);(start,6);(start0,6);(stop,6)}
        Flow Graph:
          [0->{},1->{4,5},2->{6,7},4->{4,5},5->{6,7},6->{},7->{4},9->{0,1,2}]
        Sizebounds:
          (<0,0,A>, A) (<0,0,B>,     C) (<0,0,C>, C) (<0,0,D>,     A) (<0,0,E>, E) (<0,0,F>, A) 
          (<1,0,A>, A) (<1,0,B>, 1 + C) (<1,0,C>, C) (<1,0,D>,     A) (<1,0,E>, E) (<1,0,F>, A) 
          (<2,0,A>, A) (<2,0,B>,     A) (<2,0,C>, C) (<2,0,D>, 1 + A) (<2,0,E>, E) (<2,0,F>, A) 
          (<4,0,A>, A) (<4,0,B>,     ?) (<4,0,C>, C) (<4,0,D>,     A) (<4,0,E>, E) (<4,0,F>, A) 
          (<5,0,A>, A) (<5,0,B>,     A) (<5,0,C>, C) (<5,0,D>,     A) (<5,0,E>, E) (<5,0,F>, A) 
          (<6,0,A>, A) (<6,0,B>,     A) (<6,0,C>, C) (<6,0,D>, 1 + A) (<6,0,E>, E) (<6,0,F>, A) 
          (<7,0,A>, A) (<7,0,B>, 1 + A) (<7,0,C>, C) (<7,0,D>,     A) (<7,0,E>, E) (<7,0,F>, A) 
          (<9,0,A>, A) (<9,0,B>,     C) (<9,0,C>, C) (<9,0,D>,     E) (<9,0,E>, E) (<9,0,F>, A) 
    + Applied Processor:
        LeafRules
    + Details:
        The following transitions are estimated by its predecessors and are removed [0,6]
* Step 6: PolyRank WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          1. start(A,B,C,D,E,F)  -> lbl52(A,-1 + B,C,F,E,F) [A >= 1 && C >= 1 && B = C && D = E && F = A]                (?,1)
          2. start(A,B,C,D,E,F)  -> lbl72(A,F,C,-1 + F,E,F) [A >= 1 && 0 >= C && B = C && D = E && F = A]                (?,1)
          4. lbl52(A,B,C,D,E,F)  -> lbl52(A,-1 + B,C,D,E,F) [D >= 1 && B >= 1 && B >= 0 && A >= D && F = A]              (?,1)
          5. lbl52(A,B,C,D,E,F)  -> lbl72(A,F,C,-1 + D,E,F) [D >= 1 && A >= D && B = 0 && F = A]                         (?,1)
          7. lbl72(A,B,C,D,E,F)  -> lbl52(A,-1 + B,C,D,E,F) [D >= 1 && A >= 1 && D >= 0 && A >= 1 + D && F = A && B = A] (?,1)
          9. start0(A,B,C,D,E,F) -> start(A,C,C,E,E,A)      True                                                         (1,1)
        Signature:
          {(lbl52,6);(lbl72,6);(start,6);(start0,6);(stop,6)}
        Flow Graph:
          [1->{4,5},2->{7},4->{4,5},5->{7},7->{4},9->{1,2}]
        Sizebounds:
          (<1,0,A>, A) (<1,0,B>, 1 + C) (<1,0,C>, C) (<1,0,D>,     A) (<1,0,E>, E) (<1,0,F>, A) 
          (<2,0,A>, A) (<2,0,B>,     A) (<2,0,C>, C) (<2,0,D>, 1 + A) (<2,0,E>, E) (<2,0,F>, A) 
          (<4,0,A>, A) (<4,0,B>,     ?) (<4,0,C>, C) (<4,0,D>,     A) (<4,0,E>, E) (<4,0,F>, A) 
          (<5,0,A>, A) (<5,0,B>,     A) (<5,0,C>, C) (<5,0,D>,     A) (<5,0,E>, E) (<5,0,F>, A) 
          (<7,0,A>, A) (<7,0,B>, 1 + A) (<7,0,C>, C) (<7,0,D>,     A) (<7,0,E>, E) (<7,0,F>, A) 
          (<9,0,A>, A) (<9,0,B>,     C) (<9,0,C>, C) (<9,0,D>,     E) (<9,0,E>, E) (<9,0,F>, A) 
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
           p(lbl52) = x4    
           p(lbl72) = 1 + x4
           p(start) = x6    
          p(start0) = x1    
        
        The following rules are strictly oriented:
        [D >= 1 && A >= 1 && D >= 0 && A >= 1 + D && F = A && B = A] ==>                        
                                                  lbl72(A,B,C,D,E,F)   = 1 + D                  
                                                                       > D                      
                                                                       = lbl52(A,-1 + B,C,D,E,F)
        
        
        The following rules are weakly oriented:
          [A >= 1 && C >= 1 && B = C && D = E && F = A] ==>                        
                                     start(A,B,C,D,E,F)   = F                      
                                                         >= F                      
                                                          = lbl52(A,-1 + B,C,F,E,F)
        
          [A >= 1 && 0 >= C && B = C && D = E && F = A] ==>                        
                                     start(A,B,C,D,E,F)   = F                      
                                                         >= F                      
                                                          = lbl72(A,F,C,-1 + F,E,F)
        
        [D >= 1 && B >= 1 && B >= 0 && A >= D && F = A] ==>                        
                                     lbl52(A,B,C,D,E,F)   = D                      
                                                         >= D                      
                                                          = lbl52(A,-1 + B,C,D,E,F)
        
                   [D >= 1 && A >= D && B = 0 && F = A] ==>                        
                                     lbl52(A,B,C,D,E,F)   = D                      
                                                         >= D                      
                                                          = lbl72(A,F,C,-1 + D,E,F)
        
                                                   True ==>                        
                                    start0(A,B,C,D,E,F)   = A                      
                                                         >= A                      
                                                          = start(A,C,C,E,E,A)     
        
        
* Step 7: KnowledgePropagation WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          1. start(A,B,C,D,E,F)  -> lbl52(A,-1 + B,C,F,E,F) [A >= 1 && C >= 1 && B = C && D = E && F = A]                (?,1)
          2. start(A,B,C,D,E,F)  -> lbl72(A,F,C,-1 + F,E,F) [A >= 1 && 0 >= C && B = C && D = E && F = A]                (?,1)
          4. lbl52(A,B,C,D,E,F)  -> lbl52(A,-1 + B,C,D,E,F) [D >= 1 && B >= 1 && B >= 0 && A >= D && F = A]              (?,1)
          5. lbl52(A,B,C,D,E,F)  -> lbl72(A,F,C,-1 + D,E,F) [D >= 1 && A >= D && B = 0 && F = A]                         (?,1)
          7. lbl72(A,B,C,D,E,F)  -> lbl52(A,-1 + B,C,D,E,F) [D >= 1 && A >= 1 && D >= 0 && A >= 1 + D && F = A && B = A] (A,1)
          9. start0(A,B,C,D,E,F) -> start(A,C,C,E,E,A)      True                                                         (1,1)
        Signature:
          {(lbl52,6);(lbl72,6);(start,6);(start0,6);(stop,6)}
        Flow Graph:
          [1->{4,5},2->{7},4->{4,5},5->{7},7->{4},9->{1,2}]
        Sizebounds:
          (<1,0,A>, A) (<1,0,B>, 1 + C) (<1,0,C>, C) (<1,0,D>,     A) (<1,0,E>, E) (<1,0,F>, A) 
          (<2,0,A>, A) (<2,0,B>,     A) (<2,0,C>, C) (<2,0,D>, 1 + A) (<2,0,E>, E) (<2,0,F>, A) 
          (<4,0,A>, A) (<4,0,B>,     ?) (<4,0,C>, C) (<4,0,D>,     A) (<4,0,E>, E) (<4,0,F>, A) 
          (<5,0,A>, A) (<5,0,B>,     A) (<5,0,C>, C) (<5,0,D>,     A) (<5,0,E>, E) (<5,0,F>, A) 
          (<7,0,A>, A) (<7,0,B>, 1 + A) (<7,0,C>, C) (<7,0,D>,     A) (<7,0,E>, E) (<7,0,F>, A) 
          (<9,0,A>, A) (<9,0,B>,     C) (<9,0,C>, C) (<9,0,D>,     E) (<9,0,E>, E) (<9,0,F>, A) 
    + Applied Processor:
        KnowledgePropagation
    + Details:
        We propagate bounds from predecessors.
* Step 8: PolyRank WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          1. start(A,B,C,D,E,F)  -> lbl52(A,-1 + B,C,F,E,F) [A >= 1 && C >= 1 && B = C && D = E && F = A]                (1,1)
          2. start(A,B,C,D,E,F)  -> lbl72(A,F,C,-1 + F,E,F) [A >= 1 && 0 >= C && B = C && D = E && F = A]                (1,1)
          4. lbl52(A,B,C,D,E,F)  -> lbl52(A,-1 + B,C,D,E,F) [D >= 1 && B >= 1 && B >= 0 && A >= D && F = A]              (?,1)
          5. lbl52(A,B,C,D,E,F)  -> lbl72(A,F,C,-1 + D,E,F) [D >= 1 && A >= D && B = 0 && F = A]                         (?,1)
          7. lbl72(A,B,C,D,E,F)  -> lbl52(A,-1 + B,C,D,E,F) [D >= 1 && A >= 1 && D >= 0 && A >= 1 + D && F = A && B = A] (A,1)
          9. start0(A,B,C,D,E,F) -> start(A,C,C,E,E,A)      True                                                         (1,1)
        Signature:
          {(lbl52,6);(lbl72,6);(start,6);(start0,6);(stop,6)}
        Flow Graph:
          [1->{4,5},2->{7},4->{4,5},5->{7},7->{4},9->{1,2}]
        Sizebounds:
          (<1,0,A>, A) (<1,0,B>, 1 + C) (<1,0,C>, C) (<1,0,D>,     A) (<1,0,E>, E) (<1,0,F>, A) 
          (<2,0,A>, A) (<2,0,B>,     A) (<2,0,C>, C) (<2,0,D>, 1 + A) (<2,0,E>, E) (<2,0,F>, A) 
          (<4,0,A>, A) (<4,0,B>,     ?) (<4,0,C>, C) (<4,0,D>,     A) (<4,0,E>, E) (<4,0,F>, A) 
          (<5,0,A>, A) (<5,0,B>,     A) (<5,0,C>, C) (<5,0,D>,     A) (<5,0,E>, E) (<5,0,F>, A) 
          (<7,0,A>, A) (<7,0,B>, 1 + A) (<7,0,C>, C) (<7,0,D>,     A) (<7,0,E>, E) (<7,0,F>, A) 
          (<9,0,A>, A) (<9,0,B>,     C) (<9,0,C>, C) (<9,0,D>,     E) (<9,0,E>, E) (<9,0,F>, A) 
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
           p(lbl52) = x4
           p(lbl72) = x4
           p(start) = x1
          p(start0) = x1
        
        The following rules are strictly oriented:
        [A >= 1 && 0 >= C && B = C && D = E && F = A] ==>                        
                                   start(A,B,C,D,E,F)   = A                      
                                                        > -1 + F                 
                                                        = lbl72(A,F,C,-1 + F,E,F)
        
                 [D >= 1 && A >= D && B = 0 && F = A] ==>                        
                                   lbl52(A,B,C,D,E,F)   = D                      
                                                        > -1 + D                 
                                                        = lbl72(A,F,C,-1 + D,E,F)
        
        
        The following rules are weakly oriented:
                       [A >= 1 && C >= 1 && B = C && D = E && F = A] ==>                        
                                                  start(A,B,C,D,E,F)   = A                      
                                                                      >= F                      
                                                                       = lbl52(A,-1 + B,C,F,E,F)
        
                     [D >= 1 && B >= 1 && B >= 0 && A >= D && F = A] ==>                        
                                                  lbl52(A,B,C,D,E,F)   = D                      
                                                                      >= D                      
                                                                       = lbl52(A,-1 + B,C,D,E,F)
        
        [D >= 1 && A >= 1 && D >= 0 && A >= 1 + D && F = A && B = A] ==>                        
                                                  lbl72(A,B,C,D,E,F)   = D                      
                                                                      >= D                      
                                                                       = lbl52(A,-1 + B,C,D,E,F)
        
                                                                True ==>                        
                                                 start0(A,B,C,D,E,F)   = A                      
                                                                      >= A                      
                                                                       = start(A,C,C,E,E,A)     
        
        
* Step 9: PolyRank WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          1. start(A,B,C,D,E,F)  -> lbl52(A,-1 + B,C,F,E,F) [A >= 1 && C >= 1 && B = C && D = E && F = A]                (1,1)
          2. start(A,B,C,D,E,F)  -> lbl72(A,F,C,-1 + F,E,F) [A >= 1 && 0 >= C && B = C && D = E && F = A]                (1,1)
          4. lbl52(A,B,C,D,E,F)  -> lbl52(A,-1 + B,C,D,E,F) [D >= 1 && B >= 1 && B >= 0 && A >= D && F = A]              (?,1)
          5. lbl52(A,B,C,D,E,F)  -> lbl72(A,F,C,-1 + D,E,F) [D >= 1 && A >= D && B = 0 && F = A]                         (A,1)
          7. lbl72(A,B,C,D,E,F)  -> lbl52(A,-1 + B,C,D,E,F) [D >= 1 && A >= 1 && D >= 0 && A >= 1 + D && F = A && B = A] (A,1)
          9. start0(A,B,C,D,E,F) -> start(A,C,C,E,E,A)      True                                                         (1,1)
        Signature:
          {(lbl52,6);(lbl72,6);(start,6);(start0,6);(stop,6)}
        Flow Graph:
          [1->{4,5},2->{7},4->{4,5},5->{7},7->{4},9->{1,2}]
        Sizebounds:
          (<1,0,A>, A) (<1,0,B>, 1 + C) (<1,0,C>, C) (<1,0,D>,     A) (<1,0,E>, E) (<1,0,F>, A) 
          (<2,0,A>, A) (<2,0,B>,     A) (<2,0,C>, C) (<2,0,D>, 1 + A) (<2,0,E>, E) (<2,0,F>, A) 
          (<4,0,A>, A) (<4,0,B>,     ?) (<4,0,C>, C) (<4,0,D>,     A) (<4,0,E>, E) (<4,0,F>, A) 
          (<5,0,A>, A) (<5,0,B>,     A) (<5,0,C>, C) (<5,0,D>,     A) (<5,0,E>, E) (<5,0,F>, A) 
          (<7,0,A>, A) (<7,0,B>, 1 + A) (<7,0,C>, C) (<7,0,D>,     A) (<7,0,E>, E) (<7,0,F>, A) 
          (<9,0,A>, A) (<9,0,B>,     C) (<9,0,C>, C) (<9,0,D>,     E) (<9,0,E>, E) (<9,0,F>, A) 
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [4], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
          p(lbl52) = 1 + x2
        
        The following rules are strictly oriented:
        [D >= 1 && B >= 1 && B >= 0 && A >= D && F = A] ==>                        
                                     lbl52(A,B,C,D,E,F)   = 1 + B                  
                                                          > B                      
                                                          = lbl52(A,-1 + B,C,D,E,F)
        
        
        The following rules are weakly oriented:
        
        We use the following global sizebounds:
        (<1,0,A>, A) (<1,0,B>, 1 + C) (<1,0,C>, C) (<1,0,D>,     A) (<1,0,E>, E) (<1,0,F>, A) 
        (<2,0,A>, A) (<2,0,B>,     A) (<2,0,C>, C) (<2,0,D>, 1 + A) (<2,0,E>, E) (<2,0,F>, A) 
        (<4,0,A>, A) (<4,0,B>,     ?) (<4,0,C>, C) (<4,0,D>,     A) (<4,0,E>, E) (<4,0,F>, A) 
        (<5,0,A>, A) (<5,0,B>,     A) (<5,0,C>, C) (<5,0,D>,     A) (<5,0,E>, E) (<5,0,F>, A) 
        (<7,0,A>, A) (<7,0,B>, 1 + A) (<7,0,C>, C) (<7,0,D>,     A) (<7,0,E>, E) (<7,0,F>, A) 
        (<9,0,A>, A) (<9,0,B>,     C) (<9,0,C>, C) (<9,0,D>,     E) (<9,0,E>, E) (<9,0,F>, A) 
* Step 10: KnowledgePropagation WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          1. start(A,B,C,D,E,F)  -> lbl52(A,-1 + B,C,F,E,F) [A >= 1 && C >= 1 && B = C && D = E && F = A]                (1,1)                
          2. start(A,B,C,D,E,F)  -> lbl72(A,F,C,-1 + F,E,F) [A >= 1 && 0 >= C && B = C && D = E && F = A]                (1,1)                
          4. lbl52(A,B,C,D,E,F)  -> lbl52(A,-1 + B,C,D,E,F) [D >= 1 && B >= 1 && B >= 0 && A >= D && F = A]              (2 + 2*A + A^2 + C,1)
          5. lbl52(A,B,C,D,E,F)  -> lbl72(A,F,C,-1 + D,E,F) [D >= 1 && A >= D && B = 0 && F = A]                         (A,1)                
          7. lbl72(A,B,C,D,E,F)  -> lbl52(A,-1 + B,C,D,E,F) [D >= 1 && A >= 1 && D >= 0 && A >= 1 + D && F = A && B = A] (A,1)                
          9. start0(A,B,C,D,E,F) -> start(A,C,C,E,E,A)      True                                                         (1,1)                
        Signature:
          {(lbl52,6);(lbl72,6);(start,6);(start0,6);(stop,6)}
        Flow Graph:
          [1->{4,5},2->{7},4->{4,5},5->{7},7->{4},9->{1,2}]
        Sizebounds:
          (<1,0,A>, A) (<1,0,B>, 1 + C) (<1,0,C>, C) (<1,0,D>,     A) (<1,0,E>, E) (<1,0,F>, A) 
          (<2,0,A>, A) (<2,0,B>,     A) (<2,0,C>, C) (<2,0,D>, 1 + A) (<2,0,E>, E) (<2,0,F>, A) 
          (<4,0,A>, A) (<4,0,B>,     ?) (<4,0,C>, C) (<4,0,D>,     A) (<4,0,E>, E) (<4,0,F>, A) 
          (<5,0,A>, A) (<5,0,B>,     A) (<5,0,C>, C) (<5,0,D>,     A) (<5,0,E>, E) (<5,0,F>, A) 
          (<7,0,A>, A) (<7,0,B>, 1 + A) (<7,0,C>, C) (<7,0,D>,     A) (<7,0,E>, E) (<7,0,F>, A) 
          (<9,0,A>, A) (<9,0,B>,     C) (<9,0,C>, C) (<9,0,D>,     E) (<9,0,E>, E) (<9,0,F>, A) 
    + Applied Processor:
        KnowledgePropagation
    + Details:
        The problem is already solved.

WORST_CASE(?,O(n^2))