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
@@ -132,7 +132,7 @@
 unquote :: String -> String
 unquote (_:x)
   | null z = init y
-  | otherwise = y ++ [z !! 1] ++ unquote (drop 2 z)
+  | otherwise = y ++ [z !! 1] ++ unquote (drop 1 z)
   where (y, z) = break (== '\\') x
 
 readRational :: String -> Rational
diff --git a/jukebox.cabal b/jukebox.cabal
--- a/jukebox.cabal
+++ b/jukebox.cabal
@@ -1,5 +1,5 @@
 Name: jukebox
-Version: 0.2.13.1
+Version: 0.2.14
 Cabal-version: >= 1.8
 Build-type: Simple
 Author: Nick Smallbone
diff --git a/src/Jukebox/TPTP/Lexer.x b/src/Jukebox/TPTP/Lexer.x
--- a/src/Jukebox/TPTP/Lexer.x
+++ b/src/Jukebox/TPTP/Lexer.x
@@ -173,7 +173,7 @@
 unquote :: String -> String
 unquote (_:x)
   | null z = init y
-  | otherwise = y ++ [z !! 1] ++ unquote (drop 2 z)
+  | otherwise = y ++ [z !! 1] ++ unquote (drop 1 z)
   where (y, z) = break (== '\\') x
 
 readRational :: String -> Rational
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
@@ -33,6 +33,11 @@
       where
         msg' = "Error in " ++ show loc ++ ":\n" ++ msg
 
+    readInFile _ "-" =
+      ExceptT $ do
+        liftIO (found "standard input")
+        fmap Right getContents `catch`
+          \(e :: IOException) -> return (Left (show e))
     readInFile pos name = do
       mfile <- liftIO (findFile name)
       case mfile of
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
@@ -70,7 +70,7 @@
 
 pPrintClause :: String -> String -> String -> Doc -> Doc
 pPrintClause family name kind rest =
-  text family <> parens (sep [text name <> comma <+> text kind <> comma, rest]) <> text "."
+  text family <> parens (sep [text (escapeAtom name) <> comma <+> text kind <> comma, rest]) <> text "."
 
 instance Pretty Clause where
   pPrint (Clause (Bind _ ts)) =
diff --git a/src/Jukebox/Toolbox.hs b/src/Jukebox/Toolbox.hs
--- a/src/Jukebox/Toolbox.hs
+++ b/src/Jukebox/Toolbox.hs
@@ -196,9 +196,9 @@
           result unsatisfiable
             "PROVED.\nThe conjecture is true or the axioms are contradictory."
         loop i (c:cs) = do
-          when multi $ putStr $ comment globals $ "Part " ++ part i
+          when multi $ message globals $ "Part " ++ part i
           answer <- solve (axioms ++ c)
-          when multi $ putStr $ comment globals $ "Partial result (" ++ part i ++ "): " ++ show answer
+          when multi $ message globals $ "Partial result (" ++ part i ++ "): " ++ show answer
           case answer of
             Satisfiable ->
               result satisfiable
@@ -210,7 +210,7 @@
         multi = length conjectures > 1
         part i = show i ++ "/" ++ show (length conjectures)
         result x hint = do
-          message globals ("SZS status " ++ x)
+          putStrLn ("% SZS status " ++ x)
           unless (quiet globals) $ putStrLn ""
           message globals hint