P. Ecsedi-Tóth and A. Varga, “An effective theorem proving algorithm”, Acta Cybern, vol. 3, no. 3, pp. 249-260, Jan. 1977.