DTP Prover
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.)

Application Theorem Provers