YES(?,O(1)) * Step 1: TrivialSCCs WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f12(A,B,C,D,E,F) -> f5(400,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 (?,1) && -400 + A + B >= 0 && 400 + -1*A + B >= 0 && 400 + -1*A >= 0 && -400 + A >= 0 && A >= 1 + B && C = 0] 2. f5(A,B,C,D,E,F) -> f10(A,B,C,C,C,F) [B >= 0 && -400 + A + B >= 0 && 400 + -1*A + B >= 0 && 400 + -1*A >= 0 && -400 + A >= 0 && 0 >= 1 + C] (?,1) 3. f5(A,B,C,D,E,F) -> f10(A,B,C,C,C,F) [B >= 0 && -400 + A + B >= 0 && 400 + -1*A + B >= 0 && 400 + -1*A >= 0 && -400 + A >= 0 && C >= 1] (?,1) 4. f5(A,B,C,D,E,F) -> f11(A,B,0,0,0,F) [B >= 0 && -400 + A + B >= 0 && 400 + -1*A + B >= 0 && 400 + -1*A >= 0 && -400 + 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: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatPaths WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f12(A,B,C,D,E,F) -> f5(400,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 (?,1) && -400 + A + B >= 0 && 400 + -1*A + B >= 0 && 400 + -1*A >= 0 && -400 + A >= 0 && A >= 1 + B && C = 0] 2. f5(A,B,C,D,E,F) -> f10(A,B,C,C,C,F) [B >= 0 && -400 + A + B >= 0 && 400 + -1*A + B >= 0 && 400 + -1*A >= 0 && -400 + A >= 0 && 0 >= 1 + C] (1,1) 3. f5(A,B,C,D,E,F) -> f10(A,B,C,C,C,F) [B >= 0 && -400 + A + B >= 0 && 400 + -1*A + B >= 0 && 400 + -1*A >= 0 && -400 + A >= 0 && C >= 1] (1,1) 4. f5(A,B,C,D,E,F) -> f11(A,B,0,0,0,F) [B >= 0 && -400 + A + B >= 0 && 400 + -1*A + B >= 0 && 400 + -1*A >= 0 && -400 + A >= 0 && B >= A && C = 0] (1,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 3: PolyRank WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f12(A,B,C,D,E,F) -> f5(400,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 (?,1) && -400 + A + B >= 0 && 400 + -1*A + B >= 0 && 400 + -1*A >= 0 && -400 + A >= 0 && A >= 1 + B && C = 0] 2. f5(A,B,C,D,E,F) -> f10(A,B,C,C,C,F) [B >= 0 && -400 + A + B >= 0 && 400 + -1*A + B >= 0 && 400 + -1*A >= 0 && -400 + A >= 0 && 0 >= 1 + C] (1,1) 3. f5(A,B,C,D,E,F) -> f10(A,B,C,C,C,F) [B >= 0 && -400 + A + B >= 0 && 400 + -1*A + B >= 0 && 400 + -1*A >= 0 && -400 + A >= 0 && C >= 1] (1,1) 4. f5(A,B,C,D,E,F) -> f11(A,B,0,0,0,F) [B >= 0 && -400 + A + B >= 0 && 400 + -1*A + B >= 0 && 400 + -1*A >= 0 && -400 + 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) = 400 p(f5) = x1 + -1*x2 Following rules are strictly oriented: [B >= 0 ==> && -400 + A + B >= 0 && 400 + -1*A + B >= 0 && 400 + -1*A >= 0 && -400 + 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) = 400 >= 400 = f5(400,0,0,D,E,F) [B >= 0 && -400 + A + B >= 0 && 400 + -1*A + B >= 0 && 400 + -1*A >= 0 && -400 + 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 && -400 + A + B >= 0 && 400 + -1*A + B >= 0 && 400 + -1*A >= 0 && -400 + 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 && -400 + A + B >= 0 && 400 + -1*A + B >= 0 && 400 + -1*A >= 0 && -400 + 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(400,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 (400,1) && -400 + A + B >= 0 && 400 + -1*A + B >= 0 && 400 + -1*A >= 0 && -400 + A >= 0 && A >= 1 + B && C = 0] 2. f5(A,B,C,D,E,F) -> f10(A,B,C,C,C,F) [B >= 0 && -400 + A + B >= 0 && 400 + -1*A + B >= 0 && 400 + -1*A >= 0 && -400 + A >= 0 && 0 >= 1 + C] (1,1) 3. f5(A,B,C,D,E,F) -> f10(A,B,C,C,C,F) [B >= 0 && -400 + A + B >= 0 && 400 + -1*A + B >= 0 && 400 + -1*A >= 0 && -400 + A >= 0 && C >= 1] (1,1) 4. f5(A,B,C,D,E,F) -> f11(A,B,0,0,0,F) [B >= 0 && -400 + A + B >= 0 && 400 + -1*A + B >= 0 && 400 + -1*A >= 0 && -400 + 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))