diff --git a/Ternary/Statement.hs b/Ternary/Statement.hs
new file mode 100644
index 0000000..a855150
--- /dev/null
+++ b/Ternary/Statement.hs
@@ -0,0 +1,30 @@
+module Ternary.Statement (Statement(..), st) where
+import Ternary.Term (Vee, Term(..), Item(..))
+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
+
+i :: (Eq a) => Bool -> Term a -> Term a -> Vee a
+i v x y
+    | x == inv y  = error "x and not x under the same Vee, refusing to calculate"
+    | x /= y      = Term v . Item $ [x, y]
+    | x == y      = Term v . Item $ [x]
+
+st :: (Eq a) => Statement a  -> Vee a
+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/Term.hs b/Ternary/Term.hs
new file mode 100644
index 0000000..ea694ad
--- /dev/null
+++ b/Ternary/Term.hs
@@ -0,0 +1,34 @@
+module Ternary.Term (Term(..), Item(..), Vee) where
+import           Data.List     (concatMap, null, (++), (\\))
+import           Prelude       (Applicative, Bool (False, True), Eq, Functor,
+                                Read, Show, String, fmap, map, pure, show,
+                                (&&), (/=), (<*>), (==), (||))
+
+data Term a = Term Bool a deriving (Read)
+newtype Item a = Item [a] deriving (Read)
+type Vee a = Term (Item (Term a))
+
+instance Functor Item where
+    fmap f (Item a) = Item (map f a)
+
+instance Applicative Item where
+    pure x = Item [x]
+    (Item fs) <*> (Item xs) = Item [f x | f <- fs, x <- xs]
+
+instance (Eq a) => Eq (Item a) where
+    (Item x) == (Item y) = null dxy && null dyx
+             where
+               dxy = x \\ y
+               dyx = y \\ x
+
+instance (Eq a) => Eq (Term a) where
+  Term v x == Term w y = (v==w) && (x==y)
+  Term v x /= Term w y = (v/=w) || (x/=y)
+
+instance Show (Term String) where
+  show (Term False y) = y ++ "`"
+  show (Term True y)  = y
+
+instance Show (Term (Item (Term String))) where
+    show (Term x i) = show (Term x "V") ++ concatMap show (it i)
+                      where it (Item ii) = ii
diff --git a/Ternary/Universum.hs b/Ternary/Universum.hs
new file mode 100644
index 0000000..7397ab0
--- /dev/null
+++ b/Ternary/Universum.hs
@@ -0,0 +1,22 @@
+module Ternary.Universum (Universum(..), universum, aFromStatements) where
+import           Data.List     (nub)
+import           Ternary.Term  (Item (..), Term (..), Vee)
+
+data Universum = Aristotle
+               | Empty
+               | Default
+
+universum :: (Eq a) => Universum -> [Vee a] -> [Vee a]
+universum Aristotle facts =
+    [Term True (Item [Term x v])
+         | v <- aFromStatements facts,
+           x <- [False, True]]
+universum Empty _ = []
+universum Default xs = xs
+
+aFromStatements :: (Eq a) => [Vee a] -> [a]
+aFromStatements = nub . concatMap (extract . getItem . getVee)
+  where
+    getItem  (Item x) = x
+    getVee (Term _ i) = i
+    extract terms = [v | (Term _ v) <- terms]
diff --git a/Ternary/Vee.hs b/Ternary/Vee.hs
new file mode 100644
index 0000000..19f8753
--- /dev/null
+++ b/Ternary/Vee.hs
@@ -0,0 +1,68 @@
+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
+
+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
+
+newFact :: (Eq a) => Vee a -> Vee a -> ([Vee a], Maybe (Vee a))
+newFact a@(Term True _) b@(Term False _) = newFact b a
+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)
+
+pseudofix :: (Eq a) => (a -> a) -> a -> a
+pseudofix f x0
+ | y == y' = y
+ | otherwise = y'
+ where
+  y  = f x0
+  y' = f y
+
+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
+
+applyFacts :: (Eq a) => [Vee a] -> [Vee a] -> [Vee a]
+applyFacts old new = fst $ pseudofix next (old, new)
+
+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