NO * Step 1: TrivialSCCs NO + Considered Problem: Rules: 0. f6(A,B,C,D) -> f7(A,B,C,D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && 0 >= 1 + A] (?,1) 1. f6(A,B,C,D) -> f7(A,B,C,D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && A >= 1] (?,1) 2. f0(A,B,C,D) -> f4(A,B,C,1 + B) [B >= 0 && C >= B] (1,1) 3. f4(A,B,C,D) -> f6(E,B,C,D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && B >= 1 + D] (?,1) 4. f4(A,B,C,D) -> f6(E,B,C,D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && D >= 1 + B] (?,1) 5. f7(A,B,C,D) -> f4(A,B,C,1 + D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && C >= D] (?,1) 6. f7(A,B,C,D) -> f4(A,B,C,0) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && D >= 1 + C] (?,1) 7. f6(A,B,C,D) -> f14(0,B,C,D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && A = 0] (?,1) 8. f4(A,B,C,D) -> f14(A,B,C,B) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && B = D] (?,1) Signature: {(f0,4);(f14,4);(f4,4);(f6,4);(f7,4)} Flow Graph: [0->{5,6},1->{5,6},2->{3,4,8},3->{0,1,7},4->{0,1,7},5->{3,4,8},6->{3,4,8},7->{},8->{}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatPaths NO + Considered Problem: Rules: 0. f6(A,B,C,D) -> f7(A,B,C,D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && 0 >= 1 + A] (?,1) 1. f6(A,B,C,D) -> f7(A,B,C,D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && A >= 1] (?,1) 2. f0(A,B,C,D) -> f4(A,B,C,1 + B) [B >= 0 && C >= B] (1,1) 3. f4(A,B,C,D) -> f6(E,B,C,D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && B >= 1 + D] (?,1) 4. f4(A,B,C,D) -> f6(E,B,C,D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && D >= 1 + B] (?,1) 5. f7(A,B,C,D) -> f4(A,B,C,1 + D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && C >= D] (?,1) 6. f7(A,B,C,D) -> f4(A,B,C,0) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && D >= 1 + C] (?,1) 7. f6(A,B,C,D) -> f14(0,B,C,D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && A = 0] (1,1) 8. f4(A,B,C,D) -> f14(A,B,C,B) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && B = D] (1,1) Signature: {(f0,4);(f14,4);(f4,4);(f6,4);(f7,4)} Flow Graph: [0->{5,6},1->{5,6},2->{3,4,8},3->{0,1,7},4->{0,1,7},5->{3,4,8},6->{3,4,8},7->{},8->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(2,3),(2,8),(6,4)] * Step 3: Looptree NO + Considered Problem: Rules: 0. f6(A,B,C,D) -> f7(A,B,C,D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && 0 >= 1 + A] (?,1) 1. f6(A,B,C,D) -> f7(A,B,C,D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && A >= 1] (?,1) 2. f0(A,B,C,D) -> f4(A,B,C,1 + B) [B >= 0 && C >= B] (1,1) 3. f4(A,B,C,D) -> f6(E,B,C,D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && B >= 1 + D] (?,1) 4. f4(A,B,C,D) -> f6(E,B,C,D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && D >= 1 + B] (?,1) 5. f7(A,B,C,D) -> f4(A,B,C,1 + D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && C >= D] (?,1) 6. f7(A,B,C,D) -> f4(A,B,C,0) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && D >= 1 + C] (?,1) 7. f6(A,B,C,D) -> f14(0,B,C,D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && A = 0] (1,1) 8. f4(A,B,C,D) -> f14(A,B,C,B) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && B = D] (1,1) Signature: {(f0,4);(f14,4);(f4,4);(f6,4);(f7,4)} Flow Graph: [0->{5,6},1->{5,6},2->{4},3->{0,1,7},4->{0,1,7},5->{3,4,8},6->{3,8},7->{},8->{}] + Applied Processor: Looptree + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8] | `- p:[0,3,5,1,4,6] c: [] NO