(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(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)) 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) -> Com_1(f15(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 >= 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) -> 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, B1, C1)) [ B >= A + 1 /\ 0 >= C + 1 ] 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) -> Com_1(f2(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 ] 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) -> Com_1(f2(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 ] f15(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(f26(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 >= 0 /\ -A + B - 1 >= 0 /\ B >= A + 1 ] f26(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(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)) [ -I + 1 >= 0 /\ C - I + 1 >= 0 /\ C >= 0 /\ -A + B - 1 >= 0 /\ J >= 201 ] f26(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(f30(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 /\ C - I + 1 >= 0 /\ C >= 0 /\ -A + B - 1 >= 0 /\ I >= 1 /\ 200 >= J ] f30(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(f42(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 /\ C - I + 1 >= 0 /\ -J - I + 201 >= 0 /\ C >= 0 /\ -J + C + 200 >= 0 /\ -A + B - 1 >= 0 /\ -J + 200 >= 0 /\ B >= A + 1 ] f42(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(f68(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 /\ C - I + 1 >= 0 /\ -J - I + 201 >= 0 /\ C >= 0 /\ -J + C + 200 >= 0 /\ -A + B - 1 >= 0 /\ -J + 200 >= 0 /\ L >= A ] f42(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(f42(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 /\ C - I + 1 >= 0 /\ -J - I + 201 >= 0 /\ C >= 0 /\ -J + C + 200 >= 0 /\ -A + B - 1 >= 0 /\ -J + 200 >= 0 /\ A >= L + 1 ] f42(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(f47(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 /\ C - I + 1 >= 0 /\ -J - I + 201 >= 0 /\ C >= 0 /\ -J + C + 200 >= 0 /\ -A + B - 1 >= 0 /\ -J + 200 >= 0 /\ A >= L + 1 /\ D1 >= 1 ] f42(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(f47(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 /\ C - I + 1 >= 0 /\ -J - I + 201 >= 0 /\ C >= 0 /\ -J + C + 200 >= 0 /\ -A + B - 1 >= 0 /\ -J + 200 >= 0 /\ A >= L + 1 /\ 0 >= D1 + 1 ] f68(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(f152(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 /\ C - I + 1 >= 0 /\ -J - I + 201 >= 0 /\ C >= 0 /\ -J + C + 200 >= 0 /\ -A + B - 1 >= 0 /\ -A + L >= 0 /\ -J + 200 >= 0 /\ B >= A + 1 ] f47(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(f42(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 /\ C - I + 1 >= 0 /\ -J - I + 201 >= 0 /\ C >= 0 /\ -J + C + 200 >= 0 /\ -L + B - 2 >= 0 /\ -A + B - 1 >= 0 /\ A - L - 1 >= 0 /\ -J + 200 >= 0 /\ K >= A + 1 ] f47(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(f51(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 /\ C - I + 1 >= 0 /\ -J - I + 201 >= 0 /\ C >= 0 /\ -J + C + 200 >= 0 /\ -L + B - 2 >= 0 /\ -A + B - 1 >= 0 /\ A - L - 1 >= 0 /\ -J + 200 >= 0 /\ A >= K ] f152(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(f164(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 /\ C - I + 1 >= 0 /\ -J - I + 201 >= 0 /\ C >= 0 /\ -J + C + 200 >= 0 /\ -A + B - 1 >= 0 /\ -J + 200 >= 0 /\ B >= A + 1 ] f51(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(f58(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 /\ C - I + 1 >= 0 /\ -J - I + 201 >= 0 /\ -H >= 0 /\ C - H >= 0 /\ -J - H + 200 >= 0 /\ H >= 0 /\ C + H >= 0 /\ -J + H + 200 >= 0 /\ C >= 0 /\ -J + C + 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 /\ H >= E1*G1 /\ E1*G1 + E1 >= H + 1 /\ E1 >= D1 /\ H >= F1*G1 /\ F1*G1 + F1 >= H + 1 /\ D1 >= F1 ] f58(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(f47(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 /\ C - I + 1 >= 0 /\ -J - I + 201 >= 0 /\ C >= 0 /\ -J + C + 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 ] f164(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(f176(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 /\ C - I + 1 >= 0 /\ -J - I + 201 >= 0 /\ C >= 0 /\ -J + C + 200 >= 0 /\ -J + 200 >= 0 /\ 0 >= B ] f164(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(f167(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 /\ C - I + 1 >= 0 /\ -J - I + 201 >= 0 /\ C >= 0 /\ -J + C + 200 >= 0 /\ -J + 200 >= 0 /\ B >= 1 ] f176(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(f184(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 /\ C - I + 1 >= 0 /\ -J - I + 201 >= 0 /\ C >= 0 /\ -J + C + 200 >= 0 /\ -J + 200 >= 0 /\ B >= A + 1 ] f176(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(f176(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 /\ C - I + 1 >= 0 /\ -J - I + 201 >= 0 /\ C >= 0 /\ -J + C + 200 >= 0 /\ -J + 200 >= 0 /\ A >= B ] f167(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(f164(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 /\ C - I + 1 >= 0 /\ B - I >= 0 /\ -J - I + 201 >= 0 /\ C >= 0 /\ B + C - 1 >= 0 /\ -J + C + 200 >= 0 /\ B - 1 >= 0 /\ -J + B + 199 >= 0 /\ -J + 200 >= 0 /\ K >= B + 1 ] f167(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(f167(A, B, C, D, E, F, G, H + D1*E1, 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 /\ C - I + 1 >= 0 /\ B - I >= 0 /\ -J - I + 201 >= 0 /\ C >= 0 /\ B + C - 1 >= 0 /\ -J + C + 200 >= 0 /\ B - 1 >= 0 /\ -J + B + 199 >= 0 /\ -J + 200 >= 0 /\ B >= K ] f184(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(f199(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 /\ C - I + 1 >= 0 /\ -J - I + 201 >= 0 /\ C >= 0 /\ -J + C + 200 >= 0 /\ -A + B - 1 >= 0 /\ -J + 200 >= 0 /\ B >= A + 1 ] f199(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 ] f199(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(f210(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 ] f199(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(f210(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(f26(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 ] f210(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(f26(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 ] f26(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(f81(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 /\ C - I + 1 >= 0 /\ C >= 0 /\ -A + B - 1 >= 0 /\ 200 >= J /\ I = 0 ] f26(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(f30(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 /\ C - I + 1 >= 0 /\ C >= 0 /\ -A + B - 1 >= 0 /\ 0 >= I + 1 /\ 200 >= J ] f81(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(f87(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 /\ C - I >= 0 /\ -J - I + 200 >= 0 /\ I >= 0 /\ C + I >= 0 /\ -J + I + 200 >= 0 /\ C >= 0 /\ -J + C + 200 >= 0 /\ -A + B - 1 >= 0 /\ -J + 200 >= 0 /\ B >= A + 1 ] f87(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(f100(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 /\ C - I >= 0 /\ -J - I + 200 >= 0 /\ I >= 0 /\ C + I >= 0 /\ -J + I + 200 >= 0 /\ C >= 0 /\ -J + C + 200 >= 0 /\ -A + B - 1 >= 0 /\ -J + 200 >= 0 /\ B >= A + 1 ] f100(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(f152(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 /\ C - I >= 0 /\ Z - I - 1 >= 0 /\ -Z - I + 1 >= 0 /\ -J - I + 200 >= 0 /\ I >= 0 /\ C + I >= 0 /\ Z + I - 1 >= 0 /\ -Z + I + 1 >= 0 /\ -J + I + 200 >= 0 /\ C >= 0 /\ Z + C - 1 >= 0 /\ -Z + C + 1 >= 0 /\ -J + C + 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 ] )