diff --git a/Satchmo/Data.hs b/Satchmo/Data.hs
--- a/Satchmo/Data.hs
+++ b/Satchmo/Data.hs
@@ -1,24 +1,36 @@
 {-# language TypeFamilies #-}
+{-# language GeneralizedNewtypeDeriving #-}
 
 module Satchmo.Data 
 
-( CNF, cnf, clauses
--- FIXME: exports should be abstract
-, Clause(..), clause, literals
-, Literal (..), literal, nicht, positive, variable
+( CNF, cnf, singleton, clauses, foldr, filter, size
+, Clause, clause, literals, without
+, Literal, literal, nicht, positive, variable
 , Variable 
 )
 
 where
 
-import Control.Monad.State.Strict
+import Prelude hiding ( foldr, filter )
+import qualified Prelude
+  
+import qualified Data.Set as S
+import qualified Data.Map as M
+import qualified Data.Foldable as F
+import Data.Monoid
+import Data.List ( nub )
 
 type Variable = Int
 
-data Literal = Literal { variable :: Variable , positive :: Bool }
+data Literal =
+     Literal { variable :: ! Variable
+             , positive :: ! Bool
+             }
+     deriving ( Eq, Ord )
 
 instance Show Literal where
-    show l = ( if positive l then "" else "-" ) ++ show ( variable l )
+    show l = ( if positive l then "" else "-" )
+             ++ show ( variable l )
 
 literal :: Bool -> Variable -> Literal
 literal pos v  = Literal { positive = pos, variable = v }
@@ -26,21 +38,58 @@
 nicht :: Literal -> Literal 
 nicht x = x { positive = not $ positive x }
 
-newtype CNF     = CNF { clauses :: [ Clause ] }
+newtype CNF  = CNF ( S.Set Clause )
+    deriving ( Monoid )
 
-instance Show ( CNF  ) where
-    show ( CNF cs ) = unlines $ map show cs
+foldr f x (CNF s) = F.foldr f x s
+filter p (CNF s) = CNF $ S.filter p s
 
+size (CNF s) = S.size s
+                   
+clauses (CNF s) = F.toList s
+
+instance Show CNF  where
+    show cnf = unlines $ map show $ clauses cnf
+
 cnf :: [ Clause ] -> CNF 
-cnf cs = CNF cs
+cnf cs = CNF $ S.fromList $ Prelude.filter ( /= CTrue) cs
 
+singleton c = CNF $ S.singleton c
 
-newtype Clause = Clause { literals :: [ Literal ] }
 
+data Clause = Clause  ! ( M.Map Variable Bool )  | CTrue
+   deriving ( Eq, Ord )
+
+literals :: Clause ->  [ Literal ]
+literals c = case c of
+  Clause m -> map ( \ (v,p) -> literal p v ) $ M.toList m
+
+instance Monoid Clause where
+  mempty = Clause M.empty
+  mappend c1 c2 = case c1 of
+    CTrue -> CTrue
+    Clause m1 -> case c2 of
+      CTrue -> CTrue
+      Clause m2 ->
+        let common = M.intersection m1 m2
+        in  if M.isSubmapOf common m1 && M.isSubmapOf common m2
+            then Clause $ M.union m1 m2
+            else CTrue
+
 instance Show ( Clause ) where
-    show ( Clause xs ) = unwords ( map show xs ++ [ "0" ] )
+  show c = case c of
+    CTrue -> "# True"
+    Clause m -> unwords ( map show (literals c) ++ [ "0" ] )
 
 clause ::  [ Literal ] -> Clause 
-clause ls = Clause { literals = ls }
-
+clause ls = Prelude.foldr
+            ( \ l c -> case c of
+                 CTrue -> CTrue           
+                 Clause m -> case M.lookup (variable l) m of
+                   Nothing -> Clause $ M.insert (variable l) (positive l) m
+                   Just p -> if p == positive l then Clause m else CTrue
+            ) mempty ls
 
+without c w = case c of
+  -- CTrue -> CTrue -- ?
+  Clause m -> Clause $ M.filterWithKey ( \ v p -> w /= v ) m
diff --git a/Satchmo/Fourier_Motzkin.hs b/Satchmo/Fourier_Motzkin.hs
new file mode 100644
--- /dev/null
+++ b/Satchmo/Fourier_Motzkin.hs
@@ -0,0 +1,106 @@
+{-# language TupleSections #-}
+
+module Satchmo.Fourier_Motzkin where
+
+import Satchmo.Data
+
+import qualified Data.Map.Strict as M
+import qualified Data.Set as S
+import Control.Monad ( guard )
+import Data.Monoid
+import Data.List ( sortBy, nub )
+import Data.Function (on)
+import System.IO
+
+type Solver = CNF -> IO (Maybe (M.Map Variable Bool))
+
+fomo :: Solver
+fomo cnf = do
+  print_info "fomo" cnf
+  ( remove_satisfied $ trivial $ onesided $  eliminate fomo ) cnf
+
+print_info msg cnf = do
+  hPutStrLn stderr $ unwords [ msg, show $ size cnf, "\n" ]
+  -- hPutStrLn stderr $ show cnf ++ "\n"
+
+remove_satisfied cont cnf = do
+  print_info "remove_satisfied" cnf
+  let vars polar cl = S.fromList $ do
+        lit <- literals cl;
+        guard $ positive lit == polar
+        return $ variable lit
+      remaining = Satchmo.Data.filter
+        ( \ cl -> disjoint ( vars True cl ) ( vars False cl ))
+        cnf
+  cont cnf
+
+trivial :: Solver -> Solver
+trivial cont cnf = do
+  print_info "trivial" cnf
+  if null $ clauses cnf
+     then return $ Just M.empty
+     else if clause [] `elem` clauses cnf
+          then return $ Nothing
+          else cont cnf
+
+onesided :: Solver -> Solver
+onesided cont cnf = do
+  print_info "onesided" cnf
+  let pos = occurrences True  cnf
+      neg = occurrences False cnf
+      onlypos = M.keys $ M.difference pos neg
+      onlyneg = M.keys $ M.difference neg pos
+      assigned = M.fromList
+          $ map (,True) onlypos ++ map (,False) onlyneg
+      ks = M.keysSet assigned
+      others = Satchmo.Data.filter
+         ( \ cl -> disjoint ks
+                   $ S.fromList $ map variable $ literals cl) 
+         cnf
+  hPutStrLn stderr $ unwords [ "assigned", show assigned , "\n" ]       
+  later <- ( if size others < size cnf then fomo else cont ) others
+  return $ fmap ( M.union assigned ) later
+
+disjoint s t = S.null $ S.intersection s t
+
+eliminate :: Solver -> Solver
+eliminate cont nf = do
+  print_info "eliminate" nf
+  let pos = occurrences True  nf
+      neg = occurrences False nf
+      reductions = M.intersectionWith
+         ( \ xs ys -> let lx = length xs
+                          ly = length xs
+                      in  lx*ly - lx - ly
+         ) pos neg
+      resolve v = cnf $ do
+        cp <- pos M.! v
+        let cpv = cp `without` v
+        cn <- neg M.! v
+        let cnv = cn `without` v
+        return $  cpv <> cnv
+      others v = Satchmo.Data.filter
+        ( \ cl -> not $ elem v $ map variable $ literals cl )
+        nf
+      reconstruct v m = Prelude.or $ do
+        cp <- pos M.! v
+        return $ Prelude.not $ Prelude.or $ do
+          lit <- literals $ cp `without` v
+          let v = M.findWithDefault False ( variable lit ) m
+          return $ if positive lit then v else Prelude.not v 
+  case sortBy (compare `on` snd) $ M.toList reductions of
+        (v,c): _ -> do
+           hPutStrLn stderr $ unwords [ "completely resolve", show v, "count", show c ]
+           later <- cont $ others v <> resolve v
+           return $ fmap
+                    ( \ m -> M.insert v (reconstruct v m) m)
+                    later
+
+-- | map each var to list of clauses where it occurs 
+occurrences :: Bool -> CNF -> M.Map Variable [Clause]
+occurrences polarity  =
+  flip Satchmo.Data.foldr M.empty $ \ cl ->
+    M.unionWith (++) $ M.fromList $ do
+      lit <- literals cl
+      guard $ positive lit == polarity
+      return ( variable lit, [cl] )
diff --git a/Satchmo/SAT/CNF.hs b/Satchmo/SAT/CNF.hs
new file mode 100644
--- /dev/null
+++ b/Satchmo/SAT/CNF.hs
@@ -0,0 +1,87 @@
+-- | use this module to get the actual
+-- conjunctive normal form (a list of clauses).
+-- You can then send this to minisat,
+-- and do your own statistics and preprocessing first
+
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE DoAndIfThenElse #-}
+{-# LANGUAGE PatternSignatures #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TemplateHaskell #-}
+
+
+module Satchmo.SAT.CNF
+
+( SAT
+, fresh
+, emit
+, solve
+)
+
+where
+
+import qualified MiniSat as API
+
+import Satchmo.Data
+import Satchmo.Boolean hiding ( not )
+import Satchmo.Code
+import Satchmo.MonadSAT
+import Satchmo.Fourier_Motzkin ( fomo )
+
+import Control.Monad
+import Control.Monad.State.Strict
+import Control.Monad.Reader
+
+import Control.Applicative
+import Control.Lens
+import Data.Monoid
+import Data.Foldable
+import qualified Data.Map.Strict as M
+import System.IO
+
+data S = S { _next :: ! Variable
+           , _output :: ! CNF
+           -- , _assignment :: ! (M.Map Variable Bool)
+           }
+
+$(makeLenses ''S)
+
+newtype SAT a = SAT { unSAT :: StateT S IO a }
+  deriving ( Functor, Applicative, Monad, MonadIO, MonadState S )
+
+instance MonadFix SAT -- dummy
+
+instance MonadSAT SAT where
+  fresh = do
+      x <- get
+      modify ( next %~ succ )
+      return $ literal True $ x ^. next
+
+  emit cl = do      
+      modify ( output %~ ( singleton cl <> ) )
+
+  note msg = liftIO $ hPutStrLn stderr msg
+
+  type Decoder SAT = Reader (M.Map Variable Bool)
+  decode_variable v = do m <- ask ; return $ m M.! v
+      
+instance Decode (Reader (M.Map Variable Bool)) Boolean Bool where
+    decode b = case b of
+        Constant c -> return c
+        Boolean  l -> do 
+            v <- -- decode_variable $ variable l
+              do m <- ask ; return $ M.findWithDefault False ( variable l ) m
+            return $ if positive l then v else not v
+
+solve :: SAT (Decoder SAT a) -> IO (Maybe a)
+solve action = do
+  (a,s) <- runStateT (unSAT action)
+           $ S { _next = 1, _output = cnf [] }
+  mm <- fomo $ s^.output
+  return $ case mm of
+    Nothing -> Nothing
+    Just m -> Just $ runReader a m
+    
diff --git a/Satchmo/SAT/Tmpfile.hs b/Satchmo/SAT/Tmpfile.hs
--- a/Satchmo/SAT/Tmpfile.hs
+++ b/Satchmo/SAT/Tmpfile.hs
@@ -13,7 +13,7 @@
 
 where
 
-import Satchmo.Data
+import Satchmo.Data hiding ( size )
 import Satchmo.Code
 import Satchmo.Boolean
 import Satchmo.Boolean.Data
diff --git a/examples/RamseyFM.hs b/examples/RamseyFM.hs
new file mode 100644
--- /dev/null
+++ b/examples/RamseyFM.hs
@@ -0,0 +1,105 @@
+-- | find colouring without complete subgraphs
+-- example usage: ./dist/build/Ramsey/Ramsey 3 3 3 16
+-- last number is size of graph,
+-- earlier numbers are sizes of forbidden cliques
+
+{-# language PatternSignatures #-}
+
+import Prelude hiding ( not, and, or, product )
+import qualified Prelude
+
+import Satchmo.Relation
+import Satchmo.Code
+import Satchmo.Boolean hiding ( implies )
+import Satchmo.Counting
+
+import qualified Satchmo.Binary as B
+
+import Satchmo.SAT.CNF
+
+import Data.List (sort, tails)
+import qualified Data.Array as A
+import Control.Monad ( guard, when, forM, foldM, void )
+import System.Environment
+import Data.Ix ( range)
+
+
+main :: IO ()
+main = do
+    argv <- getArgs
+    let ns = map read $ case argv of
+          [] -> [ "3", "3", "5" ] -- small numbers, else it will blow up
+          _ -> argv
+        cs = init ns 
+        n = last ns
+    Just ( p : fs ) <- solve $ ramsey cs n
+    forM ( zip [ 1.. ] fs ) $ \ (k, f) -> do 
+        putStrLn $ unwords [ "colour", show k ]
+        printA f
+    putStrLn "with isomorphism" ; printA p
+
+printA :: A.Array (Int,Int) Bool -> IO ()
+printA a = putStrLn $ unlines $ do
+         let ((u,l),(o,r)) = A.bounds a
+         x <- [u .. o]
+         return $ unwords $ do 
+             y <- [ l ..r ]
+             return $ case a A.! (x,y) of
+                  True -> "* " ; False -> ". "
+
+ramsey (cs :: [Int]) (n :: Int) = do
+    fs <- forM cs $ \ c -> 
+         relation ((1 :: Int,1 :: Int),(n,n))
+    
+    p <- relation ((1,1),(n,n))
+    -- forM fs $ isomorphism p
+
+    -- forM fs $ cyclic 3
+
+    when False $ void $ do
+        forM [ 1 .. n ] $ \ x -> 
+            forM [ x + 1 .. n ] $ \ y -> 
+                assertM $ exactly 1 $ 
+                    for fs $ \ f -> f ! (x,y) 
+    when True $ void $ do
+        forM [ 1 .. n ] $ \ x -> 
+            forM [ x + 1 .. n ] $ \ y -> 
+                assert $ for fs $ \ f -> f ! (x,y)
+
+    forM ( zip cs fs ) $ \ (c,f) -> 
+        forM ( cliquesA c [1..n] ) $ \ xs ->
+            assert $ for ( cliquesA 2 xs ) $ \ [x,y] -> not $ f ! (x,y)
+    return $ forM (p : fs) decode
+    
+isomorphism p e = do
+    assertM $ regular 1 p
+    assertM $ regular 1 $ mirror p
+    e' <- foldM product ( mirror p ) [ e, p ]
+    assertM $ implies e e'
+    assertM $ implies e' e
+
+cyclic off f = forM ( indices f ) $ \ (i,j) -> 
+    when ( off < i Prelude.&& i < j ) 
+         $ assert_fun2 (==) ( f!(i,j) ) (f!(i-off,j-off))
+
+cliquesA k xs = 
+      let -- spec:  c!(i,j) == cliques i (drop j xs)
+          bnd = ((0,0),(k, length xs))
+          c = A.array bnd $ do
+            (i,j) <- A.range bnd
+            return ( (i,j)
+                   , if i == 0 then [ [] ]
+                     else if i > length xs - j then []               
+                     else c A.! (i,j+1) 
+                          ++ map (xs !! j : ) ( c A.! (i-1,j+1))
+                   )             
+      in  c A.! (k,0)         
+
+cliques 0 xs = return []
+cliques k xs | k > length xs = []
+cliques k (x:xs) =
+    cliques k xs ++ map (x :) ( cliques (k-1) xs )
+
+for = flip map
+
+assertM this = do x <- this ; assert [x]
diff --git a/satchmo.cabal b/satchmo.cabal
--- a/satchmo.cabal
+++ b/satchmo.cabal
@@ -1,5 +1,5 @@
 Name:           satchmo
-Version:        2.9.6
+Version:        2.9.7
 
 License:        GPL
 License-file:	gpl-2.0.txt
@@ -21,7 +21,7 @@
 Library
     ghc-options: -funbox-strict-fields
     Build-depends:  mtl, process, containers, base == 4.*,
-               array, bytestring, directory, minisat >= 0.1
+        lens, array, bytestring, directory, minisat >= 0.1
     Exposed-modules:
         Satchmo.Data
         -- Satchmo.Data.Default
@@ -55,6 +55,8 @@
         Satchmo.SAT
         Satchmo.SAT.Tmpfile
         Satchmo.SAT.Mini
+        Satchmo.SAT.CNF
+        Satchmo.Fourier_Motzkin
         -- Satchmo.SAT.BS
         -- Satchmo.SAT.Seq
         -- Satchmo.SAT.Sequence
@@ -101,6 +103,12 @@
   Type: exitcode-stdio-1.0
   hs-source-dirs: examples
   Main-Is: Ramsey.hs
+  Build-Depends: base, array, satchmo
+
+Test-Suite RamseyFM
+  Type: exitcode-stdio-1.0
+  hs-source-dirs: examples
+  Main-Is: RamseyFM.hs
   Build-Depends: base, array, satchmo