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