diff --git a/executable/SequentialMain.hs b/executable/SequentialMain.hs
--- a/executable/SequentialMain.hs
+++ b/executable/SequentialMain.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE CPP, RecordWildCards, FlexibleInstances, PatternGuards, DeriveAnyClass #-}
+{-# LANGUAGE CPP, RecordWildCards, FlexibleInstances, PatternGuards, DeriveAnyClass, RankNTypes #-}
 {-# OPTIONS_GHC -flate-specialise #-}
 module SequentialMain(main) where
 
@@ -49,16 +49,18 @@
     flags_flatten_nonground :: Bool,
     flags_flatten_goals_lightly :: Bool,
     flags_flatten_all :: Bool,
+    flags_flatten_regeneralise :: Bool,
     flags_eliminate :: [String],
     flags_backwards_goal :: Int,
     flags_flatten_backwards_goal :: Int,
     flags_equals_transformation :: Bool,
     flags_distributivity_heuristic :: Bool,
-    flags_kbo_weight0 :: Bool }
+    flags_kbo_weight0 :: Bool,
+    flags_goal_heuristic :: Bool }
 
 parseMainFlags :: OptionParser MainFlags
 parseMainFlags =
-  MainFlags <$> proof <*> trace <*> formal <*> explain <*> flipOrdering <*> giveUp <*> flatten <*> flattenNonGround <*> flattenLightly <*> flattenAll <*> eliminate <*> backwardsGoal <*> flattenBackwardsGoal <*> equalsTransformation <*> distributivityHeuristic <*> kboWeight0
+  MainFlags <$> proof <*> trace <*> formal <*> explain <*> flipOrdering <*> giveUp <*> flatten <*> flattenNonGround <*> flattenLightly <*> flattenAll <*> flattenRegeneralise <*> eliminate <*> backwardsGoal <*> flattenBackwardsGoal <*> equalsTransformation <*> distributivityHeuristic <*> kboWeight0 <*> goalHeuristic
   where
     proof =
       inGroup "Output options" $
@@ -106,6 +108,10 @@
       expert $
       inGroup "Completion heuristics" $
       bool "flatten" ["Flatten all clauses by adding new axioms (off by default)."] False
+    flattenRegeneralise =
+      expert $
+      inGroup "Completion heuristics" $
+      bool "flatten-regeneralise" ["Regeneralise rules involving flattened goal terms (off by default)."] False
     backwardsGoal =
       expert $
       inGroup "Completion heuristics" $
@@ -122,6 +128,10 @@
       expert $
       inGroup "Completion heuristics" $
       bool "distributivity-heuristic" ["Treat distributive operators specially (off by default)."] False
+    goalHeuristic =
+      expert $
+      inGroup "Completion heuristics" $
+      bool "goal-heuristic" ["Use the CP weighting heuristic from Anantharaman and Andrianarievelo (off by default)."] False
     eliminate =
       inGroup "Proof presentation" $
       concat <$>
@@ -136,10 +146,10 @@
 
 parseConfig :: OptionParser (Config Constant)
 parseConfig =
-  Config <$> maxSize <*> maxCPs <*> maxCPDepth <*> simplify <*> normPercent <*> cpSampleSize <*> cpRenormaliseThreshold <*> set_join_goals <*> always_simplify <*> complete_subsets <*>
-    (CP.Config <$> lweight <*> rweight <*> funweight <*> varweight <*> depthweight <*> dupcost <*> dupfactor) <*>
+  Config <$> maxSize <*> maxCPs <*> maxCPDepth <*> maxRules <*> simplify <*> normPercent <*> cpSampleSize <*> cpRenormaliseThreshold <*> set_join_goals <*> always_simplify <*> complete_subsets <*>
+    pure undefined <*> -- scoring function - filled in later, in runTwee
     (Join.Config <$> ground_join <*> connectedness <*> ground_connectedness <*> set_join) <*>
-    (Proof.Config <$> all_lemmas <*> flat_proof <*> ground_proof <*> show_instances <*> colour <*> show_axiom_uses)
+    (Proof.Config <$> all_lemmas <*> flat_proof <*> ground_proof <*> show_instances <*> colour <*> show_axiom_uses) <*> pure [] <*> randomMode <*> randomModeGoalDirected <*> randomModeSimple <*> randomModeBestOf <*> alwaysComplete
   where
     maxSize =
       inGroup "Resource limits" $
@@ -151,6 +161,9 @@
     maxCPDepth =
       inGroup "Resource limits" $
       flag "max-cp-depth" ["Only consider critical pairs up to this depth (unlimited by default)."] maxBound argNum
+    maxRules =
+      inGroup "Resource limits" $
+      flag "max-rules" ["Give up after generating this many rules (unlimited by default)."] maxBound argNum
     simplify =
       expert $
       inGroup "Completion heuristics" $
@@ -169,34 +182,6 @@
       expert $
       inGroup "Completion heuristics" $
       defaultFlag "cp-renormalise-threshold" "Trigger renormalisation when this percentage of CPs can be simplified" cfg_renormalise_threshold argNum
-    lweight =
-      expert $
-      inGroup "Critical pair weighting heuristics" $
-      defaultFlag "lhs-weight" "Weight given to LHS of critical pair" (CP.cfg_lhsweight . cfg_critical_pairs) argNum
-    rweight =
-      expert $
-      inGroup "Critical pair weighting heuristics" $
-      defaultFlag "rhs-weight" "Weight given to RHS of critical pair" (CP.cfg_rhsweight . cfg_critical_pairs) argNum
-    funweight =
-      expert $
-      inGroup "Critical pair weighting heuristics" $
-      defaultFlag "fun-weight" "Weight given to function symbols" (CP.cfg_funweight . cfg_critical_pairs) argNum
-    varweight =
-      expert $
-      inGroup "Critical pair weighting heuristics" $
-      defaultFlag "var-weight" "Weight given to variable symbols" (CP.cfg_varweight . cfg_critical_pairs) argNum
-    depthweight =
-      expert $
-      inGroup "Critical pair weighting heuristics" $
-      defaultFlag "depth-weight" "Weight given to critical pair depth" (CP.cfg_depthweight . cfg_critical_pairs) argNum
-    dupcost =
-      expert $
-      inGroup "Critical pair weighting heuristics" $
-      defaultFlag "dup-cost" "Cost of duplicate subterms" (CP.cfg_dupcost . cfg_critical_pairs) argNum
-    dupfactor =
-      expert $
-      inGroup "Critical pair weighting heuristics" $
-      defaultFlag "dup-factor" "Size factor of duplicate subterms" (CP.cfg_dupfactor . cfg_critical_pairs) argNum
     ground_join =
       expert $
       inGroup "Critical pair joining heuristics" $
@@ -272,6 +257,32 @@
         (splitOn "," <$> arg "<axioms>" "expected a list of axiom names" Just)
       where
         interpret xss ax = axiom_name ax `elem` xss || "all" `elem` xss
+    randomMode =
+      expert $
+      inGroup "Completion heuristics" $
+      bool "random-mode"
+        ["Use random testing to find suitable CPs (doesn't work yet!) (off by default)."]
+        False
+    randomModeGoalDirected =
+      expert $
+      inGroup "Completion heuristics" $
+      bool "random-mode-goal-directed"
+        ["Use goal-direction in --random-mode (off by default)."]
+        False
+    randomModeSimple =
+      expert $
+      inGroup "Completion heuristics" $
+      bool "random-mode-simple"
+        ["Use simple version of --random-mode (off by default)."]
+        False
+    randomModeBestOf =
+      inGroup "Completion heuristics" $
+      defaultFlag "random-mode-best-of" "Generate this many critical pairs at a time and pick the best one" cfg_random_mode_best_of argNum
+    alwaysComplete =
+      inGroup "Input and clausifier options" $
+      bool "complete"
+        ["Don't stop until the rewrite system is confluent"]
+        False
     colour = fromMaybe <$> io colourSupported <*> colourFlag
     colourFlag =
       inGroup "Proof presentation" $
@@ -287,11 +298,50 @@
       liftM2 (&&) (hSupportsANSIColor stdout)
         (return (setSGRCode [] /= "")) -- Check for Windows terminal not supporting ANSI
 
+    defaultFlag :: Show a => String -> String -> (Config Constant -> a) -> ArgParser a -> OptionParser a
     defaultFlag name desc field parser =
       flag name [desc ++ " (" ++ show def ++ " by default)."] def parser
       where
         def = field defaultConfig
 
+parseCPConfig :: OptionParser CP.Config
+parseCPConfig =
+  CP.Config <$> lweight <*> rweight <*> funweight <*> varweight <*> depthweight <*> dupcost <*> dupfactor
+  where
+    lweight =
+      expert $
+      inGroup "Critical pair weighting heuristics" $
+      defaultFlag "lhs-weight" "Weight given to LHS of critical pair" CP.cfg_lhsweight argNum
+    rweight =
+      expert $
+      inGroup "Critical pair weighting heuristics" $
+      defaultFlag "rhs-weight" "Weight given to RHS of critical pair" CP.cfg_rhsweight argNum
+    funweight =
+      expert $
+      inGroup "Critical pair weighting heuristics" $
+      defaultFlag "fun-weight" "Weight given to function symbols" CP.cfg_funweight argNum
+    varweight =
+      expert $
+      inGroup "Critical pair weighting heuristics" $
+      defaultFlag "var-weight" "Weight given to variable symbols" CP.cfg_varweight argNum
+    depthweight =
+      expert $
+      inGroup "Critical pair weighting heuristics" $
+      defaultFlag "depth-weight" "Weight given to critical pair depth" CP.cfg_depthweight argNum
+    dupcost =
+      expert $
+      inGroup "Critical pair weighting heuristics" $
+      defaultFlag "dup-cost" "Cost of duplicate subterms" CP.cfg_dupcost argNum
+    dupfactor =
+      expert $
+      inGroup "Critical pair weighting heuristics" $
+      defaultFlag "dup-factor" "Size factor of duplicate subterms" CP.cfg_dupfactor argNum
+
+    defaultFlag name desc field parser =
+      flag name [desc ++ " (" ++ show def ++ " by default)."] def parser
+      where
+        def = field CP.defaultConfig
+
 parsePrecedence :: OptionParser [String]
 parsePrecedence =
   expert $
@@ -612,8 +662,8 @@
       return $ Left (pre inp (Jukebox.Var ctx_var, ctx_minimal :@: []))
     identify inp = Left inp
 
-runTwee :: GlobalFlags -> TSTPFlags -> HornFlags -> [String] -> Config Constant -> MainFlags -> (IO () -> IO ()) -> Problem Clause -> IO Answer
-runTwee globals (TSTPFlags tstp) horn precedence config flags@MainFlags{..} later obligs = {-# SCC runTwee #-} do
+runTwee :: GlobalFlags -> TSTPFlags -> HornFlags -> [String] -> Config Constant -> CP.Config -> MainFlags -> (IO () -> IO ()) -> Problem Clause -> IO Answer
+runTwee globals (TSTPFlags tstp) horn precedence config0 cpConfig flags@MainFlags{..} later obligs = {-# SCC runTwee #-} do
   let
     -- Encode whatever needs encoding in the problem
     obligs1
@@ -651,9 +701,9 @@
         (isType c)
         (isNothing (elemIndex (base c) precedence))
         (fmap negate (elemIndex (base c) precedence))
-        (maybeNegate (Map.findWithDefault 0 c occs))
+        (maybeNegate (Map.findWithDefault 0 c funOccs))
     maybeNegate = if flags_flip_ordering then negate else id
-    occs = funsOcc prob
+    funOccs = funsOcc prob
 
     -- Translate everything to Twee.
     toEquation (t, u) =
@@ -681,6 +731,28 @@
     isDefinition Input{source = Unknown} = True
     isDefinition inp = tag inp `elem` flags_eliminate
 
+  -- Compute CP scoring heuristic
+  let
+    goalNests = nests (map goal_eqn goals)
+    goalOccs = occs (map goal_eqn goals)
+    score depth eqn
+      | flags_goal_heuristic =
+        fromIntegral (CP.score cpConfig depth eqn) *
+        product
+          [ pos (IntMap.findWithDefault 0 f eqnNests - IntMap.findWithDefault 0 f goalNests) *
+            pos (IntMap.findWithDefault 0 f eqnOccs - IntMap.findWithDefault 0 f goalOccs)
+          | f <- IntMap.keys eqnNests ] -- skip constants
+      | otherwise = 
+        fromIntegral (CP.score cpConfig depth eqn)
+      where
+        eqnNests = nests eqn
+        eqnOccs = occs eqn
+
+        pos :: Int -> Float
+        pos n = if n <= 0 then 1 else fromIntegral n+1
+    config = config0 { cfg_score_cp = score, cfg_eliminate_axioms = if flags_flatten_regeneralise then defs else [] }
+
+  let
     withGoals = foldl' (addGoal config) (initialState config) goals
     withAxioms = foldl' (addAxiom config) withGoals axioms
     withBackwardsGoal = foldn rewriteGoalsBackwards withAxioms flags_backwards_goal
@@ -982,6 +1054,7 @@
            (combine <$>
              expert hornToUnitBox <*>
              parseConfig <*>
+             parseCPConfig <*>
              parseMainFlags <*>
              (toFormulasBox =>>=
               expert (toFof <$> clausifyBox <*> pure (tags True)) =>>=
@@ -989,7 +1062,7 @@
              (runTwee <$> globalFlags <*> tstpFlags <*> expert hornFlags <*> parsePrecedence)))
   profile
   where
-    combine horn config main encode prove later prob0 = do
+    combine horn config cpConfig main encode prove later prob0 = do
       res <- horn prob0
       case res of
         Left ans -> return ans
@@ -1000,4 +1073,4 @@
             isUnitEquality _ = False
             isUnit = all isUnitEquality (map (toLiterals . what) prob0)
             main' = if isUnit then main{flags_explain_encoding = False} else main{flags_formal_proof = False}
-          encode prob >>= prove config main' later
+          encode prob >>= prove config cpConfig main' later
diff --git a/misc/Test.hs b/misc/Test.hs
--- a/misc/Test.hs
+++ b/misc/Test.hs
@@ -1,5 +1,5 @@
 {-# LANGUAGE TemplateHaskell, FlexibleInstances, FlexibleContexts, UndecidableInstances, StandaloneDeriving, ScopedTypeVariables, TupleSections, DeriveGeneric, DerivingVia, DeriveAnyClass #-}
-module Test where
+module Main where
 
 import Twee.Constraints
 import Twee.Term hiding (subst, canonicalise, F)
@@ -18,33 +18,48 @@
 import qualified Data.Map as Map
 import Data.Maybe
 import Data.Ord
-import Data.List
+import Data.List hiding (singleton)
 import Data.Typeable
 import qualified Twee.Index as Index
 import Data.Int
 import GHC.Generics
 import Twee.Utils
+import qualified Data.IntMap as M
+import qualified Twee.Index as Index
 
-data Func = F Int Integer deriving (Eq, Ord, Show)
-  deriving Labelled via (AutoLabel Func)
+data Func = F Int Integer deriving (Eq, Ord, Show, Labelled)
 
-instance Pretty Func where pPrint (F f _) = text "f" <#> int f
+instance Pretty Func where
+  pPrint (F 3 _) = text "a"
+  pPrint (F 4 _) = text "b"
+  pPrint (F 5 _) = text "zero"
+  pPrint (F 6 _) = text "plus"
+  pPrint (F 7 _) = text "times"
+  pPrint (F f _) = text "f" <#> int f
 instance PrettyTerm Func
 instance Arbitrary (Subst Func) where
   arbitrary = fmap fromJust (fmap listToSubst (liftM2 zip (fmap nub arbitrary) (infiniteListOf arbitrary)))
 instance Arbitrary Func where
-  arbitrary = F <$> choose (1, 1) <*> choose (1, 3)
+  arbitrary = F <$> choose (0, 2) <*> choose (1, 3)
 instance Minimal Func where
   minimal = fun (F 0 1)
 instance Ord.Sized Func where size (F _ n) = n
 instance Ord.Weighted Func where argWeight _ = 1
+class Arity f where
+  arity :: f -> Int
 instance Arity Func where
   arity (F 0 _) = 0
-  arity (F 1 _) = 2
+  arity (F 1 _) = 1
+  arity (F 2 _) = 2
+  arity (F 3 _) = 0 -- a
+  arity (F 4 _) = 0 -- b
+  arity (F 5 _) = 0 -- zero
+  arity (F 6 _) = 2 -- plus
+  arity (F 7 _) = 2 -- times
 instance EqualsBonus Func
 
 instance Arbitrary Var where arbitrary = fmap V (choose (0, 3))
-instance (Labelled f, Ord f, Typeable f, Arbitrary f) => Arbitrary (Fun f) where
+instance (Labelled f, Ord f, Typeable f, Arbitrary f, Arity f) => Arbitrary (Fun f) where
   arbitrary = fmap fun arbitrary
 
 instance (Labelled f, Ord f, Typeable f, Arbitrary f, Arity f) => Arbitrary (Term f) where
@@ -52,7 +67,7 @@
     sized $ \n ->
       oneof $
         [ build <$> var <$> arbitrary ] ++
-        [ do { f <- arbitrary; build <$> app f <$> vectorOf (arity f) (resize ((n-1) `div` arity f) arbitrary :: Gen (Term f)) } | n > 0 ]
+        [ do { f <- arbitrary; build <$> app (fun f) <$> vectorOf (arity f) (resize ((n-1) `div` arity f) arbitrary :: Gen (Term f)) } | n > 0 ]
   shrink (App f ts0) =
     ts ++ (build <$> app f <$> shrinkOne ts)
     where
@@ -63,6 +78,10 @@
         [ x:ys | ys <- shrinkOne xs ]
   shrink _ = []
 
+instance (Labelled f, Ord f, Typeable f, Arbitrary f, Arity f) => Arbitrary (TermList f) where
+  arbitrary = buildList <$> listOf (arbitrary :: Gen (Term f))
+  shrink = map buildList . shrink . unpack
+
 data Pair f = Pair (Term f) (Term f) deriving Show
 
 instance (Labelled f, Ord f, Typeable f, Arbitrary f, Arity f) => Arbitrary (Pair f) where
@@ -221,8 +240,95 @@
   counterexample (show eq) $
   Ord.size (eqn_lhs eq') >= Ord.size (eqn_rhs eq')
 
+--t :: Term Func
+--t = build (app (fun (F 0)) [app (fun (F 1)) [var (V 0), var (V 1)], var (V 2)])
+
+-- Define 'nest' from Fuchs "The application of goal-oriented heuristics...",
+-- then refine it to a more efficient version
+nestf :: Func -> Term Func -> Int
+nestf f _ | arity f == 0 = 0
+nestf f t = hnest (fun f) t 0 0
+  where
+    hnest _ (Var _) c a = max c a
+    hnest _ (App _ Empty) c a = max c a
+    hnest f (App g ts) c a
+      | f == g = maximum [hnest f t (c+1) a | t <- unpack ts]
+      | otherwise = maximum [hnest f t 0 (max c a) | t <- unpack ts]
+
+-- a simpler version, to illustrate the meaning
+nestf1 :: Func -> Term Func -> Int
+nestf1 f t = hnest (fun f) t 0
+  where
+    hnest _ (Var _) c = c
+    hnest _ (App _ Empty) c = c
+    hnest f (App g ts) c
+      | f == g = maximum [hnest f t (c+1) | t <- unpack ts]
+      | otherwise = max c (maximum [hnest f t 0 | t <- unpack ts])
+
+-- a more efficient version
+nestf2 :: Func -> Term Func -> Int
+nestf2 f t = hnest (fun f) (singleton t) 0 0
+  where
+    hnest _ Empty c a = max c a
+    hnest f (Cons (Var _) ts) c a = hnest f ts c a
+    hnest f (Cons (App _ Empty) ts) c a = hnest f ts c a
+    hnest f (Cons (App g ts) us) c a
+      | f == g = 
+        let a' = hnest f ts (c+1) a
+        in hnest f us c a'
+      | otherwise =
+        let a' = hnest f ts 0 a
+        in hnest f us c a'
+
+-- a version that does all function symbols at once
+nestf3 :: Term Func -> M.IntMap Int
+nestf3 t = hnest 0 0 M.empty (singleton t)
+  where
+    hnest f c as Empty = M.insertWith max f c as
+    hnest f c as (Cons (Var _) ts) = hnest f c as ts
+    hnest f c as (Cons (App _ Empty) ts) = hnest f c as ts
+    hnest f c as (Cons (App g ts) us) =
+      let as' = hnest (fun_id g) (if f == fun_id g then c+1 else 1) as ts
+      in hnest f c as' us
+
+prop_nest_1 :: Func -> Term Func -> Property
+prop_nest_1 f t = withMaxSuccess 1000000 $ nestf f t === nestf1 f t
+
+prop_nest_2 :: Func -> Term Func -> Property
+prop_nest_2 f t = withMaxSuccess 1000000 $ nestf f t === nestf2 f t
+
+prop_nest_3 :: Func -> Term Func -> Property
+prop_nest_3 f t =
+  withMaxSuccess 1000000 $
+    nestf f t === M.findWithDefault 0 (fun_id (fun f)) (nestf3 t)
+
+prop_nests :: Func -> TermList Func -> Property
+prop_nests f ts =
+  withMaxSuccess 1000000 $
+    maximum (0:map (nestf f) (unpack ts)) ===
+    M.findWithDefault 0 (fun_id (fun f)) (nests ts)
+
 return []
 main = $forAllProperties (quickCheckWithResult stdArgs { maxSuccess = 1000000 })
 
---t :: Term Func
---t = build (app (fun (F 0)) [app (fun (F 1)) [var (V 0), var (V 1)], var (V 2)])
+a = con (fun (F 3 1))
+b = con (fun (F 4 2))
+zero = con (fun (F 5 1))
+plus t u = app (fun (F 6 1)) [t, u]
+times t u = app (fun (F 7 1)) [t, u]
+x = var (V 0)
+y = var (V 1)
+
+axioms = [
+  build (plus x y) ==== plus y x,
+  times zero x ==== zero,
+  plus x zero ==== x ]
+  where
+    t ==== u = build t :=: build u
+
+rules = [orient eq (certify (axiom (Axiom 0 "axiom" eq))) | eq <- axioms]
+
+theIndex = Index.fromList [(lhs r, r) | r <- rules]
+
+term = build (plus (times zero a) b)
+strat = anywhere1 (basic (rewrite reduces theIndex))
diff --git a/tests/LAT078-1.p b/tests/LAT078-1.p
new file mode 100644
--- /dev/null
+++ b/tests/LAT078-1.p
@@ -0,0 +1,38 @@
+%--------------------------------------------------------------------------
+% File     : LAT078-1 : TPTP v9.0.0. Released v2.6.0.
+% Domain   : Lattice Theory (Ortholattices)
+% Problem  : Given single axiom MOL-27B2, prove associativity
+% Version  : [MRV03] (equality) axioms.
+% English  : Given a single axiom candidate MOL-27B2 for modular ortholattices
+%            (MOL) in terms of the Sheffer Stroke, prove a Sheffer stroke form
+%            of associativity.
+
+% Refs     : [MRV03] McCune et al. (2003), Sheffer Stroke Bases for Ortholatt
+% Source   : [MRV03]
+% Names    : MOL-27B2-associativity [MRV03]
+
+% Status   : Unsatisfiable
+% Rating   : 0.91 v8.2.0, 0.96 v8.1.0, 0.95 v7.5.0, 0.96 v7.4.0, 1.00 v7.3.0, 0.95 v7.1.0, 0.94 v7.0.0, 0.95 v6.4.0, 1.00 v2.6.0
+% Syntax   : Number of clauses     :    2 (   2 unt;   0 nHn;   1 RR)
+%            Number of literals    :    2 (   2 equ;   1 neg)
+%            Maximal clause size   :    1 (   1 avg)
+%            Maximal term depth    :    9 (   2 avg)
+%            Number of predicates  :    1 (   0 usr;   0 prp; 2-2 aty)
+%            Number of functors    :    4 (   4 usr;   3 con; 0-2 aty)
+%            Number of variables   :    4 (   1 sgn)
+% SPC      : CNF_UNS_RFO_PEQ_UEQ
+
+% Comments :
+%--------------------------------------------------------------------------
+%----Single axiom MOL-27B2
+cnf(mol_27B2,axiom,
+    f(f(f(f(B,A),f(A,C)),D),f(A,f(f(f(B,f(B,f(f(C,C),A))),A),C))) = A ).
+
+%----Denial of Sheffer stroke associativity
+cnf(associativity,negated_conjecture,
+    f(a,f(f(b,c),f(b,c))) != f(c,f(f(b,a),f(b,a))) ).
+
+%--------------------------------------------------------------------------
+
+cnf(not, axiom,
+    not(X) = f(X,X)).
diff --git a/tests/ROB007-1-a.p b/tests/ROB007-1-a.p
new file mode 100644
--- /dev/null
+++ b/tests/ROB007-1-a.p
@@ -0,0 +1,12 @@
+cnf(commutativity_of_add, axiom, add(X, Y)=add(Y, X)).
+cnf(associativity_of_add, axiom, add(add(X, Y), Z)=add(X, add(Y, Z))).
+cnf(robbins_axiom, axiom, inv(add(inv(add(X, Y)), inv(add(X, inv(Y)))))=X).
+cnf(condition, hypothesis, inv(add(a, b))=inv(b)).
+cnf(prove_huntingtons_axiom, negated_conjecture, add(inv(add(a, inv(b))), inv(add(inv(a), inv(b))))!=b).
+
+cnf(sos04,axiom,(
+    g(A) = inv(add(A,inv(A))) )).
+
+%----Definition of h
+cnf(sos05,axiom,(
+    h(A) = add(A,add(A,add(A,inv(add(A,inv(A)))))))).
diff --git a/tests/ROB007-1.p b/tests/ROB007-1.p
new file mode 100644
--- /dev/null
+++ b/tests/ROB007-1.p
@@ -0,0 +1,5 @@
+cnf(commutativity_of_add, axiom, add(X, Y)=add(Y, X)).
+cnf(associativity_of_add, axiom, add(add(X, Y), Z)=add(X, add(Y, Z))).
+cnf(robbins_axiom, axiom, negate(add(negate(add(X, Y)), negate(add(X, negate(Y)))))=X).
+cnf(condition, hypothesis, negate(add(a, b))=negate(b)).
+cnf(prove_huntingtons_axiom, negated_conjecture, add(negate(add(a, negate(b))), negate(add(negate(a), negate(b))))!=b).
diff --git a/tests/ROB027-1-inv.p b/tests/ROB027-1-inv.p
new file mode 100644
--- /dev/null
+++ b/tests/ROB027-1-inv.p
@@ -0,0 +1,58 @@
+%--------------------------------------------------------------------------
+% File     : ROB027-1 : TPTP v6.3.0. Released v1.2.0.
+% Domain   : Robbins Algebra
+% Problem  : -(-c) = c => Boolean
+% Version  : [Win90] (equality) axioms.
+%            Theorem formulation : Denies Huntington's axiom.
+% English  : If there are elements c and d such that c+d=d, then the
+%            algebra is Boolean.
+
+% Refs     : [HMT71] Henkin et al. (1971), Cylindrical Algebras
+%          : [Win90] Winker (1990), Robbins Algebra: Conditions that make a
+%          : [Wos94] Wos (1994), Two Challenge Problems
+% Source   : [Wos94]
+% Names    : - [Wos94]
+
+% Status   : Open
+% Rating   : 1.00 v2.0.0
+% Syntax   : Number of clauses     :    5 (   0 non-Horn;   5 unit;   2 RR)
+%            Number of atoms       :    5 (   5 equality)
+%            Maximal clause size   :    1 (   1 average)
+%            Number of predicates  :    1 (   0 propositional; 2-2 arity)
+%            Number of functors    :    5 (   3 constant; 0-2 arity)
+%            Number of variables   :    7 (   0 singleton)
+%            Maximal term depth    :    6 (   3 average)
+% SPC      : CNF_UNK_UEQ
+
+% Comments : Commutativity, associativity, and Huntington's axiom
+%            axiomatize Boolean algebra.
+%--------------------------------------------------------------------------
+%----Include axioms for Robbins algebra
+%--------------------------------------------------------------------------
+cnf(commutativity_of_add,axiom,
+    ( add(X,Y) = add(Y,X) )).
+
+cnf(associativity_of_add,axiom,
+    ( add(add(X,Y),Z) = add(X,add(Y,Z)) )).
+
+cnf(robbins_axiom,axiom,
+    ( inv(add(inv(add(X,Y)),inv(add(X,inv(Y))))) = X )).
+
+%--------------------------------------------------------------------------
+%--------------------------------------------------------------------------
+cnf(double_negation,hypothesis,
+    ( inv(inv(c)) = c )).
+
+cnf(prove_huntingtons_axiom,negated_conjecture,
+    add(inv(add(a,inv(b))),inv(add(inv(a),inv(b)))) != b).
+
+%--------------------------------------------------------------------------
+%----Definition of g
+cnf(sos04,axiom,(
+    g(A) = inv(add(A,inv(A))) )).
+
+%----Definition of h
+cnf(sos05,axiom,(
+    h(A) = add(A,add(A,add(A,inv(add(A,inv(A)))))))).
+
+cnf(sos06, axiom, i(X,Y) = inv(add(X, inv(add(X, Y))))).
diff --git a/tests/aim.p b/tests/aim.p
new file mode 100644
--- /dev/null
+++ b/tests/aim.p
@@ -0,0 +1,62 @@
+cnf(left_ident, axiom,
+  '1' * X = X).
+cnf(right_ident, axiom,
+  X * '1' = X).
+cnf(left_division_1, axiom,
+  X \ (X * Y) = Y).
+cnf(left_division_2, axiom,
+  X * (X \ Y) = Y).
+cnf(right_division_1, axiom,
+  (X * Y) / Y = X).
+cnf(right_division_2, axiom,
+  (X / Y) * Y = X).
+cnf(associator, axiom,
+  (X * (Y * Z)) \ ((X * Y) * Z) = a(X,Y,Z)).
+cnf(commutator, axiom,
+  (X * Y) \ (Y * X) = k(Y,X)).
+cnf(l, axiom,
+  (Y * X) \ (Y * (X * U)) = l(U,X,Y)).
+cnf(r, axiom,
+  ((U * X) * Y) / (X * Y) = r(U,X,Y)).
+cnf(t, axiom,
+  X \ (U * X) = t(U,X)).
+cnf(abelian_inner_mapping_1, axiom,
+  t(t(U,X),Y) = t(t(U,Y),X)).
+cnf(abelian_inner_mapping_2, axiom,
+  t(l(U,X,Y),Z) = l(t(U,Z),X,Y)).
+cnf(abelian_inner_mapping_3, axiom,
+  t(r(U,X,Y),Z) = r(t(U,Z),X,Y)).
+cnf(abelian_inner_mapping_4, axiom,
+  l(r(U,X,Y),Z,W) = r(l(U,Z,W),X,Y)).
+cnf(abelian_inner_mapping_5, axiom,
+  l(l(U,X,Y),Z,W) = l(l(U,Z,W),X,Y)).
+cnf(abelian_inner_mapping_6, axiom,
+  r(r(U,X,Y),Z,W) = r(r(U,Z,W),X,Y)).
+
+% aK (or "single-a") goals
+cnf(ka, conjecture,
+  k(a(X,Y,Z),U) = '1').
+cnf(aK1, conjecture,
+  a(k(X,Y),Z,U) = '1').
+cnf(aK2, conjecture,
+  a(X,k(Y,Z),U) = '1').
+cnf(aK3, conjecture,
+  a(X,Y,k(Z,U)) = '1').
+
+% aa (or "double-a") goals
+cnf(aa1, conjecture,
+  a(a(X,Y,Z),U,W) = '1').
+cnf(aa2, conjecture,
+  a(X,a(Y,Z,U),W) = '1').
+cnf(aa3, conjecture,
+  a(X,Y,a(Z,U,W)) = '1').
+
+%cnf(everything, conjecture,
+%  k(a(X,Y,Z),U) = '1' |
+%  a(k(X,Y),Z,U) = '1' |
+%  a(X,k(Y,Z),U) = '1' |
+%  a(X,Y,k(Z,U)) = '1' |
+%  a(a(X,Y,Z),U,W) = '1' |
+%  a(X,a(Y,Z,U),W) = '1' |
+%  a(X,Y,a(Z,U,W)) = '1').
+
diff --git a/tests/aim2.p b/tests/aim2.p
new file mode 100644
--- /dev/null
+++ b/tests/aim2.p
@@ -0,0 +1,64 @@
+cnf(left_ident, axiom,
+  '1' * X = X).
+cnf(right_ident, axiom,
+  X * '1' = X).
+cnf(left_division_1, axiom,
+  X \ (X * Y) = Y).
+cnf(left_division_2, axiom,
+  X * (X \ Y) = Y).
+cnf(right_division_1, axiom,
+  (X * Y) / Y = X).
+cnf(right_division_2, axiom,
+  (X / Y) * Y = X).
+cnf(associator, axiom,
+  (X * (Y * Z)) \ ((X * Y) * Z) = a(X,Y,Z)).
+cnf(commutator, axiom,
+  (X * Y) \ (Y * X) = k(Y,X)).
+cnf(l, axiom,
+  (Y * X) \ (Y * (X * U)) = l(U,X,Y)).
+cnf(r, axiom,
+  ((U * X) * Y) / (X * Y) = r(U,X,Y)).
+cnf(t, axiom,
+  X \ (U * X) = t(U,X)).
+cnf(abelian_inner_mapping_1, axiom,
+  t(t(U,X),Y) = t(t(U,Y),X)).
+cnf(abelian_inner_mapping_2, axiom,
+  t(l(U,X,Y),Z) = l(t(U,Z),X,Y)).
+cnf(abelian_inner_mapping_3, axiom,
+  t(r(U,X,Y),Z) = r(t(U,Z),X,Y)).
+cnf(abelian_inner_mapping_4, axiom,
+  l(r(U,X,Y),Z,W) = r(l(U,Z,W),X,Y)).
+cnf(abelian_inner_mapping_5, axiom,
+  l(l(U,X,Y),Z,W) = l(l(U,Z,W),X,Y)).
+cnf(abelian_inner_mapping_6, axiom,
+  r(r(U,X,Y),Z,W) = r(r(U,Z,W),X,Y)).
+
+% aK (or "single-a") goals
+cnf(ka, conjecture,
+  k(a(X,Y,Z),U) = '1').
+cnf(aK1, conjecture,
+  a(k(X,Y),Z,U) = '1').
+cnf(aK2, conjecture,
+  a(X,k(Y,Z),U) = '1').
+cnf(aK3, conjecture,
+  a(X,Y,k(Z,U)) = '1').
+
+% aa (or "double-a") goals
+cnf(aa1, conjecture,
+  a(a(X,Y,Z),U,W) = '1').
+cnf(aa2, conjecture,
+  a(X,a(Y,Z,U),W) = '1').
+cnf(aa3, conjecture,
+  a(X,Y,a(Z,U,W)) = '1').
+
+%cnf(everything, conjecture,
+%  k(a(X,Y,Z),U) = '1' |
+%  a(k(X,Y),Z,U) = '1' |
+%  a(X,k(Y,Z),U) = '1' |
+%  a(X,Y,k(Z,U)) = '1' |
+%  a(a(X,Y,Z),U,W) = '1' |
+%  a(X,a(Y,Z,U),W) = '1' |
+%  a(X,Y,a(Z,U,W)) = '1').
+
+
+cnf(bonus, axiom, (X * (Y / X)) \ X = Y \ (Y / (Y / X))).
diff --git a/tests/diff2.p b/tests/diff2.p
new file mode 100644
--- /dev/null
+++ b/tests/diff2.p
@@ -0,0 +1,34 @@
+cnf('x\\(y\\x)=x', axiom,
+    X \ (Y \ X) = X).
+cnf('x\\(x\\y)=y\\(y\\x)', axiom,
+    X \ (X \ Y) = Y \ (Y \ X)).
+cnf('(x\\y)\\z=(x\\z)\\(y\\z)', axiom,
+    (X \ Y) \ Z = (X \ Z) \ (Y \ Z)).
+
+cnf(empty, axiom,
+    X \ empty = X).
+
+cnf(equals, conjecture,
+    (X \ Y = empty & Y \ X = empty) => X = Y).
+
+cnf(union, axiom,
+    X \ union(Y, Z) = (X \ Y) \ Z).
+
+cnf(union, conjecture,
+    union(a,b) = union(b,a)).
+cnf(union, conjecture,
+    union(a,a) = a).
+cnf(union, conjecture,
+    union(a,union(b,c)) = union(union(a,b),c)).
+
+cnf(intersection, axiom,
+    intersection(X, Y) = X \ (X \ Y)).
+
+cnf(intersection, conjecture,
+    intersection(a,b) = intersection(b,a)).
+cnf(intersection, conjecture,
+    intersection(a,a) = a).
+cnf(intersection, conjecture,
+    intersection(a,intersection(b,c)) = intersection(intersection(a,b),c)).
+cnf(intersection, conjecture,
+    intersection(X, Y) = union(X,Y) \ union(X \ Y, Y \ X)).
diff --git a/tests/filter.p b/tests/filter.p
new file mode 100644
--- /dev/null
+++ b/tests/filter.p
@@ -0,0 +1,59 @@
+fof('associativity of ∘', axiom,
+    ![F, G, H]:
+    F ∘ (G ∘ H) = (F ∘ G) ∘ H).
+
+fof('∘ identity', axiom,
+    ![F]:
+    id ∘ F = F).
+
+fof('∘ identity', axiom,
+    ![F]:
+    F ∘ id = F).
+
+fof('map functor', axiom,
+    ![F, G]:
+    map(F) ∘ map(G) = map(F ∘ G)).
+
+fof('map functor', axiom,
+    map(id) = id).
+
+fof('naturality of concat', axiom,
+    ![F]:
+    map(F) ∘ concat = concat ∘ map(map(F))).
+
+fof('defn filter', axiom,
+    ![P]:
+    filter(P) = concat ∘ map(test(P))).
+
+% test(P) = \x -> if P(x) then [x] else []
+
+fof('test property', axiom,
+    ![P, F]:
+    test(P) ∘ F =
+    map(F) ∘ test(P ∘ F)).
+
+fof('map/filter', conjecture,
+    ![P, F]:
+    filter(P) ∘ map(F) = map(F) ∘ filter(P ∘ F)).
+
+
+% cond(P, F, G) = \x -> if P(x) then F(x) else G(x)
+
+%fof('test defn', axiom,
+%    ![P]:
+%    test(P) = cond(P, unit, nil)).
+%fof('cond ∘', axiom,
+%    ![F, P, G, H]:
+%    F ∘ cond(P, G, H) = cond(P, F ∘ G, F ∘ H)).
+%fof('cond ∘', axiom,
+%    ![F, P, G, H]:
+%    cond(P, G, H) ∘ F = cond(P ∘ F, G ∘ F, H ∘ F)).
+%fof('nil', axiom,
+%    ![F]:
+%    nil ∘ F = nil).
+%fof('nil', axiom,
+%    ![F]:
+%    map(F) ∘ nil = nil).
+%fof('unit', axiom,
+%    ![F]:
+%    map(F) ∘ unit = unit ∘ F).
diff --git a/tests/filter2.p b/tests/filter2.p
new file mode 100644
--- /dev/null
+++ b/tests/filter2.p
@@ -0,0 +1,59 @@
+fof('associativity of ∘', axiom,
+    ![F, G, H]:
+    F ∘ (G ∘ H) = (F ∘ G) ∘ H).
+
+fof('∘ identity', axiom,
+    ![F]:
+    id ∘ F = F).
+
+fof('∘ identity', axiom,
+    ![F]:
+    F ∘ id = F).
+
+fof('map functor', axiom,
+    ![F, G]:
+    map(F) ∘ map(G) = map(F ∘ G)).
+
+fof('map functor', axiom,
+    map(id) = id).
+
+fof('naturality of concat', axiom,
+    ![F]:
+    map(F) ∘ concat = concat ∘ map(map(F))).
+
+fof('defn filter', axiom,
+    ![P]:
+    filter(P) = concat ∘ map(test(P))).
+
+% test(P) = \x -> if P(x) then [x] else []
+
+%fof('test property', axiom,
+%    ![P, F]:
+%    test(P) ∘ F =
+%    map(F) ∘ test(P ∘ F)).
+
+fof('map/filter', conjecture,
+    ![P, F]:
+    filter(P) ∘ map(F) = map(F) ∘ filter(P ∘ F)).
+
+
+% cond(P, F, G) = \x -> if P(x) then F(x) else G(x)
+
+fof('test defn', axiom,
+    ![P]:
+    test(P) = cond(P, unit, nil)).
+fof('cond ∘', axiom,
+    ![F, P, G, H]:
+    F ∘ cond(P, G, H) = cond(P, F ∘ G, F ∘ H)).
+fof('cond ∘', axiom,
+    ![F, P, G, H]:
+    cond(P, G, H) ∘ F = cond(P ∘ F, G ∘ F, H ∘ F)).
+fof('nil', axiom,
+    ![F]:
+    nil ∘ F = nil).
+fof('nil', axiom,
+    ![F]:
+    map(F) ∘ nil = nil).
+fof('unit', axiom,
+    ![F]:
+    map(F) ∘ unit = unit ∘ F).
diff --git a/tests/lukasiewicz2.p b/tests/lukasiewicz2.p
new file mode 100644
--- /dev/null
+++ b/tests/lukasiewicz2.p
@@ -0,0 +1,5 @@
+cnf(detachment, axiom, (p(X) & p(i(X,Y))) => p(Y)).
+cnf(lukasiewicz, axiom, p(i(i(i(P,Q),R),i(i(R,P),i(S,P))))).
+cnf(simp, axiom, p(i(P, i(Q, Q)))).
+cnf(peirce, axiom, p(i(i(i(P,Q),P),P))).
+cnf(syll, conjecture, p(i(i(a,b),i(i(b,c),i(a,c))))).
diff --git a/tests/p.p b/tests/p.p
new file mode 100644
--- /dev/null
+++ b/tests/p.p
@@ -0,0 +1,11 @@
+cnf(a, axiom, p(X)!=true | p(s(X))!=true).
+cnf(a, axiom, p(X)!=false | p(s(X))!=false).
+cnf(a, axiom, p(a)=true).
+cnf(a, axiom, p(s(s(a)))!=true).
+cnf(a, axiom, true!=false).
+
+cnf(p, axiom, p(a)=true).
+cnf(p, axiom, p(s(a))=true).
+cnf(p, axiom, p(s(s(a)))=false).
+cnf(p, axiom, p(s(s(s(a))))=true).
+cnf(p, axiom, p(s(s(s(X))))=false => p(s(s(s(s(X)))))=true).
diff --git a/tests/regexp.p b/tests/regexp.p
new file mode 100644
--- /dev/null
+++ b/tests/regexp.p
@@ -0,0 +1,54 @@
+%% and, or
+cnf(def, axiom, and(true,B) = B).
+cnf(def, axiom, and(false,B) = false).
+cnf(def, axiom, and(X,Y) = and(Y,X)).
+
+cnf(def, axiom, or(true,B) = true).
+cnf(def, axiom, or(false,B) = B).
+cnf(def, axiom, or(X,Y) = or(Y,X)).
+
+%% eq
+cnf(def, axiom, eq(X,X) = true).
+cnf(def, axiom, eq(X,Y) = eq(Y,X)).
+cnf(def, axiom, eq(a,b) = false).
+cnf(def, axiom, eq(a,c) = false).
+cnf(def, axiom, eq(b,c) = false).
+
+%% haseps
+cnf(def, axiom, haseps(atom(A)) = false).
+cnf(def, axiom, haseps(zero) = false).
+cnf(def, axiom, haseps(eps) = true).
+cnf(def, axiom, haseps(plus(P,Q)) = or(haseps(P),haseps(Q))).
+cnf(def, axiom, haseps(seq(P,Q)) = and(haseps(P),haseps(Q))).
+cnf(def, axiom, haseps(star(P)) = true).
+
+%% step
+cnf(def, axiom, step(atom(A),A) = eps).
+cnf(def, axiom, eq(A,B) = false => step(atom(A),B) = zero).
+cnf(def, axiom, step(zero,B) = zero).
+cnf(def, axiom, step(eps,B) = zero).
+cnf(def, axiom, step(plus(P,Q),B) = plus(step(P,B),step(Q,B))).
+cnf(def, axiom, haseps(P) = true => step(seq(P,Q),B) = plus(seq(step(P,B),Q),step(Q,B))).
+cnf(def, axiom, haseps(P) = false => step(seq(P,Q),B) = plus(seq(step(P,B),Q),zero)).
+cnf(def, axiom, step(star(P),B) = seq(step(P,B),star(P))).
+
+%% rec
+cnf(def, axiom, rec(P,nil) = haseps(P)).
+cnf(def, axiom, rec(P,cons(A,As)) = rec(step(P,A),As)).
+
+%% question
+cnf(hypothesis, axiom, rec(seq(P,Q), As) = rec(seq(Q,P), As)).
+cnf(goal, axiom, true != false).
+
+%cnf(a, axiom, atom(A) != zero & atom(A) != eps & atom(A) != plus(P, Q) & atom(A) != seq(P, Q) & atom(A) != star(P)).
+%cnf(a, axiom, zero != eps & zero != plus(P, Q) & zero != seq(P, Q) & zero != star(P)).
+%cnf(a, axiom, eps != plus(P, Q) & eps != seq(P, Q) & eps != star(P)).
+%cnf(a, axiom, plus(P, Q) != seq(P, Q) & plus(P, Q) != star(P)).
+%cnf(a, axiom, seq(P, Q) != star(P)).
+%cnf(a, axiom, un_atom(atom(A)) = A).
+%cnf(a, axiom, un_plus_1(plus(P, Q)) = P).
+%cnf(a, axiom, un_plus_2(plus(P, Q)) = Q).
+%cnf(a, axiom, un_seq_1(seq(P, Q)) = P).
+%cnf(a, axiom, un_seq_2(seq(P, Q)) = Q).
+%cnf(a, axiom, un_star(star(P)) = P).
+%cnf(a, axiom, a != b & b != c & a != c).
diff --git a/tests/sudoku.p b/tests/sudoku.p
new file mode 100644
--- /dev/null
+++ b/tests/sudoku.p
@@ -0,0 +1,39 @@
+cnf('associativity of ∘', axiom,
+    F ∘ (G ∘ H) = (F ∘ G) ∘ H).
+
+cnf('∘ identity', axiom,
+    id ∘ F = F).
+
+cnf('∘ identity', axiom,
+    F ∘ id = F).
+
+cnf('map functor', axiom,
+    map(F) ∘ map(G) = map(F ∘ G)).
+
+cnf('map functor', axiom,
+    map(id) = id).
+
+cnf('defn pruneBy', axiom,
+    pruneBy(F) = F ∘ (map(pruneRow) ∘ F)).
+
+cnf('defn expand', axiom,
+    expand = product ∘ map(product)).
+
+cnf('expand after boxs', axiom,
+    expand ∘ boxs = map(boxs) ∘ expand).
+
+cnf('filter with boxs', axiom,
+    filter (P ∘ boxs) = map(boxs) ∘ (filter(P) ∘ map(boxs))).
+
+cnf('boxs involution', axiom,
+    boxs ∘ boxs = id).
+
+cnf('filter after product', axiom,
+    filter(all(P)) ∘ product = product ∘ map(filter(P))).
+
+cnf('law of pruneRow', axiom,
+    filter(nodups) ∘ (product ∘ pruneRow) = filter(nodups) ∘ product).
+
+cnf('conjecture', conjecture,
+    filter(all(nodups) ∘ boxs) ∘ (expand ∘ pruneBy(boxs)) =
+    filter(all(nodups) ∘ boxs) ∘ expand).
diff --git a/tests/sudoku2.p b/tests/sudoku2.p
new file mode 100644
--- /dev/null
+++ b/tests/sudoku2.p
@@ -0,0 +1,44 @@
+cnf('associativity of ∘', axiom,
+    F ∘ (G ∘ H) = (F ∘ G) ∘ H).
+
+cnf('∘ identity', axiom,
+    id ∘ F = F).
+
+cnf('∘ identity', axiom,
+    F ∘ id = F).
+
+cnf('map functor', axiom,
+    map(F) ∘ map(G) = map(F ∘ G)).
+
+cnf('map functor', axiom,
+    map(id) = id).
+
+cnf('defn pruneBy', axiom,
+    pruneBy(F) = F ∘ (map(pruneRow) ∘ F)).
+
+cnf('defn expand', axiom,
+    expand = product ∘ map(product)).
+
+cnf('expand after boxs', axiom,
+    expand ∘ boxs = map(boxs) ∘ expand).
+
+cnf('filter with boxs', axiom,
+    filter (P ∘ boxs) = map(boxs) ∘ (filter(P) ∘ map(boxs))).
+
+cnf('boxs involution', axiom,
+    boxs ∘ boxs = id).
+
+cnf('filter after product', axiom,
+    filter(all(P)) ∘ product = product ∘ map(filter(P))).
+
+cnf('law of pruneRow', axiom,
+    filter(nodups) ∘ (product ∘ pruneRow) = filter(nodups) ∘ product).
+
+cnf('lhs', axiom,
+    lhs = filter(all(nodups) ∘ boxs) ∘ (expand ∘ pruneBy(boxs))).
+
+cnf('rhs', axiom,
+    rhs = filter(all(nodups) ∘ boxs) ∘ expand).
+
+cnf('conjecture', conjecture,
+    lhs = rhs).
diff --git a/tests/sudoku3.p b/tests/sudoku3.p
new file mode 100644
--- /dev/null
+++ b/tests/sudoku3.p
@@ -0,0 +1,42 @@
+cnf('associativity of ∘', axiom,
+    F ∘ (G ∘ H) = (F ∘ G) ∘ H).
+
+cnf('∘ identity', axiom,
+    id ∘ F = F).
+
+cnf('∘ identity', axiom,
+    F ∘ id = F).
+
+cnf('map functor', axiom,
+    map(F) ∘ map(G) = map(F ∘ G)).
+
+cnf('map functor', axiom,
+    map(id) = id).
+
+cnf('defn pruneBy', axiom,
+    pruneBy(F) = F ∘ (map(pruneRow) ∘ F)).
+
+cnf('defn expand', axiom,
+    expand = product ∘ map(product)).
+
+cnf('expand after boxs', axiom,
+    expand ∘ boxs = map(boxs) ∘ expand).
+
+cnf('filter with boxs', axiom,
+    filter (P ∘ boxs) = map(boxs) ∘ (filter(P) ∘ map(boxs))).
+
+cnf('boxs involution', axiom,
+    boxs ∘ boxs = id).
+
+cnf('filter after product', axiom,
+    filter(all(P)) ∘ product = product ∘ map(filter(P))).
+
+cnf('law of pruneRow', axiom,
+    filter(nodups) ∘ (product ∘ pruneRow) = filter(nodups) ∘ product).
+
+cnf('map/filter', axiom,
+    filter(P) ∘ map(F) = map(F) ∘ filter(P ∘ F)).
+
+cnf('conjecture', conjecture,
+    filter(all(nodups) ∘ boxs) ∘ (expand ∘ pruneBy(boxs)) =
+    filter(all(nodups) ∘ boxs) ∘ expand).
diff --git a/tests/sudoku4.p b/tests/sudoku4.p
new file mode 100644
--- /dev/null
+++ b/tests/sudoku4.p
@@ -0,0 +1,45 @@
+fof('associativity of ∘', axiom,
+    ![F,G,H]: F ∘ (G ∘ H) = (F ∘ G) ∘ H).
+
+fof('∘ identity', axiom,
+    ![F]: id ∘ F = F).
+
+fof('∘ identity', axiom,
+    ![F]: F ∘ id = F).
+
+fof('map functor', axiom,
+    ![F, G]: map(F) ∘ map(G) = map(F ∘ G)).
+
+fof('map functor', axiom,
+    map(id) = id).
+
+fof('defn pruneBy', axiom,
+    ![F]: pruneBy(F) = F ∘ (map(pruneRow) ∘ F)).
+
+fof('defn expand', axiom,
+    expand = product ∘ map(product)).
+
+fof('expand after boxs', axiom,
+    expand ∘ boxs = map(boxs) ∘ expand).
+
+fof('filter with boxs', axiom,
+    ![P, F]: filter (P ∘ boxs) = map(boxs) ∘ (filter(P) ∘ map(boxs))).
+
+fof('boxs involution', axiom,
+    boxs ∘ boxs = id).
+
+fof('filter after product', axiom,
+    ![P]: filter(all(P)) ∘ product = product ∘ map(filter(P))).
+
+fof('law of pruneRow', axiom,
+    filter(nodups) ∘ (product ∘ pruneRow) = filter(nodups) ∘ product).
+
+fof('map/filter', axiom,
+    ![P, F]: filter(P) ∘ map(F) = map(F) ∘ filter(P ∘ F)).
+
+fof('product/map', axiom,
+    ![F]: product ∘ map(F) = map(map(F)) ∘ product).
+
+fof('conjecture', conjecture,
+    filter(all(nodups) ∘ boxs) ∘ (expand ∘ pruneBy(boxs)) =
+    filter(all(nodups) ∘ boxs) ∘ expand).
diff --git a/tests/sudoku5.p b/tests/sudoku5.p
new file mode 100644
--- /dev/null
+++ b/tests/sudoku5.p
@@ -0,0 +1,42 @@
+cnf('associativity of ∘', axiom,
+    F ∘ (G ∘ H) = (F ∘ G) ∘ H).
+
+cnf('∘ identity', axiom,
+    id ∘ F = F).
+
+cnf('∘ identity', axiom,
+    F ∘ id = F).
+
+cnf('map functor', axiom,
+    map(F) ∘ map(G) = map(F ∘ G)).
+
+cnf('map functor', axiom,
+    map(id) = id).
+
+cnf('defn pruneBy', axiom,
+    pruneBy(F) = F ∘ (map(pruneRow) ∘ F)).
+
+cnf('defn expand', axiom,
+    expand = product ∘ map(product)).
+
+cnf('expand after boxs', axiom,
+    expand ∘ boxs = map(boxs) ∘ expand).
+
+cnf('filter with boxs', axiom,
+    filter (P ∘ boxs) = map(boxs) ∘ (filter(P) ∘ map(boxs))).
+
+cnf('boxs involution', axiom,
+    boxs ∘ boxs = id).
+
+cnf('filter after product', axiom,
+    filter(all(P)) ∘ product = product ∘ map(filter(P))).
+
+cnf('law of pruneRow', axiom,
+    filter(nodups) ∘ (product ∘ pruneRow) = filter(nodups) ∘ product).
+
+cnf('product/map', axiom,
+    product ∘ map(F) = map(map(F)) ∘ product).
+
+cnf('conjecture', conjecture,
+    filter(all(nodups) ∘ boxs) ∘ (expand ∘ pruneBy(boxs)) =
+    filter(all(nodups) ∘ boxs) ∘ expand).
diff --git a/tests/union.p b/tests/union.p
new file mode 100644
--- /dev/null
+++ b/tests/union.p
@@ -0,0 +1,9 @@
+cnf(elem_union_1, axiom, notelem(X, A) | ~notelem(X, union(A, B))).
+cnf(elem_union_2, axiom, notelem(X, B) | ~notelem(X, union(A, B))).
+cnf(elem_union_3, axiom, notelem(X, union(A, B)) | ~notelem(X, A) | ~notelem(X, B)).
+cnf(elem_equals, axiom, A=B | ~notelem(sK1_elem_equals_X(A, B), A) | ~notelem(sK1_elem_equals_X(A, B), B)).
+cnf(union_commutative, negated_conjecture, union(a, b)!=union(b, a)).
+
+cnf(elem_equals_1, axiom, choice(A,B) = c1 => notelem(sK1_elem_equals_X(A, B), A)).
+cnf(elem_equals_2, axiom, choice(A,B) = c2 => notelem(sK1_elem_equals_X(A, B), B)).
+cnf(elem_equals_3, axiom, choice(A,B) = c3 => A=B).
diff --git a/tests/union2.p b/tests/union2.p
new file mode 100644
--- /dev/null
+++ b/tests/union2.p
@@ -0,0 +1,25 @@
+cnf(ifeq_axiom, axiom, ifeq4(A, A, B, C)=B).
+cnf(ifeq_axiom, axiom, ifeq3(A, A, B, C)=B).
+cnf(ifeq_axiom, axiom, ifeq2(A, A, B, C)=B).
+cnf(ifeq_axiom, axiom, ifeq(A, A, B, C)=B).
+cnf(elem_union_1, axiom, ifeq(notelem(X, union(A, B)), true, notelem(X, A), true)=true).
+cnf(elem_union_2, axiom, ifeq(notelem(X, union(A, B)), true, notelem(X, B), true)=true).
+cnf(elem_union_3, axiom, ifeq(notelem(X, B), true, ifeq(notelem(X, A), true, notelem(X, union(A, B)), true), true)=true).
+cnf(elem_equals, axiom, ifeq2(notelem(sK1_elem_equals_X(A, B), B), true, ifeq2(notelem(sK1_elem_equals_X(A, B), A), true, A, B), B)=B).
+%cnf(union_commutative, negated_conjecture, union(a, b)!=union(b, a)).
+%cnf(elem_equals_1, axiom, ifeq3(choice(A, B), c1, notelem(sK1_elem_equals_X(A, B), A), true)=true).
+%cnf(elem_equals_2, axiom, ifeq3(choice(A, B), c2, notelem(sK1_elem_equals_X(A, B), B), true)=true).
+%cnf(elem_equals_3, axiom, ifeq4(choice(A, B), c3, A, B)=B).
+cnf(elem_equals_1, axiom, select(c1, a, d, d) = d).
+cnf(elem_equals_1, axiom, select(c2, d, b, d) = d).
+cnf(elem_equals_1, axiom, select(c3, d, d, c) = d).
+cnf(blah, conjecture, a=d | b=d | c=d).
+cnf(select, axiom, select(C, X, X, X)=X).
+cnf(select, axiom, select(c1, X, Y, Z)=X).
+cnf(select, axiom, select(c2, X, Y, Z)=Y).
+cnf(select, axiom, select(c3, X, Y, Z)=Z).
+
+%select(C, X, Y, Z) = select(C, select(c1, X, Y, Z), select(c2, X, Y, Z), select(c3, X, Y, Z)).
+
+%  d
+%= select(
diff --git a/tests/y-i.p b/tests/y-i.p
new file mode 100644
--- /dev/null
+++ b/tests/y-i.p
@@ -0,0 +1,4 @@
+fof(k_def, axiom, ![X, Y]: (k @ X) @ Y = X).
+fof(s_def, axiom, ![X, Y, Z]: ((s @ X) @ Y) @ Z = (X @ Z) @ (Y @ Z)).
+fof(i_def, axiom, ![X]: i @ X = X).
+fof(conjecture, conjecture, ?[Y]: ![F]: Y @ F = F @ (Y @ F)).
diff --git a/twee.cabal b/twee.cabal
--- a/twee.cabal
+++ b/twee.cabal
@@ -1,5 +1,5 @@
 name:                twee
-version:             2.4.2
+version:             2.5
 synopsis:            An equational theorem prover
 homepage:            http://github.com/nick8325/twee
 license:             BSD3
@@ -38,6 +38,11 @@
   default: False
   manual: True
 
+flag parallel
+  description: Build a special parallel version of Twee.
+  default: False
+  manual: True
+
 executable twee
   main-is: Main.hs
 
@@ -45,7 +50,7 @@
   other-modules:       SequentialMain
   default-language:    Haskell2010
   build-depends:       base < 5,
-                       twee-lib == 2.4.2,
+                       twee-lib == 2.5,
                        containers,
                        pretty,
                        split,
@@ -59,3 +64,16 @@
 
   if flag(static-cxx)
     ghc-options: -pgml misc/static-libstdc++
+
+Test-Suite twee-test
+    type: exitcode-stdio-1.0
+    Default-language: Haskell2010
+    hs-source-dirs:
+        misc
+    main-is: Test.hs
+    build-depends: base < 5, QuickCheck, twee-lib == 2.5, containers, pretty
+    ghc-options:
+      -threaded
+      -rtsopts
+      -feager-blackholing
+      -with-rtsopts=-N4