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