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