(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS f3)) (VAR A B C D E F G H I J K L M N O P Q R S T U V W X Y Z A1 B1 C1 D1 E1 F1 G1 H1 I1 J1 K1 L1 M1 N1 O1 P1 Q1 R1 S1 T1 U1 V1 W1 X1 Y1 Z1 A2 B2) (RULES f3(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1, X1, Y1, Z1, A2, B2) -> Com_1(f4(C2, I2, H2, M2, F2, F, G, H, I, J2, K, L, M, 1, J, O2, N2, P2, S, T, U, V, W, X, Y, Z, A1, B1, Q2, D1, E1, G2, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1, Q1, R1, D2, K2, E2, V1, W1, X1, Y1, Z1, A2, B2)) [ N = 1 ] f3(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1, X1, Y1, Z1, A2, B2) -> Com_1(f1(N, 2, D2, H2, D2, F, G, H, I, J, K, L, M, N, C2, P, Q, R, S, 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, C2, T1, D2, I2, W1, X1, Y1, Z1, A2, B2)) [ N >= 2 ] f3(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1, X1, Y1, Z1, A2, B2) -> Com_1(f4(C2, I2, H2, N2, M2, F, G, H, I, K2, K, L, M, J2, O, P2, O2, Q2, S, T, U, V, W, X, Y, Z, A1, B1, R2, D1, E1, E2, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1, Q1, R1, D2, G2, F2, V1, W1, X1, Y1, Z1, A2, B2)) [ 0 >= L2 /\ 0 >= N /\ 0 >= J2 ] f1(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1, X1, Y1, Z1, A2, B2) -> Com_1(f4(C2, I2, H2, N2, M2, F, G, H, I, K2, K, L, M, J2, O, P2, O2, Q2, S, T, U, V, W, X, Y, Z, A1, B1, R2, D1, E1, E2, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1, Q1, R1, D2, G2, F2, V1, W1, X1, Y1, Z1, A2, B2)) [ N - B >= 0 /\ A - B >= 0 /\ B - 2 >= 0 /\ N + B - 4 >= 0 /\ A + B - 4 >= 0 /\ A - N >= 0 /\ N - 2 >= 0 /\ A + N - 4 >= 0 /\ -A + N >= 0 /\ A - 2 >= 0 /\ L2 >= 2 /\ W1 >= L2 /\ J2 >= 2 /\ W1 >= J2 /\ B >= A /\ W1 >= 0 /\ B >= 0 /\ O = J ] f1(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1, X1, Y1, Z1, A2, B2) -> Com_1(f7(C2, I2, H2, M2, F2, F, G, H, I, J, J, E1, 0, J2, O, O, N2, J, N2, T, U, V, W, X, Y, Z, A1, B1, J, D1, E1, G2, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1, Q1, R1, D2, K2, E2, V1, E1 + 1, V, I, O2, P2, B2)) [ N - B >= 0 /\ A - B >= 0 /\ B - 2 >= 0 /\ N + B - 4 >= 0 /\ A + B - 4 >= 0 /\ A - N >= 0 /\ N - 2 >= 0 /\ A + N - 4 >= 0 /\ -A + N >= 0 /\ A - 2 >= 0 /\ Q2 >= 2 /\ W1 >= Q2 /\ J2 >= 2 /\ W1 >= J2 /\ K >= O + 1 /\ B >= A /\ B >= 0 /\ W1 >= 0 /\ M = 0 /\ J = K ] f1(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1, X1, Y1, Z1, A2, B2) -> Com_1(f7(C2, I2, H2, M2, F2, F, G, H, I, J, J, E1, 0, J2, O, O, N2, J, N2, T, U, V, W, X, Y, Z, A1, B1, J, D1, E1, G2, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1, Q1, R1, D2, K2, E2, V1, E1 + 1, V, I, O2, P2, B2)) [ N - B >= 0 /\ A - B >= 0 /\ B - 2 >= 0 /\ N + B - 4 >= 0 /\ A + B - 4 >= 0 /\ A - N >= 0 /\ N - 2 >= 0 /\ A + N - 4 >= 0 /\ -A + N >= 0 /\ A - 2 >= 0 /\ Q2 >= 2 /\ W1 >= Q2 /\ J2 >= 2 /\ W1 >= J2 /\ O >= K + 1 /\ B >= A /\ B >= 0 /\ W1 >= 0 /\ M = 0 /\ J = K ] f1(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1, X1, Y1, Z1, A2, B2) -> Com_1(f1(A, B + 1, D, C2, D, D2, B, I, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1, X1, Y1, Z1, A2, B2)) [ N - B >= 0 /\ A - B >= 0 /\ B - 2 >= 0 /\ N + B - 4 >= 0 /\ A + B - 4 >= 0 /\ A - N >= 0 /\ N - 2 >= 0 /\ A + N - 4 >= 0 /\ -A + N >= 0 /\ A - 2 >= 0 /\ A >= B + 1 /\ B >= 0 ] f7(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1, X1, Y1, Z1, A2, B2) -> Com_1(f7(A, B, C, D, E, F, G, H, I, J, K, L, M + 1, C2, P, P, D2, J, D2, T, U, V, W, X, Y, Z, A1, B1, J, D1, E1 - 1, F1, G1, H1, I1, J1, H2, I2, V, I, K, M + 1, E1 - 1, R1, S1, T1, U1, V1, W1, X1, Y1, Z1, A2, B2)) [ Y1 - I >= 0 /\ -Y1 + I >= 0 /\ V - X1 >= 0 /\ -V + X1 >= 0 /\ L - W1 + 1 >= 0 /\ -E1 + W1 - 1 >= 0 /\ -L + W1 - 1 >= 0 /\ L - E1 >= 0 /\ R - C1 >= 0 /\ K - C1 >= 0 /\ J - C1 >= 0 /\ -R + C1 >= 0 /\ -K + C1 >= 0 /\ -J + C1 >= 0 /\ K - R >= 0 /\ J - R >= 0 /\ -K + R >= 0 /\ -J + R >= 0 /\ O - P >= 0 /\ -O + P >= 0 /\ N - 2 >= 0 /\ M + N - 2 >= 0 /\ M >= 0 /\ J - K >= 0 /\ -J + K >= 0 /\ K2 >= J2 + 1 /\ J >= J2 + 1 /\ I2 >= J2 + 1 /\ K >= J2 + 1 /\ G2 >= 0 /\ C2 >= 2 /\ E1 >= 0 ] f7(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1, X1, Y1, Z1, A2, B2) -> Com_1(f7(A, B, C, D, E, F, G, H, I, J, K, L, M + 1, C2, P, P, D2, J, D2, T, U, V, W, X, Y, Z, A1, B1, J, D1, E1 - 1, F1, G1, H1, I1, J1, H2, I2, V, I, K, M + 1, E1 - 1, R1, S1, T1, U1, V1, W1, X1, Y1, Z1, A2, B2)) [ Y1 - I >= 0 /\ -Y1 + I >= 0 /\ V - X1 >= 0 /\ -V + X1 >= 0 /\ L - W1 + 1 >= 0 /\ -E1 + W1 - 1 >= 0 /\ -L + W1 - 1 >= 0 /\ L - E1 >= 0 /\ R - C1 >= 0 /\ K - C1 >= 0 /\ J - C1 >= 0 /\ -R + C1 >= 0 /\ -K + C1 >= 0 /\ -J + C1 >= 0 /\ K - R >= 0 /\ J - R >= 0 /\ -K + R >= 0 /\ -J + R >= 0 /\ O - P >= 0 /\ -O + P >= 0 /\ N - 2 >= 0 /\ M + N - 2 >= 0 /\ M >= 0 /\ J - K >= 0 /\ -J + K >= 0 /\ K2 >= J2 + 1 /\ J >= J2 + 1 /\ J2 >= I2 + 1 /\ K >= J2 + 1 /\ G2 >= 0 /\ C2 >= 2 /\ E1 >= 0 ] f7(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1, X1, Y1, Z1, A2, B2) -> Com_1(f7(A, B, C, D, E, F, G, H, I, J, K, L, M + 1, C2, P, P, D2, J, D2, T, U, V, W, X, Y, Z, A1, B1, J, D1, E1 - 1, F1, G1, H1, I1, J1, H2, I2, V, I, K, M + 1, E1 - 1, R1, S1, T1, U1, V1, W1, X1, Y1, Z1, A2, B2)) [ Y1 - I >= 0 /\ -Y1 + I >= 0 /\ V - X1 >= 0 /\ -V + X1 >= 0 /\ L - W1 + 1 >= 0 /\ -E1 + W1 - 1 >= 0 /\ -L + W1 - 1 >= 0 /\ L - E1 >= 0 /\ R - C1 >= 0 /\ K - C1 >= 0 /\ J - C1 >= 0 /\ -R + C1 >= 0 /\ -K + C1 >= 0 /\ -J + C1 >= 0 /\ K - R >= 0 /\ J - R >= 0 /\ -K + R >= 0 /\ -J + R >= 0 /\ O - P >= 0 /\ -O + P >= 0 /\ N - 2 >= 0 /\ M + N - 2 >= 0 /\ M >= 0 /\ J - K >= 0 /\ -J + K >= 0 /\ K2 >= J2 + 1 /\ J2 >= J + 1 /\ I2 >= J2 + 1 /\ J2 >= K + 1 /\ G2 >= 0 /\ C2 >= 2 /\ E1 >= 0 ] f7(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1, X1, Y1, Z1, A2, B2) -> Com_1(f7(A, B, C, D, E, F, G, H, I, J, K, L, M + 1, C2, P, P, D2, J, D2, T, U, V, W, X, Y, Z, A1, B1, J, D1, E1 - 1, F1, G1, H1, I1, J1, H2, I2, V, I, K, M + 1, E1 - 1, R1, S1, T1, U1, V1, W1, X1, Y1, Z1, A2, B2)) [ Y1 - I >= 0 /\ -Y1 + I >= 0 /\ V - X1 >= 0 /\ -V + X1 >= 0 /\ L - W1 + 1 >= 0 /\ -E1 + W1 - 1 >= 0 /\ -L + W1 - 1 >= 0 /\ L - E1 >= 0 /\ R - C1 >= 0 /\ K - C1 >= 0 /\ J - C1 >= 0 /\ -R + C1 >= 0 /\ -K + C1 >= 0 /\ -J + C1 >= 0 /\ K - R >= 0 /\ J - R >= 0 /\ -K + R >= 0 /\ -J + R >= 0 /\ O - P >= 0 /\ -O + P >= 0 /\ N - 2 >= 0 /\ M + N - 2 >= 0 /\ M >= 0 /\ J - K >= 0 /\ -J + K >= 0 /\ K2 >= J2 + 1 /\ J2 >= J + 1 /\ J2 >= I2 + 1 /\ J2 >= K + 1 /\ G2 >= 0 /\ C2 >= 2 /\ E1 >= 0 ] f7(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1, X1, Y1, Z1, A2, B2) -> Com_1(f7(A, B, C, D, E, F, G, H, I, J, K, L, M + 1, C2, P, P, D2, J, D2, T, U, V, W, X, Y, Z, A1, B1, J, D1, E1 - 1, F1, G1, H1, I1, J1, H2, I2, V, I, K, M + 1, E1 - 1, R1, S1, T1, U1, V1, W1, X1, Y1, Z1, A2, B2)) [ Y1 - I >= 0 /\ -Y1 + I >= 0 /\ V - X1 >= 0 /\ -V + X1 >= 0 /\ L - W1 + 1 >= 0 /\ -E1 + W1 - 1 >= 0 /\ -L + W1 - 1 >= 0 /\ L - E1 >= 0 /\ R - C1 >= 0 /\ K - C1 >= 0 /\ J - C1 >= 0 /\ -R + C1 >= 0 /\ -K + C1 >= 0 /\ -J + C1 >= 0 /\ K - R >= 0 /\ J - R >= 0 /\ -K + R >= 0 /\ -J + R >= 0 /\ O - P >= 0 /\ -O + P >= 0 /\ N - 2 >= 0 /\ M + N - 2 >= 0 /\ M >= 0 /\ J - K >= 0 /\ -J + K >= 0 /\ J2 >= K2 + 1 /\ J >= J2 + 1 /\ I2 >= J2 + 1 /\ K >= J2 + 1 /\ G2 >= 0 /\ C2 >= 2 /\ E1 >= 0 ] f7(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1, X1, Y1, Z1, A2, B2) -> Com_1(f7(A, B, C, D, E, F, G, H, I, J, K, L, M + 1, C2, P, P, D2, J, D2, T, U, V, W, X, Y, Z, A1, B1, J, D1, E1 - 1, F1, G1, H1, I1, J1, H2, I2, V, I, K, M + 1, E1 - 1, R1, S1, T1, U1, V1, W1, X1, Y1, Z1, A2, B2)) [ Y1 - I >= 0 /\ -Y1 + I >= 0 /\ V - X1 >= 0 /\ -V + X1 >= 0 /\ L - W1 + 1 >= 0 /\ -E1 + W1 - 1 >= 0 /\ -L + W1 - 1 >= 0 /\ L - E1 >= 0 /\ R - C1 >= 0 /\ K - C1 >= 0 /\ J - C1 >= 0 /\ -R + C1 >= 0 /\ -K + C1 >= 0 /\ -J + C1 >= 0 /\ K - R >= 0 /\ J - R >= 0 /\ -K + R >= 0 /\ -J + R >= 0 /\ O - P >= 0 /\ -O + P >= 0 /\ N - 2 >= 0 /\ M + N - 2 >= 0 /\ M >= 0 /\ J - K >= 0 /\ -J + K >= 0 /\ J2 >= K2 + 1 /\ J >= J2 + 1 /\ J2 >= I2 + 1 /\ K >= J2 + 1 /\ G2 >= 0 /\ C2 >= 2 /\ E1 >= 0 ] f7(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1, X1, Y1, Z1, A2, B2) -> Com_1(f7(A, B, C, D, E, F, G, H, I, J, K, L, M + 1, C2, P, P, D2, J, D2, T, U, V, W, X, Y, Z, A1, B1, J, D1, E1 - 1, F1, G1, H1, I1, J1, H2, I2, V, I, K, M + 1, E1 - 1, R1, S1, T1, U1, V1, W1, X1, Y1, Z1, A2, B2)) [ Y1 - I >= 0 /\ -Y1 + I >= 0 /\ V - X1 >= 0 /\ -V + X1 >= 0 /\ L - W1 + 1 >= 0 /\ -E1 + W1 - 1 >= 0 /\ -L + W1 - 1 >= 0 /\ L - E1 >= 0 /\ R - C1 >= 0 /\ K - C1 >= 0 /\ J - C1 >= 0 /\ -R + C1 >= 0 /\ -K + C1 >= 0 /\ -J + C1 >= 0 /\ K - R >= 0 /\ J - R >= 0 /\ -K + R >= 0 /\ -J + R >= 0 /\ O - P >= 0 /\ -O + P >= 0 /\ N - 2 >= 0 /\ M + N - 2 >= 0 /\ M >= 0 /\ J - K >= 0 /\ -J + K >= 0 /\ J2 >= K2 + 1 /\ J2 >= J + 1 /\ I2 >= J2 + 1 /\ J2 >= K + 1 /\ G2 >= 0 /\ C2 >= 2 /\ E1 >= 0 ] f7(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1, X1, Y1, Z1, A2, B2) -> Com_1(f7(A, B, C, D, E, F, G, H, I, J, K, L, M + 1, C2, P, P, D2, J, D2, T, U, V, W, X, Y, Z, A1, B1, J, D1, E1 - 1, F1, G1, H1, I1, J1, H2, I2, V, I, K, M + 1, E1 - 1, R1, S1, T1, U1, V1, W1, X1, Y1, Z1, A2, B2)) [ Y1 - I >= 0 /\ -Y1 + I >= 0 /\ V - X1 >= 0 /\ -V + X1 >= 0 /\ L - W1 + 1 >= 0 /\ -E1 + W1 - 1 >= 0 /\ -L + W1 - 1 >= 0 /\ L - E1 >= 0 /\ R - C1 >= 0 /\ K - C1 >= 0 /\ J - C1 >= 0 /\ -R + C1 >= 0 /\ -K + C1 >= 0 /\ -J + C1 >= 0 /\ K - R >= 0 /\ J - R >= 0 /\ -K + R >= 0 /\ -J + R >= 0 /\ O - P >= 0 /\ -O + P >= 0 /\ N - 2 >= 0 /\ M + N - 2 >= 0 /\ M >= 0 /\ J - K >= 0 /\ -J + K >= 0 /\ J2 >= K2 + 1 /\ J2 >= J + 1 /\ J2 >= I2 + 1 /\ J2 >= K + 1 /\ G2 >= 0 /\ C2 >= 2 /\ E1 >= 0 ] f7(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1, X1, Y1, Z1, A2, B2) -> Com_1(f4(A, B, C, D, E, F, G, H, I, H2, K, L, M, C2, D2, K2, J2, G2, S, T, U, V, W, X, Y, Z, A1, B1, E2, D1, E1, I2, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1, Q1, F2, S1, T1, U1, V1, W1, X1, Y1, Z1, A2, B2)) [ Y1 - I >= 0 /\ -Y1 + I >= 0 /\ V - X1 >= 0 /\ -V + X1 >= 0 /\ L - W1 + 1 >= 0 /\ -E1 + W1 - 1 >= 0 /\ -L + W1 - 1 >= 0 /\ L - E1 >= 0 /\ R - C1 >= 0 /\ K - C1 >= 0 /\ J - C1 >= 0 /\ -R + C1 >= 0 /\ -K + C1 >= 0 /\ -J + C1 >= 0 /\ K - R >= 0 /\ J - R >= 0 /\ -K + R >= 0 /\ -J + R >= 0 /\ O - P >= 0 /\ -O + P >= 0 /\ N - 2 >= 0 /\ M + N - 2 >= 0 /\ M >= 0 /\ J - K >= 0 /\ -J + K >= 0 /\ E1 >= 0 /\ C2 >= 2 /\ F2 >= D2 + 1 /\ K >= D2 + 1 /\ J = P ] f7(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1, X1, Y1, Z1, A2, B2) -> Com_1(f4(A, B, C, D, E, F, G, H, I, H2, K, L, M, C2, D2, K2, J2, G2, S, T, U, V, W, X, Y, Z, A1, B1, E2, D1, E1, I2, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1, Q1, F2, S1, T1, U1, V1, W1, X1, Y1, Z1, A2, B2)) [ Y1 - I >= 0 /\ -Y1 + I >= 0 /\ V - X1 >= 0 /\ -V + X1 >= 0 /\ L - W1 + 1 >= 0 /\ -E1 + W1 - 1 >= 0 /\ -L + W1 - 1 >= 0 /\ L - E1 >= 0 /\ R - C1 >= 0 /\ K - C1 >= 0 /\ J - C1 >= 0 /\ -R + C1 >= 0 /\ -K + C1 >= 0 /\ -J + C1 >= 0 /\ K - R >= 0 /\ J - R >= 0 /\ -K + R >= 0 /\ -J + R >= 0 /\ O - P >= 0 /\ -O + P >= 0 /\ N - 2 >= 0 /\ M + N - 2 >= 0 /\ M >= 0 /\ J - K >= 0 /\ -J + K >= 0 /\ E1 >= 0 /\ C2 >= 2 /\ F2 >= D2 + 1 /\ D2 >= K + 1 /\ J = P ] f7(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1, X1, Y1, Z1, A2, B2) -> Com_1(f4(A, B, C, D, E, F, G, H, I, H2, K, L, M, C2, D2, K2, J2, G2, S, T, U, V, W, X, Y, Z, A1, B1, E2, D1, E1, I2, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1, Q1, F2, S1, T1, U1, V1, W1, X1, Y1, Z1, A2, B2)) [ Y1 - I >= 0 /\ -Y1 + I >= 0 /\ V - X1 >= 0 /\ -V + X1 >= 0 /\ L - W1 + 1 >= 0 /\ -E1 + W1 - 1 >= 0 /\ -L + W1 - 1 >= 0 /\ L - E1 >= 0 /\ R - C1 >= 0 /\ K - C1 >= 0 /\ J - C1 >= 0 /\ -R + C1 >= 0 /\ -K + C1 >= 0 /\ -J + C1 >= 0 /\ K - R >= 0 /\ J - R >= 0 /\ -K + R >= 0 /\ -J + R >= 0 /\ O - P >= 0 /\ -O + P >= 0 /\ N - 2 >= 0 /\ M + N - 2 >= 0 /\ M >= 0 /\ J - K >= 0 /\ -J + K >= 0 /\ E1 >= 0 /\ C2 >= 2 /\ D2 >= F2 + 1 /\ K >= D2 + 1 /\ J = P ] f7(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1, X1, Y1, Z1, A2, B2) -> Com_1(f4(A, B, C, D, E, F, G, H, I, H2, K, L, M, C2, D2, K2, J2, G2, S, T, U, V, W, X, Y, Z, A1, B1, E2, D1, E1, I2, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1, Q1, F2, S1, T1, U1, V1, W1, X1, Y1, Z1, A2, B2)) [ Y1 - I >= 0 /\ -Y1 + I >= 0 /\ V - X1 >= 0 /\ -V + X1 >= 0 /\ L - W1 + 1 >= 0 /\ -E1 + W1 - 1 >= 0 /\ -L + W1 - 1 >= 0 /\ L - E1 >= 0 /\ R - C1 >= 0 /\ K - C1 >= 0 /\ J - C1 >= 0 /\ -R + C1 >= 0 /\ -K + C1 >= 0 /\ -J + C1 >= 0 /\ K - R >= 0 /\ J - R >= 0 /\ -K + R >= 0 /\ -J + R >= 0 /\ O - P >= 0 /\ -O + P >= 0 /\ N - 2 >= 0 /\ M + N - 2 >= 0 /\ M >= 0 /\ J - K >= 0 /\ -J + K >= 0 /\ E1 >= 0 /\ C2 >= 2 /\ D2 >= F2 + 1 /\ D2 >= K + 1 /\ J = P ] )