diff --git a/jukebox.cabal b/jukebox.cabal
--- a/jukebox.cabal
+++ b/jukebox.cabal
@@ -1,5 +1,5 @@
 Name: jukebox
-Version: 0.5.5
+Version: 0.5.6
 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
@@ -16,6 +16,7 @@
 import Control.Monad.Trans.Class
 import Control.Monad.Trans.State.Strict
 import Data.List
+import Data.Maybe
 import Jukebox.Utils
 import Data.Typeable(Typeable)
 import Data.Monoid
@@ -374,7 +375,8 @@
 answerJustification _ = Nothing
 
 data Input a = Input
-  { tag    :: Tag,
+  { ident  :: Maybe Name,
+    tag    :: Tag,
     kind   :: Kind,
     source :: InputSource,
     what   :: a }
@@ -491,7 +493,7 @@
   rep' (x:xs) = Binary (:) x xs
 
 instance Symbolic a => Unpack (Input a) where
-  rep' (Input tag kind info what) = Unary (Input tag kind info) what
+  rep' (Input ident tag kind info what) = Unary (Input ident tag kind info) what
 
 instance Unpack CNF where
   rep' (CNF ax conj s1 s2) =
@@ -617,7 +619,8 @@
   bind (Bind vs _) = map name (Set.toList vs)
 
   inp :: Symbolic a => Input a -> [Name]
-  inp (Input _ _ source _) =
+  inp (Input ident _ _ source _) =
+    maybeToList ident ++
     case source of
       Inference _ _ inps ->
         concatMap inputNames inps
@@ -637,7 +640,7 @@
   bind (Bind vs _) = map typ (Set.toList vs)
 
   inp :: Symbolic a => Input a -> [Type]
-  inp (Input _ _ source _) =
+  inp (Input _ _ _ source _) =
     case source of
       Inference _ _ inps ->
         concatMap inputTypes inps
@@ -664,7 +667,7 @@
   term _ = mempty
 
   inp :: Symbolic a => Input a -> [Function]
-  inp (Input _ _ source _) =
+  inp (Input _ _ _ source _) =
     case source of
       Inference _ _ inps ->
         concatMap inputFunctions inps
@@ -791,8 +794,8 @@
     term (Var x) = Var (var x)
 
     input :: Symbolic a => Input a -> Input a
-    input (Input name kind source what) =
-      Input name kind source' (rename what)
+    input (Input id name kind source what) =
+      Input (fmap f id) name kind source' (rename what)
       where
         source' =
           case source of
diff --git a/src/Jukebox/Name.hs b/src/Jukebox/Name.hs
--- a/src/Jukebox/Name.hs
+++ b/src/Jukebox/Name.hs
@@ -171,4 +171,7 @@
   let idx' = idx+1
   when (idx' < 0) $ error "Name.newName: too many names"
   put $! idx'
-  return $! Unique idx' (intern (base x)) (label x) (renamer x)
+  return $! unique x idx'
+
+unique :: Named a => a -> Int64 -> Name
+unique x n = Unique n (intern (base x)) (label x) (renamer x)
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
@@ -268,7 +268,8 @@
     axiom t kind = general t (Form.Ax kind)
     conjecture t kind = general t (Form.Conj kind)
     mk kind tag form =
-      Input { Form.tag = tag,
+      Input { Form.ident = Nothing,
+              Form.tag = tag,
               Form.kind = kind,
               Form.what = form,
               Form.source =
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
@@ -38,58 +38,73 @@
   where
     prob = prettyNames prob0
 
+type PrintProofState a = State (Int, Map Name Int, [(Input Form, (String, [Doc]))]) a
+
 -- Print a problem together with all source/derivation information.
 pPrintProof :: Problem Form -> Doc
 pPrintProof prob =
-  pPrintAnnotProof (evalState (concat <$> mapM annot prob) (1, Map.empty))
+  pPrintAnnotProof (reverse out)
   where
+    (_, _, out) = execState (mapM_ annot prob) (1, Map.empty, [])
+
     fun f [] = text f
     fun f xs = text f <> parens (hsep (punctuate comma xs))
     list = brackets . hsep . punctuate comma
 
     clause n = "c" ++ show n
 
-    info inp = (kind inp, what inp)
-
     -- We maintain: the set of formulas printed so far,
     -- and the highest number given so far.
-    findNumber :: Input Form -> State (Int, Map (Kind, Form) Int) (Maybe Int)
+    findNumber :: Input Form -> PrintProofState (Maybe Int)
     findNumber inp =
-      gets (Map.lookup (info inp) . snd)
+      case ident inp of
+        Nothing -> return Nothing
+        Just id -> do
+          (_, map, _) <- get
+          return (Map.lookup id map)
 
-    newNumber :: Input Form -> State (Int, Map (Kind, Form) Int) (Maybe Int)
+    newNumber :: Input Form -> PrintProofState Int
     newNumber inp = do
-      (n, map) <- get
-      case Map.lookup (info inp) map of
+      (n, map, out) <- get
+      case ident inp of
         Nothing -> do
-          put (n+1, Map.insert (info inp) n map)
-          return (Just n)
-        Just _ -> return Nothing
+          put (n+1, map, out)
+          return n
+        Just id ->
+          case Map.lookup id map of
+            Nothing -> do
+              put (n+1, Map.insert id n map, out)
+              return n
+            Just _ -> error "newNumber: already present"
 
-    annot :: Input Form -> State (Int, Map (Kind, Form) Int) [(Input Form, (String, [Doc]))]
+    emit :: Input Form -> String -> [Doc] -> PrintProofState ()
+    emit form k xs = do
+      (n, map, out) <- get
+      put (n, map, (form, (k, xs)):out)
+
+    annot :: Input Form -> PrintProofState Int
     annot inp
       -- Formula is identical to its parent
       | Inference _ _ [InputPlus{inputValue = inp'}] <- source inp,
-          let [p, q] = prettyNames [what inp, what inp'] in
+          let p = prettyNames (what inp)
+              q = prettyNames (what inp') in
           kind inp == kind inp' &&
           -- I have NO idea why this doesn't work without show here :(
-          show p == show q =
+          show p == show q &&
+          (isJust (ident inp) || not (isJust (ident inp'))) = -- don't lose an ident
             annot inp { source = source inp' }
     annot inp = do
       mn <- findNumber inp
       case mn of
-        Just _ ->
+        Just n -> do
           -- Already processed this formula
-          return []
+          return n
         Nothing -> do
           let
             ret k stuff = do
-              res <- newNumber inp
-              case res of
-                Just n ->
-                  return [(inp { tag = clause n }, (k, stuff))]
-                Nothing ->
-                  return []
+              n <- newNumber inp
+              emit inp { tag = clause n } k stuff
+              return n
 
           case source inp of
             Unknown -> ret "plain" []
@@ -98,20 +113,17 @@
                 [fun "file" [text (escapeAtom file), text (escapeAtom (tag inp))]]
             Inference name status parents -> do
               -- Process all parents first
-              rest <- mapM (annot . inputValue) parents
-              nums <- map fromJust <$> mapM (findNumber . inputValue) parents
-
-              fmap (concat rest ++) $
-                ret "plain"
-                  [fun "inference" [
-                    text name, list [fun "status" [text status]],
-                    list [text (clause n) | n <- nums]]]
+              nums <- mapM (annot . inputValue) parents
+              ret "plain"
+                [fun "inference" [
+                  text name, list [fun "status" [text status]],
+                  list [text (clause n) | n <- nums]]]
 
 pPrintAnnotProof :: [(Input Form, (String, [Doc]))] -> Doc
 pPrintAnnotProof annots0 =
   vcat $
     [ vcat (pPrintDecls "tff" inps) | not (isReallyFof inps) ] ++
-    [ pPrintClause (family x) (tag inp) k (pp x:rest)
+    [ pPrintClause (family x) (tag inp) k (pp x:rest) <+> text (show (ident inp))
     | (inp, (k, rest)) <- annots,
       let x = what inp ]
   where
diff --git a/src/Jukebox/Tools/Clausify.hs b/src/Jukebox/Tools/Clausify.hs
--- a/src/Jukebox/Tools/Clausify.hs
+++ b/src/Jukebox/Tools/Clausify.hs
@@ -125,11 +125,11 @@
        noExistsPs      <- mapM removeExists                    . check $ noEquivPs
        noExpensiveOrPs <- fmap concat . mapM removeExpensiveOr . check $ noExistsPs
        noForAllPs      <- lift . mapM uniqueNames              . check $ noExpensiveOrPs
-       let !thm         = Input "skolemised" (Ax kind) (inference "clausify" "esa" [inp]) (And noForAllPs)
+       let !thm         = Input Nothing "skolemised" (Ax kind) (inference "clausify" "esa" [inp]) (And noForAllPs)
            !cnf_        = concatMap cnf                        . check $ noForAllPs
            !simp        = simplifyCNF                          . check $ cnf_
            cs           = fmap clause                                  $ simp
-           inps         = [ Input (tag inp ++ i) (Ax kind) (inference "clausify" "thm" [thm]) c
+           inps         = [ Input Nothing (tag inp ++ i) (Ax kind) (inference "clausify" "thm" [thm]) c
                           | (c, i) <- zip cs ("":
                                         [ '_':show i | i <- [1..] ]) ]
        return $! force . check                                         $ inps
diff --git a/src/Jukebox/Tools/EncodeTypes.hs b/src/Jukebox/Tools/EncodeTypes.hs
--- a/src/Jukebox/Tools/EncodeTypes.hs
+++ b/src/Jukebox/Tools/EncodeTypes.hs
@@ -25,7 +25,7 @@
   }
 
 guard :: Scheme1 -> (Type -> Bool) -> Input Form -> Input Form
-guard scheme mono (Input t k info f) = Input t k info (aux (pos k) f)
+guard scheme mono (Input _ t k info f) = Input Nothing t k info (aux (pos k) f)
   where aux pos (ForAll (Bind vs f))
           | pos = forAll scheme (Bind vs (aux pos f))
           | otherwise = notInwards (exists scheme (Bind vs (Not (aux pos f))))
@@ -65,20 +65,20 @@
         map (simplify . ForAll . bind) . split . simplify . foldr (/\) true $
           funcAxioms ++ typeAxioms
   return $
-    [ Input ("types" ++ show i) (Ax Axiom) (inference "type_axiom" "esa" []) axiom | (axiom, i) <- zip axioms [1..] ] ++
+    [ Input Nothing ("types" ++ show i) (Ax Axiom) (inference "type_axiom" "esa" []) axiom | (axiom, i) <- zip axioms [1..] ] ++
     map (guard scheme1' mono') inps
 
 translate scheme mono f =
   let f' =
         Form.run f $ \inps -> do
-          forM inps $ \inp@(Input tag kind _ f) -> do
+          forM inps $ \inp@(Input _ tag kind _ f) -> do
             let prepare f = fmap (foldr (/\) true) (run (withName tag (removeEquiv (simplify f))))
             case kind of
               Ax{} ->
-                fmap (Input tag kind (inference "type_encoding" "esa" [inp])) $
+                fmap (Input Nothing tag kind (inference "type_encoding" "esa" [inp])) $
                   prepare f
               Conj{} ->
-                fmap (Input tag kind (inference "type_encoding" "esa" [inp])) $
+                fmap (Input Nothing tag kind (inference "type_encoding" "esa" [inp])) $
                 fmap notInwards $ prepare $ nt f
       trType O = O
       trType _ = indType
diff --git a/src/Jukebox/Tools/GuessModel.hs b/src/Jukebox/Tools/GuessModel.hs
--- a/src/Jukebox/Tools/GuessModel.hs
+++ b/src/Jukebox/Tools/GuessModel.hs
@@ -57,8 +57,8 @@
   let withExpansive f func = f func (base (name func) `elem` expansive) answer
   (constructors, prelude) <- universe univ i
   program <- fmap concat (mapM (withExpansive (function constructors)) (functions forms))
-  return (map (Input "adt" (Ax Axiom) Unknown) prelude ++
-          map (Input "program" (Ax Axiom) Unknown) program ++
+  return (map (Input Nothing "adt" (Ax Axiom) Unknown) prelude ++
+          map (Input Nothing "program" (Ax Axiom) Unknown) program ++
           forms)
 
 ind :: Symbolic a => a -> Type
diff --git a/src/Jukebox/Tools/HornToUnit.hs b/src/Jukebox/Tools/HornToUnit.hs
--- a/src/Jukebox/Tools/HornToUnit.hs
+++ b/src/Jukebox/Tools/HornToUnit.hs
@@ -147,7 +147,7 @@
   | null bad = prob
   | otherwise =
     good ++ map (fmap addConjecture) bad ++
-    [Input { tag = "goal", kind = Ax NegatedConjecture, source = Unknown,
+    [Input { ident = Nothing, tag = "goal", kind = Ax NegatedConjecture, source = Unknown,
              what = clause [Neg (a :=: b)] }]
   where
     (bad, good) = partition unsuitable prob
@@ -279,6 +279,7 @@
 
     toInput (tag, l) =
       Input {
+        ident = Nothing,
         tag = tag,
         kind = Ax Axiom,
         source = Unknown,