(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS start)) (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) (RULES start(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) -> Com_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)) 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) -> 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, B1, C1)) [ B >= A + 1 /\ C >= 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) -> Com_1(f43(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)) [ B >= A + 1 /\ 0 >= C ] 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) -> Com_1(f0(A, B + 1, E1, D1, E1, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1)) [ A >= B /\ D1 >= C + 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) -> Com_1(f0(A, B + 1, C, D1, 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)) [ A >= B /\ C >= D1 ] 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, B1, C1) -> Com_1(f54(A, B, C, D, E, F, G, H, 1, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1)) [ C - 1 >= 0 /\ -A + B - 1 >= 0 /\ B >= A + 1 ] f54(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) -> Com_1(f43(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)) [ -I + 1 >= 0 /\ -A + B - 1 >= 0 /\ J >= 201 ] f54(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) -> 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, A1, B1, C1)) [ -I + 1 >= 0 /\ -A + B - 1 >= 0 /\ I >= 1 /\ 200 >= J ] 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, B1, C1) -> Com_1(f67(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)) [ -I + 1 >= 0 /\ -J - I + 201 >= 0 /\ -A + B - 1 >= 0 /\ -J + 200 >= 0 /\ B >= A + 1 ] f67(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) -> Com_1(f89(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)) [ -I + 1 >= 0 /\ -J - I + 201 >= 0 /\ -A + B - 1 >= 0 /\ -J + 200 >= 0 /\ L >= A ] f67(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) -> Com_1(f67(A, B, C, D, E, F, G, H, I, J, K, L + 1, 0, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1)) [ -I + 1 >= 0 /\ -J - I + 201 >= 0 /\ -A + B - 1 >= 0 /\ -J + 200 >= 0 /\ A >= L + 1 ] f67(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) -> Com_1(f71(A, B, C, D, E, F, G, H, I, J, K, L, D1, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1)) [ -I + 1 >= 0 /\ -J - I + 201 >= 0 /\ -A + B - 1 >= 0 /\ -J + 200 >= 0 /\ A >= L + 1 /\ D1 >= 1 ] f67(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) -> Com_1(f71(A, B, C, D, E, F, G, H, I, J, K, L, D1, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1)) [ -I + 1 >= 0 /\ -J - I + 201 >= 0 /\ -A + B - 1 >= 0 /\ -J + 200 >= 0 /\ A >= L + 1 /\ 0 >= D1 + 1 ] f89(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) -> Com_1(f161(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)) [ -I + 1 >= 0 /\ -J - I + 201 >= 0 /\ -A + B - 1 >= 0 /\ -A + L >= 0 /\ -J + 200 >= 0 /\ B >= A + 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, B1, C1) -> Com_1(f67(A, B, C, D, E, F, G, H, I, J, K, L + 1, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1)) [ -I + 1 >= 0 /\ -J - I + 201 >= 0 /\ -L + B - 2 >= 0 /\ -A + B - 1 >= 0 /\ A - L - 1 >= 0 /\ -J + 200 >= 0 /\ K >= A + 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, B1, C1) -> Com_1(f74(A, B, C, D, E, F, G, 0, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1)) [ -I + 1 >= 0 /\ -J - I + 201 >= 0 /\ -L + B - 2 >= 0 /\ -A + B - 1 >= 0 /\ A - L - 1 >= 0 /\ -J + 200 >= 0 /\ A >= K ] f161(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) -> Com_1(f171(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)) [ -I + 1 >= 0 /\ -J - I + 201 >= 0 /\ -A + B - 1 >= 0 /\ -J + 200 >= 0 /\ B >= A + 1 ] f74(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) -> Com_1(f80(A, B, C, D, E, F, G, D1, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1)) [ -I + 1 >= 0 /\ H - I + 1 >= 0 /\ -H - I + 1 >= 0 /\ -J - I + 201 >= 0 /\ -H >= 0 /\ -J - H + 200 >= 0 /\ H >= 0 /\ -J + H + 200 >= 0 /\ -L + B - 2 >= 0 /\ -K + B - 1 >= 0 /\ -A + B - 1 >= 0 /\ A - L - 1 >= 0 /\ A - K >= 0 /\ -J + 200 >= 0 /\ B >= A + 1 ] f80(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) -> Com_1(f71(A, B, C, D, E, F, G, H, I, J, K + 1, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1)) [ -I + 1 >= 0 /\ -J - I + 201 >= 0 /\ -L + B - 2 >= 0 /\ -K + B - 1 >= 0 /\ -A + B - 1 >= 0 /\ A - L - 1 >= 0 /\ A - K >= 0 /\ -J + 200 >= 0 /\ B >= A + 1 ] f171(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) -> Com_1(f181(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)) [ -I + 1 >= 0 /\ -J - I + 201 >= 0 /\ -J + 200 >= 0 /\ 0 >= B ] f171(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) -> Com_1(f173(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)) [ -I + 1 >= 0 /\ -J - I + 201 >= 0 /\ -J + 200 >= 0 /\ B >= 1 ] f181(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) -> Com_1(f188(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, D1, Z, A1, B1, C1)) [ -I + 1 >= 0 /\ -J - I + 201 >= 0 /\ -J + 200 >= 0 /\ B >= A + 1 ] f181(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) -> Com_1(f181(A, B + 1, 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)) [ -I + 1 >= 0 /\ -J - I + 201 >= 0 /\ -J + 200 >= 0 /\ A >= B ] f173(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) -> Com_1(f171(A, B - 1, 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)) [ -I + 1 >= 0 /\ B - I >= 0 /\ -J - I + 201 >= 0 /\ B - 1 >= 0 /\ -J + B + 199 >= 0 /\ -J + 200 >= 0 /\ K >= B + 1 ] f173(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) -> Com_1(f173(A, B, C, D, E, F, G, D1, I, J, K + 1, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1)) [ -I + 1 >= 0 /\ B - I >= 0 /\ -J - I + 201 >= 0 /\ B - 1 >= 0 /\ -J + B + 199 >= 0 /\ -J + 200 >= 0 /\ B >= K ] f188(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) -> Com_1(f201(A, B, 0, 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)) [ -I + 1 >= 0 /\ -J - I + 201 >= 0 /\ -A + B - 1 >= 0 /\ -J + 200 >= 0 /\ B >= A + 1 ] f201(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) -> Com_1(f218(A, B, 0, D, E, F, G, H, 0, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, 0, Y, Z, A1, B1, C1)) [ -I + 1 >= 0 /\ C - I + 1 >= 0 /\ -C - I + 1 >= 0 /\ -J - I + 201 >= 0 /\ -C >= 0 /\ -J - C + 200 >= 0 /\ C >= 0 /\ -J + C + 200 >= 0 /\ -A + B - 1 >= 0 /\ -J + 200 >= 0 /\ B >= A + 1 ] f201(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) -> Com_1(f211(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, D1, Y, Z, A1, B1, C1)) [ -I + 1 >= 0 /\ C - I + 1 >= 0 /\ -C - I + 1 >= 0 /\ -J - I + 201 >= 0 /\ -C >= 0 /\ -J - C + 200 >= 0 /\ C >= 0 /\ -J + C + 200 >= 0 /\ -A + B - 1 >= 0 /\ -J + 200 >= 0 /\ B >= A + 1 /\ D1 >= 1 ] f201(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) -> Com_1(f211(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, D1, Y, Z, A1, B1, C1)) [ -I + 1 >= 0 /\ C - I + 1 >= 0 /\ -C - I + 1 >= 0 /\ -J - I + 201 >= 0 /\ -C >= 0 /\ -J - C + 200 >= 0 /\ C >= 0 /\ -J + C + 200 >= 0 /\ -A + B - 1 >= 0 /\ -J + 200 >= 0 /\ B >= A + 1 /\ 0 >= D1 + 1 ] f218(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) -> Com_1(f54(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, B1, C1)) [ -I >= 0 /\ C - I >= 0 /\ -C - I >= 0 /\ X - I >= 0 /\ -X - I >= 0 /\ -J - I + 200 >= 0 /\ I >= 0 /\ C + I >= 0 /\ -C + I >= 0 /\ X + I >= 0 /\ -X + I >= 0 /\ -J + I + 200 >= 0 /\ -C >= 0 /\ X - C >= 0 /\ -X - C >= 0 /\ -J - C + 200 >= 0 /\ C >= 0 /\ X + C >= 0 /\ -X + C >= 0 /\ -J + C + 200 >= 0 /\ -X >= 0 /\ -J - X + 200 >= 0 /\ X >= 0 /\ -J + X + 200 >= 0 /\ -A + B - 1 >= 0 /\ -J + 200 >= 0 /\ B >= A + 1 ] f211(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) -> Com_1(f54(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, B1, C1)) [ -I + 1 >= 0 /\ C - I + 1 >= 0 /\ -C - I + 1 >= 0 /\ -J - I + 201 >= 0 /\ -C >= 0 /\ -J - C + 200 >= 0 /\ C >= 0 /\ -J + C + 200 >= 0 /\ -A + B - 1 >= 0 /\ -J + 200 >= 0 /\ B >= A + 1 ] f54(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) -> Com_1(f99(A, B, C, D, E, F, G, H, 0, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1)) [ -I + 1 >= 0 /\ -A + B - 1 >= 0 /\ 200 >= J /\ I = 0 ] f54(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) -> 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, A1, B1, C1)) [ -I + 1 >= 0 /\ -A + B - 1 >= 0 /\ 0 >= I + 1 /\ 200 >= J ] f99(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) -> Com_1(f104(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)) [ -I >= 0 /\ -J - I + 200 >= 0 /\ I >= 0 /\ -J + I + 200 >= 0 /\ -A + B - 1 >= 0 /\ -J + 200 >= 0 /\ B >= A + 1 ] f104(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) -> Com_1(f115(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, 1, A1, B1, C1)) [ -I >= 0 /\ -J - I + 200 >= 0 /\ I >= 0 /\ -J + I + 200 >= 0 /\ -A + B - 1 >= 0 /\ -J + 200 >= 0 /\ B >= A + 1 ] f115(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) -> Com_1(f161(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)) [ -I >= 0 /\ Z - I - 1 >= 0 /\ -Z - I + 1 >= 0 /\ -J - I + 200 >= 0 /\ I >= 0 /\ Z + I - 1 >= 0 /\ -Z + I + 1 >= 0 /\ -J + I + 200 >= 0 /\ -Z + 1 >= 0 /\ -J - Z + 201 >= 0 /\ Z - 1 >= 0 /\ -J + Z + 199 >= 0 /\ -A + B - 1 >= 0 /\ -J + 200 >= 0 /\ B >= A + 1 /\ Z >= 1 ] )