We prove that the Cutting Plane proof system based on
Gomory-Chvatal cuts polynomially simulates the
lift-and-project system with integer coefficients
written in unary. The restriction on coefficients can be
omitted when using Krajicek's cut-free Gentzen-style extension
of both systems. We also prove that Tseitin tautologies
have short proofs in ... more >>>