(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(f11(A, B, C, D, E, 0, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, 0)) f11(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(f11(A + 1, B, 1, D, E, F, G, Y, X, Z, A1, D, Y, Y, Y, Y, 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 >= Y /\ B >= A + 1 ] f11(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(f37(A, B, B1, D, E, F, G, Y, X, Z, A1, D, Y, Y, Y, Y, 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 >= Y /\ 0 >= B1 ] f11(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(f37(A, B, B1, D, E, F, G, Y, X, Z, A1, D, Y, Y, Y, Y, 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 >= Y /\ B1 >= 2 ] f11(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(f45(A, B, C, D, E, F, G, Y, X, Z, A1, D, Y, Y, Y, 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 /\ Y >= 1 /\ B >= A + 1 ] f11(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(f45(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 ] f37(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(f45(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 - D >= 0 /\ -L + D >= 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 ] f37(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(f45(A, B, 2, D + 1, E, 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 - D >= 0 /\ -L + D >= 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 ] f37(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(f45(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 - D >= 0 /\ -L + D >= 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 ] f45(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(f53(A, B, C, 0, X, 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 /\ X >= 1 ] f45(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(f53(A, B, C, 0, X, 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 /\ 0 >= X ] f53(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(f53(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 /\ D - F >= 0 /\ -D - F >= 0 /\ W - F >= 0 /\ -W - F >= 0 /\ F >= 0 /\ D + F >= 0 /\ -D + F >= 0 /\ W + F >= 0 /\ -W + F >= 0 /\ -D >= 0 /\ W - D >= 0 /\ -W - D >= 0 /\ D >= 0 /\ W + D >= 0 /\ -W + D >= 0 /\ -W >= 0 /\ W >= 0 ] )