Related tools

CVC-lite
ICS
BarcelogicTools

Various links

haRVey-FOL uses the E-prover to check the satisfiability of literals within a given first-order theory.
haRVey-SAT has been successfully combined with the proof-Assistant Isabelle.
haRVey-SAT uses the SMT-lib input language Version 1.1.
haRVey-SAT can be used with the MiniSat SAT solver, or with zChaff.
The old haRVey page.