diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,4 +1,4 @@
-Copyright (c) 2009-2018, Nick Smallbone
+Copyright (c) 2009-2026, Nick Smallbone
 
 All rights reserved.
 
diff --git a/quickspec.cabal b/quickspec.cabal
--- a/quickspec.cabal
+++ b/quickspec.cabal
@@ -1,5 +1,5 @@
 Name:                quickspec
-Version:             2.2
+Version:             2.2.1
 Cabal-version:       >= 1.10
 Build-type:          Simple
 
@@ -9,7 +9,7 @@
 
 License:             BSD3
 License-file:        LICENSE
-Copyright:           2009-2019 Nick Smallbone
+Copyright:           2009-2026 Nick Smallbone
 
 Category:            Testing
 
@@ -67,7 +67,7 @@
 
 source-repository head
   type:     git
-  location: git://github.com/nick8325/quickspec.git
+  location: https://github.com/nick8325/quickspec.git
   branch:   master
 
 library
@@ -92,6 +92,7 @@
     QuickSpec.Internal.Pruning.Types
     QuickSpec.Internal.Pruning.UntypedTwee
     QuickSpec.Internal.Pruning.PartialApplication
+    QuickSpec.Internal.Pruning.Conditionals
     QuickSpec.Internal.Term
     QuickSpec.Internal.Terminal
     QuickSpec.Internal.Testing
@@ -108,9 +109,10 @@
     containers,
     data-lens-light >= 0.1.1,
     dlist,
+    hashable >= 1.5,
     random,
     spoon,
     template-haskell,
     transformers,
-    twee-lib,
+    twee-lib >= 2.6,
     uglymemo
diff --git a/src/QuickSpec.hs b/src/QuickSpec.hs
--- a/src/QuickSpec.hs
+++ b/src/QuickSpec.hs
@@ -94,10 +94,10 @@
   type (==>), liftC, instanceOf,
 
   -- * Customising QuickSpec
-  withMaxTermSize, withMaxTests, withMaxTestSize, withMaxFunctions, defaultTo,
+  withMaxTermSize, withMaxTermDepth, withMaxTests, withMaxTestSize, withMaxFunctions, defaultTo,
   withPruningDepth, withPruningTermSize, withFixedSeed,
   withInferInstanceTypes, withPrintStyle, PrintStyle(..),
-  withConsistencyCheck,
+  withConsistencyCheck, withBackgroundStrings,
 
   -- * Integrating with QuickCheck
   (=~=),
diff --git a/src/QuickSpec/Internal.hs b/src/QuickSpec/Internal.hs
--- a/src/QuickSpec/Internal.hs
+++ b/src/QuickSpec/Internal.hs
@@ -56,6 +56,11 @@
 addBackground props =
   Sig $ \_ cfg -> cfg { Haskell.cfg_background = Haskell.cfg_background cfg ++ props }
 
+-- | Add some properties to the background theory.
+withBackgroundStrings :: [String] -> Sig
+withBackgroundStrings props =
+  Sig $ \_ cfg -> cfg { Haskell.cfg_background_str = Haskell.cfg_background_str cfg ++ props }
+
 -- | A signature.
 newtype Sig = Sig { unSig :: Context -> Haskell.Config -> Haskell.Config }
 
@@ -357,6 +362,10 @@
 withMaxTermSize :: Int -> Sig
 withMaxTermSize n = Sig (\_ -> setL Haskell.lens_max_size n)
 
+-- | Set the maximum depth of terms to explore (default: unlimited).
+withMaxTermDepth :: Int -> Sig
+withMaxTermDepth n = Sig (\_ -> setL Haskell.lens_max_depth n)
+
 withMaxCommutativeSize :: Int -> Sig
 withMaxCommutativeSize n = Sig (\_ -> setL Haskell.lens_max_commutative_size n)
 
@@ -417,6 +426,11 @@
 -- false laws
 withConsistencyCheck :: Sig
 withConsistencyCheck = Sig (\_ -> setL (Haskell.lens_check_consistency) True)
+
+-- | (Experimental) Still return laws even if a resource limit
+-- occurred (memory exhaustion, timeout caused by System.Timeout)
+withResourceLimitHandling :: Sig
+withResourceLimitHandling = Sig (\_ -> setL (Haskell.lens_handle_resource_limit) True)
 
 -- | A signature containing boolean functions:
 -- @(`||`)@, @(`&&`)@, `not`, `True`, `False`.
diff --git a/src/QuickSpec/Internal/Explore.hs b/src/QuickSpec/Internal/Explore.hs
--- a/src/QuickSpec/Internal/Explore.hs
+++ b/src/QuickSpec/Internal/Explore.hs
@@ -61,7 +61,7 @@
   mapEnumerator (sortBy' measure) e
 
 quickSpec ::
-  (Ord fun, Ord norm, Sized fun, Typed fun, Ord result, PrettyTerm fun,
+  (Ord fun, Ord norm, FuncSized fun, Typed fun, Ord result, PrettyTerm fun,
   MonadPruner (Term fun) norm m, MonadTester testcase (Term fun) m, MonadTerminal m) =>
   (Prop (Term fun) -> m ()) ->
   (Term fun -> testcase -> Maybe result) ->
diff --git a/src/QuickSpec/Internal/Explore/Conditionals.hs b/src/QuickSpec/Internal/Explore/Conditionals.hs
--- a/src/QuickSpec/Internal/Explore/Conditionals.hs
+++ b/src/QuickSpec/Internal/Explore/Conditionals.hs
@@ -30,34 +30,22 @@
   deriving (Functor, Applicative, Monad, MonadIO, MonadTester testcase term, MonadTerminal)
 instance MonadTrans Conditionals where
   lift = Conditionals
-instance (Typed fun, Ord fun, PrettyTerm fun, Ord norm, MonadPruner (Term (WithConstructor fun)) norm m, Predicate fun, MonadTerminal m) =>
+instance (Typed fun, Ord fun, PrettyTerm fun, Ord norm, MonadPruner (Term fun) norm m, Predicate fun, MonadTerminal m) =>
   MonadPruner (Term fun) norm (Conditionals m) where
-  normaliser = lift $ do
-    norm <- normaliser
-    return (norm . fmap Normal)
-  add prop = do
-    redundant <- conditionallyRedundant prop
-    if redundant then return False else do
-      res <- lift (add (Prop.mapFun Normal prop))
-      considerConditionalising prop
-      return res
-
-  decodeNormalForm hole t = lift $ do
-    t <- decodeNormalForm (fmap (fmap Normal) . hole) t
-    let f (Normal x) = Just x
-        f _ = Nothing
-    return $ t >>= sequence . Term.mapFun f
+  normaliser = lift normaliser
+  add = lift . add . conditionalise
+  decodeNormalForm hole t = lift (decodeNormalForm hole t)
 
 conditionalsUniverse :: (Typed fun, Predicate fun) => [Type] -> [fun] -> Universe
 conditionalsUniverse tys funs =
   universe $
     tys ++
-    (map typ $
-      map Normal funs ++
-      [ Constructor pred clas_test_case | pred <- funs, Predicate{..} <- [classify pred] ])
+    (map typ funs)
+      -- map Normal funs) -- ++
+      -- [ Constructor pred clas_test_case | pred <- funs, Predicate{..} <- [classify pred] ])
 
 runConditionals ::
-  (PrettyTerm fun, Ord norm, MonadPruner (Term (WithConstructor fun)) norm m, Predicate fun, MonadTerminal m) =>
+  (PrettyTerm fun, Ord norm, MonadPruner (Term fun) norm m, Predicate fun, MonadTerminal m) =>
   [fun] -> Conditionals m a -> m a
 runConditionals preds mx =
   run (mapM_ considerPredicate preds >> mx)
@@ -73,42 +61,19 @@
   | Function
   deriving (Eq, Ord, Functor)
 
+{-
 data WithConstructor fun =
     Constructor fun Type
   | Normal fun
   deriving (Eq, Ord)
-
-instance Sized fun => Sized (WithConstructor fun) where
-  size Constructor{} = 0
-  size (Normal f) = size f
-
-instance Pretty fun => Pretty (WithConstructor fun) where
-  pPrintPrec l p (Constructor f _) = pPrintPrec l p f <#> text "_con"
-  pPrintPrec l p (Normal f) = pPrintPrec l p f
-
-instance PrettyTerm fun => PrettyTerm (WithConstructor fun) where
-  termStyle (Constructor _ _) = curried
-  termStyle (Normal f) = termStyle f
-
-instance (Predicate fun, Background fun) => Background (WithConstructor fun) where
-  background (Normal f) = map (Prop.mapFun Normal) (background f)
-  background _ = []
-
-instance Typed fun => Typed (WithConstructor fun) where
-  typ (Constructor pred ty) =
-    arrowType (typeArgs (typ pred)) ty
-  typ (Normal f) = typ f
-  otherTypesDL (Constructor pred _) = typesDL pred
-  otherTypesDL (Normal f) = otherTypesDL f
-  typeSubst_ sub (Constructor pred ty) = Constructor (typeSubst_ sub pred) (typeSubst_ sub ty)
-  typeSubst_ sub (Normal f) = Normal (typeSubst_ sub f)
+-}
 
 predType :: TyCon -> [Type] -> Type
 predType name tys =
-  Twee.build (Twee.app (Twee.fun name) tys)
+  Twee.build (Twee.app (Twee.Sym name) tys)
 
 considerPredicate ::
-  (PrettyTerm fun, Ord norm, MonadPruner (Term (WithConstructor fun)) norm m, Predicate fun, MonadTerminal m) =>
+  (PrettyTerm fun, Ord norm, MonadPruner (Term fun) norm m, Predicate fun, MonadTerminal m) =>
   fun -> Conditionals m ()
 considerPredicate f =
   case classify f of
@@ -116,75 +81,14 @@
       let
         x = Var (V ty 0)
         eqns =
-          [Fun (Constructor f ty) :@: [Fun (Normal sel) :$: x | sel <- sels] === x,
-           Fun (Normal f) :@: [Fun (Normal sel) :$: x | sel <- sels] === fmap Normal true]
+          [Fun f :@: [Fun sel :$: x | sel <- sels] === true]
       mapM_ (lift . add) eqns
     _ -> return ()
 
 considerConditionalising ::
-  (Typed fun, Ord fun, PrettyTerm fun, Ord norm, MonadPruner (Term (WithConstructor fun)) norm m, Predicate fun, MonadTerminal m) =>
+  (Typed fun, Ord fun, PrettyTerm fun, Ord norm, MonadPruner (Term fun) norm m, Predicate fun, MonadTerminal m) =>
   Prop (Term fun) -> Conditionals m ()
-considerConditionalising (lhs :=>: t :=: u) = do
-  norm <- normaliser
-  -- If we have discovered that "somePredicate x_1 x_2 ... x_n = True"
-  -- we should add the axiom "get_x_n (toSomePredicate x_1 x_2 ... x_n) = x_n"
-  -- to the set of known equations
-  case t of
-    Fun f :@: ts | Predicate{..} <- classify f -> -- It is an interesting predicate, i.e. it was added by the user
-      when (norm u == norm clas_true) $
-        addPredicate lhs f ts
-    _ -> return ()
-
-conditionallyRedundant ::
-  (Typed fun, Ord fun, PrettyTerm fun, Ord norm, MonadPruner (Term (WithConstructor fun)) norm m, Predicate fun, MonadTerminal m) =>
-  Prop (Term fun) -> Conditionals m Bool
-conditionallyRedundant (lhs :=>: t :=: u) = do
-  t' <- normalise t
-  u' <- normalise u
-  conditionallyRedundant' lhs t u t' u'
-
-conditionallyRedundant' ::
-  (Typed fun, Ord fun, PrettyTerm fun, Ord norm, MonadPruner (Term (WithConstructor fun)) norm m, Predicate fun, MonadTerminal m) =>
-  [Equation (Term fun)] -> Term fun -> Term fun -> norm -> norm -> Conditionals m Bool
-conditionallyRedundant' lhs t u t' u' = do
-  forM_ (usort (funs [t, u])) $ \f ->
-    case classify f of
-      Selector{..} -> do
-        let
-          Predicate{..} = classify clas_pred
-          tys = typeArgs (typ clas_pred)
-          argss = sequence [ [ arg | arg <- terms [t, u] >>= subterms, typ arg == ty ] | ty <- tys ]
-        forM_ argss $ \args -> do
-          norm <- normaliser
-          let p = Fun clas_pred :@: args
-          when (norm p == norm clas_true) $ do
-            addPredicate lhs clas_pred args
-      _ -> return ()
-
-  t'' <- normalise t
-  u'' <- normalise u
-  if t'' == u'' then
-    return True
-   else if t'' == t' && u'' == u' then
-     return False
-    else
-     conditionallyRedundant' lhs t u t'' u''
-
-addPredicate ::
-  (PrettyTerm fun, Ord norm, MonadPruner (Term (WithConstructor fun)) norm m, Predicate fun, MonadTerminal m) =>
-  [Equation (Term fun)] -> fun -> [Term fun] -> Conditionals m ()
-addPredicate lhs f ts = do
-  let Predicate{..} = classify f
-      ts' = map (fmap Normal) ts
-      lhs' = map (fmap (fmap Normal)) lhs
-      -- The "to_p x1 x2 ... xm" term
-      construction = Fun (Constructor f clas_test_case) :@: ts'
-      -- The "p_n (to_p x1 x2 ... xn ... xm) = xn"
-      -- equations
-      equations = [ lhs' :=>: Fun (Normal (clas_selectors !! i)) :$: construction :=: x | (x, i) <- zip ts' [0..]]
-
-  -- Declare the relevant equations as axioms
-  mapM_ (lift . add) equations
+considerConditionalising (lhs :=>: t :=: u) = return ()
 
 conditionalise :: (PrettyTerm fun, Typed fun, Ord fun, Predicate fun) => Prop (Term fun) -> Prop (Term fun)
 conditionalise (lhs :=>: t :=: u) =
@@ -212,3 +116,4 @@
 
     replaceMany subs t =
       foldr (uncurry replace) t subs
+
diff --git a/src/QuickSpec/Internal/Explore/Polymorphic.hs b/src/QuickSpec/Internal/Explore/Polymorphic.hs
--- a/src/QuickSpec/Internal/Explore/Polymorphic.hs
+++ b/src/QuickSpec/Internal/Explore/Polymorphic.hs
@@ -173,7 +173,7 @@
 
     genType = Twee.build . aux 0 . Twee.singleton
       where
-        aux !_ Twee.Empty = mempty
+        aux !_ Twee.Nil = mempty
         aux n (Twee.Cons (Twee.Var _) ts) =
           Twee.var (Twee.V n) `mappend` aux (n+1) ts
         aux n (Twee.Cons (Twee.App f ts) us) =
diff --git a/src/QuickSpec/Internal/Explore/Schemas.hs b/src/QuickSpec/Internal/Explore/Schemas.hs
--- a/src/QuickSpec/Internal/Explore/Schemas.hs
+++ b/src/QuickSpec/Internal/Explore/Schemas.hs
@@ -22,7 +22,7 @@
 import Data.Set(Set)
 import Data.Maybe
 import Control.Monad
-import Data.Label
+import Data.Intern
 
 -- | Constrains how variables of a particular type may occur in a term.
 data VariableUse =
@@ -157,7 +157,7 @@
   -- the same number and different but unifiable types, then a type substitution
   -- can turn them into the same variable.)
   where
-    m = fromIntegral (labelNum (label (ty, n)))
+    m = fromIntegral (symId (intern (ty, n)))
 
 -- | Instantiate a schema by making all the variables different.
 mostGeneral :: (Type -> VariableUse) -> Term f -> Term f
diff --git a/src/QuickSpec/Internal/Haskell.hs b/src/QuickSpec/Internal/Haskell.hs
--- a/src/QuickSpec/Internal/Haskell.hs
+++ b/src/QuickSpec/Internal/Haskell.hs
@@ -65,6 +65,12 @@
 import qualified Data.Map.Strict as Map
 import Test.QuickCheck.Gen
 import Test.QuickCheck.Random
+import Data.IORef
+import Control.Monad.IO.Class
+import Control.Exception
+import QuickSpec.Internal.Parse
+import Text.ParserCombinators.ReadP(ReadP, string)
+import Data.Hashable
 
 baseInstances :: Instances
 baseInstances =
@@ -403,6 +409,10 @@
     comparing $ \con ->
       (typeArity (typ con), typ con, con_name con)
 
+instance Hashable Constant where
+  hashWithSalt s con =
+    s `hashWithSalt` con_name con `hashWithSalt` typ (con_value con)
+
 instance Background Constant
 
 con :: Typeable a => String -> a -> Constant
@@ -479,6 +489,9 @@
 instance Sized Constant where
   size = con_size
 
+instance FuncSized Constant where
+  sizeApp f ts = size f + sum ts
+
 instance Predicate Constant where
   classify = con_classify
 
@@ -617,6 +630,7 @@
     cfg_quickCheck :: QuickCheck.Config,
     cfg_twee :: Twee.Config,
     cfg_max_size :: Int,
+    cfg_max_depth :: Int,
     cfg_max_commutative_size :: Int,
     cfg_max_functions :: Int,
     cfg_instances :: Instances,
@@ -627,14 +641,17 @@
     cfg_default_to :: Type,
     cfg_infer_instance_types :: Bool,
     cfg_background :: [Prop (Term Constant)],
+    cfg_background_str :: [String],
     cfg_print_filter :: Prop (Term Constant) -> Bool,
     cfg_print_style :: PrintStyle,
-    cfg_check_consistency :: Bool
+    cfg_check_consistency :: Bool,
+    cfg_handle_resource_limit :: Bool
     }
 
 lens_quickCheck = lens cfg_quickCheck (\x y -> y { cfg_quickCheck = x })
 lens_twee = lens cfg_twee (\x y -> y { cfg_twee = x })
 lens_max_size = lens cfg_max_size (\x y -> y { cfg_max_size = x })
+lens_max_depth = lens cfg_max_depth (\x y -> y { cfg_max_depth = x })
 lens_max_commutative_size = lens cfg_max_commutative_size (\x y -> y { cfg_max_commutative_size = x })
 lens_max_functions = lens cfg_max_functions (\x y -> y { cfg_max_functions = x })
 lens_instances = lens cfg_instances (\x y -> y { cfg_instances = x })
@@ -642,9 +659,11 @@
 lens_default_to = lens cfg_default_to (\x y -> y { cfg_default_to = x })
 lens_infer_instance_types = lens cfg_infer_instance_types (\x y -> y { cfg_infer_instance_types = x })
 lens_background = lens cfg_background (\x y -> y { cfg_background = x })
+lens_background_str = lens cfg_background_str (\x y -> y { cfg_background_str = x })
 lens_print_filter = lens cfg_print_filter (\x y -> y { cfg_print_filter = x })
 lens_print_style = lens cfg_print_style (\x y -> y { cfg_print_style = x })
 lens_check_consistency = lens cfg_check_consistency (\x y -> y { cfg_check_consistency = x })
+lens_handle_resource_limit = lens cfg_handle_resource_limit (\x y -> y { cfg_handle_resource_limit = x })
 
 defaultConfig :: Config
 defaultConfig =
@@ -652,6 +671,7 @@
     cfg_quickCheck = QuickCheck.Config { QuickCheck.cfg_num_tests = 1000, QuickCheck.cfg_max_test_size = 100, QuickCheck.cfg_fixed_seed = Nothing },
     cfg_twee = Twee.Config { Twee.cfg_max_term_size = minBound, Twee.cfg_max_cp_depth = maxBound },
     cfg_max_size = 7,
+    cfg_max_depth = maxBound,
     cfg_max_commutative_size = 5,
     cfg_max_functions = maxBound,
     cfg_instances = mempty,
@@ -659,9 +679,11 @@
     cfg_default_to = typeRep (Proxy :: Proxy Int),
     cfg_infer_instance_types = False,
     cfg_background = [],
+    cfg_background_str = [],
     cfg_print_filter = \_ -> True,
     cfg_print_style = ForHumans,
-    cfg_check_consistency = False }
+    cfg_check_consistency = False,
+    cfg_handle_resource_limit = False }
 
 -- Extra types for the universe that come from in-scope instances.
 instanceTypes :: Instances -> Config -> [Type]
@@ -682,10 +704,10 @@
     groundInstances =
       [ dict
       | -- () :- dict
-        Twee.App tc (Twee.Cons (Twee.App unit Twee.Empty) (Twee.Cons dict Twee.Empty)) <-
+        Twee.App (Twee.Sym tc) (Twee.Cons (Twee.App (Twee.Sym unit) Twee.Nil) (Twee.Cons dict Twee.Nil)) <-
         map (typeRes . typ) (is_instances insts),
-        Twee.fun_value tc == tyCon (Proxy :: Proxy (:-)),
-        Twee.fun_value unit == tyCon (Proxy :: Proxy (() :: Constraint)),
+        tc == tyCon (Proxy :: Proxy (:-)),
+        unit == tyCon (Proxy :: Proxy (() :: Constraint)),
         Twee.isGround dict ]
 
 data Warnings =
@@ -731,6 +753,9 @@
 
 quickSpec :: Config -> IO [Prop (Term Constant)]
 quickSpec cfg@Config{..} = do
+  propNo <- newIORef 1
+  props <- newIORef ([] :: [Prop (Term Constant)])
+
   let
     constantsOf f =
       usort (concatMap funs $
@@ -752,8 +777,8 @@
       norm <- normaliser
       let prop' = prettierProp funs norm prop
       when (not (hasBackgroundPredicates prop') && not (isBackgroundProp prop') && cfg_print_filter prop) $ do
-        (n :: Int, props) <- get
-        put (n+1, props)
+        n <- liftIO $ readIORef propNo
+        liftIO $ writeIORef propNo (n+1)
         putLine $
           case cfg_print_style of
             ForHumans ->
@@ -795,6 +820,7 @@
       sortTerms measure $
       filterEnumerator (all constraintsOk . funs) $
       filterEnumerator (\t -> length (usort (funs t)) <= cfg_max_functions) $
+      filterEnumerator (\t -> depth t <= cfg_max_depth) $
       filterEnumerator (\t -> size t + length (conditions t) <= cfg_max_size) $
       enumerateConstants atomic `mappend` enumerateApplications
       where
@@ -819,7 +845,7 @@
           putLine "quickspec_laws ="
       let
         pres prop = do
-          modify $ \(k, props) -> (k, prop:props)
+          liftIO $ modifyIORef props (prop:)
           if n == 0 then return () else present (constantsOf f) prop
       QuickSpec.Internal.Explore.quickSpec pres (flip eval) cfg_max_size cfg_max_commutative_size use univ
         (enumerator (map Fun (constantsOf g)))
@@ -830,11 +856,18 @@
     main = do
       forM_ cfg_background $ \prop -> do
         add prop
+      forM_ cfg_background_str $ \prop_str -> do
+        add (parseProp parseFun prop_str)
+
       mapM_ round [0..rounds-1]
       where
         round n = mainOf n (concat . take 1 . drop n) (concat . take (n+1))
         rounds = length cfg_constants
 
+    -- Used in adding background functions from strings
+    parseFun :: ReadP Constant
+    parseFun = msum [do { string (con_name c); return c } | c <- constants ]
+
     -- Used in checkConsistency. Generate a term to be used when a
     -- Twee proof contains a hole ("?"), i.e. a don't-care variable.
     hole ty = do
@@ -877,12 +910,22 @@
           putLine (printf "  %s is false" (prettyShow (prettiestProp constants norm inst)))
         putLine ""
 
-  join $
-    fmap withStdioTerminal $
-    generate $
-    QuickCheck.run cfg_quickCheck (arbitraryTestCase cfg_default_to instances) eval $
-    Twee.run cfg_twee { Twee.cfg_max_term_size = Twee.cfg_max_term_size cfg_twee `max` cfg_max_size } $
-    runConditionals constants $ do
-      result <- fmap (reverse . snd) $ flip execStateT (1, []) main
-      when cfg_check_consistency $ void $ execStateT checkConsistency Map.empty
-      return result
+  handleJust (\ex -> if cfg_handle_resource_limit && isResourceLimitException ex then Just () else Nothing) return $
+    join $
+      fmap withStdioTerminal $
+      generate $
+      QuickCheck.run cfg_quickCheck (arbitraryTestCase cfg_default_to instances) eval $
+      Twee.run cfg_twee { Twee.cfg_max_term_size = Twee.cfg_max_term_size cfg_twee `max` cfg_max_size } $
+      runConditionals constants $ do
+        main
+        when cfg_check_consistency $ void $ execStateT checkConsistency Map.empty
+
+  let maybeConditionalise prop
+        | prop == prop' = [prop]
+        | otherwise = [prop, prop']
+        where prop' = conditionalise prop
+
+  -- Return conditional properties both in conditionalised and raw form.
+  -- Raw form is needed if the properties will be passed to addBackground,
+  -- but conditionalised is better for other uses.
+  concatMap maybeConditionalise . reverse <$> readIORef props
diff --git a/src/QuickSpec/Internal/Haskell/Resolve.hs b/src/QuickSpec/Internal/Haskell/Resolve.hs
--- a/src/QuickSpec/Internal/Haskell/Resolve.hs
+++ b/src/QuickSpec/Internal/Haskell/Resolve.hs
@@ -61,9 +61,9 @@
       -- (see comment about is_instances).
       case typ x of
         -- A function of type a -> (b -> c) gets uncurried.
-        App (F _ Arrow) (Cons _ (Cons (App (F _ Arrow) _) Empty)) ->
+        App (Sym Arrow) (Cons _ (Cons (App (Sym Arrow) _) Nil)) ->
           polyInst (apply uncur x)
-        App (F _ Arrow) _ ->
+        App (Sym Arrow) _ ->
           makeInstances [x]
         -- A plain old value x (not a function) turns into \() -> x.
         _ ->
@@ -94,10 +94,10 @@
 --
 -- Invariant: the type of the returned value is an instance of the argument type.
 find_ :: Instances -> Type -> [Value Identity]
-find_ _ (App (F _ unit) Empty)
+find_ _ (App (Sym unit) Nil)
   | unit == tyCon (Proxy :: Proxy ()) =
     return (toValue (Identity ()))
-find_ insts (App (F _ pair) (Cons ty1 (Cons ty2 Empty)))
+find_ insts (App (Sym pair) (Cons ty1 (Cons ty2 Nil)))
   | pair == tyCon (Proxy :: Proxy (,)) = do
     x <- is_find insts ty1
     sub <- maybeToList (match ty1 (typ x))
@@ -109,7 +109,7 @@
   -- Find a function whose result type unifies with ty.
   -- Rename it to avoid clashes with ty.
   fun <- fmap (polyRename ty) (is_instances insts)
-  App (F _ Arrow) (Cons arg (Cons res Empty)) <- return (typ fun)
+  App (Sym Arrow) (Cons arg (Cons res Nil)) <- return (typ fun)
   sub <- maybeToList (unify ty res)
   fun <- return (typeSubst sub fun)
   arg <- return (typeSubst sub arg)
diff --git a/src/QuickSpec/Internal/Parse.hs b/src/QuickSpec/Internal/Parse.hs
--- a/src/QuickSpec/Internal/Parse.hs
+++ b/src/QuickSpec/Internal/Parse.hs
@@ -9,7 +9,7 @@
 import QuickSpec.Internal.Prop
 import QuickSpec.Internal.Term hiding (char)
 import QuickSpec.Internal.Type
-import qualified Data.Label as Label
+import qualified Data.Intern as Intern
 import Text.ParserCombinators.ReadP
 
 class Parse fun a where
@@ -20,8 +20,8 @@
     x <- satisfy isUpper
     xs <- munch isAlphaNum
     let name = x:xs
-    -- Use Data.Label as an easy way to generate a variable number
-    return (V typeVar (fromIntegral (Label.labelNum (Label.label name))))
+    -- Use Data.Intern as an easy way to generate a variable number
+    return (V typeVar (fromIntegral (Intern.symId (Intern.intern name))))
 
 instance (fun1 ~ fun, Apply (Term fun)) => Parse fun1 (Term fun) where
   parse pfun =
diff --git a/src/QuickSpec/Internal/Prop.hs b/src/QuickSpec/Internal/Prop.hs
--- a/src/QuickSpec/Internal/Prop.hs
+++ b/src/QuickSpec/Internal/Prop.hs
@@ -48,6 +48,14 @@
   where
     both f (t :=: u) = f t :=: f u
 
+mapTermM :: Monad m => (Term fun1 -> m (Term fun2)) -> Prop (Term fun1) -> m (Prop (Term fun2))
+mapTermM f (lhs :=>: rhs) = do
+  lhs <- mapM (both f) lhs
+  rhs <- both f rhs
+  return (lhs :=>: rhs)
+  where
+    both f (t :=: u) = liftM2 (:=:) (f t) (f u)
+
 instance Typed a => Typed (Prop a) where
   typ _ = typeOf True
   otherTypesDL p = DList.fromList (literals p) >>= typesDL
diff --git a/src/QuickSpec/Internal/Pruning/Conditionals.hs b/src/QuickSpec/Internal/Pruning/Conditionals.hs
new file mode 100644
--- /dev/null
+++ b/src/QuickSpec/Internal/Pruning/Conditionals.hs
@@ -0,0 +1,102 @@
+-- Encode conditionals during pruning.
+{-# OPTIONS_HADDOCK hide #-}
+{-# LANGUAGE FlexibleInstances, GeneralizedNewtypeDeriving, MultiParamTypeClasses, FlexibleContexts, ScopedTypeVariables, UndecidableInstances, DeriveGeneric #-}
+module QuickSpec.Internal.Pruning.Conditionals where
+
+import QuickSpec.Internal.Pruning
+import QuickSpec.Internal.Pruning.Background(Background(..))
+import QuickSpec.Internal.Testing
+import QuickSpec.Internal.Term
+import QuickSpec.Internal.Type
+import QuickSpec.Internal.Prop hiding (mapFun)
+import QuickSpec.Internal.Terminal
+import QuickSpec.Internal.Utils
+import Control.Monad.IO.Class
+import Control.Monad.Trans.Class
+import GHC.Generics
+import Data.Hashable
+import Data.Hashable.Generic
+
+data Conditionals fun =
+    Func fun
+  | Guard Type (UnconditionalTerm fun) (UnconditionalTerm fun) (UnconditionalTerm fun) (UnconditionalTerm fun) [Var]
+  deriving (Eq, Ord, Show, Typeable, Generic)
+
+instance Hashable fun => Hashable (Conditionals fun) where
+  hashWithSalt = genericHashWithSalt
+
+instance Arity fun => Arity (Conditionals fun) where
+  arity (Func f) = arity f
+  arity (Guard _ _ _ _ _ vs) = length vs + 1
+
+instance Sized fun => Sized (Conditionals fun) where
+  size (Func f) = size f
+  size Guard{} = 0
+
+instance Sized fun => FuncSized (Conditionals fun) where
+  -- Note: since there is no FuncSized instance for PartiallyApplied
+  -- we just assume that Func f is adding the size of its arguments
+  sizeApp (Func f) ts = size f + sum ts
+  sizeApp Guard{} ts = penalty + maximum ts
+    where
+      penalty = 3
+
+instance Pretty fun => Pretty (Conditionals fun) where
+  pPrint (Func f) = pPrint f
+  pPrint Guard{} = text "guard"
+
+instance PrettyTerm fun => PrettyTerm (Conditionals fun) where
+  termStyle (Func f) = termStyle f
+  termStyle Guard{} = uncurried
+
+instance Typed fun => Typed (Conditionals fun) where
+  typ (Func f) = typ f
+  typ (Guard ty t _ _ _ vs) = arrowType (typ t:map typ vs) ty
+
+  typeSubst_ sub (Func f) = Func (typeSubst_ sub f)
+  typeSubst_ sub (Guard ty t u v w vs) = Guard (typeSubst_ sub ty) (typeSubst_ sub t) (typeSubst_ sub u) (typeSubst_ sub v) (typeSubst_ sub w) (typeSubst_ sub vs)
+
+instance EqualsBonus (Conditionals fun) where
+
+type ConditionalTerm fun = Term fun
+type UnconditionalTerm fun = Term (Conditionals fun)
+
+newtype Pruner fun pruner a =
+  Pruner { run :: pruner a }
+  deriving (Functor, Applicative, Monad, MonadIO, MonadTester testcase term, MonadTerminal)
+
+instance MonadTrans (Pruner fun) where
+  lift = Pruner
+
+instance (PrettyTerm fun, Typed fun, MonadPruner (UnconditionalTerm fun) norm pruner) => MonadPruner (ConditionalTerm fun) norm (Pruner fun pruner) where
+  normaliser =
+    Pruner $ do
+      norm <- normaliser :: pruner (UnconditionalTerm fun -> norm)
+
+      return $ \t ->
+        norm . mapFun Func $ t
+
+  add prop = and <$> lift (mapM add (conditionalise' (canonicalise prop)))
+
+  decodeNormalForm hole t =
+    Pruner $ do
+      t <- decodeNormalForm (fmap (fmap Func) . hole) t
+      let elimIfEq (Func f) = Just f
+          elimIfEq Guard{} = Nothing
+      return $ t >>= mapFunM elimIfEq
+
+instance (Typed fun, Arity fun, Background fun) => Background (Conditionals fun) where
+  background (Func f) = concatMap conditionalise' (background f)
+  background Guard{} = []
+
+conditionalise :: Typed fun => Prop (UnconditionalTerm fun) -> [Prop (UnconditionalTerm fun)]
+conditionalise prop@([] :=>: _) = [prop]
+conditionalise ((t :=: u):lhs :=>: v :=: w) =
+  ([] :=>: guarded t v):conditionalise (lhs :=>: guarded u w)
+  where
+    guarded x y = Fun (Guard ty t u v w vs) :@: (x:map Var vs) :=: y
+    vs = usort (concatMap vars [t, u, v, w])
+    ty = typ t
+
+conditionalise' :: Typed fun => Prop (ConditionalTerm fun) -> [Prop (UnconditionalTerm fun)]
+conditionalise' = conditionalise . mapTerm (mapFun Func)
diff --git a/src/QuickSpec/Internal/Pruning/PartialApplication.hs b/src/QuickSpec/Internal/Pruning/PartialApplication.hs
--- a/src/QuickSpec/Internal/Pruning/PartialApplication.hs
+++ b/src/QuickSpec/Internal/Pruning/PartialApplication.hs
@@ -1,6 +1,6 @@
 -- Pruning support for partial application and the like.
 {-# OPTIONS_HADDOCK hide #-}
-{-# LANGUAGE FlexibleInstances, TypeSynonymInstances, RecordWildCards, MultiParamTypeClasses, FlexibleContexts, GeneralizedNewtypeDeriving, UndecidableInstances, DeriveFunctor #-}
+{-# LANGUAGE FlexibleInstances, TypeSynonymInstances, RecordWildCards, MultiParamTypeClasses, FlexibleContexts, GeneralizedNewtypeDeriving, UndecidableInstances, DeriveFunctor, DeriveGeneric #-}
 module QuickSpec.Internal.Pruning.PartialApplication where
 
 import QuickSpec.Internal.Term as Term
@@ -12,6 +12,9 @@
 import QuickSpec.Internal.Testing
 import Control.Monad.IO.Class
 import Control.Monad.Trans.Class
+import GHC.Generics
+import Data.Hashable
+import Data.Hashable.Generic
 
 data PartiallyApplied f =
     -- A partially-applied function symbol.
@@ -20,7 +23,10 @@
     -- The ($) operator, for oversaturated applications.
     -- The type argument is the type of the first argument to ($).
   | Apply Type
-  deriving (Eq, Ord, Functor)
+  deriving (Eq, Ord, Functor, Generic)
+
+instance Hashable f => Hashable (PartiallyApplied f) where
+  hashWithSalt = genericHashWithSalt
 
 instance Sized f => Sized (PartiallyApplied f) where
   size (Partial f _) = size f
diff --git a/src/QuickSpec/Internal/Pruning/Twee.hs b/src/QuickSpec/Internal/Pruning/Twee.hs
--- a/src/QuickSpec/Internal/Pruning/Twee.hs
+++ b/src/QuickSpec/Internal/Pruning/Twee.hs
@@ -15,17 +15,19 @@
 import Control.Monad.Trans.Class
 import Control.Monad.IO.Class
 import qualified QuickSpec.Internal.Pruning.UntypedTwee as Untyped
+import qualified QuickSpec.Internal.Pruning.Conditionals as Conditionals
+import QuickSpec.Internal.Pruning.Conditionals(Conditionals)
 import QuickSpec.Internal.Pruning.UntypedTwee(Config(..))
-import Data.Typeable
+import Data.Intern
 
 newtype Pruner fun m a =
-  Pruner (PartialApplication.Pruner fun (Types.Pruner (PartiallyApplied fun) (Background.Pruner (Tagged (PartiallyApplied fun)) (Untyped.Pruner (Tagged (PartiallyApplied fun)) m))) a)
+  Pruner (PartialApplication.Pruner fun (Conditionals.Pruner (PartiallyApplied fun) (Types.Pruner (Conditionals (PartiallyApplied fun)) (Background.Pruner (Tagged (Conditionals (PartiallyApplied fun))) (Untyped.Pruner (Tagged (Conditionals (PartiallyApplied fun))) m)))) a)
   deriving (Functor, Applicative, Monad, MonadIO, MonadTester testcase term,
-            MonadPruner (Term fun) (Untyped.Norm (Tagged (PartiallyApplied fun))), MonadTerminal)
+            MonadPruner (Term fun) (Untyped.Norm (Tagged (Conditionals (PartiallyApplied fun)))), MonadTerminal)
 
 instance MonadTrans (Pruner fun) where
-  lift = Pruner . lift . lift . lift . lift
+  lift = Pruner . lift . lift . lift . lift . lift
 
-run :: (Sized fun, Typeable fun, Ord fun, Monad m) => Config -> Pruner fun m a -> m a
+run :: (Sized fun, Intern fun, Ord fun, PrettyTerm fun, Monad m) => Config -> Pruner fun m a -> m a
 run config (Pruner x) =
-  Untyped.run config (Background.run (Types.run (PartialApplication.run x)))
+  Untyped.run config (Background.run (Types.run (Conditionals.run (PartialApplication.run x))))
diff --git a/src/QuickSpec/Internal/Pruning/Types.hs b/src/QuickSpec/Internal/Pruning/Types.hs
--- a/src/QuickSpec/Internal/Pruning/Types.hs
+++ b/src/QuickSpec/Internal/Pruning/Types.hs
@@ -1,6 +1,6 @@
 -- Encode monomorphic types during pruning.
 {-# OPTIONS_HADDOCK hide #-}
-{-# LANGUAGE FlexibleInstances, GeneralizedNewtypeDeriving, MultiParamTypeClasses, FlexibleContexts, ScopedTypeVariables, UndecidableInstances #-}
+{-# LANGUAGE FlexibleInstances, GeneralizedNewtypeDeriving, MultiParamTypeClasses, FlexibleContexts, ScopedTypeVariables, UndecidableInstances, DeriveGeneric #-}
 module QuickSpec.Internal.Pruning.Types where
 
 import QuickSpec.Internal.Pruning
@@ -12,12 +12,18 @@
 import QuickSpec.Internal.Terminal
 import Control.Monad.IO.Class
 import Control.Monad.Trans.Class
+import GHC.Generics
+import Data.Hashable
+import Data.Hashable.Generic
 
 data Tagged fun =
     Func fun
   | Tag Type
-  deriving (Eq, Ord, Show, Typeable)
+  deriving (Eq, Ord, Show, Typeable, Generic)
 
+instance Hashable fun => Hashable (Tagged fun) where
+  hashWithSalt = genericHashWithSalt
+
 instance Arity fun => Arity (Tagged fun) where
   arity (Func f) = arity f
   arity (Tag _) = 1
@@ -25,6 +31,10 @@
 instance Sized fun => Sized (Tagged fun) where
   size (Func f) = size f
   size (Tag _) = 0
+
+instance FuncSized fun => FuncSized (Tagged fun) where
+  sizeApp (Func f) ts = sizeApp f ts
+  sizeApp (Tag t) ts = sum ts
 
 instance Pretty fun => Pretty (Tagged fun) where
   pPrint (Func f) = pPrint f
diff --git a/src/QuickSpec/Internal/Pruning/UntypedTwee.hs b/src/QuickSpec/Internal/Pruning/UntypedTwee.hs
--- a/src/QuickSpec/Internal/Pruning/UntypedTwee.hs
+++ b/src/QuickSpec/Internal/Pruning/UntypedTwee.hs
@@ -1,6 +1,6 @@
 -- A pruner that uses twee. Does not respect types.
 {-# OPTIONS_HADDOCK hide #-}
-{-# LANGUAGE RecordWildCards, FlexibleContexts, FlexibleInstances, GADTs, PatternSynonyms, GeneralizedNewtypeDeriving, MultiParamTypeClasses, UndecidableInstances #-}
+{-# LANGUAGE RecordWildCards, FlexibleContexts, FlexibleInstances, GADTs, PatternSynonyms, GeneralizedNewtypeDeriving, MultiParamTypeClasses, UndecidableInstances, DeriveGeneric #-}
 module QuickSpec.Internal.Pruning.UntypedTwee where
 
 import QuickSpec.Internal.Testing
@@ -16,7 +16,7 @@
 import Twee hiding (Config(..))
 import Twee.Rule hiding (normalForms)
 import Twee.Proof hiding (Config, defaultConfig)
-import Twee.Base(Ordered(..), Labelled)
+import Twee.Base(Ordered(..))
 import Control.Monad.Trans.Reader
 import Control.Monad.Trans.State.Strict hiding (State)
 import Control.Monad.Trans.Class
@@ -27,6 +27,9 @@
 import qualified Data.Map.Strict as Map
 import qualified Data.IntMap as IntMap
 import Control.Monad
+import GHC.Generics
+import Data.Hashable
+import Data.Hashable.Generic
 
 data Config =
   Config {
@@ -37,37 +40,42 @@
 lens_max_cp_depth = lens cfg_max_cp_depth (\x y -> y { cfg_max_cp_depth = x })
 
 data Extended fun = Minimal | Skolem Twee.Var | Function fun
-  deriving (Eq, Ord, Typeable)
+  deriving (Eq, Ord, Typeable, Generic)
 
-instance (Ord fun, Typeable fun) => Labelled (Extended fun)
+instance Hashable fun => Hashable (Extended fun) where
+  hashWithSalt = genericHashWithSalt
 
 instance Sized fun => Sized (Extended fun) where
   size (Function f) = size f
   size _ = 1
+  --sizeMode (Function f) = sizeMode f
+  --sizeMode _ = AddArgs
 
+instance FuncSized fun => FuncSized (Extended fun) where
+  sizeApp (Function f) ts = sizeApp f ts
+  sizeApp _ [] = 1
+
+instance Twee.Weighted (Extended fun)
+instance KBO.ArgWeighted fun where
+  argWeight _ = 1
 instance KBO.Sized (Extended fun) where
   size _ = 1
 
-instance Arity fun => Arity (Extended fun) where
-  arity (Function f) = arity f
-  arity (Skolem _) = 0
-  arity Minimal = 0
-
-instance (Ord fun, Typeable fun) => Twee.Minimal (Extended fun) where
-  minimal = Twee.fun Minimal
+instance Twee.Intern fun => Twee.Minimal (Extended fun) where
+  minimal = Twee.Sym Minimal
+  skolem = Twee.Sym . Skolem . Twee.V
 
 instance EqualsBonus (Extended fun)
-
-instance (Ord fun, Typeable fun, Pretty fun) => Pretty (Extended fun) where
+instance (Twee.Intern fun, Pretty fun) => Pretty (Extended fun) where
   pPrintPrec l p (Function f) = pPrintPrec l p f
   pPrintPrec _ _ Minimal = text "?"
   pPrintPrec _ _ (Skolem (Twee.V x)) = text ("sk" ++ show x)
 
-instance (Ord fun, Typeable fun, PrettyTerm fun) => PrettyTerm (Extended fun) where
+instance (Twee.Intern fun, PrettyTerm fun) => PrettyTerm (Extended fun) where
   termStyle (Function f) = termStyle f
   termStyle _ = curried
 
-instance (Sized fun, Pretty fun, PrettyTerm fun, Ord fun, Typeable fun, Arity fun, EqualsBonus fun) => Ordered (Extended fun) where
+instance (Ord fun, Pretty fun, PrettyTerm fun, Twee.Intern fun) => Ordered (Extended fun) where
   lessEq = KBO.lessEq
   lessIn = KBO.lessIn
   lessEqSkolem = KBO.lessEqSkolem
@@ -79,26 +87,23 @@
 instance MonadTrans (Pruner fun) where
   lift = Pruner . lift . lift
 
-run :: (Typeable fun, Ord fun, Sized fun, Monad m) => Config -> Pruner fun m a -> m a
+run :: (Twee.Intern fun, Ord fun, PrettyTerm fun, FuncSized fun, Monad m) => Config -> Pruner fun m a -> m a
 run Config{..} (Pruner x) =
   evalStateT (runReaderT x config) (initialState config)
   where
     config =
       defaultConfig {
-        Twee.cfg_accept_term = Just (\t -> size t <= cfg_max_term_size),
+        Twee.cfg_accept_term = Just (\t -> termSize t <= cfg_max_term_size),
         Twee.cfg_max_cp_depth = cfg_max_cp_depth }
 
-instance (Labelled fun, Sized fun) => Sized (Twee.Term fun) where
-  size (Twee.Var _) = 1
-  size (Twee.App f ts) =
-    size (Twee.fun_value f) + sum (map size (Twee.unpack ts))
-
-instance KBO.Weighted (Extended fun) where
-  argWeight _ = 1
+termSize :: (Twee.Intern fun, FuncSized fun) => Twee.Term fun -> Int
+termSize (Twee.Var _) = 1
+termSize (Twee.App (Twee.Sym f) ts) =
+  sizeApp f (map termSize (Twee.unpack ts))
 
 type Norm fun = Twee.Term (Extended fun)
 
-instance (Ord fun, Typed fun, Typeable fun, Arity fun, PrettyTerm fun, EqualsBonus fun, Sized fun, Monad m) =>
+instance (Ord fun, Typed fun, Twee.Intern fun, PrettyTerm fun, EqualsBonus fun, Sized fun, Monad m) =>
   MonadPruner (Term fun) (Norm fun) (Pruner fun m) where
   normaliser = Pruner $ do
     state <- lift get
@@ -125,11 +130,11 @@
     where
       decode (Twee.Var (Twee.V n)) ty =
         Just (Var (V ty n))
-      decode (Twee.App (Twee.F _ Minimal) Twee.Empty) ty =
+      decode (Twee.App (Twee.Sym Minimal) Twee.Nil) ty =
         hole ty
-      decode (Twee.App (Twee.F _ (Skolem (Twee.V n))) Twee.Empty) ty =
+      decode (Twee.App (Twee.Sym (Skolem (Twee.V n))) Twee.Nil) ty =
         Just (Var (V ty n))
-      decode (Twee.App (Twee.F _ (Function f)) ts) _ =
+      decode (Twee.App (Twee.Sym (Function f)) ts) _ =
         (Fun f :@:) <$> zipWithM decode (Twee.unpack ts) args
         where
           args = typeArgs (typ f)
@@ -153,19 +158,19 @@
 
     return (map toTheorem actives)
 
-normaliseTwee :: (Ord fun, Typeable fun, Arity fun, PrettyTerm fun, EqualsBonus fun, Sized fun) =>
+normaliseTwee :: (Twee.Intern fun, Ord fun, PrettyTerm fun, EqualsBonus fun, Sized fun) =>
   State (Extended fun) -> Term fun -> Norm fun
 normaliseTwee state t =
   result u (normaliseTerm state u)
   where
     u = simplifyTerm state (skolemise t)
 
-normalFormsTwee :: (Ord fun, Typeable fun, Arity fun, PrettyTerm fun, EqualsBonus fun, Sized fun) =>
+normalFormsTwee :: (Twee.Intern fun, Ord fun, PrettyTerm fun, EqualsBonus fun, Sized fun) =>
   State (Extended fun) -> Term fun -> Set (Norm fun)
 normalFormsTwee state t =
   Set.fromList . Map.elems $ Map.mapWithKey result (normalForms state (skolemise t))
 
-addTwee :: (Ord fun, Typeable fun, Arity fun, PrettyTerm fun, EqualsBonus fun, Sized fun) =>
+addTwee :: (Twee.Intern fun, Ord fun, PrettyTerm fun, EqualsBonus fun, Sized fun) =>
   Twee.Config (Extended fun) -> Term fun -> Term fun -> State (Extended fun) -> State (Extended fun)
 addTwee config t u state =
   interreduce config $
@@ -174,22 +179,22 @@
   where
     axiom = Axiom 0 (prettyShow (t :=: u)) (toTwee t Twee.:=: toTwee u)
 
-toTwee :: (Ord f, Typeable f) =>
+toTwee :: (Ord f, Twee.Intern f) =>
   Term f -> Twee.Term (Extended f)
 toTwee = Twee.build . tt
   where
     tt (Var (V _ x)) =
       Twee.var (Twee.V x)
     tt (Fun f :@: ts) =
-      Twee.app (Twee.fun (Function f)) (map tt ts)
+      Twee.app (Twee.Sym (Function f)) (map tt ts)
     tt _ = error "partially applied term"
 
-skolemise :: (Ord f, Typeable f) =>
+skolemise :: (Ord f, Twee.Intern f) =>
   Term f -> Twee.Term (Extended f)
 skolemise = Twee.build . sk
   where
     sk (Var (V _ x)) =
-      Twee.con (Twee.fun (Skolem (Twee.V x)))
+      Twee.con (Twee.Sym (Skolem (Twee.V x)))
     sk (Fun f :@: ts) =
-      Twee.app (Twee.fun (Function f)) (map sk ts)
+      Twee.app (Twee.Sym (Function f)) (map sk ts)
     sk _ = error "partially applied term"
diff --git a/src/QuickSpec/Internal/Term.hs b/src/QuickSpec/Internal/Term.hs
--- a/src/QuickSpec/Internal/Term.hs
+++ b/src/QuickSpec/Internal/Term.hs
@@ -18,15 +18,15 @@
 import Data.Map(Map)
 import Data.List
 import Data.Ord
-import Data.Maybe
+import Data.Hashable
 
 -- | A typed term.
 data Term f = Var {-# UNPACK #-} !Var | Fun !f | !(Term f) :$: !(Term f)
-  deriving (Eq, Ord, Show, Functor, Foldable, Traversable)
+  deriving (Eq, Ord, Show, Functor, Foldable, Traversable, Generic, Hashable)
 
 -- | A variable, which has a type and a number.
 data Var = V { var_ty :: !Type, var_id :: {-# UNPACK #-} !Int }
-  deriving (Eq, Ord, Show, Generic)
+  deriving (Eq, Ord, Show, Generic, Hashable)
 
 instance CoArbitrary Var where
   coarbitrary = coarbitrary . var_id
@@ -87,16 +87,16 @@
 class Sized a where
   size :: a -> Int
 
-instance Sized f => Sized (Term f) where
+class FuncSized a where
+  sizeApp :: a -> [Int] -> Int
+
+instance FuncSized f => Sized (Term f) where
   size (Var _) = 1
-  size (Fun f) = size f
-  size (t :$: u) =
-    size t + size u +
+  size (Var _ :@: ts) =
     -- Penalise applied function variables, because they can be used
     -- to build many many terms without any constants at all
-    case t of
-      Var _ -> 1
-      _ -> 0
+    2 + sum (map size ts)
+  size (Fun f :@: ts) = sizeApp f (map size ts)
 
 instance Pretty Var where
   pPrint x = parens $ text "X" <#> pPrint (var_id x+1) <+> text "::" <+> pPrint (var_ty x)
@@ -157,6 +157,12 @@
 mapFun f (t :$: u) = mapFun f t :$: mapFun f u
 
 -- | Map a function over function symbols.
+mapFunM :: Monad m => (f -> m g) -> Term f -> m (Term g)
+mapFunM _ (Var x) = return (Var x)
+mapFunM f (Fun x) = Fun <$> f x
+mapFunM f (t :$: u) = liftM2 (:$:) (mapFunM f t) (mapFunM f u)
+
+-- | Map a function over function symbols.
 flatMapFun :: (f -> Term g) -> Term f -> Term g
 flatMapFun _ (Var x) = Var x
 flatMapFun f (Fun x) = f x
@@ -251,7 +257,7 @@
 -- if measure (schema t) < measure (schema u) then t < u.
 type Measure f = (Int, Int, Int, Int, MeasureFuns f, Int, [Var])
 -- | Compute the term ordering for a term.
-measure :: (Sized f, Typed f) => Term f -> Measure f
+measure :: (FuncSized f, Typed f) => Term f -> Measure f
 measure t =
   (depth t, size t, missing t, -length (vars t), MeasureFuns (skel t),
    -length (usort (vars t)), vars t)
@@ -296,6 +302,10 @@
 instance (Sized fun1, Sized fun2) => Sized (fun1 :+: fun2) where
   size (Inl x) = size x
   size (Inr x) = size x
+
+instance (FuncSized fun1, FuncSized fun2) => FuncSized (fun1 :+: fun2) where
+  sizeApp (Inl x) = sizeApp x
+  sizeApp (Inr x) = sizeApp x
 
 instance (Typed fun1, Typed fun2) => Typed (fun1 :+: fun2) where
   typ (Inl x) = typ x
diff --git a/src/QuickSpec/Internal/Type.hs b/src/QuickSpec/Internal/Type.hs
--- a/src/QuickSpec/Internal/Type.hs
+++ b/src/QuickSpec/Internal/Type.hs
@@ -39,6 +39,8 @@
 import Data.List hiding (singleton)
 import Data.Char
 import Data.Functor.Identity
+import Data.Intern
+import Data.Hashable
 
 -- | A (possibly polymorphic) type.
 type Type = Term TyCon
@@ -54,7 +56,10 @@
   | String String
   deriving (Eq, Ord, Show, Typeable)
 
-instance Labelled TyCon
+instance Hashable TyCon where
+  hashWithSalt s Arrow = s `hashWithSalt` (0 :: Int)
+  hashWithSalt s (TyCon tc) = s `hashWithSalt` (1 :: Int) `hashWithSalt` Ty.tyConFingerprint tc
+  hashWithSalt s (String xs) = s `hashWithSalt` (2 :: Int) `hashWithSalt` xs
 
 instance Pretty TyCon where
   pPrint Arrow = text "->"
@@ -79,6 +84,8 @@
     | take 2 (show con) == "(," ||
       take 3 (show con) == "(%," =
       fixedArity (1+length (filter (== ',') (show con))) tupleStyle
+    | Just n <- Data.List.lookup con tupleTyCons =
+      fixedArity n tupleStyle
     | isAlphaNum (head (show con)) = curried
     | otherwise = infixStyle 5
 
@@ -139,7 +146,7 @@
 
 -- | Turn a `TyCon` into a type.
 typeFromTyCon :: TyCon -> Type
-typeFromTyCon tc = build (con (fun tc))
+typeFromTyCon tc = build (con (Sym tc))
 
 -- | Function application for type constructors.
 --
@@ -152,7 +159,7 @@
 arrowType :: [Type] -> Type -> Type
 arrowType [] res = res
 arrowType (arg:args) res =
-  build (app (fun Arrow) [arg, arrowType args res])
+  build (app (Sym Arrow) [arg, arrowType args res])
 
 -- | Is a given type a function type?
 isArrowType :: Type -> Bool
@@ -162,20 +169,20 @@
 --
 -- For multiple-argument functions, unpacks one argument.
 unpackArrow :: Type -> Maybe (Type, Type)
-unpackArrow (App (F _ Arrow) (Cons t (Cons u Empty))) =
+unpackArrow (App (Sym Arrow) (Cons t (Cons u Nil))) =
   Just (t, u)
 unpackArrow _ =
   Nothing
 
 -- | The arguments of a function type.
 typeArgs :: Type -> [Type]
-typeArgs (App (F _ Arrow) (Cons arg (Cons res Empty))) =
+typeArgs (App (Sym Arrow) (Cons arg (Cons res Nil))) =
   arg:typeArgs res
 typeArgs _ = []
 
 -- | The result of a function type.
 typeRes :: Type -> Type
-typeRes (App (F _ Arrow) (Cons _ (Cons res Empty))) =
+typeRes (App (Sym Arrow) (Cons _ (Cons res Nil))) =
   typeRes res
 typeRes ty = ty
 
@@ -183,7 +190,7 @@
 -- @n@ arguments. Crashes if the type does not have enough arguments.
 typeDrop :: Int -> Type -> Type
 typeDrop 0 ty = ty
-typeDrop n (App (F _ Arrow) (Cons _ (Cons ty Empty))) =
+typeDrop n (App (Sym Arrow) (Cons _ (Cons ty Nil))) =
   typeDrop (n-1) ty
 typeDrop _ _ =
   error "typeDrop on non-function type"
@@ -205,7 +212,7 @@
 skolemiseTypeVars :: Typed a => a -> a
 skolemiseTypeVars = typeSubst (const aTy)
   where
-    aTy = build (con (fun (tyCon (Proxy :: Proxy A))))
+    aTy = build (con (Sym (tyCon (Proxy :: Proxy A))))
 
 -- | Construct a type from a `Ty.TypeRep`.
 fromTypeRep :: Ty.TypeRep -> Type
@@ -214,7 +221,7 @@
       build (var (V n))
   | otherwise =
     let (tyCon, tys) = Ty.splitTyConApp ty in
-    build (app (fun (fromTyCon tyCon)) (map fromTypeRep tys))
+    build (app (Sym (fromTyCon tyCon)) (map fromTypeRep tys))
 
 -- | Construct a `TyCon` type from a "Data.Typeable" `Ty.TyCon`.
 fromTyCon :: Ty.TyCon -> TyCon
@@ -223,11 +230,19 @@
   | otherwise = TyCon ty
 
 -- | Some built-in type consructors.
-arrowTyCon, commaTyCon, listTyCon, dictTyCon :: Ty.TyCon
+arrowTyCon, unitTyCon, tuple2TyCon, tuple3TyCon, tuple4TyCon, tuple5TyCon, tuple6TyCon, tuple7TyCon, listTyCon, dictTyCon :: Ty.TyCon
 arrowTyCon = mkCon (Proxy :: Proxy (->))
-commaTyCon = mkCon (Proxy :: Proxy (,))
+unitTyCon = mkCon (Proxy :: Proxy ())
+tuple2TyCon = mkCon (Proxy :: Proxy (,))
+tuple3TyCon = mkCon (Proxy :: Proxy (,,))
+tuple4TyCon = mkCon (Proxy :: Proxy (,,,))
+tuple5TyCon = mkCon (Proxy :: Proxy (,,,,))
+tuple6TyCon = mkCon (Proxy :: Proxy (,,,,,))
+tuple7TyCon = mkCon (Proxy :: Proxy (,,,,,,))
 listTyCon  = mkCon (Proxy :: Proxy [])
 dictTyCon  = mkCon (Proxy :: Proxy Dict)
+tupleTyCons :: [(Ty.TyCon, Int)]
+tupleTyCons = [(unitTyCon, 0), (tuple2TyCon, 2), (tuple3TyCon, 3), (tuple4TyCon, 4), (tuple5TyCon, 5), (tuple6TyCon, 6), (tuple7TyCon, 7)]
 
 mkCon :: Typeable a => proxy a -> Ty.TyCon
 mkCon = fst . Ty.splitTyConApp . Ty.typeRep
@@ -238,7 +253,7 @@
 
 -- | Check if a type is of the form @`Dict` c@, and if so, return @c@.
 getDictionary :: Type -> Maybe Type
-getDictionary (App (F _ (TyCon dict)) (Cons ty Empty))
+getDictionary (App (Sym (TyCon dict)) (Cons ty Nil))
   | dict == dictTyCon = Just ty
 getDictionary _ = Nothing
 
@@ -261,16 +276,16 @@
 instance CoArbitrary Type where
   coarbitrary = coarbitrary . singleton
 instance CoArbitrary (TermList TyCon) where
-  coarbitrary Empty = variant 0
+  coarbitrary Nil = variant 0
   coarbitrary ConsSym{hd = Var (V x), rest = ts} =
     variant 1 . coarbitrary x . coarbitrary ts
   coarbitrary ConsSym{hd = App f _, rest = ts} =
-    variant 2 . coarbitrary (fun_id f) . coarbitrary ts
+    variant 2 . coarbitrary (symId f) . coarbitrary ts
 
 -- | Pretty-print a type. Differs from the `Pretty` instance by printing type
 -- variables in lowercase.
 pPrintType :: Type -> Doc
-pPrintType = ppr . typeSubst (\(V x) -> build (con (fun (String (as !! x))))) . canonicalise
+pPrintType = ppr . typeSubst (\(V x) -> build (con (Sym (String (as !! x))))) . canonicalise
   where
     as = supply [[x] | x <- ['a'..'z']]
     -- Print dictionary arguments specially
@@ -358,12 +373,12 @@
   typeSubst_ = subst
 
 instance Apply Type where
-  tryApply (App (F _ Arrow) (Cons arg (Cons res Empty))) t
+  tryApply (App (Sym Arrow) (Cons arg (Cons res Nil))) t
     | t == arg = Just res
   tryApply _ _ = Nothing
 
 instance (Typed a, Typed b) => Typed (a, b) where
-  typ (x, y) = build (app (fun (TyCon commaTyCon)) [typ x, typ y])
+  typ (x, y) = build (app (Sym (TyCon tuple2TyCon)) [typ x, typ y])
   otherTypesDL (x, y) = otherTypesDL x `mplus` otherTypesDL y
   typeSubst_ f (x, y) = (typeSubst_ f x, typeSubst_ f y)
 
diff --git a/src/QuickSpec/Internal/Utils.hs b/src/QuickSpec/Internal/Utils.hs
--- a/src/QuickSpec/Internal/Utils.hs
+++ b/src/QuickSpec/Internal/Utils.hs
@@ -1,6 +1,6 @@
 -- | Miscellaneous utility functions.
 {-# OPTIONS_HADDOCK hide #-}
-{-# LANGUAGE CPP #-}
+{-# LANGUAGE CPP, ScopedTypeVariables #-}
 module QuickSpec.Internal.Utils where
 
 import Control.Arrow((&&&))
@@ -20,6 +20,7 @@
 import Twee.Base hiding (lookup)
 import Control.Monad.Trans.State.Strict
 import Control.Monad
+import Data.Typeable
 
 (#) :: Category.Category cat => cat b c -> cat a b -> cat a c
 (#) = (Category..)
@@ -136,3 +137,18 @@
       | otherwise = fxp y
       where
         y = f x
+
+isResourceLimitException :: SomeException -> Bool
+isResourceLimitException ex =
+  fromException ex == Just StackOverflow ||
+  fromException ex == Just HeapOverflow ||
+  isTimeout ex ||
+  case fromException ex of
+    Just (SomeAsyncException ex) -> isResourceLimitException (SomeException ex)
+    Nothing -> False
+  where
+    -- The Timeout type wasn't exported until GHC 8.10,
+    -- otherwise we could just do:
+    -- isJust (fromException ex :: Maybe Timeout)
+    isTimeout (SomeException ex) =
+      tyConModule (typeRepTyCon (typeOf ex)) == "System.Timeout"