diff --git a/ChangeLog b/ChangeLog
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,59 @@
+2013-07-23  John D. Ramsdell  <ramsdell@mitre.org>
+
+        * cpsa.cabal (Version):  Tagged as version 2.3.0
+
+	* src/CPSA/Lib/*.hs:  Added priorities to help guide the search.
+
+	* src/CPSA/Lib/Protocol.hs (mkRole): Positions are now used to
+	specify non-origination introductions rather than heights.
+
+	* doc/cpsaspec.tex: Reverted back to zero-based indexing.
+
+	* doc/cpsauser.tex: Removed Diffie-Hellman documentation as the
+	implementation of the algebra continues to have serious issues.
+
+2013-07-22  John D. Ramsdell  <ramsdell@mitre.org>
+
+	* src/CPSA/Graph/Tree.hs (makeTree): Skeletons without children
+	that are not marked "empty cohort" are now counted as live.
+
+2013-06-13  John D. Ramsdell  <ramsdell@mitre.org>
+
+	* src/CPSA/Lib/Algebra.hs: Added isMesgVar for acquires check.
+
+	* src/CPSA/Lib/Strand.hs (thinStrand, thinManyStrands):  Added
+	transitive reduction before thinning.
+
+	* src/CPSA/*/Algebra.hs:  Removed support for GHC 6.x.
+
+2013-04-23  John D. Ramsdell  <ramsdell@mitre.org>
+
+	* src/prover9.pl: Removed erroneous quotes that were added to the
+	translation of constants.
+
+2013-04-10  John D. Ramsdell  <ramsdell@mitre.org>
+
+	* src/prover9.pl: Changed the formula translation algorithm so
+	that predicates for the sort declarations of variables are added
+	to generated formulas.  Previously, the sort information was
+	ignored.
+
+2013-03-29  John D. Ramsdell  <ramsdell@mitre.org>
+
+	* src/CPSA/DiffieHellman/Algebra.hs (mgu): Changed so function
+	performs substitutions on all vars on LHS, not just the ones not
+	that were originally on the LHS.
+
+2013-03-12  John D. Ramsdell  <ramsdell@mitre.org>
+
+	* src/CPSA/Annotations/Annotations.hs (obligation): Replaced an
+	irrefutable pattern that raised an exception with a maybeToList.
+
+2013-03-06  John D. Ramsdell  <ramsdell@mitre.org>
+
+	* src/CPSA/DiffieHellman/Algebra.hs (sLoad):  Added code that
+	allows testing of unification and matching in GHCi.
+
 2013-02-28  John D. Ramsdell  <ramsdell@mitre.org>
 
 	* doc/*.html:  Convert to HTML 5 mainly by eliminating the DOCTYPE
diff --git a/NEWS b/NEWS
--- a/NEWS
+++ b/NEWS
@@ -1,5 +1,23 @@
 CPSA NEWS -- history of user-visible changes.
 
+* Changes in version 2.3.0
+
+** Priorities for influencing search order added
+   The priority form in roles and skeletons allows the search to focus
+   on specific nodes of interest.
+
+** Role non-origination with position changed
+   A non-origination assumption of the form (3 a) now means the
+   assumption is add when the height of the strand is greater that 3.
+   It used to be added when the height of the strand is at least three.
+
+** Shape Analysis Sentence to Prover9 translator improved
+   Changed the formula translation algorithm so that predicates for
+   the sort declarations of variables are added to generated formulas.
+   Previously, the sort information was ignored.
+
+** Bug fixed in cpsaannotations
+
 * Changes in version 2.2.13
 
 ** Better support for Cygwin users
diff --git a/cpsa.cabal b/cpsa.cabal
--- a/cpsa.cabal
+++ b/cpsa.cabal
@@ -1,5 +1,5 @@
 Name:			cpsa
-Version:		2.2.13
+Version:		2.3.0
 Maintainer:		ramsdell@mitre.org
 Cabal-Version:		>= 1.6
 License:		BSD3
@@ -47,8 +47,7 @@
 Data-Files:
   index.html readme.html cpsauser.html cpsa.mk Make.hs cpsaprimer.pdf
   cpsaoverview.pdf cpsaintroslides.pdf cpsaspec.pdf cpsadesign.pdf
-  cpsadha.pdf ffgg.scm ns.scm blanchet.scm or.scm woolam.scm
-  yahalom.scm dhke.scm
+  ffgg.scm ns.scm blanchet.scm or.scm woolam.scm yahalom.scm
 Data-Dir:	    	doc
 Extra-Source-Files:
   Makefile ChangeLog README NEWS ghci cpsatst setup.bat
@@ -120,7 +119,7 @@
   Main-Is:		CPSA/Lib/Main.hs
   Build-Depends:	base >= 3 && < 5, containers, parallel, array
   GHC-Options:
-    -Wall -fno-warn-name-shadowing -fwarn-unused-imports -threaded
+    -Wall -fno-warn-name-shadowing -fwarn-unused-imports -threaded -rtsopts
   Hs-Source-Dirs:	src
   Other-Modules:
     Paths_cpsa CPSA.Lib.Vector CPSA.Lib.Utilities CPSA.Lib.Pretty
@@ -131,8 +130,6 @@
     CPSA.DiffieHellman.IntLinEq CPSA.SimpleDiffieHellman.Algebra
     CPSA.DiffieHellmanNoReciprocal.Algebra
     CPSA.DiffieHellmanNoReciprocal.LinDiophEq
-  if impl(ghc >= 7.0.0)
-    GHC-Options: -rtsopts
 
 Executable cpsagraph
   Main-Is:		CPSA/Graph/Main.hs
diff --git a/doc/Makefile b/doc/Makefile
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -14,7 +14,6 @@
 SLIDES = cpsaintroslides
 DESIGN = cpsadesign
 SPEC = cpsaspec
-DHA = cpsadha
 BIB = cpsa
 
 TEX_SRCS = macros.tex bcasyntax.tex
@@ -33,7 +32,7 @@
 	makeindex $*
 
 all:	$(PRIMER).pdf $(OVERVIEW).pdf $(SLIDES).pdf \
-		$(DESIGN).pdf $(SPEC).pdf $(DHA).pdf
+		$(DESIGN).pdf $(SPEC).pdf
 
 $(PRIMER).pdf:	$(MP_SRCS:.mp=-0.mps) $(TEX_SRCS) \
 		 $(PRIMER).tex $(PRIMER).bbl
@@ -60,12 +59,8 @@
 	if test -f $(SPEC).idx; then $(MAKE) $(SPEC).ind; fi
 	pdflatex $(SPEC).tex
 
-$(DHA).pdf: $(DHA).tex $(DHA).bbl
-	if test ! -f $(DHA).aux; then pdflatex $(DHA).tex; fi
-	pdflatex $(DHA).tex
-
 CLEAN_FILES := $(PRIMER).pdf $(OVERVIEW).pdf $(SLIDES).pdf \
-		$(DESIGN).pdf $(SPEC).pdf $(DHA).pdf \
+		$(DESIGN).pdf $(SPEC).pdf \
 	$(wildcard *.log *.aux *.toc *.mps *.mpx) \
 	$(wildcard *.bbl *.blg *.ind *.idx *.ilg *.out)
 
diff --git a/doc/cpsadesign.pdf b/doc/cpsadesign.pdf
Binary files a/doc/cpsadesign.pdf and b/doc/cpsadesign.pdf differ
diff --git a/doc/cpsadha.pdf b/doc/cpsadha.pdf
deleted file mode 100644
Binary files a/doc/cpsadha.pdf and /dev/null differ
diff --git a/doc/cpsaintroslides.pdf b/doc/cpsaintroslides.pdf
Binary files a/doc/cpsaintroslides.pdf and b/doc/cpsaintroslides.pdf differ
diff --git a/doc/cpsaoverview.pdf b/doc/cpsaoverview.pdf
Binary files a/doc/cpsaoverview.pdf and b/doc/cpsaoverview.pdf differ
diff --git a/doc/cpsaprimer.pdf b/doc/cpsaprimer.pdf
Binary files a/doc/cpsaprimer.pdf and b/doc/cpsaprimer.pdf differ
diff --git a/doc/cpsaspec.pdf b/doc/cpsaspec.pdf
Binary files a/doc/cpsaspec.pdf and b/doc/cpsaspec.pdf differ
diff --git a/doc/cpsaspec.tex b/doc/cpsaspec.tex
--- a/doc/cpsaspec.tex
+++ b/doc/cpsaspec.tex
@@ -156,10 +156,10 @@
 \section{Notation}\label{sec:notation}
 
 A finite sequence\index{sequence} is a function from an initial
-segment of the whole numbers.  The length of a sequence~$X$ is~$|X|$,
-and sequence~$X=\seq{X(1),\ldots,X(n)}$ for $n=|X|$.  Alternatively,
-$\seq{x_1,x_2,\ldots,x_n} =x_1\cons x_2\cons\ldots\cons
-x_n\cons\seq{}$.  If~$S$ is a set, then~$S^\ast$ is the set of finite
+segment of the natural numbers.  The length of a sequence~$X$ is~$|X|$,
+and sequence~$X=\seq{X(0),\ldots,X(n-1)}$ for $n=|X|$.  Alternatively,
+$\seq{x_0,x_1,\ldots,x_{n-1}} =x_0\cons x_1\cons\ldots\cons
+x_{n-1}\cons\seq{}$.  If~$S$ is a set, then~$S^\ast$ is the set of finite
 sequences of~$S$, and~$S^+$ is the non-empty finite sequences of~$S$.
 The concatenation of sequences~$X_0$ and~$X_1$ is~$X_0\append X_1$.
 The prefix of sequence~$X$ of length~$n$ is~$\prefix{X}{n}$.
@@ -317,15 +317,15 @@
 \alga_X\rightarrow\alga_Y$ induced by~$\sigma$ is also
 denoted~$\sigma$.
 
-A \index{position}\emph{position}~$p$ is a finite sequence of whole
+A \index{position}\emph{position}~$p$ is a finite sequence of natural
 numbers.  The term in~$t$ that \emph{occurs at}~$p$, written~$t\termat
 p$, is:
 $$\begin{array}{l}
 t\termat\seq{}=t;\\
-(t_1,t_2)\termat i\cons p=t_i\termat p\mbox{ for $i\in\{1,2\}$};\\
-\enc{t_1}{t_2}\termat i\cons p=t_i\termat p\mbox{ for
-  $i\in\{1,2\}$};\\
-t^{-1}\termat 1\cons p=t\termat p.
+(t_0,t_1)\termat i\cons p=t_i\termat p\mbox{ for $i\in\{0,1\}$};\\
+\enc{t_0}{t_1}\termat i\cons p=t_i\termat p\mbox{ for
+  $i\in\{0,1\}$};\\
+t^{-1}\termat 0\cons p=t\termat p.
 \end{array}$$
 A term~$t$ \index{occurs in}\emph{occurs in} term~$t'$ if $t=t'\termat
 p$ for some~$p$.  A message~$T$ \emph{occurs in} message~$T'$ if the
@@ -340,12 +340,12 @@
 $$\carpos(t,t')=\left\{
 \begin{array}{ll}
 \{\seq{}\}&\mbox{if $t'\equiv t$, else}\\
-\multicolumn{2}{l}{\{1\cons p \mid
+\multicolumn{2}{l}{\{0\cons p \mid
 p\in\carpos(t,t_1)\}}\\
-& \mbox{if $t'=\enc{t_1}{t_2}$, else}\\
+& \mbox{if $t'=\enc{t_0}{t_1}$, else}\\
 \multicolumn{2}{l}{\{i\cons p \mid
-i\in\{1,2\}, p\in\carpos(t,t_i)\}} \\
-& \mbox{if $t'=(t_1,t_2)$ else}\\
+i\in\{0,1\}, p\in\carpos(t,t_i)\}} \\
+& \mbox{if $t'=(t_0,t_1)$ else}\\
 \emptyset&\mbox{otherwise.}
 \end{array}\right.$$
 
@@ -400,13 +400,13 @@
 Message events occur at nodes in a strand space.  For each strand~$s$,
 there is a node for every event in~$\Theta(s)$.  The
 \index{nodes}\emph{nodes} of strand space $\Theta$ are $\{(s,i)\mid
-s\in\sdom(\Theta), 1\leq i\leq |\Theta(s)|\}$, the event at a node is
+s\in\sdom(\Theta), 0\leq i< |\Theta(s)|\}$, the event at a node is
 \index{evt@\evt}$\evt_\Theta(s,i)=\Theta(s)(i)$, and the message at a
 node is \index{msg@\msg}$\msg_\Theta(s,i) = m$ such that
 $\evt_\Theta(s,i) = \pm m$.  Just as a position names a subterm within
 another term, a strand names a trace within a strand space, and a node
 names an event in a strand space.  The relation~$\Rightarrow$ defined
-by $\{(s,i)\Rightarrow(s,i+1)\mid s\in\sdom(\Theta), 1\leq
+by $\{(s,i-1)\Rightarrow(s,i)\mid s\in\sdom(\Theta), 1\leq
 i<|\Theta(s)|\}$ is called the \index{strand succession}\emph{strand
   succession relation}.
 
@@ -460,7 +460,7 @@
 set of variables that occur in~$\prefix{C}{h}$, (4) if the variables
 in $t\in N$ occur in $\sdom(\sigma)$, then $\sigma(t)$ is
 non-originating in $\Upsilon(\Theta_X,\to)$, and (5) if $t\in U$
-originates at index~$i$ in~$C$, and $i\leq h$, then $\sigma(t)$
+originates at index~$i$ in~$C$, and $i<h$, then $\sigma(t)$
 uniquely originates in $\Upsilon(\Theta_X,\to)$ at node $(s,i)$.
 Origination assumptions in bundles specified by roles are called
 \index{inherited origination assumptions}\emph{inherited origination
@@ -687,7 +687,7 @@
 \seq{\inbnd\enc{\enc{s}{a^{-1}}}{b},\outbnd\enc{d}{s}}\rangle,
 \end{array}
 &\mbox{Traces}\\
-&\{(1,1)\prec(2,1),(2,2)\prec(1,2)\},
+&\{(0,0)\prec(1,0),(1,1)\prec(0,1)\},
 &\mbox{Node orderings}\\
 &\{a^{-1},b^{-1}\},
 &\mbox{Non-origination}\\
@@ -752,7 +752,7 @@
 \mbox{Traces}\\
 \mbox{\emph{Note key is $b'$ not $b$!}}
 \end{array}\\
-&\{(2,1)\prec(1,1)\},
+&\{(1,0)\prec(0,0)\},
 &\mbox{Node orderings}\\
 &\{a^{-1},b^{-1}\},
 &\mbox{Non-origination}\\
@@ -775,7 +775,7 @@
 \seq{\inbnd\enc{\enc{s}{a^{-1}}}{b},\outbnd\enc{d}{s}},
 \seq{\inbnd d,\outbnd d}},
 &\mbox{Traces}\\
-&\{(1,2)\prec(2,1),
+&\{(0,1)\prec(1,0),
 &\mbox{Node orderings}\\
 &\{a^{-1},b^{-1}\},
 &\mbox{Non-origination}\\
@@ -1143,7 +1143,7 @@
 Skeleton~$k_0$ reduces to skeleton~$k_1$ by pruning, written
 $k_0\reduction{\ops{P}_s}k_1$, iff there is a most general
 unifier~$\sigma$ such that $\sigma(\Theta_{k_0}(s)(j))\equiv
-\Theta_{k_0}(s')(j)$ for all $1\leq j\leq|\Theta_{k_0}(s)|$, no
+\Theta_{k_0}(s')(j)$ for all $0\leq j<|\Theta_{k_0}(s)|$, no
 variable in $\sdom(\sigma)$ occurs in the trace of any strand other
 than~$s$, $\sigma$ is a renaming, $t\in U_{k_0}$ implies $\sigma(t)\in
 U_{k_0}$, $t\in N_{k_0}$ implies $\sigma(t)\in N_{k_0}$, there is
@@ -1645,7 +1645,7 @@
 Suppose there are strands~$s$ and~$s'$, where one of them is the newly
 created strand, and a most general unifier~$\sigma'$ such that
 $\sigma'(\Theta_{k_1}(s)(j))\equiv \sigma'(\Theta_{k_1}(s')(j))$ for
-$1\leq j\leq|\Theta_{k_1}(s)|$.  Skeleton~$k_4$ is a
+$0\leq j<|\Theta_{k_1}(s)|$.  Skeleton~$k_4$ is a
 \index{displacement}\emph{displacement} if
 $k_1\reduction{\ops{S}_{\sigma'}}k_2\reduction{\ops{C}_{s,s'}}k_3
 \reduction{\fn{pskel}}k_4$.
@@ -1718,7 +1718,7 @@
   $\sigma'=\sigma_0\circ\sigma_r$ for some $\sigma_0$.)
 
 \item[Ensure previous events do not transform:] For each $\sigma'$,
-  find most general unifiers~$\sigma$ such that for $1\leq i<h$,
+  find most general unifiers~$\sigma$ such that for $0\leq i<h$,
   $\sigma(t_c)$ is carried only within $\sigma(T_e)$ at $\sigma(C(i))$
   and $\sigma'\unlhd\sigma$.  The function \fn{cowt}, presented in
   Figure~\ref{fig:cowt}, performs the explorations, producing the
@@ -1771,7 +1771,7 @@
 Let $k_0$ and $k_1$ be two skeletons such that there are two
 strands,~$s$ and~$s'$, and a most general unifier~$\sigma$ such that
 $\sigma(\Theta_{k_0}(s)(j))\equiv \sigma(\Theta_{k_0}(s')(j))$ for all
-$1\leq j\leq|\Theta_{k_0}(s)|$.  Then~$k_0$ \emph{collapses} to~$k_1$,
+$0\leq j<|\Theta_{k_0}(s)|$.  Then~$k_0$ \emph{collapses} to~$k_1$,
 written $k_0\reduction{\fn{clp}}k_1$, if
 $k_0\reduction{\ops{S}_\sigma}k\reduction{\ops{C}_{s,s'}}k'
 \reduction{\fn{skel}}k_1$.
@@ -2140,7 +2140,7 @@
 Shape formulas make use of protocol specific predicates and protocol
 independent predicates.  For each role $r=\role_Y(C,N,U)$ in
 protocol~$P$, there are protocol specific binary predicates
-$P[r,h,x]\colon\dom{nat}\times S$ for every $1\leq h\leq|C|$
+$P[r,h,x]\colon\dom{nat}\times S$ for every $0\leq h<|C|$
 and~$x\colon\srt{S}$ that occurs in~$C|_h$.  The protocol independent
 predicate of arity four is $\cn{prec}\colon
 \dom{nat}\times\dom{nat}\times\dom{nat}\times\dom{nat}$.  The protocol
diff --git a/doc/cpsauser.html b/doc/cpsauser.html
--- a/doc/cpsauser.html
+++ b/doc/cpsauser.html
@@ -3,7 +3,7 @@
 <head>
   <meta http-equiv="content-type"
   content="application/xhtml+xml; charset=UTF-8" />
-  <title>CPSA 2.2 User Guide</title>
+  <title>CPSA 2.3 User Guide</title>
   <meta name="generator" content="Amaya 9.54, see http://www.w3.org/Amaya/" />
   <style type="text/css">
     h1 { text-align: center }
@@ -12,7 +12,7 @@
 </head>
 
 <body>
-<h1>CPSA 2.2 User Guide</h1>
+<h1>CPSA 2.3 User Guide</h1>
 
 <p>The Cryptographic Protocol Shapes Analyzer (CPSA) attempts to enumerate all
 essentially different executions possible for a cryptographic protocol. We call
@@ -138,18 +138,18 @@
 DECL       ::= (ID+ SORT)
 TRACE      ::= (trace EVENT+)
 EVENT      ::= (send TERM) | (recv TERM)
-ROLE-ALIST ::= (non-orig HT-TERM*) ROLE-ALIST
-            |  (pen-non-orig HT-TERM*) ROLE-ALIST
+ROLE-ALIST ::= (non-orig POS-TERM*) ROLE-ALIST
+            |  (pen-non-orig POS-TERM*) ROLE-ALIST
             |  (uniq-orig TERM*) ROLE-ALIST | ...
-HT-TERM    ::= TERM | (INT TERM)
+            |  (priority NODE-INT*) SKEL-ALIST
+POS-TERM    ::= TERM | (INT TERM)
 PROT-ALIST ::= ...</pre>
 </blockquote>
 
 <p>The protocol <code>ID</code> is a symbol that names the protocol, and the role
 <code>ID</code> is a symbol that names the role. The <code>ALG</code> symbol identifies
 the algebra used by the protocol. For the Basic Cryptographic Algebra, the
-symbol is <code>basic</code>. For the Diffie-Hellman Algebra, the symbol is
-<code>diffie-hellman</code>. The <code>var</code> form contains symbols that
+symbol is <code>basic</code>. The <code>var</code> form contains symbols that
 declare the sort of the variables used in this role. The set of sort
 symbols is algebra specific. The protocol association list has no
 predefined keys, while the role association list has three. The value
@@ -158,7 +158,7 @@
 in the role's trace, but each of its variables must occur in some
 term.  A role non-origination assumption of the form <code>(3 a)</code>
 asserts that atom <code>a</code> will not be mapped into an instance
-unless its height is at least three.  For each <code>pen-non-orig</code>
+unless its height is greater than three.  For each <code>pen-non-orig</code>
 term, each of its variables must occur in some term, but unlike a
 non-origination assumption, the term may be carried.
 Each <code>uniq-orig</code> term must originate in the role's trace. Every
@@ -188,7 +188,8 @@
 SKEL-ALIST ::= (non-orig TERM*) SKEL-ALIST
             |  (pen-non-orig TERM*) SKEL-ALIST
             |  (uniq-orig TERM*) SKEL-ALIST
-            |  (precedes NODE-PAIR*) SKEL-ALIST | ...
+            |  (precedes NODE-PAIR*) SKEL-ALIST
+            |  (priority NODE-INT*) SKEL-ALIST | ...
 NODE-PAIR  ::= (NODE NODE)
 NODE       ::= (INT INT)</pre>
 </blockquote>
@@ -241,33 +242,6 @@
 <code>(operation collapsed INT INT)</code>, where the two <code>INT</code>s identify
 the strands merged. Shape collapsing is used to find related shapes.</p>
 
-<p>The current Diffie-Hellman support is experimental and known to
-have flaws. The additional sorts and terms in the Diffie-Hellman
-Algebra follow.</p>
-
-<blockquote>
-  <pre>SORT ::= ... | base | expn
-TERM ::= ... | (gen) | (exp TERM TERM)</pre>
-</blockquote>
-
-<p>Given exponent <code>x</code>, <code>(gen)</code> is the group
-generator constant, and
-given <code>g</code> and <code>x</code>, <code>(exp g x)</code>
-is <code>g</code> raised to the <code>x</code> power.  Terms of the
-form <code>(gen)</code> or <code>(exp g x)</code> are of sort <code>base</code>,
-and <code>x</code> is of sort <code>expn</code>.  Terms of
-sort <code>expn</code> are atoms, but terms of sort <code>base</code> are
-not.</p>
-
-<p>Reasoning about the commutativity of exponents is supported via
-  following equation.</p>
-
-<blockquote>
-  <pre>(exp (exp (gen) x) y) = (exp (exp (gen) y) x)</pre>
-</blockquote>
-
-<p>To avoid known Diffie-Hellman flaws, avoid variables of sort base.</p>
-
 <h3>Macros and Includes</h3>
 
 <p>After reading the input, <code>cpsa</code> expands macros before in analyzing
@@ -368,6 +342,26 @@
 
 <p>An error message that begins with "No test for unrealized node" identifies a
 severe error that should be reported as a bug.</p>
+
+<h3 id="priority">Search order</h3>
+
+<p>In its analysis, CPSA will attempt to solve unrealized nodes until the 
+skeleton is realized, and then generalize until a shape is obtained.  When 
+there are multiple unrealized nodes, by default, CPSA will chose the topmost,
+rightmost unrealized node among those unrealized nodes with maximum priority.
+The default priority of a node is 5, and higher numbers represent a higher 
+priority.  When a node has non-positive priority, it is left unsolved.</p>
+
+<p>In a role, in order to specify a priority for an event other than
+the default, add a comment of the
+form <code>(priority (<var>i</var> <var>p</var>))</code>,
+where <var>i</var> is the index of the event in the trace,
+and <var>p</var> is the priority.
+Priorities are inherited
+from roles, but may be overridden in a skeleton with a 
+<code>priority</code> comment of the form
+<code>(priority (<var>n</var> <var>p</var>))</code>,
+where <var>n</var> is a node.
 
 <h2 id="cpsagraph">Visualization</h2>
 
diff --git a/doc/dhke.scm b/doc/dhke.scm
deleted file mode 100644
--- a/doc/dhke.scm
+++ /dev/null
@@ -1,29 +0,0 @@
-(herald "Diffie-Hellman Key Exchange" (algebra diffie-hellman))
-
-;; The Diffie-Hellman problem is given (exp (gen) x), and (exp (gen)
-;; y), compute the value of (exp (exp (gen) x) y) which is also (exp
-;; (exp (gen) y) x).
-
-(defprotocol dhke diffie-hellman
-  (defrole init (vars (a b akey) (x y expn))
-    (trace
-     (send (enc "i" (exp (gen) x) (invk a)))
-     (recv (cat (enc (exp (gen) y) (invk b))
-		(enc a b (exp (exp (gen) y) x))))
-     (send (enc "i" a b (exp (exp (gen) y) x))))
-    (uniq-orig  x))
-  (defrole resp (vars (a b akey) (x y expn))
-    (trace
-     (recv (enc "i" (exp (gen) x) (invk a)))
-     (send (cat (enc (exp (gen) y) (invk b))
-		(enc a b (exp (exp (gen) x) y))))
-     (recv (enc "i" a b (exp (exp (gen) x) y))))
-    (uniq-orig y)))
-
-(defskeleton dhke (vars (a b akey))
-  (defstrand resp 3 (a a) (b b))
-  (non-orig (invk a) (invk b)))
-
- (defskeleton dhke (vars (a b akey))
-   (defstrand init 2 (a a) (b b))
-   (non-orig (invk a) (invk b)))
diff --git a/doc/macros.tex b/doc/macros.tex
--- a/doc/macros.tex
+++ b/doc/macros.tex
@@ -1,5 +1,5 @@
 \newcommand{\cpsa}{\textsc{cpsa}}
-\newcommand{\version}{2.2.13}
+\newcommand{\version}{2.3.0}
 \newcommand{\cpsacopying}{\begingroup
   \renewcommand{\thefootnote}{}\footnotetext{{\copyright} 2010 The
     MITRE Corporation.  Permission to copy without fee all or part of
diff --git a/src/CPSA/Annotations/Annotations.hs b/src/CPSA/Annotations/Annotations.hs
--- a/src/CPSA/Annotations/Annotations.hs
+++ b/src/CPSA/Annotations/Annotations.hs
@@ -11,6 +11,7 @@
 import Control.Monad
 import qualified Data.List as L
 import qualified Data.Set as S
+import qualified Data.Maybe as M
 import CPSA.Lib.CPSA
 import CPSA.Annotations.Formulas
 
@@ -457,7 +458,7 @@
       (t, fs) <- annos !! s                      -- t relies on (fs !! p)
       let guar = [ if t == t' then f else says t' f | -- Believe t
                    (s, p) <- ns,                 -- For each predecessor
-                   let Just (t', fs) = annos !! s, -- t' is the speaker
+                   (t', fs) <- M.maybeToList (annos !! s), -- t' is the speaker
                    let f = fs !! p ]               -- f is the guarantee
       return (n, t, implies guar (fs !! p))
 
diff --git a/src/CPSA/Basic/Algebra.hs b/src/CPSA/Basic/Algebra.hs
--- a/src/CPSA/Basic/Algebra.hs
+++ b/src/CPSA/Basic/Algebra.hs
@@ -10,7 +10,7 @@
 -- modify it under the terms of the BSD License as published by the
 -- University of California.
 
-{-# LANGUAGE MultiParamTypeClasses, CPP #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
 
 module CPSA.Basic.Algebra (name, origin) where
 
@@ -24,14 +24,6 @@
 import qualified CPSA.Lib.CPSA as C
 import CPSA.Lib.CPSA (SExpr(..), Pos, annotation)
 
--- Preserve the ability to use GHC 6.x
-foldrWithKey :: (k -> a -> b -> b) -> b -> Map k a -> b
-#if defined __GLASGOW_HASKELL__ && __GLASGOW_HASKELL__ < 700
-foldrWithKey = M.foldWithKey
-#else
-foldrWithKey = M.foldrWithKey
-#endif
-
 name :: String
 name = "basic"
 
@@ -154,6 +146,10 @@
 varId (F Akey [I x]) = x
 varId _ = error "Algebra.varId: term not a variable with its sort"
 
+isMesgVar :: Term -> Bool
+isMesgVar (I _) = True
+isMesgVar _ = False
+
 -- A list of terms are well-formed if each one has the correct
 -- structure and every occurrence of an identifier in a term has the
 -- same sort.  Variable environments are used to check the sort
@@ -435,6 +431,7 @@
 
 instance C.Term Term where
     isVar = isVar
+    isMesgVar = isMesgVar
     isAtom = isAtom
     termsWellFormed = termsWellFormed
     occursIn = occursIn
@@ -753,7 +750,7 @@
 identityEnvFor (Env r) ts =
     all (allId $ flip S.notMember dom) ts
     where
-      dom = foldrWithKey f S.empty r -- The domain of r
+      dom = M.foldrWithKey f S.empty r -- The domain of r
       f x (I y) dom
           | x == y = dom        -- Ignore trivial bindings
           | otherwise = S.insert x dom
diff --git a/src/CPSA/DiffieHellman/Algebra.hs b/src/CPSA/DiffieHellman/Algebra.hs
--- a/src/CPSA/DiffieHellman/Algebra.hs
+++ b/src/CPSA/DiffieHellman/Algebra.hs
@@ -14,7 +14,7 @@
 -- modify it under the terms of the BSD License as published by the
 -- University of California.
 
-{-# LANGUAGE MultiParamTypeClasses, CPP #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
 
 module CPSA.DiffieHellman.Algebra (name, origin) where
 
@@ -29,14 +29,6 @@
 import CPSA.Lib.CPSA (SExpr(..), Pos, annotation)
 import qualified CPSA.DiffieHellman.IntLinEq as I
 
--- Preserve the ability to use GHC 6.x
-foldrWithKey :: (k -> a -> b -> b) -> b -> Map k a -> b
-#if defined __GLASGOW_HASKELL__ && __GLASGOW_HASKELL__ < 700
-foldrWithKey = M.foldWithKey
-#else
-foldrWithKey = M.foldrWithKey
-#endif
-
 {-- Debugging support
 import System.IO.Unsafe
 
@@ -59,11 +51,59 @@
 zt _ y = y
 --}
 
-{-- Export iUnify and iMatch for GHCi for debugging
+{- Export iUnify and iMatch for GHCi for debugging
+
+For this to work, you must install the package bytestring-handle from
+Hackage and tell GHCi that it is not hidden on the command line or
+within GHCi with:
+
+:set -package bytestring-handle
+
+-}
+
+{--
+import System.IO (Handle)
+import Data.ByteString.Lazy.Char8 (pack)
+import Data.ByteString.Handle
+import Control.Exception (try)
+import System.IO.Unsafe
+
+stringHandle :: String -> IO Handle
+stringHandle s = readHandle False (pack s)
+
+stringPosHandle :: String -> IO C.PosHandle
+stringPosHandle s =
+    do
+      h <- stringHandle s
+      C.posHandle "" h
+
+stringLoad :: String -> IO [SExpr Pos]
+stringLoad s =
+    do
+      h <- stringPosHandle s
+      loop h []
+    where
+      loop h xs =
+          do
+            x <- C.load h
+            case x of
+              Nothing ->
+                return $ reverse xs
+              Just x ->
+                loop h (x : xs)
+
+sLoad :: String -> Maybe [SExpr Pos]
+sLoad s =
+    unsafePerformIO (stringLoad s >>= return . Just)
+
+-- Test unification
+
 iUnify :: String -> String -> String -> Maybe Subst
 iUnify vars t t' =
     iRun unify emptySubst vars t t'
 
+-- Test matching
+
 iMatch :: String -> String -> String -> Maybe Env
 iMatch vars t t' =
     iRun match emptyEnv vars t t'
@@ -72,9 +112,9 @@
         String -> String -> String -> Maybe a
 iRun f mt vars t t' =
     do
-      vars <- C.load "" vars
-      [t] <- C.load "" t
-      [t'] <- C.load "" t'
+      vars <- sLoad vars
+      [t] <- sLoad t
+      [t'] <- sLoad t'
       (gen, vars) <- loadVars origin vars
       t <- loadTerm vars t
       t' <- loadTerm vars t'
@@ -152,7 +192,7 @@
 
 mul :: Group -> Group -> Group
 mul t t' =
-    foldrWithKey f t' t         -- Fold over the mappings in t
+    M.foldrWithKey f t' t       -- Fold over the mappings in t
     where
       f x c t =                 -- Alter the mapping of
           M.alter (g c) x t     -- variable x in t
@@ -289,6 +329,10 @@
 varId (G t) | isGroupVar t = head $ M.keys t
 varId _ = error "Algebra.varId: term not a variable with its sort"
 
+isMesgVar :: Term -> Bool
+isMesgVar (I _) = True
+isMesgVar _ = False
+
 -- A list of terms are well-formed if each one has the correct
 -- structure and every occurrence of an identifier in a term has the
 -- same sort.  Variable environments are used to check the sort
@@ -475,7 +519,6 @@
     ba term
     where
       ba (I _) = True           -- A mesg sorted variable is always buildable
-      ba (F Base [I _]) = True  -- as is a base sorted variable
       ba (C _) = True           -- So is a tag
       ba (F Cat [t0, t1]) =
           ba t0 && ba t1
@@ -658,6 +701,7 @@
 
 instance C.Term Term where
     isVar = isVar
+    isMesgVar = isMesgVar
     isAtom = isAtom
     termsWellFormed = termsWellFormed
     occursIn = occursIn
@@ -847,7 +891,7 @@
 
 groupSubst :: IdMap -> Group -> Group
 groupSubst subst t =
-    foldrWithKey f M.empty t
+    M.foldrWithKey f M.empty t
     where
       f x n t =
           mul (expg (groupLookup subst x) n) t
@@ -1172,28 +1216,28 @@
 matchGroup ::  Group -> Group -> Set Id -> Gen -> Maybe (Set Id, Gen, IdMap)
 matchGroup t0 t1 v g =
     case partition t0 t1 v of
-      (_, [], []) -> return (v, g, emptyIdMap)
-      (_, [], _) -> Nothing
-      (n, t0, t1) ->
+      ([], []) -> return (v, g, emptyIdMap)
+      ([], _) -> Nothing
+      (t0, t1) ->
           do
             subst <- I.intLinEq (map snd t0, map snd t1)
-            return $ mgu v n (map fst t0) (map fst t1) subst g
+            return $ mgu v (map fst t0) (map fst t1) subst g
 
 type Coeff = [(Id, Int)]
 
 -- Move variables on the RHS of the equation to the LHS
-partition ::  Group -> Group -> Set Id -> (Int, Coeff, Coeff)
+partition ::  Group -> Group -> Set Id -> (Coeff, Coeff)
 partition t0 t1 v =
-    (length v0, v0 ++ map (\(x,n) -> (x, negate n)) v1, c1)
+    (v0 ++ map (\(x,n) -> (x, negate n)) v1, c1)
     where
       v0 = M.assocs t0
       (v1, c1) = L.partition f (M.assocs t1)
       f (x, _) = S.member x v
 
-mgu :: Set Id -> Int -> [Id] -> [Id] -> I.Subst -> Gen -> (Set Id, Gen, IdMap)
-mgu v _ _ _ [] gen = (v, gen, emptyIdMap)
-mgu v n vars syms subst gen =
-    (v', gen', foldl f emptyIdMap (zip vars [0..(n - 1)]))
+mgu :: Set Id -> [Id] -> [Id] -> I.Subst -> Gen -> (Set Id, Gen, IdMap)
+mgu v _ _ [] gen = (v, gen, emptyIdMap)
+mgu v vars syms subst gen =
+    (v', gen', foldl f emptyIdMap (zip vars [0..]))
     where
       (gen', genSyms) = genVars vars (length (fst (snd (head subst)))) gen
       v' = foldl (flip S.insert) v genSyms
@@ -1260,7 +1304,7 @@
 groupEnv g v env grp ((x, t):map)
     | M.lookup x t /= Just 1 = groupEnv g v env grp map
     | otherwise =
-        let (_, t0, t1) = partition M.empty (mul t (M.singleton x (-1))) v in
+        let (t0, t1) = partition M.empty (mul t (M.singleton x (-1))) v in
         case matchGroup (group t0) (group t1) S.empty g of
           Nothing -> groupEnv g v env grp map
           Just (v', g', subst) ->
@@ -1271,7 +1315,7 @@
 -- Specialize an environment by mapping the generated variables to one.
 specialize :: Env -> Env
 specialize (Env (v, r)) =
-    Env (S.empty, foldrWithKey f M.empty r)
+    Env (S.empty, M.foldrWithKey f M.empty r)
     where
       f x t r = M.insert x (instantiate special t) r
       -- Environment mapping generated variables to one
@@ -1317,7 +1361,7 @@
 matchRenaming :: GenEnv -> Bool
 matchRenaming (gen, Env (v, e)) =
     nonGrp S.empty (M.elems e) &&
-    groupMatchRenaming v gen (foldrWithKey grp M.empty e)
+    groupMatchRenaming v gen (M.foldrWithKey grp M.empty e)
     where
       nonGrp _ [] = True
       nonGrp s (I x:e) =
@@ -1341,7 +1385,7 @@
 
 groupMatchElim :: Set Id -> Gen -> Map Id Group -> Group -> (Id, Int) -> Bool
 groupMatchElim v gen ge t (x, 1) =
-    let (_, t0, t1) = partition M.empty (mul t (M.singleton x (-1))) v in
+    let (t0, t1) = partition M.empty (mul t (M.singleton x (-1))) v in
     case matchGroup (group t0) (group t1) S.empty gen of
       Nothing -> False
       Just (v', gen', subst) ->
diff --git a/src/CPSA/DiffieHellmanNoReciprocal/Algebra.hs b/src/CPSA/DiffieHellmanNoReciprocal/Algebra.hs
--- a/src/CPSA/DiffieHellmanNoReciprocal/Algebra.hs
+++ b/src/CPSA/DiffieHellmanNoReciprocal/Algebra.hs
@@ -62,14 +62,6 @@
 zt _ y = y
 --}
 
--- Preserve the ability to use GHC 6.x
-foldrWithKey :: (k -> a -> b -> b) -> b -> Map k a -> b
-#if defined __GLASGOW_HASKELL__ && __GLASGOW_HASKELL__ < 700
-foldrWithKey = M.foldWithKey
-#else
-foldrWithKey = M.foldrWithKey
-#endif
-
 -- Export iUnify and iMatch for debugging in GHCi.
 -- Both functions request a declaration and then two terms.
 -- Example: ((x y z expn)) (mul x x y) z
@@ -196,7 +188,7 @@
 
 mul :: Group -> Group -> Group
 mul t t' =
-    foldrWithKey f t' t         -- Fold over the mappings in t
+    M.foldrWithKey f t' t       -- Fold over the mappings in t
     where
       f x c t =                 -- Alter the mapping of
           M.alter (g c) x t     -- variable x in t
@@ -265,6 +257,10 @@
 varId (G t) | isGroupVar t = head $ M.keys t
 varId _ = error "Algebra.varId: term not a variable with its sort"
 
+isMesgVar :: Term -> Bool
+isMesgVar (I _) = True
+isMesgVar _ = False
+
 -- A list of terms are well-formed if each one has the correct
 -- structure and every occurrence of an identifier in a term has the
 -- same sort.  Variable environments are used to check the sort
@@ -441,7 +437,7 @@
 
 expnHeldBy :: Term -> Term -> Bool
 expnHeldBy (G t) (G t')
-    | t == t' = 
+    | t == t' =
         True
 expnHeldBy (G t) (G t')
     | isGroupVar t =
@@ -473,7 +469,7 @@
           S.member (F Base [t]) knowns || ba t0 && be t1
       bb _ = False
       -- Buildable exponent
-      be t = buildableExponent t 
+      be t = buildableExponent t
              [ g | t <- S.elems unguessable, g <- getGroup t ]
 
 getGroup :: Term -> [Group]
@@ -495,7 +491,7 @@
                   usefulKnowns ++ [ mul k k' |
                                     k <- usefulKnowns,
                                     k' <- filteredLevel (n - 1) ]
-      usefulKnowns = L.filter (flip notElem unguessables) 
+      usefulKnowns = L.filter (flip notElem unguessables)
                      (map (flip M.singleton 1) (M.keys t))
 
 -- Compute the decomposition given some known terms and some unguessable
@@ -616,6 +612,7 @@
 
 instance C.Term Term where
     isVar = isVar
+    isMesgVar = isMesgVar
     isAtom = isAtom
     termsWellFormed = termsWellFormed
     occursIn = occursIn
@@ -803,7 +800,7 @@
 
 groupSubst :: IdMap -> Group -> Group
 groupSubst subst t =
-    foldrWithKey f M.empty t
+    M.foldrWithKey f M.empty t
     where
       f x n t =
           mul (expg (groupLookup subst x) n) t
@@ -963,7 +960,7 @@
           mkmgus (map fst t) bases (g, Subst s)
 
 mkmgus :: [Id] -> [[Int]] -> GenSubst -> GenSubst
-mkmgus vars [] (g, Subst s) = 
+mkmgus vars [] (g, Subst s) =
     (g, Subst $ foldl f s vars)
     where
       f s v = M.insert v (G M.empty) s
@@ -1022,9 +1019,9 @@
           | otherwise -> F Exp [t0, G t1']
 
 groupChase :: Subst -> Group -> Group
-groupChase (Subst subst) t = 
+groupChase (Subst subst) t =
     loop t
-    where 
+    where
       loop t =
           case groupSubst subst t of
             t' | t == t' -> t'
diff --git a/src/CPSA/Graph/Loader.hs b/src/CPSA/Graph/Loader.hs
--- a/src/CPSA/Graph/Loader.hs
+++ b/src/CPSA/Graph/Loader.hs
@@ -14,7 +14,7 @@
 module CPSA.Graph.Loader (Preskel, Vertex, protocol, role, env, inst,
                           part, lastVertex, vertices, Node, vnode,
                           strands, label, parent, seen, unrealized, shape,
-                          protSrc, preskelSrc, initial, strand, pos,
+                          empty, protSrc, preskelSrc, initial, strand, pos,
                           prev, next, msg, out, succs, preds,
                           State, loadFirst, loadNext)
                           where
@@ -35,7 +35,8 @@
       strands :: Int,           -- Number of strands
       initial :: [Vertex],      -- The initial node in each strand
       unrealized :: Maybe [Vertex], -- Nodes not realized if available
-      shape :: Bool,            -- Is preskel ashape?
+      shape :: Bool,            -- Is preskel a shape?
+      empty :: Bool,            -- Does preskel have an empty cohort?
       protSrc :: SExpr Pos,     -- Source for the protocol
       preskelSrc :: SExpr Pos } -- Source for this preskeleton
     deriving Show
@@ -252,6 +253,7 @@
       let heights = map (length . trace) insts
       unrealized <- loadNodes heights (assoc "unrealized" xs)
       let shape = maybe False (const True) (assoc "shape" xs)
+      let empty = elem "empty cohort" (qassoc "comment" xs)
       let orderings = maybe [] id (assoc "precedes" xs)
       pairs <- loadOrderings heights orderings
       let graph = adj heights pairs
@@ -270,6 +272,7 @@
                              initial = initial,
                              unrealized = unrealized',
                              shape = shape,
+                             empty = empty,
                              protSrc = src p,
                              preskelSrc = s }
             where
@@ -397,6 +400,16 @@
 
 -- assoc key alist =
 --    concat [ rest | L _ (S _ head : rest) <- alist, key == head ]
+
+qassoc :: String -> [SExpr Pos] -> [String]
+qassoc key xs =
+  case assoc key xs of
+    Nothing -> []
+    Just vals ->
+      concatMap f vals
+      where
+        f (Q _ s) = [s]
+        f _ = []
 
 nassoc :: Monad m => String -> [SExpr Pos] -> m (Maybe Int)
 nassoc key xs =
diff --git a/src/CPSA/Graph/Tree.hs b/src/CPSA/Graph/Tree.hs
--- a/src/CPSA/Graph/Tree.hs
+++ b/src/CPSA/Graph/Tree.hs
@@ -53,6 +53,7 @@
     where
       live kids dups =
           maybe True null (unrealized k) ||
+          null kids && null dups && not (empty k) ||
           any alive kids || any alive dups
       x [] [] = 1
       -- The width of a duplicate is one
diff --git a/src/CPSA/Lib/Algebra.hs b/src/CPSA/Lib/Algebra.hs
--- a/src/CPSA/Lib/Algebra.hs
+++ b/src/CPSA/Lib/Algebra.hs
@@ -27,6 +27,7 @@
 
 class (Ord t, Show t) => Term t where
     isVar :: t -> Bool          -- Is term a variable in the algebra?
+    isMesgVar :: t -> Bool      -- Is term a variable of sort mesg?
     isAtom :: t -> Bool       -- Is the sort of this term a base sort?
 
     -- Does a term occur in another term?
diff --git a/src/CPSA/Lib/Cohort.hs b/src/CPSA/Lib/Cohort.hs
--- a/src/CPSA/Lib/Cohort.hs
+++ b/src/CPSA/Lib/Cohort.hs
@@ -76,6 +76,10 @@
 usePruningDuringGeneralization :: Bool
 usePruningDuringGeneralization = False -- True
 
+-- Minimum priority to solve
+minPriority :: Int
+minPriority = 1
+
 -- Penetrator derivable predicate and checking for unrealized skeletons.
 
 derivable :: Algebra t p g s e c => Set t -> Set t -> t -> Bool
@@ -193,14 +197,32 @@
 reduce :: Algebra t p g s e c => Mode -> Preskel t p g s e c ->
           [Preskel t p g s e c]
 reduce mode k =
-    firstJust (map (testStrand mode k u a) ss)
-                  (whenRealized k) -- Skeleton is realized
+    maybe (whenRealized k) id (findTest mode k u a)
     where
-      ss = strandVisitOrder mode (strands  k)
       (a, u) = avoid k
       whenRealized k =
           if noGeneralization mode then [] else maximize k
 
+prioritizeVertices :: Algebra t p g s e c => Preskel t p g s e c ->
+                      [Vertex t p g s e c] -> [Vertex t p g s e c]
+prioritizeVertices k vs =
+     map fst $ filter keep $ L.sortBy prios $ map addPrio vs
+     where
+       addPrio v = (v, priority k (sid $ strand v, pos v))
+       prios (_, p) (_, p') = compare p p'
+       keep (_, p) = p >= minPriority
+
+priority :: Algebra t p g s e c => Preskel t p g s e c -> Node -> Int
+priority k (s, i) =
+  case lookup (s, i) (kpriority k) of
+    Just p -> p
+    Nothing -> rpriority (role $ insts k !! s) !! i
+
+nodeOrder :: Algebra t p g s e c => Mode ->
+             Preskel t p g s e c -> [Vertex t p g s e c]
+nodeOrder mode k =
+    concatMap (nodeVisitOrder mode) (strandVisitOrder mode (strands  k))
+
 strandVisitOrder :: Mode -> [a] -> [a]
 strandVisitOrder mode ss =
     if visitOldStrandsFirst mode then
@@ -208,19 +230,19 @@
     else
         reverse ss     -- Visit recently added strands first (default)
 
--- Returns the first Just value in a list or the default when there is
--- none.
-firstJust :: [Maybe a] -> a -> a
-firstJust [] x = x
-firstJust (Just x : _) _ = x
-firstJust (Nothing : xs) x = firstJust xs x
+nodeVisitOrder :: Algebra t p g s e c => Mode ->
+                  Strand t p g s e c -> [Vertex t p g s e c]
+nodeVisitOrder mode s =
+    if reverseNodeOrder mode == rsearch (role $ inst s) then
+        nodes s                -- Visit earliest nodes first (default)
+    else
+        reverse $ nodes s       -- Visit latest nodes first
 
 -- Look for a test node in a strand
-testStrand :: Algebra t p g s e c => Mode -> Preskel t p g s e c ->
-              [t] -> Set t -> Strand t p g s e c ->
-              Maybe [Preskel t p g s e c]
-testStrand mode k u a s =
-    loop (nodeVisitOrder mode s)
+findTest :: Algebra t p g s e c => Mode -> Preskel t p g s e c ->
+              [t] -> Set t -> Maybe [Preskel t p g s e c]
+findTest mode k u a =
+    loop (prioritizeVertices k $ nodeOrder mode k)
     where
       loop [] = Nothing
       loop (n : nodes) =
@@ -234,14 +256,6 @@
                     loop nodes
                 else
                     Just $ testNode mode k u ts der (graphNode n) t
-
-nodeVisitOrder :: Algebra t p g s e c => Mode ->
-                  Strand t p g s e c -> [Vertex t p g s e c]
-nodeVisitOrder mode s =
-    if reverseNodeOrder mode == rsearch (role $ inst s) then
-        nodes s                -- Visit earliest nodes first (default)
-    else
-        reverse $ nodes s       -- Visit latest nodes first
 
 -- Look for a critical term that makes this node a test node.
 testNode :: Algebra t p g s e c => Mode -> Preskel t p g s e c ->
diff --git a/src/CPSA/Lib/Displayer.hs b/src/CPSA/Lib/Displayer.hs
--- a/src/CPSA/Lib/Displayer.hs
+++ b/src/CPSA/Lib/Displayer.hs
@@ -87,11 +87,17 @@
      (displayOptional "non-orig" (displayTerms ctx (knon k))
       (displayOptional "pen-non-orig" (displayTerms ctx (kpnon k))
        (displayOptional "uniq-orig" (displayTerms ctx (kunique k))
-        (kcomment k ++
-         (displayOperation k ctx
-          (displayOptional "traces" traces rest))))))
+        (displayOptional "priority" priorities
+         (kcomment k ++
+          (displayOperation k ctx
+           (displayOptional "traces" traces rest)))))))
     where
+      priorities = map displayPriority (kpriority k)
       traces = map (L () . displayTrace ctx . trace) (insts k)
+
+displayPriority :: (Node, Int) -> SExpr ()
+displayPriority (n, p) =
+    L () [displayNode n, N () p]
 
 displayInst :: Algebra t p g s e c => c ->
                Instance t p g s e c -> SExpr ()
diff --git a/src/CPSA/Lib/Loader.hs b/src/CPSA/Lib/Loader.hs
--- a/src/CPSA/Lib/Loader.hs
+++ b/src/CPSA/Lib/Loader.hs
@@ -112,7 +112,8 @@
       let as = L.filter (varsSeen vs . snd) a
       -- Drop runiques that refer to unused variable declarations
       let us = L.filter (varsSeen vs) u
-      let r = mkRole name vs c ns as us comment reverseSearch
+      prios <- mapM (loadRolePriority (length c)) (assoc "priority" rest)
+      let r = mkRole name vs c ns as us comment prios reverseSearch
       case roleWellFormed r of
         Return () -> return (gen, r)
         Fail msg -> fail (shows pos $ showString "Role not well formed: " msg)
@@ -128,6 +129,11 @@
     Return r >>= k = k r
     fail s = Fail s
 
+loadRolePriority :: Monad m => Int -> SExpr Pos -> m (Int, Int)
+loadRolePriority n (L _ [N _ i, N _ p])
+    | 0 <= i && i < n = return (i, p)
+loadRolePriority _ x = fail (shows (annotation x) "Malformed priority")
+
 -- Are the vars in t a subset of ones in t.
 varsSeen :: Algebra t p g s e c => [t] -> t -> Bool
 varsSeen vs t =
@@ -158,11 +164,13 @@
           failwith (showString "non-orig " $ showst t " carried")
                        $ all (not . carriedBy t) terms
       lenCheck (Nothing, _) = return ()
-      lenCheck (Just len, t) =
+      lenCheck (Just len, _) | len >= length (rtrace role) =
+          fail $ showString "invalid position " $ show len
+      lenCheck (Just len, t) | otherwise =
           case usedPos t (rtrace role) of
-            Just p | p < len -> return ()
+            Just p | p <= len -> return ()
             Just _ -> fail $ showst t
-                      $ showString " appears after length " $ show len
+                      $ showString " appears after position " $ show len
             Nothing -> fail msg
           where
             msg = "no used position for non-originating atom " ++ showst t ""
@@ -171,7 +179,8 @@
                        $ originates t (rtrace role)
       origVarCheck v =
           failwith (showString "variable " $ showst v " not acquired")
-                       $ isAtom v || isJust (acquiredPos v (rtrace role))
+                       $ not (isMesgVar v) ||
+                         isJust (acquiredPos v (rtrace role))
 
 failwith :: Monad m => String -> Bool -> m ()
 failwith msg test =
@@ -270,9 +279,9 @@
 loadPosBaseTerm :: (Algebra t p g s e c, Monad m) => [t] ->
                    SExpr Pos -> m (Maybe Int, t)
 loadPosBaseTerm vars x'@(L _ [N _ opos, x])
-    | opos <= 0 =
+    | opos < 0 =
         fail (shows (annotation x')
-              "Expecting a positive non-origination trace length")
+              "Expecting a non-negative non-origination position")
     | otherwise =
         do
           t <- loadBaseTerm vars x
@@ -326,12 +335,13 @@
 loadInsts top p kvars gen insts xs =
     do
       _ <- alist [] xs          -- Check syntax of xs
-      loadRest top kvars p gen (reverse insts) order nr ar ur kcomment
+      loadRest top kvars p gen (reverse insts) order nr ar ur pl kcomment
     where
       order = assoc "precedes" xs
       nr = assoc "non-orig" xs
       ar = assoc "pen-non-orig" xs
       ur = assoc "uniq-orig" xs
+      pl = assoc "priority" xs
       comment = assoc "comment" xs
       kcomment =
           if null comment then
@@ -382,8 +392,8 @@
 loadRest :: (Algebra t p g s e c, Monad m) => Pos -> [t] ->
             Prot t p g s e c -> g -> [Instance t p g s e c] ->
             [SExpr Pos] -> [SExpr Pos] -> [SExpr Pos] -> [SExpr Pos] ->
-            [SExpr ()] -> m (Preskel t p g s e c)
-loadRest pos vars p gen insts orderings nr ar ur comment =
+            [SExpr Pos] -> [SExpr ()] -> m (Preskel t p g s e c)
+loadRest pos vars p gen insts orderings nr ar ur pl comment =
     do
       case null insts of
         True -> fail (shows pos "No strands")
@@ -394,7 +404,8 @@
       ar <- loadBaseTerms vars ar
       ur <- loadBaseTerms vars ur
       let (nr', ar', ur') = foldl addInstOrigs (nr, ar, ur) insts
-      let k = mkPreskel gen p insts o nr' ar' ur' comment
+      prios <- mapM (loadPriorities heights) pl
+      let k = mkPreskel gen p insts o nr' ar' ur' prios comment
       case termsWellFormed $ nr' ++ ar' ++ ur' ++ kterms k of
         False -> fail (shows pos "Terms in skeleton not well formed")
         True -> return ()
@@ -439,6 +450,14 @@
           | s == 0 = Just x
           | otherwise = height xs (s - 1)
 loadNode _ x = fail (shows (annotation x) "Malformed node")
+
+loadPriorities :: Monad m => [Int] -> SExpr Pos -> m (Node, Int)
+loadPriorities heights (L _ [x, N _ p]) =
+    do
+      n <- loadNode heights x
+      return (n, p)
+loadPriorities _ x =
+    fail (shows (annotation x) "Malformed priority")
 
 addInstOrigs :: Algebra t p g s e c => ([t], [t], [t]) ->
                 Instance t p g s e c -> ([t], [t], [t])
diff --git a/src/CPSA/Lib/Protocol.hs b/src/CPSA/Lib/Protocol.hs
--- a/src/CPSA/Lib/Protocol.hs
+++ b/src/CPSA/Lib/Protocol.hs
@@ -8,10 +8,10 @@
 
 module CPSA.Lib.Protocol (Event (..), evtTerm, evtMap, Trace, evt,
     tterms, originates, originationPos, acquiredPos, usedPos, Role,
-    rname, rvars, rtrace, rnon, rpnon, runique, rcomment, rsearch,
-    rnorig, rpnorig, ruorig, mkRole, varSubset, varsInTerms, addVars,
-    Prot, mkProt, pname, alg, pgen, roles, varsAllAtoms, pcomment,
-    flow) where
+    rname, rvars, rtrace, rnon, rpnon, runique, rcomment,
+    rsearch, rnorig, rpnorig, ruorig, rpriority, mkRole, varSubset,
+    varsInTerms, addVars, Prot, mkProt, pname, alg, pgen, roles,
+    varsAllAtoms, pcomment, flow) where
 
 import qualified Data.List as L
 import qualified Data.Set as S
@@ -163,9 +163,13 @@
       rsearch :: Bool, -- True when suggesting reverse test node search
       rnorig :: [(t, Int)],     -- Nons plus origination position
       rpnorig :: [(t, Int)], -- Penetrator nons plus origination position
-      ruorig :: [(t, Int)] }    -- Uniques plus origination position
+      ruorig :: [(t, Int)],     -- Uniques plus origination position
+      rpriority :: [Int] }      -- List of all priorities
     deriving Show
 
+defaultPriority :: Int
+defaultPriority = 5
+
 -- The empty role name is used with listener strands.  All roles in a
 -- protocol must have a name with more than one character.
 
@@ -175,11 +179,11 @@
 -- Create a role
 mkRole :: Algebra t p g s e c => String -> [t] -> Trace t p g s e c ->
           [(Maybe Int, t)] -> [(Maybe Int, t)] -> [t] ->
-          [SExpr ()] -> Bool -> Role t p g s e c
-mkRole name vars trace non pnon unique comment rev =
+          [SExpr ()] -> [(Int, Int)] -> Bool -> Role t p g s e c
+mkRole name vars trace non pnon unique comment priority rev =
     Role { rname = name,
            rvars = L.nub vars,  -- Every variable here must
-           rtrace = trace,      --  occur in the trace.
+           rtrace = trace,      -- occur in the trace.
            rnon = non,
            rpnon = pnon,
            runique = L.nub unique,
@@ -187,6 +191,7 @@
            rnorig = map addNonOrig $ nonNub non,
            rpnorig = map addNonOrig $ nonNub pnon,
            ruorig = map addUniqueOrig $ L.nub unique,
+           rpriority = addDefaultPrio priority,
            rsearch = rev
          }
     where
@@ -200,10 +205,10 @@
             Just p ->
                 case len of
                   Nothing -> (t, p)
-                  Just len | len > p -> (t, len - 1)
+                  Just len | len >= p -> (t, len)
                            | otherwise -> error msg
           where
-            msg = "Protocol.mkRole: Length for atom too early in trace"
+            msg = "Protocol.mkRole: Position for atom too early in trace"
       -- Drop non-origination assumptions for the same atom.
       nonNub nons =
           reverse $ foldl f [] nons
@@ -211,6 +216,13 @@
             f acc non@(_, t)
                 | any (\(_, t') -> t == t') acc = acc
                 | otherwise = non : acc
+      addDefaultPrio priority =
+          map f (nats $ length trace)
+          where
+            f n =
+              case lookup n priority of
+                Nothing -> defaultPriority
+                Just p -> p
 
 -- Protocols
 
diff --git a/src/CPSA/Lib/Strand.hs b/src/CPSA/Lib/Strand.hs
--- a/src/CPSA/Lib/Strand.hs
+++ b/src/CPSA/Lib/Strand.hs
@@ -9,9 +9,9 @@
 module CPSA.Lib.Strand (Instance, mkInstance, bldInstance, mkListener,
     role, env, trace, height, listenerTerm, Sid, Node, mkPreskel,
     firstSkeleton, Pair, Preskel, gen, protocol, insts, orderings,
-    pov, knon, kpnon, kunique, korig, kcomment, nstrands, kvars,
+    pov, knon, kpnon, kunique, korig, kpriority, kcomment, nstrands, kvars,
     kterms, uniqOrig, preskelWellFormed, verbosePreskelWellFormed,
-    Strand, inst, nodes, Vertex, preds, event,
+    Strand, inst, sid, nodes, Vertex, strand, pos, preds, event,
     graphNode, strands, vertex, Gist, gist, contract, augment,
     inheritRnon, inheritRpnon, inheritRunique, addListener, Cause
     (..), Direction (..), Method (..), Operation (..), operation,
@@ -199,7 +199,7 @@
               (g, Instance t p g s e c)
 mkListener gen term =
     (gen'', Instance { role = mkRole "" vars [In rterm, Out rterm]
-                              [] [] [] [] False,
+                              [] [] [] [] [] False,
                        env = env,
                        trace = [In term, Out term],
                        height = 2 })
@@ -371,6 +371,7 @@
       knon :: ![t],             -- A list of atoms
       kpnon :: ![t],            -- A list of atoms
       kunique :: ![t],          -- A list of atoms
+      kpriority :: [(Node, Int)], -- Override node priority
       kcomment :: [SExpr ()],   -- Comments from the input
       korig :: ![(t, [Node])],  -- This is an association list with a
                                 -- pair for each element of kunique.
@@ -433,12 +434,12 @@
 -- must be consumed by firstSkeleton.
 mkPreskel :: Algebra t p g s e c => g -> Prot t p g s e c ->
              [Instance t p g s e c] -> [Pair] -> [t] -> [t] -> [t] ->
-             [SExpr ()] -> Preskel t p g s e c
-mkPreskel gen protocol insts orderings non pnon unique comment =
+             [(Node, Int)] -> [SExpr ()] -> Preskel t p g s e c
+mkPreskel gen protocol insts orderings non pnon unique prio comment =
     k { kcomment = comment }
     where
       k = newPreskel gen protocol insts orderings non pnon
-          unique New prob Nothing
+          unique prio New prob Nothing
       prob = strandids k        -- Fixed point on k is okay.
 
 -- Strand functions
@@ -466,9 +467,9 @@
 -- within this module.
 newPreskel :: Algebra t p g s e c => g -> Prot t p g s e c ->
              [Instance t p g s e c] -> [Pair] -> [t] -> [t] -> [t] ->
-             Operation t p g s e c -> [Sid] ->
+             [(Node, Int)] -> Operation t p g s e c -> [Sid] ->
              Maybe (Preskel t p g s e c) -> Preskel t p g s e c
-newPreskel gen protocol insts orderings non pnon unique oper prob pov =
+newPreskel gen protocol insts orderings non pnon unique prio oper prob pov =
     let orderings' = L.nub orderings
         unique' = L.nub unique
         g = graph trace height insts orderings'
@@ -485,6 +486,7 @@
                       knon = L.nub non,
                       kpnon = L.nub pnon,
                       kunique = unique',
+                      kpriority = prio,
                       kcomment = [],
                       korig = orig,
                       tc = map graphPair tc,
@@ -869,7 +871,8 @@
       let unique' = map (substitute subst) (kunique k)
       let operation' = substOper subst (operation k)
       let k' = newPreskel gen' (protocol k) insts'
-               (orderings k) non' pnon' unique' operation' (prob k) (pov k)
+               (orderings k) non' pnon' unique' (kpriority k)
+               operation' (prob k) (pov k)
       k' <- wellFormedPreskel k'
       case not validate || validateMappingSubst k0 phi subst k' of
         True -> return (k0, k', n, phi, compose subst hsubst)
@@ -926,6 +929,7 @@
               (knon k)
               (kpnon k)
               (kunique k)
+              (updatePriority perm (kpriority k))
               (operation k)
               (updateProb perm (prob k))
               (pov k)
@@ -963,6 +967,10 @@
 updateProb mapping prob =
     map (mapping !!) prob
 
+updatePriority :: [Sid] -> [(Node, Int)] -> [(Node, Int)]
+updatePriority mapping kpriority =
+    map (\(n, i) -> (permuteNode mapping n, i)) kpriority
+
 -- Purge a strand.  Used by thinning.  The same as pruning except
 -- edges to the purged strand are forwarded as a first step.
 purge :: Algebra t p g s e c => PRS t p g s e c ->
@@ -982,6 +990,7 @@
               (knon k)
               (kpnon k)
               (kunique k)
+              (updatePriority perm (kpriority k))
               (operation k)
               (updateProb perm (prob k))
               (pov k)
@@ -1072,6 +1081,7 @@
                   (knon k)
                   (kpnon k)
                   (kunique k)
+                  (kpriority k)
                   (operation k)
                   (prob k)
                   (pov k)
@@ -1306,6 +1316,7 @@
             e <- ges
             (gen, env) <- thinStrandCheck k s e
             [ prs' | prs <- ksubst False prs (gen, substitution env),
+                     prs <- reduce prs,
                      prs' <- purge prs s s',
                      prs'' <- purge prs s' s,
                      gist (skel prs') == gist (skel prs'')]
@@ -1380,6 +1391,7 @@
       let k = skel prs
       (gen, env) <- thinManyMatch k ps
       [ prs' | prs <- ksubst False prs (gen, substitution env),
+               prs <- reduce prs,
                prs' <- compressMany prs ps,
                prs'' <- compressMany prs (swap ps),
                gist (skel prs') == gist (skel prs'')]
@@ -1446,6 +1458,7 @@
                   (knon k)
                   (kpnon k)
                   (kunique k)
+                  (kpriority k)
                   (operation k)
                   (prob k)
                   (pov k)
@@ -1546,7 +1559,8 @@
       let pnon' = inheritRpnon inst ++ (kpnon k)
       let unique' = inheritRunique inst ++ (kunique k)
       let k' = newPreskel (gen k) (protocol k) insts'
-           orderings' non' pnon' unique' (operation k) (prob k) (pov k)
+           orderings' non' pnon' unique' (kpriority k)
+           (operation k) (prob k) (pov k)
       k' <- wellFormedPreskel k'
       return (k0, k', n, phi, hsubst)
 
@@ -1637,7 +1651,8 @@
       homomorphismFilter prs
     where
       k' = newPreskel gen' (protocol k) insts' orderings' (knon k)
-           (kpnon k) (kunique k) (AddedListener t cause) (prob k) (pov k)
+           (kpnon k) (kunique k) (kpriority k)
+           (AddedListener t cause) (prob k) (pov k)
       (gen', inst) = mkListener (gen k) t
       insts' = insts k ++ [inst]
       pair = ((length (insts k), 1), n)
@@ -1785,7 +1800,7 @@
                   [Sid] -> Preskel t p g s e c
 deleteNodeRest k gen n insts' orderings prob =
     newPreskel gen (protocol k) insts' orderings non' pnon' unique'
-                   (Generalized (Deleted n)) prob (pov k)
+                   prio' (Generalized (Deleted n)) prob (pov k)
     where
       -- Drop nons that aren't mentioned anywhere
       non' = filter mentionedIn (knon k)
@@ -1795,6 +1810,10 @@
       -- Drop uniques that aren't held anywhere
       unique' = filter heldIn (kunique k)
       heldIn t = any (heldBy t) terms
+      -- Drop unused priorities
+      prio' = filter within (kpriority k)
+      within ((s, i), _) =
+        s < fst n || s == fst n && i < snd n
 
 -- Node ordering weakening
 
@@ -1824,7 +1843,7 @@
     addIdentity k'
     where
       k' = newPreskel (gen k) (protocol k) (insts k)
-           orderings (knon k) (kpnon k) (kunique k)
+           orderings (knon k) (kpnon k) (kunique k) (kpriority k)
            (Generalized (Weakened p)) (prob k) (pov k)
 
 -- Origination assumption forgetting
@@ -1982,10 +2001,10 @@
 changeLocations k env gen t locs =
     [addIdentity k0, addIdentity k1]
     where
-      k0 = newPreskel gen' (protocol k) insts' (orderings k)
-           non pnon unique0 (Generalized (Separated t)) (prob k) (pov k)
-      k1 = newPreskel gen' (protocol k) insts' (orderings k)
-           non pnon unique1 (Generalized (Separated t)) (prob k) (pov k)
+      k0 = newPreskel gen' (protocol k) insts' (orderings k) non pnon unique0
+           (kpriority k) (Generalized (Separated t)) (prob k) (pov k)
+      k1 = newPreskel gen' (protocol k) insts' (orderings k) non pnon unique1
+           (kpriority k) (Generalized (Separated t)) (prob k) (pov k)
       (gen', insts') = changeStrands locs t gen (strands k)
       non = knon k ++ map (instantiate env) (knon k)
       pnon = kpnon k ++ map (instantiate env) (kpnon k)
diff --git a/src/CPSA/Pretty/Main.hs b/src/CPSA/Pretty/Main.hs
--- a/src/CPSA/Pretty/Main.hs
+++ b/src/CPSA/Pretty/Main.hs
@@ -97,14 +97,14 @@
             do
               msg <- usage options ["Bad option combination\n"]
               abort msg
-          else             
+          else
             loop flags $ params { prefix = False }
       loop (Json : flags) params =
           if not (prefix params) then
             do
               msg <- usage options ["Bad option combination\n"]
               abort msg
-          else             
+          else
             loop flags $ params { json = True }
       loop (Margin value : flags) params =
           case readDec value of
diff --git a/src/CPSA/SimpleDiffieHellman/Algebra.hs b/src/CPSA/SimpleDiffieHellman/Algebra.hs
--- a/src/CPSA/SimpleDiffieHellman/Algebra.hs
+++ b/src/CPSA/SimpleDiffieHellman/Algebra.hs
@@ -15,7 +15,7 @@
 -- modify it under the terms of the BSD License as published by the
 -- University of California.
 
-{-# LANGUAGE MultiParamTypeClasses, CPP #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
 
 module CPSA.SimpleDiffieHellman.Algebra (name, origin) where
 
@@ -29,14 +29,6 @@
 import qualified CPSA.Lib.CPSA as C
 import CPSA.Lib.CPSA (SExpr(..), Pos, annotation)
 
--- Preserve the ability to use GHC 6.x
-foldrWithKey :: (k -> a -> b -> b) -> b -> Map k a -> b
-#if defined __GLASGOW_HASKELL__ && __GLASGOW_HASKELL__ < 700
-foldrWithKey = M.foldWithKey
-#else
-foldrWithKey = M.foldrWithKey
-#endif
-
 name :: String
 name = "diffie-hellman"
 
@@ -225,6 +217,10 @@
 varId (F Expn [I x]) = x
 varId _ = error "Algebra.varId: term not a variable with its sort"
 
+isMesgVar :: Term -> Bool
+isMesgVar (I _) = True
+isMesgVar _ = False
+
 -- A list of terms are well-formed if each one has the correct
 -- structure and every occurrence of an identifier in a term has the
 -- same sort.  Variable environments are used to check the sort
@@ -578,6 +574,7 @@
 
 instance C.Term Term where
     isVar = isVar
+    isMesgVar = isMesgVar
     isAtom = isAtom
     termsWellFormed = termsWellFormed
     occursIn = occursIn
@@ -945,7 +942,7 @@
 identityEnvFor (Env r) ts =
     all (allId $ flip S.notMember dom) ts
     where
-      dom = foldrWithKey f S.empty r -- The domain of r
+      dom = M.foldrWithKey f S.empty r -- The domain of r
       f x (I y) dom
           | x == y = dom        -- Ignore trivial bindings
           | otherwise = S.insert x dom
diff --git a/src/prover9.pl b/src/prover9.pl
--- a/src/prover9.pl
+++ b/src/prover9.pl
@@ -111,15 +111,15 @@
 
 %% Quantifiers forall and exists
 
-%% This code simply drops the sort declarations.
-
 quantifier(_, [[], Body], Pretty) :-
 	!,
 	form_to_pretty(Body, Pretty).
 quantifier(Kind, [Decls, Body], Pretty) :-
 	quantifier_op(Kind, Op),
-	decls(Decls, Vars),
-	quantifier_rest(Op, Vars, Body, Pretties),
+	decls(Decls, SVars),
+	quantifier_preds(SVars, Vars, Preds),
+	quantifier_body(Kind, Preds, Body, SBody),
+	quantifier_rest(Op, Vars, SBody, Pretties),
 	pp:blo(2, Pretties, Pretty).
 
 quantifier_op(forall, Pretty) :-
@@ -129,19 +129,44 @@
 
 %% Collect vars in declarations.
 
-decls(Decls, Vars) :-
-	decls(Decls, Vars, []).
+decls(Decls, SortedVars) :-
+	decls(Decls, SortedVars, []).
 
-decls([], Vars, Vars).
-decls([Decl|Decls], Vars, End) :-
-	decl(Decl, Vars, Middle),
+decls([], SVars, SVars).
+decls([Decl|Decls], SVars, End) :-
+	decl(Decl, _, SVars, Middle),
 	decls(Decls, Middle, End).
 
-decl([_], Vars, Vars).
-decl([Var|Decl], [Var|Vars], End) :-
+decl([Sort], Sort, SVars, SVars) :-
+	atom(Sort).
+decl([Var|Decl], Sort, [(Var,Sort)|SVars], End) :-
 	atom(Var),
-	decl(Decl, Vars, End).
+	decl(Decl, Sort, SVars, End).
 
+quantifier_preds([], [], []).
+quantifier_preds([(Var,mesg)|SVars], [Var|Vars], Preds) :-
+        !,
+        quantifier_preds(SVars, Vars, Preds).
+quantifier_preds([(Var,Sort)|SVars], [Var|Vars], [[Sort, Var]|Preds]) :-
+        quantifier_preds(SVars, Vars, Preds).
+
+quantifier_body(_, [], Body, Body) :-
+        !.
+quantifier_body(exists, Preds, [and|Forms], [and|Conj]) :-
+        !,
+        append(Preds, Forms, Conj).
+quantifier_body(exists, Preds, Body, [and|Conj]) :-
+        append(Preds, [Body], Conj).
+quantifier_body(forall, Preds, [implies, [and|Forms], Body],
+		[implies, [and|Conj], Body]) :-
+        !,
+        append(Preds, Forms, Conj).
+quantifier_body(forall, Preds, [implies, Form, Body],
+		[implies, [and|Conj], Body]) :-
+        !,
+        append(Preds, [Form], Conj).
+quantifier_body(forall, Preds, Body, [implies, [and|Preds], Body]).
+
 quantifier_rest(_, [], Body, [Left, Brk, Pretty, Right]) :-
 	pp:atm('(', Left),
 	pp:brk(0, Brk),
@@ -178,16 +203,11 @@
 	load_term(Term, Internal),
 	term_pp(Internal, Pretty).
 
-%% Load a term using CPSA's parsing rules for terms.  Also, convert
-%% variables into uppercase atoms, and constants into lowercase atoms.
+%% Load a term using CPSA's parsing rules for terms.
 
 load_term(Term, Internal) :-
 	atom(Term),
-	upcase_symbol(Term, Internal).
-load_term(Term, Internal) :-
-	string(Term),
-	string_to_atom(Term, Atom),
-	downcase_symbol(Atom, Internal).
+	load_atom(Term, Internal).
 load_term(Term, Term) :-
 	integer(Term),
 	Term >= 0.
@@ -208,28 +228,33 @@
 	atom(Term),
 	load_terms(Terms, Internals).
 
-upcase_symbol(Atom, Symbol) :-
-	atom_chars(Atom, Chars),
-	upcase_parts(Chars, Parts),
-	atom_chars(Symbol, Parts).
-
-upcase_parts([First|Rest], [Lead|Tail]) :-
-	upcase_atom(First, Lead),
-	symbol_parts(Rest, Tail).
+%% Convert variables into uppercase atoms, and constants into
+%% lowercase atoms.
 
-downcase_symbol(Atom, Symbol) :-
-	atom_chars(Atom, Chars),
-	downcase_parts(Chars, Parts),
+load_atom('""', []) :- % The name for a listener is the null constant.
+        !.
+load_atom(Atom, Symbol) :-
+        atom_chars(Atom, Chars),
+	parts(Chars, Parts),
 	atom_chars(Symbol, Parts).
 
-%% The null constant is used for the name of the listener role.
+parts(['"'|Chars], Parts) :-
+        !,
+        downcase_parts(Chars, Parts).
+parts(Chars, Parts) :-
+        upcase_parts(Chars, Parts).
 
-downcase_parts([], ['"', '"']).
 downcase_parts([First|Rest], [Lead|Tail]) :-
 	downcase_atom(First, Lead),
 	symbol_parts(Rest, Tail).
 
+upcase_parts([First|Rest], [Lead|Tail]) :-
+	upcase_atom(First, Lead),
+	symbol_parts(Rest, Tail).
+
 symbol_parts([], []).
+symbol_parts(['"'], []) :-
+        !.
 symbol_parts(['-'|Rest], ['_'|Tail]) :-
 	!,
 	symbol_parts(Rest, Tail).
diff --git a/tst/DH_hack.tst b/tst/DH_hack.tst
--- a/tst/DH_hack.tst
+++ b/tst/DH_hack.tst
@@ -1,6 +1,6 @@
 (herald "DH Hack" (bound 15))
 
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from DH_hack.scm")
 (comment "Strand count bounded at 15")
 
diff --git a/tst/blanchet.tst b/tst/blanchet.tst
--- a/tst/blanchet.tst
+++ b/tst/blanchet.tst
@@ -1,7 +1,7 @@
 (herald "Blanchet's Simple Example Protocol"
   (comment "There is a flaw in this protocol by design"))
 
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from blanchet.scm")
 
 (defprotocol blanchet basic
diff --git a/tst/completeness-test.tst b/tst/completeness-test.tst
--- a/tst/completeness-test.tst
+++ b/tst/completeness-test.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from completeness-test.scm")
 
 (defprotocol completeness-test basic
diff --git a/tst/crushing.tst b/tst/crushing.tst
--- a/tst/crushing.tst
+++ b/tst/crushing.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from crushing.scm")
 
 (defprotocol crushing basic
diff --git a/tst/dass_simple.tst b/tst/dass_simple.tst
--- a/tst/dass_simple.tst
+++ b/tst/dass_simple.tst
@@ -1,6 +1,6 @@
 (herald "Distributed Authentication Security Service Protocol Variants")
 
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from dass_simple.scm")
 
 (defprotocol dass-simple basic
diff --git a/tst/denning-sacco.tst b/tst/denning-sacco.tst
--- a/tst/denning-sacco.tst
+++ b/tst/denning-sacco.tst
@@ -1,6 +1,6 @@
 (herald "Denning-Sacco Protocol")
 
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from denning-sacco.scm")
 
 (defprotocol denning-sacco basic
diff --git a/tst/deorig_contract.tst b/tst/deorig_contract.tst
--- a/tst/deorig_contract.tst
+++ b/tst/deorig_contract.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from deorig_contract.scm")
 
 (defprotocol deorig-contract basic
diff --git a/tst/deorig_mesg.tst b/tst/deorig_mesg.tst
--- a/tst/deorig_mesg.tst
+++ b/tst/deorig_mesg.tst
@@ -1,6 +1,6 @@
 (herald deorig-mesg)
 
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from deorig_mesg.scm")
 
 (defprotocol deorig-mesg basic
diff --git a/tst/deorig_simple.tst b/tst/deorig_simple.tst
--- a/tst/deorig_simple.tst
+++ b/tst/deorig_simple.tst
@@ -1,6 +1,6 @@
 (herald deorig-simple)
 
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from deorig_simple.scm")
 
 (defprotocol deorig-simple basic
diff --git a/tst/dh_cert.tst b/tst/dh_cert.tst
--- a/tst/dh_cert.tst
+++ b/tst/dh_cert.tst
@@ -1,6 +1,6 @@
 (herald "Diffie-Hellman with Certificate" (algebra diffie-hellman))
 
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from dh_cert.scm")
 
 (defprotocol dh-cert diffie-hellman
diff --git a/tst/dhke.tst b/tst/dhke.tst
--- a/tst/dhke.tst
+++ b/tst/dhke.tst
@@ -1,6 +1,6 @@
 (herald "Diffie-Hellman Key Exchange" (algebra diffie-hellman))
 
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from dhke.scm")
 
 (defprotocol dhke diffie-hellman
diff --git a/tst/dy.tst b/tst/dy.tst
--- a/tst/dy.tst
+++ b/tst/dy.tst
@@ -1,6 +1,6 @@
 (herald "Example 1.3 from 1983 Dolev-Yao Paper")
 
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from dy.lsp")
 
 (defprotocol dy basic
diff --git a/tst/encsig.tst b/tst/encsig.tst
--- a/tst/encsig.tst
+++ b/tst/encsig.tst
@@ -1,7 +1,7 @@
 (herald "Encrypted Signed Message Example"
   (comment "Shows examples of key usage of asymmetric keys"))
 
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from encsig.scm")
 
 (defprotocol mult-keys-enc-sig basic
diff --git a/tst/epmo-hash.tst b/tst/epmo-hash.tst
--- a/tst/epmo-hash.tst
+++ b/tst/epmo-hash.tst
@@ -1,7 +1,7 @@
 (herald "Electronic Purchase with Money Order Protocol with Key Hashing"
   (comment "Annotated with trust management formulas"))
 
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from epmo-hash.scm")
 
 (defprotocol epmo basic
diff --git a/tst/epmo-key-hash.tst b/tst/epmo-key-hash.tst
--- a/tst/epmo-key-hash.tst
+++ b/tst/epmo-key-hash.tst
@@ -1,7 +1,7 @@
 (herald "Electronic Purchase with Money Order Protocol with Key Hashing"
   (comment "Annotated with trust management formulas"))
 
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from epmo-key-hash.scm")
 
 (defprotocol epmo basic
diff --git a/tst/epmo.tst b/tst/epmo.tst
--- a/tst/epmo.tst
+++ b/tst/epmo.tst
@@ -1,7 +1,7 @@
 (herald "Electronic Purchase with Money Order Protocol"
   (comment "Annotated with trust management formulas"))
 
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from epmo.scm")
 
 (defprotocol epmo basic
diff --git a/tst/epmo_acctnum-key-hash.tst b/tst/epmo_acctnum-key-hash.tst
--- a/tst/epmo_acctnum-key-hash.tst
+++ b/tst/epmo_acctnum-key-hash.tst
@@ -2,7 +2,7 @@
   "Electronic Purchase with Money Order Protocol Variant with Key Hashing"
   (comment "This version includes account numbers in exchanges"))
 
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from epmo_acctnum-key-hash.scm")
 
 (defprotocol epmo_acctnum basic
diff --git a/tst/epmo_acctnum.tst b/tst/epmo_acctnum.tst
# file too large to diff: tst/epmo_acctnum.tst
diff --git a/tst/ffgg.tst b/tst/ffgg.tst
--- a/tst/ffgg.tst
+++ b/tst/ffgg.tst
@@ -1,7 +1,7 @@
 (herald "The ffgg Protocol"
   (comment "From A Necessarily Parallel Attack by Jon K. Millen"))
 
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from ffgg.scm")
 
 (defprotocol ffgg basic
diff --git a/tst/fragile_pruning.tst b/tst/fragile_pruning.tst
--- a/tst/fragile_pruning.tst
+++ b/tst/fragile_pruning.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from fragile_pruning.scm")
 
 (defprotocol fragile_pruning basic
diff --git a/tst/hashtest-key-hash.tst b/tst/hashtest-key-hash.tst
--- a/tst/hashtest-key-hash.tst
+++ b/tst/hashtest-key-hash.tst
@@ -1,6 +1,6 @@
 (herald "Hashtest")
 
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from hashtest-key-hash.scm")
 
 (defprotocol hashtest basic
diff --git a/tst/hashtest.tst b/tst/hashtest.tst
--- a/tst/hashtest.tst
+++ b/tst/hashtest.tst
@@ -1,6 +1,6 @@
 (herald "Hashtest")
 
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from hashtest.scm")
 
 (defprotocol hashtest basic
diff --git a/tst/incompleteness_example.tst b/tst/incompleteness_example.tst
--- a/tst/incompleteness_example.tst
+++ b/tst/incompleteness_example.tst
@@ -1,8 +1,8 @@
 (herald incompleteness-example
   (comment "Shows a shape not found by CPSA"))
 
-(comment "CPSA 2.2.11")
-(comment "All input read from incompleteness-example.scm")
+(comment "CPSA 2.3.0")
+(comment "All input read from incompleteness_example.scm")
 
 (defprotocol incompleteness-example basic
   (defrole init
diff --git a/tst/isoreject.tst b/tst/isoreject.tst
--- a/tst/isoreject.tst
+++ b/tst/isoreject.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from isoreject.scm")
 
 (defprotocol isoreject basic
diff --git a/tst/kelly1.tst b/tst/kelly1.tst
--- a/tst/kelly1.tst
+++ b/tst/kelly1.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from kelly1.scm")
 
 (defprotocol kelly1 basic
diff --git a/tst/kerberos.tst b/tst/kerberos.tst
--- a/tst/kerberos.tst
+++ b/tst/kerberos.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from kerberos.scm")
 
 (defprotocol kerberos basic
diff --git a/tst/mass.tst b/tst/mass.tst
--- a/tst/mass.tst
+++ b/tst/mass.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from mass.lsp")
 
 (defprotocol mass basic
diff --git a/tst/mass2.tst b/tst/mass2.tst
--- a/tst/mass2.tst
+++ b/tst/mass2.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from mass2.lsp")
 
 (defprotocol mass2 basic
diff --git a/tst/missing_contraction.tst b/tst/missing_contraction.tst
--- a/tst/missing_contraction.tst
+++ b/tst/missing_contraction.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from missing_contraction.scm")
 
 (defprotocol missing-contraction basic
diff --git a/tst/neuman-stubblebine-reauth.tst b/tst/neuman-stubblebine-reauth.tst
--- a/tst/neuman-stubblebine-reauth.tst
+++ b/tst/neuman-stubblebine-reauth.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from neuman-stubblebine-reauth.lsp")
 
 (defprotocol neuman-stubblebine-reauth basic
diff --git a/tst/neuman-stubblebine.tst b/tst/neuman-stubblebine.tst
--- a/tst/neuman-stubblebine.tst
+++ b/tst/neuman-stubblebine.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from neuman-stubblebine.scm")
 
 (defprotocol neuman-stubblebine basic
diff --git a/tst/no_contraction.tst b/tst/no_contraction.tst
--- a/tst/no_contraction.tst
+++ b/tst/no_contraction.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from no_contraction.scm")
 
 (defprotocol no-contraction basic
diff --git a/tst/non_transforming.tst b/tst/non_transforming.tst
--- a/tst/non_transforming.tst
+++ b/tst/non_transforming.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from non_transforming.scm")
 
 (defprotocol non_transforming basic
diff --git a/tst/nonaug-prune.tst b/tst/nonaug-prune.tst
--- a/tst/nonaug-prune.tst
+++ b/tst/nonaug-prune.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from nonaug-prune.scm")
 
 (defprotocol nonaug-prune basic
diff --git a/tst/ns-l.tst b/tst/ns-l.tst
--- a/tst/ns-l.tst
+++ b/tst/ns-l.tst
@@ -1,7 +1,7 @@
 (herald "Needham-Schroeder-Low Public-Key Protocol"
   (comment "With deflistener's"))
 
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from ns-l.scm")
 
 (defprotocol ns basic
diff --git a/tst/ns.tst b/tst/ns.tst
--- a/tst/ns.tst
+++ b/tst/ns.tst
@@ -1,6 +1,6 @@
 (herald "Needham-Schroeder Public-Key Protocol Variants")
 
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from ns.scm")
 
 (defprotocol ns basic
diff --git a/tst/nsl3.tst b/tst/nsl3.tst
--- a/tst/nsl3.tst
+++ b/tst/nsl3.tst
@@ -1,6 +1,6 @@
 (herald "Three Party Needham-Schroeder-Lowe Protocol")
 
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from nsl3.scm")
 
 (defprotocol nsl3 basic
diff --git a/tst/nsl4cm1.tst b/tst/nsl4cm1.tst
# file too large to diff: tst/nsl4cm1.tst
diff --git a/tst/nslsk.tst b/tst/nslsk.tst
--- a/tst/nslsk.tst
+++ b/tst/nslsk.tst
@@ -1,6 +1,6 @@
 (herald "Needham-Schroeder-Lowe Protocol with symmetric encryption")
 
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from nslsk.scm")
 
 (defprotocol nslsk basic
diff --git a/tst/or.tst b/tst/or.tst
--- a/tst/or.tst
+++ b/tst/or.tst
@@ -1,7 +1,7 @@
 (herald "Otway-Rees Protocol"
   (comment "Standard version using variables of sort mesg"))
 
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from or.scm")
 
 (defprotocol or basic
diff --git a/tst/pca.tst b/tst/pca.tst
--- a/tst/pca.tst
+++ b/tst/pca.tst
@@ -1,7 +1,7 @@
 (herald "Privacy Certificate Authority" (bound 15)
   (comment "Generation of an Attestation Identity Certificate"))
 
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from pca.scm")
 (comment "Strand count bounded at 15")
 
diff --git a/tst/pen-non-orig-test.tst b/tst/pen-non-orig-test.tst
--- a/tst/pen-non-orig-test.tst
+++ b/tst/pen-non-orig-test.tst
@@ -1,6 +1,6 @@
 (herald "pen-non-orig test")
 
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from pen-non-orig-test.scm")
 
 (defprotocol pennonorigtest basic
diff --git a/tst/pkinit.tst b/tst/pkinit.tst
--- a/tst/pkinit.tst
+++ b/tst/pkinit.tst
@@ -1,6 +1,6 @@
 (herald "Kerberos PK init")
 
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from pkinit.scm")
 
 (defprotocol pkinit basic
diff --git a/tst/preprocess.tst b/tst/preprocess.tst
--- a/tst/preprocess.tst
+++ b/tst/preprocess.tst
@@ -1,6 +1,6 @@
 (herald "Pre-processing test example: modified NS with two responders")
 
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from preprocess.scm")
 
 (defprotocol ns basic
diff --git a/tst/print.tst b/tst/print.tst
--- a/tst/print.tst
+++ b/tst/print.tst
@@ -1,7 +1,7 @@
 (herald "Print Test"
   (comment "See if read forms look like printed ones"))
 
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from print.scm")
 
 (defprotocol print-test basic
diff --git a/tst/pruning1.tst b/tst/pruning1.tst
--- a/tst/pruning1.tst
+++ b/tst/pruning1.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from pruning1.scm")
 
 (defprotocol prune basic
diff --git a/tst/sigenc.tst b/tst/sigenc.tst
--- a/tst/sigenc.tst
+++ b/tst/sigenc.tst
@@ -1,7 +1,7 @@
 (herald "Signed Encrypted Message Example"
   (comment "Shows examples of key usage of asymmetric keys"))
 
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from sigenc.scm")
 
 (defprotocol mult-keys-sig-enc basic
diff --git a/tst/sorted_epmo_acctnum.tst b/tst/sorted_epmo_acctnum.tst
--- a/tst/sorted_epmo_acctnum.tst
+++ b/tst/sorted_epmo_acctnum.tst
@@ -4,7 +4,7 @@
     "This version uses sorts to avoid confusion"
     "between a nonce and other data"))
 
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from sorted_epmo_acctnum.scm")
 (comment "Strand count bounded at 12")
 
diff --git a/tst/targetterms2.tst b/tst/targetterms2.tst
--- a/tst/targetterms2.tst
+++ b/tst/targetterms2.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from targetterms2.scm")
 
 (defprotocol targetterms2 basic
diff --git a/tst/targetterms6.tst b/tst/targetterms6.tst
--- a/tst/targetterms6.tst
+++ b/tst/targetterms6.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from targetterms6.scm")
 
 (defprotocol targetterms6 basic
diff --git a/tst/targetterms8.tst b/tst/targetterms8.tst
--- a/tst/targetterms8.tst
+++ b/tst/targetterms8.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from targetterms8.scm")
 
 (defprotocol targetterms8 basic
diff --git a/tst/timestamping.tst b/tst/timestamping.tst
--- a/tst/timestamping.tst
+++ b/tst/timestamping.tst
@@ -1,6 +1,6 @@
 (herald timestamping-service)
 
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from timestamping.scm")
 
 (defprotocol timestamping-service basic
diff --git a/tst/tor.tst b/tst/tor.tst
--- a/tst/tor.tst
+++ b/tst/tor.tst
@@ -1,7 +1,7 @@
 (herald "Tor Circuit-Level Handshake Protocol" (algebra diffie-hellman)
   (comment "Achieves unilateral authentication"))
 
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from tor.scm")
 
 (defprotocol tor diffie-hellman
diff --git a/tst/uncarried_keys.tst b/tst/uncarried_keys.tst
--- a/tst/uncarried_keys.tst
+++ b/tst/uncarried_keys.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from uncarried_keys.scm")
 
 (defprotocol uncarried-keys basic
diff --git a/tst/uo.tst b/tst/uo.tst
--- a/tst/uo.tst
+++ b/tst/uo.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from uo.scm")
 
 (defprotocol uniq-orig basic
diff --git a/tst/wang-hash.tst b/tst/wang-hash.tst
--- a/tst/wang-hash.tst
+++ b/tst/wang-hash.tst
@@ -1,6 +1,6 @@
 (herald "Wang's Fair Exchange Protocol" (bound 10))
 
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from wang-hash.scm")
 (comment "Strand count bounded at 10")
 
diff --git a/tst/wang-key-hash.tst b/tst/wang-key-hash.tst
--- a/tst/wang-key-hash.tst
+++ b/tst/wang-key-hash.tst
@@ -1,6 +1,6 @@
 (herald "Wang's Fair Exchange Protocol" (bound 10))
 
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from wang-key-hash.scm")
 (comment "Strand count bounded at 10")
 
diff --git a/tst/weird.tst b/tst/weird.tst
--- a/tst/weird.tst
+++ b/tst/weird.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from weird.scm")
 
 (defprotocol weird basic
diff --git a/tst/wide-mouth-frog-scyther.tst b/tst/wide-mouth-frog-scyther.tst
--- a/tst/wide-mouth-frog-scyther.tst
+++ b/tst/wide-mouth-frog-scyther.tst
@@ -1,7 +1,7 @@
 (herald "Wide-Mouth Frog Protocol from Scyther"
   (comment "This protocol has an infinite number of shapes"))
 
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from wide-mouth-frog-scyther.lsp")
 
 (defprotocol wide-mouth-frog basic
diff --git a/tst/wide-mouth-frog.tst b/tst/wide-mouth-frog.tst
--- a/tst/wide-mouth-frog.tst
+++ b/tst/wide-mouth-frog.tst
@@ -1,7 +1,7 @@
 (herald "Wide-Mouth Frog Protocol"
   (comment "This protocol has an infinite number of shapes"))
 
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from wide-mouth-frog.lsp")
 
 (defprotocol wide-mouth-frog basic
diff --git a/tst/wonthull.tst b/tst/wonthull.tst
--- a/tst/wonthull.tst
+++ b/tst/wonthull.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from wonthull.scm")
 
 (defprotocol wonthull basic
diff --git a/tst/wonthull2.tst b/tst/wonthull2.tst
--- a/tst/wonthull2.tst
+++ b/tst/wonthull2.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from wonthull2.scm")
 
 (defprotocol wonthull2 basic
diff --git a/tst/wonthull3.tst b/tst/wonthull3.tst
--- a/tst/wonthull3.tst
+++ b/tst/wonthull3.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from wonthull3.scm")
 
 (defprotocol wonthull3 basic
diff --git a/tst/woolam.tst b/tst/woolam.tst
--- a/tst/woolam.tst
+++ b/tst/woolam.tst
@@ -1,6 +1,6 @@
 (herald "Woo-Lam Protocol")
 
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from woolam.scm")
 
 (defprotocol woolam basic
diff --git a/tst/yahalom-6.3.6.tst b/tst/yahalom-6.3.6.tst
--- a/tst/yahalom-6.3.6.tst
+++ b/tst/yahalom-6.3.6.tst
@@ -2,10 +2,12 @@
   (comment "A Survey of Authentication Protocol Literature:"
     "Version 1.0, John Clark and Jeremy Jacob,"
     "Yahalom Protocol, Section 6.3.6, Page 49")
-  (url "http://www.eecs.umich.edu/acal/swerve/docs/49-1.pdf"))
+  (url "http://www.eecs.umich.edu/acal/swerve/docs/49-1.pdf")
+  (bound 15))
 
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from yahalom-6.3.6.scm")
+(comment "Strand count bounded at 15")
 
 (defprotocol yahalom basic
   (defrole init
diff --git a/tst/yahalom.tst b/tst/yahalom.tst
--- a/tst/yahalom.tst
+++ b/tst/yahalom.tst
@@ -1,7 +1,8 @@
-(herald "Yahalom Protocol Without Forwarding")
+(herald "Yahalom Protocol Without Forwarding" (bound 15))
 
-(comment "CPSA 2.2.11")
+(comment "CPSA 2.3.0")
 (comment "All input read from yahalom.scm")
+(comment "Strand count bounded at 15")
 
 (defprotocol yahalom basic
   (defrole init