NO * Step 1: UnsatPaths NO + Considered Problem: Rules: 0. f0(A,B) -> f9(C,B) True (1,1) 1. f9(A,B) -> f19(A,0) [A >= 6] (?,1) 2. f9(A,B) -> f10(A,C) [A >= 6 && C >= 1] (?,1) 3. f9(A,B) -> f10(A,C) [A >= 6 && 0 >= 1 + C] (?,1) 4. f9(A,B) -> f10(A,B) [5 >= A] (?,1) 5. f19(A,B) -> f19(-1 + A,B) [-1*B >= 0 && B >= 0 && A >= 3] (?,1) 6. f10(A,B) -> f9(1 + A,B) [A >= 6] (?,1) 7. f10(A,B) -> f9(1 + A,B) [5 >= A] (?,1) 8. f19(A,B) -> f9(A,B) [-1*B >= 0 && B >= 0 && 2 >= A] (?,1) Signature: {(f0,2);(f10,2);(f19,2);(f9,2)} Flow Graph: [0->{1,2,3,4},1->{5,8},2->{6,7},3->{6,7},4->{6,7},5->{5,8},6->{1,2,3,4},7->{1,2,3,4},8->{1,2,3,4}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(1,8),(2,7),(3,7),(4,6),(6,4),(8,1),(8,2),(8,3)] * Step 2: FromIts NO + Considered Problem: Rules: 0. f0(A,B) -> f9(C,B) True (1,1) 1. f9(A,B) -> f19(A,0) [A >= 6] (?,1) 2. f9(A,B) -> f10(A,C) [A >= 6 && C >= 1] (?,1) 3. f9(A,B) -> f10(A,C) [A >= 6 && 0 >= 1 + C] (?,1) 4. f9(A,B) -> f10(A,B) [5 >= A] (?,1) 5. f19(A,B) -> f19(-1 + A,B) [-1*B >= 0 && B >= 0 && A >= 3] (?,1) 6. f10(A,B) -> f9(1 + A,B) [A >= 6] (?,1) 7. f10(A,B) -> f9(1 + A,B) [5 >= A] (?,1) 8. f19(A,B) -> f9(A,B) [-1*B >= 0 && B >= 0 && 2 >= A] (?,1) Signature: {(f0,2);(f10,2);(f19,2);(f9,2)} Flow Graph: [0->{1,2,3,4},1->{5},2->{6},3->{6},4->{7},5->{5,8},6->{1,2,3},7->{1,2,3,4},8->{4}] + Applied Processor: FromIts + Details: () * Step 3: CloseWith NO + Considered Problem: Rules: f0(A,B) -> f9(C,B) True f9(A,B) -> f19(A,0) [A >= 6] f9(A,B) -> f10(A,C) [A >= 6 && C >= 1] f9(A,B) -> f10(A,C) [A >= 6 && 0 >= 1 + C] f9(A,B) -> f10(A,B) [5 >= A] f19(A,B) -> f19(-1 + A,B) [-1*B >= 0 && B >= 0 && A >= 3] f10(A,B) -> f9(1 + A,B) [A >= 6] f10(A,B) -> f9(1 + A,B) [5 >= A] f19(A,B) -> f9(A,B) [-1*B >= 0 && B >= 0 && 2 >= A] Signature: {(f0,2);(f10,2);(f19,2);(f9,2)} Rule Graph: [0->{1,2,3,4},1->{5},2->{6},3->{6},4->{7},5->{5,8},6->{1,2,3},7->{1,2,3,4},8->{4}] + Applied Processor: CloseWith False + Details: () NO