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