YES * Step 1: UnsatPaths YES + Considered Problem: Rules: 0. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f9(A,1 + B,1 + C,B1,B1,B1,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [-1 + B + -1*C >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -17 + A + C >= 0 && 17 + -1*A + C >= 0 && -1 + B >= 0 && -18 + A + B >= 0 && 16 + -1*A + B >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && A >= 1 + B] 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) -> f0(A,B,C,D,E,F,G,B1,I,H,E1,F1,C1,D1,G1,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [-1*I + T >= 0 (?,1) && -1 + I >= 0 && -14 + G + I >= 0 && -17 + C + I >= 0 && -15 + I + Y >= 0 && -14 + I + U >= 0 && -2 + I + T >= 0 && I + -1*T >= 0 && -18 + B + I >= 0 && -1 + I + J >= 0 && -1 + I + -1*J >= 0 && -18 + A + I >= 0 && 16 + -1*A + I >= 0 && -3 + C + -1*G >= 0 && -1 + -1*G + Y >= 0 && -1*G + U >= 0 && -4 + B + -1*G >= 0 && G + -1*U >= 0 && -14 + G + T >= 0 && -1*D + X >= 0 && -1*D + W >= 0 && D + -1*X >= 0 && D + -1*W >= 0 && 2 + -1*C + Y >= 0 && -1 + B + -1*C >= 0 && -16 + C >= 0 && -30 + C + Y >= 0 && -2 + C + -1*Y >= 0 && -3 + C + -1*U >= 0 && -17 + C + T >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -16 + C + J >= 0 && -16 + C + -1*J >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && -1*A1 + Z >= 0 && -3 + B + -1*Y >= 0 && -14 + Y >= 0 && -1 + -1*U + Y >= 0 && -15 + T + Y >= 0 && -31 + B + Y >= 0 && 3 + -1*B + Y >= 0 && -14 + J + Y >= 0 && -14 + -1*J + Y >= 0 && -31 + A + Y >= 0 && 3 + -1*A + Y >= 0 && W + -1*X >= 0 && -1*W + X >= 0 && -4 + B + -1*U >= 0 && -14 + T + U >= 0 && -1 + T >= 0 && -18 + B + T >= 0 && -1 + J + T >= 0 && -1 + -1*J + T >= 0 && -18 + A + T >= 0 && 16 + -1*A + T >= 0 && -17 + B >= 0 && -17 + B + J >= 0 && -17 + B + -1*J >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -1*J >= 0 && -17 + A + -1*J >= 0 && 17 + -1*A + -1*J >= 0 && J >= 0 && -17 + A + J >= 0 && 17 + -1*A + J >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && D1 >= 1 + C1 && G >= 0 && H >= 1 && I >= 1] 2. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f0(A,B,C,D,E,F,G,B1,I,H,E1,F1,C1,D1,G1,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [-1*I + T >= 0 (?,1) && -1 + I >= 0 && -14 + G + I >= 0 && -17 + C + I >= 0 && -15 + I + Y >= 0 && -14 + I + U >= 0 && -2 + I + T >= 0 && I + -1*T >= 0 && -18 + B + I >= 0 && -1 + I + J >= 0 && -1 + I + -1*J >= 0 && -18 + A + I >= 0 && 16 + -1*A + I >= 0 && -3 + C + -1*G >= 0 && -1 + -1*G + Y >= 0 && -1*G + U >= 0 && -4 + B + -1*G >= 0 && G + -1*U >= 0 && -14 + G + T >= 0 && -1*D + X >= 0 && -1*D + W >= 0 && D + -1*X >= 0 && D + -1*W >= 0 && 2 + -1*C + Y >= 0 && -1 + B + -1*C >= 0 && -16 + C >= 0 && -30 + C + Y >= 0 && -2 + C + -1*Y >= 0 && -3 + C + -1*U >= 0 && -17 + C + T >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -16 + C + J >= 0 && -16 + C + -1*J >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && -1*A1 + Z >= 0 && -3 + B + -1*Y >= 0 && -14 + Y >= 0 && -1 + -1*U + Y >= 0 && -15 + T + Y >= 0 && -31 + B + Y >= 0 && 3 + -1*B + Y >= 0 && -14 + J + Y >= 0 && -14 + -1*J + Y >= 0 && -31 + A + Y >= 0 && 3 + -1*A + Y >= 0 && W + -1*X >= 0 && -1*W + X >= 0 && -4 + B + -1*U >= 0 && -14 + T + U >= 0 && -1 + T >= 0 && -18 + B + T >= 0 && -1 + J + T >= 0 && -1 + -1*J + T >= 0 && -18 + A + T >= 0 && 16 + -1*A + T >= 0 && -17 + B >= 0 && -17 + B + J >= 0 && -17 + B + -1*J >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -1*J >= 0 && -17 + A + -1*J >= 0 && 17 + -1*A + -1*J >= 0 && J >= 0 && -17 + A + J >= 0 && 17 + -1*A + J >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && D1 >= 1 + C1 && G >= 0 && 0 >= 1 + H && I >= 1] 3. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f5(A,B,C,D,E,F,-1 + G,R,1 + I,0,F1,C1,M,D1,O,E1,R,P,B1,1 + I,-1 + G,I,W,X,Y,Z,A1) [-1*I + T >= 0 (?,1) && -1 + I >= 0 && -14 + G + I >= 0 && -17 + C + I >= 0 && -15 + I + Y >= 0 && -14 + I + U >= 0 && -2 + I + T >= 0 && I + -1*T >= 0 && -18 + B + I >= 0 && -1 + I + J >= 0 && -1 + I + -1*J >= 0 && -18 + A + I >= 0 && 16 + -1*A + I >= 0 && -3 + C + -1*G >= 0 && -1 + -1*G + Y >= 0 && -1*G + U >= 0 && -4 + B + -1*G >= 0 && G + -1*U >= 0 && -14 + G + T >= 0 && -1*D + X >= 0 && -1*D + W >= 0 && D + -1*X >= 0 && D + -1*W >= 0 && 2 + -1*C + Y >= 0 && -1 + B + -1*C >= 0 && -16 + C >= 0 && -30 + C + Y >= 0 && -2 + C + -1*Y >= 0 && -3 + C + -1*U >= 0 && -17 + C + T >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -16 + C + J >= 0 && -16 + C + -1*J >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && -1*A1 + Z >= 0 && -3 + B + -1*Y >= 0 && -14 + Y >= 0 && -1 + -1*U + Y >= 0 && -15 + T + Y >= 0 && -31 + B + Y >= 0 && 3 + -1*B + Y >= 0 && -14 + J + Y >= 0 && -14 + -1*J + Y >= 0 && -31 + A + Y >= 0 && 3 + -1*A + Y >= 0 && W + -1*X >= 0 && -1*W + X >= 0 && -4 + B + -1*U >= 0 && -14 + T + U >= 0 && -1 + T >= 0 && -18 + B + T >= 0 && -1 + J + T >= 0 && -1 + -1*J + T >= 0 && -18 + A + T >= 0 && 16 + -1*A + T >= 0 && -17 + B >= 0 && -17 + B + J >= 0 && -17 + B + -1*J >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -1*J >= 0 && -17 + A + -1*J >= 0 && 17 + -1*A + -1*J >= 0 && J >= 0 && -17 + A + J >= 0 && 17 + -1*A + J >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && M >= D1 && G >= 0 && I >= 0 && P >= 1 && H >= 1 && J = 0] 4. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f5(A,B,C,D,E,F,-1 + G,R,1 + I,0,F1,C1,M,D1,O,E1,R,P,B1,1 + I,-1 + G,I,W,X,Y,Z,A1) [-1*I + T >= 0 (?,1) && -1 + I >= 0 && -14 + G + I >= 0 && -17 + C + I >= 0 && -15 + I + Y >= 0 && -14 + I + U >= 0 && -2 + I + T >= 0 && I + -1*T >= 0 && -18 + B + I >= 0 && -1 + I + J >= 0 && -1 + I + -1*J >= 0 && -18 + A + I >= 0 && 16 + -1*A + I >= 0 && -3 + C + -1*G >= 0 && -1 + -1*G + Y >= 0 && -1*G + U >= 0 && -4 + B + -1*G >= 0 && G + -1*U >= 0 && -14 + G + T >= 0 && -1*D + X >= 0 && -1*D + W >= 0 && D + -1*X >= 0 && D + -1*W >= 0 && 2 + -1*C + Y >= 0 && -1 + B + -1*C >= 0 && -16 + C >= 0 && -30 + C + Y >= 0 && -2 + C + -1*Y >= 0 && -3 + C + -1*U >= 0 && -17 + C + T >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -16 + C + J >= 0 && -16 + C + -1*J >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && -1*A1 + Z >= 0 && -3 + B + -1*Y >= 0 && -14 + Y >= 0 && -1 + -1*U + Y >= 0 && -15 + T + Y >= 0 && -31 + B + Y >= 0 && 3 + -1*B + Y >= 0 && -14 + J + Y >= 0 && -14 + -1*J + Y >= 0 && -31 + A + Y >= 0 && 3 + -1*A + Y >= 0 && W + -1*X >= 0 && -1*W + X >= 0 && -4 + B + -1*U >= 0 && -14 + T + U >= 0 && -1 + T >= 0 && -18 + B + T >= 0 && -1 + J + T >= 0 && -1 + -1*J + T >= 0 && -18 + A + T >= 0 && 16 + -1*A + T >= 0 && -17 + B >= 0 && -17 + B + J >= 0 && -17 + B + -1*J >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -1*J >= 0 && -17 + A + -1*J >= 0 && 17 + -1*A + -1*J >= 0 && J >= 0 && -17 + A + J >= 0 && 17 + -1*A + J >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && M >= D1 && G >= 0 && I >= 0 && P >= 1 && 0 >= 1 + H && J = 0] 5. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f5(A,B,C,D,E,F,-1 + G,R,1 + I,0,F1,C1,M,D1,O,E1,R,P,B1,1 + I,-1 + G,I,W,X,Y,Z,A1) [-1*I + T >= 0 (?,1) && -1 + I >= 0 && -14 + G + I >= 0 && -17 + C + I >= 0 && -15 + I + Y >= 0 && -14 + I + U >= 0 && -2 + I + T >= 0 && I + -1*T >= 0 && -18 + B + I >= 0 && -1 + I + J >= 0 && -1 + I + -1*J >= 0 && -18 + A + I >= 0 && 16 + -1*A + I >= 0 && -3 + C + -1*G >= 0 && -1 + -1*G + Y >= 0 && -1*G + U >= 0 && -4 + B + -1*G >= 0 && G + -1*U >= 0 && -14 + G + T >= 0 && -1*D + X >= 0 && -1*D + W >= 0 && D + -1*X >= 0 && D + -1*W >= 0 && 2 + -1*C + Y >= 0 && -1 + B + -1*C >= 0 && -16 + C >= 0 && -30 + C + Y >= 0 && -2 + C + -1*Y >= 0 && -3 + C + -1*U >= 0 && -17 + C + T >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -16 + C + J >= 0 && -16 + C + -1*J >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && -1*A1 + Z >= 0 && -3 + B + -1*Y >= 0 && -14 + Y >= 0 && -1 + -1*U + Y >= 0 && -15 + T + Y >= 0 && -31 + B + Y >= 0 && 3 + -1*B + Y >= 0 && -14 + J + Y >= 0 && -14 + -1*J + Y >= 0 && -31 + A + Y >= 0 && 3 + -1*A + Y >= 0 && W + -1*X >= 0 && -1*W + X >= 0 && -4 + B + -1*U >= 0 && -14 + T + U >= 0 && -1 + T >= 0 && -18 + B + T >= 0 && -1 + J + T >= 0 && -1 + -1*J + T >= 0 && -18 + A + T >= 0 && 16 + -1*A + T >= 0 && -17 + B >= 0 && -17 + B + J >= 0 && -17 + B + -1*J >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -1*J >= 0 && -17 + A + -1*J >= 0 && 17 + -1*A + -1*J >= 0 && J >= 0 && -17 + A + J >= 0 && 17 + -1*A + J >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && M >= D1 && G >= 0 && I >= 0 && 0 >= 1 + P && H >= 1 && J = 0] 6. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f5(A,B,C,D,E,F,-1 + G,R,1 + I,0,F1,C1,M,D1,O,E1,R,P,B1,1 + I,-1 + G,I,W,X,Y,Z,A1) [-1*I + T >= 0 (?,1) && -1 + I >= 0 && -14 + G + I >= 0 && -17 + C + I >= 0 && -15 + I + Y >= 0 && -14 + I + U >= 0 && -2 + I + T >= 0 && I + -1*T >= 0 && -18 + B + I >= 0 && -1 + I + J >= 0 && -1 + I + -1*J >= 0 && -18 + A + I >= 0 && 16 + -1*A + I >= 0 && -3 + C + -1*G >= 0 && -1 + -1*G + Y >= 0 && -1*G + U >= 0 && -4 + B + -1*G >= 0 && G + -1*U >= 0 && -14 + G + T >= 0 && -1*D + X >= 0 && -1*D + W >= 0 && D + -1*X >= 0 && D + -1*W >= 0 && 2 + -1*C + Y >= 0 && -1 + B + -1*C >= 0 && -16 + C >= 0 && -30 + C + Y >= 0 && -2 + C + -1*Y >= 0 && -3 + C + -1*U >= 0 && -17 + C + T >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -16 + C + J >= 0 && -16 + C + -1*J >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && -1*A1 + Z >= 0 && -3 + B + -1*Y >= 0 && -14 + Y >= 0 && -1 + -1*U + Y >= 0 && -15 + T + Y >= 0 && -31 + B + Y >= 0 && 3 + -1*B + Y >= 0 && -14 + J + Y >= 0 && -14 + -1*J + Y >= 0 && -31 + A + Y >= 0 && 3 + -1*A + Y >= 0 && W + -1*X >= 0 && -1*W + X >= 0 && -4 + B + -1*U >= 0 && -14 + T + U >= 0 && -1 + T >= 0 && -18 + B + T >= 0 && -1 + J + T >= 0 && -1 + -1*J + T >= 0 && -18 + A + T >= 0 && 16 + -1*A + T >= 0 && -17 + B >= 0 && -17 + B + J >= 0 && -17 + B + -1*J >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -1*J >= 0 && -17 + A + -1*J >= 0 && 17 + -1*A + -1*J >= 0 && J >= 0 && -17 + A + J >= 0 && 17 + -1*A + J >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && M >= D1 && G >= 0 && I >= 0 && 0 >= 1 + P && 0 >= 1 + H && J = 0] 7. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f12(A,B,C,D,E,F,G,H,I,0,E1,F1,M,C1,O,0,R,R,S,T,U,I,B1,X,Y,Z,A1) [-1*I + T >= 0 (?,1) && -1 + I >= 0 && -14 + G + I >= 0 && -17 + C + I >= 0 && -15 + I + Y >= 0 && -14 + I + U >= 0 && -2 + I + T >= 0 && I + -1*T >= 0 && -18 + B + I >= 0 && -1 + I + J >= 0 && -1 + I + -1*J >= 0 && -18 + A + I >= 0 && 16 + -1*A + I >= 0 && -3 + C + -1*G >= 0 && -1 + -1*G + Y >= 0 && -1*G + U >= 0 && -4 + B + -1*G >= 0 && G + -1*U >= 0 && -14 + G + T >= 0 && -1*D + X >= 0 && -1*D + W >= 0 && D + -1*X >= 0 && D + -1*W >= 0 && 2 + -1*C + Y >= 0 && -1 + B + -1*C >= 0 && -16 + C >= 0 && -30 + C + Y >= 0 && -2 + C + -1*Y >= 0 && -3 + C + -1*U >= 0 && -17 + C + T >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -16 + C + J >= 0 && -16 + C + -1*J >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && -1*A1 + Z >= 0 && -3 + B + -1*Y >= 0 && -14 + Y >= 0 && -1 + -1*U + Y >= 0 && -15 + T + Y >= 0 && -31 + B + Y >= 0 && 3 + -1*B + Y >= 0 && -14 + J + Y >= 0 && -14 + -1*J + Y >= 0 && -31 + A + Y >= 0 && 3 + -1*A + Y >= 0 && W + -1*X >= 0 && -1*W + X >= 0 && -4 + B + -1*U >= 0 && -14 + T + U >= 0 && -1 + T >= 0 && -18 + B + T >= 0 && -1 + J + T >= 0 && -1 + -1*J + T >= 0 && -18 + A + T >= 0 && 16 + -1*A + T >= 0 && -17 + B >= 0 && -17 + B + J >= 0 && -17 + B + -1*J >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -1*J >= 0 && -17 + A + -1*J >= 0 && 17 + -1*A + -1*J >= 0 && J >= 0 && -17 + A + J >= 0 && 17 + -1*A + J >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && M >= C1 && G >= 0 && H >= 1 && I >= 0 && P = 0 && J = 0] 8. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f12(A,B,C,D,E,F,G,H,I,0,E1,F1,M,C1,O,0,R,R,S,T,U,I,B1,X,Y,Z,A1) [-1*I + T >= 0 (?,1) && -1 + I >= 0 && -14 + G + I >= 0 && -17 + C + I >= 0 && -15 + I + Y >= 0 && -14 + I + U >= 0 && -2 + I + T >= 0 && I + -1*T >= 0 && -18 + B + I >= 0 && -1 + I + J >= 0 && -1 + I + -1*J >= 0 && -18 + A + I >= 0 && 16 + -1*A + I >= 0 && -3 + C + -1*G >= 0 && -1 + -1*G + Y >= 0 && -1*G + U >= 0 && -4 + B + -1*G >= 0 && G + -1*U >= 0 && -14 + G + T >= 0 && -1*D + X >= 0 && -1*D + W >= 0 && D + -1*X >= 0 && D + -1*W >= 0 && 2 + -1*C + Y >= 0 && -1 + B + -1*C >= 0 && -16 + C >= 0 && -30 + C + Y >= 0 && -2 + C + -1*Y >= 0 && -3 + C + -1*U >= 0 && -17 + C + T >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -16 + C + J >= 0 && -16 + C + -1*J >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && -1*A1 + Z >= 0 && -3 + B + -1*Y >= 0 && -14 + Y >= 0 && -1 + -1*U + Y >= 0 && -15 + T + Y >= 0 && -31 + B + Y >= 0 && 3 + -1*B + Y >= 0 && -14 + J + Y >= 0 && -14 + -1*J + Y >= 0 && -31 + A + Y >= 0 && 3 + -1*A + Y >= 0 && W + -1*X >= 0 && -1*W + X >= 0 && -4 + B + -1*U >= 0 && -14 + T + U >= 0 && -1 + T >= 0 && -18 + B + T >= 0 && -1 + J + T >= 0 && -1 + -1*J + T >= 0 && -18 + A + T >= 0 && 16 + -1*A + T >= 0 && -17 + B >= 0 && -17 + B + J >= 0 && -17 + B + -1*J >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -1*J >= 0 && -17 + A + -1*J >= 0 && 17 + -1*A + -1*J >= 0 && J >= 0 && -17 + A + J >= 0 && 17 + -1*A + J >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && M >= C1 && G >= 0 && 0 >= 1 + H && I >= 0 && P = 0 && J = 0] 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [-1 + B + -1*C >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -17 + A + C >= 0 && 17 + -1*A + C >= 0 && -1 + B >= 0 && -18 + A + B >= 0 && 16 + -1*A + B >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && D1 >= G1 && C >= 2 && E1 >= 1 && B1 >= 1 && B >= A && D >= 1] 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [-1 + B + -1*C >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -17 + A + C >= 0 && 17 + -1*A + C >= 0 && -1 + B >= 0 && -18 + A + B >= 0 && 16 + -1*A + B >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && D1 >= G1 && C >= 2 && E1 >= 1 && B1 >= 1 && B >= A && 0 >= 1 + D] 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [-1 + B + -1*C >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -17 + A + C >= 0 && 17 + -1*A + C >= 0 && -1 + B >= 0 && -18 + A + B >= 0 && 16 + -1*A + B >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && D1 >= G1 && C >= 2 && E1 >= 1 && 0 >= 1 + B1 && B >= A && D >= 1] 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [-1 + B + -1*C >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -17 + A + C >= 0 && 17 + -1*A + C >= 0 && -1 + B >= 0 && -18 + A + B >= 0 && 16 + -1*A + B >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && D1 >= G1 && C >= 2 && E1 >= 1 && 0 >= 1 + B1 && B >= A && 0 >= 1 + D] 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [-1 + B + -1*C >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -17 + A + C >= 0 && 17 + -1*A + C >= 0 && -1 + B >= 0 && -18 + A + B >= 0 && 16 + -1*A + B >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && D1 >= G1 && C >= 2 && 0 >= 1 + E1 && B1 >= 1 && B >= A && D >= 1] 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [-1 + B + -1*C >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -17 + A + C >= 0 && 17 + -1*A + C >= 0 && -1 + B >= 0 && -18 + A + B >= 0 && 16 + -1*A + B >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && D1 >= G1 && C >= 2 && 0 >= 1 + E1 && B1 >= 1 && B >= A && 0 >= 1 + D] 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [-1 + B + -1*C >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -17 + A + C >= 0 && 17 + -1*A + C >= 0 && -1 + B >= 0 && -18 + A + B >= 0 && 16 + -1*A + B >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && D1 >= G1 && C >= 2 && 0 >= 1 + E1 && 0 >= 1 + B1 && B >= A && D >= 1] 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [-1 + B + -1*C >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -17 + A + C >= 0 && 17 + -1*A + C >= 0 && -1 + B >= 0 && -18 + A + B >= 0 && 16 + -1*A + B >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && D1 >= G1 && C >= 2 && 0 >= 1 + E1 && 0 >= 1 + B1 && B >= A && 0 >= 1 + D] 17. f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f9(17,1,0,B1,B1,B1,G,H,I,J,K,L,M,N,O,P,E1,R,S,T,U,V,W,X,Y,Z,A1) True (1,1) Signature: {(f0,27);(f12,27);(f5,27);(f6,27);(f9,27)} Flow Graph: [0->{0,9,10,11,12,13,14,15,16},1->{},2->{},3->{1,2,3,4,5,6,7,8},4->{1,2,3,4,5,6,7,8},5->{1,2,3,4,5,6,7,8} ,6->{1,2,3,4,5,6,7,8},7->{},8->{},9->{1,2,3,4,5,6,7,8},10->{1,2,3,4,5,6,7,8},11->{1,2,3,4,5,6,7,8},12->{1,2 ,3,4,5,6,7,8},13->{1,2,3,4,5,6,7,8},14->{1,2,3,4,5,6,7,8},15->{1,2,3,4,5,6,7,8},16->{1,2,3,4,5,6,7,8},17->{0 ,9,10,11,12,13,14,15,16}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(9,2) ,(9,4) ,(9,6) ,(9,8) ,(10,2) ,(10,4) ,(10,6) ,(10,8) ,(11,1) ,(11,3) ,(11,5) ,(11,7) ,(12,1) ,(12,3) ,(12,5) ,(12,7) ,(13,2) ,(13,4) ,(13,6) ,(13,8) ,(14,2) ,(14,4) ,(14,6) ,(14,8) ,(15,1) ,(15,3) ,(15,5) ,(15,7) ,(16,1) ,(16,3) ,(16,5) ,(16,7) ,(17,9) ,(17,10) ,(17,11) ,(17,12) ,(17,13) ,(17,14) ,(17,15) ,(17,16)] * Step 2: FromIts YES + Considered Problem: Rules: 0. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f9(A,1 + B,1 + C,B1,B1,B1,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [-1 + B + -1*C >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -17 + A + C >= 0 && 17 + -1*A + C >= 0 && -1 + B >= 0 && -18 + A + B >= 0 && 16 + -1*A + B >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && A >= 1 + B] 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) -> f0(A,B,C,D,E,F,G,B1,I,H,E1,F1,C1,D1,G1,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [-1*I + T >= 0 (?,1) && -1 + I >= 0 && -14 + G + I >= 0 && -17 + C + I >= 0 && -15 + I + Y >= 0 && -14 + I + U >= 0 && -2 + I + T >= 0 && I + -1*T >= 0 && -18 + B + I >= 0 && -1 + I + J >= 0 && -1 + I + -1*J >= 0 && -18 + A + I >= 0 && 16 + -1*A + I >= 0 && -3 + C + -1*G >= 0 && -1 + -1*G + Y >= 0 && -1*G + U >= 0 && -4 + B + -1*G >= 0 && G + -1*U >= 0 && -14 + G + T >= 0 && -1*D + X >= 0 && -1*D + W >= 0 && D + -1*X >= 0 && D + -1*W >= 0 && 2 + -1*C + Y >= 0 && -1 + B + -1*C >= 0 && -16 + C >= 0 && -30 + C + Y >= 0 && -2 + C + -1*Y >= 0 && -3 + C + -1*U >= 0 && -17 + C + T >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -16 + C + J >= 0 && -16 + C + -1*J >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && -1*A1 + Z >= 0 && -3 + B + -1*Y >= 0 && -14 + Y >= 0 && -1 + -1*U + Y >= 0 && -15 + T + Y >= 0 && -31 + B + Y >= 0 && 3 + -1*B + Y >= 0 && -14 + J + Y >= 0 && -14 + -1*J + Y >= 0 && -31 + A + Y >= 0 && 3 + -1*A + Y >= 0 && W + -1*X >= 0 && -1*W + X >= 0 && -4 + B + -1*U >= 0 && -14 + T + U >= 0 && -1 + T >= 0 && -18 + B + T >= 0 && -1 + J + T >= 0 && -1 + -1*J + T >= 0 && -18 + A + T >= 0 && 16 + -1*A + T >= 0 && -17 + B >= 0 && -17 + B + J >= 0 && -17 + B + -1*J >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -1*J >= 0 && -17 + A + -1*J >= 0 && 17 + -1*A + -1*J >= 0 && J >= 0 && -17 + A + J >= 0 && 17 + -1*A + J >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && D1 >= 1 + C1 && G >= 0 && H >= 1 && I >= 1] 2. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f0(A,B,C,D,E,F,G,B1,I,H,E1,F1,C1,D1,G1,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [-1*I + T >= 0 (?,1) && -1 + I >= 0 && -14 + G + I >= 0 && -17 + C + I >= 0 && -15 + I + Y >= 0 && -14 + I + U >= 0 && -2 + I + T >= 0 && I + -1*T >= 0 && -18 + B + I >= 0 && -1 + I + J >= 0 && -1 + I + -1*J >= 0 && -18 + A + I >= 0 && 16 + -1*A + I >= 0 && -3 + C + -1*G >= 0 && -1 + -1*G + Y >= 0 && -1*G + U >= 0 && -4 + B + -1*G >= 0 && G + -1*U >= 0 && -14 + G + T >= 0 && -1*D + X >= 0 && -1*D + W >= 0 && D + -1*X >= 0 && D + -1*W >= 0 && 2 + -1*C + Y >= 0 && -1 + B + -1*C >= 0 && -16 + C >= 0 && -30 + C + Y >= 0 && -2 + C + -1*Y >= 0 && -3 + C + -1*U >= 0 && -17 + C + T >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -16 + C + J >= 0 && -16 + C + -1*J >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && -1*A1 + Z >= 0 && -3 + B + -1*Y >= 0 && -14 + Y >= 0 && -1 + -1*U + Y >= 0 && -15 + T + Y >= 0 && -31 + B + Y >= 0 && 3 + -1*B + Y >= 0 && -14 + J + Y >= 0 && -14 + -1*J + Y >= 0 && -31 + A + Y >= 0 && 3 + -1*A + Y >= 0 && W + -1*X >= 0 && -1*W + X >= 0 && -4 + B + -1*U >= 0 && -14 + T + U >= 0 && -1 + T >= 0 && -18 + B + T >= 0 && -1 + J + T >= 0 && -1 + -1*J + T >= 0 && -18 + A + T >= 0 && 16 + -1*A + T >= 0 && -17 + B >= 0 && -17 + B + J >= 0 && -17 + B + -1*J >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -1*J >= 0 && -17 + A + -1*J >= 0 && 17 + -1*A + -1*J >= 0 && J >= 0 && -17 + A + J >= 0 && 17 + -1*A + J >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && D1 >= 1 + C1 && G >= 0 && 0 >= 1 + H && I >= 1] 3. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f5(A,B,C,D,E,F,-1 + G,R,1 + I,0,F1,C1,M,D1,O,E1,R,P,B1,1 + I,-1 + G,I,W,X,Y,Z,A1) [-1*I + T >= 0 (?,1) && -1 + I >= 0 && -14 + G + I >= 0 && -17 + C + I >= 0 && -15 + I + Y >= 0 && -14 + I + U >= 0 && -2 + I + T >= 0 && I + -1*T >= 0 && -18 + B + I >= 0 && -1 + I + J >= 0 && -1 + I + -1*J >= 0 && -18 + A + I >= 0 && 16 + -1*A + I >= 0 && -3 + C + -1*G >= 0 && -1 + -1*G + Y >= 0 && -1*G + U >= 0 && -4 + B + -1*G >= 0 && G + -1*U >= 0 && -14 + G + T >= 0 && -1*D + X >= 0 && -1*D + W >= 0 && D + -1*X >= 0 && D + -1*W >= 0 && 2 + -1*C + Y >= 0 && -1 + B + -1*C >= 0 && -16 + C >= 0 && -30 + C + Y >= 0 && -2 + C + -1*Y >= 0 && -3 + C + -1*U >= 0 && -17 + C + T >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -16 + C + J >= 0 && -16 + C + -1*J >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && -1*A1 + Z >= 0 && -3 + B + -1*Y >= 0 && -14 + Y >= 0 && -1 + -1*U + Y >= 0 && -15 + T + Y >= 0 && -31 + B + Y >= 0 && 3 + -1*B + Y >= 0 && -14 + J + Y >= 0 && -14 + -1*J + Y >= 0 && -31 + A + Y >= 0 && 3 + -1*A + Y >= 0 && W + -1*X >= 0 && -1*W + X >= 0 && -4 + B + -1*U >= 0 && -14 + T + U >= 0 && -1 + T >= 0 && -18 + B + T >= 0 && -1 + J + T >= 0 && -1 + -1*J + T >= 0 && -18 + A + T >= 0 && 16 + -1*A + T >= 0 && -17 + B >= 0 && -17 + B + J >= 0 && -17 + B + -1*J >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -1*J >= 0 && -17 + A + -1*J >= 0 && 17 + -1*A + -1*J >= 0 && J >= 0 && -17 + A + J >= 0 && 17 + -1*A + J >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && M >= D1 && G >= 0 && I >= 0 && P >= 1 && H >= 1 && J = 0] 4. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f5(A,B,C,D,E,F,-1 + G,R,1 + I,0,F1,C1,M,D1,O,E1,R,P,B1,1 + I,-1 + G,I,W,X,Y,Z,A1) [-1*I + T >= 0 (?,1) && -1 + I >= 0 && -14 + G + I >= 0 && -17 + C + I >= 0 && -15 + I + Y >= 0 && -14 + I + U >= 0 && -2 + I + T >= 0 && I + -1*T >= 0 && -18 + B + I >= 0 && -1 + I + J >= 0 && -1 + I + -1*J >= 0 && -18 + A + I >= 0 && 16 + -1*A + I >= 0 && -3 + C + -1*G >= 0 && -1 + -1*G + Y >= 0 && -1*G + U >= 0 && -4 + B + -1*G >= 0 && G + -1*U >= 0 && -14 + G + T >= 0 && -1*D + X >= 0 && -1*D + W >= 0 && D + -1*X >= 0 && D + -1*W >= 0 && 2 + -1*C + Y >= 0 && -1 + B + -1*C >= 0 && -16 + C >= 0 && -30 + C + Y >= 0 && -2 + C + -1*Y >= 0 && -3 + C + -1*U >= 0 && -17 + C + T >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -16 + C + J >= 0 && -16 + C + -1*J >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && -1*A1 + Z >= 0 && -3 + B + -1*Y >= 0 && -14 + Y >= 0 && -1 + -1*U + Y >= 0 && -15 + T + Y >= 0 && -31 + B + Y >= 0 && 3 + -1*B + Y >= 0 && -14 + J + Y >= 0 && -14 + -1*J + Y >= 0 && -31 + A + Y >= 0 && 3 + -1*A + Y >= 0 && W + -1*X >= 0 && -1*W + X >= 0 && -4 + B + -1*U >= 0 && -14 + T + U >= 0 && -1 + T >= 0 && -18 + B + T >= 0 && -1 + J + T >= 0 && -1 + -1*J + T >= 0 && -18 + A + T >= 0 && 16 + -1*A + T >= 0 && -17 + B >= 0 && -17 + B + J >= 0 && -17 + B + -1*J >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -1*J >= 0 && -17 + A + -1*J >= 0 && 17 + -1*A + -1*J >= 0 && J >= 0 && -17 + A + J >= 0 && 17 + -1*A + J >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && M >= D1 && G >= 0 && I >= 0 && P >= 1 && 0 >= 1 + H && J = 0] 5. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f5(A,B,C,D,E,F,-1 + G,R,1 + I,0,F1,C1,M,D1,O,E1,R,P,B1,1 + I,-1 + G,I,W,X,Y,Z,A1) [-1*I + T >= 0 (?,1) && -1 + I >= 0 && -14 + G + I >= 0 && -17 + C + I >= 0 && -15 + I + Y >= 0 && -14 + I + U >= 0 && -2 + I + T >= 0 && I + -1*T >= 0 && -18 + B + I >= 0 && -1 + I + J >= 0 && -1 + I + -1*J >= 0 && -18 + A + I >= 0 && 16 + -1*A + I >= 0 && -3 + C + -1*G >= 0 && -1 + -1*G + Y >= 0 && -1*G + U >= 0 && -4 + B + -1*G >= 0 && G + -1*U >= 0 && -14 + G + T >= 0 && -1*D + X >= 0 && -1*D + W >= 0 && D + -1*X >= 0 && D + -1*W >= 0 && 2 + -1*C + Y >= 0 && -1 + B + -1*C >= 0 && -16 + C >= 0 && -30 + C + Y >= 0 && -2 + C + -1*Y >= 0 && -3 + C + -1*U >= 0 && -17 + C + T >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -16 + C + J >= 0 && -16 + C + -1*J >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && -1*A1 + Z >= 0 && -3 + B + -1*Y >= 0 && -14 + Y >= 0 && -1 + -1*U + Y >= 0 && -15 + T + Y >= 0 && -31 + B + Y >= 0 && 3 + -1*B + Y >= 0 && -14 + J + Y >= 0 && -14 + -1*J + Y >= 0 && -31 + A + Y >= 0 && 3 + -1*A + Y >= 0 && W + -1*X >= 0 && -1*W + X >= 0 && -4 + B + -1*U >= 0 && -14 + T + U >= 0 && -1 + T >= 0 && -18 + B + T >= 0 && -1 + J + T >= 0 && -1 + -1*J + T >= 0 && -18 + A + T >= 0 && 16 + -1*A + T >= 0 && -17 + B >= 0 && -17 + B + J >= 0 && -17 + B + -1*J >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -1*J >= 0 && -17 + A + -1*J >= 0 && 17 + -1*A + -1*J >= 0 && J >= 0 && -17 + A + J >= 0 && 17 + -1*A + J >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && M >= D1 && G >= 0 && I >= 0 && 0 >= 1 + P && H >= 1 && J = 0] 6. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f5(A,B,C,D,E,F,-1 + G,R,1 + I,0,F1,C1,M,D1,O,E1,R,P,B1,1 + I,-1 + G,I,W,X,Y,Z,A1) [-1*I + T >= 0 (?,1) && -1 + I >= 0 && -14 + G + I >= 0 && -17 + C + I >= 0 && -15 + I + Y >= 0 && -14 + I + U >= 0 && -2 + I + T >= 0 && I + -1*T >= 0 && -18 + B + I >= 0 && -1 + I + J >= 0 && -1 + I + -1*J >= 0 && -18 + A + I >= 0 && 16 + -1*A + I >= 0 && -3 + C + -1*G >= 0 && -1 + -1*G + Y >= 0 && -1*G + U >= 0 && -4 + B + -1*G >= 0 && G + -1*U >= 0 && -14 + G + T >= 0 && -1*D + X >= 0 && -1*D + W >= 0 && D + -1*X >= 0 && D + -1*W >= 0 && 2 + -1*C + Y >= 0 && -1 + B + -1*C >= 0 && -16 + C >= 0 && -30 + C + Y >= 0 && -2 + C + -1*Y >= 0 && -3 + C + -1*U >= 0 && -17 + C + T >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -16 + C + J >= 0 && -16 + C + -1*J >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && -1*A1 + Z >= 0 && -3 + B + -1*Y >= 0 && -14 + Y >= 0 && -1 + -1*U + Y >= 0 && -15 + T + Y >= 0 && -31 + B + Y >= 0 && 3 + -1*B + Y >= 0 && -14 + J + Y >= 0 && -14 + -1*J + Y >= 0 && -31 + A + Y >= 0 && 3 + -1*A + Y >= 0 && W + -1*X >= 0 && -1*W + X >= 0 && -4 + B + -1*U >= 0 && -14 + T + U >= 0 && -1 + T >= 0 && -18 + B + T >= 0 && -1 + J + T >= 0 && -1 + -1*J + T >= 0 && -18 + A + T >= 0 && 16 + -1*A + T >= 0 && -17 + B >= 0 && -17 + B + J >= 0 && -17 + B + -1*J >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -1*J >= 0 && -17 + A + -1*J >= 0 && 17 + -1*A + -1*J >= 0 && J >= 0 && -17 + A + J >= 0 && 17 + -1*A + J >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && M >= D1 && G >= 0 && I >= 0 && 0 >= 1 + P && 0 >= 1 + H && J = 0] 7. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f12(A,B,C,D,E,F,G,H,I,0,E1,F1,M,C1,O,0,R,R,S,T,U,I,B1,X,Y,Z,A1) [-1*I + T >= 0 (?,1) && -1 + I >= 0 && -14 + G + I >= 0 && -17 + C + I >= 0 && -15 + I + Y >= 0 && -14 + I + U >= 0 && -2 + I + T >= 0 && I + -1*T >= 0 && -18 + B + I >= 0 && -1 + I + J >= 0 && -1 + I + -1*J >= 0 && -18 + A + I >= 0 && 16 + -1*A + I >= 0 && -3 + C + -1*G >= 0 && -1 + -1*G + Y >= 0 && -1*G + U >= 0 && -4 + B + -1*G >= 0 && G + -1*U >= 0 && -14 + G + T >= 0 && -1*D + X >= 0 && -1*D + W >= 0 && D + -1*X >= 0 && D + -1*W >= 0 && 2 + -1*C + Y >= 0 && -1 + B + -1*C >= 0 && -16 + C >= 0 && -30 + C + Y >= 0 && -2 + C + -1*Y >= 0 && -3 + C + -1*U >= 0 && -17 + C + T >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -16 + C + J >= 0 && -16 + C + -1*J >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && -1*A1 + Z >= 0 && -3 + B + -1*Y >= 0 && -14 + Y >= 0 && -1 + -1*U + Y >= 0 && -15 + T + Y >= 0 && -31 + B + Y >= 0 && 3 + -1*B + Y >= 0 && -14 + J + Y >= 0 && -14 + -1*J + Y >= 0 && -31 + A + Y >= 0 && 3 + -1*A + Y >= 0 && W + -1*X >= 0 && -1*W + X >= 0 && -4 + B + -1*U >= 0 && -14 + T + U >= 0 && -1 + T >= 0 && -18 + B + T >= 0 && -1 + J + T >= 0 && -1 + -1*J + T >= 0 && -18 + A + T >= 0 && 16 + -1*A + T >= 0 && -17 + B >= 0 && -17 + B + J >= 0 && -17 + B + -1*J >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -1*J >= 0 && -17 + A + -1*J >= 0 && 17 + -1*A + -1*J >= 0 && J >= 0 && -17 + A + J >= 0 && 17 + -1*A + J >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && M >= C1 && G >= 0 && H >= 1 && I >= 0 && P = 0 && J = 0] 8. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f12(A,B,C,D,E,F,G,H,I,0,E1,F1,M,C1,O,0,R,R,S,T,U,I,B1,X,Y,Z,A1) [-1*I + T >= 0 (?,1) && -1 + I >= 0 && -14 + G + I >= 0 && -17 + C + I >= 0 && -15 + I + Y >= 0 && -14 + I + U >= 0 && -2 + I + T >= 0 && I + -1*T >= 0 && -18 + B + I >= 0 && -1 + I + J >= 0 && -1 + I + -1*J >= 0 && -18 + A + I >= 0 && 16 + -1*A + I >= 0 && -3 + C + -1*G >= 0 && -1 + -1*G + Y >= 0 && -1*G + U >= 0 && -4 + B + -1*G >= 0 && G + -1*U >= 0 && -14 + G + T >= 0 && -1*D + X >= 0 && -1*D + W >= 0 && D + -1*X >= 0 && D + -1*W >= 0 && 2 + -1*C + Y >= 0 && -1 + B + -1*C >= 0 && -16 + C >= 0 && -30 + C + Y >= 0 && -2 + C + -1*Y >= 0 && -3 + C + -1*U >= 0 && -17 + C + T >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -16 + C + J >= 0 && -16 + C + -1*J >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && -1*A1 + Z >= 0 && -3 + B + -1*Y >= 0 && -14 + Y >= 0 && -1 + -1*U + Y >= 0 && -15 + T + Y >= 0 && -31 + B + Y >= 0 && 3 + -1*B + Y >= 0 && -14 + J + Y >= 0 && -14 + -1*J + Y >= 0 && -31 + A + Y >= 0 && 3 + -1*A + Y >= 0 && W + -1*X >= 0 && -1*W + X >= 0 && -4 + B + -1*U >= 0 && -14 + T + U >= 0 && -1 + T >= 0 && -18 + B + T >= 0 && -1 + J + T >= 0 && -1 + -1*J + T >= 0 && -18 + A + T >= 0 && 16 + -1*A + T >= 0 && -17 + B >= 0 && -17 + B + J >= 0 && -17 + B + -1*J >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -1*J >= 0 && -17 + A + -1*J >= 0 && 17 + -1*A + -1*J >= 0 && J >= 0 && -17 + A + J >= 0 && 17 + -1*A + J >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && M >= C1 && G >= 0 && 0 >= 1 + H && I >= 0 && P = 0 && J = 0] 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [-1 + B + -1*C >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -17 + A + C >= 0 && 17 + -1*A + C >= 0 && -1 + B >= 0 && -18 + A + B >= 0 && 16 + -1*A + B >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && D1 >= G1 && C >= 2 && E1 >= 1 && B1 >= 1 && B >= A && D >= 1] 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [-1 + B + -1*C >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -17 + A + C >= 0 && 17 + -1*A + C >= 0 && -1 + B >= 0 && -18 + A + B >= 0 && 16 + -1*A + B >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && D1 >= G1 && C >= 2 && E1 >= 1 && B1 >= 1 && B >= A && 0 >= 1 + D] 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [-1 + B + -1*C >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -17 + A + C >= 0 && 17 + -1*A + C >= 0 && -1 + B >= 0 && -18 + A + B >= 0 && 16 + -1*A + B >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && D1 >= G1 && C >= 2 && E1 >= 1 && 0 >= 1 + B1 && B >= A && D >= 1] 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [-1 + B + -1*C >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -17 + A + C >= 0 && 17 + -1*A + C >= 0 && -1 + B >= 0 && -18 + A + B >= 0 && 16 + -1*A + B >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && D1 >= G1 && C >= 2 && E1 >= 1 && 0 >= 1 + B1 && B >= A && 0 >= 1 + D] 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [-1 + B + -1*C >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -17 + A + C >= 0 && 17 + -1*A + C >= 0 && -1 + B >= 0 && -18 + A + B >= 0 && 16 + -1*A + B >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && D1 >= G1 && C >= 2 && 0 >= 1 + E1 && B1 >= 1 && B >= A && D >= 1] 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [-1 + B + -1*C >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -17 + A + C >= 0 && 17 + -1*A + C >= 0 && -1 + B >= 0 && -18 + A + B >= 0 && 16 + -1*A + B >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && D1 >= G1 && C >= 2 && 0 >= 1 + E1 && B1 >= 1 && B >= A && 0 >= 1 + D] 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [-1 + B + -1*C >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -17 + A + C >= 0 && 17 + -1*A + C >= 0 && -1 + B >= 0 && -18 + A + B >= 0 && 16 + -1*A + B >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && D1 >= G1 && C >= 2 && 0 >= 1 + E1 && 0 >= 1 + B1 && B >= A && D >= 1] 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [-1 + B + -1*C >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -17 + A + C >= 0 && 17 + -1*A + C >= 0 && -1 + B >= 0 && -18 + A + B >= 0 && 16 + -1*A + B >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && D1 >= G1 && C >= 2 && 0 >= 1 + E1 && 0 >= 1 + B1 && B >= A && 0 >= 1 + D] 17. f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f9(17,1,0,B1,B1,B1,G,H,I,J,K,L,M,N,O,P,E1,R,S,T,U,V,W,X,Y,Z,A1) True (1,1) Signature: {(f0,27);(f12,27);(f5,27);(f6,27);(f9,27)} Flow Graph: [0->{0,9,10,11,12,13,14,15,16},1->{},2->{},3->{1,2,3,4,5,6,7,8},4->{1,2,3,4,5,6,7,8},5->{1,2,3,4,5,6,7,8} ,6->{1,2,3,4,5,6,7,8},7->{},8->{},9->{1,3,5,7},10->{1,3,5,7},11->{2,4,6,8},12->{2,4,6,8},13->{1,3,5,7} ,14->{1,3,5,7},15->{2,4,6,8},16->{2,4,6,8},17->{0}] + Applied Processor: FromIts + Details: () * Step 3: Decompose YES + Considered Problem: Rules: 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) -> f9(A,1 + B,1 + C,B1,B1,B1,G,H,I,J,K,L,M,N,O ,P,Q,R,S,T,U,V,W,X,Y,Z ,A1) [-1 + B + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -17 + A + C >= 0 && 17 + -1*A + C >= 0 && -1 + B >= 0 && -18 + A + B >= 0 && 16 + -1*A + B >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && A >= 1 + B] 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) -> f0(A,B,C,D,E,F,G,B1,I,H,E1,F1,C1,D1,G1,P,Q,R ,S,T,U,V,W,X,Y,Z ,A1) [-1*I + T >= 0 && -1 + I >= 0 && -14 + G + I >= 0 && -17 + C + I >= 0 && -15 + I + Y >= 0 && -14 + I + U >= 0 && -2 + I + T >= 0 && I + -1*T >= 0 && -18 + B + I >= 0 && -1 + I + J >= 0 && -1 + I + -1*J >= 0 && -18 + A + I >= 0 && 16 + -1*A + I >= 0 && -3 + C + -1*G >= 0 && -1 + -1*G + Y >= 0 && -1*G + U >= 0 && -4 + B + -1*G >= 0 && G + -1*U >= 0 && -14 + G + T >= 0 && -1*D + X >= 0 && -1*D + W >= 0 && D + -1*X >= 0 && D + -1*W >= 0 && 2 + -1*C + Y >= 0 && -1 + B + -1*C >= 0 && -16 + C >= 0 && -30 + C + Y >= 0 && -2 + C + -1*Y >= 0 && -3 + C + -1*U >= 0 && -17 + C + T >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -16 + C + J >= 0 && -16 + C + -1*J >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && -1*A1 + Z >= 0 && -3 + B + -1*Y >= 0 && -14 + Y >= 0 && -1 + -1*U + Y >= 0 && -15 + T + Y >= 0 && -31 + B + Y >= 0 && 3 + -1*B + Y >= 0 && -14 + J + Y >= 0 && -14 + -1*J + Y >= 0 && -31 + A + Y >= 0 && 3 + -1*A + Y >= 0 && W + -1*X >= 0 && -1*W + X >= 0 && -4 + B + -1*U >= 0 && -14 + T + U >= 0 && -1 + T >= 0 && -18 + B + T >= 0 && -1 + J + T >= 0 && -1 + -1*J + T >= 0 && -18 + A + T >= 0 && 16 + -1*A + T >= 0 && -17 + B >= 0 && -17 + B + J >= 0 && -17 + B + -1*J >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -1*J >= 0 && -17 + A + -1*J >= 0 && 17 + -1*A + -1*J >= 0 && J >= 0 && -17 + A + J >= 0 && 17 + -1*A + J >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && D1 >= 1 + C1 && G >= 0 && H >= 1 && I >= 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) -> f0(A,B,C,D,E,F,G,B1,I,H,E1,F1,C1,D1,G1,P,Q,R ,S,T,U,V,W,X,Y,Z ,A1) [-1*I + T >= 0 && -1 + I >= 0 && -14 + G + I >= 0 && -17 + C + I >= 0 && -15 + I + Y >= 0 && -14 + I + U >= 0 && -2 + I + T >= 0 && I + -1*T >= 0 && -18 + B + I >= 0 && -1 + I + J >= 0 && -1 + I + -1*J >= 0 && -18 + A + I >= 0 && 16 + -1*A + I >= 0 && -3 + C + -1*G >= 0 && -1 + -1*G + Y >= 0 && -1*G + U >= 0 && -4 + B + -1*G >= 0 && G + -1*U >= 0 && -14 + G + T >= 0 && -1*D + X >= 0 && -1*D + W >= 0 && D + -1*X >= 0 && D + -1*W >= 0 && 2 + -1*C + Y >= 0 && -1 + B + -1*C >= 0 && -16 + C >= 0 && -30 + C + Y >= 0 && -2 + C + -1*Y >= 0 && -3 + C + -1*U >= 0 && -17 + C + T >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -16 + C + J >= 0 && -16 + C + -1*J >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && -1*A1 + Z >= 0 && -3 + B + -1*Y >= 0 && -14 + Y >= 0 && -1 + -1*U + Y >= 0 && -15 + T + Y >= 0 && -31 + B + Y >= 0 && 3 + -1*B + Y >= 0 && -14 + J + Y >= 0 && -14 + -1*J + Y >= 0 && -31 + A + Y >= 0 && 3 + -1*A + Y >= 0 && W + -1*X >= 0 && -1*W + X >= 0 && -4 + B + -1*U >= 0 && -14 + T + U >= 0 && -1 + T >= 0 && -18 + B + T >= 0 && -1 + J + T >= 0 && -1 + -1*J + T >= 0 && -18 + A + T >= 0 && 16 + -1*A + T >= 0 && -17 + B >= 0 && -17 + B + J >= 0 && -17 + B + -1*J >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -1*J >= 0 && -17 + A + -1*J >= 0 && 17 + -1*A + -1*J >= 0 && J >= 0 && -17 + A + J >= 0 && 17 + -1*A + J >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && D1 >= 1 + C1 && G >= 0 && 0 >= 1 + H && I >= 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) -> f5(A,B,C,D,E,F,-1 + G,R,1 + I,0,F1,C1,M,D1,O ,E1,R,P,B1,1 + I,-1 + G,I,W,X,Y,Z ,A1) [-1*I + T >= 0 && -1 + I >= 0 && -14 + G + I >= 0 && -17 + C + I >= 0 && -15 + I + Y >= 0 && -14 + I + U >= 0 && -2 + I + T >= 0 && I + -1*T >= 0 && -18 + B + I >= 0 && -1 + I + J >= 0 && -1 + I + -1*J >= 0 && -18 + A + I >= 0 && 16 + -1*A + I >= 0 && -3 + C + -1*G >= 0 && -1 + -1*G + Y >= 0 && -1*G + U >= 0 && -4 + B + -1*G >= 0 && G + -1*U >= 0 && -14 + G + T >= 0 && -1*D + X >= 0 && -1*D + W >= 0 && D + -1*X >= 0 && D + -1*W >= 0 && 2 + -1*C + Y >= 0 && -1 + B + -1*C >= 0 && -16 + C >= 0 && -30 + C + Y >= 0 && -2 + C + -1*Y >= 0 && -3 + C + -1*U >= 0 && -17 + C + T >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -16 + C + J >= 0 && -16 + C + -1*J >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && -1*A1 + Z >= 0 && -3 + B + -1*Y >= 0 && -14 + Y >= 0 && -1 + -1*U + Y >= 0 && -15 + T + Y >= 0 && -31 + B + Y >= 0 && 3 + -1*B + Y >= 0 && -14 + J + Y >= 0 && -14 + -1*J + Y >= 0 && -31 + A + Y >= 0 && 3 + -1*A + Y >= 0 && W + -1*X >= 0 && -1*W + X >= 0 && -4 + B + -1*U >= 0 && -14 + T + U >= 0 && -1 + T >= 0 && -18 + B + T >= 0 && -1 + J + T >= 0 && -1 + -1*J + T >= 0 && -18 + A + T >= 0 && 16 + -1*A + T >= 0 && -17 + B >= 0 && -17 + B + J >= 0 && -17 + B + -1*J >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -1*J >= 0 && -17 + A + -1*J >= 0 && 17 + -1*A + -1*J >= 0 && J >= 0 && -17 + A + J >= 0 && 17 + -1*A + J >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && M >= D1 && G >= 0 && I >= 0 && P >= 1 && H >= 1 && J = 0] 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) -> f5(A,B,C,D,E,F,-1 + G,R,1 + I,0,F1,C1,M,D1,O ,E1,R,P,B1,1 + I,-1 + G,I,W,X,Y,Z ,A1) [-1*I + T >= 0 && -1 + I >= 0 && -14 + G + I >= 0 && -17 + C + I >= 0 && -15 + I + Y >= 0 && -14 + I + U >= 0 && -2 + I + T >= 0 && I + -1*T >= 0 && -18 + B + I >= 0 && -1 + I + J >= 0 && -1 + I + -1*J >= 0 && -18 + A + I >= 0 && 16 + -1*A + I >= 0 && -3 + C + -1*G >= 0 && -1 + -1*G + Y >= 0 && -1*G + U >= 0 && -4 + B + -1*G >= 0 && G + -1*U >= 0 && -14 + G + T >= 0 && -1*D + X >= 0 && -1*D + W >= 0 && D + -1*X >= 0 && D + -1*W >= 0 && 2 + -1*C + Y >= 0 && -1 + B + -1*C >= 0 && -16 + C >= 0 && -30 + C + Y >= 0 && -2 + C + -1*Y >= 0 && -3 + C + -1*U >= 0 && -17 + C + T >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -16 + C + J >= 0 && -16 + C + -1*J >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && -1*A1 + Z >= 0 && -3 + B + -1*Y >= 0 && -14 + Y >= 0 && -1 + -1*U + Y >= 0 && -15 + T + Y >= 0 && -31 + B + Y >= 0 && 3 + -1*B + Y >= 0 && -14 + J + Y >= 0 && -14 + -1*J + Y >= 0 && -31 + A + Y >= 0 && 3 + -1*A + Y >= 0 && W + -1*X >= 0 && -1*W + X >= 0 && -4 + B + -1*U >= 0 && -14 + T + U >= 0 && -1 + T >= 0 && -18 + B + T >= 0 && -1 + J + T >= 0 && -1 + -1*J + T >= 0 && -18 + A + T >= 0 && 16 + -1*A + T >= 0 && -17 + B >= 0 && -17 + B + J >= 0 && -17 + B + -1*J >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -1*J >= 0 && -17 + A + -1*J >= 0 && 17 + -1*A + -1*J >= 0 && J >= 0 && -17 + A + J >= 0 && 17 + -1*A + J >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && M >= D1 && G >= 0 && I >= 0 && P >= 1 && 0 >= 1 + H && J = 0] 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) -> f5(A,B,C,D,E,F,-1 + G,R,1 + I,0,F1,C1,M,D1,O ,E1,R,P,B1,1 + I,-1 + G,I,W,X,Y,Z ,A1) [-1*I + T >= 0 && -1 + I >= 0 && -14 + G + I >= 0 && -17 + C + I >= 0 && -15 + I + Y >= 0 && -14 + I + U >= 0 && -2 + I + T >= 0 && I + -1*T >= 0 && -18 + B + I >= 0 && -1 + I + J >= 0 && -1 + I + -1*J >= 0 && -18 + A + I >= 0 && 16 + -1*A + I >= 0 && -3 + C + -1*G >= 0 && -1 + -1*G + Y >= 0 && -1*G + U >= 0 && -4 + B + -1*G >= 0 && G + -1*U >= 0 && -14 + G + T >= 0 && -1*D + X >= 0 && -1*D + W >= 0 && D + -1*X >= 0 && D + -1*W >= 0 && 2 + -1*C + Y >= 0 && -1 + B + -1*C >= 0 && -16 + C >= 0 && -30 + C + Y >= 0 && -2 + C + -1*Y >= 0 && -3 + C + -1*U >= 0 && -17 + C + T >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -16 + C + J >= 0 && -16 + C + -1*J >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && -1*A1 + Z >= 0 && -3 + B + -1*Y >= 0 && -14 + Y >= 0 && -1 + -1*U + Y >= 0 && -15 + T + Y >= 0 && -31 + B + Y >= 0 && 3 + -1*B + Y >= 0 && -14 + J + Y >= 0 && -14 + -1*J + Y >= 0 && -31 + A + Y >= 0 && 3 + -1*A + Y >= 0 && W + -1*X >= 0 && -1*W + X >= 0 && -4 + B + -1*U >= 0 && -14 + T + U >= 0 && -1 + T >= 0 && -18 + B + T >= 0 && -1 + J + T >= 0 && -1 + -1*J + T >= 0 && -18 + A + T >= 0 && 16 + -1*A + T >= 0 && -17 + B >= 0 && -17 + B + J >= 0 && -17 + B + -1*J >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -1*J >= 0 && -17 + A + -1*J >= 0 && 17 + -1*A + -1*J >= 0 && J >= 0 && -17 + A + J >= 0 && 17 + -1*A + J >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && M >= D1 && G >= 0 && I >= 0 && 0 >= 1 + P && H >= 1 && J = 0] 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) -> f5(A,B,C,D,E,F,-1 + G,R,1 + I,0,F1,C1,M,D1,O ,E1,R,P,B1,1 + I,-1 + G,I,W,X,Y,Z ,A1) [-1*I + T >= 0 && -1 + I >= 0 && -14 + G + I >= 0 && -17 + C + I >= 0 && -15 + I + Y >= 0 && -14 + I + U >= 0 && -2 + I + T >= 0 && I + -1*T >= 0 && -18 + B + I >= 0 && -1 + I + J >= 0 && -1 + I + -1*J >= 0 && -18 + A + I >= 0 && 16 + -1*A + I >= 0 && -3 + C + -1*G >= 0 && -1 + -1*G + Y >= 0 && -1*G + U >= 0 && -4 + B + -1*G >= 0 && G + -1*U >= 0 && -14 + G + T >= 0 && -1*D + X >= 0 && -1*D + W >= 0 && D + -1*X >= 0 && D + -1*W >= 0 && 2 + -1*C + Y >= 0 && -1 + B + -1*C >= 0 && -16 + C >= 0 && -30 + C + Y >= 0 && -2 + C + -1*Y >= 0 && -3 + C + -1*U >= 0 && -17 + C + T >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -16 + C + J >= 0 && -16 + C + -1*J >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && -1*A1 + Z >= 0 && -3 + B + -1*Y >= 0 && -14 + Y >= 0 && -1 + -1*U + Y >= 0 && -15 + T + Y >= 0 && -31 + B + Y >= 0 && 3 + -1*B + Y >= 0 && -14 + J + Y >= 0 && -14 + -1*J + Y >= 0 && -31 + A + Y >= 0 && 3 + -1*A + Y >= 0 && W + -1*X >= 0 && -1*W + X >= 0 && -4 + B + -1*U >= 0 && -14 + T + U >= 0 && -1 + T >= 0 && -18 + B + T >= 0 && -1 + J + T >= 0 && -1 + -1*J + T >= 0 && -18 + A + T >= 0 && 16 + -1*A + T >= 0 && -17 + B >= 0 && -17 + B + J >= 0 && -17 + B + -1*J >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -1*J >= 0 && -17 + A + -1*J >= 0 && 17 + -1*A + -1*J >= 0 && J >= 0 && -17 + A + J >= 0 && 17 + -1*A + J >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && M >= D1 && G >= 0 && I >= 0 && 0 >= 1 + P && 0 >= 1 + H && J = 0] 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) -> f12(A,B,C,D,E,F,G,H,I,0,E1,F1,M,C1,O,0,R,R,S ,T,U,I,B1,X,Y,Z ,A1) [-1*I + T >= 0 && -1 + I >= 0 && -14 + G + I >= 0 && -17 + C + I >= 0 && -15 + I + Y >= 0 && -14 + I + U >= 0 && -2 + I + T >= 0 && I + -1*T >= 0 && -18 + B + I >= 0 && -1 + I + J >= 0 && -1 + I + -1*J >= 0 && -18 + A + I >= 0 && 16 + -1*A + I >= 0 && -3 + C + -1*G >= 0 && -1 + -1*G + Y >= 0 && -1*G + U >= 0 && -4 + B + -1*G >= 0 && G + -1*U >= 0 && -14 + G + T >= 0 && -1*D + X >= 0 && -1*D + W >= 0 && D + -1*X >= 0 && D + -1*W >= 0 && 2 + -1*C + Y >= 0 && -1 + B + -1*C >= 0 && -16 + C >= 0 && -30 + C + Y >= 0 && -2 + C + -1*Y >= 0 && -3 + C + -1*U >= 0 && -17 + C + T >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -16 + C + J >= 0 && -16 + C + -1*J >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && -1*A1 + Z >= 0 && -3 + B + -1*Y >= 0 && -14 + Y >= 0 && -1 + -1*U + Y >= 0 && -15 + T + Y >= 0 && -31 + B + Y >= 0 && 3 + -1*B + Y >= 0 && -14 + J + Y >= 0 && -14 + -1*J + Y >= 0 && -31 + A + Y >= 0 && 3 + -1*A + Y >= 0 && W + -1*X >= 0 && -1*W + X >= 0 && -4 + B + -1*U >= 0 && -14 + T + U >= 0 && -1 + T >= 0 && -18 + B + T >= 0 && -1 + J + T >= 0 && -1 + -1*J + T >= 0 && -18 + A + T >= 0 && 16 + -1*A + T >= 0 && -17 + B >= 0 && -17 + B + J >= 0 && -17 + B + -1*J >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -1*J >= 0 && -17 + A + -1*J >= 0 && 17 + -1*A + -1*J >= 0 && J >= 0 && -17 + A + J >= 0 && 17 + -1*A + J >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && M >= C1 && G >= 0 && H >= 1 && I >= 0 && P = 0 && J = 0] 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) -> f12(A,B,C,D,E,F,G,H,I,0,E1,F1,M,C1,O,0,R,R,S ,T,U,I,B1,X,Y,Z ,A1) [-1*I + T >= 0 && -1 + I >= 0 && -14 + G + I >= 0 && -17 + C + I >= 0 && -15 + I + Y >= 0 && -14 + I + U >= 0 && -2 + I + T >= 0 && I + -1*T >= 0 && -18 + B + I >= 0 && -1 + I + J >= 0 && -1 + I + -1*J >= 0 && -18 + A + I >= 0 && 16 + -1*A + I >= 0 && -3 + C + -1*G >= 0 && -1 + -1*G + Y >= 0 && -1*G + U >= 0 && -4 + B + -1*G >= 0 && G + -1*U >= 0 && -14 + G + T >= 0 && -1*D + X >= 0 && -1*D + W >= 0 && D + -1*X >= 0 && D + -1*W >= 0 && 2 + -1*C + Y >= 0 && -1 + B + -1*C >= 0 && -16 + C >= 0 && -30 + C + Y >= 0 && -2 + C + -1*Y >= 0 && -3 + C + -1*U >= 0 && -17 + C + T >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -16 + C + J >= 0 && -16 + C + -1*J >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && -1*A1 + Z >= 0 && -3 + B + -1*Y >= 0 && -14 + Y >= 0 && -1 + -1*U + Y >= 0 && -15 + T + Y >= 0 && -31 + B + Y >= 0 && 3 + -1*B + Y >= 0 && -14 + J + Y >= 0 && -14 + -1*J + Y >= 0 && -31 + A + Y >= 0 && 3 + -1*A + Y >= 0 && W + -1*X >= 0 && -1*W + X >= 0 && -4 + B + -1*U >= 0 && -14 + T + U >= 0 && -1 + T >= 0 && -18 + B + T >= 0 && -1 + J + T >= 0 && -1 + -1*J + T >= 0 && -18 + A + T >= 0 && 16 + -1*A + T >= 0 && -17 + B >= 0 && -17 + B + J >= 0 && -17 + B + -1*J >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -1*J >= 0 && -17 + A + -1*J >= 0 && 17 + -1*A + -1*J >= 0 && J >= 0 && -17 + A + J >= 0 && 17 + -1*A + J >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && M >= C1 && G >= 0 && 0 >= 1 + H && I >= 0 && P = 0 && J = 0] f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1 ,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1 ,G1) [-1 + B + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -17 + A + C >= 0 && 17 + -1*A + C >= 0 && -1 + B >= 0 && -18 + A + B >= 0 && 16 + -1*A + B >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && D1 >= G1 && C >= 2 && E1 >= 1 && B1 >= 1 && B >= A && D >= 1] 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1 ,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1 ,G1) [-1 + B + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -17 + A + C >= 0 && 17 + -1*A + C >= 0 && -1 + B >= 0 && -18 + A + B >= 0 && 16 + -1*A + B >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && D1 >= G1 && C >= 2 && E1 >= 1 && B1 >= 1 && B >= A && 0 >= 1 + D] 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1 ,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1 ,G1) [-1 + B + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -17 + A + C >= 0 && 17 + -1*A + C >= 0 && -1 + B >= 0 && -18 + A + B >= 0 && 16 + -1*A + B >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && D1 >= G1 && C >= 2 && E1 >= 1 && 0 >= 1 + B1 && B >= A && D >= 1] 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1 ,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1 ,G1) [-1 + B + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -17 + A + C >= 0 && 17 + -1*A + C >= 0 && -1 + B >= 0 && -18 + A + B >= 0 && 16 + -1*A + B >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && D1 >= G1 && C >= 2 && E1 >= 1 && 0 >= 1 + B1 && B >= A && 0 >= 1 + D] 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1 ,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1 ,G1) [-1 + B + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -17 + A + C >= 0 && 17 + -1*A + C >= 0 && -1 + B >= 0 && -18 + A + B >= 0 && 16 + -1*A + B >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && D1 >= G1 && C >= 2 && 0 >= 1 + E1 && B1 >= 1 && B >= A && D >= 1] 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1 ,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1 ,G1) [-1 + B + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -17 + A + C >= 0 && 17 + -1*A + C >= 0 && -1 + B >= 0 && -18 + A + B >= 0 && 16 + -1*A + B >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && D1 >= G1 && C >= 2 && 0 >= 1 + E1 && B1 >= 1 && B >= A && 0 >= 1 + D] 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1 ,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1 ,G1) [-1 + B + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -17 + A + C >= 0 && 17 + -1*A + C >= 0 && -1 + B >= 0 && -18 + A + B >= 0 && 16 + -1*A + B >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && D1 >= G1 && C >= 2 && 0 >= 1 + E1 && 0 >= 1 + B1 && B >= A && D >= 1] 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1 ,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1 ,G1) [-1 + B + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -17 + A + C >= 0 && 17 + -1*A + C >= 0 && -1 + B >= 0 && -18 + A + B >= 0 && 16 + -1*A + B >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && D1 >= G1 && C >= 2 && 0 >= 1 + E1 && 0 >= 1 + B1 && B >= A && 0 >= 1 + D] f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f9(17,1,0,B1,B1,B1,G,H,I,J,K,L,M,N,O,P,E1,R,S ,T,U,V,W,X,Y,Z ,A1) True Signature: {(f0,27);(f12,27);(f5,27);(f6,27);(f9,27)} Rule Graph: [0->{0,9,10,11,12,13,14,15,16},1->{},2->{},3->{1,2,3,4,5,6,7,8},4->{1,2,3,4,5,6,7,8},5->{1,2,3,4,5,6,7,8} ,6->{1,2,3,4,5,6,7,8},7->{},8->{},9->{1,3,5,7},10->{1,3,5,7},11->{2,4,6,8},12->{2,4,6,8},13->{1,3,5,7} ,14->{1,3,5,7},15->{2,4,6,8},16->{2,4,6,8},17->{0}] + Applied Processor: Decompose NoGreedy + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17] | +- p:[0] c: [0] | `- p:[3,4,5,6] c: [6] | `- p:[3,4,5] c: [5] | `- p:[3,4] c: [4] | `- p:[3] c: [3] * Step 4: CloseWith YES + Considered Problem: (Rules: 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) -> f9(A,1 + B,1 + C,B1,B1,B1,G,H,I,J,K,L,M,N,O ,P,Q,R,S,T,U,V,W,X,Y,Z ,A1) [-1 + B + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -17 + A + C >= 0 && 17 + -1*A + C >= 0 && -1 + B >= 0 && -18 + A + B >= 0 && 16 + -1*A + B >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && A >= 1 + B] 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) -> f0(A,B,C,D,E,F,G,B1,I,H,E1,F1,C1,D1,G1,P,Q,R ,S,T,U,V,W,X,Y,Z ,A1) [-1*I + T >= 0 && -1 + I >= 0 && -14 + G + I >= 0 && -17 + C + I >= 0 && -15 + I + Y >= 0 && -14 + I + U >= 0 && -2 + I + T >= 0 && I + -1*T >= 0 && -18 + B + I >= 0 && -1 + I + J >= 0 && -1 + I + -1*J >= 0 && -18 + A + I >= 0 && 16 + -1*A + I >= 0 && -3 + C + -1*G >= 0 && -1 + -1*G + Y >= 0 && -1*G + U >= 0 && -4 + B + -1*G >= 0 && G + -1*U >= 0 && -14 + G + T >= 0 && -1*D + X >= 0 && -1*D + W >= 0 && D + -1*X >= 0 && D + -1*W >= 0 && 2 + -1*C + Y >= 0 && -1 + B + -1*C >= 0 && -16 + C >= 0 && -30 + C + Y >= 0 && -2 + C + -1*Y >= 0 && -3 + C + -1*U >= 0 && -17 + C + T >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -16 + C + J >= 0 && -16 + C + -1*J >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && -1*A1 + Z >= 0 && -3 + B + -1*Y >= 0 && -14 + Y >= 0 && -1 + -1*U + Y >= 0 && -15 + T + Y >= 0 && -31 + B + Y >= 0 && 3 + -1*B + Y >= 0 && -14 + J + Y >= 0 && -14 + -1*J + Y >= 0 && -31 + A + Y >= 0 && 3 + -1*A + Y >= 0 && W + -1*X >= 0 && -1*W + X >= 0 && -4 + B + -1*U >= 0 && -14 + T + U >= 0 && -1 + T >= 0 && -18 + B + T >= 0 && -1 + J + T >= 0 && -1 + -1*J + T >= 0 && -18 + A + T >= 0 && 16 + -1*A + T >= 0 && -17 + B >= 0 && -17 + B + J >= 0 && -17 + B + -1*J >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -1*J >= 0 && -17 + A + -1*J >= 0 && 17 + -1*A + -1*J >= 0 && J >= 0 && -17 + A + J >= 0 && 17 + -1*A + J >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && D1 >= 1 + C1 && G >= 0 && H >= 1 && I >= 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) -> f0(A,B,C,D,E,F,G,B1,I,H,E1,F1,C1,D1,G1,P,Q,R ,S,T,U,V,W,X,Y,Z ,A1) [-1*I + T >= 0 && -1 + I >= 0 && -14 + G + I >= 0 && -17 + C + I >= 0 && -15 + I + Y >= 0 && -14 + I + U >= 0 && -2 + I + T >= 0 && I + -1*T >= 0 && -18 + B + I >= 0 && -1 + I + J >= 0 && -1 + I + -1*J >= 0 && -18 + A + I >= 0 && 16 + -1*A + I >= 0 && -3 + C + -1*G >= 0 && -1 + -1*G + Y >= 0 && -1*G + U >= 0 && -4 + B + -1*G >= 0 && G + -1*U >= 0 && -14 + G + T >= 0 && -1*D + X >= 0 && -1*D + W >= 0 && D + -1*X >= 0 && D + -1*W >= 0 && 2 + -1*C + Y >= 0 && -1 + B + -1*C >= 0 && -16 + C >= 0 && -30 + C + Y >= 0 && -2 + C + -1*Y >= 0 && -3 + C + -1*U >= 0 && -17 + C + T >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -16 + C + J >= 0 && -16 + C + -1*J >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && -1*A1 + Z >= 0 && -3 + B + -1*Y >= 0 && -14 + Y >= 0 && -1 + -1*U + Y >= 0 && -15 + T + Y >= 0 && -31 + B + Y >= 0 && 3 + -1*B + Y >= 0 && -14 + J + Y >= 0 && -14 + -1*J + Y >= 0 && -31 + A + Y >= 0 && 3 + -1*A + Y >= 0 && W + -1*X >= 0 && -1*W + X >= 0 && -4 + B + -1*U >= 0 && -14 + T + U >= 0 && -1 + T >= 0 && -18 + B + T >= 0 && -1 + J + T >= 0 && -1 + -1*J + T >= 0 && -18 + A + T >= 0 && 16 + -1*A + T >= 0 && -17 + B >= 0 && -17 + B + J >= 0 && -17 + B + -1*J >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -1*J >= 0 && -17 + A + -1*J >= 0 && 17 + -1*A + -1*J >= 0 && J >= 0 && -17 + A + J >= 0 && 17 + -1*A + J >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && D1 >= 1 + C1 && G >= 0 && 0 >= 1 + H && I >= 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) -> f5(A,B,C,D,E,F,-1 + G,R,1 + I,0,F1,C1,M,D1,O ,E1,R,P,B1,1 + I,-1 + G,I,W,X,Y,Z ,A1) [-1*I + T >= 0 && -1 + I >= 0 && -14 + G + I >= 0 && -17 + C + I >= 0 && -15 + I + Y >= 0 && -14 + I + U >= 0 && -2 + I + T >= 0 && I + -1*T >= 0 && -18 + B + I >= 0 && -1 + I + J >= 0 && -1 + I + -1*J >= 0 && -18 + A + I >= 0 && 16 + -1*A + I >= 0 && -3 + C + -1*G >= 0 && -1 + -1*G + Y >= 0 && -1*G + U >= 0 && -4 + B + -1*G >= 0 && G + -1*U >= 0 && -14 + G + T >= 0 && -1*D + X >= 0 && -1*D + W >= 0 && D + -1*X >= 0 && D + -1*W >= 0 && 2 + -1*C + Y >= 0 && -1 + B + -1*C >= 0 && -16 + C >= 0 && -30 + C + Y >= 0 && -2 + C + -1*Y >= 0 && -3 + C + -1*U >= 0 && -17 + C + T >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -16 + C + J >= 0 && -16 + C + -1*J >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && -1*A1 + Z >= 0 && -3 + B + -1*Y >= 0 && -14 + Y >= 0 && -1 + -1*U + Y >= 0 && -15 + T + Y >= 0 && -31 + B + Y >= 0 && 3 + -1*B + Y >= 0 && -14 + J + Y >= 0 && -14 + -1*J + Y >= 0 && -31 + A + Y >= 0 && 3 + -1*A + Y >= 0 && W + -1*X >= 0 && -1*W + X >= 0 && -4 + B + -1*U >= 0 && -14 + T + U >= 0 && -1 + T >= 0 && -18 + B + T >= 0 && -1 + J + T >= 0 && -1 + -1*J + T >= 0 && -18 + A + T >= 0 && 16 + -1*A + T >= 0 && -17 + B >= 0 && -17 + B + J >= 0 && -17 + B + -1*J >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -1*J >= 0 && -17 + A + -1*J >= 0 && 17 + -1*A + -1*J >= 0 && J >= 0 && -17 + A + J >= 0 && 17 + -1*A + J >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && M >= D1 && G >= 0 && I >= 0 && P >= 1 && H >= 1 && J = 0] 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) -> f5(A,B,C,D,E,F,-1 + G,R,1 + I,0,F1,C1,M,D1,O ,E1,R,P,B1,1 + I,-1 + G,I,W,X,Y,Z ,A1) [-1*I + T >= 0 && -1 + I >= 0 && -14 + G + I >= 0 && -17 + C + I >= 0 && -15 + I + Y >= 0 && -14 + I + U >= 0 && -2 + I + T >= 0 && I + -1*T >= 0 && -18 + B + I >= 0 && -1 + I + J >= 0 && -1 + I + -1*J >= 0 && -18 + A + I >= 0 && 16 + -1*A + I >= 0 && -3 + C + -1*G >= 0 && -1 + -1*G + Y >= 0 && -1*G + U >= 0 && -4 + B + -1*G >= 0 && G + -1*U >= 0 && -14 + G + T >= 0 && -1*D + X >= 0 && -1*D + W >= 0 && D + -1*X >= 0 && D + -1*W >= 0 && 2 + -1*C + Y >= 0 && -1 + B + -1*C >= 0 && -16 + C >= 0 && -30 + C + Y >= 0 && -2 + C + -1*Y >= 0 && -3 + C + -1*U >= 0 && -17 + C + T >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -16 + C + J >= 0 && -16 + C + -1*J >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && -1*A1 + Z >= 0 && -3 + B + -1*Y >= 0 && -14 + Y >= 0 && -1 + -1*U + Y >= 0 && -15 + T + Y >= 0 && -31 + B + Y >= 0 && 3 + -1*B + Y >= 0 && -14 + J + Y >= 0 && -14 + -1*J + Y >= 0 && -31 + A + Y >= 0 && 3 + -1*A + Y >= 0 && W + -1*X >= 0 && -1*W + X >= 0 && -4 + B + -1*U >= 0 && -14 + T + U >= 0 && -1 + T >= 0 && -18 + B + T >= 0 && -1 + J + T >= 0 && -1 + -1*J + T >= 0 && -18 + A + T >= 0 && 16 + -1*A + T >= 0 && -17 + B >= 0 && -17 + B + J >= 0 && -17 + B + -1*J >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -1*J >= 0 && -17 + A + -1*J >= 0 && 17 + -1*A + -1*J >= 0 && J >= 0 && -17 + A + J >= 0 && 17 + -1*A + J >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && M >= D1 && G >= 0 && I >= 0 && P >= 1 && 0 >= 1 + H && J = 0] 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) -> f5(A,B,C,D,E,F,-1 + G,R,1 + I,0,F1,C1,M,D1,O ,E1,R,P,B1,1 + I,-1 + G,I,W,X,Y,Z ,A1) [-1*I + T >= 0 && -1 + I >= 0 && -14 + G + I >= 0 && -17 + C + I >= 0 && -15 + I + Y >= 0 && -14 + I + U >= 0 && -2 + I + T >= 0 && I + -1*T >= 0 && -18 + B + I >= 0 && -1 + I + J >= 0 && -1 + I + -1*J >= 0 && -18 + A + I >= 0 && 16 + -1*A + I >= 0 && -3 + C + -1*G >= 0 && -1 + -1*G + Y >= 0 && -1*G + U >= 0 && -4 + B + -1*G >= 0 && G + -1*U >= 0 && -14 + G + T >= 0 && -1*D + X >= 0 && -1*D + W >= 0 && D + -1*X >= 0 && D + -1*W >= 0 && 2 + -1*C + Y >= 0 && -1 + B + -1*C >= 0 && -16 + C >= 0 && -30 + C + Y >= 0 && -2 + C + -1*Y >= 0 && -3 + C + -1*U >= 0 && -17 + C + T >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -16 + C + J >= 0 && -16 + C + -1*J >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && -1*A1 + Z >= 0 && -3 + B + -1*Y >= 0 && -14 + Y >= 0 && -1 + -1*U + Y >= 0 && -15 + T + Y >= 0 && -31 + B + Y >= 0 && 3 + -1*B + Y >= 0 && -14 + J + Y >= 0 && -14 + -1*J + Y >= 0 && -31 + A + Y >= 0 && 3 + -1*A + Y >= 0 && W + -1*X >= 0 && -1*W + X >= 0 && -4 + B + -1*U >= 0 && -14 + T + U >= 0 && -1 + T >= 0 && -18 + B + T >= 0 && -1 + J + T >= 0 && -1 + -1*J + T >= 0 && -18 + A + T >= 0 && 16 + -1*A + T >= 0 && -17 + B >= 0 && -17 + B + J >= 0 && -17 + B + -1*J >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -1*J >= 0 && -17 + A + -1*J >= 0 && 17 + -1*A + -1*J >= 0 && J >= 0 && -17 + A + J >= 0 && 17 + -1*A + J >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && M >= D1 && G >= 0 && I >= 0 && 0 >= 1 + P && H >= 1 && J = 0] 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) -> f5(A,B,C,D,E,F,-1 + G,R,1 + I,0,F1,C1,M,D1,O ,E1,R,P,B1,1 + I,-1 + G,I,W,X,Y,Z ,A1) [-1*I + T >= 0 && -1 + I >= 0 && -14 + G + I >= 0 && -17 + C + I >= 0 && -15 + I + Y >= 0 && -14 + I + U >= 0 && -2 + I + T >= 0 && I + -1*T >= 0 && -18 + B + I >= 0 && -1 + I + J >= 0 && -1 + I + -1*J >= 0 && -18 + A + I >= 0 && 16 + -1*A + I >= 0 && -3 + C + -1*G >= 0 && -1 + -1*G + Y >= 0 && -1*G + U >= 0 && -4 + B + -1*G >= 0 && G + -1*U >= 0 && -14 + G + T >= 0 && -1*D + X >= 0 && -1*D + W >= 0 && D + -1*X >= 0 && D + -1*W >= 0 && 2 + -1*C + Y >= 0 && -1 + B + -1*C >= 0 && -16 + C >= 0 && -30 + C + Y >= 0 && -2 + C + -1*Y >= 0 && -3 + C + -1*U >= 0 && -17 + C + T >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -16 + C + J >= 0 && -16 + C + -1*J >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && -1*A1 + Z >= 0 && -3 + B + -1*Y >= 0 && -14 + Y >= 0 && -1 + -1*U + Y >= 0 && -15 + T + Y >= 0 && -31 + B + Y >= 0 && 3 + -1*B + Y >= 0 && -14 + J + Y >= 0 && -14 + -1*J + Y >= 0 && -31 + A + Y >= 0 && 3 + -1*A + Y >= 0 && W + -1*X >= 0 && -1*W + X >= 0 && -4 + B + -1*U >= 0 && -14 + T + U >= 0 && -1 + T >= 0 && -18 + B + T >= 0 && -1 + J + T >= 0 && -1 + -1*J + T >= 0 && -18 + A + T >= 0 && 16 + -1*A + T >= 0 && -17 + B >= 0 && -17 + B + J >= 0 && -17 + B + -1*J >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -1*J >= 0 && -17 + A + -1*J >= 0 && 17 + -1*A + -1*J >= 0 && J >= 0 && -17 + A + J >= 0 && 17 + -1*A + J >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && M >= D1 && G >= 0 && I >= 0 && 0 >= 1 + P && 0 >= 1 + H && J = 0] 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) -> f12(A,B,C,D,E,F,G,H,I,0,E1,F1,M,C1,O,0,R,R,S ,T,U,I,B1,X,Y,Z ,A1) [-1*I + T >= 0 && -1 + I >= 0 && -14 + G + I >= 0 && -17 + C + I >= 0 && -15 + I + Y >= 0 && -14 + I + U >= 0 && -2 + I + T >= 0 && I + -1*T >= 0 && -18 + B + I >= 0 && -1 + I + J >= 0 && -1 + I + -1*J >= 0 && -18 + A + I >= 0 && 16 + -1*A + I >= 0 && -3 + C + -1*G >= 0 && -1 + -1*G + Y >= 0 && -1*G + U >= 0 && -4 + B + -1*G >= 0 && G + -1*U >= 0 && -14 + G + T >= 0 && -1*D + X >= 0 && -1*D + W >= 0 && D + -1*X >= 0 && D + -1*W >= 0 && 2 + -1*C + Y >= 0 && -1 + B + -1*C >= 0 && -16 + C >= 0 && -30 + C + Y >= 0 && -2 + C + -1*Y >= 0 && -3 + C + -1*U >= 0 && -17 + C + T >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -16 + C + J >= 0 && -16 + C + -1*J >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && -1*A1 + Z >= 0 && -3 + B + -1*Y >= 0 && -14 + Y >= 0 && -1 + -1*U + Y >= 0 && -15 + T + Y >= 0 && -31 + B + Y >= 0 && 3 + -1*B + Y >= 0 && -14 + J + Y >= 0 && -14 + -1*J + Y >= 0 && -31 + A + Y >= 0 && 3 + -1*A + Y >= 0 && W + -1*X >= 0 && -1*W + X >= 0 && -4 + B + -1*U >= 0 && -14 + T + U >= 0 && -1 + T >= 0 && -18 + B + T >= 0 && -1 + J + T >= 0 && -1 + -1*J + T >= 0 && -18 + A + T >= 0 && 16 + -1*A + T >= 0 && -17 + B >= 0 && -17 + B + J >= 0 && -17 + B + -1*J >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -1*J >= 0 && -17 + A + -1*J >= 0 && 17 + -1*A + -1*J >= 0 && J >= 0 && -17 + A + J >= 0 && 17 + -1*A + J >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && M >= C1 && G >= 0 && H >= 1 && I >= 0 && P = 0 && J = 0] 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) -> f12(A,B,C,D,E,F,G,H,I,0,E1,F1,M,C1,O,0,R,R,S ,T,U,I,B1,X,Y,Z ,A1) [-1*I + T >= 0 && -1 + I >= 0 && -14 + G + I >= 0 && -17 + C + I >= 0 && -15 + I + Y >= 0 && -14 + I + U >= 0 && -2 + I + T >= 0 && I + -1*T >= 0 && -18 + B + I >= 0 && -1 + I + J >= 0 && -1 + I + -1*J >= 0 && -18 + A + I >= 0 && 16 + -1*A + I >= 0 && -3 + C + -1*G >= 0 && -1 + -1*G + Y >= 0 && -1*G + U >= 0 && -4 + B + -1*G >= 0 && G + -1*U >= 0 && -14 + G + T >= 0 && -1*D + X >= 0 && -1*D + W >= 0 && D + -1*X >= 0 && D + -1*W >= 0 && 2 + -1*C + Y >= 0 && -1 + B + -1*C >= 0 && -16 + C >= 0 && -30 + C + Y >= 0 && -2 + C + -1*Y >= 0 && -3 + C + -1*U >= 0 && -17 + C + T >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -16 + C + J >= 0 && -16 + C + -1*J >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && -1*A1 + Z >= 0 && -3 + B + -1*Y >= 0 && -14 + Y >= 0 && -1 + -1*U + Y >= 0 && -15 + T + Y >= 0 && -31 + B + Y >= 0 && 3 + -1*B + Y >= 0 && -14 + J + Y >= 0 && -14 + -1*J + Y >= 0 && -31 + A + Y >= 0 && 3 + -1*A + Y >= 0 && W + -1*X >= 0 && -1*W + X >= 0 && -4 + B + -1*U >= 0 && -14 + T + U >= 0 && -1 + T >= 0 && -18 + B + T >= 0 && -1 + J + T >= 0 && -1 + -1*J + T >= 0 && -18 + A + T >= 0 && 16 + -1*A + T >= 0 && -17 + B >= 0 && -17 + B + J >= 0 && -17 + B + -1*J >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -1*J >= 0 && -17 + A + -1*J >= 0 && 17 + -1*A + -1*J >= 0 && J >= 0 && -17 + A + J >= 0 && 17 + -1*A + J >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && M >= C1 && G >= 0 && 0 >= 1 + H && I >= 0 && P = 0 && J = 0] f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1 ,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1 ,G1) [-1 + B + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -17 + A + C >= 0 && 17 + -1*A + C >= 0 && -1 + B >= 0 && -18 + A + B >= 0 && 16 + -1*A + B >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && D1 >= G1 && C >= 2 && E1 >= 1 && B1 >= 1 && B >= A && D >= 1] 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1 ,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1 ,G1) [-1 + B + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -17 + A + C >= 0 && 17 + -1*A + C >= 0 && -1 + B >= 0 && -18 + A + B >= 0 && 16 + -1*A + B >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && D1 >= G1 && C >= 2 && E1 >= 1 && B1 >= 1 && B >= A && 0 >= 1 + D] 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1 ,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1 ,G1) [-1 + B + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -17 + A + C >= 0 && 17 + -1*A + C >= 0 && -1 + B >= 0 && -18 + A + B >= 0 && 16 + -1*A + B >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && D1 >= G1 && C >= 2 && E1 >= 1 && 0 >= 1 + B1 && B >= A && D >= 1] 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1 ,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1 ,G1) [-1 + B + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -17 + A + C >= 0 && 17 + -1*A + C >= 0 && -1 + B >= 0 && -18 + A + B >= 0 && 16 + -1*A + B >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && D1 >= G1 && C >= 2 && E1 >= 1 && 0 >= 1 + B1 && B >= A && 0 >= 1 + D] 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1 ,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1 ,G1) [-1 + B + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -17 + A + C >= 0 && 17 + -1*A + C >= 0 && -1 + B >= 0 && -18 + A + B >= 0 && 16 + -1*A + B >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && D1 >= G1 && C >= 2 && 0 >= 1 + E1 && B1 >= 1 && B >= A && D >= 1] 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1 ,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1 ,G1) [-1 + B + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -17 + A + C >= 0 && 17 + -1*A + C >= 0 && -1 + B >= 0 && -18 + A + B >= 0 && 16 + -1*A + B >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && D1 >= G1 && C >= 2 && 0 >= 1 + E1 && B1 >= 1 && B >= A && 0 >= 1 + D] 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1 ,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1 ,G1) [-1 + B + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -17 + A + C >= 0 && 17 + -1*A + C >= 0 && -1 + B >= 0 && -18 + A + B >= 0 && 16 + -1*A + B >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && D1 >= G1 && C >= 2 && 0 >= 1 + E1 && 0 >= 1 + B1 && B >= A && D >= 1] 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1 ,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1 ,G1) [-1 + B + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -17 + A + C >= 0 && 17 + -1*A + C >= 0 && -1 + B >= 0 && -18 + A + B >= 0 && 16 + -1*A + B >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && D1 >= G1 && C >= 2 && 0 >= 1 + E1 && 0 >= 1 + B1 && B >= A && 0 >= 1 + D] f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f9(17,1,0,B1,B1,B1,G,H,I,J,K,L,M,N,O,P,E1,R,S ,T,U,V,W,X,Y,Z ,A1) True Signature: {(f0,27);(f12,27);(f5,27);(f6,27);(f9,27)} Rule Graph: [0->{0,9,10,11,12,13,14,15,16},1->{},2->{},3->{1,2,3,4,5,6,7,8},4->{1,2,3,4,5,6,7,8},5->{1,2,3,4,5,6,7,8} ,6->{1,2,3,4,5,6,7,8},7->{},8->{},9->{1,3,5,7},10->{1,3,5,7},11->{2,4,6,8},12->{2,4,6,8},13->{1,3,5,7} ,14->{1,3,5,7},15->{2,4,6,8},16->{2,4,6,8},17->{0}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17] | +- p:[0] c: [0] | `- p:[3,4,5,6] c: [6] | `- p:[3,4,5] c: [5] | `- p:[3,4] c: [4] | `- p:[3] c: [3]) + Applied Processor: CloseWith True + Details: () YES