(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) (RULES f0(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f13(A, B, C, Y, E, 0, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, 0)) [ Y >= 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) -> Com_1(f13(A, B, C, Y, E, 0, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, 0)) [ 0 >= Y ] f13(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f13(A + 1, B, 1, D, E, F, G, X, Y, Z, A1, E, X, X, X, X, R, R, 1, 1, 1, 0, W)) [ -F >= 0 /\ W - F >= 0 /\ -W - F >= 0 /\ F >= 0 /\ W + F >= 0 /\ -W + F >= 0 /\ -W >= 0 /\ W >= 0 /\ 0 >= X /\ B >= A + 1 ] f13(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f39(A, B, B1, D, E, F, G, X, Y, Z, A1, E, X, X, X, X, R, 0, B1, B1, B1, 0, W)) [ -F >= 0 /\ W - F >= 0 /\ -W - F >= 0 /\ F >= 0 /\ W + F >= 0 /\ -W + F >= 0 /\ -W >= 0 /\ W >= 0 /\ B >= A + 1 /\ 0 >= X /\ 0 >= B1 ] f13(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f39(A, B, B1, D, E, F, G, X, Y, Z, A1, E, X, X, X, X, R, 0, B1, B1, B1, 0, W)) [ -F >= 0 /\ W - F >= 0 /\ -W - F >= 0 /\ F >= 0 /\ W + F >= 0 /\ -W + F >= 0 /\ -W >= 0 /\ W >= 0 /\ B >= A + 1 /\ 0 >= X /\ B1 >= 2 ] f13(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f47(A, B, C, D, E, F, G, X, Y, Z, A1, E, X, X, X, P, Q, R, S, T, U, V, W)) [ -F >= 0 /\ W - F >= 0 /\ -W - F >= 0 /\ F >= 0 /\ W + F >= 0 /\ -W + F >= 0 /\ -W >= 0 /\ W >= 0 /\ X >= 1 /\ B >= A + 1 ] f13(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_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)) [ -F >= 0 /\ W - F >= 0 /\ -W - F >= 0 /\ F >= 0 /\ W + F >= 0 /\ -W + F >= 0 /\ -W >= 0 /\ W >= 0 /\ A >= B ] f39(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_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)) [ -F >= 0 /\ W - F >= 0 /\ -W - F >= 0 /\ V - F >= 0 /\ -V - F >= 0 /\ R - F >= 0 /\ -R - F >= 0 /\ -P - F >= 0 /\ F >= 0 /\ W + F >= 0 /\ -W + F >= 0 /\ V + F >= 0 /\ -V + F >= 0 /\ R + F >= 0 /\ -R + F >= 0 /\ -P + F >= 0 /\ L - E >= 0 /\ -L + E >= 0 /\ -W >= 0 /\ V - W >= 0 /\ -V - W >= 0 /\ R - W >= 0 /\ -R - W >= 0 /\ -P - W >= 0 /\ W >= 0 /\ V + W >= 0 /\ -V + W >= 0 /\ R + W >= 0 /\ -R + W >= 0 /\ -P + W >= 0 /\ -V >= 0 /\ R - V >= 0 /\ -R - V >= 0 /\ -P - V >= 0 /\ V >= 0 /\ R + V >= 0 /\ -R + V >= 0 /\ -P + V >= 0 /\ -A + B - 1 >= 0 /\ -R >= 0 /\ -P - R >= 0 /\ R >= 0 /\ -P + R >= 0 /\ -P >= 0 /\ 1 >= C ] f39(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f47(A, B, 2, D, E + 1, F, H, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W)) [ -F >= 0 /\ W - F >= 0 /\ -W - F >= 0 /\ V - F >= 0 /\ -V - F >= 0 /\ R - F >= 0 /\ -R - F >= 0 /\ -P - F >= 0 /\ F >= 0 /\ W + F >= 0 /\ -W + F >= 0 /\ V + F >= 0 /\ -V + F >= 0 /\ R + F >= 0 /\ -R + F >= 0 /\ -P + F >= 0 /\ L - E >= 0 /\ -L + E >= 0 /\ -W >= 0 /\ V - W >= 0 /\ -V - W >= 0 /\ R - W >= 0 /\ -R - W >= 0 /\ -P - W >= 0 /\ W >= 0 /\ V + W >= 0 /\ -V + W >= 0 /\ R + W >= 0 /\ -R + W >= 0 /\ -P + W >= 0 /\ -V >= 0 /\ R - V >= 0 /\ -R - V >= 0 /\ -P - V >= 0 /\ V >= 0 /\ R + V >= 0 /\ -R + V >= 0 /\ -P + V >= 0 /\ -A + B - 1 >= 0 /\ -R >= 0 /\ -P - R >= 0 /\ R >= 0 /\ -P + R >= 0 /\ -P >= 0 /\ C = 2 ] f39(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_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)) [ -F >= 0 /\ W - F >= 0 /\ -W - F >= 0 /\ V - F >= 0 /\ -V - F >= 0 /\ R - F >= 0 /\ -R - F >= 0 /\ -P - F >= 0 /\ F >= 0 /\ W + F >= 0 /\ -W + F >= 0 /\ V + F >= 0 /\ -V + F >= 0 /\ R + F >= 0 /\ -R + F >= 0 /\ -P + F >= 0 /\ L - E >= 0 /\ -L + E >= 0 /\ -W >= 0 /\ V - W >= 0 /\ -V - W >= 0 /\ R - W >= 0 /\ -R - W >= 0 /\ -P - W >= 0 /\ W >= 0 /\ V + W >= 0 /\ -V + W >= 0 /\ R + W >= 0 /\ -R + W >= 0 /\ -P + W >= 0 /\ -V >= 0 /\ R - V >= 0 /\ -R - V >= 0 /\ -P - V >= 0 /\ V >= 0 /\ R + V >= 0 /\ -R + V >= 0 /\ -P + V >= 0 /\ -A + B - 1 >= 0 /\ -R >= 0 /\ -P - R >= 0 /\ R >= 0 /\ -P + R >= 0 /\ -P >= 0 /\ C >= 3 ] f47(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f54(A, B, C, D, 0, 0, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W)) [ -F >= 0 /\ W - F >= 0 /\ -W - F >= 0 /\ F >= 0 /\ W + F >= 0 /\ -W + F >= 0 /\ -W >= 0 /\ W >= 0 /\ 0 >= D ] f47(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f54(A, B, C, D, 0, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W)) [ -F >= 0 /\ W - F >= 0 /\ -W - F >= 0 /\ F >= 0 /\ W + F >= 0 /\ -W + F >= 0 /\ -W >= 0 /\ W >= 0 /\ D >= 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) -> Com_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)) [ -F >= 0 /\ E - F >= 0 /\ -E - F >= 0 /\ W - F >= 0 /\ -W - F >= 0 /\ F >= 0 /\ E + F >= 0 /\ -E + F >= 0 /\ W + F >= 0 /\ -W + F >= 0 /\ -E >= 0 /\ W - E >= 0 /\ -W - E >= 0 /\ E >= 0 /\ W + E >= 0 /\ -W + E >= 0 /\ -W >= 0 /\ W >= 0 ] )