Mixed-integer programs (MIPs) involving logical implications modeled through big-M coefficients are notoriously among the hardest to solve. In this paper, we propose and analyze computationally an automatic problem reformulation of quite general applicability, aimed at removing the model dependency on the big-M coefficients. Our solution scheme defines a master integer linear problem (ILP) with no continuous variables, which contains combinatorial information on the feasible integer variable combinations that can be \u201cdistilled\u201d from the original MIP model. The master solutions are sent to a slave linear program (LP), which validates them and possibly returns combinatorial inequalities to be added to the current master ILP. The ine...