EQP is not as stable and polished as our main production theorem prover Otter. But it has obtained several interesting results, and we have decided to make it available (including the source code) to everyone, with no restrictions (and of course no warranty). EQP's documentation is not good, but if you already know Otter, you might not have great difficulty in learning to use EQP.
Here is the whole package by FTP, including the source code, users' guide, and example input files. For a quick preview, see the README file, the users' guide, and the ChangeLog file.
These activities are projects of the Mathematics and Computer Science Division of Argonne National Laboratory.