(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 X Y Z A1) (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, X, Y, Z, A1) -> Com_1(f13(A, 0, 0, 2*A, 4*A, 4*A + 3, 4*A + 4, A, C1, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1)) [ 1 >= A*B1 /\ A*B1 + B1 >= 2 /\ C1 >= B1 /\ 1 >= A*D1 /\ A*D1 + D1 >= 2 /\ D1 >= C1 ] f13(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1) -> Com_1(f24(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1)) [ A - H >= 0 /\ -A + H >= 0 /\ -C >= 0 /\ C >= 0 /\ J >= D + 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, X, Y, Z, A1) -> Com_1(f13(A, B - 2*C1 + C1^2 + 1, C, D, E, F, G, H, I, J + 1, C1, -C1 + 1, -2*C1 + C1^2 + 1, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1)) [ A - H >= 0 /\ -A + H >= 0 /\ -C >= 0 /\ C >= 0 /\ 0 >= C1 /\ D >= J ] f13(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1) -> Com_1(f13(A, B - 2*C1 + C1^2 + 1, C, D, E, F, G, H, I, J + 1, C1, -C1 + 1, -2*C1 + C1^2 + 1, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1)) [ A - H >= 0 /\ -A + H >= 0 /\ -C >= 0 /\ C >= 0 /\ C1 >= 2 /\ D >= J ] f13(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1) -> Com_1(f13(A, B, C, D, E, F, G, H, I, J + 1, 1, 0, 0, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1)) [ A - H >= 0 /\ -A + H >= 0 /\ -C >= 0 /\ C >= 0 /\ D >= J ] f24(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1) -> Com_1(f37(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, 0, Q, R, S, T, U, V, W, X, Y, Z, A1)) [ A - H >= 0 /\ -A + H >= 0 /\ J - D - 1 >= 0 /\ -C >= 0 /\ C >= 0 /\ J >= A + 1 /\ P = 0 ] f24(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1) -> Com_1(f31(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1)) [ A - H >= 0 /\ -A + H >= 0 /\ J - D - 1 >= 0 /\ -C >= 0 /\ C >= 0 /\ P >= 1 /\ J >= A + 1 ] f24(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1) -> Com_1(f31(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1)) [ A - H >= 0 /\ -A + H >= 0 /\ J - D - 1 >= 0 /\ -C >= 0 /\ C >= 0 /\ 0 >= P + 1 /\ J >= A + 1 ] f24(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1) -> Com_1(f24(A, B, C, D, E, F, G, H, I, J + 1, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1)) [ A - H >= 0 /\ -A + H >= 0 /\ J - D - 1 >= 0 /\ -C >= 0 /\ C >= 0 /\ A >= J ] f37(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1) -> Com_1(f118(A, B, C*E, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1)) [ J - H - 1 >= 0 /\ A - H >= 0 /\ -A + H >= 0 /\ J - D - 1 >= 0 /\ -A + J - 1 >= 0 /\ O >= N + 1 ] f37(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1) -> Com_1(f40(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1)) [ J - H - 1 >= 0 /\ A - H >= 0 /\ -A + H >= 0 /\ J - D - 1 >= 0 /\ -A + J - 1 >= 0 /\ N >= O ] f31(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1) -> Com_1(f37(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1)) [ J - H - 1 >= 0 /\ A - H >= 0 /\ -A + H >= 0 /\ J - D - 1 >= 0 /\ -C >= 0 /\ C >= 0 /\ -A + J - 1 >= 0 /\ J >= A + 1 ] f118(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1) -> 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, X, Y, Z, A1)) [ J - H - 1 >= 0 /\ A - H >= 0 /\ -A + H >= 0 /\ J - D - 1 >= 0 /\ -N + O - 1 >= 0 /\ -A + J - 1 >= 0 /\ J >= A + 1 ] f40(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1) -> Com_1(f71(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1)) [ J - H - 1 >= 0 /\ A - H >= 0 /\ -A + H >= 0 /\ J - D - 1 >= 0 /\ N - O >= 0 /\ -A + J - 1 >= 0 /\ Q >= 1 ] f40(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1) -> Com_1(f64(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, 0, Q, R, S, T, U, V, W, X, Y, Z, A1)) [ J - H - 1 >= 0 /\ A - H >= 0 /\ -A + H >= 0 /\ J - D - 1 >= 0 /\ N - O >= 0 /\ -A + J - 1 >= 0 /\ 0 >= Q /\ P = 0 ] f40(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1) -> Com_1(f44(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1)) [ J - H - 1 >= 0 /\ A - H >= 0 /\ -A + H >= 0 /\ J - D - 1 >= 0 /\ N - O >= 0 /\ -A + J - 1 >= 0 /\ P >= 1 /\ 0 >= Q ] f40(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1) -> Com_1(f44(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1)) [ J - H - 1 >= 0 /\ A - H >= 0 /\ -A + H >= 0 /\ J - D - 1 >= 0 /\ N - O >= 0 /\ -A + J - 1 >= 0 /\ 0 >= P + 1 /\ 0 >= Q ] f71(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1) -> Com_1(f86(A, B, C, D, E, F, G, H, I, J, K, C1, M, N, O, P, Q, R, S, T, U, V, W, X, Y, B1^2, A1)) [ J - H - 1 >= 0 /\ A - H >= 0 /\ -A + H >= 0 /\ J - D - 1 >= 0 /\ Q - 1 >= 0 /\ N - O >= 0 /\ -A + J - 1 >= 0 /\ B1 >= 1 /\ J >= D + 1 ] f71(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1) -> Com_1(f86(A, B, C, D, E, F, G, H, I, J, K, C1, M, N, O, P, Q, R, S, T, U, V, W, X, Y, B1^2, A1)) [ J - H - 1 >= 0 /\ A - H >= 0 /\ -A + H >= 0 /\ J - D - 1 >= 0 /\ Q - 1 >= 0 /\ N - O >= 0 /\ -A + J - 1 >= 0 /\ 0 >= B1 + 1 /\ J >= D + 1 ] f71(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1) -> Com_1(f86(A, B, C, D, E, F, G, H, I, J, K, C1, M, N, O, P, Q, R, S, T, U, V, W, X, Y, 0, A1)) [ J - H - 1 >= 0 /\ A - H >= 0 /\ -A + H >= 0 /\ J - D - 1 >= 0 /\ Q - 1 >= 0 /\ N - O >= 0 /\ -A + J - 1 >= 0 /\ J >= D + 1 ] f64(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1) -> Com_1(f40(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q + 1, R, S, T, U, V, W, X, Y, Z, A1)) [ J - H - 1 >= 0 /\ A - H >= 0 /\ -A + H >= 0 /\ J - D - 1 >= 0 /\ -Q >= 0 /\ P - Q >= 0 /\ -P - Q >= 0 /\ -P >= 0 /\ P >= 0 /\ N - O >= 0 /\ -A + J - 1 >= 0 /\ J >= E + 1 ] f64(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1) -> Com_1(f64(A, B, C, D, E, F, G, H, I, J + 2, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1)) [ J - H - 1 >= 0 /\ A - H >= 0 /\ -A + H >= 0 /\ J - D - 1 >= 0 /\ -Q >= 0 /\ P - Q >= 0 /\ -P - Q >= 0 /\ -P >= 0 /\ P >= 0 /\ N - O >= 0 /\ -A + J - 1 >= 0 /\ E >= J ] f44(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1) -> Com_1(f50(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1)) [ J - H - 1 >= 0 /\ A - H >= 0 /\ -A + H >= 0 /\ J - D - 1 >= 0 /\ -Q >= 0 /\ N - O >= 0 /\ -A + J - 1 >= 0 /\ J >= A + 1 ] f50(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1) -> Com_1(f57(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, Q + D)) [ J - H - 1 >= 0 /\ A - H >= 0 /\ -A + H >= 0 /\ J - D - 1 >= 0 /\ -Q >= 0 /\ N - O >= 0 /\ -A + J - 1 >= 0 /\ J >= A + 1 ] f86(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1) -> Com_1(f91(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, L^2, V, W, X, Y, Z, A1)) [ J - H - 1 >= 0 /\ A - H >= 0 /\ -A + H >= 0 /\ J - D - 1 >= 0 /\ Q - 1 >= 0 /\ N - O >= 0 /\ -A + J - 1 >= 0 /\ L >= 1 ] f86(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1) -> Com_1(f91(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, L^2, V, W, X, Y, Z, A1)) [ J - H - 1 >= 0 /\ A - H >= 0 /\ -A + H >= 0 /\ J - D - 1 >= 0 /\ Q - 1 >= 0 /\ N - O >= 0 /\ -A + J - 1 >= 0 /\ 0 >= L + 1 ] f86(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1) -> Com_1(f91(A, B, C, D, E, F, G, H, I, J, K, 0, M, N, O, P, Q, R, S, T, 0, V, W, X, Y, Z, A1)) [ J - H - 1 >= 0 /\ A - H >= 0 /\ -A + H >= 0 /\ J - D - 1 >= 0 /\ Q - 1 >= 0 /\ N - O >= 0 /\ -A + J - 1 >= 0 /\ L = 0 ] f57(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1) -> Com_1(f40(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q + 1, R, S, T, U, V, W, X, Y, Z, A1)) [ J - H - 1 >= 0 /\ A - H >= 0 /\ -A + H >= 0 /\ J - D - 1 >= 0 /\ -A1 + D >= 0 /\ J - A1 - 1 >= 0 /\ -Q >= 0 /\ N - O >= 0 /\ -A + J - 1 >= 0 /\ J >= A + 1 ] f91(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1) -> Com_1(f37(A, B, C + B, D, E, F, G, H, I, J, K, L, M, N, O + 1, P, Q, R, S, T, U, V, W, X, Y, Z, A1)) [ J - H - 1 >= 0 /\ A - H >= 0 /\ -A + H >= 0 /\ J - D - 1 >= 0 /\ Q - 1 >= 0 /\ N - O >= 0 /\ -A + J - 1 >= 0 /\ J >= A + 1 ] )