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