diff --git a/.gitignore b/.gitignore
--- a/.gitignore
+++ b/.gitignore
@@ -56,6 +56,7 @@
 bench/p12
 bench/p30
 bench/candidates
+bench/redundants
 bench/gps
 bench/gps2
 bench/lowtests
diff --git a/Makefile b/Makefile
--- a/Makefile
+++ b/Makefile
@@ -31,6 +31,7 @@
   eg/tree \
   eg/bst \
   bench/candidates \
+  bench/redundants \
   bench/ill-hit \
   bench/longshot \
   bench/lowtests \
diff --git a/bench/redundants.hs b/bench/redundants.hs
new file mode 100644
--- /dev/null
+++ b/bench/redundants.hs
@@ -0,0 +1,115 @@
+-- Print redundant candidates
+--
+-- Copyright (C) 2023 Rudy Matela
+-- Distributed under the 3-Clause BSD licence (see the file LICENSE).
+import Conjure
+
+-- This script needs some internal utilities of Conjure:
+import Conjure.Engine
+import Conjure.Defn
+import Conjure.Utils
+
+
+-- | This function prints redundant candidates.
+--
+-- The arguments are, in their respective order:
+--
+-- * maximum candidate size (5 = few seconds, 7 = few minutes);
+-- * function name (for pretty-printing purposes);
+-- * proxy value to indicate the type of functions to generate;
+-- * list of primitives, in Conjure-compatible form.
+printRedundantCandidates :: Conjurable f => Int -> String -> f -> [Prim] -> IO ()
+printRedundantCandidates n nm f ps  =  do
+  putStrLn $ "Redundant candidates for: " ++ nm ++ " :: " ++ show (typeOf f)
+  putStrLn $ "  pruning with " ++ show nRules ++ "/" ++ show nREs ++ " rules"
+  putStrLn $ "  " ++ show (map length css) ++ " candidates"
+  putStrLn $ "  " ++ show numUnique ++ "/" ++ show numCandidates ++ " unique candidates"
+  putStrLn $ "  " ++ show numRedundant ++ "/" ++ show numCandidates ++ " redundant candidates"
+  putStrLn ""
+  printThy thy
+  putStrLn $ unlines . map showClass $ filter (\xs -> length xs > 1) $ classes
+  where
+  numCandidates  =  length candidates
+  numUnique      =  length classes
+  numRedundant   =  numCandidates - numUnique
+  classes        =  classifyBy (equalModuloTesting maxTests maxEvalRecursions nm f) candidates
+  candidates     =  concat css
+  css            =  take n css'
+  (css', thy)    =  candidateDefnsC args nm f ps  -- Conjure uses this for listing candidates
+  nRules         =  length (rules thy)
+  nREs           =  length (equations thy) + nRules
+  maxTests       =  360 -- a hardcoded value probably will not hurt in this simple benchmark
+  maxEvalRecursions  =  60
+
+  -- shows a class of candidates
+  showClass :: [Defn] -> String
+  showClass cs  =  unlines $ heading : map (indent . showDefn) cs
+    where
+    heading  =  "class of " ++ show (length cs) ++ " equivalent candidates:\n"
+
+
+main :: IO ()
+main  =  do
+
+  -- This N value limits the maximum size of candidates,
+  -- increase it to print redundant candidates of bigger size.
+  let n = 5
+  -- With n = 5, this should run in a few seconds.
+  -- With n = 7 and -O2 optimization,
+  -- this should take a few minutes to run and generate a ~300K text file.
+  -- We can also customize the n per-function below:
+
+  printRedundantCandidates n "foo" (undefined :: Int -> Int)
+    [ pr (0 :: Int)
+    , pr (1 :: Int)
+    , prim "+" ((+) :: Int -> Int -> Int)
+    , prim "*" ((+) :: Int -> Int -> Int)
+    , prim "-" ((-) :: Int -> Int -> Int)
+    ]
+
+  printRedundantCandidates n "?" (undefined :: Int -> Int -> Int)
+    [ pr (0 :: Int)
+    , prim "+" ((+) :: Int -> Int -> Int)
+    , prim "*" ((+) :: Int -> Int -> Int)
+    , prim "dec" (subtract 1 :: Int -> Int)
+    ]
+
+  printRedundantCandidates n "goo" (undefined :: [Int] -> [Int])
+    [ pr ([] :: [Int])
+    , prim ":" ((:) :: Int -> [Int] -> [Int])
+    , prim "++" ((++) :: [Int] -> [Int] -> [Int])
+    ]
+
+  printRedundantCandidates n "??" (undefined :: [Int] -> [Int] -> [Int])
+    [ pr ([] :: [Int])
+    , prim ":" ((:) :: Int -> [Int] -> [Int])
+    , prim "++" ((++) :: [Int] -> [Int] -> [Int])
+    ]
+
+  printRedundantCandidates n "ton" (undefined :: Bool -> Bool)
+    [ pr False
+    , pr True
+    , prim "&&" (&&)
+    , prim "||" (||)
+    , prim "not" not
+    ]
+
+  printRedundantCandidates n "&|" (undefined :: Bool -> Bool -> Bool)
+    [ pr False
+    , pr True
+    , prim "&&" (&&)
+    , prim "||" (||)
+    , prim "not" not
+    ]
+
+  -- Degenerate case:
+  -- lots of redundancy, since 0 `mod` 0 = undefined
+  -- Speculate is not able to discover that x `mod` x = 0
+  -- nevertheless useful for observing candidate filtering
+  -- through other means
+  {-
+  printRedundantCandidates n "gcd" (undefined :: Int -> Int -> Int)
+    [ pr (0::Int)
+    , prim "`mod`" (mod :: Int -> Int -> Int)
+    ]
+  -}
diff --git a/bench/redundants.out b/bench/redundants.out
new file mode 100644
--- /dev/null
+++ b/bench/redundants.out
@@ -0,0 +1,2117 @@
+Redundant candidates for: foo :: Int -> Int
+  pruning with 15/35 rules
+  [3,4,12,32,54] candidates
+  68/105 unique candidates
+  37/105 redundant candidates
+
+rules:
+x * y == x + y
+x * y == y + x
+x - x == 0
+x + 0 == x
+0 + x == x
+x - 0 == x
+(x + y) + z == x + (y + z)
+(x + y) + z == y + (x + z)
+x - (y - z) == z + (x - y)
+(x - y) - z == x - (y + z)
+(x - y) - z == x - (z + y)
+(x + y) - z == x + (y - z)
+(x + y) - z == y + (x - z)
+x + (y - x) == y
+(x - y) + y == x
+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 - z) == x + (y - z)
+(x - z) + y == x + (y - z)
+(z - y) + x == (x - y) + z
+y - (x + y) == 0 - x
+y - (y + x) == 0 - x
+z - (y + z) == x - (x + y)
+z - (y + z) == x - (y + x)
+z - (z + y) == x - (x + y)
+z - (z + y) == x - (y + x)
+x + (0 - y) == x - y
+(0 - y) + x == x - y
+x - (x + 1) == 0 - 1
+x - (1 + x) == 0 - 1
+y - (y + 1) == x - (x + 1)
+y - (y + 1) == x - (1 + x)
+y - (1 + y) == x - (1 + x)
+
+class of 4 equivalent candidates:
+
+    foo x  =  x
+
+    foo 0  =  0
+    foo x  =  x
+
+    foo 1  =  1
+    foo x  =  x
+
+    foo 0  =  0
+    foo 1  =  1
+    foo x  =  x
+
+
+class of 2 equivalent candidates:
+
+    foo 0  =  0
+    foo x  =  1
+
+    foo 0  =  0
+    foo 1  =  1
+    foo x  =  1
+
+
+class of 2 equivalent candidates:
+
+    foo 0  =  1
+    foo x  =  x
+
+    foo 0  =  1
+    foo 1  =  1
+    foo x  =  x
+
+
+class of 2 equivalent candidates:
+
+    foo 0  =  1
+    foo x  =  0
+
+    foo 0  =  1
+    foo 1  =  0
+    foo x  =  0
+
+
+class of 2 equivalent candidates:
+
+    foo x  =  x + x
+
+    foo 0  =  0
+    foo x  =  x + x
+
+
+class of 4 equivalent candidates:
+
+    foo x  =  x + 1
+
+    foo x  =  1 + x
+
+    foo 0  =  1
+    foo x  =  x + 1
+
+    foo 0  =  1
+    foo x  =  1 + x
+
+
+class of 4 equivalent candidates:
+
+    foo x  =  x - 1
+
+    foo x  =  (0 - 1) + x
+
+    foo x  =  x + (0 - 1)
+
+    foo 1  =  0
+    foo x  =  x - 1
+
+
+class of 5 equivalent candidates:
+
+    foo x  =  0 - x
+
+    foo 0  =  0
+    foo x  =  0 - x
+
+    foo x  =  x - (x + x)
+
+    foo x  =  1 - (x + 1)
+
+    foo x  =  1 - (1 + x)
+
+
+class of 4 equivalent candidates:
+
+    foo x  =  0 - 1
+
+    foo x  =  x - (x + 1)
+
+    foo x  =  x - (1 + x)
+
+    foo x  =  1 - (1 + 1)
+
+
+class of 5 equivalent candidates:
+
+    foo x  =  1 - x
+
+    foo 0  =  1
+    foo x  =  1 - x
+
+    foo x  =  (0 - x) + 1
+
+    foo x  =  1 + (0 - x)
+
+    foo 1  =  0
+    foo x  =  1 - x
+
+
+class of 2 equivalent candidates:
+
+    foo 1  =  0
+    foo x  =  x
+
+    foo 0  =  0
+    foo 1  =  0
+    foo x  =  x
+
+
+class of 2 equivalent candidates:
+
+    foo 1  =  0
+    foo x  =  1
+
+    foo 0  =  1
+    foo 1  =  0
+    foo x  =  1
+
+
+class of 2 equivalent candidates:
+
+    foo 1  =  1
+    foo x  =  0
+
+    foo 0  =  0
+    foo 1  =  1
+    foo x  =  0
+
+
+class of 2 equivalent candidates:
+
+    foo 0  =  0
+    foo x  =  x + 1
+
+    foo 0  =  0
+    foo x  =  1 + x
+
+
+class of 2 equivalent candidates:
+
+    foo x  =  (x - 1) + x
+
+    foo x  =  x + (x - 1)
+
+
+class of 2 equivalent candidates:
+
+    foo x  =  (1 - x) + 1
+
+    foo x  =  1 + (1 - x)
+
+
+class of 3 equivalent candidates:
+
+    foo x  =  x + (x + 1)
+
+    foo x  =  x + (1 + x)
+
+    foo x  =  1 + (x + x)
+
+
+class of 3 equivalent candidates:
+
+    foo x  =  x + (1 + 1)
+
+    foo x  =  1 + (x + 1)
+
+    foo x  =  1 + (1 + x)
+
+
+class of 2 equivalent candidates:
+
+    foo x  =  0 - (x + 1)
+
+    foo x  =  0 - (1 + x)
+
+
+class of 2 equivalent candidates:
+
+    foo 1  =  0
+    foo x  =  x + 1
+
+    foo 1  =  0
+    foo x  =  1 + x
+
+
+class of 2 equivalent candidates:
+
+    foo 1  =  1
+    foo x  =  x + 1
+
+    foo 1  =  1
+    foo x  =  1 + x
+
+
+
+Redundant candidates for: ? :: Int -> Int -> Int
+  pruning with 10/23 rules
+  [3,10,40,116,338] candidates
+  363/507 unique candidates
+  144/507 redundant candidates
+
+rules:
+x * y == x + y
+x * y == y + x
+x + 0 == x
+0 + x == x
+dec (x + y) == x + dec y
+dec (x + y) == y + dec x
+dec (x + y) == dec x + y
+dec (x + y) == dec y + x
+(x + y) + z == x + (y + z)
+(x + y) + z == y + (x + z)
+equations:
+y + x == x + y
+y + dec x == x + dec y
+dec x + y == x + dec y
+dec y + x == dec x + y
+x + dec 0 == dec x
+dec 0 + x == dec x
+y + (x + z) == x + (y + z)
+z + (x + y) == x + (y + z)
+z + (y + x) == x + (y + z)
+y + dec (dec x) == x + dec (dec y)
+dec (dec x) + y == x + dec (dec y)
+x + dec (dec 0) == dec (dec x)
+dec (dec 0) + x == dec (dec x)
+
+class of 2 equivalent candidates:
+
+    x ? y  =  x
+
+    0 ? x  =  0
+    x ? y  =  x
+
+
+class of 2 equivalent candidates:
+
+    x ? y  =  y
+
+    x ? 0  =  0
+    x ? y  =  y
+
+
+class of 3 equivalent candidates:
+
+    x ? y  =  0
+
+    x ? 0  =  0
+    x ? y  =  dec x ? 0
+
+    0 ? x  =  0
+    x ? y  =  0 ? dec y
+
+
+class of 4 equivalent candidates:
+
+    x ? y  =  dec x
+
+    x ? y  =  dec 0 + x
+
+    x ? y  =  x + dec 0
+
+    0 ? x  =  dec 0
+    x ? y  =  dec x
+
+
+class of 4 equivalent candidates:
+
+    x ? y  =  dec y
+
+    x ? y  =  dec 0 + y
+
+    x ? y  =  y + dec 0
+
+    x ? 0  =  dec 0
+    x ? y  =  dec y
+
+
+class of 2 equivalent candidates:
+
+    x ? 0  =  x
+    x ? y  =  y
+
+    0 ? 0  =  0
+    0 ? x  =  x
+    x ? 0  =  x
+    x ? y  =  y
+
+
+class of 2 equivalent candidates:
+
+    x ? 0  =  x
+    x ? y  =  0
+
+    0 ? 0  =  0
+    0 ? x  =  0
+    x ? 0  =  x
+    x ? y  =  0
+
+
+class of 2 equivalent candidates:
+
+    x ? 0  =  0
+    x ? y  =  x
+
+    0 ? 0  =  0
+    0 ? x  =  0
+    x ? 0  =  0
+    x ? y  =  x
+
+
+class of 2 equivalent candidates:
+
+    0 ? x  =  x
+    x ? y  =  0
+
+    0 ? 0  =  0
+    0 ? x  =  x
+    x ? 0  =  0
+    x ? y  =  0
+
+
+class of 2 equivalent candidates:
+
+    0 ? x  =  0
+    x ? y  =  y
+
+    0 ? 0  =  0
+    0 ? x  =  0
+    x ? 0  =  0
+    x ? y  =  y
+
+
+class of 2 equivalent candidates:
+
+    x ? y  =  x + x
+
+    0 ? x  =  0
+    x ? y  =  x + x
+
+
+class of 8 equivalent candidates:
+
+    x ? y  =  x + y
+
+    x ? y  =  y + x
+
+    x ? 0  =  x
+    x ? y  =  x + y
+
+    x ? 0  =  x
+    x ? y  =  y + x
+
+    0 ? x  =  x
+    x ? y  =  x + y
+
+    0 ? x  =  x
+    x ? y  =  y + x
+
+    0 ? 0  =  0
+    0 ? x  =  x
+    x ? 0  =  x
+    x ? y  =  x + y
+
+    0 ? 0  =  0
+    0 ? x  =  x
+    x ? 0  =  x
+    x ? y  =  y + x
+
+
+class of 2 equivalent candidates:
+
+    x ? y  =  y + y
+
+    x ? 0  =  0
+    x ? y  =  y + y
+
+
+class of 5 equivalent candidates:
+
+    x ? y  =  dec (dec x)
+
+    x ? y  =  dec (dec 0) + x
+
+    x ? y  =  x + dec (dec 0)
+
+    x ? y  =  dec x + dec 0
+
+    x ? y  =  dec 0 + dec x
+
+
+class of 5 equivalent candidates:
+
+    x ? y  =  dec (dec y)
+
+    x ? y  =  dec (dec 0) + y
+
+    x ? y  =  y + dec (dec 0)
+
+    x ? y  =  dec y + dec 0
+
+    x ? y  =  dec 0 + dec y
+
+
+class of 2 equivalent candidates:
+
+    x ? y  =  dec (dec 0)
+
+    x ? y  =  dec 0 + dec 0
+
+
+class of 5 equivalent candidates:
+
+    x ? 0  =  x
+    x ? y  =  dec x
+
+    x ? 0  =  x
+    x ? y  =  dec x ? 0
+
+    x ? 0  =  x
+    x ? y  =  dec 0 + x
+
+    x ? 0  =  x
+    x ? y  =  x + dec 0
+
+    0 ? 0  =  0
+    0 ? x  =  dec 0
+    x ? 0  =  x
+    x ? y  =  dec x
+
+
+class of 4 equivalent candidates:
+
+    x ? 0  =  x
+    x ? y  =  dec y
+
+    x ? 0  =  x
+    x ? y  =  dec 0 + y
+
+    x ? 0  =  x
+    x ? y  =  y + dec 0
+
+    0 ? 0  =  0
+    0 ? x  =  dec x
+    x ? 0  =  x
+    x ? y  =  dec y
+
+
+class of 2 equivalent candidates:
+
+    x ? 0  =  x
+    x ? y  =  dec 0
+
+    0 ? 0  =  0
+    0 ? x  =  dec 0
+    x ? 0  =  x
+    x ? y  =  dec 0
+
+
+class of 4 equivalent candidates:
+
+    x ? 0  =  0
+    x ? y  =  dec x
+
+    x ? 0  =  0
+    x ? y  =  dec 0 + x
+
+    x ? 0  =  0
+    x ? y  =  x + dec 0
+
+    0 ? 0  =  0
+    0 ? x  =  dec 0
+    x ? 0  =  0
+    x ? y  =  dec x
+
+
+class of 3 equivalent candidates:
+
+    x ? 0  =  0
+    x ? y  =  dec y
+
+    x ? 0  =  0
+    x ? y  =  dec 0 + y
+
+    x ? 0  =  0
+    x ? y  =  y + dec 0
+
+
+class of 4 equivalent candidates:
+
+    x ? 0  =  dec x
+    x ? y  =  x
+
+    x ? 0  =  dec 0 + x
+    x ? y  =  x
+
+    x ? 0  =  x + dec 0
+    x ? y  =  x
+
+    0 ? 0  =  dec 0
+    0 ? x  =  0
+    x ? 0  =  dec x
+    x ? y  =  x
+
+
+class of 4 equivalent candidates:
+
+    x ? 0  =  dec x
+    x ? y  =  y
+
+    x ? 0  =  dec 0 + x
+    x ? y  =  y
+
+    x ? 0  =  x + dec 0
+    x ? y  =  y
+
+    0 ? 0  =  dec 0
+    0 ? x  =  x
+    x ? 0  =  dec x
+    x ? y  =  y
+
+
+class of 4 equivalent candidates:
+
+    x ? 0  =  dec x
+    x ? y  =  0
+
+    x ? 0  =  dec 0 + x
+    x ? y  =  0
+
+    x ? 0  =  x + dec 0
+    x ? y  =  0
+
+    0 ? 0  =  dec 0
+    0 ? x  =  0
+    x ? 0  =  dec x
+    x ? y  =  0
+
+
+class of 2 equivalent candidates:
+
+    x ? 0  =  dec 0
+    x ? y  =  x
+
+    0 ? 0  =  dec 0
+    0 ? x  =  0
+    x ? 0  =  dec 0
+    x ? y  =  x
+
+
+class of 4 equivalent candidates:
+
+    0 ? x  =  x
+    x ? y  =  dec x
+
+    0 ? x  =  x
+    x ? y  =  dec 0 + x
+
+    0 ? x  =  x
+    x ? y  =  x + dec 0
+
+    0 ? 0  =  0
+    0 ? x  =  x
+    x ? 0  =  dec x
+    x ? y  =  dec x
+
+
+class of 5 equivalent candidates:
+
+    0 ? x  =  x
+    x ? y  =  dec y
+
+    0 ? x  =  x
+    x ? y  =  0 ? dec y
+
+    0 ? x  =  x
+    x ? y  =  dec 0 + y
+
+    0 ? x  =  x
+    x ? y  =  y + dec 0
+
+    0 ? 0  =  0
+    0 ? x  =  x
+    x ? 0  =  dec 0
+    x ? y  =  dec y
+
+
+class of 2 equivalent candidates:
+
+    0 ? x  =  x
+    x ? y  =  dec 0
+
+    0 ? 0  =  0
+    0 ? x  =  x
+    x ? 0  =  dec 0
+    x ? y  =  dec 0
+
+
+class of 3 equivalent candidates:
+
+    0 ? x  =  0
+    x ? y  =  dec x
+
+    0 ? x  =  0
+    x ? y  =  dec 0 + x
+
+    0 ? x  =  0
+    x ? y  =  x + dec 0
+
+
+class of 4 equivalent candidates:
+
+    0 ? x  =  0
+    x ? y  =  dec y
+
+    0 ? x  =  0
+    x ? y  =  dec 0 + y
+
+    0 ? x  =  0
+    x ? y  =  y + dec 0
+
+    0 ? 0  =  0
+    0 ? x  =  0
+    x ? 0  =  dec 0
+    x ? y  =  dec y
+
+
+class of 4 equivalent candidates:
+
+    0 ? x  =  dec x
+    x ? y  =  x
+
+    0 ? x  =  dec 0 + x
+    x ? y  =  x
+
+    0 ? x  =  x + dec 0
+    x ? y  =  x
+
+    0 ? 0  =  dec 0
+    0 ? x  =  dec x
+    x ? 0  =  x
+    x ? y  =  x
+
+
+class of 4 equivalent candidates:
+
+    0 ? x  =  dec x
+    x ? y  =  y
+
+    0 ? x  =  dec 0 + x
+    x ? y  =  y
+
+    0 ? x  =  x + dec 0
+    x ? y  =  y
+
+    0 ? 0  =  dec 0
+    0 ? x  =  dec x
+    x ? 0  =  0
+    x ? y  =  y
+
+
+class of 4 equivalent candidates:
+
+    0 ? x  =  dec x
+    x ? y  =  0
+
+    0 ? x  =  dec 0 + x
+    x ? y  =  0
+
+    0 ? x  =  x + dec 0
+    x ? y  =  0
+
+    0 ? 0  =  dec 0
+    0 ? x  =  dec x
+    x ? 0  =  0
+    x ? y  =  0
+
+
+class of 2 equivalent candidates:
+
+    0 ? x  =  dec 0
+    x ? y  =  y
+
+    0 ? 0  =  dec 0
+    0 ? x  =  dec 0
+    x ? 0  =  0
+    x ? y  =  y
+
+
+class of 2 equivalent candidates:
+
+    x ? y  =  dec x + x
+
+    x ? y  =  x + dec x
+
+
+class of 4 equivalent candidates:
+
+    x ? y  =  dec x + y
+
+    x ? y  =  dec y + x
+
+    x ? y  =  x + dec y
+
+    x ? y  =  y + dec x
+
+
+class of 2 equivalent candidates:
+
+    x ? y  =  dec y + y
+
+    x ? y  =  y + dec y
+
+
+class of 2 equivalent candidates:
+
+    x ? 0  =  x
+    x ? y  =  x + x
+
+    0 ? 0  =  0
+    0 ? x  =  0
+    x ? 0  =  x
+    x ? y  =  x + x
+
+
+class of 2 equivalent candidates:
+
+    x ? 0  =  0
+    x ? y  =  x + x
+
+    0 ? 0  =  0
+    0 ? x  =  0
+    x ? 0  =  0
+    x ? y  =  x + x
+
+
+class of 4 equivalent candidates:
+
+    x ? 0  =  0
+    x ? y  =  x + y
+
+    x ? 0  =  0
+    x ? y  =  y + x
+
+    0 ? 0  =  0
+    0 ? x  =  x
+    x ? 0  =  0
+    x ? y  =  x + y
+
+    0 ? 0  =  0
+    0 ? x  =  x
+    x ? 0  =  0
+    x ? y  =  y + x
+
+
+class of 2 equivalent candidates:
+
+    x ? 0  =  x + x
+    x ? y  =  x
+
+    0 ? 0  =  0
+    0 ? x  =  0
+    x ? 0  =  x + x
+    x ? y  =  x
+
+
+class of 2 equivalent candidates:
+
+    x ? 0  =  x + x
+    x ? y  =  y
+
+    0 ? 0  =  0
+    0 ? x  =  x
+    x ? 0  =  x + x
+    x ? y  =  y
+
+
+class of 2 equivalent candidates:
+
+    x ? 0  =  x + x
+    x ? y  =  0
+
+    0 ? 0  =  0
+    0 ? x  =  0
+    x ? 0  =  x + x
+    x ? y  =  0
+
+
+class of 2 equivalent candidates:
+
+    0 ? x  =  x
+    x ? y  =  y + y
+
+    0 ? 0  =  0
+    0 ? x  =  x
+    x ? 0  =  0
+    x ? y  =  y + y
+
+
+class of 4 equivalent candidates:
+
+    0 ? x  =  0
+    x ? y  =  x + y
+
+    0 ? x  =  0
+    x ? y  =  y + x
+
+    0 ? 0  =  0
+    0 ? x  =  0
+    x ? 0  =  x
+    x ? y  =  x + y
+
+    0 ? 0  =  0
+    0 ? x  =  0
+    x ? 0  =  x
+    x ? y  =  y + x
+
+
+class of 2 equivalent candidates:
+
+    0 ? x  =  0
+    x ? y  =  y + y
+
+    0 ? 0  =  0
+    0 ? x  =  0
+    x ? 0  =  0
+    x ? y  =  y + y
+
+
+class of 2 equivalent candidates:
+
+    0 ? x  =  x + x
+    x ? y  =  x
+
+    0 ? 0  =  0
+    0 ? x  =  x + x
+    x ? 0  =  x
+    x ? y  =  x
+
+
+class of 2 equivalent candidates:
+
+    0 ? x  =  x + x
+    x ? y  =  y
+
+    0 ? 0  =  0
+    0 ? x  =  x + x
+    x ? 0  =  0
+    x ? y  =  y
+
+
+class of 2 equivalent candidates:
+
+    0 ? x  =  x + x
+    x ? y  =  0
+
+    0 ? 0  =  0
+    0 ? x  =  x + x
+    x ? 0  =  0
+    x ? y  =  0
+
+
+class of 3 equivalent candidates:
+
+    x ? y  =  dec (dec x) + x
+
+    x ? y  =  x + dec (dec x)
+
+    x ? y  =  dec x + dec x
+
+
+class of 6 equivalent candidates:
+
+    x ? y  =  dec (dec x) + y
+
+    x ? y  =  dec (dec y) + x
+
+    x ? y  =  x + dec (dec y)
+
+    x ? y  =  y + dec (dec x)
+
+    x ? y  =  dec x + dec y
+
+    x ? y  =  dec y + dec x
+
+
+class of 3 equivalent candidates:
+
+    x ? y  =  dec (dec y) + y
+
+    x ? y  =  y + dec (dec y)
+
+    x ? y  =  dec y + dec y
+
+
+class of 3 equivalent candidates:
+
+    x ? y  =  x + (x + y)
+
+    x ? y  =  x + (y + x)
+
+    x ? y  =  y + (x + x)
+
+
+class of 3 equivalent candidates:
+
+    x ? y  =  x + (y + y)
+
+    x ? y  =  y + (x + y)
+
+    x ? y  =  y + (y + x)
+
+
+class of 2 equivalent candidates:
+
+    x ? 0  =  x
+    x ? y  =  dec x + x
+
+    x ? 0  =  x
+    x ? y  =  x + dec x
+
+
+class of 4 equivalent candidates:
+
+    x ? 0  =  x
+    x ? y  =  dec x + y
+
+    x ? 0  =  x
+    x ? y  =  dec y + x
+
+    x ? 0  =  x
+    x ? y  =  x + dec y
+
+    x ? 0  =  x
+    x ? y  =  y + dec x
+
+
+class of 2 equivalent candidates:
+
+    x ? 0  =  x
+    x ? y  =  dec y + y
+
+    x ? 0  =  x
+    x ? y  =  y + dec y
+
+
+class of 2 equivalent candidates:
+
+    x ? 0  =  0
+    x ? y  =  dec x + x
+
+    x ? 0  =  0
+    x ? y  =  x + dec x
+
+
+class of 4 equivalent candidates:
+
+    x ? 0  =  0
+    x ? y  =  dec x + y
+
+    x ? 0  =  0
+    x ? y  =  dec y + x
+
+    x ? 0  =  0
+    x ? y  =  x + dec y
+
+    x ? 0  =  0
+    x ? y  =  y + dec x
+
+
+class of 2 equivalent candidates:
+
+    x ? 0  =  0
+    x ? y  =  dec y + y
+
+    x ? 0  =  0
+    x ? y  =  y + dec y
+
+
+class of 2 equivalent candidates:
+
+    x ? 0  =  dec x
+    x ? y  =  x + y
+
+    x ? 0  =  dec x
+    x ? y  =  y + x
+
+
+class of 2 equivalent candidates:
+
+    x ? 0  =  dec 0
+    x ? y  =  x + y
+
+    x ? 0  =  dec 0
+    x ? y  =  y + x
+
+
+class of 2 equivalent candidates:
+
+    x ? 0  =  dec x + x
+    x ? y  =  x
+
+    x ? 0  =  x + dec x
+    x ? y  =  x
+
+
+class of 2 equivalent candidates:
+
+    x ? 0  =  dec x + x
+    x ? y  =  y
+
+    x ? 0  =  x + dec x
+    x ? y  =  y
+
+
+class of 2 equivalent candidates:
+
+    x ? 0  =  dec x + x
+    x ? y  =  0
+
+    x ? 0  =  x + dec x
+    x ? y  =  0
+
+
+class of 2 equivalent candidates:
+
+    0 ? x  =  x
+    x ? y  =  dec x + x
+
+    0 ? x  =  x
+    x ? y  =  x + dec x
+
+
+class of 4 equivalent candidates:
+
+    0 ? x  =  x
+    x ? y  =  dec x + y
+
+    0 ? x  =  x
+    x ? y  =  dec y + x
+
+    0 ? x  =  x
+    x ? y  =  x + dec y
+
+    0 ? x  =  x
+    x ? y  =  y + dec x
+
+
+class of 2 equivalent candidates:
+
+    0 ? x  =  x
+    x ? y  =  dec y + y
+
+    0 ? x  =  x
+    x ? y  =  y + dec y
+
+
+class of 2 equivalent candidates:
+
+    0 ? x  =  0
+    x ? y  =  dec x + x
+
+    0 ? x  =  0
+    x ? y  =  x + dec x
+
+
+class of 4 equivalent candidates:
+
+    0 ? x  =  0
+    x ? y  =  dec x + y
+
+    0 ? x  =  0
+    x ? y  =  dec y + x
+
+    0 ? x  =  0
+    x ? y  =  x + dec y
+
+    0 ? x  =  0
+    x ? y  =  y + dec x
+
+
+class of 2 equivalent candidates:
+
+    0 ? x  =  0
+    x ? y  =  dec y + y
+
+    0 ? x  =  0
+    x ? y  =  y + dec y
+
+
+class of 2 equivalent candidates:
+
+    0 ? x  =  dec x
+    x ? y  =  x + y
+
+    0 ? x  =  dec x
+    x ? y  =  y + x
+
+
+class of 2 equivalent candidates:
+
+    0 ? x  =  dec 0
+    x ? y  =  x + y
+
+    0 ? x  =  dec 0
+    x ? y  =  y + x
+
+
+class of 2 equivalent candidates:
+
+    0 ? x  =  dec x + x
+    x ? y  =  x
+
+    0 ? x  =  x + dec x
+    x ? y  =  x
+
+
+class of 2 equivalent candidates:
+
+    0 ? x  =  dec x + x
+    x ? y  =  y
+
+    0 ? x  =  x + dec x
+    x ? y  =  y
+
+
+class of 2 equivalent candidates:
+
+    0 ? x  =  dec x + x
+    x ? y  =  0
+
+    0 ? x  =  x + dec x
+    x ? y  =  0
+
+
+class of 2 equivalent candidates:
+
+    0 ? 0  =  0
+    0 ? x  =  0
+    x ? 0  =  0
+    x ? y  =  x + y
+
+    0 ? 0  =  0
+    0 ? x  =  0
+    x ? 0  =  0
+    x ? y  =  y + x
+
+
+
+Redundant candidates for: goo :: [Int] -> [Int]
+  pruning with 4/4 rules
+  [2,1,2,3,4] candidates
+  9/12 unique candidates
+  3/12 redundant candidates
+
+rules:
+xs ++ [] == xs
+[] ++ xs == xs
+(xs ++ ys) ++ zs == xs ++ (ys ++ zs)
+(x:xs) ++ ys == x:(xs ++ ys)
+
+class of 3 equivalent candidates:
+
+    goo xs  =  xs
+
+    goo []  =  []
+    goo (x:xs)  =  x:xs
+
+    goo []  =  []
+    goo (x:xs)  =  x:goo xs
+
+
+class of 2 equivalent candidates:
+
+    goo xs  =  []
+
+    goo []  =  []
+    goo (x:xs)  =  goo xs
+
+
+
+Redundant candidates for: ?? :: [Int] -> [Int] -> [Int]
+  pruning with 4/4 rules
+  [3,7,13,66,152] candidates
+  161/241 unique candidates
+  80/241 redundant candidates
+
+rules:
+xs ++ [] == xs
+[] ++ xs == xs
+(xs ++ ys) ++ zs == xs ++ (ys ++ zs)
+(x:xs) ++ ys == x:(xs ++ ys)
+
+class of 4 equivalent candidates:
+
+    xs ?? ys  =  xs
+
+    xs ?? []  =  xs
+    xs ?? (x:ys)  =  xs ?? ys
+
+    xs ?? []  =  xs
+    xs ?? (x:ys)  =  xs ?? []
+
+    [] ?? xs  =  []
+    (x:xs) ?? ys  =  x:xs
+
+
+class of 4 equivalent candidates:
+
+    xs ?? ys  =  ys
+
+    [] ?? xs  =  xs
+    (x:xs) ?? ys  =  xs ?? ys
+
+    [] ?? xs  =  xs
+    (x:xs) ?? ys  =  [] ?? ys
+
+    xs ?? []  =  []
+    xs ?? (x:ys)  =  x:ys
+
+
+class of 29 equivalent candidates:
+
+    xs ?? ys  =  []
+
+    xs ?? []  =  []
+    xs ?? (x:ys)  =  xs ?? ys
+
+    xs ?? []  =  []
+    xs ?? (x:ys)  =  xs ?? []
+
+    xs ?? []  =  []
+    xs ?? (x:ys)  =  ys ?? xs
+
+    xs ?? []  =  []
+    xs ?? (x:ys)  =  ys ?? ys
+
+    xs ?? []  =  []
+    xs ?? (x:ys)  =  ys ?? []
+
+    xs ?? []  =  []
+    xs ?? (x:ys)  =  [] ?? xs
+
+    xs ?? []  =  []
+    xs ?? (x:ys)  =  [] ?? ys
+
+    [] ?? xs  =  []
+    (x:xs) ?? ys  =  xs ?? xs
+
+    [] ?? xs  =  []
+    (x:xs) ?? ys  =  xs ?? ys
+
+    [] ?? xs  =  []
+    (x:xs) ?? ys  =  xs ?? []
+
+    [] ?? xs  =  []
+    (x:xs) ?? ys  =  ys ?? xs
+
+    [] ?? xs  =  []
+    (x:xs) ?? ys  =  ys ?? []
+
+    [] ?? xs  =  []
+    (x:xs) ?? ys  =  [] ?? xs
+
+    [] ?? xs  =  []
+    (x:xs) ?? ys  =  [] ?? ys
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  xs ?? xs
+    (x:xs) ?? []  =  []
+    (x:xs) ?? (y:ys)  =  []
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  xs ?? []
+    (x:xs) ?? []  =  []
+    (x:xs) ?? (y:ys)  =  []
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  [] ?? xs
+    (x:xs) ?? []  =  []
+    (x:xs) ?? (y:ys)  =  []
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  []
+    (x:xs) ?? []  =  xs ?? xs
+    (x:xs) ?? (y:ys)  =  []
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  []
+    (x:xs) ?? []  =  xs ?? []
+    (x:xs) ?? (y:ys)  =  []
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  []
+    (x:xs) ?? []  =  [] ?? xs
+    (x:xs) ?? (y:ys)  =  []
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  []
+    (x:xs) ?? []  =  []
+    (x:xs) ?? (y:ys)  =  xs ?? xs
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  []
+    (x:xs) ?? []  =  []
+    (x:xs) ?? (y:ys)  =  xs ?? ys
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  []
+    (x:xs) ?? []  =  []
+    (x:xs) ?? (y:ys)  =  xs ?? []
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  []
+    (x:xs) ?? []  =  []
+    (x:xs) ?? (y:ys)  =  ys ?? xs
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  []
+    (x:xs) ?? []  =  []
+    (x:xs) ?? (y:ys)  =  ys ?? ys
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  []
+    (x:xs) ?? []  =  []
+    (x:xs) ?? (y:ys)  =  ys ?? []
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  []
+    (x:xs) ?? []  =  []
+    (x:xs) ?? (y:ys)  =  [] ?? xs
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  []
+    (x:xs) ?? []  =  []
+    (x:xs) ?? (y:ys)  =  [] ?? ys
+
+
+class of 3 equivalent candidates:
+
+    xs ?? []  =  xs
+    xs ?? (x:ys)  =  ys
+
+    xs ?? []  =  xs
+    xs ?? (x:ys)  =  ys ?? []
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  xs
+    (x:xs) ?? []  =  x:xs
+    (x:xs) ?? (y:ys)  =  ys
+
+
+class of 5 equivalent candidates:
+
+    xs ?? []  =  xs
+    xs ?? (x:ys)  =  []
+
+    xs ?? []  =  xs
+    xs ?? (x:ys)  =  ys ?? ys
+
+    xs ?? []  =  xs
+    xs ?? (x:ys)  =  [] ?? xs
+
+    xs ?? []  =  xs
+    xs ?? (x:ys)  =  [] ?? ys
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  []
+    (x:xs) ?? []  =  x:xs
+    (x:xs) ?? (y:ys)  =  []
+
+
+class of 2 equivalent candidates:
+
+    xs ?? []  =  []
+    xs ?? (x:ys)  =  xs
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  []
+    (x:xs) ?? []  =  []
+    (x:xs) ?? (y:ys)  =  x:xs
+
+
+class of 2 equivalent candidates:
+
+    xs ?? []  =  []
+    xs ?? (x:ys)  =  ys
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  xs
+    (x:xs) ?? []  =  xs ?? []
+    (x:xs) ?? (y:ys)  =  ys
+
+
+class of 5 equivalent candidates:
+
+    [] ?? xs  =  xs
+    (x:xs) ?? ys  =  []
+
+    [] ?? xs  =  xs
+    (x:xs) ?? ys  =  xs ?? xs
+
+    [] ?? xs  =  xs
+    (x:xs) ?? ys  =  xs ?? []
+
+    [] ?? xs  =  xs
+    (x:xs) ?? ys  =  ys ?? []
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  x:xs
+    (x:xs) ?? []  =  []
+    (x:xs) ?? (y:ys)  =  []
+
+
+class of 2 equivalent candidates:
+
+    [] ?? xs  =  []
+    (x:xs) ?? ys  =  xs
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  [] ?? xs
+    (x:xs) ?? []  =  xs
+    (x:xs) ?? (y:ys)  =  xs
+
+
+class of 2 equivalent candidates:
+
+    [] ?? xs  =  []
+    (x:xs) ?? ys  =  ys
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  []
+    (x:xs) ?? []  =  []
+    (x:xs) ?? (y:ys)  =  y:ys
+
+
+class of 3 equivalent candidates:
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  xs
+    (x:xs) ?? []  =  xs
+    (x:xs) ?? (y:ys)  =  []
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  xs
+    (x:xs) ?? []  =  xs
+    (x:xs) ?? (y:ys)  =  xs ?? xs
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  xs
+    (x:xs) ?? []  =  xs
+    (x:xs) ?? (y:ys)  =  ys ?? ys
+
+
+class of 2 equivalent candidates:
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  xs
+    (x:xs) ?? []  =  []
+    (x:xs) ?? (y:ys)  =  xs
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  xs
+    (x:xs) ?? []  =  xs ?? []
+    (x:xs) ?? (y:ys)  =  xs
+
+
+class of 7 equivalent candidates:
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  xs
+    (x:xs) ?? []  =  []
+    (x:xs) ?? (y:ys)  =  []
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  xs
+    (x:xs) ?? []  =  xs ?? xs
+    (x:xs) ?? (y:ys)  =  []
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  xs
+    (x:xs) ?? []  =  xs ?? []
+    (x:xs) ?? (y:ys)  =  []
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  xs
+    (x:xs) ?? []  =  []
+    (x:xs) ?? (y:ys)  =  xs ?? xs
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  xs
+    (x:xs) ?? []  =  []
+    (x:xs) ?? (y:ys)  =  xs ?? []
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  xs
+    (x:xs) ?? []  =  []
+    (x:xs) ?? (y:ys)  =  ys ?? ys
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  xs
+    (x:xs) ?? []  =  []
+    (x:xs) ?? (y:ys)  =  ys ?? []
+
+
+class of 2 equivalent candidates:
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  []
+    (x:xs) ?? []  =  xs
+    (x:xs) ?? (y:ys)  =  ys
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  [] ?? xs
+    (x:xs) ?? []  =  xs
+    (x:xs) ?? (y:ys)  =  ys
+
+
+class of 7 equivalent candidates:
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  []
+    (x:xs) ?? []  =  xs
+    (x:xs) ?? (y:ys)  =  []
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  xs ?? xs
+    (x:xs) ?? []  =  xs
+    (x:xs) ?? (y:ys)  =  []
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  [] ?? xs
+    (x:xs) ?? []  =  xs
+    (x:xs) ?? (y:ys)  =  []
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  []
+    (x:xs) ?? []  =  xs
+    (x:xs) ?? (y:ys)  =  xs ?? xs
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  []
+    (x:xs) ?? []  =  xs
+    (x:xs) ?? (y:ys)  =  ys ?? ys
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  []
+    (x:xs) ?? []  =  xs
+    (x:xs) ?? (y:ys)  =  [] ?? xs
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  []
+    (x:xs) ?? []  =  xs
+    (x:xs) ?? (y:ys)  =  [] ?? ys
+
+
+class of 5 equivalent candidates:
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  []
+    (x:xs) ?? []  =  []
+    (x:xs) ?? (y:ys)  =  xs
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  xs ?? []
+    (x:xs) ?? []  =  []
+    (x:xs) ?? (y:ys)  =  xs
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  [] ?? xs
+    (x:xs) ?? []  =  []
+    (x:xs) ?? (y:ys)  =  xs
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  []
+    (x:xs) ?? []  =  xs ?? []
+    (x:xs) ?? (y:ys)  =  xs
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  []
+    (x:xs) ?? []  =  [] ?? xs
+    (x:xs) ?? (y:ys)  =  xs
+
+
+class of 5 equivalent candidates:
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  []
+    (x:xs) ?? []  =  []
+    (x:xs) ?? (y:ys)  =  ys
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  xs ?? []
+    (x:xs) ?? []  =  []
+    (x:xs) ?? (y:ys)  =  ys
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  [] ?? xs
+    (x:xs) ?? []  =  []
+    (x:xs) ?? (y:ys)  =  ys
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  []
+    (x:xs) ?? []  =  xs ?? []
+    (x:xs) ?? (y:ys)  =  ys
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  []
+    (x:xs) ?? []  =  [] ?? xs
+    (x:xs) ?? (y:ys)  =  ys
+
+
+class of 2 equivalent candidates:
+
+    [] ?? xs  =  xs
+    (x:xs) ?? ys  =  [] ?? xs
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  x:xs
+    (x:xs) ?? []  =  xs
+    (x:xs) ?? (y:ys)  =  xs
+
+
+class of 2 equivalent candidates:
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  xs
+    (x:xs) ?? []  =  xs
+    (x:xs) ?? (y:ys)  =  xs ?? ys
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  xs
+    (x:xs) ?? []  =  xs
+    (x:xs) ?? (y:ys)  =  ys ?? xs
+
+
+class of 2 equivalent candidates:
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  xs
+    (x:xs) ?? []  =  xs
+    (x:xs) ?? (y:ys)  =  xs ?? []
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  xs
+    (x:xs) ?? []  =  xs
+    (x:xs) ?? (y:ys)  =  [] ?? xs
+
+
+class of 2 equivalent candidates:
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  xs
+    (x:xs) ?? []  =  xs
+    (x:xs) ?? (y:ys)  =  ys ?? []
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  xs
+    (x:xs) ?? []  =  xs
+    (x:xs) ?? (y:ys)  =  [] ?? ys
+
+
+class of 2 equivalent candidates:
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  xs
+    (x:xs) ?? []  =  xs ?? xs
+    (x:xs) ?? (y:ys)  =  xs
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  xs
+    (x:xs) ?? []  =  [] ?? xs
+    (x:xs) ?? (y:ys)  =  xs
+
+
+class of 2 equivalent candidates:
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  xs
+    (x:xs) ?? []  =  xs ?? xs
+    (x:xs) ?? (y:ys)  =  ys
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  xs
+    (x:xs) ?? []  =  [] ?? xs
+    (x:xs) ?? (y:ys)  =  ys
+
+
+class of 2 equivalent candidates:
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  xs ?? xs
+    (x:xs) ?? []  =  xs
+    (x:xs) ?? (y:ys)  =  xs
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  xs ?? []
+    (x:xs) ?? []  =  xs
+    (x:xs) ?? (y:ys)  =  xs
+
+
+class of 2 equivalent candidates:
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  xs ?? xs
+    (x:xs) ?? []  =  xs
+    (x:xs) ?? (y:ys)  =  ys
+
+    [] ?? []  =  []
+    [] ?? (x:xs)  =  xs ?? []
+    (x:xs) ?? []  =  xs
+    (x:xs) ?? (y:ys)  =  ys
+
+
+
+Redundant candidates for: ton :: Bool -> Bool
+  pruning with 39/49 rules
+  [3,3,0,0,0] candidates
+  4/6 unique candidates
+  2/6 redundant candidates
+
+rules:
+not False == True
+not True == False
+p && p == p
+p || p == p
+not (not p) == p
+p && False == False
+p && True == p
+False && p == False
+True && p == p
+p || False == p
+p || True == True
+False || p == p
+True || p == True
+not (p && q) == not p || not q
+not (p && q) == not q || not p
+not (p || q) == not p && not q
+not (p || q) == not q && not p
+p && not p == False
+not p && p == False
+p || not p == True
+not p || p == True
+(p && q) && r == p && (q && r)
+(p && q) && r == q && (p && r)
+(p || q) || r == p || (q || r)
+(p || q) || r == q || (p || r)
+p && (p && q) == p && q
+p && (q && p) == p && q
+p && (q && p) == q && p
+p || (p || q) == p || q
+p || (q || p) == p || q
+p || (q || p) == q || p
+p && (p || q) == p
+p && (q || p) == p
+(p || q) && p == p
+(p || q) && q == q
+p || p && q == p
+p || q && p == p
+p && q || p == p
+p && q || q == q
+equations:
+q && p == p && q
+q || p == p || q
+q && (p && r) == p && (q && r)
+r && (p && q) == p && (q && r)
+r && (q && p) == p && (q && r)
+q || (p || r) == p || (q || r)
+r || (p || q) == p || (q || r)
+r || (q || p) == p || (q || r)
+(r || q) && p == p && (q || r)
+r && q || p == p || q && r
+
+class of 2 equivalent candidates:
+
+    ton p  =  p
+
+    ton False  =  False
+    ton True  =  True
+
+
+class of 2 equivalent candidates:
+
+    ton p  =  not p
+
+    ton False  =  True
+    ton True  =  False
+
+
+
+Redundant candidates for: &| :: Bool -> Bool -> Bool
+  pruning with 39/49 rules
+  [4,14,26,8,4] candidates
+  16/56 unique candidates
+  40/56 redundant candidates
+
+rules:
+not False == True
+not True == False
+p && p == p
+p || p == p
+not (not p) == p
+p && False == False
+p && True == p
+False && p == False
+True && p == p
+p || False == p
+p || True == True
+False || p == p
+True || p == True
+not (p && q) == not p || not q
+not (p && q) == not q || not p
+not (p || q) == not p && not q
+not (p || q) == not q && not p
+p && not p == False
+not p && p == False
+p || not p == True
+not p || p == True
+(p && q) && r == p && (q && r)
+(p && q) && r == q && (p && r)
+(p || q) || r == p || (q || r)
+(p || q) || r == q || (p || r)
+p && (p && q) == p && q
+p && (q && p) == p && q
+p && (q && p) == q && p
+p || (p || q) == p || q
+p || (q || p) == p || q
+p || (q || p) == q || p
+p && (p || q) == p
+p && (q || p) == p
+(p || q) && p == p
+(p || q) && q == q
+p || p && q == p
+p || q && p == p
+p && q || p == p
+p && q || q == q
+equations:
+q && p == p && q
+q || p == p || q
+q && (p && r) == p && (q && r)
+r && (p && q) == p && (q && r)
+r && (q && p) == p && (q && r)
+q || (p || r) == p || (q || r)
+r || (p || q) == p || (q || r)
+r || (q || p) == p || (q || r)
+(r || q) && p == p && (q || r)
+r && q || p == p || q && r
+
+class of 2 equivalent candidates:
+
+    p &| q  =  p
+
+    False &| p  =  False
+    True &| p  =  True
+
+
+class of 2 equivalent candidates:
+
+    p &| q  =  q
+
+    p &| False  =  False
+    p &| True  =  True
+
+
+class of 2 equivalent candidates:
+
+    p &| q  =  not p
+
+    False &| p  =  True
+    True &| p  =  False
+
+
+class of 2 equivalent candidates:
+
+    p &| q  =  not q
+
+    p &| False  =  True
+    p &| True  =  False
+
+
+class of 5 equivalent candidates:
+
+    p &| False  =  p
+    p &| True  =  False
+
+    False &| p  =  False
+    True &| p  =  not p
+
+    False &| False  =  False
+    False &| True  =  False
+    True &| False  =  True
+    True &| True  =  False
+
+    p &| q  =  not q && p
+
+    p &| q  =  p && not q
+
+
+class of 5 equivalent candidates:
+
+    p &| False  =  p
+    p &| True  =  True
+
+    False &| p  =  p
+    True &| p  =  True
+
+    p &| q  =  p || q
+
+    p &| q  =  q || p
+
+    False &| False  =  False
+    False &| True  =  True
+    True &| False  =  True
+    True &| True  =  True
+
+
+class of 5 equivalent candidates:
+
+    p &| False  =  False
+    p &| True  =  p
+
+    False &| p  =  False
+    True &| p  =  p
+
+    p &| q  =  p && q
+
+    p &| q  =  q && p
+
+    False &| False  =  False
+    False &| True  =  False
+    True &| False  =  False
+    True &| True  =  True
+
+
+class of 5 equivalent candidates:
+
+    p &| False  =  True
+    p &| True  =  p
+
+    False &| p  =  not p
+    True &| p  =  True
+
+    False &| False  =  True
+    False &| True  =  False
+    True &| False  =  True
+    True &| True  =  True
+
+    p &| q  =  not q || p
+
+    p &| q  =  p || not q
+
+
+class of 5 equivalent candidates:
+
+    False &| p  =  p
+    True &| p  =  False
+
+    p &| False  =  False
+    p &| True  =  not p
+
+    False &| False  =  False
+    False &| True  =  True
+    True &| False  =  False
+    True &| True  =  False
+
+    p &| q  =  not p && q
+
+    p &| q  =  q && not p
+
+
+class of 5 equivalent candidates:
+
+    False &| p  =  True
+    True &| p  =  p
+
+    p &| False  =  not p
+    p &| True  =  True
+
+    False &| False  =  True
+    False &| True  =  True
+    True &| False  =  False
+    True &| True  =  True
+
+    p &| q  =  not p || q
+
+    p &| q  =  q || not p
+
+
+class of 3 equivalent candidates:
+
+    p &| False  =  p
+    p &| True  =  not p
+
+    False &| p  =  p
+    True &| p  =  not p
+
+    False &| False  =  False
+    False &| True  =  True
+    True &| False  =  True
+    True &| True  =  False
+
+
+class of 5 equivalent candidates:
+
+    p &| False  =  True
+    p &| True  =  not p
+
+    False &| p  =  True
+    True &| p  =  not p
+
+    False &| False  =  True
+    False &| True  =  True
+    True &| False  =  True
+    True &| True  =  False
+
+    p &| q  =  not p || not q
+
+    p &| q  =  not q || not p
+
+
+class of 3 equivalent candidates:
+
+    p &| False  =  not p
+    p &| True  =  p
+
+    False &| p  =  not p
+    True &| p  =  p
+
+    False &| False  =  True
+    False &| True  =  False
+    True &| False  =  False
+    True &| True  =  True
+
+
+class of 5 equivalent candidates:
+
+    p &| False  =  not p
+    p &| True  =  False
+
+    False &| p  =  not p
+    True &| p  =  False
+
+    False &| False  =  True
+    False &| True  =  False
+    True &| False  =  False
+    True &| True  =  False
+
+    p &| q  =  not p && not q
+
+    p &| q  =  not q && not p
+
+
+
diff --git a/bench/runtime/zero/bench/candidates.runtime b/bench/runtime/zero/bench/candidates.runtime
--- a/bench/runtime/zero/bench/candidates.runtime
+++ b/bench/runtime/zero/bench/candidates.runtime
@@ -1,1 +1,1 @@
-11.0
+10.9
diff --git a/bench/runtime/zero/bench/gps.runtime b/bench/runtime/zero/bench/gps.runtime
--- a/bench/runtime/zero/bench/gps.runtime
+++ b/bench/runtime/zero/bench/gps.runtime
@@ -1,1 +1,1 @@
-23.2
+26.2
diff --git a/bench/runtime/zero/bench/gps2.runtime b/bench/runtime/zero/bench/gps2.runtime
--- a/bench/runtime/zero/bench/gps2.runtime
+++ b/bench/runtime/zero/bench/gps2.runtime
@@ -1,1 +1,1 @@
-9.0
+9.3
diff --git a/bench/runtime/zero/bench/redundants.runtime b/bench/runtime/zero/bench/redundants.runtime
new file mode 100644
--- /dev/null
+++ b/bench/runtime/zero/bench/redundants.runtime
@@ -0,0 +1,1 @@
+3.7
diff --git a/bench/runtime/zero/bench/take-drop.runtime b/bench/runtime/zero/bench/take-drop.runtime
--- a/bench/runtime/zero/bench/take-drop.runtime
+++ b/bench/runtime/zero/bench/take-drop.runtime
@@ -1,1 +1,1 @@
-0.5
+0.6
diff --git a/bench/runtime/zero/bench/terpret.runtime b/bench/runtime/zero/bench/terpret.runtime
--- a/bench/runtime/zero/bench/terpret.runtime
+++ b/bench/runtime/zero/bench/terpret.runtime
@@ -1,1 +1,1 @@
-12.4
+12.0
diff --git a/bench/runtime/zero/eg/bools.runtime b/bench/runtime/zero/eg/bools.runtime
--- a/bench/runtime/zero/eg/bools.runtime
+++ b/bench/runtime/zero/eg/bools.runtime
@@ -1,1 +1,1 @@
-3.2
+3.1
diff --git a/bench/runtime/zero/eg/bst.runtime b/bench/runtime/zero/eg/bst.runtime
--- a/bench/runtime/zero/eg/bst.runtime
+++ b/bench/runtime/zero/eg/bst.runtime
@@ -1,1 +1,1 @@
-6.5
+6.6
diff --git a/bench/runtime/zero/eg/factorial.runtime b/bench/runtime/zero/eg/factorial.runtime
--- a/bench/runtime/zero/eg/factorial.runtime
+++ b/bench/runtime/zero/eg/factorial.runtime
@@ -1,1 +1,1 @@
-2.5
+2.4
diff --git a/bench/runtime/zero/eg/fib01.runtime b/bench/runtime/zero/eg/fib01.runtime
--- a/bench/runtime/zero/eg/fib01.runtime
+++ b/bench/runtime/zero/eg/fib01.runtime
@@ -1,1 +1,1 @@
-4.5
+5.7
diff --git a/bench/runtime/zero/eg/fibonacci.runtime b/bench/runtime/zero/eg/fibonacci.runtime
--- a/bench/runtime/zero/eg/fibonacci.runtime
+++ b/bench/runtime/zero/eg/fibonacci.runtime
@@ -1,1 +1,1 @@
-4.6
+4.7
diff --git a/bench/runtime/zero/eg/list.runtime b/bench/runtime/zero/eg/list.runtime
--- a/bench/runtime/zero/eg/list.runtime
+++ b/bench/runtime/zero/eg/list.runtime
@@ -1,1 +1,1 @@
-1.3
+1.2
diff --git a/bench/runtime/zero/eg/pow.runtime b/bench/runtime/zero/eg/pow.runtime
--- a/bench/runtime/zero/eg/pow.runtime
+++ b/bench/runtime/zero/eg/pow.runtime
@@ -1,1 +1,1 @@
-3.9
+3.7
diff --git a/bench/runtime/zero/eg/replicate.runtime b/bench/runtime/zero/eg/replicate.runtime
--- a/bench/runtime/zero/eg/replicate.runtime
+++ b/bench/runtime/zero/eg/replicate.runtime
@@ -1,1 +1,1 @@
-0.5
+0.4
diff --git a/bench/runtime/zero/eg/setelem.runtime b/bench/runtime/zero/eg/setelem.runtime
--- a/bench/runtime/zero/eg/setelem.runtime
+++ b/bench/runtime/zero/eg/setelem.runtime
@@ -1,1 +1,1 @@
-2.0
+1.9
diff --git a/bench/runtime/zero/eg/sort.runtime b/bench/runtime/zero/eg/sort.runtime
--- a/bench/runtime/zero/eg/sort.runtime
+++ b/bench/runtime/zero/eg/sort.runtime
@@ -1,1 +1,1 @@
-1.0
+1.2
diff --git a/bench/runtime/zero/eg/spec.runtime b/bench/runtime/zero/eg/spec.runtime
--- a/bench/runtime/zero/eg/spec.runtime
+++ b/bench/runtime/zero/eg/spec.runtime
@@ -1,1 +1,1 @@
-1.1
+1.0
diff --git a/bench/runtime/zero/eg/tree.runtime b/bench/runtime/zero/eg/tree.runtime
--- a/bench/runtime/zero/eg/tree.runtime
+++ b/bench/runtime/zero/eg/tree.runtime
@@ -1,1 +1,1 @@
-2.0
+1.9
diff --git a/bench/runtime/zero/versions b/bench/runtime/zero/versions
--- a/bench/runtime/zero/versions
+++ b/bench/runtime/zero/versions
@@ -1,4 +1,4 @@
 GHC 9.0.2
 leancheck-1.0.0
-express-1.0.10
+express-1.0.12
 speculate-0.4.14
diff --git a/changelog.md b/changelog.md
--- a/changelog.md
+++ b/changelog.md
@@ -2,6 +2,15 @@
 ============================
 
 
+v0.5.6
+------
+
+* `Conjure` module: no main API changes
+* `Conjure.Engine`: add `equalModuloTesting`
+* `Conjure.Utils`: add some misc functions
+* add `bench/redundants` that reports groups of redundant candidates
+
+
 v0.5.4
 ------
 
diff --git a/code-conjure.cabal b/code-conjure.cabal
--- a/code-conjure.cabal
+++ b/code-conjure.cabal
@@ -3,7 +3,7 @@
 -- Copyright (C) 2021 Rudy Matela
 -- Distributed under the 3-Clause BSD licence (see the file LICENSE).
 name:                code-conjure
-version:             0.5.4
+version:             0.5.6
 synopsis:            synthesize Haskell functions out of partial definitions
 description:
   Conjure is a tool that synthesizes Haskell functions out of partial definitions.
@@ -60,7 +60,7 @@
 source-repository this
   type:            git
   location:        https://github.com/rudymatela/conjure
-  tag:             v0.5.4
+  tag:             v0.5.6
 
 library
   exposed-modules: Conjure
diff --git a/mk/depend.mk b/mk/depend.mk
--- a/mk/depend.mk
+++ b/mk/depend.mk
@@ -107,6 +107,19 @@
   src/Conjure/Conjurable.hs \
   src/Conjure/Conjurable/Derive.hs \
   bench/p30.hs
+bench/redundants: \
+  bench/redundants.hs \
+  mk/toplibs
+bench/redundants.o: \
+  src/Conjure/Utils.hs \
+  src/Conjure/Prim.hs \
+  src/Conjure.hs \
+  src/Conjure/Expr.hs \
+  src/Conjure/Engine.hs \
+  src/Conjure/Defn.hs \
+  src/Conjure/Conjurable.hs \
+  src/Conjure/Conjurable/Derive.hs \
+  bench/redundants.hs
 bench/self: \
   bench/self.hs \
   mk/toplibs
diff --git a/src/Conjure/Engine.hs b/src/Conjure/Engine.hs
--- a/src/Conjure/Engine.hs
+++ b/src/Conjure/Engine.hs
@@ -31,6 +31,7 @@
   , candidateDefnsC
   , conjureTheory
   , conjureTheoryWith
+  , equalModuloTesting
   , module Data.Express
   , module Data.Express.Fixtures
   , module Test.Speculate.Engine
@@ -336,7 +337,12 @@
 
 
 nubCandidates :: Conjurable f => Args -> String -> f -> [[Defn]] -> [[Defn]]
-nubCandidates Args{..} nm f  =  discardLaterT (===)
+nubCandidates Args{..} nm f  =
+  discardLaterT $ equalModuloTesting maxTests maxEvalRecursions nm f
+
+
+equalModuloTesting :: Conjurable f => Int -> Int -> String -> f -> Defn -> Defn -> Bool
+equalModuloTesting maxTests maxEvalRecursions nm f  =  (===)
   where
   err  =  error "nubCandidates: unexpected evaluation error."
   eq  =  conjureDynamicEq f
diff --git a/src/Conjure/Utils.hs b/src/Conjure/Utils.hs
--- a/src/Conjure/Utils.hs
+++ b/src/Conjure/Utils.hs
@@ -32,6 +32,11 @@
   , choices
   , choicesThat
   , foldr0
+  , indent
+  , indentBy
+  , classify   -- from LeanCheck.Stats
+  , classifyBy -- from LeanCheck.Stats
+  , classifyOn -- from LeanCheck.Stats
   )
 where
 
@@ -44,6 +49,8 @@
 
 import System.IO.Unsafe
 
+import Test.LeanCheck.Stats (classify, classifyBy, classifyOn)
+
 -- | Checks if all elements of a list are equal.
 --
 -- Exceptionally this function returns false for an empty or unit list.
@@ -134,3 +141,11 @@
 foldr0 :: (a -> a -> a) -> a -> [a] -> a
 foldr0 f z xs | null xs   = z
               | otherwise = foldr1 f xs
+
+-- | Indents a block of text by 4 spaces
+indent :: String -> String
+indent  =  indentBy 4
+
+-- | Indents a block of text with the provided amount of spaces
+indentBy :: Int -> String -> String
+indentBy n  =  unlines . map (replicate n ' ' ++) . lines