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,V,W) -> f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [A >= B] (?,1) 1. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [C >= 3] (?,1) 2. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [1 >= C] (?,1) 3. f54(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f54(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) True (?,1) 4. f56(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) True (?,1) 5. f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f54(A,B,C,D,0,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [D >= 1] (?,1) 6. f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f54(A,B,C,D,0,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [0 >= D] (?,1) 7. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f47(A,B,2,D,1 + E,F,H,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [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,V,W) -> f47(A,B,C,D,E,F,G,X,Y,Z,A1,E,X,X,X,P,Q,R,S,T,U,V,W) [X >= 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,V,W) -> f39(A,B,B1,D,E,F,G,X,Y,Z,A1,E,X,X,X,X,R,0,B1,B1,B1,0,W) [B >= 1 + A && 0 >= X && B1 >= 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,V,W) -> f39(A,B,B1,D,E,F,G,X,Y,Z,A1,E,X,X,X,X,R,0,B1,B1,B1,0,W) [B >= 1 + A && 0 >= X && 0 >= B1] (?,1) 11. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f13(1 + A,B,1,D,E,F,G,X,Y,Z,A1,E,X,X,X,X,R,R,1,1,1,0,W) [0 >= X && 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,V,W) -> f13(A,B,C,Y,E,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,0) [0 >= Y] (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,V,W) -> f13(A,B,C,Y,E,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,0) [Y >= 1] (1,1) Signature: {(f0,23);(f13,23);(f39,23);(f47,23);(f54,23);(f56,23);(f59,23)} 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,V,W) -> f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [A >= B] (1,1) 1. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [C >= 3] (1,1) 2. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [1 >= C] (1,1) 3. f54(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f54(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) True (?,1) 4. f56(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) True (1,1) 5. f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f54(A,B,C,D,0,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [D >= 1] (1,1) 6. f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f54(A,B,C,D,0,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [0 >= D] (1,1) 7. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f47(A,B,2,D,1 + E,F,H,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [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,V,W) -> f47(A,B,C,D,E,F,G,X,Y,Z,A1,E,X,X,X,P,Q,R,S,T,U,V,W) [X >= 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,V,W) -> f39(A,B,B1,D,E,F,G,X,Y,Z,A1,E,X,X,X,X,R,0,B1,B1,B1,0,W) [B >= 1 + A && 0 >= X && B1 >= 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,V,W) -> f39(A,B,B1,D,E,F,G,X,Y,Z,A1,E,X,X,X,X,R,0,B1,B1,B1,0,W) [B >= 1 + A && 0 >= X && 0 >= B1] (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,V,W) -> f13(1 + A,B,1,D,E,F,G,X,Y,Z,A1,E,X,X,X,X,R,R,1,1,1,0,W) [0 >= X && 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,V,W) -> f13(A,B,C,Y,E,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,0) [0 >= Y] (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,V,W) -> f13(A,B,C,Y,E,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,0) [Y >= 1] (1,1) Signature: {(f0,23);(f13,23);(f39,23);(f47,23);(f54,23);(f56,23);(f59,23)} 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,V,W) -> f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [A >= B] (1,1) 1. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [C >= 3] (1,1) 2. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [1 >= C] (1,1) 3. f54(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f54(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) True (?,1) 4. f56(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) True (1,1) 5. f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f54(A,B,C,D,0,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [D >= 1] (1,1) 6. f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f54(A,B,C,D,0,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [0 >= D] (1,1) 7. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f47(A,B,2,D,1 + E,F,H,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [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,V,W) -> f47(A,B,C,D,E,F,G,X,Y,Z,A1,E,X,X,X,P,Q,R,S,T,U,V,W) [X >= 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,V,W) -> f39(A,B,B1,D,E,F,G,X,Y,Z,A1,E,X,X,X,X,R,0,B1,B1,B1,0,W) [B >= 1 + A && 0 >= X && B1 >= 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,V,W) -> f39(A,B,B1,D,E,F,G,X,Y,Z,A1,E,X,X,X,X,R,0,B1,B1,B1,0,W) [B >= 1 + A && 0 >= X && 0 >= B1] (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,V,W) -> f13(1 + A,B,1,D,E,F,G,X,Y,Z,A1,E,X,X,X,X,R,R,1,1,1,0,W) [0 >= X && 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,V,W) -> f13(A,B,C,Y,E,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,0) [0 >= Y] (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,V,W) -> f13(A,B,C,Y,E,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,0) [Y >= 1] (1,1) Signature: {(f0,23);(f13,23);(f39,23);(f47,23);(f54,23);(f56,23);(f59,23)} 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,V,W) -> f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [A >= B] (1,1) 1. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [C >= 3] (1,1) 2. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [1 >= C] (1,1) 3. f54(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f54(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) True (?,1) 5. f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f54(A,B,C,D,0,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [D >= 1] (1,1) 6. f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f54(A,B,C,D,0,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [0 >= D] (1,1) 7. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f47(A,B,2,D,1 + E,F,H,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [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,V,W) -> f47(A,B,C,D,E,F,G,X,Y,Z,A1,E,X,X,X,P,Q,R,S,T,U,V,W) [X >= 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,V,W) -> f39(A,B,B1,D,E,F,G,X,Y,Z,A1,E,X,X,X,X,R,0,B1,B1,B1,0,W) [B >= 1 + A && 0 >= X && B1 >= 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,V,W) -> f39(A,B,B1,D,E,F,G,X,Y,Z,A1,E,X,X,X,X,R,0,B1,B1,B1,0,W) [B >= 1 + A && 0 >= X && 0 >= B1] (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,V,W) -> f13(1 + A,B,1,D,E,F,G,X,Y,Z,A1,E,X,X,X,X,R,R,1,1,1,0,W) [0 >= X && 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,V,W) -> f13(A,B,C,Y,E,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,0) [0 >= Y] (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,V,W) -> f13(A,B,C,Y,E,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,0) [Y >= 1] (1,1) Signature: {(f0,23);(f13,23);(f39,23);(f47,23);(f54,23);(f56,23);(f59,23)} 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,V,W) -> f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [A >= B] (?,1) 1. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [C >= 3] (?,1) 2. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [1 >= C] (?,1) 3. f54(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f54(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) True (?,1) 5. f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f54(A,B,C,D,0,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [D >= 1] (?,1) 6. f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f54(A,B,C,D,0,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [0 >= D] (?,1) 7. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f47(A,B,2,D,1 + E,F,H,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [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,V,W) -> f47(A,B,C,D,E,F,G,X,Y,Z,A1,E,X,X,X,P,Q,R,S,T,U,V,W) [X >= 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,V,W) -> f39(A,B,B1,D,E,F,G,X,Y,Z,A1,E,X,X,X,X,R,0,B1,B1,B1,0,W) [B >= 1 + A && 0 >= X && B1 >= 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,V,W) -> f39(A,B,B1,D,E,F,G,X,Y,Z,A1,E,X,X,X,X,R,0,B1,B1,B1,0,W) [B >= 1 + A && 0 >= X && 0 >= B1] (?,1) 11. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f13(1 + A,B,1,D,E,F,G,X,Y,Z,A1,E,X,X,X,X,R,R,1,1,1,0,W) [0 >= X && 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,V,W) -> f13(A,B,C,Y,E,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,0) [0 >= Y] (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,V,W) -> f13(A,B,C,Y,E,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,0) [Y >= 1] (1,1) 14. f54(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) True (?,1) Signature: {(exitus616,23);(f0,23);(f13,23);(f39,23);(f47,23);(f54,23);(f56,23);(f59,23)} 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,V,W) -> f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [A >= B] (?,1) 1. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [C >= 3] (?,1) 2. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [1 >= C] (?,1) 3. f54(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f54(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) True (?,1) 5. f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f54(A,B,C,D,0,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [D >= 1] (?,1) 6. f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f54(A,B,C,D,0,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [0 >= D] (?,1) 7. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f47(A,B,2,D,1 + E,F,H,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [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,V,W) -> f47(A,B,C,D,E,F,G,X,Y,Z,A1,E,X,X,X,P,Q,R,S,T,U,V,W) [X >= 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,V,W) -> f39(A,B,B1,D,E,F,G,X,Y,Z,A1,E,X,X,X,X,R,0,B1,B1,B1,0,W) [B >= 1 + A && 0 >= X && B1 >= 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,V,W) -> f39(A,B,B1,D,E,F,G,X,Y,Z,A1,E,X,X,X,X,R,0,B1,B1,B1,0,W) [B >= 1 + A && 0 >= X && 0 >= B1] (?,1) 11. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f13(1 + A,B,1,D,E,F,G,X,Y,Z,A1,E,X,X,X,X,R,R,1,1,1,0,W) [0 >= X && 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,V,W) -> f13(A,B,C,Y,E,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,0) [0 >= Y] (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,V,W) -> f13(A,B,C,Y,E,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,0) [Y >= 1] (1,1) 14. f54(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) True (?,1) Signature: {(exitus616,23);(f0,23);(f13,23);(f39,23);(f47,23);(f54,23);(f56,23);(f59,23)} 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