MAYBE * Step 1: TrivialSCCs 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: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatPaths 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) 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,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,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,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,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: UnsatPaths + Details: We remove following edges from the transition graph: [(2,7),(3,7),(6,11),(8,11)] * Step 3: UnreachableRules 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) 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,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,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,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,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},3->{0,3},4->{8,11},5->{8,11},6->{8},7->{8,11},8->{8},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 4: AddSinks 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) 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) 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) 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},3->{0,3},7->{8,11},8->{8},9->{8,11},11->{2,9}] + Applied Processor: AddSinks + Details: () * Step 5: UnsatPaths 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) 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) 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) 12. f8(A,B,C,D,E,F,G,H,I,J,K,L,M) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M) True (?,1) 13. f1(A,B,C,D,E,F,G,H,I,J,K,L,M) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M) True (?,1) Signature: {(exitus616,13);(f1,13);(f10,13);(f12,13);(f13,13);(f15,13);(f300,13);(f32,13);(f8,13)} Flow Graph: [0->{},1->{0,3,7,12},2->{0,3,7,12},3->{0,3,7,12},7->{8,11,13},8->{8,11,13},9->{8,11,13},11->{2,9},12->{} ,13->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(2,7),(3,7),(8,11)] * Step 6: Failure 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) 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) 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) 12. f8(A,B,C,D,E,F,G,H,I,J,K,L,M) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M) True (?,1) 13. f1(A,B,C,D,E,F,G,H,I,J,K,L,M) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M) True (?,1) Signature: {(exitus616,13);(f1,13);(f10,13);(f12,13);(f13,13);(f15,13);(f300,13);(f32,13);(f8,13)} Flow Graph: [0->{},1->{0,3,7,12},2->{0,3,12},3->{0,3,12},7->{8,11,13},8->{8,13},9->{8,11,13},11->{2,9},12->{},13->{}] + Applied Processor: LooptreeTransformer + Details: We construct a looptree: P: [0,1,2,3,7,8,9,11,12,13] | +- p:[11,9] c: [11] | +- p:[8] c: [] | `- p:[3] c: [3] MAYBE