diff --git a/jukebox.cabal b/jukebox.cabal
--- a/jukebox.cabal
+++ b/jukebox.cabal
@@ -1,5 +1,5 @@
 Name: jukebox
-Version: 0.2.1
+Version: 0.2.2
 Cabal-version: >= 1.8
 Build-type: Simple
 Author: Nick Smallbone
diff --git a/src/Jukebox/TPTP/Parse/Core.hs b/src/Jukebox/TPTP/Parse/Core.hs
--- a/src/Jukebox/TPTP/Parse/Core.hs
+++ b/src/Jukebox/TPTP/Parse/Core.hs
@@ -306,7 +306,9 @@
 cnf = do
   MkState p t f _ n <- getState
   putState (MkState p t f Map.empty n)
-  formula NoQuantification __
+  form <- formula NoQuantification __
+  MkState _ _ _ vs _ <- getState
+  return (ForAll (Bind (Set.fromList (Map.elems vs)) form))
 tff = formula Typed Map.empty
 fof = formula Untyped Map.empty
 
diff --git a/src/Jukebox/Toolbox.hs b/src/Jukebox/Toolbox.hs
--- a/src/Jukebox/Toolbox.hs
+++ b/src/Jukebox/Toolbox.hs
@@ -89,9 +89,11 @@
 
 toFofIO :: GlobalFlags -> (Problem Form -> IO CNF) -> Scheme -> Problem Form -> IO (Problem Form)
 toFofIO globals clausify scheme f = do
-  cs <- clausify f >>= oneConjecture
+  CNF{..} <- clausify f
   unless (quiet globals) $ hPutStrLn stderr "Monotonicity analysis..."
-  m <- monotone (map what cs)
+  -- 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))
   let isMonotone ty =
         case Map.lookup ty m of
           Just Nothing -> False