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