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.2.0.0
+version:             0.2.0.1
 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
@@ -15,6 +15,11 @@
 data Clause = Clause (Set Formula) Justification
            deriving (Show)
 
+data Justification
+  = Given
+  | Resolved Clause Clause Unifier Unifier
+    deriving (Eq, Ord, Show)
+
 instance Eq Clause where
   (==) (Clause cs1 _) (Clause cs2 _) = cs1 == cs2
 
@@ -26,11 +31,6 @@
 
 empty = Clause S.empty Given
 
-data Justification
-  = Given
-  | 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
@@ -88,10 +88,15 @@
 
 showTrace c = showTraceRec 0 c
 
-showTraceRec n c@(Clause cs Given) = (ind n) ++ "GIVEN " ++ show cs
+showTraceRec n c@(Clause cs Given) = (ind n) ++ "GIVEN " ++ showLits cs
 showTraceRec n c@(Clause cs (Resolved a b u _)) =
-  (ind n) ++ show cs ++ "\t" ++ show u ++ "\n" ++
+  (ind n) ++ showLits cs ++ "  " ++ show u ++ "\n" ++
   showTraceRec (n+1) a ++ "\n" ++
   showTraceRec (n+1) b
 
 ind n = L.concat $ L.replicate n "  "
+
+showLits ls = "{" ++ (L.concat $ L.intersperse " " $ L.map show lits) ++ "}"
+  where
+    lits = S.toList ls
+    n = L.length lits
diff --git a/src/Folly/Formula.hs b/src/Folly/Formula.hs
--- a/src/Folly/Formula.hs
+++ b/src/Folly/Formula.hs
@@ -5,6 +5,7 @@
   appendVarName, collectVars,
   var, func, constant,
   te, fa, pr, con, dis, neg, imp, bic, t, f,
+  (/\), (\/),
   vars, freeVars, isAtom, stripNegations,
   generalize, subFormula,
   applyToTerms,
@@ -86,7 +87,7 @@
 showFormula T = "True"
 showFormula F = "False"
 showFormula (P predName args) = predName ++ "[" ++ (concat $ intersperse ", " $ L.map showTerm args)  ++ "]"
---showFormula (N (P name args)) = "~" ++ show (P name args)
+showFormula (N (P name args)) = "~" ++ show (P name args)
 showFormula (N f) = "~(" ++ show f ++ ")"
 showFormula (B op f1 f2) = "(" ++ show f1 ++ " " ++ op ++ " "  ++ show f2 ++ ")"
 showFormula (Q q t f) = "(" ++ q ++ " "  ++ show t ++ " . " ++ show f ++ ")"
@@ -120,6 +121,9 @@
 neg f = N f
 t = T
 f = F
+
+(/\) = con
+(\/) = dis
 
 vars :: Formula -> Set Term
 vars T = S.empty
diff --git a/src/Folly/Lexer.hs b/src/Folly/Lexer.hs
--- a/src/Folly/Lexer.hs
+++ b/src/Folly/Lexer.hs
@@ -57,8 +57,8 @@
 
 lexer :: String -> Error [Token]
 lexer str = case parse parseToks "LEXER" str of
-  Left err -> Failed $ show err
-  Right toks -> Succeeded $ toks
+  Left err -> Left $ show err
+  Right toks -> Right toks
 
 parseToks = endBy parseTok spaces
 
diff --git a/src/Folly/Parser.hs b/src/Folly/Parser.hs
--- a/src/Folly/Parser.hs
+++ b/src/Folly/Parser.hs
@@ -14,8 +14,8 @@
 
 parseTheorem :: [Token] -> Error Theorem
 parseTheorem toks = case parse parseTheoremToks "PARSER" toks of
-  Left err -> Failed $ show err
-  Right thm -> Succeeded thm
+  Left err -> Left $ show err
+  Right thm -> Right thm
 
 parseTheoremToks = do
   axioms <- parseHypothesis
@@ -34,8 +34,8 @@
 
 parseFormula :: [Token] -> Error (Formula)
 parseFormula toks = case parse parseForm "PARSER" toks of
-  Left err -> Failed $ show err
-  Right formula -> Succeeded formula
+  Left err -> Left $ show err
+  Right formula -> Right formula
 
 parseForm = buildExpressionParser table parseFactor
 
diff --git a/src/Folly/Resolution.hs b/src/Folly/Resolution.hs
--- a/src/Folly/Resolution.hs
+++ b/src/Folly/Resolution.hs
@@ -4,6 +4,7 @@
                         maxClause) where
 
 import Data.List as L
+import Data.Maybe
 import Data.Set as S
 
 import Folly.Clause as C
@@ -11,7 +12,10 @@
 import Folly.Theorem
 
 isValid :: Theorem -> Bool
-isValid t = isValid' maxClause standardSkolem t
+isValid t =
+  case isValid' maxClause standardSkolem t of
+   Just _ -> True
+   Nothing -> False
 
 maxClause cs = S.findMax cs
 
@@ -23,24 +27,29 @@
   
 isValid' :: (Set Clause -> Clause) -> -- Clause selection
             (Theorem -> Set Clause) -> -- Preprocessor
-            Theorem -> Bool
+            Theorem -> Maybe Clause
 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)
+   True -> Nothing
+   False ->
+     case S.member C.empty clauses of
+      True -> S.lookupGE C.empty clauses
+      False -> resolve s (S.singleton (s clauses)) (S.delete (s clauses) clauses)
   where
     clauses = p t
 
-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)
+resolve :: (Set Clause -> Clause) -> Set Clause -> Set Clause -> Maybe Clause
+resolve s axioms cls =
+  case S.member C.empty cls of
+   True -> S.lookupGE C.empty cls
+   False -> case S.size cls == 0 of
+     True -> Nothing
+     False ->
+       let c = s cls
+           newClauses = genNewClauses c axioms
+           nextAxioms = S.insert c axioms
+           nextCls = S.delete c $ S.union newClauses cls in
+        resolve s nextAxioms nextCls
 
 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/Utils.hs b/src/Folly/Utils.hs
--- a/src/Folly/Utils.hs
+++ b/src/Folly/Utils.hs
@@ -1,32 +1,11 @@
 module Folly.Utils(
   Name,
-  Error(..), extractValue) where
+  Error, extractValue) where
 
 type Name = String
 
-data Error a =
-  Succeeded a |
-  Failed String
-  deriving (Show)
-
-instance Applicative Error where
-  pure = Succeeded
-  (Succeeded f) <*> (Succeeded x) = Succeeded (f x)
-  (Failed m) <*> _ = Failed m
-
-instance Functor Error where
-  fmap f (Succeeded a) = Succeeded (f a)
-  fmap _ (Failed m) = Failed m
-
-instance Monad Error where
-  return a = Succeeded a
-  (Succeeded a) >>= f = f a
-  (Failed errMsg) >>= f = (Failed errMsg)
-
-instance Eq a => Eq (Error a) where
-  (==) (Succeeded v1) (Succeeded v2) = v1 == v2
-  (==) _ _ = False
+type Error a = Either String a
 
 extractValue :: Error a -> a
-extractValue (Succeeded val) = val
-extractValue (Failed errMsg) = error $ "Computation Failed: " ++ errMsg
+extractValue (Right val) = val
+extractValue (Left errMsg) = error $ "Computation Failed: " ++ errMsg
diff --git a/src/Main.hs b/src/Main.hs
--- a/src/Main.hs
+++ b/src/Main.hs
@@ -17,8 +17,8 @@
   thmString <- hGetContents fHandle
   let thm = processTheoremFile thmString
   case thm of
-    Failed errMsg -> putStrLn errMsg
-    Succeeded t -> do
+    Left errMsg -> putStrLn errMsg
+    Right t -> do
       putStr $ show t
       case isValid t of
         True -> putStrLn "\n\nIs Valid"
diff --git a/test/Folly/LexerTests.hs b/test/Folly/LexerTests.hs
--- a/test/Folly/LexerTests.hs
+++ b/test/Folly/LexerTests.hs
@@ -8,23 +8,23 @@
   testFunction lexer lexerCases
 
 lexerCases =
-  [("nooo", Succeeded $ [testVar "nooo"]),
-   ("(", Succeeded $ [testSep "("]),
-   (")", Succeeded $ [testSep ")"]),
-   ("[", Succeeded $ [testSep "["]),
-   ("]", Succeeded $ [testSep "]"]),
-   (",", Succeeded $ [testSep ","]),
-   (".", Succeeded $ [testSep "."]),
-   ("|", Succeeded $ [testOp "|"]),
-   ("&", Succeeded $ [testOp "&"]),
-   ("~", Succeeded $ [testOp "~"]),
-   ("->", Succeeded $ [testOp "->"]),
-   ("<->", Succeeded $ [testOp "<->"]),
-   ("E", Succeeded $ [testQuant "E"]),
-   ("Q", Succeeded $ [testQuant "Q"]),
-   ("=", Succeeded $ [testPred "="]),
-   ("Ever", Succeeded $ [testPred "Ever"]),
-   ("Quacks", Succeeded $ [testPred "Quacks"]),
-   ("N#%_Man", Succeeded $ [testPred "N#%_Man"]),
-   ("n#2@", Succeeded $ [testVar "n#2@"]),
-   ("V z . E k. F[z] -> G[k]", Succeeded $ [testPred "V", testVar "z", testSep ".", testPred "E", testVar "k", testSep ".", testPred "F", testSep "[", testVar "z", testSep "]", testOp "->", testPred "G", testSep "[", testVar "k", testSep "]"])]
+  [("nooo", Right $ [testVar "nooo"]),
+   ("(", Right $ [testSep "("]),
+   (")", Right $ [testSep ")"]),
+   ("[", Right $ [testSep "["]),
+   ("]", Right $ [testSep "]"]),
+   (",", Right $ [testSep ","]),
+   (".", Right $ [testSep "."]),
+   ("|", Right $ [testOp "|"]),
+   ("&", Right $ [testOp "&"]),
+   ("~", Right $ [testOp "~"]),
+   ("->", Right $ [testOp "->"]),
+   ("<->", Right $ [testOp "<->"]),
+   ("E", Right $ [testQuant "E"]),
+   ("Q", Right $ [testQuant "Q"]),
+   ("=", Right $ [testPred "="]),
+   ("Ever", Right $ [testPred "Ever"]),
+   ("Quacks", Right $ [testPred "Quacks"]),
+   ("N#%_Man", Right $ [testPred "N#%_Man"]),
+   ("n#2@", Right $ [testVar "n#2@"]),
+   ("V z . E k. F[z] -> G[k]", Right $ [testPred "V", testVar "z", testSep ".", testPred "E", testVar "k", testSep ".", testPred "F", testSep "[", testVar "z", testSep "]", testOp "->", testPred "G", testSep "[", testVar "k", testSep "]"])]
diff --git a/test/Folly/ParserTests.hs b/test/Folly/ParserTests.hs
--- a/test/Folly/ParserTests.hs
+++ b/test/Folly/ParserTests.hs
@@ -11,15 +11,15 @@
 
 parseFormulaCases :: [(String, Error Formula)]
 parseFormulaCases =
-  [("Dog[ a ]", Succeeded $ pr "Dog" [var "a"]),
-   ("~Super[ k, kill(a, b)]", Succeeded $ neg (pr "Super" [var "k", func "kill" [var "a", var "b"]])),
-   ("Dog[x] & Owns[John, x]", Succeeded $ con (pr "Dog" [var "x"]) (pr "Owns" [constant "John", var "x"])),
-   ("Dog [x] & (Owns[John, x] | Not[Cat, John])", Succeeded $ con (pr "Dog" [var "x"]) (dis (pr "Owns" [constant "John", var "x"]) (pr "Not" [constant "Cat", constant "John"]))),
-   ("Ex[p] | ~Ex[x]", Succeeded $ dis (pr "Ex" [var "p"]) (neg (pr "Ex" [var "x"]))),
-   ("Ex[p] -> ~Ex[x]", Succeeded $ imp (pr "Ex" [var "p"]) (neg (pr "Ex" [var "x"]))),
-   ("Ex[p] <-> ~Vx[x]", Succeeded $ bic (pr "Ex" [var "p"]) (neg (pr "Vx" [var "x"]))),
-   ("V x . U#12[x]", Succeeded $ fa (var "x") (pr "U#12" [var "x"])),
-   ("E y . K[f(l, y, No)]", Succeeded $ te (var "y") (pr "K" [func "f" [var "l", var "y", constant "No"]])),
-   ("V z . E k. F[z] -> G[k]", Succeeded $ fa (var "z") (te (var "k") (imp (pr "F" [var "z"]) (pr "G" [var "k"])))),
-   ("E y. K[y] -> V x. Z[x, y]", Succeeded $ te (var "y") (imp (pr "K" [var "y"]) (fa (var "x") (pr "Z" [var "x", var "y"])))),
-   ("E y. K[y] -> Z[x, y]", Succeeded $ te (var "y") (imp (pr "K" [var "y"]) (pr "Z" [var "x", var "y"])))]
+  [("Dog[ a ]", Right $ pr "Dog" [var "a"]),
+   ("~Super[ k, kill(a, b)]", Right $ neg (pr "Super" [var "k", func "kill" [var "a", var "b"]])),
+   ("Dog[x] & Owns[John, x]", Right $ con (pr "Dog" [var "x"]) (pr "Owns" [constant "John", var "x"])),
+   ("Dog [x] & (Owns[John, x] | Not[Cat, John])", Right $ con (pr "Dog" [var "x"]) (dis (pr "Owns" [constant "John", var "x"]) (pr "Not" [constant "Cat", constant "John"]))),
+   ("Ex[p] | ~Ex[x]", Right $ dis (pr "Ex" [var "p"]) (neg (pr "Ex" [var "x"]))),
+   ("Ex[p] -> ~Ex[x]", Right $ imp (pr "Ex" [var "p"]) (neg (pr "Ex" [var "x"]))),
+   ("Ex[p] <-> ~Vx[x]", Right $ bic (pr "Ex" [var "p"]) (neg (pr "Vx" [var "x"]))),
+   ("V x . U#12[x]", Right $ fa (var "x") (pr "U#12" [var "x"])),
+   ("E y . K[f(l, y, No)]", Right $ te (var "y") (pr "K" [func "f" [var "l", var "y", constant "No"]])),
+   ("V z . E k. F[z] -> G[k]", Right $ fa (var "z") (te (var "k") (imp (pr "F" [var "z"]) (pr "G" [var "k"])))),
+   ("E y. K[y] -> V x. Z[x, y]", Right $ te (var "y") (imp (pr "K" [var "y"]) (fa (var "x") (pr "Z" [var "x", var "y"])))),
+   ("E y. K[y] -> Z[x, y]", Right $ te (var "y") (imp (pr "K" [var "y"]) (pr "Z" [var "x", var "y"])))]