diff --git a/jukebox.cabal b/jukebox.cabal
--- a/jukebox.cabal
+++ b/jukebox.cabal
@@ -1,5 +1,5 @@
 Name: jukebox
-Version: 0.2.14
+Version: 0.2.15
 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
@@ -35,18 +35,21 @@
     do return (toCNF (reverse theory) (reverse obligs))
   
   clausifyInputs theory obligs (inp:inps) | kind inp == Axiom =
-    do cs <- clausForm (tag inp) (what inp)
+    do cs <- clausForm inp
        clausifyInputs (cs ++ theory) obligs inps
 
   clausifyInputs theory obligs (inp:inps) | kind inp `elem` [Conjecture, Question] =
-    do clausifyObligs theory obligs (tag inp) (split' (what inp)) inps
+    do clausifyObligs theory obligs inp (split' (what inp)) inps
 
   clausifyObligs theory obligs _ [] inps =
     do clausifyInputs theory obligs inps
   
-  clausifyObligs theory obligs s (a:as) inps =
-    do cs <- clausForm s (nt a)
-       clausifyObligs theory (cs:obligs) s as inps
+  clausifyObligs theory obligs inp (a:as) inps =
+    do cs <-
+         clausForm inp {
+           what = nt a,
+           source = Inference "negate_conjecture" "cth" [inp] }
+       clausifyObligs theory (cs:obligs) inp as inps
 
   split' a | splitting flags = if null split_a then [true] else split_a
     where split_a = split a
@@ -99,18 +102,19 @@
 ----------------------------------------------------------------------
 -- core clausification algorithm
 
-clausForm :: String -> Form -> M [Input Clause]
-clausForm s p =
-  withName s $
-    do miniscoped      <- miniscope . check . simplify         . check $ p
+clausForm :: Input Form -> M [Input Clause]
+clausForm 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 !cnf_        = concatMap cnf                        . check $ noForAllPs
+       let !thm         = Input "skolemised" Axiom (Inference "clausify" "esa" [inp]) (And noForAllPs)
+           !cnf_        = concatMap cnf                        . check $ noForAllPs
            !simp        = simplifyCNF                          . check $ cnf_
            cs           = fmap clause                                  $ simp
-           inps         = [ Input (s ++ i) Axiom c
+           inps         = [ Input (tag inp ++ i) Axiom (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
@@ -167,9 +167,11 @@
     -- Just exists so that parsing followed by pretty-printing is
     -- somewhat lossless; the simplify function will get rid of it
   | Connective Connective Form Form
+  deriving (Eq, Ord)
 
 -- Miscellaneous connectives that exist in TPTP
 data Connective = Implies | Follows | Xor | Nor | Nand
+  deriving (Eq, Ord)
 
 connective :: Connective -> Form -> Form -> Form
 connective Implies t u = nt t \/ u
@@ -179,6 +181,7 @@
 connective Nand t u = nt (t /\ u)
 
 data Bind a = Bind (Set Variable) a
+  deriving (Eq, Ord)
 
 true, false :: Form
 true = And []
@@ -290,6 +293,15 @@
 toLiterals :: Clause -> [Literal]
 toLiterals (Clause (Bind _ ls)) = ls
 
+toClause :: Form -> Maybe Clause
+toClause (ForAll (Bind _ f)) = toClause f
+toClause f = clause <$> cl f
+  where
+    cl (Or fs) = concat <$> mapM cl fs
+    cl (Literal l) = Just [l]
+    cl (Not (Literal l)) = Just [neg l]
+    cl _ = Nothing
+
 ----------------------------------------------------------------------
 -- Problems
 
@@ -308,10 +320,16 @@
 data NoAnswerReason = GaveUp | Timeout deriving (Eq, Ord, Show)
 
 data Input a = Input
-  { tag ::  Tag,
-    kind :: Kind,
-    what :: a }
+  { tag    :: Tag,
+    kind   :: Kind,
+    source :: InputSource,
+    what   :: a }
 
+data InputSource =
+    Unknown
+  | FromFile String Int
+  | Inference String String [Input Form]
+
 type Problem a = [Input a]
 
 instance Functor Input where
@@ -404,7 +422,7 @@
   rep' (x:xs) = Binary (:) x xs
 
 instance Symbolic a => Unpack (Input a) where
-  rep' (Input tag kind what) = Unary (Input tag kind) what
+  rep' (Input tag kind info what) = Unary (Input tag kind info) what
 
 instance Unpack CNF where
   rep' (CNF ax conj s1 s2) =
@@ -543,6 +561,19 @@
 functions = usort . termsAndBinders term mempty where
   term (f :@: _) = return f
   term _ = mempty
+
+funOcc :: Symbolic a => Function -> a -> Int
+funOcc f x = getSum (occ x)
+  where
+    occ :: Symbolic a => a -> Sum Int
+    occ x = collect occ x `mappend` occ1 x
+
+    occ1 :: Symbolic a => a -> Sum Int
+    occ1 x
+      | Term <- typeOf x,
+        g :@: _ <- x,
+        f == g = Sum 1
+      | otherwise = mempty
 
 isFof :: Symbolic a => a -> Bool
 isFof f = length (types' f) <= 1
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) prelude ++
-          map (Input "program" Axiom) program ++
+  return (map (Input "adt" Axiom Unknown) prelude ++
+          map (Input "program" 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
@@ -25,7 +25,7 @@
   }
 
 guard :: Scheme1 -> (Type -> Bool) -> Input Form -> Input Form
-guard scheme mono (Input t k f) = Input t k (aux (pos k) f)
+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))))
@@ -65,18 +65,25 @@
         map (simplify . ForAll . bind) . split . simplify . foldr (/\) true $
           funcAxioms ++ typeAxioms
   return $
-    [ Input ("types" ++ show i) Axiom axiom | (axiom, i) <- zip axioms [1..] ] ++
+    [ Input ("types" ++ show i) Axiom (Inference "type_axiom" "esa" []) axiom | (axiom, i) <- zip axioms [1..] ] ++
     map (guard scheme1' mono') inps
 
 translate scheme mono f =
   let f' =
         Form.run f $ \inps -> do
-          forM inps $ \(Input tag kind f) -> do
+          forM inps $ \inp@(Input tag kind _ f) -> do
             let prepare f = fmap (foldr (/\) true) (run (withName tag (removeEquiv (simplify f))))
-            fmap (Input tag kind) $
-              case kind of
-                Axiom -> prepare f
-                Conjecture -> fmap notInwards (prepare (nt f))
+            case kind of
+              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))
       typeI = Type (name "$i") (Finite 0) Infinite
       trType O = O
       trType ty = typeI
diff --git a/src/Jukebox/Provers/E.hs b/src/Jukebox/Provers/E.hs
--- a/src/Jukebox/Provers/E.hs
+++ b/src/Jukebox/Provers/E.hs
@@ -88,7 +88,7 @@
           , suffix == suffix' ]
         parse xs =
           let toks = scan xs
-          in case run_ parser (UserState initialState toks) of
+          in case run_ parser (UserState (initialState Nothing) toks) of
             Ok _ ts -> ts
             _ -> error "runE: couldn't parse result from E"
         parser =
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
@@ -31,7 +31,8 @@
 -- The parser monad
 
 data ParseState =
-  MkState ![Input Form]            -- problem being constructed, inputs are in reverse order
+  MkState (Maybe String)           -- filename
+          ![Input Form]            -- problem being constructed, inputs are in reverse order
           !(Map String Type)       -- types in scope
           !(Map String [Function]) -- functions in scope
           !(Map String Variable)   -- variables in scope, for CNF
@@ -43,9 +44,9 @@
 data IncludeStatement = Include String (Maybe [Tag]) deriving Show
 
 -- The initial parser state.
-initialState :: ParseState
-initialState =
-  initialStateFrom []
+initialState :: Maybe String -> ParseState
+initialState mfile =
+  initialStateFrom mfile []
     (Map.fromList [(show (name ty), ty) | ty <- [int, rat, real]])
     (Map.fromList
        [ (fun,
@@ -77,8 +78,8 @@
        fun ["$to_rat"]  (\ty -> FunType [ty] rat) ++
        fun ["$to_real"] (\ty -> FunType [ty] real)
 
-initialStateFrom :: [Name] -> Map String Type -> Map String [Function] -> ParseState
-initialStateFrom xs tys fs = MkState [] tys fs Map.empty n
+initialStateFrom :: Maybe String -> [Name] -> Map String Type -> Map String [Function] -> ParseState
+initialStateFrom mfile xs tys fs = MkState mfile [] tys fs Map.empty n
   where
     n = maximum (0:[succ m | Unique m _ _ <- xs])
 
@@ -117,7 +118,7 @@
   Location file (fromIntegral row) (fromIntegral col)
 
 parseProblem :: FilePath -> String -> ParseResult [Input Form]
-parseProblem name contents = parseProblemFrom initialState name contents
+parseProblem name contents = parseProblemFrom (initialState (Just name)) name contents
 
 parseProblemFrom :: ParseState -> FilePath -> String -> ParseResult [Input Form]
 parseProblemFrom state name contents =
@@ -155,11 +156,11 @@
     merge (Just xs) (Just ys) = Just (xs `intersect` ys)
 
     finalise :: ParseState -> Problem Form
-    finalise (MkState p _ _ _ _) = check (reverse p)
+    finalise (MkState _ p _ _ _ _) = check (reverse p)
 
 -- Wee function for testing.
 testParser :: Parser a -> String -> Either [String] a
-testParser p s = snd (run (const []) p (UserState initialState (scan s)))
+testParser p s = snd (run (const []) p (UserState (initialState Nothing) (scan s)))
 
 -- Primitive parsers.
 
@@ -250,17 +251,25 @@
 
 -- A TPTP kind.
 kind :: Parser (Tag -> Form -> Input Form)
-kind = axiom Axiom <|> axiom Hypothesis <|> axiom Definition <|>
-       axiom Assumption <|> axiom Lemma <|> axiom Theorem <|>
-       general Conjecture Form.Conjecture <|>
-       general NegatedConjecture Form.Axiom <|>
-       general Question Form.Question
-  where axiom t = general t Form.Axiom
-        general k kind = keyword k >> return (mk kind)
-        mk kind tag form =
-          Input { Form.tag = tag,
-                  Form.kind = kind,
-                  Form.what = form }
+kind = do
+  MkState mfile _ _ _ _ _ <- getState
+  UserState _ (At (L.Pos n _) _) <- getPosition
+  let
+    axiom t = general t Form.Axiom
+    general k kind = keyword k >> return (mk kind)
+    mk kind tag form =
+      Input { Form.tag = tag,
+              Form.kind = kind,
+              Form.what = form,
+              Form.source =
+                case mfile of
+                  Nothing -> Form.Unknown
+                  Just file -> FromFile file (fromIntegral n) }
+  axiom Axiom <|> axiom Hypothesis <|> axiom Definition <|>
+    axiom Assumption <|> axiom Lemma <|> axiom Theorem <|>
+    general Conjecture Form.Conjecture <|>
+    general NegatedConjecture Form.Axiom <|>
+    general Question Form.Question
 
 -- A formula name.
 tag :: Parser Tag
@@ -282,8 +291,8 @@
 
 newFormula :: Input Form -> Parser ()
 newFormula input = do
-  MkState p t f v n <- getState
-  putState (MkState (input:p) t f v n)
+  MkState mfile p t f v n <- getState
+  putState (MkState mfile (input:p) t f v n)
   
 newFunction :: String -> FunType -> Parser Function
 newFunction name ty = do
@@ -325,22 +334,22 @@
 {-# INLINE lookupType #-}
 lookupType :: String -> Parser Type
 lookupType xs = do
-  MkState p t f v n <- getState
+  MkState mfile p t f v n <- getState
   case Map.lookup xs t of
     Nothing -> do
       let ty = Type (name xs) Infinite Infinite
-      putState (MkState p (Map.insert xs ty t) f v n)
+      putState (MkState mfile p (Map.insert xs ty t) f v n)
       return ty
     Just ty -> return ty
 
 {-# INLINE lookupFunction #-}
 lookupFunction :: FunType -> String -> Parser [Name ::: FunType]
 lookupFunction def x = do
-  MkState p t f v n <- getState
+  MkState mfile p t f v n <- getState
   case Map.lookup x f of
     Nothing -> do
       let decl = name x ::: def
-      putState (MkState p t (Map.insert x [decl] f) v n)
+      putState (MkState mfile p t (Map.insert x [decl] f) v n)
       return [decl]
     Just fs -> return fs
 
@@ -352,10 +361,10 @@
 
 cnf, tff, fof :: Parser Form
 cnf = do
-  MkState p t f _ n <- getState
-  putState (MkState p t f Map.empty n)
+  MkState mfile p t f _ n <- getState
+  putState (MkState mfile p t f Map.empty n)
   form <- formula NoQuantification __
-  MkState _ _ _ vs _ <- getState
+  MkState _ _ _ _ vs _ <- getState
   return (ForAll (Bind (Set.fromList (Map.elems vs)) form))
 tff = formula Typed Map.empty
 fof = formula Untyped Map.empty
@@ -424,12 +433,12 @@
   {-# INLINE var #-}
   var NoQuantification _ = do
     x <- variable
-    MkState p t f ctx n <- getState
+    MkState mfile p t f ctx n <- getState
     case Map.lookup x ctx of
       Just v -> return (Var v)
       Nothing -> do
         let v = Unique (n+1) x defaultRenamer ::: individual
-        putState (MkState p t f (Map.insert x v ctx) (n+1))
+        putState (MkState mfile p t f (Map.insert x v ctx) (n+1))
         return (Var v)
   var _ ctx = do
     x <- variable
@@ -562,8 +571,8 @@
                Untyped ->
                  fatalError "Used a typed quantification in an untyped formula" };
              type_ } <|> return individual
-  MkState p t f v n <- getState
-  putState (MkState p t f v (n+1))
+  MkState mfile p t f v n <- getState
+  putState (MkState mfile p t f v (n+1))
   return (Unique n x defaultRenamer ::: ty)
 
 -- Parse a type
diff --git a/src/Jukebox/TPTP/ParseSnippet.hs b/src/Jukebox/TPTP/ParseSnippet.hs
--- a/src/Jukebox/TPTP/ParseSnippet.hs
+++ b/src/Jukebox/TPTP/ParseSnippet.hs
@@ -21,8 +21,8 @@
 form :: Symbolic a => Parser a -> [(String, Type)] -> [(String, Function)] -> String -> a
 form parser types funs0 str =
   case run_ (parser <* eof)
-            (UserState (MkState [] (Map.delete "$i" (Map.fromList types)) (Map.fromList funs) Map.empty 0) (scan str)) of
-    Ok (UserState (MkState _ types' funs' _ _) (At _ (Cons Eof _))) res
+            (UserState (MkState Nothing [] (Map.delete "$i" (Map.fromList types)) (Map.fromList funs) Map.empty 0) (scan str)) of
+    Ok (UserState (MkState _ _ types' funs' _ _) (At _ (Cons Eof _))) res
       | Map.insert "$i" individual (Map.fromList types) /=
         Map.insert "$i" individual types' ->
         error $ "ParseSnippet: type implicitly defined: " ++
diff --git a/src/Jukebox/TPTP/Parsec.hs b/src/Jukebox/TPTP/Parsec.hs
--- a/src/Jukebox/TPTP/Parsec.hs
+++ b/src/Jukebox/TPTP/Parsec.hs
@@ -173,3 +173,7 @@
 {-# INLINE putState #-}
 putState :: state -> Parsec (UserState state a) ()
 putState state = Parsec (\ok err UserState{userStream = stream} exp -> ok () err (UserState state stream) exp)
+
+{-# INLINE getPosition #-}
+getPosition :: Stream a b => Parsec a (Position a)
+getPosition = Parsec (\ok err inp exp -> ok (position inp) err inp exp)
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
@@ -1,10 +1,11 @@
 -- Pretty-printing of formulae. WARNING: icky code inside!
-{-# LANGUAGE FlexibleContexts, TypeSynonymInstances, TypeOperators, FlexibleInstances, CPP, GADTs #-}
-module Jukebox.TPTP.Print(prettyShow, prettyNames, showClauses, pPrintClauses, showProblem, pPrintProblem)
+{-# LANGUAGE FlexibleContexts, TypeSynonymInstances, TypeOperators, FlexibleInstances, CPP, GADTs, PatternGuards #-}
+module Jukebox.TPTP.Print(prettyShow, prettyNames, showClauses, pPrintClauses, showProblem, pPrintProblem, pPrintProof)
        where
 
 #include "errors.h"
 import Data.Char
+import Data.Maybe
 import Text.PrettyPrint.HughesPJ
 import qualified Jukebox.TPTP.Lexer as L
 import Jukebox.Form
@@ -33,6 +34,92 @@
   where
     prob = prettyNames prob0
 
+-- 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)))
+  where
+    fun f [] = text f
+    fun f xs = text f <> parens (fsep (punctuate comma xs))
+    list = brackets . fsep . punctuate comma
+
+    clause n = "c" ++ show n
+
+    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
+      | 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)
+
+pPrintAnnotProof :: [(Input Form, (String, [Doc]))] -> Doc
+pPrintAnnotProof annots0 =
+  vcat $
+    [ vcat (pPrintDecls inps) | not (isReallyFof inps) ] ++
+    [ pPrintClause (family x) (tag inp) k (pp x:rest)
+    | (inp, (k, rest)) <- annots,
+      let x = what inp ]
+  where
+    inps0 = map fst annots0
+    inps = prettyNames inps0
+    annots = zip inps (map snd annots0)
+
+    family x
+      | isReallyFof x && isJust (toClause x) = "cnf"
+      | isReallyFof x = "fof"
+      | otherwise = "tff"
+
+    pp x
+      | isReallyFof x =
+        case toClause x of
+          Nothing -> pPrintFof 0 x
+          Just cl -> pPrint cl
+      | otherwise =
+        pPrintTff 0 x
+
 showProblem :: Problem Form -> String
 showProblem = show . pPrintProblem
 
@@ -57,7 +144,7 @@
     funcDecl (f ::: ty) = typeClause f (pPrint ty)
     typeClause name ty =
       pPrintClause "tff" "type" "type"
-        (text (escapeAtom (show name)) <> colon <+> ty)
+        [text (escapeAtom (show name)) <> colon <+> ty]
 
 instance Pretty a => Pretty (Input a) where
   pPrint = pPrintInput "tff" pPrint
@@ -66,11 +153,11 @@
 
 pPrintInput :: String -> (a -> Doc) -> Input a -> Doc
 pPrintInput family pp i =
-  pPrintClause family (tag i) (show (kind i)) (pp (what i))
+  pPrintClause family (tag i) (show (kind i)) [pp (what i)]
 
-pPrintClause :: String -> String -> String -> Doc -> Doc
+pPrintClause :: String -> String -> String -> [Doc] -> Doc
 pPrintClause family name kind rest =
-  text family <> parens (sep [text (escapeAtom name) <> comma <+> text kind <> comma, rest]) <> text "."
+  text family <> parens (sep (punctuate comma ([text (escapeAtom name), text kind] ++ rest))) <> text "."
 
 instance Pretty Clause where
   pPrint (Clause (Bind _ ts)) =