(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS f6)) (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) (RULES f9(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) -> Com_1(f9(A, B + 1, C + 1, B1, B1, B1, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1)) [ B - C - 1 >= 0 /\ C >= 0 /\ B + C - 1 >= 0 /\ -B + C + 1 >= 0 /\ A + C - 17 >= 0 /\ -A + C + 17 >= 0 /\ B - 1 >= 0 /\ A + B - 18 >= 0 /\ -A + B + 16 >= 0 /\ -A + 17 >= 0 /\ A - 17 >= 0 /\ A >= B + 1 ] f5(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) -> Com_1(f0(A, B, C, D, E, F, G, B1, I, H, E1, F1, C1, D1, G1, P, Q, R, S, T, U, V, W, X, Y, Z, A1)) [ T - I >= 0 /\ I - 1 >= 0 /\ G + I - 14 >= 0 /\ C + I - 17 >= 0 /\ Y + I - 15 >= 0 /\ U + I - 14 >= 0 /\ T + I - 2 >= 0 /\ -T + I >= 0 /\ B + I - 18 >= 0 /\ J + I - 1 >= 0 /\ -J + I - 1 >= 0 /\ A + I - 18 >= 0 /\ -A + I + 16 >= 0 /\ C - G - 3 >= 0 /\ Y - G - 1 >= 0 /\ U - G >= 0 /\ B - G - 4 >= 0 /\ -U + G >= 0 /\ T + G - 14 >= 0 /\ X - D >= 0 /\ W - D >= 0 /\ -X + D >= 0 /\ -W + D >= 0 /\ Y - C + 2 >= 0 /\ B - C - 1 >= 0 /\ C - 16 >= 0 /\ Y + C - 30 >= 0 /\ -Y + C - 2 >= 0 /\ -U + C - 3 >= 0 /\ T + C - 17 >= 0 /\ B + C - 33 >= 0 /\ -B + C + 1 >= 0 /\ J + C - 16 >= 0 /\ -J + C - 16 >= 0 /\ A + C - 33 >= 0 /\ -A + C + 1 >= 0 /\ Z - A1 >= 0 /\ B - Y - 3 >= 0 /\ Y - 14 >= 0 /\ -U + Y - 1 >= 0 /\ T + Y - 15 >= 0 /\ B + Y - 31 >= 0 /\ -B + Y + 3 >= 0 /\ J + Y - 14 >= 0 /\ -J + Y - 14 >= 0 /\ A + Y - 31 >= 0 /\ -A + Y + 3 >= 0 /\ W - X >= 0 /\ -W + X >= 0 /\ B - U - 4 >= 0 /\ T + U - 14 >= 0 /\ T - 1 >= 0 /\ B + T - 18 >= 0 /\ J + T - 1 >= 0 /\ -J + T - 1 >= 0 /\ A + T - 18 >= 0 /\ -A + T + 16 >= 0 /\ B - 17 >= 0 /\ J + B - 17 >= 0 /\ -J + B - 17 >= 0 /\ A + B - 34 >= 0 /\ -A + B >= 0 /\ -J >= 0 /\ A - J - 17 >= 0 /\ -A - J + 17 >= 0 /\ J >= 0 /\ A + J - 17 >= 0 /\ -A + J + 17 >= 0 /\ -A + 17 >= 0 /\ A - 17 >= 0 /\ D1 >= C1 + 1 /\ G >= 0 /\ H >= 1 /\ I >= 1 ] f5(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) -> Com_1(f0(A, B, C, D, E, F, G, B1, I, H, E1, F1, C1, D1, G1, P, Q, R, S, T, U, V, W, X, Y, Z, A1)) [ T - I >= 0 /\ I - 1 >= 0 /\ G + I - 14 >= 0 /\ C + I - 17 >= 0 /\ Y + I - 15 >= 0 /\ U + I - 14 >= 0 /\ T + I - 2 >= 0 /\ -T + I >= 0 /\ B + I - 18 >= 0 /\ J + I - 1 >= 0 /\ -J + I - 1 >= 0 /\ A + I - 18 >= 0 /\ -A + I + 16 >= 0 /\ C - G - 3 >= 0 /\ Y - G - 1 >= 0 /\ U - G >= 0 /\ B - G - 4 >= 0 /\ -U + G >= 0 /\ T + G - 14 >= 0 /\ X - D >= 0 /\ W - D >= 0 /\ -X + D >= 0 /\ -W + D >= 0 /\ Y - C + 2 >= 0 /\ B - C - 1 >= 0 /\ C - 16 >= 0 /\ Y + C - 30 >= 0 /\ -Y + C - 2 >= 0 /\ -U + C - 3 >= 0 /\ T + C - 17 >= 0 /\ B + C - 33 >= 0 /\ -B + C + 1 >= 0 /\ J + C - 16 >= 0 /\ -J + C - 16 >= 0 /\ A + C - 33 >= 0 /\ -A + C + 1 >= 0 /\ Z - A1 >= 0 /\ B - Y - 3 >= 0 /\ Y - 14 >= 0 /\ -U + Y - 1 >= 0 /\ T + Y - 15 >= 0 /\ B + Y - 31 >= 0 /\ -B + Y + 3 >= 0 /\ J + Y - 14 >= 0 /\ -J + Y - 14 >= 0 /\ A + Y - 31 >= 0 /\ -A + Y + 3 >= 0 /\ W - X >= 0 /\ -W + X >= 0 /\ B - U - 4 >= 0 /\ T + U - 14 >= 0 /\ T - 1 >= 0 /\ B + T - 18 >= 0 /\ J + T - 1 >= 0 /\ -J + T - 1 >= 0 /\ A + T - 18 >= 0 /\ -A + T + 16 >= 0 /\ B - 17 >= 0 /\ J + B - 17 >= 0 /\ -J + B - 17 >= 0 /\ A + B - 34 >= 0 /\ -A + B >= 0 /\ -J >= 0 /\ A - J - 17 >= 0 /\ -A - J + 17 >= 0 /\ J >= 0 /\ A + J - 17 >= 0 /\ -A + J + 17 >= 0 /\ -A + 17 >= 0 /\ A - 17 >= 0 /\ D1 >= C1 + 1 /\ G >= 0 /\ 0 >= H + 1 /\ I >= 1 ] f5(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) -> Com_1(f5(A, B, C, D, E, F, G - 1, R, I + 1, 0, F1, C1, M, D1, O, E1, R, P, B1, I + 1, G - 1, I, W, X, Y, Z, A1)) [ T - I >= 0 /\ I - 1 >= 0 /\ G + I - 14 >= 0 /\ C + I - 17 >= 0 /\ Y + I - 15 >= 0 /\ U + I - 14 >= 0 /\ T + I - 2 >= 0 /\ -T + I >= 0 /\ B + I - 18 >= 0 /\ J + I - 1 >= 0 /\ -J + I - 1 >= 0 /\ A + I - 18 >= 0 /\ -A + I + 16 >= 0 /\ C - G - 3 >= 0 /\ Y - G - 1 >= 0 /\ U - G >= 0 /\ B - G - 4 >= 0 /\ -U + G >= 0 /\ T + G - 14 >= 0 /\ X - D >= 0 /\ W - D >= 0 /\ -X + D >= 0 /\ -W + D >= 0 /\ Y - C + 2 >= 0 /\ B - C - 1 >= 0 /\ C - 16 >= 0 /\ Y + C - 30 >= 0 /\ -Y + C - 2 >= 0 /\ -U + C - 3 >= 0 /\ T + C - 17 >= 0 /\ B + C - 33 >= 0 /\ -B + C + 1 >= 0 /\ J + C - 16 >= 0 /\ -J + C - 16 >= 0 /\ A + C - 33 >= 0 /\ -A + C + 1 >= 0 /\ Z - A1 >= 0 /\ B - Y - 3 >= 0 /\ Y - 14 >= 0 /\ -U + Y - 1 >= 0 /\ T + Y - 15 >= 0 /\ B + Y - 31 >= 0 /\ -B + Y + 3 >= 0 /\ J + Y - 14 >= 0 /\ -J + Y - 14 >= 0 /\ A + Y - 31 >= 0 /\ -A + Y + 3 >= 0 /\ W - X >= 0 /\ -W + X >= 0 /\ B - U - 4 >= 0 /\ T + U - 14 >= 0 /\ T - 1 >= 0 /\ B + T - 18 >= 0 /\ J + T - 1 >= 0 /\ -J + T - 1 >= 0 /\ A + T - 18 >= 0 /\ -A + T + 16 >= 0 /\ B - 17 >= 0 /\ J + B - 17 >= 0 /\ -J + B - 17 >= 0 /\ A + B - 34 >= 0 /\ -A + B >= 0 /\ -J >= 0 /\ A - J - 17 >= 0 /\ -A - J + 17 >= 0 /\ J >= 0 /\ A + J - 17 >= 0 /\ -A + J + 17 >= 0 /\ -A + 17 >= 0 /\ A - 17 >= 0 /\ M >= D1 /\ G >= 0 /\ I >= 0 /\ P >= 1 /\ H >= 1 /\ J = 0 ] f5(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) -> Com_1(f5(A, B, C, D, E, F, G - 1, R, I + 1, 0, F1, C1, M, D1, O, E1, R, P, B1, I + 1, G - 1, I, W, X, Y, Z, A1)) [ T - I >= 0 /\ I - 1 >= 0 /\ G + I - 14 >= 0 /\ C + I - 17 >= 0 /\ Y + I - 15 >= 0 /\ U + I - 14 >= 0 /\ T + I - 2 >= 0 /\ -T + I >= 0 /\ B + I - 18 >= 0 /\ J + I - 1 >= 0 /\ -J + I - 1 >= 0 /\ A + I - 18 >= 0 /\ -A + I + 16 >= 0 /\ C - G - 3 >= 0 /\ Y - G - 1 >= 0 /\ U - G >= 0 /\ B - G - 4 >= 0 /\ -U + G >= 0 /\ T + G - 14 >= 0 /\ X - D >= 0 /\ W - D >= 0 /\ -X + D >= 0 /\ -W + D >= 0 /\ Y - C + 2 >= 0 /\ B - C - 1 >= 0 /\ C - 16 >= 0 /\ Y + C - 30 >= 0 /\ -Y + C - 2 >= 0 /\ -U + C - 3 >= 0 /\ T + C - 17 >= 0 /\ B + C - 33 >= 0 /\ -B + C + 1 >= 0 /\ J + C - 16 >= 0 /\ -J + C - 16 >= 0 /\ A + C - 33 >= 0 /\ -A + C + 1 >= 0 /\ Z - A1 >= 0 /\ B - Y - 3 >= 0 /\ Y - 14 >= 0 /\ -U + Y - 1 >= 0 /\ T + Y - 15 >= 0 /\ B + Y - 31 >= 0 /\ -B + Y + 3 >= 0 /\ J + Y - 14 >= 0 /\ -J + Y - 14 >= 0 /\ A + Y - 31 >= 0 /\ -A + Y + 3 >= 0 /\ W - X >= 0 /\ -W + X >= 0 /\ B - U - 4 >= 0 /\ T + U - 14 >= 0 /\ T - 1 >= 0 /\ B + T - 18 >= 0 /\ J + T - 1 >= 0 /\ -J + T - 1 >= 0 /\ A + T - 18 >= 0 /\ -A + T + 16 >= 0 /\ B - 17 >= 0 /\ J + B - 17 >= 0 /\ -J + B - 17 >= 0 /\ A + B - 34 >= 0 /\ -A + B >= 0 /\ -J >= 0 /\ A - J - 17 >= 0 /\ -A - J + 17 >= 0 /\ J >= 0 /\ A + J - 17 >= 0 /\ -A + J + 17 >= 0 /\ -A + 17 >= 0 /\ A - 17 >= 0 /\ M >= D1 /\ G >= 0 /\ I >= 0 /\ P >= 1 /\ 0 >= H + 1 /\ J = 0 ] f5(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) -> Com_1(f5(A, B, C, D, E, F, G - 1, R, I + 1, 0, F1, C1, M, D1, O, E1, R, P, B1, I + 1, G - 1, I, W, X, Y, Z, A1)) [ T - I >= 0 /\ I - 1 >= 0 /\ G + I - 14 >= 0 /\ C + I - 17 >= 0 /\ Y + I - 15 >= 0 /\ U + I - 14 >= 0 /\ T + I - 2 >= 0 /\ -T + I >= 0 /\ B + I - 18 >= 0 /\ J + I - 1 >= 0 /\ -J + I - 1 >= 0 /\ A + I - 18 >= 0 /\ -A + I + 16 >= 0 /\ C - G - 3 >= 0 /\ Y - G - 1 >= 0 /\ U - G >= 0 /\ B - G - 4 >= 0 /\ -U + G >= 0 /\ T + G - 14 >= 0 /\ X - D >= 0 /\ W - D >= 0 /\ -X + D >= 0 /\ -W + D >= 0 /\ Y - C + 2 >= 0 /\ B - C - 1 >= 0 /\ C - 16 >= 0 /\ Y + C - 30 >= 0 /\ -Y + C - 2 >= 0 /\ -U + C - 3 >= 0 /\ T + C - 17 >= 0 /\ B + C - 33 >= 0 /\ -B + C + 1 >= 0 /\ J + C - 16 >= 0 /\ -J + C - 16 >= 0 /\ A + C - 33 >= 0 /\ -A + C + 1 >= 0 /\ Z - A1 >= 0 /\ B - Y - 3 >= 0 /\ Y - 14 >= 0 /\ -U + Y - 1 >= 0 /\ T + Y - 15 >= 0 /\ B + Y - 31 >= 0 /\ -B + Y + 3 >= 0 /\ J + Y - 14 >= 0 /\ -J + Y - 14 >= 0 /\ A + Y - 31 >= 0 /\ -A + Y + 3 >= 0 /\ W - X >= 0 /\ -W + X >= 0 /\ B - U - 4 >= 0 /\ T + U - 14 >= 0 /\ T - 1 >= 0 /\ B + T - 18 >= 0 /\ J + T - 1 >= 0 /\ -J + T - 1 >= 0 /\ A + T - 18 >= 0 /\ -A + T + 16 >= 0 /\ B - 17 >= 0 /\ J + B - 17 >= 0 /\ -J + B - 17 >= 0 /\ A + B - 34 >= 0 /\ -A + B >= 0 /\ -J >= 0 /\ A - J - 17 >= 0 /\ -A - J + 17 >= 0 /\ J >= 0 /\ A + J - 17 >= 0 /\ -A + J + 17 >= 0 /\ -A + 17 >= 0 /\ A - 17 >= 0 /\ M >= D1 /\ G >= 0 /\ I >= 0 /\ 0 >= P + 1 /\ H >= 1 /\ J = 0 ] f5(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) -> Com_1(f5(A, B, C, D, E, F, G - 1, R, I + 1, 0, F1, C1, M, D1, O, E1, R, P, B1, I + 1, G - 1, I, W, X, Y, Z, A1)) [ T - I >= 0 /\ I - 1 >= 0 /\ G + I - 14 >= 0 /\ C + I - 17 >= 0 /\ Y + I - 15 >= 0 /\ U + I - 14 >= 0 /\ T + I - 2 >= 0 /\ -T + I >= 0 /\ B + I - 18 >= 0 /\ J + I - 1 >= 0 /\ -J + I - 1 >= 0 /\ A + I - 18 >= 0 /\ -A + I + 16 >= 0 /\ C - G - 3 >= 0 /\ Y - G - 1 >= 0 /\ U - G >= 0 /\ B - G - 4 >= 0 /\ -U + G >= 0 /\ T + G - 14 >= 0 /\ X - D >= 0 /\ W - D >= 0 /\ -X + D >= 0 /\ -W + D >= 0 /\ Y - C + 2 >= 0 /\ B - C - 1 >= 0 /\ C - 16 >= 0 /\ Y + C - 30 >= 0 /\ -Y + C - 2 >= 0 /\ -U + C - 3 >= 0 /\ T + C - 17 >= 0 /\ B + C - 33 >= 0 /\ -B + C + 1 >= 0 /\ J + C - 16 >= 0 /\ -J + C - 16 >= 0 /\ A + C - 33 >= 0 /\ -A + C + 1 >= 0 /\ Z - A1 >= 0 /\ B - Y - 3 >= 0 /\ Y - 14 >= 0 /\ -U + Y - 1 >= 0 /\ T + Y - 15 >= 0 /\ B + Y - 31 >= 0 /\ -B + Y + 3 >= 0 /\ J + Y - 14 >= 0 /\ -J + Y - 14 >= 0 /\ A + Y - 31 >= 0 /\ -A + Y + 3 >= 0 /\ W - X >= 0 /\ -W + X >= 0 /\ B - U - 4 >= 0 /\ T + U - 14 >= 0 /\ T - 1 >= 0 /\ B + T - 18 >= 0 /\ J + T - 1 >= 0 /\ -J + T - 1 >= 0 /\ A + T - 18 >= 0 /\ -A + T + 16 >= 0 /\ B - 17 >= 0 /\ J + B - 17 >= 0 /\ -J + B - 17 >= 0 /\ A + B - 34 >= 0 /\ -A + B >= 0 /\ -J >= 0 /\ A - J - 17 >= 0 /\ -A - J + 17 >= 0 /\ J >= 0 /\ A + J - 17 >= 0 /\ -A + J + 17 >= 0 /\ -A + 17 >= 0 /\ A - 17 >= 0 /\ M >= D1 /\ G >= 0 /\ I >= 0 /\ 0 >= P + 1 /\ 0 >= H + 1 /\ J = 0 ] f5(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) -> Com_1(f12(A, B, C, D, E, F, G, H, I, 0, E1, F1, M, C1, O, 0, R, R, S, T, U, I, B1, X, Y, Z, A1)) [ T - I >= 0 /\ I - 1 >= 0 /\ G + I - 14 >= 0 /\ C + I - 17 >= 0 /\ Y + I - 15 >= 0 /\ U + I - 14 >= 0 /\ T + I - 2 >= 0 /\ -T + I >= 0 /\ B + I - 18 >= 0 /\ J + I - 1 >= 0 /\ -J + I - 1 >= 0 /\ A + I - 18 >= 0 /\ -A + I + 16 >= 0 /\ C - G - 3 >= 0 /\ Y - G - 1 >= 0 /\ U - G >= 0 /\ B - G - 4 >= 0 /\ -U + G >= 0 /\ T + G - 14 >= 0 /\ X - D >= 0 /\ W - D >= 0 /\ -X + D >= 0 /\ -W + D >= 0 /\ Y - C + 2 >= 0 /\ B - C - 1 >= 0 /\ C - 16 >= 0 /\ Y + C - 30 >= 0 /\ -Y + C - 2 >= 0 /\ -U + C - 3 >= 0 /\ T + C - 17 >= 0 /\ B + C - 33 >= 0 /\ -B + C + 1 >= 0 /\ J + C - 16 >= 0 /\ -J + C - 16 >= 0 /\ A + C - 33 >= 0 /\ -A + C + 1 >= 0 /\ Z - A1 >= 0 /\ B - Y - 3 >= 0 /\ Y - 14 >= 0 /\ -U + Y - 1 >= 0 /\ T + Y - 15 >= 0 /\ B + Y - 31 >= 0 /\ -B + Y + 3 >= 0 /\ J + Y - 14 >= 0 /\ -J + Y - 14 >= 0 /\ A + Y - 31 >= 0 /\ -A + Y + 3 >= 0 /\ W - X >= 0 /\ -W + X >= 0 /\ B - U - 4 >= 0 /\ T + U - 14 >= 0 /\ T - 1 >= 0 /\ B + T - 18 >= 0 /\ J + T - 1 >= 0 /\ -J + T - 1 >= 0 /\ A + T - 18 >= 0 /\ -A + T + 16 >= 0 /\ B - 17 >= 0 /\ J + B - 17 >= 0 /\ -J + B - 17 >= 0 /\ A + B - 34 >= 0 /\ -A + B >= 0 /\ -J >= 0 /\ A - J - 17 >= 0 /\ -A - J + 17 >= 0 /\ J >= 0 /\ A + J - 17 >= 0 /\ -A + J + 17 >= 0 /\ -A + 17 >= 0 /\ A - 17 >= 0 /\ M >= C1 /\ G >= 0 /\ H >= 1 /\ I >= 0 /\ P = 0 /\ J = 0 ] f5(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) -> Com_1(f12(A, B, C, D, E, F, G, H, I, 0, E1, F1, M, C1, O, 0, R, R, S, T, U, I, B1, X, Y, Z, A1)) [ T - I >= 0 /\ I - 1 >= 0 /\ G + I - 14 >= 0 /\ C + I - 17 >= 0 /\ Y + I - 15 >= 0 /\ U + I - 14 >= 0 /\ T + I - 2 >= 0 /\ -T + I >= 0 /\ B + I - 18 >= 0 /\ J + I - 1 >= 0 /\ -J + I - 1 >= 0 /\ A + I - 18 >= 0 /\ -A + I + 16 >= 0 /\ C - G - 3 >= 0 /\ Y - G - 1 >= 0 /\ U - G >= 0 /\ B - G - 4 >= 0 /\ -U + G >= 0 /\ T + G - 14 >= 0 /\ X - D >= 0 /\ W - D >= 0 /\ -X + D >= 0 /\ -W + D >= 0 /\ Y - C + 2 >= 0 /\ B - C - 1 >= 0 /\ C - 16 >= 0 /\ Y + C - 30 >= 0 /\ -Y + C - 2 >= 0 /\ -U + C - 3 >= 0 /\ T + C - 17 >= 0 /\ B + C - 33 >= 0 /\ -B + C + 1 >= 0 /\ J + C - 16 >= 0 /\ -J + C - 16 >= 0 /\ A + C - 33 >= 0 /\ -A + C + 1 >= 0 /\ Z - A1 >= 0 /\ B - Y - 3 >= 0 /\ Y - 14 >= 0 /\ -U + Y - 1 >= 0 /\ T + Y - 15 >= 0 /\ B + Y - 31 >= 0 /\ -B + Y + 3 >= 0 /\ J + Y - 14 >= 0 /\ -J + Y - 14 >= 0 /\ A + Y - 31 >= 0 /\ -A + Y + 3 >= 0 /\ W - X >= 0 /\ -W + X >= 0 /\ B - U - 4 >= 0 /\ T + U - 14 >= 0 /\ T - 1 >= 0 /\ B + T - 18 >= 0 /\ J + T - 1 >= 0 /\ -J + T - 1 >= 0 /\ A + T - 18 >= 0 /\ -A + T + 16 >= 0 /\ B - 17 >= 0 /\ J + B - 17 >= 0 /\ -J + B - 17 >= 0 /\ A + B - 34 >= 0 /\ -A + B >= 0 /\ -J >= 0 /\ A - J - 17 >= 0 /\ -A - J + 17 >= 0 /\ J >= 0 /\ A + J - 17 >= 0 /\ -A + J + 17 >= 0 /\ -A + 17 >= 0 /\ A - 17 >= 0 /\ M >= C1 /\ G >= 0 /\ 0 >= H + 1 /\ I >= 0 /\ P = 0 /\ J = 0 ] f9(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) -> Com_1(f5(A, B, C, D, E, F, C - 3, B1, 1, 0, H1, I1, M, N, O, C1, B1, E1, F1, 1, C - 3, V, D, D, C - 2, D1, G1)) [ B - C - 1 >= 0 /\ C >= 0 /\ B + C - 1 >= 0 /\ -B + C + 1 >= 0 /\ A + C - 17 >= 0 /\ -A + C + 17 >= 0 /\ B - 1 >= 0 /\ A + B - 18 >= 0 /\ -A + B + 16 >= 0 /\ -A + 17 >= 0 /\ A - 17 >= 0 /\ D1 >= G1 /\ C >= 2 /\ E1 >= 1 /\ B1 >= 1 /\ B >= A /\ D >= 1 ] f9(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) -> Com_1(f5(A, B, C, D, E, F, C - 3, B1, 1, 0, H1, I1, M, N, O, C1, B1, E1, F1, 1, C - 3, V, D, D, C - 2, D1, G1)) [ B - C - 1 >= 0 /\ C >= 0 /\ B + C - 1 >= 0 /\ -B + C + 1 >= 0 /\ A + C - 17 >= 0 /\ -A + C + 17 >= 0 /\ B - 1 >= 0 /\ A + B - 18 >= 0 /\ -A + B + 16 >= 0 /\ -A + 17 >= 0 /\ A - 17 >= 0 /\ D1 >= G1 /\ C >= 2 /\ E1 >= 1 /\ B1 >= 1 /\ B >= A /\ 0 >= D + 1 ] f9(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) -> Com_1(f5(A, B, C, D, E, F, C - 3, B1, 1, 0, H1, I1, M, N, O, C1, B1, E1, F1, 1, C - 3, V, D, D, C - 2, D1, G1)) [ B - C - 1 >= 0 /\ C >= 0 /\ B + C - 1 >= 0 /\ -B + C + 1 >= 0 /\ A + C - 17 >= 0 /\ -A + C + 17 >= 0 /\ B - 1 >= 0 /\ A + B - 18 >= 0 /\ -A + B + 16 >= 0 /\ -A + 17 >= 0 /\ A - 17 >= 0 /\ D1 >= G1 /\ C >= 2 /\ E1 >= 1 /\ 0 >= B1 + 1 /\ B >= A /\ D >= 1 ] f9(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) -> Com_1(f5(A, B, C, D, E, F, C - 3, B1, 1, 0, H1, I1, M, N, O, C1, B1, E1, F1, 1, C - 3, V, D, D, C - 2, D1, G1)) [ B - C - 1 >= 0 /\ C >= 0 /\ B + C - 1 >= 0 /\ -B + C + 1 >= 0 /\ A + C - 17 >= 0 /\ -A + C + 17 >= 0 /\ B - 1 >= 0 /\ A + B - 18 >= 0 /\ -A + B + 16 >= 0 /\ -A + 17 >= 0 /\ A - 17 >= 0 /\ D1 >= G1 /\ C >= 2 /\ E1 >= 1 /\ 0 >= B1 + 1 /\ B >= A /\ 0 >= D + 1 ] f9(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) -> Com_1(f5(A, B, C, D, E, F, C - 3, B1, 1, 0, H1, I1, M, N, O, C1, B1, E1, F1, 1, C - 3, V, D, D, C - 2, D1, G1)) [ B - C - 1 >= 0 /\ C >= 0 /\ B + C - 1 >= 0 /\ -B + C + 1 >= 0 /\ A + C - 17 >= 0 /\ -A + C + 17 >= 0 /\ B - 1 >= 0 /\ A + B - 18 >= 0 /\ -A + B + 16 >= 0 /\ -A + 17 >= 0 /\ A - 17 >= 0 /\ D1 >= G1 /\ C >= 2 /\ 0 >= E1 + 1 /\ B1 >= 1 /\ B >= A /\ D >= 1 ] f9(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) -> Com_1(f5(A, B, C, D, E, F, C - 3, B1, 1, 0, H1, I1, M, N, O, C1, B1, E1, F1, 1, C - 3, V, D, D, C - 2, D1, G1)) [ B - C - 1 >= 0 /\ C >= 0 /\ B + C - 1 >= 0 /\ -B + C + 1 >= 0 /\ A + C - 17 >= 0 /\ -A + C + 17 >= 0 /\ B - 1 >= 0 /\ A + B - 18 >= 0 /\ -A + B + 16 >= 0 /\ -A + 17 >= 0 /\ A - 17 >= 0 /\ D1 >= G1 /\ C >= 2 /\ 0 >= E1 + 1 /\ B1 >= 1 /\ B >= A /\ 0 >= D + 1 ] f9(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) -> Com_1(f5(A, B, C, D, E, F, C - 3, B1, 1, 0, H1, I1, M, N, O, C1, B1, E1, F1, 1, C - 3, V, D, D, C - 2, D1, G1)) [ B - C - 1 >= 0 /\ C >= 0 /\ B + C - 1 >= 0 /\ -B + C + 1 >= 0 /\ A + C - 17 >= 0 /\ -A + C + 17 >= 0 /\ B - 1 >= 0 /\ A + B - 18 >= 0 /\ -A + B + 16 >= 0 /\ -A + 17 >= 0 /\ A - 17 >= 0 /\ D1 >= G1 /\ C >= 2 /\ 0 >= E1 + 1 /\ 0 >= B1 + 1 /\ B >= A /\ D >= 1 ] f9(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) -> Com_1(f5(A, B, C, D, E, F, C - 3, B1, 1, 0, H1, I1, M, N, O, C1, B1, E1, F1, 1, C - 3, V, D, D, C - 2, D1, G1)) [ B - C - 1 >= 0 /\ C >= 0 /\ B + C - 1 >= 0 /\ -B + C + 1 >= 0 /\ A + C - 17 >= 0 /\ -A + C + 17 >= 0 /\ B - 1 >= 0 /\ A + B - 18 >= 0 /\ -A + B + 16 >= 0 /\ -A + 17 >= 0 /\ A - 17 >= 0 /\ D1 >= G1 /\ C >= 2 /\ 0 >= E1 + 1 /\ 0 >= B1 + 1 /\ B >= A /\ 0 >= D + 1 ] f6(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) -> Com_1(f9(17, 1, 0, B1, B1, B1, G, H, I, J, K, L, M, N, O, P, E1, R, S, T, U, V, W, X, Y, Z, A1)) )