ProverX

This is the kernel of the whole system. 

Produced with Yves Robert and Bob Veroff, this tool integrates several different packages for ATP.