diff --git a/app/FOLSyntax.hs b/app/FOLSyntax.hs
index 111f69a..88b5861 100644
--- a/app/FOLSyntax.hs
+++ b/app/FOLSyntax.hs
@@ -1,5 +1,8 @@
 module FOLSyntax where
 
+import Data.List ( find )
+import Data.Maybe ( fromJust )
+
 data Term = Var String | Fun String [Term] deriving (Eq, Ord)
 data Formula
     = Pred String [Term]
@@ -29,4 +32,33 @@ instance Show Formula where
     show (All x f) = "(forall " ++ x ++ ". " ++ show f ++ ")"
     show (Exists x f) = "(exists " ++ x ++ ". " ++ show f ++ ")"
     show T = "true"
-    show F = "false"
\ No newline at end of file
+    show F = "false"
+
+-- infinite list of variable names
+vars :: [String]
+vars = ['v' : show n | n <- [(0 :: Int)..]]
+
+-- finds a fresh variable i.e. a variable not occuring in vs
+findFresh :: [String] -> String
+findFresh vs = fromJust $ find (`notElem` vs) vars
+
+-- free variables of a term
+termFreeVars :: Term -> [String]
+termFreeVars (Var x) = [x]
+termFreeVars (Fun _ ts) = concatMap termFreeVars ts
+
+-- substitution on terms
+termSubst :: Term -> String -> Term -> Term
+termSubst t@(Var x) y s = if x == y then s else t
+termSubst (Fun f ts) y s = Fun f $ map (\t' -> termSubst t' y s) ts
+
+-- return *all* vars in a formula, i.e. bound ones and free ones
+formulaVars :: Formula -> [String]
+formulaVars (Pred _ ts) = concatMap termFreeVars ts
+formulaVars (Neg f) = formulaVars f
+formulaVars (Conj f1 f2) = formulaVars f1 ++ formulaVars f2
+formulaVars (Disj f1 f2) = formulaVars f1 ++ formulaVars f2
+formulaVars (Impl f1 f2) = formulaVars f1 ++ formulaVars f2
+formulaVars (All x f) = x : formulaVars f
+formulaVars (Exists x f) = x : formulaVars f
+formulaVars _ = []
\ No newline at end of file
diff --git a/app/Lexer.hs b/app/Lexer.hs
index 2184d43..bfc6e52 100644
--- a/app/Lexer.hs
+++ b/app/Lexer.hs
@@ -1,11 +1,9 @@
-{-# LANGUAGE ImportQualifiedPost #-}
-
 module Lexer where
 
 import Text.Parsec.Char (alphaNum, letter, oneOf)
 import Text.Parsec.Language (emptyDef)
 import Text.Parsec.String (Parser)
-import Text.Parsec.Token qualified as Tok
+import qualified Text.Parsec.Token as Tok
 
 lexer :: Tok.TokenParser ()
 lexer = Tok.makeTokenParser style
diff --git a/app/Main.hs b/app/Main.hs
index b1aa46f..f9258fb 100644
--- a/app/Main.hs
+++ b/app/Main.hs
@@ -1,287 +1,15 @@
 module Main where
 
-import Data.List
-import Data.Maybe
-import qualified Data.Set as Set
-import FOLSyntax
-import Parser
-
-fromRight :: Either a b -> b
-fromRight (Left _) = error "fromRight called on left value!"
-fromRight (Right b) = b
-
--- free variables of a term
-termFreeVars :: Term -> [String]
-termFreeVars (Var x) = [x]
-termFreeVars (Fun _ ts) = concatMap termFreeVars ts
-
--- substitution on terms
-termSubst :: Term -> String -> Term -> Term
-termSubst t@(Var x) y s = if x == y then s else t
-termSubst (Fun f ts) y s = Fun f $ map (\t' -> termSubst t' y s) ts
-
--- unification algorithm of martelli montanari
-unify :: [(Term, Term)] -> Maybe [(Term, Term)]
-unify [] = Just []
--- (delete)
-unify ((Var x, Var y) : rest) | x == y = unify rest
--- (decomp)
-unify ((Fun f es, Fun g ds) : rest) | f == g && length es == length ds = unify $ zip es ds ++ rest
--- (conflict)
-unify ((Fun _ _, Fun _ _) : _) = Nothing
--- (orient)
-unify ((Fun f ts, Var x) : rest) = unify $ (Var x, Fun f ts) : rest
--- (occurs)
-unify ((Var x, t) : _) | x `elem` termFreeVars t && Var x /= t = Nothing
--- (elim)
-unify ((Var x, t) : rest) | notElem x (termFreeVars t) && x `elem` concatMap (\(t1, t2) -> termFreeVars t1 ++ termFreeVars t2) rest = unify $ (Var x, t) : map (\(t1, t2) -> (termSubst t1 x t, termSubst t2 x t)) rest
--- decent
-unify ((t, s) : rest) = do
-    rest' <- unify rest
-    return $ (t, s) : rest'
-
-{-
-Now we define some functions to convert given terms to normalforms
-i.e. negation normalform, prenex normal, skolemform, conjunctive normalform
--}
-
--- negation normalform
-makeNNF :: Formula -> Formula
-makeNNF form = if form == f' then form else makeNNF f'
-    where
-        f' = nnfStep form
-        nnfStep (Conj f1 f2) = Conj (nnfStep f1) (nnfStep f2)
-        nnfStep (Disj f1 f2) = Disj (nnfStep f1) (nnfStep f2)
-        nnfStep (Impl f1 f2) = Disj (Neg f1) f2
-        nnfStep (All x f) = All x (nnfStep f)
-        nnfStep (Exists x f) = Exists x (nnfStep f)
-        nnfStep (Neg (Conj f1 f2)) = Disj (Neg f1) (Neg f2)
-        nnfStep (Neg (Disj f1 f2)) = Conj (Neg f1) (Neg f2)
-        nnfStep (Neg (Impl f1 f2)) = Conj f1 (Neg f2)
-        nnfStep (Neg (All x f)) = Exists x (Neg f)
-        nnfStep (Neg (Exists x f)) = All x (Neg f)
-        nnfStep (Neg (Neg f)) = f
-        nnfStep (Neg T) = F
-        nnfStep (Neg F) = T
-        nnfStep f = f
-
--- infinite list of variable names
-vars :: [String]
-vars = ['v' : show n | n <- [(0 :: Int)..]]
-
--- return *all* vars in a formula, i.e. bound ones and free ones
-formulaVars :: Formula -> [String]
-formulaVars (Pred _ ts) = concatMap termFreeVars ts
-formulaVars (Neg f) = formulaVars f
-formulaVars (Conj f1 f2) = formulaVars f1 ++ formulaVars f2
-formulaVars (Disj f1 f2) = formulaVars f1 ++ formulaVars f2
-formulaVars (Impl f1 f2) = formulaVars f1 ++ formulaVars f2
-formulaVars (All x f) = x : formulaVars f
-formulaVars (Exists x f) = x : formulaVars f
-formulaVars _ = []
-
--- renames all occurences of variable v with v' in a term
-renameTerm :: Term -> String -> String -> Term
-renameTerm t@(Var x) v v' = if x == v then Var v' else t
-renameTerm (Fun g ts) v v' = Fun g (map (\t -> renameTerm t v v') ts)
-
--- renames all occurences of free variable v with v' in a formula
-renameFormula :: Formula -> String -> String -> Formula
-renameFormula (Pred p ts) v v' = Pred p (map (\t -> renameTerm t v v') ts)
-renameFormula (Neg f') v v' = Neg $ renameFormula f' v v'
-renameFormula (Conj f1 f2) v v' = Conj (renameFormula f1 v v') (renameFormula f2 v v')
-renameFormula (Disj f1 f2) v v' = Disj (renameFormula f1 v v') (renameFormula f2 v v')
-renameFormula (Impl f1 f2) v v' = Impl (renameFormula f1 v v') (renameFormula f2 v v')
-renameFormula (All y f') v v' | y /= v = All y $ renameFormula f' v v'
-renameFormula (Exists y f') v v' | y /= v = Exists y $ renameFormula f' v v'
-renameFormula f' _ _ = f'
-
--- finds a fresh variable i.e. a variable not occuring in vs
-findFresh :: [String] -> String
-findFresh vs = fromJust $ find (`notElem` vs) vars
-
--- rename every binder in formula to be disjunct
-renameBinders :: Formula -> Formula
-renameBinders f = fst $ go f []
-    where
-        go :: Formula -> [String] -> (Formula, [String])
-        go (All x f') vs = (All x' f'', vs')
-            where
-                (f'', vs') = go (renameFormula f' x x') (x' : vs)
-                x' = findFresh (formulaVars f ++ vs)
-        go (Exists x f') vs = (Exists x' f'', vs')
-            where
-                (f'', vs') = go (renameFormula f' x x') (x' : vs)
-                x' = findFresh (formulaVars f ++ vs)
-        go (Neg f') vs = (Neg f'', vs')
-            where
-                (f'', vs') = go f' vs
-        go (Conj f1 f2) vs = (Conj f1' f2', vs'')
-            where
-                (f1', vs') = go f1 vs
-                (f2', vs'') = go f2 vs'
-        go (Disj f1 f2) vs = (Disj f1' f2', vs'')
-            where
-                (f1', vs') = go f1 vs
-                (f2', vs'') = go f2 vs'
-        go (Impl f1 f2) vs = (Impl f1' f2', vs'')
-            where
-                (f1', vs') = go f1 vs
-                (f2', vs'') = go f2 vs'
-        go f' vs = (f', vs)
-
--- prenex normalform
--- TODO make it so that forall has higher priority to be moved left (makes skolem functions smaller)
-makePNF :: Formula -> Formula
-makePNF form = go form
-    where
-        go f = let f' = pnfStep f in
-            if f == f' then f else go f'
-        -- swapping rules
-        pnfStep (Conj phi (Exists x psi)) = Exists x (Conj phi psi)
-        pnfStep (Disj phi (Exists x psi)) = Exists x (Disj phi psi)
-        pnfStep (Conj (Exists x psi) phi) = Exists x (Conj psi phi)
-        pnfStep (Disj (Exists x psi) phi) = Exists x (Disj psi phi)
-        pnfStep (Conj phi (All x psi)) = All x (Conj phi psi)
-        pnfStep (Disj phi (All x psi)) = All x (Disj phi psi)
-        pnfStep (Conj (All x psi) phi) = All x (Conj psi phi)
-        pnfStep (Disj (All x psi) phi) = All x (Disj psi phi)
-        {-
-        pnfStep (Conj phi (Exists x psi)) = Exists x (Conj phi psi)
-        pnfStep (Conj phi (All x psi)) = All x (Conj phi psi)
-        pnfStep (Disj phi (Exists x psi)) = Exists x (Disj phi psi)
-        pnfStep (Disj phi (All x psi)) = All x (Disj phi psi)
-        pnfStep (Conj (Exists x psi) phi) = Exists x (Conj psi phi)
-        pnfStep (Conj (All x psi) phi) = All x (Conj psi phi)
-        pnfStep (Disj (Exists x psi) phi) = Exists x (Disj psi phi)
-        pnfStep (Disj (All x psi) phi) = All x (Disj psi phi)
-        -}
-        -- descent rules
-        pnfStep (All x f) = All x (pnfStep f)
-        pnfStep (Exists x f) = Exists x (pnfStep f)
-        pnfStep (Conj f1 f2) = Conj (pnfStep f1) (pnfStep f2)
-        pnfStep (Disj f1 f2) = Disj (pnfStep f1) (pnfStep f2)
-        pnfStep (Impl f1 f2) = Impl (pnfStep f1) (pnfStep f2) -- can't happen, gets removed in makeNNF
-        pnfStep (Neg f) = Neg (pnfStep f)
-        pnfStep f = f
-
--- infinite function names for skolemizing
-skolemFuns :: [String]
-skolemFuns = ["sk" ++ show n | n <- [(0 :: Int)..]]
-
--- returns all function names in a formula
-usedFunctions :: Formula -> [String]
-usedFunctions (Pred _ ts) = concatMap termFunctions ts
-    where
-        termFunctions (Var _) = []
-        termFunctions (Fun f ts') = f : concatMap termFunctions ts'
-usedFunctions (Neg f) = usedFunctions f
-usedFunctions (Conj f1 f2) = usedFunctions f1 ++ usedFunctions f2
-usedFunctions (Disj f1 f2) = usedFunctions f1 ++ usedFunctions f2
-usedFunctions (Impl f1 f2) = usedFunctions f1 ++ usedFunctions f2
-usedFunctions (All _ f) = usedFunctions f
-usedFunctions (Exists _ f) = usedFunctions f
-usedFunctions _ = []
-
--- skolem form of a formula
-makeSkolem :: Formula -> Formula
-makeSkolem form = go form [] []
-    where
-        substTermInFormula :: Formula -> String -> Term -> Formula
-        substTermInFormula (Pred p ts) x s = Pred p $ map (\t -> termSubst t x s) ts
-        substTermInFormula (Neg f) x s = Neg $ substTermInFormula f x s
-        substTermInFormula (Conj f1 f2) x s = Conj (substTermInFormula f1 x s) (substTermInFormula f2 x s)
-        substTermInFormula (Disj f1 f2) x s = Disj (substTermInFormula f1 x s) (substTermInFormula f2 x s)
-        substTermInFormula (Impl f1 f2) x s = Impl (substTermInFormula f1 x s) (substTermInFormula f2 x s)
-        substTermInFormula f@(All y f') x s = if x == y then f else All y (substTermInFormula f' x s)
-        substTermInFormula f@(Exists y f') x s = if x == y then f else Exists y (substTermInFormula f' x s)
-        substTermInFormula f _ _ = f
-        go (All x f) vs skolems = All x (go f (vs ++ [Var x]) skolems)
-        go (Exists x f) vs skolems = go (substTermInFormula f x (Fun newSkolem vs)) vs (newSkolem : skolems)
-            where newSkolem = fromJust $ find (`notElem` skolems) skolemFuns
-        go f _ _ = f
-
--- conjunctive normalform, removes all quantors, so its ready for resolution
-makeCNF :: Formula -> Formula
-makeCNF form = go form
-    where
-        go f = let f' = cnfStep f in
-            if f == f' then f else go f'
-        cnfStep (Conj phi psi) = Conj (cnfStep phi) (cnfStep psi)
-        cnfStep (Disj (Conj phi psi) xi) = Conj (Disj phi xi) (Disj psi xi)
-        cnfStep (Disj xi (Conj phi psi)) = Conj (Disj xi phi) (Disj xi psi)
-        cnfStep (All _ f) = cnfStep f
-        cnfStep (Exists _ f) = cnfStep f
-        cnfStep f = f
-
--- create the list of clauses from a formula
--- TODO not working correctly for `makeCNFList formula5`
-makeCNFList :: Formula -> [[Formula]]
-makeCNFList form = go form
-    where
-        go (Conj f1 f2) = go f1 ++ go f2
-        go (Disj f1 f2) = [collectDisjs f1 ++ collectDisjs f2]
-            where
-                collectDisjs (Disj f1' f2') = collectDisjs f1' ++ collectDisjs f2'
-                collectDisjs f' = [f']
-        go f = [[f]]
-
--- unifies predicates, e.g. P(x,y) == P(f(a), z)
-unifyPredicates :: (Formula, [Formula]) -> (Formula, [Formula]) -> Maybe (([Formula], [Formula]), [(Term, Term)])
-unifyPredicates (e1@(Pred p1 ts1), c1) (e2@(Neg (Pred p2 ts2)), c2) | p1 == p2 && length p1 == length p2 = do
-        mgu <- unify $ zip ts1 ts2
-        return ((c1', c2'), mgu)
-    where
-        c1' = filter (/= e1) c1
-        c2' = filter (/= e2) c2
-unifyPredicates _ _ = Nothing
-
--- applies an mgu to a given formula, asserts that the formula contains no quantifiers
-applyMgu :: Formula -> [(Term, Term)] -> Formula
-applyMgu (Pred p ts) mgu = Pred p $ map (`applyMguTerm` mgu) ts
-applyMgu (Neg f) mgu = Neg $ applyMgu f mgu
-applyMgu (Conj f1 f2) mgu = Conj (applyMgu f1 mgu) (applyMgu f2 mgu)
-applyMgu (Disj f1 f2) mgu = Disj (applyMgu f1 mgu) (applyMgu f2 mgu)
-applyMgu (Impl f1 f2) mgu = Impl (applyMgu f1 mgu) (applyMgu f2 mgu)
-applyMgu f _ = f
--- applies mgu to term
-applyMguTerm :: Term -> [(Term, Term)] -> Term
-applyMguTerm (Var x) [] = Var x
-applyMguTerm (Var x) ((Var y, t) : rest) = if x == y then t else applyMguTerm (Var x) rest
-applyMguTerm (Fun f ts) mgu = Fun f $ map (`applyMguTerm` mgu) ts
-applyMguTerm t _ = t
-
--- replace every fresh variable in a formula with a new name, this is only correct in our resolution context!!
-makeVariablesDisjunct :: [[Formula]] -> [[Formula]]
-makeVariablesDisjunct form = snd $ foldr (\clause (used', clauses') -> let (used'', clause') = makeClauseDisjunct used' clause in (used'', clause' : clauses')) ([], []) form
-makeClauseDisjunct :: [String] -> [Formula] -> ([String], [Formula])
-makeClauseDisjunct used clause = (concatMap formulaVars newClause ++ newUsed, newClause)
-    where
-        criticalVars = used `intersect` concatMap formulaVars clause
-        (newUsed, newClause) = foldr foldFun (used, clause) criticalVars
-            where
-                foldFun oldVar (used', clause') = (v' : used', map (\f -> renameFormula f oldVar v') clause') 
-                    where
-                        v' = findFresh used'
-
--- a single resolution step as described in gloin
--- TODO before each step, rename every clause so that variable names are disjunct!
-rifStep :: [[Formula]] -> Either () [[Formula]]
-rifStep clauses = if [] `elem` clauses then Left () else Right newClauses
-    where
-        -- rename all variables
-        clauses' = makeVariablesDisjunct clauses
-        resolveClauses :: [Formula] -> [Formula] -> [(([Formula], [Formula]), [(Term, Term)])]
-        resolveClauses c1 c2 = let zippedElems = [((e1, c1), (e2, c2)) | e1 <- c1, e2 <- c2] in mapMaybe (uncurry unifyPredicates) zippedElems
-        zippedClauses = [(c1, c2) | c1 <- clauses', c2 <- clauses', c1 /= c2]
-        clausesWithMgus = concatMap (uncurry resolveClauses) zippedClauses
-        newClauses = Set.toList . Set.fromList $ clauses' ++ map (\((f1, f2), mgu) -> map (`applyMgu` mgu) f1 ++ map (`applyMgu` mgu) f2) clausesWithMgus
-
--- do resolution until we have proven unfulfillability of formula set
-doResolution :: [[Formula]] -> Either () [[Formula]]
-doResolution f = do
-    f' <- rifStep f
-    doResolution f'
+import FOLSyntax ( Formula(Conj, Neg, Impl), Term(..) )
+import Parser ( parseFormula )
+import Resolution ( CNF, doResolution )
+import Normalforms
+    ( makeNNF,
+      renameBinders,
+      makePNF,
+      makeSkolem,
+      makeCNF,
+      makeClauseSet )
 
 {-
 To prove a formula we:
@@ -289,35 +17,8 @@ To prove a formula we:
 2. Transform `Neg phi` to a clause list
 3. doResolution on clause list
 -}
-proveFormula :: Formula -> Either () [[Formula]]
-proveFormula form = doResolution . makeCNFList . makeCNF . makeSkolem . makePNF . renameBinders . makeNNF $ Neg form
-
-proveFormulaIO :: Formula -> IO ()
-proveFormulaIO f = do
-    let f' = makeNNF (Neg f)
-    print f'
-    putStrLn ""
-    let f'' = renameBinders f'
-    print f''
-    putStrLn ""
-
-    let f''' = makePNF f''
-    print f'''
-    putStrLn ""
-
-    let f'''' = makeSkolem f'''
-    print f''''
-    putStrLn ""
-
-    let g = makeCNF f''''
-    print g
-    putStrLn ""
-
-    let g' = makeCNFList g
-    print g'
-    case doResolution g' of
-        Left _ -> putStrLn "Success!!"
-        _ -> return ()
+proveFormula :: Formula -> Either () CNF
+proveFormula form = doResolution . makeClauseSet . makeCNF . makeSkolem . makePNF . renameBinders . makeNNF $ Neg form
 
 -- unification examples
 terma1 :: Term
@@ -335,98 +36,58 @@ termb3 = Fun "f" [Var "z", Var "z"]
 
 -- NNF example from gloin
 formula1 :: Formula
-formula1 = Neg (Conj (Disj (Pred "A" []) (Neg $ Pred "B" [])) (Pred "C" []))
+formula1 = parseFormula "!((A () \\/ !B()) /\\ (C ()))"
 
 -- PNF and skolem example from gloin
-formula2 :: String
-formula2 = "forall x. (forall y. L(y,x)) -> exists y.M(x,y)"
+formula2 :: Formula
+formula2 = parseFormula "forall x. (forall y. L(y,x)) -> exists y.M(x,y)"
 
 -- Resolution example from gloin script
 formula3 :: Formula
-formula3 = Impl (Conj (Pred "P" [Fun "a" []]) (All "x" $ Impl (Pred "P" [Var "x"]) (Pred "P" [Fun "f" [Var "x"]]))) (Exists "x" $ Pred "P" [Fun "f" [Fun "f" [Var "x"]]])
+formula3 = parseFormula "P(a()) /\\ (forall x. P(x) -> P(f(x))) -> (exists x. P(f(f(x)))) "
 
--- Resolution example from gloin exercises (already in cnf)
+-- Resolution example from gloin exercises (sheet 11, ex 5) [already in CNF]
 formula4 :: Formula
-formula4 = Conj (Disj (Pred "P" [Fun "f" [Var "x"], Var "y"]) (Disj (Pred "S" [Var "y", Var "z"]) (Pred "P" [Var "y"]))) (Conj (Neg $ Pred "S" [Fun "f" [Fun "f" [Var "x"]], Var "x"]) (Neg $ Pred "P" [Fun "f" [Var "z"]]))
+formula4 = parseFormula "((S(f(x), y)) \\/ (S(y, z)) \\/ (P(y))) /\\ (!(S(f(f(x)), x))) /\\ (!P(f(z)))"
 
 -- now a big example, sheet 11, exercise 6: Drogenschmuggel, this doesn't work yet but I'm sure its just the exercise thats wrong...
-phi1 :: Formula
-phi1 = All "x" $ Impl (Conj (Pred "E" [Var "x"]) (Neg $ Pred "I" [Var "x"])) (Exists "y" $ Conj (Pred "Z" [Var "y"]) (Pred "S" [Var "y", Var "x"]))
-phi2 :: Formula
-phi2 = Exists "x" $ Conj (Conj (Pred "D" [Var "x"]) (Pred "E" [Var "x"])) (All "y" $ Impl (Pred "S" [Var "y", Var "x"]) (Pred "D" [Var "y"]))
-phi3 :: Formula
-phi3 = All "x" $ Impl (Pred "I" [Var "x"]) (Neg $ Pred "D" [Var "x"])
-psi' :: Formula
-psi' = Exists "x" $ Conj (Pred "Z" [Var "x"]) (Pred "D" [Var "x"])
-
 formula5 :: Formula
-formula5 = Impl (Conj (Conj phi1 phi2) phi3) psi'
-
--- exercise 2: Ärzte und Quacksalber
-formula6 :: [[Formula]]
-formula6 = [
-    [Neg $ Pred "D" [Var "x1"], Pred "L" [Fun "f" [Var "x1"], Var "x1"]],
-    [Pred "P" [Fun "f" [Var "x2"]], Neg $ Pred "L" [Fun "f" [Var "x2"], Var "x2"]],
-    [Neg $ Pred "P" [Var "x3"], Neg $ Pred "Q" [Var "y3"], Neg $ Pred "L" [Var "x3", Var "y3"]],
-    [Pred "D" [Fun "a" []]],
-    [Pred "Q" [Fun "a" []]]]
-
--- Drogenschmuggel but already as clauses, fifth clause is wrong, arguments to S need to be swapped!!
-formula7 :: [[Formula]]
-formula7 = [
-    [Neg $ Pred "E" [Var "x2"], Pred "I" [Var "x2"], Pred "Z" [Fun "f" [Var "x2"]]],
-    [Neg $ Pred "E" [Var "x3"], Pred "I" [Var "x3"], Pred "S" [Var "x3", Fun "f" [Var "x3"]]],
-    [Pred "D" [Fun "c" []]],
-    [Pred "E" [Fun "c" []]],
-    [Neg $ Pred "S" [Fun "c" [], Var "y"], Pred "D" [Var "y"]],
-    [Neg $ Pred "I" [Var "x4"], Neg $ Pred "D" [Var "x4"]],
-    [Neg $ Pred "Z" [Var "x5"], Neg $ Pred "D" [Var "x5"]]
-    ]
-
-formula8 :: [[Formula]]
-formula8 = [
-    [Neg $ Pred "E" [Var "x2"], Pred "I" [Var "x2"], Pred "Z" [Fun "f" [Var "x21", Var "x22", Var "x2"]]],
-    [Neg $ Pred "E" [Var "x3"], Pred "I" [Var "x3"], Pred "S" [Var "x3", Fun "f" [Var "x31", Var "x32", Var "x3"]]],
-    [Pred "D" [Fun "c" [Var "x5", Var "x4"]]],
-    [Pred "E" [Fun "c" [Var "x5'", Var "x4'"]]],
-    [Neg $ Pred "S" [Fun "c" [Var "x5''", Var "x4''"], Var "y"], Pred "D" [Var "y"]],
-    [Neg $ Pred "I" [Var "x44"], Neg $ Pred "D" [Var "x44"]],
-    [Neg $ Pred "Z" [Var "x55"], Neg $ Pred "D" [Var "x55"]]
-    ]
+formula5 = Impl (Conj phi1 (Conj phi2 phi3)) psi
+    where
+        phi1 = parseFormula "forall x.E(x) /\\ !I(x) -> exists y.Z(y) /\\ S(y,x)"
+        phi2 = parseFormula "exists x. (D(x) /\\ E(x)) /\\ forall y. S(y,x) -> D(y)"
+        phi3 = parseFormula "forall x.I(x) -> !D(x)"
+        psi = parseFormula "exists x. Z(x) /\\ D(x)"
 
 -- aerzte und quacksalber v2
-formula9 :: Formula 
-formula9 = Impl (Conj psi1 psi2) psi3
+formula6 :: Formula
+formula6 = Impl (Conj psi1 psi2) psi3
     where
-        psi1 = All "x" $ Impl (Pred "D" [Var "x"]) (Exists "y" $ Conj (Pred "P" [Var "y"]) (Pred "L" [Var "y", Var "x"]))
-        psi2 = All "x" $ Impl (Pred "P" [Var "x"]) (All "y" $ Impl (Pred "Q" [Var "y"]) (Neg $ Pred "L" [Var "x", Var "y"]))
-        psi3 = All "x" $ Impl (Pred "D" [Var "x"]) (Neg $ Pred "Q" [Var "x"])
+        psi1 = parseFormula "forall x. D(x) -> exists y. P(y) /\\ L(y,x)"
+        psi2 = parseFormula "forall x. P(x) -> forall y. Q(y) -> !L(x, y)"
+        psi3 = parseFormula "forall x. D(x) -> !Q(x)"
 
 main :: IO ()
 main = do
     putStrLn $ "Now making NNF of formula: " ++ show formula1
     print $ makeNNF formula1
     putStrLn $ "Now making PNF of formula: " ++ show formula2
-    print $ makePNF (fromRight $ parseFormula formula2)
+    print . makePNF . renameBinders $ makeNNF formula2
     putStrLn $ "Now making Skolemform of formula: " ++ show formula2
-    print $ makeSkolem (fromRight $ parseFormula formula2)
+    print . makeSkolem . makePNF . renameBinders $ makeNNF formula2
     putStrLn $ "Now proving formula by resolution: " ++ show formula3
     case proveFormula formula3 of
         Left _ -> putStrLn "Success!"
         Right _ -> return ()
     putStrLn $ "Now Proving formula by resolution: " ++ show formula4
-    case doResolution $ makeCNFList formula4 of
+    case doResolution $ makeClauseSet formula4 of
+        Left _ -> putStrLn "Success!"
+        Right _ -> return ()
+    putStrLn $ "Now Proving formula by resolution: " ++ show formula5
+    case proveFormula formula5 of
         Left _ -> putStrLn "Success!"
         Right _ -> return ()
     putStrLn $ "Now Proving formula by resolution: " ++ show formula6
-    case doResolution formula6 of
-        Left _ -> putStrLn "Success!"
-        Right _ -> return ()
-    putStrLn $ "Now Proving formula by resolution: " ++ show (Neg formula5)
-    case proveFormula (Neg formula5) of
-        Left _ -> putStrLn "Success!"
-        Right _ -> return ()
-    putStrLn $ "Now proving formula by resolution: " ++ show formula7
-    case doResolution formula7 of
+    case proveFormula formula6 of
         Left _ -> putStrLn "Success!"
         Right _ -> return ()
\ No newline at end of file
diff --git a/app/Normalforms.hs b/app/Normalforms.hs
new file mode 100644
index 0000000..87db682
--- /dev/null
+++ b/app/Normalforms.hs
@@ -0,0 +1,144 @@
+module Normalforms where
+
+import FOLSyntax
+    ( Formula(..), Term(..), formulaVars, termSubst, findFresh )
+import qualified Data.Set as Set
+import Resolution ( CNF, renameFormula )
+import Data.List ( find )
+import Data.Maybe ( fromJust )
+
+{-
+Now we define some functions to convert given terms to normalforms
+i.e. negation normalform, prenex normal, skolemform, conjunctive normalform
+-}
+
+-- negation normalform
+makeNNF :: Formula -> Formula
+makeNNF form = if form == f' then form else makeNNF f'
+    where
+        f' = nnfStep form
+        nnfStep (Conj f1 f2) = Conj (nnfStep f1) (nnfStep f2)
+        nnfStep (Disj f1 f2) = Disj (nnfStep f1) (nnfStep f2)
+        nnfStep (Impl f1 f2) = Disj (Neg f1) f2
+        nnfStep (All x f) = All x (nnfStep f)
+        nnfStep (Exists x f) = Exists x (nnfStep f)
+        nnfStep (Neg (Conj f1 f2)) = Disj (Neg f1) (Neg f2)
+        nnfStep (Neg (Disj f1 f2)) = Conj (Neg f1) (Neg f2)
+        nnfStep (Neg (Impl f1 f2)) = Conj f1 (Neg f2)
+        nnfStep (Neg (All x f)) = Exists x (Neg f)
+        nnfStep (Neg (Exists x f)) = All x (Neg f)
+        nnfStep (Neg (Neg f)) = f
+        nnfStep (Neg T) = F
+        nnfStep (Neg F) = T
+        nnfStep f = f
+
+-- rename every binder in formula to be disjunct
+renameBinders :: Formula -> Formula
+renameBinders f = fst $ go f []
+    where
+        go :: Formula -> [String] -> (Formula, [String])
+        go (All x f') vs = (All x' f'', vs')
+            where
+                (f'', vs') = go (renameFormula f' x x') (x' : vs)
+                x' = findFresh (formulaVars f ++ vs)
+        go (Exists x f') vs = (Exists x' f'', vs')
+            where
+                (f'', vs') = go (renameFormula f' x x') (x' : vs)
+                x' = findFresh (formulaVars f ++ vs)
+        go (Neg f') vs = (Neg f'', vs')
+            where
+                (f'', vs') = go f' vs
+        go (Conj f1 f2) vs = (Conj f1' f2', vs'')
+            where
+                (f1', vs') = go f1 vs
+                (f2', vs'') = go f2 vs'
+        go (Disj f1 f2) vs = (Disj f1' f2', vs'')
+            where
+                (f1', vs') = go f1 vs
+                (f2', vs'') = go f2 vs'
+        go (Impl f1 f2) vs = (Impl f1' f2', vs'')
+            where
+                (f1', vs') = go f1 vs
+                (f2', vs'') = go f2 vs'
+        go f' vs = (f', vs)
+
+-- prenex normalform
+-- TODO make it so that forall has higher priority to be moved left (makes skolem functions smaller)
+makePNF :: Formula -> Formula
+makePNF form = let form' = pnfStep form in
+            if form == form' then form else makePNF form'
+    where
+        -- swapping rules
+        pnfStep (Conj phi (Exists x psi)) = Exists x (Conj phi psi)
+        pnfStep (Disj phi (Exists x psi)) = Exists x (Disj phi psi)
+        pnfStep (Conj (Exists x psi) phi) = Exists x (Conj psi phi)
+        pnfStep (Disj (Exists x psi) phi) = Exists x (Disj psi phi)
+        pnfStep (Conj phi (All x psi)) = All x (Conj phi psi)
+        pnfStep (Disj phi (All x psi)) = All x (Disj phi psi)
+        pnfStep (Conj (All x psi) phi) = All x (Conj psi phi)
+        pnfStep (Disj (All x psi) phi) = All x (Disj psi phi)
+        -- descent rules
+        pnfStep (All x f) = All x (pnfStep f)
+        pnfStep (Exists x f) = Exists x (pnfStep f)
+        pnfStep (Conj f1 f2) = Conj (pnfStep f1) (pnfStep f2)
+        pnfStep (Disj f1 f2) = Disj (pnfStep f1) (pnfStep f2)
+        pnfStep (Impl f1 f2) = Impl (pnfStep f1) (pnfStep f2) -- can't happen, gets removed in makeNNF
+        pnfStep (Neg f) = Neg (pnfStep f)
+        pnfStep f = f
+
+-- infinite function names for skolemizing
+skolemFuns :: [String]
+skolemFuns = ["sk" ++ show n | n <- [(0 :: Int)..]]
+
+-- returns all function names in a formula
+usedFunctions :: Formula -> [String]
+usedFunctions (Pred _ ts) = concatMap termFunctions ts
+    where
+        termFunctions (Var _) = []
+        termFunctions (Fun f ts') = f : concatMap termFunctions ts'
+usedFunctions (Neg f) = usedFunctions f
+usedFunctions (Conj f1 f2) = usedFunctions f1 ++ usedFunctions f2
+usedFunctions (Disj f1 f2) = usedFunctions f1 ++ usedFunctions f2
+usedFunctions (Impl f1 f2) = usedFunctions f1 ++ usedFunctions f2
+usedFunctions (All _ f) = usedFunctions f
+usedFunctions (Exists _ f) = usedFunctions f
+usedFunctions _ = []
+
+-- skolem form of a formula
+makeSkolem :: Formula -> Formula
+makeSkolem form = go form [] []
+    where
+        substTermInFormula :: Formula -> String -> Term -> Formula
+        substTermInFormula (Pred p ts) x s = Pred p $ map (\t -> termSubst t x s) ts
+        substTermInFormula (Neg f) x s = Neg $ substTermInFormula f x s
+        substTermInFormula (Conj f1 f2) x s = Conj (substTermInFormula f1 x s) (substTermInFormula f2 x s)
+        substTermInFormula (Disj f1 f2) x s = Disj (substTermInFormula f1 x s) (substTermInFormula f2 x s)
+        substTermInFormula (Impl f1 f2) x s = Impl (substTermInFormula f1 x s) (substTermInFormula f2 x s)
+        substTermInFormula f@(All y f') x s = if x == y then f else All y (substTermInFormula f' x s)
+        substTermInFormula f@(Exists y f') x s = if x == y then f else Exists y (substTermInFormula f' x s)
+        substTermInFormula f _ _ = f
+        go (All x f) vs skolems = All x (go f (vs ++ [Var x]) skolems)
+        go (Exists x f) vs skolems = go (substTermInFormula f x (Fun newSkolem vs)) vs (newSkolem : skolems)
+            where newSkolem = fromJust $ find (`notElem` skolems) skolemFuns
+        go f _ _ = f
+
+-- conjunctive normalform, removes all quantors, so its ready for resolution
+makeCNF :: Formula -> Formula
+makeCNF form = let form' = cnfStep form in
+            if form == form' then form else makeCNF form'
+    where
+        cnfStep (Conj phi psi) = Conj (cnfStep phi) (cnfStep psi)
+        cnfStep (Disj (Conj phi psi) xi) = Conj (Disj phi xi) (Disj psi xi)
+        cnfStep (Disj xi (Conj phi psi)) = Conj (Disj xi phi) (Disj xi psi)
+        cnfStep (All _ f) = cnfStep f
+        cnfStep (Exists _ f) = cnfStep f
+        cnfStep f = f
+
+-- create the list of clauses from a formula
+makeClauseSet :: Formula -> CNF
+makeClauseSet (Conj f1 f2) = makeClauseSet f1 `Set.union` makeClauseSet f2
+makeClauseSet (Disj f1 f2) = Set.singleton $ collectDisjs f1 `Set.union` collectDisjs f2
+    where
+        collectDisjs (Disj f1' f2') = collectDisjs f1' `Set.union` collectDisjs f2'
+        collectDisjs f' = Set.singleton f'
+makeClauseSet f = Set.singleton $ Set.singleton f
diff --git a/app/Parser.hs b/app/Parser.hs
index 27d2a41..15503d2 100644
--- a/app/Parser.hs
+++ b/app/Parser.hs
@@ -1,10 +1,17 @@
 module Parser (parseFormula) where
 
 import Lexer
-import FOLSyntax
-import Text.Parsec
+    ( comma,
+      dot,
+      identifier,
+      parens,
+      reserved,
+      reservedOp,
+      whiteSpace )
+import FOLSyntax ( Formula(..), Term(..) )
+import Text.Parsec ( sepBy, eof, (<?>), (<|>), parse, try )
 import Text.Parsec.String (Parser)
-import Data.Functor
+import Data.Functor ( ($>) )
 
 import Prelude hiding (pred, all)
 
@@ -75,5 +82,10 @@ contents p = do
   eof
   return r
 
-parseFormula :: String -> Either ParseError Formula
-parseFormula = parse (contents formula) "stdin"
\ No newline at end of file
+
+fromRight :: Either a b -> b
+fromRight (Left _) = error "fromRight called on left value!"
+fromRight (Right b) = b
+
+parseFormula :: String -> Formula
+parseFormula = fromRight . parse (contents formula) "stdin"
\ No newline at end of file
diff --git a/app/Resolution.hs b/app/Resolution.hs
new file mode 100644
index 0000000..9389581
--- /dev/null
+++ b/app/Resolution.hs
@@ -0,0 +1,123 @@
+module Resolution where
+import Data.Set (Set)
+import qualified Data.Set as Set
+import FOLSyntax
+    ( Formula(Exists, Pred, Neg, Conj, Disj, Impl, All),
+      Term(..),
+      formulaVars,
+      termFreeVars,
+      termSubst,
+      findFresh )
+import Data.List.Extra ( intersect )
+import Data.Maybe ( mapMaybe )
+
+type CNF = Set Clause
+type Clause = Set Literal
+type Literal = Formula
+type Unifier = [(Term, Term)]
+
+-- unification algorithm of martelli montanari
+unify :: [(Term, Term)] -> Maybe [(Term, Term)]
+unify [] = Just []
+-- (delete)
+unify ((Var x, Var y) : rest) | x == y = unify rest
+-- (decomp)
+unify ((Fun f es, Fun g ds) : rest) | f == g && length es == length ds = unify $ zip es ds ++ rest
+-- (conflict)
+unify ((Fun _ _, Fun _ _) : _) = Nothing
+-- (orient)
+unify ((Fun f ts, Var x) : rest) = unify $ (Var x, Fun f ts) : rest
+-- (occurs)
+unify ((Var x, t) : _) | x `elem` termFreeVars t && Var x /= t = Nothing
+-- (elim)
+unify ((Var x, t) : rest) | notElem x (termFreeVars t) && x `elem` concatMap (\(t1, t2) -> termFreeVars t1 ++ termFreeVars t2) rest = unify $ (Var x, t) : map (\(t1, t2) -> (termSubst t1 x t, termSubst t2 x t)) rest
+-- decent
+unify ((t, s) : rest) = do
+    rest' <- unify rest
+    return $ (t, s) : rest'
+
+-- unifies predicates, e.g. P(x,y) == P(f(a), z)
+unifyPredicates :: Literal -> Literal -> Maybe Unifier
+unifyPredicates (Pred p1 ts1) (Neg (Pred p2 ts2)) | p1 == p2 && length p1 == length p2 = unify $ zip ts1 ts2
+unifyPredicates _ _ = Nothing
+
+setConcat :: Ord a => [Set a] -> Set a
+setConcat = foldr Set.union Set.empty
+
+-- a single resolution step as described in gloin
+resolveStep :: CNF -> Either () CNF
+resolveStep clauses = if Set.empty `Set.member` clauses then Left () else Right $ clauses `Set.union` newClauses
+    where
+        -- rename all variables
+        zippedClauses = [(c1, c2) | c1 <- Set.toList clauses, c2 <- Set.toList clauses, c1 /= c2]
+        newClauses = setConcat $ map (uncurry resolveClauses) zippedClauses
+
+-- applies an mgu to a given formula, asserts that the formula contains no quantifiers
+applyMgu :: Formula -> [(Term, Term)] -> Formula
+applyMgu (Pred p ts) mgu = Pred p $ map (`applyMguTerm` mgu) ts
+applyMgu (Neg f) mgu = Neg $ applyMgu f mgu
+applyMgu (Conj f1 f2) mgu = Conj (applyMgu f1 mgu) (applyMgu f2 mgu)
+applyMgu (Disj f1 f2) mgu = Disj (applyMgu f1 mgu) (applyMgu f2 mgu)
+applyMgu (Impl f1 f2) mgu = Impl (applyMgu f1 mgu) (applyMgu f2 mgu)
+applyMgu f _ = f
+-- applies mgu to term
+applyMguTerm :: Term -> [(Term, Term)] -> Term
+applyMguTerm (Var x) [] = Var x
+applyMguTerm (Var x) ((Var y, t) : rest) = if x == y then t else applyMguTerm (Var x) rest
+applyMguTerm (Fun f ts) mgu = Fun f $ map (`applyMguTerm` mgu) ts
+applyMguTerm t _ = t
+
+-- takes two clauses and makes the variables these clauses disjunct
+makeVariablesDisjunct :: Clause -> Clause -> (Clause, Clause)
+makeVariablesDisjunct c1 c2 = (c1', c2')
+    where
+        (used, c1') = makeClauseDisjunct [] c1
+        (_, c2') = makeClauseDisjunct used c2
+-- takes a list of variable names and ensures that the clause does not contain these variables (by renaming), then returns all variables used in the clause + used before
+makeClauseDisjunct :: [String] -> Clause -> ([String], Clause)
+makeClauseDisjunct used clause = (concatMap formulaVars newClause ++ newUsed, newClause)
+    where
+        criticalVars = used `intersect` concatMap formulaVars clause
+        (newUsed, newClause) = foldr foldFun (used, clause) criticalVars
+            where
+                foldFun oldVar (used', clause') = (v' : used', Set.map (\f -> renameFormula f oldVar v') clause')
+                    where
+                        v' = findFresh used'
+
+-- renames all occurences of variable v with v' in a term
+renameTerm :: Term -> String -> String -> Term
+renameTerm t@(Var x) v v' = if x == v then Var v' else t
+renameTerm (Fun g ts) v v' = Fun g (map (\t -> renameTerm t v v') ts)
+
+-- renames all occurences of free variable v with v' in a formula
+renameFormula :: Formula -> String -> String -> Formula
+renameFormula (Pred p ts) v v' = Pred p (map (\t -> renameTerm t v v') ts)
+renameFormula (Neg f') v v' = Neg $ renameFormula f' v v'
+renameFormula (Conj f1 f2) v v' = Conj (renameFormula f1 v v') (renameFormula f2 v v')
+renameFormula (Disj f1 f2) v v' = Disj (renameFormula f1 v v') (renameFormula f2 v v')
+renameFormula (Impl f1 f2) v v' = Impl (renameFormula f1 v v') (renameFormula f2 v v')
+renameFormula (All y f') v v' | y /= v = All y $ renameFormula f' v v'
+renameFormula (Exists y f') v v' | y /= v = Exists y $ renameFormula f' v v'
+renameFormula f' _ _ = f'
+
+-- takes two clauses and tries to unify every literal in a crossproduct, returns the set of all clauses resulting from this resolution step
+resolveClauses :: Clause -> Clause -> Set Clause
+resolveClauses c1 c2 = Set.fromList newClauses
+    where
+        -- first make variables in both clauses disjunct
+        (c1', c2') = makeVariablesDisjunct c1 c2
+        zippedLiterals = [(lit1, lit2) | lit1 <- Set.toList c1', lit2 <- Set.toList c2']
+        newClauses = concat $ mapMaybe (\(l1, l2) -> do
+                                            -- first calculate mgu
+                                            mgu <- unifyPredicates l1 l2
+                                            -- now apply mgu to clauses without l1 and l2
+                                            let c1'' = Set.map (`applyMgu` mgu) (c1' `Set.difference` Set.singleton l1)
+                                            let c2'' = Set.map (`applyMgu` mgu) (c2' `Set.difference` Set.singleton l2)
+                                            return [c1'', c2'']
+                            ) zippedLiterals
+
+-- do resolution until we have proven unfulfillability of formula set
+doResolution :: CNF -> Either () CNF
+doResolution f = do
+    f' <- resolveStep f
+    doResolution f'
\ No newline at end of file
diff --git a/resolution.cabal b/resolution.cabal
index 1feb784..b00543e 100644
--- a/resolution.cabal
+++ b/resolution.cabal
@@ -71,7 +71,7 @@ executable resolution
     -- Directories containing source files.
     hs-source-dirs:   app
 
-    other-modules:    Lexer, Parser, FOLSyntax
+    other-modules:    Lexer, Parser, FOLSyntax, Resolution, Normalforms
 
     -- Base language which the package is written in.
     default-language: Haskell2010