WORST_CASE(?,O(1))
* Step 1: RestrictVarsProcessor WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S) -> f12(3,T,3,1,0,F,G,H,I,J,K,L,M,N,O,P,Q,R,S) True (1,1)
1. f12(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S) -> f12(A,B,C,T,1 + E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S) [C >= 1 + E] (?,1)
2. f24(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S) -> f24(A,B,C,D,E,F,1 + G,T,I,J,K,L,M,N,O,P,Q,R,S) [F >= 1 + G] (?,1)
3. f36(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S) -> f36(A,B,C,D,E,F,G,H,I,1 + J,T,L,M,N,O,P,Q,R,S) [I >= 1 + J] (?,1)
4. f36(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S) -> f46(A,B,C,D,E,F,G,H,I,J,K,K,K,N,O,P,Q,R,S) [J >= I] (?,1)
5. f24(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S) -> f36(A,B,C,D,E,F,G,H,A,0,1,L,M,H,H,T,Q,R,S) [G >= F] (?,1)
6. f12(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S) -> f24(A,B,C,D,E,A,0,1,I,J,K,L,M,N,O,P,D,D,T) [E >= C] (?,1)
Signature:
{(f0,19);(f12,19);(f24,19);(f36,19);(f46,19)}
Flow Graph:
[0->{1,6},1->{1,6},2->{2,5},3->{3,4},4->{},5->{3,4},6->{2,5}]
+ Applied Processor:
RestrictVarsProcessor
+ Details:
We removed the arguments [B,L,M,N,O,P,Q,R,S] .
* Step 2: LocalSizeboundsProc WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,C,D,E,F,G,H,I,J,K) -> f12(3,3,1,0,F,G,H,I,J,K) True (1,1)
1. f12(A,C,D,E,F,G,H,I,J,K) -> f12(A,C,T,1 + E,F,G,H,I,J,K) [C >= 1 + E] (?,1)
2. f24(A,C,D,E,F,G,H,I,J,K) -> f24(A,C,D,E,F,1 + G,T,I,J,K) [F >= 1 + G] (?,1)
3. f36(A,C,D,E,F,G,H,I,J,K) -> f36(A,C,D,E,F,G,H,I,1 + J,T) [I >= 1 + J] (?,1)
4. f36(A,C,D,E,F,G,H,I,J,K) -> f46(A,C,D,E,F,G,H,I,J,K) [J >= I] (?,1)
5. f24(A,C,D,E,F,G,H,I,J,K) -> f36(A,C,D,E,F,G,H,A,0,1) [G >= F] (?,1)
6. f12(A,C,D,E,F,G,H,I,J,K) -> f24(A,C,D,E,A,0,1,I,J,K) [E >= C] (?,1)
Signature:
{(f0,10);(f12,10);(f24,10);(f36,10);(f46,10)}
Flow Graph:
[0->{1,6},1->{1,6},2->{2,5},3->{3,4},4->{},5->{3,4},6->{2,5}]
+ Applied Processor:
LocalSizeboundsProc
+ Details:
LocalSizebounds generated; rvgraph
(<0,0,A>, 3, .= 3) (<0,0,C>, 3, .= 3) (<0,0,D>, 1, .= 1) (<0,0,E>, 0, .= 0) (<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) (<0,0,K>, K, .= 0)
(<1,0,A>, A, .= 0) (<1,0,C>, C, .= 0) (<1,0,D>, ?, .?) (<1,0,E>, 1 + E, .+ 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) (<1,0,K>, K, .= 0)
(<2,0,A>, A, .= 0) (<2,0,C>, C, .= 0) (<2,0,D>, D, .= 0) (<2,0,E>, E, .= 0) (<2,0,F>, F, .= 0) (<2,0,G>, 1 + G, .+ 1) (<2,0,H>, ?, .?) (<2,0,I>, I, .= 0) (<2,0,J>, J, .= 0) (<2,0,K>, K, .= 0)
(<3,0,A>, A, .= 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) (<3,0,I>, I, .= 0) (<3,0,J>, 1 + J, .+ 1) (<3,0,K>, ?, .?)
(<4,0,A>, A, .= 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) (<4,0,K>, K, .= 0)
(<5,0,A>, A, .= 0) (<5,0,C>, C, .= 0) (<5,0,D>, D, .= 0) (<5,0,E>, E, .= 0) (<5,0,F>, F, .= 0) (<5,0,G>, G, .= 0) (<5,0,H>, H, .= 0) (<5,0,I>, A, .= 0) (<5,0,J>, 0, .= 0) (<5,0,K>, 1, .= 1)
(<6,0,A>, A, .= 0) (<6,0,C>, C, .= 0) (<6,0,D>, D, .= 0) (<6,0,E>, E, .= 0) (<6,0,F>, A, .= 0) (<6,0,G>, 0, .= 0) (<6,0,H>, 1, .= 1) (<6,0,I>, I, .= 0) (<6,0,J>, J, .= 0) (<6,0,K>, K, .= 0)
* Step 3: SizeboundsProc WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,C,D,E,F,G,H,I,J,K) -> f12(3,3,1,0,F,G,H,I,J,K) True (1,1)
1. f12(A,C,D,E,F,G,H,I,J,K) -> f12(A,C,T,1 + E,F,G,H,I,J,K) [C >= 1 + E] (?,1)
2. f24(A,C,D,E,F,G,H,I,J,K) -> f24(A,C,D,E,F,1 + G,T,I,J,K) [F >= 1 + G] (?,1)
3. f36(A,C,D,E,F,G,H,I,J,K) -> f36(A,C,D,E,F,G,H,I,1 + J,T) [I >= 1 + J] (?,1)
4. f36(A,C,D,E,F,G,H,I,J,K) -> f46(A,C,D,E,F,G,H,I,J,K) [J >= I] (?,1)
5. f24(A,C,D,E,F,G,H,I,J,K) -> f36(A,C,D,E,F,G,H,A,0,1) [G >= F] (?,1)
6. f12(A,C,D,E,F,G,H,I,J,K) -> f24(A,C,D,E,A,0,1,I,J,K) [E >= C] (?,1)
Signature:
{(f0,10);(f12,10);(f24,10);(f36,10);(f46,10)}
Flow Graph:
[0->{1,6},1->{1,6},2->{2,5},3->{3,4},4->{},5->{3,4},6->{2,5}]
Sizebounds:
(<0,0,A>, ?) (<0,0,C>, ?) (<0,0,D>, ?) (<0,0,E>, ?) (<0,0,F>, ?) (<0,0,G>, ?) (<0,0,H>, ?) (<0,0,I>, ?) (<0,0,J>, ?) (<0,0,K>, ?)
(<1,0,A>, ?) (<1,0,C>, ?) (<1,0,D>, ?) (<1,0,E>, ?) (<1,0,F>, ?) (<1,0,G>, ?) (<1,0,H>, ?) (<1,0,I>, ?) (<1,0,J>, ?) (<1,0,K>, ?)
(<2,0,A>, ?) (<2,0,C>, ?) (<2,0,D>, ?) (<2,0,E>, ?) (<2,0,F>, ?) (<2,0,G>, ?) (<2,0,H>, ?) (<2,0,I>, ?) (<2,0,J>, ?) (<2,0,K>, ?)
(<3,0,A>, ?) (<3,0,C>, ?) (<3,0,D>, ?) (<3,0,E>, ?) (<3,0,F>, ?) (<3,0,G>, ?) (<3,0,H>, ?) (<3,0,I>, ?) (<3,0,J>, ?) (<3,0,K>, ?)
(<4,0,A>, ?) (<4,0,C>, ?) (<4,0,D>, ?) (<4,0,E>, ?) (<4,0,F>, ?) (<4,0,G>, ?) (<4,0,H>, ?) (<4,0,I>, ?) (<4,0,J>, ?) (<4,0,K>, ?)
(<5,0,A>, ?) (<5,0,C>, ?) (<5,0,D>, ?) (<5,0,E>, ?) (<5,0,F>, ?) (<5,0,G>, ?) (<5,0,H>, ?) (<5,0,I>, ?) (<5,0,J>, ?) (<5,0,K>, ?)
(<6,0,A>, ?) (<6,0,C>, ?) (<6,0,D>, ?) (<6,0,E>, ?) (<6,0,F>, ?) (<6,0,G>, ?) (<6,0,H>, ?) (<6,0,I>, ?) (<6,0,J>, ?) (<6,0,K>, ?)
+ Applied Processor:
SizeboundsProc
+ Details:
Sizebounds computed:
(<0,0,A>, 3) (<0,0,C>, 3) (<0,0,D>, 1) (<0,0,E>, 0) (<0,0,F>, F) (<0,0,G>, G) (<0,0,H>, H) (<0,0,I>, I) (<0,0,J>, J) (<0,0,K>, K)
(<1,0,A>, 3) (<1,0,C>, 3) (<1,0,D>, ?) (<1,0,E>, 3) (<1,0,F>, F) (<1,0,G>, G) (<1,0,H>, H) (<1,0,I>, I) (<1,0,J>, J) (<1,0,K>, K)
(<2,0,A>, 3) (<2,0,C>, 3) (<2,0,D>, ?) (<2,0,E>, 3) (<2,0,F>, 3) (<2,0,G>, 3) (<2,0,H>, ?) (<2,0,I>, I) (<2,0,J>, J) (<2,0,K>, K)
(<3,0,A>, 3) (<3,0,C>, 3) (<3,0,D>, ?) (<3,0,E>, 3) (<3,0,F>, 3) (<3,0,G>, 3) (<3,0,H>, ?) (<3,0,I>, 3) (<3,0,J>, 3) (<3,0,K>, ?)
(<4,0,A>, 3) (<4,0,C>, 3) (<4,0,D>, ?) (<4,0,E>, 3) (<4,0,F>, 3) (<4,0,G>, 3) (<4,0,H>, ?) (<4,0,I>, 3) (<4,0,J>, 3) (<4,0,K>, ?)
(<5,0,A>, 3) (<5,0,C>, 3) (<5,0,D>, ?) (<5,0,E>, 3) (<5,0,F>, 3) (<5,0,G>, 3) (<5,0,H>, ?) (<5,0,I>, 3) (<5,0,J>, 0) (<5,0,K>, 1)
(<6,0,A>, 3) (<6,0,C>, 3) (<6,0,D>, ?) (<6,0,E>, 3) (<6,0,F>, 3) (<6,0,G>, 0) (<6,0,H>, 1) (<6,0,I>, I) (<6,0,J>, J) (<6,0,K>, K)
* Step 4: UnsatPaths WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,C,D,E,F,G,H,I,J,K) -> f12(3,3,1,0,F,G,H,I,J,K) True (1,1)
1. f12(A,C,D,E,F,G,H,I,J,K) -> f12(A,C,T,1 + E,F,G,H,I,J,K) [C >= 1 + E] (?,1)
2. f24(A,C,D,E,F,G,H,I,J,K) -> f24(A,C,D,E,F,1 + G,T,I,J,K) [F >= 1 + G] (?,1)
3. f36(A,C,D,E,F,G,H,I,J,K) -> f36(A,C,D,E,F,G,H,I,1 + J,T) [I >= 1 + J] (?,1)
4. f36(A,C,D,E,F,G,H,I,J,K) -> f46(A,C,D,E,F,G,H,I,J,K) [J >= I] (?,1)
5. f24(A,C,D,E,F,G,H,I,J,K) -> f36(A,C,D,E,F,G,H,A,0,1) [G >= F] (?,1)
6. f12(A,C,D,E,F,G,H,I,J,K) -> f24(A,C,D,E,A,0,1,I,J,K) [E >= C] (?,1)
Signature:
{(f0,10);(f12,10);(f24,10);(f36,10);(f46,10)}
Flow Graph:
[0->{1,6},1->{1,6},2->{2,5},3->{3,4},4->{},5->{3,4},6->{2,5}]
Sizebounds:
(<0,0,A>, 3) (<0,0,C>, 3) (<0,0,D>, 1) (<0,0,E>, 0) (<0,0,F>, F) (<0,0,G>, G) (<0,0,H>, H) (<0,0,I>, I) (<0,0,J>, J) (<0,0,K>, K)
(<1,0,A>, 3) (<1,0,C>, 3) (<1,0,D>, ?) (<1,0,E>, 3) (<1,0,F>, F) (<1,0,G>, G) (<1,0,H>, H) (<1,0,I>, I) (<1,0,J>, J) (<1,0,K>, K)
(<2,0,A>, 3) (<2,0,C>, 3) (<2,0,D>, ?) (<2,0,E>, 3) (<2,0,F>, 3) (<2,0,G>, 3) (<2,0,H>, ?) (<2,0,I>, I) (<2,0,J>, J) (<2,0,K>, K)
(<3,0,A>, 3) (<3,0,C>, 3) (<3,0,D>, ?) (<3,0,E>, 3) (<3,0,F>, 3) (<3,0,G>, 3) (<3,0,H>, ?) (<3,0,I>, 3) (<3,0,J>, 3) (<3,0,K>, ?)
(<4,0,A>, 3) (<4,0,C>, 3) (<4,0,D>, ?) (<4,0,E>, 3) (<4,0,F>, 3) (<4,0,G>, 3) (<4,0,H>, ?) (<4,0,I>, 3) (<4,0,J>, 3) (<4,0,K>, ?)
(<5,0,A>, 3) (<5,0,C>, 3) (<5,0,D>, ?) (<5,0,E>, 3) (<5,0,F>, 3) (<5,0,G>, 3) (<5,0,H>, ?) (<5,0,I>, 3) (<5,0,J>, 0) (<5,0,K>, 1)
(<6,0,A>, 3) (<6,0,C>, 3) (<6,0,D>, ?) (<6,0,E>, 3) (<6,0,F>, 3) (<6,0,G>, 0) (<6,0,H>, 1) (<6,0,I>, I) (<6,0,J>, J) (<6,0,K>, K)
+ Applied Processor:
UnsatPaths
+ Details:
We remove following edges from the transition graph: [(0,6)]
* Step 5: LeafRules WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,C,D,E,F,G,H,I,J,K) -> f12(3,3,1,0,F,G,H,I,J,K) True (1,1)
1. f12(A,C,D,E,F,G,H,I,J,K) -> f12(A,C,T,1 + E,F,G,H,I,J,K) [C >= 1 + E] (?,1)
2. f24(A,C,D,E,F,G,H,I,J,K) -> f24(A,C,D,E,F,1 + G,T,I,J,K) [F >= 1 + G] (?,1)
3. f36(A,C,D,E,F,G,H,I,J,K) -> f36(A,C,D,E,F,G,H,I,1 + J,T) [I >= 1 + J] (?,1)
4. f36(A,C,D,E,F,G,H,I,J,K) -> f46(A,C,D,E,F,G,H,I,J,K) [J >= I] (?,1)
5. f24(A,C,D,E,F,G,H,I,J,K) -> f36(A,C,D,E,F,G,H,A,0,1) [G >= F] (?,1)
6. f12(A,C,D,E,F,G,H,I,J,K) -> f24(A,C,D,E,A,0,1,I,J,K) [E >= C] (?,1)
Signature:
{(f0,10);(f12,10);(f24,10);(f36,10);(f46,10)}
Flow Graph:
[0->{1},1->{1,6},2->{2,5},3->{3,4},4->{},5->{3,4},6->{2,5}]
Sizebounds:
(<0,0,A>, 3) (<0,0,C>, 3) (<0,0,D>, 1) (<0,0,E>, 0) (<0,0,F>, F) (<0,0,G>, G) (<0,0,H>, H) (<0,0,I>, I) (<0,0,J>, J) (<0,0,K>, K)
(<1,0,A>, 3) (<1,0,C>, 3) (<1,0,D>, ?) (<1,0,E>, 3) (<1,0,F>, F) (<1,0,G>, G) (<1,0,H>, H) (<1,0,I>, I) (<1,0,J>, J) (<1,0,K>, K)
(<2,0,A>, 3) (<2,0,C>, 3) (<2,0,D>, ?) (<2,0,E>, 3) (<2,0,F>, 3) (<2,0,G>, 3) (<2,0,H>, ?) (<2,0,I>, I) (<2,0,J>, J) (<2,0,K>, K)
(<3,0,A>, 3) (<3,0,C>, 3) (<3,0,D>, ?) (<3,0,E>, 3) (<3,0,F>, 3) (<3,0,G>, 3) (<3,0,H>, ?) (<3,0,I>, 3) (<3,0,J>, 3) (<3,0,K>, ?)
(<4,0,A>, 3) (<4,0,C>, 3) (<4,0,D>, ?) (<4,0,E>, 3) (<4,0,F>, 3) (<4,0,G>, 3) (<4,0,H>, ?) (<4,0,I>, 3) (<4,0,J>, 3) (<4,0,K>, ?)
(<5,0,A>, 3) (<5,0,C>, 3) (<5,0,D>, ?) (<5,0,E>, 3) (<5,0,F>, 3) (<5,0,G>, 3) (<5,0,H>, ?) (<5,0,I>, 3) (<5,0,J>, 0) (<5,0,K>, 1)
(<6,0,A>, 3) (<6,0,C>, 3) (<6,0,D>, ?) (<6,0,E>, 3) (<6,0,F>, 3) (<6,0,G>, 0) (<6,0,H>, 1) (<6,0,I>, I) (<6,0,J>, J) (<6,0,K>, K)
+ Applied Processor:
LeafRules
+ Details:
The following transitions are estimated by its predecessors and are removed [4]
* Step 6: PolyRank WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,C,D,E,F,G,H,I,J,K) -> f12(3,3,1,0,F,G,H,I,J,K) True (1,1)
1. f12(A,C,D,E,F,G,H,I,J,K) -> f12(A,C,T,1 + E,F,G,H,I,J,K) [C >= 1 + E] (?,1)
2. f24(A,C,D,E,F,G,H,I,J,K) -> f24(A,C,D,E,F,1 + G,T,I,J,K) [F >= 1 + G] (?,1)
3. f36(A,C,D,E,F,G,H,I,J,K) -> f36(A,C,D,E,F,G,H,I,1 + J,T) [I >= 1 + J] (?,1)
5. f24(A,C,D,E,F,G,H,I,J,K) -> f36(A,C,D,E,F,G,H,A,0,1) [G >= F] (?,1)
6. f12(A,C,D,E,F,G,H,I,J,K) -> f24(A,C,D,E,A,0,1,I,J,K) [E >= C] (?,1)
Signature:
{(f0,10);(f12,10);(f24,10);(f36,10);(f46,10)}
Flow Graph:
[0->{1},1->{1,6},2->{2,5},3->{3},5->{3},6->{2,5}]
Sizebounds:
(<0,0,A>, 3) (<0,0,C>, 3) (<0,0,D>, 1) (<0,0,E>, 0) (<0,0,F>, F) (<0,0,G>, G) (<0,0,H>, H) (<0,0,I>, I) (<0,0,J>, J) (<0,0,K>, K)
(<1,0,A>, 3) (<1,0,C>, 3) (<1,0,D>, ?) (<1,0,E>, 3) (<1,0,F>, F) (<1,0,G>, G) (<1,0,H>, H) (<1,0,I>, I) (<1,0,J>, J) (<1,0,K>, K)
(<2,0,A>, 3) (<2,0,C>, 3) (<2,0,D>, ?) (<2,0,E>, 3) (<2,0,F>, 3) (<2,0,G>, 3) (<2,0,H>, ?) (<2,0,I>, I) (<2,0,J>, J) (<2,0,K>, K)
(<3,0,A>, 3) (<3,0,C>, 3) (<3,0,D>, ?) (<3,0,E>, 3) (<3,0,F>, 3) (<3,0,G>, 3) (<3,0,H>, ?) (<3,0,I>, 3) (<3,0,J>, 3) (<3,0,K>, ?)
(<5,0,A>, 3) (<5,0,C>, 3) (<5,0,D>, ?) (<5,0,E>, 3) (<5,0,F>, 3) (<5,0,G>, 3) (<5,0,H>, ?) (<5,0,I>, 3) (<5,0,J>, 0) (<5,0,K>, 1)
(<6,0,A>, 3) (<6,0,C>, 3) (<6,0,D>, ?) (<6,0,E>, 3) (<6,0,F>, 3) (<6,0,G>, 0) (<6,0,H>, 1) (<6,0,I>, I) (<6,0,J>, J) (<6,0,K>, K)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f0) = 1
p(f12) = 1
p(f24) = 0
p(f36) = 0
The following rules are strictly oriented:
[E >= C] ==>
f12(A,C,D,E,F,G,H,I,J,K) = 1
> 0
= f24(A,C,D,E,A,0,1,I,J,K)
The following rules are weakly oriented:
True ==>
f0(A,C,D,E,F,G,H,I,J,K) = 1
>= 1
= f12(3,3,1,0,F,G,H,I,J,K)
[C >= 1 + E] ==>
f12(A,C,D,E,F,G,H,I,J,K) = 1
>= 1
= f12(A,C,T,1 + E,F,G,H,I,J,K)
[F >= 1 + G] ==>
f24(A,C,D,E,F,G,H,I,J,K) = 0
>= 0
= f24(A,C,D,E,F,1 + G,T,I,J,K)
[I >= 1 + J] ==>
f36(A,C,D,E,F,G,H,I,J,K) = 0
>= 0
= f36(A,C,D,E,F,G,H,I,1 + J,T)
[G >= F] ==>
f24(A,C,D,E,F,G,H,I,J,K) = 0
>= 0
= f36(A,C,D,E,F,G,H,A,0,1)
* Step 7: PolyRank WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,C,D,E,F,G,H,I,J,K) -> f12(3,3,1,0,F,G,H,I,J,K) True (1,1)
1. f12(A,C,D,E,F,G,H,I,J,K) -> f12(A,C,T,1 + E,F,G,H,I,J,K) [C >= 1 + E] (?,1)
2. f24(A,C,D,E,F,G,H,I,J,K) -> f24(A,C,D,E,F,1 + G,T,I,J,K) [F >= 1 + G] (?,1)
3. f36(A,C,D,E,F,G,H,I,J,K) -> f36(A,C,D,E,F,G,H,I,1 + J,T) [I >= 1 + J] (?,1)
5. f24(A,C,D,E,F,G,H,I,J,K) -> f36(A,C,D,E,F,G,H,A,0,1) [G >= F] (?,1)
6. f12(A,C,D,E,F,G,H,I,J,K) -> f24(A,C,D,E,A,0,1,I,J,K) [E >= C] (1,1)
Signature:
{(f0,10);(f12,10);(f24,10);(f36,10);(f46,10)}
Flow Graph:
[0->{1},1->{1,6},2->{2,5},3->{3},5->{3},6->{2,5}]
Sizebounds:
(<0,0,A>, 3) (<0,0,C>, 3) (<0,0,D>, 1) (<0,0,E>, 0) (<0,0,F>, F) (<0,0,G>, G) (<0,0,H>, H) (<0,0,I>, I) (<0,0,J>, J) (<0,0,K>, K)
(<1,0,A>, 3) (<1,0,C>, 3) (<1,0,D>, ?) (<1,0,E>, 3) (<1,0,F>, F) (<1,0,G>, G) (<1,0,H>, H) (<1,0,I>, I) (<1,0,J>, J) (<1,0,K>, K)
(<2,0,A>, 3) (<2,0,C>, 3) (<2,0,D>, ?) (<2,0,E>, 3) (<2,0,F>, 3) (<2,0,G>, 3) (<2,0,H>, ?) (<2,0,I>, I) (<2,0,J>, J) (<2,0,K>, K)
(<3,0,A>, 3) (<3,0,C>, 3) (<3,0,D>, ?) (<3,0,E>, 3) (<3,0,F>, 3) (<3,0,G>, 3) (<3,0,H>, ?) (<3,0,I>, 3) (<3,0,J>, 3) (<3,0,K>, ?)
(<5,0,A>, 3) (<5,0,C>, 3) (<5,0,D>, ?) (<5,0,E>, 3) (<5,0,F>, 3) (<5,0,G>, 3) (<5,0,H>, ?) (<5,0,I>, 3) (<5,0,J>, 0) (<5,0,K>, 1)
(<6,0,A>, 3) (<6,0,C>, 3) (<6,0,D>, ?) (<6,0,E>, 3) (<6,0,F>, 3) (<6,0,G>, 0) (<6,0,H>, 1) (<6,0,I>, I) (<6,0,J>, J) (<6,0,K>, K)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f0) = 1
p(f12) = 1
p(f24) = 1
p(f36) = 0
The following rules are strictly oriented:
[G >= F] ==>
f24(A,C,D,E,F,G,H,I,J,K) = 1
> 0
= f36(A,C,D,E,F,G,H,A,0,1)
The following rules are weakly oriented:
True ==>
f0(A,C,D,E,F,G,H,I,J,K) = 1
>= 1
= f12(3,3,1,0,F,G,H,I,J,K)
[C >= 1 + E] ==>
f12(A,C,D,E,F,G,H,I,J,K) = 1
>= 1
= f12(A,C,T,1 + E,F,G,H,I,J,K)
[F >= 1 + G] ==>
f24(A,C,D,E,F,G,H,I,J,K) = 1
>= 1
= f24(A,C,D,E,F,1 + G,T,I,J,K)
[I >= 1 + J] ==>
f36(A,C,D,E,F,G,H,I,J,K) = 0
>= 0
= f36(A,C,D,E,F,G,H,I,1 + J,T)
[E >= C] ==>
f12(A,C,D,E,F,G,H,I,J,K) = 1
>= 1
= f24(A,C,D,E,A,0,1,I,J,K)
* Step 8: PolyRank WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,C,D,E,F,G,H,I,J,K) -> f12(3,3,1,0,F,G,H,I,J,K) True (1,1)
1. f12(A,C,D,E,F,G,H,I,J,K) -> f12(A,C,T,1 + E,F,G,H,I,J,K) [C >= 1 + E] (?,1)
2. f24(A,C,D,E,F,G,H,I,J,K) -> f24(A,C,D,E,F,1 + G,T,I,J,K) [F >= 1 + G] (?,1)
3. f36(A,C,D,E,F,G,H,I,J,K) -> f36(A,C,D,E,F,G,H,I,1 + J,T) [I >= 1 + J] (?,1)
5. f24(A,C,D,E,F,G,H,I,J,K) -> f36(A,C,D,E,F,G,H,A,0,1) [G >= F] (1,1)
6. f12(A,C,D,E,F,G,H,I,J,K) -> f24(A,C,D,E,A,0,1,I,J,K) [E >= C] (1,1)
Signature:
{(f0,10);(f12,10);(f24,10);(f36,10);(f46,10)}
Flow Graph:
[0->{1},1->{1,6},2->{2,5},3->{3},5->{3},6->{2,5}]
Sizebounds:
(<0,0,A>, 3) (<0,0,C>, 3) (<0,0,D>, 1) (<0,0,E>, 0) (<0,0,F>, F) (<0,0,G>, G) (<0,0,H>, H) (<0,0,I>, I) (<0,0,J>, J) (<0,0,K>, K)
(<1,0,A>, 3) (<1,0,C>, 3) (<1,0,D>, ?) (<1,0,E>, 3) (<1,0,F>, F) (<1,0,G>, G) (<1,0,H>, H) (<1,0,I>, I) (<1,0,J>, J) (<1,0,K>, K)
(<2,0,A>, 3) (<2,0,C>, 3) (<2,0,D>, ?) (<2,0,E>, 3) (<2,0,F>, 3) (<2,0,G>, 3) (<2,0,H>, ?) (<2,0,I>, I) (<2,0,J>, J) (<2,0,K>, K)
(<3,0,A>, 3) (<3,0,C>, 3) (<3,0,D>, ?) (<3,0,E>, 3) (<3,0,F>, 3) (<3,0,G>, 3) (<3,0,H>, ?) (<3,0,I>, 3) (<3,0,J>, 3) (<3,0,K>, ?)
(<5,0,A>, 3) (<5,0,C>, 3) (<5,0,D>, ?) (<5,0,E>, 3) (<5,0,F>, 3) (<5,0,G>, 3) (<5,0,H>, ?) (<5,0,I>, 3) (<5,0,J>, 0) (<5,0,K>, 1)
(<6,0,A>, 3) (<6,0,C>, 3) (<6,0,D>, ?) (<6,0,E>, 3) (<6,0,F>, 3) (<6,0,G>, 0) (<6,0,H>, 1) (<6,0,I>, I) (<6,0,J>, J) (<6,0,K>, K)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f0) = 3
p(f12) = x1
p(f24) = x1
p(f36) = x8 + -1*x9
The following rules are strictly oriented:
[I >= 1 + J] ==>
f36(A,C,D,E,F,G,H,I,J,K) = I + -1*J
> -1 + I + -1*J
= f36(A,C,D,E,F,G,H,I,1 + J,T)
The following rules are weakly oriented:
True ==>
f0(A,C,D,E,F,G,H,I,J,K) = 3
>= 3
= f12(3,3,1,0,F,G,H,I,J,K)
[C >= 1 + E] ==>
f12(A,C,D,E,F,G,H,I,J,K) = A
>= A
= f12(A,C,T,1 + E,F,G,H,I,J,K)
[F >= 1 + G] ==>
f24(A,C,D,E,F,G,H,I,J,K) = A
>= A
= f24(A,C,D,E,F,1 + G,T,I,J,K)
[G >= F] ==>
f24(A,C,D,E,F,G,H,I,J,K) = A
>= A
= f36(A,C,D,E,F,G,H,A,0,1)
[E >= C] ==>
f12(A,C,D,E,F,G,H,I,J,K) = A
>= A
= f24(A,C,D,E,A,0,1,I,J,K)
* Step 9: PolyRank WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,C,D,E,F,G,H,I,J,K) -> f12(3,3,1,0,F,G,H,I,J,K) True (1,1)
1. f12(A,C,D,E,F,G,H,I,J,K) -> f12(A,C,T,1 + E,F,G,H,I,J,K) [C >= 1 + E] (?,1)
2. f24(A,C,D,E,F,G,H,I,J,K) -> f24(A,C,D,E,F,1 + G,T,I,J,K) [F >= 1 + G] (?,1)
3. f36(A,C,D,E,F,G,H,I,J,K) -> f36(A,C,D,E,F,G,H,I,1 + J,T) [I >= 1 + J] (3,1)
5. f24(A,C,D,E,F,G,H,I,J,K) -> f36(A,C,D,E,F,G,H,A,0,1) [G >= F] (1,1)
6. f12(A,C,D,E,F,G,H,I,J,K) -> f24(A,C,D,E,A,0,1,I,J,K) [E >= C] (1,1)
Signature:
{(f0,10);(f12,10);(f24,10);(f36,10);(f46,10)}
Flow Graph:
[0->{1},1->{1,6},2->{2,5},3->{3},5->{3},6->{2,5}]
Sizebounds:
(<0,0,A>, 3) (<0,0,C>, 3) (<0,0,D>, 1) (<0,0,E>, 0) (<0,0,F>, F) (<0,0,G>, G) (<0,0,H>, H) (<0,0,I>, I) (<0,0,J>, J) (<0,0,K>, K)
(<1,0,A>, 3) (<1,0,C>, 3) (<1,0,D>, ?) (<1,0,E>, 3) (<1,0,F>, F) (<1,0,G>, G) (<1,0,H>, H) (<1,0,I>, I) (<1,0,J>, J) (<1,0,K>, K)
(<2,0,A>, 3) (<2,0,C>, 3) (<2,0,D>, ?) (<2,0,E>, 3) (<2,0,F>, 3) (<2,0,G>, 3) (<2,0,H>, ?) (<2,0,I>, I) (<2,0,J>, J) (<2,0,K>, K)
(<3,0,A>, 3) (<3,0,C>, 3) (<3,0,D>, ?) (<3,0,E>, 3) (<3,0,F>, 3) (<3,0,G>, 3) (<3,0,H>, ?) (<3,0,I>, 3) (<3,0,J>, 3) (<3,0,K>, ?)
(<5,0,A>, 3) (<5,0,C>, 3) (<5,0,D>, ?) (<5,0,E>, 3) (<5,0,F>, 3) (<5,0,G>, 3) (<5,0,H>, ?) (<5,0,I>, 3) (<5,0,J>, 0) (<5,0,K>, 1)
(<6,0,A>, 3) (<6,0,C>, 3) (<6,0,D>, ?) (<6,0,E>, 3) (<6,0,F>, 3) (<6,0,G>, 0) (<6,0,H>, 1) (<6,0,I>, I) (<6,0,J>, J) (<6,0,K>, K)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f0) = 3
p(f12) = x1
p(f24) = x5 + -1*x6
p(f36) = x5 + -1*x6
The following rules are strictly oriented:
[F >= 1 + G] ==>
f24(A,C,D,E,F,G,H,I,J,K) = F + -1*G
> -1 + F + -1*G
= f24(A,C,D,E,F,1 + G,T,I,J,K)
The following rules are weakly oriented:
True ==>
f0(A,C,D,E,F,G,H,I,J,K) = 3
>= 3
= f12(3,3,1,0,F,G,H,I,J,K)
[C >= 1 + E] ==>
f12(A,C,D,E,F,G,H,I,J,K) = A
>= A
= f12(A,C,T,1 + E,F,G,H,I,J,K)
[I >= 1 + J] ==>
f36(A,C,D,E,F,G,H,I,J,K) = F + -1*G
>= F + -1*G
= f36(A,C,D,E,F,G,H,I,1 + J,T)
[G >= F] ==>
f24(A,C,D,E,F,G,H,I,J,K) = F + -1*G
>= F + -1*G
= f36(A,C,D,E,F,G,H,A,0,1)
[E >= C] ==>
f12(A,C,D,E,F,G,H,I,J,K) = A
>= A
= f24(A,C,D,E,A,0,1,I,J,K)
* Step 10: PolyRank WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,C,D,E,F,G,H,I,J,K) -> f12(3,3,1,0,F,G,H,I,J,K) True (1,1)
1. f12(A,C,D,E,F,G,H,I,J,K) -> f12(A,C,T,1 + E,F,G,H,I,J,K) [C >= 1 + E] (?,1)
2. f24(A,C,D,E,F,G,H,I,J,K) -> f24(A,C,D,E,F,1 + G,T,I,J,K) [F >= 1 + G] (3,1)
3. f36(A,C,D,E,F,G,H,I,J,K) -> f36(A,C,D,E,F,G,H,I,1 + J,T) [I >= 1 + J] (3,1)
5. f24(A,C,D,E,F,G,H,I,J,K) -> f36(A,C,D,E,F,G,H,A,0,1) [G >= F] (1,1)
6. f12(A,C,D,E,F,G,H,I,J,K) -> f24(A,C,D,E,A,0,1,I,J,K) [E >= C] (1,1)
Signature:
{(f0,10);(f12,10);(f24,10);(f36,10);(f46,10)}
Flow Graph:
[0->{1},1->{1,6},2->{2,5},3->{3},5->{3},6->{2,5}]
Sizebounds:
(<0,0,A>, 3) (<0,0,C>, 3) (<0,0,D>, 1) (<0,0,E>, 0) (<0,0,F>, F) (<0,0,G>, G) (<0,0,H>, H) (<0,0,I>, I) (<0,0,J>, J) (<0,0,K>, K)
(<1,0,A>, 3) (<1,0,C>, 3) (<1,0,D>, ?) (<1,0,E>, 3) (<1,0,F>, F) (<1,0,G>, G) (<1,0,H>, H) (<1,0,I>, I) (<1,0,J>, J) (<1,0,K>, K)
(<2,0,A>, 3) (<2,0,C>, 3) (<2,0,D>, ?) (<2,0,E>, 3) (<2,0,F>, 3) (<2,0,G>, 3) (<2,0,H>, ?) (<2,0,I>, I) (<2,0,J>, J) (<2,0,K>, K)
(<3,0,A>, 3) (<3,0,C>, 3) (<3,0,D>, ?) (<3,0,E>, 3) (<3,0,F>, 3) (<3,0,G>, 3) (<3,0,H>, ?) (<3,0,I>, 3) (<3,0,J>, 3) (<3,0,K>, ?)
(<5,0,A>, 3) (<5,0,C>, 3) (<5,0,D>, ?) (<5,0,E>, 3) (<5,0,F>, 3) (<5,0,G>, 3) (<5,0,H>, ?) (<5,0,I>, 3) (<5,0,J>, 0) (<5,0,K>, 1)
(<6,0,A>, 3) (<6,0,C>, 3) (<6,0,D>, ?) (<6,0,E>, 3) (<6,0,F>, 3) (<6,0,G>, 0) (<6,0,H>, 1) (<6,0,I>, I) (<6,0,J>, J) (<6,0,K>, K)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f0) = 3
p(f12) = x2 + -1*x4
p(f24) = x2 + -1*x4
p(f36) = x2 + -1*x4
The following rules are strictly oriented:
[C >= 1 + E] ==>
f12(A,C,D,E,F,G,H,I,J,K) = C + -1*E
> -1 + C + -1*E
= f12(A,C,T,1 + E,F,G,H,I,J,K)
The following rules are weakly oriented:
True ==>
f0(A,C,D,E,F,G,H,I,J,K) = 3
>= 3
= f12(3,3,1,0,F,G,H,I,J,K)
[F >= 1 + G] ==>
f24(A,C,D,E,F,G,H,I,J,K) = C + -1*E
>= C + -1*E
= f24(A,C,D,E,F,1 + G,T,I,J,K)
[I >= 1 + J] ==>
f36(A,C,D,E,F,G,H,I,J,K) = C + -1*E
>= C + -1*E
= f36(A,C,D,E,F,G,H,I,1 + J,T)
[G >= F] ==>
f24(A,C,D,E,F,G,H,I,J,K) = C + -1*E
>= C + -1*E
= f36(A,C,D,E,F,G,H,A,0,1)
[E >= C] ==>
f12(A,C,D,E,F,G,H,I,J,K) = C + -1*E
>= C + -1*E
= f24(A,C,D,E,A,0,1,I,J,K)
* Step 11: KnowledgePropagation WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,C,D,E,F,G,H,I,J,K) -> f12(3,3,1,0,F,G,H,I,J,K) True (1,1)
1. f12(A,C,D,E,F,G,H,I,J,K) -> f12(A,C,T,1 + E,F,G,H,I,J,K) [C >= 1 + E] (3,1)
2. f24(A,C,D,E,F,G,H,I,J,K) -> f24(A,C,D,E,F,1 + G,T,I,J,K) [F >= 1 + G] (3,1)
3. f36(A,C,D,E,F,G,H,I,J,K) -> f36(A,C,D,E,F,G,H,I,1 + J,T) [I >= 1 + J] (3,1)
5. f24(A,C,D,E,F,G,H,I,J,K) -> f36(A,C,D,E,F,G,H,A,0,1) [G >= F] (1,1)
6. f12(A,C,D,E,F,G,H,I,J,K) -> f24(A,C,D,E,A,0,1,I,J,K) [E >= C] (1,1)
Signature:
{(f0,10);(f12,10);(f24,10);(f36,10);(f46,10)}
Flow Graph:
[0->{1},1->{1,6},2->{2,5},3->{3},5->{3},6->{2,5}]
Sizebounds:
(<0,0,A>, 3) (<0,0,C>, 3) (<0,0,D>, 1) (<0,0,E>, 0) (<0,0,F>, F) (<0,0,G>, G) (<0,0,H>, H) (<0,0,I>, I) (<0,0,J>, J) (<0,0,K>, K)
(<1,0,A>, 3) (<1,0,C>, 3) (<1,0,D>, ?) (<1,0,E>, 3) (<1,0,F>, F) (<1,0,G>, G) (<1,0,H>, H) (<1,0,I>, I) (<1,0,J>, J) (<1,0,K>, K)
(<2,0,A>, 3) (<2,0,C>, 3) (<2,0,D>, ?) (<2,0,E>, 3) (<2,0,F>, 3) (<2,0,G>, 3) (<2,0,H>, ?) (<2,0,I>, I) (<2,0,J>, J) (<2,0,K>, K)
(<3,0,A>, 3) (<3,0,C>, 3) (<3,0,D>, ?) (<3,0,E>, 3) (<3,0,F>, 3) (<3,0,G>, 3) (<3,0,H>, ?) (<3,0,I>, 3) (<3,0,J>, 3) (<3,0,K>, ?)
(<5,0,A>, 3) (<5,0,C>, 3) (<5,0,D>, ?) (<5,0,E>, 3) (<5,0,F>, 3) (<5,0,G>, 3) (<5,0,H>, ?) (<5,0,I>, 3) (<5,0,J>, 0) (<5,0,K>, 1)
(<6,0,A>, 3) (<6,0,C>, 3) (<6,0,D>, ?) (<6,0,E>, 3) (<6,0,F>, 3) (<6,0,G>, 0) (<6,0,H>, 1) (<6,0,I>, I) (<6,0,J>, J) (<6,0,K>, K)
+ Applied Processor:
KnowledgePropagation
+ Details:
The problem is already solved.
WORST_CASE(?,O(1))