diff --git a/Data/Boolean.hs b/Data/Boolean.hs
--- a/Data/Boolean.hs
+++ b/Data/Boolean.hs
@@ -25,8 +25,11 @@
 
   ) where
 
-import Data.List ( nub )
+import Data.Maybe ( mapMaybe )
+import qualified Data.IntMap as IM
 
+import Control.Monad ( guard, liftM )
+
 -- | Boolean formulas are represented as values of type @Boolean@.
 -- 
 data Boolean
@@ -78,7 +81,7 @@
 -- 
 booleanToCNF :: Boolean -> CNF
 booleanToCNF
-  = map (nub . map literal . disjunction)
+  = mapMaybe (simpleClause . map literal . disjunction)
   . conjunction
   . asLongAsPossible distribute
   . asLongAsPossible pushNots
@@ -110,6 +113,22 @@
 
 
 -- private helper functions
+
+-- remove duplicate literals from clauses and drop clauses that
+-- contain one literal both positively and negatively.
+--
+simpleClause :: Clause -> Maybe Clause
+simpleClause = liftM (map lit . IM.toList) . foldl add (Just IM.empty)
+ where
+  lit (x,True)  = Pos x
+  lit (x,False) = Neg x
+
+  add mm l = do
+    m <- mm
+    let x = literalVar l; kind = isPositiveLiteral l
+    maybe (Just (IM.insert x kind m))
+          (\b -> guard (b==kind) >> Just m)
+          (IM.lookup x m)
 
 conjunction :: Boolean -> [Boolean]
 conjunction b = flat b []
diff --git a/incremental-sat-solver.cabal b/incremental-sat-solver.cabal
--- a/incremental-sat-solver.cabal
+++ b/incremental-sat-solver.cabal
@@ -1,5 +1,5 @@
 Name:          incremental-sat-solver
-Version:       0.1.5
+Version:       0.1.6
 Cabal-Version: >= 1.6
 Synopsis:      Simple, Incremental SAT Solving as a Library
 Description:   This Haskell library provides an implementation of the