diff --git a/jukebox.cabal b/jukebox.cabal
--- a/jukebox.cabal
+++ b/jukebox.cabal
@@ -1,5 +1,5 @@
 Name: jukebox
-Version: 0.2.10
+Version: 0.2.11
 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
@@ -41,7 +41,7 @@
       -- if there is a model of size >= tsize then there is a model of size tsize
       tsize :: DomainSize } deriving Typeable
 
-data FunType = FunType { args :: [Type], res :: Type } deriving (Eq, Typeable)
+data FunType = FunType { args :: [Type], res :: Type } deriving (Eq, Ord, Typeable)
 
 -- Helper function for defining (Eq, Ord) instances
 typeMaybeName :: Type -> Maybe Name
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
@@ -57,7 +57,7 @@
     funcDecl (f ::: ty) = typeClause f (pPrint ty)
     typeClause name ty =
       pPrintClause "tff" "type" "type"
-        (pPrint name <> colon <+> ty)
+        (text (escapeAtom (show name)) <> colon <+> ty)
 
 instance Pretty a => Pretty (Input a) where
   pPrint = pPrintInput "tff" pPrint
diff --git a/src/Jukebox/Toolbox.hs b/src/Jukebox/Toolbox.hs
--- a/src/Jukebox/Toolbox.hs
+++ b/src/Jukebox/Toolbox.hs
@@ -76,7 +76,6 @@
 
 clausifyIO :: GlobalFlags -> ClausifyFlags -> Problem Form -> IO CNF
 clausifyIO globals flags prob = do
-  unless (quiet globals) $ hPutStrLn stderr "Clausifying problem..."
   return $! clausify flags prob
 
 toFofBox :: OptionParser (Problem Form -> IO (Problem Form))
@@ -95,7 +94,6 @@
 toFofIO :: GlobalFlags -> (Problem Form -> IO CNF) -> Scheme -> Problem Form -> IO (Problem Form)
 toFofIO globals clausify scheme f = do
   CNF{..} <- clausify f
-  unless (quiet globals) $ hPutStrLn stderr "Monotonicity analysis..."
   -- In some cases we might get better results by considering each
   -- problem (axioms + conjecture) separately, but no big deal.
   m <- monotone (map what (axioms ++ concat conjectures))
@@ -123,7 +121,6 @@
 
 monotonicity :: GlobalFlags -> Problem Clause -> IO String
 monotonicity globals cs = do
-  unless (quiet globals) $ hPutStrLn stderr "Monotonicity analysis..."
   m <- monotone (map what cs)
   let info (ty, Nothing) = [base ty ++ ": not monotone"]
       info (ty, Just m) =
@@ -139,7 +136,6 @@
 
 annotateMonotonicityBox :: OptionParser (Problem Clause -> IO (Problem Clause))
 annotateMonotonicityBox = (\globals x -> do
-  unless (quiet globals) $ putStrLn "Monotonicity analysis..."
   annotateMonotonicity x) <$> globalFlags
 
 prettyPrintProblemBox :: OptionParser (Problem Form -> IO ())
@@ -153,7 +149,6 @@
 
 prettyPrintIO :: (a -> String) -> GlobalFlags -> (String -> IO ()) -> a -> IO ()
 prettyPrintIO shw globals write prob = do
-  unless (quiet globals) $ hPutStrLn stderr "Writing output..."
   write (shw prob ++ "\n")
 
 writeFileBox :: OptionParser (String -> IO ())
@@ -202,7 +197,6 @@
 
 inferBox :: OptionParser (Problem Clause -> IO (Problem Clause, Type -> Type))
 inferBox = (\globals prob -> do
-  unless (quiet globals) $ putStrLn "Inferring types..."
   return (run prob inferTypes)) <$> globalFlags
 
 printInferredBox :: OptionParser ((Problem Clause, Type -> Type) -> IO (Problem Clause))