YES(?,O(1)) * Step 1: UnsatPaths WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f0(A,B,C) -> f8(0,10,0) True (1,1) 1. f8(A,B,C) -> f8(2 + A,B,1 + C) [B >= 1 + C] (?,1) 2. f8(A,B,C) -> f6(A,B,C) [2*B >= 1 + A && C >= B] (?,1) 3. f8(A,B,C) -> f6(A,B,C) [A >= 2*B && C >= B] (?,1) Signature: {(f0,3);(f6,3);(f8,3)} Flow Graph: [0->{1,2,3},1->{1,2,3},2->{},3->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(0,2),(0,3)] * Step 2: TrivialSCCs WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f0(A,B,C) -> f8(0,10,0) True (1,1) 1. f8(A,B,C) -> f8(2 + A,B,1 + C) [B >= 1 + C] (?,1) 2. f8(A,B,C) -> f6(A,B,C) [2*B >= 1 + A && C >= B] (?,1) 3. f8(A,B,C) -> f6(A,B,C) [A >= 2*B && C >= B] (?,1) Signature: {(f0,3);(f6,3);(f8,3)} Flow Graph: [0->{1},1->{1,2,3},2->{},3->{}] + 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. f0(A,B,C) -> f8(0,10,0) True (1,1) 1. f8(A,B,C) -> f8(2 + A,B,1 + C) [B >= 1 + C] (?,1) 2. f8(A,B,C) -> f6(A,B,C) [2*B >= 1 + A && C >= B] (1,1) 3. f8(A,B,C) -> f6(A,B,C) [A >= 2*B && C >= B] (1,1) Signature: {(f0,3);(f6,3);(f8,3)} Flow Graph: [0->{1},1->{1,2,3},2->{},3->{}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f0) = 10 p(f6) = x2 + -1*x3 p(f8) = x2 + -1*x3 Following rules are strictly oriented: [B >= 1 + C] ==> f8(A,B,C) = B + -1*C > -1 + B + -1*C = f8(2 + A,B,1 + C) Following rules are weakly oriented: True ==> f0(A,B,C) = 10 >= 10 = f8(0,10,0) [2*B >= 1 + A && C >= B] ==> f8(A,B,C) = B + -1*C >= B + -1*C = f6(A,B,C) [A >= 2*B && C >= B] ==> f8(A,B,C) = B + -1*C >= B + -1*C = f6(A,B,C) * Step 4: KnowledgePropagation WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f0(A,B,C) -> f8(0,10,0) True (1,1) 1. f8(A,B,C) -> f8(2 + A,B,1 + C) [B >= 1 + C] (10,1) 2. f8(A,B,C) -> f6(A,B,C) [2*B >= 1 + A && C >= B] (1,1) 3. f8(A,B,C) -> f6(A,B,C) [A >= 2*B && C >= B] (1,1) Signature: {(f0,3);(f6,3);(f8,3)} Flow Graph: [0->{1},1->{1,2,3},2->{},3->{}] + Applied Processor: KnowledgePropagation + Details: The problem is already solved. YES(?,O(1))