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