A resolution based theorem prover for first-order logic with equality.

TPTP format is used for both problem input and proof output. Problems can be in clause (CNF) or general first-order (FOF) form.

Inference rules used are binary resolution, factoring and paramodulation. Performance is as yet poor, primarily because inference control is still mostly on the to-do list.