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."