diff --git a/Main.hs b/Main.hs
index 9927ad2..a9f931a 100644
--- a/Main.hs
+++ b/Main.hs
@@ -1,99 +1,51 @@
 module Main (main) where
-
-import Data.Foldable (Foldable, any)
-import Data.List (head, tail)
-import Data.Maybe (isNothing)
-import GHC.Base (Maybe (..), (==))
+import Prelude (IO, String, getContents, lines, map, print,
+            otherwise, Bool(..), filter, id, unlines,
+                mapM_, ($), elem, notElem, (||), putStrLn, read, (.))
+import Ternary.Statement  (Statement (..), st)
+import Ternary.Universum  (Universum (..), universum)
+import Ternary.Vee        (cleared, think)
 import System.Environment (getArgs)
-import Ternary.Statement (Statement (..), st)
-import Ternary.Term (Item (..), Term (..))
-import Ternary.Universum (Universum (..), universum)
-import Ternary.Vee (cleared, hasContradiction, think)
-import Prelude
-  ( Bool (..),
-    IO,
-    String,
-    elem,
-    filter,
-    getContents,
-    id,
-    lines,
-    map,
-    mapM_,
-    notElem,
-    otherwise,
-    print,
-    putStrLn,
-    read,
-    unlines,
-    ($),
-    (.),
-    (||),
-  )
+import Data.Foldable (Foldable)
 
-mainSolve :: Universum -> Bool -> IO ()
-mainSolve u onlyNew = do
+main2 :: Universum -> Bool -> IO ()
+main2 u onlyNew = do
   strs <- getContents
   let statements = map str2vee . lines $ strs
       str2vee x = st (read x :: Statement String)
   mapM_ print
     . (if onlyNew then filter (`notElem` statements) else id)
     . cleared
-    . think (universum u)
-    $ statements
+    . think (universum u) $ statements
 
-mainProve :: Universum -> Bool -> IO ()
-mainProve u onlyNew = do
-  strs <- getContents
-  let statements = map str2vee . tail . lines $ strs
-      proveThis = str2vee . head . lines $ strs
-      str2vee x = st (read x :: Statement String)
-      results = cleared . think (universum u) $ statements
-      anyContradictions = any (hasContradiction proveThis) results
-      proof = swapNothingJF $ if anyContradictions then Nothing else Just (Item recalc == Item results)
-      recalc = cleared . think (universum u) $ proveThis : statements
-      swapNothingJF x
-        | isNothing x = Just False
-        | x == Just False = Nothing
-        | x == Just True = Just True
-
-  print recalc
-  putStrLn ""
-  print results
-  putStrLn ""
-  print proof
-
-withArgs :: (String -> Bool) -> IO ()
+withArgs :: (String -> Bool) -> IO () 
 withArgs a
-  | a "-h" || a "--help" =
-      putStrLn . unlines $
-        [ "Logical statement solver",
-          "Usage: solver [PARAMETERS]",
-          "",
-          "Designed according to N.P.Brousentsov works",
-          "and Lewis Carrol diagram. PARAMETERS:",
-          "",
-          "--aristotle, -A\tuse Aristotle logical universum VxVx' for each x",
-          "--new, -n\tfilters only 'new' facts, excluding defined",
-          "--help, -h\tshows this help",
-          "--version, -v\tshows this version",
-          "",
-          "Takes statement \"Socrates is a human\" in such format, e.g.",
-          "",
-          "A \"Socrates\" \"human\"",
-          "",
-          "There are A, E, O, I traditional statements.",
-          "Also there are A~, E~, O~, I~ with negated first part"
-        ]
+  | a "-h" || a "--help" = putStrLn . unlines $
+    ["Logical statement solver",
+     "Usage: solver [PARAMETERS]",
+     "",
+     "Designed according to N.P.Brousentsov works",
+     "and Lewis Carrol diagram. PARAMETERS:",
+     "",
+     "--aristotle, -A\tuse Aristotle logical universum VxVx' for each x",
+     "--new, -n\tfilters only 'new' facts, excluding defined",
+     "--help, -h\tshows this help",
+     "--version, -v\tshows this version",
+     "",
+     "Takes statement \"Socrates is a human\" in such format, e.g.",
+     "",
+     "A \"Socrates\" \"human\"",
+     "",
+     "There are A, E, O, I traditional statements exist.",
+     "Also there are A~, E~, O~, I~ with negated first part"
+    ]
   | a "--version" || a "-v" = putStrLn "v1.0.2"
-  | a "--prove" = mainProve Aristotle False
-  | otherwise = mainSolve uni onlyNew
-  where
-    onlyNew = a "--new" || a "-n"
-    uni =
-      if a "-A" || a "--aristotle"
-        then Aristotle
-        else Empty
+  | otherwise = main2 uni onlyNew where
+     onlyNew = a "--new" || a "-n"
+     uni =
+       if a "-A" || a "--aristotle"
+         then Aristotle
+         else Empty
 
 main :: IO ()
 main = do
diff --git a/Ternary/Statement.hs b/Ternary/Statement.hs
index ef8b74c..a855150 100644
--- a/Ternary/Statement.hs
+++ b/Ternary/Statement.hs
@@ -1,18 +1,14 @@
 module Ternary.Statement (Statement(..), st) where
 import Ternary.Term (Vee, Term(..), Item(..))
-
-data StatementKind = A | I | E | O | A' | I' | E' | O' deriving (Eq, Show, Read)
-data Statement a = Statement StatementKind a a deriving (Eq, Read)
-
-instance Show a => Show (Statement a) where
-  show (Statement A x y) = "Every " ++ show x ++ " is " ++ show y
-  show (Statement I x y) = "Some of " ++ show x ++ " is " ++ show y
-  show (Statement E x y) = "None of " ++ show x ++ " is " ++ show y
-  show (Statement O x y) = "Some of " ++ show x ++ " isn't " ++ show y
-  show (Statement A' x y) = "Every non-" ++ show x ++ " is " ++ show y
-  show (Statement I' x y) = "Some of non-" ++ show x ++ " is " ++ show y
-  show (Statement E' x y) = "None of non-" ++ show x ++ " is " ++ show y
-  show (Statement O' x y) = "Some of non-" ++ show x ++ " isn't " ++ show y
+data Statement a = A a a -- Affirmo (general affirmative)
+               | I a a -- affIrmo (private affirmative)
+               | E a a -- nEgo    (general negative)
+               | O a a -- negO    (private negative)
+               | A' a a
+               | I' a a
+               | E' a a
+               | O' a a
+               deriving (Eq, Show, Read)
 
 inv :: (Eq a) => Term a -> Term a
 inv (Term p x) = Term (not p) x
@@ -24,11 +20,11 @@ i v x y
     | x == y      = Term v . Item $ [x]
 
 st :: (Eq a) => Statement a  -> Vee a
-st (Statement A x y) = i False (Term True x) (Term False y)
-st (Statement I x y) = i True (Term True x) (Term True y)
-st (Statement E x y) = i False (Term True x) (Term True y)
-st (Statement O x y) = i True (Term True x) (Term False y)
-st (Statement A' x y) = i False (Term False x) (Term False y)
-st (Statement I' x y) = i True (Term False x) (Term True y)
-st (Statement E' x y) = i False (Term False x) (Term True y)
-st (Statement O' x y) = i True (Term False x) (Term False y)
+st (A x y) = i False (Term True x) (Term False y)
+st (I x y) = i True (Term True x) (Term True y)
+st (E x y) = i False (Term True x) (Term True y)
+st (O x y) = i True (Term True x) (Term False y)
+st (A' x y) = i False (Term False x) (Term False y)
+st (I' x y) = i True (Term False x) (Term True y)
+st (E' x y) = i False (Term False x) (Term True y)
+st (O' x y) = i True (Term False x) (Term False y)
diff --git a/Ternary/Vee.hs b/Ternary/Vee.hs
index 1743b9e..19f8753 100644
--- a/Ternary/Vee.hs
+++ b/Ternary/Vee.hs
@@ -1,118 +1,68 @@
-module Ternary.Vee (isObvious, hasContradiction, newFact, cleared, think) where
-
-import Data.Foldable (concatMap)
-import Data.List
-  ( elem,
-    filter,
-    head,
-    intersect,
-    iterate,
-    length,
-    nub,
-    null,
-    union,
-    (\\),
-  )
-import Data.Maybe (Maybe (Nothing), mapMaybe)
-import GHC.Base ((<), (>))
-import GHC.Maybe (Maybe (..))
-import Ternary.Term (Item (..), Term (..), Vee)
-import Prelude
-  ( Bool (False, True),
-    Eq,
-    any,
-    foldr,
-    fst,
-    map,
-    not,
-    notElem,
-    otherwise,
-    return,
-    snd,
-    ($),
-    (&&),
-    (.),
-    (/=),
-    (<$>),
-    (<*>),
-    (=<<),
-    (==),
-  )
-
-type Knowledge a = [Vee a]
-
-type InferenceRule a = Vee a -> Vee a -> (Knowledge a, Maybe (Vee a))
-
+module Ternary.Vee (isObvious, newFact, cleared, think) where
+import           Data.List    (head, intersect, length, nub, null, union, (\\))
+import           Data.Maybe   (Maybe (Nothing), mapMaybe)
+import           Prelude      (Bool (False, True), Eq, any, foldr, fst, map,
+                               not, notElem, otherwise, return, snd, ($), (&&),
+                               (.), (/=), (<$>), (<*>), (=<<), (==))
+import           Ternary.Term (Item (..), Term (..), Vee)
 isSubsetOf :: (Eq a) => [a] -> [a] -> Bool
 a `isSubsetOf` b = nda && not ndb
-  where
-    nda = null $ a \\ b
-    ndb = null $ b \\ a
+    where
+     nda = null $ a \\ b
+     ndb = null $ b \\ a
 
 isObvious :: (Eq a) => Vee a -> Vee a -> Bool
 isObvious (Term x (Item a)) (Term y (Item b))
-  | x /= y = False
-  | x = a `isSubsetOf` b
-  | not x = b `isSubsetOf` a
+    | x /= y = False
+    | x = a `isSubsetOf` b
+    | not x = b `isSubsetOf` a
 
-hasContradiction :: (Eq a) => Vee a -> Vee a -> Bool
-hasContradiction (Term x (Item a)) (Term y (Item b))
-  | a == b && x /= y = True
-  | a `isSubsetOf` b && x < y = True
-  | b `isSubsetOf` a && x > y = True
-  | otherwise = False
-
-notT :: Term a -> Term a
-notT (Term x v) = Term (not x) v
-
-rulePosFromNeg :: (Eq a) => InferenceRule a
-rulePosFromNeg (Term False (Item negSet)) positive@(Term True (Item posSet))
-  | length diff /= 1 = ([], Nothing)
-  | missing `elem` posSet = ([], Nothing)
-  | otherwise = ([positive], Just (Term True (Item (missing : posSet))))
-  where
-    diff = negSet \\ posSet
-    missing = notT (head diff)
-
-ruleNegFromNeg :: (Eq a) => InferenceRule a
-ruleNegFromNeg (Term False (Item i0)) (Term False (Item i1))
-  | length evidence /= 1 = ([], Nothing)
-  | null diff0 && null diff1 = (map (Term False . Item) [i0, i1], Just (Term False (Item result)))
-  | otherwise = ([], Just (Term False (Item result)))
-  where
-    evidence = map notT i0 `intersect` i1
-    diff0 = (i0 \\ i1) \\ map notT evidence
-    diff1 = (i1 \\ i0) \\ evidence
-    result = (i0 `intersect` i1) `union` diff0 `union` diff1
-
-newFact :: (Eq a) => InferenceRule a
+newFact :: (Eq a) => Vee a -> Vee a -> ([Vee a], Maybe (Vee a))
 newFact a@(Term True _) b@(Term False _) = newFact b a
-newFact a@(Term False _) b@(Term True _) = rulePosFromNeg a b
-newFact a@(Term False _) b@(Term False _) = ruleNegFromNeg a b
+newFact (Term False (Item iF)) tT@(Term True (Item iT))
+    | length ldF /= 1 = ([], Nothing)
+    | otherwise =
+        if d'F `notElem` iT
+        then (return tT, return (Term True (Item (d'F:iT))))
+        else ([], Nothing)
+      where
+        ldF = iF \\ iT
+        d'F = notT . head $ ldF
+        notT (Term x v) = Term (not x) v
+newFact (Term False (Item i0)) (Term False (Item i1))
+    | length e /= 1 = ([], Nothing)
+    | otherwise =
+        if null d0 && null d1
+        then (map (Term False . Item) [i0, i1], vee0)
+        else ([], vee0)
+    where
+      notT (Term x v) = Term (not x) v
+      terms = (i0 `intersect` i1) `union` d0 `union` d1
+      e = map notT i0 `intersect` i1
+      d0 = (i0 \\ i1) \\ map notT e
+      d1 = (i1 \\ i0) \\ e
+      vee0 = return (Term False (Item terms))
 newFact _ _ = ([], Nothing)
 
-next :: (Eq a) => (Knowledge a, Knowledge a) -> (Knowledge a, Knowledge a)
-next (old, new) = (old `union` new \\ used, added)
-  where
-    results = [newFact o n | o <- old, n <- new]
-    used = concatMap fst results
-    added = mapMaybe snd results
+pseudofix :: (Eq a) => (a -> a) -> a -> a
+pseudofix f x0
+ | y == y' = y
+ | otherwise = y'
+ where
+  y  = f x0
+  y' = f y
 
-applyFacts :: (Eq a) => Knowledge a -> Knowledge a -> Knowledge a
-applyFacts old new =
-  fst . head . dropStable $ iterate next (old, new)
-  where
-    dropStable (x : y : xs)
-      | x == y = [x]
-      | otherwise = dropStable (y : xs)
-    dropStable _ = []
+next :: (Eq a) => ([Vee a], [Vee a]) -> ([Vee a], [Vee a])
+next (o,n) = (o `union` n \\ (fst =<< r), mapMaybe snd r)
+ where
+   r = newFact <$> o <*> n
 
-cleared :: (Eq a) => Knowledge a -> Knowledge a
-cleared vees = nub $ filter (not . isRedundant) vees
-  where
-    isRedundant v = any (isObvious v) vees
+applyFacts :: (Eq a) => [Vee a] -> [Vee a] -> [Vee a]
+applyFacts old new = fst $ pseudofix next (old, new)
 
-think :: (Eq a) => (Knowledge a -> Knowledge a) -> Knowledge a -> Knowledge a
-think addition = foldr (applyFacts . withUni . return) []
-  where
+cleared :: (Eq a) => [Vee a] -> [Vee a]
+cleared vees = nub [vee | vee <- vees, not $ any (isObvious vee) vees]
+
+think :: (Eq a) => ([Vee a]->[Vee a]) -> [Vee a] -> [Vee a]
+think addition = foldr (applyFacts . withUni . return) [] where
     withUni vees = applyFacts (addition vees) vees
diff --git a/Tests/syllotest b/Tests/syllotest
index 6aed93e..0458467 100644
--- a/Tests/syllotest
+++ b/Tests/syllotest
@@ -1,96 +1,96 @@
-(Statement A "y" "z", Statement A "x" "y", Statement A "x" "z")
-(Statement A "y" "z", Statement E' "x" "y", Statement E' "x" "z")
-(Statement E "y" "z", Statement A "x" "y", Statement E "x" "z")
-(Statement E "y" "z", Statement E' "x" "y", Statement A' "x" "z")
-(Statement A "y" "z", Statement A "x" "y", Statement I "x" "z")
-(Statement A "y" "z", Statement A "x" "y", Statement I' "x" "z")
-(Statement A "y" "z", Statement E' "x" "y", Statement O "x" "z")
-(Statement A "y" "z", Statement E' "x" "y", Statement O' "x" "z")
-(Statement E "y" "z", Statement A "x" "y", Statement O "x" "z")
-(Statement E "y" "z", Statement A "x" "y", Statement O' "x" "z")
-(Statement E "y" "z", Statement E' "x" "y", Statement I "x" "z")
-(Statement E "y" "z", Statement E' "x" "y", Statement I' "x" "z")
-(Statement A "y" "z", Statement A' "x" "y", Statement I "x" "z")
-(Statement A "y" "z", Statement E "x" "y", Statement O' "x" "z")
-(Statement E "y" "z", Statement A' "x" "y", Statement O "x" "z")
-(Statement E "y" "z", Statement E "x" "y", Statement I' "x" "z")
-(Statement A "y" "z", Statement I "x" "y", Statement I "x" "z")
-(Statement A "y" "z", Statement O' "x" "y", Statement O' "x" "z")
-(Statement E "y" "z", Statement I "x" "y", Statement O "x" "z")
-(Statement E "y" "z", Statement O' "x" "y", Statement I' "x" "z")
-(Statement I "y" "z", Statement A' "x" "y", Statement I "x" "z")
-(Statement I "y" "z", Statement E "x" "y", Statement O' "x" "z")
-(Statement O "y" "z", Statement A' "x" "y", Statement O "x" "z")
-(Statement O "y" "z", Statement E "x" "y", Statement I' "x" "z")
-(Statement A "z" "y", Statement A' "x" "y", Statement A' "x" "z")
-(Statement A "z" "y", Statement E "x" "y", Statement E "x" "z")
-(Statement E "z" "y", Statement A "x" "y", Statement E "x" "z")
-(Statement E "z" "y", Statement E' "x" "y", Statement A' "x" "z")
-(Statement A "z" "y", Statement A' "x" "y", Statement I "x" "z")
-(Statement A "z" "y", Statement A' "x" "y", Statement I' "x" "z")
-(Statement A "z" "y", Statement E "x" "y", Statement O "x" "z")
-(Statement A "z" "y", Statement E "x" "y", Statement O' "x" "z")
-(Statement E "z" "y", Statement A "x" "y", Statement O "x" "z")
-(Statement E "z" "y", Statement A "x" "y", Statement O' "x" "z")
-(Statement E "z" "y", Statement E' "x" "y", Statement I "x" "z")
-(Statement E "z" "y", Statement E' "x" "y", Statement I' "x" "z")
-(Statement A "z" "y", Statement A "x" "y", Statement I' "x" "z")
-(Statement A "z" "y", Statement E' "x" "y", Statement O "x" "z")
-(Statement E "z" "y", Statement A' "x" "y", Statement O "x" "z")
-(Statement E "z" "y", Statement E "x" "y", Statement I' "x" "z")
-(Statement A "z" "y", Statement I' "x" "y", Statement I' "x" "z")
-(Statement A "z" "y", Statement O "x" "y", Statement O "x" "z")
-(Statement E "z" "y", Statement I "x" "y", Statement O "x" "z")
-(Statement E "z" "y", Statement O' "x" "y", Statement I' "x" "z")
-(Statement I "z" "y", Statement A' "x" "y", Statement I "x" "z")
-(Statement I "z" "y", Statement E "x" "y", Statement O' "x" "z")
-(Statement O "z" "y", Statement A "x" "y", Statement O' "x" "z")
-(Statement O "z" "y", Statement E' "x" "y", Statement I "x" "z")
-(Statement A "y" "z", Statement A' "y" "x", Statement A "x" "z")
-(Statement A "y" "z", Statement E' "y" "x", Statement E' "x" "z")
-(Statement E "y" "z", Statement A' "y" "x", Statement E "x" "z")
-(Statement E "y" "z", Statement E' "y" "x", Statement A' "x" "z")
-(Statement A "y" "z", Statement A' "y" "x", Statement I "x" "z")
-(Statement A "y" "z", Statement A' "y" "x", Statement I' "x" "z")
-(Statement A "y" "z", Statement E' "y" "x", Statement O "x" "z")
-(Statement A "y" "z", Statement E' "y" "x", Statement O' "x" "z")
-(Statement E "y" "z", Statement A' "y" "x", Statement O "x" "z")
-(Statement E "y" "z", Statement A' "y" "x", Statement O' "x" "z")
-(Statement E "y" "z", Statement E' "y" "x", Statement I "x" "z")
-(Statement E "y" "z", Statement E' "y" "x", Statement I' "x" "z")
-(Statement A "y" "z", Statement A "y" "x", Statement I "x" "z")
-(Statement A "y" "z", Statement E "y" "x", Statement O' "x" "z")
-(Statement E "y" "z", Statement A "y" "x", Statement O "x" "z")
-(Statement E "y" "z", Statement E "y" "x", Statement I' "x" "z")
-(Statement A "y" "z", Statement I "y" "x", Statement I "x" "z")
-(Statement A "y" "z", Statement O "y" "x", Statement O' "x" "z")
-(Statement E "y" "z", Statement I "y" "x", Statement O "x" "z")
-(Statement E "y" "z", Statement O "y" "x", Statement I' "x" "z")
-(Statement I "y" "z", Statement A "y" "x", Statement I "x" "z")
-(Statement I "y" "z", Statement E "y" "x", Statement O' "x" "z")
-(Statement O "y" "z", Statement A "y" "x", Statement O "x" "z")
-(Statement O "y" "z", Statement E "y" "x", Statement I' "x" "z")
-(Statement A "z" "y", Statement A "y" "x", Statement A' "x" "z")
-(Statement A "z" "y", Statement E "y" "x", Statement E "x" "z")
-(Statement E "z" "y", Statement A' "y" "x", Statement E "x" "z")
-(Statement E "z" "y", Statement E' "y" "x", Statement A' "x" "z")
-(Statement A "z" "y", Statement A "y" "x", Statement I "x" "z")
-(Statement A "z" "y", Statement A "y" "x", Statement I' "x" "z")
-(Statement A "z" "y", Statement E "y" "x", Statement O "x" "z")
-(Statement A "z" "y", Statement E "y" "x", Statement O' "x" "z")
-(Statement E "z" "y", Statement A' "y" "x", Statement O "x" "z")
-(Statement E "z" "y", Statement A' "y" "x", Statement O' "x" "z")
-(Statement E "z" "y", Statement E' "y" "x", Statement I "x" "z")
-(Statement E "z" "y", Statement E' "y" "x", Statement I' "x" "z")
-(Statement A "z" "y", Statement A' "y" "x", Statement I' "x" "z")
-(Statement A "z" "y", Statement E' "y" "x", Statement O "x" "z")
-(Statement E "z" "y", Statement A "y" "x", Statement O "x" "z")
-(Statement E "z" "y", Statement E "y" "x", Statement I' "x" "z")
-(Statement A "z" "y", Statement I' "y" "x", Statement I' "x" "z")
-(Statement A "z" "y", Statement O' "y" "x", Statement O "x" "z")
-(Statement E "z" "y", Statement I "y" "x", Statement O "x" "z")
-(Statement E "z" "y", Statement O "y" "x", Statement I' "x" "z")
-(Statement I "z" "y", Statement A "y" "x", Statement I "x" "z")
-(Statement I "z" "y", Statement E "y" "x", Statement O' "x" "z")
-(Statement O "z" "y", Statement A' "y" "x", Statement O' "x" "z")
-(Statement O "z" "y", Statement E' "y" "x", Statement I "x" "z")
+(A "y" "z", A "x" "y", A "x" "z")
+(A "y" "z", E' "x" "y", E' "x" "z")
+(E "y" "z", A "x" "y", E "x" "z")
+(E "y" "z", E' "x" "y", A' "x" "z")
+(A "y" "z", A "x" "y", I "x" "z")
+(A "y" "z", A "x" "y", I' "x" "z")
+(A "y" "z", E' "x" "y", O "x" "z")
+(A "y" "z", E' "x" "y", O' "x" "z")
+(E "y" "z", A "x" "y", O "x" "z")
+(E "y" "z", A "x" "y", O' "x" "z")
+(E "y" "z", E' "x" "y", I "x" "z")
+(E "y" "z", E' "x" "y", I' "x" "z")
+(A "y" "z", A' "x" "y", I "x" "z")
+(A "y" "z", E "x" "y", O' "x" "z")
+(E "y" "z", A' "x" "y", O "x" "z")
+(E "y" "z", E "x" "y", I' "x" "z")
+(A "y" "z", I "x" "y", I "x" "z")
+(A "y" "z", O' "x" "y", O' "x" "z")
+(E "y" "z", I "x" "y", O "x" "z")
+(E "y" "z", O' "x" "y", I' "x" "z")
+(I "y" "z", A' "x" "y", I "x" "z")
+(I "y" "z", E "x" "y", O' "x" "z")
+(O "y" "z", A' "x" "y", O "x" "z")
+(O "y" "z", E "x" "y", I' "x" "z")
+(A "z" "y", A' "x" "y", A' "x" "z")
+(A "z" "y", E "x" "y", E "x" "z")
+(E "z" "y", A "x" "y", E "x" "z")
+(E "z" "y", E' "x" "y", A' "x" "z")
+(A "z" "y", A' "x" "y", I "x" "z")
+(A "z" "y", A' "x" "y", I' "x" "z")
+(A "z" "y", E "x" "y", O "x" "z")
+(A "z" "y", E "x" "y", O' "x" "z")
+(E "z" "y", A "x" "y", O "x" "z")
+(E "z" "y", A "x" "y", O' "x" "z")
+(E "z" "y", E' "x" "y", I "x" "z")
+(E "z" "y", E' "x" "y", I' "x" "z")
+(A "z" "y", A "x" "y", I' "x" "z")
+(A "z" "y", E' "x" "y", O "x" "z")
+(E "z" "y", A' "x" "y", O "x" "z")
+(E "z" "y", E "x" "y", I' "x" "z")
+(A "z" "y", I' "x" "y", I' "x" "z")
+(A "z" "y", O "x" "y", O "x" "z")
+(E "z" "y", I "x" "y", O "x" "z")
+(E "z" "y", O' "x" "y", I' "x" "z")
+(I "z" "y", A' "x" "y", I "x" "z")
+(I "z" "y", E "x" "y", O' "x" "z")
+(O "z" "y", A "x" "y", O' "x" "z")
+(O "z" "y", E' "x" "y", I "x" "z")
+(A "y" "z", A' "y" "x", A "x" "z")
+(A "y" "z", E' "y" "x", E' "x" "z")
+(E "y" "z", A' "y" "x", E "x" "z")
+(E "y" "z", E' "y" "x", A' "x" "z")
+(A "y" "z", A' "y" "x", I "x" "z")
+(A "y" "z", A' "y" "x", I' "x" "z")
+(A "y" "z", E' "y" "x", O "x" "z")
+(A "y" "z", E' "y" "x", O' "x" "z")
+(E "y" "z", A' "y" "x", O "x" "z")
+(E "y" "z", A' "y" "x", O' "x" "z")
+(E "y" "z", E' "y" "x", I "x" "z")
+(E "y" "z", E' "y" "x", I' "x" "z")
+(A "y" "z", A "y" "x", I "x" "z")
+(A "y" "z", E "y" "x", O' "x" "z")
+(E "y" "z", A "y" "x", O "x" "z")
+(E "y" "z", E "y" "x", I' "x" "z")
+(A "y" "z", I "y" "x", I "x" "z")
+(A "y" "z", O "y" "x", O' "x" "z")
+(E "y" "z", I "y" "x", O "x" "z")
+(E "y" "z", O "y" "x", I' "x" "z")
+(I "y" "z", A "y" "x", I "x" "z")
+(I "y" "z", E "y" "x", O' "x" "z")
+(O "y" "z", A "y" "x", O "x" "z")
+(O "y" "z", E "y" "x", I' "x" "z")
+(A "z" "y", A "y" "x", A' "x" "z")
+(A "z" "y", E "y" "x", E "x" "z")
+(E "z" "y", A' "y" "x", E "x" "z")
+(E "z" "y", E' "y" "x", A' "x" "z")
+(A "z" "y", A "y" "x", I "x" "z")
+(A "z" "y", A "y" "x", I' "x" "z")
+(A "z" "y", E "y" "x", O "x" "z")
+(A "z" "y", E "y" "x", O' "x" "z")
+(E "z" "y", A' "y" "x", O "x" "z")
+(E "z" "y", A' "y" "x", O' "x" "z")
+(E "z" "y", E' "y" "x", I "x" "z")
+(E "z" "y", E' "y" "x", I' "x" "z")
+(A "z" "y", A' "y" "x", I' "x" "z")
+(A "z" "y", E' "y" "x", O "x" "z")
+(E "z" "y", A "y" "x", O "x" "z")
+(E "z" "y", E "y" "x", I' "x" "z")
+(A "z" "y", I' "y" "x", I' "x" "z")
+(A "z" "y", O' "y" "x", O "x" "z")
+(E "z" "y", I "y" "x", O "x" "z")
+(E "z" "y", O "y" "x", I' "x" "z")
+(I "z" "y", A "y" "x", I "x" "z")
+(I "z" "y", E "y" "x", O' "x" "z")
+(O "z" "y", A' "y" "x", O' "x" "z")
+(O "z" "y", E' "y" "x", I "x" "z")
diff --git a/shell.nix b/shell.nix
deleted file mode 100644
index 78b508d..0000000
--- a/shell.nix
+++ /dev/null
@@ -1,7 +0,0 @@
-{ pkgs ? import <nixpkgs> {} }:
-
-pkgs.mkShell {
-  buildInputs = with pkgs; [
-    ghc
-  ];
-}
\ No newline at end of file