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.2.0
+version:             0.1.3.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/Formula.hs b/src/Folly/Formula.hs
--- a/src/Folly/Formula.hs
+++ b/src/Folly/Formula.hs
@@ -12,6 +12,7 @@
   toPNF, toSkolemForm, skf,
   Clause,
   toClausalForm,
+  isTautology,
   matchingLiterals) where
 
 import Control.Monad
@@ -129,6 +130,14 @@
 freeVars (N f) = freeVars f
 freeVars (Q _ v f) = S.delete v (freeVars f)
 
+isAtom :: Formula -> Bool
+isAtom (P _ _) = True
+isAtom _ = False
+
+stripNegations :: Formula -> Formula
+stripNegations (N t) = t
+stripNegations f = f
+
 literalArgs :: Formula -> [Term]
 literalArgs (P _ a) = a
 literalArgs (N (P _ a)) = a
@@ -289,3 +298,9 @@
 splitDis :: Formula -> Clause
 splitDis (B "|" l r) = (splitDis l) ++ (splitDis r)
 splitDis f = [f]
+
+isTautology :: Clause -> Bool
+isTautology c = L.length (L.intersect atoms negAtoms) > 0
+  where
+    atoms = L.filter isAtom c
+    negAtoms = L.map stripNegations $ L.filter (not . isAtom) c
diff --git a/src/Folly/Resolution.hs b/src/Folly/Resolution.hs
--- a/src/Folly/Resolution.hs
+++ b/src/Folly/Resolution.hs
@@ -10,7 +10,7 @@
 import Folly.Unification
 
 isValid :: Theorem -> Bool
-isValid t = not $ resolve clauseSet
+isValid t = not $ resolve $ deleteTautologies $ clauseSet
   where
     formulas = (neg (conclusion t)) : (hypothesis t)
     clauses = uniqueVarNames $ L.concat $ L.map toClausalForm formulas
@@ -18,7 +18,7 @@
 
 resolve :: Set Clause -> Bool
 resolve cls = case S.member [] cls of
-  True -> False
+  True -> True
   False -> resolveIter [cls]
 
 resolveIter :: [Set Clause] -> Bool
@@ -34,7 +34,7 @@
       _ -> generateNewClauses (head clauseSets) (L.foldl S.union S.empty (tail clauseSets))
 
 generateNewClauses :: Set Clause -> Set Clause -> Set Clause
-generateNewClauses recent old = newClauses
+generateNewClauses recent old = deleteTautologies $ newClauses
   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
@@ -64,3 +64,6 @@
 
 addSuffixToVarNames :: String -> Formula -> Formula
 addSuffixToVarNames suffix form = applyToTerms form (appendVarName suffix)
+
+deleteTautologies :: Set Clause -> Set Clause
+deleteTautologies clauses = S.filter (not . isTautology) clauses
diff --git a/src/Main.hs b/src/Main.hs
--- a/src/Main.hs
+++ b/src/Main.hs
@@ -20,6 +20,8 @@
     Failed errMsg -> putStrLn errMsg
     Succeeded t -> do
       putStr $ show t
-      putStrLn $ "\n\nis " ++ (show $ isValid t)
+      case isValid t of
+        True -> putStrLn "\n\nIs Valid"
+        False -> putStrLn "\n\nIs not valid"
 
 processTheoremFile thmFileContents = (lexer thmFileContents) >>= parseTheorem