diff --git a/.gitignore b/.gitignore
--- a/.gitignore
+++ b/.gitignore
@@ -3,8 +3,10 @@
 **/cabal.sandbox.config
 **/idx/
 **/dist/
+dist-newstyle
 **/log/
 .stack-work
+stack.yaml.lock
 
 doc/**/*.html
 doc/**/*.css
diff --git a/.travis.yml b/.travis.yml
--- a/.travis.yml
+++ b/.travis.yml
@@ -1,6 +1,6 @@
 # .travis.yml file for Speculate
 #
-# Copyright:   (c) 2017-2018 Rudy Matela
+# Copyright:   (c) 2017-2020 Rudy Matela
 # License:     3-Clause BSD  (see the file LICENSE)
 # Maintainer:  Rudy Matela <rudy@matela.com.br>
 
@@ -22,6 +22,9 @@
 - export PATH=/opt/ghc/$GHCVER/bin:/opt/cabal/$CABALVER/bin:$PATH
 - ghc --version
 - cabal --version
+- haddock --version
+- du -hd3 ~/.cabal ~/.ghc || true
+- du -hd4 ~/.stack || true
 - rm -f ~/.cabal/config && cabal update
 # Download and unpack the stack executable
 # "Once Travis whitelists the stack.dev files," simply include stack in the
@@ -31,36 +34,42 @@
 - travis_retry curl -L https://www.stackage.org/stack/linux-x86_64 | tar xz --wildcards --strip-components=1 -C ~/.local/bin '*/stack'
 - stack config set system-ghc --global true
 - stack --version
-- cabal install leancheck express cmdargs
+- cabal install leancheck express cmdargs || cabal install leancheck express cmdargs --lib
 
 script:
-- make && make test-without-extra-deps
+- make && make test
 - make haddock
 - make test-sdist
-- travis_wait 40 cabal test expr --ghc-option=-O0
-- travis_wait 40 stack $STACKR --no-terminal --skip-ghc-check test speculate:test:expr --ghc-options=-O0
+- cabal test expr --ghc-option=-O0
+- stack --resolver $STACKVER --no-terminal --skip-ghc-check test speculate:test:expr --ghc-options=-O0
 
 matrix:
   allow_failures:
   - ghc: 'head'
   include:
   - ghc: 'head'
-    env:                   GHCVER=head         CABALVER=head
+    env:                   GHCVER=head         CABALVER=head   STACKVER=nightly-2020-03-28
     addons: {apt: {packages: [ghc-head,   cabal-install-head], sources: hvr-ghc}}
+  - ghc: '8.10'
+    env:                   GHCVER=8.10.1       CABALVER=3.2    STACKVER=nightly-2020-03-28
+    addons: {apt: {packages: [ghc-8.10.1, cabal-install-3.2],  sources: hvr-ghc}}
+  - ghc: '8.8'
+    env:                   GHCVER=8.8.3        CABALVER=3.0    STACKVER=lts-15.5
+    addons: {apt: {packages: [ghc-8.8.3,  cabal-install-3.0],  sources: hvr-ghc}}
   - ghc: '8.6'
-    env:                   GHCVER=8.6.1        CABALVER=2.4
-    addons: {apt: {packages: [ghc-8.6.1,  cabal-install-2.4],  sources: hvr-ghc}}
+    env:                   GHCVER=8.6.5        CABALVER=2.4    STACKVER=lts-14.27
+    addons: {apt: {packages: [ghc-8.6.5,  cabal-install-2.4],  sources: hvr-ghc}}
   - ghc: '8.4'
-    env:                   GHCVER=8.4.4        CABALVER=2.2
+    env:                   GHCVER=8.4.4        CABALVER=2.2    STACKVER=lts-12.26
     addons: {apt: {packages: [ghc-8.4.4,  cabal-install-2.2],  sources: hvr-ghc}}
   - ghc: '8.2'
-    env:                   GHCVER=8.2.2        CABALVER=2.0
+    env:                   GHCVER=8.2.2        CABALVER=2.0    STACKVER=lts-11.22
     addons: {apt: {packages: [ghc-8.2.2,  cabal-install-2.0],  sources: hvr-ghc}}
   - ghc: '8.0'
-    env:                   GHCVER=8.0.2        CABALVER=1.24
+    env:                   GHCVER=8.0.2        CABALVER=1.24   STACKVER=lts-9.21
     addons: {apt: {packages: [ghc-8.0.2,  cabal-install-1.24], sources: hvr-ghc}}
   - ghc: '7.10'
-    env:                   GHCVER=7.10.3       CABALVER=1.22   STACKR=--resolver=lts-11.11
+    env:                   GHCVER=7.10.3       CABALVER=1.22   STACKVER=lts-6.35
     addons: {apt: {packages: [ghc-7.10.3, cabal-install-1.22], sources: hvr-ghc}}
   # we only support stack with GHC >= 7.10
   - ghc: '7.8'
@@ -70,11 +79,12 @@
     - export PATH=/opt/ghc/$GHCVER/bin:/opt/cabal/$CABALVER/bin:$PATH
     - ghc --version
     - cabal --version
+    - haddock --version
     - rm -f ~/.cabal/config && cabal update
     - cabal install Cabal==1.18.*
     - cabal install leancheck express cmdargs
     script:
-    - make && make test-without-extra-deps
+    - make && make test
     - make haddock HADDOCKFLAGS=
     - make test-sdist
     - cabal test
diff --git a/Makefile b/Makefile
--- a/Makefile
+++ b/Makefile
@@ -24,7 +24,7 @@
   test/reason \
   test/utils \
   test/stats
-MOSTEG = \
+EG = \
   eg/arith \
   eg/arith-negate-abs \
   eg/bool \
@@ -48,13 +48,12 @@
   eg/tauts \
   eg/monad \
   eg/tuples \
+  eg/speculate-reason \
   bench/arithficial \
   bench/nord \
   bench/unit
-EG = $(MOSTEG) \
+EXTRAEG = \
   eg/regexes \
-  eg/speculate-reason
-EXTRAEG = $(EG) \
   eg/pretty-compact \
   eg/algebraic-graphs
 # regexes needs regex-tdfa, which may break the build
@@ -82,11 +81,8 @@
   $(patsubst %,%.run,$(TESTS)) \
   $(patsubst %,%.diff-test,$(EG) $(wildcard bench/*-c))
 
-test-without-extra-deps: all $(patsubst %,%.run,$(TESTS)) \
-                             $(patsubst %,%.diff-test,$(MOSTEG) $(wildcard bench/*-c))
-
-test-extra-deps: all $(patsubst %,%.run,$(TESTS)) \
-                     $(patsubst %,%.diff-test,$(EXTRAEG) $(wildcard bench/*-c))
+test-with-extra-deps: all test test-sdist \
+  $(patsubst %,%.diff-test,$(EXTRAEG) $(wildcard bench/*-c))
 
 test-sdist:
 	./test/sdist
@@ -171,13 +167,13 @@
 
 update-slow-diff-test: $(patsubst %,%.update-slow-diff-test,$(EG) $(wildcard bench/*-c))
 
-bench: all
+bench: all $(EG)
 	./test/benchmark-cmp $(EG) bench/*-c
 
-save-bench: all
+save-bench: all $(EG)
 	./test/benchmark-save $(EG) bench/*-c
 
-memory-benchmark: all
+memory-benchmark: all $(EG)
 	./test/memory-benchmark $(EG) bench/*-c
 
 qs-bench:
diff --git a/TODO.md b/TODO.md
--- a/TODO.md
+++ b/TODO.md
@@ -10,8 +10,6 @@
   I can use a custom data structure that computes
   matches all at once while traversing an expression.
 
-* fix issues with Dershowitz and Knuth-Bendix orders.
-
 * (code readability) review and document code
 
 * (code readability) rename semi to inqualities everywhere.
diff --git a/bench/runtime-zero b/bench/runtime-zero
--- a/bench/runtime-zero
+++ b/bench/runtime-zero
@@ -1,35 +1,35 @@
 GHC 8.6.5
-express-0.1.0
+express-0.1.1
 leancheck-0.9.1
 arith               0.260
-arith-c             0.610
-arithficial         0.976
-arith-negate-abs    1.823
-binarytree          1.793
-binarytree0         0.533
-bool                1.950
-bool-c              1.753
-colour              2.206
-digraphs            1.603
-fun                 1.243
-insertsort          8.320
-insertsort0         1.000
-length              0.640
-list                2.730
-list-c              1.673
-minus               0.580
-minus-c             0.966
-monad               0.653
+arith-c             0.603
+arithficial         0.966
+arith-negate-abs    1.846
+binarytree          1.753
+binarytree0         0.520
+bool                1.983
+bool-c              1.723
+colour              2.130
+digraphs            1.560
+fun                 1.190
+insertsort          8.593
+insertsort0         0.996
+length              0.646
+list                2.826
+list-c              1.770
+minus               0.603
+minus-c             0.996
+monad               0.690
 nord                0.010
-oddeven             6.930
-plus-abs            3.866
-pretty              9.183
-ratio               9.320
-regexes             8.300
-sets                7.610
-speculate-reason    3.710
-string              0.953
-tauts               4.466
-tuples              1.313
+oddeven             7.340
+plus-abs            3.786
+pretty              9.080
+ratio               9.300
+regexes             8.013
+sets                7.696
+speculate-reason    3.300
+string              0.950
+tauts               4.286
+tuples              1.286
 unit                0.010
-zip                 2.490
+zip                 2.463
diff --git a/eg/algebraic-graphs.hs b/eg/algebraic-graphs.hs
--- a/eg/algebraic-graphs.hs
+++ b/eg/algebraic-graphs.hs
@@ -1,14 +1,10 @@
 {-# LANGUAGE TemplateHaskell #-}
 import Test.Speculate
-import Test.Speculate.Expr.Instance (name)
 import Data.Function (on)
 import Control.Monad (unless)
 
 import Algebra.Graph
 
-instance Ord a => Ord (Graph a) where
-  (<=) = isSubgraphOf
-
 -- deriveListable ''Graph {-
 instance (Ord a, Listable a) => Listable (Graph a) where
   tiers = concatMapT graphs $ setsOf tiers
@@ -18,8 +14,12 @@
     fromAdjList :: [(a,[a])] -> Graph a
     fromAdjList ness = graph [n | (n,_) <- ness]
                              [(n1,n2) | (n1,n2s) <- ness, n2 <- n2s]
+    graph vs es = foldr overlay empty $ map vertex vs ++ map (uncurry edge) es
 -- -}
 
+instance Name Nat3 where name _ = "x"
+instance Name (Graph a) where name _ = "g1"
+
 main :: IO ()
 main = do
   unless (listableGraphOK 180 a) $
@@ -41,7 +41,6 @@
         , constant "overlay"   (overlay -:> gr a)
         , constant "connect"   (connect -:> gr a)
         , constant "edge"      (edge    -:> a)
-        , constant "length"    (length  -:> gr a)
         , constant "size"      (size    -:> gr a)
         ]
     , showConditions = False
diff --git a/eg/pretty-compact.hs b/eg/pretty-compact.hs
--- a/eg/pretty-compact.hs
+++ b/eg/pretty-compact.hs
@@ -34,11 +34,11 @@
 da :: Doc Any
 da = undefined
 
-instance Name Doc where name _ = "d1"
+instance Name (Doc a) where name _ = "d1"
 
 main :: IO ()
 main = speculate args
-  { instances = [reifyInstances "d1" da]
+  { instances = [reifyInstances da]
   , showConditions = False
   , maxSize = 4
   , maxTests = 360
diff --git a/mk/ghcdeps b/mk/ghcdeps
--- a/mk/ghcdeps
+++ b/mk/ghcdeps
@@ -2,7 +2,7 @@
 #
 # ghcdeps: generate Haskell make dependencies for compiling with GHC.
 #
-# Copyright (c) 2015-2019 Rudy Matela.
+# Copyright (c) 2015-2020 Rudy Matela.
 # Distributed under the 3-Clause BSD licence.
 #
 # From a list of files provided on standard input,
diff --git a/mk/haddock-i b/mk/haddock-i
--- a/mk/haddock-i
+++ b/mk/haddock-i
@@ -2,7 +2,7 @@
 #
 # haddock-i: list haddock's -i parameters.
 #
-# Copyright (c) 2015-2019 Rudy Matela.
+# Copyright (c) 2015-2020 Rudy Matela.
 # Distributed under the 3-Clause BSD licence.
 #
 # $ haddock-i <package1> <package2> ... <packageN>
diff --git a/mk/haskell.mk b/mk/haskell.mk
--- a/mk/haskell.mk
+++ b/mk/haskell.mk
@@ -1,6 +1,6 @@
 # Implicit rules for compiling Haskell code.
 #
-# Copyright (c) 2015-2019 Rudy Matela.
+# Copyright (c) 2015-2020 Rudy Matela.
 # Distributed under the 3-Clause BSD licence.
 #
 # You can optionally configure the "Configuration variables" below in your main
@@ -39,7 +39,7 @@
 # ALL_HSS: all Haskell files
 # You can override ALL/LIB_HSS in your main Makefile
 LIST_LIB_HSS ?= find src -name "*.hs"
-LIST_ALL_HSS ?= find \( -path "./dist" -o -path "./.stack-work" \) -prune \
+LIST_ALL_HSS ?= find \( -path "./dist*" -o -path "./.stack-work" -o -path "./Setup.hs" \) -prune \
                      -o -name "*.*hs" -print
 LIB_HSS ?= $(shell $(LIST_LIB_HSS))
 ALL_HSS ?= $(shell $(LIST_ALL_HSS))
@@ -97,7 +97,7 @@
 haddock: doc/index.html
 
 clean-haddock:
-	rm -f doc/*.{html,css,js,png,gif,json} doc/src/*.{html,css,js} README.html
+	rm -f doc/*.{html,css,js,png,gif,json} doc/src/* README.html
 
 upload-haddock:
 	@echo "use \`cabal upload -d' instead"
diff --git a/mk/install-on b/mk/install-on
new file mode 100644
--- /dev/null
+++ b/mk/install-on
@@ -0,0 +1,30 @@
+#!/bin/bash
+#
+# mk/install-on: install or updates the mk folder on a Haskell project
+#
+# usage: ./mk/install-on path/to/project
+#
+# This assumes a few things:
+#
+# * tests are stored in a "test/" folder
+# * sources are stored in a "src/" folder
+set -e
+
+errxit() {
+	echo "$@" > /dev/stderr
+	exit 1
+}
+
+src=`dirname $0`/..
+dst="$1"
+
+[ -n "$dst" ] || errxit "destination folder not provided"
+
+mkdir -p $dst/mk
+mkdir -p $dst/test
+
+cp $src/mk/ghcdeps    $dst/mk/ghcdeps
+cp $src/mk/haddock-i  $dst/mk/haddock-i
+cp $src/mk/haskell.mk $dst/mk/haskell.mk
+cp $src/mk/install-on $dst/mk/install-on
+cp $src/test/sdist    $dst/test/sdist
diff --git a/speculate.cabal b/speculate.cabal
--- a/speculate.cabal
+++ b/speculate.cabal
@@ -1,5 +1,5 @@
 name:                speculate
-version:             0.4.1
+version:             0.4.2
 synopsis:            discovery of properties about Haskell functions
 description:
   Speculate automatically discovers laws about Haskell functions.
@@ -57,6 +57,7 @@
                   , mk/ghcdeps
                   , mk/haddock-i
                   , mk/haskell.mk
+                  , mk/install-on
                   , stack.yaml
                   , test/benchmark
                   , test/benchmark-cmp
@@ -67,7 +68,9 @@
                   , test/update-diff
                   , test/sdist
 
-tested-with: GHC==8.6
+tested-with: GHC==8.10
+           , GHC==8.8
+           , GHC==8.6
            , GHC==8.4
            , GHC==8.2
            , GHC==8.0
@@ -81,7 +84,7 @@
 source-repository this
   type:            git
   location:        https://github.com/rudymatela/speculate
-  tag:             v0.4.1
+  tag:             v0.4.2
 
 
 library
@@ -117,8 +120,8 @@
                  , Test.Speculate.Utils.Timeout
                  , Test.Speculate.Utils.Tuple
   build-depends: base >= 4 && < 5
-               , leancheck >= 0.9.1
-               , express >= 0.1.1
+               , leancheck >= 0.9.3
+               , express >= 0.1.3
                , cmdargs
                , containers
   hs-source-dirs:    src
@@ -177,13 +180,6 @@
   other-modules:     Test, Test.ListableExpr
   hs-source-dirs:    test
   build-depends:     base >= 4 && < 5, leancheck, express, speculate
-  default-language:  Haskell2010
-  type:              exitcode-stdio-1.0
-
-benchmark plus-abs
-  main-is:           plus-abs.hs
-  hs-source-dirs:    eg
-  build-depends:     base >= 4 && < 5, speculate
   default-language:  Haskell2010
   type:              exitcode-stdio-1.0
 
diff --git a/src/Test/Speculate/Expr/Core.hs b/src/Test/Speculate/Expr/Core.hs
--- a/src/Test/Speculate/Expr/Core.hs
+++ b/src/Test/Speculate/Expr/Core.hs
@@ -14,6 +14,7 @@
   -- * Order
   , lexicompare
   , lexicompareBy
+  , fastCompare
 
   -- * Properties
   , isConstantNamed
@@ -37,6 +38,16 @@
 import Test.Speculate.Utils.List
 import Data.Monoid ((<>))
 import Data.Functor ((<$>)) -- for GHC <= 7.8
+
+-- faster comparison, to be used when nubSorting Expr values
+fastCompare :: Expr -> Expr -> Ordering
+fastCompare  =  cmp
+  where
+  (f :$ x)       `cmp` (g :$ y)        =  f  `cmp` g <> x `cmp` y
+  (_ :$ _)       `cmp` _               =  GT
+  _              `cmp` (_ :$ _)        =  LT
+  x@(Value n1 _) `cmp` y@(Value n2 _)  =  typ x `compareTy` typ y
+                                       <> n1 `compare` n2
 
 lexicompare :: Expr -> Expr -> Ordering
 lexicompare = lexicompareBy compare
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
@@ -208,22 +208,23 @@
                             $ criticalPairs thy
 
 criticalPairs :: Thy -> [(Expr,Expr)]
-criticalPairs thy@Thy {rules = rs, compareE = cmp} =
-  nubMerges [r `criticalPairsWith` s | r <- rs, s <- rs]
+criticalPairs thy@Thy{rules = rs}  =
+  nubMergesBy fastCompareEqn [r `criticalPairsWith` s | r <- rs, s <- rs]
   where
   criticalPairsWith :: Rule -> Rule -> [(Expr,Expr)]
   r1@(e1,_) `criticalPairsWith` r2@(e2,_) =
-      nubSortBy (compareEqn thy)
+      nubSortBy fastCompareEqn
     . map sortuple
     . filter (uncurry (/=))
     . concatMap (\e -> (e `reductions1` r1) ** (e `reductions1` r2))
-    . nubSortBy cmp
+    . nubSortBy fastCompare
     $ overlaps e1 e2
   xs ** ys = [(x,y) | x <- xs, y <- ys]
   sortuple (x,y) | x < y     = (y,x)
                  | otherwise = (x,y)
+  fastCompareEqn = fastCompare `on` foldPair
   (<) :: Expr -> Expr -> Bool
-  e1 < e2 = e1 `cmp` e2 == LT
+  e1 < e2 = e1 `fastCompare` e2 == LT
 
 -- Warning: will have to also be applied in reverse to get all overlaps.
 --
diff --git a/src/Test/Speculate/Reason/Order.hs b/src/Test/Speculate/Reason/Order.hs
--- a/src/Test/Speculate/Reason/Order.hs
+++ b/src/Test/Speculate/Reason/Order.hs
@@ -16,6 +16,8 @@
   , weight
   , weightExcept
   , gtExcept
+  , funny
+  , serious
   )
 where
 
@@ -47,7 +49,6 @@
 (>|) :: Expr -> Expr -> Bool
 (>|) = kboBy weight (>)
 infix 4 >|
--- TODO: FIXME: this KBO is not closed under substitution!
 
 kboBy :: (Expr -> Int) -> (Expr -> Expr -> Bool) -> Expr -> Expr -> Bool
 kboBy w (->-) e1 e2 = e1 >=\/ e2
@@ -123,6 +124,8 @@
 --
 -- > x - y |> x + negate y  -- as (-) > (+)
 -- > negate x + y |> negate (x + negate y)  -- as (+) > negate, as I->I->I > I->I
+--
+-- This is not a simplification order on 'funny' 'Expr's.
 (|>) :: Expr -> Expr -> Bool
 (|>) = dwoBy (>)
 infix 4 |>
@@ -130,6 +133,8 @@
 -- | Dershowitz reduction order as defined in TRAAT
 --
 -- @|>@ a "D" for Dershowitz
+--
+-- This is not a simplification order on 'funny' 'Expr's.
 dwoBy :: (Expr -> Expr -> Bool) -> Expr -> Expr -> Bool
 dwoBy (>) = (|>)
   where
@@ -147,6 +152,25 @@
     e1 |>= e2 = e1 == e2
              || e1 |> e2
 
+-- | Returns 'True' when an 'Expr'ession has either
+--   a functional type or functional 'var'iables.
+--
+-- > funny xx        =  False
+-- > funny one       =  False
+-- > funny idE       =  True
+-- > funny (ff one)  =  True
+funny :: Expr -> Bool
+funny e  =  any (isFunTy . typ) $ e:vars e
+
+-- | Returns 'True' when an 'Expr'ession has
+--   no functional return type and no functional 'var'iables.
+--
+-- > serious xx        =  True
+-- > serious one       =  True
+-- > serious idE       =  False
+-- > serious (ff one)  =  False
+serious :: Expr -> Bool
+serious  =  not . funny
 
 
 --- Misc Utilities ---
diff --git a/stack.yaml b/stack.yaml
--- a/stack.yaml
+++ b/stack.yaml
@@ -1,12 +1,8 @@
-resolver: lts-13.30
+resolver: lts-15.5 # or ghc-8.8.3
 
 packages:
 - .
 
 extra-deps:
-- leancheck-0.9.1
-- express-0.1.1
-
-flags: {}
-
-extra-package-dbs: []
+- leancheck-0.9.3
+- express-0.1.3
diff --git a/test/model/algebraic-graphs-s4.out b/test/model/algebraic-graphs-s4.out
--- a/test/model/algebraic-graphs-s4.out
+++ b/test/model/algebraic-graphs-s4.out
@@ -2,10 +2,10 @@
 max  #-tests   = 1080
 max  #-vars    =    2  (for inequational and conditional laws)
 
-_ :: Bool  (holes: Bool)
-_ :: Int  (holes: Int)
-_ :: Nat3  (holes: Nat3)
-_ :: Graph Nat3  (holes: Graph Nat3)
+_ :: Bool
+_ :: Int
+_ :: Nat3
+_ :: Graph Nat3
 0 :: Nat3
 0 :: Int
 True :: Bool
@@ -16,36 +16,33 @@
 overlay :: Graph Nat3 -> Graph Nat3 -> Graph Nat3
 connect :: Graph Nat3 -> Graph Nat3 -> Graph Nat3
 edge :: Nat3 -> Nat3 -> Graph Nat3
-length :: Graph Nat3 -> Int
 size :: Graph Nat3 -> Int
 
-length (vertex i) == length (vertex j)
-  size (vertex i) == length (vertex 0)
-length (edge i j) == length (edge k i')
-length (edge i j) == size (edge k i')
-   length (x * y) == length (x + y)
-     size (x * y) == size (x + y)
-            x + x == x
-        x + empty == x
-        x * empty == x
-        empty * x == x
-            x + y == y + x
-      overlay x y == x + y
-      connect x y == x * y
+size (vertex x) == size empty
+size (edge x y) == size (edge z x')
+ size (g1 * g2) == size (g1 + g2)
+        g1 + g1 == g1
+     g1 + empty == g1
+     g1 * empty == g1
+     empty * g1 == g1
+        g1 + g2 == g2 + g1
+  overlay g1 g2 == g1 + g2
+  connect g1 g2 == g1 * g2
 
-                0 <= length x
-                0 <= size x
-         length x <= size x
-       size empty <= size x
-         length x <= length (x + y)
-           size x <= size (x + y)
-         length x <= size (y + x)
-length (edge i i) <= size x
-            empty <= x
-                x <= x + y
-                x <= x * y
-                x <= y * x
-         vertex i <= edge i j
-         vertex i <= edge j i
-            x + y <= x * y
+              0 <= size g1
+     size empty <= size g1
+        size g1 <= size (g1 + g2)
+size (edge x x) <= size (g1 + g2)
+          empty <= g1
+             g1 <= g1 + g2
+             g1 <= g1 * g2
+             g1 <= g2 * g1
+       vertex 0 <= vertex x
+       vertex x <= edge x y
+       vertex x <= edge y x
+       edge x x <= edge x y
+       edge x x <= edge y x
+        g1 + g2 <= g1 * g2
+       edge 0 0 <= edge x y
+       edge 0 x <= edge x 0
 
diff --git a/test/model/algebraic-graphs.out b/test/model/algebraic-graphs.out
--- a/test/model/algebraic-graphs.out
+++ b/test/model/algebraic-graphs.out
@@ -4,10 +4,10 @@
 max  #-tests   = 1080
 max  #-vars    =    2  (for inequational and conditional laws)
 
-_ :: Bool  (holes: Bool)
-_ :: Int  (holes: Int)
-_ :: Nat3  (holes: Nat3)
-_ :: Graph Nat3  (holes: Graph Nat3)
+_ :: Bool
+_ :: Int
+_ :: Nat3
+_ :: Graph Nat3
 0 :: Nat3
 0 :: Int
 True :: Bool
@@ -18,41 +18,37 @@
 overlay :: Graph Nat3 -> Graph Nat3 -> Graph Nat3
 connect :: Graph Nat3 -> Graph Nat3 -> Graph Nat3
 edge :: Nat3 -> Nat3 -> Graph Nat3
-length :: Graph Nat3 -> Int
 size :: Graph Nat3 -> Int
 
-    length (vertex i) == length (vertex j)
-      size (vertex i) == length (vertex 0)
-       length (x * y) == length (x + y)
-         size (x * y) == size (x + y)
-length (x + vertex i) == length (x + vertex j)
-  size (x + vertex i) == size (x + vertex j)
-                x + x == x
-            x + empty == x
-            x * empty == x
-            empty * x == x
-                x + y == y + x
-          overlay x y == x + y
-          connect x y == x * y
-            x + x * y == x * y
-            x + y * x == y * x
-             edge i j == vertex i * vertex j
-          (x + y) + z == x + (y + z)
-          (x * y) * z == x * (y * z)
-          x * (x * y) == x * (x + y)
-          (x + y) * x == y * (x * x)
+     size (vertex x) == size empty
+      size (g1 * g2) == size (g1 + g2)
+size (g1 + vertex x) == size (g1 + vertex y)
+             g1 + g1 == g1
+          g1 + empty == g1
+          g1 * empty == g1
+          empty * g1 == g1
+             g1 + g2 == g2 + g1
+       overlay g1 g2 == g1 + g2
+       connect g1 g2 == g1 * g2
+        g1 + g1 * g2 == g1 * g2
+        g1 + g2 * g1 == g2 * g1
+            edge x y == vertex x * vertex y
+      (g1 + g2) + g3 == g1 + (g2 + g3)
+      (g1 * g2) * g3 == g1 * (g2 * g3)
+      g1 * (g1 * g2) == g1 * (g1 + g2)
+      (g1 + g2) * g1 == g2 * (g1 * g1)
 
-         0 <= length x
-         0 <= size x
-  length x <= size x
-size empty <= size x
-  length x <= length (x + y)
-    size x <= size (x + y)
-  length x <= size (y + x)
-size empty <= length (edge i i)
-     empty <= x
-         x <= x + y
-         x <= x * y
-         x <= y * x
-     x + y <= x * y
+         0 <= size g1
+size empty <= size g1
+   size g1 <= size (g1 + g2)
+     empty <= g1
+        g1 <= g1 + g2
+        g1 <= g1 * g2
+        g1 <= g2 * g1
+  vertex 0 <= vertex x
+  edge x x <= edge x y
+  edge x x <= edge y x
+   g1 + g2 <= g1 * g2
+  edge 0 0 <= edge x y
+  edge 0 x <= edge x 0
 
diff --git a/test/model/pretty-compact-s4.out b/test/model/pretty-compact-s4.out
--- a/test/model/pretty-compact-s4.out
+++ b/test/model/pretty-compact-s4.out
@@ -4,10 +4,10 @@
 max  #-tests   =  360
 max  #-vars    =    2  (for inequational and conditional laws)
 
-_ :: Char  (holes: Char)
-_ :: Int  (holes: Int)
-_ :: ODoc Any  (holes: ODoc Any)
-_ :: [Char]  (holes: [Char])
+_ :: Char
+_ :: Int
+_ :: ODoc Any
+_ :: [Char]
 text :: [Char] -> ODoc Any
 char :: Char -> ODoc Any
 flush :: ODoc Any -> ODoc Any
@@ -18,6 +18,10 @@
 (</>) :: ODoc Any -> ODoc Any -> ODoc Any
 (<//>) :: ODoc Any -> ODoc Any -> ODoc Any
 (<$$>) :: ODoc Any -> ODoc Any -> ODoc Any
+
+Warning: no Listable instance for Any, variables of this type will not be considered
+Warning: no Eq instance for Any, equations of this type will not be considered
+Warning: no Ord instance for Any, inequations of this type will not be considered
 
         d1 $$ d2 == flush d1 <> d2
       d1 <$$> d2 == flush d1 <> d2
diff --git a/test/model/pretty-compact.out b/test/model/pretty-compact.out
--- a/test/model/pretty-compact.out
+++ b/test/model/pretty-compact.out
@@ -4,10 +4,10 @@
 max  #-tests   =  360
 max  #-vars    =    2  (for inequational and conditional laws)
 
-_ :: Char  (holes: Char)
-_ :: Int  (holes: Int)
-_ :: ODoc Any  (holes: ODoc Any)
-_ :: [Char]  (holes: [Char])
+_ :: Char
+_ :: Int
+_ :: ODoc Any
+_ :: [Char]
 text :: [Char] -> ODoc Any
 char :: Char -> ODoc Any
 flush :: ODoc Any -> ODoc Any
@@ -18,6 +18,10 @@
 (</>) :: ODoc Any -> ODoc Any -> ODoc Any
 (<//>) :: ODoc Any -> ODoc Any -> ODoc Any
 (<$$>) :: ODoc Any -> ODoc Any -> ODoc Any
+
+Warning: no Listable instance for Any, variables of this type will not be considered
+Warning: no Eq instance for Any, equations of this type will not be considered
+Warning: no Ord instance for Any, inequations of this type will not be considered
 
         d1 $$ d2 == flush d1 <> d2
       d1 <$$> d2 == flush d1 <> d2
diff --git a/test/order.hs b/test/order.hs
--- a/test/order.hs
+++ b/test/order.hs
@@ -1,7 +1,6 @@
 {-# Language DeriveDataTypeable, StandaloneDeriving #-} -- Travis
 import Test
 import Test.Speculate.Utils
-import qualified Test.LeanCheck.Utils as LC (comparison)
 
 import Test.Speculate.Expr
 import Test.Speculate.Reason (emptyThy)
@@ -21,8 +20,8 @@
   [ True -- see test-expr.hs for general Expr orders
 
   , holds n $ compare ==== (compareComplexity <> lexicompare)
-  , holds n $ LC.comparison lexicompare
-  , holds n $ LC.comparison compareComplexity
+  , holds n $ isComparison lexicompare
+  , holds n $ isComparison compareComplexity
 
   , holds n $ \(IntToIntE e1) (IntToIntE e2) (IntE e3) -> let cmp = lexicompare in
                 e1 `cmp` e2 == (e1 :$ e3) `cmp` (e2 :$ e3)
@@ -39,6 +38,10 @@
   , value "xx" xx < value "emptyThyght" (Thyght emptyThy)
 
   , holds n $ simplificationOrder (|>|)
+  , holds n $ seriousSimplificationOrder (|> )
+  , holds n $ seriousSimplificationOrder (dwoBy (<))
+  , fails 10080 $ compatible (|>) -- fails for funny exprs
+
   , fails n $ simplificationOrder ( >|) -- TODO: make this pass (holds)
   , fails n $ closedUnderSub ( >|) -- reason for the above, I believe this is an actual bug in >|
 -- > > checkFor 5040 $ closedUnderSub ( >|)
@@ -50,26 +53,6 @@
 -- The above bug did exist before the introduction of Express and probably
 -- since the creation of (>|).
 
--- TODO: fix the following two tests
--- > > checkFor 10080 $ simplificationOrder (dwoBy (<))
--- > *** Failed! Falsifiable (after 6901 tests):
--- > (f _ :: Int) (id _ :: Int) (_ :: Int)
--- > > checkFor 10080 $ simplificationOrder (|> )
--- > *** Failed! Falsifiable (after 6901 tests):
--- > (f _ :: Int) (id _ :: Int) (_ :: Int)
-
-  -- TODO: fix the following two tests with 10000 tests:
-  , holds 5040 $ simplificationOrder (|> )
-  , holds 5040 $ simplificationOrder (dwoBy (<))
-  , fails 10080 $ compatible (|>)
--- TODO: fix the following two tests
--- > > checkFor 10080 $ compatible    (|>)
--- > *** Failed! Falsifiable (after 6901 tests):
--- > (f _ :: Int) (id _ :: Int) (_ :: Int)
--- Like the one above
--- Compatibility fails whenever there are function variables.
-
-
   , fails n $ \e1 e2 -> (e1 |>| e2) == (e1 |>  e2)
   , fails n $ \e1 e2 -> (e1 |>| e2) == (e1  >| e2)
   , fails n $ \e1 e2 -> (e1 |>  e2) == (e1  >| e2)
@@ -111,6 +94,13 @@
   e1 `lgt` e2 = e1 `lexicompare` e2 == GT
   e1 `cgt` e2 = e1 `compare` e2 == GT
 
+-- weaker than simplificationOrder
+seriousSimplificationOrder :: (Expr -> Expr -> Bool) -> Expr -> Expr -> Expr -> Bool
+seriousSimplificationOrder (>) = seriousp $ simplificationOrder (>)
+
+seriousp :: (Expr -> Expr -> Expr -> Bool) -> Expr -> Expr -> Expr -> Bool
+seriousp prop  =  \e1 e2 e3 -> serious e1 && serious e2 && serious e3 ==> prop e1 e2 e3
+
 simplificationOrder :: (Expr -> Expr -> Bool) -> Expr -> Expr -> Expr -> Bool
 simplificationOrder (>) = \e1 e2 e3 -> reductionOrder  (>) e1 e2 e3
                                     && subtermProperty (>) e1
@@ -121,7 +111,7 @@
                           $ subexprs e -- isn't this subexprsV? I don't think so
 
 reductionOrder :: (Expr -> Expr -> Bool) -> Expr -> Expr -> Expr -> Bool
-reductionOrder (>) = \e1 e2 e3 -> strictPartialOrder (>) e1 e2 e3
+reductionOrder (>) = \e1 e2 e3 -> isStrictPartialOrder (>) e1 e2 e3
                                && compatible         (>) e1 e2 e3
                                && closedUnderSub     (>) e1 e2 e3
 
diff --git a/test/reason.hs b/test/reason.hs
--- a/test/reason.hs
+++ b/test/reason.hs
@@ -93,34 +93,34 @@
 --, holds n $ \(SameTypedPairsE eqs) -> theorize'' eqs == theorize eqs
 
   , holds n $ okThy . deduce
-  , holds n $ idempotent deduce
+  , holds n $ isIdempotent deduce
   , holds n $ \thy -> ((>=) `on` length . equations) (deduce thy) thy
   , holds n $ \thy -> ((==) `on` rules)              (deduce thy) thy
 
   , holds n $ okThy . simplify
-  , holds n $ idempotent simplify
+  , holds n $ isIdempotent simplify
   , holds n $ \thy -> ((<=) `on` length . equations) (simplify thy) thy
   , holds n $ \thy -> ((==) `on` rules)              (simplify thy) thy
 
   , holds n $ okThy . delete
-  , holds n $ idempotent delete
+  , holds n $ isIdempotent delete
   , holds n $ \thy -> ((<=) `on` length . equations) (delete thy) thy
   , holds n $ \thy -> ((==) `on` rules)              (delete thy) thy
 
   , holds n $ okThy . orient
-  , holds n $ idempotent orient
+  , holds n $ isIdempotent orient
   , holds n $ \thy -> ((<=) `on` length . equations) (orient thy) thy
   , holds n $ \thy -> ((>=) `on` length . rules)     (orient thy) thy
   , holds n $ \thy -> length (equations thy)      - length (equations $ orient thy)
                    >= length (rules $ orient thy) - length (rules thy)
 
   , holds n $ okThy . compose
-  , holds n $ idempotent compose
+  , holds n $ isIdempotent compose
   , holds n $ \thy -> ((<=) `on` length . rules)     (compose thy) thy
   , holds n $ \thy -> ((==) `on` equations)          (compose thy) thy
 
   , holds n $ okThy . collapse
-  , holds n $ idempotent collapse
+  , holds n $ isIdempotent collapse
   , holds n $ \thy -> ((<=) `on` length . rules)     (collapse thy) thy
   , holds n $ \thy -> ((>=) `on` length . equations) (collapse thy) thy
 
@@ -144,7 +144,7 @@
                $ thy' { keepE = keepUpToLength (max (size e1) (size e2)) }
        in  equivalent thy e1 e2
 
-  , holds n $ idempotent finalize
+  , holds n $ isIdempotent finalize
 
   , criticalPairs emptyThy { rules = [ ((xx -+- yy) -+- zz,xx -+- (yy -+- zz))
                                      , (negate' xx -+- xx, zero) ] }
@@ -154,22 +154,11 @@
   , criticalPairs emptyThy { rules = [ (negate' (negate' xx), id' xx) ] }
       == [ (negate' (id' xx), id' (negate' xx)) ]
 
-  , criticalPairs emptyThy { canReduceTo = dwoBy (\e1 e2 -> e1 `lexicompare` e2 == GT)
-                           , rules = [ (foo (goo (foo xx)), xx)
-                                     , (foo (goo xx), goo (foo xx)) ] }
-      == (let sortuple (x,y) | x < y     = (y,x)
-                             | otherwise = (x,y)
-          in nubSort . map sortuple
-           $ [ (goo xx,                   foo (goo (goo (foo xx))))
-             , (goo (foo xx),             foo (goo xx))
-             , (goo (foo (foo xx)),       xx)
-             , (goo (foo (foo (goo xx))), goo xx) ])
-
   , criticalPairs emptyThy { rules = [ (foo (goo (foo xx)), xx)
                                      , (foo (goo xx), goo (foo xx)) ] }
-      == [ (goo (foo xx),             foo (goo xx))
+      == [ (goo xx,                   foo (goo (goo (foo xx))))
+         , (goo (foo xx),             foo (goo xx))
          , (goo (foo (foo xx)),       xx)
-         , (foo (goo (goo (foo xx))), goo xx)
          , (goo (foo (foo (goo xx))), goo xx) ]
 
   , theorize [ (xx -*- yy) -*- (yy -*- zz)  ~~  yy ]
diff --git a/test/sdist b/test/sdist
--- a/test/sdist
+++ b/test/sdist
@@ -1,33 +1,40 @@
 #!/bin/bash
 #
-# test-sdist: tests the package generated by "cabal sdist".
+# test/sdist: tests the package generated by "cabal sdist".
 #
-# Copyright (c) 2015-2018 Rudy Matela.
+# Copyright (c) 2015-2020 Rudy Matela.
 # Distributed under the 3-Clause BSD licence.
+
+set -xe
+
 export LC_ALL=C  # consistent sort
+
 pkgver=` cat *.cabal | grep "^version:" | sed -e "s/version: *//"`
 pkgname=`cat *.cabal | grep "^name:"    | sed -e "s/name: *//"`
-pkg=$pkgname-$pkgver
-set -x
-cabal sdist &&
-cd dist &&
-tar -tf $pkg.tar.gz | sort --ignore-case          > ls-cabal-i  &&
-tar -tf $pkg.tar.gz | sort --ignore-case --unique > ls-cabal-iu &&
-diff -rud ls-cabal-i ls-cabal-iu &&
-rm -f ls-cabal ls-cabal-ignore-case &&
-if [ -d ../.git ]
+pkgbase=$pkgname-$pkgver
+
+cabal sdist
+
+# Try to find the package generated by cabal.
+pkg=`find dist* -name $pkgbase.tar.gz`
+[ -f "$pkg" ]
+# If the script fails here, either:
+#   * no package was generated
+#   * there are packages in both dist and dist-newstyle folders.
+
+tmp=`mktemp -d /tmp/test-sdist-XXXXXXXXXX`
+
+# Test if our file is compatible with case-insensitive filesystems.
+tar -tf $pkg | sort --ignore-case          > $tmp/ls-cabal-i
+tar -tf $pkg | sort --ignore-case --unique > $tmp/ls-cabal-iu
+diff -rud $tmp/ls-cabal-i $tmp/ls-cabal-iu
+
+if [ -d .git ]
 then
-	# on git repo, test if files are the same
-	git -C .. ls-files                                      | sort > ls-git   &&
-	tar -tf $pkg.tar.gz | grep -v "/$" | sed -e "s,$pkg/,," | sort > ls-cabal &&
-	diff -rud ls-git ls-cabal &&
-	rm -f ls-git ls-cabal
-else
-	# outside of git repo, test build
-	rm -rf $pkg/ &&
-	tar -xzf $pkg.tar.gz &&
-	cd $pkg/ &&
-	cabal configure --enable-tests --enable-benchmarks &&
-	cabal build &&
-	cabal test
+	# Test if files included by cabal are the same as files tracked in git.
+	git ls-files                                         | sort > $tmp/ls-git
+	tar -tf $pkg | grep -v "/$" | sed -e "s,$pkgbase/,," | sort > $tmp/ls-cabal
+	diff -rud $tmp/ls-git $tmp/ls-cabal
 fi
+
+rm -r $tmp
diff --git a/test/utils.hs b/test/utils.hs
--- a/test/utils.hs
+++ b/test/utils.hs
@@ -8,7 +8,7 @@
 import Data.List
 import Data.Function
 
-import Test.LeanCheck.Utils (comparison)
+import Test.LeanCheck.Utils
 
 main :: IO ()
 main = mainTest tests 10000
@@ -78,7 +78,7 @@
   , compareIndex [3,2,1::Int] 1 3 == GT
   , compareIndex [3,2,1::Int] 4 1 == GT
   , compareIndex [3,2,1::Int] 1 0 == LT
-  , holds n $ \xs -> comparison (compareIndex (xs::[Int]))
+  , holds n $ \xs -> isComparison (compareIndex (xs::[Int]))
 
   , partitionByMarkers '#' '*' "" == ("","")
   , partitionByMarkers '#' '*' "abc*def" == ("abc","def")