diff --git a/jukebox.cabal b/jukebox.cabal
--- a/jukebox.cabal
+++ b/jukebox.cabal
@@ -1,5 +1,5 @@
 Name: jukebox
-Version: 0.5.7
+Version: 0.5.8
 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
@@ -327,6 +327,11 @@
 type Tag = String
 
 data Kind = Ax AxKind | Conj ConjKind deriving (Eq, Ord)
+
+isAxiom :: Kind -> Bool
+isAxiom (Ax _) = True
+isAxiom (Conj _) = False
+
 data AxKind =
   Axiom | Hypothesis | Definition | Assumption | Lemma | TheoremKind |
   NegatedConjecture deriving (Eq, Ord)
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
@@ -19,6 +19,7 @@
 import Text.PrettyPrint.HughesPJClass
 import Control.Monad.Trans.State.Strict
 import Data.Symbol
+import Control.Monad
 
 pPrintClauses :: Problem Clause -> Doc
 pPrintClauses prob0
@@ -88,11 +89,10 @@
       | Inference _ _ [InputPlus{inputValue = inp'}] <- source inp,
           let p = prettyNames (what inp)
               q = prettyNames (what inp') in
-          kind inp == kind inp' &&
+          isAxiom (kind inp) == isAxiom (kind inp') &&
           -- I have NO idea why this doesn't work without show here :(
-          show p == show q &&
-          (isJust (ident inp) || not (isJust (ident inp'))) = -- don't lose an ident
-            annot inp { source = source inp' }
+          show p == show q =
+          annot inp { source = source inp', ident = ident inp `mplus` ident inp' }
     annot inp = do
       mn <- findNumber inp
       case mn of