MAYBE * Step 1: ArgumentFilter MAYBE + Considered Problem: Rules: 0. f8(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f32(A,B,N,D,E,F,G,H,I,J,K,L,M) [A >= B] (?,1) 1. f15(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f8(A,B,C,N,E,F,G,H,I,J,K,L,M) True (1,1) 2. f300(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f8(1 + A,B,C,D,E,F,G,H,I,J,K,L,M) [B >= E] (?,1) 3. f8(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f8(1 + A,B,C,D,E,F,G,H,I,J,K,L,M) [B >= 1 + A && B >= E] (?,1) 4. f13(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f1(A,B,N,D,E,O,P,0,2,0,0,L,M) True (?,1) 5. f12(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f1(A,B,N,D,E,O,P,0,I,0,0,1 + I,M) [4 >= I] (?,1) 6. f10(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f1(A,B,N,D,E,O,P,0,I,0,0,L,2) True (?,1) 7. f8(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f1(A,B,N,D,E,O,P,0,I,0,0,L,M) [B >= 1 + A && E >= 1 + B] (?,1) 8. f1(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f1(A,B,N,D,E,O,P,0,I,0,0,L,M) [E >= 1 + B && 4 >= M] (?,1) 9. f300(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f1(A,B,N,D,E,O,P,0,I,0,0,L,M) [E >= 1 + B] (?,1) 10. f12(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f300(A,1 + B,N,D,E,O,G,1,I,1,1,L,M) [I >= 5] (?,1) 11. f1(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f300(A,1 + B,N,D,E,O,G,1,I,1,1,L,M) [E >= 1 + B && M >= 5] (?,1) Signature: {(f1,13);(f10,13);(f12,13);(f13,13);(f15,13);(f300,13);(f32,13);(f8,13)} Flow Graph: [0->{},1->{0,3,7},2->{0,3,7},3->{0,3,7},4->{8,11},5->{8,11},6->{8,11},7->{8,11},8->{8,11},9->{8,11},10->{2 ,9},11->{2,9}] + Applied Processor: ArgumentFilter [2,3,5,6,7,9,10,11] + Details: We remove following argument positions: [2,3,5,6,7,9,10,11]. * Step 2: UnreachableRules MAYBE + Considered Problem: Rules: 0. f8(A,B,E,I,M) -> f32(A,B,E,I,M) [A >= B] (?,1) 1. f15(A,B,E,I,M) -> f8(A,B,E,I,M) True (1,1) 2. f300(A,B,E,I,M) -> f8(1 + A,B,E,I,M) [B >= E] (?,1) 3. f8(A,B,E,I,M) -> f8(1 + A,B,E,I,M) [B >= 1 + A && B >= E] (?,1) 4. f13(A,B,E,I,M) -> f1(A,B,E,2,M) True (?,1) 5. f12(A,B,E,I,M) -> f1(A,B,E,I,M) [4 >= I] (?,1) 6. f10(A,B,E,I,M) -> f1(A,B,E,I,2) True (?,1) 7. f8(A,B,E,I,M) -> f1(A,B,E,I,M) [B >= 1 + A && E >= 1 + B] (?,1) 8. f1(A,B,E,I,M) -> f1(A,B,E,I,M) [E >= 1 + B && 4 >= M] (?,1) 9. f300(A,B,E,I,M) -> f1(A,B,E,I,M) [E >= 1 + B] (?,1) 10. f12(A,B,E,I,M) -> f300(A,1 + B,E,I,M) [I >= 5] (?,1) 11. f1(A,B,E,I,M) -> f300(A,1 + B,E,I,M) [E >= 1 + B && M >= 5] (?,1) Signature: {(f1,13);(f10,13);(f12,13);(f13,13);(f15,13);(f300,13);(f32,13);(f8,13)} Flow Graph: [0->{},1->{0,3,7},2->{0,3,7},3->{0,3,7},4->{8,11},5->{8,11},6->{8,11},7->{8,11},8->{8,11},9->{8,11},10->{2 ,9},11->{2,9}] + Applied Processor: UnreachableRules + Details: Following transitions are not reachable from the starting states and are revomed: [4,5,6,10] * Step 3: UnsatPaths MAYBE + Considered Problem: Rules: 0. f8(A,B,E,I,M) -> f32(A,B,E,I,M) [A >= B] (?,1) 1. f15(A,B,E,I,M) -> f8(A,B,E,I,M) True (1,1) 2. f300(A,B,E,I,M) -> f8(1 + A,B,E,I,M) [B >= E] (?,1) 3. f8(A,B,E,I,M) -> f8(1 + A,B,E,I,M) [B >= 1 + A && B >= E] (?,1) 7. f8(A,B,E,I,M) -> f1(A,B,E,I,M) [B >= 1 + A && E >= 1 + B] (?,1) 8. f1(A,B,E,I,M) -> f1(A,B,E,I,M) [E >= 1 + B && 4 >= M] (?,1) 9. f300(A,B,E,I,M) -> f1(A,B,E,I,M) [E >= 1 + B] (?,1) 11. f1(A,B,E,I,M) -> f300(A,1 + B,E,I,M) [E >= 1 + B && M >= 5] (?,1) Signature: {(f1,13);(f10,13);(f12,13);(f13,13);(f15,13);(f300,13);(f32,13);(f8,13)} Flow Graph: [0->{},1->{0,3,7},2->{0,3,7},3->{0,3,7},7->{8,11},8->{8,11},9->{8,11},11->{2,9}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(2,7),(3,7),(8,11)] * Step 4: FromIts MAYBE + Considered Problem: Rules: 0. f8(A,B,E,I,M) -> f32(A,B,E,I,M) [A >= B] (?,1) 1. f15(A,B,E,I,M) -> f8(A,B,E,I,M) True (1,1) 2. f300(A,B,E,I,M) -> f8(1 + A,B,E,I,M) [B >= E] (?,1) 3. f8(A,B,E,I,M) -> f8(1 + A,B,E,I,M) [B >= 1 + A && B >= E] (?,1) 7. f8(A,B,E,I,M) -> f1(A,B,E,I,M) [B >= 1 + A && E >= 1 + B] (?,1) 8. f1(A,B,E,I,M) -> f1(A,B,E,I,M) [E >= 1 + B && 4 >= M] (?,1) 9. f300(A,B,E,I,M) -> f1(A,B,E,I,M) [E >= 1 + B] (?,1) 11. f1(A,B,E,I,M) -> f300(A,1 + B,E,I,M) [E >= 1 + B && M >= 5] (?,1) Signature: {(f1,13);(f10,13);(f12,13);(f13,13);(f15,13);(f300,13);(f32,13);(f8,13)} Flow Graph: [0->{},1->{0,3,7},2->{0,3},3->{0,3},7->{8,11},8->{8},9->{8,11},11->{2,9}] + Applied Processor: FromIts + Details: () * Step 5: Unfold MAYBE + Considered Problem: Rules: f8(A,B,E,I,M) -> f32(A,B,E,I,M) [A >= B] f15(A,B,E,I,M) -> f8(A,B,E,I,M) True f300(A,B,E,I,M) -> f8(1 + A,B,E,I,M) [B >= E] f8(A,B,E,I,M) -> f8(1 + A,B,E,I,M) [B >= 1 + A && B >= E] f8(A,B,E,I,M) -> f1(A,B,E,I,M) [B >= 1 + A && E >= 1 + B] f1(A,B,E,I,M) -> f1(A,B,E,I,M) [E >= 1 + B && 4 >= M] f300(A,B,E,I,M) -> f1(A,B,E,I,M) [E >= 1 + B] f1(A,B,E,I,M) -> f300(A,1 + B,E,I,M) [E >= 1 + B && M >= 5] Signature: {(f1,13);(f10,13);(f12,13);(f13,13);(f15,13);(f300,13);(f32,13);(f8,13)} Rule Graph: [0->{},1->{0,3,7},2->{0,3},3->{0,3},7->{8,11},8->{8},9->{8,11},11->{2,9}] + Applied Processor: Unfold + Details: () * Step 6: AddSinks MAYBE + Considered Problem: Rules: f8.0(A,B,E,I,M) -> f32.12(A,B,E,I,M) [A >= B] f15.1(A,B,E,I,M) -> f8.0(A,B,E,I,M) True f15.1(A,B,E,I,M) -> f8.3(A,B,E,I,M) True f15.1(A,B,E,I,M) -> f8.7(A,B,E,I,M) True f300.2(A,B,E,I,M) -> f8.0(1 + A,B,E,I,M) [B >= E] f300.2(A,B,E,I,M) -> f8.3(1 + A,B,E,I,M) [B >= E] f8.3(A,B,E,I,M) -> f8.0(1 + A,B,E,I,M) [B >= 1 + A && B >= E] f8.3(A,B,E,I,M) -> f8.3(1 + A,B,E,I,M) [B >= 1 + A && B >= E] f8.7(A,B,E,I,M) -> f1.8(A,B,E,I,M) [B >= 1 + A && E >= 1 + B] f8.7(A,B,E,I,M) -> f1.11(A,B,E,I,M) [B >= 1 + A && E >= 1 + B] f1.8(A,B,E,I,M) -> f1.8(A,B,E,I,M) [E >= 1 + B && 4 >= M] f300.9(A,B,E,I,M) -> f1.8(A,B,E,I,M) [E >= 1 + B] f300.9(A,B,E,I,M) -> f1.11(A,B,E,I,M) [E >= 1 + B] f1.11(A,B,E,I,M) -> f300.2(A,1 + B,E,I,M) [E >= 1 + B && M >= 5] f1.11(A,B,E,I,M) -> f300.9(A,1 + B,E,I,M) [E >= 1 + B && M >= 5] Signature: {(f1.11,5);(f1.8,5);(f15.1,5);(f300.2,5);(f300.9,5);(f32.12,5);(f8.0,5);(f8.3,5);(f8.7,5)} Rule Graph: [0->{},1->{0},2->{6,7},3->{8,9},4->{0},5->{6,7},6->{0},7->{6,7},8->{10},9->{13,14},10->{10},11->{10} ,12->{13,14},13->{4,5},14->{11,12}] + Applied Processor: AddSinks + Details: () * Step 7: Failure MAYBE + Considered Problem: Rules: f8.0(A,B,E,I,M) -> f32.12(A,B,E,I,M) [A >= B] f15.1(A,B,E,I,M) -> f8.0(A,B,E,I,M) True f15.1(A,B,E,I,M) -> f8.3(A,B,E,I,M) True f15.1(A,B,E,I,M) -> f8.7(A,B,E,I,M) True f300.2(A,B,E,I,M) -> f8.0(1 + A,B,E,I,M) [B >= E] f300.2(A,B,E,I,M) -> f8.3(1 + A,B,E,I,M) [B >= E] f8.3(A,B,E,I,M) -> f8.0(1 + A,B,E,I,M) [B >= 1 + A && B >= E] f8.3(A,B,E,I,M) -> f8.3(1 + A,B,E,I,M) [B >= 1 + A && B >= E] f8.7(A,B,E,I,M) -> f1.8(A,B,E,I,M) [B >= 1 + A && E >= 1 + B] f8.7(A,B,E,I,M) -> f1.11(A,B,E,I,M) [B >= 1 + A && E >= 1 + B] f1.8(A,B,E,I,M) -> f1.8(A,B,E,I,M) [E >= 1 + B && 4 >= M] f300.9(A,B,E,I,M) -> f1.8(A,B,E,I,M) [E >= 1 + B] f300.9(A,B,E,I,M) -> f1.11(A,B,E,I,M) [E >= 1 + B] f1.11(A,B,E,I,M) -> f300.2(A,1 + B,E,I,M) [E >= 1 + B && M >= 5] f1.11(A,B,E,I,M) -> f300.9(A,1 + B,E,I,M) [E >= 1 + B && M >= 5] f1.8(A,B,E,I,M) -> exitus616(A,B,E,I,M) True f32.12(A,B,E,I,M) -> exitus616(A,B,E,I,M) True f32.12(A,B,E,I,M) -> exitus616(A,B,E,I,M) True f1.8(A,B,E,I,M) -> exitus616(A,B,E,I,M) True f32.12(A,B,E,I,M) -> exitus616(A,B,E,I,M) True f32.12(A,B,E,I,M) -> exitus616(A,B,E,I,M) True Signature: {(exitus616,5);(f1.11,5);(f1.8,5);(f15.1,5);(f300.2,5);(f300.9,5);(f32.12,5);(f8.0,5);(f8.3,5);(f8.7,5)} Rule Graph: [0->{16,17,19,20},1->{0},2->{6,7},3->{8,9},4->{0},5->{6,7},6->{0},7->{6,7},8->{10},9->{13,14},10->{10,15 ,18},11->{10},12->{13,14},13->{4,5},14->{11,12}] + Applied Processor: Decompose Greedy + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20] | +- p:[14,12] c: [12,14] | +- p:[10] c: [] | `- p:[7] c: [7] MAYBE