* METEOR

METEOR is a theorem prover based on Model Elimination. It runs on Unix machines and networks of Unix machines (and used to run on the BBN Butterfly TC2000)

There are several papers describing METEOR, theoretical and empirical results, and modifications to the search mechanism