Metis is an automatic theorem prover for first order logic with equality. Features of Metis * Coded in Standard ML (SML), with an emphasis on keeping the code as simple as possible. * Compiled using MLton to give respectable performance on standard benchmarks. * Reads in problems in the standard .tptp file format of the TPTP problem set. * Outputs detailed proofs in TSTP format, where each proof step is one of 6 simple rules. * Outputs saturated clause sets when input problems are discovered to be unprovable. Project Status Metis is being actively developed