diff --git a/Jukebox/Provers/SPASS.hs b/Jukebox/Provers/SPASS.hs
new file mode 100644
--- /dev/null
+++ b/Jukebox/Provers/SPASS.hs
@@ -0,0 +1,67 @@
+{-# LANGUAGE GADTs #-}
+module Jukebox.Provers.SPASS where
+
+import Jukebox.Form hiding (tag, Or)
+import Jukebox.Name
+import Jukebox.Options
+import Control.Applicative hiding (Const)
+import Control.Monad
+import Jukebox.Utils
+import Jukebox.TPTP.Parsec
+import Jukebox.TPTP.ClauseParser hiding (newFunction, Term)
+import Jukebox.TPTP.Print
+import Jukebox.TPTP.Lexer hiding (Normal, keyword, Axiom, name, Var)
+import Text.PrettyPrint.HughesPJ hiding (parens)
+import Data.Maybe
+import qualified Data.ByteString.Char8 as BS
+import qualified Data.ByteString.Lazy.Char8 as BSL
+import qualified Jukebox.Seq as S
+import qualified Jukebox.Map as Map
+import Jukebox.Map(Map)
+import Data.Hashable
+import System.Exit
+
+data SPASSFlags =
+  SPASSFlags {
+    spass   :: String,
+    timeout :: Maybe Int,
+    sos     :: Bool }
+
+spassFlags =
+  inGroup "SPASS prover options" $
+  SPASSFlags <$>
+    flag "spass"
+      ["Path to SPASS.",
+       "Default: SPASS"]
+      "SPASS"
+      argFile <*>
+    flag "timeout"
+      ["Timeout in seconds.",
+       "Default: (none)"]
+      Nothing
+      (fmap Just argNum) <*>
+    flag "sos"
+      ["Use set-of-support strategy.",
+       "Default: false"]
+      False
+      (pure True)
+
+runSPASS :: (Pretty a, Symbolic a) => SPASSFlags -> Problem a -> IO Answer
+runSPASS flags prob
+  | not (isFof (open prob)) = error "runSPASS: SPASS doesn't support many-typed problems"
+  | otherwise = do
+    (code, str) <- popen (spass flags) spassFlags
+                   (BS.pack (render (prettyProblem "cnf" Normal prob)))
+    return (extractAnswer (BS.unpack str))
+  where
+    spassFlags =
+      ["-TimeLimit=" ++ show n | Just n <- [timeout flags] ] ++
+      ["-SOS" | sos flags] ++
+      ["-TPTP", "-Stdin"]
+
+extractAnswer :: String -> Answer
+extractAnswer result =
+  head $
+    [ Unsatisfiable    | "SPASS beiseite: Proof found." <- lines result ] ++
+    [ Satisfiable      | "SPASS beiseite: Completion found." <- lines result ] ++
+    [ NoAnswer Timeout ]
diff --git a/jukebox.cabal b/jukebox.cabal
--- a/jukebox.cabal
+++ b/jukebox.cabal
@@ -1,5 +1,5 @@
 Name: jukebox
-Version: 0.1.1
+Version: 0.1.2
 Cabal-version: >= 1.8
 Build-type: Simple
 Author: Nick Smallbone
@@ -38,6 +38,7 @@
     Jukebox.Options
     Jukebox.ProgressBar
     Jukebox.Provers.E
+    Jukebox.Provers.SPASS
     Jukebox.Sat3
     Jukebox.SatEq
     Jukebox.Sat