diff --git a/jukebox.cabal b/jukebox.cabal
--- a/jukebox.cabal
+++ b/jukebox.cabal
@@ -1,5 +1,5 @@
 Name: jukebox
-Version: 0.2.15
+Version: 0.2.16
 Cabal-version: >= 1.8
 Build-type: Simple
 Author: Nick Smallbone
diff --git a/src/Jukebox/Clausify.hs b/src/Jukebox/Clausify.hs
--- a/src/Jukebox/Clausify.hs
+++ b/src/Jukebox/Clausify.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeOperators, BangPatterns, CPP #-}
+{-# LANGUAGE TypeOperators, BangPatterns, CPP, PatternGuards #-}
 module Jukebox.Clausify where
 
 import Jukebox.Form hiding (run)
@@ -34,8 +34,9 @@
   clausifyInputs theory obligs [] =
     do return (toCNF (reverse theory) (reverse obligs))
   
-  clausifyInputs theory obligs (inp:inps) | kind inp == Axiom =
-    do cs <- clausForm inp
+  clausifyInputs theory obligs (inp:inps)
+    | Axiom axiom <- kind inp =
+    do cs <- clausForm axiom inp
        clausifyInputs (cs ++ theory) obligs inps
 
   clausifyInputs theory obligs (inp:inps) | kind inp `elem` [Conjecture, Question] =
@@ -46,7 +47,7 @@
   
   clausifyObligs theory obligs inp (a:as) inps =
     do cs <-
-         clausForm inp {
+         clausForm "negated_conjecture" inp {
            what = nt a,
            source = Inference "negate_conjecture" "cth" [inp] }
        clausifyObligs theory (cs:obligs) inp as inps
@@ -102,19 +103,19 @@
 ----------------------------------------------------------------------
 -- core clausification algorithm
 
-clausForm :: Input Form -> M [Input Clause]
-clausForm inp =
+clausForm :: String -> Input Form -> M [Input Clause]
+clausForm kind inp =
   withName (tag inp) $
     do miniscoped      <- miniscope . check . simplify         . check $ what inp
        noEquivPs       <- removeEquiv                          . check $ miniscoped
        noExistsPs      <- mapM removeExists                    . check $ noEquivPs
        noExpensiveOrPs <- fmap concat . mapM removeExpensiveOr . check $ noExistsPs
        noForAllPs      <- lift . mapM uniqueNames              . check $ noExpensiveOrPs
-       let !thm         = Input "skolemised" Axiom (Inference "clausify" "esa" [inp]) (And noForAllPs)
+       let !thm         = Input "skolemised" (Axiom 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) Axiom (Inference "clausify" "thm" [thm]) c
+           inps         = [ Input (tag inp ++ i) (Axiom kind) (Inference "clausify" "thm" [thm]) c
                           | (c, i) <- zip cs ("":
                                         [ '_':show i | i <- [1..] ]) ]
        return $! force . check                                         $ inps
diff --git a/src/Jukebox/Form.hs b/src/Jukebox/Form.hs
--- a/src/Jukebox/Form.hs
+++ b/src/Jukebox/Form.hs
@@ -307,7 +307,7 @@
 
 type Tag = String
 
-data Kind = Axiom | Conjecture | Question deriving (Eq, Ord)
+data Kind = Axiom String | Conjecture | Question deriving (Eq, Ord)
 
 data Answer = Satisfiable | Unsatisfiable | NoAnswer NoAnswerReason
   deriving (Eq, Ord)
diff --git a/src/Jukebox/GuessModel.hs b/src/Jukebox/GuessModel.hs
--- a/src/Jukebox/GuessModel.hs
+++ b/src/Jukebox/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" Axiom Unknown) prelude ++
-          map (Input "program" Axiom Unknown) program ++
+  return (map (Input "adt" (Axiom "axiom") Unknown) prelude ++
+          map (Input "program" (Axiom "axiom") Unknown) program ++
           forms)
 
 ind :: Symbolic a => a -> Type
diff --git a/src/Jukebox/Monotonox/ToFOF.hs b/src/Jukebox/Monotonox/ToFOF.hs
--- a/src/Jukebox/Monotonox/ToFOF.hs
+++ b/src/Jukebox/Monotonox/ToFOF.hs
@@ -28,10 +28,10 @@
 guard scheme mono (Input t k info f) = Input t k info (aux (pos k) f)
   where aux pos (ForAll (Bind vs f))
           | pos = forAll scheme (Bind vs (aux pos f))
-          | otherwise = Not (exists scheme (Bind vs (Not (aux pos f))))
+          | otherwise = notInwards (exists scheme (Bind vs (Not (aux pos f))))
         aux pos (Exists (Bind vs f))
           | pos = exists scheme (Bind vs (aux pos f))
-          | otherwise = Not (forAll scheme (Bind vs (Not (aux pos f))))
+          | otherwise = notInwards (forAll scheme (Bind vs (Not (aux pos f))))
         aux _pos (Literal (Pos (t :=: u)))
           | not (mono (typ t)) = equals scheme t u
         aux _pos (Literal (Neg (t :=: u)))
@@ -42,7 +42,7 @@
         aux pos (Or fs) = Or (fmap (aux pos) fs)
         aux _pos (Equiv _ _) = error "ToFOF.guard: equiv should have been eliminated"
         aux _pos (Connective _ _ _) = error "ToFOF.guard: connective should have been eliminated"
-        pos Axiom = True
+        pos Axiom{} = True
         pos Conjecture = False
 
 translate, translate1 :: Scheme -> (Type -> Bool) -> Problem Form -> Problem Form
@@ -65,7 +65,7 @@
         map (simplify . ForAll . bind) . split . simplify . foldr (/\) true $
           funcAxioms ++ typeAxioms
   return $
-    [ Input ("types" ++ show i) Axiom (Inference "type_axiom" "esa" []) axiom | (axiom, i) <- zip axioms [1..] ] ++
+    [ Input ("types" ++ show i) (Axiom "axiom") (Inference "type_axiom" "esa" []) axiom | (axiom, i) <- zip axioms [1..] ] ++
     map (guard scheme1' mono') inps
 
 translate scheme mono f =
@@ -74,16 +74,12 @@
           forM inps $ \inp@(Input tag kind _ f) -> do
             let prepare f = fmap (foldr (/\) true) (run (withName tag (removeEquiv (simplify f))))
             case kind of
-              Axiom ->
+              Axiom{} ->
                 fmap (Input tag kind (Inference "type_encoding" "esa" [inp])) $
                   prepare f
               Conjecture ->
-                let
-                  neg_inp =
-                    Input tag Axiom
-                      (Inference "negate_conjecture" "cth" [inp]) (nt f) in
-                fmap (Input tag kind (Inference "type_encoding" "esa" [neg_inp])) $
-                fmap notInwards (prepare (nt f))
+                fmap (Input tag kind (Inference "type_encoding" "esa" [inp])) $
+                fmap notInwards $ prepare $ nt f
       typeI = Type (name "$i") (Finite 0) Infinite
       trType O = O
       trType ty = typeI
diff --git a/src/Jukebox/SMTLIB.hs b/src/Jukebox/SMTLIB.hs
--- a/src/Jukebox/SMTLIB.hs
+++ b/src/Jukebox/SMTLIB.hs
@@ -183,7 +183,7 @@
 pPrintType ty = pPrintName (name ty)
 
 pPrintInput :: Input Form -> Doc
-pPrintInput Input{kind = Axiom, what = form} =
+pPrintInput Input{kind = Axiom _, what = form} =
   sexp ["assert", pPrintForm form]
 pPrintInput Input{kind = Conjecture, what = form} =
   sexp ["assert", sexp ["not", pPrintForm form]]
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
@@ -255,7 +255,7 @@
   MkState mfile _ _ _ _ _ <- getState
   UserState _ (At (L.Pos n _) _) <- getPosition
   let
-    axiom t = general t Form.Axiom
+    axiom t = general t (Form.Axiom (show t))
     general k kind = keyword k >> return (mk kind)
     mk kind tag form =
       Input { Form.tag = tag,
@@ -267,8 +267,8 @@
                   Just file -> FromFile file (fromIntegral n) }
   axiom Axiom <|> axiom Hypothesis <|> axiom Definition <|>
     axiom Assumption <|> axiom Lemma <|> axiom Theorem <|>
+    axiom NegatedConjecture <|>
     general Conjecture Form.Conjecture <|>
-    general NegatedConjecture Form.Axiom <|>
     general Question Form.Question
 
 -- A formula name.
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
@@ -16,6 +16,7 @@
 import Jukebox.Name
 import Jukebox.Utils
 import Text.PrettyPrint.HughesPJClass
+import Control.Monad.Trans.State.Strict
 
 pPrintClauses :: Problem Clause -> Doc
 pPrintClauses prob0
@@ -37,7 +38,7 @@
 -- Print a problem together with all source/derivation information.
 pPrintProof :: Problem Form -> Doc
 pPrintProof prob =
-  pPrintAnnotProof (reverse (annot 1 Set.empty Map.empty (reverse prob)))
+  pPrintAnnotProof (evalState (concat <$> mapM annot prob) (1, Map.empty))
   where
     fun f [] = text f
     fun f xs = text f <> parens (fsep (punctuate comma xs))
@@ -48,53 +49,56 @@
     info inp = (kind inp, what inp)
 
     -- We maintain: the set of formulas printed so far,
-    -- the set of formulas which have been given a clause number so far,
     -- and the highest number given so far.
-    -- The clauses come out in reverse dependency order.
-    annot :: Int -> Set (Kind, Form) -> Map (Kind, Form) Int -> [Input Form] -> [(Input Form, (String, [Doc]))]
-    annot _ _ _ [] = []
-    annot m seen named (inp:inps)
-        -- Already processed this formula
-      | Set.member (kind inp, what inp) seen =
-          annot m seen named inps
-        -- Formula is identical to its parent
+    findNumber :: Input Form -> State (Int, Map (Kind, Form) Int) (Maybe Int)
+    findNumber inp =
+      gets (Map.lookup (info inp) . snd)
+
+    newNumber :: Input Form -> State (Int, Map (Kind, Form) Int) (Maybe Int)
+    newNumber inp = do
+      (n, map) <- get
+      case Map.lookup (info inp) map of
+        Nothing -> do
+          put (n+1, Map.insert (info inp) n map)
+          return (Just n)
+        Just _ -> return Nothing
+
+    annot :: Input Form -> State (Int, Map (Kind, Form) Int) [(Input Form, (String, [Doc]))]
+    annot inp
+      -- Formula is identical to its parent
       | Inference _ _ [inp'] <- source inp,
-        let [p, q] = prettyNames [what inp, what inp'] in
-        kind inp == kind inp' &&
-        -- I have NO idea why this doesn't work without show here :(
-        show p == show q =
-          annot m seen named (inp { source = source inp' }:inps)
-      | otherwise =
-        case Map.lookup (info inp) named of
-          Nothing ->
-            -- Give the formula a name
-            annot (m+1) seen (Map.insert (info inp) m named) (inp:inps)
-          Just n ->
-            -- A new formula - print it out
-            let
-              (k, m', named', new, stuff) =
-                case source inp of
-                  Unknown ->
-                    ("plain", m, named, [], [])
-                  FromFile file _ ->
-                    (show (kind inp), m, named, [],
-                     [fun "file" [text (escapeAtom file), text (escapeAtom (tag inp))]])
-                  Inference name status parents ->
-                    -- Give any unnamed parents a name
-                    let
-                      unnamed = [inp | inp <- parents, not (info inp `Map.member` named)]
-                      named' =
-                        named `Map.union`
-                        Map.fromList (zip (map info parents) [m..])
-                    in
-                      ("plain", m+length unnamed, named', parents,
-                       [fun "inference" [
-                         text name, list [fun "status" [text status]],
-                         list [text (clause (fromJust (Map.lookup (info inp) named'))) | inp <- parents]]])
-            in
-              (inp { tag = clause n }, (k, stuff)):
-              annot m' (Set.insert (info inp) seen) named' (new++inps)
+          let [p, q] = prettyNames [what inp, what inp'] in
+          kind inp == kind inp' &&
+          -- I have NO idea why this doesn't work without show here :(
+          show p == show q =
+            annot inp { source = source inp' }
+      | otherwise = do
+          mn <- newNumber inp
+          case mn of
+            Nothing ->
+              -- Already processed this formula
+              return []
+            Just n -> do
+              let
+                ret k stuff =
+                  return [(inp { tag = clause n }, (k, stuff))]
 
+              case source inp of
+                Unknown -> ret "plain" []
+                FromFile file _ ->
+                  ret (show (kind inp))
+                    [fun "file" [text (escapeAtom file), text (escapeAtom (tag inp))]]
+                Inference name status parents -> do
+                  -- Process all parents first
+                  rest <- mapM annot parents
+                  nums <- map fromJust <$> mapM findNumber parents
+
+                  fmap (concat rest ++) $
+                    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 $
@@ -285,7 +289,7 @@
       nest 2 (pPrintForm bind 1 f)]
 
 instance Show Kind where
-  show Axiom = "axiom"
+  show (Axiom kind) = kind
   show Conjecture = "conjecture"
   show Question = "question"