(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) (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) -> Com_1(f1(A, 2, Y, C1, Z, A1, B1, D1, E1, F1, Y, L, M, N, O, P, Q, R, S, T, U, V, W, G1)) [ A >= 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) -> Com_1(f4(D1, 0, 0, D, E, F, G, H, E1, J, K, L, M, C1, O, B1, Y, Z, A1, F1, U, V, W, X)) [ 0 >= D1 /\ 0 >= A ] 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) -> Com_1(f10(Y, U + 1, C, D, E, F, G, H, I, J, C, L, M, C, U, 0, C, 0, C, C, U, V, W, X)) [ A - B >= 0 /\ B - 2 >= 0 /\ A + B - 4 >= 0 /\ A - 2 >= 0 /\ B >= A /\ B >= 0 /\ Z >= Y /\ Y >= 2 /\ 0 >= C + 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) -> Com_1(f10(Y, U + 1, C, D, E, F, G, H, I, J, C, L, M, C, U, 0, C, 0, C, C, U, V, W, X)) [ A - B >= 0 /\ B - 2 >= 0 /\ A + B - 4 >= 0 /\ A - 2 >= 0 /\ B >= A /\ B >= 0 /\ Z >= Y /\ Y >= 2 /\ C >= 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) -> Com_1(f1(A, B + 1, D, B1, Y, Z, A1, C1, D1, E1, D, F1, B, N, O, P, Q, R, S, T, U, V, W, X)) [ A - B >= 0 /\ B - 2 >= 0 /\ A + B - 4 >= 0 /\ A - 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) -> Com_1(f10(A1, Z, Y, D, E, F, G, H, I, J, Y, L, M, N, O, 0, Y, 0, Y, N, U - 1, B1, U - 1, X)) [ O - U >= 0 /\ N - T >= 0 /\ -N + T >= 0 /\ -R >= 0 /\ P - R >= 0 /\ -P - R >= 0 /\ A - R - 2 >= 0 /\ R >= 0 /\ P + R >= 0 /\ -P + R >= 0 /\ A + R - 2 >= 0 /\ -P >= 0 /\ A - P - 2 >= 0 /\ P >= 0 /\ A + P - 2 >= 0 /\ A - 2 >= 0 /\ N >= C1 + 1 /\ U >= 0 /\ A1 >= 2 /\ Z >= A1 /\ C1 >= Y + 1 /\ P = 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) -> Com_1(f10(A1, Z, Y, D, E, F, G, H, I, J, Y, L, M, N, O, 0, Y, 0, Y, N, U - 1, B1, U - 1, X)) [ O - U >= 0 /\ N - T >= 0 /\ -N + T >= 0 /\ -R >= 0 /\ P - R >= 0 /\ -P - R >= 0 /\ A - R - 2 >= 0 /\ R >= 0 /\ P + R >= 0 /\ -P + R >= 0 /\ A + R - 2 >= 0 /\ -P >= 0 /\ A - P - 2 >= 0 /\ P >= 0 /\ A + P - 2 >= 0 /\ A - 2 >= 0 /\ N >= C1 + 1 /\ U >= 0 /\ A1 >= 2 /\ Z >= A1 /\ Y >= C1 + 1 /\ P = 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) -> Com_1(f10(A1, Z, Y, D, E, F, G, H, I, J, Y, L, M, N, O, 0, Y, 0, Y, N, U - 1, B1, U - 1, X)) [ O - U >= 0 /\ N - T >= 0 /\ -N + T >= 0 /\ -R >= 0 /\ P - R >= 0 /\ -P - R >= 0 /\ A - R - 2 >= 0 /\ R >= 0 /\ P + R >= 0 /\ -P + R >= 0 /\ A + R - 2 >= 0 /\ -P >= 0 /\ A - P - 2 >= 0 /\ P >= 0 /\ A + P - 2 >= 0 /\ A - 2 >= 0 /\ C1 >= N + 1 /\ U >= 0 /\ A1 >= 2 /\ Z >= A1 /\ C1 >= Y + 1 /\ P = 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) -> Com_1(f10(A1, Z, Y, D, E, F, G, H, I, J, Y, L, M, N, O, 0, Y, 0, Y, N, U - 1, B1, U - 1, X)) [ O - U >= 0 /\ N - T >= 0 /\ -N + T >= 0 /\ -R >= 0 /\ P - R >= 0 /\ -P - R >= 0 /\ A - R - 2 >= 0 /\ R >= 0 /\ P + R >= 0 /\ -P + R >= 0 /\ A + R - 2 >= 0 /\ -P >= 0 /\ A - P - 2 >= 0 /\ P >= 0 /\ A + P - 2 >= 0 /\ A - 2 >= 0 /\ C1 >= N + 1 /\ U >= 0 /\ A1 >= 2 /\ Z >= A1 /\ Y >= C1 + 1 /\ P = 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) -> Com_1(f4(D1, B, C, D, E, F, G, H, E1, J, K, L, M, C1, O, B1, Y, Z, A1, F1, U, V, W, X)) [ O - U >= 0 /\ N - T >= 0 /\ -N + T >= 0 /\ -R >= 0 /\ P - R >= 0 /\ -P - R >= 0 /\ A - R - 2 >= 0 /\ R >= 0 /\ P + R >= 0 /\ -P + R >= 0 /\ A + R - 2 >= 0 /\ -P >= 0 /\ A - P - 2 >= 0 /\ P >= 0 /\ A + P - 2 >= 0 /\ A - 2 >= 0 /\ D1 >= 2 /\ U >= 0 /\ P = N ] )