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.3.0
+version:             0.1.4.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
@@ -10,7 +10,6 @@
   applyToTerms,
   literalArgs,
   toPNF, toSkolemForm, skf,
-  Clause,
   toClausalForm,
   isTautology,
   matchingLiterals) where
@@ -86,7 +85,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 ++ ")"
@@ -274,15 +273,13 @@
 skf n vars = Func ("skl" ++ show n) vars
 
 -- Conversion to clausal form
-type Clause = [Formula]
-
-toClausalForm :: Formula -> [Clause]
+toClausalForm :: Formula -> [[Formula]]
 toClausalForm = splitClauses . removeUniversals . distributeDisjunction . toSkolemForm
 
-distributeDisjunction :: Formula -> Formula
+distributeDisjunction :: (Formula) -> (Formula)
 distributeDisjunction f = transformFormula distrDis f
 
-distrDis :: Formula -> Formula
+distrDis :: (Formula) -> (Formula)
 distrDis (B "|" (B "&" l r) f) = (B "&" (B "|" l f) (B "|" r f))
 distrDis (B "|" f (B "&" l r)) = (B "&" (B "|" f l) (B "|" f r))
 distrDis f = f
@@ -291,15 +288,15 @@
 removeUniversals (Q "V" v f) = removeUniversals f
 removeUniversals f = f
 
-splitClauses :: Formula -> [Clause]
+splitClauses :: Formula -> [[Formula]]
 splitClauses (B "&" l r) = (splitClauses l) ++ (splitClauses r)
 splitClauses f = [splitDis f]
 
-splitDis :: Formula -> Clause
+splitDis :: Formula -> [Formula]
 splitDis (B "|" l r) = (splitDis l) ++ (splitDis r)
 splitDis f = [f]
 
-isTautology :: Clause -> Bool
+isTautology :: [Formula] -> Bool
 isTautology c = L.length (L.intersect atoms negAtoms) > 0
   where
     atoms = L.filter isAtom c
diff --git a/src/Folly/Resolution.hs b/src/Folly/Resolution.hs
--- a/src/Folly/Resolution.hs
+++ b/src/Folly/Resolution.hs
@@ -16,12 +16,12 @@
     clauses = uniqueVarNames $ L.concat $ L.map toClausalForm formulas
     clauseSet = S.fromList clauses
 
-resolve :: Set Clause -> Bool
+resolve :: Set [Formula] -> Bool
 resolve cls = case S.member [] cls of
   True -> True
   False -> resolveIter [cls]
 
-resolveIter :: [Set Clause] -> Bool
+resolveIter :: [Set [Formula]] -> Bool
 resolveIter [] = error "Empty list of clause sets"
 resolveIter clauseSets = case S.size newClauses == 0 of
   True -> True
@@ -33,37 +33,37 @@
       1 -> generateNewClauses (head clauseSets) (head clauseSets)
       _ -> generateNewClauses (head clauseSets) (L.foldl S.union S.empty (tail clauseSets))
 
-generateNewClauses :: Set Clause -> Set Clause -> Set Clause
+generateNewClauses :: Set [Formula] -> Set [Formula] -> Set [Formula]
 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
 
-resolvedClauses :: Clause -> Clause -> Set Clause
+resolvedClauses :: [Formula] -> [Formula] -> Set [Formula]
 resolvedClauses left right = S.fromList resClauses
   where
     mResClauses = L.map (\ x -> (L.map (\ y -> tryToResolve x left y right) right)) left
     resClauses = L.map fromJust $ L.filter (/= Nothing) $ L.concat mResClauses 
 
-tryToResolve :: Formula -> Clause -> Formula -> Clause -> Maybe Clause
+tryToResolve :: Formula -> [Formula] -> Formula -> [Formula] -> Maybe [Formula]
 tryToResolve leftLiteral leftClause rightLiteral rightClause =
   case matchingLiterals leftLiteral rightLiteral of
     True -> unifiedResolvedClause leftLiteral leftClause rightLiteral rightClause
     False -> Nothing
 
-unifiedResolvedClause :: Formula -> Clause -> Formula -> Clause -> Maybe Clause
+unifiedResolvedClause :: Formula -> [Formula] -> Formula -> [Formula] -> Maybe [Formula]
 unifiedResolvedClause lLit lc rLit rc = case mostGeneralUnifier $ zip (literalArgs lLit) (literalArgs rLit) of
   Just mgu -> Just $ L.map (\ lit -> applyToTerms lit (applyUnifier mgu)) ((L.delete lLit lc) ++ (L.delete rLit rc))
   Nothing -> Nothing
 
-uniqueVarNames :: [Clause] -> [Clause]
+uniqueVarNames :: [[Formula]] -> [[Formula]]
 uniqueVarNames cls = zipWith attachSuffix cls (L.map show [1..length cls])
 
-attachSuffix :: Clause -> String -> Clause
+attachSuffix :: [Formula] -> String -> [Formula]
 attachSuffix cls suffix = L.map (addSuffixToVarNames suffix) cls
 
 addSuffixToVarNames :: String -> Formula -> Formula
 addSuffixToVarNames suffix form = applyToTerms form (appendVarName suffix)
 
-deleteTautologies :: Set Clause -> Set Clause
+deleteTautologies :: Set [Formula] -> Set [Formula]
 deleteTautologies clauses = S.filter (not . isTautology) clauses
diff --git a/src/Folly/Utils.hs b/src/Folly/Utils.hs
--- a/src/Folly/Utils.hs
+++ b/src/Folly/Utils.hs
@@ -9,6 +9,15 @@
   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