diff --git a/Folly.cabal b/Folly.cabal
--- a/Folly.cabal
+++ b/Folly.cabal
@@ -2,7 +2,7 @@
 --  see http://haskell.org/cabal/users-guide/
 
 name:                Folly
-version:             0.1.5.2
+version:             0.2.0.0
 synopsis:            A first order logic library in Haskell
 description:         An implementation of first order logic in Haskell that
 		     includes a library of modules for incorporating first
diff --git a/src/Folly/Clause.hs b/src/Folly/Clause.hs
--- a/src/Folly/Clause.hs
+++ b/src/Folly/Clause.hs
@@ -5,6 +5,7 @@
                     showTrace) where
 
 import Data.List as L
+import Data.Map as M
 import Data.Maybe
 import Data.Set as S
 
@@ -21,15 +22,21 @@
   (<=) (Clause cs1 _) (Clause cs2 _) = cs1 <= cs2
 
 givenClause cs = Clause cs Given
-resolvedClause cs lc rc mgu = Clause cs (Resolved lc rc mgu)
+resolvedClause cs lc rc mgu = Clause cs (Resolved lc rc mgu M.empty)
 
 empty = Clause S.empty Given
 
 data Justification
   = Given
-  | Resolved Clause Clause Unifier
+  | Resolved Clause Clause Unifier Unifier
     deriving (Eq, Ord, Show)
 
+applySub :: Unifier -> Clause -> Clause
+applySub u c@(Clause lits j) =
+  Clause (S.map (\lit -> applyToTerms lit (applyUnifier u)) lits) j
+
+allVars (Clause cs _) = L.concatMap collectVars $ S.toList cs
+
 deleteTautologies :: Set Clause -> Set Clause
 deleteTautologies formulas = S.filter (not . dnfIsTautology) formulas
 
@@ -43,7 +50,12 @@
     negAtoms = S.map stripNegations $ S.filter (not . isAtom) c
 
 resolvedClauses :: Clause -> Clause -> Set Clause
-resolvedClauses l@(Clause left _) r@(Clause right _) =
+resolvedClauses c1 c2 =
+  let rho = uniqueVarSub (allVars c1) (allVars c2) in
+   resolvedClausesU (applySub rho c1) c2
+
+resolvedClausesU :: Clause -> Clause -> Set Clause
+resolvedClausesU l@(Clause left _) r@(Clause right _) =
   case left == right of
    True ->  S.empty
    False -> S.fromList resClauses
@@ -77,7 +89,7 @@
 showTrace c = showTraceRec 0 c
 
 showTraceRec n c@(Clause cs Given) = (ind n) ++ "GIVEN " ++ show cs
-showTraceRec n c@(Clause cs (Resolved a b u)) =
+showTraceRec n c@(Clause cs (Resolved a b u _)) =
   (ind n) ++ show cs ++ "\t" ++ show u ++ "\n" ++
   showTraceRec (n+1) a ++ "\n" ++
   showTraceRec (n+1) b
diff --git a/src/Folly/Formula.hs b/src/Folly/Formula.hs
--- a/src/Folly/Formula.hs
+++ b/src/Folly/Formula.hs
@@ -1,8 +1,8 @@
 module Folly.Formula(
   Term, Formula,
   fvt, subTerm, isVar, isConst, isFunc,
-  funcName, funcArgs,
-  appendVarName,
+  funcName, funcArgs, varName,
+  appendVarName, collectVars,
   var, func, constant,
   te, fa, pr, con, dis, neg, imp, bic, t, f,
   vars, freeVars, isAtom, stripNegations,
@@ -51,6 +51,8 @@
   False -> Func n args
 constant n = Constant n
 
+varName (Var n) = n
+
 appendVarName :: String -> Term -> Term
 appendVarName suffix (Var n) = Var (n ++ suffix)
 appendVarName suffix (Func name args) = Func name $ L.map (appendVarName suffix) args
@@ -94,6 +96,13 @@
 applyToTerms (B n l r) f = B n (applyToTerms l f) (applyToTerms r f)
 applyToTerms (Q n v l) f = Q n (f v) (applyToTerms l f)
 applyToTerms (N l) f = N (applyToTerms l f)
+
+collectVars :: Formula -> [Term]
+collectVars (P _ args) = L.concatMap (\t -> if isVar t then [t] else []) args
+collectVars (N f) = collectVars f
+collectVars (B _ a b) = collectVars a ++ collectVars b
+collectVars (Q _ v f) = v:(collectVars f)
+collectVars _ = []
 
 te :: Term -> Formula -> Formula
 te v@(Var _) f = Q "E" v f
diff --git a/src/Folly/Resolution.hs b/src/Folly/Resolution.hs
--- a/src/Folly/Resolution.hs
+++ b/src/Folly/Resolution.hs
@@ -1,4 +1,7 @@
-module Folly.Resolution(isValid) where
+module Folly.Resolution(isValid,
+                        isValid',
+                        standardSkolem,
+                        maxClause) where
 
 import Data.List as L
 import Data.Set as S
@@ -8,38 +11,36 @@
 import Folly.Theorem
 
 isValid :: Theorem -> Bool
-isValid t = not $ resolve $ deleteTautologies $ clauseSet
-  where
-    formulas = (neg (conclusion t)) : (hypothesis t)
-    clauses = L.map (givenClause . S.fromList) $ uniqueVarNames $ toClausalForm $ L.foldr (\l r -> con l r) (head formulas) (tail formulas)
-    clauseSet = S.fromList clauses
+isValid t = isValid' maxClause standardSkolem t
 
-resolve :: Set Clause -> Bool
-resolve cls = case S.member C.empty cls of
-  True -> False
-  False -> resolveIter [cls]
+maxClause cs = S.findMax cs
 
-resolveIter :: [Set Clause] -> Bool
-resolveIter [] = error "Empty list of clause sets"
-resolveIter clauseSets = case S.size newClauses == 0 of
-  True -> True
-  False -> case S.member C.empty newClauses of
-    True -> False
-    False -> resolveIter (newClauses:clauseSets)
+standardSkolem t = deleteTautologies $ clauseSet
   where
-    newClauses = generateNewClauses (head clauseSets) (L.foldl S.union S.empty clauseSets)
-
-generateNewClauses :: Set Clause -> Set Clause -> Set Clause
-generateNewClauses recent old = deleteTautologies $ newClauses
+    formulas = (neg (conclusion t)) : (hypothesis t)
+    clauses = L.map (givenClause . S.fromList) $ toClausalForm $ L.foldr (\l r -> con l r) (head formulas) (tail formulas)
+    clauseSet = S.fromList clauses
+  
+isValid' :: (Set Clause -> Clause) -> -- Clause selection
+            (Theorem -> Set Clause) -> -- Preprocessor
+            Theorem -> Bool
+isValid' s p t =
+  case S.size clauses == 0 of
+   True -> False
+   False -> not $ resolve s (S.singleton (s clauses)) (S.delete (s clauses) clauses)
   where
-    newClauses = S.fold S.union S.empty $ S.map (\c -> genNewClauses c old) recent
-    genNewClauses c cs = S.fold S.union S.empty $ S.map (\x -> resolvedClauses c x) cs
-
-uniqueVarNames :: [[Formula]] -> [[Formula]]
-uniqueVarNames cls = zipWith attachSuffix cls (L.map show [1..length cls])
+    clauses = p t
 
-attachSuffix :: [Formula] -> String -> [Formula]
-attachSuffix cls suffix = L.map (addSuffixToVarNames suffix) cls
+resolve :: (Set Clause -> Clause) -> Set Clause -> Set Clause -> Bool
+resolve s axioms cls = case S.member C.empty axioms ||
+                            S.member C.empty cls of
+  True -> False
+  False -> case S.size cls == 0 of
+    True -> True
+    False ->
+      let c = s cls
+          newClauses = genNewClauses c axioms in
+       resolve s (S.insert c axioms) (S.delete c $ S.union newClauses cls)
 
-addSuffixToVarNames :: String -> Formula -> Formula
-addSuffixToVarNames suffix form = applyToTerms form (appendVarName suffix)
+genNewClauses c cls =
+  S.fold S.union S.empty $ S.map (\x -> S.union (resolvedClauses c x) (resolvedClauses x c)) (S.delete c cls)
diff --git a/src/Folly/Unification.hs b/src/Folly/Unification.hs
--- a/src/Folly/Unification.hs
+++ b/src/Folly/Unification.hs
@@ -1,7 +1,8 @@
 module Folly.Unification(Unifier,
                          applyUnifier,
                          mostGeneralUnifier,
-                         unifier) where
+                         unifier,
+                         uniqueVarSub) where
 
 import Control.Monad
 import Data.List as L
@@ -12,6 +13,19 @@
 
 type Unifier = Map Term Term
 
+uniqueVarSub :: [Term] -> [Term] -> Unifier
+uniqueVarSub lt rt =
+  let overlappingNames = L.intersect lt rt in
+   case overlappingNames of
+    [] -> M.empty
+    _ -> M.fromList $ L.zip overlappingNames (genUniqueVars (L.length overlappingNames) (lt ++ rt))
+
+genUniqueVars n exclude =
+  let excludedNames = L.reverse $ L.sort $ L.map varName exclude
+      prefixes = L.replicate n $ L.head excludedNames
+      newNames = L.zipWith (\p z -> p ++ show z) prefixes $ [1..n] in
+   L.map var newNames
+   
 unifier :: [(Term, Term)] -> Unifier
 unifier subs = M.fromList subs