diff --git a/executable/SequentialMain.hs b/executable/SequentialMain.hs
--- a/executable/SequentialMain.hs
+++ b/executable/SequentialMain.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE CPP, RecordWildCards, FlexibleInstances, PatternGuards, DeriveAnyClass, RankNTypes #-}
+{-# LANGUAGE CPP, RecordWildCards, FlexibleInstances, PatternGuards, DeriveAnyClass, RankNTypes, ApplicativeDo #-}
 {-# OPTIONS_GHC -flate-specialise #-}
 module SequentialMain(main) where
 
@@ -32,7 +32,7 @@
 import System.IO
 import System.Exit
 import qualified Data.Set as Set
-import qualified Data.Label as Label
+import qualified Data.Intern as Intern
 import System.Console.ANSI
 import Data.Symbol
 import Twee.Profile
@@ -40,6 +40,7 @@
 data MainFlags =
   MainFlags {
     flags_proof :: Bool,
+    flags_proof_on_saturation :: Bool,
     flags_trace :: Maybe (String, String),
     flags_formal_proof :: Bool,
     flags_explain_encoding :: Bool,
@@ -56,197 +57,234 @@
     flags_equals_transformation :: Bool,
     flags_distributivity_heuristic :: Bool,
     flags_kbo_weight0 :: Bool,
+    flags_kbo_weight0_unary :: Bool,
     flags_goal_heuristic :: Bool }
 
 parseMainFlags :: OptionParser MainFlags
-parseMainFlags =
-  MainFlags <$> proof <*> trace <*> formal <*> explain <*> flipOrdering <*> giveUp <*> flatten <*> flattenNonGround <*> flattenLightly <*> flattenAll <*> flattenRegeneralise <*> eliminate <*> backwardsGoal <*> flattenBackwardsGoal <*> equalsTransformation <*> distributivityHeuristic <*> kboWeight0 <*> goalHeuristic
-  where
-    proof =
-      inGroup "Output options" $
-      bool "proof" ["Produce proofs (on by default)."]
-      True
-    trace =
-      expert $
-      inGroup "Output options" $
-      flag "trace"
-        ["Write a Prolog-format execution trace to this file (off by default)."]
-        Nothing ((\x y -> Just (x, y)) <$> argFile <*> argModule)
-    formal =
-      expert $
-      inGroup "Output options" $
-      bool "formal-proof" ["Print proof as formal TSTP derivation (requires --tstp; off by default)."] False
-    explain =
-      expert $
-      inGroup "Output options" $
-      bool "explain-encoding" ["In CASC mode, explain the conditional encoding (off by default)."] False
-    flipOrdering =
-      expert $
-      inGroup "Term order options" $
-      bool "flip-ordering" ["Make more common function symbols smaller (off by default)."] False
-    kboWeight0 =
-      expert $
-      inGroup "Term order options" $
-      bool "kbo-weight0" ["Give functions of arity >= 2 a weight of 0."] False
-    giveUp =
-      expert $
-      inGroup "Output options" $
-      bool "give-up-on-saturation" ["Report SZS status GiveUp rather than Unsatisfiable on saturation (off by default)."] False
-    flatten =
-      expert $
-      inGroup "Completion heuristics" $
-      bool "flatten-goal" ["Flatten goal by adding new axioms (on by default)."] True
-    flattenNonGround =
-      expert $
-      inGroup "Completion heuristics" $
-      bool "flatten-nonground" ["Flatten even non-ground clauses (off by default)."] False
-    flattenLightly =
-      expert $
-      inGroup "Completion heuristics" $
-      bool "flatten-goal-lightly" ["Flatten goal non-recursively by adding new axioms (off by default)."] False
-    flattenAll =
-      expert $
-      inGroup "Completion heuristics" $
-      bool "flatten" ["Flatten all clauses by adding new axioms (off by default)."] False
-    flattenRegeneralise =
-      expert $
-      inGroup "Completion heuristics" $
-      bool "flatten-regeneralise" ["Regeneralise rules involving flattened goal terms (off by default)."] False
-    backwardsGoal =
-      expert $
-      inGroup "Completion heuristics" $
-      flag "backwards-goal" ["Try rewriting backwards from the goal this many times (0 by default)."] 0 argNum
-    flattenBackwardsGoal =
-      expert $
-      inGroup "Completion heuristics" $
-      flag "flatten-backwards-goal" ["Try rewriting backwards from the goal this many times when flattening (0 by default)."] 0 argNum
-    equalsTransformation =
-      expert $
-      inGroup "Completion heuristics" $
-      bool "equals-transformation" ["Apply the 'equals transformation' even to ground goals (off by default)."] False
-    distributivityHeuristic =
-      expert $
-      inGroup "Completion heuristics" $
-      bool "distributivity-heuristic" ["Treat distributive operators specially (off by default)."] False
-    goalHeuristic =
-      expert $
-      inGroup "Completion heuristics" $
-      bool "goal-heuristic" ["Use the CP weighting heuristic from Anantharaman and Andrianarievelo (off by default)."] False
-    eliminate =
-      inGroup "Proof presentation" $
-      concat <$>
-      manyFlags "eliminate"
-        ["Treat these axioms as definitions and eliminate them from the proof.",
-         "The axiom must have the shape f(x1...xn) = t, where x1...xn are",
-         "distinct variables. The term f must not otherwise appear in the problem!",
-         "This is not checked."]
-        (splitOn "," <$> arg "<axioms>" "expected a list of axiom names" Just)
+parseMainFlags = do
+  let argModule = arg "<module>" "expected a Prolog module name" Just
+  flags_proof <-
+    inGroup "Output options" $
+    bool "proof" ["Produce proofs (on by default)."]
+    True
+  flags_proof_on_saturation <-
+    expert $
+    inGroup "Output options" $
+    bool "proof-on-saturation" ["Produce proofs of all rewrite rules on saturation (off by default)."]
+    False
+  flags_trace <-
+    expert $
+    inGroup "Output options" $
+    flag "trace"
+      ["Write a Prolog-format execution trace to this file (off by default)."]
+      Nothing ((\x y -> Just (x, y)) <$> argFile <*> argModule)
+  flags_formal_proof <-
+    expert $
+    inGroup "Output options" $
+    bool "formal-proof" ["Print proof as formal TSTP derivation (requires --tstp; off by default)."] False
+  flags_explain_encoding <-
+    expert $
+    inGroup "Output options" $
+    bool "explain-encoding" ["In CASC mode, explain the conditional encoding (off by default)."] False
+  flags_flip_ordering <-
+    expert $
+    inGroup "Term order options" $
+    bool "flip-ordering" ["Make more common function symbols smaller (off by default)."] False
+  flags_kbo_weight0 <-
+    expert $
+    inGroup "Term order options" $
+    bool "kbo-weight0" ["Give functions of arity >= 2 a weight of 0."] False
+  flags_kbo_weight0_unary <-
+    expert $
+    inGroup "Term order options" $
+    bool "kbo-weight0-unary" ["Give one function of arity 1 a weight of 0."] True
+  flags_give_up_on_saturation <-
+    expert $
+    inGroup "Output options" $
+    bool "give-up-on-saturation" ["Report SZS status GiveUp rather than Unsatisfiable on saturation (off by default)."] False
+  flags_flatten_goals <-
+    expert $
+    inGroup "Completion heuristics" $
+    bool "flatten-goal" ["Flatten goal by adding new axioms (on by default)."] True
+  flags_flatten_nonground <-
+    expert $
+    inGroup "Completion heuristics" $
+    bool "flatten-nonground" ["Flatten even non-ground clauses (off by default)."] False
+  flags_flatten_goals_lightly <-
+    expert $
+    inGroup "Completion heuristics" $
+    bool "flatten-goal-lightly" ["Flatten goal non-recursively by adding new axioms (off by default)."] False
+  flags_flatten_all <-
+    expert $
+    inGroup "Completion heuristics" $
+    bool "flatten" ["Flatten all clauses by adding new axioms (off by default)."] False
+  flags_flatten_regeneralise <-
+    expert $
+    inGroup "Completion heuristics" $
+    bool "flatten-regeneralise" ["Regeneralise rules involving flattened goal terms (off by default)."] False
+  flags_backwards_goal <-
+    expert $
+    inGroup "Completion heuristics" $
+    flag "backwards-goal" ["Try rewriting backwards from the goal this many times (0 by default)."] 0 argNum
+  flags_flatten_backwards_goal <-
+    expert $
+    inGroup "Completion heuristics" $
+    flag "flatten-backwards-goal" ["Try rewriting backwards from the goal this many times when flattening (0 by default)."] 0 argNum
+  flags_equals_transformation <-
+    expert $
+    inGroup "Completion heuristics" $
+    bool "equals-transformation" ["Apply the 'equals transformation' even to ground goals (off by default)."] False
+  flags_distributivity_heuristic <-
+    expert $
+    inGroup "Completion heuristics" $
+    bool "distributivity-heuristic" ["Treat distributive operators specially (off by default)."] False
+  flags_goal_heuristic <-
+    expert $
+    inGroup "Completion heuristics" $
+    bool "goal-heuristic" ["Use the CP weighting heuristic from Anantharaman and Andrianarievelo (off by default)."] False
+  flags_eliminate <-
+    inGroup "Proof presentation" $
+    concat <$>
+    manyFlags "eliminate"
+      ["Treat these axioms as definitions and eliminate them from the proof.",
+       "The axiom must have the shape f(x1...xn) = t, where x1...xn are",
+       "distinct variables. The term f must not otherwise appear in the problem!",
+       "This is not checked."]
+      (splitOn "," <$> arg "<axioms>" "expected a list of axiom names" Just)
 
-    argModule = arg "<module>" "expected a Prolog module name" Just
+  return MainFlags{..}
 
 parseConfig :: OptionParser (Config Constant)
-parseConfig =
-  Config <$> maxSize <*> maxCPs <*> maxCPDepth <*> maxRules <*> simplify <*> normPercent <*> cpSampleSize <*> cpRenormaliseThreshold <*> set_join_goals <*> always_simplify <*> complete_subsets <*>
-    pure undefined <*> -- scoring function - filled in later, in runTwee
-    (Join.Config <$> ground_join <*> connectedness <*> ground_connectedness <*> set_join) <*>
-    (Proof.Config <$> all_lemmas <*> flat_proof <*> ground_proof <*> show_instances <*> colour <*> show_axiom_uses) <*> pure [] <*> randomMode <*> randomModeGoalDirected <*> randomModeSimple <*> randomModeBestOf <*> alwaysComplete
-  where
-    maxSize =
-      inGroup "Resource limits" $
-      flag "max-term-size" ["Discard rewrite rules whose left-hand side is bigger than this limit (unlimited by default)."] Nothing (Just <$> checkSize <$> argNum)
-    checkSize n t = KBO.size t <= n
-    maxCPs =
-      inGroup "Resource limits" $
-      flag "max-cps" ["Give up after considering this many critical pairs (unlimited by default)."] maxBound argNum
-    maxCPDepth =
-      inGroup "Resource limits" $
-      flag "max-cp-depth" ["Only consider critical pairs up to this depth (unlimited by default)."] maxBound argNum
-    maxRules =
-      inGroup "Resource limits" $
-      flag "max-rules" ["Give up after generating this many rules (unlimited by default)."] maxBound argNum
-    simplify =
-      expert $
-      inGroup "Completion heuristics" $
-      bool "simplify"
-        ["Simplify rewrite rules with respect to one another (on by default)."]
-        True
-    normPercent =
-      expert $
-      inGroup "Completion heuristics" $
-      defaultFlag "normalise-queue-percent" "Percent of time spent renormalising queued critical pairs" cfg_renormalise_percent argNum
-    cpSampleSize =
-      expert $
-      inGroup "Completion heuristics" $
-      defaultFlag "cp-sample-size" "Size of random CP sample used to trigger renormalisation" cfg_cp_sample_size argNum
-    cpRenormaliseThreshold =
-      expert $
-      inGroup "Completion heuristics" $
-      defaultFlag "cp-renormalise-threshold" "Trigger renormalisation when this percentage of CPs can be simplified" cfg_renormalise_threshold argNum
-    ground_join =
+parseConfig = do
+  cfg_accept_term <-
+    let checkSize n t = KBO.size (t :: Term Constant) <= n in
+    inGroup "Resource limits" $
+    flag "max-term-size" ["Discard rewrite rules whose left-hand side is bigger than this limit (unlimited by default)."] Nothing (Just <$> checkSize <$> argNum)
+  cfg_max_critical_pairs <-
+    inGroup "Resource limits" $
+    flag "max-cps" ["Give up after considering this many critical pairs (unlimited by default)."] maxBound argNum
+  cfg_max_cp_depth <-
+    inGroup "Resource limits" $
+    flag "max-cp-depth" ["Only consider critical pairs up to this depth (unlimited by default)."] maxBound argNum
+  cfg_max_rules <-
+    inGroup "Resource limits" $
+    flag "max-rules" ["Give up after generating this many rules (unlimited by default)."] maxBound argNum
+  cfg_max_time <-
+    inGroup "Resource limits" $
+    flag "max-time" ["Give up after running for this long in seconds (unlimited by default)."] Nothing (Just <$> argNum)
+  cfg_simplify <-
+    expert $
+    inGroup "Completion heuristics" $
+    bool "simplify"
+      ["Simplify rewrite rules with respect to one another (on by default)."]
+      True
+  cfg_renormalise_percent <-
+    expert $
+    inGroup "Completion heuristics" $
+    defaultFlag "normalise-queue-percent" "Percent of time spent renormalising queued critical pairs" cfg_renormalise_percent argNum
+  cfg_cp_sample_size <-
+    expert $
+    inGroup "Completion heuristics" $
+    defaultFlag "cp-sample-size" "Size of random CP sample used to trigger renormalisation" cfg_cp_sample_size argNum
+  cfg_renormalise_threshold <-
+    expert $
+    inGroup "Completion heuristics" $
+    defaultFlag "cp-renormalise-threshold" "Trigger renormalisation when this percentage of CPs can be simplified" cfg_renormalise_threshold argNum
+  cfg_set_join_goals <-
+    expert $
+    inGroup "Critical pair joining heuristics" $
+    bool "set-join-goals"
+      ["Compute all normal forms when joining goal terms (on by default)."]
+      True
+  cfg_always_simplify <-
+    expert $
+    inGroup "Debugging options" $
+    bool "always-simplify"
+      ["Interreduce rules after every step."]
+      False
+  cfg_complete_subsets <-
+    expert $
+    inGroup "Critical pair joining heuristics" $
+    bool "complete-subsets"
+      ["Identify and exploit complete subsets of the axioms in joining (off by default)."]
+      False
+  let cfg_score_cp = undefined -- filled in later, in runTwee
+
+  cfg_join <- do
+    cfg_ground_join <-
       expert $
       inGroup "Critical pair joining heuristics" $
       bool "ground-joining"
         ["Test terms for ground joinability (on by default)."]
         True
-    connectedness =
+    cfg_use_connectedness_standalone <-
       expert $
       inGroup "Critical pair joining heuristics" $
       bool "connectedness"
         ["Test terms for subconnectedness, as a separate check (on by default)."]
         True
-    ground_connectedness =
+    cfg_use_connectedness_in_ground_joining <-
       expert $
       inGroup "Critical pair joining heuristics" $
       bool "ground-connectedness"
         ["Test terms for subconnectedness, as part of ground joinability testing (off by default)."]
         False
-    complete_subsets =
-      expert $
-      inGroup "Critical pair joining heuristics" $
-      bool "complete-subsets"
-        ["Identify and exploit complete subsets of the axioms in joining (off by default)."]
-        False
-    set_join =
+    cfg_set_join <-
       expert $
       inGroup "Critical pair joining heuristics" $
       bool "set-join"
         ["Compute all normal forms when joining critical pairs (off by default)."]
         False
-    set_join_goals =
-      expert $
+    cfg_ground_join_limit <-
       inGroup "Critical pair joining heuristics" $
-      bool "set-join-goals"
-        ["Compute all normal forms when joining goal terms (on by default)."]
-        True
-    always_simplify =
-      expert $
-      inGroup "Debugging options" $
-      bool "always-simplify"
-        ["Interreduce rules after every step."]
-        False
-    all_lemmas =
+      flag "ground-joining-limit" ["Assume not ground joinable after considering this many orderings (unlimited by default)."] maxBound argNum
+    cfg_ground_join_incomplete_limit <-
+      inGroup "Critical pair joining heuristics" $
+      flag "ground-joining-incomplete-limit" ["Assume ground joinable after considering this many orderings (unlimited by default)."] maxBound argNum
+    return Join.Config{..}
+
+  cfg_proof_presentation <- do
+    cfg_all_lemmas <-
       inGroup "Proof presentation" $
       bool "all-lemmas"
         ["Produce a proof with one lemma for each critical pair (off by default)."]
         False
-    flat_proof =
+    cfg_no_lemmas <-
       inGroup "Proof presentation" $
       bool "no-lemmas"
         ["Produce a proof with no lemmas (off by default).",
          "May lead to exponentially large proofs."]
         False
-    ground_proof =
+    cfg_ground_proof <-
       inGroup "Proof presentation" $
       bool "ground-proof"
         ["Produce a ground proof (off by default).",
          "May lead to exponentially large proofs."]
         False
-    show_instances =
+    cfg_show_instances <-
       inGroup "Proof presentation" $
       bool "show-instances"
         ["Show which instance of a lemma or axiom each rewrite step uses (off by default)."]
         False
-    show_axiom_uses =
+    cfg_use_colour <-
+      let
+        colourFlag =
+          inGroup "Proof presentation" $
+          primFlag "(no-)colour"
+            ["Produce output in colour (on by default if writing output to a terminal)."]
+            (`elem` map fst colourFlags)
+            (\_ y -> return y)
+            Nothing
+            (pure (`lookup` colourFlags))
+        colourFlags = [("--colour", True), ("--no-colour", False),
+                       ("--color", True), ("--no-color", False)]
+        colourSupported =
+          liftM2 (&&) (hSupportsANSIColor stdout)
+            (return (setSGRCode [] /= "")) -- Check for Windows terminal not supporting ANSI
+      in fromMaybe <$> io colourSupported <*> colourFlag
+
+    cfg_show_uses_of_axioms <-
+      let interpret xss ax = axiom_name ax `elem` xss || "all" `elem` xss in
       inGroup "Proof presentation" $
       interpret <$>
       concat <$>
@@ -255,49 +293,68 @@
          "Separate multiple axiom names with commas.",
          "Use --show-uses-of all to show uses of all axioms."]
         (splitOn "," <$> arg "<axioms>" "expected a list of axiom names" Just)
-      where
-        interpret xss ax = axiom_name ax `elem` xss || "all" `elem` xss
-    randomMode =
-      expert $
-      inGroup "Completion heuristics" $
-      bool "random-mode"
-        ["Use random testing to find suitable CPs (doesn't work yet!) (off by default)."]
-        False
-    randomModeGoalDirected =
-      expert $
-      inGroup "Completion heuristics" $
-      bool "random-mode-goal-directed"
-        ["Use goal-direction in --random-mode (off by default)."]
-        False
-    randomModeSimple =
-      expert $
-      inGroup "Completion heuristics" $
-      bool "random-mode-simple"
-        ["Use simple version of --random-mode (off by default)."]
-        False
-    randomModeBestOf =
-      inGroup "Completion heuristics" $
-      defaultFlag "random-mode-best-of" "Generate this many critical pairs at a time and pick the best one" cfg_random_mode_best_of argNum
-    alwaysComplete =
-      inGroup "Input and clausifier options" $
-      bool "complete"
-        ["Don't stop until the rewrite system is confluent"]
+
+    cfg_show_peaks <-
+      inGroup "Proof presentation" $
+      bool "show-peaks"
+        ["Show peak terms in a proof (off by default)."]
         False
-    colour = fromMaybe <$> io colourSupported <*> colourFlag
-    colourFlag =
+    cfg_eliminate_existentials_coding <-
       inGroup "Proof presentation" $
-      primFlag "(no-)colour"
-        ["Produce output in colour (on by default if writing output to a terminal)."]
-        (`elem` map fst colourFlags)
-        (\_ y -> return y)
-        Nothing
-        (pure (`lookup` colourFlags))
-    colourFlags = [("--colour", True), ("--no-colour", False),
-                   ("--color", True), ("--no-color", False)]
-    colourSupported =
-      liftM2 (&&) (hSupportsANSIColor stdout)
-        (return (setSGRCode [] /= "")) -- Check for Windows terminal not supporting ANSI
+      bool "eliminate-existentials-coding"
+        ["Eliminate $equals from proofs (on by default)."]
+        True
+    cfg_show_subterms <-
+      inGroup "Proof presentation" $
+      bool "show-subterms"
+        ["Show which subterm is rewritten at each step (off by default)."]
+        False
 
+    return Proof.Config{..}
+
+  let cfg_eliminate_axioms = [] -- filled in later
+
+  cfg_random_mode <-
+    expert $
+    inGroup "Completion heuristics" $
+    bool "random-mode"
+      ["Use random testing to find suitable CPs (doesn't work yet!) (off by default)."]
+      False
+  cfg_random_mode_goal_directed <-
+    expert $
+    inGroup "Completion heuristics" $
+    bool "random-mode-goal-directed"
+      ["Use goal-direction in --random-mode (off by default)."]
+      False
+  cfg_random_mode_simple <-
+    expert $
+    inGroup "Completion heuristics" $
+    bool "random-mode-simple"
+      ["Use simple version of --random-mode (off by default)."]
+      False
+  cfg_random_mode_best_of <-
+    inGroup "Completion heuristics" $
+    defaultFlag "random-mode-best-of" "Generate this many critical pairs at a time and pick the best one" cfg_random_mode_best_of argNum
+  cfg_always_complete <-
+    inGroup "Input and clausifier options" $
+    bool "complete"
+      ["Don't stop until the rewrite system is confluent"]
+      False
+  cfg_hint_skel_cost <-
+    expert $
+    inGroup "Critical pair weighting heuristics" $
+    defaultFlag "hint-skel-cost" "Size of hint skeletons" cfg_hint_skel_cost argNum
+  cfg_hint_skel_factor <-
+    expert $
+    inGroup "Critical pair weighting heuristics" $
+    defaultFlag "hint-skel-factor" "Size factor of hint skeletons" cfg_hint_skel_factor argNum
+  cfg_print_score <-
+    expert $
+    inGroup "Output options" $
+    bool "print-score" ["Print score of each generated rule (off by default)."] False
+
+  return Config{..}
+  where
     defaultFlag :: Show a => String -> String -> (Config Constant -> a) -> ArgParser a -> OptionParser a
     defaultFlag name desc field parser =
       flag name [desc ++ " (" ++ show def ++ " by default)."] def parser
@@ -305,38 +362,41 @@
         def = field defaultConfig
 
 parseCPConfig :: OptionParser CP.Config
-parseCPConfig =
-  CP.Config <$> lweight <*> rweight <*> funweight <*> varweight <*> depthweight <*> dupcost <*> dupfactor
+parseCPConfig = do
+  cfg_lhsweight <-
+    expert $
+    inGroup "Critical pair weighting heuristics" $
+    defaultFlag "lhs-weight" "Weight given to LHS of critical pair" CP.cfg_lhsweight argNum
+  cfg_rhsweight <-
+    expert $
+    inGroup "Critical pair weighting heuristics" $
+    defaultFlag "rhs-weight" "Weight given to RHS of critical pair" CP.cfg_rhsweight argNum
+  cfg_funweight <-
+    expert $
+    inGroup "Critical pair weighting heuristics" $
+    defaultFlag "fun-weight" "Weight given to function symbols" CP.cfg_funweight argNum
+  cfg_varweight <-
+    expert $
+    inGroup "Critical pair weighting heuristics" $
+    defaultFlag "var-weight" "Weight given to variable symbols" CP.cfg_varweight argNum
+  cfg_depthweight <-
+    expert $
+    inGroup "Critical pair weighting heuristics" $
+    defaultFlag "depth-weight" "Weight given to critical pair depth" CP.cfg_depthweight argNum
+  cfg_dupcost <-
+    expert $
+    inGroup "Critical pair weighting heuristics" $
+    defaultFlag "dup-cost" "Cost of duplicate subterms" CP.cfg_dupcost argNum
+  cfg_dupfactor <-
+    expert $
+    inGroup "Critical pair weighting heuristics" $
+    defaultFlag "dup-factor" "Size factor of duplicate subterms" CP.cfg_dupfactor argNum
+  cfg_resonance <-
+    expert $
+    inGroup "Critical pair weighting heuristics" $
+    bool "resonance" ["Interpret hints as resonators by only allowing substitutions which map variables to variables (off by default)."] False
+  return CP.Config{..}
   where
-    lweight =
-      expert $
-      inGroup "Critical pair weighting heuristics" $
-      defaultFlag "lhs-weight" "Weight given to LHS of critical pair" CP.cfg_lhsweight argNum
-    rweight =
-      expert $
-      inGroup "Critical pair weighting heuristics" $
-      defaultFlag "rhs-weight" "Weight given to RHS of critical pair" CP.cfg_rhsweight argNum
-    funweight =
-      expert $
-      inGroup "Critical pair weighting heuristics" $
-      defaultFlag "fun-weight" "Weight given to function symbols" CP.cfg_funweight argNum
-    varweight =
-      expert $
-      inGroup "Critical pair weighting heuristics" $
-      defaultFlag "var-weight" "Weight given to variable symbols" CP.cfg_varweight argNum
-    depthweight =
-      expert $
-      inGroup "Critical pair weighting heuristics" $
-      defaultFlag "depth-weight" "Weight given to critical pair depth" CP.cfg_depthweight argNum
-    dupcost =
-      expert $
-      inGroup "Critical pair weighting heuristics" $
-      defaultFlag "dup-cost" "Cost of duplicate subterms" CP.cfg_dupcost argNum
-    dupfactor =
-      expert $
-      inGroup "Critical pair weighting heuristics" $
-      defaultFlag "dup-factor" "Size factor of duplicate subterms" CP.cfg_dupfactor argNum
-
     defaultFlag name desc field parser =
       flag name [desc ++ " (" ++ show def ++ " by default)."] def parser
       where
@@ -351,6 +411,7 @@
 
 data Constant =
   Minimal |
+  Skolem Int |
   Constant {
     con_prec   :: {-# UNPACK #-} !Precedence,
     con_id     :: {-# UNPACK #-} !Jukebox.Function,
@@ -358,20 +419,23 @@
     con_size   :: !Integer,
     con_weight :: !Integer,
     con_bonus  :: !Bool }
-  deriving (Eq, Ord, Labelled)
+  deriving (Eq, Ord)
 
-data Precedence = Precedence !Bool !Bool !(Maybe Int) !Int
+data Precedence = Precedence !Bool !Bool !Bool !(Maybe Int) !Int
   deriving (Eq, Ord)
 
 instance KBO.Sized Constant where
   size Minimal = 1
+  size Skolem{} = 1
   size Constant{..} = con_size
 instance KBO.Weighted Constant where
   argWeight Minimal = 1
+  argWeight Skolem{} = 1
   argWeight Constant{..} = con_weight
 
 instance Pretty Constant where
   pPrint Minimal = text "?"
+  pPrint (Skolem n) = text ("sk" ++ show n)
   pPrint Constant{..} = text (removePostfix (base con_id))
     where
       removePostfix ('_':x:xs) | con_arity == 1 = x:xs
@@ -379,6 +443,7 @@
 
 instance PrettyTerm Constant where
   termStyle Minimal = uncurried
+  termStyle Skolem{} = uncurried
   termStyle Constant{..}
     | hasLabel "type_tag" con_id = invisible
     | "_" `isPrefixOf` base con_id && con_arity == 1 = postfix
@@ -390,7 +455,8 @@
         _ -> uncurried
 
 instance Minimal Constant where
-  minimal = fun Minimal
+  minimal = Sym Minimal
+  skolem = Sym . Skolem
 
 instance Ordered Constant where
   lessEq t u = KBO.lessEq t u
@@ -399,12 +465,16 @@
 
 instance EqualsBonus Constant where
   hasEqualsBonus Minimal = False
+  hasEqualsBonus Skolem{} = False
   hasEqualsBonus c = con_bonus c
   isEquals Minimal = False
+  isEquals Skolem{} = False
   isEquals c = SequentialMain.isEquals (con_id c)
   isTrue Minimal = False
+  isTrue Skolem{} = False
   isTrue c = SequentialMain.isTrue (con_id c)
   isFalse Minimal = False
+  isFalse Skolem{} = False
   isFalse c = SequentialMain.isFalse (con_id c)
 
 data TweeContext =
@@ -425,13 +495,16 @@
       con_prec = prec,
       con_id = fun,
       con_arity = Jukebox.arity fun,
-      con_size = if flags_kbo_weight0 && Jukebox.arity fun >= 2 then 0 else 1,
+      con_size = if flags_kbo_weight0 && Jukebox.arity fun >= 2 then 0 else if flags_kbo_weight0_unary && isInv then 0 else 1,
       con_weight = 1,
       con_bonus = bonus fun }
   where
     bonus fun =
       (isIfeq fun && encoding flags /= Asymmetric2) ||
       SequentialMain.isEquals fun
+    isInv =
+      case prec of
+        Precedence _ x _ _ _ -> x
 
 isType :: Jukebox.Function -> Bool
 isType fun =
@@ -461,20 +534,20 @@
 tweeTerm flags horn ctx prec t = build (tm t)
   where
     tm (Jukebox.Var (x ::: _)) =
-      var (V (fromIntegral (Label.labelNum (Label.label x))))
+      var (V (Intern.symId (Intern.intern x)))
     tm (f :@: ts) =
-      app (fun (tweeConstant flags horn ctx (prec f) f)) (map tm ts)
+      app (Sym (tweeConstant flags horn ctx (prec f) f)) (map tm ts)
 
 jukeboxTerm :: TweeContext -> Term Constant -> Jukebox.Term
 jukeboxTerm TweeContext{..} (Var (V x)) =
   Jukebox.Var (Unique (fromIntegral x) (intern "X") Nothing defaultRenamer ::: ctx_type)
-jukeboxTerm ctx@TweeContext{..} (App f t) =
-  jukeboxFunction ctx (fun_value f) :@: map (jukeboxTerm ctx) ts
+jukeboxTerm ctx@TweeContext{..} (App (Sym f) t) =
+  jukeboxFunction ctx f :@: map (jukeboxTerm ctx) ts
   where
     ts = unpack t
 
-makeContext :: Problem Clause -> TweeContext
-makeContext prob = run prob $ \prob -> do
+makeContext :: [Jukebox.Term] -> Problem Clause -> TweeContext
+makeContext hints prob = run (hints, prob) $ \(_, prob) -> do
   let
     ty =
       case types' prob of
@@ -495,9 +568,9 @@
     ctx_equals = equals,
     ctx_type = ty }
 
-flattenGoals :: Int -> Bool -> Bool -> Bool -> Problem Clause -> Problem Clause
-flattenGoals backwardsGoal flattenNonGround flattenAll full prob =
-  run prob $ \prob -> do
+flattenGoals :: Int -> Bool -> Bool -> Bool -> [Jukebox.Term] -> Problem Clause -> Problem Clause
+flattenGoals backwardsGoal flattenNonGround flattenAll full hints prob =
+  run (hints, prob) $ \(_, prob) -> do
     let ts = usort $ extraTerms prob
     cs <- mapM define ts
     return (prob ++ cs)
@@ -525,7 +598,7 @@
       let vs  = Jukebox.vars ts
           g = name ::: FunType (map typ vs) (typ f)
           c = clause [Pos (g :@: map Jukebox.Var vs Jukebox.:=: f :@: ts)]
-      return Input{tag = "flattening", kind = Jukebox.Ax Definition,
+      return Input{ident = Nothing, tag = "flattening", kind = Jukebox.Ax Definition,
                    what = c, source = Unknown }
 
     backwards 0 _ t = [t]
@@ -540,9 +613,9 @@
         ground u,
         v <- backwards (n-1) cs u ]
 
-addDistributivityHeuristic :: Problem Clause -> Problem Clause
-addDistributivityHeuristic prob =
-  run prob $ \prob -> do
+addDistributivityHeuristic :: [Jukebox.Term] -> Problem Clause -> Problem Clause
+addDistributivityHeuristic hints prob =
+  run (hints, prob) $ \(_, prob) -> do
     cs <- mapM add prob
     return (prob ++ catMaybes cs)
 
@@ -579,7 +652,7 @@
       let vs  = Jukebox.vars t
           g = name ::: FunType (map typ vs) (typ t)
           c = clause [Pos (g :@: map Jukebox.Var vs Jukebox.:=: t)]
-      return Input{tag = "distributivity_heuristic", kind = Jukebox.Ax Definition,
+      return Input{ident = Nothing, tag = "distributivity_heuristic", kind = Jukebox.Ax Definition,
                    what = c, source = Unknown }
 
 -- Encode existentials so that all goals are ground.
@@ -587,7 +660,9 @@
 addNarrowing alwaysNarrow TweeContext{..} prob =
   unchanged ++ equalityClauses
   where
-    (unchanged, nonGroundGoals) = partitionEithers (map f prob)
+    prob' = [inp { ident = Just (variant "addNarrowing" [i :: Int]) } | (i, inp) <- zip [0..] prob]
+
+    (unchanged, nonGroundGoals) = partitionEithers (map f prob')
       where
         f inp@Input{what = Clause (Bind _ [Neg (x Jukebox.:=: y)])}
           | not (ground x) || not (ground y) || alwaysNarrow =
@@ -613,6 +688,7 @@
           -- Equisatisfiable to the input clauses
           justification =
             Input {
+              ident = Just (name "addNarrowing2"),
               tag  = "new_negated_conjecture",
               kind = Jukebox.Ax NegatedConjecture,
               what =
@@ -622,15 +698,16 @@
                 inference "encode_existential" "esa"
                   (map (fmap toForm . fst) nonGroundGoals) }
 
-          input tag form =
+          input tag form i =
             Input {
+              ident = Just (variant "addNarrowing3" [i :: Int]),
               tag = tag,
-              kind = Conj Conjecture,
+              kind = Jukebox.Ax NegatedConjecture,
               what = clause [form],
               source =
                 inference "split_conjunct" "thm" [justification] }
 
-        in [input tag form | (tag, form) <- equalityLiterals]
+        in [input tag form i | ((tag, form), i) <- zip equalityLiterals [0..]]
 
 data PreEquation =
   PreEquation {
@@ -662,19 +739,19 @@
       return $ Left (pre inp (Jukebox.Var ctx_var, ctx_minimal :@: []))
     identify inp = Left inp
 
-runTwee :: GlobalFlags -> TSTPFlags -> HornFlags -> [String] -> Config Constant -> CP.Config -> MainFlags -> (IO () -> IO ()) -> Problem Clause -> IO Answer
-runTwee globals (TSTPFlags tstp) horn precedence config0 cpConfig flags@MainFlags{..} later obligs = {-# SCC runTwee #-} do
+runTwee :: GlobalFlags -> TSTPFlags -> HornFlags -> [String] -> Config Constant -> CP.Config -> MainFlags -> (IO () -> IO ()) -> [Jukebox.Term] -> Problem Clause -> IO Answer
+runTwee globals (TSTPFlags tstp) horn precedence config0 cpConfig flags@MainFlags{..} later hints obligs = {-# SCC runTwee #-} do
   let
     -- Encode whatever needs encoding in the problem
     obligs1
-      | flags_flatten_goals_lightly = flattenGoals flags_flatten_backwards_goal flags_flatten_nonground False False obligs
-      | flags_flatten_all = flattenGoals flags_flatten_backwards_goal flags_flatten_nonground True True obligs
-      | flags_flatten_goals = flattenGoals flags_flatten_backwards_goal flags_flatten_nonground False True obligs
+      | flags_flatten_goals_lightly = flattenGoals flags_flatten_backwards_goal flags_flatten_nonground False False hints obligs
+      | flags_flatten_all = flattenGoals flags_flatten_backwards_goal flags_flatten_nonground True True hints obligs
+      | flags_flatten_goals = flattenGoals flags_flatten_backwards_goal flags_flatten_nonground False True hints obligs
       | otherwise = obligs
     obligs2
-      | flags_distributivity_heuristic = addDistributivityHeuristic obligs1
+      | flags_distributivity_heuristic = addDistributivityHeuristic hints obligs1
       | otherwise = obligs1
-    ctx = makeContext obligs2
+    ctx = makeContext hints obligs2
     lowercaseSkolem x
       | hasLabel "skolem" x =
         withRenamer x $ \s i ->
@@ -682,7 +759,7 @@
             Renaming xss xs ->
               Renaming (map (map toLower) xss) (map toLower xs)
       | otherwise = x
-    prob = prettyNames (mapName lowercaseSkolem (addNarrowing flags_equals_transformation ctx obligs2))
+    (hints', prob) = prettyNames (mapName lowercaseSkolem (hints, addNarrowing flags_equals_transformation ctx obligs2))
 
   (unsortedAxioms0, goals0) <-
     case identifyProblem ctx prob of
@@ -699,23 +776,31 @@
     prec c =
       Precedence
         (isType c)
+        (Just c == maxUnary)
         (isNothing (elemIndex (base c) precedence))
         (fmap negate (elemIndex (base c) precedence))
         (maybeNegate (Map.findWithDefault 0 c funOccs))
     maybeNegate = if flags_flip_ordering then negate else id
     funOccs = funsOcc prob
+    maxUnary =
+      case filter (\(f, _) -> arity f == 1 && not (isType f)) (Map.toList funOccs) of
+        [] -> Nothing
+        xs -> Just (fst (maximumBy (comparing snd) xs))
 
     -- Translate everything to Twee.
-    toEquation (t, u) =
-      canonicalise (tweeTerm flags horn ctx prec t :=: tweeTerm flags horn ctx prec u)
+    toTerm t = tweeTerm flags horn ctx prec t
+    toEquation (t, u) = canonicalise (toTerm t :=: toTerm u)
 
     axiomCompare ax1 ax2
+      | isEquality ax1' && not (isEquality ax2') = GT
+      | isEquality ax2' && not (isEquality ax1') = LT
       | ax1' `simplerThan` ax2' = LT
       | ax2' `simplerThan` ax1' = GT
       | otherwise = EQ
       where
         ax1' = toEquation (pre_eqn ax1)
         ax2' = toEquation (pre_eqn ax2)
+        isEquality ax = isJust (decodeEquality (eqn_lhs ax)) || isJust (decodeEquality (eqn_rhs ax))
     axioms0 = sortBy axiomCompare unsortedAxioms0
 
     goals =
@@ -735,15 +820,15 @@
   let
     goalNests = nests (map goal_eqn goals)
     goalOccs = occs (map goal_eqn goals)
-    score depth eqn
+    score depth hints eqn
       | flags_goal_heuristic =
-        fromIntegral (CP.score cpConfig depth eqn) *
+        CP.score cpConfig depth hints eqn *
         product
           [ pos (IntMap.findWithDefault 0 f eqnNests - IntMap.findWithDefault 0 f goalNests) *
             pos (IntMap.findWithDefault 0 f eqnOccs - IntMap.findWithDefault 0 f goalOccs)
           | f <- IntMap.keys eqnNests ] -- skip constants
       | otherwise = 
-        fromIntegral (CP.score cpConfig depth eqn)
+        CP.score cpConfig depth hints eqn
       where
         eqnNests = nests eqn
         eqnOccs = occs eqn
@@ -753,7 +838,8 @@
     config = config0 { cfg_score_cp = score, cfg_eliminate_axioms = if flags_flatten_regeneralise then defs else [] }
 
   let
-    withGoals = foldl' (addGoal config) (initialState config) goals
+    withHints = foldl' (addHint config) (initialState config) (map toTerm hints')
+    withGoals = foldl' (addGoal config) withHints goals
     withAxioms = foldl' (addAxiom config) withGoals axioms
     withBackwardsGoal = foldn rewriteGoalsBackwards withAxioms flags_backwards_goal
 
@@ -781,7 +867,7 @@
         say (prettyShow msg)
         sayTrace (show (traceMsg msg)) }
 
-    traceMsg (NewActive active) =
+    traceMsg (NewActive _ active) =
       step "add" [traceActive active]
     traceMsg (NewEquation eqn) =
       step "hard" [traceEqn eqn]
@@ -839,7 +925,7 @@
           (cfg_proof_presentation config){cfg_all_lemmas = True}
         | otherwise =
           cfg_proof_presentation config
-      pres = present cfg_present $ map (eliminateDefinitionsFromGoal defs) $ solutions state
+      pres = present cfg_present [] $ map (eliminateDefinitionsFromGoal defs) $ solutions state
 
     sayTrace ""
     forM_ (pres_axioms pres) $ \p ->
@@ -926,7 +1012,7 @@
       print $ pPrintProof $
         map pre_form axioms0 ++
         map pre_form goals0 ++
-        [ Input "rule" (Jukebox.Ax Jukebox.Axiom) Unknown $
+        [ Input Nothing "rule" (Jukebox.Ax Jukebox.Axiom) Unknown $
             toForm $ clause
               [Pos (jukeboxTerm ctx (lhs rule) Jukebox.:=: jukeboxTerm ctx (rhs rule))]
         | rule <- rules state ]
@@ -941,6 +1027,10 @@
     forM_ actives $ \active ->
       putStrLn ("  " ++ prettyShow (canonicalise (active_rule active)))
     putStrLn ""
+    
+    when flags_proof_on_saturation $ do
+      let pres = present (cfg_proof_presentation config) (map active_proof actives) []
+      print $ pPrintPresentation (cfg_proof_presentation config) pres
 
   return $
     if solved state then Unsat Unsatisfiable Nothing
@@ -959,6 +1049,7 @@
   Problem Form
 presentToJukebox ctx toEquation axioms goals Presentation{..} =
   [ Input {
+      ident = Nothing,
       tag = pg_name,
       kind = Jukebox.Ax Jukebox.Axiom,
       what = false,
@@ -973,11 +1064,15 @@
   where
     axiom_proofs =
       Map.fromList
-        [ (axiom_number, fromJust (lookup axiom_number axioms))
+        [ (axiom_number, (fromJust (lookup axiom_number axioms)) { ident = Just (ident axiom_number) })
         | Axiom{..} <- pres_axioms ]
+      where
+        ident i = variant "axiom" [i]
 
     lemma_proofs =
-      Map.fromList [(p, tstp p) | p <- pres_lemmas]
+      Map.fromList [(p, (tstp p) { ident = Just (ident i) }) | (i, p) <- zip [0..] pres_lemmas]
+      where
+        ident i = variant "lemma" [i :: Int]
 
     goal_proofs =
       Map.fromList [(pg_number, tstp pg_proof) | ProvedGoal{..} <- pres_goals]
@@ -988,6 +1083,7 @@
     deriv :: Derivation Constant -> Input Form
     deriv p =
       Input {
+        ident = Nothing,
         tag = "step",
         kind = Jukebox.Ax Jukebox.Axiom,
         what = jukeboxEquation (equation (certify p)),
@@ -1062,8 +1158,12 @@
              (runTwee <$> globalFlags <*> tstpFlags <*> expert hornFlags <*> parsePrecedence)))
   profile
   where
+    getHint Input{what = Clause (Bind _ [Pos (Tru (hint :@: [t]))])}
+      | base (name hint) == "$hint" = Left t
+    getHint c = Right c
     combine horn config cpConfig main encode prove later prob0 = do
-      res <- horn prob0
+      let (hints, nonHints) = partitionEithers (map getHint prob0)
+      res <- horn nonHints
       case res of
         Left ans -> return ans
         Right prob -> do
@@ -1073,4 +1173,4 @@
             isUnitEquality _ = False
             isUnit = all isUnitEquality (map (toLiterals . what) prob0)
             main' = if isUnit then main{flags_explain_encoding = False} else main{flags_formal_proof = False}
-          encode prob >>= prove config cpConfig main' later
+          encode prob >>= prove config cpConfig main' later hints
diff --git a/misc/BestTwee.hs b/misc/BestTwee.hs
--- a/misc/BestTwee.hs
+++ b/misc/BestTwee.hs
@@ -83,24 +83,24 @@
 bonuses :: [(String, (Int, Int, Int, Int, Int, Int))]
 bonuses =
   [("no bonus", (1, 1, 1, 1, 1, 1)),
-   ("low bonus", (1, 1, 2, 3, 5, 10)),
-   --("medium bonus", (1, 2, 4, 6, 8, 10)),
+   --("low bonus", (1, 1, 2, 3, 5, 10)),
+   ("medium bonus", (1, 2, 4, 6, 8, 10)),
    --("high bonus", (0, 1, 2, 3, 4, 5)),
    --("big fish", (0, 0, 0, 0, 1, 1)),
    ("rating 1", (0, 0, 0, 0, 0, 1))]
 
 readResults ok = do
-  filenames <- glob "/home/nick/writing/twee/times/*-twee-casc-extra-*"
+  filenames <- glob "/home/nick/twee-out/*/times"
   fmap (filter (\(x, _) -> x `notElem` banned)) $ forM filenames $ \filename -> do
-    let name = takeFileName filename
+    let name = takeFileName (takeDirectory filename)
     let unpack xs = (takeBaseName name, read time :: Double) where [name, time] = words xs
     solved <- filter (ok . fst) . map unpack . lines <$> readFile filename
     let solvedInTime t = [name | (name, time) <- solved, time < t]
 --    fast <- filterM (solvedInTime 120 directory) solved
 --    med  <- filterM (solvedInTime 240 directory) solved
 --    slow <- filterM (solvedInTime 600 directory) solved
-    let fast = solvedInTime 210
-    let med  = solvedInTime 300
+    let fast = solvedInTime 120
+    let med  = solvedInTime 210
     let slow = solvedInTime (1/0)
     
     return (name, (fast, med, slow))
@@ -117,8 +117,8 @@
     find x = fromJust (lookup x results)
 
 main = do
-  probs <- lines <$> readFile "unsat"
-  results <- readResults (`elem` probs)
+  --probs <- lines <$> readFile "unsat"
+  results <- readResults (const True) -- `elem` probs)
   let
     options =
       [("fast", \(fast, _, _) -> (fast, [], [])),
@@ -140,7 +140,7 @@
         best = greedy results1
 
       putStrLn (option ++ "/" ++ bonus ++ ":")
-      forM_ (take 6 $ zip3 [1..] best (inits best)) $ \(i, name, names) -> do
+      forM_ (take 8 $ zip3 [1..] best (inits best)) $ \(i, name, names) -> do
         putStrLn (show i ++ ". " ++ name ++ " " ++ show (score results1 (name:names)) ++ ", useful at levels " ++ show (drop (length fixed) $ levels results1 name names))
 
       putStrLn ""
@@ -167,7 +167,11 @@
         Nothing -> Left (length probs)
 
 fixed :: [String]
-fixed = fixed_new
+fixed = [
+  "twee-250707-casc---lhs-weight-1---flip-ordering---normalise-queue-percent-10---cp-renormalise-threshold-10---complete-subsets---ground-joining-incomplete-limit-15",
+  "twee-250707-casc---no-flatten-goal---ground-joining-incomplete-limit-15"
+  ]
+
 fixed_new = take 6 [
   "twee-210619-twee-casc-extra-lhsnormal-flatten",
   "twee-210619-twee-casc-extra-lhs9-flip-nogoal-kbo0",
diff --git a/tests/KLE125+1.p b/tests/KLE125+1.p
new file mode 100644
--- /dev/null
+++ b/tests/KLE125+1.p
@@ -0,0 +1,47 @@
+%------------------------------------------------------------------------------
+% File     : KLE125+1 : TPTP v9.0.0. Released v4.0.0.
+% Domain   : Kleene Algebra (Modal with Divergence)
+% Problem  : Quasicommutation theorem
+% Version  : [Hoe08] axioms.
+% English  : If x quasicommutes over y, then x+y terminates if x and y
+%            individually do.
+
+% Refs     : [BD86]  Bachmair & Dershowitz (1986), Commutation, Transformat
+%          : [Str07] Struth (2007), Reasoning Automatically about Terminati
+%          : [Hoe08] Hoefner (2008), Email to G. Sutcliffe
+% Source   : [Hoe08]
+% Names    :
+
+% Status   : Theorem
+% Rating   : 1.00 v4.0.0
+% Syntax   : Number of formulae    :   29 (  26 unt;   0 def)
+%            Number of atoms       :   33 (  32 equ)
+%            Maximal formula atoms :    3 (   1 avg)
+%            Number of connectives :    4 (   0   ~;   0   |;   0   &)
+%                                         (   2 <=>;   2  =>;   0  <=;   0 <~>)
+%            Maximal formula depth :    5 (   3 avg)
+%            Maximal term depth    :    6 (   2 avg)
+%            Number of predicates  :    2 (   1 usr;   0 prp; 2-2 aty)
+%            Number of functors    :   16 (  16 usr;   2 con; 0-2 aty)
+%            Number of variables   :   49 (  49   !;   0   ?)
+% SPC      : FOF_THM_RFO_SEQ
+
+% Comments : An abstract version of a theorem in [BD86].
+%          : Equational encoding
+%------------------------------------------------------------------------------
+%---Include axioms for modal Kleene algebra with divergence
+include('Axioms/KLE001+0.ax').
+%---Include axioms for Boolean domain/codomain
+include('Axioms/KLE001+4.ax').
+%---Include axioms for diamond and boxes
+include('Axioms/KLE001+6.ax').
+%---Include axioms for divergence
+include('Axioms/KLE001+7.ax').
+%------------------------------------------------------------------------------
+fof(goals,conjecture,
+    ! [X0,X1] :
+      ( addition(multiplication(X0,X1),multiplication(X1,star(addition(X1,X0)))) = multiplication(X1,star(addition(X1,X0)))
+     => ( divergence(addition(X1,X0)) = zero
+      <= addition(divergence(X1),divergence(X0)) = zero ) ) ).
+
+%------------------------------------------------------------------------------
diff --git a/tests/ROB001-1-a.p b/tests/ROB001-1-a.p
new file mode 100644
--- /dev/null
+++ b/tests/ROB001-1-a.p
@@ -0,0 +1,42 @@
+%------------------------------------------------------------------------------
+% File     : ROB001-1 : TPTP v9.0.0. Released v1.0.0.
+% Domain   : Robbins Algebra
+% Problem  : Is every Robbins algebra Boolean?
+% Version  : [Win90] (equality) axioms.
+% English  :
+
+% Refs     : [HMT71] Henkin et al. (1971), Cylindrical Algebras
+%          : [Win90] Winker (1990), Robbins Algebra: Conditions that make a
+% Source   : [TPTP]
+% Names    :
+
+% Status   : Unsatisfiable
+% Rating   : 1.00 v2.0.0
+% Syntax   : Number of clauses     :    4 (   4 unt;   0 nHn;   1 RR)
+%            Number of literals    :    4 (   4 equ;   1 neg)
+%            Maximal clause size   :    1 (   1 avg)
+%            Maximal term depth    :    6 (   2 avg)
+%            Number of predicates  :    1 (   0 usr;   0 prp; 2-2 aty)
+%            Number of functors    :    4 (   4 usr;   2 con; 0-2 aty)
+%            Number of variables   :    7 (   0 sgn)
+% SPC      : CNF_UNS_RFO_PEQ_UEQ
+
+% Comments : Commutativity, associativity, and Huntington's axiom axiomatize 
+%            Boolean algebra.
+%------------------------------------------------------------------------------
+%----Include axioms for Robbins algebra
+include('Axioms/ROB001-0.ax').
+%------------------------------------------------------------------------------
+cnf(prove_huntingtons_axiom,negated_conjecture,
+    add(negate(add(a,negate(b))),negate(add(negate(a),negate(b)))) != b ).
+
+%------------------------------------------------------------------------------
+
+cnf(sos04,axiom,(
+    g(A) = inv(add(A,inv(A))) )).
+
+%----Definition of h
+%cnf(sos05,axiom,(
+%    h(A) = add(A,add(A,add(A,inv(add(A,inv(A)))))))).
+cnf(sos05,axiom,(
+    $hint(add(A,add(A,add(A,g(A))))))).
diff --git a/tests/ROB007-1-b.p b/tests/ROB007-1-b.p
new file mode 100644
--- /dev/null
+++ b/tests/ROB007-1-b.p
@@ -0,0 +1,12 @@
+cnf(commutativity_of_add, axiom, add(X, Y)=add(Y, X)).
+cnf(associativity_of_add, axiom, add(add(X, Y), Z)=add(X, add(Y, Z))).
+cnf(robbins_axiom, axiom, inv(add(inv(add(X, Y)), inv(add(X, inv(Y)))))=X).
+cnf(condition, hypothesis, inv(add(a, b))=inv(b)).
+cnf(prove_huntingtons_axiom, negated_conjecture, add(inv(add(a, inv(b))), inv(add(inv(a), inv(b))))!=b).
+
+cnf(sos04,axiom,(
+    $hint(inv(add(A,inv(A)))) )).
+
+%----Definition of h
+cnf(sos05,axiom,(
+    $hint(add(A,add(A,add(A,inv(add(A,inv(A))))))))).
diff --git a/tests/aim.p b/tests/aim.p
--- a/tests/aim.p
+++ b/tests/aim.p
@@ -35,21 +35,21 @@
 
 % aK (or "single-a") goals
 cnf(ka, conjecture,
-  k(a(X,Y,Z),U) = '1').
+  k(a(x,y,z),u) = '1').
 cnf(aK1, conjecture,
-  a(k(X,Y),Z,U) = '1').
+  a(k(x,y),z,u) = '1').
 cnf(aK2, conjecture,
-  a(X,k(Y,Z),U) = '1').
+  a(x,k(y,z),u) = '1').
 cnf(aK3, conjecture,
-  a(X,Y,k(Z,U)) = '1').
+  a(x,y,k(z,u)) = '1').
 
 % aa (or "double-a") goals
 cnf(aa1, conjecture,
-  a(a(X,Y,Z),U,W) = '1').
+  a(a(x,y,z),u,w) = '1').
 cnf(aa2, conjecture,
-  a(X,a(Y,Z,U),W) = '1').
+  a(x,a(y,z,u),w) = '1').
 cnf(aa3, conjecture,
-  a(X,Y,a(Z,U,W)) = '1').
+  a(x,y,a(z,u,w)) = '1').
 
 %cnf(everything, conjecture,
 %  k(a(X,Y,Z),U) = '1' |
diff --git a/tests/nicomachus-tptp-2.p b/tests/nicomachus-tptp-2.p
new file mode 100644
--- /dev/null
+++ b/tests/nicomachus-tptp-2.p
@@ -0,0 +1,19 @@
+cnf(plus_comm, axiom, plus(X, Y)=plus(Y, X)).
+cnf(plus_assoc, axiom, plus(X, plus(Y, Z))=plus(plus(X, Y), Z)).
+cnf(times_comm, axiom, times(X, Y)=times(Y, X)).
+cnf(times_assoc, axiom, times(X, times(Y, Z))=times(times(X, Y), Z)).
+cnf(plus_zero, axiom, plus(X, zero)=X).
+cnf(times_zero, axiom, times(X, zero)=zero).
+cnf(times_one, axiom, times(X, one)=X).
+cnf(distr, axiom, times(X, plus(Y, Z))=plus(times(X, Y), times(X, Z))).
+cnf(distr, axiom, times(plus(X, Y), Z)=plus(times(X, Z), times(Y, Z))).
+cnf(plus_s, axiom, plus(s(X), Y)=s(plus(X, Y))).
+cnf(times_s, axiom, times(s(X), Y)=plus(Y, times(X, Y))).
+cnf(sum_zero, axiom, sum(zero)=zero).
+cnf(sum_s, axiom, sum(s(N))=plus(s(N), sum(N))).
+cnf(cubes_zero, axiom, cubes(zero)=zero).
+cnf(cubes_s, axiom, cubes(s(N))=plus(times(s(N), times(s(N), s(N))), cubes(N))).
+cnf(plus_sum_step_1, axiom, plus(sum(zero), sum(zero))!=times(zero, s(zero)) | plus(sum(ih_a), sum(ih_a))=times(ih_a, s(ih_a))).
+cnf(plus_sum, axiom, plus(sum(zero), sum(zero))!=times(zero, s(zero)) | plus(sum(s(ih_a)), sum(s(ih_a)))!=times(s(ih_a), s(s(ih_a))) | plus(sum(N), sum(N))=times(N, s(N))).
+cnf(ih, axiom, times(sum(a), sum(a))=cubes(a)).
+cnf(conjecture, negated_conjecture, times(sum(s(a)), sum(s(a)))!=cubes(s(a))).
diff --git a/tests/nicomachus-tptp.p b/tests/nicomachus-tptp.p
new file mode 100644
--- /dev/null
+++ b/tests/nicomachus-tptp.p
@@ -0,0 +1,20 @@
+cnf(plus_comm, axiom, plus(X, Y)=plus(Y, X)).
+cnf(plus_assoc, axiom, plus(X, plus(Y, Z))=plus(plus(X, Y), Z)).
+cnf(times_comm, axiom, times(X, Y)=times(Y, X)).
+cnf(times_assoc, axiom, times(X, times(Y, Z))=times(times(X, Y), Z)).
+cnf(plus_zero, axiom, plus(X, zero)=X).
+cnf(times_zero, axiom, times(X, zero)=zero).
+cnf(times_one, axiom, times(X, one)=X).
+cnf(distr, axiom, times(X, plus(Y, Z))=plus(times(X, Y), times(X, Z))).
+cnf(distr, axiom, times(plus(X, Y), Z)=plus(times(X, Z), times(Y, Z))).
+cnf(plus_s, axiom, plus(s(X), Y)=s(plus(X, Y))).
+cnf(times_s, axiom, times(s(X), Y)=plus(Y, times(X, Y))).
+cnf(sum_zero, axiom, sum(zero)=zero).
+cnf(sum_s, axiom, sum(s(N))=plus(s(N), sum(N))).
+cnf(cubes_zero, axiom, cubes(zero)=zero).
+cnf(cubes_s, axiom, cubes(s(N))=plus(times(s(N), times(s(N), s(N))), cubes(N))).
+%cnf(plus_sum, axiom, plus(sum(N), sum(N))=times(N, s(N))).
+cnf(plus_sum_step_1, axiom, plus(sum(zero), sum(zero)) = times(zero, s(zero)) => plus(sum(ih_a), sum(ih_a)) = times(ih_a, s(ih_a))).
+cnf(plus_sum, axiom, (plus(sum(zero), sum(zero)) = times(zero, s(zero)) & plus(sum(s(ih_a)), sum(s(ih_a))) = times(s(ih_a), s(s(ih_a)))) => plus(sum(N),sum(N))=times(N,s(N))).
+cnf(ih, axiom, times(sum(a), sum(a))=cubes(a)).
+cnf(conjecture, negated_conjecture, times(sum(s(a)), sum(s(a)))!=cubes(s(a))).
diff --git a/tests/nicomachus2.p b/tests/nicomachus2.p
new file mode 100644
--- /dev/null
+++ b/tests/nicomachus2.p
@@ -0,0 +1,36 @@
+cnf(plus_comm, axiom,
+    X + Y = Y + X).
+cnf(plus_assoc, axiom,
+    X + (Y + Z) = (X + Y) + Z).
+cnf(times_comm, axiom,
+    X * Y = Y * X).
+cnf(times_assoc, axiom,
+    X * (Y * Z) = (X * Y) * Z).
+cnf(plus_zero, axiom,
+    X + zero = X).
+cnf(times_zero, axiom,
+    X * zero = zero).
+cnf(times_one, axiom,
+    X * one = X).
+cnf(distr, axiom,
+    X * (Y + Z) = (X * Y) + (X * Z)).
+cnf(distr, axiom,
+    (X + Y) * Z = (X * Z) + (Y * Z)).
+cnf(plus_s, axiom,
+    s(X) + Y = s(X+Y)).
+cnf(times_s, axiom,
+    s(X)*Y = Y + (X*Y)).
+cnf(sum_zero, axiom,
+    sum(zero) = zero).
+cnf(sum_s, axiom,
+    sum(s(N)) = s(N) + sum(N)).
+cnf(cubes_zero, axiom,
+    cubes(zero) = zero).
+cnf(cubes_s, axiom,
+    cubes(s(N)) = (s(N) * (s(N) * s(N))) + cubes(N)).
+cnf(plus_sum, axiom,
+    sum(N) + sum(N) = N * s(N)).
+cnf(ih, axiom,
+    sum(a) * sum(a) = cubes(a)).
+cnf(conjecture, conjecture,
+    sum(s(a)) * sum(s(a)) = cubes(s(a))).
diff --git a/tests/rob.p b/tests/rob.p
new file mode 100644
--- /dev/null
+++ b/tests/rob.p
@@ -0,0 +1,7 @@
+cnf(commutativity_of_add, axiom, add(X, Y)=add(Y, X)).
+cnf(associativity_of_add, axiom,
+    add(add(X, Y), Z)=add(X, add(Y, Z))).
+cnf(robbins_axiom, axiom,
+    negate(add(negate(add(X, Y)), negate(add(X, negate(Y)))))=X).
+cnf(winker_specialised, conjecture,
+    add(add(x,x), negate(add(negate(add(x,add(x,x))),x))) = add(x,x)).
diff --git a/tests/rob2.p b/tests/rob2.p
new file mode 100644
--- /dev/null
+++ b/tests/rob2.p
@@ -0,0 +1,7 @@
+cnf(commutativity_of_add, axiom, add(X, Y)=add(Y, X)).
+cnf(associativity_of_add, axiom,
+    add(add(X, Y), Z)=add(X, add(Y, Z))).
+cnf(robbins_axiom, axiom,
+    negate(add(negate(add(X, Y)), negate(add(X, negate(Y)))))=X).
+fof(winker, conjecture,
+    ?[X,Y]: add(X,Y) = X).
diff --git a/tests/sum.p b/tests/sum.p
new file mode 100644
--- /dev/null
+++ b/tests/sum.p
@@ -0,0 +1,30 @@
+cnf(plus_comm, axiom,
+    X + Y = Y + X).
+cnf(plus_assoc, axiom,
+    X + (Y + Z) = (X + Y) + Z).
+cnf(times_comm, axiom,
+    X * Y = Y * X).
+cnf(times_assoc, axiom,
+    X * (Y * Z) = (X * Y) * Z).
+cnf(plus_zero, axiom,
+    X + zero = X).
+cnf(times_zero, axiom,
+    X * zero = zero).
+cnf(times_one, axiom,
+    X * one = X).
+cnf(distr, axiom,
+    X * (Y + Z) = (X * Y) + (X * Z)).
+cnf(distr, axiom,
+    (X + Y) * Z = (X * Z) + (Y * Z)).
+cnf(plus_s, axiom,
+    s(X) + Y = s(X+Y)).
+cnf(times_s, axiom,
+    s(X)*Y = Y + (X*Y)).
+cnf(sum_zero, axiom,
+    sum(zero) = zero).
+cnf(sum_s, axiom,
+    sum(s(N)) = s(N) + sum(N)).
+cnf(ih, axiom,
+    sum(a) + sum(a) = a * s(a)).
+cnf(conjecture, conjecture,
+    sum(s(a)) + sum(s(a)) = s(a) * s(s(a))).
diff --git a/tests/wos.p b/tests/wos.p
new file mode 100644
--- /dev/null
+++ b/tests/wos.p
@@ -0,0 +1,6 @@
+cnf(a, axiom,
+    prod(inv(prod(inv(prod(inv(prod(Xl,X2)),prod(X2,Xl))),prod(inv(prod(Z,Y)), prod(Z,inv(prod(prod(V,inv(X)),inv(Y))))))),X) = V).
+
+%fof(associativity, conjecture, prod(a,prod(b,c)) = prod(prod(a,b),c)).
+fof(identity_and_inverse, conjecture,  ?[X]: (![Y]: prod(X,Y)=Y & ![Y]: prod(Y, inv(Y)) = X)).
+%fof(commutativity, conjecture, prod(a,b) = prod(b,a)).
diff --git a/twee.cabal b/twee.cabal
--- a/twee.cabal
+++ b/twee.cabal
@@ -1,5 +1,5 @@
 name:                twee
-version:             2.5
+version:             2.6.1
 synopsis:            An equational theorem prover
 homepage:            http://github.com/nick8325/twee
 license:             BSD3
@@ -25,7 +25,7 @@
 
 source-repository head
   type:     git
-  location: git://github.com/nick8325/twee.git
+  location: https://github.com/nick8325/twee.git
   branch:   master
 
 flag static
@@ -44,17 +44,22 @@
   manual: True
 
 executable twee
+  --if flag(parallel)
+  --  main-is: ParallelMain.hs
+  --  build-depends: async, unix
+  --  c-sources: executable/link.c
+  --else
   main-is: Main.hs
 
   hs-source-dirs:      executable
   other-modules:       SequentialMain
   default-language:    Haskell2010
   build-depends:       base < 5,
-                       twee-lib == 2.5,
+                       twee-lib == 2.6.1,
                        containers,
                        pretty,
                        split,
-                       jukebox >= 0.5.4,
+                       jukebox >= 0.5.9,
                        ansi-terminal >= 0.9,
                        symbol
   ghc-options:         -W -fno-warn-incomplete-patterns
@@ -71,7 +76,7 @@
     hs-source-dirs:
         misc
     main-is: Test.hs
-    build-depends: base < 5, QuickCheck, twee-lib == 2.5, containers, pretty
+    build-depends: base < 5, QuickCheck, twee-lib == 2.6.1, containers, pretty
     ghc-options:
       -threaded
       -rtsopts