diff --git a/jukebox.cabal b/jukebox.cabal
--- a/jukebox.cabal
+++ b/jukebox.cabal
@@ -1,5 +1,5 @@
 Name: jukebox
-Version: 0.5.11
+Version: 0.5.12
 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
@@ -390,11 +390,14 @@
 data InputSource =
     Unknown
   | FromFile String Int
-  | Inference String String [InputPlus Form]
+  | Inference (Maybe Kind) String String [InputPlus Form]
 
 inference :: String -> String -> [Input Form] -> InputSource
-inference name status parents = Inference name status (map inputPlus parents)
+inference = inference' Nothing
 
+inference' :: Maybe Kind -> String -> String -> [Input Form] -> InputSource
+inference' role name status parents = Inference role name status (map inputPlus parents)
+
 data InputPlus a = InputPlus
   { inputNames     :: [Name],
     inputFunctions :: [Function],
@@ -633,7 +636,7 @@
   inp (Input ident _ _ source _) =
     maybeToList ident ++
     case source of
-      Inference _ _ inps ->
+      Inference _ _ _ inps ->
         concatMap inputNames inps
       _ -> []
 
@@ -676,7 +679,7 @@
   inp :: Symbolic a => Input a -> [Function]
   inp (Input _ _ _ source _) =
     case source of
-      Inference _ _ inps ->
+      Inference _ _ _ inps ->
         concatMap inputFunctions inps
       _ -> []
 
@@ -806,8 +809,8 @@
       where
         source' =
           case source of
-            Inference inf status forms ->
-              Inference inf status (map inputPlus forms)
+            Inference mkind inf status forms ->
+              Inference mkind inf status (map inputPlus forms)
             _ -> source
 
     inputPlus  :: InputPlus Form -> InputPlus Form
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 _ _ [InputPlus{inputValue = inp'}] <- source inp,
+      | Inference Nothing _ _ [InputPlus{inputValue = inp'}] <- source inp,
           let p = prettyNames (what inp)
               q = prettyNames (what inp') in
           isAxiom (kind inp) == isAxiom (kind inp') &&
@@ -111,10 +111,10 @@
             FromFile file _ ->
               ret (show (kind inp))
                 [fun "file" [text (escapeAtom file), text (escapeAtom (tag inp))]]
-            Inference name status parents -> do
+            Inference mkind name status parents -> do
               -- Process all parents first
               nums <- mapM (annot . inputValue) parents
-              ret "plain"
+              ret (case mkind of { Nothing -> "plain"; Just kind -> show kind })
                 [fun "inference" [
                   text name, list [fun "status" [text status]],
                   list [text (clause n) | n <- nums]]]
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
@@ -63,7 +63,7 @@
     do cs <-
          clausForm NegatedConjecture inp {
            what = nt a,
-           source = inference "negate_conjecture" "cth" [inp] }
+           source = inference' (Just (Ax NegatedConjecture)) "negate_conjecture" "cth" [inp] }
        clausifyObligs theory (cs:obligs) inp as inps
 
   split' a | splitting flags = if null split_a then [true] else split_a