diff --git a/Data/Logic/KnowledgeBase.hs b/Data/Logic/KnowledgeBase.hs
--- a/Data/Logic/KnowledgeBase.hs
+++ b/Data/Logic/KnowledgeBase.hs
@@ -1,5 +1,5 @@
-{-# LANGUAGE DeriveDataTypeable, FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, OverloadedStrings, RankNTypes,
-             TypeSynonymInstances, UndecidableInstances #-}
+{-# LANGUAGE DeriveDataTypeable, FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, OverloadedStrings, PackageImports,
+             RankNTypes, TemplateHaskell, TypeSynonymInstances, UndecidableInstances #-}
 {-# OPTIONS -Wall #-}
 
 {- KnowledgeBase.hs -}
@@ -24,9 +24,9 @@
     , showKB
     ) where
 
-import Control.Monad.Identity (Identity(runIdentity))
-import Control.Monad.State (StateT, evalStateT, MonadState(get, put))
-import Control.Monad.Trans (lift)
+import "mtl" Control.Monad.Identity (Identity(runIdentity))
+import "mtl" Control.Monad.State (StateT, evalStateT, MonadState(get, put))
+import "mtl" Control.Monad.Trans (lift)
 import Data.Generics (Data, Typeable)
 import Data.Logic.Classes.FirstOrder (FirstOrderFormula)
 import Data.Logic.Classes.Negatable (Negatable(..))
@@ -34,7 +34,9 @@
 import Data.Logic.Normal.Implicative (ImplicativeForm, implicativeNormalForm)
 import Data.Logic.Normal.Skolem (NormalT, runNormalT)
 import Data.Logic.Resolution (prove, SetOfSupport, getSetOfSupport)
+import Data.SafeCopy (deriveSafeCopy, base)
 import qualified Data.Set.Extra as S
+import Happstack.Data (Default(defaultValue), deriveNewDataNoDefault)
 import Prelude hiding (negate)
 
 type SentenceCount = Int
@@ -62,24 +64,27 @@
 
 data ProverState inf
     = ProverState
-      { knowledgeBase :: KnowledgeBase inf
+      { recursionLimit :: Maybe Int
+      , knowledgeBase :: KnowledgeBase inf
       , sentenceCount :: Int }
 
-zeroKB :: ProverState inf
-zeroKB = ProverState
-         { knowledgeBase = S.empty
+zeroKB :: Maybe Int -> ProverState inf
+zeroKB limit =
+    ProverState
+         { recursionLimit = limit
+         , knowledgeBase = S.empty
          , sentenceCount = 1 }
 
 -- |A monad for running the knowledge base.
 type ProverT inf = StateT (ProverState inf)
 type ProverT' v term inf m a = ProverT inf (NormalT v term m) a
 
-runProverT' :: Monad m => ProverT' v term inf m a -> m a
-runProverT' = runNormalT . runProverT
-runProverT :: Monad m => StateT (ProverState inf) m a -> m a
-runProverT action = evalStateT action zeroKB
-runProver' :: ProverT' v term inf Identity a -> a
-runProver' = runIdentity . runProverT'
+runProverT' :: Monad m => Maybe Int -> ProverT' v term inf m a -> m a
+runProverT' limit = runNormalT . runProverT limit
+runProverT :: Monad m => Maybe Int -> StateT (ProverState inf) m a -> m a
+runProverT limit action = evalStateT action (zeroKB limit)
+runProver' :: Maybe Int -> ProverT' v term inf Identity a -> a
+runProver' limit = runIdentity . runProverT' limit
 {-
 runProver :: StateT (ProverState inf) Identity a -> a
 runProver = runIdentity . runProverT
@@ -94,6 +99,13 @@
     -- ^ Both are satisfiable
     deriving (Data, Typeable, Eq, Ord, Show)
 
+$(deriveSafeCopy 1 'base ''ProofResult)
+
+$(deriveNewDataNoDefault [''ProofResult])
+
+instance Default ProofResult where
+    defaultValue = Invalid
+
 data Proof lit = Proof {proofResult :: ProofResult, proof :: S.Set (ImplicativeForm lit)} deriving (Data, Typeable, Eq, Ord)
 
 instance (Ord lit, Show lit, Literal lit term v p f, FirstOrderFormula lit term v p f) => Show (Proof lit) where
@@ -112,26 +124,31 @@
 
 -- |Return a flag indicating whether sentence was disproved, along
 -- with a disproof.
-inconsistantKB :: forall m formula term v p f lit. (FirstOrderFormula formula term v p f, Literal lit term v p f, Monad m) =>
+inconsistantKB :: forall m formula term v p f lit. (FirstOrderFormula formula term v p f, Literal lit term v p f, Monad m, Show term) =>
                   formula -> ProverT' v term (ImplicativeForm lit) m (Bool, SetOfSupport lit v term)
-inconsistantKB s = lift (implicativeNormalForm s) >>= return . getSetOfSupport >>= \ sos -> getKB >>= return . prove S.empty sos . S.map wiItem
+inconsistantKB s =
+    get >>= \ st ->
+    lift (implicativeNormalForm s) >>=
+    return . getSetOfSupport >>= \ sos ->
+    getKB >>=
+    return . prove (recursionLimit st) S.empty sos . S.map wiItem
 
 -- |Return a flag indicating whether sentence was proved, along with a
 -- proof.
-theoremKB :: forall m formula term v p f lit. (Monad m, FirstOrderFormula formula term v p f, Literal lit term v p f) =>
+theoremKB :: forall m formula term v p f lit. (Monad m, FirstOrderFormula formula term v p f, Literal lit term v p f, Show term) =>
              formula -> ProverT' v term (ImplicativeForm lit) m (Bool, SetOfSupport lit v term)
 theoremKB s = inconsistantKB ((.~.) s)
 
 -- |Try to prove a sentence, return the result and the proof.
 -- askKB should be in KnowledgeBase module. However, since resolution
 -- is here functions are here, it is also placed in this module.
-askKB :: (Monad m, FirstOrderFormula formula term v p f, Literal lit term v p f) =>
+askKB :: (Monad m, FirstOrderFormula formula term v p f, Literal lit term v p f, Show term) =>
          formula -> ProverT' v term (ImplicativeForm lit) m Bool
 askKB s = theoremKB s >>= return . fst
 
 -- |See whether the sentence is true, false or invalid.  Return proofs
 -- for truth and falsity.
-validKB :: (FirstOrderFormula formula term v p f, Literal lit term v p f, Monad m) =>
+validKB :: (FirstOrderFormula formula term v p f, Literal lit term v p f, Monad m, Show term) =>
            formula -> ProverT' v term (ImplicativeForm lit) m (ProofResult, SetOfSupport lit v term, SetOfSupport lit v term)
 validKB s =
     theoremKB s >>= \ (proved, proof1) ->
@@ -141,7 +158,7 @@
 -- |Validate a sentence and insert it into the knowledgebase.  Returns
 -- the INF sentences derived from the new sentence, or Nothing if the
 -- new sentence is inconsistant with the current knowledgebase.
-tellKB :: (FirstOrderFormula formula term v p f, Literal lit term v p f, Monad m) =>
+tellKB :: (FirstOrderFormula formula term v p f, Literal lit term v p f, Monad m, Show term) =>
           formula -> ProverT' v term (ImplicativeForm lit) m (Proof lit)
 tellKB s =
     do st <- get
@@ -154,7 +171,7 @@
                      , sentenceCount = sentenceCount st + 1 }
        return $ Proof {proofResult = valid, proof = S.map wiItem inf'}
 
-loadKB :: (FirstOrderFormula formula term v p f, Literal lit term v p f, Monad m) =>
+loadKB :: (FirstOrderFormula formula term v p f, Literal lit term v p f, Monad m, Show term) =>
           [formula] -> ProverT' v term (ImplicativeForm lit) m [Proof lit]
 loadKB sentences = mapM tellKB sentences
 
diff --git a/Data/Logic/Normal/Implicative.hs b/Data/Logic/Normal/Implicative.hs
--- a/Data/Logic/Normal/Implicative.hs
+++ b/Data/Logic/Normal/Implicative.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE DeriveDataTypeable, RankNTypes, ScopedTypeVariables #-}
+{-# LANGUAGE DeriveDataTypeable, PackageImports, RankNTypes, ScopedTypeVariables #-}
 {-# OPTIONS -Wall #-}
 module Data.Logic.Normal.Implicative
     ( ImplicativeForm(INF, neg, pos)
@@ -11,7 +11,7 @@
 import Data.Logic.Normal.Clause (clauseNormalForm)
 import Data.Logic.Normal.Skolem (NormalT)
 
-import Control.Monad.State (MonadPlus, msum)
+import "mtl" Control.Monad.State (MonadPlus, msum)
 import Data.Generics (Data, Typeable, listify)
 import Data.List (intersperse)
 import Data.Logic.Classes.FirstOrder (FirstOrderFormula(..))
diff --git a/Data/Logic/Normal/Skolem.hs b/Data/Logic/Normal/Skolem.hs
--- a/Data/Logic/Normal/Skolem.hs
+++ b/Data/Logic/Normal/Skolem.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE RankNTypes, ScopedTypeVariables #-}
+{-# LANGUAGE PackageImports, RankNTypes, ScopedTypeVariables #-}
 {-# OPTIONS -Wall #-}
 module Data.Logic.Normal.Skolem
     ( LiteralMapT
@@ -14,8 +14,8 @@
 import Data.Logic.Normal.Negation (negationNormalForm)
 import Data.Logic.Normal.Prenex (prenexNormalForm)
 
-import Control.Monad.Identity (Identity(runIdentity))
-import Control.Monad.State (StateT(runStateT), get, put)
+import "mtl" Control.Monad.Identity (Identity(runIdentity))
+import "mtl" Control.Monad.State (StateT(runStateT), get, put)
 import Data.Logic.Classes.FirstOrder (FirstOrderFormula(..), freeVars, Quant(..), substitute)
 import Data.Logic.Classes.Propositional (Combine(..), BinOp(..))
 import Data.Logic.Classes.Logic (Logic(..))
diff --git a/Data/Logic/Resolution.hs b/Data/Logic/Resolution.hs
--- a/Data/Logic/Resolution.hs
+++ b/Data/Logic/Resolution.hs
@@ -26,15 +26,22 @@
 
 type Unification lit v term = (ImplicativeForm lit, Subst v term)
 
-prove :: Literal lit term v p f =>
-         SetOfSupport lit v term -> SetOfSupport lit v term -> S.Set (ImplicativeForm lit) -> (Bool, SetOfSupport lit v term)
-prove ss1 ss2' kb =
+prove :: (Literal lit term v p f, Show v, Show term) =>
+         Maybe Int -- ^ Recursion limit.  We continue recursing until this
+                   -- becomes zero.  If it is negative it may recurse until
+                   -- it overflows the stack.
+      -> SetOfSupport lit v term
+      -> SetOfSupport lit v term
+      -> S.Set (ImplicativeForm lit)
+      -> (Bool, SetOfSupport lit v term)
+prove (Just 0) ss1 _ _ = (False, ss1)
+prove limit ss1 ss2' kb  =
     case S.minView ss2' of
       Nothing -> (False, ss1)
       Just (s, ss2) ->
           case prove' s kb ss2 ss1 of
             (ss', True) -> (True, (S.insert s (S.union ss1 ss')))
-            (ss', False) -> prove (S.insert s ss1) ss' (S.insert (fst s) kb)
+            (ss', False) -> prove (maybe Nothing (\ n -> Just (n - 1)) limit) (S.insert s ss1) ss' (S.insert (fst s) kb)
 -- prove ss1 [] _kb = (False, ss1)
 -- prove ss1 (s:ss2) kb =
 --     let
diff --git a/Data/Logic/Test.hs b/Data/Logic/Test.hs
--- a/Data/Logic/Test.hs
+++ b/Data/Logic/Test.hs
@@ -182,7 +182,7 @@
       doExpected (ConvertToChiou result) =
           TestCase (assertEqual (name f ++ " converted to Chiou") result (convertFOF id id id (formula f)))
       doExpected (ChiouKB1 result) =
-          TestCase (assertEqual (name f ++ " Chiou KB") result (runProver' (loadKB [formula f] >>= return . head)))
+          TestCase (assertEqual (name f ++ " Chiou KB") result (runProver' Nothing (loadKB [formula f] >>= return . head)))
       doExpected (PropLogicSat result) =
           TestCase (assertEqual (name f ++ " PropLogic.satisfiable") result (runNormal (plSat (formula f))))
       doExpected (SatSolverCNF result) =
@@ -233,11 +233,11 @@
           [TestLabel (proofName p ++ " with " ++ fst (proofKnowledge p)) . TestList $
            [TestCase (assertEqual (proofName p ++ " with " ++ fst (proofKnowledge p) ++ " using Chiou prover")
                       result
-                      (runProver' (loadKB kb >> theoremKB c)))]]
+                      (runProver' Nothing (loadKB kb >> theoremKB c)))]]
       doExpected (ChiouKB result) =
           [TestLabel (proofName p ++ " with " ++ fst (proofKnowledge p)) . TestList $
            [TestCase (assertEqual (proofName p ++ " with " ++ fst (proofKnowledge p) ++ " Chiou knowledge base")
                       result
-                      (runProver' (loadKB kb >> getKB)))]]
+                      (runProver' Nothing (loadKB kb >> getKB)))]]
       kb = snd (proofKnowledge p) :: [formula]
       c = conjecture p :: formula
diff --git a/Data/Logic/Types/FirstOrderPublic.hs b/Data/Logic/Types/FirstOrderPublic.hs
--- a/Data/Logic/Types/FirstOrderPublic.hs
+++ b/Data/Logic/Types/FirstOrderPublic.hs
@@ -8,6 +8,7 @@
 
 module Data.Logic.Types.FirstOrderPublic
     ( Formula(..)
+    , Bijection(..)
     ) where
 
 import Data.Data (Data)
@@ -15,7 +16,6 @@
 import Data.Logic.Classes.Boolean (Boolean(..))
 import Data.Logic.Classes.FirstOrder (FirstOrderFormula(..))
 import qualified Data.Logic.Types.FirstOrder as N
-import Data.Logic.Classes.Literal (Literal)
 import Data.Logic.Classes.Logic (Logic(..))
 import Data.Logic.Classes.Negatable (Negatable(..))
 import Data.Logic.Classes.Pred (Pred(..))
diff --git a/logic-classes.cabal b/logic-classes.cabal
--- a/logic-classes.cabal
+++ b/logic-classes.cabal
@@ -1,5 +1,5 @@
 Name:             logic-classes
-Version:          0.45
+Version:          0.47
 License:          BSD3
 Author:           David Fox <dsf@seereason.com>
 Maintainer:       SeeReason Partners <partners@seereason.com>
@@ -14,7 +14,7 @@
 Cabal-version:    >= 1.2
 
 Library
- GHC-options: -threaded -Wall -O2
+ GHC-options: -Wall -O2
  Exposed-Modules:  Data.Logic
                    Data.Logic.Classes.Arity
                    Data.Logic.Classes.Boolean
@@ -43,7 +43,7 @@
                    Data.Logic.Types.FirstOrderPublic
                    Data.Logic.Types.Propositional
  Other-Modules:    Data.Logic.Test
- Build-Depends:    base < 5, containers, fgl, happstack-data, incremental-sat-solver,
+ Build-Depends:    base >= 4.3 && < 5, containers, fgl, happstack-data, incremental-sat-solver,
                    mtl, syb-with-class, text, PropLogic, pretty, safecopy, set-extra, syb
 
 Executable tests