MAYBE * Step 1: TrivialSCCs MAYBE + Considered Problem: Rules: 0. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [A >= B] (?,1) 1. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [C >= 3] (?,1) 2. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [1 >= C] (?,1) 3. f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) True (?,1) 4. f54(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f57(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) True (?,1) 5. f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f52(A,B,C,D,0,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [D >= 1] (?,1) 6. f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f52(A,B,C,D,0,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [0 >= D] (?,1) 7. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f45(A,B,2,D,1 + E,F,H,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [C = 2] (?,1) 8. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f45(A,B,C,D,E,F,G,V,W,X,Y,E,V,V,O,P,Q,R,S,T,U) [V >= 1 && B >= 1 + A] (?,1) 9. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f37(A,B,Z,D,E,F,G,V,W,X,Y,E,V,V,V,Q,0,Z,Z,0,U) [B >= 1 + A && 0 >= V && Z >= 2] (?,1) 10. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f37(A,B,Z,D,E,F,G,V,W,X,Y,E,V,V,V,Q,0,Z,Z,0,U) [B >= 1 + A && 0 >= V && 0 >= Z] (?,1) 11. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f13(1 + A,B,1,D,E,F,G,V,W,X,Y,E,V,V,V,Q,Q,1,1,0,U) [0 >= V && B >= 1 + A] (?,1) 12. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f13(A,B,C,W,E,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,0) [0 >= W] (1,1) 13. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f13(A,B,C,W,E,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,0) [W >= 1] (1,1) Signature: {(f0,21);(f13,21);(f37,21);(f45,21);(f52,21);(f54,21);(f57,21)} Flow Graph: [0->{5,6},1->{5,6},2->{5,6},3->{3},4->{},5->{3},6->{3},7->{5,6},8->{5,6},9->{1,2,7},10->{1,2,7},11->{0,8,9 ,10,11},12->{0,8,9,10,11},13->{0,8,9,10,11}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatPaths MAYBE + Considered Problem: Rules: 0. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [A >= B] (1,1) 1. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [C >= 3] (1,1) 2. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [1 >= C] (1,1) 3. f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) True (?,1) 4. f54(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f57(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) True (1,1) 5. f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f52(A,B,C,D,0,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [D >= 1] (1,1) 6. f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f52(A,B,C,D,0,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [0 >= D] (1,1) 7. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f45(A,B,2,D,1 + E,F,H,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [C = 2] (1,1) 8. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f45(A,B,C,D,E,F,G,V,W,X,Y,E,V,V,O,P,Q,R,S,T,U) [V >= 1 && B >= 1 + A] (1,1) 9. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f37(A,B,Z,D,E,F,G,V,W,X,Y,E,V,V,V,Q,0,Z,Z,0,U) [B >= 1 + A && 0 >= V && Z >= 2] (1,1) 10. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f37(A,B,Z,D,E,F,G,V,W,X,Y,E,V,V,V,Q,0,Z,Z,0,U) [B >= 1 + A && 0 >= V && 0 >= Z] (1,1) 11. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f13(1 + A,B,1,D,E,F,G,V,W,X,Y,E,V,V,V,Q,Q,1,1,0,U) [0 >= V && B >= 1 + A] (?,1) 12. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f13(A,B,C,W,E,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,0) [0 >= W] (1,1) 13. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f13(A,B,C,W,E,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,0) [W >= 1] (1,1) Signature: {(f0,21);(f13,21);(f37,21);(f45,21);(f52,21);(f54,21);(f57,21)} Flow Graph: [0->{5,6},1->{5,6},2->{5,6},3->{3},4->{},5->{3},6->{3},7->{5,6},8->{5,6},9->{1,2,7},10->{1,2,7},11->{0,8,9 ,10,11},12->{0,8,9,10,11},13->{0,8,9,10,11}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(9,2),(10,1),(10,7)] * Step 3: UnreachableRules MAYBE + Considered Problem: Rules: 0. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [A >= B] (1,1) 1. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [C >= 3] (1,1) 2. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [1 >= C] (1,1) 3. f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) True (?,1) 4. f54(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f57(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) True (1,1) 5. f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f52(A,B,C,D,0,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [D >= 1] (1,1) 6. f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f52(A,B,C,D,0,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [0 >= D] (1,1) 7. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f45(A,B,2,D,1 + E,F,H,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [C = 2] (1,1) 8. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f45(A,B,C,D,E,F,G,V,W,X,Y,E,V,V,O,P,Q,R,S,T,U) [V >= 1 && B >= 1 + A] (1,1) 9. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f37(A,B,Z,D,E,F,G,V,W,X,Y,E,V,V,V,Q,0,Z,Z,0,U) [B >= 1 + A && 0 >= V && Z >= 2] (1,1) 10. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f37(A,B,Z,D,E,F,G,V,W,X,Y,E,V,V,V,Q,0,Z,Z,0,U) [B >= 1 + A && 0 >= V && 0 >= Z] (1,1) 11. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f13(1 + A,B,1,D,E,F,G,V,W,X,Y,E,V,V,V,Q,Q,1,1,0,U) [0 >= V && B >= 1 + A] (?,1) 12. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f13(A,B,C,W,E,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,0) [0 >= W] (1,1) 13. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f13(A,B,C,W,E,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,0) [W >= 1] (1,1) Signature: {(f0,21);(f13,21);(f37,21);(f45,21);(f52,21);(f54,21);(f57,21)} Flow Graph: [0->{5,6},1->{5,6},2->{5,6},3->{3},4->{},5->{3},6->{3},7->{5,6},8->{5,6},9->{1,7},10->{2},11->{0,8,9,10 ,11},12->{0,8,9,10,11},13->{0,8,9,10,11}] + Applied Processor: UnreachableRules + Details: Following transitions are not reachable from the starting states and are revomed: [4] * Step 4: AddSinks MAYBE + Considered Problem: Rules: 0. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [A >= B] (1,1) 1. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [C >= 3] (1,1) 2. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [1 >= C] (1,1) 3. f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) True (?,1) 5. f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f52(A,B,C,D,0,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [D >= 1] (1,1) 6. f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f52(A,B,C,D,0,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [0 >= D] (1,1) 7. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f45(A,B,2,D,1 + E,F,H,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [C = 2] (1,1) 8. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f45(A,B,C,D,E,F,G,V,W,X,Y,E,V,V,O,P,Q,R,S,T,U) [V >= 1 && B >= 1 + A] (1,1) 9. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f37(A,B,Z,D,E,F,G,V,W,X,Y,E,V,V,V,Q,0,Z,Z,0,U) [B >= 1 + A && 0 >= V && Z >= 2] (1,1) 10. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f37(A,B,Z,D,E,F,G,V,W,X,Y,E,V,V,V,Q,0,Z,Z,0,U) [B >= 1 + A && 0 >= V && 0 >= Z] (1,1) 11. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f13(1 + A,B,1,D,E,F,G,V,W,X,Y,E,V,V,V,Q,Q,1,1,0,U) [0 >= V && B >= 1 + A] (?,1) 12. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f13(A,B,C,W,E,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,0) [0 >= W] (1,1) 13. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f13(A,B,C,W,E,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,0) [W >= 1] (1,1) Signature: {(f0,21);(f13,21);(f37,21);(f45,21);(f52,21);(f54,21);(f57,21)} Flow Graph: [0->{5,6},1->{5,6},2->{5,6},3->{3},5->{3},6->{3},7->{5,6},8->{5,6},9->{1,7},10->{2},11->{0,8,9,10,11} ,12->{0,8,9,10,11},13->{0,8,9,10,11}] + Applied Processor: AddSinks + Details: () * Step 5: UnsatPaths MAYBE + Considered Problem: Rules: 0. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [A >= B] (?,1) 1. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [C >= 3] (?,1) 2. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [1 >= C] (?,1) 3. f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) True (?,1) 5. f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f52(A,B,C,D,0,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [D >= 1] (?,1) 6. f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f52(A,B,C,D,0,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [0 >= D] (?,1) 7. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f45(A,B,2,D,1 + E,F,H,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [C = 2] (?,1) 8. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f45(A,B,C,D,E,F,G,V,W,X,Y,E,V,V,O,P,Q,R,S,T,U) [V >= 1 && B >= 1 + A] (?,1) 9. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f37(A,B,Z,D,E,F,G,V,W,X,Y,E,V,V,V,Q,0,Z,Z,0,U) [B >= 1 + A && 0 >= V && Z >= 2] (?,1) 10. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f37(A,B,Z,D,E,F,G,V,W,X,Y,E,V,V,V,Q,0,Z,Z,0,U) [B >= 1 + A && 0 >= V && 0 >= Z] (?,1) 11. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f13(1 + A,B,1,D,E,F,G,V,W,X,Y,E,V,V,V,Q,Q,1,1,0,U) [0 >= V && B >= 1 + A] (?,1) 12. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f13(A,B,C,W,E,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,0) [0 >= W] (1,1) 13. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f13(A,B,C,W,E,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,0) [W >= 1] (1,1) 14. f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) True (?,1) Signature: {(exitus616,21);(f0,21);(f13,21);(f37,21);(f45,21);(f52,21);(f54,21);(f57,21)} Flow Graph: [0->{5,6},1->{5,6},2->{5,6},3->{3,14},5->{3,14},6->{3,14},7->{5,6},8->{5,6},9->{1,2,7},10->{1,2,7},11->{0 ,8,9,10,11},12->{0,8,9,10,11},13->{0,8,9,10,11},14->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(9,2),(10,1),(10,7)] * Step 6: Failure MAYBE + Considered Problem: Rules: 0. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [A >= B] (?,1) 1. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [C >= 3] (?,1) 2. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [1 >= C] (?,1) 3. f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) True (?,1) 5. f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f52(A,B,C,D,0,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [D >= 1] (?,1) 6. f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f52(A,B,C,D,0,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [0 >= D] (?,1) 7. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f45(A,B,2,D,1 + E,F,H,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [C = 2] (?,1) 8. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f45(A,B,C,D,E,F,G,V,W,X,Y,E,V,V,O,P,Q,R,S,T,U) [V >= 1 && B >= 1 + A] (?,1) 9. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f37(A,B,Z,D,E,F,G,V,W,X,Y,E,V,V,V,Q,0,Z,Z,0,U) [B >= 1 + A && 0 >= V && Z >= 2] (?,1) 10. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f37(A,B,Z,D,E,F,G,V,W,X,Y,E,V,V,V,Q,0,Z,Z,0,U) [B >= 1 + A && 0 >= V && 0 >= Z] (?,1) 11. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f13(1 + A,B,1,D,E,F,G,V,W,X,Y,E,V,V,V,Q,Q,1,1,0,U) [0 >= V && B >= 1 + A] (?,1) 12. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f13(A,B,C,W,E,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,0) [0 >= W] (1,1) 13. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f13(A,B,C,W,E,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,0) [W >= 1] (1,1) 14. f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) True (?,1) Signature: {(exitus616,21);(f0,21);(f13,21);(f37,21);(f45,21);(f52,21);(f54,21);(f57,21)} Flow Graph: [0->{5,6},1->{5,6},2->{5,6},3->{3,14},5->{3,14},6->{3,14},7->{5,6},8->{5,6},9->{1,7},10->{2},11->{0,8,9,10 ,11},12->{0,8,9,10,11},13->{0,8,9,10,11},14->{}] + Applied Processor: LooptreeTransformer + Details: We construct a looptree: P: [0,1,2,3,5,6,7,8,9,10,11,12,13,14] | +- p:[11] c: [11] | `- p:[3] c: [] MAYBE