diff --git a/.gitignore b/.gitignore
--- a/.gitignore
+++ b/.gitignore
@@ -82,6 +82,7 @@
 eg/tauts
 eg/tuples
 eg/oddeven
+bench/addition
 bench/expressions
 bench/representatives
 bench/representatives2
diff --git a/Makefile b/Makefile
--- a/Makefile
+++ b/Makefile
@@ -15,6 +15,9 @@
   $(shell grep -q "Arch Linux" /etc/lsb-release && echo --optghc=-dynamic --optghc=-package=cmdargs --optghc=-package=regex-tdfa --optghc=-package=algebraic-graphs)
 MAXTESTS = 4000
 MAXSIZE = -s4
+# Sets the number of jobs to the the number of processors minus one.
+NJOBS := $(shell grep ^processor /proc/cpuinfo | head -n -1 | wc -l | sed 's/^0$$/1/')
+LONG := $(shell which long >/dev/null 2>/dev/null && echo long)
 TESTS = \
   test/creason \
   test/engine \
@@ -47,6 +50,7 @@
   eg/monad \
   eg/tuples \
   eg/speculate-reason \
+  bench/addition \
   bench/arithficial \
   bench/lowtests \
   bench/nord \
@@ -108,6 +112,15 @@
 
 test-via-stack:
 	stack test speculate:test:engine --ghc-options="$(GHCFLAGS) -O0" --system-ghc --no-install-ghc --no-terminal
+
+fastest:
+	$(LONG) make test -j$(NJOBS)
+
+fastestbench:
+	$(LONG) make test -j$(NJOBS) && $(LONG) make bench
+
+fastxtestbench:
+	$(LONG) make txt -j$(NJOBS) && $(LONG) make test -j$(NJOBS) && $(LONG) make bench
 
 legacy-test:
 	make clean  &&  make -j8 GHC=ghc-8.2   &&  make quick-test -j8 GHC=ghc-8.2
diff --git a/bench/addition.hs b/bench/addition.hs
new file mode 100644
--- /dev/null
+++ b/bench/addition.hs
@@ -0,0 +1,13 @@
+import Test.Speculate
+
+main :: IO ()
+main = speculate args
+  { maxSize = 7
+  , showTheory = True
+  , showSemiequations = False
+  , showConditions = False
+  , constants =
+      [ showConstant (0::Int)
+      , constant "+"  ((+) :: Int -> Int -> Int)
+      ]
+  }
diff --git a/bench/addition.txt b/bench/addition.txt
new file mode 100644
--- /dev/null
+++ b/bench/addition.txt
@@ -0,0 +1,31 @@
+max expr size  =    7
+  |- on ineqs  =    6
+  |- on conds  =    6
+max  #-tests   =  500
+max  #-vars    =    2  (for inequational and conditional laws)
+
+_ :: Int
+0 :: Int
+(+) :: Int -> Int -> Int
+
+rules:
+x + 0 == x
+0 + x == x
+(x + y) + z == x + (y + z)
+(x + y) + z == y + (x + z)
+equations:
+y + x == x + y
+y + (x + z) == x + (y + z)
+z + (x + y) == x + (y + z)
+z + (y + x) == x + (y + z)
+y + (x + (x' + z)) == x + (y + (z + x'))
+z + (x + (y + x')) == x + (y + (z + x'))
+z + (y + (x + x')) == x + (y + (z + x'))
+z + (x' + (x + y)) == x + (y + (z + x'))
+x' + (y + (z + x)) == x + (y + (z + x'))
+x' + (z + (y + x)) == x + (y + (z + x'))
+
+      x + 0 == x
+      x + y == y + x
+(x + y) + z == x + (y + z)
+
diff --git a/bench/list-t.txt b/bench/list-t.txt
--- a/bench/list-t.txt
+++ b/bench/list-t.txt
@@ -22,6 +22,7 @@
 equations:
 head (xs ++ (x:zs)) == head (xs ++ (x:ys))
 head (xs ++ [x]) == head (xs ++ (x:ys))
+head (xs ++ (x:tail [])) == head (xs ++ (x:ys))
 
         head (x:xs) == x
 head (xs ++ (x:ys)) == head (xs ++ (x:zs))
diff --git a/bench/runtime/lapmatrud/bench/addition.runtime b/bench/runtime/lapmatrud/bench/addition.runtime
new file mode 100644
--- /dev/null
+++ b/bench/runtime/lapmatrud/bench/addition.runtime
@@ -0,0 +1,1 @@
+0.22
diff --git a/bench/runtime/lapmatrud/bench/arith-c.runtime b/bench/runtime/lapmatrud/bench/arith-c.runtime
new file mode 100644
--- /dev/null
+++ b/bench/runtime/lapmatrud/bench/arith-c.runtime
@@ -0,0 +1,1 @@
+0.35
diff --git a/bench/runtime/lapmatrud/bench/arith-t.runtime b/bench/runtime/lapmatrud/bench/arith-t.runtime
new file mode 100644
--- /dev/null
+++ b/bench/runtime/lapmatrud/bench/arith-t.runtime
@@ -0,0 +1,1 @@
+6.58
diff --git a/bench/runtime/lapmatrud/bench/arithficial.runtime b/bench/runtime/lapmatrud/bench/arithficial.runtime
--- a/bench/runtime/lapmatrud/bench/arithficial.runtime
+++ b/bench/runtime/lapmatrud/bench/arithficial.runtime
@@ -1,1 +1,1 @@
-0.37
+0.24
diff --git a/bench/runtime/lapmatrud/bench/bool-c.runtime b/bench/runtime/lapmatrud/bench/bool-c.runtime
new file mode 100644
--- /dev/null
+++ b/bench/runtime/lapmatrud/bench/bool-c.runtime
@@ -0,0 +1,1 @@
+1.26
diff --git a/bench/runtime/lapmatrud/bench/list-c.runtime b/bench/runtime/lapmatrud/bench/list-c.runtime
new file mode 100644
--- /dev/null
+++ b/bench/runtime/lapmatrud/bench/list-c.runtime
@@ -0,0 +1,1 @@
+0.94
diff --git a/bench/runtime/lapmatrud/bench/list-t.runtime b/bench/runtime/lapmatrud/bench/list-t.runtime
new file mode 100644
--- /dev/null
+++ b/bench/runtime/lapmatrud/bench/list-t.runtime
@@ -0,0 +1,1 @@
+0.24
diff --git a/bench/runtime/lapmatrud/bench/minus-c.runtime b/bench/runtime/lapmatrud/bench/minus-c.runtime
new file mode 100644
--- /dev/null
+++ b/bench/runtime/lapmatrud/bench/minus-c.runtime
@@ -0,0 +1,1 @@
+0.51
diff --git a/bench/runtime/lapmatrud/bench/stats.runtime b/bench/runtime/lapmatrud/bench/stats.runtime
new file mode 100644
--- /dev/null
+++ b/bench/runtime/lapmatrud/bench/stats.runtime
@@ -0,0 +1,1 @@
+0.16
diff --git a/bench/runtime/lapmatrud/eg/arith-negate-abs.runtime b/bench/runtime/lapmatrud/eg/arith-negate-abs.runtime
--- a/bench/runtime/lapmatrud/eg/arith-negate-abs.runtime
+++ b/bench/runtime/lapmatrud/eg/arith-negate-abs.runtime
@@ -1,1 +1,1 @@
-0.92
+1.02
diff --git a/bench/runtime/lapmatrud/eg/arith.runtime b/bench/runtime/lapmatrud/eg/arith.runtime
--- a/bench/runtime/lapmatrud/eg/arith.runtime
+++ b/bench/runtime/lapmatrud/eg/arith.runtime
@@ -1,1 +1,1 @@
-0.14
+0.16
diff --git a/bench/runtime/lapmatrud/eg/binarytree.runtime b/bench/runtime/lapmatrud/eg/binarytree.runtime
--- a/bench/runtime/lapmatrud/eg/binarytree.runtime
+++ b/bench/runtime/lapmatrud/eg/binarytree.runtime
@@ -1,1 +1,1 @@
-0.90
+1.00
diff --git a/bench/runtime/lapmatrud/eg/binarytree0.runtime b/bench/runtime/lapmatrud/eg/binarytree0.runtime
--- a/bench/runtime/lapmatrud/eg/binarytree0.runtime
+++ b/bench/runtime/lapmatrud/eg/binarytree0.runtime
@@ -1,1 +1,1 @@
-0.28
+0.31
diff --git a/bench/runtime/lapmatrud/eg/bool.runtime b/bench/runtime/lapmatrud/eg/bool.runtime
--- a/bench/runtime/lapmatrud/eg/bool.runtime
+++ b/bench/runtime/lapmatrud/eg/bool.runtime
@@ -1,1 +1,1 @@
-1.05
+1.43
diff --git a/bench/runtime/lapmatrud/eg/colour.runtime b/bench/runtime/lapmatrud/eg/colour.runtime
--- a/bench/runtime/lapmatrud/eg/colour.runtime
+++ b/bench/runtime/lapmatrud/eg/colour.runtime
@@ -1,1 +1,1 @@
-1.07
+1.16
diff --git a/bench/runtime/lapmatrud/eg/digraphs.runtime b/bench/runtime/lapmatrud/eg/digraphs.runtime
--- a/bench/runtime/lapmatrud/eg/digraphs.runtime
+++ b/bench/runtime/lapmatrud/eg/digraphs.runtime
@@ -1,1 +1,1 @@
-0.80
+0.90
diff --git a/bench/runtime/lapmatrud/eg/fun.runtime b/bench/runtime/lapmatrud/eg/fun.runtime
--- a/bench/runtime/lapmatrud/eg/fun.runtime
+++ b/bench/runtime/lapmatrud/eg/fun.runtime
@@ -1,1 +1,1 @@
-0.58
+0.64
diff --git a/bench/runtime/lapmatrud/eg/insertsort.runtime b/bench/runtime/lapmatrud/eg/insertsort.runtime
--- a/bench/runtime/lapmatrud/eg/insertsort.runtime
+++ b/bench/runtime/lapmatrud/eg/insertsort.runtime
@@ -1,1 +1,1 @@
-4.08
+4.47
diff --git a/bench/runtime/lapmatrud/eg/insertsort0.runtime b/bench/runtime/lapmatrud/eg/insertsort0.runtime
--- a/bench/runtime/lapmatrud/eg/insertsort0.runtime
+++ b/bench/runtime/lapmatrud/eg/insertsort0.runtime
@@ -1,1 +1,1 @@
-0.52
+0.55
diff --git a/bench/runtime/lapmatrud/eg/length.runtime b/bench/runtime/lapmatrud/eg/length.runtime
--- a/bench/runtime/lapmatrud/eg/length.runtime
+++ b/bench/runtime/lapmatrud/eg/length.runtime
@@ -1,1 +1,1 @@
-0.25
+0.14
diff --git a/bench/runtime/lapmatrud/eg/list.runtime b/bench/runtime/lapmatrud/eg/list.runtime
--- a/bench/runtime/lapmatrud/eg/list.runtime
+++ b/bench/runtime/lapmatrud/eg/list.runtime
@@ -1,1 +1,1 @@
-1.38
+1.51
diff --git a/bench/runtime/lapmatrud/eg/minus.runtime b/bench/runtime/lapmatrud/eg/minus.runtime
--- a/bench/runtime/lapmatrud/eg/minus.runtime
+++ b/bench/runtime/lapmatrud/eg/minus.runtime
@@ -1,1 +1,1 @@
-0.34
+0.30
diff --git a/bench/runtime/lapmatrud/eg/monad.runtime b/bench/runtime/lapmatrud/eg/monad.runtime
--- a/bench/runtime/lapmatrud/eg/monad.runtime
+++ b/bench/runtime/lapmatrud/eg/monad.runtime
@@ -1,1 +1,1 @@
-0.36
+0.37
diff --git a/bench/runtime/lapmatrud/eg/oddeven.runtime b/bench/runtime/lapmatrud/eg/oddeven.runtime
--- a/bench/runtime/lapmatrud/eg/oddeven.runtime
+++ b/bench/runtime/lapmatrud/eg/oddeven.runtime
@@ -1,1 +1,1 @@
-3.56
+3.90
diff --git a/bench/runtime/lapmatrud/eg/plus-abs.runtime b/bench/runtime/lapmatrud/eg/plus-abs.runtime
--- a/bench/runtime/lapmatrud/eg/plus-abs.runtime
+++ b/bench/runtime/lapmatrud/eg/plus-abs.runtime
@@ -1,1 +1,1 @@
-1.94
+2.17
diff --git a/bench/runtime/lapmatrud/eg/ratio.runtime b/bench/runtime/lapmatrud/eg/ratio.runtime
--- a/bench/runtime/lapmatrud/eg/ratio.runtime
+++ b/bench/runtime/lapmatrud/eg/ratio.runtime
@@ -1,1 +1,1 @@
-4.39
+4.87
diff --git a/bench/runtime/lapmatrud/eg/sets.runtime b/bench/runtime/lapmatrud/eg/sets.runtime
--- a/bench/runtime/lapmatrud/eg/sets.runtime
+++ b/bench/runtime/lapmatrud/eg/sets.runtime
@@ -1,1 +1,1 @@
-4.09
+4.93
diff --git a/bench/runtime/lapmatrud/eg/speculate-reason.runtime b/bench/runtime/lapmatrud/eg/speculate-reason.runtime
--- a/bench/runtime/lapmatrud/eg/speculate-reason.runtime
+++ b/bench/runtime/lapmatrud/eg/speculate-reason.runtime
@@ -1,1 +1,1 @@
-1.59
+1.62
diff --git a/bench/runtime/lapmatrud/eg/string.runtime b/bench/runtime/lapmatrud/eg/string.runtime
--- a/bench/runtime/lapmatrud/eg/string.runtime
+++ b/bench/runtime/lapmatrud/eg/string.runtime
@@ -1,1 +1,1 @@
-0.52
+0.53
diff --git a/bench/runtime/lapmatrud/eg/tauts.runtime b/bench/runtime/lapmatrud/eg/tauts.runtime
--- a/bench/runtime/lapmatrud/eg/tauts.runtime
+++ b/bench/runtime/lapmatrud/eg/tauts.runtime
@@ -1,1 +1,1 @@
-2.34
+2.32
diff --git a/bench/runtime/lapmatrud/eg/tuples.runtime b/bench/runtime/lapmatrud/eg/tuples.runtime
--- a/bench/runtime/lapmatrud/eg/tuples.runtime
+++ b/bench/runtime/lapmatrud/eg/tuples.runtime
@@ -1,1 +1,1 @@
-0.74
+0.72
diff --git a/bench/runtime/lapmatrud/eg/zip.runtime b/bench/runtime/lapmatrud/eg/zip.runtime
--- a/bench/runtime/lapmatrud/eg/zip.runtime
+++ b/bench/runtime/lapmatrud/eg/zip.runtime
@@ -1,1 +1,1 @@
-1.24
+1.39
diff --git a/bench/runtime/zero/bench/addition.runtime b/bench/runtime/zero/bench/addition.runtime
new file mode 100644
--- /dev/null
+++ b/bench/runtime/zero/bench/addition.runtime
@@ -0,0 +1,1 @@
+0.45
diff --git a/bench/runtime/zero/bench/arith-c.runtime b/bench/runtime/zero/bench/arith-c.runtime
--- a/bench/runtime/zero/bench/arith-c.runtime
+++ b/bench/runtime/zero/bench/arith-c.runtime
@@ -1,1 +1,1 @@
-0.75
+0.60
diff --git a/bench/runtime/zero/bench/arith-t.runtime b/bench/runtime/zero/bench/arith-t.runtime
--- a/bench/runtime/zero/bench/arith-t.runtime
+++ b/bench/runtime/zero/bench/arith-t.runtime
@@ -1,1 +1,1 @@
-11.26
+10.02
diff --git a/bench/runtime/zero/bench/arithficial.runtime b/bench/runtime/zero/bench/arithficial.runtime
--- a/bench/runtime/zero/bench/arithficial.runtime
+++ b/bench/runtime/zero/bench/arithficial.runtime
@@ -1,1 +1,1 @@
-0.44
+0.60
diff --git a/bench/runtime/zero/bench/bool-c.runtime b/bench/runtime/zero/bench/bool-c.runtime
--- a/bench/runtime/zero/bench/bool-c.runtime
+++ b/bench/runtime/zero/bench/bool-c.runtime
@@ -1,1 +1,1 @@
-2.14
+1.81
diff --git a/bench/runtime/zero/bench/list-c.runtime b/bench/runtime/zero/bench/list-c.runtime
--- a/bench/runtime/zero/bench/list-c.runtime
+++ b/bench/runtime/zero/bench/list-c.runtime
@@ -1,1 +1,1 @@
-1.59
+1.60
diff --git a/bench/runtime/zero/bench/list-t.runtime b/bench/runtime/zero/bench/list-t.runtime
--- a/bench/runtime/zero/bench/list-t.runtime
+++ b/bench/runtime/zero/bench/list-t.runtime
@@ -1,1 +1,1 @@
-0.43
+0.48
diff --git a/bench/runtime/zero/bench/lowtests.runtime b/bench/runtime/zero/bench/lowtests.runtime
--- a/bench/runtime/zero/bench/lowtests.runtime
+++ b/bench/runtime/zero/bench/lowtests.runtime
@@ -1,1 +1,1 @@
-0.48
+0.46
diff --git a/bench/runtime/zero/bench/minus-c.runtime b/bench/runtime/zero/bench/minus-c.runtime
--- a/bench/runtime/zero/bench/minus-c.runtime
+++ b/bench/runtime/zero/bench/minus-c.runtime
@@ -1,1 +1,1 @@
-0.90
+0.91
diff --git a/bench/runtime/zero/bench/stats.runtime b/bench/runtime/zero/bench/stats.runtime
--- a/bench/runtime/zero/bench/stats.runtime
+++ b/bench/runtime/zero/bench/stats.runtime
@@ -1,1 +1,1 @@
-0.28
+0.30
diff --git a/bench/runtime/zero/bench/trilean.runtime b/bench/runtime/zero/bench/trilean.runtime
--- a/bench/runtime/zero/bench/trilean.runtime
+++ b/bench/runtime/zero/bench/trilean.runtime
@@ -1,1 +1,1 @@
-0.04
+0.05
diff --git a/bench/runtime/zero/eg/arith-negate-abs.runtime b/bench/runtime/zero/eg/arith-negate-abs.runtime
--- a/bench/runtime/zero/eg/arith-negate-abs.runtime
+++ b/bench/runtime/zero/eg/arith-negate-abs.runtime
@@ -1,1 +1,1 @@
-1.78
+1.58
diff --git a/bench/runtime/zero/eg/arith.runtime b/bench/runtime/zero/eg/arith.runtime
--- a/bench/runtime/zero/eg/arith.runtime
+++ b/bench/runtime/zero/eg/arith.runtime
@@ -1,1 +1,1 @@
-0.28
+0.26
diff --git a/bench/runtime/zero/eg/binarytree.runtime b/bench/runtime/zero/eg/binarytree.runtime
--- a/bench/runtime/zero/eg/binarytree.runtime
+++ b/bench/runtime/zero/eg/binarytree.runtime
@@ -1,1 +1,1 @@
-1.90
+1.89
diff --git a/bench/runtime/zero/eg/binarytree0.runtime b/bench/runtime/zero/eg/binarytree0.runtime
--- a/bench/runtime/zero/eg/binarytree0.runtime
+++ b/bench/runtime/zero/eg/binarytree0.runtime
@@ -1,1 +1,1 @@
-0.53
+0.60
diff --git a/bench/runtime/zero/eg/bool.runtime b/bench/runtime/zero/eg/bool.runtime
--- a/bench/runtime/zero/eg/bool.runtime
+++ b/bench/runtime/zero/eg/bool.runtime
@@ -1,1 +1,1 @@
-2.49
+2.42
diff --git a/bench/runtime/zero/eg/digraphs.runtime b/bench/runtime/zero/eg/digraphs.runtime
--- a/bench/runtime/zero/eg/digraphs.runtime
+++ b/bench/runtime/zero/eg/digraphs.runtime
@@ -1,1 +1,1 @@
-1.54
+1.49
diff --git a/bench/runtime/zero/eg/fun.runtime b/bench/runtime/zero/eg/fun.runtime
--- a/bench/runtime/zero/eg/fun.runtime
+++ b/bench/runtime/zero/eg/fun.runtime
@@ -1,1 +1,1 @@
-1.07
+1.08
diff --git a/bench/runtime/zero/eg/insertsort.runtime b/bench/runtime/zero/eg/insertsort.runtime
--- a/bench/runtime/zero/eg/insertsort.runtime
+++ b/bench/runtime/zero/eg/insertsort.runtime
@@ -1,1 +1,1 @@
-7.74
+7.38
diff --git a/bench/runtime/zero/eg/length.runtime b/bench/runtime/zero/eg/length.runtime
--- a/bench/runtime/zero/eg/length.runtime
+++ b/bench/runtime/zero/eg/length.runtime
@@ -1,1 +1,1 @@
-0.25
+0.24
diff --git a/bench/runtime/zero/eg/minus.runtime b/bench/runtime/zero/eg/minus.runtime
--- a/bench/runtime/zero/eg/minus.runtime
+++ b/bench/runtime/zero/eg/minus.runtime
@@ -1,1 +1,1 @@
-0.52
+0.65
diff --git a/bench/runtime/zero/eg/monad.runtime b/bench/runtime/zero/eg/monad.runtime
--- a/bench/runtime/zero/eg/monad.runtime
+++ b/bench/runtime/zero/eg/monad.runtime
@@ -1,1 +1,1 @@
-0.59
+0.61
diff --git a/bench/runtime/zero/eg/oddeven.runtime b/bench/runtime/zero/eg/oddeven.runtime
--- a/bench/runtime/zero/eg/oddeven.runtime
+++ b/bench/runtime/zero/eg/oddeven.runtime
@@ -1,1 +1,1 @@
-6.87
+6.85
diff --git a/bench/runtime/zero/eg/plus-abs.runtime b/bench/runtime/zero/eg/plus-abs.runtime
--- a/bench/runtime/zero/eg/plus-abs.runtime
+++ b/bench/runtime/zero/eg/plus-abs.runtime
@@ -1,1 +1,1 @@
-3.77
+3.50
diff --git a/bench/runtime/zero/eg/ratio.runtime b/bench/runtime/zero/eg/ratio.runtime
--- a/bench/runtime/zero/eg/ratio.runtime
+++ b/bench/runtime/zero/eg/ratio.runtime
@@ -1,1 +1,1 @@
-8.34
+7.64
diff --git a/bench/runtime/zero/eg/sets.runtime b/bench/runtime/zero/eg/sets.runtime
--- a/bench/runtime/zero/eg/sets.runtime
+++ b/bench/runtime/zero/eg/sets.runtime
@@ -1,1 +1,1 @@
-7.94
+7.34
diff --git a/bench/runtime/zero/eg/speculate-reason.runtime b/bench/runtime/zero/eg/speculate-reason.runtime
--- a/bench/runtime/zero/eg/speculate-reason.runtime
+++ b/bench/runtime/zero/eg/speculate-reason.runtime
@@ -1,1 +1,1 @@
-2.98
+2.95
diff --git a/bench/runtime/zero/eg/string.runtime b/bench/runtime/zero/eg/string.runtime
--- a/bench/runtime/zero/eg/string.runtime
+++ b/bench/runtime/zero/eg/string.runtime
@@ -1,1 +1,1 @@
-0.92
+0.87
diff --git a/bench/runtime/zero/eg/tauts.runtime b/bench/runtime/zero/eg/tauts.runtime
--- a/bench/runtime/zero/eg/tauts.runtime
+++ b/bench/runtime/zero/eg/tauts.runtime
@@ -1,1 +1,1 @@
-4.12
+4.13
diff --git a/bench/runtime/zero/eg/tuples.runtime b/bench/runtime/zero/eg/tuples.runtime
--- a/bench/runtime/zero/eg/tuples.runtime
+++ b/bench/runtime/zero/eg/tuples.runtime
@@ -1,1 +1,1 @@
-1.28
+1.27
diff --git a/bench/runtime/zero/eg/zip.runtime b/bench/runtime/zero/eg/zip.runtime
--- a/bench/runtime/zero/eg/zip.runtime
+++ b/bench/runtime/zero/eg/zip.runtime
@@ -1,1 +1,1 @@
-2.38
+2.41
diff --git a/changelog.md b/changelog.md
--- a/changelog.md
+++ b/changelog.md
@@ -2,6 +2,17 @@
 =======================
 
 
+v0.4.20 (February 2024)
+-----------------------
+
+* minor changes only
+* improve `consider` by favouring the normalization
+  _only_ if it reduces the number of variables
+* revert back (v0.4.16) to using vanilla syntactic unification
+  instead of syntactic unification modulo commutativity
+* some internal refactoring
+
+
 v0.4.18 (February 2024)
 -----------------------
 
diff --git a/eg/insertsort.txt b/eg/insertsort.txt
--- a/eg/insertsort.txt
+++ b/eg/insertsort.txt
@@ -30,7 +30,7 @@
     ([] == insert x xs) == False
         (xs == sort xs) == ordered xs
        elem x (sort xs) == elem x xs
-             (xs == []) == ([] == sort xs)
+        (sort xs == []) == (xs == [])
    all (x ==) (sort xs) == all (x ==) xs
     all (x <) (sort xs) == all (x <) xs
           all (x <=) xs == ordered (x:sort xs)
diff --git a/eg/insertsort0.txt b/eg/insertsort0.txt
--- a/eg/insertsort0.txt
+++ b/eg/insertsort0.txt
@@ -22,7 +22,7 @@
 
    (xs == insert x xs) == False
    ([] == insert x xs) == False
-            (xs == []) == ([] == sort xs)
+       (sort xs == []) == (xs == [])
                sort [] == []
         sort (sort xs) == sort xs
            insert x [] == [x]
diff --git a/mk/depend.mk b/mk/depend.mk
--- a/mk/depend.mk
+++ b/mk/depend.mk
@@ -1,3 +1,36 @@
+bench/addition: \
+  bench/addition.hs \
+  mk/toplibs
+bench/addition.o: \
+  src/Test/Speculate/Utils/Tuple.hs \
+  src/Test/Speculate/Utils/Timeout.hs \
+  src/Test/Speculate/Utils/Tiers.hs \
+  src/Test/Speculate/Utils/String.hs \
+  src/Test/Speculate/Utils/PrettyPrint.hs \
+  src/Test/Speculate/Utils.hs \
+  src/Test/Speculate/Utils/Ord.hs \
+  src/Test/Speculate/Utils/Misc.hs \
+  src/Test/Speculate/Utils/Memoize.hs \
+  src/Test/Speculate/Utils/List.hs \
+  src/Test/Speculate/Utils/Digraph.hs \
+  src/Test/Speculate/Utils/Colour.hs \
+  src/Test/Speculate/Utils/Class.hs \
+  src/Test/Speculate/SemiReason.hs \
+  src/Test/Speculate/Sanity.hs \
+  src/Test/Speculate/Report.hs \
+  src/Test/Speculate/Reason.hs \
+  src/Test/Speculate/Reason/Order.hs \
+  src/Test/Speculate/Pretty.hs \
+  src/Test/Speculate.hs \
+  src/Test/Speculate/Expr.hs \
+  src/Test/Speculate/Expr/Instance.hs \
+  src/Test/Speculate/Expr/Ground.hs \
+  src/Test/Speculate/Expr/Equate.hs \
+  src/Test/Speculate/Expr/Core.hs \
+  src/Test/Speculate/Engine.hs \
+  src/Test/Speculate/CondReason.hs \
+  src/Test/Speculate/Args.hs \
+  bench/addition.hs
 bench/arithficial: \
   bench/arithficial.hs \
   mk/toplibs
diff --git a/speculate.cabal b/speculate.cabal
--- a/speculate.cabal
+++ b/speculate.cabal
@@ -1,5 +1,5 @@
 name:                speculate
-version:             0.4.18
+version:             0.4.20
 synopsis:            discovery of properties about Haskell functions
 description:
   Speculate automatically discovers laws about Haskell functions.
@@ -70,7 +70,7 @@
 source-repository this
   type:            git
   location:        https://github.com/rudymatela/speculate
-  tag:             v0.4.18
+  tag:             v0.4.20
 
 
 library
diff --git a/src/Test/Speculate/Engine.hs b/src/Test/Speculate/Engine.hs
--- a/src/Test/Speculate/Engine.hs
+++ b/src/Test/Speculate/Engine.hs
@@ -180,8 +180,8 @@
   where
   ns = rehole $ normalizeE thy (fastMostGeneralVariation s)
   -- between s and ns, choose the one with less holes to call equivalencesBetween
-  ms | length (holes s) < length (holes ns) = s
-     | otherwise = ns
+  ms | length (holes s) <= length (holes ns) = s
+     | otherwise = ns -- favour ns only if it reduces the number of variables
   e1 -===- e2  =  normalize thy e1 == normalize thy e2 || e1 === e2
   ss = uptoT sz sss
   sssWs = sss \/ wcons0 sz s
diff --git a/src/Test/Speculate/Reason.hs b/src/Test/Speculate/Reason.hs
--- a/src/Test/Speculate/Reason.hs
+++ b/src/Test/Speculate/Reason.hs
@@ -158,7 +158,7 @@
 normalize :: Thy -> Expr -> Expr
 normalize Thy {rules = rs} = n
   where
-  n e = case concatMap (e `reductions1`) rs of
+  n e = case concatMap (`reductions1` e) rs of
           []     -> e -- already normalized
           (e':_) -> n e'
 
@@ -167,7 +167,7 @@
 normalizeE thy@(Thy {equations = eqs, canReduceTo = (->-)})  =  n1
   where
   n1  =  n2 . normalize thy
-  n2 e = case filter (e ->-) (concatMap (e `reductions1`) $ eqs ++ map swap eqs) of
+  n2 e = case filter (e ->-) (concatMap (`reductions1` e) $ eqs ++ map swap eqs) of
          []     -> e -- already normalized
          (e':_) -> n1 e'
 
@@ -188,12 +188,14 @@
 reduceRoot e (e1,e2) = (e2 //-) <$> (e `match` e1)
 
 -- Lists all reductions by one rule, note that reductions may be repeated.
-reductions1 :: Expr -> Rule -> [Expr]
-reductions1 e (l,_) | size l > size e = [] -- optional optimization
-reductions1 e@(e1 :$ e2) r = maybeToList (e `reduceRoot` r)
-                          ++ map (:$ e2) (reductions1 e1 r)
-                          ++ map (e1 :$) (reductions1 e2 r)
-reductions1 e r = maybeToList (e `reduceRoot` r)
+reductions1 :: Rule -> Expr -> [Expr]
+reductions1 r@(l,_)  =  r1
+  where
+  r1 e  |  size l > size e  =  [] -- optional optimization
+  r1 e@(e1 :$ e2)  =  maybeToList (e `reduceRoot` r)
+                   ++ map (:$ e2) (r1 e1)
+                   ++ map (e1 :$) (r1 e2)
+  r1 e  =  maybeToList (e `reduceRoot` r)
 
 -- as defined by Martin & Nipkow in "Ordered Rewriting and Confluence" on 1990
 -- this definition is sound, but incomplete (some groundJoinable pairs won't be
@@ -225,7 +227,7 @@
       nubSortBy compareEqnQuickly
     . map sortuple
     . filter (uncurry (/=))
-    . concatMap (\e -> (e `reductions1` r1) ** (e `reductions1` r2))
+    . concatMap (\e -> (r1 `reductions1` e) ** (r2 `reductions1` e))
     $ overlaps e1 e2
   xs ** ys = [(x,y) | x <- xs, y <- ys]
   sortuple (x,y) | x < y     = (y,x)
@@ -237,12 +239,11 @@
   overlaps :: Expr -> Expr -> [Expr]
   overlaps e1 e2 = nubSortBy compareQuickly
                  . map (canonicalize . (e2' //-))
-                 $ (e1' `unifn`) `mapMaybe` nonVarSubexprs e2'
+                 $ (e1' `unification`) `mapMaybe` nonVarSubexprs e2'
     where
     nonVarSubexprs = discard isVar . nubSubexprs
     e1' = renameVarsBy (++ "1") e1
     e2' = renameVarsBy (++ "2") e2
-    unifn = unificationC (commutativeOperators thy)
 
 equivalent :: Thy -> Expr -> Expr -> Bool
 equivalent thy e1 e2 = e1' == e2'
@@ -269,7 +270,7 @@
   where
   eqs = equations thy
   step = nubMergeMap reductionsEqs1
-  reductionsEqs1 e = e `L.insert` nubMergeMap (reductions1 e) (eqs ++ map swap eqs)
+  reductionsEqs1 e = e `L.insert` nubMergeMap (`reductions1` e) (eqs ++ map swap eqs)
 
 insert :: Equation -> Thy -> Thy
 insert (e1,e2) thy
@@ -358,7 +359,7 @@
   collapsable = not . null . collapse
   collapse :: Rule -> [Equation]
   collapse (e1,e2) = foldr (+++) []
-    [ nubSort [ canonicalizeEqn thy (e,e2) | e <- reductions1 e1 (e1',e2') ]
+    [ nubSort [ canonicalizeEqn thy (e,e2) | e <- reductions1 (e1',e2') e1 ]
     | (e1',e2') <- rs
     , (e1',e2') /= (e1,e2)
     , e1 =| e1' ]
diff --git a/test/reason.hs b/test/reason.hs
--- a/test/reason.hs
+++ b/test/reason.hs
@@ -42,7 +42,7 @@
 
   putStrLn "\\e e1 e2 -> length $ reductions 1 e (e1,e2)"
   reportCountsBy (\(e,e1,e2) -> if e1 > e2 && typ e1 == typ e2
-                                  then "OK, length " ++ show (length $ reductions1 e (e1,e2))
+                                  then "OK, length " ++ show (length $ reductions1 (e1,e2) e)
                                   else "Not OK")
                  (take n list)