Abstract

We prove that the Cutting Plane proof system based on Gomory–Chvátal cuts polynomially simulates the lift-and-project system with integer coefficients written in unary. The restriction on the coefficients can be omitted when using Krajíček’s cut-free Gentzen-style extension of both systems. We also prove that Tseitin tautologies have short proofs in this extension