(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS f0)) (VAR A B C D E F G H I J K L M N O P Q) (RULES f47(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f51(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 + 1 >= 0 /\ C - I >= 0 /\ B - I >= 0 /\ -B - I + 2 >= 0 /\ M - I >= 0 /\ -M - I + 2 >= 0 /\ L - I >= 0 /\ -L - I + 2 >= 0 /\ -A - I + 2 >= 0 /\ I >= 0 /\ -H + I >= 0 /\ G + I - 1 >= 0 /\ F + I - 1 >= 0 /\ E + I >= 0 /\ D + I >= 0 /\ C + I - 2 >= 0 /\ B + I >= 0 /\ -B + I >= 0 /\ M + I - 1 >= 0 /\ -M + I + 1 >= 0 /\ L + I - 1 >= 0 /\ -L + I + 1 >= 0 /\ -A + I >= 0 /\ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H + 1 >= 0 /\ C - H >= 0 /\ B - H >= 0 /\ -B - H + 2 >= 0 /\ M - H >= 0 /\ -M - H + 2 >= 0 /\ L - H >= 0 /\ -L - H + 2 >= 0 /\ A - H >= 0 /\ -A - H + 2 >= 0 /\ G + H - 1 >= 0 /\ C + H - 2 >= 0 /\ -A + H >= 0 /\ C - G - 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G >= 0 /\ C + G - 1 >= 0 /\ B + G - 1 >= 0 /\ -B + G + 1 >= 0 /\ M + G - 1 >= 0 /\ -M + G + 1 >= 0 /\ L + G - 1 >= 0 /\ -L + G + 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ C - F + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F - 2 >= 0 /\ B + F - 1 >= 0 /\ -B + F >= 0 /\ M + F - 2 >= 0 /\ -M + F >= 0 /\ L + F - 2 >= 0 /\ -L + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ B + E >= 0 /\ -B + E + 1 >= 0 /\ M + E - 1 >= 0 /\ -M + E + 1 >= 0 /\ L + E - 1 >= 0 /\ -L + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ B + D >= 0 /\ -B + D + 1 >= 0 /\ M + D - 1 >= 0 /\ -M + D + 1 >= 0 /\ L + D - 1 >= 0 /\ -L + D + 1 >= 0 /\ -A + D + 1 >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ -B + C >= 0 /\ M + C - 2 >= 0 /\ -M + C >= 0 /\ L + C - 2 >= 0 /\ -L + C >= 0 /\ A + C - 2 >= 0 /\ -A + C >= 0 /\ -B + 1 >= 0 /\ M - B >= 0 /\ -M - B + 2 >= 0 /\ L - B >= 0 /\ -L - B + 2 >= 0 /\ -A - B + 2 >= 0 /\ B >= 0 /\ M + B - 1 >= 0 /\ -M + B + 1 >= 0 /\ L + B - 1 >= 0 /\ -L + B + 1 >= 0 /\ -A + B >= 0 /\ N - O >= 0 /\ K - O >= 0 /\ J - O >= 0 /\ -N + O >= 0 /\ -K + O >= 0 /\ -J + O >= 0 /\ K - N >= 0 /\ J - N >= 0 /\ -K + N >= 0 /\ -J + N >= 0 /\ -M + 1 >= 0 /\ L - M >= 0 /\ -L - M + 2 >= 0 /\ -A - M + 2 >= 0 /\ M - 1 >= 0 /\ L + M - 2 >= 0 /\ -L + M >= 0 /\ -A + M >= 0 /\ -L + 1 >= 0 /\ -A - L + 2 >= 0 /\ L - 1 >= 0 /\ -A + L >= 0 /\ J - K >= 0 /\ -J + K >= 0 /\ -A + 1 >= 0 /\ A >= 1 ] f0(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f10(A, B, R, S, 0, 1, 0, H, I, J, K, L, M, N, O, P, Q)) [ R >= 1 /\ S >= 0 ] 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 >= 0 /\ C + G - 1 >= 0 /\ C - F >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F - 2 >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ C - 1 >= 0 /\ C >= 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 >= 0 /\ C + G - 1 >= 0 /\ C - F >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F - 2 >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ C - 1 >= 0 /\ C >= G + 1 /\ G >= 1 ] f14(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f22(A, B, C, D, E, F, G, H, 1, K, K, R, M, N, O, P, Q)) [ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H + 1 >= 0 /\ C - H >= 0 /\ H >= 0 /\ G + H - 1 >= 0 /\ F + H - 1 >= 0 /\ E + H >= 0 /\ D + H >= 0 /\ C + H - 2 >= 0 /\ C - G - 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G >= 0 /\ C + G - 1 >= 0 /\ C - F >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F - 2 >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ C - 1 >= 0 /\ G + 1 >= C /\ 1 >= R /\ R >= 0 ] f14(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f22(A, B, C, D, E, F, G, H, 0, K, K, R, M, N, O, P, Q)) [ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H + 1 >= 0 /\ C - H >= 0 /\ H >= 0 /\ G + H - 1 >= 0 /\ F + H - 1 >= 0 /\ E + H >= 0 /\ D + H >= 0 /\ C + H - 2 >= 0 /\ C - G - 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G >= 0 /\ C + G - 1 >= 0 /\ C - F >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F - 2 >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ C - 1 >= 0 /\ C >= G + 2 /\ 1 >= R /\ R >= 0 ] f22(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f26(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 + 1 >= 0 /\ C - I >= 0 /\ L - I + 1 >= 0 /\ -L - I + 2 >= 0 /\ I >= 0 /\ -H + I + 1 >= 0 /\ G + I >= 0 /\ F + I - 1 >= 0 /\ E + I >= 0 /\ D + I >= 0 /\ C + I - 2 >= 0 /\ L + I >= 0 /\ -L + I + 1 >= 0 /\ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H + 1 >= 0 /\ C - H >= 0 /\ L - H + 1 >= 0 /\ -L - H + 2 >= 0 /\ G + H - 1 >= 0 /\ C + H - 2 >= 0 /\ C - G - 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G >= 0 /\ C + G - 1 >= 0 /\ L + G >= 0 /\ -L + G + 1 >= 0 /\ C - F >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F - 2 >= 0 /\ L + F - 1 >= 0 /\ -L + F >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ L + E >= 0 /\ -L + E + 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ L + D >= 0 /\ -L + D + 1 >= 0 /\ C - 1 >= 0 /\ L + C - 1 >= 0 /\ -L + C >= 0 /\ -L + 1 >= 0 /\ L >= 0 /\ J - K >= 0 /\ -J + K >= 0 /\ L >= 1 /\ 0 >= D /\ 0 >= E ] f22(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f26(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 + 1 >= 0 /\ C - I >= 0 /\ L - I + 1 >= 0 /\ -L - I + 2 >= 0 /\ I >= 0 /\ -H + I + 1 >= 0 /\ G + I >= 0 /\ F + I - 1 >= 0 /\ E + I >= 0 /\ D + I >= 0 /\ C + I - 2 >= 0 /\ L + I >= 0 /\ -L + I + 1 >= 0 /\ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H + 1 >= 0 /\ C - H >= 0 /\ L - H + 1 >= 0 /\ -L - H + 2 >= 0 /\ G + H - 1 >= 0 /\ C + H - 2 >= 0 /\ C - G - 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G >= 0 /\ C + G - 1 >= 0 /\ L + G >= 0 /\ -L + G + 1 >= 0 /\ C - F >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F - 2 >= 0 /\ L + F - 1 >= 0 /\ -L + F >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ L + E >= 0 /\ -L + E + 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ L + D >= 0 /\ -L + D + 1 >= 0 /\ C - 1 >= 0 /\ L + C - 1 >= 0 /\ -L + C >= 0 /\ -L + 1 >= 0 /\ L >= 0 /\ J - K >= 0 /\ -J + K >= 0 /\ L >= 1 /\ 0 >= D /\ E = 1 ] f22(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f26(A, B, C, R, 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 + 1 >= 0 /\ C - I >= 0 /\ L - I + 1 >= 0 /\ -L - I + 2 >= 0 /\ I >= 0 /\ -H + I + 1 >= 0 /\ G + I >= 0 /\ F + I - 1 >= 0 /\ E + I >= 0 /\ D + I >= 0 /\ C + I - 2 >= 0 /\ L + I >= 0 /\ -L + I + 1 >= 0 /\ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H + 1 >= 0 /\ C - H >= 0 /\ L - H + 1 >= 0 /\ -L - H + 2 >= 0 /\ G + H - 1 >= 0 /\ C + H - 2 >= 0 /\ C - G - 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G >= 0 /\ C + G - 1 >= 0 /\ L + G >= 0 /\ -L + G + 1 >= 0 /\ C - F >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F - 2 >= 0 /\ L + F - 1 >= 0 /\ -L + F >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ L + E >= 0 /\ -L + E + 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ L + D >= 0 /\ -L + D + 1 >= 0 /\ C - 1 >= 0 /\ L + C - 1 >= 0 /\ -L + C >= 0 /\ -L + 1 >= 0 /\ L >= 0 /\ J - K >= 0 /\ -J + K >= 0 /\ E >= 2 /\ 0 >= D /\ R >= 0 ] f22(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f26(A, B, C, D - 1, 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 + 1 >= 0 /\ C - I >= 0 /\ L - I + 1 >= 0 /\ -L - I + 2 >= 0 /\ I >= 0 /\ -H + I + 1 >= 0 /\ G + I >= 0 /\ F + I - 1 >= 0 /\ E + I >= 0 /\ D + I >= 0 /\ C + I - 2 >= 0 /\ L + I >= 0 /\ -L + I + 1 >= 0 /\ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H + 1 >= 0 /\ C - H >= 0 /\ L - H + 1 >= 0 /\ -L - H + 2 >= 0 /\ G + H - 1 >= 0 /\ C + H - 2 >= 0 /\ C - G - 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G >= 0 /\ C + G - 1 >= 0 /\ L + G >= 0 /\ -L + G + 1 >= 0 /\ C - F >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F - 2 >= 0 /\ L + F - 1 >= 0 /\ -L + F >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ L + E >= 0 /\ -L + E + 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ L + D >= 0 /\ -L + D + 1 >= 0 /\ C - 1 >= 0 /\ L + C - 1 >= 0 /\ -L + C >= 0 /\ -L + 1 >= 0 /\ L >= 0 /\ J - K >= 0 /\ -J + K >= 0 /\ D >= 1 ] f26(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f41(H, I, C, D, E, F, G, H, I, J, K, L, 1, J, O, P, Q)) [ -I + 1 >= 0 /\ -H - I + 2 >= 0 /\ G - I + 1 >= 0 /\ F - I >= 0 /\ E - I + 1 >= 0 /\ D - I + 1 >= 0 /\ C - I >= 0 /\ L - I + 1 >= 0 /\ -L - I + 2 >= 0 /\ I >= 0 /\ -H + I + 1 >= 0 /\ G + I >= 0 /\ F + I - 1 >= 0 /\ E + I >= 0 /\ D + I >= 0 /\ C + I - 2 >= 0 /\ L + I >= 0 /\ -L + I + 1 >= 0 /\ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H + 1 >= 0 /\ C - H >= 0 /\ L - H + 1 >= 0 /\ -L - H + 2 >= 0 /\ G + H - 1 >= 0 /\ C + H - 2 >= 0 /\ C - G - 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G >= 0 /\ C + G - 1 >= 0 /\ L + G >= 0 /\ -L + G + 1 >= 0 /\ C - F + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F - 2 >= 0 /\ L + F - 1 >= 0 /\ -L + F >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ L + E >= 0 /\ -L + E + 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ L + D >= 0 /\ -L + D + 1 >= 0 /\ C - 1 >= 0 /\ L + C - 1 >= 0 /\ -L + C >= 0 /\ -L + 1 >= 0 /\ L >= 0 /\ J - K >= 0 /\ -J + K >= 0 /\ M >= 1 /\ L >= 1 ] f26(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f41(H, I, C, D, E, F, G, H, I, J, K, L, 1, J, J, P, Q)) [ -I + 1 >= 0 /\ -H - I + 2 >= 0 /\ G - I + 1 >= 0 /\ F - I >= 0 /\ E - I + 1 >= 0 /\ D - I + 1 >= 0 /\ C - I >= 0 /\ L - I + 1 >= 0 /\ -L - I + 2 >= 0 /\ I >= 0 /\ -H + I + 1 >= 0 /\ G + I >= 0 /\ F + I - 1 >= 0 /\ E + I >= 0 /\ D + I >= 0 /\ C + I - 2 >= 0 /\ L + I >= 0 /\ -L + I + 1 >= 0 /\ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H + 1 >= 0 /\ C - H >= 0 /\ L - H + 1 >= 0 /\ -L - H + 2 >= 0 /\ G + H - 1 >= 0 /\ C + H - 2 >= 0 /\ C - G - 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G >= 0 /\ C + G - 1 >= 0 /\ L + G >= 0 /\ -L + G + 1 >= 0 /\ C - F + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F - 2 >= 0 /\ L + F - 1 >= 0 /\ -L + F >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ L + E >= 0 /\ -L + E + 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ L + D >= 0 /\ -L + D + 1 >= 0 /\ C - 1 >= 0 /\ L + C - 1 >= 0 /\ -L + C >= 0 /\ -L + 1 >= 0 /\ L >= 0 /\ J - K >= 0 /\ -J + K >= 0 /\ 0 >= M /\ L >= 1 ] f41(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f43(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 + 1 >= 0 /\ C - I >= 0 /\ B - I >= 0 /\ -B - I + 2 >= 0 /\ M - I >= 0 /\ -M - I + 2 >= 0 /\ L - I >= 0 /\ -L - I + 2 >= 0 /\ -A - I + 2 >= 0 /\ I >= 0 /\ -H + I + 1 >= 0 /\ G + I >= 0 /\ F + I - 1 >= 0 /\ E + I >= 0 /\ D + I >= 0 /\ C + I - 2 >= 0 /\ B + I >= 0 /\ -B + I >= 0 /\ M + I - 1 >= 0 /\ -M + I + 1 >= 0 /\ L + I - 1 >= 0 /\ -L + I + 1 >= 0 /\ -A + I + 1 >= 0 /\ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H + 1 >= 0 /\ C - H >= 0 /\ B - H + 1 >= 0 /\ -B - H + 2 >= 0 /\ M - H >= 0 /\ -M - H + 2 >= 0 /\ L - H >= 0 /\ -L - H + 2 >= 0 /\ A - H >= 0 /\ -A - H + 2 >= 0 /\ G + H - 1 >= 0 /\ C + H - 2 >= 0 /\ -A + H >= 0 /\ C - G - 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G >= 0 /\ C + G - 1 >= 0 /\ B + G >= 0 /\ -B + G + 1 >= 0 /\ M + G - 1 >= 0 /\ -M + G + 1 >= 0 /\ L + G - 1 >= 0 /\ -L + G + 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ C - F + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F - 2 >= 0 /\ B + F - 1 >= 0 /\ -B + F >= 0 /\ M + F - 2 >= 0 /\ -M + F >= 0 /\ L + F - 2 >= 0 /\ -L + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ B + E >= 0 /\ -B + E + 1 >= 0 /\ M + E - 1 >= 0 /\ -M + E + 1 >= 0 /\ L + E - 1 >= 0 /\ -L + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ B + D >= 0 /\ -B + D + 1 >= 0 /\ M + D - 1 >= 0 /\ -M + D + 1 >= 0 /\ L + D - 1 >= 0 /\ -L + D + 1 >= 0 /\ -A + D + 1 >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ -B + C >= 0 /\ M + C - 2 >= 0 /\ -M + C >= 0 /\ L + C - 2 >= 0 /\ -L + C >= 0 /\ A + C - 2 >= 0 /\ -A + C >= 0 /\ -B + 1 >= 0 /\ M - B >= 0 /\ -M - B + 2 >= 0 /\ L - B >= 0 /\ -L - B + 2 >= 0 /\ -A - B + 2 >= 0 /\ B >= 0 /\ M + B - 1 >= 0 /\ -M + B + 1 >= 0 /\ L + B - 1 >= 0 /\ -L + B + 1 >= 0 /\ -A + B + 1 >= 0 /\ K - N >= 0 /\ J - N >= 0 /\ -K + N >= 0 /\ -J + N >= 0 /\ -M + 1 >= 0 /\ L - M >= 0 /\ -L - M + 2 >= 0 /\ -A - M + 2 >= 0 /\ M - 1 >= 0 /\ L + M - 2 >= 0 /\ -L + M >= 0 /\ -A + M >= 0 /\ -L + 1 >= 0 /\ -A - L + 2 >= 0 /\ L - 1 >= 0 /\ -A + L >= 0 /\ J - K >= 0 /\ -J + K >= 0 /\ -A + 1 >= 0 /\ 0 >= A + 1 /\ N = O ] f41(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f43(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 + 1 >= 0 /\ C - I >= 0 /\ B - I >= 0 /\ -B - I + 2 >= 0 /\ M - I >= 0 /\ -M - I + 2 >= 0 /\ L - I >= 0 /\ -L - I + 2 >= 0 /\ -A - I + 2 >= 0 /\ I >= 0 /\ -H + I + 1 >= 0 /\ G + I >= 0 /\ F + I - 1 >= 0 /\ E + I >= 0 /\ D + I >= 0 /\ C + I - 2 >= 0 /\ B + I >= 0 /\ -B + I >= 0 /\ M + I - 1 >= 0 /\ -M + I + 1 >= 0 /\ L + I - 1 >= 0 /\ -L + I + 1 >= 0 /\ -A + I + 1 >= 0 /\ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H + 1 >= 0 /\ C - H >= 0 /\ B - H + 1 >= 0 /\ -B - H + 2 >= 0 /\ M - H >= 0 /\ -M - H + 2 >= 0 /\ L - H >= 0 /\ -L - H + 2 >= 0 /\ A - H >= 0 /\ -A - H + 2 >= 0 /\ G + H - 1 >= 0 /\ C + H - 2 >= 0 /\ -A + H >= 0 /\ C - G - 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G >= 0 /\ C + G - 1 >= 0 /\ B + G >= 0 /\ -B + G + 1 >= 0 /\ M + G - 1 >= 0 /\ -M + G + 1 >= 0 /\ L + G - 1 >= 0 /\ -L + G + 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ C - F + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F - 2 >= 0 /\ B + F - 1 >= 0 /\ -B + F >= 0 /\ M + F - 2 >= 0 /\ -M + F >= 0 /\ L + F - 2 >= 0 /\ -L + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ B + E >= 0 /\ -B + E + 1 >= 0 /\ M + E - 1 >= 0 /\ -M + E + 1 >= 0 /\ L + E - 1 >= 0 /\ -L + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ B + D >= 0 /\ -B + D + 1 >= 0 /\ M + D - 1 >= 0 /\ -M + D + 1 >= 0 /\ L + D - 1 >= 0 /\ -L + D + 1 >= 0 /\ -A + D + 1 >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ -B + C >= 0 /\ M + C - 2 >= 0 /\ -M + C >= 0 /\ L + C - 2 >= 0 /\ -L + C >= 0 /\ A + C - 2 >= 0 /\ -A + C >= 0 /\ -B + 1 >= 0 /\ M - B >= 0 /\ -M - B + 2 >= 0 /\ L - B >= 0 /\ -L - B + 2 >= 0 /\ -A - B + 2 >= 0 /\ B >= 0 /\ M + B - 1 >= 0 /\ -M + B + 1 >= 0 /\ L + B - 1 >= 0 /\ -L + B + 1 >= 0 /\ -A + B + 1 >= 0 /\ K - N >= 0 /\ J - N >= 0 /\ -K + N >= 0 /\ -J + N >= 0 /\ -M + 1 >= 0 /\ L - M >= 0 /\ -L - M + 2 >= 0 /\ -A - M + 2 >= 0 /\ M - 1 >= 0 /\ L + M - 2 >= 0 /\ -L + M >= 0 /\ -A + M >= 0 /\ -L + 1 >= 0 /\ -A - L + 2 >= 0 /\ L - 1 >= 0 /\ -A + L >= 0 /\ J - K >= 0 /\ -J + K >= 0 /\ -A + 1 >= 0 /\ A >= 1 /\ N = O ] f41(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f47(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 + 1 >= 0 /\ C - I >= 0 /\ B - I >= 0 /\ -B - I + 2 >= 0 /\ M - I >= 0 /\ -M - I + 2 >= 0 /\ L - I >= 0 /\ -L - I + 2 >= 0 /\ -A - I + 2 >= 0 /\ I >= 0 /\ -H + I + 1 >= 0 /\ G + I >= 0 /\ F + I - 1 >= 0 /\ E + I >= 0 /\ D + I >= 0 /\ C + I - 2 >= 0 /\ B + I >= 0 /\ -B + I >= 0 /\ M + I - 1 >= 0 /\ -M + I + 1 >= 0 /\ L + I - 1 >= 0 /\ -L + I + 1 >= 0 /\ -A + I + 1 >= 0 /\ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H + 1 >= 0 /\ C - H >= 0 /\ B - H + 1 >= 0 /\ -B - H + 2 >= 0 /\ M - H >= 0 /\ -M - H + 2 >= 0 /\ L - H >= 0 /\ -L - H + 2 >= 0 /\ A - H >= 0 /\ -A - H + 2 >= 0 /\ G + H - 1 >= 0 /\ C + H - 2 >= 0 /\ -A + H >= 0 /\ C - G - 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G >= 0 /\ C + G - 1 >= 0 /\ B + G >= 0 /\ -B + G + 1 >= 0 /\ M + G - 1 >= 0 /\ -M + G + 1 >= 0 /\ L + G - 1 >= 0 /\ -L + G + 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ C - F + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F - 2 >= 0 /\ B + F - 1 >= 0 /\ -B + F >= 0 /\ M + F - 2 >= 0 /\ -M + F >= 0 /\ L + F - 2 >= 0 /\ -L + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ B + E >= 0 /\ -B + E + 1 >= 0 /\ M + E - 1 >= 0 /\ -M + E + 1 >= 0 /\ L + E - 1 >= 0 /\ -L + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ B + D >= 0 /\ -B + D + 1 >= 0 /\ M + D - 1 >= 0 /\ -M + D + 1 >= 0 /\ L + D - 1 >= 0 /\ -L + D + 1 >= 0 /\ -A + D + 1 >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ -B + C >= 0 /\ M + C - 2 >= 0 /\ -M + C >= 0 /\ L + C - 2 >= 0 /\ -L + C >= 0 /\ A + C - 2 >= 0 /\ -A + C >= 0 /\ -B + 1 >= 0 /\ M - B >= 0 /\ -M - B + 2 >= 0 /\ L - B >= 0 /\ -L - B + 2 >= 0 /\ -A - B + 2 >= 0 /\ B >= 0 /\ M + B - 1 >= 0 /\ -M + B + 1 >= 0 /\ L + B - 1 >= 0 /\ -L + B + 1 >= 0 /\ -A + B + 1 >= 0 /\ K - N >= 0 /\ J - N >= 0 /\ -K + N >= 0 /\ -J + N >= 0 /\ -M + 1 >= 0 /\ L - M >= 0 /\ -L - M + 2 >= 0 /\ -A - M + 2 >= 0 /\ M - 1 >= 0 /\ L + M - 2 >= 0 /\ -L + M >= 0 /\ -A + M >= 0 /\ -L + 1 >= 0 /\ -A - L + 2 >= 0 /\ L - 1 >= 0 /\ -A + L >= 0 /\ J - K >= 0 /\ -J + K >= 0 /\ -A + 1 >= 0 /\ A = 0 /\ N = O ] f43(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f45(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 + 1 >= 0 /\ C - I >= 0 /\ B - I >= 0 /\ -B - I + 2 >= 0 /\ M - I >= 0 /\ -M - I + 2 >= 0 /\ L - I >= 0 /\ -L - I + 2 >= 0 /\ -A - I + 2 >= 0 /\ I >= 0 /\ -H + I + 1 >= 0 /\ G + I >= 0 /\ F + I - 1 >= 0 /\ E + I >= 0 /\ D + I >= 0 /\ C + I - 2 >= 0 /\ B + I >= 0 /\ -B + I >= 0 /\ M + I - 1 >= 0 /\ -M + I + 1 >= 0 /\ L + I - 1 >= 0 /\ -L + I + 1 >= 0 /\ -A + I + 1 >= 0 /\ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H + 1 >= 0 /\ C - H >= 0 /\ B - H + 1 >= 0 /\ -B - H + 2 >= 0 /\ M - H >= 0 /\ -M - H + 2 >= 0 /\ L - H >= 0 /\ -L - H + 2 >= 0 /\ A - H >= 0 /\ -A - H + 2 >= 0 /\ G + H - 1 >= 0 /\ C + H - 2 >= 0 /\ -A + H >= 0 /\ C - G - 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G >= 0 /\ C + G - 1 >= 0 /\ B + G >= 0 /\ -B + G + 1 >= 0 /\ M + G - 1 >= 0 /\ -M + G + 1 >= 0 /\ L + G - 1 >= 0 /\ -L + G + 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ C - F + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F - 2 >= 0 /\ B + F - 1 >= 0 /\ -B + F >= 0 /\ M + F - 2 >= 0 /\ -M + F >= 0 /\ L + F - 2 >= 0 /\ -L + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ B + E >= 0 /\ -B + E + 1 >= 0 /\ M + E - 1 >= 0 /\ -M + E + 1 >= 0 /\ L + E - 1 >= 0 /\ -L + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ B + D >= 0 /\ -B + D + 1 >= 0 /\ M + D - 1 >= 0 /\ -M + D + 1 >= 0 /\ L + D - 1 >= 0 /\ -L + D + 1 >= 0 /\ -A + D + 1 >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ -B + C >= 0 /\ M + C - 2 >= 0 /\ -M + C >= 0 /\ L + C - 2 >= 0 /\ -L + C >= 0 /\ A + C - 2 >= 0 /\ -A + C >= 0 /\ -B + 1 >= 0 /\ M - B >= 0 /\ -M - B + 2 >= 0 /\ L - B >= 0 /\ -L - B + 2 >= 0 /\ -A - B + 2 >= 0 /\ B >= 0 /\ M + B - 1 >= 0 /\ -M + B + 1 >= 0 /\ L + B - 1 >= 0 /\ -L + B + 1 >= 0 /\ -A + B + 1 >= 0 /\ N - O >= 0 /\ K - O >= 0 /\ J - O >= 0 /\ -N + O >= 0 /\ -K + O >= 0 /\ -J + O >= 0 /\ K - N >= 0 /\ J - N >= 0 /\ -K + N >= 0 /\ -J + N >= 0 /\ -M + 1 >= 0 /\ L - M >= 0 /\ -L - M + 2 >= 0 /\ -A - M + 2 >= 0 /\ M - 1 >= 0 /\ L + M - 2 >= 0 /\ -L + M >= 0 /\ -A + M >= 0 /\ -L + 1 >= 0 /\ -A - L + 2 >= 0 /\ L - 1 >= 0 /\ -A + L >= 0 /\ J - K >= 0 /\ -J + K >= 0 /\ -A + 1 >= 0 /\ B = 0 ] f43(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f47(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 + 1 >= 0 /\ C - I >= 0 /\ B - I >= 0 /\ -B - I + 2 >= 0 /\ M - I >= 0 /\ -M - I + 2 >= 0 /\ L - I >= 0 /\ -L - I + 2 >= 0 /\ -A - I + 2 >= 0 /\ I >= 0 /\ -H + I + 1 >= 0 /\ G + I >= 0 /\ F + I - 1 >= 0 /\ E + I >= 0 /\ D + I >= 0 /\ C + I - 2 >= 0 /\ B + I >= 0 /\ -B + I >= 0 /\ M + I - 1 >= 0 /\ -M + I + 1 >= 0 /\ L + I - 1 >= 0 /\ -L + I + 1 >= 0 /\ -A + I + 1 >= 0 /\ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H + 1 >= 0 /\ C - H >= 0 /\ B - H + 1 >= 0 /\ -B - H + 2 >= 0 /\ M - H >= 0 /\ -M - H + 2 >= 0 /\ L - H >= 0 /\ -L - H + 2 >= 0 /\ A - H >= 0 /\ -A - H + 2 >= 0 /\ G + H - 1 >= 0 /\ C + H - 2 >= 0 /\ -A + H >= 0 /\ C - G - 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G >= 0 /\ C + G - 1 >= 0 /\ B + G >= 0 /\ -B + G + 1 >= 0 /\ M + G - 1 >= 0 /\ -M + G + 1 >= 0 /\ L + G - 1 >= 0 /\ -L + G + 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ C - F + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F - 2 >= 0 /\ B + F - 1 >= 0 /\ -B + F >= 0 /\ M + F - 2 >= 0 /\ -M + F >= 0 /\ L + F - 2 >= 0 /\ -L + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ B + E >= 0 /\ -B + E + 1 >= 0 /\ M + E - 1 >= 0 /\ -M + E + 1 >= 0 /\ L + E - 1 >= 0 /\ -L + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ B + D >= 0 /\ -B + D + 1 >= 0 /\ M + D - 1 >= 0 /\ -M + D + 1 >= 0 /\ L + D - 1 >= 0 /\ -L + D + 1 >= 0 /\ -A + D + 1 >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ -B + C >= 0 /\ M + C - 2 >= 0 /\ -M + C >= 0 /\ L + C - 2 >= 0 /\ -L + C >= 0 /\ A + C - 2 >= 0 /\ -A + C >= 0 /\ -B + 1 >= 0 /\ M - B >= 0 /\ -M - B + 2 >= 0 /\ L - B >= 0 /\ -L - B + 2 >= 0 /\ -A - B + 2 >= 0 /\ B >= 0 /\ M + B - 1 >= 0 /\ -M + B + 1 >= 0 /\ L + B - 1 >= 0 /\ -L + B + 1 >= 0 /\ -A + B + 1 >= 0 /\ N - O >= 0 /\ K - O >= 0 /\ J - O >= 0 /\ -N + O >= 0 /\ -K + O >= 0 /\ -J + O >= 0 /\ K - N >= 0 /\ J - N >= 0 /\ -K + N >= 0 /\ -J + N >= 0 /\ -M + 1 >= 0 /\ L - M >= 0 /\ -L - M + 2 >= 0 /\ -A - M + 2 >= 0 /\ M - 1 >= 0 /\ L + M - 2 >= 0 /\ -L + M >= 0 /\ -A + M >= 0 /\ -L + 1 >= 0 /\ -A - L + 2 >= 0 /\ L - 1 >= 0 /\ -A + L >= 0 /\ J - K >= 0 /\ -J + K >= 0 /\ -A + 1 >= 0 /\ B >= 1 ] f47(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f45(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 + 1 >= 0 /\ C - I >= 0 /\ B - I >= 0 /\ -B - I + 2 >= 0 /\ M - I >= 0 /\ -M - I + 2 >= 0 /\ L - I >= 0 /\ -L - I + 2 >= 0 /\ -A - I + 2 >= 0 /\ I >= 0 /\ -H + I >= 0 /\ G + I - 1 >= 0 /\ F + I - 1 >= 0 /\ E + I >= 0 /\ D + I >= 0 /\ C + I - 2 >= 0 /\ B + I >= 0 /\ -B + I >= 0 /\ M + I - 1 >= 0 /\ -M + I + 1 >= 0 /\ L + I - 1 >= 0 /\ -L + I + 1 >= 0 /\ -A + I >= 0 /\ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H + 1 >= 0 /\ C - H >= 0 /\ B - H >= 0 /\ -B - H + 2 >= 0 /\ M - H >= 0 /\ -M - H + 2 >= 0 /\ L - H >= 0 /\ -L - H + 2 >= 0 /\ A - H >= 0 /\ -A - H + 2 >= 0 /\ G + H - 1 >= 0 /\ C + H - 2 >= 0 /\ -A + H >= 0 /\ C - G - 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G >= 0 /\ C + G - 1 >= 0 /\ B + G - 1 >= 0 /\ -B + G + 1 >= 0 /\ M + G - 1 >= 0 /\ -M + G + 1 >= 0 /\ L + G - 1 >= 0 /\ -L + G + 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ C - F + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F - 2 >= 0 /\ B + F - 1 >= 0 /\ -B + F >= 0 /\ M + F - 2 >= 0 /\ -M + F >= 0 /\ L + F - 2 >= 0 /\ -L + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ B + E >= 0 /\ -B + E + 1 >= 0 /\ M + E - 1 >= 0 /\ -M + E + 1 >= 0 /\ L + E - 1 >= 0 /\ -L + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ B + D >= 0 /\ -B + D + 1 >= 0 /\ M + D - 1 >= 0 /\ -M + D + 1 >= 0 /\ L + D - 1 >= 0 /\ -L + D + 1 >= 0 /\ -A + D + 1 >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ -B + C >= 0 /\ M + C - 2 >= 0 /\ -M + C >= 0 /\ L + C - 2 >= 0 /\ -L + C >= 0 /\ A + C - 2 >= 0 /\ -A + C >= 0 /\ -B + 1 >= 0 /\ M - B >= 0 /\ -M - B + 2 >= 0 /\ L - B >= 0 /\ -L - B + 2 >= 0 /\ -A - B + 2 >= 0 /\ B >= 0 /\ M + B - 1 >= 0 /\ -M + B + 1 >= 0 /\ L + B - 1 >= 0 /\ -L + B + 1 >= 0 /\ -A + B >= 0 /\ N - O >= 0 /\ K - O >= 0 /\ J - O >= 0 /\ -N + O >= 0 /\ -K + O >= 0 /\ -J + O >= 0 /\ K - N >= 0 /\ J - N >= 0 /\ -K + N >= 0 /\ -J + N >= 0 /\ -M + 1 >= 0 /\ L - M >= 0 /\ -L - M + 2 >= 0 /\ -A - M + 2 >= 0 /\ M - 1 >= 0 /\ L + M - 2 >= 0 /\ -L + M >= 0 /\ -A + M >= 0 /\ -L + 1 >= 0 /\ -A - L + 2 >= 0 /\ L - 1 >= 0 /\ -A + L >= 0 /\ J - K >= 0 /\ -J + K >= 0 /\ -A + 1 >= 0 /\ 0 >= B /\ 0 >= A ] f47(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f51(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 + 1 >= 0 /\ C - I >= 0 /\ B - I >= 0 /\ -B - I + 2 >= 0 /\ M - I >= 0 /\ -M - I + 2 >= 0 /\ L - I >= 0 /\ -L - I + 2 >= 0 /\ -A - I + 2 >= 0 /\ I >= 0 /\ -H + I >= 0 /\ G + I - 1 >= 0 /\ F + I - 1 >= 0 /\ E + I >= 0 /\ D + I >= 0 /\ C + I - 2 >= 0 /\ B + I >= 0 /\ -B + I >= 0 /\ M + I - 1 >= 0 /\ -M + I + 1 >= 0 /\ L + I - 1 >= 0 /\ -L + I + 1 >= 0 /\ -A + I >= 0 /\ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H + 1 >= 0 /\ C - H >= 0 /\ B - H >= 0 /\ -B - H + 2 >= 0 /\ M - H >= 0 /\ -M - H + 2 >= 0 /\ L - H >= 0 /\ -L - H + 2 >= 0 /\ A - H >= 0 /\ -A - H + 2 >= 0 /\ G + H - 1 >= 0 /\ C + H - 2 >= 0 /\ -A + H >= 0 /\ C - G - 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G >= 0 /\ C + G - 1 >= 0 /\ B + G - 1 >= 0 /\ -B + G + 1 >= 0 /\ M + G - 1 >= 0 /\ -M + G + 1 >= 0 /\ L + G - 1 >= 0 /\ -L + G + 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ C - F + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F - 2 >= 0 /\ B + F - 1 >= 0 /\ -B + F >= 0 /\ M + F - 2 >= 0 /\ -M + F >= 0 /\ L + F - 2 >= 0 /\ -L + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ B + E >= 0 /\ -B + E + 1 >= 0 /\ M + E - 1 >= 0 /\ -M + E + 1 >= 0 /\ L + E - 1 >= 0 /\ -L + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ B + D >= 0 /\ -B + D + 1 >= 0 /\ M + D - 1 >= 0 /\ -M + D + 1 >= 0 /\ L + D - 1 >= 0 /\ -L + D + 1 >= 0 /\ -A + D + 1 >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ -B + C >= 0 /\ M + C - 2 >= 0 /\ -M + C >= 0 /\ L + C - 2 >= 0 /\ -L + C >= 0 /\ A + C - 2 >= 0 /\ -A + C >= 0 /\ -B + 1 >= 0 /\ M - B >= 0 /\ -M - B + 2 >= 0 /\ L - B >= 0 /\ -L - B + 2 >= 0 /\ -A - B + 2 >= 0 /\ B >= 0 /\ M + B - 1 >= 0 /\ -M + B + 1 >= 0 /\ L + B - 1 >= 0 /\ -L + B + 1 >= 0 /\ -A + B >= 0 /\ N - O >= 0 /\ K - O >= 0 /\ J - O >= 0 /\ -N + O >= 0 /\ -K + O >= 0 /\ -J + O >= 0 /\ K - N >= 0 /\ J - N >= 0 /\ -K + N >= 0 /\ -J + N >= 0 /\ -M + 1 >= 0 /\ L - M >= 0 /\ -L - M + 2 >= 0 /\ -A - M + 2 >= 0 /\ M - 1 >= 0 /\ L + M - 2 >= 0 /\ -L + M >= 0 /\ -A + M >= 0 /\ -L + 1 >= 0 /\ -A - L + 2 >= 0 /\ L - 1 >= 0 /\ -A + L >= 0 /\ J - K >= 0 /\ -J + K >= 0 /\ -A + 1 >= 0 /\ B >= 1 /\ 0 >= A ] f51(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f45(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 + 1 >= 0 /\ C - I >= 0 /\ B - I >= 0 /\ -B - I + 2 >= 0 /\ M - I >= 0 /\ -M - I + 2 >= 0 /\ L - I >= 0 /\ -L - 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 - 1 >= 0 /\ C + I - 2 >= 0 /\ B + I - 2 >= 0 /\ -B + I >= 0 /\ M + I - 2 >= 0 /\ -M + I >= 0 /\ L + I - 2 >= 0 /\ -L + I >= 0 /\ -A + I >= 0 /\ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H + 1 >= 0 /\ C - H >= 0 /\ B - H >= 0 /\ -B - H + 2 >= 0 /\ M - H >= 0 /\ -M - H + 2 >= 0 /\ L - H >= 0 /\ -L - H + 2 >= 0 /\ A - H >= 0 /\ -A - H + 2 >= 0 /\ G + H - 1 >= 0 /\ C + H - 2 >= 0 /\ -A + H >= 0 /\ C - G - 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G >= 0 /\ C + G - 1 >= 0 /\ B + G - 1 >= 0 /\ -B + G + 1 >= 0 /\ M + G - 1 >= 0 /\ -M + G + 1 >= 0 /\ L + G - 1 >= 0 /\ -L + G + 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ C - F + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F - 2 >= 0 /\ B + F - 2 >= 0 /\ -B + F >= 0 /\ M + F - 2 >= 0 /\ -M + F >= 0 /\ L + F - 2 >= 0 /\ -L + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ B + E - 1 >= 0 /\ -B + E + 1 >= 0 /\ M + E - 1 >= 0 /\ -M + E + 1 >= 0 /\ L + E - 1 >= 0 /\ -L + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ B + D - 1 >= 0 /\ -B + D + 1 >= 0 /\ M + D - 1 >= 0 /\ -M + D + 1 >= 0 /\ L + D - 1 >= 0 /\ -L + D + 1 >= 0 /\ -A + D + 1 >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ -B + C >= 0 /\ M + C - 2 >= 0 /\ -M + C >= 0 /\ L + C - 2 >= 0 /\ -L + C >= 0 /\ A + C - 2 >= 0 /\ -A + C >= 0 /\ -B + 1 >= 0 /\ M - B >= 0 /\ -M - B + 2 >= 0 /\ L - B >= 0 /\ -L - B + 2 >= 0 /\ -A - B + 2 >= 0 /\ B - 1 >= 0 /\ M + B - 2 >= 0 /\ -M + B >= 0 /\ L + B - 2 >= 0 /\ -L + B >= 0 /\ -A + B >= 0 /\ N - O >= 0 /\ K - O >= 0 /\ J - O >= 0 /\ -N + O >= 0 /\ -K + O >= 0 /\ -J + O >= 0 /\ K - N >= 0 /\ J - N >= 0 /\ -K + N >= 0 /\ -J + N >= 0 /\ -M + 1 >= 0 /\ L - M >= 0 /\ -L - M + 2 >= 0 /\ -A - M + 2 >= 0 /\ M - 1 >= 0 /\ L + M - 2 >= 0 /\ -L + M >= 0 /\ -A + M >= 0 /\ -L + 1 >= 0 /\ -A - L + 2 >= 0 /\ L - 1 >= 0 /\ -A + L >= 0 /\ J - K >= 0 /\ -J + K >= 0 /\ -A + 1 >= 0 /\ B >= 1 ] f41(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f58(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, R)) [ -I + 1 >= 0 /\ -H - I + 2 >= 0 /\ G - I + 1 >= 0 /\ F - I >= 0 /\ E - I + 1 >= 0 /\ D - I + 1 >= 0 /\ C - I >= 0 /\ B - I >= 0 /\ -B - I + 2 >= 0 /\ M - I >= 0 /\ -M - I + 2 >= 0 /\ L - I >= 0 /\ -L - I + 2 >= 0 /\ -A - I + 2 >= 0 /\ I >= 0 /\ -H + I + 1 >= 0 /\ G + I >= 0 /\ F + I - 1 >= 0 /\ E + I >= 0 /\ D + I >= 0 /\ C + I - 2 >= 0 /\ B + I >= 0 /\ -B + I >= 0 /\ M + I - 1 >= 0 /\ -M + I + 1 >= 0 /\ L + I - 1 >= 0 /\ -L + I + 1 >= 0 /\ -A + I + 1 >= 0 /\ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H + 1 >= 0 /\ C - H >= 0 /\ B - H + 1 >= 0 /\ -B - H + 2 >= 0 /\ M - H >= 0 /\ -M - H + 2 >= 0 /\ L - H >= 0 /\ -L - H + 2 >= 0 /\ A - H >= 0 /\ -A - H + 2 >= 0 /\ G + H - 1 >= 0 /\ C + H - 2 >= 0 /\ -A + H >= 0 /\ C - G - 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G >= 0 /\ C + G - 1 >= 0 /\ B + G >= 0 /\ -B + G + 1 >= 0 /\ M + G - 1 >= 0 /\ -M + G + 1 >= 0 /\ L + G - 1 >= 0 /\ -L + G + 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ C - F + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F - 2 >= 0 /\ B + F - 1 >= 0 /\ -B + F >= 0 /\ M + F - 2 >= 0 /\ -M + F >= 0 /\ L + F - 2 >= 0 /\ -L + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ B + E >= 0 /\ -B + E + 1 >= 0 /\ M + E - 1 >= 0 /\ -M + E + 1 >= 0 /\ L + E - 1 >= 0 /\ -L + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ B + D >= 0 /\ -B + D + 1 >= 0 /\ M + D - 1 >= 0 /\ -M + D + 1 >= 0 /\ L + D - 1 >= 0 /\ -L + D + 1 >= 0 /\ -A + D + 1 >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ -B + C >= 0 /\ M + C - 2 >= 0 /\ -M + C >= 0 /\ L + C - 2 >= 0 /\ -L + C >= 0 /\ A + C - 2 >= 0 /\ -A + C >= 0 /\ -B + 1 >= 0 /\ M - B >= 0 /\ -M - B + 2 >= 0 /\ L - B >= 0 /\ -L - B + 2 >= 0 /\ -A - B + 2 >= 0 /\ B >= 0 /\ M + B - 1 >= 0 /\ -M + B + 1 >= 0 /\ L + B - 1 >= 0 /\ -L + B + 1 >= 0 /\ -A + B + 1 >= 0 /\ K - N >= 0 /\ J - N >= 0 /\ -K + N >= 0 /\ -J + N >= 0 /\ -M + 1 >= 0 /\ L - M >= 0 /\ -L - M + 2 >= 0 /\ -A - M + 2 >= 0 /\ M - 1 >= 0 /\ L + M - 2 >= 0 /\ -L + M >= 0 /\ -A + M >= 0 /\ -L + 1 >= 0 /\ -A - L + 2 >= 0 /\ L - 1 >= 0 /\ -A + L >= 0 /\ J - K >= 0 /\ -J + K >= 0 /\ -A + 1 >= 0 /\ R >= 0 /\ N >= O + 1 /\ 1 >= R ] f41(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f58(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, R)) [ -I + 1 >= 0 /\ -H - I + 2 >= 0 /\ G - I + 1 >= 0 /\ F - I >= 0 /\ E - I + 1 >= 0 /\ D - I + 1 >= 0 /\ C - I >= 0 /\ B - I >= 0 /\ -B - I + 2 >= 0 /\ M - I >= 0 /\ -M - I + 2 >= 0 /\ L - I >= 0 /\ -L - I + 2 >= 0 /\ -A - I + 2 >= 0 /\ I >= 0 /\ -H + I + 1 >= 0 /\ G + I >= 0 /\ F + I - 1 >= 0 /\ E + I >= 0 /\ D + I >= 0 /\ C + I - 2 >= 0 /\ B + I >= 0 /\ -B + I >= 0 /\ M + I - 1 >= 0 /\ -M + I + 1 >= 0 /\ L + I - 1 >= 0 /\ -L + I + 1 >= 0 /\ -A + I + 1 >= 0 /\ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H + 1 >= 0 /\ C - H >= 0 /\ B - H + 1 >= 0 /\ -B - H + 2 >= 0 /\ M - H >= 0 /\ -M - H + 2 >= 0 /\ L - H >= 0 /\ -L - H + 2 >= 0 /\ A - H >= 0 /\ -A - H + 2 >= 0 /\ G + H - 1 >= 0 /\ C + H - 2 >= 0 /\ -A + H >= 0 /\ C - G - 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G >= 0 /\ C + G - 1 >= 0 /\ B + G >= 0 /\ -B + G + 1 >= 0 /\ M + G - 1 >= 0 /\ -M + G + 1 >= 0 /\ L + G - 1 >= 0 /\ -L + G + 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ C - F + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F - 2 >= 0 /\ B + F - 1 >= 0 /\ -B + F >= 0 /\ M + F - 2 >= 0 /\ -M + F >= 0 /\ L + F - 2 >= 0 /\ -L + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ B + E >= 0 /\ -B + E + 1 >= 0 /\ M + E - 1 >= 0 /\ -M + E + 1 >= 0 /\ L + E - 1 >= 0 /\ -L + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ B + D >= 0 /\ -B + D + 1 >= 0 /\ M + D - 1 >= 0 /\ -M + D + 1 >= 0 /\ L + D - 1 >= 0 /\ -L + D + 1 >= 0 /\ -A + D + 1 >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ -B + C >= 0 /\ M + C - 2 >= 0 /\ -M + C >= 0 /\ L + C - 2 >= 0 /\ -L + C >= 0 /\ A + C - 2 >= 0 /\ -A + C >= 0 /\ -B + 1 >= 0 /\ M - B >= 0 /\ -M - B + 2 >= 0 /\ L - B >= 0 /\ -L - B + 2 >= 0 /\ -A - B + 2 >= 0 /\ B >= 0 /\ M + B - 1 >= 0 /\ -M + B + 1 >= 0 /\ L + B - 1 >= 0 /\ -L + B + 1 >= 0 /\ -A + B + 1 >= 0 /\ K - N >= 0 /\ J - N >= 0 /\ -K + N >= 0 /\ -J + N >= 0 /\ -M + 1 >= 0 /\ L - M >= 0 /\ -L - M + 2 >= 0 /\ -A - M + 2 >= 0 /\ M - 1 >= 0 /\ L + M - 2 >= 0 /\ -L + M >= 0 /\ -A + M >= 0 /\ -L + 1 >= 0 /\ -A - L + 2 >= 0 /\ L - 1 >= 0 /\ -A + L >= 0 /\ J - K >= 0 /\ -J + K >= 0 /\ -A + 1 >= 0 /\ R >= 0 /\ O >= N + 1 /\ 1 >= R ] f45(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f58(A, B, C, D, E, F, G, H, I, J, K, L, M, N, 0, P, R)) [ -I + 1 >= 0 /\ -H - I + 2 >= 0 /\ G - I + 1 >= 0 /\ F - I >= 0 /\ E - I + 1 >= 0 /\ D - I + 1 >= 0 /\ C - I >= 0 /\ B - I >= 0 /\ -B - I + 2 >= 0 /\ P - I - 1 >= 0 /\ -P - I + 4 >= 0 /\ M - I >= 0 /\ -M - I + 2 >= 0 /\ L - I >= 0 /\ -L - I + 2 >= 0 /\ -A - I + 2 >= 0 /\ I >= 0 /\ -H + I + 1 >= 0 /\ G + I >= 0 /\ F + I - 1 >= 0 /\ E + I >= 0 /\ D + I >= 0 /\ C + I - 2 >= 0 /\ B + I >= 0 /\ -B + I >= 0 /\ P + I - 1 >= 0 /\ -P + I + 2 >= 0 /\ M + I - 1 >= 0 /\ -M + I + 1 >= 0 /\ L + I - 1 >= 0 /\ -L + I + 1 >= 0 /\ -A + I + 1 >= 0 /\ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H + 1 >= 0 /\ C - H >= 0 /\ B - H + 1 >= 0 /\ -B - H + 2 >= 0 /\ P - H >= 0 /\ -P - H + 4 >= 0 /\ M - H >= 0 /\ -M - H + 2 >= 0 /\ L - H >= 0 /\ -L - H + 2 >= 0 /\ A - H >= 0 /\ -A - H + 2 >= 0 /\ G + H - 1 >= 0 /\ C + H - 2 >= 0 /\ -A + H >= 0 /\ C - G - 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G >= 0 /\ C + G - 1 >= 0 /\ B + G >= 0 /\ -B + G + 1 >= 0 /\ P + G - 1 >= 0 /\ -P + G + 3 >= 0 /\ M + G - 1 >= 0 /\ -M + G + 1 >= 0 /\ L + G - 1 >= 0 /\ -L + G + 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ C - F + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F - 2 >= 0 /\ B + F - 1 >= 0 /\ -B + F >= 0 /\ P + F - 2 >= 0 /\ -P + F + 2 >= 0 /\ M + F - 2 >= 0 /\ -M + F >= 0 /\ L + F - 2 >= 0 /\ -L + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ B + E >= 0 /\ -B + E + 1 >= 0 /\ P + E - 1 >= 0 /\ -P + E + 3 >= 0 /\ M + E - 1 >= 0 /\ -M + E + 1 >= 0 /\ L + E - 1 >= 0 /\ -L + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ B + D >= 0 /\ -B + D + 1 >= 0 /\ P + D - 1 >= 0 /\ -P + D + 3 >= 0 /\ M + D - 1 >= 0 /\ -M + D + 1 >= 0 /\ L + D - 1 >= 0 /\ -L + D + 1 >= 0 /\ -A + D + 1 >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ -B + C >= 0 /\ P + C - 3 >= 0 /\ -P + C + 2 >= 0 /\ M + C - 2 >= 0 /\ -M + C >= 0 /\ L + C - 2 >= 0 /\ -L + C >= 0 /\ A + C - 2 >= 0 /\ -A + C >= 0 /\ -B + 1 >= 0 /\ P - B - 1 >= 0 /\ -P - B + 4 >= 0 /\ M - B >= 0 /\ -M - B + 2 >= 0 /\ L - B >= 0 /\ -L - 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 /\ L + B - 1 >= 0 /\ -L + B + 1 >= 0 /\ -A + B + 1 >= 0 /\ -P + 3 >= 0 /\ M - P + 2 >= 0 /\ -M - P + 4 >= 0 /\ L - P + 2 >= 0 /\ -L - P + 4 >= 0 /\ -A - P + 4 >= 0 /\ P - 1 >= 0 /\ M + P - 2 >= 0 /\ -M + P >= 0 /\ L + P - 2 >= 0 /\ -L + P >= 0 /\ -A + P >= 0 /\ N - O >= 0 /\ K - O >= 0 /\ J - O >= 0 /\ -N + O >= 0 /\ -K + O >= 0 /\ -J + O >= 0 /\ K - N >= 0 /\ J - N >= 0 /\ -K + N >= 0 /\ -J + N >= 0 /\ -M + 1 >= 0 /\ L - M >= 0 /\ -L - M + 2 >= 0 /\ -A - M + 2 >= 0 /\ M - 1 >= 0 /\ L + M - 2 >= 0 /\ -L + M >= 0 /\ -A + M >= 0 /\ -L + 1 >= 0 /\ -A - L + 2 >= 0 /\ L - 1 >= 0 /\ -A + L >= 0 /\ J - K >= 0 /\ -J + K >= 0 /\ -A + 1 >= 0 /\ R >= 0 /\ O >= 1 /\ 1 >= R ] f45(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f58(A, B, C, D, E, F, G, H, I, J, K, L, M, N, 1, P, R)) [ -I + 1 >= 0 /\ -H - I + 2 >= 0 /\ G - I + 1 >= 0 /\ F - I >= 0 /\ E - I + 1 >= 0 /\ D - I + 1 >= 0 /\ C - I >= 0 /\ B - I >= 0 /\ -B - I + 2 >= 0 /\ P - I - 1 >= 0 /\ -P - I + 4 >= 0 /\ M - I >= 0 /\ -M - I + 2 >= 0 /\ L - I >= 0 /\ -L - I + 2 >= 0 /\ -A - I + 2 >= 0 /\ I >= 0 /\ -H + I + 1 >= 0 /\ G + I >= 0 /\ F + I - 1 >= 0 /\ E + I >= 0 /\ D + I >= 0 /\ C + I - 2 >= 0 /\ B + I >= 0 /\ -B + I >= 0 /\ P + I - 1 >= 0 /\ -P + I + 2 >= 0 /\ M + I - 1 >= 0 /\ -M + I + 1 >= 0 /\ L + I - 1 >= 0 /\ -L + I + 1 >= 0 /\ -A + I + 1 >= 0 /\ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H + 1 >= 0 /\ C - H >= 0 /\ B - H + 1 >= 0 /\ -B - H + 2 >= 0 /\ P - H >= 0 /\ -P - H + 4 >= 0 /\ M - H >= 0 /\ -M - H + 2 >= 0 /\ L - H >= 0 /\ -L - H + 2 >= 0 /\ A - H >= 0 /\ -A - H + 2 >= 0 /\ G + H - 1 >= 0 /\ C + H - 2 >= 0 /\ -A + H >= 0 /\ C - G - 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G >= 0 /\ C + G - 1 >= 0 /\ B + G >= 0 /\ -B + G + 1 >= 0 /\ P + G - 1 >= 0 /\ -P + G + 3 >= 0 /\ M + G - 1 >= 0 /\ -M + G + 1 >= 0 /\ L + G - 1 >= 0 /\ -L + G + 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ C - F + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F - 2 >= 0 /\ B + F - 1 >= 0 /\ -B + F >= 0 /\ P + F - 2 >= 0 /\ -P + F + 2 >= 0 /\ M + F - 2 >= 0 /\ -M + F >= 0 /\ L + F - 2 >= 0 /\ -L + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ B + E >= 0 /\ -B + E + 1 >= 0 /\ P + E - 1 >= 0 /\ -P + E + 3 >= 0 /\ M + E - 1 >= 0 /\ -M + E + 1 >= 0 /\ L + E - 1 >= 0 /\ -L + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ B + D >= 0 /\ -B + D + 1 >= 0 /\ P + D - 1 >= 0 /\ -P + D + 3 >= 0 /\ M + D - 1 >= 0 /\ -M + D + 1 >= 0 /\ L + D - 1 >= 0 /\ -L + D + 1 >= 0 /\ -A + D + 1 >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ -B + C >= 0 /\ P + C - 3 >= 0 /\ -P + C + 2 >= 0 /\ M + C - 2 >= 0 /\ -M + C >= 0 /\ L + C - 2 >= 0 /\ -L + C >= 0 /\ A + C - 2 >= 0 /\ -A + C >= 0 /\ -B + 1 >= 0 /\ P - B - 1 >= 0 /\ -P - B + 4 >= 0 /\ M - B >= 0 /\ -M - B + 2 >= 0 /\ L - B >= 0 /\ -L - 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 /\ L + B - 1 >= 0 /\ -L + B + 1 >= 0 /\ -A + B + 1 >= 0 /\ -P + 3 >= 0 /\ M - P + 2 >= 0 /\ -M - P + 4 >= 0 /\ L - P + 2 >= 0 /\ -L - P + 4 >= 0 /\ -A - P + 4 >= 0 /\ P - 1 >= 0 /\ M + P - 2 >= 0 /\ -M + P >= 0 /\ L + P - 2 >= 0 /\ -L + P >= 0 /\ -A + P >= 0 /\ N - O >= 0 /\ K - O >= 0 /\ J - O >= 0 /\ -N + O >= 0 /\ -K + O >= 0 /\ -J + O >= 0 /\ K - N >= 0 /\ J - N >= 0 /\ -K + N >= 0 /\ -J + N >= 0 /\ -M + 1 >= 0 /\ L - M >= 0 /\ -L - M + 2 >= 0 /\ -A - M + 2 >= 0 /\ M - 1 >= 0 /\ L + M - 2 >= 0 /\ -L + M >= 0 /\ -A + M >= 0 /\ -L + 1 >= 0 /\ -A - L + 2 >= 0 /\ L - 1 >= 0 /\ -A + L >= 0 /\ J - K >= 0 /\ -J + K >= 0 /\ -A + 1 >= 0 /\ R >= 0 /\ 0 >= O /\ 1 >= R ] f58(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f62(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 + 1 >= 0 /\ C - I >= 0 /\ B - I >= 0 /\ -B - I + 2 >= 0 /\ Q - I + 1 >= 0 /\ -Q - I + 2 >= 0 /\ M - I >= 0 /\ -M - I + 2 >= 0 /\ L - I >= 0 /\ -L - I + 2 >= 0 /\ -A - I + 2 >= 0 /\ I >= 0 /\ -H + I + 1 >= 0 /\ G + I >= 0 /\ F + I - 1 >= 0 /\ E + I >= 0 /\ D + I >= 0 /\ C + I - 2 >= 0 /\ B + I >= 0 /\ -B + I >= 0 /\ Q + I >= 0 /\ -Q + I + 1 >= 0 /\ M + I - 1 >= 0 /\ -M + I + 1 >= 0 /\ L + I - 1 >= 0 /\ -L + I + 1 >= 0 /\ -A + I + 1 >= 0 /\ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H + 1 >= 0 /\ C - H >= 0 /\ B - H + 1 >= 0 /\ -B - H + 2 >= 0 /\ Q - H + 1 >= 0 /\ -Q - H + 2 >= 0 /\ M - H >= 0 /\ -M - H + 2 >= 0 /\ L - H >= 0 /\ -L - H + 2 >= 0 /\ A - H >= 0 /\ -A - H + 2 >= 0 /\ G + H - 1 >= 0 /\ C + H - 2 >= 0 /\ -A + H >= 0 /\ C - G - 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G >= 0 /\ C + G - 1 >= 0 /\ B + G >= 0 /\ -B + G + 1 >= 0 /\ Q + G >= 0 /\ -Q + G + 1 >= 0 /\ M + G - 1 >= 0 /\ -M + G + 1 >= 0 /\ L + G - 1 >= 0 /\ -L + G + 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ C - F + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F - 2 >= 0 /\ B + F - 1 >= 0 /\ -B + F >= 0 /\ Q + F - 1 >= 0 /\ -Q + F >= 0 /\ M + F - 2 >= 0 /\ -M + F >= 0 /\ L + F - 2 >= 0 /\ -L + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ B + E >= 0 /\ -B + E + 1 >= 0 /\ Q + E >= 0 /\ -Q + E + 1 >= 0 /\ M + E - 1 >= 0 /\ -M + E + 1 >= 0 /\ L + E - 1 >= 0 /\ -L + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ B + D >= 0 /\ -B + D + 1 >= 0 /\ Q + D >= 0 /\ -Q + D + 1 >= 0 /\ M + D - 1 >= 0 /\ -M + D + 1 >= 0 /\ L + D - 1 >= 0 /\ -L + D + 1 >= 0 /\ -A + D + 1 >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ -B + C >= 0 /\ Q + C - 1 >= 0 /\ -Q + C >= 0 /\ M + C - 2 >= 0 /\ -M + C >= 0 /\ L + C - 2 >= 0 /\ -L + C >= 0 /\ A + C - 2 >= 0 /\ -A + C >= 0 /\ -B + 1 >= 0 /\ Q - B + 1 >= 0 /\ -Q - B + 2 >= 0 /\ M - B >= 0 /\ -M - B + 2 >= 0 /\ L - B >= 0 /\ -L - B + 2 >= 0 /\ -A - B + 2 >= 0 /\ B >= 0 /\ Q + B >= 0 /\ -Q + B + 1 >= 0 /\ M + B - 1 >= 0 /\ -M + B + 1 >= 0 /\ L + B - 1 >= 0 /\ -L + B + 1 >= 0 /\ -A + B + 1 >= 0 /\ -Q + 1 >= 0 /\ M - Q >= 0 /\ -M - Q + 2 >= 0 /\ L - Q >= 0 /\ -L - Q + 2 >= 0 /\ -A - Q + 2 >= 0 /\ Q >= 0 /\ M + Q - 1 >= 0 /\ -M + Q + 1 >= 0 /\ L + Q - 1 >= 0 /\ -L + Q + 1 >= 0 /\ -A + Q + 1 >= 0 /\ K - N >= 0 /\ J - N >= 0 /\ -K + N >= 0 /\ -J + N >= 0 /\ -M + 1 >= 0 /\ L - M >= 0 /\ -L - M + 2 >= 0 /\ -A - M + 2 >= 0 /\ M - 1 >= 0 /\ L + M - 2 >= 0 /\ -L + M >= 0 /\ -A + M >= 0 /\ -L + 1 >= 0 /\ -A - L + 2 >= 0 /\ L - 1 >= 0 /\ -A + L >= 0 /\ J - K >= 0 /\ -J + K >= 0 /\ -A + 1 >= 0 /\ 0 >= E /\ 0 >= D /\ Q >= 1 ] f58(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f62(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 + 1 >= 0 /\ C - I >= 0 /\ B - I >= 0 /\ -B - I + 2 >= 0 /\ Q - I + 1 >= 0 /\ -Q - I + 2 >= 0 /\ M - I >= 0 /\ -M - I + 2 >= 0 /\ L - I >= 0 /\ -L - I + 2 >= 0 /\ -A - I + 2 >= 0 /\ I >= 0 /\ -H + I + 1 >= 0 /\ G + I >= 0 /\ F + I - 1 >= 0 /\ E + I >= 0 /\ D + I >= 0 /\ C + I - 2 >= 0 /\ B + I >= 0 /\ -B + I >= 0 /\ Q + I >= 0 /\ -Q + I + 1 >= 0 /\ M + I - 1 >= 0 /\ -M + I + 1 >= 0 /\ L + I - 1 >= 0 /\ -L + I + 1 >= 0 /\ -A + I + 1 >= 0 /\ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H + 1 >= 0 /\ C - H >= 0 /\ B - H + 1 >= 0 /\ -B - H + 2 >= 0 /\ Q - H + 1 >= 0 /\ -Q - H + 2 >= 0 /\ M - H >= 0 /\ -M - H + 2 >= 0 /\ L - H >= 0 /\ -L - H + 2 >= 0 /\ A - H >= 0 /\ -A - H + 2 >= 0 /\ G + H - 1 >= 0 /\ C + H - 2 >= 0 /\ -A + H >= 0 /\ C - G - 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G >= 0 /\ C + G - 1 >= 0 /\ B + G >= 0 /\ -B + G + 1 >= 0 /\ Q + G >= 0 /\ -Q + G + 1 >= 0 /\ M + G - 1 >= 0 /\ -M + G + 1 >= 0 /\ L + G - 1 >= 0 /\ -L + G + 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ C - F + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F - 2 >= 0 /\ B + F - 1 >= 0 /\ -B + F >= 0 /\ Q + F - 1 >= 0 /\ -Q + F >= 0 /\ M + F - 2 >= 0 /\ -M + F >= 0 /\ L + F - 2 >= 0 /\ -L + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ B + E >= 0 /\ -B + E + 1 >= 0 /\ Q + E >= 0 /\ -Q + E + 1 >= 0 /\ M + E - 1 >= 0 /\ -M + E + 1 >= 0 /\ L + E - 1 >= 0 /\ -L + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ B + D >= 0 /\ -B + D + 1 >= 0 /\ Q + D >= 0 /\ -Q + D + 1 >= 0 /\ M + D - 1 >= 0 /\ -M + D + 1 >= 0 /\ L + D - 1 >= 0 /\ -L + D + 1 >= 0 /\ -A + D + 1 >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ -B + C >= 0 /\ Q + C - 1 >= 0 /\ -Q + C >= 0 /\ M + C - 2 >= 0 /\ -M + C >= 0 /\ L + C - 2 >= 0 /\ -L + C >= 0 /\ A + C - 2 >= 0 /\ -A + C >= 0 /\ -B + 1 >= 0 /\ Q - B + 1 >= 0 /\ -Q - B + 2 >= 0 /\ M - B >= 0 /\ -M - B + 2 >= 0 /\ L - B >= 0 /\ -L - B + 2 >= 0 /\ -A - B + 2 >= 0 /\ B >= 0 /\ Q + B >= 0 /\ -Q + B + 1 >= 0 /\ M + B - 1 >= 0 /\ -M + B + 1 >= 0 /\ L + B - 1 >= 0 /\ -L + B + 1 >= 0 /\ -A + B + 1 >= 0 /\ -Q + 1 >= 0 /\ M - Q >= 0 /\ -M - Q + 2 >= 0 /\ L - Q >= 0 /\ -L - Q + 2 >= 0 /\ -A - Q + 2 >= 0 /\ Q >= 0 /\ M + Q - 1 >= 0 /\ -M + Q + 1 >= 0 /\ L + Q - 1 >= 0 /\ -L + Q + 1 >= 0 /\ -A + Q + 1 >= 0 /\ K - N >= 0 /\ J - N >= 0 /\ -K + N >= 0 /\ -J + N >= 0 /\ -M + 1 >= 0 /\ L - M >= 0 /\ -L - M + 2 >= 0 /\ -A - M + 2 >= 0 /\ M - 1 >= 0 /\ L + M - 2 >= 0 /\ -L + M >= 0 /\ -A + M >= 0 /\ -L + 1 >= 0 /\ -A - L + 2 >= 0 /\ L - 1 >= 0 /\ -A + L >= 0 /\ J - K >= 0 /\ -J + K >= 0 /\ -A + 1 >= 0 /\ 0 >= D /\ Q >= 1 /\ E = 1 ] f58(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f62(A, B, C, R, 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 + 1 >= 0 /\ C - I >= 0 /\ B - I >= 0 /\ -B - I + 2 >= 0 /\ Q - I + 1 >= 0 /\ -Q - I + 2 >= 0 /\ M - I >= 0 /\ -M - I + 2 >= 0 /\ L - I >= 0 /\ -L - I + 2 >= 0 /\ -A - I + 2 >= 0 /\ I >= 0 /\ -H + I + 1 >= 0 /\ G + I >= 0 /\ F + I - 1 >= 0 /\ E + I >= 0 /\ D + I >= 0 /\ C + I - 2 >= 0 /\ B + I >= 0 /\ -B + I >= 0 /\ Q + I >= 0 /\ -Q + I + 1 >= 0 /\ M + I - 1 >= 0 /\ -M + I + 1 >= 0 /\ L + I - 1 >= 0 /\ -L + I + 1 >= 0 /\ -A + I + 1 >= 0 /\ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H + 1 >= 0 /\ C - H >= 0 /\ B - H + 1 >= 0 /\ -B - H + 2 >= 0 /\ Q - H + 1 >= 0 /\ -Q - H + 2 >= 0 /\ M - H >= 0 /\ -M - H + 2 >= 0 /\ L - H >= 0 /\ -L - H + 2 >= 0 /\ A - H >= 0 /\ -A - H + 2 >= 0 /\ G + H - 1 >= 0 /\ C + H - 2 >= 0 /\ -A + H >= 0 /\ C - G - 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G >= 0 /\ C + G - 1 >= 0 /\ B + G >= 0 /\ -B + G + 1 >= 0 /\ Q + G >= 0 /\ -Q + G + 1 >= 0 /\ M + G - 1 >= 0 /\ -M + G + 1 >= 0 /\ L + G - 1 >= 0 /\ -L + G + 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ C - F + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F - 2 >= 0 /\ B + F - 1 >= 0 /\ -B + F >= 0 /\ Q + F - 1 >= 0 /\ -Q + F >= 0 /\ M + F - 2 >= 0 /\ -M + F >= 0 /\ L + F - 2 >= 0 /\ -L + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ B + E >= 0 /\ -B + E + 1 >= 0 /\ Q + E >= 0 /\ -Q + E + 1 >= 0 /\ M + E - 1 >= 0 /\ -M + E + 1 >= 0 /\ L + E - 1 >= 0 /\ -L + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ B + D >= 0 /\ -B + D + 1 >= 0 /\ Q + D >= 0 /\ -Q + D + 1 >= 0 /\ M + D - 1 >= 0 /\ -M + D + 1 >= 0 /\ L + D - 1 >= 0 /\ -L + D + 1 >= 0 /\ -A + D + 1 >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ -B + C >= 0 /\ Q + C - 1 >= 0 /\ -Q + C >= 0 /\ M + C - 2 >= 0 /\ -M + C >= 0 /\ L + C - 2 >= 0 /\ -L + C >= 0 /\ A + C - 2 >= 0 /\ -A + C >= 0 /\ -B + 1 >= 0 /\ Q - B + 1 >= 0 /\ -Q - B + 2 >= 0 /\ M - B >= 0 /\ -M - B + 2 >= 0 /\ L - B >= 0 /\ -L - B + 2 >= 0 /\ -A - B + 2 >= 0 /\ B >= 0 /\ Q + B >= 0 /\ -Q + B + 1 >= 0 /\ M + B - 1 >= 0 /\ -M + B + 1 >= 0 /\ L + B - 1 >= 0 /\ -L + B + 1 >= 0 /\ -A + B + 1 >= 0 /\ -Q + 1 >= 0 /\ M - Q >= 0 /\ -M - Q + 2 >= 0 /\ L - Q >= 0 /\ -L - Q + 2 >= 0 /\ -A - Q + 2 >= 0 /\ Q >= 0 /\ M + Q - 1 >= 0 /\ -M + Q + 1 >= 0 /\ L + Q - 1 >= 0 /\ -L + Q + 1 >= 0 /\ -A + Q + 1 >= 0 /\ K - N >= 0 /\ J - N >= 0 /\ -K + N >= 0 /\ -J + N >= 0 /\ -M + 1 >= 0 /\ L - M >= 0 /\ -L - M + 2 >= 0 /\ -A - M + 2 >= 0 /\ M - 1 >= 0 /\ L + M - 2 >= 0 /\ -L + M >= 0 /\ -A + M >= 0 /\ -L + 1 >= 0 /\ -A - L + 2 >= 0 /\ L - 1 >= 0 /\ -A + L >= 0 /\ J - K >= 0 /\ -J + K >= 0 /\ -A + 1 >= 0 /\ E >= 2 /\ 0 >= D /\ R >= 0 ] f58(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f62(A, B, C, D - 1, 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 + 1 >= 0 /\ C - I >= 0 /\ B - I >= 0 /\ -B - I + 2 >= 0 /\ Q - I + 1 >= 0 /\ -Q - I + 2 >= 0 /\ M - I >= 0 /\ -M - I + 2 >= 0 /\ L - I >= 0 /\ -L - I + 2 >= 0 /\ -A - I + 2 >= 0 /\ I >= 0 /\ -H + I + 1 >= 0 /\ G + I >= 0 /\ F + I - 1 >= 0 /\ E + I >= 0 /\ D + I >= 0 /\ C + I - 2 >= 0 /\ B + I >= 0 /\ -B + I >= 0 /\ Q + I >= 0 /\ -Q + I + 1 >= 0 /\ M + I - 1 >= 0 /\ -M + I + 1 >= 0 /\ L + I - 1 >= 0 /\ -L + I + 1 >= 0 /\ -A + I + 1 >= 0 /\ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H + 1 >= 0 /\ C - H >= 0 /\ B - H + 1 >= 0 /\ -B - H + 2 >= 0 /\ Q - H + 1 >= 0 /\ -Q - H + 2 >= 0 /\ M - H >= 0 /\ -M - H + 2 >= 0 /\ L - H >= 0 /\ -L - H + 2 >= 0 /\ A - H >= 0 /\ -A - H + 2 >= 0 /\ G + H - 1 >= 0 /\ C + H - 2 >= 0 /\ -A + H >= 0 /\ C - G - 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G >= 0 /\ C + G - 1 >= 0 /\ B + G >= 0 /\ -B + G + 1 >= 0 /\ Q + G >= 0 /\ -Q + G + 1 >= 0 /\ M + G - 1 >= 0 /\ -M + G + 1 >= 0 /\ L + G - 1 >= 0 /\ -L + G + 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ C - F + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F - 2 >= 0 /\ B + F - 1 >= 0 /\ -B + F >= 0 /\ Q + F - 1 >= 0 /\ -Q + F >= 0 /\ M + F - 2 >= 0 /\ -M + F >= 0 /\ L + F - 2 >= 0 /\ -L + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ B + E >= 0 /\ -B + E + 1 >= 0 /\ Q + E >= 0 /\ -Q + E + 1 >= 0 /\ M + E - 1 >= 0 /\ -M + E + 1 >= 0 /\ L + E - 1 >= 0 /\ -L + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ B + D >= 0 /\ -B + D + 1 >= 0 /\ Q + D >= 0 /\ -Q + D + 1 >= 0 /\ M + D - 1 >= 0 /\ -M + D + 1 >= 0 /\ L + D - 1 >= 0 /\ -L + D + 1 >= 0 /\ -A + D + 1 >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ -B + C >= 0 /\ Q + C - 1 >= 0 /\ -Q + C >= 0 /\ M + C - 2 >= 0 /\ -M + C >= 0 /\ L + C - 2 >= 0 /\ -L + C >= 0 /\ A + C - 2 >= 0 /\ -A + C >= 0 /\ -B + 1 >= 0 /\ Q - B + 1 >= 0 /\ -Q - B + 2 >= 0 /\ M - B >= 0 /\ -M - B + 2 >= 0 /\ L - B >= 0 /\ -L - B + 2 >= 0 /\ -A - B + 2 >= 0 /\ B >= 0 /\ Q + B >= 0 /\ -Q + B + 1 >= 0 /\ M + B - 1 >= 0 /\ -M + B + 1 >= 0 /\ L + B - 1 >= 0 /\ -L + B + 1 >= 0 /\ -A + B + 1 >= 0 /\ -Q + 1 >= 0 /\ M - Q >= 0 /\ -M - Q + 2 >= 0 /\ L - Q >= 0 /\ -L - Q + 2 >= 0 /\ -A - Q + 2 >= 0 /\ Q >= 0 /\ M + Q - 1 >= 0 /\ -M + Q + 1 >= 0 /\ L + Q - 1 >= 0 /\ -L + Q + 1 >= 0 /\ -A + Q + 1 >= 0 /\ K - N >= 0 /\ J - N >= 0 /\ -K + N >= 0 /\ -J + N >= 0 /\ -M + 1 >= 0 /\ L - M >= 0 /\ -L - M + 2 >= 0 /\ -A - M + 2 >= 0 /\ M - 1 >= 0 /\ L + M - 2 >= 0 /\ -L + M >= 0 /\ -A + M >= 0 /\ -L + 1 >= 0 /\ -A - L + 2 >= 0 /\ L - 1 >= 0 /\ -A + L >= 0 /\ J - K >= 0 /\ -J + K >= 0 /\ -A + 1 >= 0 /\ D >= 1 ] f62(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f22(A, B, C, D, E, F, G, H, I, J, K, R, 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 + 1 >= 0 /\ C - I >= 0 /\ B - I >= 0 /\ -B - I + 2 >= 0 /\ Q - I + 1 >= 0 /\ -Q - I + 2 >= 0 /\ M - I >= 0 /\ -M - I + 2 >= 0 /\ L - I >= 0 /\ -L - I + 2 >= 0 /\ -A - I + 2 >= 0 /\ I >= 0 /\ -H + I + 1 >= 0 /\ G + I >= 0 /\ F + I - 1 >= 0 /\ E + I >= 0 /\ D + I >= 0 /\ C + I - 2 >= 0 /\ B + I >= 0 /\ -B + I >= 0 /\ Q + I >= 0 /\ -Q + I + 1 >= 0 /\ M + I - 1 >= 0 /\ -M + I + 1 >= 0 /\ L + I - 1 >= 0 /\ -L + I + 1 >= 0 /\ -A + I + 1 >= 0 /\ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H + 1 >= 0 /\ C - H >= 0 /\ B - H + 1 >= 0 /\ -B - H + 2 >= 0 /\ Q - H + 1 >= 0 /\ -Q - H + 2 >= 0 /\ M - H >= 0 /\ -M - H + 2 >= 0 /\ L - H >= 0 /\ -L - H + 2 >= 0 /\ A - H >= 0 /\ -A - H + 2 >= 0 /\ G + H - 1 >= 0 /\ C + H - 2 >= 0 /\ -A + H >= 0 /\ C - G - 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G >= 0 /\ C + G - 1 >= 0 /\ B + G >= 0 /\ -B + G + 1 >= 0 /\ Q + G >= 0 /\ -Q + G + 1 >= 0 /\ M + G - 1 >= 0 /\ -M + G + 1 >= 0 /\ L + G - 1 >= 0 /\ -L + G + 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ C - F + 2 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F - 2 >= 0 /\ B + F - 1 >= 0 /\ -B + F >= 0 /\ Q + F - 1 >= 0 /\ -Q + F >= 0 /\ M + F - 2 >= 0 /\ -M + F >= 0 /\ L + F - 2 >= 0 /\ -L + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ B + E >= 0 /\ -B + E + 1 >= 0 /\ Q + E >= 0 /\ -Q + E + 1 >= 0 /\ M + E - 1 >= 0 /\ -M + E + 1 >= 0 /\ L + E - 1 >= 0 /\ -L + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ B + D >= 0 /\ -B + D + 1 >= 0 /\ Q + D >= 0 /\ -Q + D + 1 >= 0 /\ M + D - 1 >= 0 /\ -M + D + 1 >= 0 /\ L + D - 1 >= 0 /\ -L + D + 1 >= 0 /\ -A + D + 1 >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ -B + C >= 0 /\ Q + C - 1 >= 0 /\ -Q + C >= 0 /\ M + C - 2 >= 0 /\ -M + C >= 0 /\ L + C - 2 >= 0 /\ -L + C >= 0 /\ A + C - 2 >= 0 /\ -A + C >= 0 /\ -B + 1 >= 0 /\ Q - B + 1 >= 0 /\ -Q - B + 2 >= 0 /\ M - B >= 0 /\ -M - B + 2 >= 0 /\ L - B >= 0 /\ -L - B + 2 >= 0 /\ -A - B + 2 >= 0 /\ B >= 0 /\ Q + B >= 0 /\ -Q + B + 1 >= 0 /\ M + B - 1 >= 0 /\ -M + B + 1 >= 0 /\ L + B - 1 >= 0 /\ -L + B + 1 >= 0 /\ -A + B + 1 >= 0 /\ -Q + 1 >= 0 /\ M - Q >= 0 /\ -M - Q + 2 >= 0 /\ L - Q >= 0 /\ -L - Q + 2 >= 0 /\ -A - Q + 2 >= 0 /\ Q >= 0 /\ M + Q - 1 >= 0 /\ -M + Q + 1 >= 0 /\ L + Q - 1 >= 0 /\ -L + Q + 1 >= 0 /\ -A + Q + 1 >= 0 /\ K - N >= 0 /\ J - N >= 0 /\ -K + N >= 0 /\ -J + N >= 0 /\ -M + 1 >= 0 /\ L - M >= 0 /\ -L - M + 2 >= 0 /\ -A - M + 2 >= 0 /\ M - 1 >= 0 /\ L + M - 2 >= 0 /\ -L + M >= 0 /\ -A + M >= 0 /\ -L + 1 >= 0 /\ -A - L + 2 >= 0 /\ L - 1 >= 0 /\ -A + L >= 0 /\ J - K >= 0 /\ -J + K >= 0 /\ -A + 1 >= 0 /\ C >= F /\ R >= 0 /\ 0 >= Q /\ 1 >= R ] f26(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f22(A, B, C, D, E, F, G, H, I, J, K, R, 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 + 1 >= 0 /\ C - I >= 0 /\ L - I + 1 >= 0 /\ -L - I + 2 >= 0 /\ I >= 0 /\ -H + I + 1 >= 0 /\ G + I >= 0 /\ F + I - 1 >= 0 /\ E + I >= 0 /\ D + I >= 0 /\ C + I - 2 >= 0 /\ L + I >= 0 /\ -L + I + 1 >= 0 /\ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H + 1 >= 0 /\ C - H >= 0 /\ L - H + 1 >= 0 /\ -L - H + 2 >= 0 /\ G + H - 1 >= 0 /\ C + H - 2 >= 0 /\ C - G - 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G >= 0 /\ C + G - 1 >= 0 /\ L + G >= 0 /\ -L + G + 1 >= 0 /\ C - F + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F - 2 >= 0 /\ L + F - 1 >= 0 /\ -L + F >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ L + E >= 0 /\ -L + E + 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ L + D >= 0 /\ -L + D + 1 >= 0 /\ C - 1 >= 0 /\ L + C - 1 >= 0 /\ -L + C >= 0 /\ -L + 1 >= 0 /\ L >= 0 /\ J - K >= 0 /\ -J + K >= 0 /\ 0 >= L /\ C >= F /\ 1 >= R /\ R >= 0 ] f62(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, 0, L, 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 + 1 >= 0 /\ C - I >= 0 /\ B - I >= 0 /\ -B - I + 2 >= 0 /\ Q - I + 1 >= 0 /\ -Q - I + 2 >= 0 /\ M - I >= 0 /\ -M - I + 2 >= 0 /\ L - I >= 0 /\ -L - I + 2 >= 0 /\ -A - I + 2 >= 0 /\ I >= 0 /\ -H + I + 1 >= 0 /\ G + I >= 0 /\ F + I - 1 >= 0 /\ E + I >= 0 /\ D + I >= 0 /\ C + I - 2 >= 0 /\ B + I >= 0 /\ -B + I >= 0 /\ Q + I >= 0 /\ -Q + I + 1 >= 0 /\ M + I - 1 >= 0 /\ -M + I + 1 >= 0 /\ L + I - 1 >= 0 /\ -L + I + 1 >= 0 /\ -A + I + 1 >= 0 /\ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H + 1 >= 0 /\ C - H >= 0 /\ B - H + 1 >= 0 /\ -B - H + 2 >= 0 /\ Q - H + 1 >= 0 /\ -Q - H + 2 >= 0 /\ M - H >= 0 /\ -M - H + 2 >= 0 /\ L - H >= 0 /\ -L - H + 2 >= 0 /\ A - H >= 0 /\ -A - H + 2 >= 0 /\ G + H - 1 >= 0 /\ C + H - 2 >= 0 /\ -A + H >= 0 /\ C - G - 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G >= 0 /\ C + G - 1 >= 0 /\ B + G >= 0 /\ -B + G + 1 >= 0 /\ Q + G >= 0 /\ -Q + G + 1 >= 0 /\ M + G - 1 >= 0 /\ -M + G + 1 >= 0 /\ L + G - 1 >= 0 /\ -L + G + 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ C - F + 2 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F - 2 >= 0 /\ B + F - 1 >= 0 /\ -B + F >= 0 /\ Q + F - 1 >= 0 /\ -Q + F >= 0 /\ M + F - 2 >= 0 /\ -M + F >= 0 /\ L + F - 2 >= 0 /\ -L + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ B + E >= 0 /\ -B + E + 1 >= 0 /\ Q + E >= 0 /\ -Q + E + 1 >= 0 /\ M + E - 1 >= 0 /\ -M + E + 1 >= 0 /\ L + E - 1 >= 0 /\ -L + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ B + D >= 0 /\ -B + D + 1 >= 0 /\ Q + D >= 0 /\ -Q + D + 1 >= 0 /\ M + D - 1 >= 0 /\ -M + D + 1 >= 0 /\ L + D - 1 >= 0 /\ -L + D + 1 >= 0 /\ -A + D + 1 >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ -B + C >= 0 /\ Q + C - 1 >= 0 /\ -Q + C >= 0 /\ M + C - 2 >= 0 /\ -M + C >= 0 /\ L + C - 2 >= 0 /\ -L + C >= 0 /\ A + C - 2 >= 0 /\ -A + C >= 0 /\ -B + 1 >= 0 /\ Q - B + 1 >= 0 /\ -Q - B + 2 >= 0 /\ M - B >= 0 /\ -M - B + 2 >= 0 /\ L - B >= 0 /\ -L - B + 2 >= 0 /\ -A - B + 2 >= 0 /\ B >= 0 /\ Q + B >= 0 /\ -Q + B + 1 >= 0 /\ M + B - 1 >= 0 /\ -M + B + 1 >= 0 /\ L + B - 1 >= 0 /\ -L + B + 1 >= 0 /\ -A + B + 1 >= 0 /\ -Q + 1 >= 0 /\ M - Q >= 0 /\ -M - Q + 2 >= 0 /\ L - Q >= 0 /\ -L - Q + 2 >= 0 /\ -A - Q + 2 >= 0 /\ Q >= 0 /\ M + Q - 1 >= 0 /\ -M + Q + 1 >= 0 /\ L + Q - 1 >= 0 /\ -L + Q + 1 >= 0 /\ -A + Q + 1 >= 0 /\ K - N >= 0 /\ J - N >= 0 /\ -K + N >= 0 /\ -J + N >= 0 /\ -M + 1 >= 0 /\ L - M >= 0 /\ -L - M + 2 >= 0 /\ -A - M + 2 >= 0 /\ M - 1 >= 0 /\ L + M - 2 >= 0 /\ -L + M >= 0 /\ -A + M >= 0 /\ -L + 1 >= 0 /\ -A - L + 2 >= 0 /\ L - 1 >= 0 /\ -A + L >= 0 /\ J - K >= 0 /\ -J + K >= 0 /\ -A + 1 >= 0 /\ K >= 1 /\ C >= F /\ Q = 1 ] f62(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, 1, L, 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 + 1 >= 0 /\ C - I >= 0 /\ B - I >= 0 /\ -B - I + 2 >= 0 /\ Q - I + 1 >= 0 /\ -Q - I + 2 >= 0 /\ M - I >= 0 /\ -M - I + 2 >= 0 /\ L - I >= 0 /\ -L - I + 2 >= 0 /\ -A - I + 2 >= 0 /\ I >= 0 /\ -H + I + 1 >= 0 /\ G + I >= 0 /\ F + I - 1 >= 0 /\ E + I >= 0 /\ D + I >= 0 /\ C + I - 2 >= 0 /\ B + I >= 0 /\ -B + I >= 0 /\ Q + I >= 0 /\ -Q + I + 1 >= 0 /\ M + I - 1 >= 0 /\ -M + I + 1 >= 0 /\ L + I - 1 >= 0 /\ -L + I + 1 >= 0 /\ -A + I + 1 >= 0 /\ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H + 1 >= 0 /\ C - H >= 0 /\ B - H + 1 >= 0 /\ -B - H + 2 >= 0 /\ Q - H + 1 >= 0 /\ -Q - H + 2 >= 0 /\ M - H >= 0 /\ -M - H + 2 >= 0 /\ L - H >= 0 /\ -L - H + 2 >= 0 /\ A - H >= 0 /\ -A - H + 2 >= 0 /\ G + H - 1 >= 0 /\ C + H - 2 >= 0 /\ -A + H >= 0 /\ C - G - 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ D + G >= 0 /\ C + G - 1 >= 0 /\ B + G >= 0 /\ -B + G + 1 >= 0 /\ Q + G >= 0 /\ -Q + G + 1 >= 0 /\ M + G - 1 >= 0 /\ -M + G + 1 >= 0 /\ L + G - 1 >= 0 /\ -L + G + 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ C - F + 2 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F - 2 >= 0 /\ B + F - 1 >= 0 /\ -B + F >= 0 /\ Q + F - 1 >= 0 /\ -Q + F >= 0 /\ M + F - 2 >= 0 /\ -M + F >= 0 /\ L + F - 2 >= 0 /\ -L + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ B + E >= 0 /\ -B + E + 1 >= 0 /\ Q + E >= 0 /\ -Q + E + 1 >= 0 /\ M + E - 1 >= 0 /\ -M + E + 1 >= 0 /\ L + E - 1 >= 0 /\ -L + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ B + D >= 0 /\ -B + D + 1 >= 0 /\ Q + D >= 0 /\ -Q + D + 1 >= 0 /\ M + D - 1 >= 0 /\ -M + D + 1 >= 0 /\ L + D - 1 >= 0 /\ -L + D + 1 >= 0 /\ -A + D + 1 >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ -B + C >= 0 /\ Q + C - 1 >= 0 /\ -Q + C >= 0 /\ M + C - 2 >= 0 /\ -M + C >= 0 /\ L + C - 2 >= 0 /\ -L + C >= 0 /\ A + C - 2 >= 0 /\ -A + C >= 0 /\ -B + 1 >= 0 /\ Q - B + 1 >= 0 /\ -Q - B + 2 >= 0 /\ M - B >= 0 /\ -M - B + 2 >= 0 /\ L - B >= 0 /\ -L - B + 2 >= 0 /\ -A - B + 2 >= 0 /\ B >= 0 /\ Q + B >= 0 /\ -Q + B + 1 >= 0 /\ M + B - 1 >= 0 /\ -M + B + 1 >= 0 /\ L + B - 1 >= 0 /\ -L + B + 1 >= 0 /\ -A + B + 1 >= 0 /\ -Q + 1 >= 0 /\ M - Q >= 0 /\ -M - Q + 2 >= 0 /\ L - Q >= 0 /\ -L - Q + 2 >= 0 /\ -A - Q + 2 >= 0 /\ Q >= 0 /\ M + Q - 1 >= 0 /\ -M + Q + 1 >= 0 /\ L + Q - 1 >= 0 /\ -L + Q + 1 >= 0 /\ -A + Q + 1 >= 0 /\ K - N >= 0 /\ J - N >= 0 /\ -K + N >= 0 /\ -J + N >= 0 /\ -M + 1 >= 0 /\ L - M >= 0 /\ -L - M + 2 >= 0 /\ -A - M + 2 >= 0 /\ M - 1 >= 0 /\ L + M - 2 >= 0 /\ -L + M >= 0 /\ -A + M >= 0 /\ -L + 1 >= 0 /\ -A - L + 2 >= 0 /\ L - 1 >= 0 /\ -A + L >= 0 /\ J - K >= 0 /\ -J + K >= 0 /\ -A + 1 >= 0 /\ 0 >= K /\ C >= F /\ Q = 1 ] f10(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f81(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 >= 0 /\ C + G - 1 >= 0 /\ C - F >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F - 2 >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ C - 1 >= 0 /\ G >= C ] )