Merge branch 'master' into bv-core

24 files changed, 1182 insertions, 151 deletions

diff --git a/NEWS b/NEWS
index ba396ad0c..3c38aab56 100644
--- a/NEWS
+++ b/NEWS
@@ -10,6 +10,7 @@ Changes since 1.0
 * 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 support in interactive mode
 * 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
diff --git a/src/Makefile.am b/src/Makefile.am
index 3d90f302e..b505750d4 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -137,7 +137,7 @@ gitinfo: gitinfo.tmp
 # .PHONY ensures the .tmp version is always rebuilt (to check for any changes)
 .PHONY: gitinfo.tmp
 gitinfo.tmp:
-	$(AM_V_GEN)(cd "$(top_srcdir)" && sed 's,^ref: refs/heads/,,' .git/HEAD && git show-ref refs/heads/`sed 's,^ref: refs/heads/,,' .git/HEAD` && echo "Modifications: `test -z \"\`git status -s -uno\`\" && echo false || echo true`") >"$@" 2>/dev/null || true
+	$(AM_V_GEN)(cd "$(top_srcdir)"; if ! grep -q '^ref: refs/heads/' .git/HEAD; then echo; fi; sed 's,^ref: refs/heads/,,' .git/HEAD; git show-ref refs/heads/`sed 's,^ref: refs/heads/,,' .git/HEAD`; echo "Modifications: `test -z \"\`git status -s -uno\`\" && echo false || echo true`") >"$@" 2>/dev/null || true
 
 install-data-local:
 	(echo include/cvc4.h; \
diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp
index 08a3e49d0..98294f92b 100644
--- a/src/decision/decision_engine.cpp
+++ b/src/decision/decision_engine.cpp
@@ -29,7 +29,7 @@ using namespace std;
 namespace CVC4 {
 
 DecisionEngine::DecisionEngine(context::Context *sc,
-                                 context::Context *uc) :
+                               context::UserContext *uc) :
   d_enabledStrategies(),
   d_needIteSkolemMap(),
   d_relevancyStrategy(NULL),
diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h
index ea16cec16..859443d00 100644
--- a/src/decision/decision_engine.h
+++ b/src/decision/decision_engine.h
@@ -50,7 +50,7 @@ class DecisionEngine {
   DPLLSatSolverInterface* d_satSolver;
 
   context::Context* d_satContext;
-  context::Context* d_userContext;
+  context::UserContext* d_userContext;
 
   // Does decision engine know the answer?
   context::CDO<SatValue> d_result;
@@ -64,7 +64,7 @@ public:
   // Necessary functions
 
   /** Constructor */
-  DecisionEngine(context::Context *sc, context::Context *uc);
+  DecisionEngine(context::Context *sc, context::UserContext *uc);
 
   /** Destructor, currently does nothing */
   ~DecisionEngine() {
diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp
index 0b63dfbe1..b77d3ba6b 100644
--- a/src/decision/justification_heuristic.cpp
+++ b/src/decision/justification_heuristic.cpp
@@ -28,7 +28,7 @@
 using namespace CVC4;
 
 JustificationHeuristic::JustificationHeuristic(CVC4::DecisionEngine* de,
-                                               context::Context *uc,
+                                               context::UserContext *uc,
                                                context::Context *c):
   ITEDecisionStrategy(de, c),
   d_justified(c),
@@ -38,7 +38,7 @@ JustificationHeuristic::JustificationHeuristic(CVC4::DecisionEngine* de,
   d_timestat("decision::jh::time"),
   d_assertions(uc),
   d_iteAssertions(uc),
-  d_iteCache(),
+  d_iteCache(uc),
   d_visited(),
   d_visitedComputeITE(),
   d_curDecision() {
@@ -199,19 +199,20 @@ SatValue JustificationHeuristic::tryGetSatValue(Node n)
   }//end of else
 }
 
-const JustificationHeuristic::IteList&
+JustificationHeuristic::IteList
 JustificationHeuristic::getITEs(TNode n)
 {
   IteCache::iterator it = d_iteCache.find(n);
   if(it != d_iteCache.end()) {
-    return it->second;
+    return (*it).second;
   } else {
     // Compute the list of ITEs
     // TODO: optimize by avoiding multiple lookup for d_iteCache[n]
-    d_iteCache[n] = IteList();
     d_visitedComputeITE.clear();
-    computeITEs(n, d_iteCache[n]);
-    return d_iteCache[n];
+    IteList ilist;
+    computeITEs(n, ilist);
+    d_iteCache.insert(n, ilist);
+    return ilist;
   }
 }
 
@@ -462,15 +463,15 @@ bool JustificationHeuristic::handleITE(TNode node, SatValue desiredVal)
 
 bool JustificationHeuristic::handleEmbeddedITEs(TNode node)
 {
-  const IteList& l = getITEs(node);
+  const IteList l = getITEs(node);
   Trace("decision::jh::ite") << " ite size = " << l.size() << std::endl;
 
   for(IteList::const_iterator i = l.begin(); i != l.end(); ++i) {
-    if(d_visited.find(i->first) == d_visited.end()) {
-      d_visited.insert(i->first);
-      if(findSplitterRec(i->second, SAT_VALUE_TRUE))
+    if(d_visited.find((*i).first) == d_visited.end()) {
+      d_visited.insert((*i).first);
+      if(findSplitterRec((*i).second, SAT_VALUE_TRUE))
         return true;
-      d_visited.erase(i->first);
+      d_visited.erase((*i).first);
     }
   }
   return false;
diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h
index 91c21d981..d8f9a15a8 100644
--- a/src/decision/justification_heuristic.h
+++ b/src/decision/justification_heuristic.h
@@ -38,7 +38,7 @@ namespace decision {
 
 class JustificationHeuristic : public ITEDecisionStrategy {
   typedef std::vector<pair<TNode,TNode> > IteList;
-  typedef hash_map<TNode,IteList,TNodeHashFunction> IteCache;
+  typedef context::CDHashMap<TNode,IteList,TNodeHashFunction> IteCache;
   typedef context::CDHashMap<TNode,TNode,TNodeHashFunction> SkolemMap;
 
   // being 'justified' is monotonic with respect to decisions
@@ -82,7 +82,7 @@ class JustificationHeuristic : public ITEDecisionStrategy {
   SatLiteral d_curDecision;
 public:
   JustificationHeuristic(CVC4::DecisionEngine* de,
-                         context::Context *uc,
+                         context::UserContext *uc,
                          context::Context *c);
 
   ~JustificationHeuristic();
@@ -110,7 +110,7 @@ private:
   SatValue tryGetSatValue(Node n);
 
   /* Get list of all term-ITEs for the atomic formula v */
-  const JustificationHeuristic::IteList& getITEs(TNode n);
+  JustificationHeuristic::IteList getITEs(TNode n);
 
   /* Compute all term-ITEs in a node recursively */
   void computeITEs(TNode n, IteList &l);
diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index c1d2c2bb1..cba896e4e 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -162,9 +162,15 @@ InteractiveShell::~InteractiveShell() {
 }
 
 Command* InteractiveShell::readCommand() {
+  char* lineBuf = NULL;
+  string line = "";
+
+restart:
+
   /* Don't do anything if the input is closed or if we've seen a
    * QuitCommand. */
-  if( d_in.eof() || d_quit ) {
+  if(d_in.eof() || d_quit) {
+    d_out << endl;
     return NULL;
   }
 
@@ -173,30 +179,32 @@ Command* InteractiveShell::readCommand() {
     throw ParserException("Interactive input broken.");
   }
 
-  char* lineBuf = NULL;
-  string input;
-  stringbuf sb;
-  string line;
-
   /* Prompt the user for input. */
   if(d_usingReadline) {
 #if HAVE_LIBREADLINE
-    lineBuf = ::readline(d_options[options::verbosity] >= 0 ? "CVC4> " : "");
+    lineBuf = ::readline(d_options[options::verbosity] >= 0 ? (line == "" ? "CVC4> " : "... > ") : "");
     if(lineBuf != NULL && lineBuf[0] != '\0') {
       ::add_history(lineBuf);
     }
-    line = lineBuf == NULL ? "" : lineBuf;
+    line += lineBuf == NULL ? "" : lineBuf;
     free(lineBuf);
 #endif /* HAVE_LIBREADLINE */
   } else {
     if(d_options[options::verbosity] >= 0) {
-      d_out << "CVC4> " << flush;
+      if(line == "") {
+        d_out << "CVC4> " << flush;
+      } else {
+        d_out << "... > " << flush;
+      }
     }
 
     /* Read a line */
-    d_in.get(sb,'\n');
-    line = sb.str();
+    stringbuf sb;
+    d_in.get(sb);
+    line += sb.str();
   }
+
+  string input = "";
   while(true) {
     Debug("interactive") << "Input now '" << input << line << "'" << endl << flush;
 
@@ -221,20 +229,24 @@ Command* InteractiveShell::readCommand() {
         (d_usingReadline && lineBuf == NULL) ) {
       input += line;
 
-      if( input.empty() ) {
+      if(input.empty()) {
         /* Nothing left to parse. */
+        d_out << endl;
         return NULL;
       }
 
       /* Some input left to parse, but nothing left to read.
          Jump out of input loop. */
-      break;
+      d_out << endl;
+      input = line = "";
+      d_in.clear();
+      goto restart;
     }
 
     if(!d_usingReadline) {
       /* Extract the newline delimiter from the stream too */
       int c CVC4_UNUSED = d_in.get();
-      assert( c == '\n' );
+      assert(c == '\n');
       Debug("interactive") << "Next char is '" << (char)c << "'" << endl << flush;
     }
 
@@ -259,7 +271,8 @@ Command* InteractiveShell::readCommand() {
         }
 
         /* Read a line */
-        d_in.get(sb,'\n');
+        stringbuf sb;
+        d_in.get(sb);
         line = sb.str();
       }
     } else {
@@ -296,6 +309,9 @@ Command* InteractiveShell::readCommand() {
 #endif /* HAVE_LIBREADLINE */
       }
     }
+  } catch(ParserEndOfFileException& pe) {
+    line += "\n";
+    goto restart;
   } catch(ParserException& pe) {
     d_out << pe << endl;
     // We can't really clear out the sequence and abort the current line,
diff --git a/src/main/options_handlers.h b/src/main/options_handlers.h
index f14a67d5f..4bb4841fe 100644
--- a/src/main/options_handlers.h
+++ b/src/main/options_handlers.h
@@ -27,8 +27,12 @@ inline void showConfiguration(std::string option, SmtEngine* smt) {
   printf("\n");
   printf("version    : %s\n", Configuration::getVersionString().c_str());
   if(Configuration::isGitBuild()) {
+    const char* branchName = Configuration::getGitBranchName();
+    if(*branchName == '\0') {
+      branchName = "-";
+    }
     printf("scm        : git [%s %s%s]\n",
-           Configuration::getGitBranchName(),
+           branchName,
            std::string(Configuration::getGitCommit()).substr(0, 8).c_str(),
            Configuration::hasGitModifications() ?
              " (with modifications)" : "");
diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp
index fbf2b8650..2279865ae 100644
--- a/src/parser/antlr_input.cpp
+++ b/src/parser/antlr_input.cpp
@@ -283,16 +283,22 @@ void AntlrInput::warning(const std::string& message) {
   Warning() << getInputStream()->getName() << ':' << d_lexer->getLine(d_lexer) << '.' << d_lexer->getCharPositionInLine(d_lexer) << ": " << message << endl;
 }
 
-void AntlrInput::parseError(const std::string& message)
+void AntlrInput::parseError(const std::string& message, bool eofException)
   throw (ParserException) {
   Debug("parser") << "Throwing exception: "
       << getInputStream()->getName() << ":"
       << d_lexer->getLine(d_lexer) << "."
       << d_lexer->getCharPositionInLine(d_lexer) << ": "
       << message << endl;
-  throw ParserException(message, getInputStream()->getName(),
-                        d_lexer->getLine(d_lexer),
-                        d_lexer->getCharPositionInLine(d_lexer));
+  if(eofException) {
+    throw ParserEndOfFileException(message, getInputStream()->getName(),
+                                   d_lexer->getLine(d_lexer),
+                                   d_lexer->getCharPositionInLine(d_lexer));
+  } else {
+    throw ParserException(message, getInputStream()->getName(),
+                          d_lexer->getLine(d_lexer),
+                          d_lexer->getCharPositionInLine(d_lexer));
+  }
 }
 
 
diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h
index a2fe99f52..020db0d50 100644
--- a/src/parser/antlr_input.h
+++ b/src/parser/antlr_input.h
@@ -209,7 +209,7 @@ protected:
   /**
    * Throws a <code>ParserException</code> with the given message.
    */
-  void parseError(const std::string& msg)
+  void parseError(const std::string& msg, bool eofException = false)
     throw (ParserException);
 
   /** Set the ANTLR3 lexer for this input. */
diff --git a/src/parser/antlr_input_imports.cpp b/src/parser/antlr_input_imports.cpp
index 9c92846bb..07283f1af 100644
--- a/src/parser/antlr_input_imports.cpp
+++ b/src/parser/antlr_input_imports.cpp
@@ -261,7 +261,7 @@ void AntlrInput::reportError(pANTLR3_BASE_RECOGNIZER recognizer) {
   }
 
   // Call the error display routine
-  input->parseError(ss.str());
+  input->parseError(ss.str(), ((pANTLR3_COMMON_TOKEN)ex->token)->type == ANTLR3_TOKEN_EOF);
 }
 
 ///
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index b8ec160e8..e5e26c9a2 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -625,8 +625,7 @@ mainCommand[CVC4::Command*& cmd]
   : ASSERT_TOK formula[f] { cmd = new AssertCommand(f); }
 
   | QUERY_TOK formula[f] { cmd = new QueryCommand(f); }
-  | CHECKSAT_TOK formula[f] { cmd = new CheckSatCommand(f); }
-  | CHECKSAT_TOK { cmd = new CheckSatCommand(); }
+  | CHECKSAT_TOK formula[f]? { cmd = f.isNull() ? new CheckSatCommand() : new CheckSatCommand(f); }
 
     /* options */
   | OPTION_TOK
diff --git a/src/parser/input.h b/src/parser/input.h
index f4b36469b..5fd3611be 100644
--- a/src/parser/input.h
+++ b/src/parser/input.h
@@ -178,7 +178,7 @@ protected:
   /**
    * Throws a <code>ParserException</code> with the given message.
    */
-  virtual void parseError(const std::string& msg)
+  virtual void parseError(const std::string& msg, bool eofException = false)
     throw (ParserException) = 0;
 
   /** Parse an expression from the input by invoking the
diff --git a/src/parser/parser_exception.h b/src/parser/parser_exception.h
index 8abc04c15..6eae3047d 100644
--- a/src/parser/parser_exception.h
+++ b/src/parser/parser_exception.h
@@ -89,6 +89,30 @@ protected:
   unsigned long d_column;
 };/* class ParserException */
 
+class CVC4_PUBLIC ParserEndOfFileException : public ParserException {
+public:
+
+  // Constructors same as ParserException's
+
+  ParserEndOfFileException() throw() :
+    ParserException() {
+  }
+
+  ParserEndOfFileException(const std::string& msg) throw() :
+    ParserException(msg) {
+  }
+
+  ParserEndOfFileException(const char* msg) throw() :
+    ParserException(msg) {
+  }
+
+  ParserEndOfFileException(const std::string& msg, const std::string& filename,
+                           unsigned long line, unsigned long column) throw() :
+    ParserException(msg, filename, line, column) {
+  }
+
+};/* class ParserEndOfFileException */
+
 }/* CVC4::parser namespace */
 }/* CVC4 namespace */
 
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 8541ca6ae..ef4fd5fea 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -74,6 +74,17 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   }
 }
 
+static std::string maybeQuoteSymbol(const std::string& s) {
+  // this is the set of SMT-LIBv2 permitted characters in "simple" (non-quoted) symbols
+  if(s.find_first_not_of("ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789~!@$%^&*_-+=<>.?/") != string::npos) {
+    // need to quote it
+    stringstream ss;
+    ss << '|' << s << '|';
+    return ss.str();
+  }
+  return s;
+}
+
 void Smt2Printer::toStream(std::ostream& out, TNode n,
                            int toDepth, bool types) const throw() {
   // null
@@ -86,7 +97,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   if(n.isVar()) {
     string s;
     if(n.getAttribute(expr::VarNameAttr(), s)) {
-      out << s;
+      out << maybeQuoteSymbol(s);
     } else {
       if(n.getKind() == kind::VARIABLE) {
         out << "var_";
@@ -175,7 +186,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
       break;
 
     case kind::DATATYPE_TYPE:
-      out << n.getConst<Datatype>().getName();
+      out << maybeQuoteSymbol(n.getConst<Datatype>().getName());
       break;
 
     case kind::UNINTERPRETED_CONSTANT: {
@@ -196,7 +207,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   if(n.getKind() == kind::SORT_TYPE) {
     string name;
     if(n.getAttribute(expr::VarNameAttr(), name)) {
-      out << name;
+      out << maybeQuoteSymbol(name);
       return;
     }
   }
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 50cdf33a3..2a73cb444 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -136,6 +136,12 @@ struct SmtEngineStatistics {
   IntStat d_numAssertionsPost;
   /** time spent in checkModel() */
   TimerStat d_checkModelTime;
+  /** time spent in PropEngine::checkSat() */
+  TimerStat d_solveTime;
+  /** time spent in pushing/popping */
+  TimerStat d_pushPopTime;
+  /** time spent in processAssertions() */
+  TimerStat d_processAssertionsTime;
 
   SmtEngineStatistics() :
     d_definitionExpansionTime("smt::SmtEngine::definitionExpansionTime"),
@@ -152,7 +158,10 @@ struct SmtEngineStatistics {
     d_cnfConversionTime("smt::SmtEngine::cnfConversionTime"),
     d_numAssertionsPre("smt::SmtEngine::numAssertionsPreITERemoval", 0),
     d_numAssertionsPost("smt::SmtEngine::numAssertionsPostITERemoval", 0),
-    d_checkModelTime("smt::SmtEngine::checkModelTime") {
+    d_checkModelTime("smt::SmtEngine::checkModelTime"),
+    d_solveTime("smt::SmtEngine::solveTime"),
+    d_pushPopTime("smt::SmtEngine::pushPopTime"),
+    d_processAssertionsTime("smt::SmtEngine::processAssertionsTime") {
 
     StatisticsRegistry::registerStat(&d_definitionExpansionTime);
     StatisticsRegistry::registerStat(&d_rewriteBooleanTermsTime);
@@ -169,6 +178,9 @@ struct SmtEngineStatistics {
     StatisticsRegistry::registerStat(&d_numAssertionsPre);
     StatisticsRegistry::registerStat(&d_numAssertionsPost);
     StatisticsRegistry::registerStat(&d_checkModelTime);
+    StatisticsRegistry::registerStat(&d_solveTime);
+    StatisticsRegistry::registerStat(&d_pushPopTime);
+    StatisticsRegistry::registerStat(&d_processAssertionsTime);
   }
 
   ~SmtEngineStatistics() {
@@ -187,6 +199,9 @@ struct SmtEngineStatistics {
     StatisticsRegistry::unregisterStat(&d_numAssertionsPre);
     StatisticsRegistry::unregisterStat(&d_numAssertionsPost);
     StatisticsRegistry::unregisterStat(&d_checkModelTime);
+    StatisticsRegistry::unregisterStat(&d_solveTime);
+    StatisticsRegistry::unregisterStat(&d_pushPopTime);
+    StatisticsRegistry::unregisterStat(&d_processAssertionsTime);
   }
 };/* struct SmtEngineStatistics */
 
@@ -2480,6 +2495,8 @@ Result SmtEngine::check() {
     resource = d_resourceBudgetPerCall;
   }
 
+  TimerStat::CodeTimer solveTimer(d_stats->d_solveTime);
+
   Chat() << "solving..." << endl;
   Trace("smt") << "SmtEngine::check(): running check" << endl;
   Result result = d_propEngine->checkSat(millis, resource);
@@ -2562,6 +2579,8 @@ bool SmtEnginePrivate::checkForBadSkolems(TNode n, TNode skolem, hash_map<Node,
 }
 
 void SmtEnginePrivate::processAssertions() {
+  TimerStat::CodeTimer paTimer(d_smt.d_stats->d_processAssertionsTime);
+
   Assert(d_smt.d_fullyInited);
   Assert(d_smt.d_pendingPops == 0);
 
@@ -3538,6 +3557,7 @@ void SmtEngine::internalPush() {
   doPendingPops();
   if(options::incrementalSolving()) {
     d_private->processAssertions();
+    TimerStat::CodeTimer pushPopTimer(d_stats->d_pushPopTime);
     d_userContext->push();
     // the d_context push is done inside of the SAT solver
     d_propEngine->push();
@@ -3558,6 +3578,7 @@ void SmtEngine::internalPop(bool immediate) {
 void SmtEngine::doPendingPops() {
   Assert(d_pendingPops == 0 || options::incrementalSolving());
   while(d_pendingPops > 0) {
+    TimerStat::CodeTimer pushPopTimer(d_stats->d_pushPopTime);
     d_propEngine->pop();
     // the d_context pop is done inside of the SAT solver
     d_userContext->pop();
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index f4d79b468..2fcf43054 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -90,7 +90,7 @@ EqualityEngine::EqualityEngine(context::Context* context, std::string name)
 , d_nodesCount(context, 0)
 , d_assertedEqualitiesCount(context, 0)
 , d_equalityTriggersCount(context, 0)
-, d_nodesThatEvaluateSize(context, 0)
+, d_subtermEvaluatesSize(context, 0)
 , d_stats(name)
 , d_inPropagate(false)
 , d_triggerDatabaseSize(context, 0)
@@ -114,7 +114,7 @@ EqualityEngine::EqualityEngine(EqualityEngineNotify& notify, context::Context* c
 , d_nodesCount(context, 0)
 , d_assertedEqualitiesCount(context, 0)
 , d_equalityTriggersCount(context, 0)
-, d_nodesThatEvaluateSize(context, 0)
+, d_subtermEvaluatesSize(context, 0)
 , d_stats(name)
 , d_inPropagate(false)
 , d_triggerDatabaseSize(context, 0)
@@ -141,18 +141,18 @@ void EqualityEngine::enqueue(const MergeCandidate& candidate, bool back) {
   }
 }
 
-EqualityNodeId EqualityEngine::newApplicationNode(TNode original, EqualityNodeId t1, EqualityNodeId t2, bool isEquality) {
+EqualityNodeId EqualityEngine::newApplicationNode(TNode original, EqualityNodeId t1, EqualityNodeId t2, FunctionApplicationType type) {
   Debug("equality") << d_name << "::eq::newApplicationNode(" << original << ", " << t1 << ", " << t2 << ")" << std::endl;
 
   ++ d_stats.functionTermsCount;
 
   // Get another id for this
   EqualityNodeId funId = newNode(original);
-  FunctionApplication funOriginal(isEquality, t1, t2);
+  FunctionApplication funOriginal(type, t1, t2);
   // The function application we're creating
   EqualityNodeId t1ClassId = getEqualityNode(t1).getFind();
   EqualityNodeId t2ClassId = getEqualityNode(t2).getFind();
-  FunctionApplication funNormalized(isEquality, t1ClassId, t2ClassId);
+  FunctionApplication funNormalized(type, t1ClassId, t2ClassId);
 
   // We add the original version
   d_applications[funId] = FunctionApplicationPair(funOriginal, funNormalized);
@@ -203,8 +203,8 @@ EqualityNodeId EqualityEngine::newNode(TNode node) {
   d_nodeIndividualTrigger.push_back(+null_set_id);
   // Mark non-constant by default
   d_isConstant.push_back(false);
-  // Makr non-evaluate by default
-  d_evaluates.push_back(false);
+  // No terms to evaluate by defaul
+  d_subtermsToEvaluate.push_back(0);
   // Mark Boolean nodes
   d_isBoolean.push_back(false);
   // Mark the node as internal by default
@@ -227,12 +227,29 @@ EqualityNodeId EqualityEngine::newNode(TNode node) {
 
 void EqualityEngine::addFunctionKind(Kind fun, bool interpreted) {
   d_congruenceKinds |= fun;
-  if (interpreted) {
+  if (interpreted && fun != kind::EQUAL) {
     Debug("equality::evaluation") << d_name << "::eq::addFunctionKind(): " << fun << " is interpreted " << std::endl;
     d_congruenceKindsInterpreted |= fun;
   }
 }
 
+bool isOperator(TNode node) {
+  if (node.getKind() == kind::BUILTIN) {
+    return true;
+  }
+  return false;
+}
+
+void EqualityEngine::subtermEvaluates(EqualityNodeId id)  {
+  Debug("equality::evaluation") << d_name << "::eq::subtermEvaluates(" << d_nodes[id] << "): " << d_subtermsToEvaluate[id] << std::endl;
+  Assert(!d_isInternal[id]);
+  Assert(d_subtermsToEvaluate[id] > 0);
+  d_subtermsToEvaluate[id] --;
+  d_subtermEvaluates.push_back(id);
+  d_subtermEvaluatesSize = d_subtermEvaluates.size();
+  Debug("equality::evaluation") << d_name << "::eq::subtermEvaluates(" << d_nodes[id] << "): new " << d_subtermsToEvaluate[id] << std::endl;
+}
+
 void EqualityEngine::addTerm(TNode t) {
 
   Debug("equality") << d_name << "::eq::addTerm(" << t << ")" << std::endl;
@@ -254,45 +271,48 @@ void EqualityEngine::addTerm(TNode t) {
     addTerm(t[1]);
     EqualityNodeId t0id = getNodeId(t[0]);
     EqualityNodeId t1id = getNodeId(t[1]);
-    result = newApplicationNode(t, t0id, t1id, true);
+    result = newApplicationNode(t, t0id, t1id, APP_EQUALITY);
     d_isInternal[result] = false;
-
   } else if (t.getNumChildren() > 0 && d_congruenceKinds[t.getKind()]) {
     TNode tOp = t.getOperator();
     // Add the operator
     addTerm(tOp);
     result = getNodeId(tOp);
     d_isInternal[result] = true;
-    d_isConstant[result] = isInterpretedFunctionKind(t.getKind());
-    d_evaluates[result] = isInterpretedFunctionKind(t.getKind());
     // Add all the children and Curryfy
+    bool isInterpreted = isInterpretedFunctionKind(t.getKind());
     for (unsigned i = 0; i < t.getNumChildren(); ++ i) {
       // Add the child
       addTerm(t[i]);
+      EqualityNodeId tiId = getNodeId(t[i]);
       // Add the application
-      result = newApplicationNode(t, result, getNodeId(t[i]), false);
+      result = newApplicationNode(t, result, tiId, isInterpreted ? APP_INTERPRETED : APP_UNINTERPRETED);
     }
     d_isInternal[result] = false;
-    if (t.isConst()) {
-      d_isConstant[result] = true;
-      d_evaluates[result] = true;
+    d_isConstant[result] = t.isConst();
+    // If interpreted, set the number of non-interpreted children
+    if (isInterpreted) {
+      // How many children are not constants yet 
+      d_subtermsToEvaluate[result] = t.getNumChildren();
+      for (unsigned i = 0; i < t.getNumChildren(); ++ i) {
+	if (isConstant(getNodeId(t[i]))) {
+	  subtermEvaluates(result);
+	}
+      }
     }
   } else {
     // Otherwise we just create the new id
     result = newNode(t);
     // Is this an operator
     d_isInternal[result] = false;
-    if (t.isConst()) {
-      d_isConstant[result] = true;
-      d_evaluates[result] = true;
-    }
+    d_isConstant[result] = t.isConst() && !isOperator(t);
   }
 
   if (t.getType().isBoolean()) {
     // We set this here as this only applies to actual terms, not the
     // intermediate application terms
     d_isBoolean[result] = true;
-  } else if (t.isConst()) {
+  } else if (d_isConstant[result]) {
     // Non-Boolean constants are trigger terms for all tags
     EqualityNodeId tId = getNodeId(t);
     d_newSetTags = 0;
@@ -585,10 +605,16 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
         EqualityNodeId funId = useNode.getApplicationId();
         Debug("equality") << d_name << "::eq::merge(" << class1.getFind() << "," << class2.getFind() << "): " << d_nodes[currentId] << " in " << d_nodes[funId] << std::endl;
         const FunctionApplication& fun = d_applications[useNode.getApplicationId()].normalized;
-        // Check if there is an application with find arguments
+        // If it's interpreted and we can interpret
+	if (fun.isInterpreted() && class1isConstant && !d_isInternal[class2Id]) {
+	  // Get the actual term id 
+	  TNode term = d_nodes[useNode.getApplicationId()];
+	  subtermEvaluates(getNodeId(term));
+	}
+	// Check if there is an application with find arguments
         EqualityNodeId aNormalized = getEqualityNode(fun.a).getFind();
         EqualityNodeId bNormalized = getEqualityNode(fun.b).getFind();
-        FunctionApplication funNormalized(fun.isEquality, aNormalized, bNormalized);
+        FunctionApplication funNormalized(fun.type, aNormalized, bNormalized);
         ApplicationIdsMap::iterator find = d_applicationLookup.find(funNormalized);
         if (find != d_applicationLookup.end()) {
           // Applications fun and the funNormalized can be merged due to congruence
@@ -788,10 +814,11 @@ void EqualityEngine::backtrack() {
     d_applicationLookups.resize(d_applicationLookupsCount);
   }
 
-  if (d_nodesThatEvaluate.size() > d_nodesThatEvaluateSize) {
-    for(int i = d_nodesThatEvaluate.size() - 1, i_end = (int)d_nodesThatEvaluateSize; i >= i_end; --i) {
-      d_evaluates[d_nodesThatEvaluate[i]] = false;
+  if (d_subtermEvaluates.size() > d_subtermEvaluatesSize) {
+    for(int i = d_subtermEvaluates.size() - 1, i_end = (int)d_subtermEvaluatesSize; i >= i_end; --i) {
+      d_subtermsToEvaluate[d_subtermEvaluates[i]] ++;
     }
+    d_subtermEvaluates.resize(d_subtermEvaluatesSize);
   }
 
   if (d_nodes.size() > d_nodesCount) {
@@ -802,7 +829,7 @@ void EqualityEngine::backtrack() {
       d_nodeIds.erase(d_nodes[i]);
 
       const FunctionApplication& app = d_applications[i].original;
-      if (app.isApplication()) {
+      if (!app.isNull()) {
         // Remove b from use-list
         getEqualityNode(app.b).removeTopFromUseList(d_useListNodes);
         // Remove a from use-list
@@ -816,7 +843,7 @@ void EqualityEngine::backtrack() {
     d_nodeTriggers.resize(d_nodesCount);
     d_nodeIndividualTrigger.resize(d_nodesCount);
     d_isConstant.resize(d_nodesCount);
-    d_evaluates.resize(d_nodesCount);
+    d_subtermsToEvaluate.resize(d_nodesCount);
     d_isBoolean.resize(d_nodesCount);
     d_isInternal.resize(d_nodesCount);
     d_equalityGraph.resize(d_nodesCount);
@@ -994,7 +1021,7 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
               Debug("equality") << d_name << "::eq::getExplanation(): due to reflexivity, going deeper" << std::endl;
               EqualityNodeId eqId = currentNode == d_trueId ? edgeNode : currentNode;
               const FunctionApplication& eq = d_applications[eqId].original;
-              Assert(eq.isEquality, "Must be an equality");
+              Assert(eq.isEquality(), "Must be an equality");
               
               // Explain why a = b constant
               Debug("equality") << push;
@@ -1211,20 +1238,6 @@ void EqualityEngine::processEvaluationQueue() {
   Debug("equality::evaluation") << d_name << "::eq::processEvaluationQueue(): done" << std::endl;
 }
 
-void EqualityEngine::evaluateApplication(const FunctionApplication& funNormalized, EqualityNodeId funId) {
-
-  // Evaluate special for equality and other
-  if (!funNormalized.isEquality) {
-    // We can't add new terms 
-    d_evaluationQueue.push(funId);
-  } else {
-    if (funNormalized.a != funNormalized.b) {
-      // We don't enqueue fun -> true, as this is convered with reflexivity
-      enqueue(MergeCandidate(funId, d_falseId, MERGED_THROUGH_CONSTANTS, TNode::null()));
-    }
-  }
-}
-
 void EqualityEngine::propagate() {
 
   if (d_inPropagate) {
@@ -1466,7 +1479,7 @@ bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const
   }
   
   // Create the equality
-  FunctionApplication eqNormalized(true, t1ClassId, t2ClassId);
+  FunctionApplication eqNormalized(APP_EQUALITY, t1ClassId, t2ClassId);
   ApplicationIdsMap::const_iterator find = d_applicationLookup.find(eqNormalized);
   if (find != d_applicationLookup.end()) {
     if (getEqualityNode(find->second).getFind() == getEqualityNode(d_falseId).getFind()) {
@@ -1618,19 +1631,11 @@ void EqualityEngine::storeApplicationLookup(FunctionApplication& funNormalized,
   Assert(d_applicationLookupsCount == d_applicationLookups.size());
 
   // If an equality over constants we merge to false
-  if (funNormalized.isEquality && funNormalized.a == funNormalized.b) {
-    enqueue(MergeCandidate(funId, d_trueId, MERGED_THROUGH_REFLEXIVITY, TNode::null()));
-  }
-
-  // Now check for application evaluation
-  if (!d_evaluates[funId]) {
-    if (d_evaluates[funNormalized.a] && d_evaluates[funNormalized.b]) {
-      // Depending on the "internal"
-      if (d_isInternal[funId]) {
-        setEvaluates(funId);
-      } else {
-        evaluateApplication(funNormalized, funId);
-      }
+  if (funNormalized.isEquality()) {
+    if (funNormalized.a == funNormalized.b) {
+      enqueue(MergeCandidate(funId, d_trueId, MERGED_THROUGH_REFLEXIVITY, TNode::null()));
+    } else if (d_isConstant[funNormalized.a] && d_isConstant[funNormalized.b]) {
+      enqueue(MergeCandidate(funId, d_falseId, MERGED_THROUGH_CONSTANTS, TNode::null()));
     }
   }
 }
@@ -1798,7 +1803,7 @@ void EqualityEngine::getDisequalities(bool allowConstants, EqualityNodeId classI
 
       const FunctionApplication& fun = d_applications[useListNode.getApplicationId()].original;
       // If it's an equality asserted to false, we do the work
-      if (fun.isEquality && getEqualityNode(funId).getFind() == getEqualityNode(d_false).getFind()) {
+      if (fun.isEquality() && getEqualityNode(funId).getFind() == getEqualityNode(d_false).getFind()) {
         // Get the other equality member
         bool lhs = false;
         EqualityNodeId toCompare = fun.b;
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 3d80c486a..0a5d70a9c 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -418,20 +418,11 @@ private:
   std::vector<bool> d_isConstant;
 
   /**
-   * Map from ids to whether they evaluate. A node evaluates 
-   * (1) if it is a constant
-   * (2) if it is internal and it's children evaluate
-   * (3) if it is non-internal and it's children are constants
+   * Map from ids of proper terms, to the number of non-constant direct subterms. If we update an interpreted
+   * application to a constant, we can decrease this value. If we hit 0, we can evaluate the term.
    * 
-   * Example:
-   * 
-   *  f(x) + g(y)
-   * 
-   * If f and g are interpreted, in the context x = 0, the nodes 
-   * f(x) and g(y) evaluate, but not f(x) + g(y). The term f(x) + g(y) 
-   * evaluates if we evaluate f(0) and g(0) to constants c1 and c2.
    */
-  std::vector<bool> d_evaluates;
+  std::vector<unsigned> d_subtermsToEvaluate;
   
   /** 
    * For nodes that we need to postpone evaluation.
@@ -443,32 +434,14 @@ private:
    */
   void processEvaluationQueue();
   
-  /** 
-   * Check whether the node evaluates in the current context 
-   */
-  bool evaluates(EqualityNodeId id) const {
-    return d_evaluates[id];
-  }
-
   /** Vector of nodes that evaluate. */
-  std::vector<EqualityNodeId> d_nodesThatEvaluate;
+  std::vector<EqualityNodeId> d_subtermEvaluates;
 
   /** Size of the nodes that evaluate vector. */
-  context::CDO<unsigned> d_nodesThatEvaluateSize;
+  context::CDO<unsigned> d_subtermEvaluatesSize;
   
   /** Set the node evaluate flag */
-  void setEvaluates(EqualityNodeId id) {
-    Assert(!d_evaluates[id]);
-    d_evaluates[id] = true;
-    d_nodesThatEvaluate.push_back(id);
-    d_nodesThatEvaluateSize = d_nodesThatEvaluate.size();
-  }
-
-  /** 
-   * Propagate something that evaluates.
-   * @param fragile if true, no new terms are added, but 
-   */
-  void evaluateApplication(const FunctionApplication& funNormalized, EqualityNodeId funId);
+  void subtermEvaluates(EqualityNodeId id);
 
   /**
    * Returns the evaluation of the term when all (direct) children are replaced with 
@@ -503,7 +476,7 @@ private:
   Statistics d_stats;
 
   /** Add a new function application node to the database, i.e APP t1 t2 */
-  EqualityNodeId newApplicationNode(TNode original, EqualityNodeId t1, EqualityNodeId t2, bool isEquality);
+  EqualityNodeId newApplicationNode(TNode original, EqualityNodeId t1, EqualityNodeId t2, FunctionApplicationType type);
 
   /** Add a new node to the database */
   EqualityNodeId newNode(TNode t);
diff --git a/src/theory/uf/equality_engine_types.h b/src/theory/uf/equality_engine_types.h
index e05000160..f993b941b 100644
--- a/src/theory/uf/equality_engine_types.h
+++ b/src/theory/uf/equality_engine_types.h
@@ -264,6 +264,15 @@ struct EqualityPairHashFunction {
   }
 };
 
+enum FunctionApplicationType {
+  /** This application is an equality a = b */
+  APP_EQUALITY,
+  /** This is a part of an uninterpreted application f(t1, ...., tn) */
+  APP_UNINTERPRETED,
+  /** This is a part of an interpreted application f(t1, ..., tn) */
+  APP_INTERPRETED
+};
+
 /**
  * Represents the function APPLY a b. If isEquality is true then it
  * represents the predicate (a = b). Note that since one can not 
@@ -271,16 +280,35 @@ struct EqualityPairHashFunction {
  * function below are still well defined.
  */
 struct FunctionApplication {
-  bool isEquality;
+  /** Type of application */
+  FunctionApplicationType type;
+  /** The actuall application elements */
   EqualityNodeId a, b;
-  FunctionApplication(bool isEquality = false, EqualityNodeId a = null_id, EqualityNodeId b = null_id)
-  : isEquality(isEquality), a(a), b(b) {}
+
+  /** Construct an application */
+  FunctionApplication(FunctionApplicationType type = APP_EQUALITY, EqualityNodeId a = null_id, EqualityNodeId b = null_id)
+  : type(type), a(a), b(b) {}
+
+  /** Equality of two applications */
   bool operator == (const FunctionApplication& other) const {
-    return isEquality == other.isEquality && a == other.a && b == other.b;
+    return type == other.type && a == other.a && b == other.b;
   }
-  bool isApplication() const {
-    return a != null_id && b != null_id;
+
+  /** Is this a null application */
+  bool isNull() const {
+    return a == null_id || b == null_id;
   }
+
+  /** Is this an equality */
+  bool isEquality() const {
+    return type == APP_EQUALITY;
+  }
+
+  /** Is this an interpreted application (equality is special, i.e. not interpreted) */
+  bool isInterpreted() const {
+    return type == APP_INTERPRETED;
+  }
+
 };
 
 struct FunctionApplicationHashFunction {
@@ -303,7 +331,7 @@ struct FunctionApplicationPair {
   FunctionApplicationPair(const FunctionApplication& original, const FunctionApplication& normalized)
   : original(original), normalized(normalized) {}
   bool isNull() const {
-    return !original.isApplication();
+    return original.isNull();
   }
 };
 
diff --git a/src/util/configuration.cpp b/src/util/configuration.cpp
index 9be4e4104..ce6273a13 100644
--- a/src/util/configuration.cpp
+++ b/src/util/configuration.cpp
@@ -216,8 +216,13 @@ std::string Configuration::getGitId() {
     return "";
   }
 
+  const char* branchName = getGitBranchName();
+  if(*branchName == '\0') {
+    branchName = "-";
+  }
+
   stringstream ss;
-  ss << "git " << getGitBranchName() << " " << string(getGitCommit()).substr(0, 8)
+  ss << "git " << branchName << " " << string(getGitCommit()).substr(0, 8)
      << ( ::CVC4::Configuration::hasGitModifications() ? " (with modifications)" : "" );
   return ss.str();
 }
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index cc385327e..96d07d7f3 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -113,6 +113,7 @@ TPTP_TESTS = \
 
 # Regression tests derived from bug reports
 BUG_TESTS = \
+	smt2output.smt2 \
 	bug32.cvc \
 	bug49.smt \
 	bug161.smt \
@@ -144,7 +145,8 @@ BUG_TESTS = \
 	bug421b.smt2 \
 	bug425.cvc \
 	bug480.smt2 \
-	bug486.cvc
+	bug486.cvc \
+	bug497.cvc
 
 TESTS =	$(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS)
 
diff --git a/test/regress/regress0/bug497.cvc b/test/regress/regress0/bug497.cvc
new file mode 100644
index 000000000..ce34ab6ad
--- /dev/null
+++ b/test/regress/regress0/bug497.cvc
@@ -0,0 +1,920 @@
+% COMMAND-LINE: --decision=justification --incremental
+% EXPECT: sat
+% EXPECT: sat
+% EXIT: 10
+OPTION "logic" "QF_UFLIA";
+_nat : TYPE = INT;
+_base : INT;
+ASSERT _base <= 0;
+_n : _nat;
+ASSERT _n >= _base;
+_check_quant : BOOLEAN;
+
+% maxdepth = 1
+x100 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state126_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_OrbitalState_Complex_OrbitalState %  LOCAL/200
+x101 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state122_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_OrbitalState_Complex_OrbitalState %  LOCAL/201
+x2 : _nat -> INT;
+			% GroundTrack_OrbitalPosition %  INPUT,STATE(1,)/102
+x102 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state221_rlt_chart_data_vars_Chart_OrbitalState_Attitude %  LOCAL,STATE(1,)/202
+x3 : _nat -> INT;
+			% GroundTrack_OrbitalVelocity %  INPUT,STATE(1,)/103
+x103 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state221_rlt_chart_data_vars_Chart_InertialNavigation_AbsoluteVelocity %  LOCAL/203
+x4 : _nat -> INT;
+			% dockVisibility_status %  INPUT,STATE(1,)/104
+x104 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state221_rlt_chart_data_vars_Chart_InertialNavigation_AbsolutePosition %  LOCAL/204
+x5 : _nat -> BOOLEAN;
+			% opticsAvailability_status %  INPUT,STATE(1,)/105
+x105 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state221_rlt_chart_data_vars_Chart_InertialNavigation_timer %  LOCAL/205
+x6 : _nat -> BOOLEAN;
+			% sunlight_status %  INPUT,STATE(1,)/106
+x106 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state221_rlt_chart_data_vars_Chart_OrbitalState_Velocity %  LOCAL,STATE(1,)/206
+x7 : _nat -> INT;
+			% GPS_satelliteVisibility_status %  INPUT,STATE(1,)/107
+x107 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state221_rlt_chart_data_vars_Chart_OrbitalState_Position %  LOCAL,STATE(1,)/207
+x8 : _nat -> BOOLEAN;
+			% GPS_receiverAvailability_status %  INPUT,STATE(1,)/108
+x108 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state221_rlt_chart_data_vars_Chart_InertialNavigation_AbsoluteAttitude %  LOCAL/208
+x9 : _nat -> INT;
+			% StarPlanetTracker_planetVisibility %  INPUT,STATE(1,)/109
+x109 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state221_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_OrbitalState_Complex_OrbitalState %  LOCAL,STATE(1,)/209
+x10 : _nat -> INT;
+			% StarPlanetTracker_starVisibility %  INPUT,STATE(1,)/110
+x110 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state221_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_InertialNavigation %  LOCAL/210
+x11 : _nat -> BOOLEAN;
+			% InertialNavigation_time %  INPUT/111
+x111 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state367_rlt_chart_data_vars_Chart_OrbitalState_Time %  LOCAL,STATE(1,)/211
+x12 : _nat -> INT;
+			% GroundTrack_Time %  INPUT/112
+x112 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state367_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_OrbitalState_Complex_OrbitalState2 %  LOCAL,STATE(1,)/212
+x13 : _nat -> INT;
+			% RealTimeClock_time %  INPUT,STATE(1,)/113
+x113 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state499_rlt_chart_data_vars_Chart_InertialNavigation_AbsoluteVelocity %  LOCAL,STATE(1,)/213
+x14 : _nat -> INT;
+			% StageTransition %  INPUT,STATE(1,)/114
+x114 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state499_rlt_chart_data_vars_Chart_InertialNavigation_AbsolutePosition %  LOCAL,STATE(1,)/214
+x15 : _nat -> BOOLEAN;
+			% CaptureApproachComplete %  OUTPUT,STATE(1,)/115
+x115 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state499_rlt_chart_data_vars_Chart_InertialNavigation_AbsoluteAttitude %  LOCAL,STATE(1,)/215
+x16 : _nat -> BOOLEAN;
+			% DockingApproachComplete %  OUTPUT,STATE(1,)/116
+x116 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state499_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_InertialNavigation %  LOCAL,STATE(1,)/216
+x17 : _nat -> BOOLEAN;
+			% AttemptingToDock %  OUTPUT,STATE(1,)/117
+x117 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state627_rlt_chart_data_states_Chart_MissionPhaseStates_DockingApproach_dockingSensor %  LOCAL,STATE(1,)/217
+x118 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state545_rlt_chart_data_vars_Chart_dockingSensor_timer %  LOCAL/218
+x119 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state545_rlt_chart_data_states_Chart_MissionPhaseStates_DockingApproach_dockingSensor %  LOCAL/219
+x20 : _nat -> BOOLEAN;
+			% ApproachOrbitComplete %  OUTPUT,STATE(1,)/120
+x120 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state542_rlt_chart_data_states_Chart_MissionPhaseStates_DockingApproach_dockingSensor %  LOCAL/220
+x21 : _nat -> BOOLEAN;
+			% FarApproachComplete %  OUTPUT,STATE(1,)/121
+x121 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state540_rlt_chart_data_states_Chart_MissionPhaseStates_DockingApproach_dockingSensor %  LOCAL/221
+x22 : _nat -> BOOLEAN;
+			% ProximityOperationsComplete %  OUTPUT,STATE(1,)/122
+x122 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state765_rlt_chart_data_states_Chart_MissionPhaseStates_LatchCapture_latch %  LOCAL,STATE(1,)/222
+x123 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state690_rlt_chart_data_states_Chart_MissionPhaseStates_LatchCapture_LatchCaptureCheck %  LOCAL,STATE(1,)/223
+x124 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state706_rlt_chart_data_states_Chart_MissionPhaseStates_LatchCapture_latch %  LOCAL/224
+x125 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state702_rlt_chart_data_states_Chart_MissionPhaseStates_LatchCapture_latch %  LOCAL/225
+x26 : _nat -> INT;
+			% MWI_FcnMin_Out110 %  LOCAL,STATE(1,)/126
+x126 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state759_rlt_chart_data_states_Chart_MissionPhaseStates_LatchCapture_latch %  LOCAL/226
+x27 : _nat -> INT;
+			% MWI_FcnMin_Out19 %  LOCAL,STATE(1,)/127
+x127 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state757_rlt_chart_data_states_Chart_MissionPhaseStates_LatchCapture_latch %  LOCAL/227
+x28 : _nat -> INT;
+			% MWI_FcnMin_In1n8 %  LOCAL/128
+x128 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state753_rlt_chart_data_states_Chart_MissionPhaseStates_LatchCapture_latch %  LOCAL/228
+x29 : _nat -> INT;
+			% MWI_FcnMin_Out18 %  LOCAL,STATE(1,)/129
+x129 : _nat -> BOOLEAN;
+			% sequence1 %  LOCAL/229
+x30 : _nat -> INT;
+			% MWI_FcnMin_Out17 %  LOCAL/130
+x31 : _nat -> INT;
+			% MWI_FcnMin_Out13 %  LOCAL,STATE(1,)/131
+x32 : _nat -> INT;
+			% MWI_FcnMin_Out12 %  LOCAL,STATE(1,)/132
+x33 : _nat -> INT;
+			% MWI_FcnMin_Out11 %  LOCAL,STATE(1,)/133
+x34 : _nat -> INT;
+			% MWI_FcnMin_In1n %  LOCAL/134
+x35 : _nat -> INT;
+			% MWI_FcnMin_Out1 %  LOCAL,STATE(1,)/135
+x36 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state1_rlt_chart_data_vars_Chart_OrbitalState_Time %  LOCAL,STATE(1,)/136
+x37 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state1_rlt_chart_data_vars_Chart_LatchCapture_timer %  LOCAL,STATE(1,)/137
+x38 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state1_rlt_chart_data_vars_Chart_StarPlanetTracker_timer %  LOCAL,STATE(1,)/138
+x39 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state1_rlt_chart_data_vars_Chart_OrbitalState_Attitude %  LOCAL,STATE(1,)/139
+x40 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state1_rlt_chart_data_vars_Chart_CaptureApproach_timer %  LOCAL,STATE(1,)/140
+x41 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state1_rlt_chart_data_vars_Chart_GPS_timer %  LOCAL,STATE(1,)/141
+x42 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state1_rlt_chart_data_vars_Chart_InertialNavigation_AbsoluteVelocity %  LOCAL,STATE(1,)/142
+x43 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state1_rlt_chart_data_vars_Chart_InertialNavigation_AbsolutePosition %  LOCAL,STATE(1,)/143
+x44 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state1_rlt_chart_data_vars_Chart_InertialNavigation_timer %  LOCAL,STATE(1,)/144
+x45 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state1_rlt_chart_data_vars_Chart_latch_status %  LOCAL,STATE(1,)/145
+x46 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state1_rlt_chart_data_vars_Chart_dockingSensor_timer %  LOCAL,STATE(1,)/146
+x47 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state1_rlt_chart_data_vars_Chart_OrbitalState_Velocity %  LOCAL,STATE(1,)/147
+x48 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state1_rlt_chart_data_vars_Chart_OrbitalState_Position %  LOCAL,STATE(1,)/148
+x49 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state1_rlt_chart_data_vars_Chart_dockingSensor_RelativeAttitude %  LOCAL,STATE(1,)/149
+x50 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state1_rlt_chart_data_vars_Chart_GPS_AbsolutePosition %  LOCAL,STATE(1,)/150
+x51 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state1_rlt_chart_data_vars_Chart_DockingApproach_timer %  LOCAL,STATE(1,)/151
+x52 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state1_rlt_chart_data_vars_Chart_InertialNavigation_AbsoluteAttitude %  LOCAL,STATE(1,)/152
+x53 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state1_rlt_chart_data_vars_Chart_StarPlanetTracker_AbsolutePosition %  LOCAL,STATE(1,)/153
+x54 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state1_rlt_chart_data_states_Chart_MissionPhaseStates_DockingApproach_dockingSensor %  LOCAL,STATE(1,)/154
+x55 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state1_rlt_chart_data_states_Chart_MissionPhaseStates_DockingApproach_DockingApproach %  LOCAL,STATE(1,)/155
+x56 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state1_rlt_chart_data_states_Chart_MissionPhaseStates_LatchCapture_latch %  LOCAL,STATE(1,)/156
+x57 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state1_rlt_chart_data_states_Chart_MissionPhaseStates_LatchCapture_LatchCaptureCheck %  LOCAL,STATE(1,)/157
+x58 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state1_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_GPS %  LOCAL,STATE(1,)/158
+x59 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state1_rlt_chart_data_states_Chart %  LOCAL,STATE(1,)/159
+x60 : _nat -> [0..2];
+			% Chart_main_simp_rlt_node_state1_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_OrbitalState_Complex_OrbitalState2 %  LOCAL,STATE(1,)/160
+x61 : _nat -> [0..4];
+			% Chart_main_simp_rlt_node_state1_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_OrbitalState_Complex_OrbitalState %  LOCAL,STATE(1,)/161
+x62 : _nat -> [0..3];
+			% Chart_main_simp_rlt_node_state1_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_StarPlanetTracker %  LOCAL,STATE(1,)/162
+x63 : _nat -> [0..5];
+			% Chart_main_simp_rlt_node_state1_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_CaptureApproach %  LOCAL,STATE(1,)/163
+x64 : _nat -> [0..3];
+			% Chart_main_simp_rlt_node_state1_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_InertialNavigation %  LOCAL,STATE(1,)/164
+x65 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state1_rlt_chart_data_states_Chart_MissionPhaseStates %  LOCAL,STATE(1,)/165
+x66 : _nat -> BOOLEAN;
+			% Chart_main_simp_rlt_node_state1_rlt_chart_data_outports_FarApproachComplete %  LOCAL/166
+x68 : _nat -> BOOLEAN;
+			% Chart_main_simp_rlt_node_state1_rlt_chart_data_outports_AttemptingToDock %  LOCAL/168
+x71 : _nat -> BOOLEAN;
+			% Chart_main_simp_rlt_node_state1_rlt_chart_data_outports_ProximityOperationsComplete %  LOCAL/171
+x73 : _nat -> BOOLEAN;
+			% Chart_main_simp_rlt_node_state1_rlt_chart_data_outports_DockingApproachComplete %  LOCAL/173
+x74 : _nat -> BOOLEAN;
+			% Chart_main_simp_rlt_node_state1_rlt_chart_data_outports_ApproachOrbitComplete %  LOCAL/174
+x76 : _nat -> BOOLEAN;
+			% Chart_main_simp_rlt_node_state1_rlt_chart_data_outports_CaptureApproachComplete %  LOCAL/176
+x77 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state364_rlt_chart_data_vars_Chart_InertialNavigation_AbsoluteVelocity %  LOCAL,STATE(1,)/177
+x78 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state364_rlt_chart_data_vars_Chart_InertialNavigation_AbsolutePosition %  LOCAL,STATE(1,)/178
+x79 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state364_rlt_chart_data_vars_Chart_InertialNavigation_AbsoluteAttitude %  LOCAL,STATE(1,)/179
+x80 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state364_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_InertialNavigation %  LOCAL,STATE(1,)/180
+x81 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state155_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_GPS %  LOCAL,STATE(1,)/181
+x82 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state155_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_OrbitalState_Complex_OrbitalState2 %  LOCAL,STATE(1,)/182
+x83 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state155_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_OrbitalState_Complex_OrbitalState %  LOCAL,STATE(1,)/183
+x84 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state155_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_StarPlanetTracker %  LOCAL,STATE(1,)/184
+x85 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state155_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_InertialNavigation %  LOCAL/185
+x86 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state155_rlt_chart_data_states_Chart_MissionPhaseStates %  LOCAL,STATE(1,)/186
+x87 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state104_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_InertialNavigation %  LOCAL/187
+x88 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state100_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_StarPlanetTracker %  LOCAL/188
+x89 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state98_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_StarPlanetTracker %  LOCAL/189
+x90 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state96_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_StarPlanetTracker %  LOCAL/190
+x91 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state82_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_OrbitalState_Complex_OrbitalState %  LOCAL/191
+x92 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state78_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_OrbitalState_Complex_OrbitalState %  LOCAL/192
+x93 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state148_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_InertialNavigation %  LOCAL/193
+x94 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state144_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_InertialNavigation %  LOCAL/194
+x95 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state136_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_GPS %  LOCAL/195
+x96 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state134_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_GPS %  LOCAL/196
+x97 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state132_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_GPS %  LOCAL/197
+x98 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state130_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_OrbitalState_Complex_OrbitalState2 %  LOCAL/198
+x99 : _nat -> INT;
+			% Chart_main_simp_rlt_node_state128_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_OrbitalState_Complex_OrbitalState2 %  LOCAL/199
+
+
+% Generic definitions
+DEF__174 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x74(_M)) = (IF (_M = _base) THEN FALSE ELSE (x20((_M - 1))) ENDIF));
+DEF__176 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x76(_M)) = (IF (_M = _base) THEN FALSE ELSE (x15((_M - 1))) ENDIF));
+DEF__177 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x77(_M)) = (IF ((x83(_M)) = 1) THEN (x42(_M)) ELSE (IF ((x83(_M)) = 2) THEN (x42(_M)) ELSE (IF ((x83(_M)) = 3) THEN (x103(_M)) ELSE (IF ((x83(_M)) = 4) THEN (IF ((NOT ((((((((x2(_M)) = 2) AND ((x50(_M)) = 2)) OR (((x2(_M)) = 2) AND ((x53(_M)) = 2))) OR (((x53(_M)) = 2) AND ((x50(_M)) = 2))) OR (((x43(_M)) = 2) AND ((x2(_M)) = 2))) OR (((x43(_M)) = 2) AND ((x50(_M)) = 2))) OR (((x43(_M)) = 2) AND ((x53(_M)) = 2)))) <=> TRUE) THEN (IF ((NOT (((x52(_M)) = 2) OR ((x53(_M)) = 2))) <=> TRUE) THEN (IF ((NOT ((((((((x3(_M)) = 2) AND ((x50(_M)) = 2)) OR (((x3(_M)) = 2) AND ((x53(_M)) = 2))) OR (((x53(_M)) = 2) AND ((x50(_M)) = 2))) OR (((x42(_M)) = 2) AND ((x3(_M)) = 2))) OR (((x42(_M)) = 2) AND ((x50(_M)) = 2))) OR (((x42(_M)) = 2) AND ((x53(_M)) = 2)))) <=> TRUE) THEN (x42(_M)) ELSE (x103(_M)) ENDIF) ELSE (x103(_M)) ENDIF) ELSE (x103(_M)) ENDIF) ELSE (x42(_M)) ENDIF) ENDIF) ENDIF) ENDIF));
+DEF__178 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x78(_M)) = (IF ((x83(_M)) = 1) THEN (x43(_M)) ELSE (IF ((x83(_M)) = 2) THEN (x43(_M)) ELSE (IF ((x83(_M)) = 3) THEN (x104(_M)) ELSE (IF ((x83(_M)) = 4) THEN (IF ((NOT ((((((((x2(_M)) = 2) AND ((x50(_M)) = 2)) OR (((x2(_M)) = 2) AND ((x53(_M)) = 2))) OR (((x53(_M)) = 2) AND ((x50(_M)) = 2))) OR (((x43(_M)) = 2) AND ((x2(_M)) = 2))) OR (((x43(_M)) = 2) AND ((x50(_M)) = 2))) OR (((x43(_M)) = 2) AND ((x53(_M)) = 2)))) <=> TRUE) THEN (IF ((NOT (((x52(_M)) = 2) OR ((x53(_M)) = 2))) <=> TRUE) THEN (IF ((NOT ((((((((x3(_M)) = 2) AND ((x50(_M)) = 2)) OR (((x3(_M)) = 2) AND ((x53(_M)) = 2))) OR (((x53(_M)) = 2) AND ((x50(_M)) = 2))) OR (((x42(_M)) = 2) AND ((x3(_M)) = 2))) OR (((x42(_M)) = 2) AND ((x50(_M)) = 2))) OR (((x42(_M)) = 2) AND ((x53(_M)) = 2)))) <=> TRUE) THEN (x43(_M)) ELSE (x104(_M)) ENDIF) ELSE (x104(_M)) ENDIF) ELSE (x104(_M)) ENDIF) ELSE (x43(_M)) ENDIF) ENDIF) ENDIF) ENDIF));
+DEF__179 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x79(_M)) = (IF ((x83(_M)) = 1) THEN (x52(_M)) ELSE (IF ((x83(_M)) = 2) THEN (x52(_M)) ELSE (IF ((x83(_M)) = 3) THEN (x108(_M)) ELSE (IF ((x83(_M)) = 4) THEN (IF ((NOT ((((((((x2(_M)) = 2) AND ((x50(_M)) = 2)) OR (((x2(_M)) = 2) AND ((x53(_M)) = 2))) OR (((x53(_M)) = 2) AND ((x50(_M)) = 2))) OR (((x43(_M)) = 2) AND ((x2(_M)) = 2))) OR (((x43(_M)) = 2) AND ((x50(_M)) = 2))) OR (((x43(_M)) = 2) AND ((x53(_M)) = 2)))) <=> TRUE) THEN (IF ((NOT (((x52(_M)) = 2) OR ((x53(_M)) = 2))) <=> TRUE) THEN (IF ((NOT ((((((((x3(_M)) = 2) AND ((x50(_M)) = 2)) OR (((x3(_M)) = 2) AND ((x53(_M)) = 2))) OR (((x53(_M)) = 2) AND ((x50(_M)) = 2))) OR (((x42(_M)) = 2) AND ((x3(_M)) = 2))) OR (((x42(_M)) = 2) AND ((x50(_M)) = 2))) OR (((x42(_M)) = 2) AND ((x53(_M)) = 2)))) <=> TRUE) THEN (x52(_M)) ELSE (x108(_M)) ENDIF) ELSE (x108(_M)) ENDIF) ELSE (x108(_M)) ENDIF) ELSE (x52(_M)) ENDIF) ENDIF) ENDIF) ENDIF));
+DEF__180 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x80(_M)) = (IF ((x83(_M)) = 1) THEN (x85(_M)) ELSE (IF ((x83(_M)) = 2) THEN (x85(_M)) ELSE (IF ((x83(_M)) = 3) THEN (x110(_M)) ELSE (IF ((x83(_M)) = 4) THEN (IF ((NOT ((((((((x2(_M)) = 2) AND ((x50(_M)) = 2)) OR (((x2(_M)) = 2) AND ((x53(_M)) = 2))) OR (((x53(_M)) = 2) AND ((x50(_M)) = 2))) OR (((x43(_M)) = 2) AND ((x2(_M)) = 2))) OR (((x43(_M)) = 2) AND ((x50(_M)) = 2))) OR (((x43(_M)) = 2) AND ((x53(_M)) = 2)))) <=> TRUE) THEN (IF ((NOT (((x52(_M)) = 2) OR ((x53(_M)) = 2))) <=> TRUE) THEN (IF ((NOT ((((((((x3(_M)) = 2) AND ((x50(_M)) = 2)) OR (((x3(_M)) = 2) AND ((x53(_M)) = 2))) OR (((x53(_M)) = 2) AND ((x50(_M)) = 2))) OR (((x42(_M)) = 2) AND ((x3(_M)) = 2))) OR (((x42(_M)) = 2) AND ((x50(_M)) = 2))) OR (((x42(_M)) = 2) AND ((x53(_M)) = 2)))) <=> TRUE) THEN (x85(_M)) ELSE (x110(_M)) ENDIF) ELSE (x110(_M)) ENDIF) ELSE (x110(_M)) ENDIF) ELSE (x85(_M)) ENDIF) ENDIF) ENDIF) ENDIF));
+DEF__181 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x81(_M)) = (IF ((x63(_M)) = 1) THEN (x58(_M)) ELSE (IF ((x63(_M)) = 2) THEN (x58(_M)) ELSE (IF ((x63(_M)) = 3) THEN (x58(_M)) ELSE (IF ((x63(_M)) = 4) THEN (x95(_M)) ELSE (IF ((x63(_M)) = 5) THEN (x95(_M)) ELSE (x58(_M)) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF));
+DEF__182 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x82(_M)) = (IF ((x63(_M)) = 1) THEN (x60(_M)) ELSE (IF ((x63(_M)) = 2) THEN (x60(_M)) ELSE (IF ((x63(_M)) = 3) THEN (x60(_M)) ELSE (IF ((x63(_M)) = 4) THEN (x98(_M)) ELSE (IF ((x63(_M)) = 5) THEN (x98(_M)) ELSE (x60(_M)) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF));
+DEF__183 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x83(_M)) = (IF ((x63(_M)) = 1) THEN (x61(_M)) ELSE (IF ((x63(_M)) = 2) THEN (x61(_M)) ELSE (IF ((x63(_M)) = 3) THEN (x61(_M)) ELSE (IF ((x63(_M)) = 4) THEN (x100(_M)) ELSE (IF ((x63(_M)) = 5) THEN (x100(_M)) ELSE (x61(_M)) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF));
+DEF__184 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x84(_M)) = (IF ((x63(_M)) = 1) THEN (x62(_M)) ELSE (IF ((x63(_M)) = 2) THEN (x62(_M)) ELSE (IF ((x63(_M)) = 3) THEN (x62(_M)) ELSE (IF ((x63(_M)) = 4) THEN (x88(_M)) ELSE (IF ((x63(_M)) = 5) THEN (x88(_M)) ELSE (x62(_M)) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF));
+DEF__185 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x85(_M)) = (IF ((x63(_M)) = 1) THEN (x64(_M)) ELSE (IF ((x63(_M)) = 2) THEN (x64(_M)) ELSE (IF ((x63(_M)) = 3) THEN (x64(_M)) ELSE (IF ((x63(_M)) = 4) THEN (x93(_M)) ELSE (IF ((x63(_M)) = 5) THEN (x93(_M)) ELSE (x64(_M)) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF));
+DEF__186 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x86(_M)) = (IF ((x63(_M)) = 1) THEN (x65(_M)) ELSE (IF ((x63(_M)) = 2) THEN (x65(_M)) ELSE (IF ((x63(_M)) = 3) THEN (x65(_M)) ELSE (IF ((x63(_M)) = 4) THEN 10 ELSE (IF ((x63(_M)) = 5) THEN 2 ELSE (x65(_M)) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF));
+DEF__187 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x87(_M)) = (IF ((x94(_M)) = 2) THEN 0 ELSE (x94(_M)) ENDIF));
+DEF__188 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x88(_M)) = (IF ((x89(_M)) = 3) THEN 0 ELSE (x89(_M)) ENDIF));
+DEF__189 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x89(_M)) = (IF ((x90(_M)) = 2) THEN 0 ELSE (x90(_M)) ENDIF));
+DEF__190 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x90(_M)) = (IF ((x62(_M)) = 1) THEN 0 ELSE (x62(_M)) ENDIF));
+DEF__191 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x91(_M)) = (IF ((x101(_M)) = 3) THEN 0 ELSE (x101(_M)) ENDIF));
+DEF__192 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x92(_M)) = (IF ((x61(_M)) = 1) THEN 0 ELSE (x61(_M)) ENDIF));
+DEF__193 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x93(_M)) = (IF ((x87(_M)) = 3) THEN 0 ELSE (x87(_M)) ENDIF));
+DEF__194 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x94(_M)) = (IF ((x64(_M)) = 1) THEN 0 ELSE (x64(_M)) ENDIF));
+DEF__195 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x95(_M)) = (IF ((x96(_M)) = 3) THEN 0 ELSE (x96(_M)) ENDIF));
+DEF__196 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x96(_M)) = (IF ((x97(_M)) = 2) THEN 0 ELSE (x97(_M)) ENDIF));
+DEF__197 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x97(_M)) = (IF ((x58(_M)) = 1) THEN 0 ELSE (x58(_M)) ENDIF));
+DEF__198 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x98(_M)) = (IF ((x99(_M)) = 2) THEN 0 ELSE (x99(_M)) ENDIF));
+DEF__199 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x99(_M)) = (IF ((x60(_M)) = 1) THEN 0 ELSE (x60(_M)) ENDIF));
+DEF__200 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x100(_M)) = (IF ((x91(_M)) = 4) THEN 0 ELSE (x91(_M)) ENDIF));
+DEF__201 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x101(_M)) = (IF ((x92(_M)) = 2) THEN 0 ELSE (x92(_M)) ENDIF));
+DEF__202 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x102(_M)) = (IF (((((((x2(_M)) = 2) OR ((x50(_M)) = 2)) OR ((x53(_M)) = 2)) AND ((((x3(_M)) = 2) OR ((x50(_M)) = 2)) OR ((x53(_M)) = 2))) AND ((x53(_M)) = 2)) <=> TRUE) THEN 2 ELSE (x39(_M)) ENDIF));
+DEF__115 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x15(_M)) = (IF ((NOT ((x59(_M)) = 0)) <=> TRUE) THEN (IF ((x65(_M)) = 1) THEN (x76(_M)) ELSE (IF ((x65(_M)) = 2) THEN ((NOT ((x14(_M)) = 8)) AND ((NOT ((x14(_M)) = 6)) AND (x76(_M)))) ELSE (IF ((x65(_M)) = 3) THEN (x76(_M)) ELSE (IF ((x65(_M)) = 4) THEN (x76(_M)) ELSE (IF ((x65(_M)) = 5) THEN (x76(_M)) ELSE (IF ((x65(_M)) = 6) THEN (x76(_M)) ELSE (IF ((x65(_M)) = 7) THEN (x76(_M)) ELSE (IF ((x65(_M)) = 8) THEN (x76(_M)) ELSE (IF ((x65(_M)) = 9) THEN (IF ((x63(_M)) = 1) THEN (x76(_M)) ELSE (IF ((x63(_M)) = 2) THEN (x76(_M)) ELSE (IF ((x63(_M)) = 3) THEN (x76(_M)) ELSE (((x63(_M)) = 4) OR (x76(_M))) ENDIF) ENDIF) ENDIF) ELSE (x76(_M)) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x76(_M)) ENDIF));
+DEF__203 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x103(_M)) = (IF (((((((x2(_M)) = 2) OR ((x50(_M)) = 2)) OR ((x53(_M)) = 2)) AND ((((x3(_M)) = 2) OR ((x50(_M)) = 2)) OR ((x53(_M)) = 2))) AND ((x53(_M)) = 2)) <=> TRUE) THEN (IF ((x86(_M)) = 9) THEN (IF ((x85(_M)) = 1) THEN 2 ELSE (IF ((x85(_M)) = 2) THEN (IF ((x30(_M)) = 6) THEN 1 ELSE (IF ((x30(_M)) < 6) THEN 2 ELSE (IF ((x11(_M)) <=> TRUE) THEN 0 ELSE (x42(_M)) ENDIF) ENDIF) ENDIF) ELSE (IF ((x85(_M)) = 3) THEN 2 ELSE (x42(_M)) ENDIF) ENDIF) ENDIF) ELSE (x42(_M)) ENDIF) ELSE (x42(_M)) ENDIF));
+DEF__116 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x16(_M)) = (IF ((NOT ((x59(_M)) = 0)) <=> TRUE) THEN (IF ((x65(_M)) = 1) THEN (x73(_M)) ELSE (IF ((x65(_M)) = 2) THEN (x73(_M)) ELSE (IF ((x65(_M)) = 3) THEN (x73(_M)) ELSE (IF ((x65(_M)) = 4) THEN (x73(_M)) ELSE (IF ((x65(_M)) = 5) THEN (x73(_M)) ELSE (IF ((x65(_M)) = 6) THEN (x73(_M)) ELSE (IF ((x65(_M)) = 7) THEN (x73(_M)) ELSE (IF ((x65(_M)) = 8) THEN (x73(_M)) ELSE (IF ((x65(_M)) = 9) THEN (IF ((x63(_M)) = 1) THEN (x73(_M)) ELSE (IF ((x63(_M)) = 2) THEN (x73(_M)) ELSE (IF ((x63(_M)) = 3) THEN (x73(_M)) ELSE ((NOT ((x63(_M)) = 4)) AND (x73(_M))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65(_M)) = 10) THEN (IF ((x55(_M)) = 1) THEN (x73(_M)) ELSE (IF ((x55(_M)) = 2) THEN (x73(_M)) ELSE (((x55(_M)) = 3) OR (x73(_M))) ENDIF) ENDIF) ELSE (IF ((x65(_M)) = 11) THEN (x73(_M)) ELSE (IF ((x65(_M)) = 12) THEN (IF ((x57(_M)) = 1) THEN (x73(_M)) ELSE (IF ((x57(_M)) = 2) THEN (x73(_M)) ELSE ((NOT ((x57(_M)) = 3)) AND (x73(_M))) ENDIF) ENDIF) ELSE (x73(_M)) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x73(_M)) ENDIF));
+DEF__204 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x104(_M)) = (IF (((((((x2(_M)) = 2) OR ((x50(_M)) = 2)) OR ((x53(_M)) = 2)) AND ((((x3(_M)) = 2) OR ((x50(_M)) = 2)) OR ((x53(_M)) = 2))) AND ((x53(_M)) = 2)) <=> TRUE) THEN (IF ((x86(_M)) = 9) THEN (IF ((x85(_M)) = 1) THEN 2 ELSE (IF ((x85(_M)) = 2) THEN (IF ((x30(_M)) = 6) THEN 1 ELSE (IF ((x30(_M)) < 6) THEN 2 ELSE (IF ((x11(_M)) <=> TRUE) THEN 0 ELSE (x43(_M)) ENDIF) ENDIF) ENDIF) ELSE (IF ((x85(_M)) = 3) THEN 2 ELSE (x43(_M)) ENDIF) ENDIF) ENDIF) ELSE (x43(_M)) ENDIF) ELSE (x43(_M)) ENDIF));
+DEF__117 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x17(_M)) = (IF ((NOT ((x59(_M)) = 0)) <=> TRUE) THEN (IF ((x65(_M)) = 1) THEN (x68(_M)) ELSE (IF ((x65(_M)) = 2) THEN (x68(_M)) ELSE (IF ((x65(_M)) = 3) THEN (x68(_M)) ELSE (IF ((x65(_M)) = 4) THEN (x68(_M)) ELSE (IF ((x65(_M)) = 5) THEN (x68(_M)) ELSE (IF ((x65(_M)) = 6) THEN (x68(_M)) ELSE (IF ((x65(_M)) = 7) THEN (x68(_M)) ELSE (IF ((x65(_M)) = 8) THEN (x68(_M)) ELSE (IF ((x65(_M)) = 9) THEN (x68(_M)) ELSE (IF ((x65(_M)) = 10) THEN (IF ((x55(_M)) = 1) THEN (x68(_M)) ELSE (IF ((x55(_M)) = 2) THEN (x68(_M)) ELSE (((x55(_M)) = 3) OR (x68(_M))) ENDIF) ENDIF) ELSE (IF ((x65(_M)) = 11) THEN (x68(_M)) ELSE (IF ((x65(_M)) = 12) THEN (IF ((x57(_M)) = 1) THEN (x68(_M)) ELSE (IF ((x57(_M)) = 2) THEN (x68(_M)) ELSE ((NOT ((x57(_M)) = 3)) AND ((NOT ((x57(_M)) = 4)) AND (x68(_M)))) ENDIF) ENDIF) ELSE (x68(_M)) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x68(_M)) ENDIF));
+DEF__205 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x105(_M)) = (IF (((((((x2(_M)) = 2) OR ((x50(_M)) = 2)) OR ((x53(_M)) = 2)) AND ((((x3(_M)) = 2) OR ((x50(_M)) = 2)) OR ((x53(_M)) = 2))) AND ((x53(_M)) = 2)) <=> TRUE) THEN (IF ((x86(_M)) = 9) THEN (IF ((x85(_M)) = 1) THEN 0 ELSE (IF ((x85(_M)) = 2) THEN (IF ((x30(_M)) = 6) THEN (x30(_M)) ELSE (IF ((x30(_M)) < 6) THEN 0 ELSE (x30(_M)) ENDIF) ENDIF) ELSE (IF ((x85(_M)) = 3) THEN 0 ELSE (x30(_M)) ENDIF) ENDIF) ENDIF) ELSE (x44(_M)) ENDIF) ELSE (x44(_M)) ENDIF));
+DEF__206 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x106(_M)) = (IF (((((((x2(_M)) = 2) OR ((x50(_M)) = 2)) OR ((x53(_M)) = 2)) AND ((((x3(_M)) = 2) OR ((x50(_M)) = 2)) OR ((x53(_M)) = 2))) AND ((x53(_M)) = 2)) <=> TRUE) THEN 2 ELSE (x47(_M)) ENDIF));
+DEF__207 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x107(_M)) = (IF (((((((x2(_M)) = 2) OR ((x50(_M)) = 2)) OR ((x53(_M)) = 2)) AND ((((x3(_M)) = 2) OR ((x50(_M)) = 2)) OR ((x53(_M)) = 2))) AND ((x53(_M)) = 2)) <=> TRUE) THEN 2 ELSE (x48(_M)) ENDIF));
+DEF__120 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x20(_M)) = (IF ((NOT ((x59(_M)) = 0)) <=> TRUE) THEN (IF ((x65(_M)) = 1) THEN (x74(_M)) ELSE (IF ((x65(_M)) = 2) THEN ((NOT ((x14(_M)) = 8)) AND ((NOT ((x14(_M)) = 6)) AND (x74(_M)))) ELSE (IF ((x65(_M)) = 3) THEN (((x14(_M)) = 2) OR (x74(_M))) ELSE (IF ((x65(_M)) = 4) THEN ((NOT ((x14(_M)) = 1)) AND (x74(_M))) ELSE (x74(_M)) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x74(_M)) ENDIF));
+DEF__208 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x108(_M)) = (IF (((((((x2(_M)) = 2) OR ((x50(_M)) = 2)) OR ((x53(_M)) = 2)) AND ((((x3(_M)) = 2) OR ((x50(_M)) = 2)) OR ((x53(_M)) = 2))) AND ((x53(_M)) = 2)) <=> TRUE) THEN (IF ((x86(_M)) = 9) THEN (IF ((x85(_M)) = 1) THEN 2 ELSE (IF ((x85(_M)) = 2) THEN (IF ((x30(_M)) = 6) THEN 1 ELSE (IF ((x30(_M)) < 6) THEN 2 ELSE (IF ((x11(_M)) <=> TRUE) THEN 0 ELSE (x52(_M)) ENDIF) ENDIF) ENDIF) ELSE (IF ((x85(_M)) = 3) THEN 2 ELSE (x52(_M)) ENDIF) ENDIF) ENDIF) ELSE (x52(_M)) ENDIF) ELSE (x52(_M)) ENDIF));
+DEF__121 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x21(_M)) = (IF ((NOT ((x59(_M)) = 0)) <=> TRUE) THEN (IF ((x65(_M)) = 1) THEN (x66(_M)) ELSE (IF ((x65(_M)) = 2) THEN ((NOT ((x14(_M)) = 8)) AND ((NOT ((x14(_M)) = 6)) AND (x66(_M)))) ELSE (IF ((x65(_M)) = 3) THEN (x66(_M)) ELSE (IF ((x65(_M)) = 4) THEN (x66(_M)) ELSE (IF ((x65(_M)) = 5) THEN (x66(_M)) ELSE (IF ((x65(_M)) = 6) THEN (IF ((x14(_M)) = 5) THEN (x66(_M)) ELSE (((x14(_M)) = 4) OR (x66(_M))) ENDIF) ELSE (x66(_M)) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x66(_M)) ENDIF));
+DEF__209 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x109(_M)) = (IF (((((((x2(_M)) = 2) OR ((x50(_M)) = 2)) OR ((x53(_M)) = 2)) AND ((((x3(_M)) = 2) OR ((x50(_M)) = 2)) OR ((x53(_M)) = 2))) AND ((x53(_M)) = 2)) <=> TRUE) THEN 4 ELSE (x83(_M)) ENDIF));
+DEF__122 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x22(_M)) = (IF ((NOT ((x59(_M)) = 0)) <=> TRUE) THEN (IF ((x65(_M)) = 1) THEN (x71(_M)) ELSE (IF ((x65(_M)) = 2) THEN ((NOT ((x14(_M)) = 8)) AND ((NOT ((x14(_M)) = 6)) AND (x71(_M)))) ELSE (IF ((x65(_M)) = 3) THEN (x71(_M)) ELSE (IF ((x65(_M)) = 4) THEN (IF ((x14(_M)) = 1) THEN (x71(_M)) ELSE (((x14(_M)) = 3) OR (x71(_M))) ENDIF) ELSE (x71(_M)) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x71(_M)) ENDIF));
+DEF__210 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x110(_M)) = (IF (((((((x2(_M)) = 2) OR ((x50(_M)) = 2)) OR ((x53(_M)) = 2)) AND ((((x3(_M)) = 2) OR ((x50(_M)) = 2)) OR ((x53(_M)) = 2))) AND ((x53(_M)) = 2)) <=> TRUE) THEN (IF ((x86(_M)) = 9) THEN (IF ((x85(_M)) = 1) THEN 2 ELSE (IF ((x85(_M)) = 2) THEN (IF ((x30(_M)) = 6) THEN 3 ELSE (IF ((x30(_M)) < 6) THEN 2 ELSE (IF ((x11(_M)) <=> TRUE) THEN 1 ELSE (x85(_M)) ENDIF) ENDIF) ENDIF) ELSE (IF ((x85(_M)) = 3) THEN 2 ELSE (x85(_M)) ENDIF) ENDIF) ENDIF) ELSE (x85(_M)) ENDIF) ELSE (x85(_M)) ENDIF));
+DEF__211 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x111(_M)) = (IF (((((x12(_M)) = 2) OR ((x50(_M)) = 2)) OR ((x53(_M)) = 2)) <=> TRUE) THEN 2 ELSE (x36(_M)) ENDIF));
+DEF__212 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x112(_M)) = (IF (((((x12(_M)) = 2) OR ((x50(_M)) = 2)) OR ((x53(_M)) = 2)) <=> TRUE) THEN 2 ELSE (x82(_M)) ENDIF));
+DEF__126 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x26(_M)) = (IF (((x37(_M)) + 1) < 9) THEN ((x37(_M)) + 1) ELSE 9 ENDIF));
+DEF__213 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x113(_M)) = (IF ((x11(_M)) <=> TRUE) THEN 0 ELSE (x77(_M)) ENDIF));
+DEF__127 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x27(_M)) = (IF (((x51(_M)) + 1) < 9) THEN ((x51(_M)) + 1) ELSE 9 ENDIF));
+DEF__214 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x114(_M)) = (IF ((x11(_M)) <=> TRUE) THEN 0 ELSE (x78(_M)) ENDIF));
+DEF__128 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x28(_M)) = ((IF ((x55(_M)) = 1) THEN (x46(_M)) ELSE (IF ((x55(_M)) = 2) THEN (x46(_M)) ELSE (IF ((x55(_M)) = 3) THEN (x118(_M)) ELSE (IF ((x55(_M)) = 4) THEN (x118(_M)) ELSE (x46(_M)) ENDIF) ENDIF) ENDIF) ENDIF) + 1));
+DEF__215 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x115(_M)) = (IF ((x11(_M)) <=> TRUE) THEN 0 ELSE (x79(_M)) ENDIF));
+DEF__216 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x116(_M)) = (IF ((x11(_M)) <=> TRUE) THEN 1 ELSE (x80(_M)) ENDIF));
+DEF__129 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x29(_M)) = (IF ((x28(_M)) < 6) THEN (x28(_M)) ELSE 6 ENDIF));
+DEF__217 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x117(_M)) = (IF ((x55(_M)) = 1) THEN (x54(_M)) ELSE (IF ((x55(_M)) = 2) THEN (x54(_M)) ELSE (IF ((x55(_M)) = 3) THEN (x119(_M)) ELSE (IF ((x55(_M)) = 4) THEN (x119(_M)) ELSE (x54(_M)) ENDIF) ENDIF) ENDIF) ENDIF));
+DEF__130 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x30(_M)) = (IF (((x44(_M)) + 1) < 6) THEN ((x44(_M)) + 1) ELSE 6 ENDIF));
+DEF__131 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x31(_M)) = (IF (((x40(_M)) + 1) < 11) THEN ((x40(_M)) + 1) ELSE 11 ENDIF));
+DEF__218 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x118(_M)) = (IF ((x120(_M)) = 3) THEN 0 ELSE (IF ((x54(_M)) = 1) THEN 0 ELSE (x46(_M)) ENDIF) ENDIF));
+DEF__132 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x32(_M)) = (IF (((x41(_M)) + 1) < 6) THEN ((x41(_M)) + 1) ELSE 6 ENDIF));
+DEF__219 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x119(_M)) = (IF ((x120(_M)) = 3) THEN 0 ELSE (x120(_M)) ENDIF));
+DEF__133 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x33(_M)) = (IF (((x38(_M)) + 1) < 6) THEN ((x38(_M)) + 1) ELSE 6 ENDIF));
+DEF__220 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x120(_M)) = (IF ((x121(_M)) = 2) THEN 0 ELSE (x121(_M)) ENDIF));
+DEF__134 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x34(_M)) = ((IF ((x83(_M)) = 1) THEN (x44(_M)) ELSE (IF ((x83(_M)) = 2) THEN (x44(_M)) ELSE (IF ((x83(_M)) = 3) THEN (x105(_M)) ELSE (IF ((x83(_M)) = 4) THEN (IF ((NOT ((((((((x2(_M)) = 2) AND ((x50(_M)) = 2)) OR (((x2(_M)) = 2) AND ((x53(_M)) = 2))) OR (((x53(_M)) = 2) AND ((x50(_M)) = 2))) OR (((x43(_M)) = 2) AND ((x2(_M)) = 2))) OR (((x43(_M)) = 2) AND ((x50(_M)) = 2))) OR (((x43(_M)) = 2) AND ((x53(_M)) = 2)))) <=> TRUE) THEN (IF ((NOT (((x52(_M)) = 2) OR ((x53(_M)) = 2))) <=> TRUE) THEN (IF ((NOT ((((((((x3(_M)) = 2) AND ((x50(_M)) = 2)) OR (((x3(_M)) = 2) AND ((x53(_M)) = 2))) OR (((x53(_M)) = 2) AND ((x50(_M)) = 2))) OR (((x42(_M)) = 2) AND ((x3(_M)) = 2))) OR (((x42(_M)) = 2) AND ((x50(_M)) = 2))) OR (((x42(_M)) = 2) AND ((x53(_M)) = 2)))) <=> TRUE) THEN (x44(_M)) ELSE (x105(_M)) ENDIF) ELSE (x105(_M)) ENDIF) ELSE (x105(_M)) ENDIF) ELSE (x44(_M)) ENDIF) ENDIF) ENDIF) ENDIF) + 1));
+DEF__221 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x121(_M)) = (IF ((x54(_M)) = 1) THEN 0 ELSE (x54(_M)) ENDIF));
+DEF__222 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x122(_M)) = (IF ((x57(_M)) = 1) THEN (x56(_M)) ELSE (IF ((x57(_M)) = 2) THEN (x56(_M)) ELSE (IF ((x57(_M)) = 3) THEN (x126(_M)) ELSE (IF ((x57(_M)) = 4) THEN (x126(_M)) ELSE (x56(_M)) ENDIF) ENDIF) ENDIF) ENDIF));
+DEF__135 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x35(_M)) = (IF ((x34(_M)) < 6) THEN (x34(_M)) ELSE 6 ENDIF));
+DEF__223 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x123(_M)) = (IF ((x26(_M)) = 8) THEN 3 ELSE (x57(_M)) ENDIF));
+DEF__136 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x36(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x36((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x36((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x36((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x36((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x36((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (IF ((x14((_M - 1))) = 5) THEN (x36((_M - 1))) ELSE (IF ((x14((_M - 1))) = 4) THEN 1 ELSE (x36((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 7) THEN (x36((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x36((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x82((_M - 1))) = 1) THEN (x111((_M - 1))) ELSE (IF ((x82((_M - 1))) = 2) THEN (IF ((NOT ((x13((_M - 1))) = 2)) <=> TRUE) THEN 1 ELSE (x111((_M - 1))) ENDIF) ELSE (x36((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x36((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x36((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN (x36((_M - 1))) ELSE (IF ((x55((_M - 1))) = 4) THEN 1 ELSE (x36((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x36((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x36((_M - 1))) ENDIF) ENDIF));
+DEF__224 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x124(_M)) = (IF ((x128(_M)) = 3) THEN 0 ELSE (x128(_M)) ENDIF));
+DEF__137 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x37(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x37((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x37((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x37((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x37((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x37((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (x37((_M - 1))) ELSE (IF ((x65((_M - 1))) = 7) THEN (x37((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x37((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (x37((_M - 1))) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x37((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x37((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN 0 ELSE (x37((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 11) THEN (x37((_M - 1))) ELSE (IF ((x65((_M - 1))) = 12) THEN (x26((_M - 1))) ELSE (x37((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x37((_M - 1))) ENDIF) ENDIF));
+DEF__225 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x125(_M)) = (IF ((x56(_M)) = 1) THEN 0 ELSE (x56(_M)) ENDIF));
+DEF__138 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x38(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x38((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x38((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x38((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x38((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x38((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (x38((_M - 1))) ELSE (IF ((x65((_M - 1))) = 7) THEN (x38((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x38((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x84((_M - 1))) = 1) THEN (IF (((NOT (((x9((_M - 1))) = 0) OR ((x10((_M - 1))) = 0))) AND (x5((_M - 1)))) <=> TRUE) THEN 0 ELSE (x33((_M - 1))) ENDIF) ELSE (IF ((x84((_M - 1))) = 2) THEN (IF ((((x33((_M - 1))) = 6) AND ((((x9((_M - 1))) = 0) OR ((x10((_M - 1))) = 0)) OR (NOT (x5((_M - 1)))))) <=> TRUE) THEN (x33((_M - 1))) ELSE (IF (((((((x33((_M - 1))) = 6) AND ((x9((_M - 1))) = 2)) AND ((x10((_M - 1))) = 2)) AND (x5((_M - 1)))) AND (NOT (x6((_M - 1))))) <=> TRUE) THEN (x33((_M - 1))) ELSE (IF (((((x33((_M - 1))) < 6) AND ((((x9((_M - 1))) = 0) OR ((x10((_M - 1))) = 0)) OR (NOT (x5((_M - 1)))))) OR ((x5((_M - 1))) AND (((x6((_M - 1))) OR ((x9((_M - 1))) = 1)) OR ((x10((_M - 1))) = 1)))) <=> TRUE) THEN 0 ELSE (x33((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x84((_M - 1))) = 3) THEN (IF (((((NOT ((x9((_M - 1))) = 2)) AND (NOT ((x10((_M - 1))) = 2))) AND (NOT (x5((_M - 1))))) OR (x6((_M - 1)))) <=> TRUE) THEN 0 ELSE (x33((_M - 1))) ENDIF) ELSE (x33((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (x38((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x38((_M - 1))) ENDIF) ENDIF));
+DEF__226 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x126(_M)) = (IF ((x127(_M)) = 5) THEN 0 ELSE (x127(_M)) ENDIF));
+DEF__139 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x39(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x39((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x39((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x39((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x39((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x39((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (IF ((x14((_M - 1))) = 5) THEN (x39((_M - 1))) ELSE (IF ((x14((_M - 1))) = 4) THEN 0 ELSE (x39((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 7) THEN (x39((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x39((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x83((_M - 1))) = 1) THEN (IF (((NOT ((((x50((_M - 1))) = 0) AND ((x53((_M - 1))) = 0)) AND ((x2((_M - 1))) = 0))) AND (NOT ((((x50((_M - 1))) = 0) AND ((x53((_M - 1))) = 0)) AND ((x3((_M - 1))) = 0)))) <=> TRUE) THEN 0 ELSE (IF ((((((((x50((_M - 1))) = 0) AND ((x50((_M - 1))) = 0)) AND ((x53((_M - 1))) = 0)) AND ((x53((_M - 1))) = 0)) AND ((x2((_M - 1))) = 0)) AND ((x3((_M - 1))) = 0)) <=> TRUE) THEN 0 ELSE (x39((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x83((_M - 1))) = 2) THEN (IF ((((((x2((_M - 1))) = 0) AND ((x50((_M - 1))) = 0)) AND ((x53((_M - 1))) = 0)) AND ((((x3((_M - 1))) = 0) AND ((x50((_M - 1))) = 0)) AND ((x53((_M - 1))) = 0))) <=> TRUE) THEN 0 ELSE (IF (((((((((x2((_M - 1))) = 2) AND ((x50((_M - 1))) = 2)) OR (((x2((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) OR (((x53((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x2((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) <=> TRUE) THEN (IF (((((((((x3((_M - 1))) = 2) AND ((x50((_M - 1))) = 2)) OR (((x3((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) OR (((x53((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x3((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) <=> TRUE) THEN (IF ((((x52((_M - 1))) = 2) OR ((x53((_M - 1))) = 2)) <=> TRUE) THEN 1 ELSE (x39((_M - 1))) ENDIF) ELSE (x39((_M - 1))) ENDIF) ELSE (x39((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x83((_M - 1))) = 3) THEN (x102((_M - 1))) ELSE (IF ((x83((_M - 1))) = 4) THEN (IF ((NOT ((((((((x2((_M - 1))) = 2) AND ((x50((_M - 1))) = 2)) OR (((x2((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) OR (((x53((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x2((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x53((_M - 1))) = 2)))) <=> TRUE) THEN (IF ((NOT (((x52((_M - 1))) = 2) OR ((x53((_M - 1))) = 2))) <=> TRUE) THEN (IF ((NOT ((((((((x3((_M - 1))) = 2) AND ((x50((_M - 1))) = 2)) OR (((x3((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) OR (((x53((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x3((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x53((_M - 1))) = 2)))) <=> TRUE) THEN 0 ELSE (x102((_M - 1))) ENDIF) ELSE (x102((_M - 1))) ENDIF) ELSE (x102((_M - 1))) ENDIF) ELSE (x39((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x39((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x39((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN (x39((_M - 1))) ELSE (IF ((x55((_M - 1))) = 4) THEN 0 ELSE (x39((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x39((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x39((_M - 1))) ENDIF) ENDIF));
+DEF__227 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x127(_M)) = (IF ((x124(_M)) = 4) THEN 0 ELSE (x124(_M)) ENDIF));
+DEF__140 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x40(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x40((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x40((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x40((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x40((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x40((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (IF ((x14((_M - 1))) = 5) THEN (x40((_M - 1))) ELSE (IF ((x14((_M - 1))) = 4) THEN 0 ELSE (x40((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 7) THEN (x40((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x40((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (x31((_M - 1))) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x40((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x40((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN (x40((_M - 1))) ELSE (IF ((x55((_M - 1))) = 4) THEN 0 ELSE (x40((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x40((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x40((_M - 1))) ENDIF) ENDIF));
+DEF__228 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x128(_M)) = (IF ((x125(_M)) = 2) THEN 0 ELSE (x125(_M)) ENDIF));
+DEF__141 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x41(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x41((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x41((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x41((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x41((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x41((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (x41((_M - 1))) ELSE (IF ((x65((_M - 1))) = 7) THEN (x41((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x41((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x81((_M - 1))) = 1) THEN (IF (((NOT ((x7((_M - 1))) = 0)) AND (x8((_M - 1)))) <=> TRUE) THEN 0 ELSE (x32((_M - 1))) ENDIF) ELSE (IF ((x81((_M - 1))) = 2) THEN (IF ((((x32((_M - 1))) = 6) AND (((x7((_M - 1))) = 0) OR (NOT (x8((_M - 1)))))) <=> TRUE) THEN (x32((_M - 1))) ELSE (IF ((((((x32((_M - 1))) = 6) AND ((x7((_M - 1))) = 2)) AND (x8((_M - 1)))) AND (NOT (x6((_M - 1))))) <=> TRUE) THEN (x32((_M - 1))) ELSE (IF (((((x32((_M - 1))) < 6) AND (((x7((_M - 1))) = 0) OR (NOT (x8((_M - 1)))))) OR ((x8((_M - 1))) AND (((x7((_M - 1))) = 1) OR (x6((_M - 1)))))) <=> TRUE) THEN 0 ELSE (x32((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x81((_M - 1))) = 3) THEN (IF (((NOT (((x7((_M - 1))) = 2) AND (x8((_M - 1))))) OR (x6((_M - 1)))) <=> TRUE) THEN 0 ELSE (x32((_M - 1))) ENDIF) ELSE (x32((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (x41((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x41((_M - 1))) ENDIF) ENDIF));
+DEF__229 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x129(_M)) = ((NOT (x17(_M))) OR (((((x20(_M)) AND (x22(_M))) AND (x21(_M))) AND (x15(_M))) AND (x16(_M)))));
+DEF__142 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x42(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x42((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x42((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x42((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x42((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x42((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (IF ((x14((_M - 1))) = 5) THEN (x42((_M - 1))) ELSE (IF ((x14((_M - 1))) = 4) THEN 0 ELSE (x42((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 7) THEN (x42((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x42((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x80((_M - 1))) = 1) THEN (x77((_M - 1))) ELSE (IF ((x80((_M - 1))) = 2) THEN (IF ((x35((_M - 1))) = 6) THEN 1 ELSE (IF ((x35((_M - 1))) < 6) THEN 2 ELSE (x113((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x80((_M - 1))) = 3) THEN (x113((_M - 1))) ELSE (x77((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x42((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x42((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN (x42((_M - 1))) ELSE (IF ((x55((_M - 1))) = 4) THEN 0 ELSE (x42((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x42((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x42((_M - 1))) ENDIF) ENDIF));
+DEF__143 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x43(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x43((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x43((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x43((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x43((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x43((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (IF ((x14((_M - 1))) = 5) THEN (x43((_M - 1))) ELSE (IF ((x14((_M - 1))) = 4) THEN 0 ELSE (x43((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 7) THEN (x43((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x43((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x80((_M - 1))) = 1) THEN (x78((_M - 1))) ELSE (IF ((x80((_M - 1))) = 2) THEN (IF ((x35((_M - 1))) = 6) THEN 1 ELSE (IF ((x35((_M - 1))) < 6) THEN 2 ELSE (x114((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x80((_M - 1))) = 3) THEN (x114((_M - 1))) ELSE (x78((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x43((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x43((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN (x43((_M - 1))) ELSE (IF ((x55((_M - 1))) = 4) THEN 0 ELSE (x43((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x43((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x43((_M - 1))) ENDIF) ENDIF));
+DEF__144 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x44(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x44((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x44((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x44((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x44((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x44((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (x44((_M - 1))) ELSE (IF ((x65((_M - 1))) = 7) THEN (x44((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x44((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x80((_M - 1))) = 1) THEN (x35((_M - 1))) ELSE (IF ((x80((_M - 1))) = 2) THEN (IF ((x35((_M - 1))) = 6) THEN (x35((_M - 1))) ELSE (IF ((x35((_M - 1))) < 6) THEN 0 ELSE (x35((_M - 1))) ENDIF) ENDIF) ELSE (x35((_M - 1))) ENDIF) ENDIF) ELSE (x44((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x44((_M - 1))) ENDIF) ENDIF));
+DEF__145 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x45(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x45((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x45((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x45((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x45((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x45((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (x45((_M - 1))) ELSE (IF ((x65((_M - 1))) = 7) THEN (x45((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x45((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (x45((_M - 1))) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x45((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x45((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN 0 ELSE (x45((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 11) THEN (x45((_M - 1))) ELSE (IF ((x65((_M - 1))) = 12) THEN (IF ((x122((_M - 1))) = 1) THEN 1 ELSE (IF ((x122((_M - 1))) = 2) THEN 0 ELSE (IF ((x122((_M - 1))) = 3) THEN 3 ELSE (IF ((x122((_M - 1))) = 4) THEN 0 ELSE (IF ((x122((_M - 1))) = 5) THEN 0 ELSE (x45((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x45((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x45((_M - 1))) ENDIF) ENDIF));
+DEF__146 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x46(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x46((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x46((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x46((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x46((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x46((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (x46((_M - 1))) ELSE (IF ((x65((_M - 1))) = 7) THEN (x46((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x46((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (x46((_M - 1))) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x117((_M - 1))) = 1) THEN (IF (((NOT ((x4((_M - 1))) = 0)) AND (x5((_M - 1)))) <=> TRUE) THEN 0 ELSE (IF ((((x4((_M - 1))) = 0) OR (NOT (x5((_M - 1))))) <=> TRUE) THEN 0 ELSE (x29((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x117((_M - 1))) = 2) THEN (x29((_M - 1))) ELSE (IF ((x117((_M - 1))) = 3) THEN (IF ((((NOT ((x4((_M - 1))) = 2)) AND (NOT (x5((_M - 1))))) OR (x6((_M - 1)))) <=> TRUE) THEN 0 ELSE (IF (((((x4((_M - 1))) = 2) AND (x5((_M - 1)))) AND (NOT (x6((_M - 1))))) <=> TRUE) THEN 0 ELSE (x29((_M - 1))) ENDIF) ENDIF) ELSE (x29((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (x46((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x46((_M - 1))) ENDIF) ENDIF));
+DEF__147 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x47(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x47((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x47((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x47((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x47((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x47((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (IF ((x14((_M - 1))) = 5) THEN (x47((_M - 1))) ELSE (IF ((x14((_M - 1))) = 4) THEN 0 ELSE (x47((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 7) THEN (x47((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x47((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x83((_M - 1))) = 1) THEN (IF (((NOT ((((x50((_M - 1))) = 0) AND ((x53((_M - 1))) = 0)) AND ((x2((_M - 1))) = 0))) AND (NOT ((((x50((_M - 1))) = 0) AND ((x53((_M - 1))) = 0)) AND ((x3((_M - 1))) = 0)))) <=> TRUE) THEN 1 ELSE (IF ((((((((x50((_M - 1))) = 0) AND ((x50((_M - 1))) = 0)) AND ((x53((_M - 1))) = 0)) AND ((x53((_M - 1))) = 0)) AND ((x2((_M - 1))) = 0)) AND ((x3((_M - 1))) = 0)) <=> TRUE) THEN 0 ELSE (x47((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x83((_M - 1))) = 2) THEN (IF ((((((x2((_M - 1))) = 0) AND ((x50((_M - 1))) = 0)) AND ((x53((_M - 1))) = 0)) AND ((((x3((_M - 1))) = 0) AND ((x50((_M - 1))) = 0)) AND ((x53((_M - 1))) = 0))) <=> TRUE) THEN 0 ELSE (IF (((((((((x2((_M - 1))) = 2) AND ((x50((_M - 1))) = 2)) OR (((x2((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) OR (((x53((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x2((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) <=> TRUE) THEN (IF (((((((((x3((_M - 1))) = 2) AND ((x50((_M - 1))) = 2)) OR (((x3((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) OR (((x53((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x3((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) <=> TRUE) THEN (IF ((((x52((_M - 1))) = 2) OR ((x53((_M - 1))) = 2)) <=> TRUE) THEN 2 ELSE (x47((_M - 1))) ENDIF) ELSE (x47((_M - 1))) ENDIF) ELSE (x47((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x83((_M - 1))) = 3) THEN (x106((_M - 1))) ELSE (IF ((x83((_M - 1))) = 4) THEN (IF ((NOT ((((((((x2((_M - 1))) = 2) AND ((x50((_M - 1))) = 2)) OR (((x2((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) OR (((x53((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x2((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x53((_M - 1))) = 2)))) <=> TRUE) THEN (IF ((NOT (((x52((_M - 1))) = 2) OR ((x53((_M - 1))) = 2))) <=> TRUE) THEN (IF ((NOT ((((((((x3((_M - 1))) = 2) AND ((x50((_M - 1))) = 2)) OR (((x3((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) OR (((x53((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x3((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x53((_M - 1))) = 2)))) <=> TRUE) THEN 1 ELSE (x106((_M - 1))) ENDIF) ELSE (x106((_M - 1))) ENDIF) ELSE (x106((_M - 1))) ENDIF) ELSE (x47((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x47((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x47((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN (x47((_M - 1))) ELSE (IF ((x55((_M - 1))) = 4) THEN 0 ELSE (x47((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x47((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x47((_M - 1))) ENDIF) ENDIF));
+DEF__148 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x48(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x48((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x48((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x48((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x48((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x48((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (IF ((x14((_M - 1))) = 5) THEN (x48((_M - 1))) ELSE (IF ((x14((_M - 1))) = 4) THEN 0 ELSE (x48((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 7) THEN (x48((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x48((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x83((_M - 1))) = 1) THEN (IF (((NOT ((((x50((_M - 1))) = 0) AND ((x53((_M - 1))) = 0)) AND ((x2((_M - 1))) = 0))) AND (NOT ((((x50((_M - 1))) = 0) AND ((x53((_M - 1))) = 0)) AND ((x3((_M - 1))) = 0)))) <=> TRUE) THEN 1 ELSE (IF ((((((((x50((_M - 1))) = 0) AND ((x50((_M - 1))) = 0)) AND ((x53((_M - 1))) = 0)) AND ((x53((_M - 1))) = 0)) AND ((x2((_M - 1))) = 0)) AND ((x3((_M - 1))) = 0)) <=> TRUE) THEN 0 ELSE (x48((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x83((_M - 1))) = 2) THEN (IF ((((((x2((_M - 1))) = 0) AND ((x50((_M - 1))) = 0)) AND ((x53((_M - 1))) = 0)) AND ((((x3((_M - 1))) = 0) AND ((x50((_M - 1))) = 0)) AND ((x53((_M - 1))) = 0))) <=> TRUE) THEN 0 ELSE (IF (((((((((x2((_M - 1))) = 2) AND ((x50((_M - 1))) = 2)) OR (((x2((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) OR (((x53((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x2((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) <=> TRUE) THEN (IF (((((((((x3((_M - 1))) = 2) AND ((x50((_M - 1))) = 2)) OR (((x3((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) OR (((x53((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x3((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) <=> TRUE) THEN (IF ((((x52((_M - 1))) = 2) OR ((x53((_M - 1))) = 2)) <=> TRUE) THEN 2 ELSE (x48((_M - 1))) ENDIF) ELSE (x48((_M - 1))) ENDIF) ELSE (x48((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x83((_M - 1))) = 3) THEN (x107((_M - 1))) ELSE (IF ((x83((_M - 1))) = 4) THEN (IF ((NOT ((((((((x2((_M - 1))) = 2) AND ((x50((_M - 1))) = 2)) OR (((x2((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) OR (((x53((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x2((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x53((_M - 1))) = 2)))) <=> TRUE) THEN (IF ((NOT (((x52((_M - 1))) = 2) OR ((x53((_M - 1))) = 2))) <=> TRUE) THEN (IF ((NOT ((((((((x3((_M - 1))) = 2) AND ((x50((_M - 1))) = 2)) OR (((x3((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) OR (((x53((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x3((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x53((_M - 1))) = 2)))) <=> TRUE) THEN 1 ELSE (x107((_M - 1))) ENDIF) ELSE (x107((_M - 1))) ENDIF) ELSE (x107((_M - 1))) ENDIF) ELSE (x48((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x48((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x48((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN (x48((_M - 1))) ELSE (IF ((x55((_M - 1))) = 4) THEN 0 ELSE (x48((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x48((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x48((_M - 1))) ENDIF) ENDIF));
+DEF__149 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x49(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x49((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x49((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x49((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x49((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x49((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (x49((_M - 1))) ELSE (IF ((x65((_M - 1))) = 7) THEN (x49((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x49((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x63((_M - 1))) = 1) THEN (x49((_M - 1))) ELSE (IF ((x63((_M - 1))) = 2) THEN (x49((_M - 1))) ELSE (IF ((x63((_M - 1))) = 3) THEN (x49((_M - 1))) ELSE (IF ((x63((_M - 1))) = 4) THEN 0 ELSE (x49((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x117((_M - 1))) = 1) THEN (IF (((NOT ((x4((_M - 1))) = 0)) AND (x5((_M - 1)))) <=> TRUE) THEN 1 ELSE (IF ((((x4((_M - 1))) = 0) OR (NOT (x5((_M - 1))))) <=> TRUE) THEN 0 ELSE (x49((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x117((_M - 1))) = 2) THEN (IF ((((x29((_M - 1))) = 6) AND (((x4((_M - 1))) = 0) OR (NOT (x5((_M - 1)))))) <=> TRUE) THEN 0 ELSE (IF ((((((x29((_M - 1))) < 6) AND ((x4((_M - 1))) = 2)) AND (x5((_M - 1)))) AND (NOT (x6((_M - 1))))) <=> TRUE) THEN 2 ELSE (IF (((((x29((_M - 1))) < 6) AND (((x4((_M - 1))) = 0) OR (NOT (x5((_M - 1)))))) OR ((x5((_M - 1))) AND (((x4((_M - 1))) = 1) OR (x6((_M - 1)))))) <=> TRUE) THEN 1 ELSE (x49((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x117((_M - 1))) = 3) THEN (IF ((((NOT ((x4((_M - 1))) = 2)) AND (NOT (x5((_M - 1))))) OR (x6((_M - 1)))) <=> TRUE) THEN 1 ELSE (IF (((((x4((_M - 1))) = 2) AND (x5((_M - 1)))) AND (NOT (x6((_M - 1))))) <=> TRUE) THEN 2 ELSE (x49((_M - 1))) ENDIF) ENDIF) ELSE (x49((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 11) THEN (x49((_M - 1))) ELSE (IF ((x65((_M - 1))) = 12) THEN (IF ((x57((_M - 1))) = 1) THEN (x49((_M - 1))) ELSE (IF ((x57((_M - 1))) = 2) THEN (x49((_M - 1))) ELSE (IF ((x57((_M - 1))) = 3) THEN 0 ELSE (x49((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (x49((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x49((_M - 1))) ENDIF) ENDIF));
+DEF__150 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x50(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x50((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x50((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x50((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x50((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x50((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (IF ((x14((_M - 1))) = 5) THEN (x50((_M - 1))) ELSE (IF ((x14((_M - 1))) = 4) THEN 0 ELSE (x50((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 7) THEN (x50((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x50((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x81((_M - 1))) = 1) THEN (IF (((NOT ((x7((_M - 1))) = 0)) AND (x8((_M - 1)))) <=> TRUE) THEN 1 ELSE (IF ((((x7((_M - 1))) = 0) OR (NOT (x8((_M - 1))))) <=> TRUE) THEN 0 ELSE (x50((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x81((_M - 1))) = 2) THEN (IF ((((x32((_M - 1))) = 6) AND (((x7((_M - 1))) = 0) OR (NOT (x8((_M - 1)))))) <=> TRUE) THEN 0 ELSE (IF ((((((x32((_M - 1))) = 6) AND ((x7((_M - 1))) = 2)) AND (x8((_M - 1)))) AND (NOT (x6((_M - 1))))) <=> TRUE) THEN 2 ELSE (IF (((((x32((_M - 1))) < 6) AND (((x7((_M - 1))) = 0) OR (NOT (x8((_M - 1)))))) OR ((x8((_M - 1))) AND (((x7((_M - 1))) = 1) OR (x6((_M - 1)))))) <=> TRUE) THEN 1 ELSE (x50((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x81((_M - 1))) = 3) THEN (IF (((NOT (((x7((_M - 1))) = 2) AND (x8((_M - 1))))) OR (x6((_M - 1)))) <=> TRUE) THEN 1 ELSE 2 ENDIF) ELSE (x50((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x50((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x50((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN (x50((_M - 1))) ELSE (IF ((x55((_M - 1))) = 4) THEN 0 ELSE (x50((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x50((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x50((_M - 1))) ENDIF) ENDIF));
+DEF__151 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x51(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x51((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x51((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x51((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x51((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x51((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (x51((_M - 1))) ELSE (IF ((x65((_M - 1))) = 7) THEN (x51((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x51((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x63((_M - 1))) = 1) THEN (x51((_M - 1))) ELSE (IF ((x63((_M - 1))) = 2) THEN (x51((_M - 1))) ELSE (IF ((x63((_M - 1))) = 3) THEN (x51((_M - 1))) ELSE (IF ((x63((_M - 1))) = 4) THEN 0 ELSE (x51((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 10) THEN (x27((_M - 1))) ELSE (IF ((x65((_M - 1))) = 11) THEN (x51((_M - 1))) ELSE (IF ((x65((_M - 1))) = 12) THEN (IF ((x57((_M - 1))) = 1) THEN (x51((_M - 1))) ELSE (IF ((x57((_M - 1))) = 2) THEN (x51((_M - 1))) ELSE (IF ((x57((_M - 1))) = 3) THEN 0 ELSE (x51((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (x51((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x51((_M - 1))) ENDIF) ENDIF));
+DEF__152 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x52(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x52((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x52((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x52((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x52((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x52((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (IF ((x14((_M - 1))) = 5) THEN (x52((_M - 1))) ELSE (IF ((x14((_M - 1))) = 4) THEN 0 ELSE (x52((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 7) THEN (x52((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x52((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x80((_M - 1))) = 1) THEN (x79((_M - 1))) ELSE (IF ((x80((_M - 1))) = 2) THEN (IF ((x35((_M - 1))) = 6) THEN 1 ELSE (IF ((x35((_M - 1))) < 6) THEN 2 ELSE (x115((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x80((_M - 1))) = 3) THEN (x115((_M - 1))) ELSE (x79((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x52((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x52((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN (x52((_M - 1))) ELSE (IF ((x55((_M - 1))) = 4) THEN 0 ELSE (x52((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x52((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x52((_M - 1))) ENDIF) ENDIF));
+DEF__153 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x53(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x53((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x53((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x53((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x53((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x53((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (IF ((x14((_M - 1))) = 5) THEN (x53((_M - 1))) ELSE (IF ((x14((_M - 1))) = 4) THEN 0 ELSE (x53((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 7) THEN (x53((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x53((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x84((_M - 1))) = 1) THEN (IF (((NOT (((x9((_M - 1))) = 0) OR ((x10((_M - 1))) = 0))) AND (x5((_M - 1)))) <=> TRUE) THEN 1 ELSE 0 ENDIF) ELSE (IF ((x84((_M - 1))) = 2) THEN (IF ((((x33((_M - 1))) = 6) AND ((((x9((_M - 1))) = 0) OR ((x10((_M - 1))) = 0)) OR (NOT (x5((_M - 1)))))) <=> TRUE) THEN 0 ELSE (IF (((((((x33((_M - 1))) = 6) AND ((x9((_M - 1))) = 2)) AND ((x10((_M - 1))) = 2)) AND (x5((_M - 1)))) AND (NOT (x6((_M - 1))))) <=> TRUE) THEN 2 ELSE (IF (((((x33((_M - 1))) < 6) AND ((((x9((_M - 1))) = 0) OR ((x10((_M - 1))) = 0)) OR (NOT (x5((_M - 1)))))) OR ((x5((_M - 1))) AND (((x6((_M - 1))) OR ((x9((_M - 1))) = 1)) OR ((x10((_M - 1))) = 1)))) <=> TRUE) THEN 1 ELSE (x53((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x84((_M - 1))) = 3) THEN (IF (((((NOT ((x9((_M - 1))) = 2)) AND (NOT ((x10((_M - 1))) = 2))) AND (NOT (x5((_M - 1))))) OR (x6((_M - 1)))) <=> TRUE) THEN 1 ELSE (IF ((((((x9((_M - 1))) = 2) AND ((x10((_M - 1))) = 2)) AND (x5((_M - 1)))) AND (NOT (x6((_M - 1))))) <=> TRUE) THEN 2 ELSE (x53((_M - 1))) ENDIF) ENDIF) ELSE (x53((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x53((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x53((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN (x53((_M - 1))) ELSE (IF ((x55((_M - 1))) = 4) THEN 0 ELSE (x53((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x53((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x53((_M - 1))) ENDIF) ENDIF));
+DEF__154 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x54(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x54((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x54((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x54((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x54((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x54((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (x54((_M - 1))) ELSE (IF ((x65((_M - 1))) = 7) THEN (x54((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x54((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x63((_M - 1))) = 1) THEN (x54((_M - 1))) ELSE (IF ((x63((_M - 1))) = 2) THEN (x54((_M - 1))) ELSE (IF ((x63((_M - 1))) = 3) THEN (x54((_M - 1))) ELSE (IF ((x63((_M - 1))) = 4) THEN 1 ELSE (x54((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x117((_M - 1))) = 1) THEN (IF (((NOT ((x4((_M - 1))) = 0)) AND (x5((_M - 1)))) <=> TRUE) THEN 2 ELSE (IF ((((x4((_M - 1))) = 0) OR (NOT (x5((_M - 1))))) <=> TRUE) THEN 1 ELSE (x117((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x117((_M - 1))) = 2) THEN (IF ((((x29((_M - 1))) = 6) AND (((x4((_M - 1))) = 0) OR (NOT (x5((_M - 1)))))) <=> TRUE) THEN 1 ELSE (IF ((((((x29((_M - 1))) < 6) AND ((x4((_M - 1))) = 2)) AND (x5((_M - 1)))) AND (NOT (x6((_M - 1))))) <=> TRUE) THEN 3 ELSE (IF (((((x29((_M - 1))) < 6) AND (((x4((_M - 1))) = 0) OR (NOT (x5((_M - 1)))))) OR ((x5((_M - 1))) AND (((x4((_M - 1))) = 1) OR (x6((_M - 1)))))) <=> TRUE) THEN 2 ELSE (x117((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x117((_M - 1))) = 3) THEN (IF ((((NOT ((x4((_M - 1))) = 2)) AND (NOT (x5((_M - 1))))) OR (x6((_M - 1)))) <=> TRUE) THEN 2 ELSE (IF (((((x4((_M - 1))) = 2) AND (x5((_M - 1)))) AND (NOT (x6((_M - 1))))) <=> TRUE) THEN 3 ELSE (x117((_M - 1))) ENDIF) ENDIF) ELSE (x117((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 11) THEN (x54((_M - 1))) ELSE (IF ((x65((_M - 1))) = 12) THEN (IF ((x57((_M - 1))) = 1) THEN (x54((_M - 1))) ELSE (IF ((x57((_M - 1))) = 2) THEN (x54((_M - 1))) ELSE (IF ((x57((_M - 1))) = 3) THEN 1 ELSE (x54((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (x54((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x54((_M - 1))) ENDIF) ENDIF));
+DEF__155 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x55(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x55((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x55((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x55((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x55((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x55((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (x55((_M - 1))) ELSE (IF ((x65((_M - 1))) = 7) THEN (x55((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x55((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x63((_M - 1))) = 1) THEN (x55((_M - 1))) ELSE (IF ((x63((_M - 1))) = 2) THEN (x55((_M - 1))) ELSE (IF ((x63((_M - 1))) = 3) THEN (x55((_M - 1))) ELSE (IF ((x63((_M - 1))) = 4) THEN 1 ELSE (x55((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (IF (((((NOT ((x49((_M - 1))) = 0)) AND (NOT ((x49((_M - 1))) = 0))) AND (NOT ((x49((_M - 1))) = 0))) AND ((x27((_M - 1))) < 9)) <=> TRUE) THEN 2 ELSE (IF ((x27((_M - 1))) = 9) THEN 4 ELSE (x55((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x55((_M - 1))) = 2) THEN (IF (((((x49((_M - 1))) = 2) AND (((x49((_M - 1))) = 2) AND ((x49((_M - 1))) = 2))) AND ((x49((_M - 1))) = 2)) <=> TRUE) THEN 3 ELSE (IF ((((((x49((_M - 1))) = 1) AND ((x49((_M - 1))) = 1)) AND ((x49((_M - 1))) = 1)) AND ((x49((_M - 1))) = 1)) <=> TRUE) THEN 5 ELSE (IF ((x27((_M - 1))) = 9) THEN 4 ELSE (IF (((((x49((_M - 1))) = 0) OR ((x49((_M - 1))) = 0)) OR ((x49((_M - 1))) = 0)) <=> TRUE) THEN 4 ELSE (IF ((NOT ((x49((_M - 1))) = 2)) <=> TRUE) THEN 4 ELSE (x55((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (IF ((x55((_M - 1))) = 3) THEN 0 ELSE (IF ((x55((_M - 1))) = 4) THEN 0 ELSE (IF ((x55((_M - 1))) = 5) THEN 4 ELSE (x55((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 11) THEN (x55((_M - 1))) ELSE (IF ((x65((_M - 1))) = 12) THEN (IF ((x57((_M - 1))) = 1) THEN (x55((_M - 1))) ELSE (IF ((x57((_M - 1))) = 2) THEN (x55((_M - 1))) ELSE (IF ((x57((_M - 1))) = 3) THEN 1 ELSE (x55((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (x55((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x55((_M - 1))) ENDIF) ENDIF));
+DEF__156 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x56(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x56((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x56((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x56((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x56((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x56((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (x56((_M - 1))) ELSE (IF ((x65((_M - 1))) = 7) THEN (x56((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x56((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (x56((_M - 1))) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x56((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x56((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN 1 ELSE (x56((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 11) THEN (x56((_M - 1))) ELSE (IF ((x65((_M - 1))) = 12) THEN (IF ((x122((_M - 1))) = 1) THEN 2 ELSE (IF ((x122((_M - 1))) = 2) THEN 3 ELSE (IF ((x122((_M - 1))) = 3) THEN 4 ELSE (IF ((x122((_M - 1))) = 4) THEN 1 ELSE (IF ((x122((_M - 1))) = 5) THEN 1 ELSE (x122((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x56((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x56((_M - 1))) ENDIF) ENDIF));
+DEF__157 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x57(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x57((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x57((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x57((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x57((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x57((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (x57((_M - 1))) ELSE (IF ((x65((_M - 1))) = 7) THEN (x57((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x57((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (x57((_M - 1))) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x57((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x57((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN 1 ELSE (x57((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 11) THEN (x57((_M - 1))) ELSE (IF ((x65((_M - 1))) = 12) THEN (IF ((x57((_M - 1))) = 1) THEN (IF ((x45((_M - 1))) = 1) THEN 2 ELSE (x123((_M - 1))) ENDIF) ELSE (IF ((x57((_M - 1))) = 2) THEN (IF ((x45((_M - 1))) = 3) THEN 4 ELSE (IF ((x45((_M - 1))) = 2) THEN 3 ELSE (x123((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x57((_M - 1))) = 3) THEN 0 ELSE (IF ((x57((_M - 1))) = 4) THEN 0 ELSE (x57((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x57((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x57((_M - 1))) ENDIF) ENDIF));
+DEF__158 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x58(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x58((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x58((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x58((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x58((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x58((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (IF ((x14((_M - 1))) = 5) THEN (x58((_M - 1))) ELSE (IF ((x14((_M - 1))) = 4) THEN 1 ELSE (x58((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 7) THEN (x58((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x58((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x81((_M - 1))) = 1) THEN (IF (((NOT ((x7((_M - 1))) = 0)) AND (x8((_M - 1)))) <=> TRUE) THEN 2 ELSE (IF ((((x7((_M - 1))) = 0) OR (NOT (x8((_M - 1))))) <=> TRUE) THEN 1 ELSE (x81((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x81((_M - 1))) = 2) THEN (IF ((((x32((_M - 1))) = 6) AND (((x7((_M - 1))) = 0) OR (NOT (x8((_M - 1)))))) <=> TRUE) THEN 1 ELSE (IF ((((((x32((_M - 1))) = 6) AND ((x7((_M - 1))) = 2)) AND (x8((_M - 1)))) AND (NOT (x6((_M - 1))))) <=> TRUE) THEN 3 ELSE (IF (((((x32((_M - 1))) < 6) AND (((x7((_M - 1))) = 0) OR (NOT (x8((_M - 1)))))) OR ((x8((_M - 1))) AND (((x7((_M - 1))) = 1) OR (x6((_M - 1)))))) <=> TRUE) THEN 2 ELSE (x81((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x81((_M - 1))) = 3) THEN (IF (((NOT (((x7((_M - 1))) = 2) AND (x8((_M - 1))))) OR (x6((_M - 1)))) <=> TRUE) THEN 2 ELSE 3 ENDIF) ELSE (x81((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x58((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x58((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN (x58((_M - 1))) ELSE (IF ((x55((_M - 1))) = 4) THEN 1 ELSE (x58((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x58((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x58((_M - 1))) ENDIF) ENDIF));
+DEF__159 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x59(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (x59((_M - 1))) ELSE 1 ENDIF) ENDIF));
+DEF__160 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x60(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x60((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x60((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x60((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x60((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x60((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (IF ((x14((_M - 1))) = 5) THEN (x60((_M - 1))) ELSE (IF ((x14((_M - 1))) = 4) THEN 1 ELSE (x60((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 7) THEN (x60((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x60((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x82((_M - 1))) = 1) THEN (x112((_M - 1))) ELSE (IF ((x82((_M - 1))) = 2) THEN (IF ((NOT ((x13((_M - 1))) = 2)) <=> TRUE) THEN 1 ELSE (x112((_M - 1))) ENDIF) ELSE (x82((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x60((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x60((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN (x60((_M - 1))) ELSE (IF ((x55((_M - 1))) = 4) THEN 1 ELSE (x60((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x60((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x60((_M - 1))) ENDIF) ENDIF));
+DEF__161 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x61(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x61((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x61((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x61((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x61((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x61((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (IF ((x14((_M - 1))) = 5) THEN (x61((_M - 1))) ELSE (IF ((x14((_M - 1))) = 4) THEN 1 ELSE (x61((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 7) THEN (x61((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x61((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x83((_M - 1))) = 1) THEN (IF (((NOT ((((x50((_M - 1))) = 0) AND ((x53((_M - 1))) = 0)) AND ((x2((_M - 1))) = 0))) AND (NOT ((((x50((_M - 1))) = 0) AND ((x53((_M - 1))) = 0)) AND ((x3((_M - 1))) = 0)))) <=> TRUE) THEN 2 ELSE (IF ((((((((x50((_M - 1))) = 0) AND ((x50((_M - 1))) = 0)) AND ((x53((_M - 1))) = 0)) AND ((x53((_M - 1))) = 0)) AND ((x2((_M - 1))) = 0)) AND ((x3((_M - 1))) = 0)) <=> TRUE) THEN 1 ELSE (x83((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x83((_M - 1))) = 2) THEN (IF ((((((x2((_M - 1))) = 0) AND ((x50((_M - 1))) = 0)) AND ((x53((_M - 1))) = 0)) AND ((((x3((_M - 1))) = 0) AND ((x50((_M - 1))) = 0)) AND ((x53((_M - 1))) = 0))) <=> TRUE) THEN 1 ELSE (IF (((((((((x2((_M - 1))) = 2) AND ((x50((_M - 1))) = 2)) OR (((x2((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) OR (((x53((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x2((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) <=> TRUE) THEN (IF (((((((((x3((_M - 1))) = 2) AND ((x50((_M - 1))) = 2)) OR (((x3((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) OR (((x53((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x3((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) <=> TRUE) THEN (IF ((((x52((_M - 1))) = 2) OR ((x53((_M - 1))) = 2)) <=> TRUE) THEN 3 ELSE (x83((_M - 1))) ENDIF) ELSE (x83((_M - 1))) ENDIF) ELSE (x83((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x83((_M - 1))) = 3) THEN (x109((_M - 1))) ELSE (IF ((x83((_M - 1))) = 4) THEN (IF ((NOT ((((((((x2((_M - 1))) = 2) AND ((x50((_M - 1))) = 2)) OR (((x2((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) OR (((x53((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x2((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x53((_M - 1))) = 2)))) <=> TRUE) THEN (IF ((NOT (((x52((_M - 1))) = 2) OR ((x53((_M - 1))) = 2))) <=> TRUE) THEN (IF ((NOT ((((((((x3((_M - 1))) = 2) AND ((x50((_M - 1))) = 2)) OR (((x3((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) OR (((x53((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x3((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x53((_M - 1))) = 2)))) <=> TRUE) THEN 2 ELSE (x109((_M - 1))) ENDIF) ELSE (x109((_M - 1))) ENDIF) ELSE (x109((_M - 1))) ENDIF) ELSE (x83((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x61((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x61((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN (x61((_M - 1))) ELSE (IF ((x55((_M - 1))) = 4) THEN 1 ELSE (x61((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x61((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x61((_M - 1))) ENDIF) ENDIF));
+DEF__162 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x62(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x62((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x62((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x62((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x62((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x62((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (IF ((x14((_M - 1))) = 5) THEN (x62((_M - 1))) ELSE (IF ((x14((_M - 1))) = 4) THEN 1 ELSE (x62((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 7) THEN (x62((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x62((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x84((_M - 1))) = 1) THEN (IF (((NOT (((x9((_M - 1))) = 0) OR ((x10((_M - 1))) = 0))) AND (x5((_M - 1)))) <=> TRUE) THEN 2 ELSE 1 ENDIF) ELSE (IF ((x84((_M - 1))) = 2) THEN (IF ((((x33((_M - 1))) = 6) AND ((((x9((_M - 1))) = 0) OR ((x10((_M - 1))) = 0)) OR (NOT (x5((_M - 1)))))) <=> TRUE) THEN 1 ELSE (IF (((((((x33((_M - 1))) = 6) AND ((x9((_M - 1))) = 2)) AND ((x10((_M - 1))) = 2)) AND (x5((_M - 1)))) AND (NOT (x6((_M - 1))))) <=> TRUE) THEN 3 ELSE (IF (((((x33((_M - 1))) < 6) AND ((((x9((_M - 1))) = 0) OR ((x10((_M - 1))) = 0)) OR (NOT (x5((_M - 1)))))) OR ((x5((_M - 1))) AND (((x6((_M - 1))) OR ((x9((_M - 1))) = 1)) OR ((x10((_M - 1))) = 1)))) <=> TRUE) THEN 2 ELSE (x84((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x84((_M - 1))) = 3) THEN (IF (((((NOT ((x9((_M - 1))) = 2)) AND (NOT ((x10((_M - 1))) = 2))) AND (NOT (x5((_M - 1))))) OR (x6((_M - 1)))) <=> TRUE) THEN 2 ELSE (IF ((((((x9((_M - 1))) = 2) AND ((x10((_M - 1))) = 2)) AND (x5((_M - 1)))) AND (NOT (x6((_M - 1))))) <=> TRUE) THEN 3 ELSE (x84((_M - 1))) ENDIF) ENDIF) ELSE (x84((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x62((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x62((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN (x62((_M - 1))) ELSE (IF ((x55((_M - 1))) = 4) THEN 1 ELSE (x62((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x62((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x62((_M - 1))) ENDIF) ENDIF));
+DEF__163 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x63(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x63((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x63((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x63((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x63((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x63((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (IF ((x14((_M - 1))) = 5) THEN (x63((_M - 1))) ELSE (IF ((x14((_M - 1))) = 4) THEN 1 ELSE (x63((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 7) THEN (x63((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x63((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x63((_M - 1))) = 1) THEN (IF ((((((NOT ((x48((_M - 1))) = 0)) AND (NOT ((x47((_M - 1))) = 0))) AND (NOT ((x39((_M - 1))) = 0))) AND (NOT ((x36((_M - 1))) = 0))) AND ((x31((_M - 1))) < 11)) <=> TRUE) THEN 2 ELSE (IF ((x31((_M - 1))) = 11) THEN 5 ELSE (x63((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x63((_M - 1))) = 2) THEN (IF ((((((x48((_M - 1))) = 2) AND ((x47((_M - 1))) = 2)) AND (NOT ((x39((_M - 1))) = 0))) AND ((x36((_M - 1))) = 2)) <=> TRUE) THEN 4 ELSE (IF ((((((x48((_M - 1))) = 1) AND ((x47((_M - 1))) = 1)) AND ((x39((_M - 1))) = 0)) AND ((x36((_M - 1))) = 1)) <=> TRUE) THEN 3 ELSE (IF (((((((x48((_M - 1))) = 0) OR ((x47((_M - 1))) = 0)) OR ((x39((_M - 1))) = 0)) OR ((x36((_M - 1))) = 0)) OR ((x31((_M - 1))) = 11)) <=> TRUE) THEN 5 ELSE (x63((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x63((_M - 1))) = 3) THEN 5 ELSE (IF ((x63((_M - 1))) = 4) THEN 0 ELSE (IF ((x63((_M - 1))) = 5) THEN 0 ELSE (x63((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x63((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x63((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN (x63((_M - 1))) ELSE (IF ((x55((_M - 1))) = 4) THEN 1 ELSE (x63((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x63((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x63((_M - 1))) ENDIF) ENDIF));
+DEF__164 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x64(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x64((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x64((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x64((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x64((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x64((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (IF ((x14((_M - 1))) = 5) THEN (x64((_M - 1))) ELSE (IF ((x14((_M - 1))) = 4) THEN 1 ELSE (x64((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 7) THEN (x64((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x64((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x80((_M - 1))) = 1) THEN (x80((_M - 1))) ELSE (IF ((x80((_M - 1))) = 2) THEN (IF ((x35((_M - 1))) = 6) THEN 3 ELSE (IF ((x35((_M - 1))) < 6) THEN 2 ELSE (x116((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x80((_M - 1))) = 3) THEN (x116((_M - 1))) ELSE (x80((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x64((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x64((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN (x64((_M - 1))) ELSE (IF ((x55((_M - 1))) = 4) THEN 1 ELSE (x64((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x64((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x64((_M - 1))) ENDIF) ENDIF));
+DEF__165 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x65(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (IF ((x14((_M - 1))) = 0) THEN 3 ELSE (x65((_M - 1))) ENDIF) ELSE (IF ((x65((_M - 1))) = 2) THEN (IF ((x14((_M - 1))) = 8) THEN 7 ELSE (IF ((x14((_M - 1))) = 6) THEN 3 ELSE (x65((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 3) THEN (IF ((x14((_M - 1))) = 2) THEN 4 ELSE (x65((_M - 1))) ENDIF) ELSE (IF ((x65((_M - 1))) = 4) THEN (IF ((x14((_M - 1))) = 1) THEN 3 ELSE (IF ((x14((_M - 1))) = 3) THEN 6 ELSE (x65((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 5) THEN (IF ((x14((_M - 1))) = 7) THEN 2 ELSE (x65((_M - 1))) ENDIF) ELSE (IF ((x65((_M - 1))) = 6) THEN (IF ((x14((_M - 1))) = 5) THEN 2 ELSE (IF ((x14((_M - 1))) = 4) THEN 9 ELSE (x65((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 7) THEN (x65((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x65((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (x86((_M - 1))) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x65((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x65((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN 12 ELSE (IF ((x55((_M - 1))) = 4) THEN 9 ELSE (x65((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 11) THEN (IF ((x14((_M - 1))) = 9) THEN 5 ELSE (IF ((x14((_M - 1))) = 10) THEN 8 ELSE (x65((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 12) THEN (IF ((x57((_M - 1))) = 1) THEN (x65((_M - 1))) ELSE (IF ((x57((_M - 1))) = 2) THEN (x65((_M - 1))) ELSE (IF ((x57((_M - 1))) = 3) THEN 10 ELSE (IF ((x57((_M - 1))) = 4) THEN 11 ELSE (x65((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x65((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE 1 ENDIF) ENDIF));
+DEF__166 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x66(_M)) = (IF (_M = _base) THEN FALSE ELSE (x21((_M - 1))) ENDIF));
+DEF__168 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x68(_M)) = (IF (_M = _base) THEN FALSE ELSE (x17((_M - 1))) ENDIF));
+DEF__171 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x71(_M)) = (IF (_M = _base) THEN FALSE ELSE (x22((_M - 1))) ENDIF));
+DEF__173 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x73(_M)) = (IF (_M = _base) THEN FALSE ELSE (x16((_M - 1))) ENDIF));
+% Property(ies)
+
+P : _nat -> BOOLEAN = LAMBDA(_M : _nat): (x129(_M));
+
+
+
+
+% INDUCT : Single property verification.
+% INDUCT :  MAIN.
+% INDUCT :  not refinement_pass.
+% INDUCT :  Checking K = 2. No message received.
+% INDUCT :  setup step loop - initialize step.
+PUSH;
+% INDUCT : ;4b 
+ASSERT (DEF__174( (_n + 0)));
+ASSERT (DEF__176( (_n + 0)));
+ASSERT (DEF__177( (_n + 0)));
+ASSERT (DEF__178( (_n + 0)));
+ASSERT (DEF__179( (_n + 0)));
+ASSERT (DEF__180( (_n + 0)));
+ASSERT (DEF__181( (_n + 0)));
+ASSERT (DEF__182( (_n + 0)));
+ASSERT (DEF__183( (_n + 0)));
+ASSERT (DEF__184( (_n + 0)));
+ASSERT (DEF__185( (_n + 0)));
+ASSERT (DEF__186( (_n + 0)));
+ASSERT (DEF__187( (_n + 0)));
+ASSERT (DEF__188( (_n + 0)));
+ASSERT (DEF__189( (_n + 0)));
+ASSERT (DEF__190( (_n + 0)));
+ASSERT (DEF__191( (_n + 0)));
+ASSERT (DEF__192( (_n + 0)));
+ASSERT (DEF__193( (_n + 0)));
+ASSERT (DEF__194( (_n + 0)));
+ASSERT (DEF__195( (_n + 0)));
+ASSERT (DEF__196( (_n + 0)));
+ASSERT (DEF__197( (_n + 0)));
+ASSERT (DEF__198( (_n + 0)));
+ASSERT (DEF__199( (_n + 0)));
+ASSERT (DEF__200( (_n + 0)));
+ASSERT (DEF__201( (_n + 0)));
+ASSERT (DEF__202( (_n + 0)));
+ASSERT (DEF__115( (_n + 0)));
+ASSERT (DEF__203( (_n + 0)));
+ASSERT (DEF__116( (_n + 0)));
+ASSERT (DEF__204( (_n + 0)));
+ASSERT (DEF__117( (_n + 0)));
+ASSERT (DEF__205( (_n + 0)));
+ASSERT (DEF__206( (_n + 0)));
+ASSERT (DEF__207( (_n + 0)));
+ASSERT (DEF__120( (_n + 0)));
+ASSERT (DEF__208( (_n + 0)));
+ASSERT (DEF__121( (_n + 0)));
+ASSERT (DEF__209( (_n + 0)));
+ASSERT (DEF__122( (_n + 0)));
+ASSERT (DEF__210( (_n + 0)));
+ASSERT (DEF__211( (_n + 0)));
+ASSERT (DEF__212( (_n + 0)));
+ASSERT (DEF__126( (_n + 0)));
+ASSERT (DEF__213( (_n + 0)));
+ASSERT (DEF__127( (_n + 0)));
+ASSERT (DEF__214( (_n + 0)));
+ASSERT (DEF__128( (_n + 0)));
+ASSERT (DEF__215( (_n + 0)));
+ASSERT (DEF__216( (_n + 0)));
+ASSERT (DEF__129( (_n + 0)));
+ASSERT (DEF__217( (_n + 0)));
+ASSERT (DEF__130( (_n + 0)));
+ASSERT (DEF__131( (_n + 0)));
+ASSERT (DEF__218( (_n + 0)));
+ASSERT (DEF__132( (_n + 0)));
+ASSERT (DEF__219( (_n + 0)));
+ASSERT (DEF__133( (_n + 0)));
+ASSERT (DEF__220( (_n + 0)));
+ASSERT (DEF__134( (_n + 0)));
+ASSERT (DEF__221( (_n + 0)));
+ASSERT (DEF__222( (_n + 0)));
+ASSERT (DEF__135( (_n + 0)));
+ASSERT (DEF__223( (_n + 0)));
+ASSERT (DEF__136( (_n + 0)));
+ASSERT (DEF__224( (_n + 0)));
+ASSERT (DEF__137( (_n + 0)));
+ASSERT (DEF__225( (_n + 0)));
+ASSERT (DEF__138( (_n + 0)));
+ASSERT (DEF__226( (_n + 0)));
+ASSERT (DEF__139( (_n + 0)));
+ASSERT (DEF__227( (_n + 0)));
+ASSERT (DEF__140( (_n + 0)));
+ASSERT (DEF__228( (_n + 0)));
+ASSERT (DEF__141( (_n + 0)));
+ASSERT (DEF__229( (_n + 0)));
+ASSERT (DEF__142( (_n + 0)));
+ASSERT (DEF__143( (_n + 0)));
+ASSERT (DEF__144( (_n + 0)));
+ASSERT (DEF__145( (_n + 0)));
+ASSERT (DEF__146( (_n + 0)));
+ASSERT (DEF__147( (_n + 0)));
+ASSERT (DEF__148( (_n + 0)));
+ASSERT (DEF__149( (_n + 0)));
+ASSERT (DEF__150( (_n + 0)));
+ASSERT (DEF__151( (_n + 0)));
+ASSERT (DEF__152( (_n + 0)));
+ASSERT (DEF__153( (_n + 0)));
+ASSERT (DEF__154( (_n + 0)));
+ASSERT (DEF__155( (_n + 0)));
+ASSERT (DEF__156( (_n + 0)));
+ASSERT (DEF__157( (_n + 0)));
+ASSERT (DEF__158( (_n + 0)));
+ASSERT (DEF__159( (_n + 0)));
+ASSERT (DEF__160( (_n + 0)));
+ASSERT (DEF__161( (_n + 0)));
+ASSERT (DEF__162( (_n + 0)));
+ASSERT (DEF__163( (_n + 0)));
+ASSERT (DEF__164( (_n + 0)));
+ASSERT (DEF__165( (_n + 0)));
+ASSERT (DEF__166( (_n + 0)));
+ASSERT (DEF__168( (_n + 0)));
+ASSERT (DEF__171( (_n + 0)));
+ASSERT (DEF__173( (_n + 0)));
+ASSERT (DEF__174( (_n - 1)));
+ASSERT (DEF__176( (_n - 1)));
+ASSERT (DEF__177( (_n - 1)));
+ASSERT (DEF__178( (_n - 1)));
+ASSERT (DEF__179( (_n - 1)));
+ASSERT (DEF__180( (_n - 1)));
+ASSERT (DEF__181( (_n - 1)));
+ASSERT (DEF__182( (_n - 1)));
+ASSERT (DEF__183( (_n - 1)));
+ASSERT (DEF__184( (_n - 1)));
+ASSERT (DEF__185( (_n - 1)));
+ASSERT (DEF__186( (_n - 1)));
+ASSERT (DEF__187( (_n - 1)));
+ASSERT (DEF__188( (_n - 1)));
+ASSERT (DEF__189( (_n - 1)));
+ASSERT (DEF__190( (_n - 1)));
+ASSERT (DEF__191( (_n - 1)));
+ASSERT (DEF__192( (_n - 1)));
+ASSERT (DEF__193( (_n - 1)));
+ASSERT (DEF__194( (_n - 1)));
+ASSERT (DEF__195( (_n - 1)));
+ASSERT (DEF__196( (_n - 1)));
+ASSERT (DEF__197( (_n - 1)));
+ASSERT (DEF__198( (_n - 1)));
+ASSERT (DEF__199( (_n - 1)));
+ASSERT (DEF__200( (_n - 1)));
+ASSERT (DEF__201( (_n - 1)));
+ASSERT (DEF__202( (_n - 1)));
+ASSERT (DEF__115( (_n - 1)));
+ASSERT (DEF__203( (_n - 1)));
+ASSERT (DEF__116( (_n - 1)));
+ASSERT (DEF__204( (_n - 1)));
+ASSERT (DEF__117( (_n - 1)));
+ASSERT (DEF__205( (_n - 1)));
+ASSERT (DEF__206( (_n - 1)));
+ASSERT (DEF__207( (_n - 1)));
+ASSERT (DEF__120( (_n - 1)));
+ASSERT (DEF__208( (_n - 1)));
+ASSERT (DEF__121( (_n - 1)));
+ASSERT (DEF__209( (_n - 1)));
+ASSERT (DEF__122( (_n - 1)));
+ASSERT (DEF__210( (_n - 1)));
+ASSERT (DEF__211( (_n - 1)));
+ASSERT (DEF__212( (_n - 1)));
+ASSERT (DEF__126( (_n - 1)));
+ASSERT (DEF__213( (_n - 1)));
+ASSERT (DEF__127( (_n - 1)));
+ASSERT (DEF__214( (_n - 1)));
+ASSERT (DEF__128( (_n - 1)));
+ASSERT (DEF__215( (_n - 1)));
+ASSERT (DEF__216( (_n - 1)));
+ASSERT (DEF__129( (_n - 1)));
+ASSERT (DEF__217( (_n - 1)));
+ASSERT (DEF__130( (_n - 1)));
+ASSERT (DEF__131( (_n - 1)));
+ASSERT (DEF__218( (_n - 1)));
+ASSERT (DEF__132( (_n - 1)));
+ASSERT (DEF__219( (_n - 1)));
+ASSERT (DEF__133( (_n - 1)));
+ASSERT (DEF__220( (_n - 1)));
+ASSERT (DEF__134( (_n - 1)));
+ASSERT (DEF__221( (_n - 1)));
+ASSERT (DEF__222( (_n - 1)));
+ASSERT (DEF__135( (_n - 1)));
+ASSERT (DEF__223( (_n - 1)));
+ASSERT (DEF__136( (_n - 1)));
+ASSERT (DEF__224( (_n - 1)));
+ASSERT (DEF__137( (_n - 1)));
+ASSERT (DEF__225( (_n - 1)));
+ASSERT (DEF__138( (_n - 1)));
+ASSERT (DEF__226( (_n - 1)));
+ASSERT (DEF__139( (_n - 1)));
+ASSERT (DEF__227( (_n - 1)));
+ASSERT (DEF__140( (_n - 1)));
+ASSERT (DEF__228( (_n - 1)));
+ASSERT (DEF__141( (_n - 1)));
+ASSERT (DEF__229( (_n - 1)));
+ASSERT (DEF__142( (_n - 1)));
+ASSERT (DEF__143( (_n - 1)));
+ASSERT (DEF__144( (_n - 1)));
+ASSERT (DEF__145( (_n - 1)));
+ASSERT (DEF__146( (_n - 1)));
+ASSERT (DEF__147( (_n - 1)));
+ASSERT (DEF__148( (_n - 1)));
+ASSERT (DEF__149( (_n - 1)));
+ASSERT (DEF__150( (_n - 1)));
+ASSERT (DEF__151( (_n - 1)));
+ASSERT (DEF__152( (_n - 1)));
+ASSERT (DEF__153( (_n - 1)));
+ASSERT (DEF__154( (_n - 1)));
+ASSERT (DEF__155( (_n - 1)));
+ASSERT (DEF__156( (_n - 1)));
+ASSERT (DEF__157( (_n - 1)));
+ASSERT (DEF__158( (_n - 1)));
+ASSERT (DEF__159( (_n - 1)));
+ASSERT (DEF__160( (_n - 1)));
+ASSERT (DEF__161( (_n - 1)));
+ASSERT (DEF__162( (_n - 1)));
+ASSERT (DEF__163( (_n - 1)));
+ASSERT (DEF__164( (_n - 1)));
+ASSERT (DEF__165( (_n - 1)));
+ASSERT (DEF__166( (_n - 1)));
+ASSERT (DEF__168( (_n - 1)));
+ASSERT (DEF__171( (_n - 1)));
+ASSERT (DEF__173( (_n - 1)));
+ASSERT (P( (_n - 1)));
+ASSERT (NOT (P( _n)));
+% PUSH; %safe
+ASSERT TRUE;
+CHECKSAT;
+%ECHO "__DONE__";
+% INDUCT : sat
+% INDUCT : __DONE__
+% POP; %safe
+% INDUCT :  Inductive step is Invalid at K = 2. Continuing search.
+POP;
+ASSERT (P( (_n - 1)));
+ASSERT (P( (_n - 2)));
+ASSERT (DEF__174( (_n + 0)));
+ASSERT (DEF__176( (_n + 0)));
+ASSERT (DEF__177( (_n + 0)));
+ASSERT (DEF__178( (_n + 0)));
+ASSERT (DEF__179( (_n + 0)));
+ASSERT (DEF__180( (_n + 0)));
+ASSERT (DEF__181( (_n + 0)));
+ASSERT (DEF__182( (_n + 0)));
+ASSERT (DEF__183( (_n + 0)));
+ASSERT (DEF__184( (_n + 0)));
+ASSERT (DEF__185( (_n + 0)));
+ASSERT (DEF__186( (_n + 0)));
+ASSERT (DEF__187( (_n + 0)));
+ASSERT (DEF__188( (_n + 0)));
+ASSERT (DEF__189( (_n + 0)));
+ASSERT (DEF__190( (_n + 0)));
+ASSERT (DEF__191( (_n + 0)));
+ASSERT (DEF__192( (_n + 0)));
+ASSERT (DEF__193( (_n + 0)));
+ASSERT (DEF__194( (_n + 0)));
+ASSERT (DEF__195( (_n + 0)));
+ASSERT (DEF__196( (_n + 0)));
+ASSERT (DEF__197( (_n + 0)));
+ASSERT (DEF__198( (_n + 0)));
+ASSERT (DEF__199( (_n + 0)));
+ASSERT (DEF__200( (_n + 0)));
+ASSERT (DEF__201( (_n + 0)));
+ASSERT (DEF__202( (_n + 0)));
+ASSERT (DEF__115( (_n + 0)));
+ASSERT (DEF__203( (_n + 0)));
+ASSERT (DEF__116( (_n + 0)));
+ASSERT (DEF__204( (_n + 0)));
+ASSERT (DEF__117( (_n + 0)));
+ASSERT (DEF__205( (_n + 0)));
+ASSERT (DEF__206( (_n + 0)));
+ASSERT (DEF__207( (_n + 0)));
+ASSERT (DEF__120( (_n + 0)));
+ASSERT (DEF__208( (_n + 0)));
+ASSERT (DEF__121( (_n + 0)));
+ASSERT (DEF__209( (_n + 0)));
+ASSERT (DEF__122( (_n + 0)));
+ASSERT (DEF__210( (_n + 0)));
+ASSERT (DEF__211( (_n + 0)));
+ASSERT (DEF__212( (_n + 0)));
+ASSERT (DEF__126( (_n + 0)));
+ASSERT (DEF__213( (_n + 0)));
+ASSERT (DEF__127( (_n + 0)));
+ASSERT (DEF__214( (_n + 0)));
+ASSERT (DEF__128( (_n + 0)));
+ASSERT (DEF__215( (_n + 0)));
+ASSERT (DEF__216( (_n + 0)));
+ASSERT (DEF__129( (_n + 0)));
+ASSERT (DEF__217( (_n + 0)));
+ASSERT (DEF__130( (_n + 0)));
+ASSERT (DEF__131( (_n + 0)));
+ASSERT (DEF__218( (_n + 0)));
+ASSERT (DEF__132( (_n + 0)));
+ASSERT (DEF__219( (_n + 0)));
+ASSERT (DEF__133( (_n + 0)));
+ASSERT (DEF__220( (_n + 0)));
+ASSERT (DEF__134( (_n + 0)));
+ASSERT (DEF__221( (_n + 0)));
+ASSERT (DEF__222( (_n + 0)));
+ASSERT (DEF__135( (_n + 0)));
+ASSERT (DEF__223( (_n + 0)));
+ASSERT (DEF__136( (_n + 0)));
+ASSERT (DEF__224( (_n + 0)));
+ASSERT (DEF__137( (_n + 0)));
+ASSERT (DEF__225( (_n + 0)));
+ASSERT (DEF__138( (_n + 0)));
+ASSERT (DEF__226( (_n + 0)));
+ASSERT (DEF__139( (_n + 0)));
+ASSERT (DEF__227( (_n + 0)));
+ASSERT (DEF__140( (_n + 0)));
+ASSERT (DEF__228( (_n + 0)));
+ASSERT (DEF__141( (_n + 0)));
+ASSERT (DEF__229( (_n + 0)));
+ASSERT (DEF__142( (_n + 0)));
+ASSERT (DEF__143( (_n + 0)));
+ASSERT (DEF__144( (_n + 0)));
+ASSERT (DEF__145( (_n + 0)));
+ASSERT (DEF__146( (_n + 0)));
+ASSERT (DEF__147( (_n + 0)));
+ASSERT (DEF__148( (_n + 0)));
+ASSERT (DEF__149( (_n + 0)));
+ASSERT (DEF__150( (_n + 0)));
+ASSERT (DEF__151( (_n + 0)));
+ASSERT (DEF__152( (_n + 0)));
+ASSERT (DEF__153( (_n + 0)));
+ASSERT (DEF__154( (_n + 0)));
+ASSERT (DEF__155( (_n + 0)));
+ASSERT (DEF__156( (_n + 0)));
+ASSERT (DEF__157( (_n + 0)));
+ASSERT (DEF__158( (_n + 0)));
+ASSERT (DEF__159( (_n + 0)));
+ASSERT (DEF__160( (_n + 0)));
+ASSERT (DEF__161( (_n + 0)));
+ASSERT (DEF__162( (_n + 0)));
+ASSERT (DEF__163( (_n + 0)));
+ASSERT (DEF__164( (_n + 0)));
+ASSERT (DEF__165( (_n + 0)));
+ASSERT (DEF__166( (_n + 0)));
+ASSERT (DEF__168( (_n + 0)));
+ASSERT (DEF__171( (_n + 0)));
+ASSERT (DEF__173( (_n + 0)));
+% INDUCT :  not refinement_pass.
+% INDUCT :  Checking K = 3. No message received.
+% INDUCT :  setup step loop - initialize step.
+PUSH;
+% INDUCT : ;4b 
+ASSERT (DEF__174( (_n - 1)));
+ASSERT (DEF__176( (_n - 1)));
+ASSERT (DEF__177( (_n - 1)));
+ASSERT (DEF__178( (_n - 1)));
+ASSERT (DEF__179( (_n - 1)));
+ASSERT (DEF__180( (_n - 1)));
+ASSERT (DEF__181( (_n - 1)));
+ASSERT (DEF__182( (_n - 1)));
+ASSERT (DEF__183( (_n - 1)));
+ASSERT (DEF__184( (_n - 1)));
+ASSERT (DEF__185( (_n - 1)));
+ASSERT (DEF__186( (_n - 1)));
+ASSERT (DEF__187( (_n - 1)));
+ASSERT (DEF__188( (_n - 1)));
+ASSERT (DEF__189( (_n - 1)));
+ASSERT (DEF__190( (_n - 1)));
+ASSERT (DEF__191( (_n - 1)));
+ASSERT (DEF__192( (_n - 1)));
+ASSERT (DEF__193( (_n - 1)));
+ASSERT (DEF__194( (_n - 1)));
+ASSERT (DEF__195( (_n - 1)));
+ASSERT (DEF__196( (_n - 1)));
+ASSERT (DEF__197( (_n - 1)));
+ASSERT (DEF__198( (_n - 1)));
+ASSERT (DEF__199( (_n - 1)));
+ASSERT (DEF__200( (_n - 1)));
+ASSERT (DEF__201( (_n - 1)));
+ASSERT (DEF__202( (_n - 1)));
+ASSERT (DEF__115( (_n - 1)));
+ASSERT (DEF__203( (_n - 1)));
+ASSERT (DEF__116( (_n - 1)));
+ASSERT (DEF__204( (_n - 1)));
+ASSERT (DEF__117( (_n - 1)));
+ASSERT (DEF__205( (_n - 1)));
+ASSERT (DEF__206( (_n - 1)));
+ASSERT (DEF__207( (_n - 1)));
+ASSERT (DEF__120( (_n - 1)));
+ASSERT (DEF__208( (_n - 1)));
+ASSERT (DEF__121( (_n - 1)));
+ASSERT (DEF__209( (_n - 1)));
+ASSERT (DEF__122( (_n - 1)));
+ASSERT (DEF__210( (_n - 1)));
+ASSERT (DEF__211( (_n - 1)));
+ASSERT (DEF__212( (_n - 1)));
+ASSERT (DEF__126( (_n - 1)));
+ASSERT (DEF__213( (_n - 1)));
+ASSERT (DEF__127( (_n - 1)));
+ASSERT (DEF__214( (_n - 1)));
+ASSERT (DEF__128( (_n - 1)));
+ASSERT (DEF__215( (_n - 1)));
+ASSERT (DEF__216( (_n - 1)));
+ASSERT (DEF__129( (_n - 1)));
+ASSERT (DEF__217( (_n - 1)));
+ASSERT (DEF__130( (_n - 1)));
+ASSERT (DEF__131( (_n - 1)));
+ASSERT (DEF__218( (_n - 1)));
+ASSERT (DEF__132( (_n - 1)));
+ASSERT (DEF__219( (_n - 1)));
+ASSERT (DEF__133( (_n - 1)));
+ASSERT (DEF__220( (_n - 1)));
+ASSERT (DEF__134( (_n - 1)));
+ASSERT (DEF__221( (_n - 1)));
+ASSERT (DEF__222( (_n - 1)));
+ASSERT (DEF__135( (_n - 1)));
+ASSERT (DEF__223( (_n - 1)));
+ASSERT (DEF__136( (_n - 1)));
+ASSERT (DEF__224( (_n - 1)));
+ASSERT (DEF__137( (_n - 1)));
+ASSERT (DEF__225( (_n - 1)));
+ASSERT (DEF__138( (_n - 1)));
+ASSERT (DEF__226( (_n - 1)));
+ASSERT (DEF__139( (_n - 1)));
+ASSERT (DEF__227( (_n - 1)));
+ASSERT (DEF__140( (_n - 1)));
+ASSERT (DEF__228( (_n - 1)));
+ASSERT (DEF__141( (_n - 1)));
+ASSERT (DEF__229( (_n - 1)));
+ASSERT (DEF__142( (_n - 1)));
+ASSERT (DEF__143( (_n - 1)));
+ASSERT (DEF__144( (_n - 1)));
+ASSERT (DEF__145( (_n - 1)));
+ASSERT (DEF__146( (_n - 1)));
+ASSERT (DEF__147( (_n - 1)));
+ASSERT (DEF__148( (_n - 1)));
+ASSERT (DEF__149( (_n - 1)));
+ASSERT (DEF__150( (_n - 1)));
+ASSERT (DEF__151( (_n - 1)));
+ASSERT (DEF__152( (_n - 1)));
+ASSERT (DEF__153( (_n - 1)));
+ASSERT (DEF__154( (_n - 1)));
+ASSERT (DEF__155( (_n - 1)));
+ASSERT (DEF__156( (_n - 1)));
+ASSERT (DEF__157( (_n - 1)));
+ASSERT (DEF__158( (_n - 1)));
+ASSERT (DEF__159( (_n - 1)));
+ASSERT (DEF__160( (_n - 1)));
+ASSERT (DEF__161( (_n - 1)));
+ASSERT (DEF__162( (_n - 1)));
+ASSERT (DEF__163( (_n - 1)));
+ASSERT (DEF__164( (_n - 1)));
+ASSERT (DEF__165( (_n - 1)));
+ASSERT (DEF__166( (_n - 1)));
+ASSERT (DEF__168( (_n - 1)));
+ASSERT (DEF__171( (_n - 1)));
+ASSERT (DEF__173( (_n - 1)));
+ASSERT (DEF__174( (_n - 2)));
+ASSERT (DEF__176( (_n - 2)));
+ASSERT (DEF__177( (_n - 2)));
+ASSERT (DEF__178( (_n - 2)));
+ASSERT (DEF__179( (_n - 2)));
+ASSERT (DEF__180( (_n - 2)));
+ASSERT (DEF__181( (_n - 2)));
+ASSERT (DEF__182( (_n - 2)));
+ASSERT (DEF__183( (_n - 2)));
+ASSERT (DEF__184( (_n - 2)));
+ASSERT (DEF__185( (_n - 2)));
+ASSERT (DEF__186( (_n - 2)));
+ASSERT (DEF__187( (_n - 2)));
+ASSERT (DEF__188( (_n - 2)));
+ASSERT (DEF__189( (_n - 2)));
+ASSERT (DEF__190( (_n - 2)));
+ASSERT (DEF__191( (_n - 2)));
+ASSERT (DEF__192( (_n - 2)));
+ASSERT (DEF__193( (_n - 2)));
+ASSERT (DEF__194( (_n - 2)));
+ASSERT (DEF__195( (_n - 2)));
+ASSERT (DEF__196( (_n - 2)));
+ASSERT (DEF__197( (_n - 2)));
+ASSERT (DEF__198( (_n - 2)));
+ASSERT (DEF__199( (_n - 2)));
+ASSERT (DEF__200( (_n - 2)));
+ASSERT (DEF__201( (_n - 2)));
+ASSERT (DEF__202( (_n - 2)));
+ASSERT (DEF__115( (_n - 2)));
+ASSERT (DEF__203( (_n - 2)));
+ASSERT (DEF__116( (_n - 2)));
+ASSERT (DEF__204( (_n - 2)));
+ASSERT (DEF__117( (_n - 2)));
+ASSERT (DEF__205( (_n - 2)));
+ASSERT (DEF__206( (_n - 2)));
+ASSERT (DEF__207( (_n - 2)));
+ASSERT (DEF__120( (_n - 2)));
+ASSERT (DEF__208( (_n - 2)));
+ASSERT (DEF__121( (_n - 2)));
+ASSERT (DEF__209( (_n - 2)));
+ASSERT (DEF__122( (_n - 2)));
+ASSERT (DEF__210( (_n - 2)));
+ASSERT (DEF__211( (_n - 2)));
+ASSERT (DEF__212( (_n - 2)));
+ASSERT (DEF__126( (_n - 2)));
+ASSERT (DEF__213( (_n - 2)));
+ASSERT (DEF__127( (_n - 2)));
+ASSERT (DEF__214( (_n - 2)));
+ASSERT (DEF__128( (_n - 2)));
+ASSERT (DEF__215( (_n - 2)));
+ASSERT (DEF__216( (_n - 2)));
+ASSERT (DEF__129( (_n - 2)));
+ASSERT (DEF__217( (_n - 2)));
+ASSERT (DEF__130( (_n - 2)));
+ASSERT (DEF__131( (_n - 2)));
+ASSERT (DEF__218( (_n - 2)));
+ASSERT (DEF__132( (_n - 2)));
+ASSERT (DEF__219( (_n - 2)));
+ASSERT (DEF__133( (_n - 2)));
+ASSERT (DEF__220( (_n - 2)));
+ASSERT (DEF__134( (_n - 2)));
+ASSERT (DEF__221( (_n - 2)));
+ASSERT (DEF__222( (_n - 2)));
+ASSERT (DEF__135( (_n - 2)));
+ASSERT (DEF__223( (_n - 2)));
+ASSERT (DEF__136( (_n - 2)));
+ASSERT (DEF__224( (_n - 2)));
+ASSERT (DEF__137( (_n - 2)));
+ASSERT (DEF__225( (_n - 2)));
+ASSERT (DEF__138( (_n - 2)));
+ASSERT (DEF__226( (_n - 2)));
+ASSERT (DEF__139( (_n - 2)));
+ASSERT (DEF__227( (_n - 2)));
+ASSERT (DEF__140( (_n - 2)));
+ASSERT (DEF__228( (_n - 2)));
+ASSERT (DEF__141( (_n - 2)));
+ASSERT (DEF__229( (_n - 2)));
+ASSERT (DEF__142( (_n - 2)));
+ASSERT (DEF__143( (_n - 2)));
+ASSERT (DEF__144( (_n - 2)));
+ASSERT (DEF__145( (_n - 2)));
+ASSERT (DEF__146( (_n - 2)));
+ASSERT (DEF__147( (_n - 2)));
+ASSERT (DEF__148( (_n - 2)));
+ASSERT (DEF__149( (_n - 2)));
+ASSERT (DEF__150( (_n - 2)));
+ASSERT (DEF__151( (_n - 2)));
+ASSERT (DEF__152( (_n - 2)));
+ASSERT (DEF__153( (_n - 2)));
+ASSERT (DEF__154( (_n - 2)));
+ASSERT (DEF__155( (_n - 2)));
+ASSERT (DEF__156( (_n - 2)));
+ASSERT (DEF__157( (_n - 2)));
+ASSERT (DEF__158( (_n - 2)));
+ASSERT (DEF__159( (_n - 2)));
+ASSERT (DEF__160( (_n - 2)));
+ASSERT (DEF__161( (_n - 2)));
+ASSERT (DEF__162( (_n - 2)));
+ASSERT (DEF__163( (_n - 2)));
+ASSERT (DEF__164( (_n - 2)));
+ASSERT (DEF__165( (_n - 2)));
+ASSERT (DEF__166( (_n - 2)));
+ASSERT (DEF__168( (_n - 2)));
+ASSERT (DEF__171( (_n - 2)));
+ASSERT (DEF__173( (_n - 2)));
+ASSERT (NOT (P( _n)));
+% PUSH; %safe
+ASSERT TRUE;
+CHECKSAT;
+%ECHO "__DONE__";
+% INDUCT :  Abort in 3 step.
diff --git a/test/regress/regress0/smt2output.smt2 b/test/regress/regress0/smt2output.smt2
new file mode 100644
index 000000000..26050d931
--- /dev/null
+++ b/test/regress/regress0/smt2output.smt2
@@ -0,0 +1,15 @@
+; This test checks the correct output behavior of SMT-LIBv2 symbols
+; (sometimes they have to be |quoted| with pipes).
+;
+; COMMAND-LINE: -qm
+; EXIT: 10
+(declare-fun |toto| () Bool)
+(declare-fun |to to| () Bool)
+(assert (and toto |to to|))
+(check-sat)
+; EXPECT: sat
+(get-model)
+; EXPECT: (model
+; EXPECT: (define-fun toto () Bool true)
+; EXPECT: (define-fun |to to| () Bool true)
+; EXPECT: )
diff --git a/test/unit/main/interactive_shell_black.h b/test/unit/main/interactive_shell_black.h
index 664027c49..66fcabed0 100644
--- a/test/unit/main/interactive_shell_black.h
+++ b/test/unit/main/interactive_shell_black.h
@@ -69,13 +69,13 @@ private:
   }
 
   void testAssertTrue() {
-    *d_sin << "ASSERT TRUE;" << flush;
+    *d_sin << "ASSERT TRUE;\n" << flush;
     InteractiveShell shell(*d_exprManager, d_options);
     countCommands( shell, 1, 1 );
   }
 
   void testQueryFalse() {
-    *d_sin << "QUERY FALSE;" << flush;
+    *d_sin << "QUERY FALSE;\n" << flush;
     InteractiveShell shell(*d_exprManager, d_options);
     countCommands( shell, 1, 1 );
   }