SNARK
SNARK (SRI's New Automated Reasoning Kit) is described as "an automated theorem-proving program" being developed in Common Lisp. Its principal inference rules are resolution and paramodulation. SNARK's style of theorem proving is similar to Otter's."

SNARK is available here under the Mozilla Public License.

Application Theorem Provers