An Implementation of the Model Elimination Proof Procedure. - S. Fleisig; Donald W. Loveland; A. K. Smiley III; D. L. Yarmush (J. ACM, 1974)