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