diff --git a/dist/build/Jukebox/TPTP/Lexer.hs b/dist/build/Jukebox/TPTP/Lexer.hs
--- a/dist/build/Jukebox/TPTP/Lexer.hs
+++ b/dist/build/Jukebox/TPTP/Lexer.hs
@@ -323,12 +323,190 @@
 
 
 
+{-# LINE 9 "<command-line>" #-}
+{-# LINE 1 "/usr/lib/ghc-8.0.1/include/ghcversion.h" #-}
 
 
 
 
+
+
+
+
+
+
+
+
+
+
+
+
+
 {-# LINE 9 "<command-line>" #-}
-{-# LINE 1 "/usr/lib/ghc-7.10.3/include/ghcversion.h" #-}
+{-# LINE 1 "/tmp/ghc684_0/ghc_2.h" #-}
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
 
 
 
diff --git a/jukebox.cabal b/jukebox.cabal
--- a/jukebox.cabal
+++ b/jukebox.cabal
@@ -1,5 +1,5 @@
 Name: jukebox
-Version: 0.2.7
+Version: 0.2.8
 Cabal-version: >= 1.8
 Build-type: Simple
 Author: Nick Smallbone
diff --git a/src/Jukebox/Form.hs b/src/Jukebox/Form.hs
--- a/src/Jukebox/Form.hs
+++ b/src/Jukebox/Form.hs
@@ -543,7 +543,8 @@
   term _ = mempty
 
 isFof :: Symbolic a => a -> Bool
-isFof f = length (types' f) <= 1
+isFof _ = False
+--isFof f = length (types' f) <= 1
 
 uniqueNames :: Symbolic a => a -> NameM a
 uniqueNames t = evalStateT (aux Map.empty t) (Map.fromList [(x, t) | x ::: t <- Set.toList (free t)])
diff --git a/src/Jukebox/Monotonox/ToFOF.hs b/src/Jukebox/Monotonox/ToFOF.hs
--- a/src/Jukebox/Monotonox/ToFOF.hs
+++ b/src/Jukebox/Monotonox/ToFOF.hs
@@ -78,7 +78,9 @@
                 Axiom -> prepare f
                 Conjecture -> fmap notInwards (prepare (nt f))
       typeI = Type (name "$i") (Finite 0) Infinite
-  in Form.run (translate1 scheme mono f') (return . mapType (const typeI))
+      trType O = O
+      trType ty = typeI
+  in Form.run (translate1 scheme mono f') (return . mapType trType)
 
 -- Typing functions.
 
diff --git a/src/Jukebox/SMTLIB.hs b/src/Jukebox/SMTLIB.hs
--- a/src/Jukebox/SMTLIB.hs
+++ b/src/Jukebox/SMTLIB.hs
@@ -25,6 +25,8 @@
     , "and"
     , "axiom"
     , "inversion"
+    , "bit0"
+    , "bit1"
     , "bitv"
     , "bool"
     , "check"
diff --git a/src/Jukebox/TPTP/Parse.hs b/src/Jukebox/TPTP/Parse.hs
--- a/src/Jukebox/TPTP/Parse.hs
+++ b/src/Jukebox/TPTP/Parse.hs
@@ -8,7 +8,6 @@
 import Jukebox.Form hiding (Pos, run)
 import Control.Exception
 import Data.List
-import System.IO
 
 parseString :: String -> IO (Problem Form)
 parseString xs =
@@ -20,11 +19,11 @@
     Parser.ParseStalled loc _ _ ->
       error ("Include directive found at " ++ show loc)
 
-parseProblem :: [FilePath] -> FilePath -> IO (Either String (Problem Form))
-parseProblem dirs name = parseProblemWith (findFileTPTP dirs) name
+parseProblem :: (FilePath -> IO ()) -> [FilePath] -> FilePath -> IO (Either String (Problem Form))
+parseProblem found dirs name = parseProblemWith found (findFileTPTP dirs) name
 
-parseProblemWith :: (FilePath -> IO (Maybe FilePath)) -> FilePath -> IO (Either String (Problem Form))
-parseProblemWith findFile name =
+parseProblemWith :: (FilePath -> IO ()) -> (FilePath -> IO (Maybe FilePath)) -> FilePath -> IO (Either String (Problem Form))
+parseProblemWith found findFile name =
   runExceptT $ do
     file <- readInFile (Parser.Location "<command line>" 0 0) name
     process (Parser.parseProblem name file)
@@ -41,7 +40,7 @@
           err pos ("File '" ++ name ++ "' not found")
         Just file ->
           ExceptT $ do
-            liftIO $ hPutStrLn stderr $ "Reading " ++ file ++ "..."
+            liftIO (found file)
             fmap Right (readFile file) `catch`
               \(e :: IOException) -> return (Left (show e))
 
diff --git a/src/Jukebox/TPTP/Print.hs b/src/Jukebox/TPTP/Print.hs
--- a/src/Jukebox/TPTP/Print.hs
+++ b/src/Jukebox/TPTP/Print.hs
@@ -37,7 +37,7 @@
 showProblem = show . pPrintProblem
 
 isReallyFof :: Symbolic a => a -> Bool
-isReallyFof = all p . types
+isReallyFof = const False -- all p . types
   where
     p O = True
     p (Type ty _ _) | ty == i = True
diff --git a/src/Jukebox/Toolbox.hs b/src/Jukebox/Toolbox.hs
--- a/src/Jukebox/Toolbox.hs
+++ b/src/Jukebox/Toolbox.hs
@@ -59,11 +59,12 @@
 allFiles f xs = mapM_ f xs
 
 parseProblemBox :: OptionParser (FilePath -> IO (Problem Form))
-parseProblemBox = parseProblemIO <$> findFileFlags
+parseProblemBox = parseProblemIO <$> globalFlags <*> findFileFlags
 
-parseProblemIO :: [FilePath] -> FilePath -> IO (Problem Form)
-parseProblemIO dirs f = do
-  r <- parseProblem dirs f
+parseProblemIO :: GlobalFlags -> [FilePath] -> FilePath -> IO (Problem Form)
+parseProblemIO flags dirs f = do
+  let found file = unless (quiet flags) $ hPutStrLn stderr $ "Reading " ++ file ++ "..."
+  r <- parseProblem found dirs f
   case r of
     Left err -> do
       hPutStrLn stderr err
@@ -197,7 +198,7 @@
             NoAnswer x -> result (show x)
         multi = length conjectures > 1
         part i = show i ++ "/" ++ show (length conjectures)
-        result x = putStrLn ("+++ RESULT: " ++ x)
+        result x = putStrLn ("% SZS status " ++ x)
 
 inferBox :: OptionParser (Problem Clause -> IO (Problem Clause, Type -> Type))
 inferBox = (\globals prob -> do