diff --git a/picologic.cabal b/picologic.cabal
--- a/picologic.cabal
+++ b/picologic.cabal
@@ -1,5 +1,5 @@
 name:                picologic
-version:             0.1.1
+version:             0.1.2
 synopsis:            Utilities for symbolic predicate logic expressions
 homepage:            https://github.com/sdiehl/picologic
 license:             MIT
@@ -28,16 +28,20 @@
     Picologic,
     Picologic.Solver,
     Picologic.AST,
-    Picologic.Parser
+    Picologic.Parser,
+    Picologic.Pretty,
+    Picologic.Tseitin
+  other-modules:
+    Picologic.Lexer
   hs-source-dirs:      src
   other-extensions:    DeriveDataTypeable, BangPatterns
   build-depends:       
-    base        >= 4.6 && <4.8,
-    picosat     >= 0.1 && <0.2,
-    containers  >= 0.5 && <0.6,
-    mtl         >= 2.1 && <2.2,
-    pretty      >= 1.1 && <1.2,
-    parsec      >= 3.1 && <3.2
+    base >= 2   && <5,
+    picosat,
+    containers,
+    mtl,
+    pretty,
+    parsec
   default-language:    Haskell2010
 
 executable picologic
@@ -47,7 +51,7 @@
     other-modules: Picologic.Repl
     other-extensions:    DeriveDataTypeable, BangPatterns
     build-depends:       
-      base        >= 4.6 && <4.8,
+      base        >= 2   && <5,
       picosat     >= 0.1 && <0.2,
       containers  >= 0.5 && <0.6,
       mtl         >= 2.1 && <2.2,
@@ -58,3 +62,25 @@
     default-language:    Haskell2010
   else
     buildable: False
+
+--Todo: how to fail 'cabal test' on a QuickCheck error?
+Test-Suite picologic-quickcheck
+   type:       exitcode-stdio-1.0
+   main-is:    tests.hs
+   hs-source-dirs: tests
+   build-depends: 
+      base >= 2 && <5,
+      QuickCheck,
+      containers,
+      picosat,
+      mtl,
+      pretty,
+      picologic
+
+Test-Suite pretty-print-test
+   type:       exitcode-stdio-1.0
+   main-is:    PrettyPrintTest.hs
+   hs-source-dirs: tests
+   build-depends: 
+      base >= 2 && <5,
+      picologic
diff --git a/src/Picologic/AST.hs b/src/Picologic/AST.hs
--- a/src/Picologic/AST.hs
+++ b/src/Picologic/AST.hs
@@ -34,7 +34,7 @@
   | Disj      Expr Expr  -- ^ Logical disjunction
   | Iff       Expr Expr  -- ^ Logical biconditional
   | Implies   Expr Expr  -- ^ Material implication
-  deriving (Eq, Ord, Show, Data, Typeable)
+  deriving (Eq, Ord, Data, Typeable)
 
 -- | Evaluate expression.
 eval :: Ctx -> Expr -> Bool
@@ -57,14 +57,15 @@
     go (Implies e1 e2) !vs = go e1 vs ++ go e2 vs
 
 -- | Negation normal form.
+-- (May result in exponential growth)
 nnf :: Expr -> Expr
 nnf ex = case ex of
   e@(Var _)             -> e
   e@(Neg (Var _))       -> e
-  Neg (Neg e)           -> e
+  Neg (Neg e)           -> nnf e
 
   Conj e1 e2            -> nnf e1 `Conj` nnf e2
-  Neg (Conj e1 e2)      -> nnf $ Neg e1 `Conj` Neg e2
+  Neg (Conj e1 e2)      -> nnf $ Neg e1 `Disj` Neg e2
 
   Disj e1 e2            -> nnf e1 `Disj` nnf e2
   Neg (Disj e1 e2)      -> nnf $ Neg e1 `Conj` Neg e2
@@ -72,15 +73,16 @@
   Implies e1 e2         -> nnf $ Neg e1 `Disj` e2
   Neg (Implies e1 e2)   -> nnf $ e1 `Conj` Neg e2
 
-  Iff e1 e2             -> let a = e1 `Conj` e2
-                               b = Neg e1 `Conj` Neg e2
-                               in nnf $ a `Disj` b
+  Iff e1 e2             -> let a = e1 `Disj` Neg e2
+                               b = Neg e1 `Disj` e2
+                               in nnf $ a `Conj` b
 
   Neg (Iff e1 e2)       -> let a = e1 `Disj` e2
                                b = Neg e1 `Disj` Neg e2
                                in nnf $ a `Conj` b
 
 -- | Conjunctive normal form.
+-- (May result in exponential growth)
 cnf :: Expr -> Expr
 cnf = simp . cnf' . nnf
   where
@@ -97,8 +99,8 @@
 -- | Remove tautologies.
 simp :: Expr -> Expr
 simp ex = case ex of
-  Disj e1 (Neg e2) | e1 == e2 -> e1
-  Disj (Neg e1) e2 | e1 == e2 -> e1
+  -- Disj e1 (Neg e2) | e1 == e2 -> True
+  -- Disj (Neg e1) e2 | e1 == e2 -> True
   Disj e1 e2 -> Disj (simp e1) (simp e2)
   Conj e1 e2       | e1 == e2 -> e1
                    | otherwise -> Conj (simp e1) (simp e2)
diff --git a/src/Picologic/Lexer.hs b/src/Picologic/Lexer.hs
new file mode 100644
--- /dev/null
+++ b/src/Picologic/Lexer.hs
@@ -0,0 +1,74 @@
+module Picologic.Lexer (
+  Parser,
+  Op,
+  contents,
+  parens,
+  reservedOp,
+  reserved,
+  identifier,
+) where
+
+import Control.Monad.Identity
+
+import Text.Parsec
+import Text.Parsec.Language (haskellStyle)
+import qualified Text.Parsec.Token as Tok
+import qualified Text.Parsec.Expr as Ex
+
+type Parser   = ParsecT String () Identity
+type Lexer    = Tok.GenTokenParser String () Identity
+type Language = Tok.GenLanguageDef String () Identity
+type Op       = Ex.Operator String () Identity
+
+-------------------------------------------------------------------------------
+-- Lexer
+-------------------------------------------------------------------------------
+
+reservedOps :: [String]
+reservedOps = [
+    "->",
+    "&",
+    "|",
+    "<->",
+    "~"
+  ]
+
+reservedNames :: [String]
+reservedNames = []
+
+lexerStyle :: Language
+lexerStyle = haskellStyle
+  { Tok.commentStart    = "{-"
+  , Tok.commentEnd      = "-}"
+  , Tok.commentLine     = "--"
+  , Tok.nestedComments  = True
+  , Tok.identStart      = letter
+  , Tok.identLetter     = alphaNum
+  , Tok.opStart         = Tok.opLetter lexerStyle
+  , Tok.opLetter        = oneOf "`~!@$%^&*-+=;:<>./?#"
+  , Tok.reservedOpNames = reservedOps
+  , Tok.reservedNames   = reservedNames
+  , Tok.caseSensitive   = True
+  }
+
+lexer :: Lexer
+lexer = Tok.makeTokenParser lexerStyle
+
+reservedOp :: String -> Parser ()
+reservedOp = Tok.reservedOp lexer
+
+reserved :: String -> Parser ()
+reserved = Tok.reserved lexer
+
+identifier :: Parser String
+identifier = Tok.identifier lexer
+
+parens :: Parser a -> Parser a
+parens = Tok.parens lexer
+
+contents :: Parser a -> Parser a
+contents p = do
+  Tok.whiteSpace lexer
+  r <- p
+  eof
+  return r
diff --git a/src/Picologic/Pretty.hs b/src/Picologic/Pretty.hs
new file mode 100644
--- /dev/null
+++ b/src/Picologic/Pretty.hs
@@ -0,0 +1,73 @@
+module Picologic.Pretty (
+  ppExprU,
+  ppExprA,
+  ppExprLisp,
+  ppSolutions,
+) where
+
+import Picologic.AST (Expr(..), Ident(..), Solutions(..))
+import Text.PrettyPrint
+import Data.List (intersperse)
+
+-- | Pretty print with unicode symbols.
+ppExprU :: Expr -> Doc
+ppExprU ex = case ex of
+  Var (Ident n) -> text n
+  Neg expr      -> char '¬' <> ppExprU expr
+  Conj a b      -> con '∧' a b
+  Disj a b      -> con '∨' a b
+  Implies a b   -> con '→' a b
+  Iff a b       -> con '↔' a b
+  where con c a b =
+          parens $ sep [ppExprU a, char c <+> ppExprU b]
+
+-- | Pretty print with ascii symbols.
+ppExprA :: Expr -> Doc
+ppExprA ex = case ex of
+  Var (Ident n)  ->  text n
+  Neg expr       ->  char '~' <> ppExprA expr
+  Conj e1 e2     ->  parens $ ppExprA e1 <+> char '&' <+> ppExprA e2
+  Disj e1 e2     ->  parens $ ppExprA e1 <+> char '|' <+> ppExprA e2
+  Implies e1 e2  ->  parens $ ppExprA e1 <+> text "->" <+> ppExprA e2
+  Iff e1 e2      ->  parens $ ppExprA e1 <+> text "<->" <+> ppExprA e2
+
+-- | Pretty print into S-Expressions
+ppExprLisp :: Expr -> Doc
+ppExprLisp ex = case ex of
+  Var (Ident n)       -> text n
+  Conj a b            -> con "and" $ ands [a, b]
+  Disj a b            -> con "or" $ ors [a, b]
+  Implies a b         -> con "==>" [a, b]
+  Iff a b             -> con "==" $ iffs [a, b]
+  Neg (Var (Ident n)) -> text $ "-" ++ n
+  Neg (Conj a b)      -> con "nand" $ ands [a, b]
+  Neg (Disj a b)      -> con "nor" $ ors [a, b]
+  Neg (Iff a b)       -> con "xor" $ iffs [a, b]
+  Neg expr            -> parens $ text "not" <+> ppExprLisp expr
+  where con c xs =
+          parens $
+          sep [text c,
+               nest 1 $ sep $ map ppExprLisp xs]
+
+ands [] = []
+ands (Conj a b : xs) = ands [a] ++ ands [b] ++ ands xs
+ands (x:xs) = x : ands xs
+
+ors [] = []
+ors (Disj a b : xs) = ors [a] ++ ors [b] ++ ors xs
+ors (x:xs) = x : ors xs
+
+iffs [] = []
+iffs (Iff a b : xs) = iffs [a] ++ iffs [b] ++ iffs xs
+iffs (x:xs) = x : iffs xs
+
+instance Show Expr where
+  show = show . ppExprLisp
+
+
+ppSolutions :: Solutions -> String
+ppSolutions (Solutions xs) =
+  concat (concat $ intersperse ["\n"] (fmap showExprs xs))
+
+showExprs :: [Expr] -> [String]
+showExprs xs = intersperse " " $ fmap (render . ppExprU) xs
diff --git a/src/Picologic/Solver.hs b/src/Picologic/Solver.hs
--- a/src/Picologic/Solver.hs
+++ b/src/Picologic/Solver.hs
@@ -1,38 +1,81 @@
 module Picologic.Solver (
   solveProp,
-  clausesExpr,
+  solveCNF,
+  solveOneCNF,
+  clausesExpr
 ) where
 
 import Picologic.AST
+import Picologic.Pretty
 import Picosat
 
 import Data.List
 import qualified Data.Map as M
 import Control.Monad.Writer
 
-data Clause
-  = CV Int       -- ^Clause variable ( a or -a )
-  | CL [Clause]  -- ^Set of clause under disjuntion
+-- | Yield the solutions for an expression using the PicoSAT solver.
+solveProp :: Expr -> IO Solutions
+solveProp p = solveCNF $ cnf p
 
-instance Show Clause where
-  show (CV i) = show i
-  show (CL xs) = concat (intersperse " " (fmap show xs))
+-- | Yield the solutions for an expression using the PicoSAT
+-- solver. The Expression must be in CNF form already.
+solveCNF :: Expr -> IO Solutions
+solveCNF p = do
+  solutions <- solveAll ds
+  return $ Solutions $ fmap (backSubst vs') solutions
+  where
+    cs = clausesFromCNF p
+    ds = cnfToDimacs vs cs
+    vs  = M.fromList $ zip vars [1..]
+    vs' = M.fromList $ zip [1..] vars
+    vars = variables p
 
--- | Yield the soutions for an expressions using the PicosSAT solver.
-solveProp :: Expr -> IO Solutions
-solveProp p = solveAll cs >>= return . Solutions . fmap (backSubst vs')
+-- | Yield one single solution for an expression using the PicoSAT
+-- solver. The Expression must be in CNF form already.
+solveOneCNF :: Expr -> IO [Expr]
+solveOneCNF p = do
+  solution <- solve ds
+  return $ backSubst vs' solution
   where
-    cs = filter (not . null) $ fmap toInts $ execWriter $ clauses vs (cnf p)
+    cs = clausesFromCNF p
+    ds = cnfToDimacs vs cs
     vs  = M.fromList $ zip vars [1..]
     vs' = M.fromList $ zip [1..] vars
-    vars = variables (cnf p)
+    vars = variables p
 
+clausesFromCNF :: Expr -> [[Expr]]
+clausesFromCNF p =
+  [ [ case lit of
+         v@(Var name) -> v
+         v@(Neg (Var name)) -> v
+         x -> error $ "input not in CNF: \n" ++ show p
+    | lit <- ors [clause] ]
+  | clause <- ands [p]]
+
+ands :: [Expr] -> [Expr]
+ands [] = []
+ands (Conj a b : xs) = ands [a] ++ ands [b] ++ ands xs
+ands (x:xs) = x : ands xs
+
+ors :: [Expr] -> [Expr]
+ors [] = []
+ors (Disj a b : xs) = ors [a] ++ ors [b] ++ ors xs
+ors (x:xs) = x : ors xs
+
+cnfToDimacs :: M.Map Ident Int -> [[Expr]] -> [[Int]]
+cnfToDimacs vs cs = map (map encode) cs
+  where encode (Var ident)       = vs M.! ident
+        encode (Neg (Var ident)) = negate $ vs M.! ident
+  
+
 -- | Yield the integer clauses given to the SAT solver.
 clausesExpr :: Expr -> [[Int]]
-clausesExpr p = filter (not . null) $ fmap toInts $ execWriter $ clauses vs (cnf p)
+clausesExpr p = ds
   where
-    vs = M.fromList $ zip vars [1..]
-    vars = variables (cnf p)
+    cs = clausesFromCNF p
+    vs  = M.fromList $ zip vars [1..]
+    vars = variables p
+    ds = cnfToDimacs vs cs
 
 backSubst :: M.Map Int Ident -> Solution -> [Expr]
 backSubst env (Solution xs) = fmap go xs
@@ -42,32 +85,3 @@
 backSubst _ Unsatisfiable = []
 backSubst _ Unknown = []
 
-toInts :: Clause -> [Int]
-toInts (CL xs) = fmap (\(CV n) -> n) xs
-toInts (CV x) = [x]
-
-neg :: Clause -> Clause
-neg (CV n) = CV (-n)
-neg (CL xs) = CL (fmap neg xs)
-
-combine :: Clause -> Clause -> Clause
-combine (CL x) (CL y) = CL (x++y)
-combine (CL x) y = combine (CL x) (CL [y])
-combine x (CL y) = combine (CL [x]) (CL y)
-combine x y = CL [x, y]
-
-clauses :: M.Map Ident Int -> Expr -> Writer [Clause] Clause
-clauses env ex = case ex of
-  Var v -> return $ CV (env M.! v)
-  Neg x -> do
-    cs <- clauses env x
-    return (neg cs)
-  Conj e1 e2 -> do
-    cs1 <- clauses env e1
-    cs2 <- clauses env e2
-    tell [cs1, cs2]
-    return (CL [])
-  Disj e1 e2 -> do
-    cs1 <- clauses env e1
-    cs2 <- clauses env e2
-    return (combine cs1 cs2)
diff --git a/src/Picologic/Tseitin.hs b/src/Picologic/Tseitin.hs
new file mode 100644
--- /dev/null
+++ b/src/Picologic/Tseitin.hs
@@ -0,0 +1,182 @@
+module Picologic.Tseitin
+       (tseitinCNF,
+        dropTseitinVarsInSolutions,
+        dropTseitinVars,
+        
+       ) where
+
+-- TODO: How efficient is the `mappend` used by Writer?
+-- TODO: For cases like (Conj (Conj a b) c) the introduction
+--       of one Tseitin var can be enough.
+-- TODO: The outermost (Conj (Conj ...) ...) needn't be
+--       Tseitin encoded at all.
+--       Also, the (Disj (Disj ...) ...) below, needn't be encoded
+--       when they use only variables or negated variables.
+--       Tseitin transformation can be used specifically there to
+--       turn other expressions into variables.
+
+import Prelude hiding (or, and)
+
+import Picologic.AST
+import Control.Monad.State.Strict
+import Control.Monad.Writer.Strict
+
+type TS a = StateT Int (Writer [Expr]) a
+
+evalTS :: TS a -> (a, [Expr])
+evalTS action = 
+  runWriter (evalStateT action 1)
+
+var :: TS Expr
+var = do
+  n <- get
+  put $ succ n
+  return $ Var $ Ident $ "ts*" ++ show n
+
+or xs = foldl1 Disj xs
+and xs = foldl1 Conj xs
+
+tseitinCNF :: Expr -> Expr
+tseitinCNF e =
+  let (var, clauses) = evalTS $ tseitin $ simplify e
+  in and (var : clauses)
+
+neg (Neg x) = x
+neg x       = Neg x
+
+tseitin :: Expr -> TS Expr
+
+tseitin lit@(Var _) = return lit
+
+tseitin lit@(Neg (Var _)) = return lit
+
+tseitin (Conj x y) = do
+  a <- tseitin x
+  b <- tseitin y
+  c <- var
+  tell [or [neg a, neg b, c],
+        or [a, neg c],
+        or [b, neg c]]
+  return c
+
+tseitin (Neg (Conj x y)) = do
+  a <- tseitin x
+  b <- tseitin y
+  c <- var
+  tell [or [neg a, neg b, neg c],
+        or [a, c],
+        or [b, c]]
+  return c
+
+tseitin (Disj x y) = do
+  a <- tseitin x
+  b <- tseitin y
+  c <- var
+  tell [or [a, b, neg c],
+        or [neg a, c],
+        or [neg b, c]]
+  return c
+
+tseitin (Neg (Disj x y)) = do
+  a <- tseitin x
+  b <- tseitin y
+  c <- var
+  tell [or [a, b, c],
+        or [neg a, neg c],
+        or [neg b, neg c]]
+  return c
+
+
+-- |
+-- @
+-- (c -> (a -> b)) & (-c -> -(a->b))
+-- (-c | (-a | b)) & (c | (a&-b))
+-- (-a|b|-c) & (a|c) & (-b|c)
+-- @
+tseitin (Implies x y) = do
+  a <- tseitin x
+  b <- tseitin y
+  c <- var
+  tell [or [neg a, b, neg c],
+        or [a, c],
+        or [neg b, c]]
+  return c
+
+-- |
+-- @
+-- (c -> -(a -> b)) & (-c -> (a->b))
+-- (-c | (a&-b)) & (c | (-a|b))
+-- (a|-c) & (-b|-c) & (-a|b|c)
+-- @
+tseitin (Neg (Implies x y)) = do
+  a <- tseitin x
+  b <- tseitin y
+  c <- var
+  tell [or [a, neg c],
+        or [neg b, neg c],
+        or [neg a, b, c]]
+  return c
+
+-- |
+-- @
+-- (c -> a == b) & (-c -> a /= b)
+-- (-c | ((-a|b) & (a|-b))) & (c | ((a|b) & (-a|-b)))
+-- (-a|b|-c) & (a|-b|-c) & (a|b|c) & (-a|-b|c)
+-- @
+tseitin (Iff x y) = do
+  a <- tseitin x
+  b <- tseitin y
+  c <- var
+  tell [or [neg a, b, neg c],
+        or [a, neg b, neg c],
+        or [a, b, c],
+        or [neg a, neg b, c]]
+  return c
+
+-- |
+-- @
+-- (c -> a /= b) & (-c -> a == b)
+-- (-c | ((a|b) & (-a|-b))) & (c | ((-a|b) & (a|-b)))
+-- (a|b|-c) & (-a|-b|-c) & (-a|b|c) & (a|-b|c)
+-- @
+tseitin (Neg (Iff x y)) = do
+  a <- tseitin x
+  b <- tseitin y
+  c <- var
+  tell [or [a, b, neg c],
+        or [neg a, neg b, neg c],
+        or [neg a, b, c],
+        or [a, neg b, c]]
+  return c
+
+tseitin (Neg x) = do
+  a <- tseitin x
+  c <- var
+  tell [or [neg a, neg c],
+        or [a, c]]
+  return c
+
+dropTseitinVarsInSolutions (Solutions xs) =
+  Solutions $ map dropTseitinVars xs
+
+dropTseitinVars :: [Expr] -> [Expr]
+dropTseitinVars = filter (\x -> not $ isTseitinLiteral x)
+
+isTseitinLiteral :: Expr -> Bool
+isTseitinLiteral lit =
+  case lit of
+    (Var (Ident nm)) -> tseitinName nm
+    (Neg (Var (Ident nm))) -> tseitinName nm
+
+tseitinName ('t':'s':'*':_) = True
+tseitinName _               = False
+
+simplify :: Expr -> Expr
+simplify (Neg (Neg x)) = simplify x
+simplify v@(Var _) = v
+simplify (Neg a) = neg $ simplify a
+simplify (Conj a b) = Conj (simplify a) (simplify b)
+simplify (Disj a b) = Disj (simplify a) (simplify b)
+simplify (Implies a b) = Implies (simplify a) (simplify b)
+simplify (Iff a b) = Iff (simplify a) (simplify b)
+                        
diff --git a/tests/PrettyPrintTest.hs b/tests/PrettyPrintTest.hs
new file mode 100644
--- /dev/null
+++ b/tests/PrettyPrintTest.hs
@@ -0,0 +1,17 @@
+import Picologic
+
+main = print $ ppExprLisp d
+  where a =
+          Disj (Var (Ident "some-var"))
+               (Disj (Var (Ident "another-var"))
+                     (Iff (Var (Ident "ggg"))
+                          (Neg (Iff (Neg (Var (Ident "var-x")))
+                                    (Var (Ident "origin"))))))
+        b = 
+          Conj (Var (Ident "var-y"))
+               (Conj (Var (Ident "ccc"))
+                     (Iff (Var (Ident "ddddd"))
+                          (Neg (Iff (Neg (Var (Ident "abcdefg")))
+                                    (Var (Ident "ggg"))))))
+        c = Disj a b
+        d = Conj c c
diff --git a/tests/tests.hs b/tests/tests.hs
new file mode 100644
--- /dev/null
+++ b/tests/tests.hs
@@ -0,0 +1,85 @@
+import Picologic.AST
+import Picologic.Tseitin
+import Picologic.Solver
+import Picologic.Pretty
+
+import Test.QuickCheck
+import qualified Data.Map as M
+import qualified Data.Set as S
+import System.Exit (exitFailure)
+import System.IO.Unsafe (unsafePerformIO)
+
+instance Arbitrary Expr where
+  arbitrary = sized $ \n ->
+                tree (round $ sqrt $ fromIntegral n :: Int)
+    where tree 0 = elements $ map (Var . Ident) ["a", "b", "c", "d"]
+          tree n =
+            oneof
+            [do a <- tree (pred n)
+                return $ Neg a,
+             do l <- arbitrary
+                let n2 = l `mod` n
+                a <- tree n2
+                b <- tree (n-n2)
+                con <- elements [Conj, Disj, Implies, Iff]
+                return $ con a b]
+  shrink (Var _) = []
+  shrink (Neg (Neg x)) = [x, Neg x] ++ map Neg (shrink x)
+  shrink (Neg x) = [x] ++ map Neg (shrink x)
+  shrink (Conj a b) = [a, b]
+                     ++ map (Conj a) (shrink b)
+                     ++ map (\aa-> Conj aa b) (shrink a)
+  shrink (Disj a b) = [a, b]
+                     ++ map (Disj a) (shrink b)
+                     ++ map (\aa-> Disj aa b) (shrink a)
+  shrink (Implies a b) = [a, b]
+                     ++ map (Implies a) (shrink b)
+                     ++ map (\aa-> Implies aa b) (shrink a)
+  shrink (Iff a b) = [a, b]
+                     ++ map (Iff a) (shrink b)
+                     ++ map (\aa-> Iff aa b) (shrink a)
+
+
+env = M.fromList [(Ident "a", True),
+                  (Ident "b", True),
+                  (Ident "c", False),
+                  (Ident "d", False)]
+
+test_nnf :: Expr -> Bool
+test_nnf e = eval env e == eval env (nnf e)
+
+test_cnf :: Expr -> Bool
+test_cnf e = eval env e == eval env (cnf e)
+
+test_tseitin :: Expr -> Bool
+test_tseitin e = unsafePerformIO test
+  where test = do
+          let ts = tseitinCNF e
+          -- putStrLn "\nexpr"
+          -- print $ ppExprLisp e
+          -- putStrLn "tseitin"
+          -- print $ ppExprLisp ts
+          -- putStrLn "tseitin clauses"
+          -- mapM_ print $ clausesExpr ts
+          as <- solveCNF $ cnf e
+          bs0 <- solveCNF ts
+          let bs =  dropTseitinVarsInSolutions bs0
+          case (as, bs) of
+            (Solutions av, Solutions bv) -> do
+              --print ("as", av)
+              --print ("bs", bv)
+              return $ S.fromList av == S.fromList bv
+
+qc = verboseCheckWith (stdArgs { maxSuccess = 1000 })
+
+-- how to make an error fail a 'cabal test'?
+qcwf p = verboseCheckWith (stdArgs { maxSuccess = 1000 })
+         (whenFail exitFailure p)
+
+main = do
+  putStrLn "nnf"
+  qc test_nnf
+  putStrLn "cnf"
+  qc test_cnf
+  putStrLn "tseitin"
+  qc test_tseitin