(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS f2)) (VAR A B C D E F G H I J K L M N O P Q R S T U V W) (RULES f2(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f13(1, X, Y, Z, A1, B1, C1, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W)) [ A = 1 ] f13(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f16(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W)) [ -A + 1 >= 0 /\ A - 1 >= 0 /\ H >= I ] f16(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f16(A, B, C, D, E, F, G, H, I, J, K + 1, L + 2, M, N, O, P, Q, R, S, T, U, V, W)) [ H - I >= 0 /\ -A + 1 >= 0 /\ A - 1 >= 0 /\ J >= K ] f2(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f27(A, X, Y, Z, A1, B1, C1, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W)) [ 0 >= A ] f2(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f27(A, X, Y, Z, A1, B1, C1, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W)) [ A >= 2 ] f27(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f35(A, B, C, D, E, F, G, H, I, J, K, L, H - I + 2, 1, 0, P, Q, R, S, T, U, V, W)) [ 0 >= I /\ H >= I ] f27(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f35(A, B, C, D, E, F, G, H, I, J, K, L, H - I + 2, 1, 0, P, Q, R, S, T, U, V, W)) [ I >= 2 /\ H >= I ] f27(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f35(A, B, C, D, E, F, G, H, 1, J, K, L, 1, 1, 0, P, Q, R, S, T, U, V, W)) [ H >= 1 /\ I = 1 ] f35(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f38(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W)) [ H - I >= 0 /\ P >= 2*X /\ 3*X >= P + 1 /\ X + 1 >= Q ] f38(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f53(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W)) [ H - I >= 0 /\ 0 >= Q /\ J >= K ] f38(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f53(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W)) [ H - I >= 0 /\ Q >= 2 /\ J >= K ] f38(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f38(A, B, C, D, E, F, G, H, I, J, K + 1, X + 3, M, N, O, P, 1, B*Y + B*Z, A1*B - B*B1, C*C1 - C*D1, -C*E1 - C*F1, V, W)) [ H - I >= 0 /\ J >= K + 4*X /\ 5*X + K >= J + 1 /\ 0 >= K /\ J >= K /\ Q = 1 ] f38(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f38(A, B, C, D, E, F, G, H, I, J, K + 1, X + 3, M, N, O, P, 1, B*Y + B*Z, A1*B - B*B1, C*C1 - C*D1, -C*E1 - C*F1, V, W)) [ H - I >= 0 /\ J >= K + 4*X /\ 5*X + K >= J + 1 /\ J >= K /\ K >= 2 /\ Q = 1 ] f38(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f38(A, B, C, D, E, F, G, H, I, J, 2, 1, M, N, O, P, 1, B*X + B*Y, B*Z - A1*B, B1*C - C*C1, -C*D1 - C*E1, V, W)) [ H - I >= 0 /\ J >= 1 /\ K = 1 /\ Q = 1 ] f53(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f38(A, B, C, D, E, F, G, H, I, J, K + 1, J - K + 2, M, N, O, P, Q, B*X + B*Y, B*Z - A1*B, B1*C - C*C1, -C*D1 - C*E1, P - F1 + 3, W)) [ H - I >= 0 /\ J - K >= 0 /\ Q >= 2*F1 /\ 3*F1 >= Q + 1 /\ 0 >= K ] f53(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f38(A, B, C, D, E, F, G, H, I, J, K + 1, J - K + 2, M, N, O, P, Q, B*X + B*Y, B*Z - A1*B, B1*C - C*C1, -C*D1 - C*E1, P - F1 + 3, W)) [ H - I >= 0 /\ J - K >= 0 /\ Q >= 2*F1 /\ 3*F1 >= Q + 1 /\ K >= 2 ] f53(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f38(A, B, C, D, E, F, G, H, I, J, 2, 1, M, N, O, P, Q, B*X + B*Y, B*Z - A1*B, B1*C - C*C1, -C*D1 - C*E1, P - F1 + 3, W)) [ H - I >= 0 /\ J - K >= 0 /\ Q >= 2*F1 /\ 3*F1 >= Q + 1 /\ K = 1 ] f38(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f35(A, B, C, D, N, F, G, H, I, J, K, L, M, F*N - G*O + N, F*O + G*N + O, P, Q + 1, R, S, T, U, V, W + 2)) [ H - I >= 0 /\ K >= J + 1 ] f35(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f27(A, B, C, D, E, F, G, H, I + 1, J, K, L, M, N, O, P, Q, R, S, T, U, V, W)) [ H - I >= 0 /\ P >= 2*X /\ 3*X >= P + 1 /\ Q >= X + 2 ] f27(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f1(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W)) [ 0 >= A + 2 /\ I >= H + 1 ] f27(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f1(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W)) [ A >= 0 /\ I >= H + 1 ] f27(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f1(-1, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W)) [ I >= H + 1 /\ A + 1 = 0 ] f16(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f13(A, B, C, D, E, F, G, H, I + 1, J, K, L, M, N, O, P, Q, R, S, T, U, V, W)) [ H - I >= 0 /\ -A + 1 >= 0 /\ A - 1 >= 0 /\ K >= J + 1 ] f13(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f27(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W)) [ -A + 1 >= 0 /\ A - 1 >= 0 /\ I >= H + 1 ] )