Fix incremental bug in symmetry breaker.

Thanks to Christoph Sticksel for reporting this.

diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp
index fcb6c3cd5b9d59a873416c6a10f14f98387adfa1..f5d7f923590071c6daba6a3e1b1300c1e190e025 100644 (file)
--- a/src/theory/uf/symmetry_breaker.cpp
+++ b/src/theory/uf/symmetry_breaker.cpp
@@ -52,6 +52,8 @@ namespace CVC4 {
 namespace theory {
 namespace uf {
 
+using namespace ::CVC4::context;
+
 SymmetryBreaker::Template::Template() :
   d_template(),
   d_sets(),
@@ -165,7 +167,10 @@ void SymmetryBreaker::Template::reset() {
   d_reps.clear();
 }
 
-SymmetryBreaker::SymmetryBreaker() :
+SymmetryBreaker::SymmetryBreaker(context::Context* context) :
+  ContextNotifyObj(context),
+  d_assertionsToRerun(context),
+  d_rerunningAssertions(false),
   d_phi(),
   d_phiSet(),
   d_permutations(),
@@ -175,6 +180,31 @@ SymmetryBreaker::SymmetryBreaker() :
   d_termEqs() {
 }
 
+class SBGuard {
+  bool& d_ref;
+  bool d_old;
+public:
+  SBGuard(bool& b) : d_ref(b), d_old(b) {}
+  ~SBGuard() { Debug("uf") << "reset to " << d_old << std::endl; d_ref = d_old; }
+};/* class SBGuard */
+
+void SymmetryBreaker::rerunAssertionsIfNecessary() {
+  if(d_rerunningAssertions || !d_phi.empty() || d_assertionsToRerun.empty()) {
+    return;
+  }
+
+  SBGuard g(d_rerunningAssertions);
+  d_rerunningAssertions = true;
+
+  Debug("ufsymm") << "UFSYMM: rerunning assertions..." << std::endl;
+  for(CDList<Node>::const_iterator i = d_assertionsToRerun.begin();
+      i != d_assertionsToRerun.end();
+      ++i) {
+    assertFormula(*i);
+  }
+  Debug("ufsymm") << "UFSYMM: DONE rerunning assertions..." << std::endl;
+}
+
 Node SymmetryBreaker::norm(TNode phi) {
   Node n = Rewriter::rewrite(phi);
   return normInternal(n);
@@ -254,6 +284,10 @@ Node SymmetryBreaker::normInternal(TNode n) {
 }
 
 void SymmetryBreaker::assertFormula(TNode phi) {
+  rerunAssertionsIfNecessary();
+  if(!d_rerunningAssertions) {
+    d_assertionsToRerun.push_back(phi);
+  }
   // use d_phi, put into d_permutations
   Debug("ufsymm") << "UFSYMM assertFormula(): phi is " << phi << endl;
   d_phi.push_back(phi);
@@ -322,6 +356,7 @@ void SymmetryBreaker::clear() {
 }
 
 void SymmetryBreaker::apply(std::vector<Node>& newClauses) {
+  rerunAssertionsIfNecessary();
   guessPermutations();
   Debug("ufsymm") << "UFSYMM =====================================================" << endl
                   << "UFSYMM have " << d_permutations.size() << " permutation sets" << endl;

diff --git a/src/theory/uf/symmetry_breaker.h b/src/theory/uf/symmetry_breaker.h
index cf54b62c2137e00bd6ef821b17605406049a4657..d04da048a131a1e04b381e0a39168d276005a5b0 100644 (file)
--- a/src/theory/uf/symmetry_breaker.h
+++ b/src/theory/uf/symmetry_breaker.h
@@ -50,13 +50,15 @@
 
 #include "expr/node.h"
 #include "expr/node_builder.h"
+#include "context/context.h"
+#include "context/cdlist.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
 namespace theory {
 namespace uf {
 
-class SymmetryBreaker {
+class SymmetryBreaker : public context::ContextNotifyObj {
 
   class Template {
     Node d_template;
@@ -92,6 +94,19 @@ public:
 
 private:
 
+  /**
+   * This class wasn't initially built to be incremental.  It should
+   * be attached to a UserContext so that it clears everything when
+   * a pop occurs.  This "assertionsToRerun" is a set of assertions to
+   * feed back through assertFormula() when we started getting things
+   * again.  It's not just a matter of effectiveness, but also soundness;
+   * if some assertions (still in scope) are not seen by a symmetry-breaking
+   * round, then some symmetries that don't actually exist might be broken,
+   * leading to unsound results!
+   */
+  context::CDList<Node> d_assertionsToRerun;
+  bool d_rerunningAssertions;
+
   std::vector<Node> d_phi;
   std::set<TNode> d_phiSet;
   Permutations d_permutations;
@@ -101,6 +116,7 @@ private:
   TermEqs d_termEqs;
 
   void clear();
+  void rerunAssertionsIfNecessary();
 
   void guessPermutations();
   bool invariantByPermutations(const Permutation& p);
@@ -140,9 +156,17 @@ private:
                  d_initNormalizationTimer,
                  "theory::uf::symmetry_breaker::timers::initNormalization");
 
+protected:
+
+  void contextNotifyPop() {
+    Debug("ufsymm") << "UFSYMM: clearing state due to pop" << std::endl;
+    clear();
+  }
+
 public:
 
-  SymmetryBreaker();
+  SymmetryBreaker(context::Context* context);
+  ~SymmetryBreaker() throw() {}
   void assertFormula(TNode phi);
   void apply(std::vector<Node>& newClauses);
 

diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 69a9633605311ea479c289d1599bd36a1030343b..41935984f9e35ca4c2abdefe56812fa9c63cb75b 100644 (file)
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -38,7 +38,8 @@ TheoryUF::TheoryUF(context::Context* c, context::UserContext* u, OutputChannel&
   d_conflict(c, false),
   d_literalsToPropagate(c),
   d_literalsToPropagateIndex(c, 0),
-  d_functionsTerms(c)
+  d_functionsTerms(c),
+  d_symb(u)
 {
   // The kinds we are treating as function application in congruence
   d_equalityEngine.addFunctionKind(kind::APPLY_UF);

diff --git a/test/regress/regress0/GEO123+1.minimized.smt2 b/test/regress/regress0/GEO123+1.minimized.smt2
new file mode 100644 (file)
index 0000000..8cc1fa7
--- /dev/null
+++ b/test/regress/regress0/GEO123+1.minimized.smt2
@@ -0,0 +1,397 @@
+; COMMAND-LINE: --incremental
+; EXPECT: sat
+; EXPECT: sat
+; EXIT: 10
+;
+; This is a benchmark demonstrating a nasty incremental bug in the UF
+; symmetry breaker, now fixed.
+;
+(set-logic QF_UF)
+(declare-fun _substvar_29615_ () Bool)
+(declare-sort T 0)
+(declare-fun incident_o (T T) Bool)
+(declare-fun sK25 () T)
+(declare-fun sK26 () T)
+(declare-fun ordered_by (T T T) Bool)
+(declare-fun sK21 (T T) T)
+(declare-fun incident_c (T T) Bool)
+(declare-fun between_o (T T T T) Bool)
+(declare-fun start_point (T T) Bool)
+(declare-fun sK12 (T T) T)
+(declare-fun meet (T T T) Bool)
+(declare-fun end_point (T T) Bool)
+(declare-fun inner_point (T T) Bool)
+(declare-fun part_of (T T) Bool)
+(declare-fun open (T) Bool)
+(declare-fun sK22 (T T) T)
+(declare-fun sK19 (T) T)
+(declare-fun sum (T T) T)
+(declare-fun sK4 (T T T) T)
+(declare-fun sK2 (T T) T)
+(declare-fun sK3 (T T) T)
+(declare-fun sK0 (T T) T)
+(declare-fun sK1 (T T T) T)
+(declare-fun sK24 () T)
+(declare-fun iProver_c13 () T)
+(declare-fun iProver_c41 () T)
+(declare-fun iProver_c14 () T)
+(assert (incident_o sK26 sK24))
+(assert (not (ordered_by sK24 sK25 sK26)))
+(assert (not (= sK25 sK26)))
+(assert (start_point (sK19 sK24) sK24))
+(check-sat)
+(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK0 sK24 sK25))) (let ((_let_2 (sK21 _let_0 _let_1))) (let ((_let_3 (sK22 _let_0 _let_1))) (or (ordered_by _let_1 _let_2 _let_3) (ordered_by _let_0 _let_2 _let_3) (= _let_1 _let_0)))))))
+(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK0 iProver_c13 sK25))) (let ((_let_2 (sK21 _let_0 _let_1))) (let ((_let_3 (sK22 _let_0 _let_1))) (or (ordered_by _let_1 _let_2 _let_3) (ordered_by _let_0 _let_2 _let_3) (= _let_1 _let_0)))))))
+(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK12 sK24 sK25))) (let ((_let_2 (sK21 _let_1 _let_0))) (let ((_let_3 (sK22 _let_1 _let_0))) (or (ordered_by _let_0 _let_2 _let_3) (ordered_by _let_1 _let_2 _let_3) (= _let_0 _let_1)))))))
+(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK12 iProver_c13 sK25))) (let ((_let_2 (sK21 _let_1 _let_0))) (let ((_let_3 (sK22 _let_1 _let_0))) (or (ordered_by _let_0 _let_2 _let_3) (ordered_by _let_1 _let_2 _let_3) (= _let_0 _let_1)))))))
+(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK12 sK24 sK25))) (let ((_let_2 (sK21 _let_0 _let_1))) (let ((_let_3 (sK22 _let_0 _let_1))) (or (ordered_by _let_1 _let_2 _let_3) (ordered_by _let_0 _let_2 _let_3) (= _let_1 _let_0)))))))
+(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK12 iProver_c13 sK25))) (let ((_let_2 (sK21 _let_0 _let_1))) (let ((_let_3 (sK22 _let_0 _let_1))) (or (ordered_by _let_1 _let_2 _let_3) (ordered_by _let_0 _let_2 _let_3) (= _let_1 _let_0)))))))
+(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK0 sK24 sK25))) (let ((_let_2 (sK21 _let_1 _let_0))) (let ((_let_3 (sK22 _let_1 _let_0))) (or (ordered_by _let_0 _let_2 _let_3) (ordered_by _let_1 _let_2 _let_3) (= _let_0 _let_1)))))))
+(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK0 iProver_c13 sK25))) (let ((_let_2 (sK21 _let_1 _let_0))) (let ((_let_3 (sK22 _let_1 _let_0))) (or (ordered_by _let_0 _let_2 _let_3) (ordered_by _let_1 _let_2 _let_3) (= _let_0 _let_1)))))))
+(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK0 sK24 sK25))) (let ((_let_2 (sK12 _let_0 _let_1))) (or (= _let_1 _let_0) (incident_c _let_2 _let_1) (incident_c _let_2 _let_0))))))
+(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK0 iProver_c13 sK25))) (let ((_let_2 (sK12 _let_0 _let_1))) (or (= _let_1 _let_0) (incident_c _let_2 _let_1) (incident_c _let_2 _let_0))))))
+(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK12 sK24 sK25))) (let ((_let_2 (sK12 _let_1 _let_0))) (or (= _let_0 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 _let_1))))))
+(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK12 iProver_c13 sK25))) (let ((_let_2 (sK12 _let_1 _let_0))) (or (= _let_0 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 _let_1))))))
+(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK12 sK24 sK25))) (let ((_let_2 (sK12 _let_0 _let_1))) (or (= _let_1 _let_0) (incident_c _let_2 _let_1) (incident_c _let_2 _let_0))))))
+(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK12 iProver_c13 sK25))) (let ((_let_2 (sK12 _let_0 _let_1))) (or (= _let_1 _let_0) (incident_c _let_2 _let_1) (incident_c _let_2 _let_0))))))
+(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK0 sK24 sK25))) (let ((_let_2 (sK12 _let_1 _let_0))) (or (= _let_0 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 _let_1))))))
+(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK0 iProver_c13 sK25))) (let ((_let_2 (sK12 _let_1 _let_0))) (or (= _let_0 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 _let_1))))))
+(assert (let ((_let_0 (sK12 sK24 sK25))) (or (= sK25 sK24) (not (incident_c _let_0 sK25)) (not (incident_c _let_0 sK24)))))
+(assert (let ((_let_0 (sK12 iProver_c13 sK25))) (or (= sK25 iProver_c13) (not (incident_c _let_0 sK25)) (not (incident_c _let_0 iProver_c13)))))
+(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK0 sK24 sK25))) (or (= _let_1 _let_0) (not (part_of _let_0 _let_1)) (open _let_0)))))
+(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK0 iProver_c13 sK25))) (or (= _let_1 _let_0) (open _let_0) (not (part_of _let_0 _let_1))))))
+(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK12 sK24 sK25))) (or (= _let_0 _let_1) (not (part_of _let_1 _let_0)) (open _let_1)))))
+(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK12 iProver_c13 sK25))) (or (= _let_0 _let_1) (not (part_of _let_1 _let_0)) (open _let_1)))))
+(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK12 sK24 sK25))) (or (= _let_1 _let_0) (open _let_0) (not (part_of _let_0 _let_1))))))
+(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK12 iProver_c13 sK25))) (or (= _let_1 _let_0) (open _let_0) (not (part_of _let_0 _let_1))))))
+(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK0 sK24 sK25))) (or (= _let_0 _let_1) (not (part_of _let_1 _let_0)) (open _let_1)))))
+(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK0 iProver_c13 sK25))) (or (= _let_0 _let_1) (not (part_of _let_1 _let_0)) (open _let_1)))))
+(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (not (incident_c _let_0 sK24)) (not (meet sK24 sK25 sK24)) (end_point _let_0 sK25))))
+(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (end_point _let_0 sK25) (not (incident_c _let_0 iProver_c13)) (not (meet iProver_c14 sK25 iProver_c13)))))
+(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (not (incident_c _let_0 sK24)) (not (meet sK24 sK25 sK24)) (end_point _let_0 sK24))))
+(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (not (incident_c _let_0 iProver_c13)) (not (meet iProver_c14 sK25 iProver_c13)) (end_point _let_0 iProver_c13))))
+(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (not (incident_c _let_0 sK24)) (incident_c (sK4 sK24 sK25 _let_0) sK25) (meet _let_0 sK25 sK24))))
+(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (not (incident_c _let_0 iProver_c13)) (incident_c (sK4 iProver_c13 sK25 _let_0) sK25) (meet _let_0 sK25 iProver_c13))))
+(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (not (incident_c _let_0 sK24)) (meet _let_0 sK25 sK24) (incident_c (sK4 sK24 sK25 _let_0) sK24))))
+(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (not (incident_c _let_0 iProver_c13)) (meet _let_0 sK25 iProver_c13) (incident_c (sK4 iProver_c13 sK25 _let_0) iProver_c13))))
+(assert (let ((_let_0 (sK4 sK24 sK25 (sK12 sK26 sK25)))) (or (not (incident_c (sK12 sK26 sK25) sK25)) (not (incident_c (sK12 sK26 sK25) sK24)) (meet (sK12 sK26 sK25) sK25 sK24) (not (end_point _let_0 sK25)) (not (end_point _let_0 sK24)))))
+(assert (let ((_let_0 (sK4 iProver_c13 sK25 (sK12 sK26 sK25)))) (or (not (incident_c (sK12 sK26 sK25) sK25)) (not (incident_c (sK12 sK26 sK25) iProver_c13)) (meet (sK12 sK26 sK25) sK25 iProver_c13) (not (end_point _let_0 sK25)) (not (end_point _let_0 iProver_c13)))))
+(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (end_point _let_0 sK25) (inner_point _let_0 sK25))))
+(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (part_of sK25 sK24))) (or (not (part_of sK24 sK24)) (not (incident_c _let_0 sK25)) _let_1 (not _let_1) (part_of sK24 sK25) (not (incident_c _let_0 sK24)) (not (end_point _let_0 sK24))))))
+(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (part_of iProver_c13 iProver_c14)) (not (incident_c _let_0 sK25)) (part_of sK25 iProver_c13) (part_of iProver_c13 sK25) (not (incident_c _let_0 iProver_c13)) (not (part_of sK25 iProver_c14)) (not (end_point _let_0 iProver_c14)))))
+(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (end_point _let_0 sK25) (part_of (sK2 sK25 _let_0) sK25))))
+(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (end_point _let_0 sK25) (part_of (sK3 sK25 _let_0) sK25))))
+(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (end_point _let_0 sK25) (incident_c _let_0 (sK2 sK25 _let_0)))))
+(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (end_point _let_0 sK25) (incident_c _let_0 (sK3 sK25 _let_0)))))
+(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (end_point _let_0 sK25) (not (part_of (sK2 sK25 _let_0) (sK3 sK25 _let_0))))))
+(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (end_point _let_0 sK25) (not (part_of (sK3 sK25 _let_0) (sK2 sK25 _let_0))))))
+(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (incident_c _let_0 (sum sK25 sK24)))))
+(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (incident_c _let_0 (sum sK25 iProver_c13)))))
+(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (incident_c _let_0 (sum sK24 sK25)))))
+(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (incident_c _let_0 (sum iProver_c13 sK25)))))
+(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK1 sK24 sK24 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 sK24) (= (sum sK24 sK24) _let_0)))))
+(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0)))))
+(assert (let ((_let_0 (sK0 sK24 sK25))) (let ((_let_1 (sK1 sK24 sK24 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 sK24) (= (sum sK24 sK24) _let_0)))))
+(assert (let ((_let_0 (sK0 iProver_c41 sK25))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0)))))
+(assert (let ((_let_0 (sK12 sK24 sK25))) (let ((_let_1 (sK1 sK24 sK24 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 sK24) (= (sum sK24 sK24) _let_0)))))
+(assert (let ((_let_0 (sK12 iProver_c13 sK25))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0)))))
+(assert (let ((_let_0 (sK12 iProver_c41 sK25))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0)))))
+(assert (let ((_let_0 (sK0 iProver_c13 sK25))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0)))))
+(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (not (part_of sK25 sK24)) (incident_c _let_0 sK24))))
+(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (not (part_of sK25 iProver_c13)) (incident_c _let_0 iProver_c13))))
+(assert (or (part_of sK24 sK25) (not (incident_c (sK0 sK24 sK25) sK25))))
+(assert (or (part_of iProver_c13 sK25) (not (incident_c (sK0 iProver_c13 sK25) sK25))))
+(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK0 sK24 sK26))) (let ((_let_2 (sK21 _let_0 _let_1))) (let ((_let_3 (sK22 _let_0 _let_1))) (or (ordered_by _let_1 _let_2 _let_3) (ordered_by _let_0 _let_2 _let_3) (= _let_1 _let_0)))))))
+(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK0 iProver_c13 sK26))) (let ((_let_2 (sK21 _let_0 _let_1))) (let ((_let_3 (sK22 _let_0 _let_1))) (or (ordered_by _let_1 _let_2 _let_3) (ordered_by _let_0 _let_2 _let_3) (= _let_1 _let_0)))))))
+(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK12 sK24 sK26))) (let ((_let_2 (sK21 _let_1 _let_0))) (let ((_let_3 (sK22 _let_1 _let_0))) (or (ordered_by _let_0 _let_2 _let_3) (ordered_by _let_1 _let_2 _let_3) (= _let_0 _let_1)))))))
+(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK12 iProver_c13 sK26))) (let ((_let_2 (sK21 _let_1 _let_0))) (let ((_let_3 (sK22 _let_1 _let_0))) (or (ordered_by _let_0 _let_2 _let_3) (ordered_by _let_1 _let_2 _let_3) (= _let_0 _let_1)))))))
+(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK12 sK24 sK26))) (let ((_let_2 (sK21 _let_0 _let_1))) (let ((_let_3 (sK22 _let_0 _let_1))) (or (ordered_by _let_1 _let_2 _let_3) (ordered_by _let_0 _let_2 _let_3) (= _let_1 _let_0)))))))
+(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK12 iProver_c13 sK26))) (let ((_let_2 (sK21 _let_0 _let_1))) (let ((_let_3 (sK22 _let_0 _let_1))) (or (ordered_by _let_1 _let_2 _let_3) (ordered_by _let_0 _let_2 _let_3) (= _let_1 _let_0)))))))
+(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK0 sK24 sK26))) (let ((_let_2 (sK21 _let_1 _let_0))) (let ((_let_3 (sK22 _let_1 _let_0))) (or (ordered_by _let_0 _let_2 _let_3) (ordered_by _let_1 _let_2 _let_3) (= _let_0 _let_1)))))))
+(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK0 iProver_c13 sK26))) (let ((_let_2 (sK21 _let_1 _let_0))) (let ((_let_3 (sK22 _let_1 _let_0))) (or (ordered_by _let_0 _let_2 _let_3) (ordered_by _let_1 _let_2 _let_3) (= _let_0 _let_1)))))))
+(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK0 sK24 sK26))) (let ((_let_2 (sK12 _let_0 _let_1))) (or (= _let_1 _let_0) (incident_c _let_2 _let_1) (incident_c _let_2 _let_0))))))
+(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK0 iProver_c13 sK26))) (let ((_let_2 (sK12 _let_0 _let_1))) (or (= _let_1 _let_0) (incident_c _let_2 _let_1) (incident_c _let_2 _let_0))))))
+(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK12 sK24 sK26))) (let ((_let_2 (sK12 _let_1 _let_0))) (or (= _let_0 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 _let_1))))))
+(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK12 iProver_c13 sK26))) (let ((_let_2 (sK12 _let_1 _let_0))) (or (= _let_0 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 _let_1))))))
+(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK12 sK24 sK26))) (let ((_let_2 (sK12 _let_0 _let_1))) (or (= _let_1 _let_0) (incident_c _let_2 _let_1) (incident_c _let_2 _let_0))))))
+(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK12 iProver_c13 sK26))) (let ((_let_2 (sK12 _let_0 _let_1))) (or (= _let_1 _let_0) (incident_c _let_2 _let_1) (incident_c _let_2 _let_0))))))
+(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK0 sK24 sK26))) (let ((_let_2 (sK12 _let_1 _let_0))) (or (= _let_0 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 _let_1))))))
+(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK0 iProver_c13 sK26))) (let ((_let_2 (sK12 _let_1 _let_0))) (or (= _let_0 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 _let_1))))))
+(assert (let ((_let_0 (sK12 sK24 sK26))) (or (= sK26 sK24) (not (incident_c _let_0 sK26)) (not (incident_c _let_0 sK24)))))
+(assert (let ((_let_0 (sK12 iProver_c13 sK26))) (or (= sK26 iProver_c13) (not (incident_c _let_0 sK26)) (not (incident_c _let_0 iProver_c13)))))
+(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK0 sK24 sK26))) (or (= _let_1 _let_0) (not (part_of _let_0 _let_1)) (open _let_0)))))
+(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK0 iProver_c13 sK26))) (or (= _let_1 _let_0) (open _let_0) (not (part_of _let_0 _let_1))))))
+(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK12 sK24 sK26))) (or (= _let_0 _let_1) (not (part_of _let_1 _let_0)) (open _let_1)))))
+(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK12 iProver_c13 sK26))) (or (= _let_0 _let_1) (not (part_of _let_1 _let_0)) (open _let_1)))))
+(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK12 sK24 sK26))) (or (= _let_1 _let_0) (open _let_0) (not (part_of _let_0 _let_1))))))
+(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK12 iProver_c13 sK26))) (or (= _let_1 _let_0) (open _let_0) (not (part_of _let_0 _let_1))))))
+(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK0 sK24 sK26))) (or (= _let_0 _let_1) (not (part_of _let_1 _let_0)) (open _let_1)))))
+(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK0 iProver_c13 sK26))) (or (= _let_0 _let_1) (not (part_of _let_1 _let_0)) (open _let_1)))))
+(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (not (incident_c _let_0 sK24)) (not (meet sK24 sK26 sK24)) (end_point _let_0 sK26))))
+(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (end_point _let_0 sK26) (not (incident_c _let_0 iProver_c13)) (not (meet iProver_c14 sK26 iProver_c13)))))
+(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (not (incident_c _let_0 sK24)) (not (meet sK24 sK26 sK24)) (end_point _let_0 sK24))))
+(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (not (incident_c _let_0 iProver_c13)) (not (meet iProver_c14 sK26 iProver_c13)) (end_point _let_0 iProver_c13))))
+(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (not (incident_c _let_0 sK24)) (incident_c (sK4 sK24 sK26 _let_0) sK26) (meet _let_0 sK26 sK24))))
+(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (not (incident_c _let_0 iProver_c13)) (incident_c (sK4 iProver_c13 sK26 _let_0) sK26) (meet _let_0 sK26 iProver_c13))))
+(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (not (incident_c _let_0 sK24)) (meet _let_0 sK26 sK24) (incident_c (sK4 sK24 sK26 _let_0) sK24))))
+(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (not (incident_c _let_0 iProver_c13)) (meet _let_0 sK26 iProver_c13) (incident_c (sK4 iProver_c13 sK26 _let_0) iProver_c13))))
+(assert (let ((_let_0 (sK4 sK24 sK26 (sK12 sK25 sK26)))) (or (not (incident_c (sK12 sK25 sK26) sK26)) (not (incident_c (sK12 sK25 sK26) sK24)) (meet (sK12 sK25 sK26) sK26 sK24) (not (end_point _let_0 sK26)) (not (end_point _let_0 sK24)))))
+(assert (let ((_let_0 (sK4 iProver_c13 sK26 (sK12 sK25 sK26)))) (or (not (incident_c (sK12 sK25 sK26) sK26)) (not (incident_c (sK12 sK25 sK26) iProver_c13)) (meet (sK12 sK25 sK26) sK26 iProver_c13) (not (end_point _let_0 sK26)) (not (end_point _let_0 iProver_c13)))))
+(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (end_point _let_0 sK26) (inner_point _let_0 sK26))))
+(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (part_of sK26 sK24))) (or (not (part_of sK24 sK24)) (not (incident_c _let_0 sK26)) (part_of sK24 sK26) _let_1 (not _let_1) (not (incident_c _let_0 sK24)) (not (end_point _let_0 sK24))))))
+(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (part_of iProver_c13 iProver_c14)) (not (incident_c _let_0 sK26)) (part_of iProver_c13 sK26) (part_of sK26 iProver_c13) (not (incident_c _let_0 iProver_c13)) (not (part_of sK26 iProver_c14)) (not (end_point _let_0 iProver_c14)))))
+(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (end_point _let_0 sK26) (part_of (sK2 sK26 _let_0) sK26))))
+(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (end_point _let_0 sK26) (part_of (sK3 sK26 _let_0) sK26))))
+(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (end_point _let_0 sK26) (incident_c _let_0 (sK2 sK26 _let_0)))))
+(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (end_point _let_0 sK26) (incident_c _let_0 (sK3 sK26 _let_0)))))
+(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (end_point _let_0 sK26) (not (part_of (sK2 sK26 _let_0) (sK3 sK26 _let_0))))))
+(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (end_point _let_0 sK26) (not (part_of (sK3 sK26 _let_0) (sK2 sK26 _let_0))))))
+(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (incident_c _let_0 (sum sK26 sK24)))))
+(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (incident_c _let_0 (sum sK26 iProver_c13)))))
+(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (incident_c _let_0 (sum sK24 sK26)))))
+(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (incident_c _let_0 (sum iProver_c13 sK26)))))
+(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK1 sK24 sK24 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 sK24) (= (sum sK24 sK24) _let_0)))))
+(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0)))))
+(assert (let ((_let_0 (sK0 sK24 sK26))) (let ((_let_1 (sK1 sK24 sK24 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 sK24) (= (sum sK24 sK24) _let_0)))))
+(assert (let ((_let_0 (sK0 iProver_c41 sK26))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0)))))
+(assert (let ((_let_0 (sK12 sK24 sK26))) (let ((_let_1 (sK1 sK24 sK24 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 sK24) (= (sum sK24 sK24) _let_0)))))
+(assert (let ((_let_0 (sK12 iProver_c13 sK26))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0)))))
+(assert (let ((_let_0 (sK12 iProver_c41 sK26))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0)))))
+(assert (let ((_let_0 (sK0 iProver_c13 sK26))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0)))))
+(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (not (part_of sK26 sK24)) (incident_c _let_0 sK24))))
+(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (not (part_of sK26 iProver_c13)) (incident_c _let_0 iProver_c13))))
+(assert (or (part_of sK24 sK26) (not (incident_c (sK0 sK24 sK26) sK26))))
+(assert (or (part_of iProver_c13 sK26) (not (incident_c (sK0 iProver_c13 sK26) sK26))))
+(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK21 sK24 sK25))) (let ((_let_2 (sK21 _let_1 _let_0))) (let ((_let_3 (sK22 _let_1 _let_0))) (or (ordered_by _let_0 _let_2 _let_3) (ordered_by _let_1 _let_2 _let_3) (= _let_0 _let_1)))))))
+(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK21 iProver_c13 sK25))) (let ((_let_2 (sK21 _let_1 _let_0))) (let ((_let_3 (sK22 _let_1 _let_0))) (or (ordered_by _let_0 _let_2 _let_3) (ordered_by _let_1 _let_2 _let_3) (= _let_0 _let_1)))))))
+(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK21 sK24 sK25))) (let ((_let_2 (sK21 _let_0 _let_1))) (let ((_let_3 (sK22 _let_0 _let_1))) (or (ordered_by _let_1 _let_2 _let_3) (ordered_by _let_0 _let_2 _let_3) (= _let_1 _let_0)))))))
+(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK21 iProver_c13 sK25))) (let ((_let_2 (sK21 _let_0 _let_1))) (let ((_let_3 (sK22 _let_0 _let_1))) (or (ordered_by _let_1 _let_2 _let_3) (ordered_by _let_0 _let_2 _let_3) (= _let_1 _let_0)))))))
+(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK22 sK24 sK25))) (let ((_let_2 (sK21 _let_1 _let_0))) (let ((_let_3 (sK22 _let_1 _let_0))) (or (ordered_by _let_0 _let_2 _let_3) (ordered_by _let_1 _let_2 _let_3) (= _let_0 _let_1)))))))
+(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK22 iProver_c13 sK25))) (let ((_let_2 (sK21 _let_1 _let_0))) (let ((_let_3 (sK22 _let_1 _let_0))) (or (ordered_by _let_0 _let_2 _let_3) (ordered_by _let_1 _let_2 _let_3) (= _let_0 _let_1)))))))
+(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK22 sK24 sK25))) (let ((_let_2 (sK21 _let_0 _let_1))) (let ((_let_3 (sK22 _let_0 _let_1))) (or (ordered_by _let_1 _let_2 _let_3) (ordered_by _let_0 _let_2 _let_3) (= _let_1 _let_0)))))))
+(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK22 iProver_c13 sK25))) (let ((_let_2 (sK21 _let_0 _let_1))) (let ((_let_3 (sK22 _let_0 _let_1))) (or (ordered_by _let_1 _let_2 _let_3) (ordered_by _let_0 _let_2 _let_3) (= _let_1 _let_0)))))))
+(assert (let ((_let_0 (sK21 sK24 sK25))) (let ((_let_1 (sK22 sK24 sK25))) (or (not (ordered_by sK25 _let_0 _let_1)) (not (ordered_by sK24 _let_0 _let_1)) (= sK25 sK24)))))
+(assert (let ((_let_0 (sK21 iProver_c13 sK25))) (let ((_let_1 (sK22 iProver_c13 sK25))) (or (not (ordered_by sK25 _let_0 _let_1)) (not (ordered_by iProver_c13 _let_0 _let_1)) (= sK25 iProver_c13)))))
+(assert (let ((_let_0 (sK21 sK26 sK25))) (or (not (ordered_by sK25 _let_0 (sK22 sK26 sK25))) (incident_o _let_0 sK25))))
+(assert (let ((_let_0 (sK22 sK26 sK25))) (or (not (ordered_by sK25 (sK21 sK26 sK25) _let_0)) (incident_o _let_0 sK25))))
+(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK22 sK26 sK25))) (or (not (ordered_by sK25 _let_0 _let_1)) (not (ordered_by sK25 _let_1 sK24)) (between_o sK25 _let_0 _let_1 sK24)))))
+(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK22 sK26 sK25))) (or (not (ordered_by sK25 _let_0 _let_1)) (not (ordered_by sK25 _let_1 iProver_c13)) (between_o sK25 _let_0 _let_1 iProver_c13)))))
+(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK22 sK26 sK25))) (or (not (ordered_by sK25 _let_0 _let_1)) (not (ordered_by sK25 _let_1 sK24)) (between_o sK25 sK24 _let_1 _let_0)))))
+(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK22 sK26 sK25))) (or (not (ordered_by sK25 _let_0 _let_1)) (not (ordered_by sK25 _let_1 iProver_c13)) (between_o sK25 iProver_c13 _let_1 _let_0)))))
+(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK21 sK24 sK25))) (let ((_let_2 (sK12 _let_1 _let_0))) (or (= _let_0 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 _let_1))))))
+(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK21 iProver_c13 sK25))) (let ((_let_2 (sK12 _let_1 _let_0))) (or (= _let_0 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 _let_1))))))
+(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK21 sK24 sK25))) (let ((_let_2 (sK12 _let_0 _let_1))) (or (= _let_1 _let_0) (incident_c _let_2 _let_1) (incident_c _let_2 _let_0))))))
+(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK21 iProver_c13 sK25))) (let ((_let_2 (sK12 _let_0 _let_1))) (or (= _let_1 _let_0) (incident_c _let_2 _let_1) (incident_c _let_2 _let_0))))))
+(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK22 sK24 sK25))) (let ((_let_2 (sK12 _let_1 _let_0))) (or (= _let_0 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 _let_1))))))
+(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK22 iProver_c13 sK25))) (let ((_let_2 (sK12 _let_1 _let_0))) (or (= _let_0 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 _let_1))))))
+(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK22 sK24 sK25))) (let ((_let_2 (sK12 _let_0 _let_1))) (or (= _let_1 _let_0) (incident_c _let_2 _let_1) (incident_c _let_2 _let_0))))))
+(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK22 iProver_c13 sK25))) (let ((_let_2 (sK12 _let_0 _let_1))) (or (= _let_1 _let_0) (incident_c _let_2 _let_1) (incident_c _let_2 _let_0))))))
+(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK21 sK24 sK25))) (or (= _let_0 _let_1) (not (part_of _let_1 _let_0)) (open _let_1)))))
+(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK21 iProver_c13 sK25))) (or (= _let_0 _let_1) (not (part_of _let_1 _let_0)) (open _let_1)))))
+(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK21 sK24 sK25))) (or (= _let_1 _let_0) (not (part_of _let_0 _let_1)) (open _let_0)))))
+(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK21 iProver_c13 sK25))) (or (= _let_1 _let_0) (open _let_0) (not (part_of _let_0 _let_1))))))
+(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK22 sK24 sK25))) (or (= _let_0 _let_1) (not (part_of _let_1 _let_0)) (open _let_1)))))
+(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK22 iProver_c13 sK25))) (or (= _let_0 _let_1) (not (part_of _let_1 _let_0)) (open _let_1)))))
+(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK22 sK24 sK25))) (or (= _let_1 _let_0) (not (part_of _let_0 _let_1)) (open _let_0)))))
+(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK22 iProver_c13 sK25))) (or (= _let_1 _let_0) (open _let_0) (not (part_of _let_0 _let_1))))))
+(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK1 sK24 sK24 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 sK24) (= (sum sK24 sK24) _let_0)))))
+(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0)))))
+(assert (let ((_let_0 (sK22 sK24 sK25))) (let ((_let_1 (sK1 sK24 sK24 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 sK24) (= (sum sK24 sK24) _let_0)))))
+(assert (let ((_let_0 (sK22 iProver_c41 sK25))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0)))))
+(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK1 sK24 sK24 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 sK24) (= (sum sK24 sK24) _let_0)))))
+(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0)))))
+(assert (let ((_let_0 (sK21 sK24 sK25))) (let ((_let_1 (sK1 sK24 sK24 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 sK24) (= (sum sK24 sK24) _let_0)))))
+(assert (let ((_let_0 (sK21 iProver_c13 sK25))) (let ((_let_1 (sK1 iProver_c13 iProver_c13 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c13) (= (sum iProver_c13 iProver_c13) _let_0)))))
+(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK1 iProver_c13 iProver_c13 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c13) (= (sum iProver_c13 iProver_c13) _let_0)))))
+(assert (let ((_let_0 (sK21 iProver_c13 sK25))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0)))))
+(assert (let ((_let_0 (sK21 iProver_c41 sK25))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0)))))
+(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK22 sK24 sK25))) (let ((_let_2 (sK1 sK24 _let_0 _let_1))) (or (incident_c _let_2 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 sK24) (= (sum _let_0 sK24) _let_1))))))
+(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK22 iProver_c14 sK25))) (let ((_let_2 (sK1 iProver_c13 _let_0 _let_1))) (or (incident_c _let_2 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 iProver_c13) (= (sum _let_0 iProver_c13) _let_1))))))
+(assert (let ((_let_0 (sK22 iProver_c14 sK25))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0)))))
+(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK1 _let_0 sK24 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 sK24) (= (sum sK24 _let_0) _let_0)))))
+(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK1 _let_0 iProver_c13 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c13) (= (sum iProver_c13 _let_0) _let_0)))))
+(assert (let ((_let_0 (sK22 sK26 sK25))) (or (incident_c (sK1 _let_0 _let_0 _let_0) _let_0) (= (sum _let_0 _let_0) _let_0))))
+(assert (let ((_let_0 (sK22 iProver_c13 sK25))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0)))))
+(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK22 iProver_c13 sK25))) (let ((_let_2 (sK1 iProver_c13 _let_0 _let_1))) (or (incident_c _let_2 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 iProver_c13) (= (sum _let_0 iProver_c13) _let_1))))))
+(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK22 sK24 sK25))) (let ((_let_2 (sK1 _let_0 _let_0 _let_1))) (or (incident_c _let_2 _let_1) (incident_c _let_2 _let_0) (= (sum _let_0 _let_0) _let_1))))))
+(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK22 iProver_c13 sK25))) (let ((_let_2 (sK1 _let_0 _let_0 _let_1))) (or (incident_c _let_2 _let_1) (incident_c _let_2 _let_0) (= (sum _let_0 _let_0) _let_1))))))
+(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK22 sK24 sK25))) (let ((_let_2 (sK1 _let_0 sK24 _let_1))) (or (incident_c _let_2 _let_1) (incident_c _let_2 sK24) (incident_c _let_2 _let_0) (= (sum sK24 _let_0) _let_1))))))
+(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK22 iProver_c14 sK25))) (let ((_let_2 (sK1 _let_0 iProver_c13 _let_1))) (or (incident_c _let_2 _let_1) (incident_c _let_2 iProver_c13) (incident_c _let_2 _let_0) (= (sum iProver_c13 _let_0) _let_1))))))
+(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK22 sK26 sK25))) (let ((_let_2 (sK1 sK24 _let_1 _let_0))) (or (incident_c _let_2 _let_0) (incident_c _let_2 _let_1) (incident_c _let_2 sK24) (= (sum _let_1 sK24) _let_0))))))
+(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK22 sK26 sK25))) (let ((_let_2 (sK1 iProver_c13 _let_1 _let_0))) (or (incident_c _let_2 _let_0) (incident_c _let_2 _let_1) (incident_c _let_2 iProver_c13) (= (sum _let_1 iProver_c13) _let_0))))))
+(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK1 sK24 _let_0 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 sK24) (= (sum _let_0 sK24) _let_0)))))
+(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK1 iProver_c13 _let_0 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c13) (= (sum _let_0 iProver_c13) _let_0)))))
+(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK21 sK24 sK25))) (let ((_let_2 (sK1 sK24 _let_0 _let_1))) (or (incident_c _let_2 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 sK24) (= (sum _let_0 sK24) _let_1))))))
+(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK21 iProver_c14 sK25))) (let ((_let_2 (sK1 iProver_c13 _let_0 _let_1))) (or (incident_c _let_2 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 iProver_c13) (= (sum _let_0 iProver_c13) _let_1))))))
+(assert (let ((_let_0 (sK21 iProver_c14 sK25))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0)))))
+(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK21 sK24 sK26))) (let ((_let_2 (sK21 _let_1 _let_0))) (let ((_let_3 (sK22 _let_1 _let_0))) (or (ordered_by _let_0 _let_2 _let_3) (ordered_by _let_1 _let_2 _let_3) (= _let_0 _let_1)))))))
+(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK21 iProver_c13 sK26))) (let ((_let_2 (sK21 _let_1 _let_0))) (let ((_let_3 (sK22 _let_1 _let_0))) (or (ordered_by _let_0 _let_2 _let_3) (ordered_by _let_1 _let_2 _let_3) (= _let_0 _let_1)))))))
+(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK21 sK24 sK26))) (let ((_let_2 (sK21 _let_0 _let_1))) (let ((_let_3 (sK22 _let_0 _let_1))) (or (ordered_by _let_1 _let_2 _let_3) (ordered_by _let_0 _let_2 _let_3) (= _let_1 _let_0)))))))
+(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK21 iProver_c13 sK26))) (let ((_let_2 (sK21 _let_0 _let_1))) (let ((_let_3 (sK22 _let_0 _let_1))) (or (ordered_by _let_1 _let_2 _let_3) (ordered_by _let_0 _let_2 _let_3) (= _let_1 _let_0)))))))
+(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK22 sK24 sK26))) (let ((_let_2 (sK21 _let_1 _let_0))) (let ((_let_3 (sK22 _let_1 _let_0))) (or (ordered_by _let_0 _let_2 _let_3) (ordered_by _let_1 _let_2 _let_3) (= _let_0 _let_1)))))))
+(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK22 iProver_c13 sK26))) (let ((_let_2 (sK21 _let_1 _let_0))) (let ((_let_3 (sK22 _let_1 _let_0))) (or (ordered_by _let_0 _let_2 _let_3) (ordered_by _let_1 _let_2 _let_3) (= _let_0 _let_1)))))))
+(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK22 sK24 sK26))) (let ((_let_2 (sK21 _let_0 _let_1))) (let ((_let_3 (sK22 _let_0 _let_1))) (or (ordered_by _let_1 _let_2 _let_3) (ordered_by _let_0 _let_2 _let_3) (= _let_1 _let_0)))))))
+(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK22 iProver_c13 sK26))) (let ((_let_2 (sK21 _let_0 _let_1))) (let ((_let_3 (sK22 _let_0 _let_1))) (or (ordered_by _let_1 _let_2 _let_3) (ordered_by _let_0 _let_2 _let_3) (= _let_1 _let_0)))))))
+(assert (let ((_let_0 (sK21 sK24 sK26))) (let ((_let_1 (sK22 sK24 sK26))) (or (not (ordered_by sK26 _let_0 _let_1)) (not (ordered_by sK24 _let_0 _let_1)) (= sK26 sK24)))))
+(assert (let ((_let_0 (sK21 iProver_c13 sK26))) (let ((_let_1 (sK22 iProver_c13 sK26))) (or (not (ordered_by sK26 _let_0 _let_1)) (not (ordered_by iProver_c13 _let_0 _let_1)) (= sK26 iProver_c13)))))
+(assert (let ((_let_0 (sK21 sK25 sK26))) (or (not (ordered_by sK26 _let_0 (sK22 sK25 sK26))) (incident_o _let_0 sK26))))
+(assert (let ((_let_0 (sK22 sK25 sK26))) (or (not (ordered_by sK26 (sK21 sK25 sK26) _let_0)) (incident_o _let_0 sK26))))
+(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK22 sK25 sK26))) (or (not (ordered_by sK26 _let_0 _let_1)) (not (ordered_by sK26 _let_1 sK24)) (between_o sK26 _let_0 _let_1 sK24)))))
+(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK22 sK25 sK26))) (or (not (ordered_by sK26 _let_0 _let_1)) (not (ordered_by sK26 _let_1 iProver_c13)) (between_o sK26 _let_0 _let_1 iProver_c13)))))
+(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK22 sK25 sK26))) (or (not (ordered_by sK26 _let_0 _let_1)) (not (ordered_by sK26 _let_1 sK24)) (between_o sK26 sK24 _let_1 _let_0)))))
+(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK22 sK25 sK26))) (or (not (ordered_by sK26 _let_0 _let_1)) (not (ordered_by sK26 _let_1 iProver_c13)) (between_o sK26 iProver_c13 _let_1 _let_0)))))
+(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK21 sK24 sK26))) (let ((_let_2 (sK12 _let_1 _let_0))) (or (= _let_0 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 _let_1))))))
+(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK21 iProver_c13 sK26))) (let ((_let_2 (sK12 _let_1 _let_0))) (or (= _let_0 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 _let_1))))))
+(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK21 sK24 sK26))) (let ((_let_2 (sK12 _let_0 _let_1))) (or (= _let_1 _let_0) (incident_c _let_2 _let_1) (incident_c _let_2 _let_0))))))
+(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK21 iProver_c13 sK26))) (let ((_let_2 (sK12 _let_0 _let_1))) (or (= _let_1 _let_0) (incident_c _let_2 _let_1) (incident_c _let_2 _let_0))))))
+(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK22 sK24 sK26))) (let ((_let_2 (sK12 _let_1 _let_0))) (or (= _let_0 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 _let_1))))))
+(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK22 iProver_c13 sK26))) (let ((_let_2 (sK12 _let_1 _let_0))) (or (= _let_0 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 _let_1))))))
+(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK22 sK24 sK26))) (let ((_let_2 (sK12 _let_0 _let_1))) (or (= _let_1 _let_0) (incident_c _let_2 _let_1) (incident_c _let_2 _let_0))))))
+(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK22 iProver_c13 sK26))) (let ((_let_2 (sK12 _let_0 _let_1))) (or (= _let_1 _let_0) (incident_c _let_2 _let_1) (incident_c _let_2 _let_0))))))
+(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK21 sK24 sK26))) (or (= _let_0 _let_1) (not (part_of _let_1 _let_0)) (open _let_1)))))
+(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK21 iProver_c13 sK26))) (or (= _let_0 _let_1) (not (part_of _let_1 _let_0)) (open _let_1)))))
+(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK21 sK24 sK26))) (or (= _let_1 _let_0) (not (part_of _let_0 _let_1)) (open _let_0)))))
+(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK21 iProver_c13 sK26))) (or (= _let_1 _let_0) (open _let_0) (not (part_of _let_0 _let_1))))))
+(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK22 sK24 sK26))) (or (= _let_0 _let_1) (not (part_of _let_1 _let_0)) (open _let_1)))))
+(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK22 iProver_c13 sK26))) (or (= _let_0 _let_1) (not (part_of _let_1 _let_0)) (open _let_1)))))
+(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK22 sK24 sK26))) (or (= _let_1 _let_0) (not (part_of _let_0 _let_1)) (open _let_0)))))
+(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK22 iProver_c13 sK26))) (or (= _let_1 _let_0) (open _let_0) (not (part_of _let_0 _let_1))))))
+(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK1 sK24 sK24 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 sK24) (= (sum sK24 sK24) _let_0)))))
+(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0)))))
+(assert (let ((_let_0 (sK22 sK24 sK26))) (let ((_let_1 (sK1 sK24 sK24 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 sK24) (= (sum sK24 sK24) _let_0)))))
+(assert (let ((_let_0 (sK22 iProver_c41 sK26))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0)))))
+(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK1 sK24 sK24 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 sK24) (= (sum sK24 sK24) _let_0)))))
+(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0)))))
+(assert (let ((_let_0 (sK21 sK24 sK26))) (let ((_let_1 (sK1 sK24 sK24 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 sK24) (= (sum sK24 sK24) _let_0)))))
+(assert (let ((_let_0 (sK21 iProver_c13 sK26))) (let ((_let_1 (sK1 iProver_c13 iProver_c13 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c13) (= (sum iProver_c13 iProver_c13) _let_0)))))
+(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK1 iProver_c13 iProver_c13 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c13) (= (sum iProver_c13 iProver_c13) _let_0)))))
+(assert (let ((_let_0 (sK21 iProver_c13 sK26))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0)))))
+(assert (let ((_let_0 (sK21 iProver_c41 sK26))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0)))))
+(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK22 sK24 sK26))) (let ((_let_2 (sK1 sK24 _let_0 _let_1))) (or (incident_c _let_2 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 sK24) (= (sum _let_0 sK24) _let_1))))))
+(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK22 iProver_c14 sK26))) (let ((_let_2 (sK1 iProver_c13 _let_0 _let_1))) (or (incident_c _let_2 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 iProver_c13) (= (sum _let_0 iProver_c13) _let_1))))))
+(assert (let ((_let_0 (sK22 iProver_c14 sK26))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0)))))
+(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK1 _let_0 sK24 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 sK24) (= (sum sK24 _let_0) _let_0)))))
+(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK1 _let_0 iProver_c13 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c13) (= (sum iProver_c13 _let_0) _let_0)))))
+(assert (let ((_let_0 (sK22 sK25 sK26))) (or (incident_c (sK1 _let_0 _let_0 _let_0) _let_0) (= (sum _let_0 _let_0) _let_0))))
+(assert (let ((_let_0 (sK22 iProver_c13 sK26))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0)))))
+(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK22 iProver_c13 sK26))) (let ((_let_2 (sK1 iProver_c13 _let_0 _let_1))) (or (incident_c _let_2 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 iProver_c13) (= (sum _let_0 iProver_c13) _let_1))))))
+(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK22 sK24 sK26))) (let ((_let_2 (sK1 _let_0 _let_0 _let_1))) (or (incident_c _let_2 _let_1) (incident_c _let_2 _let_0) (= (sum _let_0 _let_0) _let_1))))))
+(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK22 iProver_c13 sK26))) (let ((_let_2 (sK1 _let_0 _let_0 _let_1))) (or (incident_c _let_2 _let_1) (incident_c _let_2 _let_0) (= (sum _let_0 _let_0) _let_1))))))
+(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK22 sK24 sK26))) (let ((_let_2 (sK1 _let_0 sK24 _let_1))) (or (incident_c _let_2 _let_1) (incident_c _let_2 sK24) (incident_c _let_2 _let_0) (= (sum sK24 _let_0) _let_1))))))
+(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK22 iProver_c14 sK26))) (let ((_let_2 (sK1 _let_0 iProver_c13 _let_1))) (or (incident_c _let_2 _let_1) (incident_c _let_2 iProver_c13) (incident_c _let_2 _let_0) (= (sum iProver_c13 _let_0) _let_1))))))
+(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK22 sK25 sK26))) (let ((_let_2 (sK1 sK24 _let_1 _let_0))) (or (incident_c _let_2 _let_0) (incident_c _let_2 _let_1) (incident_c _let_2 sK24) (= (sum _let_1 sK24) _let_0))))))
+(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK22 sK25 sK26))) (let ((_let_2 (sK1 iProver_c13 _let_1 _let_0))) (or (incident_c _let_2 _let_0) (incident_c _let_2 _let_1) (incident_c _let_2 iProver_c13) (= (sum _let_1 iProver_c13) _let_0))))))
+(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK1 sK24 _let_0 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 sK24) (= (sum _let_0 sK24) _let_0)))))
+(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK1 iProver_c13 _let_0 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c13) (= (sum _let_0 iProver_c13) _let_0)))))
+(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK21 sK24 sK26))) (let ((_let_2 (sK1 sK24 _let_0 _let_1))) (or (incident_c _let_2 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 sK24) (= (sum _let_0 sK24) _let_1))))))
+(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK21 iProver_c14 sK26))) (let ((_let_2 (sK1 iProver_c13 _let_0 _let_1))) (or (incident_c _let_2 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 iProver_c13) (= (sum _let_0 iProver_c13) _let_1))))))
+(assert (let ((_let_0 (sK21 iProver_c14 sK26))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0)))))
+(assert (or (= iProver_c13 iProver_c14) false false _substvar_29615_ false false))
+(assert (or (not (incident_c sK24 sK24)) (not (meet sK24 sK25 sK24)) (not (incident_c sK24 sK25)) (end_point sK24 sK25)))
+(assert (or (not (meet iProver_c14 sK25 iProver_c13)) (not (incident_c sK24 sK25)) (end_point sK24 sK25) (not (incident_c sK24 iProver_c13))))
+(assert (or (not (incident_c sK24 sK24)) (end_point sK24 sK24) (not (meet sK24 sK25 sK24)) (not (incident_c sK24 sK25))))
+(assert (or (not (meet iProver_c14 sK25 iProver_c13)) (not (incident_c sK24 sK25)) (not (incident_c sK24 iProver_c13)) (end_point sK24 iProver_c13)))
+(assert (or (not (incident_c sK24 sK24)) (meet sK24 sK25 sK24) (not (incident_c sK24 sK25)) (incident_c (sK4 sK24 sK25 sK24) sK25)))
+(assert (or (not (incident_c sK24 sK25)) (not (incident_c sK24 iProver_c13)) (incident_c (sK4 iProver_c13 sK25 sK24) sK25) (meet sK24 sK25 iProver_c13)))
+(assert (or (not (incident_c sK24 sK24)) (meet sK24 sK25 sK24) (not (incident_c sK24 sK25)) (incident_c (sK4 sK24 sK25 sK24) sK24)))
+(assert (or (not (incident_c sK24 sK25)) (not (incident_c sK24 iProver_c13)) (meet sK24 sK25 iProver_c13) (incident_c (sK4 iProver_c13 sK25 sK24) iProver_c13)))
+(assert (let ((_let_0 (sK4 sK24 sK25 sK24))) (or (not (incident_c sK24 sK24)) (meet sK24 sK25 sK24) (not (incident_c sK24 sK25)) (not (end_point _let_0 sK25)) (not (end_point _let_0 sK24)))))
+(assert (let ((_let_0 (sK4 iProver_c13 sK25 sK24))) (or (not (incident_c sK24 sK25)) (not (incident_c sK24 iProver_c13)) (meet sK24 sK25 iProver_c13) (not (end_point _let_0 sK25)) (not (end_point _let_0 iProver_c13)))))
+(assert (or (not (incident_c sK24 sK25)) (end_point sK24 sK25) (inner_point sK24 sK25)))
+(assert (let ((_let_0 (part_of sK25 sK24))) (or (not (incident_c sK24 sK24)) (not (part_of sK24 sK24)) (not (end_point sK24 sK24)) _let_0 (not _let_0) (part_of sK24 sK25) (not (incident_c sK24 sK25)))))
+(assert (or (not (part_of iProver_c13 iProver_c14)) (part_of sK25 iProver_c13) (part_of iProver_c13 sK25) (not (part_of sK25 iProver_c14)) (not (incident_c sK24 sK25)) (not (incident_c sK24 iProver_c13)) (not (end_point sK24 iProver_c14))))
+(assert (or (not (incident_c sK24 sK25)) (end_point sK24 sK25) (part_of (sK2 sK25 sK24) sK25)))
+(assert (or (not (incident_c sK24 sK25)) (end_point sK24 sK25) (part_of (sK3 sK25 sK24) sK25)))
+(assert (or (not (incident_c sK24 sK25)) (end_point sK24 sK25) (incident_c sK24 (sK2 sK25 sK24))))
+(assert (or (not (incident_c sK24 sK25)) (end_point sK24 sK25) (incident_c sK24 (sK3 sK25 sK24))))
+(assert (or (not (incident_c sK24 sK25)) (end_point sK24 sK25) (not (part_of (sK2 sK25 sK24) (sK3 sK25 sK24)))))
+(assert (or (not (incident_c sK24 sK25)) (end_point sK24 sK25) (not (part_of (sK3 sK25 sK24) (sK2 sK25 sK24)))))
+(assert (or (not (incident_c sK24 sK25)) (incident_c sK24 (sum sK25 sK24))))
+(assert (or (not (incident_c sK24 sK25)) (incident_c sK24 (sum sK25 iProver_c13))))
+(assert (or (not (incident_c sK24 sK25)) (incident_c sK24 (sum sK24 sK25))))
+(assert (or (not (incident_c sK24 sK25)) (incident_c sK24 (sum iProver_c13 sK25))))
+(assert (or (incident_c sK24 sK24) (not (part_of sK25 sK24)) (not (incident_c sK24 sK25))))
+(assert (or (not (part_of sK25 iProver_c13)) (not (incident_c sK24 sK25)) (incident_c sK24 iProver_c13)))
+(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK21 _let_0 sK24))) (let ((_let_2 (sK22 _let_0 sK24))) (or (ordered_by sK24 _let_1 _let_2) (ordered_by _let_0 _let_1 _let_2) (= sK24 _let_0))))))
+(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK12 _let_0 sK24))) (or (= sK24 _let_0) (incident_c _let_1 sK24) (incident_c _let_1 _let_0)))))
+(assert (let ((_let_0 (sK12 sK26 sK25))) (or (open _let_0) (= sK24 _let_0) (not (part_of _let_0 sK24)))))
+(assert (let ((_let_0 (sK12 sK26 sK25))) (or (open sK24) (not (part_of sK24 _let_0)) (= _let_0 sK24))))
+(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK21 sK24 _let_0))) (let ((_let_2 (sK22 sK24 _let_0))) (or (= _let_0 sK24) (ordered_by sK24 _let_1 _let_2) (ordered_by _let_0 _let_1 _let_2))))))
+(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK12 sK24 _let_0))) (or (= _let_0 sK24) (incident_c _let_1 sK24) (incident_c _let_1 _let_0)))))
+(assert (or (not (incident_c sK24 sK24)) (not (meet sK24 sK26 sK24)) (not (incident_c sK24 sK26)) (end_point sK24 sK26)))
+(assert (or (not (meet iProver_c14 sK26 iProver_c13)) (not (incident_c sK24 iProver_c13)) (not (incident_c sK24 sK26)) (end_point sK24 sK26)))
+(assert (or (not (incident_c sK24 sK24)) (end_point sK24 sK24) (not (meet sK24 sK26 sK24)) (not (incident_c sK24 sK26))))
+(assert (or (not (meet iProver_c14 sK26 iProver_c13)) (not (incident_c sK24 iProver_c13)) (end_point sK24 iProver_c13) (not (incident_c sK24 sK26))))
+(assert (or (not (incident_c sK24 sK24)) (meet sK24 sK26 sK24) (not (incident_c sK24 sK26)) (incident_c (sK4 sK24 sK26 sK24) sK26)))
+(assert (or (not (incident_c sK24 iProver_c13)) (not (incident_c sK24 sK26)) (incident_c (sK4 iProver_c13 sK26 sK24) sK26) (meet sK24 sK26 iProver_c13)))
+(assert (or (not (incident_c sK24 sK24)) (meet sK24 sK26 sK24) (not (incident_c sK24 sK26)) (incident_c (sK4 sK24 sK26 sK24) sK24)))
+(assert (or (not (incident_c sK24 iProver_c13)) (not (incident_c sK24 sK26)) (meet sK24 sK26 iProver_c13) (incident_c (sK4 iProver_c13 sK26 sK24) iProver_c13)))
+(assert (let ((_let_0 (sK4 sK24 sK26 sK24))) (or (not (incident_c sK24 sK24)) (meet sK24 sK26 sK24) (not (incident_c sK24 sK26)) (not (end_point _let_0 sK26)) (not (end_point _let_0 sK24)))))
+(assert (let ((_let_0 (sK4 iProver_c13 sK26 sK24))) (or (not (incident_c sK24 iProver_c13)) (not (incident_c sK24 sK26)) (meet sK24 sK26 iProver_c13) (not (end_point _let_0 sK26)) (not (end_point _let_0 iProver_c13)))))
+(assert (or (not (incident_c sK24 sK26)) (end_point sK24 sK26) (inner_point sK24 sK26)))
+(assert (let ((_let_0 (part_of sK26 sK24))) (or (not (incident_c sK24 sK24)) (not (part_of sK24 sK24)) (not (end_point sK24 sK24)) (part_of sK24 sK26) _let_0 (not _let_0) (not (incident_c sK24 sK26)))))
+(assert (or (not (part_of iProver_c13 iProver_c14)) (part_of iProver_c13 sK26) (part_of sK26 iProver_c13) (not (part_of sK26 iProver_c14)) (not (incident_c sK24 iProver_c13)) (not (end_point sK24 iProver_c14)) (not (incident_c sK24 sK26))))
+(assert (or (not (incident_c sK24 sK26)) (end_point sK24 sK26) (part_of (sK2 sK26 sK24) sK26)))
+(assert (or (not (incident_c sK24 sK26)) (end_point sK24 sK26) (part_of (sK3 sK26 sK24) sK26)))
+(assert (or (not (incident_c sK24 sK26)) (end_point sK24 sK26) (incident_c sK24 (sK2 sK26 sK24))))
+(assert (or (not (incident_c sK24 sK26)) (end_point sK24 sK26) (incident_c sK24 (sK3 sK26 sK24))))
+(assert (or (not (incident_c sK24 sK26)) (end_point sK24 sK26) (not (part_of (sK2 sK26 sK24) (sK3 sK26 sK24)))))
+(assert (or (not (incident_c sK24 sK26)) (end_point sK24 sK26) (not (part_of (sK3 sK26 sK24) (sK2 sK26 sK24)))))
+(assert (or (not (incident_c sK24 sK26)) (incident_c sK24 (sum sK26 sK24))))
+(assert (or (not (incident_c sK24 sK26)) (incident_c sK24 (sum sK26 iProver_c13))))
+(assert (or (not (incident_c sK24 sK26)) (incident_c sK24 (sum sK24 sK26))))
+(assert (or (not (incident_c sK24 sK26)) (incident_c sK24 (sum iProver_c13 sK26))))
+(assert (or (incident_c sK24 sK24) (not (part_of sK26 sK24)) (not (incident_c sK24 sK26))))
+(assert (or (not (part_of sK26 iProver_c13)) (incident_c sK24 iProver_c13) (not (incident_c sK24 sK26))))
+(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK21 _let_0 sK24))) (let ((_let_2 (sK22 _let_0 sK24))) (or (ordered_by sK24 _let_1 _let_2) (ordered_by _let_0 _let_1 _let_2) (= sK24 _let_0))))))
+(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK12 _let_0 sK24))) (or (= sK24 _let_0) (incident_c _let_1 sK24) (incident_c _let_1 _let_0)))))
+(assert (let ((_let_0 (sK12 sK25 sK26))) (or (open _let_0) (= sK24 _let_0) (not (part_of _let_0 sK24)))))
+(assert (let ((_let_0 (sK12 sK25 sK26))) (or (open sK24) (not (part_of sK24 _let_0)) (= _let_0 sK24))))
+(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK21 sK24 _let_0))) (let ((_let_2 (sK22 sK24 _let_0))) (or (= _let_0 sK24) (ordered_by sK24 _let_1 _let_2) (ordered_by _let_0 _let_1 _let_2))))))
+(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK12 sK24 _let_0))) (or (= _let_0 sK24) (incident_c _let_1 sK24) (incident_c _let_1 _let_0)))))
+(assert (let ((_let_0 (sK1 sK24 sK24 sK25))) (or (not (incident_c _let_0 sK25)) (not (incident_c _let_0 sK24)) (= (sum sK24 sK24) sK25))))
+(assert (let ((_let_0 (sK1 iProver_c13 iProver_c14 sK25))) (or (not (incident_c _let_0 sK25)) (not (incident_c _let_0 iProver_c14)) (= (sum iProver_c14 iProver_c13) sK25))))
+(assert (let ((_let_0 (sK1 sK24 sK24 sK26))) (or (not (incident_c _let_0 sK26)) (not (incident_c _let_0 sK24)) (= (sum sK24 sK24) sK26))))
+(assert (let ((_let_0 (sK1 iProver_c13 iProver_c14 sK26))) (or (not (incident_c _let_0 sK26)) (not (incident_c _let_0 iProver_c14)) (= (sum iProver_c14 iProver_c13) sK26))))
+(assert (let ((_let_0 (sum sK24 sK24))) (or (open sK25) (= _let_0 sK25) (not (part_of sK25 _let_0)))))
+(assert (let ((_let_0 (sum iProver_c13 iProver_c14))) (or (open sK25) (= _let_0 sK25) (not (part_of sK25 _let_0)))))
+(assert (let ((_let_0 (sum sK24 sK24))) (or (open sK26) (= _let_0 sK26) (not (part_of sK26 _let_0)))))
+(assert (let ((_let_0 (sum iProver_c13 iProver_c14))) (or (open sK26) (= _let_0 sK26) (not (part_of sK26 _let_0)))))
+(assert (let ((_let_0 (sum sK24 sK24))) (or (open _let_0) (not (part_of _let_0 sK25)) (= sK25 _let_0))))
+(assert (let ((_let_0 (sum iProver_c13 iProver_c14))) (or (open _let_0) (not (part_of _let_0 sK25)) (= sK25 _let_0))))
+(assert (let ((_let_0 (sum sK24 sK24))) (or (open _let_0) (not (part_of _let_0 sK26)) (= sK26 _let_0))))
+(assert (let ((_let_0 (sum iProver_c13 iProver_c14))) (or (open _let_0) (not (part_of _let_0 sK26)) (= sK26 _let_0))))
+(assert (let ((_let_0 (sum sK24 sK24))) (let ((_let_1 (sK12 _let_0 sK25))) (or (= sK25 _let_0) (incident_c _let_1 _let_0) (incident_c _let_1 sK25)))))
+(assert (let ((_let_0 (sum iProver_c13 iProver_c14))) (let ((_let_1 (sK12 _let_0 sK25))) (or (= sK25 _let_0) (incident_c _let_1 _let_0) (incident_c _let_1 sK25)))))
+(assert (let ((_let_0 (sum sK24 sK24))) (let ((_let_1 (sK12 _let_0 sK26))) (or (= sK26 _let_0) (incident_c _let_1 _let_0) (incident_c _let_1 sK26)))))
+(assert (let ((_let_0 (sum iProver_c13 iProver_c14))) (let ((_let_1 (sK12 _let_0 sK26))) (or (= sK26 _let_0) (incident_c _let_1 _let_0) (incident_c _let_1 sK26)))))
+(assert (let ((_let_0 (sK19 sK24))) (or (not (incident_o sK25 sK24)) (not (start_point _let_0 sK24)) (ordered_by sK24 _let_0 sK25) (= _let_0 sK25))))
+(assert (let ((_let_0 (sK19 iProver_c13))) (or (not (start_point _let_0 iProver_c13)) (not (incident_o sK25 iProver_c13)) (ordered_by iProver_c13 _let_0 sK25) (= _let_0 sK25))))
+(assert (let ((_let_0 (sK19 sK24))) (or (not (incident_o sK26 sK24)) (not (start_point _let_0 sK24)) (ordered_by sK24 _let_0 sK26) (= _let_0 sK26))))
+(assert (let ((_let_0 (sK19 iProver_c13))) (or (not (start_point _let_0 iProver_c13)) (not (incident_o sK26 iProver_c13)) (ordered_by iProver_c13 _let_0 sK26) (= _let_0 sK26))))
+(assert (let ((_let_0 (sK21 sK25 sK26))) (or (incident_o _let_0 sK26) (not (ordered_by sK26 _let_0 sK24)))))
+(assert (or (not (ordered_by sK26 (sK21 sK25 sK26) sK24)) (incident_o sK24 sK26)))
+(assert (let ((_let_0 (sK21 sK25 sK26))) (or (not (ordered_by sK26 _let_0 sK24)) (not (ordered_by sK26 sK24 sK24)) (between_o sK26 _let_0 sK24 sK24))))
+(assert (let ((_let_0 (sK21 sK25 sK26))) (or (not (ordered_by sK26 _let_0 sK24)) (not (ordered_by sK26 sK24 iProver_c13)) (between_o sK26 _let_0 sK24 iProver_c13))))
+(assert (let ((_let_0 (sK21 sK25 sK26))) (or (not (ordered_by sK26 _let_0 sK24)) (not (ordered_by sK26 sK24 sK24)) (between_o sK26 sK24 sK24 _let_0))))
+(assert (let ((_let_0 (sK21 sK25 sK26))) (or (not (ordered_by sK26 _let_0 sK24)) (not (ordered_by sK26 sK24 iProver_c13)) (between_o sK26 iProver_c13 sK24 _let_0))))
+(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK21 _let_0 sK24))) (let ((_let_2 (sK22 _let_0 sK24))) (or (ordered_by sK24 _let_1 _let_2) (ordered_by _let_0 _let_1 _let_2) (= sK24 _let_0))))))
+(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK12 _let_0 sK24))) (or (= sK24 _let_0) (incident_c _let_1 sK24) (incident_c _let_1 _let_0)))))
+(assert (let ((_let_0 (sK22 sK25 sK26))) (or (open _let_0) (= sK24 _let_0) (not (part_of _let_0 sK24)))))
+(assert (let ((_let_0 (sK22 sK25 sK26))) (or (open sK24) (not (part_of sK24 _let_0)) (= _let_0 sK24))))
+(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK21 sK24 _let_0))) (let ((_let_2 (sK22 sK24 _let_0))) (or (= _let_0 sK24) (ordered_by sK24 _let_1 _let_2) (ordered_by _let_0 _let_1 _let_2))))))
+(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK12 sK24 _let_0))) (or (= _let_0 sK24) (incident_c _let_1 sK24) (incident_c _let_1 _let_0)))))
+(assert (let ((_let_0 (sK21 sK26 sK25))) (or (incident_o _let_0 sK25) (not (ordered_by sK25 _let_0 sK24)))))
+(assert (or (not (ordered_by sK25 (sK21 sK26 sK25) sK24)) (incident_o sK24 sK25)))
+(assert (let ((_let_0 (sK21 sK26 sK25))) (or (not (ordered_by sK25 _let_0 sK24)) (not (ordered_by sK25 sK24 sK24)) (between_o sK25 _let_0 sK24 sK24))))
+(assert (let ((_let_0 (sK21 sK26 sK25))) (or (not (ordered_by sK25 _let_0 sK24)) (not (ordered_by sK25 sK24 iProver_c13)) (between_o sK25 _let_0 sK24 iProver_c13))))
+(assert (let ((_let_0 (sK21 sK26 sK25))) (or (not (ordered_by sK25 _let_0 sK24)) (not (ordered_by sK25 sK24 sK24)) (between_o sK25 sK24 sK24 _let_0))))
+(assert (let ((_let_0 (sK21 sK26 sK25))) (or (not (ordered_by sK25 _let_0 sK24)) (not (ordered_by sK25 sK24 iProver_c13)) (between_o sK25 iProver_c13 sK24 _let_0))))
+(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK21 _let_0 sK24))) (let ((_let_2 (sK22 _let_0 sK24))) (or (ordered_by sK24 _let_1 _let_2) (ordered_by _let_0 _let_1 _let_2) (= sK24 _let_0))))))
+(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK12 _let_0 sK24))) (or (= sK24 _let_0) (incident_c _let_1 sK24) (incident_c _let_1 _let_0)))))
+(assert (let ((_let_0 (sK22 sK26 sK25))) (or (open _let_0) (= sK24 _let_0) (not (part_of _let_0 sK24)))))
+(assert (let ((_let_0 (sK22 sK26 sK25))) (or (open sK24) (not (part_of sK24 _let_0)) (= _let_0 sK24))))
+(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK21 sK24 _let_0))) (let ((_let_2 (sK22 sK24 _let_0))) (or (= _let_0 sK24) (ordered_by sK24 _let_1 _let_2) (ordered_by _let_0 _let_1 _let_2))))))
+(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK12 sK24 _let_0))) (or (= _let_0 sK24) (incident_c _let_1 sK24) (incident_c _let_1 _let_0)))))
+(check-sat)
+

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index fec081ca81315a3e37dfac38c924a142c22025cf..4c14de996904c48ca33ce705d01cd1dd9d495bbc 100644 (file)
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -115,6 +115,7 @@ TPTP_TESTS = \
 
 # Regression tests derived from bug reports
 BUG_TESTS = \
+       GEO123+1.minimized.smt2 \
        smt2output.smt2 \
        bug32.cvc \
        bug49.smt \