>Proofs are (currently) based on resolution Proofs are actually based on a practical version of extended resolution [1] called DRAT. Extended resolution is an

>Proofs are (currently) based on resolution Proofs are actually based on a practical version of extended resolution [1] called DRAT. Extended resolution is an extremely strong proof system, and research on techniques that are not efficiently modelled by resolution are in fact being prioritised (see for instance [2]). This is not to say that CreuSAT is not very impressive, but just a correction on the current state of the things. [1]: https://en.wikipedia.org/wiki/Frege_system#Extended_Frege_system https://en.wikipedia.org/wiki/Frege_system#Extended_Frege_sy... [2]: https://link.springer.com/chapter/10.1007/978-3-642-31365-3_28 https://link.springer.com/chapter/10.1007/978-3-642-31365-3_...