(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS f0)) (VAR A B C D E F G H I J K L M N O P Q R S T) (RULES f0(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T) -> Com_1(f7(8, 0, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T)) f7(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T) -> Com_1(f7(A, B + 1, U + V, W, X + Y, Z, A1 + B1, C1, D1 + E1, F1, U + V + D1 + E1, U + V - D1 - E1, X + Y + A1 + B1, X + Y - A1 - B1, -3196, G1, H1, I1 + J1, K1 + J1, J1)) [ B >= 0 /\ A + B - 8 >= 0 /\ -A + B + 8 >= 0 /\ -A + 8 >= 0 /\ A - 8 >= 0 /\ 7 >= B ] f62(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T) -> Com_1(f62(A, B + 1, U + V, W, X + Y, Z, A1 + B1, C1, D1 + E1, F1, U + V + D1 + E1, U + V - D1 - E1, X + Y + A1 + B1, X + Y - A1 - B1, -3196, G1, H1, I1 + J1, K1 + J1, J1)) [ B >= 0 /\ A + B - 8 >= 0 /\ -A + B + 8 >= 0 /\ -A + 8 >= 0 /\ A - 8 >= 0 /\ 7 >= B ] f62(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T) -> Com_1(f118(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T)) [ B >= 0 /\ A + B - 8 >= 0 /\ -A + B + 8 >= 0 /\ -A + 8 >= 0 /\ A - 8 >= 0 /\ B >= 8 ] f7(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T) -> Com_1(f62(A, 0, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T)) [ B >= 0 /\ A + B - 8 >= 0 /\ -A + B + 8 >= 0 /\ -A + 8 >= 0 /\ A - 8 >= 0 /\ B >= 8 ] )