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