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