Some final minor changes before cutting 1.1.

* update documentation
* update the cut-release script
* spelling/wording updates
* add a (previously-failing) fuzzer regression

10 files changed, 1235 insertions, 69 deletions

diff --git a/AUTHORS b/AUTHORS
index 133786ae1..921985a4b 100644
--- a/AUTHORS
+++ b/AUTHORS
@@ -8,6 +8,7 @@ The core authors and designers of CVC4 are:
   Liana Hadarean <lianah@cs.nyu.edu>, New York University
   Dejan Jovanovic <dejan@cs.nyu.edu>, New York University
   Tim King <taking@cs.nyu.edu>, New York University
+  Tianyi Liang <tianyi-liang@uiowa.edu>, The University of Iowa
   Andrew Reynolds <andrew.j.reynolds@gmail.com>, The University of Iowa
   Cesare Tinelli <tinelli@cs.uiowa.edu>, The University of Iowa
 
diff --git a/INSTALL b/INSTALL
index 3dea1de7d..ff8824ef7 100644
--- a/INSTALL
+++ b/INSTALL
@@ -1,11 +1,12 @@
-CVC4 release version 1.0.
+CVC4 release version 1.1.
 
 *** Quick-start instructions
 
 *** Build dependences
 
-The following tools and libraries are required to run CVC4. Versions
-given are minimum versions; more recent versions should be compatible.
+The following tools and libraries are required to build and run CVC4.
+Versions given are minimum versions; more recent versions should be
+compatible.
 
   GNU C and C++ (gcc and g++), reasonably recent versions
   GNU Make
@@ -40,7 +41,7 @@ libantlr3c.  On a 32-bit machine, or if you have difficulty building
 libantlr3c (or difficulty getting CVC4 to link against it later), you
 may need to remove the --enable-64bit part in the script.  (If you're
 curious, the manual instructions are at
-http://church.cims.nyu.edu/wiki/Developer%27s_Guide#ANTLR3 .)
+http://cvc4.cs.nyu.edu/wiki/Developer%27s_Guide#ANTLR3 .)
 
 *** Building CVC4
 
@@ -173,6 +174,13 @@ cvc-users@cs.nyu.edu.
 
 *** Building CVC4 from a repository checkout
 
+CVC4's main repository is kept on GitHub at:
+
+  https://github.com/CVC4/CVC4
+
+and there are numerous experimental forks housed on GitHub as well,
+by different developers, implementing various features.
+
 The following tools and libraries are additionally required to build
 CVC4 from from a repository checkout rather than from a prepared
 source tarball.
diff --git a/NEWS b/NEWS
index 844610486..c68340442 100644
--- a/NEWS
+++ b/NEWS
@@ -5,19 +5,24 @@ Changes since 1.0
 
 * bit-vector solver now has a specialized decision procedure for unsigned bit-
   vector inequalities
-* tuple and record support in the compatibility library
-* user patterns are now supported in the SMT-LIBv1.2 parser
-* SMT-LIB get-model output now is easier to machine-parse: contains (model...)
+* numerous important bug fixes, performance improvements, and usability
+  improvements
+* support for multiline input in interactive mode
 * Win32-building support via mingw
-* for printing commands as they're invoked from the driver, you now need
-  verbosity of 3 or higher (e.g. -vvv) instead of verbosity 1 or higher (-v).
-  This allows tracing the solver's activities without having too much output.
-* multiline input support in interactive mode
-* To make CVC4 quieter in abnormal (e.g., "warning" conditions), you can
+* SMT-LIB get-model output now is easier to machine-parse: contains (model...)
+* user patterns for quantifier instantiation are now supported in the
+  SMT-LIBv1.2 parser
+* --finite-model-find was incomplete when using --incremental, now fixed
+* the E-matching procedure is slightly improved
+* Boolean terms are now supported in datatypes
+* tuple and record support have been added to the compatibility library
+* driver verbosity change: for printing all commands as they're executed, you
+  now need verbosity level >= 3 (e.g., -vvv) instead of level 1 (-v).  This
+  allows tracing the solver's activities (with -v and -vv) without having too
+  much output.
+* to make CVC4 quieter in abnormal (e.g., "warning" conditions), you can
   use -q.  Previously, this would silence all output (including "sat" or
   "unsat") as well.  Now, single -q silences messages and warnings, and
   double -qq silences all output (except on exception or signal).
-* Boolean term support in datatypes
-* numerous bug fixes, usability improvements, and build system improvements
 
--- Morgan Deters <mdeters@cs.nyu.edu>  Tue, 26 Mar 2013 15:17:52 -0400
+-- Morgan Deters <mdeters@cs.nyu.edu>  Wed, 03 Apr 2013 13:06:35 -0400
diff --git a/README b/README
index bedd7721a..bda916610 100644
--- a/README
+++ b/README
@@ -1,4 +1,4 @@
-This is CVC4 release version 1.0.  For build and installation notes,
+This is CVC4 release version 1.1.  For build and installation notes,
 please see the INSTALL file included with this distribution.
 
 This first official release of CVC4 is the result of more than three
diff --git a/RELEASE-NOTES b/RELEASE-NOTES
index 38d1459ad..43d87487a 100644
--- a/RELEASE-NOTES
+++ b/RELEASE-NOTES
@@ -1,4 +1,4 @@
-Release Notes for CVC4 1.0, December 2012
+Release Notes for CVC4 1.1, April 2013
 
 ** Getting started
 
@@ -17,7 +17,7 @@ this, you can use the --lang option.
 
 The CVC family of systems relies on Type Correctness Conditions (TCCs) when
 mixing two types that have a compatible base type.  TCCs, and the checking of
-such, are not supported by CVC4 1.0.  This is an issue when mixing integers and
+such, are not supported by CVC4 1.1.  This is an issue when mixing integers and
 reals.  A function defined only on integers can be applied to REAL (as INT is a
 subtype of REAL), and CVC4 will not complain.  It is up to the user to ensure 
 that the REAL expression must be an integer.  If the REAL expression is not
@@ -84,12 +84,12 @@ processed.
 
 For the latest news on SMT-LIB compliance, please check:
 
-  http://church.cims.nyu.edu/wiki/SMT-LIB_Compliance
+  http://cvc4.cs.nyu.edu/wiki/SMT-LIB_Compliance
 
 ** Getting statistics
 
 Statistics can be dumped on exit (both normal and abnormal exits) with
-the --statistics command line option.
+the --stats command line option.
 
 ** Time and resource limits
 
@@ -118,7 +118,7 @@ heap.
 
 ** Proof support
 
-CVC4 1.0 has limited support for proofs, and they are disabled by default.
+CVC4 1.1 has limited support for proofs, and they are disabled by default.
 (Run the configure script with --enable-proof to enable proofs).  Proofs
 are exported in LFSC format and are limited to the propositional backbone
 of the discovered proof (theory lemmas are stated without proof in this
@@ -126,7 +126,7 @@ release).
 
 ** Nonlinear arithmetic
 
-CVC4 1.0 has a state-of-the-art linear arithmetic solver.  However, there
+CVC4 1.1 has a state-of-the-art linear arithmetic solver.  However, there
 is extremely limited support for nonlinear arithmetic in this release.
 
 ** Portfolio solving
diff --git a/contrib/cut-release b/contrib/cut-release
index 2b7f6f683..03c8a3ed1 100755
--- a/contrib/cut-release
+++ b/contrib/cut-release
@@ -4,6 +4,9 @@
 #
 
 function isthatright {
+  if $dryrun; then
+    echo -n "[DRY RUN] "
+  fi
   if [ -z "$1" ]; then
     echo -n "Does that look right? [y/n] "
   else
@@ -24,6 +27,8 @@ function isthatright {
 if [ "$1" = -n ]; then
   dryrun=true
   shift
+  echo
+  echo '************************* DRY RUN *************************'
 else
   dryrun=false
 fi
@@ -34,8 +39,8 @@ if [ $# -lt 1 ]; then
   exit 1
 fi
 
-if ! [ -e src/expr/node.h -a -e .svn ]; then
-  echo "$(basename "$0"): ERROR: You should run this from the top-level of a CVC4 subversion working directory" >&2
+if ! [ -e src/expr/node.h -a -e .git ]; then
+  echo "$(basename "$0"): ERROR: You should run this from the top-level of a CVC4 git working directory" >&2
   exit 1
 fi
 
@@ -68,37 +73,32 @@ echo
 isthatright
 
 echo "Checking whether release \`$version' already exists..."
-if ! svn ls "https://subversive.cims.nyu.edu/cvc4/cvc4/tags/releases/$version" 2>&1 >/dev/null | grep non-existent >/dev/null; then
-  echo "$(basename "$0"): ERROR: Subversion repo already contains a release \`$version'" >&2
+if [ -n "`git tag -l "$version"`" ]; then
+  echo "$(basename "$0"): ERROR: Git repo already contains a release \`$version'" >&2
   $dryrun || exit 1
 fi
 
 echo "Checking working directory for local modifications..."
 if $dryrun; then
-  if [ -n "$(svn status -q configure.ac)" ]; then
+  if [ -n "$(git status -s configure.ac)" ]; then
     echo "$(basename "$0"): ERROR: In dry-run mode, cannot operate properly with local modifications to \"configure.ac\", sorry" >&2
     exit 1
   fi
-elif [ -n "$(svn status -q | grep -v '^M *[0-9]* *NEWS$')" ]; then
-  echo "$(basename "$0"): ERROR: \"svn status\" indicates there are local modifications; please commit first" >&2
+elif [ -n "$(git status -s | grep -v '^ *M *\(NEWS\|README\|AUTHORS\|RELEASE-NOTES\|INSTALL\|THANKS\|library_versions\|contrib/cut-release\)$')" ]; then
+  echo "$(basename "$0"): ERROR: \"git status\" indicates there are local modifications; please commit first" >&2
   exit 1
 fi
 
-root="$(svn info | grep "^Repository Root: https://subversive.cims.nyu.edu/.*" | cut -f3 -d' ')"
-if [ -z "$root" ]; then
-  echo "$(basename "$0"): ERROR: Can't get repository root URL" 2>&1
-  $dryrun || exit 1
-fi
-
 echo "Checking repo for unmerged updates..."
-if [ `svn -uq status | grep -v '^M *[0-9]* *NEWS$' | wc -l` -ne 1 ]; then
+git fetch &>/dev/null
+if git status -sb | grep -q '^## .* \[.*behind '; then
   echo "$(basename "$0"): ERROR: This working directory isn't up to date" 2>&1
   $dryrun || exit 1
 fi
 
 echo "Checking sources for broken public headers..."
 suspect_files="\
-$(grep -r --exclude-dir=.svn '^[ \t]*#[ \t]*include[ \t]*"[^/]*"' src |
+$(grep -r --exclude-dir=.git '^[ \t]*#[ \t]*include[ \t]*"[^/]*"' src |
   grep -v '"cvc4parser_public\.h"' |
   grep -v '"cvc4_public\.h"' |
   grep -v '"cvc4_private\.h"' |
@@ -110,24 +110,37 @@ $(grep -r --exclude-dir=.svn '^[ \t]*#[ \t]*include[ \t]*"[^/]*"' src |
   xargs echo)"
 if [ -n "$suspect_files" ]; then
   echo "$(basename "$0"): ERROR: The following publicly-installed headers appear" 2>&1
-  echo "$(basename "$0"): ERROR:   to have relative #includes and may be broken up" 2>&1
-  echo "$(basename "$0"): ERROR:   on install: $suspect_files" 2>&1
+  echo "$(basename "$0"): ERROR:   to have relative #includes and may be broken" 2>&1
+  echo "$(basename "$0"): ERROR:   after install: $suspect_files" 2>&1
   $dryrun || exit 1
 fi
 
-echo "Checking NEWS file for recent updates..."
-if [ -n "$(svn status -q NEWS)" ]; then
-  echo "+ It's locally modified."
-else
-  echo -n "+ "
-  svn info NEWS | grep '^Last Changed Date: '
-  echo
-  echo "You should probably make sure to put some notes in the NEWS file"
-  echo "for this release, indicating the most important changes from the"
-  echo "last release."
-  echo
-  isthatright "Continue without updating NEWS"
-fi
+for updatefile in NEWS README AUTHORS RELEASE-NOTES INSTALL THANKS; do
+  echo "Checking $updatefile file for recent updates..."
+  if [ -n "$(git status -s $updatefile)" ]; then
+    echo "+ It's locally modified."
+  else
+    git log -n 1 --date=local --pretty=format:'+ Last changed on %ad (%ar)' $updatefile
+    echo
+    case $updatefile in
+      NEWS)
+        echo "You should make sure to put some notes in the NEWS file for"
+        echo "release $version, indicating the most important changes since the"
+        echo "last release."
+        ;;
+      AUTHORS)
+        echo "You should make sure there are no new authors to list for $version."
+        ;;
+      *)
+        echo "You should ensure that $updatefile is appropriately updated"
+        echo "for $version before continuing.  (Maybe it even lists the previous"
+        echo "version number!)"
+        ;;
+    esac
+    echo
+    isthatright "Continue without updating $updatefile"
+  fi
+done
 
 echo "Adjusting version info lines in configure.ac..."
 if ! grep '^m4_define(_CVC4_MAJOR,  *[0-9][0-9]* *)' configure.ac &>/dev/null ||
@@ -142,12 +155,12 @@ perl -pi -e 's/^m4_define\(_CVC4_MAJOR, ( *)[0-9]+( *)\)/m4_define(_CVC4_MAJOR,
              s/^m4_define\(_CVC4_RELEASE, ( *)[0-9]+( *)\)/m4_define(_CVC4_RELEASE, ${1}'"$release"'$2)/;
              s/^m4_define\(_CVC4_EXTRAVERSION, ( *)\[.*\]( *)\)/m4_define(_CVC4_EXTRAVERSION, $1\['"$extra"'\]$2)/' configure.ac
 
-trap 'echo; echo; echo "Aborting in error."; svn revert configure.ac; echo' EXIT
+trap 'echo; echo; echo "Aborting in error."; git co -- configure.ac; echo' EXIT
 
 echo
 echo 'Made the following change to configure.ac:'
 echo
-svn diff configure.ac
+git diff configure.ac
 echo
 isthatright
 
@@ -158,8 +171,8 @@ if ! grep '^m4_define(_CVC4_MAJOR,  *'"$major"' *)' configure.ac &>/dev/null ||
   echo "$(basename "$0"): INTERNAL ERROR: Cannot find the modified version info lines in configure.ac, bailing..." >&2
   exit 1
 fi
-if [ -z "$(svn status -q configure.ac)" ]; then
-  echo "$(basename "$0"): INTERNAL ERROR: \"svn status\" indicates there are no local modifications to configure.ac; I expected the ones I just made!" >&2
+if [ -z "$(git status -s configure.ac)" ]; then
+  echo "$(basename "$0"): INTERNAL ERROR: \"git status\" indicates there are no local modifications to configure.ac; I expected the ones I just made!" >&2
   exit 1
 fi
 
@@ -219,36 +232,48 @@ gpg -b --armor "cvc4-$version.tar.gz"
 #cp -p "release-$version/src/main/pcvc4" "pcvc4-$version"
 #gpg -b --armor "pcvc4-$version"
 
+if $dryrun; then
+  echo
+  echo '************************* DRY RUN *************************'
+fi
+
 echo
-echo "About to run: svn commit -m \"Cutting release $version.\""
+echo "About to run: git commit -am \"Cutting release $version.\""
 isthatright
-$dryrun || svn commit -m "Cutting release $version."
+$dryrun || git commit -am "Cutting release $version."
 
 echo
-echo "About to run: svn copy -m \"Cutting release $version.\" \"$root\" \"https://subversive.cims.nyu.edu/cvc4/cvc4/tags/releases/$version\""
+echo "About to run: git tag \"$version\""
 isthatright
-$dryrun || svn copy -m "Cutting release $version." "$root" "https://subversive.cims.nyu.edu/cvc4/cvc4/tags/releases/$version"
+$dryrun || git tag "$version"
 
 echo
-if [ "$(svn info | grep '^URL: https://subversive.cims.nyu.edu/cvc4/cvc4/trunk$')" ]; then
+andbranch=
+if git status -bs | grep -q '^## master\($\|  *\)'; then
   if [ "$release" = 0 ]; then
-    echo "About to run: svn copy -m \"Branching release $version for bugfixes.\" \"https://subversive.cims.nyu.edu/cvc4/cvc4/tags/releases/$version\" \"https://subversive.cims.nyu.edu/cvc4/cvc4/branches/releases/$version.x\""
+    echo "About to run: git branch \"$version.x\""
     isthatright
-    $dryrun || svn copy -m "Branching release $version for bugfixes." "https://subversive.cims.nyu.edu/cvc4/cvc4/tags/releases/$version" "https://subversive.cims.nyu.edu/cvc4/cvc4/branches/releases/$version.x"
+    $dryrun || git branch "$version.x"
+    andbranch=", the $version.x branch,"
   else
     echo "Not branching, because this is a minor release (i.e., not a \"dot-oh\""
-    echo "release), so I'm guessing you have a devel repository outside of trunk"
+    echo "release), so I'm guessing you have a devel branch outside of master"
     echo "somewhere?  You can still make a branch manually, of course."
   fi
 else
   echo "Not branching, because it appears there already is a branch"
-  echo "to work with for version $version ..?  (You're not on trunk.)"
+  echo "to work with for version $version ..?  (You're not on master.)"
   echo "You can still make a branch manually, of course."
 fi
 
 echo
-echo "Done.  Next steps are to upload and advertise these packages and to add"
-echo "a $version release to Bugzilla."
+echo "Done.  Next steps are to:"
+echo
+echo "1. push to GitHub (don't forget to push master$andbranch and the $version tag)"
+echo "2. upload source and binaries"
+echo "3. advertise these packages"
+echo "4. add a $version release and next-milestone to Bugzilla."
+echo
 
 trap '' EXIT
 
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index fad6c1839..9abdaa034 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -299,7 +299,7 @@ class TheoryEngine {
       NodeManager* curr = NodeManager::currentNM();
       Node restartVar =  curr->mkSkolem("restartVar",
                                         curr->booleanType(),
-                                        "A boolean variable assrted to be true to force a restart");
+                                        "A boolean variable asserted to be true to force a restart");
       Trace("theory::restart") << "EngineOutputChannel<" << d_theory << ">::restart(" << restartVar << ")" << std::endl;
       ++ d_statistics.restartDemands;
       lemma(restartVar, true);
diff --git a/test/regress/regress0/auflia/Makefile.am b/test/regress/regress0/auflia/Makefile.am
index a649cfef5..5a6ab9e2b 100644
--- a/test/regress/regress0/auflia/Makefile.am
+++ b/test/regress/regress0/auflia/Makefile.am
@@ -22,6 +22,7 @@ TESTS =	\
 	fuzz05.smt \
 	fuzz06.smt \
 	fuzz-error232.smt \
+	fuzz-error1099.smt \
 	a17.smt \
 	error72.delta2.smt \
 	x2.smt
diff --git a/test/regress/regress0/auflia/fuzz-error1099.smt b/test/regress/regress0/auflia/fuzz-error1099.smt
new file mode 100644
index 000000000..6a465abac
--- /dev/null
+++ b/test/regress/regress0/auflia/fuzz-error1099.smt
@@ -0,0 +1,1126 @@
+(benchmark fuzzsmt
+:logic AUFLIA
+:status sat
+:extrafuns ((f0 Int Int Int))
+:extrafuns ((f1 Array Array Array Array))
+:extrapreds ((p0 Int))
+:extrapreds ((p1 Array))
+:extrafuns ((v0 Int))
+:extrafuns ((v1 Int))
+:extrafuns ((v2 Int))
+:extrafuns ((v3 Array))
+:assumption
+(forall (?qvar0 Int) 
+(exists (?qvar1 Int) (?qvar2 Int) (?qvar3 Int) 
+(flet ($qf0 (p0 ?qvar1))
+(flet ($qf1 (p0 ?qvar2))
+(flet ($qf2 (p0 ?qvar2))
+(flet ($qf3 (< (f0 ?qvar0 ?qvar1) (f0 ?qvar2 ?qvar0)))
+(flet ($qf4 (p0 ?qvar1))
+(flet ($qf5 (p0 ?qvar1))
+(flet ($qf6 (= (f0 ?qvar0 ?qvar3) (f0 ?qvar3 ?qvar2)))
+(flet ($qf7 (if_then_else $qf2 $qf3 $qf5))
+(flet ($qf8 (if_then_else $qf6 $qf7 $qf6))
+(flet ($qf9 (or $qf0 $qf0))
+(flet ($qf10 (iff $qf8 $qf8))
+(flet ($qf11 (and $qf9 $qf1))
+(flet ($qf12 (iff $qf4 $qf10))
+(flet ($qf13 (or $qf11 $qf12))
+$qf13
+))))))))))))))))
+:formula
+(let (?e4 14)
+(let (?e5 0)
+(let (?e6 13)
+(let (?e7 (~ v0))
+(let (?e8 (~ v2))
+(let (?e9 (- v1 v2))
+(let (?e10 (* ?e8 (~ ?e6)))
+(let (?e11 (ite (p0 v0) 1 0))
+(let (?e12 (+ v1 ?e9))
+(let (?e13 (+ ?e10 v0))
+(let (?e14 (- v1 ?e12))
+(let (?e15 (+ ?e8 v0))
+(let (?e16 (f0 ?e8 ?e14))
+(let (?e17 (+ ?e15 ?e10))
+(let (?e18 (f0 v2 v1))
+(let (?e19 (+ v2 ?e12))
+(let (?e20 (f0 ?e17 v2))
+(let (?e21 (~ ?e7))
+(let (?e22 (* ?e13 ?e6))
+(let (?e23 (~ ?e9))
+(let (?e24 (~ ?e13))
+(let (?e25 (~ ?e13))
+(let (?e26 (* v2 ?e6))
+(let (?e27 (~ ?e8))
+(let (?e28 (~ ?e16))
+(let (?e29 (f0 ?e25 ?e27))
+(let (?e30 (* ?e9 ?e5))
+(let (?e31 (- ?e10 ?e29))
+(let (?e32 (f0 ?e18 ?e16))
+(let (?e33 (~ ?e27))
+(let (?e34 (+ ?e25 ?e9))
+(let (?e35 (~ ?e21))
+(let (?e36 (ite (p0 ?e25) 1 0))
+(let (?e37 (+ ?e12 ?e20))
+(let (?e38 (* ?e4 ?e25))
+(let (?e39 (select v3 ?e28))
+(let (?e40 (select v3 ?e23))
+(let (?e41 (f1 v3 v3 v3))
+(flet ($e42 (p1 ?e41))
+(flet ($e43 (p1 ?e41))
+(flet ($e44 (p1 ?e41))
+(flet ($e45 (p1 v3))
+(flet ($e46 (p0 ?e24))
+(flet ($e47 (= ?e32 ?e15))
+(flet ($e48 (> ?e33 ?e9))
+(flet ($e49 (<= ?e23 ?e8))
+(flet ($e50 (= v2 ?e40))
+(flet ($e51 (>= v0 ?e24))
+(flet ($e52 (distinct ?e29 ?e28))
+(flet ($e53 (>= ?e21 ?e21))
+(flet ($e54 (> ?e14 ?e34))
+(flet ($e55 (<= ?e24 ?e21))
+(flet ($e56 (> ?e26 ?e38))
+(flet ($e57 (< ?e35 v0))
+(flet ($e58 (p0 ?e37))
+(flet ($e59 (>= ?e30 ?e13))
+(flet ($e60 (= ?e12 ?e19))
+(flet ($e61 (<= ?e21 ?e27))
+(flet ($e62 (p0 ?e17))
+(flet ($e63 (distinct ?e31 ?e40))
+(flet ($e64 (>= ?e7 ?e12))
+(flet ($e65 (= ?e12 ?e28))
+(flet ($e66 (>= ?e11 v0))
+(flet ($e67 (p0 ?e17))
+(flet ($e68 (= ?e22 ?e18))
+(flet ($e69 (= ?e39 ?e8))
+(flet ($e70 (= ?e26 ?e12))
+(flet ($e71 (> v1 ?e22))
+(flet ($e72 (distinct ?e10 ?e34))
+(flet ($e73 (<= ?e36 ?e13))
+(flet ($e74 (> ?e20 ?e13))
+(flet ($e75 (> ?e25 ?e17))
+(flet ($e76 (< ?e10 ?e15))
+(flet ($e77 (> ?e16 ?e28))
+(let (?e78 (ite $e48 v3 ?e41))
+(let (?e79 (ite $e44 v3 ?e78))
+(let (?e80 (ite $e73 v3 ?e78))
+(let (?e81 (ite $e75 ?e79 ?e79))
+(let (?e82 (ite $e59 ?e81 ?e78))
+(let (?e83 (ite $e66 ?e81 ?e80))
+(let (?e84 (ite $e71 ?e80 ?e79))
+(let (?e85 (ite $e52 ?e78 ?e84))
+(let (?e86 (ite $e55 ?e80 ?e83))
+(let (?e87 (ite $e65 ?e41 ?e83))
+(let (?e88 (ite $e55 ?e80 ?e78))
+(let (?e89 (ite $e73 ?e80 ?e82))
+(let (?e90 (ite $e64 ?e87 v3))
+(let (?e91 (ite $e53 ?e85 ?e86))
+(let (?e92 (ite $e61 ?e80 ?e90))
+(let (?e93 (ite $e51 ?e92 ?e86))
+(let (?e94 (ite $e50 ?e84 ?e89))
+(let (?e95 (ite $e60 ?e91 ?e78))
+(let (?e96 (ite $e76 ?e87 ?e83))
+(let (?e97 (ite $e69 ?e95 ?e41))
+(let (?e98 (ite $e69 ?e88 ?e41))
+(let (?e99 (ite $e54 ?e93 ?e92))
+(let (?e100 (ite $e49 ?e86 ?e85))
+(let (?e101 (ite $e46 ?e92 ?e88))
+(let (?e102 (ite $e76 ?e79 ?e86))
+(let (?e103 (ite $e43 ?e83 ?e94))
+(let (?e104 (ite $e42 ?e79 ?e91))
+(let (?e105 (ite $e58 ?e100 ?e87))
+(let (?e106 (ite $e75 ?e95 ?e80))
+(let (?e107 (ite $e47 ?e100 ?e95))
+(let (?e108 (ite $e61 ?e97 ?e86))
+(let (?e109 (ite $e57 ?e87 ?e80))
+(let (?e110 (ite $e77 ?e106 ?e84))
+(let (?e111 (ite $e70 v3 ?e41))
+(let (?e112 (ite $e67 ?e96 ?e104))
+(let (?e113 (ite $e65 ?e84 ?e103))
+(let (?e114 (ite $e60 ?e101 ?e78))
+(let (?e115 (ite $e72 ?e91 ?e110))
+(let (?e116 (ite $e74 ?e110 ?e87))
+(let (?e117 (ite $e63 ?e106 ?e102))
+(let (?e118 (ite $e54 ?e108 ?e99))
+(let (?e119 (ite $e45 ?e93 ?e91))
+(let (?e120 (ite $e75 ?e117 ?e78))
+(let (?e121 (ite $e62 ?e108 ?e106))
+(let (?e122 (ite $e64 ?e79 ?e106))
+(let (?e123 (ite $e42 ?e104 ?e83))
+(let (?e124 (ite $e63 ?e88 ?e111))
+(let (?e125 (ite $e54 ?e81 ?e103))
+(let (?e126 (ite $e58 ?e99 ?e79))
+(let (?e127 (ite $e54 ?e83 ?e101))
+(let (?e128 (ite $e75 ?e101 ?e83))
+(let (?e129 (ite $e56 ?e84 ?e106))
+(let (?e130 (ite $e63 ?e110 ?e103))
+(let (?e131 (ite $e68 ?e80 v3))
+(let (?e132 (ite $e50 ?e16 ?e27))
+(let (?e133 (ite $e47 v1 ?e19))
+(let (?e134 (ite $e69 ?e38 ?e26))
+(let (?e135 (ite $e62 ?e17 ?e19))
+(let (?e136 (ite $e44 ?e30 ?e38))
+(let (?e137 (ite $e67 ?e15 ?e7))
+(let (?e138 (ite $e72 ?e33 ?e12))
+(let (?e139 (ite $e46 v2 v1))
+(let (?e140 (ite $e53 ?e39 ?e36))
+(let (?e141 (ite $e60 ?e11 ?e18))
+(let (?e142 (ite $e61 ?e32 ?e134))
+(let (?e143 (ite $e49 ?e24 ?e22))
+(let (?e144 (ite $e66 ?e28 ?e24))
+(let (?e145 (ite $e76 ?e8 ?e35))
+(let (?e146 (ite $e64 ?e22 ?e134))
+(let (?e147 (ite $e51 ?e9 ?e18))
+(let (?e148 (ite $e56 ?e34 ?e27))
+(let (?e149 (ite $e42 ?e137 ?e28))
+(let (?e150 (ite $e56 ?e20 ?e18))
+(let (?e151 (ite $e75 ?e23 ?e35))
+(let (?e152 (ite $e76 ?e28 ?e134))
+(let (?e153 (ite $e76 ?e13 ?e24))
+(let (?e154 (ite $e45 v0 ?e10))
+(let (?e155 (ite $e43 ?e37 ?e15))
+(let (?e156 (ite $e47 ?e33 ?e155))
+(let (?e157 (ite $e48 ?e151 ?e26))
+(let (?e158 (ite $e70 ?e154 ?e140))
+(let (?e159 (ite $e77 ?e14 ?e17))
+(let (?e160 (ite $e71 ?e27 ?e132))
+(let (?e161 (ite $e44 ?e38 ?e136))
+(let (?e162 (ite $e57 ?e40 ?e14))
+(let (?e163 (ite $e52 ?e31 ?e26))
+(let (?e164 (ite $e74 ?e11 ?e28))
+(let (?e165 (ite $e50 ?e24 ?e154))
+(let (?e166 (ite $e73 ?e132 ?e27))
+(let (?e167 (ite $e68 ?e153 ?e24))
+(let (?e168 (ite $e64 ?e164 ?e148))
+(let (?e169 (ite $e63 ?e38 ?e26))
+(let (?e170 (ite $e45 ?e32 ?e14))
+(let (?e171 (ite $e61 ?e162 ?e11))
+(let (?e172 (ite $e45 ?e29 ?e137))
+(let (?e173 (ite $e54 ?e143 ?e144))
+(let (?e174 (ite $e53 ?e25 ?e155))
+(let (?e175 (ite $e69 ?e147 ?e174))
+(let (?e176 (ite $e65 ?e21 ?e160))
+(let (?e177 (ite $e59 ?e26 ?e158))
+(let (?e178 (ite $e55 ?e172 ?e138))
+(let (?e179 (ite $e67 ?e173 ?e153))
+(let (?e180 (ite $e58 ?e37 ?e26))
+(let (?e181 (select ?e115 ?e140))
+(let (?e182 (select ?e113 ?e144))
+(let (?e183 (f1 ?e122 ?e107 ?e127))
+(let (?e184 (f1 ?e100 ?e120 ?e122))
+(let (?e185 (f1 ?e124 ?e101 ?e97))
+(let (?e186 (f1 ?e102 ?e183 ?e101))
+(let (?e187 (f1 ?e123 ?e123 ?e123))
+(let (?e188 (f1 ?e101 ?e84 ?e113))
+(let (?e189 (f1 ?e117 ?e117 ?e41))
+(let (?e190 (f1 ?e185 ?e117 ?e106))
+(let (?e191 (f1 ?e103 ?e101 ?e103))
+(let (?e192 (f1 ?e126 ?e126 ?e126))
+(let (?e193 (f1 ?e108 ?e106 ?e128))
+(let (?e194 (f1 ?e85 ?e109 ?e103))
+(let (?e195 (f1 ?e125 ?e88 ?e83))
+(let (?e196 (f1 ?e99 ?e185 ?e87))
+(let (?e197 (f1 ?e196 ?e97 ?e129))
+(let (?e198 (f1 ?e116 ?e186 ?e126))
+(let (?e199 (f1 ?e88 ?e125 ?e195))
+(let (?e200 (f1 ?e114 ?e114 ?e114))
+(let (?e201 (f1 ?e81 ?e199 ?e131))
+(let (?e202 (f1 ?e103 ?e183 ?e130))
+(let (?e203 (f1 ?e41 ?e115 ?e93))
+(let (?e204 (f1 ?e82 ?e103 ?e202))
+(let (?e205 (f1 ?e117 ?e188 ?e109))
+(let (?e206 (f1 ?e104 ?e195 ?e130))
+(let (?e207 (f1 ?e119 ?e106 ?e84))
+(let (?e208 (f1 ?e103 ?e108 ?e88))
+(let (?e209 (f1 ?e98 ?e117 ?e203))
+(let (?e210 (f1 ?e196 ?e91 ?e85))
+(let (?e211 (f1 ?e118 ?e105 ?e95))
+(let (?e212 (f1 ?e95 ?e190 ?e195))
+(let (?e213 (f1 ?e112 ?e112 ?e209))
+(let (?e214 (f1 ?e99 ?e205 ?e104))
+(let (?e215 (f1 ?e86 ?e86 ?e197))
+(let (?e216 (f1 ?e89 ?e89 ?e89))
+(let (?e217 (f1 ?e78 ?e78 ?e78))
+(let (?e218 (f1 ?e90 ?e130 ?e123))
+(let (?e219 (f1 ?e202 ?e91 ?e86))
+(let (?e220 (f1 ?e92 ?e212 ?e123))
+(let (?e221 (f1 ?e129 ?e187 ?e78))
+(let (?e222 (f1 ?e111 ?e216 ?e220))
+(let (?e223 (f1 ?e126 ?e212 ?e112))
+(let (?e224 (f1 ?e111 ?e186 ?e187))
+(let (?e225 (f1 ?e79 ?e101 ?e115))
+(let (?e226 (f1 ?e92 ?e223 ?e117))
+(let (?e227 (f1 ?e80 ?e80 ?e120))
+(let (?e228 (f1 ?e94 ?e94 ?e94))
+(let (?e229 (f1 v3 v3 v3))
+(let (?e230 (f1 ?e121 ?e121 ?e226))
+(let (?e231 (f1 ?e94 ?e189 ?e126))
+(let (?e232 (f1 ?e99 ?e109 ?e98))
+(let (?e233 (f1 ?e110 ?e110 ?e110))
+(let (?e234 (f1 ?e211 ?e194 ?e108))
+(let (?e235 (f1 ?e96 ?e96 ?e81))
+(let (?e236 (f0 ?e179 ?e136))
+(let (?e237 (- ?e159 ?e38))
+(let (?e238 (ite (p0 ?e23) 1 0))
+(let (?e239 (* ?e173 (~ ?e4)))
+(let (?e240 (+ ?e29 ?e154))
+(let (?e241 (+ ?e28 ?e144))
+(let (?e242 (~ ?e16))
+(let (?e243 (~ ?e27))
+(let (?e244 (* ?e172 ?e4))
+(let (?e245 (+ ?e10 ?e31))
+(let (?e246 (* ?e4 ?e20))
+(let (?e247 (~ ?e154))
+(let (?e248 (+ ?e33 ?e23))
+(let (?e249 (* ?e35 (~ ?e4)))
+(let (?e250 (* ?e177 (~ ?e4)))
+(let (?e251 (- ?e16 ?e39))
+(let (?e252 (- ?e137 v1))
+(let (?e253 (* ?e31 (~ ?e4)))
+(let (?e254 (ite (p0 ?e150) 1 0))
+(let (?e255 (ite (p0 ?e38) 1 0))
+(let (?e256 (* ?e18 ?e6))
+(let (?e257 (ite (p0 ?e159) 1 0))
+(let (?e258 (+ ?e133 ?e181))
+(let (?e259 (* ?e6 v0))
+(let (?e260 (- ?e151 ?e31))
+(let (?e261 (f0 ?e12 ?e142))
+(let (?e262 (* ?e171 (~ ?e5)))
+(let (?e263 (* ?e176 (~ ?e6)))
+(let (?e264 (- ?e250 ?e38))
+(let (?e265 (f0 ?e153 ?e133))
+(let (?e266 (ite (p0 ?e138) 1 0))
+(let (?e267 (f0 ?e257 ?e151))
+(let (?e268 (* (~ ?e5) ?e174))
+(let (?e269 (ite (p0 ?e144) 1 0))
+(let (?e270 (f0 ?e132 v1))
+(let (?e271 (* ?e174 ?e6))
+(let (?e272 (- ?e7 ?e165))
+(let (?e273 (f0 ?e9 ?e243))
+(let (?e274 (- ?e148 ?e269))
+(let (?e275 (f0 ?e26 ?e132))
+(let (?e276 (ite (p0 ?e178) 1 0))
+(let (?e277 (+ ?e272 ?e172))
+(let (?e278 (+ ?e30 ?e261))
+(let (?e279 (+ ?e167 ?e143))
+(let (?e280 (* ?e247 (~ ?e4)))
+(let (?e281 (+ ?e154 ?e27))
+(let (?e282 (* ?e168 (~ ?e5)))
+(let (?e283 (+ ?e139 ?e21))
+(let (?e284 (+ ?e175 ?e180))
+(let (?e285 (* ?e4 ?e271))
+(let (?e286 (ite (p0 ?e244) 1 0))
+(let (?e287 (* ?e6 ?e152))
+(let (?e288 (- ?e168 ?e36))
+(let (?e289 (* ?e144 (~ ?e5)))
+(let (?e290 (f0 ?e17 ?e148))
+(let (?e291 (ite (p0 ?e176) 1 0))
+(let (?e292 (f0 ?e10 ?e284))
+(let (?e293 (ite (p0 ?e279) 1 0))
+(let (?e294 (~ ?e158))
+(let (?e295 (ite (p0 ?e146) 1 0))
+(let (?e296 (+ ?e29 ?e273))
+(let (?e297 (* ?e149 (~ ?e4)))
+(let (?e298 (~ ?e11))
+(let (?e299 (f0 ?e161 ?e162))
+(let (?e300 (ite (p0 ?e240) 1 0))
+(let (?e301 (f0 ?e182 ?e256))
+(let (?e302 (f0 ?e238 ?e31))
+(let (?e303 (f0 ?e236 ?e274))
+(let (?e304 (ite (p0 ?e19) 1 0))
+(let (?e305 (+ ?e143 ?e291))
+(let (?e306 (f0 ?e167 ?e166))
+(let (?e307 (* ?e5 ?e147))
+(let (?e308 (ite (p0 ?e169) 1 0))
+(let (?e309 (ite (p0 ?e25) 1 0))
+(let (?e310 (f0 ?e34 ?e280))
+(let (?e311 (- ?e24 ?e182))
+(let (?e312 (+ v2 ?e245))
+(let (?e313 (* ?e282 (~ ?e6)))
+(let (?e314 (~ ?e172))
+(let (?e315 (f0 ?e170 ?e294))
+(let (?e316 (* (~ ?e5) ?e147))
+(let (?e317 (+ ?e14 ?e245))
+(let (?e318 (f0 ?e141 ?e153))
+(let (?e319 (* ?e297 ?e6))
+(let (?e320 (+ ?e135 ?e311))
+(let (?e321 (f0 ?e138 ?e241))
+(let (?e322 (ite (p0 ?e156) 1 0))
+(let (?e323 (- ?e13 ?e260))
+(let (?e324 (f0 ?e243 ?e12))
+(let (?e325 (~ ?e31))
+(let (?e326 (* ?e6 ?e180))
+(let (?e327 (f0 ?e140 ?e276))
+(let (?e328 (- ?e253 ?e271))
+(let (?e329 (- ?e32 ?e20))
+(let (?e330 (* ?e6 ?e145))
+(let (?e331 (+ ?e22 ?e277))
+(let (?e332 (+ ?e163 ?e269))
+(let (?e333 (- ?e9 ?e246))
+(let (?e334 (f0 ?e157 ?e173))
+(let (?e335 (+ ?e33 v0))
+(let (?e336 (* ?e40 (~ ?e4)))
+(let (?e337 (- ?e330 ?e7))
+(let (?e338 (ite (p0 ?e160) 1 0))
+(let (?e339 (f0 ?e164 ?e242))
+(let (?e340 (* ?e5 ?e156))
+(let (?e341 (- ?e8 ?e259))
+(let (?e342 (+ ?e134 ?e160))
+(let (?e343 (f0 ?e165 ?e305))
+(let (?e344 (ite (p0 ?e37) 1 0))
+(let (?e345 (f0 ?e293 ?e278))
+(let (?e346 (f0 ?e155 ?e153))
+(let (?e347 (+ ?e40 ?e325))
+(let (?e348 (~ ?e15))
+(flet ($e349 (p1 ?e190))
+(flet ($e350 (p1 ?e214))
+(flet ($e351 (p1 ?e80))
+(flet ($e352 (p1 ?e203))
+(flet ($e353 (p1 ?e116))
+(flet ($e354 (p1 ?e209))
+(flet ($e355 (p1 ?e232))
+(flet ($e356 (p1 ?e81))
+(flet ($e357 (p1 ?e183))
+(flet ($e358 (p1 ?e95))
+(flet ($e359 (p1 ?e206))
+(flet ($e360 (p1 ?e196))
+(flet ($e361 (p1 ?e232))
+(flet ($e362 (p1 ?e234))
+(flet ($e363 (p1 ?e230))
+(flet ($e364 (p1 ?e80))
+(flet ($e365 (p1 ?e212))
+(flet ($e366 (p1 ?e186))
+(flet ($e367 (p1 ?e234))
+(flet ($e368 (p1 ?e104))
+(flet ($e369 (p1 ?e198))
+(flet ($e370 (p1 ?e128))
+(flet ($e371 (p1 ?e189))
+(flet ($e372 (p1 ?e120))
+(flet ($e373 (p1 ?e91))
+(flet ($e374 (p1 ?e233))
+(flet ($e375 (p1 ?e191))
+(flet ($e376 (p1 ?e227))
+(flet ($e377 (p1 ?e197))
+(flet ($e378 (p1 ?e119))
+(flet ($e379 (p1 ?e129))
+(flet ($e380 (p1 ?e101))
+(flet ($e381 (p1 ?e117))
+(flet ($e382 (p1 ?e105))
+(flet ($e383 (p1 ?e216))
+(flet ($e384 (p1 ?e199))
+(flet ($e385 (p1 ?e130))
+(flet ($e386 (p1 ?e93))
+(flet ($e387 (p1 ?e93))
+(flet ($e388 (p1 ?e226))
+(flet ($e389 (p1 ?e207))
+(flet ($e390 (p1 ?e90))
+(flet ($e391 (p1 ?e127))
+(flet ($e392 (p1 ?e124))
+(flet ($e393 (p1 ?e84))
+(flet ($e394 (p1 ?e222))
+(flet ($e395 (p1 ?e220))
+(flet ($e396 (p1 ?e107))
+(flet ($e397 (p1 ?e223))
+(flet ($e398 (p1 ?e193))
+(flet ($e399 (p1 ?e187))
+(flet ($e400 (p1 ?e188))
+(flet ($e401 (p1 ?e228))
+(flet ($e402 (p1 ?e195))
+(flet ($e403 (p1 ?e211))
+(flet ($e404 (p1 ?e219))
+(flet ($e405 (p1 ?e229))
+(flet ($e406 (p1 ?e186))
+(flet ($e407 (p1 ?e79))
+(flet ($e408 (p1 ?e231))
+(flet ($e409 (p1 ?e94))
+(flet ($e410 (p1 ?e208))
+(flet ($e411 (p1 ?e192))
+(flet ($e412 (p1 ?e203))
+(flet ($e413 (p1 ?e100))
+(flet ($e414 (p1 ?e208))
+(flet ($e415 (p1 ?e86))
+(flet ($e416 (p1 ?e121))
+(flet ($e417 (p1 ?e193))
+(flet ($e418 (p1 ?e118))
+(flet ($e419 (p1 ?e126))
+(flet ($e420 (p1 ?e110))
+(flet ($e421 (p1 ?e187))
+(flet ($e422 (p1 ?e123))
+(flet ($e423 (p1 ?e214))
+(flet ($e424 (p1 ?e106))
+(flet ($e425 (p1 ?e122))
+(flet ($e426 (p1 ?e87))
+(flet ($e427 (p1 ?e220))
+(flet ($e428 (p1 ?e198))
+(flet ($e429 (p1 ?e100))
+(flet ($e430 (p1 ?e107))
+(flet ($e431 (p1 ?e100))
+(flet ($e432 (p1 ?e113))
+(flet ($e433 (p1 ?e97))
+(flet ($e434 (p1 ?e114))
+(flet ($e435 (p1 ?e221))
+(flet ($e436 (p1 ?e113))
+(flet ($e437 (p1 ?e128))
+(flet ($e438 (p1 ?e212))
+(flet ($e439 (p1 ?e225))
+(flet ($e440 (p1 ?e130))
+(flet ($e441 (p1 ?e131))
+(flet ($e442 (p1 ?e102))
+(flet ($e443 (p1 ?e217))
+(flet ($e444 (p1 ?e205))
+(flet ($e445 (p1 ?e221))
+(flet ($e446 (p1 ?e115))
+(flet ($e447 (p1 ?e115))
+(flet ($e448 (p1 ?e92))
+(flet ($e449 (p1 ?e122))
+(flet ($e450 (p1 ?e232))
+(flet ($e451 (p1 ?e215))
+(flet ($e452 (p1 ?e86))
+(flet ($e453 (p1 ?e210))
+(flet ($e454 (p1 ?e125))
+(flet ($e455 (p1 ?e88))
+(flet ($e456 (p1 ?e99))
+(flet ($e457 (p1 ?e186))
+(flet ($e458 (p1 ?e94))
+(flet ($e459 (p1 ?e96))
+(flet ($e460 (p1 ?e110))
+(flet ($e461 (p1 ?e198))
+(flet ($e462 (p1 ?e123))
+(flet ($e463 (p1 ?e111))
+(flet ($e464 (p1 ?e196))
+(flet ($e465 (p1 ?e217))
+(flet ($e466 (p1 ?e217))
+(flet ($e467 (p1 ?e98))
+(flet ($e468 (p1 ?e184))
+(flet ($e469 (p1 ?e118))
+(flet ($e470 (p1 ?e91))
+(flet ($e471 (p1 ?e201))
+(flet ($e472 (p1 ?e200))
+(flet ($e473 (p1 ?e109))
+(flet ($e474 (p1 ?e103))
+(flet ($e475 (p1 v3))
+(flet ($e476 (p1 ?e117))
+(flet ($e477 (p1 ?e114))
+(flet ($e478 (p1 ?e108))
+(flet ($e479 (p1 ?e215))
+(flet ($e480 (p1 ?e82))
+(flet ($e481 (p1 ?e83))
+(flet ($e482 (p1 ?e235))
+(flet ($e483 (p1 ?e213))
+(flet ($e484 (p1 ?e112))
+(flet ($e485 (p1 ?e197))
+(flet ($e486 (p1 ?e90))
+(flet ($e487 (p1 ?e107))
+(flet ($e488 (p1 ?e85))
+(flet ($e489 (p1 ?e193))
+(flet ($e490 (p1 ?e220))
+(flet ($e491 (p1 ?e194))
+(flet ($e492 (p1 ?e224))
+(flet ($e493 (p1 ?e183))
+(flet ($e494 (p1 ?e89))
+(flet ($e495 (p1 ?e85))
+(flet ($e496 (p1 ?e109))
+(flet ($e497 (p1 ?e202))
+(flet ($e498 (p1 ?e41))
+(flet ($e499 (p1 ?e98))
+(flet ($e500 (p1 ?e221))
+(flet ($e501 (p1 ?e193))
+(flet ($e502 (p1 ?e185))
+(flet ($e503 (p1 ?e124))
+(flet ($e504 (p1 ?e204))
+(flet ($e505 (p1 ?e78))
+(flet ($e506 (p1 ?e209))
+(flet ($e507 (p1 ?e218))
+(flet ($e508 (distinct ?e34 ?e35))
+(flet ($e509 (p0 ?e150))
+(flet ($e510 (<= ?e311 ?e23))
+(flet ($e511 (> ?e271 ?e241))
+(flet ($e512 (p0 ?e135))
+(flet ($e513 (<= ?e335 ?e345))
+(flet ($e514 (< ?e301 ?e158))
+(flet ($e515 (>= ?e269 ?e340))
+(flet ($e516 (< ?e27 ?e132))
+(flet ($e517 (p0 ?e147))
+(flet ($e518 (< ?e38 ?e13))
+(flet ($e519 (>= ?e31 ?e146))
+(flet ($e520 (>= ?e32 ?e175))
+(flet ($e521 (<= ?e304 ?e317))
+(flet ($e522 (< ?e166 ?e341))
+(flet ($e523 (< ?e166 ?e169))
+(flet ($e524 (>= ?e282 ?e283))
+(flet ($e525 (distinct ?e27 ?e134))
+(flet ($e526 (<= ?e298 ?e151))
+(flet ($e527 (= v1 ?e137))
+(flet ($e528 (< v0 ?e285))
+(flet ($e529 (p0 ?e284))
+(flet ($e530 (< ?e332 ?e345))
+(flet ($e531 (= ?e316 ?e38))
+(flet ($e532 (p0 ?e155))
+(flet ($e533 (<= ?e293 ?e335))
+(flet ($e534 (> ?e20 ?e279))
+(flet ($e535 (= ?e8 ?e178))
+(flet ($e536 (= ?e167 ?e237))
+(flet ($e537 (>= ?e310 ?e347))
+(flet ($e538 (distinct ?e253 ?e182))
+(flet ($e539 (distinct ?e170 ?e10))
+(flet ($e540 (= ?e326 ?e255))
+(flet ($e541 (< ?e241 ?e286))
+(flet ($e542 (p0 ?e40))
+(flet ($e543 (> v2 ?e340))
+(flet ($e544 (p0 ?e346))
+(flet ($e545 (>= ?e242 ?e132))
+(flet ($e546 (distinct ?e328 ?e132))
+(flet ($e547 (>= ?e285 ?e281))
+(flet ($e548 (> ?e299 ?e290))
+(flet ($e549 (p0 ?e236))
+(flet ($e550 (> ?e181 ?e244))
+(flet ($e551 (<= ?e17 ?e175))
+(flet ($e552 (< ?e14 ?e37))
+(flet ($e553 (distinct ?e329 ?e137))
+(flet ($e554 (> ?e320 ?e150))
+(flet ($e555 (= ?e144 ?e236))
+(flet ($e556 (<= ?e34 ?e169))
+(flet ($e557 (<= ?e348 v1))
+(flet ($e558 (<= ?e29 ?e320))
+(flet ($e559 (distinct ?e39 ?e260))
+(flet ($e560 (< ?e265 ?e329))
+(flet ($e561 (> ?e346 ?e278))
+(flet ($e562 (> ?e273 ?e11))
+(flet ($e563 (> ?e250 ?e251))
+(flet ($e564 (= ?e315 ?e298))
+(flet ($e565 (p0 ?e239))
+(flet ($e566 (< ?e36 ?e153))
+(flet ($e567 (> ?e165 ?e148))
+(flet ($e568 (> ?e344 ?e14))
+(flet ($e569 (p0 ?e19))
+(flet ($e570 (distinct ?e177 ?e135))
+(flet ($e571 (< ?e255 ?e272))
+(flet ($e572 (= ?e176 ?e10))
+(flet ($e573 (>= ?e11 ?e179))
+(flet ($e574 (>= ?e241 ?e257))
+(flet ($e575 (= ?e256 ?e283))
+(flet ($e576 (>= ?e318 ?e282))
+(flet ($e577 (< ?e142 ?e296))
+(flet ($e578 (distinct ?e174 ?e296))
+(flet ($e579 (= ?e339 ?e156))
+(flet ($e580 (> ?e300 ?e319))
+(flet ($e581 (>= ?e270 ?e33))
+(flet ($e582 (= ?e163 ?e158))
+(flet ($e583 (= ?e336 ?e14))
+(flet ($e584 (> ?e274 ?e140))
+(flet ($e585 (> ?e245 ?e326))
+(flet ($e586 (p0 ?e21))
+(flet ($e587 (distinct ?e300 ?e37))
+(flet ($e588 (= ?e314 ?e314))
+(flet ($e589 (<= ?e132 ?e333))
+(flet ($e590 (p0 ?e266))
+(flet ($e591 (< ?e152 ?e168))
+(flet ($e592 (= ?e13 ?e178))
+(flet ($e593 (distinct ?e246 ?e248))
+(flet ($e594 (> ?e254 ?e144))
+(flet ($e595 (> ?e277 ?e338))
+(flet ($e596 (p0 ?e181))
+(flet ($e597 (< ?e28 ?e154))
+(flet ($e598 (= ?e270 ?e320))
+(flet ($e599 (distinct ?e276 ?e163))
+(flet ($e600 (> ?e293 ?e281))
+(flet ($e601 (> ?e18 ?e136))
+(flet ($e602 (= ?e334 ?e22))
+(flet ($e603 (<= ?e258 ?e339))
+(flet ($e604 (>= ?e344 ?e288))
+(flet ($e605 (<= ?e237 ?e176))
+(flet ($e606 (< ?e143 ?e288))
+(flet ($e607 (= ?e24 ?e309))
+(flet ($e608 (distinct ?e180 ?e176))
+(flet ($e609 (p0 ?e345))
+(flet ($e610 (> ?e295 ?e298))
+(flet ($e611 (distinct ?e164 ?e307))
+(flet ($e612 (p0 ?e322))
+(flet ($e613 (<= ?e261 ?e307))
+(flet ($e614 (< ?e145 ?e347))
+(flet ($e615 (= ?e346 ?e156))
+(flet ($e616 (distinct ?e264 ?e344))
+(flet ($e617 (< ?e133 ?e274))
+(flet ($e618 (p0 ?e320))
+(flet ($e619 (distinct ?e13 ?e283))
+(flet ($e620 (< ?e323 ?e335))
+(flet ($e621 (> ?e305 ?e133))
+(flet ($e622 (p0 ?e317))
+(flet ($e623 (distinct ?e309 ?e139))
+(flet ($e624 (distinct ?e237 ?e26))
+(flet ($e625 (< ?e313 ?e242))
+(flet ($e626 (> ?e140 ?e140))
+(flet ($e627 (>= ?e20 ?e19))
+(flet ($e628 (>= ?e13 ?e268))
+(flet ($e629 (p0 ?e294))
+(flet ($e630 (distinct ?e291 ?e13))
+(flet ($e631 (>= ?e238 ?e325))
+(flet ($e632 (distinct ?e161 ?e146))
+(flet ($e633 (>= ?e142 ?e36))
+(flet ($e634 (< ?e247 ?e254))
+(flet ($e635 (< ?e157 ?e181))
+(flet ($e636 (p0 ?e275))
+(flet ($e637 (< ?e30 ?e24))
+(flet ($e638 (p0 ?e302))
+(flet ($e639 (> ?e162 ?e344))
+(flet ($e640 (>= ?e327 ?e344))
+(flet ($e641 (distinct ?e151 ?e348))
+(flet ($e642 (> ?e9 ?e257))
+(flet ($e643 (< ?e155 ?e181))
+(flet ($e644 (> v2 ?e296))
+(flet ($e645 (distinct ?e257 ?e39))
+(flet ($e646 (> ?e173 ?e286))
+(flet ($e647 (>= ?e23 ?e338))
+(flet ($e648 (<= ?e342 ?e346))
+(flet ($e649 (<= ?e336 ?e292))
+(flet ($e650 (= ?e15 ?e303))
+(flet ($e651 (= ?e16 ?e31))
+(flet ($e652 (< ?e38 ?e327))
+(flet ($e653 (< ?e294 ?e265))
+(flet ($e654 (= ?e171 ?e16))
+(flet ($e655 (< ?e284 ?e179))
+(flet ($e656 (> ?e252 ?e342))
+(flet ($e657 (= ?e149 ?e40))
+(flet ($e658 (distinct ?e12 ?e169))
+(flet ($e659 (> ?e249 ?e180))
+(flet ($e660 (distinct ?e272 ?e308))
+(flet ($e661 (p0 ?e287))
+(flet ($e662 (> ?e337 ?e7))
+(flet ($e663 (< ?e159 ?e26))
+(flet ($e664 (>= ?e138 ?e304))
+(flet ($e665 (distinct ?e303 ?e19))
+(flet ($e666 (distinct ?e324 ?e339))
+(flet ($e667 (p0 ?e171))
+(flet ($e668 (>= ?e154 ?e19))
+(flet ($e669 (> ?e30 ?e36))
+(flet ($e670 (> ?e267 ?e275))
+(flet ($e671 (= ?e291 ?e258))
+(flet ($e672 (< ?e257 ?e292))
+(flet ($e673 (> ?e312 ?e32))
+(flet ($e674 (> ?e25 ?e179))
+(flet ($e675 (distinct ?e170 ?e344))
+(flet ($e676 (distinct ?e132 ?e151))
+(flet ($e677 (>= ?e141 ?e241))
+(flet ($e678 (< ?e280 ?e303))
+(flet ($e679 (< ?e306 v1))
+(flet ($e680 (>= ?e259 ?e176))
+(flet ($e681 (>= ?e338 ?e245))
+(flet ($e682 (> ?e330 ?e256))
+(flet ($e683 (> ?e160 ?e154))
+(flet ($e684 (>= ?e9 ?e239))
+(flet ($e685 (>= ?e331 ?e285))
+(flet ($e686 (> ?e321 ?e333))
+(flet ($e687 (< ?e343 ?e249))
+(flet ($e688 (= ?e158 ?e291))
+(flet ($e689 (p0 ?e274))
+(flet ($e690 (>= ?e331 ?e245))
+(flet ($e691 (<= ?e289 ?e347))
+(flet ($e692 (<= ?e138 ?e18))
+(flet ($e693 (< ?e297 ?e311))
+(flet ($e694 (<= ?e243 ?e17))
+(flet ($e695 (<= ?e263 ?e346))
+(flet ($e696 (p0 ?e240))
+(flet ($e697 (<= ?e306 ?e141))
+(flet ($e698 (= ?e290 ?e181))
+(flet ($e699 (= ?e262 ?e342))
+(flet ($e700 (= ?e172 ?e284))
+(flet ($e701 (or $e695 $e668))
+(flet ($e702 (or $e373 $e424))
+(flet ($e703 (and $e522 $e652))
+(flet ($e704 (if_then_else $e62 $e599 $e392))
+(flet ($e705 (or $e636 $e409))
+(flet ($e706 (xor $e72 $e622))
+(flet ($e707 (implies $e677 $e545))
+(flet ($e708 (or $e613 $e582))
+(flet ($e709 (or $e386 $e655))
+(flet ($e710 (if_then_else $e43 $e621 $e541))
+(flet ($e711 (implies $e588 $e614))
+(flet ($e712 (if_then_else $e403 $e436 $e539))
+(flet ($e713 (and $e681 $e604))
+(flet ($e714 (iff $e400 $e57))
+(flet ($e715 (not $e435))
+(flet ($e716 (if_then_else $e450 $e697 $e547))
+(flet ($e717 (implies $e607 $e438))
+(flet ($e718 (or $e714 $e444))
+(flet ($e719 (or $e443 $e395))
+(flet ($e720 (if_then_else $e446 $e398 $e675))
+(flet ($e721 (and $e470 $e76))
+(flet ($e722 (iff $e388 $e510))
+(flet ($e723 (if_then_else $e75 $e427 $e640))
+(flet ($e724 (iff $e375 $e679))
+(flet ($e725 (implies $e421 $e653))
+(flet ($e726 (not $e54))
+(flet ($e727 (iff $e565 $e466))
+(flet ($e728 (or $e724 $e459))
+(flet ($e729 (implies $e65 $e524))
+(flet ($e730 (if_then_else $e384 $e667 $e608))
+(flet ($e731 (xor $e486 $e442))
+(flet ($e732 (not $e698))
+(flet ($e733 (and $e518 $e645))
+(flet ($e734 (not $e529))
+(flet ($e735 (implies $e523 $e708))
+(flet ($e736 (not $e729))
+(flet ($e737 (implies $e59 $e479))
+(flet ($e738 (xor $e553 $e511))
+(flet ($e739 (or $e74 $e540))
+(flet ($e740 (implies $e456 $e557))
+(flet ($e741 (if_then_else $e644 $e377 $e46))
+(flet ($e742 (xor $e380 $e720))
+(flet ($e743 (implies $e663 $e405))
+(flet ($e744 (iff $e683 $e502))
+(flet ($e745 (and $e691 $e391))
+(flet ($e746 (or $e457 $e627))
+(flet ($e747 (xor $e69 $e743))
+(flet ($e748 (iff $e671 $e658))
+(flet ($e749 (and $e702 $e531))
+(flet ($e750 (or $e487 $e705))
+(flet ($e751 (and $e366 $e696))
+(flet ($e752 (and $e390 $e717))
+(flet ($e753 (not $e354))
+(flet ($e754 (if_then_else $e734 $e509 $e587))
+(flet ($e755 (iff $e631 $e372))
+(flet ($e756 (if_then_else $e478 $e356 $e48))
+(flet ($e757 (and $e497 $e725))
+(flet ($e758 (and $e617 $e418))
+(flet ($e759 (not $e441))
+(flet ($e760 (xor $e549 $e733))
+(flet ($e761 (if_then_else $e731 $e693 $e475))
+(flet ($e762 (xor $e750 $e469))
+(flet ($e763 (not $e572))
+(flet ($e764 (not $e445))
+(flet ($e765 (implies $e472 $e596))
+(flet ($e766 (and $e60 $e422))
+(flet ($e767 (or $e710 $e431))
+(flet ($e768 (and $e460 $e73))
+(flet ($e769 (not $e465))
+(flet ($e770 (not $e581))
+(flet ($e771 (or $e639 $e699))
+(flet ($e772 (if_then_else $e464 $e692 $e609))
+(flet ($e773 (if_then_else $e563 $e685 $e381))
+(flet ($e774 (or $e704 $e625))
+(flet ($e775 (and $e404 $e651))
+(flet ($e776 (not $e597))
+(flet ($e777 (or $e566 $e352))
+(flet ($e778 (not $e741))
+(flet ($e779 (and $e577 $e593))
+(flet ($e780 (iff $e642 $e763))
+(flet ($e781 (xor $e64 $e420))
+(flet ($e782 (iff $e562 $e575))
+(flet ($e783 (or $e430 $e727))
+(flet ($e784 (xor $e453 $e52))
+(flet ($e785 (implies $e71 $e739))
+(flet ($e786 (xor $e632 $e63))
+(flet ($e787 (implies $e49 $e473))
+(flet ($e788 (implies $e528 $e555))
+(flet ($e789 (if_then_else $e661 $e748 $e481))
+(flet ($e790 (xor $e713 $e361))
+(flet ($e791 (and $e67 $e783))
+(flet ($e792 (not $e791))
+(flet ($e793 (not $e483))
+(flet ($e794 (or $e730 $e56))
+(flet ($e795 (not $e394))
+(flet ($e796 (if_then_else $e784 $e496 $e51))
+(flet ($e797 (implies $e690 $e350))
+(flet ($e798 (xor $e389 $e519))
+(flet ($e799 (xor $e703 $e629))
+(flet ($e800 (if_then_else $e349 $e360 $e526))
+(flet ($e801 (not $e684))
+(flet ($e802 (xor $e425 $e462))
+(flet ($e803 (xor $e458 $e532))
+(flet ($e804 (implies $e778 $e439))
+(flet ($e805 (or $e618 $e707))
+(flet ($e806 (iff $e770 $e795))
+(flet ($e807 (implies $e546 $e365))
+(flet ($e808 (and $e408 $e47))
+(flet ($e809 (and $e358 $e584))
+(flet ($e810 (if_then_else $e500 $e536 $e680))
+(flet ($e811 (iff $e423 $e550))
+(flet ($e812 (xor $e635 $e689))
+(flet ($e813 (iff $e754 $e506))
+(flet ($e814 (iff $e809 $e601))
+(flet ($e815 (xor $e637 $e633))
+(flet ($e816 (if_then_else $e673 $e490 $e504))
+(flet ($e817 (or $e538 $e371))
+(flet ($e818 (xor $e77 $e591))
+(flet ($e819 (implies $e58 $e382))
+(flet ($e820 (xor $e804 $e674))
+(flet ($e821 (or $e753 $e628))
+(flet ($e822 (or $e719 $e558))
+(flet ($e823 (xor $e780 $e535))
+(flet ($e824 (and $e737 $e448))
+(flet ($e825 (or $e771 $e811))
+(flet ($e826 (not $e559))
+(flet ($e827 (implies $e682 $e414))
+(flet ($e828 (implies $e790 $e53))
+(flet ($e829 (if_then_else $e759 $e626 $e45))
+(flet ($e830 (not $e449))
+(flet ($e831 (or $e471 $e564))
+(flet ($e832 (implies $e586 $e687))
+(flet ($e833 (if_then_else $e686 $e814 $e568))
+(flet ($e834 (implies $e567 $e385))
+(flet ($e835 (or $e505 $e461))
+(flet ($e836 (xor $e779 $e738))
+(flet ($e837 (implies $e756 $e406))
+(flet ($e838 (if_then_else $e611 $e722 $e777))
+(flet ($e839 (implies $e433 $e428))
+(flet ($e840 (or $e484 $e672))
+(flet ($e841 (and $e548 $e374))
+(flet ($e842 (and $e833 $e669))
+(flet ($e843 (iff $e837 $e634))
+(flet ($e844 (or $e772 $e806))
+(flet ($e845 (or $e595 $e495))
+(flet ($e846 (implies $e646 $e561))
+(flet ($e847 (implies $e751 $e721))
+(flet ($e848 (if_then_else $e551 $e747 $e508))
+(flet ($e849 (if_then_else $e796 $e801 $e802))
+(flet ($e850 (if_then_else $e527 $e616 $e42))
+(flet ($e851 (implies $e507 $e752))
+(flet ($e852 (if_then_else $e606 $e827 $e590))
+(flet ($e853 (iff $e825 $e768))
+(flet ($e854 (if_then_else $e569 $e583 $e774))
+(flet ($e855 (iff $e787 $e396))
+(flet ($e856 (if_then_else $e513 $e718 $e755))
+(flet ($e857 (or $e468 $e376))
+(flet ($e858 (iff $e855 $e823))
+(flet ($e859 (xor $e854 $e670))
+(flet ($e860 (implies $e357 $e516))
+(flet ($e861 (if_then_else $e859 $e849 $e412))
+(flet ($e862 (or $e474 $e775))
+(flet ($e863 (iff $e781 $e831))
+(flet ($e864 (and $e455 $e740))
+(flet ($e865 (iff $e419 $e701))
+(flet ($e866 (if_then_else $e578 $e794 $e50))
+(flet ($e867 (or $e589 $e454))
+(flet ($e868 (if_then_else $e841 $e525 $e762))
+(flet ($e869 (and $e648 $e765))
+(flet ($e870 (or $e851 $e353))
+(flet ($e871 (and $e364 $e853))
+(flet ($e872 (xor $e813 $e817))
+(flet ($e873 (not $e429))
+(flet ($e874 (or $e761 $e715))
+(flet ($e875 (xor $e800 $e840))
+(flet ($e876 (not $e848))
+(flet ($e877 (or $e716 $e368))
+(flet ($e878 (and $e657 $e847))
+(flet ($e879 (xor $e514 $e818))
+(flet ($e880 (iff $e592 $e447))
+(flet ($e881 (and $e440 $e678))
+(flet ($e882 (and $e826 $e411))
+(flet ($e883 (xor $e432 $e757))
+(flet ($e884 (and $e832 $e351))
+(flet ($e885 (iff $e610 $e877))
+(flet ($e886 (and $e624 $e55))
+(flet ($e887 (and $e498 $e764))
+(flet ($e888 (and $e416 $e362))
+(flet ($e889 (iff $e410 $e819))
+(flet ($e890 (not $e594))
+(flet ($e891 (and $e600 $e735))
+(flet ($e892 (implies $e863 $e489))
+(flet ($e893 (or $e712 $e874))
+(flet ($e894 (xor $e688 $e688))
+(flet ($e895 (and $e786 $e370))
+(flet ($e896 (not $e570))
+(flet ($e897 (not $e649))
+(flet ($e898 (xor $e797 $e820))
+(flet ($e899 (iff $e369 $e852))
+(flet ($e900 (not $e893))
+(flet ($e901 (if_then_else $e660 $e485 $e534))
+(flet ($e902 (or $e650 $e709))
+(flet ($e903 (and $e619 $e758))
+(flet ($e904 (not $e799))
+(flet ($e905 (or $e902 $e630))
+(flet ($e906 (xor $e662 $e706))
+(flet ($e907 (xor $e864 $e766))
+(flet ($e908 (or $e402 $e760))
+(flet ($e909 (and $e493 $e463))
+(flet ($e910 (and $e723 $e785))
+(flet ($e911 (if_then_else $e834 $e654 $e605))
+(flet ($e912 (xor $e615 $e846))
+(flet ($e913 (xor $e554 $e530))
+(flet ($e914 (not $e451))
+(flet ($e915 (not $e665))
+(flet ($e916 (xor $e835 $e560))
+(flet ($e917 (iff $e782 $e393))
+(flet ($e918 (if_then_else $e492 $e61 $e875))
+(flet ($e919 (xor $e838 $e892))
+(flet ($e920 (and $e437 $e769))
+(flet ($e921 (not $e773))
+(flet ($e922 (and $e480 $e571))
+(flet ($e923 (iff $e656 $e857))
+(flet ($e924 (xor $e367 $e873))
+(flet ($e925 (and $e886 $e732))
+(flet ($e926 (or $e861 $e641))
+(flet ($e927 (xor $e517 $e901))
+(flet ($e928 (not $e927))
+(flet ($e929 (or $e711 $e920))
+(flet ($e930 (or $e363 $e808))
+(flet ($e931 (not $e912))
+(flet ($e932 (if_then_else $e881 $e397 $e910))
+(flet ($e933 (xor $e824 $e70))
+(flet ($e934 (iff $e700 $e850))
+(flet ($e935 (iff $e891 $e909))
+(flet ($e936 (not $e383))
+(flet ($e937 (implies $e576 $e935))
+(flet ($e938 (if_then_else $e579 $e807 $e387))
+(flet ($e939 (iff $e598 $e925))
+(flet ($e940 (not $e862))
+(flet ($e941 (implies $e643 $e844))
+(flet ($e942 (xor $e894 $e895))
+(flet ($e943 (or $e896 $e736))
+(flet ($e944 (if_then_else $e872 $e482 $e866))
+(flet ($e945 (not $e792))
+(flet ($e946 (if_then_else $e830 $e491 $e638))
+(flet ($e947 (iff $e919 $e533))
+(flet ($e948 (if_then_else $e666 $e860 $e915))
+(flet ($e949 (iff $e44 $e836))
+(flet ($e950 (implies $e520 $e869))
+(flet ($e951 (implies $e776 $e889))
+(flet ($e952 (or $e949 $e574))
+(flet ($e953 (if_then_else $e694 $e659 $e821))
+(flet ($e954 (iff $e789 $e664))
+(flet ($e955 (or $e911 $e884))
+(flet ($e956 (and $e544 $e544))
+(flet ($e957 (implies $e926 $e941))
+(flet ($e958 (not $e950))
+(flet ($e959 (xor $e945 $e767))
+(flet ($e960 (not $e612))
+(flet ($e961 (implies $e899 $e868))
+(flet ($e962 (and $e870 $e379))
+(flet ($e963 (if_then_else $e933 $e960 $e913))
+(flet ($e964 (not $e865))
+(flet ($e965 (xor $e788 $e918))
+(flet ($e966 (xor $e905 $e900))
+(flet ($e967 (or $e728 $e880))
+(flet ($e968 (or $e413 $e966))
+(flet ($e969 (xor $e917 $e958))
+(flet ($e970 (not $e967))
+(flet ($e971 (and $e839 $e962))
+(flet ($e972 (if_then_else $e882 $e812 $e858))
+(flet ($e973 (if_then_else $e890 $e951 $e537))
+(flet ($e974 (and $e930 $e434))
+(flet ($e975 (not $e742))
+(flet ($e976 (if_then_else $e415 $e355 $e887))
+(flet ($e977 (implies $e503 $e878))
+(flet ($e978 (if_then_else $e931 $e904 $e745))
+(flet ($e979 (xor $e968 $e585))
+(flet ($e980 (iff $e879 $e952))
+(flet ($e981 (xor $e477 $e867))
+(flet ($e982 (or $e972 $e556))
+(flet ($e983 (and $e407 $e943))
+(flet ($e984 (and $e542 $e948))
+(flet ($e985 (implies $e975 $e803))
+(flet ($e986 (or $e984 $e977))
+(flet ($e987 (and $e888 $e647))
+(flet ($e988 (and $e499 $e749))
+(flet ($e989 (implies $e973 $e938))
+(flet ($e990 (not $e603))
+(flet ($e991 (implies $e982 $e982))
+(flet ($e992 (and $e417 $e793))
+(flet ($e993 (not $e987))
+(flet ($e994 (iff $e974 $e969))
+(flet ($e995 (iff $e954 $e426))
+(flet ($e996 (not $e501))
+(flet ($e997 (iff $e907 $e946))
+(flet ($e998 (implies $e822 $e997))
+(flet ($e999 (xor $e988 $e378))
+(flet ($e1000 (not $e939))
+(flet ($e1001 (not $e543))
+(flet ($e1002 (if_then_else $e816 $e580 $e961))
+(flet ($e1003 (or $e68 $e921))
+(flet ($e1004 (not $e942))
+(flet ($e1005 (iff $e980 $e979))
+(flet ($e1006 (iff $e871 $e805))
+(flet ($e1007 (xor $e903 $e842))
+(flet ($e1008 (implies $e956 $e399))
+(flet ($e1009 (iff $e986 $e883))
+(flet ($e1010 (if_then_else $e885 $e947 $e798))
+(flet ($e1011 (implies $e494 $e906))
+(flet ($e1012 (xor $e936 $e916))
+(flet ($e1013 (not $e66))
+(flet ($e1014 (or $e994 $e1002))
+(flet ($e1015 (or $e957 $e744))
+(flet ($e1016 (xor $e620 $e1009))
+(flet ($e1017 (if_then_else $e521 $e452 $e856))
+(flet ($e1018 (or $e515 $e929))
+(flet ($e1019 (not $e928))
+(flet ($e1020 (iff $e934 $e1018))
+(flet ($e1021 (not $e476))
+(flet ($e1022 (implies $e953 $e1013))
+(flet ($e1023 (iff $e1005 $e923))
+(flet ($e1024 (xor $e897 $e843))
+(flet ($e1025 (if_then_else $e993 $e845 $e1023))
+(flet ($e1026 (and $e932 $e1004))
+(flet ($e1027 (implies $e914 $e573))
+(flet ($e1028 (implies $e1000 $e1025))
+(flet ($e1029 (not $e1017))
+(flet ($e1030 (implies $e963 $e964))
+(flet ($e1031 (xor $e810 $e944))
+(flet ($e1032 (xor $e1011 $e359))
+(flet ($e1033 (iff $e971 $e992))
+(flet ($e1034 (xor $e1014 $e1030))
+(flet ($e1035 (or $e983 $e937))
+(flet ($e1036 (not $e990))
+(flet ($e1037 (iff $e908 $e676))
+(flet ($e1038 (if_then_else $e815 $e1020 $e1006))
+(flet ($e1039 (and $e995 $e512))
+(flet ($e1040 (iff $e1024 $e1007))
+(flet ($e1041 (iff $e1031 $e726))
+(flet ($e1042 (implies $e1027 $e828))
+(flet ($e1043 (and $e1041 $e1019))
+(flet ($e1044 (xor $e1012 $e1028))
+(flet ($e1045 (not $e602))
+(flet ($e1046 (and $e1040 $e1022))
+(flet ($e1047 (xor $e1035 $e1021))
+(flet ($e1048 (implies $e552 $e1045))
+(flet ($e1049 (iff $e1029 $e924))
+(flet ($e1050 (implies $e991 $e1038))
+(flet ($e1051 (implies $e981 $e976))
+(flet ($e1052 (if_then_else $e1033 $e488 $e1026))
+(flet ($e1053 (not $e1039))
+(flet ($e1054 (implies $e1049 $e1016))
+(flet ($e1055 (iff $e1053 $e1043))
+(flet ($e1056 (if_then_else $e1044 $e1032 $e959))
+(flet ($e1057 (or $e965 $e922))
+(flet ($e1058 (or $e829 $e1050))
+(flet ($e1059 (iff $e1042 $e876))
+(flet ($e1060 (or $e1037 $e998))
+(flet ($e1061 (not $e1010))
+(flet ($e1062 (and $e1052 $e1015))
+(flet ($e1063 (iff $e1048 $e746))
+(flet ($e1064 (implies $e999 $e999))
+(flet ($e1065 (and $e898 $e1008))
+(flet ($e1066 (not $e1036))
+(flet ($e1067 (implies $e940 $e1058))
+(flet ($e1068 (xor $e1003 $e978))
+(flet ($e1069 (iff $e1051 $e1060))
+(flet ($e1070 (if_then_else $e1047 $e1056 $e1057))
+(flet ($e1071 (or $e401 $e1061))
+(flet ($e1072 (iff $e1001 $e1055))
+(flet ($e1073 (iff $e989 $e985))
+(flet ($e1074 (not $e1071))
+(flet ($e1075 (if_then_else $e1073 $e996 $e1063))
+(flet ($e1076 (implies $e1072 $e1064))
+(flet ($e1077 (iff $e1034 $e1062))
+(flet ($e1078 (xor $e1068 $e1069))
+(flet ($e1079 (implies $e1077 $e1067))
+(flet ($e1080 (xor $e955 $e1046))
+(flet ($e1081 (and $e1076 $e970))
+(flet ($e1082 (or $e1065 $e1080))
+(flet ($e1083 (iff $e1059 $e1079))
+(flet ($e1084 (xor $e1054 $e623))
+(flet ($e1085 (implies $e467 $e1078))
+(flet ($e1086 (not $e1083))
+(flet ($e1087 (implies $e1081 $e1085))
+(flet ($e1088 (and $e1066 $e1070))
+(flet ($e1089 (xor $e1082 $e1088))
+(flet ($e1090 (if_then_else $e1089 $e1084 $e1087))
+(flet ($e1091 (not $e1075))
+(flet ($e1092 (or $e1090 $e1086))
+(flet ($e1093 (if_then_else $e1091 $e1091 $e1074))
+(flet ($e1094 (iff $e1092 $e1092))
+(flet ($e1095 (or $e1094 $e1093))
+$e1095
+)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+
diff --git a/test/unit/no_cxxtest b/test/unit/no_cxxtest
index 57e5064d9..fec2dfb82 100755
--- a/test/unit/no_cxxtest
+++ b/test/unit/no_cxxtest
@@ -3,7 +3,7 @@
 echo
 echo '***************************************************************************'
 echo '*                                                                         *'
-echo '*   WARNING:  CxxTest not found at configure time; tests cannot be run.   *'
+echo '*  WARNING:  CxxTest not found at configure time; unit tests cannot run.  *'
 echo '*                                                                         *'
 echo '***************************************************************************'
 echo