diff --git a/jukebox.cabal b/jukebox.cabal
--- a/jukebox.cabal
+++ b/jukebox.cabal
@@ -1,5 +1,5 @@
 Name: jukebox
-Version: 0.2.16
+Version: 0.2.17
 Cabal-version: >= 1.8
 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
@@ -73,15 +73,20 @@
           show p == show q =
             annot inp { source = source inp' }
       | otherwise = do
-          mn <- newNumber inp
+          mn <- findNumber inp
           case mn of
-            Nothing ->
+            Just _ ->
               -- Already processed this formula
               return []
-            Just n -> do
+            Nothing -> do
               let
-                ret k stuff =
-                  return [(inp { tag = clause n }, (k, stuff))]
+                ret k stuff = do
+                  res <- newNumber inp
+                  case res of
+                    Just n ->
+                      return [(inp { tag = clause n }, (k, stuff))]
+                    Nothing ->
+                      return []
 
               case source inp of
                 Unknown -> ret "plain" []