SPASS is an automated theorem prover for full first-order logic with equality and a number of non-classical logics. We describe our recent developments in SPASS 3.5
