YES * Step 1: UnsatPaths YES + Considered Problem: Rules: 0. f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> 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) True (1,1) 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) -> f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A >= B] (?,1) 2. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f8(A,B,1 + C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A >= C] (?,1) 3. 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) -> f17(A,1 + B,C,B1,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A >= B] (?,1) 4. f27(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f31(A,B,C,D,E,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [50 >= E] (?,1) 5. f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f34(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A >= 1 + B] (?,1) 6. f34(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f34(A,B,1 + C,D,E,B1 + F,B1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A >= C] (?,1) 7. f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f50(A,B,C,D,E,F,G,B1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [3 >= E] (?,1) 8. f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f50(A,B,C,D,E,F,G,0,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [E >= 4] (?,1) 9. f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A >= 1 + B] (?,1) 10. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f53(A,B,1 + C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [H >= I] (?,1) 11. f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f53(A,B,1 + C,D,E,F,G,H,I,B1,100*B1,C1,100*B1 + C1,D1,100*B1 + D1,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A >= C && E >= 5] (?,1) 12. f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f69(A,B,C,D,E,F,G,H,C1,B1,100*B1,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A >= C && 4 >= E] (?,1) 13. f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f69(A,B,C,D,E,F,G,H,F1,B1,100*B1,C1,100*B1 + C1,D1,E1,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [E >= 5 && A >= C && E1 >= 1 + 100*B1 + D1] (?,1) 14. f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f69(A,B,C,D,E,F,G,H,F1,B1,100*B1,C1,100*B1 + C1,D1,E1,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [E >= 5 && A >= C && 100*B1 + D1 >= 1 + E1] (?,1) 15. f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f69(A,B,C,D,E,F,G,H,E1,B1,100*B1,C1,D1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [E >= 5 && A >= C && D1 >= 1 + 100*B1 + C1] (?,1) 16. f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f69(A,B,C,D,E,F,G,H,E1,B1,100*B1,C1,D1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [E >= 5 && A >= C && 100*B1 + C1 >= 1 + D1] (?,1) 17. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,B1 + -1*C1,D1,E1,F1,K1,G1,I1,W,X,Y,Z,A1) [E1 >= 1 + D1 + K (?,1) && 1 >= G1*H1 + H1*I1 && G1*H1 + H1 + H1*I1 >= 2 && F1 >= H1 && 1 >= G1*J1 + I1*J1 && G1*J1 + I1*J1 + J1 >= 2 && J1 >= F1 && I >= 1 + H] 18. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,B1 + -1*C1,D1,E1,F1,K1,G1,I1,W,X,Y,Z,A1) [D1 + K >= 1 + E1 (?,1) && 1 >= G1*H1 + H1*I1 && G1*H1 + H1 + H1*I1 >= 2 && F1 >= H1 && 1 >= G1*J1 + I1*J1 && G1*J1 + I1*J1 + J1 >= 2 && J1 >= F1 && I >= 1 + H] 19. f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f92(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,B1*S,Q,R,S,T,U,V,C1,D1,E1,F1,A1) [T >= 0 (?,1) && S >= C1*K1*S && C1*K1*S + K1 >= 1 + S && K1 >= E1 && S >= C1*G1*S && C1*G1*S + G1 >= 1 + S && E1 >= G1 && 1 >= C1*I1 && C1*I1 + I1 >= 2 && D1 >= I1 && 1 >= C1*H1 && C1*H1 + H1 >= 2 && H1 >= D1 && S >= C1*J1*S && C1*J1*S + J1 >= 1 + S && 1 >= C1*L1 && C1*L1 + L1 >= 2 && J1 >= L1*M1 + M1 && L1*M1 + 2*M1 >= 1 + J1 && M1 >= F1 && S >= C1*N1*S && C1*N1*S + N1 >= 1 + S && 1 >= C1*O1 && C1*O1 + O1 >= 2 && N1 >= O1*P1 + P1 && O1*P1 + 2*P1 >= 1 + N1 && F1 >= P1] 20. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f92(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,B1,C1,C1 + K,D1,T,U,V,E1,F1,K1,G1,A1) [H1 >= E1*H1*I1 (?,1) && E1*H1*I1 + I1 >= 1 + H1 && L1 >= E1*J1*L1 && E1*J1*L1 + J1 >= 1 + L1 && N1 >= E1*M1*N1 && E1*M1*N1 + M1 >= 1 + N1 && I1 + M1*O1 >= J1*O1 && J1*O1 + O1 >= 1 + I1 + M1*O1 && O1 >= K1 && H1 >= E1*H1*P1 && E1*H1*P1 + P1 >= 1 + H1 && L1 >= E1*L1*Q1 && E1*L1*Q1 + Q1 >= 1 + L1 && N1 >= E1*N1*R1 && E1*N1*R1 + R1 >= 1 + N1 && P1 + R1*S1 >= Q1*S1 && Q1*S1 + S1 >= 1 + P1 + R1*S1 && K1 >= S1 && H1 >= E1*H1*T1 && E1*H1*T1 + T1 >= 1 + H1 && L1 >= E1*L1*U1 && E1*L1*U1 + U1 >= 1 + L1 && N1 >= E1*N1*V1 && E1*N1*V1 + V1 >= 1 + N1 && T1 + V1*W1 >= U1*W1 && U1*W1 + W1 >= 1 + T1 + V1*W1 && 1 >= E1*X1 && E1*X1 + X1 >= 2 && W1 >= X1*Y1 + Y1 && X1*Y1 + 2*Y1 >= 1 + W1 && Y1 >= G1 && H1 >= E1*H1*Z1 && E1*H1*Z1 + Z1 >= 1 + H1 && L1 >= A2*E1*L1 && A2 + A2*E1*L1 >= 1 + L1 && N1 >= B2*E1*N1 && B2 + B2*E1*N1 >= 1 + N1 && B2*C2 + Z1 >= A2*C2 && A2*C2 + C2 >= 1 + B2*C2 + Z1 && 1 >= D2*E1 && D2 + D2*E1 >= 2 && C2 >= D2*E2 + E2 && D2*E2 + 2*E2 >= 1 + C2 && G1 >= E2 && F2*N1 + H1 >= F2*L1 && F2 + F2*L1 >= 1 + F2*N1 + H1 && F2 >= D1 && G2*N1 + H1 >= G2*L1 && G2 + G2*L1 >= 1 + G2*N1 + H1 && D1 >= G2 && H1*H2 + H2*I2*N1 >= H2*I2*L1 && H2*I2*L1 + I2 >= 1 + H1*H2 + H2*I2*N1 && I2 >= B1 && H1*H2 + H2*J2*N1 >= H2*J2*L1 && H2*J2*L1 + J2 >= 1 + H1*H2 + H2*J2*N1 && B1 >= J2 && 1 >= E1*K2 && E1*K2 + K2 >= 2 && F1 >= K2 && 1 >= E1*L2 && E1*L2 + L2 >= 2 && L2 >= F1 && I >= 1 + H] 21. f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f92(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,-1*B1*S,Q,R,-1*S,T,U,V,C1,D1,-1*E1*S,F1,A1) [1 >= C1*E1 (?,1) && C1*E1 + E1 >= 2 && 0 >= 1 + T && 1 >= C1*K1 && C1*K1 + K1 >= 2 && D1 >= K1 && 1 >= C1*G1 && C1*G1 + G1 >= 2 && G1 >= D1 && 1 >= C1*I1 && C1*I1 + I1 >= 2 && 1 >= C1*H1 && C1*H1 + H1 >= 2 && 0 >= H1*J1 + I1*S + J1 && H1*J1 + I1*S + 2*J1 >= 1 && F1 >= J1 && 1 >= C1*L1 && C1*L1 + L1 >= 2 && 1 >= C1*M1 && C1*M1 + M1 >= 2 && 0 >= L1*S + M1*N1 + N1 && L1*S + M1*N1 + 2*N1 >= 1 && N1 >= F1] 22. f92(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f92(A,B,C,D,E,F,G,H,I,J,B1,L,M,N,O,C1,Q,R,S,T,U,V,W,X,Y,Z,1 + A1) [B >= 1 + A1] (?,1) 23. f101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f101(A,B,C,D,E,F,G,H,I,J,B1,L,M,N,O,C1,Q,R,S,T,U,V,W,X,Y,Z,1 + A1) [C >= 1 + A1] (?,1) 24. f110(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f110(A,B,C,D,E,F,G,H,I,J,B1,L,M,N,O,C1,Q,R,S,T,U,V,W,X,Y,Z,1 + A1) [A >= A1] (?,1) 25. f119(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f119(A,B,C,D,E,F,G,H,I,J,B1,L,M,N,O,C1,Q,R,S,T,U,V,W,X,Y,Z,1 + A1) [A >= A1] (?,1) 26. f132(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f132(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A >= B] (?,1) 27. f132(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f27(A,B,C,D,1 + E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [B >= 1 + A] (?,1) 28. f119(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f53(A,B,1 + C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A1 >= 1 + A] (?,1) 29. f110(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f119(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A1 >= 1 + A] (?,1) 30. f101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f110(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A1 >= C] (?,1) 31. f92(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A1 >= B] (?,1) 32. f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f50(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [C >= 1 + A] (?,1) 33. f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f132(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [B >= A] (?,1) 34. f34(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f31(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [C >= 1 + A] (?,1) 35. f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [B >= A && 0 >= 1 + F] (?,1) 36. f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [B >= A && F >= 1] (?,1) 37. f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f1(A,B,C,D,E,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [B >= A && F = 0] (?,1) 38. f27(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> 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) [E >= 51] (?,1) 39. 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) -> f27(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [B >= 1 + A] (?,1) 40. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f5(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [C >= 1 + A] (?,1) 41. 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) -> 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) [B >= 1 + A] (?,1) Signature: {(f1,27) ;(f101,27) ;(f110,27) ;(f119,27) ;(f132,27) ;(f17,27) ;(f2,27) ;(f27,27) ;(f31,27) ;(f34,27) ;(f46,27) ;(f5,27) ;(f50,27) ;(f53,27) ;(f69,27) ;(f8,27) ;(f80,27) ;(f92,27)} Flow Graph: [0->{1,41},1->{2,40},2->{2,40},3->{3,39},4->{5,35,36,37},5->{6,34},6->{6,34},7->{9,33},8->{9,33},9->{11,12 ,13,14,15,16,32},10->{11,12,13,14,15,16,32},11->{11,12,13,14,15,16,32},12->{10,17,18,20},13->{10,17,18,20} ,14->{10,17,18,20},15->{10,17,18,20},16->{10,17,18,20},17->{19,21},18->{19,21},19->{22,31},20->{22,31} ,21->{22,31},22->{22,31},23->{23,30},24->{24,29},25->{25,28},26->{26,27},27->{4,38},28->{11,12,13,14,15,16 ,32},29->{25,28},30->{24,29},31->{23,30},32->{9,33},33->{26,27},34->{5,35,36,37},35->{7,8},36->{7,8},37->{} ,38->{},39->{4,38},40->{1,41},41->{3,39}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(4,35),(4,36),(11,12),(29,25),(41,3)] * Step 2: UnreachableRules YES + Considered Problem: Rules: 0. f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> 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) True (1,1) 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) -> f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A >= B] (?,1) 2. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f8(A,B,1 + C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A >= C] (?,1) 3. 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) -> f17(A,1 + B,C,B1,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A >= B] (?,1) 4. f27(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f31(A,B,C,D,E,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [50 >= E] (?,1) 5. f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f34(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A >= 1 + B] (?,1) 6. f34(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f34(A,B,1 + C,D,E,B1 + F,B1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A >= C] (?,1) 7. f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f50(A,B,C,D,E,F,G,B1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [3 >= E] (?,1) 8. f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f50(A,B,C,D,E,F,G,0,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [E >= 4] (?,1) 9. f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A >= 1 + B] (?,1) 10. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f53(A,B,1 + C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [H >= I] (?,1) 11. f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f53(A,B,1 + C,D,E,F,G,H,I,B1,100*B1,C1,100*B1 + C1,D1,100*B1 + D1,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A >= C && E >= 5] (?,1) 12. f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f69(A,B,C,D,E,F,G,H,C1,B1,100*B1,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A >= C && 4 >= E] (?,1) 13. f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f69(A,B,C,D,E,F,G,H,F1,B1,100*B1,C1,100*B1 + C1,D1,E1,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [E >= 5 && A >= C && E1 >= 1 + 100*B1 + D1] (?,1) 14. f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f69(A,B,C,D,E,F,G,H,F1,B1,100*B1,C1,100*B1 + C1,D1,E1,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [E >= 5 && A >= C && 100*B1 + D1 >= 1 + E1] (?,1) 15. f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f69(A,B,C,D,E,F,G,H,E1,B1,100*B1,C1,D1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [E >= 5 && A >= C && D1 >= 1 + 100*B1 + C1] (?,1) 16. f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f69(A,B,C,D,E,F,G,H,E1,B1,100*B1,C1,D1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [E >= 5 && A >= C && 100*B1 + C1 >= 1 + D1] (?,1) 17. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,B1 + -1*C1,D1,E1,F1,K1,G1,I1,W,X,Y,Z,A1) [E1 >= 1 + D1 + K (?,1) && 1 >= G1*H1 + H1*I1 && G1*H1 + H1 + H1*I1 >= 2 && F1 >= H1 && 1 >= G1*J1 + I1*J1 && G1*J1 + I1*J1 + J1 >= 2 && J1 >= F1 && I >= 1 + H] 18. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,B1 + -1*C1,D1,E1,F1,K1,G1,I1,W,X,Y,Z,A1) [D1 + K >= 1 + E1 (?,1) && 1 >= G1*H1 + H1*I1 && G1*H1 + H1 + H1*I1 >= 2 && F1 >= H1 && 1 >= G1*J1 + I1*J1 && G1*J1 + I1*J1 + J1 >= 2 && J1 >= F1 && I >= 1 + H] 19. f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f92(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,B1*S,Q,R,S,T,U,V,C1,D1,E1,F1,A1) [T >= 0 (?,1) && S >= C1*K1*S && C1*K1*S + K1 >= 1 + S && K1 >= E1 && S >= C1*G1*S && C1*G1*S + G1 >= 1 + S && E1 >= G1 && 1 >= C1*I1 && C1*I1 + I1 >= 2 && D1 >= I1 && 1 >= C1*H1 && C1*H1 + H1 >= 2 && H1 >= D1 && S >= C1*J1*S && C1*J1*S + J1 >= 1 + S && 1 >= C1*L1 && C1*L1 + L1 >= 2 && J1 >= L1*M1 + M1 && L1*M1 + 2*M1 >= 1 + J1 && M1 >= F1 && S >= C1*N1*S && C1*N1*S + N1 >= 1 + S && 1 >= C1*O1 && C1*O1 + O1 >= 2 && N1 >= O1*P1 + P1 && O1*P1 + 2*P1 >= 1 + N1 && F1 >= P1] 20. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f92(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,B1,C1,C1 + K,D1,T,U,V,E1,F1,K1,G1,A1) [H1 >= E1*H1*I1 (?,1) && E1*H1*I1 + I1 >= 1 + H1 && L1 >= E1*J1*L1 && E1*J1*L1 + J1 >= 1 + L1 && N1 >= E1*M1*N1 && E1*M1*N1 + M1 >= 1 + N1 && I1 + M1*O1 >= J1*O1 && J1*O1 + O1 >= 1 + I1 + M1*O1 && O1 >= K1 && H1 >= E1*H1*P1 && E1*H1*P1 + P1 >= 1 + H1 && L1 >= E1*L1*Q1 && E1*L1*Q1 + Q1 >= 1 + L1 && N1 >= E1*N1*R1 && E1*N1*R1 + R1 >= 1 + N1 && P1 + R1*S1 >= Q1*S1 && Q1*S1 + S1 >= 1 + P1 + R1*S1 && K1 >= S1 && H1 >= E1*H1*T1 && E1*H1*T1 + T1 >= 1 + H1 && L1 >= E1*L1*U1 && E1*L1*U1 + U1 >= 1 + L1 && N1 >= E1*N1*V1 && E1*N1*V1 + V1 >= 1 + N1 && T1 + V1*W1 >= U1*W1 && U1*W1 + W1 >= 1 + T1 + V1*W1 && 1 >= E1*X1 && E1*X1 + X1 >= 2 && W1 >= X1*Y1 + Y1 && X1*Y1 + 2*Y1 >= 1 + W1 && Y1 >= G1 && H1 >= E1*H1*Z1 && E1*H1*Z1 + Z1 >= 1 + H1 && L1 >= A2*E1*L1 && A2 + A2*E1*L1 >= 1 + L1 && N1 >= B2*E1*N1 && B2 + B2*E1*N1 >= 1 + N1 && B2*C2 + Z1 >= A2*C2 && A2*C2 + C2 >= 1 + B2*C2 + Z1 && 1 >= D2*E1 && D2 + D2*E1 >= 2 && C2 >= D2*E2 + E2 && D2*E2 + 2*E2 >= 1 + C2 && G1 >= E2 && F2*N1 + H1 >= F2*L1 && F2 + F2*L1 >= 1 + F2*N1 + H1 && F2 >= D1 && G2*N1 + H1 >= G2*L1 && G2 + G2*L1 >= 1 + G2*N1 + H1 && D1 >= G2 && H1*H2 + H2*I2*N1 >= H2*I2*L1 && H2*I2*L1 + I2 >= 1 + H1*H2 + H2*I2*N1 && I2 >= B1 && H1*H2 + H2*J2*N1 >= H2*J2*L1 && H2*J2*L1 + J2 >= 1 + H1*H2 + H2*J2*N1 && B1 >= J2 && 1 >= E1*K2 && E1*K2 + K2 >= 2 && F1 >= K2 && 1 >= E1*L2 && E1*L2 + L2 >= 2 && L2 >= F1 && I >= 1 + H] 21. f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f92(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,-1*B1*S,Q,R,-1*S,T,U,V,C1,D1,-1*E1*S,F1,A1) [1 >= C1*E1 (?,1) && C1*E1 + E1 >= 2 && 0 >= 1 + T && 1 >= C1*K1 && C1*K1 + K1 >= 2 && D1 >= K1 && 1 >= C1*G1 && C1*G1 + G1 >= 2 && G1 >= D1 && 1 >= C1*I1 && C1*I1 + I1 >= 2 && 1 >= C1*H1 && C1*H1 + H1 >= 2 && 0 >= H1*J1 + I1*S + J1 && H1*J1 + I1*S + 2*J1 >= 1 && F1 >= J1 && 1 >= C1*L1 && C1*L1 + L1 >= 2 && 1 >= C1*M1 && C1*M1 + M1 >= 2 && 0 >= L1*S + M1*N1 + N1 && L1*S + M1*N1 + 2*N1 >= 1 && N1 >= F1] 22. f92(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f92(A,B,C,D,E,F,G,H,I,J,B1,L,M,N,O,C1,Q,R,S,T,U,V,W,X,Y,Z,1 + A1) [B >= 1 + A1] (?,1) 23. f101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f101(A,B,C,D,E,F,G,H,I,J,B1,L,M,N,O,C1,Q,R,S,T,U,V,W,X,Y,Z,1 + A1) [C >= 1 + A1] (?,1) 24. f110(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f110(A,B,C,D,E,F,G,H,I,J,B1,L,M,N,O,C1,Q,R,S,T,U,V,W,X,Y,Z,1 + A1) [A >= A1] (?,1) 25. f119(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f119(A,B,C,D,E,F,G,H,I,J,B1,L,M,N,O,C1,Q,R,S,T,U,V,W,X,Y,Z,1 + A1) [A >= A1] (?,1) 26. f132(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f132(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A >= B] (?,1) 27. f132(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f27(A,B,C,D,1 + E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [B >= 1 + A] (?,1) 28. f119(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f53(A,B,1 + C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A1 >= 1 + A] (?,1) 29. f110(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f119(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A1 >= 1 + A] (?,1) 30. f101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f110(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A1 >= C] (?,1) 31. f92(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A1 >= B] (?,1) 32. f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f50(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [C >= 1 + A] (?,1) 33. f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f132(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [B >= A] (?,1) 34. f34(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f31(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [C >= 1 + A] (?,1) 35. f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [B >= A && 0 >= 1 + F] (?,1) 36. f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [B >= A && F >= 1] (?,1) 37. f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f1(A,B,C,D,E,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [B >= A && F = 0] (?,1) 38. f27(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> 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) [E >= 51] (?,1) 39. 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) -> f27(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [B >= 1 + A] (?,1) 40. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f5(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [C >= 1 + A] (?,1) 41. 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) -> 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) [B >= 1 + A] (?,1) Signature: {(f1,27) ;(f101,27) ;(f110,27) ;(f119,27) ;(f132,27) ;(f17,27) ;(f2,27) ;(f27,27) ;(f31,27) ;(f34,27) ;(f46,27) ;(f5,27) ;(f50,27) ;(f53,27) ;(f69,27) ;(f8,27) ;(f80,27) ;(f92,27)} Flow Graph: [0->{1,41},1->{2,40},2->{2,40},3->{3,39},4->{5,37},5->{6,34},6->{6,34},7->{9,33},8->{9,33},9->{11,12,13,14 ,15,16,32},10->{11,12,13,14,15,16,32},11->{11,13,14,15,16,32},12->{10,17,18,20},13->{10,17,18,20},14->{10,17 ,18,20},15->{10,17,18,20},16->{10,17,18,20},17->{19,21},18->{19,21},19->{22,31},20->{22,31},21->{22,31} ,22->{22,31},23->{23,30},24->{24,29},25->{25,28},26->{26,27},27->{4,38},28->{11,12,13,14,15,16,32},29->{28} ,30->{24,29},31->{23,30},32->{9,33},33->{26,27},34->{5,35,36,37},35->{7,8},36->{7,8},37->{},38->{},39->{4 ,38},40->{1,41},41->{39}] + Applied Processor: UnreachableRules + Details: Following transitions are not reachable from the starting states and are revomed: [3,25] * Step 3: FromIts YES + Considered Problem: Rules: 0. f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> 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) True (1,1) 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) -> f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A >= B] (?,1) 2. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f8(A,B,1 + C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A >= C] (?,1) 4. f27(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f31(A,B,C,D,E,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [50 >= E] (?,1) 5. f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f34(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A >= 1 + B] (?,1) 6. f34(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f34(A,B,1 + C,D,E,B1 + F,B1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A >= C] (?,1) 7. f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f50(A,B,C,D,E,F,G,B1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [3 >= E] (?,1) 8. f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f50(A,B,C,D,E,F,G,0,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [E >= 4] (?,1) 9. f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A >= 1 + B] (?,1) 10. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f53(A,B,1 + C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [H >= I] (?,1) 11. f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f53(A,B,1 + C,D,E,F,G,H,I,B1,100*B1,C1,100*B1 + C1,D1,100*B1 + D1,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A >= C && E >= 5] (?,1) 12. f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f69(A,B,C,D,E,F,G,H,C1,B1,100*B1,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A >= C && 4 >= E] (?,1) 13. f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f69(A,B,C,D,E,F,G,H,F1,B1,100*B1,C1,100*B1 + C1,D1,E1,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [E >= 5 && A >= C && E1 >= 1 + 100*B1 + D1] (?,1) 14. f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f69(A,B,C,D,E,F,G,H,F1,B1,100*B1,C1,100*B1 + C1,D1,E1,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [E >= 5 && A >= C && 100*B1 + D1 >= 1 + E1] (?,1) 15. f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f69(A,B,C,D,E,F,G,H,E1,B1,100*B1,C1,D1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [E >= 5 && A >= C && D1 >= 1 + 100*B1 + C1] (?,1) 16. f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f69(A,B,C,D,E,F,G,H,E1,B1,100*B1,C1,D1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [E >= 5 && A >= C && 100*B1 + C1 >= 1 + D1] (?,1) 17. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,B1 + -1*C1,D1,E1,F1,K1,G1,I1,W,X,Y,Z,A1) [E1 >= 1 + D1 + K (?,1) && 1 >= G1*H1 + H1*I1 && G1*H1 + H1 + H1*I1 >= 2 && F1 >= H1 && 1 >= G1*J1 + I1*J1 && G1*J1 + I1*J1 + J1 >= 2 && J1 >= F1 && I >= 1 + H] 18. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,B1 + -1*C1,D1,E1,F1,K1,G1,I1,W,X,Y,Z,A1) [D1 + K >= 1 + E1 (?,1) && 1 >= G1*H1 + H1*I1 && G1*H1 + H1 + H1*I1 >= 2 && F1 >= H1 && 1 >= G1*J1 + I1*J1 && G1*J1 + I1*J1 + J1 >= 2 && J1 >= F1 && I >= 1 + H] 19. f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f92(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,B1*S,Q,R,S,T,U,V,C1,D1,E1,F1,A1) [T >= 0 (?,1) && S >= C1*K1*S && C1*K1*S + K1 >= 1 + S && K1 >= E1 && S >= C1*G1*S && C1*G1*S + G1 >= 1 + S && E1 >= G1 && 1 >= C1*I1 && C1*I1 + I1 >= 2 && D1 >= I1 && 1 >= C1*H1 && C1*H1 + H1 >= 2 && H1 >= D1 && S >= C1*J1*S && C1*J1*S + J1 >= 1 + S && 1 >= C1*L1 && C1*L1 + L1 >= 2 && J1 >= L1*M1 + M1 && L1*M1 + 2*M1 >= 1 + J1 && M1 >= F1 && S >= C1*N1*S && C1*N1*S + N1 >= 1 + S && 1 >= C1*O1 && C1*O1 + O1 >= 2 && N1 >= O1*P1 + P1 && O1*P1 + 2*P1 >= 1 + N1 && F1 >= P1] 20. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f92(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,B1,C1,C1 + K,D1,T,U,V,E1,F1,K1,G1,A1) [H1 >= E1*H1*I1 (?,1) && E1*H1*I1 + I1 >= 1 + H1 && L1 >= E1*J1*L1 && E1*J1*L1 + J1 >= 1 + L1 && N1 >= E1*M1*N1 && E1*M1*N1 + M1 >= 1 + N1 && I1 + M1*O1 >= J1*O1 && J1*O1 + O1 >= 1 + I1 + M1*O1 && O1 >= K1 && H1 >= E1*H1*P1 && E1*H1*P1 + P1 >= 1 + H1 && L1 >= E1*L1*Q1 && E1*L1*Q1 + Q1 >= 1 + L1 && N1 >= E1*N1*R1 && E1*N1*R1 + R1 >= 1 + N1 && P1 + R1*S1 >= Q1*S1 && Q1*S1 + S1 >= 1 + P1 + R1*S1 && K1 >= S1 && H1 >= E1*H1*T1 && E1*H1*T1 + T1 >= 1 + H1 && L1 >= E1*L1*U1 && E1*L1*U1 + U1 >= 1 + L1 && N1 >= E1*N1*V1 && E1*N1*V1 + V1 >= 1 + N1 && T1 + V1*W1 >= U1*W1 && U1*W1 + W1 >= 1 + T1 + V1*W1 && 1 >= E1*X1 && E1*X1 + X1 >= 2 && W1 >= X1*Y1 + Y1 && X1*Y1 + 2*Y1 >= 1 + W1 && Y1 >= G1 && H1 >= E1*H1*Z1 && E1*H1*Z1 + Z1 >= 1 + H1 && L1 >= A2*E1*L1 && A2 + A2*E1*L1 >= 1 + L1 && N1 >= B2*E1*N1 && B2 + B2*E1*N1 >= 1 + N1 && B2*C2 + Z1 >= A2*C2 && A2*C2 + C2 >= 1 + B2*C2 + Z1 && 1 >= D2*E1 && D2 + D2*E1 >= 2 && C2 >= D2*E2 + E2 && D2*E2 + 2*E2 >= 1 + C2 && G1 >= E2 && F2*N1 + H1 >= F2*L1 && F2 + F2*L1 >= 1 + F2*N1 + H1 && F2 >= D1 && G2*N1 + H1 >= G2*L1 && G2 + G2*L1 >= 1 + G2*N1 + H1 && D1 >= G2 && H1*H2 + H2*I2*N1 >= H2*I2*L1 && H2*I2*L1 + I2 >= 1 + H1*H2 + H2*I2*N1 && I2 >= B1 && H1*H2 + H2*J2*N1 >= H2*J2*L1 && H2*J2*L1 + J2 >= 1 + H1*H2 + H2*J2*N1 && B1 >= J2 && 1 >= E1*K2 && E1*K2 + K2 >= 2 && F1 >= K2 && 1 >= E1*L2 && E1*L2 + L2 >= 2 && L2 >= F1 && I >= 1 + H] 21. f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f92(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,-1*B1*S,Q,R,-1*S,T,U,V,C1,D1,-1*E1*S,F1,A1) [1 >= C1*E1 (?,1) && C1*E1 + E1 >= 2 && 0 >= 1 + T && 1 >= C1*K1 && C1*K1 + K1 >= 2 && D1 >= K1 && 1 >= C1*G1 && C1*G1 + G1 >= 2 && G1 >= D1 && 1 >= C1*I1 && C1*I1 + I1 >= 2 && 1 >= C1*H1 && C1*H1 + H1 >= 2 && 0 >= H1*J1 + I1*S + J1 && H1*J1 + I1*S + 2*J1 >= 1 && F1 >= J1 && 1 >= C1*L1 && C1*L1 + L1 >= 2 && 1 >= C1*M1 && C1*M1 + M1 >= 2 && 0 >= L1*S + M1*N1 + N1 && L1*S + M1*N1 + 2*N1 >= 1 && N1 >= F1] 22. f92(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f92(A,B,C,D,E,F,G,H,I,J,B1,L,M,N,O,C1,Q,R,S,T,U,V,W,X,Y,Z,1 + A1) [B >= 1 + A1] (?,1) 23. f101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f101(A,B,C,D,E,F,G,H,I,J,B1,L,M,N,O,C1,Q,R,S,T,U,V,W,X,Y,Z,1 + A1) [C >= 1 + A1] (?,1) 24. f110(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f110(A,B,C,D,E,F,G,H,I,J,B1,L,M,N,O,C1,Q,R,S,T,U,V,W,X,Y,Z,1 + A1) [A >= A1] (?,1) 26. f132(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f132(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A >= B] (?,1) 27. f132(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f27(A,B,C,D,1 + E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [B >= 1 + A] (?,1) 28. f119(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f53(A,B,1 + C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A1 >= 1 + A] (?,1) 29. f110(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f119(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A1 >= 1 + A] (?,1) 30. f101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f110(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A1 >= C] (?,1) 31. f92(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A1 >= B] (?,1) 32. f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f50(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [C >= 1 + A] (?,1) 33. f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f132(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [B >= A] (?,1) 34. f34(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f31(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [C >= 1 + A] (?,1) 35. f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [B >= A && 0 >= 1 + F] (?,1) 36. f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [B >= A && F >= 1] (?,1) 37. f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f1(A,B,C,D,E,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [B >= A && F = 0] (?,1) 38. f27(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> 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) [E >= 51] (?,1) 39. 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) -> f27(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [B >= 1 + A] (?,1) 40. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f5(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [C >= 1 + A] (?,1) 41. 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) -> 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) [B >= 1 + A] (?,1) Signature: {(f1,27) ;(f101,27) ;(f110,27) ;(f119,27) ;(f132,27) ;(f17,27) ;(f2,27) ;(f27,27) ;(f31,27) ;(f34,27) ;(f46,27) ;(f5,27) ;(f50,27) ;(f53,27) ;(f69,27) ;(f8,27) ;(f80,27) ;(f92,27)} Flow Graph: [0->{1,41},1->{2,40},2->{2,40},4->{5,37},5->{6,34},6->{6,34},7->{9,33},8->{9,33},9->{11,12,13,14,15,16,32} ,10->{11,12,13,14,15,16,32},11->{11,13,14,15,16,32},12->{10,17,18,20},13->{10,17,18,20},14->{10,17,18,20} ,15->{10,17,18,20},16->{10,17,18,20},17->{19,21},18->{19,21},19->{22,31},20->{22,31},21->{22,31},22->{22,31} ,23->{23,30},24->{24,29},26->{26,27},27->{4,38},28->{11,12,13,14,15,16,32},29->{28},30->{24,29},31->{23,30} ,32->{9,33},33->{26,27},34->{5,35,36,37},35->{7,8},36->{7,8},37->{},38->{},39->{4,38},40->{1,41},41->{39}] + Applied Processor: FromIts + Details: () * Step 4: Decompose YES + Considered Problem: Rules: f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> 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) True 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) -> f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [A >= B] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f8(A,B,1 + C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R ,S,T,U,V,W,X,Y,Z ,A1) [A >= C] f27(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f31(A,B,C,D,E,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [50 >= E] f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f34(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [A >= 1 + B] f34(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f34(A,B,1 + C,D,E,B1 + F,B1,H,I,J,K,L,M,N,O ,P,Q,R,S,T,U,V,W,X,Y,Z ,A1) [A >= C] f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f50(A,B,C,D,E,F,G,B1,I,J,K,L,M,N,O,P,Q,R,S ,T,U,V,W,X,Y,Z ,A1) [3 >= E] f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f50(A,B,C,D,E,F,G,0,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [E >= 4] f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [A >= 1 + B] f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f53(A,B,1 + C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R ,S,T,U,V,W,X,Y,Z ,A1) [H >= I] f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f53(A,B,1 + C,D,E,F,G,H,I,B1,100*B1,C1 ,100*B1 + C1,D1,100*B1 + D1,P,Q,R,S,T,U,V,W,X,Y,Z ,A1) [A >= C && E >= 5] f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f69(A,B,C,D,E,F,G,H,C1,B1,100*B1,L,M,N,O,P ,Q,R,S,T,U,V,W,X,Y,Z ,A1) [A >= C && 4 >= E] f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f69(A,B,C,D,E,F,G,H,F1,B1,100*B1,C1 ,100*B1 + C1,D1,E1,P,Q,R,S,T,U,V,W,X,Y,Z ,A1) [E >= 5 && A >= C && E1 >= 1 + 100*B1 + D1] f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f69(A,B,C,D,E,F,G,H,F1,B1,100*B1,C1 ,100*B1 + C1,D1,E1,P,Q,R,S,T,U,V,W,X,Y,Z ,A1) [E >= 5 && A >= C && 100*B1 + D1 >= 1 + E1] f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f69(A,B,C,D,E,F,G,H,E1,B1,100*B1,C1,D1,N,O ,P,Q,R,S,T,U,V,W,X,Y,Z ,A1) [E >= 5 && A >= C && D1 >= 1 + 100*B1 + C1] f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f69(A,B,C,D,E,F,G,H,E1,B1,100*B1,C1,D1,N,O ,P,Q,R,S,T,U,V,W,X,Y,Z ,A1) [E >= 5 && A >= C && 100*B1 + C1 >= 1 + D1] f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O ,B1 + -1*C1,D1,E1,F1,K1,G1,I1,W,X,Y,Z ,A1) [E1 >= 1 + D1 + K && 1 >= G1*H1 + H1*I1 && G1*H1 + H1 + H1*I1 >= 2 && F1 >= H1 && 1 >= G1*J1 + I1*J1 && G1*J1 + I1*J1 + J1 >= 2 && J1 >= F1 && I >= 1 + H] f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O ,B1 + -1*C1,D1,E1,F1,K1,G1,I1,W,X,Y,Z ,A1) [D1 + K >= 1 + E1 && 1 >= G1*H1 + H1*I1 && G1*H1 + H1 + H1*I1 >= 2 && F1 >= H1 && 1 >= G1*J1 + I1*J1 && G1*J1 + I1*J1 + J1 >= 2 && J1 >= F1 && I >= 1 + H] f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f92(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,B1*S,Q,R ,S,T,U,V,C1,D1,E1,F1 ,A1) [T >= 0 && S >= C1*K1*S && C1*K1*S + K1 >= 1 + S && K1 >= E1 && S >= C1*G1*S && C1*G1*S + G1 >= 1 + S && E1 >= G1 && 1 >= C1*I1 && C1*I1 + I1 >= 2 && D1 >= I1 && 1 >= C1*H1 && C1*H1 + H1 >= 2 && H1 >= D1 && S >= C1*J1*S && C1*J1*S + J1 >= 1 + S && 1 >= C1*L1 && C1*L1 + L1 >= 2 && J1 >= L1*M1 + M1 && L1*M1 + 2*M1 >= 1 + J1 && M1 >= F1 && S >= C1*N1*S && C1*N1*S + N1 >= 1 + S && 1 >= C1*O1 && C1*O1 + O1 >= 2 && N1 >= O1*P1 + P1 && O1*P1 + 2*P1 >= 1 + N1 && F1 >= P1] f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f92(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,B1,C1 ,C1 + K,D1,T,U,V,E1,F1,K1,G1 ,A1) [H1 >= E1*H1*I1 && E1*H1*I1 + I1 >= 1 + H1 && L1 >= E1*J1*L1 && E1*J1*L1 + J1 >= 1 + L1 && N1 >= E1*M1*N1 && E1*M1*N1 + M1 >= 1 + N1 && I1 + M1*O1 >= J1*O1 && J1*O1 + O1 >= 1 + I1 + M1*O1 && O1 >= K1 && H1 >= E1*H1*P1 && E1*H1*P1 + P1 >= 1 + H1 && L1 >= E1*L1*Q1 && E1*L1*Q1 + Q1 >= 1 + L1 && N1 >= E1*N1*R1 && E1*N1*R1 + R1 >= 1 + N1 && P1 + R1*S1 >= Q1*S1 && Q1*S1 + S1 >= 1 + P1 + R1*S1 && K1 >= S1 && H1 >= E1*H1*T1 && E1*H1*T1 + T1 >= 1 + H1 && L1 >= E1*L1*U1 && E1*L1*U1 + U1 >= 1 + L1 && N1 >= E1*N1*V1 && E1*N1*V1 + V1 >= 1 + N1 && T1 + V1*W1 >= U1*W1 && U1*W1 + W1 >= 1 + T1 + V1*W1 && 1 >= E1*X1 && E1*X1 + X1 >= 2 && W1 >= X1*Y1 + Y1 && X1*Y1 + 2*Y1 >= 1 + W1 && Y1 >= G1 && H1 >= E1*H1*Z1 && E1*H1*Z1 + Z1 >= 1 + H1 && L1 >= A2*E1*L1 && A2 + A2*E1*L1 >= 1 + L1 && N1 >= B2*E1*N1 && B2 + B2*E1*N1 >= 1 + N1 && B2*C2 + Z1 >= A2*C2 && A2*C2 + C2 >= 1 + B2*C2 + Z1 && 1 >= D2*E1 && D2 + D2*E1 >= 2 && C2 >= D2*E2 + E2 && D2*E2 + 2*E2 >= 1 + C2 && G1 >= E2 && F2*N1 + H1 >= F2*L1 && F2 + F2*L1 >= 1 + F2*N1 + H1 && F2 >= D1 && G2*N1 + H1 >= G2*L1 && G2 + G2*L1 >= 1 + G2*N1 + H1 && D1 >= G2 && H1*H2 + H2*I2*N1 >= H2*I2*L1 && H2*I2*L1 + I2 >= 1 + H1*H2 + H2*I2*N1 && I2 >= B1 && H1*H2 + H2*J2*N1 >= H2*J2*L1 && H2*J2*L1 + J2 >= 1 + H1*H2 + H2*J2*N1 && B1 >= J2 && 1 >= E1*K2 && E1*K2 + K2 >= 2 && F1 >= K2 && 1 >= E1*L2 && E1*L2 + L2 >= 2 && L2 >= F1 && I >= 1 + H] f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f92(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,-1*B1*S,Q ,R,-1*S,T,U,V,C1,D1,-1*E1*S,F1 ,A1) [1 >= C1*E1 && C1*E1 + E1 >= 2 && 0 >= 1 + T && 1 >= C1*K1 && C1*K1 + K1 >= 2 && D1 >= K1 && 1 >= C1*G1 && C1*G1 + G1 >= 2 && G1 >= D1 && 1 >= C1*I1 && C1*I1 + I1 >= 2 && 1 >= C1*H1 && C1*H1 + H1 >= 2 && 0 >= H1*J1 + I1*S + J1 && H1*J1 + I1*S + 2*J1 >= 1 && F1 >= J1 && 1 >= C1*L1 && C1*L1 + L1 >= 2 && 1 >= C1*M1 && C1*M1 + M1 >= 2 && 0 >= L1*S + M1*N1 + N1 && L1*S + M1*N1 + 2*N1 >= 1 && N1 >= F1] f92(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f92(A,B,C,D,E,F,G,H,I,J,B1,L,M,N,O,C1,Q,R,S ,T,U,V,W,X,Y,Z ,1 + A1) [B >= 1 + A1] f101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f101(A,B,C,D,E,F,G,H,I,J,B1,L,M,N,O,C1,Q,R ,S,T,U,V,W,X,Y,Z ,1 + A1) [C >= 1 + A1] f110(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f110(A,B,C,D,E,F,G,H,I,J,B1,L,M,N,O,C1,Q,R ,S,T,U,V,W,X,Y,Z ,1 + A1) [A >= A1] f132(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f132(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q ,R,S,T,U,V,W,X,Y,Z ,A1) [A >= B] f132(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f27(A,B,C,D,1 + E,F,G,H,I,J,K,L,M,N,O,P,Q,R ,S,T,U,V,W,X,Y,Z ,A1) [B >= 1 + A] f119(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f53(A,B,1 + C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R ,S,T,U,V,W,X,Y,Z ,A1) [A1 >= 1 + A] f110(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f119(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S ,T,U,V,W,X,Y,Z ,A1) [A1 >= 1 + A] f101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f110(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S ,T,U,V,W,X,Y,Z ,A1) [A1 >= C] f92(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S ,T,U,V,W,X,Y,Z ,A1) [A1 >= B] f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f50(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R ,S,T,U,V,W,X,Y,Z ,A1) [C >= 1 + A] f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f132(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S ,T,U,V,W,X,Y,Z ,A1) [B >= A] f34(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f31(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R ,S,T,U,V,W,X,Y,Z ,A1) [C >= 1 + A] f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [B >= A && 0 >= 1 + F] f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [B >= A && F >= 1] f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f1(A,B,C,D,E,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [B >= A && F = 0] f27(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> 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) [E >= 51] 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) -> f27(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [B >= 1 + A] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f5(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R ,S,T,U,V,W,X,Y,Z ,A1) [C >= 1 + A] 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) -> 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) [B >= 1 + A] Signature: {(f1,27) ;(f101,27) ;(f110,27) ;(f119,27) ;(f132,27) ;(f17,27) ;(f2,27) ;(f27,27) ;(f31,27) ;(f34,27) ;(f46,27) ;(f5,27) ;(f50,27) ;(f53,27) ;(f69,27) ;(f8,27) ;(f80,27) ;(f92,27)} Rule Graph: [0->{1,41},1->{2,40},2->{2,40},4->{5,37},5->{6,34},6->{6,34},7->{9,33},8->{9,33},9->{11,12,13,14,15,16,32} ,10->{11,12,13,14,15,16,32},11->{11,13,14,15,16,32},12->{10,17,18,20},13->{10,17,18,20},14->{10,17,18,20} ,15->{10,17,18,20},16->{10,17,18,20},17->{19,21},18->{19,21},19->{22,31},20->{22,31},21->{22,31},22->{22,31} ,23->{23,30},24->{24,29},26->{26,27},27->{4,38},28->{11,12,13,14,15,16,32},29->{28},30->{24,29},31->{23,30} ,32->{9,33},33->{26,27},34->{5,35,36,37},35->{7,8},36->{7,8},37->{},38->{},39->{4,38},40->{1,41},41->{39}] + Applied Processor: Decompose NoGreedy + Details: We construct a looptree: P: [0,1,2,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41] | +- p:[1,40,2] c: [2] | | | `- p:[1,40] c: [1,40] | `- p:[4,27,26,33,7,35,34,5,6,36,8,32,9,10,12,28,29,24,30,23,31,19,17,13,11,14,15,16,18,20,21,22] c: [24] | `- p:[4,27,26,33,7,35,34,5,6,36,8,32,9,10,12,28,29,30,23,31,19,17,13,11,14,15,16,18,20,21,22] c: [9] | +- p:[10,12,28,29,30,23,31,19,17,13,11,14,15,16,18,20,21,22] c: [22] | | | `- p:[10,12,28,29,30,23,31,19,17,13,11,14,15,16,18,20,21] c: [10,11,12,13,14,15,16,17,18,19,20,21,28,29,30,31] | | | `- p:[23] c: [23] | `- p:[4,27,26,33,7,35,34,5,6,36,8] c: [6] | `- p:[4,27,26,33,7,35,34,5,36,8] c: [7] | `- p:[4,27,26,33,8,35,34,5,36] c: [26] | `- p:[4,27,33,8,35,34,5,36] c: [4,5,8,27,33,34,35,36] * Step 5: CloseWith YES + Considered Problem: (Rules: f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> 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) True 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) -> f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [A >= B] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f8(A,B,1 + C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R ,S,T,U,V,W,X,Y,Z ,A1) [A >= C] f27(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f31(A,B,C,D,E,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [50 >= E] f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f34(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [A >= 1 + B] f34(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f34(A,B,1 + C,D,E,B1 + F,B1,H,I,J,K,L,M,N,O ,P,Q,R,S,T,U,V,W,X,Y,Z ,A1) [A >= C] f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f50(A,B,C,D,E,F,G,B1,I,J,K,L,M,N,O,P,Q,R,S ,T,U,V,W,X,Y,Z ,A1) [3 >= E] f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f50(A,B,C,D,E,F,G,0,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [E >= 4] f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [A >= 1 + B] f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f53(A,B,1 + C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R ,S,T,U,V,W,X,Y,Z ,A1) [H >= I] f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f53(A,B,1 + C,D,E,F,G,H,I,B1,100*B1,C1 ,100*B1 + C1,D1,100*B1 + D1,P,Q,R,S,T,U,V,W,X,Y,Z ,A1) [A >= C && E >= 5] f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f69(A,B,C,D,E,F,G,H,C1,B1,100*B1,L,M,N,O,P ,Q,R,S,T,U,V,W,X,Y,Z ,A1) [A >= C && 4 >= E] f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f69(A,B,C,D,E,F,G,H,F1,B1,100*B1,C1 ,100*B1 + C1,D1,E1,P,Q,R,S,T,U,V,W,X,Y,Z ,A1) [E >= 5 && A >= C && E1 >= 1 + 100*B1 + D1] f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f69(A,B,C,D,E,F,G,H,F1,B1,100*B1,C1 ,100*B1 + C1,D1,E1,P,Q,R,S,T,U,V,W,X,Y,Z ,A1) [E >= 5 && A >= C && 100*B1 + D1 >= 1 + E1] f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f69(A,B,C,D,E,F,G,H,E1,B1,100*B1,C1,D1,N,O ,P,Q,R,S,T,U,V,W,X,Y,Z ,A1) [E >= 5 && A >= C && D1 >= 1 + 100*B1 + C1] f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f69(A,B,C,D,E,F,G,H,E1,B1,100*B1,C1,D1,N,O ,P,Q,R,S,T,U,V,W,X,Y,Z ,A1) [E >= 5 && A >= C && 100*B1 + C1 >= 1 + D1] f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O ,B1 + -1*C1,D1,E1,F1,K1,G1,I1,W,X,Y,Z ,A1) [E1 >= 1 + D1 + K && 1 >= G1*H1 + H1*I1 && G1*H1 + H1 + H1*I1 >= 2 && F1 >= H1 && 1 >= G1*J1 + I1*J1 && G1*J1 + I1*J1 + J1 >= 2 && J1 >= F1 && I >= 1 + H] f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O ,B1 + -1*C1,D1,E1,F1,K1,G1,I1,W,X,Y,Z ,A1) [D1 + K >= 1 + E1 && 1 >= G1*H1 + H1*I1 && G1*H1 + H1 + H1*I1 >= 2 && F1 >= H1 && 1 >= G1*J1 + I1*J1 && G1*J1 + I1*J1 + J1 >= 2 && J1 >= F1 && I >= 1 + H] f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f92(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,B1*S,Q,R ,S,T,U,V,C1,D1,E1,F1 ,A1) [T >= 0 && S >= C1*K1*S && C1*K1*S + K1 >= 1 + S && K1 >= E1 && S >= C1*G1*S && C1*G1*S + G1 >= 1 + S && E1 >= G1 && 1 >= C1*I1 && C1*I1 + I1 >= 2 && D1 >= I1 && 1 >= C1*H1 && C1*H1 + H1 >= 2 && H1 >= D1 && S >= C1*J1*S && C1*J1*S + J1 >= 1 + S && 1 >= C1*L1 && C1*L1 + L1 >= 2 && J1 >= L1*M1 + M1 && L1*M1 + 2*M1 >= 1 + J1 && M1 >= F1 && S >= C1*N1*S && C1*N1*S + N1 >= 1 + S && 1 >= C1*O1 && C1*O1 + O1 >= 2 && N1 >= O1*P1 + P1 && O1*P1 + 2*P1 >= 1 + N1 && F1 >= P1] f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f92(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,B1,C1 ,C1 + K,D1,T,U,V,E1,F1,K1,G1 ,A1) [H1 >= E1*H1*I1 && E1*H1*I1 + I1 >= 1 + H1 && L1 >= E1*J1*L1 && E1*J1*L1 + J1 >= 1 + L1 && N1 >= E1*M1*N1 && E1*M1*N1 + M1 >= 1 + N1 && I1 + M1*O1 >= J1*O1 && J1*O1 + O1 >= 1 + I1 + M1*O1 && O1 >= K1 && H1 >= E1*H1*P1 && E1*H1*P1 + P1 >= 1 + H1 && L1 >= E1*L1*Q1 && E1*L1*Q1 + Q1 >= 1 + L1 && N1 >= E1*N1*R1 && E1*N1*R1 + R1 >= 1 + N1 && P1 + R1*S1 >= Q1*S1 && Q1*S1 + S1 >= 1 + P1 + R1*S1 && K1 >= S1 && H1 >= E1*H1*T1 && E1*H1*T1 + T1 >= 1 + H1 && L1 >= E1*L1*U1 && E1*L1*U1 + U1 >= 1 + L1 && N1 >= E1*N1*V1 && E1*N1*V1 + V1 >= 1 + N1 && T1 + V1*W1 >= U1*W1 && U1*W1 + W1 >= 1 + T1 + V1*W1 && 1 >= E1*X1 && E1*X1 + X1 >= 2 && W1 >= X1*Y1 + Y1 && X1*Y1 + 2*Y1 >= 1 + W1 && Y1 >= G1 && H1 >= E1*H1*Z1 && E1*H1*Z1 + Z1 >= 1 + H1 && L1 >= A2*E1*L1 && A2 + A2*E1*L1 >= 1 + L1 && N1 >= B2*E1*N1 && B2 + B2*E1*N1 >= 1 + N1 && B2*C2 + Z1 >= A2*C2 && A2*C2 + C2 >= 1 + B2*C2 + Z1 && 1 >= D2*E1 && D2 + D2*E1 >= 2 && C2 >= D2*E2 + E2 && D2*E2 + 2*E2 >= 1 + C2 && G1 >= E2 && F2*N1 + H1 >= F2*L1 && F2 + F2*L1 >= 1 + F2*N1 + H1 && F2 >= D1 && G2*N1 + H1 >= G2*L1 && G2 + G2*L1 >= 1 + G2*N1 + H1 && D1 >= G2 && H1*H2 + H2*I2*N1 >= H2*I2*L1 && H2*I2*L1 + I2 >= 1 + H1*H2 + H2*I2*N1 && I2 >= B1 && H1*H2 + H2*J2*N1 >= H2*J2*L1 && H2*J2*L1 + J2 >= 1 + H1*H2 + H2*J2*N1 && B1 >= J2 && 1 >= E1*K2 && E1*K2 + K2 >= 2 && F1 >= K2 && 1 >= E1*L2 && E1*L2 + L2 >= 2 && L2 >= F1 && I >= 1 + H] f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f92(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,-1*B1*S,Q ,R,-1*S,T,U,V,C1,D1,-1*E1*S,F1 ,A1) [1 >= C1*E1 && C1*E1 + E1 >= 2 && 0 >= 1 + T && 1 >= C1*K1 && C1*K1 + K1 >= 2 && D1 >= K1 && 1 >= C1*G1 && C1*G1 + G1 >= 2 && G1 >= D1 && 1 >= C1*I1 && C1*I1 + I1 >= 2 && 1 >= C1*H1 && C1*H1 + H1 >= 2 && 0 >= H1*J1 + I1*S + J1 && H1*J1 + I1*S + 2*J1 >= 1 && F1 >= J1 && 1 >= C1*L1 && C1*L1 + L1 >= 2 && 1 >= C1*M1 && C1*M1 + M1 >= 2 && 0 >= L1*S + M1*N1 + N1 && L1*S + M1*N1 + 2*N1 >= 1 && N1 >= F1] f92(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f92(A,B,C,D,E,F,G,H,I,J,B1,L,M,N,O,C1,Q,R,S ,T,U,V,W,X,Y,Z ,1 + A1) [B >= 1 + A1] f101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f101(A,B,C,D,E,F,G,H,I,J,B1,L,M,N,O,C1,Q,R ,S,T,U,V,W,X,Y,Z ,1 + A1) [C >= 1 + A1] f110(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f110(A,B,C,D,E,F,G,H,I,J,B1,L,M,N,O,C1,Q,R ,S,T,U,V,W,X,Y,Z ,1 + A1) [A >= A1] f132(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f132(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q ,R,S,T,U,V,W,X,Y,Z ,A1) [A >= B] f132(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f27(A,B,C,D,1 + E,F,G,H,I,J,K,L,M,N,O,P,Q,R ,S,T,U,V,W,X,Y,Z ,A1) [B >= 1 + A] f119(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f53(A,B,1 + C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R ,S,T,U,V,W,X,Y,Z ,A1) [A1 >= 1 + A] f110(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f119(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S ,T,U,V,W,X,Y,Z ,A1) [A1 >= 1 + A] f101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f110(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S ,T,U,V,W,X,Y,Z ,A1) [A1 >= C] f92(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S ,T,U,V,W,X,Y,Z ,A1) [A1 >= B] f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f50(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R ,S,T,U,V,W,X,Y,Z ,A1) [C >= 1 + A] f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f132(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S ,T,U,V,W,X,Y,Z ,A1) [B >= A] f34(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f31(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R ,S,T,U,V,W,X,Y,Z ,A1) [C >= 1 + A] f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [B >= A && 0 >= 1 + F] f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [B >= A && F >= 1] f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f1(A,B,C,D,E,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [B >= A && F = 0] f27(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> 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) [E >= 51] 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) -> f27(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [B >= 1 + A] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f5(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R ,S,T,U,V,W,X,Y,Z ,A1) [C >= 1 + A] 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) -> 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) [B >= 1 + A] Signature: {(f1,27) ;(f101,27) ;(f110,27) ;(f119,27) ;(f132,27) ;(f17,27) ;(f2,27) ;(f27,27) ;(f31,27) ;(f34,27) ;(f46,27) ;(f5,27) ;(f50,27) ;(f53,27) ;(f69,27) ;(f8,27) ;(f80,27) ;(f92,27)} Rule Graph: [0->{1,41},1->{2,40},2->{2,40},4->{5,37},5->{6,34},6->{6,34},7->{9,33},8->{9,33},9->{11,12,13,14,15,16,32} ,10->{11,12,13,14,15,16,32},11->{11,13,14,15,16,32},12->{10,17,18,20},13->{10,17,18,20},14->{10,17,18,20} ,15->{10,17,18,20},16->{10,17,18,20},17->{19,21},18->{19,21},19->{22,31},20->{22,31},21->{22,31},22->{22,31} ,23->{23,30},24->{24,29},26->{26,27},27->{4,38},28->{11,12,13,14,15,16,32},29->{28},30->{24,29},31->{23,30} ,32->{9,33},33->{26,27},34->{5,35,36,37},35->{7,8},36->{7,8},37->{},38->{},39->{4,38},40->{1,41},41->{39}] ,We construct a looptree: P: [0,1,2,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41] | +- p:[1,40,2] c: [2] | | | `- p:[1,40] c: [1,40] | `- p:[4,27,26,33,7,35,34,5,6,36,8,32,9,10,12,28,29,24,30,23,31,19,17,13,11,14,15,16,18,20,21,22] c: [24] | `- p:[4,27,26,33,7,35,34,5,6,36,8,32,9,10,12,28,29,30,23,31,19,17,13,11,14,15,16,18,20,21,22] c: [9] | +- p:[10,12,28,29,30,23,31,19,17,13,11,14,15,16,18,20,21,22] c: [22] | | | `- p:[10,12,28,29,30,23,31,19,17,13,11,14,15,16,18,20,21] c: [10,11,12,13,14,15,16,17,18,19,20,21,28,29,30,31] | | | `- p:[23] c: [23] | `- p:[4,27,26,33,7,35,34,5,6,36,8] c: [6] | `- p:[4,27,26,33,7,35,34,5,36,8] c: [7] | `- p:[4,27,26,33,8,35,34,5,36] c: [26] | `- p:[4,27,33,8,35,34,5,36] c: [4,5,8,27,33,34,35,36]) + Applied Processor: CloseWith True + Details: () YES