(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS f0)) (VAR A B C D E F G H I J K L M) (RULES f0(A, B, C, D, E, F, G, H, I, J, K, L, M) -> Com_1(f15(50, 5, 0, D, E, F, G, H, I, J, K, L, M)) f15(A, B, C, D, E, F, G, H, I, J, K, L, M) -> Com_1(f19(A, B, C, 0, 0, F, G, H, I, J, K, L, M)) [ C >= 0 /\ B + C - 5 >= 0 /\ -B + C + 5 >= 0 /\ A + C - 50 >= 0 /\ -A + C + 50 >= 0 /\ -B + 5 >= 0 /\ A - B - 45 >= 0 /\ -A - B + 55 >= 0 /\ B - 5 >= 0 /\ A + B - 55 >= 0 /\ -A + B + 45 >= 0 /\ -A + 50 >= 0 /\ A - 50 >= 0 /\ B >= C ] f19(A, B, C, D, E, F, G, H, I, J, K, L, M) -> Com_1(f19(A, B, C, D + N, E + 1, F, G, H, I, J, K, L, M)) [ E >= 0 /\ C + E >= 0 /\ B + E - 5 >= 0 /\ -B + E + 5 >= 0 /\ A + E - 50 >= 0 /\ -A + E + 50 >= 0 /\ C >= 0 /\ B + C - 5 >= 0 /\ -B + C + 5 >= 0 /\ A + C - 50 >= 0 /\ -A + C + 50 >= 0 /\ -B + 5 >= 0 /\ A - B - 45 >= 0 /\ -A - B + 55 >= 0 /\ B - 5 >= 0 /\ A + B - 55 >= 0 /\ -A + B + 45 >= 0 /\ -A + 50 >= 0 /\ A - 50 >= 0 /\ B >= E /\ E >= C + 1 ] f19(A, B, C, D, E, F, G, H, I, J, K, L, M) -> Com_1(f19(A, B, C, D + N, E + 1, F, G, H, I, J, K, L, M)) [ E >= 0 /\ C + E >= 0 /\ B + E - 5 >= 0 /\ -B + E + 5 >= 0 /\ A + E - 50 >= 0 /\ -A + E + 50 >= 0 /\ C >= 0 /\ B + C - 5 >= 0 /\ -B + C + 5 >= 0 /\ A + C - 50 >= 0 /\ -A + C + 50 >= 0 /\ -B + 5 >= 0 /\ A - B - 45 >= 0 /\ -A - B + 55 >= 0 /\ B - 5 >= 0 /\ A + B - 55 >= 0 /\ -A + B + 45 >= 0 /\ -A + 50 >= 0 /\ A - 50 >= 0 /\ C >= E + 1 /\ B >= E ] f19(A, B, C, D, E, F, G, H, I, J, K, L, M) -> Com_1(f19(A, B, C, D + N, C + 1, F, G, H, I, J, K, L, M)) [ E >= 0 /\ C + E >= 0 /\ B + E - 5 >= 0 /\ -B + E + 5 >= 0 /\ A + E - 50 >= 0 /\ -A + E + 50 >= 0 /\ C >= 0 /\ B + C - 5 >= 0 /\ -B + C + 5 >= 0 /\ A + C - 50 >= 0 /\ -A + C + 50 >= 0 /\ -B + 5 >= 0 /\ A - B - 45 >= 0 /\ -A - B + 55 >= 0 /\ B - 5 >= 0 /\ A + B - 55 >= 0 /\ -A + B + 45 >= 0 /\ -A + 50 >= 0 /\ A - 50 >= 0 /\ B >= E /\ C = E ] f33(A, B, C, D, E, F, G, H, I, J, K, L, M) -> Com_1(f36(A, B, C, D, E, F, G, G + 1, I, J, K, L, M)) [ G >= 0 /\ F + G - 5 >= 0 /\ -F + G + 5 >= 0 /\ C + G - 6 >= 0 /\ B + G - 5 >= 0 /\ -B + G + 5 >= 0 /\ M + G - 50 >= 0 /\ -M + G + 50 >= 0 /\ A + G - 50 >= 0 /\ -A + G + 50 >= 0 /\ -F + 5 >= 0 /\ C - F - 1 >= 0 /\ B - F >= 0 /\ -B - F + 10 >= 0 /\ M - F - 45 >= 0 /\ -M - F + 55 >= 0 /\ A - F - 45 >= 0 /\ -A - F + 55 >= 0 /\ F - 5 >= 0 /\ C + F - 11 >= 0 /\ B + F - 10 >= 0 /\ -B + F >= 0 /\ M + F - 55 >= 0 /\ -M + F + 45 >= 0 /\ A + F - 55 >= 0 /\ -A + F + 45 >= 0 /\ C - 6 >= 0 /\ B + C - 11 >= 0 /\ -B + C - 1 >= 0 /\ M + C - 56 >= 0 /\ -M + C + 44 >= 0 /\ A + C - 56 >= 0 /\ -A + C + 44 >= 0 /\ -B + 5 >= 0 /\ M - B - 45 >= 0 /\ -M - B + 55 >= 0 /\ A - B - 45 >= 0 /\ -A - B + 55 >= 0 /\ B - 5 >= 0 /\ M + B - 55 >= 0 /\ -M + B + 45 >= 0 /\ A + B - 55 >= 0 /\ -A + B + 45 >= 0 /\ -M + 50 >= 0 /\ A - M >= 0 /\ -A - M + 100 >= 0 /\ M - 50 >= 0 /\ A + M - 100 >= 0 /\ -A + M >= 0 /\ -A + 50 >= 0 /\ A - 50 >= 0 /\ F >= G + 1 ] f36(A, B, C, D, E, F, G, H, I, J, K, L, M) -> Com_1(f41(A, B, C, D, E, F, G, H, N, 0, K, L, M)) [ H - 1 >= 0 /\ G + H - 1 >= 0 /\ -G + H - 1 >= 0 /\ F + H - 6 >= 0 /\ -F + H + 4 >= 0 /\ C + H - 7 >= 0 /\ B + H - 6 >= 0 /\ -B + H + 4 >= 0 /\ M + H - 51 >= 0 /\ -M + H + 49 >= 0 /\ A + H - 51 >= 0 /\ -A + H + 49 >= 0 /\ -G + 4 >= 0 /\ F - G - 1 >= 0 /\ -F - G + 9 >= 0 /\ C - G - 2 >= 0 /\ B - G - 1 >= 0 /\ -B - G + 9 >= 0 /\ M - G - 46 >= 0 /\ -M - G + 54 >= 0 /\ A - G - 46 >= 0 /\ -A - G + 54 >= 0 /\ G >= 0 /\ F + G - 5 >= 0 /\ -F + G + 5 >= 0 /\ C + G - 6 >= 0 /\ B + G - 5 >= 0 /\ -B + G + 5 >= 0 /\ M + G - 50 >= 0 /\ -M + G + 50 >= 0 /\ A + G - 50 >= 0 /\ -A + G + 50 >= 0 /\ -F + 5 >= 0 /\ C - F - 1 >= 0 /\ B - F >= 0 /\ -B - F + 10 >= 0 /\ M - F - 45 >= 0 /\ -M - F + 55 >= 0 /\ A - F - 45 >= 0 /\ -A - F + 55 >= 0 /\ F - 5 >= 0 /\ C + F - 11 >= 0 /\ B + F - 10 >= 0 /\ -B + F >= 0 /\ M + F - 55 >= 0 /\ -M + F + 45 >= 0 /\ A + F - 55 >= 0 /\ -A + F + 45 >= 0 /\ C - 6 >= 0 /\ B + C - 11 >= 0 /\ -B + C - 1 >= 0 /\ M + C - 56 >= 0 /\ -M + C + 44 >= 0 /\ A + C - 56 >= 0 /\ -A + C + 44 >= 0 /\ -B + 5 >= 0 /\ M - B - 45 >= 0 /\ -M - B + 55 >= 0 /\ A - B - 45 >= 0 /\ -A - B + 55 >= 0 /\ B - 5 >= 0 /\ M + B - 55 >= 0 /\ -M + B + 45 >= 0 /\ A + B - 55 >= 0 /\ -A + B + 45 >= 0 /\ -M + 50 >= 0 /\ A - M >= 0 /\ -A - M + 100 >= 0 /\ M - 50 >= 0 /\ A + M - 100 >= 0 /\ -A + M >= 0 /\ -A + 50 >= 0 /\ A - 50 >= 0 /\ G >= 1 /\ F >= H ] f41(A, B, C, D, E, F, G, H, I, J, K, L, M) -> Com_1(f41(A, B, C, D, E, F, G, H, N, J + 1, K, L, M)) [ -H + 5 >= 0 /\ G - H + 4 >= 0 /\ -G - H + 9 >= 0 /\ F - H >= 0 /\ -F - H + 10 >= 0 /\ C - H - 1 >= 0 /\ B - H >= 0 /\ -B - H + 10 >= 0 /\ M - H - 45 >= 0 /\ -M - H + 55 >= 0 /\ J - H + 5 >= 0 /\ A - H - 45 >= 0 /\ -A - H + 55 >= 0 /\ H - 2 >= 0 /\ G + H - 3 >= 0 /\ -G + H - 1 >= 0 /\ F + H - 7 >= 0 /\ -F + H + 3 >= 0 /\ C + H - 8 >= 0 /\ B + H - 7 >= 0 /\ -B + H + 3 >= 0 /\ M + H - 52 >= 0 /\ -M + H + 48 >= 0 /\ J + H - 2 >= 0 /\ A + H - 52 >= 0 /\ -A + H + 48 >= 0 /\ -G + 4 >= 0 /\ F - G - 1 >= 0 /\ -F - G + 9 >= 0 /\ C - G - 2 >= 0 /\ B - G - 1 >= 0 /\ -B - G + 9 >= 0 /\ M - G - 46 >= 0 /\ -M - G + 54 >= 0 /\ J - G + 4 >= 0 /\ A - G - 46 >= 0 /\ -A - G + 54 >= 0 /\ G - 1 >= 0 /\ F + G - 6 >= 0 /\ -F + G + 4 >= 0 /\ C + G - 7 >= 0 /\ B + G - 6 >= 0 /\ -B + G + 4 >= 0 /\ M + G - 51 >= 0 /\ -M + G + 49 >= 0 /\ J + G - 1 >= 0 /\ A + G - 51 >= 0 /\ -A + G + 49 >= 0 /\ -F + 5 >= 0 /\ C - F - 1 >= 0 /\ B - F >= 0 /\ -B - F + 10 >= 0 /\ M - F - 45 >= 0 /\ -M - F + 55 >= 0 /\ J - F + 5 >= 0 /\ A - F - 45 >= 0 /\ -A - F + 55 >= 0 /\ F - 5 >= 0 /\ C + F - 11 >= 0 /\ B + F - 10 >= 0 /\ -B + F >= 0 /\ M + F - 55 >= 0 /\ -M + F + 45 >= 0 /\ J + F - 5 >= 0 /\ A + F - 55 >= 0 /\ -A + F + 45 >= 0 /\ C - 6 >= 0 /\ B + C - 11 >= 0 /\ -B + C - 1 >= 0 /\ M + C - 56 >= 0 /\ -M + C + 44 >= 0 /\ J + C - 6 >= 0 /\ A + C - 56 >= 0 /\ -A + C + 44 >= 0 /\ -B + 5 >= 0 /\ M - B - 45 >= 0 /\ -M - B + 55 >= 0 /\ J - B + 5 >= 0 /\ A - B - 45 >= 0 /\ -A - B + 55 >= 0 /\ B - 5 >= 0 /\ M + B - 55 >= 0 /\ -M + B + 45 >= 0 /\ J + B - 5 >= 0 /\ A + B - 55 >= 0 /\ -A + B + 45 >= 0 /\ -M + 50 >= 0 /\ J - M + 50 >= 0 /\ A - M >= 0 /\ -A - M + 100 >= 0 /\ M - 50 >= 0 /\ J + M - 50 >= 0 /\ A + M - 100 >= 0 /\ -A + M >= 0 /\ J >= 0 /\ A + J - 50 >= 0 /\ -A + J + 50 >= 0 /\ -A + 50 >= 0 /\ A - 50 >= 0 /\ G >= J + 1 ] f36(A, B, C, D, E, F, G, H, I, J, K, L, M) -> Com_1(f36(A, B, C, D, E, F, 0, H + 1, N, J, K, L, M)) [ H - 1 >= 0 /\ G + H - 1 >= 0 /\ -G + H - 1 >= 0 /\ F + H - 6 >= 0 /\ -F + H + 4 >= 0 /\ C + H - 7 >= 0 /\ B + H - 6 >= 0 /\ -B + H + 4 >= 0 /\ M + H - 51 >= 0 /\ -M + H + 49 >= 0 /\ A + H - 51 >= 0 /\ -A + H + 49 >= 0 /\ -G + 4 >= 0 /\ F - G - 1 >= 0 /\ -F - G + 9 >= 0 /\ C - G - 2 >= 0 /\ B - G - 1 >= 0 /\ -B - G + 9 >= 0 /\ M - G - 46 >= 0 /\ -M - G + 54 >= 0 /\ A - G - 46 >= 0 /\ -A - G + 54 >= 0 /\ G >= 0 /\ F + G - 5 >= 0 /\ -F + G + 5 >= 0 /\ C + G - 6 >= 0 /\ B + G - 5 >= 0 /\ -B + G + 5 >= 0 /\ M + G - 50 >= 0 /\ -M + G + 50 >= 0 /\ A + G - 50 >= 0 /\ -A + G + 50 >= 0 /\ -F + 5 >= 0 /\ C - F - 1 >= 0 /\ B - F >= 0 /\ -B - F + 10 >= 0 /\ M - F - 45 >= 0 /\ -M - F + 55 >= 0 /\ A - F - 45 >= 0 /\ -A - F + 55 >= 0 /\ F - 5 >= 0 /\ C + F - 11 >= 0 /\ B + F - 10 >= 0 /\ -B + F >= 0 /\ M + F - 55 >= 0 /\ -M + F + 45 >= 0 /\ A + F - 55 >= 0 /\ -A + F + 45 >= 0 /\ C - 6 >= 0 /\ B + C - 11 >= 0 /\ -B + C - 1 >= 0 /\ M + C - 56 >= 0 /\ -M + C + 44 >= 0 /\ A + C - 56 >= 0 /\ -A + C + 44 >= 0 /\ -B + 5 >= 0 /\ M - B - 45 >= 0 /\ -M - B + 55 >= 0 /\ A - B - 45 >= 0 /\ -A - B + 55 >= 0 /\ B - 5 >= 0 /\ M + B - 55 >= 0 /\ -M + B + 45 >= 0 /\ A + B - 55 >= 0 /\ -A + B + 45 >= 0 /\ -M + 50 >= 0 /\ A - M >= 0 /\ -A - M + 100 >= 0 /\ M - 50 >= 0 /\ A + M - 100 >= 0 /\ -A + M >= 0 /\ -A + 50 >= 0 /\ A - 50 >= 0 /\ F >= H /\ G = 0 ] f50(A, B, C, D, E, F, G, H, I, J, K, L, M) -> Com_1(f54(A, B, C, D, E, F, G, H, N, 0, K, L, M)) [ H - 1 >= 0 /\ G + H - 1 >= 0 /\ -G + H - 1 >= 0 /\ F + H - 6 >= 0 /\ -F + H + 4 >= 0 /\ C + H - 7 >= 0 /\ B + H - 6 >= 0 /\ -B + H + 4 >= 0 /\ M + H - 51 >= 0 /\ -M + H + 49 >= 0 /\ A + H - 51 >= 0 /\ -A + H + 49 >= 0 /\ G >= 0 /\ F + G - 5 >= 0 /\ -F + G + 5 >= 0 /\ C + G - 6 >= 0 /\ B + G - 5 >= 0 /\ -B + G + 5 >= 0 /\ M + G - 50 >= 0 /\ -M + G + 50 >= 0 /\ A + G - 50 >= 0 /\ -A + G + 50 >= 0 /\ -F + 5 >= 0 /\ C - F - 1 >= 0 /\ B - F >= 0 /\ -B - F + 10 >= 0 /\ M - F - 45 >= 0 /\ -M - F + 55 >= 0 /\ A - F - 45 >= 0 /\ -A - F + 55 >= 0 /\ F - 5 >= 0 /\ C + F - 11 >= 0 /\ B + F - 10 >= 0 /\ -B + F >= 0 /\ M + F - 55 >= 0 /\ -M + F + 45 >= 0 /\ A + F - 55 >= 0 /\ -A + F + 45 >= 0 /\ C - 6 >= 0 /\ B + C - 11 >= 0 /\ -B + C - 1 >= 0 /\ M + C - 56 >= 0 /\ -M + C + 44 >= 0 /\ A + C - 56 >= 0 /\ -A + C + 44 >= 0 /\ -B + 5 >= 0 /\ M - B - 45 >= 0 /\ -M - B + 55 >= 0 /\ A - B - 45 >= 0 /\ -A - B + 55 >= 0 /\ B - 5 >= 0 /\ M + B - 55 >= 0 /\ -M + B + 45 >= 0 /\ A + B - 55 >= 0 /\ -A + B + 45 >= 0 /\ -M + 50 >= 0 /\ A - M >= 0 /\ -A - M + 100 >= 0 /\ M - 50 >= 0 /\ A + M - 100 >= 0 /\ -A + M >= 0 /\ -A + 50 >= 0 /\ A - 50 >= 0 /\ F >= H ] f54(A, B, C, D, E, F, G, H, I, J, K, L, M) -> Com_1(f54(A, B, C, D, E, F, G, H, N, J + 1, K, L, M)) [ H - 1 >= 0 /\ G + H - 1 >= 0 /\ -G + H - 1 >= 0 /\ F + H - 6 >= 0 /\ -F + H + 4 >= 0 /\ C + H - 7 >= 0 /\ B + H - 6 >= 0 /\ -B + H + 4 >= 0 /\ M + H - 51 >= 0 /\ -M + H + 49 >= 0 /\ J + H - 1 >= 0 /\ A + H - 51 >= 0 /\ -A + H + 49 >= 0 /\ -G + 4 >= 0 /\ F - G - 1 >= 0 /\ -F - G + 9 >= 0 /\ C - G - 2 >= 0 /\ B - G - 1 >= 0 /\ -B - G + 9 >= 0 /\ M - G - 46 >= 0 /\ -M - G + 54 >= 0 /\ J - G + 4 >= 0 /\ A - G - 46 >= 0 /\ -A - G + 54 >= 0 /\ G >= 0 /\ F + G - 5 >= 0 /\ -F + G + 5 >= 0 /\ C + G - 6 >= 0 /\ B + G - 5 >= 0 /\ -B + G + 5 >= 0 /\ M + G - 50 >= 0 /\ -M + G + 50 >= 0 /\ J + G >= 0 /\ A + G - 50 >= 0 /\ -A + G + 50 >= 0 /\ -F + 5 >= 0 /\ C - F - 1 >= 0 /\ B - F >= 0 /\ -B - F + 10 >= 0 /\ M - F - 45 >= 0 /\ -M - F + 55 >= 0 /\ J - F + 5 >= 0 /\ A - F - 45 >= 0 /\ -A - F + 55 >= 0 /\ F - 5 >= 0 /\ C + F - 11 >= 0 /\ B + F - 10 >= 0 /\ -B + F >= 0 /\ M + F - 55 >= 0 /\ -M + F + 45 >= 0 /\ J + F - 5 >= 0 /\ A + F - 55 >= 0 /\ -A + F + 45 >= 0 /\ C - 6 >= 0 /\ B + C - 11 >= 0 /\ -B + C - 1 >= 0 /\ M + C - 56 >= 0 /\ -M + C + 44 >= 0 /\ J + C - 6 >= 0 /\ A + C - 56 >= 0 /\ -A + C + 44 >= 0 /\ -B + 5 >= 0 /\ M - B - 45 >= 0 /\ -M - B + 55 >= 0 /\ J - B + 5 >= 0 /\ A - B - 45 >= 0 /\ -A - B + 55 >= 0 /\ B - 5 >= 0 /\ M + B - 55 >= 0 /\ -M + B + 45 >= 0 /\ J + B - 5 >= 0 /\ A + B - 55 >= 0 /\ -A + B + 45 >= 0 /\ -M + 50 >= 0 /\ J - M + 50 >= 0 /\ A - M >= 0 /\ -A - M + 100 >= 0 /\ M - 50 >= 0 /\ J + M - 50 >= 0 /\ A + M - 100 >= 0 /\ -A + M >= 0 /\ J >= 0 /\ A + J - 50 >= 0 /\ -A + J + 50 >= 0 /\ -A + 50 >= 0 /\ A - 50 >= 0 /\ G >= J ] f66(A, B, C, D, E, F, G, H, I, J, K, L, M) -> Com_1(f70(A, B, C, D, E, F, G, 0, N, J, K, L, M)) [ G - 1 >= 0 /\ F + G - 6 >= 0 /\ -F + G + 4 >= 0 /\ C + G - 7 >= 0 /\ B + G - 6 >= 0 /\ -B + G + 4 >= 0 /\ M + G - 51 >= 0 /\ -M + G + 49 >= 0 /\ A + G - 51 >= 0 /\ -A + G + 49 >= 0 /\ -F + 5 >= 0 /\ C - F - 1 >= 0 /\ B - F >= 0 /\ -B - F + 10 >= 0 /\ M - F - 45 >= 0 /\ -M - F + 55 >= 0 /\ A - F - 45 >= 0 /\ -A - F + 55 >= 0 /\ F - 5 >= 0 /\ C + F - 11 >= 0 /\ B + F - 10 >= 0 /\ -B + F >= 0 /\ M + F - 55 >= 0 /\ -M + F + 45 >= 0 /\ A + F - 55 >= 0 /\ -A + F + 45 >= 0 /\ C - 6 >= 0 /\ B + C - 11 >= 0 /\ -B + C - 1 >= 0 /\ M + C - 56 >= 0 /\ -M + C + 44 >= 0 /\ A + C - 56 >= 0 /\ -A + C + 44 >= 0 /\ -B + 5 >= 0 /\ M - B - 45 >= 0 /\ -M - B + 55 >= 0 /\ A - B - 45 >= 0 /\ -A - B + 55 >= 0 /\ B - 5 >= 0 /\ M + B - 55 >= 0 /\ -M + B + 45 >= 0 /\ A + B - 55 >= 0 /\ -A + B + 45 >= 0 /\ -M + 50 >= 0 /\ A - M >= 0 /\ -A - M + 100 >= 0 /\ M - 50 >= 0 /\ A + M - 100 >= 0 /\ -A + M >= 0 /\ -A + 50 >= 0 /\ A - 50 >= 0 /\ F >= G ] f70(A, B, C, D, E, F, G, H, I, J, K, L, M) -> Com_1(f70(A, B, C, D, E, F, G, H + 1, N, J, K, L, M)) [ H >= 0 /\ G + H - 1 >= 0 /\ F + H - 5 >= 0 /\ -F + H + 5 >= 0 /\ C + H - 6 >= 0 /\ B + H - 5 >= 0 /\ -B + H + 5 >= 0 /\ M + H - 50 >= 0 /\ -M + H + 50 >= 0 /\ A + H - 50 >= 0 /\ -A + H + 50 >= 0 /\ G - 1 >= 0 /\ F + G - 6 >= 0 /\ -F + G + 4 >= 0 /\ C + G - 7 >= 0 /\ B + G - 6 >= 0 /\ -B + G + 4 >= 0 /\ M + G - 51 >= 0 /\ -M + G + 49 >= 0 /\ A + G - 51 >= 0 /\ -A + G + 49 >= 0 /\ -F + 5 >= 0 /\ C - F - 1 >= 0 /\ B - F >= 0 /\ -B - F + 10 >= 0 /\ M - F - 45 >= 0 /\ -M - F + 55 >= 0 /\ A - F - 45 >= 0 /\ -A - F + 55 >= 0 /\ F - 5 >= 0 /\ C + F - 11 >= 0 /\ B + F - 10 >= 0 /\ -B + F >= 0 /\ M + F - 55 >= 0 /\ -M + F + 45 >= 0 /\ A + F - 55 >= 0 /\ -A + F + 45 >= 0 /\ C - 6 >= 0 /\ B + C - 11 >= 0 /\ -B + C - 1 >= 0 /\ M + C - 56 >= 0 /\ -M + C + 44 >= 0 /\ A + C - 56 >= 0 /\ -A + C + 44 >= 0 /\ -B + 5 >= 0 /\ M - B - 45 >= 0 /\ -M - B + 55 >= 0 /\ A - B - 45 >= 0 /\ -A - B + 55 >= 0 /\ B - 5 >= 0 /\ M + B - 55 >= 0 /\ -M + B + 45 >= 0 /\ A + B - 55 >= 0 /\ -A + B + 45 >= 0 /\ -M + 50 >= 0 /\ A - M >= 0 /\ -A - M + 100 >= 0 /\ M - 50 >= 0 /\ A + M - 100 >= 0 /\ -A + M >= 0 /\ -A + 50 >= 0 /\ A - 50 >= 0 /\ G >= H + 1 ] f80(A, B, C, D, E, F, G, H, I, J, K, L, M) -> Com_1(f84(A, B, C, D, E, F, G, G + 1, N, J, K, L, M)) [ -G + 4 >= 0 /\ F - G - 1 >= 0 /\ -F - G + 9 >= 0 /\ C - G - 2 >= 0 /\ B - G - 1 >= 0 /\ -B - G + 9 >= 0 /\ M - G - 46 >= 0 /\ -M - G + 54 >= 0 /\ A - G - 46 >= 0 /\ -A - G + 54 >= 0 /\ -F + 5 >= 0 /\ C - F - 1 >= 0 /\ B - F >= 0 /\ -B - F + 10 >= 0 /\ M - F - 45 >= 0 /\ -M - F + 55 >= 0 /\ A - F - 45 >= 0 /\ -A - F + 55 >= 0 /\ F - 5 >= 0 /\ C + F - 11 >= 0 /\ B + F - 10 >= 0 /\ -B + F >= 0 /\ M + F - 55 >= 0 /\ -M + F + 45 >= 0 /\ A + F - 55 >= 0 /\ -A + F + 45 >= 0 /\ C - 6 >= 0 /\ B + C - 11 >= 0 /\ -B + C - 1 >= 0 /\ M + C - 56 >= 0 /\ -M + C + 44 >= 0 /\ A + C - 56 >= 0 /\ -A + C + 44 >= 0 /\ -B + 5 >= 0 /\ M - B - 45 >= 0 /\ -M - B + 55 >= 0 /\ A - B - 45 >= 0 /\ -A - B + 55 >= 0 /\ B - 5 >= 0 /\ M + B - 55 >= 0 /\ -M + B + 45 >= 0 /\ A + B - 55 >= 0 /\ -A + B + 45 >= 0 /\ -M + 50 >= 0 /\ A - M >= 0 /\ -A - M + 100 >= 0 /\ M - 50 >= 0 /\ A + M - 100 >= 0 /\ -A + M >= 0 /\ -A + 50 >= 0 /\ A - 50 >= 0 /\ G >= 0 ] f84(A, B, C, D, E, F, G, H, I, J, K, L, M) -> Com_1(f84(A, B, C, D, E, F, G, H + 1, N, J, K, L, M)) [ -G + H - 1 >= 0 /\ -G + 4 >= 0 /\ F - G - 1 >= 0 /\ -F - G + 9 >= 0 /\ C - G - 2 >= 0 /\ B - G - 1 >= 0 /\ -B - G + 9 >= 0 /\ M - G - 46 >= 0 /\ -M - G + 54 >= 0 /\ A - G - 46 >= 0 /\ -A - G + 54 >= 0 /\ -F + 5 >= 0 /\ C - F - 1 >= 0 /\ B - F >= 0 /\ -B - F + 10 >= 0 /\ M - F - 45 >= 0 /\ -M - F + 55 >= 0 /\ A - F - 45 >= 0 /\ -A - F + 55 >= 0 /\ F - 5 >= 0 /\ C + F - 11 >= 0 /\ B + F - 10 >= 0 /\ -B + F >= 0 /\ M + F - 55 >= 0 /\ -M + F + 45 >= 0 /\ A + F - 55 >= 0 /\ -A + F + 45 >= 0 /\ C - 6 >= 0 /\ B + C - 11 >= 0 /\ -B + C - 1 >= 0 /\ M + C - 56 >= 0 /\ -M + C + 44 >= 0 /\ A + C - 56 >= 0 /\ -A + C + 44 >= 0 /\ -B + 5 >= 0 /\ M - B - 45 >= 0 /\ -M - B + 55 >= 0 /\ A - B - 45 >= 0 /\ -A - B + 55 >= 0 /\ B - 5 >= 0 /\ M + B - 55 >= 0 /\ -M + B + 45 >= 0 /\ A + B - 55 >= 0 /\ -A + B + 45 >= 0 /\ -M + 50 >= 0 /\ A - M >= 0 /\ -A - M + 100 >= 0 /\ M - 50 >= 0 /\ A + M - 100 >= 0 /\ -A + M >= 0 /\ -A + 50 >= 0 /\ A - 50 >= 0 /\ F >= H ] f84(A, B, C, D, E, F, G, H, I, J, K, L, M) -> Com_1(f80(A, B, C, D, E, F, G - 1, H, I, J, K, L, M)) [ -G + H - 1 >= 0 /\ -G + 4 >= 0 /\ F - G - 1 >= 0 /\ -F - G + 9 >= 0 /\ C - G - 2 >= 0 /\ B - G - 1 >= 0 /\ -B - G + 9 >= 0 /\ M - G - 46 >= 0 /\ -M - G + 54 >= 0 /\ A - G - 46 >= 0 /\ -A - G + 54 >= 0 /\ -F + 5 >= 0 /\ C - F - 1 >= 0 /\ B - F >= 0 /\ -B - F + 10 >= 0 /\ M - F - 45 >= 0 /\ -M - F + 55 >= 0 /\ A - F - 45 >= 0 /\ -A - F + 55 >= 0 /\ F - 5 >= 0 /\ C + F - 11 >= 0 /\ B + F - 10 >= 0 /\ -B + F >= 0 /\ M + F - 55 >= 0 /\ -M + F + 45 >= 0 /\ A + F - 55 >= 0 /\ -A + F + 45 >= 0 /\ C - 6 >= 0 /\ B + C - 11 >= 0 /\ -B + C - 1 >= 0 /\ M + C - 56 >= 0 /\ -M + C + 44 >= 0 /\ A + C - 56 >= 0 /\ -A + C + 44 >= 0 /\ -B + 5 >= 0 /\ M - B - 45 >= 0 /\ -M - B + 55 >= 0 /\ A - B - 45 >= 0 /\ -A - B + 55 >= 0 /\ B - 5 >= 0 /\ M + B - 55 >= 0 /\ -M + B + 45 >= 0 /\ A + B - 55 >= 0 /\ -A + B + 45 >= 0 /\ -M + 50 >= 0 /\ A - M >= 0 /\ -A - M + 100 >= 0 /\ M - 50 >= 0 /\ A + M - 100 >= 0 /\ -A + M >= 0 /\ -A + 50 >= 0 /\ A - 50 >= 0 /\ H >= F + 1 ] f80(A, B, C, D, E, F, G, H, I, J, K, L, M) -> Com_1(f96(A, B, C, D, E, F, G, H, I, J, 0, 0, M)) [ -G + 4 >= 0 /\ F - G - 1 >= 0 /\ -F - G + 9 >= 0 /\ C - G - 2 >= 0 /\ B - G - 1 >= 0 /\ -B - G + 9 >= 0 /\ M - G - 46 >= 0 /\ -M - G + 54 >= 0 /\ A - G - 46 >= 0 /\ -A - G + 54 >= 0 /\ -F + 5 >= 0 /\ C - F - 1 >= 0 /\ B - F >= 0 /\ -B - F + 10 >= 0 /\ M - F - 45 >= 0 /\ -M - F + 55 >= 0 /\ A - F - 45 >= 0 /\ -A - F + 55 >= 0 /\ F - 5 >= 0 /\ C + F - 11 >= 0 /\ B + F - 10 >= 0 /\ -B + F >= 0 /\ M + F - 55 >= 0 /\ -M + F + 45 >= 0 /\ A + F - 55 >= 0 /\ -A + F + 45 >= 0 /\ C - 6 >= 0 /\ B + C - 11 >= 0 /\ -B + C - 1 >= 0 /\ M + C - 56 >= 0 /\ -M + C + 44 >= 0 /\ A + C - 56 >= 0 /\ -A + C + 44 >= 0 /\ -B + 5 >= 0 /\ M - B - 45 >= 0 /\ -M - B + 55 >= 0 /\ A - B - 45 >= 0 /\ -A - B + 55 >= 0 /\ B - 5 >= 0 /\ M + B - 55 >= 0 /\ -M + B + 45 >= 0 /\ A + B - 55 >= 0 /\ -A + B + 45 >= 0 /\ -M + 50 >= 0 /\ A - M >= 0 /\ -A - M + 100 >= 0 /\ M - 50 >= 0 /\ A + M - 100 >= 0 /\ -A + M >= 0 /\ -A + 50 >= 0 /\ A - 50 >= 0 /\ 0 >= G + 1 ] f70(A, B, C, D, E, F, G, H, I, J, K, L, M) -> Com_1(f66(A, B, C, D, E, F, G + 1, H, I, J, K, L, M)) [ H >= 0 /\ G + H - 1 >= 0 /\ F + H - 5 >= 0 /\ -F + H + 5 >= 0 /\ C + H - 6 >= 0 /\ B + H - 5 >= 0 /\ -B + H + 5 >= 0 /\ M + H - 50 >= 0 /\ -M + H + 50 >= 0 /\ A + H - 50 >= 0 /\ -A + H + 50 >= 0 /\ G - 1 >= 0 /\ F + G - 6 >= 0 /\ -F + G + 4 >= 0 /\ C + G - 7 >= 0 /\ B + G - 6 >= 0 /\ -B + G + 4 >= 0 /\ M + G - 51 >= 0 /\ -M + G + 49 >= 0 /\ A + G - 51 >= 0 /\ -A + G + 49 >= 0 /\ -F + 5 >= 0 /\ C - F - 1 >= 0 /\ B - F >= 0 /\ -B - F + 10 >= 0 /\ M - F - 45 >= 0 /\ -M - F + 55 >= 0 /\ A - F - 45 >= 0 /\ -A - F + 55 >= 0 /\ F - 5 >= 0 /\ C + F - 11 >= 0 /\ B + F - 10 >= 0 /\ -B + F >= 0 /\ M + F - 55 >= 0 /\ -M + F + 45 >= 0 /\ A + F - 55 >= 0 /\ -A + F + 45 >= 0 /\ C - 6 >= 0 /\ B + C - 11 >= 0 /\ -B + C - 1 >= 0 /\ M + C - 56 >= 0 /\ -M + C + 44 >= 0 /\ A + C - 56 >= 0 /\ -A + C + 44 >= 0 /\ -B + 5 >= 0 /\ M - B - 45 >= 0 /\ -M - B + 55 >= 0 /\ A - B - 45 >= 0 /\ -A - B + 55 >= 0 /\ B - 5 >= 0 /\ M + B - 55 >= 0 /\ -M + B + 45 >= 0 /\ A + B - 55 >= 0 /\ -A + B + 45 >= 0 /\ -M + 50 >= 0 /\ A - M >= 0 /\ -A - M + 100 >= 0 /\ M - 50 >= 0 /\ A + M - 100 >= 0 /\ -A + M >= 0 /\ -A + 50 >= 0 /\ A - 50 >= 0 /\ H >= G ] f66(A, B, C, D, E, F, G, H, I, J, K, L, M) -> Com_1(f80(A, B, C, D, E, F, F - 1, H, I, J, K, L, M)) [ G - 1 >= 0 /\ F + G - 6 >= 0 /\ -F + G + 4 >= 0 /\ C + G - 7 >= 0 /\ B + G - 6 >= 0 /\ -B + G + 4 >= 0 /\ M + G - 51 >= 0 /\ -M + G + 49 >= 0 /\ A + G - 51 >= 0 /\ -A + G + 49 >= 0 /\ -F + 5 >= 0 /\ C - F - 1 >= 0 /\ B - F >= 0 /\ -B - F + 10 >= 0 /\ M - F - 45 >= 0 /\ -M - F + 55 >= 0 /\ A - F - 45 >= 0 /\ -A - F + 55 >= 0 /\ F - 5 >= 0 /\ C + F - 11 >= 0 /\ B + F - 10 >= 0 /\ -B + F >= 0 /\ M + F - 55 >= 0 /\ -M + F + 45 >= 0 /\ A + F - 55 >= 0 /\ -A + F + 45 >= 0 /\ C - 6 >= 0 /\ B + C - 11 >= 0 /\ -B + C - 1 >= 0 /\ M + C - 56 >= 0 /\ -M + C + 44 >= 0 /\ A + C - 56 >= 0 /\ -A + C + 44 >= 0 /\ -B + 5 >= 0 /\ M - B - 45 >= 0 /\ -M - B + 55 >= 0 /\ A - B - 45 >= 0 /\ -A - B + 55 >= 0 /\ B - 5 >= 0 /\ M + B - 55 >= 0 /\ -M + B + 45 >= 0 /\ A + B - 55 >= 0 /\ -A + B + 45 >= 0 /\ -M + 50 >= 0 /\ A - M >= 0 /\ -A - M + 100 >= 0 /\ M - 50 >= 0 /\ A + M - 100 >= 0 /\ -A + M >= 0 /\ -A + 50 >= 0 /\ A - 50 >= 0 /\ G >= F + 1 ] f54(A, B, C, D, E, F, G, H, I, J, K, L, M) -> Com_1(f50(A, B, C, D, E, F, G, H + 1, I, J, K, L, M)) [ H - 1 >= 0 /\ G + H - 1 >= 0 /\ -G + H - 1 >= 0 /\ F + H - 6 >= 0 /\ -F + H + 4 >= 0 /\ C + H - 7 >= 0 /\ B + H - 6 >= 0 /\ -B + H + 4 >= 0 /\ M + H - 51 >= 0 /\ -M + H + 49 >= 0 /\ J + H - 1 >= 0 /\ A + H - 51 >= 0 /\ -A + H + 49 >= 0 /\ -G + 4 >= 0 /\ F - G - 1 >= 0 /\ -F - G + 9 >= 0 /\ C - G - 2 >= 0 /\ B - G - 1 >= 0 /\ -B - G + 9 >= 0 /\ M - G - 46 >= 0 /\ -M - G + 54 >= 0 /\ J - G + 4 >= 0 /\ A - G - 46 >= 0 /\ -A - G + 54 >= 0 /\ G >= 0 /\ F + G - 5 >= 0 /\ -F + G + 5 >= 0 /\ C + G - 6 >= 0 /\ B + G - 5 >= 0 /\ -B + G + 5 >= 0 /\ M + G - 50 >= 0 /\ -M + G + 50 >= 0 /\ J + G >= 0 /\ A + G - 50 >= 0 /\ -A + G + 50 >= 0 /\ -F + 5 >= 0 /\ C - F - 1 >= 0 /\ B - F >= 0 /\ -B - F + 10 >= 0 /\ M - F - 45 >= 0 /\ -M - F + 55 >= 0 /\ J - F + 5 >= 0 /\ A - F - 45 >= 0 /\ -A - F + 55 >= 0 /\ F - 5 >= 0 /\ C + F - 11 >= 0 /\ B + F - 10 >= 0 /\ -B + F >= 0 /\ M + F - 55 >= 0 /\ -M + F + 45 >= 0 /\ J + F - 5 >= 0 /\ A + F - 55 >= 0 /\ -A + F + 45 >= 0 /\ C - 6 >= 0 /\ B + C - 11 >= 0 /\ -B + C - 1 >= 0 /\ M + C - 56 >= 0 /\ -M + C + 44 >= 0 /\ J + C - 6 >= 0 /\ A + C - 56 >= 0 /\ -A + C + 44 >= 0 /\ -B + 5 >= 0 /\ M - B - 45 >= 0 /\ -M - B + 55 >= 0 /\ J - B + 5 >= 0 /\ A - B - 45 >= 0 /\ -A - B + 55 >= 0 /\ B - 5 >= 0 /\ M + B - 55 >= 0 /\ -M + B + 45 >= 0 /\ J + B - 5 >= 0 /\ A + B - 55 >= 0 /\ -A + B + 45 >= 0 /\ -M + 50 >= 0 /\ J - M + 50 >= 0 /\ A - M >= 0 /\ -A - M + 100 >= 0 /\ M - 50 >= 0 /\ J + M - 50 >= 0 /\ A + M - 100 >= 0 /\ -A + M >= 0 /\ J >= 0 /\ A + J - 50 >= 0 /\ -A + J + 50 >= 0 /\ -A + 50 >= 0 /\ A - 50 >= 0 /\ J >= G + 1 ] f50(A, B, C, D, E, F, G, H, I, J, K, L, M) -> Com_1(f33(A, B, C, D, E, F, G + 1, H, I, J, K, L, M)) [ H - 1 >= 0 /\ G + H - 1 >= 0 /\ -G + H - 1 >= 0 /\ F + H - 6 >= 0 /\ -F + H + 4 >= 0 /\ C + H - 7 >= 0 /\ B + H - 6 >= 0 /\ -B + H + 4 >= 0 /\ M + H - 51 >= 0 /\ -M + H + 49 >= 0 /\ A + H - 51 >= 0 /\ -A + H + 49 >= 0 /\ G >= 0 /\ F + G - 5 >= 0 /\ -F + G + 5 >= 0 /\ C + G - 6 >= 0 /\ B + G - 5 >= 0 /\ -B + G + 5 >= 0 /\ M + G - 50 >= 0 /\ -M + G + 50 >= 0 /\ A + G - 50 >= 0 /\ -A + G + 50 >= 0 /\ -F + 5 >= 0 /\ C - F - 1 >= 0 /\ B - F >= 0 /\ -B - F + 10 >= 0 /\ M - F - 45 >= 0 /\ -M - F + 55 >= 0 /\ A - F - 45 >= 0 /\ -A - F + 55 >= 0 /\ F - 5 >= 0 /\ C + F - 11 >= 0 /\ B + F - 10 >= 0 /\ -B + F >= 0 /\ M + F - 55 >= 0 /\ -M + F + 45 >= 0 /\ A + F - 55 >= 0 /\ -A + F + 45 >= 0 /\ C - 6 >= 0 /\ B + C - 11 >= 0 /\ -B + C - 1 >= 0 /\ M + C - 56 >= 0 /\ -M + C + 44 >= 0 /\ A + C - 56 >= 0 /\ -A + C + 44 >= 0 /\ -B + 5 >= 0 /\ M - B - 45 >= 0 /\ -M - B + 55 >= 0 /\ A - B - 45 >= 0 /\ -A - B + 55 >= 0 /\ B - 5 >= 0 /\ M + B - 55 >= 0 /\ -M + B + 45 >= 0 /\ A + B - 55 >= 0 /\ -A + B + 45 >= 0 /\ -M + 50 >= 0 /\ A - M >= 0 /\ -A - M + 100 >= 0 /\ M - 50 >= 0 /\ A + M - 100 >= 0 /\ -A + M >= 0 /\ -A + 50 >= 0 /\ A - 50 >= 0 /\ H >= F + 1 ] f41(A, B, C, D, E, F, G, H, I, J, K, L, M) -> Com_1(f36(A, B, C, D, E, F, G, H + 1, I, J, K, L, M)) [ -H + 5 >= 0 /\ G - H + 4 >= 0 /\ -G - H + 9 >= 0 /\ F - H >= 0 /\ -F - H + 10 >= 0 /\ C - H - 1 >= 0 /\ B - H >= 0 /\ -B - H + 10 >= 0 /\ M - H - 45 >= 0 /\ -M - H + 55 >= 0 /\ J - H + 5 >= 0 /\ A - H - 45 >= 0 /\ -A - H + 55 >= 0 /\ H - 2 >= 0 /\ G + H - 3 >= 0 /\ -G + H - 1 >= 0 /\ F + H - 7 >= 0 /\ -F + H + 3 >= 0 /\ C + H - 8 >= 0 /\ B + H - 7 >= 0 /\ -B + H + 3 >= 0 /\ M + H - 52 >= 0 /\ -M + H + 48 >= 0 /\ J + H - 2 >= 0 /\ A + H - 52 >= 0 /\ -A + H + 48 >= 0 /\ -G + 4 >= 0 /\ F - G - 1 >= 0 /\ -F - G + 9 >= 0 /\ C - G - 2 >= 0 /\ B - G - 1 >= 0 /\ -B - G + 9 >= 0 /\ M - G - 46 >= 0 /\ -M - G + 54 >= 0 /\ J - G + 4 >= 0 /\ A - G - 46 >= 0 /\ -A - G + 54 >= 0 /\ G - 1 >= 0 /\ F + G - 6 >= 0 /\ -F + G + 4 >= 0 /\ C + G - 7 >= 0 /\ B + G - 6 >= 0 /\ -B + G + 4 >= 0 /\ M + G - 51 >= 0 /\ -M + G + 49 >= 0 /\ J + G - 1 >= 0 /\ A + G - 51 >= 0 /\ -A + G + 49 >= 0 /\ -F + 5 >= 0 /\ C - F - 1 >= 0 /\ B - F >= 0 /\ -B - F + 10 >= 0 /\ M - F - 45 >= 0 /\ -M - F + 55 >= 0 /\ J - F + 5 >= 0 /\ A - F - 45 >= 0 /\ -A - F + 55 >= 0 /\ F - 5 >= 0 /\ C + F - 11 >= 0 /\ B + F - 10 >= 0 /\ -B + F >= 0 /\ M + F - 55 >= 0 /\ -M + F + 45 >= 0 /\ J + F - 5 >= 0 /\ A + F - 55 >= 0 /\ -A + F + 45 >= 0 /\ C - 6 >= 0 /\ B + C - 11 >= 0 /\ -B + C - 1 >= 0 /\ M + C - 56 >= 0 /\ -M + C + 44 >= 0 /\ J + C - 6 >= 0 /\ A + C - 56 >= 0 /\ -A + C + 44 >= 0 /\ -B + 5 >= 0 /\ M - B - 45 >= 0 /\ -M - B + 55 >= 0 /\ J - B + 5 >= 0 /\ A - B - 45 >= 0 /\ -A - B + 55 >= 0 /\ B - 5 >= 0 /\ M + B - 55 >= 0 /\ -M + B + 45 >= 0 /\ J + B - 5 >= 0 /\ A + B - 55 >= 0 /\ -A + B + 45 >= 0 /\ -M + 50 >= 0 /\ J - M + 50 >= 0 /\ A - M >= 0 /\ -A - M + 100 >= 0 /\ M - 50 >= 0 /\ J + M - 50 >= 0 /\ A + M - 100 >= 0 /\ -A + M >= 0 /\ J >= 0 /\ A + J - 50 >= 0 /\ -A + J + 50 >= 0 /\ -A + 50 >= 0 /\ A - 50 >= 0 /\ J >= G ] f36(A, B, C, D, E, F, G, H, I, J, K, L, M) -> Com_1(f50(A, B, C, D, E, F, G, G + 1, I, J, K, L, M)) [ H - 1 >= 0 /\ G + H - 1 >= 0 /\ -G + H - 1 >= 0 /\ F + H - 6 >= 0 /\ -F + H + 4 >= 0 /\ C + H - 7 >= 0 /\ B + H - 6 >= 0 /\ -B + H + 4 >= 0 /\ M + H - 51 >= 0 /\ -M + H + 49 >= 0 /\ A + H - 51 >= 0 /\ -A + H + 49 >= 0 /\ -G + 4 >= 0 /\ F - G - 1 >= 0 /\ -F - G + 9 >= 0 /\ C - G - 2 >= 0 /\ B - G - 1 >= 0 /\ -B - G + 9 >= 0 /\ M - G - 46 >= 0 /\ -M - G + 54 >= 0 /\ A - G - 46 >= 0 /\ -A - G + 54 >= 0 /\ G >= 0 /\ F + G - 5 >= 0 /\ -F + G + 5 >= 0 /\ C + G - 6 >= 0 /\ B + G - 5 >= 0 /\ -B + G + 5 >= 0 /\ M + G - 50 >= 0 /\ -M + G + 50 >= 0 /\ A + G - 50 >= 0 /\ -A + G + 50 >= 0 /\ -F + 5 >= 0 /\ C - F - 1 >= 0 /\ B - F >= 0 /\ -B - F + 10 >= 0 /\ M - F - 45 >= 0 /\ -M - F + 55 >= 0 /\ A - F - 45 >= 0 /\ -A - F + 55 >= 0 /\ F - 5 >= 0 /\ C + F - 11 >= 0 /\ B + F - 10 >= 0 /\ -B + F >= 0 /\ M + F - 55 >= 0 /\ -M + F + 45 >= 0 /\ A + F - 55 >= 0 /\ -A + F + 45 >= 0 /\ C - 6 >= 0 /\ B + C - 11 >= 0 /\ -B + C - 1 >= 0 /\ M + C - 56 >= 0 /\ -M + C + 44 >= 0 /\ A + C - 56 >= 0 /\ -A + C + 44 >= 0 /\ -B + 5 >= 0 /\ M - B - 45 >= 0 /\ -M - B + 55 >= 0 /\ A - B - 45 >= 0 /\ -A - B + 55 >= 0 /\ B - 5 >= 0 /\ M + B - 55 >= 0 /\ -M + B + 45 >= 0 /\ A + B - 55 >= 0 /\ -A + B + 45 >= 0 /\ -M + 50 >= 0 /\ A - M >= 0 /\ -A - M + 100 >= 0 /\ M - 50 >= 0 /\ A + M - 100 >= 0 /\ -A + M >= 0 /\ -A + 50 >= 0 /\ A - 50 >= 0 /\ H >= F + 1 ] f33(A, B, C, D, E, F, G, H, I, J, K, L, M) -> Com_1(f66(A, B, C, D, E, F, 1, H, I, J, K, L, M)) [ G >= 0 /\ F + G - 5 >= 0 /\ -F + G + 5 >= 0 /\ C + G - 6 >= 0 /\ B + G - 5 >= 0 /\ -B + G + 5 >= 0 /\ M + G - 50 >= 0 /\ -M + G + 50 >= 0 /\ A + G - 50 >= 0 /\ -A + G + 50 >= 0 /\ -F + 5 >= 0 /\ C - F - 1 >= 0 /\ B - F >= 0 /\ -B - F + 10 >= 0 /\ M - F - 45 >= 0 /\ -M - F + 55 >= 0 /\ A - F - 45 >= 0 /\ -A - F + 55 >= 0 /\ F - 5 >= 0 /\ C + F - 11 >= 0 /\ B + F - 10 >= 0 /\ -B + F >= 0 /\ M + F - 55 >= 0 /\ -M + F + 45 >= 0 /\ A + F - 55 >= 0 /\ -A + F + 45 >= 0 /\ C - 6 >= 0 /\ B + C - 11 >= 0 /\ -B + C - 1 >= 0 /\ M + C - 56 >= 0 /\ -M + C + 44 >= 0 /\ A + C - 56 >= 0 /\ -A + C + 44 >= 0 /\ -B + 5 >= 0 /\ M - B - 45 >= 0 /\ -M - B + 55 >= 0 /\ A - B - 45 >= 0 /\ -A - B + 55 >= 0 /\ B - 5 >= 0 /\ M + B - 55 >= 0 /\ -M + B + 45 >= 0 /\ A + B - 55 >= 0 /\ -A + B + 45 >= 0 /\ -M + 50 >= 0 /\ A - M >= 0 /\ -A - M + 100 >= 0 /\ M - 50 >= 0 /\ A + M - 100 >= 0 /\ -A + M >= 0 /\ -A + 50 >= 0 /\ A - 50 >= 0 /\ G >= F ] f19(A, B, C, D, E, F, G, H, I, J, K, L, M) -> Com_1(f15(A, B, C + 1, D, E, F, G, H, I, J, K, L, M)) [ E >= 0 /\ C + E >= 0 /\ B + E - 5 >= 0 /\ -B + E + 5 >= 0 /\ A + E - 50 >= 0 /\ -A + E + 50 >= 0 /\ C >= 0 /\ B + C - 5 >= 0 /\ -B + C + 5 >= 0 /\ A + C - 50 >= 0 /\ -A + C + 50 >= 0 /\ -B + 5 >= 0 /\ A - B - 45 >= 0 /\ -A - B + 55 >= 0 /\ B - 5 >= 0 /\ A + B - 55 >= 0 /\ -A + B + 45 >= 0 /\ -A + 50 >= 0 /\ A - 50 >= 0 /\ E >= B + 1 ] f15(A, B, C, D, E, F, G, H, I, J, K, L, M) -> Com_1(f33(A, B, C, D, E, B, 0, H, I, J, K, L, A)) [ C >= 0 /\ B + C - 5 >= 0 /\ -B + C + 5 >= 0 /\ A + C - 50 >= 0 /\ -A + C + 50 >= 0 /\ -B + 5 >= 0 /\ A - B - 45 >= 0 /\ -A - B + 55 >= 0 /\ B - 5 >= 0 /\ A + B - 55 >= 0 /\ -A + B + 45 >= 0 /\ -A + 50 >= 0 /\ A - 50 >= 0 /\ C >= B + 1 ] )