projects / cvc5.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: 4af9af2)
Refactor pbRewrites preprocessing pass (#1767)
authorAndres Noetzli <andres.noetzli@gmail.com>
Thu, 19 Apr 2018 18:47:38 +0000 (11:47 -0700)
committerGitHub <noreply@github.com>
Thu, 19 Apr 2018 18:47:38 +0000 (11:47 -0700)
This commit refactors the pbRewrites preprocessing pass into the new
style. This commit is essentially just a code move and adds a regression
test for the preprocessing pass. It also makes use of the
AssertionPipeline::replace function to do proper dependency tracking.

src/Makefile.am patch | blob | history
src/preprocessing/passes/pseudo_boolean_processor.cpp [new file with mode: 0644] patch | blob
src/preprocessing/passes/pseudo_boolean_processor.h [new file with mode: 0644] patch | blob
src/preprocessing/preprocessing_pass_context.h patch | blob | history
src/preprocessing/preprocessing_pass_registry.h patch | blob | history
src/smt/smt_engine.cpp patch | blob | history
src/theory/arith/pseudoboolean_proc.cpp [deleted file] patch | blob | history
src/theory/arith/pseudoboolean_proc.h [deleted file] patch | blob | history
test/regress/Makefile.tests patch | blob | history
test/regress/regress1/arith/pbrewrites-test.smt2 [new file with mode: 0644] patch | blob

diff --git a/src/Makefile.am b/src/Makefile.am
index 67e105089d9f56eab840134db00ec283b5bf41f5..f89a8426ec8ed53c2c7b82bc156404982f1e144c 100644 (file)
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -62,10 +62,12 @@ libcvc4_la_SOURCES = \
        decision/decision_strategy.h \
        decision/justification_heuristic.cpp \
        decision/justification_heuristic.h \
-       preprocessing/passes/int_to_bv.cpp \
-       preprocessing/passes/int_to_bv.h \
        preprocessing/passes/bv_gauss.cpp \
        preprocessing/passes/bv_gauss.h \
+       preprocessing/passes/int_to_bv.cpp \
+       preprocessing/passes/int_to_bv.h \
+       preprocessing/passes/pseudo_boolean_processor.cpp \
+       preprocessing/passes/pseudo_boolean_processor.h \
        preprocessing/preprocessing_pass.cpp \
        preprocessing/preprocessing_pass.h \
        preprocessing/preprocessing_pass_context.cpp \
@@ -246,8 +248,6 @@ libcvc4_la_SOURCES = \
        theory/arith/normal_form.h\
        theory/arith/partial_model.cpp \
        theory/arith/partial_model.h \
-       theory/arith/pseudoboolean_proc.cpp \
-       theory/arith/pseudoboolean_proc.h \
        theory/arith/simplex.cpp \
        theory/arith/simplex.h \
        theory/arith/simplex_update.cpp \
diff --git a/src/preprocessing/passes/pseudo_boolean_processor.cpp b/src/preprocessing/passes/pseudo_boolean_processor.cpp
new file mode 100644 (file)
index 0000000..c102bee
--- /dev/null
+++ b/src/preprocessing/passes/pseudo_boolean_processor.cpp
@@ -0,0 +1,418 @@
+/*********************                                                        */
+/*! \file pseudo_boolean_processor.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Tim King, Paul Meng
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "preprocessing/passes/pseudo_boolean_processor.h"
+
+#include "base/output.h"
+#include "theory/arith/arith_utilities.h"
+#include "theory/arith/normal_form.h"
+#include "theory/rewriter.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+using namespace CVC4::theory;
+using namespace CVC4::theory::arith;
+
+PseudoBooleanProcessor::PseudoBooleanProcessor(
+    PreprocessingPassContext* preprocContext)
+    : PreprocessingPass(preprocContext, "pseudo-boolean-processor"),
+      d_pbBounds(preprocContext->getUserContext()),
+      d_subCache(preprocContext->getUserContext()),
+      d_pbs(preprocContext->getUserContext(), 0)
+{
+}
+
+PreprocessingPassResult PseudoBooleanProcessor::applyInternal(
+    AssertionPipeline* assertionsToPreprocess)
+{
+  learn(assertionsToPreprocess->ref());
+  if (likelyToHelp())
+  {
+    applyReplacements(assertionsToPreprocess);
+  }
+
+  return PreprocessingPassResult::NO_CONFLICT;
+}
+
+bool PseudoBooleanProcessor::decomposeAssertion(Node assertion, bool negated)
+{
+  if (assertion.getKind() != kind::GEQ)
+  {
+    return false;
+  }
+  Assert(assertion.getKind() == kind::GEQ);
+
+  Debug("pbs::rewrites") << "decomposeAssertion" << assertion << std::endl;
+
+  Node l = assertion[0];
+  Node r = assertion[1];
+
+  if (r.getKind() != kind::CONST_RATIONAL)
+  {
+    Debug("pbs::rewrites") << "not rhs constant" << assertion << std::endl;
+    return false;
+  }
+  // don't bother matching on anything other than + on the left hand side
+  if (l.getKind() != kind::PLUS)
+  {
+    Debug("pbs::rewrites") << "not plus" << assertion << std::endl;
+    return false;
+  }
+
+  if (!Polynomial::isMember(l))
+  {
+    Debug("pbs::rewrites") << "not polynomial" << assertion << std::endl;
+    return false;
+  }
+
+  Polynomial p = Polynomial::parsePolynomial(l);
+  clear();
+  if (negated)
+  {
+    // (not (>= p r))
+    // (< p r)
+    // (> (-p) (-r))
+    // (>= (-p) (-r +1))
+    d_off = (-r.getConst<Rational>());
+
+    if (d_off.value().isIntegral())
+    {
+      d_off = d_off.value() + Rational(1);
+    }
+    else
+    {
+      d_off = Rational(d_off.value().ceiling());
+    }
+  }
+  else
+  {
+    // (>= p r)
+    d_off = r.getConst<Rational>();
+    d_off = Rational(d_off.value().ceiling());
+  }
+  Assert(d_off.value().isIntegral());
+
+  int adj = negated ? -1 : 1;
+  for (Polynomial::iterator i = p.begin(), end = p.end(); i != end; ++i)
+  {
+    Monomial m = *i;
+    const Rational& coeff = m.getConstant().getValue();
+    if (!(coeff.isOne() || coeff.isNegativeOne()))
+    {
+      return false;
+    }
+    Assert(coeff.sgn() != 0);
+
+    const VarList& vl = m.getVarList();
+    Node v = vl.getNode();
+
+    if (!isPseudoBoolean(v))
+    {
+      return false;
+    }
+    int sgn = adj * coeff.sgn();
+    if (sgn > 0)
+    {
+      d_pos.push_back(v);
+    }
+    else
+    {
+      d_neg.push_back(v);
+    }
+  }
+  // all of the variables are pseudoboolean
+  // with coefficients +/- and the offsetoff
+  return true;
+}
+
+bool PseudoBooleanProcessor::isPseudoBoolean(Node v) const
+{
+  CDNode2PairMap::const_iterator ci = d_pbBounds.find(v);
+  if (ci != d_pbBounds.end())
+  {
+    const std::pair<Node, Node>& p = (*ci).second;
+    return !(p.first).isNull() && !(p.second).isNull();
+  }
+  return false;
+}
+
+void PseudoBooleanProcessor::addGeqZero(Node v, Node exp)
+{
+  Assert(isIntVar(v));
+  Assert(!exp.isNull());
+  CDNode2PairMap::const_iterator ci = d_pbBounds.find(v);
+
+  Debug("pbs::rewrites") << "addGeqZero " << v << std::endl;
+
+  if (ci == d_pbBounds.end())
+  {
+    d_pbBounds.insert(v, std::make_pair(exp, Node::null()));
+  }
+  else
+  {
+    const std::pair<Node, Node>& p = (*ci).second;
+    if (p.first.isNull())
+    {
+      Assert(!p.second.isNull());
+      d_pbBounds.insert(v, std::make_pair(exp, p.second));
+      Debug("pbs::rewrites") << "add pbs " << v << std::endl;
+      Assert(isPseudoBoolean(v));
+      d_pbs = d_pbs + 1;
+    }
+  }
+}
+
+void PseudoBooleanProcessor::addLeqOne(Node v, Node exp)
+{
+  Assert(isIntVar(v));
+  Assert(!exp.isNull());
+  Debug("pbs::rewrites") << "addLeqOne " << v << std::endl;
+  CDNode2PairMap::const_iterator ci = d_pbBounds.find(v);
+  if (ci == d_pbBounds.end())
+  {
+    d_pbBounds.insert(v, std::make_pair(Node::null(), exp));
+  }
+  else
+  {
+    const std::pair<Node, Node>& p = (*ci).second;
+    if (p.second.isNull())
+    {
+      Assert(!p.first.isNull());
+      d_pbBounds.insert(v, std::make_pair(p.first, exp));
+      Debug("pbs::rewrites") << "add pbs " << v << std::endl;
+      Assert(isPseudoBoolean(v));
+      d_pbs = d_pbs + 1;
+    }
+  }
+}
+
+void PseudoBooleanProcessor::learnRewrittenGeq(Node assertion,
+                                               bool negated,
+                                               Node orig)
+{
+  Assert(assertion.getKind() == kind::GEQ);
+  Assert(assertion == Rewriter::rewrite(assertion));
+
+  // assume assertion is rewritten
+  Node l = assertion[0];
+  Node r = assertion[1];
+
+  if (r.getKind() == kind::CONST_RATIONAL)
+  {
+    const Rational& rc = r.getConst<Rational>();
+    if (isIntVar(l))
+    {
+      if (!negated && rc.isZero())
+      {  // (>= x 0)
+        addGeqZero(l, orig);
+      }
+      else if (negated && rc == Rational(2))
+      {
+        addLeqOne(l, orig);
+      }
+    }
+    else if (l.getKind() == kind::MULT && l.getNumChildren() == 2)
+    {
+      Node c = l[0], v = l[1];
+      if (c.getKind() == kind::CONST_RATIONAL
+          && c.getConst<Rational>().isNegativeOne())
+      {
+        if (isIntVar(v))
+        {
+          if (!negated && rc.isNegativeOne())
+          {  // (>= (* -1 x) -1)
+            addLeqOne(v, orig);
+          }
+        }
+      }
+    }
+  }
+
+  if (!negated)
+  {
+    learnGeqSub(assertion);
+  }
+}
+
+void PseudoBooleanProcessor::learnInternal(Node assertion,
+                                           bool negated,
+                                           Node orig)
+{
+  switch (assertion.getKind())
+  {
+    case kind::GEQ:
+    case kind::GT:
+    case kind::LEQ:
+    case kind::LT:
+    {
+      Node rw = Rewriter::rewrite(assertion);
+      if (assertion == rw)
+      {
+        if (assertion.getKind() == kind::GEQ)
+        {
+          learnRewrittenGeq(assertion, negated, orig);
+        }
+      }
+      else
+      {
+        learnInternal(rw, negated, orig);
+      }
+    }
+    break;
+    case kind::NOT: learnInternal(assertion[0], !negated, orig); break;
+    default: break;  // do nothing
+  }
+}
+
+void PseudoBooleanProcessor::learn(Node assertion)
+{
+  if (assertion.getKind() == kind::AND)
+  {
+    Node::iterator ci = assertion.begin(), cend = assertion.end();
+    for (; ci != cend; ++ci)
+    {
+      learn(*ci);
+    }
+  }
+  else
+  {
+    learnInternal(assertion, false, assertion);
+  }
+}
+
+Node PseudoBooleanProcessor::mkGeqOne(Node v)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  return nm->mkNode(kind::GEQ, v, mkRationalNode(Rational(1)));
+}
+
+void PseudoBooleanProcessor::learn(const std::vector<Node>& assertions)
+{
+  std::vector<Node>::const_iterator ci, cend;
+  ci = assertions.begin();
+  cend = assertions.end();
+  for (; ci != cend; ++ci)
+  {
+    learn(*ci);
+  }
+}
+
+void PseudoBooleanProcessor::addSub(Node from, Node to)
+{
+  if (!d_subCache.hasSubstitution(from))
+  {
+    Node rw_to = Rewriter::rewrite(to);
+    d_subCache.addSubstitution(from, rw_to);
+  }
+}
+
+void PseudoBooleanProcessor::learnGeqSub(Node geq)
+{
+  Assert(geq.getKind() == kind::GEQ);
+  const bool negated = false;
+  bool success = decomposeAssertion(geq, negated);
+  if (!success)
+  {
+    Debug("pbs::rewrites") << "failed " << std::endl;
+    return;
+  }
+  Assert(d_off.value().isIntegral());
+  Integer off = d_off.value().ceiling();
+
+  // \sum pos >= \sum neg + off
+
+  // for now special case everything we want
+  // target easy clauses
+  if (d_pos.size() == 1 && d_neg.size() == 1 && off.isZero())
+  {
+    // x >= y
+    // |- (y >= 1) => (x >= 1)
+    Node x = d_pos.front();
+    Node y = d_neg.front();
+
+    Node xGeq1 = mkGeqOne(x);
+    Node yGeq1 = mkGeqOne(y);
+    Node imp = yGeq1.impNode(xGeq1);
+    addSub(geq, imp);
+  }
+  else if (d_pos.size() == 0 && d_neg.size() == 2 && off.isNegativeOne())
+  {
+    // 0 >= (x + y -1)
+    // |- 1 >= x + y
+    // |- (or (not (x >= 1)) (not (y >= 1)))
+    Node x = d_neg[0];
+    Node y = d_neg[1];
+
+    Node xGeq1 = mkGeqOne(x);
+    Node yGeq1 = mkGeqOne(y);
+    Node cases = (xGeq1.notNode()).orNode(yGeq1.notNode());
+    addSub(geq, cases);
+  }
+  else if (d_pos.size() == 2 && d_neg.size() == 1 && off.isZero())
+  {
+    // (x + y) >= z
+    // |- (z >= 1) => (or (x >= 1) (y >=1 ))
+    Node x = d_pos[0];
+    Node y = d_pos[1];
+    Node z = d_neg[0];
+
+    Node xGeq1 = mkGeqOne(x);
+    Node yGeq1 = mkGeqOne(y);
+    Node zGeq1 = mkGeqOne(z);
+    NodeManager* nm = NodeManager::currentNM();
+    Node dis = nm->mkNode(kind::OR, zGeq1.notNode(), xGeq1, yGeq1);
+    addSub(geq, dis);
+  }
+}
+
+Node PseudoBooleanProcessor::applyReplacements(Node pre)
+{
+  Node assertion = Rewriter::rewrite(pre);
+
+  Node result = d_subCache.apply(assertion);
+  if (Debug.isOn("pbs::rewrites") && result != assertion)
+  {
+    Debug("pbs::rewrites") << "applyReplacements" << assertion << "-> "
+                           << result << std::endl;
+  }
+  return result;
+}
+
+bool PseudoBooleanProcessor::likelyToHelp() const { return d_pbs >= 100; }
+
+void PseudoBooleanProcessor::applyReplacements(
+    AssertionPipeline* assertionsToPreprocess)
+{
+  for (size_t i = 0, N = assertionsToPreprocess->size(); i < N; ++i)
+  {
+    assertionsToPreprocess->replace(
+        i, applyReplacements((*assertionsToPreprocess)[i]));
+  }
+}
+
+void PseudoBooleanProcessor::clear()
+{
+  d_off.clear();
+  d_pos.clear();
+  d_neg.clear();
+}
+
+}  // namespace passes
+}  // namespace preprocessing
+}  // namespace CVC4
diff --git a/src/preprocessing/passes/pseudo_boolean_processor.h b/src/preprocessing/passes/pseudo_boolean_processor.h
new file mode 100644 (file)
index 0000000..261470c
--- /dev/null
+++ b/src/preprocessing/passes/pseudo_boolean_processor.h
@@ -0,0 +1,117 @@
+/*********************                                                        */
+/*! \file pseudo_boolean_processor.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Tim King, Paul Meng
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H
+#define __CVC4__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H
+
+#include <unordered_set>
+#include <vector>
+
+#include "context/cdhashmap.h"
+#include "context/cdo.h"
+#include "context/context.h"
+#include "expr/node.h"
+#include "preprocessing/preprocessing_pass.h"
+#include "preprocessing/preprocessing_pass_context.h"
+#include "theory/substitutions.h"
+#include "util/maybe.h"
+#include "util/rational.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+class PseudoBooleanProcessor : public PreprocessingPass
+{
+ public:
+  PseudoBooleanProcessor(PreprocessingPassContext* preprocContext);
+
+ protected:
+  PreprocessingPassResult applyInternal(
+      AssertionPipeline* assertionsToPreprocess) override;
+
+ private:
+  /** Assumes that the assertions have been rewritten. */
+  void learn(const std::vector<Node>& assertions);
+
+  /** Assumes that the assertions have been rewritten. */
+  void applyReplacements(AssertionPipeline* assertionsToPreprocess);
+
+  bool likelyToHelp() const;
+
+  bool isPseudoBoolean(Node v) const;
+
+  // Adds the fact the that integert typed variable v
+  //   must be >= 0 to the context.
+  // This is explained by the explanation exp.
+  // exp cannot be null.
+  void addGeqZero(Node v, Node exp);
+
+  // Adds the fact the that integert typed variable v
+  //   must be <= 1 to the context.
+  // This is explained by the explanation exp.
+  // exp cannot be null.
+  void addLeqOne(Node v, Node exp);
+
+  static inline bool isIntVar(Node v)
+  {
+    return v.isVar() && v.getType().isInteger();
+  }
+
+  void clear();
+
+  /** Assumes that the assertion has been rewritten. */
+  void learn(Node assertion);
+
+  /** Rewrites a node  */
+  Node applyReplacements(Node pre);
+
+  void learnInternal(Node assertion, bool negated, Node orig);
+  void learnRewrittenGeq(Node assertion, bool negated, Node orig);
+
+  void addSub(Node from, Node to);
+  void learnGeqSub(Node geq);
+
+  static Node mkGeqOne(Node v);
+
+  // x ->  <geqZero, leqOne>
+  typedef context::CDHashMap<Node, std::pair<Node, Node>, NodeHashFunction>
+      CDNode2PairMap;
+  CDNode2PairMap d_pbBounds;
+  theory::SubstitutionMap d_subCache;
+
+  typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
+  NodeSet d_learningCache;
+
+  context::CDO<unsigned> d_pbs;
+
+  // decompose into \sum pos >= neg + off
+  Maybe<Rational> d_off;
+  std::vector<Node> d_pos;
+  std::vector<Node> d_neg;
+
+  /** Returns true if successful. */
+  bool decomposeAssertion(Node assertion, bool negated);
+};
+
+}  // namespace passes
+}  // namespace preprocessing
+}  // namespace CVC4
+
+#endif  // __CVC4__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H
diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h
index 2e7a4eaf2e46c5a05350f21042007b3312e523df..66f4d92978dad808aeaea88a95051b3a4738ed2c 100644 (file)
--- a/src/preprocessing/preprocessing_pass_context.h
+++ b/src/preprocessing/preprocessing_pass_context.h
@@ -21,10 +21,9 @@
 #ifndef __CVC4__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H
 #define __CVC4__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H
 
+#include "context/context.h"
 #include "decision/decision_engine.h"
 #include "smt/smt_engine.h"
-#include "theory/arith/pseudoboolean_proc.h"
-#include "theory/booleans/circuit_propagator.h"
 #include "theory/theory_engine.h"
 
 namespace CVC4 {
@@ -37,6 +36,7 @@ class PreprocessingPassContext {
   TheoryEngine* getTheoryEngine() { return d_smt->d_theoryEngine; }
   DecisionEngine* getDecisionEngine() { return d_smt->d_decisionEngine; }
   prop::PropEngine* getPropEngine() { return d_smt->d_propEngine; }
+  context::Context* getUserContext() { return d_smt->d_userContext; }
 
  private:
   /* Pointer to the SmtEngine that this context was created in. */
diff --git a/src/preprocessing/preprocessing_pass_registry.h b/src/preprocessing/preprocessing_pass_registry.h
index 75c66a035b4d844b57c9367c1666d3a90a292d94..37cff676bc7c27b93a4ab778618c7157cccc1125 100644 (file)
--- a/src/preprocessing/preprocessing_pass_registry.h
+++ b/src/preprocessing/preprocessing_pass_registry.h
@@ -24,11 +24,7 @@
 #include <string>
 #include <unordered_map>
 
-#include "decision/decision_engine.h"
 #include "preprocessing/preprocessing_pass.h"
-#include "theory/arith/pseudoboolean_proc.h"
-#include "theory/booleans/circuit_propagator.h"
-#include "theory/theory_engine.h"
 
 namespace CVC4 {
 namespace preprocessing {
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 57cf3ac8c72786465b9132475df02b06abcbb611..65d3697b720b8533c49c36202978b987376150bf 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -68,8 +68,9 @@
 #include "options/strings_options.h"
 #include "options/theory_options.h"
 #include "options/uf_options.h"
-#include "preprocessing/passes/int_to_bv.h"
 #include "preprocessing/passes/bv_gauss.h"
+#include "preprocessing/passes/int_to_bv.h"
+#include "preprocessing/passes/pseudo_boolean_processor.h"
 #include "preprocessing/preprocessing_pass.h"
 #include "preprocessing/preprocessing_pass_context.h"
 #include "preprocessing/preprocessing_pass_registry.h"
@@ -90,7 +91,6 @@
 #include "smt_util/nary_builder.h"
 #include "smt_util/node_visitor.h"
 #include "theory/arith/arith_msum.h"
-#include "theory/arith/pseudoboolean_proc.h"
 #include "theory/booleans/circuit_propagator.h"
 #include "theory/bv/bvintropow2.h"
 #include "theory/bv/theory_bv_rewriter.h"
@@ -571,7 +571,6 @@ public:
  private:
   std::unique_ptr<PreprocessingPassContext> d_preprocessingPassContext;
   PreprocessingPassRegistry d_preprocessingPassRegistry;
-  theory::arith::PseudoBooleanProcessor d_pbsProcessor;
 
   /** The top level substitutions */
   SubstitutionMap d_topLevelSubstitutions;
@@ -597,8 +596,6 @@ public:
   void removeITEs();
 
   Node realToInt(TNode n, NodeToNodeHashMap& cache, std::vector< Node >& var_eq);
-  Node intToBV(TNode n, NodeToNodeHashMap& cache);
-  Node intToBVMakeBinary(TNode n, NodeToNodeHashMap& cache);
   Node purifyNlTerms(TNode n, NodeToNodeHashMap& cache, NodeToNodeHashMap& bcache, std::vector< Node >& var_eq, bool beneathMult = false);
 
   /**
@@ -685,7 +682,6 @@ public:
     d_exprNames(smt.d_userContext),
     d_iteSkolemMap(),
     d_iteRemover(smt.d_userContext),
-    d_pbsProcessor(smt.d_userContext),
     d_topLevelSubstitutions(smt.d_userContext)
   {
     d_smt.d_nodeManager->subscribeEvents(this);
@@ -2552,10 +2548,15 @@ void SmtEnginePrivate::finishInit() {
   d_preprocessingPassContext.reset(new PreprocessingPassContext(&d_smt));
   // TODO: register passes here (this will likely change when we add support for
   // actually assembling preprocessing pipelines).
-  std::unique_ptr<IntToBV> intToBV(new IntToBV(d_preprocessingPassContext.get()));
   std::unique_ptr<BVGauss> bvGauss(new BVGauss(d_preprocessingPassContext.get()));
-  d_preprocessingPassRegistry.registerPass("int-to-bv", std::move(intToBV));
+  std::unique_ptr<IntToBV> intToBV(new IntToBV(d_preprocessingPassContext.get()));
+  std::unique_ptr<PseudoBooleanProcessor> pbProc(
+      new PseudoBooleanProcessor(d_preprocessingPassContext.get()));
+  
   d_preprocessingPassRegistry.registerPass("bv-gauss", std::move(bvGauss));
+  d_preprocessingPassRegistry.registerPass("int-to-bv", std::move(intToBV));
+  d_preprocessingPassRegistry.registerPass("pseudo-boolean-processor",
+                                           std::move(pbProc));
 }
 
 Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map<Node, Node, NodeHashFunction>& cache, bool expandOnly)
@@ -4268,10 +4269,8 @@ void SmtEnginePrivate::processAssertions() {
   }
 
   if( options::pbRewrites() ){
-    d_pbsProcessor.learn(d_assertions.ref());
-    if(d_pbsProcessor.likelyToHelp()){
-      d_pbsProcessor.applyReplacements(d_assertions.ref());
-    }
+    d_preprocessingPassRegistry.getPass("pseudo-boolean-processor")
+        ->apply(&d_assertions);
   }
 
   Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-simplify" << endl;
diff --git a/src/theory/arith/pseudoboolean_proc.cpp b/src/theory/arith/pseudoboolean_proc.cpp
deleted file mode 100644 (file)
index 1cdb90e..0000000
--- a/src/theory/arith/pseudoboolean_proc.cpp
+++ /dev/null
@@ -1,332 +0,0 @@
-/*********************                                                        */
-/*! \file pseudoboolean_proc.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Tim King, Paul Meng
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "theory/arith/pseudoboolean_proc.h"
-
-#include "base/output.h"
-#include "theory/arith/arith_utilities.h"
-#include "theory/arith/normal_form.h"
-#include "theory/rewriter.h"
-
-namespace CVC4 {
-namespace theory {
-namespace arith {
-
-
-PseudoBooleanProcessor::PseudoBooleanProcessor(context::Context* user_context)
-  : d_pbBounds(user_context)
-  , d_subCache(user_context)
-  , d_pbs(user_context, 0)
-{}
-
-bool PseudoBooleanProcessor::decomposeAssertion(Node assertion, bool negated){
-  if (assertion.getKind() != kind::GEQ){ return false; }
-  Assert(assertion.getKind() == kind::GEQ);
-
-  Debug("pbs::rewrites") << "decomposeAssertion" << assertion  << std::endl;
-
-  Node l = assertion[0];
-  Node r = assertion[1];
-
-  if( r.getKind() != kind::CONST_RATIONAL ){
-    Debug("pbs::rewrites") << "not rhs constant" << assertion  << std::endl;
-    return false;
-  }
-  // don't bother matching on anything other than + on the left hand side
-  if( l.getKind() != kind::PLUS){
-    Debug("pbs::rewrites") << "not plus" << assertion  << std::endl;
-    return false;
-  }
-
-  if(!Polynomial::isMember(l)){
-    Debug("pbs::rewrites") << "not polynomial" << assertion  << std::endl;
-    return false;
-  }
-
-  Polynomial p = Polynomial::parsePolynomial(l);
-  clear();
-  if (negated)
-  {
-    // (not (>= p r))
-    // (< p r)
-    // (> (-p) (-r))
-    // (>= (-p) (-r +1))
-    d_off = (-r.getConst<Rational>());
-
-    if (d_off.value().isIntegral())
-    {
-      d_off = d_off.value() + Rational(1);
-    }
-    else
-    {
-      d_off = Rational(d_off.value().ceiling());
-    }
-  }
-  else
-  {
-    // (>= p r)
-    d_off = r.getConst<Rational>();
-    d_off = Rational(d_off.value().ceiling());
-  }
-  Assert(d_off.value().isIntegral());
-
-  int adj = negated ? -1 : 1;
-  for(Polynomial::iterator i=p.begin(), end=p.end(); i != end; ++i){
-    Monomial m = *i;
-    const Rational& coeff = m.getConstant().getValue();
-    if(!(coeff.isOne() || coeff.isNegativeOne())){ return false; }
-    Assert(coeff.sgn() != 0);
-
-    const VarList& vl = m.getVarList();
-    Node v = vl.getNode();
-
-    if(!isPseudoBoolean(v)){ return false; }
-    int sgn = adj * coeff.sgn();
-    if(sgn > 0){
-      d_pos.push_back(v);
-    }else{
-      d_neg.push_back(v);
-    }
-  }
-  // all of the variables are pseudoboolean
-  // with coefficients +/- and the offsetoff
-  return true;
-}
-
-bool PseudoBooleanProcessor::isPseudoBoolean(Node v) const{
-  CDNode2PairMap::const_iterator ci = d_pbBounds.find(v);
-  if(ci != d_pbBounds.end()){
-    const PairNode& p = (*ci).second;
-    return !(p.first).isNull() && !(p.second).isNull();
-  }
-  return false;
-}
-
-void PseudoBooleanProcessor::addGeqZero(Node v, Node exp){
-  Assert(isIntVar(v));
-  Assert(!exp.isNull());
-  CDNode2PairMap::const_iterator ci = d_pbBounds.find(v);
-
-  Debug("pbs::rewrites") << "addGeqZero " << v << std::endl;
-
-  if(ci == d_pbBounds.end()){
-    d_pbBounds.insert(v, std::make_pair(exp, Node::null()));
-  }else{
-    const PairNode& p = (*ci).second;
-    if(p.first.isNull()){
-      Assert(!p.second.isNull());
-      d_pbBounds.insert(v, std::make_pair(exp, p.second));
-      Debug("pbs::rewrites") << "add pbs " << v << std::endl;
-      Assert(isPseudoBoolean(v));
-      d_pbs = d_pbs + 1;
-    }
-  }
-}
-
-void PseudoBooleanProcessor::addLeqOne(Node v, Node exp){
-  Assert(isIntVar(v));
-  Assert(!exp.isNull());
-  Debug("pbs::rewrites") << "addLeqOne " << v << std::endl;
-  CDNode2PairMap::const_iterator ci = d_pbBounds.find(v);
-  if(ci == d_pbBounds.end()){
-    d_pbBounds.insert(v, std::make_pair(Node::null(), exp));
-  }else{
-    const PairNode& p = (*ci).second;
-    if(p.second.isNull()){
-      Assert(!p.first.isNull());
-      d_pbBounds.insert(v, std::make_pair(p.first, exp));
-      Debug("pbs::rewrites") << "add pbs " << v << std::endl;
-      Assert(isPseudoBoolean(v));
-      d_pbs = d_pbs + 1;
-    }
-  }
-}
-
-void PseudoBooleanProcessor::learnRewrittenGeq(Node assertion, bool negated, Node orig){
-  Assert(assertion.getKind() == kind::GEQ);
-  Assert(assertion == Rewriter::rewrite(assertion));
-
-  // assume assertion is rewritten
-  Node l = assertion[0];
-  Node r = assertion[1];
-
-
-  if(r.getKind() == kind::CONST_RATIONAL){
-    const Rational& rc = r.getConst<Rational>();
-    if(isIntVar(l)){
-      if(!negated && rc.isZero()){  // (>= x 0)
-       addGeqZero(l, orig);
-      }else if(negated && rc == Rational(2)){
-       addLeqOne(l, orig);
-      }
-    }else if(l.getKind() == kind::MULT && l.getNumChildren() == 2){
-      Node c = l[0], v = l[1];
-      if(c.getKind() == kind::CONST_RATIONAL && c.getConst<Rational>().isNegativeOne()){
-       if(isIntVar(v)){
-         if(!negated && rc.isNegativeOne()){ // (>= (* -1 x) -1)
-           addLeqOne(v, orig);
-         }
-       }
-      }
-    }
-  }
-
-  if(!negated){
-    learnGeqSub(assertion);
-  }
-}
-
-void PseudoBooleanProcessor::learnInternal(Node assertion, bool negated, Node orig){
-  switch(assertion.getKind()){
-  case kind::GEQ:
-  case kind::GT:
-  case kind::LEQ:
-  case kind::LT:
-    {
-      Node rw = Rewriter::rewrite(assertion);
-      if(assertion == rw){
-       if(assertion.getKind() == kind::GEQ){
-         learnRewrittenGeq(assertion, negated, orig);
-       }
-      }else{
-       learnInternal(rw, negated, orig);
-      }
-    }
-    break;
-  case kind::NOT:
-    learnInternal(assertion[0], !negated, orig);
-    break;
-  default:
-    break; // do nothing
-  }
-}
-
-void PseudoBooleanProcessor::learn(Node assertion){
-  if(assertion.getKind() == kind::AND){
-    Node::iterator ci=assertion.begin(), cend = assertion.end();
-    for(; ci != cend; ++ci){
-      learn(*ci);
-    }
-  }else{
-    learnInternal(assertion, false, assertion);
-  }
-}
-
-Node PseudoBooleanProcessor::mkGeqOne(Node v){
-  NodeManager* nm = NodeManager::currentNM();
-  return nm->mkNode(kind::GEQ, v, mkRationalNode(Rational(1)));
-}
-
-void PseudoBooleanProcessor::learn(const NodeVec& assertions){
-  NodeVec::const_iterator ci, cend;
-  ci = assertions.begin(); cend=assertions.end();
-  for(; ci != cend; ++ci ){
-    learn(*ci);
-  }
-}
-
-void PseudoBooleanProcessor::addSub(Node from, Node to){
-  if(!d_subCache.hasSubstitution(from)){
-    Node rw_to = Rewriter::rewrite(to);
-    d_subCache.addSubstitution(from, rw_to);
-  }
-}
-
-void PseudoBooleanProcessor::learnGeqSub(Node geq){
-  Assert(geq.getKind() == kind::GEQ);
-  const bool negated = false;
-  bool success = decomposeAssertion(geq, negated);
-  if(!success){
-    Debug("pbs::rewrites") << "failed " << std::endl;
-    return;
-  }
-  Assert(d_off.value().isIntegral());
-  Integer off = d_off.value().ceiling();
-
-  // \sum pos >= \sum neg + off
-
-  // for now special case everything we want
-  // target easy clauses
-  if( d_pos.size() == 1 && d_neg.size() == 1 && off.isZero() ){
-    // x >= y
-    // |- (y >= 1) => (x >= 1)
-    Node x = d_pos.front();
-    Node y = d_neg.front();
-
-    Node xGeq1 = mkGeqOne(x);
-    Node yGeq1 = mkGeqOne(y);
-    Node imp = yGeq1.impNode(xGeq1);
-    addSub(geq, imp);
-  }else if( d_pos.size() == 0 && d_neg.size() == 2 && off.isNegativeOne()){
-    // 0 >= (x + y -1)
-    // |- 1 >= x + y
-    // |- (or (not (x >= 1)) (not (y >= 1)))
-    Node x = d_neg[0];
-    Node y = d_neg[1];
-
-    Node xGeq1 = mkGeqOne(x);
-    Node yGeq1 = mkGeqOne(y);
-    Node cases = (xGeq1.notNode()).orNode(yGeq1.notNode());
-    addSub(geq, cases);
-  }else if( d_pos.size() == 2 && d_neg.size() == 1 && off.isZero() ){
-    // (x + y) >= z
-    // |- (z >= 1) => (or (x >= 1) (y >=1 ))
-    Node x = d_pos[0];
-    Node y = d_pos[1];
-    Node z = d_neg[0];
-
-    Node xGeq1 = mkGeqOne(x);
-    Node yGeq1 = mkGeqOne(y);
-    Node zGeq1 = mkGeqOne(z);
-    NodeManager* nm =NodeManager::currentNM();
-    Node dis = nm->mkNode(kind::OR, zGeq1.notNode(), xGeq1, yGeq1);
-    addSub(geq, dis);
-  }
-}
-
-Node PseudoBooleanProcessor::applyReplacements(Node pre){
-  Node assertion = Rewriter::rewrite(pre);
-
-  Node result = d_subCache.apply(assertion);
-  if(Debug.isOn("pbs::rewrites") && result != assertion ){
-    Debug("pbs::rewrites") << "applyReplacements" <<assertion << "-> " << result << std::endl;
-  }
-  return result;
-}
-
-bool PseudoBooleanProcessor::likelyToHelp() const{
-  return d_pbs >= 100;
-}
-
-void PseudoBooleanProcessor::applyReplacements(NodeVec& assertions){
-  for(size_t i=0, N=assertions.size(); i < N; ++i){
-    Node assertion = assertions[i];
-    Node res = applyReplacements(assertion);
-    assertions[i] = res;
-  }
-}
-
-void PseudoBooleanProcessor::clear() {
-  d_off.clear();
-  d_pos.clear();
-  d_neg.clear();
-}
-
-
-}/* CVC4::theory::arith namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
diff --git a/src/theory/arith/pseudoboolean_proc.h b/src/theory/arith/pseudoboolean_proc.h
deleted file mode 100644 (file)
index 0b91ed0..0000000
--- a/src/theory/arith/pseudoboolean_proc.h
+++ /dev/null
@@ -1,108 +0,0 @@
-/*********************                                                        */
-/*! \file pseudoboolean_proc.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Tim King, Paul Meng
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "cvc4_private.h"
-
-#pragma once
-
-#include <unordered_set>
-#include <vector>
-
-#include "context/cdhashmap.h"
-#include "context/cdo.h"
-#include "context/context.h"
-#include "expr/node.h"
-#include "theory/substitutions.h"
-#include "util/maybe.h"
-#include "util/rational.h"
-
-namespace CVC4 {
-namespace theory {
-namespace arith {
-
-class PseudoBooleanProcessor {
-private:
-  // x ->  <geqZero, leqOne>
-  typedef std::pair<Node, Node> PairNode;
-  typedef std::vector<Node> NodeVec;
-  typedef context::CDHashMap<Node, PairNode, NodeHashFunction> CDNode2PairMap;
-  CDNode2PairMap d_pbBounds;
-  SubstitutionMap d_subCache;
-
-  typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
-  NodeSet d_learningCache;
-
-  context::CDO<unsigned> d_pbs;
-
-  // decompose into \sum pos >= neg + off
-  Maybe<Rational> d_off;
-  NodeVec d_pos;
-  NodeVec d_neg;
-  void clear();
-  /** Returns true if successful. */
-  bool decomposeAssertion(Node assertion, bool negated);
-
-public:
-  PseudoBooleanProcessor(context::Context* user_context);
-
-  /** Assumes that the assertions have been rewritten. */
-  void learn(const NodeVec& assertions);
-
-  /** Assumes that the assertions have been rewritten. */
-  void applyReplacements(NodeVec& assertions);
-
-  bool likelyToHelp() const;
-
-  bool isPseudoBoolean(Node v) const;
-
-  // Adds the fact the that integert typed variable v
-  //   must be >= 0 to the context.
-  // This is explained by the explanation exp.
-  // exp cannot be null.
-  void addGeqZero(Node v, Node exp);
-
-
-  // Adds the fact the that integert typed variable v
-  //   must be <= 1 to the context.
-  // This is explained by the explanation exp.
-  // exp cannot be null.
-  void addLeqOne(Node v, Node exp);
-
-  static inline bool isIntVar(Node v){
-    return v.isVar() && v.getType().isInteger();
-  }
-
-private:
-  /** Assumes that the assertion has been rewritten. */
-  void learn(Node assertion);
-
-  /** Rewrites a node  */
-  Node applyReplacements(Node assertion);
-
-  void learnInternal(Node assertion, bool negated, Node orig);
-  void learnRewrittenGeq(Node assertion, bool negated, Node orig);
-
-  void addSub(Node from, Node to);
-  void learnGeqSub(Node geq);
-
-  static Node mkGeqOne(Node v);
-};
-
-
-}/* CVC4::theory::arith namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index f41a3a15f5de394e26a60c83c9d8db2d357aa3df..56965f2723b628cd35801deed2408be32029590d 100644 (file)
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -989,6 +989,7 @@ REG1_TESTS = \
        regress1/arith/mod.02.smt2 \
        regress1/arith/mod.03.smt2 \
        regress1/arith/mult.02.smt2 \
+       regress1/arith/pbrewrites-test.smt2 \
        regress1/arith/problem__003.smt2 \
        regress1/arrayinuf_error.smt2 \
        regress1/aufbv/bug580.smt2 \
@@ -1038,6 +1039,7 @@ REG1_TESTS = \
        regress1/errorcrash.smt2 \
        regress1/fmf-fun-dbu.smt2 \
        regress1/fmf/ALG008-1.smt2 \
+       regress1/fmf/Hoare-z3.931718.smt \
        regress1/fmf/LeftistHeap.scala-8-ncm.smt2 \
        regress1/fmf/PUZ001+1.smt2 \
        regress1/fmf/agree466.smt2 \
@@ -1065,7 +1067,6 @@ REG1_TESTS = \
        regress1/fmf/fore19-exp2-core.smt2 \
        regress1/fmf/german169.smt2 \
        regress1/fmf/german73.smt2 \
-       regress1/fmf/Hoare-z3.931718.smt \
        regress1/fmf/issue916-fmf-or.smt2 \
        regress1/fmf/jasmin-cdt-crash.smt2 \
        regress1/fmf/ko-bound-set.cvc \
diff --git a/test/regress/regress1/arith/pbrewrites-test.smt2 b/test/regress/regress1/arith/pbrewrites-test.smt2
new file mode 100644 (file)
index 0000000..1f38f15
--- /dev/null
+++ b/test/regress/regress1/arith/pbrewrites-test.smt2
@@ -0,0 +1,2937 @@
+; COMMAND-LINE: --pb-rewrites
+; EXPECT: sat
+(set-info :smt-lib-version 2.6)
+(set-logic QF_LIA)
+(set-info :category "industrial")
+(declare-fun x0 () Int)
+(declare-fun x1 () Int)
+(declare-fun x2 () Int)
+(declare-fun x3 () Int)
+(declare-fun x4 () Int)
+(declare-fun x5 () Int)
+(declare-fun x6 () Int)
+(declare-fun x7 () Int)
+(declare-fun x8 () Int)
+(declare-fun x9 () Int)
+(declare-fun x10 () Int)
+(declare-fun x11 () Int)
+(declare-fun x12 () Int)
+(declare-fun x13 () Int)
+(declare-fun x14 () Int)
+(declare-fun x15 () Int)
+(declare-fun x16 () Int)
+(declare-fun x17 () Int)
+(declare-fun x18 () Int)
+(declare-fun x19 () Int)
+(declare-fun x20 () Int)
+(declare-fun x21 () Int)
+(declare-fun x22 () Int)
+(declare-fun x23 () Int)
+(declare-fun x24 () Int)
+(declare-fun x25 () Int)
+(declare-fun x26 () Int)
+(declare-fun x27 () Int)
+(declare-fun x28 () Int)
+(declare-fun x29 () Int)
+(declare-fun x30 () Int)
+(declare-fun x31 () Int)
+(declare-fun x32 () Int)
+(declare-fun x33 () Int)
+(declare-fun x34 () Int)
+(declare-fun x35 () Int)
+(declare-fun x36 () Int)
+(declare-fun x37 () Int)
+(declare-fun x38 () Int)
+(declare-fun x39 () Int)
+(declare-fun x40 () Int)
+(declare-fun x41 () Int)
+(declare-fun x42 () Int)
+(declare-fun x43 () Int)
+(declare-fun x44 () Int)
+(declare-fun x45 () Int)
+(declare-fun x46 () Int)
+(declare-fun x47 () Int)
+(declare-fun x48 () Int)
+(declare-fun x49 () Int)
+(declare-fun x50 () Int)
+(declare-fun x51 () Int)
+(declare-fun x52 () Int)
+(declare-fun x53 () Int)
+(declare-fun x54 () Int)
+(declare-fun x55 () Int)
+(declare-fun x56 () Int)
+(declare-fun x57 () Int)
+(declare-fun x58 () Int)
+(declare-fun x59 () Int)
+(declare-fun x60 () Int)
+(declare-fun x61 () Int)
+(declare-fun x62 () Int)
+(declare-fun x63 () Int)
+(declare-fun x64 () Int)
+(declare-fun x65 () Int)
+(declare-fun x66 () Int)
+(declare-fun x67 () Int)
+(declare-fun x68 () Int)
+(declare-fun x69 () Int)
+(declare-fun x70 () Int)
+(declare-fun x71 () Int)
+(declare-fun x72 () Int)
+(declare-fun x73 () Int)
+(declare-fun x74 () Int)
+(declare-fun x75 () Int)
+(declare-fun x76 () Int)
+(declare-fun x77 () Int)
+(declare-fun x78 () Int)
+(declare-fun x79 () Int)
+(declare-fun x80 () Int)
+(declare-fun x81 () Int)
+(declare-fun x82 () Int)
+(declare-fun x83 () Int)
+(declare-fun x84 () Int)
+(declare-fun x85 () Int)
+(declare-fun x86 () Int)
+(declare-fun x87 () Int)
+(declare-fun x88 () Int)
+(declare-fun x89 () Int)
+(declare-fun x90 () Int)
+(declare-fun x91 () Int)
+(declare-fun x92 () Int)
+(declare-fun x93 () Int)
+(declare-fun x94 () Int)
+(declare-fun x95 () Int)
+(declare-fun x96 () Int)
+(declare-fun x97 () Int)
+(declare-fun x98 () Int)
+(declare-fun x99 () Int)
+(declare-fun x100 () Int)
+(declare-fun x101 () Int)
+(declare-fun x102 () Int)
+(declare-fun x103 () Int)
+(declare-fun x104 () Int)
+(declare-fun x105 () Int)
+(declare-fun x106 () Int)
+(declare-fun x107 () Int)
+(declare-fun x108 () Int)
+(declare-fun x109 () Int)
+(declare-fun x110 () Int)
+(declare-fun x111 () Int)
+(declare-fun x112 () Int)
+(declare-fun x113 () Int)
+(declare-fun x114 () Int)
+(declare-fun x115 () Int)
+(declare-fun x116 () Int)
+(declare-fun x117 () Int)
+(declare-fun x118 () Int)
+(declare-fun x119 () Int)
+(declare-fun x120 () Int)
+(declare-fun x121 () Int)
+(declare-fun x122 () Int)
+(declare-fun x123 () Int)
+(declare-fun x124 () Int)
+(declare-fun x125 () Int)
+(declare-fun x126 () Int)
+(declare-fun x127 () Int)
+(declare-fun x128 () Int)
+(declare-fun x129 () Int)
+(declare-fun x130 () Int)
+(declare-fun x131 () Int)
+(declare-fun x132 () Int)
+(declare-fun x133 () Int)
+(declare-fun x134 () Int)
+(declare-fun x135 () Int)
+(declare-fun x136 () Int)
+(declare-fun x137 () Int)
+(declare-fun x138 () Int)
+(declare-fun x139 () Int)
+(declare-fun x140 () Int)
+(declare-fun x141 () Int)
+(declare-fun x142 () Int)
+(declare-fun x143 () Int)
+(declare-fun x144 () Int)
+(declare-fun x145 () Int)
+(declare-fun x146 () Int)
+(declare-fun x147 () Int)
+(declare-fun x148 () Int)
+(declare-fun x149 () Int)
+(declare-fun x150 () Int)
+(declare-fun x151 () Int)
+(declare-fun x152 () Int)
+(declare-fun x153 () Int)
+(declare-fun x154 () Int)
+(declare-fun x155 () Int)
+(declare-fun x156 () Int)
+(declare-fun x157 () Int)
+(declare-fun x158 () Int)
+(declare-fun x159 () Int)
+(declare-fun x160 () Int)
+(declare-fun x161 () Int)
+(declare-fun x162 () Int)
+(declare-fun x163 () Int)
+(declare-fun x164 () Int)
+(declare-fun x165 () Int)
+(declare-fun x166 () Int)
+(declare-fun x167 () Int)
+(declare-fun x168 () Int)
+(declare-fun x169 () Int)
+(declare-fun x170 () Int)
+(declare-fun x171 () Int)
+(declare-fun x172 () Int)
+(declare-fun x173 () Int)
+(declare-fun x174 () Int)
+(declare-fun x175 () Int)
+(declare-fun x176 () Int)
+(declare-fun x177 () Int)
+(declare-fun x178 () Int)
+(declare-fun x179 () Int)
+(declare-fun x180 () Int)
+(declare-fun x181 () Int)
+(declare-fun x182 () Int)
+(declare-fun x183 () Int)
+(declare-fun x184 () Int)
+(declare-fun x185 () Int)
+(declare-fun x186 () Int)
+(declare-fun x187 () Int)
+(declare-fun x188 () Int)
+(declare-fun x189 () Int)
+(declare-fun x190 () Int)
+(declare-fun x191 () Int)
+(declare-fun x192 () Int)
+(declare-fun x193 () Int)
+(declare-fun x194 () Int)
+(declare-fun x195 () Int)
+(declare-fun x196 () Int)
+(declare-fun x197 () Int)
+(declare-fun x198 () Int)
+(declare-fun x199 () Int)
+(declare-fun x200 () Int)
+(declare-fun x201 () Int)
+(declare-fun x202 () Int)
+(declare-fun x203 () Int)
+(declare-fun x204 () Int)
+(declare-fun x205 () Int)
+(declare-fun x206 () Int)
+(declare-fun x207 () Int)
+(declare-fun x208 () Int)
+(declare-fun x209 () Int)
+(declare-fun x210 () Int)
+(declare-fun x211 () Int)
+(declare-fun x212 () Int)
+(declare-fun x213 () Int)
+(declare-fun x214 () Int)
+(declare-fun x215 () Int)
+(declare-fun x216 () Int)
+(declare-fun x217 () Int)
+(declare-fun x218 () Int)
+(declare-fun x219 () Int)
+(declare-fun x220 () Int)
+(declare-fun x221 () Int)
+(declare-fun x222 () Int)
+(declare-fun x223 () Int)
+(declare-fun x224 () Int)
+(declare-fun x225 () Int)
+(declare-fun x226 () Int)
+(declare-fun x227 () Int)
+(declare-fun x228 () Int)
+(declare-fun x229 () Int)
+(declare-fun x230 () Int)
+(declare-fun x231 () Int)
+(declare-fun x232 () Int)
+(declare-fun x233 () Int)
+(declare-fun x234 () Int)
+(declare-fun x235 () Int)
+(declare-fun x236 () Int)
+(declare-fun x237 () Int)
+(declare-fun x238 () Int)
+(declare-fun x239 () Int)
+(declare-fun x240 () Int)
+(declare-fun x241 () Int)
+(declare-fun x242 () Int)
+(declare-fun x243 () Int)
+(declare-fun x244 () Int)
+(declare-fun x245 () Int)
+(declare-fun x246 () Int)
+(declare-fun x247 () Int)
+(declare-fun x248 () Int)
+(declare-fun x249 () Int)
+(declare-fun x250 () Int)
+(declare-fun x251 () Int)
+(declare-fun x252 () Int)
+(declare-fun x253 () Int)
+(declare-fun x254 () Int)
+(declare-fun x255 () Int)
+(declare-fun x256 () Int)
+(declare-fun x257 () Int)
+(declare-fun x258 () Int)
+(declare-fun x259 () Int)
+(declare-fun x260 () Int)
+(declare-fun x261 () Int)
+(declare-fun x262 () Int)
+(declare-fun x263 () Int)
+(declare-fun x264 () Int)
+(declare-fun x265 () Int)
+(declare-fun x266 () Int)
+(declare-fun x267 () Int)
+(declare-fun x268 () Int)
+(declare-fun x269 () Int)
+(declare-fun x270 () Int)
+(declare-fun x271 () Int)
+(declare-fun x272 () Int)
+(declare-fun x273 () Int)
+(declare-fun x274 () Int)
+(declare-fun x275 () Int)
+(declare-fun x276 () Int)
+(declare-fun x277 () Int)
+(declare-fun x278 () Int)
+(declare-fun x279 () Int)
+(declare-fun x280 () Int)
+(declare-fun x281 () Int)
+(declare-fun x282 () Int)
+(declare-fun x283 () Int)
+(declare-fun x284 () Int)
+(declare-fun x285 () Int)
+(declare-fun x286 () Int)
+(declare-fun x287 () Int)
+(declare-fun x288 () Int)
+(declare-fun x289 () Int)
+(declare-fun x290 () Int)
+(declare-fun x291 () Int)
+(declare-fun x292 () Int)
+(declare-fun x293 () Int)
+(declare-fun x294 () Int)
+(declare-fun x295 () Int)
+(declare-fun x296 () Int)
+(declare-fun x297 () Int)
+(declare-fun x298 () Int)
+(declare-fun x299 () Int)
+(declare-fun x300 () Int)
+(declare-fun x301 () Int)
+(declare-fun x302 () Int)
+(declare-fun x303 () Int)
+(declare-fun x304 () Int)
+(declare-fun x305 () Int)
+(declare-fun x306 () Int)
+(declare-fun x307 () Int)
+(declare-fun x308 () Int)
+(declare-fun x309 () Int)
+(declare-fun x310 () Int)
+(declare-fun x311 () Int)
+(declare-fun x312 () Int)
+(declare-fun x313 () Int)
+(declare-fun x314 () Int)
+(declare-fun x315 () Int)
+(declare-fun x316 () Int)
+(declare-fun x317 () Int)
+(declare-fun x318 () Int)
+(declare-fun x319 () Int)
+(declare-fun x320 () Int)
+(declare-fun x321 () Int)
+(declare-fun x322 () Int)
+(declare-fun x323 () Int)
+(declare-fun x324 () Int)
+(declare-fun x325 () Int)
+(declare-fun x326 () Int)
+(declare-fun x327 () Int)
+(declare-fun x328 () Int)
+(declare-fun x329 () Int)
+(declare-fun x330 () Int)
+(declare-fun x331 () Int)
+(declare-fun x332 () Int)
+(declare-fun x333 () Int)
+(declare-fun x334 () Int)
+(declare-fun x335 () Int)
+(declare-fun x336 () Int)
+(declare-fun x337 () Int)
+(declare-fun x338 () Int)
+(declare-fun x339 () Int)
+(declare-fun x340 () Int)
+(declare-fun x341 () Int)
+(declare-fun x342 () Int)
+(declare-fun x343 () Int)
+(declare-fun x344 () Int)
+(declare-fun x345 () Int)
+(declare-fun x346 () Int)
+(declare-fun x347 () Int)
+(declare-fun x348 () Int)
+(declare-fun x349 () Int)
+(declare-fun x350 () Int)
+(declare-fun x351 () Int)
+(declare-fun x352 () Int)
+(declare-fun x353 () Int)
+(declare-fun x354 () Int)
+(declare-fun x355 () Int)
+(declare-fun x356 () Int)
+(declare-fun x357 () Int)
+(declare-fun x358 () Int)
+(declare-fun x359 () Int)
+(declare-fun x360 () Int)
+(declare-fun x361 () Int)
+(declare-fun x362 () Int)
+(declare-fun x363 () Int)
+(declare-fun x364 () Int)
+(declare-fun x365 () Int)
+(declare-fun x366 () Int)
+(declare-fun x367 () Int)
+(declare-fun x368 () Int)
+(declare-fun x369 () Int)
+(declare-fun x370 () Int)
+(declare-fun x371 () Int)
+(declare-fun x372 () Int)
+(declare-fun x373 () Int)
+(declare-fun x374 () Int)
+(declare-fun x375 () Int)
+(declare-fun x376 () Int)
+(declare-fun x377 () Int)
+(declare-fun x378 () Int)
+(declare-fun x379 () Int)
+(declare-fun x380 () Int)
+(declare-fun x381 () Int)
+(declare-fun x382 () Int)
+(declare-fun x383 () Int)
+(declare-fun x384 () Int)
+(declare-fun x385 () Int)
+(declare-fun x386 () Int)
+(declare-fun x387 () Int)
+(declare-fun x388 () Int)
+(declare-fun x389 () Int)
+(declare-fun x390 () Int)
+(declare-fun x391 () Int)
+(declare-fun x392 () Int)
+(declare-fun x393 () Int)
+(declare-fun x394 () Int)
+(declare-fun x395 () Int)
+(declare-fun x396 () Int)
+(declare-fun x397 () Int)
+(declare-fun x398 () Int)
+(declare-fun x399 () Int)
+(declare-fun x400 () Int)
+(declare-fun x401 () Int)
+(declare-fun x402 () Int)
+(declare-fun x403 () Int)
+(declare-fun x404 () Int)
+(declare-fun x405 () Int)
+(declare-fun x406 () Int)
+(declare-fun x407 () Int)
+(declare-fun x408 () Int)
+(declare-fun x409 () Int)
+(declare-fun x410 () Int)
+(declare-fun x411 () Int)
+(declare-fun x412 () Int)
+(declare-fun x413 () Int)
+(declare-fun x414 () Int)
+(declare-fun x415 () Int)
+(declare-fun x416 () Int)
+(declare-fun x417 () Int)
+(declare-fun x418 () Int)
+(declare-fun x419 () Int)
+(declare-fun x420 () Int)
+(declare-fun x421 () Int)
+(declare-fun x422 () Int)
+(declare-fun x423 () Int)
+(declare-fun x424 () Int)
+(declare-fun x425 () Int)
+(declare-fun x426 () Int)
+(declare-fun x427 () Int)
+(declare-fun x428 () Int)
+(declare-fun x429 () Int)
+(declare-fun x430 () Int)
+(declare-fun x431 () Int)
+(declare-fun x432 () Int)
+(declare-fun x433 () Int)
+(declare-fun x434 () Int)
+(declare-fun x435 () Int)
+(declare-fun x436 () Int)
+(declare-fun x437 () Int)
+(declare-fun x438 () Int)
+(declare-fun x439 () Int)
+(declare-fun x440 () Int)
+(declare-fun x441 () Int)
+(declare-fun x442 () Int)
+(declare-fun x443 () Int)
+(declare-fun x444 () Int)
+(declare-fun x445 () Int)
+(declare-fun x446 () Int)
+(declare-fun x447 () Int)
+(declare-fun x448 () Int)
+(declare-fun x449 () Int)
+(declare-fun x450 () Int)
+(declare-fun x451 () Int)
+(declare-fun x452 () Int)
+(declare-fun x453 () Int)
+(declare-fun x454 () Int)
+(declare-fun x455 () Int)
+(declare-fun x456 () Int)
+(declare-fun x457 () Int)
+(declare-fun x458 () Int)
+(declare-fun x459 () Int)
+(declare-fun x460 () Int)
+(declare-fun x461 () Int)
+(declare-fun x462 () Int)
+(declare-fun x463 () Int)
+(declare-fun x464 () Int)
+(declare-fun x465 () Int)
+(declare-fun x466 () Int)
+(declare-fun x467 () Int)
+(declare-fun x468 () Int)
+(declare-fun x469 () Int)
+(declare-fun x470 () Int)
+(declare-fun x471 () Int)
+(declare-fun x472 () Int)
+(declare-fun x473 () Int)
+(declare-fun x474 () Int)
+(declare-fun x475 () Int)
+(declare-fun x476 () Int)
+(declare-fun x477 () Int)
+(declare-fun x478 () Int)
+(declare-fun x479 () Int)
+(declare-fun x480 () Int)
+(declare-fun x481 () Int)
+(declare-fun x482 () Int)
+(declare-fun x483 () Int)
+(declare-fun x484 () Int)
+(declare-fun x485 () Int)
+(declare-fun x486 () Int)
+(declare-fun x487 () Int)
+(declare-fun x488 () Int)
+(declare-fun x489 () Int)
+(declare-fun x490 () Int)
+(declare-fun x491 () Int)
+(declare-fun x492 () Int)
+(declare-fun x493 () Int)
+(declare-fun x494 () Int)
+(declare-fun x495 () Int)
+(declare-fun x496 () Int)
+(declare-fun x497 () Int)
+(declare-fun x498 () Int)
+(declare-fun x499 () Int)
+(declare-fun x500 () Int)
+(declare-fun x501 () Int)
+(declare-fun x502 () Int)
+(declare-fun x503 () Int)
+(declare-fun x504 () Int)
+(declare-fun x505 () Int)
+(declare-fun x506 () Int)
+(declare-fun x507 () Int)
+(declare-fun x508 () Int)
+(declare-fun x509 () Int)
+(declare-fun x510 () Int)
+(declare-fun x511 () Int)
+(declare-fun x512 () Int)
+(declare-fun x513 () Int)
+(declare-fun x514 () Int)
+(declare-fun x515 () Int)
+(declare-fun x516 () Int)
+(declare-fun x517 () Int)
+(declare-fun x518 () Int)
+(declare-fun x519 () Int)
+(declare-fun x520 () Int)
+(declare-fun x521 () Int)
+(declare-fun x522 () Int)
+(declare-fun x523 () Int)
+(declare-fun x524 () Int)
+(declare-fun x525 () Int)
+(declare-fun x526 () Int)
+(declare-fun x527 () Int)
+(declare-fun x528 () Int)
+(declare-fun x529 () Int)
+(declare-fun x530 () Int)
+(declare-fun x531 () Int)
+(declare-fun x532 () Int)
+(declare-fun x533 () Int)
+(declare-fun x534 () Int)
+(declare-fun x535 () Int)
+(declare-fun x536 () Int)
+(declare-fun x537 () Int)
+(declare-fun x538 () Int)
+(declare-fun x539 () Int)
+(declare-fun x540 () Int)
+(declare-fun x541 () Int)
+(declare-fun x542 () Int)
+(declare-fun x543 () Int)
+(declare-fun x544 () Int)
+(declare-fun x545 () Int)
+(declare-fun x546 () Int)
+(declare-fun x547 () Int)
+(declare-fun x548 () Int)
+(declare-fun x549 () Int)
+(declare-fun x550 () Int)
+(declare-fun x551 () Int)
+(declare-fun x552 () Int)
+(declare-fun x553 () Int)
+(declare-fun x554 () Int)
+(declare-fun x555 () Int)
+(declare-fun x556 () Int)
+(declare-fun x557 () Int)
+(declare-fun x558 () Int)
+(declare-fun x559 () Int)
+(declare-fun x560 () Int)
+(declare-fun x561 () Int)
+(declare-fun x562 () Int)
+(declare-fun x563 () Int)
+(declare-fun x564 () Int)
+(declare-fun x565 () Int)
+(declare-fun x566 () Int)
+(declare-fun x567 () Int)
+(declare-fun x568 () Int)
+(declare-fun x569 () Int)
+(declare-fun x570 () Int)
+(declare-fun x571 () Int)
+(declare-fun x572 () Int)
+(declare-fun x573 () Int)
+(declare-fun x574 () Int)
+(declare-fun x575 () Int)
+(declare-fun x576 () Int)
+(declare-fun x577 () Int)
+(declare-fun x578 () Int)
+(declare-fun x579 () Int)
+(declare-fun x580 () Int)
+(declare-fun x581 () Int)
+(declare-fun x582 () Int)
+(declare-fun x583 () Int)
+(declare-fun x584 () Int)
+(declare-fun x585 () Int)
+(declare-fun x586 () Int)
+(declare-fun x587 () Int)
+(declare-fun x588 () Int)
+(declare-fun x589 () Int)
+(declare-fun x590 () Int)
+(declare-fun x591 () Int)
+(declare-fun x592 () Int)
+(declare-fun x593 () Int)
+(declare-fun x594 () Int)
+(declare-fun x595 () Int)
+(declare-fun x596 () Int)
+(declare-fun x597 () Int)
+(declare-fun x598 () Int)
+(declare-fun x599 () Int)
+(declare-fun x600 () Int)
+(declare-fun x601 () Int)
+(declare-fun x602 () Int)
+(declare-fun x603 () Int)
+(declare-fun x604 () Int)
+(declare-fun x605 () Int)
+(declare-fun x606 () Int)
+(declare-fun x607 () Int)
+(declare-fun x608 () Int)
+(declare-fun x609 () Int)
+(declare-fun x610 () Int)
+(declare-fun x611 () Int)
+(declare-fun x612 () Int)
+(declare-fun x613 () Int)
+(declare-fun x614 () Int)
+(declare-fun x615 () Int)
+(declare-fun x616 () Int)
+(declare-fun x617 () Int)
+(declare-fun x618 () Int)
+(declare-fun x619 () Int)
+(declare-fun x620 () Int)
+(declare-fun x621 () Int)
+(declare-fun x622 () Int)
+(declare-fun x623 () Int)
+(declare-fun x624 () Int)
+(declare-fun x625 () Int)
+(declare-fun x626 () Int)
+(declare-fun x627 () Int)
+(declare-fun x628 () Int)
+(declare-fun x629 () Int)
+(declare-fun x630 () Int)
+(declare-fun x631 () Int)
+(declare-fun x632 () Int)
+(declare-fun x633 () Int)
+(declare-fun x634 () Int)
+(declare-fun x635 () Int)
+(declare-fun x636 () Int)
+(declare-fun x637 () Int)
+(declare-fun x638 () Int)
+(declare-fun x639 () Int)
+(declare-fun x640 () Int)
+(declare-fun x641 () Int)
+(declare-fun x642 () Int)
+(declare-fun x643 () Int)
+(declare-fun x644 () Int)
+(declare-fun x645 () Int)
+(declare-fun x646 () Int)
+(declare-fun x647 () Int)
+(declare-fun x648 () Int)
+(declare-fun x649 () Int)
+(declare-fun x650 () Int)
+(declare-fun x651 () Int)
+(declare-fun x652 () Int)
+(declare-fun x653 () Int)
+(declare-fun x654 () Int)
+(declare-fun x655 () Int)
+(declare-fun x656 () Int)
+(declare-fun x657 () Int)
+(declare-fun x658 () Int)
+(declare-fun x659 () Int)
+(declare-fun x660 () Int)
+(declare-fun x661 () Int)
+(declare-fun x662 () Int)
+(declare-fun x663 () Int)
+(declare-fun x664 () Int)
+(declare-fun x665 () Int)
+(declare-fun x666 () Int)
+(declare-fun x667 () Int)
+(declare-fun x668 () Int)
+(declare-fun x669 () Int)
+(declare-fun x670 () Int)
+(declare-fun x671 () Int)
+(declare-fun x672 () Int)
+(declare-fun x673 () Int)
+(declare-fun x674 () Int)
+(declare-fun x675 () Int)
+(declare-fun x676 () Int)
+(declare-fun x677 () Int)
+(declare-fun x678 () Int)
+(declare-fun x679 () Int)
+(declare-fun x680 () Int)
+(declare-fun x681 () Int)
+(declare-fun x682 () Int)
+(declare-fun x683 () Int)
+(declare-fun x684 () Int)
+(declare-fun x685 () Int)
+(declare-fun x686 () Int)
+(declare-fun x687 () Int)
+(declare-fun x688 () Int)
+(declare-fun x689 () Int)
+(declare-fun x690 () Int)
+(declare-fun x691 () Int)
+(declare-fun x692 () Int)
+(declare-fun x693 () Int)
+(declare-fun x694 () Int)
+(declare-fun x695 () Int)
+(declare-fun x696 () Int)
+(declare-fun x697 () Int)
+(declare-fun x698 () Int)
+(declare-fun x699 () Int)
+(declare-fun x700 () Int)
+(declare-fun x701 () Int)
+(declare-fun x702 () Int)
+(declare-fun x703 () Int)
+(declare-fun x704 () Int)
+(declare-fun x705 () Int)
+(declare-fun x706 () Int)
+(declare-fun x707 () Int)
+(declare-fun x708 () Int)
+(declare-fun x709 () Int)
+(declare-fun x710 () Int)
+(declare-fun x711 () Int)
+(declare-fun x712 () Int)
+(declare-fun x713 () Int)
+(declare-fun x714 () Int)
+(declare-fun x715 () Int)
+(declare-fun x716 () Int)
+(declare-fun x717 () Int)
+(declare-fun x718 () Int)
+(declare-fun x719 () Int)
+(declare-fun x720 () Int)
+(declare-fun x721 () Int)
+(declare-fun x722 () Int)
+(declare-fun x723 () Int)
+(declare-fun x724 () Int)
+(declare-fun x725 () Int)
+(declare-fun x726 () Int)
+(declare-fun x727 () Int)
+(declare-fun x728 () Int)
+(declare-fun x729 () Int)
+(declare-fun x730 () Int)
+(declare-fun x731 () Int)
+(declare-fun x732 () Int)
+(declare-fun x733 () Int)
+(declare-fun x734 () Int)
+(declare-fun x735 () Int)
+(declare-fun x736 () Int)
+(declare-fun x737 () Int)
+(declare-fun x738 () Int)
+(declare-fun x739 () Int)
+(declare-fun x740 () Int)
+(declare-fun x741 () Int)
+(declare-fun x742 () Int)
+(declare-fun x743 () Int)
+(declare-fun x744 () Int)
+(declare-fun x745 () Int)
+(declare-fun x746 () Int)
+(declare-fun x747 () Int)
+(declare-fun x748 () Int)
+(declare-fun x749 () Int)
+(declare-fun x750 () Int)
+(declare-fun x751 () Int)
+(declare-fun x752 () Int)
+(declare-fun x753 () Int)
+(declare-fun x754 () Int)
+(declare-fun x755 () Int)
+(declare-fun x756 () Int)
+(declare-fun x757 () Int)
+(declare-fun x758 () Int)
+(declare-fun x759 () Int)
+(declare-fun x760 () Int)
+(declare-fun x761 () Int)
+(declare-fun x762 () Int)
+(declare-fun x763 () Int)
+(declare-fun x764 () Int)
+(declare-fun x765 () Int)
+(declare-fun x766 () Int)
+(declare-fun x767 () Int)
+(declare-fun x768 () Int)
+(declare-fun x769 () Int)
+(declare-fun x770 () Int)
+(declare-fun x771 () Int)
+(declare-fun x772 () Int)
+(declare-fun x773 () Int)
+(declare-fun x774 () Int)
+(declare-fun x775 () Int)
+(declare-fun x776 () Int)
+(declare-fun x777 () Int)
+(declare-fun x778 () Int)
+(declare-fun x779 () Int)
+(declare-fun x780 () Int)
+(declare-fun x781 () Int)
+(declare-fun x782 () Int)
+(declare-fun x783 () Int)
+(declare-fun x784 () Int)
+(declare-fun x785 () Int)
+(declare-fun x786 () Int)
+(declare-fun x787 () Int)
+(declare-fun x788 () Int)
+(declare-fun x789 () Int)
+(declare-fun x790 () Int)
+(declare-fun x791 () Int)
+(declare-fun x792 () Int)
+(declare-fun x793 () Int)
+(declare-fun x794 () Int)
+(declare-fun x795 () Int)
+(declare-fun x796 () Int)
+(declare-fun x797 () Int)
+(declare-fun x798 () Int)
+(declare-fun x799 () Int)
+(declare-fun x800 () Int)
+(declare-fun x801 () Int)
+(declare-fun x802 () Int)
+(declare-fun x803 () Int)
+(declare-fun x804 () Int)
+(declare-fun x805 () Int)
+(declare-fun x806 () Int)
+(declare-fun x807 () Int)
+(declare-fun x808 () Int)
+(declare-fun x809 () Int)
+(declare-fun x810 () Int)
+(declare-fun x811 () Int)
+(declare-fun x812 () Int)
+(declare-fun x813 () Int)
+(declare-fun x814 () Int)
+(declare-fun x815 () Int)
+(declare-fun x816 () Int)
+(declare-fun x817 () Int)
+(declare-fun x818 () Int)
+(declare-fun x819 () Int)
+(declare-fun x820 () Int)
+(declare-fun x821 () Int)
+(declare-fun x822 () Int)
+(declare-fun x823 () Int)
+(declare-fun x824 () Int)
+(declare-fun x825 () Int)
+(declare-fun x826 () Int)
+(declare-fun x827 () Int)
+(declare-fun x828 () Int)
+(declare-fun x829 () Int)
+(declare-fun x830 () Int)
+(declare-fun x831 () Int)
+(declare-fun x832 () Int)
+(declare-fun x833 () Int)
+(declare-fun x834 () Int)
+(declare-fun x835 () Int)
+(declare-fun x836 () Int)
+(declare-fun x837 () Int)
+(declare-fun x838 () Int)
+(declare-fun x839 () Int)
+(declare-fun x840 () Int)
+(declare-fun x841 () Int)
+(declare-fun x842 () Int)
+(declare-fun x843 () Int)
+(declare-fun x844 () Int)
+(declare-fun x845 () Int)
+(declare-fun x846 () Int)
+(declare-fun x847 () Int)
+(declare-fun x848 () Int)
+(declare-fun x849 () Int)
+(declare-fun x850 () Int)
+(declare-fun x851 () Int)
+(declare-fun x852 () Int)
+(declare-fun x853 () Int)
+(declare-fun x854 () Int)
+(declare-fun x855 () Int)
+(declare-fun x856 () Int)
+(declare-fun x857 () Int)
+(declare-fun x858 () Int)
+(declare-fun x859 () Int)
+(declare-fun x860 () Int)
+(declare-fun x861 () Int)
+(declare-fun x862 () Int)
+(declare-fun x863 () Int)
+(declare-fun x864 () Int)
+(declare-fun x865 () Int)
+(declare-fun x866 () Int)
+(declare-fun x867 () Int)
+(declare-fun x868 () Int)
+(declare-fun x869 () Int)
+(declare-fun x870 () Int)
+(declare-fun x871 () Int)
+(declare-fun x872 () Int)
+(declare-fun x873 () Int)
+(declare-fun x874 () Int)
+(declare-fun x875 () Int)
+(declare-fun x876 () Int)
+(declare-fun x877 () Int)
+(declare-fun x878 () Int)
+(declare-fun x879 () Int)
+(declare-fun x880 () Int)
+(declare-fun x881 () Int)
+(declare-fun x882 () Int)
+(declare-fun x883 () Int)
+(declare-fun x884 () Int)
+(declare-fun x885 () Int)
+(declare-fun x886 () Int)
+(declare-fun x887 () Int)
+(declare-fun x888 () Int)
+(declare-fun x889 () Int)
+(declare-fun x890 () Int)
+(declare-fun x891 () Int)
+(declare-fun x892 () Int)
+(declare-fun x893 () Int)
+(declare-fun x894 () Int)
+(declare-fun x895 () Int)
+(declare-fun x896 () Int)
+(declare-fun x897 () Int)
+(declare-fun x898 () Int)
+(declare-fun x899 () Int)
+(declare-fun x900 () Int)
+(declare-fun x901 () Int)
+(declare-fun x902 () Int)
+(declare-fun x903 () Int)
+(declare-fun x904 () Int)
+(declare-fun x905 () Int)
+(declare-fun x906 () Int)
+(declare-fun x907 () Int)
+(declare-fun x908 () Int)
+(declare-fun x909 () Int)
+(declare-fun x910 () Int)
+(declare-fun x911 () Int)
+(declare-fun x912 () Int)
+(declare-fun x913 () Int)
+(declare-fun x914 () Int)
+(declare-fun x915 () Int)
+(declare-fun x916 () Int)
+(declare-fun x917 () Int)
+(declare-fun x918 () Int)
+(declare-fun x919 () Int)
+(declare-fun x920 () Int)
+(declare-fun x921 () Int)
+(declare-fun x922 () Int)
+(declare-fun x923 () Int)
+(declare-fun x924 () Int)
+(declare-fun x925 () Int)
+(declare-fun x926 () Int)
+(declare-fun x927 () Int)
+(declare-fun x928 () Int)
+(declare-fun x929 () Int)
+(declare-fun x930 () Int)
+(declare-fun x931 () Int)
+(declare-fun x932 () Int)
+(declare-fun x933 () Int)
+(declare-fun x934 () Int)
+(declare-fun x935 () Int)
+(declare-fun x936 () Int)
+(declare-fun x937 () Int)
+(declare-fun x938 () Int)
+(declare-fun x939 () Int)
+(declare-fun x940 () Int)
+(declare-fun x941 () Int)
+(declare-fun x942 () Int)
+(declare-fun x943 () Int)
+(declare-fun x944 () Int)
+(declare-fun x945 () Int)
+(declare-fun x946 () Int)
+(declare-fun x947 () Int)
+(declare-fun x948 () Int)
+(declare-fun x949 () Int)
+(declare-fun x950 () Int)
+(declare-fun x951 () Int)
+(declare-fun x952 () Int)
+(declare-fun x953 () Int)
+(declare-fun x954 () Int)
+(declare-fun x955 () Int)
+(declare-fun x956 () Int)
+(declare-fun x957 () Int)
+(declare-fun x958 () Int)
+(declare-fun x959 () Int)
+(declare-fun x960 () Int)
+(declare-fun x961 () Int)
+(declare-fun x962 () Int)
+(declare-fun x963 () Int)
+(declare-fun x964 () Int)
+(declare-fun x965 () Int)
+(declare-fun x966 () Int)
+(declare-fun x967 () Int)
+(declare-fun x968 () Int)
+(declare-fun x969 () Int)
+(declare-fun x970 () Int)
+(declare-fun x971 () Int)
+(declare-fun x972 () Int)
+(declare-fun x973 () Int)
+(declare-fun x974 () Int)
+(declare-fun x975 () Int)
+(declare-fun x976 () Int)
+(declare-fun x977 () Int)
+(declare-fun x978 () Int)
+(declare-fun x979 () Int)
+(declare-fun x980 () Int)
+(declare-fun x981 () Int)
+(declare-fun x982 () Int)
+(declare-fun x983 () Int)
+(declare-fun x984 () Int)
+(declare-fun x985 () Int)
+(declare-fun x986 () Int)
+(declare-fun x987 () Int)
+(declare-fun x988 () Int)
+(declare-fun x989 () Int)
+(declare-fun x990 () Int)
+(declare-fun x991 () Int)
+(declare-fun x992 () Int)
+(declare-fun x993 () Int)
+(declare-fun x994 () Int)
+(declare-fun x995 () Int)
+(declare-fun x996 () Int)
+(declare-fun x997 () Int)
+(declare-fun x998 () Int)
+(declare-fun x999 () Int)
+(declare-fun x1000 () Int)
+(declare-fun x1001 () Int)
+(declare-fun x1002 () Int)
+(declare-fun x1003 () Int)
+(declare-fun x1004 () Int)
+(declare-fun x1005 () Int)
+(declare-fun x1006 () Int)
+(declare-fun x1007 () Int)
+(declare-fun x1008 () Int)
+(declare-fun x1009 () Int)
+(declare-fun x1010 () Int)
+(declare-fun x1011 () Int)
+(declare-fun x1012 () Int)
+(declare-fun x1013 () Int)
+(declare-fun x1014 () Int)
+(declare-fun x1015 () Int)
+(declare-fun x1016 () Int)
+(declare-fun x1017 () Int)
+(declare-fun x1018 () Int)
+(declare-fun x1019 () Int)
+(declare-fun x1020 () Int)
+(declare-fun x1021 () Int)
+(declare-fun x1022 () Int)
+(declare-fun x1023 () Int)
+(declare-fun x1024 () Int)
+(declare-fun x1025 () Int)
+(declare-fun x1026 () Int)
+(declare-fun x1027 () Int)
+(declare-fun x1028 () Int)
+(declare-fun x1029 () Int)
+(declare-fun x1030 () Int)
+(declare-fun x1031 () Int)
+(declare-fun x1032 () Int)
+(declare-fun x1033 () Int)
+(declare-fun x1034 () Int)
+(declare-fun x1035 () Int)
+(declare-fun x1036 () Int)
+(declare-fun x1037 () Int)
+(declare-fun x1038 () Int)
+(declare-fun x1039 () Int)
+(declare-fun x1040 () Int)
+(declare-fun x1041 () Int)
+(declare-fun x1042 () Int)
+(declare-fun x1043 () Int)
+(declare-fun x1044 () Int)
+(declare-fun x1045 () Int)
+(declare-fun x1046 () Int)
+(declare-fun x1047 () Int)
+(declare-fun x1048 () Int)
+(declare-fun x1049 () Int)
+(declare-fun x1050 () Int)
+(declare-fun x1051 () Int)
+(declare-fun x1052 () Int)
+(declare-fun x1053 () Int)
+(declare-fun x1054 () Int)
+(declare-fun x1055 () Int)
+(declare-fun x1056 () Int)
+(declare-fun x1057 () Int)
+(declare-fun x1058 () Int)
+(declare-fun x1059 () Int)
+(declare-fun x1060 () Int)
+(declare-fun x1061 () Int)
+(declare-fun x1062 () Int)
+(declare-fun x1063 () Int)
+(declare-fun x1064 () Int)
+(declare-fun x1065 () Int)
+(declare-fun x1066 () Int)
+(declare-fun x1067 () Int)
+(declare-fun x1068 () Int)
+(declare-fun x1069 () Int)
+(declare-fun x1070 () Int)
+(declare-fun x1071 () Int)
+(declare-fun x1072 () Int)
+(declare-fun x1073 () Int)
+(declare-fun x1074 () Int)
+(declare-fun x1075 () Int)
+(declare-fun x1076 () Int)
+(declare-fun x1077 () Int)
+(declare-fun x1078 () Int)
+(declare-fun x1079 () Int)
+(declare-fun x1080 () Int)
+(declare-fun x1081 () Int)
+(declare-fun x1082 () Int)
+(declare-fun x1083 () Int)
+(declare-fun x1084 () Int)
+(declare-fun x1085 () Int)
+(declare-fun x1086 () Int)
+(declare-fun x1087 () Int)
+(declare-fun x1088 () Int)
+(declare-fun x1089 () Int)
+(declare-fun x1090 () Int)
+(declare-fun x1091 () Int)
+(declare-fun x1092 () Int)
+(declare-fun x1093 () Int)
+(declare-fun x1094 () Int)
+(declare-fun x1095 () Int)
+(declare-fun x1096 () Int)
+(declare-fun x1097 () Int)
+(declare-fun x1098 () Int)
+(declare-fun x1099 () Int)
+(declare-fun x1100 () Int)
+(declare-fun x1101 () Int)
+(declare-fun x1102 () Int)
+(declare-fun x1103 () Int)
+(declare-fun x1104 () Int)
+(declare-fun x1105 () Int)
+(declare-fun x1106 () Int)
+(declare-fun x1107 () Int)
+(declare-fun x1108 () Int)
+(declare-fun x1109 () Int)
+(declare-fun x1110 () Int)
+(declare-fun x1111 () Int)
+(declare-fun x1112 () Int)
+(declare-fun x1113 () Int)
+(declare-fun x1114 () Int)
+(declare-fun x1115 () Int)
+(declare-fun x1116 () Int)
+(declare-fun x1117 () Int)
+(declare-fun x1118 () Int)
+(declare-fun x1119 () Int)
+(declare-fun x1120 () Int)
+(declare-fun x1121 () Int)
+(declare-fun x1122 () Int)
+(declare-fun x1123 () Int)
+(declare-fun x1124 () Int)
+(declare-fun x1125 () Int)
+(declare-fun x1126 () Int)
+(declare-fun x1127 () Int)
+(declare-fun x1128 () Int)
+(declare-fun x1129 () Int)
+(declare-fun x1130 () Int)
+(declare-fun x1131 () Int)
+(declare-fun x1132 () Int)
+(declare-fun x1133 () Int)
+(declare-fun x1134 () Int)
+(declare-fun x1135 () Int)
+(declare-fun x1136 () Int)
+(declare-fun x1137 () Int)
+(declare-fun x1138 () Int)
+(declare-fun x1139 () Int)
+(declare-fun x1140 () Int)
+(declare-fun x1141 () Int)
+(declare-fun x1142 () Int)
+(declare-fun x1143 () Int)
+(declare-fun x1144 () Int)
+(declare-fun x1145 () Int)
+(declare-fun x1146 () Int)
+(declare-fun x1147 () Int)
+(declare-fun x1148 () Int)
+(declare-fun x1149 () Int)
+(declare-fun x1150 () Int)
+(declare-fun x1151 () Int)
+(declare-fun x1152 () Int)
+(declare-fun x1153 () Int)
+(declare-fun x1154 () Int)
+(declare-fun x1155 () Int)
+(declare-fun x1156 () Int)
+(declare-fun x1157 () Int)
+(declare-fun x1158 () Int)
+(declare-fun x1159 () Int)
+(declare-fun x1160 () Int)
+(declare-fun x1161 () Int)
+(declare-fun x1162 () Int)
+(declare-fun x1163 () Int)
+(declare-fun x1164 () Int)
+(declare-fun x1165 () Int)
+(declare-fun x1166 () Int)
+(declare-fun x1167 () Int)
+(declare-fun x1168 () Int)
+(declare-fun x1169 () Int)
+(declare-fun x1170 () Int)
+(declare-fun x1171 () Int)
+(declare-fun x1172 () Int)
+(declare-fun x1173 () Int)
+(declare-fun x1174 () Int)
+(declare-fun x1175 () Int)
+(declare-fun x1176 () Int)
+(declare-fun x1177 () Int)
+(declare-fun x1178 () Int)
+(declare-fun x1179 () Int)
+(declare-fun x1180 () Int)
+(declare-fun x1181 () Int)
+(declare-fun x1182 () Int)
+(declare-fun x1183 () Int)
+(declare-fun x1184 () Int)
+(declare-fun x1185 () Int)
+(declare-fun x1186 () Int)
+(declare-fun x1187 () Int)
+(declare-fun x1188 () Int)
+(declare-fun x1189 () Int)
+(declare-fun x1190 () Int)
+(declare-fun x1191 () Int)
+(declare-fun x1192 () Int)
+(declare-fun x1193 () Int)
+(declare-fun x1194 () Int)
+(declare-fun x1195 () Int)
+(declare-fun x1196 () Int)
+(declare-fun x1197 () Int)
+(declare-fun x1198 () Int)
+(declare-fun x1199 () Int)
+(declare-fun x1200 () Int)
+(declare-fun x1201 () Int)
+(declare-fun x1202 () Int)
+(declare-fun x1203 () Int)
+(declare-fun x1204 () Int)
+(declare-fun x1205 () Int)
+(declare-fun x1206 () Int)
+(declare-fun x1207 () Int)
+(declare-fun x1208 () Int)
+(declare-fun x1209 () Int)
+(declare-fun x1210 () Int)
+(declare-fun x1211 () Int)
+(declare-fun x1212 () Int)
+(declare-fun x1213 () Int)
+(declare-fun x1214 () Int)
+(declare-fun x1215 () Int)
+(declare-fun x1216 () Int)
+(declare-fun x1217 () Int)
+(declare-fun x1218 () Int)
+(declare-fun x1219 () Int)
+(declare-fun x1220 () Int)
+(declare-fun x1221 () Int)
+(declare-fun x1222 () Int)
+(declare-fun x1223 () Int)
+(declare-fun x1224 () Int)
+(declare-fun x1225 () Int)
+(declare-fun x1226 () Int)
+(declare-fun x1227 () Int)
+(declare-fun x1228 () Int)
+(declare-fun x1229 () Int)
+(declare-fun x1230 () Int)
+(declare-fun x1231 () Int)
+(declare-fun x1232 () Int)
+(declare-fun x1233 () Int)
+(declare-fun x1234 () Int)
+(declare-fun x1235 () Int)
+(declare-fun x1236 () Int)
+(declare-fun x1237 () Int)
+(declare-fun x1238 () Int)
+(declare-fun x1239 () Int)
+(declare-fun x1240 () Int)
+(declare-fun x1241 () Int)
+(declare-fun x1242 () Int)
+(declare-fun x1243 () Int)
+(declare-fun x1244 () Int)
+(declare-fun x1245 () Int)
+(declare-fun x1246 () Int)
+(declare-fun x1247 () Int)
+(declare-fun x1248 () Int)
+(declare-fun x1249 () Int)
+(declare-fun x1250 () Int)
+(declare-fun x1251 () Int)
+(declare-fun x1252 () Int)
+(declare-fun x1253 () Int)
+(declare-fun x1254 () Int)
+(declare-fun x1255 () Int)
+(declare-fun x1256 () Int)
+(declare-fun x1257 () Int)
+(declare-fun x1258 () Int)
+(declare-fun x1259 () Int)
+(declare-fun x1260 () Int)
+(declare-fun x1261 () Int)
+(declare-fun x1262 () Int)
+(declare-fun x1263 () Int)
+(declare-fun x1264 () Int)
+(declare-fun x1265 () Int)
+(declare-fun x1266 () Int)
+(declare-fun x1267 () Int)
+(declare-fun x1268 () Int)
+(declare-fun x1269 () Int)
+(declare-fun x1270 () Int)
+(declare-fun x1271 () Int)
+(declare-fun x1272 () Int)
+(declare-fun x1273 () Int)
+(declare-fun x1274 () Int)
+(declare-fun x1275 () Int)
+(declare-fun x1276 () Int)
+(declare-fun x1277 () Int)
+(declare-fun x1278 () Int)
+(declare-fun x1279 () Int)
+(declare-fun x1280 () Int)
+(declare-fun x1281 () Int)
+(declare-fun x1282 () Int)
+(declare-fun x1283 () Int)
+(declare-fun x1284 () Int)
+(declare-fun x1285 () Int)
+(declare-fun x1286 () Int)
+(declare-fun x1287 () Int)
+(declare-fun x1288 () Int)
+(declare-fun x1289 () Int)
+(declare-fun x1290 () Int)
+(declare-fun x1291 () Int)
+(declare-fun x1292 () Int)
+(declare-fun x1293 () Int)
+(declare-fun x1294 () Int)
+(declare-fun x1295 () Int)
+(declare-fun x1296 () Int)
+(declare-fun x1297 () Int)
+(declare-fun x1298 () Int)
+(declare-fun x1299 () Int)
+(declare-fun x1300 () Int)
+(declare-fun x1301 () Int)
+(declare-fun x1302 () Int)
+(declare-fun x1303 () Int)
+(declare-fun x1304 () Int)
+(declare-fun x1305 () Int)
+(declare-fun x1306 () Int)
+(declare-fun x1307 () Int)
+(declare-fun x1308 () Int)
+(declare-fun x1309 () Int)
+(declare-fun x1310 () Int)
+(declare-fun x1311 () Int)
+(declare-fun x1312 () Int)
+(declare-fun x1313 () Int)
+(declare-fun x1314 () Int)
+(declare-fun x1315 () Int)
+(declare-fun x1316 () Int)
+(declare-fun x1317 () Int)
+(declare-fun x1318 () Int)
+(declare-fun x1319 () Int)
+(declare-fun x1320 () Int)
+(declare-fun x1321 () Int)
+(declare-fun x1322 () Int)
+(declare-fun x1323 () Int)
+(declare-fun x1324 () Int)
+(declare-fun x1325 () Int)
+(declare-fun x1326 () Int)
+(declare-fun x1327 () Int)
+(declare-fun x1328 () Int)
+(declare-fun x1329 () Int)
+(declare-fun x1330 () Int)
+(declare-fun x1331 () Int)
+(declare-fun x1332 () Int)
+(declare-fun x1333 () Int)
+(declare-fun x1334 () Int)
+(declare-fun x1335 () Int)
+(declare-fun x1336 () Int)
+(declare-fun x1337 () Int)
+(declare-fun x1338 () Int)
+(declare-fun x1339 () Int)
+(declare-fun x1340 () Int)
+(declare-fun x1341 () Int)
+(declare-fun x1342 () Int)
+(declare-fun x1343 () Int)
+(declare-fun x1344 () Int)
+(declare-fun x1345 () Int)
+(declare-fun x1346 () Int)
+(declare-fun x1347 () Int)
+(declare-fun x1348 () Int)
+(declare-fun x1349 () Int)
+(declare-fun x1350 () Int)
+(declare-fun x1351 () Int)
+(declare-fun x1352 () Int)
+(declare-fun x1353 () Int)
+(declare-fun x1354 () Int)
+(declare-fun x1355 () Int)
+(declare-fun x1356 () Int)
+(declare-fun x1357 () Int)
+(declare-fun x1358 () Int)
+(declare-fun x1359 () Int)
+(declare-fun x1360 () Int)
+(declare-fun x1361 () Int)
+(declare-fun x1362 () Int)
+(declare-fun x1363 () Int)
+(declare-fun x1364 () Int)
+(declare-fun x1365 () Int)
+(declare-fun x1366 () Int)
+(declare-fun x1367 () Int)
+(declare-fun x1368 () Int)
+(declare-fun x1369 () Int)
+(declare-fun x1370 () Int)
+(declare-fun x1371 () Int)
+(declare-fun x1372 () Int)
+(declare-fun x1373 () Int)
+(declare-fun x1374 () Int)
+(declare-fun x1375 () Int)
+(declare-fun x1376 () Int)
+(declare-fun x1377 () Int)
+(declare-fun x1378 () Int)
+(declare-fun x1379 () Int)
+(declare-fun x1380 () Int)
+(declare-fun x1381 () Int)
+(declare-fun x1382 () Int)
+(declare-fun x1383 () Int)
+(declare-fun x1384 () Int)
+(declare-fun x1385 () Int)
+(declare-fun x1386 () Int)
+(declare-fun x1387 () Int)
+(declare-fun x1388 () Int)
+(declare-fun x1389 () Int)
+(declare-fun x1390 () Int)
+(declare-fun x1391 () Int)
+(declare-fun x1392 () Int)
+(declare-fun x1393 () Int)
+(declare-fun x1394 () Int)
+(declare-fun x1395 () Int)
+(declare-fun x1396 () Int)
+(declare-fun x1397 () Int)
+(declare-fun x1398 () Int)
+(declare-fun x1399 () Int)
+(declare-fun x1400 () Int)
+(declare-fun x1401 () Int)
+(declare-fun x1402 () Int)
+(declare-fun x1403 () Int)
+(declare-fun x1404 () Int)
+(declare-fun x1405 () Int)
+(declare-fun x1406 () Int)
+(declare-fun x1407 () Int)
+(declare-fun x1408 () Int)
+(declare-fun x1409 () Int)
+(declare-fun x1410 () Int)
+(declare-fun x1411 () Int)
+(declare-fun x1412 () Int)
+(declare-fun x1413 () Int)
+(declare-fun x1414 () Int)
+(declare-fun x1415 () Int)
+(declare-fun x1416 () Int)
+(declare-fun x1417 () Int)
+(declare-fun x1418 () Int)
+(declare-fun x1419 () Int)
+(declare-fun x1420 () Int)
+(declare-fun x1421 () Int)
+(declare-fun x1422 () Int)
+(declare-fun x1423 () Int)
+(declare-fun x1424 () Int)
+(declare-fun x1425 () Int)
+(declare-fun x1426 () Int)
+(declare-fun x1427 () Int)
+(declare-fun x1428 () Int)
+(declare-fun x1429 () Int)
+(declare-fun x1430 () Int)
+(declare-fun x1431 () Int)
+(declare-fun x1432 () Int)
+(declare-fun x1433 () Int)
+(declare-fun x1434 () Int)
+(declare-fun x1435 () Int)
+(declare-fun x1436 () Int)
+(declare-fun x1437 () Int)
+(declare-fun x1438 () Int)
+(declare-fun x1439 () Int)
+(declare-fun x1440 () Int)
+(declare-fun x1441 () Int)
+(declare-fun x1442 () Int)
+(declare-fun x1443 () Int)
+(declare-fun x1444 () Int)
+(declare-fun x1445 () Int)
+(declare-fun x1446 () Int)
+(declare-fun x1447 () Int)
+(declare-fun x1448 () Int)
+(declare-fun x1449 () Int)
+(declare-fun x1450 () Int)
+(declare-fun x1451 () Int)
+(declare-fun x1452 () Int)
+(declare-fun x1453 () Int)
+(declare-fun x1454 () Int)
+(declare-fun x1455 () Int)
+(declare-fun x1456 () Int)
+(declare-fun x1457 () Int)
+(declare-fun x1458 () Int)
+(declare-fun x1459 () Int)
+(declare-fun x1460 () Int)
+(declare-fun x1461 () Int)
+(declare-fun x1462 () Int)
+(declare-fun x1463 () Int)
+(declare-fun x1464 () Int)
+(declare-fun x1465 () Int)
+(declare-fun x1466 () Int)
+(declare-fun x1467 () Int)
+(declare-fun x1468 () Int)
+(declare-fun x1469 () Int)
+(declare-fun x1470 () Int)
+(declare-fun x1471 () Int)
+(declare-fun x1472 () Int)
+(declare-fun x1473 () Int)
+(declare-fun x1474 () Int)
+(declare-fun x1475 () Int)
+(declare-fun x1476 () Int)
+(declare-fun x1477 () Int)
+(declare-fun x1478 () Int)
+(declare-fun x1479 () Int)
+(declare-fun x1480 () Int)
+(declare-fun x1481 () Int)
+(declare-fun x1482 () Int)
+(declare-fun x1483 () Int)
+(declare-fun x1484 () Int)
+(declare-fun x1485 () Int)
+(declare-fun x1486 () Int)
+(declare-fun x1487 () Int)
+(declare-fun x1488 () Int)
+(declare-fun x1489 () Int)
+(declare-fun x1490 () Int)
+(declare-fun x1491 () Int)
+(declare-fun x1492 () Int)
+(declare-fun x1493 () Int)
+(declare-fun x1494 () Int)
+(declare-fun x1495 () Int)
+(declare-fun x1496 () Int)
+(declare-fun x1497 () Int)
+(declare-fun x1498 () Int)
+(declare-fun x1499 () Int)
+(declare-fun x1500 () Int)
+(declare-fun x1501 () Int)
+(declare-fun x1502 () Int)
+(declare-fun x1503 () Int)
+(declare-fun x1504 () Int)
+(declare-fun x1505 () Int)
+(declare-fun x1506 () Int)
+(declare-fun x1507 () Int)
+(declare-fun x1508 () Int)
+(declare-fun x1509 () Int)
+(declare-fun x1510 () Int)
+(declare-fun x1511 () Int)
+(declare-fun x1512 () Int)
+(declare-fun x1513 () Int)
+(declare-fun x1514 () Int)
+(declare-fun x1515 () Int)
+(declare-fun x1516 () Int)
+(declare-fun x1517 () Int)
+(declare-fun x1518 () Int)
+(declare-fun x1519 () Int)
+(declare-fun x1520 () Int)
+(declare-fun x1521 () Int)
+(declare-fun x1522 () Int)
+(declare-fun x1523 () Int)
+(declare-fun x1524 () Int)
+(declare-fun x1525 () Int)
+(declare-fun x1526 () Int)
+(declare-fun x1527 () Int)
+(declare-fun x1528 () Int)
+(declare-fun x1529 () Int)
+(declare-fun x1530 () Int)
+(declare-fun x1531 () Int)
+(declare-fun x1532 () Int)
+(declare-fun x1533 () Int)
+(declare-fun x1534 () Int)
+(declare-fun x1535 () Int)
+(declare-fun x1536 () Int)
+(declare-fun x1537 () Int)
+(declare-fun x1538 () Int)
+(declare-fun x1539 () Int)
+(declare-fun x1540 () Int)
+(declare-fun x1541 () Int)
+(declare-fun x1542 () Int)
+(declare-fun x1543 () Int)
+(declare-fun x1544 () Int)
+(declare-fun x1545 () Int)
+(declare-fun x1546 () Int)
+(declare-fun x1547 () Int)
+(declare-fun x1548 () Int)
+(declare-fun x1549 () Int)
+(declare-fun x1550 () Int)
+(declare-fun x1551 () Int)
+(declare-fun x1552 () Int)
+(declare-fun x1553 () Int)
+(declare-fun x1554 () Int)
+(declare-fun x1555 () Int)
+(declare-fun x1556 () Int)
+(declare-fun x1557 () Int)
+(declare-fun x1558 () Int)
+(declare-fun x1559 () Int)
+(declare-fun x1560 () Int)
+(declare-fun x1561 () Int)
+(declare-fun x1562 () Int)
+(declare-fun x1563 () Int)
+(declare-fun x1564 () Int)
+(declare-fun x1565 () Int)
+(declare-fun x1566 () Int)
+(declare-fun x1567 () Int)
+(declare-fun x1568 () Int)
+(declare-fun x1569 () Int)
+(declare-fun x1570 () Int)
+(declare-fun x1571 () Int)
+(declare-fun x1572 () Int)
+(declare-fun x1573 () Int)
+(declare-fun x1574 () Int)
+(declare-fun x1575 () Int)
+(declare-fun x1576 () Int)
+(declare-fun x1577 () Int)
+(declare-fun x1578 () Int)
+(declare-fun x1579 () Int)
+(declare-fun x1580 () Int)
+(declare-fun x1581 () Int)
+(declare-fun x1582 () Int)
+(declare-fun x1583 () Int)
+(declare-fun x1584 () Int)
+(declare-fun x1585 () Int)
+(declare-fun x1586 () Int)
+(declare-fun x1587 () Int)
+(declare-fun x1588 () Int)
+(declare-fun x1589 () Int)
+(declare-fun x1590 () Int)
+(declare-fun x1591 () Int)
+(declare-fun x1592 () Int)
+(declare-fun x1593 () Int)
+(declare-fun x1594 () Int)
+(declare-fun x1595 () Int)
+(declare-fun x1596 () Int)
+(declare-fun x1597 () Int)
+(declare-fun x1598 () Int)
+(declare-fun x1599 () Int)
+(declare-fun x1600 () Int)
+(declare-fun x1601 () Int)
+(declare-fun x1602 () Int)
+(declare-fun x1603 () Int)
+(declare-fun x1604 () Int)
+(declare-fun x1605 () Int)
+(declare-fun x1606 () Int)
+(declare-fun x1607 () Int)
+(declare-fun x1608 () Int)
+(declare-fun x1609 () Int)
+(declare-fun x1610 () Int)
+(declare-fun x1611 () Int)
+(declare-fun x1612 () Int)
+(declare-fun x1613 () Int)
+(declare-fun x1614 () Int)
+(declare-fun x1615 () Int)
+(declare-fun x1616 () Int)
+(declare-fun x1617 () Int)
+(declare-fun x1618 () Int)
+(declare-fun x1619 () Int)
+(declare-fun x1620 () Int)
+(declare-fun x1621 () Int)
+(declare-fun x1622 () Int)
+(declare-fun x1623 () Int)
+(declare-fun x1624 () Int)
+(declare-fun x1625 () Int)
+(declare-fun x1626 () Int)
+(declare-fun x1627 () Int)
+(declare-fun x1628 () Int)
+(declare-fun x1629 () Int)
+(declare-fun x1630 () Int)
+(declare-fun x1631 () Int)
+(declare-fun x1632 () Int)
+(declare-fun x1633 () Int)
+(declare-fun x1634 () Int)
+(declare-fun x1635 () Int)
+(declare-fun x1636 () Int)
+(declare-fun x1637 () Int)
+(declare-fun x1638 () Int)
+(declare-fun x1639 () Int)
+(declare-fun x1640 () Int)
+(declare-fun x1641 () Int)
+(declare-fun x1642 () Int)
+(declare-fun x1643 () Int)
+(declare-fun x1644 () Int)
+(declare-fun x1645 () Int)
+(declare-fun x1646 () Int)
+(declare-fun x1647 () Int)
+(declare-fun x1648 () Int)
+(declare-fun x1649 () Int)
+(declare-fun x1650 () Int)
+(declare-fun x1651 () Int)
+(declare-fun x1652 () Int)
+(declare-fun x1653 () Int)
+(declare-fun x1654 () Int)
+(declare-fun x1655 () Int)
+(declare-fun x1656 () Int)
+(declare-fun x1657 () Int)
+(declare-fun x1658 () Int)
+(declare-fun x1659 () Int)
+(declare-fun x1660 () Int)
+(declare-fun x1661 () Int)
+(declare-fun x1662 () Int)
+(declare-fun x1663 () Int)
+(declare-fun x1664 () Int)
+(declare-fun x1665 () Int)
+(declare-fun x1666 () Int)
+(declare-fun x1667 () Int)
+(declare-fun x1668 () Int)
+(declare-fun x1669 () Int)
+(declare-fun x1670 () Int)
+(declare-fun x1671 () Int)
+(declare-fun x1672 () Int)
+(declare-fun x1673 () Int)
+(declare-fun x1674 () Int)
+(declare-fun x1675 () Int)
+(declare-fun x1676 () Int)
+(declare-fun x1677 () Int)
+(declare-fun x1678 () Int)
+(declare-fun x1679 () Int)
+(declare-fun x1680 () Int)
+(declare-fun x1681 () Int)
+(declare-fun x1682 () Int)
+(declare-fun x1683 () Int)
+(declare-fun x1684 () Int)
+(declare-fun x1685 () Int)
+(declare-fun x1686 () Int)
+(declare-fun x1687 () Int)
+(declare-fun x1688 () Int)
+(declare-fun x1689 () Int)
+(declare-fun x1690 () Int)
+(declare-fun x1691 () Int)
+(declare-fun x1692 () Int)
+(declare-fun x1693 () Int)
+(declare-fun x1694 () Int)
+(declare-fun x1695 () Int)
+(declare-fun x1696 () Int)
+(declare-fun x1697 () Int)
+(declare-fun x1698 () Int)
+(declare-fun x1699 () Int)
+(declare-fun x1700 () Int)
+(declare-fun x1701 () Int)
+(declare-fun x1702 () Int)
+(declare-fun x1703 () Int)
+(declare-fun x1704 () Int)
+(declare-fun x1705 () Int)
+(declare-fun x1706 () Int)
+(declare-fun x1707 () Int)
+(declare-fun x1708 () Int)
+(declare-fun x1709 () Int)
+(declare-fun x1710 () Int)
+(declare-fun x1711 () Int)
+(declare-fun x1712 () Int)
+(declare-fun x1713 () Int)
+(declare-fun x1714 () Int)
+(declare-fun x1715 () Int)
+(declare-fun x1716 () Int)
+(declare-fun x1717 () Int)
+(declare-fun x1718 () Int)
+(declare-fun x1719 () Int)
+(declare-fun x1720 () Int)
+(declare-fun x1721 () Int)
+(declare-fun x1722 () Int)
+(declare-fun x1723 () Int)
+(declare-fun x1724 () Int)
+(declare-fun x1725 () Int)
+(declare-fun x1726 () Int)
+(declare-fun x1727 () Int)
+(declare-fun x1728 () Int)
+(declare-fun x1729 () Int)
+(declare-fun x1730 () Int)
+(declare-fun x1731 () Int)
+(declare-fun x1732 () Int)
+(declare-fun x1733 () Int)
+(declare-fun x1734 () Int)
+(declare-fun x1735 () Int)
+(declare-fun x1736 () Int)
+(declare-fun x1737 () Int)
+(declare-fun x1738 () Int)
+(declare-fun x1739 () Int)
+(declare-fun x1740 () Int)
+(declare-fun x1741 () Int)
+(declare-fun x1742 () Int)
+(declare-fun x1743 () Int)
+(declare-fun x1744 () Int)
+(declare-fun x1745 () Int)
+(declare-fun x1746 () Int)
+(declare-fun x1747 () Int)
+(declare-fun x1748 () Int)
+(declare-fun x1749 () Int)
+(declare-fun x1750 () Int)
+(declare-fun x1751 () Int)
+(declare-fun x1752 () Int)
+(declare-fun x1753 () Int)
+(declare-fun x1754 () Int)
+(declare-fun x1755 () Int)
+(declare-fun x1756 () Int)
+(declare-fun x1757 () Int)
+(declare-fun x1758 () Int)
+(declare-fun x1759 () Int)
+(declare-fun x1760 () Int)
+(declare-fun x1761 () Int)
+(declare-fun x1762 () Int)
+(declare-fun x1763 () Int)
+(declare-fun x1764 () Int)
+(declare-fun x1765 () Int)
+(declare-fun x1766 () Int)
+(declare-fun x1767 () Int)
+(declare-fun x1768 () Int)
+(declare-fun x1769 () Int)
+(declare-fun x1770 () Int)
+(declare-fun x1771 () Int)
+(declare-fun x1772 () Int)
+(declare-fun x1773 () Int)
+(declare-fun x1774 () Int)
+(declare-fun x1775 () Int)
+(declare-fun x1776 () Int)
+(declare-fun x1777 () Int)
+(declare-fun x1778 () Int)
+(declare-fun x1779 () Int)
+(declare-fun x1780 () Int)
+(declare-fun x1781 () Int)
+(declare-fun x1782 () Int)
+(declare-fun x1783 () Int)
+(declare-fun x1784 () Int)
+(declare-fun x1785 () Int)
+(declare-fun x1786 () Int)
+(declare-fun x1787 () Int)
+(declare-fun x1788 () Int)
+(declare-fun x1789 () Int)
+(declare-fun x1790 () Int)
+(declare-fun x1791 () Int)
+(declare-fun x1792 () Int)
+(declare-fun x1793 () Int)
+(declare-fun x1794 () Int)
+(declare-fun x1795 () Int)
+(declare-fun x1796 () Int)
+(declare-fun x1797 () Int)
+(declare-fun x1798 () Int)
+(declare-fun x1799 () Int)
+(declare-fun x1800 () Int)
+(declare-fun x1801 () Int)
+(declare-fun x1802 () Int)
+(declare-fun x1803 () Int)
+(declare-fun x1804 () Int)
+(declare-fun x1805 () Int)
+(declare-fun x1806 () Int)
+(declare-fun x1807 () Int)
+(declare-fun x1808 () Int)
+(declare-fun x1809 () Int)
+(declare-fun x1810 () Int)
+(declare-fun x1811 () Int)
+(declare-fun x1812 () Int)
+(declare-fun x1813 () Int)
+(declare-fun x1814 () Int)
+(declare-fun x1815 () Int)
+(declare-fun x1816 () Int)
+(declare-fun x1817 () Int)
+(declare-fun x1818 () Int)
+(declare-fun x1819 () Int)
+(declare-fun x1820 () Int)
+(declare-fun x1821 () Int)
+(declare-fun x1822 () Int)
+(declare-fun x1823 () Int)
+(declare-fun x1824 () Int)
+(declare-fun x1825 () Int)
+(declare-fun x1826 () Int)
+(declare-fun x1827 () Int)
+(declare-fun x1828 () Int)
+(declare-fun x1829 () Int)
+(declare-fun x1830 () Int)
+(declare-fun x1831 () Int)
+(declare-fun x1832 () Int)
+(declare-fun x1833 () Int)
+(declare-fun x1834 () Int)
+(declare-fun x1835 () Int)
+(declare-fun x1836 () Int)
+(declare-fun x1837 () Int)
+(declare-fun x1838 () Int)
+(declare-fun x1839 () Int)
+(declare-fun x1840 () Int)
+(declare-fun x1841 () Int)
+(declare-fun x1842 () Int)
+(declare-fun x1843 () Int)
+(declare-fun x1844 () Int)
+(declare-fun x1845 () Int)
+(declare-fun x1846 () Int)
+(declare-fun x1847 () Int)
+(declare-fun x1848 () Int)
+(declare-fun x1849 () Int)
+(declare-fun x1850 () Int)
+(declare-fun x1851 () Int)
+(declare-fun x1852 () Int)
+(declare-fun x1853 () Int)
+(declare-fun x1854 () Int)
+(declare-fun x1855 () Int)
+(declare-fun x1856 () Int)
+(declare-fun x1857 () Int)
+(declare-fun x1858 () Int)
+(declare-fun x1859 () Int)
+(declare-fun x1860 () Int)
+(declare-fun x1861 () Int)
+(declare-fun x1862 () Int)
+(declare-fun x1863 () Int)
+(declare-fun x1864 () Int)
+(declare-fun x1865 () Int)
+(declare-fun x1866 () Int)
+(declare-fun x1867 () Int)
+(declare-fun x1868 () Int)
+(declare-fun x1869 () Int)
+(declare-fun x1870 () Int)
+(declare-fun x1871 () Int)
+(declare-fun x1872 () Int)
+(declare-fun x1873 () Int)
+(declare-fun x1874 () Int)
+(declare-fun x1875 () Int)
+(declare-fun x1876 () Int)
+(declare-fun x1877 () Int)
+(declare-fun x1878 () Int)
+(declare-fun x1879 () Int)
+(declare-fun x1880 () Int)
+(declare-fun x1881 () Int)
+(declare-fun x1882 () Int)
+(declare-fun x1883 () Int)
+(declare-fun x1884 () Int)
+(declare-fun x1885 () Int)
+(declare-fun x1886 () Int)
+(declare-fun x1887 () Int)
+(declare-fun x1888 () Int)
+(declare-fun x1889 () Int)
+(declare-fun x1890 () Int)
+(declare-fun x1891 () Int)
+(declare-fun x1892 () Int)
+(declare-fun x1893 () Int)
+(declare-fun x1894 () Int)
+(declare-fun x1895 () Int)
+(declare-fun x1896 () Int)
+(declare-fun x1897 () Int)
+(declare-fun x1898 () Int)
+(declare-fun x1899 () Int)
+(declare-fun x1900 () Int)
+(declare-fun x1901 () Int)
+(declare-fun x1902 () Int)
+(declare-fun x1903 () Int)
+(declare-fun x1904 () Int)
+(declare-fun x1905 () Int)
+(declare-fun x1906 () Int)
+(declare-fun x1907 () Int)
+(declare-fun x1908 () Int)
+(declare-fun x1909 () Int)
+(declare-fun x1910 () Int)
+(declare-fun x1911 () Int)
+(declare-fun x1912 () Int)
+(declare-fun x1913 () Int)
+(declare-fun x1914 () Int)
+(declare-fun x1915 () Int)
+(declare-fun x1916 () Int)
+(declare-fun x1917 () Int)
+(declare-fun x1918 () Int)
+(declare-fun x1919 () Int)
+(declare-fun x1920 () Int)
+(declare-fun x1921 () Int)
+(declare-fun x1922 () Int)
+(declare-fun x1923 () Int)
+(declare-fun x1924 () Int)
+(declare-fun x1925 () Int)
+(declare-fun x1926 () Int)
+(declare-fun x1927 () Int)
+(declare-fun x1928 () Int)
+(declare-fun x1929 () Int)
+(declare-fun x1930 () Int)
+(declare-fun x1931 () Int)
+(declare-fun x1932 () Int)
+(declare-fun x1933 () Int)
+(declare-fun x1934 () Int)
+(declare-fun x1935 () Int)
+(declare-fun x1936 () Int)
+(declare-fun x1937 () Int)
+(declare-fun x1938 () Int)
+(declare-fun x1939 () Int)
+(declare-fun x1940 () Int)
+(declare-fun x1941 () Int)
+(declare-fun x1942 () Int)
+(declare-fun x1943 () Int)
+(declare-fun x1944 () Int)
+(declare-fun x1945 () Int)
+(declare-fun x1946 () Int)
+(declare-fun x1947 () Int)
+(declare-fun x1948 () Int)
+(declare-fun x1949 () Int)
+(declare-fun x1950 () Int)
+(declare-fun x1951 () Int)
+(declare-fun x1952 () Int)
+(declare-fun x1953 () Int)
+(declare-fun x1954 () Int)
+(declare-fun x1955 () Int)
+(declare-fun x1956 () Int)
+(declare-fun x1957 () Int)
+(declare-fun x1958 () Int)
+(declare-fun x1959 () Int)
+(declare-fun x1960 () Int)
+(declare-fun x1961 () Int)
+(declare-fun x1962 () Int)
+(declare-fun x1963 () Int)
+(declare-fun x1964 () Int)
+(declare-fun x1965 () Int)
+(declare-fun x1966 () Int)
+(declare-fun x1967 () Int)
+(declare-fun x1968 () Int)
+(declare-fun x1969 () Int)
+(declare-fun x1970 () Int)
+(declare-fun x1971 () Int)
+(declare-fun x1972 () Int)
+(declare-fun x1973 () Int)
+(declare-fun x1974 () Int)
+(declare-fun x1975 () Int)
+(declare-fun x1976 () Int)
+(declare-fun x1977 () Int)
+(declare-fun x1978 () Int)
+(declare-fun x1979 () Int)
+(declare-fun x1980 () Int)
+(declare-fun x1981 () Int)
+(declare-fun x1982 () Int)
+(declare-fun x1983 () Int)
+(declare-fun x1984 () Int)
+(declare-fun x1985 () Int)
+(declare-fun x1986 () Int)
+(declare-fun x1987 () Int)
+(declare-fun x1988 () Int)
+(declare-fun x1989 () Int)
+(declare-fun x1990 () Int)
+(declare-fun x1991 () Int)
+(declare-fun x1992 () Int)
+(declare-fun x1993 () Int)
+(declare-fun x1994 () Int)
+(declare-fun x1995 () Int)
+(declare-fun x1996 () Int)
+(declare-fun x1997 () Int)
+(declare-fun x1998 () Int)
+(declare-fun x1999 () Int)
+(declare-fun x2000 () Int)
+(declare-fun x2001 () Int)
+(declare-fun x2002 () Int)
+(declare-fun x2003 () Int)
+(declare-fun x2004 () Int)
+(declare-fun x2005 () Int)
+(declare-fun x2006 () Int)
+(declare-fun x2007 () Int)
+(declare-fun x2008 () Int)
+(declare-fun x2009 () Int)
+(declare-fun x2010 () Int)
+(declare-fun x2011 () Int)
+(declare-fun x2012 () Int)
+(declare-fun x2013 () Int)
+(declare-fun x2014 () Int)
+(declare-fun x2015 () Int)
+(declare-fun x2016 () Int)
+(declare-fun x2017 () Int)
+(declare-fun x2018 () Int)
+(declare-fun x2019 () Int)
+(declare-fun x2020 () Int)
+(declare-fun x2021 () Int)
+(declare-fun x2022 () Int)
+(declare-fun x2023 () Int)
+(declare-fun x2024 () Int)
+(declare-fun x2025 () Int)
+(declare-fun x2026 () Int)
+(declare-fun x2027 () Int)
+(declare-fun x2028 () Int)
+(declare-fun x2029 () Int)
+(declare-fun x2030 () Int)
+(declare-fun x2031 () Int)
+(declare-fun x2032 () Int)
+(declare-fun x2033 () Int)
+(declare-fun x2034 () Int)
+(declare-fun x2035 () Int)
+(declare-fun x2036 () Int)
+(declare-fun x2037 () Int)
+(declare-fun x2038 () Int)
+(declare-fun x2039 () Int)
+(declare-fun x2040 () Int)
+(declare-fun x2041 () Int)
+(declare-fun x2042 () Int)
+(declare-fun x2043 () Int)
+(declare-fun x2044 () Int)
+(declare-fun x2045 () Int)
+(declare-fun x2046 () Int)
+(declare-fun x2047 () Int)
+(declare-fun x2048 () Int)
+(declare-fun x2049 () Int)
+(declare-fun x2050 () Int)
+(declare-fun x2051 () Int)
+(declare-fun x2052 () Int)
+(declare-fun x2053 () Int)
+(declare-fun x2054 () Int)
+(declare-fun x2055 () Int)
+(declare-fun x2056 () Int)
+(declare-fun x2057 () Int)
+(declare-fun x2058 () Int)
+(declare-fun x2059 () Int)
+(declare-fun x2060 () Int)
+(declare-fun x2061 () Int)
+(declare-fun x2062 () Int)
+(declare-fun x2063 () Int)
+(declare-fun x2064 () Int)
+(declare-fun x2065 () Int)
+(declare-fun x2066 () Int)
+(declare-fun x2067 () Int)
+(declare-fun x2068 () Int)
+(declare-fun x2069 () Int)
+(declare-fun x2070 () Int)
+(declare-fun x2071 () Int)
+(declare-fun x2072 () Int)
+(declare-fun x2073 () Int)
+(declare-fun x2074 () Int)
+(declare-fun x2075 () Int)
+(declare-fun x2076 () Int)
+(declare-fun x2077 () Int)
+(declare-fun x2078 () Int)
+(declare-fun x2079 () Int)
+(declare-fun x2080 () Int)
+(declare-fun x2081 () Int)
+(declare-fun x2082 () Int)
+(declare-fun x2083 () Int)
+(declare-fun x2084 () Int)
+(declare-fun x2085 () Int)
+(declare-fun x2086 () Int)
+(declare-fun x2087 () Int)
+(declare-fun x2088 () Int)
+(declare-fun x2089 () Int)
+(declare-fun x2090 () Int)
+(declare-fun x2091 () Int)
+(declare-fun x2092 () Int)
+(declare-fun x2093 () Int)
+(declare-fun x2094 () Int)
+(declare-fun x2095 () Int)
+(declare-fun x2096 () Int)
+(declare-fun x2097 () Int)
+(declare-fun x2098 () Int)
+(declare-fun x2099 () Int)
+(declare-fun x2100 () Int)
+(declare-fun x2101 () Int)
+(declare-fun x2102 () Int)
+(declare-fun x2103 () Int)
+(declare-fun x2104 () Int)
+(declare-fun x2105 () Int)
+(declare-fun x2106 () Int)
+(declare-fun x2107 () Int)
+(declare-fun x2108 () Int)
+(declare-fun x2109 () Int)
+(declare-fun x2110 () Int)
+(declare-fun x2111 () Int)
+(declare-fun x2112 () Int)
+(declare-fun x2113 () Int)
+(declare-fun x2114 () Int)
+(declare-fun x2115 () Int)
+(declare-fun x2116 () Int)
+(declare-fun x2117 () Int)
+(declare-fun x2118 () Int)
+(declare-fun x2119 () Int)
+(declare-fun x2120 () Int)
+(declare-fun x2121 () Int)
+(declare-fun x2122 () Int)
+(declare-fun x2123 () Int)
+(declare-fun x2124 () Int)
+(declare-fun x2125 () Int)
+(declare-fun x2126 () Int)
+(declare-fun x2127 () Int)
+(declare-fun x2128 () Int)
+(declare-fun x2129 () Int)
+(declare-fun x2130 () Int)
+(declare-fun x2131 () Int)
+(declare-fun x2132 () Int)
+(declare-fun x2133 () Int)
+(declare-fun x2134 () Int)
+(declare-fun x2135 () Int)
+(declare-fun x2136 () Int)
+(declare-fun x2137 () Int)
+(declare-fun x2138 () Int)
+(declare-fun x2139 () Int)
+(declare-fun x2140 () Int)
+(declare-fun x2141 () Int)
+(declare-fun x2142 () Int)
+(declare-fun x2143 () Int)
+(declare-fun x2144 () Int)
+(declare-fun x2145 () Int)
+(declare-fun x2146 () Int)
+(declare-fun x2147 () Int)
+(declare-fun x2148 () Int)
+(declare-fun x2149 () Int)
+(declare-fun x2150 () Int)
+(declare-fun x2151 () Int)
+(declare-fun x2152 () Int)
+(declare-fun x2153 () Int)
+(declare-fun x2154 () Int)
+(declare-fun x2155 () Int)
+(declare-fun x2156 () Int)
+(declare-fun x2157 () Int)
+(declare-fun x2158 () Int)
+(declare-fun x2159 () Int)
+(declare-fun x2160 () Int)
+(declare-fun x2161 () Int)
+(declare-fun x2162 () Int)
+(declare-fun x2163 () Int)
+(declare-fun x2164 () Int)
+(declare-fun x2165 () Int)
+(declare-fun x2166 () Int)
+(declare-fun x2167 () Int)
+(declare-fun x2168 () Int)
+(declare-fun x2169 () Int)
+(declare-fun x2170 () Int)
+(declare-fun x2171 () Int)
+(declare-fun x2172 () Int)
+(declare-fun x2173 () Int)
+(declare-fun x2174 () Int)
+(declare-fun x2175 () Int)
+(declare-fun x2176 () Int)
+(declare-fun x2177 () Int)
+(declare-fun x2178 () Int)
+(declare-fun x2179 () Int)
+(declare-fun x2180 () Int)
+(declare-fun x2181 () Int)
+(declare-fun x2182 () Int)
+(declare-fun x2183 () Int)
+(declare-fun x2184 () Int)
+(declare-fun x2185 () Int)
+(declare-fun x2186 () Int)
+(declare-fun x2187 () Int)
+(declare-fun x2188 () Int)
+(declare-fun x2189 () Int)
+(declare-fun x2190 () Int)
+(declare-fun x2191 () Int)
+(declare-fun x2192 () Int)
+(declare-fun x2193 () Int)
+(declare-fun x2194 () Int)
+(declare-fun x2195 () Int)
+(declare-fun x2196 () Int)
+(declare-fun x2197 () Int)
+(declare-fun x2198 () Int)
+(declare-fun x2199 () Int)
+(declare-fun x2200 () Int)
+(declare-fun x2201 () Int)
+(declare-fun x2202 () Int)
+(declare-fun x2203 () Int)
+(declare-fun x2204 () Int)
+(declare-fun x2205 () Int)
+(declare-fun x2206 () Int)
+(declare-fun x2207 () Int)
+(declare-fun x2208 () Int)
+(declare-fun x2209 () Int)
+(declare-fun x2210 () Int)
+(declare-fun x2211 () Int)
+(declare-fun x2212 () Int)
+(declare-fun x2213 () Int)
+(declare-fun x2214 () Int)
+(declare-fun x2215 () Int)
+(declare-fun x2216 () Int)
+(declare-fun x2217 () Int)
+(declare-fun x2218 () Int)
+(declare-fun x2219 () Int)
+(declare-fun x2220 () Int)
+(declare-fun x2221 () Int)
+(declare-fun x2222 () Int)
+(declare-fun x2223 () Int)
+(declare-fun x2224 () Int)
+(declare-fun x2225 () Int)
+(declare-fun x2226 () Int)
+(declare-fun x2227 () Int)
+(declare-fun x2228 () Int)
+(declare-fun x2229 () Int)
+(declare-fun x2230 () Int)
+(declare-fun x2231 () Int)
+(declare-fun x2232 () Int)
+(declare-fun x2233 () Int)
+(declare-fun x2234 () Int)
+(declare-fun x2235 () Int)
+(declare-fun x2236 () Int)
+(declare-fun x2237 () Int)
+(declare-fun x2238 () Int)
+(declare-fun x2239 () Int)
+(declare-fun x2240 () Int)
+(declare-fun x2241 () Int)
+(declare-fun x2242 () Int)
+(declare-fun x2243 () Int)
+(declare-fun x2244 () Int)
+(declare-fun x2245 () Int)
+(declare-fun x2246 () Int)
+(declare-fun x2247 () Int)
+(declare-fun x2248 () Int)
+(declare-fun x2249 () Int)
+(declare-fun x2250 () Int)
+(declare-fun x2251 () Int)
+(declare-fun x2252 () Int)
+(declare-fun x2253 () Int)
+(declare-fun x2254 () Int)
+(declare-fun x2255 () Int)
+(declare-fun x2256 () Int)
+(declare-fun x2257 () Int)
+(declare-fun x2258 () Int)
+(declare-fun x2259 () Int)
+(declare-fun x2260 () Int)
+(declare-fun x2261 () Int)
+(declare-fun x2262 () Int)
+(declare-fun x2263 () Int)
+(declare-fun x2264 () Int)
+(declare-fun x2265 () Int)
+(declare-fun x2266 () Int)
+(declare-fun x2267 () Int)
+(declare-fun x2268 () Int)
+(declare-fun x2269 () Int)
+(declare-fun x2270 () Int)
+(declare-fun x2271 () Int)
+(declare-fun x2272 () Int)
+(declare-fun x2273 () Int)
+(declare-fun x2274 () Int)
+(declare-fun x2275 () Int)
+(declare-fun x2276 () Int)
+(declare-fun x2277 () Int)
+(declare-fun x2278 () Int)
+(declare-fun x2279 () Int)
+(declare-fun x2280 () Int)
+(declare-fun x2281 () Int)
+(declare-fun x2282 () Int)
+(declare-fun x2283 () Int)
+(declare-fun x2284 () Int)
+(declare-fun x2285 () Int)
+(declare-fun x2286 () Int)
+(declare-fun x2287 () Int)
+(declare-fun x2288 () Int)
+(declare-fun x2289 () Int)
+(declare-fun x2290 () Int)
+(declare-fun x2291 () Int)
+(declare-fun x2292 () Int)
+(declare-fun x2293 () Int)
+(declare-fun x2294 () Int)
+(declare-fun x2295 () Int)
+(declare-fun x2296 () Int)
+(declare-fun x2297 () Int)
+(declare-fun x2298 () Int)
+(declare-fun x2299 () Int)
+(declare-fun x2300 () Int)
+(declare-fun x2301 () Int)
+(declare-fun x2302 () Int)
+(declare-fun x2303 () Int)
+(declare-fun x2304 () Int)
+(declare-fun x2305 () Int)
+(declare-fun x2306 () Int)
+(declare-fun x2307 () Int)
+(declare-fun x2308 () Int)
+(declare-fun x2309 () Int)
+(declare-fun x2310 () Int)
+(declare-fun x2311 () Int)
+(declare-fun x2312 () Int)
+(declare-fun x2313 () Int)
+(declare-fun x2314 () Int)
+(declare-fun x2315 () Int)
+(declare-fun x2316 () Int)
+(declare-fun x2317 () Int)
+(declare-fun x2318 () Int)
+(declare-fun x2319 () Int)
+(declare-fun x2320 () Int)
+(declare-fun x2321 () Int)
+(declare-fun x2322 () Int)
+(declare-fun x2323 () Int)
+(declare-fun x2324 () Int)
+(declare-fun x2325 () Int)
+(declare-fun x2326 () Int)
+(declare-fun x2327 () Int)
+(declare-fun x2328 () Int)
+(declare-fun x2329 () Int)
+(declare-fun x2330 () Int)
+(declare-fun x2331 () Int)
+(declare-fun x2332 () Int)
+(declare-fun x2333 () Int)
+(declare-fun x2334 () Int)
+(declare-fun x2335 () Int)
+(declare-fun x2336 () Int)
+(declare-fun x2337 () Int)
+(declare-fun x2338 () Int)
+(declare-fun x2339 () Int)
+(declare-fun x2340 () Int)
+(declare-fun x2341 () Int)
+(declare-fun x2342 () Int)
+(declare-fun x2343 () Int)
+(declare-fun x2344 () Int)
+(declare-fun x2345 () Int)
+(declare-fun x2346 () Int)
+(declare-fun x2347 () Int)
+(declare-fun x2348 () Int)
+(declare-fun x2349 () Int)
+(declare-fun x2350 () Int)
+(declare-fun x2351 () Int)
+(declare-fun x2352 () Int)
+(declare-fun x2353 () Int)
+(declare-fun x2354 () Int)
+(declare-fun x2355 () Int)
+(declare-fun x2356 () Int)
+(declare-fun x2357 () Int)
+(declare-fun x2358 () Int)
+(declare-fun x2359 () Int)
+(declare-fun x2360 () Int)
+(declare-fun x2361 () Int)
+(declare-fun x2362 () Int)
+(declare-fun x2363 () Int)
+(declare-fun x2364 () Int)
+(declare-fun x2365 () Int)
+(declare-fun x2366 () Int)
+(declare-fun x2367 () Int)
+(declare-fun x2368 () Int)
+(declare-fun x2369 () Int)
+(declare-fun x2370 () Int)
+(declare-fun x2371 () Int)
+(declare-fun x2372 () Int)
+(declare-fun x2373 () Int)
+(declare-fun x2374 () Int)
+(declare-fun x2375 () Int)
+(declare-fun x2376 () Int)
+(declare-fun x2377 () Int)
+(declare-fun x2378 () Int)
+(declare-fun x2379 () Int)
+(declare-fun x2380 () Int)
+(declare-fun x2381 () Int)
+(declare-fun x2382 () Int)
+(declare-fun x2383 () Int)
+(declare-fun x2384 () Int)
+(declare-fun x2385 () Int)
+(declare-fun x2386 () Int)
+(declare-fun x2387 () Int)
+(declare-fun x2388 () Int)
+(declare-fun x2389 () Int)
+(declare-fun x2390 () Int)
+(declare-fun x2391 () Int)
+(declare-fun x2392 () Int)
+(declare-fun x2393 () Int)
+(declare-fun x2394 () Int)
+(declare-fun x2395 () Int)
+(declare-fun x2396 () Int)
+(declare-fun x2397 () Int)
+(declare-fun x2398 () Int)
+(declare-fun x2399 () Int)
+(declare-fun x2400 () Int)
+(declare-fun x2401 () Int)
+(declare-fun x2402 () Int)
+(declare-fun x2403 () Int)
+(declare-fun x2404 () Int)
+(declare-fun x2405 () Int)
+(declare-fun x2406 () Int)
+(declare-fun x2407 () Int)
+(declare-fun x2408 () Int)
+(declare-fun x2409 () Int)
+(declare-fun x2410 () Int)
+(declare-fun x2411 () Int)
+(declare-fun x2412 () Int)
+(declare-fun x2413 () Int)
+(declare-fun x2414 () Int)
+(declare-fun x2415 () Int)
+(declare-fun x2416 () Int)
+(declare-fun x2417 () Int)
+(declare-fun x2418 () Int)
+(declare-fun x2419 () Int)
+(declare-fun x2420 () Int)
+(declare-fun x2421 () Int)
+(declare-fun x2422 () Int)
+(declare-fun x2423 () Int)
+(declare-fun x2424 () Int)
+(declare-fun x2425 () Int)
+(declare-fun x2426 () Int)
+(declare-fun x2427 () Int)
+(declare-fun x2428 () Int)
+(declare-fun x2429 () Int)
+(declare-fun x2430 () Int)
+(declare-fun x2431 () Int)
+(declare-fun x2432 () Int)
+(declare-fun x2433 () Int)
+(declare-fun x2434 () Int)
+(declare-fun x2435 () Int)
+(declare-fun x2436 () Int)
+(declare-fun x2437 () Int)
+(declare-fun x2438 () Int)
+(declare-fun x2439 () Int)
+(declare-fun x2440 () Int)
+(declare-fun x2441 () Int)
+(declare-fun x2442 () Int)
+(declare-fun x2443 () Int)
+(declare-fun x2444 () Int)
+(declare-fun x2445 () Int)
+(declare-fun x2446 () Int)
+(declare-fun x2447 () Int)
+(declare-fun x2448 () Int)
+(declare-fun x2449 () Int)
+(declare-fun x2450 () Int)
+(declare-fun x2451 () Int)
+(declare-fun x2452 () Int)
+(declare-fun x2453 () Int)
+(declare-fun x2454 () Int)
+(declare-fun x2455 () Int)
+(declare-fun x2456 () Int)
+(declare-fun x2457 () Int)
+(declare-fun x2458 () Int)
+(declare-fun x2459 () Int)
+(declare-fun x2460 () Int)
+(declare-fun x2461 () Int)
+(declare-fun x2462 () Int)
+(declare-fun x2463 () Int)
+(declare-fun x2464 () Int)
+(declare-fun x2465 () Int)
+(declare-fun x2466 () Int)
+(declare-fun x2467 () Int)
+(declare-fun x2468 () Int)
+(declare-fun x2469 () Int)
+(declare-fun x2470 () Int)
+(declare-fun x2471 () Int)
+(declare-fun x2472 () Int)
+(declare-fun x2473 () Int)
+(declare-fun x2474 () Int)
+(declare-fun x2475 () Int)
+(declare-fun x2476 () Int)
+(declare-fun x2477 () Int)
+(declare-fun x2478 () Int)
+(declare-fun x2479 () Int)
+(declare-fun x2480 () Int)
+(declare-fun x2481 () Int)
+(declare-fun x2482 () Int)
+(declare-fun x2483 () Int)
+(declare-fun x2484 () Int)
+(declare-fun x2485 () Int)
+(declare-fun x2486 () Int)
+(declare-fun x2487 () Int)
+(declare-fun x2488 () Int)
+(declare-fun x2489 () Int)
+(declare-fun x2490 () Int)
+(declare-fun x2491 () Int)
+(declare-fun x2492 () Int)
+(declare-fun x2493 () Int)
+(declare-fun x2494 () Int)
+(declare-fun x2495 () Int)
+(declare-fun x2496 () Int)
+(declare-fun x2497 () Int)
+(declare-fun x2498 () Int)
+(declare-fun x2499 () Int)
+(declare-fun x2500 () Int)
+(declare-fun x2501 () Int)
+(declare-fun x2502 () Int)
+(declare-fun x2503 () Int)
+(declare-fun x2504 () Int)
+(declare-fun x2505 () Int)
+(declare-fun x2506 () Int)
+(declare-fun x2507 () Int)
+(declare-fun x2508 () Int)
+(declare-fun x2509 () Int)
+(declare-fun x2510 () Int)
+(declare-fun x2511 () Int)
+(declare-fun x2512 () Int)
+(declare-fun x2513 () Int)
+(declare-fun x2514 () Int)
+(declare-fun x2515 () Int)
+(declare-fun x2516 () Int)
+(declare-fun x2517 () Int)
+(declare-fun x2518 () Int)
+(declare-fun x2519 () Int)
+(declare-fun x2520 () Int)
+(declare-fun x2521 () Int)
+(declare-fun x2522 () Int)
+(declare-fun x2523 () Int)
+(declare-fun x2524 () Int)
+(declare-fun x2525 () Int)
+(declare-fun x2526 () Int)
+(declare-fun x2527 () Int)
+(declare-fun x2528 () Int)
+(declare-fun x2529 () Int)
+(declare-fun x2530 () Int)
+(declare-fun x2531 () Int)
+(declare-fun x2532 () Int)
+(declare-fun x2533 () Int)
+(declare-fun x2534 () Int)
+(declare-fun x2535 () Int)
+(declare-fun x2536 () Int)
+(declare-fun x2537 () Int)
+(declare-fun x2538 () Int)
+(declare-fun x2539 () Int)
+(declare-fun x2540 () Int)
+(declare-fun x2541 () Int)
+(declare-fun x2542 () Int)
+(declare-fun x2543 () Int)
+(declare-fun x2544 () Int)
+(declare-fun x2545 () Int)
+(declare-fun x2546 () Int)
+(declare-fun x2547 () Int)
+(declare-fun x2548 () Int)
+(declare-fun x2549 () Int)
+(declare-fun x2550 () Int)
+(declare-fun x2551 () Int)
+(declare-fun x2552 () Int)
+(declare-fun x2553 () Int)
+(declare-fun x2554 () Int)
+(declare-fun x2555 () Int)
+(declare-fun x2556 () Int)
+(declare-fun x2557 () Int)
+(declare-fun x2558 () Int)
+(declare-fun x2559 () Int)
+(declare-fun x2560 () Int)
+(declare-fun x2561 () Int)
+(declare-fun x2562 () Int)
+(declare-fun x2563 () Int)
+(declare-fun x2564 () Int)
+(declare-fun x2565 () Int)
+(declare-fun x2566 () Int)
+(declare-fun x2567 () Int)
+(declare-fun x2568 () Int)
+(declare-fun x2569 () Int)
+(declare-fun x2570 () Int)
+(declare-fun x2571 () Int)
+(declare-fun x2572 () Int)
+(declare-fun x2573 () Int)
+(declare-fun x2574 () Int)
+(declare-fun x2575 () Int)
+(declare-fun x2576 () Int)
+(declare-fun x2577 () Int)
+(declare-fun x2578 () Int)
+(declare-fun x2579 () Int)
+(declare-fun x2580 () Int)
+(declare-fun x2581 () Int)
+(declare-fun x2582 () Int)
+(declare-fun x2583 () Int)
+(declare-fun x2584 () Int)
+(declare-fun x2585 () Int)
+(declare-fun x2586 () Int)
+(declare-fun x2587 () Int)
+(declare-fun x2588 () Int)
+(declare-fun x2589 () Int)
+(declare-fun x2590 () Int)
+(declare-fun x2591 () Int)
+(declare-fun x2592 () Int)
+(declare-fun x2593 () Int)
+(declare-fun x2594 () Int)
+(declare-fun x2595 () Int)
+(declare-fun x2596 () Int)
+(declare-fun x2597 () Int)
+(declare-fun x2598 () Int)
+(declare-fun x2599 () Int)
+(declare-fun x2600 () Int)
+(declare-fun x2601 () Int)
+(declare-fun x2602 () Int)
+(declare-fun x2603 () Int)
+(declare-fun x2604 () Int)
+(declare-fun x2605 () Int)
+(declare-fun x2606 () Int)
+(declare-fun x2607 () Int)
+(declare-fun x2608 () Int)
+(declare-fun x2609 () Int)
+(declare-fun x2610 () Int)
+(declare-fun x2611 () Int)
+(declare-fun x2612 () Int)
+(declare-fun x2613 () Int)
+(declare-fun x2614 () Int)
+(declare-fun x2615 () Int)
+(declare-fun x2616 () Int)
+(declare-fun x2617 () Int)
+(declare-fun x2618 () Int)
+(declare-fun x2619 () Int)
+(declare-fun x2620 () Int)
+(declare-fun x2621 () Int)
+(declare-fun x2622 () Int)
+(declare-fun x2623 () Int)
+(declare-fun x2624 () Int)
+(declare-fun x2625 () Int)
+(declare-fun x2626 () Int)
+(declare-fun x2627 () Int)
+(declare-fun x2628 () Int)
+(declare-fun x2629 () Int)
+(declare-fun x2630 () Int)
+(declare-fun x2631 () Int)
+(declare-fun x2632 () Int)
+(declare-fun x2633 () Int)
+(declare-fun x2634 () Int)
+(declare-fun x2635 () Int)
+(declare-fun x2636 () Int)
+(declare-fun x2637 () Int)
+(declare-fun x2638 () Int)
+(declare-fun x2639 () Int)
+(declare-fun x2640 () Int)
+(declare-fun x2641 () Int)
+(declare-fun x2642 () Int)
+(declare-fun x2643 () Int)
+(declare-fun x2644 () Int)
+(declare-fun x2645 () Int)
+(declare-fun x2646 () Int)
+(declare-fun x2647 () Int)
+(declare-fun x2648 () Int)
+(declare-fun x2649 () Int)
+(declare-fun x2650 () Int)
+(declare-fun x2651 () Int)
+(declare-fun x2652 () Int)
+(declare-fun x2653 () Int)
+(declare-fun x2654 () Int)
+(declare-fun x2655 () Int)
+(declare-fun x2656 () Int)
+(declare-fun x2657 () Int)
+(declare-fun x2658 () Int)
+(declare-fun x2659 () Int)
+(declare-fun x2660 () Int)
+(declare-fun x2661 () Int)
+(declare-fun x2662 () Int)
+(declare-fun x2663 () Int)
+(declare-fun x2664 () Int)
+(declare-fun x2665 () Int)
+(declare-fun x2666 () Int)
+(declare-fun x2667 () Int)
+(declare-fun x2668 () Int)
+(declare-fun x2669 () Int)
+(declare-fun x2670 () Int)
+(declare-fun x2671 () Int)
+(declare-fun x2672 () Int)
+(declare-fun x2673 () Int)
+(declare-fun x2674 () Int)
+(declare-fun x2675 () Int)
+(declare-fun x2676 () Int)
+(declare-fun x2677 () Int)
+(declare-fun x2678 () Int)
+(declare-fun x2679 () Int)
+(declare-fun x2680 () Int)
+(declare-fun x2681 () Int)
+(declare-fun x2682 () Int)
+(declare-fun x2683 () Int)
+(declare-fun x2684 () Int)
+(declare-fun x2685 () Int)
+(declare-fun x2686 () Int)
+(declare-fun x2687 () Int)
+(declare-fun x2688 () Int)
+(declare-fun x2689 () Int)
+(declare-fun x2690 () Int)
+(declare-fun x2691 () Int)
+(declare-fun x2692 () Int)
+(declare-fun x2693 () Int)
+(declare-fun x2694 () Int)
+(declare-fun x2695 () Int)
+(declare-fun x2696 () Int)
+(declare-fun x2697 () Int)
+(declare-fun x2698 () Int)
+(declare-fun x2699 () Int)
+(declare-fun x2700 () Int)
+(declare-fun x2701 () Int)
+(declare-fun x2702 () Int)
+(declare-fun x2703 () Int)
+(declare-fun x2704 () Int)
+(declare-fun x2705 () Int)
+(declare-fun x2706 () Int)
+(declare-fun x2707 () Int)
+(declare-fun x2708 () Int)
+(declare-fun x2709 () Int)
+(declare-fun x2710 () Int)
+(declare-fun x2711 () Int)
+(declare-fun x2712 () Int)
+(declare-fun x2713 () Int)
+(declare-fun x2714 () Int)
+(declare-fun x2715 () Int)
+(declare-fun x2716 () Int)
+(declare-fun x2717 () Int)
+(declare-fun x2718 () Int)
+(declare-fun x2719 () Int)
+(declare-fun x2720 () Int)
+(declare-fun x2721 () Int)
+(declare-fun x2722 () Int)
+(declare-fun x2723 () Int)
+(declare-fun x2724 () Int)
+(declare-fun x2725 () Int)
+(declare-fun x2726 () Int)
+(declare-fun x2727 () Int)
+(declare-fun x2728 () Int)
+(assert (>= (* 1 x113) 0))
+(assert (>= (* (- 1) x113) (- 1)))
+(assert (>= (* 1 x114) 0))
+(assert (>= (* (- 1) x114) (- 1)))
+(assert (>= (* 1 x115) 0))
+(assert (>= (* (- 1) x115) (- 1)))
+(assert (>= (* 1 x116) 0))
+(assert (>= (* (- 1) x116) (- 1)))
+(assert (>= (* 1 x117) 0))
+(assert (>= (* (- 1) x117) (- 1)))
+(assert (>= (* 1 x118) 0))
+(assert (>= (* (- 1) x118) (- 1)))
+(assert (>= (* 1 x119) 0))
+(assert (>= (* (- 1) x119) (- 1)))
+(assert (>= (* 1 x120) 0))
+(assert (>= (* (- 1) x120) (- 1)))
+(assert (>= (* 1 x121) 0))
+(assert (>= (* (- 1) x121) (- 1)))
+(assert (>= (* 1 x122) 0))
+(assert (>= (* (- 1) x122) (- 1)))
+(assert (>= (* 1 x123) 0))
+(assert (>= (* (- 1) x123) (- 1)))
+(assert (>= (* 1 x124) 0))
+(assert (>= (* (- 1) x124) (- 1)))
+(assert (>= (* 1 x125) 0))
+(assert (>= (* (- 1) x125) (- 1)))
+(assert (>= (* 1 x126) 0))
+(assert (>= (* (- 1) x126) (- 1)))
+(assert (>= (* 1 x127) 0))
+(assert (>= (* (- 1) x127) (- 1)))
+(assert (>= (* 1 x128) 0))
+(assert (>= (* (- 1) x128) (- 1)))
+(assert (>= (* 1 x129) 0))
+(assert (>= (* (- 1) x129) (- 1)))
+(assert (>= (* 1 x130) 0))
+(assert (>= (* (- 1) x130) (- 1)))
+(assert (>= (* 1 x131) 0))
+(assert (>= (* (- 1) x131) (- 1)))
+(assert (>= (* 1 x132) 0))
+(assert (>= (* (- 1) x132) (- 1)))
+(assert (>= (* 1 x133) 0))
+(assert (>= (* (- 1) x133) (- 1)))
+(assert (>= (* 1 x134) 0))
+(assert (>= (* (- 1) x134) (- 1)))
+(assert (>= (* 1 x135) 0))
+(assert (>= (* (- 1) x135) (- 1)))
+(assert (>= (* 1 x136) 0))
+(assert (>= (* (- 1) x136) (- 1)))
+(assert (>= (* 1 x137) 0))
+(assert (>= (* (- 1) x137) (- 1)))
+(assert (>= (* 1 x138) 0))
+(assert (>= (* (- 1) x138) (- 1)))
+(assert (>= (* 1 x139) 0))
+(assert (>= (* (- 1) x139) (- 1)))
+(assert (>= (* 1 x140) 0))
+(assert (>= (* (- 1) x140) (- 1)))
+(assert (>= (* 1 x141) 0))
+(assert (>= (* (- 1) x141) (- 1)))
+(assert (>= (* 1 x142) 0))
+(assert (>= (* (- 1) x142) (- 1)))
+(assert (>= (* 1 x143) 0))
+(assert (>= (* (- 1) x143) (- 1)))
+(assert (>= (* 1 x144) 0))
+(assert (>= (* (- 1) x144) (- 1)))
+(assert (>= (* 1 x145) 0))
+(assert (>= (* (- 1) x145) (- 1)))
+(assert (>= (* 1 x146) 0))
+(assert (>= (* (- 1) x146) (- 1)))
+(assert (>= (* 1 x147) 0))
+(assert (>= (* (- 1) x147) (- 1)))
+(assert (>= (* 1 x148) 0))
+(assert (>= (* (- 1) x148) (- 1)))
+(assert (>= (* 1 x149) 0))
+(assert (>= (* (- 1) x149) (- 1)))
+(assert (>= (* 1 x150) 0))
+(assert (>= (* (- 1) x150) (- 1)))
+(assert (>= (* 1 x151) 0))
+(assert (>= (* (- 1) x151) (- 1)))
+(assert (>= (* 1 x152) 0))
+(assert (>= (* (- 1) x152) (- 1)))
+(assert (>= (* 1 x153) 0))
+(assert (>= (* (- 1) x153) (- 1)))
+(assert (>= (* 1 x154) 0))
+(assert (>= (* (- 1) x154) (- 1)))
+(assert (>= (* 1 x155) 0))
+(assert (>= (* (- 1) x155) (- 1)))
+(assert (>= (* 1 x156) 0))
+(assert (>= (* (- 1) x156) (- 1)))
+(assert (>= (* 1 x157) 0))
+(assert (>= (* (- 1) x157) (- 1)))
+(assert (>= (* 1 x158) 0))
+(assert (>= (* (- 1) x158) (- 1)))
+(assert (>= (* 1 x159) 0))
+(assert (>= (* (- 1) x159) (- 1)))
+(assert (>= (* 1 x160) 0))
+(assert (>= (* (- 1) x160) (- 1)))
+(assert (>= (* 1 x161) 0))
+(assert (>= (* (- 1) x161) (- 1)))
+(assert (>= (* 1 x162) 0))
+(assert (>= (* (- 1) x162) (- 1)))
+(assert (>= (* 1 x163) 0))
+(assert (>= (* (- 1) x163) (- 1)))
+(assert (>= (* 1 x164) 0))
+(assert (>= (* (- 1) x164) (- 1)))
+(assert (>= (* 1 x165) 0))
+(assert (>= (* (- 1) x165) (- 1)))
+(assert (>= (* 1 x166) 0))
+(assert (>= (* (- 1) x166) (- 1)))
+(assert (>= (* 1 x167) 0))
+(assert (>= (* (- 1) x167) (- 1)))
+(assert (>= (* 1 x168) 0))
+(assert (>= (* (- 1) x168) (- 1)))
+(assert (>= (* 1 x169) 0))
+(assert (>= (* (- 1) x169) (- 1)))
+(assert (>= (* 1 x170) 0))
+(assert (>= (* (- 1) x170) (- 1)))
+(assert (>= (* 1 x171) 0))
+(assert (>= (* (- 1) x171) (- 1)))
+(assert (>= (* 1 x172) 0))
+(assert (>= (* (- 1) x172) (- 1)))
+(assert (>= (* 1 x173) 0))
+(assert (>= (* (- 1) x173) (- 1)))
+(assert (>= (* 1 x174) 0))
+(assert (>= (* (- 1) x174) (- 1)))
+(assert (>= (* 1 x175) 0))
+(assert (>= (* (- 1) x175) (- 1)))
+(assert (>= (* 1 x176) 0))
+(assert (>= (* (- 1) x176) (- 1)))
+(assert (>= (* 1 x177) 0))
+(assert (>= (* (- 1) x177) (- 1)))
+(assert (>= (* 1 x178) 0))
+(assert (>= (* (- 1) x178) (- 1)))
+(assert (>= (* 1 x179) 0))
+(assert (>= (* (- 1) x179) (- 1)))
+(assert (>= (* 1 x180) 0))
+(assert (>= (* (- 1) x180) (- 1)))
+(assert (>= (* 1 x181) 0))
+(assert (>= (* (- 1) x181) (- 1)))
+(assert (>= (* 1 x182) 0))
+(assert (>= (* (- 1) x182) (- 1)))
+(assert (>= (* 1 x183) 0))
+(assert (>= (* (- 1) x183) (- 1)))
+(assert (>= (* 1 x184) 0))
+(assert (>= (* (- 1) x184) (- 1)))
+(assert (>= (* 1 x185) 0))
+(assert (>= (* (- 1) x185) (- 1)))
+(assert (>= (* 1 x186) 0))
+(assert (>= (* (- 1) x186) (- 1)))
+(assert (>= (* 1 x187) 0))
+(assert (>= (* (- 1) x187) (- 1)))
+(assert (>= (* 1 x188) 0))
+(assert (>= (* (- 1) x188) (- 1)))
+(assert (>= (* 1 x189) 0))
+(assert (>= (* (- 1) x189) (- 1)))
+(assert (>= (* 1 x190) 0))
+(assert (>= (* (- 1) x190) (- 1)))
+(assert (>= (* 1 x191) 0))
+(assert (>= (* (- 1) x191) (- 1)))
+(assert (>= (* 1 x192) 0))
+(assert (>= (* (- 1) x192) (- 1)))
+(assert (>= (* 1 x193) 0))
+(assert (>= (* (- 1) x193) (- 1)))
+(assert (>= (* 1 x194) 0))
+(assert (>= (* (- 1) x194) (- 1)))
+(assert (>= (* 1 x195) 0))
+(assert (>= (* (- 1) x195) (- 1)))
+(assert (>= (* 1 x196) 0))
+(assert (>= (* (- 1) x196) (- 1)))
+(assert (>= (* 1 x197) 0))
+(assert (>= (* (- 1) x197) (- 1)))
+(assert (>= (* 1 x198) 0))
+(assert (>= (* (- 1) x198) (- 1)))
+(assert (>= (* 1 x199) 0))
+(assert (>= (* (- 1) x199) (- 1)))
+(assert (>= (* 1 x200) 0))
+(assert (>= (* (- 1) x200) (- 1)))
+(assert (>= (* 1 x201) 0))
+(assert (>= (* (- 1) x201) (- 1)))
+(assert (>= (* 1 x202) 0))
+(assert (>= (* (- 1) x202) (- 1)))
+(assert (>= (* 1 x203) 0))
+(assert (>= (* (- 1) x203) (- 1)))
+(assert (>= (* 1 x204) 0))
+(assert (>= (* (- 1) x204) (- 1)))
+(assert (>= (* 1 x205) 0))
+(assert (>= (* (- 1) x205) (- 1)))
+(assert (>= (* 1 x206) 0))
+(assert (>= (* (- 1) x206) (- 1)))
+(assert (>= (* 1 x207) 0))
+(assert (>= (* (- 1) x207) (- 1)))
+(assert (>= (* 1 x208) 0))
+(assert (>= (* (- 1) x208) (- 1)))
+(assert (>= (* 1 x209) 0))
+(assert (>= (* (- 1) x209) (- 1)))
+(assert (>= (* 1 x210) 0))
+(assert (>= (* (- 1) x210) (- 1)))
+(assert (>= (* 1 x211) 0))
+(assert (>= (* (- 1) x211) (- 1)))
+(assert (>= (* 1 x212) 0))
+(assert (>= (* (- 1) x212) (- 1)))
+(assert (>= (+ (* 1 x113) (* (- 1) x164)) 0))
+(check-sat)
+(exit)