Start with an example
Each one is a file committed to this repository, checked on every push.
Loading the checker…
Or check your own
No file chosen
No file chosen
No proof checked yet.
A SAT solver answering unsatisfiable is an assertion, not a proof. Drop a DIMACS formula and its DRAT or LRAT refutation below and this page will check every step of it, here, in this tab.
Nothing is uploaded. The checker is a 73 KB WebAssembly module that imports nothing at all — it has no way to call out. Open the network tab and watch.
Each one is a file committed to this repository, checked on every push.
Loading the checker…
No file chosen
No file chosen
No proof checked yet.