diff --git a/executable/Main.hs b/executable/Main.hs
--- a/executable/Main.hs
+++ b/executable/Main.hs
@@ -18,8 +18,8 @@
   args <- getArgs
   let
     progTool = prog ++ " <toolname>"
-    help =
-      printHelp ExitSuccess $
+    help code =
+      printHelp code $
         intercalate [""] $
           [usageText progTool "Jukebox, a first-order logic toolbox"] ++
           [["<toolname> can be any of the following:"] ++
@@ -28,9 +28,9 @@
           [["For more information about each tool, run " ++ progTool ++ " --help."]]
     usage msg = printError prog msg
   case args of
-    [] -> help
-    ["help"] -> help
-    ["--help"] -> help
+    [] -> help (ExitFailure 1)
+    ["help"] -> help ExitSuccess
+    ["--help"] -> help ExitSuccess
     ["--version"] ->
       putStrLn $ "Jukebox version " ++
 #ifdef VERSION_jukebox
diff --git a/jukebox.cabal b/jukebox.cabal
--- a/jukebox.cabal
+++ b/jukebox.cabal
@@ -1,5 +1,5 @@
 Name: jukebox
-Version: 0.5.9
+Version: 0.5.10
 Cabal-version: >= 1.10
 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
@@ -651,11 +651,7 @@
   bind (Bind vs _) = map typ (Set.toList vs)
 
   inp :: Symbolic a => Input a -> [Type]
-  inp (Input _ _ _ source _) =
-    case source of
-      Inference _ _ inps ->
-        concatMap inputTypes inps
-      _ -> []
+  inp _ = []
 
 types' :: Symbolic a => a -> [Type]
 types' = filter (/= O) . types
diff --git a/src/Jukebox/Options.hs b/src/Jukebox/Options.hs
--- a/src/Jukebox/Options.hs
+++ b/src/Jukebox/Options.hs
@@ -307,8 +307,13 @@
 
 printHelp :: ExitCode -> [String] -> IO a
 printHelp code xs = do
-  mapM_ (hPutStrLn stderr) xs
+  mapM_ (hPutStrLn handle) xs
   exitWith code
+  where
+    handle =
+      case code of
+        ExitSuccess -> stdout
+        ExitFailure _ -> stderr
 
 printError :: String -> String -> IO a
 printError name err =
diff --git a/src/Jukebox/TPTP/ParseSnippet.hs b/src/Jukebox/TPTP/ParseSnippet.hs
--- a/src/Jukebox/TPTP/ParseSnippet.hs
+++ b/src/Jukebox/TPTP/ParseSnippet.hs
@@ -19,6 +19,9 @@
 tff = form TPTP.Parse.Core.tff
 cnf = form TPTP.Parse.Core.cnf
 
+term :: [(String, Type)] -> [(String, Function)] -> String -> Term
+term = form (TPTP.Parse.Core.term NoQuantification Map.empty)
+
 form :: Symbolic a => Parser a -> [(String, Type)] -> [(String, Function)] -> String -> a
 form parser types0 funs0 str =
   case run_ (parser <* eof)
@@ -33,8 +36,8 @@
                 show (map snd (Map.toList funs' \\ Map.toList funs))
       | otherwise -> mapType elimI res
     Ok{} -> error "ParseSnippet: lexical error"
-    TPTP.Parsec.Error _ msg -> error $ "ParseSnippet: parse error: " ++ msg
-    Expected _ exp -> error $ "ParseSnippet: parse error: expected " ++ show exp
+    TPTP.Parsec.Error _ msg -> error $ "ParseSnippet: parse error: " ++ msg ++ " for " ++ str
+    Expected _ exp -> error $ "ParseSnippet: parse error: expected " ++ show exp ++ " for " ++ str
 
   where
     funs = Map.mapKeys intern $ Map.fromList $ map (mapFunType introI) funs0
@@ -53,3 +56,11 @@
         Nothing -> id
         Just i ->
           \ty -> if ty == i then indType else ty
+
+giveProblem :: Symbolic a => a -> ([(String, Type)] -> [(String, Function)] -> String -> b) -> String -> b
+giveProblem prob cont str =
+  cont (extract (types prob)) (extract (functions prob)) str
+  where
+    extract :: Named a => [a] -> [(String, a)]
+    extract xs =
+      [(unintern sym, x) | x <- xs, Fixed (Basic sym) _ <- [name x]]