(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)) [ -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 /\ N - H >= 0 /\ -N - H + 2 >= 0 /\ K - H >= 0 /\ -K - H + 2 >= 0 /\ J - H >= 0 /\ -J - 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 /\ N + G - 1 >= 0 /\ -N + G + 1 >= 0 /\ K + G - 1 >= 0 /\ -K + G + 1 >= 0 /\ J + G - 1 >= 0 /\ -J + G + 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F - 2 >= 0 /\ B + F - 1 >= 0 /\ -B + F >= 0 /\ N + F - 2 >= 0 /\ -N + F >= 0 /\ K + F - 1 >= 0 /\ -K + F >= 0 /\ J + F - 2 >= 0 /\ -J + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ B + E >= 0 /\ -B + E + 1 >= 0 /\ N + E - 1 >= 0 /\ -N + E + 1 >= 0 /\ K + E >= 0 /\ -K + E + 1 >= 0 /\ J + E - 1 >= 0 /\ -J + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ B + D >= 0 /\ -B + D + 1 >= 0 /\ N + D - 1 >= 0 /\ -N + D + 1 >= 0 /\ K + D >= 0 /\ -K + D + 1 >= 0 /\ J + D - 1 >= 0 /\ -J + D + 1 >= 0 /\ -A + D + 1 >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ -B + C >= 0 /\ N + C - 2 >= 0 /\ -N + C >= 0 /\ K + C - 2 >= 0 /\ -K + C >= 0 /\ J + C - 2 >= 0 /\ -J + C >= 0 /\ A + C - 2 >= 0 /\ -A + C >= 0 /\ -B + 1 >= 0 /\ N - B >= 0 /\ -N - B + 2 >= 0 /\ K - B >= 0 /\ -K - B + 2 >= 0 /\ J - B >= 0 /\ -J - B + 2 >= 0 /\ -A - B + 2 >= 0 /\ B >= 0 /\ N + B - 1 >= 0 /\ -N + B + 1 >= 0 /\ K + B >= 0 /\ -K + B >= 0 /\ J + B - 1 >= 0 /\ -J + B + 1 >= 0 /\ -A + B >= 0 /\ O - P >= 0 /\ M - P >= 0 /\ L - P >= 0 /\ -O + P >= 0 /\ -M + P >= 0 /\ -L + P >= 0 /\ M - O >= 0 /\ L - O >= 0 /\ -M + O >= 0 /\ -L + O >= 0 /\ -N + 1 >= 0 /\ K - N + 1 >= 0 /\ -K - N + 2 >= 0 /\ J - N >= 0 /\ -J - N + 2 >= 0 /\ -A - N + 2 >= 0 /\ N - 1 >= 0 /\ K + N - 1 >= 0 /\ -K + N >= 0 /\ J + N - 2 >= 0 /\ -J + N >= 0 /\ -A + N >= 0 /\ L - M >= 0 /\ -L + M >= 0 /\ -K + 1 >= 0 /\ J - K >= 0 /\ -J - K + 2 >= 0 /\ -A - K + 2 >= 0 /\ K >= 0 /\ J + K - 1 >= 0 /\ -J + K + 1 >= 0 /\ -A + K >= 0 /\ -J + 1 >= 0 /\ -A - J + 2 >= 0 /\ J - 1 >= 0 /\ -A + J >= 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 /\ 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 /\ 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 ] 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, R, 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 + 1 >= 0 /\ -B - I + 2 >= 0 /\ N - I >= 0 /\ -N - I + 2 >= 0 /\ K - I + 1 >= 0 /\ -K - I + 2 >= 0 /\ J - I >= 0 /\ -J - 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 - 1 >= 0 /\ B + I >= 0 /\ -B + I + 1 >= 0 /\ N + I - 1 >= 0 /\ -N + I + 1 >= 0 /\ K + I >= 0 /\ -K + I + 1 >= 0 /\ J + I - 1 >= 0 /\ -J + 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 /\ N - H >= 0 /\ -N - H + 2 >= 0 /\ K - H + 1 >= 0 /\ -K - H + 2 >= 0 /\ J - H >= 0 /\ -J - 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 /\ N + G - 1 >= 0 /\ -N + G + 1 >= 0 /\ K + G >= 0 /\ -K + G + 1 >= 0 /\ J + G - 1 >= 0 /\ -J + G + 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F - 2 >= 0 /\ B + F - 1 >= 0 /\ -B + F >= 0 /\ N + F - 2 >= 0 /\ -N + F >= 0 /\ K + F - 1 >= 0 /\ -K + F >= 0 /\ J + F - 2 >= 0 /\ -J + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ B + E >= 0 /\ -B + E + 1 >= 0 /\ N + E - 1 >= 0 /\ -N + E + 1 >= 0 /\ K + E >= 0 /\ -K + E + 1 >= 0 /\ J + E - 1 >= 0 /\ -J + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ B + D >= 0 /\ -B + D + 1 >= 0 /\ N + D - 1 >= 0 /\ -N + D + 1 >= 0 /\ K + D >= 0 /\ -K + D + 1 >= 0 /\ J + D - 1 >= 0 /\ -J + D + 1 >= 0 /\ -A + D + 1 >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ -B + C >= 0 /\ N + C - 2 >= 0 /\ -N + C >= 0 /\ K + C - 2 >= 0 /\ -K + C >= 0 /\ J + C - 2 >= 0 /\ -J + C >= 0 /\ A + C - 2 >= 0 /\ -A + C >= 0 /\ -B + 1 >= 0 /\ N - B >= 0 /\ -N - B + 2 >= 0 /\ K - B >= 0 /\ -K - B + 2 >= 0 /\ J - B >= 0 /\ -J - B + 2 >= 0 /\ -A - B + 2 >= 0 /\ B >= 0 /\ N + B - 1 >= 0 /\ -N + B + 1 >= 0 /\ K + B >= 0 /\ -K + B >= 0 /\ J + B - 1 >= 0 /\ -J + B + 1 >= 0 /\ -A + B + 1 >= 0 /\ M - O >= 0 /\ L - O >= 0 /\ -M + O >= 0 /\ -L + O >= 0 /\ -N + 1 >= 0 /\ K - N + 1 >= 0 /\ -K - N + 2 >= 0 /\ J - N >= 0 /\ -J - N + 2 >= 0 /\ -A - N + 2 >= 0 /\ N - 1 >= 0 /\ K + N - 1 >= 0 /\ -K + N >= 0 /\ J + N - 2 >= 0 /\ -J + N >= 0 /\ -A + N >= 0 /\ L - M >= 0 /\ -L + M >= 0 /\ -K + 1 >= 0 /\ J - K >= 0 /\ -J - K + 2 >= 0 /\ -A - K + 2 >= 0 /\ K >= 0 /\ J + K - 1 >= 0 /\ -J + K + 1 >= 0 /\ -A + K + 1 >= 0 /\ -J + 1 >= 0 /\ -A - J + 2 >= 0 /\ J - 1 >= 0 /\ -A + J >= 0 /\ -A + 1 >= 0 /\ R >= 0 /\ 0 >= I /\ 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, R, K, L, 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 /\ K - H + 1 >= 0 /\ -K - H + 2 >= 0 /\ J - H + 1 >= 0 /\ -J - 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 /\ K + G >= 0 /\ -K + G + 1 >= 0 /\ J + G >= 0 /\ -J + G + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F - 2 >= 0 /\ K + F - 1 >= 0 /\ -K + F >= 0 /\ J + F - 1 >= 0 /\ -J + F >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ K + E >= 0 /\ -K + E + 1 >= 0 /\ J + E >= 0 /\ -J + E + 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ K + D >= 0 /\ -K + D + 1 >= 0 /\ J + D >= 0 /\ -J + D + 1 >= 0 /\ C - 1 >= 0 /\ K + C - 2 >= 0 /\ -K + C >= 0 /\ J + C - 1 >= 0 /\ -J + C >= 0 /\ L - M >= 0 /\ -L + M >= 0 /\ -K + 1 >= 0 /\ J - K + 1 >= 0 /\ -J - K + 2 >= 0 /\ K >= 0 /\ J + K >= 0 /\ -J + K + 1 >= 0 /\ -J + 1 >= 0 /\ J >= 0 /\ 0 >= J /\ 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, I, R, 1, M, 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 /\ 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, I, R, 0, M, 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 /\ 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)) [ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H + 1 >= 0 /\ C - H >= 0 /\ K - H + 1 >= 0 /\ -K - H + 2 >= 0 /\ J - H + 1 >= 0 /\ -J - 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 /\ K + G >= 0 /\ -K + G + 1 >= 0 /\ J + G >= 0 /\ -J + G + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F - 2 >= 0 /\ K + F - 1 >= 0 /\ -K + F >= 0 /\ J + F - 1 >= 0 /\ -J + F >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ K + E >= 0 /\ -K + E + 1 >= 0 /\ J + E >= 0 /\ -J + E + 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ K + D >= 0 /\ -K + D + 1 >= 0 /\ J + D >= 0 /\ -J + D + 1 >= 0 /\ C - 1 >= 0 /\ K + C - 2 >= 0 /\ -K + C >= 0 /\ J + C - 1 >= 0 /\ -J + C >= 0 /\ L - M >= 0 /\ -L + M >= 0 /\ -K + 1 >= 0 /\ J - K + 1 >= 0 /\ -J - K + 2 >= 0 /\ K >= 0 /\ J + K >= 0 /\ -J + K + 1 >= 0 /\ -J + 1 >= 0 /\ J >= 0 /\ J >= 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)) [ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H + 1 >= 0 /\ C - H >= 0 /\ K - H + 1 >= 0 /\ -K - H + 2 >= 0 /\ J - H + 1 >= 0 /\ -J - 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 /\ K + G >= 0 /\ -K + G + 1 >= 0 /\ J + G >= 0 /\ -J + G + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F - 2 >= 0 /\ K + F - 1 >= 0 /\ -K + F >= 0 /\ J + F - 1 >= 0 /\ -J + F >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ K + E >= 0 /\ -K + E + 1 >= 0 /\ J + E >= 0 /\ -J + E + 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ K + D >= 0 /\ -K + D + 1 >= 0 /\ J + D >= 0 /\ -J + D + 1 >= 0 /\ C - 1 >= 0 /\ K + C - 2 >= 0 /\ -K + C >= 0 /\ J + C - 1 >= 0 /\ -J + C >= 0 /\ L - M >= 0 /\ -L + M >= 0 /\ -K + 1 >= 0 /\ J - K + 1 >= 0 /\ -J - K + 2 >= 0 /\ K >= 0 /\ J + K >= 0 /\ -J + K + 1 >= 0 /\ -J + 1 >= 0 /\ J >= 0 /\ J >= 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)) [ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H + 1 >= 0 /\ C - H >= 0 /\ K - H + 1 >= 0 /\ -K - H + 2 >= 0 /\ J - H + 1 >= 0 /\ -J - 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 /\ K + G >= 0 /\ -K + G + 1 >= 0 /\ J + G >= 0 /\ -J + G + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F - 2 >= 0 /\ K + F - 1 >= 0 /\ -K + F >= 0 /\ J + F - 1 >= 0 /\ -J + F >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ K + E >= 0 /\ -K + E + 1 >= 0 /\ J + E >= 0 /\ -J + E + 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ K + D >= 0 /\ -K + D + 1 >= 0 /\ J + D >= 0 /\ -J + D + 1 >= 0 /\ C - 1 >= 0 /\ K + C - 2 >= 0 /\ -K + C >= 0 /\ J + C - 1 >= 0 /\ -J + C >= 0 /\ L - M >= 0 /\ -L + M >= 0 /\ -K + 1 >= 0 /\ J - K + 1 >= 0 /\ -J - K + 2 >= 0 /\ K >= 0 /\ J + K >= 0 /\ -J + K + 1 >= 0 /\ -J + 1 >= 0 /\ J >= 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)) [ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H + 1 >= 0 /\ C - H >= 0 /\ K - H + 1 >= 0 /\ -K - H + 2 >= 0 /\ J - H + 1 >= 0 /\ -J - 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 /\ K + G >= 0 /\ -K + G + 1 >= 0 /\ J + G >= 0 /\ -J + G + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F - 2 >= 0 /\ K + F - 1 >= 0 /\ -K + F >= 0 /\ J + F - 1 >= 0 /\ -J + F >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ K + E >= 0 /\ -K + E + 1 >= 0 /\ J + E >= 0 /\ -J + E + 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ K + D >= 0 /\ -K + D + 1 >= 0 /\ J + D >= 0 /\ -J + D + 1 >= 0 /\ C - 1 >= 0 /\ K + C - 2 >= 0 /\ -K + C >= 0 /\ J + C - 1 >= 0 /\ -J + C >= 0 /\ L - M >= 0 /\ -L + M >= 0 /\ -K + 1 >= 0 /\ J - K + 1 >= 0 /\ -J - K + 2 >= 0 /\ K >= 0 /\ J + K >= 0 /\ -J + K + 1 >= 0 /\ -J + 1 >= 0 /\ J >= 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, K, C, D, E, F, G, H, I, J, K, L, M, 1, L, P, Q)) [ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H + 1 >= 0 /\ C - H >= 0 /\ K - H + 1 >= 0 /\ -K - H + 2 >= 0 /\ J - H + 1 >= 0 /\ -J - 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 /\ K + G >= 0 /\ -K + G + 1 >= 0 /\ J + G >= 0 /\ -J + G + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F - 2 >= 0 /\ K + F - 1 >= 0 /\ -K + F >= 0 /\ J + F - 1 >= 0 /\ -J + F >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ K + E >= 0 /\ -K + E + 1 >= 0 /\ J + E >= 0 /\ -J + E + 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ K + D >= 0 /\ -K + D + 1 >= 0 /\ J + D >= 0 /\ -J + D + 1 >= 0 /\ C - 1 >= 0 /\ K + C - 2 >= 0 /\ -K + C >= 0 /\ J + C - 1 >= 0 /\ -J + C >= 0 /\ L - M >= 0 /\ -L + M >= 0 /\ -K + 1 >= 0 /\ J - K + 1 >= 0 /\ -J - K + 2 >= 0 /\ K >= 0 /\ J + K >= 0 /\ -J + K + 1 >= 0 /\ -J + 1 >= 0 /\ J >= 0 /\ N >= 1 /\ J >= 1 ] f26(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f41(H, K, C, D, E, F, G, H, I, J, K, L, M, 1, L, L, Q)) [ -H + 1 >= 0 /\ G - H + 1 >= 0 /\ F - H >= 0 /\ E - H + 1 >= 0 /\ D - H + 1 >= 0 /\ C - H >= 0 /\ K - H + 1 >= 0 /\ -K - H + 2 >= 0 /\ J - H + 1 >= 0 /\ -J - 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 /\ K + G >= 0 /\ -K + G + 1 >= 0 /\ J + G >= 0 /\ -J + G + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F - 2 >= 0 /\ K + F - 1 >= 0 /\ -K + F >= 0 /\ J + F - 1 >= 0 /\ -J + F >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ K + E >= 0 /\ -K + E + 1 >= 0 /\ J + E >= 0 /\ -J + E + 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ K + D >= 0 /\ -K + D + 1 >= 0 /\ J + D >= 0 /\ -J + D + 1 >= 0 /\ C - 1 >= 0 /\ K + C - 2 >= 0 /\ -K + C >= 0 /\ J + C - 1 >= 0 /\ -J + C >= 0 /\ L - M >= 0 /\ -L + M >= 0 /\ -K + 1 >= 0 /\ J - K + 1 >= 0 /\ -J - K + 2 >= 0 /\ K >= 0 /\ J + K >= 0 /\ -J + K + 1 >= 0 /\ -J + 1 >= 0 /\ J >= 0 /\ 0 >= N /\ J >= 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, O, O, Q)) [ -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 /\ N - H >= 0 /\ -N - H + 2 >= 0 /\ K - H + 1 >= 0 /\ -K - H + 2 >= 0 /\ J - H >= 0 /\ -J - 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 /\ N + G - 1 >= 0 /\ -N + G + 1 >= 0 /\ K + G >= 0 /\ -K + G + 1 >= 0 /\ J + G - 1 >= 0 /\ -J + G + 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F - 2 >= 0 /\ B + F - 1 >= 0 /\ -B + F >= 0 /\ N + F - 2 >= 0 /\ -N + F >= 0 /\ K + F - 1 >= 0 /\ -K + F >= 0 /\ J + F - 2 >= 0 /\ -J + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ B + E >= 0 /\ -B + E + 1 >= 0 /\ N + E - 1 >= 0 /\ -N + E + 1 >= 0 /\ K + E >= 0 /\ -K + E + 1 >= 0 /\ J + E - 1 >= 0 /\ -J + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ B + D >= 0 /\ -B + D + 1 >= 0 /\ N + D - 1 >= 0 /\ -N + D + 1 >= 0 /\ K + D >= 0 /\ -K + D + 1 >= 0 /\ J + D - 1 >= 0 /\ -J + D + 1 >= 0 /\ -A + D + 1 >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ -B + C >= 0 /\ N + C - 2 >= 0 /\ -N + C >= 0 /\ K + C - 2 >= 0 /\ -K + C >= 0 /\ J + C - 2 >= 0 /\ -J + C >= 0 /\ A + C - 2 >= 0 /\ -A + C >= 0 /\ -B + 1 >= 0 /\ N - B >= 0 /\ -N - B + 2 >= 0 /\ K - B >= 0 /\ -K - B + 2 >= 0 /\ J - B >= 0 /\ -J - B + 2 >= 0 /\ -A - B + 2 >= 0 /\ B >= 0 /\ N + B - 1 >= 0 /\ -N + B + 1 >= 0 /\ K + B >= 0 /\ -K + B >= 0 /\ J + B - 1 >= 0 /\ -J + B + 1 >= 0 /\ -A + B + 1 >= 0 /\ M - O >= 0 /\ L - O >= 0 /\ -M + O >= 0 /\ -L + O >= 0 /\ -N + 1 >= 0 /\ K - N + 1 >= 0 /\ -K - N + 2 >= 0 /\ J - N >= 0 /\ -J - N + 2 >= 0 /\ -A - N + 2 >= 0 /\ N - 1 >= 0 /\ K + N - 1 >= 0 /\ -K + N >= 0 /\ J + N - 2 >= 0 /\ -J + N >= 0 /\ -A + N >= 0 /\ L - M >= 0 /\ -L + M >= 0 /\ -K + 1 >= 0 /\ J - K >= 0 /\ -J - K + 2 >= 0 /\ -A - K + 2 >= 0 /\ K >= 0 /\ J + K - 1 >= 0 /\ -J + K + 1 >= 0 /\ -A + K + 1 >= 0 /\ -J + 1 >= 0 /\ -A - J + 2 >= 0 /\ J - 1 >= 0 /\ -A + J >= 0 /\ -A + 1 >= 0 /\ 0 >= A + 1 /\ O = P ] 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, O, O, Q)) [ -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 /\ N - H >= 0 /\ -N - H + 2 >= 0 /\ K - H + 1 >= 0 /\ -K - H + 2 >= 0 /\ J - H >= 0 /\ -J - 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 /\ N + G - 1 >= 0 /\ -N + G + 1 >= 0 /\ K + G >= 0 /\ -K + G + 1 >= 0 /\ J + G - 1 >= 0 /\ -J + G + 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F - 2 >= 0 /\ B + F - 1 >= 0 /\ -B + F >= 0 /\ N + F - 2 >= 0 /\ -N + F >= 0 /\ K + F - 1 >= 0 /\ -K + F >= 0 /\ J + F - 2 >= 0 /\ -J + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ B + E >= 0 /\ -B + E + 1 >= 0 /\ N + E - 1 >= 0 /\ -N + E + 1 >= 0 /\ K + E >= 0 /\ -K + E + 1 >= 0 /\ J + E - 1 >= 0 /\ -J + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ B + D >= 0 /\ -B + D + 1 >= 0 /\ N + D - 1 >= 0 /\ -N + D + 1 >= 0 /\ K + D >= 0 /\ -K + D + 1 >= 0 /\ J + D - 1 >= 0 /\ -J + D + 1 >= 0 /\ -A + D + 1 >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ -B + C >= 0 /\ N + C - 2 >= 0 /\ -N + C >= 0 /\ K + C - 2 >= 0 /\ -K + C >= 0 /\ J + C - 2 >= 0 /\ -J + C >= 0 /\ A + C - 2 >= 0 /\ -A + C >= 0 /\ -B + 1 >= 0 /\ N - B >= 0 /\ -N - B + 2 >= 0 /\ K - B >= 0 /\ -K - B + 2 >= 0 /\ J - B >= 0 /\ -J - B + 2 >= 0 /\ -A - B + 2 >= 0 /\ B >= 0 /\ N + B - 1 >= 0 /\ -N + B + 1 >= 0 /\ K + B >= 0 /\ -K + B >= 0 /\ J + B - 1 >= 0 /\ -J + B + 1 >= 0 /\ -A + B + 1 >= 0 /\ M - O >= 0 /\ L - O >= 0 /\ -M + O >= 0 /\ -L + O >= 0 /\ -N + 1 >= 0 /\ K - N + 1 >= 0 /\ -K - N + 2 >= 0 /\ J - N >= 0 /\ -J - N + 2 >= 0 /\ -A - N + 2 >= 0 /\ N - 1 >= 0 /\ K + N - 1 >= 0 /\ -K + N >= 0 /\ J + N - 2 >= 0 /\ -J + N >= 0 /\ -A + N >= 0 /\ L - M >= 0 /\ -L + M >= 0 /\ -K + 1 >= 0 /\ J - K >= 0 /\ -J - K + 2 >= 0 /\ -A - K + 2 >= 0 /\ K >= 0 /\ J + K - 1 >= 0 /\ -J + K + 1 >= 0 /\ -A + K + 1 >= 0 /\ -J + 1 >= 0 /\ -A - J + 2 >= 0 /\ J - 1 >= 0 /\ -A + J >= 0 /\ -A + 1 >= 0 /\ A >= 1 /\ O = P ] 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, O, O, Q)) [ -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 /\ N - H >= 0 /\ -N - H + 2 >= 0 /\ K - H + 1 >= 0 /\ -K - H + 2 >= 0 /\ J - H >= 0 /\ -J - 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 /\ N + G - 1 >= 0 /\ -N + G + 1 >= 0 /\ K + G >= 0 /\ -K + G + 1 >= 0 /\ J + G - 1 >= 0 /\ -J + G + 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F - 2 >= 0 /\ B + F - 1 >= 0 /\ -B + F >= 0 /\ N + F - 2 >= 0 /\ -N + F >= 0 /\ K + F - 1 >= 0 /\ -K + F >= 0 /\ J + F - 2 >= 0 /\ -J + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ B + E >= 0 /\ -B + E + 1 >= 0 /\ N + E - 1 >= 0 /\ -N + E + 1 >= 0 /\ K + E >= 0 /\ -K + E + 1 >= 0 /\ J + E - 1 >= 0 /\ -J + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ B + D >= 0 /\ -B + D + 1 >= 0 /\ N + D - 1 >= 0 /\ -N + D + 1 >= 0 /\ K + D >= 0 /\ -K + D + 1 >= 0 /\ J + D - 1 >= 0 /\ -J + D + 1 >= 0 /\ -A + D + 1 >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ -B + C >= 0 /\ N + C - 2 >= 0 /\ -N + C >= 0 /\ K + C - 2 >= 0 /\ -K + C >= 0 /\ J + C - 2 >= 0 /\ -J + C >= 0 /\ A + C - 2 >= 0 /\ -A + C >= 0 /\ -B + 1 >= 0 /\ N - B >= 0 /\ -N - B + 2 >= 0 /\ K - B >= 0 /\ -K - B + 2 >= 0 /\ J - B >= 0 /\ -J - B + 2 >= 0 /\ -A - B + 2 >= 0 /\ B >= 0 /\ N + B - 1 >= 0 /\ -N + B + 1 >= 0 /\ K + B >= 0 /\ -K + B >= 0 /\ J + B - 1 >= 0 /\ -J + B + 1 >= 0 /\ -A + B + 1 >= 0 /\ M - O >= 0 /\ L - O >= 0 /\ -M + O >= 0 /\ -L + O >= 0 /\ -N + 1 >= 0 /\ K - N + 1 >= 0 /\ -K - N + 2 >= 0 /\ J - N >= 0 /\ -J - N + 2 >= 0 /\ -A - N + 2 >= 0 /\ N - 1 >= 0 /\ K + N - 1 >= 0 /\ -K + N >= 0 /\ J + N - 2 >= 0 /\ -J + N >= 0 /\ -A + N >= 0 /\ L - M >= 0 /\ -L + M >= 0 /\ -K + 1 >= 0 /\ J - K >= 0 /\ -J - K + 2 >= 0 /\ -A - K + 2 >= 0 /\ K >= 0 /\ J + K - 1 >= 0 /\ -J + K + 1 >= 0 /\ -A + K + 1 >= 0 /\ -J + 1 >= 0 /\ -A - J + 2 >= 0 /\ J - 1 >= 0 /\ -A + J >= 0 /\ -A + 1 >= 0 /\ A = 0 /\ O = P ] 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, P, 1)) [ -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 /\ N - H >= 0 /\ -N - H + 2 >= 0 /\ K - H + 1 >= 0 /\ -K - H + 2 >= 0 /\ J - H >= 0 /\ -J - 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 /\ N + G - 1 >= 0 /\ -N + G + 1 >= 0 /\ K + G >= 0 /\ -K + G + 1 >= 0 /\ J + G - 1 >= 0 /\ -J + G + 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F - 2 >= 0 /\ B + F - 1 >= 0 /\ -B + F >= 0 /\ N + F - 2 >= 0 /\ -N + F >= 0 /\ K + F - 1 >= 0 /\ -K + F >= 0 /\ J + F - 2 >= 0 /\ -J + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ B + E >= 0 /\ -B + E + 1 >= 0 /\ N + E - 1 >= 0 /\ -N + E + 1 >= 0 /\ K + E >= 0 /\ -K + E + 1 >= 0 /\ J + E - 1 >= 0 /\ -J + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ B + D >= 0 /\ -B + D + 1 >= 0 /\ N + D - 1 >= 0 /\ -N + D + 1 >= 0 /\ K + D >= 0 /\ -K + D + 1 >= 0 /\ J + D - 1 >= 0 /\ -J + D + 1 >= 0 /\ -A + D + 1 >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ -B + C >= 0 /\ N + C - 2 >= 0 /\ -N + C >= 0 /\ K + C - 2 >= 0 /\ -K + C >= 0 /\ J + C - 2 >= 0 /\ -J + C >= 0 /\ A + C - 2 >= 0 /\ -A + C >= 0 /\ -B + 1 >= 0 /\ N - B >= 0 /\ -N - B + 2 >= 0 /\ K - B >= 0 /\ -K - B + 2 >= 0 /\ J - B >= 0 /\ -J - B + 2 >= 0 /\ -A - B + 2 >= 0 /\ B >= 0 /\ N + B - 1 >= 0 /\ -N + B + 1 >= 0 /\ K + B >= 0 /\ -K + B >= 0 /\ J + B - 1 >= 0 /\ -J + B + 1 >= 0 /\ -A + B + 1 >= 0 /\ O - P >= 0 /\ M - P >= 0 /\ L - P >= 0 /\ -O + P >= 0 /\ -M + P >= 0 /\ -L + P >= 0 /\ M - O >= 0 /\ L - O >= 0 /\ -M + O >= 0 /\ -L + O >= 0 /\ -N + 1 >= 0 /\ K - N + 1 >= 0 /\ -K - N + 2 >= 0 /\ J - N >= 0 /\ -J - N + 2 >= 0 /\ -A - N + 2 >= 0 /\ N - 1 >= 0 /\ K + N - 1 >= 0 /\ -K + N >= 0 /\ J + N - 2 >= 0 /\ -J + N >= 0 /\ -A + N >= 0 /\ L - M >= 0 /\ -L + M >= 0 /\ -K + 1 >= 0 /\ J - K >= 0 /\ -J - K + 2 >= 0 /\ -A - K + 2 >= 0 /\ K >= 0 /\ J + K - 1 >= 0 /\ -J + K + 1 >= 0 /\ -A + K + 1 >= 0 /\ -J + 1 >= 0 /\ -A - J + 2 >= 0 /\ J - 1 >= 0 /\ -A + J >= 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)) [ -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 /\ N - H >= 0 /\ -N - H + 2 >= 0 /\ K - H + 1 >= 0 /\ -K - H + 2 >= 0 /\ J - H >= 0 /\ -J - 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 /\ N + G - 1 >= 0 /\ -N + G + 1 >= 0 /\ K + G >= 0 /\ -K + G + 1 >= 0 /\ J + G - 1 >= 0 /\ -J + G + 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F - 2 >= 0 /\ B + F - 1 >= 0 /\ -B + F >= 0 /\ N + F - 2 >= 0 /\ -N + F >= 0 /\ K + F - 1 >= 0 /\ -K + F >= 0 /\ J + F - 2 >= 0 /\ -J + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ B + E >= 0 /\ -B + E + 1 >= 0 /\ N + E - 1 >= 0 /\ -N + E + 1 >= 0 /\ K + E >= 0 /\ -K + E + 1 >= 0 /\ J + E - 1 >= 0 /\ -J + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ B + D >= 0 /\ -B + D + 1 >= 0 /\ N + D - 1 >= 0 /\ -N + D + 1 >= 0 /\ K + D >= 0 /\ -K + D + 1 >= 0 /\ J + D - 1 >= 0 /\ -J + D + 1 >= 0 /\ -A + D + 1 >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ -B + C >= 0 /\ N + C - 2 >= 0 /\ -N + C >= 0 /\ K + C - 2 >= 0 /\ -K + C >= 0 /\ J + C - 2 >= 0 /\ -J + C >= 0 /\ A + C - 2 >= 0 /\ -A + C >= 0 /\ -B + 1 >= 0 /\ N - B >= 0 /\ -N - B + 2 >= 0 /\ K - B >= 0 /\ -K - B + 2 >= 0 /\ J - B >= 0 /\ -J - B + 2 >= 0 /\ -A - B + 2 >= 0 /\ B >= 0 /\ N + B - 1 >= 0 /\ -N + B + 1 >= 0 /\ K + B >= 0 /\ -K + B >= 0 /\ J + B - 1 >= 0 /\ -J + B + 1 >= 0 /\ -A + B + 1 >= 0 /\ O - P >= 0 /\ M - P >= 0 /\ L - P >= 0 /\ -O + P >= 0 /\ -M + P >= 0 /\ -L + P >= 0 /\ M - O >= 0 /\ L - O >= 0 /\ -M + O >= 0 /\ -L + O >= 0 /\ -N + 1 >= 0 /\ K - N + 1 >= 0 /\ -K - N + 2 >= 0 /\ J - N >= 0 /\ -J - N + 2 >= 0 /\ -A - N + 2 >= 0 /\ N - 1 >= 0 /\ K + N - 1 >= 0 /\ -K + N >= 0 /\ J + N - 2 >= 0 /\ -J + N >= 0 /\ -A + N >= 0 /\ L - M >= 0 /\ -L + M >= 0 /\ -K + 1 >= 0 /\ J - K >= 0 /\ -J - K + 2 >= 0 /\ -A - K + 2 >= 0 /\ K >= 0 /\ J + K - 1 >= 0 /\ -J + K + 1 >= 0 /\ -A + K + 1 >= 0 /\ -J + 1 >= 0 /\ -A - J + 2 >= 0 /\ J - 1 >= 0 /\ -A + J >= 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, P, 2)) [ -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 /\ N - H >= 0 /\ -N - H + 2 >= 0 /\ K - H >= 0 /\ -K - H + 2 >= 0 /\ J - H >= 0 /\ -J - 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 /\ N + G - 1 >= 0 /\ -N + G + 1 >= 0 /\ K + G - 1 >= 0 /\ -K + G + 1 >= 0 /\ J + G - 1 >= 0 /\ -J + G + 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F - 2 >= 0 /\ B + F - 1 >= 0 /\ -B + F >= 0 /\ N + F - 2 >= 0 /\ -N + F >= 0 /\ K + F - 1 >= 0 /\ -K + F >= 0 /\ J + F - 2 >= 0 /\ -J + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ B + E >= 0 /\ -B + E + 1 >= 0 /\ N + E - 1 >= 0 /\ -N + E + 1 >= 0 /\ K + E >= 0 /\ -K + E + 1 >= 0 /\ J + E - 1 >= 0 /\ -J + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ B + D >= 0 /\ -B + D + 1 >= 0 /\ N + D - 1 >= 0 /\ -N + D + 1 >= 0 /\ K + D >= 0 /\ -K + D + 1 >= 0 /\ J + D - 1 >= 0 /\ -J + D + 1 >= 0 /\ -A + D + 1 >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ -B + C >= 0 /\ N + C - 2 >= 0 /\ -N + C >= 0 /\ K + C - 2 >= 0 /\ -K + C >= 0 /\ J + C - 2 >= 0 /\ -J + C >= 0 /\ A + C - 2 >= 0 /\ -A + C >= 0 /\ -B + 1 >= 0 /\ N - B >= 0 /\ -N - B + 2 >= 0 /\ K - B >= 0 /\ -K - B + 2 >= 0 /\ J - B >= 0 /\ -J - B + 2 >= 0 /\ -A - B + 2 >= 0 /\ B >= 0 /\ N + B - 1 >= 0 /\ -N + B + 1 >= 0 /\ K + B >= 0 /\ -K + B >= 0 /\ J + B - 1 >= 0 /\ -J + B + 1 >= 0 /\ -A + B >= 0 /\ O - P >= 0 /\ M - P >= 0 /\ L - P >= 0 /\ -O + P >= 0 /\ -M + P >= 0 /\ -L + P >= 0 /\ M - O >= 0 /\ L - O >= 0 /\ -M + O >= 0 /\ -L + O >= 0 /\ -N + 1 >= 0 /\ K - N + 1 >= 0 /\ -K - N + 2 >= 0 /\ J - N >= 0 /\ -J - N + 2 >= 0 /\ -A - N + 2 >= 0 /\ N - 1 >= 0 /\ K + N - 1 >= 0 /\ -K + N >= 0 /\ J + N - 2 >= 0 /\ -J + N >= 0 /\ -A + N >= 0 /\ L - M >= 0 /\ -L + M >= 0 /\ -K + 1 >= 0 /\ J - K >= 0 /\ -J - K + 2 >= 0 /\ -A - K + 2 >= 0 /\ K >= 0 /\ J + K - 1 >= 0 /\ -J + K + 1 >= 0 /\ -A + K >= 0 /\ -J + 1 >= 0 /\ -A - J + 2 >= 0 /\ J - 1 >= 0 /\ -A + J >= 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)) [ -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 /\ N - H >= 0 /\ -N - H + 2 >= 0 /\ K - H >= 0 /\ -K - H + 2 >= 0 /\ J - H >= 0 /\ -J - 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 /\ N + G - 1 >= 0 /\ -N + G + 1 >= 0 /\ K + G - 1 >= 0 /\ -K + G + 1 >= 0 /\ J + G - 1 >= 0 /\ -J + G + 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F - 2 >= 0 /\ B + F - 1 >= 0 /\ -B + F >= 0 /\ N + F - 2 >= 0 /\ -N + F >= 0 /\ K + F - 1 >= 0 /\ -K + F >= 0 /\ J + F - 2 >= 0 /\ -J + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ B + E >= 0 /\ -B + E + 1 >= 0 /\ N + E - 1 >= 0 /\ -N + E + 1 >= 0 /\ K + E >= 0 /\ -K + E + 1 >= 0 /\ J + E - 1 >= 0 /\ -J + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ B + D >= 0 /\ -B + D + 1 >= 0 /\ N + D - 1 >= 0 /\ -N + D + 1 >= 0 /\ K + D >= 0 /\ -K + D + 1 >= 0 /\ J + D - 1 >= 0 /\ -J + D + 1 >= 0 /\ -A + D + 1 >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ -B + C >= 0 /\ N + C - 2 >= 0 /\ -N + C >= 0 /\ K + C - 2 >= 0 /\ -K + C >= 0 /\ J + C - 2 >= 0 /\ -J + C >= 0 /\ A + C - 2 >= 0 /\ -A + C >= 0 /\ -B + 1 >= 0 /\ N - B >= 0 /\ -N - B + 2 >= 0 /\ K - B >= 0 /\ -K - B + 2 >= 0 /\ J - B >= 0 /\ -J - B + 2 >= 0 /\ -A - B + 2 >= 0 /\ B >= 0 /\ N + B - 1 >= 0 /\ -N + B + 1 >= 0 /\ K + B >= 0 /\ -K + B >= 0 /\ J + B - 1 >= 0 /\ -J + B + 1 >= 0 /\ -A + B >= 0 /\ O - P >= 0 /\ M - P >= 0 /\ L - P >= 0 /\ -O + P >= 0 /\ -M + P >= 0 /\ -L + P >= 0 /\ M - O >= 0 /\ L - O >= 0 /\ -M + O >= 0 /\ -L + O >= 0 /\ -N + 1 >= 0 /\ K - N + 1 >= 0 /\ -K - N + 2 >= 0 /\ J - N >= 0 /\ -J - N + 2 >= 0 /\ -A - N + 2 >= 0 /\ N - 1 >= 0 /\ K + N - 1 >= 0 /\ -K + N >= 0 /\ J + N - 2 >= 0 /\ -J + N >= 0 /\ -A + N >= 0 /\ L - M >= 0 /\ -L + M >= 0 /\ -K + 1 >= 0 /\ J - K >= 0 /\ -J - K + 2 >= 0 /\ -A - K + 2 >= 0 /\ K >= 0 /\ J + K - 1 >= 0 /\ -J + K + 1 >= 0 /\ -A + K >= 0 /\ -J + 1 >= 0 /\ -A - J + 2 >= 0 /\ J - 1 >= 0 /\ -A + J >= 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, P, 3)) [ -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 /\ N - H >= 0 /\ -N - H + 2 >= 0 /\ K - H >= 0 /\ -K - H + 2 >= 0 /\ J - H >= 0 /\ -J - 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 /\ N + G - 1 >= 0 /\ -N + G + 1 >= 0 /\ K + G - 1 >= 0 /\ -K + G + 1 >= 0 /\ J + G - 1 >= 0 /\ -J + G + 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F - 2 >= 0 /\ B + F - 2 >= 0 /\ -B + F >= 0 /\ N + F - 2 >= 0 /\ -N + F >= 0 /\ K + F - 2 >= 0 /\ -K + F >= 0 /\ J + F - 2 >= 0 /\ -J + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ B + E - 1 >= 0 /\ -B + E + 1 >= 0 /\ N + E - 1 >= 0 /\ -N + E + 1 >= 0 /\ K + E - 1 >= 0 /\ -K + E + 1 >= 0 /\ J + E - 1 >= 0 /\ -J + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ B + D - 1 >= 0 /\ -B + D + 1 >= 0 /\ N + D - 1 >= 0 /\ -N + D + 1 >= 0 /\ K + D - 1 >= 0 /\ -K + D + 1 >= 0 /\ J + D - 1 >= 0 /\ -J + D + 1 >= 0 /\ -A + D + 1 >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ -B + C >= 0 /\ N + C - 2 >= 0 /\ -N + C >= 0 /\ K + C - 2 >= 0 /\ -K + C >= 0 /\ J + C - 2 >= 0 /\ -J + C >= 0 /\ A + C - 2 >= 0 /\ -A + C >= 0 /\ -B + 1 >= 0 /\ N - B >= 0 /\ -N - B + 2 >= 0 /\ K - B >= 0 /\ -K - B + 2 >= 0 /\ J - B >= 0 /\ -J - B + 2 >= 0 /\ -A - B + 2 >= 0 /\ B - 1 >= 0 /\ N + B - 2 >= 0 /\ -N + B >= 0 /\ K + B - 2 >= 0 /\ -K + B >= 0 /\ J + B - 2 >= 0 /\ -J + B >= 0 /\ -A + B >= 0 /\ O - P >= 0 /\ M - P >= 0 /\ L - P >= 0 /\ -O + P >= 0 /\ -M + P >= 0 /\ -L + P >= 0 /\ M - O >= 0 /\ L - O >= 0 /\ -M + O >= 0 /\ -L + O >= 0 /\ -N + 1 >= 0 /\ K - N >= 0 /\ -K - N + 2 >= 0 /\ J - N >= 0 /\ -J - N + 2 >= 0 /\ -A - N + 2 >= 0 /\ N - 1 >= 0 /\ K + N - 2 >= 0 /\ -K + N >= 0 /\ J + N - 2 >= 0 /\ -J + N >= 0 /\ -A + N >= 0 /\ L - M >= 0 /\ -L + M >= 0 /\ -K + 1 >= 0 /\ J - K >= 0 /\ -J - K + 2 >= 0 /\ -A - K + 2 >= 0 /\ K - 1 >= 0 /\ J + K - 2 >= 0 /\ -J + K >= 0 /\ -A + K >= 0 /\ -J + 1 >= 0 /\ -A - J + 2 >= 0 /\ J - 1 >= 0 /\ -A + J >= 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, R, J, K, L, 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 /\ B - H + 1 >= 0 /\ -B - H + 2 >= 0 /\ N - H >= 0 /\ -N - H + 2 >= 0 /\ K - H + 1 >= 0 /\ -K - H + 2 >= 0 /\ J - H >= 0 /\ -J - 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 /\ N + G - 1 >= 0 /\ -N + G + 1 >= 0 /\ K + G >= 0 /\ -K + G + 1 >= 0 /\ J + G - 1 >= 0 /\ -J + G + 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F - 2 >= 0 /\ B + F - 1 >= 0 /\ -B + F >= 0 /\ N + F - 2 >= 0 /\ -N + F >= 0 /\ K + F - 1 >= 0 /\ -K + F >= 0 /\ J + F - 2 >= 0 /\ -J + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ B + E >= 0 /\ -B + E + 1 >= 0 /\ N + E - 1 >= 0 /\ -N + E + 1 >= 0 /\ K + E >= 0 /\ -K + E + 1 >= 0 /\ J + E - 1 >= 0 /\ -J + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ B + D >= 0 /\ -B + D + 1 >= 0 /\ N + D - 1 >= 0 /\ -N + D + 1 >= 0 /\ K + D >= 0 /\ -K + D + 1 >= 0 /\ J + D - 1 >= 0 /\ -J + D + 1 >= 0 /\ -A + D + 1 >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ -B + C >= 0 /\ N + C - 2 >= 0 /\ -N + C >= 0 /\ K + C - 2 >= 0 /\ -K + C >= 0 /\ J + C - 2 >= 0 /\ -J + C >= 0 /\ A + C - 2 >= 0 /\ -A + C >= 0 /\ -B + 1 >= 0 /\ N - B >= 0 /\ -N - B + 2 >= 0 /\ K - B >= 0 /\ -K - B + 2 >= 0 /\ J - B >= 0 /\ -J - B + 2 >= 0 /\ -A - B + 2 >= 0 /\ B >= 0 /\ N + B - 1 >= 0 /\ -N + B + 1 >= 0 /\ K + B >= 0 /\ -K + B >= 0 /\ J + B - 1 >= 0 /\ -J + B + 1 >= 0 /\ -A + B + 1 >= 0 /\ M - O >= 0 /\ L - O >= 0 /\ -M + O >= 0 /\ -L + O >= 0 /\ -N + 1 >= 0 /\ K - N + 1 >= 0 /\ -K - N + 2 >= 0 /\ J - N >= 0 /\ -J - N + 2 >= 0 /\ -A - N + 2 >= 0 /\ N - 1 >= 0 /\ K + N - 1 >= 0 /\ -K + N >= 0 /\ J + N - 2 >= 0 /\ -J + N >= 0 /\ -A + N >= 0 /\ L - M >= 0 /\ -L + M >= 0 /\ -K + 1 >= 0 /\ J - K >= 0 /\ -J - K + 2 >= 0 /\ -A - K + 2 >= 0 /\ K >= 0 /\ J + K - 1 >= 0 /\ -J + K + 1 >= 0 /\ -A + K + 1 >= 0 /\ -J + 1 >= 0 /\ -A - J + 2 >= 0 /\ J - 1 >= 0 /\ -A + J >= 0 /\ -A + 1 >= 0 /\ R >= 0 /\ O >= P + 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, R, J, K, L, 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 /\ B - H + 1 >= 0 /\ -B - H + 2 >= 0 /\ N - H >= 0 /\ -N - H + 2 >= 0 /\ K - H + 1 >= 0 /\ -K - H + 2 >= 0 /\ J - H >= 0 /\ -J - 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 /\ N + G - 1 >= 0 /\ -N + G + 1 >= 0 /\ K + G >= 0 /\ -K + G + 1 >= 0 /\ J + G - 1 >= 0 /\ -J + G + 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F - 2 >= 0 /\ B + F - 1 >= 0 /\ -B + F >= 0 /\ N + F - 2 >= 0 /\ -N + F >= 0 /\ K + F - 1 >= 0 /\ -K + F >= 0 /\ J + F - 2 >= 0 /\ -J + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ B + E >= 0 /\ -B + E + 1 >= 0 /\ N + E - 1 >= 0 /\ -N + E + 1 >= 0 /\ K + E >= 0 /\ -K + E + 1 >= 0 /\ J + E - 1 >= 0 /\ -J + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ B + D >= 0 /\ -B + D + 1 >= 0 /\ N + D - 1 >= 0 /\ -N + D + 1 >= 0 /\ K + D >= 0 /\ -K + D + 1 >= 0 /\ J + D - 1 >= 0 /\ -J + D + 1 >= 0 /\ -A + D + 1 >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ -B + C >= 0 /\ N + C - 2 >= 0 /\ -N + C >= 0 /\ K + C - 2 >= 0 /\ -K + C >= 0 /\ J + C - 2 >= 0 /\ -J + C >= 0 /\ A + C - 2 >= 0 /\ -A + C >= 0 /\ -B + 1 >= 0 /\ N - B >= 0 /\ -N - B + 2 >= 0 /\ K - B >= 0 /\ -K - B + 2 >= 0 /\ J - B >= 0 /\ -J - B + 2 >= 0 /\ -A - B + 2 >= 0 /\ B >= 0 /\ N + B - 1 >= 0 /\ -N + B + 1 >= 0 /\ K + B >= 0 /\ -K + B >= 0 /\ J + B - 1 >= 0 /\ -J + B + 1 >= 0 /\ -A + B + 1 >= 0 /\ M - O >= 0 /\ L - O >= 0 /\ -M + O >= 0 /\ -L + O >= 0 /\ -N + 1 >= 0 /\ K - N + 1 >= 0 /\ -K - N + 2 >= 0 /\ J - N >= 0 /\ -J - N + 2 >= 0 /\ -A - N + 2 >= 0 /\ N - 1 >= 0 /\ K + N - 1 >= 0 /\ -K + N >= 0 /\ J + N - 2 >= 0 /\ -J + N >= 0 /\ -A + N >= 0 /\ L - M >= 0 /\ -L + M >= 0 /\ -K + 1 >= 0 /\ J - K >= 0 /\ -J - K + 2 >= 0 /\ -A - K + 2 >= 0 /\ K >= 0 /\ J + K - 1 >= 0 /\ -J + K + 1 >= 0 /\ -A + K + 1 >= 0 /\ -J + 1 >= 0 /\ -A - J + 2 >= 0 /\ J - 1 >= 0 /\ -A + J >= 0 /\ -A + 1 >= 0 /\ R >= 0 /\ P >= 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, R, J, K, L, M, N, O, 0, Q)) [ -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 >= 0 /\ -Q - H + 4 >= 0 /\ N - H >= 0 /\ -N - H + 2 >= 0 /\ K - H + 1 >= 0 /\ -K - H + 2 >= 0 /\ J - H >= 0 /\ -J - 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 - 1 >= 0 /\ -Q + G + 3 >= 0 /\ N + G - 1 >= 0 /\ -N + G + 1 >= 0 /\ K + G >= 0 /\ -K + G + 1 >= 0 /\ J + G - 1 >= 0 /\ -J + G + 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 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 - 2 >= 0 /\ -Q + F + 2 >= 0 /\ N + F - 2 >= 0 /\ -N + F >= 0 /\ K + F - 1 >= 0 /\ -K + F >= 0 /\ J + F - 2 >= 0 /\ -J + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ B + E >= 0 /\ -B + E + 1 >= 0 /\ Q + E - 1 >= 0 /\ -Q + E + 3 >= 0 /\ N + E - 1 >= 0 /\ -N + E + 1 >= 0 /\ K + E >= 0 /\ -K + E + 1 >= 0 /\ J + E - 1 >= 0 /\ -J + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ B + D >= 0 /\ -B + D + 1 >= 0 /\ Q + D - 1 >= 0 /\ -Q + D + 3 >= 0 /\ N + D - 1 >= 0 /\ -N + D + 1 >= 0 /\ K + D >= 0 /\ -K + D + 1 >= 0 /\ J + D - 1 >= 0 /\ -J + D + 1 >= 0 /\ -A + D + 1 >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ -B + C >= 0 /\ Q + C - 3 >= 0 /\ -Q + C + 2 >= 0 /\ N + C - 2 >= 0 /\ -N + C >= 0 /\ K + C - 2 >= 0 /\ -K + C >= 0 /\ J + C - 2 >= 0 /\ -J + C >= 0 /\ A + C - 2 >= 0 /\ -A + C >= 0 /\ -B + 1 >= 0 /\ Q - B - 1 >= 0 /\ -Q - B + 4 >= 0 /\ N - B >= 0 /\ -N - B + 2 >= 0 /\ K - B >= 0 /\ -K - B + 2 >= 0 /\ J - B >= 0 /\ -J - B + 2 >= 0 /\ -A - B + 2 >= 0 /\ B >= 0 /\ Q + B - 1 >= 0 /\ -Q + B + 2 >= 0 /\ N + B - 1 >= 0 /\ -N + B + 1 >= 0 /\ K + B >= 0 /\ -K + B >= 0 /\ J + B - 1 >= 0 /\ -J + B + 1 >= 0 /\ -A + B + 1 >= 0 /\ -Q + 3 >= 0 /\ N - Q + 2 >= 0 /\ -N - Q + 4 >= 0 /\ K - Q + 2 >= 0 /\ -K - Q + 4 >= 0 /\ J - Q + 2 >= 0 /\ -J - Q + 4 >= 0 /\ -A - Q + 4 >= 0 /\ Q - 1 >= 0 /\ N + Q - 2 >= 0 /\ -N + Q >= 0 /\ K + Q - 1 >= 0 /\ -K + Q - 1 >= 0 /\ J + Q - 2 >= 0 /\ -J + Q >= 0 /\ -A + Q >= 0 /\ O - P >= 0 /\ M - P >= 0 /\ L - P >= 0 /\ -O + P >= 0 /\ -M + P >= 0 /\ -L + P >= 0 /\ M - O >= 0 /\ L - O >= 0 /\ -M + O >= 0 /\ -L + O >= 0 /\ -N + 1 >= 0 /\ K - N + 1 >= 0 /\ -K - N + 2 >= 0 /\ J - N >= 0 /\ -J - N + 2 >= 0 /\ -A - N + 2 >= 0 /\ N - 1 >= 0 /\ K + N - 1 >= 0 /\ -K + N >= 0 /\ J + N - 2 >= 0 /\ -J + N >= 0 /\ -A + N >= 0 /\ L - M >= 0 /\ -L + M >= 0 /\ -K + 1 >= 0 /\ J - K >= 0 /\ -J - K + 2 >= 0 /\ -A - K + 2 >= 0 /\ K >= 0 /\ J + K - 1 >= 0 /\ -J + K + 1 >= 0 /\ -A + K + 1 >= 0 /\ -J + 1 >= 0 /\ -A - J + 2 >= 0 /\ J - 1 >= 0 /\ -A + J >= 0 /\ -A + 1 >= 0 /\ R >= 0 /\ P >= 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, R, J, K, L, M, N, O, 1, Q)) [ -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 >= 0 /\ -Q - H + 4 >= 0 /\ N - H >= 0 /\ -N - H + 2 >= 0 /\ K - H + 1 >= 0 /\ -K - H + 2 >= 0 /\ J - H >= 0 /\ -J - 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 - 1 >= 0 /\ -Q + G + 3 >= 0 /\ N + G - 1 >= 0 /\ -N + G + 1 >= 0 /\ K + G >= 0 /\ -K + G + 1 >= 0 /\ J + G - 1 >= 0 /\ -J + G + 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 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 - 2 >= 0 /\ -Q + F + 2 >= 0 /\ N + F - 2 >= 0 /\ -N + F >= 0 /\ K + F - 1 >= 0 /\ -K + F >= 0 /\ J + F - 2 >= 0 /\ -J + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ B + E >= 0 /\ -B + E + 1 >= 0 /\ Q + E - 1 >= 0 /\ -Q + E + 3 >= 0 /\ N + E - 1 >= 0 /\ -N + E + 1 >= 0 /\ K + E >= 0 /\ -K + E + 1 >= 0 /\ J + E - 1 >= 0 /\ -J + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ B + D >= 0 /\ -B + D + 1 >= 0 /\ Q + D - 1 >= 0 /\ -Q + D + 3 >= 0 /\ N + D - 1 >= 0 /\ -N + D + 1 >= 0 /\ K + D >= 0 /\ -K + D + 1 >= 0 /\ J + D - 1 >= 0 /\ -J + D + 1 >= 0 /\ -A + D + 1 >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ -B + C >= 0 /\ Q + C - 3 >= 0 /\ -Q + C + 2 >= 0 /\ N + C - 2 >= 0 /\ -N + C >= 0 /\ K + C - 2 >= 0 /\ -K + C >= 0 /\ J + C - 2 >= 0 /\ -J + C >= 0 /\ A + C - 2 >= 0 /\ -A + C >= 0 /\ -B + 1 >= 0 /\ Q - B - 1 >= 0 /\ -Q - B + 4 >= 0 /\ N - B >= 0 /\ -N - B + 2 >= 0 /\ K - B >= 0 /\ -K - B + 2 >= 0 /\ J - B >= 0 /\ -J - B + 2 >= 0 /\ -A - B + 2 >= 0 /\ B >= 0 /\ Q + B - 1 >= 0 /\ -Q + B + 2 >= 0 /\ N + B - 1 >= 0 /\ -N + B + 1 >= 0 /\ K + B >= 0 /\ -K + B >= 0 /\ J + B - 1 >= 0 /\ -J + B + 1 >= 0 /\ -A + B + 1 >= 0 /\ -Q + 3 >= 0 /\ N - Q + 2 >= 0 /\ -N - Q + 4 >= 0 /\ K - Q + 2 >= 0 /\ -K - Q + 4 >= 0 /\ J - Q + 2 >= 0 /\ -J - Q + 4 >= 0 /\ -A - Q + 4 >= 0 /\ Q - 1 >= 0 /\ N + Q - 2 >= 0 /\ -N + Q >= 0 /\ K + Q - 1 >= 0 /\ -K + Q - 1 >= 0 /\ J + Q - 2 >= 0 /\ -J + Q >= 0 /\ -A + Q >= 0 /\ O - P >= 0 /\ M - P >= 0 /\ L - P >= 0 /\ -O + P >= 0 /\ -M + P >= 0 /\ -L + P >= 0 /\ M - O >= 0 /\ L - O >= 0 /\ -M + O >= 0 /\ -L + O >= 0 /\ -N + 1 >= 0 /\ K - N + 1 >= 0 /\ -K - N + 2 >= 0 /\ J - N >= 0 /\ -J - N + 2 >= 0 /\ -A - N + 2 >= 0 /\ N - 1 >= 0 /\ K + N - 1 >= 0 /\ -K + N >= 0 /\ J + N - 2 >= 0 /\ -J + N >= 0 /\ -A + N >= 0 /\ L - M >= 0 /\ -L + M >= 0 /\ -K + 1 >= 0 /\ J - K >= 0 /\ -J - K + 2 >= 0 /\ -A - K + 2 >= 0 /\ K >= 0 /\ J + K - 1 >= 0 /\ -J + K + 1 >= 0 /\ -A + K + 1 >= 0 /\ -J + 1 >= 0 /\ -A - J + 2 >= 0 /\ J - 1 >= 0 /\ -A + J >= 0 /\ -A + 1 >= 0 /\ R >= 0 /\ 0 >= P /\ 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 + 1 >= 0 /\ -B - I + 2 >= 0 /\ N - I >= 0 /\ -N - I + 2 >= 0 /\ K - I + 1 >= 0 /\ -K - I + 2 >= 0 /\ J - I >= 0 /\ -J - 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 - 1 >= 0 /\ B + I >= 0 /\ -B + I + 1 >= 0 /\ N + I - 1 >= 0 /\ -N + I + 1 >= 0 /\ K + I >= 0 /\ -K + I + 1 >= 0 /\ J + I - 1 >= 0 /\ -J + 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 /\ N - H >= 0 /\ -N - H + 2 >= 0 /\ K - H + 1 >= 0 /\ -K - H + 2 >= 0 /\ J - H >= 0 /\ -J - 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 /\ N + G - 1 >= 0 /\ -N + G + 1 >= 0 /\ K + G >= 0 /\ -K + G + 1 >= 0 /\ J + G - 1 >= 0 /\ -J + G + 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F - 2 >= 0 /\ B + F - 1 >= 0 /\ -B + F >= 0 /\ N + F - 2 >= 0 /\ -N + F >= 0 /\ K + F - 1 >= 0 /\ -K + F >= 0 /\ J + F - 2 >= 0 /\ -J + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ B + E >= 0 /\ -B + E + 1 >= 0 /\ N + E - 1 >= 0 /\ -N + E + 1 >= 0 /\ K + E >= 0 /\ -K + E + 1 >= 0 /\ J + E - 1 >= 0 /\ -J + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ B + D >= 0 /\ -B + D + 1 >= 0 /\ N + D - 1 >= 0 /\ -N + D + 1 >= 0 /\ K + D >= 0 /\ -K + D + 1 >= 0 /\ J + D - 1 >= 0 /\ -J + D + 1 >= 0 /\ -A + D + 1 >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ -B + C >= 0 /\ N + C - 2 >= 0 /\ -N + C >= 0 /\ K + C - 2 >= 0 /\ -K + C >= 0 /\ J + C - 2 >= 0 /\ -J + C >= 0 /\ A + C - 2 >= 0 /\ -A + C >= 0 /\ -B + 1 >= 0 /\ N - B >= 0 /\ -N - B + 2 >= 0 /\ K - B >= 0 /\ -K - B + 2 >= 0 /\ J - B >= 0 /\ -J - B + 2 >= 0 /\ -A - B + 2 >= 0 /\ B >= 0 /\ N + B - 1 >= 0 /\ -N + B + 1 >= 0 /\ K + B >= 0 /\ -K + B >= 0 /\ J + B - 1 >= 0 /\ -J + B + 1 >= 0 /\ -A + B + 1 >= 0 /\ M - O >= 0 /\ L - O >= 0 /\ -M + O >= 0 /\ -L + O >= 0 /\ -N + 1 >= 0 /\ K - N + 1 >= 0 /\ -K - N + 2 >= 0 /\ J - N >= 0 /\ -J - N + 2 >= 0 /\ -A - N + 2 >= 0 /\ N - 1 >= 0 /\ K + N - 1 >= 0 /\ -K + N >= 0 /\ J + N - 2 >= 0 /\ -J + N >= 0 /\ -A + N >= 0 /\ L - M >= 0 /\ -L + M >= 0 /\ -K + 1 >= 0 /\ J - K >= 0 /\ -J - K + 2 >= 0 /\ -A - K + 2 >= 0 /\ K >= 0 /\ J + K - 1 >= 0 /\ -J + K + 1 >= 0 /\ -A + K + 1 >= 0 /\ -J + 1 >= 0 /\ -A - J + 2 >= 0 /\ J - 1 >= 0 /\ -A + J >= 0 /\ -A + 1 >= 0 /\ 0 >= E /\ 0 >= D /\ I >= 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 + 1 >= 0 /\ -B - I + 2 >= 0 /\ N - I >= 0 /\ -N - I + 2 >= 0 /\ K - I + 1 >= 0 /\ -K - I + 2 >= 0 /\ J - I >= 0 /\ -J - 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 - 1 >= 0 /\ B + I >= 0 /\ -B + I + 1 >= 0 /\ N + I - 1 >= 0 /\ -N + I + 1 >= 0 /\ K + I >= 0 /\ -K + I + 1 >= 0 /\ J + I - 1 >= 0 /\ -J + 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 /\ N - H >= 0 /\ -N - H + 2 >= 0 /\ K - H + 1 >= 0 /\ -K - H + 2 >= 0 /\ J - H >= 0 /\ -J - 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 /\ N + G - 1 >= 0 /\ -N + G + 1 >= 0 /\ K + G >= 0 /\ -K + G + 1 >= 0 /\ J + G - 1 >= 0 /\ -J + G + 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F - 2 >= 0 /\ B + F - 1 >= 0 /\ -B + F >= 0 /\ N + F - 2 >= 0 /\ -N + F >= 0 /\ K + F - 1 >= 0 /\ -K + F >= 0 /\ J + F - 2 >= 0 /\ -J + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ B + E >= 0 /\ -B + E + 1 >= 0 /\ N + E - 1 >= 0 /\ -N + E + 1 >= 0 /\ K + E >= 0 /\ -K + E + 1 >= 0 /\ J + E - 1 >= 0 /\ -J + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ B + D >= 0 /\ -B + D + 1 >= 0 /\ N + D - 1 >= 0 /\ -N + D + 1 >= 0 /\ K + D >= 0 /\ -K + D + 1 >= 0 /\ J + D - 1 >= 0 /\ -J + D + 1 >= 0 /\ -A + D + 1 >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ -B + C >= 0 /\ N + C - 2 >= 0 /\ -N + C >= 0 /\ K + C - 2 >= 0 /\ -K + C >= 0 /\ J + C - 2 >= 0 /\ -J + C >= 0 /\ A + C - 2 >= 0 /\ -A + C >= 0 /\ -B + 1 >= 0 /\ N - B >= 0 /\ -N - B + 2 >= 0 /\ K - B >= 0 /\ -K - B + 2 >= 0 /\ J - B >= 0 /\ -J - B + 2 >= 0 /\ -A - B + 2 >= 0 /\ B >= 0 /\ N + B - 1 >= 0 /\ -N + B + 1 >= 0 /\ K + B >= 0 /\ -K + B >= 0 /\ J + B - 1 >= 0 /\ -J + B + 1 >= 0 /\ -A + B + 1 >= 0 /\ M - O >= 0 /\ L - O >= 0 /\ -M + O >= 0 /\ -L + O >= 0 /\ -N + 1 >= 0 /\ K - N + 1 >= 0 /\ -K - N + 2 >= 0 /\ J - N >= 0 /\ -J - N + 2 >= 0 /\ -A - N + 2 >= 0 /\ N - 1 >= 0 /\ K + N - 1 >= 0 /\ -K + N >= 0 /\ J + N - 2 >= 0 /\ -J + N >= 0 /\ -A + N >= 0 /\ L - M >= 0 /\ -L + M >= 0 /\ -K + 1 >= 0 /\ J - K >= 0 /\ -J - K + 2 >= 0 /\ -A - K + 2 >= 0 /\ K >= 0 /\ J + K - 1 >= 0 /\ -J + K + 1 >= 0 /\ -A + K + 1 >= 0 /\ -J + 1 >= 0 /\ -A - J + 2 >= 0 /\ J - 1 >= 0 /\ -A + J >= 0 /\ -A + 1 >= 0 /\ 0 >= D /\ I >= 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 + 1 >= 0 /\ -B - I + 2 >= 0 /\ N - I >= 0 /\ -N - I + 2 >= 0 /\ K - I + 1 >= 0 /\ -K - I + 2 >= 0 /\ J - I >= 0 /\ -J - 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 - 1 >= 0 /\ B + I >= 0 /\ -B + I + 1 >= 0 /\ N + I - 1 >= 0 /\ -N + I + 1 >= 0 /\ K + I >= 0 /\ -K + I + 1 >= 0 /\ J + I - 1 >= 0 /\ -J + 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 /\ N - H >= 0 /\ -N - H + 2 >= 0 /\ K - H + 1 >= 0 /\ -K - H + 2 >= 0 /\ J - H >= 0 /\ -J - 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 /\ N + G - 1 >= 0 /\ -N + G + 1 >= 0 /\ K + G >= 0 /\ -K + G + 1 >= 0 /\ J + G - 1 >= 0 /\ -J + G + 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F - 2 >= 0 /\ B + F - 1 >= 0 /\ -B + F >= 0 /\ N + F - 2 >= 0 /\ -N + F >= 0 /\ K + F - 1 >= 0 /\ -K + F >= 0 /\ J + F - 2 >= 0 /\ -J + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ B + E >= 0 /\ -B + E + 1 >= 0 /\ N + E - 1 >= 0 /\ -N + E + 1 >= 0 /\ K + E >= 0 /\ -K + E + 1 >= 0 /\ J + E - 1 >= 0 /\ -J + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ B + D >= 0 /\ -B + D + 1 >= 0 /\ N + D - 1 >= 0 /\ -N + D + 1 >= 0 /\ K + D >= 0 /\ -K + D + 1 >= 0 /\ J + D - 1 >= 0 /\ -J + D + 1 >= 0 /\ -A + D + 1 >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ -B + C >= 0 /\ N + C - 2 >= 0 /\ -N + C >= 0 /\ K + C - 2 >= 0 /\ -K + C >= 0 /\ J + C - 2 >= 0 /\ -J + C >= 0 /\ A + C - 2 >= 0 /\ -A + C >= 0 /\ -B + 1 >= 0 /\ N - B >= 0 /\ -N - B + 2 >= 0 /\ K - B >= 0 /\ -K - B + 2 >= 0 /\ J - B >= 0 /\ -J - B + 2 >= 0 /\ -A - B + 2 >= 0 /\ B >= 0 /\ N + B - 1 >= 0 /\ -N + B + 1 >= 0 /\ K + B >= 0 /\ -K + B >= 0 /\ J + B - 1 >= 0 /\ -J + B + 1 >= 0 /\ -A + B + 1 >= 0 /\ M - O >= 0 /\ L - O >= 0 /\ -M + O >= 0 /\ -L + O >= 0 /\ -N + 1 >= 0 /\ K - N + 1 >= 0 /\ -K - N + 2 >= 0 /\ J - N >= 0 /\ -J - N + 2 >= 0 /\ -A - N + 2 >= 0 /\ N - 1 >= 0 /\ K + N - 1 >= 0 /\ -K + N >= 0 /\ J + N - 2 >= 0 /\ -J + N >= 0 /\ -A + N >= 0 /\ L - M >= 0 /\ -L + M >= 0 /\ -K + 1 >= 0 /\ J - K >= 0 /\ -J - K + 2 >= 0 /\ -A - K + 2 >= 0 /\ K >= 0 /\ J + K - 1 >= 0 /\ -J + K + 1 >= 0 /\ -A + K + 1 >= 0 /\ -J + 1 >= 0 /\ -A - J + 2 >= 0 /\ J - 1 >= 0 /\ -A + J >= 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 + 1 >= 0 /\ -B - I + 2 >= 0 /\ N - I >= 0 /\ -N - I + 2 >= 0 /\ K - I + 1 >= 0 /\ -K - I + 2 >= 0 /\ J - I >= 0 /\ -J - 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 - 1 >= 0 /\ B + I >= 0 /\ -B + I + 1 >= 0 /\ N + I - 1 >= 0 /\ -N + I + 1 >= 0 /\ K + I >= 0 /\ -K + I + 1 >= 0 /\ J + I - 1 >= 0 /\ -J + 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 /\ N - H >= 0 /\ -N - H + 2 >= 0 /\ K - H + 1 >= 0 /\ -K - H + 2 >= 0 /\ J - H >= 0 /\ -J - 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 /\ N + G - 1 >= 0 /\ -N + G + 1 >= 0 /\ K + G >= 0 /\ -K + G + 1 >= 0 /\ J + G - 1 >= 0 /\ -J + G + 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F - 2 >= 0 /\ B + F - 1 >= 0 /\ -B + F >= 0 /\ N + F - 2 >= 0 /\ -N + F >= 0 /\ K + F - 1 >= 0 /\ -K + F >= 0 /\ J + F - 2 >= 0 /\ -J + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ B + E >= 0 /\ -B + E + 1 >= 0 /\ N + E - 1 >= 0 /\ -N + E + 1 >= 0 /\ K + E >= 0 /\ -K + E + 1 >= 0 /\ J + E - 1 >= 0 /\ -J + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ B + D >= 0 /\ -B + D + 1 >= 0 /\ N + D - 1 >= 0 /\ -N + D + 1 >= 0 /\ K + D >= 0 /\ -K + D + 1 >= 0 /\ J + D - 1 >= 0 /\ -J + D + 1 >= 0 /\ -A + D + 1 >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ -B + C >= 0 /\ N + C - 2 >= 0 /\ -N + C >= 0 /\ K + C - 2 >= 0 /\ -K + C >= 0 /\ J + C - 2 >= 0 /\ -J + C >= 0 /\ A + C - 2 >= 0 /\ -A + C >= 0 /\ -B + 1 >= 0 /\ N - B >= 0 /\ -N - B + 2 >= 0 /\ K - B >= 0 /\ -K - B + 2 >= 0 /\ J - B >= 0 /\ -J - B + 2 >= 0 /\ -A - B + 2 >= 0 /\ B >= 0 /\ N + B - 1 >= 0 /\ -N + B + 1 >= 0 /\ K + B >= 0 /\ -K + B >= 0 /\ J + B - 1 >= 0 /\ -J + B + 1 >= 0 /\ -A + B + 1 >= 0 /\ M - O >= 0 /\ L - O >= 0 /\ -M + O >= 0 /\ -L + O >= 0 /\ -N + 1 >= 0 /\ K - N + 1 >= 0 /\ -K - N + 2 >= 0 /\ J - N >= 0 /\ -J - N + 2 >= 0 /\ -A - N + 2 >= 0 /\ N - 1 >= 0 /\ K + N - 1 >= 0 /\ -K + N >= 0 /\ J + N - 2 >= 0 /\ -J + N >= 0 /\ -A + N >= 0 /\ L - M >= 0 /\ -L + M >= 0 /\ -K + 1 >= 0 /\ J - K >= 0 /\ -J - K + 2 >= 0 /\ -A - K + 2 >= 0 /\ K >= 0 /\ J + K - 1 >= 0 /\ -J + K + 1 >= 0 /\ -A + K + 1 >= 0 /\ -J + 1 >= 0 /\ -A - J + 2 >= 0 /\ J - 1 >= 0 /\ -A + J >= 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(f10(A, B, C, D, E, F, G + 1, H, 1, J, K, L, 0, 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 + 1 >= 0 /\ -B - I + 2 >= 0 /\ N - I >= 0 /\ -N - I + 2 >= 0 /\ K - I + 1 >= 0 /\ -K - I + 2 >= 0 /\ J - I >= 0 /\ -J - 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 - 1 >= 0 /\ B + I >= 0 /\ -B + I + 1 >= 0 /\ N + I - 1 >= 0 /\ -N + I + 1 >= 0 /\ K + I >= 0 /\ -K + I + 1 >= 0 /\ J + I - 1 >= 0 /\ -J + 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 /\ N - H >= 0 /\ -N - H + 2 >= 0 /\ K - H + 1 >= 0 /\ -K - H + 2 >= 0 /\ J - H >= 0 /\ -J - 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 /\ N + G - 1 >= 0 /\ -N + G + 1 >= 0 /\ K + G >= 0 /\ -K + G + 1 >= 0 /\ J + G - 1 >= 0 /\ -J + G + 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F - 2 >= 0 /\ B + F - 1 >= 0 /\ -B + F >= 0 /\ N + F - 2 >= 0 /\ -N + F >= 0 /\ K + F - 1 >= 0 /\ -K + F >= 0 /\ J + F - 2 >= 0 /\ -J + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ B + E >= 0 /\ -B + E + 1 >= 0 /\ N + E - 1 >= 0 /\ -N + E + 1 >= 0 /\ K + E >= 0 /\ -K + E + 1 >= 0 /\ J + E - 1 >= 0 /\ -J + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ B + D >= 0 /\ -B + D + 1 >= 0 /\ N + D - 1 >= 0 /\ -N + D + 1 >= 0 /\ K + D >= 0 /\ -K + D + 1 >= 0 /\ J + D - 1 >= 0 /\ -J + D + 1 >= 0 /\ -A + D + 1 >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ -B + C >= 0 /\ N + C - 2 >= 0 /\ -N + C >= 0 /\ K + C - 2 >= 0 /\ -K + C >= 0 /\ J + C - 2 >= 0 /\ -J + C >= 0 /\ A + C - 2 >= 0 /\ -A + C >= 0 /\ -B + 1 >= 0 /\ N - B >= 0 /\ -N - B + 2 >= 0 /\ K - B >= 0 /\ -K - B + 2 >= 0 /\ J - B >= 0 /\ -J - B + 2 >= 0 /\ -A - B + 2 >= 0 /\ B >= 0 /\ N + B - 1 >= 0 /\ -N + B + 1 >= 0 /\ K + B >= 0 /\ -K + B >= 0 /\ J + B - 1 >= 0 /\ -J + B + 1 >= 0 /\ -A + B + 1 >= 0 /\ M - O >= 0 /\ L - O >= 0 /\ -M + O >= 0 /\ -L + O >= 0 /\ -N + 1 >= 0 /\ K - N + 1 >= 0 /\ -K - N + 2 >= 0 /\ J - N >= 0 /\ -J - N + 2 >= 0 /\ -A - N + 2 >= 0 /\ N - 1 >= 0 /\ K + N - 1 >= 0 /\ -K + N >= 0 /\ J + N - 2 >= 0 /\ -J + N >= 0 /\ -A + N >= 0 /\ L - M >= 0 /\ -L + M >= 0 /\ -K + 1 >= 0 /\ J - K >= 0 /\ -J - K + 2 >= 0 /\ -A - K + 2 >= 0 /\ K >= 0 /\ J + K - 1 >= 0 /\ -J + K + 1 >= 0 /\ -A + K + 1 >= 0 /\ -J + 1 >= 0 /\ -A - J + 2 >= 0 /\ J - 1 >= 0 /\ -A + J >= 0 /\ -A + 1 >= 0 /\ M >= 1 /\ I = 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, 1, J, K, L, 1, 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 + 1 >= 0 /\ -B - I + 2 >= 0 /\ N - I >= 0 /\ -N - I + 2 >= 0 /\ K - I + 1 >= 0 /\ -K - I + 2 >= 0 /\ J - I >= 0 /\ -J - 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 - 1 >= 0 /\ B + I >= 0 /\ -B + I + 1 >= 0 /\ N + I - 1 >= 0 /\ -N + I + 1 >= 0 /\ K + I >= 0 /\ -K + I + 1 >= 0 /\ J + I - 1 >= 0 /\ -J + 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 /\ N - H >= 0 /\ -N - H + 2 >= 0 /\ K - H + 1 >= 0 /\ -K - H + 2 >= 0 /\ J - H >= 0 /\ -J - 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 /\ N + G - 1 >= 0 /\ -N + G + 1 >= 0 /\ K + G >= 0 /\ -K + G + 1 >= 0 /\ J + G - 1 >= 0 /\ -J + G + 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F - 2 >= 0 /\ B + F - 1 >= 0 /\ -B + F >= 0 /\ N + F - 2 >= 0 /\ -N + F >= 0 /\ K + F - 1 >= 0 /\ -K + F >= 0 /\ J + F - 2 >= 0 /\ -J + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ B + E >= 0 /\ -B + E + 1 >= 0 /\ N + E - 1 >= 0 /\ -N + E + 1 >= 0 /\ K + E >= 0 /\ -K + E + 1 >= 0 /\ J + E - 1 >= 0 /\ -J + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ B + D >= 0 /\ -B + D + 1 >= 0 /\ N + D - 1 >= 0 /\ -N + D + 1 >= 0 /\ K + D >= 0 /\ -K + D + 1 >= 0 /\ J + D - 1 >= 0 /\ -J + D + 1 >= 0 /\ -A + D + 1 >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ -B + C >= 0 /\ N + C - 2 >= 0 /\ -N + C >= 0 /\ K + C - 2 >= 0 /\ -K + C >= 0 /\ J + C - 2 >= 0 /\ -J + C >= 0 /\ A + C - 2 >= 0 /\ -A + C >= 0 /\ -B + 1 >= 0 /\ N - B >= 0 /\ -N - B + 2 >= 0 /\ K - B >= 0 /\ -K - B + 2 >= 0 /\ J - B >= 0 /\ -J - B + 2 >= 0 /\ -A - B + 2 >= 0 /\ B >= 0 /\ N + B - 1 >= 0 /\ -N + B + 1 >= 0 /\ K + B >= 0 /\ -K + B >= 0 /\ J + B - 1 >= 0 /\ -J + B + 1 >= 0 /\ -A + B + 1 >= 0 /\ M - O >= 0 /\ L - O >= 0 /\ -M + O >= 0 /\ -L + O >= 0 /\ -N + 1 >= 0 /\ K - N + 1 >= 0 /\ -K - N + 2 >= 0 /\ J - N >= 0 /\ -J - N + 2 >= 0 /\ -A - N + 2 >= 0 /\ N - 1 >= 0 /\ K + N - 1 >= 0 /\ -K + N >= 0 /\ J + N - 2 >= 0 /\ -J + N >= 0 /\ -A + N >= 0 /\ L - M >= 0 /\ -L + M >= 0 /\ -K + 1 >= 0 /\ J - K >= 0 /\ -J - K + 2 >= 0 /\ -A - K + 2 >= 0 /\ K >= 0 /\ J + K - 1 >= 0 /\ -J + K + 1 >= 0 /\ -A + K + 1 >= 0 /\ -J + 1 >= 0 /\ -A - J + 2 >= 0 /\ J - 1 >= 0 /\ -A + J >= 0 /\ -A + 1 >= 0 /\ 0 >= M /\ I = 1 ] f10(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q) -> Com_1(f79(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 /\ 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 ] )