Paradox is a finite-domain model finder for pure first-order logic (FOL) with equality developed by Koen Lindström Claessen and Niklas Sörensson at the Chalmers University of Technology.
<!-- Primary and non independent -->
<!-- Alt reference that cant be waybacked: http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.817.9812&rep=rep1&type=pdf -->