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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(D,O1,P1,D,0,M1,Q1,R1,S1,T1,U1,C,C,C,N1,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [A >= B && A >= 0 && M1 >= 2 && 0 >= 1 + C && N1 >= M1 && D >= M1 && E = 0] (?,1) 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(D,O1,P1,D,0,M1,Q1,R1,S1,T1,U1,C,C,C,N1,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [A >= B && A >= 0 && M1 >= 2 && C >= 1 && N1 >= M1 && D >= M1 && E = 0] (?,1) 2. 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f1(1 + A,B,K,D,E,F,G,H,I,K,M1,L,M,N,O,O1,A,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [B >= 1 + A && A >= 0] (?,1) 3. 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,D,1,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,1 + D,Q1,D,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [A >= 0 && M1 >= 2 && 0 >= 1 + N && R1 >= M1 && 0 >= 1 + O1 && E = 1] (?,1) 4. 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,D,1,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,1 + D,Q1,D,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [A >= 0 && M1 >= 2 && 0 >= 1 + N && R1 >= M1 && O1 >= 1 && E = 1] (?,1) 5. 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,D,1,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,1 + D,Q1,D,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [A >= 0 && M1 >= 2 && N >= 1 && R1 >= M1 && 0 >= 1 + O1 && E = 1] (?,1) 6. 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,D,1,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,1 + D,Q1,D,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [A >= 0 && M1 >= 2 && N >= 1 && R1 >= M1 && O1 >= 1 && E = 1] (?,1) 7. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,D,E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,R,S,T,U,P1,Q1,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [U >= 0 && M1 >= 2 && 0 >= 1 + N && 0 >= 1 + O1 && 0 >= 1 + Q1] (?,1) 8. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,D,E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,R,S,T,U,P1,Q1,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [U >= 0 && M1 >= 2 && 0 >= 1 + N && 0 >= 1 + O1 && Q1 >= 1] (?,1) 9. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,D,E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,R,S,T,U,P1,Q1,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [U >= 0 && M1 >= 2 && 0 >= 1 + N && O1 >= 1 && 0 >= 1 + Q1] (?,1) 10. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,D,E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,R,S,T,U,P1,Q1,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [U >= 0 && M1 >= 2 && 0 >= 1 + N && O1 >= 1 && Q1 >= 1] (?,1) 11. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,D,E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,R,S,T,U,P1,Q1,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [U >= 0 && M1 >= 2 && N >= 1 && 0 >= 1 + O1 && 0 >= 1 + Q1] (?,1) 12. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,D,E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,R,S,T,U,P1,Q1,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [U >= 0 && M1 >= 2 && N >= 1 && 0 >= 1 + O1 && Q1 >= 1] (?,1) 13. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,D,E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,R,S,T,U,P1,Q1,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [U >= 0 && M1 >= 2 && N >= 1 && O1 >= 1 && 0 >= 1 + Q1] (?,1) 14. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,D,E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,R,S,T,U,P1,Q1,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [U >= 0 && M1 >= 2 && N >= 1 && O1 >= 1 && Q1 >= 1] (?,1) 15. f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[E >= 0 && D >= 0 && M1 >= 2 && 0 >= 1 + R1 && 0 >= 1 + O1 && 0 >= 1 + Q1] (?,1) ,J1,K1,L1) 16. f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[E >= 0 && D >= 0 && M1 >= 2 && 0 >= 1 + R1 && 0 >= 1 + O1 && Q1 >= 1] (?,1) ,J1,K1,L1) 17. f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[E >= 0 && D >= 0 && M1 >= 2 && 0 >= 1 + R1 && O1 >= 1 && 0 >= 1 + Q1] (?,1) ,J1,K1,L1) 18. f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[E >= 0 && D >= 0 && M1 >= 2 && 0 >= 1 + R1 && O1 >= 1 && Q1 >= 1] (?,1) ,J1,K1,L1) 19. f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[E >= 0 && D >= 0 && M1 >= 2 && R1 >= 1 && 0 >= 1 + O1 && 0 >= 1 + Q1] (?,1) ,J1,K1,L1) 20. f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[E >= 0 && D >= 0 && M1 >= 2 && R1 >= 1 && 0 >= 1 + O1 && Q1 >= 1] (?,1) ,J1,K1,L1) 21. f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[E >= 0 && D >= 0 && M1 >= 2 && R1 >= 1 && O1 >= 1 && 0 >= 1 + Q1] (?,1) ,J1,K1,L1) 22. f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[E >= 0 && D >= 0 && M1 >= 2 && R1 >= 1 && O1 >= 1 && Q1 >= 1] (?,1) ,J1,K1,L1) 23. f7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,I1,J1,K1,L1) [P1 >= 1 + B1 && C1 >= 0 && M1 >= 2 && O1 >= 1 + P1 && 0 >= 1 + O1 && D1 = 0] (?,1) 24. f7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,I1,J1,K1,L1) [P1 >= 1 + B1 && C1 >= 0 && M1 >= 2 && O1 >= 1 + P1 && O1 >= 1 && D1 = 0] (?,1) 25. f7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,I1,J1,K1,L1) [P1 >= 1 + B1 && C1 >= 0 && M1 >= 2 && P1 >= 1 + O1 && 0 >= 1 + O1 && D1 = 0] (?,1) 26. f7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,I1,J1,K1,L1) [P1 >= 1 + B1 && C1 >= 0 && M1 >= 2 && P1 >= 1 + O1 && O1 >= 1 && D1 = 0] (?,1) 27. f7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,I1,J1,K1,L1) [B1 >= 1 + P1 && C1 >= 0 && M1 >= 2 && O1 >= 1 + P1 && 0 >= 1 + O1 && D1 = 0] (?,1) 28. f7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,I1,J1,K1,L1) [B1 >= 1 + P1 && C1 >= 0 && M1 >= 2 && O1 >= 1 + P1 && O1 >= 1 && D1 = 0] (?,1) 29. f7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,I1,J1,K1,L1) [B1 >= 1 + P1 && C1 >= 0 && M1 >= 2 && P1 >= 1 + O1 && 0 >= 1 + O1 && D1 = 0] (?,1) 30. f7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,I1,J1,K1,L1) [B1 >= 1 + P1 && C1 >= 0 && M1 >= 2 && P1 >= 1 + O1 && O1 >= 1 && D1 = 0] (?,1) 31. f7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f16(A,B,C,D,E,M1,G,O1,I,J,K,P1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,U1,C1,T1,Q1,R1,S1,N1,I1,J1,K1,L1) [C1 >= 0 && 0 >= 1 + P1 && M1 >= 2 && D1 = B1] (?,1) 32. f7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f16(A,B,C,D,E,M1,G,O1,I,J,K,P1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,U1,C1,T1,Q1,R1,S1,N1,I1,J1,K1,L1) [C1 >= 0 && P1 >= 1 && M1 >= 2 && D1 = B1] (?,1) 33. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [Q1 >= 1 + B1 && I1 >= 0 && M1 >= 2 && O1 >= 1 + Q1 && 0 >= 1 + O1 && D1 = 0] (?,1) 34. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [Q1 >= 1 + B1 && I1 >= 0 && M1 >= 2 && O1 >= 1 + Q1 && O1 >= 1 && D1 = 0] (?,1) 35. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [Q1 >= 1 + B1 && I1 >= 0 && M1 >= 2 && Q1 >= 1 + O1 && 0 >= 1 + O1 && D1 = 0] (?,1) 36. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [Q1 >= 1 + B1 && I1 >= 0 && M1 >= 2 && Q1 >= 1 + O1 && O1 >= 1 && D1 = 0] (?,1) 37. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [B1 >= 1 + Q1 && I1 >= 0 && M1 >= 2 && O1 >= 1 + Q1 && 0 >= 1 + O1 && D1 = 0] (?,1) 38. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [B1 >= 1 + Q1 && I1 >= 0 && M1 >= 2 && O1 >= 1 + Q1 && O1 >= 1 && D1 = 0] (?,1) 39. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [B1 >= 1 + Q1 && I1 >= 0 && M1 >= 2 && Q1 >= 1 + O1 && 0 >= 1 + O1 && D1 = 0] (?,1) 40. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [B1 >= 1 + Q1 && I1 >= 0 && M1 >= 2 && Q1 >= 1 + O1 && O1 >= 1 && D1 = 0] (?,1) 41. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f16(A,B,C,D,E,M1,G,O1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,T1,C1,S1,P1,Q1,R1,U1,I1,J1,K1,L1) [M1 >= 2 && I1 >= 0 && D1 = B1] (?,1) 42. f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f1(2,O1,P1,D,E,O1,G,H,P1,P1,Q1,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,M1,R1) [O1 >= 2] (1,1) 43. f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f16(R1,P1,Q1,D,E,O1,S1,T1,U1,N1,Y1,0,Z1,A2,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,F2,C1,E2,B2,C2,D2,G2,I1,J1,M1,L1) [0 >= V1 && 0 >= W1 && 0 >= O1 && 0 >= X1] (1,1) 44. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,1 + I1,M1,G,H,I,J,K,L,O1,P1,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,L,I1,0,L,0,L,L,I1,J1,K1,L1) [Q1 >= 2 && M1 >= 2 && U >= 0 && L >= 1 && 0 >= 1 + L && N = 0 && E = 1] (?,1) 45. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,1 + I1,M1,G,H,I,J,K,L,O1,P1,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,L,I1,0,L,0,L,L,I1,J1,K1,L1) [Q1 >= 2 && M1 >= 2 && U >= 0 && L >= 1 && N = 0 && E = 1] (?,1) 46. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,1 + I1,M1,G,H,I,J,K,L,O1,P1,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,L,I1,0,L,0,L,L,I1,J1,K1,L1) [Q1 >= 2 && M1 >= 2 && U >= 0 && 0 >= 1 + L && N = 0 && E = 1] (?,1) 47. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,1 + I1,M1,G,H,I,J,K,L,O1,P1,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,L,I1,0,L,0,L,L,I1,J1,K1,L1) [Q1 >= 2 && M1 >= 2 && U >= 0 && 0 >= 1 + L && L >= 1 && N = 0 && E = 1] (?,1) 48. f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,1 + I1,M1,G,H,I,J,K,L,O1,P1,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,L,I1,0,L,0,L,L,I1,J1,K1,L1) [Q1 >= 2 && M1 >= 2 && D >= 0 && E >= 0 && L >= 1 && 0 >= 1 + L && N = 0] (?,1) 49. f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,1 + I1,M1,G,H,I,J,K,L,O1,P1,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,L,I1,0,L,0,L,L,I1,J1,K1,L1) [Q1 >= 2 && M1 >= 2 && D >= 0 && E >= 0 && L >= 1 && N = 0] (?,1) 50. f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,1 + I1,M1,G,H,I,J,K,L,O1,P1,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,L,I1,0,L,0,L,L,I1,J1,K1,L1) [Q1 >= 2 && M1 >= 2 && D >= 0 && E >= 0 && 0 >= 1 + L && N = 0] (?,1) 51. f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,1 + I1,M1,G,H,I,J,K,L,O1,P1,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,L,I1,0,L,0,L,L,I1,J1,K1,L1) [Q1 >= 2 && M1 >= 2 && D >= 0 && E >= 0 && 0 >= 1 + L && L >= 1 && N = 0] (?,1) Signature: {(f1,38);(f10,38);(f11,38);(f14,38);(f15,38);(f16,38);(f7,38);(f8,38)} Flow Graph: [0->{15,16,17,18,19,20,21,22,48,49,50,51},1->{15,16,17,18,19,20,21,22,48,49,50,51},2->{0,1,2},3->{15,16,17 ,18,19,20,21,22,48,49,50,51},4->{15,16,17,18,19,20,21,22,48,49,50,51},5->{15,16,17,18,19,20,21,22,48,49,50 ,51},6->{15,16,17,18,19,20,21,22,48,49,50,51},7->{15,16,17,18,19,20,21,22,48,49,50,51},8->{15,16,17,18,19,20 ,21,22,48,49,50,51},9->{15,16,17,18,19,20,21,22,48,49,50,51},10->{15,16,17,18,19,20,21,22,48,49,50,51} ,11->{15,16,17,18,19,20,21,22,48,49,50,51},12->{15,16,17,18,19,20,21,22,48,49,50,51},13->{15,16,17,18,19,20 ,21,22,48,49,50,51},14->{15,16,17,18,19,20,21,22,48,49,50,51},15->{15,16,17,18,19,20,21,22,48,49,50,51} ,16->{15,16,17,18,19,20,21,22,48,49,50,51},17->{15,16,17,18,19,20,21,22,48,49,50,51},18->{15,16,17,18,19,20 ,21,22,48,49,50,51},19->{15,16,17,18,19,20,21,22,48,49,50,51},20->{15,16,17,18,19,20,21,22,48,49,50,51} ,21->{15,16,17,18,19,20,21,22,48,49,50,51},22->{15,16,17,18,19,20,21,22,48,49,50,51},23->{33,34,35,36,37,38 ,39,40,41},24->{33,34,35,36,37,38,39,40,41},25->{33,34,35,36,37,38,39,40,41},26->{33,34,35,36,37,38,39,40 ,41},27->{33,34,35,36,37,38,39,40,41},28->{33,34,35,36,37,38,39,40,41},29->{33,34,35,36,37,38,39,40,41} ,30->{33,34,35,36,37,38,39,40,41},31->{},32->{},33->{33,34,35,36,37,38,39,40,41},34->{33,34,35,36,37,38,39 ,40,41},35->{33,34,35,36,37,38,39,40,41},36->{33,34,35,36,37,38,39,40,41},37->{33,34,35,36,37,38,39,40,41} ,38->{33,34,35,36,37,38,39,40,41},39->{33,34,35,36,37,38,39,40,41},40->{33,34,35,36,37,38,39,40,41},41->{} ,42->{0,1,2},43->{},44->{33,34,35,36,37,38,39,40,41},45->{33,34,35,36,37,38,39,40,41},46->{33,34,35,36,37,38 ,39,40,41},47->{33,34,35,36,37,38,39,40,41},48->{33,34,35,36,37,38,39,40,41},49->{33,34,35,36,37,38,39,40 ,41},50->{33,34,35,36,37,38,39,40,41},51->{33,34,35,36,37,38,39,40,41}] + Applied Processor: UnsatRules + Details: Following transitions have unsatisfiable constraints and are removed: [44,47,48,51] * 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(D,O1,P1,D,0,M1,Q1,R1,S1,T1,U1,C,C,C,N1,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [A >= B && A >= 0 && M1 >= 2 && 0 >= 1 + C && N1 >= M1 && D >= M1 && E = 0] (?,1) 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(D,O1,P1,D,0,M1,Q1,R1,S1,T1,U1,C,C,C,N1,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [A >= B && A >= 0 && M1 >= 2 && C >= 1 && N1 >= M1 && D >= M1 && E = 0] (?,1) 2. 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f1(1 + A,B,K,D,E,F,G,H,I,K,M1,L,M,N,O,O1,A,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [B >= 1 + A && A >= 0] (?,1) 3. 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,D,1,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,1 + D,Q1,D,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [A >= 0 && M1 >= 2 && 0 >= 1 + N && R1 >= M1 && 0 >= 1 + O1 && E = 1] (?,1) 4. 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,D,1,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,1 + D,Q1,D,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [A >= 0 && M1 >= 2 && 0 >= 1 + N && R1 >= M1 && O1 >= 1 && E = 1] (?,1) 5. 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,D,1,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,1 + D,Q1,D,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [A >= 0 && M1 >= 2 && N >= 1 && R1 >= M1 && 0 >= 1 + O1 && E = 1] (?,1) 6. 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,D,1,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,1 + D,Q1,D,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [A >= 0 && M1 >= 2 && N >= 1 && R1 >= M1 && O1 >= 1 && E = 1] (?,1) 7. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,D,E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,R,S,T,U,P1,Q1,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [U >= 0 && M1 >= 2 && 0 >= 1 + N && 0 >= 1 + O1 && 0 >= 1 + Q1] (?,1) 8. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,D,E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,R,S,T,U,P1,Q1,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [U >= 0 && M1 >= 2 && 0 >= 1 + N && 0 >= 1 + O1 && Q1 >= 1] (?,1) 9. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,D,E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,R,S,T,U,P1,Q1,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [U >= 0 && M1 >= 2 && 0 >= 1 + N && O1 >= 1 && 0 >= 1 + Q1] (?,1) 10. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,D,E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,R,S,T,U,P1,Q1,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [U >= 0 && M1 >= 2 && 0 >= 1 + N && O1 >= 1 && Q1 >= 1] (?,1) 11. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,D,E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,R,S,T,U,P1,Q1,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [U >= 0 && M1 >= 2 && N >= 1 && 0 >= 1 + O1 && 0 >= 1 + Q1] (?,1) 12. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,D,E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,R,S,T,U,P1,Q1,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [U >= 0 && M1 >= 2 && N >= 1 && 0 >= 1 + O1 && Q1 >= 1] (?,1) 13. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,D,E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,R,S,T,U,P1,Q1,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [U >= 0 && M1 >= 2 && N >= 1 && O1 >= 1 && 0 >= 1 + Q1] (?,1) 14. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,D,E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,R,S,T,U,P1,Q1,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [U >= 0 && M1 >= 2 && N >= 1 && O1 >= 1 && Q1 >= 1] (?,1) 15. f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[E >= 0 && D >= 0 && M1 >= 2 && 0 >= 1 + R1 && 0 >= 1 + O1 && 0 >= 1 + Q1] (?,1) ,J1,K1,L1) 16. f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[E >= 0 && D >= 0 && M1 >= 2 && 0 >= 1 + R1 && 0 >= 1 + O1 && Q1 >= 1] (?,1) ,J1,K1,L1) 17. f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[E >= 0 && D >= 0 && M1 >= 2 && 0 >= 1 + R1 && O1 >= 1 && 0 >= 1 + Q1] (?,1) ,J1,K1,L1) 18. f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[E >= 0 && D >= 0 && M1 >= 2 && 0 >= 1 + R1 && O1 >= 1 && Q1 >= 1] (?,1) ,J1,K1,L1) 19. f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[E >= 0 && D >= 0 && M1 >= 2 && R1 >= 1 && 0 >= 1 + O1 && 0 >= 1 + Q1] (?,1) ,J1,K1,L1) 20. f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[E >= 0 && D >= 0 && M1 >= 2 && R1 >= 1 && 0 >= 1 + O1 && Q1 >= 1] (?,1) ,J1,K1,L1) 21. f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[E >= 0 && D >= 0 && M1 >= 2 && R1 >= 1 && O1 >= 1 && 0 >= 1 + Q1] (?,1) ,J1,K1,L1) 22. f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[E >= 0 && D >= 0 && M1 >= 2 && R1 >= 1 && O1 >= 1 && Q1 >= 1] (?,1) ,J1,K1,L1) 23. f7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,I1,J1,K1,L1) [P1 >= 1 + B1 && C1 >= 0 && M1 >= 2 && O1 >= 1 + P1 && 0 >= 1 + O1 && D1 = 0] (?,1) 24. f7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,I1,J1,K1,L1) [P1 >= 1 + B1 && C1 >= 0 && M1 >= 2 && O1 >= 1 + P1 && O1 >= 1 && D1 = 0] (?,1) 25. f7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,I1,J1,K1,L1) [P1 >= 1 + B1 && C1 >= 0 && M1 >= 2 && P1 >= 1 + O1 && 0 >= 1 + O1 && D1 = 0] (?,1) 26. f7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,I1,J1,K1,L1) [P1 >= 1 + B1 && C1 >= 0 && M1 >= 2 && P1 >= 1 + O1 && O1 >= 1 && D1 = 0] (?,1) 27. f7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,I1,J1,K1,L1) [B1 >= 1 + P1 && C1 >= 0 && M1 >= 2 && O1 >= 1 + P1 && 0 >= 1 + O1 && D1 = 0] (?,1) 28. f7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,I1,J1,K1,L1) [B1 >= 1 + P1 && C1 >= 0 && M1 >= 2 && O1 >= 1 + P1 && O1 >= 1 && D1 = 0] (?,1) 29. f7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,I1,J1,K1,L1) [B1 >= 1 + P1 && C1 >= 0 && M1 >= 2 && P1 >= 1 + O1 && 0 >= 1 + O1 && D1 = 0] (?,1) 30. f7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,I1,J1,K1,L1) [B1 >= 1 + P1 && C1 >= 0 && M1 >= 2 && P1 >= 1 + O1 && O1 >= 1 && D1 = 0] (?,1) 31. f7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f16(A,B,C,D,E,M1,G,O1,I,J,K,P1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,U1,C1,T1,Q1,R1,S1,N1,I1,J1,K1,L1) [C1 >= 0 && 0 >= 1 + P1 && M1 >= 2 && D1 = B1] (?,1) 32. f7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f16(A,B,C,D,E,M1,G,O1,I,J,K,P1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,U1,C1,T1,Q1,R1,S1,N1,I1,J1,K1,L1) [C1 >= 0 && P1 >= 1 && M1 >= 2 && D1 = B1] (?,1) 33. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [Q1 >= 1 + B1 && I1 >= 0 && M1 >= 2 && O1 >= 1 + Q1 && 0 >= 1 + O1 && D1 = 0] (?,1) 34. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [Q1 >= 1 + B1 && I1 >= 0 && M1 >= 2 && O1 >= 1 + Q1 && O1 >= 1 && D1 = 0] (?,1) 35. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [Q1 >= 1 + B1 && I1 >= 0 && M1 >= 2 && Q1 >= 1 + O1 && 0 >= 1 + O1 && D1 = 0] (?,1) 36. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [Q1 >= 1 + B1 && I1 >= 0 && M1 >= 2 && Q1 >= 1 + O1 && O1 >= 1 && D1 = 0] (?,1) 37. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [B1 >= 1 + Q1 && I1 >= 0 && M1 >= 2 && O1 >= 1 + Q1 && 0 >= 1 + O1 && D1 = 0] (?,1) 38. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [B1 >= 1 + Q1 && I1 >= 0 && M1 >= 2 && O1 >= 1 + Q1 && O1 >= 1 && D1 = 0] (?,1) 39. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [B1 >= 1 + Q1 && I1 >= 0 && M1 >= 2 && Q1 >= 1 + O1 && 0 >= 1 + O1 && D1 = 0] (?,1) 40. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [B1 >= 1 + Q1 && I1 >= 0 && M1 >= 2 && Q1 >= 1 + O1 && O1 >= 1 && D1 = 0] (?,1) 41. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f16(A,B,C,D,E,M1,G,O1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,T1,C1,S1,P1,Q1,R1,U1,I1,J1,K1,L1) [M1 >= 2 && I1 >= 0 && D1 = B1] (?,1) 42. f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f1(2,O1,P1,D,E,O1,G,H,P1,P1,Q1,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,M1,R1) [O1 >= 2] (1,1) 43. f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f16(R1,P1,Q1,D,E,O1,S1,T1,U1,N1,Y1,0,Z1,A2,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,F2,C1,E2,B2,C2,D2,G2,I1,J1,M1,L1) [0 >= V1 && 0 >= W1 && 0 >= O1 && 0 >= X1] (1,1) 45. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,1 + I1,M1,G,H,I,J,K,L,O1,P1,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,L,I1,0,L,0,L,L,I1,J1,K1,L1) [Q1 >= 2 && M1 >= 2 && U >= 0 && L >= 1 && N = 0 && E = 1] (?,1) 46. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,1 + I1,M1,G,H,I,J,K,L,O1,P1,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,L,I1,0,L,0,L,L,I1,J1,K1,L1) [Q1 >= 2 && M1 >= 2 && U >= 0 && 0 >= 1 + L && N = 0 && E = 1] (?,1) 49. f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,1 + I1,M1,G,H,I,J,K,L,O1,P1,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,L,I1,0,L,0,L,L,I1,J1,K1,L1) [Q1 >= 2 && M1 >= 2 && D >= 0 && E >= 0 && L >= 1 && N = 0] (?,1) 50. f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,1 + I1,M1,G,H,I,J,K,L,O1,P1,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,L,I1,0,L,0,L,L,I1,J1,K1,L1) [Q1 >= 2 && M1 >= 2 && D >= 0 && E >= 0 && 0 >= 1 + L && N = 0] (?,1) Signature: {(f1,38);(f10,38);(f11,38);(f14,38);(f15,38);(f16,38);(f7,38);(f8,38)} Flow Graph: [0->{15,16,17,18,19,20,21,22,49,50},1->{15,16,17,18,19,20,21,22,49,50},2->{0,1,2},3->{15,16,17,18,19,20,21 ,22,49,50},4->{15,16,17,18,19,20,21,22,49,50},5->{15,16,17,18,19,20,21,22,49,50},6->{15,16,17,18,19,20,21,22 ,49,50},7->{15,16,17,18,19,20,21,22,49,50},8->{15,16,17,18,19,20,21,22,49,50},9->{15,16,17,18,19,20,21,22,49 ,50},10->{15,16,17,18,19,20,21,22,49,50},11->{15,16,17,18,19,20,21,22,49,50},12->{15,16,17,18,19,20,21,22,49 ,50},13->{15,16,17,18,19,20,21,22,49,50},14->{15,16,17,18,19,20,21,22,49,50},15->{15,16,17,18,19,20,21,22,49 ,50},16->{15,16,17,18,19,20,21,22,49,50},17->{15,16,17,18,19,20,21,22,49,50},18->{15,16,17,18,19,20,21,22,49 ,50},19->{15,16,17,18,19,20,21,22,49,50},20->{15,16,17,18,19,20,21,22,49,50},21->{15,16,17,18,19,20,21,22,49 ,50},22->{15,16,17,18,19,20,21,22,49,50},23->{33,34,35,36,37,38,39,40,41},24->{33,34,35,36,37,38,39,40,41} ,25->{33,34,35,36,37,38,39,40,41},26->{33,34,35,36,37,38,39,40,41},27->{33,34,35,36,37,38,39,40,41},28->{33 ,34,35,36,37,38,39,40,41},29->{33,34,35,36,37,38,39,40,41},30->{33,34,35,36,37,38,39,40,41},31->{},32->{} ,33->{33,34,35,36,37,38,39,40,41},34->{33,34,35,36,37,38,39,40,41},35->{33,34,35,36,37,38,39,40,41},36->{33 ,34,35,36,37,38,39,40,41},37->{33,34,35,36,37,38,39,40,41},38->{33,34,35,36,37,38,39,40,41},39->{33,34,35,36 ,37,38,39,40,41},40->{33,34,35,36,37,38,39,40,41},41->{},42->{0,1,2},43->{},45->{33,34,35,36,37,38,39,40,41} ,46->{33,34,35,36,37,38,39,40,41},49->{33,34,35,36,37,38,39,40,41},50->{33,34,35,36,37,38,39,40,41}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(0,49) ,(0,50) ,(1,49) ,(1,50) ,(3,49) ,(3,50) ,(4,49) ,(4,50) ,(5,49) ,(5,50) ,(6,49) ,(6,50) ,(7,49) ,(7,50) ,(8,49) ,(8,50) ,(9,49) ,(9,50) ,(10,49) ,(10,50) ,(11,49) ,(11,50) ,(12,49) ,(12,50) ,(13,49) ,(13,50) ,(14,49) ,(14,50) ,(15,49) ,(16,49) ,(17,50) ,(18,50) ,(19,49) ,(20,49) ,(21,50) ,(22,50) ,(23,40) ,(23,41) ,(30,33) ,(30,41) ,(33,40) ,(33,41) ,(40,33) ,(40,41) ,(45,33) ,(45,41) ,(46,40) ,(46,41) ,(49,33) ,(49,41) ,(50,40) ,(50,41)] * 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(D,O1,P1,D,0,M1,Q1,R1,S1,T1,U1,C,C,C,N1,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [A >= B && A >= 0 && M1 >= 2 && 0 >= 1 + C && N1 >= M1 && D >= M1 && E = 0] (?,1) 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(D,O1,P1,D,0,M1,Q1,R1,S1,T1,U1,C,C,C,N1,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [A >= B && A >= 0 && M1 >= 2 && C >= 1 && N1 >= M1 && D >= M1 && E = 0] (?,1) 2. 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f1(1 + A,B,K,D,E,F,G,H,I,K,M1,L,M,N,O,O1,A,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [B >= 1 + A && A >= 0] (?,1) 3. 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,D,1,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,1 + D,Q1,D,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [A >= 0 && M1 >= 2 && 0 >= 1 + N && R1 >= M1 && 0 >= 1 + O1 && E = 1] (?,1) 4. 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,D,1,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,1 + D,Q1,D,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [A >= 0 && M1 >= 2 && 0 >= 1 + N && R1 >= M1 && O1 >= 1 && E = 1] (?,1) 5. 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,D,1,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,1 + D,Q1,D,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [A >= 0 && M1 >= 2 && N >= 1 && R1 >= M1 && 0 >= 1 + O1 && E = 1] (?,1) 6. 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,D,1,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,1 + D,Q1,D,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [A >= 0 && M1 >= 2 && N >= 1 && R1 >= M1 && O1 >= 1 && E = 1] (?,1) 7. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,D,E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,R,S,T,U,P1,Q1,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [U >= 0 && M1 >= 2 && 0 >= 1 + N && 0 >= 1 + O1 && 0 >= 1 + Q1] (?,1) 8. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,D,E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,R,S,T,U,P1,Q1,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [U >= 0 && M1 >= 2 && 0 >= 1 + N && 0 >= 1 + O1 && Q1 >= 1] (?,1) 9. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,D,E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,R,S,T,U,P1,Q1,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [U >= 0 && M1 >= 2 && 0 >= 1 + N && O1 >= 1 && 0 >= 1 + Q1] (?,1) 10. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,D,E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,R,S,T,U,P1,Q1,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [U >= 0 && M1 >= 2 && 0 >= 1 + N && O1 >= 1 && Q1 >= 1] (?,1) 11. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,D,E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,R,S,T,U,P1,Q1,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [U >= 0 && M1 >= 2 && N >= 1 && 0 >= 1 + O1 && 0 >= 1 + Q1] (?,1) 12. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,D,E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,R,S,T,U,P1,Q1,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [U >= 0 && M1 >= 2 && N >= 1 && 0 >= 1 + O1 && Q1 >= 1] (?,1) 13. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,D,E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,R,S,T,U,P1,Q1,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [U >= 0 && M1 >= 2 && N >= 1 && O1 >= 1 && 0 >= 1 + Q1] (?,1) 14. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,D,E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,R,S,T,U,P1,Q1,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [U >= 0 && M1 >= 2 && N >= 1 && O1 >= 1 && Q1 >= 1] (?,1) 15. f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[E >= 0 && D >= 0 && M1 >= 2 && 0 >= 1 + R1 && 0 >= 1 + O1 && 0 >= 1 + Q1] (?,1) ,J1,K1,L1) 16. f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[E >= 0 && D >= 0 && M1 >= 2 && 0 >= 1 + R1 && 0 >= 1 + O1 && Q1 >= 1] (?,1) ,J1,K1,L1) 17. f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[E >= 0 && D >= 0 && M1 >= 2 && 0 >= 1 + R1 && O1 >= 1 && 0 >= 1 + Q1] (?,1) ,J1,K1,L1) 18. f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[E >= 0 && D >= 0 && M1 >= 2 && 0 >= 1 + R1 && O1 >= 1 && Q1 >= 1] (?,1) ,J1,K1,L1) 19. f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[E >= 0 && D >= 0 && M1 >= 2 && R1 >= 1 && 0 >= 1 + O1 && 0 >= 1 + Q1] (?,1) ,J1,K1,L1) 20. f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[E >= 0 && D >= 0 && M1 >= 2 && R1 >= 1 && 0 >= 1 + O1 && Q1 >= 1] (?,1) ,J1,K1,L1) 21. f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[E >= 0 && D >= 0 && M1 >= 2 && R1 >= 1 && O1 >= 1 && 0 >= 1 + Q1] (?,1) ,J1,K1,L1) 22. f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[E >= 0 && D >= 0 && M1 >= 2 && R1 >= 1 && O1 >= 1 && Q1 >= 1] (?,1) ,J1,K1,L1) 23. f7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,I1,J1,K1,L1) [P1 >= 1 + B1 && C1 >= 0 && M1 >= 2 && O1 >= 1 + P1 && 0 >= 1 + O1 && D1 = 0] (?,1) 24. f7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,I1,J1,K1,L1) [P1 >= 1 + B1 && C1 >= 0 && M1 >= 2 && O1 >= 1 + P1 && O1 >= 1 && D1 = 0] (?,1) 25. f7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,I1,J1,K1,L1) [P1 >= 1 + B1 && C1 >= 0 && M1 >= 2 && P1 >= 1 + O1 && 0 >= 1 + O1 && D1 = 0] (?,1) 26. f7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,I1,J1,K1,L1) [P1 >= 1 + B1 && C1 >= 0 && M1 >= 2 && P1 >= 1 + O1 && O1 >= 1 && D1 = 0] (?,1) 27. f7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,I1,J1,K1,L1) [B1 >= 1 + P1 && C1 >= 0 && M1 >= 2 && O1 >= 1 + P1 && 0 >= 1 + O1 && D1 = 0] (?,1) 28. f7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,I1,J1,K1,L1) [B1 >= 1 + P1 && C1 >= 0 && M1 >= 2 && O1 >= 1 + P1 && O1 >= 1 && D1 = 0] (?,1) 29. f7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,I1,J1,K1,L1) [B1 >= 1 + P1 && C1 >= 0 && M1 >= 2 && P1 >= 1 + O1 && 0 >= 1 + O1 && D1 = 0] (?,1) 30. f7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,I1,J1,K1,L1) [B1 >= 1 + P1 && C1 >= 0 && M1 >= 2 && P1 >= 1 + O1 && O1 >= 1 && D1 = 0] (?,1) 31. f7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f16(A,B,C,D,E,M1,G,O1,I,J,K,P1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,U1,C1,T1,Q1,R1,S1,N1,I1,J1,K1,L1) [C1 >= 0 && 0 >= 1 + P1 && M1 >= 2 && D1 = B1] (?,1) 32. f7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f16(A,B,C,D,E,M1,G,O1,I,J,K,P1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,U1,C1,T1,Q1,R1,S1,N1,I1,J1,K1,L1) [C1 >= 0 && P1 >= 1 && M1 >= 2 && D1 = B1] (?,1) 33. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [Q1 >= 1 + B1 && I1 >= 0 && M1 >= 2 && O1 >= 1 + Q1 && 0 >= 1 + O1 && D1 = 0] (?,1) 34. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [Q1 >= 1 + B1 && I1 >= 0 && M1 >= 2 && O1 >= 1 + Q1 && O1 >= 1 && D1 = 0] (?,1) 35. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [Q1 >= 1 + B1 && I1 >= 0 && M1 >= 2 && Q1 >= 1 + O1 && 0 >= 1 + O1 && D1 = 0] (?,1) 36. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [Q1 >= 1 + B1 && I1 >= 0 && M1 >= 2 && Q1 >= 1 + O1 && O1 >= 1 && D1 = 0] (?,1) 37. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [B1 >= 1 + Q1 && I1 >= 0 && M1 >= 2 && O1 >= 1 + Q1 && 0 >= 1 + O1 && D1 = 0] (?,1) 38. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [B1 >= 1 + Q1 && I1 >= 0 && M1 >= 2 && O1 >= 1 + Q1 && O1 >= 1 && D1 = 0] (?,1) 39. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [B1 >= 1 + Q1 && I1 >= 0 && M1 >= 2 && Q1 >= 1 + O1 && 0 >= 1 + O1 && D1 = 0] (?,1) 40. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [B1 >= 1 + Q1 && I1 >= 0 && M1 >= 2 && Q1 >= 1 + O1 && O1 >= 1 && D1 = 0] (?,1) 41. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f16(A,B,C,D,E,M1,G,O1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,T1,C1,S1,P1,Q1,R1,U1,I1,J1,K1,L1) [M1 >= 2 && I1 >= 0 && D1 = B1] (?,1) 42. f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f1(2,O1,P1,D,E,O1,G,H,P1,P1,Q1,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,M1,R1) [O1 >= 2] (1,1) 43. f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f16(R1,P1,Q1,D,E,O1,S1,T1,U1,N1,Y1,0,Z1,A2,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,F2,C1,E2,B2,C2,D2,G2,I1,J1,M1,L1) [0 >= V1 && 0 >= W1 && 0 >= O1 && 0 >= X1] (1,1) 45. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,1 + I1,M1,G,H,I,J,K,L,O1,P1,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,L,I1,0,L,0,L,L,I1,J1,K1,L1) [Q1 >= 2 && M1 >= 2 && U >= 0 && L >= 1 && N = 0 && E = 1] (?,1) 46. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,1 + I1,M1,G,H,I,J,K,L,O1,P1,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,L,I1,0,L,0,L,L,I1,J1,K1,L1) [Q1 >= 2 && M1 >= 2 && U >= 0 && 0 >= 1 + L && N = 0 && E = 1] (?,1) 49. f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,1 + I1,M1,G,H,I,J,K,L,O1,P1,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,L,I1,0,L,0,L,L,I1,J1,K1,L1) [Q1 >= 2 && M1 >= 2 && D >= 0 && E >= 0 && L >= 1 && N = 0] (?,1) 50. f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,1 + I1,M1,G,H,I,J,K,L,O1,P1,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,L,I1,0,L,0,L,L,I1,J1,K1,L1) [Q1 >= 2 && M1 >= 2 && D >= 0 && E >= 0 && 0 >= 1 + L && N = 0] (?,1) Signature: {(f1,38);(f10,38);(f11,38);(f14,38);(f15,38);(f16,38);(f7,38);(f8,38)} Flow Graph: [0->{15,16,17,18,19,20,21,22},1->{15,16,17,18,19,20,21,22},2->{0,1,2},3->{15,16,17,18,19,20,21,22},4->{15 ,16,17,18,19,20,21,22},5->{15,16,17,18,19,20,21,22},6->{15,16,17,18,19,20,21,22},7->{15,16,17,18,19,20,21 ,22},8->{15,16,17,18,19,20,21,22},9->{15,16,17,18,19,20,21,22},10->{15,16,17,18,19,20,21,22},11->{15,16,17 ,18,19,20,21,22},12->{15,16,17,18,19,20,21,22},13->{15,16,17,18,19,20,21,22},14->{15,16,17,18,19,20,21,22} ,15->{15,16,17,18,19,20,21,22,50},16->{15,16,17,18,19,20,21,22,50},17->{15,16,17,18,19,20,21,22,49},18->{15 ,16,17,18,19,20,21,22,49},19->{15,16,17,18,19,20,21,22,50},20->{15,16,17,18,19,20,21,22,50},21->{15,16,17,18 ,19,20,21,22,49},22->{15,16,17,18,19,20,21,22,49},23->{33,34,35,36,37,38,39},24->{33,34,35,36,37,38,39,40 ,41},25->{33,34,35,36,37,38,39,40,41},26->{33,34,35,36,37,38,39,40,41},27->{33,34,35,36,37,38,39,40,41} ,28->{33,34,35,36,37,38,39,40,41},29->{33,34,35,36,37,38,39,40,41},30->{34,35,36,37,38,39,40},31->{},32->{} ,33->{33,34,35,36,37,38,39},34->{33,34,35,36,37,38,39,40,41},35->{33,34,35,36,37,38,39,40,41},36->{33,34,35 ,36,37,38,39,40,41},37->{33,34,35,36,37,38,39,40,41},38->{33,34,35,36,37,38,39,40,41},39->{33,34,35,36,37,38 ,39,40,41},40->{34,35,36,37,38,39,40},41->{},42->{0,1,2},43->{},45->{34,35,36,37,38,39,40},46->{33,34,35,36 ,37,38,39},49->{34,35,36,37,38,39,40},50->{33,34,35,36,37,38,39}] + Applied Processor: UnreachableRules + Details: Following transitions are not reachable from the starting states and are revomed: [3 ,4 ,5 ,6 ,7 ,8 ,9 ,10 ,11 ,12 ,13 ,14 ,23 ,24 ,25 ,26 ,27 ,28 ,29 ,30 ,31 ,32 ,45 ,46] * 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(D,O1,P1,D,0,M1,Q1,R1,S1,T1,U1,C,C,C,N1,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [A >= B && A >= 0 && M1 >= 2 && 0 >= 1 + C && N1 >= M1 && D >= M1 && E = 0] (?,1) 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(D,O1,P1,D,0,M1,Q1,R1,S1,T1,U1,C,C,C,N1,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [A >= B && A >= 0 && M1 >= 2 && C >= 1 && N1 >= M1 && D >= M1 && E = 0] (?,1) 2. 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f1(1 + A,B,K,D,E,F,G,H,I,K,M1,L,M,N,O,O1,A,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [B >= 1 + A && A >= 0] (?,1) 15. f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[E >= 0 && D >= 0 && M1 >= 2 && 0 >= 1 + R1 && 0 >= 1 + O1 && 0 >= 1 + Q1] (?,1) ,J1,K1,L1) 16. f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[E >= 0 && D >= 0 && M1 >= 2 && 0 >= 1 + R1 && 0 >= 1 + O1 && Q1 >= 1] (?,1) ,J1,K1,L1) 17. f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[E >= 0 && D >= 0 && M1 >= 2 && 0 >= 1 + R1 && O1 >= 1 && 0 >= 1 + Q1] (?,1) ,J1,K1,L1) 18. f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[E >= 0 && D >= 0 && M1 >= 2 && 0 >= 1 + R1 && O1 >= 1 && Q1 >= 1] (?,1) ,J1,K1,L1) 19. f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[E >= 0 && D >= 0 && M1 >= 2 && R1 >= 1 && 0 >= 1 + O1 && 0 >= 1 + Q1] (?,1) ,J1,K1,L1) 20. f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[E >= 0 && D >= 0 && M1 >= 2 && R1 >= 1 && 0 >= 1 + O1 && Q1 >= 1] (?,1) ,J1,K1,L1) 21. f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[E >= 0 && D >= 0 && M1 >= 2 && R1 >= 1 && O1 >= 1 && 0 >= 1 + Q1] (?,1) ,J1,K1,L1) 22. f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[E >= 0 && D >= 0 && M1 >= 2 && R1 >= 1 && O1 >= 1 && Q1 >= 1] (?,1) ,J1,K1,L1) 33. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [Q1 >= 1 + B1 && I1 >= 0 && M1 >= 2 && O1 >= 1 + Q1 && 0 >= 1 + O1 && D1 = 0] (?,1) 34. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [Q1 >= 1 + B1 && I1 >= 0 && M1 >= 2 && O1 >= 1 + Q1 && O1 >= 1 && D1 = 0] (?,1) 35. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [Q1 >= 1 + B1 && I1 >= 0 && M1 >= 2 && Q1 >= 1 + O1 && 0 >= 1 + O1 && D1 = 0] (?,1) 36. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [Q1 >= 1 + B1 && I1 >= 0 && M1 >= 2 && Q1 >= 1 + O1 && O1 >= 1 && D1 = 0] (?,1) 37. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [B1 >= 1 + Q1 && I1 >= 0 && M1 >= 2 && O1 >= 1 + Q1 && 0 >= 1 + O1 && D1 = 0] (?,1) 38. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [B1 >= 1 + Q1 && I1 >= 0 && M1 >= 2 && O1 >= 1 + Q1 && O1 >= 1 && D1 = 0] (?,1) 39. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [B1 >= 1 + Q1 && I1 >= 0 && M1 >= 2 && Q1 >= 1 + O1 && 0 >= 1 + O1 && D1 = 0] (?,1) 40. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [B1 >= 1 + Q1 && I1 >= 0 && M1 >= 2 && Q1 >= 1 + O1 && O1 >= 1 && D1 = 0] (?,1) 41. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f16(A,B,C,D,E,M1,G,O1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,T1,C1,S1,P1,Q1,R1,U1,I1,J1,K1,L1) [M1 >= 2 && I1 >= 0 && D1 = B1] (?,1) 42. f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f1(2,O1,P1,D,E,O1,G,H,P1,P1,Q1,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,M1,R1) [O1 >= 2] (1,1) 43. f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f16(R1,P1,Q1,D,E,O1,S1,T1,U1,N1,Y1,0,Z1,A2,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,F2,C1,E2,B2,C2,D2,G2,I1,J1,M1,L1) [0 >= V1 && 0 >= W1 && 0 >= O1 && 0 >= X1] (1,1) 49. f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,1 + I1,M1,G,H,I,J,K,L,O1,P1,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,L,I1,0,L,0,L,L,I1,J1,K1,L1) [Q1 >= 2 && M1 >= 2 && D >= 0 && E >= 0 && L >= 1 && N = 0] (?,1) 50. f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D,1 + I1,M1,G,H,I,J,K,L,O1,P1,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,L,I1,0,L,0,L,L,I1,J1,K1,L1) [Q1 >= 2 && M1 >= 2 && D >= 0 && E >= 0 && 0 >= 1 + L && N = 0] (?,1) Signature: {(f1,38);(f10,38);(f11,38);(f14,38);(f15,38);(f16,38);(f7,38);(f8,38)} Flow Graph: [0->{15,16,17,18,19,20,21,22},1->{15,16,17,18,19,20,21,22},2->{0,1,2},15->{15,16,17,18,19,20,21,22,50} ,16->{15,16,17,18,19,20,21,22,50},17->{15,16,17,18,19,20,21,22,49},18->{15,16,17,18,19,20,21,22,49},19->{15 ,16,17,18,19,20,21,22,50},20->{15,16,17,18,19,20,21,22,50},21->{15,16,17,18,19,20,21,22,49},22->{15,16,17,18 ,19,20,21,22,49},33->{33,34,35,36,37,38,39},34->{33,34,35,36,37,38,39,40,41},35->{33,34,35,36,37,38,39,40 ,41},36->{33,34,35,36,37,38,39,40,41},37->{33,34,35,36,37,38,39,40,41},38->{33,34,35,36,37,38,39,40,41} ,39->{33,34,35,36,37,38,39,40,41},40->{34,35,36,37,38,39,40},41->{},42->{0,1,2},43->{},49->{34,35,36,37,38 ,39,40},50->{33,34,35,36,37,38,39}] + 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(D,O1 ,P1,D,0,M1,Q1,R1,S1,T1,U1,C,C,C,N1,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1 ,L1) [A >= B && A >= 0 && M1 >= 2 && 0 >= 1 + C && N1 >= M1 && D >= M1 && E = 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(D,O1 ,P1,D,0,M1,Q1,R1,S1,T1,U1,C,C,C,N1,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1 ,L1) [A >= B && A >= 0 && M1 >= 2 && C >= 1 && N1 >= M1 && D >= M1 && E = 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f1(1 + A,B ,K,D,E,F,G,H,I,K,M1,L,M,N,O,O1,A,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1 ,L1) [B >= 1 + A && A >= 0] f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C ,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1 ,L1) [E >= 0 && D >= 0 && M1 >= 2 && 0 >= 1 + R1 && 0 >= 1 + O1 && 0 >= 1 + Q1] f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C ,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1 ,L1) [E >= 0 && D >= 0 && M1 >= 2 && 0 >= 1 + R1 && 0 >= 1 + O1 && Q1 >= 1] f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C ,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1 ,L1) [E >= 0 && D >= 0 && M1 >= 2 && 0 >= 1 + R1 && O1 >= 1 && 0 >= 1 + Q1] f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C ,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1 ,L1) [E >= 0 && D >= 0 && M1 >= 2 && 0 >= 1 + R1 && O1 >= 1 && Q1 >= 1] f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C ,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1 ,L1) [E >= 0 && D >= 0 && M1 >= 2 && R1 >= 1 && 0 >= 1 + O1 && 0 >= 1 + Q1] f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C ,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1 ,L1) [E >= 0 && D >= 0 && M1 >= 2 && R1 >= 1 && 0 >= 1 + O1 && Q1 >= 1] f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C ,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1 ,L1) [E >= 0 && D >= 0 && M1 >= 2 && R1 >= 1 && O1 >= 1 && 0 >= 1 + Q1] f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C ,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1 ,L1) [E >= 0 && D >= 0 && M1 >= 2 && R1 >= 1 && O1 >= 1 && Q1 >= 1] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D ,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1 ,L1) [Q1 >= 1 + B1 && I1 >= 0 && M1 >= 2 && O1 >= 1 + Q1 && 0 >= 1 + O1 && D1 = 0] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D ,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1 ,L1) [Q1 >= 1 + B1 && I1 >= 0 && M1 >= 2 && O1 >= 1 + Q1 && O1 >= 1 && D1 = 0] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D ,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1 ,L1) [Q1 >= 1 + B1 && I1 >= 0 && M1 >= 2 && Q1 >= 1 + O1 && 0 >= 1 + O1 && D1 = 0] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D ,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1 ,L1) [Q1 >= 1 + B1 && I1 >= 0 && M1 >= 2 && Q1 >= 1 + O1 && O1 >= 1 && D1 = 0] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D ,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1 ,L1) [B1 >= 1 + Q1 && I1 >= 0 && M1 >= 2 && O1 >= 1 + Q1 && 0 >= 1 + O1 && D1 = 0] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D ,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1 ,L1) [B1 >= 1 + Q1 && I1 >= 0 && M1 >= 2 && O1 >= 1 + Q1 && O1 >= 1 && D1 = 0] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D ,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1 ,L1) [B1 >= 1 + Q1 && I1 >= 0 && M1 >= 2 && Q1 >= 1 + O1 && 0 >= 1 + O1 && D1 = 0] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D ,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1 ,L1) [B1 >= 1 + Q1 && I1 >= 0 && M1 >= 2 && Q1 >= 1 + O1 && O1 >= 1 && D1 = 0] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f16(A,B,C ,D,E,M1,G,O1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,T1,C1,S1,P1,Q1,R1,U1,I1,J1,K1 ,L1) [M1 >= 2 && I1 >= 0 && D1 = B1] f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f1(2,O1,P1 ,D,E,O1,G,H,P1,P1,Q1,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,M1 ,R1) [O1 >= 2] f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f16(R1,P1 ,Q1,D,E,O1,S1,T1,U1,N1,Y1,0,Z1,A2,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,F2,C1,E2,B2,C2,D2,G2,I1,J1,M1 ,L1) [0 >= V1 && 0 >= W1 && 0 >= O1 && 0 >= X1] f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D ,1 + I1,M1,G,H,I,J,K,L,O1,P1,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,L,I1,0,L,0,L,L,I1,J1,K1 ,L1) [Q1 >= 2 && M1 >= 2 && D >= 0 && E >= 0 && L >= 1 && N = 0] f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D ,1 + I1,M1,G,H,I,J,K,L,O1,P1,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,L,I1,0,L,0,L,L,I1,J1,K1 ,L1) [Q1 >= 2 && M1 >= 2 && D >= 0 && E >= 0 && 0 >= 1 + L && N = 0] Signature: {(f1,38);(f10,38);(f11,38);(f14,38);(f15,38);(f16,38);(f7,38);(f8,38)} Rule Graph: [0->{15,16,17,18,19,20,21,22},1->{15,16,17,18,19,20,21,22},2->{0,1,2},15->{15,16,17,18,19,20,21,22,50} ,16->{15,16,17,18,19,20,21,22,50},17->{15,16,17,18,19,20,21,22,49},18->{15,16,17,18,19,20,21,22,49},19->{15 ,16,17,18,19,20,21,22,50},20->{15,16,17,18,19,20,21,22,50},21->{15,16,17,18,19,20,21,22,49},22->{15,16,17,18 ,19,20,21,22,49},33->{33,34,35,36,37,38,39},34->{33,34,35,36,37,38,39,40,41},35->{33,34,35,36,37,38,39,40 ,41},36->{33,34,35,36,37,38,39,40,41},37->{33,34,35,36,37,38,39,40,41},38->{33,34,35,36,37,38,39,40,41} ,39->{33,34,35,36,37,38,39,40,41},40->{34,35,36,37,38,39,40},41->{},42->{0,1,2},43->{},49->{34,35,36,37,38 ,39,40},50->{33,34,35,36,37,38,39}] + Applied Processor: Decompose NoGreedy + Details: We construct a looptree: P: [0,1,2,15,16,17,18,19,20,21,22,33,34,35,36,37,38,39,40,41,42,43,49,50] | +- p:[2] c: [2] | +- p:[15,16,17,18,19,20,21,22] c: [22] | | | `- p:[15,16,17,18,19,20,21] c: [21] | | | `- p:[15,16,17,18,19,20] c: [20] | | | `- p:[15,16,17,18,19] c: [19] | | | `- p:[15,16,17,18] c: [18] | | | `- p:[15,16,17] c: [17] | | | `- p:[15,16] c: [16] | | | `- p:[15] c: [15] | `- p:[34,33,35,36,37,38,39,40] c: [40] | `- p:[33,34,35,36,37,38,39] c: [39] | `- p:[33,34,35,36,37,38] c: [38] | `- p:[33,34,35,36,37] c: [37] | `- p:[33,34,35,36] c: [36] | `- p:[33,34,35] c: [35] | `- p:[33,34] c: [34] | `- p:[33] c: [33] * 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(D,O1 ,P1,D,0,M1,Q1,R1,S1,T1,U1,C,C,C,N1,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1 ,L1) [A >= B && A >= 0 && M1 >= 2 && 0 >= 1 + C && N1 >= M1 && D >= M1 && E = 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(D,O1 ,P1,D,0,M1,Q1,R1,S1,T1,U1,C,C,C,N1,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1 ,L1) [A >= B && A >= 0 && M1 >= 2 && C >= 1 && N1 >= M1 && D >= M1 && E = 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,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f1(1 + A,B ,K,D,E,F,G,H,I,K,M1,L,M,N,O,O1,A,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1 ,L1) [B >= 1 + A && A >= 0] f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C ,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1 ,L1) [E >= 0 && D >= 0 && M1 >= 2 && 0 >= 1 + R1 && 0 >= 1 + O1 && 0 >= 1 + Q1] f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C ,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1 ,L1) [E >= 0 && D >= 0 && M1 >= 2 && 0 >= 1 + R1 && 0 >= 1 + O1 && Q1 >= 1] f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C ,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1 ,L1) [E >= 0 && D >= 0 && M1 >= 2 && 0 >= 1 + R1 && O1 >= 1 && 0 >= 1 + Q1] f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C ,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1 ,L1) [E >= 0 && D >= 0 && M1 >= 2 && 0 >= 1 + R1 && O1 >= 1 && Q1 >= 1] f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C ,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1 ,L1) [E >= 0 && D >= 0 && M1 >= 2 && R1 >= 1 && 0 >= 1 + O1 && 0 >= 1 + Q1] f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C ,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1 ,L1) [E >= 0 && D >= 0 && M1 >= 2 && R1 >= 1 && 0 >= 1 + O1 && Q1 >= 1] f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C ,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1 ,L1) [E >= 0 && D >= 0 && M1 >= 2 && R1 >= 1 && O1 >= 1 && 0 >= 1 + Q1] f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(A,B,C ,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1 ,L1) [E >= 0 && D >= 0 && M1 >= 2 && R1 >= 1 && O1 >= 1 && Q1 >= 1] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D ,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1 ,L1) [Q1 >= 1 + B1 && I1 >= 0 && M1 >= 2 && O1 >= 1 + Q1 && 0 >= 1 + O1 && D1 = 0] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D ,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1 ,L1) [Q1 >= 1 + B1 && I1 >= 0 && M1 >= 2 && O1 >= 1 + Q1 && O1 >= 1 && D1 = 0] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D ,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1 ,L1) [Q1 >= 1 + B1 && I1 >= 0 && M1 >= 2 && Q1 >= 1 + O1 && 0 >= 1 + O1 && D1 = 0] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D ,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1 ,L1) [Q1 >= 1 + B1 && I1 >= 0 && M1 >= 2 && Q1 >= 1 + O1 && O1 >= 1 && D1 = 0] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D ,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1 ,L1) [B1 >= 1 + Q1 && I1 >= 0 && M1 >= 2 && O1 >= 1 + Q1 && 0 >= 1 + O1 && D1 = 0] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D ,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1 ,L1) [B1 >= 1 + Q1 && I1 >= 0 && M1 >= 2 && O1 >= 1 + Q1 && O1 >= 1 && D1 = 0] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D ,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1 ,L1) [B1 >= 1 + Q1 && I1 >= 0 && M1 >= 2 && Q1 >= 1 + O1 && 0 >= 1 + O1 && D1 = 0] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D ,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1 ,L1) [B1 >= 1 + Q1 && I1 >= 0 && M1 >= 2 && Q1 >= 1 + O1 && O1 >= 1 && D1 = 0] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f16(A,B,C ,D,E,M1,G,O1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,T1,C1,S1,P1,Q1,R1,U1,I1,J1,K1 ,L1) [M1 >= 2 && I1 >= 0 && D1 = B1] f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f1(2,O1,P1 ,D,E,O1,G,H,P1,P1,Q1,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,M1 ,R1) [O1 >= 2] f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f16(R1,P1 ,Q1,D,E,O1,S1,T1,U1,N1,Y1,0,Z1,A2,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,F2,C1,E2,B2,C2,D2,G2,I1,J1,M1 ,L1) [0 >= V1 && 0 >= W1 && 0 >= O1 && 0 >= X1] f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D ,1 + I1,M1,G,H,I,J,K,L,O1,P1,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,L,I1,0,L,0,L,L,I1,J1,K1 ,L1) [Q1 >= 2 && M1 >= 2 && D >= 0 && E >= 0 && L >= 1 && N = 0] f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,B,C,D ,1 + I1,M1,G,H,I,J,K,L,O1,P1,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,L,I1,0,L,0,L,L,I1,J1,K1 ,L1) [Q1 >= 2 && M1 >= 2 && D >= 0 && E >= 0 && 0 >= 1 + L && N = 0] Signature: {(f1,38);(f10,38);(f11,38);(f14,38);(f15,38);(f16,38);(f7,38);(f8,38)} Rule Graph: [0->{15,16,17,18,19,20,21,22},1->{15,16,17,18,19,20,21,22},2->{0,1,2},15->{15,16,17,18,19,20,21,22,50} ,16->{15,16,17,18,19,20,21,22,50},17->{15,16,17,18,19,20,21,22,49},18->{15,16,17,18,19,20,21,22,49},19->{15 ,16,17,18,19,20,21,22,50},20->{15,16,17,18,19,20,21,22,50},21->{15,16,17,18,19,20,21,22,49},22->{15,16,17,18 ,19,20,21,22,49},33->{33,34,35,36,37,38,39},34->{33,34,35,36,37,38,39,40,41},35->{33,34,35,36,37,38,39,40 ,41},36->{33,34,35,36,37,38,39,40,41},37->{33,34,35,36,37,38,39,40,41},38->{33,34,35,36,37,38,39,40,41} ,39->{33,34,35,36,37,38,39,40,41},40->{34,35,36,37,38,39,40},41->{},42->{0,1,2},43->{},49->{34,35,36,37,38 ,39,40},50->{33,34,35,36,37,38,39}] ,We construct a looptree: P: [0,1,2,15,16,17,18,19,20,21,22,33,34,35,36,37,38,39,40,41,42,43,49,50] | +- p:[2] c: [2] | +- p:[15,16,17,18,19,20,21,22] c: [22] | | | `- p:[15,16,17,18,19,20,21] c: [21] | | | `- p:[15,16,17,18,19,20] c: [20] | | | `- p:[15,16,17,18,19] c: [19] | | | `- p:[15,16,17,18] c: [18] | | | `- p:[15,16,17] c: [17] | | | `- p:[15,16] c: [16] | | | `- p:[15] c: [15] | `- p:[34,33,35,36,37,38,39,40] c: [40] | `- p:[33,34,35,36,37,38,39] c: [39] | `- p:[33,34,35,36,37,38] c: [38] | `- p:[33,34,35,36,37] c: [37] | `- p:[33,34,35,36] c: [36] | `- p:[33,34,35] c: [35] | `- p:[33,34] c: [34] | `- p:[33] c: [33]) + Applied Processor: CloseWith True + Details: () YES