diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -30,8 +30,10 @@
       - run: du -hd3 ~/.cabal ~/.ghc || true
 
       - run: haddock --version || sudo apt-get install ghc-haddock
-      - run: ghc   --version
-      - run: cabal --version
+      - run: ghc     --version
+      - run: cabal   --version
+      - run: haddock --version
+      - run: ghc-pkg list
 
       - name: Check out repository
         uses: actions/checkout@v2
@@ -86,8 +88,10 @@
       - run: make --version || apt-get update
       - run: make --version || apt-get install make
 
-      - run: ghc   --version
-      - run: cabal --version
+      - run: ghc     --version
+      - run: cabal   --version
+      - run: haddock --version
+      - run: ghc-pkg list
 
       - name: Check out repository
         uses: actions/checkout@v2
@@ -117,15 +121,8 @@
           key:          v1-${{ runner.os }}-stack-${{ hashFiles('stack.yaml') }}
           restore-keys: v1-${{ runner.os }}-stack-
 
-      - name: Check out repository
-        uses: actions/checkout@v2
-      - run: make test-via-stack
+      - run: stack --version
 
-  test-with-hugs:
-    runs-on: ubuntu-latest
-    needs: build-and-test
-    steps:
-      - run: sudo apt-get install hugs
       - name: Check out repository
         uses: actions/checkout@v2
-      - run: make hugs-test
+      - run: make test-via-stack
diff --git a/.gitignore b/.gitignore
--- a/.gitignore
+++ b/.gitignore
@@ -32,6 +32,7 @@
 eg/factorial
 eg/ints
 eg/list
+eg/tapps
 bench/self
 proto/u-conjure
 test/expr
diff --git a/Makefile b/Makefile
--- a/Makefile
+++ b/Makefile
@@ -10,6 +10,8 @@
   eg/factorial \
   eg/ints \
   eg/bools \
+  eg/list \
+  eg/tapps \
   bench/self \
   proto/u-conjure
 
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -46,22 +46,24 @@
 
 and
 
-	background :: [Expr]
-	background =
-	  [ val (0::Int)
-	  , val (1::Int)
-	  , value "+" ((+) :: Int -> Int -> Int)
-	  , value "*" ((*) :: Int -> Int -> Int)
-	  ]
+	primitives :: [Expr]
+	primitives  =  [ val (0::Int)
+	               , val (1::Int)
+	               , value "+" ((+) :: Int -> Int -> Int)
+	               , value "*" ((*) :: Int -> Int -> Int)
+	               ]
 
 running
 
-	> conjure "square" square background
+	> conjure "square" square primitives
 
 yields
 
 	square :: Int -> Int
-	-- looking through 815 candidates, 100% match, 3/3 assignments
+	-- testing 3 combinations of argument values
+	-- looking through 3 candidates of size 1
+	-- looking through 3 candidates of size 2
+	-- looking through 5 candidates of size 3
 	square x  =  x * x
 
 in less than a second.
@@ -84,27 +86,34 @@
 
 and
 
-	background :: [Expr]
-	background  =
-	  [ val (0::Int)
-	  , val (1::Int)
-	  , value "+" ((+) :: Int -> Int -> Int)
-	  , value "*" ((*) :: Int -> Int -> Int)
-	  , value "dec" (subtract 1 :: Int -> Int)
-	  , value "isZero" ((==0) :: Int -> Bool)
-	  , val False
-	  , val True
-	  ]
+	primitives :: [Expr]
+	primitives  =  [ val (0::Int)
+	               , val (1::Int)
+	               , value "+" ((+) :: Int -> Int -> Int)
+	               , value "*" ((*) :: Int -> Int -> Int)
+	               , value "dec" (subtract 1 :: Int -> Int)
+	               , value "==" ((==) :: Int -> Int -> Bool)
+	               ]
 
 running
 
-	> conjure "factorial" factorial background
+	> conjure "factorial" factorial primitives
 
 yields
 
 	factorial :: Int -> Int
-	-- looking through 8576 candidates, 100% match, 6/6 assignments
-	factorial x  =  if isZero x then 1 else x * factorial (dec x)
+	-- testing 6 combinations of argument values
+	-- looking through 3 candidates of size 1
+	-- looking through 5 candidates of size 2
+	-- looking through 8 candidates of size 3
+	-- looking through 26 candidates of size 4
+	-- looking through 59 candidates of size 5
+	-- looking through 167 candidates of size 6
+	-- looking through 581 candidates of size 7
+	-- looking through 1654 candidates of size 8
+	-- looking through 5754 candidates of size 9
+	-- looking through 17797 candidates of size 10
+	factorial n  =  if n == 0 then 1 else n * factorial (dec n)
 
 in about 3 seconds.
 
@@ -112,9 +121,9 @@
 
 It is also possible to generate:
 
-    factorial x  =  if x == 0 then 1 else x * factorial x - 1
+    factorial n  =  if n == 0 then 1 else n * factorial (n - 1)
 
-in about 30s by changing the background and increasing the size limit.
+in about 90s by including `(-) :: Int -> Int -> Int` in the primitives.
 
 
 Related work
diff --git a/TODO.md b/TODO.md
--- a/TODO.md
+++ b/TODO.md
@@ -3,11 +3,24 @@
 
 A non-exhaustive list of things TO DO for Conjure.
 
-* reduce to unique `candidateExprs` through testing.
-  We should only enumerate functions that were tested to be different.
-  We can limit the tests to the ones that are defined in the given function.
+* report number of "hit" assignments, add ill example as a bench
 
-* use partially defined implementations?
+* refactor `candidateExprs` and `conjpureWith`.
+  Move down conjuring of `(===)` from `conjpureWith` into `candidateExprs`.
+
+* refactor `conjureTiersFor` to use `conjureMaybeTiersFor`
+
+* implement `conjureHasTiers` and use it on `conjureMkEquation`;
+  this will make it easy to backport unique candidateExprs from the erased
+  commit back into the tool: just `discardLaterT (===)`.
+  Will this impact performance a bit?  I don't think so.
+
+
+### for later
+
+* allow conjuring from tests instead of partial definitions?
+
+* allow conjuring from partially defined implementations?
 
     partial :: ((Int -> Int) -> Int -> Int) -> (Int -> Int)
     partial impl  =  f
diff --git a/bench/runtime/zero/eg/arith.runtime b/bench/runtime/zero/eg/arith.runtime
--- a/bench/runtime/zero/eg/arith.runtime
+++ b/bench/runtime/zero/eg/arith.runtime
@@ -1,1 +1,1 @@
-4.55
+0.82
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.29
+7.31
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.31
+7.68
diff --git a/bench/runtime/zero/eg/ints.runtime b/bench/runtime/zero/eg/ints.runtime
--- a/bench/runtime/zero/eg/ints.runtime
+++ b/bench/runtime/zero/eg/ints.runtime
@@ -1,1 +1,1 @@
-1.95
+2.42
diff --git a/bench/runtime/zero/eg/list.runtime b/bench/runtime/zero/eg/list.runtime
new file mode 100644
--- /dev/null
+++ b/bench/runtime/zero/eg/list.runtime
@@ -0,0 +1,1 @@
+8.59
diff --git a/bench/runtime/zero/eg/tapps.runtime b/bench/runtime/zero/eg/tapps.runtime
new file mode 100644
--- /dev/null
+++ b/bench/runtime/zero/eg/tapps.runtime
@@ -0,0 +1,1 @@
+1.24
diff --git a/bench/self.hs b/bench/self.hs
--- a/bench/self.hs
+++ b/bench/self.hs
@@ -6,17 +6,17 @@
 
 main :: IO ()
 main = do
-  cj "?" ((+) :: Int -> Int -> Int)   background
-  cj "?" ((*) :: Int -> Int -> Int)   background
-  cj "i" ((+1) :: Int -> Int)         background
-  cj "d" ((subtract 1) :: Int -> Int) background
+  cj "?" ((+) :: Int -> Int -> Int)   primitives
+  cj "?" ((*) :: Int -> Int -> Int)   primitives
+  cj "i" ((+1) :: Int -> Int)         primitives
+  cj "d" ((subtract 1) :: Int -> Int) primitives
   where
   -- the monomorphism restriction strikes again
   cj :: Conjurable f => String -> f -> [Expr] -> IO ()
   cj  =  conjureWith args{maxSize=3,maxEquationSize=0}
 
-background :: [Expr]
-background =
+primitives :: [Expr]
+primitives =
   [ val (0::Int)
   , val (1::Int)
   , value "+" ((+) :: Int -> Int -> Int)
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.1.2
+version:             0.2.0
 synopsis:            conjure Haskell functions out of partial definitions
 description:
   Conjure is a tool that produces Haskell functions out of partial definitions.
@@ -47,7 +47,15 @@
                   , test/model/eg/*.out
                   , test/model/proto/*.out
                   , test/sdist
-tested-with: GHC==8.10
+tested-with: GHC==9.0
+           , GHC==8.10
+           , GHC==8.8
+           , GHC==8.6
+           , GHC==8.4
+           , GHC==8.2
+           , GHC==8.0
+           , GHC==7.10
+           , GHC==7.8
 
 source-repository head
   type:            git
@@ -56,7 +64,7 @@
 source-repository this
   type:            git
   location:        https://github.com/rudymatela/conjure
-  tag:             v0.1.2
+  tag:             v0.2.0
 
 library
   exposed-modules: Conjure
diff --git a/eg/arith.hs b/eg/arith.hs
--- a/eg/arith.hs
+++ b/eg/arith.hs
@@ -28,13 +28,13 @@
 
 main :: IO ()
 main = do
-  conjure "double" double background
-  conjure "add"    add    background
-  conjure "square" square background
-  conjure "tnpo"   tnpo   background
+  conjure "double" double primitives
+  conjure "add"    add    primitives
+  conjure "square" square primitives
+  conjure "tnpo"   tnpo   primitives
 
-background :: [Expr]
-background =
+primitives :: [Expr]
+primitives =
   [ val (0::Int)
   , val (1::Int)
   , value "+" ((+) :: Int -> Int -> Int)
diff --git a/eg/bools.hs b/eg/bools.hs
--- a/eg/bools.hs
+++ b/eg/bools.hs
@@ -16,15 +16,15 @@
 
 main :: IO ()
 main = do
-  conjure "and" (and' :: [Bool] -> Bool) background
-  conjure "or"  (or'  :: [Bool] -> Bool) background
+  conjure "and" (and' :: [Bool] -> Bool) primitives
+  conjure "or"  (or'  :: [Bool] -> Bool) primitives
 
   -- conjure can use fold as well
-  conjureWithMaxSize 4 "and" (and' :: [Bool] -> Bool) backgroundWithFold
-  conjureWithMaxSize 4 "or"  (or'  :: [Bool] -> Bool) backgroundWithFold
+  conjure "and" (and' :: [Bool] -> Bool) primitivesWithFold
+  conjure "or"  (or'  :: [Bool] -> Bool) primitivesWithFold
 
-background :: [Expr]
-background =
+primitives :: [Expr]
+primitives =
   [ value "not" not
   , value "||" (||)
   , value "&&" (&&)
@@ -33,10 +33,10 @@
   , value "tail" (tail :: [Bool] -> [Bool])
   ]
 
-backgroundWithFold :: [Expr]
-backgroundWithFold  =
+primitivesWithFold :: [Expr]
+primitivesWithFold  =
     value "foldr" (foldr :: (Bool -> Bool -> Bool) -> Bool -> [Bool] -> Bool)
-  : background
+  : primitives
 
 -- target (for and):
 
diff --git a/eg/factorial.hs b/eg/factorial.hs
--- a/eg/factorial.hs
+++ b/eg/factorial.hs
@@ -14,19 +14,23 @@
 
 
 main :: IO ()
-main  =  conjure "factorial n" factorial background
-
-
-background :: [Expr]
-background  =
-  [ val (0::Int)
-  , val (1::Int)
-  , value "+" ((+) :: Int -> Int -> Int)
-  , value "*" ((*) :: Int -> Int -> Int)
-  , value "dec" (subtract 1 :: Int -> Int)
-  , value "isZero" ((==0) :: Int -> Bool)
-  ]
+main  =  do
+  -- using enumFromTo
+  conjure "factorial n" factorial
+    [ val (1::Int)
+    , value "enumFromTo" (enumFromTo :: Int -> Int -> [Int])
+    , value "product" (product :: [Int] -> Int)
+    ]
 
+  -- explicit recursion
+  conjure "factorial n" factorial
+    [ val (0::Int)
+    , val (1::Int)
+    , value "+" ((+) :: Int -> Int -> Int)
+    , value "*" ((*) :: Int -> Int -> Int)
+    , value "dec" (subtract 1 :: Int -> Int)
+    , value "==" ((==) :: Int -> Int -> Bool)
+    ]
 
 -- the actual factorial function:
 -- factorial n  =  if n == 0 then 1 else n * factorial (n - 1)
@@ -41,3 +45,47 @@
 --
 -- factorial n  =  if (isZero n) then 1 else (n * factorial (dec n))
 --                 1   2      3       4       5 6 7          8   9 symbols
+
+
+{-
+-- Paramorphism of Naturals encoded as integers
+para :: (Int -> b -> b) -> b -> Int -> b
+para (?) z  =  p
+  where
+  p n  |  n < 0  =  z  -- no negatives for you :-)
+  p 0  =  z
+  p n  =  n ? p (n-1)
+
+The following works with a maxSize of 4, but not with a maxSize of 5.
+
+  -- using a paramorphism
+  conjure "factorial n" factorial
+    [ val (1::Int)
+    , value "para" (para :: (Int->Int->Int) -> Int -> Int -> Int)
+    , value "*" ((*) :: Int -> Int -> Int)
+    ]
+
+
+the factorial function is the following:
+
+fact  =  para (*) 1
+
+
+now consider the following grow_fast function:
+
+grow_fast  =  para (para (*)) 1  :: Integer -> Integer
+
+
+> growFast 1
+1
+> growFast 2
+2
+> growFast 3
+6
+> growFast 4
+2880
+> growFast 5
+7148302174930174893017438921... 8000 digits!
+> growFast 6
+stack overflow
+-}
diff --git a/eg/ints.hs b/eg/ints.hs
--- a/eg/ints.hs
+++ b/eg/ints.hs
@@ -25,16 +25,16 @@
 
 main :: IO ()
 main = do
-  conjure "second"  (second   :: [Int] -> Int) background
-  conjure "third"   (third    :: [Int] -> Int) background
-  conjure "sum"     (sum'     :: [Int] -> Int) background
-  conjure "product" (product' :: [Int] -> Int) background
+  conjure "second"  (second   :: [Int] -> Int) primitives
+  conjure "third"   (third    :: [Int] -> Int) primitives
+  conjure "sum"     (sum'     :: [Int] -> Int) primitives
+  conjure "product" (product' :: [Int] -> Int) primitives
 
-  conjureWithMaxSize 4 "sum"     (sum'     :: [Int] -> Int) backgroundWithFold
-  conjureWithMaxSize 4 "product" (product' :: [Int] -> Int) backgroundWithFold
+  conjure "sum"     (sum'     :: [Int] -> Int) primitivesWithFold
+  conjure "product" (product' :: [Int] -> Int) primitivesWithFold
 
-background :: [Expr]
-background =
+primitives :: [Expr]
+primitives =
   [ val (0 :: Int)
   , val (1 :: Int)
   , value "+" ((+) :: Int -> Int -> Int)
@@ -44,10 +44,10 @@
   , value "tail" (tail :: [Int] -> [Int])
   ]
 
-backgroundWithFold :: [Expr]
-backgroundWithFold  =
+primitivesWithFold :: [Expr]
+primitivesWithFold  =
     value "foldr" (foldr :: (Int -> Int -> Int) -> Int -> [Int] -> Int)
-  : background
+  : primitives
 
 -- sum xs      =  if null xs then 0 else head xs + sum (tail xs)
 -- product xs  =  if null xs then 1 else head xs * product (tail xs)
diff --git a/eg/list.hs b/eg/list.hs
--- a/eg/list.hs
+++ b/eg/list.hs
@@ -31,7 +31,7 @@
 main = do
   -- length xs  =  if null xs then 0 else 1 + length (tail xs)
   --               1  2    3       4      5 6 7       8    9
-  conjureWith args {maxSize = 9} "length" length'
+  conjure "length" length'
     [ val (0 :: Int)
     , val (1 :: Int)
     , value "+" ((+) :: Int -> Int -> Int)
@@ -41,7 +41,8 @@
 
   -- reverse xs  =  if null xs then [] else reverse (tail xs) ++ [head xs]
   --                1  2    3       4       5        6    7   8  9 10 11 12
-  conjureWith args {maxSize = 11} "reverse" reverse'
+  -- needs size 11 with unit
+  conjure "reverse" reverse'
     [ val ([] :: [Int])
     , value "unit" ((:[]) :: Int -> [Int])
     , value "++" ((++) :: [Int] -> [Int] -> [Int])
@@ -52,10 +53,41 @@
 
   -- sort xs  =  if null xs then [] else insert (head xs) (sort (tail xs))
   --             1  2    3       4       5       6    7    8     9    10
-  conjureWith args {maxSize = 10} "sort" sort'
+  conjure "sort" sort'
     [ val ([] :: [Int])
     , value "insert" (insert :: Int -> [Int] -> [Int])
     , value "head" (head :: [Int] -> Int)
     , value "tail" (tail :: [Int] -> [Int])
     , value "null" (null :: [Int] -> Bool)
+    ]
+
+  -- now through folds
+  -- length xs  =  foldr (const (1 +)) 0 xs
+  conjure "length" length'
+    [ val (0 :: Int)
+    , val (1 :: Int)
+    , value "+" ((+) :: Int -> Int -> Int)
+    , value "foldr" (foldr :: (Int -> Int -> Int) -> Int -> [Int] -> Int)
+    , value "const" (const :: (Int -> Int) -> Int -> (Int -> Int)) -- cheating?
+    ]
+
+  -- now through folds and some cheating
+  --  reverse xs  =  foldr (\x xs -> xs ++ [x]) [] xs
+  --  reverse xs  =  foldr (flip (++) . unit) [] xs
+  conjure "reverse" reverse'
+    [ val ([] :: [Int])
+    , value "unit" ((:[]) :: Int -> [Int])
+    , value "++" ((++) :: [Int] -> [Int] -> [Int])
+    , value "foldr" (foldr :: (Int->[Int]->[Int]) -> [Int] -> [Int] -> [Int])
+    -- these last two are cheats:
+    , value "flip" (flip :: ([Int]->[Int]->[Int]) -> [Int] -> [Int] -> [Int])
+    , value "." ((.) :: ([Int]->[Int]->[Int]) -> (Int->[Int]) -> Int -> [Int] -> [Int])
+    ]
+
+  -- now through folds
+  -- sort xs  =  foldr insert [] xs
+  conjure "sort" sort'
+    [ val ([] :: [Int])
+    , value "insert" (insert :: Int -> [Int] -> [Int])
+    , value "foldr" (foldr :: (Int -> [Int] -> [Int]) -> [Int] -> [Int] -> [Int])
     ]
diff --git a/eg/tapps.hs b/eg/tapps.hs
new file mode 100644
--- /dev/null
+++ b/eg/tapps.hs
@@ -0,0 +1,81 @@
+-- tapps.hs: conjure with (portable) type applications
+--
+-- Copyright (C) 2021 Rudy Matela
+-- Distributed under the 3-Clause BSD licence (see the file LICENSE).
+{-# LANGUAGE CPP #-}
+#if __GLASGOW_HASKELL__ < 800
+#else
+{-# LANGUAGE TypeApplications #-}
+#endif
+
+import Conjure
+
+third :: [Int] -> Int
+third [x,y,z]  =  z
+third [x,y,z,w]  =  z
+
+product' :: [Int] -> Int
+product' [x]      =  x
+product' [x,y]    =  x*y
+product' [x,y,z]  =  x*y*z
+
+main :: IO ()
+main = do
+  conjure "third"   third    primitives
+  conjure "product" product' primitives
+  conjure "product" product' primitivesWithFold
+
+primitives :: [Expr]
+primitives =
+  [ val (0 :: Int)
+  , val (1 :: Int)
+#if __GLASGOW_HASKELL__ < 800
+  , value "+" ((+) :: Int -> Int -> Int)
+  , value "*" ((*) :: Int -> Int -> Int)
+  , value "null" (null :: [Int] -> Bool)
+  , value "head" (head :: [Int] -> Int)
+  , value "tail" (tail :: [Int] -> [Int])
+#else
+  , value "+" ((+) @Int)
+  , value "*" ((*) @Int)
+-- the following #if was added just for dramatic effect (see notes below)
+#if __GLASGOW_HASKELL__ < 710
+  , value "null" (null @Int)
+#else
+  , value "null" (null @[] @Int)
+#endif
+  , value "head" (head @Int)
+  , value "tail" (tail @Int)
+#endif
+  ]
+
+primitivesWithFold :: [Expr]
+#if __GLASGOW_HASKELL__ < 800
+primitivesWithFold  =
+    value "foldr" (foldr :: (Int -> Int -> Int) -> Int -> [Int] -> Int)
+  : primitives
+#else
+-- the following #if was added just for dramatic effect (see notes below)
+#if __GLASGOW_HASKELL__ < 710
+primitivesWithFold  =  value "foldr" (foldr @Int @Int) : primitives
+#else
+primitivesWithFold  =  value "foldr" (foldr @[] @Int @Int) : primitives
+#endif
+#endif
+
+-- Some notes:
+--
+-- From GHC 7.8 to GHC 7.10,
+-- null, foldr and other functions were generalized
+-- from lists to foldable containers.
+-- The type application for the old version of null
+-- is different than the one for the new version.
+--
+-- In the case of this file this is not really an issue
+-- as the above change was introduced before TypeApplications even existed.
+--
+-- This illustrates that
+-- we may have to use a different type application patterns
+-- when using different versions of libraries.
+-- In some cases, code using TypeApplications may be
+-- less portable than it's full type binding counterparts.
diff --git a/mk/depend.mk b/mk/depend.mk
--- a/mk/depend.mk
+++ b/mk/depend.mk
@@ -58,6 +58,16 @@
   src/Conjure/Engine.hs \
   src/Conjure/Conjurable.hs \
   eg/list.hs
+eg/tapps: \
+  eg/tapps.hs \
+  mk/toplibs
+eg/tapps.o: \
+  src/Conjure/Utils.hs \
+  src/Conjure.hs \
+  src/Conjure/Expr.hs \
+  src/Conjure/Engine.hs \
+  src/Conjure/Conjurable.hs \
+  eg/tapps.hs
 mk/All.o: \
   src/Conjure/Utils.hs \
   src/Conjure.hs \
diff --git a/src/Conjure.hs b/src/Conjure.hs
--- a/src/Conjure.hs
+++ b/src/Conjure.hs
@@ -21,8 +21,8 @@
 --
 -- Step 2: declare a list with the potential building blocks:
 --
--- > background :: [Expr]
--- > background =
+-- > primitives :: [Expr]
+-- > primitives =
 -- >   [ val (0::Int)
 -- >   , val (1::Int)
 -- >   , value "+" ((+) :: Int -> Int -> Int)
@@ -31,9 +31,12 @@
 --
 -- Step 3: call conjure and see your generated function:
 --
--- > > conjure "square" square background
+-- > > conjure "square" square primitives
 -- > square :: Int -> Int
--- > -- looking through 815 candidates, 100% match, 3/3 assignments
+-- > -- testing 3 combinations of argument values
+-- > -- looking through 3 candidates of size 1
+-- > -- looking through 3 candidates of size 2
+-- > -- looking through 5 candidates of size 3
 -- > square x  =  x * x
 {-# LANGUAGE CPP #-}
 module Conjure
diff --git a/src/Conjure/Engine.hs b/src/Conjure/Engine.hs
--- a/src/Conjure/Engine.hs
+++ b/src/Conjure/Engine.hs
@@ -58,7 +58,7 @@
 args :: Args
 args = Args
   { maxTests           =  60
-  , maxSize            =   9
+  , maxSize            =  12
   , maxRecursiveCalls  =   1
   , maxEquationSize    =   5
   , maxRecursionSize   =  60
@@ -66,51 +66,45 @@
 
 -- | Like 'conjure' but in the pure world.
 --
--- Returns a triple whose:
---
--- 1. first element is the number of candidates considered
---
--- 2. second element is the number of defined points in the given function
+-- Returns a triple with:
 --
--- 3. third element is a list of implementations encoded as 'Expr's
---    paired with the number of matching points.
-conjpure :: Conjurable f => String -> f -> [Expr] -> (Int,Int,[(Int,Expr)])
+-- 1. tiers of implementations
+-- 2. tiers of candidate bodies
+-- 3. a list of tests
+conjpure :: Conjurable f => String -> f -> [Expr] -> ([[Expr]], [[Expr]], [Expr])
 conjpure =  conjpureWith args
 
 -- | Like 'conjpure' but allows setting options through 'Args' and 'args'.
-conjpureWith :: Conjurable f => Args -> String -> f -> [Expr] -> (Int,Int,[(Int,Expr)])
-conjpureWith Args{..} nm f es  =  (length candidates,totalDefined,) $ sortBy compareResult
-  [ (ffxx .=. re, ffxx -==- e)
-  | e <- candidates
-  , apparentlyTerminates rrff e
-  , let re = recursexpr maxRecursionSize vffxx e
-  , ffxx ?=? re
-  ]
+conjpureWith :: Conjurable f => Args -> String -> f -> [Expr] -> ([[Expr]], [[Expr]], [Expr])
+conjpureWith Args{..} nm f es  =  (implementationsT, candidatesT, tests)
   where
-  totalDefined  =  ffxx .=. ffxx
-  candidates  =  filter (\e -> typ e == typ ffxx)
-              .  concat
-              .  take maxSize
-              $  candidateExprs nm f maxEquationSize maxRecursiveCalls (===)
-                 [nub $ [val False, val True] ++ es ++ conjureIfs f]
+  tests  =  [ffxx //- bs | bs <- dbss]
+  implementationsT  =  mapT (vffxx -==-) $ filterT implements candidatesT
+  implements e  =  apparentlyTerminates rrff e
+                && ffxx ?=? recursexpr maxRecursionSize vffxx e
+  candidatesT  =  filterT (\e -> typ e == typ ffxx)
+               .  take maxSize
+               $  candidateExprs nm f maxEquationSize maxRecursiveCalls (===) es
   ffxx   =  canonicalApplication nm f
   vffxx  =  canonicalVarApplication nm f
   (rrff:_)   =  unfoldApp vffxx
 
-  (===), (?=?) :: Expr -> Expr -> Bool
-  e1 === e2  =  isReallyTrue      (e1 -==- e2)
+  e1 === e2  =  isReallyTrue (e1 -==- e2)
   e1 ?=? e2  =  isTrueWhenDefined (e1 -==- e2)
-
-  e1 .=. e2  =  countTrue         (e1 -==- e2)
   (-==-)  =  conjureMkEquation f
 
-  isTrueWhenDefined  =  all (errorToTrue  . eval False) . gs
-  isReallyTrue       =  all (errorToFalse . eval False) . gs
-  countTrue        =  count (errorToFalse . eval False) . gs
+  isTrueWhenDefined e  =  all (errorToFalse . eval False) $ map (e //-) dbss
+  isReallyTrue  =  all (errorToFalse . eval False) . gs
 
   gs :: Expr -> [Expr]
   gs  =  take maxTests . grounds (conjureTiersFor f)
 
+  bss, dbss :: [[(Expr,Expr)]]
+  bss  =  take maxTests $ groundBinds (conjureTiersFor f) ffxx
+  dbss  =  [bs | bs <- bss, errorToFalse . eval False $ e //- bs]
+    where
+    e  =  ffxx -==- ffxx
+
 -- | Conjures an implementation of a partially defined function.
 --
 -- Takes a 'String' with the name of a function,
@@ -124,8 +118,8 @@
 -- > square 1  =  1
 -- > square 2  =  4
 -- >
--- > background :: [Expr]
--- > background =
+-- > primitives :: [Expr]
+-- > primitives =
 -- >   [ val (0::Int)
 -- >   , val (1::Int)
 -- >   , value "+" ((+) :: Int -> Int -> Int)
@@ -134,12 +128,15 @@
 --
 -- The conjure function does the following:
 --
--- > > conjure "square" square background
+-- > > conjure "square" square primitives
 -- > square :: Int -> Int
--- > -- looking through 815 candidates, 100% match, 3/3 assignments
+-- > -- testing 3 combinations of argument values
+-- > -- looking through 3 candidates of size 1
+-- > -- looking through 3 candidates of size 2
+-- > -- looking through 5 candidates of size 3
 -- > square x  =  x * x
 --
--- The background is defined with 'val' and 'value'.
+-- The primitives list is defined with 'val' and 'value'.
 conjure :: Conjurable f => String -> f -> [Expr] -> IO ()
 conjure  =  conjureWith args
 
@@ -159,17 +156,18 @@
 conjureWith :: Conjurable f => Args -> String -> f -> [Expr] -> IO ()
 conjureWith args nm f es  =  do
   print (var (head $ words nm) f)
-  putStr $ "-- looking through " ++ show ncs ++ " candidates"
-  hFlush stdout
-  case rs of
-    []    -> putStrLn $ "\ncannot conjure"
-    ((n,e):_) -> do putStrLn $ ", " ++ showMatch n
-                    putStrLn $ showEq e
---  nes -> putStrLn . unlines $ "":[showEq e ++ "  -- " ++ show n | (n,e) <- nes]
-  putStrLn ""
+  putStrLn $ "-- testing " ++ show (length ts) ++ " combinations of argument values"
+  pr 1 rs
   where
-  (ncs,t,rs)  =  conjpureWith args nm f es
-  showMatch n  =  show (n % t) ++ "% match, " ++ show n ++ "/" ++ show t ++ " assignments"
+  pr n []  =  putStrLn $ "cannot conjure"
+  pr n ((is,es):rs)  =  do
+    putStrLn $ "-- looking through " ++ show (length es) ++ " candidates of size " ++ show n
+    case is of
+      []     ->  pr (n+1) rs
+      (i:_)  ->  do putStrLn $ showEq i
+                    putStrLn ""
+  rs  =  zip iss css
+  (iss, css, ts)  =  conjpureWith args nm f es
   showEq eq  =  showExpr (lhs eq) ++ "  =  " ++ showExpr (rhs eq)
 
 candidateExprs :: Conjurable f
@@ -177,9 +175,20 @@
                -> Int
                -> Int
                -> (Expr -> Expr -> Bool)
-               -> [[Expr]]
+               -> [Expr]
                -> [[Expr]]
-candidateExprs nm f sz mc (===) ess  =  expressionsT $ [ef:exs] \/ ess
+candidateExprs nm f sz mc (===) es  =
+  candidateExprsT nm f sz mc (===)
+    [nub $ [val False, val True] ++ es ++ conjureIfs f]
+
+candidateExprsT :: Conjurable f
+                => String -> f
+                -> Int
+                -> Int
+                -> (Expr -> Expr -> Bool)
+                -> [[Expr]]
+                -> [[Expr]]
+candidateExprsT nm f sz mc (===) ess  =  expressionsT $ [ef:exs] \/ ess
   where
   (ef:exs)  =  unfoldApp $ canonicalVarApplication nm f
   thy  =  theoryFromAtoms (===) sz $ [conjureHoles f] \/ ess
diff --git a/src/Conjure/Expr.hs b/src/Conjure/Expr.hs
--- a/src/Conjure/Expr.hs
+++ b/src/Conjure/Expr.hs
@@ -168,7 +168,7 @@
 -- > > ifFor (undefined :: String)
 -- > if :: Bool -> [Char] -> [Char] -> [Char]
 --
--- You need to provide this as part of your building blocks on the background
+-- You need to provide this as part of your building blocks on the primitives
 -- if you want recursive functions to be considered and produced.
 ifFor :: Typeable a => a -> Expr
 ifFor a  =  value "if" (\p x y -> if p then x else y `asTypeOf` a)
diff --git a/test/model/bench/self.out b/test/model/bench/self.out
--- a/test/model/bench/self.out
+++ b/test/model/bench/self.out
@@ -1,16 +1,27 @@
 (?) :: Int -> Int -> Int
--- looking through 52 candidates, 100% match, 60/60 assignments
+-- testing 60 combinations of argument values
+-- looking through 4 candidates of size 1
+-- looking through 0 candidates of size 2
+-- looking through 48 candidates of size 3
 x ? y  =  x + y
 
 (?) :: Int -> Int -> Int
--- looking through 52 candidates, 100% match, 60/60 assignments
+-- testing 60 combinations of argument values
+-- looking through 4 candidates of size 1
+-- looking through 0 candidates of size 2
+-- looking through 48 candidates of size 3
 x ? y  =  x * y
 
 i :: Int -> Int
--- looking through 24 candidates, 100% match, 60/60 assignments
+-- testing 60 combinations of argument values
+-- looking through 3 candidates of size 1
+-- looking through 3 candidates of size 2
+-- looking through 18 candidates of size 3
 i x  =  x + 1
 
 d :: Int -> Int
--- looking through 24 candidates
+-- testing 60 combinations of argument values
+-- looking through 3 candidates of size 1
+-- looking through 3 candidates of size 2
+-- looking through 18 candidates of size 3
 cannot conjure
-
diff --git a/test/model/eg/arith.out b/test/model/eg/arith.out
--- a/test/model/eg/arith.out
+++ b/test/model/eg/arith.out
@@ -1,16 +1,32 @@
 double :: Int -> Int
--- looking through 815 candidates, 100% match, 4/4 assignments
+-- testing 4 combinations of argument values
+-- looking through 3 candidates of size 1
+-- looking through 3 candidates of size 2
+-- looking through 5 candidates of size 3
 double x  =  x + x
 
 add :: Int -> Int -> Int
--- looking through 28024 candidates, 100% match, 4/4 assignments
+-- testing 4 combinations of argument values
+-- looking through 4 candidates of size 1
+-- looking through 0 candidates of size 2
+-- looking through 29 candidates of size 3
 add x y  =  x + y
 
 square :: Int -> Int
--- looking through 815 candidates, 100% match, 3/3 assignments
+-- testing 3 combinations of argument values
+-- looking through 3 candidates of size 1
+-- looking through 3 candidates of size 2
+-- looking through 5 candidates of size 3
 square x  =  x * x
 
 tnpo :: Int -> Int
--- looking through 815 candidates, 100% match, 3/3 assignments
+-- testing 3 combinations of argument values
+-- looking through 3 candidates of size 1
+-- looking through 3 candidates of size 2
+-- looking through 5 candidates of size 3
+-- looking through 20 candidates of size 4
+-- looking through 13 candidates of size 5
+-- looking through 97 candidates of size 6
+-- looking through 42 candidates of size 7
 tnpo x  =  x + (x + (x + 1))
 
diff --git a/test/model/eg/bools.out b/test/model/eg/bools.out
--- a/test/model/eg/bools.out
+++ b/test/model/eg/bools.out
@@ -1,16 +1,44 @@
 and :: [Bool] -> Bool
--- looking through 1207 candidates, 100% match, 14/14 assignments
+-- testing 14 combinations of argument values
+-- looking through 2 candidates of size 1
+-- looking through 3 candidates of size 2
+-- looking through 6 candidates of size 3
+-- looking through 6 candidates of size 4
+-- looking through 16 candidates of size 5
+-- looking through 41 candidates of size 6
+-- looking through 103 candidates of size 7
+-- looking through 278 candidates of size 8
+-- looking through 752 candidates of size 9
 and ps  =  null ps || head ps && and (tail ps)
 
 or :: [Bool] -> Bool
--- looking through 1207 candidates, 78% match, 11/14 assignments
-or ps  =  head ps || or (tail ps)
+-- testing 14 combinations of argument values
+-- looking through 2 candidates of size 1
+-- looking through 3 candidates of size 2
+-- looking through 6 candidates of size 3
+-- looking through 6 candidates of size 4
+-- looking through 16 candidates of size 5
+-- looking through 41 candidates of size 6
+-- looking through 103 candidates of size 7
+-- looking through 278 candidates of size 8
+-- looking through 752 candidates of size 9
+-- looking through 1963 candidates of size 10
+-- looking through 5427 candidates of size 11
+or ps  =  not (null ps || not (head ps || or (tail ps)))
 
 and :: [Bool] -> Bool
--- looking through 19 candidates, 100% match, 14/14 assignments
+-- testing 14 combinations of argument values
+-- looking through 2 candidates of size 1
+-- looking through 3 candidates of size 2
+-- looking through 6 candidates of size 3
+-- looking through 8 candidates of size 4
 and ps  =  foldr (&&) True ps
 
 or :: [Bool] -> Bool
--- looking through 19 candidates, 100% match, 14/14 assignments
+-- testing 14 combinations of argument values
+-- looking through 2 candidates of size 1
+-- looking through 3 candidates of size 2
+-- looking through 6 candidates of size 3
+-- looking through 8 candidates of size 4
 or ps  =  foldr (||) False ps
 
diff --git a/test/model/eg/factorial.out b/test/model/eg/factorial.out
--- a/test/model/eg/factorial.out
+++ b/test/model/eg/factorial.out
@@ -1,4 +1,22 @@
 factorial :: Int -> Int
--- looking through 8576 candidates, 100% match, 6/6 assignments
-factorial n  =  if isZero n then 1 else n * factorial (dec n)
+-- testing 6 combinations of argument values
+-- looking through 2 candidates of size 1
+-- looking through 2 candidates of size 2
+-- looking through 0 candidates of size 3
+-- looking through 2 candidates of size 4
+factorial n  =  product (enumFromTo 1 n)
+
+factorial :: Int -> Int
+-- testing 6 combinations of argument values
+-- looking through 3 candidates of size 1
+-- looking through 5 candidates of size 2
+-- looking through 8 candidates of size 3
+-- looking through 26 candidates of size 4
+-- looking through 59 candidates of size 5
+-- looking through 167 candidates of size 6
+-- looking through 581 candidates of size 7
+-- looking through 1654 candidates of size 8
+-- looking through 5754 candidates of size 9
+-- looking through 17797 candidates of size 10
+factorial n  =  if n == 0 then 1 else n * factorial (dec n)
 
diff --git a/test/model/eg/ints.out b/test/model/eg/ints.out
--- a/test/model/eg/ints.out
+++ b/test/model/eg/ints.out
@@ -1,24 +1,59 @@
 second :: [Int] -> Int
--- looking through 636 candidates, 100% match, 47/47 assignments
+-- testing 47 combinations of argument values
+-- looking through 2 candidates of size 1
+-- looking through 2 candidates of size 2
+-- looking through 3 candidates of size 3
 second xs  =  head (tail xs)
 
 third :: [Int] -> Int
--- looking through 636 candidates, 100% match, 34/34 assignments
+-- testing 34 combinations of argument values
+-- looking through 2 candidates of size 1
+-- looking through 2 candidates of size 2
+-- looking through 3 candidates of size 3
+-- looking through 5 candidates of size 4
 third xs  =  head (tail (tail xs))
 
 sum :: [Int] -> Int
--- looking through 636 candidates, 13% match, 5/37 assignments
-sum xs  =  if null (tail xs) then head xs else sum xs
+-- testing 37 combinations of argument values
+-- looking through 2 candidates of size 1
+-- looking through 2 candidates of size 2
+-- looking through 3 candidates of size 3
+-- looking through 5 candidates of size 4
+-- looking through 13 candidates of size 5
+-- looking through 26 candidates of size 6
+-- looking through 63 candidates of size 7
+-- looking through 154 candidates of size 8
+-- looking through 368 candidates of size 9
+-- looking through 902 candidates of size 10
+sum xs  =  if null xs then 0 else head xs + sum (tail xs)
 
 product :: [Int] -> Int
--- looking through 636 candidates, 13% match, 5/37 assignments
-product xs  =  if null (tail xs) then head xs else product xs
+-- testing 37 combinations of argument values
+-- looking through 2 candidates of size 1
+-- looking through 2 candidates of size 2
+-- looking through 3 candidates of size 3
+-- looking through 5 candidates of size 4
+-- looking through 13 candidates of size 5
+-- looking through 26 candidates of size 6
+-- looking through 63 candidates of size 7
+-- looking through 154 candidates of size 8
+-- looking through 368 candidates of size 9
+-- looking through 902 candidates of size 10
+product xs  =  if null xs then 1 else head xs * product (tail xs)
 
 sum :: [Int] -> Int
--- looking through 15 candidates, 100% match, 37/37 assignments
+-- testing 37 combinations of argument values
+-- looking through 2 candidates of size 1
+-- looking through 2 candidates of size 2
+-- looking through 3 candidates of size 3
+-- looking through 8 candidates of size 4
 sum xs  =  foldr (+) 0 xs
 
 product :: [Int] -> Int
--- looking through 15 candidates, 100% match, 37/37 assignments
+-- testing 37 combinations of argument values
+-- looking through 2 candidates of size 1
+-- looking through 2 candidates of size 2
+-- looking through 3 candidates of size 3
+-- looking through 8 candidates of size 4
 product xs  =  foldr (*) 1 xs
 
diff --git a/test/model/eg/list.out b/test/model/eg/list.out
new file mode 100644
--- /dev/null
+++ b/test/model/eg/list.out
@@ -0,0 +1,71 @@
+length :: [Int] -> Int
+-- testing 38 combinations of argument values
+-- looking through 2 candidates of size 1
+-- looking through 1 candidates of size 2
+-- looking through 2 candidates of size 3
+-- looking through 3 candidates of size 4
+-- looking through 5 candidates of size 5
+-- looking through 11 candidates of size 6
+-- looking through 22 candidates of size 7
+-- looking through 53 candidates of size 8
+-- looking through 101 candidates of size 9
+length xs  =  if null xs then 0 else 1 + length (tail xs)
+
+reverse :: [Int] -> [Int]
+-- testing 38 combinations of argument values
+-- looking through 2 candidates of size 1
+-- looking through 4 candidates of size 2
+-- looking through 9 candidates of size 3
+-- looking through 24 candidates of size 4
+-- looking through 65 candidates of size 5
+-- looking through 215 candidates of size 6
+-- looking through 673 candidates of size 7
+-- looking through 2178 candidates of size 8
+-- looking through 7154 candidates of size 9
+-- looking through 23801 candidates of size 10
+-- looking through 80160 candidates of size 11
+reverse xs  =  if null xs then xs else reverse (tail xs) ++ unit (head xs)
+
+sort :: [Int] -> [Int]
+-- testing 30 combinations of argument values
+-- looking through 2 candidates of size 1
+-- looking through 4 candidates of size 2
+-- looking through 6 candidates of size 3
+-- looking through 12 candidates of size 4
+-- looking through 31 candidates of size 5
+-- looking through 98 candidates of size 6
+-- looking through 287 candidates of size 7
+-- looking through 792 candidates of size 8
+-- looking through 2220 candidates of size 9
+-- looking through 6516 candidates of size 10
+sort xs  =  if null xs then xs else insert (head xs) (sort (tail xs))
+
+length :: [Int] -> Int
+-- testing 38 combinations of argument values
+-- looking through 2 candidates of size 1
+-- looking through 1 candidates of size 2
+-- looking through 1 candidates of size 3
+-- looking through 4 candidates of size 4
+-- looking through 4 candidates of size 5
+-- looking through 27 candidates of size 6
+length xs  =  foldr (const (1 +)) 0 xs
+
+reverse :: [Int] -> [Int]
+-- testing 38 combinations of argument values
+-- looking through 2 candidates of size 1
+-- looking through 2 candidates of size 2
+-- looking through 1 candidates of size 3
+-- looking through 5 candidates of size 4
+-- looking through 1 candidates of size 5
+-- looking through 25 candidates of size 6
+-- looking through 77 candidates of size 7
+reverse xs  =  foldr (flip (++) . unit) [] xs
+
+sort :: [Int] -> [Int]
+-- testing 30 combinations of argument values
+-- looking through 2 candidates of size 1
+-- looking through 2 candidates of size 2
+-- looking through 0 candidates of size 3
+-- looking through 2 candidates of size 4
+sort xs  =  foldr insert [] xs
+
diff --git a/test/model/eg/tapps.out b/test/model/eg/tapps.out
new file mode 100644
--- /dev/null
+++ b/test/model/eg/tapps.out
@@ -0,0 +1,30 @@
+third :: [Int] -> Int
+-- testing 34 combinations of argument values
+-- looking through 2 candidates of size 1
+-- looking through 2 candidates of size 2
+-- looking through 3 candidates of size 3
+-- looking through 5 candidates of size 4
+third xs  =  head (tail (tail xs))
+
+product :: [Int] -> Int
+-- testing 37 combinations of argument values
+-- looking through 2 candidates of size 1
+-- looking through 2 candidates of size 2
+-- looking through 3 candidates of size 3
+-- looking through 5 candidates of size 4
+-- looking through 13 candidates of size 5
+-- looking through 26 candidates of size 6
+-- looking through 63 candidates of size 7
+-- looking through 154 candidates of size 8
+-- looking through 368 candidates of size 9
+-- looking through 902 candidates of size 10
+product xs  =  if null xs then 1 else head xs * product (tail xs)
+
+product :: [Int] -> Int
+-- testing 37 combinations of argument values
+-- looking through 2 candidates of size 1
+-- looking through 2 candidates of size 2
+-- looking through 3 candidates of size 3
+-- looking through 8 candidates of size 4
+product xs  =  foldr (*) 1 xs
+
