(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 W X Y Z A1 B1 C1 D1 E1 F1 G1 H1) (RULES f11(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, B1, C1, D1, E1, F1, G1, H1) -> Com_1(f11(A, B + 1, D, I1, D, J1, B, I, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1)) [ B - 2 >= 0 /\ K + B - 4 >= 0 /\ K - 2 >= 0 /\ A >= B + 1 /\ B >= 0 ] 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, B1, C1, D1, E1, F1, G1, H1) -> Com_1(f2(A, B, C, D, E, F, G, H, I, J, I1, J1, J, J1, J, Q, Q, I, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1)) [ H1 - 2 >= 0 /\ K + H1 - 4 >= 0 /\ M - O >= 0 /\ J - O >= 0 /\ -M + O >= 0 /\ -J + O >= 0 /\ J - M >= 0 /\ -J + M >= 0 /\ K - 2 >= 0 /\ 0 >= J + 1 /\ I1 >= 2 ] 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, B1, C1, D1, E1, F1, G1, H1) -> Com_1(f2(A, B, C, D, E, F, G, H, I, J, I1, J1, J, J1, J, Q, Q, I, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1)) [ H1 - 2 >= 0 /\ K + H1 - 4 >= 0 /\ M - O >= 0 /\ J - O >= 0 /\ -M + O >= 0 /\ -J + O >= 0 /\ J - M >= 0 /\ -J + M >= 0 /\ K - 2 >= 0 /\ J >= 1 /\ I1 >= 2 ] f5(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, B1, C1, D1, E1, F1, G1, H1) -> Com_1(f5(A, B, C, D, E, F, G, H, I, J, 1, I1, J, I1, J, P, Q, R, I, U, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1)) [ M - O >= 0 /\ J - O >= 0 /\ -M + O >= 0 /\ -J + O >= 0 /\ J - M >= 0 /\ -J + M >= 0 /\ -K + 1 >= 0 /\ K - 1 >= 0 /\ 0 >= J + 1 ] f5(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, B1, C1, D1, E1, F1, G1, H1) -> Com_1(f5(A, B, C, D, E, F, G, H, I, J, 1, I1, J, I1, J, P, Q, R, I, U, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1)) [ M - O >= 0 /\ J - O >= 0 /\ -M + O >= 0 /\ -J + O >= 0 /\ J - M >= 0 /\ -J + M >= 0 /\ -K + 1 >= 0 /\ K - 1 >= 0 /\ J >= 1 ] f0(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, B1, C1, D1, E1, F1, G1, H1) -> Com_1(f11(J1, 2, K1, L1, K1, F, G, H, I, J, J1, L, M, N, O, P, Q, R, S, T, U, I1, K1, M1, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1)) [ J1 >= 2 ] f0(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, B1, C1, D1, E1, F1, G1, H1) -> Com_1(f1(K1, M1, L1, U1, T1, F, G, H, I, P1, J1, V1, W1, N, X1, P, Q, R, S, T, U, I1, S1, X, D2, Q1, R1, Y1, Z1, A2, B2, C2, E2, H1)) [ 0 >= N1 /\ 0 >= J1 /\ 0 >= O1 /\ Y = 0 ] f0(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, B1, C1, D1, E1, F1, G1, H1) -> Com_1(f5(J1, L1, K1, S1, R1, F, G, H, I, J, 1, T1, J, T1, J, P, Q, R, S, T, U, I1, Q1, X, Y, M1, P1, B1, C1, D1, E1, F1, G1, H1)) [ 0 >= J + 1 ] f0(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, B1, C1, D1, E1, F1, G1, H1) -> Com_1(f5(J1, L1, K1, S1, R1, F, G, H, I, J, 1, T1, J, T1, J, P, Q, R, S, T, U, I1, Q1, X, Y, M1, P1, B1, C1, D1, E1, F1, G1, H1)) [ J >= 1 ] f11(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, B1, C1, D1, E1, F1, G1, H1) -> Com_1(f2(J1, L1, K1, S1, R1, F, G, H, I, J, I1, T1, J, T1, J, P, Q, R, S, T, U, V, Q1, X, Y, M1, P1, B1, C1, D1, E1, F1, G1, H1)) [ B - 2 >= 0 /\ K + B - 4 >= 0 /\ K - 2 >= 0 /\ U1 >= 2 /\ H1 >= U1 /\ V1 >= 2 /\ H1 >= V1 /\ B >= A /\ B >= 0 /\ I1 >= 2 /\ 0 >= J + 1 /\ H1 >= 0 ] f11(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, B1, C1, D1, E1, F1, G1, H1) -> Com_1(f2(J1, L1, K1, S1, R1, F, G, H, I, J, I1, T1, J, T1, J, P, Q, R, S, T, U, V, Q1, X, Y, M1, P1, B1, C1, D1, E1, F1, G1, H1)) [ B - 2 >= 0 /\ K + B - 4 >= 0 /\ K - 2 >= 0 /\ U1 >= 2 /\ H1 >= U1 /\ V1 >= 2 /\ H1 >= V1 /\ B >= A /\ B >= 0 /\ I1 >= 2 /\ J >= 1 /\ H1 >= 0 ] )