Paradox is a finite-domain model finder for pure first-order logic with equality.
Paradox is a MACE-style model finder, which means that it translates a first-order problem into a
sequence of SAT problems, which are solved by a SAT solver (in our case MiniSat).
Paradox is the proud winner of the SAT/Models division of the CASC World Championship on First-Order
Automated Theorem Proving in 2003, 2004, 2005 and 2006.
These details are provided for information only. No information here is legal advice and should not be used as such.