read_only = true
help = "interleave full saturate instantiation with other techniques"
+[[option]]
+ name = "fullSaturateStratify"
+ category = "regular"
+ long = "fs-stratify"
+ type = "bool"
+ default = "false"
+ read_only = true
+ help = "stratify effort levels in enumerative instantiation, which favors speed over fairness"
+
[[option]]
name = "literalMatchMode"
category = "regular"
doCheck = quant_e == QEFFORT_LAST_CALL;
fullEffort = !d_quantEngine->hasAddedLemma();
}
- if (doCheck)
+ if (!doCheck)
{
- double clSet = 0;
- if (Trace.isOn("fs-engine"))
- {
- clSet = double(clock()) / double(CLOCKS_PER_SEC);
- Trace("fs-engine") << "---Full Saturation Round, effort = " << e << "---"
- << std::endl;
- }
- int addedLemmas = 0;
- for (unsigned i = 0;
- i < d_quantEngine->getModel()->getNumAssertedQuantifiers();
- i++)
+ return;
+ }
+ double clSet = 0;
+ if (Trace.isOn("fs-engine"))
+ {
+ clSet = double(clock()) / double(CLOCKS_PER_SEC);
+ Trace("fs-engine") << "---Full Saturation Round, effort = " << e << "---"
+ << std::endl;
+ }
+ unsigned rstart = options::fullSaturateQuantRd() ? 0 : 1;
+ unsigned rend = fullEffort ? 1 : rstart;
+ unsigned addedLemmas = 0;
+ // First try in relevant domain of all quantified formulas, if no
+ // instantiations exist, try arbitrary ground terms.
+ // Notice that this stratification of effort levels makes it so that some
+ // quantified formulas may not be instantiated (if they have no instances
+ // at effort level r=0 but another quantified formula does). We prefer
+ // this stratification since effort level r=1 may be highly expensive in the
+ // case where we have a quantified formula with many entailed instances.
+ FirstOrderModel* fm = d_quantEngine->getModel();
+ RelevantDomain* rd = d_quantEngine->getRelevantDomain();
+ unsigned nquant = fm->getNumAssertedQuantifiers();
+ std::map<Node, bool> alreadyProc;
+ for (unsigned r = rstart; r <= rend; r++)
+ {
+ if (rd || r > 0)
{
- Node q = d_quantEngine->getModel()->getAssertedQuantifier(i, true);
- if (d_quantEngine->hasOwnership(q, this)
- && d_quantEngine->getModel()->isQuantifierActive(q))
+ if (r == 0)
+ {
+ Trace("inst-alg") << "-> Relevant domain instantiate..." << std::endl;
+ Trace("inst-alg-debug") << "Compute relevant domain..." << std::endl;
+ rd->compute();
+ Trace("inst-alg-debug") << "...finished" << std::endl;
+ }
+ else
+ {
+ Trace("inst-alg") << "-> Ground term instantiate..." << std::endl;
+ }
+ for (unsigned i = 0; i < nquant; i++)
{
- if (process(q, fullEffort))
+ Node q = fm->getAssertedQuantifier(i, true);
+ bool doProcess = d_quantEngine->hasOwnership(q, this)
+ && fm->isQuantifierActive(q)
+ && alreadyProc.find(q) == alreadyProc.end();
+ if (doProcess)
{
- // added lemma
- addedLemmas++;
- if (d_quantEngine->inConflict())
+ if (process(q, fullEffort, r == 0))
{
- break;
+ // don't need to mark this if we are not stratifying
+ if (!options::fullSaturateStratify())
+ {
+ alreadyProc[q] = true;
+ }
+ // added lemma
+ addedLemmas++;
+ if (d_quantEngine->inConflict())
+ {
+ break;
+ }
}
}
}
+ if (d_quantEngine->inConflict()
+ || (addedLemmas > 0 && options::fullSaturateStratify()))
+ {
+ // we break if we are in conflict, or if we added any lemma at this
+ // effort level and we stratify effort levels.
+ break;
+ }
}
- if (Trace.isOn("fs-engine"))
- {
- Trace("fs-engine") << "Added lemmas = " << addedLemmas << std::endl;
- double clSet2 = double(clock()) / double(CLOCKS_PER_SEC);
- Trace("fs-engine") << "Finished full saturation engine, time = "
- << (clSet2 - clSet) << std::endl;
- }
+ }
+ if (Trace.isOn("fs-engine"))
+ {
+ Trace("fs-engine") << "Added lemmas = " << addedLemmas << std::endl;
+ double clSet2 = double(clock()) / double(CLOCKS_PER_SEC);
+ Trace("fs-engine") << "Finished full saturation engine, time = "
+ << (clSet2 - clSet) << std::endl;
}
}
-bool InstStrategyEnum::process(Node f, bool fullEffort)
+bool InstStrategyEnum::process(Node f, bool fullEffort, bool isRd)
{
// ignore if constant true (rare case of non-standard quantifier whose body is
// rewritten to true)
{
return false;
}
- // first, try from relevant domain
RelevantDomain* rd = d_quantEngine->getRelevantDomain();
- unsigned rstart = options::fullSaturateQuantRd() ? 0 : 1;
- unsigned rend = fullEffort ? 1 : rstart;
- for (unsigned r = rstart; r <= rend; r++)
+ unsigned final_max_i = 0;
+ std::vector<unsigned> maxs;
+ std::vector<bool> max_zero;
+ bool has_zero = false;
+ std::map<TypeNode, std::vector<Node> > term_db_list;
+ std::vector<TypeNode> ftypes;
+ TermDb* tdb = d_quantEngine->getTermDatabase();
+ EqualityQuery* qy = d_quantEngine->getEqualityQuery();
+ // iterate over substitutions for variables
+ for (unsigned i = 0; i < f[0].getNumChildren(); i++)
{
- if (rd || r > 0)
+ TypeNode tn = f[0][i].getType();
+ ftypes.push_back(tn);
+ unsigned ts;
+ if (isRd)
{
- if (r == 0)
+ ts = rd->getRDomain(f, i)->d_terms.size();
+ }
+ else
+ {
+ ts = tdb->getNumTypeGroundTerms(tn);
+ std::map<TypeNode, std::vector<Node> >::iterator ittd =
+ term_db_list.find(tn);
+ if (ittd == term_db_list.end())
{
- Trace("inst-alg") << "-> Relevant domain instantiate " << f << "..."
- << std::endl;
- Trace("inst-alg-debug") << "Compute relevant domain..." << std::endl;
- rd->compute();
- Trace("inst-alg-debug") << "...finished" << std::endl;
+ std::map<Node, Node> reps_found;
+ for (unsigned j = 0; j < ts; j++)
+ {
+ Node gt = tdb->getTypeGroundTerm(ftypes[i], j);
+ if (!options::cbqi() || !quantifiers::TermUtil::hasInstConstAttr(gt))
+ {
+ Node rep = qy->getRepresentative(gt);
+ if (reps_found.find(rep) == reps_found.end())
+ {
+ reps_found[rep] = gt;
+ term_db_list[tn].push_back(gt);
+ }
+ }
+ }
+ ts = term_db_list[tn].size();
}
else
{
- Trace("inst-alg") << "-> Ground term instantiate " << f << "..."
- << std::endl;
+ ts = ittd->second.size();
}
- unsigned final_max_i = 0;
- std::vector<unsigned> maxs;
- std::vector<bool> max_zero;
- bool has_zero = false;
- std::map<TypeNode, std::vector<Node> > term_db_list;
- std::vector<TypeNode> ftypes;
- // iterate over substitutions for variables
- for (unsigned i = 0; i < f[0].getNumChildren(); i++)
+ }
+ // consider a default value if at full effort
+ max_zero.push_back(fullEffort && ts == 0);
+ ts = (fullEffort && ts == 0) ? 1 : ts;
+ Trace("inst-alg-rd") << "Variable " << i << " has " << ts
+ << " in relevant domain." << std::endl;
+ if (ts == 0)
+ {
+ has_zero = true;
+ break;
+ }
+ maxs.push_back(ts);
+ if (ts > final_max_i)
+ {
+ final_max_i = ts;
+ }
+ }
+ if (!has_zero)
+ {
+ Trace("inst-alg-rd") << "Will do " << final_max_i
+ << " stages of instantiation." << std::endl;
+ unsigned max_i = 0;
+ bool success;
+ Instantiate* ie = d_quantEngine->getInstantiate();
+ while (max_i <= final_max_i)
+ {
+ Trace("inst-alg-rd") << "Try stage " << max_i << "..." << std::endl;
+ std::vector<unsigned> childIndex;
+ int index = 0;
+ do
{
- TypeNode tn = f[0][i].getType();
- ftypes.push_back(tn);
- unsigned ts;
- if (r == 0)
- {
- ts = rd->getRDomain(f, i)->d_terms.size();
- }
- else
+ while (index >= 0 && index < (int)f[0].getNumChildren())
{
- ts = d_quantEngine->getTermDatabase()->getNumTypeGroundTerms(tn);
- std::map<TypeNode, std::vector<Node> >::iterator ittd =
- term_db_list.find(tn);
- if (ittd == term_db_list.end())
+ if (index == static_cast<int>(childIndex.size()))
{
- std::map<Node, Node> reps_found;
- for (unsigned j = 0; j < ts; j++)
- {
- Node gt = d_quantEngine->getTermDatabase()->getTypeGroundTerm(
- ftypes[i], j);
- if (!options::cbqi()
- || !quantifiers::TermUtil::hasInstConstAttr(gt))
- {
- Node rep =
- d_quantEngine->getEqualityQuery()->getRepresentative(gt);
- if (reps_found.find(rep) == reps_found.end())
- {
- reps_found[rep] = gt;
- term_db_list[tn].push_back(gt);
- }
- }
- }
- ts = term_db_list[tn].size();
+ childIndex.push_back(-1);
}
else
{
- ts = ittd->second.size();
+ Assert(index == static_cast<int>(childIndex.size()) - 1);
+ unsigned nv = childIndex[index] + 1;
+ if (nv < maxs[index] && nv <= max_i)
+ {
+ childIndex[index] = nv;
+ index++;
+ }
+ else
+ {
+ childIndex.pop_back();
+ index--;
+ }
}
}
- // consider a default value if at full effort
- max_zero.push_back(fullEffort && ts == 0);
- ts = (fullEffort && ts == 0) ? 1 : ts;
- Trace("inst-alg-rd") << "Variable " << i << " has " << ts
- << " in relevant domain." << std::endl;
- if (ts == 0)
+ success = index >= 0;
+ if (success)
{
- has_zero = true;
- break;
- }
- else
- {
- maxs.push_back(ts);
- if (ts > final_max_i)
+ if (Trace.isOn("inst-alg-rd"))
{
- final_max_i = ts;
+ Trace("inst-alg-rd") << "Try instantiation { ";
+ for (unsigned i : childIndex)
+ {
+ Trace("inst-alg-rd") << i << " ";
+ }
+ Trace("inst-alg-rd") << "}" << std::endl;
}
- }
- }
- if (!has_zero)
- {
- Trace("inst-alg-rd") << "Will do " << final_max_i
- << " stages of instantiation." << std::endl;
- unsigned max_i = 0;
- bool success;
- while (max_i <= final_max_i)
- {
- Trace("inst-alg-rd") << "Try stage " << max_i << "..." << std::endl;
- std::vector<unsigned> childIndex;
- int index = 0;
- do
+ // try instantiation
+ std::vector<Node> terms;
+ for (unsigned i = 0, nchild = f[0].getNumChildren(); i < nchild; i++)
{
- while (index >= 0 && index < (int)f[0].getNumChildren())
+ if (max_zero[i])
{
- if (index == (int)childIndex.size())
- {
- childIndex.push_back(-1);
- }
- else
- {
- Assert(index == (int)(childIndex.size()) - 1);
- unsigned nv = childIndex[index] + 1;
- if (nv < maxs[index] && nv <= max_i)
- {
- childIndex[index] = nv;
- index++;
- }
- else
- {
- childIndex.pop_back();
- index--;
- }
- }
+ // no terms available, will report incomplete instantiation
+ terms.push_back(Node::null());
+ Trace("inst-alg-rd") << " null" << std::endl;
}
- success = index >= 0;
- if (success)
+ else if (isRd)
{
- Trace("inst-alg-rd") << "Try instantiation { ";
- for (unsigned j = 0; j < childIndex.size(); j++)
- {
- Trace("inst-alg-rd") << childIndex[j] << " ";
- }
- Trace("inst-alg-rd") << "}" << std::endl;
- // try instantiation
- std::vector<Node> terms;
- for (unsigned i = 0; i < f[0].getNumChildren(); i++)
- {
- if (max_zero[i])
- {
- // no terms available, will report incomplete instantiation
- terms.push_back(Node::null());
- Trace("inst-alg-rd") << " null" << std::endl;
- }
- else if (r == 0)
- {
- terms.push_back(rd->getRDomain(f, i)->d_terms[childIndex[i]]);
- Trace("inst-alg-rd")
- << " " << rd->getRDomain(f, i)->d_terms[childIndex[i]]
- << std::endl;
- }
- else
- {
- Assert(childIndex[i] < term_db_list[ftypes[i]].size());
- terms.push_back(term_db_list[ftypes[i]][childIndex[i]]);
- Trace("inst-alg-rd") << " "
- << term_db_list[ftypes[i]][childIndex[i]]
- << std::endl;
- }
- }
- if (d_quantEngine->getInstantiate()->addInstantiation(f, terms))
- {
- Trace("inst-alg-rd") << "Success!" << std::endl;
- ++(d_quantEngine->d_statistics.d_instantiations_guess);
- return true;
- }
- else
- {
- index--;
- }
+ terms.push_back(rd->getRDomain(f, i)->d_terms[childIndex[i]]);
+ Trace("inst-alg-rd")
+ << " " << rd->getRDomain(f, i)->d_terms[childIndex[i]]
+ << std::endl;
}
- } while (success);
- max_i++;
+ else
+ {
+ Assert(childIndex[i] < term_db_list[ftypes[i]].size());
+ terms.push_back(term_db_list[ftypes[i]][childIndex[i]]);
+ Trace("inst-alg-rd")
+ << " " << term_db_list[ftypes[i]][childIndex[i]]
+ << std::endl;
+ }
+ }
+ if (ie->addInstantiation(f, terms))
+ {
+ Trace("inst-alg-rd") << "Success!" << std::endl;
+ ++(d_quantEngine->d_statistics.d_instantiations_guess);
+ return true;
+ }
+ else
+ {
+ index--;
+ }
}
- }
+ } while (success);
+ max_i++;
}
}
// TODO : term enumerator instantiation?
* well-typed term *not* occurring in the current context.
* This handles corner cases where there are no well-typed
* ground terms in the current context to instantiate with.
+ *
+ * The flag isRd indicates whether we are trying relevant domain
+ * instantiations. If this flag is false, we are trying arbitrary ground
+ * term instantiations.
*/
- bool process(Node q, bool fullEffort);
+ bool process(Node q, bool fullEffort, bool isRd);
}; /* class InstStrategyEnum */
} /* CVC4::theory::quantifiers namespace */
regress2/quantifiers/mutualrec2.cvc
regress2/quantifiers/net-policy-no-time.smt2
regress2/quantifiers/nunchaku2309663.nun.min.smt2
+ regress2/quantifiers/syn874-1.smt2
regress2/simplify.javafe.ast.ArrayInit.35_without_quantification2.smt2
regress2/strings/cmu-dis-0707-3.smt2
regress2/strings/cmu-disagree-0707-dd.smt2
--- /dev/null
+; COMMAND-LINE: --full-saturate-quant --fs-stratify
+; EXPECT: unsat
+(set-logic ALL)
+(declare-sort $$unsorted 0)
+(declare-fun ssNder1_0 () Bool)
+(declare-fun ssNder1_1r1 ($$unsorted) Bool)
+(declare-fun ssNder1_2r1r1 ($$unsorted $$unsorted) Bool)
+(declare-fun ssNder1_3r1r1r1 ($$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun ssNder1_4r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun skc30 () $$unsorted)
+(declare-fun ssPv16_5r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun skc31 () $$unsorted)
+(declare-fun ssNder1_5r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun skc28 () $$unsorted)
+(declare-fun ssPv15_6r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun skc29 () $$unsorted)
+(declare-fun ssNder1_6r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun skc26 () $$unsorted)
+(declare-fun ssPv14_7r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun skc27 () $$unsorted)
+(declare-fun ssNder1_7r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun skc24 () $$unsorted)
+(declare-fun ssPv13_8r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun skc25 () $$unsorted)
+(declare-fun ssNder1_8r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun ssNder1_9r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun ssNder1_10r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun skc22 () $$unsorted)
+(declare-fun ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun skc23 () $$unsorted)
+(declare-fun ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun skc20 () $$unsorted)
+(declare-fun ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun skc21 () $$unsorted)
+(declare-fun ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun skc18 () $$unsorted)
+(declare-fun ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun skc19 () $$unsorted)
+(declare-fun ssPv10_11r1r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun ssPv20_1r1 ($$unsorted) Bool)
+(declare-fun ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun skc16 () $$unsorted)
+(declare-fun ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun skc17 () $$unsorted)
+(declare-fun ssPv12_9r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun ssPv19_2r1r1 ($$unsorted $$unsorted) Bool)
+(declare-fun ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun ssPv17_4r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun ssPv18_3r1r1r1 ($$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun ssPv11_10r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(meta-info :filename "SYN874-1")
+(assert true)
+(assert (forall ((U $$unsorted)) (ssNder1_1r1 U) ))
+(assert (forall ((U $$unsorted) (V $$unsorted)) (or (not (ssNder1_1r1 U)) (ssNder1_2r1r1 U V)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted)) (or (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssNder1_3r1r1r1 U V W)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted)) (or (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssNder1_4r1r1r1r1 U V W X)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted)) (or (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv16_5r1r1r1r1r1 U V W X skc30)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted)) (or (not (ssPv16_5r1r1r1r1r1 U V W X skc31)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U))) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted)) (or (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssNder1_5r1r1r1r1r1 U V W X Y)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted)) (or (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv15_6r1r1r1r1r1r1 U V W X Y skc28)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted)) (or (not (ssPv15_6r1r1r1r1r1r1 U V W X Y skc29)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U))) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted)) (or (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted)) (or (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv14_7r1r1r1r1r1r1r1 U V W X Y Z skc26)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted)) (or (not (ssPv14_7r1r1r1r1r1r1r1 U V W X Y Z skc27)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U))) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted)) (or (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted)) (or (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv13_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 skc24)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted)) (or (not (ssPv13_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 skc25)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U))) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted)) (or (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted)) (or (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted)) (or (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted)) (or (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted)) (or (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted)) (or (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 skc22)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted)) (or (not (ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 skc23)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U))) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted)) (or (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted)) (or (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 skc20)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted)) (or (not (ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 skc21)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U))) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted)) (or (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted)) (or (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 skc18)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted)) (or (not (ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 skc19)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U))) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted)) (or (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssPv10_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssPv15_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv20_1r1 U)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted)) (or (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted)) (or (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 skc16)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted)) (or (not (ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 skc17)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U))) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted)) (or (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssPv12_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssPv20_1r1 U)) (not (ssNder1_1r1 U)) (ssPv16_5r1r1r1r1r1 U V W X Y)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted)) (or (not (ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssPv10_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv13_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted)) (or (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssPv10_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssPv13_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssPv19_2r1r1 U V)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U))) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted)) (or (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted)) (or (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssPv20_1r1 U)) (not (ssNder1_1r1 U)) (ssPv19_2r1r1 U V)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted)) (or (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssPv15_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssPv20_1r1 U)) (not (ssNder1_1r1 U)) (ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10) (ssPv17_4r1r1r1r1 U V W X)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted)) (or (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted)) (or (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssPv12_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9) (ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted)) (or (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssPv12_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssPv14_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10) (ssPv20_1r1 U)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted)) (or (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssPv17_4r1r1r1r1 U V W X)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U))) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted) (X12 $$unsorted)) (or (not (ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted)) (or (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssPv20_1r1 U)) (not (ssNder1_1r1 U)) (ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11) (ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9) (ssPv15_6r1r1r1r1r1r1 U V W X Y Z)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted)) (or (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssPv19_2r1r1 U V)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10) (ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11) (ssPv16_5r1r1r1r1r1 U V W X Y)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted)) (or (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8) (ssPv13_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2) (ssPv18_3r1r1r1 U V W)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted)) (or (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssPv13_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssPv18_3r1r1r1 U V W)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted)) (or (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssPv13_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11) (ssPv10_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted) (X12 $$unsorted) (X13 $$unsorted)) (or (not (ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12)) (not (ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted)) (or (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10) (ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9) (ssPv12_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted)) (or (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted) (X12 $$unsorted)) (or (not (ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12) (ssPv15_6r1r1r1r1r1r1 U V W X Y Z) (ssPv16_5r1r1r1r1r1 U V W X Y)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted) (X12 $$unsorted)) (or (not (ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) (not (ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12)) (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv15_6r1r1r1r1r1r1 U V W X Y Z) (ssPv17_4r1r1r1r1 U V W X)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted) (X12 $$unsorted) (X13 $$unsorted)) (or (not (ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12)) (not (ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssPv15_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssPv16_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssPv17_4r1r1r1r1 U V W X)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted) (X12 $$unsorted) (X13 $$unsorted)) (or (not (ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12)) (not (ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13)) (not (ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8) (ssPv15_6r1r1r1r1r1r1 U V W X Y Z) (ssPv20_1r1 U)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted) (X12 $$unsorted)) (or (not (ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) (not (ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12)) (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted) (X12 $$unsorted) (X13 $$unsorted)) (or (not (ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12)) (not (ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssPv14_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13) (ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6) (ssPv13_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted) (X12 $$unsorted) (X13 $$unsorted)) (or (not (ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12)) (not (ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13)) (not (ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssPv13_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssPv20_1r1 U)) (not (ssNder1_1r1 U)) (ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted) (X12 $$unsorted) (X13 $$unsorted)) (or (not (ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12)) (not (ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) (not (ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssPv18_3r1r1r1 U V W)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13) (ssPv14_7r1r1r1r1r1r1r1 U V W X Y Z X1)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted) (X12 $$unsorted) (X13 $$unsorted)) (or (not (ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12)) (not (ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13) (ssPv11_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4) (ssPv13_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted) (X12 $$unsorted) (X13 $$unsorted)) (or (not (ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12)) (not (ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13)) (not (ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssPv17_4r1r1r1r1 U V W X)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9) (ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted) (X12 $$unsorted) (X13 $$unsorted)) (or (not (ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12)) (not (ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13)) (not (ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssPv15_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11) (ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted) (X12 $$unsorted) (X13 $$unsorted)) (or (not (ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12)) (not (ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) (not (ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssPv13_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13) (ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted) (X12 $$unsorted) (X13 $$unsorted) (X14 $$unsorted)) (or (not (ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13)) (not (ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14)) (not (ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12)) (not (ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssPv12_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssPv14_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv13_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted) (X12 $$unsorted) (X13 $$unsorted) (X14 $$unsorted)) (or (not (ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13)) (not (ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14)) (not (ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12)) (not (ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10) (ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9) (ssPv19_2r1r1 U V)) ))
+(assert true)
+(check-sat)
projects / cvc5.git / commitdiff