WORST_CASE(?,O(1))
* Step 1: RestrictVarsProcessor WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,B,C,D,E,F,G) -> f15(0,H,I,0,E,F,G) True (1,1)
1. f15(A,B,C,D,E,F,G) -> f15(A,B,C,1 + D,E,F,G) [49 >= D] (?,1)
2. f25(A,B,C,D,E,F,G) -> f25(A,B,C,D,1 + E,F,G) [49 >= E] (?,1)
3. f33(A,B,C,D,E,F,G) -> f33(1 + A,B,C,D,E,F,G) [49 >= A] (?,1)
4. f42(A,B,C,D,E,F,G) -> f42(A,B,C,D,E,1 + F,G) [49 >= F] (?,1)
5. f52(A,B,C,D,E,F,G) -> f52(A,B,C,D,E,F,1 + G) [49 >= G] (?,1)
6. f60(A,B,C,D,E,F,G) -> f60(1 + A,B,C,D,E,F,G) [49 >= A] (?,1)
7. f60(A,B,C,D,E,F,G) -> f69(A,B,C,D,E,F,G) [A >= 50] (?,1)
8. f52(A,B,C,D,E,F,G) -> f60(0,B,C,D,E,F,G) [G >= 50] (?,1)
9. f42(A,B,C,D,E,F,G) -> f52(A,B,C,D,E,F,0) [F >= 50] (?,1)
10. f33(A,B,C,D,E,F,G) -> f42(A,B,C,D,E,0,G) [A >= 50] (?,1)
11. f25(A,B,C,D,E,F,G) -> f33(0,B,C,D,E,F,G) [E >= 50] (?,1)
12. f15(A,B,C,D,E,F,G) -> f25(A,B,C,D,0,F,G) [D >= 50] (?,1)
Signature:
{(f0,7);(f15,7);(f25,7);(f33,7);(f42,7);(f52,7);(f60,7);(f69,7)}
Flow Graph:
[0->{1,12},1->{1,12},2->{2,11},3->{3,10},4->{4,9},5->{5,8},6->{6,7},7->{},8->{6,7},9->{5,8},10->{4,9}
,11->{3,10},12->{2,11}]
+ Applied Processor:
RestrictVarsProcessor
+ Details:
We removed the arguments [B,C] .
* Step 2: LocalSizeboundsProc WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,D,E,F,G) -> f15(0,0,E,F,G) True (1,1)
1. f15(A,D,E,F,G) -> f15(A,1 + D,E,F,G) [49 >= D] (?,1)
2. f25(A,D,E,F,G) -> f25(A,D,1 + E,F,G) [49 >= E] (?,1)
3. f33(A,D,E,F,G) -> f33(1 + A,D,E,F,G) [49 >= A] (?,1)
4. f42(A,D,E,F,G) -> f42(A,D,E,1 + F,G) [49 >= F] (?,1)
5. f52(A,D,E,F,G) -> f52(A,D,E,F,1 + G) [49 >= G] (?,1)
6. f60(A,D,E,F,G) -> f60(1 + A,D,E,F,G) [49 >= A] (?,1)
7. f60(A,D,E,F,G) -> f69(A,D,E,F,G) [A >= 50] (?,1)
8. f52(A,D,E,F,G) -> f60(0,D,E,F,G) [G >= 50] (?,1)
9. f42(A,D,E,F,G) -> f52(A,D,E,F,0) [F >= 50] (?,1)
10. f33(A,D,E,F,G) -> f42(A,D,E,0,G) [A >= 50] (?,1)
11. f25(A,D,E,F,G) -> f33(0,D,E,F,G) [E >= 50] (?,1)
12. f15(A,D,E,F,G) -> f25(A,D,0,F,G) [D >= 50] (?,1)
Signature:
{(f0,5);(f15,5);(f25,5);(f33,5);(f42,5);(f52,5);(f60,5);(f69,5)}
Flow Graph:
[0->{1,12},1->{1,12},2->{2,11},3->{3,10},4->{4,9},5->{5,8},6->{6,7},7->{},8->{6,7},9->{5,8},10->{4,9}
,11->{3,10},12->{2,11}]
+ Applied Processor:
LocalSizeboundsProc
+ Details:
LocalSizebounds generated; rvgraph
(< 0,0,A>, 0, .= 0) (< 0,0,D>, 0, .= 0) (< 0,0,E>, E, .= 0) (< 0,0,F>, F, .= 0) (< 0,0,G>, G, .= 0)
(< 1,0,A>, A, .= 0) (< 1,0,D>, 1 + D, .+ 1) (< 1,0,E>, E, .= 0) (< 1,0,F>, F, .= 0) (< 1,0,G>, G, .= 0)
(< 2,0,A>, A, .= 0) (< 2,0,D>, D, .= 0) (< 2,0,E>, 1 + E, .+ 1) (< 2,0,F>, F, .= 0) (< 2,0,G>, G, .= 0)
(< 3,0,A>, 1 + A, .+ 1) (< 3,0,D>, D, .= 0) (< 3,0,E>, E, .= 0) (< 3,0,F>, F, .= 0) (< 3,0,G>, G, .= 0)
(< 4,0,A>, A, .= 0) (< 4,0,D>, D, .= 0) (< 4,0,E>, E, .= 0) (< 4,0,F>, 1 + F, .+ 1) (< 4,0,G>, G, .= 0)
(< 5,0,A>, A, .= 0) (< 5,0,D>, D, .= 0) (< 5,0,E>, E, .= 0) (< 5,0,F>, F, .= 0) (< 5,0,G>, 1 + G, .+ 1)
(< 6,0,A>, 1 + A, .+ 1) (< 6,0,D>, D, .= 0) (< 6,0,E>, E, .= 0) (< 6,0,F>, F, .= 0) (< 6,0,G>, G, .= 0)
(< 7,0,A>, A, .= 0) (< 7,0,D>, D, .= 0) (< 7,0,E>, E, .= 0) (< 7,0,F>, F, .= 0) (< 7,0,G>, G, .= 0)
(< 8,0,A>, 0, .= 0) (< 8,0,D>, D, .= 0) (< 8,0,E>, E, .= 0) (< 8,0,F>, F, .= 0) (< 8,0,G>, G, .= 0)
(< 9,0,A>, A, .= 0) (< 9,0,D>, D, .= 0) (< 9,0,E>, E, .= 0) (< 9,0,F>, F, .= 0) (< 9,0,G>, 0, .= 0)
(<10,0,A>, A, .= 0) (<10,0,D>, D, .= 0) (<10,0,E>, E, .= 0) (<10,0,F>, 0, .= 0) (<10,0,G>, G, .= 0)
(<11,0,A>, 0, .= 0) (<11,0,D>, D, .= 0) (<11,0,E>, E, .= 0) (<11,0,F>, F, .= 0) (<11,0,G>, G, .= 0)
(<12,0,A>, A, .= 0) (<12,0,D>, D, .= 0) (<12,0,E>, 0, .= 0) (<12,0,F>, F, .= 0) (<12,0,G>, G, .= 0)
* Step 3: SizeboundsProc WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,D,E,F,G) -> f15(0,0,E,F,G) True (1,1)
1. f15(A,D,E,F,G) -> f15(A,1 + D,E,F,G) [49 >= D] (?,1)
2. f25(A,D,E,F,G) -> f25(A,D,1 + E,F,G) [49 >= E] (?,1)
3. f33(A,D,E,F,G) -> f33(1 + A,D,E,F,G) [49 >= A] (?,1)
4. f42(A,D,E,F,G) -> f42(A,D,E,1 + F,G) [49 >= F] (?,1)
5. f52(A,D,E,F,G) -> f52(A,D,E,F,1 + G) [49 >= G] (?,1)
6. f60(A,D,E,F,G) -> f60(1 + A,D,E,F,G) [49 >= A] (?,1)
7. f60(A,D,E,F,G) -> f69(A,D,E,F,G) [A >= 50] (?,1)
8. f52(A,D,E,F,G) -> f60(0,D,E,F,G) [G >= 50] (?,1)
9. f42(A,D,E,F,G) -> f52(A,D,E,F,0) [F >= 50] (?,1)
10. f33(A,D,E,F,G) -> f42(A,D,E,0,G) [A >= 50] (?,1)
11. f25(A,D,E,F,G) -> f33(0,D,E,F,G) [E >= 50] (?,1)
12. f15(A,D,E,F,G) -> f25(A,D,0,F,G) [D >= 50] (?,1)
Signature:
{(f0,5);(f15,5);(f25,5);(f33,5);(f42,5);(f52,5);(f60,5);(f69,5)}
Flow Graph:
[0->{1,12},1->{1,12},2->{2,11},3->{3,10},4->{4,9},5->{5,8},6->{6,7},7->{},8->{6,7},9->{5,8},10->{4,9}
,11->{3,10},12->{2,11}]
Sizebounds:
(< 0,0,A>, ?) (< 0,0,D>, ?) (< 0,0,E>, ?) (< 0,0,F>, ?) (< 0,0,G>, ?)
(< 1,0,A>, ?) (< 1,0,D>, ?) (< 1,0,E>, ?) (< 1,0,F>, ?) (< 1,0,G>, ?)
(< 2,0,A>, ?) (< 2,0,D>, ?) (< 2,0,E>, ?) (< 2,0,F>, ?) (< 2,0,G>, ?)
(< 3,0,A>, ?) (< 3,0,D>, ?) (< 3,0,E>, ?) (< 3,0,F>, ?) (< 3,0,G>, ?)
(< 4,0,A>, ?) (< 4,0,D>, ?) (< 4,0,E>, ?) (< 4,0,F>, ?) (< 4,0,G>, ?)
(< 5,0,A>, ?) (< 5,0,D>, ?) (< 5,0,E>, ?) (< 5,0,F>, ?) (< 5,0,G>, ?)
(< 6,0,A>, ?) (< 6,0,D>, ?) (< 6,0,E>, ?) (< 6,0,F>, ?) (< 6,0,G>, ?)
(< 7,0,A>, ?) (< 7,0,D>, ?) (< 7,0,E>, ?) (< 7,0,F>, ?) (< 7,0,G>, ?)
(< 8,0,A>, ?) (< 8,0,D>, ?) (< 8,0,E>, ?) (< 8,0,F>, ?) (< 8,0,G>, ?)
(< 9,0,A>, ?) (< 9,0,D>, ?) (< 9,0,E>, ?) (< 9,0,F>, ?) (< 9,0,G>, ?)
(<10,0,A>, ?) (<10,0,D>, ?) (<10,0,E>, ?) (<10,0,F>, ?) (<10,0,G>, ?)
(<11,0,A>, ?) (<11,0,D>, ?) (<11,0,E>, ?) (<11,0,F>, ?) (<11,0,G>, ?)
(<12,0,A>, ?) (<12,0,D>, ?) (<12,0,E>, ?) (<12,0,F>, ?) (<12,0,G>, ?)
+ Applied Processor:
SizeboundsProc
+ Details:
Sizebounds computed:
(< 0,0,A>, 0) (< 0,0,D>, 0) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G)
(< 1,0,A>, 0) (< 1,0,D>, 50) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G)
(< 2,0,A>, 0) (< 2,0,D>, 50) (< 2,0,E>, 50) (< 2,0,F>, F) (< 2,0,G>, G)
(< 3,0,A>, 50) (< 3,0,D>, 50) (< 3,0,E>, 50) (< 3,0,F>, F) (< 3,0,G>, G)
(< 4,0,A>, 50) (< 4,0,D>, 50) (< 4,0,E>, 50) (< 4,0,F>, 50) (< 4,0,G>, G)
(< 5,0,A>, 50) (< 5,0,D>, 50) (< 5,0,E>, 50) (< 5,0,F>, 50) (< 5,0,G>, 50)
(< 6,0,A>, 50) (< 6,0,D>, 50) (< 6,0,E>, 50) (< 6,0,F>, 50) (< 6,0,G>, 50)
(< 7,0,A>, 50) (< 7,0,D>, 50) (< 7,0,E>, 50) (< 7,0,F>, 50) (< 7,0,G>, 50)
(< 8,0,A>, 0) (< 8,0,D>, 50) (< 8,0,E>, 50) (< 8,0,F>, 50) (< 8,0,G>, 50)
(< 9,0,A>, 50) (< 9,0,D>, 50) (< 9,0,E>, 50) (< 9,0,F>, 50) (< 9,0,G>, 0)
(<10,0,A>, 50) (<10,0,D>, 50) (<10,0,E>, 50) (<10,0,F>, 0) (<10,0,G>, G)
(<11,0,A>, 0) (<11,0,D>, 50) (<11,0,E>, 50) (<11,0,F>, F) (<11,0,G>, G)
(<12,0,A>, 0) (<12,0,D>, 50) (<12,0,E>, 0) (<12,0,F>, F) (<12,0,G>, G)
* Step 4: UnsatPaths WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,D,E,F,G) -> f15(0,0,E,F,G) True (1,1)
1. f15(A,D,E,F,G) -> f15(A,1 + D,E,F,G) [49 >= D] (?,1)
2. f25(A,D,E,F,G) -> f25(A,D,1 + E,F,G) [49 >= E] (?,1)
3. f33(A,D,E,F,G) -> f33(1 + A,D,E,F,G) [49 >= A] (?,1)
4. f42(A,D,E,F,G) -> f42(A,D,E,1 + F,G) [49 >= F] (?,1)
5. f52(A,D,E,F,G) -> f52(A,D,E,F,1 + G) [49 >= G] (?,1)
6. f60(A,D,E,F,G) -> f60(1 + A,D,E,F,G) [49 >= A] (?,1)
7. f60(A,D,E,F,G) -> f69(A,D,E,F,G) [A >= 50] (?,1)
8. f52(A,D,E,F,G) -> f60(0,D,E,F,G) [G >= 50] (?,1)
9. f42(A,D,E,F,G) -> f52(A,D,E,F,0) [F >= 50] (?,1)
10. f33(A,D,E,F,G) -> f42(A,D,E,0,G) [A >= 50] (?,1)
11. f25(A,D,E,F,G) -> f33(0,D,E,F,G) [E >= 50] (?,1)
12. f15(A,D,E,F,G) -> f25(A,D,0,F,G) [D >= 50] (?,1)
Signature:
{(f0,5);(f15,5);(f25,5);(f33,5);(f42,5);(f52,5);(f60,5);(f69,5)}
Flow Graph:
[0->{1,12},1->{1,12},2->{2,11},3->{3,10},4->{4,9},5->{5,8},6->{6,7},7->{},8->{6,7},9->{5,8},10->{4,9}
,11->{3,10},12->{2,11}]
Sizebounds:
(< 0,0,A>, 0) (< 0,0,D>, 0) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G)
(< 1,0,A>, 0) (< 1,0,D>, 50) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G)
(< 2,0,A>, 0) (< 2,0,D>, 50) (< 2,0,E>, 50) (< 2,0,F>, F) (< 2,0,G>, G)
(< 3,0,A>, 50) (< 3,0,D>, 50) (< 3,0,E>, 50) (< 3,0,F>, F) (< 3,0,G>, G)
(< 4,0,A>, 50) (< 4,0,D>, 50) (< 4,0,E>, 50) (< 4,0,F>, 50) (< 4,0,G>, G)
(< 5,0,A>, 50) (< 5,0,D>, 50) (< 5,0,E>, 50) (< 5,0,F>, 50) (< 5,0,G>, 50)
(< 6,0,A>, 50) (< 6,0,D>, 50) (< 6,0,E>, 50) (< 6,0,F>, 50) (< 6,0,G>, 50)
(< 7,0,A>, 50) (< 7,0,D>, 50) (< 7,0,E>, 50) (< 7,0,F>, 50) (< 7,0,G>, 50)
(< 8,0,A>, 0) (< 8,0,D>, 50) (< 8,0,E>, 50) (< 8,0,F>, 50) (< 8,0,G>, 50)
(< 9,0,A>, 50) (< 9,0,D>, 50) (< 9,0,E>, 50) (< 9,0,F>, 50) (< 9,0,G>, 0)
(<10,0,A>, 50) (<10,0,D>, 50) (<10,0,E>, 50) (<10,0,F>, 0) (<10,0,G>, G)
(<11,0,A>, 0) (<11,0,D>, 50) (<11,0,E>, 50) (<11,0,F>, F) (<11,0,G>, G)
(<12,0,A>, 0) (<12,0,D>, 50) (<12,0,E>, 0) (<12,0,F>, F) (<12,0,G>, G)
+ Applied Processor:
UnsatPaths
+ Details:
We remove following edges from the transition graph: [(0,12),(8,7),(9,8),(10,9),(11,10),(12,11)]
* Step 5: LeafRules WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,D,E,F,G) -> f15(0,0,E,F,G) True (1,1)
1. f15(A,D,E,F,G) -> f15(A,1 + D,E,F,G) [49 >= D] (?,1)
2. f25(A,D,E,F,G) -> f25(A,D,1 + E,F,G) [49 >= E] (?,1)
3. f33(A,D,E,F,G) -> f33(1 + A,D,E,F,G) [49 >= A] (?,1)
4. f42(A,D,E,F,G) -> f42(A,D,E,1 + F,G) [49 >= F] (?,1)
5. f52(A,D,E,F,G) -> f52(A,D,E,F,1 + G) [49 >= G] (?,1)
6. f60(A,D,E,F,G) -> f60(1 + A,D,E,F,G) [49 >= A] (?,1)
7. f60(A,D,E,F,G) -> f69(A,D,E,F,G) [A >= 50] (?,1)
8. f52(A,D,E,F,G) -> f60(0,D,E,F,G) [G >= 50] (?,1)
9. f42(A,D,E,F,G) -> f52(A,D,E,F,0) [F >= 50] (?,1)
10. f33(A,D,E,F,G) -> f42(A,D,E,0,G) [A >= 50] (?,1)
11. f25(A,D,E,F,G) -> f33(0,D,E,F,G) [E >= 50] (?,1)
12. f15(A,D,E,F,G) -> f25(A,D,0,F,G) [D >= 50] (?,1)
Signature:
{(f0,5);(f15,5);(f25,5);(f33,5);(f42,5);(f52,5);(f60,5);(f69,5)}
Flow Graph:
[0->{1},1->{1,12},2->{2,11},3->{3,10},4->{4,9},5->{5,8},6->{6,7},7->{},8->{6},9->{5},10->{4},11->{3}
,12->{2}]
Sizebounds:
(< 0,0,A>, 0) (< 0,0,D>, 0) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G)
(< 1,0,A>, 0) (< 1,0,D>, 50) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G)
(< 2,0,A>, 0) (< 2,0,D>, 50) (< 2,0,E>, 50) (< 2,0,F>, F) (< 2,0,G>, G)
(< 3,0,A>, 50) (< 3,0,D>, 50) (< 3,0,E>, 50) (< 3,0,F>, F) (< 3,0,G>, G)
(< 4,0,A>, 50) (< 4,0,D>, 50) (< 4,0,E>, 50) (< 4,0,F>, 50) (< 4,0,G>, G)
(< 5,0,A>, 50) (< 5,0,D>, 50) (< 5,0,E>, 50) (< 5,0,F>, 50) (< 5,0,G>, 50)
(< 6,0,A>, 50) (< 6,0,D>, 50) (< 6,0,E>, 50) (< 6,0,F>, 50) (< 6,0,G>, 50)
(< 7,0,A>, 50) (< 7,0,D>, 50) (< 7,0,E>, 50) (< 7,0,F>, 50) (< 7,0,G>, 50)
(< 8,0,A>, 0) (< 8,0,D>, 50) (< 8,0,E>, 50) (< 8,0,F>, 50) (< 8,0,G>, 50)
(< 9,0,A>, 50) (< 9,0,D>, 50) (< 9,0,E>, 50) (< 9,0,F>, 50) (< 9,0,G>, 0)
(<10,0,A>, 50) (<10,0,D>, 50) (<10,0,E>, 50) (<10,0,F>, 0) (<10,0,G>, G)
(<11,0,A>, 0) (<11,0,D>, 50) (<11,0,E>, 50) (<11,0,F>, F) (<11,0,G>, G)
(<12,0,A>, 0) (<12,0,D>, 50) (<12,0,E>, 0) (<12,0,F>, F) (<12,0,G>, G)
+ Applied Processor:
LeafRules
+ Details:
The following transitions are estimated by its predecessors and are removed [7]
* Step 6: PolyRank WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,D,E,F,G) -> f15(0,0,E,F,G) True (1,1)
1. f15(A,D,E,F,G) -> f15(A,1 + D,E,F,G) [49 >= D] (?,1)
2. f25(A,D,E,F,G) -> f25(A,D,1 + E,F,G) [49 >= E] (?,1)
3. f33(A,D,E,F,G) -> f33(1 + A,D,E,F,G) [49 >= A] (?,1)
4. f42(A,D,E,F,G) -> f42(A,D,E,1 + F,G) [49 >= F] (?,1)
5. f52(A,D,E,F,G) -> f52(A,D,E,F,1 + G) [49 >= G] (?,1)
6. f60(A,D,E,F,G) -> f60(1 + A,D,E,F,G) [49 >= A] (?,1)
8. f52(A,D,E,F,G) -> f60(0,D,E,F,G) [G >= 50] (?,1)
9. f42(A,D,E,F,G) -> f52(A,D,E,F,0) [F >= 50] (?,1)
10. f33(A,D,E,F,G) -> f42(A,D,E,0,G) [A >= 50] (?,1)
11. f25(A,D,E,F,G) -> f33(0,D,E,F,G) [E >= 50] (?,1)
12. f15(A,D,E,F,G) -> f25(A,D,0,F,G) [D >= 50] (?,1)
Signature:
{(f0,5);(f15,5);(f25,5);(f33,5);(f42,5);(f52,5);(f60,5);(f69,5)}
Flow Graph:
[0->{1},1->{1,12},2->{2,11},3->{3,10},4->{4,9},5->{5,8},6->{6},8->{6},9->{5},10->{4},11->{3},12->{2}]
Sizebounds:
(< 0,0,A>, 0) (< 0,0,D>, 0) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G)
(< 1,0,A>, 0) (< 1,0,D>, 50) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G)
(< 2,0,A>, 0) (< 2,0,D>, 50) (< 2,0,E>, 50) (< 2,0,F>, F) (< 2,0,G>, G)
(< 3,0,A>, 50) (< 3,0,D>, 50) (< 3,0,E>, 50) (< 3,0,F>, F) (< 3,0,G>, G)
(< 4,0,A>, 50) (< 4,0,D>, 50) (< 4,0,E>, 50) (< 4,0,F>, 50) (< 4,0,G>, G)
(< 5,0,A>, 50) (< 5,0,D>, 50) (< 5,0,E>, 50) (< 5,0,F>, 50) (< 5,0,G>, 50)
(< 6,0,A>, 50) (< 6,0,D>, 50) (< 6,0,E>, 50) (< 6,0,F>, 50) (< 6,0,G>, 50)
(< 8,0,A>, 0) (< 8,0,D>, 50) (< 8,0,E>, 50) (< 8,0,F>, 50) (< 8,0,G>, 50)
(< 9,0,A>, 50) (< 9,0,D>, 50) (< 9,0,E>, 50) (< 9,0,F>, 50) (< 9,0,G>, 0)
(<10,0,A>, 50) (<10,0,D>, 50) (<10,0,E>, 50) (<10,0,F>, 0) (<10,0,G>, G)
(<11,0,A>, 0) (<11,0,D>, 50) (<11,0,E>, 50) (<11,0,F>, F) (<11,0,G>, G)
(<12,0,A>, 0) (<12,0,D>, 50) (<12,0,E>, 0) (<12,0,F>, F) (<12,0,G>, G)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f0) = 1
p(f15) = 1
p(f25) = 0
p(f33) = 0
p(f42) = 0
p(f52) = 0
p(f60) = 0
The following rules are strictly oriented:
[D >= 50] ==>
f15(A,D,E,F,G) = 1
> 0
= f25(A,D,0,F,G)
The following rules are weakly oriented:
True ==>
f0(A,D,E,F,G) = 1
>= 1
= f15(0,0,E,F,G)
[49 >= D] ==>
f15(A,D,E,F,G) = 1
>= 1
= f15(A,1 + D,E,F,G)
[49 >= E] ==>
f25(A,D,E,F,G) = 0
>= 0
= f25(A,D,1 + E,F,G)
[49 >= A] ==>
f33(A,D,E,F,G) = 0
>= 0
= f33(1 + A,D,E,F,G)
[49 >= F] ==>
f42(A,D,E,F,G) = 0
>= 0
= f42(A,D,E,1 + F,G)
[49 >= G] ==>
f52(A,D,E,F,G) = 0
>= 0
= f52(A,D,E,F,1 + G)
[49 >= A] ==>
f60(A,D,E,F,G) = 0
>= 0
= f60(1 + A,D,E,F,G)
[G >= 50] ==>
f52(A,D,E,F,G) = 0
>= 0
= f60(0,D,E,F,G)
[F >= 50] ==>
f42(A,D,E,F,G) = 0
>= 0
= f52(A,D,E,F,0)
[A >= 50] ==>
f33(A,D,E,F,G) = 0
>= 0
= f42(A,D,E,0,G)
[E >= 50] ==>
f25(A,D,E,F,G) = 0
>= 0
= f33(0,D,E,F,G)
* Step 7: PolyRank WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,D,E,F,G) -> f15(0,0,E,F,G) True (1,1)
1. f15(A,D,E,F,G) -> f15(A,1 + D,E,F,G) [49 >= D] (?,1)
2. f25(A,D,E,F,G) -> f25(A,D,1 + E,F,G) [49 >= E] (?,1)
3. f33(A,D,E,F,G) -> f33(1 + A,D,E,F,G) [49 >= A] (?,1)
4. f42(A,D,E,F,G) -> f42(A,D,E,1 + F,G) [49 >= F] (?,1)
5. f52(A,D,E,F,G) -> f52(A,D,E,F,1 + G) [49 >= G] (?,1)
6. f60(A,D,E,F,G) -> f60(1 + A,D,E,F,G) [49 >= A] (?,1)
8. f52(A,D,E,F,G) -> f60(0,D,E,F,G) [G >= 50] (?,1)
9. f42(A,D,E,F,G) -> f52(A,D,E,F,0) [F >= 50] (?,1)
10. f33(A,D,E,F,G) -> f42(A,D,E,0,G) [A >= 50] (?,1)
11. f25(A,D,E,F,G) -> f33(0,D,E,F,G) [E >= 50] (?,1)
12. f15(A,D,E,F,G) -> f25(A,D,0,F,G) [D >= 50] (1,1)
Signature:
{(f0,5);(f15,5);(f25,5);(f33,5);(f42,5);(f52,5);(f60,5);(f69,5)}
Flow Graph:
[0->{1},1->{1,12},2->{2,11},3->{3,10},4->{4,9},5->{5,8},6->{6},8->{6},9->{5},10->{4},11->{3},12->{2}]
Sizebounds:
(< 0,0,A>, 0) (< 0,0,D>, 0) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G)
(< 1,0,A>, 0) (< 1,0,D>, 50) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G)
(< 2,0,A>, 0) (< 2,0,D>, 50) (< 2,0,E>, 50) (< 2,0,F>, F) (< 2,0,G>, G)
(< 3,0,A>, 50) (< 3,0,D>, 50) (< 3,0,E>, 50) (< 3,0,F>, F) (< 3,0,G>, G)
(< 4,0,A>, 50) (< 4,0,D>, 50) (< 4,0,E>, 50) (< 4,0,F>, 50) (< 4,0,G>, G)
(< 5,0,A>, 50) (< 5,0,D>, 50) (< 5,0,E>, 50) (< 5,0,F>, 50) (< 5,0,G>, 50)
(< 6,0,A>, 50) (< 6,0,D>, 50) (< 6,0,E>, 50) (< 6,0,F>, 50) (< 6,0,G>, 50)
(< 8,0,A>, 0) (< 8,0,D>, 50) (< 8,0,E>, 50) (< 8,0,F>, 50) (< 8,0,G>, 50)
(< 9,0,A>, 50) (< 9,0,D>, 50) (< 9,0,E>, 50) (< 9,0,F>, 50) (< 9,0,G>, 0)
(<10,0,A>, 50) (<10,0,D>, 50) (<10,0,E>, 50) (<10,0,F>, 0) (<10,0,G>, G)
(<11,0,A>, 0) (<11,0,D>, 50) (<11,0,E>, 50) (<11,0,F>, F) (<11,0,G>, G)
(<12,0,A>, 0) (<12,0,D>, 50) (<12,0,E>, 0) (<12,0,F>, F) (<12,0,G>, G)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f0) = 50
p(f15) = 50
p(f25) = 50
p(f33) = 50
p(f42) = 50
p(f52) = 50 + -1*x5
p(f60) = 50 + -1*x5
The following rules are strictly oriented:
[49 >= G] ==>
f52(A,D,E,F,G) = 50 + -1*G
> 49 + -1*G
= f52(A,D,E,F,1 + G)
The following rules are weakly oriented:
True ==>
f0(A,D,E,F,G) = 50
>= 50
= f15(0,0,E,F,G)
[49 >= D] ==>
f15(A,D,E,F,G) = 50
>= 50
= f15(A,1 + D,E,F,G)
[49 >= E] ==>
f25(A,D,E,F,G) = 50
>= 50
= f25(A,D,1 + E,F,G)
[49 >= A] ==>
f33(A,D,E,F,G) = 50
>= 50
= f33(1 + A,D,E,F,G)
[49 >= F] ==>
f42(A,D,E,F,G) = 50
>= 50
= f42(A,D,E,1 + F,G)
[49 >= A] ==>
f60(A,D,E,F,G) = 50 + -1*G
>= 50 + -1*G
= f60(1 + A,D,E,F,G)
[G >= 50] ==>
f52(A,D,E,F,G) = 50 + -1*G
>= 50 + -1*G
= f60(0,D,E,F,G)
[F >= 50] ==>
f42(A,D,E,F,G) = 50
>= 50
= f52(A,D,E,F,0)
[A >= 50] ==>
f33(A,D,E,F,G) = 50
>= 50
= f42(A,D,E,0,G)
[E >= 50] ==>
f25(A,D,E,F,G) = 50
>= 50
= f33(0,D,E,F,G)
[D >= 50] ==>
f15(A,D,E,F,G) = 50
>= 50
= f25(A,D,0,F,G)
* Step 8: KnowledgePropagation WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,D,E,F,G) -> f15(0,0,E,F,G) True (1,1)
1. f15(A,D,E,F,G) -> f15(A,1 + D,E,F,G) [49 >= D] (?,1)
2. f25(A,D,E,F,G) -> f25(A,D,1 + E,F,G) [49 >= E] (?,1)
3. f33(A,D,E,F,G) -> f33(1 + A,D,E,F,G) [49 >= A] (?,1)
4. f42(A,D,E,F,G) -> f42(A,D,E,1 + F,G) [49 >= F] (?,1)
5. f52(A,D,E,F,G) -> f52(A,D,E,F,1 + G) [49 >= G] (50,1)
6. f60(A,D,E,F,G) -> f60(1 + A,D,E,F,G) [49 >= A] (?,1)
8. f52(A,D,E,F,G) -> f60(0,D,E,F,G) [G >= 50] (?,1)
9. f42(A,D,E,F,G) -> f52(A,D,E,F,0) [F >= 50] (?,1)
10. f33(A,D,E,F,G) -> f42(A,D,E,0,G) [A >= 50] (?,1)
11. f25(A,D,E,F,G) -> f33(0,D,E,F,G) [E >= 50] (?,1)
12. f15(A,D,E,F,G) -> f25(A,D,0,F,G) [D >= 50] (1,1)
Signature:
{(f0,5);(f15,5);(f25,5);(f33,5);(f42,5);(f52,5);(f60,5);(f69,5)}
Flow Graph:
[0->{1},1->{1,12},2->{2,11},3->{3,10},4->{4,9},5->{5,8},6->{6},8->{6},9->{5},10->{4},11->{3},12->{2}]
Sizebounds:
(< 0,0,A>, 0) (< 0,0,D>, 0) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G)
(< 1,0,A>, 0) (< 1,0,D>, 50) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G)
(< 2,0,A>, 0) (< 2,0,D>, 50) (< 2,0,E>, 50) (< 2,0,F>, F) (< 2,0,G>, G)
(< 3,0,A>, 50) (< 3,0,D>, 50) (< 3,0,E>, 50) (< 3,0,F>, F) (< 3,0,G>, G)
(< 4,0,A>, 50) (< 4,0,D>, 50) (< 4,0,E>, 50) (< 4,0,F>, 50) (< 4,0,G>, G)
(< 5,0,A>, 50) (< 5,0,D>, 50) (< 5,0,E>, 50) (< 5,0,F>, 50) (< 5,0,G>, 50)
(< 6,0,A>, 50) (< 6,0,D>, 50) (< 6,0,E>, 50) (< 6,0,F>, 50) (< 6,0,G>, 50)
(< 8,0,A>, 0) (< 8,0,D>, 50) (< 8,0,E>, 50) (< 8,0,F>, 50) (< 8,0,G>, 50)
(< 9,0,A>, 50) (< 9,0,D>, 50) (< 9,0,E>, 50) (< 9,0,F>, 50) (< 9,0,G>, 0)
(<10,0,A>, 50) (<10,0,D>, 50) (<10,0,E>, 50) (<10,0,F>, 0) (<10,0,G>, G)
(<11,0,A>, 0) (<11,0,D>, 50) (<11,0,E>, 50) (<11,0,F>, F) (<11,0,G>, G)
(<12,0,A>, 0) (<12,0,D>, 50) (<12,0,E>, 0) (<12,0,F>, F) (<12,0,G>, G)
+ Applied Processor:
KnowledgePropagation
+ Details:
We propagate bounds from predecessors.
* Step 9: PolyRank WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,D,E,F,G) -> f15(0,0,E,F,G) True (1,1)
1. f15(A,D,E,F,G) -> f15(A,1 + D,E,F,G) [49 >= D] (?,1)
2. f25(A,D,E,F,G) -> f25(A,D,1 + E,F,G) [49 >= E] (?,1)
3. f33(A,D,E,F,G) -> f33(1 + A,D,E,F,G) [49 >= A] (?,1)
4. f42(A,D,E,F,G) -> f42(A,D,E,1 + F,G) [49 >= F] (?,1)
5. f52(A,D,E,F,G) -> f52(A,D,E,F,1 + G) [49 >= G] (50,1)
6. f60(A,D,E,F,G) -> f60(1 + A,D,E,F,G) [49 >= A] (?,1)
8. f52(A,D,E,F,G) -> f60(0,D,E,F,G) [G >= 50] (50,1)
9. f42(A,D,E,F,G) -> f52(A,D,E,F,0) [F >= 50] (?,1)
10. f33(A,D,E,F,G) -> f42(A,D,E,0,G) [A >= 50] (?,1)
11. f25(A,D,E,F,G) -> f33(0,D,E,F,G) [E >= 50] (?,1)
12. f15(A,D,E,F,G) -> f25(A,D,0,F,G) [D >= 50] (1,1)
Signature:
{(f0,5);(f15,5);(f25,5);(f33,5);(f42,5);(f52,5);(f60,5);(f69,5)}
Flow Graph:
[0->{1},1->{1,12},2->{2,11},3->{3,10},4->{4,9},5->{5,8},6->{6},8->{6},9->{5},10->{4},11->{3},12->{2}]
Sizebounds:
(< 0,0,A>, 0) (< 0,0,D>, 0) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G)
(< 1,0,A>, 0) (< 1,0,D>, 50) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G)
(< 2,0,A>, 0) (< 2,0,D>, 50) (< 2,0,E>, 50) (< 2,0,F>, F) (< 2,0,G>, G)
(< 3,0,A>, 50) (< 3,0,D>, 50) (< 3,0,E>, 50) (< 3,0,F>, F) (< 3,0,G>, G)
(< 4,0,A>, 50) (< 4,0,D>, 50) (< 4,0,E>, 50) (< 4,0,F>, 50) (< 4,0,G>, G)
(< 5,0,A>, 50) (< 5,0,D>, 50) (< 5,0,E>, 50) (< 5,0,F>, 50) (< 5,0,G>, 50)
(< 6,0,A>, 50) (< 6,0,D>, 50) (< 6,0,E>, 50) (< 6,0,F>, 50) (< 6,0,G>, 50)
(< 8,0,A>, 0) (< 8,0,D>, 50) (< 8,0,E>, 50) (< 8,0,F>, 50) (< 8,0,G>, 50)
(< 9,0,A>, 50) (< 9,0,D>, 50) (< 9,0,E>, 50) (< 9,0,F>, 50) (< 9,0,G>, 0)
(<10,0,A>, 50) (<10,0,D>, 50) (<10,0,E>, 50) (<10,0,F>, 0) (<10,0,G>, G)
(<11,0,A>, 0) (<11,0,D>, 50) (<11,0,E>, 50) (<11,0,F>, F) (<11,0,G>, G)
(<12,0,A>, 0) (<12,0,D>, 50) (<12,0,E>, 0) (<12,0,F>, F) (<12,0,G>, G)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f0) = 50
p(f15) = 50
p(f25) = 50
p(f33) = 50
p(f42) = 50
p(f52) = 50
p(f60) = 50 + -1*x1
The following rules are strictly oriented:
[49 >= A] ==>
f60(A,D,E,F,G) = 50 + -1*A
> 49 + -1*A
= f60(1 + A,D,E,F,G)
The following rules are weakly oriented:
True ==>
f0(A,D,E,F,G) = 50
>= 50
= f15(0,0,E,F,G)
[49 >= D] ==>
f15(A,D,E,F,G) = 50
>= 50
= f15(A,1 + D,E,F,G)
[49 >= E] ==>
f25(A,D,E,F,G) = 50
>= 50
= f25(A,D,1 + E,F,G)
[49 >= A] ==>
f33(A,D,E,F,G) = 50
>= 50
= f33(1 + A,D,E,F,G)
[49 >= F] ==>
f42(A,D,E,F,G) = 50
>= 50
= f42(A,D,E,1 + F,G)
[49 >= G] ==>
f52(A,D,E,F,G) = 50
>= 50
= f52(A,D,E,F,1 + G)
[G >= 50] ==>
f52(A,D,E,F,G) = 50
>= 50
= f60(0,D,E,F,G)
[F >= 50] ==>
f42(A,D,E,F,G) = 50
>= 50
= f52(A,D,E,F,0)
[A >= 50] ==>
f33(A,D,E,F,G) = 50
>= 50
= f42(A,D,E,0,G)
[E >= 50] ==>
f25(A,D,E,F,G) = 50
>= 50
= f33(0,D,E,F,G)
[D >= 50] ==>
f15(A,D,E,F,G) = 50
>= 50
= f25(A,D,0,F,G)
* Step 10: PolyRank WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,D,E,F,G) -> f15(0,0,E,F,G) True (1,1)
1. f15(A,D,E,F,G) -> f15(A,1 + D,E,F,G) [49 >= D] (?,1)
2. f25(A,D,E,F,G) -> f25(A,D,1 + E,F,G) [49 >= E] (?,1)
3. f33(A,D,E,F,G) -> f33(1 + A,D,E,F,G) [49 >= A] (?,1)
4. f42(A,D,E,F,G) -> f42(A,D,E,1 + F,G) [49 >= F] (?,1)
5. f52(A,D,E,F,G) -> f52(A,D,E,F,1 + G) [49 >= G] (50,1)
6. f60(A,D,E,F,G) -> f60(1 + A,D,E,F,G) [49 >= A] (50,1)
8. f52(A,D,E,F,G) -> f60(0,D,E,F,G) [G >= 50] (50,1)
9. f42(A,D,E,F,G) -> f52(A,D,E,F,0) [F >= 50] (?,1)
10. f33(A,D,E,F,G) -> f42(A,D,E,0,G) [A >= 50] (?,1)
11. f25(A,D,E,F,G) -> f33(0,D,E,F,G) [E >= 50] (?,1)
12. f15(A,D,E,F,G) -> f25(A,D,0,F,G) [D >= 50] (1,1)
Signature:
{(f0,5);(f15,5);(f25,5);(f33,5);(f42,5);(f52,5);(f60,5);(f69,5)}
Flow Graph:
[0->{1},1->{1,12},2->{2,11},3->{3,10},4->{4,9},5->{5,8},6->{6},8->{6},9->{5},10->{4},11->{3},12->{2}]
Sizebounds:
(< 0,0,A>, 0) (< 0,0,D>, 0) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G)
(< 1,0,A>, 0) (< 1,0,D>, 50) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G)
(< 2,0,A>, 0) (< 2,0,D>, 50) (< 2,0,E>, 50) (< 2,0,F>, F) (< 2,0,G>, G)
(< 3,0,A>, 50) (< 3,0,D>, 50) (< 3,0,E>, 50) (< 3,0,F>, F) (< 3,0,G>, G)
(< 4,0,A>, 50) (< 4,0,D>, 50) (< 4,0,E>, 50) (< 4,0,F>, 50) (< 4,0,G>, G)
(< 5,0,A>, 50) (< 5,0,D>, 50) (< 5,0,E>, 50) (< 5,0,F>, 50) (< 5,0,G>, 50)
(< 6,0,A>, 50) (< 6,0,D>, 50) (< 6,0,E>, 50) (< 6,0,F>, 50) (< 6,0,G>, 50)
(< 8,0,A>, 0) (< 8,0,D>, 50) (< 8,0,E>, 50) (< 8,0,F>, 50) (< 8,0,G>, 50)
(< 9,0,A>, 50) (< 9,0,D>, 50) (< 9,0,E>, 50) (< 9,0,F>, 50) (< 9,0,G>, 0)
(<10,0,A>, 50) (<10,0,D>, 50) (<10,0,E>, 50) (<10,0,F>, 0) (<10,0,G>, G)
(<11,0,A>, 0) (<11,0,D>, 50) (<11,0,E>, 50) (<11,0,F>, F) (<11,0,G>, G)
(<12,0,A>, 0) (<12,0,D>, 50) (<12,0,E>, 0) (<12,0,F>, F) (<12,0,G>, G)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f0) = 50
p(f15) = 50
p(f25) = 50
p(f33) = 50
p(f42) = 50
p(f52) = 49
p(f60) = 49
The following rules are strictly oriented:
[F >= 50] ==>
f42(A,D,E,F,G) = 50
> 49
= f52(A,D,E,F,0)
The following rules are weakly oriented:
True ==>
f0(A,D,E,F,G) = 50
>= 50
= f15(0,0,E,F,G)
[49 >= D] ==>
f15(A,D,E,F,G) = 50
>= 50
= f15(A,1 + D,E,F,G)
[49 >= E] ==>
f25(A,D,E,F,G) = 50
>= 50
= f25(A,D,1 + E,F,G)
[49 >= A] ==>
f33(A,D,E,F,G) = 50
>= 50
= f33(1 + A,D,E,F,G)
[49 >= F] ==>
f42(A,D,E,F,G) = 50
>= 50
= f42(A,D,E,1 + F,G)
[49 >= G] ==>
f52(A,D,E,F,G) = 49
>= 49
= f52(A,D,E,F,1 + G)
[49 >= A] ==>
f60(A,D,E,F,G) = 49
>= 49
= f60(1 + A,D,E,F,G)
[G >= 50] ==>
f52(A,D,E,F,G) = 49
>= 49
= f60(0,D,E,F,G)
[A >= 50] ==>
f33(A,D,E,F,G) = 50
>= 50
= f42(A,D,E,0,G)
[E >= 50] ==>
f25(A,D,E,F,G) = 50
>= 50
= f33(0,D,E,F,G)
[D >= 50] ==>
f15(A,D,E,F,G) = 50
>= 50
= f25(A,D,0,F,G)
* Step 11: PolyRank WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,D,E,F,G) -> f15(0,0,E,F,G) True (1,1)
1. f15(A,D,E,F,G) -> f15(A,1 + D,E,F,G) [49 >= D] (?,1)
2. f25(A,D,E,F,G) -> f25(A,D,1 + E,F,G) [49 >= E] (?,1)
3. f33(A,D,E,F,G) -> f33(1 + A,D,E,F,G) [49 >= A] (?,1)
4. f42(A,D,E,F,G) -> f42(A,D,E,1 + F,G) [49 >= F] (?,1)
5. f52(A,D,E,F,G) -> f52(A,D,E,F,1 + G) [49 >= G] (50,1)
6. f60(A,D,E,F,G) -> f60(1 + A,D,E,F,G) [49 >= A] (50,1)
8. f52(A,D,E,F,G) -> f60(0,D,E,F,G) [G >= 50] (50,1)
9. f42(A,D,E,F,G) -> f52(A,D,E,F,0) [F >= 50] (50,1)
10. f33(A,D,E,F,G) -> f42(A,D,E,0,G) [A >= 50] (?,1)
11. f25(A,D,E,F,G) -> f33(0,D,E,F,G) [E >= 50] (?,1)
12. f15(A,D,E,F,G) -> f25(A,D,0,F,G) [D >= 50] (1,1)
Signature:
{(f0,5);(f15,5);(f25,5);(f33,5);(f42,5);(f52,5);(f60,5);(f69,5)}
Flow Graph:
[0->{1},1->{1,12},2->{2,11},3->{3,10},4->{4,9},5->{5,8},6->{6},8->{6},9->{5},10->{4},11->{3},12->{2}]
Sizebounds:
(< 0,0,A>, 0) (< 0,0,D>, 0) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G)
(< 1,0,A>, 0) (< 1,0,D>, 50) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G)
(< 2,0,A>, 0) (< 2,0,D>, 50) (< 2,0,E>, 50) (< 2,0,F>, F) (< 2,0,G>, G)
(< 3,0,A>, 50) (< 3,0,D>, 50) (< 3,0,E>, 50) (< 3,0,F>, F) (< 3,0,G>, G)
(< 4,0,A>, 50) (< 4,0,D>, 50) (< 4,0,E>, 50) (< 4,0,F>, 50) (< 4,0,G>, G)
(< 5,0,A>, 50) (< 5,0,D>, 50) (< 5,0,E>, 50) (< 5,0,F>, 50) (< 5,0,G>, 50)
(< 6,0,A>, 50) (< 6,0,D>, 50) (< 6,0,E>, 50) (< 6,0,F>, 50) (< 6,0,G>, 50)
(< 8,0,A>, 0) (< 8,0,D>, 50) (< 8,0,E>, 50) (< 8,0,F>, 50) (< 8,0,G>, 50)
(< 9,0,A>, 50) (< 9,0,D>, 50) (< 9,0,E>, 50) (< 9,0,F>, 50) (< 9,0,G>, 0)
(<10,0,A>, 50) (<10,0,D>, 50) (<10,0,E>, 50) (<10,0,F>, 0) (<10,0,G>, G)
(<11,0,A>, 0) (<11,0,D>, 50) (<11,0,E>, 50) (<11,0,F>, F) (<11,0,G>, G)
(<12,0,A>, 0) (<12,0,D>, 50) (<12,0,E>, 0) (<12,0,F>, F) (<12,0,G>, G)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f0) = 50
p(f15) = 50
p(f25) = 50
p(f33) = 50
p(f42) = 50 + -1*x4
p(f52) = 50 + -1*x4
p(f60) = 50 + -1*x4
The following rules are strictly oriented:
[49 >= F] ==>
f42(A,D,E,F,G) = 50 + -1*F
> 49 + -1*F
= f42(A,D,E,1 + F,G)
The following rules are weakly oriented:
True ==>
f0(A,D,E,F,G) = 50
>= 50
= f15(0,0,E,F,G)
[49 >= D] ==>
f15(A,D,E,F,G) = 50
>= 50
= f15(A,1 + D,E,F,G)
[49 >= E] ==>
f25(A,D,E,F,G) = 50
>= 50
= f25(A,D,1 + E,F,G)
[49 >= A] ==>
f33(A,D,E,F,G) = 50
>= 50
= f33(1 + A,D,E,F,G)
[49 >= G] ==>
f52(A,D,E,F,G) = 50 + -1*F
>= 50 + -1*F
= f52(A,D,E,F,1 + G)
[49 >= A] ==>
f60(A,D,E,F,G) = 50 + -1*F
>= 50 + -1*F
= f60(1 + A,D,E,F,G)
[G >= 50] ==>
f52(A,D,E,F,G) = 50 + -1*F
>= 50 + -1*F
= f60(0,D,E,F,G)
[F >= 50] ==>
f42(A,D,E,F,G) = 50 + -1*F
>= 50 + -1*F
= f52(A,D,E,F,0)
[A >= 50] ==>
f33(A,D,E,F,G) = 50
>= 50
= f42(A,D,E,0,G)
[E >= 50] ==>
f25(A,D,E,F,G) = 50
>= 50
= f33(0,D,E,F,G)
[D >= 50] ==>
f15(A,D,E,F,G) = 50
>= 50
= f25(A,D,0,F,G)
* Step 12: PolyRank WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,D,E,F,G) -> f15(0,0,E,F,G) True (1,1)
1. f15(A,D,E,F,G) -> f15(A,1 + D,E,F,G) [49 >= D] (?,1)
2. f25(A,D,E,F,G) -> f25(A,D,1 + E,F,G) [49 >= E] (?,1)
3. f33(A,D,E,F,G) -> f33(1 + A,D,E,F,G) [49 >= A] (?,1)
4. f42(A,D,E,F,G) -> f42(A,D,E,1 + F,G) [49 >= F] (50,1)
5. f52(A,D,E,F,G) -> f52(A,D,E,F,1 + G) [49 >= G] (50,1)
6. f60(A,D,E,F,G) -> f60(1 + A,D,E,F,G) [49 >= A] (50,1)
8. f52(A,D,E,F,G) -> f60(0,D,E,F,G) [G >= 50] (50,1)
9. f42(A,D,E,F,G) -> f52(A,D,E,F,0) [F >= 50] (50,1)
10. f33(A,D,E,F,G) -> f42(A,D,E,0,G) [A >= 50] (?,1)
11. f25(A,D,E,F,G) -> f33(0,D,E,F,G) [E >= 50] (?,1)
12. f15(A,D,E,F,G) -> f25(A,D,0,F,G) [D >= 50] (1,1)
Signature:
{(f0,5);(f15,5);(f25,5);(f33,5);(f42,5);(f52,5);(f60,5);(f69,5)}
Flow Graph:
[0->{1},1->{1,12},2->{2,11},3->{3,10},4->{4,9},5->{5,8},6->{6},8->{6},9->{5},10->{4},11->{3},12->{2}]
Sizebounds:
(< 0,0,A>, 0) (< 0,0,D>, 0) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G)
(< 1,0,A>, 0) (< 1,0,D>, 50) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G)
(< 2,0,A>, 0) (< 2,0,D>, 50) (< 2,0,E>, 50) (< 2,0,F>, F) (< 2,0,G>, G)
(< 3,0,A>, 50) (< 3,0,D>, 50) (< 3,0,E>, 50) (< 3,0,F>, F) (< 3,0,G>, G)
(< 4,0,A>, 50) (< 4,0,D>, 50) (< 4,0,E>, 50) (< 4,0,F>, 50) (< 4,0,G>, G)
(< 5,0,A>, 50) (< 5,0,D>, 50) (< 5,0,E>, 50) (< 5,0,F>, 50) (< 5,0,G>, 50)
(< 6,0,A>, 50) (< 6,0,D>, 50) (< 6,0,E>, 50) (< 6,0,F>, 50) (< 6,0,G>, 50)
(< 8,0,A>, 0) (< 8,0,D>, 50) (< 8,0,E>, 50) (< 8,0,F>, 50) (< 8,0,G>, 50)
(< 9,0,A>, 50) (< 9,0,D>, 50) (< 9,0,E>, 50) (< 9,0,F>, 50) (< 9,0,G>, 0)
(<10,0,A>, 50) (<10,0,D>, 50) (<10,0,E>, 50) (<10,0,F>, 0) (<10,0,G>, G)
(<11,0,A>, 0) (<11,0,D>, 50) (<11,0,E>, 50) (<11,0,F>, F) (<11,0,G>, G)
(<12,0,A>, 0) (<12,0,D>, 50) (<12,0,E>, 0) (<12,0,F>, F) (<12,0,G>, G)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f0) = 51
p(f15) = 51
p(f25) = 50
p(f33) = 50
p(f42) = 49
p(f52) = 49
p(f60) = 49
The following rules are strictly oriented:
[A >= 50] ==>
f33(A,D,E,F,G) = 50
> 49
= f42(A,D,E,0,G)
[D >= 50] ==>
f15(A,D,E,F,G) = 51
> 50
= f25(A,D,0,F,G)
The following rules are weakly oriented:
True ==>
f0(A,D,E,F,G) = 51
>= 51
= f15(0,0,E,F,G)
[49 >= D] ==>
f15(A,D,E,F,G) = 51
>= 51
= f15(A,1 + D,E,F,G)
[49 >= E] ==>
f25(A,D,E,F,G) = 50
>= 50
= f25(A,D,1 + E,F,G)
[49 >= A] ==>
f33(A,D,E,F,G) = 50
>= 50
= f33(1 + A,D,E,F,G)
[49 >= F] ==>
f42(A,D,E,F,G) = 49
>= 49
= f42(A,D,E,1 + F,G)
[49 >= G] ==>
f52(A,D,E,F,G) = 49
>= 49
= f52(A,D,E,F,1 + G)
[49 >= A] ==>
f60(A,D,E,F,G) = 49
>= 49
= f60(1 + A,D,E,F,G)
[G >= 50] ==>
f52(A,D,E,F,G) = 49
>= 49
= f60(0,D,E,F,G)
[F >= 50] ==>
f42(A,D,E,F,G) = 49
>= 49
= f52(A,D,E,F,0)
[E >= 50] ==>
f25(A,D,E,F,G) = 50
>= 50
= f33(0,D,E,F,G)
* Step 13: PolyRank WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,D,E,F,G) -> f15(0,0,E,F,G) True (1,1)
1. f15(A,D,E,F,G) -> f15(A,1 + D,E,F,G) [49 >= D] (?,1)
2. f25(A,D,E,F,G) -> f25(A,D,1 + E,F,G) [49 >= E] (?,1)
3. f33(A,D,E,F,G) -> f33(1 + A,D,E,F,G) [49 >= A] (?,1)
4. f42(A,D,E,F,G) -> f42(A,D,E,1 + F,G) [49 >= F] (50,1)
5. f52(A,D,E,F,G) -> f52(A,D,E,F,1 + G) [49 >= G] (50,1)
6. f60(A,D,E,F,G) -> f60(1 + A,D,E,F,G) [49 >= A] (50,1)
8. f52(A,D,E,F,G) -> f60(0,D,E,F,G) [G >= 50] (50,1)
9. f42(A,D,E,F,G) -> f52(A,D,E,F,0) [F >= 50] (50,1)
10. f33(A,D,E,F,G) -> f42(A,D,E,0,G) [A >= 50] (51,1)
11. f25(A,D,E,F,G) -> f33(0,D,E,F,G) [E >= 50] (?,1)
12. f15(A,D,E,F,G) -> f25(A,D,0,F,G) [D >= 50] (1,1)
Signature:
{(f0,5);(f15,5);(f25,5);(f33,5);(f42,5);(f52,5);(f60,5);(f69,5)}
Flow Graph:
[0->{1},1->{1,12},2->{2,11},3->{3,10},4->{4,9},5->{5,8},6->{6},8->{6},9->{5},10->{4},11->{3},12->{2}]
Sizebounds:
(< 0,0,A>, 0) (< 0,0,D>, 0) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G)
(< 1,0,A>, 0) (< 1,0,D>, 50) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G)
(< 2,0,A>, 0) (< 2,0,D>, 50) (< 2,0,E>, 50) (< 2,0,F>, F) (< 2,0,G>, G)
(< 3,0,A>, 50) (< 3,0,D>, 50) (< 3,0,E>, 50) (< 3,0,F>, F) (< 3,0,G>, G)
(< 4,0,A>, 50) (< 4,0,D>, 50) (< 4,0,E>, 50) (< 4,0,F>, 50) (< 4,0,G>, G)
(< 5,0,A>, 50) (< 5,0,D>, 50) (< 5,0,E>, 50) (< 5,0,F>, 50) (< 5,0,G>, 50)
(< 6,0,A>, 50) (< 6,0,D>, 50) (< 6,0,E>, 50) (< 6,0,F>, 50) (< 6,0,G>, 50)
(< 8,0,A>, 0) (< 8,0,D>, 50) (< 8,0,E>, 50) (< 8,0,F>, 50) (< 8,0,G>, 50)
(< 9,0,A>, 50) (< 9,0,D>, 50) (< 9,0,E>, 50) (< 9,0,F>, 50) (< 9,0,G>, 0)
(<10,0,A>, 50) (<10,0,D>, 50) (<10,0,E>, 50) (<10,0,F>, 0) (<10,0,G>, G)
(<11,0,A>, 0) (<11,0,D>, 50) (<11,0,E>, 50) (<11,0,F>, F) (<11,0,G>, G)
(<12,0,A>, 0) (<12,0,D>, 50) (<12,0,E>, 0) (<12,0,F>, F) (<12,0,G>, G)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f0) = 50
p(f15) = 50
p(f25) = 50 + -1*x3
p(f33) = 50 + -1*x3
p(f42) = 50 + -1*x3
p(f52) = 50 + -1*x3
p(f60) = 50 + -1*x3
The following rules are strictly oriented:
[49 >= E] ==>
f25(A,D,E,F,G) = 50 + -1*E
> 49 + -1*E
= f25(A,D,1 + E,F,G)
The following rules are weakly oriented:
True ==>
f0(A,D,E,F,G) = 50
>= 50
= f15(0,0,E,F,G)
[49 >= D] ==>
f15(A,D,E,F,G) = 50
>= 50
= f15(A,1 + D,E,F,G)
[49 >= A] ==>
f33(A,D,E,F,G) = 50 + -1*E
>= 50 + -1*E
= f33(1 + A,D,E,F,G)
[49 >= F] ==>
f42(A,D,E,F,G) = 50 + -1*E
>= 50 + -1*E
= f42(A,D,E,1 + F,G)
[49 >= G] ==>
f52(A,D,E,F,G) = 50 + -1*E
>= 50 + -1*E
= f52(A,D,E,F,1 + G)
[49 >= A] ==>
f60(A,D,E,F,G) = 50 + -1*E
>= 50 + -1*E
= f60(1 + A,D,E,F,G)
[G >= 50] ==>
f52(A,D,E,F,G) = 50 + -1*E
>= 50 + -1*E
= f60(0,D,E,F,G)
[F >= 50] ==>
f42(A,D,E,F,G) = 50 + -1*E
>= 50 + -1*E
= f52(A,D,E,F,0)
[A >= 50] ==>
f33(A,D,E,F,G) = 50 + -1*E
>= 50 + -1*E
= f42(A,D,E,0,G)
[E >= 50] ==>
f25(A,D,E,F,G) = 50 + -1*E
>= 50 + -1*E
= f33(0,D,E,F,G)
[D >= 50] ==>
f15(A,D,E,F,G) = 50
>= 50
= f25(A,D,0,F,G)
* Step 14: KnowledgePropagation WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,D,E,F,G) -> f15(0,0,E,F,G) True (1,1)
1. f15(A,D,E,F,G) -> f15(A,1 + D,E,F,G) [49 >= D] (?,1)
2. f25(A,D,E,F,G) -> f25(A,D,1 + E,F,G) [49 >= E] (50,1)
3. f33(A,D,E,F,G) -> f33(1 + A,D,E,F,G) [49 >= A] (?,1)
4. f42(A,D,E,F,G) -> f42(A,D,E,1 + F,G) [49 >= F] (50,1)
5. f52(A,D,E,F,G) -> f52(A,D,E,F,1 + G) [49 >= G] (50,1)
6. f60(A,D,E,F,G) -> f60(1 + A,D,E,F,G) [49 >= A] (50,1)
8. f52(A,D,E,F,G) -> f60(0,D,E,F,G) [G >= 50] (50,1)
9. f42(A,D,E,F,G) -> f52(A,D,E,F,0) [F >= 50] (50,1)
10. f33(A,D,E,F,G) -> f42(A,D,E,0,G) [A >= 50] (51,1)
11. f25(A,D,E,F,G) -> f33(0,D,E,F,G) [E >= 50] (?,1)
12. f15(A,D,E,F,G) -> f25(A,D,0,F,G) [D >= 50] (1,1)
Signature:
{(f0,5);(f15,5);(f25,5);(f33,5);(f42,5);(f52,5);(f60,5);(f69,5)}
Flow Graph:
[0->{1},1->{1,12},2->{2,11},3->{3,10},4->{4,9},5->{5,8},6->{6},8->{6},9->{5},10->{4},11->{3},12->{2}]
Sizebounds:
(< 0,0,A>, 0) (< 0,0,D>, 0) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G)
(< 1,0,A>, 0) (< 1,0,D>, 50) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G)
(< 2,0,A>, 0) (< 2,0,D>, 50) (< 2,0,E>, 50) (< 2,0,F>, F) (< 2,0,G>, G)
(< 3,0,A>, 50) (< 3,0,D>, 50) (< 3,0,E>, 50) (< 3,0,F>, F) (< 3,0,G>, G)
(< 4,0,A>, 50) (< 4,0,D>, 50) (< 4,0,E>, 50) (< 4,0,F>, 50) (< 4,0,G>, G)
(< 5,0,A>, 50) (< 5,0,D>, 50) (< 5,0,E>, 50) (< 5,0,F>, 50) (< 5,0,G>, 50)
(< 6,0,A>, 50) (< 6,0,D>, 50) (< 6,0,E>, 50) (< 6,0,F>, 50) (< 6,0,G>, 50)
(< 8,0,A>, 0) (< 8,0,D>, 50) (< 8,0,E>, 50) (< 8,0,F>, 50) (< 8,0,G>, 50)
(< 9,0,A>, 50) (< 9,0,D>, 50) (< 9,0,E>, 50) (< 9,0,F>, 50) (< 9,0,G>, 0)
(<10,0,A>, 50) (<10,0,D>, 50) (<10,0,E>, 50) (<10,0,F>, 0) (<10,0,G>, G)
(<11,0,A>, 0) (<11,0,D>, 50) (<11,0,E>, 50) (<11,0,F>, F) (<11,0,G>, G)
(<12,0,A>, 0) (<12,0,D>, 50) (<12,0,E>, 0) (<12,0,F>, F) (<12,0,G>, G)
+ Applied Processor:
KnowledgePropagation
+ Details:
We propagate bounds from predecessors.
* Step 15: PolyRank WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,D,E,F,G) -> f15(0,0,E,F,G) True (1,1)
1. f15(A,D,E,F,G) -> f15(A,1 + D,E,F,G) [49 >= D] (?,1)
2. f25(A,D,E,F,G) -> f25(A,D,1 + E,F,G) [49 >= E] (50,1)
3. f33(A,D,E,F,G) -> f33(1 + A,D,E,F,G) [49 >= A] (?,1)
4. f42(A,D,E,F,G) -> f42(A,D,E,1 + F,G) [49 >= F] (50,1)
5. f52(A,D,E,F,G) -> f52(A,D,E,F,1 + G) [49 >= G] (50,1)
6. f60(A,D,E,F,G) -> f60(1 + A,D,E,F,G) [49 >= A] (50,1)
8. f52(A,D,E,F,G) -> f60(0,D,E,F,G) [G >= 50] (50,1)
9. f42(A,D,E,F,G) -> f52(A,D,E,F,0) [F >= 50] (50,1)
10. f33(A,D,E,F,G) -> f42(A,D,E,0,G) [A >= 50] (51,1)
11. f25(A,D,E,F,G) -> f33(0,D,E,F,G) [E >= 50] (50,1)
12. f15(A,D,E,F,G) -> f25(A,D,0,F,G) [D >= 50] (1,1)
Signature:
{(f0,5);(f15,5);(f25,5);(f33,5);(f42,5);(f52,5);(f60,5);(f69,5)}
Flow Graph:
[0->{1},1->{1,12},2->{2,11},3->{3,10},4->{4,9},5->{5,8},6->{6},8->{6},9->{5},10->{4},11->{3},12->{2}]
Sizebounds:
(< 0,0,A>, 0) (< 0,0,D>, 0) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G)
(< 1,0,A>, 0) (< 1,0,D>, 50) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G)
(< 2,0,A>, 0) (< 2,0,D>, 50) (< 2,0,E>, 50) (< 2,0,F>, F) (< 2,0,G>, G)
(< 3,0,A>, 50) (< 3,0,D>, 50) (< 3,0,E>, 50) (< 3,0,F>, F) (< 3,0,G>, G)
(< 4,0,A>, 50) (< 4,0,D>, 50) (< 4,0,E>, 50) (< 4,0,F>, 50) (< 4,0,G>, G)
(< 5,0,A>, 50) (< 5,0,D>, 50) (< 5,0,E>, 50) (< 5,0,F>, 50) (< 5,0,G>, 50)
(< 6,0,A>, 50) (< 6,0,D>, 50) (< 6,0,E>, 50) (< 6,0,F>, 50) (< 6,0,G>, 50)
(< 8,0,A>, 0) (< 8,0,D>, 50) (< 8,0,E>, 50) (< 8,0,F>, 50) (< 8,0,G>, 50)
(< 9,0,A>, 50) (< 9,0,D>, 50) (< 9,0,E>, 50) (< 9,0,F>, 50) (< 9,0,G>, 0)
(<10,0,A>, 50) (<10,0,D>, 50) (<10,0,E>, 50) (<10,0,F>, 0) (<10,0,G>, G)
(<11,0,A>, 0) (<11,0,D>, 50) (<11,0,E>, 50) (<11,0,F>, F) (<11,0,G>, G)
(<12,0,A>, 0) (<12,0,D>, 50) (<12,0,E>, 0) (<12,0,F>, F) (<12,0,G>, G)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f0) = 50
p(f15) = 50 + -1*x2
p(f25) = -1*x2
p(f33) = -1*x2
p(f42) = -1*x2
p(f52) = -1*x2
p(f60) = -1*x2
The following rules are strictly oriented:
[49 >= D] ==>
f15(A,D,E,F,G) = 50 + -1*D
> 49 + -1*D
= f15(A,1 + D,E,F,G)
The following rules are weakly oriented:
True ==>
f0(A,D,E,F,G) = 50
>= 50
= f15(0,0,E,F,G)
[49 >= E] ==>
f25(A,D,E,F,G) = -1*D
>= -1*D
= f25(A,D,1 + E,F,G)
[49 >= A] ==>
f33(A,D,E,F,G) = -1*D
>= -1*D
= f33(1 + A,D,E,F,G)
[49 >= F] ==>
f42(A,D,E,F,G) = -1*D
>= -1*D
= f42(A,D,E,1 + F,G)
[49 >= G] ==>
f52(A,D,E,F,G) = -1*D
>= -1*D
= f52(A,D,E,F,1 + G)
[49 >= A] ==>
f60(A,D,E,F,G) = -1*D
>= -1*D
= f60(1 + A,D,E,F,G)
[G >= 50] ==>
f52(A,D,E,F,G) = -1*D
>= -1*D
= f60(0,D,E,F,G)
[F >= 50] ==>
f42(A,D,E,F,G) = -1*D
>= -1*D
= f52(A,D,E,F,0)
[A >= 50] ==>
f33(A,D,E,F,G) = -1*D
>= -1*D
= f42(A,D,E,0,G)
[E >= 50] ==>
f25(A,D,E,F,G) = -1*D
>= -1*D
= f33(0,D,E,F,G)
[D >= 50] ==>
f15(A,D,E,F,G) = 50 + -1*D
>= -1*D
= f25(A,D,0,F,G)
* Step 16: PolyRank WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,D,E,F,G) -> f15(0,0,E,F,G) True (1,1)
1. f15(A,D,E,F,G) -> f15(A,1 + D,E,F,G) [49 >= D] (50,1)
2. f25(A,D,E,F,G) -> f25(A,D,1 + E,F,G) [49 >= E] (50,1)
3. f33(A,D,E,F,G) -> f33(1 + A,D,E,F,G) [49 >= A] (?,1)
4. f42(A,D,E,F,G) -> f42(A,D,E,1 + F,G) [49 >= F] (50,1)
5. f52(A,D,E,F,G) -> f52(A,D,E,F,1 + G) [49 >= G] (50,1)
6. f60(A,D,E,F,G) -> f60(1 + A,D,E,F,G) [49 >= A] (50,1)
8. f52(A,D,E,F,G) -> f60(0,D,E,F,G) [G >= 50] (50,1)
9. f42(A,D,E,F,G) -> f52(A,D,E,F,0) [F >= 50] (50,1)
10. f33(A,D,E,F,G) -> f42(A,D,E,0,G) [A >= 50] (51,1)
11. f25(A,D,E,F,G) -> f33(0,D,E,F,G) [E >= 50] (50,1)
12. f15(A,D,E,F,G) -> f25(A,D,0,F,G) [D >= 50] (1,1)
Signature:
{(f0,5);(f15,5);(f25,5);(f33,5);(f42,5);(f52,5);(f60,5);(f69,5)}
Flow Graph:
[0->{1},1->{1,12},2->{2,11},3->{3,10},4->{4,9},5->{5,8},6->{6},8->{6},9->{5},10->{4},11->{3},12->{2}]
Sizebounds:
(< 0,0,A>, 0) (< 0,0,D>, 0) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G)
(< 1,0,A>, 0) (< 1,0,D>, 50) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G)
(< 2,0,A>, 0) (< 2,0,D>, 50) (< 2,0,E>, 50) (< 2,0,F>, F) (< 2,0,G>, G)
(< 3,0,A>, 50) (< 3,0,D>, 50) (< 3,0,E>, 50) (< 3,0,F>, F) (< 3,0,G>, G)
(< 4,0,A>, 50) (< 4,0,D>, 50) (< 4,0,E>, 50) (< 4,0,F>, 50) (< 4,0,G>, G)
(< 5,0,A>, 50) (< 5,0,D>, 50) (< 5,0,E>, 50) (< 5,0,F>, 50) (< 5,0,G>, 50)
(< 6,0,A>, 50) (< 6,0,D>, 50) (< 6,0,E>, 50) (< 6,0,F>, 50) (< 6,0,G>, 50)
(< 8,0,A>, 0) (< 8,0,D>, 50) (< 8,0,E>, 50) (< 8,0,F>, 50) (< 8,0,G>, 50)
(< 9,0,A>, 50) (< 9,0,D>, 50) (< 9,0,E>, 50) (< 9,0,F>, 50) (< 9,0,G>, 0)
(<10,0,A>, 50) (<10,0,D>, 50) (<10,0,E>, 50) (<10,0,F>, 0) (<10,0,G>, G)
(<11,0,A>, 0) (<11,0,D>, 50) (<11,0,E>, 50) (<11,0,F>, F) (<11,0,G>, G)
(<12,0,A>, 0) (<12,0,D>, 50) (<12,0,E>, 0) (<12,0,F>, F) (<12,0,G>, G)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [3], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f33) = 50 + -1*x1
The following rules are strictly oriented:
[49 >= A] ==>
f33(A,D,E,F,G) = 50 + -1*A
> 49 + -1*A
= f33(1 + A,D,E,F,G)
The following rules are weakly oriented:
We use the following global sizebounds:
(< 0,0,A>, 0) (< 0,0,D>, 0) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G)
(< 1,0,A>, 0) (< 1,0,D>, 50) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G)
(< 2,0,A>, 0) (< 2,0,D>, 50) (< 2,0,E>, 50) (< 2,0,F>, F) (< 2,0,G>, G)
(< 3,0,A>, 50) (< 3,0,D>, 50) (< 3,0,E>, 50) (< 3,0,F>, F) (< 3,0,G>, G)
(< 4,0,A>, 50) (< 4,0,D>, 50) (< 4,0,E>, 50) (< 4,0,F>, 50) (< 4,0,G>, G)
(< 5,0,A>, 50) (< 5,0,D>, 50) (< 5,0,E>, 50) (< 5,0,F>, 50) (< 5,0,G>, 50)
(< 6,0,A>, 50) (< 6,0,D>, 50) (< 6,0,E>, 50) (< 6,0,F>, 50) (< 6,0,G>, 50)
(< 8,0,A>, 0) (< 8,0,D>, 50) (< 8,0,E>, 50) (< 8,0,F>, 50) (< 8,0,G>, 50)
(< 9,0,A>, 50) (< 9,0,D>, 50) (< 9,0,E>, 50) (< 9,0,F>, 50) (< 9,0,G>, 0)
(<10,0,A>, 50) (<10,0,D>, 50) (<10,0,E>, 50) (<10,0,F>, 0) (<10,0,G>, G)
(<11,0,A>, 0) (<11,0,D>, 50) (<11,0,E>, 50) (<11,0,F>, F) (<11,0,G>, G)
(<12,0,A>, 0) (<12,0,D>, 50) (<12,0,E>, 0) (<12,0,F>, F) (<12,0,G>, G)
* Step 17: KnowledgePropagation WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,D,E,F,G) -> f15(0,0,E,F,G) True (1,1)
1. f15(A,D,E,F,G) -> f15(A,1 + D,E,F,G) [49 >= D] (50,1)
2. f25(A,D,E,F,G) -> f25(A,D,1 + E,F,G) [49 >= E] (50,1)
3. f33(A,D,E,F,G) -> f33(1 + A,D,E,F,G) [49 >= A] (2500,1)
4. f42(A,D,E,F,G) -> f42(A,D,E,1 + F,G) [49 >= F] (50,1)
5. f52(A,D,E,F,G) -> f52(A,D,E,F,1 + G) [49 >= G] (50,1)
6. f60(A,D,E,F,G) -> f60(1 + A,D,E,F,G) [49 >= A] (50,1)
8. f52(A,D,E,F,G) -> f60(0,D,E,F,G) [G >= 50] (50,1)
9. f42(A,D,E,F,G) -> f52(A,D,E,F,0) [F >= 50] (50,1)
10. f33(A,D,E,F,G) -> f42(A,D,E,0,G) [A >= 50] (51,1)
11. f25(A,D,E,F,G) -> f33(0,D,E,F,G) [E >= 50] (50,1)
12. f15(A,D,E,F,G) -> f25(A,D,0,F,G) [D >= 50] (1,1)
Signature:
{(f0,5);(f15,5);(f25,5);(f33,5);(f42,5);(f52,5);(f60,5);(f69,5)}
Flow Graph:
[0->{1},1->{1,12},2->{2,11},3->{3,10},4->{4,9},5->{5,8},6->{6},8->{6},9->{5},10->{4},11->{3},12->{2}]
Sizebounds:
(< 0,0,A>, 0) (< 0,0,D>, 0) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G)
(< 1,0,A>, 0) (< 1,0,D>, 50) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G)
(< 2,0,A>, 0) (< 2,0,D>, 50) (< 2,0,E>, 50) (< 2,0,F>, F) (< 2,0,G>, G)
(< 3,0,A>, 50) (< 3,0,D>, 50) (< 3,0,E>, 50) (< 3,0,F>, F) (< 3,0,G>, G)
(< 4,0,A>, 50) (< 4,0,D>, 50) (< 4,0,E>, 50) (< 4,0,F>, 50) (< 4,0,G>, G)
(< 5,0,A>, 50) (< 5,0,D>, 50) (< 5,0,E>, 50) (< 5,0,F>, 50) (< 5,0,G>, 50)
(< 6,0,A>, 50) (< 6,0,D>, 50) (< 6,0,E>, 50) (< 6,0,F>, 50) (< 6,0,G>, 50)
(< 8,0,A>, 0) (< 8,0,D>, 50) (< 8,0,E>, 50) (< 8,0,F>, 50) (< 8,0,G>, 50)
(< 9,0,A>, 50) (< 9,0,D>, 50) (< 9,0,E>, 50) (< 9,0,F>, 50) (< 9,0,G>, 0)
(<10,0,A>, 50) (<10,0,D>, 50) (<10,0,E>, 50) (<10,0,F>, 0) (<10,0,G>, G)
(<11,0,A>, 0) (<11,0,D>, 50) (<11,0,E>, 50) (<11,0,F>, F) (<11,0,G>, G)
(<12,0,A>, 0) (<12,0,D>, 50) (<12,0,E>, 0) (<12,0,F>, F) (<12,0,G>, G)
+ Applied Processor:
KnowledgePropagation
+ Details:
The problem is already solved.
WORST_CASE(?,O(1))