Paradox and EquinoxEquinox is an automated theorem prover for pure first-order logic with equality. Equinox actually implements a hierarchy of logics, realized as a stack of theorem provers that use abstraction refinement to talk with each other. In the bottom sits an efficient SAT solver (MiniSat). The main aims of Equinox are (1) to be a theorem prover that performs well at large, automatically generated problems,
