WORST_CASE(?,O(1)) * Step 1: LocalSizeboundsProc WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f0(A,B,C) -> f10(1,B,C) True (1,1) 1. f10(A,B,C) -> f13(A,1,C) [5 >= A] (?,1) 2. f13(A,B,C) -> f13(A,1 + B,C) [5 >= B] (?,1) 3. f21(A,B,C) -> f24(A,1,C) [5 >= A] (?,1) 4. f24(A,B,C) -> f27(A,B,1) [5 >= B] (?,1) 5. f27(A,B,C) -> f27(A,B,1 + C) [5 >= C] (?,1) 6. f27(A,B,C) -> f24(A,1 + B,C) [C >= 6] (?,1) 7. f24(A,B,C) -> f21(1 + A,B,C) [B >= 6] (?,1) 8. f21(A,B,C) -> f39(A,B,C) [A >= 6] (?,1) 9. f13(A,B,C) -> f10(1 + A,B,C) [B >= 6] (?,1) 10. f10(A,B,C) -> f21(1,B,C) [A >= 6] (?,1) Signature: {(f0,3);(f10,3);(f13,3);(f21,3);(f24,3);(f27,3);(f39,3)} Flow Graph: [0->{1,10},1->{2,9},2->{2,9},3->{4,7},4->{5,6},5->{5,6},6->{4,7},7->{3,8},8->{},9->{1,10},10->{3,8}] + Applied Processor: LocalSizeboundsProc + Details: LocalSizebounds generated; rvgraph (< 0,0,A>, 1, .= 1) (< 0,0,B>, B, .= 0) (< 0,0,C>, C, .= 0) (< 1,0,A>, A, .= 0) (< 1,0,B>, 1, .= 1) (< 1,0,C>, C, .= 0) (< 2,0,A>, A, .= 0) (< 2,0,B>, 1 + B, .+ 1) (< 2,0,C>, C, .= 0) (< 3,0,A>, A, .= 0) (< 3,0,B>, 1, .= 1) (< 3,0,C>, C, .= 0) (< 4,0,A>, A, .= 0) (< 4,0,B>, B, .= 0) (< 4,0,C>, 1, .= 1) (< 5,0,A>, A, .= 0) (< 5,0,B>, B, .= 0) (< 5,0,C>, 1 + C, .+ 1) (< 6,0,A>, A, .= 0) (< 6,0,B>, 1 + B, .+ 1) (< 6,0,C>, C, .= 0) (< 7,0,A>, 1 + A, .+ 1) (< 7,0,B>, B, .= 0) (< 7,0,C>, C, .= 0) (< 8,0,A>, A, .= 0) (< 8,0,B>, B, .= 0) (< 8,0,C>, C, .= 0) (< 9,0,A>, 1 + A, .+ 1) (< 9,0,B>, B, .= 0) (< 9,0,C>, C, .= 0) (<10,0,A>, 1, .= 1) (<10,0,B>, B, .= 0) (<10,0,C>, C, .= 0) * Step 2: SizeboundsProc WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f0(A,B,C) -> f10(1,B,C) True (1,1) 1. f10(A,B,C) -> f13(A,1,C) [5 >= A] (?,1) 2. f13(A,B,C) -> f13(A,1 + B,C) [5 >= B] (?,1) 3. f21(A,B,C) -> f24(A,1,C) [5 >= A] (?,1) 4. f24(A,B,C) -> f27(A,B,1) [5 >= B] (?,1) 5. f27(A,B,C) -> f27(A,B,1 + C) [5 >= C] (?,1) 6. f27(A,B,C) -> f24(A,1 + B,C) [C >= 6] (?,1) 7. f24(A,B,C) -> f21(1 + A,B,C) [B >= 6] (?,1) 8. f21(A,B,C) -> f39(A,B,C) [A >= 6] (?,1) 9. f13(A,B,C) -> f10(1 + A,B,C) [B >= 6] (?,1) 10. f10(A,B,C) -> f21(1,B,C) [A >= 6] (?,1) Signature: {(f0,3);(f10,3);(f13,3);(f21,3);(f24,3);(f27,3);(f39,3)} Flow Graph: [0->{1,10},1->{2,9},2->{2,9},3->{4,7},4->{5,6},5->{5,6},6->{4,7},7->{3,8},8->{},9->{1,10},10->{3,8}] Sizebounds: (< 0,0,A>, ?) (< 0,0,B>, ?) (< 0,0,C>, ?) (< 1,0,A>, ?) (< 1,0,B>, ?) (< 1,0,C>, ?) (< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, ?) (< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, ?) (< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, ?) (< 5,0,A>, ?) (< 5,0,B>, ?) (< 5,0,C>, ?) (< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,C>, ?) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, ?) (<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?) + Applied Processor: SizeboundsProc + Details: Sizebounds computed: (< 0,0,A>, 1) (< 0,0,B>, B) (< 0,0,C>, C) (< 1,0,A>, 5) (< 1,0,B>, 1) (< 1,0,C>, C) (< 2,0,A>, 5) (< 2,0,B>, 6) (< 2,0,C>, C) (< 3,0,A>, 5) (< 3,0,B>, 1) (< 3,0,C>, ?) (< 4,0,A>, ?) (< 4,0,B>, 5) (< 4,0,C>, 1) (< 5,0,A>, ?) (< 5,0,B>, 5) (< 5,0,C>, 6) (< 6,0,A>, ?) (< 6,0,B>, 5) (< 6,0,C>, 6) (< 7,0,A>, ?) (< 7,0,B>, 5) (< 7,0,C>, ?) (< 8,0,A>, ?) (< 8,0,B>, 6 + B) (< 8,0,C>, ?) (< 9,0,A>, 5) (< 9,0,B>, 6) (< 9,0,C>, C) (<10,0,A>, 1) (<10,0,B>, 6 + B) (<10,0,C>, C) * Step 3: UnsatPaths WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f0(A,B,C) -> f10(1,B,C) True (1,1) 1. f10(A,B,C) -> f13(A,1,C) [5 >= A] (?,1) 2. f13(A,B,C) -> f13(A,1 + B,C) [5 >= B] (?,1) 3. f21(A,B,C) -> f24(A,1,C) [5 >= A] (?,1) 4. f24(A,B,C) -> f27(A,B,1) [5 >= B] (?,1) 5. f27(A,B,C) -> f27(A,B,1 + C) [5 >= C] (?,1) 6. f27(A,B,C) -> f24(A,1 + B,C) [C >= 6] (?,1) 7. f24(A,B,C) -> f21(1 + A,B,C) [B >= 6] (?,1) 8. f21(A,B,C) -> f39(A,B,C) [A >= 6] (?,1) 9. f13(A,B,C) -> f10(1 + A,B,C) [B >= 6] (?,1) 10. f10(A,B,C) -> f21(1,B,C) [A >= 6] (?,1) Signature: {(f0,3);(f10,3);(f13,3);(f21,3);(f24,3);(f27,3);(f39,3)} Flow Graph: [0->{1,10},1->{2,9},2->{2,9},3->{4,7},4->{5,6},5->{5,6},6->{4,7},7->{3,8},8->{},9->{1,10},10->{3,8}] Sizebounds: (< 0,0,A>, 1) (< 0,0,B>, B) (< 0,0,C>, C) (< 1,0,A>, 5) (< 1,0,B>, 1) (< 1,0,C>, C) (< 2,0,A>, 5) (< 2,0,B>, 6) (< 2,0,C>, C) (< 3,0,A>, 5) (< 3,0,B>, 1) (< 3,0,C>, ?) (< 4,0,A>, ?) (< 4,0,B>, 5) (< 4,0,C>, 1) (< 5,0,A>, ?) (< 5,0,B>, 5) (< 5,0,C>, 6) (< 6,0,A>, ?) (< 6,0,B>, 5) (< 6,0,C>, 6) (< 7,0,A>, ?) (< 7,0,B>, 5) (< 7,0,C>, ?) (< 8,0,A>, ?) (< 8,0,B>, 6 + B) (< 8,0,C>, ?) (< 9,0,A>, 5) (< 9,0,B>, 6) (< 9,0,C>, C) (<10,0,A>, 1) (<10,0,B>, 6 + B) (<10,0,C>, C) + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(0,10),(1,9),(3,7),(4,6),(10,8)] * Step 4: LeafRules WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f0(A,B,C) -> f10(1,B,C) True (1,1) 1. f10(A,B,C) -> f13(A,1,C) [5 >= A] (?,1) 2. f13(A,B,C) -> f13(A,1 + B,C) [5 >= B] (?,1) 3. f21(A,B,C) -> f24(A,1,C) [5 >= A] (?,1) 4. f24(A,B,C) -> f27(A,B,1) [5 >= B] (?,1) 5. f27(A,B,C) -> f27(A,B,1 + C) [5 >= C] (?,1) 6. f27(A,B,C) -> f24(A,1 + B,C) [C >= 6] (?,1) 7. f24(A,B,C) -> f21(1 + A,B,C) [B >= 6] (?,1) 8. f21(A,B,C) -> f39(A,B,C) [A >= 6] (?,1) 9. f13(A,B,C) -> f10(1 + A,B,C) [B >= 6] (?,1) 10. f10(A,B,C) -> f21(1,B,C) [A >= 6] (?,1) Signature: {(f0,3);(f10,3);(f13,3);(f21,3);(f24,3);(f27,3);(f39,3)} Flow Graph: [0->{1},1->{2},2->{2,9},3->{4},4->{5},5->{5,6},6->{4,7},7->{3,8},8->{},9->{1,10},10->{3}] Sizebounds: (< 0,0,A>, 1) (< 0,0,B>, B) (< 0,0,C>, C) (< 1,0,A>, 5) (< 1,0,B>, 1) (< 1,0,C>, C) (< 2,0,A>, 5) (< 2,0,B>, 6) (< 2,0,C>, C) (< 3,0,A>, 5) (< 3,0,B>, 1) (< 3,0,C>, ?) (< 4,0,A>, ?) (< 4,0,B>, 5) (< 4,0,C>, 1) (< 5,0,A>, ?) (< 5,0,B>, 5) (< 5,0,C>, 6) (< 6,0,A>, ?) (< 6,0,B>, 5) (< 6,0,C>, 6) (< 7,0,A>, ?) (< 7,0,B>, 5) (< 7,0,C>, ?) (< 8,0,A>, ?) (< 8,0,B>, 6 + B) (< 8,0,C>, ?) (< 9,0,A>, 5) (< 9,0,B>, 6) (< 9,0,C>, C) (<10,0,A>, 1) (<10,0,B>, 6 + B) (<10,0,C>, C) + Applied Processor: LeafRules + Details: The following transitions are estimated by its predecessors and are removed [8] * Step 5: PolyRank WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f0(A,B,C) -> f10(1,B,C) True (1,1) 1. f10(A,B,C) -> f13(A,1,C) [5 >= A] (?,1) 2. f13(A,B,C) -> f13(A,1 + B,C) [5 >= B] (?,1) 3. f21(A,B,C) -> f24(A,1,C) [5 >= A] (?,1) 4. f24(A,B,C) -> f27(A,B,1) [5 >= B] (?,1) 5. f27(A,B,C) -> f27(A,B,1 + C) [5 >= C] (?,1) 6. f27(A,B,C) -> f24(A,1 + B,C) [C >= 6] (?,1) 7. f24(A,B,C) -> f21(1 + A,B,C) [B >= 6] (?,1) 9. f13(A,B,C) -> f10(1 + A,B,C) [B >= 6] (?,1) 10. f10(A,B,C) -> f21(1,B,C) [A >= 6] (?,1) Signature: {(f0,3);(f10,3);(f13,3);(f21,3);(f24,3);(f27,3);(f39,3)} Flow Graph: [0->{1},1->{2},2->{2,9},3->{4},4->{5},5->{5,6},6->{4,7},7->{3},9->{1,10},10->{3}] Sizebounds: (< 0,0,A>, 1) (< 0,0,B>, B) (< 0,0,C>, C) (< 1,0,A>, 5) (< 1,0,B>, 1) (< 1,0,C>, C) (< 2,0,A>, 5) (< 2,0,B>, 6) (< 2,0,C>, C) (< 3,0,A>, 5) (< 3,0,B>, 1) (< 3,0,C>, ?) (< 4,0,A>, ?) (< 4,0,B>, 5) (< 4,0,C>, 1) (< 5,0,A>, ?) (< 5,0,B>, 5) (< 5,0,C>, 6) (< 6,0,A>, ?) (< 6,0,B>, 5) (< 6,0,C>, 6) (< 7,0,A>, ?) (< 7,0,B>, 5) (< 7,0,C>, ?) (< 9,0,A>, 5) (< 9,0,B>, 6) (< 9,0,C>, C) (<10,0,A>, 1) (<10,0,B>, 6 + B) (<10,0,C>, C) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f0) = 1 p(f10) = 1 p(f13) = 1 p(f21) = 0 p(f24) = 0 p(f27) = 0 The following rules are strictly oriented: [A >= 6] ==> f10(A,B,C) = 1 > 0 = f21(1,B,C) The following rules are weakly oriented: True ==> f0(A,B,C) = 1 >= 1 = f10(1,B,C) [5 >= A] ==> f10(A,B,C) = 1 >= 1 = f13(A,1,C) [5 >= B] ==> f13(A,B,C) = 1 >= 1 = f13(A,1 + B,C) [5 >= A] ==> f21(A,B,C) = 0 >= 0 = f24(A,1,C) [5 >= B] ==> f24(A,B,C) = 0 >= 0 = f27(A,B,1) [5 >= C] ==> f27(A,B,C) = 0 >= 0 = f27(A,B,1 + C) [C >= 6] ==> f27(A,B,C) = 0 >= 0 = f24(A,1 + B,C) [B >= 6] ==> f24(A,B,C) = 0 >= 0 = f21(1 + A,B,C) [B >= 6] ==> f13(A,B,C) = 1 >= 1 = f10(1 + A,B,C) * Step 6: PolyRank WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f0(A,B,C) -> f10(1,B,C) True (1,1) 1. f10(A,B,C) -> f13(A,1,C) [5 >= A] (?,1) 2. f13(A,B,C) -> f13(A,1 + B,C) [5 >= B] (?,1) 3. f21(A,B,C) -> f24(A,1,C) [5 >= A] (?,1) 4. f24(A,B,C) -> f27(A,B,1) [5 >= B] (?,1) 5. f27(A,B,C) -> f27(A,B,1 + C) [5 >= C] (?,1) 6. f27(A,B,C) -> f24(A,1 + B,C) [C >= 6] (?,1) 7. f24(A,B,C) -> f21(1 + A,B,C) [B >= 6] (?,1) 9. f13(A,B,C) -> f10(1 + A,B,C) [B >= 6] (?,1) 10. f10(A,B,C) -> f21(1,B,C) [A >= 6] (1,1) Signature: {(f0,3);(f10,3);(f13,3);(f21,3);(f24,3);(f27,3);(f39,3)} Flow Graph: [0->{1},1->{2},2->{2,9},3->{4},4->{5},5->{5,6},6->{4,7},7->{3},9->{1,10},10->{3}] Sizebounds: (< 0,0,A>, 1) (< 0,0,B>, B) (< 0,0,C>, C) (< 1,0,A>, 5) (< 1,0,B>, 1) (< 1,0,C>, C) (< 2,0,A>, 5) (< 2,0,B>, 6) (< 2,0,C>, C) (< 3,0,A>, 5) (< 3,0,B>, 1) (< 3,0,C>, ?) (< 4,0,A>, ?) (< 4,0,B>, 5) (< 4,0,C>, 1) (< 5,0,A>, ?) (< 5,0,B>, 5) (< 5,0,C>, 6) (< 6,0,A>, ?) (< 6,0,B>, 5) (< 6,0,C>, 6) (< 7,0,A>, ?) (< 7,0,B>, 5) (< 7,0,C>, ?) (< 9,0,A>, 5) (< 9,0,B>, 6) (< 9,0,C>, C) (<10,0,A>, 1) (<10,0,B>, 6 + B) (<10,0,C>, C) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f0) = 5 p(f10) = 5 p(f13) = 5 p(f21) = 6 + -1*x1 p(f24) = 5 + -1*x1 p(f27) = 5 + -1*x1 The following rules are strictly oriented: [5 >= A] ==> f21(A,B,C) = 6 + -1*A > 5 + -1*A = f24(A,1,C) The following rules are weakly oriented: True ==> f0(A,B,C) = 5 >= 5 = f10(1,B,C) [5 >= A] ==> f10(A,B,C) = 5 >= 5 = f13(A,1,C) [5 >= B] ==> f13(A,B,C) = 5 >= 5 = f13(A,1 + B,C) [5 >= B] ==> f24(A,B,C) = 5 + -1*A >= 5 + -1*A = f27(A,B,1) [5 >= C] ==> f27(A,B,C) = 5 + -1*A >= 5 + -1*A = f27(A,B,1 + C) [C >= 6] ==> f27(A,B,C) = 5 + -1*A >= 5 + -1*A = f24(A,1 + B,C) [B >= 6] ==> f24(A,B,C) = 5 + -1*A >= 5 + -1*A = f21(1 + A,B,C) [B >= 6] ==> f13(A,B,C) = 5 >= 5 = f10(1 + A,B,C) [A >= 6] ==> f10(A,B,C) = 5 >= 5 = f21(1,B,C) * Step 7: PolyRank WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f0(A,B,C) -> f10(1,B,C) True (1,1) 1. f10(A,B,C) -> f13(A,1,C) [5 >= A] (?,1) 2. f13(A,B,C) -> f13(A,1 + B,C) [5 >= B] (?,1) 3. f21(A,B,C) -> f24(A,1,C) [5 >= A] (5,1) 4. f24(A,B,C) -> f27(A,B,1) [5 >= B] (?,1) 5. f27(A,B,C) -> f27(A,B,1 + C) [5 >= C] (?,1) 6. f27(A,B,C) -> f24(A,1 + B,C) [C >= 6] (?,1) 7. f24(A,B,C) -> f21(1 + A,B,C) [B >= 6] (?,1) 9. f13(A,B,C) -> f10(1 + A,B,C) [B >= 6] (?,1) 10. f10(A,B,C) -> f21(1,B,C) [A >= 6] (1,1) Signature: {(f0,3);(f10,3);(f13,3);(f21,3);(f24,3);(f27,3);(f39,3)} Flow Graph: [0->{1},1->{2},2->{2,9},3->{4},4->{5},5->{5,6},6->{4,7},7->{3},9->{1,10},10->{3}] Sizebounds: (< 0,0,A>, 1) (< 0,0,B>, B) (< 0,0,C>, C) (< 1,0,A>, 5) (< 1,0,B>, 1) (< 1,0,C>, C) (< 2,0,A>, 5) (< 2,0,B>, 6) (< 2,0,C>, C) (< 3,0,A>, 5) (< 3,0,B>, 1) (< 3,0,C>, ?) (< 4,0,A>, ?) (< 4,0,B>, 5) (< 4,0,C>, 1) (< 5,0,A>, ?) (< 5,0,B>, 5) (< 5,0,C>, 6) (< 6,0,A>, ?) (< 6,0,B>, 5) (< 6,0,C>, 6) (< 7,0,A>, ?) (< 7,0,B>, 5) (< 7,0,C>, ?) (< 9,0,A>, 5) (< 9,0,B>, 6) (< 9,0,C>, C) (<10,0,A>, 1) (<10,0,B>, 6 + B) (<10,0,C>, C) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [1,9,2], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f10) = 6 + -1*x1 p(f13) = 5 + -1*x1 The following rules are strictly oriented: [5 >= A] ==> f10(A,B,C) = 6 + -1*A > 5 + -1*A = f13(A,1,C) The following rules are weakly oriented: [5 >= B] ==> f13(A,B,C) = 5 + -1*A >= 5 + -1*A = f13(A,1 + B,C) [B >= 6] ==> f13(A,B,C) = 5 + -1*A >= 5 + -1*A = f10(1 + A,B,C) We use the following global sizebounds: (< 0,0,A>, 1) (< 0,0,B>, B) (< 0,0,C>, C) (< 1,0,A>, 5) (< 1,0,B>, 1) (< 1,0,C>, C) (< 2,0,A>, 5) (< 2,0,B>, 6) (< 2,0,C>, C) (< 3,0,A>, 5) (< 3,0,B>, 1) (< 3,0,C>, ?) (< 4,0,A>, ?) (< 4,0,B>, 5) (< 4,0,C>, 1) (< 5,0,A>, ?) (< 5,0,B>, 5) (< 5,0,C>, 6) (< 6,0,A>, ?) (< 6,0,B>, 5) (< 6,0,C>, 6) (< 7,0,A>, ?) (< 7,0,B>, 5) (< 7,0,C>, ?) (< 9,0,A>, 5) (< 9,0,B>, 6) (< 9,0,C>, C) (<10,0,A>, 1) (<10,0,B>, 6 + B) (<10,0,C>, C) * Step 8: PolyRank WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f0(A,B,C) -> f10(1,B,C) True (1,1) 1. f10(A,B,C) -> f13(A,1,C) [5 >= A] (7,1) 2. f13(A,B,C) -> f13(A,1 + B,C) [5 >= B] (?,1) 3. f21(A,B,C) -> f24(A,1,C) [5 >= A] (5,1) 4. f24(A,B,C) -> f27(A,B,1) [5 >= B] (?,1) 5. f27(A,B,C) -> f27(A,B,1 + C) [5 >= C] (?,1) 6. f27(A,B,C) -> f24(A,1 + B,C) [C >= 6] (?,1) 7. f24(A,B,C) -> f21(1 + A,B,C) [B >= 6] (?,1) 9. f13(A,B,C) -> f10(1 + A,B,C) [B >= 6] (?,1) 10. f10(A,B,C) -> f21(1,B,C) [A >= 6] (1,1) Signature: {(f0,3);(f10,3);(f13,3);(f21,3);(f24,3);(f27,3);(f39,3)} Flow Graph: [0->{1},1->{2},2->{2,9},3->{4},4->{5},5->{5,6},6->{4,7},7->{3},9->{1,10},10->{3}] Sizebounds: (< 0,0,A>, 1) (< 0,0,B>, B) (< 0,0,C>, C) (< 1,0,A>, 5) (< 1,0,B>, 1) (< 1,0,C>, C) (< 2,0,A>, 5) (< 2,0,B>, 6) (< 2,0,C>, C) (< 3,0,A>, 5) (< 3,0,B>, 1) (< 3,0,C>, ?) (< 4,0,A>, ?) (< 4,0,B>, 5) (< 4,0,C>, 1) (< 5,0,A>, ?) (< 5,0,B>, 5) (< 5,0,C>, 6) (< 6,0,A>, ?) (< 6,0,B>, 5) (< 6,0,C>, 6) (< 7,0,A>, ?) (< 7,0,B>, 5) (< 7,0,C>, ?) (< 9,0,A>, 5) (< 9,0,B>, 6) (< 9,0,C>, C) (<10,0,A>, 1) (<10,0,B>, 6 + B) (<10,0,C>, C) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [2], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f13) = 6 + -1*x2 The following rules are strictly oriented: [5 >= B] ==> f13(A,B,C) = 6 + -1*B > 5 + -1*B = f13(A,1 + B,C) The following rules are weakly oriented: We use the following global sizebounds: (< 0,0,A>, 1) (< 0,0,B>, B) (< 0,0,C>, C) (< 1,0,A>, 5) (< 1,0,B>, 1) (< 1,0,C>, C) (< 2,0,A>, 5) (< 2,0,B>, 6) (< 2,0,C>, C) (< 3,0,A>, 5) (< 3,0,B>, 1) (< 3,0,C>, ?) (< 4,0,A>, ?) (< 4,0,B>, 5) (< 4,0,C>, 1) (< 5,0,A>, ?) (< 5,0,B>, 5) (< 5,0,C>, 6) (< 6,0,A>, ?) (< 6,0,B>, 5) (< 6,0,C>, 6) (< 7,0,A>, ?) (< 7,0,B>, 5) (< 7,0,C>, ?) (< 9,0,A>, 5) (< 9,0,B>, 6) (< 9,0,C>, C) (<10,0,A>, 1) (<10,0,B>, 6 + B) (<10,0,C>, C) * Step 9: KnowledgePropagation WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f0(A,B,C) -> f10(1,B,C) True (1,1) 1. f10(A,B,C) -> f13(A,1,C) [5 >= A] (7,1) 2. f13(A,B,C) -> f13(A,1 + B,C) [5 >= B] (49,1) 3. f21(A,B,C) -> f24(A,1,C) [5 >= A] (5,1) 4. f24(A,B,C) -> f27(A,B,1) [5 >= B] (?,1) 5. f27(A,B,C) -> f27(A,B,1 + C) [5 >= C] (?,1) 6. f27(A,B,C) -> f24(A,1 + B,C) [C >= 6] (?,1) 7. f24(A,B,C) -> f21(1 + A,B,C) [B >= 6] (?,1) 9. f13(A,B,C) -> f10(1 + A,B,C) [B >= 6] (?,1) 10. f10(A,B,C) -> f21(1,B,C) [A >= 6] (1,1) Signature: {(f0,3);(f10,3);(f13,3);(f21,3);(f24,3);(f27,3);(f39,3)} Flow Graph: [0->{1},1->{2},2->{2,9},3->{4},4->{5},5->{5,6},6->{4,7},7->{3},9->{1,10},10->{3}] Sizebounds: (< 0,0,A>, 1) (< 0,0,B>, B) (< 0,0,C>, C) (< 1,0,A>, 5) (< 1,0,B>, 1) (< 1,0,C>, C) (< 2,0,A>, 5) (< 2,0,B>, 6) (< 2,0,C>, C) (< 3,0,A>, 5) (< 3,0,B>, 1) (< 3,0,C>, ?) (< 4,0,A>, ?) (< 4,0,B>, 5) (< 4,0,C>, 1) (< 5,0,A>, ?) (< 5,0,B>, 5) (< 5,0,C>, 6) (< 6,0,A>, ?) (< 6,0,B>, 5) (< 6,0,C>, 6) (< 7,0,A>, ?) (< 7,0,B>, 5) (< 7,0,C>, ?) (< 9,0,A>, 5) (< 9,0,B>, 6) (< 9,0,C>, C) (<10,0,A>, 1) (<10,0,B>, 6 + B) (<10,0,C>, C) + Applied Processor: KnowledgePropagation + Details: We propagate bounds from predecessors. * Step 10: PolyRank WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f0(A,B,C) -> f10(1,B,C) True (1,1) 1. f10(A,B,C) -> f13(A,1,C) [5 >= A] (7,1) 2. f13(A,B,C) -> f13(A,1 + B,C) [5 >= B] (49,1) 3. f21(A,B,C) -> f24(A,1,C) [5 >= A] (5,1) 4. f24(A,B,C) -> f27(A,B,1) [5 >= B] (?,1) 5. f27(A,B,C) -> f27(A,B,1 + C) [5 >= C] (?,1) 6. f27(A,B,C) -> f24(A,1 + B,C) [C >= 6] (?,1) 7. f24(A,B,C) -> f21(1 + A,B,C) [B >= 6] (?,1) 9. f13(A,B,C) -> f10(1 + A,B,C) [B >= 6] (49,1) 10. f10(A,B,C) -> f21(1,B,C) [A >= 6] (1,1) Signature: {(f0,3);(f10,3);(f13,3);(f21,3);(f24,3);(f27,3);(f39,3)} Flow Graph: [0->{1},1->{2},2->{2,9},3->{4},4->{5},5->{5,6},6->{4,7},7->{3},9->{1,10},10->{3}] Sizebounds: (< 0,0,A>, 1) (< 0,0,B>, B) (< 0,0,C>, C) (< 1,0,A>, 5) (< 1,0,B>, 1) (< 1,0,C>, C) (< 2,0,A>, 5) (< 2,0,B>, 6) (< 2,0,C>, C) (< 3,0,A>, 5) (< 3,0,B>, 1) (< 3,0,C>, ?) (< 4,0,A>, ?) (< 4,0,B>, 5) (< 4,0,C>, 1) (< 5,0,A>, ?) (< 5,0,B>, 5) (< 5,0,C>, 6) (< 6,0,A>, ?) (< 6,0,B>, 5) (< 6,0,C>, 6) (< 7,0,A>, ?) (< 7,0,B>, 5) (< 7,0,C>, ?) (< 9,0,A>, 5) (< 9,0,B>, 6) (< 9,0,C>, C) (<10,0,A>, 1) (<10,0,B>, 6 + B) (<10,0,C>, C) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [7,6,5,4], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f21) = 0 p(f24) = 1 p(f27) = 1 The following rules are strictly oriented: [B >= 6] ==> f24(A,B,C) = 1 > 0 = f21(1 + A,B,C) The following rules are weakly oriented: [5 >= B] ==> f24(A,B,C) = 1 >= 1 = f27(A,B,1) [5 >= C] ==> f27(A,B,C) = 1 >= 1 = f27(A,B,1 + C) [C >= 6] ==> f27(A,B,C) = 1 >= 1 = f24(A,1 + B,C) We use the following global sizebounds: (< 0,0,A>, 1) (< 0,0,B>, B) (< 0,0,C>, C) (< 1,0,A>, 5) (< 1,0,B>, 1) (< 1,0,C>, C) (< 2,0,A>, 5) (< 2,0,B>, 6) (< 2,0,C>, C) (< 3,0,A>, 5) (< 3,0,B>, 1) (< 3,0,C>, ?) (< 4,0,A>, ?) (< 4,0,B>, 5) (< 4,0,C>, 1) (< 5,0,A>, ?) (< 5,0,B>, 5) (< 5,0,C>, 6) (< 6,0,A>, ?) (< 6,0,B>, 5) (< 6,0,C>, 6) (< 7,0,A>, ?) (< 7,0,B>, 5) (< 7,0,C>, ?) (< 9,0,A>, 5) (< 9,0,B>, 6) (< 9,0,C>, C) (<10,0,A>, 1) (<10,0,B>, 6 + B) (<10,0,C>, C) * Step 11: PolyRank WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f0(A,B,C) -> f10(1,B,C) True (1,1) 1. f10(A,B,C) -> f13(A,1,C) [5 >= A] (7,1) 2. f13(A,B,C) -> f13(A,1 + B,C) [5 >= B] (49,1) 3. f21(A,B,C) -> f24(A,1,C) [5 >= A] (5,1) 4. f24(A,B,C) -> f27(A,B,1) [5 >= B] (?,1) 5. f27(A,B,C) -> f27(A,B,1 + C) [5 >= C] (?,1) 6. f27(A,B,C) -> f24(A,1 + B,C) [C >= 6] (?,1) 7. f24(A,B,C) -> f21(1 + A,B,C) [B >= 6] (5,1) 9. f13(A,B,C) -> f10(1 + A,B,C) [B >= 6] (49,1) 10. f10(A,B,C) -> f21(1,B,C) [A >= 6] (1,1) Signature: {(f0,3);(f10,3);(f13,3);(f21,3);(f24,3);(f27,3);(f39,3)} Flow Graph: [0->{1},1->{2},2->{2,9},3->{4},4->{5},5->{5,6},6->{4,7},7->{3},9->{1,10},10->{3}] Sizebounds: (< 0,0,A>, 1) (< 0,0,B>, B) (< 0,0,C>, C) (< 1,0,A>, 5) (< 1,0,B>, 1) (< 1,0,C>, C) (< 2,0,A>, 5) (< 2,0,B>, 6) (< 2,0,C>, C) (< 3,0,A>, 5) (< 3,0,B>, 1) (< 3,0,C>, ?) (< 4,0,A>, ?) (< 4,0,B>, 5) (< 4,0,C>, 1) (< 5,0,A>, ?) (< 5,0,B>, 5) (< 5,0,C>, 6) (< 6,0,A>, ?) (< 6,0,B>, 5) (< 6,0,C>, 6) (< 7,0,A>, ?) (< 7,0,B>, 5) (< 7,0,C>, ?) (< 9,0,A>, 5) (< 9,0,B>, 6) (< 9,0,C>, C) (<10,0,A>, 1) (<10,0,B>, 6 + B) (<10,0,C>, C) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [7,6,5,4], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f21) = 6 + -1*x2 p(f24) = 6 + -1*x2 p(f27) = 5 + -1*x2 The following rules are strictly oriented: [5 >= B] ==> f24(A,B,C) = 6 + -1*B > 5 + -1*B = f27(A,B,1) The following rules are weakly oriented: [5 >= C] ==> f27(A,B,C) = 5 + -1*B >= 5 + -1*B = f27(A,B,1 + C) [C >= 6] ==> f27(A,B,C) = 5 + -1*B >= 5 + -1*B = f24(A,1 + B,C) [B >= 6] ==> f24(A,B,C) = 6 + -1*B >= 6 + -1*B = f21(1 + A,B,C) We use the following global sizebounds: (< 0,0,A>, 1) (< 0,0,B>, B) (< 0,0,C>, C) (< 1,0,A>, 5) (< 1,0,B>, 1) (< 1,0,C>, C) (< 2,0,A>, 5) (< 2,0,B>, 6) (< 2,0,C>, C) (< 3,0,A>, 5) (< 3,0,B>, 1) (< 3,0,C>, ?) (< 4,0,A>, ?) (< 4,0,B>, 5) (< 4,0,C>, 1) (< 5,0,A>, ?) (< 5,0,B>, 5) (< 5,0,C>, 6) (< 6,0,A>, ?) (< 6,0,B>, 5) (< 6,0,C>, 6) (< 7,0,A>, ?) (< 7,0,B>, 5) (< 7,0,C>, ?) (< 9,0,A>, 5) (< 9,0,B>, 6) (< 9,0,C>, C) (<10,0,A>, 1) (<10,0,B>, 6 + B) (<10,0,C>, C) * Step 12: PolyRank WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f0(A,B,C) -> f10(1,B,C) True (1,1) 1. f10(A,B,C) -> f13(A,1,C) [5 >= A] (7,1) 2. f13(A,B,C) -> f13(A,1 + B,C) [5 >= B] (49,1) 3. f21(A,B,C) -> f24(A,1,C) [5 >= A] (5,1) 4. f24(A,B,C) -> f27(A,B,1) [5 >= B] (35,1) 5. f27(A,B,C) -> f27(A,B,1 + C) [5 >= C] (?,1) 6. f27(A,B,C) -> f24(A,1 + B,C) [C >= 6] (?,1) 7. f24(A,B,C) -> f21(1 + A,B,C) [B >= 6] (5,1) 9. f13(A,B,C) -> f10(1 + A,B,C) [B >= 6] (49,1) 10. f10(A,B,C) -> f21(1,B,C) [A >= 6] (1,1) Signature: {(f0,3);(f10,3);(f13,3);(f21,3);(f24,3);(f27,3);(f39,3)} Flow Graph: [0->{1},1->{2},2->{2,9},3->{4},4->{5},5->{5,6},6->{4,7},7->{3},9->{1,10},10->{3}] Sizebounds: (< 0,0,A>, 1) (< 0,0,B>, B) (< 0,0,C>, C) (< 1,0,A>, 5) (< 1,0,B>, 1) (< 1,0,C>, C) (< 2,0,A>, 5) (< 2,0,B>, 6) (< 2,0,C>, C) (< 3,0,A>, 5) (< 3,0,B>, 1) (< 3,0,C>, ?) (< 4,0,A>, ?) (< 4,0,B>, 5) (< 4,0,C>, 1) (< 5,0,A>, ?) (< 5,0,B>, 5) (< 5,0,C>, 6) (< 6,0,A>, ?) (< 6,0,B>, 5) (< 6,0,C>, 6) (< 7,0,A>, ?) (< 7,0,B>, 5) (< 7,0,C>, ?) (< 9,0,A>, 5) (< 9,0,B>, 6) (< 9,0,C>, C) (<10,0,A>, 1) (<10,0,B>, 6 + B) (<10,0,C>, C) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [3,7,6,5], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f21) = 0 p(f24) = 0 p(f27) = 1 The following rules are strictly oriented: [C >= 6] ==> f27(A,B,C) = 1 > 0 = f24(A,1 + B,C) The following rules are weakly oriented: [5 >= A] ==> f21(A,B,C) = 0 >= 0 = f24(A,1,C) [5 >= C] ==> f27(A,B,C) = 1 >= 1 = f27(A,B,1 + C) [B >= 6] ==> f24(A,B,C) = 0 >= 0 = f21(1 + A,B,C) We use the following global sizebounds: (< 0,0,A>, 1) (< 0,0,B>, B) (< 0,0,C>, C) (< 1,0,A>, 5) (< 1,0,B>, 1) (< 1,0,C>, C) (< 2,0,A>, 5) (< 2,0,B>, 6) (< 2,0,C>, C) (< 3,0,A>, 5) (< 3,0,B>, 1) (< 3,0,C>, ?) (< 4,0,A>, ?) (< 4,0,B>, 5) (< 4,0,C>, 1) (< 5,0,A>, ?) (< 5,0,B>, 5) (< 5,0,C>, 6) (< 6,0,A>, ?) (< 6,0,B>, 5) (< 6,0,C>, 6) (< 7,0,A>, ?) (< 7,0,B>, 5) (< 7,0,C>, ?) (< 9,0,A>, 5) (< 9,0,B>, 6) (< 9,0,C>, C) (<10,0,A>, 1) (<10,0,B>, 6 + B) (<10,0,C>, C) * Step 13: PolyRank WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f0(A,B,C) -> f10(1,B,C) True (1,1) 1. f10(A,B,C) -> f13(A,1,C) [5 >= A] (7,1) 2. f13(A,B,C) -> f13(A,1 + B,C) [5 >= B] (49,1) 3. f21(A,B,C) -> f24(A,1,C) [5 >= A] (5,1) 4. f24(A,B,C) -> f27(A,B,1) [5 >= B] (35,1) 5. f27(A,B,C) -> f27(A,B,1 + C) [5 >= C] (?,1) 6. f27(A,B,C) -> f24(A,1 + B,C) [C >= 6] (35,1) 7. f24(A,B,C) -> f21(1 + A,B,C) [B >= 6] (5,1) 9. f13(A,B,C) -> f10(1 + A,B,C) [B >= 6] (49,1) 10. f10(A,B,C) -> f21(1,B,C) [A >= 6] (1,1) Signature: {(f0,3);(f10,3);(f13,3);(f21,3);(f24,3);(f27,3);(f39,3)} Flow Graph: [0->{1},1->{2},2->{2,9},3->{4},4->{5},5->{5,6},6->{4,7},7->{3},9->{1,10},10->{3}] Sizebounds: (< 0,0,A>, 1) (< 0,0,B>, B) (< 0,0,C>, C) (< 1,0,A>, 5) (< 1,0,B>, 1) (< 1,0,C>, C) (< 2,0,A>, 5) (< 2,0,B>, 6) (< 2,0,C>, C) (< 3,0,A>, 5) (< 3,0,B>, 1) (< 3,0,C>, ?) (< 4,0,A>, ?) (< 4,0,B>, 5) (< 4,0,C>, 1) (< 5,0,A>, ?) (< 5,0,B>, 5) (< 5,0,C>, 6) (< 6,0,A>, ?) (< 6,0,B>, 5) (< 6,0,C>, 6) (< 7,0,A>, ?) (< 7,0,B>, 5) (< 7,0,C>, ?) (< 9,0,A>, 5) (< 9,0,B>, 6) (< 9,0,C>, C) (<10,0,A>, 1) (<10,0,B>, 6 + B) (<10,0,C>, C) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [7,5,4], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f21) = 5 p(f24) = 5 p(f27) = 6 + -1*x3 The following rules are strictly oriented: [5 >= C] ==> f27(A,B,C) = 6 + -1*C > 5 + -1*C = f27(A,B,1 + C) The following rules are weakly oriented: [5 >= B] ==> f24(A,B,C) = 5 >= 5 = f27(A,B,1) [B >= 6] ==> f24(A,B,C) = 5 >= 5 = f21(1 + A,B,C) We use the following global sizebounds: (< 0,0,A>, 1) (< 0,0,B>, B) (< 0,0,C>, C) (< 1,0,A>, 5) (< 1,0,B>, 1) (< 1,0,C>, C) (< 2,0,A>, 5) (< 2,0,B>, 6) (< 2,0,C>, C) (< 3,0,A>, 5) (< 3,0,B>, 1) (< 3,0,C>, ?) (< 4,0,A>, ?) (< 4,0,B>, 5) (< 4,0,C>, 1) (< 5,0,A>, ?) (< 5,0,B>, 5) (< 5,0,C>, 6) (< 6,0,A>, ?) (< 6,0,B>, 5) (< 6,0,C>, 6) (< 7,0,A>, ?) (< 7,0,B>, 5) (< 7,0,C>, ?) (< 9,0,A>, 5) (< 9,0,B>, 6) (< 9,0,C>, C) (<10,0,A>, 1) (<10,0,B>, 6 + B) (<10,0,C>, C) * Step 14: KnowledgePropagation WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f0(A,B,C) -> f10(1,B,C) True (1,1) 1. f10(A,B,C) -> f13(A,1,C) [5 >= A] (7,1) 2. f13(A,B,C) -> f13(A,1 + B,C) [5 >= B] (49,1) 3. f21(A,B,C) -> f24(A,1,C) [5 >= A] (5,1) 4. f24(A,B,C) -> f27(A,B,1) [5 >= B] (35,1) 5. f27(A,B,C) -> f27(A,B,1 + C) [5 >= C] (200,1) 6. f27(A,B,C) -> f24(A,1 + B,C) [C >= 6] (35,1) 7. f24(A,B,C) -> f21(1 + A,B,C) [B >= 6] (5,1) 9. f13(A,B,C) -> f10(1 + A,B,C) [B >= 6] (49,1) 10. f10(A,B,C) -> f21(1,B,C) [A >= 6] (1,1) Signature: {(f0,3);(f10,3);(f13,3);(f21,3);(f24,3);(f27,3);(f39,3)} Flow Graph: [0->{1},1->{2},2->{2,9},3->{4},4->{5},5->{5,6},6->{4,7},7->{3},9->{1,10},10->{3}] Sizebounds: (< 0,0,A>, 1) (< 0,0,B>, B) (< 0,0,C>, C) (< 1,0,A>, 5) (< 1,0,B>, 1) (< 1,0,C>, C) (< 2,0,A>, 5) (< 2,0,B>, 6) (< 2,0,C>, C) (< 3,0,A>, 5) (< 3,0,B>, 1) (< 3,0,C>, ?) (< 4,0,A>, ?) (< 4,0,B>, 5) (< 4,0,C>, 1) (< 5,0,A>, ?) (< 5,0,B>, 5) (< 5,0,C>, 6) (< 6,0,A>, ?) (< 6,0,B>, 5) (< 6,0,C>, 6) (< 7,0,A>, ?) (< 7,0,B>, 5) (< 7,0,C>, ?) (< 9,0,A>, 5) (< 9,0,B>, 6) (< 9,0,C>, C) (<10,0,A>, 1) (<10,0,B>, 6 + B) (<10,0,C>, C) + Applied Processor: KnowledgePropagation + Details: The problem is already solved. WORST_CASE(?,O(1))