diff --git a/jukebox.cabal b/jukebox.cabal
--- a/jukebox.cabal
+++ b/jukebox.cabal
@@ -1,5 +1,5 @@
 Name: jukebox
-Version: 0.2.11
+Version: 0.2.13
 Cabal-version: >= 1.8
 Build-type: Simple
 Author: Nick Smallbone
diff --git a/src/Jukebox/Clausify.hs b/src/Jukebox/Clausify.hs
--- a/src/Jukebox/Clausify.hs
+++ b/src/Jukebox/Clausify.hs
@@ -20,11 +20,10 @@
 newtype ClausifyFlags = ClausifyFlags { splitting :: Bool } deriving Show
 
 clausifyFlags =
-  inGroup "Clausifier options" $
+  inGroup "Input and clausifier options" $
   ClausifyFlags <$>
     bool "split"
-      ["Split the conjecture into several sub-conjectures.",
-       "Default: (off)"]
+      ["Split the conjecture into several sub-conjectures."]
 
 ----------------------------------------------------------------------
 -- clausify
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
@@ -86,10 +86,10 @@
 
 tagsFlags :: OptionParser Bool
 tagsFlags =
+  inGroup "Options for encoding types" $
   bool "more-axioms"
-    ["Add extra typing axioms for function arguments,",
-     "when using typing tags.",
-     "These are unnecessary for completeness but may help (or hinder!) the prover."]
+    ["Add extra, redundant typing axioms for function arguments.",
+     "May help or hinder the prover. Only affects --encoding tags."]
 
 tags :: Bool -> Scheme
 tags moreAxioms = Scheme
diff --git a/src/Jukebox/Options.hs b/src/Jukebox/Options.hs
--- a/src/Jukebox/Options.hs
+++ b/src/Jukebox/Options.hs
@@ -193,7 +193,7 @@
 flag :: String -> [String] -> a -> ArgParser a -> OptionParser a
 flag name help def (Annotated desc (SeqParser args f)) =
   Annotated [desc'] (await name def g)
-  where desc' = Flag name "Common options" help desc
+  where desc' = Flag name "General options" help desc
         g xs =
           case f xs of
             Left (Mistake err) -> Error (Mistake ("Error in option --" ++ name ++ ": " ++ err))
@@ -271,8 +271,12 @@
   where f x | x == toolProgName t = Just (t, parser p')
         f _ = Nothing
         p' = p <* versionParser <* helpParser
-        helpParser = flag "help" ["Show this help text."] () (argUsage ExitSuccess (help t p'))
-        versionParser = flag "version" ["Print the version number."] () (argUsage ExitSuccess [greeting t])
+        helpParser =
+          inGroup "Miscellaneous options" $
+          flag "help" ["Show this help text."] () (argUsage ExitSuccess (help t p'))
+        versionParser =
+          inGroup "Miscellaneous options" $
+          flag "version" ["Print the version number."] () (argUsage ExitSuccess [greeting t])
 
 -- Use the program name as a tool name if possible.
 getEffectiveArgs :: ToolParser a -> IO [String]
@@ -328,22 +332,28 @@
 
 helpTool :: Tool -> ToolParser a -> ToolParser a
 helpTool t0 p = usageTool t0 "help" help "help for"
-  where help = concat [
+  where help = intercalate [""] [
           [greeting t0],
           usage t0 "<toolname> ",
-          ["<toolname> can be any of the following:"],
-          concat [ justify (toolProgName t) [toolHelp t] | t <- descr p ],
-          ["", "Use " ++ toolProgName t0 ++ " <toolname> --help for help on a particular tool."]
-          ]
+          ["Please run " ++ toolProgName t0 ++ " <toolname> --help, where <toolname> can be any of the following:"],
+          intercalate [""] [ justify (toolProgName t) [toolHelp t] | t <- descr p ]]
 
 help :: Tool -> OptionParser a -> [String]
-help t p = concat [
-  [greeting t],
-  usage t "",
-  ["<option> can be any of the following:"],
-  concat [ justify ("--" ++ flagName f ++ " " ++ flagArgs f) (flagHelp f) | f <- nub (descr p) ]
-  ]
+help t p =
+  intercalate [""]
+    [[greeting t],
+     usage t "",
+     intercalate [""] [
+       [flagGroup f0 ++ ":"] ++
+       concat [justify ("--" ++ flagName f ++ " " ++ flagArgs f) (flagHelp f) | f <- fs]
+       | fs@(f0:_) <- groups (nub (descr p)) ]]
 
+  where
+    groups [] = []
+    groups (f:fs) =
+      (f:[f' | f' <- fs, flagGroup f == flagGroup f']):
+      groups [f' | f' <- fs, flagGroup f /= flagGroup f']
+
 greeting :: Tool -> String
 greeting t = toolName t ++ ", version " ++ toolVersion t ++ "."
 
@@ -352,9 +362,8 @@
   "Usage: " ++ toolProgName t ++ " " ++ opts ++ "<option>* <file>*",
   toolHelp t ++ ".",
   "",
-  "<file> should be in TPTP format.",
-  ""
+  "<file> should be in TPTP format."
   ]
 
 justify :: String -> [String] -> [String]
-justify name help = ["", "  " ++ name] ++ map ("    " ++) help
+justify name help = ["  " ++ name] ++ map ("    " ++) help
diff --git a/src/Jukebox/TPTP/FindFile.hs b/src/Jukebox/TPTP/FindFile.hs
--- a/src/Jukebox/TPTP/FindFile.hs
+++ b/src/Jukebox/TPTP/FindFile.hs
@@ -32,6 +32,7 @@
         f _ = return []
 
 findFileFlags =
+  inGroup "Input and clausifier options" $
   concat <$>
   sequenceA [
     pure ["."],
diff --git a/src/Jukebox/Toolbox.hs b/src/Jukebox/Toolbox.hs
--- a/src/Jukebox/Toolbox.hs
+++ b/src/Jukebox/Toolbox.hs
@@ -28,11 +28,10 @@
 
 globalFlags :: OptionParser GlobalFlags
 globalFlags =
-  inGroup "Global options" $
+  inGroup "Output options" $
   GlobalFlags <$>
     bool "quiet"
-      ["Do not print any informational output.",
-       "Default: (off)"]
+      ["Do not print any informational output."]
 
 (=>>=) :: (Monad m, Applicative f) => f (a -> m b) -> f (b -> m c) -> f (a -> m c)
 f =>>= g = (>=>) <$> f <*> g
@@ -46,9 +45,18 @@
 greetingBox t = greetingBoxIO t <$> globalFlags
 
 greetingBoxIO :: Tool -> GlobalFlags -> IO ()
-greetingBoxIO t GlobalFlags{quiet = quiet} =
-  unless quiet $ hPutStrLn stderr (greeting t)
+greetingBoxIO t globals = message globals (greeting t)
 
+message :: GlobalFlags -> String -> IO ()
+message globals msg =
+  putStr (comment globals msg)
+
+comment :: GlobalFlags -> String -> String
+comment globals msg
+  | quiet globals = ""
+  | otherwise =
+    unlines ["% " ++ line | line <- lines msg]
+
 allFilesBox :: OptionParser ((FilePath -> IO ()) -> IO ())
 allFilesBox = flip allFiles <$> filenames
 
@@ -63,7 +71,7 @@
 
 parseProblemIO :: GlobalFlags -> [FilePath] -> FilePath -> IO (Problem Form)
 parseProblemIO flags dirs f = do
-  let found file = unless (quiet flags) $ hPutStrLn stderr $ "Reading " ++ file ++ "..."
+  let found file = message flags $ "Reading " ++ file ++ "..."
   r <- parseProblem found dirs f
   case r of
     Left err -> do
@@ -106,10 +114,10 @@
 
 schemeBox :: OptionParser Scheme
 schemeBox =
+  inGroup "Options for encoding types" $
   choose <$>
   flag "encoding"
-    ["Which type encoding to use.",
-     "Default: --encoding guards"]
+    ["Which type encoding to use (defaults to guards)."]
     "guards"
     (argOption ["guards", "tags"])
   <*> tagsFlags
@@ -153,47 +161,58 @@
 
 writeFileBox :: OptionParser (String -> IO ())
 writeFileBox =
+  inGroup "Output options" $
   flag "output"
-    ["Where to write the output.",
-     "Default: stdout"]
+    ["Where to write the output file (defaults to stdout)."]
     putStr
     (fmap myWriteFile argFile)
   where myWriteFile "/dev/null" _ = return ()
+        myWriteFile "-" contents = putStr contents
         myWriteFile file contents = writeFile file contents
 
 guessModelBox :: OptionParser (Problem Form -> IO (Problem Form))
-guessModelBox = guessModelIO <$> expansive <*> universe
+guessModelBox =
+  inGroup "Options for the model guesser:" $
+  guessModelIO <$> expansive <*> universe
   where universe = choose <$>
                    flag "universe"
-                   ["Which universe to find the model in.",
-                    "Default: peano"]
+                   ["Which universe to find the model in (defaults to peano)."]
                    "peano"
                    (argOption ["peano", "trees"])
         choose "peano" = Peano
         choose "trees" = Trees
         expansive = manyFlags "expansive"
-                    ["Allow a function to construct 'new' terms in its base base."]
+                    ["Allow a function to construct 'new' terms in its base case."]
                     (arg "<function>" "expected a function name" Just)
 
 guessModelIO :: [String] -> Universe -> Problem Form -> IO (Problem Form)
 guessModelIO expansive univ prob = return (guessModel expansive univ prob)
 
 allObligsBox :: OptionParser ((Problem Clause -> IO Answer) -> CNF -> IO ())
-allObligsBox = pure allObligsIO
+allObligsBox = allObligsIO <$> globalFlags
 
-allObligsIO solve CNF{..} = loop 1 conjectures
-  where loop _ [] = result unsatisfiable
+allObligsIO globals solve CNF{..} = loop 1 conjectures
+  where loop _ [] =
+          result unsatisfiable
+            "PROVED.\nThe conjecture is true or the axioms are contradictory."
         loop i (c:cs) = do
-          when multi $ putStrLn $ "Part " ++ part i
+          when multi $ putStr $ comment globals $ "Part " ++ part i
           answer <- solve (axioms ++ c)
-          when multi $ putStrLn $ "+++ PARTIAL (" ++ part i ++ "): " ++ show answer
+          when multi $ putStr $ comment globals $ "Partial result (" ++ part i ++ "): " ++ show answer
           case answer of
-            Satisfiable -> result satisfiable
+            Satisfiable ->
+              result satisfiable
+                "DISPROVED.\nThe conjecture is not true and the axioms are consistent."
             Unsatisfiable -> loop (i+1) cs
-            NoAnswer x -> result (show x)
+            NoAnswer x ->
+              result (show x)
+                "GAVE UP.\nCouldn't prove or disprove the conjecture."
         multi = length conjectures > 1
         part i = show i ++ "/" ++ show (length conjectures)
-        result x = putStrLn ("% SZS status " ++ x)
+        result x hint = do
+          message globals ("SZS status " ++ x)
+          putStrLn ""
+          message globals hint
 
 inferBox :: OptionParser (Problem Clause -> IO (Problem Clause, Type -> Type))
 inferBox = (\globals prob -> do