YES * Step 1: UnsatRules YES + Considered Problem: Rules: 0. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f1(A,1 + B,D,B1,Y,Z,A1,C1,D1,E1,D,F1,B,N,O,P,Q,R,S,T,U,V,W,X) [A >= 1 + B && B >= 0] (?,1) 1. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,U,V,W,X) [B1 >= 1 + N && O >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + B1 && P = 0] (?,1) 2. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,U,V,W,X) [B1 >= 1 + N && O >= 0 && A1 >= 2 && Z >= A1 && B1 >= 1 + Y && P = 0] (?,1) 3. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,U,V,W,X) [N >= 1 + B1 && O >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + B1 && P = 0] (?,1) 4. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,U,V,W,X) [N >= 1 + B1 && O >= 0 && A1 >= 2 && Z >= A1 && B1 >= 1 + Y && P = 0] (?,1) 5. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f4(E1,D1,F1,D,E,F,G,H,G1,J,K,L,M,C1,O,B1,Y,Z,A1,H1,U,V,W,X) [O >= 0 && E1 >= 2 && D1 >= E1 && 0 >= 1 + F1 && P = N] (?,1) 6. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f4(E1,D1,F1,D,E,F,G,H,G1,J,K,L,M,C1,O,B1,Y,Z,A1,H1,U,V,W,X) [O >= 0 && E1 >= 2 && D1 >= E1 && F1 >= 1 && P = N] (?,1) 7. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (?,1) 8. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (?,1) 9. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (?,1) 10. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (?,1) 11. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f4(D1,B,C,D,E,F,G,H,E1,J,K,L,M,C1,O,B1,Y,Z,A1,F1,U,V,W,X) [D1 >= 2 && U >= 0 && P = N] (?,1) 12. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(Y,1 + U,C,D,E,F,G,H,I,J,C,L,M,C,U,0,C,0,C,C,U,V,W,X) [B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1 && 0 >= 1 + C] (?,1) 13. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(Y,1 + U,C,D,E,F,G,H,I,J,C,L,M,C,U,0,C,0,C,C,U,V,W,X) [B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] (?,1) 14. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(Y,1 + U,C,D,E,F,G,H,I,J,C,L,M,C,U,0,C,0,C,C,U,V,W,X) [B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] (?,1) 15. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(Y,1 + U,C,D,E,F,G,H,I,J,C,L,M,C,U,0,C,0,C,C,U,V,W,X) [B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C && C >= 1] (?,1) 16. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f4(D1,0,0,D,E,F,G,H,E1,J,K,L,M,C1,O,B1,Y,Z,A1,F1,U,V,W,X) [0 >= D1 && 0 >= A] (1,1) 17. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f1(A,2,Y,C1,Z,A1,B1,D1,E1,F1,Y,L,M,N,O,P,Q,R,S,T,U,V,W,G1) [A >= 2] (1,1) Signature: {(f1,24);(f10,24);(f3,24);(f4,24);(f9,24)} Flow Graph: [0->{0,12,13,14,15},1->{7,8,9,10,11},2->{7,8,9,10,11},3->{7,8,9,10,11},4->{7,8,9,10,11},5->{},6->{},7->{7 ,8,9,10,11},8->{7,8,9,10,11},9->{7,8,9,10,11},10->{7,8,9,10,11},11->{},12->{7,8,9,10,11},13->{7,8,9,10,11} ,14->{7,8,9,10,11},15->{7,8,9,10,11},16->{},17->{0,12,13,14,15}] + Applied Processor: UnsatRules + Details: Following transitions have unsatisfiable constraints and are removed: [12,15] * Step 2: UnsatPaths YES + Considered Problem: Rules: 0. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f1(A,1 + B,D,B1,Y,Z,A1,C1,D1,E1,D,F1,B,N,O,P,Q,R,S,T,U,V,W,X) [A >= 1 + B && B >= 0] (?,1) 1. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,U,V,W,X) [B1 >= 1 + N && O >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + B1 && P = 0] (?,1) 2. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,U,V,W,X) [B1 >= 1 + N && O >= 0 && A1 >= 2 && Z >= A1 && B1 >= 1 + Y && P = 0] (?,1) 3. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,U,V,W,X) [N >= 1 + B1 && O >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + B1 && P = 0] (?,1) 4. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,U,V,W,X) [N >= 1 + B1 && O >= 0 && A1 >= 2 && Z >= A1 && B1 >= 1 + Y && P = 0] (?,1) 5. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f4(E1,D1,F1,D,E,F,G,H,G1,J,K,L,M,C1,O,B1,Y,Z,A1,H1,U,V,W,X) [O >= 0 && E1 >= 2 && D1 >= E1 && 0 >= 1 + F1 && P = N] (?,1) 6. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f4(E1,D1,F1,D,E,F,G,H,G1,J,K,L,M,C1,O,B1,Y,Z,A1,H1,U,V,W,X) [O >= 0 && E1 >= 2 && D1 >= E1 && F1 >= 1 && P = N] (?,1) 7. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (?,1) 8. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (?,1) 9. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (?,1) 10. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (?,1) 11. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f4(D1,B,C,D,E,F,G,H,E1,J,K,L,M,C1,O,B1,Y,Z,A1,F1,U,V,W,X) [D1 >= 2 && U >= 0 && P = N] (?,1) 13. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(Y,1 + U,C,D,E,F,G,H,I,J,C,L,M,C,U,0,C,0,C,C,U,V,W,X) [B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] (?,1) 14. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(Y,1 + U,C,D,E,F,G,H,I,J,C,L,M,C,U,0,C,0,C,C,U,V,W,X) [B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] (?,1) 16. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f4(D1,0,0,D,E,F,G,H,E1,J,K,L,M,C1,O,B1,Y,Z,A1,F1,U,V,W,X) [0 >= D1 && 0 >= A] (1,1) 17. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f1(A,2,Y,C1,Z,A1,B1,D1,E1,F1,Y,L,M,N,O,P,Q,R,S,T,U,V,W,G1) [A >= 2] (1,1) Signature: {(f1,24);(f10,24);(f3,24);(f4,24);(f9,24)} Flow Graph: [0->{0,13,14},1->{7,8,9,10,11},2->{7,8,9,10,11},3->{7,8,9,10,11},4->{7,8,9,10,11},5->{},6->{},7->{7,8,9,10 ,11},8->{7,8,9,10,11},9->{7,8,9,10,11},10->{7,8,9,10,11},11->{},13->{7,8,9,10,11},14->{7,8,9,10,11},16->{} ,17->{0,13,14}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(13,11),(14,11)] * Step 3: UnreachableRules YES + Considered Problem: Rules: 0. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f1(A,1 + B,D,B1,Y,Z,A1,C1,D1,E1,D,F1,B,N,O,P,Q,R,S,T,U,V,W,X) [A >= 1 + B && B >= 0] (?,1) 1. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,U,V,W,X) [B1 >= 1 + N && O >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + B1 && P = 0] (?,1) 2. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,U,V,W,X) [B1 >= 1 + N && O >= 0 && A1 >= 2 && Z >= A1 && B1 >= 1 + Y && P = 0] (?,1) 3. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,U,V,W,X) [N >= 1 + B1 && O >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + B1 && P = 0] (?,1) 4. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,U,V,W,X) [N >= 1 + B1 && O >= 0 && A1 >= 2 && Z >= A1 && B1 >= 1 + Y && P = 0] (?,1) 5. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f4(E1,D1,F1,D,E,F,G,H,G1,J,K,L,M,C1,O,B1,Y,Z,A1,H1,U,V,W,X) [O >= 0 && E1 >= 2 && D1 >= E1 && 0 >= 1 + F1 && P = N] (?,1) 6. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f4(E1,D1,F1,D,E,F,G,H,G1,J,K,L,M,C1,O,B1,Y,Z,A1,H1,U,V,W,X) [O >= 0 && E1 >= 2 && D1 >= E1 && F1 >= 1 && P = N] (?,1) 7. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (?,1) 8. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (?,1) 9. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (?,1) 10. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (?,1) 11. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f4(D1,B,C,D,E,F,G,H,E1,J,K,L,M,C1,O,B1,Y,Z,A1,F1,U,V,W,X) [D1 >= 2 && U >= 0 && P = N] (?,1) 13. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(Y,1 + U,C,D,E,F,G,H,I,J,C,L,M,C,U,0,C,0,C,C,U,V,W,X) [B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] (?,1) 14. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(Y,1 + U,C,D,E,F,G,H,I,J,C,L,M,C,U,0,C,0,C,C,U,V,W,X) [B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] (?,1) 16. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f4(D1,0,0,D,E,F,G,H,E1,J,K,L,M,C1,O,B1,Y,Z,A1,F1,U,V,W,X) [0 >= D1 && 0 >= A] (1,1) 17. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f1(A,2,Y,C1,Z,A1,B1,D1,E1,F1,Y,L,M,N,O,P,Q,R,S,T,U,V,W,G1) [A >= 2] (1,1) Signature: {(f1,24);(f10,24);(f3,24);(f4,24);(f9,24)} Flow Graph: [0->{0,13,14},1->{7,8,9,10,11},2->{7,8,9,10,11},3->{7,8,9,10,11},4->{7,8,9,10,11},5->{},6->{},7->{7,8,9,10 ,11},8->{7,8,9,10,11},9->{7,8,9,10,11},10->{7,8,9,10,11},11->{},13->{7,8,9,10},14->{7,8,9,10},16->{},17->{0 ,13,14}] + Applied Processor: UnreachableRules + Details: Following transitions are not reachable from the starting states and are revomed: [1,2,3,4,5,6] * Step 4: FromIts YES + Considered Problem: Rules: 0. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f1(A,1 + B,D,B1,Y,Z,A1,C1,D1,E1,D,F1,B,N,O,P,Q,R,S,T,U,V,W,X) [A >= 1 + B && B >= 0] (?,1) 7. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (?,1) 8. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (?,1) 9. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (?,1) 10. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (?,1) 11. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f4(D1,B,C,D,E,F,G,H,E1,J,K,L,M,C1,O,B1,Y,Z,A1,F1,U,V,W,X) [D1 >= 2 && U >= 0 && P = N] (?,1) 13. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(Y,1 + U,C,D,E,F,G,H,I,J,C,L,M,C,U,0,C,0,C,C,U,V,W,X) [B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] (?,1) 14. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(Y,1 + U,C,D,E,F,G,H,I,J,C,L,M,C,U,0,C,0,C,C,U,V,W,X) [B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] (?,1) 16. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f4(D1,0,0,D,E,F,G,H,E1,J,K,L,M,C1,O,B1,Y,Z,A1,F1,U,V,W,X) [0 >= D1 && 0 >= A] (1,1) 17. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f1(A,2,Y,C1,Z,A1,B1,D1,E1,F1,Y,L,M,N,O,P,Q,R,S,T,U,V,W,G1) [A >= 2] (1,1) Signature: {(f1,24);(f10,24);(f3,24);(f4,24);(f9,24)} Flow Graph: [0->{0,13,14},7->{7,8,9,10,11},8->{7,8,9,10,11},9->{7,8,9,10,11},10->{7,8,9,10,11},11->{},13->{7,8,9,10} ,14->{7,8,9,10},16->{},17->{0,13,14}] + Applied Processor: FromIts + Details: () * Step 5: Decompose YES + Considered Problem: Rules: f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f1(A,1 + B,D,B1,Y,Z,A1,C1,D1,E1,D,F1,B,N,O,P,Q,R ,S,T,U,V,W ,X) [A >= 1 + B && B >= 0] f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U ,B1,-1 + U ,X) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U ,B1,-1 + U ,X) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U ,B1,-1 + U ,X) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U ,B1,-1 + U ,X) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f4(D1,B,C,D,E,F,G,H,E1,J,K,L,M,C1,O,B1,Y,Z,A1,F1,U ,V,W ,X) [D1 >= 2 && U >= 0 && P = N] f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(Y,1 + U,C,D,E,F,G,H,I,J,C,L,M,C,U,0,C,0,C,C,U,V ,W ,X) [B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(Y,1 + U,C,D,E,F,G,H,I,J,C,L,M,C,U,0,C,0,C,C,U,V ,W ,X) [B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f4(D1,0,0,D,E,F,G,H,E1,J,K,L,M,C1,O,B1,Y,Z,A1,F1,U ,V,W ,X) [0 >= D1 && 0 >= A] f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f1(A,2,Y,C1,Z,A1,B1,D1,E1,F1,Y,L,M,N,O,P,Q,R,S,T,U ,V,W ,G1) [A >= 2] Signature: {(f1,24);(f10,24);(f3,24);(f4,24);(f9,24)} Rule Graph: [0->{0,13,14},7->{7,8,9,10,11},8->{7,8,9,10,11},9->{7,8,9,10,11},10->{7,8,9,10,11},11->{},13->{7,8,9,10} ,14->{7,8,9,10},16->{},17->{0,13,14}] + Applied Processor: Decompose NoGreedy + Details: We construct a looptree: P: [0,7,8,9,10,11,13,14,16,17] | +- p:[0] c: [0] | `- p:[7,8,9,10] c: [10] | `- p:[7,8,9] c: [9] | `- p:[7,8] c: [8] | `- p:[7] c: [7] * Step 6: CloseWith YES + Considered Problem: (Rules: f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f1(A,1 + B,D,B1,Y,Z,A1,C1,D1,E1,D,F1,B,N,O,P,Q,R ,S,T,U,V,W ,X) [A >= 1 + B && B >= 0] f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U ,B1,-1 + U ,X) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U ,B1,-1 + U ,X) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U ,B1,-1 + U ,X) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U ,B1,-1 + U ,X) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f4(D1,B,C,D,E,F,G,H,E1,J,K,L,M,C1,O,B1,Y,Z,A1,F1,U ,V,W ,X) [D1 >= 2 && U >= 0 && P = N] f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(Y,1 + U,C,D,E,F,G,H,I,J,C,L,M,C,U,0,C,0,C,C,U,V ,W ,X) [B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(Y,1 + U,C,D,E,F,G,H,I,J,C,L,M,C,U,0,C,0,C,C,U,V ,W ,X) [B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f4(D1,0,0,D,E,F,G,H,E1,J,K,L,M,C1,O,B1,Y,Z,A1,F1,U ,V,W ,X) [0 >= D1 && 0 >= A] f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f1(A,2,Y,C1,Z,A1,B1,D1,E1,F1,Y,L,M,N,O,P,Q,R,S,T,U ,V,W ,G1) [A >= 2] Signature: {(f1,24);(f10,24);(f3,24);(f4,24);(f9,24)} Rule Graph: [0->{0,13,14},7->{7,8,9,10,11},8->{7,8,9,10,11},9->{7,8,9,10,11},10->{7,8,9,10,11},11->{},13->{7,8,9,10} ,14->{7,8,9,10},16->{},17->{0,13,14}] ,We construct a looptree: P: [0,7,8,9,10,11,13,14,16,17] | +- p:[0] c: [0] | `- p:[7,8,9,10] c: [10] | `- p:[7,8,9] c: [9] | `- p:[7,8] c: [8] | `- p:[7] c: [7]) + Applied Processor: CloseWith True + Details: () YES