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