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