DTP Prover, the Don Theorem Prover is described as 'an inference engine for first-order predicate calculus, [specialized] in domain-independent control of reasoning.'
The source for DTP Prover is available here
(and previously here, but that link is broken.)