WORST_CASE(?,O(n^1))
* Step 1: LocalSizeboundsProc WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          0.  start(A,B,C,D)  -> stop(A,B,C,D)          [0 >= A && B = C && D = A]                               (?,1)
          1.  start(A,B,C,D)  -> lbl6(A,B,C,D)          [A >= 1 && 0 >= C && B = C && D = A]                     (?,1)
          2.  start(A,B,C,D)  -> cut(A,B,C,D)           [A >= 1 && D = A && B = A && C = A]                      (?,1)
          3.  start(A,B,C,D)  -> lbl101(A,B + -1*D,C,D) [A >= 1 && C >= 1 + A && B = C && D = A]                 (?,1)
          4.  start(A,B,C,D)  -> lbl111(A,B,C,-1*B + D) [A >= 1 + C && C >= 1 && B = C && D = A]                 (?,1)
          5.  lbl6(A,B,C,D)   -> stop(A,B,C,D)          [A >= 1 && 0 >= C && D = A && B = C]                     (?,1)
          6.  lbl101(A,B,C,D) -> cut(A,B,C,D)           [A >= B && B >= 1 && C >= 2*B && D = B]                  (?,1)
          7.  lbl101(A,B,C,D) -> lbl101(A,B + -1*D,C,D) [B >= 1 + D && A >= D && B >= 1 && D >= 1 && C >= B + D] (?,1)
          8.  lbl101(A,B,C,D) -> lbl111(A,B,C,-1*B + D) [D >= 1 + B && A >= D && B >= 1 && D >= 1 && C >= B + D] (?,1)
          9.  lbl111(A,B,C,D) -> cut(A,B,C,D)           [C >= B && B >= 1 && A >= 2*B && D = B]                  (?,1)
          10. lbl111(A,B,C,D) -> lbl101(A,B + -1*D,C,D) [B >= 1 + D && C >= B && B >= 1 && D >= 1 && A >= B + D] (?,1)
          11. lbl111(A,B,C,D) -> lbl111(A,B,C,-1*B + D) [D >= 1 + B && C >= B && B >= 1 && D >= 1 && A >= B + D] (?,1)
          12. cut(A,B,C,D)    -> stop(A,B,C,D)          [A >= B && B >= 1 && C >= B && D = B]                    (?,1)
          13. start0(A,B,C,D) -> start(A,C,C,A)         True                                                     (1,1)
        Signature:
          {(cut,4);(lbl101,4);(lbl111,4);(lbl6,4);(start,4);(start0,4);(stop,4)}
        Flow Graph:
          [0->{},1->{5},2->{12},3->{6,7,8},4->{9,10,11},5->{},6->{12},7->{6,7,8},8->{9,10,11},9->{12},10->{6,7,8}
          ,11->{9,10,11},12->{},13->{0,1,2,3,4}]
        
    + 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>,         D, .= 0) 
          (< 1,0,A>, A, .= 0) (< 1,0,B>,         B, .= 0) (< 1,0,C>, C, .= 0) (< 1,0,D>,         D, .= 0) 
          (< 2,0,A>, A, .= 0) (< 2,0,B>,         B, .= 0) (< 2,0,C>, C, .= 0) (< 2,0,D>,         D, .= 0) 
          (< 3,0,A>, A, .= 0) (< 3,0,B>,     B + D, .* 0) (< 3,0,C>, C, .= 0) (< 3,0,D>,         D, .= 0) 
          (< 4,0,A>, A, .= 0) (< 4,0,B>,         B, .= 0) (< 4,0,C>, C, .= 0) (< 4,0,D>,     B + D, .* 0) 
          (< 5,0,A>, A, .= 0) (< 5,0,B>,         B, .= 0) (< 5,0,C>, C, .= 0) (< 5,0,D>,         D, .= 0) 
          (< 6,0,A>, A, .= 0) (< 6,0,B>,         B, .= 0) (< 6,0,C>, C, .= 0) (< 6,0,D>,         D, .= 0) 
          (< 7,0,A>, A, .= 0) (< 7,0,B>, 1 + A + B, .* 1) (< 7,0,C>, C, .= 0) (< 7,0,D>,         D, .= 0) 
          (< 8,0,A>, A, .= 0) (< 8,0,B>,         B, .= 0) (< 8,0,C>, C, .= 0) (< 8,0,D>,     B + D, .* 0) 
          (< 9,0,A>, A, .= 0) (< 9,0,B>,         B, .= 0) (< 9,0,C>, C, .= 0) (< 9,0,D>,         D, .= 0) 
          (<10,0,A>, A, .= 0) (<10,0,B>, 1 + B + D, .* 1) (<10,0,C>, C, .= 0) (<10,0,D>,         D, .= 0) 
          (<11,0,A>, A, .= 0) (<11,0,B>,         B, .= 0) (<11,0,C>, C, .= 0) (<11,0,D>, 1 + B + D, .* 1) 
          (<12,0,A>, A, .= 0) (<12,0,B>,         B, .= 0) (<12,0,C>, C, .= 0) (<12,0,D>,         D, .= 0) 
          (<13,0,A>, A, .= 0) (<13,0,B>,         C, .= 0) (<13,0,C>, C, .= 0) (<13,0,D>,         A, .= 0) 
* Step 2: SizeboundsProc WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          0.  start(A,B,C,D)  -> stop(A,B,C,D)          [0 >= A && B = C && D = A]                               (?,1)
          1.  start(A,B,C,D)  -> lbl6(A,B,C,D)          [A >= 1 && 0 >= C && B = C && D = A]                     (?,1)
          2.  start(A,B,C,D)  -> cut(A,B,C,D)           [A >= 1 && D = A && B = A && C = A]                      (?,1)
          3.  start(A,B,C,D)  -> lbl101(A,B + -1*D,C,D) [A >= 1 && C >= 1 + A && B = C && D = A]                 (?,1)
          4.  start(A,B,C,D)  -> lbl111(A,B,C,-1*B + D) [A >= 1 + C && C >= 1 && B = C && D = A]                 (?,1)
          5.  lbl6(A,B,C,D)   -> stop(A,B,C,D)          [A >= 1 && 0 >= C && D = A && B = C]                     (?,1)
          6.  lbl101(A,B,C,D) -> cut(A,B,C,D)           [A >= B && B >= 1 && C >= 2*B && D = B]                  (?,1)
          7.  lbl101(A,B,C,D) -> lbl101(A,B + -1*D,C,D) [B >= 1 + D && A >= D && B >= 1 && D >= 1 && C >= B + D] (?,1)
          8.  lbl101(A,B,C,D) -> lbl111(A,B,C,-1*B + D) [D >= 1 + B && A >= D && B >= 1 && D >= 1 && C >= B + D] (?,1)
          9.  lbl111(A,B,C,D) -> cut(A,B,C,D)           [C >= B && B >= 1 && A >= 2*B && D = B]                  (?,1)
          10. lbl111(A,B,C,D) -> lbl101(A,B + -1*D,C,D) [B >= 1 + D && C >= B && B >= 1 && D >= 1 && A >= B + D] (?,1)
          11. lbl111(A,B,C,D) -> lbl111(A,B,C,-1*B + D) [D >= 1 + B && C >= B && B >= 1 && D >= 1 && A >= B + D] (?,1)
          12. cut(A,B,C,D)    -> stop(A,B,C,D)          [A >= B && B >= 1 && C >= B && D = B]                    (?,1)
          13. start0(A,B,C,D) -> start(A,C,C,A)         True                                                     (1,1)
        Signature:
          {(cut,4);(lbl101,4);(lbl111,4);(lbl6,4);(start,4);(start0,4);(stop,4)}
        Flow Graph:
          [0->{},1->{5},2->{12},3->{6,7,8},4->{9,10,11},5->{},6->{12},7->{6,7,8},8->{9,10,11},9->{12},10->{6,7,8}
          ,11->{9,10,11},12->{},13->{0,1,2,3,4}]
        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>, ?) 
          (< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, ?) 
          (< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,C>, ?) (< 7,0,D>, ?) 
          (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?) 
          (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, ?) (< 9,0,D>, ?) 
          (<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?) (<10,0,D>, ?) 
          (<11,0,A>, ?) (<11,0,B>, ?) (<11,0,C>, ?) (<11,0,D>, ?) 
          (<12,0,A>, ?) (<12,0,B>, ?) (<12,0,C>, ?) (<12,0,D>, ?) 
          (<13,0,A>, ?) (<13,0,B>, ?) (<13,0,C>, ?) (<13,0,D>, ?) 
    + Applied Processor:
        SizeboundsProc
    + Details:
        Sizebounds computed:
          (< 0,0,A>, A) (< 0,0,B>,     C) (< 0,0,C>, C) (< 0,0,D>,     A) 
          (< 1,0,A>, A) (< 1,0,B>,     C) (< 1,0,C>, C) (< 1,0,D>,     A) 
          (< 2,0,A>, A) (< 2,0,B>,     C) (< 2,0,C>, C) (< 2,0,D>,     A) 
          (< 3,0,A>, A) (< 3,0,B>, A + C) (< 3,0,C>, C) (< 3,0,D>,     A) 
          (< 4,0,A>, A) (< 4,0,B>,     C) (< 4,0,C>, C) (< 4,0,D>, A + C) 
          (< 5,0,A>, A) (< 5,0,B>,     C) (< 5,0,C>, C) (< 5,0,D>,     A) 
          (< 6,0,A>, A) (< 6,0,B>,     ?) (< 6,0,C>, C) (< 6,0,D>,     ?) 
          (< 7,0,A>, A) (< 7,0,B>,     ?) (< 7,0,C>, C) (< 7,0,D>,     ?) 
          (< 8,0,A>, A) (< 8,0,B>,     ?) (< 8,0,C>, C) (< 8,0,D>,     ?) 
          (< 9,0,A>, A) (< 9,0,B>,     ?) (< 9,0,C>, C) (< 9,0,D>,     ?) 
          (<10,0,A>, A) (<10,0,B>,     ?) (<10,0,C>, C) (<10,0,D>,     ?) 
          (<11,0,A>, A) (<11,0,B>,     ?) (<11,0,C>, C) (<11,0,D>,     ?) 
          (<12,0,A>, A) (<12,0,B>,     ?) (<12,0,C>, C) (<12,0,D>,     ?) 
          (<13,0,A>, A) (<13,0,B>,     C) (<13,0,C>, C) (<13,0,D>,     A) 
* Step 3: LeafRules WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          0.  start(A,B,C,D)  -> stop(A,B,C,D)          [0 >= A && B = C && D = A]                               (?,1)
          1.  start(A,B,C,D)  -> lbl6(A,B,C,D)          [A >= 1 && 0 >= C && B = C && D = A]                     (?,1)
          2.  start(A,B,C,D)  -> cut(A,B,C,D)           [A >= 1 && D = A && B = A && C = A]                      (?,1)
          3.  start(A,B,C,D)  -> lbl101(A,B + -1*D,C,D) [A >= 1 && C >= 1 + A && B = C && D = A]                 (?,1)
          4.  start(A,B,C,D)  -> lbl111(A,B,C,-1*B + D) [A >= 1 + C && C >= 1 && B = C && D = A]                 (?,1)
          5.  lbl6(A,B,C,D)   -> stop(A,B,C,D)          [A >= 1 && 0 >= C && D = A && B = C]                     (?,1)
          6.  lbl101(A,B,C,D) -> cut(A,B,C,D)           [A >= B && B >= 1 && C >= 2*B && D = B]                  (?,1)
          7.  lbl101(A,B,C,D) -> lbl101(A,B + -1*D,C,D) [B >= 1 + D && A >= D && B >= 1 && D >= 1 && C >= B + D] (?,1)
          8.  lbl101(A,B,C,D) -> lbl111(A,B,C,-1*B + D) [D >= 1 + B && A >= D && B >= 1 && D >= 1 && C >= B + D] (?,1)
          9.  lbl111(A,B,C,D) -> cut(A,B,C,D)           [C >= B && B >= 1 && A >= 2*B && D = B]                  (?,1)
          10. lbl111(A,B,C,D) -> lbl101(A,B + -1*D,C,D) [B >= 1 + D && C >= B && B >= 1 && D >= 1 && A >= B + D] (?,1)
          11. lbl111(A,B,C,D) -> lbl111(A,B,C,-1*B + D) [D >= 1 + B && C >= B && B >= 1 && D >= 1 && A >= B + D] (?,1)
          12. cut(A,B,C,D)    -> stop(A,B,C,D)          [A >= B && B >= 1 && C >= B && D = B]                    (?,1)
          13. start0(A,B,C,D) -> start(A,C,C,A)         True                                                     (1,1)
        Signature:
          {(cut,4);(lbl101,4);(lbl111,4);(lbl6,4);(start,4);(start0,4);(stop,4)}
        Flow Graph:
          [0->{},1->{5},2->{12},3->{6,7,8},4->{9,10,11},5->{},6->{12},7->{6,7,8},8->{9,10,11},9->{12},10->{6,7,8}
          ,11->{9,10,11},12->{},13->{0,1,2,3,4}]
        Sizebounds:
          (< 0,0,A>, A) (< 0,0,B>,     C) (< 0,0,C>, C) (< 0,0,D>,     A) 
          (< 1,0,A>, A) (< 1,0,B>,     C) (< 1,0,C>, C) (< 1,0,D>,     A) 
          (< 2,0,A>, A) (< 2,0,B>,     C) (< 2,0,C>, C) (< 2,0,D>,     A) 
          (< 3,0,A>, A) (< 3,0,B>, A + C) (< 3,0,C>, C) (< 3,0,D>,     A) 
          (< 4,0,A>, A) (< 4,0,B>,     C) (< 4,0,C>, C) (< 4,0,D>, A + C) 
          (< 5,0,A>, A) (< 5,0,B>,     C) (< 5,0,C>, C) (< 5,0,D>,     A) 
          (< 6,0,A>, A) (< 6,0,B>,     ?) (< 6,0,C>, C) (< 6,0,D>,     ?) 
          (< 7,0,A>, A) (< 7,0,B>,     ?) (< 7,0,C>, C) (< 7,0,D>,     ?) 
          (< 8,0,A>, A) (< 8,0,B>,     ?) (< 8,0,C>, C) (< 8,0,D>,     ?) 
          (< 9,0,A>, A) (< 9,0,B>,     ?) (< 9,0,C>, C) (< 9,0,D>,     ?) 
          (<10,0,A>, A) (<10,0,B>,     ?) (<10,0,C>, C) (<10,0,D>,     ?) 
          (<11,0,A>, A) (<11,0,B>,     ?) (<11,0,C>, C) (<11,0,D>,     ?) 
          (<12,0,A>, A) (<12,0,B>,     ?) (<12,0,C>, C) (<12,0,D>,     ?) 
          (<13,0,A>, A) (<13,0,B>,     C) (<13,0,C>, C) (<13,0,D>,     A) 
    + Applied Processor:
        LeafRules
    + Details:
        The following transitions are estimated by its predecessors and are removed [1,2,6,9,0,5,12]
* Step 4: PolyRank WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          3.  start(A,B,C,D)  -> lbl101(A,B + -1*D,C,D) [A >= 1 && C >= 1 + A && B = C && D = A]                 (?,1)
          4.  start(A,B,C,D)  -> lbl111(A,B,C,-1*B + D) [A >= 1 + C && C >= 1 && B = C && D = A]                 (?,1)
          7.  lbl101(A,B,C,D) -> lbl101(A,B + -1*D,C,D) [B >= 1 + D && A >= D && B >= 1 && D >= 1 && C >= B + D] (?,1)
          8.  lbl101(A,B,C,D) -> lbl111(A,B,C,-1*B + D) [D >= 1 + B && A >= D && B >= 1 && D >= 1 && C >= B + D] (?,1)
          10. lbl111(A,B,C,D) -> lbl101(A,B + -1*D,C,D) [B >= 1 + D && C >= B && B >= 1 && D >= 1 && A >= B + D] (?,1)
          11. lbl111(A,B,C,D) -> lbl111(A,B,C,-1*B + D) [D >= 1 + B && C >= B && B >= 1 && D >= 1 && A >= B + D] (?,1)
          13. start0(A,B,C,D) -> start(A,C,C,A)         True                                                     (1,1)
        Signature:
          {(cut,4);(lbl101,4);(lbl111,4);(lbl6,4);(start,4);(start0,4);(stop,4)}
        Flow Graph:
          [3->{7,8},4->{10,11},7->{7,8},8->{10,11},10->{7,8},11->{10,11},13->{3,4}]
        Sizebounds:
          (< 3,0,A>, A) (< 3,0,B>, A + C) (< 3,0,C>, C) (< 3,0,D>,     A) 
          (< 4,0,A>, A) (< 4,0,B>,     C) (< 4,0,C>, C) (< 4,0,D>, A + C) 
          (< 7,0,A>, A) (< 7,0,B>,     ?) (< 7,0,C>, C) (< 7,0,D>,     ?) 
          (< 8,0,A>, A) (< 8,0,B>,     ?) (< 8,0,C>, C) (< 8,0,D>,     ?) 
          (<10,0,A>, A) (<10,0,B>,     ?) (<10,0,C>, C) (<10,0,D>,     ?) 
          (<11,0,A>, A) (<11,0,B>,     ?) (<11,0,C>, C) (<11,0,D>,     ?) 
          (<13,0,A>, A) (<13,0,B>,     C) (<13,0,C>, C) (<13,0,D>,     A) 
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
          p(lbl101) = x4
          p(lbl111) = x4
           p(start) = x4
          p(start0) = x1
        
        The following rules are strictly oriented:
        [D >= 1 + B && C >= B && B >= 1 && D >= 1 && A >= B + D] ==>                       
                                                 lbl111(A,B,C,D)   = D                     
                                                                   > -1*B + D              
                                                                   = lbl111(A,B,C,-1*B + D)
        
        
        The following rules are weakly oriented:
                        [A >= 1 && C >= 1 + A && B = C && D = A] ==>                       
                                                  start(A,B,C,D)   = D                     
                                                                  >= D                     
                                                                   = lbl101(A,B + -1*D,C,D)
        
                        [A >= 1 + C && C >= 1 && B = C && D = A] ==>                       
                                                  start(A,B,C,D)   = D                     
                                                                  >= -1*B + D              
                                                                   = lbl111(A,B,C,-1*B + D)
        
        [B >= 1 + D && A >= D && B >= 1 && D >= 1 && C >= B + D] ==>                       
                                                 lbl101(A,B,C,D)   = D                     
                                                                  >= D                     
                                                                   = lbl101(A,B + -1*D,C,D)
        
        [D >= 1 + B && A >= D && B >= 1 && D >= 1 && C >= B + D] ==>                       
                                                 lbl101(A,B,C,D)   = D                     
                                                                  >= -1*B + D              
                                                                   = lbl111(A,B,C,-1*B + D)
        
        [B >= 1 + D && C >= B && B >= 1 && D >= 1 && A >= B + D] ==>                       
                                                 lbl111(A,B,C,D)   = D                     
                                                                  >= D                     
                                                                   = lbl101(A,B + -1*D,C,D)
        
                                                            True ==>                       
                                                 start0(A,B,C,D)   = A                     
                                                                  >= A                     
                                                                   = start(A,C,C,A)        
        
        
* Step 5: KnowledgePropagation WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          3.  start(A,B,C,D)  -> lbl101(A,B + -1*D,C,D) [A >= 1 && C >= 1 + A && B = C && D = A]                 (?,1)
          4.  start(A,B,C,D)  -> lbl111(A,B,C,-1*B + D) [A >= 1 + C && C >= 1 && B = C && D = A]                 (?,1)
          7.  lbl101(A,B,C,D) -> lbl101(A,B + -1*D,C,D) [B >= 1 + D && A >= D && B >= 1 && D >= 1 && C >= B + D] (?,1)
          8.  lbl101(A,B,C,D) -> lbl111(A,B,C,-1*B + D) [D >= 1 + B && A >= D && B >= 1 && D >= 1 && C >= B + D] (?,1)
          10. lbl111(A,B,C,D) -> lbl101(A,B + -1*D,C,D) [B >= 1 + D && C >= B && B >= 1 && D >= 1 && A >= B + D] (?,1)
          11. lbl111(A,B,C,D) -> lbl111(A,B,C,-1*B + D) [D >= 1 + B && C >= B && B >= 1 && D >= 1 && A >= B + D] (A,1)
          13. start0(A,B,C,D) -> start(A,C,C,A)         True                                                     (1,1)
        Signature:
          {(cut,4);(lbl101,4);(lbl111,4);(lbl6,4);(start,4);(start0,4);(stop,4)}
        Flow Graph:
          [3->{7,8},4->{10,11},7->{7,8},8->{10,11},10->{7,8},11->{10,11},13->{3,4}]
        Sizebounds:
          (< 3,0,A>, A) (< 3,0,B>, A + C) (< 3,0,C>, C) (< 3,0,D>,     A) 
          (< 4,0,A>, A) (< 4,0,B>,     C) (< 4,0,C>, C) (< 4,0,D>, A + C) 
          (< 7,0,A>, A) (< 7,0,B>,     ?) (< 7,0,C>, C) (< 7,0,D>,     ?) 
          (< 8,0,A>, A) (< 8,0,B>,     ?) (< 8,0,C>, C) (< 8,0,D>,     ?) 
          (<10,0,A>, A) (<10,0,B>,     ?) (<10,0,C>, C) (<10,0,D>,     ?) 
          (<11,0,A>, A) (<11,0,B>,     ?) (<11,0,C>, C) (<11,0,D>,     ?) 
          (<13,0,A>, A) (<13,0,B>,     C) (<13,0,C>, C) (<13,0,D>,     A) 
    + Applied Processor:
        KnowledgePropagation
    + Details:
        We propagate bounds from predecessors.
* Step 6: PolyRank WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          3.  start(A,B,C,D)  -> lbl101(A,B + -1*D,C,D) [A >= 1 && C >= 1 + A && B = C && D = A]                 (1,1)
          4.  start(A,B,C,D)  -> lbl111(A,B,C,-1*B + D) [A >= 1 + C && C >= 1 && B = C && D = A]                 (1,1)
          7.  lbl101(A,B,C,D) -> lbl101(A,B + -1*D,C,D) [B >= 1 + D && A >= D && B >= 1 && D >= 1 && C >= B + D] (?,1)
          8.  lbl101(A,B,C,D) -> lbl111(A,B,C,-1*B + D) [D >= 1 + B && A >= D && B >= 1 && D >= 1 && C >= B + D] (?,1)
          10. lbl111(A,B,C,D) -> lbl101(A,B + -1*D,C,D) [B >= 1 + D && C >= B && B >= 1 && D >= 1 && A >= B + D] (?,1)
          11. lbl111(A,B,C,D) -> lbl111(A,B,C,-1*B + D) [D >= 1 + B && C >= B && B >= 1 && D >= 1 && A >= B + D] (A,1)
          13. start0(A,B,C,D) -> start(A,C,C,A)         True                                                     (1,1)
        Signature:
          {(cut,4);(lbl101,4);(lbl111,4);(lbl6,4);(start,4);(start0,4);(stop,4)}
        Flow Graph:
          [3->{7,8},4->{10,11},7->{7,8},8->{10,11},10->{7,8},11->{10,11},13->{3,4}]
        Sizebounds:
          (< 3,0,A>, A) (< 3,0,B>, A + C) (< 3,0,C>, C) (< 3,0,D>,     A) 
          (< 4,0,A>, A) (< 4,0,B>,     C) (< 4,0,C>, C) (< 4,0,D>, A + C) 
          (< 7,0,A>, A) (< 7,0,B>,     ?) (< 7,0,C>, C) (< 7,0,D>,     ?) 
          (< 8,0,A>, A) (< 8,0,B>,     ?) (< 8,0,C>, C) (< 8,0,D>,     ?) 
          (<10,0,A>, A) (<10,0,B>,     ?) (<10,0,C>, C) (<10,0,D>,     ?) 
          (<11,0,A>, A) (<11,0,B>,     ?) (<11,0,C>, C) (<11,0,D>,     ?) 
          (<13,0,A>, A) (<13,0,B>,     C) (<13,0,C>, C) (<13,0,D>,     A) 
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
          p(lbl101) = -1 + x4
          p(lbl111) = x4     
           p(start) = x4     
          p(start0) = x1     
        
        The following rules are strictly oriented:
                        [A >= 1 && C >= 1 + A && B = C && D = A] ==>                       
                                                  start(A,B,C,D)   = D                     
                                                                   > -1 + D                
                                                                   = lbl101(A,B + -1*D,C,D)
        
                        [A >= 1 + C && C >= 1 && B = C && D = A] ==>                       
                                                  start(A,B,C,D)   = D                     
                                                                   > -1*B + D              
                                                                   = lbl111(A,B,C,-1*B + D)
        
        [B >= 1 + D && C >= B && B >= 1 && D >= 1 && A >= B + D] ==>                       
                                                 lbl111(A,B,C,D)   = D                     
                                                                   > -1 + D                
                                                                   = lbl101(A,B + -1*D,C,D)
        
        [D >= 1 + B && C >= B && B >= 1 && D >= 1 && A >= B + D] ==>                       
                                                 lbl111(A,B,C,D)   = D                     
                                                                   > -1*B + D              
                                                                   = lbl111(A,B,C,-1*B + D)
        
        
        The following rules are weakly oriented:
        [B >= 1 + D && A >= D && B >= 1 && D >= 1 && C >= B + D] ==>                       
                                                 lbl101(A,B,C,D)   = -1 + D                
                                                                  >= -1 + D                
                                                                   = lbl101(A,B + -1*D,C,D)
        
        [D >= 1 + B && A >= D && B >= 1 && D >= 1 && C >= B + D] ==>                       
                                                 lbl101(A,B,C,D)   = -1 + D                
                                                                  >= -1*B + D              
                                                                   = lbl111(A,B,C,-1*B + D)
        
                                                            True ==>                       
                                                 start0(A,B,C,D)   = A                     
                                                                  >= A                     
                                                                   = start(A,C,C,A)        
        
        
* Step 7: PolyRank WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          3.  start(A,B,C,D)  -> lbl101(A,B + -1*D,C,D) [A >= 1 && C >= 1 + A && B = C && D = A]                 (1,1)
          4.  start(A,B,C,D)  -> lbl111(A,B,C,-1*B + D) [A >= 1 + C && C >= 1 && B = C && D = A]                 (1,1)
          7.  lbl101(A,B,C,D) -> lbl101(A,B + -1*D,C,D) [B >= 1 + D && A >= D && B >= 1 && D >= 1 && C >= B + D] (?,1)
          8.  lbl101(A,B,C,D) -> lbl111(A,B,C,-1*B + D) [D >= 1 + B && A >= D && B >= 1 && D >= 1 && C >= B + D] (?,1)
          10. lbl111(A,B,C,D) -> lbl101(A,B + -1*D,C,D) [B >= 1 + D && C >= B && B >= 1 && D >= 1 && A >= B + D] (A,1)
          11. lbl111(A,B,C,D) -> lbl111(A,B,C,-1*B + D) [D >= 1 + B && C >= B && B >= 1 && D >= 1 && A >= B + D] (A,1)
          13. start0(A,B,C,D) -> start(A,C,C,A)         True                                                     (1,1)
        Signature:
          {(cut,4);(lbl101,4);(lbl111,4);(lbl6,4);(start,4);(start0,4);(stop,4)}
        Flow Graph:
          [3->{7,8},4->{10,11},7->{7,8},8->{10,11},10->{7,8},11->{10,11},13->{3,4}]
        Sizebounds:
          (< 3,0,A>, A) (< 3,0,B>, A + C) (< 3,0,C>, C) (< 3,0,D>,     A) 
          (< 4,0,A>, A) (< 4,0,B>,     C) (< 4,0,C>, C) (< 4,0,D>, A + C) 
          (< 7,0,A>, A) (< 7,0,B>,     ?) (< 7,0,C>, C) (< 7,0,D>,     ?) 
          (< 8,0,A>, A) (< 8,0,B>,     ?) (< 8,0,C>, C) (< 8,0,D>,     ?) 
          (<10,0,A>, A) (<10,0,B>,     ?) (<10,0,C>, C) (<10,0,D>,     ?) 
          (<11,0,A>, A) (<11,0,B>,     ?) (<11,0,C>, C) (<11,0,D>,     ?) 
          (<13,0,A>, A) (<13,0,B>,     C) (<13,0,C>, C) (<13,0,D>,     A) 
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
          p(lbl101) = x2     
          p(lbl111) = -1 + x2
           p(start) = x3     
          p(start0) = x3     
        
        The following rules are strictly oriented:
                        [A >= 1 + C && C >= 1 && B = C && D = A] ==>                       
                                                  start(A,B,C,D)   = C                     
                                                                   > -1 + B                
                                                                   = lbl111(A,B,C,-1*B + D)
        
        [D >= 1 + B && A >= D && B >= 1 && D >= 1 && C >= B + D] ==>                       
                                                 lbl101(A,B,C,D)   = B                     
                                                                   > -1 + B                
                                                                   = lbl111(A,B,C,-1*B + D)
        
        
        The following rules are weakly oriented:
                        [A >= 1 && C >= 1 + A && B = C && D = A] ==>                       
                                                  start(A,B,C,D)   = C                     
                                                                  >= B + -1*D              
                                                                   = lbl101(A,B + -1*D,C,D)
        
        [B >= 1 + D && A >= D && B >= 1 && D >= 1 && C >= B + D] ==>                       
                                                 lbl101(A,B,C,D)   = B                     
                                                                  >= B + -1*D              
                                                                   = lbl101(A,B + -1*D,C,D)
        
        [B >= 1 + D && C >= B && B >= 1 && D >= 1 && A >= B + D] ==>                       
                                                 lbl111(A,B,C,D)   = -1 + B                
                                                                  >= B + -1*D              
                                                                   = lbl101(A,B + -1*D,C,D)
        
        [D >= 1 + B && C >= B && B >= 1 && D >= 1 && A >= B + D] ==>                       
                                                 lbl111(A,B,C,D)   = -1 + B                
                                                                  >= -1 + B                
                                                                   = lbl111(A,B,C,-1*B + D)
        
                                                            True ==>                       
                                                 start0(A,B,C,D)   = C                     
                                                                  >= C                     
                                                                   = start(A,C,C,A)        
        
        
* Step 8: PolyRank WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          3.  start(A,B,C,D)  -> lbl101(A,B + -1*D,C,D) [A >= 1 && C >= 1 + A && B = C && D = A]                 (1,1)
          4.  start(A,B,C,D)  -> lbl111(A,B,C,-1*B + D) [A >= 1 + C && C >= 1 && B = C && D = A]                 (1,1)
          7.  lbl101(A,B,C,D) -> lbl101(A,B + -1*D,C,D) [B >= 1 + D && A >= D && B >= 1 && D >= 1 && C >= B + D] (?,1)
          8.  lbl101(A,B,C,D) -> lbl111(A,B,C,-1*B + D) [D >= 1 + B && A >= D && B >= 1 && D >= 1 && C >= B + D] (C,1)
          10. lbl111(A,B,C,D) -> lbl101(A,B + -1*D,C,D) [B >= 1 + D && C >= B && B >= 1 && D >= 1 && A >= B + D] (A,1)
          11. lbl111(A,B,C,D) -> lbl111(A,B,C,-1*B + D) [D >= 1 + B && C >= B && B >= 1 && D >= 1 && A >= B + D] (A,1)
          13. start0(A,B,C,D) -> start(A,C,C,A)         True                                                     (1,1)
        Signature:
          {(cut,4);(lbl101,4);(lbl111,4);(lbl6,4);(start,4);(start0,4);(stop,4)}
        Flow Graph:
          [3->{7,8},4->{10,11},7->{7,8},8->{10,11},10->{7,8},11->{10,11},13->{3,4}]
        Sizebounds:
          (< 3,0,A>, A) (< 3,0,B>, A + C) (< 3,0,C>, C) (< 3,0,D>,     A) 
          (< 4,0,A>, A) (< 4,0,B>,     C) (< 4,0,C>, C) (< 4,0,D>, A + C) 
          (< 7,0,A>, A) (< 7,0,B>,     ?) (< 7,0,C>, C) (< 7,0,D>,     ?) 
          (< 8,0,A>, A) (< 8,0,B>,     ?) (< 8,0,C>, C) (< 8,0,D>,     ?) 
          (<10,0,A>, A) (<10,0,B>,     ?) (<10,0,C>, C) (<10,0,D>,     ?) 
          (<11,0,A>, A) (<11,0,B>,     ?) (<11,0,C>, C) (<11,0,D>,     ?) 
          (<13,0,A>, A) (<13,0,B>,     C) (<13,0,C>, C) (<13,0,D>,     A) 
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
          p(lbl101) = x2
          p(lbl111) = x2
           p(start) = x2
          p(start0) = x3
        
        The following rules are strictly oriented:
                        [A >= 1 && C >= 1 + A && B = C && D = A] ==>                       
                                                  start(A,B,C,D)   = B                     
                                                                   > B + -1*D              
                                                                   = lbl101(A,B + -1*D,C,D)
        
        [B >= 1 + D && A >= D && B >= 1 && D >= 1 && C >= B + D] ==>                       
                                                 lbl101(A,B,C,D)   = B                     
                                                                   > B + -1*D              
                                                                   = lbl101(A,B + -1*D,C,D)
        
        [B >= 1 + D && C >= B && B >= 1 && D >= 1 && A >= B + D] ==>                       
                                                 lbl111(A,B,C,D)   = B                     
                                                                   > B + -1*D              
                                                                   = lbl101(A,B + -1*D,C,D)
        
        
        The following rules are weakly oriented:
                        [A >= 1 + C && C >= 1 && B = C && D = A] ==>                       
                                                  start(A,B,C,D)   = B                     
                                                                  >= B                     
                                                                   = lbl111(A,B,C,-1*B + D)
        
        [D >= 1 + B && A >= D && B >= 1 && D >= 1 && C >= B + D] ==>                       
                                                 lbl101(A,B,C,D)   = B                     
                                                                  >= B                     
                                                                   = lbl111(A,B,C,-1*B + D)
        
        [D >= 1 + B && C >= B && B >= 1 && D >= 1 && A >= B + D] ==>                       
                                                 lbl111(A,B,C,D)   = B                     
                                                                  >= B                     
                                                                   = lbl111(A,B,C,-1*B + D)
        
                                                            True ==>                       
                                                 start0(A,B,C,D)   = C                     
                                                                  >= C                     
                                                                   = start(A,C,C,A)        
        
        
* Step 9: KnowledgePropagation WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          3.  start(A,B,C,D)  -> lbl101(A,B + -1*D,C,D) [A >= 1 && C >= 1 + A && B = C && D = A]                 (1,1)
          4.  start(A,B,C,D)  -> lbl111(A,B,C,-1*B + D) [A >= 1 + C && C >= 1 && B = C && D = A]                 (1,1)
          7.  lbl101(A,B,C,D) -> lbl101(A,B + -1*D,C,D) [B >= 1 + D && A >= D && B >= 1 && D >= 1 && C >= B + D] (C,1)
          8.  lbl101(A,B,C,D) -> lbl111(A,B,C,-1*B + D) [D >= 1 + B && A >= D && B >= 1 && D >= 1 && C >= B + D] (C,1)
          10. lbl111(A,B,C,D) -> lbl101(A,B + -1*D,C,D) [B >= 1 + D && C >= B && B >= 1 && D >= 1 && A >= B + D] (A,1)
          11. lbl111(A,B,C,D) -> lbl111(A,B,C,-1*B + D) [D >= 1 + B && C >= B && B >= 1 && D >= 1 && A >= B + D] (A,1)
          13. start0(A,B,C,D) -> start(A,C,C,A)         True                                                     (1,1)
        Signature:
          {(cut,4);(lbl101,4);(lbl111,4);(lbl6,4);(start,4);(start0,4);(stop,4)}
        Flow Graph:
          [3->{7,8},4->{10,11},7->{7,8},8->{10,11},10->{7,8},11->{10,11},13->{3,4}]
        Sizebounds:
          (< 3,0,A>, A) (< 3,0,B>, A + C) (< 3,0,C>, C) (< 3,0,D>,     A) 
          (< 4,0,A>, A) (< 4,0,B>,     C) (< 4,0,C>, C) (< 4,0,D>, A + C) 
          (< 7,0,A>, A) (< 7,0,B>,     ?) (< 7,0,C>, C) (< 7,0,D>,     ?) 
          (< 8,0,A>, A) (< 8,0,B>,     ?) (< 8,0,C>, C) (< 8,0,D>,     ?) 
          (<10,0,A>, A) (<10,0,B>,     ?) (<10,0,C>, C) (<10,0,D>,     ?) 
          (<11,0,A>, A) (<11,0,B>,     ?) (<11,0,C>, C) (<11,0,D>,     ?) 
          (<13,0,A>, A) (<13,0,B>,     C) (<13,0,C>, C) (<13,0,D>,     A) 
    + Applied Processor:
        KnowledgePropagation
    + Details:
        The problem is already solved.

WORST_CASE(?,O(n^1))