math/otter - The NetBSD Packages Collection

Otter (Organized Techniques for Theorem-proving and Effective
Research) is a resolution-style theorem-proving program for
first-order logic with equality.  Otter includes the inference rules
binary resolution, hyperresolution, UR-resolution, and binary
paramodulation.  Some of its other abilities and features are
conversion from first-order formulas to clauses, forward and back
subsumption, factoring, weighting, answer literals, term ordering,
forward and back demodulation, evaluable functions and predicates, and
Knuth-Bendix completion.  Otter is coded in C, is free, and is
portable to many different kinds of computer.