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

WORST_CASE(?,O(n^2))