The source for DTP Prover is available here (and previously here, but that link is broken.)

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