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