(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(f11(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, 0, 0)) f11(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T) -> Com_1(f11(A + 1, B, C, 1, E, U, V, W, X, C, U, U, U, O, O, 1, 1, 0, S, T)) [ -T >= 0 /\ S - T >= 0 /\ -S - T >= 0 /\ T >= 0 /\ S + T >= 0 /\ -S + T >= 0 /\ -S >= 0 /\ S >= 0 /\ 0 >= U /\ B >= A + 1 ] f11(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T) -> Com_1(f35(A, B, C, Y, E, U, V, W, X, C, U, U, U, O, 0, Y, Y, 0, S, T)) [ -T >= 0 /\ S - T >= 0 /\ -S - T >= 0 /\ T >= 0 /\ S + T >= 0 /\ -S + T >= 0 /\ -S >= 0 /\ S >= 0 /\ B >= A + 1 /\ 0 >= U /\ 0 >= Y ] f11(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T) -> Com_1(f35(A, B, C, Y, E, U, V, W, X, C, U, U, U, O, 0, Y, Y, 0, S, T)) [ -T >= 0 /\ S - T >= 0 /\ -S - T >= 0 /\ T >= 0 /\ S + T >= 0 /\ -S + T >= 0 /\ -S >= 0 /\ S >= 0 /\ B >= A + 1 /\ 0 >= U /\ Y >= 2 ] f11(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T) -> Com_1(f47(A, B, 0, D, E, U, V, W, X, C, U, U, M, N, O, P, Q, R, S, T)) [ -T >= 0 /\ S - T >= 0 /\ -S - T >= 0 /\ T >= 0 /\ S + T >= 0 /\ -S + T >= 0 /\ -S >= 0 /\ S >= 0 /\ U >= 1 /\ B >= A + 1 ] f11(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T) -> Com_1(f47(A, B, 0, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T)) [ -T >= 0 /\ S - T >= 0 /\ -S - T >= 0 /\ T >= 0 /\ S + T >= 0 /\ -S + T >= 0 /\ -S >= 0 /\ S >= 0 /\ A >= B ] f35(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T) -> Com_1(f47(A, B, 0, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T)) [ J - C >= 0 /\ -J + C >= 0 /\ -T >= 0 /\ S - T >= 0 /\ -S - T >= 0 /\ R - T >= 0 /\ -R - T >= 0 /\ O - T >= 0 /\ -O - T >= 0 /\ -M - T >= 0 /\ T >= 0 /\ S + T >= 0 /\ -S + T >= 0 /\ R + T >= 0 /\ -R + T >= 0 /\ O + T >= 0 /\ -O + T >= 0 /\ -M + T >= 0 /\ -A + B - 1 >= 0 /\ -S >= 0 /\ R - S >= 0 /\ -R - S >= 0 /\ O - S >= 0 /\ -O - S >= 0 /\ -M - S >= 0 /\ S >= 0 /\ R + S >= 0 /\ -R + S >= 0 /\ O + S >= 0 /\ -O + S >= 0 /\ -M + S >= 0 /\ -R >= 0 /\ O - R >= 0 /\ -O - R >= 0 /\ -M - R >= 0 /\ R >= 0 /\ O + R >= 0 /\ -O + R >= 0 /\ -M + R >= 0 /\ -O >= 0 /\ -M - O >= 0 /\ O >= 0 /\ -M + O >= 0 /\ -M >= 0 /\ 1 >= D ] f35(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T) -> Com_1(f47(A, B, 0, 2, F, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T)) [ J - C >= 0 /\ -J + C >= 0 /\ -T >= 0 /\ S - T >= 0 /\ -S - T >= 0 /\ R - T >= 0 /\ -R - T >= 0 /\ O - T >= 0 /\ -O - T >= 0 /\ -M - T >= 0 /\ T >= 0 /\ S + T >= 0 /\ -S + T >= 0 /\ R + T >= 0 /\ -R + T >= 0 /\ O + T >= 0 /\ -O + T >= 0 /\ -M + T >= 0 /\ -A + B - 1 >= 0 /\ -S >= 0 /\ R - S >= 0 /\ -R - S >= 0 /\ O - S >= 0 /\ -O - S >= 0 /\ -M - S >= 0 /\ S >= 0 /\ R + S >= 0 /\ -R + S >= 0 /\ O + S >= 0 /\ -O + S >= 0 /\ -M + S >= 0 /\ -R >= 0 /\ O - R >= 0 /\ -O - R >= 0 /\ -M - R >= 0 /\ R >= 0 /\ O + R >= 0 /\ -O + R >= 0 /\ -M + R >= 0 /\ -O >= 0 /\ -M - O >= 0 /\ O >= 0 /\ -M + O >= 0 /\ -M >= 0 /\ D = 2 ] f35(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T) -> Com_1(f47(A, B, 0, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T)) [ J - C >= 0 /\ -J + C >= 0 /\ -T >= 0 /\ S - T >= 0 /\ -S - T >= 0 /\ R - T >= 0 /\ -R - T >= 0 /\ O - T >= 0 /\ -O - T >= 0 /\ -M - T >= 0 /\ T >= 0 /\ S + T >= 0 /\ -S + T >= 0 /\ R + T >= 0 /\ -R + T >= 0 /\ O + T >= 0 /\ -O + T >= 0 /\ -M + T >= 0 /\ -A + B - 1 >= 0 /\ -S >= 0 /\ R - S >= 0 /\ -R - S >= 0 /\ O - S >= 0 /\ -O - S >= 0 /\ -M - S >= 0 /\ S >= 0 /\ R + S >= 0 /\ -R + S >= 0 /\ O + S >= 0 /\ -O + S >= 0 /\ -M + S >= 0 /\ -R >= 0 /\ O - R >= 0 /\ -O - R >= 0 /\ -M - R >= 0 /\ R >= 0 /\ O + R >= 0 /\ -O + R >= 0 /\ -M + R >= 0 /\ -O >= 0 /\ -M - O >= 0 /\ O >= 0 /\ -M + O >= 0 /\ -M >= 0 /\ D >= 3 ] f47(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T) -> Com_1(f47(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T)) [ -C >= 0 /\ T - C >= 0 /\ -T - C >= 0 /\ S - C >= 0 /\ -S - C >= 0 /\ C >= 0 /\ T + C >= 0 /\ -T + C >= 0 /\ S + C >= 0 /\ -S + C >= 0 /\ -T >= 0 /\ S - T >= 0 /\ -S - T >= 0 /\ T >= 0 /\ S + T >= 0 /\ -S + T >= 0 /\ -S >= 0 /\ S >= 0 ] )