YES(?,O(1)) * Step 1: TrivialSCCs WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f0(A,B,C) -> f8(0,B,C) True (1,1) 1. f8(A,B,C) -> f14(A,A,C) [A >= 0 && 0 >= A && 0 >= D] (?,1) 2. f8(A,B,C) -> f14(A,A,C) [A >= 0 && 0 >= A] (?,1) 3. f23(A,B,C) -> f28(A,B,D) [A >= 0 && 0 >= A && 0 >= 1 + E] (?,1) 4. f23(A,B,C) -> f28(A,B,D) [A >= 0 && 0 >= A] (?,1) 5. f23(A,B,C) -> f23(1 + A,B,C) [A >= 0 && 0 >= A] (?,1) 6. f28(A,B,C) -> f23(1 + A,B,C) [-1*A >= 0 && A >= 0] (?,1) 7. f28(A,B,C) -> f23(1 + A,B,C) [-1*A >= 0 && A >= 0 && 0 >= 1 + D] (?,1) 8. f23(A,B,C) -> f38(A,B,C) [A >= 0 && A >= 1] (?,1) 9. f8(A,B,C) -> f8(1 + A,A,C) [A >= 0 && 0 >= A] (?,1) 10. f14(A,B,C) -> f8(1 + A,B,C) [-1*B >= 0 (?,1) && A + -1*B >= 0 && -1*A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && -1*A >= 0 && A >= 0] 11. f14(A,B,C) -> f8(1 + A,B,C) [-1*B >= 0 (?,1) && A + -1*B >= 0 && -1*A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && -1*A >= 0 && A >= 0 && 0 >= 1 + D] 12. f8(A,B,C) -> f23(0,B,C) [A >= 0 && A >= 1] (?,1) Signature: {(f0,3);(f14,3);(f23,3);(f28,3);(f38,3);(f8,3)} Flow Graph: [0->{1,2,9,12},1->{10,11},2->{10,11},3->{6,7},4->{6,7},5->{3,4,5,8},6->{3,4,5,8},7->{3,4,5,8},8->{},9->{1 ,2,9,12},10->{1,2,9,12},11->{1,2,9,12},12->{3,4,5,8}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatPaths WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f0(A,B,C) -> f8(0,B,C) True (1,1) 1. f8(A,B,C) -> f14(A,A,C) [A >= 0 && 0 >= A && 0 >= D] (?,1) 2. f8(A,B,C) -> f14(A,A,C) [A >= 0 && 0 >= A] (?,1) 3. f23(A,B,C) -> f28(A,B,D) [A >= 0 && 0 >= A && 0 >= 1 + E] (?,1) 4. f23(A,B,C) -> f28(A,B,D) [A >= 0 && 0 >= A] (?,1) 5. f23(A,B,C) -> f23(1 + A,B,C) [A >= 0 && 0 >= A] (?,1) 6. f28(A,B,C) -> f23(1 + A,B,C) [-1*A >= 0 && A >= 0] (?,1) 7. f28(A,B,C) -> f23(1 + A,B,C) [-1*A >= 0 && A >= 0 && 0 >= 1 + D] (?,1) 8. f23(A,B,C) -> f38(A,B,C) [A >= 0 && A >= 1] (1,1) 9. f8(A,B,C) -> f8(1 + A,A,C) [A >= 0 && 0 >= A] (?,1) 10. f14(A,B,C) -> f8(1 + A,B,C) [-1*B >= 0 (?,1) && A + -1*B >= 0 && -1*A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && -1*A >= 0 && A >= 0] 11. f14(A,B,C) -> f8(1 + A,B,C) [-1*B >= 0 (?,1) && A + -1*B >= 0 && -1*A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && -1*A >= 0 && A >= 0 && 0 >= 1 + D] 12. f8(A,B,C) -> f23(0,B,C) [A >= 0 && A >= 1] (1,1) Signature: {(f0,3);(f14,3);(f23,3);(f28,3);(f38,3);(f8,3)} Flow Graph: [0->{1,2,9,12},1->{10,11},2->{10,11},3->{6,7},4->{6,7},5->{3,4,5,8},6->{3,4,5,8},7->{3,4,5,8},8->{},9->{1 ,2,9,12},10->{1,2,9,12},11->{1,2,9,12},12->{3,4,5,8}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(0,12) ,(5,3) ,(5,4) ,(5,5) ,(6,3) ,(6,4) ,(6,5) ,(7,3) ,(7,4) ,(7,5) ,(9,1) ,(9,2) ,(9,9) ,(10,1) ,(10,2) ,(10,9) ,(11,1) ,(11,2) ,(11,9) ,(12,8)] * Step 3: PolyRank WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f0(A,B,C) -> f8(0,B,C) True (1,1) 1. f8(A,B,C) -> f14(A,A,C) [A >= 0 && 0 >= A && 0 >= D] (?,1) 2. f8(A,B,C) -> f14(A,A,C) [A >= 0 && 0 >= A] (?,1) 3. f23(A,B,C) -> f28(A,B,D) [A >= 0 && 0 >= A && 0 >= 1 + E] (?,1) 4. f23(A,B,C) -> f28(A,B,D) [A >= 0 && 0 >= A] (?,1) 5. f23(A,B,C) -> f23(1 + A,B,C) [A >= 0 && 0 >= A] (?,1) 6. f28(A,B,C) -> f23(1 + A,B,C) [-1*A >= 0 && A >= 0] (?,1) 7. f28(A,B,C) -> f23(1 + A,B,C) [-1*A >= 0 && A >= 0 && 0 >= 1 + D] (?,1) 8. f23(A,B,C) -> f38(A,B,C) [A >= 0 && A >= 1] (1,1) 9. f8(A,B,C) -> f8(1 + A,A,C) [A >= 0 && 0 >= A] (?,1) 10. f14(A,B,C) -> f8(1 + A,B,C) [-1*B >= 0 (?,1) && A + -1*B >= 0 && -1*A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && -1*A >= 0 && A >= 0] 11. f14(A,B,C) -> f8(1 + A,B,C) [-1*B >= 0 (?,1) && A + -1*B >= 0 && -1*A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && -1*A >= 0 && A >= 0 && 0 >= 1 + D] 12. f8(A,B,C) -> f23(0,B,C) [A >= 0 && A >= 1] (1,1) Signature: {(f0,3);(f14,3);(f23,3);(f28,3);(f38,3);(f8,3)} Flow Graph: [0->{1,2,9},1->{10,11},2->{10,11},3->{6,7},4->{6,7},5->{8},6->{8},7->{8},8->{},9->{12},10->{12},11->{12} ,12->{3,4,5}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f0) = 1 p(f14) = 1 p(f23) = 1 + -1*x1 p(f28) = 1 + -1*x1 p(f38) = 1 + -1*x1 p(f8) = 1 Following rules are strictly oriented: [-1*A >= 0 && A >= 0 && 0 >= 1 + D] ==> f28(A,B,C) = 1 + -1*A > -1*A = f23(1 + A,B,C) Following rules are weakly oriented: True ==> f0(A,B,C) = 1 >= 1 = f8(0,B,C) [A >= 0 && 0 >= A && 0 >= D] ==> f8(A,B,C) = 1 >= 1 = f14(A,A,C) [A >= 0 && 0 >= A] ==> f8(A,B,C) = 1 >= 1 = f14(A,A,C) [A >= 0 && 0 >= A && 0 >= 1 + E] ==> f23(A,B,C) = 1 + -1*A >= 1 + -1*A = f28(A,B,D) [A >= 0 && 0 >= A] ==> f23(A,B,C) = 1 + -1*A >= 1 + -1*A = f28(A,B,D) [A >= 0 && 0 >= A] ==> f23(A,B,C) = 1 + -1*A >= -1*A = f23(1 + A,B,C) [-1*A >= 0 && A >= 0] ==> f28(A,B,C) = 1 + -1*A >= -1*A = f23(1 + A,B,C) [A >= 0 && A >= 1] ==> f23(A,B,C) = 1 + -1*A >= 1 + -1*A = f38(A,B,C) [A >= 0 && 0 >= A] ==> f8(A,B,C) = 1 >= 1 = f8(1 + A,A,C) [-1*B >= 0 ==> && A + -1*B >= 0 && -1*A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && -1*A >= 0 && A >= 0] f14(A,B,C) = 1 >= 1 = f8(1 + A,B,C) [-1*B >= 0 ==> && A + -1*B >= 0 && -1*A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && -1*A >= 0 && A >= 0 && 0 >= 1 + D] f14(A,B,C) = 1 >= 1 = f8(1 + A,B,C) [A >= 0 && A >= 1] ==> f8(A,B,C) = 1 >= 1 = f23(0,B,C) * Step 4: KnowledgePropagation WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f0(A,B,C) -> f8(0,B,C) True (1,1) 1. f8(A,B,C) -> f14(A,A,C) [A >= 0 && 0 >= A && 0 >= D] (?,1) 2. f8(A,B,C) -> f14(A,A,C) [A >= 0 && 0 >= A] (?,1) 3. f23(A,B,C) -> f28(A,B,D) [A >= 0 && 0 >= A && 0 >= 1 + E] (?,1) 4. f23(A,B,C) -> f28(A,B,D) [A >= 0 && 0 >= A] (?,1) 5. f23(A,B,C) -> f23(1 + A,B,C) [A >= 0 && 0 >= A] (?,1) 6. f28(A,B,C) -> f23(1 + A,B,C) [-1*A >= 0 && A >= 0] (?,1) 7. f28(A,B,C) -> f23(1 + A,B,C) [-1*A >= 0 && A >= 0 && 0 >= 1 + D] (1,1) 8. f23(A,B,C) -> f38(A,B,C) [A >= 0 && A >= 1] (1,1) 9. f8(A,B,C) -> f8(1 + A,A,C) [A >= 0 && 0 >= A] (?,1) 10. f14(A,B,C) -> f8(1 + A,B,C) [-1*B >= 0 (?,1) && A + -1*B >= 0 && -1*A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && -1*A >= 0 && A >= 0] 11. f14(A,B,C) -> f8(1 + A,B,C) [-1*B >= 0 (?,1) && A + -1*B >= 0 && -1*A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && -1*A >= 0 && A >= 0 && 0 >= 1 + D] 12. f8(A,B,C) -> f23(0,B,C) [A >= 0 && A >= 1] (1,1) Signature: {(f0,3);(f14,3);(f23,3);(f28,3);(f38,3);(f8,3)} Flow Graph: [0->{1,2,9},1->{10,11},2->{10,11},3->{6,7},4->{6,7},5->{8},6->{8},7->{8},8->{},9->{12},10->{12},11->{12} ,12->{3,4,5}] + Applied Processor: KnowledgePropagation + Details: We propagate bounds from predecessors. * Step 5: PolyRank WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f0(A,B,C) -> f8(0,B,C) True (1,1) 1. f8(A,B,C) -> f14(A,A,C) [A >= 0 && 0 >= A && 0 >= D] (1,1) 2. f8(A,B,C) -> f14(A,A,C) [A >= 0 && 0 >= A] (1,1) 3. f23(A,B,C) -> f28(A,B,D) [A >= 0 && 0 >= A && 0 >= 1 + E] (1,1) 4. f23(A,B,C) -> f28(A,B,D) [A >= 0 && 0 >= A] (1,1) 5. f23(A,B,C) -> f23(1 + A,B,C) [A >= 0 && 0 >= A] (1,1) 6. f28(A,B,C) -> f23(1 + A,B,C) [-1*A >= 0 && A >= 0] (2,1) 7. f28(A,B,C) -> f23(1 + A,B,C) [-1*A >= 0 && A >= 0 && 0 >= 1 + D] (1,1) 8. f23(A,B,C) -> f38(A,B,C) [A >= 0 && A >= 1] (1,1) 9. f8(A,B,C) -> f8(1 + A,A,C) [A >= 0 && 0 >= A] (1,1) 10. f14(A,B,C) -> f8(1 + A,B,C) [-1*B >= 0 (2,1) && A + -1*B >= 0 && -1*A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && -1*A >= 0 && A >= 0] 11. f14(A,B,C) -> f8(1 + A,B,C) [-1*B >= 0 (2,1) && A + -1*B >= 0 && -1*A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && -1*A >= 0 && A >= 0 && 0 >= 1 + D] 12. f8(A,B,C) -> f23(0,B,C) [A >= 0 && A >= 1] (1,1) Signature: {(f0,3);(f14,3);(f23,3);(f28,3);(f38,3);(f8,3)} Flow Graph: [0->{1,2,9},1->{10,11},2->{10,11},3->{6,7},4->{6,7},5->{8},6->{8},7->{8},8->{},9->{12},10->{12},11->{12} ,12->{3,4,5}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: The problem is already solved. YES(?,O(1))