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