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

WORST_CASE(?,O(n^3))