YES(?,O(1)) * Step 1: UnsatPaths WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f12(A,B,C,D,E,F) -> f5(4,0,0,D,E,F) True (1,1) 1. f5(A,B,C,D,E,F) -> f5(A,1 + B,G,H,E,G) [B >= 0 && -4 + A + B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && -4 + A >= 0 && A >= 1 + B && C = 0] (?,1) 2. f5(A,B,C,D,E,F) -> f10(A,B,C,C,C,F) [B >= 0 && -4 + A + B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && -4 + A >= 0 && 0 >= 1 + C] (?,1) 3. f5(A,B,C,D,E,F) -> f10(A,B,C,C,C,F) [B >= 0 && -4 + A + B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && -4 + A >= 0 && C >= 1] (?,1) 4. f5(A,B,C,D,E,F) -> f11(A,B,0,0,0,F) [B >= 0 && -4 + A + B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && -4 + A >= 0 && B >= A && C = 0] (?,1) Signature: {(f10,6);(f11,6);(f12,6);(f5,6)} Flow Graph: [0->{1,2,3,4},1->{1,2,3,4},2->{},3->{},4->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(0,2),(0,3),(0,4)] * Step 2: TrivialSCCs WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f12(A,B,C,D,E,F) -> f5(4,0,0,D,E,F) True (1,1) 1. f5(A,B,C,D,E,F) -> f5(A,1 + B,G,H,E,G) [B >= 0 && -4 + A + B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && -4 + A >= 0 && A >= 1 + B && C = 0] (?,1) 2. f5(A,B,C,D,E,F) -> f10(A,B,C,C,C,F) [B >= 0 && -4 + A + B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && -4 + A >= 0 && 0 >= 1 + C] (?,1) 3. f5(A,B,C,D,E,F) -> f10(A,B,C,C,C,F) [B >= 0 && -4 + A + B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && -4 + A >= 0 && C >= 1] (?,1) 4. f5(A,B,C,D,E,F) -> f11(A,B,0,0,0,F) [B >= 0 && -4 + A + B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && -4 + A >= 0 && B >= A && C = 0] (?,1) Signature: {(f10,6);(f11,6);(f12,6);(f5,6)} Flow Graph: [0->{1},1->{1,2,3,4},2->{},3->{},4->{}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 3: PolyRank WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f12(A,B,C,D,E,F) -> f5(4,0,0,D,E,F) True (1,1) 1. f5(A,B,C,D,E,F) -> f5(A,1 + B,G,H,E,G) [B >= 0 && -4 + A + B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && -4 + A >= 0 && A >= 1 + B && C = 0] (?,1) 2. f5(A,B,C,D,E,F) -> f10(A,B,C,C,C,F) [B >= 0 && -4 + A + B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && -4 + A >= 0 && 0 >= 1 + C] (1,1) 3. f5(A,B,C,D,E,F) -> f10(A,B,C,C,C,F) [B >= 0 && -4 + A + B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && -4 + A >= 0 && C >= 1] (1,1) 4. f5(A,B,C,D,E,F) -> f11(A,B,0,0,0,F) [B >= 0 && -4 + A + B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && -4 + A >= 0 && B >= A && C = 0] (1,1) Signature: {(f10,6);(f11,6);(f12,6);(f5,6)} Flow Graph: [0->{1},1->{1,2,3,4},2->{},3->{},4->{}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f10) = x1 + -1*x2 p(f11) = x1 + -1*x2 p(f12) = 4 p(f5) = x1 + -1*x2 Following rules are strictly oriented: [B >= 0 && -4 + A + B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && -4 + A >= 0 && A >= 1 + B && C = 0] ==> f5(A,B,C,D,E,F) = A + -1*B > -1 + A + -1*B = f5(A,1 + B,G,H,E,G) Following rules are weakly oriented: True ==> f12(A,B,C,D,E,F) = 4 >= 4 = f5(4,0,0,D,E,F) [B >= 0 && -4 + A + B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && -4 + A >= 0 && 0 >= 1 + C] ==> f5(A,B,C,D,E,F) = A + -1*B >= A + -1*B = f10(A,B,C,C,C,F) [B >= 0 && -4 + A + B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && -4 + A >= 0 && C >= 1] ==> f5(A,B,C,D,E,F) = A + -1*B >= A + -1*B = f10(A,B,C,C,C,F) [B >= 0 && -4 + A + B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && -4 + A >= 0 && B >= A && C = 0] ==> f5(A,B,C,D,E,F) = A + -1*B >= A + -1*B = f11(A,B,0,0,0,F) * Step 4: KnowledgePropagation WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f12(A,B,C,D,E,F) -> f5(4,0,0,D,E,F) True (1,1) 1. f5(A,B,C,D,E,F) -> f5(A,1 + B,G,H,E,G) [B >= 0 && -4 + A + B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && -4 + A >= 0 && A >= 1 + B && C = 0] (4,1) 2. f5(A,B,C,D,E,F) -> f10(A,B,C,C,C,F) [B >= 0 && -4 + A + B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && -4 + A >= 0 && 0 >= 1 + C] (1,1) 3. f5(A,B,C,D,E,F) -> f10(A,B,C,C,C,F) [B >= 0 && -4 + A + B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && -4 + A >= 0 && C >= 1] (1,1) 4. f5(A,B,C,D,E,F) -> f11(A,B,0,0,0,F) [B >= 0 && -4 + A + B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && -4 + A >= 0 && B >= A && C = 0] (1,1) Signature: {(f10,6);(f11,6);(f12,6);(f5,6)} Flow Graph: [0->{1},1->{1,2,3,4},2->{},3->{},4->{}] + Applied Processor: KnowledgePropagation + Details: The problem is already solved. YES(?,O(1))