MAYBE * Step 1: UnsatPaths MAYBE + Considered Problem: Rules: 0. f0(A,B) -> f9(C,B) True (1,1) 1. f9(A,B) -> f20(A,B) [A >= 6] (?,1) 2. f9(A,B) -> f20(A,0) [5 >= A] (?,1) 3. f9(A,B) -> f12(A,C) [5 >= A && C >= 1] (?,1) 4. f9(A,B) -> f12(A,C) [5 >= A && 0 >= 1 + C] (?,1) 5. f20(A,B) -> f20(-1 + A,B) [A >= 3] (?,1) 6. f20(A,B) -> f9(A,B) [2 >= A] (?,1) 7. f12(A,B) -> f9(1 + A,B) [5 + -1*A >= 0 && 5 >= A] (?,1) Signature: {(f0,2);(f12,2);(f20,2);(f9,2)} Flow Graph: [0->{1,2,3,4},1->{5,6},2->{5,6},3->{7},4->{7},5->{5,6},6->{1,2,3,4},7->{1,2,3,4}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(1,6),(6,1)] * Step 2: Failure MAYBE + Considered Problem: Rules: 0. f0(A,B) -> f9(C,B) True (1,1) 1. f9(A,B) -> f20(A,B) [A >= 6] (?,1) 2. f9(A,B) -> f20(A,0) [5 >= A] (?,1) 3. f9(A,B) -> f12(A,C) [5 >= A && C >= 1] (?,1) 4. f9(A,B) -> f12(A,C) [5 >= A && 0 >= 1 + C] (?,1) 5. f20(A,B) -> f20(-1 + A,B) [A >= 3] (?,1) 6. f20(A,B) -> f9(A,B) [2 >= A] (?,1) 7. f12(A,B) -> f9(1 + A,B) [5 + -1*A >= 0 && 5 >= A] (?,1) Signature: {(f0,2);(f12,2);(f20,2);(f9,2)} Flow Graph: [0->{1,2,3,4},1->{5},2->{5,6},3->{7},4->{7},5->{5,6},6->{2,3,4},7->{1,2,3,4}] + Applied Processor: Failing "Open problems left." + Details: Open problems left. MAYBE