The most recent version of Metis can be downloaded from http://www.gilith.com/software/metis/.
The Metis home page contains a collection of links to resources.
The command metis --help is used to display tool help.
Unfortunately there is no documentation for the source code of Metis, but one design goal of the code was to make it readable, and I'd be happy to answer questions about it emailed to metis-users@gilith.com
There is an email list for Metis users: you can subscribe and view the archives at http://www.gilith.com/mailman/listinfo/metis-users.
I strongly recommend using MLton (or Poly/ML) over Moscow ML to run opentheory, for reasons of speed (MLton is about 10 times faster than Moscow ML).
Metis is doing a paramodulation step internally, but this is broken down in the CNF refutation into one of six simple inference rules, which are described in doc/logical-kernel.txt and can be found in the Thm module of the source code.
The approach of breaking proofs down into tiny inference rules is done to make it easier to replay the proofs when Metis is being used as a tactic in a higher order logic theorem prover, but it makes the proofs less readable.
