Title:   Have SPASS with OCC1N^=_g
Authors:Christian G. Fermuller, Georeg Moser

Abstract:

We prove that a particular superposition based inference operator
decides a fragment of clause logic with equality, called OCC1N^=_g.  
We also show that the theorem prover SPASS not only implements the 
corresponding operator, but also generates standard descriptions of
unique term models for all satisfiable clause sets in OCC1N^=_g.