WORST_CASE(?,O(n^1))
* Step 1: UnsatRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. start(A,B,C,D,E,F,G,H) -> stop(A,B,C,D,E,F,G,H) [A >= 5 && B = C && D = E && F = G && H = A] (?,1)
1. start(A,B,C,D,E,F,G,H) -> lbl92(A,B,C,H,E,0,G,1 + H) [2 >= A && B = C && D = E && F = G && H = A] (?,1)
2. start(A,B,C,D,E,F,G,H) -> lbl82(A,0,C,D,E,1,G,H) [A >= 3 && 4 >= A && B = C && D = E && F = G && H = A] (?,1)
3. lbl92(A,B,C,D,E,F,G,H) -> stop(A,B,C,D,E,F,G,H) [D >= 4 && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] (?,1)
4. lbl92(A,B,C,D,E,F,G,H) -> lbl92(A,B,C,H,E,0,G,1 + H) [1 >= D && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] (?,1)
5. lbl92(A,B,C,D,E,F,G,H) -> lbl82(A,0,C,D,E,1,G,H) [D >= 2 && 3 >= D && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] (?,1)
6. lbl82(A,B,C,D,E,F,G,H) -> lbl92(A,B,C,H,E,F,G,1 + H) [2 >= H && 9 >= B && B >= 0 && H >= A && H >= 3 && 4 >= H && F = 1 + B] (?,1)
7. lbl82(A,B,C,D,E,F,G,H) -> lbl92(A,B,C,H,E,F,G,1 + H) [H >= A && H >= 3 && 4 >= H && F = 10 && B = 9] (?,1)
8. lbl82(A,B,C,D,E,F,G,H) -> lbl82(A,F,C,D,E,1 + F,G,H) [H >= 3 && 8 >= B && 9 >= B && B >= 0 && H >= A && 4 >= H && F = 1 + B] (?,1)
9. start0(A,B,C,D,E,F,G,H) -> start(A,C,C,E,E,G,G,A) True (1,1)
Signature:
{(lbl82,8);(lbl92,8);(start,8);(start0,8);(stop,8)}
Flow Graph:
[0->{},1->{3,4,5},2->{6,7,8},3->{},4->{3,4,5},5->{6,7,8},6->{3,4,5},7->{3,4,5},8->{6,7,8},9->{0,1,2}]
+ Applied Processor:
UnsatRules
+ Details:
The following transitions have unsatisfiable constraints and are removed: [6]
* Step 2: LocalSizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. start(A,B,C,D,E,F,G,H) -> stop(A,B,C,D,E,F,G,H) [A >= 5 && B = C && D = E && F = G && H = A] (?,1)
1. start(A,B,C,D,E,F,G,H) -> lbl92(A,B,C,H,E,0,G,1 + H) [2 >= A && B = C && D = E && F = G && H = A] (?,1)
2. start(A,B,C,D,E,F,G,H) -> lbl82(A,0,C,D,E,1,G,H) [A >= 3 && 4 >= A && B = C && D = E && F = G && H = A] (?,1)
3. lbl92(A,B,C,D,E,F,G,H) -> stop(A,B,C,D,E,F,G,H) [D >= 4 && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] (?,1)
4. lbl92(A,B,C,D,E,F,G,H) -> lbl92(A,B,C,H,E,0,G,1 + H) [1 >= D && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] (?,1)
5. lbl92(A,B,C,D,E,F,G,H) -> lbl82(A,0,C,D,E,1,G,H) [D >= 2 && 3 >= D && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] (?,1)
7. lbl82(A,B,C,D,E,F,G,H) -> lbl92(A,B,C,H,E,F,G,1 + H) [H >= A && H >= 3 && 4 >= H && F = 10 && B = 9] (?,1)
8. lbl82(A,B,C,D,E,F,G,H) -> lbl82(A,F,C,D,E,1 + F,G,H) [H >= 3 && 8 >= B && 9 >= B && B >= 0 && H >= A && 4 >= H && F = 1 + B] (?,1)
9. start0(A,B,C,D,E,F,G,H) -> start(A,C,C,E,E,G,G,A) True (1,1)
Signature:
{(lbl82,8);(lbl92,8);(start,8);(start0,8);(stop,8)}
Flow Graph:
[0->{},1->{3,4,5},2->{7,8},3->{},4->{3,4,5},5->{7,8},7->{3,4,5},8->{7,8},9->{0,1,2}]
+ Applied Processor:
LocalSizeboundsProc
+ Details:
LocalSizebounds generated; rvgraph
(<0,0,A>, A, .= 0) (<0,0,B>, B, .= 0) (<0,0,C>, C, .= 0) (<0,0,D>, 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>, B, .= 0) (<1,0,C>, C, .= 0) (<1,0,D>, H, .= 0) (<1,0,E>, E, .= 0) (<1,0,F>, 0, .= 0) (<1,0,G>, G, .= 0) (<1,0,H>, 1 + H, .+ 1)
(<2,0,A>, A, .= 0) (<2,0,B>, 0, .= 0) (<2,0,C>, C, .= 0) (<2,0,D>, D, .= 0) (<2,0,E>, E, .= 0) (<2,0,F>, 1, .= 1) (<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>, D, .= 0) (<3,0,E>, E, .= 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>, H, .= 0) (<4,0,E>, E, .= 0) (<4,0,F>, 0, .= 0) (<4,0,G>, G, .= 0) (<4,0,H>, 1 + H, .+ 1)
(<5,0,A>, A, .= 0) (<5,0,B>, 0, .= 0) (<5,0,C>, C, .= 0) (<5,0,D>, D, .= 0) (<5,0,E>, E, .= 0) (<5,0,F>, 1, .= 1) (<5,0,G>, G, .= 0) (<5,0,H>, H, .= 0)
(<7,0,A>, A, .= 0) (<7,0,B>, B, .= 0) (<7,0,C>, C, .= 0) (<7,0,D>, H, .= 0) (<7,0,E>, E, .= 0) (<7,0,F>, F, .= 0) (<7,0,G>, G, .= 0) (<7,0,H>, 5, .= 5)
(<8,0,A>, A, .= 0) (<8,0,B>, F, .= 0) (<8,0,C>, C, .= 0) (<8,0,D>, D, .= 0) (<8,0,E>, E, .= 0) (<8,0,F>, 11, .= 11) (<8,0,G>, G, .= 0) (<8,0,H>, H, .= 0)
(<9,0,A>, A, .= 0) (<9,0,B>, C, .= 0) (<9,0,C>, C, .= 0) (<9,0,D>, E, .= 0) (<9,0,E>, E, .= 0) (<9,0,F>, G, .= 0) (<9,0,G>, G, .= 0) (<9,0,H>, A, .= 0)
* Step 3: SizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. start(A,B,C,D,E,F,G,H) -> stop(A,B,C,D,E,F,G,H) [A >= 5 && B = C && D = E && F = G && H = A] (?,1)
1. start(A,B,C,D,E,F,G,H) -> lbl92(A,B,C,H,E,0,G,1 + H) [2 >= A && B = C && D = E && F = G && H = A] (?,1)
2. start(A,B,C,D,E,F,G,H) -> lbl82(A,0,C,D,E,1,G,H) [A >= 3 && 4 >= A && B = C && D = E && F = G && H = A] (?,1)
3. lbl92(A,B,C,D,E,F,G,H) -> stop(A,B,C,D,E,F,G,H) [D >= 4 && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] (?,1)
4. lbl92(A,B,C,D,E,F,G,H) -> lbl92(A,B,C,H,E,0,G,1 + H) [1 >= D && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] (?,1)
5. lbl92(A,B,C,D,E,F,G,H) -> lbl82(A,0,C,D,E,1,G,H) [D >= 2 && 3 >= D && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] (?,1)
7. lbl82(A,B,C,D,E,F,G,H) -> lbl92(A,B,C,H,E,F,G,1 + H) [H >= A && H >= 3 && 4 >= H && F = 10 && B = 9] (?,1)
8. lbl82(A,B,C,D,E,F,G,H) -> lbl82(A,F,C,D,E,1 + F,G,H) [H >= 3 && 8 >= B && 9 >= B && B >= 0 && H >= A && 4 >= H && F = 1 + B] (?,1)
9. start0(A,B,C,D,E,F,G,H) -> start(A,C,C,E,E,G,G,A) True (1,1)
Signature:
{(lbl82,8);(lbl92,8);(start,8);(start0,8);(stop,8)}
Flow Graph:
[0->{},1->{3,4,5},2->{7,8},3->{},4->{3,4,5},5->{7,8},7->{3,4,5},8->{7,8},9->{0,1,2}]
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>, ?)
(<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>, ?)
+ 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>, C) (<1,0,C>, C) (<1,0,D>, A) (<1,0,E>, E) (<1,0,F>, 0) (<1,0,G>, G) (<1,0,H>, 1 + A)
(<2,0,A>, A) (<2,0,B>, 0) (<2,0,C>, C) (<2,0,D>, E) (<2,0,E>, E) (<2,0,F>, 1) (<2,0,G>, G) (<2,0,H>, A)
(<3,0,A>, A) (<3,0,B>, 11 + C) (<3,0,C>, C) (<3,0,D>, ?) (<3,0,E>, E) (<3,0,F>, 11) (<3,0,G>, G) (<3,0,H>, ?)
(<4,0,A>, A) (<4,0,B>, 11 + C) (<4,0,C>, C) (<4,0,D>, ?) (<4,0,E>, E) (<4,0,F>, 0) (<4,0,G>, G) (<4,0,H>, ?)
(<5,0,A>, A) (<5,0,B>, 0) (<5,0,C>, C) (<5,0,D>, ?) (<5,0,E>, E) (<5,0,F>, 1) (<5,0,G>, G) (<5,0,H>, ?)
(<7,0,A>, A) (<7,0,B>, 11) (<7,0,C>, C) (<7,0,D>, ?) (<7,0,E>, E) (<7,0,F>, 11) (<7,0,G>, G) (<7,0,H>, 5)
(<8,0,A>, A) (<8,0,B>, 11) (<8,0,C>, C) (<8,0,D>, ?) (<8,0,E>, E) (<8,0,F>, 11) (<8,0,G>, G) (<8,0,H>, 4)
(<9,0,A>, A) (<9,0,B>, C) (<9,0,C>, C) (<9,0,D>, E) (<9,0,E>, E) (<9,0,F>, G) (<9,0,G>, G) (<9,0,H>, A)
* Step 4: ChainProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. start(A,B,C,D,E,F,G,H) -> stop(A,B,C,D,E,F,G,H) [A >= 5 && B = C && D = E && F = G && H = A] (?,1)
1. start(A,B,C,D,E,F,G,H) -> lbl92(A,B,C,H,E,0,G,1 + H) [2 >= A && B = C && D = E && F = G && H = A] (?,1)
2. start(A,B,C,D,E,F,G,H) -> lbl82(A,0,C,D,E,1,G,H) [A >= 3 && 4 >= A && B = C && D = E && F = G && H = A] (?,1)
3. lbl92(A,B,C,D,E,F,G,H) -> stop(A,B,C,D,E,F,G,H) [D >= 4 && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] (?,1)
4. lbl92(A,B,C,D,E,F,G,H) -> lbl92(A,B,C,H,E,0,G,1 + H) [1 >= D && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] (?,1)
5. lbl92(A,B,C,D,E,F,G,H) -> lbl82(A,0,C,D,E,1,G,H) [D >= 2 && 3 >= D && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] (?,1)
7. lbl82(A,B,C,D,E,F,G,H) -> lbl92(A,B,C,H,E,F,G,1 + H) [H >= A && H >= 3 && 4 >= H && F = 10 && B = 9] (?,1)
8. lbl82(A,B,C,D,E,F,G,H) -> lbl82(A,F,C,D,E,1 + F,G,H) [H >= 3 && 8 >= B && 9 >= B && B >= 0 && H >= A && 4 >= H && F = 1 + B] (?,1)
9. start0(A,B,C,D,E,F,G,H) -> start(A,C,C,E,E,G,G,A) True (1,1)
Signature:
{(lbl82,8);(lbl92,8);(start,8);(start0,8);(stop,8)}
Flow Graph:
[0->{},1->{3,4,5},2->{7,8},3->{},4->{3,4,5},5->{7,8},7->{3,4,5},8->{7,8},9->{0,1,2}]
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>, C) (<1,0,C>, C) (<1,0,D>, A) (<1,0,E>, E) (<1,0,F>, 0) (<1,0,G>, G) (<1,0,H>, 1 + A)
(<2,0,A>, A) (<2,0,B>, 0) (<2,0,C>, C) (<2,0,D>, E) (<2,0,E>, E) (<2,0,F>, 1) (<2,0,G>, G) (<2,0,H>, A)
(<3,0,A>, A) (<3,0,B>, 11 + C) (<3,0,C>, C) (<3,0,D>, ?) (<3,0,E>, E) (<3,0,F>, 11) (<3,0,G>, G) (<3,0,H>, ?)
(<4,0,A>, A) (<4,0,B>, 11 + C) (<4,0,C>, C) (<4,0,D>, ?) (<4,0,E>, E) (<4,0,F>, 0) (<4,0,G>, G) (<4,0,H>, ?)
(<5,0,A>, A) (<5,0,B>, 0) (<5,0,C>, C) (<5,0,D>, ?) (<5,0,E>, E) (<5,0,F>, 1) (<5,0,G>, G) (<5,0,H>, ?)
(<7,0,A>, A) (<7,0,B>, 11) (<7,0,C>, C) (<7,0,D>, ?) (<7,0,E>, E) (<7,0,F>, 11) (<7,0,G>, G) (<7,0,H>, 5)
(<8,0,A>, A) (<8,0,B>, 11) (<8,0,C>, C) (<8,0,D>, ?) (<8,0,E>, E) (<8,0,F>, 11) (<8,0,G>, G) (<8,0,H>, 4)
(<9,0,A>, A) (<9,0,B>, C) (<9,0,C>, C) (<9,0,D>, E) (<9,0,E>, E) (<9,0,F>, G) (<9,0,G>, G) (<9,0,H>, A)
+ Applied Processor:
ChainProcessor False [0,1,2,3,4,5,7,8,9]
+ Details:
We chained rule 9 to obtain the rules [10,11,12] .
* Step 5: UnreachableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. start(A,B,C,D,E,F,G,H) -> stop(A,B,C,D,E,F,G,H) [A >= 5 && B = C && D = E && F = G && H = A] (?,1)
1. start(A,B,C,D,E,F,G,H) -> lbl92(A,B,C,H,E,0,G,1 + H) [2 >= A && B = C && D = E && F = G && H = A] (?,1)
2. start(A,B,C,D,E,F,G,H) -> lbl82(A,0,C,D,E,1,G,H) [A >= 3 && 4 >= A && B = C && D = E && F = G && H = A] (?,1)
3. lbl92(A,B,C,D,E,F,G,H) -> stop(A,B,C,D,E,F,G,H) [D >= 4 && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] (?,1)
4. lbl92(A,B,C,D,E,F,G,H) -> lbl92(A,B,C,H,E,0,G,1 + H) [1 >= D && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] (?,1)
5. lbl92(A,B,C,D,E,F,G,H) -> lbl82(A,0,C,D,E,1,G,H) [D >= 2 && 3 >= D && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] (?,1)
7. lbl82(A,B,C,D,E,F,G,H) -> lbl92(A,B,C,H,E,F,G,1 + H) [H >= A && H >= 3 && 4 >= H && F = 10 && B = 9] (?,1)
8. lbl82(A,B,C,D,E,F,G,H) -> lbl82(A,F,C,D,E,1 + F,G,H) [H >= 3 && 8 >= B && 9 >= B && B >= 0 && H >= A && 4 >= H && F = 1 + B] (?,1)
10. start0(A,B,C,D,E,F,G,H) -> stop(A,C,C,E,E,G,G,A) [A >= 5 && C = C && E = E && G = G && A = A] (1,2)
11. start0(A,B,C,D,E,F,G,H) -> lbl92(A,C,C,A,E,0,G,1 + A) [2 >= A && C = C && E = E && G = G && A = A] (1,2)
12. start0(A,B,C,D,E,F,G,H) -> lbl82(A,0,C,E,E,1,G,A) [A >= 3 && 4 >= A && C = C && E = E && G = G && A = A] (1,2)
Signature:
{(lbl82,8);(lbl92,8);(start,8);(start0,8);(stop,8)}
Flow Graph:
[0->{},1->{3,4,5},2->{7,8},3->{},4->{3,4,5},5->{7,8},7->{3,4,5},8->{7,8},10->{},11->{3,4,5},12->{7,8}]
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>, C) (< 1,0,C>, C) (< 1,0,D>, A) (< 1,0,E>, E) (< 1,0,F>, 0) (< 1,0,G>, G) (< 1,0,H>, 1 + A)
(< 2,0,A>, A) (< 2,0,B>, 0) (< 2,0,C>, C) (< 2,0,D>, E) (< 2,0,E>, E) (< 2,0,F>, 1) (< 2,0,G>, G) (< 2,0,H>, A)
(< 3,0,A>, A) (< 3,0,B>, 11 + C) (< 3,0,C>, C) (< 3,0,D>, ?) (< 3,0,E>, E) (< 3,0,F>, 11) (< 3,0,G>, G) (< 3,0,H>, ?)
(< 4,0,A>, A) (< 4,0,B>, 11 + C) (< 4,0,C>, C) (< 4,0,D>, ?) (< 4,0,E>, E) (< 4,0,F>, 0) (< 4,0,G>, G) (< 4,0,H>, ?)
(< 5,0,A>, A) (< 5,0,B>, 0) (< 5,0,C>, C) (< 5,0,D>, ?) (< 5,0,E>, E) (< 5,0,F>, 1) (< 5,0,G>, G) (< 5,0,H>, ?)
(< 7,0,A>, A) (< 7,0,B>, 11) (< 7,0,C>, C) (< 7,0,D>, ?) (< 7,0,E>, E) (< 7,0,F>, 11) (< 7,0,G>, G) (< 7,0,H>, 5)
(< 8,0,A>, A) (< 8,0,B>, 11) (< 8,0,C>, C) (< 8,0,D>, ?) (< 8,0,E>, E) (< 8,0,F>, 11) (< 8,0,G>, G) (< 8,0,H>, 4)
(<10,0,A>, A) (<10,0,B>, C) (<10,0,C>, C) (<10,0,D>, E) (<10,0,E>, E) (<10,0,F>, G) (<10,0,G>, G) (<10,0,H>, A)
(<11,0,A>, A) (<11,0,B>, C) (<11,0,C>, C) (<11,0,D>, A) (<11,0,E>, E) (<11,0,F>, 0) (<11,0,G>, G) (<11,0,H>, 1 + A)
(<12,0,A>, A) (<12,0,B>, 0) (<12,0,C>, C) (<12,0,D>, E) (<12,0,E>, E) (<12,0,F>, 1) (<12,0,G>, G) (<12,0,H>, A)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [0,1,2]
* Step 6: UnsatPaths WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
3. lbl92(A,B,C,D,E,F,G,H) -> stop(A,B,C,D,E,F,G,H) [D >= 4 && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] (?,1)
4. lbl92(A,B,C,D,E,F,G,H) -> lbl92(A,B,C,H,E,0,G,1 + H) [1 >= D && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] (?,1)
5. lbl92(A,B,C,D,E,F,G,H) -> lbl82(A,0,C,D,E,1,G,H) [D >= 2 && 3 >= D && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] (?,1)
7. lbl82(A,B,C,D,E,F,G,H) -> lbl92(A,B,C,H,E,F,G,1 + H) [H >= A && H >= 3 && 4 >= H && F = 10 && B = 9] (?,1)
8. lbl82(A,B,C,D,E,F,G,H) -> lbl82(A,F,C,D,E,1 + F,G,H) [H >= 3 && 8 >= B && 9 >= B && B >= 0 && H >= A && 4 >= H && F = 1 + B] (?,1)
10. start0(A,B,C,D,E,F,G,H) -> stop(A,C,C,E,E,G,G,A) [A >= 5 && C = C && E = E && G = G && A = A] (1,2)
11. start0(A,B,C,D,E,F,G,H) -> lbl92(A,C,C,A,E,0,G,1 + A) [2 >= A && C = C && E = E && G = G && A = A] (1,2)
12. start0(A,B,C,D,E,F,G,H) -> lbl82(A,0,C,E,E,1,G,A) [A >= 3 && 4 >= A && C = C && E = E && G = G && A = A] (1,2)
Signature:
{(lbl82,8);(lbl92,8);(start,8);(start0,8);(stop,8)}
Flow Graph:
[3->{},4->{3,4,5},5->{7,8},7->{3,4,5},8->{7,8},10->{},11->{3,4,5},12->{7,8}]
Sizebounds:
(< 3,0,A>, A) (< 3,0,B>, 11 + C) (< 3,0,C>, C) (< 3,0,D>, ?) (< 3,0,E>, E) (< 3,0,F>, 11) (< 3,0,G>, G) (< 3,0,H>, ?)
(< 4,0,A>, A) (< 4,0,B>, 11 + C) (< 4,0,C>, C) (< 4,0,D>, ?) (< 4,0,E>, E) (< 4,0,F>, 0) (< 4,0,G>, G) (< 4,0,H>, ?)
(< 5,0,A>, A) (< 5,0,B>, 0) (< 5,0,C>, C) (< 5,0,D>, ?) (< 5,0,E>, E) (< 5,0,F>, 1) (< 5,0,G>, G) (< 5,0,H>, ?)
(< 7,0,A>, A) (< 7,0,B>, 11) (< 7,0,C>, C) (< 7,0,D>, ?) (< 7,0,E>, E) (< 7,0,F>, 11) (< 7,0,G>, G) (< 7,0,H>, 5)
(< 8,0,A>, A) (< 8,0,B>, 11) (< 8,0,C>, C) (< 8,0,D>, ?) (< 8,0,E>, E) (< 8,0,F>, 11) (< 8,0,G>, G) (< 8,0,H>, 4)
(<10,0,A>, A) (<10,0,B>, C) (<10,0,C>, C) (<10,0,D>, E) (<10,0,E>, E) (<10,0,F>, G) (<10,0,G>, G) (<10,0,H>, A)
(<11,0,A>, A) (<11,0,B>, C) (<11,0,C>, C) (<11,0,D>, A) (<11,0,E>, E) (<11,0,F>, 0) (<11,0,G>, G) (<11,0,H>, 1 + A)
(<12,0,A>, A) (<12,0,B>, 0) (<12,0,C>, C) (<12,0,D>, E) (<12,0,E>, E) (<12,0,F>, 1) (<12,0,G>, G) (<12,0,H>, A)
+ Applied Processor:
UnsatPaths
+ Details:
We remove following edges from the transition graph: [(4,3),(5,7),(7,4),(11,3),(12,7)]
* Step 7: LeafRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
3. lbl92(A,B,C,D,E,F,G,H) -> stop(A,B,C,D,E,F,G,H) [D >= 4 && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] (?,1)
4. lbl92(A,B,C,D,E,F,G,H) -> lbl92(A,B,C,H,E,0,G,1 + H) [1 >= D && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] (?,1)
5. lbl92(A,B,C,D,E,F,G,H) -> lbl82(A,0,C,D,E,1,G,H) [D >= 2 && 3 >= D && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] (?,1)
7. lbl82(A,B,C,D,E,F,G,H) -> lbl92(A,B,C,H,E,F,G,1 + H) [H >= A && H >= 3 && 4 >= H && F = 10 && B = 9] (?,1)
8. lbl82(A,B,C,D,E,F,G,H) -> lbl82(A,F,C,D,E,1 + F,G,H) [H >= 3 && 8 >= B && 9 >= B && B >= 0 && H >= A && 4 >= H && F = 1 + B] (?,1)
10. start0(A,B,C,D,E,F,G,H) -> stop(A,C,C,E,E,G,G,A) [A >= 5 && C = C && E = E && G = G && A = A] (1,2)
11. start0(A,B,C,D,E,F,G,H) -> lbl92(A,C,C,A,E,0,G,1 + A) [2 >= A && C = C && E = E && G = G && A = A] (1,2)
12. start0(A,B,C,D,E,F,G,H) -> lbl82(A,0,C,E,E,1,G,A) [A >= 3 && 4 >= A && C = C && E = E && G = G && A = A] (1,2)
Signature:
{(lbl82,8);(lbl92,8);(start,8);(start0,8);(stop,8)}
Flow Graph:
[3->{},4->{4,5},5->{8},7->{3,5},8->{7,8},10->{},11->{4,5},12->{8}]
Sizebounds:
(< 3,0,A>, A) (< 3,0,B>, 11 + C) (< 3,0,C>, C) (< 3,0,D>, ?) (< 3,0,E>, E) (< 3,0,F>, 11) (< 3,0,G>, G) (< 3,0,H>, ?)
(< 4,0,A>, A) (< 4,0,B>, 11 + C) (< 4,0,C>, C) (< 4,0,D>, ?) (< 4,0,E>, E) (< 4,0,F>, 0) (< 4,0,G>, G) (< 4,0,H>, ?)
(< 5,0,A>, A) (< 5,0,B>, 0) (< 5,0,C>, C) (< 5,0,D>, ?) (< 5,0,E>, E) (< 5,0,F>, 1) (< 5,0,G>, G) (< 5,0,H>, ?)
(< 7,0,A>, A) (< 7,0,B>, 11) (< 7,0,C>, C) (< 7,0,D>, ?) (< 7,0,E>, E) (< 7,0,F>, 11) (< 7,0,G>, G) (< 7,0,H>, 5)
(< 8,0,A>, A) (< 8,0,B>, 11) (< 8,0,C>, C) (< 8,0,D>, ?) (< 8,0,E>, E) (< 8,0,F>, 11) (< 8,0,G>, G) (< 8,0,H>, 4)
(<10,0,A>, A) (<10,0,B>, C) (<10,0,C>, C) (<10,0,D>, E) (<10,0,E>, E) (<10,0,F>, G) (<10,0,G>, G) (<10,0,H>, A)
(<11,0,A>, A) (<11,0,B>, C) (<11,0,C>, C) (<11,0,D>, A) (<11,0,E>, E) (<11,0,F>, 0) (<11,0,G>, G) (<11,0,H>, 1 + A)
(<12,0,A>, A) (<12,0,B>, 0) (<12,0,C>, C) (<12,0,D>, E) (<12,0,E>, E) (<12,0,F>, 1) (<12,0,G>, G) (<12,0,H>, A)
+ Applied Processor:
LeafRules
+ Details:
The following transitions are estimated by its predecessors and are removed [3]
* Step 8: LocalSizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
4. lbl92(A,B,C,D,E,F,G,H) -> lbl92(A,B,C,H,E,0,G,1 + H) [1 >= D && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] (?,1)
5. lbl92(A,B,C,D,E,F,G,H) -> lbl82(A,0,C,D,E,1,G,H) [D >= 2 && 3 >= D && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] (?,1)
7. lbl82(A,B,C,D,E,F,G,H) -> lbl92(A,B,C,H,E,F,G,1 + H) [H >= A && H >= 3 && 4 >= H && F = 10 && B = 9] (?,1)
8. lbl82(A,B,C,D,E,F,G,H) -> lbl82(A,F,C,D,E,1 + F,G,H) [H >= 3 && 8 >= B && 9 >= B && B >= 0 && H >= A && 4 >= H && F = 1 + B] (?,1)
10. start0(A,B,C,D,E,F,G,H) -> stop(A,C,C,E,E,G,G,A) [A >= 5 && C = C && E = E && G = G && A = A] (1,2)
11. start0(A,B,C,D,E,F,G,H) -> lbl92(A,C,C,A,E,0,G,1 + A) [2 >= A && C = C && E = E && G = G && A = A] (1,2)
12. start0(A,B,C,D,E,F,G,H) -> lbl82(A,0,C,E,E,1,G,A) [A >= 3 && 4 >= A && C = C && E = E && G = G && A = A] (1,2)
Signature:
{(lbl82,8);(lbl92,8);(start,8);(start0,8);(stop,8)}
Flow Graph:
[4->{4,5},5->{8},7->{5},8->{7,8},10->{},11->{4,5},12->{8}]
Sizebounds:
(< 4,0,A>, A) (< 4,0,B>, 11 + C) (< 4,0,C>, C) (< 4,0,D>, ?) (< 4,0,E>, E) (< 4,0,F>, 0) (< 4,0,G>, G) (< 4,0,H>, ?)
(< 5,0,A>, A) (< 5,0,B>, 0) (< 5,0,C>, C) (< 5,0,D>, ?) (< 5,0,E>, E) (< 5,0,F>, 1) (< 5,0,G>, G) (< 5,0,H>, ?)
(< 7,0,A>, A) (< 7,0,B>, 11) (< 7,0,C>, C) (< 7,0,D>, ?) (< 7,0,E>, E) (< 7,0,F>, 11) (< 7,0,G>, G) (< 7,0,H>, 5)
(< 8,0,A>, A) (< 8,0,B>, 11) (< 8,0,C>, C) (< 8,0,D>, ?) (< 8,0,E>, E) (< 8,0,F>, 11) (< 8,0,G>, G) (< 8,0,H>, 4)
(<10,0,A>, A) (<10,0,B>, C) (<10,0,C>, C) (<10,0,D>, E) (<10,0,E>, E) (<10,0,F>, G) (<10,0,G>, G) (<10,0,H>, A)
(<11,0,A>, A) (<11,0,B>, C) (<11,0,C>, C) (<11,0,D>, A) (<11,0,E>, E) (<11,0,F>, 0) (<11,0,G>, G) (<11,0,H>, 1 + A)
(<12,0,A>, A) (<12,0,B>, 0) (<12,0,C>, C) (<12,0,D>, E) (<12,0,E>, E) (<12,0,F>, 1) (<12,0,G>, G) (<12,0,H>, A)
+ Applied Processor:
LocalSizeboundsProc
+ Details:
LocalSizebounds generated; rvgraph
(< 4,0,A>, A, .= 0) (< 4,0,B>, B, .= 0) (< 4,0,C>, C, .= 0) (< 4,0,D>, H, .= 0) (< 4,0,E>, E, .= 0) (< 4,0,F>, 0, .= 0) (< 4,0,G>, G, .= 0) (< 4,0,H>, 1 + H, .+ 1)
(< 5,0,A>, A, .= 0) (< 5,0,B>, 0, .= 0) (< 5,0,C>, C, .= 0) (< 5,0,D>, D, .= 0) (< 5,0,E>, E, .= 0) (< 5,0,F>, 1, .= 1) (< 5,0,G>, G, .= 0) (< 5,0,H>, H, .= 0)
(< 7,0,A>, A, .= 0) (< 7,0,B>, B, .= 0) (< 7,0,C>, C, .= 0) (< 7,0,D>, H, .= 0) (< 7,0,E>, E, .= 0) (< 7,0,F>, F, .= 0) (< 7,0,G>, G, .= 0) (< 7,0,H>, 5, .= 5)
(< 8,0,A>, A, .= 0) (< 8,0,B>, F, .= 0) (< 8,0,C>, C, .= 0) (< 8,0,D>, D, .= 0) (< 8,0,E>, E, .= 0) (< 8,0,F>, 11, .= 11) (< 8,0,G>, G, .= 0) (< 8,0,H>, H, .= 0)
(<10,0,A>, A, .= 0) (<10,0,B>, C, .= 0) (<10,0,C>, C, .= 0) (<10,0,D>, E, .= 0) (<10,0,E>, E, .= 0) (<10,0,F>, G, .= 0) (<10,0,G>, G, .= 0) (<10,0,H>, A, .= 0)
(<11,0,A>, A, .= 0) (<11,0,B>, C, .= 0) (<11,0,C>, C, .= 0) (<11,0,D>, A, .= 0) (<11,0,E>, E, .= 0) (<11,0,F>, 0, .= 0) (<11,0,G>, G, .= 0) (<11,0,H>, 1 + A, .+ 1)
(<12,0,A>, A, .= 0) (<12,0,B>, 0, .= 0) (<12,0,C>, C, .= 0) (<12,0,D>, E, .= 0) (<12,0,E>, E, .= 0) (<12,0,F>, 1, .= 1) (<12,0,G>, G, .= 0) (<12,0,H>, A, .= 0)
* Step 9: SizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
4. lbl92(A,B,C,D,E,F,G,H) -> lbl92(A,B,C,H,E,0,G,1 + H) [1 >= D && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] (?,1)
5. lbl92(A,B,C,D,E,F,G,H) -> lbl82(A,0,C,D,E,1,G,H) [D >= 2 && 3 >= D && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] (?,1)
7. lbl82(A,B,C,D,E,F,G,H) -> lbl92(A,B,C,H,E,F,G,1 + H) [H >= A && H >= 3 && 4 >= H && F = 10 && B = 9] (?,1)
8. lbl82(A,B,C,D,E,F,G,H) -> lbl82(A,F,C,D,E,1 + F,G,H) [H >= 3 && 8 >= B && 9 >= B && B >= 0 && H >= A && 4 >= H && F = 1 + B] (?,1)
10. start0(A,B,C,D,E,F,G,H) -> stop(A,C,C,E,E,G,G,A) [A >= 5 && C = C && E = E && G = G && A = A] (1,2)
11. start0(A,B,C,D,E,F,G,H) -> lbl92(A,C,C,A,E,0,G,1 + A) [2 >= A && C = C && E = E && G = G && A = A] (1,2)
12. start0(A,B,C,D,E,F,G,H) -> lbl82(A,0,C,E,E,1,G,A) [A >= 3 && 4 >= A && C = C && E = E && G = G && A = A] (1,2)
Signature:
{(lbl82,8);(lbl92,8);(start,8);(start0,8);(stop,8)}
Flow Graph:
[4->{4,5},5->{8},7->{5},8->{7,8},10->{},11->{4,5},12->{8}]
Sizebounds:
(< 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>, ?)
(< 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>, ?)
(<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>, ?)
+ Applied Processor:
SizeboundsProc
+ Details:
Sizebounds computed:
(< 4,0,A>, A) (< 4,0,B>, C) (< 4,0,C>, C) (< 4,0,D>, ?) (< 4,0,E>, E) (< 4,0,F>, 0) (< 4,0,G>, G) (< 4,0,H>, ?)
(< 5,0,A>, A) (< 5,0,B>, 0) (< 5,0,C>, C) (< 5,0,D>, ?) (< 5,0,E>, E) (< 5,0,F>, 1) (< 5,0,G>, G) (< 5,0,H>, ?)
(< 7,0,A>, A) (< 7,0,B>, 11) (< 7,0,C>, C) (< 7,0,D>, 4) (< 7,0,E>, E) (< 7,0,F>, 11) (< 7,0,G>, G) (< 7,0,H>, 5)
(< 8,0,A>, A) (< 8,0,B>, 11) (< 8,0,C>, C) (< 8,0,D>, ?) (< 8,0,E>, E) (< 8,0,F>, 11) (< 8,0,G>, G) (< 8,0,H>, 4)
(<10,0,A>, A) (<10,0,B>, C) (<10,0,C>, C) (<10,0,D>, E) (<10,0,E>, E) (<10,0,F>, G) (<10,0,G>, G) (<10,0,H>, A)
(<11,0,A>, A) (<11,0,B>, C) (<11,0,C>, C) (<11,0,D>, A) (<11,0,E>, E) (<11,0,F>, 0) (<11,0,G>, G) (<11,0,H>, 1 + A)
(<12,0,A>, A) (<12,0,B>, 0) (<12,0,C>, C) (<12,0,D>, E) (<12,0,E>, E) (<12,0,F>, 1) (<12,0,G>, G) (<12,0,H>, A)
* Step 10: LocationConstraintsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
4. lbl92(A,B,C,D,E,F,G,H) -> lbl92(A,B,C,H,E,0,G,1 + H) [1 >= D && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] (?,1)
5. lbl92(A,B,C,D,E,F,G,H) -> lbl82(A,0,C,D,E,1,G,H) [D >= 2 && 3 >= D && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] (?,1)
7. lbl82(A,B,C,D,E,F,G,H) -> lbl92(A,B,C,H,E,F,G,1 + H) [H >= A && H >= 3 && 4 >= H && F = 10 && B = 9] (?,1)
8. lbl82(A,B,C,D,E,F,G,H) -> lbl82(A,F,C,D,E,1 + F,G,H) [H >= 3 && 8 >= B && 9 >= B && B >= 0 && H >= A && 4 >= H && F = 1 + B] (?,1)
10. start0(A,B,C,D,E,F,G,H) -> stop(A,C,C,E,E,G,G,A) [A >= 5 && C = C && E = E && G = G && A = A] (1,2)
11. start0(A,B,C,D,E,F,G,H) -> lbl92(A,C,C,A,E,0,G,1 + A) [2 >= A && C = C && E = E && G = G && A = A] (1,2)
12. start0(A,B,C,D,E,F,G,H) -> lbl82(A,0,C,E,E,1,G,A) [A >= 3 && 4 >= A && C = C && E = E && G = G && A = A] (1,2)
Signature:
{(lbl82,8);(lbl92,8);(start,8);(start0,8);(stop,8)}
Flow Graph:
[4->{4,5},5->{8},7->{5},8->{7,8},10->{},11->{4,5},12->{8}]
Sizebounds:
(< 4,0,A>, A) (< 4,0,B>, C) (< 4,0,C>, C) (< 4,0,D>, ?) (< 4,0,E>, E) (< 4,0,F>, 0) (< 4,0,G>, G) (< 4,0,H>, ?)
(< 5,0,A>, A) (< 5,0,B>, 0) (< 5,0,C>, C) (< 5,0,D>, ?) (< 5,0,E>, E) (< 5,0,F>, 1) (< 5,0,G>, G) (< 5,0,H>, ?)
(< 7,0,A>, A) (< 7,0,B>, 11) (< 7,0,C>, C) (< 7,0,D>, 4) (< 7,0,E>, E) (< 7,0,F>, 11) (< 7,0,G>, G) (< 7,0,H>, 5)
(< 8,0,A>, A) (< 8,0,B>, 11) (< 8,0,C>, C) (< 8,0,D>, ?) (< 8,0,E>, E) (< 8,0,F>, 11) (< 8,0,G>, G) (< 8,0,H>, 4)
(<10,0,A>, A) (<10,0,B>, C) (<10,0,C>, C) (<10,0,D>, E) (<10,0,E>, E) (<10,0,F>, G) (<10,0,G>, G) (<10,0,H>, A)
(<11,0,A>, A) (<11,0,B>, C) (<11,0,C>, C) (<11,0,D>, A) (<11,0,E>, E) (<11,0,F>, 0) (<11,0,G>, G) (<11,0,H>, 1 + A)
(<12,0,A>, A) (<12,0,B>, 0) (<12,0,C>, C) (<12,0,D>, E) (<12,0,E>, E) (<12,0,F>, 1) (<12,0,G>, G) (<12,0,H>, A)
+ Applied Processor:
LocationConstraintsProc
+ Details:
We computed the location constraints 4 : [4 >= A && 2 >= A] 5 : [4 >= A] 7 : [4 >= A
&& H >= 3] 8 : [4 >= A] 10 : True 11 : True 12 : True .
* Step 11: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
4. lbl92(A,B,C,D,E,F,G,H) -> lbl92(A,B,C,H,E,0,G,1 + H) [1 >= D && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] (?,1)
5. lbl92(A,B,C,D,E,F,G,H) -> lbl82(A,0,C,D,E,1,G,H) [D >= 2 && 3 >= D && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] (?,1)
7. lbl82(A,B,C,D,E,F,G,H) -> lbl92(A,B,C,H,E,F,G,1 + H) [H >= A && H >= 3 && 4 >= H && F = 10 && B = 9] (?,1)
8. lbl82(A,B,C,D,E,F,G,H) -> lbl82(A,F,C,D,E,1 + F,G,H) [H >= 3 && 8 >= B && 9 >= B && B >= 0 && H >= A && 4 >= H && F = 1 + B] (?,1)
10. start0(A,B,C,D,E,F,G,H) -> stop(A,C,C,E,E,G,G,A) [A >= 5 && C = C && E = E && G = G && A = A] (1,2)
11. start0(A,B,C,D,E,F,G,H) -> lbl92(A,C,C,A,E,0,G,1 + A) [2 >= A && C = C && E = E && G = G && A = A] (1,2)
12. start0(A,B,C,D,E,F,G,H) -> lbl82(A,0,C,E,E,1,G,A) [A >= 3 && 4 >= A && C = C && E = E && G = G && A = A] (1,2)
Signature:
{(lbl82,8);(lbl92,8);(start,8);(start0,8);(stop,8)}
Flow Graph:
[4->{4,5},5->{8},7->{5},8->{7,8},10->{},11->{4,5},12->{8}]
Sizebounds:
(< 4,0,A>, A) (< 4,0,B>, C) (< 4,0,C>, C) (< 4,0,D>, ?) (< 4,0,E>, E) (< 4,0,F>, 0) (< 4,0,G>, G) (< 4,0,H>, ?)
(< 5,0,A>, A) (< 5,0,B>, 0) (< 5,0,C>, C) (< 5,0,D>, ?) (< 5,0,E>, E) (< 5,0,F>, 1) (< 5,0,G>, G) (< 5,0,H>, ?)
(< 7,0,A>, A) (< 7,0,B>, 11) (< 7,0,C>, C) (< 7,0,D>, 4) (< 7,0,E>, E) (< 7,0,F>, 11) (< 7,0,G>, G) (< 7,0,H>, 5)
(< 8,0,A>, A) (< 8,0,B>, 11) (< 8,0,C>, C) (< 8,0,D>, ?) (< 8,0,E>, E) (< 8,0,F>, 11) (< 8,0,G>, G) (< 8,0,H>, 4)
(<10,0,A>, A) (<10,0,B>, C) (<10,0,C>, C) (<10,0,D>, E) (<10,0,E>, E) (<10,0,F>, G) (<10,0,G>, G) (<10,0,H>, A)
(<11,0,A>, A) (<11,0,B>, C) (<11,0,C>, C) (<11,0,D>, A) (<11,0,E>, E) (<11,0,F>, 0) (<11,0,G>, G) (<11,0,H>, 1 + A)
(<12,0,A>, A) (<12,0,B>, 0) (<12,0,C>, C) (<12,0,D>, E) (<12,0,E>, E) (<12,0,F>, 1) (<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(lbl82) = 45 + -1*x2 + -9*x8
p(lbl92) = 45 + -9*x8
p(start0) = 45 + -9*x1
p(stop) = 45 + -9*x8
The following rules are strictly oriented:
[H >= 3 && 8 >= B && 9 >= B && B >= 0 && H >= A && 4 >= H && F = 1 + B] ==>
lbl82(A,B,C,D,E,F,G,H) = 45 + -1*B + -9*H
> 45 + -1*F + -9*H
= lbl82(A,F,C,D,E,1 + F,G,H)
The following rules are weakly oriented:
[1 >= D && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] ==>
lbl92(A,B,C,D,E,F,G,H) = 45 + -9*H
>= 36 + -9*H
= lbl92(A,B,C,H,E,0,G,1 + H)
[D >= 2 && 3 >= D && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] ==>
lbl92(A,B,C,D,E,F,G,H) = 45 + -9*H
>= 45 + -9*H
= lbl82(A,0,C,D,E,1,G,H)
[H >= A && H >= 3 && 4 >= H && F = 10 && B = 9] ==>
lbl82(A,B,C,D,E,F,G,H) = 45 + -1*B + -9*H
>= 36 + -9*H
= lbl92(A,B,C,H,E,F,G,1 + H)
[A >= 5 && C = C && E = E && G = G && A = A] ==>
start0(A,B,C,D,E,F,G,H) = 45 + -9*A
>= 45 + -9*A
= stop(A,C,C,E,E,G,G,A)
[2 >= A && C = C && E = E && G = G && A = A] ==>
start0(A,B,C,D,E,F,G,H) = 45 + -9*A
>= 36 + -9*A
= lbl92(A,C,C,A,E,0,G,1 + A)
[A >= 3 && 4 >= A && C = C && E = E && G = G && A = A] ==>
start0(A,B,C,D,E,F,G,H) = 45 + -9*A
>= 45 + -9*A
= lbl82(A,0,C,E,E,1,G,A)
* Step 12: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
4. lbl92(A,B,C,D,E,F,G,H) -> lbl92(A,B,C,H,E,0,G,1 + H) [1 >= D && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] (?,1)
5. lbl92(A,B,C,D,E,F,G,H) -> lbl82(A,0,C,D,E,1,G,H) [D >= 2 && 3 >= D && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] (?,1)
7. lbl82(A,B,C,D,E,F,G,H) -> lbl92(A,B,C,H,E,F,G,1 + H) [H >= A && H >= 3 && 4 >= H && F = 10 && B = 9] (?,1)
8. lbl82(A,B,C,D,E,F,G,H) -> lbl82(A,F,C,D,E,1 + F,G,H) [H >= 3 && 8 >= B && 9 >= B && B >= 0 && H >= A && 4 >= H && F = 1 + B] (45 + 9*A,1)
10. start0(A,B,C,D,E,F,G,H) -> stop(A,C,C,E,E,G,G,A) [A >= 5 && C = C && E = E && G = G && A = A] (1,2)
11. start0(A,B,C,D,E,F,G,H) -> lbl92(A,C,C,A,E,0,G,1 + A) [2 >= A && C = C && E = E && G = G && A = A] (1,2)
12. start0(A,B,C,D,E,F,G,H) -> lbl82(A,0,C,E,E,1,G,A) [A >= 3 && 4 >= A && C = C && E = E && G = G && A = A] (1,2)
Signature:
{(lbl82,8);(lbl92,8);(start,8);(start0,8);(stop,8)}
Flow Graph:
[4->{4,5},5->{8},7->{5},8->{7,8},10->{},11->{4,5},12->{8}]
Sizebounds:
(< 4,0,A>, A) (< 4,0,B>, C) (< 4,0,C>, C) (< 4,0,D>, ?) (< 4,0,E>, E) (< 4,0,F>, 0) (< 4,0,G>, G) (< 4,0,H>, ?)
(< 5,0,A>, A) (< 5,0,B>, 0) (< 5,0,C>, C) (< 5,0,D>, ?) (< 5,0,E>, E) (< 5,0,F>, 1) (< 5,0,G>, G) (< 5,0,H>, ?)
(< 7,0,A>, A) (< 7,0,B>, 11) (< 7,0,C>, C) (< 7,0,D>, 4) (< 7,0,E>, E) (< 7,0,F>, 11) (< 7,0,G>, G) (< 7,0,H>, 5)
(< 8,0,A>, A) (< 8,0,B>, 11) (< 8,0,C>, C) (< 8,0,D>, ?) (< 8,0,E>, E) (< 8,0,F>, 11) (< 8,0,G>, G) (< 8,0,H>, 4)
(<10,0,A>, A) (<10,0,B>, C) (<10,0,C>, C) (<10,0,D>, E) (<10,0,E>, E) (<10,0,F>, G) (<10,0,G>, G) (<10,0,H>, A)
(<11,0,A>, A) (<11,0,B>, C) (<11,0,C>, C) (<11,0,D>, A) (<11,0,E>, E) (<11,0,F>, 0) (<11,0,G>, G) (<11,0,H>, 1 + A)
(<12,0,A>, A) (<12,0,B>, 0) (<12,0,C>, C) (<12,0,D>, E) (<12,0,E>, E) (<12,0,F>, 1) (<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(lbl82) = 5 + -1*x8
p(lbl92) = 4 + -1*x4
p(start0) = 5 + -1*x1
p(stop) = 5 + -1*x8
The following rules are strictly oriented:
[H >= A && H >= 3 && 4 >= H && F = 10 && B = 9] ==>
lbl82(A,B,C,D,E,F,G,H) = 5 + -1*H
> 4 + -1*H
= lbl92(A,B,C,H,E,F,G,1 + H)
The following rules are weakly oriented:
[1 >= D && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] ==>
lbl92(A,B,C,D,E,F,G,H) = 4 + -1*D
>= 4 + -1*H
= lbl92(A,B,C,H,E,0,G,1 + H)
[D >= 2 && 3 >= D && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] ==>
lbl92(A,B,C,D,E,F,G,H) = 4 + -1*D
>= 5 + -1*H
= lbl82(A,0,C,D,E,1,G,H)
[H >= 3 && 8 >= B && 9 >= B && B >= 0 && H >= A && 4 >= H && F = 1 + B] ==>
lbl82(A,B,C,D,E,F,G,H) = 5 + -1*H
>= 5 + -1*H
= lbl82(A,F,C,D,E,1 + F,G,H)
[A >= 5 && C = C && E = E && G = G && A = A] ==>
start0(A,B,C,D,E,F,G,H) = 5 + -1*A
>= 5 + -1*A
= stop(A,C,C,E,E,G,G,A)
[2 >= A && C = C && E = E && G = G && A = A] ==>
start0(A,B,C,D,E,F,G,H) = 5 + -1*A
>= 4 + -1*A
= lbl92(A,C,C,A,E,0,G,1 + A)
[A >= 3 && 4 >= A && C = C && E = E && G = G && A = A] ==>
start0(A,B,C,D,E,F,G,H) = 5 + -1*A
>= 5 + -1*A
= lbl82(A,0,C,E,E,1,G,A)
* Step 13: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
4. lbl92(A,B,C,D,E,F,G,H) -> lbl92(A,B,C,H,E,0,G,1 + H) [1 >= D && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] (?,1)
5. lbl92(A,B,C,D,E,F,G,H) -> lbl82(A,0,C,D,E,1,G,H) [D >= 2 && 3 >= D && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] (?,1)
7. lbl82(A,B,C,D,E,F,G,H) -> lbl92(A,B,C,H,E,F,G,1 + H) [H >= A && H >= 3 && 4 >= H && F = 10 && B = 9] (5 + A,1)
8. lbl82(A,B,C,D,E,F,G,H) -> lbl82(A,F,C,D,E,1 + F,G,H) [H >= 3 && 8 >= B && 9 >= B && B >= 0 && H >= A && 4 >= H && F = 1 + B] (45 + 9*A,1)
10. start0(A,B,C,D,E,F,G,H) -> stop(A,C,C,E,E,G,G,A) [A >= 5 && C = C && E = E && G = G && A = A] (1,2)
11. start0(A,B,C,D,E,F,G,H) -> lbl92(A,C,C,A,E,0,G,1 + A) [2 >= A && C = C && E = E && G = G && A = A] (1,2)
12. start0(A,B,C,D,E,F,G,H) -> lbl82(A,0,C,E,E,1,G,A) [A >= 3 && 4 >= A && C = C && E = E && G = G && A = A] (1,2)
Signature:
{(lbl82,8);(lbl92,8);(start,8);(start0,8);(stop,8)}
Flow Graph:
[4->{4,5},5->{8},7->{5},8->{7,8},10->{},11->{4,5},12->{8}]
Sizebounds:
(< 4,0,A>, A) (< 4,0,B>, C) (< 4,0,C>, C) (< 4,0,D>, ?) (< 4,0,E>, E) (< 4,0,F>, 0) (< 4,0,G>, G) (< 4,0,H>, ?)
(< 5,0,A>, A) (< 5,0,B>, 0) (< 5,0,C>, C) (< 5,0,D>, ?) (< 5,0,E>, E) (< 5,0,F>, 1) (< 5,0,G>, G) (< 5,0,H>, ?)
(< 7,0,A>, A) (< 7,0,B>, 11) (< 7,0,C>, C) (< 7,0,D>, 4) (< 7,0,E>, E) (< 7,0,F>, 11) (< 7,0,G>, G) (< 7,0,H>, 5)
(< 8,0,A>, A) (< 8,0,B>, 11) (< 8,0,C>, C) (< 8,0,D>, ?) (< 8,0,E>, E) (< 8,0,F>, 11) (< 8,0,G>, G) (< 8,0,H>, 4)
(<10,0,A>, A) (<10,0,B>, C) (<10,0,C>, C) (<10,0,D>, E) (<10,0,E>, E) (<10,0,F>, G) (<10,0,G>, G) (<10,0,H>, A)
(<11,0,A>, A) (<11,0,B>, C) (<11,0,C>, C) (<11,0,D>, A) (<11,0,E>, E) (<11,0,F>, 0) (<11,0,G>, G) (<11,0,H>, 1 + A)
(<12,0,A>, A) (<12,0,B>, 0) (<12,0,C>, C) (<12,0,D>, E) (<12,0,E>, E) (<12,0,F>, 1) (<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(lbl82) = 4 + -1*x8
p(lbl92) = 4 + -1*x4
p(start0) = 4 + -1*x1
p(stop) = 4 + -1*x8
The following rules are strictly oriented:
[D >= 2 && 3 >= D && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] ==>
lbl92(A,B,C,D,E,F,G,H) = 4 + -1*D
> 4 + -1*H
= lbl82(A,0,C,D,E,1,G,H)
The following rules are weakly oriented:
[1 >= D && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] ==>
lbl92(A,B,C,D,E,F,G,H) = 4 + -1*D
>= 4 + -1*H
= lbl92(A,B,C,H,E,0,G,1 + H)
[H >= A && H >= 3 && 4 >= H && F = 10 && B = 9] ==>
lbl82(A,B,C,D,E,F,G,H) = 4 + -1*H
>= 4 + -1*H
= lbl92(A,B,C,H,E,F,G,1 + H)
[H >= 3 && 8 >= B && 9 >= B && B >= 0 && H >= A && 4 >= H && F = 1 + B] ==>
lbl82(A,B,C,D,E,F,G,H) = 4 + -1*H
>= 4 + -1*H
= lbl82(A,F,C,D,E,1 + F,G,H)
[A >= 5 && C = C && E = E && G = G && A = A] ==>
start0(A,B,C,D,E,F,G,H) = 4 + -1*A
>= 4 + -1*A
= stop(A,C,C,E,E,G,G,A)
[2 >= A && C = C && E = E && G = G && A = A] ==>
start0(A,B,C,D,E,F,G,H) = 4 + -1*A
>= 4 + -1*A
= lbl92(A,C,C,A,E,0,G,1 + A)
[A >= 3 && 4 >= A && C = C && E = E && G = G && A = A] ==>
start0(A,B,C,D,E,F,G,H) = 4 + -1*A
>= 4 + -1*A
= lbl82(A,0,C,E,E,1,G,A)
* Step 14: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
4. lbl92(A,B,C,D,E,F,G,H) -> lbl92(A,B,C,H,E,0,G,1 + H) [1 >= D && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] (?,1)
5. lbl92(A,B,C,D,E,F,G,H) -> lbl82(A,0,C,D,E,1,G,H) [D >= 2 && 3 >= D && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] (4 + A,1)
7. lbl82(A,B,C,D,E,F,G,H) -> lbl92(A,B,C,H,E,F,G,1 + H) [H >= A && H >= 3 && 4 >= H && F = 10 && B = 9] (5 + A,1)
8. lbl82(A,B,C,D,E,F,G,H) -> lbl82(A,F,C,D,E,1 + F,G,H) [H >= 3 && 8 >= B && 9 >= B && B >= 0 && H >= A && 4 >= H && F = 1 + B] (45 + 9*A,1)
10. start0(A,B,C,D,E,F,G,H) -> stop(A,C,C,E,E,G,G,A) [A >= 5 && C = C && E = E && G = G && A = A] (1,2)
11. start0(A,B,C,D,E,F,G,H) -> lbl92(A,C,C,A,E,0,G,1 + A) [2 >= A && C = C && E = E && G = G && A = A] (1,2)
12. start0(A,B,C,D,E,F,G,H) -> lbl82(A,0,C,E,E,1,G,A) [A >= 3 && 4 >= A && C = C && E = E && G = G && A = A] (1,2)
Signature:
{(lbl82,8);(lbl92,8);(start,8);(start0,8);(stop,8)}
Flow Graph:
[4->{4,5},5->{8},7->{5},8->{7,8},10->{},11->{4,5},12->{8}]
Sizebounds:
(< 4,0,A>, A) (< 4,0,B>, C) (< 4,0,C>, C) (< 4,0,D>, ?) (< 4,0,E>, E) (< 4,0,F>, 0) (< 4,0,G>, G) (< 4,0,H>, ?)
(< 5,0,A>, A) (< 5,0,B>, 0) (< 5,0,C>, C) (< 5,0,D>, ?) (< 5,0,E>, E) (< 5,0,F>, 1) (< 5,0,G>, G) (< 5,0,H>, ?)
(< 7,0,A>, A) (< 7,0,B>, 11) (< 7,0,C>, C) (< 7,0,D>, 4) (< 7,0,E>, E) (< 7,0,F>, 11) (< 7,0,G>, G) (< 7,0,H>, 5)
(< 8,0,A>, A) (< 8,0,B>, 11) (< 8,0,C>, C) (< 8,0,D>, ?) (< 8,0,E>, E) (< 8,0,F>, 11) (< 8,0,G>, G) (< 8,0,H>, 4)
(<10,0,A>, A) (<10,0,B>, C) (<10,0,C>, C) (<10,0,D>, E) (<10,0,E>, E) (<10,0,F>, G) (<10,0,G>, G) (<10,0,H>, A)
(<11,0,A>, A) (<11,0,B>, C) (<11,0,C>, C) (<11,0,D>, A) (<11,0,E>, E) (<11,0,F>, 0) (<11,0,G>, G) (<11,0,H>, 1 + A)
(<12,0,A>, A) (<12,0,B>, 0) (<12,0,C>, C) (<12,0,D>, E) (<12,0,E>, E) (<12,0,F>, 1) (<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(lbl82) = -1
p(lbl92) = 2 + -1*x4
p(start0) = 3 + -1*x1
p(stop) = 3 + -1*x8
The following rules are strictly oriented:
[1 >= D && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] ==>
lbl92(A,B,C,D,E,F,G,H) = 2 + -1*D
> 2 + -1*H
= lbl92(A,B,C,H,E,0,G,1 + H)
The following rules are weakly oriented:
[D >= 2 && 3 >= D && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] ==>
lbl92(A,B,C,D,E,F,G,H) = 2 + -1*D
>= -1
= lbl82(A,0,C,D,E,1,G,H)
[H >= A && H >= 3 && 4 >= H && F = 10 && B = 9] ==>
lbl82(A,B,C,D,E,F,G,H) = -1
>= 2 + -1*H
= lbl92(A,B,C,H,E,F,G,1 + H)
[H >= 3 && 8 >= B && 9 >= B && B >= 0 && H >= A && 4 >= H && F = 1 + B] ==>
lbl82(A,B,C,D,E,F,G,H) = -1
>= -1
= lbl82(A,F,C,D,E,1 + F,G,H)
[A >= 5 && C = C && E = E && G = G && A = A] ==>
start0(A,B,C,D,E,F,G,H) = 3 + -1*A
>= 3 + -1*A
= stop(A,C,C,E,E,G,G,A)
[2 >= A && C = C && E = E && G = G && A = A] ==>
start0(A,B,C,D,E,F,G,H) = 3 + -1*A
>= 2 + -1*A
= lbl92(A,C,C,A,E,0,G,1 + A)
[A >= 3 && 4 >= A && C = C && E = E && G = G && A = A] ==>
start0(A,B,C,D,E,F,G,H) = 3 + -1*A
>= -1
= lbl82(A,0,C,E,E,1,G,A)
* Step 15: UnsatPaths WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
4. lbl92(A,B,C,D,E,F,G,H) -> lbl92(A,B,C,H,E,0,G,1 + H) [1 >= D && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] (3 + A,1)
5. lbl92(A,B,C,D,E,F,G,H) -> lbl82(A,0,C,D,E,1,G,H) [D >= 2 && 3 >= D && D >= A && 10 + F >= 5*D && F >= 0 && H = 1 + D] (4 + A,1)
7. lbl82(A,B,C,D,E,F,G,H) -> lbl92(A,B,C,H,E,F,G,1 + H) [H >= A && H >= 3 && 4 >= H && F = 10 && B = 9] (5 + A,1)
8. lbl82(A,B,C,D,E,F,G,H) -> lbl82(A,F,C,D,E,1 + F,G,H) [H >= 3 && 8 >= B && 9 >= B && B >= 0 && H >= A && 4 >= H && F = 1 + B] (45 + 9*A,1)
10. start0(A,B,C,D,E,F,G,H) -> stop(A,C,C,E,E,G,G,A) [A >= 5 && C = C && E = E && G = G && A = A] (1,2)
11. start0(A,B,C,D,E,F,G,H) -> lbl92(A,C,C,A,E,0,G,1 + A) [2 >= A && C = C && E = E && G = G && A = A] (1,2)
12. start0(A,B,C,D,E,F,G,H) -> lbl82(A,0,C,E,E,1,G,A) [A >= 3 && 4 >= A && C = C && E = E && G = G && A = A] (1,2)
Signature:
{(lbl82,8);(lbl92,8);(start,8);(start0,8);(stop,8)}
Flow Graph:
[4->{4,5},5->{8},7->{5},8->{7,8},10->{},11->{4,5},12->{8}]
Sizebounds:
(< 4,0,A>, A) (< 4,0,B>, C) (< 4,0,C>, C) (< 4,0,D>, ?) (< 4,0,E>, E) (< 4,0,F>, 0) (< 4,0,G>, G) (< 4,0,H>, ?)
(< 5,0,A>, A) (< 5,0,B>, 0) (< 5,0,C>, C) (< 5,0,D>, ?) (< 5,0,E>, E) (< 5,0,F>, 1) (< 5,0,G>, G) (< 5,0,H>, ?)
(< 7,0,A>, A) (< 7,0,B>, 11) (< 7,0,C>, C) (< 7,0,D>, 4) (< 7,0,E>, E) (< 7,0,F>, 11) (< 7,0,G>, G) (< 7,0,H>, 5)
(< 8,0,A>, A) (< 8,0,B>, 11) (< 8,0,C>, C) (< 8,0,D>, ?) (< 8,0,E>, E) (< 8,0,F>, 11) (< 8,0,G>, G) (< 8,0,H>, 4)
(<10,0,A>, A) (<10,0,B>, C) (<10,0,C>, C) (<10,0,D>, E) (<10,0,E>, E) (<10,0,F>, G) (<10,0,G>, G) (<10,0,H>, A)
(<11,0,A>, A) (<11,0,B>, C) (<11,0,C>, C) (<11,0,D>, A) (<11,0,E>, E) (<11,0,F>, 0) (<11,0,G>, G) (<11,0,H>, 1 + A)
(<12,0,A>, A) (<12,0,B>, 0) (<12,0,C>, C) (<12,0,D>, E) (<12,0,E>, E) (<12,0,F>, 1) (<12,0,G>, G) (<12,0,H>, A)
+ Applied Processor:
UnsatPaths
+ Details:
The problem is already solved.
WORST_CASE(?,O(n^1))