diff --git a/jukebox.cabal b/jukebox.cabal
--- a/jukebox.cabal
+++ b/jukebox.cabal
@@ -1,5 +1,5 @@
 Name: jukebox
-Version: 0.5.12
+Version: 0.5.13
 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
@@ -313,6 +313,8 @@
 toLiterals (Clause (Bind _ ls)) = ls
 
 toClause :: Form -> Maybe Clause
+toClause (And [c]) = toClause c
+toClause (Or [c]) = toClause c
 toClause (ForAll (Bind _ f)) = toClause f
 toClause f = clause <$> cl f
   where
@@ -389,7 +391,7 @@
 
 data InputSource =
     Unknown
-  | FromFile String Int
+  | FromFile String String Int
   | Inference (Maybe Kind) String String [InputPlus Form]
 
 inference :: String -> String -> [Input Form] -> InputSource
@@ -397,6 +399,10 @@
 
 inference' :: Maybe Kind -> String -> String -> [Input Form] -> InputSource
 inference' role name status parents = Inference role name status (map inputPlus parents)
+
+derivedClause :: String -> String -> Input Form -> a -> Input a
+derivedClause name status parent clause =
+  Input Nothing (tag parent) (kind parent) (inference name status [parent]) clause
 
 data InputPlus a = InputPlus
   { inputNames     :: [Name],
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
@@ -275,7 +275,7 @@
               Form.source =
                 case mfile of
                   Nothing -> Form.Unknown
-                  Just file -> FromFile file (fromIntegral n) }
+                  Just file -> FromFile file tag (fromIntegral n) }
   axiom L.Axiom Axiom <|>
     axiom L.Hypothesis Hypothesis <|>
     axiom L.Definition Definition <|>
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
@@ -108,9 +108,9 @@
 
           case source inp of
             Unknown -> ret "plain" []
-            FromFile file _ ->
+            FromFile file tag _ ->
               ret (show (kind inp))
-                [fun "file" [text (escapeAtom file), text (escapeAtom (tag inp))]]
+                [fun "file" [text (escapeAtom file), text (escapeAtom tag)]]
             Inference mkind name status parents -> do
               -- Process all parents first
               nums <- mapM (annot . inputValue) parents
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
@@ -127,7 +127,8 @@
       elim inp
         | (null poss && length negs /= 1 && not (allowConjunctiveConjectures flags)) ||
           (not (null poss) && length negs > 1 && multi flags) =
-          inp{what = clause (Neg ((tuple tys :@: ts) :=: (tuple tys :@: us)):poss)}
+          derivedClause "tupling" "esa" (fmap toForm inp) $
+            clause (Neg ((tuple tys :@: ts) :=: (tuple tys :@: us)):poss)
         where
           (poss, negs) = partition pos (toLiterals (what inp))
           ts = [t | l <- negs, let Neg (t :=: _) = l]
@@ -194,7 +195,7 @@
         ([], _) -> return [c]
         ([Pos l], ls) -> do
           l <- foldM (encode (tag c)) l ls
-          return [c { what = clause [Pos l] }]
+          return [derivedClause "ifeq_intro" "esa" (fmap toForm c) (clause [Pos l])]
         _ ->
           if dropNonHorn flags then
             return []
@@ -282,7 +283,7 @@
         ident = Nothing,
         tag = tag,
         kind = Ax Axiom,
-        source = Unknown,
+        source = inference "ifeq_elim" "esa" [],
         what = clause [Pos l] }
 
     (ifeqName, freshName, passiveName, xvar, yvar, zvar) = run_ prob $ do