diff --git a/Twee.hs b/Twee.hs
--- a/Twee.hs
+++ b/Twee.hs
@@ -1,5 +1,5 @@
 -- | The main prover loop.
-{-# LANGUAGE RecordWildCards, MultiParamTypeClasses, GADTs, BangPatterns, OverloadedStrings, ScopedTypeVariables, GeneralizedNewtypeDeriving, PatternGuards, TypeFamilies, FlexibleInstances #-}
+{-# LANGUAGE RecordWildCards, MultiParamTypeClasses, GADTs, BangPatterns, OverloadedStrings, ScopedTypeVariables, GeneralizedNewtypeDeriving, PatternGuards, TypeFamilies, FlexibleInstances, RankNTypes, TupleSections #-}
 module Twee where
 
 import Twee.Base
@@ -39,6 +39,11 @@
 import Data.Ord
 import Data.PackedSequence(PackedSequence)
 import qualified Data.PackedSequence as PackedSequence
+import Test.QuickCheck.Gen hiding (sample)
+import Test.QuickCheck.Random
+import Debug.Trace
+import Twee.Generate
+import qualified System.Random as Random
 
 ----------------------------------------------------------------------
 -- * Configuration and prover state.
@@ -47,23 +52,31 @@
 -- | The prover configuration.
 data Config f =
   Config {
-    cfg_accept_term            :: Maybe (Term f -> Bool),
-    cfg_max_critical_pairs     :: Int64,
-    cfg_max_cp_depth           :: Int,
-    cfg_simplify               :: Bool,
-    cfg_renormalise_percent    :: Int,
-    cfg_cp_sample_size         :: Int,
-    cfg_renormalise_threshold  :: Int,
-    cfg_set_join_goals         :: Bool,
-    cfg_always_simplify        :: Bool,
-    cfg_complete_subsets       :: Bool,
-    cfg_critical_pairs         :: CP.Config,
-    cfg_join                   :: Join.Config,
-    cfg_proof_presentation     :: Proof.Config f }
+    cfg_accept_term               :: Maybe (Term f -> Bool),
+    cfg_max_critical_pairs        :: Int64,
+    cfg_max_cp_depth              :: Int,
+    cfg_max_rules                 :: Int,
+    cfg_simplify                  :: Bool,
+    cfg_renormalise_percent       :: Int,
+    cfg_cp_sample_size            :: Int,
+    cfg_renormalise_threshold     :: Int,
+    cfg_set_join_goals            :: Bool,
+    cfg_always_simplify           :: Bool,
+    cfg_complete_subsets          :: Bool,
+    cfg_score_cp                  :: Depth -> Equation f -> Float,
+    cfg_join                      :: Join.Config,
+    cfg_proof_presentation        :: Proof.Config f,
+    cfg_eliminate_axioms          :: [Axiom f],
+    cfg_random_mode               :: Bool,
+    cfg_random_mode_goal_directed :: Bool,
+    cfg_random_mode_simple        :: Bool,
+    cfg_random_mode_best_of       :: Int,
+    cfg_always_complete           :: Bool }
 
 -- | The prover state.
 data State f =
   State {
+    st_axioms         :: ![Axiom f],
     st_rules          :: !(RuleIndex f (Rule f)),
     st_active_set     :: !(IntMap (Active f)),
     st_joinable       :: !(Index f (Equation f)),
@@ -75,15 +88,18 @@
     st_cp_sample      :: !(Sample (Maybe (Overlap (Active f) f))),
     st_not_complete   :: !IntSet,
     st_complete       :: !(Index f (Rule f)),
-    st_messages_rev   :: ![Message f] }
+    st_messages_rev   :: ![Message f],
+    st_random_seed    :: Maybe QCGen,
+    st_problem_term   :: Maybe (ConfluenceFailure f) }
 
 -- | The default prover configuration.
-defaultConfig :: Config f
+defaultConfig :: Function f => Config f
 defaultConfig =
   Config {
     cfg_accept_term = Nothing,
     cfg_max_critical_pairs = maxBound,
     cfg_max_cp_depth = maxBound,
+    cfg_max_rules = maxBound,
     cfg_simplify = True,
     cfg_renormalise_percent = 5,
     cfg_renormalise_threshold = 20,
@@ -91,21 +107,29 @@
     cfg_set_join_goals = True,
     cfg_always_simplify = False,
     cfg_complete_subsets = False,
-    cfg_critical_pairs = CP.defaultConfig,
+    cfg_score_cp = \d eqn -> fromIntegral (score CP.defaultConfig d eqn),
     cfg_join = Join.defaultConfig,
-    cfg_proof_presentation = Proof.defaultConfig }
+    cfg_proof_presentation = Proof.defaultConfig,
+    cfg_eliminate_axioms = [],
+    cfg_random_mode = False,
+    cfg_random_mode_goal_directed = False,
+    cfg_random_mode_best_of = 1,
+    cfg_random_mode_simple = False,
+    cfg_always_complete = False }
 
 -- | Does this configuration run the prover in a complete mode?
 configIsComplete :: Config f -> Bool
 configIsComplete Config{..} =
   isNothing (cfg_accept_term) &&
   cfg_max_critical_pairs == maxBound &&
-  cfg_max_cp_depth == maxBound
+  cfg_max_cp_depth == maxBound &&
+  cfg_max_rules == maxBound
 
 -- | The initial state.
 initialState :: Config f -> State f
 initialState Config{..} =
   State {
+    st_axioms = [],
     st_rules = RuleIndex.empty,
     st_active_set = IntMap.empty,
     st_joinable = Index.empty,
@@ -117,7 +141,12 @@
     st_cp_sample = emptySample cfg_cp_sample_size,
     st_not_complete = IntSet.empty,
     st_complete = Index.empty,
-    st_messages_rev = [] }
+    st_messages_rev = [],
+    st_random_seed =
+      case cfg_random_mode of
+        False -> Nothing
+        True -> Just (mkQCGen 12345),
+    st_problem_term = Nothing }
 
 ----------------------------------------------------------------------
 -- * Messages.
@@ -139,9 +168,12 @@
   | Interreduce
     -- | Status update: how many queued critical pairs there are.
   | Status !Int
+    -- | New problem term discovered.
+  | NewProblemTerm !(ConfluenceFailure f)
 
 instance Function f => Pretty (Message f) where
   pPrint (NewActive rule) = pPrint rule
+ --   $$ case cp_top (active_cp rule) of { Just t -> text "  (normal forms of term" <+> pPrint t <#> text ")"; Nothing -> pPrintEmpty }
   pPrint (NewEquation eqn) =
     text "  (hard)" <+> pPrint eqn
   pPrint (DeleteActive rule) =
@@ -158,6 +190,17 @@
     text "  (simplifying rules with respect to one another...)"
   pPrint (Status n) =
     text "  (" <#> pPrint n <+> text "queued critical pairs)"
+  pPrint (NewProblemTerm cf) =
+    text "" $$
+    text "Problem term:" <+> pPrint (cf_term cf) $$
+    text "  NF 1:" $$ ppR (cf_term cf) (cf_left cf) $$
+    text "  NF 2:" $$ ppR (cf_term cf) (cf_right cf)
+    where
+      ppR _ [] = pPrintEmpty
+      ppR t (rr@(r,_,_):rs) =
+        text "    -> {by" <+> pPrint r <#> text "}" $$
+        text "       " <#> pPrint (ruleResult1 t rr) $$
+        ppR (ruleResult1 t rr) rs
 
 -- | Emit a message.
 message :: PrettyTerm f => Message f -> State f -> State f
@@ -180,6 +223,8 @@
 -- | Compute all critical pairs from a rule.
 {-# INLINEABLE makePassives #-}
 makePassives :: Function f => Config f -> State f -> Active f -> [Passive]
+-- don't generate critical pairs when in random mode
+makePassives Config{cfg_random_mode = True} _ _ = []
 makePassives config@Config{..} State{..} rule =
 -- XXX factor out depth calculation
   stampWith "make critical pair" length
@@ -192,7 +237,7 @@
 
 data Passive =
   Passive {
-    passive_score :: {-# UNPACK #-} !Int32,
+    passive_score :: {-# UNPACK #-} !Float,
     passive_rule1 :: {-# UNPACK #-} !Id,
     passive_rule2 :: {-# UNPACK #-} !Id,
     passive_how   :: !How }
@@ -212,7 +257,7 @@
     batch_kind      :: !BatchKind,
     batch_rule      :: {-# UNPACK #-} !Id,
     batch_best      :: {-# UNPACK #-} !Passive,
-    batch_rest      :: {-# UNPACK #-} !(PackedSequence (Int32, Id, How)) }
+    batch_rest      :: {-# UNPACK #-} !(PackedSequence (Float, Id, How)) }
 
 data BatchKind = Rule1 | Rule2 deriving Eq
 
@@ -252,9 +297,9 @@
 
 {-# INLINEABLE makePassive #-}
 makePassive :: Function f => Config f -> Overlap (Active f) f -> Passive
-makePassive Config{..} overlap@Overlap{..} =
+makePassive Config{..} Overlap{..} =
   Passive {
-    passive_score = fromIntegral (score cfg_critical_pairs depth overlap),
+    passive_score = cfg_score_cp depth overlap_eqn,
     passive_rule1 = active_id overlap_rule1,
     passive_rule2 = active_id overlap_rule2,
     passive_how   = overlap_how }
@@ -280,10 +325,10 @@
   let r1 = overlap_rule1 overlap
       r2 = overlap_rule2 overlap
   return passive {
-    passive_score = fromIntegral $
-      fromIntegral (passive_score passive) `intMin`
+    passive_score =
+      passive_score passive `min`
       -- XXX factor out depth calculation
-      score cfg_critical_pairs (succ (the r1 `max` the r2)) overlap }
+      cfg_score_cp (succ (the r1 `max` the r2)) (overlap_eqn overlap) }
 
 -- | Check if we should renormalise the queue.
 {-# INLINEABLE shouldSimplifyQueue #-}
@@ -489,8 +534,22 @@
         Nothing -> state'
 
     Left (cp, model) ->
+      generaliseCP cp $
       foldl' (\state cp -> addCP config model state info cp) state (split cp)
 
+  where
+    generaliseCP cp state
+      | null cfg_eliminate_axioms = state
+      | canonicalise (cp_eqn cp) == canonicalise (cp_eqn cp') = state
+      | otherwise =
+        consider config{cfg_eliminate_axioms = []} state info cp'
+      where
+        deriv =
+          let d1 = Proof.eliminateDefinitions cfg_eliminate_axioms (cp_proof cp)
+              [d2] = fixpointOn (map (equation . certify)) (Proof.generaliseProof False) [d1]
+          in d2
+        cp' = cp { cp_eqn = equation (certify deriv), cp_proof = deriv }
+
 {-# INLINEABLE addCP #-}
 addCP :: Function f => Config f -> Model f -> State f -> Info -> CriticalPair f -> State f
 addCP config model state@State{..} info CriticalPair{..} =
@@ -512,7 +571,7 @@
 {-# INLINEABLE addAxiom #-}
 addAxiom :: Function f => Config f -> State f -> Axiom f -> State f
 addAxiom config state axiom =
-  consider config state
+  consider config state{st_axioms = axiom:st_axioms state}
     Info { info_depth = 0, info_max = IntSet.fromList [axiom_number axiom | cfg_complete_subsets config] }
     CriticalPair {
       cp_eqn = axiom_eqn axiom,
@@ -764,14 +823,103 @@
 {-# INLINEABLE complete1 #-}
 complete1 :: Function f => Config f -> State f -> (Bool, State f)
 complete1 config@Config{..} state
+  | fromIntegral (st_next_active state) > cfg_max_rules =
+    (False, state)
   | st_considered state >= cfg_max_critical_pairs =
     (False, state)
-  | solved state = (False, state)
+  | solved state && not cfg_always_complete = (False, state)
   | otherwise =
-    case dequeue config state of
-      (Nothing, state) -> (False, state)
-      (Just (info, overlap, _, _), state) ->
-        (True, consider config state info overlap)
+    case st_random_seed state of
+      Nothing -> -- normal mode
+        case dequeue config state of
+          (Nothing, state) -> (False, state)
+          (Just (info, overlap, _, _), state) ->
+            (True, consider config state info overlap)
+      Just g -> -- random mode
+        let (g1, g2) = Random.split g in
+        let state' = state { st_random_seed = Just g2 } in
+        case findCriticalPair config state' g1 of
+          Nothing -> (True, state'{st_problem_term = Nothing})
+          Just (info, overlap, changed, cf) ->
+            let maybeMessage st =
+                  case st_problem_term st of
+                    Just cf | changed -> message (NewProblemTerm cf) st
+                    _ -> st
+                state'' = consider config (maybeMessage state'{st_problem_term = Just cf}) info overlap
+                progress = st_next_active state' /= st_next_active state'' in
+            (True, state''{st_problem_term = if progress then st_problem_term state'' else Nothing})
+
+{-# INLINEABLE findCriticalPair #-}
+findCriticalPair :: Function f => Config f -> State f -> QCGen -> Maybe (Info, CriticalPair f, Bool, ConfluenceFailure f)
+findCriticalPair config state g = retry `mplus` random
+  where
+    trace _ x = x
+    traceM _ = return ()
+    sizes = concat [replicate 10 i | i <- [10,20..100]]
+
+    retry = (hasUNFRetry strat <$> st_problem_term state) >>= toOverlap False >>= return . snd
+    random = pickBest randoms
+      where
+        pickBest =
+          listToMaybe . map snd . sortBy (comparing fst) . take (cfg_random_mode_best_of config) . catMaybes
+        randoms = unGen (sequence [resize n test | n <- sizes]) g 0
+
+    test = do
+      !(t, rs) <- gen
+      () <- traceM ("checking " ++ prettyShow t)
+      --toOverlap True <$> (hasUNF strat t rs <>) <$> hasUNFRandom strat t
+      return $ toOverlap True $ if cfg_random_mode_simple config then hasUNFSimple strat t rs else hasUNF strat t rs
+
+    gen =
+      if cfg_random_mode_goal_directed config then
+        generateGoalTerm (goalTerms state) (Index.elems (index_all (st_rules state)))
+      else do
+        t <- generateTerm lhss
+        r <- normaliseWith1Random (const True) strat t
+        return (t, r)
+
+    strat = basic (rewrite reducesSkolem (index_all (st_rules state)))
+    lhss = map lhs (Index.elems (index_all (st_rules state)))
+
+    toOverlap _ UniqueNormalForm{} = Nothing
+    toOverlap changed (HasCriticalPair r1 (r2, n) cf) =
+    {-
+      Debug.Trace.trace
+        (prettyShow $
+          text "" $$
+          text "Problem term before shrinking:" <+> pPrint (cf_orig_term cf) $$
+          text "  NF 1:" <+> pPrint (cf_orig_left_term cf) $$
+          text "  NF 2:" <+> pPrint (cf_orig_right_term cf)) $
+      -}
+      trace ("Term " ++ prettyShow (cf_term cf) ++ " has critical pair (" ++ prettyShow r1 ++ ", " ++ prettyShow r2 ++ ", " ++ show n ++ ")") $
+      let r2' = renameAvoiding r1 r2 in
+      let Just o = overlapAt (How n Forwards Forwards) r1 r2' r1 r2' in
+      case simplifyOverlap (index_all (st_rules state)) o of
+        Nothing ->
+          trace ("Overlap " ++ prettyShow (overlap_eqn o) ++ " was spurious") Nothing -- should be rare
+        Just o' ->
+          Just (cfg_score_cp config 0 (overlap_eqn o'), (Info 0 IntSet.empty, makeCriticalPair o, changed, cf))
+
+-- Return all goal terms. Handles the $equals coding.
+goalTerms :: Function f => State f -> [Term f]
+goalTerms state =
+  -- Goals that are not related to $equals.
+  [ t
+  | eqn <- map goal_eqn (st_goals state),
+    t <- concatMap unpack (terms eqn), 
+    True ]
+{-
+    not (isTrueTerm t), not (isFalseTerm t)] ++
+  -- Axioms of the form $equals(t, u) = $false.
+  [ goalTerm
+  | t :=: u <- map axiom_eqn (st_axioms state),
+    (lhs, rhs) <- maybeToList $
+      if isFalseTerm t then decodeEquality u 
+      else if isFalseTerm u then decodeEquality t
+      else Nothing,
+    goalTerm <- [t, u] ]
+-}
+
 
 {-# INLINEABLE solved #-}
 solved :: Function f => State f -> Bool
diff --git a/Twee/Base.hs b/Twee/Base.hs
--- a/Twee/Base.hs
+++ b/Twee/Base.hs
@@ -1,19 +1,21 @@
 -- | Useful operations on terms and similar. Also re-exports some generally
 -- useful modules such as 'Twee.Term' and 'Twee.Pretty'.
 
-{-# LANGUAGE TypeFamilies, FlexibleInstances, UndecidableInstances, DeriveFunctor, DefaultSignatures, FlexibleContexts, TypeOperators, MultiParamTypeClasses, GeneralizedNewtypeDeriving, ConstraintKinds, RecordWildCards #-}
+{-# LANGUAGE TypeFamilies, FlexibleInstances, UndecidableInstances, DeriveFunctor, DefaultSignatures, FlexibleContexts, TypeOperators, MultiParamTypeClasses, GeneralizedNewtypeDeriving, ConstraintKinds, RecordWildCards, BangPatterns #-}
 module Twee.Base(
   -- * Re-exported functionality
   module Twee.Term, module Twee.Pretty,
   -- * The 'Symbolic' typeclass
   Symbolic(..), subst, terms,
   TermOf, TermListOf, SubstOf, TriangleSubstOf, BuilderOf, FunOf,
-  vars, isGround, funs, occ, occVar, canonicalise, renameAvoiding, renameManyAvoiding, freshVar,
+  vars, isGround, funs, occ, occVar, occs, nests, canonicalise, renameAvoiding, renameManyAvoiding, freshVar,
   -- * General-purpose functionality
   Id(..), Has(..),
   -- * Typeclasses
   Minimal(..), minimalTerm, isMinimal, erase, eraseExcept, ground,
-  Ordered(..), lessThan, orientTerms, EqualsBonus(..), Strictness(..), Function) where
+  Ordered(..), lessThan, orientTerms,
+  EqualsBonus(..), isTrueTerm, isFalseTerm, decodeEquality,
+  Strictness(..), Function) where
 
 import Prelude hiding (lookup)
 import Control.Monad
@@ -147,6 +149,29 @@
 occVar :: Symbolic a => Var -> a -> Int
 occVar x t = length (filter (== x) (vars t))
 
+-- | Count how many times all function symbols occur in the argument.
+{-# INLINE occs #-}
+occs :: Symbolic a => a -> IntMap.IntMap Int
+occs = foldl' insert IntMap.empty . funs
+  where
+    insert !m !f = IntMap.insertWith (+) (fun_id f) 1 m
+
+-- | 'nest' from Fuchs, "The application of goal-oriented heuristics
+-- for proving equational theorems via the unfailing Knuth-Bendix
+-- completion procedure"
+{-# INLINE nests #-}
+nests :: Symbolic a => a -> IntMap.IntMap Int
+nests t = foldl' (hnest 0 0) IntMap.empty (terms t)
+
+-- helper function for nests
+hnest :: Int -> Int -> IntMap.IntMap Int -> TermList f -> IntMap.IntMap Int
+hnest !f !c !as Empty = IntMap.insertWith max f c as
+hnest f c as (Cons (Var _) ts) = hnest f c as ts
+hnest f c as (Cons (App _ Empty) ts) = hnest f c as ts
+hnest f c as (Cons (App g ts) us) =
+  let as' = hnest (fun_id g) (if f == fun_id g then c+1 else 1) as ts
+  in hnest f c as' us
+
 -- | Rename the argument so that variables are introduced in a canonical order
 -- (starting with V0, then V1 and so on).
 {-# INLINEABLE canonicalise #-}
@@ -228,6 +253,18 @@
   isEquals _ = False
   isTrue _ = False
   isFalse _ = False
+
+isFalseTerm, isTrueTerm :: (EqualsBonus f, Labelled f) => Term f -> Bool
+isFalseTerm (App false _) = isFalse false
+isFalseTerm _ = False
+isTrueTerm (App true _) = isTrue true
+isTrueTerm _ = False
+
+-- Decode $equals(t,u) into an equation t=u.
+decodeEquality :: (EqualsBonus f, Labelled f) => Term f -> Maybe (Term f, Term f)
+decodeEquality (App equals (Cons t (Cons u Empty)))
+  | isEquals equals = Just (t, u)
+decodeEquality _ = Nothing
 
 instance (Labelled f, EqualsBonus f) => EqualsBonus (Fun f) where
   hasEqualsBonus = hasEqualsBonus . fun_value
diff --git a/Twee/CP.hs b/Twee/CP.hs
--- a/Twee/CP.hs
+++ b/Twee/CP.hs
@@ -158,7 +158,7 @@
 {-# INLINE overlapAt' #-}
 overlapAt' :: How -> a -> a -> Equation f -> Equation f -> Maybe (Overlap a f)
 overlapAt' how@How{how_pos = n} r1 r2 (!outer :=: (!outer')) (!inner :=: (!inner')) = do
-  let t = at n (singleton outer)
+  let t = outer `at` n
   sub <- unifyTri inner t
   let
     -- Make sure to keep in sync with overlapProof
@@ -223,13 +223,12 @@
 -- where l is the biggest term and r is the smallest,
 -- and variables have weight 1 and functions have weight cfg_funweight.
 {-# INLINEABLE score #-}
-score :: Function f => Config -> Depth -> Overlap a f -> Int
-score Config{..} depth Overlap{..} =
+score :: Function f => Config -> Depth -> Equation f -> Int
+score Config{..} depth (l :=: r) =
   fromIntegral depth * cfg_depthweight +
   (m + n) * cfg_rhsweight +
   intMax m n * (cfg_lhsweight - cfg_rhsweight)
   where
-    l :=: r = overlap_eqn
     m = size' 0 (singleton l)
     n = size' 0 (singleton r)
 
@@ -360,7 +359,7 @@
     Just rightSub = match (lhs right) inner
 
     path = positionToPath (lhs left) (how_pos overlap_how)
-    inner = at (pathToPosition overlap_top path) (singleton overlap_top)
+    inner = overlap_top `atPath` path
 
     proof =
       Proof.symm (ruleDerivation (subst leftSub left))
diff --git a/Twee/Generate.hs b/Twee/Generate.hs
new file mode 100644
--- /dev/null
+++ b/Twee/Generate.hs
@@ -0,0 +1,121 @@
+{-# LANGUAGE OverloadedStrings #-}
+module Twee.Generate(generateTerm, generateGoalTerm, permuteVars) where
+
+import Test.QuickCheck hiding (Function)
+import Twee.Base
+import Twee.Rule
+import Data.Maybe
+import Twee.Profile
+import Twee.Utils
+import Debug.Trace
+
+type Pat f = Term f
+type LHS f = Term f
+
+-- the generator
+
+generateTerm :: Function f => [LHS f] -> Gen (Term f)
+generateTerm lhss = generateTerm' lhss (build (var (V 0)))
+
+generateTerm' :: Function f => [LHS f] -> Pat f -> Gen (Term f)
+generateTerm' lhss pat =
+  stampGen "generateTerm'" $ do
+  sized $ \n -> do
+    sub <- gen n lhss pat emptyTriangleSubst
+    permuteVars (subst sub pat)
+
+gen :: Function f => Int -> [LHS f] -> Pat f -> TriangleSubst f -> Gen (TriangleSubst f)
+gen n lhss p sub =
+  -- TODO: play around with frequencies
+  frequency $
+  [ (1, return sub) ] ++
+  -- commit to top-level function...
+  [ (n, genList (reduce n (length ps)) lhss ps sub)
+  | App f psl <- [p]
+  , let ps = unpack psl
+  ] ++
+  -- ...or use a LHS for inspiration
+  [ (n, gen n lhss p' sub')
+  | n > 0
+  , lhs <- map (renameAvoiding p) lhss
+  , Just sub' <- [unifyTriFrom lhs p sub]
+  , let p' = subst sub' p
+  , n >= (len p' - len p)
+  , not (isVariantOf p' p) -- make progress
+  ]
+  where
+    reduce n m
+      | m <= 1 = n-1
+      | otherwise = n `div` m
+
+-- just a helper function
+genList :: Function f => Int -> [LHS f] -> [Pat f] -> TriangleSubst f -> Gen (TriangleSubst f)
+genList _n _lhss [] sub =
+  do return sub
+
+genList n lhss (p:ps) sub =
+  do sub' <- gen n lhss (subst sub p) sub
+     sub'' <- genList n lhss ps sub'
+     return sub''
+
+-- Generate a term by starting with a goal term and rewriting
+-- backwawrds a certain number of times.
+generateGoalTerm :: Function f => [Term f] -> [Rule f] -> Gen (Term f, Reduction1 f)
+generateGoalTerm goals rules = stampGen "generateGoalTerm" $ sized $ \n -> do
+  t <- frequency [(len u, return u) | u <- goals]
+  -- () <- traceM ("Goal term: " ++ prettyShow t)
+  let ok u = len u <= n
+  (u, r) <- loop (n `div` 5 + 1) (rewriteBackwardsWithReduction ok rules) (t, [])
+  -- () <- traceM ("intermediate generated " ++ prettyShow u)
+  -- fill in any holes with randomly-generated terms
+  v <- generateTerm' (map lhs rules) u
+  -- () <- traceM ("generated " ++ prettyShow v)
+  -- () <- traceM ("proof " ++ prettyShow r)
+  return (v, rematchReduction1 v r)
+
+loop :: Monad m => Int -> (a -> m a) -> a -> m a
+loop 0 _ x = return x
+loop n f x | n > 0 = f x >>= loop (n-1) f
+
+-- Apply a rule backwards at a given position in a term.
+-- The goal rhs and the subterm must be unifiable.
+tryBackwardsRewrite :: Rule f -> Term f -> Int -> Maybe (Term f, Reduction1 f)
+tryBackwardsRewrite rule t n = do
+  sub <- unify (rhs rule) (t `at` n)
+  return $
+    (build (replacePositionSub sub n (singleton (lhs rule)) (singleton t)),
+     [(rule, sub, positionToPath t n)])
+
+rewriteBackwardsWithReduction :: Function f => (Term f -> Bool) -> [Rule f] -> (Term f, Reduction1 f) -> Gen (Term f, Reduction1 f)
+rewriteBackwardsWithReduction ok rules (t, r) = do
+  res <- rewriteBackwards ok rules t
+  case res of
+    Nothing -> return (t, r)
+    Just (u, r') -> return (u, r' `trans1` r)
+
+-- Pick a random rule and rewrite the term backwards using it.
+rewriteBackwards :: Function f => (Term f -> Bool) -> [Rule f] -> Term f -> Gen (Maybe (Term f, Reduction1 f))
+rewriteBackwards ok rules t0
+  | not (ok t0) = return Nothing
+  | otherwise = 
+    frequency $
+      [(1, return Nothing)] ++ -- in case no rules work
+      [ -- penalise unification with a variable as it can result in "type-incorrect" terms
+        (if isVar (t `at` n) then 1 else 10*(overlap (t `at` n) (rhs rule)+1)*(if n == 0 then 2 else 1),
+         return (Just (u, r)))
+      | n <- [0..len t-1],
+        rule <- rules,
+        (u, r) <- maybeToList (tryBackwardsRewrite rule t n),
+        ok u ]
+  where
+    t = renameAvoiding rules t0
+    overlap (App f ts) (App g us) | f == g =
+      1 + sum (zipWith overlap (unpack ts) (unpack us))
+    overlap _ _ = 0
+
+permuteVars :: Term f -> Gen (Term f)
+permuteVars t = do
+  let vs = usort (vars t)
+  ws <- shuffle vs
+  let Just sub = listToSubst [(v, build (var w)) | (v, w) <- zip vs ws]
+  return (subst sub t)
diff --git a/Twee/Join.hs b/Twee/Join.hs
--- a/Twee/Join.hs
+++ b/Twee/Join.hs
@@ -237,8 +237,8 @@
 {-# INLINEABLE valid #-}
 valid :: Function f => Model f -> Reduction f -> Bool
 valid model red =
-  and [ reducesInModel model rule emptySubst
-      | rule <- red ]
+  and [ reducesInModel model (subst sub rule) emptySubst
+      | (rule, sub) <- red ]
 
 optimise :: (a -> [a]) -> (a -> Bool) -> a -> a
 optimise f p x =
diff --git a/Twee/Profile.hs b/Twee/Profile.hs
--- a/Twee/Profile.hs
+++ b/Twee/Profile.hs
@@ -1,6 +1,6 @@
 -- Basic support for profiling.
 {-# LANGUAGE BangPatterns, RecordWildCards, CPP, OverloadedStrings #-}
-module Twee.Profile(stamp, stampWith, stampM, profile) where
+module Twee.Profile(stamp, stampWith, stampM, stampGen, stampGen', profile) where
 
 #ifdef PROFILE
 import System.IO.Unsafe
@@ -17,6 +17,7 @@
 import Data.Symbol
 import Data.Symbol.Unsafe
 import Data.Hashable
+import Test.QuickCheck.Gen
 
 instance Hashable Symbol where
   hashWithSalt s (Symbol n _) = hashWithSalt s n
@@ -97,6 +98,12 @@
   liftIO (exit m str)
   return x
 
+stampGen :: Symbol -> Gen a -> Gen a
+stampGen sym gen = MkGen (\g n -> stamp sym (unGen gen g n))
+
+stampGen' :: (a -> Symbol) -> Gen a -> Gen a
+stampGen' sym gen = MkGen (\g n -> let x = unGen gen g n in stamp (sym x) x)
+
 report :: (Record -> Word64) -> HashMap Symbol Record -> IO ()
 report f cs = mapM_ pr ts
   where
@@ -126,6 +133,7 @@
   report rec_cumulative log
 #else
 import Control.Monad.IO.Class
+import Test.QuickCheck
 
 stamp :: symbol -> a -> a
 stamp _ = id
@@ -135,6 +143,12 @@
 
 stampM :: MonadIO m => symbol -> m a -> m a
 stampM _ = id
+
+stampGen :: symbol -> Gen a -> Gen a
+stampGen _ = id
+
+stampGen' :: (a -> symbol) -> Gen a -> Gen a
+stampGen' _ = id
 
 profile :: IO ()
 profile = return ()
diff --git a/Twee/Proof.hs b/Twee/Proof.hs
--- a/Twee/Proof.hs
+++ b/Twee/Proof.hs
@@ -10,6 +10,7 @@
   -- * Analysing proofs
   simplify, steps, usedLemmas, usedAxioms, usedLemmasAndSubsts, usedAxiomsAndSubsts,
   groundAxiomsAndSubsts, eliminateDefinitions, eliminateDefinitionsFromGoal,
+  simplifyProof, generaliseProof,
 
   -- * Pretty-printing proofs
   Config(..), defaultConfig, Presentation(..),
@@ -556,7 +557,7 @@
       inlineTrivialLemmas config .
       tightenProof
 
-    simp = simpCore . generaliseProof
+    simp = simpCore . generaliseProof True
     -- generaliseProof undoes the effect of groundProof!
     -- But we still want to run generaliseProof first, to simplify the proof
     simp' = (simpCore . groundProof) `onlyIf` cfg_ground_proof
@@ -666,14 +667,14 @@
             sub <- maybeToList (match u t),
             subst sub (eqn_rhs eq) == eqn_rhs eq ]
 
-generaliseProof :: Function f => [Derivation f] -> [Derivation f]
-generaliseProof =
+generaliseProof :: Function f => Bool -> [Derivation f] -> [Derivation f]
+generaliseProof instGoal =
   simplificationPass (const generaliseLemma) (const generaliseGoal)
   where
     generaliseLemma p = lemma (certify q) sub
       where
         (q, sub) = generalise p
-    generaliseGoal p = subst sub q
+    generaliseGoal p = if instGoal then subst sub q else q
       where
         (q, sub) = generalise (certify p)
 
@@ -892,12 +893,6 @@
 --   * a proof that both sides of the conjecture are equal
 -- and we can present that to the user.
 
--- Decode $equals(t,u) into an equation t=u.
-decodeEquality :: Function f => Term f -> Maybe (Equation f)
-decodeEquality (App equals (Cons t (Cons u Empty)))
-  | isEquals equals = Just (t :=: u)
-decodeEquality _ = Nothing
-
 -- Tries to transform a proof of $true = $false into a proof of
 -- the original existentially-quantified formula.
 decodeGoal :: Function f => ProvedGoal f -> ProvedGoal f
@@ -922,12 +917,6 @@
   | isFalseTerm t = extract (steps (symm deriv))
   | otherwise = Nothing
   where
-    isFalseTerm, isTrueTerm :: Term f -> Bool
-    isFalseTerm (App false _) = isFalse false
-    isFalseTerm _ = False
-    isTrueTerm (App true _) = isTrue true
-    isTrueTerm _ = False
-
     t :=: u = equation pg_proof
     deriv = derivation pg_proof
 
@@ -935,7 +924,7 @@
     decodeReflexivity :: Derivation f -> Maybe (Term f)
     decodeReflexivity (Symm (UseAxiom Axiom{..} sub)) = do
       guard (isTrueTerm (eqn_rhs axiom_eqn))
-      (t :=: u) <- decodeEquality (eqn_lhs axiom_eqn)
+      (t, u) <- decodeEquality (eqn_lhs axiom_eqn)
       guard (t == u)
       return (subst sub t)
     decodeReflexivity _ = Nothing
@@ -944,8 +933,8 @@
     decodeConjecture :: Derivation f -> Maybe (String, Equation f, Subst f)
     decodeConjecture (UseAxiom Axiom{..} sub) = do
       guard (isFalseTerm (eqn_rhs axiom_eqn))
-      eqn <- decodeEquality (eqn_lhs axiom_eqn)
-      return (axiom_name, eqn, sub)
+      (t, u) <- decodeEquality (eqn_lhs axiom_eqn)
+      return (axiom_name, t :=: u, sub)
     decodeConjecture _ = Nothing
 
     extract (p:ps) = do
diff --git a/Twee/Rule.hs b/Twee/Rule.hs
--- a/Twee/Rule.hs
+++ b/Twee/Rule.hs
@@ -20,6 +20,19 @@
 import qualified Twee.Proof as Proof
 import Twee.Proof(Derivation, Proof)
 import Data.Tuple
+import Twee.Profile
+import Data.MemoUgly
+import Debug.Trace
+import Twee.Pretty
+import Data.Function
+import Control.Arrow((***))
+import GHC.Stack
+import Test.QuickCheck hiding (Function, subterms, Fun)
+import Twee.Profile
+import Test.QuickCheck.Gen
+import Data.Semigroup
+import qualified Data.List.NonEmpty as NonEmpty
+import Test.QuickCheck.Random
 
 --------------------------------------------------------------------------------
 -- * Rewrite rules.
@@ -189,13 +202,13 @@
 -- | Compute the normal form of a term wrt only oriented rules.
 {-# INLINEABLE simplify #-}
 simplify :: (Function f, Has a (Rule f)) => Index f a -> Term f -> Term f
-simplify = simplifyOutermost
+simplify idx t = stamp "simplify" (simplifyOutermost idx t)
 
 -- | Compute the normal form of a term wrt only oriented rules, using outermost reduction.
 simplifyOutermost :: (Function f, Has a (Rule f)) => Index f a -> Term f -> Term f
 simplifyOutermost !idx !t
   | t == u = t
-  | otherwise = simplify idx u
+  | otherwise = simplifyOutermost idx u
   where
     u = build (simp (singleton t))
 
@@ -238,41 +251,44 @@
 -- | A strategy gives a set of possible reductions for a term.
 type Strategy f = Term f -> [Reduction f]
 
--- | A reduction proof is just a sequence of rewrite steps, stored
--- as a list in reverse order. In each rewrite step, all subterms that
--- are exactly equal to the LHS of the rule are replaced by the RHS,
--- i.e. the rewrite step is performed as a parallel rewrite without
--- matching.
-type Reduction f = [Rule f]
+-- | A reduction proof is just a sequence of rewrite steps. In each
+-- rewrite step, all subterms that are exactly equal to the LHS of the
+-- rule are replaced by the RHS, i.e. the rewrite step is performed as
+-- a parallel rewrite without matching.
+type Reduction f = [(Rule f, Subst f)]
 
 -- | Transitivity for reduction sequences.
 trans :: Reduction f -> Reduction f -> Reduction f
-trans p q = q ++ p
+trans p q = p ++ q
 
 -- | Compute the final term resulting from a reduction, given the
 -- starting term.
 result :: Term f -> Reduction f -> Term f
 result t [] = t
-result t (r:rs) = ruleResult u r
+result t (r:rs) = result u rs
   where
-    u = result t rs
+    !u = ruleResult t r
 
 -- | Turn a reduction into a proof.
 reductionProof :: Function f => Term f -> Reduction f -> Derivation f
-reductionProof t ps = red t (Proof.Refl t) (reverse ps)
+reductionProof t ps = red t (Proof.Refl t) ps
   where
     red _ p [] = p
     red t p (q:qs) =
       red (ruleResult t q) (p `Proof.trans` ruleProof t q) qs
 
 -- Helpers for result and reductionProof.
-ruleResult :: Term f -> Rule f -> Term f
-ruleResult t r = build (replace (lhs r) (rhs r) (singleton t))
+ruleResult :: Term f -> (Rule f, Subst f) -> Term f
+ruleResult t (r0, sub) = build (replace (lhs r) (rhs r) (singleton t))
+  where
+    r = subst sub r0
 
-ruleProof :: Function f => Term f -> Rule f -> Derivation f
-ruleProof t r@(Rule _ _ lhs _)
-  | t == lhs = ruleDerivation r
-  | len t < len lhs = Proof.Refl t
+ruleProof :: Function f => Term f -> (Rule f, Subst f) -> Derivation f
+ruleProof t (r0, sub)
+  | t == lhs r = ruleDerivation r
+  | len t < len (lhs r) = Proof.Refl t
+  where
+    r = subst sub r0
 ruleProof (App f ts) rule =
   Proof.cong f [ruleProof u rule | u <- unpack ts]
 ruleProof t _ = Proof.Refl t
@@ -284,17 +300,12 @@
 -- | Normalise a term wrt a particular strategy.
 {-# INLINE normaliseWith #-}
 normaliseWith :: Function f => (Term f -> Bool) -> Strategy f -> Term f -> Reduction f
-normaliseWith ok strat t = res
+normaliseWith ok strat t = aux t
   where
-    res = aux 0 [] t
-    aux 1000 p _ =
-      error $
-        "Possibly nonterminating rewrite:\n" ++ prettyShow p
-    aux n p t =
+    aux t =
       case anywhere strat t of
-        (q:_) | u <- result t q, ok u ->
-          aux (n+1) (p `trans` q) u
-        _ -> p
+        (p:_) | u <- result t p, ok u -> p `trans` aux u
+        _ -> []
 
 -- | Compute all normal forms of a set of terms wrt a particular strategy.
 normalForms :: Function f => Strategy f -> Map (Term f) (Reduction f) -> Map (Term f) (Term f, Reduction f)
@@ -350,7 +361,7 @@
 rewrite p rules t = do
   (sub, rule) <- Index.matches t rules
   guard (p (the rule) sub)
-  return [subst sub (the rule)]
+  return [(the rule, sub)]
 
 -- | A strategy which applies one rule only.
 {-# INLINEABLE tryRule #-}
@@ -358,7 +369,7 @@
 tryRule p rule t = do
   sub <- maybeToList (match (lhs (the rule)) t)
   guard (p (the rule) sub)
-  return [subst sub (the rule)]
+  return [(the rule, sub)]
 
 -- | Check if a rule can be applied, given an ordering <= on terms.
 {-# INLINEABLE reducesWith #-}
@@ -414,3 +425,429 @@
 reducesSkolem :: Function f => Rule f -> Subst f -> Bool
 reducesSkolem rule sub =
   reducesWith (\t u -> lessEqSkolem t u) rule sub
+
+--------------------------------------------------------------------------------
+-- * Rewriting that performs only a single step at a time (not in parallel).
+--------------------------------------------------------------------------------
+
+-- | A reduction proof is a sequence of rewrite steps, stored as a
+-- list. Each rewrite step is coded as a rule, a
+-- substitution and a path to be rewritten.
+type Reduction1 f = [(Rule f, Subst f, [Int])]
+
+-- | Transitivity for reduction sequences.
+trans1 :: Reduction1 f -> Reduction1 f -> Reduction1 f
+trans1 p q = p ++ q
+
+-- TODO: get rid of the below copy-and-pasting by introducing a typeclass
+
+-- | Compute the final term resulting from a reduction, given the
+-- starting term.
+result1 :: HasCallStack => Term f -> Reduction1 f -> Term f
+result1 t [] = t
+result1 t (r:rs) = result1 u rs
+  where
+    !u = ruleResult1 t r
+
+-- | Turn a reduction into a proof.
+reductionProof1 :: Function f => Term f -> Reduction1 f -> Derivation f
+reductionProof1 t ps = red t (Proof.Refl t) ps
+  where
+    red _ p [] = p
+    red t p (q:qs) =
+      red (ruleResult1 t q) (p `Proof.trans` ruleProof1 t q) qs
+
+-- Helpers for result1 and reductionProof1.
+ruleResult1 :: HasCallStack => Term f -> (Rule f, Subst f, [Int]) -> Term f
+ruleResult1 t (r0, sub, p)
+  | t `at` n == lhs r =
+    build (replacePosition n (rhs r) (singleton t))
+  | otherwise = error "ruleResult1: selected subterm is not equal to lhs of rule"
+  where
+    r = subst sub r0
+    n = pathToPosition t p
+
+ruleProof1 :: Function f => Term f -> (Rule f, Subst f, [Int]) -> Derivation f
+ruleProof1 t (r0, sub, p)
+  | t `atPath` p == lhs r =
+    Proof.congPath p t (ruleDerivation r)    
+  | otherwise = error "ruleProof1: selected subterm is not equal to lhs of rule"
+  where
+    r = subst sub r0
+
+-- | A strategy gives a set of possible reductions for a term.
+type Strategy1 f = Term f -> [(Rule f, Subst f, [Int])]
+
+-- | Apply a strategy anywhere in a term.
+anywhere1 :: Strategy1 f -> Strategy1 f
+anywhere1 strat t =
+  stamp "anywhere1 (whnf)"
+  [ (r, sub, p ++ p')
+  | n <- reverse [0..len t-1], -- innermost
+    let p = positionToPath t n,
+    (r, sub, p') <- strat (t `at` n) ]
+
+-- | Apply a basic strategy to a term.
+basic :: Strategy f -> Strategy1 f
+basic strat t = [(r, sub, []) | [(r, sub)] <- strat t]
+
+-- | Normalise a term wrt a particular strategy.
+{-# INLINE normaliseWith1 #-}
+normaliseWith1 :: Function f => (Term f -> Bool) -> Strategy1 f -> Term f -> Reduction1 f
+normaliseWith1 ok strat t = aux t
+  where
+    aux t =
+      case anywhere1 strat t of
+        (p:_) | u <- ruleResult1 t p, ok u ->
+          [p] `trans1` aux u
+        _ -> []
+
+-- | Normalise a term wrt a particular strategy, picking random
+-- rewrites at every step.
+{-# INLINE normaliseWith1Random #-}
+normaliseWith1Random :: Function f => (Term f -> Bool) -> Strategy1 f -> Term f -> Gen (Reduction1 f)
+normaliseWith1Random ok strat t = aux t
+  where
+    aux t =
+      let choices = [(p, u) | p <- anywhere1 strat t, let u = stamp "normaliseWith1Random.result1" (ruleResult1 t p), ok u] in
+      case choices of
+        [] -> return []
+        _ -> do
+          (p, u) <- elements choices
+          fmap ([p] `trans1`) (aux u)
+
+rematchReduction1 :: HasCallStack => Term f -> Reduction1 f -> Reduction1 f
+rematchReduction1 _ [] = []
+rematchReduction1 t ((r, _, pos):rs) =
+  case match (lhs r) (t `atPath` pos) of
+    Just sub ->
+      let red = (r, sub, pos) in
+      red:rematchReduction1 (ruleResult1 t red) rs
+    Nothing -> error "rematch failed"
+
+--------------------------------------------------------------------------------
+-- * Testing whether a term has a unique normal form.
+--------------------------------------------------------------------------------
+
+data UNF f =
+    -- Function has a unique normal form
+    UniqueNormalForm (Term f) (Reduction1 f)
+  | -- This pair of rules has an unjoinable critical pair
+    HasCriticalPair (Rule f) (Rule f, Int) (ConfluenceFailure f)
+
+data ConfluenceFailure f =
+  ConfluenceFailure {
+    cf_term  :: Term f,
+    cf_left  :: Reduction1 f,
+    cf_right :: Reduction1 f,
+    cf_orig_term :: Term f,
+    cf_orig_left :: Reduction1 f }
+
+cf_left_term, cf_right_term :: ConfluenceFailure f -> Term f
+cf_left_term ConfluenceFailure{..} = result1 cf_term cf_left
+cf_right_term ConfluenceFailure{..} = result1 cf_term cf_right
+{-
+cf_orig_left_term, cf_orig_right_term :: ConfluenceFailure f -> Term f
+cf_orig_left_term ConfluenceFailure{..} = result1 cf_orig_term cf_orig_left
+cf_orig_right_term ConfluenceFailure{..} = result1 cf_orig_term cf_orig_right
+-}
+instance Semigroup (UNF f) where
+  -- mconcat finds the first HasCriticalPair in the list
+  UniqueNormalForm{} <> x = x
+  x@HasCriticalPair{} <> _ = x
+
+instance Function f => Pretty (UNF f) where
+  pPrint UniqueNormalForm{} = text "unique normal form"
+  pPrint (HasCriticalPair r1 (r2, n) _) = text "critical pair" <+> pPrint r1 <+> pPrint (r2, n)
+
+hasUNFRetry :: Function f => Strategy1 f -> ConfluenceFailure f -> UNF f
+hasUNFRetry strat ConfluenceFailure{..} =
+  hasUNF strat cf_orig_term cf_orig_left {- <>
+  hasUNF strat cf_term cf_right -}
+
+hasUNFRandom :: Function f => Strategy1 f -> Term f -> Gen (UNF f)
+hasUNFRandom strat t =
+  sconcat . NonEmpty.fromList <$> sequence
+  [ do r <- normaliseWith1Random (const True) strat u
+       return (hasUNF strat u r)
+  | u <- reverseSubterms t,
+    _ <- [1..5] ]
+
+hasUNFSimple :: Function f => Strategy1 f -> Term f -> Reduction1 f -> UNF f
+hasUNFSimple strat t0 r0 = magic t0 r0
+  where
+    normSteps t = normaliseWith1 (const True) strat t
+    norm =
+      memo $ \t ->
+        stamp "hasUNF.norm" $
+        case anywhere1 strat t of
+          [] -> t
+          r:_ -> norm (ruleResult1 t r)
+
+    magic t [] = UniqueNormalForm (norm t) (normSteps t)
+    magic t (r@(rule, sub, pos):rs) =
+      case magic (ruleResult1 t r) rs of
+        res@HasCriticalPair{} -> res
+        UniqueNormalForm v rsu ->
+          maybe (UniqueNormalForm v (r:rsu)) sconcat $ NonEmpty.nonEmpty $ outer `mplus` inner
+      where
+        outer = do
+          let t' = t `atPath` pos
+          n <- [1..len t'-1] -- 0 case is handled in inner
+          let pos' = positionToPath t' n
+          guard (not (isVar (t' `at` n)))
+          guard (criticalOverlap (lhs rule) pos')
+          (rule', sub', []) <- strat (t' `at` n)
+
+          guard (norm (ruleResult1 t (rule', sub', pos ++ pos')) /= norm (ruleResult1 t r))
+          return $
+            HasCriticalPair rule (rule', pathToPosition (lhs rule) pos') $
+            ConfluenceFailure t' [(rule, sub, [])] [(rule', sub', pos')] t0 r0
+
+        inner = do
+          pos' <- inits pos
+          let t' = t `atPath` pos'
+          (rule', sub', []) <- strat t'
+          let posInner = drop (length pos') pos
+          guard (criticalOverlap (lhs rule') posInner)
+
+          guard (norm (ruleResult1 t (rule', sub', pos')) /= norm (ruleResult1 t r))
+          return $
+            HasCriticalPair rule' (rule, pathToPosition (lhs rule') posInner) $
+            ConfluenceFailure t' [(rule', sub', [])] [(rule, sub, posInner)] t0 r0
+
+    criticalOverlap (Var _) _ = False
+    criticalOverlap App{} [] = True
+    criticalOverlap t (p:ps) = criticalOverlap (unpack (children t) !! p) ps
+
+hasUNF :: (HasCallStack, Function f) => Strategy1 f -> Term f -> Reduction1 f -> UNF f
+hasUNF strat t0 r0 =
+  let res = magic t0 r0
+  in stamp (case res of { UniqueNormalForm{} -> "hasUNF.UNF"; HasCriticalPair{} -> "hasUNF.CP" }) res
+  where
+    trace _ x = x
+    --normFirstStep t = trace (prettyShow (t, take 1 $ anywhere1 strat t)) $ head (head (anywhere1 strat t))
+    normSteps t = normaliseWith1 (const True) strat t
+    normStepsVia r t = r `trans1` normSteps (result1 t r)
+    norm =
+      memo $ \t ->
+        stamp "hasUNF.norm" $
+        case anywhere1 strat t of
+          [] -> t
+          r:_ -> norm (ruleResult1 t r)
+
+    normStepsR t = unGen (replicateM 10 (normaliseWith1Random (const True) strat t)) (mkQCGen 1234) 10
+    --normR t = result1 t (normStepsR t)
+
+    --magic :: Term f -> Reduction1 f -> UNF f
+    magic t [] = UniqueNormalForm (norm t) (normSteps t)
+    magic t (r:rs) =
+      let u = ruleResult1 t r in
+      case magic u rs of
+        res@HasCriticalPair{} -> res
+        UniqueNormalForm v rsu ->
+          sconcat (NonEmpty.fromList [magic1 t rst r u rsu v | rst <- normStepsR t])
+
+    magic1 t rst (r, sub, p) u rsu v
+      | nt == v = UniqueNormalForm v rst
+      | not (oriented (orientation r)) && not (reducesSkolem r sub) =
+        -- v <-* u -> t, nt /= v
+        conflict u rsu v ([(backwards r, sub, p)] `trans1` rst) nt
+      | otherwise = conflict t ([(r, sub, p)] `trans1` rsu) v rst nt
+      where
+        nt = result1 t rst
+      
+    -- precondition: normR t r1 /= normR t r2
+    --conflict, conflict' :: Term f -> Reduction1 f -> Term f -> Reduction1 f -> Term f -> UNF f
+    conflict t rs1 u rs2 v = stamp "conflict" (conflict' t rs1 u rs2 v)
+    conflict' t (r1:rs1) u (r2:rs2) v
+      | trace "" $
+        trace ("Conflicting term: " ++ prettyShow t) $
+        trace ("Rule 1: " ++ prettyShow r1) $
+        trace ("Rule 2: " ++ prettyShow r2) $
+        trace "" False = undefined
+
+    conflict' t (r1:rs1) u (r2:rs2) v
+      | not ok = error "not ok"
+      | r1 == r2 = conflict' (ruleResult1 t r1) rs1 u rs2 v
+      | otherwise =
+        case commute t r1 r2 of
+          Nothing -> criticalPair t r1 r2
+          Just (rs1', rs2') ->
+            trace "" $
+            trace ("t = " ++ prettyShow t) $
+            trace ("r1 = " ++ prettyShow r1) $
+            trace ("u = " ++ prettyShow (ruleResult1 t r1)) $
+            trace ("r2 = " ++ prettyShow r2) $
+            trace ("v = " ++ prettyShow (ruleResult1 t r2)) $
+            trace ("rs1' = " ++ prettyShow rs1') $
+            trace ("rs2' = " ++ prettyShow rs2') $
+            let w = result1 t (r1:rs1') in
+            if norm w == u then
+              conflict' (ruleResult1 t r2) (rs2' ++ normSteps w) u rs2 v
+            else
+              conflict' (ruleResult1 t r1) rs1 u (rs1' ++ normSteps w) (norm w)
+      where
+        ok =
+          norm u == u && norm v == v &&
+          result1 t (r1:rs1) == u &&
+          result1 t (r2:rs2) == v
+
+    criticalPair t (r1, sub1, (p1:ps1)) (r2, sub2, (p2:ps2))
+      | p1 == p2 = criticalPair (unpack (children t) !! p1) (r1, sub1, ps1) (r2, sub2, ps2)
+    criticalPair t (r1, sub1, []) (r2, sub2, p) =
+      makeCriticalPair t r1 sub1 r2 sub2 p
+    criticalPair t (r1, sub1, p) (r2, sub2, []) =
+      makeCriticalPair t r2 sub2 r1 sub1 p
+
+    makeCriticalPair t r1 sub1 r2 sub2 p =
+      HasCriticalPair r1 (r2, pathToPosition (lhs r1) p) $
+      ConfluenceFailure t [(r1, sub1, [])] [(r2, sub2, p)] t0 r0
+      
+    --commute :: Term f -> (Rule f, Subst f, [Int]) -> (Rule f, Subst f, [Int]) -> Maybe (Reduction1 f, Reduction1 f)
+    commute t r1@(rule1, sub1, (p1:ps1)) r2@(rule2, sub2, (p2:ps2))
+      | p1 == p2 =
+        -- descend into same subterm
+        fmap (both (map (atPos p1))) (commute (unpack (children t) !! p1) (rule1, sub1, ps1) (rule2, sub2, ps2))
+      | otherwise =
+        -- parallel subterms
+        trace "parallel subterms" $ Just ([r2], [r1])
+    commute t r1@(_, _, _:_) r2@(_, _, []) =
+      -- swap rules so the one which rewrites the root comes first
+      fmap (\(x, y) -> (y, x)) $ commute t r2 r1
+    commute t r1@(rule1, _, []) r2@(_, _, ps)
+      | not (criticalOverlap (lhs rule1) ps) =
+        trace "non-overlapping" $ Just (nonOverlapping t r1 r2)
+    commute t r1 r2
+      | norm u == norm v = trace "joinable" $ Just (normSteps u, normSteps v)
+        where
+          u = ruleResult1 t r1
+          v = ruleResult1 t r2
+    commute _ _ _ = Nothing
+
+    -- Precondition: r1 can be commuted with some number of parallel
+    -- rewrites of r2
+    nonOverlapping t r1 r2 = stamp "nonOverlapping" (nonOverlapping' t r1 r2)
+    nonOverlapping' t r1@(rule1, _, p1) r2@(rule2, _, p2)
+      | trace "" $
+        trace ("Non-overlapping reduction: " ++ prettyShow t) $
+        trace ("First rule: " ++ prettyShow r1) $
+        trace ("Second rule: " ++ prettyShow r2) $
+        trace ("Reduction of first rule: " ++ prettyShow u) $
+        trace ("Reduction of second rule: " ++ prettyShow v) $
+        trace ("Positions before: " ++ prettyShow ps2Before) $
+        trace ("Positions after: " ++ prettyShow ps2After) $
+        trace ("Rules before: " ++ prettyShow rs2Before) $
+        trace ("Rules after: " ++ prettyShow rs2After) $
+        trace ("Final step: " ++
+          if correctlyOriented && not reflexivity then "right " ++ prettyShow [(rule1, sub1After, p1)]
+          else if not (correctlyOriented || reflexivity) then "left " ++ prettyShow [(backwards rule1, sub1After, p1)]
+          else "none") $
+        trace ("Final term: " ++ prettyShow w) $
+        trace ("Rewrite proof:\n" ++ prettyShow (Proof.certify (reductionProof1 t ([r1] `trans1` conf1)))) $
+        trace ("Rewrite proof:\n" ++ prettyShow (Proof.certify (reductionProof1 t ([r2] `trans1` conf2)))) $
+        False = undefined
+      | otherwise = (conf1, conf2)
+      where
+        u = result1 t [r1]
+        v = result1 t [r2]
+        (ps2Before, ps2After) = track rule1 p1 p2
+        rs2Before = [(rule2, rematch rule2 p t, p) | p <- ps2Before, p /= p2]
+        rs2After = [(rule2, rematch rule2 p u, p) | p <- ps2After]
+
+        -- Two paths:
+        -- (1) r1; rs2After
+        -- (2) rs2Before; r1
+        -- But, in (2), if r1 is oriented the wrong way, we do this instead:
+        -- (1) r1; rs2After; backwards r1
+        -- (2) rs2Before
+
+        -- TODO don't code term ordering
+        correctlyOriented = oriented (orientation rule1) || reducesSkolem rule1 sub1After
+        reflexivity = subst sub1After (lhs rule1) == subst sub1After (rhs rule1)
+        sub1After = rematch rule1 p1 (result1 v rs2Before)
+
+        -- The two reductions are: [red1] `trans` conf1, [red2] `trans` conf2
+        conf1 = rs2After `trans1` (if correctlyOriented || reflexivity then [] else [(backwards rule1, sub1After, p1)])
+        conf2 = rs2Before `trans1` (if correctlyOriented && not reflexivity then [(rule1, sub1After, p1)] else [])
+
+        -- Check that both reductions give the same result
+        w1 = result1 u conf1
+        w2 = result1 v conf2
+        w | w1 == w2 = w1
+        
+    criticalOverlap (Var _) _ = False
+    criticalOverlap App{} [] = True
+    criticalOverlap t (p:ps) = criticalOverlap (unpack (children t) !! p) ps
+
+    atPos p (r, sub, ps) = (r, sub, p:ps)
+    both f (x, y) = (f x, f y)
+
+    -- find the substitution for a rewrite
+    rematch r pos t = sub
+      where
+        Just sub = match (lhs r) (t `atPath` pos)
+
+-- Given a path in a term which is below a variable, find the variable
+-- and the part of the path below the variable
+decomposePath (Var x) ps = (x, ps)
+decomposePath t (p:ps) = decomposePath (unpack (children t) !! p) ps
+
+-- positions of a variable in a term
+varPos :: Var -> Term f -> [Int]
+varPos x t = [n | n <- [0..len t-1], t `at` n == build (var x)]
+
+-- Consider a rewrite t -> u at position pr in a term, and a position
+-- pt that does not overlap with the rewrite:
+-- (1) Suppose that right now the rewrite could be applied, but
+--     instead do a different rewrite at position pt. What other
+--     positions must be also rewrite for the original rewrite to
+--     still be applicable?
+--     (e.g.: if the rule is f(x,x)->..., and the position is one of
+--     the "x"s, if we rewrite one "x" we must also rewrite the other)
+-- (2) Where does the position pt "move to" after the rewrite?
+track :: Rule f -> [Int] -> [Int] -> ([[Int]], [[Int]])
+track r (p:pr) (p':pt)
+    -- common prefix
+  | p == p' = (map (p:) *** map (p:)) (track r pr pt)
+    -- parallel prefix
+  | otherwise = ([p':pt], [p':pt])
+track _ (_:_) [] =
+  -- position being tracked < position of rewrite
+  ([[]], [[]])
+track Rule{lhs = lhs, rhs = rhs} [] pt =
+  -- strategy: find what variable position pt occurs under in the lhs of the rule,
+  -- then find all occurrences of that variable in the rhs of the rule
+  let
+    (x, p) = decomposePath lhs pt
+  in
+    ([positionToPath lhs n ++ p | n <- varPos x lhs],
+     [positionToPath rhs n ++ p | n <- varPos x rhs])
+
+{-
+hasUNFSlow :: Function f => Strategy1 f -> Term f -> UNF f
+hasUNFSlow strat t0 =
+  head $
+    -- optimisation: check if any subterm has a non-unique normal form first
+    [r | r@HasCriticalPair{} <- map magic (sortBy (comparing len) (properSubterms t0))] ++
+    [magic t0]
+  where
+    magic = memo $ \t ->
+      --trace ("magic " ++ prettyShow t) $
+      let
+        as = [(red, {-trace ("recursing from " ++ prettyShow t ++ " to " ++ prettyShow (result1 t red) ++ " via " ++ prettyShow red) $-} magic (result1 t red)) | red <- strat t, if result1 t red == t then error "oops" else True]
+
+        conflict (r1, []) (r2, p) = HasCriticalPair r1 (r2, pathToPosition (lhs r1) p)
+        conflict (r1, p) (r2, []) = HasCriticalPair r2 (r1, pathToPosition (lhs r2) p)
+        conflict (r1, (m:ms)) (r2, (n:ns)) | m == n = conflict (r1, ms) (r2, ns)
+        conflict _ _ = error "something has gone wrong in the magic function"
+
+        res = head $
+          [r | r@HasCriticalPair{} <- map snd as] ++
+          case nubBy ((==) `on` snd) ([(red, t) | (red, UniqueNormalForm t) <- as]) of
+            [] -> [UniqueNormalForm t]
+            [(_, t)] -> [UniqueNormalForm t]
+            ((r1, _, n1):_, t1):((r2, _, n2):_, t2):_ ->
+              [conflict (r1, positionToPath t n1) (r2, positionToPath t n2)]
+      in {-traceShow (pPrint res)-} res
+-}
diff --git a/Twee/Term.hs b/Twee/Term.hs
--- a/Twee/Term.hs
+++ b/Twee/Term.hs
@@ -33,7 +33,7 @@
   build, buildList,
   con, app, var,
   -- * Access to subterms
-  children, properSubterms, subtermsList, subterms, reverseSubtermsList, reverseSubterms, occurs, isSubtermOf, isSubtermOfList, at,
+  children, properSubterms, subtermsList, subterms, reverseSubtermsList, reverseSubterms, occurs, isSubtermOf, isSubtermOfList, at, listAt, atPath,
   -- * Substitutions
   Substitution(..),
   subst,
@@ -79,6 +79,7 @@
 import Twee.Utils
 import qualified Data.Label as Label
 import Data.Typeable
+import GHC.Stack
 
 --------------------------------------------------------------------------------
 -- * A type class for builders
@@ -520,6 +521,14 @@
 empty :: forall f. TermList f
 empty = buildList (mempty :: Builder f)
 
+-- | Index into a term.
+at :: Term f -> Int -> Term f
+t `at` n = singleton t `listAt` n
+
+-- | Index into a term using a path.
+atPath :: Term f -> [Int] -> Term f
+t `atPath` p = t `at` pathToPosition t p
+
 -- | Get the children (direct subterms) of a term.
 children :: Term f -> TermList f
 children t =
@@ -607,7 +616,7 @@
 {-# INLINE reverseSubtermsList #-}
 reverseSubtermsList :: TermList f -> [Term f]
 reverseSubtermsList t =
-  [ unsafeAt n t | n <- [k-1,k-2..0] ]
+  [ t `unsafeListAt` n | n <- [k-1,k-2..0] ]
   where
     k = lenList t
 
@@ -711,7 +720,7 @@
       | otherwise = list (k+1) u (n-len t)
 
 -- | Convert a path in a term into a position.
-pathToPosition :: Term f -> [Int] -> Int
+pathToPosition :: HasCallStack => Term f -> [Int] -> Int
 pathToPosition t ns = term 0 t ns
   where
     term k _ [] = k
diff --git a/Twee/Term/Core.hs b/Twee/Term/Core.hs
--- a/Twee/Term/Core.hs
+++ b/Twee/Term/Core.hs
@@ -85,14 +85,14 @@
 type role TermList nominal
 
 -- | Index into a termlist.
-at :: Int -> TermList f -> Term f
-at n t
+listAt :: TermList f -> Int -> Term f
+t `listAt` n
   | n < 0 || low t + n >= high t = error "term index out of bounds"
-  | otherwise = unsafeAt n t
+  | otherwise = t `unsafeListAt` n
 
 -- | Index into a termlist, without bounds checking.
-unsafeAt :: Int -> TermList f -> Term f
-unsafeAt n (TermList lo hi arr) =
+unsafeListAt :: TermList f -> Int -> Term f
+TermList lo hi arr `unsafeListAt` n =
   case TermList (lo+n) hi arr of
     UnsafeCons t _ -> t
 
diff --git a/twee-lib.cabal b/twee-lib.cabal
--- a/twee-lib.cabal
+++ b/twee-lib.cabal
@@ -1,5 +1,5 @@
 name:                twee-lib
-version:             2.4.2
+version:             2.5
 synopsis:            An equational theorem prover
 homepage:            http://github.com/nick8325/twee
 license:             BSD3
@@ -51,6 +51,7 @@
     Twee.Constraints
     Twee.CP
     Twee.Equation
+    Twee.Generate
     Twee.Index
     Twee.Join
     Twee.KBO
@@ -62,6 +63,7 @@
     Twee.Term
     Twee.Task
     Twee.Utils
+    Twee.Term.Core
     Data.Label
   other-modules:
     Data.BatchedQueue
@@ -70,10 +72,10 @@
     Data.Heap
     Data.Numbered
     Data.PackedSequence
-    Twee.Term.Core
 
   build-depends:
-    base >= 4 && < 5,
+    -- base >= 4.11 for Semigroup in Prelude
+    base >= 4.11 && < 5,
     containers,
     transformers,
     dlist,
@@ -83,7 +85,8 @@
     uglymemo,
     random,
     bytestring,
-    cereal
+    cereal,
+    QuickCheck
   hs-source-dirs:      .
   ghc-options:         -W -fno-warn-incomplete-patterns -fno-warn-dodgy-imports
   default-language:    Haskell2010