Changing const TNode& to TNode in the CNF conversion + a new small benchmark that...

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index a5924a54416caa6a83ea4d26bd77721d17cb4f42..44768009ec89fc2bcf5e985ee8b0869eb56e39ac 100644 (file)
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -61,23 +61,23 @@ void CnfStream::assertClause(SatLiteral a, SatLiteral b, SatLiteral c) {
   assertClause(clause);
 }
 
-bool CnfStream::isCached(const TNode& n) const {
+bool CnfStream::isCached(TNode n) const {
   return d_translationCache.find(n) != d_translationCache.end();
 }
 
-SatLiteral CnfStream::lookupInCache(const TNode& n) const {
+SatLiteral CnfStream::lookupInCache(TNode n) const {
   Assert(isCached(n), "Node is not in CNF translation cache");
   return d_translationCache.find(n)->second;
 }
 
-void CnfStream::cacheTranslation(const TNode& node, SatLiteral lit) {
+void CnfStream::cacheTranslation(TNode node, SatLiteral lit) {
   Debug("cnf") << "caching translation " << node << " to " << lit << endl;
   // We always cash bot the node and the negation at the same time
   d_translationCache[node] = lit;
   d_translationCache[node.notNode()] = ~lit;
 }
 
-SatLiteral CnfStream::newLiteral(const TNode& node, bool theoryLiteral) {
+SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) {
   SatLiteral lit = SatLiteral(d_satSolver->newVar(theoryLiteral));
   cacheTranslation(node, lit);
   if (theoryLiteral) {
@@ -96,7 +96,7 @@ Node CnfStream::getNode(const SatLiteral& literal) {
   return node;
 }
 
-SatLiteral CnfStream::getLiteral(const TNode& node) {
+SatLiteral CnfStream::getLiteral(TNode node) {
   TranslationCache::iterator find = d_translationCache.find(node);
   Assert(find != d_translationCache.end(), "Literal not in the CNF Cache");
   SatLiteral literal = find->second;
@@ -104,14 +104,14 @@ SatLiteral CnfStream::getLiteral(const TNode& node) {
   return literal;
 }
 
-SatLiteral TseitinCnfStream::handleAtom(const TNode& node) {
+SatLiteral TseitinCnfStream::handleAtom(TNode node) {
   Assert(node.isAtomic(), "handleAtom(n) expects n to be an atom");
   Assert(!isCached(node), "atom already mapped!");
 
   Debug("cnf") << "handleAtom(" << node << ")" << endl;
  
-   bool theoryLiteral = node.getKind() != kind::VARIABLE;
-   SatLiteral lit = newLiteral(node, theoryLiteral);
+  bool theoryLiteral = node.getKind() != kind::VARIABLE;
+  SatLiteral lit = newLiteral(node, theoryLiteral);
 
   switch(node.getKind()) {
   case TRUE:
@@ -127,7 +127,7 @@ SatLiteral TseitinCnfStream::handleAtom(const TNode& node) {
   return lit;
 }
 
-SatLiteral TseitinCnfStream::handleXor(const TNode& xorNode) {
+SatLiteral TseitinCnfStream::handleXor(TNode xorNode) {
   Assert(!isCached(xorNode), "Atom already mapped!");
   Assert(xorNode.getKind() == XOR, "Expecting an XOR expression!");
   Assert(xorNode.getNumChildren() == 2, "Expecting exactly 2 children!");
@@ -145,7 +145,7 @@ SatLiteral TseitinCnfStream::handleXor(const TNode& xorNode) {
   return xorLit;
 }
 
-SatLiteral TseitinCnfStream::handleOr(const TNode& orNode) {
+SatLiteral TseitinCnfStream::handleOr(TNode orNode) {
   Assert(!isCached(orNode), "Atom already mapped!");
   Assert(orNode.getKind() == OR, "Expecting an OR expression!");
   Assert(orNode.getNumChildren() > 1, "Expecting more then 1 child!");
@@ -181,7 +181,7 @@ SatLiteral TseitinCnfStream::handleOr(const TNode& orNode) {
   return orLit;
 }
 
-SatLiteral TseitinCnfStream::handleAnd(const TNode& andNode) {
+SatLiteral TseitinCnfStream::handleAnd(TNode andNode) {
   Assert(!isCached(andNode), "Atom already mapped!");
   Assert(andNode.getKind() == AND, "Expecting an AND expression!");
   Assert(andNode.getNumChildren() > 1, "Expecting more than 1 child!");
@@ -216,7 +216,7 @@ SatLiteral TseitinCnfStream::handleAnd(const TNode& andNode) {
   return andLit;
 }
 
-SatLiteral TseitinCnfStream::handleImplies(const TNode& impliesNode) {
+SatLiteral TseitinCnfStream::handleImplies(TNode impliesNode) {
   Assert(!isCached(impliesNode), "Atom already mapped!");
   Assert(impliesNode.getKind() == IMPLIES, "Expecting an IMPLIES expression!");
   Assert(impliesNode.getNumChildren() == 2, "Expecting exactly 2 children!");
@@ -241,7 +241,7 @@ SatLiteral TseitinCnfStream::handleImplies(const TNode& impliesNode) {
 }
 
 
-SatLiteral TseitinCnfStream::handleIff(const TNode& iffNode) {
+SatLiteral TseitinCnfStream::handleIff(TNode iffNode) {
   Assert(!isCached(iffNode), "Atom already mapped!");
   Assert(iffNode.getKind() == IFF, "Expecting an IFF expression!");
   Assert(iffNode.getNumChildren() == 2, "Expecting exactly 2 children!");
@@ -271,7 +271,7 @@ SatLiteral TseitinCnfStream::handleIff(const TNode& iffNode) {
 }
 
 
-SatLiteral TseitinCnfStream::handleNot(const TNode& notNode) {
+SatLiteral TseitinCnfStream::handleNot(TNode notNode) {
   Assert(!isCached(notNode), "Atom already mapped!");
   Assert(notNode.getKind() == NOT, "Expecting a NOT expression!");
   Assert(notNode.getNumChildren() == 1, "Expecting exactly 2 children!");
@@ -284,7 +284,7 @@ SatLiteral TseitinCnfStream::handleNot(const TNode& notNode) {
   return notLit;
 }
 
-SatLiteral TseitinCnfStream::handleIte(const TNode& iteNode) {
+SatLiteral TseitinCnfStream::handleIte(TNode iteNode) {
   Assert(iteNode.getKind() == ITE);
   Assert(iteNode.getNumChildren() == 3);
 
@@ -309,7 +309,7 @@ SatLiteral TseitinCnfStream::handleIte(const TNode& iteNode) {
   return iteLit;
 }
 
-SatLiteral TseitinCnfStream::toCNF(const TNode& node) {
+SatLiteral TseitinCnfStream::toCNF(TNode node) {
 
   // If the node has already been translated, return the previous translation
   if(isCached(node)) {
@@ -342,7 +342,7 @@ SatLiteral TseitinCnfStream::toCNF(const TNode& node) {
   }
 }
 
-void TseitinCnfStream::convertAndAssert(const TNode& node) {
+void TseitinCnfStream::convertAndAssert(TNode node) {
   Debug("cnf") << "convertAndAssert(" << node << ")" << endl;
   // If the node is a conjuntion, we handle each conjunct separatelu
   if(node.getKind() == AND) {

diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index 2581046c1802a11b80d0553824140d071d9ff0ea..7d7912e10bffb3bc22ec2ac656f465d0cb41ff53 100644 (file)
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -87,14 +87,14 @@ protected:
    * @param node the node
    * @return true if the node has been cached
    */
-  bool isCached(const TNode& node) const;
+  bool isCached(TNode node) const;
 
   /**
    * Returns the cashed literal corresponding to the given node.
    * @param node the node to lookup
    * @return returns the corresponding literal
    */
-  SatLiteral lookupInCache(const TNode& n) const;
+  SatLiteral lookupInCache(TNode n) const;
 
   /**
    * Caches the pair of the node and the literal corresponding to the
@@ -102,7 +102,7 @@ protected:
    * @param node node
    * @param lit
    */
-  void cacheTranslation(const TNode& node, SatLiteral lit);
+  void cacheTranslation(TNode node, SatLiteral lit);
 
   /**
    * Acquires a new variable from the SAT solver to represent the node and
@@ -112,7 +112,7 @@ protected:
    *        informed when set to true/false
    * @return the literal corresponding to the formula
    */
-  SatLiteral newLiteral(const TNode& node, bool theoryLiteral = false);
+  SatLiteral newLiteral(TNode node, bool theoryLiteral = false);
 
 public:
 
@@ -136,7 +136,7 @@ public:
    * @param node node to convert and assert
    * @param whether the sat solver can choose to remove this clause
    */
-  virtual void convertAndAssert(const TNode& node) = 0;
+  virtual void convertAndAssert(TNode node) = 0;
 
   /**
    * Returns a node the is represented by a give SatLiteral literal.
@@ -149,7 +149,7 @@ public:
    * Returns the literal the represents the given node in the SAT CNF
    * representation.
    */
-  SatLiteral getLiteral(const TNode& node);
+  SatLiteral getLiteral(TNode node);
 
 }; /* class CnfStream */
 
@@ -171,7 +171,7 @@ public:
    * Convert a given formula to CNF and assert it to the SAT solver.
    * @param node the formula to assert
    */
-  void convertAndAssert(const TNode& node);
+  void convertAndAssert(TNode node);
 
   /**
    * Constructs the stream to use the given sat solver.
@@ -191,21 +191,21 @@ private:
   //   - returning l
   //
   // handleX( n ) can assume that n is not in d_translationCache
-  SatLiteral handleAtom(const TNode& node);
-  SatLiteral handleNot(const TNode& node);
-  SatLiteral handleXor(const TNode& node);
-  SatLiteral handleImplies(const TNode& node);
-  SatLiteral handleIff(const TNode& node);
-  SatLiteral handleIte(const TNode& node);
-  SatLiteral handleAnd(const TNode& node);
-  SatLiteral handleOr(const TNode& node);
+  SatLiteral handleAtom(TNode node);
+  SatLiteral handleNot(TNode node);
+  SatLiteral handleXor(TNode node);
+  SatLiteral handleImplies(TNode node);
+  SatLiteral handleIff(TNode node);
+  SatLiteral handleIte(TNode node);
+  SatLiteral handleAnd(TNode node);
+  SatLiteral handleOr(TNode node);
 
   /**
    * Transforms the node into CNF recursively.
    * @param node the formula to transform
    * @return the literal representing the root of the formula
    */
-  SatLiteral toCNF(const TNode& node);
+  SatLiteral toCNF(TNode node);
 
 }; /* class TseitinCnfStream */
 

diff --git a/src/prop/sat.h b/src/prop/sat.h
index f105310803e703f18ef78195a0b820bd37274a18..ec38bb0193d1e4cb67be1ea5abd50643b65febf2 100644 (file)
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -179,7 +179,7 @@ void SatSolver::theoryCheck(SatClause& conflict) {
   Node conflictNode = d_theoryEngine->getConflict();
   // If the conflict is there, construct the conflict clause
   if (!conflictNode.isNull()) {
-    Debug("prop") << "SatSolver::theoryCheck() => conflict" << std::endl;
+    Debug("prop") << "SatSolver::theoryCheck() => conflict: " << conflictNode << std::endl;
     Node::const_iterator literal_it = conflictNode.begin();
     Node::const_iterator literal_end = conflictNode.end();
     while (literal_it != literal_end) {

diff --git a/test/regress/regress0/uf/iso_icl_repgen004.smt b/test/regress/regress0/uf/iso_icl_repgen004.smt
new file mode 100644 (file)
index 0000000..76b63d2
--- /dev/null
+++ b/test/regress/regress0/uf/iso_icl_repgen004.smt
@@ -0,0 +1,53 @@
+(benchmark iso_icl_repgen004.smt
+  :source {
+http://www.cs.bham.ac.uk/~vxs/quasigroups/benchmark/
+
+}
+  :status unsat
+  :difficulty { 1 }
+  :category { crafted }
+  :logic QF_UF
+  :extrasorts (I)
+  :extrafuns ((op1 I I I))
+  :extrafuns ((op I I I))
+  :extrafuns ((e5 I))
+  :extrafuns ((e4 I))
+  :extrafuns ((e3 I))
+  :extrafuns ((e2 I))
+  :extrafuns ((e1 I))
+  :extrafuns ((e0 I))
+  :assumption
+(let (?cvc_0 (op e0 e0)) (let (?cvc_1 (op e0 e1)) (let (?cvc_2 (op e0 e2)) (let (?cvc_3 (op e0 e3)) (let (?cvc_4 (op e0 e4)) (let (?cvc_5 (op e0 e5)) (let (?cvc_6 (op e1 e0)) (let (?cvc_7 (op e1 e1)) (let (?cvc_8 (op e1 e2)) (let (?cvc_9 (op e1 e3)) (let (?cvc_10 (op e1 e4)) (let (?cvc_11 (op e1 e5)) (let (?cvc_12 (op e2 e0)) (let (?cvc_13 (op e2 e1)) (let (?cvc_14 (op e2 e2)) (let (?cvc_15 (op e2 e3)) (let (?cvc_16 (op e2 e4)) (let (?cvc_17 (op e2 e5)) (let (?cvc_18 (op e3 e0)) (let (?cvc_19 (op e3 e1)) (let (?cvc_20 (op e3 e2)) (let (?cvc_21 (op e3 e3)) (let (?cvc_22 (op e3 e4)) (let (?cvc_23 (op e3 e5)) (let (?cvc_24 (op e4 e0)) (let (?cvc_25 (op e4 e1)) (let (?cvc_26 (op e4 e2)) (let (?cvc_27 (op e4 e3)) (let (?cvc_28 (op e4 e4)) (let (?cvc_29 (op e4 e5)) (let (?cvc_30 (op e5 e0)) (let (?cvc_31 (op e5 e1)) (let (?cvc_32 (op e5 e2)) (let (?cvc_33 (op e5 e3)) (let (?cvc_34 (op e5 e4)) (let (?cvc_35 (op e5 e5)) (and (and (and (and (and (and (and (and (and (and (or (or (or (or (or (= ?cvc_0 e0)  (= ?cvc_0 e1) )  (= ?cvc_0 e2) )  (= ?cvc_0 e3) )  (= ?cvc_0 e4) )  (= ?cvc_0 e5) ) (or (or (or (or (or (= ?cvc_1 e0)  (= ?cvc_1 e1) )  (= ?cvc_1 e2) )  (= ?cvc_1 e3) )  (= ?cvc_1 e4) )  (= ?cvc_1 e5) )) (or (or (or (or (or (= ?cvc_2 e0)  (= ?cvc_2 e1) )  (= ?cvc_2 e2) )  (= ?cvc_2 e3) )  (= ?cvc_2 e4) )  (= ?cvc_2 e5) )) (or (or (or (or (or (= ?cvc_3 e0)  (= ?cvc_3 e1) )  (= ?cvc_3 e2) )  (= ?cvc_3 e3) )  (= ?cvc_3 e4) )  (= ?cvc_3 e5) )) (or (or (or (or (or (= ?cvc_4 e0)  (= ?cvc_4 e1) )  (= ?cvc_4 e2) )  (= ?cvc_4 e3) )  (= ?cvc_4 e4) )  (= ?cvc_4 e5) )) (or (or (or (or (or (= ?cvc_5 e0)  (= ?cvc_5 e1) )  (= ?cvc_5 e2) )  (= ?cvc_5 e3) )  (= ?cvc_5 e4) )  (= ?cvc_5 e5) )) (and (and (and (and (and (or (or (or (or (or (= ?cvc_6 e0)  (= ?cvc_6 e1) )  (= ?cvc_6 e2) )  (= ?cvc_6 e3) )  (= ?cvc_6 e4) )  (= ?cvc_6 e5) ) (or (or (or (or (or (= ?cvc_7 e0)  (= ?cvc_7 e1) )  (= ?cvc_7 e2) )  (= ?cvc_7 e3) )  (= ?cvc_7 e4) )  (= ?cvc_7 e5) )) (or (or (or (or (or (= ?cvc_8 e0)  (= ?cvc_8 e1) )  (= ?cvc_8 e2) )  (= ?cvc_8 e3) )  (= ?cvc_8 e4) )  (= ?cvc_8 e5) )) (or (or (or (or (or (= ?cvc_9 e0)  (= ?cvc_9 e1) )  (= ?cvc_9 e2) )  (= ?cvc_9 e3) )  (= ?cvc_9 e4) )  (= ?cvc_9 e5) )) (or (or (or (or (or (= ?cvc_10 e0)  (= ?cvc_10 e1) )  (= ?cvc_10 e2) )  (= ?cvc_10 e3) )  (= ?cvc_10 e4) )  (= ?cvc_10 e5) )) (or (or (or (or (or (= ?cvc_11 e0)  (= ?cvc_11 e1) )  (= ?cvc_11 e2) )  (= ?cvc_11 e3) )  (= ?cvc_11 e4) )  (= ?cvc_11 e5) ))) (and (and (and (and (and (or (or (or (or (or (= ?cvc_12 e0)  (= ?cvc_12 e1) )  (= ?cvc_12 e2) )  (= ?cvc_12 e3) )  (= ?cvc_12 e4) )  (= ?cvc_12 e5) ) (or (or (or (or (or (= ?cvc_13 e0)  (= ?cvc_13 e1) )  (= ?cvc_13 e2) )  (= ?cvc_13 e3) )  (= ?cvc_13 e4) )  (= ?cvc_13 e5) )) (or (or (or (or (or (= ?cvc_14 e0)  (= ?cvc_14 e1) )  (= ?cvc_14 e2) )  (= ?cvc_14 e3) )  (= ?cvc_14 e4) )  (= ?cvc_14 e5) )) (or (or (or (or (or (= ?cvc_15 e0)  (= ?cvc_15 e1) )  (= ?cvc_15 e2) )  (= ?cvc_15 e3) )  (= ?cvc_15 e4) )  (= ?cvc_15 e5) )) (or (or (or (or (or (= ?cvc_16 e0)  (= ?cvc_16 e1) )  (= ?cvc_16 e2) )  (= ?cvc_16 e3) )  (= ?cvc_16 e4) )  (= ?cvc_16 e5) )) (or (or (or (or (or (= ?cvc_17 e0)  (= ?cvc_17 e1) )  (= ?cvc_17 e2) )  (= ?cvc_17 e3) )  (= ?cvc_17 e4) )  (= ?cvc_17 e5) ))) (and (and (and (and (and (or (or (or (or (or (= ?cvc_18 e0)  (= ?cvc_18 e1) )  (= ?cvc_18 e2) )  (= ?cvc_18 e3) )  (= ?cvc_18 e4) )  (= ?cvc_18 e5) ) (or (or (or (or (or (= ?cvc_19 e0)  (= ?cvc_19 e1) )  (= ?cvc_19 e2) )  (= ?cvc_19 e3) )  (= ?cvc_19 e4) )  (= ?cvc_19 e5) )) (or (or (or (or (or (= ?cvc_20 e0)  (= ?cvc_20 e1) )  (= ?cvc_20 e2) )  (= ?cvc_20 e3) )  (= ?cvc_20 e4) )  (= ?cvc_20 e5) )) (or (or (or (or (or (= ?cvc_21 e0)  (= ?cvc_21 e1) )  (= ?cvc_21 e2) )  (= ?cvc_21 e3) )  (= ?cvc_21 e4) )  (= ?cvc_21 e5) )) (or (or (or (or (or (= ?cvc_22 e0)  (= ?cvc_22 e1) )  (= ?cvc_22 e2) )  (= ?cvc_22 e3) )  (= ?cvc_22 e4) )  (= ?cvc_22 e5) )) (or (or (or (or (or (= ?cvc_23 e0)  (= ?cvc_23 e1) )  (= ?cvc_23 e2) )  (= ?cvc_23 e3) )  (= ?cvc_23 e4) )  (= ?cvc_23 e5) ))) (and (and (and (and (and (or (or (or (or (or (= ?cvc_24 e0)  (= ?cvc_24 e1) )  (= ?cvc_24 e2) )  (= ?cvc_24 e3) )  (= ?cvc_24 e4) )  (= ?cvc_24 e5) ) (or (or (or (or (or (= ?cvc_25 e0)  (= ?cvc_25 e1) )  (= ?cvc_25 e2) )  (= ?cvc_25 e3) )  (= ?cvc_25 e4) )  (= ?cvc_25 e5) )) (or (or (or (or (or (= ?cvc_26 e0)  (= ?cvc_26 e1) )  (= ?cvc_26 e2) )  (= ?cvc_26 e3) )  (= ?cvc_26 e4) )  (= ?cvc_26 e5) )) (or (or (or (or (or (= ?cvc_27 e0)  (= ?cvc_27 e1) )  (= ?cvc_27 e2) )  (= ?cvc_27 e3) )  (= ?cvc_27 e4) )  (= ?cvc_27 e5) )) (or (or (or (or (or (= ?cvc_28 e0)  (= ?cvc_28 e1) )  (= ?cvc_28 e2) )  (= ?cvc_28 e3) )  (= ?cvc_28 e4) )  (= ?cvc_28 e5) )) (or (or (or (or (or (= ?cvc_29 e0)  (= ?cvc_29 e1) )  (= ?cvc_29 e2) )  (= ?cvc_29 e3) )  (= ?cvc_29 e4) )  (= ?cvc_29 e5) ))) (and (and (and (and (and (or (or (or (or (or (= ?cvc_30 e0)  (= ?cvc_30 e1) )  (= ?cvc_30 e2) )  (= ?cvc_30 e3) )  (= ?cvc_30 e4) )  (= ?cvc_30 e5) ) (or (or (or (or (or (= ?cvc_31 e0)  (= ?cvc_31 e1) )  (= ?cvc_31 e2) )  (= ?cvc_31 e3) )  (= ?cvc_31 e4) )  (= ?cvc_31 e5) )) (or (or (or (or (or (= ?cvc_32 e0)  (= ?cvc_32 e1) )  (= ?cvc_32 e2) )  (= ?cvc_32 e3) )  (= ?cvc_32 e4) )  (= ?cvc_32 e5) )) (or (or (or (or (or (= ?cvc_33 e0)  (= ?cvc_33 e1) )  (= ?cvc_33 e2) )  (= ?cvc_33 e3) )  (= ?cvc_33 e4) )  (= ?cvc_33 e5) )) (or (or (or (or (or (= ?cvc_34 e0)  (= ?cvc_34 e1) )  (= ?cvc_34 e2) )  (= ?cvc_34 e3) )  (= ?cvc_34 e4) )  (= ?cvc_34 e5) )) (or (or (or (or (or (= ?cvc_35 e0)  (= ?cvc_35 e1) )  (= ?cvc_35 e2) )  (= ?cvc_35 e3) )  (= ?cvc_35 e4) )  (= ?cvc_35 e5) )))))))))))))))))))))))))))))))))))))))
+  :assumption
+(let (?cvc_1 (op e0 e0)) (flet ($cvc_0 (= ?cvc_1 e0)) (flet ($cvc_7 (= ?cvc_1 e1)) (flet ($cvc_13 (= ?cvc_1 e2)) (flet ($cvc_14 (= ?cvc_1 e3)) (flet ($cvc_15 (= ?cvc_1 e4)) (flet ($cvc_16 (= ?cvc_1 e5)) (let (?cvc_2 (op e0 e1)) (flet ($cvc_18 (= ?cvc_2 e0)) (flet ($cvc_26 (= ?cvc_2 e1)) (flet ($cvc_33 (= ?cvc_2 e2)) (flet ($cvc_36 (= ?cvc_2 e3)) (flet ($cvc_39 (= ?cvc_2 e4)) (flet ($cvc_42 (= ?cvc_2 e5)) (let (?cvc_3 (op e0 e2)) (flet ($cvc_46 (= ?cvc_3 e0)) (flet ($cvc_55 (= ?cvc_3 e1)) (flet ($cvc_63 (= ?cvc_3 e2)) (flet ($cvc_68 (= ?cvc_3 e3)) (flet ($cvc_73 (= ?cvc_3 e4)) (flet ($cvc_78 (= ?cvc_3 e5)) (let (?cvc_4 (op e0 e3)) (flet ($cvc_84 (= ?cvc_4 e0)) (flet ($cvc_94 (= ?cvc_4 e1)) (flet ($cvc_103 (= ?cvc_4 e2)) (flet ($cvc_110 (= ?cvc_4 e3)) (flet ($cvc_117 (= ?cvc_4 e4)) (flet ($cvc_124 (= ?cvc_4 e5)) (let (?cvc_5 (op e0 e4)) (flet ($cvc_132 (= ?cvc_5 e0)) (flet ($cvc_143 (= ?cvc_5 e1)) (flet ($cvc_153 (= ?cvc_5 e2)) (flet ($cvc_162 (= ?cvc_5 e3)) (flet ($cvc_171 (= ?cvc_5 e4)) (flet ($cvc_180 (= ?cvc_5 e5)) (let (?cvc_6 (op e0 e5)) (flet ($cvc_190 (= ?cvc_6 e0)) (flet ($cvc_202 (= ?cvc_6 e1)) (flet ($cvc_213 (= ?cvc_6 e2)) (flet ($cvc_224 (= ?cvc_6 e3)) (flet ($cvc_235 (= ?cvc_6 e4)) (flet ($cvc_246 (= ?cvc_6 e5)) (let (?cvc_8 (op e1 e0)) (flet ($cvc_17 (= ?cvc_8 e0)) (flet ($cvc_20 (= ?cvc_8 e1)) (flet ($cvc_32 (= ?cvc_8 e2)) (flet ($cvc_35 (= ?cvc_8 e3)) (flet ($cvc_38 (= ?cvc_8 e4)) (flet ($cvc_41 (= ?cvc_8 e5)) (let (?cvc_21 (op e1 e1)) (flet ($cvc_19 (= ?cvc_21 e0)) (flet ($cvc_27 (= ?cvc_21 e1)) (flet ($cvc_34 (= ?cvc_21 e2)) (flet ($cvc_37 (= ?cvc_21 e3)) (flet ($cvc_40 (= ?cvc_21 e4)) (flet ($cvc_43 (= ?cvc_21 e5)) (let (?cvc_22 (op e1 e2)) (flet ($cvc_47 (= ?cvc_22 e0)) (flet ($cvc_56 (= ?cvc_22 e1)) (flet ($cvc_64 (= ?cvc_22 e2)) (flet ($cvc_69 (= ?cvc_22 e3)) (flet ($cvc_74 (= ?cvc_22 e4)) (flet ($cvc_79 (= ?cvc_22 e5)) (let (?cvc_23 (op e1 e3)) (flet ($cvc_85 (= ?cvc_23 e0)) (flet ($cvc_95 (= ?cvc_23 e1)) (flet ($cvc_104 (= ?cvc_23 e2)) (flet ($cvc_111 (= ?cvc_23 e3)) (flet ($cvc_118 (= ?cvc_23 e4)) (flet ($cvc_125 (= ?cvc_23 e5)) (let (?cvc_24 (op e1 e4)) (flet ($cvc_133 (= ?cvc_24 e0)) (flet ($cvc_144 (= ?cvc_24 e1)) (flet ($cvc_154 (= ?cvc_24 e2)) (flet ($cvc_163 (= ?cvc_24 e3)) (flet ($cvc_172 (= ?cvc_24 e4)) (flet ($cvc_181 (= ?cvc_24 e5)) (let (?cvc_25 (op e1 e5)) (flet ($cvc_191 (= ?cvc_25 e0)) (flet ($cvc_203 (= ?cvc_25 e1)) (flet ($cvc_214 (= ?cvc_25 e2)) (flet ($cvc_225 (= ?cvc_25 e3)) (flet ($cvc_236 (= ?cvc_25 e4)) (flet ($cvc_247 (= ?cvc_25 e5)) (let (?cvc_9 (op e2 e0)) (flet ($cvc_44 (= ?cvc_9 e0)) (flet ($cvc_49 (= ?cvc_9 e1)) (flet ($cvc_61 (= ?cvc_9 e2)) (flet ($cvc_66 (= ?cvc_9 e3)) (flet ($cvc_71 (= ?cvc_9 e4)) (flet ($cvc_76 (= ?cvc_9 e5)) (let (?cvc_28 (op e2 e1)) (flet ($cvc_45 (= ?cvc_28 e0)) (flet ($cvc_50 (= ?cvc_28 e1)) (flet ($cvc_62 (= ?cvc_28 e2)) (flet ($cvc_67 (= ?cvc_28 e3)) (flet ($cvc_72 (= ?cvc_28 e4)) (flet ($cvc_77 (= ?cvc_28 e5)) (let (?cvc_51 (op e2 e2)) (flet ($cvc_48 (= ?cvc_51 e0)) (flet ($cvc_57 (= ?cvc_51 e1)) (flet ($cvc_65 (= ?cvc_51 e2)) (flet ($cvc_70 (= ?cvc_51 e3)) (flet ($cvc_75 (= ?cvc_51 e4)) (flet ($cvc_80 (= ?cvc_51 e5)) (let (?cvc_52 (op e2 e3)) (flet ($cvc_86 (= ?cvc_52 e0)) (flet ($cvc_96 (= ?cvc_52 e1)) (flet ($cvc_105 (= ?cvc_52 e2)) (flet ($cvc_112 (= ?cvc_52 e3)) (flet ($cvc_119 (= ?cvc_52 e4)) (flet ($cvc_126 (= ?cvc_52 e5)) (let (?cvc_53 (op e2 e4)) (flet ($cvc_134 (= ?cvc_53 e0)) (flet ($cvc_145 (= ?cvc_53 e1)) (flet ($cvc_155 (= ?cvc_53 e2)) (flet ($cvc_164 (= ?cvc_53 e3)) (flet ($cvc_173 (= ?cvc_53 e4)) (flet ($cvc_182 (= ?cvc_53 e5)) (let (?cvc_54 (op e2 e5)) (flet ($cvc_192 (= ?cvc_54 e0)) (flet ($cvc_204 (= ?cvc_54 e1)) (flet ($cvc_215 (= ?cvc_54 e2)) (flet ($cvc_226 (= ?cvc_54 e3)) (flet ($cvc_237 (= ?cvc_54 e4)) (flet ($cvc_248 (= ?cvc_54 e5)) (let (?cvc_10 (op e3 e0)) (flet ($cvc_81 (= ?cvc_10 e0)) (flet ($cvc_88 (= ?cvc_10 e1)) (flet ($cvc_100 (= ?cvc_10 e2)) (flet ($cvc_107 (= ?cvc_10 e3)) (flet ($cvc_114 (= ?cvc_10 e4)) (flet ($cvc_121 (= ?cvc_10 e5)) (let (?cvc_29 (op e3 e1)) (flet ($cvc_82 (= ?cvc_29 e0)) (flet ($cvc_89 (= ?cvc_29 e1)) (flet ($cvc_101 (= ?cvc_29 e2)) (flet ($cvc_108 (= ?cvc_29 e3)) (flet ($cvc_115 (= ?cvc_29 e4)) (flet ($cvc_122 (= ?cvc_29 e5)) (let (?cvc_58 (op e3 e2)) (flet ($cvc_83 (= ?cvc_58 e0)) (flet ($cvc_90 (= ?cvc_58 e1)) (flet ($cvc_102 (= ?cvc_58 e2)) (flet ($cvc_109 (= ?cvc_58 e3)) (flet ($cvc_116 (= ?cvc_58 e4)) (flet ($cvc_123 (= ?cvc_58 e5)) (let (?cvc_91 (op e3 e3)) (flet ($cvc_87 (= ?cvc_91 e0)) (flet ($cvc_97 (= ?cvc_91 e1)) (flet ($cvc_106 (= ?cvc_91 e2)) (flet ($cvc_113 (= ?cvc_91 e3)) (flet ($cvc_120 (= ?cvc_91 e4)) (flet ($cvc_127 (= ?cvc_91 e5)) (let (?cvc_92 (op e3 e4)) (flet ($cvc_135 (= ?cvc_92 e0)) (flet ($cvc_146 (= ?cvc_92 e1)) (flet ($cvc_156 (= ?cvc_92 e2)) (flet ($cvc_165 (= ?cvc_92 e3)) (flet ($cvc_174 (= ?cvc_92 e4)) (flet ($cvc_183 (= ?cvc_92 e5)) (let (?cvc_93 (op e3 e5)) (flet ($cvc_193 (= ?cvc_93 e0)) (flet ($cvc_205 (= ?cvc_93 e1)) (flet ($cvc_216 (= ?cvc_93 e2)) (flet ($cvc_227 (= ?cvc_93 e3)) (flet ($cvc_238 (= ?cvc_93 e4)) (flet ($cvc_249 (= ?cvc_93 e5)) (let (?cvc_11 (op e4 e0)) (flet ($cvc_128 (= ?cvc_11 e0)) (flet ($cvc_137 (= ?cvc_11 e1)) (flet ($cvc_149 (= ?cvc_11 e2)) (flet ($cvc_158 (= ?cvc_11 e3)) (flet ($cvc_167 (= ?cvc_11 e4)) (flet ($cvc_176 (= ?cvc_11 e5)) (let (?cvc_30 (op e4 e1)) (flet ($cvc_129 (= ?cvc_30 e0)) (flet ($cvc_138 (= ?cvc_30 e1)) (flet ($cvc_150 (= ?cvc_30 e2)) (flet ($cvc_159 (= ?cvc_30 e3)) (flet ($cvc_168 (= ?cvc_30 e4)) (flet ($cvc_177 (= ?cvc_30 e5)) (let (?cvc_59 (op e4 e2)) (flet ($cvc_130 (= ?cvc_59 e0)) (flet ($cvc_139 (= ?cvc_59 e1)) (flet ($cvc_151 (= ?cvc_59 e2)) (flet ($cvc_160 (= ?cvc_59 e3)) (flet ($cvc_169 (= ?cvc_59 e4)) (flet ($cvc_178 (= ?cvc_59 e5)) (let (?cvc_98 (op e4 e3)) (flet ($cvc_131 (= ?cvc_98 e0)) (flet ($cvc_140 (= ?cvc_98 e1)) (flet ($cvc_152 (= ?cvc_98 e2)) (flet ($cvc_161 (= ?cvc_98 e3)) (flet ($cvc_170 (= ?cvc_98 e4)) (flet ($cvc_179 (= ?cvc_98 e5)) (let (?cvc_141 (op e4 e4)) (flet ($cvc_136 (= ?cvc_141 e0)) (flet ($cvc_147 (= ?cvc_141 e1)) (flet ($cvc_157 (= ?cvc_141 e2)) (flet ($cvc_166 (= ?cvc_141 e3)) (flet ($cvc_175 (= ?cvc_141 e4)) (flet ($cvc_184 (= ?cvc_141 e5)) (let (?cvc_142 (op e4 e5)) (flet ($cvc_194 (= ?cvc_142 e0)) (flet ($cvc_206 (= ?cvc_142 e1)) (flet ($cvc_217 (= ?cvc_142 e2)) (flet ($cvc_228 (= ?cvc_142 e3)) (flet ($cvc_239 (= ?cvc_142 e4)) (flet ($cvc_250 (= ?cvc_142 e5)) (let (?cvc_12 (op e5 e0)) (flet ($cvc_185 (= ?cvc_12 e0)) (flet ($cvc_196 (= ?cvc_12 e1)) (flet ($cvc_208 (= ?cvc_12 e2)) (flet ($cvc_219 (= ?cvc_12 e3)) (flet ($cvc_230 (= ?cvc_12 e4)) (flet ($cvc_241 (= ?cvc_12 e5)) (let (?cvc_31 (op e5 e1)) (flet ($cvc_186 (= ?cvc_31 e0)) (flet ($cvc_197 (= ?cvc_31 e1)) (flet ($cvc_209 (= ?cvc_31 e2)) (flet ($cvc_220 (= ?cvc_31 e3)) (flet ($cvc_231 (= ?cvc_31 e4)) (flet ($cvc_242 (= ?cvc_31 e5)) (let (?cvc_60 (op e5 e2)) (flet ($cvc_187 (= ?cvc_60 e0)) (flet ($cvc_198 (= ?cvc_60 e1)) (flet ($cvc_210 (= ?cvc_60 e2)) (flet ($cvc_221 (= ?cvc_60 e3)) (flet ($cvc_232 (= ?cvc_60 e4)) (flet ($cvc_243 (= ?cvc_60 e5)) (let (?cvc_99 (op e5 e3)) (flet ($cvc_188 (= ?cvc_99 e0)) (flet ($cvc_199 (= ?cvc_99 e1)) (flet ($cvc_211 (= ?cvc_99 e2)) (flet ($cvc_222 (= ?cvc_99 e3)) (flet ($cvc_233 (= ?cvc_99 e4)) (flet ($cvc_244 (= ?cvc_99 e5)) (let (?cvc_148 (op e5 e4)) (flet ($cvc_189 (= ?cvc_148 e0)) (flet ($cvc_200 (= ?cvc_148 e1)) (flet ($cvc_212 (= ?cvc_148 e2)) (flet ($cvc_223 (= ?cvc_148 e3)) (flet ($cvc_234 (= ?cvc_148 e4)) (flet ($cvc_245 (= ?cvc_148 e5)) (let (?cvc_201 (op e5 e5)) (flet ($cvc_195 (= ?cvc_201 e0)) (flet ($cvc_207 (= ?cvc_201 e1)) (flet ($cvc_218 (= ?cvc_201 e2)) (flet ($cvc_229 (= ?cvc_201 e3)) (flet ($cvc_240 (= ?cvc_201 e4)) (flet ($cvc_251 (= ?cvc_201 e5)) (and (and (and (and (and (and (and (and (and (and (and (or (or (or (or (or $cvc_0  $cvc_18 )  $cvc_46 )  $cvc_84 )  $cvc_132 )  $cvc_190 ) (or (or (or (or (or $cvc_0  $cvc_17 )  $cvc_44 )  $cvc_81 )  $cvc_128 )  $cvc_185 )) (and (or (or (or (or (or $cvc_7  $cvc_26 )  $cvc_55 )  $cvc_94 )  $cvc_143 )  $cvc_202 ) (or (or (or (or (or $cvc_7  $cvc_20 )  $cvc_49 )  $cvc_88 )  $cvc_137 )  $cvc_196 ))) (and (or (or (or (or (or $cvc_13  $cvc_33 )  $cvc_63 )  $cvc_103 )  $cvc_153 )  $cvc_213 ) (or (or (or (or (or $cvc_13  $cvc_32 )  $cvc_61 )  $cvc_100 )  $cvc_149 )  $cvc_208 ))) (and (or (or (or (or (or $cvc_14  $cvc_36 )  $cvc_68 )  $cvc_110 )  $cvc_162 )  $cvc_224 ) (or (or (or (or (or $cvc_14  $cvc_35 )  $cvc_66 )  $cvc_107 )  $cvc_158 )  $cvc_219 ))) (and (or (or (or (or (or $cvc_15  $cvc_39 )  $cvc_73 )  $cvc_117 )  $cvc_171 )  $cvc_235 ) (or (or (or (or (or $cvc_15  $cvc_38 )  $cvc_71 )  $cvc_114 )  $cvc_167 )  $cvc_230 ))) (and (or (or (or (or (or $cvc_16  $cvc_42 )  $cvc_78 )  $cvc_124 )  $cvc_180 )  $cvc_246 ) (or (or (or (or (or $cvc_16  $cvc_41 )  $cvc_76 )  $cvc_121 )  $cvc_176 )  $cvc_241 ))) (and (and (and (and (and (and (or (or (or (or (or $cvc_17  $cvc_19 )  $cvc_47 )  $cvc_85 )  $cvc_133 )  $cvc_191 ) (or (or (or (or (or $cvc_18  $cvc_19 )  $cvc_45 )  $cvc_82 )  $cvc_129 )  $cvc_186 )) (and (or (or (or (or (or $cvc_20  $cvc_27 )  $cvc_56 )  $cvc_95 )  $cvc_144 )  $cvc_203 ) (or (or (or (or (or $cvc_26  $cvc_27 )  $cvc_50 )  $cvc_89 )  $cvc_138 )  $cvc_197 ))) (and (or (or (or (or (or $cvc_32  $cvc_34 )  $cvc_64 )  $cvc_104 )  $cvc_154 )  $cvc_214 ) (or (or (or (or (or $cvc_33  $cvc_34 )  $cvc_62 )  $cvc_101 )  $cvc_150 )  $cvc_209 ))) (and (or (or (or (or (or $cvc_35  $cvc_37 )  $cvc_69 )  $cvc_111 )  $cvc_163 )  $cvc_225 ) (or (or (or (or (or $cvc_36  $cvc_37 )  $cvc_67 )  $cvc_108 )  $cvc_159 )  $cvc_220 ))) (and (or (or (or (or (or $cvc_38  $cvc_40 )  $cvc_74 )  $cvc_118 )  $cvc_172 )  $cvc_236 ) (or (or (or (or (or $cvc_39  $cvc_40 )  $cvc_72 )  $cvc_115 )  $cvc_168 )  $cvc_231 ))) (and (or (or (or (or (or $cvc_41  $cvc_43 )  $cvc_79 )  $cvc_125 )  $cvc_181 )  $cvc_247 ) (or (or (or (or (or $cvc_42  $cvc_43 )  $cvc_77 )  $cvc_122 )  $cvc_177 )  $cvc_242 )))) (and (and (and (and (and (and (or (or (or (or (or $cvc_44  $cvc_45 )  $cvc_48 )  $cvc_86 )  $cvc_134 )  $cvc_192 ) (or (or (or (or (or $cvc_46  $cvc_47 )  $cvc_48 )  $cvc_83 )  $cvc_130 )  $cvc_187 )) (and (or (or (or (or (or $cvc_49  $cvc_50 )  $cvc_57 )  $cvc_96 )  $cvc_145 )  $cvc_204 ) (or (or (or (or (or $cvc_55  $cvc_56 )  $cvc_57 )  $cvc_90 )  $cvc_139 )  $cvc_198 ))) (and (or (or (or (or (or $cvc_61  $cvc_62 )  $cvc_65 )  $cvc_105 )  $cvc_155 )  $cvc_215 ) (or (or (or (or (or $cvc_63  $cvc_64 )  $cvc_65 )  $cvc_102 )  $cvc_151 )  $cvc_210 ))) (and (or (or (or (or (or $cvc_66  $cvc_67 )  $cvc_70 )  $cvc_112 )  $cvc_164 )  $cvc_226 ) (or (or (or (or (or $cvc_68  $cvc_69 )  $cvc_70 )  $cvc_109 )  $cvc_160 )  $cvc_221 ))) (and (or (or (or (or (or $cvc_71  $cvc_72 )  $cvc_75 )  $cvc_119 )  $cvc_173 )  $cvc_237 ) (or (or (or (or (or $cvc_73  $cvc_74 )  $cvc_75 )  $cvc_116 )  $cvc_169 )  $cvc_232 ))) (and (or (or (or (or (or $cvc_76  $cvc_77 )  $cvc_80 )  $cvc_126 )  $cvc_182 )  $cvc_248 ) (or (or (or (or (or $cvc_78  $cvc_79 )  $cvc_80 )  $cvc_123 )  $cvc_178 )  $cvc_243 )))) (and (and (and (and (and (and (or (or (or (or (or $cvc_81  $cvc_82 )  $cvc_83 )  $cvc_87 )  $cvc_135 )  $cvc_193 ) (or (or (or (or (or $cvc_84  $cvc_85 )  $cvc_86 )  $cvc_87 )  $cvc_131 )  $cvc_188 )) (and (or (or (or (or (or $cvc_88  $cvc_89 )  $cvc_90 )  $cvc_97 )  $cvc_146 )  $cvc_205 ) (or (or (or (or (or $cvc_94  $cvc_95 )  $cvc_96 )  $cvc_97 )  $cvc_140 )  $cvc_199 ))) (and (or (or (or (or (or $cvc_100  $cvc_101 )  $cvc_102 )  $cvc_106 )  $cvc_156 )  $cvc_216 ) (or (or (or (or (or $cvc_103  $cvc_104 )  $cvc_105 )  $cvc_106 )  $cvc_152 )  $cvc_211 ))) (and (or (or (or (or (or $cvc_107  $cvc_108 )  $cvc_109 )  $cvc_113 )  $cvc_165 )  $cvc_227 ) (or (or (or (or (or $cvc_110  $cvc_111 )  $cvc_112 )  $cvc_113 )  $cvc_161 )  $cvc_222 ))) (and (or (or (or (or (or $cvc_114  $cvc_115 )  $cvc_116 )  $cvc_120 )  $cvc_174 )  $cvc_238 ) (or (or (or (or (or $cvc_117  $cvc_118 )  $cvc_119 )  $cvc_120 )  $cvc_170 )  $cvc_233 ))) (and (or (or (or (or (or $cvc_121  $cvc_122 )  $cvc_123 )  $cvc_127 )  $cvc_183 )  $cvc_249 ) (or (or (or (or (or $cvc_124  $cvc_125 )  $cvc_126 )  $cvc_127 )  $cvc_179 )  $cvc_244 )))) (and (and (and (and (and (and (or (or (or (or (or $cvc_128  $cvc_129 )  $cvc_130 )  $cvc_131 )  $cvc_136 )  $cvc_194 ) (or (or (or (or (or $cvc_132  $cvc_133 )  $cvc_134 )  $cvc_135 )  $cvc_136 )  $cvc_189 )) (and (or (or (or (or (or $cvc_137  $cvc_138 )  $cvc_139 )  $cvc_140 )  $cvc_147 )  $cvc_206 ) (or (or (or (or (or $cvc_143  $cvc_144 )  $cvc_145 )  $cvc_146 )  $cvc_147 )  $cvc_200 ))) (and (or (or (or (or (or $cvc_149  $cvc_150 )  $cvc_151 )  $cvc_152 )  $cvc_157 )  $cvc_217 ) (or (or (or (or (or $cvc_153  $cvc_154 )  $cvc_155 )  $cvc_156 )  $cvc_157 )  $cvc_212 ))) (and (or (or (or (or (or $cvc_158  $cvc_159 )  $cvc_160 )  $cvc_161 )  $cvc_166 )  $cvc_228 ) (or (or (or (or (or $cvc_162  $cvc_163 )  $cvc_164 )  $cvc_165 )  $cvc_166 )  $cvc_223 ))) (and (or (or (or (or (or $cvc_167  $cvc_168 )  $cvc_169 )  $cvc_170 )  $cvc_175 )  $cvc_239 ) (or (or (or (or (or $cvc_171  $cvc_172 )  $cvc_173 )  $cvc_174 )  $cvc_175 )  $cvc_234 ))) (and (or (or (or (or (or $cvc_176  $cvc_177 )  $cvc_178 )  $cvc_179 )  $cvc_184 )  $cvc_250 ) (or (or (or (or (or $cvc_180  $cvc_181 )  $cvc_182 )  $cvc_183 )  $cvc_184 )  $cvc_245 )))) (and (and (and (and (and (and (or (or (or (or (or $cvc_185  $cvc_186 )  $cvc_187 )  $cvc_188 )  $cvc_189 )  $cvc_195 ) (or (or (or (or (or $cvc_190  $cvc_191 )  $cvc_192 )  $cvc_193 )  $cvc_194 )  $cvc_195 )) (and (or (or (or (or (or $cvc_196  $cvc_197 )  $cvc_198 )  $cvc_199 )  $cvc_200 )  $cvc_207 ) (or (or (or (or (or $cvc_202  $cvc_203 )  $cvc_204 )  $cvc_205 )  $cvc_206 )  $cvc_207 ))) (and (or (or (or (or (or $cvc_208  $cvc_209 )  $cvc_210 )  $cvc_211 )  $cvc_212 )  $cvc_218 ) (or (or (or (or (or $cvc_213  $cvc_214 )  $cvc_215 )  $cvc_216 )  $cvc_217 )  $cvc_218 ))) (and (or (or (or (or (or $cvc_219  $cvc_220 )  $cvc_221 )  $cvc_222 )  $cvc_223 )  $cvc_229 ) (or (or (or (or (or $cvc_224  $cvc_225 )  $cvc_226 )  $cvc_227 )  $cvc_228 )  $cvc_229 ))) (and (or (or (or (or (or $cvc_230  $cvc_231 )  $cvc_232 )  $cvc_233 )  $cvc_234 )  $cvc_240 ) (or (or (or (or (or $cvc_235  $cvc_236 )  $cvc_237 )  $cvc_238 )  $cvc_239 )  $cvc_240 ))) (and (or (or (or (or (or $cvc_241  $cvc_242 )  $cvc_243 )  $cvc_244 )  $cvc_245 )  $cvc_251 ) (or (or (or (or (or $cvc_246  $cvc_247 )  $cvc_248 )  $cvc_249 )  $cvc_250 )  $cvc_251 ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+  :assumption
+(let (?cvc_0 (op e0 e0)) (let (?cvc_1 (op e0 e1)) (let (?cvc_4 (op e0 e2)) (let (?cvc_9 (op e0 e3)) (let (?cvc_16 (op e0 e4)) (let (?cvc_25 (op e0 e5)) (let (?cvc_2 (op e1 e0)) (let (?cvc_3 (op e1 e1)) (let (?cvc_6 (op e1 e2)) (let (?cvc_11 (op e1 e3)) (let (?cvc_18 (op e1 e4)) (let (?cvc_27 (op e1 e5)) (let (?cvc_5 (op e2 e0)) (let (?cvc_7 (op e2 e1)) (let (?cvc_8 (op e2 e2)) (let (?cvc_13 (op e2 e3)) (let (?cvc_20 (op e2 e4)) (let (?cvc_29 (op e2 e5)) (let (?cvc_10 (op e3 e0)) (let (?cvc_12 (op e3 e1)) (let (?cvc_14 (op e3 e2)) (let (?cvc_15 (op e3 e3)) (let (?cvc_22 (op e3 e4)) (let (?cvc_31 (op e3 e5)) (let (?cvc_17 (op e4 e0)) (let (?cvc_19 (op e4 e1)) (let (?cvc_21 (op e4 e2)) (let (?cvc_23 (op e4 e3)) (let (?cvc_24 (op e4 e4)) (let (?cvc_33 (op e4 e5)) (let (?cvc_26 (op e5 e0)) (let (?cvc_28 (op e5 e1)) (let (?cvc_30 (op e5 e2)) (let (?cvc_32 (op e5 e3)) (let (?cvc_34 (op e5 e4)) (let (?cvc_35 (op e5 e5)) (or (or (or (or (or (and (and (and (and (and (= (op ?cvc_0 ?cvc_0) e0) (= (op ?cvc_2 ?cvc_1) e1)) (= (op ?cvc_5 ?cvc_4) e2)) (= (op ?cvc_10 ?cvc_9) e3)) (= (op ?cvc_17 ?cvc_16) e4)) (= (op ?cvc_26 ?cvc_25) e5))  (and (and (and (and (and (= (op ?cvc_1 ?cvc_2) e0) (= (op ?cvc_3 ?cvc_3) e1)) (= (op ?cvc_7 ?cvc_6) e2)) (= (op ?cvc_12 ?cvc_11) e3)) (= (op ?cvc_19 ?cvc_18) e4)) (= (op ?cvc_28 ?cvc_27) e5)) )  (and (and (and (and (and (= (op ?cvc_4 ?cvc_5) e0) (= (op ?cvc_6 ?cvc_7) e1)) (= (op ?cvc_8 ?cvc_8) e2)) (= (op ?cvc_14 ?cvc_13) e3)) (= (op ?cvc_21 ?cvc_20) e4)) (= (op ?cvc_30 ?cvc_29) e5)) )  (and (and (and (and (and (= (op ?cvc_9 ?cvc_10) e0) (= (op ?cvc_11 ?cvc_12) e1)) (= (op ?cvc_13 ?cvc_14) e2)) (= (op ?cvc_15 ?cvc_15) e3)) (= (op ?cvc_23 ?cvc_22) e4)) (= (op ?cvc_32 ?cvc_31) e5)) )  (and (and (and (and (and (= (op ?cvc_16 ?cvc_17) e0) (= (op ?cvc_18 ?cvc_19) e1)) (= (op ?cvc_20 ?cvc_21) e2)) (= (op ?cvc_22 ?cvc_23) e3)) (= (op ?cvc_24 ?cvc_24) e4)) (= (op ?cvc_34 ?cvc_33) e5)) )  (and (and (and (and (and (= (op ?cvc_25 ?cvc_26) e0) (= (op ?cvc_27 ?cvc_28) e1)) (= (op ?cvc_29 ?cvc_30) e2)) (= (op ?cvc_31 ?cvc_32) e3)) (= (op ?cvc_33 ?cvc_34) e4)) (= (op ?cvc_35 ?cvc_35) e5)) )))))))))))))))))))))))))))))))))))))
+  :assumption
+(and (and (and (and (and (not (= (op e0 e0) e0)) (not (= (op e1 e1) e1))) (not (= (op e2 e2) e2))) (not (= (op e3 e3) e3))) (not (= (op e4 e4) e4))) (not (= (op e5 e5) e5)))
+  :assumption
+(let (?cvc_0 (op e0 e0)) (let (?cvc_6 (op e0 e1)) (let (?cvc_12 (op e0 e2)) (let (?cvc_18 (op e0 e3)) (let (?cvc_24 (op e0 e4)) (let (?cvc_30 (op e0 e5)) (let (?cvc_1 (op e1 e0)) (let (?cvc_7 (op e1 e1)) (let (?cvc_13 (op e1 e2)) (let (?cvc_19 (op e1 e3)) (let (?cvc_25 (op e1 e4)) (let (?cvc_31 (op e1 e5)) (let (?cvc_2 (op e2 e0)) (let (?cvc_8 (op e2 e1)) (let (?cvc_14 (op e2 e2)) (let (?cvc_20 (op e2 e3)) (let (?cvc_26 (op e2 e4)) (let (?cvc_32 (op e2 e5)) (let (?cvc_3 (op e3 e0)) (let (?cvc_9 (op e3 e1)) (let (?cvc_15 (op e3 e2)) (let (?cvc_21 (op e3 e3)) (let (?cvc_27 (op e3 e4)) (let (?cvc_33 (op e3 e5)) (let (?cvc_4 (op e4 e0)) (let (?cvc_10 (op e4 e1)) (let (?cvc_16 (op e4 e2)) (let (?cvc_22 (op e4 e3)) (let (?cvc_28 (op e4 e4)) (let (?cvc_34 (op e4 e5)) (let (?cvc_5 (op e5 e0)) (let (?cvc_11 (op e5 e1)) (let (?cvc_17 (op e5 e2)) (let (?cvc_23 (op e5 e3)) (let (?cvc_29 (op e5 e4)) (let (?cvc_35 (op e5 e5)) (or (or (or (or (or (and (and (and (and (and (not (= (op ?cvc_0 e0) ?cvc_0)) (not (= (op ?cvc_1 e1) ?cvc_1))) (not (= (op ?cvc_2 e2) ?cvc_2))) (not (= (op ?cvc_3 e3) ?cvc_3))) (not (= (op ?cvc_4 e4) ?cvc_4))) (not (= (op ?cvc_5 e5) ?cvc_5)))  (and (and (and (and (and (not (= (op ?cvc_6 e0) ?cvc_6)) (not (= (op ?cvc_7 e1) ?cvc_7))) (not (= (op ?cvc_8 e2) ?cvc_8))) (not (= (op ?cvc_9 e3) ?cvc_9))) (not (= (op ?cvc_10 e4) ?cvc_10))) (not (= (op ?cvc_11 e5) ?cvc_11))) )  (and (and (and (and (and (not (= (op ?cvc_12 e0) ?cvc_12)) (not (= (op ?cvc_13 e1) ?cvc_13))) (not (= (op ?cvc_14 e2) ?cvc_14))) (not (= (op ?cvc_15 e3) ?cvc_15))) (not (= (op ?cvc_16 e4) ?cvc_16))) (not (= (op ?cvc_17 e5) ?cvc_17))) )  (and (and (and (and (and (not (= (op ?cvc_18 e0) ?cvc_18)) (not (= (op ?cvc_19 e1) ?cvc_19))) (not (= (op ?cvc_20 e2) ?cvc_20))) (not (= (op ?cvc_21 e3) ?cvc_21))) (not (= (op ?cvc_22 e4) ?cvc_22))) (not (= (op ?cvc_23 e5) ?cvc_23))) )  (and (and (and (and (and (not (= (op ?cvc_24 e0) ?cvc_24)) (not (= (op ?cvc_25 e1) ?cvc_25))) (not (= (op ?cvc_26 e2) ?cvc_26))) (not (= (op ?cvc_27 e3) ?cvc_27))) (not (= (op ?cvc_28 e4) ?cvc_28))) (not (= (op ?cvc_29 e5) ?cvc_29))) )  (and (and (and (and (and (not (= (op ?cvc_30 e0) ?cvc_30)) (not (= (op ?cvc_31 e1) ?cvc_31))) (not (= (op ?cvc_32 e2) ?cvc_32))) (not (= (op ?cvc_33 e3) ?cvc_33))) (not (= (op ?cvc_34 e4) ?cvc_34))) (not (= (op ?cvc_35 e5) ?cvc_35))) )))))))))))))))))))))))))))))))))))))
+  :assumption
+(and (and (and (and (and (or (or (or (or (or (= (op e0 (op e0 e0)) e0)  (= (op e0 (op e0 e1)) e1) )  (= (op e0 (op e0 e2)) e2) )  (= (op e0 (op e0 e3)) e3) )  (= (op e0 (op e0 e4)) e4) )  (= (op e0 (op e0 e5)) e5) ) (or (or (or (or (or (= (op e1 (op e1 e0)) e0)  (= (op e1 (op e1 e1)) e1) )  (= (op e1 (op e1 e2)) e2) )  (= (op e1 (op e1 e3)) e3) )  (= (op e1 (op e1 e4)) e4) )  (= (op e1 (op e1 e5)) e5) )) (or (or (or (or (or (= (op e2 (op e2 e0)) e0)  (= (op e2 (op e2 e1)) e1) )  (= (op e2 (op e2 e2)) e2) )  (= (op e2 (op e2 e3)) e3) )  (= (op e2 (op e2 e4)) e4) )  (= (op e2 (op e2 e5)) e5) )) (or (or (or (or (or (= (op e3 (op e3 e0)) e0)  (= (op e3 (op e3 e1)) e1) )  (= (op e3 (op e3 e2)) e2) )  (= (op e3 (op e3 e3)) e3) )  (= (op e3 (op e3 e4)) e4) )  (= (op e3 (op e3 e5)) e5) )) (or (or (or (or (or (= (op e4 (op e4 e0)) e0)  (= (op e4 (op e4 e1)) e1) )  (= (op e4 (op e4 e2)) e2) )  (= (op e4 (op e4 e3)) e3) )  (= (op e4 (op e4 e4)) e4) )  (= (op e4 (op e4 e5)) e5) )) (or (or (or (or (or (= (op e5 (op e5 e0)) e0)  (= (op e5 (op e5 e1)) e1) )  (= (op e5 (op e5 e2)) e2) )  (= (op e5 (op e5 e3)) e3) )  (= (op e5 (op e5 e4)) e4) )  (= (op e5 (op e5 e5)) e5) ))
+  :assumption
+(or (or (or (or (or (= (op e0 (op e0 e0)) e0)  (= (op e1 (op e1 e1)) e1) )  (= (op e2 (op e2 e2)) e2) )  (= (op e3 (op e3 e3)) e3) )  (= (op e4 (op e4 e4)) e4) )  (= (op e5 (op e5 e5)) e5) )
+  :assumption
+(and (and (and (and (and (or (or (or (or (or (= (op (op e0 e0) e0) e0)  (= (op (op e1 e0) e0) e1) )  (= (op (op e2 e0) e0) e2) )  (= (op (op e3 e0) e0) e3) )  (= (op (op e4 e0) e0) e4) )  (= (op (op e5 e0) e0) e5) ) (or (or (or (or (or (= (op (op e0 e1) e1) e0)  (= (op (op e1 e1) e1) e1) )  (= (op (op e2 e1) e1) e2) )  (= (op (op e3 e1) e1) e3) )  (= (op (op e4 e1) e1) e4) )  (= (op (op e5 e1) e1) e5) )) (or (or (or (or (or (= (op (op e0 e2) e2) e0)  (= (op (op e1 e2) e2) e1) )  (= (op (op e2 e2) e2) e2) )  (= (op (op e3 e2) e2) e3) )  (= (op (op e4 e2) e2) e4) )  (= (op (op e5 e2) e2) e5) )) (or (or (or (or (or (= (op (op e0 e3) e3) e0)  (= (op (op e1 e3) e3) e1) )  (= (op (op e2 e3) e3) e2) )  (= (op (op e3 e3) e3) e3) )  (= (op (op e4 e3) e3) e4) )  (= (op (op e5 e3) e3) e5) )) (or (or (or (or (or (= (op (op e0 e4) e4) e0)  (= (op (op e1 e4) e4) e1) )  (= (op (op e2 e4) e4) e2) )  (= (op (op e3 e4) e4) e3) )  (= (op (op e4 e4) e4) e4) )  (= (op (op e5 e4) e4) e5) )) (or (or (or (or (or (= (op (op e0 e5) e5) e0)  (= (op (op e1 e5) e5) e1) )  (= (op (op e2 e5) e5) e2) )  (= (op (op e3 e5) e5) e3) )  (= (op (op e4 e5) e5) e4) )  (= (op (op e5 e5) e5) e5) ))
+  :assumption
+(let (?cvc_0 (op e0 e0)) (let (?cvc_6 (op e0 e1)) (let (?cvc_12 (op e0 e2)) (let (?cvc_18 (op e0 e3)) (let (?cvc_24 (op e0 e4)) (let (?cvc_30 (op e0 e5)) (let (?cvc_1 (op e1 e0)) (let (?cvc_7 (op e1 e1)) (let (?cvc_13 (op e1 e2)) (let (?cvc_19 (op e1 e3)) (let (?cvc_25 (op e1 e4)) (let (?cvc_31 (op e1 e5)) (let (?cvc_2 (op e2 e0)) (let (?cvc_8 (op e2 e1)) (let (?cvc_14 (op e2 e2)) (let (?cvc_20 (op e2 e3)) (let (?cvc_26 (op e2 e4)) (let (?cvc_32 (op e2 e5)) (let (?cvc_3 (op e3 e0)) (let (?cvc_9 (op e3 e1)) (let (?cvc_15 (op e3 e2)) (let (?cvc_21 (op e3 e3)) (let (?cvc_27 (op e3 e4)) (let (?cvc_33 (op e3 e5)) (let (?cvc_4 (op e4 e0)) (let (?cvc_10 (op e4 e1)) (let (?cvc_16 (op e4 e2)) (let (?cvc_22 (op e4 e3)) (let (?cvc_28 (op e4 e4)) (let (?cvc_34 (op e4 e5)) (let (?cvc_5 (op e5 e0)) (let (?cvc_11 (op e5 e1)) (let (?cvc_17 (op e5 e2)) (let (?cvc_23 (op e5 e3)) (let (?cvc_29 (op e5 e4)) (let (?cvc_35 (op e5 e5)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?cvc_0 ?cvc_1)) (not (= ?cvc_0 ?cvc_2))) (not (= ?cvc_0 ?cvc_3))) (not (= ?cvc_0 ?cvc_4))) (not (= ?cvc_0 ?cvc_5))) (not (= ?cvc_1 ?cvc_2))) (not (= ?cvc_1 ?cvc_3))) (not (= ?cvc_1 ?cvc_4))) (not (= ?cvc_1 ?cvc_5))) (not (= ?cvc_2 ?cvc_3))) (not (= ?cvc_2 ?cvc_4))) (not (= ?cvc_2 ?cvc_5))) (not (= ?cvc_3 ?cvc_4))) (not (= ?cvc_3 ?cvc_5))) (not (= ?cvc_4 ?cvc_5))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?cvc_6 ?cvc_7)) (not (= ?cvc_6 ?cvc_8))) (not (= ?cvc_6 ?cvc_9))) (not (= ?cvc_6 ?cvc_10))) (not (= ?cvc_6 ?cvc_11))) (not (= ?cvc_7 ?cvc_8))) (not (= ?cvc_7 ?cvc_9))) (not (= ?cvc_7 ?cvc_10))) (not (= ?cvc_7 ?cvc_11))) (not (= ?cvc_8 ?cvc_9))) (not (= ?cvc_8 ?cvc_10))) (not (= ?cvc_8 ?cvc_11))) (not (= ?cvc_9 ?cvc_10))) (not (= ?cvc_9 ?cvc_11))) (not (= ?cvc_10 ?cvc_11)))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?cvc_12 ?cvc_13)) (not (= ?cvc_12 ?cvc_14))) (not (= ?cvc_12 ?cvc_15))) (not (= ?cvc_12 ?cvc_16))) (not (= ?cvc_12 ?cvc_17))) (not (= ?cvc_13 ?cvc_14))) (not (= ?cvc_13 ?cvc_15))) (not (= ?cvc_13 ?cvc_16))) (not (= ?cvc_13 ?cvc_17))) (not (= ?cvc_14 ?cvc_15))) (not (= ?cvc_14 ?cvc_16))) (not (= ?cvc_14 ?cvc_17))) (not (= ?cvc_15 ?cvc_16))) (not (= ?cvc_15 ?cvc_17))) (not (= ?cvc_16 ?cvc_17)))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?cvc_18 ?cvc_19)) (not (= ?cvc_18 ?cvc_20))) (not (= ?cvc_18 ?cvc_21))) (not (= ?cvc_18 ?cvc_22))) (not (= ?cvc_18 ?cvc_23))) (not (= ?cvc_19 ?cvc_20))) (not (= ?cvc_19 ?cvc_21))) (not (= ?cvc_19 ?cvc_22))) (not (= ?cvc_19 ?cvc_23))) (not (= ?cvc_20 ?cvc_21))) (not (= ?cvc_20 ?cvc_22))) (not (= ?cvc_20 ?cvc_23))) (not (= ?cvc_21 ?cvc_22))) (not (= ?cvc_21 ?cvc_23))) (not (= ?cvc_22 ?cvc_23)))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?cvc_24 ?cvc_25)) (not (= ?cvc_24 ?cvc_26))) (not (= ?cvc_24 ?cvc_27))) (not (= ?cvc_24 ?cvc_28))) (not (= ?cvc_24 ?cvc_29))) (not (= ?cvc_25 ?cvc_26))) (not (= ?cvc_25 ?cvc_27))) (not (= ?cvc_25 ?cvc_28))) (not (= ?cvc_25 ?cvc_29))) (not (= ?cvc_26 ?cvc_27))) (not (= ?cvc_26 ?cvc_28))) (not (= ?cvc_26 ?cvc_29))) (not (= ?cvc_27 ?cvc_28))) (not (= ?cvc_27 ?cvc_29))) (not (= ?cvc_28 ?cvc_29)))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?cvc_30 ?cvc_31)) (not (= ?cvc_30 ?cvc_32))) (not (= ?cvc_30 ?cvc_33))) (not (= ?cvc_30 ?cvc_34))) (not (= ?cvc_30 ?cvc_35))) (not (= ?cvc_31 ?cvc_32))) (not (= ?cvc_31 ?cvc_33))) (not (= ?cvc_31 ?cvc_34))) (not (= ?cvc_31 ?cvc_35))) (not (= ?cvc_32 ?cvc_33))) (not (= ?cvc_32 ?cvc_34))) (not (= ?cvc_32 ?cvc_35))) (not (= ?cvc_33 ?cvc_34))) (not (= ?cvc_33 ?cvc_35))) (not (= ?cvc_34 ?cvc_35)))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?cvc_0 ?cvc_6)) (not (= ?cvc_0 ?cvc_12))) (not (= ?cvc_0 ?cvc_18))) (not (= ?cvc_0 ?cvc_24))) (not (= ?cvc_0 ?cvc_30))) (not (= ?cvc_6 ?cvc_12))) (not (= ?cvc_6 ?cvc_18))) (not (= ?cvc_6 ?cvc_24))) (not (= ?cvc_6 ?cvc_30))) (not (= ?cvc_12 ?cvc_18))) (not (= ?cvc_12 ?cvc_24))) (not (= ?cvc_12 ?cvc_30))) (not (= ?cvc_18 ?cvc_24))) (not (= ?cvc_18 ?cvc_30))) (not (= ?cvc_24 ?cvc_30))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?cvc_1 ?cvc_7)) (not (= ?cvc_1 ?cvc_13))) (not (= ?cvc_1 ?cvc_19))) (not (= ?cvc_1 ?cvc_25))) (not (= ?cvc_1 ?cvc_31))) (not (= ?cvc_7 ?cvc_13))) (not (= ?cvc_7 ?cvc_19))) (not (= ?cvc_7 ?cvc_25))) (not (= ?cvc_7 ?cvc_31))) (not (= ?cvc_13 ?cvc_19))) (not (= ?cvc_13 ?cvc_25))) (not (= ?cvc_13 ?cvc_31))) (not (= ?cvc_19 ?cvc_25))) (not (= ?cvc_19 ?cvc_31))) (not (= ?cvc_25 ?cvc_31)))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?cvc_2 ?cvc_8)) (not (= ?cvc_2 ?cvc_14))) (not (= ?cvc_2 ?cvc_20))) (not (= ?cvc_2 ?cvc_26))) (not (= ?cvc_2 ?cvc_32))) (not (= ?cvc_8 ?cvc_14))) (not (= ?cvc_8 ?cvc_20))) (not (= ?cvc_8 ?cvc_26))) (not (= ?cvc_8 ?cvc_32))) (not (= ?cvc_14 ?cvc_20))) (not (= ?cvc_14 ?cvc_26))) (not (= ?cvc_14 ?cvc_32))) (not (= ?cvc_20 ?cvc_26))) (not (= ?cvc_20 ?cvc_32))) (not (= ?cvc_26 ?cvc_32)))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?cvc_3 ?cvc_9)) (not (= ?cvc_3 ?cvc_15))) (not (= ?cvc_3 ?cvc_21))) (not (= ?cvc_3 ?cvc_27))) (not (= ?cvc_3 ?cvc_33))) (not (= ?cvc_9 ?cvc_15))) (not (= ?cvc_9 ?cvc_21))) (not (= ?cvc_9 ?cvc_27))) (not (= ?cvc_9 ?cvc_33))) (not (= ?cvc_15 ?cvc_21))) (not (= ?cvc_15 ?cvc_27))) (not (= ?cvc_15 ?cvc_33))) (not (= ?cvc_21 ?cvc_27))) (not (= ?cvc_21 ?cvc_33))) (not (= ?cvc_27 ?cvc_33)))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?cvc_4 ?cvc_10)) (not (= ?cvc_4 ?cvc_16))) (not (= ?cvc_4 ?cvc_22))) (not (= ?cvc_4 ?cvc_28))) (not (= ?cvc_4 ?cvc_34))) (not (= ?cvc_10 ?cvc_16))) (not (= ?cvc_10 ?cvc_22))) (not (= ?cvc_10 ?cvc_28))) (not (= ?cvc_10 ?cvc_34))) (not (= ?cvc_16 ?cvc_22))) (not (= ?cvc_16 ?cvc_28))) (not (= ?cvc_16 ?cvc_34))) (not (= ?cvc_22 ?cvc_28))) (not (= ?cvc_22 ?cvc_34))) (not (= ?cvc_28 ?cvc_34)))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?cvc_5 ?cvc_11)) (not (= ?cvc_5 ?cvc_17))) (not (= ?cvc_5 ?cvc_23))) (not (= ?cvc_5 ?cvc_29))) (not (= ?cvc_5 ?cvc_35))) (not (= ?cvc_11 ?cvc_17))) (not (= ?cvc_11 ?cvc_23))) (not (= ?cvc_11 ?cvc_29))) (not (= ?cvc_11 ?cvc_35))) (not (= ?cvc_17 ?cvc_23))) (not (= ?cvc_17 ?cvc_29))) (not (= ?cvc_17 ?cvc_35))) (not (= ?cvc_23 ?cvc_29))) (not (= ?cvc_23 ?cvc_35))) (not (= ?cvc_29 ?cvc_35)))))))))))))))))))))))))))))))))))))))))
+  :assumption
+(and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= e0 e1)) (not (= e0 e2))) (not (= e0 e3))) (not (= e0 e4))) (not (= e0 e5))) (not (= e1 e2))) (not (= e1 e3))) (not (= e1 e4))) (not (= e1 e5))) (not (= e2 e3))) (not (= e2 e4))) (not (= e2 e5))) (not (= e3 e4))) (not (= e3 e5))) (not (= e4 e5)))
+  :assumption
+(let (?cvc_0 (op e5 e5)) (let (?cvc_3 (op e5 ?cvc_0)) (let (?cvc_1 (op e5 ?cvc_3)) (let (?cvc_2 (op ?cvc_1 ?cvc_1)) (let (?cvc_4 (op e5 ?cvc_2)) (not (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= e5 (op ?cvc_0 ?cvc_0)) (= ?cvc_2 (op ?cvc_0 ?cvc_2))) (= ?cvc_4 (op ?cvc_0 ?cvc_3))) (= ?cvc_3 (op ?cvc_0 e5))) (= ?cvc_1 (op ?cvc_0 ?cvc_4))) (= ?cvc_0 (op ?cvc_0 ?cvc_1))) (= ?cvc_0 (op ?cvc_2 ?cvc_0))) (= ?cvc_3 (op ?cvc_2 ?cvc_2))) (= ?cvc_2 (op ?cvc_2 ?cvc_3))) (= ?cvc_1 (op ?cvc_2 e5))) (= e5 (op ?cvc_2 ?cvc_4))) (= ?cvc_4 (op ?cvc_2 ?cvc_1))) (= ?cvc_4 (op ?cvc_3 ?cvc_0))) (= ?cvc_1 (op ?cvc_3 ?cvc_2))) (= e5 (op ?cvc_3 ?cvc_3))) (= ?cvc_2 (op ?cvc_3 e5))) (= ?cvc_0 (op ?cvc_3 ?cvc_4))) (= ?cvc_3 (op ?cvc_3 ?cvc_1))) (= ?cvc_3 ?cvc_3)) (= ?cvc_4 ?cvc_4)) (= ?cvc_1 ?cvc_1)) (= ?cvc_0 ?cvc_0)) (= ?cvc_2 (op e5 ?cvc_4))) (= e5 (op e5 ?cvc_1))) (= ?cvc_2 (op ?cvc_4 ?cvc_0))) (= e5 (op ?cvc_4 ?cvc_2))) (= ?cvc_0 (op ?cvc_4 ?cvc_3))) (= ?cvc_4 (op ?cvc_4 e5))) (= ?cvc_3 (op ?cvc_4 ?cvc_4))) (= ?cvc_1 (op ?cvc_4 ?cvc_1))) (= ?cvc_1 (op ?cvc_1 ?cvc_0))) (= ?cvc_0 (op ?cvc_1 ?cvc_2))) (= ?cvc_3 (op ?cvc_1 ?cvc_3))) (= e5 (op ?cvc_1 e5))) (= ?cvc_4 (op ?cvc_1 ?cvc_4))) (= ?cvc_2 ?cvc_2)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?cvc_0 ?cvc_2)) (not (= ?cvc_0 ?cvc_3))) (not (= ?cvc_0 e5))) (not (= ?cvc_0 ?cvc_4))) (not (= ?cvc_0 ?cvc_1))) (not (= ?cvc_2 ?cvc_0))) (not (= ?cvc_2 ?cvc_3))) (not (= ?cvc_2 e5))) (not (= ?cvc_2 ?cvc_4))) (not (= ?cvc_2 ?cvc_1))) (not (= ?cvc_3 ?cvc_0))) (not (= ?cvc_3 ?cvc_2))) (not (= ?cvc_3 e5))) (not (= ?cvc_3 ?cvc_4))) (not (= ?cvc_3 ?cvc_1))) (not (= e5 ?cvc_0))) (not (= e5 ?cvc_2))) (not (= e5 ?cvc_3))) (not (= e5 ?cvc_4))) (not (= e5 ?cvc_1))) (not (= ?cvc_4 ?cvc_0))) (not (= ?cvc_4 ?cvc_2))) (not (= ?cvc_4 ?cvc_3))) (not (= ?cvc_4 e5))) (not (= ?cvc_4 ?cvc_1))) (not (= ?cvc_1 ?cvc_0))) (not (= ?cvc_1 ?cvc_2))) (not (= ?cvc_1 ?cvc_3))) (not (= ?cvc_1 e5))) (not (= ?cvc_1 ?cvc_4))))))))))
+  :assumption
+(let (?cvc_0 (op e4 e4)) (let (?cvc_3 (op e4 ?cvc_0)) (let (?cvc_1 (op e4 ?cvc_3)) (let (?cvc_2 (op ?cvc_1 ?cvc_1)) (let (?cvc_4 (op e4 ?cvc_2)) (not (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= e4 (op ?cvc_0 ?cvc_0)) (= ?cvc_2 (op ?cvc_0 ?cvc_2))) (= ?cvc_4 (op ?cvc_0 ?cvc_3))) (= ?cvc_3 (op ?cvc_0 e4))) (= ?cvc_1 (op ?cvc_0 ?cvc_4))) (= ?cvc_0 (op ?cvc_0 ?cvc_1))) (= ?cvc_0 (op ?cvc_2 ?cvc_0))) (= ?cvc_3 (op ?cvc_2 ?cvc_2))) (= ?cvc_2 (op ?cvc_2 ?cvc_3))) (= ?cvc_1 (op ?cvc_2 e4))) (= e4 (op ?cvc_2 ?cvc_4))) (= ?cvc_4 (op ?cvc_2 ?cvc_1))) (= ?cvc_4 (op ?cvc_3 ?cvc_0))) (= ?cvc_1 (op ?cvc_3 ?cvc_2))) (= e4 (op ?cvc_3 ?cvc_3))) (= ?cvc_2 (op ?cvc_3 e4))) (= ?cvc_0 (op ?cvc_3 ?cvc_4))) (= ?cvc_3 (op ?cvc_3 ?cvc_1))) (= ?cvc_3 ?cvc_3)) (= ?cvc_4 ?cvc_4)) (= ?cvc_1 ?cvc_1)) (= ?cvc_0 ?cvc_0)) (= ?cvc_2 (op e4 ?cvc_4))) (= e4 (op e4 ?cvc_1))) (= ?cvc_2 (op ?cvc_4 ?cvc_0))) (= e4 (op ?cvc_4 ?cvc_2))) (= ?cvc_0 (op ?cvc_4 ?cvc_3))) (= ?cvc_4 (op ?cvc_4 e4))) (= ?cvc_3 (op ?cvc_4 ?cvc_4))) (= ?cvc_1 (op ?cvc_4 ?cvc_1))) (= ?cvc_1 (op ?cvc_1 ?cvc_0))) (= ?cvc_0 (op ?cvc_1 ?cvc_2))) (= ?cvc_3 (op ?cvc_1 ?cvc_3))) (= e4 (op ?cvc_1 e4))) (= ?cvc_4 (op ?cvc_1 ?cvc_4))) (= ?cvc_2 ?cvc_2)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?cvc_0 ?cvc_2)) (not (= ?cvc_0 ?cvc_3))) (not (= ?cvc_0 e4))) (not (= ?cvc_0 ?cvc_4))) (not (= ?cvc_0 ?cvc_1))) (not (= ?cvc_2 ?cvc_0))) (not (= ?cvc_2 ?cvc_3))) (not (= ?cvc_2 e4))) (not (= ?cvc_2 ?cvc_4))) (not (= ?cvc_2 ?cvc_1))) (not (= ?cvc_3 ?cvc_0))) (not (= ?cvc_3 ?cvc_2))) (not (= ?cvc_3 e4))) (not (= ?cvc_3 ?cvc_4))) (not (= ?cvc_3 ?cvc_1))) (not (= e4 ?cvc_0))) (not (= e4 ?cvc_2))) (not (= e4 ?cvc_3))) (not (= e4 ?cvc_4))) (not (= e4 ?cvc_1))) (not (= ?cvc_4 ?cvc_0))) (not (= ?cvc_4 ?cvc_2))) (not (= ?cvc_4 ?cvc_3))) (not (= ?cvc_4 e4))) (not (= ?cvc_4 ?cvc_1))) (not (= ?cvc_1 ?cvc_0))) (not (= ?cvc_1 ?cvc_2))) (not (= ?cvc_1 ?cvc_3))) (not (= ?cvc_1 e4))) (not (= ?cvc_1 ?cvc_4))))))))))
+  :assumption
+(let (?cvc_0 (op e3 e3)) (let (?cvc_3 (op e3 ?cvc_0)) (let (?cvc_1 (op e3 ?cvc_3)) (let (?cvc_2 (op ?cvc_1 ?cvc_1)) (let (?cvc_4 (op e3 ?cvc_2)) (not (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= e3 (op ?cvc_0 ?cvc_0)) (= ?cvc_2 (op ?cvc_0 ?cvc_2))) (= ?cvc_4 (op ?cvc_0 ?cvc_3))) (= ?cvc_3 (op ?cvc_0 e3))) (= ?cvc_1 (op ?cvc_0 ?cvc_4))) (= ?cvc_0 (op ?cvc_0 ?cvc_1))) (= ?cvc_0 (op ?cvc_2 ?cvc_0))) (= ?cvc_3 (op ?cvc_2 ?cvc_2))) (= ?cvc_2 (op ?cvc_2 ?cvc_3))) (= ?cvc_1 (op ?cvc_2 e3))) (= e3 (op ?cvc_2 ?cvc_4))) (= ?cvc_4 (op ?cvc_2 ?cvc_1))) (= ?cvc_4 (op ?cvc_3 ?cvc_0))) (= ?cvc_1 (op ?cvc_3 ?cvc_2))) (= e3 (op ?cvc_3 ?cvc_3))) (= ?cvc_2 (op ?cvc_3 e3))) (= ?cvc_0 (op ?cvc_3 ?cvc_4))) (= ?cvc_3 (op ?cvc_3 ?cvc_1))) (= ?cvc_3 ?cvc_3)) (= ?cvc_4 ?cvc_4)) (= ?cvc_1 ?cvc_1)) (= ?cvc_0 ?cvc_0)) (= ?cvc_2 (op e3 ?cvc_4))) (= e3 (op e3 ?cvc_1))) (= ?cvc_2 (op ?cvc_4 ?cvc_0))) (= e3 (op ?cvc_4 ?cvc_2))) (= ?cvc_0 (op ?cvc_4 ?cvc_3))) (= ?cvc_4 (op ?cvc_4 e3))) (= ?cvc_3 (op ?cvc_4 ?cvc_4))) (= ?cvc_1 (op ?cvc_4 ?cvc_1))) (= ?cvc_1 (op ?cvc_1 ?cvc_0))) (= ?cvc_0 (op ?cvc_1 ?cvc_2))) (= ?cvc_3 (op ?cvc_1 ?cvc_3))) (= e3 (op ?cvc_1 e3))) (= ?cvc_4 (op ?cvc_1 ?cvc_4))) (= ?cvc_2 ?cvc_2)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?cvc_0 ?cvc_2)) (not (= ?cvc_0 ?cvc_3))) (not (= ?cvc_0 e3))) (not (= ?cvc_0 ?cvc_4))) (not (= ?cvc_0 ?cvc_1))) (not (= ?cvc_2 ?cvc_0))) (not (= ?cvc_2 ?cvc_3))) (not (= ?cvc_2 e3))) (not (= ?cvc_2 ?cvc_4))) (not (= ?cvc_2 ?cvc_1))) (not (= ?cvc_3 ?cvc_0))) (not (= ?cvc_3 ?cvc_2))) (not (= ?cvc_3 e3))) (not (= ?cvc_3 ?cvc_4))) (not (= ?cvc_3 ?cvc_1))) (not (= e3 ?cvc_0))) (not (= e3 ?cvc_2))) (not (= e3 ?cvc_3))) (not (= e3 ?cvc_4))) (not (= e3 ?cvc_1))) (not (= ?cvc_4 ?cvc_0))) (not (= ?cvc_4 ?cvc_2))) (not (= ?cvc_4 ?cvc_3))) (not (= ?cvc_4 e3))) (not (= ?cvc_4 ?cvc_1))) (not (= ?cvc_1 ?cvc_0))) (not (= ?cvc_1 ?cvc_2))) (not (= ?cvc_1 ?cvc_3))) (not (= ?cvc_1 e3))) (not (= ?cvc_1 ?cvc_4))))))))))
+  :assumption
+(let (?cvc_0 (op e2 e2)) (let (?cvc_3 (op e2 ?cvc_0)) (let (?cvc_1 (op e2 ?cvc_3)) (let (?cvc_2 (op ?cvc_1 ?cvc_1)) (let (?cvc_4 (op e2 ?cvc_2)) (not (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= e2 (op ?cvc_0 ?cvc_0)) (= ?cvc_2 (op ?cvc_0 ?cvc_2))) (= ?cvc_4 (op ?cvc_0 ?cvc_3))) (= ?cvc_3 (op ?cvc_0 e2))) (= ?cvc_1 (op ?cvc_0 ?cvc_4))) (= ?cvc_0 (op ?cvc_0 ?cvc_1))) (= ?cvc_0 (op ?cvc_2 ?cvc_0))) (= ?cvc_3 (op ?cvc_2 ?cvc_2))) (= ?cvc_2 (op ?cvc_2 ?cvc_3))) (= ?cvc_1 (op ?cvc_2 e2))) (= e2 (op ?cvc_2 ?cvc_4))) (= ?cvc_4 (op ?cvc_2 ?cvc_1))) (= ?cvc_4 (op ?cvc_3 ?cvc_0))) (= ?cvc_1 (op ?cvc_3 ?cvc_2))) (= e2 (op ?cvc_3 ?cvc_3))) (= ?cvc_2 (op ?cvc_3 e2))) (= ?cvc_0 (op ?cvc_3 ?cvc_4))) (= ?cvc_3 (op ?cvc_3 ?cvc_1))) (= ?cvc_3 ?cvc_3)) (= ?cvc_4 ?cvc_4)) (= ?cvc_1 ?cvc_1)) (= ?cvc_0 ?cvc_0)) (= ?cvc_2 (op e2 ?cvc_4))) (= e2 (op e2 ?cvc_1))) (= ?cvc_2 (op ?cvc_4 ?cvc_0))) (= e2 (op ?cvc_4 ?cvc_2))) (= ?cvc_0 (op ?cvc_4 ?cvc_3))) (= ?cvc_4 (op ?cvc_4 e2))) (= ?cvc_3 (op ?cvc_4 ?cvc_4))) (= ?cvc_1 (op ?cvc_4 ?cvc_1))) (= ?cvc_1 (op ?cvc_1 ?cvc_0))) (= ?cvc_0 (op ?cvc_1 ?cvc_2))) (= ?cvc_3 (op ?cvc_1 ?cvc_3))) (= e2 (op ?cvc_1 e2))) (= ?cvc_4 (op ?cvc_1 ?cvc_4))) (= ?cvc_2 ?cvc_2)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?cvc_0 ?cvc_2)) (not (= ?cvc_0 ?cvc_3))) (not (= ?cvc_0 e2))) (not (= ?cvc_0 ?cvc_4))) (not (= ?cvc_0 ?cvc_1))) (not (= ?cvc_2 ?cvc_0))) (not (= ?cvc_2 ?cvc_3))) (not (= ?cvc_2 e2))) (not (= ?cvc_2 ?cvc_4))) (not (= ?cvc_2 ?cvc_1))) (not (= ?cvc_3 ?cvc_0))) (not (= ?cvc_3 ?cvc_2))) (not (= ?cvc_3 e2))) (not (= ?cvc_3 ?cvc_4))) (not (= ?cvc_3 ?cvc_1))) (not (= e2 ?cvc_0))) (not (= e2 ?cvc_2))) (not (= e2 ?cvc_3))) (not (= e2 ?cvc_4))) (not (= e2 ?cvc_1))) (not (= ?cvc_4 ?cvc_0))) (not (= ?cvc_4 ?cvc_2))) (not (= ?cvc_4 ?cvc_3))) (not (= ?cvc_4 e2))) (not (= ?cvc_4 ?cvc_1))) (not (= ?cvc_1 ?cvc_0))) (not (= ?cvc_1 ?cvc_2))) (not (= ?cvc_1 ?cvc_3))) (not (= ?cvc_1 e2))) (not (= ?cvc_1 ?cvc_4))))))))))
+  :assumption
+(let (?cvc_0 (op e1 e1)) (let (?cvc_3 (op e1 ?cvc_0)) (let (?cvc_1 (op e1 ?cvc_3)) (let (?cvc_2 (op ?cvc_1 ?cvc_1)) (let (?cvc_4 (op e1 ?cvc_2)) (not (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= e1 (op ?cvc_0 ?cvc_0)) (= ?cvc_2 (op ?cvc_0 ?cvc_2))) (= ?cvc_4 (op ?cvc_0 ?cvc_3))) (= ?cvc_3 (op ?cvc_0 e1))) (= ?cvc_1 (op ?cvc_0 ?cvc_4))) (= ?cvc_0 (op ?cvc_0 ?cvc_1))) (= ?cvc_0 (op ?cvc_2 ?cvc_0))) (= ?cvc_3 (op ?cvc_2 ?cvc_2))) (= ?cvc_2 (op ?cvc_2 ?cvc_3))) (= ?cvc_1 (op ?cvc_2 e1))) (= e1 (op ?cvc_2 ?cvc_4))) (= ?cvc_4 (op ?cvc_2 ?cvc_1))) (= ?cvc_4 (op ?cvc_3 ?cvc_0))) (= ?cvc_1 (op ?cvc_3 ?cvc_2))) (= e1 (op ?cvc_3 ?cvc_3))) (= ?cvc_2 (op ?cvc_3 e1))) (= ?cvc_0 (op ?cvc_3 ?cvc_4))) (= ?cvc_3 (op ?cvc_3 ?cvc_1))) (= ?cvc_3 ?cvc_3)) (= ?cvc_4 ?cvc_4)) (= ?cvc_1 ?cvc_1)) (= ?cvc_0 ?cvc_0)) (= ?cvc_2 (op e1 ?cvc_4))) (= e1 (op e1 ?cvc_1))) (= ?cvc_2 (op ?cvc_4 ?cvc_0))) (= e1 (op ?cvc_4 ?cvc_2))) (= ?cvc_0 (op ?cvc_4 ?cvc_3))) (= ?cvc_4 (op ?cvc_4 e1))) (= ?cvc_3 (op ?cvc_4 ?cvc_4))) (= ?cvc_1 (op ?cvc_4 ?cvc_1))) (= ?cvc_1 (op ?cvc_1 ?cvc_0))) (= ?cvc_0 (op ?cvc_1 ?cvc_2))) (= ?cvc_3 (op ?cvc_1 ?cvc_3))) (= e1 (op ?cvc_1 e1))) (= ?cvc_4 (op ?cvc_1 ?cvc_4))) (= ?cvc_2 ?cvc_2)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?cvc_0 ?cvc_2)) (not (= ?cvc_0 ?cvc_3))) (not (= ?cvc_0 e1))) (not (= ?cvc_0 ?cvc_4))) (not (= ?cvc_0 ?cvc_1))) (not (= ?cvc_2 ?cvc_0))) (not (= ?cvc_2 ?cvc_3))) (not (= ?cvc_2 e1))) (not (= ?cvc_2 ?cvc_4))) (not (= ?cvc_2 ?cvc_1))) (not (= ?cvc_3 ?cvc_0))) (not (= ?cvc_3 ?cvc_2))) (not (= ?cvc_3 e1))) (not (= ?cvc_3 ?cvc_4))) (not (= ?cvc_3 ?cvc_1))) (not (= e1 ?cvc_0))) (not (= e1 ?cvc_2))) (not (= e1 ?cvc_3))) (not (= e1 ?cvc_4))) (not (= e1 ?cvc_1))) (not (= ?cvc_4 ?cvc_0))) (not (= ?cvc_4 ?cvc_2))) (not (= ?cvc_4 ?cvc_3))) (not (= ?cvc_4 e1))) (not (= ?cvc_4 ?cvc_1))) (not (= ?cvc_1 ?cvc_0))) (not (= ?cvc_1 ?cvc_2))) (not (= ?cvc_1 ?cvc_3))) (not (= ?cvc_1 e1))) (not (= ?cvc_1 ?cvc_4))))))))))
+  :assumption
+(let (?cvc_0 (op e0 e0)) (let (?cvc_3 (op e0 ?cvc_0)) (let (?cvc_1 (op e0 ?cvc_3)) (let (?cvc_2 (op ?cvc_1 ?cvc_1)) (let (?cvc_4 (op e0 ?cvc_2)) (not (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= e0 (op ?cvc_0 ?cvc_0)) (= ?cvc_2 (op ?cvc_0 ?cvc_2))) (= ?cvc_4 (op ?cvc_0 ?cvc_3))) (= ?cvc_3 (op ?cvc_0 e0))) (= ?cvc_1 (op ?cvc_0 ?cvc_4))) (= ?cvc_0 (op ?cvc_0 ?cvc_1))) (= ?cvc_0 (op ?cvc_2 ?cvc_0))) (= ?cvc_3 (op ?cvc_2 ?cvc_2))) (= ?cvc_2 (op ?cvc_2 ?cvc_3))) (= ?cvc_1 (op ?cvc_2 e0))) (= e0 (op ?cvc_2 ?cvc_4))) (= ?cvc_4 (op ?cvc_2 ?cvc_1))) (= ?cvc_4 (op ?cvc_3 ?cvc_0))) (= ?cvc_1 (op ?cvc_3 ?cvc_2))) (= e0 (op ?cvc_3 ?cvc_3))) (= ?cvc_2 (op ?cvc_3 e0))) (= ?cvc_0 (op ?cvc_3 ?cvc_4))) (= ?cvc_3 (op ?cvc_3 ?cvc_1))) (= ?cvc_3 ?cvc_3)) (= ?cvc_4 ?cvc_4)) (= ?cvc_1 ?cvc_1)) (= ?cvc_0 ?cvc_0)) (= ?cvc_2 (op e0 ?cvc_4))) (= e0 (op e0 ?cvc_1))) (= ?cvc_2 (op ?cvc_4 ?cvc_0))) (= e0 (op ?cvc_4 ?cvc_2))) (= ?cvc_0 (op ?cvc_4 ?cvc_3))) (= ?cvc_4 (op ?cvc_4 e0))) (= ?cvc_3 (op ?cvc_4 ?cvc_4))) (= ?cvc_1 (op ?cvc_4 ?cvc_1))) (= ?cvc_1 (op ?cvc_1 ?cvc_0))) (= ?cvc_0 (op ?cvc_1 ?cvc_2))) (= ?cvc_3 (op ?cvc_1 ?cvc_3))) (= e0 (op ?cvc_1 e0))) (= ?cvc_4 (op ?cvc_1 ?cvc_4))) (= ?cvc_2 ?cvc_2)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?cvc_0 ?cvc_2)) (not (= ?cvc_0 ?cvc_3))) (not (= ?cvc_0 e0))) (not (= ?cvc_0 ?cvc_4))) (not (= ?cvc_0 ?cvc_1))) (not (= ?cvc_2 ?cvc_0))) (not (= ?cvc_2 ?cvc_3))) (not (= ?cvc_2 e0))) (not (= ?cvc_2 ?cvc_4))) (not (= ?cvc_2 ?cvc_1))) (not (= ?cvc_3 ?cvc_0))) (not (= ?cvc_3 ?cvc_2))) (not (= ?cvc_3 e0))) (not (= ?cvc_3 ?cvc_4))) (not (= ?cvc_3 ?cvc_1))) (not (= e0 ?cvc_0))) (not (= e0 ?cvc_2))) (not (= e0 ?cvc_3))) (not (= e0 ?cvc_4))) (not (= e0 ?cvc_1))) (not (= ?cvc_4 ?cvc_0))) (not (= ?cvc_4 ?cvc_2))) (not (= ?cvc_4 ?cvc_3))) (not (= ?cvc_4 e0))) (not (= ?cvc_4 ?cvc_1))) (not (= ?cvc_1 ?cvc_0))) (not (= ?cvc_1 ?cvc_2))) (not (= ?cvc_1 ?cvc_3))) (not (= ?cvc_1 e0))) (not (= ?cvc_1 ?cvc_4))))))))))
+  :formula
+(not false)
+)