diff --git a/speculate.cabal b/speculate.cabal
--- a/speculate.cabal
+++ b/speculate.cabal
@@ -1,5 +1,5 @@
 name:                speculate
-version:             0.2.2
+version:             0.2.3
 synopsis:            discovery of properties about Haskell functions
 description:
   Speculate automatically discovers laws about Haskell functions.
@@ -31,7 +31,7 @@
 source-repository this
   type:            git
   location:        https://github.com/rudymatela/speculate
-  tag:             v0.2.2
+  tag:             v0.2.3
 
 
 library
@@ -46,6 +46,7 @@
                  , Test.Speculate.Expr.Ground
                  , Test.Speculate.Expr.Match
                  , Test.Speculate.Expr.TypeInfo
+                 , Test.Speculate.Pretty
                  , Test.Speculate.Reason
                  , Test.Speculate.Reason.Order
                  , Test.Speculate.SemiReason
diff --git a/src/Test/Speculate/Args.hs b/src/Test/Speculate/Args.hs
--- a/src/Test/Speculate/Args.hs
+++ b/src/Test/Speculate/Args.hs
@@ -55,6 +55,7 @@
                                --   maximum number of tests
   , maxConstants :: Maybe Int  -- ^ __(intermediary)__ maximum nubmer of constants allowed when considering expressions
   , maxDepth     :: Maybe Int  -- ^ __(intermediary)__ maximum depth of considered expressions
+  , showCounts   :: Bool       -- ^ __(intermediary)__ show counts of equations, inequalities and conditional equations
   , showTheory   :: Bool       -- ^ __(debug)__ whether to show raw theory
   , showArgs     :: Bool       -- ^ __(debug)__ show _this_ args before running
   , showHelp     :: Bool       -- ^ __(advanced)__ whether to show the command line help
@@ -92,6 +93,7 @@
   , showSemiequations    = True
   , showConditions       = True
   , showConstantLaws     = False
+  , showCounts           = False
   , showDot              = False
   , quietDot             = False
   , showClassesFor       = []
@@ -243,6 +245,7 @@
   , "cmax-constants"     --= \s a -> a {maxConstants = Just $ read s}
   , "eeval-timeout"      --= \s a -> a {evalTimeout = Just $ read s}
   , "ddepth"             --= \s a -> a {maxDepth = Just $ read s}
+  , " counts"            --.   \a -> a {showCounts = True}
   , "gsemi-digraph"      --.   \a -> a {showDot = True
                                        ,quietDot = False
                                        ,showConstants = False
@@ -264,12 +267,11 @@
   , "aall-foreground"    --.   \a -> a {constants = discard (== background) (constants a)}
   ]
   where
-  (short:long) --= fun = flagReq  [[short],long] ((Right .) . fun) "X" ""
-  (short:long) --. fun = flagNone [[short],long] fun                   ""
+  (short:long) --= fun = flagReq  (filter (/= " ") [[short],long]) ((Right .) . fun) "X" ""
+  (short:long) --. fun = flagNone (filter (/= " ") [[short],long]) fun                   ""
   parseMinTests :: String -> Int -> Int
   parseMinTests s | last s == '%' = \x -> read (init s) * x `div` 100
                   | otherwise     = const (read s)
--- TODO: implement space char semantics
 
 getArgs :: Args -> IO Args
 getArgs = processArgs . prepareArgs
diff --git a/src/Test/Speculate/CondReason.hs b/src/Test/Speculate/CondReason.hs
--- a/src/Test/Speculate/CondReason.hs
+++ b/src/Test/Speculate/CondReason.hs
@@ -126,13 +126,9 @@
 canonicalCEqn :: (Expr -> Expr -> Ordering) -> (Expr,Expr,Expr) -> Bool
 canonicalCEqn cmp = canonicalCEqnBy cmp preludeInstances
 
-prettyChy :: ((Expr,Expr,Expr) -> Bool) -> Chy -> String
-prettyChy shouldShow =
-    table "r r r l l"
-  . map (\(pre,e1,e2) -> [ showOpExpr "==>" pre
-                         , "==>", showOpExpr "==" e1
-                         , "==",  showOpExpr "==" e2 ])
-  . sortOn (typ . (\(c,x,y) -> x))
+finalCondEquations :: ((Expr,Expr,Expr) -> Bool) -> Chy -> [(Expr,Expr,Expr)]
+finalCondEquations shouldShow =
+    sortOn (typ . (\(c,x,y) -> x))
   . filter shouldShow
   . cequations
   . cfinalize
diff --git a/src/Test/Speculate/Engine.hs b/src/Test/Speculate/Engine.hs
--- a/src/Test/Speculate/Engine.hs
+++ b/src/Test/Speculate/Engine.hs
@@ -95,6 +95,19 @@
 ----------------------------
 -- * Enumerating expressions
 
+-- | Computes a theory from atomic expressions.  Example:
+--
+-- > > theoryFromAtoms 5 compare (const True) (equal preludeInstances 100)
+-- > >   [hole (undefined :: Int),constant "+" ((+) :: Int -> Int -> Int)]
+-- > Thy { rules = [ (x + y) + z == x + (y + z) ]
+-- >     , equations = [ y + x == x + y
+-- >                   , y + (x + z) == x + (y + z)
+-- >                   , z + (x + y) == x + (y + z)
+-- >                   , z + (y + x) == x + (y + z) ]
+-- >     , canReduceTo = (|>)
+-- >     , closureLimit = 2
+-- >     , keepE = keepUpToLength 5
+-- >     }
 theoryFromAtoms :: Int -> (Expr -> Expr -> Ordering) -> (Expr -> Bool) -> (Expr -> Expr -> Bool) -> [Expr] -> Thy
 theoryFromAtoms sz cmp keep (===) = fst . theoryAndRepresentativesFromAtoms sz cmp keep (===)
 
@@ -108,6 +121,8 @@
   where
   fes *$* xes = filter keep $ catMaybes [fe $$ xe | fe <- fes, xe <- xes]
 
+-- | Given atomic expressions, compute theory and representative schema
+--   expressions.
 theoryAndRepresentativesFromAtoms :: Int
                                   -> (Expr -> Expr -> Ordering)
                                   -> (Expr -> Bool) -> (Expr -> Expr -> Bool)
@@ -136,6 +151,14 @@
 distinctFromSchemas :: Instances -> Int -> Int -> Thy -> [Expr] -> [Expr]
 distinctFromSchemas ti nt nv thy = map C.rep . classesFromSchemas ti nt nv thy
 
+-- > > classesFromSchemas preludeInstances 500 2 thy [_ + _, _ + (_ + _)]
+-- > [ (x + x :: Int,[])
+-- > , (x + y :: Int,[y + x :: Int])
+-- > , (y + y :: Int,[])
+-- > , (x + (x + x) :: Int,[])
+-- > , (x + (x + y) :: Int,[x + (y + x) :: Int,y + (x + x) :: Int])
+-- > , (x + (y + y) :: Int,[y + (x + y) :: Int,y + (y + x) :: Int])
+-- > , (y + (y + y) :: Int,[]) ]
 classesFromSchemas :: Instances -> Int -> Int -> Thy -> [Expr] -> [Class Expr]
 classesFromSchemas ti nt nv thy = C.mergesThat (equal ti nt)
                                 . C.mergesOn (normalizeE thy)
@@ -144,6 +167,14 @@
 -- won't detect all equivalences.  here we test the few remaining
 -- there shouldn't be that much overhead
 
+-- | Returns all classes of expressions that can be build from expression
+--   schemas (single variable expressions).  Examples:
+--
+-- > > classesFromSchema preludeInstances thy 2 (i_ -+- i_)
+-- > [ (x + x :: Int,[])
+-- > , (x + y :: Int,[])
+-- > , (y + x :: Int,[])
+-- > , (y + y :: Int,[]) ]
 classesFromSchema :: Instances -> Thy -> Int -> Expr -> [Class Expr]
 classesFromSchema ti thy n = C.mergesOn (normalizeE thy)
                            . map C.fromRep
diff --git a/src/Test/Speculate/Pretty.hs b/src/Test/Speculate/Pretty.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Speculate/Pretty.hs
@@ -0,0 +1,49 @@
+-- | Pretty printing of Equations, Inequalities and Conditional Equations
+module Test.Speculate.Pretty
+  ( prettyThy, prettyEquations
+  , prettyShy, prettySemiEquations
+  , prettyChy, prettyCondEquations
+  )
+where
+
+import Test.Speculate.Expr
+import Test.Speculate.Utils.PrettyPrint
+import Test.Speculate.Reason     (Thy, finalEquations)
+import Test.Speculate.SemiReason (Shy, finalSemiEquations)
+import Test.Speculate.CondReason (Chy, finalCondEquations)
+
+type Equation = (Expr,Expr)
+type CondEquation = (Expr,Expr,Expr)
+
+prettyThy :: (Equation -> Bool) -> Instances -> Thy -> String
+prettyThy shouldShow ti = prettyEquations . finalEquations shouldShow ti
+
+prettyChy :: (CondEquation -> Bool) -> Chy -> String
+prettyChy shouldShow = prettyCondEquations . finalCondEquations shouldShow
+
+prettyShy :: (Equation -> Bool) -> Instances -> (Expr -> Expr -> Bool) -> Shy -> String
+prettyShy shouldShow insts equivalentInstanceOf =
+  prettySemiEquations . finalSemiEquations shouldShow insts equivalentInstanceOf
+
+prettyEquations :: [Equation] -> String
+prettyEquations =
+  table "r l l" . map showEquation
+  where
+  showEquation (e1,e2)
+--  | typ e1 == boolTy = [showOpExpr "<==>" e1, "<==>", showOpExpr "<==>" e2]
+    | otherwise        = [showOpExpr "==" e1, "==", showOpExpr "==" e2]
+
+prettySemiEquations :: [Equation] -> String
+prettySemiEquations =
+  table "r l l" . map showSELine
+  where
+  showSELine (e1,e2) = showLineWithOp (if typ e1 == boolTy then "==>" else "<=") (e1,e2)
+  showLineWithOp o (e1,e2) = [showOpExpr o e1, o, showOpExpr o e2]
+
+prettyCondEquations :: [CondEquation] -> String
+prettyCondEquations =
+  table "r r r l l" . map showCELine
+  where
+  showCELine (ce,e1,e2) = [ showOpExpr "==>" ce
+                          , "==>", showOpExpr "==" e1
+                          , "==",  showOpExpr "==" e2 ]
diff --git a/src/Test/Speculate/Reason.hs b/src/Test/Speculate/Reason.hs
--- a/src/Test/Speculate/Reason.hs
+++ b/src/Test/Speculate/Reason.hs
@@ -15,7 +15,7 @@
   , (|==|)
   , theorize
   , theorizeBy
-  , prettyThy
+  , finalEquations
   , criticalPairs
   , normalizedCriticalPairs
   , append
@@ -414,17 +414,13 @@
   showEquations = unlines . map showEquation
   showEquation (e1,e2) = showExpr e1 ++ " == " ++ showExpr e2
 
-prettyThy :: (Equation -> Bool) -> Instances -> Thy -> String
-prettyThy shouldShow ti thy =
-    table "r l l" . map showEquation
-  . sortOn (typ . fst) . sortBy (compareE thy `on` uncurry phonyEquation)
+finalEquations :: (Equation -> Bool) -> Instances -> Thy -> [Equation]
+finalEquations shouldShow ti thy =
+    sortOn (typ . fst) . sortBy (compareE thy `on` uncurry phonyEquation)
   . filter shouldShow
   $ rules thy' ++ map swap (equations thy')
   where
   thy' = canonicalizeThyWith ti . discardRedundantRulesByEquations $ finalize thy
-  showEquation (e1,e2)
---  | typ e1 == boolTy = [showOpExpr "<==>" e1, "<==>", showOpExpr "<==>" e2]
-    | otherwise        = [showOpExpr "==" e1, "==", showOpExpr "==" e2]
 
 -- | Finalize a theory by discarding redundant equations.  If after finalizing
 --   you 'complete', redundant equations might pop-up again.
diff --git a/src/Test/Speculate/Report.hs b/src/Test/Speculate/Report.hs
--- a/src/Test/Speculate/Report.hs
+++ b/src/Test/Speculate/Report.hs
@@ -12,6 +12,7 @@
 import Test.Speculate.Args
 import Test.Speculate.Utils
 import Test.Speculate.Utils.Colour
+import Test.Speculate.Pretty
 
 import Data.Ratio ((%))
 import Control.Monad (when,unless)
@@ -38,15 +39,20 @@
       putStrLn "Use `--force` or `args{force=true}` to ignore instance errors."
       fail "exiting"
   when (showTheory args)       . putStrLn $ showThy thy
-  when (showEquations args) . putStrLn $ prettyThy (shouldShowEquation args) ti thy
+  let shy = semiTheoryFromThyAndReps ti n (maxVars args) thy
+          $ filter (\e -> lengthE e <= computeMaxSemiSize args) es
+  let chy = conditionalTheoryFromThyAndReps ti (compareExpr args) n (maxVars args) (computeMaxCondSize args) thy es
+  let equations     = finalEquations     (shouldShowEquation args) ti                          thy
+  let semiEquations = finalSemiEquations (shouldShowEquation args) ti (equivalentInstance thy) shy
+  let condEquations = finalCondEquations (shouldShowConditionalEquation args)                  chy
+  when (showEquations args)        . putStrLn $ prettyEquations equations
+  when (showSemiequations args)    . putStrLn $ prettySemiEquations semiEquations
+  when (reallyShowConditions args) . putStrLn $ prettyCondEquations condEquations
+  when (showCounts args) . putStrLn . unlines
+    $  [ "#-equations      = " ++ show (length equations)     | showEquations        args ]
+    ++ [ "#-semi-equations = " ++ show (length semiEquations) | showSemiequations    args ]
+    ++ [ "#-cond-equations = " ++ show (length condEquations) | reallyShowConditions args ]
   reportClassesFor ti n (showClassesFor args) thy es
-  when (showSemiequations args) . putStrLn
-    . prettyShy (shouldShowEquation args) ti (equivalentInstance thy)
-    . semiTheoryFromThyAndReps ti n (maxVars args) thy
-    $ filter (\e -> lengthE e <= computeMaxSemiSize args) es
-  when (reallyShowConditions args) . putStrLn
-    . prettyChy (shouldShowConditionalEquation args)
-    $ conditionalTheoryFromThyAndReps ti (compareExpr args) n (maxVars args) (computeMaxCondSize args) thy es
   when (showDot args) $
     reportDot ti (onlyTypes args) (quietDot args) (maxVars args) n thy es
 
diff --git a/src/Test/Speculate/SemiReason.hs b/src/Test/Speculate/SemiReason.hs
--- a/src/Test/Speculate/SemiReason.hs
+++ b/src/Test/Speculate/SemiReason.hs
@@ -81,20 +81,15 @@
           . concatMap (\(e1,e2) -> [e1,e2])
           $ sequations shy
 
-prettyShy :: (Equation -> Bool) -> Instances -> (Expr -> Expr -> Bool) -> Shy -> String
-prettyShy shouldShow insts equivalentInstanceOf shy =
-    table "r l l"
-  . map showSELine
-  . sortOn (typ . fst)
+finalSemiEquations :: (Equation -> Bool) -> Instances -> (Expr -> Expr -> Bool) -> Shy -> [Equation]
+finalSemiEquations shouldShow insts equivalentInstanceOf shy =
+    sortOn (typ . fst)
   . filter shouldShow
   . discardLater (equivalentInstanceOf `on` uncurry phonyEquation)
   . discard (transConsequence shy)
   . discardLater (isInstanceOf `on` uncurry phonyEquation)
   . sequations
   $ canonicalizeShyWith insts shy
-  where
-  showSELine (e1,e2) = showLineWithOp (if typ e1 == boolTy then "==>" else "<=") (e1,e2)
-  showLineWithOp o (e1,e2) = [showOpExpr o e1, o, showOpExpr o e2]
 
 canonicalizeShyWith :: Instances -> Shy -> Shy
 canonicalizeShyWith = mapSemiEquations . canonicalizeSemiEquationWith
diff --git a/tests/Test.hs b/tests/Test.hs
--- a/tests/Test.hs
+++ b/tests/Test.hs
@@ -116,6 +116,7 @@
 import qualified Test.Speculate.Expr as E
 import Test.Speculate.Reason
 import Test.Speculate.Reason.Order
+import Test.Speculate.Engine hiding (true, false)
 
 import Data.Char (ord)
 import Data.Dynamic