diff --git a/Twee.hs b/Twee.hs
--- a/Twee.hs
+++ b/Twee.hs
@@ -434,11 +434,11 @@
 -- Name and number are for information only.
 data Goal f =
   Goal {
-    goal_name   :: String,
-    goal_number :: Int,
-    goal_eqn    :: Equation f,
-    goal_lhs    :: Set (Resulting f),
-    goal_rhs    :: Set (Resulting f) }
+    goal_name     :: String,
+    goal_number   :: Int,
+    goal_eqn      :: Equation f,
+    goal_lhs      :: Set (Resulting f),
+    goal_rhs      :: Set (Resulting f) }
 
 -- Add a new goal.
 {-# INLINEABLE addGoal #-}
@@ -450,14 +450,35 @@
 {-# INLINEABLE normaliseGoals #-}
 normaliseGoals :: Function f => State f -> State f
 normaliseGoals state@State{..} =
-  {-# SCC normaliseGoals #-}
   state {
     st_goals =
-      map (goalMap (successors (rewrite reduces (index_all st_rules)) . Set.toList)) st_goals }
+      map (goalMap (Rule.normalForms (rewrite reduces (index_all st_rules)))) st_goals }
   where
     goalMap f goal@Goal{..} =
       goal { goal_lhs = f goal_lhs, goal_rhs = f goal_rhs }
 
+-- Recompute all normal forms of all goals. Starts from the original goal term.
+-- Different from normalising all goals, because there may be an intermediate
+-- term on one of the reduction paths which we can now rewrite in a different
+-- way.
+{-# INLINEABLE recomputeGoals #-}
+recomputeGoals :: Function f => State f -> State f
+recomputeGoals state =
+  -- Make this strict so that newTask can time it correctly
+  forceList (map goal_lhs (st_goals state')) `seq`
+  forceList (map goal_rhs (st_goals state')) `seq`
+  state'
+  where
+    state' =
+      normaliseGoals (state { st_goals = map reset (st_goals state) })
+
+    reset goal@Goal{goal_eqn = t :=: u, ..} =
+      goal { goal_lhs = Set.singleton (reduce (Refl t)),
+             goal_rhs = Set.singleton (reduce (Refl u)) }
+
+    forceList [] = ()
+    forceList (x:xs) = x `seq` forceList xs
+
 -- Create a goal.
 {-# INLINE goal #-}
 goal :: Int -> String -> Equation f -> Goal f
@@ -517,7 +538,6 @@
       sub <- match t' t
       matchIn sub u' u
 
-
 ----------------------------------------------------------------------
 -- The main loop.
 ----------------------------------------------------------------------
@@ -535,11 +555,14 @@
          lift $ output_message SimplifyQueue
          state <- StateM.get
          StateM.put $! simplifyQueue config state,
-       newTask 0.25 0.05 $ do
+       newTask 1 0.05 $ do
          when cfg_simplify $ do
            lift $ output_message Interreduce
            state <- StateM.get
-           StateM.put $! interreduce config state]
+           StateM.put $! interreduce config state,
+       newTask 1 0.02 $ do
+          state <- StateM.get
+          StateM.put $! recomputeGoals state ]
 
     let
       loop = do
@@ -608,7 +631,7 @@
 {-# INLINEABLE normalForms #-}
 normalForms :: Function f => State f -> Term f -> Set (Resulting f)
 normalForms State{..} t =
-  Rule.normalForms (rewrite reduces (index_all st_rules)) [reduce (Refl t)]
+  Rule.normalForms (rewrite reduces (index_all st_rules)) (Set.singleton (reduce (Refl t)))
 
 {-# INLINEABLE simplifyTerm #-}
 simplifyTerm :: Function f => State f -> Term f -> Term f
diff --git a/Twee/Base.hs b/Twee/Base.hs
--- a/Twee/Base.hs
+++ b/Twee/Base.hs
@@ -193,6 +193,7 @@
 class Skolem f where
   -- | Turn a variable into a Skolem constant.
   skolem  :: Var -> Fun f
+  getSkolem :: Fun f -> Maybe Var
 
 -- | For types which have a notion of arity.
 class Arity f where
@@ -273,6 +274,8 @@
 
 instance (Typeable f, Ord f) => Skolem (Extended f) where
   skolem x = fun (Skolem x)
+  getSkolem (F (Skolem x)) = Just x
+  getSkolem _ = Nothing
 
 instance EqualsBonus f => EqualsBonus (Extended f) where
   hasEqualsBonus (Function f) = hasEqualsBonus f
diff --git a/Twee/CP.hs b/Twee/CP.hs
--- a/Twee/CP.hs
+++ b/Twee/CP.hs
@@ -184,6 +184,8 @@
     size' n ts
       | Cons (App f ws@(Cons a (Cons b us))) vs <- ts,
         hasEqualsBonus (fun_value f),
+        not (isVar a),
+        not (isVar b),
         Just sub <- unify a b =
         size' (n+cfg_funweight*size f) ws `min`
         size' (size' (n+1) (subst sub us)) (subst sub vs)
diff --git a/Twee/Join.hs b/Twee/Join.hs
--- a/Twee/Join.hs
+++ b/Twee/Join.hs
@@ -54,8 +54,8 @@
       Right (Nothing, [])
     _ | cfg_set_join config &&
         not (null $ Set.intersection
-          (normalForms (rewrite reduces (index_all idx)) [reduce (Refl t)])
-          (normalForms (rewrite reduces (index_all idx)) [reduce (Refl u)])) ->
+          (normalForms (rewrite reduces (index_all idx)) (Set.singleton (reduce (Refl t))))
+          (normalForms (rewrite reduces (index_all idx)) (Set.singleton (reduce (Refl u))))) ->
       Right (Just cp, [])
     Just cp ->
       case groundJoinFromMaybe config eqns idx mmodel (branches (And [])) cp of
diff --git a/Twee/Rule.hs b/Twee/Rule.hs
--- a/Twee/Rule.hs
+++ b/Twee/Rule.hs
@@ -3,7 +3,7 @@
 module Twee.Rule where
 
 import Twee.Base
-import Twee.Constraints
+import Twee.Constraints hiding (funs)
 import qualified Twee.Index as Index
 import Twee.Index(Index)
 import Control.Monad
@@ -351,33 +351,36 @@
         _ -> Resulting t p
 
 -- | Compute all normal forms of a set of terms wrt a particular strategy.
-normalForms :: Function f => Strategy f -> [Resulting f] -> Set (Resulting f)
+normalForms :: Function f => Strategy f -> Set (Resulting f) -> Set (Resulting f)
 normalForms strat ps = snd (successorsAndNormalForms strat ps)
 
 -- | Compute all successors of a set of terms (a successor of a term @t@
 -- is a term @u@ such that @t ->* u@).
-successors :: Function f => Strategy f -> [Resulting f] -> Set (Resulting f)
-successors strat ps = Set.union qs rs
+successors :: Function f => Strategy f -> Set (Resulting f) -> Set (Resulting f)
+successors strat ps =
+  Set.union qs rs
   where
     (qs, rs) = successorsAndNormalForms strat ps
 
 {-# INLINEABLE successorsAndNormalForms #-}
-successorsAndNormalForms :: Function f => Strategy f -> [Resulting f] ->
+successorsAndNormalForms :: Function f => Strategy f -> Set (Resulting f) ->
   (Set (Resulting f), Set (Resulting f))
 successorsAndNormalForms strat ps =
   {-# SCC successorsAndNormalForms #-} go Set.empty Set.empty ps
   where
-    go dead norm [] = (dead, norm)
-    go dead norm (p:ps)
-      | p `Set.member` dead = go dead norm ps
-      | p `Set.member` norm = go dead norm ps
-      | null qs = go dead (Set.insert p norm) ps
-      | otherwise =
-        go (Set.insert p dead) norm (qs ++ ps)
-      where
-        qs =
-          [ reduce (reduction p `Trans` q)
-          | q <- anywhere strat (result p) ]
+    go dead norm ps =
+      case Set.minView ps of
+        Nothing -> (dead, norm)
+        Just (p, ps)
+          | p `Set.member` dead -> go dead norm ps
+          | p `Set.member` norm -> go dead norm ps
+          | null qs -> go dead (Set.insert p norm) ps
+          | otherwise ->
+            go (Set.insert p dead) norm (Set.fromList qs `Set.union` ps)
+          where
+            qs =
+              [ reduce (reduction p `trans` q)
+              | q <- anywhere strat (result p) ]
 
 -- | Apply a strategy anywhere in a term.
 anywhere :: Strategy f -> Strategy f
@@ -485,4 +488,5 @@
 reducesSkolem rule sub =
   reducesWith (\t u -> lessEq (subst skolemise t) (subst skolemise u)) rule sub
   where
-    skolemise = con . skolem
+    skolemise (V x) = con (skolem (V (x + k)))
+    V k = maximum (V 0:map succ (catMaybes (map getSkolem (funs rule))))
diff --git a/Twee/Term.hs b/Twee/Term.hs
--- a/Twee/Term.hs
+++ b/Twee/Term.hs
@@ -48,7 +48,7 @@
   match, matchIn, matchList, matchListIn, isInstanceOf, isVariantOf,
   -- * Unification
   unify, unifyList,
-  unifyTri, unifyListTri,
+  unifyTri, unifyListTri, unifyListTriFrom,
   TriangleSubst(..),
   close,
   -- * Positions in terms
@@ -401,7 +401,11 @@
 -- | Unify two termlists, returning a triangle substitution.
 -- This is slightly faster than 'unify'.
 unifyListTri :: TermList f -> TermList f -> Maybe (TriangleSubst f)
-unifyListTri !t !u = fmap Triangle ({-# SCC unify #-} loop emptySubst t u)
+unifyListTri t u = unifyListTriFrom t u (Triangle emptySubst)
+
+unifyListTriFrom :: TermList f -> TermList f -> TriangleSubst f -> Maybe (TriangleSubst f)
+unifyListTriFrom !t !u (Triangle !sub) =
+  fmap Triangle ({-# SCC unify #-} loop sub t u)
   where
     loop !_ !_ !_ | False = undefined
     loop sub Empty Empty = Just sub
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.1.3
+version:             2.1.4
 synopsis:            An equational theorem prover
 homepage:            http://github.com/nick8325/twee
 license:             BSD3