Using sophisticated models in resolution theorem proving - Sandford, David M. (Springer Verlag, 1980)