MAYBE * Step 1: UnsatPaths MAYBE + Considered Problem: Rules: 0. f4(A,B,C) -> f5(A,B,C) [A >= 1 + B] (?,1) 1. f0(A,B,C) -> f4(D,1 + D,B) True (1,1) 2. f4(A,B,C) -> f4(D,1 + D,B) True (?,1) Signature: {(f0,3);(f4,3);(f5,3)} Flow Graph: [0->{},1->{0,2},2->{0,2}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(1,0),(2,0)] * Step 2: FromIts MAYBE + Considered Problem: Rules: 0. f4(A,B,C) -> f5(A,B,C) [A >= 1 + B] (?,1) 1. f0(A,B,C) -> f4(D,1 + D,B) True (1,1) 2. f4(A,B,C) -> f4(D,1 + D,B) True (?,1) Signature: {(f0,3);(f4,3);(f5,3)} Flow Graph: [0->{},1->{2},2->{2}] + Applied Processor: FromIts + Details: () * Step 3: Unfold MAYBE + Considered Problem: Rules: f4(A,B,C) -> f5(A,B,C) [A >= 1 + B] f0(A,B,C) -> f4(D,1 + D,B) True f4(A,B,C) -> f4(D,1 + D,B) True Signature: {(f0,3);(f4,3);(f5,3)} Rule Graph: [0->{},1->{2},2->{2}] + Applied Processor: Unfold + Details: () * Step 4: AddSinks MAYBE + Considered Problem: Rules: f4.0(A,B,C) -> f5.3(A,B,C) [A >= 1 + B] f0.1(A,B,C) -> f4.2(D,1 + D,B) True f4.2(A,B,C) -> f4.2(D,1 + D,B) True Signature: {(f0.1,3);(f4.0,3);(f4.2,3);(f5.3,3)} Rule Graph: [0->{},1->{2},2->{2}] + Applied Processor: AddSinks + Details: () * Step 5: Failure MAYBE + Considered Problem: Rules: f4.0(A,B,C) -> f5.3(A,B,C) [A >= 1 + B] f0.1(A,B,C) -> f4.2(D,1 + D,B) True f4.2(A,B,C) -> f4.2(D,1 + D,B) True f4.2(A,B,C) -> exitus616(A,B,C) True f5.3(A,B,C) -> exitus616(A,B,C) True Signature: {(exitus616,3);(f0.1,3);(f4.0,3);(f4.2,3);(f5.3,3)} Rule Graph: [0->{4},1->{2},2->{2,3}] + Applied Processor: Decompose Greedy + Details: We construct a looptree: P: [0,1,2,3,4] | `- p:[2] c: [] MAYBE