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