(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS f2)) (VAR A B C D E F G H I J K L M N O P Q) (RULES f48(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f52(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q)) [ -I + 1 >= 0 /\ -H - I + 2 >= 0 /\ G - I + 1 >= 0 /\ F - I >= 0 /\ E - I + 1 >= 0 /\ D - I >= 0 /\ C - I + 1 >= 0 /\ B - I + 1 >= 0 /\ -B - I + 2 >= 0 /\ M - I >= 0 /\ -M - I + 2 >= 0 /\ J - I + 1 >= 0 /\ -J - I + 2 >= 0 /\ -A - I + 2 >= 0 /\ I - 1 >= 0 /\ -H + I >= 0 /\ G + I - 1 >= 0 /\ F + I - 2 >= 0 /\ E + I - 1 >= 0 /\ D + I - 2 >= 0 /\ C + I - 1 >= 0 /\ B + I - 1 >= 0 /\ -B + I >= 0 /\ M + I - 2 >= 0 /\ -M + I >= 0 /\ J + I - 1 >= 0 /\ -J + I >= 0 /\ -A + I >= 0 /\ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H >= 0 /\ C - H + 1 >= 0 /\ B - H >= 0 /\ -B - H + 2 >= 0 /\ M - H >= 0 /\ -M - H + 2 >= 0 /\ J - H >= 0 /\ -J - H + 2 >= 0 /\ A - H >= 0 /\ -A - H + 2 >= 0 /\ G + H - 1 >= 0 /\ D + H - 2 >= 0 /\ -A + H >= 0 /\ D - G - 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G - 1 >= 0 /\ C + G >= 0 /\ B + G - 1 >= 0 /\ -B + G + 1 >= 0 /\ M + G - 1 >= 0 /\ -M + G + 1 >= 0 /\ J + G - 1 >= 0 /\ -J + G + 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ D - F + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 2 >= 0 /\ C + F - 1 >= 0 /\ B + F - 1 >= 0 /\ -B + F >= 0 /\ M + F - 2 >= 0 /\ -M + F >= 0 /\ J + F - 1 >= 0 /\ -J + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E - 1 >= 0 /\ C + E >= 0 /\ B + E >= 0 /\ -B + E + 1 >= 0 /\ M + E - 1 >= 0 /\ -M + E + 1 >= 0 /\ J + E >= 0 /\ -J + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ D - 1 >= 0 /\ C + D - 1 >= 0 /\ B + D - 2 >= 0 /\ -B + D >= 0 /\ M + D - 2 >= 0 /\ -M + D >= 0 /\ J + D - 2 >= 0 /\ -J + D >= 0 /\ A + D - 2 >= 0 /\ -A + D >= 0 /\ C >= 0 /\ B + C >= 0 /\ -B + C + 1 >= 0 /\ M + C - 1 >= 0 /\ -M + C + 1 >= 0 /\ J + C >= 0 /\ -J + C + 1 >= 0 /\ -A + C + 1 >= 0 /\ -B + 1 >= 0 /\ M - B >= 0 /\ -M - B + 2 >= 0 /\ J - B >= 0 /\ -J - B + 2 >= 0 /\ -A - B + 2 >= 0 /\ B >= 0 /\ M + B - 1 >= 0 /\ -M + B + 1 >= 0 /\ J + B >= 0 /\ -J + B >= 0 /\ -A + B >= 0 /\ N - O >= 0 /\ L - O >= 0 /\ K - O >= 0 /\ -N + O >= 0 /\ -L + O >= 0 /\ -K + O >= 0 /\ L - N >= 0 /\ K - N >= 0 /\ -L + N >= 0 /\ -K + N >= 0 /\ -M + 1 >= 0 /\ J - M + 1 >= 0 /\ -J - M + 2 >= 0 /\ -A - M + 2 >= 0 /\ M - 1 >= 0 /\ J + M - 1 >= 0 /\ -J + M >= 0 /\ -A + M >= 0 /\ K - L >= 0 /\ -K + L >= 0 /\ -J + 1 >= 0 /\ -A - J + 2 >= 0 /\ J >= 0 /\ -A + J >= 0 /\ -A + 1 >= 0 /\ A >= 1 ] f2(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f10(A, B, C, D, 0, 1, 0, H, I, J, K, L, M, N, O, P, Q)) [ C >= 0 /\ D >= 1 ] f10(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f14(A, B, C, D, E, F, G, 1, I, J, K, L, M, N, O, P, Q)) [ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G - 1 >= 0 /\ C + G >= 0 /\ D - F >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 2 >= 0 /\ C + F - 1 >= 0 /\ E >= 0 /\ D + E - 1 >= 0 /\ C + E >= 0 /\ D - 1 >= 0 /\ C + D - 1 >= 0 /\ C >= 0 /\ D >= G + 1 /\ 0 >= G ] f10(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f14(A, B, C, D, E, F, G, 0, I, J, K, L, M, N, O, P, Q)) [ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G - 1 >= 0 /\ C + G >= 0 /\ D - F >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 2 >= 0 /\ C + F - 1 >= 0 /\ E >= 0 /\ D + E - 1 >= 0 /\ C + E >= 0 /\ D - 1 >= 0 /\ C + D - 1 >= 0 /\ C >= 0 /\ D >= G + 1 /\ G >= 1 ] f14(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f23(A, B, C, D, E, F, G, H, I, 1, L, L, M, N, O, P, Q)) [ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H >= 0 /\ C - H + 1 >= 0 /\ H >= 0 /\ G + H - 1 >= 0 /\ F + H - 1 >= 0 /\ E + H >= 0 /\ D + H - 2 >= 0 /\ C + H >= 0 /\ D - G - 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G - 1 >= 0 /\ C + G >= 0 /\ D - F >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 2 >= 0 /\ C + F - 1 >= 0 /\ E >= 0 /\ D + E - 1 >= 0 /\ C + E >= 0 /\ D - 1 >= 0 /\ C + D - 1 >= 0 /\ C >= 0 /\ I >= 0 /\ G + 1 >= D /\ 1 >= I ] f14(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f23(A, B, C, D, E, F, G, H, I, 0, L, L, M, N, O, P, Q)) [ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H >= 0 /\ C - H + 1 >= 0 /\ H >= 0 /\ G + H - 1 >= 0 /\ F + H - 1 >= 0 /\ E + H >= 0 /\ D + H - 2 >= 0 /\ C + H >= 0 /\ D - G - 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G - 1 >= 0 /\ C + G >= 0 /\ D - F >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 2 >= 0 /\ C + F - 1 >= 0 /\ E >= 0 /\ D + E - 1 >= 0 /\ C + E >= 0 /\ D - 1 >= 0 /\ C + D - 1 >= 0 /\ C >= 0 /\ I >= 0 /\ D >= G + 2 /\ 1 >= I ] f23(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f27(A, B, C, D, E + 1, F, G, H, I, J, K, L, M, N, O, P, Q)) [ -I + 1 >= 0 /\ -H - I + 2 >= 0 /\ G - I + 1 >= 0 /\ F - I >= 0 /\ E - I + 1 >= 0 /\ D - I >= 0 /\ C - I + 1 >= 0 /\ J - I + 1 >= 0 /\ -J - I + 2 >= 0 /\ I >= 0 /\ -H + I + 1 >= 0 /\ G + I >= 0 /\ F + I - 1 >= 0 /\ E + I >= 0 /\ D + I - 1 >= 0 /\ C + I >= 0 /\ J + I >= 0 /\ -J + I + 1 >= 0 /\ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H >= 0 /\ C - H + 1 >= 0 /\ J - H + 1 >= 0 /\ -J - H + 2 >= 0 /\ G + H - 1 >= 0 /\ D + H - 2 >= 0 /\ D - G - 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G - 1 >= 0 /\ C + G >= 0 /\ J + G >= 0 /\ -J + G + 1 >= 0 /\ D - F >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 2 >= 0 /\ C + F - 1 >= 0 /\ J + F - 1 >= 0 /\ -J + F >= 0 /\ E >= 0 /\ D + E - 1 >= 0 /\ C + E >= 0 /\ J + E >= 0 /\ -J + E + 1 >= 0 /\ D - 1 >= 0 /\ C + D - 1 >= 0 /\ J + D - 2 >= 0 /\ -J + D >= 0 /\ C >= 0 /\ J + C >= 0 /\ -J + C + 1 >= 0 /\ K - L >= 0 /\ -K + L >= 0 /\ -J + 1 >= 0 /\ J >= 0 /\ I >= 1 /\ 0 >= C /\ 0 >= E ] f23(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f27(A, B, C, D, E + 1, F, G, H, I, J, K, L, M, N, O, P, Q)) [ -I + 1 >= 0 /\ -H - I + 2 >= 0 /\ G - I + 1 >= 0 /\ F - I >= 0 /\ E - I + 1 >= 0 /\ D - I >= 0 /\ C - I + 1 >= 0 /\ J - I + 1 >= 0 /\ -J - I + 2 >= 0 /\ I >= 0 /\ -H + I + 1 >= 0 /\ G + I >= 0 /\ F + I - 1 >= 0 /\ E + I >= 0 /\ D + I - 1 >= 0 /\ C + I >= 0 /\ J + I >= 0 /\ -J + I + 1 >= 0 /\ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H >= 0 /\ C - H + 1 >= 0 /\ J - H + 1 >= 0 /\ -J - H + 2 >= 0 /\ G + H - 1 >= 0 /\ D + H - 2 >= 0 /\ D - G - 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G - 1 >= 0 /\ C + G >= 0 /\ J + G >= 0 /\ -J + G + 1 >= 0 /\ D - F >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 2 >= 0 /\ C + F - 1 >= 0 /\ J + F - 1 >= 0 /\ -J + F >= 0 /\ E >= 0 /\ D + E - 1 >= 0 /\ C + E >= 0 /\ J + E >= 0 /\ -J + E + 1 >= 0 /\ D - 1 >= 0 /\ C + D - 1 >= 0 /\ J + D - 2 >= 0 /\ -J + D >= 0 /\ C >= 0 /\ J + C >= 0 /\ -J + C + 1 >= 0 /\ K - L >= 0 /\ -K + L >= 0 /\ -J + 1 >= 0 /\ J >= 0 /\ I >= 1 /\ 0 >= C /\ E = 1 ] f23(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f27(A, B, C, D, 0, F + 1, G, H, I, J, K, L, M, N, O, P, Q)) [ -I + 1 >= 0 /\ -H - I + 2 >= 0 /\ G - I + 1 >= 0 /\ F - I >= 0 /\ E - I + 1 >= 0 /\ D - I >= 0 /\ C - I + 1 >= 0 /\ J - I + 1 >= 0 /\ -J - I + 2 >= 0 /\ I >= 0 /\ -H + I + 1 >= 0 /\ G + I >= 0 /\ F + I - 1 >= 0 /\ E + I >= 0 /\ D + I - 1 >= 0 /\ C + I >= 0 /\ J + I >= 0 /\ -J + I + 1 >= 0 /\ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H >= 0 /\ C - H + 1 >= 0 /\ J - H + 1 >= 0 /\ -J - H + 2 >= 0 /\ G + H - 1 >= 0 /\ D + H - 2 >= 0 /\ D - G - 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G - 1 >= 0 /\ C + G >= 0 /\ J + G >= 0 /\ -J + G + 1 >= 0 /\ D - F >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 2 >= 0 /\ C + F - 1 >= 0 /\ J + F - 1 >= 0 /\ -J + F >= 0 /\ E >= 0 /\ D + E - 1 >= 0 /\ C + E >= 0 /\ J + E >= 0 /\ -J + E + 1 >= 0 /\ D - 1 >= 0 /\ C + D - 1 >= 0 /\ J + D - 2 >= 0 /\ -J + D >= 0 /\ C >= 0 /\ J + C >= 0 /\ -J + C + 1 >= 0 /\ K - L >= 0 /\ -K + L >= 0 /\ -J + 1 >= 0 /\ J >= 0 /\ E >= 2 /\ C = 0 ] f23(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f27(A, B, C - 1, D, E, F, G, H, I, J, K, L, M, N, O, P, Q)) [ -I + 1 >= 0 /\ -H - I + 2 >= 0 /\ G - I + 1 >= 0 /\ F - I >= 0 /\ E - I + 1 >= 0 /\ D - I >= 0 /\ C - I + 1 >= 0 /\ J - I + 1 >= 0 /\ -J - I + 2 >= 0 /\ I >= 0 /\ -H + I + 1 >= 0 /\ G + I >= 0 /\ F + I - 1 >= 0 /\ E + I >= 0 /\ D + I - 1 >= 0 /\ C + I >= 0 /\ J + I >= 0 /\ -J + I + 1 >= 0 /\ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H >= 0 /\ C - H + 1 >= 0 /\ J - H + 1 >= 0 /\ -J - H + 2 >= 0 /\ G + H - 1 >= 0 /\ D + H - 2 >= 0 /\ D - G - 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G - 1 >= 0 /\ C + G >= 0 /\ J + G >= 0 /\ -J + G + 1 >= 0 /\ D - F >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 2 >= 0 /\ C + F - 1 >= 0 /\ J + F - 1 >= 0 /\ -J + F >= 0 /\ E >= 0 /\ D + E - 1 >= 0 /\ C + E >= 0 /\ J + E >= 0 /\ -J + E + 1 >= 0 /\ D - 1 >= 0 /\ C + D - 1 >= 0 /\ J + D - 2 >= 0 /\ -J + D >= 0 /\ C >= 0 /\ J + C >= 0 /\ -J + C + 1 >= 0 /\ K - L >= 0 /\ -K + L >= 0 /\ -J + 1 >= 0 /\ J >= 0 /\ C >= 1 ] f27(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f42(H, J, C, D, E, F, G, H, I, J, K, L, 1, K, O, P, Q)) [ -I + 1 >= 0 /\ -H - I + 2 >= 0 /\ G - I + 1 >= 0 /\ F - I >= 0 /\ E - I + 1 >= 0 /\ D - I >= 0 /\ C - I + 1 >= 0 /\ J - I + 1 >= 0 /\ -J - I + 2 >= 0 /\ I >= 0 /\ -H + I + 1 >= 0 /\ G + I >= 0 /\ F + I - 1 >= 0 /\ E + I >= 0 /\ D + I - 1 >= 0 /\ C + I >= 0 /\ J + I >= 0 /\ -J + I + 1 >= 0 /\ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H >= 0 /\ C - H + 1 >= 0 /\ J - H + 1 >= 0 /\ -J - H + 2 >= 0 /\ G + H - 1 >= 0 /\ D + H - 2 >= 0 /\ D - G - 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G - 1 >= 0 /\ C + G >= 0 /\ J + G >= 0 /\ -J + G + 1 >= 0 /\ D - F + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 2 >= 0 /\ C + F - 1 >= 0 /\ J + F - 1 >= 0 /\ -J + F >= 0 /\ E >= 0 /\ D + E - 1 >= 0 /\ C + E >= 0 /\ J + E >= 0 /\ -J + E + 1 >= 0 /\ D - 1 >= 0 /\ C + D - 1 >= 0 /\ J + D - 2 >= 0 /\ -J + D >= 0 /\ C >= 0 /\ J + C >= 0 /\ -J + C + 1 >= 0 /\ K - L >= 0 /\ -K + L >= 0 /\ -J + 1 >= 0 /\ J >= 0 /\ M >= 1 /\ I >= 1 ] f27(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f42(H, J, C, D, E, F, G, H, I, J, K, L, 1, K, K, P, Q)) [ -I + 1 >= 0 /\ -H - I + 2 >= 0 /\ G - I + 1 >= 0 /\ F - I >= 0 /\ E - I + 1 >= 0 /\ D - I >= 0 /\ C - I + 1 >= 0 /\ J - I + 1 >= 0 /\ -J - I + 2 >= 0 /\ I >= 0 /\ -H + I + 1 >= 0 /\ G + I >= 0 /\ F + I - 1 >= 0 /\ E + I >= 0 /\ D + I - 1 >= 0 /\ C + I >= 0 /\ J + I >= 0 /\ -J + I + 1 >= 0 /\ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H >= 0 /\ C - H + 1 >= 0 /\ J - H + 1 >= 0 /\ -J - H + 2 >= 0 /\ G + H - 1 >= 0 /\ D + H - 2 >= 0 /\ D - G - 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G - 1 >= 0 /\ C + G >= 0 /\ J + G >= 0 /\ -J + G + 1 >= 0 /\ D - F + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 2 >= 0 /\ C + F - 1 >= 0 /\ J + F - 1 >= 0 /\ -J + F >= 0 /\ E >= 0 /\ D + E - 1 >= 0 /\ C + E >= 0 /\ J + E >= 0 /\ -J + E + 1 >= 0 /\ D - 1 >= 0 /\ C + D - 1 >= 0 /\ J + D - 2 >= 0 /\ -J + D >= 0 /\ C >= 0 /\ J + C >= 0 /\ -J + C + 1 >= 0 /\ K - L >= 0 /\ -K + L >= 0 /\ -J + 1 >= 0 /\ J >= 0 /\ 0 >= M /\ I >= 1 ] f42(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f44(A, B, C, D, E, F, G, H, I, J, K, L, M, N, N, P, Q)) [ -I + 1 >= 0 /\ -H - I + 2 >= 0 /\ G - I + 1 >= 0 /\ F - I >= 0 /\ E - I + 1 >= 0 /\ D - I >= 0 /\ C - I + 1 >= 0 /\ B - I + 1 >= 0 /\ -B - I + 2 >= 0 /\ M - I >= 0 /\ -M - I + 2 >= 0 /\ J - I + 1 >= 0 /\ -J - I + 2 >= 0 /\ -A - I + 2 >= 0 /\ I - 1 >= 0 /\ -H + I >= 0 /\ G + I - 1 >= 0 /\ F + I - 2 >= 0 /\ E + I - 1 >= 0 /\ D + I - 2 >= 0 /\ C + I - 1 >= 0 /\ B + I - 1 >= 0 /\ -B + I >= 0 /\ M + I - 2 >= 0 /\ -M + I >= 0 /\ J + I - 1 >= 0 /\ -J + I >= 0 /\ -A + I >= 0 /\ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H >= 0 /\ C - H + 1 >= 0 /\ B - H + 1 >= 0 /\ -B - H + 2 >= 0 /\ M - H >= 0 /\ -M - H + 2 >= 0 /\ J - H + 1 >= 0 /\ -J - H + 2 >= 0 /\ A - H >= 0 /\ -A - H + 2 >= 0 /\ G + H - 1 >= 0 /\ D + H - 2 >= 0 /\ -A + H >= 0 /\ D - G - 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G - 1 >= 0 /\ C + G >= 0 /\ B + G >= 0 /\ -B + G + 1 >= 0 /\ M + G - 1 >= 0 /\ -M + G + 1 >= 0 /\ J + G >= 0 /\ -J + G + 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ D - F + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 2 >= 0 /\ C + F - 1 >= 0 /\ B + F - 1 >= 0 /\ -B + F >= 0 /\ M + F - 2 >= 0 /\ -M + F >= 0 /\ J + F - 1 >= 0 /\ -J + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E - 1 >= 0 /\ C + E >= 0 /\ B + E >= 0 /\ -B + E + 1 >= 0 /\ M + E - 1 >= 0 /\ -M + E + 1 >= 0 /\ J + E >= 0 /\ -J + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ D - 1 >= 0 /\ C + D - 1 >= 0 /\ B + D - 2 >= 0 /\ -B + D >= 0 /\ M + D - 2 >= 0 /\ -M + D >= 0 /\ J + D - 2 >= 0 /\ -J + D >= 0 /\ A + D - 2 >= 0 /\ -A + D >= 0 /\ C >= 0 /\ B + C >= 0 /\ -B + C + 1 >= 0 /\ M + C - 1 >= 0 /\ -M + C + 1 >= 0 /\ J + C >= 0 /\ -J + C + 1 >= 0 /\ -A + C + 1 >= 0 /\ -B + 1 >= 0 /\ M - B >= 0 /\ -M - B + 2 >= 0 /\ J - B >= 0 /\ -J - B + 2 >= 0 /\ -A - B + 2 >= 0 /\ B >= 0 /\ M + B - 1 >= 0 /\ -M + B + 1 >= 0 /\ J + B >= 0 /\ -J + B >= 0 /\ -A + B + 1 >= 0 /\ L - N >= 0 /\ K - N >= 0 /\ -L + N >= 0 /\ -K + N >= 0 /\ -M + 1 >= 0 /\ J - M + 1 >= 0 /\ -J - M + 2 >= 0 /\ -A - M + 2 >= 0 /\ M - 1 >= 0 /\ J + M - 1 >= 0 /\ -J + M >= 0 /\ -A + M >= 0 /\ K - L >= 0 /\ -K + L >= 0 /\ -J + 1 >= 0 /\ -A - J + 2 >= 0 /\ J >= 0 /\ -A + J + 1 >= 0 /\ -A + 1 >= 0 /\ 0 >= A + 1 /\ N = O ] f42(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f44(A, B, C, D, E, F, G, H, I, J, K, L, M, N, N, P, Q)) [ -I + 1 >= 0 /\ -H - I + 2 >= 0 /\ G - I + 1 >= 0 /\ F - I >= 0 /\ E - I + 1 >= 0 /\ D - I >= 0 /\ C - I + 1 >= 0 /\ B - I + 1 >= 0 /\ -B - I + 2 >= 0 /\ M - I >= 0 /\ -M - I + 2 >= 0 /\ J - I + 1 >= 0 /\ -J - I + 2 >= 0 /\ -A - I + 2 >= 0 /\ I - 1 >= 0 /\ -H + I >= 0 /\ G + I - 1 >= 0 /\ F + I - 2 >= 0 /\ E + I - 1 >= 0 /\ D + I - 2 >= 0 /\ C + I - 1 >= 0 /\ B + I - 1 >= 0 /\ -B + I >= 0 /\ M + I - 2 >= 0 /\ -M + I >= 0 /\ J + I - 1 >= 0 /\ -J + I >= 0 /\ -A + I >= 0 /\ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H >= 0 /\ C - H + 1 >= 0 /\ B - H + 1 >= 0 /\ -B - H + 2 >= 0 /\ M - H >= 0 /\ -M - H + 2 >= 0 /\ J - H + 1 >= 0 /\ -J - H + 2 >= 0 /\ A - H >= 0 /\ -A - H + 2 >= 0 /\ G + H - 1 >= 0 /\ D + H - 2 >= 0 /\ -A + H >= 0 /\ D - G - 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G - 1 >= 0 /\ C + G >= 0 /\ B + G >= 0 /\ -B + G + 1 >= 0 /\ M + G - 1 >= 0 /\ -M + G + 1 >= 0 /\ J + G >= 0 /\ -J + G + 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ D - F + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 2 >= 0 /\ C + F - 1 >= 0 /\ B + F - 1 >= 0 /\ -B + F >= 0 /\ M + F - 2 >= 0 /\ -M + F >= 0 /\ J + F - 1 >= 0 /\ -J + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E - 1 >= 0 /\ C + E >= 0 /\ B + E >= 0 /\ -B + E + 1 >= 0 /\ M + E - 1 >= 0 /\ -M + E + 1 >= 0 /\ J + E >= 0 /\ -J + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ D - 1 >= 0 /\ C + D - 1 >= 0 /\ B + D - 2 >= 0 /\ -B + D >= 0 /\ M + D - 2 >= 0 /\ -M + D >= 0 /\ J + D - 2 >= 0 /\ -J + D >= 0 /\ A + D - 2 >= 0 /\ -A + D >= 0 /\ C >= 0 /\ B + C >= 0 /\ -B + C + 1 >= 0 /\ M + C - 1 >= 0 /\ -M + C + 1 >= 0 /\ J + C >= 0 /\ -J + C + 1 >= 0 /\ -A + C + 1 >= 0 /\ -B + 1 >= 0 /\ M - B >= 0 /\ -M - B + 2 >= 0 /\ J - B >= 0 /\ -J - B + 2 >= 0 /\ -A - B + 2 >= 0 /\ B >= 0 /\ M + B - 1 >= 0 /\ -M + B + 1 >= 0 /\ J + B >= 0 /\ -J + B >= 0 /\ -A + B + 1 >= 0 /\ L - N >= 0 /\ K - N >= 0 /\ -L + N >= 0 /\ -K + N >= 0 /\ -M + 1 >= 0 /\ J - M + 1 >= 0 /\ -J - M + 2 >= 0 /\ -A - M + 2 >= 0 /\ M - 1 >= 0 /\ J + M - 1 >= 0 /\ -J + M >= 0 /\ -A + M >= 0 /\ K - L >= 0 /\ -K + L >= 0 /\ -J + 1 >= 0 /\ -A - J + 2 >= 0 /\ J >= 0 /\ -A + J + 1 >= 0 /\ -A + 1 >= 0 /\ A >= 1 /\ N = O ] f42(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f48(0, B, C, D, E, F, G, H, I, J, K, L, M, N, N, P, Q)) [ -I + 1 >= 0 /\ -H - I + 2 >= 0 /\ G - I + 1 >= 0 /\ F - I >= 0 /\ E - I + 1 >= 0 /\ D - I >= 0 /\ C - I + 1 >= 0 /\ B - I + 1 >= 0 /\ -B - I + 2 >= 0 /\ M - I >= 0 /\ -M - I + 2 >= 0 /\ J - I + 1 >= 0 /\ -J - I + 2 >= 0 /\ -A - I + 2 >= 0 /\ I - 1 >= 0 /\ -H + I >= 0 /\ G + I - 1 >= 0 /\ F + I - 2 >= 0 /\ E + I - 1 >= 0 /\ D + I - 2 >= 0 /\ C + I - 1 >= 0 /\ B + I - 1 >= 0 /\ -B + I >= 0 /\ M + I - 2 >= 0 /\ -M + I >= 0 /\ J + I - 1 >= 0 /\ -J + I >= 0 /\ -A + I >= 0 /\ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H >= 0 /\ C - H + 1 >= 0 /\ B - H + 1 >= 0 /\ -B - H + 2 >= 0 /\ M - H >= 0 /\ -M - H + 2 >= 0 /\ J - H + 1 >= 0 /\ -J - H + 2 >= 0 /\ A - H >= 0 /\ -A - H + 2 >= 0 /\ G + H - 1 >= 0 /\ D + H - 2 >= 0 /\ -A + H >= 0 /\ D - G - 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G - 1 >= 0 /\ C + G >= 0 /\ B + G >= 0 /\ -B + G + 1 >= 0 /\ M + G - 1 >= 0 /\ -M + G + 1 >= 0 /\ J + G >= 0 /\ -J + G + 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ D - F + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 2 >= 0 /\ C + F - 1 >= 0 /\ B + F - 1 >= 0 /\ -B + F >= 0 /\ M + F - 2 >= 0 /\ -M + F >= 0 /\ J + F - 1 >= 0 /\ -J + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E - 1 >= 0 /\ C + E >= 0 /\ B + E >= 0 /\ -B + E + 1 >= 0 /\ M + E - 1 >= 0 /\ -M + E + 1 >= 0 /\ J + E >= 0 /\ -J + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ D - 1 >= 0 /\ C + D - 1 >= 0 /\ B + D - 2 >= 0 /\ -B + D >= 0 /\ M + D - 2 >= 0 /\ -M + D >= 0 /\ J + D - 2 >= 0 /\ -J + D >= 0 /\ A + D - 2 >= 0 /\ -A + D >= 0 /\ C >= 0 /\ B + C >= 0 /\ -B + C + 1 >= 0 /\ M + C - 1 >= 0 /\ -M + C + 1 >= 0 /\ J + C >= 0 /\ -J + C + 1 >= 0 /\ -A + C + 1 >= 0 /\ -B + 1 >= 0 /\ M - B >= 0 /\ -M - B + 2 >= 0 /\ J - B >= 0 /\ -J - B + 2 >= 0 /\ -A - B + 2 >= 0 /\ B >= 0 /\ M + B - 1 >= 0 /\ -M + B + 1 >= 0 /\ J + B >= 0 /\ -J + B >= 0 /\ -A + B + 1 >= 0 /\ L - N >= 0 /\ K - N >= 0 /\ -L + N >= 0 /\ -K + N >= 0 /\ -M + 1 >= 0 /\ J - M + 1 >= 0 /\ -J - M + 2 >= 0 /\ -A - M + 2 >= 0 /\ M - 1 >= 0 /\ J + M - 1 >= 0 /\ -J + M >= 0 /\ -A + M >= 0 /\ K - L >= 0 /\ -K + L >= 0 /\ -J + 1 >= 0 /\ -A - J + 2 >= 0 /\ J >= 0 /\ -A + J + 1 >= 0 /\ -A + 1 >= 0 /\ A = 0 /\ N = O ] f44(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f46(A, 0, C, D, E, F, G, H, I, J, K, L, M, N, O, 1, Q)) [ -I + 1 >= 0 /\ -H - I + 2 >= 0 /\ G - I + 1 >= 0 /\ F - I >= 0 /\ E - I + 1 >= 0 /\ D - I >= 0 /\ C - I + 1 >= 0 /\ B - I + 1 >= 0 /\ -B - I + 2 >= 0 /\ M - I >= 0 /\ -M - I + 2 >= 0 /\ J - I + 1 >= 0 /\ -J - I + 2 >= 0 /\ -A - I + 2 >= 0 /\ I - 1 >= 0 /\ -H + I >= 0 /\ G + I - 1 >= 0 /\ F + I - 2 >= 0 /\ E + I - 1 >= 0 /\ D + I - 2 >= 0 /\ C + I - 1 >= 0 /\ B + I - 1 >= 0 /\ -B + I >= 0 /\ M + I - 2 >= 0 /\ -M + I >= 0 /\ J + I - 1 >= 0 /\ -J + I >= 0 /\ -A + I >= 0 /\ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H >= 0 /\ C - H + 1 >= 0 /\ B - H + 1 >= 0 /\ -B - H + 2 >= 0 /\ M - H >= 0 /\ -M - H + 2 >= 0 /\ J - H + 1 >= 0 /\ -J - H + 2 >= 0 /\ A - H >= 0 /\ -A - H + 2 >= 0 /\ G + H - 1 >= 0 /\ D + H - 2 >= 0 /\ -A + H >= 0 /\ D - G - 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G - 1 >= 0 /\ C + G >= 0 /\ B + G >= 0 /\ -B + G + 1 >= 0 /\ M + G - 1 >= 0 /\ -M + G + 1 >= 0 /\ J + G >= 0 /\ -J + G + 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ D - F + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 2 >= 0 /\ C + F - 1 >= 0 /\ B + F - 1 >= 0 /\ -B + F >= 0 /\ M + F - 2 >= 0 /\ -M + F >= 0 /\ J + F - 1 >= 0 /\ -J + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E - 1 >= 0 /\ C + E >= 0 /\ B + E >= 0 /\ -B + E + 1 >= 0 /\ M + E - 1 >= 0 /\ -M + E + 1 >= 0 /\ J + E >= 0 /\ -J + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ D - 1 >= 0 /\ C + D - 1 >= 0 /\ B + D - 2 >= 0 /\ -B + D >= 0 /\ M + D - 2 >= 0 /\ -M + D >= 0 /\ J + D - 2 >= 0 /\ -J + D >= 0 /\ A + D - 2 >= 0 /\ -A + D >= 0 /\ C >= 0 /\ B + C >= 0 /\ -B + C + 1 >= 0 /\ M + C - 1 >= 0 /\ -M + C + 1 >= 0 /\ J + C >= 0 /\ -J + C + 1 >= 0 /\ -A + C + 1 >= 0 /\ -B + 1 >= 0 /\ M - B >= 0 /\ -M - B + 2 >= 0 /\ J - B >= 0 /\ -J - B + 2 >= 0 /\ -A - B + 2 >= 0 /\ B >= 0 /\ M + B - 1 >= 0 /\ -M + B + 1 >= 0 /\ J + B >= 0 /\ -J + B >= 0 /\ -A + B + 1 >= 0 /\ N - O >= 0 /\ L - O >= 0 /\ K - O >= 0 /\ -N + O >= 0 /\ -L + O >= 0 /\ -K + O >= 0 /\ L - N >= 0 /\ K - N >= 0 /\ -L + N >= 0 /\ -K + N >= 0 /\ -M + 1 >= 0 /\ J - M + 1 >= 0 /\ -J - M + 2 >= 0 /\ -A - M + 2 >= 0 /\ M - 1 >= 0 /\ J + M - 1 >= 0 /\ -J + M >= 0 /\ -A + M >= 0 /\ K - L >= 0 /\ -K + L >= 0 /\ -J + 1 >= 0 /\ -A - J + 2 >= 0 /\ J >= 0 /\ -A + J + 1 >= 0 /\ -A + 1 >= 0 /\ B = 0 ] f44(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f48(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q)) [ -I + 1 >= 0 /\ -H - I + 2 >= 0 /\ G - I + 1 >= 0 /\ F - I >= 0 /\ E - I + 1 >= 0 /\ D - I >= 0 /\ C - I + 1 >= 0 /\ B - I + 1 >= 0 /\ -B - I + 2 >= 0 /\ M - I >= 0 /\ -M - I + 2 >= 0 /\ J - I + 1 >= 0 /\ -J - I + 2 >= 0 /\ -A - I + 2 >= 0 /\ I - 1 >= 0 /\ -H + I >= 0 /\ G + I - 1 >= 0 /\ F + I - 2 >= 0 /\ E + I - 1 >= 0 /\ D + I - 2 >= 0 /\ C + I - 1 >= 0 /\ B + I - 1 >= 0 /\ -B + I >= 0 /\ M + I - 2 >= 0 /\ -M + I >= 0 /\ J + I - 1 >= 0 /\ -J + I >= 0 /\ -A + I >= 0 /\ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H >= 0 /\ C - H + 1 >= 0 /\ B - H + 1 >= 0 /\ -B - H + 2 >= 0 /\ M - H >= 0 /\ -M - H + 2 >= 0 /\ J - H + 1 >= 0 /\ -J - H + 2 >= 0 /\ A - H >= 0 /\ -A - H + 2 >= 0 /\ G + H - 1 >= 0 /\ D + H - 2 >= 0 /\ -A + H >= 0 /\ D - G - 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G - 1 >= 0 /\ C + G >= 0 /\ B + G >= 0 /\ -B + G + 1 >= 0 /\ M + G - 1 >= 0 /\ -M + G + 1 >= 0 /\ J + G >= 0 /\ -J + G + 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ D - F + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 2 >= 0 /\ C + F - 1 >= 0 /\ B + F - 1 >= 0 /\ -B + F >= 0 /\ M + F - 2 >= 0 /\ -M + F >= 0 /\ J + F - 1 >= 0 /\ -J + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E - 1 >= 0 /\ C + E >= 0 /\ B + E >= 0 /\ -B + E + 1 >= 0 /\ M + E - 1 >= 0 /\ -M + E + 1 >= 0 /\ J + E >= 0 /\ -J + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ D - 1 >= 0 /\ C + D - 1 >= 0 /\ B + D - 2 >= 0 /\ -B + D >= 0 /\ M + D - 2 >= 0 /\ -M + D >= 0 /\ J + D - 2 >= 0 /\ -J + D >= 0 /\ A + D - 2 >= 0 /\ -A + D >= 0 /\ C >= 0 /\ B + C >= 0 /\ -B + C + 1 >= 0 /\ M + C - 1 >= 0 /\ -M + C + 1 >= 0 /\ J + C >= 0 /\ -J + C + 1 >= 0 /\ -A + C + 1 >= 0 /\ -B + 1 >= 0 /\ M - B >= 0 /\ -M - B + 2 >= 0 /\ J - B >= 0 /\ -J - B + 2 >= 0 /\ -A - B + 2 >= 0 /\ B >= 0 /\ M + B - 1 >= 0 /\ -M + B + 1 >= 0 /\ J + B >= 0 /\ -J + B >= 0 /\ -A + B + 1 >= 0 /\ N - O >= 0 /\ L - O >= 0 /\ K - O >= 0 /\ -N + O >= 0 /\ -L + O >= 0 /\ -K + O >= 0 /\ L - N >= 0 /\ K - N >= 0 /\ -L + N >= 0 /\ -K + N >= 0 /\ -M + 1 >= 0 /\ J - M + 1 >= 0 /\ -J - M + 2 >= 0 /\ -A - M + 2 >= 0 /\ M - 1 >= 0 /\ J + M - 1 >= 0 /\ -J + M >= 0 /\ -A + M >= 0 /\ K - L >= 0 /\ -K + L >= 0 /\ -J + 1 >= 0 /\ -A - J + 2 >= 0 /\ J >= 0 /\ -A + J + 1 >= 0 /\ -A + 1 >= 0 /\ B >= 1 ] f48(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f46(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, 2, Q)) [ -I + 1 >= 0 /\ -H - I + 2 >= 0 /\ G - I + 1 >= 0 /\ F - I >= 0 /\ E - I + 1 >= 0 /\ D - I >= 0 /\ C - I + 1 >= 0 /\ B - I + 1 >= 0 /\ -B - I + 2 >= 0 /\ M - I >= 0 /\ -M - I + 2 >= 0 /\ J - I + 1 >= 0 /\ -J - I + 2 >= 0 /\ -A - I + 2 >= 0 /\ I - 1 >= 0 /\ -H + I >= 0 /\ G + I - 1 >= 0 /\ F + I - 2 >= 0 /\ E + I - 1 >= 0 /\ D + I - 2 >= 0 /\ C + I - 1 >= 0 /\ B + I - 1 >= 0 /\ -B + I >= 0 /\ M + I - 2 >= 0 /\ -M + I >= 0 /\ J + I - 1 >= 0 /\ -J + I >= 0 /\ -A + I >= 0 /\ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H >= 0 /\ C - H + 1 >= 0 /\ B - H >= 0 /\ -B - H + 2 >= 0 /\ M - H >= 0 /\ -M - H + 2 >= 0 /\ J - H >= 0 /\ -J - H + 2 >= 0 /\ A - H >= 0 /\ -A - H + 2 >= 0 /\ G + H - 1 >= 0 /\ D + H - 2 >= 0 /\ -A + H >= 0 /\ D - G - 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G - 1 >= 0 /\ C + G >= 0 /\ B + G - 1 >= 0 /\ -B + G + 1 >= 0 /\ M + G - 1 >= 0 /\ -M + G + 1 >= 0 /\ J + G - 1 >= 0 /\ -J + G + 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ D - F + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 2 >= 0 /\ C + F - 1 >= 0 /\ B + F - 1 >= 0 /\ -B + F >= 0 /\ M + F - 2 >= 0 /\ -M + F >= 0 /\ J + F - 1 >= 0 /\ -J + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E - 1 >= 0 /\ C + E >= 0 /\ B + E >= 0 /\ -B + E + 1 >= 0 /\ M + E - 1 >= 0 /\ -M + E + 1 >= 0 /\ J + E >= 0 /\ -J + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ D - 1 >= 0 /\ C + D - 1 >= 0 /\ B + D - 2 >= 0 /\ -B + D >= 0 /\ M + D - 2 >= 0 /\ -M + D >= 0 /\ J + D - 2 >= 0 /\ -J + D >= 0 /\ A + D - 2 >= 0 /\ -A + D >= 0 /\ C >= 0 /\ B + C >= 0 /\ -B + C + 1 >= 0 /\ M + C - 1 >= 0 /\ -M + C + 1 >= 0 /\ J + C >= 0 /\ -J + C + 1 >= 0 /\ -A + C + 1 >= 0 /\ -B + 1 >= 0 /\ M - B >= 0 /\ -M - B + 2 >= 0 /\ J - B >= 0 /\ -J - B + 2 >= 0 /\ -A - B + 2 >= 0 /\ B >= 0 /\ M + B - 1 >= 0 /\ -M + B + 1 >= 0 /\ J + B >= 0 /\ -J + B >= 0 /\ -A + B >= 0 /\ N - O >= 0 /\ L - O >= 0 /\ K - O >= 0 /\ -N + O >= 0 /\ -L + O >= 0 /\ -K + O >= 0 /\ L - N >= 0 /\ K - N >= 0 /\ -L + N >= 0 /\ -K + N >= 0 /\ -M + 1 >= 0 /\ J - M + 1 >= 0 /\ -J - M + 2 >= 0 /\ -A - M + 2 >= 0 /\ M - 1 >= 0 /\ J + M - 1 >= 0 /\ -J + M >= 0 /\ -A + M >= 0 /\ K - L >= 0 /\ -K + L >= 0 /\ -J + 1 >= 0 /\ -A - J + 2 >= 0 /\ J >= 0 /\ -A + J >= 0 /\ -A + 1 >= 0 /\ 0 >= B /\ 0 >= A ] f48(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f52(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q)) [ -I + 1 >= 0 /\ -H - I + 2 >= 0 /\ G - I + 1 >= 0 /\ F - I >= 0 /\ E - I + 1 >= 0 /\ D - I >= 0 /\ C - I + 1 >= 0 /\ B - I + 1 >= 0 /\ -B - I + 2 >= 0 /\ M - I >= 0 /\ -M - I + 2 >= 0 /\ J - I + 1 >= 0 /\ -J - I + 2 >= 0 /\ -A - I + 2 >= 0 /\ I - 1 >= 0 /\ -H + I >= 0 /\ G + I - 1 >= 0 /\ F + I - 2 >= 0 /\ E + I - 1 >= 0 /\ D + I - 2 >= 0 /\ C + I - 1 >= 0 /\ B + I - 1 >= 0 /\ -B + I >= 0 /\ M + I - 2 >= 0 /\ -M + I >= 0 /\ J + I - 1 >= 0 /\ -J + I >= 0 /\ -A + I >= 0 /\ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H >= 0 /\ C - H + 1 >= 0 /\ B - H >= 0 /\ -B - H + 2 >= 0 /\ M - H >= 0 /\ -M - H + 2 >= 0 /\ J - H >= 0 /\ -J - H + 2 >= 0 /\ A - H >= 0 /\ -A - H + 2 >= 0 /\ G + H - 1 >= 0 /\ D + H - 2 >= 0 /\ -A + H >= 0 /\ D - G - 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G - 1 >= 0 /\ C + G >= 0 /\ B + G - 1 >= 0 /\ -B + G + 1 >= 0 /\ M + G - 1 >= 0 /\ -M + G + 1 >= 0 /\ J + G - 1 >= 0 /\ -J + G + 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ D - F + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 2 >= 0 /\ C + F - 1 >= 0 /\ B + F - 1 >= 0 /\ -B + F >= 0 /\ M + F - 2 >= 0 /\ -M + F >= 0 /\ J + F - 1 >= 0 /\ -J + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E - 1 >= 0 /\ C + E >= 0 /\ B + E >= 0 /\ -B + E + 1 >= 0 /\ M + E - 1 >= 0 /\ -M + E + 1 >= 0 /\ J + E >= 0 /\ -J + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ D - 1 >= 0 /\ C + D - 1 >= 0 /\ B + D - 2 >= 0 /\ -B + D >= 0 /\ M + D - 2 >= 0 /\ -M + D >= 0 /\ J + D - 2 >= 0 /\ -J + D >= 0 /\ A + D - 2 >= 0 /\ -A + D >= 0 /\ C >= 0 /\ B + C >= 0 /\ -B + C + 1 >= 0 /\ M + C - 1 >= 0 /\ -M + C + 1 >= 0 /\ J + C >= 0 /\ -J + C + 1 >= 0 /\ -A + C + 1 >= 0 /\ -B + 1 >= 0 /\ M - B >= 0 /\ -M - B + 2 >= 0 /\ J - B >= 0 /\ -J - B + 2 >= 0 /\ -A - B + 2 >= 0 /\ B >= 0 /\ M + B - 1 >= 0 /\ -M + B + 1 >= 0 /\ J + B >= 0 /\ -J + B >= 0 /\ -A + B >= 0 /\ N - O >= 0 /\ L - O >= 0 /\ K - O >= 0 /\ -N + O >= 0 /\ -L + O >= 0 /\ -K + O >= 0 /\ L - N >= 0 /\ K - N >= 0 /\ -L + N >= 0 /\ -K + N >= 0 /\ -M + 1 >= 0 /\ J - M + 1 >= 0 /\ -J - M + 2 >= 0 /\ -A - M + 2 >= 0 /\ M - 1 >= 0 /\ J + M - 1 >= 0 /\ -J + M >= 0 /\ -A + M >= 0 /\ K - L >= 0 /\ -K + L >= 0 /\ -J + 1 >= 0 /\ -A - J + 2 >= 0 /\ J >= 0 /\ -A + J >= 0 /\ -A + 1 >= 0 /\ B >= 1 /\ 0 >= A ] f52(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f46(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, 3, Q)) [ -I + 1 >= 0 /\ -H - I + 2 >= 0 /\ G - I + 1 >= 0 /\ F - I >= 0 /\ E - I + 1 >= 0 /\ D - I >= 0 /\ C - I + 1 >= 0 /\ B - I >= 0 /\ -B - I + 2 >= 0 /\ M - I >= 0 /\ -M - I + 2 >= 0 /\ J - I >= 0 /\ -J - I + 2 >= 0 /\ -A - I + 2 >= 0 /\ I - 1 >= 0 /\ -H + I >= 0 /\ G + I - 1 >= 0 /\ F + I - 2 >= 0 /\ E + I - 1 >= 0 /\ D + I - 2 >= 0 /\ C + I - 1 >= 0 /\ B + I - 2 >= 0 /\ -B + I >= 0 /\ M + I - 2 >= 0 /\ -M + I >= 0 /\ J + I - 2 >= 0 /\ -J + I >= 0 /\ -A + I >= 0 /\ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H >= 0 /\ C - H + 1 >= 0 /\ B - H >= 0 /\ -B - H + 2 >= 0 /\ M - H >= 0 /\ -M - H + 2 >= 0 /\ J - H >= 0 /\ -J - H + 2 >= 0 /\ A - H >= 0 /\ -A - H + 2 >= 0 /\ G + H - 1 >= 0 /\ D + H - 2 >= 0 /\ -A + H >= 0 /\ D - G - 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G - 1 >= 0 /\ C + G >= 0 /\ B + G - 1 >= 0 /\ -B + G + 1 >= 0 /\ M + G - 1 >= 0 /\ -M + G + 1 >= 0 /\ J + G - 1 >= 0 /\ -J + G + 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ D - F + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 2 >= 0 /\ C + F - 1 >= 0 /\ B + F - 2 >= 0 /\ -B + F >= 0 /\ M + F - 2 >= 0 /\ -M + F >= 0 /\ J + F - 2 >= 0 /\ -J + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E - 1 >= 0 /\ C + E >= 0 /\ B + E - 1 >= 0 /\ -B + E + 1 >= 0 /\ M + E - 1 >= 0 /\ -M + E + 1 >= 0 /\ J + E - 1 >= 0 /\ -J + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ D - 1 >= 0 /\ C + D - 1 >= 0 /\ B + D - 2 >= 0 /\ -B + D >= 0 /\ M + D - 2 >= 0 /\ -M + D >= 0 /\ J + D - 2 >= 0 /\ -J + D >= 0 /\ A + D - 2 >= 0 /\ -A + D >= 0 /\ C >= 0 /\ B + C - 1 >= 0 /\ -B + C + 1 >= 0 /\ M + C - 1 >= 0 /\ -M + C + 1 >= 0 /\ J + C - 1 >= 0 /\ -J + C + 1 >= 0 /\ -A + C + 1 >= 0 /\ -B + 1 >= 0 /\ M - B >= 0 /\ -M - B + 2 >= 0 /\ J - B >= 0 /\ -J - B + 2 >= 0 /\ -A - B + 2 >= 0 /\ B - 1 >= 0 /\ M + B - 2 >= 0 /\ -M + B >= 0 /\ J + B - 2 >= 0 /\ -J + B >= 0 /\ -A + B >= 0 /\ N - O >= 0 /\ L - O >= 0 /\ K - O >= 0 /\ -N + O >= 0 /\ -L + O >= 0 /\ -K + O >= 0 /\ L - N >= 0 /\ K - N >= 0 /\ -L + N >= 0 /\ -K + N >= 0 /\ -M + 1 >= 0 /\ J - M >= 0 /\ -J - M + 2 >= 0 /\ -A - M + 2 >= 0 /\ M - 1 >= 0 /\ J + M - 2 >= 0 /\ -J + M >= 0 /\ -A + M >= 0 /\ K - L >= 0 /\ -K + L >= 0 /\ -J + 1 >= 0 /\ -A - J + 2 >= 0 /\ J - 1 >= 0 /\ -A + J >= 0 /\ -A + 1 >= 0 /\ B >= 1 ] f42(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f59(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q)) [ -I + 1 >= 0 /\ -H - I + 2 >= 0 /\ G - I + 1 >= 0 /\ F - I >= 0 /\ E - I + 1 >= 0 /\ D - I >= 0 /\ C - I + 1 >= 0 /\ B - I + 1 >= 0 /\ -B - I + 2 >= 0 /\ M - I >= 0 /\ -M - I + 2 >= 0 /\ J - I + 1 >= 0 /\ -J - I + 2 >= 0 /\ -A - I + 2 >= 0 /\ I - 1 >= 0 /\ -H + I >= 0 /\ G + I - 1 >= 0 /\ F + I - 2 >= 0 /\ E + I - 1 >= 0 /\ D + I - 2 >= 0 /\ C + I - 1 >= 0 /\ B + I - 1 >= 0 /\ -B + I >= 0 /\ M + I - 2 >= 0 /\ -M + I >= 0 /\ J + I - 1 >= 0 /\ -J + I >= 0 /\ -A + I >= 0 /\ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H >= 0 /\ C - H + 1 >= 0 /\ B - H + 1 >= 0 /\ -B - H + 2 >= 0 /\ M - H >= 0 /\ -M - H + 2 >= 0 /\ J - H + 1 >= 0 /\ -J - H + 2 >= 0 /\ A - H >= 0 /\ -A - H + 2 >= 0 /\ G + H - 1 >= 0 /\ D + H - 2 >= 0 /\ -A + H >= 0 /\ D - G - 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G - 1 >= 0 /\ C + G >= 0 /\ B + G >= 0 /\ -B + G + 1 >= 0 /\ M + G - 1 >= 0 /\ -M + G + 1 >= 0 /\ J + G >= 0 /\ -J + G + 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ D - F + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 2 >= 0 /\ C + F - 1 >= 0 /\ B + F - 1 >= 0 /\ -B + F >= 0 /\ M + F - 2 >= 0 /\ -M + F >= 0 /\ J + F - 1 >= 0 /\ -J + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E - 1 >= 0 /\ C + E >= 0 /\ B + E >= 0 /\ -B + E + 1 >= 0 /\ M + E - 1 >= 0 /\ -M + E + 1 >= 0 /\ J + E >= 0 /\ -J + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ D - 1 >= 0 /\ C + D - 1 >= 0 /\ B + D - 2 >= 0 /\ -B + D >= 0 /\ M + D - 2 >= 0 /\ -M + D >= 0 /\ J + D - 2 >= 0 /\ -J + D >= 0 /\ A + D - 2 >= 0 /\ -A + D >= 0 /\ C >= 0 /\ B + C >= 0 /\ -B + C + 1 >= 0 /\ M + C - 1 >= 0 /\ -M + C + 1 >= 0 /\ J + C >= 0 /\ -J + C + 1 >= 0 /\ -A + C + 1 >= 0 /\ -B + 1 >= 0 /\ M - B >= 0 /\ -M - B + 2 >= 0 /\ J - B >= 0 /\ -J - B + 2 >= 0 /\ -A - B + 2 >= 0 /\ B >= 0 /\ M + B - 1 >= 0 /\ -M + B + 1 >= 0 /\ J + B >= 0 /\ -J + B >= 0 /\ -A + B + 1 >= 0 /\ L - N >= 0 /\ K - N >= 0 /\ -L + N >= 0 /\ -K + N >= 0 /\ -M + 1 >= 0 /\ J - M + 1 >= 0 /\ -J - M + 2 >= 0 /\ -A - M + 2 >= 0 /\ M - 1 >= 0 /\ J + M - 1 >= 0 /\ -J + M >= 0 /\ -A + M >= 0 /\ K - L >= 0 /\ -K + L >= 0 /\ -J + 1 >= 0 /\ -A - J + 2 >= 0 /\ J >= 0 /\ -A + J + 1 >= 0 /\ -A + 1 >= 0 /\ Q >= 0 /\ N >= O + 1 /\ 1 >= Q ] f42(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f59(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q)) [ -I + 1 >= 0 /\ -H - I + 2 >= 0 /\ G - I + 1 >= 0 /\ F - I >= 0 /\ E - I + 1 >= 0 /\ D - I >= 0 /\ C - I + 1 >= 0 /\ B - I + 1 >= 0 /\ -B - I + 2 >= 0 /\ M - I >= 0 /\ -M - I + 2 >= 0 /\ J - I + 1 >= 0 /\ -J - I + 2 >= 0 /\ -A - I + 2 >= 0 /\ I - 1 >= 0 /\ -H + I >= 0 /\ G + I - 1 >= 0 /\ F + I - 2 >= 0 /\ E + I - 1 >= 0 /\ D + I - 2 >= 0 /\ C + I - 1 >= 0 /\ B + I - 1 >= 0 /\ -B + I >= 0 /\ M + I - 2 >= 0 /\ -M + I >= 0 /\ J + I - 1 >= 0 /\ -J + I >= 0 /\ -A + I >= 0 /\ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H >= 0 /\ C - H + 1 >= 0 /\ B - H + 1 >= 0 /\ -B - H + 2 >= 0 /\ M - H >= 0 /\ -M - H + 2 >= 0 /\ J - H + 1 >= 0 /\ -J - H + 2 >= 0 /\ A - H >= 0 /\ -A - H + 2 >= 0 /\ G + H - 1 >= 0 /\ D + H - 2 >= 0 /\ -A + H >= 0 /\ D - G - 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G - 1 >= 0 /\ C + G >= 0 /\ B + G >= 0 /\ -B + G + 1 >= 0 /\ M + G - 1 >= 0 /\ -M + G + 1 >= 0 /\ J + G >= 0 /\ -J + G + 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ D - F + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 2 >= 0 /\ C + F - 1 >= 0 /\ B + F - 1 >= 0 /\ -B + F >= 0 /\ M + F - 2 >= 0 /\ -M + F >= 0 /\ J + F - 1 >= 0 /\ -J + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E - 1 >= 0 /\ C + E >= 0 /\ B + E >= 0 /\ -B + E + 1 >= 0 /\ M + E - 1 >= 0 /\ -M + E + 1 >= 0 /\ J + E >= 0 /\ -J + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ D - 1 >= 0 /\ C + D - 1 >= 0 /\ B + D - 2 >= 0 /\ -B + D >= 0 /\ M + D - 2 >= 0 /\ -M + D >= 0 /\ J + D - 2 >= 0 /\ -J + D >= 0 /\ A + D - 2 >= 0 /\ -A + D >= 0 /\ C >= 0 /\ B + C >= 0 /\ -B + C + 1 >= 0 /\ M + C - 1 >= 0 /\ -M + C + 1 >= 0 /\ J + C >= 0 /\ -J + C + 1 >= 0 /\ -A + C + 1 >= 0 /\ -B + 1 >= 0 /\ M - B >= 0 /\ -M - B + 2 >= 0 /\ J - B >= 0 /\ -J - B + 2 >= 0 /\ -A - B + 2 >= 0 /\ B >= 0 /\ M + B - 1 >= 0 /\ -M + B + 1 >= 0 /\ J + B >= 0 /\ -J + B >= 0 /\ -A + B + 1 >= 0 /\ L - N >= 0 /\ K - N >= 0 /\ -L + N >= 0 /\ -K + N >= 0 /\ -M + 1 >= 0 /\ J - M + 1 >= 0 /\ -J - M + 2 >= 0 /\ -A - M + 2 >= 0 /\ M - 1 >= 0 /\ J + M - 1 >= 0 /\ -J + M >= 0 /\ -A + M >= 0 /\ K - L >= 0 /\ -K + L >= 0 /\ -J + 1 >= 0 /\ -A - J + 2 >= 0 /\ J >= 0 /\ -A + J + 1 >= 0 /\ -A + 1 >= 0 /\ Q >= 0 /\ O >= N + 1 /\ 1 >= Q ] f46(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f59(A, B, C, D, E, F, G, H, I, J, K, L, M, N, 0, P, Q)) [ -I + 1 >= 0 /\ -H - I + 2 >= 0 /\ G - I + 1 >= 0 /\ F - I >= 0 /\ E - I + 1 >= 0 /\ D - I >= 0 /\ C - I + 1 >= 0 /\ B - I + 1 >= 0 /\ -B - I + 2 >= 0 /\ P - I >= 0 /\ -P - I + 4 >= 0 /\ M - I >= 0 /\ -M - I + 2 >= 0 /\ J - I + 1 >= 0 /\ -J - I + 2 >= 0 /\ -A - I + 2 >= 0 /\ I - 1 >= 0 /\ -H + I >= 0 /\ G + I - 1 >= 0 /\ F + I - 2 >= 0 /\ E + I - 1 >= 0 /\ D + I - 2 >= 0 /\ C + I - 1 >= 0 /\ B + I - 1 >= 0 /\ -B + I >= 0 /\ P + I - 2 >= 0 /\ -P + I + 2 >= 0 /\ M + I - 2 >= 0 /\ -M + I >= 0 /\ J + I - 1 >= 0 /\ -J + I >= 0 /\ -A + I >= 0 /\ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H >= 0 /\ C - H + 1 >= 0 /\ B - H + 1 >= 0 /\ -B - H + 2 >= 0 /\ P - H >= 0 /\ -P - H + 4 >= 0 /\ M - H >= 0 /\ -M - H + 2 >= 0 /\ J - H + 1 >= 0 /\ -J - H + 2 >= 0 /\ A - H >= 0 /\ -A - H + 2 >= 0 /\ G + H - 1 >= 0 /\ D + H - 2 >= 0 /\ -A + H >= 0 /\ D - G - 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G - 1 >= 0 /\ C + G >= 0 /\ B + G >= 0 /\ -B + G + 1 >= 0 /\ P + G - 1 >= 0 /\ -P + G + 3 >= 0 /\ M + G - 1 >= 0 /\ -M + G + 1 >= 0 /\ J + G >= 0 /\ -J + G + 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ D - F + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 2 >= 0 /\ C + F - 1 >= 0 /\ B + F - 1 >= 0 /\ -B + F >= 0 /\ P + F - 2 >= 0 /\ -P + F + 2 >= 0 /\ M + F - 2 >= 0 /\ -M + F >= 0 /\ J + F - 1 >= 0 /\ -J + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E - 1 >= 0 /\ C + E >= 0 /\ B + E >= 0 /\ -B + E + 1 >= 0 /\ P + E - 1 >= 0 /\ -P + E + 3 >= 0 /\ M + E - 1 >= 0 /\ -M + E + 1 >= 0 /\ J + E >= 0 /\ -J + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ D - 1 >= 0 /\ C + D - 1 >= 0 /\ B + D - 2 >= 0 /\ -B + D >= 0 /\ P + D - 3 >= 0 /\ -P + D + 2 >= 0 /\ M + D - 2 >= 0 /\ -M + D >= 0 /\ J + D - 2 >= 0 /\ -J + D >= 0 /\ A + D - 2 >= 0 /\ -A + D >= 0 /\ C >= 0 /\ B + C >= 0 /\ -B + C + 1 >= 0 /\ P + C - 1 >= 0 /\ -P + C + 3 >= 0 /\ M + C - 1 >= 0 /\ -M + C + 1 >= 0 /\ J + C >= 0 /\ -J + C + 1 >= 0 /\ -A + C + 1 >= 0 /\ -B + 1 >= 0 /\ P - B - 1 >= 0 /\ -P - B + 4 >= 0 /\ M - B >= 0 /\ -M - B + 2 >= 0 /\ J - B >= 0 /\ -J - B + 2 >= 0 /\ -A - B + 2 >= 0 /\ B >= 0 /\ P + B - 1 >= 0 /\ -P + B + 2 >= 0 /\ M + B - 1 >= 0 /\ -M + B + 1 >= 0 /\ J + B >= 0 /\ -J + B >= 0 /\ -A + B + 1 >= 0 /\ -P + 3 >= 0 /\ M - P + 2 >= 0 /\ -M - P + 4 >= 0 /\ J - P + 2 >= 0 /\ -J - P + 4 >= 0 /\ -A - P + 4 >= 0 /\ P - 1 >= 0 /\ M + P - 2 >= 0 /\ -M + P >= 0 /\ J + P - 1 >= 0 /\ -J + P - 1 >= 0 /\ -A + P >= 0 /\ N - O >= 0 /\ L - O >= 0 /\ K - O >= 0 /\ -N + O >= 0 /\ -L + O >= 0 /\ -K + O >= 0 /\ L - N >= 0 /\ K - N >= 0 /\ -L + N >= 0 /\ -K + N >= 0 /\ -M + 1 >= 0 /\ J - M + 1 >= 0 /\ -J - M + 2 >= 0 /\ -A - M + 2 >= 0 /\ M - 1 >= 0 /\ J + M - 1 >= 0 /\ -J + M >= 0 /\ -A + M >= 0 /\ K - L >= 0 /\ -K + L >= 0 /\ -J + 1 >= 0 /\ -A - J + 2 >= 0 /\ J >= 0 /\ -A + J + 1 >= 0 /\ -A + 1 >= 0 /\ Q >= 0 /\ O >= 1 /\ 1 >= Q ] f46(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f59(A, B, C, D, E, F, G, H, I, J, K, L, M, N, 1, P, Q)) [ -I + 1 >= 0 /\ -H - I + 2 >= 0 /\ G - I + 1 >= 0 /\ F - I >= 0 /\ E - I + 1 >= 0 /\ D - I >= 0 /\ C - I + 1 >= 0 /\ B - I + 1 >= 0 /\ -B - I + 2 >= 0 /\ P - I >= 0 /\ -P - I + 4 >= 0 /\ M - I >= 0 /\ -M - I + 2 >= 0 /\ J - I + 1 >= 0 /\ -J - I + 2 >= 0 /\ -A - I + 2 >= 0 /\ I - 1 >= 0 /\ -H + I >= 0 /\ G + I - 1 >= 0 /\ F + I - 2 >= 0 /\ E + I - 1 >= 0 /\ D + I - 2 >= 0 /\ C + I - 1 >= 0 /\ B + I - 1 >= 0 /\ -B + I >= 0 /\ P + I - 2 >= 0 /\ -P + I + 2 >= 0 /\ M + I - 2 >= 0 /\ -M + I >= 0 /\ J + I - 1 >= 0 /\ -J + I >= 0 /\ -A + I >= 0 /\ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H >= 0 /\ C - H + 1 >= 0 /\ B - H + 1 >= 0 /\ -B - H + 2 >= 0 /\ P - H >= 0 /\ -P - H + 4 >= 0 /\ M - H >= 0 /\ -M - H + 2 >= 0 /\ J - H + 1 >= 0 /\ -J - H + 2 >= 0 /\ A - H >= 0 /\ -A - H + 2 >= 0 /\ G + H - 1 >= 0 /\ D + H - 2 >= 0 /\ -A + H >= 0 /\ D - G - 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G - 1 >= 0 /\ C + G >= 0 /\ B + G >= 0 /\ -B + G + 1 >= 0 /\ P + G - 1 >= 0 /\ -P + G + 3 >= 0 /\ M + G - 1 >= 0 /\ -M + G + 1 >= 0 /\ J + G >= 0 /\ -J + G + 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ D - F + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 2 >= 0 /\ C + F - 1 >= 0 /\ B + F - 1 >= 0 /\ -B + F >= 0 /\ P + F - 2 >= 0 /\ -P + F + 2 >= 0 /\ M + F - 2 >= 0 /\ -M + F >= 0 /\ J + F - 1 >= 0 /\ -J + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E - 1 >= 0 /\ C + E >= 0 /\ B + E >= 0 /\ -B + E + 1 >= 0 /\ P + E - 1 >= 0 /\ -P + E + 3 >= 0 /\ M + E - 1 >= 0 /\ -M + E + 1 >= 0 /\ J + E >= 0 /\ -J + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ D - 1 >= 0 /\ C + D - 1 >= 0 /\ B + D - 2 >= 0 /\ -B + D >= 0 /\ P + D - 3 >= 0 /\ -P + D + 2 >= 0 /\ M + D - 2 >= 0 /\ -M + D >= 0 /\ J + D - 2 >= 0 /\ -J + D >= 0 /\ A + D - 2 >= 0 /\ -A + D >= 0 /\ C >= 0 /\ B + C >= 0 /\ -B + C + 1 >= 0 /\ P + C - 1 >= 0 /\ -P + C + 3 >= 0 /\ M + C - 1 >= 0 /\ -M + C + 1 >= 0 /\ J + C >= 0 /\ -J + C + 1 >= 0 /\ -A + C + 1 >= 0 /\ -B + 1 >= 0 /\ P - B - 1 >= 0 /\ -P - B + 4 >= 0 /\ M - B >= 0 /\ -M - B + 2 >= 0 /\ J - B >= 0 /\ -J - B + 2 >= 0 /\ -A - B + 2 >= 0 /\ B >= 0 /\ P + B - 1 >= 0 /\ -P + B + 2 >= 0 /\ M + B - 1 >= 0 /\ -M + B + 1 >= 0 /\ J + B >= 0 /\ -J + B >= 0 /\ -A + B + 1 >= 0 /\ -P + 3 >= 0 /\ M - P + 2 >= 0 /\ -M - P + 4 >= 0 /\ J - P + 2 >= 0 /\ -J - P + 4 >= 0 /\ -A - P + 4 >= 0 /\ P - 1 >= 0 /\ M + P - 2 >= 0 /\ -M + P >= 0 /\ J + P - 1 >= 0 /\ -J + P - 1 >= 0 /\ -A + P >= 0 /\ N - O >= 0 /\ L - O >= 0 /\ K - O >= 0 /\ -N + O >= 0 /\ -L + O >= 0 /\ -K + O >= 0 /\ L - N >= 0 /\ K - N >= 0 /\ -L + N >= 0 /\ -K + N >= 0 /\ -M + 1 >= 0 /\ J - M + 1 >= 0 /\ -J - M + 2 >= 0 /\ -A - M + 2 >= 0 /\ M - 1 >= 0 /\ J + M - 1 >= 0 /\ -J + M >= 0 /\ -A + M >= 0 /\ K - L >= 0 /\ -K + L >= 0 /\ -J + 1 >= 0 /\ -A - J + 2 >= 0 /\ J >= 0 /\ -A + J + 1 >= 0 /\ -A + 1 >= 0 /\ Q >= 0 /\ 0 >= O /\ 1 >= Q ] f59(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f63(A, B, C, D, E + 1, F, G, H, I, J, K, L, M, N, O, P, Q)) [ -I + 1 >= 0 /\ -H - I + 2 >= 0 /\ G - I + 1 >= 0 /\ F - I >= 0 /\ E - I + 1 >= 0 /\ D - I >= 0 /\ C - I + 1 >= 0 /\ B - I + 1 >= 0 /\ -B - I + 2 >= 0 /\ Q - I + 1 >= 0 /\ -Q - I + 2 >= 0 /\ M - I >= 0 /\ -M - I + 2 >= 0 /\ J - I + 1 >= 0 /\ -J - I + 2 >= 0 /\ -A - I + 2 >= 0 /\ I - 1 >= 0 /\ -H + I >= 0 /\ G + I - 1 >= 0 /\ F + I - 2 >= 0 /\ E + I - 1 >= 0 /\ D + I - 2 >= 0 /\ C + I - 1 >= 0 /\ B + I - 1 >= 0 /\ -B + I >= 0 /\ Q + I - 1 >= 0 /\ -Q + I >= 0 /\ M + I - 2 >= 0 /\ -M + I >= 0 /\ J + I - 1 >= 0 /\ -J + I >= 0 /\ -A + I >= 0 /\ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H >= 0 /\ C - H + 1 >= 0 /\ B - H + 1 >= 0 /\ -B - H + 2 >= 0 /\ Q - H + 1 >= 0 /\ -Q - H + 2 >= 0 /\ M - H >= 0 /\ -M - H + 2 >= 0 /\ J - H + 1 >= 0 /\ -J - H + 2 >= 0 /\ A - H >= 0 /\ -A - H + 2 >= 0 /\ G + H - 1 >= 0 /\ D + H - 2 >= 0 /\ -A + H >= 0 /\ D - G - 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G - 1 >= 0 /\ C + G >= 0 /\ B + G >= 0 /\ -B + G + 1 >= 0 /\ Q + G >= 0 /\ -Q + G + 1 >= 0 /\ M + G - 1 >= 0 /\ -M + G + 1 >= 0 /\ J + G >= 0 /\ -J + G + 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ D - F + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 2 >= 0 /\ C + F - 1 >= 0 /\ B + F - 1 >= 0 /\ -B + F >= 0 /\ Q + F - 1 >= 0 /\ -Q + F >= 0 /\ M + F - 2 >= 0 /\ -M + F >= 0 /\ J + F - 1 >= 0 /\ -J + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E - 1 >= 0 /\ C + E >= 0 /\ B + E >= 0 /\ -B + E + 1 >= 0 /\ Q + E >= 0 /\ -Q + E + 1 >= 0 /\ M + E - 1 >= 0 /\ -M + E + 1 >= 0 /\ J + E >= 0 /\ -J + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ D - 1 >= 0 /\ C + D - 1 >= 0 /\ B + D - 2 >= 0 /\ -B + D >= 0 /\ Q + D - 1 >= 0 /\ -Q + D >= 0 /\ M + D - 2 >= 0 /\ -M + D >= 0 /\ J + D - 2 >= 0 /\ -J + D >= 0 /\ A + D - 2 >= 0 /\ -A + D >= 0 /\ C >= 0 /\ B + C >= 0 /\ -B + C + 1 >= 0 /\ Q + C >= 0 /\ -Q + C + 1 >= 0 /\ M + C - 1 >= 0 /\ -M + C + 1 >= 0 /\ J + C >= 0 /\ -J + C + 1 >= 0 /\ -A + C + 1 >= 0 /\ -B + 1 >= 0 /\ Q - B + 1 >= 0 /\ -Q - B + 2 >= 0 /\ M - B >= 0 /\ -M - B + 2 >= 0 /\ J - B >= 0 /\ -J - B + 2 >= 0 /\ -A - B + 2 >= 0 /\ B >= 0 /\ Q + B >= 0 /\ -Q + B + 1 >= 0 /\ M + B - 1 >= 0 /\ -M + B + 1 >= 0 /\ J + B >= 0 /\ -J + B >= 0 /\ -A + B + 1 >= 0 /\ -Q + 1 >= 0 /\ M - Q >= 0 /\ -M - Q + 2 >= 0 /\ J - Q + 1 >= 0 /\ -J - Q + 2 >= 0 /\ -A - Q + 2 >= 0 /\ Q >= 0 /\ M + Q - 1 >= 0 /\ -M + Q + 1 >= 0 /\ J + Q >= 0 /\ -J + Q + 1 >= 0 /\ -A + Q + 1 >= 0 /\ L - N >= 0 /\ K - N >= 0 /\ -L + N >= 0 /\ -K + N >= 0 /\ -M + 1 >= 0 /\ J - M + 1 >= 0 /\ -J - M + 2 >= 0 /\ -A - M + 2 >= 0 /\ M - 1 >= 0 /\ J + M - 1 >= 0 /\ -J + M >= 0 /\ -A + M >= 0 /\ K - L >= 0 /\ -K + L >= 0 /\ -J + 1 >= 0 /\ -A - J + 2 >= 0 /\ J >= 0 /\ -A + J + 1 >= 0 /\ -A + 1 >= 0 /\ Q >= 1 /\ 0 >= C /\ 0 >= E ] f59(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f63(A, B, C, D, E + 1, F, G, H, I, J, K, L, M, N, O, P, Q)) [ -I + 1 >= 0 /\ -H - I + 2 >= 0 /\ G - I + 1 >= 0 /\ F - I >= 0 /\ E - I + 1 >= 0 /\ D - I >= 0 /\ C - I + 1 >= 0 /\ B - I + 1 >= 0 /\ -B - I + 2 >= 0 /\ Q - I + 1 >= 0 /\ -Q - I + 2 >= 0 /\ M - I >= 0 /\ -M - I + 2 >= 0 /\ J - I + 1 >= 0 /\ -J - I + 2 >= 0 /\ -A - I + 2 >= 0 /\ I - 1 >= 0 /\ -H + I >= 0 /\ G + I - 1 >= 0 /\ F + I - 2 >= 0 /\ E + I - 1 >= 0 /\ D + I - 2 >= 0 /\ C + I - 1 >= 0 /\ B + I - 1 >= 0 /\ -B + I >= 0 /\ Q + I - 1 >= 0 /\ -Q + I >= 0 /\ M + I - 2 >= 0 /\ -M + I >= 0 /\ J + I - 1 >= 0 /\ -J + I >= 0 /\ -A + I >= 0 /\ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H >= 0 /\ C - H + 1 >= 0 /\ B - H + 1 >= 0 /\ -B - H + 2 >= 0 /\ Q - H + 1 >= 0 /\ -Q - H + 2 >= 0 /\ M - H >= 0 /\ -M - H + 2 >= 0 /\ J - H + 1 >= 0 /\ -J - H + 2 >= 0 /\ A - H >= 0 /\ -A - H + 2 >= 0 /\ G + H - 1 >= 0 /\ D + H - 2 >= 0 /\ -A + H >= 0 /\ D - G - 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G - 1 >= 0 /\ C + G >= 0 /\ B + G >= 0 /\ -B + G + 1 >= 0 /\ Q + G >= 0 /\ -Q + G + 1 >= 0 /\ M + G - 1 >= 0 /\ -M + G + 1 >= 0 /\ J + G >= 0 /\ -J + G + 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ D - F + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 2 >= 0 /\ C + F - 1 >= 0 /\ B + F - 1 >= 0 /\ -B + F >= 0 /\ Q + F - 1 >= 0 /\ -Q + F >= 0 /\ M + F - 2 >= 0 /\ -M + F >= 0 /\ J + F - 1 >= 0 /\ -J + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E - 1 >= 0 /\ C + E >= 0 /\ B + E >= 0 /\ -B + E + 1 >= 0 /\ Q + E >= 0 /\ -Q + E + 1 >= 0 /\ M + E - 1 >= 0 /\ -M + E + 1 >= 0 /\ J + E >= 0 /\ -J + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ D - 1 >= 0 /\ C + D - 1 >= 0 /\ B + D - 2 >= 0 /\ -B + D >= 0 /\ Q + D - 1 >= 0 /\ -Q + D >= 0 /\ M + D - 2 >= 0 /\ -M + D >= 0 /\ J + D - 2 >= 0 /\ -J + D >= 0 /\ A + D - 2 >= 0 /\ -A + D >= 0 /\ C >= 0 /\ B + C >= 0 /\ -B + C + 1 >= 0 /\ Q + C >= 0 /\ -Q + C + 1 >= 0 /\ M + C - 1 >= 0 /\ -M + C + 1 >= 0 /\ J + C >= 0 /\ -J + C + 1 >= 0 /\ -A + C + 1 >= 0 /\ -B + 1 >= 0 /\ Q - B + 1 >= 0 /\ -Q - B + 2 >= 0 /\ M - B >= 0 /\ -M - B + 2 >= 0 /\ J - B >= 0 /\ -J - B + 2 >= 0 /\ -A - B + 2 >= 0 /\ B >= 0 /\ Q + B >= 0 /\ -Q + B + 1 >= 0 /\ M + B - 1 >= 0 /\ -M + B + 1 >= 0 /\ J + B >= 0 /\ -J + B >= 0 /\ -A + B + 1 >= 0 /\ -Q + 1 >= 0 /\ M - Q >= 0 /\ -M - Q + 2 >= 0 /\ J - Q + 1 >= 0 /\ -J - Q + 2 >= 0 /\ -A - Q + 2 >= 0 /\ Q >= 0 /\ M + Q - 1 >= 0 /\ -M + Q + 1 >= 0 /\ J + Q >= 0 /\ -J + Q + 1 >= 0 /\ -A + Q + 1 >= 0 /\ L - N >= 0 /\ K - N >= 0 /\ -L + N >= 0 /\ -K + N >= 0 /\ -M + 1 >= 0 /\ J - M + 1 >= 0 /\ -J - M + 2 >= 0 /\ -A - M + 2 >= 0 /\ M - 1 >= 0 /\ J + M - 1 >= 0 /\ -J + M >= 0 /\ -A + M >= 0 /\ K - L >= 0 /\ -K + L >= 0 /\ -J + 1 >= 0 /\ -A - J + 2 >= 0 /\ J >= 0 /\ -A + J + 1 >= 0 /\ -A + 1 >= 0 /\ Q >= 1 /\ 0 >= C /\ E = 1 ] f59(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f63(A, B, C, D, 0, F + 1, G, H, I, J, K, L, M, N, O, P, Q)) [ -I + 1 >= 0 /\ -H - I + 2 >= 0 /\ G - I + 1 >= 0 /\ F - I >= 0 /\ E - I + 1 >= 0 /\ D - I >= 0 /\ C - I + 1 >= 0 /\ B - I + 1 >= 0 /\ -B - I + 2 >= 0 /\ Q - I + 1 >= 0 /\ -Q - I + 2 >= 0 /\ M - I >= 0 /\ -M - I + 2 >= 0 /\ J - I + 1 >= 0 /\ -J - I + 2 >= 0 /\ -A - I + 2 >= 0 /\ I - 1 >= 0 /\ -H + I >= 0 /\ G + I - 1 >= 0 /\ F + I - 2 >= 0 /\ E + I - 1 >= 0 /\ D + I - 2 >= 0 /\ C + I - 1 >= 0 /\ B + I - 1 >= 0 /\ -B + I >= 0 /\ Q + I - 1 >= 0 /\ -Q + I >= 0 /\ M + I - 2 >= 0 /\ -M + I >= 0 /\ J + I - 1 >= 0 /\ -J + I >= 0 /\ -A + I >= 0 /\ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H >= 0 /\ C - H + 1 >= 0 /\ B - H + 1 >= 0 /\ -B - H + 2 >= 0 /\ Q - H + 1 >= 0 /\ -Q - H + 2 >= 0 /\ M - H >= 0 /\ -M - H + 2 >= 0 /\ J - H + 1 >= 0 /\ -J - H + 2 >= 0 /\ A - H >= 0 /\ -A - H + 2 >= 0 /\ G + H - 1 >= 0 /\ D + H - 2 >= 0 /\ -A + H >= 0 /\ D - G - 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G - 1 >= 0 /\ C + G >= 0 /\ B + G >= 0 /\ -B + G + 1 >= 0 /\ Q + G >= 0 /\ -Q + G + 1 >= 0 /\ M + G - 1 >= 0 /\ -M + G + 1 >= 0 /\ J + G >= 0 /\ -J + G + 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ D - F + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 2 >= 0 /\ C + F - 1 >= 0 /\ B + F - 1 >= 0 /\ -B + F >= 0 /\ Q + F - 1 >= 0 /\ -Q + F >= 0 /\ M + F - 2 >= 0 /\ -M + F >= 0 /\ J + F - 1 >= 0 /\ -J + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E - 1 >= 0 /\ C + E >= 0 /\ B + E >= 0 /\ -B + E + 1 >= 0 /\ Q + E >= 0 /\ -Q + E + 1 >= 0 /\ M + E - 1 >= 0 /\ -M + E + 1 >= 0 /\ J + E >= 0 /\ -J + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ D - 1 >= 0 /\ C + D - 1 >= 0 /\ B + D - 2 >= 0 /\ -B + D >= 0 /\ Q + D - 1 >= 0 /\ -Q + D >= 0 /\ M + D - 2 >= 0 /\ -M + D >= 0 /\ J + D - 2 >= 0 /\ -J + D >= 0 /\ A + D - 2 >= 0 /\ -A + D >= 0 /\ C >= 0 /\ B + C >= 0 /\ -B + C + 1 >= 0 /\ Q + C >= 0 /\ -Q + C + 1 >= 0 /\ M + C - 1 >= 0 /\ -M + C + 1 >= 0 /\ J + C >= 0 /\ -J + C + 1 >= 0 /\ -A + C + 1 >= 0 /\ -B + 1 >= 0 /\ Q - B + 1 >= 0 /\ -Q - B + 2 >= 0 /\ M - B >= 0 /\ -M - B + 2 >= 0 /\ J - B >= 0 /\ -J - B + 2 >= 0 /\ -A - B + 2 >= 0 /\ B >= 0 /\ Q + B >= 0 /\ -Q + B + 1 >= 0 /\ M + B - 1 >= 0 /\ -M + B + 1 >= 0 /\ J + B >= 0 /\ -J + B >= 0 /\ -A + B + 1 >= 0 /\ -Q + 1 >= 0 /\ M - Q >= 0 /\ -M - Q + 2 >= 0 /\ J - Q + 1 >= 0 /\ -J - Q + 2 >= 0 /\ -A - Q + 2 >= 0 /\ Q >= 0 /\ M + Q - 1 >= 0 /\ -M + Q + 1 >= 0 /\ J + Q >= 0 /\ -J + Q + 1 >= 0 /\ -A + Q + 1 >= 0 /\ L - N >= 0 /\ K - N >= 0 /\ -L + N >= 0 /\ -K + N >= 0 /\ -M + 1 >= 0 /\ J - M + 1 >= 0 /\ -J - M + 2 >= 0 /\ -A - M + 2 >= 0 /\ M - 1 >= 0 /\ J + M - 1 >= 0 /\ -J + M >= 0 /\ -A + M >= 0 /\ K - L >= 0 /\ -K + L >= 0 /\ -J + 1 >= 0 /\ -A - J + 2 >= 0 /\ J >= 0 /\ -A + J + 1 >= 0 /\ -A + 1 >= 0 /\ E >= 2 /\ C = 0 ] f59(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f63(A, B, C - 1, D, E, F, G, H, I, J, K, L, M, N, O, P, Q)) [ -I + 1 >= 0 /\ -H - I + 2 >= 0 /\ G - I + 1 >= 0 /\ F - I >= 0 /\ E - I + 1 >= 0 /\ D - I >= 0 /\ C - I + 1 >= 0 /\ B - I + 1 >= 0 /\ -B - I + 2 >= 0 /\ Q - I + 1 >= 0 /\ -Q - I + 2 >= 0 /\ M - I >= 0 /\ -M - I + 2 >= 0 /\ J - I + 1 >= 0 /\ -J - I + 2 >= 0 /\ -A - I + 2 >= 0 /\ I - 1 >= 0 /\ -H + I >= 0 /\ G + I - 1 >= 0 /\ F + I - 2 >= 0 /\ E + I - 1 >= 0 /\ D + I - 2 >= 0 /\ C + I - 1 >= 0 /\ B + I - 1 >= 0 /\ -B + I >= 0 /\ Q + I - 1 >= 0 /\ -Q + I >= 0 /\ M + I - 2 >= 0 /\ -M + I >= 0 /\ J + I - 1 >= 0 /\ -J + I >= 0 /\ -A + I >= 0 /\ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H >= 0 /\ C - H + 1 >= 0 /\ B - H + 1 >= 0 /\ -B - H + 2 >= 0 /\ Q - H + 1 >= 0 /\ -Q - H + 2 >= 0 /\ M - H >= 0 /\ -M - H + 2 >= 0 /\ J - H + 1 >= 0 /\ -J - H + 2 >= 0 /\ A - H >= 0 /\ -A - H + 2 >= 0 /\ G + H - 1 >= 0 /\ D + H - 2 >= 0 /\ -A + H >= 0 /\ D - G - 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G - 1 >= 0 /\ C + G >= 0 /\ B + G >= 0 /\ -B + G + 1 >= 0 /\ Q + G >= 0 /\ -Q + G + 1 >= 0 /\ M + G - 1 >= 0 /\ -M + G + 1 >= 0 /\ J + G >= 0 /\ -J + G + 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ D - F + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 2 >= 0 /\ C + F - 1 >= 0 /\ B + F - 1 >= 0 /\ -B + F >= 0 /\ Q + F - 1 >= 0 /\ -Q + F >= 0 /\ M + F - 2 >= 0 /\ -M + F >= 0 /\ J + F - 1 >= 0 /\ -J + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E - 1 >= 0 /\ C + E >= 0 /\ B + E >= 0 /\ -B + E + 1 >= 0 /\ Q + E >= 0 /\ -Q + E + 1 >= 0 /\ M + E - 1 >= 0 /\ -M + E + 1 >= 0 /\ J + E >= 0 /\ -J + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ D - 1 >= 0 /\ C + D - 1 >= 0 /\ B + D - 2 >= 0 /\ -B + D >= 0 /\ Q + D - 1 >= 0 /\ -Q + D >= 0 /\ M + D - 2 >= 0 /\ -M + D >= 0 /\ J + D - 2 >= 0 /\ -J + D >= 0 /\ A + D - 2 >= 0 /\ -A + D >= 0 /\ C >= 0 /\ B + C >= 0 /\ -B + C + 1 >= 0 /\ Q + C >= 0 /\ -Q + C + 1 >= 0 /\ M + C - 1 >= 0 /\ -M + C + 1 >= 0 /\ J + C >= 0 /\ -J + C + 1 >= 0 /\ -A + C + 1 >= 0 /\ -B + 1 >= 0 /\ Q - B + 1 >= 0 /\ -Q - B + 2 >= 0 /\ M - B >= 0 /\ -M - B + 2 >= 0 /\ J - B >= 0 /\ -J - B + 2 >= 0 /\ -A - B + 2 >= 0 /\ B >= 0 /\ Q + B >= 0 /\ -Q + B + 1 >= 0 /\ M + B - 1 >= 0 /\ -M + B + 1 >= 0 /\ J + B >= 0 /\ -J + B >= 0 /\ -A + B + 1 >= 0 /\ -Q + 1 >= 0 /\ M - Q >= 0 /\ -M - Q + 2 >= 0 /\ J - Q + 1 >= 0 /\ -J - Q + 2 >= 0 /\ -A - Q + 2 >= 0 /\ Q >= 0 /\ M + Q - 1 >= 0 /\ -M + Q + 1 >= 0 /\ J + Q >= 0 /\ -J + Q + 1 >= 0 /\ -A + Q + 1 >= 0 /\ L - N >= 0 /\ K - N >= 0 /\ -L + N >= 0 /\ -K + N >= 0 /\ -M + 1 >= 0 /\ J - M + 1 >= 0 /\ -J - M + 2 >= 0 /\ -A - M + 2 >= 0 /\ M - 1 >= 0 /\ J + M - 1 >= 0 /\ -J + M >= 0 /\ -A + M >= 0 /\ K - L >= 0 /\ -K + L >= 0 /\ -J + 1 >= 0 /\ -A - J + 2 >= 0 /\ J >= 0 /\ -A + J + 1 >= 0 /\ -A + 1 >= 0 /\ C >= 1 ] f63(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f23(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q)) [ -I + 1 >= 0 /\ -H - I + 2 >= 0 /\ G - I + 1 >= 0 /\ F - I >= 0 /\ E - I + 1 >= 0 /\ D - I >= 0 /\ C - I + 1 >= 0 /\ B - I + 1 >= 0 /\ -B - I + 2 >= 0 /\ Q - I + 1 >= 0 /\ -Q - I + 2 >= 0 /\ M - I >= 0 /\ -M - I + 2 >= 0 /\ J - I + 1 >= 0 /\ -J - I + 2 >= 0 /\ -A - I + 2 >= 0 /\ I - 1 >= 0 /\ -H + I >= 0 /\ G + I - 1 >= 0 /\ F + I - 2 >= 0 /\ E + I - 1 >= 0 /\ D + I - 2 >= 0 /\ C + I - 1 >= 0 /\ B + I - 1 >= 0 /\ -B + I >= 0 /\ Q + I - 1 >= 0 /\ -Q + I >= 0 /\ M + I - 2 >= 0 /\ -M + I >= 0 /\ J + I - 1 >= 0 /\ -J + I >= 0 /\ -A + I >= 0 /\ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H >= 0 /\ C - H + 1 >= 0 /\ B - H + 1 >= 0 /\ -B - H + 2 >= 0 /\ Q - H + 1 >= 0 /\ -Q - H + 2 >= 0 /\ M - H >= 0 /\ -M - H + 2 >= 0 /\ J - H + 1 >= 0 /\ -J - H + 2 >= 0 /\ A - H >= 0 /\ -A - H + 2 >= 0 /\ G + H - 1 >= 0 /\ D + H - 2 >= 0 /\ -A + H >= 0 /\ D - G - 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G - 1 >= 0 /\ C + G >= 0 /\ B + G >= 0 /\ -B + G + 1 >= 0 /\ Q + G >= 0 /\ -Q + G + 1 >= 0 /\ M + G - 1 >= 0 /\ -M + G + 1 >= 0 /\ J + G >= 0 /\ -J + G + 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ D - F + 2 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 2 >= 0 /\ C + F - 1 >= 0 /\ B + F - 1 >= 0 /\ -B + F >= 0 /\ Q + F - 1 >= 0 /\ -Q + F >= 0 /\ M + F - 2 >= 0 /\ -M + F >= 0 /\ J + F - 1 >= 0 /\ -J + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E - 1 >= 0 /\ C + E >= 0 /\ B + E >= 0 /\ -B + E + 1 >= 0 /\ Q + E >= 0 /\ -Q + E + 1 >= 0 /\ M + E - 1 >= 0 /\ -M + E + 1 >= 0 /\ J + E >= 0 /\ -J + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ D - 1 >= 0 /\ C + D - 1 >= 0 /\ B + D - 2 >= 0 /\ -B + D >= 0 /\ Q + D - 1 >= 0 /\ -Q + D >= 0 /\ M + D - 2 >= 0 /\ -M + D >= 0 /\ J + D - 2 >= 0 /\ -J + D >= 0 /\ A + D - 2 >= 0 /\ -A + D >= 0 /\ C >= 0 /\ B + C >= 0 /\ -B + C + 1 >= 0 /\ Q + C >= 0 /\ -Q + C + 1 >= 0 /\ M + C - 1 >= 0 /\ -M + C + 1 >= 0 /\ J + C >= 0 /\ -J + C + 1 >= 0 /\ -A + C + 1 >= 0 /\ -B + 1 >= 0 /\ Q - B + 1 >= 0 /\ -Q - B + 2 >= 0 /\ M - B >= 0 /\ -M - B + 2 >= 0 /\ J - B >= 0 /\ -J - B + 2 >= 0 /\ -A - B + 2 >= 0 /\ B >= 0 /\ Q + B >= 0 /\ -Q + B + 1 >= 0 /\ M + B - 1 >= 0 /\ -M + B + 1 >= 0 /\ J + B >= 0 /\ -J + B >= 0 /\ -A + B + 1 >= 0 /\ -Q + 1 >= 0 /\ M - Q >= 0 /\ -M - Q + 2 >= 0 /\ J - Q + 1 >= 0 /\ -J - Q + 2 >= 0 /\ -A - Q + 2 >= 0 /\ Q >= 0 /\ M + Q - 1 >= 0 /\ -M + Q + 1 >= 0 /\ J + Q >= 0 /\ -J + Q + 1 >= 0 /\ -A + Q + 1 >= 0 /\ L - N >= 0 /\ K - N >= 0 /\ -L + N >= 0 /\ -K + N >= 0 /\ -M + 1 >= 0 /\ J - M + 1 >= 0 /\ -J - M + 2 >= 0 /\ -A - M + 2 >= 0 /\ M - 1 >= 0 /\ J + M - 1 >= 0 /\ -J + M >= 0 /\ -A + M >= 0 /\ K - L >= 0 /\ -K + L >= 0 /\ -J + 1 >= 0 /\ -A - J + 2 >= 0 /\ J >= 0 /\ -A + J + 1 >= 0 /\ -A + 1 >= 0 /\ I >= 0 /\ 1 >= I /\ 0 >= Q /\ D >= F ] f27(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f23(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q)) [ -I + 1 >= 0 /\ -H - I + 2 >= 0 /\ G - I + 1 >= 0 /\ F - I >= 0 /\ E - I + 1 >= 0 /\ D - I >= 0 /\ C - I + 1 >= 0 /\ J - I + 1 >= 0 /\ -J - I + 2 >= 0 /\ I >= 0 /\ -H + I + 1 >= 0 /\ G + I >= 0 /\ F + I - 1 >= 0 /\ E + I >= 0 /\ D + I - 1 >= 0 /\ C + I >= 0 /\ J + I >= 0 /\ -J + I + 1 >= 0 /\ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H >= 0 /\ C - H + 1 >= 0 /\ J - H + 1 >= 0 /\ -J - H + 2 >= 0 /\ G + H - 1 >= 0 /\ D + H - 2 >= 0 /\ D - G - 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G - 1 >= 0 /\ C + G >= 0 /\ J + G >= 0 /\ -J + G + 1 >= 0 /\ D - F + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 2 >= 0 /\ C + F - 1 >= 0 /\ J + F - 1 >= 0 /\ -J + F >= 0 /\ E >= 0 /\ D + E - 1 >= 0 /\ C + E >= 0 /\ J + E >= 0 /\ -J + E + 1 >= 0 /\ D - 1 >= 0 /\ C + D - 1 >= 0 /\ J + D - 2 >= 0 /\ -J + D >= 0 /\ C >= 0 /\ J + C >= 0 /\ -J + C + 1 >= 0 /\ K - L >= 0 /\ -K + L >= 0 /\ -J + 1 >= 0 /\ J >= 0 /\ D >= F /\ I = 0 ] f63(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f10(A, B, C, D, E, F, G + 1, H, I, J, K, 0, M, N, O, P, 1)) [ -I + 1 >= 0 /\ -H - I + 2 >= 0 /\ G - I + 1 >= 0 /\ F - I >= 0 /\ E - I + 1 >= 0 /\ D - I >= 0 /\ C - I + 1 >= 0 /\ B - I + 1 >= 0 /\ -B - I + 2 >= 0 /\ Q - I + 1 >= 0 /\ -Q - I + 2 >= 0 /\ M - I >= 0 /\ -M - I + 2 >= 0 /\ J - I + 1 >= 0 /\ -J - I + 2 >= 0 /\ -A - I + 2 >= 0 /\ I - 1 >= 0 /\ -H + I >= 0 /\ G + I - 1 >= 0 /\ F + I - 2 >= 0 /\ E + I - 1 >= 0 /\ D + I - 2 >= 0 /\ C + I - 1 >= 0 /\ B + I - 1 >= 0 /\ -B + I >= 0 /\ Q + I - 1 >= 0 /\ -Q + I >= 0 /\ M + I - 2 >= 0 /\ -M + I >= 0 /\ J + I - 1 >= 0 /\ -J + I >= 0 /\ -A + I >= 0 /\ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H >= 0 /\ C - H + 1 >= 0 /\ B - H + 1 >= 0 /\ -B - H + 2 >= 0 /\ Q - H + 1 >= 0 /\ -Q - H + 2 >= 0 /\ M - H >= 0 /\ -M - H + 2 >= 0 /\ J - H + 1 >= 0 /\ -J - H + 2 >= 0 /\ A - H >= 0 /\ -A - H + 2 >= 0 /\ G + H - 1 >= 0 /\ D + H - 2 >= 0 /\ -A + H >= 0 /\ D - G - 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G - 1 >= 0 /\ C + G >= 0 /\ B + G >= 0 /\ -B + G + 1 >= 0 /\ Q + G >= 0 /\ -Q + G + 1 >= 0 /\ M + G - 1 >= 0 /\ -M + G + 1 >= 0 /\ J + G >= 0 /\ -J + G + 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ D - F + 2 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 2 >= 0 /\ C + F - 1 >= 0 /\ B + F - 1 >= 0 /\ -B + F >= 0 /\ Q + F - 1 >= 0 /\ -Q + F >= 0 /\ M + F - 2 >= 0 /\ -M + F >= 0 /\ J + F - 1 >= 0 /\ -J + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E - 1 >= 0 /\ C + E >= 0 /\ B + E >= 0 /\ -B + E + 1 >= 0 /\ Q + E >= 0 /\ -Q + E + 1 >= 0 /\ M + E - 1 >= 0 /\ -M + E + 1 >= 0 /\ J + E >= 0 /\ -J + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ D - 1 >= 0 /\ C + D - 1 >= 0 /\ B + D - 2 >= 0 /\ -B + D >= 0 /\ Q + D - 1 >= 0 /\ -Q + D >= 0 /\ M + D - 2 >= 0 /\ -M + D >= 0 /\ J + D - 2 >= 0 /\ -J + D >= 0 /\ A + D - 2 >= 0 /\ -A + D >= 0 /\ C >= 0 /\ B + C >= 0 /\ -B + C + 1 >= 0 /\ Q + C >= 0 /\ -Q + C + 1 >= 0 /\ M + C - 1 >= 0 /\ -M + C + 1 >= 0 /\ J + C >= 0 /\ -J + C + 1 >= 0 /\ -A + C + 1 >= 0 /\ -B + 1 >= 0 /\ Q - B + 1 >= 0 /\ -Q - B + 2 >= 0 /\ M - B >= 0 /\ -M - B + 2 >= 0 /\ J - B >= 0 /\ -J - B + 2 >= 0 /\ -A - B + 2 >= 0 /\ B >= 0 /\ Q + B >= 0 /\ -Q + B + 1 >= 0 /\ M + B - 1 >= 0 /\ -M + B + 1 >= 0 /\ J + B >= 0 /\ -J + B >= 0 /\ -A + B + 1 >= 0 /\ -Q + 1 >= 0 /\ M - Q >= 0 /\ -M - Q + 2 >= 0 /\ J - Q + 1 >= 0 /\ -J - Q + 2 >= 0 /\ -A - Q + 2 >= 0 /\ Q >= 0 /\ M + Q - 1 >= 0 /\ -M + Q + 1 >= 0 /\ J + Q >= 0 /\ -J + Q + 1 >= 0 /\ -A + Q + 1 >= 0 /\ L - N >= 0 /\ K - N >= 0 /\ -L + N >= 0 /\ -K + N >= 0 /\ -M + 1 >= 0 /\ J - M + 1 >= 0 /\ -J - M + 2 >= 0 /\ -A - M + 2 >= 0 /\ M - 1 >= 0 /\ J + M - 1 >= 0 /\ -J + M >= 0 /\ -A + M >= 0 /\ K - L >= 0 /\ -K + L >= 0 /\ -J + 1 >= 0 /\ -A - J + 2 >= 0 /\ J >= 0 /\ -A + J + 1 >= 0 /\ -A + 1 >= 0 /\ L >= 1 /\ D >= F /\ Q = 1 ] f63(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f10(A, B, C, D, E, F, G + 1, H, I, J, K, 1, M, N, O, P, 1)) [ -I + 1 >= 0 /\ -H - I + 2 >= 0 /\ G - I + 1 >= 0 /\ F - I >= 0 /\ E - I + 1 >= 0 /\ D - I >= 0 /\ C - I + 1 >= 0 /\ B - I + 1 >= 0 /\ -B - I + 2 >= 0 /\ Q - I + 1 >= 0 /\ -Q - I + 2 >= 0 /\ M - I >= 0 /\ -M - I + 2 >= 0 /\ J - I + 1 >= 0 /\ -J - I + 2 >= 0 /\ -A - I + 2 >= 0 /\ I - 1 >= 0 /\ -H + I >= 0 /\ G + I - 1 >= 0 /\ F + I - 2 >= 0 /\ E + I - 1 >= 0 /\ D + I - 2 >= 0 /\ C + I - 1 >= 0 /\ B + I - 1 >= 0 /\ -B + I >= 0 /\ Q + I - 1 >= 0 /\ -Q + I >= 0 /\ M + I - 2 >= 0 /\ -M + I >= 0 /\ J + I - 1 >= 0 /\ -J + I >= 0 /\ -A + I >= 0 /\ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H >= 0 /\ C - H + 1 >= 0 /\ B - H + 1 >= 0 /\ -B - H + 2 >= 0 /\ Q - H + 1 >= 0 /\ -Q - H + 2 >= 0 /\ M - H >= 0 /\ -M - H + 2 >= 0 /\ J - H + 1 >= 0 /\ -J - H + 2 >= 0 /\ A - H >= 0 /\ -A - H + 2 >= 0 /\ G + H - 1 >= 0 /\ D + H - 2 >= 0 /\ -A + H >= 0 /\ D - G - 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G - 1 >= 0 /\ C + G >= 0 /\ B + G >= 0 /\ -B + G + 1 >= 0 /\ Q + G >= 0 /\ -Q + G + 1 >= 0 /\ M + G - 1 >= 0 /\ -M + G + 1 >= 0 /\ J + G >= 0 /\ -J + G + 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ D - F + 2 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 2 >= 0 /\ C + F - 1 >= 0 /\ B + F - 1 >= 0 /\ -B + F >= 0 /\ Q + F - 1 >= 0 /\ -Q + F >= 0 /\ M + F - 2 >= 0 /\ -M + F >= 0 /\ J + F - 1 >= 0 /\ -J + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E - 1 >= 0 /\ C + E >= 0 /\ B + E >= 0 /\ -B + E + 1 >= 0 /\ Q + E >= 0 /\ -Q + E + 1 >= 0 /\ M + E - 1 >= 0 /\ -M + E + 1 >= 0 /\ J + E >= 0 /\ -J + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ D - 1 >= 0 /\ C + D - 1 >= 0 /\ B + D - 2 >= 0 /\ -B + D >= 0 /\ Q + D - 1 >= 0 /\ -Q + D >= 0 /\ M + D - 2 >= 0 /\ -M + D >= 0 /\ J + D - 2 >= 0 /\ -J + D >= 0 /\ A + D - 2 >= 0 /\ -A + D >= 0 /\ C >= 0 /\ B + C >= 0 /\ -B + C + 1 >= 0 /\ Q + C >= 0 /\ -Q + C + 1 >= 0 /\ M + C - 1 >= 0 /\ -M + C + 1 >= 0 /\ J + C >= 0 /\ -J + C + 1 >= 0 /\ -A + C + 1 >= 0 /\ -B + 1 >= 0 /\ Q - B + 1 >= 0 /\ -Q - B + 2 >= 0 /\ M - B >= 0 /\ -M - B + 2 >= 0 /\ J - B >= 0 /\ -J - B + 2 >= 0 /\ -A - B + 2 >= 0 /\ B >= 0 /\ Q + B >= 0 /\ -Q + B + 1 >= 0 /\ M + B - 1 >= 0 /\ -M + B + 1 >= 0 /\ J + B >= 0 /\ -J + B >= 0 /\ -A + B + 1 >= 0 /\ -Q + 1 >= 0 /\ M - Q >= 0 /\ -M - Q + 2 >= 0 /\ J - Q + 1 >= 0 /\ -J - Q + 2 >= 0 /\ -A - Q + 2 >= 0 /\ Q >= 0 /\ M + Q - 1 >= 0 /\ -M + Q + 1 >= 0 /\ J + Q >= 0 /\ -J + Q + 1 >= 0 /\ -A + Q + 1 >= 0 /\ L - N >= 0 /\ K - N >= 0 /\ -L + N >= 0 /\ -K + N >= 0 /\ -M + 1 >= 0 /\ J - M + 1 >= 0 /\ -J - M + 2 >= 0 /\ -A - M + 2 >= 0 /\ M - 1 >= 0 /\ J + M - 1 >= 0 /\ -J + M >= 0 /\ -A + M >= 0 /\ K - L >= 0 /\ -K + L >= 0 /\ -J + 1 >= 0 /\ -A - J + 2 >= 0 /\ J >= 0 /\ -A + J + 1 >= 0 /\ -A + 1 >= 0 /\ 0 >= L /\ D >= F /\ Q = 1 ] f10(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f1(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q)) [ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G - 1 >= 0 /\ C + G >= 0 /\ D - F >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 2 >= 0 /\ C + F - 1 >= 0 /\ E >= 0 /\ D + E - 1 >= 0 /\ C + E >= 0 /\ D - 1 >= 0 /\ C + D - 1 >= 0 /\ C >= 0 /\ G >= D ] )