diff --git a/BPS.cabal b/BPS.cabal
--- a/BPS.cabal
+++ b/BPS.cabal
@@ -5,7 +5,7 @@
 -- see: https://github.com/sol/hpack
 
 name:           BPS
-version:        0.1.0.0
+version:        0.1.1.0
 synopsis:       Translations of classic Truth Maintenance Systems
 description:    Haskell monad transformer-based translations of two classic Truth Maintenance System algorithms of Forbus and de Kleer's /Building Problem Solvers/.  This version includes justification-based and assumption-based TMS (JTMS and ATMS) implementations.  See the GitHub repository <https://github.com/jphmrst/bps/>, or the Haddock documentation.
 category:       Truth maintenance
@@ -19,7 +19,7 @@
 build-type:     Simple
 extra-source-files:
     README.md
-    ChangeLog.md
+    CHANGELOG.md
     Haskell-LICENSE.txt
 
 source-repository head
@@ -31,6 +31,7 @@
       Data.TMS.ATMS.ATMST
       Data.TMS.ChooseDebugging
       Data.TMS.Dbg
+      Data.TMS.Formatters
       Data.TMS.Helpers
       Data.TMS.JTMS
       Data.TMS.MList
@@ -62,6 +63,29 @@
   ghc-options: -threaded -rtsopts -with-rtsopts=-N
   build-depends:
       BPS
+    , STMonadTrans >=0.4.6 && <0.5
+    , base (>=4.14.1 && <4.15) || (>=4.15.1 && <4.16) || (>=4.16.0 && <4.17)
+    , extra ==1.7.*
+    , free
+    , mtl >=2.2.2 && <2.3
+    , resourcet
+    , symbol
+    , template-haskell
+    , transformers >=0.5.6 && <0.6
+  default-language: Haskell2010
+
+executable hbps_profile
+  main-is: Main.hs
+  other-modules:
+      ATMSTrun
+      JTMSrun
+      Paths_BPS
+  hs-source-dirs:
+      src/main/haskell/prof
+  ghc-options: -threaded -rtsopts -with-rtsopts=-N
+  build-depends:
+      BPS
+    , MonadRandom
     , STMonadTrans >=0.4.6 && <0.5
     , base (>=4.14.1 && <4.15) || (>=4.15.1 && <4.16) || (>=4.16.0 && <4.17)
     , extra ==1.7.*
diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,54 @@
+
+Note that the *repository* version numbers do not directly correspond
+to the release numbers of either the Haskell or Scala releases.
+Haskell releases adhere to Haskell's [Package Versioning
+Policy](https://pvp.haskell.org/); Scala releases use the [Semantic
+Versioning spec](https://semver.org/).
+
+# Version 0.6.0 (Haskell 0.1.1.0, Scala 0.1.0)
+
+ - Added `interpretations` in Haskell implementation.  Only lighted
+   tested at this point.
+
+# Version 0.5.0 (Haskell 0.1.0.0, Scala 0.1.0)
+
+ - First version with Haskell: working implementation of a monad
+   transformer for the JTMS and ATMS.  The `interpretations` and
+   `explain-node` functions of the ATMS are not yet translated, and
+   are omitted from the module API.
+
+ - Promoting Scala release to 0.1.0.  No significant additions, but it
+   will be nice to distinguish new feature additions at 0.x.0 from
+   patches and documentation additions at 0.x.y.
+
+# Version 0.4.0 (Scala only, 0.0.4)
+
+ - Documentation for both JTMS and ATMS.
+
+ - Generator for large randomized ATMS examples.
+
+ - Some tweaks to data structure selection based on rough profiling.
+ 
+# Version 0.3.0 (Scala only, 0.0.3)
+
+ - Contains a mostly-working version of a standalone ATMS.
+
+# Version 0.2.0 (Scala only, 0.0.2)
+
+ - Separation of the standalone JTMS from (untranslated) JTMS+JTRE
+   wrapper.
+
+    - Further testing and debugging of the standalone JTMS.
+
+    - Scaladoc documentation of the standalone JTMS.
+
+    - There may be additional type parameters in later versions of
+      the standalone JTMS.
+
+ - First version containing this file.
+
+# Version 0.1.0 (Scala only, 0.0.1)
+
+Initial release
+
+ - Contains a mostly-working version of the standalone JTMS.
diff --git a/ChangeLog.md b/ChangeLog.md
deleted file mode 100644
--- a/ChangeLog.md
+++ /dev/null
@@ -1,51 +0,0 @@
-
-Note that the *repository* version numbers do not directly correspond
-to the release numbers of either the Haskell or Scala releases.
-Haskell releases adhere to Haskell's [Package Versioning
-Policy](https://pvp.haskell.org/); Scala releases use the [Semantic
-Versioning spec](https://semver.org/).
-
-# In Haskell branch — Haskell 0.2.0.0
-
- - Translation of ATMS underway.
-
-# Version 0.5.0 (Haskell 0.1.0.0, Scala 0.1.0)
-
- - First version with Haskell: working implementation of a monad
-   transformer for JTMSes.
-
- - Promoting Scala release to 0.1.0.  No significant additions, but it
-   will be nice to distinguish new feature additions at 0.x.0 from
-   patches and documentation additions at 0.x.y.
-
-# Version 0.4.0 (Scala only, 0.0.4)
-
- - Documentation for both JTMS and ATMS.
-
- - Generator for large randomized ATMS examples.
-
- - Some tweaks to data structure selection based on rough profiling.
- 
-# Version 0.3.0 (Scala only, 0.0.3)
-
- - Contains a mostly-working version of a standalone ATMS.
-
-# Version 0.2.0 (Scala only, 0.0.2)
-
- - Separation of the standalone JTMS from (untranslated) JTMS+JTRE
-   wrapper.
-
-    - Further testing and debugging of the standalone JTMS.
-
-    - Scaladoc documentation of the standalone JTMS.
-
-    - There may be additional type parameters in later versions of
-      the standalone JTMS.
-
- - First version containing this file.
-
-# Version 0.1.0 (Scala only, 0.0.1)
-
-Initial release
-
- - Contains a mostly-working version of the standalone JTMS.
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -6,11 +6,10 @@
 
 The current version includes working versions of the justification-
 and assumption-based truth maintenance systems (JTMS and ATMS) in both
-languages.  The Haskell translation omits the two top-level functions
-`interpretations` and `explainNode` of the original system, but
-otherwise both translations include all of the original functionality
-of these two TMSes.  There is a partial translation of the rule engine
-wrapper for these TMSes in Scala.
+languages.  The Haskell translation omits the two top-level function
+of the original system, but otherwise both translations include all of
+the original functionality of these two TMSes.  There is a partial
+translation of the rule engine wrapper for these TMSes in Scala.
 
 To contribute, submit pull requests to one of the three branches
 `atms` (Scala), `jtms` (Scala) or `haskell` (both JTMS and ATMS), or
diff --git a/src/main/haskell/app/ATMSTrun.hs b/src/main/haskell/app/ATMSTrun.hs
--- a/src/main/haskell/app/ATMSTrun.hs
+++ b/src/main/haskell/app/ATMSTrun.hs
@@ -1,34 +1,100 @@
 module ATMSTrun where
 
-import Data.Symbol
+import Control.Monad.State
+import Data.TMS.Formatters
 import Data.TMS.ATMS.ATMST
 
+-- Corresponds to Lisp function `book-1` in src/main/lisp/atms/atest.lisp
 runATMS1 :: IO (Either AtmsErr ())
 runATMS1 = do
   runATMST $ do
-    atms <- createATMS "Ex1"
-    setInformantStringViaString atms
-    setDatumStringViaString atms
-    -- debugAtms "Created" atms
-    na <- createNode atms "A" True False
-    -- debugAtms "Added assumption node A" atms
-    nc <- createNode atms "C" True False
-    -- debugAtms "Added assumption node C" atms
-    ne <- createNode atms "E" True False
-    -- debugAtms "Added assumption node E" atms
-    nh <- createNode atms "H" False False
-    -- debugAtms "Added non-assumption node H" atms
-    justifyNode "R1" nh [nc, ne]
-    -- debugAtms "After rule R1" atms
-    ng <- createNode atms "G" False False
-    -- debugAtms "After non-assumption node G" atms
-    justifyNode "R2" ng [na, nc]
-    -- debugAtms "After rule R2" atms
-    nx <- createNode atms "X" False True
-    -- debugAtms "After contradiction node X" atms
-    justifyNode "R3" nx [ng]
-    -- debugAtms "After rule R3" atms
-    nb <- createNode atms "B" True False
-    debugAtms "Added assumption node B" atms
-    justifyNode "R4" nh [nb, nc]
-    debugAtms "After rule R4" atms
+    do
+      atms <- createATMS "Ex1"
+      setInformantStringViaString atms
+      setDatumStringViaString atms
+      -- debugAtms "Created" atms
+      na <- createNode atms "A" True False
+      -- debugAtms "Added assumption node A" atms
+      nc <- createNode atms "C" True False
+      -- debugAtms "Added assumption node C" atms
+      ne <- createNode atms "E" True False
+      -- debugAtms "Added assumption node E" atms
+      nh <- createNode atms "H" False False
+      -- debugAtms "Added non-assumption node H" atms
+      justifyNode "R1" nh [nc, ne]
+      -- debugAtms "After rule R1" atms
+      ng <- createNode atms "G" False False
+      -- debugAtms "After non-assumption node G" atms
+      justifyNode "R2" ng [na, nc]
+      -- debugAtms "After rule R2" atms
+      nx <- createNode atms "X" False True
+      -- debugAtms "After contradiction node X" atms
+      justifyNode "R3" nx [ng]
+      -- debugAtms "After rule R3" atms
+      nb <- createNode atms "B" True False
+
+      liftIO $ putStrLn "Added assumption node B"
+      debug atms
+      justifyNode "R4" nh [nb, nc]
+      liftIO $ putStrLn "After rule R4"
+      debug atms
+
+      liftIO $ putStrLn "----------------------------------------"
+      i1 <- interpretations atms [[na, nc], [nh, ng]]
+      liftIO $ putStrLn "Interpretations for (a, c); (h, g): "
+      forM_ i1 $ debug
+
+      liftIO $ putStrLn "----------------------------------------"
+      i2 <- interpretations atms [[nh, ng]]
+      liftIO $ putStrLn "Interpretations for (h, g): "
+      forM_ i2 $ debug
+
+      liftIO $ putStrLn "----------------------------------------"
+      i3 <- interpretations atms [[nh]]
+      liftIO $ putStrLn "Interpretations for (h): "
+      forM_ i3 $ debug
+
+    do
+      liftIO $ putStrLn "========================================"
+      atms <- createATMS "Ex2"
+      setInformantStringViaString atms
+      setDatumStringViaString atms
+      na <- createNode atms "A" True False
+      nb <- createNode atms "B" True False
+      nc <- createNode atms "C" True False
+      nd <- createNode atms "D" True False
+      ne <- createNode atms "E" True False
+      nf <- createNode atms "F" True False
+      ng <- createNode atms "G" True False
+      nh <- createNode atms "H" True False
+      nm <- createNode atms "M" False False
+      nn <- createNode atms "N" False False
+      np <- createNode atms "P" False False
+      nq <- createNode atms "Q" False False
+      nr <- createNode atms "R" False False
+      ns <- createNode atms "S" False False
+      nk1 <- createNode atms "K1" False False
+      nk2 <- createNode atms "K2" False False
+      nk3 <- createNode atms "K3" False False
+      justifyNode "R01" nm [na, nb]
+      justifyNode "R02" nm [nc, nd]
+      justifyNode "R03" nn [nb, nc]
+      justifyNode "R04" np [nc]
+      justifyNode "R05" nq [nc, nd, ne]
+      justifyNode "R06" nr [nf, ng]
+      justifyNode "R07" ns [nf, nh]
+      justifyNode "R08" nk1 [nm, np]
+      justifyNode "R09" nk1 [nn, nq]
+      justifyNode "R10" nk2 [nn]
+      justifyNode "R11" nk2 [np]
+      justifyNode "R12" nk3 [nn, nq]
+      justifyNode "R13" nk3 [nq, nr, ns]
+      nx <- createNode atms "X" False True
+      justifyNode "X" nx [nc, nf]
+
+      debug atms
+
+      liftIO $ putStrLn "----------------------------------------"
+      i3 <- interpretations atms [[nk3]]
+      liftIO $ putStrLn "Interpretations for (k3): "
+      forM_ i3 $ debug
diff --git a/src/main/haskell/lib/Data/TMS/ATMS/ATMST.hs b/src/main/haskell/lib/Data/TMS/ATMS/ATMST.hs
--- a/src/main/haskell/lib/Data/TMS/ATMS/ATMST.hs
+++ b/src/main/haskell/lib/Data/TMS/ATMS/ATMST.hs
@@ -17,10 +17,9 @@
 typing, which necessitates some additional tagging, and to the
 abomination which is Lisp's @do@ macro.  The translation relies on
 mutable data structures using `STT` state thread references.  A more
-pure translation, possibly not relying on the [@ST@
-monad]("Control.Monad.ST")/[@STT@
-transformer]("Control.Monad.ST.Trans"), is a significant piece of
-future work.
+pure translation, possibly not relying on the
+[@ST@ monad]("Control.Monad.ST")/[@STT@ transformer]("Control.Monad.ST.Trans"),
+is a significant piece of future work.
 
 Note also there are restrictions on the embedded monad @m@ which can
 be wrapped in the `STT` transformer; see [the @Control.Monad.ST.Trans@
@@ -43,6 +42,7 @@
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
 
 module Data.TMS.ATMS.ATMST (
   -- * The ATMST monad
@@ -84,7 +84,7 @@
   Env, EnvTable, envIndex, envAssumptions, getEnvNodes,
 
   -- * Deduction and search utilities
-  {- interpretations, -}
+  interpretations, interpretationsWithDefaults,
 
   -- ** Related to a node
   isTrueNode, isInNode, isInNodeByEnv, isOutNode, isNodeConsistentWith,
@@ -95,27 +95,35 @@
 
   -- * Printing and debugging
 
-  -- |Functions prefixed @format@ build a computation returning a
+  -- | In addition to the functions documented below, many of the
+  -- types defined in this module are instances of the classes defined
+  -- in `Data.TMS.Formatters`.  Specifically:
+  --
+  --  - __Defined for `format`, `blurb`, etc:__ `Node`, `Justification`
+  --
+  --  - __Defined for `pprint`:__ `Node`, `JustRule`, `Justification`,
+  --    `Env`, `EnvTable`
+  --
+  --  - __Defined for `debug`:__ `ATMS`, `Node`, `JustRule`, `Env`
+  --
+  -- Functions prefixed @format@ build a computation returning a
   -- `String`.  Functions prefixed @debug@ or @print@ build a unit
   -- computation printing the artifact in question to standard output;
   -- those with prefix @debug@ are generally more verbose.
-  debugAtms, printAtms, debugAtmsEnvs,
+  debugAtmsEnvs,
   printAtmsStatistics,
 
   -- ** Nodes and node lists
-  formatNode, formatNodes, debugNode, printNode,
   whyNodes, whyNode,
 
   -- ** Environments, labels, and tables
-  debugEnv, debugEnvTable, formatNodeLabel,
+  debugEnvTable, formatNodeLabel, debugNodeLabel,
   debugNogoods,
-  printEnv, printNogoods, printEnvs, printEnvTable, printTable,
-
-  -- ** Justifications
-  debugJust, printJust, formatJustification
+  printNogoods, printEnvs
 
   ) where
 
+import Control.Monad
 import Control.Monad.State
 import Control.Monad.ST.Trans
 -- import Control.Monad.Except
@@ -123,6 +131,7 @@
 import Control.Monad.Extra
 import Data.List
 import Data.Symbol
+import Data.TMS.Formatters
 import Data.TMS.Helpers
 import Data.TMS.MList
 import Data.TMS.Dbg
@@ -325,9 +334,25 @@
   -- |List of external procedures to be executed for this ATMS.
   atmsEnqueueProcedure :: STRef s (r -> ATMST s m ()),
   -- |Set to `True` when we wish to debug this ATMS.
-  atmsDebugging :: STRef s Bool
+  adebugging :: STRef s Bool
 }
 
+-- |Print the internal title signifying an ATMS.
+--
+-- Translated from @print-atms@ in @atms.lisp@.
+instance NodeDatum d => Printed (ATMS d i r) ATMST where
+  pprint atms = liftIO $ putStrLn $ "#<ATMS: " ++ atmsTitle atms ++ ">"
+
+-- |Give a verbose printout of an `ATMS`.
+instance NodeDatum d => Debugged (ATMS d i r) ATMST where
+  debug atms = do
+    liftIO $ putStrLn $ "=============== " ++ atmsTitle atms
+    debugNodes atms
+    debugJusts atms
+    debugAtmsEnvs atms
+    debugNogoods atms
+    liftIO $ putStrLn "=============== "
+
 -- |Shortcut maker for reading from an `ATMS` reference.
 getATMSMutable ::
   (Monad m, NodeDatum d) =>
@@ -485,12 +510,6 @@
 {-# INLINE setEnqueueProcedure #-}
 setEnqueueProcedure = setATMSMutable atmsEnqueueProcedure
 
--- |Print the internal title signifying an ATMS.
---
--- Translated from @print-atms@ in @atms.lisp@.
-printAtms :: (MonadIO m, NodeDatum d) => ATMS d i r s m -> ATMST s m ()
-printAtms atms = liftIO $ putStrLn $ "#<ATMS: " ++ atmsTitle atms ++ ">"
-
 -- |Get the next node counter value, incrementing for future accesses.
 nextNodeCounter :: (Monad m, NodeDatum d) => ATMS d i r s m -> ATMST s m Int
 nextNodeCounter jtms = sttLayer $ do
@@ -546,6 +565,48 @@
 instance (Monad m, NodeDatum d) => Show (Node d i r s m) where
   show n = "<Node " ++ show (nodeIndex n) ++ ">"
 
+-- |`format`, `blurb`, etc. may be applied to `Node`s in an
+-- `ATMST`.
+instance NodeDatum d => Formatted (Node d i r) ATMST where
+  format node = do
+    datumFmt <- getDatumString $ nodeATMS node
+    return $ datumFmt (nodeDatum node)
+
+-- |Print a `Node` of an `ATMS` with its tag.
+--
+-- Translated from @print-tms-node@ in @atms.lisp@.
+instance NodeDatum d => Printed (Node d i r) ATMST where
+  pprint node = do
+    str <- nodeString node
+    liftIO $ putStr $ "<NODE: " ++ str ++ ">"
+
+-- |Give a verbose printout of a `Node` of an `ATMS`.
+instance NodeDatum d => Debugged (Node d i r) ATMST where
+  debug node = do
+    let atms = nodeATMS node
+    datumFmt <- getDatumString atms
+    informantFmt <- getInformantString atms
+    liftIO $ putStrLn $ "- " ++ datumFmt (nodeDatum node)
+
+    label <- getNodeLabel node
+    case label of
+      [] -> liftIO $ putStrLn "  Empty label"
+      [env] -> do
+        liftIO $ putStr "  Single environment label: "
+        debug env
+      _ -> forM_ label $ \env -> do
+        liftIO $ putStrLn "  - "
+        debug env
+
+    conseqs <- getNodeConsequences node
+    case conseqs of
+      [] -> liftIO $ putStrLn "  Antecedent to no justifications"
+      _ -> do
+        liftIO $ putStr "  Antecedent to:"
+        forM_ conseqs $ \ conseq -> do
+          liftIO $ putStr $ " " ++ informantFmt (justInformant conseq)
+        liftIO $ putStrLn ""
+
 -- |Shortcut maker for reading from a `Node` reference.
 getNodeMutable ::
   (Monad m, NodeDatum d) =>
@@ -628,10 +689,48 @@
 instance (Monad m, NodeDatum d) => Eq (JustRule d i r s m) where
   e1 == e2 = (justIndex e1) == (justIndex e2)
 
+-- |Print a more verbose description of a `Just`ification rule of an
+-- `ATMS`.
+--
+-- Translated from @print-just@ in @atms.lisp@.
+instance NodeDatum d => Printed (JustRule d i r) ATMST where
+  pprint rule = do
+    infStr <- formatJustInformant rule
+    liftIO $ putStr $ "<" ++ infStr ++ " " ++ show (justIndex rule) ++ ">"
+
+instance NodeDatum d => Debugged (JustRule d i r) ATMST where
+  debug (JustRule idx inf conseq ants) = do
+    let atms = nodeATMS conseq
+    informantFmt <- getInformantString atms
+    datumFmt <- getDatumString atms
+    liftIO $ putStrLn $ "  "
+      ++ "[" ++ informantFmt inf ++ "." ++ show idx ++ "] "
+      ++ datumFmt (nodeDatum conseq) ++ " <= "
+      ++ intercalate ", " (map (datumFmt . nodeDatum) ants)
+
 -- |Description of why a `Node` may be believed by the `ATMS`.
 data Justification d i r s m =
   ByRule (JustRule d i r s m) | ByAssumption (Node d i r s m) | ByContradiction
 
+-- |`format`, `blurb`, etc. may be applied to `Node`s in an
+-- `ATMST`.
+instance NodeDatum d => Formatted (Justification d i r) ATMST where
+  format (ByRule j) = return $ "By rule " ++ show (justIndex j)
+  format (ByAssumption n) = do
+    nodeFmt <- getNodeString (nodeATMS n)
+    return $ "By assumption " ++ nodeFmt n
+  format ByContradiction = return "By contradiction"
+
+-- |`format`, `blurb`, etc. may be applied to `Justification`s
+-- in an `ATMST`.
+instance NodeDatum d => Printed (Justification d i r) ATMST where
+  pprint j = case j of
+    ByRule rule -> pprint rule
+    ByAssumption node -> do
+      liftIO $ putStr $ "Assumed node "
+      pprint node
+    ByContradiction -> liftIO $ putStrLn $ "By contradiction"
+
 -- |Explanation of why a `Node` may be believed by the `ATMS` for
 -- output to a query.
 data Explanation d i r s m =
@@ -670,6 +769,39 @@
 instance (Monad m, NodeDatum d) => Show (Env d i r s m) where
   show n = "<Env " ++ show (envIndex n) ++ ">"
 
+-- |`format` etc. for `Env`, translated from @print-env@ in @atms.lisp@.
+instance NodeDatum d => Formatted (Env d i r) ATMST where
+  format env = do
+    let assumptions = envAssumptions env
+    case (null assumptions) of
+      True -> return "<empty env>"
+      False -> do
+        printer <- getNodeString $ nodeATMS $ head assumptions
+        strs <- mapM format assumptions
+        return $ "<env:" ++ intercalate "," strs ++ ">"
+
+-- |`pprint` for `Env`, translated from @print-env@ in @atms.lisp@.
+instance NodeDatum d => Printed (Env d i r) ATMST where
+  pprint env = do
+    whenM (envIsNogood env) $ liftIO $ putStr "* "
+    -- liftIO $ putStr "ZZZZZ "
+    envString env
+    liftIO $ putStrLn ""
+
+-- |Give a verbose printout of one `Env`ironment of an `ATMS`.
+instance NodeDatum d => Debugged (Env d i r) ATMST where
+  debug env = do
+    isNogood <- envIsNogood env
+    case envAssumptions env of
+      [] -> liftIO $ putStrLn "<empty env>"
+      nodes @ (n : _) -> do
+        let atms = nodeATMS n
+        datumFmt <- getDatumString atms
+        when isNogood $ liftIO $ putStr "[X] "
+        liftIO $ putStrLn $
+          (intercalate ", " $ map (datumFmt . nodeDatum) nodes)
+          ++ " (count " ++ show (length nodes) ++ ")"
+
 -- |Shortcut maker for reading from a `Env` reference.
 getEnvMutable ::
   (Monad m, NodeDatum d) =>
@@ -708,6 +840,15 @@
 -- length.
 newtype EnvTable d i r s m = EnvTable (STArray s Int [Env d i r s m])
 
+-- |Print the `Env`ironments contained in the given `EnvTable`.
+--
+-- Translated from @print-env-table@ in @atms.lisp@.
+instance NodeDatum d => Printed (EnvTable d i r) ATMST where
+  pprint (EnvTable arr) = do
+    let (lo, hi) = boundsSTArray arr
+    forM_ [lo..hi] $ \i ->
+      forMM_ (sttLayer $ readSTArray arr i) pprint
+
 findInEnvTable ::
   (Monad m, NodeDatum d) =>
     (Env d i r s m -> Bool) -> EnvTable d i r s m ->
@@ -868,7 +1009,8 @@
 --
 -- Translated from @node-consistent-with?@ in @atms.lisp@.
 isNodeConsistentWith ::
-  (Monad m, NodeDatum d) => Node d i r s m -> Env d i r s m -> ATMST s m Bool
+  (Debuggable m, NodeDatum d) =>
+    Node d i r s m -> Env d i r s m -> ATMST s m Bool
 isNodeConsistentWith node env = do
   labelEnvs <- getNodeLabel node
   anyByM (\ le -> do
@@ -918,7 +1060,7 @@
 -- `ATMS`.
 --
 -- Translated from @make-contradiction@ in @atms.lisp@.
-makeContradiction :: (Monad m, NodeDatum d) => Node d i r s m -> ATMST s m ()
+makeContradiction :: (Debuggable m, NodeDatum d) => Node d i r s m -> ATMST s m ()
 makeContradiction node = do
   let atms = nodeATMS node
   unlessM (getNodeIsContradictory node) $ do
@@ -948,7 +1090,8 @@
 
   -- Register the new justification with the nodes that can trigger
   -- it.
-  sttLayer $ forM_ antecedents $ \node -> push just $ nodeConsequences node
+  sttLayer $ forM_ antecedents $ \node ->
+    {-# SCC "justifyNode.push" #-} push just $ nodeConsequences node
 
   -- Register the new justification with the ATMS itself.
   sttLayer $ push just $ atmsJusts atms
@@ -962,14 +1105,13 @@
 -- `Node`s to be a contradiction associated with the given informant.
 --
 -- Translated from @nogood-nodes@ in @atms.lisp@.
-nogoodNodes :: (Monad m, NodeDatum d) => i -> [Node d i r s m] -> ATMST s m ()
+nogoodNodes :: (Debuggable m, NodeDatum d) => i -> [Node d i r s m] -> ATMST s m ()
 nogoodNodes informant nodes = do
   contra <- getContradictionNode (nodeATMS (head nodes))
   justifyNode informant contra nodes
 
 -- * Label updating
 
---
 -- Translated from @propagate@ in @atms.lisp@.
 propagate ::
   (Debuggable m, NodeDatum d) =>
@@ -993,10 +1135,10 @@
   liftIO $ putStrLn "Calling propagate with"
   let atms = nodeATMS $ justConsequence justRule
   liftIO $ putStr ". Just: "
-  debugJust justRule
+  debug justRule
 
   case antecedent of
-    Just n -> debugNode n
+    Just n -> debug n
     Nothing -> liftIO $ putStrLn ". No antecedent"
 
   envLen <- sttLayer $ mlength envs
@@ -1007,16 +1149,15 @@
       envm <- sttLayer $ mcar envs
       case envm of
         Nothing -> liftIO $ putStrLn "<nulled out>"
-        Just env -> debugEnv env
+        Just env -> debug env
     _ -> do
       liftIO $ putStrLn ". Envs:"
       mlistFor_ sttLayer envs $ \em -> do
         liftIO $ putStr "  . "
         case em of
-          Just e -> debugEnv e
+          Just e -> debug e
           Nothing -> liftIO $ putStrLn "<nulled out>"
 
---
 -- Translated from @update@ in @atms.lisp@.
 update ::
   (Debuggable m, NodeDatum d) =>
@@ -1069,12 +1210,10 @@
   (MonadIO m, NodeDatum d) =>
     MList s (Maybe (Env d i r s m)) ->
       Node d i r s m ->
-        JustRule d i r s m ->
+        Justification d i r s m ->
           ATMST s m ()
-debugUpdateArgs envs consequence justRule = do
+debugUpdateArgs envs consequence justification = do
   liftIO $ putStrLn "Calling update with"
-  let atms = nodeATMS $ justConsequence justRule
-
   envLen <- sttLayer $ mlength envs
   case envLen of
     0 -> liftIO $ putStrLn ". No envs"
@@ -1083,21 +1222,26 @@
       envm <- sttLayer $ mcar envs
       case envm of
         Nothing -> liftIO $ putStrLn "<nulled out>"
-        Just env -> debugEnv env
+        Just env -> debug env
     _ -> do
       liftIO $ putStrLn ". Envs:"
       mlistFor_ sttLayer envs $ \em -> do
         liftIO $ putStr "  . "
         case em of
-          Just e -> debugEnv e
+          Just e -> debug e
           Nothing -> liftIO $ putStrLn "<nulled out>"
 
   liftIO $ putStr ". Consequence: "
-  blurbNode consequence
+  blurb consequence
   liftIO $ putStrLn ""
 
   liftIO $ putStr ". Just: "
-  debugJust justRule
+  case justification of
+    ByRule justRule -> debug justRule
+    ByAssumption node -> do
+      liftIO $ putStr "by assumption "
+      pprint node
+    ByContradiction -> liftIO $ putStrLn "by contradiction"
 
 -- |Internal method to update the label of this node to include the
 -- given environments.  The inclusion is not simply list extension;
@@ -1187,7 +1331,7 @@
   let atms = nodeATMS node
 
   liftIO $ putStr "Calling updateLabel with node "
-  blurbNode node
+  blurb node
   liftIO $ putStrLn ""
 
   envLen <- sttLayer $ mlength newEnvs
@@ -1198,13 +1342,13 @@
       envm <- sttLayer $ mcar newEnvs
       case envm of
         Nothing -> liftIO $ putStrLn "<nulled out>"
-        Just env -> debugEnv env
+        Just env -> debug env
     _ -> do
       liftIO $ putStrLn ". Envs:"
       mlistFor_ sttLayer newEnvs $ \em -> do
         liftIO $ putStr "  . "
         case em of
-          Just e -> debugEnv e
+          Just e -> debug e
           Nothing -> liftIO $ putStrLn "<nulled out>"
 
 debugUpdateLabelFinal ::
@@ -1217,12 +1361,12 @@
     [] -> liftIO $ putStrLn ". No label envs"
     [env] -> do
       liftIO $ putStr ". Single label env: "
-      debugEnv env
+      debug env
     _ -> do
       liftIO $ putStrLn ". Final envs:"
       forM_ labelEnvs $ \e -> do
         liftIO $ putStr "  . "
-        debugEnv e
+        debug e
 
   envLen <- sttLayer $ mlength newEnvs
   case envLen of
@@ -1232,16 +1376,16 @@
       envm <- sttLayer $ mcar newEnvs
       case envm of
         Nothing -> liftIO $ putStrLn "<nulled out>"
-        Just env -> debugEnv env
+        Just env -> debug env
     _ -> do
       liftIO $ putStrLn ". Final envs:"
       mlistFor_ sttLayer newEnvs $ \em -> do
         liftIO $ putStr "  . "
         case em of
-          Just e -> debugEnv e
+          Just e -> debug e
           Nothing -> liftIO $ putStrLn "<nulled out>"
 
-  debugNode node
+  debug node
 
 -- |Update the label of node @antecedent@ to include the given @envs@
 -- environments, pruning environments which are a superset of another
@@ -1255,12 +1399,13 @@
     (MList s (Maybe (Env d i r s m))) ->
       [Node d i r s m] ->
         ATMST s m (MList s (Maybe (Env d i r s m)))
-weave antecedent givenEnvs antecedents = do
+weave antecedent givenEnvs antecedents = {-# SCC "weave.top" #-} do
   $(dbg [| debugWeaveArgs antecedent givenEnvs antecedents |])
 
   envsRef <- sttLayer $ newSTRef givenEnvs
 
   forM_ antecedents $ \node ->
+    {-# SCC "weave.outer-ants" #-}
     unless (maybe False (node ==) antecedent) $ do
       $(dbg [| debugWeaveNodeAntecedent node |])
 
@@ -1277,11 +1422,11 @@
       --  - An Env from the NODE's label.
       -- The union of these two is NEW-ENV, and the body of the loop
       -- considers how we should incorporate NEW-ENV into NEW-ENVS.
-      mlistFor_ sttLayer envs $ \envmaybe ->
+      {-# SCC "weave.forEnvLoop" #-} mlistFor_ sttLayer envs $ \envmaybe ->
         case envmaybe of
           Nothing -> return ()
           Just env -> do
-            forMM_ (sttLayer $ readSTRef $ nodeLabel node) $ \nodeEnv -> do
+            {-# SCC "weave.forEnv" #-} forMM_ (sttLayer $ readSTRef $ nodeLabel node) $ \nodeEnv -> do
               $(dbg [| debugWeavePairIntro env nodeEnv |])
 
               newEnv <- unionEnv env nodeEnv
@@ -1349,7 +1494,7 @@
 debugWeaveArgs antecedent givenEnvs antecedents = do
   liftIO $ putStrLn "Calling weave with"
   case antecedent of
-    Just n -> debugNode n
+    Just n -> debug n
     Nothing -> liftIO $ putStrLn ". No antecedent"
   let atms = case antecedent of
                Just a  -> Just $ nodeATMS a
@@ -1362,7 +1507,7 @@
       mlistFor_ sttLayer givenEnvs $ \em -> do
         liftIO $ putStr "  . "
         case em of
-          Just e -> debugEnv e
+          Just e -> debug e
           Nothing -> liftIO $ putStrLn "<nulled out>"
         return ()
     _ -> return ()
@@ -1421,7 +1566,7 @@
   liftIO $ putStrLn ""
 
 -- Translated from @in-antecedent?@ in @atms.lisp@.
-isInAntecedent :: (Monad m, NodeDatum d) => [Node d i r s m] -> ATMST s m Bool
+isInAntecedent :: (Debuggable m, NodeDatum d) => [Node d i r s m] -> ATMST s m Bool
 isInAntecedent [] = return True
 isInAntecedent nodes = do
   empty <- getEmptyEnvironment (nodeATMS (head nodes))
@@ -1431,7 +1576,7 @@
 --
 -- Translated from @weave?@ in @atms.lisp@.
 isWeave ::
-  (Monad m, NodeDatum d) => Env d i r s m -> [Node d i r s m] -> ATMST s m Bool
+  (Debuggable m, NodeDatum d) => Env d i r s m -> [Node d i r s m] -> ATMST s m Bool
 isWeave _ [] = return True
 isWeave env (n : ns) =
   anyMM (\e -> do
@@ -1504,7 +1649,7 @@
   (MonadIO m, NodeDatum d) => [Node d i r s m] -> ATMST s m ()
 debugCreateEnvStart nodes = do
   liftIO $ putStrLn $ "             - Running createEnv"
-  astr <- formatNodes "," nodes
+  astr <- formats "<none>" "," nodes
   liftIO $ putStrLn $ "               assumptions " ++ astr
 
 debugCreateEnvEnv ::
@@ -1622,7 +1767,7 @@
 --
 -- Translated from @find-or-make-env@ in @atms.lisp@.
 findOrMakeEnv ::
-  (Monad m, NodeDatum d) =>
+  (Debuggable m, NodeDatum d) =>
     [Node d i r s m] -> ATMS d i r s m -> ATMST s m (Env d i r s m)
 findOrMakeEnv [] atms = getEmptyEnvironment atms
 findOrMakeEnv assumptions atms = do
@@ -1671,7 +1816,7 @@
       ns = sortOn nodeIndex assumptions
   EnvTable envTable <- sttLayer $ readSTRef $ atmsEnvTable atms
   entries <- sttLayer $ readSTArray envTable $ length ns
-  case filter (\x -> envAssumptions x == ns) entries of
+  case filter (\x -> {-# SCC "lookupEnv.pred" #-} envAssumptions x == ns) entries of
     [] -> return Nothing
     (x : _) -> return $ Just x
 
@@ -1759,8 +1904,8 @@
     Env d i r s m -> Justification d i r s m -> ATMST s m ()
 debugNewNogoodStart cenv why = do
   liftIO $ putStr "Starting newNogood with "
-  debugEnv cenv
-  formatJustification why >>= (liftIO . putStrLn)
+  debug cenv
+  format why >>= (liftIO . putStrLn)
 
 
 -- Translated from @set-env-contradictory@ in @atms.lisp@.
@@ -1839,6 +1984,246 @@
 -- nodes, under each environment in the result at least one node of
 -- each sublist will be believed.
 --
+-- This function is for the case where no nodes are taken as defaults;
+-- here we simply call `interpretationsWithDefaults` with an empty
+-- list of defaults.
+interpretations ::
+  (Debuggable m, NodeDatum d) =>
+    ATMS d i r s m -> [[Node d i r s m]] -> ATMST s m [Env d i r s m]
+interpretations atms choiceSets = do
+  $(dbg [| do formatss' choiceSets >>=
+                liftIO . putStrLn . (++) "Called interpretations with "
+         |])
+  interpretationsWithDefaults atms choiceSets []
+
+-- |Initial setup for @interpretations@: convert the @choiceSets@ over
+-- `Node`s into structures over the nodes' labelling `Env`ironments,
+-- and set up the outermost loop.
+--
+-- Translated from these @interpretations@ in @atms.lisp@.
+--
+-- > (defun interpretations (atms choice-sets &optional defaults
+-- >                    &aux solutions)
+-- >   (let ( ;; ...
+-- >         (choice-sets (mapcar ;; Call to altSetToEnvList
+-- >                              choice-sets)))
+-- >     ;; First call interpsStartPrep for this loop
+-- >     (dolist (choice (car choice-sets))
+-- >       ;; ...
+-- >       )
+-- >     ;; Then continuation is afterDepthSolutions for
+-- >     ;; cleanup and extend-via-defaults.
+interpretationsWithDefaults ::
+  (Debuggable m, NodeDatum d) =>
+    ATMS d i r s m -> [[Node d i r s m]] -> [Node d i r s m] ->
+      ATMST s m [Env d i r s m]
+interpretationsWithDefaults atms choiceSets defaults = do
+  $(dbg [| do str <- formatss' choiceSets
+              liftIO $ putStr $ "- Refining choice sets " ++ str ++ "\n" |])
+  choiceSetEnvLists <- mapM (altSetToEnvList atms) choiceSets
+  $(dbg [| do liftIO $ putStrLn $ "  Refined choice sets to environment lists:"
+              formatss' choiceSetEnvLists >>=
+                (liftIO . putStrLn . (++) "    ") |])
+
+  let cntn = afterDepthSolutions atms choiceSetEnvLists defaults return
+  case choiceSetEnvLists of
+    [] -> cntn []
+    (cse:choiceSetEnvLists) ->
+      interpsForOneAlternative atms cse choiceSetEnvLists cntn []
+
+-- |Convert a `Node` passed in a choice-set of `interpretations` into
+-- the list of `Env`ironments in the label of that node.
+--
+-- Translated from the lambda expression of the @MAPCAR@ in this
+-- portion of @interpretations@ in @atms.lisp@:
+--
+-- >   (let ( ;; ...
+-- >         (choice-sets
+-- >           (mapcar #'(lambda (alt-set)
+-- >                       (format *trace-output*
+-- >                           "~%  - ~a --> ???" alt-set)
+-- >                       (let ((result
+-- >                              (mapcan #'(lambda (alt)
+-- >                                          (format *trace-output*
+-- >                                              "~%    - ~a --> ~a"
+-- >                                              alt (tms-node-label alt))
+-- >                                          (copy-list (tms-node-label alt)))
+-- >                                      alt-set)))
+-- >                         (format *trace-output*
+-- >                             "~%    ~a --> ~a" alt-set result)
+-- >                         result))
+-- >                   choice-sets)))
+altSetToEnvList ::
+  (Debuggable m, NodeDatum d) =>
+    ATMS d i r s m -> [Node d i r s m] -> ATMST s m [Env d i r s m]
+altSetToEnvList atms nodes = do
+  mapped <- mapM getNodeLabel nodes
+  $(dbg [| do s1 <- formats' nodes
+              s2 <- formatss' mapped
+              liftIO $ putStrLn $ "  - " ++ s1 ++ " --> " ++ s2 |])
+  return $ foldl (++) [] mapped
+
+-- |The body of @interpretations@ is translated from the Lisp in a
+-- continuation-passing style; this type is a shorthand for the common
+-- last two argument and result types of the continuation-processing
+-- functions.
+type ChoiceSetCntn d i r s m =
+  ([Env d i r s m] -> ATMST s m [Env d i r s m]) ->
+    [Env d i r s m] ->
+      ATMST s m [Env d i r s m]
+
+-- Control, and one pass through the body, of the loop in
+-- @interpretations@ (in file @atms.lisp@) in the context:
+--
+-- > (defun interpretations (atms choice-sets &optional defaults
+-- >                              &aux solutions)
+-- >   ...
+-- >   (let ((*solutions* nil)
+-- >         (choice-sets ...))
+-- >     (dolist (choice (car choice-sets)) ;; This loop
+--
+-- Aside from debugging tracing, the body of the loop just calls
+-- @getDepthSolutions@ for the first element of the list of choice
+-- sets.  The continuation of the @getDepthSolutions@ call is a
+-- recursive call to this function on the remainder of the choice sets
+-- list.
+interpsForOneAlternative ::
+  (Debuggable m, NodeDatum d) =>
+    ATMS d i r s m -> [Env d i r s m] -> [[Env d i r s m]] ->
+      ChoiceSetCntn d i r s m
+interpsForOneAlternative atms [] choiceSetEnvLists k solutions = do
+  $(dbg [| liftIO $ putStrLn "- Completed calls to getDepthSolutions" |])
+  k solutions
+interpsForOneAlternative atms (env : envs) choiceSetEnvLists k solutions = do
+  getDepthSolutions atms env choiceSetEnvLists
+                    (interpsForOneAlternative atms envs choiceSetEnvLists k)
+                    solutions
+
+-- |Translation of @get-depth-solutions1@.  This function operates a
+-- depth-first traversal over possible solutions.  Each choice set in
+-- the @choice-sets@ argument could contribute @N@ different possible
+-- next-steps to building a solution; the original Lisp function
+-- contains multiple self-recursive calls, one for each of these
+-- possible steps.  At the end of a sequence of recursive calls, one
+-- construction step per choice set, the base case received a
+-- constructed candidate solution.  The base case considers adding a
+-- to a global list of found solutions, possibly removing previous
+-- solution elements made redundant by the new solution.
+--
+-- The translation, like the rest of the translation of
+-- @interpretations@, is in continuation-passing style.  Rather than a
+-- global variable of solutions, the continuation receives the
+-- solutions-to-date-list as its final argument.  Rather than multiple
+-- recursive calls which might mutate a global list, there are
+-- extensions of the continuation which might manipulate the solutions
+-- list they are eventually passed.  The test of a constructed
+-- candidate still occurs when the search reaches a leaf at a fully
+-- constructed candidate, and calls its continuation with its
+-- transformation of the solutions list.
+--
+-- > ;; In atms.lisp
+-- > (defun get-depth-solutions1 (solution choice-sets &aux new-solution)
+-- >   (cond
+-- >     ((null choice-sets)
+-- >      (unless (do ((old-solutions *solutions* (cdr old-solutions)))
+-- >                  ((null old-solutions))
+-- >                (when (car old-solutions)
+-- >                  (case (compare-env (car old-solutions) solution)
+-- >                    ((:EQ :S12) (return t))
+-- >                    (:S21 (rplaca old-solutions nil)))))
+-- >        (push solution *solutions*)))
+-- >     ((env-nogood? solution)) ;something died.
+-- >     (t (dolist (choice (car choice-sets))
+-- >          (setq new-solution (union-env solution choice))
+-- >          (unless (env-nogood? new-solution)
+-- >            (get-depth-solutions1 new-solution (cdr choice-sets)))))))
+getDepthSolutions ::
+  (Debuggable m, NodeDatum d) =>
+    ATMS d i r s m -> Env d i r s m -> [[Env d i r s m]] ->
+      ChoiceSetCntn d i r s m
+getDepthSolutions atms cand [] k solns = do
+  $(dbg [| formats' solns >>=
+             liftIO . putStrLn . (++) "    getDepthSolutions => "
+         |])
+  let filtered = filterWithNewSoln cand solns
+  $(dbg [| formats' filtered >>= liftIO . putStrLn . (++) "    filtered "
+         |])
+  k filtered
+getDepthSolutions atms partial (cs : css) k solns = do
+  $(dbg [| do format partial >>= liftIO . putStrLn .
+                (++) "- Calling getDepthSolutions with partial solution "
+              formats' cs >>= liftIO . putStrLn . (++) "    choice sets "
+              formats' solns >>= liftIO . putStrLn . (++) "    initial solns "
+         |])
+  getDepthSolutionsFor atms partial cs css k solns
+
+-- |One pass through the body of the @getDepthSolutions$ loop.
+getDepthSolutionsFor ::
+  (Debuggable m, NodeDatum d) =>
+    ATMS d i r s m -> Env d i r s m -> [Env d i r s m] -> [[Env d i r s m]] ->
+      ChoiceSetCntn d i r s m
+getDepthSolutionsFor atms    _    []      _  k solns = do
+  $(dbg [| formats' solns >>=
+             liftIO . putStrLn . (++) "    getDepthSolutionsFor => " |])
+  k solns
+getDepthSolutionsFor atms partial (c:cs) css k solns = do
+  $(dbg [| do format c >>= liftIO . putStrLn .
+                (++) "- Calling getDepthSolutionsFor with first choice "
+              formats' cs >>= liftIO . putStrLn . (++) "    other choices "
+              formatss' css >>=
+                liftIO . putStrLn . (++) "    other choice sets "
+              formats' solns >>= liftIO . putStrLn . (++) "    initial solns "
+         |])
+  let k' = getDepthSolutionsFor atms partial cs css k
+           -- To try the next alternative of this choice set
+  newPartial <- unionEnv partial c
+  ifM (envIsNogood newPartial)
+      (do ($(dbg [| do format newPartial >>= liftIO . putStrLn .
+                         (++) "    nogood from unionEnv "
+                  |]))
+          k' solns)
+      (do ($(dbg [| do format partial >>= liftIO . putStrLn .
+                         (++) "    continuing with "
+                  |]))
+          (getDepthSolutions atms newPartial css k' solns))
+
+-- |Implementation of the list manipulation achieved in the DO-loop at:
+--
+-- > ;; In atms.lisp
+-- > (defun get-depth-solutions1 (solution choice-sets &aux new-solution)
+-- >   (cond
+-- >     ((null choice-sets)
+-- >      (unless (do ((old-solutions *solutions* (cdr old-solutions)))
+-- >                  ((null old-solutions))
+--
+-- The purpose is to add a new solution to a list of solutions.  But
+-- first the solution must be tested against existing solution to find
+-- cases where the new one is nondisjoint from some old one(s).  If
+-- the new solution is smaller than an old, then the old is redundant
+-- and should be pruned.  If the old solution is a subset of the new
+-- solution, then the new one is redundant and need not be added to
+-- the solutions list at all.
+filterWithNewSoln ::
+  (Monad m, NodeDatum d) => Env d i r s m -> [Env d i r s m] -> [Env d i r s m]
+filterWithNewSoln env envs =
+  let (redundant, _, envs') = filterWithNewSoln' env envs
+  in if redundant then envs' else env : envs'
+
+filterWithNewSoln' ::
+  (Monad m, NodeDatum d) => Env d i r s m -> [Env d i r s m] ->
+    (Bool, Bool, [Env d i r s m])
+filterWithNewSoln' _ [] = (False, False, [])
+filterWithNewSoln' e solns@(s:ss) =
+  case compareEnv s e of
+    EQenv -> (True, False, solns)
+    S12env -> (True, False, solns)
+    S21env -> let (r, c, ss') = filterWithNewSoln' e ss
+              in (r, True, ss')
+    DisjEnv -> let (r, c, ss') = filterWithNewSoln' e ss
+               in if c
+                  then (r, c, s:ss')
+                  else (r, c, solns)
+
 -- TO BE TRANSLATED from @interpretations@ in @atms.lisp@.
 --
 -- > ;; In atms.lisp
@@ -1883,33 +2268,36 @@
 -- >       (dolist (solution solutions)
 -- >    (extend-via-defaults solution defaults defaults)))
 -- >     (delete nil *solutions* :TEST #'eq)))
-interpretations ::
-  (Monad m, NodeDatum d) => ATMS d i r s m -> [[Node d i r s m]] -> ATMST s m ()
-interpretations = error "< TODO unimplemented interpretations >"
 
--- |TO BE TRANSLATED from @get-depth-solutions1@ in @atms.lisp@.
---
--- > ;; In atms.lisp
--- > (defun get-depth-solutions1 (solution choice-sets
--- >                                  &aux new-solution)
--- >   (cond ((null choice-sets)
--- >     (unless (do ((old-solutions *solutions* (cdr old-solutions)))
--- >                 ((null old-solutions))
--- >               (when (car old-solutions)
--- >                 (case (compare-env (car old-solutions) solution)
--- >                   ((:EQ :S12) (return t))
--- >                   (:S21 (rplaca old-solutions nil)))))
--- >       (push solution *solutions*)))
--- >    ((env-nogood? solution)) ;something died.
--- >    (t (dolist (choice (car choice-sets))
--- >         (setq new-solution (union-env solution choice))
--- >         (unless (env-nogood? new-solution)
--- >           (get-depth-solutions1 new-solution
--- >                                 (cdr choice-sets)))))))
-getDepthSolutions1 ::
-  (Monad m, NodeDatum d) => Env d i r s m -> [[Env d i r s m]] -> ATMST s m ()
-getDepthSolutions1 = error "< TODO unimplemented getDepthSolutions1 >"
+afterDepthSolutions ::
+  (Debuggable m, NodeDatum d) =>
+    ATMS d i r s m -> [[Env d i r s m]] -> [Node d i r s m] ->
+      ChoiceSetCntn d i r s m
+afterDepthSolutions atms choiceSets defaults k solutions =
+  if (null solutions)
+  then if (null choiceSets)
+       then do
+         empty <- getEmptyEnvironment atms
+         extendSolutionsIfDefaults atms defaults k [empty]
+       else return []
+  else extendSolutionsIfDefaults atms defaults k solutions
 
+extendSolutionsIfDefaults ::
+  (Debuggable m, NodeDatum d) =>
+    ATMS d i r s m -> [Node d i r s m] -> ChoiceSetCntn d i r s m
+extendSolutionsIfDefaults atms [] k solns = k solns
+extendSolutionsIfDefaults atms defaults k solns =
+  extendSolutionsViaDefaults atms solns defaults k []
+
+extendSolutionsViaDefaults ::
+  (Debuggable m, NodeDatum d) =>
+    ATMS d i r s m -> [Env d i r s m] -> [Node d i r s m] ->
+      ChoiceSetCntn d i r s m
+extendSolutionsViaDefaults atms [] defaults k = k
+extendSolutionsViaDefaults atms (s:ss) defaults k =
+  extendViaDefaults atms s defaults defaults
+                    (extendSolutionsViaDefaults atms ss defaults k)
+
 -- |TO BE TRANSLATED from @extend-via-defaults@ in @atms.lisp@.
 --
 -- > ;; In atms.lisp
@@ -1928,10 +2316,44 @@
 -- >     (unless (env-nogood? new-solution)
 -- >       (extend-via-defaults new-solution (cdr defaults) original))))
 extendViaDefaults ::
-  (Monad m, NodeDatum d) =>
-    Env d i r s m -> [Node d i r s m] -> [Node d i r s m] -> ATMST s m ()
-extendViaDefaults = error "< TODO unimplemented extendViaDefaults >"
+  (Debuggable m, NodeDatum d) =>
+    ATMS d i r s m -> Env d i r s m -> [Node d i r s m] -> [Node d i r s m] ->
+      ChoiceSetCntn d i r s m
+extendViaDefaults atms baseSoln remaining original k solutions =
+  extendViaDefaultsLoop atms baseSoln remaining original k solutions
 
+extendViaDefaultsLoop ::
+  (Debuggable m, NodeDatum d) =>
+    ATMS d i r s m -> Env d i r s m -> [Node d i r s m] -> [Node d i r s m] ->
+      ChoiceSetCntn d i r s m
+extendViaDefaultsLoop atms candSoln [] original k solutions = do
+
+  --  TODO Check (member solution *solutions* :TEST #'eq)
+  --
+
+  checkExtendedSoln atms candSoln original k solutions
+extendViaDefaultsLoop atms baseSoln (d:ds) original k solutions = do
+  newSoln <- consEnv d baseSoln
+  let nextLoop = extendViaDefaultsLoop atms baseSoln ds original k
+  ifM (envIsNogood newSoln)
+    (nextLoop solutions)
+    (extendViaDefaultsLoop atms newSoln ds original nextLoop solutions)
+
+checkExtendedSoln ::
+  (Debuggable m, NodeDatum d) =>
+    ATMS d i r s m -> Env d i r s m -> [Node d i r s m] ->
+      ChoiceSetCntn d i r s m
+checkExtendedSoln atms candSoln [] k solutions = k $ candSoln : solutions
+checkExtendedSoln atms candSoln (orig:origs) k solutions =
+  if (elem orig (envAssumptions candSoln))
+  then k solutions
+  else do
+    allEnv <- consEnv orig candSoln
+    ifM (envIsNogood allEnv)
+        (k solutions)
+        (checkExtendedSoln atms candSoln origs k solutions)
+
+
 -- * Generating explanations
 
 -- |This function returns a list of justifications which form a
@@ -2003,12 +2425,13 @@
 -- >   (format t "~% For ~A:" (node-string node))
 -- >   (dolist (j (tms-node-justs node))
 -- >     (print-justification j stream)))
-nodeJustifications :: (MonadIO m, NodeDatum d) => Node d i r s m -> ATMST s m ()
+nodeJustifications ::
+  (MonadIO m, NodeDatum d) => Node d i r s m -> ATMST s m ()
 nodeJustifications node = do
   nodeStr <- nodeString node
   liftIO $ putStr $ " For " ++ nodeStr ++ ":"
   justs <- getNodeJusts node
-  forM_ justs printJustification
+  forM_ justs pprint
 
 -- |Retrieve an `ATMS`'s `Env`ironment with the given index number.
 --
@@ -2025,15 +2448,6 @@
   table <- getEnvTable atms
   findInEnvTable (\env -> envIndex env == i) table
 
--- |Print an environment.
---
--- Translated from @print-env@ in @atms.lisp@.
-printEnv :: (MonadIO m, NodeDatum d) => Env d i r s m -> ATMST s m ()
-printEnv env = do
-  whenM (envIsNogood env) $ liftIO $ putStr "* "
-  envString env
-  liftIO $ putStrLn ""
-
 -- |Convert an `Env`ironment into a string listing the nodes of the
 -- environment.
 --
@@ -2051,22 +2465,13 @@
 --
 -- Translated from @print-nogoods@ in @atms.lisp@.
 printNogoods :: (MonadIO m, NodeDatum d) => ATMS d i r s m -> ATMST s m ()
-printNogoods atms = getNogoodTable atms >>= \table -> printEnvTable table
+printNogoods atms = getNogoodTable atms >>= \table -> pprint table
 
 -- |Print the `Env`ironments of an `ATMS`.
 --
 -- Translated from @print-envs@ in @atms.lisp@.
 printEnvs :: (MonadIO m, NodeDatum d) => ATMS d i r s m -> ATMST s m ()
-printEnvs atms = getEnvTable atms >>= \table -> printEnvTable table
-
--- |Print the `Env`ironments contained in the given `EnvTable`.
---
--- Translated from @print-env-table@ in @atms.lisp@.
-printEnvTable :: (MonadIO m, NodeDatum d) => EnvTable d i r s m -> ATMST s m ()
-printEnvTable (EnvTable arr) = do
-  let (lo, hi) = boundsSTArray arr
-  forM_ [lo..hi] $ \i ->
-    forMM_ (sttLayer $ readSTArray arr i) printEnv
+printEnvs atms = getEnvTable atms >>= \table -> pprint table
 
 -- |Print statistics about an `ATMS`.
 --
@@ -2079,201 +2484,49 @@
   liftIO $ putStrLn $ "Nogood table: "
   printNogoods atms
 
--- |Print the entries of an `EnvTable`.
---
--- Translated from @print-table@ in @atms.lisp@.
-printTable ::
-  (MonadIO m, NodeDatum d) => String -> EnvTable d i r s m -> ATMST s m ()
-printTable msg (EnvTable arr) = do
-  liftIO $ putStr msg
-  let (lo, hi) = boundsSTArray arr
-  forM_ [lo..hi] $ \i -> do
-    row <- sttLayer $ readSTArray arr i
-    let count = length row
-    when (count > 0) $
-      liftIO $ putStrLn $ "  " ++ show count ++ " of length " ++ show i
-
--- |Give a verbose printout of an `ATMS`.
---
-debugAtms ::
-  (MonadIO m, NodeDatum d) => String -> ATMS d i r s m -> ATMST s m ()
-debugAtms blurb atms = do
-  liftIO $ putStrLn $ "=============== " ++ atmsTitle atms ++ ": " ++ blurb
-  debugNodes atms
-  debugJusts atms
-  debugAtmsEnvs atms
-  debugNogoods atms
-  liftIO $ putStrLn "=============== "
-
 -- |Give a verbose printout of the `Node`s of an `ATMS`.
---
 debugNodes :: (MonadIO m, NodeDatum d) => ATMS d i r s m -> ATMST s m ()
 debugNodes atms = do
   nodes <- getNodes atms
   liftIO $ putStrLn $ show (length nodes) ++ " nodes:"
-  forM_ (reverse nodes) debugNode
-
--- |Computation returning a one-line summary of one `Node` of an `ATMS`.
---
-formatNode :: (Monad m, NodeDatum d) => Node d i r s m -> ATMST s m String
-formatNode node = do
-  datumFmt <- getDatumString $ nodeATMS node
-  return $ datumFmt (nodeDatum node)
-
--- |Computation returning a one-line summary of the `Node`s of an
--- `ATMS`.
---
-formatNodes ::
-  (Monad m, NodeDatum d) => String -> [Node d i r s m] -> ATMST s m String
-formatNodes sep = formatList sep formatNode
-
--- |Computation returning a one-line summary of a list of lists of
--- `Node`s of an `ATMS`.
---
-formatNodeLists ::
-  (Monad m, NodeDatum d) => String -> [[Node d i r s m]] -> ATMST s m String
-formatNodeLists sep = formatList sep $ formatNodes ","
+  forM_ (reverse nodes) debug
 
 -- |Computation returning a one-line summary of the label of a `Node`
 -- of an `ATMS`.
---
 formatNodeLabel :: (Monad m, NodeDatum d) => Node d i r s m -> ATMST s m String
 formatNodeLabel node = do
   label <- getNodeLabel node
   case label of
     [] -> return "empty"
-    _ -> formatNodeLists ", " $ map envAssumptions label
-
--- |Print a short summary of a `Node` of an `ATMS`.
---
-blurbNode :: (MonadIO m, NodeDatum d) => Node d i r s m -> ATMST s m ()
-blurbNode node = formatNode node >>= liftIO . putStr
-
--- |Print a verbose summary of a `Node` of an `ATMS`.
---
--- Translated from @print-tms-node@ in @atms.lisp@.
-printNode :: (MonadIO m, NodeDatum d) => Node d i r s m -> ATMST s m ()
-printNode node = do
-  str <- nodeString node
-  liftIO $ putStr $ "<NODE: " ++ str ++ ">"
-
--- |Give a verbose printout of a `Node` of an `ATMS`.
---
-debugNode :: (MonadIO m, NodeDatum d) => Node d i r s m -> ATMST s m ()
-debugNode node = do
-  let atms = nodeATMS node
-  datumFmt <- getDatumString atms
-  informantFmt <- getInformantString atms
-  liftIO $ putStrLn $ "- " ++ datumFmt (nodeDatum node)
-
-  label <- getNodeLabel node
-  case label of
-    [] -> liftIO $ putStrLn "  Empty label"
-    [env] -> do
-      liftIO $ putStr "  Single environment label: "
-      debugEnv env
-    _ -> forM_ label $ \env -> do
-      liftIO $ putStrLn "  - "
-      debugEnv env
-
-  conseqs <- getNodeConsequences node
-  case conseqs of
-    [] -> liftIO $ putStrLn "  Antecedent to no justifications"
-    _ -> do
-      liftIO $ putStr "  Antecedent to:"
-      forM_ conseqs $ \ conseq -> do
-        liftIO $ putStr $ " " ++ informantFmt (justInformant conseq)
-      liftIO $ putStrLn ""
-
--- |Computation returning a one-line summary of the reason an `ATMS`
--- may believe a `Node`.
---
-formatJustification ::
-  (Monad m, NodeDatum d) => Justification d i r s m -> ATMST s m String
-formatJustification (ByRule j) = return $ "By rule " ++ show (justIndex j)
-formatJustification (ByAssumption n) = do
-  nodeFmt <- getNodeString (nodeATMS n)
-  return $ "By assumption " ++ nodeFmt n
-formatJustification ByContradiction = return "By contradiction"
-
+    _ -> formatss "<none>" "; " "<none>" "," $ map envAssumptions label
 
 -- |Give a verbose printout of the `Just`ification rules of an
 -- `ATMS`.
---
 debugJusts :: (MonadIO m, NodeDatum d) => ATMS d i r s m -> ATMST s m ()
 debugJusts atms = do
   justs <- getJusts atms
   let len = length justs
   liftIO $ putStrLn $ show len ++ " justification structure"
     ++ (if len == 1 then "" else "s") ++ ":"
-  forM_ (sortOn justIndex justs) $ debugJust
+  forM_ (sortOn justIndex justs) $ debug
 
 -- |Computation returning a one-line summary of the informant of a
 -- `Just`ification rule of an `ATMS`.
---
 formatJustInformant ::
   (Monad m, NodeDatum d) => JustRule d i r s m -> ATMST s m String
 formatJustInformant rule = do
   informantFmt <- getInformantString $ nodeATMS $ justConsequence rule
   return $ informantFmt $ justInformant rule
 
--- |Print a more verbose description of a `Just`ification rule of an
--- `ATMS`.
---
--- Translated from @print-just@ in @atms.lisp@.
-printJust :: (MonadIO m, NodeDatum d) => JustRule d i r s m -> ATMST s m ()
-printJust rule = do
-  infStr <- formatJustInformant rule
-  liftIO $ putStr $ "<" ++ infStr ++ " " ++ show (justIndex rule) ++ ">"
-
--- |Print a more verbose description of the `Justification`.
-printJustification ::
-  (MonadIO m, NodeDatum d) => Justification d i r s m -> ATMST s m ()
-printJustification j = case j of
-  ByRule rule -> printJust rule
-  ByAssumption node -> do
-    liftIO $ putStr $ "Assumed node "
-    printNode node
-  ByContradiction -> liftIO $ putStrLn $ "By contradiction"
-
--- |Give a verbose printout of one `Just`ification rule of an `ATMS`.
---
-debugJust :: (MonadIO m, NodeDatum d) => JustRule d i r s m -> ATMST s m ()
-debugJust (JustRule idx inf conseq ants) = do
-  let atms = nodeATMS conseq
-  informantFmt <- getInformantString atms
-  datumFmt <- getDatumString atms
-  liftIO $ putStrLn $ "  "
-    ++ "[" ++ informantFmt inf ++ "." ++ show idx ++ "] "
-    ++ datumFmt (nodeDatum conseq) ++ " <= "
-    ++ intercalate ", " (map (datumFmt . nodeDatum) ants)
-
 -- |Give a verbose printout of the `Env`ironments of an `ATMS`.
---
 debugAtmsEnvs :: (MonadIO m, NodeDatum d) => ATMS d i r s m -> ATMST s m ()
 debugAtmsEnvs atms = do
   liftIO $ putStrLn "Environments:"
   envTable <- getEnvTable atms
   debugEnvTable atms envTable
 
--- |Give a verbose printout of one `Env`ironment of an `ATMS`.
---
-debugEnv :: (MonadIO m, NodeDatum d) => Env d i r s m -> ATMST s m ()
-debugEnv env = do
-  isNogood <- envIsNogood env
-  case envAssumptions env of
-    [] -> liftIO $ putStrLn "<empty>"
-    nodes @ (n : _) -> do
-      let atms = nodeATMS n
-      datumFmt <- getDatumString atms
-      when isNogood $ liftIO $ putStr "[X] "
-      liftIO $ putStrLn $
-        (intercalate ", " $ map (datumFmt . nodeDatum) nodes)
-        ++ " (count " ++ show (length nodes) ++ ")"
-
 -- |Print a short summary of a mutable list of nullable (via `Maybe`)
 -- `Env`ironments from an `ATMS`.
---
 blurbMaybeEnvMList ::
   (MonadIO m, NodeDatum d) => MList s (Maybe (Env d i r s m)) -> ATMST s m ()
 blurbMaybeEnvMList mlist = do
@@ -2290,7 +2543,6 @@
 
 -- |Print a short summary of a reference to a mutable list of
 -- nullable (via `Maybe`) `Env`ironments from an `ATMS`.
---
 blurbMaybeEnvMListRef ::
   (MonadIO m, NodeDatum d) =>
     STRef s (MList s (Maybe (Env d i r s m))) -> ATMST s m ()
@@ -2300,7 +2552,6 @@
 
 -- |Print a short summary of a nullable (via `Maybe`) reference to an
 -- `Env`ironment of an `ATMS`.
---
 blurbMaybeEnv ::
   (MonadIO m, NodeDatum d) => Maybe (Env d i r s m) -> ATMST s m ()
 blurbMaybeEnv envm = case envm of
@@ -2308,7 +2559,6 @@
                        Nothing -> liftIO $ putStr "<nothing>"
 
 -- |Print a short summary of one `Env`ironment of an `ATMS`.
---
 blurbEnv :: (MonadIO m, NodeDatum d) => Env d i r s m -> ATMST s m ()
 blurbEnv env = do
   wng <- sttLayer $ readSTRef $ envWhyNogood env
@@ -2324,7 +2574,6 @@
 
 -- |Give a verbose printout of the no-good `Env`ironments of an
 -- `ATMS`.
---
 debugNogoods :: (MonadIO m, NodeDatum d) => ATMS d i r s m -> ATMST s m ()
 debugNogoods atms = do
   liftIO $ putStrLn "No-good environments:"
@@ -2333,7 +2582,6 @@
 
 -- |Give a verbose printout of the `Env`ironments of an `EnvTable` of
 -- an `ATMS`.
---
 debugEnvTable ::
   (MonadIO m, NodeDatum d) =>
     ATMS d i r s m -> EnvTable d i r s m -> ATMST s m ()
@@ -2343,36 +2591,33 @@
     envs <- sttLayer $ readSTArray array i
     forM_ (reverse envs) $ \ env -> do
       liftIO $ putStr "- "
-      debugEnv env
+      debug env
 
 {-
 -- |Print a short summary of the label of a `Node` of an `ATMS`.
---
 blurbNodeLabel ::
   (MonadIO m, NodeDatum d) => Node d i r s m -> ATMST s m String
 blurbNodeLabel node = do
   -- lbl <- getNodeLabel node
   lbl <- sttLayer $ readSTRef (nodeLabel node)
-  blurbNode node
+  blurb node
   liftIO $ putStr " label: "
   blurbEnvList 10000 "\n" lbl
   liftIO $ putStrLn ""
 -}
 
 -- |Give a verbose printout of the label of a `Node` of an `ATMS`.
---
 debugNodeLabel ::
   (MonadIO m, NodeDatum d) => Node d i r s m -> ATMST s m ()
 debugNodeLabel node = do
   -- lbl <- getNodeLabel node
   lbl <- sttLayer $ readSTRef (nodeLabel node)
-  blurbNode node
+  blurb node
   liftIO $ putStr " label: "
   blurbEnvList 10000 "\n" lbl
   liftIO $ putStrLn ""
 
 -- |Print a short summary of a list of `Env`ironments of an `ATMS`.
---
 blurbEnvList ::
   (MonadIO m, NodeDatum d) => Int -> String -> [Env d i r s m] -> ATMST s m ()
 blurbEnvList multiLineIf lineLead envs =
diff --git a/src/main/haskell/lib/Data/TMS/Formatters.hs b/src/main/haskell/lib/Data/TMS/Formatters.hs
new file mode 100644
--- /dev/null
+++ b/src/main/haskell/lib/Data/TMS/Formatters.hs
@@ -0,0 +1,128 @@
+{-|
+Module      : Formatters
+Description : Formatting functions, consistently named across the TMS modules
+Copyright   : (c) John Maraist, 2022
+License     : AllRightsReserved
+Maintainer  : haskell-tms@maraist.org
+Stability   : experimental
+Portability : POSIX
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
+implied, for NON-COMMERCIAL use.  See the License for the specific
+language governing permissions and limitations under the License.
+
+-}
+
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+
+module Data.TMS.Formatters where
+
+import Control.Monad
+import Control.Monad.State
+import Control.Monad.Extra
+import Data.List
+import Data.Maybe
+import Data.Foldable
+import Data.Traversable
+
+mapAndIntercalateM ::
+  (Monad m, Traversable t) => (a -> m String) -> String -> t a -> m String
+mapAndIntercalateM f sep xs = do
+  ys <- mapM f xs
+  return $ foldl1 (\s1 s2 -> s1 ++ sep ++ s2) ys
+
+-- |Class of artifacts which can be given a short formatted
+-- description in a particular monad.
+--
+-- This is a multi-parameter class: the first argument is the artifact
+-- type; the second, the monad.  Both type constructors take two
+-- arguments, the state thread type used by the TMS thread, and the
+-- enclosed monad constructor.
+class Formatted item tmsMonad where
+  -- |Format a single artifact.
+  format :: (Monad m) => item s m -> tmsMonad s m String
+
+  -- |Format several artifacts, with the given string between each
+  -- pair.
+  formats ::
+    (Monad m, Monad (tmsMonad s m), Traversable k) =>
+      String -> String -> k (item s m) -> tmsMonad s m String
+  formats none _ xs | null xs = return none
+  formats _ sep xs = mapAndIntercalateM format sep xs
+
+  -- |Format several artifacts with the default separator.
+  formats' ::
+    (Monad m, Monad (tmsMonad s m), Traversable k) =>
+      k (item s m) -> tmsMonad s m String
+  formats' = formats "<none>" ","
+
+  -- |Format several collections of artifacts, with the given string
+  -- between each pair of collections, and a comma between each pair
+  -- of artifacts.
+  formatss ::
+    (Monad m, Monad (tmsMonad s m), Traversable k1, Traversable k2) =>
+      String -> String -> String -> String -> k1 (k2 (item s m)) ->
+        tmsMonad s m String
+  formatss outNone _ _ _ xs | null xs = return outNone
+  formatss outNone outSep inNone inSep xs =
+    mapAndIntercalateM (formats inNone inSep) outSep xs
+
+  -- |Format several collections of artifacts with the default
+  -- separators.
+  formatss' ::
+    (Monad m, Monad (tmsMonad s m), Traversable k) =>
+      k (k (item s m)) -> tmsMonad s m String
+  formatss' = formatss "<none>" "; " "<none>" ","
+
+  -- |Print a short representation of an artifact to the standard
+  -- output.
+  blurb :: (MonadIO m, MonadIO (tmsMonad s m)) => item s m -> tmsMonad s m ()
+  blurb i = format i >>= liftIO . putStr
+
+  -- |Print a short representation of a collection of artifacts to the
+  -- standard output.
+  blurbs ::
+    (MonadIO m, MonadIO (tmsMonad s m), Traversable k) =>
+      String -> String -> k (item s m) -> tmsMonad s m ()
+  blurbs none sep xs = formats none sep xs >>= liftIO . putStr
+
+  -- |Print a short representation of a collection of collections of
+  -- artifacts to the standard output.
+  blurbss ::
+    (MonadIO m, MonadIO (tmsMonad s m), Traversable k1, Traversable k2) =>
+      String -> String -> String -> String ->
+        k1 (k2 (item s m)) -> tmsMonad s m ()
+  blurbss outNone outSep inNone inSep xs =
+    formatss outNone outSep inNone inSep xs >>= liftIO . putStr
+
+-- |Class of artifacts which can be printed in a `MonadIO` to the
+-- standard output, possibly over multiple lines, but in a terse
+-- representation shorter than for debugging.
+--
+-- This is a multi-parameter class: the first argument is the artifact
+-- type; the second, the monad.  Both type constructors take two
+-- arguments, the state thread type used by the TMS thread, and the
+-- enclosed monad constructor.
+class Printed item tmsMonad where
+  pprint :: (MonadIO m) => item s m -> tmsMonad s m ()
+
+  pprints ::
+    (MonadIO m, MonadIO (tmsMonad s m)) => [item s m] -> tmsMonad s m ()
+  pprints items = forM_ items $ \i -> pprint i
+
+  pprintss ::
+    (MonadIO m, MonadIO (tmsMonad s m)) => [[item s m]] -> tmsMonad s m ()
+  pprintss itemss = forM_ itemss $ \i -> pprints i
+
+-- |Class of artifacts which can be printed for the purpose of
+-- debugging in a `MonadIO` to the standard output.
+--
+-- This is a multi-parameter class: the first argument is the artifact
+-- type; the second, the monad.  Both type constructors take two
+-- arguments, the state thread type used by the TMS thread, and the
+-- enclosed monad constructor.
+class Debugged item tmsMonad where
+  debug :: (MonadIO m) => item s m -> tmsMonad s m ()
diff --git a/src/main/haskell/prof/ATMSTrun.hs b/src/main/haskell/prof/ATMSTrun.hs
new file mode 100644
--- /dev/null
+++ b/src/main/haskell/prof/ATMSTrun.hs
@@ -0,0 +1,38 @@
+module ATMSTrun where
+
+import Control.Monad.State
+import Data.Symbol
+import Data.TMS.Formatters
+import Data.TMS.ATMS.ATMST
+
+runATMS1 :: IO (Either AtmsErr ())
+runATMS1 = do
+  runATMST $ do
+    atms <- createATMS "Ex1"
+    setInformantStringViaString atms
+    setDatumStringViaString atms
+    -- debugAtms "Created" atms
+    na <- createNode atms "A" True False
+    -- debugAtms "Added assumption node A" atms
+    nc <- createNode atms "C" True False
+    -- debugAtms "Added assumption node C" atms
+    ne <- createNode atms "E" True False
+    -- debugAtms "Added assumption node E" atms
+    nh <- createNode atms "H" False False
+    -- debugAtms "Added non-assumption node H" atms
+    justifyNode "R1" nh [nc, ne]
+    -- debugAtms "After rule R1" atms
+    ng <- createNode atms "G" False False
+    -- debugAtms "After non-assumption node G" atms
+    justifyNode "R2" ng [na, nc]
+    -- debugAtms "After rule R2" atms
+    nx <- createNode atms "X" False True
+    -- debugAtms "After contradiction node X" atms
+    justifyNode "R3" nx [ng]
+    -- debugAtms "After rule R3" atms
+    nb <- createNode atms "B" True False
+    liftIO $ putStrLn "Added assumption node B"
+    debug atms
+    justifyNode "R4" nh [nb, nc]
+    liftIO $ putStrLn "After rule R4"
+    debug atms
diff --git a/src/main/haskell/prof/JTMSrun.hs b/src/main/haskell/prof/JTMSrun.hs
new file mode 100644
--- /dev/null
+++ b/src/main/haskell/prof/JTMSrun.hs
@@ -0,0 +1,14 @@
+module JTMSrun where
+
+import Data.Symbol
+import Data.TMS.JTMS
+import Control.Monad.IO.Class
+
+runJTMS1 :: IO (Either JtmsErr ())
+runJTMS1 = runJTMST $ do
+  j <- createJTMS "Ex1"
+  na <- createNode j (intern "a") True False
+  naName <- nodeString na
+  naIn <- isInNode na
+  liftIO $ putStrLn $
+    "Node " ++ naName ++ " is " ++ if naIn then "in" else "out"
diff --git a/src/main/haskell/prof/Main.hs b/src/main/haskell/prof/Main.hs
new file mode 100644
--- /dev/null
+++ b/src/main/haskell/prof/Main.hs
@@ -0,0 +1,87 @@
+{-# LANGUAGE RankNTypes #-}
+
+module Main where
+
+import ATMSTrun
+import JTMSrun
+import Control.Monad.Random
+import Control.Monad.Random.Class
+import Data.TMS.ATMS.ATMST
+
+main :: IO ()
+main = do
+  -- gen <- getStdGen
+  let gen = mkStdGen 8675309 --- Fix for comparing like to like
+  evalRandT (runATMST $
+              makeForceATMS
+                (IntRange 800 810) (IntRange 4000 4010)
+                0.1
+                (IntRange 50 60) (IntRange 25 30)
+                False) gen
+  return ()
+
+intSet :: (RandomGen g, Monad m) => Int -> Int -> RandT g m [Int]
+intSet 0 _ = return []
+intSet n m = do
+  x <- getRandomR (0, m)
+  xs <- intSet (n - 1) m
+  return $ x : xs
+
+intSetExcept :: (RandomGen g, Monad m) => Int -> Int -> Int -> RandT g m [Int]
+intSetExcept 0 _ _ = return []
+intSetExcept n m d = do
+  x <- getRandomR (0, m)
+  if (x == d) then intSetExcept n m d else do
+    xs <- intSetExcept (n - 1) m d
+    return $ x : xs
+
+data IntRange = IntRange { lo :: Int, hi :: Int }
+
+sample :: (RandomGen g, Monad m) => IntRange -> RandT g m Int
+sample (IntRange lo hi) = getRandomR (lo, hi)
+
+coinFlip :: (RandomGen g, Monad m) => Double -> RandT g m Bool
+coinFlip p = do
+  q <- getRandomR (0.0, 1.0)
+  return $ q <= p
+
+makeForceATMS ::
+  (RandomGen g, MonadIO m) =>
+    IntRange -> IntRange -> Double -> IntRange -> IntRange -> Bool ->
+      ATMST s (RandT g m) ()
+makeForceATMS assumptionsRange nonassumptionsRange contradictionChance
+              justificationsPerConclusion antecedentsPerJustifications
+              cyclic = do
+
+  atms <- createATMS "Random ATMS"
+  setDatumStringViaString atms
+  setInformantStringViaString atms
+  assumptions <- lift $ sample assumptionsRange
+  nonassumptions <- lift $ sample nonassumptionsRange
+  let totalNodes = assumptions + nonassumptions
+
+  assumptionNodes <- forM [0 .. assumptions - 1] $ \i ->
+    createNode atms ("Node-" ++ show i) True False
+
+  nonassumptionNodes <- forM [0 .. nonassumptions - 1] $ \i -> do
+    isContradiction <- lift $ coinFlip contradictionChance
+    let idx = assumptions + i
+    createNode atms ("Node-" ++ show idx) False isContradiction
+
+  let nodes = assumptionNodes ++ nonassumptionNodes
+
+  {-# SCC "mainLoop" #-} forM_ [0 .. nonassumptions - 1] $ \i -> do
+    let idx = assumptions + i
+    let node = nodes !! idx
+    justifications <- lift $ sample justificationsPerConclusion
+    -- lift $ lift $ liftIO $ putStrLn $
+    --   show justifications ++ " justifications for node " ++ show idx
+    forM_ [0 .. justifications - 1] $ \j -> do
+      thisSize <- lift $ sample antecedentsPerJustifications
+      antsIdx <- lift $ if cyclic
+        then intSet thisSize $ idx - 1
+        else intSetExcept thisSize (totalNodes - 1) j
+      let ants = map (nodes !!) antsIdx
+      {-# SCC "justCalls" #-} justifyNode (show i ++ "." ++ show j) node ants
+    {-# SCC "forceLabel" #-} debugNodeLabel node
+
diff --git a/src/test/haskell/Testers.hs b/src/test/haskell/Testers.hs
--- a/src/test/haskell/Testers.hs
+++ b/src/test/haskell/Testers.hs
@@ -35,6 +35,7 @@
 import Data.Void
 import Data.TMS.ATMS.ATMST
 import Data.TMS.Helpers
+import Data.TMS.Formatters
 import Data.TMS.Dbg
 import Control.Monad
 import Control.Monad.Extra
@@ -109,7 +110,7 @@
     "Expect " ++ show (length nodeLists) ++ " environments" ~:
       length nodeLists @==- length labelNodeLists
     forM_ nodeLists $ \ nodeList -> do
-      nl <- formatNodes "," nodeList
+      nl <- formats "(no nodes)" "," nodeList
       "Should have environment with assumptions " ++ nl
         ~::- elem nodeList labelNodeLists