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: AddSinks 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: AddSinks + Details: () * Step 3: 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) 9. f9(A,B) -> exitus616(A,B) True (?,1) 10. f10(A,B) -> exitus616(A,B) True (?,1) 11. f19(A,B) -> exitus616(A,B) True (?,1) Signature: {(exitus616,2);(f0,2);(f10,2);(f19,2);(f9,2)} Flow Graph: [0->{1,2,3,4,9},1->{5,8,11},2->{6,7,10},3->{6,7,10},4->{6,7,10},5->{5,8,11},6->{1,2,3,4,9},7->{1,2,3,4,9} ,8->{1,2,3,4,9},9->{},10->{},11->{}] + 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 4: 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) 9. f9(A,B) -> exitus616(A,B) True (?,1) 10. f10(A,B) -> exitus616(A,B) True (?,1) 11. f19(A,B) -> exitus616(A,B) True (?,1) Signature: {(exitus616,2);(f0,2);(f10,2);(f19,2);(f9,2)} Flow Graph: [0->{1,2,3,4,9},1->{5,11},2->{6,10},3->{6,10},4->{7,10},5->{5,8,11},6->{1,2,3,9},7->{1,2,3,4,9},8->{4,9} ,9->{},10->{},11->{}] + Applied Processor: LooptreeTransformer + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11] | `- p:[1,6,2,7,4,8,5,3] c: [] MAYBE