--- a/auto-proof.rst	Thu Apr 16 21:18:40 2009 +0300
+++ b/auto-proof.rst	Thu Apr 16 21:24:25 2009 +0300
@@ -75,8 +75,10 @@
 
 * PVS Specification and Verification System
 
-Old (1992). The system is implemented in Common Lisp, and is released under
-the GNU General Public License (GPL).
+Old (1992). Many article in 199x.
+
+The system is implemented in Common Lisp, and is released under the GNU
+General Public License (GPL).
 
 See
 
@@ -110,3 +112,11 @@
 See
 
   http://www.cs.miami.edu/~tptp/
+
+* SPASS.
+
+An Automated Theorem Prover for First-Order Logic with Equality.
+
+See
+
+  http://www.spass-prover.org/index.html