YES * Step 1: TrivialSCCs YES + Considered Problem: Rules: 0. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,0,H1,W,X,Y,Z,A1,B1,D1,D1,-1 + E1,F1,0,H1,0,H1,-1 + E1,L1,M1 [-1*F + O >= 0 (?,1) ,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1) && -2 + F >= 0 && -4 + F + T1 >= 0 && F + -1*T1 >= 0 && -2 + F + P1 >= 0 && -1 + F + L1 >= 0 && -3 + F + -1*L1 >= 0 && -2 + F + J1 >= 0 && -2 + F + -1*J1 >= 0 && -2 + F + I1 >= 0 && -2 + F + -1*I1 >= 0 && -2 + F + H1 >= 0 && -2 + F + -1*H1 >= 0 && -2 + F + G1 >= 0 && -2 + F + -1*G1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -2 + C1 + F >= 0 && -2 + -1*C1 + F >= 0 && -4 + A1 + F >= 0 && -2 + F + V >= 0 && -2 + F + -1*V >= 0 && -2 + F + U >= 0 && -2 + F + -1*U >= 0 && -3 + F + P >= 0 && -1 + F + -1*P >= 0 && -4 + F + O >= 0 && F + -1*O >= 0 && -4 + A + F >= 0 && 2 + -1*T1 >= 0 && 2 + P1 + -1*T1 >= 0 && 3 + L1 + -1*T1 >= 0 && 1 + -1*L1 + -1*T1 >= 0 && 2 + J1 + -1*T1 >= 0 && 2 + -1*J1 + -1*T1 >= 0 && 2 + I1 + -1*T1 >= 0 && 2 + -1*I1 + -1*T1 >= 0 && 2 + H1 + -1*T1 >= 0 && 2 + -1*H1 + -1*T1 >= 0 && 2 + G1 + -1*T1 >= 0 && 2 + -1*G1 + -1*T1 >= 0 && 2 + D1 + -1*T1 >= 0 && 2 + -1*D1 + -1*T1 >= 0 && 2 + C1 + -1*T1 >= 0 && 2 + -1*C1 + -1*T1 >= 0 && A1 + -1*T1 >= 0 && 2 + -1*T1 + V >= 0 && 2 + -1*T1 + -1*V >= 0 && 2 + -1*T1 + U >= 0 && 2 + -1*T1 + -1*U >= 0 && 1 + P + -1*T1 >= 0 && 3 + -1*P + -1*T1 >= 0 && O + -1*T1 >= 0 && A + -1*T1 >= 0 && -2 + T1 >= 0 && -2 + P1 + T1 >= 0 && -1 + L1 + T1 >= 0 && -3 + -1*L1 + T1 >= 0 && -2 + J1 + T1 >= 0 && -2 + -1*J1 + T1 >= 0 && -2 + I1 + T1 >= 0 && -2 + -1*I1 + T1 >= 0 && -2 + H1 + T1 >= 0 && -2 + -1*H1 + T1 >= 0 && -2 + G1 + T1 >= 0 && -2 + -1*G1 + T1 >= 0 && -2 + D1 + T1 >= 0 && -2 + -1*D1 + T1 >= 0 && -2 + C1 + T1 >= 0 && -2 + -1*C1 + T1 >= 0 && -4 + A1 + T1 >= 0 && -2 + T1 + V >= 0 && -2 + T1 + -1*V >= 0 && -2 + T1 + U >= 0 && -2 + T1 + -1*U >= 0 && -3 + P + T1 >= 0 && -1 + -1*P + T1 >= 0 && -4 + O + T1 >= 0 && -4 + A + T1 >= 0 && P1 >= 0 && 1 + L1 + P1 >= 0 && -1 + -1*L1 + P1 >= 0 && J1 + P1 >= 0 && -1*J1 + P1 >= 0 && I1 + P1 >= 0 && -1*I1 + P1 >= 0 && H1 + P1 >= 0 && -1*H1 + P1 >= 0 && G1 + P1 >= 0 && -1*G1 + P1 >= 0 && D1 + P1 >= 0 && -1*D1 + P1 >= 0 && C1 + P1 >= 0 && -1*C1 + P1 >= 0 && -2 + A1 + P1 >= 0 && P1 + V >= 0 && P1 + -1*V >= 0 && P1 + U >= 0 && P1 + -1*U >= 0 && -1 + P + P1 >= 0 && 1 + -1*P + P1 >= 0 && -2 + O + P1 >= 0 && -2 + A + P1 >= 0 && -1 + -1*L1 >= 0 && -1 + J1 + -1*L1 >= 0 && -1 + -1*J1 + -1*L1 >= 0 && -1 + I1 + -1*L1 >= 0 && -1 + -1*I1 + -1*L1 >= 0 && -1 + H1 + -1*L1 >= 0 && -1 + -1*H1 + -1*L1 >= 0 && -1 + G1 + -1*L1 >= 0 && -1 + -1*G1 + -1*L1 >= 0 && -1 + D1 + -1*L1 >= 0 && -1 + -1*D1 + -1*L1 >= 0 && -1 + C1 + -1*L1 >= 0 && -1 + -1*C1 + -1*L1 >= 0 && -3 + A1 + -1*L1 >= 0 && -1 + -1*L1 + V >= 0 && -1 + -1*L1 + -1*V >= 0 && -1 + -1*L1 + U >= 0 && -1 + -1*L1 + -1*U >= 0 && -2 + -1*L1 + P >= 0 && -1*L1 + -1*P >= 0 && -3 + -1*L1 + O >= 0 && -3 + A + -1*L1 >= 0 && 1 + L1 >= 0 && 1 + J1 + L1 >= 0 && 1 + -1*J1 + L1 >= 0 && 1 + I1 + L1 >= 0 && 1 + -1*I1 + L1 >= 0 && 1 + H1 + L1 >= 0 && 1 + -1*H1 + L1 >= 0 && 1 + G1 + L1 >= 0 && 1 + -1*G1 + L1 >= 0 && 1 + D1 + L1 >= 0 && 1 + -1*D1 + L1 >= 0 && 1 + C1 + L1 >= 0 && 1 + -1*C1 + L1 >= 0 && -1 + A1 + L1 >= 0 && 1 + L1 + V >= 0 && 1 + L1 + -1*V >= 0 && 1 + L1 + U >= 0 && 1 + L1 + -1*U >= 0 && L1 + P >= 0 && 2 + L1 + -1*P >= 0 && -1 + L1 + O >= 0 && -1 + A + L1 >= 0 && -1*J1 >= 0 && I1 + -1*J1 >= 0 && -1*I1 + -1*J1 >= 0 && H1 + -1*J1 >= 0 && -1*H1 + -1*J1 >= 0 && G1 + -1*J1 >= 0 && -1*G1 + -1*J1 >= 0 && D1 + -1*J1 >= 0 && -1*D1 + -1*J1 >= 0 && C1 + -1*J1 >= 0 && -1*C1 + -1*J1 >= 0 && -2 + A1 + -1*J1 >= 0 && -1*J1 + V >= 0 && -1*J1 + -1*V >= 0 && -1*J1 + U >= 0 && -1*J1 + -1*U >= 0 && -1 + -1*J1 + P >= 0 && 1 + -1*J1 + -1*P >= 0 && -2 + -1*J1 + O >= 0 && -2 + A + -1*J1 >= 0 && J1 >= 0 && I1 + J1 >= 0 && -1*I1 + J1 >= 0 && H1 + J1 >= 0 && -1*H1 + J1 >= 0 && G1 + J1 >= 0 && -1*G1 + J1 >= 0 && D1 + J1 >= 0 && -1*D1 + J1 >= 0 && C1 + J1 >= 0 && -1*C1 + J1 >= 0 && -2 + A1 + J1 >= 0 && J1 + V >= 0 && J1 + -1*V >= 0 && J1 + U >= 0 && J1 + -1*U >= 0 && -1 + J1 + P >= 0 && 1 + J1 + -1*P >= 0 && -2 + J1 + O >= 0 && -2 + A + J1 >= 0 && -1*I1 >= 0 && H1 + -1*I1 >= 0 && -1*H1 + -1*I1 >= 0 && G1 + -1*I1 >= 0 && -1*G1 + -1*I1 >= 0 && D1 + -1*I1 >= 0 && -1*D1 + -1*I1 >= 0 && C1 + -1*I1 >= 0 && -1*C1 + -1*I1 >= 0 && -2 + A1 + -1*I1 >= 0 && -1*I1 + V >= 0 && -1*I1 + -1*V >= 0 && -1*I1 + U >= 0 && -1*I1 + -1*U >= 0 && -1 + -1*I1 + P >= 0 && 1 + -1*I1 + -1*P >= 0 && -2 + -1*I1 + O >= 0 && -2 + A + -1*I1 >= 0 && I1 >= 0 && H1 + I1 >= 0 && -1*H1 + I1 >= 0 && G1 + I1 >= 0 && -1*G1 + I1 >= 0 && D1 + I1 >= 0 && -1*D1 + I1 >= 0 && C1 + I1 >= 0 && -1*C1 + I1 >= 0 && -2 + A1 + I1 >= 0 && I1 + V >= 0 && I1 + -1*V >= 0 && I1 + U >= 0 && I1 + -1*U >= 0 && -1 + I1 + P >= 0 && 1 + I1 + -1*P >= 0 && -2 + I1 + O >= 0 && -2 + A + I1 >= 0 && -1*H1 >= 0 && G1 + -1*H1 >= 0 && -1*G1 + -1*H1 >= 0 && D1 + -1*H1 >= 0 && -1*D1 + -1*H1 >= 0 && C1 + -1*H1 >= 0 && -1*C1 + -1*H1 >= 0 && -2 + A1 + -1*H1 >= 0 && -1*H1 + V >= 0 && -1*H1 + -1*V >= 0 && -1*H1 + U >= 0 && -1*H1 + -1*U >= 0 && -1 + -1*H1 + P >= 0 && 1 + -1*H1 + -1*P >= 0 && -2 + -1*H1 + O >= 0 && -2 + A + -1*H1 >= 0 && H1 >= 0 && G1 + H1 >= 0 && -1*G1 + H1 >= 0 && D1 + H1 >= 0 && -1*D1 + H1 >= 0 && C1 + H1 >= 0 && -1*C1 + H1 >= 0 && -2 + A1 + H1 >= 0 && H1 + V >= 0 && H1 + -1*V >= 0 && H1 + U >= 0 && H1 + -1*U >= 0 && -1 + H1 + P >= 0 && 1 + H1 + -1*P >= 0 && -2 + H1 + O >= 0 && -2 + A + H1 >= 0 && -1*G1 >= 0 && D1 + -1*G1 >= 0 && -1*D1 + -1*G1 >= 0 && C1 + -1*G1 >= 0 && -1*C1 + -1*G1 >= 0 && -2 + A1 + -1*G1 >= 0 && -1*G1 + V >= 0 && -1*G1 + -1*V >= 0 && -1*G1 + U >= 0 && -1*G1 + -1*U >= 0 && -1 + -1*G1 + P >= 0 && 1 + -1*G1 + -1*P >= 0 && -2 + -1*G1 + O >= 0 && -2 + A + -1*G1 >= 0 && G1 >= 0 && D1 + G1 >= 0 && -1*D1 + G1 >= 0 && C1 + G1 >= 0 && -1*C1 + G1 >= 0 && -2 + A1 + G1 >= 0 && G1 + V >= 0 && G1 + -1*V >= 0 && G1 + U >= 0 && G1 + -1*U >= 0 && -1 + G1 + P >= 0 && 1 + G1 + -1*P >= 0 && -2 + G1 + O >= 0 && -2 + A + G1 >= 0 && -1 + C + -1*E1 >= 0 && B1 + -1*E1 >= 0 && -1*D1 >= 0 && C1 + -1*D1 >= 0 && -1*C1 + -1*D1 >= 0 && -2 + A1 + -1*D1 >= 0 && -1*D1 + V >= 0 && -1*D1 + -1*V >= 0 && -1*D1 + U >= 0 && -1*D1 + -1*U >= 0 && -1 + -1*D1 + P >= 0 && 1 + -1*D1 + -1*P >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && C1 + D1 >= 0 && -1*C1 + D1 >= 0 && -2 + A1 + D1 >= 0 && D1 + V >= 0 && D1 + -1*V >= 0 && D1 + U >= 0 && D1 + -1*U >= 0 && -1 + D1 + P >= 0 && 1 + D1 + -1*P >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && 1 + B1 + -1*C >= 0 && -1 + -1*B1 + C >= 0 && -1*C1 >= 0 && -2 + A1 + -1*C1 >= 0 && -1*C1 + V >= 0 && -1*C1 + -1*V >= 0 && -1*C1 + U >= 0 && -1*C1 + -1*U >= 0 && -1 + -1*C1 + P >= 0 && 1 + -1*C1 + -1*P >= 0 && -2 + -1*C1 + O >= 0 && -2 + A + -1*C1 >= 0 && C1 >= 0 && -2 + A1 + C1 >= 0 && C1 + V >= 0 && C1 + -1*V >= 0 && C1 + U >= 0 && C1 + -1*U >= 0 && -1 + C1 + P >= 0 && 1 + C1 + -1*P >= 0 && -2 + C1 + O >= 0 && -2 + A + C1 >= 0 && -2 + A1 >= 0 && -2 + A1 + V >= 0 && -2 + A1 + -1*V >= 0 && -2 + A1 + U >= 0 && -2 + A1 + -1*U >= 0 && -3 + A1 + P >= 0 && -1 + A1 + -1*P >= 0 && -4 + A1 + O >= 0 && -4 + A + A1 >= 0 && -1*A + A1 >= 0 && -1*V >= 0 && U + -1*V >= 0 && -1*U + -1*V >= 0 && -1 + P + -1*V >= 0 && 1 + -1*P + -1*V >= 0 && -2 + O + -1*V >= 0 && -2 + A + -1*V >= 0 && V >= 0 && U + V >= 0 && -1*U + V >= 0 && -1 + P + V >= 0 && 1 + -1*P + V >= 0 && -2 + O + V >= 0 && -2 + A + V >= 0 && -1*U >= 0 && -1 + P + -1*U >= 0 && 1 + -1*P + -1*U >= 0 && -2 + O + -1*U >= 0 && -2 + A + -1*U >= 0 && U >= 0 && -1 + P + U >= 0 && 1 + -1*P + U >= 0 && -2 + O + U >= 0 && -2 + A + U >= 0 && 1 + -1*P >= 0 && -1 + O + -1*P >= 0 && -1 + A + -1*P >= 0 && -1 + P >= 0 && -3 + O + P >= 0 && -3 + A + P >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && E1 >= 0 && A >= 2 && I1 = 0 && H1 = V && G1 = 0 && U = 0 && J1 = V] 1. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(E2,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,F2,Z,A1,B1,G2,D2,E1,F1,B2,Z1,A2,Y1,K1,L1,M1,N1,O1 [-1*F + O >= 0 (?,1) ,S1,T1,U1,V1,W1,X1) ,P1,Q1,R1,S1,T1,U1,V1,W1,X1) && -2 + F >= 0 && -4 + F + T1 >= 0 && F + -1*T1 >= 0 && -2 + F + P1 >= 0 && -1 + F + L1 >= 0 && -3 + F + -1*L1 >= 0 && -2 + F + J1 >= 0 && -2 + F + -1*J1 >= 0 && -2 + F + I1 >= 0 && -2 + F + -1*I1 >= 0 && -2 + F + H1 >= 0 && -2 + F + -1*H1 >= 0 && -2 + F + G1 >= 0 && -2 + F + -1*G1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -2 + C1 + F >= 0 && -2 + -1*C1 + F >= 0 && -4 + A1 + F >= 0 && -2 + F + V >= 0 && -2 + F + -1*V >= 0 && -2 + F + U >= 0 && -2 + F + -1*U >= 0 && -3 + F + P >= 0 && -1 + F + -1*P >= 0 && -4 + F + O >= 0 && F + -1*O >= 0 && -4 + A + F >= 0 && 2 + -1*T1 >= 0 && 2 + P1 + -1*T1 >= 0 && 3 + L1 + -1*T1 >= 0 && 1 + -1*L1 + -1*T1 >= 0 && 2 + J1 + -1*T1 >= 0 && 2 + -1*J1 + -1*T1 >= 0 && 2 + I1 + -1*T1 >= 0 && 2 + -1*I1 + -1*T1 >= 0 && 2 + H1 + -1*T1 >= 0 && 2 + -1*H1 + -1*T1 >= 0 && 2 + G1 + -1*T1 >= 0 && 2 + -1*G1 + -1*T1 >= 0 && 2 + D1 + -1*T1 >= 0 && 2 + -1*D1 + -1*T1 >= 0 && 2 + C1 + -1*T1 >= 0 && 2 + -1*C1 + -1*T1 >= 0 && A1 + -1*T1 >= 0 && 2 + -1*T1 + V >= 0 && 2 + -1*T1 + -1*V >= 0 && 2 + -1*T1 + U >= 0 && 2 + -1*T1 + -1*U >= 0 && 1 + P + -1*T1 >= 0 && 3 + -1*P + -1*T1 >= 0 && O + -1*T1 >= 0 && A + -1*T1 >= 0 && -2 + T1 >= 0 && -2 + P1 + T1 >= 0 && -1 + L1 + T1 >= 0 && -3 + -1*L1 + T1 >= 0 && -2 + J1 + T1 >= 0 && -2 + -1*J1 + T1 >= 0 && -2 + I1 + T1 >= 0 && -2 + -1*I1 + T1 >= 0 && -2 + H1 + T1 >= 0 && -2 + -1*H1 + T1 >= 0 && -2 + G1 + T1 >= 0 && -2 + -1*G1 + T1 >= 0 && -2 + D1 + T1 >= 0 && -2 + -1*D1 + T1 >= 0 && -2 + C1 + T1 >= 0 && -2 + -1*C1 + T1 >= 0 && -4 + A1 + T1 >= 0 && -2 + T1 + V >= 0 && -2 + T1 + -1*V >= 0 && -2 + T1 + U >= 0 && -2 + T1 + -1*U >= 0 && -3 + P + T1 >= 0 && -1 + -1*P + T1 >= 0 && -4 + O + T1 >= 0 && -4 + A + T1 >= 0 && P1 >= 0 && 1 + L1 + P1 >= 0 && -1 + -1*L1 + P1 >= 0 && J1 + P1 >= 0 && -1*J1 + P1 >= 0 && I1 + P1 >= 0 && -1*I1 + P1 >= 0 && H1 + P1 >= 0 && -1*H1 + P1 >= 0 && G1 + P1 >= 0 && -1*G1 + P1 >= 0 && D1 + P1 >= 0 && -1*D1 + P1 >= 0 && C1 + P1 >= 0 && -1*C1 + P1 >= 0 && -2 + A1 + P1 >= 0 && P1 + V >= 0 && P1 + -1*V >= 0 && P1 + U >= 0 && P1 + -1*U >= 0 && -1 + P + P1 >= 0 && 1 + -1*P + P1 >= 0 && -2 + O + P1 >= 0 && -2 + A + P1 >= 0 && -1 + -1*L1 >= 0 && -1 + J1 + -1*L1 >= 0 && -1 + -1*J1 + -1*L1 >= 0 && -1 + I1 + -1*L1 >= 0 && -1 + -1*I1 + -1*L1 >= 0 && -1 + H1 + -1*L1 >= 0 && -1 + -1*H1 + -1*L1 >= 0 && -1 + G1 + -1*L1 >= 0 && -1 + -1*G1 + -1*L1 >= 0 && -1 + D1 + -1*L1 >= 0 && -1 + -1*D1 + -1*L1 >= 0 && -1 + C1 + -1*L1 >= 0 && -1 + -1*C1 + -1*L1 >= 0 && -3 + A1 + -1*L1 >= 0 && -1 + -1*L1 + V >= 0 && -1 + -1*L1 + -1*V >= 0 && -1 + -1*L1 + U >= 0 && -1 + -1*L1 + -1*U >= 0 && -2 + -1*L1 + P >= 0 && -1*L1 + -1*P >= 0 && -3 + -1*L1 + O >= 0 && -3 + A + -1*L1 >= 0 && 1 + L1 >= 0 && 1 + J1 + L1 >= 0 && 1 + -1*J1 + L1 >= 0 && 1 + I1 + L1 >= 0 && 1 + -1*I1 + L1 >= 0 && 1 + H1 + L1 >= 0 && 1 + -1*H1 + L1 >= 0 && 1 + G1 + L1 >= 0 && 1 + -1*G1 + L1 >= 0 && 1 + D1 + L1 >= 0 && 1 + -1*D1 + L1 >= 0 && 1 + C1 + L1 >= 0 && 1 + -1*C1 + L1 >= 0 && -1 + A1 + L1 >= 0 && 1 + L1 + V >= 0 && 1 + L1 + -1*V >= 0 && 1 + L1 + U >= 0 && 1 + L1 + -1*U >= 0 && L1 + P >= 0 && 2 + L1 + -1*P >= 0 && -1 + L1 + O >= 0 && -1 + A + L1 >= 0 && -1*J1 >= 0 && I1 + -1*J1 >= 0 && -1*I1 + -1*J1 >= 0 && H1 + -1*J1 >= 0 && -1*H1 + -1*J1 >= 0 && G1 + -1*J1 >= 0 && -1*G1 + -1*J1 >= 0 && D1 + -1*J1 >= 0 && -1*D1 + -1*J1 >= 0 && C1 + -1*J1 >= 0 && -1*C1 + -1*J1 >= 0 && -2 + A1 + -1*J1 >= 0 && -1*J1 + V >= 0 && -1*J1 + -1*V >= 0 && -1*J1 + U >= 0 && -1*J1 + -1*U >= 0 && -1 + -1*J1 + P >= 0 && 1 + -1*J1 + -1*P >= 0 && -2 + -1*J1 + O >= 0 && -2 + A + -1*J1 >= 0 && J1 >= 0 && I1 + J1 >= 0 && -1*I1 + J1 >= 0 && H1 + J1 >= 0 && -1*H1 + J1 >= 0 && G1 + J1 >= 0 && -1*G1 + J1 >= 0 && D1 + J1 >= 0 && -1*D1 + J1 >= 0 && C1 + J1 >= 0 && -1*C1 + J1 >= 0 && -2 + A1 + J1 >= 0 && J1 + V >= 0 && J1 + -1*V >= 0 && J1 + U >= 0 && J1 + -1*U >= 0 && -1 + J1 + P >= 0 && 1 + J1 + -1*P >= 0 && -2 + J1 + O >= 0 && -2 + A + J1 >= 0 && -1*I1 >= 0 && H1 + -1*I1 >= 0 && -1*H1 + -1*I1 >= 0 && G1 + -1*I1 >= 0 && -1*G1 + -1*I1 >= 0 && D1 + -1*I1 >= 0 && -1*D1 + -1*I1 >= 0 && C1 + -1*I1 >= 0 && -1*C1 + -1*I1 >= 0 && -2 + A1 + -1*I1 >= 0 && -1*I1 + V >= 0 && -1*I1 + -1*V >= 0 && -1*I1 + U >= 0 && -1*I1 + -1*U >= 0 && -1 + -1*I1 + P >= 0 && 1 + -1*I1 + -1*P >= 0 && -2 + -1*I1 + O >= 0 && -2 + A + -1*I1 >= 0 && I1 >= 0 && H1 + I1 >= 0 && -1*H1 + I1 >= 0 && G1 + I1 >= 0 && -1*G1 + I1 >= 0 && D1 + I1 >= 0 && -1*D1 + I1 >= 0 && C1 + I1 >= 0 && -1*C1 + I1 >= 0 && -2 + A1 + I1 >= 0 && I1 + V >= 0 && I1 + -1*V >= 0 && I1 + U >= 0 && I1 + -1*U >= 0 && -1 + I1 + P >= 0 && 1 + I1 + -1*P >= 0 && -2 + I1 + O >= 0 && -2 + A + I1 >= 0 && -1*H1 >= 0 && G1 + -1*H1 >= 0 && -1*G1 + -1*H1 >= 0 && D1 + -1*H1 >= 0 && -1*D1 + -1*H1 >= 0 && C1 + -1*H1 >= 0 && -1*C1 + -1*H1 >= 0 && -2 + A1 + -1*H1 >= 0 && -1*H1 + V >= 0 && -1*H1 + -1*V >= 0 && -1*H1 + U >= 0 && -1*H1 + -1*U >= 0 && -1 + -1*H1 + P >= 0 && 1 + -1*H1 + -1*P >= 0 && -2 + -1*H1 + O >= 0 && -2 + A + -1*H1 >= 0 && H1 >= 0 && G1 + H1 >= 0 && -1*G1 + H1 >= 0 && D1 + H1 >= 0 && -1*D1 + H1 >= 0 && C1 + H1 >= 0 && -1*C1 + H1 >= 0 && -2 + A1 + H1 >= 0 && H1 + V >= 0 && H1 + -1*V >= 0 && H1 + U >= 0 && H1 + -1*U >= 0 && -1 + H1 + P >= 0 && 1 + H1 + -1*P >= 0 && -2 + H1 + O >= 0 && -2 + A + H1 >= 0 && -1*G1 >= 0 && D1 + -1*G1 >= 0 && -1*D1 + -1*G1 >= 0 && C1 + -1*G1 >= 0 && -1*C1 + -1*G1 >= 0 && -2 + A1 + -1*G1 >= 0 && -1*G1 + V >= 0 && -1*G1 + -1*V >= 0 && -1*G1 + U >= 0 && -1*G1 + -1*U >= 0 && -1 + -1*G1 + P >= 0 && 1 + -1*G1 + -1*P >= 0 && -2 + -1*G1 + O >= 0 && -2 + A + -1*G1 >= 0 && G1 >= 0 && D1 + G1 >= 0 && -1*D1 + G1 >= 0 && C1 + G1 >= 0 && -1*C1 + G1 >= 0 && -2 + A1 + G1 >= 0 && G1 + V >= 0 && G1 + -1*V >= 0 && G1 + U >= 0 && G1 + -1*U >= 0 && -1 + G1 + P >= 0 && 1 + G1 + -1*P >= 0 && -2 + G1 + O >= 0 && -2 + A + G1 >= 0 && -1 + C + -1*E1 >= 0 && B1 + -1*E1 >= 0 && -1*D1 >= 0 && C1 + -1*D1 >= 0 && -1*C1 + -1*D1 >= 0 && -2 + A1 + -1*D1 >= 0 && -1*D1 + V >= 0 && -1*D1 + -1*V >= 0 && -1*D1 + U >= 0 && -1*D1 + -1*U >= 0 && -1 + -1*D1 + P >= 0 && 1 + -1*D1 + -1*P >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && C1 + D1 >= 0 && -1*C1 + D1 >= 0 && -2 + A1 + D1 >= 0 && D1 + V >= 0 && D1 + -1*V >= 0 && D1 + U >= 0 && D1 + -1*U >= 0 && -1 + D1 + P >= 0 && 1 + D1 + -1*P >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && 1 + B1 + -1*C >= 0 && -1 + -1*B1 + C >= 0 && -1*C1 >= 0 && -2 + A1 + -1*C1 >= 0 && -1*C1 + V >= 0 && -1*C1 + -1*V >= 0 && -1*C1 + U >= 0 && -1*C1 + -1*U >= 0 && -1 + -1*C1 + P >= 0 && 1 + -1*C1 + -1*P >= 0 && -2 + -1*C1 + O >= 0 && -2 + A + -1*C1 >= 0 && C1 >= 0 && -2 + A1 + C1 >= 0 && C1 + V >= 0 && C1 + -1*V >= 0 && C1 + U >= 0 && C1 + -1*U >= 0 && -1 + C1 + P >= 0 && 1 + C1 + -1*P >= 0 && -2 + C1 + O >= 0 && -2 + A + C1 >= 0 && -2 + A1 >= 0 && -2 + A1 + V >= 0 && -2 + A1 + -1*V >= 0 && -2 + A1 + U >= 0 && -2 + A1 + -1*U >= 0 && -3 + A1 + P >= 0 && -1 + A1 + -1*P >= 0 && -4 + A1 + O >= 0 && -4 + A + A1 >= 0 && -1*A + A1 >= 0 && -1*V >= 0 && U + -1*V >= 0 && -1*U + -1*V >= 0 && -1 + P + -1*V >= 0 && 1 + -1*P + -1*V >= 0 && -2 + O + -1*V >= 0 && -2 + A + -1*V >= 0 && V >= 0 && U + V >= 0 && -1*U + V >= 0 && -1 + P + V >= 0 && 1 + -1*P + V >= 0 && -2 + O + V >= 0 && -2 + A + V >= 0 && -1*U >= 0 && -1 + P + -1*U >= 0 && 1 + -1*P + -1*U >= 0 && -2 + O + -1*U >= 0 && -2 + A + -1*U >= 0 && U >= 0 && -1 + P + U >= 0 && 1 + -1*P + U >= 0 && -2 + O + U >= 0 && -2 + A + U >= 0 && 1 + -1*P >= 0 && -1 + O + -1*P >= 0 && -1 + A + -1*P >= 0 && -1 + P >= 0 && -3 + O + P >= 0 && -3 + A + P >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && E1 >= 0 && G1 = D1] 2. f116(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f116(A,B,1 + C,D,E,-1 + F,G,H,I,J,K,L,M,N,F,1,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,U [-2 + C + F >= 0 (?,1) ,R1,S1,T1,U1,V1,W1,X1) ,1 + C,-1 + F,P1,Q1,R1,S1,T1,U1,V1,W1,X1) && -2 + F + P >= 0 && 2 + -1*T1 >= 0 && 2 + C + -1*T1 >= 0 && A1 + -1*T1 >= 0 && 2 + P + -1*T1 >= 0 && A + -1*T1 >= 0 && -2 + T1 >= 0 && -2 + C + T1 >= 0 && -4 + A1 + T1 >= 0 && -2 + P + T1 >= 0 && -4 + A + T1 >= 0 && -1*C + P >= 0 && C >= 0 && -2 + A1 + C >= 0 && C + P >= 0 && C + -1*P >= 0 && -2 + A + C >= 0 && -2 + A1 >= 0 && -2 + A1 + P >= 0 && -4 + A + A1 >= 0 && -1*A + A1 >= 0 && U + -1*V >= 0 && -1*U + V >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && A >= 2 && F >= 0 && P = 0 && U = M1] 3. f116(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f8(A,B,1 + E1,D,E,F,G,H,I,J,K,L,M,N,F,1,Q,R,S,T,0,V,W,X,Y,Z,A1,E1,V,V,E1,F1,0,V,0,V,K1,-1,M1,N1,O1,Z1,Q1[-2 + C + F >= 0 (?,1) ,R1,S1,T1,U1,V1,W1,X1) ,R1,S1,T1,U1,V1,W1,X1) && -2 + F + P >= 0 && 2 + -1*T1 >= 0 && 2 + C + -1*T1 >= 0 && A1 + -1*T1 >= 0 && 2 + P + -1*T1 >= 0 && A + -1*T1 >= 0 && -2 + T1 >= 0 && -2 + C + T1 >= 0 && -4 + A1 + T1 >= 0 && -2 + P + T1 >= 0 && -4 + A + T1 >= 0 && -1*C + P >= 0 && C >= 0 && -2 + A1 + C >= 0 && C + P >= 0 && C + -1*P >= 0 && -2 + A + C >= 0 && -2 + A1 >= 0 && -2 + A1 + P >= 0 && -4 + A + A1 >= 0 && -1*A + A1 >= 0 && U + -1*V >= 0 && -1*U + V >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && Z1 >= 0 && A >= 2 && F >= 0 && U = 0 && P = 0] 4. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f1(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,S,Z1,S,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1[2 + -1*T1 >= 0 (?,1) ,S1,T1,U1,V1,W1,X1) ,P1,Q1,R1,S1,T1,U1,V1,W1,X1) && B + -1*T1 >= 0 && Q + -1*T1 >= 0 && 2 + P + -1*T1 >= 0 && 2 + -1*P + -1*T1 >= 0 && -2 + T1 >= 0 && -4 + B + T1 >= 0 && -4 + Q + T1 >= 0 && -2 + P + T1 >= 0 && -2 + -1*P + T1 >= 0 && R + -1*T >= 0 && -1*R + T >= 0 && -1*B + Q >= 0 && -2 + B >= 0 && -4 + B + Q >= 0 && -2 + B + P >= 0 && -2 + B + -1*P >= 0 && -2 + Q >= 0 && -2 + P + Q >= 0 && -2 + -1*P + Q >= 0 && -1*P >= 0 && P >= 0 && B >= 0 && Q >= 1 + B] 5. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f116(A,Z1,0,D,E,F,G,H,I,J,K,L,M,N,O,P,A2,Y1,D2,B2,R,R,E2,F2,G2,Z1,C2,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1[2 + -1*T1 >= 0 (?,1) ,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1) && B + -1*T1 >= 0 && Q + -1*T1 >= 0 && 2 + P + -1*T1 >= 0 && 2 + -1*P + -1*T1 >= 0 && -2 + T1 >= 0 && -4 + B + T1 >= 0 && -4 + Q + T1 >= 0 && -2 + P + T1 >= 0 && -2 + -1*P + T1 >= 0 && R + -1*T >= 0 && -1*R + T >= 0 && -1*B + Q >= 0 && -2 + B >= 0 && -4 + B + Q >= 0 && -2 + B + P >= 0 && -2 + B + -1*P >= 0 && -2 + Q >= 0 && -2 + P + Q >= 0 && -2 + -1*P + Q >= 0 && -1*P >= 0 && P >= 0 && A >= 2 && C2 >= A && F >= A && B >= Q && B >= 0 && C = 0] 6. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f1(Z1,2,C,D,E,F,G,H,I,J,K,L,M,N,O,0,Z1,S,B2,S,U,V,S,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1 [Z1 >= 2 && S = W] (1,1) ,S1,T1,U1,V1,W1,X1) ,P1,A2,Y1,D2,2,E2,V1,W1,X1) 7. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(F2,E2,C,D,E,F,G,H,I,J,K,L,M,N,O,0,C2,H2,J2,I2,0,0,K2,L2,M2,Z,A1,B1,N2,D2,E1,F1,B2,Z1,A2,Y1,K1,L1,M1 [0 >= F2] (1,1) ,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,Q1,G2,S1,T1,U1,V1,W1,X1) 8. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(1,E2,C,D,E,F,G,H,I,J,K,L,M,N,O,0,H2,I2,K2,J2,0,0,M2,N2,O2,Z,A1,B1,Q2,D2,E1,F1,B2,Z1,A2,Y1,K1,L1,M1 [S = 0 && W = 0] (1,1) ,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,G2,C2,L2,T1,U1,F2,G2,P2) Signature: {(f1,50);(f10,50);(f116,50);(f8,50);(f9,50)} Flow Graph: [0->{0,1},1->{},2->{2,3},3->{0,1},4->{4,5},5->{2,3},6->{4,5},7->{},8->{}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatPaths YES + Considered Problem: Rules: 0. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,0,H1,W,X,Y,Z,A1,B1,D1,D1,-1 + E1,F1,0,H1,0,H1,-1 + E1,L1,M1 [-1*F + O >= 0 (?,1) ,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1) && -2 + F >= 0 && -4 + F + T1 >= 0 && F + -1*T1 >= 0 && -2 + F + P1 >= 0 && -1 + F + L1 >= 0 && -3 + F + -1*L1 >= 0 && -2 + F + J1 >= 0 && -2 + F + -1*J1 >= 0 && -2 + F + I1 >= 0 && -2 + F + -1*I1 >= 0 && -2 + F + H1 >= 0 && -2 + F + -1*H1 >= 0 && -2 + F + G1 >= 0 && -2 + F + -1*G1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -2 + C1 + F >= 0 && -2 + -1*C1 + F >= 0 && -4 + A1 + F >= 0 && -2 + F + V >= 0 && -2 + F + -1*V >= 0 && -2 + F + U >= 0 && -2 + F + -1*U >= 0 && -3 + F + P >= 0 && -1 + F + -1*P >= 0 && -4 + F + O >= 0 && F + -1*O >= 0 && -4 + A + F >= 0 && 2 + -1*T1 >= 0 && 2 + P1 + -1*T1 >= 0 && 3 + L1 + -1*T1 >= 0 && 1 + -1*L1 + -1*T1 >= 0 && 2 + J1 + -1*T1 >= 0 && 2 + -1*J1 + -1*T1 >= 0 && 2 + I1 + -1*T1 >= 0 && 2 + -1*I1 + -1*T1 >= 0 && 2 + H1 + -1*T1 >= 0 && 2 + -1*H1 + -1*T1 >= 0 && 2 + G1 + -1*T1 >= 0 && 2 + -1*G1 + -1*T1 >= 0 && 2 + D1 + -1*T1 >= 0 && 2 + -1*D1 + -1*T1 >= 0 && 2 + C1 + -1*T1 >= 0 && 2 + -1*C1 + -1*T1 >= 0 && A1 + -1*T1 >= 0 && 2 + -1*T1 + V >= 0 && 2 + -1*T1 + -1*V >= 0 && 2 + -1*T1 + U >= 0 && 2 + -1*T1 + -1*U >= 0 && 1 + P + -1*T1 >= 0 && 3 + -1*P + -1*T1 >= 0 && O + -1*T1 >= 0 && A + -1*T1 >= 0 && -2 + T1 >= 0 && -2 + P1 + T1 >= 0 && -1 + L1 + T1 >= 0 && -3 + -1*L1 + T1 >= 0 && -2 + J1 + T1 >= 0 && -2 + -1*J1 + T1 >= 0 && -2 + I1 + T1 >= 0 && -2 + -1*I1 + T1 >= 0 && -2 + H1 + T1 >= 0 && -2 + -1*H1 + T1 >= 0 && -2 + G1 + T1 >= 0 && -2 + -1*G1 + T1 >= 0 && -2 + D1 + T1 >= 0 && -2 + -1*D1 + T1 >= 0 && -2 + C1 + T1 >= 0 && -2 + -1*C1 + T1 >= 0 && -4 + A1 + T1 >= 0 && -2 + T1 + V >= 0 && -2 + T1 + -1*V >= 0 && -2 + T1 + U >= 0 && -2 + T1 + -1*U >= 0 && -3 + P + T1 >= 0 && -1 + -1*P + T1 >= 0 && -4 + O + T1 >= 0 && -4 + A + T1 >= 0 && P1 >= 0 && 1 + L1 + P1 >= 0 && -1 + -1*L1 + P1 >= 0 && J1 + P1 >= 0 && -1*J1 + P1 >= 0 && I1 + P1 >= 0 && -1*I1 + P1 >= 0 && H1 + P1 >= 0 && -1*H1 + P1 >= 0 && G1 + P1 >= 0 && -1*G1 + P1 >= 0 && D1 + P1 >= 0 && -1*D1 + P1 >= 0 && C1 + P1 >= 0 && -1*C1 + P1 >= 0 && -2 + A1 + P1 >= 0 && P1 + V >= 0 && P1 + -1*V >= 0 && P1 + U >= 0 && P1 + -1*U >= 0 && -1 + P + P1 >= 0 && 1 + -1*P + P1 >= 0 && -2 + O + P1 >= 0 && -2 + A + P1 >= 0 && -1 + -1*L1 >= 0 && -1 + J1 + -1*L1 >= 0 && -1 + -1*J1 + -1*L1 >= 0 && -1 + I1 + -1*L1 >= 0 && -1 + -1*I1 + -1*L1 >= 0 && -1 + H1 + -1*L1 >= 0 && -1 + -1*H1 + -1*L1 >= 0 && -1 + G1 + -1*L1 >= 0 && -1 + -1*G1 + -1*L1 >= 0 && -1 + D1 + -1*L1 >= 0 && -1 + -1*D1 + -1*L1 >= 0 && -1 + C1 + -1*L1 >= 0 && -1 + -1*C1 + -1*L1 >= 0 && -3 + A1 + -1*L1 >= 0 && -1 + -1*L1 + V >= 0 && -1 + -1*L1 + -1*V >= 0 && -1 + -1*L1 + U >= 0 && -1 + -1*L1 + -1*U >= 0 && -2 + -1*L1 + P >= 0 && -1*L1 + -1*P >= 0 && -3 + -1*L1 + O >= 0 && -3 + A + -1*L1 >= 0 && 1 + L1 >= 0 && 1 + J1 + L1 >= 0 && 1 + -1*J1 + L1 >= 0 && 1 + I1 + L1 >= 0 && 1 + -1*I1 + L1 >= 0 && 1 + H1 + L1 >= 0 && 1 + -1*H1 + L1 >= 0 && 1 + G1 + L1 >= 0 && 1 + -1*G1 + L1 >= 0 && 1 + D1 + L1 >= 0 && 1 + -1*D1 + L1 >= 0 && 1 + C1 + L1 >= 0 && 1 + -1*C1 + L1 >= 0 && -1 + A1 + L1 >= 0 && 1 + L1 + V >= 0 && 1 + L1 + -1*V >= 0 && 1 + L1 + U >= 0 && 1 + L1 + -1*U >= 0 && L1 + P >= 0 && 2 + L1 + -1*P >= 0 && -1 + L1 + O >= 0 && -1 + A + L1 >= 0 && -1*J1 >= 0 && I1 + -1*J1 >= 0 && -1*I1 + -1*J1 >= 0 && H1 + -1*J1 >= 0 && -1*H1 + -1*J1 >= 0 && G1 + -1*J1 >= 0 && -1*G1 + -1*J1 >= 0 && D1 + -1*J1 >= 0 && -1*D1 + -1*J1 >= 0 && C1 + -1*J1 >= 0 && -1*C1 + -1*J1 >= 0 && -2 + A1 + -1*J1 >= 0 && -1*J1 + V >= 0 && -1*J1 + -1*V >= 0 && -1*J1 + U >= 0 && -1*J1 + -1*U >= 0 && -1 + -1*J1 + P >= 0 && 1 + -1*J1 + -1*P >= 0 && -2 + -1*J1 + O >= 0 && -2 + A + -1*J1 >= 0 && J1 >= 0 && I1 + J1 >= 0 && -1*I1 + J1 >= 0 && H1 + J1 >= 0 && -1*H1 + J1 >= 0 && G1 + J1 >= 0 && -1*G1 + J1 >= 0 && D1 + J1 >= 0 && -1*D1 + J1 >= 0 && C1 + J1 >= 0 && -1*C1 + J1 >= 0 && -2 + A1 + J1 >= 0 && J1 + V >= 0 && J1 + -1*V >= 0 && J1 + U >= 0 && J1 + -1*U >= 0 && -1 + J1 + P >= 0 && 1 + J1 + -1*P >= 0 && -2 + J1 + O >= 0 && -2 + A + J1 >= 0 && -1*I1 >= 0 && H1 + -1*I1 >= 0 && -1*H1 + -1*I1 >= 0 && G1 + -1*I1 >= 0 && -1*G1 + -1*I1 >= 0 && D1 + -1*I1 >= 0 && -1*D1 + -1*I1 >= 0 && C1 + -1*I1 >= 0 && -1*C1 + -1*I1 >= 0 && -2 + A1 + -1*I1 >= 0 && -1*I1 + V >= 0 && -1*I1 + -1*V >= 0 && -1*I1 + U >= 0 && -1*I1 + -1*U >= 0 && -1 + -1*I1 + P >= 0 && 1 + -1*I1 + -1*P >= 0 && -2 + -1*I1 + O >= 0 && -2 + A + -1*I1 >= 0 && I1 >= 0 && H1 + I1 >= 0 && -1*H1 + I1 >= 0 && G1 + I1 >= 0 && -1*G1 + I1 >= 0 && D1 + I1 >= 0 && -1*D1 + I1 >= 0 && C1 + I1 >= 0 && -1*C1 + I1 >= 0 && -2 + A1 + I1 >= 0 && I1 + V >= 0 && I1 + -1*V >= 0 && I1 + U >= 0 && I1 + -1*U >= 0 && -1 + I1 + P >= 0 && 1 + I1 + -1*P >= 0 && -2 + I1 + O >= 0 && -2 + A + I1 >= 0 && -1*H1 >= 0 && G1 + -1*H1 >= 0 && -1*G1 + -1*H1 >= 0 && D1 + -1*H1 >= 0 && -1*D1 + -1*H1 >= 0 && C1 + -1*H1 >= 0 && -1*C1 + -1*H1 >= 0 && -2 + A1 + -1*H1 >= 0 && -1*H1 + V >= 0 && -1*H1 + -1*V >= 0 && -1*H1 + U >= 0 && -1*H1 + -1*U >= 0 && -1 + -1*H1 + P >= 0 && 1 + -1*H1 + -1*P >= 0 && -2 + -1*H1 + O >= 0 && -2 + A + -1*H1 >= 0 && H1 >= 0 && G1 + H1 >= 0 && -1*G1 + H1 >= 0 && D1 + H1 >= 0 && -1*D1 + H1 >= 0 && C1 + H1 >= 0 && -1*C1 + H1 >= 0 && -2 + A1 + H1 >= 0 && H1 + V >= 0 && H1 + -1*V >= 0 && H1 + U >= 0 && H1 + -1*U >= 0 && -1 + H1 + P >= 0 && 1 + H1 + -1*P >= 0 && -2 + H1 + O >= 0 && -2 + A + H1 >= 0 && -1*G1 >= 0 && D1 + -1*G1 >= 0 && -1*D1 + -1*G1 >= 0 && C1 + -1*G1 >= 0 && -1*C1 + -1*G1 >= 0 && -2 + A1 + -1*G1 >= 0 && -1*G1 + V >= 0 && -1*G1 + -1*V >= 0 && -1*G1 + U >= 0 && -1*G1 + -1*U >= 0 && -1 + -1*G1 + P >= 0 && 1 + -1*G1 + -1*P >= 0 && -2 + -1*G1 + O >= 0 && -2 + A + -1*G1 >= 0 && G1 >= 0 && D1 + G1 >= 0 && -1*D1 + G1 >= 0 && C1 + G1 >= 0 && -1*C1 + G1 >= 0 && -2 + A1 + G1 >= 0 && G1 + V >= 0 && G1 + -1*V >= 0 && G1 + U >= 0 && G1 + -1*U >= 0 && -1 + G1 + P >= 0 && 1 + G1 + -1*P >= 0 && -2 + G1 + O >= 0 && -2 + A + G1 >= 0 && -1 + C + -1*E1 >= 0 && B1 + -1*E1 >= 0 && -1*D1 >= 0 && C1 + -1*D1 >= 0 && -1*C1 + -1*D1 >= 0 && -2 + A1 + -1*D1 >= 0 && -1*D1 + V >= 0 && -1*D1 + -1*V >= 0 && -1*D1 + U >= 0 && -1*D1 + -1*U >= 0 && -1 + -1*D1 + P >= 0 && 1 + -1*D1 + -1*P >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && C1 + D1 >= 0 && -1*C1 + D1 >= 0 && -2 + A1 + D1 >= 0 && D1 + V >= 0 && D1 + -1*V >= 0 && D1 + U >= 0 && D1 + -1*U >= 0 && -1 + D1 + P >= 0 && 1 + D1 + -1*P >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && 1 + B1 + -1*C >= 0 && -1 + -1*B1 + C >= 0 && -1*C1 >= 0 && -2 + A1 + -1*C1 >= 0 && -1*C1 + V >= 0 && -1*C1 + -1*V >= 0 && -1*C1 + U >= 0 && -1*C1 + -1*U >= 0 && -1 + -1*C1 + P >= 0 && 1 + -1*C1 + -1*P >= 0 && -2 + -1*C1 + O >= 0 && -2 + A + -1*C1 >= 0 && C1 >= 0 && -2 + A1 + C1 >= 0 && C1 + V >= 0 && C1 + -1*V >= 0 && C1 + U >= 0 && C1 + -1*U >= 0 && -1 + C1 + P >= 0 && 1 + C1 + -1*P >= 0 && -2 + C1 + O >= 0 && -2 + A + C1 >= 0 && -2 + A1 >= 0 && -2 + A1 + V >= 0 && -2 + A1 + -1*V >= 0 && -2 + A1 + U >= 0 && -2 + A1 + -1*U >= 0 && -3 + A1 + P >= 0 && -1 + A1 + -1*P >= 0 && -4 + A1 + O >= 0 && -4 + A + A1 >= 0 && -1*A + A1 >= 0 && -1*V >= 0 && U + -1*V >= 0 && -1*U + -1*V >= 0 && -1 + P + -1*V >= 0 && 1 + -1*P + -1*V >= 0 && -2 + O + -1*V >= 0 && -2 + A + -1*V >= 0 && V >= 0 && U + V >= 0 && -1*U + V >= 0 && -1 + P + V >= 0 && 1 + -1*P + V >= 0 && -2 + O + V >= 0 && -2 + A + V >= 0 && -1*U >= 0 && -1 + P + -1*U >= 0 && 1 + -1*P + -1*U >= 0 && -2 + O + -1*U >= 0 && -2 + A + -1*U >= 0 && U >= 0 && -1 + P + U >= 0 && 1 + -1*P + U >= 0 && -2 + O + U >= 0 && -2 + A + U >= 0 && 1 + -1*P >= 0 && -1 + O + -1*P >= 0 && -1 + A + -1*P >= 0 && -1 + P >= 0 && -3 + O + P >= 0 && -3 + A + P >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && E1 >= 0 && A >= 2 && I1 = 0 && H1 = V && G1 = 0 && U = 0 && J1 = V] 1. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(E2,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,F2,Z,A1,B1,G2,D2,E1,F1,B2,Z1,A2,Y1,K1,L1,M1,N1,O1 [-1*F + O >= 0 (1,1) ,S1,T1,U1,V1,W1,X1) ,P1,Q1,R1,S1,T1,U1,V1,W1,X1) && -2 + F >= 0 && -4 + F + T1 >= 0 && F + -1*T1 >= 0 && -2 + F + P1 >= 0 && -1 + F + L1 >= 0 && -3 + F + -1*L1 >= 0 && -2 + F + J1 >= 0 && -2 + F + -1*J1 >= 0 && -2 + F + I1 >= 0 && -2 + F + -1*I1 >= 0 && -2 + F + H1 >= 0 && -2 + F + -1*H1 >= 0 && -2 + F + G1 >= 0 && -2 + F + -1*G1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -2 + C1 + F >= 0 && -2 + -1*C1 + F >= 0 && -4 + A1 + F >= 0 && -2 + F + V >= 0 && -2 + F + -1*V >= 0 && -2 + F + U >= 0 && -2 + F + -1*U >= 0 && -3 + F + P >= 0 && -1 + F + -1*P >= 0 && -4 + F + O >= 0 && F + -1*O >= 0 && -4 + A + F >= 0 && 2 + -1*T1 >= 0 && 2 + P1 + -1*T1 >= 0 && 3 + L1 + -1*T1 >= 0 && 1 + -1*L1 + -1*T1 >= 0 && 2 + J1 + -1*T1 >= 0 && 2 + -1*J1 + -1*T1 >= 0 && 2 + I1 + -1*T1 >= 0 && 2 + -1*I1 + -1*T1 >= 0 && 2 + H1 + -1*T1 >= 0 && 2 + -1*H1 + -1*T1 >= 0 && 2 + G1 + -1*T1 >= 0 && 2 + -1*G1 + -1*T1 >= 0 && 2 + D1 + -1*T1 >= 0 && 2 + -1*D1 + -1*T1 >= 0 && 2 + C1 + -1*T1 >= 0 && 2 + -1*C1 + -1*T1 >= 0 && A1 + -1*T1 >= 0 && 2 + -1*T1 + V >= 0 && 2 + -1*T1 + -1*V >= 0 && 2 + -1*T1 + U >= 0 && 2 + -1*T1 + -1*U >= 0 && 1 + P + -1*T1 >= 0 && 3 + -1*P + -1*T1 >= 0 && O + -1*T1 >= 0 && A + -1*T1 >= 0 && -2 + T1 >= 0 && -2 + P1 + T1 >= 0 && -1 + L1 + T1 >= 0 && -3 + -1*L1 + T1 >= 0 && -2 + J1 + T1 >= 0 && -2 + -1*J1 + T1 >= 0 && -2 + I1 + T1 >= 0 && -2 + -1*I1 + T1 >= 0 && -2 + H1 + T1 >= 0 && -2 + -1*H1 + T1 >= 0 && -2 + G1 + T1 >= 0 && -2 + -1*G1 + T1 >= 0 && -2 + D1 + T1 >= 0 && -2 + -1*D1 + T1 >= 0 && -2 + C1 + T1 >= 0 && -2 + -1*C1 + T1 >= 0 && -4 + A1 + T1 >= 0 && -2 + T1 + V >= 0 && -2 + T1 + -1*V >= 0 && -2 + T1 + U >= 0 && -2 + T1 + -1*U >= 0 && -3 + P + T1 >= 0 && -1 + -1*P + T1 >= 0 && -4 + O + T1 >= 0 && -4 + A + T1 >= 0 && P1 >= 0 && 1 + L1 + P1 >= 0 && -1 + -1*L1 + P1 >= 0 && J1 + P1 >= 0 && -1*J1 + P1 >= 0 && I1 + P1 >= 0 && -1*I1 + P1 >= 0 && H1 + P1 >= 0 && -1*H1 + P1 >= 0 && G1 + P1 >= 0 && -1*G1 + P1 >= 0 && D1 + P1 >= 0 && -1*D1 + P1 >= 0 && C1 + P1 >= 0 && -1*C1 + P1 >= 0 && -2 + A1 + P1 >= 0 && P1 + V >= 0 && P1 + -1*V >= 0 && P1 + U >= 0 && P1 + -1*U >= 0 && -1 + P + P1 >= 0 && 1 + -1*P + P1 >= 0 && -2 + O + P1 >= 0 && -2 + A + P1 >= 0 && -1 + -1*L1 >= 0 && -1 + J1 + -1*L1 >= 0 && -1 + -1*J1 + -1*L1 >= 0 && -1 + I1 + -1*L1 >= 0 && -1 + -1*I1 + -1*L1 >= 0 && -1 + H1 + -1*L1 >= 0 && -1 + -1*H1 + -1*L1 >= 0 && -1 + G1 + -1*L1 >= 0 && -1 + -1*G1 + -1*L1 >= 0 && -1 + D1 + -1*L1 >= 0 && -1 + -1*D1 + -1*L1 >= 0 && -1 + C1 + -1*L1 >= 0 && -1 + -1*C1 + -1*L1 >= 0 && -3 + A1 + -1*L1 >= 0 && -1 + -1*L1 + V >= 0 && -1 + -1*L1 + -1*V >= 0 && -1 + -1*L1 + U >= 0 && -1 + -1*L1 + -1*U >= 0 && -2 + -1*L1 + P >= 0 && -1*L1 + -1*P >= 0 && -3 + -1*L1 + O >= 0 && -3 + A + -1*L1 >= 0 && 1 + L1 >= 0 && 1 + J1 + L1 >= 0 && 1 + -1*J1 + L1 >= 0 && 1 + I1 + L1 >= 0 && 1 + -1*I1 + L1 >= 0 && 1 + H1 + L1 >= 0 && 1 + -1*H1 + L1 >= 0 && 1 + G1 + L1 >= 0 && 1 + -1*G1 + L1 >= 0 && 1 + D1 + L1 >= 0 && 1 + -1*D1 + L1 >= 0 && 1 + C1 + L1 >= 0 && 1 + -1*C1 + L1 >= 0 && -1 + A1 + L1 >= 0 && 1 + L1 + V >= 0 && 1 + L1 + -1*V >= 0 && 1 + L1 + U >= 0 && 1 + L1 + -1*U >= 0 && L1 + P >= 0 && 2 + L1 + -1*P >= 0 && -1 + L1 + O >= 0 && -1 + A + L1 >= 0 && -1*J1 >= 0 && I1 + -1*J1 >= 0 && -1*I1 + -1*J1 >= 0 && H1 + -1*J1 >= 0 && -1*H1 + -1*J1 >= 0 && G1 + -1*J1 >= 0 && -1*G1 + -1*J1 >= 0 && D1 + -1*J1 >= 0 && -1*D1 + -1*J1 >= 0 && C1 + -1*J1 >= 0 && -1*C1 + -1*J1 >= 0 && -2 + A1 + -1*J1 >= 0 && -1*J1 + V >= 0 && -1*J1 + -1*V >= 0 && -1*J1 + U >= 0 && -1*J1 + -1*U >= 0 && -1 + -1*J1 + P >= 0 && 1 + -1*J1 + -1*P >= 0 && -2 + -1*J1 + O >= 0 && -2 + A + -1*J1 >= 0 && J1 >= 0 && I1 + J1 >= 0 && -1*I1 + J1 >= 0 && H1 + J1 >= 0 && -1*H1 + J1 >= 0 && G1 + J1 >= 0 && -1*G1 + J1 >= 0 && D1 + J1 >= 0 && -1*D1 + J1 >= 0 && C1 + J1 >= 0 && -1*C1 + J1 >= 0 && -2 + A1 + J1 >= 0 && J1 + V >= 0 && J1 + -1*V >= 0 && J1 + U >= 0 && J1 + -1*U >= 0 && -1 + J1 + P >= 0 && 1 + J1 + -1*P >= 0 && -2 + J1 + O >= 0 && -2 + A + J1 >= 0 && -1*I1 >= 0 && H1 + -1*I1 >= 0 && -1*H1 + -1*I1 >= 0 && G1 + -1*I1 >= 0 && -1*G1 + -1*I1 >= 0 && D1 + -1*I1 >= 0 && -1*D1 + -1*I1 >= 0 && C1 + -1*I1 >= 0 && -1*C1 + -1*I1 >= 0 && -2 + A1 + -1*I1 >= 0 && -1*I1 + V >= 0 && -1*I1 + -1*V >= 0 && -1*I1 + U >= 0 && -1*I1 + -1*U >= 0 && -1 + -1*I1 + P >= 0 && 1 + -1*I1 + -1*P >= 0 && -2 + -1*I1 + O >= 0 && -2 + A + -1*I1 >= 0 && I1 >= 0 && H1 + I1 >= 0 && -1*H1 + I1 >= 0 && G1 + I1 >= 0 && -1*G1 + I1 >= 0 && D1 + I1 >= 0 && -1*D1 + I1 >= 0 && C1 + I1 >= 0 && -1*C1 + I1 >= 0 && -2 + A1 + I1 >= 0 && I1 + V >= 0 && I1 + -1*V >= 0 && I1 + U >= 0 && I1 + -1*U >= 0 && -1 + I1 + P >= 0 && 1 + I1 + -1*P >= 0 && -2 + I1 + O >= 0 && -2 + A + I1 >= 0 && -1*H1 >= 0 && G1 + -1*H1 >= 0 && -1*G1 + -1*H1 >= 0 && D1 + -1*H1 >= 0 && -1*D1 + -1*H1 >= 0 && C1 + -1*H1 >= 0 && -1*C1 + -1*H1 >= 0 && -2 + A1 + -1*H1 >= 0 && -1*H1 + V >= 0 && -1*H1 + -1*V >= 0 && -1*H1 + U >= 0 && -1*H1 + -1*U >= 0 && -1 + -1*H1 + P >= 0 && 1 + -1*H1 + -1*P >= 0 && -2 + -1*H1 + O >= 0 && -2 + A + -1*H1 >= 0 && H1 >= 0 && G1 + H1 >= 0 && -1*G1 + H1 >= 0 && D1 + H1 >= 0 && -1*D1 + H1 >= 0 && C1 + H1 >= 0 && -1*C1 + H1 >= 0 && -2 + A1 + H1 >= 0 && H1 + V >= 0 && H1 + -1*V >= 0 && H1 + U >= 0 && H1 + -1*U >= 0 && -1 + H1 + P >= 0 && 1 + H1 + -1*P >= 0 && -2 + H1 + O >= 0 && -2 + A + H1 >= 0 && -1*G1 >= 0 && D1 + -1*G1 >= 0 && -1*D1 + -1*G1 >= 0 && C1 + -1*G1 >= 0 && -1*C1 + -1*G1 >= 0 && -2 + A1 + -1*G1 >= 0 && -1*G1 + V >= 0 && -1*G1 + -1*V >= 0 && -1*G1 + U >= 0 && -1*G1 + -1*U >= 0 && -1 + -1*G1 + P >= 0 && 1 + -1*G1 + -1*P >= 0 && -2 + -1*G1 + O >= 0 && -2 + A + -1*G1 >= 0 && G1 >= 0 && D1 + G1 >= 0 && -1*D1 + G1 >= 0 && C1 + G1 >= 0 && -1*C1 + G1 >= 0 && -2 + A1 + G1 >= 0 && G1 + V >= 0 && G1 + -1*V >= 0 && G1 + U >= 0 && G1 + -1*U >= 0 && -1 + G1 + P >= 0 && 1 + G1 + -1*P >= 0 && -2 + G1 + O >= 0 && -2 + A + G1 >= 0 && -1 + C + -1*E1 >= 0 && B1 + -1*E1 >= 0 && -1*D1 >= 0 && C1 + -1*D1 >= 0 && -1*C1 + -1*D1 >= 0 && -2 + A1 + -1*D1 >= 0 && -1*D1 + V >= 0 && -1*D1 + -1*V >= 0 && -1*D1 + U >= 0 && -1*D1 + -1*U >= 0 && -1 + -1*D1 + P >= 0 && 1 + -1*D1 + -1*P >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && C1 + D1 >= 0 && -1*C1 + D1 >= 0 && -2 + A1 + D1 >= 0 && D1 + V >= 0 && D1 + -1*V >= 0 && D1 + U >= 0 && D1 + -1*U >= 0 && -1 + D1 + P >= 0 && 1 + D1 + -1*P >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && 1 + B1 + -1*C >= 0 && -1 + -1*B1 + C >= 0 && -1*C1 >= 0 && -2 + A1 + -1*C1 >= 0 && -1*C1 + V >= 0 && -1*C1 + -1*V >= 0 && -1*C1 + U >= 0 && -1*C1 + -1*U >= 0 && -1 + -1*C1 + P >= 0 && 1 + -1*C1 + -1*P >= 0 && -2 + -1*C1 + O >= 0 && -2 + A + -1*C1 >= 0 && C1 >= 0 && -2 + A1 + C1 >= 0 && C1 + V >= 0 && C1 + -1*V >= 0 && C1 + U >= 0 && C1 + -1*U >= 0 && -1 + C1 + P >= 0 && 1 + C1 + -1*P >= 0 && -2 + C1 + O >= 0 && -2 + A + C1 >= 0 && -2 + A1 >= 0 && -2 + A1 + V >= 0 && -2 + A1 + -1*V >= 0 && -2 + A1 + U >= 0 && -2 + A1 + -1*U >= 0 && -3 + A1 + P >= 0 && -1 + A1 + -1*P >= 0 && -4 + A1 + O >= 0 && -4 + A + A1 >= 0 && -1*A + A1 >= 0 && -1*V >= 0 && U + -1*V >= 0 && -1*U + -1*V >= 0 && -1 + P + -1*V >= 0 && 1 + -1*P + -1*V >= 0 && -2 + O + -1*V >= 0 && -2 + A + -1*V >= 0 && V >= 0 && U + V >= 0 && -1*U + V >= 0 && -1 + P + V >= 0 && 1 + -1*P + V >= 0 && -2 + O + V >= 0 && -2 + A + V >= 0 && -1*U >= 0 && -1 + P + -1*U >= 0 && 1 + -1*P + -1*U >= 0 && -2 + O + -1*U >= 0 && -2 + A + -1*U >= 0 && U >= 0 && -1 + P + U >= 0 && 1 + -1*P + U >= 0 && -2 + O + U >= 0 && -2 + A + U >= 0 && 1 + -1*P >= 0 && -1 + O + -1*P >= 0 && -1 + A + -1*P >= 0 && -1 + P >= 0 && -3 + O + P >= 0 && -3 + A + P >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && E1 >= 0 && G1 = D1] 2. f116(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f116(A,B,1 + C,D,E,-1 + F,G,H,I,J,K,L,M,N,F,1,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,U [-2 + C + F >= 0 (?,1) ,R1,S1,T1,U1,V1,W1,X1) ,1 + C,-1 + F,P1,Q1,R1,S1,T1,U1,V1,W1,X1) && -2 + F + P >= 0 && 2 + -1*T1 >= 0 && 2 + C + -1*T1 >= 0 && A1 + -1*T1 >= 0 && 2 + P + -1*T1 >= 0 && A + -1*T1 >= 0 && -2 + T1 >= 0 && -2 + C + T1 >= 0 && -4 + A1 + T1 >= 0 && -2 + P + T1 >= 0 && -4 + A + T1 >= 0 && -1*C + P >= 0 && C >= 0 && -2 + A1 + C >= 0 && C + P >= 0 && C + -1*P >= 0 && -2 + A + C >= 0 && -2 + A1 >= 0 && -2 + A1 + P >= 0 && -4 + A + A1 >= 0 && -1*A + A1 >= 0 && U + -1*V >= 0 && -1*U + V >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && A >= 2 && F >= 0 && P = 0 && U = M1] 3. f116(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f8(A,B,1 + E1,D,E,F,G,H,I,J,K,L,M,N,F,1,Q,R,S,T,0,V,W,X,Y,Z,A1,E1,V,V,E1,F1,0,V,0,V,K1,-1,M1,N1,O1,Z1,Q1[-2 + C + F >= 0 (1,1) ,R1,S1,T1,U1,V1,W1,X1) ,R1,S1,T1,U1,V1,W1,X1) && -2 + F + P >= 0 && 2 + -1*T1 >= 0 && 2 + C + -1*T1 >= 0 && A1 + -1*T1 >= 0 && 2 + P + -1*T1 >= 0 && A + -1*T1 >= 0 && -2 + T1 >= 0 && -2 + C + T1 >= 0 && -4 + A1 + T1 >= 0 && -2 + P + T1 >= 0 && -4 + A + T1 >= 0 && -1*C + P >= 0 && C >= 0 && -2 + A1 + C >= 0 && C + P >= 0 && C + -1*P >= 0 && -2 + A + C >= 0 && -2 + A1 >= 0 && -2 + A1 + P >= 0 && -4 + A + A1 >= 0 && -1*A + A1 >= 0 && U + -1*V >= 0 && -1*U + V >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && Z1 >= 0 && A >= 2 && F >= 0 && U = 0 && P = 0] 4. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f1(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,S,Z1,S,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1[2 + -1*T1 >= 0 (?,1) ,S1,T1,U1,V1,W1,X1) ,P1,Q1,R1,S1,T1,U1,V1,W1,X1) && B + -1*T1 >= 0 && Q + -1*T1 >= 0 && 2 + P + -1*T1 >= 0 && 2 + -1*P + -1*T1 >= 0 && -2 + T1 >= 0 && -4 + B + T1 >= 0 && -4 + Q + T1 >= 0 && -2 + P + T1 >= 0 && -2 + -1*P + T1 >= 0 && R + -1*T >= 0 && -1*R + T >= 0 && -1*B + Q >= 0 && -2 + B >= 0 && -4 + B + Q >= 0 && -2 + B + P >= 0 && -2 + B + -1*P >= 0 && -2 + Q >= 0 && -2 + P + Q >= 0 && -2 + -1*P + Q >= 0 && -1*P >= 0 && P >= 0 && B >= 0 && Q >= 1 + B] 5. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f116(A,Z1,0,D,E,F,G,H,I,J,K,L,M,N,O,P,A2,Y1,D2,B2,R,R,E2,F2,G2,Z1,C2,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1[2 + -1*T1 >= 0 (1,1) ,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1) && B + -1*T1 >= 0 && Q + -1*T1 >= 0 && 2 + P + -1*T1 >= 0 && 2 + -1*P + -1*T1 >= 0 && -2 + T1 >= 0 && -4 + B + T1 >= 0 && -4 + Q + T1 >= 0 && -2 + P + T1 >= 0 && -2 + -1*P + T1 >= 0 && R + -1*T >= 0 && -1*R + T >= 0 && -1*B + Q >= 0 && -2 + B >= 0 && -4 + B + Q >= 0 && -2 + B + P >= 0 && -2 + B + -1*P >= 0 && -2 + Q >= 0 && -2 + P + Q >= 0 && -2 + -1*P + Q >= 0 && -1*P >= 0 && P >= 0 && A >= 2 && C2 >= A && F >= A && B >= Q && B >= 0 && C = 0] 6. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f1(Z1,2,C,D,E,F,G,H,I,J,K,L,M,N,O,0,Z1,S,B2,S,U,V,S,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1 [Z1 >= 2 && S = W] (1,1) ,S1,T1,U1,V1,W1,X1) ,P1,A2,Y1,D2,2,E2,V1,W1,X1) 7. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(F2,E2,C,D,E,F,G,H,I,J,K,L,M,N,O,0,C2,H2,J2,I2,0,0,K2,L2,M2,Z,A1,B1,N2,D2,E1,F1,B2,Z1,A2,Y1,K1,L1,M1 [0 >= F2] (1,1) ,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,Q1,G2,S1,T1,U1,V1,W1,X1) 8. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(1,E2,C,D,E,F,G,H,I,J,K,L,M,N,O,0,H2,I2,K2,J2,0,0,M2,N2,O2,Z,A1,B1,Q2,D2,E1,F1,B2,Z1,A2,Y1,K1,L1,M1 [S = 0 && W = 0] (1,1) ,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,G2,C2,L2,T1,U1,F2,G2,P2) Signature: {(f1,50);(f10,50);(f116,50);(f8,50);(f9,50)} Flow Graph: [0->{0,1},1->{},2->{2,3},3->{0,1},4->{4,5},5->{2,3},6->{4,5},7->{},8->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(2,2),(2,3)] * Step 3: Looptree YES + Considered Problem: Rules: 0. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,0,H1,W,X,Y,Z,A1,B1,D1,D1,-1 + E1,F1,0,H1,0,H1,-1 + E1,L1,M1 [-1*F + O >= 0 (?,1) ,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1) && -2 + F >= 0 && -4 + F + T1 >= 0 && F + -1*T1 >= 0 && -2 + F + P1 >= 0 && -1 + F + L1 >= 0 && -3 + F + -1*L1 >= 0 && -2 + F + J1 >= 0 && -2 + F + -1*J1 >= 0 && -2 + F + I1 >= 0 && -2 + F + -1*I1 >= 0 && -2 + F + H1 >= 0 && -2 + F + -1*H1 >= 0 && -2 + F + G1 >= 0 && -2 + F + -1*G1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -2 + C1 + F >= 0 && -2 + -1*C1 + F >= 0 && -4 + A1 + F >= 0 && -2 + F + V >= 0 && -2 + F + -1*V >= 0 && -2 + F + U >= 0 && -2 + F + -1*U >= 0 && -3 + F + P >= 0 && -1 + F + -1*P >= 0 && -4 + F + O >= 0 && F + -1*O >= 0 && -4 + A + F >= 0 && 2 + -1*T1 >= 0 && 2 + P1 + -1*T1 >= 0 && 3 + L1 + -1*T1 >= 0 && 1 + -1*L1 + -1*T1 >= 0 && 2 + J1 + -1*T1 >= 0 && 2 + -1*J1 + -1*T1 >= 0 && 2 + I1 + -1*T1 >= 0 && 2 + -1*I1 + -1*T1 >= 0 && 2 + H1 + -1*T1 >= 0 && 2 + -1*H1 + -1*T1 >= 0 && 2 + G1 + -1*T1 >= 0 && 2 + -1*G1 + -1*T1 >= 0 && 2 + D1 + -1*T1 >= 0 && 2 + -1*D1 + -1*T1 >= 0 && 2 + C1 + -1*T1 >= 0 && 2 + -1*C1 + -1*T1 >= 0 && A1 + -1*T1 >= 0 && 2 + -1*T1 + V >= 0 && 2 + -1*T1 + -1*V >= 0 && 2 + -1*T1 + U >= 0 && 2 + -1*T1 + -1*U >= 0 && 1 + P + -1*T1 >= 0 && 3 + -1*P + -1*T1 >= 0 && O + -1*T1 >= 0 && A + -1*T1 >= 0 && -2 + T1 >= 0 && -2 + P1 + T1 >= 0 && -1 + L1 + T1 >= 0 && -3 + -1*L1 + T1 >= 0 && -2 + J1 + T1 >= 0 && -2 + -1*J1 + T1 >= 0 && -2 + I1 + T1 >= 0 && -2 + -1*I1 + T1 >= 0 && -2 + H1 + T1 >= 0 && -2 + -1*H1 + T1 >= 0 && -2 + G1 + T1 >= 0 && -2 + -1*G1 + T1 >= 0 && -2 + D1 + T1 >= 0 && -2 + -1*D1 + T1 >= 0 && -2 + C1 + T1 >= 0 && -2 + -1*C1 + T1 >= 0 && -4 + A1 + T1 >= 0 && -2 + T1 + V >= 0 && -2 + T1 + -1*V >= 0 && -2 + T1 + U >= 0 && -2 + T1 + -1*U >= 0 && -3 + P + T1 >= 0 && -1 + -1*P + T1 >= 0 && -4 + O + T1 >= 0 && -4 + A + T1 >= 0 && P1 >= 0 && 1 + L1 + P1 >= 0 && -1 + -1*L1 + P1 >= 0 && J1 + P1 >= 0 && -1*J1 + P1 >= 0 && I1 + P1 >= 0 && -1*I1 + P1 >= 0 && H1 + P1 >= 0 && -1*H1 + P1 >= 0 && G1 + P1 >= 0 && -1*G1 + P1 >= 0 && D1 + P1 >= 0 && -1*D1 + P1 >= 0 && C1 + P1 >= 0 && -1*C1 + P1 >= 0 && -2 + A1 + P1 >= 0 && P1 + V >= 0 && P1 + -1*V >= 0 && P1 + U >= 0 && P1 + -1*U >= 0 && -1 + P + P1 >= 0 && 1 + -1*P + P1 >= 0 && -2 + O + P1 >= 0 && -2 + A + P1 >= 0 && -1 + -1*L1 >= 0 && -1 + J1 + -1*L1 >= 0 && -1 + -1*J1 + -1*L1 >= 0 && -1 + I1 + -1*L1 >= 0 && -1 + -1*I1 + -1*L1 >= 0 && -1 + H1 + -1*L1 >= 0 && -1 + -1*H1 + -1*L1 >= 0 && -1 + G1 + -1*L1 >= 0 && -1 + -1*G1 + -1*L1 >= 0 && -1 + D1 + -1*L1 >= 0 && -1 + -1*D1 + -1*L1 >= 0 && -1 + C1 + -1*L1 >= 0 && -1 + -1*C1 + -1*L1 >= 0 && -3 + A1 + -1*L1 >= 0 && -1 + -1*L1 + V >= 0 && -1 + -1*L1 + -1*V >= 0 && -1 + -1*L1 + U >= 0 && -1 + -1*L1 + -1*U >= 0 && -2 + -1*L1 + P >= 0 && -1*L1 + -1*P >= 0 && -3 + -1*L1 + O >= 0 && -3 + A + -1*L1 >= 0 && 1 + L1 >= 0 && 1 + J1 + L1 >= 0 && 1 + -1*J1 + L1 >= 0 && 1 + I1 + L1 >= 0 && 1 + -1*I1 + L1 >= 0 && 1 + H1 + L1 >= 0 && 1 + -1*H1 + L1 >= 0 && 1 + G1 + L1 >= 0 && 1 + -1*G1 + L1 >= 0 && 1 + D1 + L1 >= 0 && 1 + -1*D1 + L1 >= 0 && 1 + C1 + L1 >= 0 && 1 + -1*C1 + L1 >= 0 && -1 + A1 + L1 >= 0 && 1 + L1 + V >= 0 && 1 + L1 + -1*V >= 0 && 1 + L1 + U >= 0 && 1 + L1 + -1*U >= 0 && L1 + P >= 0 && 2 + L1 + -1*P >= 0 && -1 + L1 + O >= 0 && -1 + A + L1 >= 0 && -1*J1 >= 0 && I1 + -1*J1 >= 0 && -1*I1 + -1*J1 >= 0 && H1 + -1*J1 >= 0 && -1*H1 + -1*J1 >= 0 && G1 + -1*J1 >= 0 && -1*G1 + -1*J1 >= 0 && D1 + -1*J1 >= 0 && -1*D1 + -1*J1 >= 0 && C1 + -1*J1 >= 0 && -1*C1 + -1*J1 >= 0 && -2 + A1 + -1*J1 >= 0 && -1*J1 + V >= 0 && -1*J1 + -1*V >= 0 && -1*J1 + U >= 0 && -1*J1 + -1*U >= 0 && -1 + -1*J1 + P >= 0 && 1 + -1*J1 + -1*P >= 0 && -2 + -1*J1 + O >= 0 && -2 + A + -1*J1 >= 0 && J1 >= 0 && I1 + J1 >= 0 && -1*I1 + J1 >= 0 && H1 + J1 >= 0 && -1*H1 + J1 >= 0 && G1 + J1 >= 0 && -1*G1 + J1 >= 0 && D1 + J1 >= 0 && -1*D1 + J1 >= 0 && C1 + J1 >= 0 && -1*C1 + J1 >= 0 && -2 + A1 + J1 >= 0 && J1 + V >= 0 && J1 + -1*V >= 0 && J1 + U >= 0 && J1 + -1*U >= 0 && -1 + J1 + P >= 0 && 1 + J1 + -1*P >= 0 && -2 + J1 + O >= 0 && -2 + A + J1 >= 0 && -1*I1 >= 0 && H1 + -1*I1 >= 0 && -1*H1 + -1*I1 >= 0 && G1 + -1*I1 >= 0 && -1*G1 + -1*I1 >= 0 && D1 + -1*I1 >= 0 && -1*D1 + -1*I1 >= 0 && C1 + -1*I1 >= 0 && -1*C1 + -1*I1 >= 0 && -2 + A1 + -1*I1 >= 0 && -1*I1 + V >= 0 && -1*I1 + -1*V >= 0 && -1*I1 + U >= 0 && -1*I1 + -1*U >= 0 && -1 + -1*I1 + P >= 0 && 1 + -1*I1 + -1*P >= 0 && -2 + -1*I1 + O >= 0 && -2 + A + -1*I1 >= 0 && I1 >= 0 && H1 + I1 >= 0 && -1*H1 + I1 >= 0 && G1 + I1 >= 0 && -1*G1 + I1 >= 0 && D1 + I1 >= 0 && -1*D1 + I1 >= 0 && C1 + I1 >= 0 && -1*C1 + I1 >= 0 && -2 + A1 + I1 >= 0 && I1 + V >= 0 && I1 + -1*V >= 0 && I1 + U >= 0 && I1 + -1*U >= 0 && -1 + I1 + P >= 0 && 1 + I1 + -1*P >= 0 && -2 + I1 + O >= 0 && -2 + A + I1 >= 0 && -1*H1 >= 0 && G1 + -1*H1 >= 0 && -1*G1 + -1*H1 >= 0 && D1 + -1*H1 >= 0 && -1*D1 + -1*H1 >= 0 && C1 + -1*H1 >= 0 && -1*C1 + -1*H1 >= 0 && -2 + A1 + -1*H1 >= 0 && -1*H1 + V >= 0 && -1*H1 + -1*V >= 0 && -1*H1 + U >= 0 && -1*H1 + -1*U >= 0 && -1 + -1*H1 + P >= 0 && 1 + -1*H1 + -1*P >= 0 && -2 + -1*H1 + O >= 0 && -2 + A + -1*H1 >= 0 && H1 >= 0 && G1 + H1 >= 0 && -1*G1 + H1 >= 0 && D1 + H1 >= 0 && -1*D1 + H1 >= 0 && C1 + H1 >= 0 && -1*C1 + H1 >= 0 && -2 + A1 + H1 >= 0 && H1 + V >= 0 && H1 + -1*V >= 0 && H1 + U >= 0 && H1 + -1*U >= 0 && -1 + H1 + P >= 0 && 1 + H1 + -1*P >= 0 && -2 + H1 + O >= 0 && -2 + A + H1 >= 0 && -1*G1 >= 0 && D1 + -1*G1 >= 0 && -1*D1 + -1*G1 >= 0 && C1 + -1*G1 >= 0 && -1*C1 + -1*G1 >= 0 && -2 + A1 + -1*G1 >= 0 && -1*G1 + V >= 0 && -1*G1 + -1*V >= 0 && -1*G1 + U >= 0 && -1*G1 + -1*U >= 0 && -1 + -1*G1 + P >= 0 && 1 + -1*G1 + -1*P >= 0 && -2 + -1*G1 + O >= 0 && -2 + A + -1*G1 >= 0 && G1 >= 0 && D1 + G1 >= 0 && -1*D1 + G1 >= 0 && C1 + G1 >= 0 && -1*C1 + G1 >= 0 && -2 + A1 + G1 >= 0 && G1 + V >= 0 && G1 + -1*V >= 0 && G1 + U >= 0 && G1 + -1*U >= 0 && -1 + G1 + P >= 0 && 1 + G1 + -1*P >= 0 && -2 + G1 + O >= 0 && -2 + A + G1 >= 0 && -1 + C + -1*E1 >= 0 && B1 + -1*E1 >= 0 && -1*D1 >= 0 && C1 + -1*D1 >= 0 && -1*C1 + -1*D1 >= 0 && -2 + A1 + -1*D1 >= 0 && -1*D1 + V >= 0 && -1*D1 + -1*V >= 0 && -1*D1 + U >= 0 && -1*D1 + -1*U >= 0 && -1 + -1*D1 + P >= 0 && 1 + -1*D1 + -1*P >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && C1 + D1 >= 0 && -1*C1 + D1 >= 0 && -2 + A1 + D1 >= 0 && D1 + V >= 0 && D1 + -1*V >= 0 && D1 + U >= 0 && D1 + -1*U >= 0 && -1 + D1 + P >= 0 && 1 + D1 + -1*P >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && 1 + B1 + -1*C >= 0 && -1 + -1*B1 + C >= 0 && -1*C1 >= 0 && -2 + A1 + -1*C1 >= 0 && -1*C1 + V >= 0 && -1*C1 + -1*V >= 0 && -1*C1 + U >= 0 && -1*C1 + -1*U >= 0 && -1 + -1*C1 + P >= 0 && 1 + -1*C1 + -1*P >= 0 && -2 + -1*C1 + O >= 0 && -2 + A + -1*C1 >= 0 && C1 >= 0 && -2 + A1 + C1 >= 0 && C1 + V >= 0 && C1 + -1*V >= 0 && C1 + U >= 0 && C1 + -1*U >= 0 && -1 + C1 + P >= 0 && 1 + C1 + -1*P >= 0 && -2 + C1 + O >= 0 && -2 + A + C1 >= 0 && -2 + A1 >= 0 && -2 + A1 + V >= 0 && -2 + A1 + -1*V >= 0 && -2 + A1 + U >= 0 && -2 + A1 + -1*U >= 0 && -3 + A1 + P >= 0 && -1 + A1 + -1*P >= 0 && -4 + A1 + O >= 0 && -4 + A + A1 >= 0 && -1*A + A1 >= 0 && -1*V >= 0 && U + -1*V >= 0 && -1*U + -1*V >= 0 && -1 + P + -1*V >= 0 && 1 + -1*P + -1*V >= 0 && -2 + O + -1*V >= 0 && -2 + A + -1*V >= 0 && V >= 0 && U + V >= 0 && -1*U + V >= 0 && -1 + P + V >= 0 && 1 + -1*P + V >= 0 && -2 + O + V >= 0 && -2 + A + V >= 0 && -1*U >= 0 && -1 + P + -1*U >= 0 && 1 + -1*P + -1*U >= 0 && -2 + O + -1*U >= 0 && -2 + A + -1*U >= 0 && U >= 0 && -1 + P + U >= 0 && 1 + -1*P + U >= 0 && -2 + O + U >= 0 && -2 + A + U >= 0 && 1 + -1*P >= 0 && -1 + O + -1*P >= 0 && -1 + A + -1*P >= 0 && -1 + P >= 0 && -3 + O + P >= 0 && -3 + A + P >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && E1 >= 0 && A >= 2 && I1 = 0 && H1 = V && G1 = 0 && U = 0 && J1 = V] 1. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(E2,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,F2,Z,A1,B1,G2,D2,E1,F1,B2,Z1,A2,Y1,K1,L1,M1,N1,O1 [-1*F + O >= 0 (1,1) ,S1,T1,U1,V1,W1,X1) ,P1,Q1,R1,S1,T1,U1,V1,W1,X1) && -2 + F >= 0 && -4 + F + T1 >= 0 && F + -1*T1 >= 0 && -2 + F + P1 >= 0 && -1 + F + L1 >= 0 && -3 + F + -1*L1 >= 0 && -2 + F + J1 >= 0 && -2 + F + -1*J1 >= 0 && -2 + F + I1 >= 0 && -2 + F + -1*I1 >= 0 && -2 + F + H1 >= 0 && -2 + F + -1*H1 >= 0 && -2 + F + G1 >= 0 && -2 + F + -1*G1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -2 + C1 + F >= 0 && -2 + -1*C1 + F >= 0 && -4 + A1 + F >= 0 && -2 + F + V >= 0 && -2 + F + -1*V >= 0 && -2 + F + U >= 0 && -2 + F + -1*U >= 0 && -3 + F + P >= 0 && -1 + F + -1*P >= 0 && -4 + F + O >= 0 && F + -1*O >= 0 && -4 + A + F >= 0 && 2 + -1*T1 >= 0 && 2 + P1 + -1*T1 >= 0 && 3 + L1 + -1*T1 >= 0 && 1 + -1*L1 + -1*T1 >= 0 && 2 + J1 + -1*T1 >= 0 && 2 + -1*J1 + -1*T1 >= 0 && 2 + I1 + -1*T1 >= 0 && 2 + -1*I1 + -1*T1 >= 0 && 2 + H1 + -1*T1 >= 0 && 2 + -1*H1 + -1*T1 >= 0 && 2 + G1 + -1*T1 >= 0 && 2 + -1*G1 + -1*T1 >= 0 && 2 + D1 + -1*T1 >= 0 && 2 + -1*D1 + -1*T1 >= 0 && 2 + C1 + -1*T1 >= 0 && 2 + -1*C1 + -1*T1 >= 0 && A1 + -1*T1 >= 0 && 2 + -1*T1 + V >= 0 && 2 + -1*T1 + -1*V >= 0 && 2 + -1*T1 + U >= 0 && 2 + -1*T1 + -1*U >= 0 && 1 + P + -1*T1 >= 0 && 3 + -1*P + -1*T1 >= 0 && O + -1*T1 >= 0 && A + -1*T1 >= 0 && -2 + T1 >= 0 && -2 + P1 + T1 >= 0 && -1 + L1 + T1 >= 0 && -3 + -1*L1 + T1 >= 0 && -2 + J1 + T1 >= 0 && -2 + -1*J1 + T1 >= 0 && -2 + I1 + T1 >= 0 && -2 + -1*I1 + T1 >= 0 && -2 + H1 + T1 >= 0 && -2 + -1*H1 + T1 >= 0 && -2 + G1 + T1 >= 0 && -2 + -1*G1 + T1 >= 0 && -2 + D1 + T1 >= 0 && -2 + -1*D1 + T1 >= 0 && -2 + C1 + T1 >= 0 && -2 + -1*C1 + T1 >= 0 && -4 + A1 + T1 >= 0 && -2 + T1 + V >= 0 && -2 + T1 + -1*V >= 0 && -2 + T1 + U >= 0 && -2 + T1 + -1*U >= 0 && -3 + P + T1 >= 0 && -1 + -1*P + T1 >= 0 && -4 + O + T1 >= 0 && -4 + A + T1 >= 0 && P1 >= 0 && 1 + L1 + P1 >= 0 && -1 + -1*L1 + P1 >= 0 && J1 + P1 >= 0 && -1*J1 + P1 >= 0 && I1 + P1 >= 0 && -1*I1 + P1 >= 0 && H1 + P1 >= 0 && -1*H1 + P1 >= 0 && G1 + P1 >= 0 && -1*G1 + P1 >= 0 && D1 + P1 >= 0 && -1*D1 + P1 >= 0 && C1 + P1 >= 0 && -1*C1 + P1 >= 0 && -2 + A1 + P1 >= 0 && P1 + V >= 0 && P1 + -1*V >= 0 && P1 + U >= 0 && P1 + -1*U >= 0 && -1 + P + P1 >= 0 && 1 + -1*P + P1 >= 0 && -2 + O + P1 >= 0 && -2 + A + P1 >= 0 && -1 + -1*L1 >= 0 && -1 + J1 + -1*L1 >= 0 && -1 + -1*J1 + -1*L1 >= 0 && -1 + I1 + -1*L1 >= 0 && -1 + -1*I1 + -1*L1 >= 0 && -1 + H1 + -1*L1 >= 0 && -1 + -1*H1 + -1*L1 >= 0 && -1 + G1 + -1*L1 >= 0 && -1 + -1*G1 + -1*L1 >= 0 && -1 + D1 + -1*L1 >= 0 && -1 + -1*D1 + -1*L1 >= 0 && -1 + C1 + -1*L1 >= 0 && -1 + -1*C1 + -1*L1 >= 0 && -3 + A1 + -1*L1 >= 0 && -1 + -1*L1 + V >= 0 && -1 + -1*L1 + -1*V >= 0 && -1 + -1*L1 + U >= 0 && -1 + -1*L1 + -1*U >= 0 && -2 + -1*L1 + P >= 0 && -1*L1 + -1*P >= 0 && -3 + -1*L1 + O >= 0 && -3 + A + -1*L1 >= 0 && 1 + L1 >= 0 && 1 + J1 + L1 >= 0 && 1 + -1*J1 + L1 >= 0 && 1 + I1 + L1 >= 0 && 1 + -1*I1 + L1 >= 0 && 1 + H1 + L1 >= 0 && 1 + -1*H1 + L1 >= 0 && 1 + G1 + L1 >= 0 && 1 + -1*G1 + L1 >= 0 && 1 + D1 + L1 >= 0 && 1 + -1*D1 + L1 >= 0 && 1 + C1 + L1 >= 0 && 1 + -1*C1 + L1 >= 0 && -1 + A1 + L1 >= 0 && 1 + L1 + V >= 0 && 1 + L1 + -1*V >= 0 && 1 + L1 + U >= 0 && 1 + L1 + -1*U >= 0 && L1 + P >= 0 && 2 + L1 + -1*P >= 0 && -1 + L1 + O >= 0 && -1 + A + L1 >= 0 && -1*J1 >= 0 && I1 + -1*J1 >= 0 && -1*I1 + -1*J1 >= 0 && H1 + -1*J1 >= 0 && -1*H1 + -1*J1 >= 0 && G1 + -1*J1 >= 0 && -1*G1 + -1*J1 >= 0 && D1 + -1*J1 >= 0 && -1*D1 + -1*J1 >= 0 && C1 + -1*J1 >= 0 && -1*C1 + -1*J1 >= 0 && -2 + A1 + -1*J1 >= 0 && -1*J1 + V >= 0 && -1*J1 + -1*V >= 0 && -1*J1 + U >= 0 && -1*J1 + -1*U >= 0 && -1 + -1*J1 + P >= 0 && 1 + -1*J1 + -1*P >= 0 && -2 + -1*J1 + O >= 0 && -2 + A + -1*J1 >= 0 && J1 >= 0 && I1 + J1 >= 0 && -1*I1 + J1 >= 0 && H1 + J1 >= 0 && -1*H1 + J1 >= 0 && G1 + J1 >= 0 && -1*G1 + J1 >= 0 && D1 + J1 >= 0 && -1*D1 + J1 >= 0 && C1 + J1 >= 0 && -1*C1 + J1 >= 0 && -2 + A1 + J1 >= 0 && J1 + V >= 0 && J1 + -1*V >= 0 && J1 + U >= 0 && J1 + -1*U >= 0 && -1 + J1 + P >= 0 && 1 + J1 + -1*P >= 0 && -2 + J1 + O >= 0 && -2 + A + J1 >= 0 && -1*I1 >= 0 && H1 + -1*I1 >= 0 && -1*H1 + -1*I1 >= 0 && G1 + -1*I1 >= 0 && -1*G1 + -1*I1 >= 0 && D1 + -1*I1 >= 0 && -1*D1 + -1*I1 >= 0 && C1 + -1*I1 >= 0 && -1*C1 + -1*I1 >= 0 && -2 + A1 + -1*I1 >= 0 && -1*I1 + V >= 0 && -1*I1 + -1*V >= 0 && -1*I1 + U >= 0 && -1*I1 + -1*U >= 0 && -1 + -1*I1 + P >= 0 && 1 + -1*I1 + -1*P >= 0 && -2 + -1*I1 + O >= 0 && -2 + A + -1*I1 >= 0 && I1 >= 0 && H1 + I1 >= 0 && -1*H1 + I1 >= 0 && G1 + I1 >= 0 && -1*G1 + I1 >= 0 && D1 + I1 >= 0 && -1*D1 + I1 >= 0 && C1 + I1 >= 0 && -1*C1 + I1 >= 0 && -2 + A1 + I1 >= 0 && I1 + V >= 0 && I1 + -1*V >= 0 && I1 + U >= 0 && I1 + -1*U >= 0 && -1 + I1 + P >= 0 && 1 + I1 + -1*P >= 0 && -2 + I1 + O >= 0 && -2 + A + I1 >= 0 && -1*H1 >= 0 && G1 + -1*H1 >= 0 && -1*G1 + -1*H1 >= 0 && D1 + -1*H1 >= 0 && -1*D1 + -1*H1 >= 0 && C1 + -1*H1 >= 0 && -1*C1 + -1*H1 >= 0 && -2 + A1 + -1*H1 >= 0 && -1*H1 + V >= 0 && -1*H1 + -1*V >= 0 && -1*H1 + U >= 0 && -1*H1 + -1*U >= 0 && -1 + -1*H1 + P >= 0 && 1 + -1*H1 + -1*P >= 0 && -2 + -1*H1 + O >= 0 && -2 + A + -1*H1 >= 0 && H1 >= 0 && G1 + H1 >= 0 && -1*G1 + H1 >= 0 && D1 + H1 >= 0 && -1*D1 + H1 >= 0 && C1 + H1 >= 0 && -1*C1 + H1 >= 0 && -2 + A1 + H1 >= 0 && H1 + V >= 0 && H1 + -1*V >= 0 && H1 + U >= 0 && H1 + -1*U >= 0 && -1 + H1 + P >= 0 && 1 + H1 + -1*P >= 0 && -2 + H1 + O >= 0 && -2 + A + H1 >= 0 && -1*G1 >= 0 && D1 + -1*G1 >= 0 && -1*D1 + -1*G1 >= 0 && C1 + -1*G1 >= 0 && -1*C1 + -1*G1 >= 0 && -2 + A1 + -1*G1 >= 0 && -1*G1 + V >= 0 && -1*G1 + -1*V >= 0 && -1*G1 + U >= 0 && -1*G1 + -1*U >= 0 && -1 + -1*G1 + P >= 0 && 1 + -1*G1 + -1*P >= 0 && -2 + -1*G1 + O >= 0 && -2 + A + -1*G1 >= 0 && G1 >= 0 && D1 + G1 >= 0 && -1*D1 + G1 >= 0 && C1 + G1 >= 0 && -1*C1 + G1 >= 0 && -2 + A1 + G1 >= 0 && G1 + V >= 0 && G1 + -1*V >= 0 && G1 + U >= 0 && G1 + -1*U >= 0 && -1 + G1 + P >= 0 && 1 + G1 + -1*P >= 0 && -2 + G1 + O >= 0 && -2 + A + G1 >= 0 && -1 + C + -1*E1 >= 0 && B1 + -1*E1 >= 0 && -1*D1 >= 0 && C1 + -1*D1 >= 0 && -1*C1 + -1*D1 >= 0 && -2 + A1 + -1*D1 >= 0 && -1*D1 + V >= 0 && -1*D1 + -1*V >= 0 && -1*D1 + U >= 0 && -1*D1 + -1*U >= 0 && -1 + -1*D1 + P >= 0 && 1 + -1*D1 + -1*P >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && C1 + D1 >= 0 && -1*C1 + D1 >= 0 && -2 + A1 + D1 >= 0 && D1 + V >= 0 && D1 + -1*V >= 0 && D1 + U >= 0 && D1 + -1*U >= 0 && -1 + D1 + P >= 0 && 1 + D1 + -1*P >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && 1 + B1 + -1*C >= 0 && -1 + -1*B1 + C >= 0 && -1*C1 >= 0 && -2 + A1 + -1*C1 >= 0 && -1*C1 + V >= 0 && -1*C1 + -1*V >= 0 && -1*C1 + U >= 0 && -1*C1 + -1*U >= 0 && -1 + -1*C1 + P >= 0 && 1 + -1*C1 + -1*P >= 0 && -2 + -1*C1 + O >= 0 && -2 + A + -1*C1 >= 0 && C1 >= 0 && -2 + A1 + C1 >= 0 && C1 + V >= 0 && C1 + -1*V >= 0 && C1 + U >= 0 && C1 + -1*U >= 0 && -1 + C1 + P >= 0 && 1 + C1 + -1*P >= 0 && -2 + C1 + O >= 0 && -2 + A + C1 >= 0 && -2 + A1 >= 0 && -2 + A1 + V >= 0 && -2 + A1 + -1*V >= 0 && -2 + A1 + U >= 0 && -2 + A1 + -1*U >= 0 && -3 + A1 + P >= 0 && -1 + A1 + -1*P >= 0 && -4 + A1 + O >= 0 && -4 + A + A1 >= 0 && -1*A + A1 >= 0 && -1*V >= 0 && U + -1*V >= 0 && -1*U + -1*V >= 0 && -1 + P + -1*V >= 0 && 1 + -1*P + -1*V >= 0 && -2 + O + -1*V >= 0 && -2 + A + -1*V >= 0 && V >= 0 && U + V >= 0 && -1*U + V >= 0 && -1 + P + V >= 0 && 1 + -1*P + V >= 0 && -2 + O + V >= 0 && -2 + A + V >= 0 && -1*U >= 0 && -1 + P + -1*U >= 0 && 1 + -1*P + -1*U >= 0 && -2 + O + -1*U >= 0 && -2 + A + -1*U >= 0 && U >= 0 && -1 + P + U >= 0 && 1 + -1*P + U >= 0 && -2 + O + U >= 0 && -2 + A + U >= 0 && 1 + -1*P >= 0 && -1 + O + -1*P >= 0 && -1 + A + -1*P >= 0 && -1 + P >= 0 && -3 + O + P >= 0 && -3 + A + P >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && E1 >= 0 && G1 = D1] 2. f116(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f116(A,B,1 + C,D,E,-1 + F,G,H,I,J,K,L,M,N,F,1,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,U [-2 + C + F >= 0 (?,1) ,R1,S1,T1,U1,V1,W1,X1) ,1 + C,-1 + F,P1,Q1,R1,S1,T1,U1,V1,W1,X1) && -2 + F + P >= 0 && 2 + -1*T1 >= 0 && 2 + C + -1*T1 >= 0 && A1 + -1*T1 >= 0 && 2 + P + -1*T1 >= 0 && A + -1*T1 >= 0 && -2 + T1 >= 0 && -2 + C + T1 >= 0 && -4 + A1 + T1 >= 0 && -2 + P + T1 >= 0 && -4 + A + T1 >= 0 && -1*C + P >= 0 && C >= 0 && -2 + A1 + C >= 0 && C + P >= 0 && C + -1*P >= 0 && -2 + A + C >= 0 && -2 + A1 >= 0 && -2 + A1 + P >= 0 && -4 + A + A1 >= 0 && -1*A + A1 >= 0 && U + -1*V >= 0 && -1*U + V >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && A >= 2 && F >= 0 && P = 0 && U = M1] 3. f116(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f8(A,B,1 + E1,D,E,F,G,H,I,J,K,L,M,N,F,1,Q,R,S,T,0,V,W,X,Y,Z,A1,E1,V,V,E1,F1,0,V,0,V,K1,-1,M1,N1,O1,Z1,Q1[-2 + C + F >= 0 (1,1) ,R1,S1,T1,U1,V1,W1,X1) ,R1,S1,T1,U1,V1,W1,X1) && -2 + F + P >= 0 && 2 + -1*T1 >= 0 && 2 + C + -1*T1 >= 0 && A1 + -1*T1 >= 0 && 2 + P + -1*T1 >= 0 && A + -1*T1 >= 0 && -2 + T1 >= 0 && -2 + C + T1 >= 0 && -4 + A1 + T1 >= 0 && -2 + P + T1 >= 0 && -4 + A + T1 >= 0 && -1*C + P >= 0 && C >= 0 && -2 + A1 + C >= 0 && C + P >= 0 && C + -1*P >= 0 && -2 + A + C >= 0 && -2 + A1 >= 0 && -2 + A1 + P >= 0 && -4 + A + A1 >= 0 && -1*A + A1 >= 0 && U + -1*V >= 0 && -1*U + V >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && Z1 >= 0 && A >= 2 && F >= 0 && U = 0 && P = 0] 4. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f1(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,S,Z1,S,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1[2 + -1*T1 >= 0 (?,1) ,S1,T1,U1,V1,W1,X1) ,P1,Q1,R1,S1,T1,U1,V1,W1,X1) && B + -1*T1 >= 0 && Q + -1*T1 >= 0 && 2 + P + -1*T1 >= 0 && 2 + -1*P + -1*T1 >= 0 && -2 + T1 >= 0 && -4 + B + T1 >= 0 && -4 + Q + T1 >= 0 && -2 + P + T1 >= 0 && -2 + -1*P + T1 >= 0 && R + -1*T >= 0 && -1*R + T >= 0 && -1*B + Q >= 0 && -2 + B >= 0 && -4 + B + Q >= 0 && -2 + B + P >= 0 && -2 + B + -1*P >= 0 && -2 + Q >= 0 && -2 + P + Q >= 0 && -2 + -1*P + Q >= 0 && -1*P >= 0 && P >= 0 && B >= 0 && Q >= 1 + B] 5. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f116(A,Z1,0,D,E,F,G,H,I,J,K,L,M,N,O,P,A2,Y1,D2,B2,R,R,E2,F2,G2,Z1,C2,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1[2 + -1*T1 >= 0 (1,1) ,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1) && B + -1*T1 >= 0 && Q + -1*T1 >= 0 && 2 + P + -1*T1 >= 0 && 2 + -1*P + -1*T1 >= 0 && -2 + T1 >= 0 && -4 + B + T1 >= 0 && -4 + Q + T1 >= 0 && -2 + P + T1 >= 0 && -2 + -1*P + T1 >= 0 && R + -1*T >= 0 && -1*R + T >= 0 && -1*B + Q >= 0 && -2 + B >= 0 && -4 + B + Q >= 0 && -2 + B + P >= 0 && -2 + B + -1*P >= 0 && -2 + Q >= 0 && -2 + P + Q >= 0 && -2 + -1*P + Q >= 0 && -1*P >= 0 && P >= 0 && A >= 2 && C2 >= A && F >= A && B >= Q && B >= 0 && C = 0] 6. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f1(Z1,2,C,D,E,F,G,H,I,J,K,L,M,N,O,0,Z1,S,B2,S,U,V,S,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1 [Z1 >= 2 && S = W] (1,1) ,S1,T1,U1,V1,W1,X1) ,P1,A2,Y1,D2,2,E2,V1,W1,X1) 7. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(F2,E2,C,D,E,F,G,H,I,J,K,L,M,N,O,0,C2,H2,J2,I2,0,0,K2,L2,M2,Z,A1,B1,N2,D2,E1,F1,B2,Z1,A2,Y1,K1,L1,M1 [0 >= F2] (1,1) ,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,Q1,G2,S1,T1,U1,V1,W1,X1) 8. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(1,E2,C,D,E,F,G,H,I,J,K,L,M,N,O,0,H2,I2,K2,J2,0,0,M2,N2,O2,Z,A1,B1,Q2,D2,E1,F1,B2,Z1,A2,Y1,K1,L1,M1 [S = 0 && W = 0] (1,1) ,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,G2,C2,L2,T1,U1,F2,G2,P2) Signature: {(f1,50);(f10,50);(f116,50);(f8,50);(f9,50)} Flow Graph: [0->{0,1},1->{},2->{},3->{0,1},4->{4,5},5->{2,3},6->{4,5},7->{},8->{}] + Applied Processor: Looptree + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8] | +- p:[4] c: [4] | `- p:[0] c: [0] YES