diff --git a/.gitignore b/.gitignore
--- a/.gitignore
+++ b/.gitignore
@@ -33,7 +33,9 @@
 eg/ints
 eg/list
 eg/tapps
+eg/spec
 bench/self
+bench/ill-hit
 proto/u-conjure
 test/expr
 test/conjurable
diff --git a/Makefile b/Makefile
--- a/Makefile
+++ b/Makefile
@@ -11,7 +11,9 @@
   eg/ints \
   eg/bools \
   eg/list \
+  eg/spec \
   eg/tapps \
+  bench/ill-hit \
   bench/self \
   proto/u-conjure
 
diff --git a/TODO.md b/TODO.md
--- a/TODO.md
+++ b/TODO.md
@@ -3,18 +3,6 @@
 
 A non-exhaustive list of things TO DO for Conjure.
 
-* report number of "hit" assignments, add ill example as a bench
-
-* 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
 
diff --git a/bench/ill-hit.hs b/bench/ill-hit.hs
new file mode 100644
--- /dev/null
+++ b/bench/ill-hit.hs
@@ -0,0 +1,55 @@
+-- ill-hit.hs: failing to hit a function completely
+--
+-- Based on an example sent by Colin Runciman
+--
+-- Even though sum' is defined for 6 values,
+-- Conjure only ever hits 4 of them.
+import Conjure
+
+sum' :: [Int] -> Int
+sum' []  =  0
+sum' [1]  =  1
+sum' [1,2]  =  3
+sum' [1,2,3]  =  6
+sum' [3,4,5]  =  12
+sum' [1,2,3,4]  =  10
+
+sumSpec :: [([Int],Int)]
+sumSpec  =  [ [] -= 0
+            , [1] -= 1
+            , [1,2] -= 3
+            , [1,2,3] -= 6
+            , [3,4,5] -= 12
+            , [1,2,3,4] -= 10
+            ]
+
+main :: IO ()
+main  =  do
+  -- the following does not hit all 6 defined values, only 4
+  conjure "sum" (sum' :: [Int] -> Int) primitives
+
+  -- the following forces 3 argument values, totaling 6
+  conjureWith as "sum" (sum' :: [Int] -> Int) primitives
+
+  -- the following conjures from a spec
+  conjure1 "sum" sumSpec primitives
+
+as :: Args
+as  =  args
+    {  forceTests = map (map val)
+                  [ [[1,2]]
+                  , [[3,4,5::Int]]
+                  , [[1,2,3,4]]
+                  ]
+    }
+
+primitives :: [Expr]
+primitives =
+  [ val (0 :: Int)
+  , val (1 :: Int)
+  , value "+" ((+) :: Int -> Int -> Int)
+  , value "*" ((*) :: Int -> Int -> Int)
+  , value "null" (null :: [Int] -> Bool)
+  , value "head" (head :: [Int] -> Int)
+  , value "tail" (tail :: [Int] -> [Int])
+  ]
diff --git a/bench/runtime/zero/bench/ill-hit.runtime b/bench/runtime/zero/bench/ill-hit.runtime
new file mode 100644
--- /dev/null
+++ b/bench/runtime/zero/bench/ill-hit.runtime
@@ -0,0 +1,1 @@
+2.26
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 @@
-1.16
+0.95
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 @@
-7.68
+7.78
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 @@
-7.75
+6.99
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 @@
-2.39
+1.83
diff --git a/bench/runtime/zero/eg/list.runtime b/bench/runtime/zero/eg/list.runtime
--- a/bench/runtime/zero/eg/list.runtime
+++ b/bench/runtime/zero/eg/list.runtime
@@ -1,1 +1,1 @@
-8.56
+10.71
diff --git a/bench/runtime/zero/eg/spec.runtime b/bench/runtime/zero/eg/spec.runtime
new file mode 100644
--- /dev/null
+++ b/bench/runtime/zero/eg/spec.runtime
@@ -0,0 +1,1 @@
+1.63
diff --git a/bench/runtime/zero/eg/tapps.runtime b/bench/runtime/zero/eg/tapps.runtime
--- a/bench/runtime/zero/eg/tapps.runtime
+++ b/bench/runtime/zero/eg/tapps.runtime
@@ -1,1 +1,1 @@
-1.20
+0.96
diff --git a/bench/runtime/zero/proto/u-conjure.runtime b/bench/runtime/zero/proto/u-conjure.runtime
--- a/bench/runtime/zero/proto/u-conjure.runtime
+++ b/bench/runtime/zero/proto/u-conjure.runtime
@@ -1,1 +1,1 @@
-0.11
+0.10
diff --git a/changelog.md b/changelog.md
new file mode 100644
--- /dev/null
+++ b/changelog.md
@@ -0,0 +1,34 @@
+Changelog for (Code) Conjure
+============================
+
+
+v0.2.4
+------
+
+* allow conjuring from specifications in addition to partial definitions
+  (`conjure1`, `conjure2`, `conjure3` and related functions)
+* improve examples
+* improve criteria for automatic primitive inclusion:
+	- only include `if :: ... -> Bool` if there are `Bool` primitives
+	- include `False` and `True` automatically only on Speculate's background
+* add code-optional candidate nubbing and debug functions
+
+
+v0.2.2
+------
+
+* by default, search for 60 argument combinations
+  among 100000 enumerated combinations
+
+
+v0.2.0
+------
+
+* search until 100% match is found and exit
+* other misc changes
+
+
+v0.1.2
+------
+
+For the changelog of earlier versions, check the git commit history.
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.2.2
+version:             0.2.4
 synopsis:            conjure Haskell functions out of partial definitions
 description:
   Conjure is a tool that produces Haskell functions out of partial definitions.
@@ -23,6 +23,7 @@
 
 extra-doc-files: README.md
                , TODO.md
+               , changelog.md
                , doc/conjure.svg
 extra-source-files: .gitignore
                   , .github/workflows/build.yml
@@ -64,13 +65,14 @@
 source-repository this
   type:            git
   location:        https://github.com/rudymatela/conjure
-  tag:             v0.2.2
+  tag:             v0.2.4
 
 library
   exposed-modules: Conjure
                  , Conjure.Conjurable
                  , Conjure.Engine
                  , Conjure.Expr
+                 , Conjure.Spec
                  , Conjure.Utils
   other-extensions: TemplateHaskell, CPP
   build-depends: base >= 4 && < 5
diff --git a/eg/bools.hs b/eg/bools.hs
--- a/eg/bools.hs
+++ b/eg/bools.hs
@@ -25,7 +25,9 @@
 
 primitives :: [Expr]
 primitives =
-  [ value "not" not
+  [ val False
+  , val True
+  , value "not" not
   , value "||" (||)
   , value "&&" (&&)
   , value "null" (null :: [Bool] -> Bool)
diff --git a/eg/list.hs b/eg/list.hs
--- a/eg/list.hs
+++ b/eg/list.hs
@@ -27,6 +27,11 @@
   | x <= y && y <= z  =  [x,y,z]
   | z <= y && y <= x  =  [z,y,x]
 
+(+++) :: [Int] -> [Int] -> [Int]
+[x]     +++ [y]      =  [x,y]
+[x,y]   +++ [z,w]    =  [x,y,z,w]
+[x,y,z] +++ [w,v,u]  =  [x,y,z,w,v,u]
+
 main :: IO ()
 main = do
   -- length xs  =  if null xs then 0 else 1 + length (tail xs)
@@ -61,7 +66,17 @@
     , value "null" (null :: [Int] -> Bool)
     ]
 
-  -- now through folds
+  -- xs ++ ys  =  if null xs then ys else head xs:(tail xs ++ ys)
+  --              1  2    3       4       5    6 7  8   9  10 11
+  conjure "++" (+++)
+    [ val ([] :: [Int])
+    , value ":" ((:) :: Int -> [Int] -> [Int])
+    , value "head" (head :: [Int] -> Int)
+    , value "tail" (tail :: [Int] -> [Int])
+    , value "null" (null :: [Int] -> Bool)
+    ]
+
+  -- now through fold
   -- length xs  =  foldr (const (1 +)) 0 xs
   conjure "length" length'
     [ val (0 :: Int)
@@ -71,7 +86,7 @@
     , value "const" (const :: (Int -> Int) -> Int -> (Int -> Int)) -- cheating?
     ]
 
-  -- now through folds and some cheating
+  -- now through fold and some cheating
   --  reverse xs  =  foldr (\x xs -> xs ++ [x]) [] xs
   --  reverse xs  =  foldr (flip (++) . unit) [] xs
   conjure "reverse" reverse'
@@ -84,10 +99,18 @@
     , value "." ((.) :: ([Int]->[Int]->[Int]) -> (Int->[Int]) -> Int -> [Int] -> [Int])
     ]
 
-  -- now through folds
+  -- now through fold
   -- 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])
+    ]
+
+  -- now through fold
+  -- xs ++ ys  =  foldr (:) ys xs
+  conjure "++" (+++)
+    [ val ([] :: [Int])
+    , value ":" ((:) :: Int -> [Int] -> [Int])
     , value "foldr" (foldr :: (Int -> [Int] -> [Int]) -> [Int] -> [Int] -> [Int])
     ]
diff --git a/eg/spec.hs b/eg/spec.hs
new file mode 100644
--- /dev/null
+++ b/eg/spec.hs
@@ -0,0 +1,50 @@
+-- spec.hs: conjuring a function from a specification
+--
+-- Adapted from Colin Runciman's example "ListFuns"
+import Conjure
+import Prelude hiding (sum)
+
+
+sumSpec :: Spec1 [Int] Int
+sumSpec  =
+  [ []      -= 0
+  , [1,2]   -= 3
+  , [3,4,5] -= 12
+  ]
+
+-- hoping for something like
+-- sum xs  =  if null xs then 0 else head xs + sum (tail xs)
+
+sumPrimitives :: [Expr]
+sumPrimitives  =
+  [ value "null" (null :: [Int] -> Bool)
+  , val (0::Int)
+  , value "+"    ((+) :: Int -> Int -> Int)
+  , value "head" (head :: [Int] -> Int)
+  , value "tail" (tail :: [Int] -> [Int])
+  ]
+
+
+appSpec :: Spec2 [Int] [Int] [Int]
+appSpec  =
+  [ (,) []      [0,1]   -= [0,1]
+  , (,) [2,3]   []      -= [2,3]
+  , (,) [4,5,6] [7,8,9] -= [4,5,6,7,8,9]
+  ]
+
+-- hoping for something like
+-- app xs ys = if null xs then ys else head xs : app (tail xs) ys
+
+appPrimitives :: [Expr]
+appPrimitives =
+  [ value "null" (null :: [Int] -> Bool)
+  , value ":"    ((:) :: Int -> [Int] -> [Int])
+  , value "head" (head :: [Int] -> Int)
+  , value "tail" (tail :: [Int] -> [Int])
+  ]
+
+
+main :: IO ()
+main = do
+  conjure1 "sum" sumSpec sumPrimitives
+  conjure2 "++"  appSpec appPrimitives
diff --git a/mk/depend.mk b/mk/depend.mk
--- a/mk/depend.mk
+++ b/mk/depend.mk
@@ -1,8 +1,20 @@
+bench/ill-hit: \
+  bench/ill-hit.hs \
+  mk/toplibs
+bench/ill-hit.o: \
+  src/Conjure/Utils.hs \
+  src/Conjure/Spec.hs \
+  src/Conjure.hs \
+  src/Conjure/Expr.hs \
+  src/Conjure/Engine.hs \
+  src/Conjure/Conjurable.hs \
+  bench/ill-hit.hs
 bench/self: \
   bench/self.hs \
   mk/toplibs
 bench/self.o: \
   src/Conjure/Utils.hs \
+  src/Conjure/Spec.hs \
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
@@ -13,6 +25,7 @@
   mk/toplibs
 eg/arith.o: \
   src/Conjure/Utils.hs \
+  src/Conjure/Spec.hs \
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
@@ -23,6 +36,7 @@
   mk/toplibs
 eg/bools.o: \
   src/Conjure/Utils.hs \
+  src/Conjure/Spec.hs \
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
@@ -33,6 +47,7 @@
   mk/toplibs
 eg/factorial.o: \
   src/Conjure/Utils.hs \
+  src/Conjure/Spec.hs \
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
@@ -43,6 +58,7 @@
   mk/toplibs
 eg/ints.o: \
   src/Conjure/Utils.hs \
+  src/Conjure/Spec.hs \
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
@@ -53,16 +69,29 @@
   mk/toplibs
 eg/list.o: \
   src/Conjure/Utils.hs \
+  src/Conjure/Spec.hs \
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
   src/Conjure/Conjurable.hs \
   eg/list.hs
+eg/spec: \
+  eg/spec.hs \
+  mk/toplibs
+eg/spec.o: \
+  src/Conjure/Utils.hs \
+  src/Conjure/Spec.hs \
+  src/Conjure.hs \
+  src/Conjure/Expr.hs \
+  src/Conjure/Engine.hs \
+  src/Conjure/Conjurable.hs \
+  eg/spec.hs
 eg/tapps: \
   eg/tapps.hs \
   mk/toplibs
 eg/tapps.o: \
   src/Conjure/Utils.hs \
+  src/Conjure/Spec.hs \
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
@@ -70,6 +99,7 @@
   eg/tapps.hs
 mk/All.o: \
   src/Conjure/Utils.hs \
+  src/Conjure/Spec.hs \
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
@@ -77,6 +107,7 @@
   mk/All.hs
 mk/Toplibs.o: \
   src/Conjure/Utils.hs \
+  src/Conjure/Spec.hs \
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
@@ -101,16 +132,24 @@
   src/Conjure/Expr.hs
 src/Conjure.o: \
   src/Conjure/Utils.hs \
+  src/Conjure/Spec.hs \
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
   src/Conjure/Conjurable.hs
+src/Conjure/Spec.o: \
+  src/Conjure/Utils.hs \
+  src/Conjure/Spec.hs \
+  src/Conjure/Expr.hs \
+  src/Conjure/Engine.hs \
+  src/Conjure/Conjurable.hs
 src/Conjure/Utils.o: \
   src/Conjure/Utils.hs
 test/conjurable.o: \
   test/Test.hs \
   test/conjurable.hs \
   src/Conjure/Utils.hs \
+  src/Conjure/Spec.hs \
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
@@ -123,6 +162,7 @@
   test/Test.hs \
   test/expr.hs \
   src/Conjure/Utils.hs \
+  src/Conjure/Spec.hs \
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
@@ -134,6 +174,7 @@
 test/Test.o: \
   test/Test.hs \
   src/Conjure/Utils.hs \
+  src/Conjure/Spec.hs \
   src/Conjure.hs \
   src/Conjure/Expr.hs \
   src/Conjure/Engine.hs \
diff --git a/src/Conjure.hs b/src/Conjure.hs
--- a/src/Conjure.hs
+++ b/src/Conjure.hs
@@ -53,6 +53,18 @@
   , Args(..)
   , args
 
+-- * Conjuring from a specification
+  , Spec1
+  , Spec2
+  , Spec3
+  , (-=)
+  , conjure1
+  , conjure2
+  , conjure3
+  , conjure1With
+  , conjure2With
+  , conjure3With
+
 -- * When using custom types
   , Conjurable (conjureEquality, conjureTiers)
   , reifyEquality, reifyTiers
@@ -64,4 +76,5 @@
 where
 
 import Conjure.Engine
+import Conjure.Spec
 import Conjure.Conjurable
diff --git a/src/Conjure/Conjurable.hs b/src/Conjure/Conjurable.hs
--- a/src/Conjure/Conjurable.hs
+++ b/src/Conjure/Conjurable.hs
@@ -17,17 +17,19 @@
   , conjureType
   , reifyTiers
   , reifyEquality
-  , canonicalApplication
-  , canonicalVarApplication
+  , conjureApplication
+  , conjureVarApplication
   , conjureHoles
   , conjureIfs
   , conjureTiersFor
+  , conjureAreEqual
   , conjureMkEquation
   )
 where
 
 import Test.LeanCheck
 import Test.LeanCheck.Utils
+import Test.LeanCheck.Error (errorToFalse)
 import Conjure.Expr hiding (application)
 import Test.Speculate.Expr
 import Data.Functor ((<$>))
@@ -109,17 +111,20 @@
   then ms
   else conjureSubTypes x $ conjureReification1 x : ms
 
+-- | like 'conjureType' but without type repetitions
+nubConjureType :: Conjurable a => a -> Reification
+nubConjureType x  =  nubOn (\(eh,_,_,_) -> eh) . conjureType x
+-- The use of nubOn above is O(n^2).
+-- So long as there is not a huge number of subtypes of a, so we're fine.
+
 conjureReification1 :: Conjurable a => a -> Reification1
 conjureReification1 x  =  (hole x, ifFor x, conjureEquality x, conjureTiers x)
 
 conjureReification :: Conjurable a => a -> [Reification1]
-conjureReification x  =  nubOn (\(eh,_,_,_) -> eh)
-                      $  conjureType x [conjureReification1 bool]
+conjureReification x  =  nubConjureType x [conjureReification1 bool]
   where
   bool :: Bool
   bool  =  error "conjureReification: evaluated proxy boolean value (definitely a bug)"
--- The use of nubOn above is O(n^2).
--- So long as there is not a huge number of subtypes of a, so we're fine.
 
 -- | Reifies equality to be used in a conjurable type.
 --
@@ -154,11 +159,21 @@
 conjureHoles f  =  [eh | (eh,_,_,Just _) <- conjureReification f]
 
 conjureIfs :: Conjurable f => f -> [Expr]
-conjureIfs f  =  [eef | (_,eef,_,Just _) <- conjureReification f]
+conjureIfs f  =  [eef | (_,eef,_,Just _) <- nubConjureType f []]
+-- this does not include if for bools automatically
+-- differently from conjureHoles, conjureMkEquation and conjureTiersFor
 
 conjureMkEquation :: Conjurable f => f -> Expr -> Expr -> Expr
 conjureMkEquation f  =  mkEquation [eq | (_,_,Just eq,_) <- conjureReification f]
 
+conjureAreEqual :: Conjurable f => f -> Int -> Expr -> Expr -> Bool
+conjureAreEqual f maxTests  =  (===)
+  where
+  (-==-)  =  conjureMkEquation f
+  e1 === e2  =  isTrue $ e1 -==- e2
+  isTrue  =  all (errorToFalse . eval False) . gs
+  gs  =  take maxTests . grounds (conjureTiersFor f)
+
 conjureTiersFor :: Conjurable f => f -> Expr -> [[Expr]]
 conjureTiersFor f e  =  tf allTiers
   where
@@ -284,9 +299,9 @@
       (Right _) == (Left _)   =  False
       (Right x) == (Right y)  =  x .== y
 
-instance (Listable a, Show a, Conjurable a, Conjurable b) => Conjurable (a -> b) where
+instance (Conjurable a, Conjurable b) => Conjurable (a -> b) where
   conjureArgumentHoles f  =  hole (argTy f) : conjureArgumentHoles (f undefined)
-  conjureSubTypes f  =   conjureType (argTy f) . conjureType (resTy f)
+  conjureSubTypes f  =  conjureType (argTy f) . conjureType (resTy f)
 
 argTy :: (a -> b) -> a
 argTy _  =  undefined
@@ -294,15 +309,15 @@
 resTy :: (a -> b) -> b
 resTy _  =  undefined
 
-canonicalApplication :: Conjurable f => String -> f -> Expr
-canonicalApplication  =  canonicalWhatApplication value
+conjureApplication :: Conjurable f => String -> f -> Expr
+conjureApplication  =  conjureWhatApplication value
 
-canonicalVarApplication :: Conjurable f => String -> f -> Expr
-canonicalVarApplication  =  canonicalWhatApplication var
+conjureVarApplication :: Conjurable f => String -> f -> Expr
+conjureVarApplication  =  conjureWhatApplication var
 
-canonicalWhatApplication :: Conjurable f => (String -> f -> Expr) -> String -> f -> Expr
-canonicalWhatApplication what nm f  =  mostGeneralCanonicalVariation . foldApp
-                                    $  what nf f : zipWith varAsTypeOf nas (conjureArgumentHoles f)
+conjureWhatApplication :: Conjurable f => (String -> f -> Expr) -> String -> f -> Expr
+conjureWhatApplication what nm f  =  mostGeneralCanonicalVariation . foldApp
+                                  $  what nf f : zipWith varAsTypeOf nas (conjureArgumentHoles f)
   where
   (nf:nas)  =  words nm ++ repeat ""
 
diff --git a/src/Conjure/Engine.hs b/src/Conjure/Engine.hs
--- a/src/Conjure/Engine.hs
+++ b/src/Conjure/Engine.hs
@@ -29,6 +29,7 @@
 import Data.Express.Fixtures hiding ((-==-))
 import qualified Data.Ratio
 import Test.LeanCheck.Error (errorToTrue, errorToFalse, errorToNothing)
+import Test.LeanCheck.Tiers
 import Test.Speculate hiding ((===), Args(..), args)
 import Test.Speculate.Reason
 import Test.Speculate.Engine
@@ -47,6 +48,7 @@
   , maxEquationSize   :: Int  -- ^ maximum size of equation operands
   , maxRecursionSize  :: Int  -- ^ maximum size of a recursive expression expansion
   , maxSearchTests    :: Int  -- ^ maximum number of tests to search for defined values
+  , forceTests :: [[Expr]]  -- ^ force tests
   }
 
 -- | Default arguments to conjure.
@@ -65,6 +67,7 @@
   , maxEquationSize    =   5
   , maxRecursionSize   =  60
   , maxSearchTests     =  100000
+  , forceTests         =  []
   }
 
 -- | Like 'conjure' but in the pure world.
@@ -72,39 +75,39 @@
 -- Returns a triple with:
 --
 -- 1. tiers of implementations
--- 2. tiers of candidate bodies
--- 3. a list of tests
-conjpure :: Conjurable f => String -> f -> [Expr] -> ([[Expr]], [[Expr]], [Expr])
+-- 2. tiers of candidate bodies (right type)
+-- 3. tiers of candidate expressions (any type)
+-- 4. a list of tests
+conjpure :: Conjurable f => String -> f -> [Expr] -> ([[Expr]], [[Expr]], [[Expr]], [Expr])
 conjpure =  conjpureWith args
 
 -- | Like 'conjpure' but allows setting options through 'Args' and 'args'.
-conjpureWith :: Conjurable f => Args -> String -> f -> [Expr] -> ([[Expr]], [[Expr]], [Expr])
-conjpureWith Args{..} nm f es  =  (implementationsT, candidatesT, tests)
+conjpureWith :: Conjurable f => Args -> String -> f -> [Expr] -> ([[Expr]], [[Expr]], [[Expr]], [Expr])
+conjpureWith Args{..} nm f es  =  (implementationsT, candidatesT, allCandidatesT, tests)
   where
   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
+  candidatesT  =  filterT (\e -> typ e == typ ffxx) allCandidatesT
+  allCandidatesT  =  take maxSize
+                  $  candidateExprs nm f maxEquationSize maxRecursiveCalls (===) es
+  ffxx   =  conjureApplication nm f
+  vffxx  =  conjureVarApplication nm f
+  (rrff:xxs)  =  unfoldApp vffxx
 
-  e1 === e2  =  isReallyTrue (e1 -==- e2)
+  (===)  =  conjureAreEqual f maxTests
   e1 ?=? e2  =  isTrueWhenDefined (e1 -==- e2)
   (-==-)  =  conjureMkEquation f
 
   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 maxSearchTests $ groundBinds (conjureTiersFor f) ffxx
-  dbss  =  take maxTests [bs | bs <- bss, errorToFalse . eval False $ e //- bs]
+  fbss  =  [zip xxs vs | vs <- forceTests, isWellTyped $ foldApp (rrff:vs)]
+  dbss  =  take maxTests
+        $  ([bs | bs <- bss, errorToFalse . eval False $ e //- bs] \\ fbss)
+        ++ fbss
     where
     e  =  ffxx -==- ffxx
 
@@ -153,6 +156,8 @@
                        ,  maxEquationSize = min sz (maxEquationSize args)
                        }
 
+
+
 -- | Like 'conjure' but allows setting options through 'Args'/'args'.
 --
 -- > conjureWith args{maxSize = 11} "function" function [...]
@@ -163,14 +168,16 @@
   pr 1 rs
   where
   pr n []  =  putStrLn $ "cannot conjure"
-  pr n ((is,es):rs)  =  do
-    putStrLn $ "-- looking through " ++ show (length es) ++ " candidates of size " ++ show n
+  pr n ((is,cs,es):rs)  =  do
+    putStrLn $ "-- looking through "
+            ++ show (length cs) ++ "/" ++ 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
+  rs  =  zip3 iss css ess
+  (iss, css, ess, ts)  =  conjpureWith args nm f es
   showEq eq  =  showExpr (lhs eq) ++ "  =  " ++ showExpr (rhs eq)
 
 candidateExprs :: Conjurable f
@@ -181,8 +188,7 @@
                -> [Expr]
                -> [[Expr]]
 candidateExprs nm f sz mc (===) es  =
-  candidateExprsT nm f sz mc (===)
-    [nub $ [val False, val True] ++ es ++ conjureIfs f]
+  candidateExprsT nm f sz mc (===) [nub $ es ++ conjureIfs f]
 
 candidateExprsT :: Conjurable f
                 => String -> f
@@ -193,9 +199,13 @@
                 -> [[Expr]]
 candidateExprsT nm f sz mc (===) ess  =  expressionsT $ [ef:exs] \/ ess
   where
-  (ef:exs)  =  unfoldApp $ canonicalVarApplication nm f
-  thy  =  theoryFromAtoms (===) sz $ [conjureHoles f] \/ ess
-  expressionsT ds  =  filterT (\e -> count (== ef) (vars e) <= mc)
+  (ef:exs)  =  unfoldApp $ conjureVarApplication nm f
+  falseAndTrue  =  [val False, val True]
+  thy  =  theoryFromAtoms (===) sz $ [conjureHoles f ++ falseAndTrue] \/ filterT (`notElem` falseAndTrue) ess
+  nubET  =  id -- no nub, good enough results
+  -- nubET  =  discardLaterT (===) -- huge computational cost
+  expressionsT ds  =  nubET
+                   $  filterT (\e -> count (== ef) (vars e) <= mc)
                    $  filterT (isRootNormalE thy)
                    $  ds \/ (delay $ productMaybeWith ($$) es es)
     where
@@ -211,3 +221,20 @@
 
 (%) :: Int -> Int -> Int
 x % y  =  x * 100 `div` y
+
+-- Debug: application that always works
+(*$$*) :: Expr -> Expr -> Maybe Expr
+e1 *$$* e2  =  Just $ e1 :$ e2
+
+-- Debug: application that works for the correct kinds
+(>$$<) :: Expr -> Expr -> Maybe Expr
+e1 >$$< e2  =  if isFunTy t1 && tyArity (argumentTy t1) == tyArity t2
+               then Just $ e1 :$ e2
+               else Nothing
+  where
+  t1  =  ktyp e1
+  t2  =  ktyp e2
+
+ktyp :: Expr -> TypeRep
+ktyp (e1 :$ e2)  =  resultTy (ktyp e1)
+ktyp e  =  typ e
diff --git a/src/Conjure/Spec.hs b/src/Conjure/Spec.hs
new file mode 100644
--- /dev/null
+++ b/src/Conjure/Spec.hs
@@ -0,0 +1,190 @@
+-- |
+-- Module      : Conjure.Spec
+-- Copyright   : (c) 2021 Rudy Matela
+-- License     : 3-Clause BSD  (see the file LICENSE)
+-- Maintainer  : Rudy Matela <rudy@matela.com.br>
+--
+-- An internal module of 'Conjure',
+-- a library for Conjuring function implementations
+-- from tests or partial definitions.
+-- (a.k.a.: functional inductive programming)
+module Conjure.Spec
+  ( Spec1
+  , Spec2
+  , Spec3
+  , (-=)
+  , conjure1
+  , conjure2
+  , conjure3
+  , conjure1With
+  , conjure2With
+  , conjure3With
+  )
+where
+
+import Conjure.Engine
+import Conjure.Conjurable
+import Conjure.Utils
+
+
+-- | A partial specification of a function with one argument:
+--
+-- > sumSpec :: Spec1 [Int] Int
+-- > sumSpec  =
+-- >   [ []      -= 0
+-- >   , [1,2]   -= 3
+-- >   , [3,4,5] -= 12
+-- >   ]
+--
+-- To be passed as one of the arguments to 'conjure1'.
+type Spec1 a b     = [(a,b)]
+
+
+-- | A partial specification of a function with two arguments:
+--
+-- > appSpec :: Spec2 [Int] [Int] [Int]
+-- > appSpec  =
+-- >   [ (,) []      [0,1]   -= [0,1]
+-- >   , (,) [2,3]   []      -= [2,3]
+-- >   , (,) [4,5,6] [7,8,9] -= [4,5,6,7,8,9]
+-- >   ]
+--
+-- To be passed as one of the arguments to 'conjure2'.
+type Spec2 a b c   = [((a,b),c)]
+
+
+-- | A partial specification of a function with three arguments.
+--
+-- To be passed as one of the arguments to 'conjure3'
+type Spec3 a b c d = [((a,b,c),d)]
+
+
+-- | To be used when constructing specifications:
+--   'Spec1',
+--   'Spec2' and
+--   'Spec3'.
+(-=) :: a -> b -> (a,b)
+(-=)  =  (,)
+
+
+-- | Conjures a one argument function from a specification.
+--
+-- Given:
+--
+-- > sumSpec :: Spec1 [Int] Int
+-- > sumSpec  =
+-- >   [ []      -= 0
+-- >   , [1,2]   -= 3
+-- >   , [3,4,5] -= 12
+-- >   ]
+--
+-- > sumPrimitives :: [Expr]
+-- > sumPrimitives  =
+-- >   [ value "null" (null :: [Int] -> Bool)
+-- >   , val (0::Int)
+-- >   , value "+"    ((+) :: Int -> Int -> Int)
+-- >   , value "head" (head :: [Int] -> Int)
+-- >   , value "tail" (tail :: [Int] -> [Int])
+-- >   ]
+--
+-- Then:
+--
+-- > > conjure1 "sum" sumSpec sumPrimitives
+-- > sum :: [Int] -> Int
+-- > -- testing 3 combinations of argument values
+-- > -- ...
+-- > -- looking through 189/465 candidates of size 10
+-- > xs ++ ys  =  if null xs then ys else head xs:(tail xs ++ ys)
+--
+-- (cf. 'Spec1', 'conjure1With')
+conjure1 :: (Eq a, Show a, Conjurable a, Conjurable b)
+         => String -> Spec1 a b -> [Expr] -> IO ()
+conjure1  =  conjure1With args
+
+
+-- | Conjures a two argument function from a specification.
+--
+-- Given:
+--
+-- > appSpec :: Spec2 [Int] [Int] [Int]
+-- > appSpec  =
+-- >   [ (,) []      [0,1]   -= [0,1]
+-- >   , (,) [2,3]   []      -= [2,3]
+-- >   , (,) [4,5,6] [7,8,9] -= [4,5,6,7,8,9]
+-- >   ]
+--
+-- > appPrimitives :: [Expr]
+-- > appPrimitives =
+-- >   [ value "null" (null :: [Int] -> Bool)
+-- >   , value ":"    ((:) :: Int -> [Int] -> [Int])
+-- >   , value "head" (head :: [Int] -> Int)
+-- >   , value "tail" (tail :: [Int] -> [Int])
+-- >   ]
+--
+-- Then:
+--
+-- > > conjure2 "++" appSpec appPrimitives
+-- > (++) :: [Int] -> [Int] -> [Int]
+-- > -- testing 3 combinations of argument values
+-- > -- ...
+-- > -- looking through 26166/57090 candidates of size 11
+-- > xs ++ ys  =  if null xs then ys else head xs:(tail xs ++ ys)
+--
+-- (cf. 'Spec2', 'conjure2With')
+conjure2 :: ( Conjurable a, Eq a, Show a
+            , Conjurable b, Eq b, Show b
+            , Conjurable c
+            ) => String -> Spec2 a b c -> [Expr] -> IO ()
+conjure2  =  conjure2With args
+
+
+-- | Conjures a three argument function from a specification.
+--
+-- (cf. 'Spec3', 'conjure3With')
+conjure3 :: ( Conjurable a, Eq a, Show a
+            , Conjurable b, Eq b, Show b
+            , Conjurable c, Eq c, Show c
+            , Conjurable d
+            ) => String -> Spec3 a b c d -> [Expr] -> IO ()
+conjure3  =  conjure3With args
+
+
+-- | Like 'conjure1' but allows setting options through 'Args'/'args'.
+conjure1With :: (Eq a, Show a, Conjurable a, Conjurable b)
+             => Args -> String -> Spec1 a b -> [Expr] -> IO ()
+conjure1With args nm bs  =  conjureWith args{forceTests=ts} nm (mkFun1 bs)
+  where
+  ts = [[val x] | (x,_) <- bs]
+
+
+-- | Like 'conjure2' but allows setting options through 'Args'/'args'.
+conjure2With :: ( Conjurable a, Eq a, Show a
+                , Conjurable b, Eq b, Show b
+                , Conjurable c
+                ) => Args -> String -> Spec2 a b c -> [Expr] -> IO ()
+conjure2With args nm bs  =  conjureWith args{forceTests=ts} nm (mkFun2 bs)
+  where
+  ts = [[val x, val y] | ((x,y),_) <- bs]
+
+
+-- | Like 'conjure3' but allows setting options through 'Args'/'args'.
+conjure3With :: ( Conjurable a, Eq a, Show a
+                , Conjurable b, Eq b, Show b
+                , Conjurable c, Eq c, Show c
+                , Conjurable d
+                ) => Args -> String -> Spec3 a b c d -> [Expr] -> IO ()
+conjure3With args nm bs  =  conjureWith args{forceTests=ts} nm (mkFun3 bs)
+  where
+  ts = [[val x, val y, val z] | ((x,y,z),_) <- bs]
+
+
+mkFun1 :: Eq a => [(a,b)] -> a -> b
+mkFun1 bs  =  \x -> fromMaybe undefined $ lookup x bs
+
+
+mkFun2 :: (Eq a, Eq b) => [((a,b),c)] -> a -> b -> c
+mkFun2 bs  =  \x y -> fromMaybe undefined $ lookup (x,y) bs
+
+
+mkFun3 :: (Eq a, Eq b, Eq c) => [((a,b,c),d)] -> a -> b -> c -> d
+mkFun3 bs  =  \x y z -> fromMaybe undefined $ lookup (x,y,z) bs
diff --git a/test/conjurable.hs b/test/conjurable.hs
--- a/test/conjurable.hs
+++ b/test/conjurable.hs
@@ -21,12 +21,12 @@
 tests n  =
   [ True
 
-  , canonicalApplication "not"   not  ==  not' pp
-  , canonicalApplication "not q" not  ==  not' qq
-  , canonicalApplication "negate"   (negate :: Int -> Int)  ==  negate' xx
-  , canonicalApplication "negate i" (negate :: Int -> Int)  ==  negate' ii
-  , canonicalApplication "+"     ((+) :: Int -> Int -> Int)  ==  xx -+- yy
-  , canonicalApplication "+ i j" ((+) :: Int -> Int -> Int)  ==  ii -+- jj
+  , conjureApplication "not"   not  ==  not' pp
+  , conjureApplication "not q" not  ==  not' qq
+  , conjureApplication "negate"   (negate :: Int -> Int)  ==  negate' xx
+  , conjureApplication "negate i" (negate :: Int -> Int)  ==  negate' ii
+  , conjureApplication "+"     ((+) :: Int -> Int -> Int)  ==  xx -+- yy
+  , conjureApplication "+ i j" ((+) :: Int -> Int -> Int)  ==  ii -+- jj
 
   , holds n $ \x y -> (x <==> y)  ==  (x == (y :: ()))
   , holds n $ \x y -> (x <==> y)  ==  (x == (y :: Int))
diff --git a/test/model/bench/ill-hit.out b/test/model/bench/ill-hit.out
new file mode 100644
--- /dev/null
+++ b/test/model/bench/ill-hit.out
@@ -0,0 +1,42 @@
+sum :: [Int] -> Int
+-- testing 4 combinations of argument values
+-- looking through 2/11 candidates of size 1
+-- looking through 2/8 candidates of size 2
+-- looking through 3/11 candidates of size 3
+-- looking through 5/18 candidates of size 4
+-- looking through 13/33 candidates of size 5
+-- looking through 26/68 candidates of size 6
+-- looking through 63/143 candidates of size 7
+-- looking through 152/336 candidates of size 8
+-- looking through 358/783 candidates of size 9
+-- looking through 860/1835 candidates of size 10
+sum xs  =  if null xs then 0 else head xs + sum (tail xs)
+
+sum :: [Int] -> Int
+-- testing 6 combinations of argument values
+-- looking through 2/11 candidates of size 1
+-- looking through 2/8 candidates of size 2
+-- looking through 3/11 candidates of size 3
+-- looking through 5/18 candidates of size 4
+-- looking through 13/33 candidates of size 5
+-- looking through 26/68 candidates of size 6
+-- looking through 63/143 candidates of size 7
+-- looking through 152/336 candidates of size 8
+-- looking through 358/783 candidates of size 9
+-- looking through 860/1835 candidates of size 10
+sum xs  =  if null xs then 0 else head xs + sum (tail xs)
+
+sum :: [Int] -> Int
+-- testing 6 combinations of argument values
+-- looking through 2/11 candidates of size 1
+-- looking through 2/8 candidates of size 2
+-- looking through 3/11 candidates of size 3
+-- looking through 5/18 candidates of size 4
+-- looking through 13/33 candidates of size 5
+-- looking through 26/68 candidates of size 6
+-- looking through 63/143 candidates of size 7
+-- looking through 152/336 candidates of size 8
+-- looking through 358/783 candidates of size 9
+-- looking through 860/1835 candidates of size 10
+sum xs  =  if null xs then 0 else head xs + sum (tail xs)
+
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,27 +1,27 @@
 (?) :: Int -> Int -> Int
 -- 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
+-- looking through 4/8 candidates of size 1
+-- looking through 0/12 candidates of size 2
+-- looking through 48/48 candidates of size 3
 x ? y  =  x + y
 
 (?) :: Int -> Int -> Int
 -- 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
+-- looking through 4/8 candidates of size 1
+-- looking through 0/12 candidates of size 2
+-- looking through 48/48 candidates of size 3
 x ? y  =  x * y
 
 i :: Int -> Int
 -- 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
+-- looking through 3/7 candidates of size 1
+-- looking through 3/9 candidates of size 2
+-- looking through 18/24 candidates of size 3
 i x  =  x + 1
 
 d :: Int -> Int
 -- 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
+-- looking through 3/7 candidates of size 1
+-- looking through 3/9 candidates of size 2
+-- looking through 18/24 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,32 +1,32 @@
 double :: Int -> Int
 -- 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
+-- looking through 3/7 candidates of size 1
+-- looking through 3/9 candidates of size 2
+-- looking through 5/11 candidates of size 3
 double x  =  x + x
 
 add :: Int -> Int -> Int
 -- 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
+-- looking through 4/8 candidates of size 1
+-- looking through 0/12 candidates of size 2
+-- looking through 29/29 candidates of size 3
 add x y  =  x + y
 
 square :: Int -> Int
 -- 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 3/7 candidates of size 1
+-- looking through 3/9 candidates of size 2
+-- looking through 5/11 candidates of size 3
 square x  =  x * x
 
 tnpo :: Int -> Int
 -- 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
+-- looking through 3/7 candidates of size 1
+-- looking through 3/9 candidates of size 2
+-- looking through 5/11 candidates of size 3
+-- looking through 20/30 candidates of size 4
+-- looking through 13/53 candidates of size 5
+-- looking through 97/123 candidates of size 6
+-- looking through 42/236 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,44 +1,44 @@
 and :: [Bool] -> Bool
 -- 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 2/12 candidates of size 1
+-- looking through 3/12 candidates of size 2
+-- looking through 6/25 candidates of size 3
+-- looking through 6/48 candidates of size 4
+-- looking through 16/84 candidates of size 5
+-- looking through 41/185 candidates of size 6
+-- looking through 103/447 candidates of size 7
+-- looking through 278/1123 candidates of size 8
+-- looking through 752/2982 candidates of size 9
 and ps  =  null ps || head ps && and (tail ps)
 
 or :: [Bool] -> Bool
 -- 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
+-- looking through 2/12 candidates of size 1
+-- looking through 3/12 candidates of size 2
+-- looking through 6/25 candidates of size 3
+-- looking through 6/48 candidates of size 4
+-- looking through 16/84 candidates of size 5
+-- looking through 41/185 candidates of size 6
+-- looking through 103/447 candidates of size 7
+-- looking through 278/1123 candidates of size 8
+-- looking through 752/2982 candidates of size 9
+-- looking through 1963/7993 candidates of size 10
+-- looking through 5427/21497 candidates of size 11
 or ps  =  not (null ps || not (head ps || or (tail ps)))
 
 and :: [Bool] -> Bool
 -- 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
+-- looking through 2/13 candidates of size 1
+-- looking through 3/14 candidates of size 2
+-- looking through 6/31 candidates of size 3
+-- looking through 8/63 candidates of size 4
 and ps  =  foldr (&&) True ps
 
 or :: [Bool] -> Bool
 -- 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
+-- looking through 2/13 candidates of size 1
+-- looking through 3/14 candidates of size 2
+-- looking through 6/31 candidates of size 3
+-- looking through 8/63 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,22 +1,22 @@
 factorial :: Int -> Int
 -- 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
+-- looking through 2/6 candidates of size 1
+-- looking through 2/4 candidates of size 2
+-- looking through 0/6 candidates of size 3
+-- looking through 2/10 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
+-- looking through 3/9 candidates of size 1
+-- looking through 5/14 candidates of size 2
+-- looking through 8/26 candidates of size 3
+-- looking through 26/66 candidates of size 4
+-- looking through 59/180 candidates of size 5
+-- looking through 167/505 candidates of size 6
+-- looking through 581/1521 candidates of size 7
+-- looking through 1654/4809 candidates of size 8
+-- looking through 5736/15120 candidates of size 9
+-- looking through 17617/48943 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,59 +1,59 @@
 second :: [Int] -> Int
 -- testing 60 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 2/11 candidates of size 1
+-- looking through 2/8 candidates of size 2
+-- looking through 3/11 candidates of size 3
 second xs  =  head (tail xs)
 
 third :: [Int] -> Int
 -- testing 60 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 2/11 candidates of size 1
+-- looking through 2/8 candidates of size 2
+-- looking through 3/11 candidates of size 3
+-- looking through 5/18 candidates of size 4
 third xs  =  head (tail (tail xs))
 
 sum :: [Int] -> Int
 -- testing 60 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
+-- looking through 2/11 candidates of size 1
+-- looking through 2/8 candidates of size 2
+-- looking through 3/11 candidates of size 3
+-- looking through 5/18 candidates of size 4
+-- looking through 13/33 candidates of size 5
+-- looking through 26/68 candidates of size 6
+-- looking through 63/143 candidates of size 7
+-- looking through 152/336 candidates of size 8
+-- looking through 358/783 candidates of size 9
+-- looking through 860/1835 candidates of size 10
 sum xs  =  if null xs then 0 else head xs + sum (tail xs)
 
 product :: [Int] -> Int
 -- testing 60 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
+-- looking through 2/11 candidates of size 1
+-- looking through 2/8 candidates of size 2
+-- looking through 3/11 candidates of size 3
+-- looking through 5/18 candidates of size 4
+-- looking through 13/33 candidates of size 5
+-- looking through 26/68 candidates of size 6
+-- looking through 63/143 candidates of size 7
+-- looking through 152/336 candidates of size 8
+-- looking through 358/783 candidates of size 9
+-- looking through 860/1835 candidates of size 10
 product xs  =  if null xs then 1 else head xs * product (tail xs)
 
 sum :: [Int] -> Int
 -- testing 60 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
+-- looking through 2/12 candidates of size 1
+-- looking through 2/10 candidates of size 2
+-- looking through 3/15 candidates of size 3
+-- looking through 8/26 candidates of size 4
 sum xs  =  foldr (+) 0 xs
 
 product :: [Int] -> Int
 -- testing 60 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
+-- looking through 2/12 candidates of size 1
+-- looking through 2/10 candidates of size 2
+-- looking through 3/15 candidates of size 3
+-- looking through 8/26 candidates of size 4
 product xs  =  foldr (*) 1 xs
 
diff --git a/test/model/eg/list.out b/test/model/eg/list.out
--- a/test/model/eg/list.out
+++ b/test/model/eg/list.out
@@ -1,71 +1,94 @@
 length :: [Int] -> Int
 -- testing 60 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
+-- looking through 2/9 candidates of size 1
+-- looking through 1/5 candidates of size 2
+-- looking through 2/7 candidates of size 3
+-- looking through 3/12 candidates of size 4
+-- looking through 5/17 candidates of size 5
+-- looking through 11/30 candidates of size 6
+-- looking through 22/57 candidates of size 7
+-- looking through 51/119 candidates of size 8
+-- looking through 95/240 candidates of size 9
 length xs  =  if null xs then 0 else 1 + length (tail xs)
 
 reverse :: [Int] -> [Int]
 -- testing 60 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
+-- looking through 2/10 candidates of size 1
+-- looking through 4/9 candidates of size 2
+-- looking through 9/23 candidates of size 3
+-- looking through 24/56 candidates of size 4
+-- looking through 65/153 candidates of size 5
+-- looking through 215/466 candidates of size 6
+-- looking through 673/1462 candidates of size 7
+-- looking through 2176/4680 candidates of size 8
+-- looking through 7126/15229 candidates of size 9
+-- looking through 23619/50202 candidates of size 10
+-- looking through 79162/167174 candidates of size 11
 reverse xs  =  if null xs then xs else reverse (tail xs) ++ unit (head xs)
 
 sort :: [Int] -> [Int]
 -- testing 60 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
+-- looking through 2/9 candidates of size 1
+-- looking through 4/7 candidates of size 2
+-- looking through 6/18 candidates of size 3
+-- looking through 12/38 candidates of size 4
+-- looking through 31/81 candidates of size 5
+-- looking through 98/207 candidates of size 6
+-- looking through 287/576 candidates of size 7
+-- looking through 790/1661 candidates of size 8
+-- looking through 2192/4759 candidates of size 9
+-- looking through 6352/13661 candidates of size 10
 sort xs  =  if null xs then xs else insert (head xs) (sort (tail xs))
 
+(++) :: [Int] -> [Int] -> [Int]
+-- testing 60 combinations of argument values
+-- looking through 3/10 candidates of size 1
+-- looking through 3/11 candidates of size 2
+-- looking through 12/28 candidates of size 3
+-- looking through 39/81 candidates of size 4
+-- looking through 83/212 candidates of size 5
+-- looking through 290/623 candidates of size 6
+-- looking through 1013/2039 candidates of size 7
+-- looking through 3482/6732 candidates of size 8
+-- looking through 11207/22507 candidates of size 9
+-- looking through 36383/74650 candidates of size 10
+-- looking through 124785/250463 candidates of size 11
+xs ++ ys  =  if null xs then ys else head xs:(tail xs ++ ys)
+
 length :: [Int] -> Int
 -- testing 60 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
+-- looking through 2/9 candidates of size 1
+-- looking through 1/4 candidates of size 2
+-- looking through 1/6 candidates of size 3
+-- looking through 4/13 candidates of size 4
+-- looking through 2/21 candidates of size 5
+-- looking through 10/45 candidates of size 6
 length xs  =  foldr (const (1 +)) 0 xs
 
 reverse :: [Int] -> [Int]
 -- testing 60 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
+-- looking through 2/10 candidates of size 1
+-- looking through 2/6 candidates of size 2
+-- looking through 1/8 candidates of size 3
+-- looking through 5/14 candidates of size 4
+-- looking through 1/19 candidates of size 5
+-- looking through 17/43 candidates of size 6
+-- looking through 37/89 candidates of size 7
 reverse xs  =  foldr (flip (++) . unit) [] xs
 
 sort :: [Int] -> [Int]
 -- testing 60 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
+-- looking through 2/7 candidates of size 1
+-- looking through 2/3 candidates of size 2
+-- looking through 0/2 candidates of size 3
+-- looking through 2/4 candidates of size 4
 sort xs  =  foldr insert [] xs
+
+(++) :: [Int] -> [Int] -> [Int]
+-- testing 60 combinations of argument values
+-- looking through 3/8 candidates of size 1
+-- looking through 0/4 candidates of size 2
+-- looking through 9/12 candidates of size 3
+-- looking through 4/4 candidates of size 4
+xs ++ ys  =  foldr (:) ys xs
 
diff --git a/test/model/eg/spec.out b/test/model/eg/spec.out
new file mode 100644
--- /dev/null
+++ b/test/model/eg/spec.out
@@ -0,0 +1,29 @@
+sum :: [Int] -> Int
+-- testing 3 combinations of argument values
+-- looking through 1/9 candidates of size 1
+-- looking through 2/5 candidates of size 2
+-- looking through 2/8 candidates of size 3
+-- looking through 2/10 candidates of size 4
+-- looking through 5/16 candidates of size 5
+-- looking through 10/29 candidates of size 6
+-- looking through 23/56 candidates of size 7
+-- looking through 46/114 candidates of size 8
+-- looking through 92/228 candidates of size 9
+-- looking through 189/465 candidates of size 10
+sum xs  =  if null xs then 0 else head xs + sum (tail xs)
+
+(++) :: [Int] -> [Int] -> [Int]
+-- testing 3 combinations of argument values
+-- looking through 2/9 candidates of size 1
+-- looking through 2/8 candidates of size 2
+-- looking through 6/18 candidates of size 3
+-- looking through 18/42 candidates of size 4
+-- looking through 38/102 candidates of size 5
+-- looking through 110/262 candidates of size 6
+-- looking through 334/746 candidates of size 7
+-- looking through 1018/2170 candidates of size 8
+-- looking through 2966/6442 candidates of size 9
+-- looking through 8662/19142 candidates of size 10
+-- looking through 26166/57090 candidates of size 11
+xs ++ ys  =  if null xs then ys else head xs:(tail xs ++ ys)
+
diff --git a/test/model/eg/tapps.out b/test/model/eg/tapps.out
--- a/test/model/eg/tapps.out
+++ b/test/model/eg/tapps.out
@@ -1,30 +1,30 @@
 third :: [Int] -> Int
 -- testing 60 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 2/11 candidates of size 1
+-- looking through 2/8 candidates of size 2
+-- looking through 3/11 candidates of size 3
+-- looking through 5/18 candidates of size 4
 third xs  =  head (tail (tail xs))
 
 product :: [Int] -> Int
 -- testing 60 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
+-- looking through 2/11 candidates of size 1
+-- looking through 2/8 candidates of size 2
+-- looking through 3/11 candidates of size 3
+-- looking through 5/18 candidates of size 4
+-- looking through 13/33 candidates of size 5
+-- looking through 26/68 candidates of size 6
+-- looking through 63/143 candidates of size 7
+-- looking through 152/336 candidates of size 8
+-- looking through 358/783 candidates of size 9
+-- looking through 860/1835 candidates of size 10
 product xs  =  if null xs then 1 else head xs * product (tail xs)
 
 product :: [Int] -> Int
 -- testing 60 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
+-- looking through 2/12 candidates of size 1
+-- looking through 2/10 candidates of size 2
+-- looking through 3/15 candidates of size 3
+-- looking through 8/26 candidates of size 4
 product xs  =  foldr (*) 1 xs