MAYBE * Step 1: ArgumentFilter MAYBE + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f31(A,O2,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,0,S,T,0,V,W,X,0,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1[L2 >= 1] (1,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2) ,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,L2,0,O2,M2,N2,0) 1. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f31(A,M2,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,0,S,T,0,V,W,X,0,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1[0 >= L2] (1,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2) ,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,L2,0,M2,I2,J2,K2) 2. f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f67(A,B,C,D,E,F,G,M2,I,J,K,L,M,N,O,P,Q,0,S,T,0,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1[-1*G2 >= 0 (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2) ,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,L2,M2,F2,G2,H2,I2,J2,K2) && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*R >= 0 && R >= 0 && 0 >= B] 3. f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f42(A,-1 + B,L2,L2,M2,N2,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1 [-1*G2 >= 0 (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2) && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*R >= 0 && R >= 0 && B >= 1 && L2 >= 1 && M2 >= 1] 4. f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f42(A,-1 + B,L2,L2,M2,N2,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1 [-1*G2 >= 0 (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2) && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*R >= 0 && R >= 0 && B >= 1 && L2 >= 1 && 0 >= M2] 5. f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f31(A,-1 + B,L2,L2,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1[-1*G2 >= 0 (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2) ,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2) && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*R >= 0 && R >= 0 && 0 >= L2 && B >= 1] 6. f67(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f104(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,0,S,T,0,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1[-1*G2 >= 0 (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2) ,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,L2,C2,D2,E2,F2,G2,H2,I2,J2,K2) && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && 0 >= H] 7. f67(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f77(A,B,C,D,E,F,L2,-1 + H,M2,N2,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1 [-1*G2 >= 0 (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2) && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && H >= 1 && M2 >= 1] 8. f67(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f77(A,B,C,D,E,F,L2,-1 + H,M2,N2,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1 [-1*G2 >= 0 (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2) && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && H >= 1 && 0 >= M2] 9. f42(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1 [-1*G2 >= 0 (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2) ,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,D,D2,E2,F2,G2,H2,I2,J2,K2) && -1 + D + -1*G2 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && -1 + D + G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1 + D >= 0 && -1 + D + Y >= 0 && -1 + D + -1*Y >= 0 && -1 + D + U >= 0 && -1 + D + -1*U >= 0 && -1 + B + D >= 0 && -1 + D + R >= 0 && -1 + D + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && B >= 0 && B + R >= 0 && B + -1*R >= 0 && -1*R >= 0 && R >= 0 && F >= 1] 10. f42(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1 [-1*G2 >= 0 (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2) ,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,D,D2,E2,F2,G2,H2,I2,J2,K2) && -1 + D + -1*G2 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && -1 + D + G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1 + D >= 0 && -1 + D + Y >= 0 && -1 + D + -1*Y >= 0 && -1 + D + U >= 0 && -1 + D + -1*U >= 0 && -1 + B + D >= 0 && -1 + D + R >= 0 && -1 + D + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && B >= 0 && B + R >= 0 && B + -1*R >= 0 && -1*R >= 0 && R >= 0 && 0 >= F] 11. f104(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f104(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,0,S,T,0,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1[-1*H >= 0 (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2) ,Q1,R1,S1,L2,-1 + L2,V1,W1,M2,N2,O2,M2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2) && G2 + -1*H >= 0 && -1*G2 + -1*H >= 0 && -1*H + Y >= 0 && -1*H + -1*Y >= 0 && -1*H + U >= 0 && -1*H + -1*U >= 0 && -1*B + -1*H >= 0 && -1*H + R >= 0 && -1*H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && L2 >= 1] 12. f104(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f144(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,0,S,N2,0,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1 [-1*H >= 0 (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2) ,P1,Q1,R1,S1,L2,L2,M2,N2,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2) && G2 + -1*H >= 0 && -1*G2 + -1*H >= 0 && -1*H + Y >= 0 && -1*H + -1*Y >= 0 && -1*H + U >= 0 && -1*H + -1*U >= 0 && -1*B + -1*H >= 0 && -1*H + R >= 0 && -1*H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && 0 >= L2] 13. f77(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f81(L2,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1[H >= 0 (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2) ,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2) && G2 + H >= 0 && -1*G2 + H >= 0 && H + Y >= 0 && H + -1*Y >= 0 && H + U >= 0 && H + -1*U >= 0 && -1*B + H >= 0 && H + R >= 0 && H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && J >= 1] 14. f77(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f81(L2,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1[H >= 0 (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2) ,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2) && G2 + H >= 0 && -1*G2 + H >= 0 && H + Y >= 0 && H + -1*Y >= 0 && H + U >= 0 && H + -1*U >= 0 && -1*B + H >= 0 && H + R >= 0 && H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && 0 >= J] 15. f81(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f83(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1 [H >= 0 (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2) ,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2) && G2 + H >= 0 && -1*G2 + H >= 0 && H + Y >= 0 && H + -1*Y >= 0 && H + U >= 0 && H + -1*U >= 0 && -1*B + H >= 0 && H + R >= 0 && H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && A >= 1] 16. f81(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f83(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1 [H >= 0 (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2) ,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2) && G2 + H >= 0 && -1*G2 + H >= 0 && H + Y >= 0 && H + -1*Y >= 0 && H + U >= 0 && H + -1*U >= 0 && -1*B + H >= 0 && H + R >= 0 && H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && 0 >= A] 17. f144(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f172(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,0,S,-1 + T,U,V,W,0,Y,N2,A1,B1,C1,O2,E1,F1,G1,H1,I1,L2,L2,M2,P2,P2[-1*H >= 0 (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2) ,0,O2,O2,1,0,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2) && G2 + -1*H >= 0 && -1*G2 + -1*H >= 0 && -1*H + -1*U1 >= 0 && -1*H + Y >= 0 && -1*H + -1*Y >= 0 && -1*H + U >= 0 && -1*H + -1*U >= 0 && -1*B + -1*H >= 0 && -1*H + R >= 0 && -1*H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + -1*U1 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + -1*U1 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*U1 >= 0 && -1*U1 + Y >= 0 && -1*U1 + -1*Y >= 0 && U + -1*U1 >= 0 && -1*U + -1*U1 >= 0 && -1*B + -1*U1 >= 0 && R + -1*U1 >= 0 && -1*R + -1*U1 >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && O2 >= 1 && T >= 1 && L2 >= 1] 18. f144(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f172(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,0,S,-1 + T,U,V,W,0,Y,N2,A1,B1,C1,O2,E1,F1,G1,H1,I1,L2,L2,M2,P2,P2[-1*H >= 0 (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2) ,0,O2,O2,1,0,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2) && G2 + -1*H >= 0 && -1*G2 + -1*H >= 0 && -1*H + -1*U1 >= 0 && -1*H + Y >= 0 && -1*H + -1*Y >= 0 && -1*H + U >= 0 && -1*H + -1*U >= 0 && -1*B + -1*H >= 0 && -1*H + R >= 0 && -1*H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + -1*U1 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + -1*U1 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*U1 >= 0 && -1*U1 + Y >= 0 && -1*U1 + -1*Y >= 0 && U + -1*U1 >= 0 && -1*U + -1*U1 >= 0 && -1*B + -1*U1 >= 0 && R + -1*U1 >= 0 && -1*R + -1*U1 >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && 0 >= 1 + O2 && T >= 1 && L2 >= 1] 19. f144(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f144(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,0,S,-1 + T,0,V,W,X,Y,N2,A1,B1,C1,0,E1,F1,G1,H1,I1,L2,L2,M2,O2,O2 [-1*H >= 0 (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2) ,0,0,0,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2) && G2 + -1*H >= 0 && -1*G2 + -1*H >= 0 && -1*H + -1*U1 >= 0 && -1*H + Y >= 0 && -1*H + -1*Y >= 0 && -1*H + U >= 0 && -1*H + -1*U >= 0 && -1*B + -1*H >= 0 && -1*H + R >= 0 && -1*H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + -1*U1 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + -1*U1 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*U1 >= 0 && -1*U1 + Y >= 0 && -1*U1 + -1*Y >= 0 && U + -1*U1 >= 0 && -1*U + -1*U1 >= 0 && -1*B + -1*U1 >= 0 && R + -1*U1 >= 0 && -1*R + -1*U1 >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && T >= 1 && L2 >= 1] 20. f144(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f144(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,0,S,-1 + T,0,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,L2,L2,M2,M1,N1 [-1*H >= 0 (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2) ,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2) && G2 + -1*H >= 0 && -1*G2 + -1*H >= 0 && -1*H + -1*U1 >= 0 && -1*H + Y >= 0 && -1*H + -1*Y >= 0 && -1*H + U >= 0 && -1*H + -1*U >= 0 && -1*B + -1*H >= 0 && -1*H + R >= 0 && -1*H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + -1*U1 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + -1*U1 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*U1 >= 0 && -1*U1 + Y >= 0 && -1*U1 + -1*Y >= 0 && U + -1*U1 >= 0 && -1*U + -1*U1 >= 0 && -1*B + -1*U1 >= 0 && R + -1*U1 >= 0 && -1*R + -1*U1 >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && T >= 1 && 0 >= L2] 21. f144(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f211(A,B,C,D,E,F,G,H,I,J,M2,L,M,N,O,P,Q,0,S,T,0,L2,M2,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1[-1*H >= 0 (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2) ,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2) && G2 + -1*H >= 0 && -1*G2 + -1*H >= 0 && -1*H + -1*U1 >= 0 && -1*H + Y >= 0 && -1*H + -1*Y >= 0 && -1*H + U >= 0 && -1*H + -1*U >= 0 && -1*B + -1*H >= 0 && -1*H + R >= 0 && -1*H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + -1*U1 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + -1*U1 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*U1 >= 0 && -1*U1 + Y >= 0 && -1*U1 + -1*Y >= 0 && U + -1*U1 >= 0 && -1*U + -1*U1 >= 0 && -1*B + -1*U1 >= 0 && R + -1*U1 >= 0 && -1*R + -1*U1 >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && 0 >= T] 22. f83(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f67(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1 [H >= 0 (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2) ,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2) && G2 + H >= 0 && -1*G2 + H >= 0 && H + Y >= 0 && H + -1*Y >= 0 && H + U >= 0 && H + -1*U >= 0 && -1*B + H >= 0 && H + R >= 0 && H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && G >= 1] 23. f83(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f67(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1 [H >= 0 (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2) ,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2) && G2 + H >= 0 && -1*G2 + H >= 0 && H + Y >= 0 && H + -1*Y >= 0 && H + U >= 0 && H + -1*U >= 0 && -1*B + H >= 0 && H + R >= 0 && H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && 0 >= G] 24. f172(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f144(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,0,V,W,X,Y,X,A1,B1,C1,D1,E1,F1,G1,H1,D1,J1,K1,L1,M1,N1,O1,P1[-1*H >= 0 (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2) ,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2) && G2 + -1*H >= 0 && -1*G2 + -1*H >= 0 && -1*H + -1*U1 >= 0 && -1*H + S1 >= 0 && -1*H + -1*S1 >= 0 && -1 + -1*H + R1 >= 0 && 1 + -1*H + -1*R1 >= 0 && -1*H + O1 >= 0 && -1*H + -1*O1 >= 0 && -1 + -1*H + K1 >= 0 && -1*H + Y >= 0 && -1*H + -1*Y >= 0 && -1*H + X >= 0 && -1*H + -1*X >= 0 && -1*H + U >= 0 && -1*H + -1*U >= 0 && -1*H + T >= 0 && -1*B + -1*H >= 0 && -1*H + R >= 0 && -1*H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + -1*U1 >= 0 && -1*G2 + S1 >= 0 && -1*G2 + -1*S1 >= 0 && -1 + -1*G2 + R1 >= 0 && 1 + -1*G2 + -1*R1 >= 0 && -1*G2 + O1 >= 0 && -1*G2 + -1*O1 >= 0 && -1 + -1*G2 + K1 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + X >= 0 && -1*G2 + -1*X >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*G2 + T >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + -1*U1 >= 0 && G2 + S1 >= 0 && G2 + -1*S1 >= 0 && -1 + G2 + R1 >= 0 && 1 + G2 + -1*R1 >= 0 && G2 + O1 >= 0 && G2 + -1*O1 >= 0 && -1 + G2 + K1 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + X >= 0 && G2 + -1*X >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && G2 + T >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*U1 >= 0 && S1 + -1*U1 >= 0 && -1*S1 + -1*U1 >= 0 && -1 + R1 + -1*U1 >= 0 && 1 + -1*R1 + -1*U1 >= 0 && O1 + -1*U1 >= 0 && -1*O1 + -1*U1 >= 0 && -1 + K1 + -1*U1 >= 0 && -1*U1 + Y >= 0 && -1*U1 + -1*Y >= 0 && -1*U1 + X >= 0 && -1*U1 + -1*X >= 0 && U + -1*U1 >= 0 && -1*U + -1*U1 >= 0 && T + -1*U1 >= 0 && -1*B + -1*U1 >= 0 && R + -1*U1 >= 0 && -1*R + -1*U1 >= 0 && -1*S1 >= 0 && -1 + R1 + -1*S1 >= 0 && 1 + -1*R1 + -1*S1 >= 0 && O1 + -1*S1 >= 0 && -1*O1 + -1*S1 >= 0 && -1 + K1 + -1*S1 >= 0 && -1*S1 + Y >= 0 && -1*S1 + -1*Y >= 0 && -1*S1 + X >= 0 && -1*S1 + -1*X >= 0 && -1*S1 + U >= 0 && -1*S1 + -1*U >= 0 && -1*S1 + T >= 0 && -1*B + -1*S1 >= 0 && R + -1*S1 >= 0 && -1*R + -1*S1 >= 0 && S1 >= 0 && -1 + R1 + S1 >= 0 && 1 + -1*R1 + S1 >= 0 && O1 + S1 >= 0 && -1*O1 + S1 >= 0 && -1 + K1 + S1 >= 0 && S1 + Y >= 0 && S1 + -1*Y >= 0 && S1 + X >= 0 && S1 + -1*X >= 0 && S1 + U >= 0 && S1 + -1*U >= 0 && S1 + T >= 0 && -1*B + S1 >= 0 && R + S1 >= 0 && -1*R + S1 >= 0 && 1 + -1*R1 >= 0 && 1 + O1 + -1*R1 >= 0 && 1 + -1*O1 + -1*R1 >= 0 && K1 + -1*R1 >= 0 && 1 + -1*R1 + Y >= 0 && 1 + -1*R1 + -1*Y >= 0 && 1 + -1*R1 + X >= 0 && 1 + -1*R1 + -1*X >= 0 && 1 + -1*R1 + U >= 0 && 1 + -1*R1 + -1*U >= 0 && 1 + -1*R1 + T >= 0 && 1 + -1*B + -1*R1 >= 0 && 1 + R + -1*R1 >= 0 && 1 + -1*R + -1*R1 >= 0 && -1 + R1 >= 0 && -1 + O1 + R1 >= 0 && -1 + -1*O1 + R1 >= 0 && -2 + K1 + R1 >= 0 && -1 + R1 + Y >= 0 && -1 + R1 + -1*Y >= 0 && -1 + R1 + X >= 0 && -1 + R1 + -1*X >= 0 && -1 + R1 + U >= 0 && -1 + R1 + -1*U >= 0 && -1 + R1 + T >= 0 && -1 + -1*B + R1 >= 0 && -1 + R + R1 >= 0 && -1 + -1*R + R1 >= 0 && -1*O1 >= 0 && -1 + K1 + -1*O1 >= 0 && -1*O1 + Y >= 0 && -1*O1 + -1*Y >= 0 && -1*O1 + X >= 0 && -1*O1 + -1*X >= 0 && -1*O1 + U >= 0 && -1*O1 + -1*U >= 0 && -1*O1 + T >= 0 && -1*B + -1*O1 >= 0 && -1*O1 + R >= 0 && -1*O1 + -1*R >= 0 && O1 >= 0 && -1 + K1 + O1 >= 0 && O1 + Y >= 0 && O1 + -1*Y >= 0 && O1 + X >= 0 && O1 + -1*X >= 0 && O1 + U >= 0 && O1 + -1*U >= 0 && O1 + T >= 0 && -1*B + O1 >= 0 && O1 + R >= 0 && O1 + -1*R >= 0 && -1 + K1 >= 0 && -1 + K1 + Y >= 0 && -1 + K1 + -1*Y >= 0 && -1 + K1 + X >= 0 && -1 + K1 + -1*X >= 0 && -1 + K1 + U >= 0 && -1 + K1 + -1*U >= 0 && -1 + K1 + T >= 0 && -1 + -1*B + K1 >= 0 && -1 + K1 + R >= 0 && -1 + K1 + -1*R >= 0 && -1*Y >= 0 && X + -1*Y >= 0 && -1*X + -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && T + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && X + Y >= 0 && -1*X + Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && T + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*X >= 0 && U + -1*X >= 0 && -1*U + -1*X >= 0 && T + -1*X >= 0 && -1*B + -1*X >= 0 && R + -1*X >= 0 && -1*R + -1*X >= 0 && X >= 0 && U + X >= 0 && -1*U + X >= 0 && T + X >= 0 && -1*B + X >= 0 && R + X >= 0 && -1*R + X >= 0 && -1*U >= 0 && T + -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && T + U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && T >= 0 && -1*B + T >= 0 && R + T >= 0 && -1*R + T >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && 0 >= X] 25. f211(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f235(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,0,L2,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1 [-1*H >= 0 (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2) ,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2) && G2 + -1*H >= 0 && -1*G2 + -1*H >= 0 && -1*H + -1*U1 >= 0 && -1*H + Y >= 0 && -1*H + -1*Y >= 0 && -1*H + U >= 0 && -1*H + -1*U >= 0 && -1*H + -1*T >= 0 && -1*B + -1*H >= 0 && -1*H + R >= 0 && -1*H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + -1*U1 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*G2 + -1*T >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + -1*U1 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && G2 + -1*T >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*U1 >= 0 && -1*U1 + Y >= 0 && -1*U1 + -1*Y >= 0 && U + -1*U1 >= 0 && -1*U + -1*U1 >= 0 && -1*T + -1*U1 >= 0 && -1*B + -1*U1 >= 0 && R + -1*U1 >= 0 && -1*R + -1*U1 >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*T + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*T + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*T + -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*T + U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*T >= 0 && -1*B + -1*T >= 0 && R + -1*T >= 0 && -1*R + -1*T >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && 0 >= K] 26. f211(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f211(A,B,C,D,E,F,G,H,I,J,-1 + K,0,L2,0,0,2,L2,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1 [-1*H >= 0 (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2) && G2 + -1*H >= 0 && -1*G2 + -1*H >= 0 && -1*H + -1*U1 >= 0 && -1*H + Y >= 0 && -1*H + -1*Y >= 0 && -1*H + U >= 0 && -1*H + -1*U >= 0 && -1*H + -1*T >= 0 && -1*B + -1*H >= 0 && -1*H + R >= 0 && -1*H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + -1*U1 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*G2 + -1*T >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + -1*U1 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && G2 + -1*T >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*U1 >= 0 && -1*U1 + Y >= 0 && -1*U1 + -1*Y >= 0 && U + -1*U1 >= 0 && -1*U + -1*U1 >= 0 && -1*T + -1*U1 >= 0 && -1*B + -1*U1 >= 0 && R + -1*U1 >= 0 && -1*R + -1*U1 >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*T + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*T + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*T + -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*T + U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*T >= 0 && -1*B + -1*T >= 0 && R + -1*T >= 0 && -1*R + -1*T >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && K >= 1] 27. f235(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f235(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1[-1*H >= 0 (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2) ,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2) && G2 + -1*H >= 0 && -1*G2 + -1*H >= 0 && -1*H + -1*U1 >= 0 && -1*H + Y >= 0 && -1*H + -1*Y >= 0 && -1*H + U >= 0 && -1*H + -1*U >= 0 && -1*H + -1*T >= 0 && -1*B + -1*H >= 0 && -1*H + R >= 0 && -1*H + -1*R >= 0 && -1*H + -1*K >= 0 && -1*G2 >= 0 && -1*G2 + -1*U1 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*G2 + -1*T >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && -1*G2 + -1*K >= 0 && G2 >= 0 && G2 + -1*U1 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && G2 + -1*T >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && G2 + -1*K >= 0 && -1*U1 >= 0 && -1*U1 + Y >= 0 && -1*U1 + -1*Y >= 0 && U + -1*U1 >= 0 && -1*U + -1*U1 >= 0 && -1*T + -1*U1 >= 0 && -1*B + -1*U1 >= 0 && R + -1*U1 >= 0 && -1*R + -1*U1 >= 0 && -1*K + -1*U1 >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*T + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && -1*K + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*T + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*K + Y >= 0 && -1*U >= 0 && -1*T + -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && -1*K + -1*U >= 0 && U >= 0 && -1*T + U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*K + U >= 0 && -1*T >= 0 && -1*B + -1*T >= 0 && R + -1*T >= 0 && -1*R + -1*T >= 0 && -1*K + -1*T >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*B + -1*K >= 0 && -1*R >= 0 && -1*K + -1*R >= 0 && R >= 0 && -1*K + R >= 0 && -1*K >= 0] Signature: {(f0,63) ;(f104,63) ;(f144,63) ;(f172,63) ;(f211,63) ;(f235,63) ;(f31,63) ;(f42,63) ;(f67,63) ;(f77,63) ;(f81,63) ;(f83,63)} Flow Graph: [0->{2,3,4,5},1->{2,3,4,5},2->{6,7,8},3->{9,10},4->{9,10},5->{2,3,4,5},6->{11,12},7->{13,14},8->{13,14} ,9->{2,3,4,5},10->{2,3,4,5},11->{11,12},12->{17,18,19,20,21},13->{15,16},14->{15,16},15->{22,23},16->{22,23} ,17->{24},18->{24},19->{17,18,19,20,21},20->{17,18,19,20,21},21->{25,26},22->{6,7,8},23->{6,7,8},24->{17,18 ,19,20,21},25->{27},26->{25,26},27->{27}] + Applied Processor: ArgumentFilter [2,4,8,11,12,13,14,15,16,18,21,22,25,26,27,28,29,30,31,32,33,34,35,37,38,39,41,42,45,47,48,49,50,51,52,53,54,55,56,57,59,60,61,62] + Details: We remove following argument positions: [2 ,4 ,8 ,11 ,12 ,13 ,14 ,15 ,16 ,18 ,21 ,22 ,25 ,26 ,27 ,28 ,29 ,30 ,31 ,32 ,33 ,34 ,35 ,37 ,38 ,39 ,41 ,42 ,45 ,47 ,48 ,49 ,50 ,51 ,52 ,53 ,54 ,55 ,56 ,57 ,59 ,60 ,61 ,62]. * Step 2: TrivialSCCs MAYBE + Considered Problem: Rules: 0. f0(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f31(A,O2,D,F,G,H,J,K,0,T,0,X,0,K1,O1,R1,S1,U1,0) [L2 >= 1] (1,1) 1. f0(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f31(A,M2,D,F,G,H,J,K,0,T,0,X,0,K1,O1,R1,S1,U1,0) [0 >= L2] (1,1) 2. f31(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f67(A,B,D,F,G,M2,J,K,0,T,0,X,Y,K1,O1,R1,S1,U1,G2) [-1*G2 >= 0 (?,1) && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*R >= 0 && R >= 0 && 0 >= B] 3. f31(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f42(A,-1 + B,L2,N2,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) [-1*G2 >= 0 (?,1) && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*R >= 0 && R >= 0 && B >= 1 && L2 >= 1 && M2 >= 1] 4. f31(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f42(A,-1 + B,L2,N2,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) [-1*G2 >= 0 (?,1) && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*R >= 0 && R >= 0 && B >= 1 && L2 >= 1 && 0 >= M2] 5. f31(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f31(A,-1 + B,L2,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) [-1*G2 >= 0 (?,1) && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*R >= 0 && R >= 0 && 0 >= L2 && B >= 1] 6. f67(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f104(A,B,D,F,G,H,J,K,0,T,0,X,Y,K1,O1,R1,S1,U1,G2) [-1*G2 >= 0 (?,1) && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && 0 >= H] 7. f67(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f77(A,B,D,F,L2,-1 + H,N2,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) [-1*G2 >= 0 (?,1) && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && H >= 1 && M2 >= 1] 8. f67(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f77(A,B,D,F,L2,-1 + H,N2,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) [-1*G2 >= 0 (?,1) && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && H >= 1 && 0 >= M2] 9. f42(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f31(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) [-1*G2 >= 0 (?,1) && -1 + D + -1*G2 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && -1 + D + G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1 + D >= 0 && -1 + D + Y >= 0 && -1 + D + -1*Y >= 0 && -1 + D + U >= 0 && -1 + D + -1*U >= 0 && -1 + B + D >= 0 && -1 + D + R >= 0 && -1 + D + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && B >= 0 && B + R >= 0 && B + -1*R >= 0 && -1*R >= 0 && R >= 0 && F >= 1] 10. f42(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f31(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) [-1*G2 >= 0 (?,1) && -1 + D + -1*G2 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && -1 + D + G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1 + D >= 0 && -1 + D + Y >= 0 && -1 + D + -1*Y >= 0 && -1 + D + U >= 0 && -1 + D + -1*U >= 0 && -1 + B + D >= 0 && -1 + D + R >= 0 && -1 + D + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && B >= 0 && B + R >= 0 && B + -1*R >= 0 && -1*R >= 0 && R >= 0 && 0 >= F] 11. f104(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f104(A,B,D,F,G,H,J,K,0,T,0,X,Y,K1,O1,R1,S1,-1 + L2,G2) [-1*H >= 0 (?,1) && G2 + -1*H >= 0 && -1*G2 + -1*H >= 0 && -1*H + Y >= 0 && -1*H + -1*Y >= 0 && -1*H + U >= 0 && -1*H + -1*U >= 0 && -1*B + -1*H >= 0 && -1*H + R >= 0 && -1*H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && L2 >= 1] 12. f104(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f144(A,B,D,F,G,H,J,K,0,N2,0,X,Y,K1,O1,R1,S1,L2,G2) [-1*H >= 0 (?,1) && G2 + -1*H >= 0 && -1*G2 + -1*H >= 0 && -1*H + Y >= 0 && -1*H + -1*Y >= 0 && -1*H + U >= 0 && -1*H + -1*U >= 0 && -1*B + -1*H >= 0 && -1*H + R >= 0 && -1*H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && 0 >= L2] 13. f77(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f81(L2,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) [H >= 0 (?,1) && G2 + H >= 0 && -1*G2 + H >= 0 && H + Y >= 0 && H + -1*Y >= 0 && H + U >= 0 && H + -1*U >= 0 && -1*B + H >= 0 && H + R >= 0 && H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && J >= 1] 14. f77(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f81(L2,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) [H >= 0 (?,1) && G2 + H >= 0 && -1*G2 + H >= 0 && H + Y >= 0 && H + -1*Y >= 0 && H + U >= 0 && H + -1*U >= 0 && -1*B + H >= 0 && H + R >= 0 && H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && 0 >= J] 15. f81(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f83(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) [H >= 0 (?,1) && G2 + H >= 0 && -1*G2 + H >= 0 && H + Y >= 0 && H + -1*Y >= 0 && H + U >= 0 && H + -1*U >= 0 && -1*B + H >= 0 && H + R >= 0 && H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && A >= 1] 16. f81(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f83(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) [H >= 0 (?,1) && G2 + H >= 0 && -1*G2 + H >= 0 && H + Y >= 0 && H + -1*Y >= 0 && H + U >= 0 && H + -1*U >= 0 && -1*B + H >= 0 && H + R >= 0 && H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && 0 >= A] 17. f144(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f172(A,B,D,F,G,H,J,K,0,-1 + T,U,0,Y,L2,0,1,0,U1,G2) [-1*H >= 0 (?,1) && G2 + -1*H >= 0 && -1*G2 + -1*H >= 0 && -1*H + -1*U1 >= 0 && -1*H + Y >= 0 && -1*H + -1*Y >= 0 && -1*H + U >= 0 && -1*H + -1*U >= 0 && -1*B + -1*H >= 0 && -1*H + R >= 0 && -1*H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + -1*U1 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + -1*U1 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*U1 >= 0 && -1*U1 + Y >= 0 && -1*U1 + -1*Y >= 0 && U + -1*U1 >= 0 && -1*U + -1*U1 >= 0 && -1*B + -1*U1 >= 0 && R + -1*U1 >= 0 && -1*R + -1*U1 >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && O2 >= 1 && T >= 1 && L2 >= 1] 18. f144(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f172(A,B,D,F,G,H,J,K,0,-1 + T,U,0,Y,L2,0,1,0,U1,G2) [-1*H >= 0 (?,1) && G2 + -1*H >= 0 && -1*G2 + -1*H >= 0 && -1*H + -1*U1 >= 0 && -1*H + Y >= 0 && -1*H + -1*Y >= 0 && -1*H + U >= 0 && -1*H + -1*U >= 0 && -1*B + -1*H >= 0 && -1*H + R >= 0 && -1*H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + -1*U1 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + -1*U1 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*U1 >= 0 && -1*U1 + Y >= 0 && -1*U1 + -1*Y >= 0 && U + -1*U1 >= 0 && -1*U + -1*U1 >= 0 && -1*B + -1*U1 >= 0 && R + -1*U1 >= 0 && -1*R + -1*U1 >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && 0 >= 1 + O2 && T >= 1 && L2 >= 1] 19. f144(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f144(A,B,D,F,G,H,J,K,0,-1 + T,0,X,Y,L2,0,R1,S1,U1,G2) [-1*H >= 0 (?,1) && G2 + -1*H >= 0 && -1*G2 + -1*H >= 0 && -1*H + -1*U1 >= 0 && -1*H + Y >= 0 && -1*H + -1*Y >= 0 && -1*H + U >= 0 && -1*H + -1*U >= 0 && -1*B + -1*H >= 0 && -1*H + R >= 0 && -1*H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + -1*U1 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + -1*U1 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*U1 >= 0 && -1*U1 + Y >= 0 && -1*U1 + -1*Y >= 0 && U + -1*U1 >= 0 && -1*U + -1*U1 >= 0 && -1*B + -1*U1 >= 0 && R + -1*U1 >= 0 && -1*R + -1*U1 >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && T >= 1 && L2 >= 1] 20. f144(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f144(A,B,D,F,G,H,J,K,0,-1 + T,0,X,Y,L2,O1,R1,S1,U1,G2) [-1*H >= 0 (?,1) && G2 + -1*H >= 0 && -1*G2 + -1*H >= 0 && -1*H + -1*U1 >= 0 && -1*H + Y >= 0 && -1*H + -1*Y >= 0 && -1*H + U >= 0 && -1*H + -1*U >= 0 && -1*B + -1*H >= 0 && -1*H + R >= 0 && -1*H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + -1*U1 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + -1*U1 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*U1 >= 0 && -1*U1 + Y >= 0 && -1*U1 + -1*Y >= 0 && U + -1*U1 >= 0 && -1*U + -1*U1 >= 0 && -1*B + -1*U1 >= 0 && R + -1*U1 >= 0 && -1*R + -1*U1 >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && T >= 1 && 0 >= L2] 21. f144(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f211(A,B,D,F,G,H,J,M2,0,T,0,X,Y,K1,O1,R1,S1,U1,G2) [-1*H >= 0 (?,1) && G2 + -1*H >= 0 && -1*G2 + -1*H >= 0 && -1*H + -1*U1 >= 0 && -1*H + Y >= 0 && -1*H + -1*Y >= 0 && -1*H + U >= 0 && -1*H + -1*U >= 0 && -1*B + -1*H >= 0 && -1*H + R >= 0 && -1*H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + -1*U1 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + -1*U1 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*U1 >= 0 && -1*U1 + Y >= 0 && -1*U1 + -1*Y >= 0 && U + -1*U1 >= 0 && -1*U + -1*U1 >= 0 && -1*B + -1*U1 >= 0 && R + -1*U1 >= 0 && -1*R + -1*U1 >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && 0 >= T] 22. f83(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f67(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) [H >= 0 (?,1) && G2 + H >= 0 && -1*G2 + H >= 0 && H + Y >= 0 && H + -1*Y >= 0 && H + U >= 0 && H + -1*U >= 0 && -1*B + H >= 0 && H + R >= 0 && H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && G >= 1] 23. f83(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f67(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) [H >= 0 (?,1) && G2 + H >= 0 && -1*G2 + H >= 0 && H + Y >= 0 && H + -1*Y >= 0 && H + U >= 0 && H + -1*U >= 0 && -1*B + H >= 0 && H + R >= 0 && H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && 0 >= G] 24. f172(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f144(A,B,D,F,G,H,J,K,R,T,0,X,Y,K1,O1,R1,S1,U1,G2) [-1*H >= 0 (?,1) && G2 + -1*H >= 0 && -1*G2 + -1*H >= 0 && -1*H + -1*U1 >= 0 && -1*H + S1 >= 0 && -1*H + -1*S1 >= 0 && -1 + -1*H + R1 >= 0 && 1 + -1*H + -1*R1 >= 0 && -1*H + O1 >= 0 && -1*H + -1*O1 >= 0 && -1 + -1*H + K1 >= 0 && -1*H + Y >= 0 && -1*H + -1*Y >= 0 && -1*H + X >= 0 && -1*H + -1*X >= 0 && -1*H + U >= 0 && -1*H + -1*U >= 0 && -1*H + T >= 0 && -1*B + -1*H >= 0 && -1*H + R >= 0 && -1*H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + -1*U1 >= 0 && -1*G2 + S1 >= 0 && -1*G2 + -1*S1 >= 0 && -1 + -1*G2 + R1 >= 0 && 1 + -1*G2 + -1*R1 >= 0 && -1*G2 + O1 >= 0 && -1*G2 + -1*O1 >= 0 && -1 + -1*G2 + K1 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + X >= 0 && -1*G2 + -1*X >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*G2 + T >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + -1*U1 >= 0 && G2 + S1 >= 0 && G2 + -1*S1 >= 0 && -1 + G2 + R1 >= 0 && 1 + G2 + -1*R1 >= 0 && G2 + O1 >= 0 && G2 + -1*O1 >= 0 && -1 + G2 + K1 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + X >= 0 && G2 + -1*X >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && G2 + T >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*U1 >= 0 && S1 + -1*U1 >= 0 && -1*S1 + -1*U1 >= 0 && -1 + R1 + -1*U1 >= 0 && 1 + -1*R1 + -1*U1 >= 0 && O1 + -1*U1 >= 0 && -1*O1 + -1*U1 >= 0 && -1 + K1 + -1*U1 >= 0 && -1*U1 + Y >= 0 && -1*U1 + -1*Y >= 0 && -1*U1 + X >= 0 && -1*U1 + -1*X >= 0 && U + -1*U1 >= 0 && -1*U + -1*U1 >= 0 && T + -1*U1 >= 0 && -1*B + -1*U1 >= 0 && R + -1*U1 >= 0 && -1*R + -1*U1 >= 0 && -1*S1 >= 0 && -1 + R1 + -1*S1 >= 0 && 1 + -1*R1 + -1*S1 >= 0 && O1 + -1*S1 >= 0 && -1*O1 + -1*S1 >= 0 && -1 + K1 + -1*S1 >= 0 && -1*S1 + Y >= 0 && -1*S1 + -1*Y >= 0 && -1*S1 + X >= 0 && -1*S1 + -1*X >= 0 && -1*S1 + U >= 0 && -1*S1 + -1*U >= 0 && -1*S1 + T >= 0 && -1*B + -1*S1 >= 0 && R + -1*S1 >= 0 && -1*R + -1*S1 >= 0 && S1 >= 0 && -1 + R1 + S1 >= 0 && 1 + -1*R1 + S1 >= 0 && O1 + S1 >= 0 && -1*O1 + S1 >= 0 && -1 + K1 + S1 >= 0 && S1 + Y >= 0 && S1 + -1*Y >= 0 && S1 + X >= 0 && S1 + -1*X >= 0 && S1 + U >= 0 && S1 + -1*U >= 0 && S1 + T >= 0 && -1*B + S1 >= 0 && R + S1 >= 0 && -1*R + S1 >= 0 && 1 + -1*R1 >= 0 && 1 + O1 + -1*R1 >= 0 && 1 + -1*O1 + -1*R1 >= 0 && K1 + -1*R1 >= 0 && 1 + -1*R1 + Y >= 0 && 1 + -1*R1 + -1*Y >= 0 && 1 + -1*R1 + X >= 0 && 1 + -1*R1 + -1*X >= 0 && 1 + -1*R1 + U >= 0 && 1 + -1*R1 + -1*U >= 0 && 1 + -1*R1 + T >= 0 && 1 + -1*B + -1*R1 >= 0 && 1 + R + -1*R1 >= 0 && 1 + -1*R + -1*R1 >= 0 && -1 + R1 >= 0 && -1 + O1 + R1 >= 0 && -1 + -1*O1 + R1 >= 0 && -2 + K1 + R1 >= 0 && -1 + R1 + Y >= 0 && -1 + R1 + -1*Y >= 0 && -1 + R1 + X >= 0 && -1 + R1 + -1*X >= 0 && -1 + R1 + U >= 0 && -1 + R1 + -1*U >= 0 && -1 + R1 + T >= 0 && -1 + -1*B + R1 >= 0 && -1 + R + R1 >= 0 && -1 + -1*R + R1 >= 0 && -1*O1 >= 0 && -1 + K1 + -1*O1 >= 0 && -1*O1 + Y >= 0 && -1*O1 + -1*Y >= 0 && -1*O1 + X >= 0 && -1*O1 + -1*X >= 0 && -1*O1 + U >= 0 && -1*O1 + -1*U >= 0 && -1*O1 + T >= 0 && -1*B + -1*O1 >= 0 && -1*O1 + R >= 0 && -1*O1 + -1*R >= 0 && O1 >= 0 && -1 + K1 + O1 >= 0 && O1 + Y >= 0 && O1 + -1*Y >= 0 && O1 + X >= 0 && O1 + -1*X >= 0 && O1 + U >= 0 && O1 + -1*U >= 0 && O1 + T >= 0 && -1*B + O1 >= 0 && O1 + R >= 0 && O1 + -1*R >= 0 && -1 + K1 >= 0 && -1 + K1 + Y >= 0 && -1 + K1 + -1*Y >= 0 && -1 + K1 + X >= 0 && -1 + K1 + -1*X >= 0 && -1 + K1 + U >= 0 && -1 + K1 + -1*U >= 0 && -1 + K1 + T >= 0 && -1 + -1*B + K1 >= 0 && -1 + K1 + R >= 0 && -1 + K1 + -1*R >= 0 && -1*Y >= 0 && X + -1*Y >= 0 && -1*X + -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && T + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && X + Y >= 0 && -1*X + Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && T + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*X >= 0 && U + -1*X >= 0 && -1*U + -1*X >= 0 && T + -1*X >= 0 && -1*B + -1*X >= 0 && R + -1*X >= 0 && -1*R + -1*X >= 0 && X >= 0 && U + X >= 0 && -1*U + X >= 0 && T + X >= 0 && -1*B + X >= 0 && R + X >= 0 && -1*R + X >= 0 && -1*U >= 0 && T + -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && T + U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && T >= 0 && -1*B + T >= 0 && R + T >= 0 && -1*R + T >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && 0 >= X] 25. f211(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f235(A,B,D,F,G,H,J,K,0,T,U,X,Y,K1,O1,R1,S1,U1,G2) [-1*H >= 0 (?,1) && G2 + -1*H >= 0 && -1*G2 + -1*H >= 0 && -1*H + -1*U1 >= 0 && -1*H + Y >= 0 && -1*H + -1*Y >= 0 && -1*H + U >= 0 && -1*H + -1*U >= 0 && -1*H + -1*T >= 0 && -1*B + -1*H >= 0 && -1*H + R >= 0 && -1*H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + -1*U1 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*G2 + -1*T >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + -1*U1 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && G2 + -1*T >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*U1 >= 0 && -1*U1 + Y >= 0 && -1*U1 + -1*Y >= 0 && U + -1*U1 >= 0 && -1*U + -1*U1 >= 0 && -1*T + -1*U1 >= 0 && -1*B + -1*U1 >= 0 && R + -1*U1 >= 0 && -1*R + -1*U1 >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*T + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*T + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*T + -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*T + U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*T >= 0 && -1*B + -1*T >= 0 && R + -1*T >= 0 && -1*R + -1*T >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && 0 >= K] 26. f211(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f211(A,B,D,F,G,H,J,-1 + K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) [-1*H >= 0 (?,1) && G2 + -1*H >= 0 && -1*G2 + -1*H >= 0 && -1*H + -1*U1 >= 0 && -1*H + Y >= 0 && -1*H + -1*Y >= 0 && -1*H + U >= 0 && -1*H + -1*U >= 0 && -1*H + -1*T >= 0 && -1*B + -1*H >= 0 && -1*H + R >= 0 && -1*H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + -1*U1 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*G2 + -1*T >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + -1*U1 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && G2 + -1*T >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*U1 >= 0 && -1*U1 + Y >= 0 && -1*U1 + -1*Y >= 0 && U + -1*U1 >= 0 && -1*U + -1*U1 >= 0 && -1*T + -1*U1 >= 0 && -1*B + -1*U1 >= 0 && R + -1*U1 >= 0 && -1*R + -1*U1 >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*T + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*T + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*T + -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*T + U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*T >= 0 && -1*B + -1*T >= 0 && R + -1*T >= 0 && -1*R + -1*T >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && K >= 1] 27. f235(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f235(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) [-1*H >= 0 (?,1) && G2 + -1*H >= 0 && -1*G2 + -1*H >= 0 && -1*H + -1*U1 >= 0 && -1*H + Y >= 0 && -1*H + -1*Y >= 0 && -1*H + U >= 0 && -1*H + -1*U >= 0 && -1*H + -1*T >= 0 && -1*B + -1*H >= 0 && -1*H + R >= 0 && -1*H + -1*R >= 0 && -1*H + -1*K >= 0 && -1*G2 >= 0 && -1*G2 + -1*U1 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*G2 + -1*T >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && -1*G2 + -1*K >= 0 && G2 >= 0 && G2 + -1*U1 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && G2 + -1*T >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && G2 + -1*K >= 0 && -1*U1 >= 0 && -1*U1 + Y >= 0 && -1*U1 + -1*Y >= 0 && U + -1*U1 >= 0 && -1*U + -1*U1 >= 0 && -1*T + -1*U1 >= 0 && -1*B + -1*U1 >= 0 && R + -1*U1 >= 0 && -1*R + -1*U1 >= 0 && -1*K + -1*U1 >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*T + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && -1*K + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*T + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*K + Y >= 0 && -1*U >= 0 && -1*T + -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && -1*K + -1*U >= 0 && U >= 0 && -1*T + U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*K + U >= 0 && -1*T >= 0 && -1*B + -1*T >= 0 && R + -1*T >= 0 && -1*R + -1*T >= 0 && -1*K + -1*T >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*B + -1*K >= 0 && -1*R >= 0 && -1*K + -1*R >= 0 && R >= 0 && -1*K + R >= 0 && -1*K >= 0] Signature: {(f0,63) ;(f104,63) ;(f144,63) ;(f172,63) ;(f211,63) ;(f235,63) ;(f31,63) ;(f42,63) ;(f67,63) ;(f77,63) ;(f81,63) ;(f83,63)} Flow Graph: [0->{2,3,4,5},1->{2,3,4,5},2->{6,7,8},3->{9,10},4->{9,10},5->{2,3,4,5},6->{11,12},7->{13,14},8->{13,14} ,9->{2,3,4,5},10->{2,3,4,5},11->{11,12},12->{17,18,19,20,21},13->{15,16},14->{15,16},15->{22,23},16->{22,23} ,17->{24},18->{24},19->{17,18,19,20,21},20->{17,18,19,20,21},21->{25,26},22->{6,7,8},23->{6,7,8},24->{17,18 ,19,20,21},25->{27},26->{25,26},27->{27}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 3: AddSinks MAYBE + Considered Problem: Rules: 0. f0(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f31(A,O2,D,F,G,H,J,K,0,T,0,X,0,K1,O1,R1,S1,U1,0) [L2 >= 1] (1,1) 1. f0(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f31(A,M2,D,F,G,H,J,K,0,T,0,X,0,K1,O1,R1,S1,U1,0) [0 >= L2] (1,1) 2. f31(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f67(A,B,D,F,G,M2,J,K,0,T,0,X,Y,K1,O1,R1,S1,U1,G2) [-1*G2 >= 0 (1,1) && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*R >= 0 && R >= 0 && 0 >= B] 3. f31(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f42(A,-1 + B,L2,N2,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) [-1*G2 >= 0 (?,1) && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*R >= 0 && R >= 0 && B >= 1 && L2 >= 1 && M2 >= 1] 4. f31(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f42(A,-1 + B,L2,N2,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) [-1*G2 >= 0 (?,1) && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*R >= 0 && R >= 0 && B >= 1 && L2 >= 1 && 0 >= M2] 5. f31(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f31(A,-1 + B,L2,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) [-1*G2 >= 0 (?,1) && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*R >= 0 && R >= 0 && 0 >= L2 && B >= 1] 6. f67(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f104(A,B,D,F,G,H,J,K,0,T,0,X,Y,K1,O1,R1,S1,U1,G2) [-1*G2 >= 0 (1,1) && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && 0 >= H] 7. f67(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f77(A,B,D,F,L2,-1 + H,N2,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) [-1*G2 >= 0 (?,1) && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && H >= 1 && M2 >= 1] 8. f67(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f77(A,B,D,F,L2,-1 + H,N2,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) [-1*G2 >= 0 (?,1) && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && H >= 1 && 0 >= M2] 9. f42(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f31(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) [-1*G2 >= 0 (?,1) && -1 + D + -1*G2 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && -1 + D + G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1 + D >= 0 && -1 + D + Y >= 0 && -1 + D + -1*Y >= 0 && -1 + D + U >= 0 && -1 + D + -1*U >= 0 && -1 + B + D >= 0 && -1 + D + R >= 0 && -1 + D + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && B >= 0 && B + R >= 0 && B + -1*R >= 0 && -1*R >= 0 && R >= 0 && F >= 1] 10. f42(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f31(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) [-1*G2 >= 0 (?,1) && -1 + D + -1*G2 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && -1 + D + G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1 + D >= 0 && -1 + D + Y >= 0 && -1 + D + -1*Y >= 0 && -1 + D + U >= 0 && -1 + D + -1*U >= 0 && -1 + B + D >= 0 && -1 + D + R >= 0 && -1 + D + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && B >= 0 && B + R >= 0 && B + -1*R >= 0 && -1*R >= 0 && R >= 0 && 0 >= F] 11. f104(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f104(A,B,D,F,G,H,J,K,0,T,0,X,Y,K1,O1,R1,S1,-1 + L2,G2) [-1*H >= 0 (?,1) && G2 + -1*H >= 0 && -1*G2 + -1*H >= 0 && -1*H + Y >= 0 && -1*H + -1*Y >= 0 && -1*H + U >= 0 && -1*H + -1*U >= 0 && -1*B + -1*H >= 0 && -1*H + R >= 0 && -1*H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && L2 >= 1] 12. f104(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f144(A,B,D,F,G,H,J,K,0,N2,0,X,Y,K1,O1,R1,S1,L2,G2) [-1*H >= 0 (1,1) && G2 + -1*H >= 0 && -1*G2 + -1*H >= 0 && -1*H + Y >= 0 && -1*H + -1*Y >= 0 && -1*H + U >= 0 && -1*H + -1*U >= 0 && -1*B + -1*H >= 0 && -1*H + R >= 0 && -1*H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && 0 >= L2] 13. f77(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f81(L2,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) [H >= 0 (?,1) && G2 + H >= 0 && -1*G2 + H >= 0 && H + Y >= 0 && H + -1*Y >= 0 && H + U >= 0 && H + -1*U >= 0 && -1*B + H >= 0 && H + R >= 0 && H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && J >= 1] 14. f77(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f81(L2,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) [H >= 0 (?,1) && G2 + H >= 0 && -1*G2 + H >= 0 && H + Y >= 0 && H + -1*Y >= 0 && H + U >= 0 && H + -1*U >= 0 && -1*B + H >= 0 && H + R >= 0 && H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && 0 >= J] 15. f81(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f83(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) [H >= 0 (?,1) && G2 + H >= 0 && -1*G2 + H >= 0 && H + Y >= 0 && H + -1*Y >= 0 && H + U >= 0 && H + -1*U >= 0 && -1*B + H >= 0 && H + R >= 0 && H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && A >= 1] 16. f81(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f83(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) [H >= 0 (?,1) && G2 + H >= 0 && -1*G2 + H >= 0 && H + Y >= 0 && H + -1*Y >= 0 && H + U >= 0 && H + -1*U >= 0 && -1*B + H >= 0 && H + R >= 0 && H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && 0 >= A] 17. f144(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f172(A,B,D,F,G,H,J,K,0,-1 + T,U,0,Y,L2,0,1,0,U1,G2) [-1*H >= 0 (?,1) && G2 + -1*H >= 0 && -1*G2 + -1*H >= 0 && -1*H + -1*U1 >= 0 && -1*H + Y >= 0 && -1*H + -1*Y >= 0 && -1*H + U >= 0 && -1*H + -1*U >= 0 && -1*B + -1*H >= 0 && -1*H + R >= 0 && -1*H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + -1*U1 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + -1*U1 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*U1 >= 0 && -1*U1 + Y >= 0 && -1*U1 + -1*Y >= 0 && U + -1*U1 >= 0 && -1*U + -1*U1 >= 0 && -1*B + -1*U1 >= 0 && R + -1*U1 >= 0 && -1*R + -1*U1 >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && O2 >= 1 && T >= 1 && L2 >= 1] 18. f144(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f172(A,B,D,F,G,H,J,K,0,-1 + T,U,0,Y,L2,0,1,0,U1,G2) [-1*H >= 0 (?,1) && G2 + -1*H >= 0 && -1*G2 + -1*H >= 0 && -1*H + -1*U1 >= 0 && -1*H + Y >= 0 && -1*H + -1*Y >= 0 && -1*H + U >= 0 && -1*H + -1*U >= 0 && -1*B + -1*H >= 0 && -1*H + R >= 0 && -1*H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + -1*U1 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + -1*U1 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*U1 >= 0 && -1*U1 + Y >= 0 && -1*U1 + -1*Y >= 0 && U + -1*U1 >= 0 && -1*U + -1*U1 >= 0 && -1*B + -1*U1 >= 0 && R + -1*U1 >= 0 && -1*R + -1*U1 >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && 0 >= 1 + O2 && T >= 1 && L2 >= 1] 19. f144(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f144(A,B,D,F,G,H,J,K,0,-1 + T,0,X,Y,L2,0,R1,S1,U1,G2) [-1*H >= 0 (?,1) && G2 + -1*H >= 0 && -1*G2 + -1*H >= 0 && -1*H + -1*U1 >= 0 && -1*H + Y >= 0 && -1*H + -1*Y >= 0 && -1*H + U >= 0 && -1*H + -1*U >= 0 && -1*B + -1*H >= 0 && -1*H + R >= 0 && -1*H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + -1*U1 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + -1*U1 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*U1 >= 0 && -1*U1 + Y >= 0 && -1*U1 + -1*Y >= 0 && U + -1*U1 >= 0 && -1*U + -1*U1 >= 0 && -1*B + -1*U1 >= 0 && R + -1*U1 >= 0 && -1*R + -1*U1 >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && T >= 1 && L2 >= 1] 20. f144(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f144(A,B,D,F,G,H,J,K,0,-1 + T,0,X,Y,L2,O1,R1,S1,U1,G2) [-1*H >= 0 (?,1) && G2 + -1*H >= 0 && -1*G2 + -1*H >= 0 && -1*H + -1*U1 >= 0 && -1*H + Y >= 0 && -1*H + -1*Y >= 0 && -1*H + U >= 0 && -1*H + -1*U >= 0 && -1*B + -1*H >= 0 && -1*H + R >= 0 && -1*H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + -1*U1 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + -1*U1 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*U1 >= 0 && -1*U1 + Y >= 0 && -1*U1 + -1*Y >= 0 && U + -1*U1 >= 0 && -1*U + -1*U1 >= 0 && -1*B + -1*U1 >= 0 && R + -1*U1 >= 0 && -1*R + -1*U1 >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && T >= 1 && 0 >= L2] 21. f144(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f211(A,B,D,F,G,H,J,M2,0,T,0,X,Y,K1,O1,R1,S1,U1,G2) [-1*H >= 0 (1,1) && G2 + -1*H >= 0 && -1*G2 + -1*H >= 0 && -1*H + -1*U1 >= 0 && -1*H + Y >= 0 && -1*H + -1*Y >= 0 && -1*H + U >= 0 && -1*H + -1*U >= 0 && -1*B + -1*H >= 0 && -1*H + R >= 0 && -1*H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + -1*U1 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + -1*U1 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*U1 >= 0 && -1*U1 + Y >= 0 && -1*U1 + -1*Y >= 0 && U + -1*U1 >= 0 && -1*U + -1*U1 >= 0 && -1*B + -1*U1 >= 0 && R + -1*U1 >= 0 && -1*R + -1*U1 >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && 0 >= T] 22. f83(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f67(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) [H >= 0 (?,1) && G2 + H >= 0 && -1*G2 + H >= 0 && H + Y >= 0 && H + -1*Y >= 0 && H + U >= 0 && H + -1*U >= 0 && -1*B + H >= 0 && H + R >= 0 && H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && G >= 1] 23. f83(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f67(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) [H >= 0 (?,1) && G2 + H >= 0 && -1*G2 + H >= 0 && H + Y >= 0 && H + -1*Y >= 0 && H + U >= 0 && H + -1*U >= 0 && -1*B + H >= 0 && H + R >= 0 && H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && 0 >= G] 24. f172(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f144(A,B,D,F,G,H,J,K,R,T,0,X,Y,K1,O1,R1,S1,U1,G2) [-1*H >= 0 (?,1) && G2 + -1*H >= 0 && -1*G2 + -1*H >= 0 && -1*H + -1*U1 >= 0 && -1*H + S1 >= 0 && -1*H + -1*S1 >= 0 && -1 + -1*H + R1 >= 0 && 1 + -1*H + -1*R1 >= 0 && -1*H + O1 >= 0 && -1*H + -1*O1 >= 0 && -1 + -1*H + K1 >= 0 && -1*H + Y >= 0 && -1*H + -1*Y >= 0 && -1*H + X >= 0 && -1*H + -1*X >= 0 && -1*H + U >= 0 && -1*H + -1*U >= 0 && -1*H + T >= 0 && -1*B + -1*H >= 0 && -1*H + R >= 0 && -1*H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + -1*U1 >= 0 && -1*G2 + S1 >= 0 && -1*G2 + -1*S1 >= 0 && -1 + -1*G2 + R1 >= 0 && 1 + -1*G2 + -1*R1 >= 0 && -1*G2 + O1 >= 0 && -1*G2 + -1*O1 >= 0 && -1 + -1*G2 + K1 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + X >= 0 && -1*G2 + -1*X >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*G2 + T >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + -1*U1 >= 0 && G2 + S1 >= 0 && G2 + -1*S1 >= 0 && -1 + G2 + R1 >= 0 && 1 + G2 + -1*R1 >= 0 && G2 + O1 >= 0 && G2 + -1*O1 >= 0 && -1 + G2 + K1 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + X >= 0 && G2 + -1*X >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && G2 + T >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*U1 >= 0 && S1 + -1*U1 >= 0 && -1*S1 + -1*U1 >= 0 && -1 + R1 + -1*U1 >= 0 && 1 + -1*R1 + -1*U1 >= 0 && O1 + -1*U1 >= 0 && -1*O1 + -1*U1 >= 0 && -1 + K1 + -1*U1 >= 0 && -1*U1 + Y >= 0 && -1*U1 + -1*Y >= 0 && -1*U1 + X >= 0 && -1*U1 + -1*X >= 0 && U + -1*U1 >= 0 && -1*U + -1*U1 >= 0 && T + -1*U1 >= 0 && -1*B + -1*U1 >= 0 && R + -1*U1 >= 0 && -1*R + -1*U1 >= 0 && -1*S1 >= 0 && -1 + R1 + -1*S1 >= 0 && 1 + -1*R1 + -1*S1 >= 0 && O1 + -1*S1 >= 0 && -1*O1 + -1*S1 >= 0 && -1 + K1 + -1*S1 >= 0 && -1*S1 + Y >= 0 && -1*S1 + -1*Y >= 0 && -1*S1 + X >= 0 && -1*S1 + -1*X >= 0 && -1*S1 + U >= 0 && -1*S1 + -1*U >= 0 && -1*S1 + T >= 0 && -1*B + -1*S1 >= 0 && R + -1*S1 >= 0 && -1*R + -1*S1 >= 0 && S1 >= 0 && -1 + R1 + S1 >= 0 && 1 + -1*R1 + S1 >= 0 && O1 + S1 >= 0 && -1*O1 + S1 >= 0 && -1 + K1 + S1 >= 0 && S1 + Y >= 0 && S1 + -1*Y >= 0 && S1 + X >= 0 && S1 + -1*X >= 0 && S1 + U >= 0 && S1 + -1*U >= 0 && S1 + T >= 0 && -1*B + S1 >= 0 && R + S1 >= 0 && -1*R + S1 >= 0 && 1 + -1*R1 >= 0 && 1 + O1 + -1*R1 >= 0 && 1 + -1*O1 + -1*R1 >= 0 && K1 + -1*R1 >= 0 && 1 + -1*R1 + Y >= 0 && 1 + -1*R1 + -1*Y >= 0 && 1 + -1*R1 + X >= 0 && 1 + -1*R1 + -1*X >= 0 && 1 + -1*R1 + U >= 0 && 1 + -1*R1 + -1*U >= 0 && 1 + -1*R1 + T >= 0 && 1 + -1*B + -1*R1 >= 0 && 1 + R + -1*R1 >= 0 && 1 + -1*R + -1*R1 >= 0 && -1 + R1 >= 0 && -1 + O1 + R1 >= 0 && -1 + -1*O1 + R1 >= 0 && -2 + K1 + R1 >= 0 && -1 + R1 + Y >= 0 && -1 + R1 + -1*Y >= 0 && -1 + R1 + X >= 0 && -1 + R1 + -1*X >= 0 && -1 + R1 + U >= 0 && -1 + R1 + -1*U >= 0 && -1 + R1 + T >= 0 && -1 + -1*B + R1 >= 0 && -1 + R + R1 >= 0 && -1 + -1*R + R1 >= 0 && -1*O1 >= 0 && -1 + K1 + -1*O1 >= 0 && -1*O1 + Y >= 0 && -1*O1 + -1*Y >= 0 && -1*O1 + X >= 0 && -1*O1 + -1*X >= 0 && -1*O1 + U >= 0 && -1*O1 + -1*U >= 0 && -1*O1 + T >= 0 && -1*B + -1*O1 >= 0 && -1*O1 + R >= 0 && -1*O1 + -1*R >= 0 && O1 >= 0 && -1 + K1 + O1 >= 0 && O1 + Y >= 0 && O1 + -1*Y >= 0 && O1 + X >= 0 && O1 + -1*X >= 0 && O1 + U >= 0 && O1 + -1*U >= 0 && O1 + T >= 0 && -1*B + O1 >= 0 && O1 + R >= 0 && O1 + -1*R >= 0 && -1 + K1 >= 0 && -1 + K1 + Y >= 0 && -1 + K1 + -1*Y >= 0 && -1 + K1 + X >= 0 && -1 + K1 + -1*X >= 0 && -1 + K1 + U >= 0 && -1 + K1 + -1*U >= 0 && -1 + K1 + T >= 0 && -1 + -1*B + K1 >= 0 && -1 + K1 + R >= 0 && -1 + K1 + -1*R >= 0 && -1*Y >= 0 && X + -1*Y >= 0 && -1*X + -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && T + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && X + Y >= 0 && -1*X + Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && T + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*X >= 0 && U + -1*X >= 0 && -1*U + -1*X >= 0 && T + -1*X >= 0 && -1*B + -1*X >= 0 && R + -1*X >= 0 && -1*R + -1*X >= 0 && X >= 0 && U + X >= 0 && -1*U + X >= 0 && T + X >= 0 && -1*B + X >= 0 && R + X >= 0 && -1*R + X >= 0 && -1*U >= 0 && T + -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && T + U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && T >= 0 && -1*B + T >= 0 && R + T >= 0 && -1*R + T >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && 0 >= X] 25. f211(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f235(A,B,D,F,G,H,J,K,0,T,U,X,Y,K1,O1,R1,S1,U1,G2) [-1*H >= 0 (1,1) && G2 + -1*H >= 0 && -1*G2 + -1*H >= 0 && -1*H + -1*U1 >= 0 && -1*H + Y >= 0 && -1*H + -1*Y >= 0 && -1*H + U >= 0 && -1*H + -1*U >= 0 && -1*H + -1*T >= 0 && -1*B + -1*H >= 0 && -1*H + R >= 0 && -1*H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + -1*U1 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*G2 + -1*T >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + -1*U1 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && G2 + -1*T >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*U1 >= 0 && -1*U1 + Y >= 0 && -1*U1 + -1*Y >= 0 && U + -1*U1 >= 0 && -1*U + -1*U1 >= 0 && -1*T + -1*U1 >= 0 && -1*B + -1*U1 >= 0 && R + -1*U1 >= 0 && -1*R + -1*U1 >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*T + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*T + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*T + -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*T + U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*T >= 0 && -1*B + -1*T >= 0 && R + -1*T >= 0 && -1*R + -1*T >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && 0 >= K] 26. f211(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f211(A,B,D,F,G,H,J,-1 + K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) [-1*H >= 0 (?,1) && G2 + -1*H >= 0 && -1*G2 + -1*H >= 0 && -1*H + -1*U1 >= 0 && -1*H + Y >= 0 && -1*H + -1*Y >= 0 && -1*H + U >= 0 && -1*H + -1*U >= 0 && -1*H + -1*T >= 0 && -1*B + -1*H >= 0 && -1*H + R >= 0 && -1*H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + -1*U1 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*G2 + -1*T >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + -1*U1 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && G2 + -1*T >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*U1 >= 0 && -1*U1 + Y >= 0 && -1*U1 + -1*Y >= 0 && U + -1*U1 >= 0 && -1*U + -1*U1 >= 0 && -1*T + -1*U1 >= 0 && -1*B + -1*U1 >= 0 && R + -1*U1 >= 0 && -1*R + -1*U1 >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*T + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*T + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*T + -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*T + U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*T >= 0 && -1*B + -1*T >= 0 && R + -1*T >= 0 && -1*R + -1*T >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && K >= 1] 27. f235(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f235(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) [-1*H >= 0 (?,1) && G2 + -1*H >= 0 && -1*G2 + -1*H >= 0 && -1*H + -1*U1 >= 0 && -1*H + Y >= 0 && -1*H + -1*Y >= 0 && -1*H + U >= 0 && -1*H + -1*U >= 0 && -1*H + -1*T >= 0 && -1*B + -1*H >= 0 && -1*H + R >= 0 && -1*H + -1*R >= 0 && -1*H + -1*K >= 0 && -1*G2 >= 0 && -1*G2 + -1*U1 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*G2 + -1*T >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && -1*G2 + -1*K >= 0 && G2 >= 0 && G2 + -1*U1 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && G2 + -1*T >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && G2 + -1*K >= 0 && -1*U1 >= 0 && -1*U1 + Y >= 0 && -1*U1 + -1*Y >= 0 && U + -1*U1 >= 0 && -1*U + -1*U1 >= 0 && -1*T + -1*U1 >= 0 && -1*B + -1*U1 >= 0 && R + -1*U1 >= 0 && -1*R + -1*U1 >= 0 && -1*K + -1*U1 >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*T + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && -1*K + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*T + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*K + Y >= 0 && -1*U >= 0 && -1*T + -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && -1*K + -1*U >= 0 && U >= 0 && -1*T + U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*K + U >= 0 && -1*T >= 0 && -1*B + -1*T >= 0 && R + -1*T >= 0 && -1*R + -1*T >= 0 && -1*K + -1*T >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*B + -1*K >= 0 && -1*R >= 0 && -1*K + -1*R >= 0 && R >= 0 && -1*K + R >= 0 && -1*K >= 0] Signature: {(f0,63) ;(f104,63) ;(f144,63) ;(f172,63) ;(f211,63) ;(f235,63) ;(f31,63) ;(f42,63) ;(f67,63) ;(f77,63) ;(f81,63) ;(f83,63)} Flow Graph: [0->{2,3,4,5},1->{2,3,4,5},2->{6,7,8},3->{9,10},4->{9,10},5->{2,3,4,5},6->{11,12},7->{13,14},8->{13,14} ,9->{2,3,4,5},10->{2,3,4,5},11->{11,12},12->{17,18,19,20,21},13->{15,16},14->{15,16},15->{22,23},16->{22,23} ,17->{24},18->{24},19->{17,18,19,20,21},20->{17,18,19,20,21},21->{25,26},22->{6,7,8},23->{6,7,8},24->{17,18 ,19,20,21},25->{27},26->{25,26},27->{27}] + Applied Processor: AddSinks + Details: () * Step 4: Failure MAYBE + Considered Problem: Rules: 0. f0(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f31(A,O2,D,F,G,H,J,K,0,T,0,X,0,K1,O1,R1,S1,U1,0) [L2 >= 1] (1,1) 1. f0(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f31(A,M2,D,F,G,H,J,K,0,T,0,X,0,K1,O1,R1,S1,U1,0) [0 >= L2] (1,1) 2. f31(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f67(A,B,D,F,G,M2,J,K,0,T,0,X,Y,K1,O1,R1,S1,U1,G2) [-1*G2 >= 0 (?,1) && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*R >= 0 && R >= 0 && 0 >= B] 3. f31(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f42(A,-1 + B,L2,N2,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) [-1*G2 >= 0 (?,1) && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*R >= 0 && R >= 0 && B >= 1 && L2 >= 1 && M2 >= 1] 4. f31(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f42(A,-1 + B,L2,N2,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) [-1*G2 >= 0 (?,1) && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*R >= 0 && R >= 0 && B >= 1 && L2 >= 1 && 0 >= M2] 5. f31(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f31(A,-1 + B,L2,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) [-1*G2 >= 0 (?,1) && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*R >= 0 && R >= 0 && 0 >= L2 && B >= 1] 6. f67(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f104(A,B,D,F,G,H,J,K,0,T,0,X,Y,K1,O1,R1,S1,U1,G2) [-1*G2 >= 0 (?,1) && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && 0 >= H] 7. f67(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f77(A,B,D,F,L2,-1 + H,N2,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) [-1*G2 >= 0 (?,1) && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && H >= 1 && M2 >= 1] 8. f67(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f77(A,B,D,F,L2,-1 + H,N2,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) [-1*G2 >= 0 (?,1) && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && H >= 1 && 0 >= M2] 9. f42(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f31(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) [-1*G2 >= 0 (?,1) && -1 + D + -1*G2 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && -1 + D + G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1 + D >= 0 && -1 + D + Y >= 0 && -1 + D + -1*Y >= 0 && -1 + D + U >= 0 && -1 + D + -1*U >= 0 && -1 + B + D >= 0 && -1 + D + R >= 0 && -1 + D + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && B >= 0 && B + R >= 0 && B + -1*R >= 0 && -1*R >= 0 && R >= 0 && F >= 1] 10. f42(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f31(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) [-1*G2 >= 0 (?,1) && -1 + D + -1*G2 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && -1 + D + G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1 + D >= 0 && -1 + D + Y >= 0 && -1 + D + -1*Y >= 0 && -1 + D + U >= 0 && -1 + D + -1*U >= 0 && -1 + B + D >= 0 && -1 + D + R >= 0 && -1 + D + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && B >= 0 && B + R >= 0 && B + -1*R >= 0 && -1*R >= 0 && R >= 0 && 0 >= F] 11. f104(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f104(A,B,D,F,G,H,J,K,0,T,0,X,Y,K1,O1,R1,S1,-1 + L2,G2) [-1*H >= 0 (?,1) && G2 + -1*H >= 0 && -1*G2 + -1*H >= 0 && -1*H + Y >= 0 && -1*H + -1*Y >= 0 && -1*H + U >= 0 && -1*H + -1*U >= 0 && -1*B + -1*H >= 0 && -1*H + R >= 0 && -1*H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && L2 >= 1] 12. f104(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f144(A,B,D,F,G,H,J,K,0,N2,0,X,Y,K1,O1,R1,S1,L2,G2) [-1*H >= 0 (?,1) && G2 + -1*H >= 0 && -1*G2 + -1*H >= 0 && -1*H + Y >= 0 && -1*H + -1*Y >= 0 && -1*H + U >= 0 && -1*H + -1*U >= 0 && -1*B + -1*H >= 0 && -1*H + R >= 0 && -1*H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && 0 >= L2] 13. f77(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f81(L2,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) [H >= 0 (?,1) && G2 + H >= 0 && -1*G2 + H >= 0 && H + Y >= 0 && H + -1*Y >= 0 && H + U >= 0 && H + -1*U >= 0 && -1*B + H >= 0 && H + R >= 0 && H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && J >= 1] 14. f77(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f81(L2,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) [H >= 0 (?,1) && G2 + H >= 0 && -1*G2 + H >= 0 && H + Y >= 0 && H + -1*Y >= 0 && H + U >= 0 && H + -1*U >= 0 && -1*B + H >= 0 && H + R >= 0 && H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && 0 >= J] 15. f81(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f83(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) [H >= 0 (?,1) && G2 + H >= 0 && -1*G2 + H >= 0 && H + Y >= 0 && H + -1*Y >= 0 && H + U >= 0 && H + -1*U >= 0 && -1*B + H >= 0 && H + R >= 0 && H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && A >= 1] 16. f81(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f83(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) [H >= 0 (?,1) && G2 + H >= 0 && -1*G2 + H >= 0 && H + Y >= 0 && H + -1*Y >= 0 && H + U >= 0 && H + -1*U >= 0 && -1*B + H >= 0 && H + R >= 0 && H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && 0 >= A] 17. f144(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f172(A,B,D,F,G,H,J,K,0,-1 + T,U,0,Y,L2,0,1,0,U1,G2) [-1*H >= 0 (?,1) && G2 + -1*H >= 0 && -1*G2 + -1*H >= 0 && -1*H + -1*U1 >= 0 && -1*H + Y >= 0 && -1*H + -1*Y >= 0 && -1*H + U >= 0 && -1*H + -1*U >= 0 && -1*B + -1*H >= 0 && -1*H + R >= 0 && -1*H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + -1*U1 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + -1*U1 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*U1 >= 0 && -1*U1 + Y >= 0 && -1*U1 + -1*Y >= 0 && U + -1*U1 >= 0 && -1*U + -1*U1 >= 0 && -1*B + -1*U1 >= 0 && R + -1*U1 >= 0 && -1*R + -1*U1 >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && O2 >= 1 && T >= 1 && L2 >= 1] 18. f144(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f172(A,B,D,F,G,H,J,K,0,-1 + T,U,0,Y,L2,0,1,0,U1,G2) [-1*H >= 0 (?,1) && G2 + -1*H >= 0 && -1*G2 + -1*H >= 0 && -1*H + -1*U1 >= 0 && -1*H + Y >= 0 && -1*H + -1*Y >= 0 && -1*H + U >= 0 && -1*H + -1*U >= 0 && -1*B + -1*H >= 0 && -1*H + R >= 0 && -1*H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + -1*U1 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + -1*U1 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*U1 >= 0 && -1*U1 + Y >= 0 && -1*U1 + -1*Y >= 0 && U + -1*U1 >= 0 && -1*U + -1*U1 >= 0 && -1*B + -1*U1 >= 0 && R + -1*U1 >= 0 && -1*R + -1*U1 >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && 0 >= 1 + O2 && T >= 1 && L2 >= 1] 19. f144(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f144(A,B,D,F,G,H,J,K,0,-1 + T,0,X,Y,L2,0,R1,S1,U1,G2) [-1*H >= 0 (?,1) && G2 + -1*H >= 0 && -1*G2 + -1*H >= 0 && -1*H + -1*U1 >= 0 && -1*H + Y >= 0 && -1*H + -1*Y >= 0 && -1*H + U >= 0 && -1*H + -1*U >= 0 && -1*B + -1*H >= 0 && -1*H + R >= 0 && -1*H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + -1*U1 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + -1*U1 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*U1 >= 0 && -1*U1 + Y >= 0 && -1*U1 + -1*Y >= 0 && U + -1*U1 >= 0 && -1*U + -1*U1 >= 0 && -1*B + -1*U1 >= 0 && R + -1*U1 >= 0 && -1*R + -1*U1 >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && T >= 1 && L2 >= 1] 20. f144(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f144(A,B,D,F,G,H,J,K,0,-1 + T,0,X,Y,L2,O1,R1,S1,U1,G2) [-1*H >= 0 (?,1) && G2 + -1*H >= 0 && -1*G2 + -1*H >= 0 && -1*H + -1*U1 >= 0 && -1*H + Y >= 0 && -1*H + -1*Y >= 0 && -1*H + U >= 0 && -1*H + -1*U >= 0 && -1*B + -1*H >= 0 && -1*H + R >= 0 && -1*H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + -1*U1 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + -1*U1 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*U1 >= 0 && -1*U1 + Y >= 0 && -1*U1 + -1*Y >= 0 && U + -1*U1 >= 0 && -1*U + -1*U1 >= 0 && -1*B + -1*U1 >= 0 && R + -1*U1 >= 0 && -1*R + -1*U1 >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && T >= 1 && 0 >= L2] 21. f144(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f211(A,B,D,F,G,H,J,M2,0,T,0,X,Y,K1,O1,R1,S1,U1,G2) [-1*H >= 0 (?,1) && G2 + -1*H >= 0 && -1*G2 + -1*H >= 0 && -1*H + -1*U1 >= 0 && -1*H + Y >= 0 && -1*H + -1*Y >= 0 && -1*H + U >= 0 && -1*H + -1*U >= 0 && -1*B + -1*H >= 0 && -1*H + R >= 0 && -1*H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + -1*U1 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + -1*U1 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*U1 >= 0 && -1*U1 + Y >= 0 && -1*U1 + -1*Y >= 0 && U + -1*U1 >= 0 && -1*U + -1*U1 >= 0 && -1*B + -1*U1 >= 0 && R + -1*U1 >= 0 && -1*R + -1*U1 >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && 0 >= T] 22. f83(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f67(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) [H >= 0 (?,1) && G2 + H >= 0 && -1*G2 + H >= 0 && H + Y >= 0 && H + -1*Y >= 0 && H + U >= 0 && H + -1*U >= 0 && -1*B + H >= 0 && H + R >= 0 && H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && G >= 1] 23. f83(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f67(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) [H >= 0 (?,1) && G2 + H >= 0 && -1*G2 + H >= 0 && H + Y >= 0 && H + -1*Y >= 0 && H + U >= 0 && H + -1*U >= 0 && -1*B + H >= 0 && H + R >= 0 && H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && 0 >= G] 24. f172(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f144(A,B,D,F,G,H,J,K,R,T,0,X,Y,K1,O1,R1,S1,U1,G2) [-1*H >= 0 (?,1) && G2 + -1*H >= 0 && -1*G2 + -1*H >= 0 && -1*H + -1*U1 >= 0 && -1*H + S1 >= 0 && -1*H + -1*S1 >= 0 && -1 + -1*H + R1 >= 0 && 1 + -1*H + -1*R1 >= 0 && -1*H + O1 >= 0 && -1*H + -1*O1 >= 0 && -1 + -1*H + K1 >= 0 && -1*H + Y >= 0 && -1*H + -1*Y >= 0 && -1*H + X >= 0 && -1*H + -1*X >= 0 && -1*H + U >= 0 && -1*H + -1*U >= 0 && -1*H + T >= 0 && -1*B + -1*H >= 0 && -1*H + R >= 0 && -1*H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + -1*U1 >= 0 && -1*G2 + S1 >= 0 && -1*G2 + -1*S1 >= 0 && -1 + -1*G2 + R1 >= 0 && 1 + -1*G2 + -1*R1 >= 0 && -1*G2 + O1 >= 0 && -1*G2 + -1*O1 >= 0 && -1 + -1*G2 + K1 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + X >= 0 && -1*G2 + -1*X >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*G2 + T >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + -1*U1 >= 0 && G2 + S1 >= 0 && G2 + -1*S1 >= 0 && -1 + G2 + R1 >= 0 && 1 + G2 + -1*R1 >= 0 && G2 + O1 >= 0 && G2 + -1*O1 >= 0 && -1 + G2 + K1 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + X >= 0 && G2 + -1*X >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && G2 + T >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*U1 >= 0 && S1 + -1*U1 >= 0 && -1*S1 + -1*U1 >= 0 && -1 + R1 + -1*U1 >= 0 && 1 + -1*R1 + -1*U1 >= 0 && O1 + -1*U1 >= 0 && -1*O1 + -1*U1 >= 0 && -1 + K1 + -1*U1 >= 0 && -1*U1 + Y >= 0 && -1*U1 + -1*Y >= 0 && -1*U1 + X >= 0 && -1*U1 + -1*X >= 0 && U + -1*U1 >= 0 && -1*U + -1*U1 >= 0 && T + -1*U1 >= 0 && -1*B + -1*U1 >= 0 && R + -1*U1 >= 0 && -1*R + -1*U1 >= 0 && -1*S1 >= 0 && -1 + R1 + -1*S1 >= 0 && 1 + -1*R1 + -1*S1 >= 0 && O1 + -1*S1 >= 0 && -1*O1 + -1*S1 >= 0 && -1 + K1 + -1*S1 >= 0 && -1*S1 + Y >= 0 && -1*S1 + -1*Y >= 0 && -1*S1 + X >= 0 && -1*S1 + -1*X >= 0 && -1*S1 + U >= 0 && -1*S1 + -1*U >= 0 && -1*S1 + T >= 0 && -1*B + -1*S1 >= 0 && R + -1*S1 >= 0 && -1*R + -1*S1 >= 0 && S1 >= 0 && -1 + R1 + S1 >= 0 && 1 + -1*R1 + S1 >= 0 && O1 + S1 >= 0 && -1*O1 + S1 >= 0 && -1 + K1 + S1 >= 0 && S1 + Y >= 0 && S1 + -1*Y >= 0 && S1 + X >= 0 && S1 + -1*X >= 0 && S1 + U >= 0 && S1 + -1*U >= 0 && S1 + T >= 0 && -1*B + S1 >= 0 && R + S1 >= 0 && -1*R + S1 >= 0 && 1 + -1*R1 >= 0 && 1 + O1 + -1*R1 >= 0 && 1 + -1*O1 + -1*R1 >= 0 && K1 + -1*R1 >= 0 && 1 + -1*R1 + Y >= 0 && 1 + -1*R1 + -1*Y >= 0 && 1 + -1*R1 + X >= 0 && 1 + -1*R1 + -1*X >= 0 && 1 + -1*R1 + U >= 0 && 1 + -1*R1 + -1*U >= 0 && 1 + -1*R1 + T >= 0 && 1 + -1*B + -1*R1 >= 0 && 1 + R + -1*R1 >= 0 && 1 + -1*R + -1*R1 >= 0 && -1 + R1 >= 0 && -1 + O1 + R1 >= 0 && -1 + -1*O1 + R1 >= 0 && -2 + K1 + R1 >= 0 && -1 + R1 + Y >= 0 && -1 + R1 + -1*Y >= 0 && -1 + R1 + X >= 0 && -1 + R1 + -1*X >= 0 && -1 + R1 + U >= 0 && -1 + R1 + -1*U >= 0 && -1 + R1 + T >= 0 && -1 + -1*B + R1 >= 0 && -1 + R + R1 >= 0 && -1 + -1*R + R1 >= 0 && -1*O1 >= 0 && -1 + K1 + -1*O1 >= 0 && -1*O1 + Y >= 0 && -1*O1 + -1*Y >= 0 && -1*O1 + X >= 0 && -1*O1 + -1*X >= 0 && -1*O1 + U >= 0 && -1*O1 + -1*U >= 0 && -1*O1 + T >= 0 && -1*B + -1*O1 >= 0 && -1*O1 + R >= 0 && -1*O1 + -1*R >= 0 && O1 >= 0 && -1 + K1 + O1 >= 0 && O1 + Y >= 0 && O1 + -1*Y >= 0 && O1 + X >= 0 && O1 + -1*X >= 0 && O1 + U >= 0 && O1 + -1*U >= 0 && O1 + T >= 0 && -1*B + O1 >= 0 && O1 + R >= 0 && O1 + -1*R >= 0 && -1 + K1 >= 0 && -1 + K1 + Y >= 0 && -1 + K1 + -1*Y >= 0 && -1 + K1 + X >= 0 && -1 + K1 + -1*X >= 0 && -1 + K1 + U >= 0 && -1 + K1 + -1*U >= 0 && -1 + K1 + T >= 0 && -1 + -1*B + K1 >= 0 && -1 + K1 + R >= 0 && -1 + K1 + -1*R >= 0 && -1*Y >= 0 && X + -1*Y >= 0 && -1*X + -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && T + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && X + Y >= 0 && -1*X + Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && T + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*X >= 0 && U + -1*X >= 0 && -1*U + -1*X >= 0 && T + -1*X >= 0 && -1*B + -1*X >= 0 && R + -1*X >= 0 && -1*R + -1*X >= 0 && X >= 0 && U + X >= 0 && -1*U + X >= 0 && T + X >= 0 && -1*B + X >= 0 && R + X >= 0 && -1*R + X >= 0 && -1*U >= 0 && T + -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && T + U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && T >= 0 && -1*B + T >= 0 && R + T >= 0 && -1*R + T >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && 0 >= X] 25. f211(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f235(A,B,D,F,G,H,J,K,0,T,U,X,Y,K1,O1,R1,S1,U1,G2) [-1*H >= 0 (?,1) && G2 + -1*H >= 0 && -1*G2 + -1*H >= 0 && -1*H + -1*U1 >= 0 && -1*H + Y >= 0 && -1*H + -1*Y >= 0 && -1*H + U >= 0 && -1*H + -1*U >= 0 && -1*H + -1*T >= 0 && -1*B + -1*H >= 0 && -1*H + R >= 0 && -1*H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + -1*U1 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*G2 + -1*T >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + -1*U1 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && G2 + -1*T >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*U1 >= 0 && -1*U1 + Y >= 0 && -1*U1 + -1*Y >= 0 && U + -1*U1 >= 0 && -1*U + -1*U1 >= 0 && -1*T + -1*U1 >= 0 && -1*B + -1*U1 >= 0 && R + -1*U1 >= 0 && -1*R + -1*U1 >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*T + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*T + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*T + -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*T + U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*T >= 0 && -1*B + -1*T >= 0 && R + -1*T >= 0 && -1*R + -1*T >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && 0 >= K] 26. f211(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f211(A,B,D,F,G,H,J,-1 + K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) [-1*H >= 0 (?,1) && G2 + -1*H >= 0 && -1*G2 + -1*H >= 0 && -1*H + -1*U1 >= 0 && -1*H + Y >= 0 && -1*H + -1*Y >= 0 && -1*H + U >= 0 && -1*H + -1*U >= 0 && -1*H + -1*T >= 0 && -1*B + -1*H >= 0 && -1*H + R >= 0 && -1*H + -1*R >= 0 && -1*G2 >= 0 && -1*G2 + -1*U1 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*G2 + -1*T >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && G2 >= 0 && G2 + -1*U1 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && G2 + -1*T >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && -1*U1 >= 0 && -1*U1 + Y >= 0 && -1*U1 + -1*Y >= 0 && U + -1*U1 >= 0 && -1*U + -1*U1 >= 0 && -1*T + -1*U1 >= 0 && -1*B + -1*U1 >= 0 && R + -1*U1 >= 0 && -1*R + -1*U1 >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*T + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*T + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*U >= 0 && -1*T + -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && U >= 0 && -1*T + U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*T >= 0 && -1*B + -1*T >= 0 && R + -1*T >= 0 && -1*R + -1*T >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*R >= 0 && R >= 0 && K >= 1] 27. f235(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> f235(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) [-1*H >= 0 (?,1) && G2 + -1*H >= 0 && -1*G2 + -1*H >= 0 && -1*H + -1*U1 >= 0 && -1*H + Y >= 0 && -1*H + -1*Y >= 0 && -1*H + U >= 0 && -1*H + -1*U >= 0 && -1*H + -1*T >= 0 && -1*B + -1*H >= 0 && -1*H + R >= 0 && -1*H + -1*R >= 0 && -1*H + -1*K >= 0 && -1*G2 >= 0 && -1*G2 + -1*U1 >= 0 && -1*G2 + Y >= 0 && -1*G2 + -1*Y >= 0 && -1*G2 + U >= 0 && -1*G2 + -1*U >= 0 && -1*G2 + -1*T >= 0 && -1*B + -1*G2 >= 0 && -1*G2 + R >= 0 && -1*G2 + -1*R >= 0 && -1*G2 + -1*K >= 0 && G2 >= 0 && G2 + -1*U1 >= 0 && G2 + Y >= 0 && G2 + -1*Y >= 0 && G2 + U >= 0 && G2 + -1*U >= 0 && G2 + -1*T >= 0 && -1*B + G2 >= 0 && G2 + R >= 0 && G2 + -1*R >= 0 && G2 + -1*K >= 0 && -1*U1 >= 0 && -1*U1 + Y >= 0 && -1*U1 + -1*Y >= 0 && U + -1*U1 >= 0 && -1*U + -1*U1 >= 0 && -1*T + -1*U1 >= 0 && -1*B + -1*U1 >= 0 && R + -1*U1 >= 0 && -1*R + -1*U1 >= 0 && -1*K + -1*U1 >= 0 && -1*Y >= 0 && U + -1*Y >= 0 && -1*U + -1*Y >= 0 && -1*T + -1*Y >= 0 && -1*B + -1*Y >= 0 && R + -1*Y >= 0 && -1*R + -1*Y >= 0 && -1*K + -1*Y >= 0 && Y >= 0 && U + Y >= 0 && -1*U + Y >= 0 && -1*T + Y >= 0 && -1*B + Y >= 0 && R + Y >= 0 && -1*R + Y >= 0 && -1*K + Y >= 0 && -1*U >= 0 && -1*T + -1*U >= 0 && -1*B + -1*U >= 0 && R + -1*U >= 0 && -1*R + -1*U >= 0 && -1*K + -1*U >= 0 && U >= 0 && -1*T + U >= 0 && -1*B + U >= 0 && R + U >= 0 && -1*R + U >= 0 && -1*K + U >= 0 && -1*T >= 0 && -1*B + -1*T >= 0 && R + -1*T >= 0 && -1*R + -1*T >= 0 && -1*K + -1*T >= 0 && -1*B >= 0 && -1*B + R >= 0 && -1*B + -1*R >= 0 && -1*B + -1*K >= 0 && -1*R >= 0 && -1*K + -1*R >= 0 && R >= 0 && -1*K + R >= 0 && -1*K >= 0] 28. f235(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) -> exitus616(A,B,D,F,G,H,J,K,R,T,U,X,Y,K1,O1,R1,S1,U1,G2) True (?,1) Signature: {(exitus616,19) ;(f0,63) ;(f104,63) ;(f144,63) ;(f172,63) ;(f211,63) ;(f235,63) ;(f31,63) ;(f42,63) ;(f67,63) ;(f77,63) ;(f81,63) ;(f83,63)} Flow Graph: [0->{2,3,4,5},1->{2,3,4,5},2->{6,7,8},3->{9,10},4->{9,10},5->{2,3,4,5},6->{11,12},7->{13,14},8->{13,14} ,9->{2,3,4,5},10->{2,3,4,5},11->{11,12},12->{17,18,19,20,21},13->{15,16},14->{15,16},15->{22,23},16->{22,23} ,17->{24},18->{24},19->{17,18,19,20,21},20->{17,18,19,20,21},21->{25,26},22->{6,7,8},23->{6,7,8},24->{17,18 ,19,20,21},25->{27,28},26->{25,26},27->{27,28},28->{}] + Applied Processor: LooptreeTransformer + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28] | +- p:[3,5,9,4,10] c: [10] | | | `- p:[3,5,9,4] c: [9] | | | `- p:[5] c: [5] | +- p:[7,22,15,13,8,23,16,14] c: [23] | | | `- p:[7,22,15,13,8,14,16] c: [22] | +- p:[11] c: [] | +- p:[17,19,20,24,18] c: [24] | | | `- p:[19,20] c: [20] | | | `- p:[19] c: [19] | +- p:[26] c: [26] | `- p:[27] c: [] MAYBE