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