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) -> stop(A,B,C,D,E,F,G,H) [0 >= 1 + A && B = C && D = A && E = F && G = H] (?,1) 1. start(A,B,C,D,E,F,G,H) -> lbl42(A,-1 + B,C,D,E,F,G,H) [A >= 0 && C >= 0 && B = C && D = A && E = F && G = H] (?,1) 2. start(A,B,C,D,E,F,G,H) -> cut(A,B,C,-1 + D,E,F,G,H) [A >= 0 && B = C && D = A && E = F && G = H] (?,1) 3. start(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,-1 + D,B,F,G,H) [H >= C && A >= 0 && B = C && D = A && E = F && G = H] (?,1) 4. lbl72(A,B,C,D,E,F,G,H) -> cut(A,B,C,D,E,F,G,H) [A >= 1 + D && 1 + D >= 0 && 1 + H >= B && 1 + E = B && G = H] (?,1) 5. lbl72(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,D,B,F,G,H) [H >= B && A >= 1 + D && 1 + D >= 0 && 1 + H >= B && 1 + E = B && G = H] (?,1) 6. lbl42(A,B,C,D,E,F,G,H) -> lbl42(A,-1 + B,C,D,E,F,G,H) [B >= 0 && 1 + B >= 0 && D >= 0 && A >= D && G = H] (?,1) 7. lbl42(A,B,C,D,E,F,G,H) -> cut(A,B,C,-1 + D,E,F,G,H) [1 + B >= 0 && D >= 0 && A >= D && G = H] (?,1) 8. lbl42(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,-1 + D,B,F,G,H) [H >= B && 1 + B >= 0 && D >= 0 && A >= D && G = H] (?,1) 9. cut(A,B,C,D,E,F,G,H) -> stop(A,B,C,D,E,F,G,H) [A >= 0 && 1 + D = 0 && G = H] (?,1) 10. cut(A,B,C,D,E,F,G,H) -> lbl42(A,-1 + B,C,D,E,F,G,H) [D >= 0 && B >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] (?,1) 11. cut(A,B,C,D,E,F,G,H) -> cut(A,B,C,-1 + D,E,F,G,H) [D >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] (?,1) 12. cut(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,-1 + D,B,F,G,H) [H >= B && D >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] (?,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);(lbl42,8);(lbl72,8);(start,8);(start0,8);(stop,8)} Flow Graph: [0->{},1->{6,7,8},2->{9,10,11,12},3->{4,5},4->{9,10,11,12},5->{4,5},6->{6,7,8},7->{9,10,11,12},8->{4,5} ,9->{},10->{6,7,8},11->{9,10,11,12},12->{4,5},13->{0,1,2,3}] + 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>, 1 + B, .+ 1) (< 1,0,C>, C, .= 0) (< 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>, 1 + D, .+ 1) (< 2,0,E>, E, .= 0) (< 2,0,F>, F, .= 0) (< 2,0,G>, G, .= 0) (< 2,0,H>, H, .= 0) (< 3,0,A>, A, .= 0) (< 3,0,B>, 1 + B, .+ 1) (< 3,0,C>, C, .= 0) (< 3,0,D>, 1 + D, .+ 1) (< 3,0,E>, B, .= 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>, C, .= 0) (< 4,0,D>, D, .= 0) (< 4,0,E>, E, .= 0) (< 4,0,F>, F, .= 0) (< 4,0,G>, G, .= 0) (< 4,0,H>, H, .= 0) (< 5,0,A>, A, .= 0) (< 5,0,B>, 1 + B, .+ 1) (< 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>, 2 + B, .+ 2) (< 6,0,C>, C, .= 0) (< 6,0,D>, D, .= 0) (< 6,0,E>, E, .= 0) (< 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>, 1 + D, .+ 1) (< 7,0,E>, E, .= 0) (< 7,0,F>, F, .= 0) (< 7,0,G>, G, .= 0) (< 7,0,H>, H, .= 0) (< 8,0,A>, A, .= 0) (< 8,0,B>, 1 + B, .+ 1) (< 8,0,C>, C, .= 0) (< 8,0,D>, 1 + D, .+ 1) (< 8,0,E>, B, .= 0) (< 8,0,F>, F, .= 0) (< 8,0,G>, G, .= 0) (< 8,0,H>, H, .= 0) (< 9,0,A>, A, .= 0) (< 9,0,B>, B, .= 0) (< 9,0,C>, C, .= 0) (< 9,0,D>, D, .= 0) (< 9,0,E>, E, .= 0) (< 9,0,F>, F, .= 0) (< 9,0,G>, G, .= 0) (< 9,0,H>, H, .= 0) (<10,0,A>, A, .= 0) (<10,0,B>, 1 + B, .+ 1) (<10,0,C>, C, .= 0) (<10,0,D>, D, .= 0) (<10,0,E>, E, .= 0) (<10,0,F>, F, .= 0) (<10,0,G>, G, .= 0) (<10,0,H>, H, .= 0) (<11,0,A>, A, .= 0) (<11,0,B>, B, .= 0) (<11,0,C>, C, .= 0) (<11,0,D>, 1 + D, .+ 1) (<11,0,E>, E, .= 0) (<11,0,F>, F, .= 0) (<11,0,G>, G, .= 0) (<11,0,H>, H, .= 0) (<12,0,A>, A, .= 0) (<12,0,B>, 1 + B, .+ 1) (<12,0,C>, C, .= 0) (<12,0,D>, 1 + D, .+ 1) (<12,0,E>, B, .= 0) (<12,0,F>, F, .= 0) (<12,0,G>, G, .= 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 2: SizeboundsProc WORST_CASE(?,O(n^3)) + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H) -> stop(A,B,C,D,E,F,G,H) [0 >= 1 + A && B = C && D = A && E = F && G = H] (?,1) 1. start(A,B,C,D,E,F,G,H) -> lbl42(A,-1 + B,C,D,E,F,G,H) [A >= 0 && C >= 0 && B = C && D = A && E = F && G = H] (?,1) 2. start(A,B,C,D,E,F,G,H) -> cut(A,B,C,-1 + D,E,F,G,H) [A >= 0 && B = C && D = A && E = F && G = H] (?,1) 3. start(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,-1 + D,B,F,G,H) [H >= C && A >= 0 && B = C && D = A && E = F && G = H] (?,1) 4. lbl72(A,B,C,D,E,F,G,H) -> cut(A,B,C,D,E,F,G,H) [A >= 1 + D && 1 + D >= 0 && 1 + H >= B && 1 + E = B && G = H] (?,1) 5. lbl72(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,D,B,F,G,H) [H >= B && A >= 1 + D && 1 + D >= 0 && 1 + H >= B && 1 + E = B && G = H] (?,1) 6. lbl42(A,B,C,D,E,F,G,H) -> lbl42(A,-1 + B,C,D,E,F,G,H) [B >= 0 && 1 + B >= 0 && D >= 0 && A >= D && G = H] (?,1) 7. lbl42(A,B,C,D,E,F,G,H) -> cut(A,B,C,-1 + D,E,F,G,H) [1 + B >= 0 && D >= 0 && A >= D && G = H] (?,1) 8. lbl42(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,-1 + D,B,F,G,H) [H >= B && 1 + B >= 0 && D >= 0 && A >= D && G = H] (?,1) 9. cut(A,B,C,D,E,F,G,H) -> stop(A,B,C,D,E,F,G,H) [A >= 0 && 1 + D = 0 && G = H] (?,1) 10. cut(A,B,C,D,E,F,G,H) -> lbl42(A,-1 + B,C,D,E,F,G,H) [D >= 0 && B >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] (?,1) 11. cut(A,B,C,D,E,F,G,H) -> cut(A,B,C,-1 + D,E,F,G,H) [D >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] (?,1) 12. cut(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,-1 + D,B,F,G,H) [H >= B && D >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] (?,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);(lbl42,8);(lbl72,8);(start,8);(start0,8);(stop,8)} Flow Graph: [0->{},1->{6,7,8},2->{9,10,11,12},3->{4,5},4->{9,10,11,12},5->{4,5},6->{6,7,8},7->{9,10,11,12},8->{4,5} ,9->{},10->{6,7,8},11->{9,10,11,12},12->{4,5},13->{0,1,2,3}] 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>, ?) (<11,0,A>, ?) (<11,0,B>, ?) (<11,0,C>, ?) (<11,0,D>, ?) (<11,0,E>, ?) (<11,0,F>, ?) (<11,0,G>, ?) (<11,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>, F) (< 0,0,F>, F) (< 0,0,G>, H) (< 0,0,H>, H) (< 1,0,A>, A) (< 1,0,B>, 1 + C) (< 1,0,C>, C) (< 1,0,D>, A) (< 1,0,E>, F) (< 1,0,F>, F) (< 1,0,G>, H) (< 1,0,H>, H) (< 2,0,A>, A) (< 2,0,B>, C) (< 2,0,C>, C) (< 2,0,D>, 1 + A) (< 2,0,E>, F) (< 2,0,F>, F) (< 2,0,G>, H) (< 2,0,H>, H) (< 3,0,A>, A) (< 3,0,B>, 1 + C) (< 3,0,C>, C) (< 3,0,D>, 1 + A) (< 3,0,E>, C) (< 3,0,F>, F) (< 3,0,G>, H) (< 3,0,H>, H) (< 4,0,A>, A) (< 4,0,B>, 1 + H) (< 4,0,C>, C) (< 4,0,D>, A) (< 4,0,E>, ?) (< 4,0,F>, F) (< 4,0,G>, H) (< 4,0,H>, H) (< 5,0,A>, A) (< 5,0,B>, 1 + H) (< 5,0,C>, C) (< 5,0,D>, A) (< 5,0,E>, 1 + C + H) (< 5,0,F>, F) (< 5,0,G>, H) (< 5,0,H>, H) (< 6,0,A>, A) (< 6,0,B>, ?) (< 6,0,C>, C) (< 6,0,D>, A) (< 6,0,E>, ?) (< 6,0,F>, F) (< 6,0,G>, H) (< 6,0,H>, H) (< 7,0,A>, A) (< 7,0,B>, ?) (< 7,0,C>, C) (< 7,0,D>, A) (< 7,0,E>, ?) (< 7,0,F>, F) (< 7,0,G>, H) (< 7,0,H>, H) (< 8,0,A>, A) (< 8,0,B>, 1 + H) (< 8,0,C>, C) (< 8,0,D>, A) (< 8,0,E>, ?) (< 8,0,F>, F) (< 8,0,G>, H) (< 8,0,H>, H) (< 9,0,A>, A) (< 9,0,B>, ?) (< 9,0,C>, C) (< 9,0,D>, 1 + A) (< 9,0,E>, ?) (< 9,0,F>, F) (< 9,0,G>, H) (< 9,0,H>, H) (<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, C) (<10,0,D>, A) (<10,0,E>, ?) (<10,0,F>, F) (<10,0,G>, H) (<10,0,H>, H) (<11,0,A>, A) (<11,0,B>, ?) (<11,0,C>, C) (<11,0,D>, A) (<11,0,E>, ?) (<11,0,F>, F) (<11,0,G>, H) (<11,0,H>, H) (<12,0,A>, A) (<12,0,B>, 1 + H) (<12,0,C>, C) (<12,0,D>, A) (<12,0,E>, ?) (<12,0,F>, F) (<12,0,G>, H) (<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 3: LeafRules WORST_CASE(?,O(n^3)) + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H) -> stop(A,B,C,D,E,F,G,H) [0 >= 1 + A && B = C && D = A && E = F && G = H] (?,1) 1. start(A,B,C,D,E,F,G,H) -> lbl42(A,-1 + B,C,D,E,F,G,H) [A >= 0 && C >= 0 && B = C && D = A && E = F && G = H] (?,1) 2. start(A,B,C,D,E,F,G,H) -> cut(A,B,C,-1 + D,E,F,G,H) [A >= 0 && B = C && D = A && E = F && G = H] (?,1) 3. start(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,-1 + D,B,F,G,H) [H >= C && A >= 0 && B = C && D = A && E = F && G = H] (?,1) 4. lbl72(A,B,C,D,E,F,G,H) -> cut(A,B,C,D,E,F,G,H) [A >= 1 + D && 1 + D >= 0 && 1 + H >= B && 1 + E = B && G = H] (?,1) 5. lbl72(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,D,B,F,G,H) [H >= B && A >= 1 + D && 1 + D >= 0 && 1 + H >= B && 1 + E = B && G = H] (?,1) 6. lbl42(A,B,C,D,E,F,G,H) -> lbl42(A,-1 + B,C,D,E,F,G,H) [B >= 0 && 1 + B >= 0 && D >= 0 && A >= D && G = H] (?,1) 7. lbl42(A,B,C,D,E,F,G,H) -> cut(A,B,C,-1 + D,E,F,G,H) [1 + B >= 0 && D >= 0 && A >= D && G = H] (?,1) 8. lbl42(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,-1 + D,B,F,G,H) [H >= B && 1 + B >= 0 && D >= 0 && A >= D && G = H] (?,1) 9. cut(A,B,C,D,E,F,G,H) -> stop(A,B,C,D,E,F,G,H) [A >= 0 && 1 + D = 0 && G = H] (?,1) 10. cut(A,B,C,D,E,F,G,H) -> lbl42(A,-1 + B,C,D,E,F,G,H) [D >= 0 && B >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] (?,1) 11. cut(A,B,C,D,E,F,G,H) -> cut(A,B,C,-1 + D,E,F,G,H) [D >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] (?,1) 12. cut(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,-1 + D,B,F,G,H) [H >= B && D >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] (?,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);(lbl42,8);(lbl72,8);(start,8);(start0,8);(stop,8)} Flow Graph: [0->{},1->{6,7,8},2->{9,10,11,12},3->{4,5},4->{9,10,11,12},5->{4,5},6->{6,7,8},7->{9,10,11,12},8->{4,5} ,9->{},10->{6,7,8},11->{9,10,11,12},12->{4,5},13->{0,1,2,3}] Sizebounds: (< 0,0,A>, A) (< 0,0,B>, C) (< 0,0,C>, C) (< 0,0,D>, A) (< 0,0,E>, F) (< 0,0,F>, F) (< 0,0,G>, H) (< 0,0,H>, H) (< 1,0,A>, A) (< 1,0,B>, 1 + C) (< 1,0,C>, C) (< 1,0,D>, A) (< 1,0,E>, F) (< 1,0,F>, F) (< 1,0,G>, H) (< 1,0,H>, H) (< 2,0,A>, A) (< 2,0,B>, C) (< 2,0,C>, C) (< 2,0,D>, 1 + A) (< 2,0,E>, F) (< 2,0,F>, F) (< 2,0,G>, H) (< 2,0,H>, H) (< 3,0,A>, A) (< 3,0,B>, 1 + C) (< 3,0,C>, C) (< 3,0,D>, 1 + A) (< 3,0,E>, C) (< 3,0,F>, F) (< 3,0,G>, H) (< 3,0,H>, H) (< 4,0,A>, A) (< 4,0,B>, 1 + H) (< 4,0,C>, C) (< 4,0,D>, A) (< 4,0,E>, ?) (< 4,0,F>, F) (< 4,0,G>, H) (< 4,0,H>, H) (< 5,0,A>, A) (< 5,0,B>, 1 + H) (< 5,0,C>, C) (< 5,0,D>, A) (< 5,0,E>, 1 + C + H) (< 5,0,F>, F) (< 5,0,G>, H) (< 5,0,H>, H) (< 6,0,A>, A) (< 6,0,B>, ?) (< 6,0,C>, C) (< 6,0,D>, A) (< 6,0,E>, ?) (< 6,0,F>, F) (< 6,0,G>, H) (< 6,0,H>, H) (< 7,0,A>, A) (< 7,0,B>, ?) (< 7,0,C>, C) (< 7,0,D>, A) (< 7,0,E>, ?) (< 7,0,F>, F) (< 7,0,G>, H) (< 7,0,H>, H) (< 8,0,A>, A) (< 8,0,B>, 1 + H) (< 8,0,C>, C) (< 8,0,D>, A) (< 8,0,E>, ?) (< 8,0,F>, F) (< 8,0,G>, H) (< 8,0,H>, H) (< 9,0,A>, A) (< 9,0,B>, ?) (< 9,0,C>, C) (< 9,0,D>, 1 + A) (< 9,0,E>, ?) (< 9,0,F>, F) (< 9,0,G>, H) (< 9,0,H>, H) (<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, C) (<10,0,D>, A) (<10,0,E>, ?) (<10,0,F>, F) (<10,0,G>, H) (<10,0,H>, H) (<11,0,A>, A) (<11,0,B>, ?) (<11,0,C>, C) (<11,0,D>, A) (<11,0,E>, ?) (<11,0,F>, F) (<11,0,G>, H) (<11,0,H>, H) (<12,0,A>, A) (<12,0,B>, 1 + H) (<12,0,C>, C) (<12,0,D>, A) (<12,0,E>, ?) (<12,0,F>, F) (<12,0,G>, H) (<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,9] * Step 4: PolyRank WORST_CASE(?,O(n^3)) + Considered Problem: Rules: 1. start(A,B,C,D,E,F,G,H) -> lbl42(A,-1 + B,C,D,E,F,G,H) [A >= 0 && C >= 0 && B = C && D = A && E = F && G = H] (?,1) 2. start(A,B,C,D,E,F,G,H) -> cut(A,B,C,-1 + D,E,F,G,H) [A >= 0 && B = C && D = A && E = F && G = H] (?,1) 3. start(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,-1 + D,B,F,G,H) [H >= C && A >= 0 && B = C && D = A && E = F && G = H] (?,1) 4. lbl72(A,B,C,D,E,F,G,H) -> cut(A,B,C,D,E,F,G,H) [A >= 1 + D && 1 + D >= 0 && 1 + H >= B && 1 + E = B && G = H] (?,1) 5. lbl72(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,D,B,F,G,H) [H >= B && A >= 1 + D && 1 + D >= 0 && 1 + H >= B && 1 + E = B && G = H] (?,1) 6. lbl42(A,B,C,D,E,F,G,H) -> lbl42(A,-1 + B,C,D,E,F,G,H) [B >= 0 && 1 + B >= 0 && D >= 0 && A >= D && G = H] (?,1) 7. lbl42(A,B,C,D,E,F,G,H) -> cut(A,B,C,-1 + D,E,F,G,H) [1 + B >= 0 && D >= 0 && A >= D && G = H] (?,1) 8. lbl42(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,-1 + D,B,F,G,H) [H >= B && 1 + B >= 0 && D >= 0 && A >= D && G = H] (?,1) 10. cut(A,B,C,D,E,F,G,H) -> lbl42(A,-1 + B,C,D,E,F,G,H) [D >= 0 && B >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] (?,1) 11. cut(A,B,C,D,E,F,G,H) -> cut(A,B,C,-1 + D,E,F,G,H) [D >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] (?,1) 12. cut(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,-1 + D,B,F,G,H) [H >= B && D >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] (?,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);(lbl42,8);(lbl72,8);(start,8);(start0,8);(stop,8)} Flow Graph: [1->{6,7,8},2->{10,11,12},3->{4,5},4->{10,11,12},5->{4,5},6->{6,7,8},7->{10,11,12},8->{4,5},10->{6,7,8} ,11->{10,11,12},12->{4,5},13->{1,2,3}] Sizebounds: (< 1,0,A>, A) (< 1,0,B>, 1 + C) (< 1,0,C>, C) (< 1,0,D>, A) (< 1,0,E>, F) (< 1,0,F>, F) (< 1,0,G>, H) (< 1,0,H>, H) (< 2,0,A>, A) (< 2,0,B>, C) (< 2,0,C>, C) (< 2,0,D>, 1 + A) (< 2,0,E>, F) (< 2,0,F>, F) (< 2,0,G>, H) (< 2,0,H>, H) (< 3,0,A>, A) (< 3,0,B>, 1 + C) (< 3,0,C>, C) (< 3,0,D>, 1 + A) (< 3,0,E>, C) (< 3,0,F>, F) (< 3,0,G>, H) (< 3,0,H>, H) (< 4,0,A>, A) (< 4,0,B>, 1 + H) (< 4,0,C>, C) (< 4,0,D>, A) (< 4,0,E>, ?) (< 4,0,F>, F) (< 4,0,G>, H) (< 4,0,H>, H) (< 5,0,A>, A) (< 5,0,B>, 1 + H) (< 5,0,C>, C) (< 5,0,D>, A) (< 5,0,E>, 1 + C + H) (< 5,0,F>, F) (< 5,0,G>, H) (< 5,0,H>, H) (< 6,0,A>, A) (< 6,0,B>, ?) (< 6,0,C>, C) (< 6,0,D>, A) (< 6,0,E>, ?) (< 6,0,F>, F) (< 6,0,G>, H) (< 6,0,H>, H) (< 7,0,A>, A) (< 7,0,B>, ?) (< 7,0,C>, C) (< 7,0,D>, A) (< 7,0,E>, ?) (< 7,0,F>, F) (< 7,0,G>, H) (< 7,0,H>, H) (< 8,0,A>, A) (< 8,0,B>, 1 + H) (< 8,0,C>, C) (< 8,0,D>, A) (< 8,0,E>, ?) (< 8,0,F>, F) (< 8,0,G>, H) (< 8,0,H>, H) (<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, C) (<10,0,D>, A) (<10,0,E>, ?) (<10,0,F>, F) (<10,0,G>, H) (<10,0,H>, H) (<11,0,A>, A) (<11,0,B>, ?) (<11,0,C>, C) (<11,0,D>, A) (<11,0,E>, ?) (<11,0,F>, F) (<11,0,G>, H) (<11,0,H>, H) (<12,0,A>, A) (<12,0,B>, 1 + H) (<12,0,C>, C) (<12,0,D>, A) (<12,0,E>, ?) (<12,0,F>, F) (<12,0,G>, H) (<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: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(cut) = x1 + x4 p(lbl42) = x1 + x4 p(lbl72) = x1 + x4 p(start) = 2*x1 p(start0) = 2*x1 The following rules are strictly oriented: [H >= B && D >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] ==> cut(A,B,C,D,E,F,G,H) = A + D > -1 + A + D = lbl72(A,1 + B,C,-1 + D,B,F,G,H) The following rules are weakly oriented: [A >= 0 && C >= 0 && B = C && D = A && E = F && G = H] ==> start(A,B,C,D,E,F,G,H) = 2*A >= A + D = lbl42(A,-1 + B,C,D,E,F,G,H) [A >= 0 && B = C && D = A && E = F && G = H] ==> start(A,B,C,D,E,F,G,H) = 2*A >= -1 + A + D = cut(A,B,C,-1 + D,E,F,G,H) [H >= C && A >= 0 && B = C && D = A && E = F && G = H] ==> start(A,B,C,D,E,F,G,H) = 2*A >= -1 + A + D = lbl72(A,1 + B,C,-1 + D,B,F,G,H) [A >= 1 + D && 1 + D >= 0 && 1 + H >= B && 1 + E = B && G = H] ==> lbl72(A,B,C,D,E,F,G,H) = A + D >= A + D = cut(A,B,C,D,E,F,G,H) [H >= B && A >= 1 + D && 1 + D >= 0 && 1 + H >= B && 1 + E = B && G = H] ==> lbl72(A,B,C,D,E,F,G,H) = A + D >= A + D = lbl72(A,1 + B,C,D,B,F,G,H) [B >= 0 && 1 + B >= 0 && D >= 0 && A >= D && G = H] ==> lbl42(A,B,C,D,E,F,G,H) = A + D >= A + D = lbl42(A,-1 + B,C,D,E,F,G,H) [1 + B >= 0 && D >= 0 && A >= D && G = H] ==> lbl42(A,B,C,D,E,F,G,H) = A + D >= -1 + A + D = cut(A,B,C,-1 + D,E,F,G,H) [H >= B && 1 + B >= 0 && D >= 0 && A >= D && G = H] ==> lbl42(A,B,C,D,E,F,G,H) = A + D >= -1 + A + D = lbl72(A,1 + B,C,-1 + D,B,F,G,H) [D >= 0 && B >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] ==> cut(A,B,C,D,E,F,G,H) = A + D >= A + D = lbl42(A,-1 + B,C,D,E,F,G,H) [D >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] ==> cut(A,B,C,D,E,F,G,H) = A + D >= -1 + A + D = cut(A,B,C,-1 + D,E,F,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 5: KnowledgePropagation WORST_CASE(?,O(n^3)) + Considered Problem: Rules: 1. start(A,B,C,D,E,F,G,H) -> lbl42(A,-1 + B,C,D,E,F,G,H) [A >= 0 && C >= 0 && B = C && D = A && E = F && G = H] (?,1) 2. start(A,B,C,D,E,F,G,H) -> cut(A,B,C,-1 + D,E,F,G,H) [A >= 0 && B = C && D = A && E = F && G = H] (?,1) 3. start(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,-1 + D,B,F,G,H) [H >= C && A >= 0 && B = C && D = A && E = F && G = H] (?,1) 4. lbl72(A,B,C,D,E,F,G,H) -> cut(A,B,C,D,E,F,G,H) [A >= 1 + D && 1 + D >= 0 && 1 + H >= B && 1 + E = B && G = H] (?,1) 5. lbl72(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,D,B,F,G,H) [H >= B && A >= 1 + D && 1 + D >= 0 && 1 + H >= B && 1 + E = B && G = H] (?,1) 6. lbl42(A,B,C,D,E,F,G,H) -> lbl42(A,-1 + B,C,D,E,F,G,H) [B >= 0 && 1 + B >= 0 && D >= 0 && A >= D && G = H] (?,1) 7. lbl42(A,B,C,D,E,F,G,H) -> cut(A,B,C,-1 + D,E,F,G,H) [1 + B >= 0 && D >= 0 && A >= D && G = H] (?,1) 8. lbl42(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,-1 + D,B,F,G,H) [H >= B && 1 + B >= 0 && D >= 0 && A >= D && G = H] (?,1) 10. cut(A,B,C,D,E,F,G,H) -> lbl42(A,-1 + B,C,D,E,F,G,H) [D >= 0 && B >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] (?,1) 11. cut(A,B,C,D,E,F,G,H) -> cut(A,B,C,-1 + D,E,F,G,H) [D >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] (?,1) 12. cut(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,-1 + D,B,F,G,H) [H >= B && D >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] (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);(lbl42,8);(lbl72,8);(start,8);(start0,8);(stop,8)} Flow Graph: [1->{6,7,8},2->{10,11,12},3->{4,5},4->{10,11,12},5->{4,5},6->{6,7,8},7->{10,11,12},8->{4,5},10->{6,7,8} ,11->{10,11,12},12->{4,5},13->{1,2,3}] Sizebounds: (< 1,0,A>, A) (< 1,0,B>, 1 + C) (< 1,0,C>, C) (< 1,0,D>, A) (< 1,0,E>, F) (< 1,0,F>, F) (< 1,0,G>, H) (< 1,0,H>, H) (< 2,0,A>, A) (< 2,0,B>, C) (< 2,0,C>, C) (< 2,0,D>, 1 + A) (< 2,0,E>, F) (< 2,0,F>, F) (< 2,0,G>, H) (< 2,0,H>, H) (< 3,0,A>, A) (< 3,0,B>, 1 + C) (< 3,0,C>, C) (< 3,0,D>, 1 + A) (< 3,0,E>, C) (< 3,0,F>, F) (< 3,0,G>, H) (< 3,0,H>, H) (< 4,0,A>, A) (< 4,0,B>, 1 + H) (< 4,0,C>, C) (< 4,0,D>, A) (< 4,0,E>, ?) (< 4,0,F>, F) (< 4,0,G>, H) (< 4,0,H>, H) (< 5,0,A>, A) (< 5,0,B>, 1 + H) (< 5,0,C>, C) (< 5,0,D>, A) (< 5,0,E>, 1 + C + H) (< 5,0,F>, F) (< 5,0,G>, H) (< 5,0,H>, H) (< 6,0,A>, A) (< 6,0,B>, ?) (< 6,0,C>, C) (< 6,0,D>, A) (< 6,0,E>, ?) (< 6,0,F>, F) (< 6,0,G>, H) (< 6,0,H>, H) (< 7,0,A>, A) (< 7,0,B>, ?) (< 7,0,C>, C) (< 7,0,D>, A) (< 7,0,E>, ?) (< 7,0,F>, F) (< 7,0,G>, H) (< 7,0,H>, H) (< 8,0,A>, A) (< 8,0,B>, 1 + H) (< 8,0,C>, C) (< 8,0,D>, A) (< 8,0,E>, ?) (< 8,0,F>, F) (< 8,0,G>, H) (< 8,0,H>, H) (<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, C) (<10,0,D>, A) (<10,0,E>, ?) (<10,0,F>, F) (<10,0,G>, H) (<10,0,H>, H) (<11,0,A>, A) (<11,0,B>, ?) (<11,0,C>, C) (<11,0,D>, A) (<11,0,E>, ?) (<11,0,F>, F) (<11,0,G>, H) (<11,0,H>, H) (<12,0,A>, A) (<12,0,B>, 1 + H) (<12,0,C>, C) (<12,0,D>, A) (<12,0,E>, ?) (<12,0,F>, F) (<12,0,G>, H) (<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: KnowledgePropagation + Details: We propagate bounds from predecessors. * Step 6: PolyRank WORST_CASE(?,O(n^3)) + Considered Problem: Rules: 1. start(A,B,C,D,E,F,G,H) -> lbl42(A,-1 + B,C,D,E,F,G,H) [A >= 0 && C >= 0 && B = C && D = A && E = F && G = H] (1,1) 2. start(A,B,C,D,E,F,G,H) -> cut(A,B,C,-1 + D,E,F,G,H) [A >= 0 && B = C && D = A && E = F && G = H] (1,1) 3. start(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,-1 + D,B,F,G,H) [H >= C && A >= 0 && B = C && D = A && E = F && G = H] (1,1) 4. lbl72(A,B,C,D,E,F,G,H) -> cut(A,B,C,D,E,F,G,H) [A >= 1 + D && 1 + D >= 0 && 1 + H >= B && 1 + E = B && G = H] (?,1) 5. lbl72(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,D,B,F,G,H) [H >= B && A >= 1 + D && 1 + D >= 0 && 1 + H >= B && 1 + E = B && G = H] (?,1) 6. lbl42(A,B,C,D,E,F,G,H) -> lbl42(A,-1 + B,C,D,E,F,G,H) [B >= 0 && 1 + B >= 0 && D >= 0 && A >= D && G = H] (?,1) 7. lbl42(A,B,C,D,E,F,G,H) -> cut(A,B,C,-1 + D,E,F,G,H) [1 + B >= 0 && D >= 0 && A >= D && G = H] (?,1) 8. lbl42(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,-1 + D,B,F,G,H) [H >= B && 1 + B >= 0 && D >= 0 && A >= D && G = H] (?,1) 10. cut(A,B,C,D,E,F,G,H) -> lbl42(A,-1 + B,C,D,E,F,G,H) [D >= 0 && B >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] (?,1) 11. cut(A,B,C,D,E,F,G,H) -> cut(A,B,C,-1 + D,E,F,G,H) [D >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] (?,1) 12. cut(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,-1 + D,B,F,G,H) [H >= B && D >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] (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);(lbl42,8);(lbl72,8);(start,8);(start0,8);(stop,8)} Flow Graph: [1->{6,7,8},2->{10,11,12},3->{4,5},4->{10,11,12},5->{4,5},6->{6,7,8},7->{10,11,12},8->{4,5},10->{6,7,8} ,11->{10,11,12},12->{4,5},13->{1,2,3}] Sizebounds: (< 1,0,A>, A) (< 1,0,B>, 1 + C) (< 1,0,C>, C) (< 1,0,D>, A) (< 1,0,E>, F) (< 1,0,F>, F) (< 1,0,G>, H) (< 1,0,H>, H) (< 2,0,A>, A) (< 2,0,B>, C) (< 2,0,C>, C) (< 2,0,D>, 1 + A) (< 2,0,E>, F) (< 2,0,F>, F) (< 2,0,G>, H) (< 2,0,H>, H) (< 3,0,A>, A) (< 3,0,B>, 1 + C) (< 3,0,C>, C) (< 3,0,D>, 1 + A) (< 3,0,E>, C) (< 3,0,F>, F) (< 3,0,G>, H) (< 3,0,H>, H) (< 4,0,A>, A) (< 4,0,B>, 1 + H) (< 4,0,C>, C) (< 4,0,D>, A) (< 4,0,E>, ?) (< 4,0,F>, F) (< 4,0,G>, H) (< 4,0,H>, H) (< 5,0,A>, A) (< 5,0,B>, 1 + H) (< 5,0,C>, C) (< 5,0,D>, A) (< 5,0,E>, 1 + C + H) (< 5,0,F>, F) (< 5,0,G>, H) (< 5,0,H>, H) (< 6,0,A>, A) (< 6,0,B>, ?) (< 6,0,C>, C) (< 6,0,D>, A) (< 6,0,E>, ?) (< 6,0,F>, F) (< 6,0,G>, H) (< 6,0,H>, H) (< 7,0,A>, A) (< 7,0,B>, ?) (< 7,0,C>, C) (< 7,0,D>, A) (< 7,0,E>, ?) (< 7,0,F>, F) (< 7,0,G>, H) (< 7,0,H>, H) (< 8,0,A>, A) (< 8,0,B>, 1 + H) (< 8,0,C>, C) (< 8,0,D>, A) (< 8,0,E>, ?) (< 8,0,F>, F) (< 8,0,G>, H) (< 8,0,H>, H) (<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, C) (<10,0,D>, A) (<10,0,E>, ?) (<10,0,F>, F) (<10,0,G>, H) (<10,0,H>, H) (<11,0,A>, A) (<11,0,B>, ?) (<11,0,C>, C) (<11,0,D>, A) (<11,0,E>, ?) (<11,0,F>, F) (<11,0,G>, H) (<11,0,H>, H) (<12,0,A>, A) (<12,0,B>, 1 + H) (<12,0,C>, C) (<12,0,D>, A) (<12,0,E>, ?) (<12,0,F>, F) (<12,0,G>, H) (<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: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(cut) = 1 + x4 p(lbl42) = x4 p(lbl72) = 1 + x4 p(start) = x1 p(start0) = x1 The following rules are strictly oriented: [D >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] ==> cut(A,B,C,D,E,F,G,H) = 1 + D > D = cut(A,B,C,-1 + D,E,F,G,H) [H >= B && D >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] ==> cut(A,B,C,D,E,F,G,H) = 1 + D > D = lbl72(A,1 + B,C,-1 + D,B,F,G,H) The following rules are weakly oriented: [A >= 0 && C >= 0 && B = C && D = A && E = F && G = H] ==> start(A,B,C,D,E,F,G,H) = A >= D = lbl42(A,-1 + B,C,D,E,F,G,H) [A >= 0 && B = C && D = A && E = F && G = H] ==> start(A,B,C,D,E,F,G,H) = A >= D = cut(A,B,C,-1 + D,E,F,G,H) [H >= C && A >= 0 && B = C && D = A && E = F && G = H] ==> start(A,B,C,D,E,F,G,H) = A >= D = lbl72(A,1 + B,C,-1 + D,B,F,G,H) [A >= 1 + D && 1 + D >= 0 && 1 + H >= B && 1 + E = B && G = H] ==> lbl72(A,B,C,D,E,F,G,H) = 1 + D >= 1 + D = cut(A,B,C,D,E,F,G,H) [H >= B && A >= 1 + D && 1 + D >= 0 && 1 + H >= B && 1 + E = B && G = H] ==> lbl72(A,B,C,D,E,F,G,H) = 1 + D >= 1 + D = lbl72(A,1 + B,C,D,B,F,G,H) [B >= 0 && 1 + B >= 0 && D >= 0 && A >= D && G = H] ==> lbl42(A,B,C,D,E,F,G,H) = D >= D = lbl42(A,-1 + B,C,D,E,F,G,H) [1 + B >= 0 && D >= 0 && A >= D && G = H] ==> lbl42(A,B,C,D,E,F,G,H) = D >= D = cut(A,B,C,-1 + D,E,F,G,H) [H >= B && 1 + B >= 0 && D >= 0 && A >= D && G = H] ==> lbl42(A,B,C,D,E,F,G,H) = D >= D = lbl72(A,1 + B,C,-1 + D,B,F,G,H) [D >= 0 && B >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] ==> cut(A,B,C,D,E,F,G,H) = 1 + D >= D = lbl42(A,-1 + B,C,D,E,F,G,H) True ==> start0(A,B,C,D,E,F,G,H) = A >= A = start(A,C,C,A,F,F,H,H) * Step 7: PolyRank WORST_CASE(?,O(n^3)) + Considered Problem: Rules: 1. start(A,B,C,D,E,F,G,H) -> lbl42(A,-1 + B,C,D,E,F,G,H) [A >= 0 && C >= 0 && B = C && D = A && E = F && G = H] (1,1) 2. start(A,B,C,D,E,F,G,H) -> cut(A,B,C,-1 + D,E,F,G,H) [A >= 0 && B = C && D = A && E = F && G = H] (1,1) 3. start(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,-1 + D,B,F,G,H) [H >= C && A >= 0 && B = C && D = A && E = F && G = H] (1,1) 4. lbl72(A,B,C,D,E,F,G,H) -> cut(A,B,C,D,E,F,G,H) [A >= 1 + D && 1 + D >= 0 && 1 + H >= B && 1 + E = B && G = H] (?,1) 5. lbl72(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,D,B,F,G,H) [H >= B && A >= 1 + D && 1 + D >= 0 && 1 + H >= B && 1 + E = B && G = H] (?,1) 6. lbl42(A,B,C,D,E,F,G,H) -> lbl42(A,-1 + B,C,D,E,F,G,H) [B >= 0 && 1 + B >= 0 && D >= 0 && A >= D && G = H] (?,1) 7. lbl42(A,B,C,D,E,F,G,H) -> cut(A,B,C,-1 + D,E,F,G,H) [1 + B >= 0 && D >= 0 && A >= D && G = H] (?,1) 8. lbl42(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,-1 + D,B,F,G,H) [H >= B && 1 + B >= 0 && D >= 0 && A >= D && G = H] (?,1) 10. cut(A,B,C,D,E,F,G,H) -> lbl42(A,-1 + B,C,D,E,F,G,H) [D >= 0 && B >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] (?,1) 11. cut(A,B,C,D,E,F,G,H) -> cut(A,B,C,-1 + D,E,F,G,H) [D >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] (A,1) 12. cut(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,-1 + D,B,F,G,H) [H >= B && D >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] (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);(lbl42,8);(lbl72,8);(start,8);(start0,8);(stop,8)} Flow Graph: [1->{6,7,8},2->{10,11,12},3->{4,5},4->{10,11,12},5->{4,5},6->{6,7,8},7->{10,11,12},8->{4,5},10->{6,7,8} ,11->{10,11,12},12->{4,5},13->{1,2,3}] Sizebounds: (< 1,0,A>, A) (< 1,0,B>, 1 + C) (< 1,0,C>, C) (< 1,0,D>, A) (< 1,0,E>, F) (< 1,0,F>, F) (< 1,0,G>, H) (< 1,0,H>, H) (< 2,0,A>, A) (< 2,0,B>, C) (< 2,0,C>, C) (< 2,0,D>, 1 + A) (< 2,0,E>, F) (< 2,0,F>, F) (< 2,0,G>, H) (< 2,0,H>, H) (< 3,0,A>, A) (< 3,0,B>, 1 + C) (< 3,0,C>, C) (< 3,0,D>, 1 + A) (< 3,0,E>, C) (< 3,0,F>, F) (< 3,0,G>, H) (< 3,0,H>, H) (< 4,0,A>, A) (< 4,0,B>, 1 + H) (< 4,0,C>, C) (< 4,0,D>, A) (< 4,0,E>, ?) (< 4,0,F>, F) (< 4,0,G>, H) (< 4,0,H>, H) (< 5,0,A>, A) (< 5,0,B>, 1 + H) (< 5,0,C>, C) (< 5,0,D>, A) (< 5,0,E>, 1 + C + H) (< 5,0,F>, F) (< 5,0,G>, H) (< 5,0,H>, H) (< 6,0,A>, A) (< 6,0,B>, ?) (< 6,0,C>, C) (< 6,0,D>, A) (< 6,0,E>, ?) (< 6,0,F>, F) (< 6,0,G>, H) (< 6,0,H>, H) (< 7,0,A>, A) (< 7,0,B>, ?) (< 7,0,C>, C) (< 7,0,D>, A) (< 7,0,E>, ?) (< 7,0,F>, F) (< 7,0,G>, H) (< 7,0,H>, H) (< 8,0,A>, A) (< 8,0,B>, 1 + H) (< 8,0,C>, C) (< 8,0,D>, A) (< 8,0,E>, ?) (< 8,0,F>, F) (< 8,0,G>, H) (< 8,0,H>, H) (<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, C) (<10,0,D>, A) (<10,0,E>, ?) (<10,0,F>, F) (<10,0,G>, H) (<10,0,H>, H) (<11,0,A>, A) (<11,0,B>, ?) (<11,0,C>, C) (<11,0,D>, A) (<11,0,E>, ?) (<11,0,F>, F) (<11,0,G>, H) (<11,0,H>, H) (<12,0,A>, A) (<12,0,B>, 1 + H) (<12,0,C>, C) (<12,0,D>, A) (<12,0,E>, ?) (<12,0,F>, F) (<12,0,G>, H) (<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: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(cut) = 1 + x4 p(lbl42) = x4 p(lbl72) = 1 + x4 p(start) = x1 p(start0) = x1 The following rules are strictly oriented: [D >= 0 && B >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] ==> cut(A,B,C,D,E,F,G,H) = 1 + D > D = lbl42(A,-1 + B,C,D,E,F,G,H) [D >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] ==> cut(A,B,C,D,E,F,G,H) = 1 + D > D = cut(A,B,C,-1 + D,E,F,G,H) [H >= B && D >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] ==> cut(A,B,C,D,E,F,G,H) = 1 + D > D = lbl72(A,1 + B,C,-1 + D,B,F,G,H) The following rules are weakly oriented: [A >= 0 && C >= 0 && B = C && D = A && E = F && G = H] ==> start(A,B,C,D,E,F,G,H) = A >= D = lbl42(A,-1 + B,C,D,E,F,G,H) [A >= 0 && B = C && D = A && E = F && G = H] ==> start(A,B,C,D,E,F,G,H) = A >= D = cut(A,B,C,-1 + D,E,F,G,H) [H >= C && A >= 0 && B = C && D = A && E = F && G = H] ==> start(A,B,C,D,E,F,G,H) = A >= D = lbl72(A,1 + B,C,-1 + D,B,F,G,H) [A >= 1 + D && 1 + D >= 0 && 1 + H >= B && 1 + E = B && G = H] ==> lbl72(A,B,C,D,E,F,G,H) = 1 + D >= 1 + D = cut(A,B,C,D,E,F,G,H) [H >= B && A >= 1 + D && 1 + D >= 0 && 1 + H >= B && 1 + E = B && G = H] ==> lbl72(A,B,C,D,E,F,G,H) = 1 + D >= 1 + D = lbl72(A,1 + B,C,D,B,F,G,H) [B >= 0 && 1 + B >= 0 && D >= 0 && A >= D && G = H] ==> lbl42(A,B,C,D,E,F,G,H) = D >= D = lbl42(A,-1 + B,C,D,E,F,G,H) [1 + B >= 0 && D >= 0 && A >= D && G = H] ==> lbl42(A,B,C,D,E,F,G,H) = D >= D = cut(A,B,C,-1 + D,E,F,G,H) [H >= B && 1 + B >= 0 && D >= 0 && A >= D && G = H] ==> lbl42(A,B,C,D,E,F,G,H) = D >= D = lbl72(A,1 + B,C,-1 + D,B,F,G,H) True ==> start0(A,B,C,D,E,F,G,H) = A >= A = start(A,C,C,A,F,F,H,H) * Step 8: PolyRank WORST_CASE(?,O(n^3)) + Considered Problem: Rules: 1. start(A,B,C,D,E,F,G,H) -> lbl42(A,-1 + B,C,D,E,F,G,H) [A >= 0 && C >= 0 && B = C && D = A && E = F && G = H] (1,1) 2. start(A,B,C,D,E,F,G,H) -> cut(A,B,C,-1 + D,E,F,G,H) [A >= 0 && B = C && D = A && E = F && G = H] (1,1) 3. start(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,-1 + D,B,F,G,H) [H >= C && A >= 0 && B = C && D = A && E = F && G = H] (1,1) 4. lbl72(A,B,C,D,E,F,G,H) -> cut(A,B,C,D,E,F,G,H) [A >= 1 + D && 1 + D >= 0 && 1 + H >= B && 1 + E = B && G = H] (?,1) 5. lbl72(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,D,B,F,G,H) [H >= B && A >= 1 + D && 1 + D >= 0 && 1 + H >= B && 1 + E = B && G = H] (?,1) 6. lbl42(A,B,C,D,E,F,G,H) -> lbl42(A,-1 + B,C,D,E,F,G,H) [B >= 0 && 1 + B >= 0 && D >= 0 && A >= D && G = H] (?,1) 7. lbl42(A,B,C,D,E,F,G,H) -> cut(A,B,C,-1 + D,E,F,G,H) [1 + B >= 0 && D >= 0 && A >= D && G = H] (?,1) 8. lbl42(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,-1 + D,B,F,G,H) [H >= B && 1 + B >= 0 && D >= 0 && A >= D && G = H] (?,1) 10. cut(A,B,C,D,E,F,G,H) -> lbl42(A,-1 + B,C,D,E,F,G,H) [D >= 0 && B >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] (A,1) 11. cut(A,B,C,D,E,F,G,H) -> cut(A,B,C,-1 + D,E,F,G,H) [D >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] (A,1) 12. cut(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,-1 + D,B,F,G,H) [H >= B && D >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] (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);(lbl42,8);(lbl72,8);(start,8);(start0,8);(stop,8)} Flow Graph: [1->{6,7,8},2->{10,11,12},3->{4,5},4->{10,11,12},5->{4,5},6->{6,7,8},7->{10,11,12},8->{4,5},10->{6,7,8} ,11->{10,11,12},12->{4,5},13->{1,2,3}] Sizebounds: (< 1,0,A>, A) (< 1,0,B>, 1 + C) (< 1,0,C>, C) (< 1,0,D>, A) (< 1,0,E>, F) (< 1,0,F>, F) (< 1,0,G>, H) (< 1,0,H>, H) (< 2,0,A>, A) (< 2,0,B>, C) (< 2,0,C>, C) (< 2,0,D>, 1 + A) (< 2,0,E>, F) (< 2,0,F>, F) (< 2,0,G>, H) (< 2,0,H>, H) (< 3,0,A>, A) (< 3,0,B>, 1 + C) (< 3,0,C>, C) (< 3,0,D>, 1 + A) (< 3,0,E>, C) (< 3,0,F>, F) (< 3,0,G>, H) (< 3,0,H>, H) (< 4,0,A>, A) (< 4,0,B>, 1 + H) (< 4,0,C>, C) (< 4,0,D>, A) (< 4,0,E>, ?) (< 4,0,F>, F) (< 4,0,G>, H) (< 4,0,H>, H) (< 5,0,A>, A) (< 5,0,B>, 1 + H) (< 5,0,C>, C) (< 5,0,D>, A) (< 5,0,E>, 1 + C + H) (< 5,0,F>, F) (< 5,0,G>, H) (< 5,0,H>, H) (< 6,0,A>, A) (< 6,0,B>, ?) (< 6,0,C>, C) (< 6,0,D>, A) (< 6,0,E>, ?) (< 6,0,F>, F) (< 6,0,G>, H) (< 6,0,H>, H) (< 7,0,A>, A) (< 7,0,B>, ?) (< 7,0,C>, C) (< 7,0,D>, A) (< 7,0,E>, ?) (< 7,0,F>, F) (< 7,0,G>, H) (< 7,0,H>, H) (< 8,0,A>, A) (< 8,0,B>, 1 + H) (< 8,0,C>, C) (< 8,0,D>, A) (< 8,0,E>, ?) (< 8,0,F>, F) (< 8,0,G>, H) (< 8,0,H>, H) (<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, C) (<10,0,D>, A) (<10,0,E>, ?) (<10,0,F>, F) (<10,0,G>, H) (<10,0,H>, H) (<11,0,A>, A) (<11,0,B>, ?) (<11,0,C>, C) (<11,0,D>, A) (<11,0,E>, ?) (<11,0,F>, F) (<11,0,G>, H) (<11,0,H>, H) (<12,0,A>, A) (<12,0,B>, 1 + H) (<12,0,C>, C) (<12,0,D>, A) (<12,0,E>, ?) (<12,0,F>, F) (<12,0,G>, H) (<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: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(cut) = 1 + x4 p(lbl42) = 1 + x4 p(lbl72) = 1 + x4 p(start) = 1 + x1 p(start0) = 1 + x1 The following rules are strictly oriented: [A >= 0 && B = C && D = A && E = F && G = H] ==> start(A,B,C,D,E,F,G,H) = 1 + A > D = cut(A,B,C,-1 + D,E,F,G,H) [H >= C && A >= 0 && B = C && D = A && E = F && G = H] ==> start(A,B,C,D,E,F,G,H) = 1 + A > D = lbl72(A,1 + B,C,-1 + D,B,F,G,H) [H >= B && 1 + B >= 0 && D >= 0 && A >= D && G = H] ==> lbl42(A,B,C,D,E,F,G,H) = 1 + D > D = lbl72(A,1 + B,C,-1 + D,B,F,G,H) [D >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] ==> cut(A,B,C,D,E,F,G,H) = 1 + D > D = cut(A,B,C,-1 + D,E,F,G,H) [H >= B && D >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] ==> cut(A,B,C,D,E,F,G,H) = 1 + D > D = lbl72(A,1 + B,C,-1 + D,B,F,G,H) The following rules are weakly oriented: [A >= 0 && C >= 0 && B = C && D = A && E = F && G = H] ==> start(A,B,C,D,E,F,G,H) = 1 + A >= 1 + D = lbl42(A,-1 + B,C,D,E,F,G,H) [A >= 1 + D && 1 + D >= 0 && 1 + H >= B && 1 + E = B && G = H] ==> lbl72(A,B,C,D,E,F,G,H) = 1 + D >= 1 + D = cut(A,B,C,D,E,F,G,H) [H >= B && A >= 1 + D && 1 + D >= 0 && 1 + H >= B && 1 + E = B && G = H] ==> lbl72(A,B,C,D,E,F,G,H) = 1 + D >= 1 + D = lbl72(A,1 + B,C,D,B,F,G,H) [B >= 0 && 1 + B >= 0 && D >= 0 && A >= D && G = H] ==> lbl42(A,B,C,D,E,F,G,H) = 1 + D >= 1 + D = lbl42(A,-1 + B,C,D,E,F,G,H) [1 + B >= 0 && D >= 0 && A >= D && G = H] ==> lbl42(A,B,C,D,E,F,G,H) = 1 + D >= D = cut(A,B,C,-1 + D,E,F,G,H) [D >= 0 && B >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] ==> cut(A,B,C,D,E,F,G,H) = 1 + D >= 1 + D = lbl42(A,-1 + B,C,D,E,F,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^3)) + Considered Problem: Rules: 1. start(A,B,C,D,E,F,G,H) -> lbl42(A,-1 + B,C,D,E,F,G,H) [A >= 0 && C >= 0 && B = C && D = A && E = F && G = H] (1,1) 2. start(A,B,C,D,E,F,G,H) -> cut(A,B,C,-1 + D,E,F,G,H) [A >= 0 && B = C && D = A && E = F && G = H] (1,1) 3. start(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,-1 + D,B,F,G,H) [H >= C && A >= 0 && B = C && D = A && E = F && G = H] (1,1) 4. lbl72(A,B,C,D,E,F,G,H) -> cut(A,B,C,D,E,F,G,H) [A >= 1 + D && 1 + D >= 0 && 1 + H >= B && 1 + E = B && G = H] (?,1) 5. lbl72(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,D,B,F,G,H) [H >= B && A >= 1 + D && 1 + D >= 0 && 1 + H >= B && 1 + E = B && G = H] (?,1) 6. lbl42(A,B,C,D,E,F,G,H) -> lbl42(A,-1 + B,C,D,E,F,G,H) [B >= 0 && 1 + B >= 0 && D >= 0 && A >= D && G = H] (?,1) 7. lbl42(A,B,C,D,E,F,G,H) -> cut(A,B,C,-1 + D,E,F,G,H) [1 + B >= 0 && D >= 0 && A >= D && G = H] (?,1) 8. lbl42(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,-1 + D,B,F,G,H) [H >= B && 1 + B >= 0 && D >= 0 && A >= D && G = H] (1 + A,1) 10. cut(A,B,C,D,E,F,G,H) -> lbl42(A,-1 + B,C,D,E,F,G,H) [D >= 0 && B >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] (A,1) 11. cut(A,B,C,D,E,F,G,H) -> cut(A,B,C,-1 + D,E,F,G,H) [D >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] (A,1) 12. cut(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,-1 + D,B,F,G,H) [H >= B && D >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] (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);(lbl42,8);(lbl72,8);(start,8);(start0,8);(stop,8)} Flow Graph: [1->{6,7,8},2->{10,11,12},3->{4,5},4->{10,11,12},5->{4,5},6->{6,7,8},7->{10,11,12},8->{4,5},10->{6,7,8} ,11->{10,11,12},12->{4,5},13->{1,2,3}] Sizebounds: (< 1,0,A>, A) (< 1,0,B>, 1 + C) (< 1,0,C>, C) (< 1,0,D>, A) (< 1,0,E>, F) (< 1,0,F>, F) (< 1,0,G>, H) (< 1,0,H>, H) (< 2,0,A>, A) (< 2,0,B>, C) (< 2,0,C>, C) (< 2,0,D>, 1 + A) (< 2,0,E>, F) (< 2,0,F>, F) (< 2,0,G>, H) (< 2,0,H>, H) (< 3,0,A>, A) (< 3,0,B>, 1 + C) (< 3,0,C>, C) (< 3,0,D>, 1 + A) (< 3,0,E>, C) (< 3,0,F>, F) (< 3,0,G>, H) (< 3,0,H>, H) (< 4,0,A>, A) (< 4,0,B>, 1 + H) (< 4,0,C>, C) (< 4,0,D>, A) (< 4,0,E>, ?) (< 4,0,F>, F) (< 4,0,G>, H) (< 4,0,H>, H) (< 5,0,A>, A) (< 5,0,B>, 1 + H) (< 5,0,C>, C) (< 5,0,D>, A) (< 5,0,E>, 1 + C + H) (< 5,0,F>, F) (< 5,0,G>, H) (< 5,0,H>, H) (< 6,0,A>, A) (< 6,0,B>, ?) (< 6,0,C>, C) (< 6,0,D>, A) (< 6,0,E>, ?) (< 6,0,F>, F) (< 6,0,G>, H) (< 6,0,H>, H) (< 7,0,A>, A) (< 7,0,B>, ?) (< 7,0,C>, C) (< 7,0,D>, A) (< 7,0,E>, ?) (< 7,0,F>, F) (< 7,0,G>, H) (< 7,0,H>, H) (< 8,0,A>, A) (< 8,0,B>, 1 + H) (< 8,0,C>, C) (< 8,0,D>, A) (< 8,0,E>, ?) (< 8,0,F>, F) (< 8,0,G>, H) (< 8,0,H>, H) (<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, C) (<10,0,D>, A) (<10,0,E>, ?) (<10,0,F>, F) (<10,0,G>, H) (<10,0,H>, H) (<11,0,A>, A) (<11,0,B>, ?) (<11,0,C>, C) (<11,0,D>, A) (<11,0,E>, ?) (<11,0,F>, F) (<11,0,G>, H) (<11,0,H>, H) (<12,0,A>, A) (<12,0,B>, 1 + H) (<12,0,C>, C) (<12,0,D>, A) (<12,0,E>, ?) (<12,0,F>, F) (<12,0,G>, H) (<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: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(cut) = 1 + x4 p(lbl42) = 1 + x4 p(lbl72) = 1 + x4 p(start) = 1 + x1 p(start0) = 1 + x1 The following rules are strictly oriented: [A >= 0 && B = C && D = A && E = F && G = H] ==> start(A,B,C,D,E,F,G,H) = 1 + A > D = cut(A,B,C,-1 + D,E,F,G,H) [H >= C && A >= 0 && B = C && D = A && E = F && G = H] ==> start(A,B,C,D,E,F,G,H) = 1 + A > D = lbl72(A,1 + B,C,-1 + D,B,F,G,H) [1 + B >= 0 && D >= 0 && A >= D && G = H] ==> lbl42(A,B,C,D,E,F,G,H) = 1 + D > D = cut(A,B,C,-1 + D,E,F,G,H) [H >= B && 1 + B >= 0 && D >= 0 && A >= D && G = H] ==> lbl42(A,B,C,D,E,F,G,H) = 1 + D > D = lbl72(A,1 + B,C,-1 + D,B,F,G,H) [D >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] ==> cut(A,B,C,D,E,F,G,H) = 1 + D > D = cut(A,B,C,-1 + D,E,F,G,H) [H >= B && D >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] ==> cut(A,B,C,D,E,F,G,H) = 1 + D > D = lbl72(A,1 + B,C,-1 + D,B,F,G,H) The following rules are weakly oriented: [A >= 0 && C >= 0 && B = C && D = A && E = F && G = H] ==> start(A,B,C,D,E,F,G,H) = 1 + A >= 1 + D = lbl42(A,-1 + B,C,D,E,F,G,H) [A >= 1 + D && 1 + D >= 0 && 1 + H >= B && 1 + E = B && G = H] ==> lbl72(A,B,C,D,E,F,G,H) = 1 + D >= 1 + D = cut(A,B,C,D,E,F,G,H) [H >= B && A >= 1 + D && 1 + D >= 0 && 1 + H >= B && 1 + E = B && G = H] ==> lbl72(A,B,C,D,E,F,G,H) = 1 + D >= 1 + D = lbl72(A,1 + B,C,D,B,F,G,H) [B >= 0 && 1 + B >= 0 && D >= 0 && A >= D && G = H] ==> lbl42(A,B,C,D,E,F,G,H) = 1 + D >= 1 + D = lbl42(A,-1 + B,C,D,E,F,G,H) [D >= 0 && B >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] ==> cut(A,B,C,D,E,F,G,H) = 1 + D >= 1 + D = lbl42(A,-1 + B,C,D,E,F,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 10: PolyRank WORST_CASE(?,O(n^3)) + Considered Problem: Rules: 1. start(A,B,C,D,E,F,G,H) -> lbl42(A,-1 + B,C,D,E,F,G,H) [A >= 0 && C >= 0 && B = C && D = A && E = F && G = H] (1,1) 2. start(A,B,C,D,E,F,G,H) -> cut(A,B,C,-1 + D,E,F,G,H) [A >= 0 && B = C && D = A && E = F && G = H] (1,1) 3. start(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,-1 + D,B,F,G,H) [H >= C && A >= 0 && B = C && D = A && E = F && G = H] (1,1) 4. lbl72(A,B,C,D,E,F,G,H) -> cut(A,B,C,D,E,F,G,H) [A >= 1 + D && 1 + D >= 0 && 1 + H >= B && 1 + E = B && G = H] (?,1) 5. lbl72(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,D,B,F,G,H) [H >= B && A >= 1 + D && 1 + D >= 0 && 1 + H >= B && 1 + E = B && G = H] (?,1) 6. lbl42(A,B,C,D,E,F,G,H) -> lbl42(A,-1 + B,C,D,E,F,G,H) [B >= 0 && 1 + B >= 0 && D >= 0 && A >= D && G = H] (?,1) 7. lbl42(A,B,C,D,E,F,G,H) -> cut(A,B,C,-1 + D,E,F,G,H) [1 + B >= 0 && D >= 0 && A >= D && G = H] (1 + A,1) 8. lbl42(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,-1 + D,B,F,G,H) [H >= B && 1 + B >= 0 && D >= 0 && A >= D && G = H] (1 + A,1) 10. cut(A,B,C,D,E,F,G,H) -> lbl42(A,-1 + B,C,D,E,F,G,H) [D >= 0 && B >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] (A,1) 11. cut(A,B,C,D,E,F,G,H) -> cut(A,B,C,-1 + D,E,F,G,H) [D >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] (A,1) 12. cut(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,-1 + D,B,F,G,H) [H >= B && D >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] (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);(lbl42,8);(lbl72,8);(start,8);(start0,8);(stop,8)} Flow Graph: [1->{6,7,8},2->{10,11,12},3->{4,5},4->{10,11,12},5->{4,5},6->{6,7,8},7->{10,11,12},8->{4,5},10->{6,7,8} ,11->{10,11,12},12->{4,5},13->{1,2,3}] Sizebounds: (< 1,0,A>, A) (< 1,0,B>, 1 + C) (< 1,0,C>, C) (< 1,0,D>, A) (< 1,0,E>, F) (< 1,0,F>, F) (< 1,0,G>, H) (< 1,0,H>, H) (< 2,0,A>, A) (< 2,0,B>, C) (< 2,0,C>, C) (< 2,0,D>, 1 + A) (< 2,0,E>, F) (< 2,0,F>, F) (< 2,0,G>, H) (< 2,0,H>, H) (< 3,0,A>, A) (< 3,0,B>, 1 + C) (< 3,0,C>, C) (< 3,0,D>, 1 + A) (< 3,0,E>, C) (< 3,0,F>, F) (< 3,0,G>, H) (< 3,0,H>, H) (< 4,0,A>, A) (< 4,0,B>, 1 + H) (< 4,0,C>, C) (< 4,0,D>, A) (< 4,0,E>, ?) (< 4,0,F>, F) (< 4,0,G>, H) (< 4,0,H>, H) (< 5,0,A>, A) (< 5,0,B>, 1 + H) (< 5,0,C>, C) (< 5,0,D>, A) (< 5,0,E>, 1 + C + H) (< 5,0,F>, F) (< 5,0,G>, H) (< 5,0,H>, H) (< 6,0,A>, A) (< 6,0,B>, ?) (< 6,0,C>, C) (< 6,0,D>, A) (< 6,0,E>, ?) (< 6,0,F>, F) (< 6,0,G>, H) (< 6,0,H>, H) (< 7,0,A>, A) (< 7,0,B>, ?) (< 7,0,C>, C) (< 7,0,D>, A) (< 7,0,E>, ?) (< 7,0,F>, F) (< 7,0,G>, H) (< 7,0,H>, H) (< 8,0,A>, A) (< 8,0,B>, 1 + H) (< 8,0,C>, C) (< 8,0,D>, A) (< 8,0,E>, ?) (< 8,0,F>, F) (< 8,0,G>, H) (< 8,0,H>, H) (<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, C) (<10,0,D>, A) (<10,0,E>, ?) (<10,0,F>, F) (<10,0,G>, H) (<10,0,H>, H) (<11,0,A>, A) (<11,0,B>, ?) (<11,0,C>, C) (<11,0,D>, A) (<11,0,E>, ?) (<11,0,F>, F) (<11,0,G>, H) (<11,0,H>, H) (<12,0,A>, A) (<12,0,B>, 1 + H) (<12,0,C>, C) (<12,0,D>, A) (<12,0,E>, ?) (<12,0,F>, F) (<12,0,G>, H) (<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: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(cut) = 1 + x4 p(lbl42) = 1 + x4 p(lbl72) = 2 + x4 p(start) = 1 + x1 p(start0) = 1 + x1 The following rules are strictly oriented: [A >= 0 && B = C && D = A && E = F && G = H] ==> start(A,B,C,D,E,F,G,H) = 1 + A > D = cut(A,B,C,-1 + D,E,F,G,H) [A >= 1 + D && 1 + D >= 0 && 1 + H >= B && 1 + E = B && G = H] ==> lbl72(A,B,C,D,E,F,G,H) = 2 + D > 1 + D = cut(A,B,C,D,E,F,G,H) [1 + B >= 0 && D >= 0 && A >= D && G = H] ==> lbl42(A,B,C,D,E,F,G,H) = 1 + D > D = cut(A,B,C,-1 + D,E,F,G,H) [D >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] ==> cut(A,B,C,D,E,F,G,H) = 1 + D > D = cut(A,B,C,-1 + D,E,F,G,H) The following rules are weakly oriented: [A >= 0 && C >= 0 && B = C && D = A && E = F && G = H] ==> start(A,B,C,D,E,F,G,H) = 1 + A >= 1 + D = lbl42(A,-1 + B,C,D,E,F,G,H) [H >= C && A >= 0 && B = C && D = A && E = F && G = H] ==> start(A,B,C,D,E,F,G,H) = 1 + A >= 1 + D = lbl72(A,1 + B,C,-1 + D,B,F,G,H) [H >= B && A >= 1 + D && 1 + D >= 0 && 1 + H >= B && 1 + E = B && G = H] ==> lbl72(A,B,C,D,E,F,G,H) = 2 + D >= 2 + D = lbl72(A,1 + B,C,D,B,F,G,H) [B >= 0 && 1 + B >= 0 && D >= 0 && A >= D && G = H] ==> lbl42(A,B,C,D,E,F,G,H) = 1 + D >= 1 + D = lbl42(A,-1 + B,C,D,E,F,G,H) [H >= B && 1 + B >= 0 && D >= 0 && A >= D && G = H] ==> lbl42(A,B,C,D,E,F,G,H) = 1 + D >= 1 + D = lbl72(A,1 + B,C,-1 + D,B,F,G,H) [D >= 0 && B >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] ==> cut(A,B,C,D,E,F,G,H) = 1 + D >= 1 + D = lbl42(A,-1 + B,C,D,E,F,G,H) [H >= B && D >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] ==> cut(A,B,C,D,E,F,G,H) = 1 + D >= 1 + D = lbl72(A,1 + B,C,-1 + D,B,F,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 11: PolyRank WORST_CASE(?,O(n^3)) + Considered Problem: Rules: 1. start(A,B,C,D,E,F,G,H) -> lbl42(A,-1 + B,C,D,E,F,G,H) [A >= 0 && C >= 0 && B = C && D = A && E = F && G = H] (1,1) 2. start(A,B,C,D,E,F,G,H) -> cut(A,B,C,-1 + D,E,F,G,H) [A >= 0 && B = C && D = A && E = F && G = H] (1,1) 3. start(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,-1 + D,B,F,G,H) [H >= C && A >= 0 && B = C && D = A && E = F && G = H] (1,1) 4. lbl72(A,B,C,D,E,F,G,H) -> cut(A,B,C,D,E,F,G,H) [A >= 1 + D && 1 + D >= 0 && 1 + H >= B && 1 + E = B && G = H] (1 + A,1) 5. lbl72(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,D,B,F,G,H) [H >= B && A >= 1 + D && 1 + D >= 0 && 1 + H >= B && 1 + E = B && G = H] (?,1) 6. lbl42(A,B,C,D,E,F,G,H) -> lbl42(A,-1 + B,C,D,E,F,G,H) [B >= 0 && 1 + B >= 0 && D >= 0 && A >= D && G = H] (?,1) 7. lbl42(A,B,C,D,E,F,G,H) -> cut(A,B,C,-1 + D,E,F,G,H) [1 + B >= 0 && D >= 0 && A >= D && G = H] (1 + A,1) 8. lbl42(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,-1 + D,B,F,G,H) [H >= B && 1 + B >= 0 && D >= 0 && A >= D && G = H] (1 + A,1) 10. cut(A,B,C,D,E,F,G,H) -> lbl42(A,-1 + B,C,D,E,F,G,H) [D >= 0 && B >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] (A,1) 11. cut(A,B,C,D,E,F,G,H) -> cut(A,B,C,-1 + D,E,F,G,H) [D >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] (A,1) 12. cut(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,-1 + D,B,F,G,H) [H >= B && D >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] (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);(lbl42,8);(lbl72,8);(start,8);(start0,8);(stop,8)} Flow Graph: [1->{6,7,8},2->{10,11,12},3->{4,5},4->{10,11,12},5->{4,5},6->{6,7,8},7->{10,11,12},8->{4,5},10->{6,7,8} ,11->{10,11,12},12->{4,5},13->{1,2,3}] Sizebounds: (< 1,0,A>, A) (< 1,0,B>, 1 + C) (< 1,0,C>, C) (< 1,0,D>, A) (< 1,0,E>, F) (< 1,0,F>, F) (< 1,0,G>, H) (< 1,0,H>, H) (< 2,0,A>, A) (< 2,0,B>, C) (< 2,0,C>, C) (< 2,0,D>, 1 + A) (< 2,0,E>, F) (< 2,0,F>, F) (< 2,0,G>, H) (< 2,0,H>, H) (< 3,0,A>, A) (< 3,0,B>, 1 + C) (< 3,0,C>, C) (< 3,0,D>, 1 + A) (< 3,0,E>, C) (< 3,0,F>, F) (< 3,0,G>, H) (< 3,0,H>, H) (< 4,0,A>, A) (< 4,0,B>, 1 + H) (< 4,0,C>, C) (< 4,0,D>, A) (< 4,0,E>, ?) (< 4,0,F>, F) (< 4,0,G>, H) (< 4,0,H>, H) (< 5,0,A>, A) (< 5,0,B>, 1 + H) (< 5,0,C>, C) (< 5,0,D>, A) (< 5,0,E>, 1 + C + H) (< 5,0,F>, F) (< 5,0,G>, H) (< 5,0,H>, H) (< 6,0,A>, A) (< 6,0,B>, ?) (< 6,0,C>, C) (< 6,0,D>, A) (< 6,0,E>, ?) (< 6,0,F>, F) (< 6,0,G>, H) (< 6,0,H>, H) (< 7,0,A>, A) (< 7,0,B>, ?) (< 7,0,C>, C) (< 7,0,D>, A) (< 7,0,E>, ?) (< 7,0,F>, F) (< 7,0,G>, H) (< 7,0,H>, H) (< 8,0,A>, A) (< 8,0,B>, 1 + H) (< 8,0,C>, C) (< 8,0,D>, A) (< 8,0,E>, ?) (< 8,0,F>, F) (< 8,0,G>, H) (< 8,0,H>, H) (<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, C) (<10,0,D>, A) (<10,0,E>, ?) (<10,0,F>, F) (<10,0,G>, H) (<10,0,H>, H) (<11,0,A>, A) (<11,0,B>, ?) (<11,0,C>, C) (<11,0,D>, A) (<11,0,E>, ?) (<11,0,F>, F) (<11,0,G>, H) (<11,0,H>, H) (<12,0,A>, A) (<12,0,B>, 1 + H) (<12,0,C>, C) (<12,0,D>, A) (<12,0,E>, ?) (<12,0,F>, F) (<12,0,G>, H) (<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: PolyRank {useFarkas = True, withSizebounds = [6,4,5,8,12,7,11], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(cut) = 1 + -1*x2 + x7 p(lbl42) = 2 + x7 p(lbl72) = 2 + -1*x2 + x8 The following rules are strictly oriented: [A >= 1 + D && 1 + D >= 0 && 1 + H >= B && 1 + E = B && G = H] ==> lbl72(A,B,C,D,E,F,G,H) = 2 + -1*B + H > 1 + -1*B + G = cut(A,B,C,D,E,F,G,H) [H >= B && A >= 1 + D && 1 + D >= 0 && 1 + H >= B && 1 + E = B && G = H] ==> lbl72(A,B,C,D,E,F,G,H) = 2 + -1*B + H > 1 + -1*B + H = lbl72(A,1 + B,C,D,B,F,G,H) The following rules are weakly oriented: [B >= 0 && 1 + B >= 0 && D >= 0 && A >= D && G = H] ==> lbl42(A,B,C,D,E,F,G,H) = 2 + G >= 2 + G = lbl42(A,-1 + B,C,D,E,F,G,H) [1 + B >= 0 && D >= 0 && A >= D && G = H] ==> lbl42(A,B,C,D,E,F,G,H) = 2 + G >= 1 + -1*B + G = cut(A,B,C,-1 + D,E,F,G,H) [H >= B && 1 + B >= 0 && D >= 0 && A >= D && G = H] ==> lbl42(A,B,C,D,E,F,G,H) = 2 + G >= 1 + -1*B + H = lbl72(A,1 + B,C,-1 + D,B,F,G,H) [D >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] ==> cut(A,B,C,D,E,F,G,H) = 1 + -1*B + G >= 1 + -1*B + G = cut(A,B,C,-1 + D,E,F,G,H) [H >= B && D >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] ==> cut(A,B,C,D,E,F,G,H) = 1 + -1*B + G >= 1 + -1*B + H = lbl72(A,1 + B,C,-1 + D,B,F,G,H) We use the following global sizebounds: (< 1,0,A>, A) (< 1,0,B>, 1 + C) (< 1,0,C>, C) (< 1,0,D>, A) (< 1,0,E>, F) (< 1,0,F>, F) (< 1,0,G>, H) (< 1,0,H>, H) (< 2,0,A>, A) (< 2,0,B>, C) (< 2,0,C>, C) (< 2,0,D>, 1 + A) (< 2,0,E>, F) (< 2,0,F>, F) (< 2,0,G>, H) (< 2,0,H>, H) (< 3,0,A>, A) (< 3,0,B>, 1 + C) (< 3,0,C>, C) (< 3,0,D>, 1 + A) (< 3,0,E>, C) (< 3,0,F>, F) (< 3,0,G>, H) (< 3,0,H>, H) (< 4,0,A>, A) (< 4,0,B>, 1 + H) (< 4,0,C>, C) (< 4,0,D>, A) (< 4,0,E>, ?) (< 4,0,F>, F) (< 4,0,G>, H) (< 4,0,H>, H) (< 5,0,A>, A) (< 5,0,B>, 1 + H) (< 5,0,C>, C) (< 5,0,D>, A) (< 5,0,E>, 1 + C + H) (< 5,0,F>, F) (< 5,0,G>, H) (< 5,0,H>, H) (< 6,0,A>, A) (< 6,0,B>, ?) (< 6,0,C>, C) (< 6,0,D>, A) (< 6,0,E>, ?) (< 6,0,F>, F) (< 6,0,G>, H) (< 6,0,H>, H) (< 7,0,A>, A) (< 7,0,B>, ?) (< 7,0,C>, C) (< 7,0,D>, A) (< 7,0,E>, ?) (< 7,0,F>, F) (< 7,0,G>, H) (< 7,0,H>, H) (< 8,0,A>, A) (< 8,0,B>, 1 + H) (< 8,0,C>, C) (< 8,0,D>, A) (< 8,0,E>, ?) (< 8,0,F>, F) (< 8,0,G>, H) (< 8,0,H>, H) (<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, C) (<10,0,D>, A) (<10,0,E>, ?) (<10,0,F>, F) (<10,0,G>, H) (<10,0,H>, H) (<11,0,A>, A) (<11,0,B>, ?) (<11,0,C>, C) (<11,0,D>, A) (<11,0,E>, ?) (<11,0,F>, F) (<11,0,G>, H) (<11,0,H>, H) (<12,0,A>, A) (<12,0,B>, 1 + H) (<12,0,C>, C) (<12,0,D>, A) (<12,0,E>, ?) (<12,0,F>, F) (<12,0,G>, H) (<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 12: PolyRank WORST_CASE(?,O(n^3)) + Considered Problem: Rules: 1. start(A,B,C,D,E,F,G,H) -> lbl42(A,-1 + B,C,D,E,F,G,H) [A >= 0 && C >= 0 && B = C && D = A && E = F && G = H] (1,1) 2. start(A,B,C,D,E,F,G,H) -> cut(A,B,C,-1 + D,E,F,G,H) [A >= 0 && B = C && D = A && E = F && G = H] (1,1) 3. start(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,-1 + D,B,F,G,H) [H >= C && A >= 0 && B = C && D = A && E = F && G = H] (1,1) 4. lbl72(A,B,C,D,E,F,G,H) -> cut(A,B,C,D,E,F,G,H) [A >= 1 + D && 1 + D >= 0 && 1 + H >= B && 1 + E = B && G = H] (1 + A,1) 5. lbl72(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,D,B,F,G,H) [H >= B && A >= 1 + D && 1 + D >= 0 && 1 + H >= B && 1 + E = B && G = H] (6 + 2*A + A*H + 2*C + 3*H,1) 6. lbl42(A,B,C,D,E,F,G,H) -> lbl42(A,-1 + B,C,D,E,F,G,H) [B >= 0 && 1 + B >= 0 && D >= 0 && A >= D && G = H] (?,1) 7. lbl42(A,B,C,D,E,F,G,H) -> cut(A,B,C,-1 + D,E,F,G,H) [1 + B >= 0 && D >= 0 && A >= D && G = H] (1 + A,1) 8. lbl42(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,-1 + D,B,F,G,H) [H >= B && 1 + B >= 0 && D >= 0 && A >= D && G = H] (1 + A,1) 10. cut(A,B,C,D,E,F,G,H) -> lbl42(A,-1 + B,C,D,E,F,G,H) [D >= 0 && B >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] (A,1) 11. cut(A,B,C,D,E,F,G,H) -> cut(A,B,C,-1 + D,E,F,G,H) [D >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] (A,1) 12. cut(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,-1 + D,B,F,G,H) [H >= B && D >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] (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);(lbl42,8);(lbl72,8);(start,8);(start0,8);(stop,8)} Flow Graph: [1->{6,7,8},2->{10,11,12},3->{4,5},4->{10,11,12},5->{4,5},6->{6,7,8},7->{10,11,12},8->{4,5},10->{6,7,8} ,11->{10,11,12},12->{4,5},13->{1,2,3}] Sizebounds: (< 1,0,A>, A) (< 1,0,B>, 1 + C) (< 1,0,C>, C) (< 1,0,D>, A) (< 1,0,E>, F) (< 1,0,F>, F) (< 1,0,G>, H) (< 1,0,H>, H) (< 2,0,A>, A) (< 2,0,B>, C) (< 2,0,C>, C) (< 2,0,D>, 1 + A) (< 2,0,E>, F) (< 2,0,F>, F) (< 2,0,G>, H) (< 2,0,H>, H) (< 3,0,A>, A) (< 3,0,B>, 1 + C) (< 3,0,C>, C) (< 3,0,D>, 1 + A) (< 3,0,E>, C) (< 3,0,F>, F) (< 3,0,G>, H) (< 3,0,H>, H) (< 4,0,A>, A) (< 4,0,B>, 1 + H) (< 4,0,C>, C) (< 4,0,D>, A) (< 4,0,E>, ?) (< 4,0,F>, F) (< 4,0,G>, H) (< 4,0,H>, H) (< 5,0,A>, A) (< 5,0,B>, 1 + H) (< 5,0,C>, C) (< 5,0,D>, A) (< 5,0,E>, 1 + C + H) (< 5,0,F>, F) (< 5,0,G>, H) (< 5,0,H>, H) (< 6,0,A>, A) (< 6,0,B>, ?) (< 6,0,C>, C) (< 6,0,D>, A) (< 6,0,E>, ?) (< 6,0,F>, F) (< 6,0,G>, H) (< 6,0,H>, H) (< 7,0,A>, A) (< 7,0,B>, ?) (< 7,0,C>, C) (< 7,0,D>, A) (< 7,0,E>, ?) (< 7,0,F>, F) (< 7,0,G>, H) (< 7,0,H>, H) (< 8,0,A>, A) (< 8,0,B>, 1 + H) (< 8,0,C>, C) (< 8,0,D>, A) (< 8,0,E>, ?) (< 8,0,F>, F) (< 8,0,G>, H) (< 8,0,H>, H) (<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, C) (<10,0,D>, A) (<10,0,E>, ?) (<10,0,F>, F) (<10,0,G>, H) (<10,0,H>, H) (<11,0,A>, A) (<11,0,B>, ?) (<11,0,C>, C) (<11,0,D>, A) (<11,0,E>, ?) (<11,0,F>, F) (<11,0,G>, H) (<11,0,H>, H) (<12,0,A>, A) (<12,0,B>, 1 + H) (<12,0,C>, C) (<12,0,D>, A) (<12,0,E>, ?) (<12,0,F>, F) (<12,0,G>, H) (<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: PolyRank {useFarkas = True, withSizebounds = [6,10,4,8,12,7,11], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(cut) = 1 + x2 + x4 p(lbl42) = 2 + x2 + x4 p(lbl72) = 1 + x2 + x4 The following rules are strictly oriented: [B >= 0 && 1 + B >= 0 && D >= 0 && A >= D && G = H] ==> lbl42(A,B,C,D,E,F,G,H) = 2 + B + D > 1 + B + D = lbl42(A,-1 + B,C,D,E,F,G,H) [1 + B >= 0 && D >= 0 && A >= D && G = H] ==> lbl42(A,B,C,D,E,F,G,H) = 2 + B + D > B + D = cut(A,B,C,-1 + D,E,F,G,H) [H >= B && 1 + B >= 0 && D >= 0 && A >= D && G = H] ==> lbl42(A,B,C,D,E,F,G,H) = 2 + B + D > 1 + B + D = lbl72(A,1 + B,C,-1 + D,B,F,G,H) The following rules are weakly oriented: [A >= 1 + D && 1 + D >= 0 && 1 + H >= B && 1 + E = B && G = H] ==> lbl72(A,B,C,D,E,F,G,H) = 1 + B + D >= 1 + B + D = cut(A,B,C,D,E,F,G,H) [D >= 0 && B >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] ==> cut(A,B,C,D,E,F,G,H) = 1 + B + D >= 1 + B + D = lbl42(A,-1 + B,C,D,E,F,G,H) [D >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] ==> cut(A,B,C,D,E,F,G,H) = 1 + B + D >= B + D = cut(A,B,C,-1 + D,E,F,G,H) [H >= B && D >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] ==> cut(A,B,C,D,E,F,G,H) = 1 + B + D >= 1 + B + D = lbl72(A,1 + B,C,-1 + D,B,F,G,H) We use the following global sizebounds: (< 1,0,A>, A) (< 1,0,B>, 1 + C) (< 1,0,C>, C) (< 1,0,D>, A) (< 1,0,E>, F) (< 1,0,F>, F) (< 1,0,G>, H) (< 1,0,H>, H) (< 2,0,A>, A) (< 2,0,B>, C) (< 2,0,C>, C) (< 2,0,D>, 1 + A) (< 2,0,E>, F) (< 2,0,F>, F) (< 2,0,G>, H) (< 2,0,H>, H) (< 3,0,A>, A) (< 3,0,B>, 1 + C) (< 3,0,C>, C) (< 3,0,D>, 1 + A) (< 3,0,E>, C) (< 3,0,F>, F) (< 3,0,G>, H) (< 3,0,H>, H) (< 4,0,A>, A) (< 4,0,B>, 1 + H) (< 4,0,C>, C) (< 4,0,D>, A) (< 4,0,E>, ?) (< 4,0,F>, F) (< 4,0,G>, H) (< 4,0,H>, H) (< 5,0,A>, A) (< 5,0,B>, 1 + H) (< 5,0,C>, C) (< 5,0,D>, A) (< 5,0,E>, 1 + C + H) (< 5,0,F>, F) (< 5,0,G>, H) (< 5,0,H>, H) (< 6,0,A>, A) (< 6,0,B>, ?) (< 6,0,C>, C) (< 6,0,D>, A) (< 6,0,E>, ?) (< 6,0,F>, F) (< 6,0,G>, H) (< 6,0,H>, H) (< 7,0,A>, A) (< 7,0,B>, ?) (< 7,0,C>, C) (< 7,0,D>, A) (< 7,0,E>, ?) (< 7,0,F>, F) (< 7,0,G>, H) (< 7,0,H>, H) (< 8,0,A>, A) (< 8,0,B>, 1 + H) (< 8,0,C>, C) (< 8,0,D>, A) (< 8,0,E>, ?) (< 8,0,F>, F) (< 8,0,G>, H) (< 8,0,H>, H) (<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, C) (<10,0,D>, A) (<10,0,E>, ?) (<10,0,F>, F) (<10,0,G>, H) (<10,0,H>, H) (<11,0,A>, A) (<11,0,B>, ?) (<11,0,C>, C) (<11,0,D>, A) (<11,0,E>, ?) (<11,0,F>, F) (<11,0,G>, H) (<11,0,H>, H) (<12,0,A>, A) (<12,0,B>, 1 + H) (<12,0,C>, C) (<12,0,D>, A) (<12,0,E>, ?) (<12,0,F>, F) (<12,0,G>, H) (<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 13: KnowledgePropagation WORST_CASE(?,O(n^3)) + Considered Problem: Rules: 1. start(A,B,C,D,E,F,G,H) -> lbl42(A,-1 + B,C,D,E,F,G,H) [A >= 0 && C >= 0 && B = C && D = A && E = F && G = H] (1,1) 2. start(A,B,C,D,E,F,G,H) -> cut(A,B,C,-1 + D,E,F,G,H) [A >= 0 && B = C && D = A && E = F && G = H] (1,1) 3. start(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,-1 + D,B,F,G,H) [H >= C && A >= 0 && B = C && D = A && E = F && G = H] (1,1) 4. lbl72(A,B,C,D,E,F,G,H) -> cut(A,B,C,D,E,F,G,H) [A >= 1 + D && 1 + D >= 0 && 1 + H >= B && 1 + E = B && G = H] (1 + A,1) 5. lbl72(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,D,B,F,G,H) [H >= B && A >= 1 + D && 1 + D >= 0 && 1 + H >= B && 1 + E = B && G = H] (6 + 2*A + A*H + 2*C + 3*H,1) 6. lbl42(A,B,C,D,E,F,G,H) -> lbl42(A,-1 + B,C,D,E,F,G,H) [B >= 0 && 1 + B >= 0 && D >= 0 && A >= D && G = H] (20 + 13*A + 2*A*C + 7*A*H + A*H^2 + 2*A^2 + A^2*H + 7*C + 2*C*H + 12*H + 3*H^2,1) 7. lbl42(A,B,C,D,E,F,G,H) -> cut(A,B,C,-1 + D,E,F,G,H) [1 + B >= 0 && D >= 0 && A >= D && G = H] (1 + A,1) 8. lbl42(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,-1 + D,B,F,G,H) [H >= B && 1 + B >= 0 && D >= 0 && A >= D && G = H] (1 + A,1) 10. cut(A,B,C,D,E,F,G,H) -> lbl42(A,-1 + B,C,D,E,F,G,H) [D >= 0 && B >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] (A,1) 11. cut(A,B,C,D,E,F,G,H) -> cut(A,B,C,-1 + D,E,F,G,H) [D >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] (A,1) 12. cut(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,-1 + D,B,F,G,H) [H >= B && D >= 0 && 1 + D >= 0 && A >= 1 + D && G = H] (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);(lbl42,8);(lbl72,8);(start,8);(start0,8);(stop,8)} Flow Graph: [1->{6,7,8},2->{10,11,12},3->{4,5},4->{10,11,12},5->{4,5},6->{6,7,8},7->{10,11,12},8->{4,5},10->{6,7,8} ,11->{10,11,12},12->{4,5},13->{1,2,3}] Sizebounds: (< 1,0,A>, A) (< 1,0,B>, 1 + C) (< 1,0,C>, C) (< 1,0,D>, A) (< 1,0,E>, F) (< 1,0,F>, F) (< 1,0,G>, H) (< 1,0,H>, H) (< 2,0,A>, A) (< 2,0,B>, C) (< 2,0,C>, C) (< 2,0,D>, 1 + A) (< 2,0,E>, F) (< 2,0,F>, F) (< 2,0,G>, H) (< 2,0,H>, H) (< 3,0,A>, A) (< 3,0,B>, 1 + C) (< 3,0,C>, C) (< 3,0,D>, 1 + A) (< 3,0,E>, C) (< 3,0,F>, F) (< 3,0,G>, H) (< 3,0,H>, H) (< 4,0,A>, A) (< 4,0,B>, 1 + H) (< 4,0,C>, C) (< 4,0,D>, A) (< 4,0,E>, ?) (< 4,0,F>, F) (< 4,0,G>, H) (< 4,0,H>, H) (< 5,0,A>, A) (< 5,0,B>, 1 + H) (< 5,0,C>, C) (< 5,0,D>, A) (< 5,0,E>, 1 + C + H) (< 5,0,F>, F) (< 5,0,G>, H) (< 5,0,H>, H) (< 6,0,A>, A) (< 6,0,B>, ?) (< 6,0,C>, C) (< 6,0,D>, A) (< 6,0,E>, ?) (< 6,0,F>, F) (< 6,0,G>, H) (< 6,0,H>, H) (< 7,0,A>, A) (< 7,0,B>, ?) (< 7,0,C>, C) (< 7,0,D>, A) (< 7,0,E>, ?) (< 7,0,F>, F) (< 7,0,G>, H) (< 7,0,H>, H) (< 8,0,A>, A) (< 8,0,B>, 1 + H) (< 8,0,C>, C) (< 8,0,D>, A) (< 8,0,E>, ?) (< 8,0,F>, F) (< 8,0,G>, H) (< 8,0,H>, H) (<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, C) (<10,0,D>, A) (<10,0,E>, ?) (<10,0,F>, F) (<10,0,G>, H) (<10,0,H>, H) (<11,0,A>, A) (<11,0,B>, ?) (<11,0,C>, C) (<11,0,D>, A) (<11,0,E>, ?) (<11,0,F>, F) (<11,0,G>, H) (<11,0,H>, H) (<12,0,A>, A) (<12,0,B>, 1 + H) (<12,0,C>, C) (<12,0,D>, A) (<12,0,E>, ?) (<12,0,F>, F) (<12,0,G>, H) (<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: KnowledgePropagation + Details: The problem is already solved. WORST_CASE(?,O(n^3))