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))