@conference {inp:BlanchettePopescuWandWeidenbach2012, title = {More SPASS with Isabelle - Superposition with Hard Sorts and Configurable Simplification}, booktitle = {Proceedings of the 3rd Conference on Interactive Theorem Proving (ITP 2012)}, year = {2012}, author = {J. C. Blanchette and A. Popescu and D. Wand and C. Weidenbach} }