Ecsedi-Tóth, P. and Varga, A. 1977. An effective theorem proving algorithm. Acta Cybernetica. 3, 3 (Jan. 1977), 249–260.