MAYBE * Step 1: UnsatPaths MAYBE + 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: Failure MAYBE + 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: Failing "Open problems left." + Details: Open problems left. MAYBE