diff --git a/.gitignore b/.gitignore
--- a/.gitignore
+++ b/.gitignore
@@ -53,6 +53,8 @@
 eg/sort
 eg/subset
 eg/spec
+bench/carry-on
+bench/strategies
 bench/self
 bench/longshot
 bench/ill-hit
@@ -67,6 +69,7 @@
 bench/lowtests
 bench/terpret
 bench/weird
+bench/unique
 proto/u-conjure
 test/expr
 test/conjurable
diff --git a/Makefile b/Makefile
--- a/Makefile
+++ b/Makefile
@@ -44,13 +44,16 @@
   bench/ill-hit \
   bench/longshot \
   bench/lowtests \
+  bench/strategies \
   bench/self \
+  bench/carry-on \
   bench/take-drop \
   bench/p12 \
   bench/p30 \
   bench/gps \
   bench/gps2 \
   bench/terpret \
+  bench/unique \
   bench/weird \
   proto/u-conjure
 
@@ -128,7 +131,10 @@
 	./$<
 
 %.txt: %
-	./$< >$<.txt
+	./$< >$@
+
+%.tee: %
+	$(LONG) unbuffer ./$< | tee $<.txt
 
 %.diff: %
 	./$< | diff -rud $<.txt -
diff --git a/bench/candidates.txt b/bench/candidates.txt
--- a/bench/candidates.txt
+++ b/bench/candidates.txt
@@ -1,7 +1,7 @@
 Candidates for: foo :: Int -> Int
   pruning with 27/65 rules
-  [3,0,8,0,30,0,194,0,1406] direct candidates, 0 duplicates
-  [3,3,9,10,32,39,197,247,1325] pattern candidates, 0 duplicates
+  [3,0,8,0,30,0,177,0,1203] direct candidates, 0 duplicates
+  [3,3,9,10,32,39,185,233,1169] pattern candidates, 0 duplicates
 
 rules:
 x - x == 0
@@ -430,8 +430,8 @@
 
 Candidates for: ? :: Int -> Int -> Int
   pruning with 13/34 rules
-  [3,3,9,18,60,162,516,1587,5148] direct candidates, 0 duplicates
-  [3,8,25,71,205,632,1976,6067,19140] pattern candidates, 0 duplicates
+  [3,3,9,18,60,162,489,1475,4619] direct candidates, 0 duplicates
+  [3,8,25,71,205,632,1957,5906,18303] pattern candidates, 0 duplicates
 
 rules:
 x * 0 == 0
@@ -3394,8 +3394,8 @@
 
 Candidates for: &| :: Bool -> Bool -> Bool
   pruning with 39/49 rules
-  [4,2,2,4,2,16,18,60,120] direct candidates, 0 duplicates
-  [4,14,26,10,2,16,18,60,120] pattern candidates, 0 duplicates
+  [4,2,2,4,2,16,17,56,110] direct candidates, 0 duplicates
+  [4,14,26,10,2,16,17,56,110] pattern candidates, 0 duplicates
 
 rules:
 not False == True
diff --git a/bench/carry-on.hs b/bench/carry-on.hs
new file mode 100644
--- /dev/null
+++ b/bench/carry-on.hs
@@ -0,0 +1,33 @@
+-- carryon.hs: conjuring implementations of a factorial function
+--
+-- Copyright (C) 2021-2024 Rudy Matela
+-- Distributed under the 3-Clause BSD licence (see the file LICENSE).
+import Conjure
+
+factorial :: Int -> Int
+factorial 1  =  1
+factorial 2  =  2
+factorial 3  =  6
+factorial 4  =  24
+
+
+main :: IO ()
+main  =  do
+  -- carry on Conjuring larger implementations
+  conjureWith args{carryOn = True, maxSize = 11} "factorial n" factorial
+    [ pr (0::Int)
+    , pr (1::Int)
+    , prim "+" ((+) :: Int -> Int -> Int)
+    , prim "*" ((*) :: Int -> Int -> Int)
+    , prim "-" ((-) :: Int -> Int -> Int)
+    ]
+  -- should produce:
+  -- factorial 0  =  1
+  -- factorial x  =  x * factorial (x - 1)
+  --
+  -- and
+  -- factorial 0  =  1
+  -- factorial 1  =  1
+  -- factorial x  =  x * factorial (x - 1)
+  --
+  -- among other implementations
diff --git a/bench/carry-on.txt b/bench/carry-on.txt
new file mode 100644
--- /dev/null
+++ b/bench/carry-on.txt
@@ -0,0 +1,47 @@
+factorial :: Int -> Int
+-- testing 4 combinations of argument values
+-- pruning with 27/65 rules
+-- looking through 3 candidates of size 1
+-- looking through 3 candidates of size 2
+-- looking through 7 candidates of size 3
+-- looking through 8 candidates of size 4
+-- looking through 28 candidates of size 5
+-- looking through 35 candidates of size 6
+-- looking through 167 candidates of size 7
+-- tested 95 candidates
+factorial 0  =  1
+factorial x  =  x * factorial (x - 1)
+
+-- looking through 203 candidates of size 8
+-- tested 254 candidates
+factorial 1  =  1
+factorial x  =  x * factorial (x - 1)
+
+-- looking through 1048 candidates of size 9
+-- tested 547 candidates
+factorial 0  =  0
+factorial 1  =  1
+factorial x  =  x * factorial (x - 1)
+
+-- tested 555 candidates
+factorial 0  =  1
+factorial 1  =  1
+factorial x  =  x * factorial (x - 1)
+
+-- looking through 1301 candidates of size 10
+-- looking through 7201 candidates of size 11
+-- tested 3216 candidates
+factorial 0  =  1
+factorial x  =  x + x * (factorial (x - 1) - 1)
+
+-- tested 3396 candidates
+factorial 0  =  1
+factorial x  =  x - x * (1 - factorial (x - 1))
+
+-- tested 3519 candidates
+factorial 0  =  1
+factorial x  =  (0 - x) * (0 - factorial (x - 1))
+
+-- tested 10004 candidates
+cannot conjure
+
diff --git a/bench/erroneous.txt b/bench/erroneous.txt
--- a/bench/erroneous.txt
+++ b/bench/erroneous.txt
@@ -1,7 +1,7 @@
 Erroneous candidates for: foo :: Int -> Int
   pruning with 41/82 rules
-  [4,8,16,42,70,162,493] candidates
-  30/795 erroneous candidates
+  [4,8,16,42,65,150,417] candidates
+  30/702 erroneous candidates
 
 foo 0  =  0
 foo x  =  x + foo (x - 2)
diff --git a/bench/gps.txt b/bench/gps.txt
--- a/bench/gps.txt
+++ b/bench/gps.txt
@@ -151,8 +151,8 @@
 -- looking through 4 candidates of size 5
 -- looking through 86 candidates of size 6
 -- looking through 5 candidates of size 7
--- looking through 537 candidates of size 8
--- tested 588 candidates
+-- looking through 513 candidates of size 8
+-- tested 564 candidates
 wallisNext (x % y)  =  (y + 1) % (x + 1)
 
 wallisNext :: Ratio Integer -> Ratio Integer
@@ -235,7 +235,7 @@
 -- looking through 13 candidates of size 5
 -- looking through 51 candidates of size 6
 -- looking through 103 candidates of size 7
--- looking through 365 candidates of size 8
+-- looking through 360 candidates of size 8
 -- tested 267 candidates
 gps13 qs  =  foldr (+) 0 qs / fromIntegral (length qs)
 
@@ -244,10 +244,10 @@
 -- pruning with 12/13 rules
 -- looking through 0 candidates of size 1
 -- looking through 0 candidates of size 2
--- looking through 4 candidates of size 3
--- looking through 3 candidates of size 4
--- looking through 39 candidates of size 5
--- tested 20 candidates
+-- looking through 3 candidates of size 3
+-- looking through 2 candidates of size 4
+-- looking through 37 candidates of size 5
+-- tested 17 candidates
 odd x  =  0 /= x `mod` 2
 
 gps14 :: [Int] -> Int
@@ -268,9 +268,9 @@
 -- looking through 0 candidates of size 3
 -- looking through 27 candidates of size 4
 -- looking through 30 candidates of size 5
--- looking through 258 candidates of size 6
--- looking through 474 candidates of size 7
--- tested 378 candidates
+-- looking through 240 candidates of size 6
+-- looking through 453 candidates of size 7
+-- tested 353 candidates
 gps14 []  =  0
 gps14 (x:xs)  =  x + gps14 xs `mod` 2
 
@@ -304,10 +304,10 @@
 -- looking through 8 candidates of size 4
 -- looking through 28 candidates of size 5
 -- looking through 35 candidates of size 6
--- looking through 179 candidates of size 7
--- looking through 217 candidates of size 8
--- looking through 1196 candidates of size 9
--- tested 492 candidates
+-- looking through 167 candidates of size 7
+-- looking through 203 candidates of size 8
+-- looking through 1048 candidates of size 9
+-- tested 466 candidates
 gps17 0  =  0
 gps17 x  =  gps17 (x - 1) + x * x
 
@@ -459,9 +459,9 @@
 -- looking through 13 candidates of size 6
 -- looking through 30 candidates of size 7
 -- looking through 75 candidates of size 8
--- looking through 195 candidates of size 9
--- looking through 474 candidates of size 10
--- tested 457 candidates
+-- looking through 194 candidates of size 9
+-- looking through 470 candidates of size 10
+-- tested 456 candidates
 gps24 cs  =  chr (ord ' ' + sum (map ord cs) `mod` 64)
 
 gps25 :: Int -> [Int]
diff --git a/bench/gps2.txt b/bench/gps2.txt
--- a/bench/gps2.txt
+++ b/bench/gps2.txt
@@ -155,11 +155,11 @@
 -- looking through 0 candidates of size 3
 -- looking through 68 candidates of size 4
 -- looking through 80 candidates of size 5
--- looking through 1084 candidates of size 6
--- looking through 1556 candidates of size 7
--- looking through 20600 candidates of size 8
--- looking through 35632 candidates of size 9
--- tested 29538 candidates
+-- looking through 980 candidates of size 6
+-- looking through 1428 candidates of size 7
+-- looking through 17324 candidates of size 8
+-- looking through 30724 candidates of size 9
+-- tested 25024 candidates
 gps10 []  =  0
 gps10 (x:xs)  =  gps10 xs + (x `div` 3 - 2)
 
diff --git a/bench/runtime/lapmatrud/bench/candidates.runtime b/bench/runtime/lapmatrud/bench/candidates.runtime
--- a/bench/runtime/lapmatrud/bench/candidates.runtime
+++ b/bench/runtime/lapmatrud/bench/candidates.runtime
@@ -1,1 +1,1 @@
-10.8
+9.1
diff --git a/bench/runtime/lapmatrud/bench/carry-on.runtime b/bench/runtime/lapmatrud/bench/carry-on.runtime
new file mode 100644
--- /dev/null
+++ b/bench/runtime/lapmatrud/bench/carry-on.runtime
@@ -0,0 +1,1 @@
+2.5
diff --git a/bench/runtime/lapmatrud/bench/erroneous.runtime b/bench/runtime/lapmatrud/bench/erroneous.runtime
--- a/bench/runtime/lapmatrud/bench/erroneous.runtime
+++ b/bench/runtime/lapmatrud/bench/erroneous.runtime
@@ -1,1 +1,1 @@
-3.2
+2.7
diff --git a/bench/runtime/lapmatrud/bench/gps.runtime b/bench/runtime/lapmatrud/bench/gps.runtime
--- a/bench/runtime/lapmatrud/bench/gps.runtime
+++ b/bench/runtime/lapmatrud/bench/gps.runtime
@@ -1,1 +1,1 @@
-15.8
+14.1
diff --git a/bench/runtime/lapmatrud/bench/gps2.runtime b/bench/runtime/lapmatrud/bench/gps2.runtime
--- a/bench/runtime/lapmatrud/bench/gps2.runtime
+++ b/bench/runtime/lapmatrud/bench/gps2.runtime
@@ -1,1 +1,1 @@
-14.3
+12.1
diff --git a/bench/runtime/lapmatrud/bench/p12.runtime b/bench/runtime/lapmatrud/bench/p12.runtime
--- a/bench/runtime/lapmatrud/bench/p12.runtime
+++ b/bench/runtime/lapmatrud/bench/p12.runtime
@@ -1,1 +1,1 @@
-1.8
+1.6
diff --git a/bench/runtime/lapmatrud/bench/redundants.runtime b/bench/runtime/lapmatrud/bench/redundants.runtime
--- a/bench/runtime/lapmatrud/bench/redundants.runtime
+++ b/bench/runtime/lapmatrud/bench/redundants.runtime
@@ -1,1 +1,1 @@
-3.2
+2.9
diff --git a/bench/runtime/lapmatrud/bench/strategies.runtime b/bench/runtime/lapmatrud/bench/strategies.runtime
new file mode 100644
--- /dev/null
+++ b/bench/runtime/lapmatrud/bench/strategies.runtime
@@ -0,0 +1,1 @@
+4.4
diff --git a/bench/runtime/lapmatrud/bench/terpret.runtime b/bench/runtime/lapmatrud/bench/terpret.runtime
--- a/bench/runtime/lapmatrud/bench/terpret.runtime
+++ b/bench/runtime/lapmatrud/bench/terpret.runtime
@@ -1,1 +1,1 @@
-9.2
+7.9
diff --git a/bench/runtime/lapmatrud/bench/unique.runtime b/bench/runtime/lapmatrud/bench/unique.runtime
new file mode 100644
--- /dev/null
+++ b/bench/runtime/lapmatrud/bench/unique.runtime
@@ -0,0 +1,1 @@
+2.2
diff --git a/bench/runtime/lapmatrud/bench/weird.runtime b/bench/runtime/lapmatrud/bench/weird.runtime
--- a/bench/runtime/lapmatrud/bench/weird.runtime
+++ b/bench/runtime/lapmatrud/bench/weird.runtime
@@ -1,1 +1,1 @@
-3.3
+2.7
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 @@
-1.0
+0.9
diff --git a/bench/runtime/lapmatrud/eg/bools.runtime b/bench/runtime/lapmatrud/eg/bools.runtime
--- a/bench/runtime/lapmatrud/eg/bools.runtime
+++ b/bench/runtime/lapmatrud/eg/bools.runtime
@@ -1,1 +1,1 @@
-2.1
+1.8
diff --git a/bench/runtime/lapmatrud/eg/bst.runtime b/bench/runtime/lapmatrud/eg/bst.runtime
--- a/bench/runtime/lapmatrud/eg/bst.runtime
+++ b/bench/runtime/lapmatrud/eg/bst.runtime
@@ -1,1 +1,1 @@
-7.9
+7.5
diff --git a/bench/runtime/lapmatrud/eg/fib01.runtime b/bench/runtime/lapmatrud/eg/fib01.runtime
--- a/bench/runtime/lapmatrud/eg/fib01.runtime
+++ b/bench/runtime/lapmatrud/eg/fib01.runtime
@@ -1,1 +1,1 @@
-1.5
+1.4
diff --git a/bench/runtime/lapmatrud/eg/fibonacci.runtime b/bench/runtime/lapmatrud/eg/fibonacci.runtime
--- a/bench/runtime/lapmatrud/eg/fibonacci.runtime
+++ b/bench/runtime/lapmatrud/eg/fibonacci.runtime
@@ -1,1 +1,1 @@
-15.5
+3.3
diff --git a/bench/runtime/lapmatrud/eg/higher.runtime b/bench/runtime/lapmatrud/eg/higher.runtime
--- a/bench/runtime/lapmatrud/eg/higher.runtime
+++ b/bench/runtime/lapmatrud/eg/higher.runtime
@@ -1,1 +1,1 @@
-0.7
+0.6
diff --git a/bench/runtime/lapmatrud/eg/ints.runtime b/bench/runtime/lapmatrud/eg/ints.runtime
--- a/bench/runtime/lapmatrud/eg/ints.runtime
+++ b/bench/runtime/lapmatrud/eg/ints.runtime
@@ -1,1 +1,1 @@
-0.6
+0.5
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.2
+1.1
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 @@
-2.1
+1.5
diff --git a/bench/runtime/lapmatrud/eg/pow.runtime b/bench/runtime/lapmatrud/eg/pow.runtime
--- a/bench/runtime/lapmatrud/eg/pow.runtime
+++ b/bench/runtime/lapmatrud/eg/pow.runtime
@@ -1,1 +1,1 @@
-4.4
+4.1
diff --git a/bench/runtime/lapmatrud/eg/setelem.runtime b/bench/runtime/lapmatrud/eg/setelem.runtime
--- a/bench/runtime/lapmatrud/eg/setelem.runtime
+++ b/bench/runtime/lapmatrud/eg/setelem.runtime
@@ -1,1 +1,1 @@
-1.3
+1.1
diff --git a/bench/runtime/lapmatrud/eg/sort.runtime b/bench/runtime/lapmatrud/eg/sort.runtime
--- a/bench/runtime/lapmatrud/eg/sort.runtime
+++ b/bench/runtime/lapmatrud/eg/sort.runtime
@@ -1,1 +1,1 @@
-1.4
+1.3
diff --git a/bench/runtime/lapmatrud/eg/tree.runtime b/bench/runtime/lapmatrud/eg/tree.runtime
--- a/bench/runtime/lapmatrud/eg/tree.runtime
+++ b/bench/runtime/lapmatrud/eg/tree.runtime
@@ -1,1 +1,1 @@
-1.4
+1.2
diff --git a/bench/runtime/lapmatrud/versions b/bench/runtime/lapmatrud/versions
--- a/bench/runtime/lapmatrud/versions
+++ b/bench/runtime/lapmatrud/versions
@@ -1,4 +1,4 @@
 GHC 9.0.2
 leancheck-1.0.2
 express-1.0.16
-speculate-0.4.18
+speculate-0.4.20
diff --git a/bench/runtime/zero/bench/carry-on.runtime b/bench/runtime/zero/bench/carry-on.runtime
new file mode 100644
--- /dev/null
+++ b/bench/runtime/zero/bench/carry-on.runtime
@@ -0,0 +1,1 @@
+4.9
diff --git a/bench/runtime/zero/bench/strategies.runtime b/bench/runtime/zero/bench/strategies.runtime
new file mode 100644
--- /dev/null
+++ b/bench/runtime/zero/bench/strategies.runtime
@@ -0,0 +1,1 @@
+8.1
diff --git a/bench/runtime/zero/bench/unique.runtime b/bench/runtime/zero/bench/unique.runtime
new file mode 100644
--- /dev/null
+++ b/bench/runtime/zero/bench/unique.runtime
@@ -0,0 +1,1 @@
+4.5
diff --git a/bench/strategies.hs b/bench/strategies.hs
new file mode 100644
--- /dev/null
+++ b/bench/strategies.hs
@@ -0,0 +1,72 @@
+-- strategies.hs: conjuring factorial with different strategies
+--
+-- Copyright (C) 2021-2024 Rudy Matela
+-- Distributed under the 3-Clause BSD licence (see the file LICENSE).
+import Conjure
+
+factorial :: Int -> Int
+factorial 1  =  1
+factorial 2  =  2
+factorial 3  =  6
+factorial 4  =  24
+
+
+mkStrategy :: String -> Args
+mkStrategy s  =  args
+  { rewriting         =  r
+  , requireDescent    =  d
+  , adHocRedundancy   =  a
+  , copyBindings      =  a -- previously c
+  , uniqueCandidates  =  u
+--, carryOn  =  True
+--, maxSize  =  10
+  }
+  where
+  itob 0  =  False
+  itob _  =  True
+  [r,d,a,u]  =  map itob $
+    case s of
+    "unique candidates" -> [1,1,1,1]
+    "default"           -> [1,1,1,0]
+    "without reasoning" -> [0,1,1,0]
+    "without descent"   -> [1,0,1,0]
+    "without ad-hoc"    -> [1,1,0,0]
+    "only reasoning"    -> [1,0,0,0]
+    "only descent"      -> [0,1,0,0]
+    "only ad-hoc"       -> [0,0,1,0]
+    "only typed"        -> [0,0,0,0]
+    _                   -> error "unknown strategy"
+
+conjureStrategy :: Conjurable f => String -> String -> f -> [Prim] -> IO ()
+conjureStrategy name nm f prims  =  do
+  putStrLn $ "-- strategy: " ++ name
+  conjureWith (mkStrategy name) nm f prims
+
+strategies :: [String]
+strategies  =  
+  [ "unique candidates"
+  , "default"
+  , "without reasoning"
+  , "without descent"
+  , "without ad-hoc"
+  , "only reasoning"
+  , "only descent"
+  , "only ad-hoc"
+  , "only typed"
+  ]
+
+main :: IO ()
+main  =  do
+  sequence_
+    [ conjureStrategy s "factorial n" factorial primitives
+    | s <- strategies
+    ]
+
+primitives :: [Prim]
+primitives = 
+    [ pr (0::Int)
+    , pr (1::Int)
+    , prim "+" ((+) :: Int -> Int -> Int)
+    , prim "*" ((*) :: Int -> Int -> Int)
+    , prim "-" ((-) :: Int -> Int -> Int)
+    ]
diff --git a/bench/strategies.txt b/bench/strategies.txt
new file mode 100644
--- /dev/null
+++ b/bench/strategies.txt
@@ -0,0 +1,135 @@
+-- strategy: unique candidates
+factorial :: Int -> Int
+-- testing 4 combinations of argument values
+-- pruning with 27/65 rules
+-- looking through 3 candidates of size 1
+-- looking through 3 candidates of size 2
+-- looking through 7 candidates of size 3
+-- looking through 8 candidates of size 4
+-- looking through 23 candidates of size 5
+-- looking through 30 candidates of size 6
+-- looking through 82 candidates of size 7
+-- tested 84 candidates
+factorial 0  =  1
+factorial x  =  x * factorial (x - 1)
+
+-- strategy: default
+factorial :: Int -> Int
+-- testing 4 combinations of argument values
+-- pruning with 27/65 rules
+-- looking through 3 candidates of size 1
+-- looking through 3 candidates of size 2
+-- looking through 7 candidates of size 3
+-- looking through 8 candidates of size 4
+-- looking through 28 candidates of size 5
+-- looking through 35 candidates of size 6
+-- looking through 167 candidates of size 7
+-- tested 95 candidates
+factorial 0  =  1
+factorial x  =  x * factorial (x - 1)
+
+-- strategy: without reasoning
+factorial :: Int -> Int
+-- testing 4 combinations of argument values
+-- pruning with 27/65 rules
+-- looking through 3 candidates of size 1
+-- looking through 3 candidates of size 2
+-- looking through 16 candidates of size 3
+-- looking through 17 candidates of size 4
+-- looking through 279 candidates of size 5
+-- looking through 313 candidates of size 6
+-- looking through 5763 candidates of size 7
+-- tested 656 candidates
+factorial 0  =  1
+factorial x  =  x * factorial (x - 1)
+
+-- strategy: without descent
+factorial :: Int -> Int
+-- testing 4 combinations of argument values
+-- pruning with 27/65 rules
+-- looking through 3 candidates of size 1
+-- looking through 3 candidates of size 2
+-- looking through 7 candidates of size 3
+-- looking through 8 candidates of size 4
+-- looking through 28 candidates of size 5
+-- looking through 35 candidates of size 6
+-- looking through 252 candidates of size 7
+-- tested 148 candidates
+factorial 0  =  1
+factorial x  =  x * factorial (x - 1)
+
+-- strategy: without ad-hoc
+factorial :: Int -> Int
+-- testing 4 combinations of argument values
+-- pruning with 27/65 rules
+-- looking through 3 candidates of size 1
+-- looking through 6 candidates of size 2
+-- looking through 12 candidates of size 3
+-- looking through 24 candidates of size 4
+-- looking through 37 candidates of size 5
+-- looking through 72 candidates of size 6
+-- looking through 196 candidates of size 7
+-- tested 165 candidates
+factorial 0  =  1
+factorial x  =  x * factorial (x - 1)
+
+-- strategy: only reasoning
+factorial :: Int -> Int
+-- testing 4 combinations of argument values
+-- pruning with 27/65 rules
+-- looking through 3 candidates of size 1
+-- looking through 6 candidates of size 2
+-- looking through 12 candidates of size 3
+-- looking through 24 candidates of size 4
+-- looking through 47 candidates of size 5
+-- looking through 82 candidates of size 6
+-- looking through 342 candidates of size 7
+-- tested 284 candidates
+factorial 0  =  1
+factorial x  =  x * factorial (x - 1)
+
+-- strategy: only descent
+factorial :: Int -> Int
+-- testing 4 combinations of argument values
+-- pruning with 27/65 rules
+-- looking through 3 candidates of size 1
+-- looking through 6 candidates of size 2
+-- looking through 21 candidates of size 3
+-- looking through 42 candidates of size 4
+-- looking through 302 candidates of size 5
+-- looking through 602 candidates of size 6
+-- looking through 6115 candidates of size 7
+-- tested 1001 candidates
+factorial 0  =  1
+factorial x  =  x * factorial (x - 1)
+
+-- strategy: only ad-hoc
+factorial :: Int -> Int
+-- testing 4 combinations of argument values
+-- pruning with 27/65 rules
+-- looking through 3 candidates of size 1
+-- looking through 3 candidates of size 2
+-- looking through 16 candidates of size 3
+-- looking through 17 candidates of size 4
+-- looking through 279 candidates of size 5
+-- looking through 313 candidates of size 6
+-- looking through 6281 candidates of size 7
+-- tested 1004 candidates
+factorial 0  =  1
+factorial x  =  x * factorial (x - 1)
+
+-- strategy: only typed
+factorial :: Int -> Int
+-- testing 4 combinations of argument values
+-- pruning with 27/65 rules
+-- looking through 3 candidates of size 1
+-- looking through 6 candidates of size 2
+-- looking through 21 candidates of size 3
+-- looking through 42 candidates of size 4
+-- looking through 330 candidates of size 5
+-- looking through 630 candidates of size 6
+-- looking through 7215 candidates of size 7
+-- tested 1945 candidates
+factorial 0  =  1
+factorial x  =  x * factorial (x - 1)
+
diff --git a/bench/terpret.txt b/bench/terpret.txt
--- a/bench/terpret.txt
+++ b/bench/terpret.txt
@@ -58,8 +58,8 @@
 -- looking through 1242 candidates of size 8
 -- looking through 3087 candidates of size 9
 -- looking through 8937 candidates of size 10
--- looking through 102875 candidates of size 11
--- tested 40385 candidates
+-- looking through 102200 candidates of size 11
+-- tested 39710 candidates
 cshift (p,q,r)  =  if p
                    then (p,r,q)
                    else (p,q,r)
diff --git a/bench/unique.hs b/bench/unique.hs
new file mode 100644
--- /dev/null
+++ b/bench/unique.hs
@@ -0,0 +1,107 @@
+-- Print unique candidates
+--
+-- Copyright (C) 2023-2024 Rudy Matela
+-- Distributed under the 3-Clause BSD licence (see the file LICENSE).
+--
+-- This can be used to track
+-- if we loose any solutions from implementing pruning techniques.
+import Conjure
+
+-- This script needs some internal utilities of Conjure:
+import Conjure.Engine
+import Conjure.Defn
+import Conjure.Defn.Redundancy
+import Conjure.Defn.Test
+import Conjure.Utils
+import Test.LeanCheck.Tiers (discardT, discardLaterT)
+
+
+-- | This function prints unique 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.
+printUniqueCandidates :: Conjurable f => Int -> String -> f -> [Prim] -> IO ()
+printUniqueCandidates n nm f ps  =  do
+  putStrLn $ "Unique candidates for: " ++ nm ++ " :: " ++ show (typeOf f)
+  putStrLn $ "  pruning with " ++ show nRules ++ "/" ++ show nREs ++ " rules"
+  putStrLn $ "  " ++ show (map length css) ++ " candidates"
+  putStrLn $ "  " ++ show (map length uss) ++ " unique candidates"
+  putStrLn $ "  " ++ show numUnique ++ "/" ++ show numCandidates ++ " unique candidates"
+  putStrLn $ "  " ++ show numRedundant ++ "/" ++ show numCandidates ++ " redundant candidates"
+  putStrLn ""
+  printThy thy
+  putStrLn $ unlines . map showDefn $ unique
+  where
+  numCandidates  =  length candidates
+  numUnique      =  length unique
+  numRedundant   =  numCandidates - numUnique
+  unique         =  concat uss
+  candidates     =  concat css
+  uss            =  discardLaterT (equalModuloTesting maxTests maxEvalRecursions nm f)
+                 $  css
+  css            =  take n
+                 $  discardT isRedundantByIntroduction -- additional pruning rule
+                 $  css'
+  (css', thy)    =  candidateDefnsC args nm f ps  -- Conjure uses this for listing candidates
+  nRules         =  length (rules thy)
+  nREs           =  length (equations thy) + nRules
+  maxTests       =  60 -- a hardcoded value probably will not hurt in this simple benchmark
+  maxEvalRecursions  =  30
+
+  -- 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
+  let n = 5
+
+  printUniqueCandidates (n+2) "foo" (undefined :: Int -> Int)
+    [ pr (0 :: Int)
+    , pr (1 :: Int)
+    , prim "+" ((+) :: Int -> Int -> Int)
+    , prim "*" ((*) :: Int -> Int -> Int)
+    , prim "-" ((-) :: Int -> Int -> Int)
+    ]
+
+  printUniqueCandidates n "?" (undefined :: Int -> Int -> Int)
+    [ pr (0 :: Int)
+    , prim "+" ((+) :: Int -> Int -> Int)
+    , prim "*" ((*) :: Int -> Int -> Int)
+    , prim "dec" (subtract 1 :: Int -> Int)
+    ]
+
+  printUniqueCandidates (n+2) "goo" (undefined :: [Int] -> [Int])
+    [ pr ([] :: [Int])
+    , prim ":" ((:) :: Int -> [Int] -> [Int])
+    , prim "++" ((++) :: [Int] -> [Int] -> [Int])
+    ]
+
+  printUniqueCandidates n "??" (undefined :: [Int] -> [Int] -> [Int])
+    [ pr ([] :: [Int])
+    , prim ":" ((:) :: Int -> [Int] -> [Int])
+    , prim "++" ((++) :: [Int] -> [Int] -> [Int])
+    ]
+
+  printUniqueCandidates (n+2) "ton" (undefined :: Bool -> Bool)
+    [ pr False
+    , pr True
+    , prim "&&" (&&)
+    , prim "||" (||)
+    , prim "not" not
+    ]
+
+  printUniqueCandidates n "&|" (undefined :: Bool -> Bool -> Bool)
+    [ pr False
+    , pr True
+    , prim "&&" (&&)
+    , prim "||" (||)
+    , prim "not" not
+    ]
diff --git a/bench/unique.txt b/bench/unique.txt
new file mode 100644
--- /dev/null
+++ b/bench/unique.txt
@@ -0,0 +1,2276 @@
+Unique candidates for: foo :: Int -> Int
+  pruning with 27/65 rules
+  [3,3,9,10,32,39,185] candidates
+  [3,3,9,10,27,34,95] unique candidates
+  181/281 unique candidates
+  100/281 redundant candidates
+
+rules:
+x - x == 0
+x * 0 == 0
+x * 1 == x
+0 * x == 0
+1 * x == x
+x + 0 == x
+0 + x == x
+x - 0 == x
+(x * y) * z == x * (y * z)
+(x * y) * z == y * (x * z)
+(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 + x) * y == x * (y + y)
+x + (y - x) == y
+(x - y) + y == x
+x * y - x == x * (y - 1)
+x * y - y == y * (x - 1)
+x * (y + 1) == x + x * y
+x * (y + 1) == x * y + x
+(x + 1) * y == y + x * y
+0 - x * y == x * (0 - y)
+0 - x * y == y * (0 - x)
+equations:
+y * x == x * y
+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)
+z + (x + y) == x + (y + z)
+z + (y + x) == x + (y + z)
+(z + y) * x == x * (y + z)
+y + (x - z) == x + (y - z)
+z * y + x == x + y * z
+(x - z) + y == x + (y - z)
+(z - y) + x == (x - y) + z
+y * (x + x) == x * (y + y)
+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 * (1 - y) == x - x * y
+x * (1 - y) == x - y * x
+y * (0 - x) == x * (0 - y)
+(0 - x) * y == x * (0 - y)
+(0 - y) * x == (0 - x) * y
+(1 - y) * x == x - x * y
+(1 - y) * x == 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)
+x * (0 - 1) == 0 - x
+(0 - 1) * x == 0 - x
+(0 - 1) * y == x - (x + y)
+(0 - 1) * y == x - (y + x)
+
+foo x  =  x
+
+foo x  =  0
+
+foo x  =  1
+
+foo 0  =  0
+foo x  =  1
+
+foo 0  =  1
+foo x  =  x
+
+foo 0  =  1
+foo x  =  0
+
+foo x  =  x + x
+
+foo x  =  x + 1
+
+foo x  =  x * x
+
+foo x  =  x - 1
+
+foo x  =  0 - x
+
+foo x  =  1 - x
+
+foo 1  =  0
+foo x  =  x
+
+foo 1  =  0
+foo x  =  1
+
+foo 1  =  1
+foo x  =  0
+
+foo 0  =  0
+foo x  =  x + 1
+
+foo 0  =  0
+foo x  =  x - 1
+
+foo 0  =  0
+foo x  =  1 - x
+
+foo 0  =  1
+foo x  =  x + x
+
+foo 0  =  1
+foo x  =  x * x
+
+foo 0  =  1
+foo x  =  x - 1
+
+foo 0  =  1
+foo x  =  0 - x
+
+foo 0  =  0
+foo 1  =  0
+foo x  =  1
+
+foo 0  =  1
+foo 1  =  0
+foo x  =  x
+
+foo 0  =  1
+foo 1  =  1
+foo x  =  0
+
+foo x  =  x * x - 1
+
+foo x  =  x + (x + x)
+
+foo x  =  x + (x + 1)
+
+foo x  =  x + x * x
+
+foo x  =  x + (x - 1)
+
+foo x  =  1 + (x + 1)
+
+foo x  =  1 + x * x
+
+foo x  =  1 + (1 - x)
+
+foo x  =  x * (x + x)
+
+foo x  =  x * (x * x)
+
+foo x  =  x * (x - 1)
+
+foo x  =  x * (0 - x)
+
+foo x  =  x * (1 - x)
+
+foo x  =  x - (x + 1)
+
+foo x  =  0 - (x + x)
+
+foo x  =  0 - (x + 1)
+
+foo x  =  1 - (x + x)
+
+foo x  =  1 - x * x
+
+foo 1  =  0
+foo x  =  x + x
+
+foo 1  =  0
+foo x  =  x + 1
+
+foo 1  =  0
+foo x  =  x * x
+
+foo 1  =  0
+foo x  =  0 - x
+
+foo 1  =  1
+foo x  =  x + x
+
+foo 1  =  1
+foo x  =  x + 1
+
+foo 1  =  1
+foo x  =  x - 1
+
+foo 1  =  1
+foo x  =  0 - x
+
+foo 1  =  1
+foo x  =  1 - x
+
+foo 0  =  0
+foo x  =  x * x - 1
+
+foo 0  =  0
+foo x  =  x + (x + 1)
+
+foo 0  =  0
+foo x  =  x + (x - 1)
+
+foo 0  =  0
+foo x  =  1 + (x + 1)
+
+foo 0  =  0
+foo x  =  1 + x * x
+
+foo 0  =  0
+foo x  =  1 + (1 - x)
+
+foo 0  =  0
+foo x  =  x - (x + 1)
+
+foo 0  =  0
+foo x  =  0 - (x + 1)
+
+foo 0  =  0
+foo x  =  1 - (x + x)
+
+foo 0  =  0
+foo x  =  1 - x * x
+
+foo 0  =  1
+foo x  =  x * x - 1
+
+foo 0  =  1
+foo x  =  x + (x + x)
+
+foo 0  =  1
+foo x  =  x + x * x
+
+foo 0  =  1
+foo x  =  x + (x - 1)
+
+foo 0  =  1
+foo x  =  1 + (x + 1)
+
+foo 0  =  1
+foo x  =  1 + (1 - x)
+
+foo 0  =  1
+foo x  =  x * (x + x)
+
+foo 0  =  1
+foo x  =  x * (x * x)
+
+foo 0  =  1
+foo x  =  x * (x - 1)
+
+foo 0  =  1
+foo x  =  x * (0 - x)
+
+foo 0  =  1
+foo x  =  x * (1 - x)
+
+foo 0  =  1
+foo x  =  x - (x + 1)
+
+foo 0  =  1
+foo x  =  0 - (x + x)
+
+foo 0  =  1
+foo x  =  0 - (x + 1)
+
+foo 0  =  0
+foo 1  =  0
+foo x  =  x + 1
+
+foo 0  =  0
+foo 1  =  1
+foo x  =  x + 1
+
+foo 0  =  0
+foo 1  =  1
+foo x  =  x - 1
+
+foo 0  =  0
+foo 1  =  1
+foo x  =  1 - x
+
+foo 0  =  1
+foo 1  =  0
+foo x  =  x + x
+
+foo 0  =  1
+foo 1  =  0
+foo x  =  x * x
+
+foo 0  =  1
+foo 1  =  0
+foo x  =  0 - x
+
+foo 0  =  1
+foo 1  =  1
+foo x  =  x + x
+
+foo 0  =  1
+foo 1  =  1
+foo x  =  x - 1
+
+foo 0  =  1
+foo 1  =  1
+foo x  =  0 - x
+
+foo 0  =  0
+foo x  =  x + foo (x - 1)
+
+foo 0  =  0
+foo x  =  foo (x - 1) + 1
+
+foo 0  =  0
+foo x  =  x * foo (x - 1)
+
+foo 0  =  0
+foo x  =  x - foo (x - 1)
+
+foo 0  =  0
+foo x  =  foo (x - 1) - x
+
+foo 0  =  0
+foo x  =  foo (x - 1) - 1
+
+foo 0  =  0
+foo x  =  1 - foo (x - 1)
+
+foo 0  =  1
+foo x  =  x + foo (x - 1)
+
+foo 0  =  1
+foo x  =  foo (x - 1) + 1
+
+foo 0  =  1
+foo x  =  x * foo (x - 1)
+
+foo 0  =  1
+foo x  =  x - foo (x - 1)
+
+foo 0  =  1
+foo x  =  foo (x - 1) - x
+
+foo 0  =  1
+foo x  =  foo (x - 1) - 1
+
+foo 0  =  1
+foo x  =  0 - foo (x - 1)
+
+foo 0  =  1
+foo x  =  1 - foo (x - 1)
+
+foo x  =  x * (x + x) - 1
+
+foo x  =  x * (x * x) - 1
+
+foo x  =  x * (x - 1) - 1
+
+foo x  =  x * (0 - x) - 1
+
+foo x  =  x * (1 - x) - 1
+
+foo x  =  x + (x * x - 1)
+
+foo x  =  x + (x + (x + x))
+
+foo x  =  x + (x + (x + 1))
+
+foo x  =  x + (x + x * x)
+
+foo x  =  x + (x + (x - 1))
+
+foo x  =  x + (1 + (x + 1))
+
+foo x  =  x + (1 + x * x)
+
+foo x  =  x + (1 + (1 - x))
+
+foo x  =  x + x * (x + x)
+
+foo x  =  x + x * (x * x)
+
+foo x  =  x + x * (1 - x)
+
+foo x  =  x + (1 - x * x)
+
+foo x  =  1 + (1 + (x + 1))
+
+foo x  =  1 + (1 + x * x)
+
+foo x  =  1 + (1 + (1 - x))
+
+foo x  =  1 + x * (x + x)
+
+foo x  =  1 + x * (x * x)
+
+foo x  =  1 + x * (x - 1)
+
+foo x  =  1 + (1 - (x + x))
+
+foo x  =  1 + (1 - x * x)
+
+foo x  =  x * (x * x - 1)
+
+foo x  =  x * (x + (x + x))
+
+foo x  =  x * (x + x * x)
+
+foo x  =  x * (x + (x - 1))
+
+foo x  =  x * (x * (x + x))
+
+foo x  =  x * (x * (x * x))
+
+foo x  =  x * (x * (x - 1))
+
+foo x  =  x * (x * (0 - x))
+
+foo x  =  x * (x * (1 - x))
+
+foo x  =  x * (0 - (x + x))
+
+foo x  =  x * (0 - (x + 1))
+
+foo x  =  x * (1 - (x + x))
+
+foo x  =  x * (1 - x * x)
+
+foo x  =  x - (1 + (x + 1))
+
+foo x  =  x - (1 + (1 - x))
+
+foo x  =  0 - (x + (x + x))
+
+foo x  =  0 - (x + (x + 1))
+
+foo x  =  0 - (1 + (x + 1))
+
+foo x  =  0 - (1 + (1 - x))
+
+foo x  =  1 - (x + (x + x))
+
+foo x  =  1 - (x + x * x)
+
+foo x  =  1 - x * (x + x)
+
+foo x  =  1 - x * (x * x)
+
+foo x  =  (x - 1) * (x - 1)
+
+foo x  =  (x - 1) * (1 - x)
+
+foo x  =  x * x - (x + x)
+
+foo 1  =  0
+foo x  =  x + (x + x)
+
+foo 1  =  0
+foo x  =  x + (x + 1)
+
+foo 1  =  0
+foo x  =  x + x * x
+
+foo 1  =  0
+foo x  =  x + (x - 1)
+
+foo 1  =  0
+foo x  =  1 + (x + 1)
+
+foo 1  =  0
+foo x  =  1 + x * x
+
+foo 1  =  0
+foo x  =  1 + (1 - x)
+
+foo 1  =  0
+foo x  =  x * (x + x)
+
+foo 1  =  0
+foo x  =  x * (x * x)
+
+foo 1  =  0
+foo x  =  x * (0 - x)
+
+foo 1  =  0
+foo x  =  x - (x + 1)
+
+foo 1  =  0
+foo x  =  0 - (x + x)
+
+foo 1  =  0
+foo x  =  0 - (x + 1)
+
+foo 1  =  0
+foo x  =  1 - (x + x)
+
+foo 1  =  1
+foo x  =  x * x - 1
+
+foo 1  =  1
+foo x  =  x + (x + x)
+
+foo 1  =  1
+foo x  =  x + (x + 1)
+
+foo 1  =  1
+foo x  =  x + x * x
+
+foo 1  =  1
+foo x  =  1 + (x + 1)
+
+foo 1  =  1
+foo x  =  1 + x * x
+
+foo 1  =  1
+foo x  =  x * (x + x)
+
+foo 1  =  1
+foo x  =  x * (x - 1)
+
+foo 1  =  1
+foo x  =  x * (0 - x)
+
+foo 1  =  1
+foo x  =  x * (1 - x)
+
+foo 1  =  1
+foo x  =  x - (x + 1)
+
+foo 1  =  1
+foo x  =  0 - (x + x)
+
+foo 1  =  1
+foo x  =  0 - (x + 1)
+
+foo 1  =  1
+foo x  =  1 - (x + x)
+
+foo 1  =  1
+foo x  =  1 - x * x
+
+
+Unique candidates for: ? :: Int -> Int -> Int
+  pruning with 13/34 rules
+  [3,8,25,71,205] candidates
+  [3,8,25,70,188] unique candidates
+  294/312 unique candidates
+  18/312 redundant candidates
+
+rules:
+x * 0 == 0
+0 * x == 0
+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)
+(x + y) + z == x + (y + z)
+(x + y) + z == y + (x + z)
+(x + x) * y == x * (y + y)
+equations:
+y * x == x * y
+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 + (x + z) == x + (y + z)
+z + (x + y) == x + (y + z)
+z + (y + x) == x + (y + z)
+(z + y) * x == x * (y + z)
+z * y + x == x + y * z
+y * (x + x) == x * (y + y)
+y + dec (dec x) == x + dec (dec y)
+dec (dec x) + y == x + dec (dec y)
+dec (dec y) + x == dec (dec x) + y
+x + dec (dec 0) == dec (dec x)
+dec (dec 0) + x == dec (dec x)
+
+x ? y  =  x
+
+x ? y  =  y
+
+x ? y  =  0
+
+x ? y  =  dec x
+
+x ? y  =  dec y
+
+x ? 0  =  x
+x ? y  =  y
+
+x ? 0  =  x
+x ? y  =  0
+
+x ? 0  =  0
+x ? y  =  x
+
+0 ? x  =  x
+x ? y  =  x
+
+0 ? x  =  x
+x ? y  =  0
+
+0 ? x  =  0
+x ? y  =  y
+
+x ? y  =  x + x
+
+x ? y  =  x + y
+
+x ? y  =  y + y
+
+x ? y  =  x * x
+
+x ? y  =  x * y
+
+x ? y  =  y * y
+
+x ? y  =  dec (dec x)
+
+x ? y  =  dec (dec y)
+
+x ? 0  =  x
+x ? y  =  dec x
+
+x ? 0  =  x
+x ? y  =  dec y
+
+x ? 0  =  0
+x ? y  =  dec x
+
+x ? 0  =  0
+x ? y  =  dec y
+
+x ? 0  =  dec x
+x ? y  =  x
+
+x ? 0  =  dec x
+x ? y  =  y
+
+x ? 0  =  dec x
+x ? y  =  0
+
+0 ? x  =  x
+x ? y  =  dec x
+
+0 ? x  =  x
+x ? y  =  dec y
+
+0 ? x  =  0
+x ? y  =  dec x
+
+0 ? x  =  0
+x ? y  =  dec y
+
+0 ? x  =  dec x
+x ? y  =  x
+
+0 ? x  =  dec x
+x ? y  =  y
+
+0 ? x  =  dec x
+x ? y  =  0
+
+0 ? x  =  x
+x ? 0  =  x
+x ? y  =  0
+
+0 ? x  =  x
+x ? 0  =  0
+x ? y  =  x
+
+0 ? x  =  0
+x ? 0  =  x
+x ? y  =  y
+
+x ? y  =  dec (x * x)
+
+x ? y  =  dec (x * y)
+
+x ? y  =  dec (y * y)
+
+x ? y  =  dec (dec (dec x))
+
+x ? y  =  dec (dec (dec y))
+
+x ? y  =  x + dec x
+
+x ? y  =  x + dec y
+
+x ? y  =  y + dec y
+
+x ? y  =  x * dec x
+
+x ? y  =  x * dec y
+
+x ? y  =  y * dec x
+
+x ? y  =  y * dec y
+
+x ? 0  =  x
+x ? y  =  x + x
+
+x ? 0  =  x
+x ? y  =  y + y
+
+x ? 0  =  x
+x ? y  =  x * x
+
+x ? 0  =  x
+x ? y  =  x * y
+
+x ? 0  =  x
+x ? y  =  y * y
+
+x ? 0  =  x
+x ? y  =  dec (dec x)
+
+x ? 0  =  x
+x ? y  =  dec (dec y)
+
+x ? 0  =  0
+x ? y  =  x + x
+
+x ? 0  =  0
+x ? y  =  x + y
+
+x ? 0  =  0
+x ? y  =  x * x
+
+x ? 0  =  0
+x ? y  =  dec (dec x)
+
+x ? 0  =  0
+x ? y  =  dec (dec y)
+
+x ? 0  =  dec x
+x ? y  =  dec y
+
+x ? 0  =  x + x
+x ? y  =  x
+
+x ? 0  =  x + x
+x ? y  =  y
+
+x ? 0  =  x + x
+x ? y  =  0
+
+x ? 0  =  x * x
+x ? y  =  x
+
+x ? 0  =  x * x
+x ? y  =  y
+
+x ? 0  =  x * x
+x ? y  =  0
+
+x ? 0  =  dec (dec x)
+x ? y  =  x
+
+x ? 0  =  dec (dec x)
+x ? y  =  y
+
+x ? 0  =  dec (dec x)
+x ? y  =  0
+
+0 ? x  =  x
+x ? y  =  x + x
+
+0 ? x  =  x
+x ? y  =  y + y
+
+0 ? x  =  x
+x ? y  =  x * x
+
+0 ? x  =  x
+x ? y  =  x * y
+
+0 ? x  =  x
+x ? y  =  y * y
+
+0 ? x  =  x
+x ? y  =  dec (dec x)
+
+0 ? x  =  x
+x ? y  =  dec (dec y)
+
+0 ? x  =  0
+x ? y  =  x + y
+
+0 ? x  =  0
+x ? y  =  y + y
+
+0 ? x  =  0
+x ? y  =  y * y
+
+0 ? x  =  0
+x ? y  =  dec (dec x)
+
+0 ? x  =  0
+x ? y  =  dec (dec y)
+
+0 ? x  =  dec x
+x ? y  =  dec x
+
+0 ? x  =  x + x
+x ? y  =  x
+
+0 ? x  =  x + x
+x ? y  =  y
+
+0 ? x  =  x + x
+x ? y  =  0
+
+0 ? x  =  x * x
+x ? y  =  x
+
+0 ? x  =  x * x
+x ? y  =  y
+
+0 ? x  =  x * x
+x ? y  =  0
+
+0 ? x  =  dec (dec x)
+x ? y  =  x
+
+0 ? x  =  dec (dec x)
+x ? y  =  y
+
+0 ? x  =  dec (dec x)
+x ? y  =  0
+
+0 ? x  =  x
+x ? 0  =  x
+x ? y  =  dec x
+
+0 ? x  =  x
+x ? 0  =  x
+x ? y  =  dec y
+
+0 ? x  =  x
+x ? 0  =  0
+x ? y  =  dec x
+
+0 ? x  =  x
+x ? 0  =  0
+x ? y  =  dec y
+
+0 ? x  =  x
+x ? 0  =  dec x
+x ? y  =  x
+
+0 ? x  =  x
+x ? 0  =  dec x
+x ? y  =  0
+
+0 ? x  =  0
+x ? 0  =  x
+x ? y  =  dec x
+
+0 ? x  =  0
+x ? 0  =  x
+x ? y  =  dec y
+
+0 ? x  =  0
+x ? 0  =  0
+x ? y  =  dec x
+
+0 ? x  =  0
+x ? 0  =  0
+x ? y  =  dec y
+
+0 ? x  =  0
+x ? 0  =  dec x
+x ? y  =  y
+
+0 ? x  =  dec x
+x ? 0  =  x
+x ? y  =  y
+
+0 ? x  =  dec x
+x ? 0  =  x
+x ? y  =  0
+
+0 ? x  =  dec x
+x ? 0  =  0
+x ? y  =  x
+
+x ? 0  =  x
+x ? y  =  y ? dec x
+
+x ? 0  =  x
+x ? y  =  y ? dec y
+
+x ? 0  =  x
+x ? y  =  dec x ? x
+
+x ? 0  =  x
+x ? y  =  dec x ? y
+
+x ? 0  =  x
+x ? y  =  dec y ? x
+
+0 ? x  =  x
+x ? y  =  x ? dec y
+
+0 ? x  =  x
+x ? y  =  y ? dec x
+
+0 ? x  =  x
+x ? y  =  y ? dec y
+
+0 ? x  =  x
+x ? y  =  dec x ? x
+
+0 ? x  =  x
+x ? y  =  dec y ? x
+
+x ? y  =  dec (dec (x * x))
+
+x ? y  =  dec (dec (x * y))
+
+x ? y  =  dec (dec (y * y))
+
+x ? y  =  dec (dec (dec (dec x)))
+
+x ? y  =  dec (dec (dec (dec y)))
+
+x ? y  =  dec (x * dec x)
+
+x ? y  =  dec (x * dec y)
+
+x ? y  =  dec (y * dec x)
+
+x ? y  =  dec (y * dec y)
+
+x ? y  =  x + (x + x)
+
+x ? y  =  x + (x + y)
+
+x ? y  =  x + (y + y)
+
+x ? y  =  x + x * x
+
+x ? y  =  x + x * y
+
+x ? y  =  x + y * y
+
+x ? y  =  x + dec (dec x)
+
+x ? y  =  x + dec (dec y)
+
+x ? y  =  y + (y + y)
+
+x ? y  =  y + x * x
+
+x ? y  =  y + x * y
+
+x ? y  =  y + y * y
+
+x ? y  =  y + dec (dec y)
+
+x ? y  =  x * (x + x)
+
+x ? y  =  x * (x + y)
+
+x ? y  =  x * (y + y)
+
+x ? y  =  x * (x * x)
+
+x ? y  =  x * (x * y)
+
+x ? y  =  x * (y * y)
+
+x ? y  =  x * dec (dec x)
+
+x ? y  =  x * dec (dec y)
+
+x ? y  =  y * (x + y)
+
+x ? y  =  y * (y + y)
+
+x ? y  =  y * (y * y)
+
+x ? y  =  y * dec (dec x)
+
+x ? y  =  y * dec (dec y)
+
+x ? y  =  dec x * dec x
+
+x ? y  =  dec x * dec y
+
+x ? y  =  dec y * dec y
+
+x ? 0  =  x
+x ? y  =  dec (x * x)
+
+x ? 0  =  x
+x ? y  =  dec (x * y)
+
+x ? 0  =  x
+x ? y  =  dec (y * y)
+
+x ? 0  =  x
+x ? y  =  dec (dec (dec x))
+
+x ? 0  =  x
+x ? y  =  dec (dec (dec y))
+
+x ? 0  =  x
+x ? y  =  x + dec x
+
+x ? 0  =  x
+x ? y  =  x + dec y
+
+x ? 0  =  x
+x ? y  =  y + dec y
+
+x ? 0  =  x
+x ? y  =  x * dec x
+
+x ? 0  =  x
+x ? y  =  x * dec y
+
+x ? 0  =  x
+x ? y  =  y * dec x
+
+x ? 0  =  x
+x ? y  =  y * dec y
+
+x ? 0  =  0
+x ? y  =  dec (x * x)
+
+x ? 0  =  0
+x ? y  =  dec (x * y)
+
+x ? 0  =  0
+x ? y  =  dec (y * y)
+
+x ? 0  =  0
+x ? y  =  dec (dec (dec x))
+
+x ? 0  =  0
+x ? y  =  dec (dec (dec y))
+
+x ? 0  =  0
+x ? y  =  x + dec x
+
+x ? 0  =  0
+x ? y  =  x + dec y
+
+x ? 0  =  0
+x ? y  =  y + dec y
+
+x ? 0  =  0
+x ? y  =  x * dec x
+
+x ? 0  =  0
+x ? y  =  x * dec y
+
+x ? 0  =  dec x
+x ? y  =  x + x
+
+x ? 0  =  dec x
+x ? y  =  x + y
+
+x ? 0  =  dec x
+x ? y  =  y + y
+
+x ? 0  =  dec x
+x ? y  =  x * x
+
+x ? 0  =  dec x
+x ? y  =  x * y
+
+x ? 0  =  dec x
+x ? y  =  y * y
+
+x ? 0  =  dec x
+x ? y  =  dec (dec x)
+
+x ? 0  =  dec x
+x ? y  =  dec (dec y)
+
+x ? 0  =  x + x
+x ? y  =  dec x
+
+x ? 0  =  x + x
+x ? y  =  dec y
+
+x ? 0  =  x * x
+x ? y  =  dec x
+
+x ? 0  =  x * x
+x ? y  =  dec y
+
+x ? 0  =  dec (dec x)
+x ? y  =  dec x
+
+x ? 0  =  dec (dec x)
+x ? y  =  dec y
+
+x ? 0  =  dec (x * x)
+x ? y  =  x
+
+x ? 0  =  dec (x * x)
+x ? y  =  y
+
+x ? 0  =  dec (x * x)
+x ? y  =  0
+
+x ? 0  =  dec (dec (dec x))
+x ? y  =  x
+
+x ? 0  =  dec (dec (dec x))
+x ? y  =  y
+
+x ? 0  =  dec (dec (dec x))
+x ? y  =  0
+
+x ? 0  =  x + dec x
+x ? y  =  x
+
+x ? 0  =  x + dec x
+x ? y  =  y
+
+x ? 0  =  x + dec x
+x ? y  =  0
+
+x ? 0  =  x * dec x
+x ? y  =  x
+
+x ? 0  =  x * dec x
+x ? y  =  y
+
+x ? 0  =  x * dec x
+x ? y  =  0
+
+0 ? x  =  x
+x ? y  =  dec (x * x)
+
+0 ? x  =  x
+x ? y  =  dec (x * y)
+
+0 ? x  =  x
+x ? y  =  dec (y * y)
+
+0 ? x  =  x
+x ? y  =  dec (dec (dec x))
+
+0 ? x  =  x
+x ? y  =  dec (dec (dec y))
+
+0 ? x  =  x
+x ? y  =  x + dec x
+
+0 ? x  =  x
+x ? y  =  x + dec y
+
+0 ? x  =  x
+x ? y  =  y + dec y
+
+0 ? x  =  x
+x ? y  =  x * dec x
+
+0 ? x  =  x
+x ? y  =  x * dec y
+
+0 ? x  =  x
+x ? y  =  y * dec x
+
+0 ? x  =  x
+x ? y  =  y * dec y
+
+0 ? x  =  0
+x ? y  =  dec (x * x)
+
+0 ? x  =  0
+x ? y  =  dec (x * y)
+
+0 ? x  =  0
+x ? y  =  dec (y * y)
+
+0 ? x  =  0
+x ? y  =  dec (dec (dec x))
+
+0 ? x  =  0
+x ? y  =  dec (dec (dec y))
+
+0 ? x  =  0
+x ? y  =  x + dec x
+
+0 ? x  =  0
+x ? y  =  x + dec y
+
+0 ? x  =  0
+x ? y  =  y + dec y
+
+0 ? x  =  0
+x ? y  =  y * dec x
+
+0 ? x  =  0
+x ? y  =  y * dec y
+
+0 ? x  =  dec x
+x ? y  =  x + x
+
+0 ? x  =  dec x
+x ? y  =  x + y
+
+0 ? x  =  dec x
+x ? y  =  y + y
+
+0 ? x  =  dec x
+x ? y  =  x * x
+
+0 ? x  =  dec x
+x ? y  =  x * y
+
+0 ? x  =  dec x
+x ? y  =  y * y
+
+0 ? x  =  dec x
+x ? y  =  dec (dec x)
+
+0 ? x  =  dec x
+x ? y  =  dec (dec y)
+
+0 ? x  =  x + x
+x ? y  =  dec x
+
+0 ? x  =  x + x
+x ? y  =  dec y
+
+0 ? x  =  x * x
+x ? y  =  dec x
+
+0 ? x  =  x * x
+x ? y  =  dec y
+
+0 ? x  =  dec (dec x)
+x ? y  =  dec x
+
+0 ? x  =  dec (dec x)
+x ? y  =  dec y
+
+0 ? x  =  dec (x * x)
+x ? y  =  x
+
+0 ? x  =  dec (x * x)
+x ? y  =  y
+
+0 ? x  =  dec (x * x)
+x ? y  =  0
+
+0 ? x  =  dec (dec (dec x))
+x ? y  =  x
+
+0 ? x  =  dec (dec (dec x))
+x ? y  =  y
+
+0 ? x  =  dec (dec (dec x))
+x ? y  =  0
+
+0 ? x  =  x + dec x
+x ? y  =  x
+
+0 ? x  =  x + dec x
+x ? y  =  y
+
+0 ? x  =  x + dec x
+x ? y  =  0
+
+0 ? x  =  x * dec x
+x ? y  =  x
+
+0 ? x  =  x * dec x
+x ? y  =  y
+
+0 ? x  =  x * dec x
+x ? y  =  0
+
+0 ? x  =  x
+x ? 0  =  x
+x ? y  =  x + x
+
+0 ? x  =  x
+x ? 0  =  x
+x ? y  =  y + y
+
+0 ? x  =  x
+x ? 0  =  x
+x ? y  =  x * x
+
+0 ? x  =  x
+x ? 0  =  x
+x ? y  =  x * y
+
+0 ? x  =  x
+x ? 0  =  x
+x ? y  =  y * y
+
+0 ? x  =  x
+x ? 0  =  x
+x ? y  =  dec (dec x)
+
+0 ? x  =  x
+x ? 0  =  x
+x ? y  =  dec (dec y)
+
+0 ? x  =  x
+x ? 0  =  0
+x ? y  =  x + x
+
+0 ? x  =  x
+x ? 0  =  0
+x ? y  =  x * x
+
+0 ? x  =  x
+x ? 0  =  0
+x ? y  =  dec (dec x)
+
+0 ? x  =  x
+x ? 0  =  0
+x ? y  =  dec (dec y)
+
+0 ? x  =  x
+x ? 0  =  dec x
+x ? y  =  dec y
+
+0 ? x  =  x
+x ? 0  =  x + x
+x ? y  =  x
+
+0 ? x  =  x
+x ? 0  =  x + x
+x ? y  =  0
+
+0 ? x  =  x
+x ? 0  =  x * x
+x ? y  =  x
+
+0 ? x  =  x
+x ? 0  =  x * x
+x ? y  =  0
+
+0 ? x  =  x
+x ? 0  =  dec (dec x)
+x ? y  =  x
+
+0 ? x  =  x
+x ? 0  =  dec (dec x)
+x ? y  =  0
+
+0 ? x  =  0
+x ? 0  =  x
+x ? y  =  y + y
+
+0 ? x  =  0
+x ? 0  =  x
+x ? y  =  y * y
+
+0 ? x  =  0
+x ? 0  =  x
+x ? y  =  dec (dec x)
+
+0 ? x  =  0
+x ? 0  =  x
+x ? y  =  dec (dec y)
+
+0 ? x  =  0
+x ? 0  =  0
+x ? y  =  x + y
+
+0 ? x  =  0
+x ? 0  =  0
+x ? y  =  dec (dec x)
+
+0 ? x  =  0
+x ? 0  =  0
+x ? y  =  dec (dec y)
+
+0 ? x  =  0
+x ? 0  =  dec x
+x ? y  =  dec y
+
+0 ? x  =  0
+x ? 0  =  x + x
+x ? y  =  y
+
+0 ? x  =  0
+x ? 0  =  x * x
+x ? y  =  y
+
+0 ? x  =  0
+x ? 0  =  dec (dec x)
+x ? y  =  y
+
+0 ? x  =  dec x
+x ? 0  =  x
+x ? y  =  dec x
+
+0 ? x  =  dec x
+x ? 0  =  0
+x ? y  =  dec x
+
+0 ? x  =  dec x
+x ? 0  =  dec x
+x ? y  =  x
+
+0 ? x  =  dec x
+x ? 0  =  dec x
+x ? y  =  y
+
+0 ? x  =  dec x
+x ? 0  =  dec x
+x ? y  =  0
+
+0 ? x  =  x + x
+x ? 0  =  x
+x ? y  =  y
+
+0 ? x  =  x + x
+x ? 0  =  x
+x ? y  =  0
+
+0 ? x  =  x + x
+x ? 0  =  0
+x ? y  =  x
+
+0 ? x  =  x * x
+x ? 0  =  x
+x ? y  =  y
+
+0 ? x  =  x * x
+x ? 0  =  x
+x ? y  =  0
+
+0 ? x  =  x * x
+x ? 0  =  0
+x ? y  =  x
+
+0 ? x  =  dec (dec x)
+x ? 0  =  x
+x ? y  =  y
+
+0 ? x  =  dec (dec x)
+x ? 0  =  x
+x ? y  =  0
+
+0 ? x  =  dec (dec x)
+x ? 0  =  0
+x ? y  =  x
+
+0 ? 0  =  0
+0 ? x  =  dec x
+x ? y  =  dec x
+
+
+Unique candidates for: goo :: [Int] -> [Int]
+  pruning with 4/4 rules
+  [2,1,1,2,4,7,10] candidates
+  [2,1,1,2,3,6,10] unique candidates
+  25/27 unique candidates
+  2/27 redundant candidates
+
+rules:
+xs ++ [] == xs
+[] ++ xs == xs
+(xs ++ ys) ++ zs == xs ++ (ys ++ zs)
+(x:xs) ++ ys == x:(xs ++ ys)
+
+goo xs  =  xs
+
+goo xs  =  []
+
+goo []  =  []
+goo (x:xs)  =  xs
+
+goo xs  =  xs ++ xs
+
+goo []  =  []
+goo (x:xs)  =  [x]
+
+goo []  =  []
+goo (x:xs)  =  xs ++ xs
+
+goo []  =  []
+goo (x:xs)  =  xs ++ goo xs
+
+goo []  =  []
+goo (x:xs)  =  goo xs ++ xs
+
+goo xs  =  xs ++ (xs ++ xs)
+
+goo []  =  []
+goo (x:xs)  =  x:x:xs
+
+goo []  =  []
+goo (x:xs)  =  [x,x]
+
+goo []  =  []
+goo (x:xs)  =  x:(xs ++ xs)
+
+goo []  =  []
+goo (x:xs)  =  xs ++ (x:xs)
+
+goo []  =  []
+goo (x:xs)  =  xs ++ [x]
+
+goo []  =  []
+goo (x:xs)  =  xs ++ (xs ++ xs)
+
+goo []  =  []
+goo (x:xs)  =  x:x:goo xs
+
+goo []  =  []
+goo (x:xs)  =  x:(xs ++ goo xs)
+
+goo []  =  []
+goo (x:xs)  =  x:(goo xs ++ xs)
+
+goo []  =  []
+goo (x:xs)  =  xs ++ (x:goo xs)
+
+goo []  =  []
+goo (x:xs)  =  xs ++ (xs ++ goo xs)
+
+goo []  =  []
+goo (x:xs)  =  xs ++ (goo xs ++ xs)
+
+goo []  =  []
+goo (x:xs)  =  goo xs ++ (x:xs)
+
+goo []  =  []
+goo (x:xs)  =  goo xs ++ [x]
+
+goo []  =  []
+goo (x:xs)  =  goo xs ++ (xs ++ xs)
+
+goo xs  =  xs ++ (xs ++ (xs ++ xs))
+
+
+Unique candidates for: ?? :: [Int] -> [Int] -> [Int]
+  pruning with 4/4 rules
+  [3,8,15,43,122] candidates
+  [3,8,15,35,89] unique candidates
+  150/191 unique candidates
+  41/191 redundant candidates
+
+rules:
+xs ++ [] == xs
+[] ++ xs == xs
+(xs ++ ys) ++ zs == xs ++ (ys ++ zs)
+(x:xs) ++ ys == x:(xs ++ ys)
+
+xs ?? ys  =  xs
+
+xs ?? ys  =  ys
+
+xs ?? ys  =  []
+
+xs ?? []  =  xs
+xs ?? (x:ys)  =  ys
+
+xs ?? []  =  xs
+xs ?? (x:ys)  =  []
+
+xs ?? []  =  []
+xs ?? (x:ys)  =  xs
+
+xs ?? []  =  []
+xs ?? (x:ys)  =  ys
+
+[] ?? xs  =  xs
+(x:xs) ?? ys  =  xs
+
+[] ?? xs  =  xs
+(x:xs) ?? ys  =  []
+
+[] ?? xs  =  []
+(x:xs) ?? ys  =  xs
+
+[] ?? xs  =  []
+(x:xs) ?? ys  =  ys
+
+xs ?? ys  =  xs ++ xs
+
+xs ?? ys  =  xs ++ ys
+
+xs ?? ys  =  ys ++ xs
+
+xs ?? ys  =  ys ++ ys
+
+[] ?? xs  =  xs
+(x:xs) ?? []  =  xs
+(x:xs) ?? (y:ys)  =  ys
+
+[] ?? xs  =  xs
+(x:xs) ?? []  =  xs
+(x:xs) ?? (y:ys)  =  []
+
+[] ?? xs  =  xs
+(x:xs) ?? []  =  []
+(x:xs) ?? (y:ys)  =  xs
+
+[] ?? xs  =  xs
+(x:xs) ?? []  =  []
+(x:xs) ?? (y:ys)  =  ys
+
+[] ?? xs  =  []
+(x:xs) ?? []  =  xs
+(x:xs) ?? (y:ys)  =  ys
+
+[] ?? xs  =  []
+(x:xs) ?? []  =  xs
+(x:xs) ?? (y:ys)  =  []
+
+[] ?? xs  =  []
+(x:xs) ?? []  =  []
+(x:xs) ?? (y:ys)  =  xs
+
+[] ?? xs  =  []
+(x:xs) ?? []  =  []
+(x:xs) ?? (y:ys)  =  ys
+
+[] ?? []  =  []
+[] ?? (x:xs)  =  xs
+(x:xs) ?? ys  =  xs
+
+[] ?? []  =  []
+[] ?? (x:xs)  =  xs
+(x:xs) ?? ys  =  ys
+
+[] ?? []  =  []
+[] ?? (x:xs)  =  xs
+(x:xs) ?? ys  =  []
+
+xs ?? []  =  xs
+xs ?? (x:ys)  =  ys ?? xs
+
+[] ?? xs  =  xs
+(x:xs) ?? ys  =  ys ?? xs
+
+xs ?? []  =  xs
+xs ?? (x:ys)  =  x:xs
+
+xs ?? []  =  xs
+xs ?? (x:ys)  =  x:ys
+
+xs ?? []  =  xs
+xs ?? (x:ys)  =  [x]
+
+xs ?? []  =  xs
+xs ?? (x:ys)  =  xs ++ xs
+
+xs ?? []  =  xs
+xs ?? (x:ys)  =  xs ++ ys
+
+xs ?? []  =  xs
+xs ?? (x:ys)  =  ys ++ xs
+
+xs ?? []  =  xs
+xs ?? (x:ys)  =  ys ++ ys
+
+xs ?? []  =  []
+xs ?? (x:ys)  =  x:xs
+
+xs ?? []  =  []
+xs ?? (x:ys)  =  [x]
+
+xs ?? []  =  []
+xs ?? (x:ys)  =  xs ++ xs
+
+xs ?? []  =  []
+xs ?? (x:ys)  =  xs ++ ys
+
+xs ?? []  =  []
+xs ?? (x:ys)  =  ys ++ xs
+
+xs ?? []  =  []
+xs ?? (x:ys)  =  ys ++ ys
+
+xs ?? []  =  xs ++ xs
+xs ?? (x:ys)  =  xs
+
+xs ?? []  =  xs ++ xs
+xs ?? (x:ys)  =  ys
+
+xs ?? []  =  xs ++ xs
+xs ?? (x:ys)  =  []
+
+[] ?? xs  =  xs
+(x:xs) ?? ys  =  x:xs
+
+[] ?? xs  =  xs
+(x:xs) ?? ys  =  x:ys
+
+[] ?? xs  =  xs
+(x:xs) ?? ys  =  [x]
+
+[] ?? xs  =  xs
+(x:xs) ?? ys  =  xs ++ xs
+
+[] ?? xs  =  xs
+(x:xs) ?? ys  =  xs ++ ys
+
+[] ?? xs  =  xs
+(x:xs) ?? ys  =  ys ++ xs
+
+[] ?? xs  =  xs
+(x:xs) ?? ys  =  ys ++ ys
+
+[] ?? xs  =  []
+(x:xs) ?? ys  =  x:ys
+
+[] ?? xs  =  []
+(x:xs) ?? ys  =  [x]
+
+[] ?? xs  =  []
+(x:xs) ?? ys  =  xs ++ xs
+
+[] ?? xs  =  []
+(x:xs) ?? ys  =  xs ++ ys
+
+[] ?? xs  =  []
+(x:xs) ?? ys  =  ys ++ xs
+
+[] ?? xs  =  []
+(x:xs) ?? ys  =  ys ++ ys
+
+[] ?? xs  =  xs ++ xs
+(x:xs) ?? ys  =  xs
+
+[] ?? xs  =  xs ++ xs
+(x:xs) ?? ys  =  ys
+
+[] ?? xs  =  xs ++ xs
+(x:xs) ?? ys  =  []
+
+[] ?? []  =  []
+[] ?? (x:xs)  =  xs
+(x:xs) ?? []  =  xs
+(x:xs) ?? (y:ys)  =  []
+
+[] ?? xs  =  xs
+(x:xs) ?? []  =  xs
+(x:xs) ?? (y:ys)  =  xs ?? []
+
+[] ?? xs  =  xs
+(x:xs) ?? []  =  xs
+(x:xs) ?? (y:ys)  =  ys ?? xs
+
+[] ?? xs  =  xs
+(x:xs) ?? []  =  xs
+(x:xs) ?? (y:ys)  =  ys ?? []
+
+[] ?? xs  =  xs
+(x:xs) ?? []  =  xs ?? xs
+(x:xs) ?? (y:ys)  =  xs
+
+[] ?? xs  =  xs
+(x:xs) ?? []  =  xs ?? xs
+(x:xs) ?? (y:ys)  =  ys
+
+[] ?? xs  =  xs
+(x:xs) ?? []  =  []
+(x:xs) ?? (y:ys)  =  xs ?? ys
+
+[] ?? xs  =  xs
+(x:xs) ?? []  =  []
+(x:xs) ?? (y:ys)  =  ys ?? xs
+
+[] ?? xs  =  []
+(x:xs) ?? []  =  xs
+(x:xs) ?? (y:ys)  =  xs ?? ys
+
+[] ?? xs  =  []
+(x:xs) ?? []  =  xs
+(x:xs) ?? (y:ys)  =  ys ?? xs
+
+[] ?? xs  =  []
+(x:xs) ?? []  =  xs ?? xs
+(x:xs) ?? (y:ys)  =  xs
+
+[] ?? xs  =  []
+(x:xs) ?? []  =  xs ?? xs
+(x:xs) ?? (y:ys)  =  ys
+
+[] ?? []  =  []
+[] ?? (x:xs)  =  xs
+(x:xs) ?? ys  =  ys ?? xs
+
+[] ?? []  =  []
+[] ?? (x:xs)  =  xs
+(x:xs) ?? ys  =  [] ?? xs
+
+[] ?? []  =  []
+[] ?? (x:xs)  =  xs ?? xs
+(x:xs) ?? ys  =  xs
+
+xs ?? ys  =  xs ++ (xs ++ xs)
+
+xs ?? ys  =  xs ++ (xs ++ ys)
+
+xs ?? ys  =  xs ++ (ys ++ xs)
+
+xs ?? ys  =  xs ++ (ys ++ ys)
+
+xs ?? ys  =  ys ++ (xs ++ xs)
+
+xs ?? ys  =  ys ++ (xs ++ ys)
+
+xs ?? ys  =  ys ++ (ys ++ xs)
+
+xs ?? ys  =  ys ++ (ys ++ ys)
+
+[] ?? xs  =  xs
+(x:xs) ?? []  =  xs
+(x:xs) ?? (y:ys)  =  x:xs
+
+[] ?? xs  =  xs
+(x:xs) ?? []  =  xs
+(x:xs) ?? (y:ys)  =  x:ys
+
+[] ?? xs  =  xs
+(x:xs) ?? []  =  xs
+(x:xs) ?? (y:ys)  =  [x]
+
+[] ?? xs  =  xs
+(x:xs) ?? []  =  xs
+(x:xs) ?? (y:ys)  =  y:xs
+
+[] ?? xs  =  xs
+(x:xs) ?? []  =  xs
+(x:xs) ?? (y:ys)  =  y:ys
+
+[] ?? xs  =  xs
+(x:xs) ?? []  =  xs
+(x:xs) ?? (y:ys)  =  [y]
+
+[] ?? xs  =  xs
+(x:xs) ?? []  =  xs
+(x:xs) ?? (y:ys)  =  xs ++ xs
+
+[] ?? xs  =  xs
+(x:xs) ?? []  =  xs
+(x:xs) ?? (y:ys)  =  xs ++ ys
+
+[] ?? xs  =  xs
+(x:xs) ?? []  =  xs
+(x:xs) ?? (y:ys)  =  ys ++ ys
+
+[] ?? xs  =  xs
+(x:xs) ?? []  =  []
+(x:xs) ?? (y:ys)  =  x:xs
+
+[] ?? xs  =  xs
+(x:xs) ?? []  =  []
+(x:xs) ?? (y:ys)  =  x:ys
+
+[] ?? xs  =  xs
+(x:xs) ?? []  =  []
+(x:xs) ?? (y:ys)  =  [x]
+
+[] ?? xs  =  xs
+(x:xs) ?? []  =  []
+(x:xs) ?? (y:ys)  =  y:xs
+
+[] ?? xs  =  xs
+(x:xs) ?? []  =  []
+(x:xs) ?? (y:ys)  =  [y]
+
+[] ?? xs  =  xs
+(x:xs) ?? []  =  []
+(x:xs) ?? (y:ys)  =  xs ++ xs
+
+[] ?? xs  =  xs
+(x:xs) ?? []  =  []
+(x:xs) ?? (y:ys)  =  xs ++ ys
+
+[] ?? xs  =  xs
+(x:xs) ?? []  =  []
+(x:xs) ?? (y:ys)  =  ys ++ ys
+
+[] ?? xs  =  xs
+(x:xs) ?? []  =  x:xs
+(x:xs) ?? (y:ys)  =  xs
+
+[] ?? xs  =  xs
+(x:xs) ?? []  =  x:xs
+(x:xs) ?? (y:ys)  =  ys
+
+[] ?? xs  =  xs
+(x:xs) ?? []  =  x:xs
+(x:xs) ?? (y:ys)  =  []
+
+[] ?? xs  =  xs
+(x:xs) ?? []  =  [x]
+(x:xs) ?? (y:ys)  =  xs
+
+[] ?? xs  =  xs
+(x:xs) ?? []  =  [x]
+(x:xs) ?? (y:ys)  =  ys
+
+[] ?? xs  =  xs
+(x:xs) ?? []  =  [x]
+(x:xs) ?? (y:ys)  =  []
+
+[] ?? xs  =  xs
+(x:xs) ?? []  =  xs ++ xs
+(x:xs) ?? (y:ys)  =  xs
+
+[] ?? xs  =  xs
+(x:xs) ?? []  =  xs ++ xs
+(x:xs) ?? (y:ys)  =  ys
+
+[] ?? xs  =  xs
+(x:xs) ?? []  =  xs ++ xs
+(x:xs) ?? (y:ys)  =  []
+
+[] ?? xs  =  []
+(x:xs) ?? []  =  xs
+(x:xs) ?? (y:ys)  =  x:xs
+
+[] ?? xs  =  []
+(x:xs) ?? []  =  xs
+(x:xs) ?? (y:ys)  =  x:ys
+
+[] ?? xs  =  []
+(x:xs) ?? []  =  xs
+(x:xs) ?? (y:ys)  =  [x]
+
+[] ?? xs  =  []
+(x:xs) ?? []  =  xs
+(x:xs) ?? (y:ys)  =  y:xs
+
+[] ?? xs  =  []
+(x:xs) ?? []  =  xs
+(x:xs) ?? (y:ys)  =  y:ys
+
+[] ?? xs  =  []
+(x:xs) ?? []  =  xs
+(x:xs) ?? (y:ys)  =  [y]
+
+[] ?? xs  =  []
+(x:xs) ?? []  =  xs
+(x:xs) ?? (y:ys)  =  xs ++ xs
+
+[] ?? xs  =  []
+(x:xs) ?? []  =  xs
+(x:xs) ?? (y:ys)  =  xs ++ ys
+
+[] ?? xs  =  []
+(x:xs) ?? []  =  xs
+(x:xs) ?? (y:ys)  =  ys ++ ys
+
+[] ?? xs  =  []
+(x:xs) ?? []  =  []
+(x:xs) ?? (y:ys)  =  x:ys
+
+[] ?? xs  =  []
+(x:xs) ?? []  =  []
+(x:xs) ?? (y:ys)  =  [x]
+
+[] ?? xs  =  []
+(x:xs) ?? []  =  []
+(x:xs) ?? (y:ys)  =  y:xs
+
+[] ?? xs  =  []
+(x:xs) ?? []  =  []
+(x:xs) ?? (y:ys)  =  [y]
+
+[] ?? xs  =  []
+(x:xs) ?? []  =  []
+(x:xs) ?? (y:ys)  =  xs ++ xs
+
+[] ?? xs  =  []
+(x:xs) ?? []  =  []
+(x:xs) ?? (y:ys)  =  xs ++ ys
+
+[] ?? xs  =  []
+(x:xs) ?? []  =  []
+(x:xs) ?? (y:ys)  =  ys ++ ys
+
+[] ?? xs  =  []
+(x:xs) ?? []  =  x:xs
+(x:xs) ?? (y:ys)  =  xs
+
+[] ?? xs  =  []
+(x:xs) ?? []  =  x:xs
+(x:xs) ?? (y:ys)  =  ys
+
+[] ?? xs  =  []
+(x:xs) ?? []  =  [x]
+(x:xs) ?? (y:ys)  =  xs
+
+[] ?? xs  =  []
+(x:xs) ?? []  =  [x]
+(x:xs) ?? (y:ys)  =  ys
+
+[] ?? xs  =  []
+(x:xs) ?? []  =  [x]
+(x:xs) ?? (y:ys)  =  []
+
+[] ?? xs  =  []
+(x:xs) ?? []  =  xs ++ xs
+(x:xs) ?? (y:ys)  =  xs
+
+[] ?? xs  =  []
+(x:xs) ?? []  =  xs ++ xs
+(x:xs) ?? (y:ys)  =  ys
+
+[] ?? xs  =  []
+(x:xs) ?? []  =  xs ++ xs
+(x:xs) ?? (y:ys)  =  []
+
+[] ?? xs  =  xs ++ xs
+(x:xs) ?? []  =  xs
+(x:xs) ?? (y:ys)  =  ys
+
+[] ?? xs  =  xs ++ xs
+(x:xs) ?? []  =  xs
+(x:xs) ?? (y:ys)  =  []
+
+[] ?? xs  =  xs ++ xs
+(x:xs) ?? []  =  []
+(x:xs) ?? (y:ys)  =  xs
+
+[] ?? xs  =  xs ++ xs
+(x:xs) ?? []  =  []
+(x:xs) ?? (y:ys)  =  ys
+
+[] ?? []  =  []
+[] ?? (x:xs)  =  xs
+(x:xs) ?? ys  =  x:xs
+
+[] ?? []  =  []
+[] ?? (x:xs)  =  xs
+(x:xs) ?? ys  =  x:ys
+
+[] ?? []  =  []
+[] ?? (x:xs)  =  xs
+(x:xs) ?? ys  =  [x]
+
+[] ?? []  =  []
+[] ?? (x:xs)  =  xs
+(x:xs) ?? ys  =  xs ++ xs
+
+[] ?? []  =  []
+[] ?? (x:xs)  =  xs
+(x:xs) ?? ys  =  xs ++ ys
+
+[] ?? []  =  []
+[] ?? (x:xs)  =  xs
+(x:xs) ?? ys  =  ys ++ xs
+
+[] ?? []  =  []
+[] ?? (x:xs)  =  xs
+(x:xs) ?? ys  =  ys ++ ys
+
+[] ?? []  =  []
+[] ?? (x:xs)  =  [x]
+(x:xs) ?? ys  =  xs
+
+[] ?? []  =  []
+[] ?? (x:xs)  =  [x]
+(x:xs) ?? ys  =  ys
+
+[] ?? []  =  []
+[] ?? (x:xs)  =  [x]
+(x:xs) ?? ys  =  []
+
+[] ?? []  =  []
+[] ?? (x:xs)  =  xs ++ xs
+(x:xs) ?? ys  =  xs
+
+[] ?? []  =  []
+[] ?? (x:xs)  =  xs ++ xs
+(x:xs) ?? ys  =  ys
+
+[] ?? []  =  []
+[] ?? (x:xs)  =  xs ++ xs
+(x:xs) ?? ys  =  []
+
+
+Unique candidates for: ton :: Bool -> Bool
+  pruning with 39/49 rules
+  [3,2,0,0,0,0,0] candidates
+  [3,1,0,0,0,0,0] unique candidates
+  4/5 unique candidates
+  1/5 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
+
+ton p  =  p
+
+ton p  =  False
+
+ton p  =  True
+
+ton p  =  not p
+
+
+Unique candidates for: &| :: Bool -> Bool -> Bool
+  pruning with 39/49 rules
+  [4,12,20,6,2] candidates
+  [4,8,4,0,0] unique candidates
+  16/44 unique candidates
+  28/44 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
+
+p &| q  =  p
+
+p &| q  =  q
+
+p &| q  =  False
+
+p &| q  =  True
+
+p &| q  =  not p
+
+p &| q  =  not q
+
+p &| False  =  p
+p &| True  =  False
+
+p &| False  =  p
+p &| True  =  True
+
+p &| False  =  False
+p &| True  =  p
+
+p &| False  =  True
+p &| True  =  p
+
+False &| p  =  p
+True &| p  =  False
+
+False &| p  =  True
+True &| p  =  p
+
+p &| False  =  p
+p &| True  =  not p
+
+p &| False  =  True
+p &| True  =  not p
+
+p &| False  =  not p
+p &| True  =  p
+
+p &| False  =  not p
+p &| True  =  False
+
+
diff --git a/bench/weird.txt b/bench/weird.txt
--- a/bench/weird.txt
+++ b/bench/weird.txt
@@ -18,11 +18,11 @@
 -- looking through 0 candidates of size 4
 -- looking through 39 candidates of size 5
 -- looking through 60 candidates of size 6
--- looking through 225 candidates of size 7
--- looking through 1056 candidates of size 8
--- looking through 1488 candidates of size 9
--- looking through 13020 candidates of size 10
--- tested 7148 candidates
+-- looking through 222 candidates of size 7
+-- looking through 996 candidates of size 8
+-- looking through 1266 candidates of size 9
+-- looking through 11700 candidates of size 10
+-- tested 6683 candidates
 x ^^^ y  =  if 0 == x * y
             then x + y
             else 0
diff --git a/changelog.md b/changelog.md
--- a/changelog.md
+++ b/changelog.md
@@ -2,6 +2,15 @@
 ============================
 
 
+v0.5.14 (February 2024)
+-----------------------
+
+* improve commutative pruning, slightly faster Conjure
+* add `carryOn`, `rewriting`, `requireDescent`, `adHocRedundancy` switches
+  to the `Args` record
+* add more benchmarks and tests
+
+
 v0.5.12 (February 2024)
 -----------------------
 
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-2024 Rudy Matela
 -- Distributed under the 3-Clause BSD licence (see the file LICENSE).
 name:                code-conjure
-version:             0.5.12
+version:             0.5.14
 synopsis:            synthesize Haskell functions out of partial definitions
 description:
   Conjure is a tool that synthesizes Haskell functions out of partial definitions.
@@ -67,7 +67,7 @@
 source-repository this
   type:            git
   location:        https://github.com/rudymatela/conjure
-  tag:             v0.5.12
+  tag:             v0.5.14
 
 library
   exposed-modules: Conjure
diff --git a/eg/bst.txt b/eg/bst.txt
--- a/eg/bst.txt
+++ b/eg/bst.txt
@@ -12,7 +12,7 @@
 -- looking through 92 candidates of size 9
 -- looking through 0 candidates of size 10
 -- looking through 304 candidates of size 11
--- looking through 199 candidates of size 12
+-- looking through 151 candidates of size 12
 -- tested 497 candidates
 mem x Leaf  =  False
 mem x (Node t1 y t2)  =  mem x t1 || (mem x t2 || x == y)
diff --git a/eg/factorial.txt b/eg/factorial.txt
--- a/eg/factorial.txt
+++ b/eg/factorial.txt
@@ -7,7 +7,7 @@
 -- looking through 8 candidates of size 4
 -- looking through 28 candidates of size 5
 -- looking through 35 candidates of size 6
--- looking through 179 candidates of size 7
+-- looking through 167 candidates of size 7
 -- tested 95 candidates
 factorial 0  =  1
 factorial x  =  x * factorial (x - 1)
diff --git a/eg/fib01.txt b/eg/fib01.txt
--- a/eg/fib01.txt
+++ b/eg/fib01.txt
@@ -18,10 +18,10 @@
 -- looking through 16 candidates of size 4
 -- looking through 44 candidates of size 5
 -- looking through 92 candidates of size 6
--- looking through 234 candidates of size 7
--- looking through 544 candidates of size 8
--- looking through 1332 candidates of size 9
--- looking through 10676 candidates of size 10
--- tested 12956 candidates
+-- looking through 210 candidates of size 7
+-- looking through 520 candidates of size 8
+-- looking through 1197 candidates of size 9
+-- looking through 10436 candidates of size 10
+-- tested 12533 candidates
 cannot conjure
 
diff --git a/eg/fibonacci.txt b/eg/fibonacci.txt
--- a/eg/fibonacci.txt
+++ b/eg/fibonacci.txt
@@ -5,15 +5,15 @@
 -- looking through 3 candidates of size 2
 -- looking through 9 candidates of size 3
 -- looking through 9 candidates of size 4
--- looking through 30 candidates of size 5
--- looking through 30 candidates of size 6
--- looking through 156 candidates of size 7
--- looking through 157 candidates of size 8
--- looking through 813 candidates of size 9
--- looking through 797 candidates of size 10
--- looking through 4449 candidates of size 11
--- looking through 4438 candidates of size 12
--- tested 6539 candidates
+-- looking through 26 candidates of size 5
+-- looking through 27 candidates of size 6
+-- looking through 116 candidates of size 7
+-- looking through 120 candidates of size 8
+-- looking through 552 candidates of size 9
+-- looking through 540 candidates of size 10
+-- looking through 2663 candidates of size 11
+-- looking through 2675 candidates of size 12
+-- tested 4147 candidates
 fibonacci 0  =  1
 fibonacci 1  =  1
 fibonacci x  =  fibonacci (x - 1) + fibonacci (x - 2)
diff --git a/eg/list.txt b/eg/list.txt
--- a/eg/list.txt
+++ b/eg/list.txt
@@ -105,9 +105,9 @@
 -- looking through 20 candidates of size 7
 -- looking through 30 candidates of size 8
 -- looking through 56 candidates of size 9
--- looking through 114 candidates of size 10
--- looking through 216 candidates of size 11
--- tested 331 candidates
+-- looking through 112 candidates of size 10
+-- looking through 200 candidates of size 11
+-- tested 319 candidates
 ordered []  =  True
 ordered (x:xs)  =  ordered xs && (null xs || x <= head xs)
 
diff --git a/eg/oddeven.txt b/eg/oddeven.txt
--- a/eg/oddeven.txt
+++ b/eg/oddeven.txt
@@ -35,8 +35,8 @@
 -- looking through 0 candidates of size 2
 -- looking through 3 candidates of size 3
 -- looking through 1 candidates of size 4
--- looking through 50 candidates of size 5
--- tested 35 candidates
+-- looking through 46 candidates of size 5
+-- tested 31 candidates
 odd x  =  1 == x `mod` 2
 
 even :: Int -> Bool
@@ -46,7 +46,7 @@
 -- looking through 0 candidates of size 2
 -- looking through 3 candidates of size 3
 -- looking through 2 candidates of size 4
--- looking through 49 candidates of size 5
--- tested 26 candidates
+-- looking through 45 candidates of size 5
+-- tested 22 candidates
 even x  =  0 == x `mod` 2
 
diff --git a/eg/pow.txt b/eg/pow.txt
--- a/eg/pow.txt
+++ b/eg/pow.txt
@@ -7,9 +7,9 @@
 -- looking through 159 candidates of size 4
 -- looking through 433 candidates of size 5
 -- looking through 1382 candidates of size 6
--- looking through 4156 candidates of size 7
--- looking through 13406 candidates of size 8
--- tested 6403 candidates
+-- looking through 4136 candidates of size 7
+-- looking through 13292 candidates of size 8
+-- tested 6383 candidates
 pow x 0  =  1
 pow x y  =  x * pow x (y - 1)
 
diff --git a/eg/sort.hs b/eg/sort.hs
--- a/eg/sort.hs
+++ b/eg/sort.hs
@@ -74,6 +74,7 @@
   -- merge (x:xs) (y:ys)  =  if x <= y then x:merge xs (y:ys) else y:merge (x:xs) ys
   --                         2  3 4  5      678     9 10 11 12  13 14 15  16 17 18 19
   -- OOM after size 17, out of reach performance wise
+  -- update: cannot reach at size 19 on lapmatrud OOM
   conjureWith args{maxSize=12} "merge" merge'
     [ pr ([] :: [Int])
     , prim ":" ((:) :: Int -> [Int] -> [Int])
diff --git a/eg/tree.txt b/eg/tree.txt
--- a/eg/tree.txt
+++ b/eg/tree.txt
@@ -55,7 +55,7 @@
 -- looking through 14 candidates of size 5
 -- looking through 34 candidates of size 6
 -- looking through 98 candidates of size 7
--- looking through 283 candidates of size 8
+-- looking through 274 candidates of size 8
 -- tested 200 candidates
 height Leaf  =  -1
 height (Node t1 x t2)  =  1 + max (height t1) (height t2)
@@ -74,7 +74,7 @@
 -- looking through 0 candidates of size 9
 -- looking through 0 candidates of size 10
 -- looking through 0 candidates of size 11
--- looking through 96 candidates of size 12
+-- looking through 80 candidates of size 12
 -- tested 88 candidates
 mem x Leaf  =  False
 mem x (Node t1 y t2)  =  mem x t1 || (mem x t2 || x == y)
@@ -92,9 +92,9 @@
 -- looking through 32 candidates of size 8
 -- looking through 80 candidates of size 9
 -- looking through 56 candidates of size 10
--- looking through 450 candidates of size 11
--- looking through 708 candidates of size 12
--- tested 1359 candidates
+-- looking through 386 candidates of size 11
+-- looking through 596 candidates of size 12
+-- tested 1183 candidates
 cannot conjure
 
 ordered :: Tree -> Bool
diff --git a/mk/depend.mk b/mk/depend.mk
--- a/mk/depend.mk
+++ b/mk/depend.mk
@@ -20,6 +20,23 @@
   src/Conjure/Conjurable.hs \
   src/Conjure/Conjurable/Derive.hs \
   bench/candidates.hs
+bench/carry-on: \
+  bench/carry-on.hs \
+  mk/toplibs
+bench/carry-on.o: \
+  src/Conjure/Utils.hs \
+  src/Conjure/Red.hs \
+  src/Conjure/Reason.hs \
+  src/Conjure/Prim.hs \
+  src/Conjure.hs \
+  src/Conjure/Expr.hs \
+  src/Conjure/Engine.hs \
+  src/Conjure/Defn/Test.hs \
+  src/Conjure/Defn/Redundancy.hs \
+  src/Conjure/Defn.hs \
+  src/Conjure/Conjurable.hs \
+  src/Conjure/Conjurable/Derive.hs \
+  bench/carry-on.hs
 bench/erroneous: \
   bench/erroneous.hs \
   mk/toplibs
@@ -190,6 +207,23 @@
   src/Conjure/Conjurable.hs \
   src/Conjure/Conjurable/Derive.hs \
   bench/self.hs
+bench/strategies: \
+  bench/strategies.hs \
+  mk/toplibs
+bench/strategies.o: \
+  src/Conjure/Utils.hs \
+  src/Conjure/Red.hs \
+  src/Conjure/Reason.hs \
+  src/Conjure/Prim.hs \
+  src/Conjure.hs \
+  src/Conjure/Expr.hs \
+  src/Conjure/Engine.hs \
+  src/Conjure/Defn/Test.hs \
+  src/Conjure/Defn/Redundancy.hs \
+  src/Conjure/Defn.hs \
+  src/Conjure/Conjurable.hs \
+  src/Conjure/Conjurable/Derive.hs \
+  bench/strategies.hs
 bench/take-drop: \
   bench/take-drop.hs \
   mk/toplibs
@@ -224,6 +258,23 @@
   src/Conjure/Conjurable.hs \
   src/Conjure/Conjurable/Derive.hs \
   bench/terpret.hs
+bench/unique: \
+  bench/unique.hs \
+  mk/toplibs
+bench/unique.o: \
+  src/Conjure/Utils.hs \
+  src/Conjure/Red.hs \
+  src/Conjure/Reason.hs \
+  src/Conjure/Prim.hs \
+  src/Conjure.hs \
+  src/Conjure/Expr.hs \
+  src/Conjure/Engine.hs \
+  src/Conjure/Defn/Test.hs \
+  src/Conjure/Defn/Redundancy.hs \
+  src/Conjure/Defn.hs \
+  src/Conjure/Conjurable.hs \
+  src/Conjure/Conjurable/Derive.hs \
+  bench/unique.hs
 bench/weird: \
   bench/weird.hs \
   mk/toplibs
diff --git a/src/Conjure/Defn/Redundancy.hs b/src/Conjure/Defn/Redundancy.hs
--- a/src/Conjure/Defn/Redundancy.hs
+++ b/src/Conjure/Defn/Redundancy.hs
@@ -141,7 +141,7 @@
 -- | Returns whether a given 'Defn' is redundant
 --   with regards to root recursions.
 --
--- When there is a single base case and all recursive calls
+-- When there is a single constant base case and all recursive calls
 -- are at the root: we have a redundant function.
 -- (Modulo error functions, which are undesired anyway.)
 --
@@ -150,11 +150,6 @@
 --
 -- Above it does not really pays off to follow the recursive calls,
 -- at the end we always reach an empty list.
---
--- The same goes for the following:
---
--- > xs ? []  =  xs
--- > xs ? (x:ys)  =  xs ? ys
 isRedundantByRootRecursions :: Defn -> Bool
 isRedundantByRootRecursions d  =  case partition isGround $ map snd d of
   ([b], rs@(_:_))  ->  all isHole rs
diff --git a/src/Conjure/Engine.hs b/src/Conjure/Engine.hs
--- a/src/Conjure/Engine.hs
+++ b/src/Conjure/Engine.hs
@@ -159,11 +159,18 @@
   , maxEquationSize       :: Int  -- ^ maximum size of equation operands
   , maxSearchTests        :: Int  -- ^ maximum number of tests to search for defined values
   , maxDeconstructionSize :: Int  -- ^ maximum size of deconstructions (e.g.: @_ - 1@)
-  , requireDescent        :: Bool -- ^ require recursive calls to deconstruct arguments
+
+  -- advanced options --
+  , carryOn               :: Bool -- ^ whether to carry on after finding a suitable candidate
+  , showTheory            :: Bool -- ^ show theory discovered by Speculate used in pruning
   , usePatterns           :: Bool -- ^ use pattern matching to create (recursive) candidates
+
+  -- pruning options --
+  , rewriting             :: Bool -- ^ unique-modulo-rewriting candidates
+  , requireDescent        :: Bool -- ^ require recursive calls to deconstruct arguments
+  , adHocRedundancy       :: Bool -- ^ ad-hoc redundancy checks
   , copyBindings          :: Bool -- ^ copy partial definition bindings in candidates
   , atomicNumbers         :: Bool -- ^ restrict constant/ground numeric expressions to atoms
-  , showTheory            :: Bool -- ^ show theory discovered by Speculate used in pruning
   , uniqueCandidates      :: Bool -- ^ unique-modulo-testing candidates
   }
 
@@ -187,11 +194,18 @@
   , maxEquationSize        =   5
   , maxSearchTests         =  100000
   , maxDeconstructionSize  =   4
-  , requireDescent         =  True
+
+  -- advanced options --
+  , carryOn                =  False
+  , showTheory             =  False
   , usePatterns            =  True
+
+  -- pruning options --
+  , rewriting              =  True
+  , requireDescent         =  True
+  , adHocRedundancy        =  True
   , copyBindings           =  True
   , atomicNumbers          =  True
-  , showTheory             =  False
   , uniqueCandidates       =  False
   }
 
@@ -239,9 +253,15 @@
     -- when (n<=12) $ putStrLn $ unlines $ map showDefn cs
     case is of
       []     ->  pr (n+1) (t+nc) rs
-      (i:_)  ->  do let nc' = fromMaybe nc (findIndex (i==) cs)
-                    putStrLn $ "-- tested " ++ show (t+nc'+1) ++ " candidates"
-                    putStrLn $ showDefn i
+      (_:_)  ->  do pr1 t is cs
+                    when (carryOn args) $ pr (n+1) (t+nc) rs
+  pr1 t [] cs  =  return ()
+  pr1 t (i:is) cs  =  do
+    let (cs',cs'') = break (i==) cs
+    let t' = t + length cs' + 1
+    putStrLn $ "-- tested " ++ show t' ++ " candidates"
+    putStrLn $ showDefn i
+    when (carryOn args) $ pr1 t' is (drop 1 cs'')
   rs  =  zip iss css
   (iss, css, ts, thy)  =  conjpure0With args nm f p es
   nRules  =  length (rules thy)
@@ -363,7 +383,8 @@
   eh  =  holeAsTypeOf efxs
   efxs  =  conjureVarApplication nm f
   (ef:exs)  =  unfoldApp efxs
-  keep  =  isRootNormalC thy . fastMostGeneralVariation
+  keep | rewriting  =  isRootNormalC thy . fastMostGeneralVariation
+       | otherwise  =  const True
   keepR | requireDescent  =  descends isDecOf efxs
         | otherwise       =  const True
     where
@@ -391,7 +412,7 @@
 -- | Return apparently unique candidate definitions
 --   using pattern matching.
 candidateDefnsC :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Defn]], Thy)
-candidateDefnsC Args{..} nm f ps  =  (discardT hasRedundantRecursion $ concatMapT fillingsFor fss,thy)
+candidateDefnsC Args{..} nm f ps  =  (discardT hasRedundant $ concatMapT fillingsFor fss,thy)
   where
   pats  =  conjurePats es nm f
   fss  =  concatMapT ps2fss pats
@@ -401,7 +422,8 @@
   efxs  =  conjureVarApplication nm f
   (ef:exs)  =  unfoldApp efxs
 
-  keep  =  isRootNormalC thy . fastMostGeneralVariation
+  keep | rewriting  =  isRootNormalC thy . fastMostGeneralVariation
+       | otherwise  =  const True
 
   appsWith :: Expr -> [Expr] -> [[Expr]]
   appsWith eh vs  =  enumerateAppsFor eh k $ vs ++ es
@@ -411,9 +433,14 @@
     -- discards non-atomic numeric ground expressions such as 1 + 1
     keepNumeric e  =  isFun e || isConst e || not (isGround e)
 
+  isRedundant | adHocRedundancy  =  \e -> isRedundantDefn e || isRedundantModuloRewriting (normalize thy) e
+              | otherwise        =  const False
+
+  hasRedundant | adHocRedundancy  =  hasRedundantRecursion
+               | otherwise        =  const False
+
   ps2fss :: [Expr] -> [[Defn]]
-  ps2fss pats  =  discardT (isRedundantModuloRewriting $ normalize thy)
-               .  discardT isRedundantDefn
+  ps2fss pats  =  discardT isRedundant
                .  products
                $  map p2eess pats
     where
diff --git a/src/Conjure/Reason.hs b/src/Conjure/Reason.hs
--- a/src/Conjure/Reason.hs
+++ b/src/Conjure/Reason.hs
@@ -55,10 +55,7 @@
 -- but nevertheless correct
 isRootNormalC :: Thy -> Expr -> Bool
 isRootNormalC thy e | not (isRootNormal thy e)  =  False
-isRootNormalC thy (ef :$ ex :$ ey)
-  | ex <= ey  =  True
-  | not (isCommutative thy ef)  =  True
-  | isRootNormal thy (ef :$ ey :$ ex)  =  False
+isRootNormalC thy (ef :$ ex :$ ey) | isCommutative thy ef  =  ex <= ey
 isRootNormalC _ _  =  True
 
 isRootNormalE :: Thy -> Expr -> Bool