diff --git a/jukebox.cabal b/jukebox.cabal
--- a/jukebox.cabal
+++ b/jukebox.cabal
@@ -1,5 +1,5 @@
 Name: jukebox
-Version: 0.5.13
+Version: 0.5.14
 Cabal-version: >= 1.10
 Build-type: Simple
 Author: Nick Smallbone
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
@@ -86,7 +86,7 @@
     annot :: Input Form -> PrintProofState Int
     annot inp
       -- Formula is identical to its parent
-      | Inference Nothing _ _ [InputPlus{inputValue = inp'}] <- source inp,
+      | Inference _ _ _ [InputPlus{inputValue = inp'}] <- source inp,
           let p = prettyNames (what inp)
               q = prettyNames (what inp') in
           isAxiom (kind inp) == isAxiom (kind inp') &&
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
@@ -118,6 +118,9 @@
 -- core clausification algorithm
 
 clausForm :: AxKind -> Input Form -> M [Input Clause]
+clausForm _ inp
+  | Just clause <- toClause (what inp) =
+    return [fmap (const clause) inp]
 clausForm kind inp =
   withName (tag inp) $
     do miniscoped      <- miniscope . check . simplify         . check $ what inp
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
@@ -107,9 +107,11 @@
 
 eliminatePredicates :: Problem Clause -> Problem Clause
 eliminatePredicates prob =
-  map (fmap elim) prob
+  map elim prob
   where
-    elim = clause . map (fmap elim1) . toLiterals
+    elim inp =
+      derivedClause "true_elimination" "esa" (fmap toForm inp) $
+        clause . map (fmap elim1) . toLiterals $ what inp
     elim1 (t :=: u) = t :=: u
     elim1 (Tru ((p ::: FunType tys _) :@: ts)) =
       ((p ::: FunType tys bool) :@: ts) :=: true
@@ -127,8 +129,9 @@
       elim inp
         | (null poss && length negs /= 1 && not (allowConjunctiveConjectures flags)) ||
           (not (null poss) && length negs > 1 && multi flags) =
+          let conj = null poss in
           derivedClause "tupling" "esa" (fmap toForm inp) $
-            clause (Neg ((tuple tys :@: ts) :=: (tuple tys :@: us)):poss)
+            clause (Neg ((tuple conj tys :@: ts) :=: (tuple conj tys :@: us)):poss)
         where
           (poss, negs) = partition pos (toLiterals (what inp))
           ts = [t | l <- negs, let Neg (t :=: _) = l]
@@ -139,8 +142,9 @@
       tuple = run_ prob $ do
         tupleType <- newName (withLabel "tuple" (name "tuple"))
         tuple <- newName (withLabel "tuple" (name "tuple"))
-        return $ \args ->
-          variant tuple args :::
+        conjectureTuple <- newName (withLabel "conjecture_tuple" (name "tuple"))
+        return $ \conj args ->
+          variant (if conj then conjectureTuple else tuple) args :::
           FunType args (Type (variant tupleType args))
 
 eliminateUnsuitableConjectures :: HornFlags -> Problem Clause -> Problem Clause