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, DerivingVia #-}
+{-# LANGUAGE CPP, RecordWildCards, FlexibleInstances, PatternGuards, DeriveAnyClass #-}
 {-# OPTIONS_GHC -flate-specialise #-}
 module SequentialMain(main) where
 
@@ -32,9 +32,10 @@
 import System.IO
 import System.Exit
 import qualified Data.Set as Set
-import qualified Twee.Label as Label
+import qualified Data.Label as Label
 import System.Console.ANSI
 import Data.Symbol
+import Twee.Profile
 
 data MainFlags =
   MainFlags {
@@ -45,14 +46,19 @@
     flags_flip_ordering :: Bool,
     flags_give_up_on_saturation :: Bool,
     flags_flatten_goals :: Bool,
+    flags_flatten_nonground :: Bool,
     flags_flatten_goals_lightly :: Bool,
     flags_flatten_all :: Bool,
     flags_eliminate :: [String],
-    flags_backwards_goal :: Int }
+    flags_backwards_goal :: Int,
+    flags_flatten_backwards_goal :: Int,
+    flags_equals_transformation :: Bool,
+    flags_distributivity_heuristic :: Bool,
+    flags_kbo_weight0 :: Bool }
 
 parseMainFlags :: OptionParser MainFlags
 parseMainFlags =
-  MainFlags <$> proof <*> trace <*> formal <*> explain <*> flipOrdering <*> giveUp <*> flatten <*> flattenLightly <*> flattenAll <*> eliminate <*> backwardsGoal
+  MainFlags <$> proof <*> trace <*> formal <*> explain <*> flipOrdering <*> giveUp <*> flatten <*> flattenNonGround <*> flattenLightly <*> flattenAll <*> eliminate <*> backwardsGoal <*> flattenBackwardsGoal <*> equalsTransformation <*> distributivityHeuristic <*> kboWeight0
   where
     proof =
       inGroup "Output options" $
@@ -76,6 +82,10 @@
       expert $
       inGroup "Term order options" $
       bool "flip-ordering" ["Make more common function symbols smaller (off by default)."] False
+    kboWeight0 =
+      expert $
+      inGroup "Term order options" $
+      bool "kbo-weight0" ["Give functions of arity >= 2 a weight of 0."] False
     giveUp =
       expert $
       inGroup "Output options" $
@@ -84,6 +94,10 @@
       expert $
       inGroup "Completion heuristics" $
       bool "flatten-goal" ["Flatten goal by adding new axioms (on by default)."] True
+    flattenNonGround =
+      expert $
+      inGroup "Completion heuristics" $
+      bool "flatten-nonground" ["Flatten even non-ground clauses (off by default)."] False
     flattenLightly =
       expert $
       inGroup "Completion heuristics" $
@@ -96,6 +110,18 @@
       expert $
       inGroup "Completion heuristics" $
       flag "backwards-goal" ["Try rewriting backwards from the goal this many times (0 by default)."] 0 argNum
+    flattenBackwardsGoal =
+      expert $
+      inGroup "Completion heuristics" $
+      flag "flatten-backwards-goal" ["Try rewriting backwards from the goal this many times when flattening (0 by default)."] 0 argNum
+    equalsTransformation =
+      expert $
+      inGroup "Completion heuristics" $
+      bool "equals-transformation" ["Apply the 'equals transformation' even to ground goals (off by default)."] False
+    distributivityHeuristic =
+      expert $
+      inGroup "Completion heuristics" $
+      bool "distributivity-heuristic" ["Treat distributive operators specially (off by default)."] False
     eliminate =
       inGroup "Proof presentation" $
       concat <$>
@@ -282,8 +308,7 @@
     con_size   :: !Integer,
     con_weight :: !Integer,
     con_bonus  :: !Bool }
-  deriving (Eq, Ord)
-  deriving Labelled via AutoLabel Constant
+  deriving (Eq, Ord, Labelled)
 
 data Precedence = Precedence !Bool !Bool !(Maybe Int) !Int
   deriving (Eq, Ord)
@@ -345,10 +370,17 @@
     ctx_type    :: Type }
 
 -- Convert back and forth between Twee and Jukebox.
-tweeConstant :: HornFlags -> TweeContext -> Precedence -> Jukebox.Function -> Constant
-tweeConstant flags TweeContext{..} prec fun
+tweeConstant :: MainFlags -> HornFlags -> TweeContext -> Precedence -> Jukebox.Function -> Constant
+tweeConstant MainFlags{..} flags TweeContext{..} prec fun
   | fun == ctx_minimal = Minimal
-  | otherwise = Constant prec fun (Jukebox.arity fun) 1 1 (bonus fun)
+  | otherwise =
+    Constant {
+      con_prec = prec,
+      con_id = fun,
+      con_arity = Jukebox.arity fun,
+      con_size = if flags_kbo_weight0 && Jukebox.arity fun >= 2 then 0 else 1,
+      con_weight = 1,
+      con_bonus = bonus fun }
   where
     bonus fun =
       (isIfeq fun && encoding flags /= Asymmetric2) ||
@@ -378,13 +410,13 @@
 jukeboxFunction _ Constant{..} = con_id
 jukeboxFunction TweeContext{..} Minimal = ctx_minimal
 
-tweeTerm :: HornFlags -> TweeContext -> (Jukebox.Function -> Precedence) -> Jukebox.Term -> Term Constant
-tweeTerm flags ctx prec t = build (tm t)
+tweeTerm :: MainFlags -> HornFlags -> TweeContext -> (Jukebox.Function -> Precedence) -> Jukebox.Term -> Term Constant
+tweeTerm flags horn ctx prec t = build (tm t)
   where
     tm (Jukebox.Var (x ::: _)) =
       var (V (fromIntegral (Label.labelNum (Label.label x))))
     tm (f :@: ts) =
-      app (fun (tweeConstant flags ctx (prec f) f)) (map tm ts)
+      app (fun (tweeConstant flags horn ctx (prec f) f)) (map tm ts)
 
 jukeboxTerm :: TweeContext -> Term Constant -> Jukebox.Term
 jukeboxTerm TweeContext{..} (Var (V x)) =
@@ -416,45 +448,102 @@
     ctx_equals = equals,
     ctx_type = ty }
 
-flattenGoals :: Bool -> Bool -> Problem Clause -> Problem Clause
-flattenGoals flattenAll full prob =
+flattenGoals :: Int -> Bool -> Bool -> Bool -> Problem Clause -> Problem Clause
+flattenGoals backwardsGoal flattenNonGround flattenAll full prob =
   run prob $ \prob -> do
-    cs <- concat <$> mapM flatten prob
-    return $
-      prob ++
-      [ Input{tag = "flattening", kind = Jukebox.Ax Definition,
-              what = c, source = Unknown }
-      | c <- cs ]
+    let ts = usort $ extraTerms prob
+    cs <- mapM define ts
+    return (prob ++ cs)
   where
-    flatten Input{what = Clause (Bind _ [Neg (x Jukebox.:=: y)])} =
-      liftM2 (++) (flat x) (flat y)
-    flatten Input{what = Clause (Bind _ [Pos (x Jukebox.:=: y)])}
-      | flattenAll =
-        liftM2 (++) (flat x) (flat y)
-    flatten _ = return []
+    extraTerms prob = concatMap (input prob) prob
+    input prob Input{what = Clause (Bind _ [Neg (x Jukebox.:=: y)])} =
+      concatMap term (backwards backwardsGoal prob x) ++
+      concatMap term (backwards backwardsGoal prob y)
+    input _ Input{what = Clause (Bind _ [Pos (x Jukebox.:=: y)])}
+      | flattenAll = term x ++ term y
+    input _ _ = []
 
-    flat (f :@: ts)
-      | not (all isVar ts) || usort ts /= ts = do
-        name <- newName f
-        let vs  = Jukebox.vars ts
-            g = name ::: FunType (map typ vs) (typ f)
-            c = clause [Pos (g :@: map Jukebox.Var vs Jukebox.:=: f :@: ts)]
-        css <- if full then concat <$> mapM flat ts else return []
-        return (c:css)
-    flat _ = return []
+    term t@(_f :@: ts) =
+      [ t
+      | ground t || flattenNonGround,
+        not (all isVar ts) || usort ts /= sort ts ] ++
+      if full then concatMap term ts else []
+    term _ = []
 
     isVar (Jukebox.Var _) = True
     isVar _ = False
 
+    define (f :@: ts) = do
+      name <- newName f
+      let vs  = Jukebox.vars ts
+          g = name ::: FunType (map typ vs) (typ f)
+          c = clause [Pos (g :@: map Jukebox.Var vs Jukebox.:=: f :@: ts)]
+      return Input{tag = "flattening", kind = Jukebox.Ax Definition,
+                   what = c, source = Unknown }
+
+    backwards 0 _ t = [t]
+    backwards n cs t =
+      t:
+      [ v
+      | Input{what = Clause (Bind _ [Pos (x0 Jukebox.:=: y0)])} <- cs,
+        (x, y) <- [(x0, y0), (y0, x0)],
+        (s, k) <- contexts t,
+        sub <- maybeToList (Jukebox.match x s),
+        let u = k (Jukebox.subst sub y),
+        ground u,
+        v <- backwards (n-1) cs u ]
+
+addDistributivityHeuristic :: Problem Clause -> Problem Clause
+addDistributivityHeuristic prob =
+  run prob $ \prob -> do
+    cs <- mapM add prob
+    return (prob ++ catMaybes cs)
+
+  where
+    add Input{what = Clause (Bind _ [Pos (t Jukebox.:=: u)])} =
+      case checkDistributivity t u `mplus` checkDistributivity u t of
+        Just (f, g, ty) -> do
+          name <- newName (base f ++ "_" ++ base g)
+          x <- Jukebox.Var <$> newSymbol "X" ty
+          y <- Jukebox.Var <$> newSymbol "Y" ty
+          z <- Jukebox.Var <$> newSymbol "Z" ty
+          Just <$> define name (g :@: [f :@: [x, y], z])
+        _ -> return Nothing
+    add _ = return Nothing
+
+    checkDistributivity
+      (f1 :@: [Jukebox.Var x1, g1 :@: [Jukebox.Var y1, Jukebox.Var z1]])
+      (g2 :@: [f2 :@: [Jukebox.Var x2, Jukebox.Var y2],
+               f3 :@: [Jukebox.Var x3, Jukebox.Var z2]])
+      | f1 == f2 && f2 == f3 && g1 == g2 &&
+        x1 == x2 && x2 == x3 && y1 == y2 && z1 == z2 =
+        Just (f1, g1, Jukebox.typ x1)
+      
+    checkDistributivity
+      (f1 :@: [g1 :@: [Jukebox.Var x1, Jukebox.Var y1], Jukebox.Var z1])
+      (g2 :@: [f2 :@: [Jukebox.Var x2, Jukebox.Var z2],
+       f3 :@: [Jukebox.Var y2, Jukebox.Var z3]])
+      | f1 == f2 && f2 == f3 && g1 == g2 &&
+        x1 == x2 && y1 == y2 && z1 == z2 && z2 == z3 =
+        Just (f1, g1, Jukebox.typ x1)
+    checkDistributivity _ _ = Nothing
+
+    define name t = do
+      let vs  = Jukebox.vars t
+          g = name ::: FunType (map typ vs) (typ t)
+          c = clause [Pos (g :@: map Jukebox.Var vs Jukebox.:=: t)]
+      return Input{tag = "distributivity_heuristic", kind = Jukebox.Ax Definition,
+                   what = c, source = Unknown }
+
 -- Encode existentials so that all goals are ground.
-addNarrowing :: TweeContext -> Problem Clause -> Problem Clause
-addNarrowing TweeContext{..} prob =
+addNarrowing :: Bool -> TweeContext -> Problem Clause -> Problem Clause
+addNarrowing alwaysNarrow TweeContext{..} prob =
   unchanged ++ equalityClauses
   where
     (unchanged, nonGroundGoals) = partitionEithers (map f prob)
       where
         f inp@Input{what = Clause (Bind _ [Neg (x Jukebox.:=: y)])}
-          | not (ground x) || not (ground y) =
+          | not (ground x) || not (ground y) || alwaysNarrow =
             Right (inp, (x, y))
         f inp = Left inp
 
@@ -483,7 +572,7 @@
                 let form = And (map (Literal . snd) equalityLiterals) in
                 ForAll (Bind (Set.fromList (vars form)) form),
               source =
-                Inference "encode_existential" "esa"
+                inference "encode_existential" "esa"
                   (map (fmap toForm . fst) nonGroundGoals) }
 
           input tag form =
@@ -492,7 +581,7 @@
               kind = Conj Conjecture,
               what = clause [form],
               source =
-                Inference "split_conjunct" "thm" [justification] }
+                inference "split_conjunct" "thm" [justification] }
 
         in [input tag form | (tag, form) <- equalityLiterals]
 
@@ -527,15 +616,18 @@
     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 MainFlags{..} later obligs = {-# SCC runTwee #-} do
+runTwee globals (TSTPFlags tstp) horn precedence config flags@MainFlags{..} later obligs = {-# SCC runTwee #-} do
   let
     -- Encode whatever needs encoding in the problem
-    obligs'
-      | flags_flatten_goals_lightly = flattenGoals False False obligs
-      | flags_flatten_all = flattenGoals True True obligs
-      | flags_flatten_goals = flattenGoals False True obligs
+    obligs1
+      | flags_flatten_goals_lightly = flattenGoals flags_flatten_backwards_goal flags_flatten_nonground False False obligs
+      | flags_flatten_all = flattenGoals flags_flatten_backwards_goal flags_flatten_nonground True True obligs
+      | flags_flatten_goals = flattenGoals flags_flatten_backwards_goal flags_flatten_nonground False True obligs
       | otherwise = obligs
-    ctx = makeContext obligs'
+    obligs2
+      | flags_distributivity_heuristic = addDistributivityHeuristic obligs1
+      | otherwise = obligs1
+    ctx = makeContext obligs2
     lowercaseSkolem x
       | hasLabel "skolem" x =
         withRenamer x $ \s i ->
@@ -543,7 +635,7 @@
             Renaming xss xs ->
               Renaming (map (map toLower) xss) (map toLower xs)
       | otherwise = x
-    prob = prettyNames (mapName lowercaseSkolem (addNarrowing ctx obligs'))
+    prob = prettyNames (mapName lowercaseSkolem (addNarrowing flags_equals_transformation ctx obligs2))
 
   (unsortedAxioms0, goals0) <-
     case identifyProblem ctx prob of
@@ -568,7 +660,7 @@
 
     -- Translate everything to Twee.
     toEquation (t, u) =
-      canonicalise (tweeTerm horn ctx prec t :=: tweeTerm horn ctx prec u)
+      canonicalise (tweeTerm flags horn ctx prec t :=: tweeTerm flags horn ctx prec u)
 
     axiomCompare ax1 ax2
       | ax1' `simplerThan` ax2' = LT
@@ -707,7 +799,7 @@
             Just inp -> go inp
            where
             go Input{source = Unknown} = []
-            go Input{source = Inference _ _ inps} = concatMap go inps
+            go Input{source = Inference _ _ inps} = concatMap (go . inputValue) inps
             go inp@Input{source = FromFile _ _} = [inp]
 
       when flags_explain_encoding $ do
@@ -758,7 +850,7 @@
          KBO.size (rhs rule), rhs rule)
       actives =
         sortBy (comparing (score . active_rule)) $
-        IntMap.elems (st_active_ids state')
+        IntMap.elems (st_active_set state')
 
     when (tstp && configIsComplete config) $ do
       putStrLn "% SZS output start Saturation"
@@ -802,7 +894,7 @@
       kind = Jukebox.Ax Jukebox.Axiom,
       what = false,
       source =
-        Inference "resolution" "thm"
+        inference "resolution" "thm"
           [-- A proof of t != u
            existentialHack pg_goal_hint (fromJust (lookup pg_number goals)),
            -- A proof of t = u
@@ -831,7 +923,7 @@
         kind = Jukebox.Ax Jukebox.Axiom,
         what = jukeboxEquation (equation (certify p)),
         source =
-          Inference name "thm" sources }
+          inference name "thm" sources }
       where
         (name, sources) = unpack p
 
@@ -861,7 +953,7 @@
           -- if not, try its ancestors.
           find inp | ok inp = [inp]
           find Input{source = Inference _ _ inps} =
-            concatMap find inps
+            concatMap (find . inputValue) inps
           find _ = []
 
           ok inp =
@@ -877,7 +969,7 @@
 
 main = do
   hSetBuffering stdout LineBuffering
-  join . parseCommandLineWithExtraArgs
+  stampM (intern "twee") . join . parseCommandLineWithExtraArgs
     ["--no-conjunctive-conjectures", "--no-split"]
 #ifdef VERSION_twee
     "Twee, an equational theorem prover" . version ("twee version " ++ VERSION_twee) $
@@ -898,6 +990,7 @@
               expert (toFof <$> clausifyBox <*> pure (tags True)) =>>=
               expert clausifyBox =>>= expert oneConjectureBox) <*>
              (runTwee <$> globalFlags <*> tstpFlags <*> expert hornFlags <*> parsePrecedence)))
+  profile
   where
     combine horn config main encode prove later prob0 = do
       res <- horn prob0
@@ -909,5 +1002,5 @@
             isUnitEquality [Neg (_ Jukebox.:=: _)] = True
             isUnitEquality _ = False
             isUnit = all isUnitEquality (map (toLiterals . what) prob0)
-            main' = if isUnit then main else main{flags_formal_proof = False}
+            main' = if isUnit then main{flags_explain_encoding = False} else main{flags_formal_proof = False}
           encode prob >>= prove config main' later
diff --git a/misc/BestTwee.hs b/misc/BestTwee.hs
--- a/misc/BestTwee.hs
+++ b/misc/BestTwee.hs
@@ -1,3 +1,6 @@
+{-# LANGUAGE TemplateHaskell #-}
+module Main where
+
 import MaxCover
 import System.FilePath
 import System.FilePath.Glob
@@ -7,6 +10,9 @@
 import Data.List
 import Data.Maybe
 import Data.Time.Clock
+import qualified Data.Map as Map
+import Data.Map(Map)
+import Data.FileEmbed
 
 solvedInTime :: NominalDiffTime -> FilePath -> String -> IO Bool
 solvedInTime timeLimit dir prob = do
@@ -18,31 +24,45 @@
   return (diffUTCTime outTime errTime <= timeLimit)
 
 notE :: [(String, Double)]
-notE = [
-  ("LAT168-1", 0.30), ("LAT171-1", 0.43), ("ALG240-1", 0.48), ("LAT174-1", 0.65), ("GRP768-1", 0.70),
-  ("LAT142-1", 0.70), ("GRP505-1", 0.74), ("LAT145-1", 0.74), ("LAT164-1", 0.74), ("RNG025-5", 0.74),
-  ("GRP506-1", 0.78), ("GRP507-1", 0.78), ("LAT018-1", 0.78), ("LAT148-1", 0.78), ("LAT153-1", 0.78),
-  ("LAT155-1", 0.78), ("RNG025-4", 0.78), ("GRP508-1", 0.83), ("KLE151-10", 0.83), ("LAT162-1", 0.83),
-  ("ALG246-1", 0.87), ("GRP024-5", 0.87), ("GRP766-1", 0.87), ("LAT146-1", 0.87), ("LAT159-1", 0.87),
-  ("LAT160-1", 0.87), ("LAT170-1", 0.87), ("LAT177-1", 0.87), ("REL022-2", 0.87), ("COL042-10", 0.91),
-  ("GRP196-1", 0.91), ("GRP666-3", 0.91), ("GRP666-4", 0.91), ("GRP666-5", 0.91), ("LAT156-1", 0.91),
-  ("LAT157-1", 0.91), ("LAT169-1", 0.91), ("LCL148-10", 0.91), ("REL020-2", 0.91), ("REL021-1", 0.91),
-  ("REL021-2", 0.91), ("REL022-1", 0.91), ("REL029-1", 0.91), ("REL033-1", 0.91), ("REL033-3", 0.91),
-  ("REL034-1", 0.91), ("REL034-2", 0.91), ("REL035-1", 0.91), ("REL035-2", 0.91), ("REL036-1", 0.91),
-  ("GRP164-1", 0.96), ("GRP164-2", 0.96), ("GRP666-2", 0.96), ("GRP678-1", 0.96), ("GRP721-1", 0.96),
-  ("GRP725-1", 0.96), ("KLE110-10", 0.96), ("LAT072-1", 0.96), ("LAT076-1", 0.96), ("LAT140-1", 0.96),
-  ("LAT141-1", 0.96), ("LAT144-1", 0.96), ("LAT147-1", 0.96), ("LAT149-1", 0.96), ("LAT151-1", 0.96),
-  ("LAT158-1", 0.96), ("LAT163-1", 0.96), ("LAT167-1", 0.96), ("LAT172-1", 0.96), ("LAT173-1", 0.96),
-  ("LAT175-1", 0.96), ("LAT176-1", 0.96), ("LAT183-10", 0.96), ("LAT186-10", 0.96), ("LCL927-10", 0.96),
-  ("REL020-1", 0.96), ("REL040-1", 0.96), ("REL040-3", 0.96), ("GRP177-1", 1.00), ("GRP724-1", 1.00),
-  ("LAT074-1", 1.00), ("LAT075-1", 1.00), ("LAT077-1", 1.00), ("LAT078-1", 1.00), ("LAT079-1", 1.00),
-  ("LAT139-1", 1.00), ("LAT161-1", 1.00), ("LCL220-10", 1.00), ("LCL330-10", 1.00), ("LCL348-10", 1.00),
-  ("REL032-1", 1.00), ("REL032-2", 1.00), ("REL038-1", 1.00), ("REL039-1", 1.00), ("ROB007-1", 1.00),
-  ("ROB033-1", 1.00)]
+notE = filter (\(x, _) -> '+' `notElem` x) [
+  ("GRP702+1", 0.06), ("GRP715+1", 0.06), ("GRP660+2", 0.12), ("GRP660+3", 0.12),
+  ("GRP665+1", 0.12), ("GRP700+1", 0.12), ("GRP658+1", 0.18), ("GRP659+1", 0.18),
+  ("GRP656+1", 0.24), ("GRP657+1", 0.24), ("GRP660+1", 0.24), ("GRP682+1", 0.24),
+  ("GRP683+1", 0.24), ("GRP685+1", 0.24), ("GRP703+1", 0.24), ("GRP704+1", 0.24),
+  ("GRP710+1", 0.24), ("GRP777+1", 0.24), ("LCL897+1", 0.29), ("LAT168-1", 0.30),
+  ("LAT171-1", 0.43), ("ALG240-1", 0.48), ("GRP654+2", 0.53), ("GRP654+3", 0.53),
+  ("GRP655+2", 0.53), ("GRP655+3", 0.53), ("LAT174-1", 0.65), ("LAT142-1", 0.70),
+  ("GRP654+1", 0.71), ("GRP655+1", 0.71), ("GRP505-1", 0.74), ("LAT145-1", 0.74),
+  ("LAT164-1", 0.74), ("GRP506-1", 0.78), ("GRP507-1", 0.78), ("LAT018-1", 0.78),
+  ("LAT148-1", 0.78), ("LAT153-1", 0.78), ("LAT155-1", 0.78), ("GRP508-1", 0.83),
+  ("KLE151-10", 0.83), ("LAT162-1", 0.83), ("LAT146-1", 0.87), ("LAT159-1", 0.87),
+  ("LAT160-1", 0.87), ("LAT170-1", 0.87), ("LAT177-1", 0.87), ("GRP664+1", 0.88),
+  ("ALG441-10", 0.91), ("COL042-10", 0.91), ("GRP196-1", 0.91), ("GRP666-3", 0.91),
+  ("GRP666-4", 0.91), ("GRP666-5", 0.91), ("LAT156-1", 0.91), ("LAT169-1", 0.91),
+  ("LCL148-10", 0.91), ("GRP164-2", 0.96), ("GRP666-2", 0.96), ("GRP678-1", 0.96),
+  ("GRP725-1", 0.96), ("KLE110-10", 0.96), ("LAT072-1", 0.96), ("LAT076-1", 0.96),
+  ("LAT140-1", 0.96), ("LAT141-1", 0.96), ("LAT144-1", 0.96), ("LAT147-1", 0.96),
+  ("LAT149-1", 0.96), ("LAT151-1", 0.96), ("LAT158-1", 0.96), ("LAT163-1", 0.96),
+  ("LAT167-1", 0.96), ("LAT172-1", 0.96), ("LAT173-1", 0.96), ("LAT175-1", 0.96),
+  ("LAT176-1", 0.96), ("LCL927-10", 0.96), ("REL040-1", 0.96), ("REL040-3", 0.96),
+  ("ALG212+1", 1.00), ("ALG213+1", 1.00), ("GRP724-1", 1.00), ("KLE122-10", 1.00),
+  ("LAT074-1", 1.00), ("LAT075-1", 1.00), ("LAT077-1", 1.00), ("LAT078-1", 1.00),
+  ("LAT079-1", 1.00), ("LAT139-1", 1.00), ("LAT161-1", 1.00), ("LCL220-10", 1.00),
+  ("LCL330-10", 1.00), ("LCL348-10", 1.00), ("REL032-2", 1.00), ("REL038-1", 1.00),
+  ("REL039-1", 1.00)]
 
+ratings :: Map String Double
+ratings =
+  Map.fromList
+    [ (name, read rating)
+    | [name, rating] <- map words (lines input)]
+  where
+    input = $(embedStringFile "ratings")
+
 problemBonus :: (Int, Int, Int, Int, Int, Int) -> String -> Int
 problemBonus (b0, b1, b2, b3, b4, b5) p =
-  case lookup p notE of
+  ebonus *
+  case Map.lookup p ratings of
     Nothing -> b0
     Just x
       | x < 0.7 ->   b1
@@ -50,6 +70,11 @@
       | x < 0.9 ->   b3
       | x < 0.95 ->  b4
       | otherwise -> b5
+  where
+    ebonus =
+      case lookup p notE of
+        Nothing -> 1
+        Just _ -> 1
 
 greatProblemsBonus :: (Int, Int, Int, Int, Int, Int) -> String -> [String]
 greatProblemsBonus b p =
@@ -58,20 +83,27 @@
 bonuses :: [(String, (Int, Int, Int, Int, Int, Int))]
 bonuses =
   [("no bonus", (1, 1, 1, 1, 1, 1)),
-   ("low bonus", (1, 1, 2, 3, 4, 5)),
-   ("medium bonus", (1, 2, 4, 6, 8, 10)),
-   ("high bonus", (0, 1, 2, 3, 4, 5)),
-   ("big fish", (0, 0, 0, 0, 1, 1))]
+   ("low bonus", (1, 1, 2, 3, 5, 10)),
+   --("medium bonus", (1, 2, 4, 6, 8, 10)),
+   --("high bonus", (0, 1, 2, 3, 4, 5)),
+   --("big fish", (0, 0, 0, 0, 1, 1)),
+   ("rating 1", (0, 0, 0, 0, 0, 1))]
 
 readResults ok = do
-  filenames <- glob "out/twee-*/success"
+  filenames <- glob "/home/nick/writing/twee/times/*-twee-casc-extra-*"
   fmap (filter (\(x, _) -> x `notElem` banned)) $ forM filenames $ \filename -> do
-    let directory = takeDirectory filename
-    let name = takeFileName directory
-    solved <- fmap (filter ok) $ lines <$> readFile filename
-    fast <- filterM (solvedInTime 120 directory) solved
-    slow <- filterM (solvedInTime 600 directory) solved
-    return (name, (fast, slow))
+    let name = takeFileName filename
+    let unpack xs = (takeBaseName name, read time :: Double) where [name, time] = words xs
+    solved <- filter (ok . fst) . map unpack . lines <$> readFile filename
+    let solvedInTime t = [name | (name, time) <- solved, time < t]
+--    fast <- filterM (solvedInTime 120 directory) solved
+--    med  <- filterM (solvedInTime 240 directory) solved
+--    slow <- filterM (solvedInTime 600 directory) solved
+    let fast = solvedInTime 210
+    let med  = solvedInTime 300
+    let slow = solvedInTime (1/0)
+    
+    return (name, (fast, med, slow))
 
 score results cover =
   length (usort (concat [probs | (name, probs) <- results, name `elem` cover]))
@@ -85,37 +117,41 @@
     find x = fromJust (lookup x results)
 
 main = do
-  probs <- lines <$> readFile "casc-j10"
+  probs <- lines <$> readFile "unsat"
   results <- readResults (`elem` probs)
   let
     options =
-      [("fast", \(fast, _) -> (fast, []))]
-       --("slow", \(_, slow) -> ([], slow)),
-       --("fast and slow", id)]
+      [("fast", \(fast, _, _) -> (fast, [], [])),
+       ("med", \(_, med, _) -> ([], med, []))]
+       --("slow", \(_, _, slow) -> ([], [], slow))]
+       --("fast and med", \(fast, med, _) -> (fast, med, []))]
 
-  forM_ options $ \(option, f) -> do
-    forM_ bonuses $ \(bonus, b) -> do
+  forM_ bonuses $ \(bonus, b) -> do
+    forM_ options $ \(option, f) -> do
       let
         results1 =
           [ (name,
              map (++ "/fast") (concatMap (greatProblemsBonus b) fast) ++
+             map (++ "/med")  (concatMap (greatProblemsBonus b) med) ++
              map (++ "/slow") (concatMap (greatProblemsBonus b) slow))
           | (name, res) <- results,
-            let (fast, slow) = f res ]
+            let (fast, med, slow) = f res ]
 
         best = greedy results1
 
       putStrLn (option ++ "/" ++ bonus ++ ":")
-      forM_ (zip3 [1..] best (inits best)) $ \(i, name, names) -> do
-        putStrLn (show i ++ ". " ++ name ++ " " ++ show (score results1 (name:names)) ++ ", useful at levels " ++ show (levels results1 name names))
+      forM_ (take 6 $ zip3 [1..] best (inits best)) $ \(i, name, names) -> do
+        putStrLn (show i ++ ". " ++ name ++ " " ++ show (score results1 (name:names)) ++ ", useful at levels " ++ show (drop (length fixed) $ levels results1 name names))
 
       putStrLn ""
 
---      putStrLn "\nBest:"
---      forM_ [1..8] $ \i -> do
---        cover <- maxCover i results1
---        putStrLn (show i ++ ": " ++ show (score results1 cover))
---        forM_ cover $ \name -> putStrLn ("  " ++ name)
+{-
+      putStrLn "Best:"
+      forM_ [1..6] $ \i -> do
+        cover <- maxCover i results1
+        putStrLn (show i ++ ": " ++ show (score results1 cover))
+        forM_ cover $ \name -> putStrLn ("  " ++ name)
+-}
 
 greedy [] = []
 greedy results =
@@ -131,27 +167,42 @@
         Nothing -> Left (length probs)
 
 fixed :: [String]
-fixed = [
-  "twee-200715-twee-goal-flip-lhs2",
-  "twee-200714-twee-goalagain",
-  "twee-200712-twee-ghc8.10",
-  "twee-200714-twee-goalagain-flip-lhs1",
-  "twee-200715-twee-goal-lhs4-var3",
-  "twee-200715-twee-goal-lhs6-var3",
-  "twee-200715-twee-goal-lhs2-var3",
-  "twee-200611-twee-flip-lhs9"]
---fixed = [
---  "twee-200612-twee-aggressive-renormalise-flip-lhs4",
---  "twee-200612-twee-aggressive-renormalise-flip-lhs9",
---  "twee-200611-twee-flip-lhs1",
---  "twee-200611-twee-lhs4",
---  "twee-200611-twee-lhs5",
---  "twee-200612-twee-aggressive-renormalise-nodup",
---  "twee-200611-twee-nosimp",
---  "twee-200612-twee-aggressive-renormalise-nodepth"]
+fixed = fixed_new
+fixed_new = take 6 [
+  "twee-210619-twee-casc-extra-lhsnormal-flatten",
+  "twee-210619-twee-casc-extra-lhs9-flip-nogoal-kbo0",
+  "twee-210619-twee-casc-extra-depth-60",
+  "twee-210619-twee-casc-extra-no-dup",
+  "twee-210619-twee-casc-extra-lhs9-nogoal-aggrnorm-kbo0",
+  "twee-210619-twee-casc-extra-lhs5-flip-aggrnorm-kbo0"]
 
+fixed_old = take 2 [
+  "twee-210619-twee-casc-extra-no-dup",
+  "twee-210621-twee-casc-extra-depth-60-kbo0",
+  "twee-210619-twee-casc-extra-lhs5-flip-aggrnorm",
+  "twee-210619-twee-casc-extra-lhs9-nogoal-aggrnorm-kbo0",
+  "twee-210621-twee-casc-extra-complete-subsets-flatten",
+  "twee-210619-twee-casc-extra-lhs9-flip-nogoal",
+  "twee-210619-twee-casc-extra-no-dup-nogoal"]
+
+{- attempt 2:
+fixed = take 0 [
+  "twee-210619-twee-casc-extra-lhs5-flip-aggrnorm-kbo0",
+  "twee-210621-twee-casc-extra-depth-60-kbo0",
+  "twee-210619-twee-casc-extra-complete-subsets",
+  "twee-210621-twee-casc-extra-flatten-lhs9-kbo0",
+  "twee-210619-twee-casc-extra-lhs9-nogoal-aggrnorm",
+  "twee-210619-twee-casc-extra-lhs9-flip-nogoal-kbo0"]
+  -}
+
+{- attempt 1:
+  "twee-210621-twee-casc-extra-flatten-lhs9-kbo0",
+  "twee-210619-twee-casc-extra-lhs9-nogoal-aggrnorm",
+  "twee-210621-twee-casc-extra-depth-60-kbo0",
+  "twee-210619-twee-casc-extra-complete-subsets",
+  "twee-210619-twee-casc-extra-lhs9-flip-nogoal-kbo0",
+  "twee-210619-twee-casc-extra-lhs5-flip-aggrnorm-kbo0"]
+-}
+
 banned :: [String]
 banned = []
---  "twee-200714-twee-goalagain",
---  "twee-200714-twee-goalagain-flip-lhs1",
---  "twee-200714-twee-goalagain-flip-lhs3"]
diff --git a/misc/Test.hs b/misc/Test.hs
new file mode 100644
--- /dev/null
+++ b/misc/Test.hs
@@ -0,0 +1,228 @@
+{-# LANGUAGE TemplateHaskell, FlexibleInstances, FlexibleContexts, UndecidableInstances, StandaloneDeriving, ScopedTypeVariables, TupleSections, DeriveGeneric, DerivingVia, DeriveAnyClass #-}
+module Test where
+
+import Twee.Constraints
+import Twee.Term hiding (subst, canonicalise, F)
+import Twee.Term.Core hiding (F)
+import Test.QuickCheck hiding (Function, Fun)
+import Test.QuickCheck.All
+import Twee.Pretty
+import Twee.CP
+import Twee.Proof
+import qualified Twee.KBO as Ord
+import Text.PrettyPrint
+import Twee.Base hiding (F)
+import Twee.Rule
+import Twee.Equation
+import Control.Monad
+import qualified Data.Map as Map
+import Data.Maybe
+import Data.Ord
+import Data.List
+import Data.Typeable
+import qualified Twee.Index as Index
+import Data.Int
+import GHC.Generics
+import Twee.Utils
+
+data Func = F Int Integer deriving (Eq, Ord, Show)
+  deriving Labelled via (AutoLabel Func)
+
+instance Pretty Func where 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)
+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
+instance Arity Func where
+  arity (F 0 _) = 0
+  arity (F 1 _) = 2
+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
+  arbitrary = fmap fun arbitrary
+
+instance (Labelled f, Ord f, Typeable f, Arbitrary f, Arity f) => Arbitrary (Term f) where
+  arbitrary =
+    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 ]
+  shrink (App f ts0) =
+    ts ++ (build <$> app f <$> shrinkOne ts)
+    where
+      ts = unpack ts0
+      shrinkOne [] = []
+      shrinkOne (x:xs) =
+        [ y:xs | y <- shrink x ] ++
+        [ x:ys | ys <- shrinkOne xs ]
+  shrink _ = []
+
+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
+  arbitrary = liftM2 Pair arbitrary arbitrary
+  shrink (Pair x y) =
+    [ Pair x' y  | x' <- shrink x ] ++
+    [ Pair x y'  | y' <- shrink y ] ++
+    [ Pair x' y' | x' <- shrink x, y' <- shrink y ]
+
+instance (Labelled f, Ord f, Typeable f, Arbitrary f, Arity f) => Arbitrary (Equation f) where
+  arbitrary = do
+    Pair t u <- arbitrary
+    return (t :=: u)
+  shrink (t :=: u) = [t' :=: u' | Pair t' u' <- shrink (Pair t u)]
+
+instance Ordered Func where
+  lessIn = Ord.lessIn
+  lessEq = Ord.lessEq
+  lessEqSkolem = Ord.lessEqSkolem
+
+instance Function f => Arbitrary (Model f) where
+  arbitrary = fmap (modelFromOrder . map Variable . nub) arbitrary
+  shrink = weakenModel
+
+{-
+prop_1 :: Model Func -> Pair Func -> Subst Func -> Property
+prop_1 model (Pair t u) sub =
+  counterexample ("Model: " ++ prettyShow model) $
+  counterexample ("Subst: " ++ prettyShow sub) $
+  conjoin $ do
+    let cp = CriticalPair (t :=: u) 0 Nothing (axiom (Axiom 0 "dummy" (t :=: u)))
+    r@(Rule _ t' u') <- map orient (map cp_eqn (split cp))
+    return $
+      counterexample ("LHS:   " ++ prettyShow t') $
+      counterexample ("RHS:   " ++ prettyShow u') $
+      counterexample ("Rule:  " ++ prettyShow r) $
+      counterexample ("Inst:  " ++ prettyShow (Rule Oriented (subst sub t') (subst sub u'))) $
+      counterexample ("Res:   " ++ show (lessIn model (subst sub u') (subst sub t'))) $
+      not (reducesInModel model r sub) || isJust (lessIn model (subst sub u') (subst sub t'))
+-}
+
+prop_2 :: Model Func -> Pair Func -> Bool
+prop_2 model (Pair t u) =
+  not (lessIn model t u == Just Strict && isJust (lessIn model u t))
+
+prop_3 :: Pair Func -> Bool
+prop_3 (Pair t u) =
+  not (lessThan t u && lessEq u t)
+
+prop_4 :: Pair Func -> Property
+prop_4 (Pair t u) =
+  t /= u ==> 
+  not (lessEq t u && lessEq u t)
+
+prop_5 :: Term Func -> Property
+prop_5 t =
+  lessEq t t .&&. not (lessThan t t)
+
+prop_paths :: Term Func -> Property
+prop_paths t =
+  forAllShrink (choose (0, len t-1)) shrink $ \n ->
+    counterexample (show (positionToPath t n)) $
+    pathToPosition t (positionToPath t n) === n
+
+prop_index :: [Term Func] -> Term Func -> Property
+prop_index ts u =
+  counterexample (show ts') $
+  counterexample (show idx) $
+  sort (catMaybes [fmap (,t) (match t u) | t <- ts']) ===
+  sort (Index.matches u idx)
+  where
+    idx = foldr (\t -> Index.insert t t) Index.empty ts
+    ts' = map canonicalise ts
+
+newtype Terms f = Terms [Term f] deriving Show
+instance (Labelled f, Ord f, Typeable f, Arbitrary f, Arity f) => Arbitrary (Terms f) where
+  arbitrary = Terms <$> arbitrary
+  shrink (Terms ts) =
+    map Terms $
+      filter (/= ts) $
+      shrink ts ++ [canonicalise ts] ++ shrinkList (return . canonicalise) ts
+
+newtype IndexOps f = IndexOps [IndexOp f] deriving Show
+data IndexOp f = Add (Term f) | Delete (Term f) deriving Show
+
+instance (Labelled f, Ord f, Typeable f, Arbitrary f, Arity f) => Arbitrary (IndexOps f) where
+  arbitrary =
+    sized $ \n -> IndexOps <$> take n <$> arbOps []
+    where
+      arbOps ts =
+        frequency $
+          [(2, do { t <- arbitrary; ops <- arbOps (t:ts); return (Add t:ops) })] ++
+          [(1, do { t <- elements ts; ops <- arbOps (delete t ts); return (Delete t:ops) }) | not (null ts)]
+  shrink (IndexOps ops) =
+    IndexOps <$> shrinkList shr ops
+    where
+      shr (Add t) = Add <$> shrink t
+      shr (Delete t) = Delete <$> shrink t
+
+
+prop_index_invariant :: IndexOps Func -> Property
+prop_index_invariant (IndexOps ops) =
+  flip (foldr (counterexample . show)) idxs $
+  property $ Index.invariant (last idxs)
+  where
+    idxs = scanl (\idx op -> applyIndex op idx) Index.empty ops
+    applyIndex (Add t) = Index.insert t t
+    applyIndex (Delete t) = Index.delete t t
+
+deriving instance Eq Symbol
+deriving instance Generic Symbol
+
+instance Arbitrary Symbol where
+  arbitrary =
+    Symbol <$>
+      arbitrary <*>
+      fmap getLarge arbitrary <*>
+      (fmap (fromIntegral . getLarge) (arbitrary :: Gen (Large Int32)) `suchThat` (> 0) `suchThat` (< 2^31))
+  shrink s =
+    filter ok (genericShrink s)
+    where
+      ok s = Twee.Term.Core.size s > 0
+
+prop_symbol_1 :: Symbol -> Property
+prop_symbol_1 s =
+  withMaxSuccess 100000 $
+  counterexample ("fun/index/size = " ++ show (isFun s, index s, Twee.Term.Core.size s)) $
+  counterexample ("n = " ++ show (fromSymbol s)) $
+  toSymbol (fromSymbol s) === twiddle s
+  where
+    twiddle s =
+      s { index = fromIntegral (fromIntegral (index s) :: Int32) }
+
+prop_symbol_2 :: Int64 -> Property
+prop_symbol_2 n =
+  withMaxSuccess 100000 $
+  fromSymbol (toSymbol n) === n
+
+prop_canonorder :: Equation Func -> Property
+prop_canonorder eqn@(t :=: u) =
+  let vs = usort (vars eqn) in
+  forAll (shuffle vs) $ \ws swap (NonNegative n) ->
+    let
+      Just sub = listToSubst (zip vs [build (var (V (w + n))) | V w <- ws])
+      eqn' = subst sub (if swap then u :=: t else t :=: u)
+    in
+      canonicalise (order eqn) === canonicalise (order eqn')
+
+prop_canonorder2 :: Equation Func -> Equation Func -> Bool
+prop_canonorder2 eqn1 eqn2 =
+  eqn1 `simplerThan` eqn2 || eqn2 `simplerThan` eqn1 || order eqn1 == order eqn2
+
+prop_canonorder3 :: Equation Func -> Property
+prop_canonorder3 eq =
+  let eq' = order eq in
+  counterexample (show eq) $
+  Ord.size (eqn_lhs eq') >= Ord.size (eqn_rhs eq')
+
+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)])
diff --git a/misc/print_trace.pl b/misc/print_trace.pl
new file mode 100644
--- /dev/null
+++ b/misc/print_trace.pl
@@ -0,0 +1,50 @@
+rules(Module, Rule, Used) :-
+    %(Module:step(add(rule(_, Rule))); Module:step(add(rule(_, Rule, _, _)))),
+    Module:step(add(rule(_, Rule, _, _))),
+    (find_lemma(Module, Rule) -> Used=true; Used=false).
+
+find_lemma(Module, Rule) :-
+    copy_term(Rule, GroundRule), numbervars(GroundRule),
+    clause(Module:lemma(GroundRule), true, Ref),
+    clause(Module:lemma(Lemma), true, Ref),
+    Rule =@= Lemma.
+
+anywhere(Module, T) :-
+    Module:goal(T); Module:axiom(T); rules(Module, T, _).
+
+module_var(Module, X) :-
+    anywhere(Module, T),
+    term_variables(T, Xs),
+    numbervars(Xs),
+    member(X, Xs).
+
+all_vars(Module, S) :-
+    setof(X, module_var(Module, X), S).
+
+module_func(Where, X/N) :-
+    call(Where, T),
+    sub_term(U, T),
+    nonvar(U),
+    functor(U, X, N),
+    X \= '='.
+
+module_func_with_count(Module, F, AxiomCount, GoalCount) :-
+    module_func(anywhere(Module), F),
+    once(setof(_, module_func(Module:axiom, F), S1); S1=[]),
+    once(setof(_, module_func(Module:goal, F), S2); S2=[]),
+    length(S1, AxiomCount),
+    length(S2, GoalCount).
+
+all_funcs(Module, S) :-
+    setof(X/AxiomCount/GoalCount, module_func_with_count(Module, X, AxiomCount, GoalCount), S).
+
+print_trace(Module) :-
+    all_vars(Module, S),
+    all_funcs(Module, T),
+    writeln((vars, S)),
+    writeln((funcs, T)),
+    forall(Module:goal(Goal), (numbervars(Goal), writeln((goal, Goal)))),
+    forall(Module:axiom(Axiom), (numbervars(Axiom), writeln((axiom, Axiom)))),
+    forall(rules(Module, Rule, Used), (numbervars(Rule), writeln((Used, Rule)))).
+
+init :- writeln(hello).
diff --git a/misc/test.hs b/misc/test.hs
deleted file mode 100644
--- a/misc/test.hs
+++ /dev/null
@@ -1,161 +0,0 @@
-{-# LANGUAGE TemplateHaskell, FlexibleInstances, FlexibleContexts, UndecidableInstances, StandaloneDeriving, ScopedTypeVariables, TupleSections, DeriveGeneric #-}
-import Twee.Constraints
-import Twee.Term hiding (subst, canonicalise, F)
-import Twee.Term.Core hiding (F)
-import Test.QuickCheck hiding (Function, Fun)
-import Test.QuickCheck.All
-import Twee.Pretty
-import Twee.CP
-import Twee.Proof
-import qualified Twee.KBO as Ord
-import Text.PrettyPrint
-import Twee.Base hiding (F)
-import Twee.Rule
-import Twee.Equation
-import Control.Monad
-import qualified Data.Map as Map
-import Data.Maybe
-import Data.Ord
-import Data.List
-import Data.Typeable
-import qualified Twee.Index as Index
-import Data.Int
-import GHC.Generics
-
-newtype Func = F Int deriving (Eq, Ord, Show)
-
-instance Pretty Func where 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)
-instance Minimal Func where
-  minimal = fun (F 0)
-instance Sized Func where size _ = 1
-instance Arity Func where
-  arity (F 0) = 0
-  arity (F 1) = 2
-instance Skolem Func
-instance EqualsBonus Func
-
-instance Arbitrary Var where arbitrary = fmap V (choose (0, 3))
-instance (Ord f, Typeable f, Arbitrary f) => Arbitrary (Fun f) where
-  arbitrary = fmap fun arbitrary
-
-instance (Ord f, Typeable f, Arbitrary f, Sized f, Arity f) => Arbitrary (Term f) where
-  arbitrary =
-    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 ]
-  shrink (App f ts0) =
-    ts ++ (build <$> app f <$> shrinkOne ts)
-    where
-      ts = unpack ts0
-      shrinkOne [] = []
-      shrinkOne (x:xs) =
-        [ y:xs | y <- shrink x ] ++
-        [ x:ys | ys <- shrinkOne xs ]
-  shrink _ = []
-
-data Pair f = Pair (Term f) (Term f) deriving Show
-
-instance (Ord f, Typeable f, Arbitrary f, Arity f, Sized f) => Arbitrary (Pair f) where
-  arbitrary = liftM2 Pair arbitrary arbitrary
-  shrink (Pair x y) =
-    [ Pair x' y  | x' <- shrink x ] ++
-    [ Pair x y'  | y' <- shrink y ] ++
-    [ Pair x' y' | x' <- shrink x, y' <- shrink y ]
-
-instance Ordered Func where
-  lessIn = Ord.lessIn
-  lessEq = Ord.lessEq
-
-instance Function f => Arbitrary (Model f) where
-  arbitrary = fmap (modelFromOrder . map Variable . nub) arbitrary
-  shrink = weakenModel
-
-prop_1 :: Model Func -> Pair Func -> Subst Func -> Property
-prop_1 model (Pair t u) sub =
-  counterexample ("Model: " ++ prettyShow model) $
-  counterexample ("Subst: " ++ prettyShow sub) $
-  conjoin $ do
-    let cp = CriticalPair (t :=: u) 0 Nothing (axiom (Axiom 0 "dummy" (t :=: u)))
-    r@(Rule _ t' u') <- map orient (map cp_eqn (split cp))
-    return $
-      counterexample ("LHS:   " ++ prettyShow t') $
-      counterexample ("RHS:   " ++ prettyShow u') $
-      counterexample ("Rule:  " ++ prettyShow r) $
-      counterexample ("Inst:  " ++ prettyShow (Rule Oriented (subst sub t') (subst sub u'))) $
-      counterexample ("Res:   " ++ show (lessIn model (subst sub u') (subst sub t'))) $
-      not (reducesInModel model r sub) || isJust (lessIn model (subst sub u') (subst sub t'))
-
-prop_2 :: Model Func -> Pair Func -> Bool
-prop_2 model (Pair t u) =
-  not (lessIn model t u == Just Strict && isJust (lessIn model u t))
-
-prop_3 :: Pair Func -> Bool
-prop_3 (Pair t u) =
-  not (lessThan t u && lessEq u t)
-
-prop_4 :: Pair Func -> Property
-prop_4 (Pair t u) =
-  t /= u ==> 
-  not (lessEq t u && lessEq u t)
-
-prop_5 :: Term Func -> Property
-prop_5 t =
-  lessEq t t .&&. not (lessThan t t)
-
-prop_paths :: Term Func -> Property
-prop_paths t =
-  forAllShrink (choose (0, len t-1)) shrink $ \n ->
-    counterexample (show (positionToPath t n)) $
-    pathToPosition t (positionToPath t n) === n
-
-deriving instance Ord f => Ord (Subst f)
-
-prop_index :: [Term Func] -> Term Func -> Property
-prop_index ts u =
-  counterexample (show ts) $
-  counterexample (show idx) $
-  sort (catMaybes [fmap (,t) (match t u) | t <- ts]) ===
-  sort (Index.matches u idx)
-  where
-    idx = foldr (\t -> Index.insert t t) Index.empty ts
-
-deriving instance Eq Symbol
-deriving instance Generic Symbol
-
-instance Arbitrary Symbol where
-  arbitrary =
-    Symbol <$>
-      arbitrary <*>
-      fmap getLarge arbitrary <*>
-      (fmap (fromIntegral . getLarge) (arbitrary :: Gen (Large Int32)) `suchThat` (> 0) `suchThat` (< 2^31))
-  shrink s =
-    filter ok (genericShrink s)
-    where
-      ok s = Twee.Term.Core.size s > 0
-
-prop_symbol_1 :: Symbol -> Property
-prop_symbol_1 s =
-  withMaxSuccess 100000 $
-  counterexample ("fun/index/size = " ++ show (isFun s, index s, Twee.Term.Core.size s)) $
-  counterexample ("n = " ++ show (fromSymbol s)) $
-  toSymbol (fromSymbol s) === twiddle s
-  where
-    twiddle s =
-      s { index = fromIntegral (fromIntegral (index s) :: Int32) }
-
-prop_symbol_2 :: Int64 -> Property
-prop_symbol_2 n =
-  withMaxSuccess 100000 $
-  fromSymbol (toSymbol n) === n
-
-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)])
diff --git a/tests/GRP196-1.p b/tests/GRP196-1.p
new file mode 100644
--- /dev/null
+++ b/tests/GRP196-1.p
@@ -0,0 +1,40 @@
+%--------------------------------------------------------------------------
+% File     : GRP196-1 : TPTP v7.4.0. Released v2.2.0.
+% Domain   : Group Theory (Semigroups)
+% Problem  : In semigroups, xyyy=yyyx -> (uy)^9 = u^9v^9.
+% Version  : [MP96] (equality) axioms.
+% English  :
+
+% Refs     : [McC98] McCune (1998), Email to G. Sutcliffe
+%          : [MP96]  McCune & Padmanabhan (1996), Automated Deduction in Eq
+%          : [McC95] McCune (1995), Four Challenge Problems in Equational L
+% Source   : [McC98]
+% Names    : CS-3 [MP96]
+%          : Problem B [McC95]
+
+% Status   : Unsatisfiable
+% Rating   : 0.88 v7.4.0, 0.91 v7.3.0, 0.89 v7.0.0, 0.95 v6.4.0, 1.00 v4.0.1, 0.93 v4.0.0, 0.92 v3.7.0, 0.89 v3.4.0, 1.00 v3.3.0, 0.93 v3.1.0, 1.00 v2.2.1
+% Syntax   : Number of clauses     :    3 (   0 non-Horn;   3 unit;   1 RR)
+%            Number of atoms       :    3 (   3 equality)
+%            Maximal clause size   :    1 (   1 average)
+%            Number of predicates  :    1 (   0 propositional; 2-2 arity)
+%            Number of functors    :    3 (   2 constant; 0-2 arity)
+%            Number of variables   :    5 (   0 singleton)
+%            Maximal term depth    :   18 (   8 average)
+% SPC      : CNF_UNS_RFO_PEQ_UEQ
+
+% Comments : The problem was originally posed for cancellative semigroups,
+%            Otter does this with a nonstandard representation [MP96].
+%--------------------------------------------------------------------------
+%----Include semigroups axioms
+include('Axioms/GRP008-0.ax').
+%--------------------------------------------------------------------------
+%----Hypothesis:
+cnf(condition,hypothesis,
+    ( '*'(X,'*'(Y,'*'(Y,Y))) = '*'(Y,'*'(Y,'*'(Y,X))) )).
+
+%----Denial of conclusion:
+cnf(prove_this,negated_conjecture,
+    (  '*'(a,'*'(b,'*'(a,'*'(b,'*'(a,'*'(b,'*'(a,'*'(b,'*'(a,'*'(b,'*'(a,'*'(b,'*'(a,'*'(b,'*'(a,'*'(b,'*'(a,b))))))))))))))))) != '*'(a,'*'(a,'*'(a,'*'(a,'*'(a,'*'(a,'*'(a,'*'(a,'*'(a,'*'(b,'*'(b,'*'(b,'*'(b,'*'(b,'*'(b,'*'(b,'*'(b,b))))))))))))))))) )).
+
+%--------------------------------------------------------------------------
diff --git a/tests/RNG025-buggy.p b/tests/RNG025-buggy.p
new file mode 100644
--- /dev/null
+++ b/tests/RNG025-buggy.p
@@ -0,0 +1,9 @@
+% SPASS solves this instantly, Twee takes ages!
+cnf(axiom, axiom, multiply(U,add(V,W))=add(multiply(U,V),multiply(U,W))).
+cnf(axiom, axiom, add(U,additive_inverse(add(additive_inverse(V),U)))=V).
+cnf(axiom, axiom, add(U,additive_inverse(add(V,add(W,U))))=additive_inverse(add(V,W))).
+cnf(axiom, axiom, add(additive_inverse(U),V)=additive_inverse(add(U,additive_inverse(V)))).
+cnf(axiom, axiom, multiply(multiply(U,V),W)=add(associator(U,V,W),multiply(U,multiply(V,W)))).
+cnf(axiom, axiom, additive_inverse(add(multiply(U,multiply(V,W)),add(multiply(U,multiply(X,W)),additive_inverse(add(multiply(multiply(U,V),W),multiply(multiply(U,X),W))))))=associator(U,add(V,X),W)).
+
+cnf(conjecture, conjecture, add(associator(U,V,W),associator(U,X,W))=associator(U,add(V,X),W)).
diff --git a/tests/append-rev-ascii.p b/tests/append-rev-ascii.p
deleted file mode 100644
--- a/tests/append-rev-ascii.p
+++ /dev/null
@@ -1,4 +0,0 @@
-fof(rev_rev, axiom, ![X]: rev(rev(X))=X).
-fof(app_assoc, axiom, ![X, Y, Z]: '++'(X, '++'(Y, Z))='++'('++'(X, Y), Z)).
-fof(rev_app, axiom, ![X, Y]: '++'(rev(X), rev(Y))=rev('++'(Y, X))).
-fof(conjecture, conjecture, '++'(a, rev(b))=rev('++'(b, rev(a)))).
diff --git a/tests/blah.p b/tests/blah.p
deleted file mode 100644
--- a/tests/blah.p
+++ /dev/null
@@ -1,5 +0,0 @@
-cnf(plus_comm, axiom, '+'(X, Y) = '+'(Y, X)).
-cnf(plus_assoc, axiom, '+'(X, '+'(Y, Z)) = '+'('+'(X, Y), Z)).
-cnf(plus_zero, axiom, '+'('0', X) = X).
-cnf(plus_inv, axiom, '+'(X, '-'(X)) = '0').
-cnf(conjecture, negated_conjecture, '*'(a, b) != '*'(b, a)).
diff --git a/tests/db.p b/tests/db.p
deleted file mode 100644
--- a/tests/db.p
+++ /dev/null
@@ -1,28 +0,0 @@
-% http://www.dcs.bbk.ac.uk/~szabolcs/rellat-jlamp-second-submission-2.pdf
-% appendix b. theorem 3.4, clause 8.
-cnf(commutativity, axiom,
-    X ∧ Y = Y ∧ X).
-cnf(associativity, axiom,
-    X ∧ (Y ∧ Z) = (X ∧ Y) ∧ Z).
-cnf(commutativity, axiom,
-    X ∨ Y = Y ∨ X).
-cnf(associativity, axiom,
-    X ∨ (Y ∨ Z) = (X ∨ Y) ∨ Z).
-cnf(absorption, axiom,
-    X ∨ (X ∧ Y) = X).
-cnf(absorption, axiom,
-    X ∧ (X ∨ Y) = X).
-cnf('definition of upme', axiom,
-    upme(X,Y,Z) = X ∧ (Y ∨ Z)).
-cnf('definition of lome', axiom,
-    lome(X,Y,Z) = (X ∧ Y) ∨ (X ∧ Z)).
-%cnf('definition of upjo', axiom,
-%    upjo(X,Y,Z) = (X ∨ Y) ∧ (X ∨ Z)).
-%cnf('definition of lojo' axiom,
-%    lojo(X,Y,Z) = X ∨ (Y ∧ Z)).
-cnf('upme property 1', axiom,
-    upme(a ∧ X1,Y1,Z1) ∨ (Y1 ∧ Z1) = (((a ∧ X1) ∧ Y1) ∨ Z1) ∧ (((a ∧ X1) ∧ Z1) ∨ Y1)).
-cnf('upme property 2', axiom,
-    upme(X,Y,Z) = upme(X,Y,a ∧ Z) ∨ upme(X,Z,a ∧ Y)).
-fof(conjecture, conjecture,
-    upme(a,x2,y2) = upme(a,x2,z2) => upme(x2,y2,z2) = lome(x2,y2,z2)).
diff --git a/tests/db2.p b/tests/db2.p
deleted file mode 100644
--- a/tests/db2.p
+++ /dev/null
@@ -1,29 +0,0 @@
-% http://www.dcs.bbk.ac.uk/~szabolcs/rellat-jlamp-second-submission-2.pdf
-% appendix b. theorem 3.4, clause 8.
-cnf(commutativity, axiom,
-    X ∧ Y = Y ∧ X).
-cnf(associativity, axiom,
-    X ∧ (Y ∧ Z) = (X ∧ Y) ∧ Z).
-cnf(commutativity, axiom,
-    X ∨ Y = Y ∨ X).
-cnf(associativity, axiom,
-    X ∨ (Y ∨ Z) = (X ∨ Y) ∨ Z).
-cnf(absorption, axiom,
-    X ∨ (X ∧ Y) = X).
-cnf(absorption, axiom,
-    X ∧ (X ∨ Y) = X).
-cnf('definition of upme', axiom,
-    upme(X,Y,Z) = X ∧ (Y ∨ Z)).
-cnf('definition of lome', axiom,
-    lome(X,Y,Z) = (X ∧ Y) ∨ (X ∧ Z)).
-cnf('definition of upjo', axiom,
-    upjo(X,Y,Z) = (X ∨ Y) ∧ (X ∨ Z)).
-cnf('definition of lojo', axiom,
-    lojo(X,Y,Z) = X ∨ (Y ∧ Z)).
-cnf('upme property 1', axiom,
-    ((a ∧ X1) ∧ (Y1 ∨ Z1)) ∨ (Y1 ∧ Z1) = (((a ∧ X1) ∧ Y1) ∨ Z1) ∧ (((a ∧ X1) ∧ Z1) ∨ Y1)).
-cnf('upme property 2', axiom,
-    X ∧ (Y ∨ Z) = (X ∧ (Y ∨ (a ∧ Z))) ∨ (X ∧ (Z ∨ (a ∧ Y)))).
-fof(conjecture, conjecture,
-    a ∧ (x2 ∨ y2) = a ∧ (x2 ∨ z2) =>
-    x2 ∧ (y2 ∨ z2) = (x2 ∧ y2) ∨ (x2 ∧ z2)).
diff --git a/tests/gmv1-ascii.p b/tests/gmv1-ascii.p
deleted file mode 100644
--- a/tests/gmv1-ascii.p
+++ /dev/null
@@ -1,19 +0,0 @@
-fof('Associativity-and', axiom, ![X, Y, Z]: 'and'('and'(X, Y), Z)='and'(X, 'and'(Y, Z))).
-fof('Associativity-or', axiom, ![X, Y, Z]: 'or'('or'(X, Y), Z)='or'(X, 'or'(Y, Z))).
-fof('Idempotence-and', axiom, ![X]: 'and'(X, X)=X).
-fof('Idempotence-or', axiom, ![X]: 'or'(X, X)=X).
-fof('Commutativity-and', axiom, ![X, Y]: 'and'(X, Y)='and'(Y, X)).
-fof('Commutativity-or', axiom, ![X, Y]: 'or'(X, Y)='or'(Y, X)).
-fof('Absorption a', axiom, ![X, Y]: 'or'('and'(X, Y), X)=X).
-fof('Absorption b', axiom, ![X, Y]: 'and'('or'(X, Y), X)=X).
-fof('Residual a', axiom, ![X, Y, Z]: 'or'('*'(X, 'and'('\\'(X, Z), Y)), Z)=Z).
-fof('Residual b', axiom, ![X, Y, Z]: 'or'('*'('and'(Y, '/'(Z, X)), X), Z)=Z).
-fof('Residual c', axiom, ![X, Y, Z]: 'and'('\\'(X, 'or'('*'(X, Y), Z)), Y)=Y).
-fof('Residual d', axiom, ![X, Y, Z]: 'and'('/'('or'('*'(Y, X), Z), X), Y)=Y).
-fof('Associativity-* (fusion)', axiom, ![X, Y, Z]: '*'('*'(X, Y), Z)='*'(X, '*'(Y, Z))).
-fof('Left monoid unit', axiom, ![X]: '*'('1', X)=X).
-fof('Right monoid unit', axiom, ![X]: '*'(X, '1')=X).
-fof('GMV a', axiom, ![X, Y]: 'or'(X, Y)='/'(X, '\\'('or'(X, Y), X))).
-fof('GMV b', axiom, ![X, Y]: 'or'(X, Y)='\\'('/'(X, 'or'(X, Y)), X)).
-fof('Definition-@', axiom, ![X, Y]: '@'(X, Y)='*'('*'(X, '\\'(X, '1')), '\\'('\\'(Y, '1'), '1'))).
-fof('Goal 1', conjecture, '@'(x, x)=x).
diff --git a/tests/gmv1.p b/tests/gmv1.p
deleted file mode 100644
--- a/tests/gmv1.p
+++ /dev/null
@@ -1,46 +0,0 @@
-cnf('Associativity-∧', axiom,
-    (X ∧ Y) ∧ Z = X ∧ (Y ∧ Z)).   
-cnf('Associativity-∨', axiom,
-    (X ∨ Y) ∨ Z = X ∨ (Y ∨ Z)).
-cnf('Idempotence-∧', axiom,
-    X ∧ X = X).
-cnf('Idempotence-∨', axiom,
-    X ∨ X = X).
-cnf('Commutativity-∧', axiom,
-    X ∧ Y = Y ∧ X).
-cnf('Commutativity-∨', axiom,
-    X ∨ Y = Y ∨ X).
-cnf('Absorption a', axiom,
-    (X ∧ Y) ∨ X = X).
-cnf('Absorption b', axiom,
-    (X ∨ Y) ∧ X = X).
-
-cnf('Residual a', axiom,
-    (X * ((X \ Z) ∧ Y)) ∨ Z = Z).
-cnf('Residual b', axiom,
-    ((Y ∧ (Z / X)) * X) ∨ Z = Z).
-cnf('Residual c', axiom,
-    (X \ ((X * Y) ∨ Z)) ∧ Y = Y).
-cnf('Residual d', axiom,
-    (((Y * X) ∨ Z) / X) ∧ Y = Y).
-
-cnf('Associativity-* (fusion)', axiom,
-    (X * Y) * Z = X * (Y * Z)).
-cnf('Left monoid unit', axiom,
-    '1' * X = X).
-cnf('Right monoid unit', axiom,
-    X * '1' = X).
-
-cnf('GMV a', axiom,
-    X ∨ Y = X / ((X ∨ Y) \ X)).
-cnf('GMV b', axiom,
-    X ∨ Y = (X / (X ∨ Y)) \ X).
-
-cnf('Definition-@', axiom,
-    X @ Y = (X * (X \ '1')) * ((Y \ '1') \ '1')).
-
-cnf('Goal 1', conjecture,
-    x @ x = x).
-  
-  
-  
diff --git a/tests/gmv10-ascii.p b/tests/gmv10-ascii.p
deleted file mode 100644
--- a/tests/gmv10-ascii.p
+++ /dev/null
@@ -1,19 +0,0 @@
-fof('Associativity-and', axiom, ![X, Y, Z]: 'and'('and'(X, Y), Z)='and'(X, 'and'(Y, Z))).
-fof('Associativity-or', axiom, ![X, Y, Z]: 'or'('or'(X, Y), Z)='or'(X, 'or'(Y, Z))).
-fof('Idempotence-and', axiom, ![X]: 'and'(X, X)=X).
-fof('Idempotence-or', axiom, ![X]: 'or'(X, X)=X).
-fof('Commutativity-and', axiom, ![X, Y]: 'and'(X, Y)='and'(Y, X)).
-fof('Commutativity-or', axiom, ![X, Y]: 'or'(X, Y)='or'(Y, X)).
-fof('Absorption a', axiom, ![X, Y]: 'or'('and'(X, Y), X)=X).
-fof('Absorption b', axiom, ![X, Y]: 'and'('or'(X, Y), X)=X).
-fof('Residual a', axiom, ![X, Y, Z]: 'or'('*'(X, 'and'('\\'(X, Z), Y)), Z)=Z).
-fof('Residual b', axiom, ![X, Y, Z]: 'or'('*'('and'(Y, '/'(Z, X)), X), Z)=Z).
-fof('Residual c', axiom, ![X, Y, Z]: 'and'('\\'(X, 'or'('*'(X, Y), Z)), Y)=Y).
-fof('Residual d', axiom, ![X, Y, Z]: 'and'('/'('or'('*'(Y, X), Z), X), Y)=Y).
-fof('Associativity-* (fusion)', axiom, ![X, Y, Z]: '*'('*'(X, Y), Z)='*'(X, '*'(Y, Z))).
-fof('Left monoid unit', axiom, ![X]: '*'('1', X)=X).
-fof('Right monoid unit', axiom, ![X]: '*'(X, '1')=X).
-fof('GMV a', axiom, ![X, Y]: 'or'(X, Y)='/'(X, '\\'('or'(X, Y), X))).
-fof('GMV b', axiom, ![X, Y]: 'or'(X, Y)='\\'('/'(X, 'or'(X, Y)), X)).
-fof('Definition-@', axiom, ![X, Y]: '@'(X, Y)='*'('*'(X, '\\'(X, '1')), '\\'('\\'(Y, '1'), '1'))).
-fof('Goal 10', conjecture, '@'('\\'(x, '1'), '1')='1').
diff --git a/tests/gmv10.p b/tests/gmv10.p
deleted file mode 100644
--- a/tests/gmv10.p
+++ /dev/null
@@ -1,46 +0,0 @@
-cnf('Associativity-∧', axiom,
-    (X ∧ Y) ∧ Z = X ∧ (Y ∧ Z)).   
-cnf('Associativity-∨', axiom,
-    (X ∨ Y) ∨ Z = X ∨ (Y ∨ Z)).
-cnf('Idempotence-∧', axiom,
-    X ∧ X = X).
-cnf('Idempotence-∨', axiom,
-    X ∨ X = X).
-cnf('Commutativity-∧', axiom,
-    X ∧ Y = Y ∧ X).
-cnf('Commutativity-∨', axiom,
-    X ∨ Y = Y ∨ X).
-cnf('Absorption a', axiom,
-    (X ∧ Y) ∨ X = X).
-cnf('Absorption b', axiom,
-    (X ∨ Y) ∧ X = X).
-
-cnf('Residual a', axiom,
-    (X * ((X \ Z) ∧ Y)) ∨ Z = Z).
-cnf('Residual b', axiom,
-    ((Y ∧ (Z / X)) * X) ∨ Z = Z).
-cnf('Residual c', axiom,
-    (X \ ((X * Y) ∨ Z)) ∧ Y = Y).
-cnf('Residual d', axiom,
-    (((Y * X) ∨ Z) / X) ∧ Y = Y).
-
-cnf('Associativity-* (fusion)', axiom,
-    (X * Y) * Z = X * (Y * Z)).
-cnf('Left monoid unit', axiom,
-    '1' * X = X).
-cnf('Right monoid unit', axiom,
-    X * '1' = X).
-
-cnf('GMV a', axiom,
-    X ∨ Y = X / ((X ∨ Y) \ X)).
-cnf('GMV b', axiom,
-    X ∨ Y = (X / (X ∨ Y)) \ X).
-
-cnf('Definition-@', axiom,
-    X @ Y = (X * (X \ '1')) * ((Y \ '1') \ '1')).
-
-  
-  
-cnf('Goal 10', conjecture,
-    (x \ '1') @ '1' = '1').
-  
diff --git a/tests/gmv11-ascii.p b/tests/gmv11-ascii.p
deleted file mode 100644
--- a/tests/gmv11-ascii.p
+++ /dev/null
@@ -1,19 +0,0 @@
-fof('Associativity-and', axiom, ![X, Y, Z]: 'and'('and'(X, Y), Z)='and'(X, 'and'(Y, Z))).
-fof('Associativity-or', axiom, ![X, Y, Z]: 'or'('or'(X, Y), Z)='or'(X, 'or'(Y, Z))).
-fof('Idempotence-and', axiom, ![X]: 'and'(X, X)=X).
-fof('Idempotence-or', axiom, ![X]: 'or'(X, X)=X).
-fof('Commutativity-and', axiom, ![X, Y]: 'and'(X, Y)='and'(Y, X)).
-fof('Commutativity-or', axiom, ![X, Y]: 'or'(X, Y)='or'(Y, X)).
-fof('Absorption a', axiom, ![X, Y]: 'or'('and'(X, Y), X)=X).
-fof('Absorption b', axiom, ![X, Y]: 'and'('or'(X, Y), X)=X).
-fof('Residual a', axiom, ![X, Y, Z]: 'or'('*'(X, 'and'('\\'(X, Z), Y)), Z)=Z).
-fof('Residual b', axiom, ![X, Y, Z]: 'or'('*'('and'(Y, '/'(Z, X)), X), Z)=Z).
-fof('Residual c', axiom, ![X, Y, Z]: 'and'('\\'(X, 'or'('*'(X, Y), Z)), Y)=Y).
-fof('Residual d', axiom, ![X, Y, Z]: 'and'('/'('or'('*'(Y, X), Z), X), Y)=Y).
-fof('Associativity-* (fusion)', axiom, ![X, Y, Z]: '*'('*'(X, Y), Z)='*'(X, '*'(Y, Z))).
-fof('Left monoid unit', axiom, ![X]: '*'('1', X)=X).
-fof('Right monoid unit', axiom, ![X]: '*'(X, '1')=X).
-fof('GMV a', axiom, ![X, Y]: 'or'(X, Y)='/'(X, '\\'('or'(X, Y), X))).
-fof('GMV b', axiom, ![X, Y]: 'or'(X, Y)='\\'('/'(X, 'or'(X, Y)), X)).
-fof('Definition-@', axiom, ![X, Y]: '@'(X, Y)='*'('*'(X, '\\'(X, '1')), '\\'('\\'(Y, '1'), '1'))).
-fof('Goal 11', conjecture, '@'('1', '\\'(x, '1'))='\\'(x, '1')).
diff --git a/tests/gmv11.p b/tests/gmv11.p
deleted file mode 100644
--- a/tests/gmv11.p
+++ /dev/null
@@ -1,46 +0,0 @@
-cnf('Associativity-∧', axiom,
-    (X ∧ Y) ∧ Z = X ∧ (Y ∧ Z)).   
-cnf('Associativity-∨', axiom,
-    (X ∨ Y) ∨ Z = X ∨ (Y ∨ Z)).
-cnf('Idempotence-∧', axiom,
-    X ∧ X = X).
-cnf('Idempotence-∨', axiom,
-    X ∨ X = X).
-cnf('Commutativity-∧', axiom,
-    X ∧ Y = Y ∧ X).
-cnf('Commutativity-∨', axiom,
-    X ∨ Y = Y ∨ X).
-cnf('Absorption a', axiom,
-    (X ∧ Y) ∨ X = X).
-cnf('Absorption b', axiom,
-    (X ∨ Y) ∧ X = X).
-
-cnf('Residual a', axiom,
-    (X * ((X \ Z) ∧ Y)) ∨ Z = Z).
-cnf('Residual b', axiom,
-    ((Y ∧ (Z / X)) * X) ∨ Z = Z).
-cnf('Residual c', axiom,
-    (X \ ((X * Y) ∨ Z)) ∧ Y = Y).
-cnf('Residual d', axiom,
-    (((Y * X) ∨ Z) / X) ∧ Y = Y).
-
-cnf('Associativity-* (fusion)', axiom,
-    (X * Y) * Z = X * (Y * Z)).
-cnf('Left monoid unit', axiom,
-    '1' * X = X).
-cnf('Right monoid unit', axiom,
-    X * '1' = X).
-
-cnf('GMV a', axiom,
-    X ∨ Y = X / ((X ∨ Y) \ X)).
-cnf('GMV b', axiom,
-    X ∨ Y = (X / (X ∨ Y)) \ X).
-
-cnf('Definition-@', axiom,
-    X @ Y = (X * (X \ '1')) * ((Y \ '1') \ '1')).
-
-  
-  
-cnf('Goal 11', conjecture,
-    '1' @ (x \ '1') = x \ '1').
-  
diff --git a/tests/gmv12-ascii.p b/tests/gmv12-ascii.p
deleted file mode 100644
--- a/tests/gmv12-ascii.p
+++ /dev/null
@@ -1,19 +0,0 @@
-fof('Associativity-and', axiom, ![X, Y, Z]: 'and'('and'(X, Y), Z)='and'(X, 'and'(Y, Z))).
-fof('Associativity-or', axiom, ![X, Y, Z]: 'or'('or'(X, Y), Z)='or'(X, 'or'(Y, Z))).
-fof('Idempotence-and', axiom, ![X]: 'and'(X, X)=X).
-fof('Idempotence-or', axiom, ![X]: 'or'(X, X)=X).
-fof('Commutativity-and', axiom, ![X, Y]: 'and'(X, Y)='and'(Y, X)).
-fof('Commutativity-or', axiom, ![X, Y]: 'or'(X, Y)='or'(Y, X)).
-fof('Absorption a', axiom, ![X, Y]: 'or'('and'(X, Y), X)=X).
-fof('Absorption b', axiom, ![X, Y]: 'and'('or'(X, Y), X)=X).
-fof('Residual a', axiom, ![X, Y, Z]: 'or'('*'(X, 'and'('\\'(X, Z), Y)), Z)=Z).
-fof('Residual b', axiom, ![X, Y, Z]: 'or'('*'('and'(Y, '/'(Z, X)), X), Z)=Z).
-fof('Residual c', axiom, ![X, Y, Z]: 'and'('\\'(X, 'or'('*'(X, Y), Z)), Y)=Y).
-fof('Residual d', axiom, ![X, Y, Z]: 'and'('/'('or'('*'(Y, X), Z), X), Y)=Y).
-fof('Associativity-* (fusion)', axiom, ![X, Y, Z]: '*'('*'(X, Y), Z)='*'(X, '*'(Y, Z))).
-fof('Left monoid unit', axiom, ![X]: '*'('1', X)=X).
-fof('Right monoid unit', axiom, ![X]: '*'(X, '1')=X).
-fof('GMV a', axiom, ![X, Y]: 'or'(X, Y)='/'(X, '\\'('or'(X, Y), X))).
-fof('GMV b', axiom, ![X, Y]: 'or'(X, Y)='\\'('/'(X, 'or'(X, Y)), X)).
-fof('Definition-@', axiom, ![X, Y]: '@'(X, Y)='*'('*'(X, '\\'(X, '1')), '\\'('\\'(Y, '1'), '1'))).
-fof('Goal 12', conjecture, '@'('/'(x, '\\'(y, x)), 'or'(x, y))='or'(x, y)).
diff --git a/tests/gmv12.p b/tests/gmv12.p
deleted file mode 100644
--- a/tests/gmv12.p
+++ /dev/null
@@ -1,46 +0,0 @@
-cnf('Associativity-∧', axiom,
-    (X ∧ Y) ∧ Z = X ∧ (Y ∧ Z)).   
-cnf('Associativity-∨', axiom,
-    (X ∨ Y) ∨ Z = X ∨ (Y ∨ Z)).
-cnf('Idempotence-∧', axiom,
-    X ∧ X = X).
-cnf('Idempotence-∨', axiom,
-    X ∨ X = X).
-cnf('Commutativity-∧', axiom,
-    X ∧ Y = Y ∧ X).
-cnf('Commutativity-∨', axiom,
-    X ∨ Y = Y ∨ X).
-cnf('Absorption a', axiom,
-    (X ∧ Y) ∨ X = X).
-cnf('Absorption b', axiom,
-    (X ∨ Y) ∧ X = X).
-
-cnf('Residual a', axiom,
-    (X * ((X \ Z) ∧ Y)) ∨ Z = Z).
-cnf('Residual b', axiom,
-    ((Y ∧ (Z / X)) * X) ∨ Z = Z).
-cnf('Residual c', axiom,
-    (X \ ((X * Y) ∨ Z)) ∧ Y = Y).
-cnf('Residual d', axiom,
-    (((Y * X) ∨ Z) / X) ∧ Y = Y).
-
-cnf('Associativity-* (fusion)', axiom,
-    (X * Y) * Z = X * (Y * Z)).
-cnf('Left monoid unit', axiom,
-    '1' * X = X).
-cnf('Right monoid unit', axiom,
-    X * '1' = X).
-
-cnf('GMV a', axiom,
-    X ∨ Y = X / ((X ∨ Y) \ X)).
-cnf('GMV b', axiom,
-    X ∨ Y = (X / (X ∨ Y)) \ X).
-
-cnf('Definition-@', axiom,
-    X @ Y = (X * (X \ '1')) * ((Y \ '1') \ '1')).
-
-  
-  
-  
-cnf('Goal 12', conjecture,
-    (x / (y \ x)) @ (x ∨ y) = x ∨ y).
diff --git a/tests/gmv13-ascii.p b/tests/gmv13-ascii.p
deleted file mode 100644
--- a/tests/gmv13-ascii.p
+++ /dev/null
@@ -1,19 +0,0 @@
-fof('Associativity-and', axiom, ![X, Y, Z]: 'and'('and'(X, Y), Z)='and'(X, 'and'(Y, Z))).
-fof('Associativity-or', axiom, ![X, Y, Z]: 'or'('or'(X, Y), Z)='or'(X, 'or'(Y, Z))).
-fof('Idempotence-and', axiom, ![X]: 'and'(X, X)=X).
-fof('Idempotence-or', axiom, ![X]: 'or'(X, X)=X).
-fof('Commutativity-and', axiom, ![X, Y]: 'and'(X, Y)='and'(Y, X)).
-fof('Commutativity-or', axiom, ![X, Y]: 'or'(X, Y)='or'(Y, X)).
-fof('Absorption a', axiom, ![X, Y]: 'or'('and'(X, Y), X)=X).
-fof('Absorption b', axiom, ![X, Y]: 'and'('or'(X, Y), X)=X).
-fof('Residual a', axiom, ![X, Y, Z]: 'or'('*'(X, 'and'('\\'(X, Z), Y)), Z)=Z).
-fof('Residual b', axiom, ![X, Y, Z]: 'or'('*'('and'(Y, '/'(Z, X)), X), Z)=Z).
-fof('Residual c', axiom, ![X, Y, Z]: 'and'('\\'(X, 'or'('*'(X, Y), Z)), Y)=Y).
-fof('Residual d', axiom, ![X, Y, Z]: 'and'('/'('or'('*'(Y, X), Z), X), Y)=Y).
-fof('Associativity-* (fusion)', axiom, ![X, Y, Z]: '*'('*'(X, Y), Z)='*'(X, '*'(Y, Z))).
-fof('Left monoid unit', axiom, ![X]: '*'('1', X)=X).
-fof('Right monoid unit', axiom, ![X]: '*'(X, '1')=X).
-fof('GMV a', axiom, ![X, Y]: 'or'(X, Y)='/'(X, '\\'('or'(X, Y), X))).
-fof('GMV b', axiom, ![X, Y]: 'or'(X, Y)='\\'('/'(X, 'or'(X, Y)), X)).
-fof('Definition-@', axiom, ![X, Y]: '@'(X, Y)='*'('*'(X, '\\'(X, '1')), '\\'('\\'(Y, '1'), '1'))).
-fof('Goal 13', conjecture, '@'('\\'('/'(x, y), x), 'or'(x, y))='or'(x, y)).
diff --git a/tests/gmv13.p b/tests/gmv13.p
deleted file mode 100644
--- a/tests/gmv13.p
+++ /dev/null
@@ -1,46 +0,0 @@
-cnf('Associativity-∧', axiom,
-    (X ∧ Y) ∧ Z = X ∧ (Y ∧ Z)).   
-cnf('Associativity-∨', axiom,
-    (X ∨ Y) ∨ Z = X ∨ (Y ∨ Z)).
-cnf('Idempotence-∧', axiom,
-    X ∧ X = X).
-cnf('Idempotence-∨', axiom,
-    X ∨ X = X).
-cnf('Commutativity-∧', axiom,
-    X ∧ Y = Y ∧ X).
-cnf('Commutativity-∨', axiom,
-    X ∨ Y = Y ∨ X).
-cnf('Absorption a', axiom,
-    (X ∧ Y) ∨ X = X).
-cnf('Absorption b', axiom,
-    (X ∨ Y) ∧ X = X).
-
-cnf('Residual a', axiom,
-    (X * ((X \ Z) ∧ Y)) ∨ Z = Z).
-cnf('Residual b', axiom,
-    ((Y ∧ (Z / X)) * X) ∨ Z = Z).
-cnf('Residual c', axiom,
-    (X \ ((X * Y) ∨ Z)) ∧ Y = Y).
-cnf('Residual d', axiom,
-    (((Y * X) ∨ Z) / X) ∧ Y = Y).
-
-cnf('Associativity-* (fusion)', axiom,
-    (X * Y) * Z = X * (Y * Z)).
-cnf('Left monoid unit', axiom,
-    '1' * X = X).
-cnf('Right monoid unit', axiom,
-    X * '1' = X).
-
-cnf('GMV a', axiom,
-    X ∨ Y = X / ((X ∨ Y) \ X)).
-cnf('GMV b', axiom,
-    X ∨ Y = (X / (X ∨ Y)) \ X).
-
-cnf('Definition-@', axiom,
-    X @ Y = (X * (X \ '1')) * ((Y \ '1') \ '1')).
-
-  
-  
-  
-cnf('Goal 13', conjecture,
-    ((x / y) \ x) @ (x ∨ y) = x ∨ y).
diff --git a/tests/gmv14-ascii.p b/tests/gmv14-ascii.p
deleted file mode 100644
--- a/tests/gmv14-ascii.p
+++ /dev/null
@@ -1,19 +0,0 @@
-fof('Associativity-and', axiom, ![X, Y, Z]: 'and'('and'(X, Y), Z)='and'(X, 'and'(Y, Z))).
-fof('Associativity-or', axiom, ![X, Y, Z]: 'or'('or'(X, Y), Z)='or'(X, 'or'(Y, Z))).
-fof('Idempotence-and', axiom, ![X]: 'and'(X, X)=X).
-fof('Idempotence-or', axiom, ![X]: 'or'(X, X)=X).
-fof('Commutativity-and', axiom, ![X, Y]: 'and'(X, Y)='and'(Y, X)).
-fof('Commutativity-or', axiom, ![X, Y]: 'or'(X, Y)='or'(Y, X)).
-fof('Absorption a', axiom, ![X, Y]: 'or'('and'(X, Y), X)=X).
-fof('Absorption b', axiom, ![X, Y]: 'and'('or'(X, Y), X)=X).
-fof('Residual a', axiom, ![X, Y, Z]: 'or'('*'(X, 'and'('\\'(X, Z), Y)), Z)=Z).
-fof('Residual b', axiom, ![X, Y, Z]: 'or'('*'('and'(Y, '/'(Z, X)), X), Z)=Z).
-fof('Residual c', axiom, ![X, Y, Z]: 'and'('\\'(X, 'or'('*'(X, Y), Z)), Y)=Y).
-fof('Residual d', axiom, ![X, Y, Z]: 'and'('/'('or'('*'(Y, X), Z), X), Y)=Y).
-fof('Associativity-* (fusion)', axiom, ![X, Y, Z]: '*'('*'(X, Y), Z)='*'(X, '*'(Y, Z))).
-fof('Left monoid unit', axiom, ![X]: '*'('1', X)=X).
-fof('Right monoid unit', axiom, ![X]: '*'(X, '1')=X).
-fof('GMV a', axiom, ![X, Y]: 'or'(X, Y)='/'(X, '\\'('or'(X, Y), X))).
-fof('GMV b', axiom, ![X, Y]: 'or'(X, Y)='\\'('/'(X, 'or'(X, Y)), X)).
-fof('Definition-@', axiom, ![X, Y]: '@'(X, Y)='*'('*'(X, '\\'(X, '1')), '\\'('\\'(Y, '1'), '1'))).
-fof('Goal 14', conjecture, '@'('or'(x, y), '/'(x, '\\'(y, x)))='/'(x, '\\'(y, x))).
diff --git a/tests/gmv14.p b/tests/gmv14.p
deleted file mode 100644
--- a/tests/gmv14.p
+++ /dev/null
@@ -1,46 +0,0 @@
-cnf('Associativity-∧', axiom,
-    (X ∧ Y) ∧ Z = X ∧ (Y ∧ Z)).   
-cnf('Associativity-∨', axiom,
-    (X ∨ Y) ∨ Z = X ∨ (Y ∨ Z)).
-cnf('Idempotence-∧', axiom,
-    X ∧ X = X).
-cnf('Idempotence-∨', axiom,
-    X ∨ X = X).
-cnf('Commutativity-∧', axiom,
-    X ∧ Y = Y ∧ X).
-cnf('Commutativity-∨', axiom,
-    X ∨ Y = Y ∨ X).
-cnf('Absorption a', axiom,
-    (X ∧ Y) ∨ X = X).
-cnf('Absorption b', axiom,
-    (X ∨ Y) ∧ X = X).
-
-cnf('Residual a', axiom,
-    (X * ((X \ Z) ∧ Y)) ∨ Z = Z).
-cnf('Residual b', axiom,
-    ((Y ∧ (Z / X)) * X) ∨ Z = Z).
-cnf('Residual c', axiom,
-    (X \ ((X * Y) ∨ Z)) ∧ Y = Y).
-cnf('Residual d', axiom,
-    (((Y * X) ∨ Z) / X) ∧ Y = Y).
-
-cnf('Associativity-* (fusion)', axiom,
-    (X * Y) * Z = X * (Y * Z)).
-cnf('Left monoid unit', axiom,
-    '1' * X = X).
-cnf('Right monoid unit', axiom,
-    X * '1' = X).
-
-cnf('GMV a', axiom,
-    X ∨ Y = X / ((X ∨ Y) \ X)).
-cnf('GMV b', axiom,
-    X ∨ Y = (X / (X ∨ Y)) \ X).
-
-cnf('Definition-@', axiom,
-    X @ Y = (X * (X \ '1')) * ((Y \ '1') \ '1')).
-
-  
-  
-  
-cnf('Goal 14', conjecture,
-    (x ∨ y) @ (x / (y \ x)) = x / (y \ x)).
diff --git a/tests/gmv15-ascii.p b/tests/gmv15-ascii.p
deleted file mode 100644
--- a/tests/gmv15-ascii.p
+++ /dev/null
@@ -1,19 +0,0 @@
-fof('Associativity-and', axiom, ![X, Y, Z]: 'and'('and'(X, Y), Z)='and'(X, 'and'(Y, Z))).
-fof('Associativity-or', axiom, ![X, Y, Z]: 'or'('or'(X, Y), Z)='or'(X, 'or'(Y, Z))).
-fof('Idempotence-and', axiom, ![X]: 'and'(X, X)=X).
-fof('Idempotence-or', axiom, ![X]: 'or'(X, X)=X).
-fof('Commutativity-and', axiom, ![X, Y]: 'and'(X, Y)='and'(Y, X)).
-fof('Commutativity-or', axiom, ![X, Y]: 'or'(X, Y)='or'(Y, X)).
-fof('Absorption a', axiom, ![X, Y]: 'or'('and'(X, Y), X)=X).
-fof('Absorption b', axiom, ![X, Y]: 'and'('or'(X, Y), X)=X).
-fof('Residual a', axiom, ![X, Y, Z]: 'or'('*'(X, 'and'('\\'(X, Z), Y)), Z)=Z).
-fof('Residual b', axiom, ![X, Y, Z]: 'or'('*'('and'(Y, '/'(Z, X)), X), Z)=Z).
-fof('Residual c', axiom, ![X, Y, Z]: 'and'('\\'(X, 'or'('*'(X, Y), Z)), Y)=Y).
-fof('Residual d', axiom, ![X, Y, Z]: 'and'('/'('or'('*'(Y, X), Z), X), Y)=Y).
-fof('Associativity-* (fusion)', axiom, ![X, Y, Z]: '*'('*'(X, Y), Z)='*'(X, '*'(Y, Z))).
-fof('Left monoid unit', axiom, ![X]: '*'('1', X)=X).
-fof('Right monoid unit', axiom, ![X]: '*'(X, '1')=X).
-fof('GMV a', axiom, ![X, Y]: 'or'(X, Y)='/'(X, '\\'('or'(X, Y), X))).
-fof('GMV b', axiom, ![X, Y]: 'or'(X, Y)='\\'('/'(X, 'or'(X, Y)), X)).
-fof('Definition-@', axiom, ![X, Y]: '@'(X, Y)='*'('*'(X, '\\'(X, '1')), '\\'('\\'(Y, '1'), '1'))).
-fof('Goal 15', conjecture, '@'('or'(x, y), '\\'('/'(x, y), x))='\\'('/'(x, y), x)).
diff --git a/tests/gmv15.p b/tests/gmv15.p
deleted file mode 100644
--- a/tests/gmv15.p
+++ /dev/null
@@ -1,46 +0,0 @@
-cnf('Associativity-∧', axiom,
-    (X ∧ Y) ∧ Z = X ∧ (Y ∧ Z)).   
-cnf('Associativity-∨', axiom,
-    (X ∨ Y) ∨ Z = X ∨ (Y ∨ Z)).
-cnf('Idempotence-∧', axiom,
-    X ∧ X = X).
-cnf('Idempotence-∨', axiom,
-    X ∨ X = X).
-cnf('Commutativity-∧', axiom,
-    X ∧ Y = Y ∧ X).
-cnf('Commutativity-∨', axiom,
-    X ∨ Y = Y ∨ X).
-cnf('Absorption a', axiom,
-    (X ∧ Y) ∨ X = X).
-cnf('Absorption b', axiom,
-    (X ∨ Y) ∧ X = X).
-
-cnf('Residual a', axiom,
-    (X * ((X \ Z) ∧ Y)) ∨ Z = Z).
-cnf('Residual b', axiom,
-    ((Y ∧ (Z / X)) * X) ∨ Z = Z).
-cnf('Residual c', axiom,
-    (X \ ((X * Y) ∨ Z)) ∧ Y = Y).
-cnf('Residual d', axiom,
-    (((Y * X) ∨ Z) / X) ∧ Y = Y).
-
-cnf('Associativity-* (fusion)', axiom,
-    (X * Y) * Z = X * (Y * Z)).
-cnf('Left monoid unit', axiom,
-    '1' * X = X).
-cnf('Right monoid unit', axiom,
-    X * '1' = X).
-
-cnf('GMV a', axiom,
-    X ∨ Y = X / ((X ∨ Y) \ X)).
-cnf('GMV b', axiom,
-    X ∨ Y = (X / (X ∨ Y)) \ X).
-
-cnf('Definition-@', axiom,
-    X @ Y = (X * (X \ '1')) * ((Y \ '1') \ '1')).
-
-  
-  
-  
-cnf('Goal 15', conjecture,
-    (x ∨ y) @ ((x / y) \ x) = (x / y) \ x).
diff --git a/tests/gmv2-ascii.p b/tests/gmv2-ascii.p
deleted file mode 100644
--- a/tests/gmv2-ascii.p
+++ /dev/null
@@ -1,19 +0,0 @@
-fof('Associativity-and', axiom, ![X, Y, Z]: 'and'('and'(X, Y), Z)='and'(X, 'and'(Y, Z))).
-fof('Associativity-or', axiom, ![X, Y, Z]: 'or'('or'(X, Y), Z)='or'(X, 'or'(Y, Z))).
-fof('Idempotence-and', axiom, ![X]: 'and'(X, X)=X).
-fof('Idempotence-or', axiom, ![X]: 'or'(X, X)=X).
-fof('Commutativity-and', axiom, ![X, Y]: 'and'(X, Y)='and'(Y, X)).
-fof('Commutativity-or', axiom, ![X, Y]: 'or'(X, Y)='or'(Y, X)).
-fof('Absorption a', axiom, ![X, Y]: 'or'('and'(X, Y), X)=X).
-fof('Absorption b', axiom, ![X, Y]: 'and'('or'(X, Y), X)=X).
-fof('Residual a', axiom, ![X, Y, Z]: 'or'('*'(X, 'and'('\\'(X, Z), Y)), Z)=Z).
-fof('Residual b', axiom, ![X, Y, Z]: 'or'('*'('and'(Y, '/'(Z, X)), X), Z)=Z).
-fof('Residual c', axiom, ![X, Y, Z]: 'and'('\\'(X, 'or'('*'(X, Y), Z)), Y)=Y).
-fof('Residual d', axiom, ![X, Y, Z]: 'and'('/'('or'('*'(Y, X), Z), X), Y)=Y).
-fof('Associativity-* (fusion)', axiom, ![X, Y, Z]: '*'('*'(X, Y), Z)='*'(X, '*'(Y, Z))).
-fof('Left monoid unit', axiom, ![X]: '*'('1', X)=X).
-fof('Right monoid unit', axiom, ![X]: '*'(X, '1')=X).
-fof('GMV a', axiom, ![X, Y]: 'or'(X, Y)='/'(X, '\\'('or'(X, Y), X))).
-fof('GMV b', axiom, ![X, Y]: 'or'(X, Y)='\\'('/'(X, 'or'(X, Y)), X)).
-fof('Definition-@', axiom, ![X, Y]: '@'(X, Y)='*'('*'(X, '\\'(X, '1')), '\\'('\\'(Y, '1'), '1'))).
-fof('Goal 2', conjecture, '@'('@'(x, y), z)='@'(x, z)).
diff --git a/tests/gmv2.p b/tests/gmv2.p
deleted file mode 100644
--- a/tests/gmv2.p
+++ /dev/null
@@ -1,46 +0,0 @@
-cnf('Associativity-∧', axiom,
-    (X ∧ Y) ∧ Z = X ∧ (Y ∧ Z)).   
-cnf('Associativity-∨', axiom,
-    (X ∨ Y) ∨ Z = X ∨ (Y ∨ Z)).
-cnf('Idempotence-∧', axiom,
-    X ∧ X = X).
-cnf('Idempotence-∨', axiom,
-    X ∨ X = X).
-cnf('Commutativity-∧', axiom,
-    X ∧ Y = Y ∧ X).
-cnf('Commutativity-∨', axiom,
-    X ∨ Y = Y ∨ X).
-cnf('Absorption a', axiom,
-    (X ∧ Y) ∨ X = X).
-cnf('Absorption b', axiom,
-    (X ∨ Y) ∧ X = X).
-
-cnf('Residual a', axiom,
-    (X * ((X \ Z) ∧ Y)) ∨ Z = Z).
-cnf('Residual b', axiom,
-    ((Y ∧ (Z / X)) * X) ∨ Z = Z).
-cnf('Residual c', axiom,
-    (X \ ((X * Y) ∨ Z)) ∧ Y = Y).
-cnf('Residual d', axiom,
-    (((Y * X) ∨ Z) / X) ∧ Y = Y).
-
-cnf('Associativity-* (fusion)', axiom,
-    (X * Y) * Z = X * (Y * Z)).
-cnf('Left monoid unit', axiom,
-    '1' * X = X).
-cnf('Right monoid unit', axiom,
-    X * '1' = X).
-
-cnf('GMV a', axiom,
-    X ∨ Y = X / ((X ∨ Y) \ X)).
-cnf('GMV b', axiom,
-    X ∨ Y = (X / (X ∨ Y)) \ X).
-
-cnf('Definition-@', axiom,
-    X @ Y = (X * (X \ '1')) * ((Y \ '1') \ '1')).
-
-cnf('Goal 2', conjecture,
-    (x @ y) @ z = x @ z).
-  
-  
-  
diff --git a/tests/gmv3-ascii.p b/tests/gmv3-ascii.p
deleted file mode 100644
--- a/tests/gmv3-ascii.p
+++ /dev/null
@@ -1,19 +0,0 @@
-fof('Associativity-and', axiom, ![X, Y, Z]: 'and'('and'(X, Y), Z)='and'(X, 'and'(Y, Z))).
-fof('Associativity-or', axiom, ![X, Y, Z]: 'or'('or'(X, Y), Z)='or'(X, 'or'(Y, Z))).
-fof('Idempotence-and', axiom, ![X]: 'and'(X, X)=X).
-fof('Idempotence-or', axiom, ![X]: 'or'(X, X)=X).
-fof('Commutativity-and', axiom, ![X, Y]: 'and'(X, Y)='and'(Y, X)).
-fof('Commutativity-or', axiom, ![X, Y]: 'or'(X, Y)='or'(Y, X)).
-fof('Absorption a', axiom, ![X, Y]: 'or'('and'(X, Y), X)=X).
-fof('Absorption b', axiom, ![X, Y]: 'and'('or'(X, Y), X)=X).
-fof('Residual a', axiom, ![X, Y, Z]: 'or'('*'(X, 'and'('\\'(X, Z), Y)), Z)=Z).
-fof('Residual b', axiom, ![X, Y, Z]: 'or'('*'('and'(Y, '/'(Z, X)), X), Z)=Z).
-fof('Residual c', axiom, ![X, Y, Z]: 'and'('\\'(X, 'or'('*'(X, Y), Z)), Y)=Y).
-fof('Residual d', axiom, ![X, Y, Z]: 'and'('/'('or'('*'(Y, X), Z), X), Y)=Y).
-fof('Associativity-* (fusion)', axiom, ![X, Y, Z]: '*'('*'(X, Y), Z)='*'(X, '*'(Y, Z))).
-fof('Left monoid unit', axiom, ![X]: '*'('1', X)=X).
-fof('Right monoid unit', axiom, ![X]: '*'(X, '1')=X).
-fof('GMV a', axiom, ![X, Y]: 'or'(X, Y)='/'(X, '\\'('or'(X, Y), X))).
-fof('GMV b', axiom, ![X, Y]: 'or'(X, Y)='\\'('/'(X, 'or'(X, Y)), X)).
-fof('Definition-@', axiom, ![X, Y]: '@'(X, Y)='*'('*'(X, '\\'(X, '1')), '\\'('\\'(Y, '1'), '1'))).
-fof('Goal 3', conjecture, '@'(x, '@'(y, z))='@'(x, z)).
diff --git a/tests/gmv3.p b/tests/gmv3.p
deleted file mode 100644
--- a/tests/gmv3.p
+++ /dev/null
@@ -1,46 +0,0 @@
-cnf('Associativity-∧', axiom,
-    (X ∧ Y) ∧ Z = X ∧ (Y ∧ Z)).   
-cnf('Associativity-∨', axiom,
-    (X ∨ Y) ∨ Z = X ∨ (Y ∨ Z)).
-cnf('Idempotence-∧', axiom,
-    X ∧ X = X).
-cnf('Idempotence-∨', axiom,
-    X ∨ X = X).
-cnf('Commutativity-∧', axiom,
-    X ∧ Y = Y ∧ X).
-cnf('Commutativity-∨', axiom,
-    X ∨ Y = Y ∨ X).
-cnf('Absorption a', axiom,
-    (X ∧ Y) ∨ X = X).
-cnf('Absorption b', axiom,
-    (X ∨ Y) ∧ X = X).
-
-cnf('Residual a', axiom,
-    (X * ((X \ Z) ∧ Y)) ∨ Z = Z).
-cnf('Residual b', axiom,
-    ((Y ∧ (Z / X)) * X) ∨ Z = Z).
-cnf('Residual c', axiom,
-    (X \ ((X * Y) ∨ Z)) ∧ Y = Y).
-cnf('Residual d', axiom,
-    (((Y * X) ∨ Z) / X) ∧ Y = Y).
-
-cnf('Associativity-* (fusion)', axiom,
-    (X * Y) * Z = X * (Y * Z)).
-cnf('Left monoid unit', axiom,
-    '1' * X = X).
-cnf('Right monoid unit', axiom,
-    X * '1' = X).
-
-cnf('GMV a', axiom,
-    X ∨ Y = X / ((X ∨ Y) \ X)).
-cnf('GMV b', axiom,
-    X ∨ Y = (X / (X ∨ Y)) \ X).
-
-cnf('Definition-@', axiom,
-    X @ Y = (X * (X \ '1')) * ((Y \ '1') \ '1')).
-
-cnf('Goal 3', conjecture,
-    x @ (y @ z) = x @ z).
-  
-  
-  
diff --git a/tests/gmv4-ascii.p b/tests/gmv4-ascii.p
deleted file mode 100644
--- a/tests/gmv4-ascii.p
+++ /dev/null
@@ -1,19 +0,0 @@
-fof('Associativity-and', axiom, ![X, Y, Z]: 'and'('and'(X, Y), Z)='and'(X, 'and'(Y, Z))).
-fof('Associativity-or', axiom, ![X, Y, Z]: 'or'('or'(X, Y), Z)='or'(X, 'or'(Y, Z))).
-fof('Idempotence-and', axiom, ![X]: 'and'(X, X)=X).
-fof('Idempotence-or', axiom, ![X]: 'or'(X, X)=X).
-fof('Commutativity-and', axiom, ![X, Y]: 'and'(X, Y)='and'(Y, X)).
-fof('Commutativity-or', axiom, ![X, Y]: 'or'(X, Y)='or'(Y, X)).
-fof('Absorption a', axiom, ![X, Y]: 'or'('and'(X, Y), X)=X).
-fof('Absorption b', axiom, ![X, Y]: 'and'('or'(X, Y), X)=X).
-fof('Residual a', axiom, ![X, Y, Z]: 'or'('*'(X, 'and'('\\'(X, Z), Y)), Z)=Z).
-fof('Residual b', axiom, ![X, Y, Z]: 'or'('*'('and'(Y, '/'(Z, X)), X), Z)=Z).
-fof('Residual c', axiom, ![X, Y, Z]: 'and'('\\'(X, 'or'('*'(X, Y), Z)), Y)=Y).
-fof('Residual d', axiom, ![X, Y, Z]: 'and'('/'('or'('*'(Y, X), Z), X), Y)=Y).
-fof('Associativity-* (fusion)', axiom, ![X, Y, Z]: '*'('*'(X, Y), Z)='*'(X, '*'(Y, Z))).
-fof('Left monoid unit', axiom, ![X]: '*'('1', X)=X).
-fof('Right monoid unit', axiom, ![X]: '*'(X, '1')=X).
-fof('GMV a', axiom, ![X, Y]: 'or'(X, Y)='/'(X, '\\'('or'(X, Y), X))).
-fof('GMV b', axiom, ![X, Y]: 'or'(X, Y)='\\'('/'(X, 'or'(X, Y)), X)).
-fof('Definition-@', axiom, ![X, Y]: '@'(X, Y)='*'('*'(X, '\\'(X, '1')), '\\'('\\'(Y, '1'), '1'))).
-fof('Goal 4', conjecture, '@'('and'(x, y), 'and'(z, u))='and'('@'(x, z), '@'(y, u))).
diff --git a/tests/gmv4.p b/tests/gmv4.p
deleted file mode 100644
--- a/tests/gmv4.p
+++ /dev/null
@@ -1,46 +0,0 @@
-cnf('Associativity-∧', axiom,
-    (X ∧ Y) ∧ Z = X ∧ (Y ∧ Z)).   
-cnf('Associativity-∨', axiom,
-    (X ∨ Y) ∨ Z = X ∨ (Y ∨ Z)).
-cnf('Idempotence-∧', axiom,
-    X ∧ X = X).
-cnf('Idempotence-∨', axiom,
-    X ∨ X = X).
-cnf('Commutativity-∧', axiom,
-    X ∧ Y = Y ∧ X).
-cnf('Commutativity-∨', axiom,
-    X ∨ Y = Y ∨ X).
-cnf('Absorption a', axiom,
-    (X ∧ Y) ∨ X = X).
-cnf('Absorption b', axiom,
-    (X ∨ Y) ∧ X = X).
-
-cnf('Residual a', axiom,
-    (X * ((X \ Z) ∧ Y)) ∨ Z = Z).
-cnf('Residual b', axiom,
-    ((Y ∧ (Z / X)) * X) ∨ Z = Z).
-cnf('Residual c', axiom,
-    (X \ ((X * Y) ∨ Z)) ∧ Y = Y).
-cnf('Residual d', axiom,
-    (((Y * X) ∨ Z) / X) ∧ Y = Y).
-
-cnf('Associativity-* (fusion)', axiom,
-    (X * Y) * Z = X * (Y * Z)).
-cnf('Left monoid unit', axiom,
-    '1' * X = X).
-cnf('Right monoid unit', axiom,
-    X * '1' = X).
-
-cnf('GMV a', axiom,
-    X ∨ Y = X / ((X ∨ Y) \ X)).
-cnf('GMV b', axiom,
-    X ∨ Y = (X / (X ∨ Y)) \ X).
-
-cnf('Definition-@', axiom,
-    X @ Y = (X * (X \ '1')) * ((Y \ '1') \ '1')).
-
-  
-cnf('Goal 4', conjecture,
-    (x ∧ y) @ (z ∧ u) = (x @ z) ∧ (y @ u)).
-  
-  
diff --git a/tests/gmv5-ascii.p b/tests/gmv5-ascii.p
deleted file mode 100644
--- a/tests/gmv5-ascii.p
+++ /dev/null
@@ -1,19 +0,0 @@
-fof('Associativity-and', axiom, ![X, Y, Z]: 'and'('and'(X, Y), Z)='and'(X, 'and'(Y, Z))).
-fof('Associativity-or', axiom, ![X, Y, Z]: 'or'('or'(X, Y), Z)='or'(X, 'or'(Y, Z))).
-fof('Idempotence-and', axiom, ![X]: 'and'(X, X)=X).
-fof('Idempotence-or', axiom, ![X]: 'or'(X, X)=X).
-fof('Commutativity-and', axiom, ![X, Y]: 'and'(X, Y)='and'(Y, X)).
-fof('Commutativity-or', axiom, ![X, Y]: 'or'(X, Y)='or'(Y, X)).
-fof('Absorption a', axiom, ![X, Y]: 'or'('and'(X, Y), X)=X).
-fof('Absorption b', axiom, ![X, Y]: 'and'('or'(X, Y), X)=X).
-fof('Residual a', axiom, ![X, Y, Z]: 'or'('*'(X, 'and'('\\'(X, Z), Y)), Z)=Z).
-fof('Residual b', axiom, ![X, Y, Z]: 'or'('*'('and'(Y, '/'(Z, X)), X), Z)=Z).
-fof('Residual c', axiom, ![X, Y, Z]: 'and'('\\'(X, 'or'('*'(X, Y), Z)), Y)=Y).
-fof('Residual d', axiom, ![X, Y, Z]: 'and'('/'('or'('*'(Y, X), Z), X), Y)=Y).
-fof('Associativity-* (fusion)', axiom, ![X, Y, Z]: '*'('*'(X, Y), Z)='*'(X, '*'(Y, Z))).
-fof('Left monoid unit', axiom, ![X]: '*'('1', X)=X).
-fof('Right monoid unit', axiom, ![X]: '*'(X, '1')=X).
-fof('GMV a', axiom, ![X, Y]: 'or'(X, Y)='/'(X, '\\'('or'(X, Y), X))).
-fof('GMV b', axiom, ![X, Y]: 'or'(X, Y)='\\'('/'(X, 'or'(X, Y)), X)).
-fof('Definition-@', axiom, ![X, Y]: '@'(X, Y)='*'('*'(X, '\\'(X, '1')), '\\'('\\'(Y, '1'), '1'))).
-fof('Goal 5', conjecture, '@'('or'(x, y), 'or'(z, u))='or'('@'(x, z), '@'(y, u))).
diff --git a/tests/gmv5.p b/tests/gmv5.p
deleted file mode 100644
--- a/tests/gmv5.p
+++ /dev/null
@@ -1,46 +0,0 @@
-cnf('Associativity-∧', axiom,
-    (X ∧ Y) ∧ Z = X ∧ (Y ∧ Z)).   
-cnf('Associativity-∨', axiom,
-    (X ∨ Y) ∨ Z = X ∨ (Y ∨ Z)).
-cnf('Idempotence-∧', axiom,
-    X ∧ X = X).
-cnf('Idempotence-∨', axiom,
-    X ∨ X = X).
-cnf('Commutativity-∧', axiom,
-    X ∧ Y = Y ∧ X).
-cnf('Commutativity-∨', axiom,
-    X ∨ Y = Y ∨ X).
-cnf('Absorption a', axiom,
-    (X ∧ Y) ∨ X = X).
-cnf('Absorption b', axiom,
-    (X ∨ Y) ∧ X = X).
-
-cnf('Residual a', axiom,
-    (X * ((X \ Z) ∧ Y)) ∨ Z = Z).
-cnf('Residual b', axiom,
-    ((Y ∧ (Z / X)) * X) ∨ Z = Z).
-cnf('Residual c', axiom,
-    (X \ ((X * Y) ∨ Z)) ∧ Y = Y).
-cnf('Residual d', axiom,
-    (((Y * X) ∨ Z) / X) ∧ Y = Y).
-
-cnf('Associativity-* (fusion)', axiom,
-    (X * Y) * Z = X * (Y * Z)).
-cnf('Left monoid unit', axiom,
-    '1' * X = X).
-cnf('Right monoid unit', axiom,
-    X * '1' = X).
-
-cnf('GMV a', axiom,
-    X ∨ Y = X / ((X ∨ Y) \ X)).
-cnf('GMV b', axiom,
-    X ∨ Y = (X / (X ∨ Y)) \ X).
-
-cnf('Definition-@', axiom,
-    X @ Y = (X * (X \ '1')) * ((Y \ '1') \ '1')).
-
-  
-cnf('Goal 5', conjecture,
-    (x ∨ y) @ (z ∨ u) = (x @ z) ∨ (y @ u)).
-  
-  
diff --git a/tests/gmv6-ascii.p b/tests/gmv6-ascii.p
deleted file mode 100644
--- a/tests/gmv6-ascii.p
+++ /dev/null
@@ -1,19 +0,0 @@
-fof('Associativity-and', axiom, ![X, Y, Z]: 'and'('and'(X, Y), Z)='and'(X, 'and'(Y, Z))).
-fof('Associativity-or', axiom, ![X, Y, Z]: 'or'('or'(X, Y), Z)='or'(X, 'or'(Y, Z))).
-fof('Idempotence-and', axiom, ![X]: 'and'(X, X)=X).
-fof('Idempotence-or', axiom, ![X]: 'or'(X, X)=X).
-fof('Commutativity-and', axiom, ![X, Y]: 'and'(X, Y)='and'(Y, X)).
-fof('Commutativity-or', axiom, ![X, Y]: 'or'(X, Y)='or'(Y, X)).
-fof('Absorption a', axiom, ![X, Y]: 'or'('and'(X, Y), X)=X).
-fof('Absorption b', axiom, ![X, Y]: 'and'('or'(X, Y), X)=X).
-fof('Residual a', axiom, ![X, Y, Z]: 'or'('*'(X, 'and'('\\'(X, Z), Y)), Z)=Z).
-fof('Residual b', axiom, ![X, Y, Z]: 'or'('*'('and'(Y, '/'(Z, X)), X), Z)=Z).
-fof('Residual c', axiom, ![X, Y, Z]: 'and'('\\'(X, 'or'('*'(X, Y), Z)), Y)=Y).
-fof('Residual d', axiom, ![X, Y, Z]: 'and'('/'('or'('*'(Y, X), Z), X), Y)=Y).
-fof('Associativity-* (fusion)', axiom, ![X, Y, Z]: '*'('*'(X, Y), Z)='*'(X, '*'(Y, Z))).
-fof('Left monoid unit', axiom, ![X]: '*'('1', X)=X).
-fof('Right monoid unit', axiom, ![X]: '*'(X, '1')=X).
-fof('GMV a', axiom, ![X, Y]: 'or'(X, Y)='/'(X, '\\'('or'(X, Y), X))).
-fof('GMV b', axiom, ![X, Y]: 'or'(X, Y)='\\'('/'(X, 'or'(X, Y)), X)).
-fof('Definition-@', axiom, ![X, Y]: '@'(X, Y)='*'('*'(X, '\\'(X, '1')), '\\'('\\'(Y, '1'), '1'))).
-fof('Goal 6', conjecture, '@'('\\'(x, y), '\\'(z, u))='\\'('@'(x, z), '@'(y, u))).
diff --git a/tests/gmv6.p b/tests/gmv6.p
deleted file mode 100644
--- a/tests/gmv6.p
+++ /dev/null
@@ -1,46 +0,0 @@
-cnf('Associativity-∧', axiom,
-    (X ∧ Y) ∧ Z = X ∧ (Y ∧ Z)).   
-cnf('Associativity-∨', axiom,
-    (X ∨ Y) ∨ Z = X ∨ (Y ∨ Z)).
-cnf('Idempotence-∧', axiom,
-    X ∧ X = X).
-cnf('Idempotence-∨', axiom,
-    X ∨ X = X).
-cnf('Commutativity-∧', axiom,
-    X ∧ Y = Y ∧ X).
-cnf('Commutativity-∨', axiom,
-    X ∨ Y = Y ∨ X).
-cnf('Absorption a', axiom,
-    (X ∧ Y) ∨ X = X).
-cnf('Absorption b', axiom,
-    (X ∨ Y) ∧ X = X).
-
-cnf('Residual a', axiom,
-    (X * ((X \ Z) ∧ Y)) ∨ Z = Z).
-cnf('Residual b', axiom,
-    ((Y ∧ (Z / X)) * X) ∨ Z = Z).
-cnf('Residual c', axiom,
-    (X \ ((X * Y) ∨ Z)) ∧ Y = Y).
-cnf('Residual d', axiom,
-    (((Y * X) ∨ Z) / X) ∧ Y = Y).
-
-cnf('Associativity-* (fusion)', axiom,
-    (X * Y) * Z = X * (Y * Z)).
-cnf('Left monoid unit', axiom,
-    '1' * X = X).
-cnf('Right monoid unit', axiom,
-    X * '1' = X).
-
-cnf('GMV a', axiom,
-    X ∨ Y = X / ((X ∨ Y) \ X)).
-cnf('GMV b', axiom,
-    X ∨ Y = (X / (X ∨ Y)) \ X).
-
-cnf('Definition-@', axiom,
-    X @ Y = (X * (X \ '1')) * ((Y \ '1') \ '1')).
-
-  
-cnf('Goal 6', conjecture,
-    (x \ y) @ (z \ u) = (x @ z) \ (y @ u)).
-  
-  
diff --git a/tests/gmv7-ascii.p b/tests/gmv7-ascii.p
deleted file mode 100644
--- a/tests/gmv7-ascii.p
+++ /dev/null
@@ -1,19 +0,0 @@
-fof('Associativity-and', axiom, ![X, Y, Z]: 'and'('and'(X, Y), Z)='and'(X, 'and'(Y, Z))).
-fof('Associativity-or', axiom, ![X, Y, Z]: 'or'('or'(X, Y), Z)='or'(X, 'or'(Y, Z))).
-fof('Idempotence-and', axiom, ![X]: 'and'(X, X)=X).
-fof('Idempotence-or', axiom, ![X]: 'or'(X, X)=X).
-fof('Commutativity-and', axiom, ![X, Y]: 'and'(X, Y)='and'(Y, X)).
-fof('Commutativity-or', axiom, ![X, Y]: 'or'(X, Y)='or'(Y, X)).
-fof('Absorption a', axiom, ![X, Y]: 'or'('and'(X, Y), X)=X).
-fof('Absorption b', axiom, ![X, Y]: 'and'('or'(X, Y), X)=X).
-fof('Residual a', axiom, ![X, Y, Z]: 'or'('*'(X, 'and'('\\'(X, Z), Y)), Z)=Z).
-fof('Residual b', axiom, ![X, Y, Z]: 'or'('*'('and'(Y, '/'(Z, X)), X), Z)=Z).
-fof('Residual c', axiom, ![X, Y, Z]: 'and'('\\'(X, 'or'('*'(X, Y), Z)), Y)=Y).
-fof('Residual d', axiom, ![X, Y, Z]: 'and'('/'('or'('*'(Y, X), Z), X), Y)=Y).
-fof('Associativity-* (fusion)', axiom, ![X, Y, Z]: '*'('*'(X, Y), Z)='*'(X, '*'(Y, Z))).
-fof('Left monoid unit', axiom, ![X]: '*'('1', X)=X).
-fof('Right monoid unit', axiom, ![X]: '*'(X, '1')=X).
-fof('GMV a', axiom, ![X, Y]: 'or'(X, Y)='/'(X, '\\'('or'(X, Y), X))).
-fof('GMV b', axiom, ![X, Y]: 'or'(X, Y)='\\'('/'(X, 'or'(X, Y)), X)).
-fof('Definition-@', axiom, ![X, Y]: '@'(X, Y)='*'('*'(X, '\\'(X, '1')), '\\'('\\'(Y, '1'), '1'))).
-fof('Goal 7', conjecture, '@'('/'(x, y), '/'(z, u))='/'('@'(x, z), '@'(y, u))).
diff --git a/tests/gmv7.p b/tests/gmv7.p
deleted file mode 100644
--- a/tests/gmv7.p
+++ /dev/null
@@ -1,46 +0,0 @@
-cnf('Associativity-∧', axiom,
-    (X ∧ Y) ∧ Z = X ∧ (Y ∧ Z)).   
-cnf('Associativity-∨', axiom,
-    (X ∨ Y) ∨ Z = X ∨ (Y ∨ Z)).
-cnf('Idempotence-∧', axiom,
-    X ∧ X = X).
-cnf('Idempotence-∨', axiom,
-    X ∨ X = X).
-cnf('Commutativity-∧', axiom,
-    X ∧ Y = Y ∧ X).
-cnf('Commutativity-∨', axiom,
-    X ∨ Y = Y ∨ X).
-cnf('Absorption a', axiom,
-    (X ∧ Y) ∨ X = X).
-cnf('Absorption b', axiom,
-    (X ∨ Y) ∧ X = X).
-
-cnf('Residual a', axiom,
-    (X * ((X \ Z) ∧ Y)) ∨ Z = Z).
-cnf('Residual b', axiom,
-    ((Y ∧ (Z / X)) * X) ∨ Z = Z).
-cnf('Residual c', axiom,
-    (X \ ((X * Y) ∨ Z)) ∧ Y = Y).
-cnf('Residual d', axiom,
-    (((Y * X) ∨ Z) / X) ∧ Y = Y).
-
-cnf('Associativity-* (fusion)', axiom,
-    (X * Y) * Z = X * (Y * Z)).
-cnf('Left monoid unit', axiom,
-    '1' * X = X).
-cnf('Right monoid unit', axiom,
-    X * '1' = X).
-
-cnf('GMV a', axiom,
-    X ∨ Y = X / ((X ∨ Y) \ X)).
-cnf('GMV b', axiom,
-    X ∨ Y = (X / (X ∨ Y)) \ X).
-
-cnf('Definition-@', axiom,
-    X @ Y = (X * (X \ '1')) * ((Y \ '1') \ '1')).
-
-  
-cnf('Goal 7', conjecture,
-    (x / y) @ (z / u) = (x @ z) / (y @ u)).
-  
-  
diff --git a/tests/gmv8-ascii.p b/tests/gmv8-ascii.p
deleted file mode 100644
--- a/tests/gmv8-ascii.p
+++ /dev/null
@@ -1,19 +0,0 @@
-fof('Associativity-and', axiom, ![X, Y, Z]: 'and'('and'(X, Y), Z)='and'(X, 'and'(Y, Z))).
-fof('Associativity-or', axiom, ![X, Y, Z]: 'or'('or'(X, Y), Z)='or'(X, 'or'(Y, Z))).
-fof('Idempotence-and', axiom, ![X]: 'and'(X, X)=X).
-fof('Idempotence-or', axiom, ![X]: 'or'(X, X)=X).
-fof('Commutativity-and', axiom, ![X, Y]: 'and'(X, Y)='and'(Y, X)).
-fof('Commutativity-or', axiom, ![X, Y]: 'or'(X, Y)='or'(Y, X)).
-fof('Absorption a', axiom, ![X, Y]: 'or'('and'(X, Y), X)=X).
-fof('Absorption b', axiom, ![X, Y]: 'and'('or'(X, Y), X)=X).
-fof('Residual a', axiom, ![X, Y, Z]: 'or'('*'(X, 'and'('\\'(X, Z), Y)), Z)=Z).
-fof('Residual b', axiom, ![X, Y, Z]: 'or'('*'('and'(Y, '/'(Z, X)), X), Z)=Z).
-fof('Residual c', axiom, ![X, Y, Z]: 'and'('\\'(X, 'or'('*'(X, Y), Z)), Y)=Y).
-fof('Residual d', axiom, ![X, Y, Z]: 'and'('/'('or'('*'(Y, X), Z), X), Y)=Y).
-fof('Associativity-* (fusion)', axiom, ![X, Y, Z]: '*'('*'(X, Y), Z)='*'(X, '*'(Y, Z))).
-fof('Left monoid unit', axiom, ![X]: '*'('1', X)=X).
-fof('Right monoid unit', axiom, ![X]: '*'(X, '1')=X).
-fof('GMV a', axiom, ![X, Y]: 'or'(X, Y)='/'(X, '\\'('or'(X, Y), X))).
-fof('GMV b', axiom, ![X, Y]: 'or'(X, Y)='\\'('/'(X, 'or'(X, Y)), X)).
-fof('Definition-@', axiom, ![X, Y]: '@'(X, Y)='*'('*'(X, '\\'(X, '1')), '\\'('\\'(Y, '1'), '1'))).
-fof('Goal 8', conjecture, '@'('*'(x, '\\'(x, '1')), '1')='*'(x, '\\'(x, '1'))).
diff --git a/tests/gmv8.p b/tests/gmv8.p
deleted file mode 100644
--- a/tests/gmv8.p
+++ /dev/null
@@ -1,46 +0,0 @@
-cnf('Associativity-∧', axiom,
-    (X ∧ Y) ∧ Z = X ∧ (Y ∧ Z)).   
-cnf('Associativity-∨', axiom,
-    (X ∨ Y) ∨ Z = X ∨ (Y ∨ Z)).
-cnf('Idempotence-∧', axiom,
-    X ∧ X = X).
-cnf('Idempotence-∨', axiom,
-    X ∨ X = X).
-cnf('Commutativity-∧', axiom,
-    X ∧ Y = Y ∧ X).
-cnf('Commutativity-∨', axiom,
-    X ∨ Y = Y ∨ X).
-cnf('Absorption a', axiom,
-    (X ∧ Y) ∨ X = X).
-cnf('Absorption b', axiom,
-    (X ∨ Y) ∧ X = X).
-
-cnf('Residual a', axiom,
-    (X * ((X \ Z) ∧ Y)) ∨ Z = Z).
-cnf('Residual b', axiom,
-    ((Y ∧ (Z / X)) * X) ∨ Z = Z).
-cnf('Residual c', axiom,
-    (X \ ((X * Y) ∨ Z)) ∧ Y = Y).
-cnf('Residual d', axiom,
-    (((Y * X) ∨ Z) / X) ∧ Y = Y).
-
-cnf('Associativity-* (fusion)', axiom,
-    (X * Y) * Z = X * (Y * Z)).
-cnf('Left monoid unit', axiom,
-    '1' * X = X).
-cnf('Right monoid unit', axiom,
-    X * '1' = X).
-
-cnf('GMV a', axiom,
-    X ∨ Y = X / ((X ∨ Y) \ X)).
-cnf('GMV b', axiom,
-    X ∨ Y = (X / (X ∨ Y)) \ X).
-
-cnf('Definition-@', axiom,
-    X @ Y = (X * (X \ '1')) * ((Y \ '1') \ '1')).
-
-  
-  
-cnf('Goal 8', conjecture,
-    (x * (x \ '1')) @ '1' = x * (x \ '1')).
-  
diff --git a/tests/gmv9-ascii.p b/tests/gmv9-ascii.p
deleted file mode 100644
--- a/tests/gmv9-ascii.p
+++ /dev/null
@@ -1,19 +0,0 @@
-fof('Associativity-and', axiom, ![X, Y, Z]: 'and'('and'(X, Y), Z)='and'(X, 'and'(Y, Z))).
-fof('Associativity-or', axiom, ![X, Y, Z]: 'or'('or'(X, Y), Z)='or'(X, 'or'(Y, Z))).
-fof('Idempotence-and', axiom, ![X]: 'and'(X, X)=X).
-fof('Idempotence-or', axiom, ![X]: 'or'(X, X)=X).
-fof('Commutativity-and', axiom, ![X, Y]: 'and'(X, Y)='and'(Y, X)).
-fof('Commutativity-or', axiom, ![X, Y]: 'or'(X, Y)='or'(Y, X)).
-fof('Absorption a', axiom, ![X, Y]: 'or'('and'(X, Y), X)=X).
-fof('Absorption b', axiom, ![X, Y]: 'and'('or'(X, Y), X)=X).
-fof('Residual a', axiom, ![X, Y, Z]: 'or'('*'(X, 'and'('\\'(X, Z), Y)), Z)=Z).
-fof('Residual b', axiom, ![X, Y, Z]: 'or'('*'('and'(Y, '/'(Z, X)), X), Z)=Z).
-fof('Residual c', axiom, ![X, Y, Z]: 'and'('\\'(X, 'or'('*'(X, Y), Z)), Y)=Y).
-fof('Residual d', axiom, ![X, Y, Z]: 'and'('/'('or'('*'(Y, X), Z), X), Y)=Y).
-fof('Associativity-* (fusion)', axiom, ![X, Y, Z]: '*'('*'(X, Y), Z)='*'(X, '*'(Y, Z))).
-fof('Left monoid unit', axiom, ![X]: '*'('1', X)=X).
-fof('Right monoid unit', axiom, ![X]: '*'(X, '1')=X).
-fof('GMV a', axiom, ![X, Y]: 'or'(X, Y)='/'(X, '\\'('or'(X, Y), X))).
-fof('GMV b', axiom, ![X, Y]: 'or'(X, Y)='\\'('/'(X, 'or'(X, Y)), X)).
-fof('Definition-@', axiom, ![X, Y]: '@'(X, Y)='*'('*'(X, '\\'(X, '1')), '\\'('\\'(Y, '1'), '1'))).
-fof('Goal 9', conjecture, '@'('1', '*'(x, '\\'(x, '1')))='1').
diff --git a/tests/gmv9.p b/tests/gmv9.p
deleted file mode 100644
--- a/tests/gmv9.p
+++ /dev/null
@@ -1,46 +0,0 @@
-cnf('Associativity-∧', axiom,
-    (X ∧ Y) ∧ Z = X ∧ (Y ∧ Z)).   
-cnf('Associativity-∨', axiom,
-    (X ∨ Y) ∨ Z = X ∨ (Y ∨ Z)).
-cnf('Idempotence-∧', axiom,
-    X ∧ X = X).
-cnf('Idempotence-∨', axiom,
-    X ∨ X = X).
-cnf('Commutativity-∧', axiom,
-    X ∧ Y = Y ∧ X).
-cnf('Commutativity-∨', axiom,
-    X ∨ Y = Y ∨ X).
-cnf('Absorption a', axiom,
-    (X ∧ Y) ∨ X = X).
-cnf('Absorption b', axiom,
-    (X ∨ Y) ∧ X = X).
-
-cnf('Residual a', axiom,
-    (X * ((X \ Z) ∧ Y)) ∨ Z = Z).
-cnf('Residual b', axiom,
-    ((Y ∧ (Z / X)) * X) ∨ Z = Z).
-cnf('Residual c', axiom,
-    (X \ ((X * Y) ∨ Z)) ∧ Y = Y).
-cnf('Residual d', axiom,
-    (((Y * X) ∨ Z) / X) ∧ Y = Y).
-
-cnf('Associativity-* (fusion)', axiom,
-    (X * Y) * Z = X * (Y * Z)).
-cnf('Left monoid unit', axiom,
-    '1' * X = X).
-cnf('Right monoid unit', axiom,
-    X * '1' = X).
-
-cnf('GMV a', axiom,
-    X ∨ Y = X / ((X ∨ Y) \ X)).
-cnf('GMV b', axiom,
-    X ∨ Y = (X / (X ∨ Y)) \ X).
-
-cnf('Definition-@', axiom,
-    X @ Y = (X * (X \ '1')) * ((Y \ '1') \ '1')).
-
-  
-  
-cnf('Goal 9', conjecture,
-    '1' @ (x * (x \ '1')) = '1').
-  
diff --git a/tests/group_plain.p b/tests/group_plain.p
deleted file mode 100644
--- a/tests/group_plain.p
+++ /dev/null
@@ -1,14 +0,0 @@
-cnf(associativity, axiom,
-    plus(X,plus(Y,Z))=plus(plus(X,Y),Z)).
-cnf(plus_zero, axiom,
-    plus(zero, X) = X).
-cnf(plus_zero, axiom,
-    plus(X, zero) = X).
-cnf(minus_left, axiom,
-    plus(neg(X),X) = zero).
-cnf(minus_right, axiom,
-    plus(X,neg(X)) = zero).
-cnf(assumption, assumption,
-    plus(a, b) = a).
-cnf(goal, conjecture,
-    b = zero).
diff --git a/tests/loop-ascii.p b/tests/loop-ascii.p
deleted file mode 100644
--- a/tests/loop-ascii.p
+++ /dev/null
@@ -1,6 +0,0 @@
-cnf(mult_ld, axiom, mult(X, back(X, Y)) = Y).
-cnf(ld_mult, axiom, back(X, mult(X, Y)) = Y).
-cnf(mult_rd, axiom, mult(slash(X, Y), Y) = X).
-cnf(rd_mult, axiom, slash(mult(X, Y), Y) = X).
-cnf(moufang, axiom, mult(X, mult(Y, mult(X, Z))) = mult(mult(mult(X, Y), X), Z)).
-cnf(conjecture, conjecture, back(a, a) = slash(a, a)).
diff --git a/tests/rellat_appendixa.p b/tests/rellat_appendixa.p
new file mode 100644
--- /dev/null
+++ b/tests/rellat_appendixa.p
@@ -0,0 +1,27 @@
+% http://www.dcs.bbk.ac.uk/~szabolcs/rellat-jlamp-second-submission-2.pdf
+% appendix a. theorem 3.4, clause 7.
+cnf(commutativity, axiom,
+    X ∧ Y = Y ∧ X).
+cnf(associativity, axiom,
+    X ∧ (Y ∧ Z) = (X ∧ Y) ∧ Z).
+cnf(commutativity, axiom,
+    X ∨ Y = Y ∨ X).
+cnf(associativity, axiom,
+    X ∨ (Y ∨ Z) = (X ∨ Y) ∨ Z).
+cnf(absorption, axiom,
+    X ∨ (X ∧ Y) = X).
+cnf(absorption, axiom,
+    X ∧ (X ∨ Y) = X).
+cnf(definition_of_upme, axiom,
+    upme(X,Y,Z) = X ∧ (Y ∨ Z)).
+cnf(definition_of_lome, axiom,
+    lome(X,Y,Z) = (X ∧ Y) ∨ (X ∧ Z)).
+cnf(definition_of_upjo, axiom,
+    upjo(X,Y,Z) = (X ∨ Y) ∧ (X ∨ Z)).
+cnf(definition_of_lojo, axiom,
+    lojo(X,Y,Z) = X ∨ (Y ∧ Z)).
+
+fof(conjecture, conjecture,
+    (![X1, Y1, W]:
+    upme(a ∧ X1,Y1,W) ∨ (Y1 ∧ W) = (((a ∧ X1) ∧ Y1) ∨ W) ∧ (((a ∧ X1) ∧ W) ∨ Y1)) =>
+    upme(a ∧ z1,z2,z3) = lome(a ∧ z1,z2,z3)).
diff --git a/tests/rellat_appendixb.p b/tests/rellat_appendixb.p
new file mode 100644
--- /dev/null
+++ b/tests/rellat_appendixb.p
@@ -0,0 +1,28 @@
+% http://www.dcs.bbk.ac.uk/~szabolcs/rellat-jlamp-second-submission-2.pdf
+% appendix b. theorem 3.4, clause 8.
+cnf(commutativity, axiom,
+    X ∧ Y = Y ∧ X).
+cnf(associativity, axiom,
+    X ∧ (Y ∧ Z) = (X ∧ Y) ∧ Z).
+cnf(commutativity, axiom,
+    X ∨ Y = Y ∨ X).
+cnf(associativity, axiom,
+    X ∨ (Y ∨ Z) = (X ∨ Y) ∨ Z).
+cnf(absorption, axiom,
+    X ∨ (X ∧ Y) = X).
+cnf(absorption, axiom,
+    X ∧ (X ∨ Y) = X).
+cnf(definition_of_upme, axiom,
+    upme(X,Y,Z) = X ∧ (Y ∨ Z)).
+cnf(definition_of_lome, axiom,
+    lome(X,Y,Z) = (X ∧ Y) ∨ (X ∧ Z)).
+cnf(definition_of_upjo, axiom,
+    upjo(X,Y,Z) = (X ∨ Y) ∧ (X ∨ Z)).
+cnf(definition_of_lojo, axiom,
+    lojo(X,Y,Z) = X ∨ (Y ∧ Z)).
+cnf(rh1, axiom,
+    upme(a ∧ X1,Y1,Z1) ∨ (Y1 ∧ Z1) = (((a ∧ X1) ∧ Y1) ∨ Z1) ∧ (((a ∧ X1) ∧ Z1) ∨ Y1)).
+cnf(rh2, axiom,
+    upme(X,Y,Z) = upme(X,Y,a ∧ Z) ∨ upme(X,Z,a ∧ Y)).
+fof(conjecture, conjecture,
+    upme(a,x2,y2) = upme(a,x2,z2) => upme(x2,y2,z2) = lome(x2,y2,z2)).
diff --git a/tests/rellat_appendixb_easier.p b/tests/rellat_appendixb_easier.p
new file mode 100644
--- /dev/null
+++ b/tests/rellat_appendixb_easier.p
@@ -0,0 +1,30 @@
+% http://www.dcs.bbk.ac.uk/~szabolcs/rellat-jlamp-second-submission-2.pdf
+% appendix b. theorem 3.4, clause 8, assuming axiom rl1.
+cnf(commutativity, axiom,
+    X ∧ Y = Y ∧ X).
+cnf(associativity, axiom,
+    X ∧ (Y ∧ Z) = (X ∧ Y) ∧ Z).
+cnf(commutativity, axiom,
+    X ∨ Y = Y ∨ X).
+cnf(associativity, axiom,
+    X ∨ (Y ∨ Z) = (X ∨ Y) ∨ Z).
+cnf(absorption, axiom,
+    X ∨ (X ∧ Y) = X).
+cnf(absorption, axiom,
+    X ∧ (X ∨ Y) = X).
+cnf(definition_of_upme, axiom,
+    upme(X,Y,Z) = X ∧ (Y ∨ Z)).
+cnf(definition_of_lome, axiom,
+    lome(X,Y,Z) = (X ∧ Y) ∨ (X ∧ Z)).
+cnf(definition_of_upjo, axiom,
+    upjo(X,Y,Z) = (X ∨ Y) ∧ (X ∨ Z)).
+cnf(definition_of_lojo, axiom,
+    lojo(X,Y,Z) = X ∨ (Y ∧ Z)).
+cnf(rh1, axiom,
+    upme(a ∧ X1,Y1,Z1) ∨ (Y1 ∧ Z1) = (((a ∧ X1) ∧ Y1) ∨ Z1) ∧ (((a ∧ X1) ∧ Z1) ∨ Y1)).
+cnf(rh2, axiom,
+    upme(X,Y,Z) = upme(X,Y,a ∧ Z) ∨ upme(X,Z,a ∧ Y)).
+cnf(rl1, axiom,
+    lome(X,Y,Z) = upme(X,upme(Y,X,Z),upme(Z,X,Y))).
+fof(conjecture, conjecture,
+    upme(a,x2,y2) = upme(a,x2,z2) => upme(x2,y2,z2) = lome(x2,y2,z2)).
diff --git a/tests/rellat_appendixc.p b/tests/rellat_appendixc.p
new file mode 100644
--- /dev/null
+++ b/tests/rellat_appendixc.p
@@ -0,0 +1,30 @@
+% http://www.dcs.bbk.ac.uk/~szabolcs/rellat-jlamp-second-submission-2.pdf
+% appendix c. theorem 3.4, clause 9.
+cnf(commutativity, axiom,
+    X ∧ Y = Y ∧ X).
+cnf(associativity, axiom,
+    X ∧ (Y ∧ Z) = (X ∧ Y) ∧ Z).
+cnf(commutativity, axiom,
+    X ∨ Y = Y ∨ X).
+cnf(associativity, axiom,
+    X ∨ (Y ∨ Z) = (X ∨ Y) ∨ Z).
+cnf(absorption, axiom,
+    X ∨ (X ∧ Y) = X).
+cnf(absorption, axiom,
+    X ∧ (X ∨ Y) = X).
+cnf(definition_of_upme, axiom,
+    upme(X,Y,Z) = X ∧ (Y ∨ Z)).
+cnf(definition_of_lome, axiom,
+    lome(X,Y,Z) = (X ∧ Y) ∨ (X ∧ Z)).
+cnf(definition_of_upjo, axiom,
+    upjo(X,Y,Z) = (X ∨ Y) ∧ (X ∨ Z)).
+cnf(definition_of_lojo, axiom,
+    lojo(X,Y,Z) = X ∨ (Y ∧ Z)).
+cnf(upme_property_1, axiom,
+    upme(a ∧ X1,Y1,Z1) ∨ (Y1 ∧ Z1) = (((a ∧ X1) ∧ Y1) ∨ Z1) ∧ (((a ∧ X1) ∧ Z1) ∨ Y1)).
+cnf(upme_property_2, axiom,
+    upme(X,Y,Z) = upme(X,Y,a ∧ Z) ∨ upme(X,Z,a ∧ Y)).
+fof(conjecture, conjecture,
+    (upme(a,x2,y2) = upme(a,x2,z2) &
+     upme(a,x2,y2) = upme(a,y2,z2)) =>
+    upjo(x2,y2,z2) = lojo(x2,y2,z2)).
diff --git a/tests/rellat_theorem34_6.p b/tests/rellat_theorem34_6.p
new file mode 100644
--- /dev/null
+++ b/tests/rellat_theorem34_6.p
@@ -0,0 +1,32 @@
+% http://www.dcs.bbk.ac.uk/~szabolcs/rellat-jlamp-second-submission-2.pdf
+% theorem 3.4, clause 6.
+cnf(commutativity, axiom,
+    X ∧ Y = Y ∧ X).
+cnf(associativity, axiom,
+    X ∧ (Y ∧ Z) = (X ∧ Y) ∧ Z).
+cnf(commutativity, axiom,
+    X ∨ Y = Y ∨ X).
+cnf(associativity, axiom,
+    X ∨ (Y ∨ Z) = (X ∨ Y) ∨ Z).
+cnf(absorption, axiom,
+    X ∨ (X ∧ Y) = X).
+cnf(absorption, axiom,
+    X ∧ (X ∨ Y) = X).
+cnf(definition_of_upme, axiom,
+    upme(X,Y,Z) = X ∧ (Y ∨ Z)).
+cnf(definition_of_lome, axiom,
+    lome(X,Y,Z) = (X ∧ Y) ∨ (X ∧ Z)).
+cnf(definition_of_upjo, axiom,
+    upjo(X,Y,Z) = (X ∨ Y) ∧ (X ∨ Z)).
+cnf(definition_of_lojo, axiom,
+    lojo(X,Y,Z) = X ∨ (Y ∧ Z)).
+cnf(eq1, axiom,
+    upme(a ∧ Z1,Z2,Z3) = lome(a ∧ Z1,Z2,Z3)).
+cnf(qu2, axiom,
+    upme(a,X2,Y2) = upme(a,X2,Z2) => upme(X2,Y2,Z2) = lome(X2,Y2,Z2)).
+fof(rl1, conjecture,
+    lome(x,y,z) =
+    (x∧(y∧(x∨z)))∨(z∧(x∨y))).
+%fof(rl2, conjecture,
+%    t∧(((x∨y)∧(x∨z))∨((u∨w)∧(u∨v))) =
+%    (t∧(((x∨y)∧(x∨z))∨(u∨(w∧v))))∨(t∧(((u∨w)∧(u∨v))∨(x∨(y∧z))))).
diff --git a/tests/rellat_theorem34_6a.p b/tests/rellat_theorem34_6a.p
new file mode 100644
--- /dev/null
+++ b/tests/rellat_theorem34_6a.p
@@ -0,0 +1,29 @@
+% http://www.dcs.bbk.ac.uk/~szabolcs/rellat-jlamp-second-submission-2.pdf
+% theorem 3.4, clause 6.
+cnf(commutativity, axiom,
+    X ∧ Y = Y ∧ X).
+cnf(associativity, axiom,
+    X ∧ (Y ∧ Z) = (X ∧ Y) ∧ Z).
+cnf(commutativity, axiom,
+    X ∨ Y = Y ∨ X).
+cnf(associativity, axiom,
+    X ∨ (Y ∨ Z) = (X ∨ Y) ∨ Z).
+cnf(absorption, axiom,
+    X ∨ (X ∧ Y) = X).
+cnf(absorption, axiom,
+    X ∧ (X ∨ Y) = X).
+cnf(definition_of_upme, axiom,
+    upme(X,Y,Z) = X ∧ (Y ∨ Z)).
+cnf(definition_of_lome, axiom,
+    lome(X,Y,Z) = (X ∧ Y) ∨ (X ∧ Z)).
+cnf(definition_of_upjo, axiom,
+    upjo(X,Y,Z) = (X ∨ Y) ∧ (X ∨ Z)).
+cnf(definition_of_lojo, axiom,
+    lojo(X,Y,Z) = X ∨ (Y ∧ Z)).
+cnf(eq1, axiom,
+    upme(a ∧ Z1,Z2,Z3) = lome(a ∧ Z1,Z2,Z3)).
+cnf(qu2, axiom,
+    upme(a,X2,Y2) = upme(a,X2,Z2) => upme(X2,Y2,Z2) = lome(X2,Y2,Z2)).
+fof(rl1, conjecture,
+    lome(x,y,z) =
+    x∧((y∧(x∨z))∨(z∧(x∨y)))).
diff --git a/tests/rellat_theorem34_6b.p b/tests/rellat_theorem34_6b.p
new file mode 100644
--- /dev/null
+++ b/tests/rellat_theorem34_6b.p
@@ -0,0 +1,29 @@
+% http://www.dcs.bbk.ac.uk/~szabolcs/rellat-jlamp-second-submission-2.pdf
+% theorem 3.4, clause 6.
+cnf(commutativity, axiom,
+    X ∧ Y = Y ∧ X).
+cnf(associativity, axiom,
+    X ∧ (Y ∧ Z) = (X ∧ Y) ∧ Z).
+cnf(commutativity, axiom,
+    X ∨ Y = Y ∨ X).
+cnf(associativity, axiom,
+    X ∨ (Y ∨ Z) = (X ∨ Y) ∨ Z).
+cnf(absorption, axiom,
+    X ∨ (X ∧ Y) = X).
+cnf(absorption, axiom,
+    X ∧ (X ∨ Y) = X).
+cnf(definition_of_upme, axiom,
+    upme(X,Y,Z) = X ∧ (Y ∨ Z)).
+cnf(definition_of_lome, axiom,
+    lome(X,Y,Z) = (X ∧ Y) ∨ (X ∧ Z)).
+cnf(definition_of_upjo, axiom,
+    upjo(X,Y,Z) = (X ∨ Y) ∧ (X ∨ Z)).
+cnf(definition_of_lojo, axiom,
+    lojo(X,Y,Z) = X ∨ (Y ∧ Z)).
+cnf(eq1, axiom,
+    upme(a ∧ Z1,Z2,Z3) = lome(a ∧ Z1,Z2,Z3)).
+cnf(qu2, axiom,
+    upme(a,X2,Y2) = upme(a,X2,Z2) => upme(X2,Y2,Z2) = lome(X2,Y2,Z2)).
+fof(rl2, conjecture,
+    t∧(((x∨y)∧(x∨z))∨((u∨w)∧(u∨v))) =
+    (t∧(((x∨y)∧(x∨z))∨(u∨(w∧v))))∨(t∧(((u∨w)∧(u∨v))∨(x∨(y∧z))))).
diff --git a/tests/y-easy.p b/tests/y-easy.p
deleted file mode 100644
--- a/tests/y-easy.p
+++ /dev/null
@@ -1,3 +0,0 @@
-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(conjecture, conjecture, ![F]: ?[X]: F @ X = X).
diff --git a/tests/y-encoded.p b/tests/y-encoded.p
new file mode 100644
--- /dev/null
+++ b/tests/y-encoded.p
@@ -0,0 +1,5 @@
+cnf(ifeq_axiom, axiom, ifeq(A, A, B, C)=B).
+cnf(k_def, axiom, '@'('@'(k, X), Y)=X).
+cnf(s_def, axiom, '@'('@'('@'(s, X), Y), Z)='@'('@'(X, Z), '@'(Y, Z))).
+cnf(conjecture, negated_conjecture, ifeq('@'(Y, f(Y)), '@'(f(Y), '@'(Y, f(Y))), a, b)=b).
+cnf(goal, negated_conjecture, a!=b).
diff --git a/twee.cabal b/twee.cabal
--- a/twee.cabal
+++ b/twee.cabal
@@ -1,5 +1,5 @@
 name:                twee
-version:             2.3.1
+version:             2.4
 synopsis:            An equational theorem prover
 homepage:            http://github.com/nick8325/twee
 license:             BSD3
@@ -31,14 +31,17 @@
 flag static
   description: Build a static binary.
   default: False
+  manual: True
 
 flag static-cxx
   description: Build a binary which statically links against libstdc++.
   default: False
+  manual: True
 
-flag parallel
-  description: Build a special parallel version of Twee.
-  default: False
+--flag parallel
+--  description: Build a special parallel version of Twee.
+--  default: False
+--  manual: True
 
 executable twee
 --  if flag(parallel)
@@ -52,11 +55,11 @@
   other-modules:       SequentialMain
   default-language:    Haskell2010
   build-depends:       base < 5,
-                       twee-lib == 2.3.1,
+                       twee-lib == 2.4,
                        containers,
                        pretty,
                        split,
-                       jukebox == 0.5.*,
+                       jukebox >= 0.5.4,
                        ansi-terminal >= 0.9,
                        symbol
   ghc-options:         -W -fno-warn-incomplete-patterns