YES * Step 1: UnsatRules YES + Considered Problem: Rules: 0. f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f15(A,1 + B,D,X1,D,Y1,B,H,I,J,K,L,M,N,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) ,R1,S1,T1,U1,V1,W1) ,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 1. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(A,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1 [H >= 0 && I >= 0 && X1 >= 2 && 0 >= 1 + Z1 && 0 >= 1 + A2 && 0 >= 1 + B2] (?,1) ,R1,S1,T1,U1,V1,W1) ,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 2. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(A,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1 [H >= 0 && I >= 0 && X1 >= 2 && 0 >= 1 + Z1 && 0 >= 1 + A2 && B2 >= 1] (?,1) ,R1,S1,T1,U1,V1,W1) ,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 3. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(A,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1 [H >= 0 && I >= 0 && X1 >= 2 && 0 >= 1 + Z1 && A2 >= 1 && 0 >= 1 + B2] (?,1) ,R1,S1,T1,U1,V1,W1) ,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 4. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(A,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1 [H >= 0 && I >= 0 && X1 >= 2 && 0 >= 1 + Z1 && A2 >= 1 && B2 >= 1] (?,1) ,R1,S1,T1,U1,V1,W1) ,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 5. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(A,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1 [H >= 0 && I >= 0 && X1 >= 2 && Z1 >= 1 && 0 >= 1 + A2 && 0 >= 1 + B2] (?,1) ,R1,S1,T1,U1,V1,W1) ,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 6. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(A,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1 [H >= 0 && I >= 0 && X1 >= 2 && Z1 >= 1 && 0 >= 1 + A2 && B2 >= 1] (?,1) ,R1,S1,T1,U1,V1,W1) ,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 7. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(A,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1 [H >= 0 && I >= 0 && X1 >= 2 && Z1 >= 1 && A2 >= 1 && 0 >= 1 + B2] (?,1) ,R1,S1,T1,U1,V1,W1) ,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 8. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(A,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1 [H >= 0 && I >= 0 && X1 >= 2 && Z1 >= 1 && A2 >= 1 && B2 >= 1] (?,1) ,R1,S1,T1,U1,V1,W1) ,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 9. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,K1,L1,M1,N1,O1,P1 [A2 >= 1 + D1 && E1 >= 0 && X1 >= 2 && Y1 >= 1 + A2 && 0 >= 1 + Y1 && F1 = 0] (?,1) ,S1,T1,U1,V1,W1) ,Q1,R1,S1,T1,U1,V1,W1) 10. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,K1,L1,M1,N1,O1,P1 [A2 >= 1 + D1 && E1 >= 0 && X1 >= 2 && Y1 >= 1 + A2 && Y1 >= 1 && F1 = 0] (?,1) ,S1,T1,U1,V1,W1) ,Q1,R1,S1,T1,U1,V1,W1) 11. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,K1,L1,M1,N1,O1,P1 [A2 >= 1 + D1 && E1 >= 0 && X1 >= 2 && A2 >= 1 + Y1 && 0 >= 1 + Y1 && F1 = 0] (?,1) ,S1,T1,U1,V1,W1) ,Q1,R1,S1,T1,U1,V1,W1) 12. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,K1,L1,M1,N1,O1,P1 [A2 >= 1 + D1 && E1 >= 0 && X1 >= 2 && A2 >= 1 + Y1 && Y1 >= 1 && F1 = 0] (?,1) ,S1,T1,U1,V1,W1) ,Q1,R1,S1,T1,U1,V1,W1) 13. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,K1,L1,M1,N1,O1,P1 [D1 >= 1 + A2 && E1 >= 0 && X1 >= 2 && Y1 >= 1 + A2 && 0 >= 1 + Y1 && F1 = 0] (?,1) ,S1,T1,U1,V1,W1) ,Q1,R1,S1,T1,U1,V1,W1) 14. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,K1,L1,M1,N1,O1,P1 [D1 >= 1 + A2 && E1 >= 0 && X1 >= 2 && Y1 >= 1 + A2 && Y1 >= 1 && F1 = 0] (?,1) ,S1,T1,U1,V1,W1) ,Q1,R1,S1,T1,U1,V1,W1) 15. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,K1,L1,M1,N1,O1,P1 [D1 >= 1 + A2 && E1 >= 0 && X1 >= 2 && A2 >= 1 + Y1 && 0 >= 1 + Y1 && F1 = 0] (?,1) ,S1,T1,U1,V1,W1) ,Q1,R1,S1,T1,U1,V1,W1) 16. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,K1,L1,M1,N1,O1,P1 [D1 >= 1 + A2 && E1 >= 0 && X1 >= 2 && A2 >= 1 + Y1 && Y1 >= 1 && F1 = 0] (?,1) ,S1,T1,U1,V1,W1) ,Q1,R1,S1,T1,U1,V1,W1) 17. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f0(A,B,C,D,E,F,G,H,I,X1,Y1,A2,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,G2,E1,F2,C2,D2,E2,H2,K1,L1,M1,N1,O1 [E1 >= 0 && 0 >= 1 + A2 && X1 >= 2 && F1 = D1] (?,1) ,S1,T1,U1,V1,W1) ,P1,Q1,R1,S1,T1,U1,V1,W1) 18. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f0(A,B,C,D,E,F,G,H,I,X1,Y1,A2,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,G2,E1,F2,C2,D2,E2,H2,K1,L1,M1,N1,O1 [E1 >= 0 && A2 >= 1 && X1 >= 2 && F1 = D1] (?,1) ,S1,T1,U1,V1,W1) ,P1,Q1,R1,S1,T1,U1,V1,W1) 19. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1 [C2 >= 1 + D1 && K1 >= 0 && X1 >= 2 && Y1 >= 1 + C2 && 0 >= 1 + Y1 && F1 = 0] (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 20. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1 [C2 >= 1 + D1 && K1 >= 0 && X1 >= 2 && Y1 >= 1 + C2 && Y1 >= 1 && F1 = 0] (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 21. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1 [C2 >= 1 + D1 && K1 >= 0 && X1 >= 2 && C2 >= 1 + Y1 && 0 >= 1 + Y1 && F1 = 0] (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 22. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1 [C2 >= 1 + D1 && K1 >= 0 && X1 >= 2 && C2 >= 1 + Y1 && Y1 >= 1 && F1 = 0] (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 23. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1 [D1 >= 1 + C2 && K1 >= 0 && X1 >= 2 && Y1 >= 1 + C2 && 0 >= 1 + Y1 && F1 = 0] (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 24. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1 [D1 >= 1 + C2 && K1 >= 0 && X1 >= 2 && Y1 >= 1 + C2 && Y1 >= 1 && F1 = 0] (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 25. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1 [D1 >= 1 + C2 && K1 >= 0 && X1 >= 2 && C2 >= 1 + Y1 && 0 >= 1 + Y1 && F1 = 0] (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 26. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1 [D1 >= 1 + C2 && K1 >= 0 && X1 >= 2 && C2 >= 1 + Y1 && Y1 >= 1 && F1 = 0] (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 27. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f0(A,B,C,D,E,F,G,H,I,X1,Y1,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,F2,E1,E2,A2,C2,D2,G2,K1,L1,M1,N1,O1,P1[X1 >= 2 && K1 >= 0 && F1 = D1] (?,1) ,R1,S1,T1,U1,V1,W1) ,Q1,R1,S1,T1,U1,V1,W1) 28. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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 -> f15(Y1,2,A2,C2,A2,F,G,H,I,Y1,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,X1,A2 [Y1 >= 2] (1,1) ,R1,S1,T1,U1,V1,W1) ,D2,P1,Q1,R1,S1,T1,U1,V1,W1) 29. f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(Y1,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 [L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && 0 >= 1 + M2 && 0 >= 1 + C && 0 >= 1 + I2] (?,1) ,R1,S1,T1,U1,V1,W1) ,K1,L1,M1,F2,O1,P1,D2,J2,Z1,T2,M2,V1,W1) 30. f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(Y1,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 [L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && 0 >= 1 + M2 && 0 >= 1 + C && I2 >= 1] (?,1) ,R1,S1,T1,U1,V1,W1) ,K1,L1,M1,F2,O1,P1,D2,J2,Z1,T2,M2,V1,W1) 31. f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(Y1,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 [L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && 0 >= 1 + M2 && C >= 1 && 0 >= 1 + I2] (?,1) ,R1,S1,T1,U1,V1,W1) ,K1,L1,M1,F2,O1,P1,D2,J2,Z1,T2,M2,V1,W1) 32. f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(Y1,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 [L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && 0 >= 1 + M2 && C >= 1 && I2 >= 1] (?,1) ,R1,S1,T1,U1,V1,W1) ,K1,L1,M1,F2,O1,P1,D2,J2,Z1,T2,M2,V1,W1) 33. f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(Y1,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 [L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && M2 >= 1 && 0 >= 1 + C && 0 >= 1 + I2] (?,1) ,R1,S1,T1,U1,V1,W1) ,K1,L1,M1,F2,O1,P1,D2,J2,Z1,T2,M2,V1,W1) 34. f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(Y1,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 [L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && M2 >= 1 && 0 >= 1 + C && I2 >= 1] (?,1) ,R1,S1,T1,U1,V1,W1) ,K1,L1,M1,F2,O1,P1,D2,J2,Z1,T2,M2,V1,W1) 35. f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(Y1,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 [L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && M2 >= 1 && C >= 1 && 0 >= 1 + I2] (?,1) ,R1,S1,T1,U1,V1,W1) ,K1,L1,M1,F2,O1,P1,D2,J2,Z1,T2,M2,V1,W1) 36. f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(Y1,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 [L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && M2 >= 1 && C >= 1 && I2 >= 1] (?,1) ,R1,S1,T1,U1,V1,W1) ,K1,L1,M1,F2,O1,P1,D2,J2,Z1,T2,M2,V1,W1) 37. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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 -> f0(A2,D2,C2,I2,H2,F,G,H,I,Y1,F2,0,J2,Z1,N2,O2,P2,Q2,R2,S2,T2,W2,X2,X,Y,K2,A1,B1,C1,C3,E1,B3,Y2,Z2,A3,D3 [0 >= U2 && 0 >= Y1 && 0 >= V2] (1,1) ,R1,S1,T1,U1,V1,W1) ,K1,L1,X1,G2,O1,P1,E2,B2,S1,T1,U1,M2,L2) 38. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,1 + K1,I,X1,Y1,L,A2,E2,F2,G2,H2,I2,J2,K2,B2,O2,P2,X,Y,C2,A1,B1,C1,L,K1,0,L,0,L,L,K1,L1[Q2 >= 2 && X1 >= 2 && I >= 0 && H >= 0 && L >= 1 && 0 >= 1 + L && Z = 0] (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,D2,S1,T1,U1,Z1,N2) 39. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,1 + K1,I,X1,Y1,L,A2,E2,F2,G2,H2,I2,J2,K2,B2,O2,P2,X,Y,C2,A1,B1,C1,L,K1,0,L,0,L,L,K1,L1[Q2 >= 2 && X1 >= 2 && I >= 0 && H >= 0 && L >= 1 && Z = 0] (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,D2,S1,T1,U1,Z1,N2) 40. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,1 + K1,I,X1,Y1,L,A2,E2,F2,G2,H2,I2,J2,K2,B2,O2,P2,X,Y,C2,A1,B1,C1,L,K1,0,L,0,L,L,K1,L1[Q2 >= 2 && X1 >= 2 && I >= 0 && H >= 0 && 0 >= 1 + L && Z = 0] (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,D2,S1,T1,U1,Z1,N2) 41. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,1 + K1,I,X1,Y1,L,A2,E2,F2,G2,H2,I2,J2,K2,B2,O2,P2,X,Y,C2,A1,B1,C1,L,K1,0,L,0,L,L,K1,L1[Q2 >= 2 && X1 >= 2 && I >= 0 && H >= 0 && 0 >= 1 + L && L >= 1 && Z = 0] (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,D2,S1,T1,U1,Z1,N2) Signature: {(f0,49);(f10,49);(f13,49);(f15,49);(f17,49);(f9,49)} Flow Graph: [0->{0,29,30,31,32,33,34,35,36},1->{1,2,3,4,5,6,7,8,38,39,40,41},2->{1,2,3,4,5,6,7,8,38,39,40,41},3->{1,2 ,3,4,5,6,7,8,38,39,40,41},4->{1,2,3,4,5,6,7,8,38,39,40,41},5->{1,2,3,4,5,6,7,8,38,39,40,41},6->{1,2,3,4,5,6 ,7,8,38,39,40,41},7->{1,2,3,4,5,6,7,8,38,39,40,41},8->{1,2,3,4,5,6,7,8,38,39,40,41},9->{19,20,21,22,23,24,25 ,26,27},10->{19,20,21,22,23,24,25,26,27},11->{19,20,21,22,23,24,25,26,27},12->{19,20,21,22,23,24,25,26,27} ,13->{19,20,21,22,23,24,25,26,27},14->{19,20,21,22,23,24,25,26,27},15->{19,20,21,22,23,24,25,26,27},16->{19 ,20,21,22,23,24,25,26,27},17->{},18->{},19->{19,20,21,22,23,24,25,26,27},20->{19,20,21,22,23,24,25,26,27} ,21->{19,20,21,22,23,24,25,26,27},22->{19,20,21,22,23,24,25,26,27},23->{19,20,21,22,23,24,25,26,27},24->{19 ,20,21,22,23,24,25,26,27},25->{19,20,21,22,23,24,25,26,27},26->{19,20,21,22,23,24,25,26,27},27->{},28->{0,29 ,30,31,32,33,34,35,36},29->{1,2,3,4,5,6,7,8,38,39,40,41},30->{1,2,3,4,5,6,7,8,38,39,40,41},31->{1,2,3,4,5,6 ,7,8,38,39,40,41},32->{1,2,3,4,5,6,7,8,38,39,40,41},33->{1,2,3,4,5,6,7,8,38,39,40,41},34->{1,2,3,4,5,6,7,8 ,38,39,40,41},35->{1,2,3,4,5,6,7,8,38,39,40,41},36->{1,2,3,4,5,6,7,8,38,39,40,41},37->{},38->{19,20,21,22,23 ,24,25,26,27},39->{19,20,21,22,23,24,25,26,27},40->{19,20,21,22,23,24,25,26,27},41->{19,20,21,22,23,24,25,26 ,27}] + Applied Processor: UnsatRules + Details: Following transitions have unsatisfiable constraints and are removed: [38,41] * Step 2: UnsatPaths YES + Considered Problem: Rules: 0. f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f15(A,1 + B,D,X1,D,Y1,B,H,I,J,K,L,M,N,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) ,R1,S1,T1,U1,V1,W1) ,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 1. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(A,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1 [H >= 0 && I >= 0 && X1 >= 2 && 0 >= 1 + Z1 && 0 >= 1 + A2 && 0 >= 1 + B2] (?,1) ,R1,S1,T1,U1,V1,W1) ,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 2. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(A,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1 [H >= 0 && I >= 0 && X1 >= 2 && 0 >= 1 + Z1 && 0 >= 1 + A2 && B2 >= 1] (?,1) ,R1,S1,T1,U1,V1,W1) ,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 3. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(A,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1 [H >= 0 && I >= 0 && X1 >= 2 && 0 >= 1 + Z1 && A2 >= 1 && 0 >= 1 + B2] (?,1) ,R1,S1,T1,U1,V1,W1) ,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 4. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(A,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1 [H >= 0 && I >= 0 && X1 >= 2 && 0 >= 1 + Z1 && A2 >= 1 && B2 >= 1] (?,1) ,R1,S1,T1,U1,V1,W1) ,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 5. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(A,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1 [H >= 0 && I >= 0 && X1 >= 2 && Z1 >= 1 && 0 >= 1 + A2 && 0 >= 1 + B2] (?,1) ,R1,S1,T1,U1,V1,W1) ,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 6. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(A,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1 [H >= 0 && I >= 0 && X1 >= 2 && Z1 >= 1 && 0 >= 1 + A2 && B2 >= 1] (?,1) ,R1,S1,T1,U1,V1,W1) ,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 7. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(A,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1 [H >= 0 && I >= 0 && X1 >= 2 && Z1 >= 1 && A2 >= 1 && 0 >= 1 + B2] (?,1) ,R1,S1,T1,U1,V1,W1) ,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 8. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(A,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1 [H >= 0 && I >= 0 && X1 >= 2 && Z1 >= 1 && A2 >= 1 && B2 >= 1] (?,1) ,R1,S1,T1,U1,V1,W1) ,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 9. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,K1,L1,M1,N1,O1,P1 [A2 >= 1 + D1 && E1 >= 0 && X1 >= 2 && Y1 >= 1 + A2 && 0 >= 1 + Y1 && F1 = 0] (?,1) ,S1,T1,U1,V1,W1) ,Q1,R1,S1,T1,U1,V1,W1) 10. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,K1,L1,M1,N1,O1,P1 [A2 >= 1 + D1 && E1 >= 0 && X1 >= 2 && Y1 >= 1 + A2 && Y1 >= 1 && F1 = 0] (?,1) ,S1,T1,U1,V1,W1) ,Q1,R1,S1,T1,U1,V1,W1) 11. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,K1,L1,M1,N1,O1,P1 [A2 >= 1 + D1 && E1 >= 0 && X1 >= 2 && A2 >= 1 + Y1 && 0 >= 1 + Y1 && F1 = 0] (?,1) ,S1,T1,U1,V1,W1) ,Q1,R1,S1,T1,U1,V1,W1) 12. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,K1,L1,M1,N1,O1,P1 [A2 >= 1 + D1 && E1 >= 0 && X1 >= 2 && A2 >= 1 + Y1 && Y1 >= 1 && F1 = 0] (?,1) ,S1,T1,U1,V1,W1) ,Q1,R1,S1,T1,U1,V1,W1) 13. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,K1,L1,M1,N1,O1,P1 [D1 >= 1 + A2 && E1 >= 0 && X1 >= 2 && Y1 >= 1 + A2 && 0 >= 1 + Y1 && F1 = 0] (?,1) ,S1,T1,U1,V1,W1) ,Q1,R1,S1,T1,U1,V1,W1) 14. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,K1,L1,M1,N1,O1,P1 [D1 >= 1 + A2 && E1 >= 0 && X1 >= 2 && Y1 >= 1 + A2 && Y1 >= 1 && F1 = 0] (?,1) ,S1,T1,U1,V1,W1) ,Q1,R1,S1,T1,U1,V1,W1) 15. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,K1,L1,M1,N1,O1,P1 [D1 >= 1 + A2 && E1 >= 0 && X1 >= 2 && A2 >= 1 + Y1 && 0 >= 1 + Y1 && F1 = 0] (?,1) ,S1,T1,U1,V1,W1) ,Q1,R1,S1,T1,U1,V1,W1) 16. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,K1,L1,M1,N1,O1,P1 [D1 >= 1 + A2 && E1 >= 0 && X1 >= 2 && A2 >= 1 + Y1 && Y1 >= 1 && F1 = 0] (?,1) ,S1,T1,U1,V1,W1) ,Q1,R1,S1,T1,U1,V1,W1) 17. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f0(A,B,C,D,E,F,G,H,I,X1,Y1,A2,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,G2,E1,F2,C2,D2,E2,H2,K1,L1,M1,N1,O1 [E1 >= 0 && 0 >= 1 + A2 && X1 >= 2 && F1 = D1] (?,1) ,S1,T1,U1,V1,W1) ,P1,Q1,R1,S1,T1,U1,V1,W1) 18. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f0(A,B,C,D,E,F,G,H,I,X1,Y1,A2,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,G2,E1,F2,C2,D2,E2,H2,K1,L1,M1,N1,O1 [E1 >= 0 && A2 >= 1 && X1 >= 2 && F1 = D1] (?,1) ,S1,T1,U1,V1,W1) ,P1,Q1,R1,S1,T1,U1,V1,W1) 19. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1 [C2 >= 1 + D1 && K1 >= 0 && X1 >= 2 && Y1 >= 1 + C2 && 0 >= 1 + Y1 && F1 = 0] (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 20. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1 [C2 >= 1 + D1 && K1 >= 0 && X1 >= 2 && Y1 >= 1 + C2 && Y1 >= 1 && F1 = 0] (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 21. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1 [C2 >= 1 + D1 && K1 >= 0 && X1 >= 2 && C2 >= 1 + Y1 && 0 >= 1 + Y1 && F1 = 0] (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 22. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1 [C2 >= 1 + D1 && K1 >= 0 && X1 >= 2 && C2 >= 1 + Y1 && Y1 >= 1 && F1 = 0] (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 23. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1 [D1 >= 1 + C2 && K1 >= 0 && X1 >= 2 && Y1 >= 1 + C2 && 0 >= 1 + Y1 && F1 = 0] (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 24. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1 [D1 >= 1 + C2 && K1 >= 0 && X1 >= 2 && Y1 >= 1 + C2 && Y1 >= 1 && F1 = 0] (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 25. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1 [D1 >= 1 + C2 && K1 >= 0 && X1 >= 2 && C2 >= 1 + Y1 && 0 >= 1 + Y1 && F1 = 0] (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 26. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1 [D1 >= 1 + C2 && K1 >= 0 && X1 >= 2 && C2 >= 1 + Y1 && Y1 >= 1 && F1 = 0] (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 27. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f0(A,B,C,D,E,F,G,H,I,X1,Y1,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,F2,E1,E2,A2,C2,D2,G2,K1,L1,M1,N1,O1,P1[X1 >= 2 && K1 >= 0 && F1 = D1] (?,1) ,R1,S1,T1,U1,V1,W1) ,Q1,R1,S1,T1,U1,V1,W1) 28. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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 -> f15(Y1,2,A2,C2,A2,F,G,H,I,Y1,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,X1,A2 [Y1 >= 2] (1,1) ,R1,S1,T1,U1,V1,W1) ,D2,P1,Q1,R1,S1,T1,U1,V1,W1) 29. f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(Y1,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 [L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && 0 >= 1 + M2 && 0 >= 1 + C && 0 >= 1 + I2] (?,1) ,R1,S1,T1,U1,V1,W1) ,K1,L1,M1,F2,O1,P1,D2,J2,Z1,T2,M2,V1,W1) 30. f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(Y1,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 [L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && 0 >= 1 + M2 && 0 >= 1 + C && I2 >= 1] (?,1) ,R1,S1,T1,U1,V1,W1) ,K1,L1,M1,F2,O1,P1,D2,J2,Z1,T2,M2,V1,W1) 31. f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(Y1,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 [L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && 0 >= 1 + M2 && C >= 1 && 0 >= 1 + I2] (?,1) ,R1,S1,T1,U1,V1,W1) ,K1,L1,M1,F2,O1,P1,D2,J2,Z1,T2,M2,V1,W1) 32. f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(Y1,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 [L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && 0 >= 1 + M2 && C >= 1 && I2 >= 1] (?,1) ,R1,S1,T1,U1,V1,W1) ,K1,L1,M1,F2,O1,P1,D2,J2,Z1,T2,M2,V1,W1) 33. f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(Y1,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 [L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && M2 >= 1 && 0 >= 1 + C && 0 >= 1 + I2] (?,1) ,R1,S1,T1,U1,V1,W1) ,K1,L1,M1,F2,O1,P1,D2,J2,Z1,T2,M2,V1,W1) 34. f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(Y1,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 [L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && M2 >= 1 && 0 >= 1 + C && I2 >= 1] (?,1) ,R1,S1,T1,U1,V1,W1) ,K1,L1,M1,F2,O1,P1,D2,J2,Z1,T2,M2,V1,W1) 35. f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(Y1,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 [L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && M2 >= 1 && C >= 1 && 0 >= 1 + I2] (?,1) ,R1,S1,T1,U1,V1,W1) ,K1,L1,M1,F2,O1,P1,D2,J2,Z1,T2,M2,V1,W1) 36. f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(Y1,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 [L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && M2 >= 1 && C >= 1 && I2 >= 1] (?,1) ,R1,S1,T1,U1,V1,W1) ,K1,L1,M1,F2,O1,P1,D2,J2,Z1,T2,M2,V1,W1) 37. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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 -> f0(A2,D2,C2,I2,H2,F,G,H,I,Y1,F2,0,J2,Z1,N2,O2,P2,Q2,R2,S2,T2,W2,X2,X,Y,K2,A1,B1,C1,C3,E1,B3,Y2,Z2,A3,D3 [0 >= U2 && 0 >= Y1 && 0 >= V2] (1,1) ,R1,S1,T1,U1,V1,W1) ,K1,L1,X1,G2,O1,P1,E2,B2,S1,T1,U1,M2,L2) 39. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,1 + K1,I,X1,Y1,L,A2,E2,F2,G2,H2,I2,J2,K2,B2,O2,P2,X,Y,C2,A1,B1,C1,L,K1,0,L,0,L,L,K1,L1[Q2 >= 2 && X1 >= 2 && I >= 0 && H >= 0 && L >= 1 && Z = 0] (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,D2,S1,T1,U1,Z1,N2) 40. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,1 + K1,I,X1,Y1,L,A2,E2,F2,G2,H2,I2,J2,K2,B2,O2,P2,X,Y,C2,A1,B1,C1,L,K1,0,L,0,L,L,K1,L1[Q2 >= 2 && X1 >= 2 && I >= 0 && H >= 0 && 0 >= 1 + L && Z = 0] (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,D2,S1,T1,U1,Z1,N2) Signature: {(f0,49);(f10,49);(f13,49);(f15,49);(f17,49);(f9,49)} Flow Graph: [0->{0,29,30,31,32,33,34,35,36},1->{1,2,3,4,5,6,7,8,39,40},2->{1,2,3,4,5,6,7,8,39,40},3->{1,2,3,4,5,6,7,8 ,39,40},4->{1,2,3,4,5,6,7,8,39,40},5->{1,2,3,4,5,6,7,8,39,40},6->{1,2,3,4,5,6,7,8,39,40},7->{1,2,3,4,5,6,7,8 ,39,40},8->{1,2,3,4,5,6,7,8,39,40},9->{19,20,21,22,23,24,25,26,27},10->{19,20,21,22,23,24,25,26,27},11->{19 ,20,21,22,23,24,25,26,27},12->{19,20,21,22,23,24,25,26,27},13->{19,20,21,22,23,24,25,26,27},14->{19,20,21,22 ,23,24,25,26,27},15->{19,20,21,22,23,24,25,26,27},16->{19,20,21,22,23,24,25,26,27},17->{},18->{},19->{19,20 ,21,22,23,24,25,26,27},20->{19,20,21,22,23,24,25,26,27},21->{19,20,21,22,23,24,25,26,27},22->{19,20,21,22,23 ,24,25,26,27},23->{19,20,21,22,23,24,25,26,27},24->{19,20,21,22,23,24,25,26,27},25->{19,20,21,22,23,24,25,26 ,27},26->{19,20,21,22,23,24,25,26,27},27->{},28->{0,29,30,31,32,33,34,35,36},29->{1,2,3,4,5,6,7,8,39,40} ,30->{1,2,3,4,5,6,7,8,39,40},31->{1,2,3,4,5,6,7,8,39,40},32->{1,2,3,4,5,6,7,8,39,40},33->{1,2,3,4,5,6,7,8,39 ,40},34->{1,2,3,4,5,6,7,8,39,40},35->{1,2,3,4,5,6,7,8,39,40},36->{1,2,3,4,5,6,7,8,39,40},37->{},39->{19,20 ,21,22,23,24,25,26,27},40->{19,20,21,22,23,24,25,26,27}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(1,39) ,(2,39) ,(3,40) ,(4,40) ,(5,39) ,(6,39) ,(7,40) ,(8,40) ,(9,26) ,(9,27) ,(16,19) ,(16,27) ,(19,26) ,(19,27) ,(26,19) ,(26,27) ,(29,39) ,(29,40) ,(30,39) ,(30,40) ,(31,39) ,(31,40) ,(32,39) ,(32,40) ,(33,39) ,(33,40) ,(34,39) ,(34,40) ,(35,39) ,(35,40) ,(36,39) ,(36,40) ,(39,19) ,(39,27) ,(40,26) ,(40,27)] * Step 3: UnreachableRules YES + Considered Problem: Rules: 0. f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f15(A,1 + B,D,X1,D,Y1,B,H,I,J,K,L,M,N,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) ,R1,S1,T1,U1,V1,W1) ,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 1. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(A,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1 [H >= 0 && I >= 0 && X1 >= 2 && 0 >= 1 + Z1 && 0 >= 1 + A2 && 0 >= 1 + B2] (?,1) ,R1,S1,T1,U1,V1,W1) ,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 2. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(A,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1 [H >= 0 && I >= 0 && X1 >= 2 && 0 >= 1 + Z1 && 0 >= 1 + A2 && B2 >= 1] (?,1) ,R1,S1,T1,U1,V1,W1) ,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 3. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(A,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1 [H >= 0 && I >= 0 && X1 >= 2 && 0 >= 1 + Z1 && A2 >= 1 && 0 >= 1 + B2] (?,1) ,R1,S1,T1,U1,V1,W1) ,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 4. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(A,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1 [H >= 0 && I >= 0 && X1 >= 2 && 0 >= 1 + Z1 && A2 >= 1 && B2 >= 1] (?,1) ,R1,S1,T1,U1,V1,W1) ,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 5. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(A,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1 [H >= 0 && I >= 0 && X1 >= 2 && Z1 >= 1 && 0 >= 1 + A2 && 0 >= 1 + B2] (?,1) ,R1,S1,T1,U1,V1,W1) ,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 6. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(A,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1 [H >= 0 && I >= 0 && X1 >= 2 && Z1 >= 1 && 0 >= 1 + A2 && B2 >= 1] (?,1) ,R1,S1,T1,U1,V1,W1) ,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 7. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(A,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1 [H >= 0 && I >= 0 && X1 >= 2 && Z1 >= 1 && A2 >= 1 && 0 >= 1 + B2] (?,1) ,R1,S1,T1,U1,V1,W1) ,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 8. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(A,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1 [H >= 0 && I >= 0 && X1 >= 2 && Z1 >= 1 && A2 >= 1 && B2 >= 1] (?,1) ,R1,S1,T1,U1,V1,W1) ,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 9. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,K1,L1,M1,N1,O1,P1 [A2 >= 1 + D1 && E1 >= 0 && X1 >= 2 && Y1 >= 1 + A2 && 0 >= 1 + Y1 && F1 = 0] (?,1) ,S1,T1,U1,V1,W1) ,Q1,R1,S1,T1,U1,V1,W1) 10. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,K1,L1,M1,N1,O1,P1 [A2 >= 1 + D1 && E1 >= 0 && X1 >= 2 && Y1 >= 1 + A2 && Y1 >= 1 && F1 = 0] (?,1) ,S1,T1,U1,V1,W1) ,Q1,R1,S1,T1,U1,V1,W1) 11. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,K1,L1,M1,N1,O1,P1 [A2 >= 1 + D1 && E1 >= 0 && X1 >= 2 && A2 >= 1 + Y1 && 0 >= 1 + Y1 && F1 = 0] (?,1) ,S1,T1,U1,V1,W1) ,Q1,R1,S1,T1,U1,V1,W1) 12. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,K1,L1,M1,N1,O1,P1 [A2 >= 1 + D1 && E1 >= 0 && X1 >= 2 && A2 >= 1 + Y1 && Y1 >= 1 && F1 = 0] (?,1) ,S1,T1,U1,V1,W1) ,Q1,R1,S1,T1,U1,V1,W1) 13. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,K1,L1,M1,N1,O1,P1 [D1 >= 1 + A2 && E1 >= 0 && X1 >= 2 && Y1 >= 1 + A2 && 0 >= 1 + Y1 && F1 = 0] (?,1) ,S1,T1,U1,V1,W1) ,Q1,R1,S1,T1,U1,V1,W1) 14. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,K1,L1,M1,N1,O1,P1 [D1 >= 1 + A2 && E1 >= 0 && X1 >= 2 && Y1 >= 1 + A2 && Y1 >= 1 && F1 = 0] (?,1) ,S1,T1,U1,V1,W1) ,Q1,R1,S1,T1,U1,V1,W1) 15. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,K1,L1,M1,N1,O1,P1 [D1 >= 1 + A2 && E1 >= 0 && X1 >= 2 && A2 >= 1 + Y1 && 0 >= 1 + Y1 && F1 = 0] (?,1) ,S1,T1,U1,V1,W1) ,Q1,R1,S1,T1,U1,V1,W1) 16. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,K1,L1,M1,N1,O1,P1 [D1 >= 1 + A2 && E1 >= 0 && X1 >= 2 && A2 >= 1 + Y1 && Y1 >= 1 && F1 = 0] (?,1) ,S1,T1,U1,V1,W1) ,Q1,R1,S1,T1,U1,V1,W1) 17. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f0(A,B,C,D,E,F,G,H,I,X1,Y1,A2,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,G2,E1,F2,C2,D2,E2,H2,K1,L1,M1,N1,O1 [E1 >= 0 && 0 >= 1 + A2 && X1 >= 2 && F1 = D1] (?,1) ,S1,T1,U1,V1,W1) ,P1,Q1,R1,S1,T1,U1,V1,W1) 18. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f0(A,B,C,D,E,F,G,H,I,X1,Y1,A2,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,G2,E1,F2,C2,D2,E2,H2,K1,L1,M1,N1,O1 [E1 >= 0 && A2 >= 1 && X1 >= 2 && F1 = D1] (?,1) ,S1,T1,U1,V1,W1) ,P1,Q1,R1,S1,T1,U1,V1,W1) 19. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1 [C2 >= 1 + D1 && K1 >= 0 && X1 >= 2 && Y1 >= 1 + C2 && 0 >= 1 + Y1 && F1 = 0] (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 20. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1 [C2 >= 1 + D1 && K1 >= 0 && X1 >= 2 && Y1 >= 1 + C2 && Y1 >= 1 && F1 = 0] (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 21. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1 [C2 >= 1 + D1 && K1 >= 0 && X1 >= 2 && C2 >= 1 + Y1 && 0 >= 1 + Y1 && F1 = 0] (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 22. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1 [C2 >= 1 + D1 && K1 >= 0 && X1 >= 2 && C2 >= 1 + Y1 && Y1 >= 1 && F1 = 0] (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 23. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1 [D1 >= 1 + C2 && K1 >= 0 && X1 >= 2 && Y1 >= 1 + C2 && 0 >= 1 + Y1 && F1 = 0] (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 24. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1 [D1 >= 1 + C2 && K1 >= 0 && X1 >= 2 && Y1 >= 1 + C2 && Y1 >= 1 && F1 = 0] (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 25. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1 [D1 >= 1 + C2 && K1 >= 0 && X1 >= 2 && C2 >= 1 + Y1 && 0 >= 1 + Y1 && F1 = 0] (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 26. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1 [D1 >= 1 + C2 && K1 >= 0 && X1 >= 2 && C2 >= 1 + Y1 && Y1 >= 1 && F1 = 0] (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 27. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f0(A,B,C,D,E,F,G,H,I,X1,Y1,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,F2,E1,E2,A2,C2,D2,G2,K1,L1,M1,N1,O1,P1[X1 >= 2 && K1 >= 0 && F1 = D1] (?,1) ,R1,S1,T1,U1,V1,W1) ,Q1,R1,S1,T1,U1,V1,W1) 28. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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 -> f15(Y1,2,A2,C2,A2,F,G,H,I,Y1,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,X1,A2 [Y1 >= 2] (1,1) ,R1,S1,T1,U1,V1,W1) ,D2,P1,Q1,R1,S1,T1,U1,V1,W1) 29. f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(Y1,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 [L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && 0 >= 1 + M2 && 0 >= 1 + C && 0 >= 1 + I2] (?,1) ,R1,S1,T1,U1,V1,W1) ,K1,L1,M1,F2,O1,P1,D2,J2,Z1,T2,M2,V1,W1) 30. f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(Y1,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 [L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && 0 >= 1 + M2 && 0 >= 1 + C && I2 >= 1] (?,1) ,R1,S1,T1,U1,V1,W1) ,K1,L1,M1,F2,O1,P1,D2,J2,Z1,T2,M2,V1,W1) 31. f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(Y1,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 [L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && 0 >= 1 + M2 && C >= 1 && 0 >= 1 + I2] (?,1) ,R1,S1,T1,U1,V1,W1) ,K1,L1,M1,F2,O1,P1,D2,J2,Z1,T2,M2,V1,W1) 32. f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(Y1,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 [L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && 0 >= 1 + M2 && C >= 1 && I2 >= 1] (?,1) ,R1,S1,T1,U1,V1,W1) ,K1,L1,M1,F2,O1,P1,D2,J2,Z1,T2,M2,V1,W1) 33. f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(Y1,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 [L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && M2 >= 1 && 0 >= 1 + C && 0 >= 1 + I2] (?,1) ,R1,S1,T1,U1,V1,W1) ,K1,L1,M1,F2,O1,P1,D2,J2,Z1,T2,M2,V1,W1) 34. f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(Y1,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 [L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && M2 >= 1 && 0 >= 1 + C && I2 >= 1] (?,1) ,R1,S1,T1,U1,V1,W1) ,K1,L1,M1,F2,O1,P1,D2,J2,Z1,T2,M2,V1,W1) 35. f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(Y1,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 [L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && M2 >= 1 && C >= 1 && 0 >= 1 + I2] (?,1) ,R1,S1,T1,U1,V1,W1) ,K1,L1,M1,F2,O1,P1,D2,J2,Z1,T2,M2,V1,W1) 36. f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(Y1,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 [L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && M2 >= 1 && C >= 1 && I2 >= 1] (?,1) ,R1,S1,T1,U1,V1,W1) ,K1,L1,M1,F2,O1,P1,D2,J2,Z1,T2,M2,V1,W1) 37. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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 -> f0(A2,D2,C2,I2,H2,F,G,H,I,Y1,F2,0,J2,Z1,N2,O2,P2,Q2,R2,S2,T2,W2,X2,X,Y,K2,A1,B1,C1,C3,E1,B3,Y2,Z2,A3,D3 [0 >= U2 && 0 >= Y1 && 0 >= V2] (1,1) ,R1,S1,T1,U1,V1,W1) ,K1,L1,X1,G2,O1,P1,E2,B2,S1,T1,U1,M2,L2) 39. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,1 + K1,I,X1,Y1,L,A2,E2,F2,G2,H2,I2,J2,K2,B2,O2,P2,X,Y,C2,A1,B1,C1,L,K1,0,L,0,L,L,K1,L1[Q2 >= 2 && X1 >= 2 && I >= 0 && H >= 0 && L >= 1 && Z = 0] (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,D2,S1,T1,U1,Z1,N2) 40. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,1 + K1,I,X1,Y1,L,A2,E2,F2,G2,H2,I2,J2,K2,B2,O2,P2,X,Y,C2,A1,B1,C1,L,K1,0,L,0,L,L,K1,L1[Q2 >= 2 && X1 >= 2 && I >= 0 && H >= 0 && 0 >= 1 + L && Z = 0] (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,D2,S1,T1,U1,Z1,N2) Signature: {(f0,49);(f10,49);(f13,49);(f15,49);(f17,49);(f9,49)} Flow Graph: [0->{0,29,30,31,32,33,34,35,36},1->{1,2,3,4,5,6,7,8,40},2->{1,2,3,4,5,6,7,8,40},3->{1,2,3,4,5,6,7,8,39} ,4->{1,2,3,4,5,6,7,8,39},5->{1,2,3,4,5,6,7,8,40},6->{1,2,3,4,5,6,7,8,40},7->{1,2,3,4,5,6,7,8,39},8->{1,2,3,4 ,5,6,7,8,39},9->{19,20,21,22,23,24,25},10->{19,20,21,22,23,24,25,26,27},11->{19,20,21,22,23,24,25,26,27} ,12->{19,20,21,22,23,24,25,26,27},13->{19,20,21,22,23,24,25,26,27},14->{19,20,21,22,23,24,25,26,27},15->{19 ,20,21,22,23,24,25,26,27},16->{20,21,22,23,24,25,26},17->{},18->{},19->{19,20,21,22,23,24,25},20->{19,20,21 ,22,23,24,25,26,27},21->{19,20,21,22,23,24,25,26,27},22->{19,20,21,22,23,24,25,26,27},23->{19,20,21,22,23,24 ,25,26,27},24->{19,20,21,22,23,24,25,26,27},25->{19,20,21,22,23,24,25,26,27},26->{20,21,22,23,24,25,26} ,27->{},28->{0,29,30,31,32,33,34,35,36},29->{1,2,3,4,5,6,7,8},30->{1,2,3,4,5,6,7,8},31->{1,2,3,4,5,6,7,8} ,32->{1,2,3,4,5,6,7,8},33->{1,2,3,4,5,6,7,8},34->{1,2,3,4,5,6,7,8},35->{1,2,3,4,5,6,7,8},36->{1,2,3,4,5,6,7 ,8},37->{},39->{20,21,22,23,24,25,26},40->{19,20,21,22,23,24,25}] + Applied Processor: UnreachableRules + Details: Following transitions are not reachable from the starting states and are revomed: [9 ,10 ,11 ,12 ,13 ,14 ,15 ,16 ,17 ,18] * Step 4: FromIts YES + Considered Problem: Rules: 0. f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f15(A,1 + B,D,X1,D,Y1,B,H,I,J,K,L,M,N,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) ,R1,S1,T1,U1,V1,W1) ,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 1. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(A,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1 [H >= 0 && I >= 0 && X1 >= 2 && 0 >= 1 + Z1 && 0 >= 1 + A2 && 0 >= 1 + B2] (?,1) ,R1,S1,T1,U1,V1,W1) ,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 2. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(A,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1 [H >= 0 && I >= 0 && X1 >= 2 && 0 >= 1 + Z1 && 0 >= 1 + A2 && B2 >= 1] (?,1) ,R1,S1,T1,U1,V1,W1) ,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 3. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(A,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1 [H >= 0 && I >= 0 && X1 >= 2 && 0 >= 1 + Z1 && A2 >= 1 && 0 >= 1 + B2] (?,1) ,R1,S1,T1,U1,V1,W1) ,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 4. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(A,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1 [H >= 0 && I >= 0 && X1 >= 2 && 0 >= 1 + Z1 && A2 >= 1 && B2 >= 1] (?,1) ,R1,S1,T1,U1,V1,W1) ,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 5. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(A,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1 [H >= 0 && I >= 0 && X1 >= 2 && Z1 >= 1 && 0 >= 1 + A2 && 0 >= 1 + B2] (?,1) ,R1,S1,T1,U1,V1,W1) ,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 6. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(A,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1 [H >= 0 && I >= 0 && X1 >= 2 && Z1 >= 1 && 0 >= 1 + A2 && B2 >= 1] (?,1) ,R1,S1,T1,U1,V1,W1) ,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 7. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(A,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1 [H >= 0 && I >= 0 && X1 >= 2 && Z1 >= 1 && A2 >= 1 && 0 >= 1 + B2] (?,1) ,R1,S1,T1,U1,V1,W1) ,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 8. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(A,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1 [H >= 0 && I >= 0 && X1 >= 2 && Z1 >= 1 && A2 >= 1 && B2 >= 1] (?,1) ,R1,S1,T1,U1,V1,W1) ,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 19. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1 [C2 >= 1 + D1 && K1 >= 0 && X1 >= 2 && Y1 >= 1 + C2 && 0 >= 1 + Y1 && F1 = 0] (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 20. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1 [C2 >= 1 + D1 && K1 >= 0 && X1 >= 2 && Y1 >= 1 + C2 && Y1 >= 1 && F1 = 0] (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 21. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1 [C2 >= 1 + D1 && K1 >= 0 && X1 >= 2 && C2 >= 1 + Y1 && 0 >= 1 + Y1 && F1 = 0] (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 22. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1 [C2 >= 1 + D1 && K1 >= 0 && X1 >= 2 && C2 >= 1 + Y1 && Y1 >= 1 && F1 = 0] (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 23. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1 [D1 >= 1 + C2 && K1 >= 0 && X1 >= 2 && Y1 >= 1 + C2 && 0 >= 1 + Y1 && F1 = 0] (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 24. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1 [D1 >= 1 + C2 && K1 >= 0 && X1 >= 2 && Y1 >= 1 + C2 && Y1 >= 1 && F1 = 0] (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 25. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1 [D1 >= 1 + C2 && K1 >= 0 && X1 >= 2 && C2 >= 1 + Y1 && 0 >= 1 + Y1 && F1 = 0] (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 26. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1 [D1 >= 1 + C2 && K1 >= 0 && X1 >= 2 && C2 >= 1 + Y1 && Y1 >= 1 && F1 = 0] (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 27. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f0(A,B,C,D,E,F,G,H,I,X1,Y1,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,F2,E1,E2,A2,C2,D2,G2,K1,L1,M1,N1,O1,P1[X1 >= 2 && K1 >= 0 && F1 = D1] (?,1) ,R1,S1,T1,U1,V1,W1) ,Q1,R1,S1,T1,U1,V1,W1) 28. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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 -> f15(Y1,2,A2,C2,A2,F,G,H,I,Y1,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,X1,A2 [Y1 >= 2] (1,1) ,R1,S1,T1,U1,V1,W1) ,D2,P1,Q1,R1,S1,T1,U1,V1,W1) 29. f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(Y1,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 [L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && 0 >= 1 + M2 && 0 >= 1 + C && 0 >= 1 + I2] (?,1) ,R1,S1,T1,U1,V1,W1) ,K1,L1,M1,F2,O1,P1,D2,J2,Z1,T2,M2,V1,W1) 30. f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(Y1,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 [L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && 0 >= 1 + M2 && 0 >= 1 + C && I2 >= 1] (?,1) ,R1,S1,T1,U1,V1,W1) ,K1,L1,M1,F2,O1,P1,D2,J2,Z1,T2,M2,V1,W1) 31. f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(Y1,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 [L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && 0 >= 1 + M2 && C >= 1 && 0 >= 1 + I2] (?,1) ,R1,S1,T1,U1,V1,W1) ,K1,L1,M1,F2,O1,P1,D2,J2,Z1,T2,M2,V1,W1) 32. f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(Y1,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 [L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && 0 >= 1 + M2 && C >= 1 && I2 >= 1] (?,1) ,R1,S1,T1,U1,V1,W1) ,K1,L1,M1,F2,O1,P1,D2,J2,Z1,T2,M2,V1,W1) 33. f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(Y1,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 [L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && M2 >= 1 && 0 >= 1 + C && 0 >= 1 + I2] (?,1) ,R1,S1,T1,U1,V1,W1) ,K1,L1,M1,F2,O1,P1,D2,J2,Z1,T2,M2,V1,W1) 34. f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(Y1,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 [L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && M2 >= 1 && 0 >= 1 + C && I2 >= 1] (?,1) ,R1,S1,T1,U1,V1,W1) ,K1,L1,M1,F2,O1,P1,D2,J2,Z1,T2,M2,V1,W1) 35. f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(Y1,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 [L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && M2 >= 1 && C >= 1 && 0 >= 1 + I2] (?,1) ,R1,S1,T1,U1,V1,W1) ,K1,L1,M1,F2,O1,P1,D2,J2,Z1,T2,M2,V1,W1) 36. f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(Y1,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 [L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && M2 >= 1 && C >= 1 && I2 >= 1] (?,1) ,R1,S1,T1,U1,V1,W1) ,K1,L1,M1,F2,O1,P1,D2,J2,Z1,T2,M2,V1,W1) 37. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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 -> f0(A2,D2,C2,I2,H2,F,G,H,I,Y1,F2,0,J2,Z1,N2,O2,P2,Q2,R2,S2,T2,W2,X2,X,Y,K2,A1,B1,C1,C3,E1,B3,Y2,Z2,A3,D3 [0 >= U2 && 0 >= Y1 && 0 >= V2] (1,1) ,R1,S1,T1,U1,V1,W1) ,K1,L1,X1,G2,O1,P1,E2,B2,S1,T1,U1,M2,L2) 39. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,1 + K1,I,X1,Y1,L,A2,E2,F2,G2,H2,I2,J2,K2,B2,O2,P2,X,Y,C2,A1,B1,C1,L,K1,0,L,0,L,L,K1,L1[Q2 >= 2 && X1 >= 2 && I >= 0 && H >= 0 && L >= 1 && Z = 0] (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,D2,S1,T1,U1,Z1,N2) 40. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,1 + K1,I,X1,Y1,L,A2,E2,F2,G2,H2,I2,J2,K2,B2,O2,P2,X,Y,C2,A1,B1,C1,L,K1,0,L,0,L,L,K1,L1[Q2 >= 2 && X1 >= 2 && I >= 0 && H >= 0 && 0 >= 1 + L && Z = 0] (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,D2,S1,T1,U1,Z1,N2) Signature: {(f0,49);(f10,49);(f13,49);(f15,49);(f17,49);(f9,49)} Flow Graph: [0->{0,29,30,31,32,33,34,35,36},1->{1,2,3,4,5,6,7,8,40},2->{1,2,3,4,5,6,7,8,40},3->{1,2,3,4,5,6,7,8,39} ,4->{1,2,3,4,5,6,7,8,39},5->{1,2,3,4,5,6,7,8,40},6->{1,2,3,4,5,6,7,8,40},7->{1,2,3,4,5,6,7,8,39},8->{1,2,3,4 ,5,6,7,8,39},19->{19,20,21,22,23,24,25},20->{19,20,21,22,23,24,25,26,27},21->{19,20,21,22,23,24,25,26,27} ,22->{19,20,21,22,23,24,25,26,27},23->{19,20,21,22,23,24,25,26,27},24->{19,20,21,22,23,24,25,26,27},25->{19 ,20,21,22,23,24,25,26,27},26->{20,21,22,23,24,25,26},27->{},28->{0,29,30,31,32,33,34,35,36},29->{1,2,3,4,5,6 ,7,8},30->{1,2,3,4,5,6,7,8},31->{1,2,3,4,5,6,7,8},32->{1,2,3,4,5,6,7,8},33->{1,2,3,4,5,6,7,8},34->{1,2,3,4,5 ,6,7,8},35->{1,2,3,4,5,6,7,8},36->{1,2,3,4,5,6,7,8},37->{},39->{20,21,22,23,24,25,26},40->{19,20,21,22,23,24 ,25}] + Applied Processor: FromIts + Details: () * Step 5: Decompose YES + Considered Problem: Rules: f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f15(A ,1 + B,D,X1,D,Y1,B,H,I,J,K,L,M,N,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) [A >= 1 + B && B >= 0] f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,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) -> f13(A ,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1,G1,H1,I1 ,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1 ,W1) [H >= 0 && I >= 0 && X1 >= 2 && 0 >= 1 + Z1 && 0 >= 1 + A2 && 0 >= 1 + B2] f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(A ,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1,G1,H1,I1 ,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1 ,W1) [H >= 0 && I >= 0 && X1 >= 2 && 0 >= 1 + Z1 && 0 >= 1 + A2 && B2 >= 1] f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(A ,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1,G1,H1,I1 ,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1 ,W1) [H >= 0 && I >= 0 && X1 >= 2 && 0 >= 1 + Z1 && A2 >= 1 && 0 >= 1 + B2] f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(A ,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1,G1,H1,I1 ,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1 ,W1) [H >= 0 && I >= 0 && X1 >= 2 && 0 >= 1 + Z1 && A2 >= 1 && B2 >= 1] f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(A ,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1,G1,H1,I1 ,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1 ,W1) [H >= 0 && I >= 0 && X1 >= 2 && Z1 >= 1 && 0 >= 1 + A2 && 0 >= 1 + B2] f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(A ,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1,G1,H1,I1 ,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1 ,W1) [H >= 0 && I >= 0 && X1 >= 2 && Z1 >= 1 && 0 >= 1 + A2 && B2 >= 1] f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(A ,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1,G1,H1,I1 ,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1 ,W1) [H >= 0 && I >= 0 && X1 >= 2 && Z1 >= 1 && A2 >= 1 && 0 >= 1 + B2] f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(A ,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1,G1,H1,I1 ,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1 ,W1) [H >= 0 && I >= 0 && X1 >= 2 && Z1 >= 1 && A2 >= 1 && B2 >= 1] f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f10(A ,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1,M1,N1,O1 ,P1,Q1,R1,S1,T1,U1,V1 ,W1) [C2 >= 1 + D1 && K1 >= 0 && X1 >= 2 && Y1 >= 1 + C2 && 0 >= 1 + Y1 && F1 = 0] f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,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) -> f10(A ,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1,M1,N1,O1 ,P1,Q1,R1,S1,T1,U1,V1 ,W1) [C2 >= 1 + D1 && K1 >= 0 && X1 >= 2 && Y1 >= 1 + C2 && Y1 >= 1 && F1 = 0] f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,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) -> f10(A ,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1,M1,N1,O1 ,P1,Q1,R1,S1,T1,U1,V1 ,W1) [C2 >= 1 + D1 && K1 >= 0 && X1 >= 2 && C2 >= 1 + Y1 && 0 >= 1 + Y1 && F1 = 0] f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,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) -> f10(A ,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1,M1,N1,O1 ,P1,Q1,R1,S1,T1,U1,V1 ,W1) [C2 >= 1 + D1 && K1 >= 0 && X1 >= 2 && C2 >= 1 + Y1 && Y1 >= 1 && F1 = 0] f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,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) -> f10(A ,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1,M1,N1,O1 ,P1,Q1,R1,S1,T1,U1,V1 ,W1) [D1 >= 1 + C2 && K1 >= 0 && X1 >= 2 && Y1 >= 1 + C2 && 0 >= 1 + Y1 && F1 = 0] f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,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) -> f10(A ,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1,M1,N1,O1 ,P1,Q1,R1,S1,T1,U1,V1 ,W1) [D1 >= 1 + C2 && K1 >= 0 && X1 >= 2 && Y1 >= 1 + C2 && Y1 >= 1 && F1 = 0] f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,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) -> f10(A ,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1,M1,N1,O1 ,P1,Q1,R1,S1,T1,U1,V1 ,W1) [D1 >= 1 + C2 && K1 >= 0 && X1 >= 2 && C2 >= 1 + Y1 && 0 >= 1 + Y1 && F1 = 0] f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,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) -> f10(A ,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1,M1,N1,O1 ,P1,Q1,R1,S1,T1,U1,V1 ,W1) [D1 >= 1 + C2 && K1 >= 0 && X1 >= 2 && C2 >= 1 + Y1 && Y1 >= 1 && F1 = 0] f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,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) -> f0(A ,B,C,D,E,F,G,H,I,X1,Y1,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,F2,E1,E2,A2,C2,D2,G2,K1,L1,M1,N1,O1,P1,Q1,R1 ,S1,T1,U1,V1 ,W1) [X1 >= 2 && K1 >= 0 && F1 = D1] f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f15(Y1 ,2,A2,C2,A2,F,G,H,I,Y1,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,X1,A2,D2,P1,Q1,R1 ,S1,T1,U1,V1 ,W1) [Y1 >= 2] f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(Y1 ,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,F2 ,O1,P1,D2,J2,Z1,T2,M2,V1 ,W1) [L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && 0 >= 1 + M2 && 0 >= 1 + C && 0 >= 1 + I2] f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(Y1 ,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,F2 ,O1,P1,D2,J2,Z1,T2,M2,V1 ,W1) [L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && 0 >= 1 + M2 && 0 >= 1 + C && I2 >= 1] f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(Y1 ,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,F2 ,O1,P1,D2,J2,Z1,T2,M2,V1 ,W1) [L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && 0 >= 1 + M2 && C >= 1 && 0 >= 1 + I2] f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(Y1 ,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,F2 ,O1,P1,D2,J2,Z1,T2,M2,V1 ,W1) [L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && 0 >= 1 + M2 && C >= 1 && I2 >= 1] f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(Y1 ,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,F2 ,O1,P1,D2,J2,Z1,T2,M2,V1 ,W1) [L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && M2 >= 1 && 0 >= 1 + C && 0 >= 1 + I2] f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(Y1 ,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,F2 ,O1,P1,D2,J2,Z1,T2,M2,V1 ,W1) [L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && M2 >= 1 && 0 >= 1 + C && I2 >= 1] f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(Y1 ,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,F2 ,O1,P1,D2,J2,Z1,T2,M2,V1 ,W1) [L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && M2 >= 1 && C >= 1 && 0 >= 1 + I2] f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(Y1 ,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,F2 ,O1,P1,D2,J2,Z1,T2,M2,V1 ,W1) [L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && M2 >= 1 && C >= 1 && I2 >= 1] f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f0(A2 ,D2,C2,I2,H2,F,G,H,I,Y1,F2,0,J2,Z1,N2,O2,P2,Q2,R2,S2,T2,W2,X2,X,Y,K2,A1,B1,C1,C3,E1,B3,Y2,Z2,A3,D3,K1,L1,X1 ,G2,O1,P1,E2,B2,S1,T1,U1,M2 ,L2) [0 >= U2 && 0 >= Y1 && 0 >= V2] f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f10(A ,B,C,D,E,F,G,1 + K1,I,X1,Y1,L,A2,E2,F2,G2,H2,I2,J2,K2,B2,O2,P2,X,Y,C2,A1,B1,C1,L,K1,0,L,0,L,L,K1,L1,M1,N1,O1 ,P1,Q1,D2,S1,T1,U1,Z1 ,N2) [Q2 >= 2 && X1 >= 2 && I >= 0 && H >= 0 && L >= 1 && Z = 0] f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,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) -> f10(A ,B,C,D,E,F,G,1 + K1,I,X1,Y1,L,A2,E2,F2,G2,H2,I2,J2,K2,B2,O2,P2,X,Y,C2,A1,B1,C1,L,K1,0,L,0,L,L,K1,L1,M1,N1,O1 ,P1,Q1,D2,S1,T1,U1,Z1 ,N2) [Q2 >= 2 && X1 >= 2 && I >= 0 && H >= 0 && 0 >= 1 + L && Z = 0] Signature: {(f0,49);(f10,49);(f13,49);(f15,49);(f17,49);(f9,49)} Rule Graph: [0->{0,29,30,31,32,33,34,35,36},1->{1,2,3,4,5,6,7,8,40},2->{1,2,3,4,5,6,7,8,40},3->{1,2,3,4,5,6,7,8,39} ,4->{1,2,3,4,5,6,7,8,39},5->{1,2,3,4,5,6,7,8,40},6->{1,2,3,4,5,6,7,8,40},7->{1,2,3,4,5,6,7,8,39},8->{1,2,3,4 ,5,6,7,8,39},19->{19,20,21,22,23,24,25},20->{19,20,21,22,23,24,25,26,27},21->{19,20,21,22,23,24,25,26,27} ,22->{19,20,21,22,23,24,25,26,27},23->{19,20,21,22,23,24,25,26,27},24->{19,20,21,22,23,24,25,26,27},25->{19 ,20,21,22,23,24,25,26,27},26->{20,21,22,23,24,25,26},27->{},28->{0,29,30,31,32,33,34,35,36},29->{1,2,3,4,5,6 ,7,8},30->{1,2,3,4,5,6,7,8},31->{1,2,3,4,5,6,7,8},32->{1,2,3,4,5,6,7,8},33->{1,2,3,4,5,6,7,8},34->{1,2,3,4,5 ,6,7,8},35->{1,2,3,4,5,6,7,8},36->{1,2,3,4,5,6,7,8},37->{},39->{20,21,22,23,24,25,26},40->{19,20,21,22,23,24 ,25}] + Applied Processor: Decompose NoGreedy + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,39,40] | +- p:[0] c: [0] | +- p:[1,2,3,4,5,6,7,8] c: [8] | | | `- p:[1,2,3,4,5,6,7] c: [7] | | | `- p:[1,2,3,4,5,6] c: [6] | | | `- p:[1,2,3,4,5] c: [5] | | | `- p:[1,2,3,4] c: [4] | | | `- p:[1,2,3] c: [3] | | | `- p:[1,2] c: [2] | | | `- p:[1] c: [1] | `- p:[20,19,21,22,23,24,25,26] c: [26] | `- p:[19,20,21,22,23,24,25] c: [25] | `- p:[19,20,21,22,23,24] c: [24] | `- p:[19,20,21,22,23] c: [23] | `- p:[19,20,21,22] c: [22] | `- p:[19,20,21] c: [21] | `- p:[19,20] c: [20] | `- p:[19] c: [19] * Step 6: CloseWith YES + Considered Problem: (Rules: f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f15(A ,1 + B,D,X1,D,Y1,B,H,I,J,K,L,M,N,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) [A >= 1 + B && B >= 0] f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,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) -> f13(A ,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1,G1,H1,I1 ,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1 ,W1) [H >= 0 && I >= 0 && X1 >= 2 && 0 >= 1 + Z1 && 0 >= 1 + A2 && 0 >= 1 + B2] f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(A ,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1,G1,H1,I1 ,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1 ,W1) [H >= 0 && I >= 0 && X1 >= 2 && 0 >= 1 + Z1 && 0 >= 1 + A2 && B2 >= 1] f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(A ,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1,G1,H1,I1 ,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1 ,W1) [H >= 0 && I >= 0 && X1 >= 2 && 0 >= 1 + Z1 && A2 >= 1 && 0 >= 1 + B2] f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(A ,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1,G1,H1,I1 ,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1 ,W1) [H >= 0 && I >= 0 && X1 >= 2 && 0 >= 1 + Z1 && A2 >= 1 && B2 >= 1] f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(A ,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1,G1,H1,I1 ,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1 ,W1) [H >= 0 && I >= 0 && X1 >= 2 && Z1 >= 1 && 0 >= 1 + A2 && 0 >= 1 + B2] f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(A ,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1,G1,H1,I1 ,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1 ,W1) [H >= 0 && I >= 0 && X1 >= 2 && Z1 >= 1 && 0 >= 1 + A2 && B2 >= 1] f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(A ,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1,G1,H1,I1 ,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1 ,W1) [H >= 0 && I >= 0 && X1 >= 2 && Z1 >= 1 && A2 >= 1 && 0 >= 1 + B2] f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(A ,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1,G1,H1,I1 ,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1 ,W1) [H >= 0 && I >= 0 && X1 >= 2 && Z1 >= 1 && A2 >= 1 && B2 >= 1] f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f10(A ,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1,M1,N1,O1 ,P1,Q1,R1,S1,T1,U1,V1 ,W1) [C2 >= 1 + D1 && K1 >= 0 && X1 >= 2 && Y1 >= 1 + C2 && 0 >= 1 + Y1 && F1 = 0] f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,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) -> f10(A ,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1,M1,N1,O1 ,P1,Q1,R1,S1,T1,U1,V1 ,W1) [C2 >= 1 + D1 && K1 >= 0 && X1 >= 2 && Y1 >= 1 + C2 && Y1 >= 1 && F1 = 0] f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,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) -> f10(A ,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1,M1,N1,O1 ,P1,Q1,R1,S1,T1,U1,V1 ,W1) [C2 >= 1 + D1 && K1 >= 0 && X1 >= 2 && C2 >= 1 + Y1 && 0 >= 1 + Y1 && F1 = 0] f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,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) -> f10(A ,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1,M1,N1,O1 ,P1,Q1,R1,S1,T1,U1,V1 ,W1) [C2 >= 1 + D1 && K1 >= 0 && X1 >= 2 && C2 >= 1 + Y1 && Y1 >= 1 && F1 = 0] f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,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) -> f10(A ,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1,M1,N1,O1 ,P1,Q1,R1,S1,T1,U1,V1 ,W1) [D1 >= 1 + C2 && K1 >= 0 && X1 >= 2 && Y1 >= 1 + C2 && 0 >= 1 + Y1 && F1 = 0] f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,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) -> f10(A ,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1,M1,N1,O1 ,P1,Q1,R1,S1,T1,U1,V1 ,W1) [D1 >= 1 + C2 && K1 >= 0 && X1 >= 2 && Y1 >= 1 + C2 && Y1 >= 1 && F1 = 0] f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,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) -> f10(A ,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1,M1,N1,O1 ,P1,Q1,R1,S1,T1,U1,V1 ,W1) [D1 >= 1 + C2 && K1 >= 0 && X1 >= 2 && C2 >= 1 + Y1 && 0 >= 1 + Y1 && F1 = 0] f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,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) -> f10(A ,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1,M1,N1,O1 ,P1,Q1,R1,S1,T1,U1,V1 ,W1) [D1 >= 1 + C2 && K1 >= 0 && X1 >= 2 && C2 >= 1 + Y1 && Y1 >= 1 && F1 = 0] f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,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) -> f0(A ,B,C,D,E,F,G,H,I,X1,Y1,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,F2,E1,E2,A2,C2,D2,G2,K1,L1,M1,N1,O1,P1,Q1,R1 ,S1,T1,U1,V1 ,W1) [X1 >= 2 && K1 >= 0 && F1 = D1] f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f15(Y1 ,2,A2,C2,A2,F,G,H,I,Y1,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,X1,A2,D2,P1,Q1,R1 ,S1,T1,U1,V1 ,W1) [Y1 >= 2] f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(Y1 ,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,F2 ,O1,P1,D2,J2,Z1,T2,M2,V1 ,W1) [L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && 0 >= 1 + M2 && 0 >= 1 + C && 0 >= 1 + I2] f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(Y1 ,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,F2 ,O1,P1,D2,J2,Z1,T2,M2,V1 ,W1) [L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && 0 >= 1 + M2 && 0 >= 1 + C && I2 >= 1] f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(Y1 ,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,F2 ,O1,P1,D2,J2,Z1,T2,M2,V1 ,W1) [L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && 0 >= 1 + M2 && C >= 1 && 0 >= 1 + I2] f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(Y1 ,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,F2 ,O1,P1,D2,J2,Z1,T2,M2,V1 ,W1) [L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && 0 >= 1 + M2 && C >= 1 && I2 >= 1] f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(Y1 ,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,F2 ,O1,P1,D2,J2,Z1,T2,M2,V1 ,W1) [L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && M2 >= 1 && 0 >= 1 + C && 0 >= 1 + I2] f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(Y1 ,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,F2 ,O1,P1,D2,J2,Z1,T2,M2,V1 ,W1) [L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && M2 >= 1 && 0 >= 1 + C && I2 >= 1] f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(Y1 ,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,F2 ,O1,P1,D2,J2,Z1,T2,M2,V1 ,W1) [L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && M2 >= 1 && C >= 1 && 0 >= 1 + I2] f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(Y1 ,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,F2 ,O1,P1,D2,J2,Z1,T2,M2,V1 ,W1) [L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && M2 >= 1 && C >= 1 && I2 >= 1] f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f0(A2 ,D2,C2,I2,H2,F,G,H,I,Y1,F2,0,J2,Z1,N2,O2,P2,Q2,R2,S2,T2,W2,X2,X,Y,K2,A1,B1,C1,C3,E1,B3,Y2,Z2,A3,D3,K1,L1,X1 ,G2,O1,P1,E2,B2,S1,T1,U1,M2 ,L2) [0 >= U2 && 0 >= Y1 && 0 >= V2] f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f10(A ,B,C,D,E,F,G,1 + K1,I,X1,Y1,L,A2,E2,F2,G2,H2,I2,J2,K2,B2,O2,P2,X,Y,C2,A1,B1,C1,L,K1,0,L,0,L,L,K1,L1,M1,N1,O1 ,P1,Q1,D2,S1,T1,U1,Z1 ,N2) [Q2 >= 2 && X1 >= 2 && I >= 0 && H >= 0 && L >= 1 && Z = 0] f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,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) -> f10(A ,B,C,D,E,F,G,1 + K1,I,X1,Y1,L,A2,E2,F2,G2,H2,I2,J2,K2,B2,O2,P2,X,Y,C2,A1,B1,C1,L,K1,0,L,0,L,L,K1,L1,M1,N1,O1 ,P1,Q1,D2,S1,T1,U1,Z1 ,N2) [Q2 >= 2 && X1 >= 2 && I >= 0 && H >= 0 && 0 >= 1 + L && Z = 0] Signature: {(f0,49);(f10,49);(f13,49);(f15,49);(f17,49);(f9,49)} Rule Graph: [0->{0,29,30,31,32,33,34,35,36},1->{1,2,3,4,5,6,7,8,40},2->{1,2,3,4,5,6,7,8,40},3->{1,2,3,4,5,6,7,8,39} ,4->{1,2,3,4,5,6,7,8,39},5->{1,2,3,4,5,6,7,8,40},6->{1,2,3,4,5,6,7,8,40},7->{1,2,3,4,5,6,7,8,39},8->{1,2,3,4 ,5,6,7,8,39},19->{19,20,21,22,23,24,25},20->{19,20,21,22,23,24,25,26,27},21->{19,20,21,22,23,24,25,26,27} ,22->{19,20,21,22,23,24,25,26,27},23->{19,20,21,22,23,24,25,26,27},24->{19,20,21,22,23,24,25,26,27},25->{19 ,20,21,22,23,24,25,26,27},26->{20,21,22,23,24,25,26},27->{},28->{0,29,30,31,32,33,34,35,36},29->{1,2,3,4,5,6 ,7,8},30->{1,2,3,4,5,6,7,8},31->{1,2,3,4,5,6,7,8},32->{1,2,3,4,5,6,7,8},33->{1,2,3,4,5,6,7,8},34->{1,2,3,4,5 ,6,7,8},35->{1,2,3,4,5,6,7,8},36->{1,2,3,4,5,6,7,8},37->{},39->{20,21,22,23,24,25,26},40->{19,20,21,22,23,24 ,25}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,39,40] | +- p:[0] c: [0] | +- p:[1,2,3,4,5,6,7,8] c: [8] | | | `- p:[1,2,3,4,5,6,7] c: [7] | | | `- p:[1,2,3,4,5,6] c: [6] | | | `- p:[1,2,3,4,5] c: [5] | | | `- p:[1,2,3,4] c: [4] | | | `- p:[1,2,3] c: [3] | | | `- p:[1,2] c: [2] | | | `- p:[1] c: [1] | `- p:[20,19,21,22,23,24,25,26] c: [26] | `- p:[19,20,21,22,23,24,25] c: [25] | `- p:[19,20,21,22,23,24] c: [24] | `- p:[19,20,21,22,23] c: [23] | `- p:[19,20,21,22] c: [22] | `- p:[19,20,21] c: [21] | `- p:[19,20] c: [20] | `- p:[19] c: [19]) + Applied Processor: CloseWith True + Details: () YES