The Stabbing Planes proof system was introduced to model the reasoning carried out in practical mixed integer programming solvers. As a proof system, it is powerful enough to simulate Cutting Planes and to refute the Tseitin formulas -- certain unsatisfiable systems of linear equations mod 2 -- which are canonical ... more >>>