diff options
| -rw-r--r-- | src/theory/datatypes/datatypes_rewriter.h | 64 | ||||
| -rw-r--r-- | src/theory/datatypes/theory_datatypes.cpp | 114 | ||||
| -rw-r--r-- | src/theory/datatypes/theory_datatypes.h | 2 | ||||
| -rw-r--r-- | src/theory/datatypes/type_enumerator.cpp | 6 | ||||
| -rw-r--r-- | src/theory/datatypes/type_enumerator.h | 3 | ||||
| -rw-r--r-- | src/theory/quantifiers/ce_guided_instantiation.cpp | 10 | ||||
| -rw-r--r-- | src/theory/quantifiers/first_order_model.cpp | 24 | ||||
| -rw-r--r-- | src/theory/quantifiers/first_order_model.h | 3 | ||||
| -rw-r--r-- | src/theory/quantifiers/full_model_check.cpp | 125 | ||||
| -rw-r--r-- | src/theory/quantifiers/full_model_check.h | 8 | ||||
| -rw-r--r-- | src/theory/quantifiers/term_database.cpp | 10 | ||||
| -rw-r--r-- | src/theory/quantifiers_engine.cpp | 4 | ||||
| -rw-r--r-- | src/theory/theory_model.cpp | 11 | ||||
| -rw-r--r-- | src/theory/theory_model.h | 1 | ||||
| -rw-r--r-- | src/theory/uf/theory_uf.cpp | 2 | ||||
| -rw-r--r-- | test/regress/regress0/fmf/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/fmf/nun-0208-to.smt2 | 180 | ||||
| -rw-r--r-- | test/regress/regress0/quantifiers/Makefile.am | 5 | ||||
| -rw-r--r-- | test/regress/regress0/quantifiers/cdt-0208-to.smt2 | 767 |
19 files changed, 1164 insertions, 178 deletions
diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index da2282a2c..1e7e714cf 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -167,19 +167,19 @@ public: //typically should not be called TypeNode tn = in.getType(); Node gt; - if( tn.isSort() ){ + bool useTe = true; + //if( !tn.isSort() ){ + // useTe = false; + //} + if( isTypeDatatype( tn ) ){ + const Datatype& dta = ((DatatypeType)(tn).toType()).getDatatype(); + useTe = !dta.isCodatatype(); + } + if( useTe ){ TypeEnumerator te(tn); gt = *te; }else{ - //check whether well-founded - //bool isWf = true; - //if( isTypeDatatype( tn ) ){ - // const Datatype& dta = ((DatatypeType)(tn).toType()).getDatatype(); - // isWf = dta.isWellFounded(); - //} - //if( isWf || in[0].isConst() ){ gt = tn.mkGroundTerm(); - //} } if( !gt.isNull() ){ //Assert( gtt.isDatatype() || gtt.isParametricDatatype() ); @@ -531,28 +531,32 @@ private: } //eqc_stack stores depth static Node normalizeCodatatypeConstantEqc( Node n, std::map< int, int >& eqc_stack, std::map< Node, int >& eqc, int depth ){ - Assert( eqc.find( n )!=eqc.end() ); - int e = eqc[n]; - std::map< int, int >::iterator it = eqc_stack.find( e ); - if( it!=eqc_stack.end() ){ - int debruijn = depth - it->second - 1; - return NodeManager::currentNM()->mkConst(UninterpretedConstant(n.getType().toType(), debruijn)); + Trace("dt-nconst-debug") << "normalizeCodatatypeConstantEqc: " << n << " depth=" << depth << std::endl; + if( eqc.find( n )==eqc.end() ){ + return n; }else{ - std::vector< Node > children; - bool childChanged = false; - eqc_stack[e] = depth; - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - Node nc = normalizeCodatatypeConstantEqc( n[i], eqc_stack, eqc, depth+1 ); - children.push_back( nc ); - childChanged = childChanged || nc!=n[i]; - } - eqc_stack.erase(e); - if( childChanged ){ - Assert( n.getKind()==kind::APPLY_CONSTRUCTOR ); - children.insert( children.begin(), n.getOperator() ); - return NodeManager::currentNM()->mkNode( n.getKind(), children ); + int e = eqc[n]; + std::map< int, int >::iterator it = eqc_stack.find( e ); + if( it!=eqc_stack.end() ){ + int debruijn = depth - it->second - 1; + return NodeManager::currentNM()->mkConst(UninterpretedConstant(n.getType().toType(), debruijn)); }else{ - return n; + std::vector< Node > children; + bool childChanged = false; + eqc_stack[e] = depth; + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + Node nc = normalizeCodatatypeConstantEqc( n[i], eqc_stack, eqc, depth+1 ); + children.push_back( nc ); + childChanged = childChanged || nc!=n[i]; + } + eqc_stack.erase(e); + if( childChanged ){ + Assert( n.getKind()==kind::APPLY_CONSTRUCTOR ); + children.insert( children.begin(), n.getOperator() ); + return NodeManager::currentNM()->mkNode( n.getKind(), children ); + }else{ + return n; + } } } } @@ -675,7 +679,7 @@ public: eqc[it->first] = eqc[it->second]; } //we now have a partition of equivalent terms - Trace("dt-nconst") << "Equivalence classes ids : " << std::endl; + Trace("dt-nconst") << "Computed equivalence classes ids : " << std::endl; for( std::map< Node, int >::iterator it = eqc.begin(); it != eqc.end(); ++it ){ Trace("dt-nconst") << " " << it->first << " -> " << it->second << std::endl; } diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 439fd0cfb..c8d7338a7 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -268,12 +268,13 @@ void TheoryDatatypes::check(Effort e) { } if( needSplit && consIndex!=-1 ) { - //if only one constructor, then this term must be this constructor if( dt.getNumConstructors()==1 ){ + //this may not be necessary? + //if only one constructor, then this term must be this constructor Node t = DatatypesRewriter::mkTester( n, 0, dt ); d_pending.push_back( t ); d_pending_exp[ t ] = d_true; - Trace("datatypes-infer") << "DtInfer : 1-cons : " << t << std::endl; + Trace("datatypes-infer") << "DtInfer : 1-cons (full) : " << t << std::endl; d_infer.push_back( t ); }else{ if( options::dtBinarySplit() ){ @@ -402,11 +403,14 @@ void TheoryDatatypes::doPendingMerges(){ d_pending_merge.clear(); } -void TheoryDatatypes::doSendLemma( Node lem ) { +bool TheoryDatatypes::doSendLemma( Node lem ) { if( d_lemmas_produced_c.find( lem )==d_lemmas_produced_c.end() ){ Trace("dt-lemma-send") << "TheoryDatatypes::doSendLemma : " << lem << std::endl; d_lemmas_produced_c[lem] = true; d_out->lemma( lem ); + return true; + }else{ + return false; } } @@ -440,7 +444,6 @@ void TheoryDatatypes::assertFact( Node fact, Node exp ){ Trace("dt-lemma-sygus") << "Sygus symmetry breaking lemma : " << d_sygus_sym_break->d_lemmas[i] << std::endl; doSendLemma( d_sygus_sym_break->d_lemmas[i] ); } - Trace("dt-lemma-sygus") << "No lemmas" << std::endl; d_sygus_sym_break->d_lemmas.clear(); /* if( d_sygus_util->d_conflict ){ @@ -1124,8 +1127,8 @@ void TheoryDatatypes::addTester( int ttindex, Node t, EqcInfo* eqc, Node n, Node nb << (*i); Assert( (*i).getKind()==NOT ); Node t_arg2; - int tindex = DatatypesRewriter::isTester( (*i)[0], t_arg2 ); - Assert( tindex!=-1 ); + DatatypesRewriter::isTester( (*i)[0], t_arg2 ); + //Assert( tindex!=-1 ); if( std::find( eq_terms.begin(), eq_terms.end(), t_arg2 )==eq_terms.end() ){ eq_terms.push_back( t_arg2 ); if( t_arg2!=t_arg ){ @@ -1569,46 +1572,31 @@ void TheoryDatatypes::collectTerms( Node n ) { if( n.getKind() == APPLY_CONSTRUCTOR ){ Debug("datatypes") << " Found constructor " << n << endl; d_consTerms.push_back( n ); - }else if( n.getKind() == APPLY_SELECTOR_TOTAL || n.getKind() == DT_SIZE || n.getKind() == DT_HEIGHT_BOUND ){ - d_selTerms.push_back( n ); - //we must also record which selectors exist - Trace("dt-collapse-sel") << " Found selector " << n << endl; - Node rep = getRepresentative( n[0] ); - //record it in the selectors - EqcInfo* eqc = getOrMakeEqcInfo( rep, true ); - //add it to the eqc info - addSelector( n, eqc, rep ); - - if( n.getKind() == DT_SIZE ){ - Node conc = NodeManager::currentNM()->mkNode( LEQ, NodeManager::currentNM()->mkConst( Rational(0) ), n ); - //must be non-negative - Trace("datatypes-infer") << "DtInfer : non-negative size : " << conc << std::endl; - d_pending.push_back( conc ); - d_pending_exp[ conc ] = d_true; - d_infer.push_back( conc ); -/* - //add size = 0 lemma - Node nn = n.eqNode( NodeManager::currentNM()->mkConst( Rational(0) ) ); - std::vector< Node > children; - children.push_back( nn.negate() ); - const Datatype& dt = ((DatatypeType)(n[0].getType()).toType()).getDatatype(); - for( unsigned i=0; i<dt.getNumConstructors(); i++ ){ - if( DatatypesRewriter::isNullaryConstructor( dt[i] ) ){ - Node test = DatatypesRewriter::mkTester( n[0], i, dt ); - children.push_back( test ); - } - } - conc = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( OR, children ); - Trace("datatypes-infer") << "DtInfer : zero size : " << conc << std::endl; - d_pending.push_back( conc ); - d_pending_exp[ conc ] = d_true; - d_infer.push_back( conc ); -*/ - } + }else{ - if( n.getKind() == DT_HEIGHT_BOUND ){ - if( n[1].getConst<Rational>().isZero() ){ + if( n.getKind() == APPLY_SELECTOR_TOTAL || n.getKind() == DT_SIZE || n.getKind() == DT_HEIGHT_BOUND ){ + d_selTerms.push_back( n ); + //we must also record which selectors exist + Trace("dt-collapse-sel") << " Found selector " << n << endl; + Node rep = getRepresentative( n[0] ); + //record it in the selectors + EqcInfo* eqc = getOrMakeEqcInfo( rep, true ); + //add it to the eqc info + addSelector( n, eqc, rep ); + + if( n.getKind() == DT_SIZE ){ + Node conc = NodeManager::currentNM()->mkNode( LEQ, NodeManager::currentNM()->mkConst( Rational(0) ), n ); + //must be non-negative + Trace("datatypes-infer") << "DtInfer : non-negative size : " << conc << std::endl; + //d_pending.push_back( conc ); + //d_pending_exp[ conc ] = d_true; + //d_infer.push_back( conc ); + d_pending_lem.push_back( conc ); + /* + //add size = 0 lemma + Node nn = n.eqNode( NodeManager::currentNM()->mkConst( Rational(0) ) ); std::vector< Node > children; + children.push_back( nn.negate() ); const Datatype& dt = ((DatatypeType)(n[0].getType()).toType()).getDatatype(); for( unsigned i=0; i<dt.getNumConstructors(); i++ ){ if( DatatypesRewriter::isNullaryConstructor( dt[i] ) ){ @@ -1616,16 +1604,36 @@ void TheoryDatatypes::collectTerms( Node n ) { children.push_back( test ); } } - Node lem; - if( children.empty() ){ - lem = n.negate(); - }else{ - lem = NodeManager::currentNM()->mkNode( IFF, n, children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( OR, children ) ); + conc = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( OR, children ); + Trace("datatypes-infer") << "DtInfer : zero size : " << conc << std::endl; + d_pending.push_back( conc ); + d_pending_exp[ conc ] = d_true; + d_infer.push_back( conc ); + */ + } + + if( n.getKind() == DT_HEIGHT_BOUND ){ + if( n[1].getConst<Rational>().isZero() ){ + std::vector< Node > children; + const Datatype& dt = ((DatatypeType)(n[0].getType()).toType()).getDatatype(); + for( unsigned i=0; i<dt.getNumConstructors(); i++ ){ + if( DatatypesRewriter::isNullaryConstructor( dt[i] ) ){ + Node test = DatatypesRewriter::mkTester( n[0], i, dt ); + children.push_back( test ); + } + } + Node lem; + if( children.empty() ){ + lem = n.negate(); + }else{ + lem = NodeManager::currentNM()->mkNode( IFF, n, children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( OR, children ) ); + } + Trace("datatypes-infer") << "DtInfer : zero height : " << lem << std::endl; + //d_pending.push_back( lem ); + //d_pending_exp[ lem ] = d_true; + //d_infer.push_back( lem ); + d_pending_lem.push_back( lem ); } - Trace("datatypes-infer") << "DtInfer : zero height : " << lem << std::endl; - d_pending.push_back( lem ); - d_pending_exp[ lem ] = d_true; - d_infer.push_back( lem ); } } } diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 4dd621c86..d56538b2a 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -203,7 +203,7 @@ private: /** do pending merged */ void doPendingMerges(); /** do send lemma */ - void doSendLemma( Node lem ); + bool doSendLemma( Node lem ); /** get or make eqc info */ EqcInfo* getOrMakeEqcInfo( TNode n, bool doMake = false ); diff --git a/src/theory/datatypes/type_enumerator.cpp b/src/theory/datatypes/type_enumerator.cpp index 57d16d31c..62446a937 100644 --- a/src/theory/datatypes/type_enumerator.cpp +++ b/src/theory/datatypes/type_enumerator.cpp @@ -170,7 +170,9 @@ Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){ Debug("dt-enum") << "datatype is datatype? " << d_type.isDatatype() << std::endl; Debug("dt-enum") << "datatype is kind " << d_type.getKind() << std::endl; Debug("dt-enum") << "datatype is " << d_type << std::endl; - Debug("dt-enum") << "properties : " << d_datatype.isCodatatype() << " " << d_datatype.isRecursiveSingleton() << " " << d_datatype.isFinite() << std::endl; + Debug("dt-enum") << "properties : " << d_datatype.isCodatatype() << " " << d_datatype.isRecursiveSingleton(); + Debug("dt-enum") << " " << d_datatype.isFinite() << std::endl; + Debug("dt-enum") << " " << d_datatype.isUFinite() << std::endl; if( d_datatype.isCodatatype() && hasCyclesDt( d_datatype ) ){ //start with uninterpreted constant @@ -218,4 +220,4 @@ Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){ //set up initial conditions (should always succeed) ++*this; //increment( d_ctor ); AlwaysAssert( !isFinished() ); -}
\ No newline at end of file +} diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h index 67dabafe4..921ba403c 100644 --- a/src/theory/datatypes/type_enumerator.h +++ b/src/theory/datatypes/type_enumerator.h @@ -23,6 +23,7 @@ #include "expr/type_node.h" #include "expr/type.h" #include "expr/kind.h" +#include "options/quantifiers_options.h" namespace CVC4 { namespace theory { @@ -158,7 +159,7 @@ public: } if( d_ctor>=d_has_debruijn+d_datatype.getNumConstructors() ){ //try next size limit as long as new terms were generated at last size, or other cases - if( prevSize==d_size_limit || ( d_size_limit==0 && d_datatype.isCodatatype() ) || !d_datatype.isFinite() ){ + if( prevSize==d_size_limit || ( d_size_limit==0 && d_datatype.isCodatatype() ) || ( options::finiteModelFind() ? !d_datatype.isUFinite() : !d_datatype.isFinite() ) ){ d_size_limit++; d_ctor = d_zeroCtor; for( unsigned i=0; i<d_sel_sum.size(); i++ ){ diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index cc0b18ffe..345a5eaef 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -463,9 +463,13 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { lem = Rewriter::rewrite( lem ); Trace("cegqi-lemma") << "Cegqi::Lemma : candidate refinement : " << lem << std::endl; Trace("cegqi-engine") << " ...refine candidate." << std::endl; - d_quantEngine->addLemma( lem ); - ++(d_statistics.d_cegqi_lemmas_refine); - conj->d_refine_count++; + bool res = d_quantEngine->addLemma( lem ); + if( res ){ + ++(d_statistics.d_cegqi_lemmas_refine); + conj->d_refine_count++; + }else{ + Trace("cegqi-engine") << " ...FAILED to add refinement!" << std::endl; + } } } conj->d_ce_sk.clear(); diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index aa2a43fbf..272f16be8 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -90,15 +90,19 @@ void FirstOrderModel::initialize() { } processInitializeQuantifier( f ); //initialize relevant models within bodies of all quantifiers - initializeModelForTerm( f[1] ); + std::map< Node, bool > visited; + initializeModelForTerm( f[1], visited ); } processInitialize( false ); } -void FirstOrderModel::initializeModelForTerm( Node n ){ - processInitializeModelForTerm( n ); - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - initializeModelForTerm( n[i] ); +void FirstOrderModel::initializeModelForTerm( Node n, std::map< Node, bool >& visited ){ + if( visited.find( n )==visited.end() ){ + visited[n] = true; + processInitializeModelForTerm( n ); + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + initializeModelForTerm( n[i], visited ); + } } } @@ -574,15 +578,6 @@ Node FirstOrderModelFmc::getUsedRepresentative(Node n, bool strict) { Trace("fmc-warn") << "WARNING : no representative for " << n << std::endl; } } -/* - Node r = getRepresentative(n); - if( d_model_basis_rep.find(tn)!=d_model_basis_rep.end() ){ - if (r==d_model_basis_rep[tn]) { - r = d_qe->getTermDatabase()->getModelBasisTerm(tn); - } - } - return r; -*/ return getRepresentative(n); } } @@ -609,7 +604,6 @@ void FirstOrderModelFmc::processInitialize( bool ispre ) { for( std::map<Node, Def * >::iterator it = d_models.begin(); it != d_models.end(); ++it ){ it->second->reset(); } - d_model_basis_rep.clear(); } } diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index a31e85d7e..d42eb61e3 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -67,7 +67,7 @@ public: //for Theory Quantifiers: /** get number to reduce quantifiers */ unsigned getNumToReduceQuantifiers() { return d_forall_to_reduce.size(); } /** initialize model for term */ - void initializeModelForTerm( Node n ); + void initializeModelForTerm( Node n, std::map< Node, bool >& visited ); virtual void processInitializeModelForTerm( Node n ) = 0; virtual void processInitializeQuantifier( Node q ) {} public: @@ -169,7 +169,6 @@ class FirstOrderModelFmc : public FirstOrderModel private: /** models for UF */ std::map<Node, Def * > d_models; - std::map<TypeNode, Node > d_model_basis_rep; std::map<TypeNode, Node > d_type_star; Node intervalOp; Node getUsedRepresentative(Node n, bool strict = false); diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index f0858f4e9..00a5241f5 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -325,11 +325,46 @@ QModelBuilder( c, qe ){ d_false = NodeManager::currentNM()->mkConst(false); } +void FullModelChecker::preProcessBuildModel(TheoryModel* m, bool fullModel) { + FirstOrderModelFmc * fm = ((FirstOrderModelFmc*)m)->asFirstOrderModelFmc(); + if( !fullModel ){ + Trace("fmc") << "---Full Model Check preprocess() " << std::endl; + d_preinitialized_types.clear(); + //traverse equality engine + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( fm->d_equalityEngine ); + std::map< TypeNode, int > typ_num; + while( !eqcs_i.isFinished() ){ + TypeNode tr = (*eqcs_i).getType(); + d_preinitialized_types[tr] = true; + ++eqcs_i; + } + + //must ensure model basis terms exists in model for each relevant type + fm->initialize(); + for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) { + Node op = it->first; + TypeNode tno = op.getType(); + for( unsigned i=0; i<tno.getNumChildren(); i++) { + preInitializeType( fm, tno[i] ); + } + } + //do not have to introduce terms for sorts of domains of quantified formulas if we are allowed to assume empty sorts + if( !options::fmfEmptySorts() ){ + for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){ + Node q = fm->getAssertedQuantifier( i ); + //make sure all types are set + for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ + preInitializeType( fm, q[0][i].getType() ); + } + } + } + } +} + void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ FirstOrderModelFmc * fm = ((FirstOrderModelFmc*)m)->asFirstOrderModelFmc(); if( !fullModel ){ Trace("fmc") << "---Full Model Check reset() " << std::endl; - fm->initialize(); d_quant_models.clear(); d_rep_ids.clear(); d_star_insts.clear(); @@ -338,50 +373,26 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ it != fm->d_rep_set.d_type_reps.end(); ++it ){ if( it->first.isSort() ){ Trace("fmc") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl; - Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(it->first); - Node rmbt = fm->getUsedRepresentative( mbt); - int mbt_index = -1; - Trace("fmc") << " Model basis term : " << mbt << std::endl; for( size_t a=0; a<it->second.size(); a++ ){ Node r = fm->getUsedRepresentative( it->second[a] ); - std::vector< Node > eqc; - ((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getEquivalenceClass( r, eqc ); - Trace("fmc-model-debug") << " " << (it->second[a]==r) << (r==mbt); - Trace("fmc-model-debug") << " : " << it->second[a] << " : " << r << " : "; - //Trace("fmc-model-debug") << r2 << " : " << ir << " : "; - Trace("fmc-model-debug") << " {"; - //find best selection for representative - for( size_t i=0; i<eqc.size(); i++ ){ - Trace("fmc-model-debug") << eqc[i] << ", "; - } - Trace("fmc-model-debug") << "}" << std::endl; - - //if this is the model basis eqc, replace with actual model basis term - if (r==rmbt || (mbt_index==-1 && a==(it->second.size()-1))) { - fm->d_model_basis_rep[it->first] = r; - r = mbt; - mbt_index = a; + if( Trace.isOn("fmc-model-debug") ){ + std::vector< Node > eqc; + ((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getEquivalenceClass( r, eqc ); + Trace("fmc-model-debug") << " " << (it->second[a]==r); + Trace("fmc-model-debug") << " : " << it->second[a] << " : " << r << " : "; + //Trace("fmc-model-debug") << r2 << " : " << ir << " : "; + Trace("fmc-model-debug") << " {"; + for( size_t i=0; i<eqc.size(); i++ ){ + Trace("fmc-model-debug") << eqc[i] << ", "; + } + Trace("fmc-model-debug") << "}" << std::endl; } d_rep_ids[it->first][r] = (int)a; } Trace("fmc-model-debug") << std::endl; - - if (mbt_index==-1) { - std::cout << " WARNING: model basis term is not a representative!" << std::endl; - exit(0); - }else{ - Trace("fmc") << "Star index for " << it->first << " is " << mbt_index << std::endl; - } - } - } - //also process non-rep set sorts - for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) { - Node op = it->first; - TypeNode tno = op.getType(); - for( unsigned i=0; i<tno.getNumChildren(); i++) { - initializeType( fm, tno[i] ); } } + //now, make models for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) { Node op = it->first; @@ -433,24 +444,26 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ entry_children.push_back(op); bool hasNonStar = false; for( unsigned i=0; i<c.getNumChildren(); i++) { - Node ri = fm->getUsedRepresentative( c[i]); - if( !ri.getType().isSort() && !ri.isConst() ){ - Trace("fmc-warn") << "Warning : model has non-constant argument in model " << ri << std::endl; - Assert( false ); - } + Node ri = fm->getUsedRepresentative( c[i] ); children.push_back(ri); + bool isStar = false; if( options::mbqiMode()!=quantifiers::MBQI_FMC_INTERVAL || !ri.getType().isInteger() ){ if (fm->isModelBasisTerm(ri) ) { ri = fm->getStar( ri.getType() ); + isStar = true; }else{ hasNonStar = true; } } + if( !isStar && !ri.isConst() ){ + Trace("fmc-warn") << "Warning : model has non-constant argument in model " << ri << " (from " << c[i] << ")" << std::endl; + Assert( false ); + } entry_children.push_back(ri); } Node n = NodeManager::currentNM()->mkNode( APPLY_UF, children ); Node nv = fm->getUsedRepresentative( v ); - if( !nv.getType().isSort() && !nv.isConst() ){ + if( !nv.isConst() ){ Trace("fmc-warn") << "Warning : model has non-constant value in model " << nv << std::endl; Assert( false ); } @@ -523,20 +536,15 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ } } -void FullModelChecker::initializeType( FirstOrderModelFmc * fm, TypeNode tn ){ - if( fm->d_model_basis_rep.find( tn )==fm->d_model_basis_rep.end() ){ - Trace("fmc") << "Initialize type " << tn << " hasType = " << fm->d_rep_set.hasType(tn) << std::endl; - Node mbn; - if (!fm->d_rep_set.hasType(tn)) { - mbn = fm->getSomeDomainElement(tn); - }else{ - mbn = d_qe->getTermDatabase()->getModelBasisTerm(tn); +void FullModelChecker::preInitializeType( FirstOrderModelFmc * fm, TypeNode tn ){ + if( d_preinitialized_types.find( tn )==d_preinitialized_types.end() ){ + d_preinitialized_types[tn] = true; + Node mb = d_qe->getTermDatabase()->getModelBasisTerm(tn); + if( !mb.isConst() ){ + Trace("fmc") << "...add model basis term to EE of model " << mb << " " << tn << std::endl; + fm->d_equalityEngine->addTerm( mb ); + fm->addTerm( mb ); } - Trace("fmc") << "Get used rep for " << mbn << std::endl; - Node mbnr = fm->getUsedRepresentative( mbn ); - Trace("fmc") << "...got " << mbnr << std::endl; - fm->d_model_basis_rep[tn] = mbnr; - Trace("fmc") << "Add model basis for type " << tn << " : " << mbn << " " << mbnr << std::endl; } } @@ -591,10 +599,6 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, Node op = NodeManager::currentNM()->mkSkolem( "qfmc", typ, "op created for full-model checking" ); d_quant_cond[f] = op; } - //make sure all types are set - for( unsigned i=0; i<f[0].getNumChildren(); i++ ){ - initializeType( fmfmc, f[0][i].getType() ); - } if( options::mbqiMode()==MBQI_NONE ){ //just exhaustive instantiate @@ -643,6 +647,7 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, Node ev = d_quant_models[f].evaluate(fmfmc, inst); if (ev==d_true) { addInst = false; + Trace("fmc-debug") << "...do not instantiate, evaluation was " << ev << std::endl; } }else{ //for debugging diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h index 29913d98d..c7bfcd189 100644 --- a/src/theory/quantifiers/full_model_check.h +++ b/src/theory/quantifiers/full_model_check.h @@ -92,8 +92,9 @@ protected: std::map<Node, Node > d_quant_cond; std::map< TypeNode, Node > d_array_cond; std::map< Node, Node > d_array_term_cond; - std::map<Node, std::vector< int > > d_star_insts; - void initializeType( FirstOrderModelFmc * fm, TypeNode tn ); + std::map< Node, std::vector< int > > d_star_insts; + std::map< TypeNode, bool > d_preinitialized_types; + void preInitializeType( FirstOrderModelFmc * fm, TypeNode tn ); Node normalizeArgReps(FirstOrderModelFmc * fm, Node op, Node n); bool exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, Node c, int c_index); protected: @@ -142,7 +143,8 @@ public: Node getFunctionValue(FirstOrderModelFmc * fm, Node op, const char* argPrefix ); - /** process build model */ + /** process build model */ + void preProcessBuildModel(TheoryModel* m, bool fullModel); void processBuildModel(TheoryModel* m, bool fullModel); /** get current model value */ Node getCurrentUfModelValue( FirstOrderModelFmc* fm, Node n, std::vector< Node > & args, bool partial ); diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 6dfd4c737..8bc9689bd 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -971,7 +971,7 @@ Node TermDb::mkSkolemizedBody( Node f, Node n, std::vector< TypeNode >& argTypes } ret = NodeManager::currentNM()->mkNode( OR, nret, n_str_ind ); } - Trace("quantifiers-sk") << "mkSkolem body for " << f << " returns : " << ret << std::endl; + Trace("quantifiers-sk-debug") << "mkSkolem body for " << f << " returns : " << ret << std::endl; //if it has an instantiation level, set the skolemized body to that level if( f.hasAttribute(InstLevelAttribute()) ){ theory::QuantifiersEngine::setInstantiationLevelAttr( ret, f.getAttribute(InstLevelAttribute()) ); @@ -1002,6 +1002,14 @@ Node TermDb::getSkolemizedBody( Node f ){ d_quantEngine->getTheoryEngine()->getSortInference()->setSkolemVar( f, f[0][i], d_skolem_constants[f][i] ); } } + if( Trace.isOn("quantifiers-sk") ){ + Trace("quantifiers-sk") << "Skolemize : "; + for( unsigned i=0; i<d_skolem_constants[f].size(); i++ ){ + Trace("quantifiers-sk") << d_skolem_constants[f][i] << " "; + } + Trace("quantifiers-sk") << "for " << std::endl; + Trace("quantifiers-sk") << " " << f << std::endl; + } } return d_skolem_body[ f ]; } diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index aee3ac4b8..19d66165a 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -602,9 +602,9 @@ void QuantifiersEngine::assertQuantifier( Node f, bool pol ){ NodeBuilder<> nb(kind::OR); nb << f << body.notNode(); Node lem = nb; - if( Trace.isOn("quantifiers-sk") ){ + if( Trace.isOn("quantifiers-sk-debug") ){ Node slem = Rewriter::rewrite( lem ); - Trace("quantifiers-sk") << "Skolemize lemma : " << slem << std::endl; + Trace("quantifiers-sk-debug") << "Skolemize lemma : " << slem << std::endl; } getOutputChannel().lemma( lem, false, true ); d_skolemized[f] = true; diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index a61df11d8..d024e0270 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -114,7 +114,8 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars, bool useDontCares) c return (*it).second; } Node ret = n; - if(n.getKind() == kind::EXISTS || n.getKind() == kind::FORALL || n.getKind() == kind::COMBINED_CARDINALITY_CONSTRAINT) { + if(n.getKind() == kind::EXISTS || n.getKind() == kind::FORALL || n.getKind() == kind::COMBINED_CARDINALITY_CONSTRAINT || + ( n.getKind() == kind::CARDINALITY_CONSTRAINT && options::ufssMode()!=theory::uf::UF_SS_FULL ) ) { // We should have terms, thanks to TheoryQuantifiers::collectModelInfo(). // However, if the Decision Engine stops us early, there might be a // quantifier that isn't assigned. In conjunction with miniscoping, this @@ -570,6 +571,10 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) Trace("model-builder") << "TheoryEngineModelBuilder: Collect model info..." << std::endl; d_te->collectModelInfo(tm, fullModel); + // model-builder specific initialization + preProcessBuildModel(tm, fullModel); + + // Loop through all terms and make sure that assignable sub-terms are in the equality engine // Also, record #eqc per type (for finite model finding) std::map< TypeNode, unsigned > eqc_usort_count; @@ -830,6 +835,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) if (t.getCardinality().isInfinite()) { bool success; do{ + Trace("model-builder-debug") << "Enumerate term of type " << t << std::endl; n = typeConstSet.nextTypeEnum(t, true); //--- AJR: this code checks whether n is a legal value Assert( !n.isNull() ); @@ -1016,6 +1022,9 @@ Node TheoryEngineModelBuilder::normalize(TheoryModel* m, TNode r, std::map< Node return retNode; } +void TheoryEngineModelBuilder::preProcessBuildModel(TheoryModel* m, bool fullModel) { + +} void TheoryEngineModelBuilder::processBuildModel(TheoryModel* m, bool fullModel) { diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index 4b27aeacb..b0952538a 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -255,6 +255,7 @@ protected: typedef std::hash_set<Node, NodeHashFunction> NodeSet; /** process build model */ + virtual void preProcessBuildModel(TheoryModel* m, bool fullModel); virtual void processBuildModel(TheoryModel* m, bool fullModel); /** normalize representative */ Node normalize(TheoryModel* m, TNode r, std::map<Node, Node>& constantReps, bool evalOnly); diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index e58c11aca..ffb537734 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -127,7 +127,7 @@ void TheoryUF::check(Effort level) { throw Exception( ss.str() ); } //needed for models - if( options::produceModels() && atom.getKind() == kind::COMBINED_CARDINALITY_CONSTRAINT ){ + if( options::produceModels() && ( atom.getKind() == kind::COMBINED_CARDINALITY_CONSTRAINT || options::ufssMode()!=UF_SS_FULL ) ){ d_equalityEngine.assertPredicate(atom, polarity, fact); } } else { diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am index 370096a1e..48b732f26 100644 --- a/test/regress/regress0/fmf/Makefile.am +++ b/test/regress/regress0/fmf/Makefile.am @@ -49,7 +49,8 @@ TESTS = \ jasmin-cdt-crash.smt2 \ loopy_coda.smt2 \ fmc_unsound_model.smt2 \ - am-bad-model.cvc + am-bad-model.cvc \ + nun-0208-to.cvc EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/fmf/nun-0208-to.smt2 b/test/regress/regress0/fmf/nun-0208-to.smt2 new file mode 100644 index 000000000..f831af1f2 --- /dev/null +++ b/test/regress/regress0/fmf/nun-0208-to.smt2 @@ -0,0 +1,180 @@ +; COMMAND-LINE: --finite-model-find +; EXPECT: sat + (set-logic ALL_SUPPORTED) + (declare-sort b__ 0) + (declare-fun __nun_card_witness_0_ () b__) + (declare-sort a__ 0) + (declare-fun __nun_card_witness_1_ () a__) + (declare-datatypes () + ((prod__ (Pair__ (_select_Pair___0 a__) (_select_Pair___1 b__))))) + (declare-datatypes () + ((list2__ + (Cons2__ (_select_Cons2___0 prod__) (_select_Cons2___1 list2__)) + (Nil2__ )))) + (declare-datatypes () + ((list__ (Cons__ (_select_Cons___0 a__) (_select_Cons___1 list__)) + (Nil__ )))) + (declare-datatypes () + ((list1__ (Cons1__ (_select_Cons1___0 b__) (_select_Cons1___1 list1__)) + (Nil1__ )))) + (declare-sort G_zip__ 0) + (declare-fun __nun_card_witness_2_ () G_zip__) + (declare-fun zip__ (list__ list1__) list2__) + (declare-fun proj_G_zip__0_ (G_zip__) list__) + (declare-fun proj_G_zip__1_ (G_zip__) list1__) + (assert + (forall ((a/166 G_zip__)) + (and + (= (zip__ (proj_G_zip__0_ a/166) (proj_G_zip__1_ a/166)) + (ite (is-Cons1__ (proj_G_zip__1_ a/166)) + (ite (is-Cons__ (proj_G_zip__0_ a/166)) + (Cons2__ + (Pair__ (_select_Cons___0 (proj_G_zip__0_ a/166)) + (_select_Cons1___0 (proj_G_zip__1_ a/166))) + (zip__ (_select_Cons___1 (proj_G_zip__0_ a/166)) + (_select_Cons1___1 (proj_G_zip__1_ a/166)))) + Nil2__) + Nil2__)) + (=> (is-Cons1__ (proj_G_zip__1_ a/166)) + (=> (is-Cons__ (proj_G_zip__0_ a/166)) + (exists ((a/168 G_zip__)) + (and + (= (_select_Cons1___1 (proj_G_zip__1_ a/166)) + (proj_G_zip__1_ a/168)) + (= (_select_Cons___1 (proj_G_zip__0_ a/166)) + (proj_G_zip__0_ a/168))))))))) + (declare-datatypes () ((nat__ (Suc__ (_select_Suc___0 nat__)) (zero__ )))) + (declare-sort G_replicate__ 0) + (declare-fun __nun_card_witness_3_ () G_replicate__) + (declare-fun replicate__ (nat__ a__) list__) + (declare-fun proj_G_replicate__0_ (G_replicate__) nat__) + (declare-fun proj_G_replicate__1_ (G_replicate__) a__) + (assert + (forall ((a/169 G_replicate__)) + (and + (= + (replicate__ (proj_G_replicate__0_ a/169) + (proj_G_replicate__1_ a/169)) + (ite (is-Suc__ (proj_G_replicate__0_ a/169)) + (Cons__ (proj_G_replicate__1_ a/169) + (replicate__ (_select_Suc___0 (proj_G_replicate__0_ a/169)) + (proj_G_replicate__1_ a/169))) + Nil__)) + (=> (is-Suc__ (proj_G_replicate__0_ a/169)) + (exists ((a/171 G_replicate__)) + (and + (= (proj_G_replicate__1_ a/169) (proj_G_replicate__1_ a/171)) + (= (_select_Suc___0 (proj_G_replicate__0_ a/169)) + (proj_G_replicate__0_ a/171)))))))) + (declare-fun j__ () nat__) + (declare-fun x__ () a__) + (declare-sort G_replicate1__ 0) + (declare-fun __nun_card_witness_4_ () G_replicate1__) + (declare-fun replicate1__ (nat__ b__) list1__) + (declare-fun proj_G_replicate1__0_ (G_replicate1__) nat__) + (declare-fun proj_G_replicate1__1_ (G_replicate1__) b__) + (assert + (forall ((a/172 G_replicate1__)) + (and + (= + (replicate1__ (proj_G_replicate1__0_ a/172) + (proj_G_replicate1__1_ a/172)) + (ite (is-Suc__ (proj_G_replicate1__0_ a/172)) + (Cons1__ (proj_G_replicate1__1_ a/172) + (replicate1__ (_select_Suc___0 (proj_G_replicate1__0_ a/172)) + (proj_G_replicate1__1_ a/172))) + Nil1__)) + (=> (is-Suc__ (proj_G_replicate1__0_ a/172)) + (exists ((a/174 G_replicate1__)) + (and + (= (proj_G_replicate1__1_ a/172) (proj_G_replicate1__1_ a/174)) + (= (_select_Suc___0 (proj_G_replicate1__0_ a/172)) + (proj_G_replicate1__0_ a/174)))))))) + (declare-fun y__ () b__) + (declare-sort G_replicate2__ 0) + (declare-fun __nun_card_witness_5_ () G_replicate2__) + (declare-fun replicate2__ (nat__ prod__) list2__) + (declare-fun proj_G_replicate2__0_ (G_replicate2__) nat__) + (declare-fun proj_G_replicate2__1_ (G_replicate2__) prod__) + (assert + (forall ((a/175 G_replicate2__)) + (and + (= + (replicate2__ (proj_G_replicate2__0_ a/175) + (proj_G_replicate2__1_ a/175)) + (ite (is-Suc__ (proj_G_replicate2__0_ a/175)) + (Cons2__ (proj_G_replicate2__1_ a/175) + (replicate2__ (_select_Suc___0 (proj_G_replicate2__0_ a/175)) + (proj_G_replicate2__1_ a/175))) + Nil2__)) + (=> (is-Suc__ (proj_G_replicate2__0_ a/175)) + (exists ((a/177 G_replicate2__)) + (and + (= (proj_G_replicate2__1_ a/175) (proj_G_replicate2__1_ a/177)) + (= (_select_Suc___0 (proj_G_replicate2__0_ a/175)) + (proj_G_replicate2__0_ a/177)))))))) + (declare-sort G_less__eq__ 0) + (declare-fun __nun_card_witness_6_ () G_less__eq__) + (declare-fun less__eq__ (nat__ nat__) Bool) + (declare-fun proj_G_less__eq__0_ (G_less__eq__) nat__) + (declare-fun proj_G_less__eq__1_ (G_less__eq__) nat__) + (assert + (forall ((a/178 G_less__eq__)) + (and + (= + (less__eq__ (proj_G_less__eq__0_ a/178) (proj_G_less__eq__1_ a/178)) + (=> (is-Suc__ (proj_G_less__eq__0_ a/178)) + (and (is-Suc__ (proj_G_less__eq__1_ a/178)) + (less__eq__ (_select_Suc___0 (proj_G_less__eq__0_ a/178)) + (_select_Suc___0 (proj_G_less__eq__1_ a/178)))))) + (exists ((a/182 G_less__eq__)) + (and + (= (_select_Suc___0 (proj_G_less__eq__1_ a/178)) + (proj_G_less__eq__1_ a/182)) + (= (_select_Suc___0 (proj_G_less__eq__0_ a/178)) + (proj_G_less__eq__0_ a/182))))))) + (declare-sort G_min__ 0) + (declare-fun __nun_card_witness_7_ () G_min__) + (declare-fun min__ (nat__ nat__) nat__) + (declare-fun proj_G_min__0_ (G_min__) nat__) + (declare-fun proj_G_min__1_ (G_min__) nat__) + (assert + (forall ((a/183 G_min__)) + (and + (= (min__ (proj_G_min__0_ a/183) (proj_G_min__1_ a/183)) + (ite (less__eq__ (proj_G_min__0_ a/183) (proj_G_min__1_ a/183)) + (proj_G_min__0_ a/183) (proj_G_min__1_ a/183))) + (exists ((a/184 G_less__eq__)) + (and (= (proj_G_min__1_ a/183) (proj_G_less__eq__1_ a/184)) + (= (proj_G_min__0_ a/183) (proj_G_less__eq__0_ a/184))))))) + (declare-fun i__ () nat__) + (assert + (not + (=> + (and + (exists ((a/212 G_min__)) + (and (= i__ (proj_G_min__1_ a/212)) (= i__ (proj_G_min__0_ a/212)))) + (exists ((a/208 G_replicate2__)) + (and (= (Pair__ x__ y__) (proj_G_replicate2__1_ a/208)) + (= (min__ i__ i__) (proj_G_replicate2__0_ a/208)) + (exists ((a/210 G_min__)) + (and (= i__ (proj_G_min__1_ a/210)) + (= i__ (proj_G_min__0_ a/210)))))) + (exists ((a/199 G_zip__)) + (and (= (replicate1__ j__ y__) (proj_G_zip__1_ a/199)) + (exists ((a/202 G_replicate1__)) + (and (= y__ (proj_G_replicate1__1_ a/202)) + (= j__ (proj_G_replicate1__0_ a/202)))) + (= (replicate__ j__ x__) (proj_G_zip__0_ a/199)) + (exists ((a/203 G_replicate__)) + (and (= x__ (proj_G_replicate__1_ a/203)) + (= j__ (proj_G_replicate__0_ a/203)))))) + (exists ((a/207 G_replicate1__)) + (and (= y__ (proj_G_replicate1__1_ a/207)) + (= j__ (proj_G_replicate1__0_ a/207)))) + (exists ((a/206 G_replicate__)) + (and (= x__ (proj_G_replicate__1_ a/206)) + (= j__ (proj_G_replicate__0_ a/206))))) + (= (replicate2__ (min__ i__ i__) (Pair__ x__ y__)) + (zip__ (replicate__ j__ x__) (replicate1__ j__ y__)))))) + (check-sat) diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index 7178710cb..3fff9b0de 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -41,7 +41,7 @@ TESTS = \ symmetric_unsat_7.smt2 \ javafe.ast.StmtVec.009.smt2 \ ARI176e1.smt2 \ - bi-artm-s.smt2 \ + bi-artm-s.smt2 \ simp-typ-test.smt2 \ macros-int-real.smt2 \ stream-x2014-09-18-unsat.smt2 \ @@ -64,7 +64,8 @@ TESTS = \ ari056.smt2 \ ext-ex-deq-trigger.smt2 \ matching-lia-1arg.smt2 \ - RND_4_16.smt2 + RND_4_16.smt2 \ + cdt-0208-to.smt2 # regression can be solved with --finite-model-find --fmf-inst-engine diff --git a/test/regress/regress0/quantifiers/cdt-0208-to.smt2 b/test/regress/regress0/quantifiers/cdt-0208-to.smt2 new file mode 100644 index 000000000..a458cea64 --- /dev/null +++ b/test/regress/regress0/quantifiers/cdt-0208-to.smt2 @@ -0,0 +1,767 @@ +; COMMAND-LINE: --full-saturate-quant +; EXPECT: unsat +(set-logic ALL_SUPPORTED) +(set-info :status unsat) +(declare-sort A$ 0) +(declare-sort A_set$ 0) +(declare-sort A_a_fun$ 0) +(declare-sort A_bool_fun$ 0) +(declare-sort Bool_a_fun$ 0) +(declare-sort A_a_llist_fun$ 0) +(declare-sort A_llist_a_fun$ 0) +(declare-sort Bool_bool_fun$ 0) +(declare-sort A_a_bool_fun_fun$ 0) +(declare-sort A_llist_bool_fun$ 0) +(declare-sort Bool_a_llist_fun$ 0) +(declare-sort A_llist_a_set_fun$ 0) +(declare-sort A_a_llist_a_fun_fun$ 0) +(declare-sort A_llist_a_llist_fun$ 0) +(declare-sort A_a_llist_bool_fun_fun$ 0) +(declare-sort A_llist_a_llist_prod_set$ 0) +(declare-sort A_a_llist_a_llist_fun_fun$ 0) +(declare-sort A_llist_a_llist_bool_fun_fun$ 0) +(declare-sort A_llist_a_llist_a_set_fun_fun$ 0) +(declare-sort A_llist_a_llist_prod_bool_fun$ 0) +(declare-sort Bool_a_llist_a_llist_prod_fun$ 0) +(declare-sort A_llist_a_llist_prod_a_set_fun$ 0) +(declare-sort A_llist_a_llist_a_llist_prod_fun$ 0) +(declare-sort A_llist_a_llist_prod_a_llist_fun$ 0) +(declare-sort A_llist_a_llist_prod_set_bool_fun$ 0) +(declare-sort Bool_a_llist_a_llist_prod_set_fun$ 0) +(declare-sort A_llist_a_llist_prod_llist_bool_fun$ 0) +(declare-sort A_llist_a_llist_a_llist_prod_set_fun$ 0) +(declare-sort A_a_llist_a_fun_fun_a_llist_a_fun_fun$ 0) +(declare-sort A_llist_a_llist_prod_bool_fun_bool_fun$ 0) +(declare-sort Bool_a_llist_a_llist_prod_bool_fun_fun$ 0) +(declare-sort A_llist_a_llist_a_llist_bool_fun_fun_fun$ 0) +(declare-sort A_llist_a_llist_a_llist_prod_bool_fun_fun$ 0) +(declare-sort A_a_llist_a_fun_fun_a_a_llist_a_fun_fun_fun$ 0) +(declare-sort A_a_llist_bool_fun_fun_a_llist_bool_fun_fun$ 0) +(declare-sort A_llist_a_llist_fun_a_llist_a_llist_fun_fun$ 0) +(declare-sort A_llist_a_llist_a_llist_a_llist_prod_fun_fun$ 0) +(declare-sort A_llist_a_llist_prod_a_llist_a_llist_prod_fun$ 0) +(declare-sort A_a_llist_a_fun_fun_a_a_llist_bool_fun_fun_fun$ 0) +(declare-sort A_a_llist_bool_fun_fun_a_a_llist_a_fun_fun_fun$ 0) +(declare-sort A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$ 0) +(declare-sort A_a_llist_a_fun_fun_a_a_llist_a_llist_fun_fun_fun$ 0) +(declare-sort A_a_llist_a_llist_fun_fun_a_a_llist_a_fun_fun_fun$ 0) +(declare-sort A_a_llist_a_llist_fun_fun_a_llist_a_llist_fun_fun$ 0) +(declare-sort A_a_llist_bool_fun_fun_a_a_llist_bool_fun_fun_fun$ 0) +(declare-sort A_llist_a_llist_prod_a_llist_a_llist_prod_set_fun$ 0) +(declare-sort A_llist_a_llist_prod_set_a_llist_a_llist_prod_fun$ 0) +(declare-sort A_llist_a_llist_prod_a_llist_a_llist_prod_prod_set$ 0) +(declare-sort A_llist_a_llist_prod_llist_a_llist_a_llist_prod_fun$ 0) +(declare-sort A_a_llist_a_llist_fun_fun_a_a_llist_bool_fun_fun_fun$ 0) +(declare-sort A_a_llist_bool_fun_fun_a_a_llist_a_llist_fun_fun_fun$ 0) +(declare-sort A_llist_a_llist_a_llist_a_llist_bool_fun_fun_fun_fun$ 0) +(declare-sort A_llist_a_llist_fun_a_llist_a_llist_bool_fun_fun_fun$ 0) +(declare-sort A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$ 0) +(declare-sort A_llist_a_llist_prod_a_llist_a_llist_bool_fun_fun_fun$ 0) +(declare-sort A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$ 0) +(declare-sort A_a_llist_a_llist_fun_fun_a_a_llist_a_llist_fun_fun_fun$ 0) +(declare-sort A_llist_a_llist_prod_a_llist_a_llist_prod_a_set_fun_fun$ 0) +(declare-sort A_llist_a_llist_prod_a_llist_a_llist_prod_prod_bool_fun$ 0) +(declare-sort A_llist_a_llist_prod_llist_a_llist_a_llist_prod_llist_fun$ 0) +(declare-sort A_llist_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_fun$ 0) +(declare-sort A_llist_a_llist_prod_set_a_llist_a_llist_prod_bool_fun_fun$ 0) +(declare-sort A_llist_a_llist_prod_a_llist_a_llist_prod_llist_bool_fun_fun$ 0) +(declare-sort A_llist_a_fun_a_llist_a_llist_fun_a_llist_a_llist_fun_fun_fun$ 0) +(declare-sort A_llist_a_llist_bool_fun_fun_a_llist_a_llist_bool_fun_fun_fun$ 0) +(declare-sort A_llist_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_set_fun$ 0) +(declare-sort A_llist_a_llist_bool_fun_fun_a_llist_a_llist_prod_bool_fun_fun$ 0) +(declare-sort A_llist_a_llist_prod_llist_a_llist_a_llist_prod_llist_prod_set$ 0) +(declare-sort A_llist_a_llist_prod_bool_fun_a_llist_a_llist_prod_bool_fun_fun$ 0) +(declare-sort A_llist_a_llist_prod_llist_a_llist_a_llist_prod_llist_bool_fun_fun$ 0) +(declare-sort A_llist_a_llist_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_fun_fun$ 0) +(declare-sort A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_fun_fun$ 0) +(declare-sort A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_fun$ 0) +(declare-sort A_llist_a_llist_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_set_fun_fun$ 0) +(declare-sort A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_set_fun_fun$ 0) +(declare-sort A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_set_fun$ 0) +(declare-sort A_llist_a_llist_prod_a_llist_a_llist_prod_llist_a_llist_a_llist_prod_fun_fun$ 0) +(declare-sort A_llist_a_llist_a_llist_a_llist_prod_fun_fun_a_llist_a_llist_bool_fun_fun_fun$ 0) +(declare-sort A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun_a_llist_a_llist_bool_fun_fun_fun$ 0) +(declare-sort A_llist_a_llist_bool_fun_fun_a_llist_a_llist_a_llist_a_llist_prod_set_fun_fun_fun$ 0) +(declare-sort A_llist_a_llist_prod_set_a_llist_a_llist_a_llist_a_llist_bool_fun_fun_fun_fun_fun$ 0) +(declare-sort A_llist_a_llist_prod_a_llist_a_llist_prod_llist_a_llist_a_llist_prod_llist_fun_fun$ 0) +(declare-sort A_llist_a_llist_prod_set_a_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun_fun$ 0) +(declare-sort A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun_a_llist_a_llist_bool_fun_fun_fun$ 0) +(declare-sort A_llist_a_llist_bool_fun_fun_a_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun_fun$ 0) +(declare-sort A_llist_a_llist_a_llist_prod_set_fun_a_llist_a_llist_a_llist_a_llist_bool_fun_fun_fun_fun_fun$ 0) +(declare-sort A_llist_a_llist_a_llist_a_llist_prod_fun_fun_a_llist_a_llist_prod_a_llist_a_llist_prod_fun_fun$ 0) +(declare-sort A_llist_a_llist_a_llist_prod_set_fun_a_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun_fun$ 0) +(declare-sort A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_fun_fun$ 0) +(declare-sort A_llist_a_llist_a_llist_a_llist_prod_fun_fun_a_llist_a_llist_a_llist_a_llist_prod_set_fun_fun_fun$ 0) +(declare-sort A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_set_fun_fun$ 0) +(declare-sort A_llist_a_llist_prod_a_llist_a_llist_prod_llist_bool_fun_fun_a_llist_a_llist_prod_llist_bool_fun_fun$ 0) +(declare-sort A_llist_a_llist_a_llist_a_llist_prod_fun_fun_a_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun_fun$ 0) +(declare-sort A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun_a_llist_a_llist_prod_a_llist_a_llist_prod_set_fun_fun$ 0) +(declare-sort A_llist_a_llist_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_fun_fun_a_llist_a_llist_bool_fun_fun_fun$ 0) +(declare-sort A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun_a_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun_fun$ 0) +(declare-sort A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun_a_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun_fun$ 0) +(declare-sort A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_bool_fun_fun$ 0) +(declare-sort A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_fun_fun_a_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun_fun$ 0) +(declare-sort A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_fun_fun_a_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun_fun$ 0) +(declare-codatatypes () ((A_llist$ (lNil$) (lCons$ (lhd$ A$) (ltl$ A_llist$))))) +(declare-datatypes () ((A_llist_a_llist_prod$ (pair$ (fst$ A_llist$) (snd$ A_llist$))))) +(declare-codatatypes () ((A_llist_a_llist_prod_llist$ (lNil$a) (lCons$a (lhd$a A_llist_a_llist_prod$) (ltl$a A_llist_a_llist_prod_llist$))))) +(declare-datatypes () ((A_llist_a_llist_prod_llist_a_llist_a_llist_prod_llist_prod$ (pair$a (fst$a A_llist_a_llist_prod_llist$) (snd$a A_llist_a_llist_prod_llist$))) + (A_llist_a_llist_prod_a_llist_a_llist_prod_prod$ (pair$b (fst$b A_llist_a_llist_prod$) (snd$b A_llist_a_llist_prod$))))) +(declare-fun p$ () A_llist_a_llist_bool_fun_fun$) +(declare-fun uu$ (Bool) A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun_a_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun_fun$) +(declare-fun xs$ () A_llist$) +(declare-fun ys$ () A_llist$) +(declare-fun sup$ (A_llist_a_llist_prod_set$ A_llist_a_llist_prod_set$) A_llist_a_llist_prod_set$) +(declare-fun the$ (A_llist_a_llist_prod_bool_fun$) A_llist_a_llist_prod$) +(declare-fun uua$ (Bool) A_llist_a_llist_bool_fun_fun_a_llist_a_llist_bool_fun_fun_fun$) +(declare-fun uub$ (A_llist_a_llist_prod_a_llist_a_llist_prod_set_fun$) A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$) +(declare-fun uuc$ (A_llist_a_llist_prod_a_llist_a_llist_prod_fun$) A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) +(declare-fun uud$ (A_llist_a_llist_prod_a_llist_a_llist_prod_prod_bool_fun$) A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) +(declare-fun uue$ (A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$) +(declare-fun uuf$ (A_llist_a_llist_prod_bool_fun$) A_llist_a_llist_bool_fun_fun$) +(declare-fun uug$ (A_set$) A_bool_fun$) +(declare-fun uuh$ (A_llist_a_llist_prod_a_llist_a_llist_prod_prod_set$) A_llist_a_llist_prod_a_llist_a_llist_prod_prod_bool_fun$) +(declare-fun uui$ (A_llist_a_llist_prod_set$) A_llist_a_llist_prod_bool_fun$) +(declare-fun uuj$ (Bool_bool_fun$) A_llist_a_llist_bool_fun_fun_a_llist_a_llist_bool_fun_fun_fun$) +(declare-fun uuk$ (Bool_a_llist_a_llist_prod_fun$ A_llist_a_llist_bool_fun_fun$) A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) +(declare-fun uul$ (A_llist_a_llist_prod_bool_fun$) A_llist_a_llist_a_llist_a_llist_prod_fun_fun_a_llist_a_llist_bool_fun_fun_fun$) +(declare-fun uum$ (Bool_a_llist_a_llist_prod_set_fun$) A_llist_a_llist_bool_fun_fun_a_llist_a_llist_a_llist_a_llist_prod_set_fun_fun_fun$) +(declare-fun uun$ (A_llist_a_llist_prod_set_bool_fun$) A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun_a_llist_a_llist_bool_fun_fun_fun$) +(declare-fun uuo$ (Bool_a_llist_a_llist_prod_bool_fun_fun$) A_llist_a_llist_bool_fun_fun_a_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun_fun$) +(declare-fun uup$ (Bool_bool_fun$) A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun_a_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun_fun$) +(declare-fun uuq$ (A_llist_a_llist_prod_bool_fun_bool_fun$) A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun_a_llist_a_llist_bool_fun_fun_fun$) +(declare-fun uur$ (A_llist_a_llist_prod_a_llist_a_llist_prod_fun$ A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) +(declare-fun uus$ (A_llist_a_llist_prod_set_a_llist_a_llist_prod_fun$ A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$) A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) +(declare-fun uut$ (A_llist_a_llist_bool_fun_fun$) A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_fun_fun_a_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun_fun$) +(declare-fun uuu$ (A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$) A_llist_a_llist_a_llist_a_llist_prod_fun_fun_a_llist_a_llist_a_llist_a_llist_prod_set_fun_fun_fun$) +(declare-fun uuv$ (A_llist_a_llist_a_llist_a_llist_prod_fun_fun$ A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) +(declare-fun uuw$ (A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) A_llist_a_llist_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_fun_fun_a_llist_a_llist_bool_fun_fun_fun$) +(declare-fun uux$ (A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_fun_fun_a_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun_fun$) +(declare-fun uuy$ (A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$) A_llist_a_llist_a_llist_a_llist_prod_fun_fun_a_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun_fun$) +(declare-fun uuz$ (A_llist_a_llist_bool_fun_fun$) A_llist_a_llist_a_llist_a_llist_prod_fun_fun_a_llist_a_llist_bool_fun_fun_fun$) +(declare-fun uva$ () A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) +(declare-fun uvb$ () A_llist_a_llist_bool_fun_fun$) +(declare-fun uvc$ () A_llist_a_llist_prod_llist_a_llist_a_llist_prod_fun$) +(declare-fun uvd$ () A_llist_a_llist_prod_llist_a_llist_a_llist_prod_llist_fun$) +(declare-fun uve$ () A_llist_a_fun$) +(declare-fun uvf$ () A_llist_a_llist_fun$) +(declare-fun uvg$ (A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$) A_llist_a_llist_prod_a_llist_a_llist_bool_fun_fun_fun$) +(declare-fun uvh$ (Bool_bool_fun$) A_a_llist_bool_fun_fun_a_a_llist_bool_fun_fun_fun$) +(declare-fun uvi$ (Bool_a_llist_fun$) A_a_llist_bool_fun_fun_a_a_llist_a_llist_fun_fun_fun$) +(declare-fun uvj$ (Bool_a_fun$) A_a_llist_bool_fun_fun_a_a_llist_a_fun_fun_fun$) +(declare-fun uvk$ (A_llist_bool_fun$) A_a_llist_a_llist_fun_fun_a_a_llist_bool_fun_fun_fun$) +(declare-fun uvl$ (A_llist_a_llist_fun$) A_a_llist_a_llist_fun_fun_a_a_llist_a_llist_fun_fun_fun$) +(declare-fun uvm$ (A_llist_a_fun$) A_a_llist_a_llist_fun_fun_a_a_llist_a_fun_fun_fun$) +(declare-fun uvn$ (A_bool_fun$) A_a_llist_a_fun_fun_a_a_llist_bool_fun_fun_fun$) +(declare-fun uvo$ (A_a_llist_fun$) A_a_llist_a_fun_fun_a_a_llist_a_llist_fun_fun_fun$) +(declare-fun uvp$ (A_a_fun$) A_a_llist_a_fun_fun_a_a_llist_a_fun_fun_fun$) +(declare-fun uvq$ () A_llist_a_llist_prod_a_llist_a_llist_prod_llist_bool_fun_fun$) +(declare-fun uvr$ () A_a_llist_bool_fun_fun$) +(declare-fun uvs$ () A_llist_a_llist_prod_a_llist_a_llist_prod_llist_bool_fun_fun$) +(declare-fun uvt$ () A_a_llist_bool_fun_fun$) +(declare-fun uvu$ () A_llist_a_llist_prod_a_llist_a_llist_prod_llist_a_llist_a_llist_prod_llist_fun_fun$) +(declare-fun uvv$ () A_a_llist_a_llist_fun_fun$) +(declare-fun uvw$ () A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_fun_fun$) +(declare-fun uvx$ () A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) +(declare-fun uvy$ (A_llist_a_llist_prod_a_llist_a_llist_prod_prod_set$) A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) +(declare-fun uvz$ (A_llist_a_llist_prod_set$) A_llist_a_llist_bool_fun_fun$) +(declare-fun uwa$ () A_llist_a_llist_prod_a_llist_a_llist_prod_llist_a_llist_a_llist_prod_fun_fun$) +(declare-fun uwb$ () A_a_llist_a_fun_fun$) +(declare-fun uwc$ (A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$) A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$) +(declare-fun uwd$ (A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) +(declare-fun uwe$ (A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) +(declare-fun uwf$ (A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$) A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$) +(declare-fun uwg$ (A_llist_a_llist_bool_fun_fun$) A_llist_a_llist_bool_fun_fun$) +(declare-fun uwh$ (A_llist_a_llist_prod_llist$) A_llist_a_llist_prod_a_llist_a_llist_prod_llist_a_llist_a_llist_prod_llist_fun_fun$) +(declare-fun uwi$ (A_llist$) A_a_llist_a_llist_fun_fun$) +(declare-fun uwj$ (A_llist$) A_a_llist_a_llist_fun_fun$) +(declare-fun uwk$ (A_llist_a_llist_prod_set$) A_llist_a_llist_fun_a_llist_a_llist_bool_fun_fun_fun$) +(declare-fun uwl$ (A_llist_bool_fun$) A_llist_a_llist_a_llist_prod_set_fun_a_llist_a_llist_a_llist_a_llist_bool_fun_fun_fun_fun_fun$) +(declare-fun uwm$ (A_llist_bool_fun$) A_llist_a_llist_a_llist_prod_set_fun_a_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun_fun$) +(declare-fun uwn$ (A_llist_a_llist_prod_set$) A_llist_a_llist_prod_set_a_llist_a_llist_a_llist_a_llist_bool_fun_fun_fun_fun_fun$) +(declare-fun uwo$ (A_llist_a_llist_prod_set$) A_llist_a_llist_prod_set_a_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun_fun$) +(declare-fun uwp$ (A_llist_a_llist_prod_bool_fun$) A_llist_a_llist_prod_bool_fun_a_llist_a_llist_prod_bool_fun_fun$) +(declare-fun uwq$ (A_llist_a_llist_prod_set$) A_llist_a_llist_prod_set_a_llist_a_llist_prod_bool_fun_fun$) +(declare-fun uwr$ (A_llist_a_llist_prod_bool_fun$) A_llist_a_llist_prod_bool_fun_a_llist_a_llist_prod_bool_fun_fun$) +(declare-fun uws$ (A_llist_a_llist_prod_set$) A_llist_a_llist_prod_bool_fun_a_llist_a_llist_prod_bool_fun_fun$) +(declare-fun uwt$ (A_llist$) A_llist_a_llist_a_llist_bool_fun_fun_fun$) +(declare-fun lset$ (A_llist_a_llist_prod_llist$) A_llist_a_llist_prod_set$) +(declare-fun swap$ (A_llist_a_llist_prod$) A_llist_a_llist_prod$) +(declare-fun lnull$ () A_llist_bool_fun$) +(declare-fun lset$a (A_llist$) A_set$) +(declare-fun swap$a (A_llist_a_llist_prod_a_llist_a_llist_prod_prod$) A_llist_a_llist_prod_a_llist_a_llist_prod_prod$) +(declare-fun image2$ (A_llist_a_llist_prod_set$ A_llist_a_llist_prod_a_llist_fun$ A_llist_a_llist_prod_a_llist_fun$) A_llist_a_llist_prod_set$) +(declare-fun in_rel$ (A_llist_a_llist_prod_set$) A_llist_a_llist_bool_fun_fun$) +(declare-fun lnull$a () A_llist_a_llist_prod_llist_bool_fun$) +(declare-fun member$ (A_llist_a_llist_prod$) A_llist_a_llist_prod_set_bool_fun$) +(declare-fun collect$ (A_llist_a_llist_prod_bool_fun$) A_llist_a_llist_prod_set$) +(declare-fun fun_app$ (A_llist_a_llist_prod_llist_a_llist_a_llist_prod_llist_fun$ A_llist_a_llist_prod_llist$) A_llist_a_llist_prod_llist$) +(declare-fun lappend$ (A_llist_a_llist_prod_llist$) A_llist_a_llist_prod_llist_a_llist_a_llist_prod_llist_fun$) +(declare-fun less_eq$ (A_llist_a_llist_prod_set$) A_llist_a_llist_prod_set_bool_fun$) +(declare-fun lfinite$ (A_llist_a_llist_prod_llist$) Bool) +(declare-fun lmember$ (A_llist_a_llist_prod$) A_llist_a_llist_prod_llist_bool_fun$) +(declare-fun lprefix$ (A_llist$) A_llist_bool_fun$) +(declare-fun member$a (A_llist_a_llist_prod_a_llist_a_llist_prod_prod$ A_llist_a_llist_prod_a_llist_a_llist_prod_prod_set$) Bool) +(declare-fun member$b (A$ A_set$) Bool) +(declare-fun member$c (A_llist_a_llist_prod_llist_a_llist_a_llist_prod_llist_prod$ A_llist_a_llist_prod_llist_a_llist_a_llist_prod_llist_prod_set$) Bool) +(declare-fun uncurry$ () A_llist_a_llist_a_llist_a_llist_prod_fun_fun_a_llist_a_llist_prod_a_llist_a_llist_prod_fun_fun$) +(declare-fun collect$a (A_llist_a_llist_prod_a_llist_a_llist_prod_prod_bool_fun$) A_llist_a_llist_prod_a_llist_a_llist_prod_prod_set$) +(declare-fun collect$b (A_bool_fun$) A_set$) +(declare-fun fun_app$a (A_llist_a_llist_fun$ A_llist$) A_llist$) +(declare-fun fun_app$b (A_llist_a_llist_prod_llist_a_llist_a_llist_prod_fun$ A_llist_a_llist_prod_llist$) A_llist_a_llist_prod$) +(declare-fun fun_app$c (A_llist_a_fun$ A_llist$) A$) +(declare-fun fun_app$d (A_llist_a_llist_a_llist_prod_fun$ A_llist$) A_llist_a_llist_prod$) +(declare-fun fun_app$e (A_llist_a_llist_a_llist_a_llist_prod_fun_fun$ A_llist$) A_llist_a_llist_a_llist_prod_fun$) +(declare-fun fun_app$f (A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_fun$ A_llist_a_llist_prod$) A_llist_a_llist_prod_a_llist_a_llist_prod_prod$) +(declare-fun fun_app$g (A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_fun_fun$ A_llist_a_llist_prod$) A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_fun$) +(declare-fun fun_app$h (A_llist_a_llist_prod_bool_fun$ A_llist_a_llist_prod$) Bool) +(declare-fun fun_app$i (A_llist_a_llist_prod_set_bool_fun$ A_llist_a_llist_prod_set$) Bool) +(declare-fun fun_app$j (A_llist_a_llist_prod_a_llist_a_llist_prod_prod_bool_fun$ A_llist_a_llist_prod_a_llist_a_llist_prod_prod$) Bool) +(declare-fun fun_app$k (A_bool_fun$ A$) Bool) +(declare-fun fun_app$l (A_llist_bool_fun$ A_llist$) Bool) +(declare-fun fun_app$m (A_llist_a_llist_bool_fun_fun$ A_llist$) A_llist_bool_fun$) +(declare-fun fun_app$n (A_llist_a_llist_a_llist_prod_set_fun$ A_llist$) A_llist_a_llist_prod_set$) +(declare-fun fun_app$o (A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$ A_llist$) A_llist_a_llist_a_llist_prod_set_fun$) +(declare-fun fun_app$p (A_llist_a_llist_a_llist_prod_bool_fun_fun$ A_llist$) A_llist_a_llist_prod_bool_fun$) +(declare-fun fun_app$q (A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$ A_llist$) A_llist_a_llist_a_llist_prod_bool_fun_fun$) +(declare-fun fun_app$r (A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$ A_llist_a_llist_prod$) A_llist_a_llist_prod_bool_fun$) +(declare-fun fun_app$s (A_llist_a_llist_prod_set_a_llist_a_llist_prod_bool_fun_fun$ A_llist_a_llist_prod_set$) A_llist_a_llist_prod_bool_fun$) +(declare-fun fun_app$t (A_llist_a_llist_prod_bool_fun_a_llist_a_llist_prod_bool_fun_fun$ A_llist_a_llist_prod_bool_fun$) A_llist_a_llist_prod_bool_fun$) +(declare-fun fun_app$u (A_llist_a_llist_prod_a_llist_a_llist_prod_llist_a_llist_a_llist_prod_llist_fun_fun$ A_llist_a_llist_prod$) A_llist_a_llist_prod_llist_a_llist_a_llist_prod_llist_fun$) +(declare-fun fun_app$v (A_a_llist_a_llist_fun_fun$ A$) A_llist_a_llist_fun$) +(declare-fun fun_app$w (A_llist_a_llist_prod_a_llist_a_llist_prod_fun$ A_llist_a_llist_prod$) A_llist_a_llist_prod$) +(declare-fun fun_app$x (A_llist_a_llist_prod_a_llist_a_llist_prod_set_fun$ A_llist_a_llist_prod$) A_llist_a_llist_prod_set$) +(declare-fun fun_app$y (A_llist_a_llist_prod_a_llist_a_llist_bool_fun_fun_fun$ A_llist_a_llist_prod$) A_llist_a_llist_bool_fun_fun$) +(declare-fun fun_app$z (A_llist_a_llist_fun_a_llist_a_llist_bool_fun_fun_fun$ A_llist_a_llist_fun$) A_llist_a_llist_bool_fun_fun$) +(declare-fun lappend$a (A_llist$) A_llist_a_llist_fun$) +(declare-fun less_eq$a (A_set$ A_set$) Bool) +(declare-fun less_eq$b (A_llist_a_llist_prod_bool_fun$) A_llist_a_llist_prod_bool_fun_bool_fun$) +(declare-fun less_eq$c (A_llist_a_llist_bool_fun_fun$ A_llist_a_llist_bool_fun_fun$) Bool) +(declare-fun lex_prod$ (A_llist_a_llist_prod_set$ A_llist_a_llist_prod_set$) A_llist_a_llist_prod_a_llist_a_llist_prod_prod_set$) +(declare-fun lfinite$a (A_llist$) Bool) +(declare-fun lmember$a (A$) A_llist_bool_fun$) +(declare-fun lprefix$a (A_llist_a_llist_prod_llist$) A_llist_a_llist_prod_llist_bool_fun$) +(declare-fun same_fst$ (A_llist_bool_fun$ A_llist_a_llist_a_llist_prod_set_fun$) A_llist_a_llist_prod_a_llist_a_llist_prod_prod_set$) +(declare-fun uncurry$a () A_llist_a_llist_bool_fun_fun_a_llist_a_llist_prod_bool_fun_fun$) +(declare-fun uncurry$b () A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun_a_llist_a_llist_prod_a_llist_a_llist_prod_set_fun_fun$) +(declare-fun uncurry$c () A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun_a_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun_fun$) +(declare-fun uncurry$d () A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_bool_fun_fun$) +(declare-fun uncurry$e (A_llist_a_llist_a_set_fun_fun$ A_llist_a_llist_prod$) A_set$) +(declare-fun uncurry$f (A_llist_a_llist_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_set_fun_fun$ A_llist_a_llist_prod$) A_llist_a_llist_prod_a_llist_a_llist_prod_prod_set$) +(declare-fun uncurry$g (A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_set_fun_fun$ A_llist_a_llist_prod_a_llist_a_llist_prod_prod$) A_llist_a_llist_prod_set$) +(declare-fun uncurry$h (A_llist_a_llist_prod_a_llist_a_llist_prod_a_set_fun_fun$ A_llist_a_llist_prod_a_llist_a_llist_prod_prod$) A_set$) +(declare-fun uncurry$i (A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_set_fun_fun$ A_llist_a_llist_prod_a_llist_a_llist_prod_prod$) A_llist_a_llist_prod_a_llist_a_llist_prod_prod_set$) +(declare-fun uncurry$j (A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_fun_fun$ A_llist_a_llist_prod_a_llist_a_llist_prod_prod$) A_llist_a_llist_prod$) +(declare-fun uncurry$k (A_llist_a_llist_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_fun_fun$ A_llist_a_llist_prod$) A_llist_a_llist_prod_a_llist_a_llist_prod_prod$) +(declare-fun uncurry$l (A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_fun_fun$ A_llist_a_llist_prod_a_llist_a_llist_prod_prod$) A_llist_a_llist_prod_a_llist_a_llist_prod_prod$) +(declare-fun fun_app$aa (A_llist_a_llist_a_llist_bool_fun_fun_fun$ A_llist$) A_llist_a_llist_bool_fun_fun$) +(declare-fun fun_app$ab (A_llist_a_llist_a_llist_a_llist_prod_fun_fun_a_llist_a_llist_prod_a_llist_a_llist_prod_fun_fun$ A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) A_llist_a_llist_prod_a_llist_a_llist_prod_fun$) +(declare-fun fun_app$ac (A_llist_a_llist_a_llist_a_llist_prod_fun_fun_a_llist_a_llist_bool_fun_fun_fun$ A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) A_llist_a_llist_bool_fun_fun$) +(declare-fun fun_app$ad (A_llist_a_llist_bool_fun_fun_a_llist_a_llist_prod_bool_fun_fun$ A_llist_a_llist_bool_fun_fun$) A_llist_a_llist_prod_bool_fun$) +(declare-fun fun_app$ae (A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_fun_fun_a_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun_fun$ A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_fun_fun$) A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) +(declare-fun fun_app$af (A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_fun_fun$ A_llist_a_llist_prod$) A_llist_a_llist_prod_a_llist_a_llist_prod_fun$) +(declare-fun fun_app$ag (A_llist_a_llist_a_llist_a_llist_prod_fun_fun_a_llist_a_llist_a_llist_a_llist_prod_set_fun_fun_fun$ A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$) +(declare-fun fun_app$ah (A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun_a_llist_a_llist_prod_a_llist_a_llist_prod_set_fun_fun$ A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$) A_llist_a_llist_prod_a_llist_a_llist_prod_set_fun$) +(declare-fun fun_app$ai (A_llist_a_llist_a_llist_a_llist_prod_fun_fun_a_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun_fun$ A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$) +(declare-fun fun_app$aj (A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun_a_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun_fun$ A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$) A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) +(declare-fun fun_app$ak (A_llist_a_llist_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_fun_fun_a_llist_a_llist_bool_fun_fun_fun$ A_llist_a_llist_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_fun_fun$) A_llist_a_llist_bool_fun_fun$) +(declare-fun fun_app$al (A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_bool_fun_fun$ A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) A_llist_a_llist_prod_a_llist_a_llist_prod_prod_bool_fun$) +(declare-fun fun_app$am (A_llist_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_fun$ A_llist$) A_llist_a_llist_prod_a_llist_a_llist_prod_prod$) +(declare-fun fun_app$an (A_llist_a_llist_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_fun_fun$ A_llist$) A_llist_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_fun$) +(declare-fun fun_app$ao (A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_fun_fun_a_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun_fun$ A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_fun_fun$) A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) +(declare-fun fun_app$ap (A_llist_a_llist_bool_fun_fun_a_llist_a_llist_bool_fun_fun_fun$ A_llist_a_llist_bool_fun_fun$) A_llist_a_llist_bool_fun_fun$) +(declare-fun fun_app$aq (A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun_a_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun_fun$ A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) +(declare-fun fun_app$ar (A_a_llist_a_llist_fun_fun_a_a_llist_a_llist_fun_fun_fun$ A_a_llist_a_llist_fun_fun$) A_a_llist_a_llist_fun_fun$) +(declare-fun fun_app$as (A_a_llist_bool_fun_fun$ A$) A_llist_bool_fun$) +(declare-fun fun_app$at (A_a_llist_a_llist_fun_fun_a_a_llist_bool_fun_fun_fun$ A_a_llist_a_llist_fun_fun$) A_a_llist_bool_fun_fun$) +(declare-fun fun_app$au (A_a_llist_a_fun_fun$ A$) A_llist_a_fun$) +(declare-fun fun_app$av (A_a_llist_a_llist_fun_fun_a_a_llist_a_fun_fun_fun$ A_a_llist_a_llist_fun_fun$) A_a_llist_a_fun_fun$) +(declare-fun fun_app$aw (A_a_llist_bool_fun_fun_a_a_llist_a_llist_fun_fun_fun$ A_a_llist_bool_fun_fun$) A_a_llist_a_llist_fun_fun$) +(declare-fun fun_app$ax (Bool_a_llist_fun$ Bool) A_llist$) +(declare-fun fun_app$ay (Bool_a_llist_a_llist_prod_fun$ Bool) A_llist_a_llist_prod$) +(declare-fun fun_app$az (Bool_bool_fun$ Bool) Bool) +(declare-fun fun_app$ba (A_a_llist_bool_fun_fun_a_a_llist_bool_fun_fun_fun$ A_a_llist_bool_fun_fun$) A_a_llist_bool_fun_fun$) +(declare-fun fun_app$bb (A_llist_a_llist_bool_fun_fun_a_llist_a_llist_a_llist_a_llist_prod_set_fun_fun_fun$ A_llist_a_llist_bool_fun_fun$) A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$) +(declare-fun fun_app$bc (Bool_a_llist_a_llist_prod_set_fun$ Bool) A_llist_a_llist_prod_set$) +(declare-fun fun_app$bd (A_llist_a_llist_bool_fun_fun_a_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun_fun$ A_llist_a_llist_bool_fun_fun$) A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$) +(declare-fun fun_app$be (Bool_a_llist_a_llist_prod_bool_fun_fun$ Bool) A_llist_a_llist_prod_bool_fun$) +(declare-fun fun_app$bf (A_a_llist_bool_fun_fun_a_a_llist_a_fun_fun_fun$ A_a_llist_bool_fun_fun$) A_a_llist_a_fun_fun$) +(declare-fun fun_app$bg (Bool_a_fun$ Bool) A$) +(declare-fun fun_app$bh (A_llist_a_llist_prod_set_a_llist_a_llist_prod_fun$ A_llist_a_llist_prod_set$) A_llist_a_llist_prod$) +(declare-fun fun_app$bi (A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun_a_llist_a_llist_bool_fun_fun_fun$ A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$) A_llist_a_llist_bool_fun_fun$) +(declare-fun fun_app$bj (A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun_a_llist_a_llist_bool_fun_fun_fun$ A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$) A_llist_a_llist_bool_fun_fun$) +(declare-fun fun_app$bk (A_llist_a_llist_prod_bool_fun_bool_fun$ A_llist_a_llist_prod_bool_fun$) Bool) +(declare-fun fun_app$bl (A_a_llist_a_fun_fun_a_a_llist_a_llist_fun_fun_fun$ A_a_llist_a_fun_fun$) A_a_llist_a_llist_fun_fun$) +(declare-fun fun_app$bm (A_a_llist_fun$ A$) A_llist$) +(declare-fun fun_app$bn (A_a_llist_a_fun_fun_a_a_llist_bool_fun_fun_fun$ A_a_llist_a_fun_fun$) A_a_llist_bool_fun_fun$) +(declare-fun fun_app$bo (A_a_llist_a_fun_fun_a_a_llist_a_fun_fun_fun$ A_a_llist_a_fun_fun$) A_a_llist_a_fun_fun$) +(declare-fun fun_app$bp (A_a_fun$ A$) A$) +(declare-fun fun_app$bq (A_llist_a_llist_prod_set_a_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun_fun$ A_llist_a_llist_prod_set$) A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$) +(declare-fun fun_app$br (A_llist_a_llist_a_llist_a_llist_bool_fun_fun_fun_fun$ A_llist$) A_llist_a_llist_a_llist_bool_fun_fun_fun$) +(declare-fun fun_app$bs (A_llist_a_llist_prod_set_a_llist_a_llist_a_llist_a_llist_bool_fun_fun_fun_fun_fun$ A_llist_a_llist_prod_set$) A_llist_a_llist_a_llist_a_llist_bool_fun_fun_fun_fun$) +(declare-fun fun_app$bt (A_llist_a_llist_a_llist_prod_set_fun_a_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun_fun$ A_llist_a_llist_a_llist_prod_set_fun$) A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$) +(declare-fun fun_app$bu (A_llist_a_llist_a_llist_prod_set_fun_a_llist_a_llist_a_llist_a_llist_bool_fun_fun_fun_fun_fun$ A_llist_a_llist_a_llist_prod_set_fun$) A_llist_a_llist_a_llist_a_llist_bool_fun_fun_fun_fun$) +(declare-fun fun_app$bv (A_llist_a_llist_prod_a_llist_a_llist_prod_llist_a_llist_a_llist_prod_fun_fun$ A_llist_a_llist_prod$) A_llist_a_llist_prod_llist_a_llist_a_llist_prod_fun$) +(declare-fun fun_app$bw (A_llist_a_llist_prod_llist_bool_fun$ A_llist_a_llist_prod_llist$) Bool) +(declare-fun fun_app$bx (A_llist_a_llist_prod_a_llist_a_llist_prod_llist_bool_fun_fun$ A_llist_a_llist_prod$) A_llist_a_llist_prod_llist_bool_fun$) +(declare-fun fun_app$by (A_llist_a_llist_prod_llist_a_llist_a_llist_prod_llist_bool_fun_fun$ A_llist_a_llist_prod_llist$) A_llist_a_llist_prod_llist_bool_fun$) +(declare-fun fun_app$bz (A_llist_a_set_fun$ A_llist$) A_set$) +(declare-fun fun_app$ca (A_llist_a_llist_a_set_fun_fun$ A_llist$) A_llist_a_set_fun$) +(declare-fun fun_app$cb (A_llist_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_set_fun$ A_llist$) A_llist_a_llist_prod_a_llist_a_llist_prod_prod_set$) +(declare-fun fun_app$cc (A_llist_a_llist_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_set_fun_fun$ A_llist$) A_llist_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_set_fun$) +(declare-fun fun_app$cd (A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_set_fun_fun$ A_llist_a_llist_prod$) A_llist_a_llist_prod_a_llist_a_llist_prod_set_fun$) +(declare-fun fun_app$ce (A_llist_a_llist_prod_a_set_fun$ A_llist_a_llist_prod$) A_set$) +(declare-fun fun_app$cf (A_llist_a_llist_prod_a_llist_a_llist_prod_a_set_fun_fun$ A_llist_a_llist_prod$) A_llist_a_llist_prod_a_set_fun$) +(declare-fun fun_app$cg (A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_set_fun$ A_llist_a_llist_prod$) A_llist_a_llist_prod_a_llist_a_llist_prod_prod_set$) +(declare-fun fun_app$ch (A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_set_fun_fun$ A_llist_a_llist_prod$) A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_set_fun$) +(declare-fun fun_app$ci (A_a_llist_bool_fun_fun_a_llist_bool_fun_fun$ A_a_llist_bool_fun_fun$) A_llist_bool_fun$) +(declare-fun fun_app$cj (A_a_llist_a_llist_fun_fun_a_llist_a_llist_fun_fun$ A_a_llist_a_llist_fun_fun$) A_llist_a_llist_fun$) +(declare-fun fun_app$ck (A_a_llist_a_fun_fun_a_llist_a_fun_fun$ A_a_llist_a_fun_fun$) A_llist_a_fun$) +(declare-fun fun_app$cl (A_llist_a_llist_fun_a_llist_a_llist_fun_fun$ A_llist_a_llist_fun$) A_llist_a_llist_fun$) +(declare-fun fun_app$cm (A_llist_a_fun_a_llist_a_llist_fun_a_llist_a_llist_fun_fun_fun$ A_llist_a_fun$) A_llist_a_llist_fun_a_llist_a_llist_fun_fun$) +(declare-fun fun_app$cn (A_llist_a_llist_prod_a_llist_a_llist_prod_llist_bool_fun_fun_a_llist_a_llist_prod_llist_bool_fun_fun$ A_llist_a_llist_prod_a_llist_a_llist_prod_llist_bool_fun_fun$) A_llist_a_llist_prod_llist_bool_fun$) +(declare-fun fun_app$co (A_a_bool_fun_fun$ A$) A_bool_fun$) +(declare-fun fun_app$cp (A_llist_a_llist_prod_a_llist_fun$ A_llist_a_llist_prod$) A_llist$) +(declare-fun inv_image$ (A_llist_a_llist_prod_set$ A_llist_a_llist_fun$) A_llist_a_llist_prod_set$) +(declare-fun undefined$ () A_llist$) +(declare-fun case_llist$ (Bool) A_a_llist_bool_fun_fun_a_llist_bool_fun_fun$) +(declare-fun llist_all2$ (A_a_bool_fun_fun$) A_llist_a_llist_bool_fun_fun$) +(declare-fun pred_llist$ (A_bool_fun$) A_llist_bool_fun$) +(declare-fun undefined$a () A$) +(declare-fun case_llist$a (A_llist$) A_a_llist_a_llist_fun_fun_a_llist_a_llist_fun_fun$) +(declare-fun case_llist$b (A$) A_a_llist_a_fun_fun_a_llist_a_fun_fun$) +(declare-fun case_llist$c (Bool) A_llist_a_llist_prod_a_llist_a_llist_prod_llist_bool_fun_fun_a_llist_a_llist_prod_llist_bool_fun_fun$) +(declare-fun case_llist$d (A_llist_a_llist_prod_llist$ A_llist_a_llist_prod_a_llist_a_llist_prod_llist_a_llist_a_llist_prod_llist_fun_fun$ A_llist_a_llist_prod_llist$) A_llist_a_llist_prod_llist$) +(declare-fun case_llist$e (A_llist_a_llist_prod$ A_llist_a_llist_prod_a_llist_a_llist_prod_llist_a_llist_a_llist_prod_fun_fun$ A_llist_a_llist_prod_llist$) A_llist_a_llist_prod$) +(declare-fun llist_all2$a (A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) A_llist_a_llist_prod_llist_a_llist_a_llist_prod_llist_bool_fun_fun$) +(declare-fun pred_llist$a (A_llist_a_llist_prod_bool_fun$) A_llist_a_llist_prod_llist_bool_fun$) +(declare-fun unfold_llist$ (A_llist_a_llist_prod_llist_bool_fun$ A_llist_a_llist_prod_llist_a_llist_a_llist_prod_fun$ A_llist_a_llist_prod_llist_a_llist_a_llist_prod_llist_fun$ A_llist_a_llist_prod_llist$) A_llist_a_llist_prod_llist$) +(declare-fun unfold_llist$a (A_llist_bool_fun$) A_llist_a_fun_a_llist_a_llist_fun_a_llist_a_llist_fun_fun_fun$) +(declare-fun internal_split$ () A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun_a_llist_a_llist_prod_a_llist_a_llist_prod_set_fun_fun$) +(declare-fun internal_split$a () A_llist_a_llist_a_llist_a_llist_prod_fun_fun_a_llist_a_llist_prod_a_llist_a_llist_prod_fun_fun$) +(declare-fun internal_split$b () A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_bool_fun_fun$) +(declare-fun internal_split$c () A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun_a_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun_fun$) +(declare-fun internal_split$d () A_llist_a_llist_bool_fun_fun_a_llist_a_llist_prod_bool_fun_fun$) +(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$)) (! (= (fun_app$ uvd$ ?v0) (ltl$a ?v0)) :pattern ((fun_app$ uvd$ ?v0)))) :named a0)) +(assert (! (forall ((?v0 A_llist$)) (! (= (fun_app$a uvf$ ?v0) (ltl$ ?v0)) :pattern ((fun_app$a uvf$ ?v0)))) :named a1)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$)) (! (= (fun_app$b uvc$ ?v0) (lhd$a ?v0)) :pattern ((fun_app$b uvc$ ?v0)))) :named a2)) +(assert (! (forall ((?v0 A_llist$)) (! (= (fun_app$c uve$ ?v0) (lhd$ ?v0)) :pattern ((fun_app$c uve$ ?v0)))) :named a3)) +(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$)) (! (= (fun_app$d (fun_app$e uvx$ ?v0) ?v1) (pair$ ?v0 ?v1)) :pattern ((fun_app$d (fun_app$e uvx$ ?v0) ?v1)))) :named a4)) +(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod$)) (! (= (fun_app$f (fun_app$g uvw$ ?v0) ?v1) (pair$b ?v0 ?v1)) :pattern ((fun_app$f (fun_app$g uvw$ ?v0) ?v1)))) :named a5)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_set$) (?v1 A_llist_a_llist_prod$)) (! (= (fun_app$h (uui$ ?v0) ?v1) (fun_app$i (member$ ?v1) ?v0)) :pattern ((fun_app$h (uui$ ?v0) ?v1)))) :named a6)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_prod_set$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$)) (! (= (fun_app$j (uuh$ ?v0) ?v1) (member$a ?v1 ?v0)) :pattern ((fun_app$j (uuh$ ?v0) ?v1)))) :named a7)) +(assert (! (forall ((?v0 A_set$) (?v1 A$)) (! (= (fun_app$k (uug$ ?v0) ?v1) (member$b ?v1 ?v0)) :pattern ((fun_app$k (uug$ ?v0) ?v1)))) :named a8)) +(assert (! (forall ((?v0 A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) (?v1 A_llist$) (?v2 A_llist$)) (! (= (fun_app$d (fun_app$e (uwd$ ?v0) ?v1) ?v2) (fun_app$d (fun_app$e ?v0 ?v2) ?v1)) :pattern ((fun_app$d (fun_app$e (uwd$ ?v0) ?v1) ?v2)))) :named a9)) +(assert (! (forall ((?v0 A_llist_a_llist_bool_fun_fun$) (?v1 A_llist$) (?v2 A_llist$)) (! (= (fun_app$l (fun_app$m (uwg$ ?v0) ?v1) ?v2) (fun_app$l (fun_app$m ?v0 ?v2) ?v1)) :pattern ((fun_app$l (fun_app$m (uwg$ ?v0) ?v1) ?v2)))) :named a10)) +(assert (! (forall ((?v0 A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$) (?v1 A_llist$) (?v2 A_llist$)) (! (= (fun_app$n (fun_app$o (uwc$ ?v0) ?v1) ?v2) (fun_app$n (fun_app$o ?v0 ?v2) ?v1)) :pattern ((fun_app$n (fun_app$o (uwc$ ?v0) ?v1) ?v2)))) :named a11)) +(assert (! (forall ((?v0 A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$) (?v1 A_llist$) (?v2 A_llist$)) (! (= (fun_app$p (fun_app$q (uwf$ ?v0) ?v1) ?v2) (fun_app$p (fun_app$q ?v0 ?v2) ?v1)) :pattern ((fun_app$p (fun_app$q (uwf$ ?v0) ?v1) ?v2)))) :named a12)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) (?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_prod$)) (! (= (fun_app$h (fun_app$r (uwe$ ?v0) ?v1) ?v2) (fun_app$h (fun_app$r ?v0 ?v2) ?v1)) :pattern ((fun_app$h (fun_app$r (uwe$ ?v0) ?v1) ?v2)))) :named a13)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_set$) (?v1 A_llist_a_llist_prod_set$) (?v2 A_llist_a_llist_prod$)) (! (= (fun_app$h (fun_app$s (uwq$ ?v0) ?v1) ?v2) (or (fun_app$i (member$ ?v2) ?v0) (fun_app$i (member$ ?v2) ?v1))) :pattern ((fun_app$h (fun_app$s (uwq$ ?v0) ?v1) ?v2)))) :named a14)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_set$) (?v1 A_llist_a_llist_prod_bool_fun$) (?v2 A_llist_a_llist_prod$)) (! (= (fun_app$h (fun_app$t (uws$ ?v0) ?v1) ?v2) (and (fun_app$i (member$ ?v2) ?v0) (fun_app$h ?v1 ?v2))) :pattern ((fun_app$h (fun_app$t (uws$ ?v0) ?v1) ?v2)))) :named a15)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_set$) (?v1 A_llist$) (?v2 A_llist$)) (! (= (fun_app$l (fun_app$m (uvz$ ?v0) ?v1) ?v2) (fun_app$i (member$ (pair$ ?v1 ?v2)) ?v0)) :pattern ((fun_app$l (fun_app$m (uvz$ ?v0) ?v1) ?v2)))) :named a16)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_prod_set$) (?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_prod$)) (! (= (fun_app$h (fun_app$r (uvy$ ?v0) ?v1) ?v2) (member$a (pair$b ?v1 ?v2) ?v0)) :pattern ((fun_app$h (fun_app$r (uvy$ ?v0) ?v1) ?v2)))) :named a17)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_bool_fun$) (?v1 A_llist_a_llist_prod_bool_fun$) (?v2 A_llist_a_llist_prod$)) (! (= (fun_app$h (fun_app$t (uwp$ ?v0) ?v1) ?v2) (or (fun_app$h ?v0 ?v2) (fun_app$h ?v1 ?v2))) :pattern ((fun_app$h (fun_app$t (uwp$ ?v0) ?v1) ?v2)))) :named a18)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_bool_fun$) (?v1 A_llist_a_llist_prod_bool_fun$) (?v2 A_llist_a_llist_prod$)) (! (= (fun_app$h (fun_app$t (uwr$ ?v0) ?v1) ?v2) (and (fun_app$h ?v0 ?v2) (fun_app$h ?v1 ?v2))) :pattern ((fun_app$h (fun_app$t (uwr$ ?v0) ?v1) ?v2)))) :named a19)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$) (?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_prod_llist$)) (! (= (fun_app$ (fun_app$u (uwh$ ?v0) ?v1) ?v2) (lCons$a ?v1 (fun_app$ (lappend$ ?v2) ?v0))) :pattern ((fun_app$ (fun_app$u (uwh$ ?v0) ?v1) ?v2)))) :named a20)) +(assert (! (forall ((?v0 A_llist$) (?v1 A$) (?v2 A_llist$)) (! (= (fun_app$a (fun_app$v (uwi$ ?v0) ?v1) ?v2) (lCons$ ?v1 (fun_app$a (lappend$a ?v2) ?v0))) :pattern ((fun_app$a (fun_app$v (uwi$ ?v0) ?v1) ?v2)))) :named a21)) +(assert (! (forall ((?v0 A_llist$) (?v1 A$) (?v2 A_llist$)) (! (= (fun_app$a (fun_app$v (uwj$ ?v0) ?v1) ?v2) (fun_app$a (lappend$a ?v2) ?v0)) :pattern ((fun_app$a (fun_app$v (uwj$ ?v0) ?v1) ?v2)))) :named a22)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_fun$) (?v1 A_llist$) (?v2 A_llist$)) (! (= (fun_app$d (fun_app$e (uuc$ ?v0) ?v1) ?v2) (fun_app$w ?v0 (pair$ ?v1 ?v2))) :pattern ((fun_app$d (fun_app$e (uuc$ ?v0) ?v1) ?v2)))) :named a23)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_bool_fun$) (?v1 A_llist$) (?v2 A_llist$)) (! (= (fun_app$l (fun_app$m (uuf$ ?v0) ?v1) ?v2) (fun_app$h ?v0 (pair$ ?v1 ?v2))) :pattern ((fun_app$l (fun_app$m (uuf$ ?v0) ?v1) ?v2)))) :named a24)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_set_fun$) (?v1 A_llist$) (?v2 A_llist$)) (! (= (fun_app$n (fun_app$o (uub$ ?v0) ?v1) ?v2) (fun_app$x ?v0 (pair$ ?v1 ?v2))) :pattern ((fun_app$n (fun_app$o (uub$ ?v0) ?v1) ?v2)))) :named a25)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) (?v1 A_llist$) (?v2 A_llist$)) (! (= (fun_app$p (fun_app$q (uue$ ?v0) ?v1) ?v2) (fun_app$r ?v0 (pair$ ?v1 ?v2))) :pattern ((fun_app$p (fun_app$q (uue$ ?v0) ?v1) ?v2)))) :named a26)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_prod_bool_fun$) (?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_prod$)) (! (= (fun_app$h (fun_app$r (uud$ ?v0) ?v1) ?v2) (fun_app$j ?v0 (pair$b ?v1 ?v2))) :pattern ((fun_app$h (fun_app$r (uud$ ?v0) ?v1) ?v2)))) :named a27)) +(assert (! (forall ((?v0 A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$) (?v1 A_llist_a_llist_prod$) (?v2 A_llist$) (?v3 A_llist$)) (! (= (fun_app$l (fun_app$m (fun_app$y (uvg$ ?v0) ?v1) ?v2) ?v3) (fun_app$h (fun_app$p (fun_app$q ?v0 ?v2) ?v3) ?v1)) :pattern ((fun_app$l (fun_app$m (fun_app$y (uvg$ ?v0) ?v1) ?v2) ?v3)))) :named a28)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_set$) (?v1 A_llist_a_llist_fun$) (?v2 A_llist$) (?v3 A_llist$)) (! (= (fun_app$l (fun_app$m (fun_app$z (uwk$ ?v0) ?v1) ?v2) ?v3) (fun_app$i (member$ (pair$ (fun_app$a ?v1 ?v2) (fun_app$a ?v1 ?v3))) ?v0)) :pattern ((fun_app$l (fun_app$m (fun_app$z (uwk$ ?v0) ?v1) ?v2) ?v3)))) :named a29)) +(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$) (?v2 A_llist$) (?v3 A_llist$)) (! (= (fun_app$l (fun_app$m (fun_app$aa (uwt$ ?v0) ?v1) ?v2) ?v3) (and (= ?v0 ?v2) (= ?v1 ?v3))) :pattern ((fun_app$l (fun_app$m (fun_app$aa (uwt$ ?v0) ?v1) ?v2) ?v3)))) :named a30)) +(assert (! (forall ((?v0 A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) (?v2 A_llist$) (?v3 A_llist$)) (! (= (fun_app$d (fun_app$e (uuv$ ?v0 ?v1) ?v2) ?v3) (fun_app$w (fun_app$ab uncurry$ ?v0) (fun_app$d (fun_app$e ?v1 ?v2) ?v3))) :pattern ((fun_app$d (fun_app$e (uuv$ ?v0 ?v1) ?v2) ?v3)))) :named a31)) +(assert (! (forall ((?v0 A_llist_a_llist_bool_fun_fun$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) (?v2 A_llist$) (?v3 A_llist$)) (! (= (fun_app$l (fun_app$m (fun_app$ac (uuz$ ?v0) ?v1) ?v2) ?v3) (fun_app$h (fun_app$ad uncurry$a ?v0) (fun_app$d (fun_app$e ?v1 ?v2) ?v3))) :pattern ((fun_app$l (fun_app$m (fun_app$ac (uuz$ ?v0) ?v1) ?v2) ?v3)))) :named a32)) +(assert (! (forall ((?v0 A_llist_a_llist_bool_fun_fun$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_fun_fun$) (?v2 A_llist_a_llist_prod$) (?v3 A_llist_a_llist_prod$)) (! (= (fun_app$h (fun_app$r (fun_app$ae (uut$ ?v0) ?v1) ?v2) ?v3) (fun_app$h (fun_app$ad uncurry$a ?v0) (fun_app$w (fun_app$af ?v1 ?v2) ?v3))) :pattern ((fun_app$h (fun_app$r (fun_app$ae (uut$ ?v0) ?v1) ?v2) ?v3)))) :named a33)) +(assert (! (forall ((?v0 A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) (?v2 A_llist$) (?v3 A_llist$)) (! (= (fun_app$n (fun_app$o (fun_app$ag (uuu$ ?v0) ?v1) ?v2) ?v3) (fun_app$x (fun_app$ah uncurry$b ?v0) (fun_app$d (fun_app$e ?v1 ?v2) ?v3))) :pattern ((fun_app$n (fun_app$o (fun_app$ag (uuu$ ?v0) ?v1) ?v2) ?v3)))) :named a34)) +(assert (! (forall ((?v0 A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) (?v2 A_llist$) (?v3 A_llist$)) (! (= (fun_app$p (fun_app$q (fun_app$ai (uuy$ ?v0) ?v1) ?v2) ?v3) (fun_app$r (fun_app$aj uncurry$c ?v0) (fun_app$d (fun_app$e ?v1 ?v2) ?v3))) :pattern ((fun_app$p (fun_app$q (fun_app$ai (uuy$ ?v0) ?v1) ?v2) ?v3)))) :named a35)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_fun_fun$) (?v2 A_llist$) (?v3 A_llist$)) (! (= (fun_app$l (fun_app$m (fun_app$ak (uuw$ ?v0) ?v1) ?v2) ?v3) (fun_app$j (fun_app$al uncurry$d ?v0) (fun_app$am (fun_app$an ?v1 ?v2) ?v3))) :pattern ((fun_app$l (fun_app$m (fun_app$ak (uuw$ ?v0) ?v1) ?v2) ?v3)))) :named a36)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_fun_fun$) (?v2 A_llist_a_llist_prod$) (?v3 A_llist_a_llist_prod$)) (! (= (fun_app$h (fun_app$r (fun_app$ao (uux$ ?v0) ?v1) ?v2) ?v3) (fun_app$j (fun_app$al uncurry$d ?v0) (fun_app$f (fun_app$g ?v1 ?v2) ?v3))) :pattern ((fun_app$h (fun_app$r (fun_app$ao (uux$ ?v0) ?v1) ?v2) ?v3)))) :named a37)) +(assert (! (forall ((?v0 Bool) (?v1 A_llist_a_llist_bool_fun_fun$) (?v2 A_llist$) (?v3 A_llist$)) (! (= (fun_app$l (fun_app$m (fun_app$ap (uua$ ?v0) ?v1) ?v2) ?v3) (and ?v0 (fun_app$l (fun_app$m ?v1 ?v2) ?v3))) :pattern ((fun_app$l (fun_app$m (fun_app$ap (uua$ ?v0) ?v1) ?v2) ?v3)))) :named a38)) +(assert (! (forall ((?v0 Bool) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) (?v2 A_llist_a_llist_prod$) (?v3 A_llist_a_llist_prod$)) (! (= (fun_app$h (fun_app$r (fun_app$aq (uu$ ?v0) ?v1) ?v2) ?v3) (and ?v0 (fun_app$h (fun_app$r ?v1 ?v2) ?v3))) :pattern ((fun_app$h (fun_app$r (fun_app$aq (uu$ ?v0) ?v1) ?v2) ?v3)))) :named a39)) +(assert (! (forall ((?v0 A_llist_a_llist_fun$) (?v1 A_a_llist_a_llist_fun_fun$) (?v2 A$) (?v3 A_llist$)) (! (= (fun_app$a (fun_app$v (fun_app$ar (uvl$ ?v0) ?v1) ?v2) ?v3) (fun_app$a ?v0 (fun_app$a (fun_app$v ?v1 ?v2) ?v3))) :pattern ((fun_app$a (fun_app$v (fun_app$ar (uvl$ ?v0) ?v1) ?v2) ?v3)))) :named a40)) +(assert (! (forall ((?v0 A_llist_bool_fun$) (?v1 A_a_llist_a_llist_fun_fun$) (?v2 A$) (?v3 A_llist$)) (! (= (fun_app$l (fun_app$as (fun_app$at (uvk$ ?v0) ?v1) ?v2) ?v3) (fun_app$l ?v0 (fun_app$a (fun_app$v ?v1 ?v2) ?v3))) :pattern ((fun_app$l (fun_app$as (fun_app$at (uvk$ ?v0) ?v1) ?v2) ?v3)))) :named a41)) +(assert (! (forall ((?v0 A_llist_a_fun$) (?v1 A_a_llist_a_llist_fun_fun$) (?v2 A$) (?v3 A_llist$)) (! (= (fun_app$c (fun_app$au (fun_app$av (uvm$ ?v0) ?v1) ?v2) ?v3) (fun_app$c ?v0 (fun_app$a (fun_app$v ?v1 ?v2) ?v3))) :pattern ((fun_app$c (fun_app$au (fun_app$av (uvm$ ?v0) ?v1) ?v2) ?v3)))) :named a42)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_fun$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) (?v2 A_llist$) (?v3 A_llist$)) (! (= (fun_app$d (fun_app$e (uur$ ?v0 ?v1) ?v2) ?v3) (fun_app$w ?v0 (fun_app$d (fun_app$e ?v1 ?v2) ?v3))) :pattern ((fun_app$d (fun_app$e (uur$ ?v0 ?v1) ?v2) ?v3)))) :named a43)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_bool_fun$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) (?v2 A_llist$) (?v3 A_llist$)) (! (= (fun_app$l (fun_app$m (fun_app$ac (uul$ ?v0) ?v1) ?v2) ?v3) (fun_app$h ?v0 (fun_app$d (fun_app$e ?v1 ?v2) ?v3))) :pattern ((fun_app$l (fun_app$m (fun_app$ac (uul$ ?v0) ?v1) ?v2) ?v3)))) :named a44)) +(assert (! (forall ((?v0 Bool_a_llist_fun$) (?v1 A_a_llist_bool_fun_fun$) (?v2 A$) (?v3 A_llist$)) (! (= (fun_app$a (fun_app$v (fun_app$aw (uvi$ ?v0) ?v1) ?v2) ?v3) (fun_app$ax ?v0 (fun_app$l (fun_app$as ?v1 ?v2) ?v3))) :pattern ((fun_app$a (fun_app$v (fun_app$aw (uvi$ ?v0) ?v1) ?v2) ?v3)))) :named a45)) +(assert (! (forall ((?v0 Bool_a_llist_a_llist_prod_fun$) (?v1 A_llist_a_llist_bool_fun_fun$) (?v2 A_llist$) (?v3 A_llist$)) (! (= (fun_app$d (fun_app$e (uuk$ ?v0 ?v1) ?v2) ?v3) (fun_app$ay ?v0 (fun_app$l (fun_app$m ?v1 ?v2) ?v3))) :pattern ((fun_app$d (fun_app$e (uuk$ ?v0 ?v1) ?v2) ?v3)))) :named a46)) +(assert (! (forall ((?v0 Bool_bool_fun$) (?v1 A_llist_a_llist_bool_fun_fun$) (?v2 A_llist$) (?v3 A_llist$)) (! (= (fun_app$l (fun_app$m (fun_app$ap (uuj$ ?v0) ?v1) ?v2) ?v3) (fun_app$az ?v0 (fun_app$l (fun_app$m ?v1 ?v2) ?v3))) :pattern ((fun_app$l (fun_app$m (fun_app$ap (uuj$ ?v0) ?v1) ?v2) ?v3)))) :named a47)) +(assert (! (forall ((?v0 Bool_bool_fun$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) (?v2 A_llist_a_llist_prod$) (?v3 A_llist_a_llist_prod$)) (! (= (fun_app$h (fun_app$r (fun_app$aq (uup$ ?v0) ?v1) ?v2) ?v3) (fun_app$az ?v0 (fun_app$h (fun_app$r ?v1 ?v2) ?v3))) :pattern ((fun_app$h (fun_app$r (fun_app$aq (uup$ ?v0) ?v1) ?v2) ?v3)))) :named a48)) +(assert (! (forall ((?v0 Bool_bool_fun$) (?v1 A_a_llist_bool_fun_fun$) (?v2 A$) (?v3 A_llist$)) (! (= (fun_app$l (fun_app$as (fun_app$ba (uvh$ ?v0) ?v1) ?v2) ?v3) (fun_app$az ?v0 (fun_app$l (fun_app$as ?v1 ?v2) ?v3))) :pattern ((fun_app$l (fun_app$as (fun_app$ba (uvh$ ?v0) ?v1) ?v2) ?v3)))) :named a49)) +(assert (! (forall ((?v0 Bool_a_llist_a_llist_prod_set_fun$) (?v1 A_llist_a_llist_bool_fun_fun$) (?v2 A_llist$) (?v3 A_llist$)) (! (= (fun_app$n (fun_app$o (fun_app$bb (uum$ ?v0) ?v1) ?v2) ?v3) (fun_app$bc ?v0 (fun_app$l (fun_app$m ?v1 ?v2) ?v3))) :pattern ((fun_app$n (fun_app$o (fun_app$bb (uum$ ?v0) ?v1) ?v2) ?v3)))) :named a50)) +(assert (! (forall ((?v0 Bool_a_llist_a_llist_prod_bool_fun_fun$) (?v1 A_llist_a_llist_bool_fun_fun$) (?v2 A_llist$) (?v3 A_llist$)) (! (= (fun_app$p (fun_app$q (fun_app$bd (uuo$ ?v0) ?v1) ?v2) ?v3) (fun_app$be ?v0 (fun_app$l (fun_app$m ?v1 ?v2) ?v3))) :pattern ((fun_app$p (fun_app$q (fun_app$bd (uuo$ ?v0) ?v1) ?v2) ?v3)))) :named a51)) +(assert (! (forall ((?v0 Bool_a_fun$) (?v1 A_a_llist_bool_fun_fun$) (?v2 A$) (?v3 A_llist$)) (! (= (fun_app$c (fun_app$au (fun_app$bf (uvj$ ?v0) ?v1) ?v2) ?v3) (fun_app$bg ?v0 (fun_app$l (fun_app$as ?v1 ?v2) ?v3))) :pattern ((fun_app$c (fun_app$au (fun_app$bf (uvj$ ?v0) ?v1) ?v2) ?v3)))) :named a52)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_set_a_llist_a_llist_prod_fun$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$) (?v2 A_llist$) (?v3 A_llist$)) (! (= (fun_app$d (fun_app$e (uus$ ?v0 ?v1) ?v2) ?v3) (fun_app$bh ?v0 (fun_app$n (fun_app$o ?v1 ?v2) ?v3))) :pattern ((fun_app$d (fun_app$e (uus$ ?v0 ?v1) ?v2) ?v3)))) :named a53)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_set_bool_fun$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$) (?v2 A_llist$) (?v3 A_llist$)) (! (= (fun_app$l (fun_app$m (fun_app$bi (uun$ ?v0) ?v1) ?v2) ?v3) (fun_app$i ?v0 (fun_app$n (fun_app$o ?v1 ?v2) ?v3))) :pattern ((fun_app$l (fun_app$m (fun_app$bi (uun$ ?v0) ?v1) ?v2) ?v3)))) :named a54)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_bool_fun_bool_fun$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$) (?v2 A_llist$) (?v3 A_llist$)) (! (= (fun_app$l (fun_app$m (fun_app$bj (uuq$ ?v0) ?v1) ?v2) ?v3) (fun_app$bk ?v0 (fun_app$p (fun_app$q ?v1 ?v2) ?v3))) :pattern ((fun_app$l (fun_app$m (fun_app$bj (uuq$ ?v0) ?v1) ?v2) ?v3)))) :named a55)) +(assert (! (forall ((?v0 A_a_llist_fun$) (?v1 A_a_llist_a_fun_fun$) (?v2 A$) (?v3 A_llist$)) (! (= (fun_app$a (fun_app$v (fun_app$bl (uvo$ ?v0) ?v1) ?v2) ?v3) (fun_app$bm ?v0 (fun_app$c (fun_app$au ?v1 ?v2) ?v3))) :pattern ((fun_app$a (fun_app$v (fun_app$bl (uvo$ ?v0) ?v1) ?v2) ?v3)))) :named a56)) +(assert (! (forall ((?v0 A_bool_fun$) (?v1 A_a_llist_a_fun_fun$) (?v2 A$) (?v3 A_llist$)) (! (= (fun_app$l (fun_app$as (fun_app$bn (uvn$ ?v0) ?v1) ?v2) ?v3) (fun_app$k ?v0 (fun_app$c (fun_app$au ?v1 ?v2) ?v3))) :pattern ((fun_app$l (fun_app$as (fun_app$bn (uvn$ ?v0) ?v1) ?v2) ?v3)))) :named a57)) +(assert (! (forall ((?v0 A_a_fun$) (?v1 A_a_llist_a_fun_fun$) (?v2 A$) (?v3 A_llist$)) (! (= (fun_app$c (fun_app$au (fun_app$bo (uvp$ ?v0) ?v1) ?v2) ?v3) (fun_app$bp ?v0 (fun_app$c (fun_app$au ?v1 ?v2) ?v3))) :pattern ((fun_app$c (fun_app$au (fun_app$bo (uvp$ ?v0) ?v1) ?v2) ?v3)))) :named a58)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_set$) (?v1 A_llist_a_llist_prod_set$) (?v2 A_llist$) (?v3 A_llist$)) (! (= (fun_app$p (fun_app$q (fun_app$bq (uwo$ ?v0) ?v1) ?v2) ?v3) (fun_app$ad uncurry$a (fun_app$aa (fun_app$br (fun_app$bs (uwn$ ?v0) ?v1) ?v2) ?v3))) :pattern ((fun_app$p (fun_app$q (fun_app$bq (uwo$ ?v0) ?v1) ?v2) ?v3)))) :named a59)) +(assert (! (forall ((?v0 A_llist_bool_fun$) (?v1 A_llist_a_llist_a_llist_prod_set_fun$) (?v2 A_llist$) (?v3 A_llist$)) (! (= (fun_app$p (fun_app$q (fun_app$bt (uwm$ ?v0) ?v1) ?v2) ?v3) (fun_app$ad uncurry$a (fun_app$aa (fun_app$br (fun_app$bu (uwl$ ?v0) ?v1) ?v2) ?v3))) :pattern ((fun_app$p (fun_app$q (fun_app$bt (uwm$ ?v0) ?v1) ?v2) ?v3)))) :named a60)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_set$) (?v1 A_llist_a_llist_prod_set$) (?v2 A_llist$) (?v3 A_llist$) (?v4 A_llist$) (?v5 A_llist$)) (! (= (fun_app$l (fun_app$m (fun_app$aa (fun_app$br (fun_app$bs (uwn$ ?v0) ?v1) ?v2) ?v3) ?v4) ?v5) (or (fun_app$i (member$ (pair$ ?v2 ?v4)) ?v0) (and (= ?v2 ?v4) (fun_app$i (member$ (pair$ ?v3 ?v5)) ?v1)))) :pattern ((fun_app$l (fun_app$m (fun_app$aa (fun_app$br (fun_app$bs (uwn$ ?v0) ?v1) ?v2) ?v3) ?v4) ?v5)))) :named a61)) +(assert (! (forall ((?v0 A_llist_bool_fun$) (?v1 A_llist_a_llist_a_llist_prod_set_fun$) (?v2 A_llist$) (?v3 A_llist$) (?v4 A_llist$) (?v5 A_llist$)) (! (= (fun_app$l (fun_app$m (fun_app$aa (fun_app$br (fun_app$bu (uwl$ ?v0) ?v1) ?v2) ?v3) ?v4) ?v5) (and (= ?v2 ?v4) (and (fun_app$l ?v0 ?v4) (fun_app$i (member$ (pair$ ?v3 ?v5)) (fun_app$n ?v1 ?v4))))) :pattern ((fun_app$l (fun_app$m (fun_app$aa (fun_app$br (fun_app$bu (uwl$ ?v0) ?v1) ?v2) ?v3) ?v4) ?v5)))) :named a62)) +(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod_llist$)) (! (= (fun_app$b (fun_app$bv uwa$ ?v0) ?v1) ?v0) :pattern ((fun_app$b (fun_app$bv uwa$ ?v0) ?v1)))) :named a63)) +(assert (! (forall ((?v0 A$) (?v1 A_llist$)) (! (= (fun_app$c (fun_app$au uwb$ ?v0) ?v1) ?v0) :pattern ((fun_app$c (fun_app$au uwb$ ?v0) ?v1)))) :named a64)) +(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod_llist$)) (! (= (fun_app$ (fun_app$u uvu$ ?v0) ?v1) ?v1) :pattern ((fun_app$ (fun_app$u uvu$ ?v0) ?v1)))) :named a65)) +(assert (! (forall ((?v0 A$) (?v1 A_llist$)) (! (= (fun_app$a (fun_app$v uvv$ ?v0) ?v1) ?v1) :pattern ((fun_app$a (fun_app$v uvv$ ?v0) ?v1)))) :named a66)) +(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod_llist$)) (! (= (fun_app$bw (fun_app$bx uvs$ ?v0) ?v1) false) :pattern ((fun_app$bw (fun_app$bx uvs$ ?v0) ?v1)))) :named a67)) +(assert (! (forall ((?v0 A$) (?v1 A_llist$)) (! (= (fun_app$l (fun_app$as uvt$ ?v0) ?v1) false) :pattern ((fun_app$l (fun_app$as uvt$ ?v0) ?v1)))) :named a68)) +(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$)) (! (= (fun_app$l (fun_app$m uvb$ ?v0) ?v1) true) :pattern ((fun_app$l (fun_app$m uvb$ ?v0) ?v1)))) :named a69)) +(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod_llist$)) (! (= (fun_app$bw (fun_app$bx uvq$ ?v0) ?v1) true) :pattern ((fun_app$bw (fun_app$bx uvq$ ?v0) ?v1)))) :named a70)) +(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod$)) (! (= (fun_app$h (fun_app$r uva$ ?v0) ?v1) true) :pattern ((fun_app$h (fun_app$r uva$ ?v0) ?v1)))) :named a71)) +(assert (! (forall ((?v0 A$) (?v1 A_llist$)) (! (= (fun_app$l (fun_app$as uvr$ ?v0) ?v1) true) :pattern ((fun_app$l (fun_app$as uvr$ ?v0) ?v1)))) :named a72)) +(assert (! (not (fun_app$l (lprefix$ xs$) ys$)) :named a73)) +(assert (! (fun_app$l (fun_app$m p$ xs$) ys$) :named a74)) +(assert (! (fun_app$i (member$ (pair$ xs$ ys$)) (collect$ (fun_app$ad uncurry$a p$))) :named a75)) +(assert (! (forall ((?v0 A_llist$)) (fun_app$l (lprefix$ lNil$) ?v0)) :named a76)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$) (?v1 A_llist_a_llist_prod_llist$) (?v2 A_llist_a_llist_prod$)) (=> (fun_app$bw (lprefix$a ?v0) ?v1) (fun_app$bw (lprefix$a (lCons$a ?v2 ?v0)) (lCons$a ?v2 ?v1)))) :named a77)) +(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$) (?v2 A$)) (=> (fun_app$l (lprefix$ ?v0) ?v1) (fun_app$l (lprefix$ (lCons$ ?v2 ?v0)) (lCons$ ?v2 ?v1)))) :named a78)) +(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$)) (=> (fun_app$l (fun_app$m p$ ?v0) ?v1) (and (=> (fun_app$l lnull$ ?v1) (fun_app$l lnull$ ?v0)) (=> (and (not (fun_app$l lnull$ ?v0)) (not (fun_app$l lnull$ ?v1))) (and (= (lhd$ ?v0) (lhd$ ?v1)) (or (fun_app$l (fun_app$m p$ (ltl$ ?v0)) (ltl$ ?v1)) (fun_app$l (lprefix$ (ltl$ ?v0)) (ltl$ ?v1)))))))) :named a79)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$) (?v1 A_llist_a_llist_prod_llist$)) (= (fun_app$bw (lprefix$a ?v0) ?v1) (or (exists ((?v2 A_llist_a_llist_prod_llist$)) (and (= ?v0 lNil$a) (= ?v1 ?v2))) (exists ((?v2 A_llist_a_llist_prod_llist$) (?v3 A_llist_a_llist_prod_llist$) (?v4 A_llist_a_llist_prod$)) (and (= ?v0 (lCons$a ?v4 ?v2)) (and (= ?v1 (lCons$a ?v4 ?v3)) (fun_app$bw (lprefix$a ?v2) ?v3))))))) :named a80)) +(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$)) (= (fun_app$l (lprefix$ ?v0) ?v1) (or (exists ((?v2 A_llist$)) (and (= ?v0 lNil$) (= ?v1 ?v2))) (exists ((?v2 A_llist$) (?v3 A_llist$) (?v4 A$)) (and (= ?v0 (lCons$ ?v4 ?v2)) (and (= ?v1 (lCons$ ?v4 ?v3)) (fun_app$l (lprefix$ ?v2) ?v3))))))) :named a81)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$) (?v1 A_llist_a_llist_prod_llist$)) (=> (and (fun_app$bw (lprefix$a ?v0) ?v1) (and (forall ((?v2 A_llist_a_llist_prod_llist$)) (=> (and (= ?v0 lNil$a) (= ?v1 ?v2)) false)) (forall ((?v2 A_llist_a_llist_prod_llist$) (?v3 A_llist_a_llist_prod_llist$) (?v4 A_llist_a_llist_prod$)) (=> (and (= ?v0 (lCons$a ?v4 ?v2)) (and (= ?v1 (lCons$a ?v4 ?v3)) (fun_app$bw (lprefix$a ?v2) ?v3))) false)))) false)) :named a82)) +(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$)) (=> (and (fun_app$l (lprefix$ ?v0) ?v1) (and (forall ((?v2 A_llist$)) (=> (and (= ?v0 lNil$) (= ?v1 ?v2)) false)) (forall ((?v2 A_llist$) (?v3 A_llist$) (?v4 A$)) (=> (and (= ?v0 (lCons$ ?v4 ?v2)) (and (= ?v1 (lCons$ ?v4 ?v3)) (fun_app$l (lprefix$ ?v2) ?v3))) false)))) false)) :named a83)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_llist_a_llist_a_llist_prod_llist_bool_fun_fun$) (?v1 A_llist_a_llist_prod_llist$) (?v2 A_llist_a_llist_prod_llist$)) (=> (and (fun_app$bw (fun_app$by ?v0 ?v1) ?v2) (forall ((?v3 A_llist_a_llist_prod_llist$) (?v4 A_llist_a_llist_prod_llist$)) (=> (fun_app$bw (fun_app$by ?v0 ?v3) ?v4) (or (exists ((?v5 A_llist_a_llist_prod_llist$)) (and (= ?v3 lNil$a) (= ?v4 ?v5))) (exists ((?v5 A_llist_a_llist_prod_llist$) (?v6 A_llist_a_llist_prod_llist$) (?v7 A_llist_a_llist_prod$)) (and (= ?v3 (lCons$a ?v7 ?v5)) (and (= ?v4 (lCons$a ?v7 ?v6)) (or (fun_app$bw (fun_app$by ?v0 ?v5) ?v6) (fun_app$bw (lprefix$a ?v5) ?v6))))))))) (fun_app$bw (lprefix$a ?v1) ?v2))) :named a84)) +(assert (! (forall ((?v0 A_llist_a_llist_bool_fun_fun$) (?v1 A_llist$) (?v2 A_llist$)) (=> (and (fun_app$l (fun_app$m ?v0 ?v1) ?v2) (forall ((?v3 A_llist$) (?v4 A_llist$)) (=> (fun_app$l (fun_app$m ?v0 ?v3) ?v4) (or (exists ((?v5 A_llist$)) (and (= ?v3 lNil$) (= ?v4 ?v5))) (exists ((?v5 A_llist$) (?v6 A_llist$) (?v7 A$)) (and (= ?v3 (lCons$ ?v7 ?v5)) (and (= ?v4 (lCons$ ?v7 ?v6)) (or (fun_app$l (fun_app$m ?v0 ?v5) ?v6) (fun_app$l (lprefix$ ?v5) ?v6))))))))) (fun_app$l (lprefix$ ?v1) ?v2))) :named a85)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$) (?v1 A_llist_a_llist_prod_llist$) (?v2 A_llist_a_llist_prod_llist_a_llist_a_llist_prod_llist_prod_set$)) (=> (and (member$c (pair$a ?v0 ?v1) ?v2) (forall ((?v3 A_llist_a_llist_prod_llist$) (?v4 A_llist_a_llist_prod_llist$)) (=> (member$c (pair$a ?v3 ?v4) ?v2) (or (fun_app$bw lnull$a ?v3) (exists ((?v5 A_llist_a_llist_prod$) (?v6 A_llist_a_llist_prod_llist$) (?v7 A_llist_a_llist_prod_llist$)) (and (= ?v3 (lCons$a ?v5 ?v6)) (and (= ?v4 (lCons$a ?v5 ?v7)) (or (member$c (pair$a ?v6 ?v7) ?v2) (fun_app$bw (lprefix$a ?v6) ?v7))))))))) (fun_app$bw (lprefix$a ?v0) ?v1))) :named a86)) +(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$) (?v2 A_llist_a_llist_prod_set$)) (=> (and (fun_app$i (member$ (pair$ ?v0 ?v1)) ?v2) (forall ((?v3 A_llist$) (?v4 A_llist$)) (=> (fun_app$i (member$ (pair$ ?v3 ?v4)) ?v2) (or (fun_app$l lnull$ ?v3) (exists ((?v5 A$) (?v6 A_llist$) (?v7 A_llist$)) (and (= ?v3 (lCons$ ?v5 ?v6)) (and (= ?v4 (lCons$ ?v5 ?v7)) (or (fun_app$i (member$ (pair$ ?v6 ?v7)) ?v2) (fun_app$l (lprefix$ ?v6) ?v7))))))))) (fun_app$l (lprefix$ ?v0) ?v1))) :named a87)) +(assert (! (forall ((?v0 A$) (?v1 A_llist$) (?v2 A$) (?v3 A_llist$)) (= (= (lCons$ ?v0 ?v1) (lCons$ ?v2 ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3)))) :named a88)) +(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod_llist$) (?v2 A_llist_a_llist_prod$) (?v3 A_llist_a_llist_prod_llist$)) (= (= (lCons$a ?v0 ?v1) (lCons$a ?v2 ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3)))) :named a89)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$)) (=> (not (fun_app$bw lnull$a ?v0)) (= (lCons$a (lhd$a ?v0) (ltl$a ?v0)) ?v0))) :named a90)) +(assert (! (forall ((?v0 A_llist$)) (=> (not (fun_app$l lnull$ ?v0)) (= (lCons$ (lhd$ ?v0) (ltl$ ?v0)) ?v0))) :named a91)) +(assert (! (forall ((?v0 A_llist$)) (= (not (= ?v0 lNil$)) (exists ((?v1 A$) (?v2 A_llist$)) (= ?v0 (lCons$ ?v1 ?v2))))) :named a92)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$)) (= (not (= ?v0 lNil$a)) (exists ((?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_prod_llist$)) (= ?v0 (lCons$a ?v1 ?v2))))) :named a93)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$)) (= (not (fun_app$bw lnull$a ?v0)) (exists ((?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_prod_llist$)) (= ?v0 (lCons$a ?v1 ?v2))))) :named a94)) +(assert (! (forall ((?v0 A_llist$)) (= (not (fun_app$l lnull$ ?v0)) (exists ((?v1 A$) (?v2 A_llist$)) (= ?v0 (lCons$ ?v1 ?v2))))) :named a95)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$)) (! (= (fun_app$bw lnull$a ?v0) (= ?v0 lNil$a)) :pattern ((fun_app$bw lnull$a ?v0)))) :named a96)) +(assert (! (forall ((?v0 A_llist$)) (! (= (fun_app$l lnull$ ?v0) (= ?v0 lNil$)) :pattern ((fun_app$l lnull$ ?v0)))) :named a97)) +(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod_llist$)) (! (= (lhd$a (lCons$a ?v0 ?v1)) ?v0) :pattern ((lCons$a ?v0 ?v1)))) :named a98)) +(assert (! (forall ((?v0 A$) (?v1 A_llist$)) (! (= (lhd$ (lCons$ ?v0 ?v1)) ?v0) :pattern ((lCons$ ?v0 ?v1)))) :named a99)) +(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod_llist$)) (! (= (ltl$a (lCons$a ?v0 ?v1)) ?v1) :pattern ((lCons$a ?v0 ?v1)))) :named a100)) +(assert (! (forall ((?v0 A$) (?v1 A_llist$)) (! (= (ltl$ (lCons$ ?v0 ?v1)) ?v1) :pattern ((lCons$ ?v0 ?v1)))) :named a101)) +(assert (! (= (ltl$a lNil$a) lNil$a) :named a102)) +(assert (! (= (ltl$ lNil$) lNil$) :named a103)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$)) (=> (and (=> (= ?v0 lNil$a) false) (=> (= ?v0 (lCons$a (lhd$a ?v0) (ltl$a ?v0))) false)) false)) :named a104)) +(assert (! (forall ((?v0 A_llist$)) (=> (and (=> (= ?v0 lNil$) false) (=> (= ?v0 (lCons$ (lhd$ ?v0) (ltl$ ?v0))) false)) false)) :named a105)) +(assert (! (forall ((?v0 A_llist$)) (=> (and (=> (= ?v0 lNil$) false) (forall ((?v1 A$) (?v2 A_llist$)) (=> (= ?v0 (lCons$ ?v1 ?v2)) false))) false)) :named a106)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$)) (=> (and (=> (= ?v0 lNil$a) false) (forall ((?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_prod_llist$)) (=> (= ?v0 (lCons$a ?v1 ?v2)) false))) false)) :named a107)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$) (?v1 A_llist_a_llist_prod_llist$)) (=> (and (=> (and (fun_app$bw lnull$a ?v0) (fun_app$bw lnull$a ?v1)) false) (=> (or (not (fun_app$bw lnull$a ?v0)) (not (fun_app$bw lnull$a ?v1))) false)) false)) :named a108)) +(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$)) (=> (and (=> (and (fun_app$l lnull$ ?v0) (fun_app$l lnull$ ?v1)) false) (=> (or (not (fun_app$l lnull$ ?v0)) (not (fun_app$l lnull$ ?v1))) false)) false)) :named a109)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$)) (=> (and (=> (fun_app$bw lnull$a ?v0) false) (=> (not (fun_app$bw lnull$a ?v0)) false)) false)) :named a110)) +(assert (! (forall ((?v0 A_llist$)) (=> (and (=> (fun_app$l lnull$ ?v0) false) (=> (not (fun_app$l lnull$ ?v0)) false)) false)) :named a111)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$) (?v1 A_llist_a_llist_prod_llist$)) (=> (and (= (fun_app$bw lnull$a ?v0) (fun_app$bw lnull$a ?v1)) (=> (and (not (fun_app$bw lnull$a ?v0)) (not (fun_app$bw lnull$a ?v1))) (and (= (lhd$a ?v0) (lhd$a ?v1)) (= (ltl$a ?v0) (ltl$a ?v1))))) (= ?v0 ?v1))) :named a112)) +(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$)) (=> (and (= (fun_app$l lnull$ ?v0) (fun_app$l lnull$ ?v1)) (=> (and (not (fun_app$l lnull$ ?v0)) (not (fun_app$l lnull$ ?v1))) (and (= (lhd$ ?v0) (lhd$ ?v1)) (= (ltl$ ?v0) (ltl$ ?v1))))) (= ?v0 ?v1))) :named a113)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$) (?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_prod_llist$)) (=> (= ?v0 (lCons$a ?v1 ?v2)) (and (not (= ?v0 lNil$a)) (and (= (lhd$a ?v0) ?v1) (= (ltl$a ?v0) ?v2))))) :named a114)) +(assert (! (forall ((?v0 A_llist$) (?v1 A$) (?v2 A_llist$)) (=> (= ?v0 (lCons$ ?v1 ?v2)) (and (not (= ?v0 lNil$)) (and (= (lhd$ ?v0) ?v1) (= (ltl$ ?v0) ?v2))))) :named a115)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$) (?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_prod_llist$)) (=> (= ?v0 (lCons$a ?v1 ?v2)) (not (fun_app$bw lnull$a ?v0)))) :named a116)) +(assert (! (forall ((?v0 A_llist$) (?v1 A$) (?v2 A_llist$)) (=> (= ?v0 (lCons$ ?v1 ?v2)) (not (fun_app$l lnull$ ?v0)))) :named a117)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$)) (=> (= ?v0 lNil$a) (fun_app$bw lnull$a ?v0))) :named a118)) +(assert (! (forall ((?v0 A_llist$)) (=> (= ?v0 lNil$) (fun_app$l lnull$ ?v0))) :named a119)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$)) (=> (fun_app$bw lnull$a ?v0) (= ?v0 lNil$a))) :named a120)) +(assert (! (forall ((?v0 A_llist$)) (=> (fun_app$l lnull$ ?v0) (= ?v0 lNil$))) :named a121)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$)) (=> (fun_app$bw lnull$a ?v0) (fun_app$bw lnull$a (ltl$a ?v0)))) :named a122)) +(assert (! (forall ((?v0 A_llist$)) (=> (fun_app$l lnull$ ?v0) (fun_app$l lnull$ (ltl$ ?v0)))) :named a123)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_llist_a_llist_a_llist_prod_llist_bool_fun_fun$) (?v1 A_llist_a_llist_prod_llist$) (?v2 A_llist_a_llist_prod_llist$)) (=> (and (fun_app$bw (fun_app$by ?v0 ?v1) ?v2) (forall ((?v3 A_llist_a_llist_prod_llist$) (?v4 A_llist_a_llist_prod_llist$)) (=> (fun_app$bw (fun_app$by ?v0 ?v3) ?v4) (and (= (fun_app$bw lnull$a ?v3) (fun_app$bw lnull$a ?v4)) (=> (and (not (fun_app$bw lnull$a ?v3)) (not (fun_app$bw lnull$a ?v4))) (and (= (lhd$a ?v3) (lhd$a ?v4)) (or (fun_app$bw (fun_app$by ?v0 (ltl$a ?v3)) (ltl$a ?v4)) (= (ltl$a ?v3) (ltl$a ?v4))))))))) (= ?v1 ?v2))) :named a124)) +(assert (! (forall ((?v0 A_llist_a_llist_bool_fun_fun$) (?v1 A_llist$) (?v2 A_llist$)) (=> (and (fun_app$l (fun_app$m ?v0 ?v1) ?v2) (forall ((?v3 A_llist$) (?v4 A_llist$)) (=> (fun_app$l (fun_app$m ?v0 ?v3) ?v4) (and (= (fun_app$l lnull$ ?v3) (fun_app$l lnull$ ?v4)) (=> (and (not (fun_app$l lnull$ ?v3)) (not (fun_app$l lnull$ ?v4))) (and (= (lhd$ ?v3) (lhd$ ?v4)) (or (fun_app$l (fun_app$m ?v0 (ltl$ ?v3)) (ltl$ ?v4)) (= (ltl$ ?v3) (ltl$ ?v4))))))))) (= ?v1 ?v2))) :named a125)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_llist_a_llist_a_llist_prod_llist_bool_fun_fun$) (?v1 A_llist_a_llist_prod_llist$) (?v2 A_llist_a_llist_prod_llist$)) (=> (and (fun_app$bw (fun_app$by ?v0 ?v1) ?v2) (forall ((?v3 A_llist_a_llist_prod_llist$) (?v4 A_llist_a_llist_prod_llist$)) (=> (fun_app$bw (fun_app$by ?v0 ?v3) ?v4) (and (= (fun_app$bw lnull$a ?v3) (fun_app$bw lnull$a ?v4)) (=> (and (not (fun_app$bw lnull$a ?v3)) (not (fun_app$bw lnull$a ?v4))) (and (= (lhd$a ?v3) (lhd$a ?v4)) (fun_app$bw (fun_app$by ?v0 (ltl$a ?v3)) (ltl$a ?v4)))))))) (= ?v1 ?v2))) :named a126)) +(assert (! (forall ((?v0 A_llist_a_llist_bool_fun_fun$) (?v1 A_llist$) (?v2 A_llist$)) (=> (and (fun_app$l (fun_app$m ?v0 ?v1) ?v2) (forall ((?v3 A_llist$) (?v4 A_llist$)) (=> (fun_app$l (fun_app$m ?v0 ?v3) ?v4) (and (= (fun_app$l lnull$ ?v3) (fun_app$l lnull$ ?v4)) (=> (and (not (fun_app$l lnull$ ?v3)) (not (fun_app$l lnull$ ?v4))) (and (= (lhd$ ?v3) (lhd$ ?v4)) (fun_app$l (fun_app$m ?v0 (ltl$ ?v3)) (ltl$ ?v4)))))))) (= ?v1 ?v2))) :named a127)) +(assert (! (forall ((?v0 A$) (?v1 A_llist$)) (not (= lNil$ (lCons$ ?v0 ?v1)))) :named a128)) +(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod_llist$)) (not (= lNil$a (lCons$a ?v0 ?v1)))) :named a129)) +(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod_llist$)) (not (fun_app$bw lnull$a (lCons$a ?v0 ?v1)))) :named a130)) +(assert (! (forall ((?v0 A$) (?v1 A_llist$)) (not (fun_app$l lnull$ (lCons$ ?v0 ?v1)))) :named a131)) +(assert (! (fun_app$bw lnull$a lNil$a) :named a132)) +(assert (! (fun_app$l lnull$ lNil$) :named a133)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$)) (=> (forall ((?v2 A_llist_a_llist_prod$) (?v3 A_llist_a_llist_prod$)) (=> (= ?v0 (pair$b ?v2 ?v3)) (fun_app$h (fun_app$r ?v1 ?v2) ?v3))) (fun_app$j (fun_app$al uncurry$d ?v1) ?v0))) :named a134)) +(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_bool_fun_fun$)) (=> (forall ((?v2 A_llist$) (?v3 A_llist$)) (=> (= ?v0 (pair$ ?v2 ?v3)) (fun_app$l (fun_app$m ?v1 ?v2) ?v3))) (fun_app$h (fun_app$ad uncurry$a ?v1) ?v0))) :named a135)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) (?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_prod$)) (=> (fun_app$h (fun_app$r ?v0 ?v1) ?v2) (fun_app$j (fun_app$al uncurry$d ?v0) (pair$b ?v1 ?v2)))) :named a136)) +(assert (! (forall ((?v0 A_llist_a_llist_bool_fun_fun$) (?v1 A_llist$) (?v2 A_llist$)) (=> (fun_app$l (fun_app$m ?v0 ?v1) ?v2) (fun_app$h (fun_app$ad uncurry$a ?v0) (pair$ ?v1 ?v2)))) :named a137)) +(assert (! (forall ((?v0 A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$) (?v1 A_llist$) (?v2 A_llist$)) (! (= (fun_app$x (fun_app$ah uncurry$b ?v0) (pair$ ?v1 ?v2)) (fun_app$n (fun_app$o ?v0 ?v1) ?v2)) :pattern ((fun_app$x (fun_app$ah uncurry$b ?v0) (pair$ ?v1 ?v2))))) :named a138)) +(assert (! (forall ((?v0 A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) (?v1 A_llist$) (?v2 A_llist$)) (! (= (fun_app$w (fun_app$ab uncurry$ ?v0) (pair$ ?v1 ?v2)) (fun_app$d (fun_app$e ?v0 ?v1) ?v2)) :pattern ((fun_app$w (fun_app$ab uncurry$ ?v0) (pair$ ?v1 ?v2))))) :named a139)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) (?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_prod$)) (! (= (fun_app$j (fun_app$al uncurry$d ?v0) (pair$b ?v1 ?v2)) (fun_app$h (fun_app$r ?v0 ?v1) ?v2)) :pattern ((fun_app$j (fun_app$al uncurry$d ?v0) (pair$b ?v1 ?v2))))) :named a140)) +(assert (! (forall ((?v0 A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$) (?v1 A_llist$) (?v2 A_llist$)) (! (= (fun_app$r (fun_app$aj uncurry$c ?v0) (pair$ ?v1 ?v2)) (fun_app$p (fun_app$q ?v0 ?v1) ?v2)) :pattern ((fun_app$r (fun_app$aj uncurry$c ?v0) (pair$ ?v1 ?v2))))) :named a141)) +(assert (! (forall ((?v0 A_llist_a_llist_bool_fun_fun$) (?v1 A_llist$) (?v2 A_llist$)) (! (= (fun_app$h (fun_app$ad uncurry$a ?v0) (pair$ ?v1 ?v2)) (fun_app$l (fun_app$m ?v0 ?v1) ?v2)) :pattern ((fun_app$h (fun_app$ad uncurry$a ?v0) (pair$ ?v1 ?v2))))) :named a142)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) (?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_prod$)) (=> (fun_app$h (fun_app$r ?v0 ?v1) ?v2) (fun_app$j (fun_app$al uncurry$d ?v0) (pair$b ?v1 ?v2)))) :named a143)) +(assert (! (forall ((?v0 A_llist_a_llist_bool_fun_fun$) (?v1 A_llist$) (?v2 A_llist$)) (=> (fun_app$l (fun_app$m ?v0 ?v1) ?v2) (fun_app$h (fun_app$ad uncurry$a ?v0) (pair$ ?v1 ?v2)))) :named a144)) +(assert (! (forall ((?v0 Bool) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) (?v2 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$)) (= (fun_app$j (fun_app$al uncurry$d (fun_app$aq (uu$ ?v0) ?v1)) ?v2) (and ?v0 (fun_app$j (fun_app$al uncurry$d ?v1) ?v2)))) :named a145)) +(assert (! (forall ((?v0 Bool) (?v1 A_llist_a_llist_bool_fun_fun$) (?v2 A_llist_a_llist_prod$)) (= (fun_app$h (fun_app$ad uncurry$a (fun_app$ap (uua$ ?v0) ?v1)) ?v2) (and ?v0 (fun_app$h (fun_app$ad uncurry$a ?v1) ?v2)))) :named a146)) +(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_prod$) (?v3 A_llist_a_llist_prod$)) (= (= (pair$b ?v0 ?v1) (pair$b ?v2 ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3)))) :named a147)) +(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$) (?v2 A_llist$) (?v3 A_llist$)) (= (= (pair$ ?v0 ?v1) (pair$ ?v2 ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3)))) :named a148)) +(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_prod$) (?v3 A_llist_a_llist_prod$)) (= (= (pair$b ?v0 ?v1) (pair$b ?v2 ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3)))) :named a149)) +(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$) (?v2 A_llist$) (?v3 A_llist$)) (= (= (pair$ ?v0 ?v1) (pair$ ?v2 ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3)))) :named a150)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) (?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_prod$)) (=> (fun_app$j (fun_app$al uncurry$d ?v0) (pair$b ?v1 ?v2)) (fun_app$h (fun_app$r ?v0 ?v1) ?v2))) :named a151)) +(assert (! (forall ((?v0 A_llist_a_llist_bool_fun_fun$) (?v1 A_llist$) (?v2 A_llist$)) (=> (fun_app$h (fun_app$ad uncurry$a ?v0) (pair$ ?v1 ?v2)) (fun_app$l (fun_app$m ?v0 ?v1) ?v2))) :named a152)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$)) (=> (and (fun_app$j (fun_app$al uncurry$d ?v0) ?v1) (forall ((?v2 A_llist_a_llist_prod$) (?v3 A_llist_a_llist_prod$)) (=> (and (= ?v1 (pair$b ?v2 ?v3)) (fun_app$h (fun_app$r ?v0 ?v2) ?v3)) false))) false)) :named a153)) +(assert (! (forall ((?v0 A_llist_a_llist_bool_fun_fun$) (?v1 A_llist_a_llist_prod$)) (=> (and (fun_app$h (fun_app$ad uncurry$a ?v0) ?v1) (forall ((?v2 A_llist$) (?v3 A_llist$)) (=> (and (= ?v1 (pair$ ?v2 ?v3)) (fun_app$l (fun_app$m ?v0 ?v2) ?v3)) false))) false)) :named a154)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_set_fun$)) (= (fun_app$ah uncurry$b (uub$ ?v0)) ?v0)) :named a155)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_fun$)) (= (fun_app$ab uncurry$ (uuc$ ?v0)) ?v0)) :named a156)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_prod_bool_fun$)) (= (fun_app$al uncurry$d (uud$ ?v0)) ?v0)) :named a157)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$)) (= (fun_app$aj uncurry$c (uue$ ?v0)) ?v0)) :named a158)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_bool_fun$)) (= (fun_app$ad uncurry$a (uuf$ ?v0)) ?v0)) :named a159)) +(assert (! (forall ((?v0 A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_set_fun$)) (=> (forall ((?v2 A_llist$) (?v3 A_llist$)) (= (fun_app$n (fun_app$o ?v0 ?v2) ?v3) (fun_app$x ?v1 (pair$ ?v2 ?v3)))) (= (fun_app$ah uncurry$b ?v0) ?v1))) :named a160)) +(assert (! (forall ((?v0 A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_fun$)) (=> (forall ((?v2 A_llist$) (?v3 A_llist$)) (= (fun_app$d (fun_app$e ?v0 ?v2) ?v3) (fun_app$w ?v1 (pair$ ?v2 ?v3)))) (= (fun_app$ab uncurry$ ?v0) ?v1))) :named a161)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_prod_bool_fun$)) (=> (forall ((?v2 A_llist_a_llist_prod$) (?v3 A_llist_a_llist_prod$)) (= (fun_app$h (fun_app$r ?v0 ?v2) ?v3) (fun_app$j ?v1 (pair$b ?v2 ?v3)))) (= (fun_app$al uncurry$d ?v0) ?v1))) :named a162)) +(assert (! (forall ((?v0 A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$)) (=> (forall ((?v2 A_llist$) (?v3 A_llist$)) (= (fun_app$p (fun_app$q ?v0 ?v2) ?v3) (fun_app$r ?v1 (pair$ ?v2 ?v3)))) (= (fun_app$aj uncurry$c ?v0) ?v1))) :named a163)) +(assert (! (forall ((?v0 A_llist_a_llist_bool_fun_fun$) (?v1 A_llist_a_llist_prod_bool_fun$)) (=> (forall ((?v2 A_llist$) (?v3 A_llist$)) (= (fun_app$l (fun_app$m ?v0 ?v2) ?v3) (fun_app$h ?v1 (pair$ ?v2 ?v3)))) (= (fun_app$ad uncurry$a ?v0) ?v1))) :named a164)) +(assert (! (forall ((?v0 A$) (?v1 A_llist_a_llist_a_set_fun_fun$) (?v2 A_llist$) (?v3 A_llist$)) (=> (member$b ?v0 (fun_app$bz (fun_app$ca ?v1 ?v2) ?v3)) (member$b ?v0 (uncurry$e ?v1 (pair$ ?v2 ?v3))))) :named a165)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_set_fun_fun$) (?v2 A_llist$) (?v3 A_llist$)) (=> (member$a ?v0 (fun_app$cb (fun_app$cc ?v1 ?v2) ?v3)) (member$a ?v0 (uncurry$f ?v1 (pair$ ?v2 ?v3))))) :named a166)) +(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_set_fun_fun$) (?v2 A_llist_a_llist_prod$) (?v3 A_llist_a_llist_prod$)) (=> (fun_app$i (member$ ?v0) (fun_app$x (fun_app$cd ?v1 ?v2) ?v3)) (fun_app$i (member$ ?v0) (uncurry$g ?v1 (pair$b ?v2 ?v3))))) :named a167)) +(assert (! (forall ((?v0 A$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_a_set_fun_fun$) (?v2 A_llist_a_llist_prod$) (?v3 A_llist_a_llist_prod$)) (=> (member$b ?v0 (fun_app$ce (fun_app$cf ?v1 ?v2) ?v3)) (member$b ?v0 (uncurry$h ?v1 (pair$b ?v2 ?v3))))) :named a168)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_set_fun_fun$) (?v2 A_llist_a_llist_prod$) (?v3 A_llist_a_llist_prod$)) (=> (member$a ?v0 (fun_app$cg (fun_app$ch ?v1 ?v2) ?v3)) (member$a ?v0 (uncurry$i ?v1 (pair$b ?v2 ?v3))))) :named a169)) +(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$) (?v2 A_llist$) (?v3 A_llist$)) (=> (fun_app$i (member$ ?v0) (fun_app$n (fun_app$o ?v1 ?v2) ?v3)) (fun_app$i (member$ ?v0) (fun_app$x (fun_app$ah uncurry$b ?v1) (pair$ ?v2 ?v3))))) :named a170)) +(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A$) (?v2 A_llist_a_llist_a_set_fun_fun$)) (=> (forall ((?v3 A_llist$) (?v4 A_llist$)) (=> (= ?v0 (pair$ ?v3 ?v4)) (member$b ?v1 (fun_app$bz (fun_app$ca ?v2 ?v3) ?v4)))) (member$b ?v1 (uncurry$e ?v2 ?v0)))) :named a171)) +(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$) (?v2 A_llist_a_llist_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_set_fun_fun$)) (=> (forall ((?v3 A_llist$) (?v4 A_llist$)) (=> (= ?v0 (pair$ ?v3 ?v4)) (member$a ?v1 (fun_app$cb (fun_app$cc ?v2 ?v3) ?v4)))) (member$a ?v1 (uncurry$f ?v2 ?v0)))) :named a172)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$) (?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_set_fun_fun$)) (=> (forall ((?v3 A_llist_a_llist_prod$) (?v4 A_llist_a_llist_prod$)) (=> (= ?v0 (pair$b ?v3 ?v4)) (fun_app$i (member$ ?v1) (fun_app$x (fun_app$cd ?v2 ?v3) ?v4)))) (fun_app$i (member$ ?v1) (uncurry$g ?v2 ?v0)))) :named a173)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$) (?v1 A$) (?v2 A_llist_a_llist_prod_a_llist_a_llist_prod_a_set_fun_fun$)) (=> (forall ((?v3 A_llist_a_llist_prod$) (?v4 A_llist_a_llist_prod$)) (=> (= ?v0 (pair$b ?v3 ?v4)) (member$b ?v1 (fun_app$ce (fun_app$cf ?v2 ?v3) ?v4)))) (member$b ?v1 (uncurry$h ?v2 ?v0)))) :named a174)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$) (?v2 A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_set_fun_fun$)) (=> (forall ((?v3 A_llist_a_llist_prod$) (?v4 A_llist_a_llist_prod$)) (=> (= ?v0 (pair$b ?v3 ?v4)) (member$a ?v1 (fun_app$cg (fun_app$ch ?v2 ?v3) ?v4)))) (member$a ?v1 (uncurry$i ?v2 ?v0)))) :named a175)) +(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$)) (=> (forall ((?v3 A_llist$) (?v4 A_llist$)) (=> (= ?v0 (pair$ ?v3 ?v4)) (fun_app$i (member$ ?v1) (fun_app$n (fun_app$o ?v2 ?v3) ?v4)))) (fun_app$i (member$ ?v1) (fun_app$x (fun_app$ah uncurry$b ?v2) ?v0)))) :named a176)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_prod_bool_fun$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_prod_bool_fun$)) (=> (forall ((?v2 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$)) (= (fun_app$j ?v0 ?v2) (fun_app$j ?v1 ?v2))) (= (collect$a ?v0) (collect$a ?v1)))) :named a177)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_bool_fun$) (?v1 A_llist_a_llist_prod_bool_fun$)) (=> (forall ((?v2 A_llist_a_llist_prod$)) (= (fun_app$h ?v0 ?v2) (fun_app$h ?v1 ?v2))) (= (collect$ ?v0) (collect$ ?v1)))) :named a178)) +(assert (! (forall ((?v0 A_set$)) (= (collect$b (uug$ ?v0)) ?v0)) :named a179)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_prod_set$)) (= (collect$a (uuh$ ?v0)) ?v0)) :named a180)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_set$)) (= (collect$ (uui$ ?v0)) ?v0)) :named a181)) +(assert (! (forall ((?v0 A$) (?v1 A_bool_fun$)) (= (member$b ?v0 (collect$b ?v1)) (fun_app$k ?v1 ?v0))) :named a182)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_prod_bool_fun$)) (= (member$a ?v0 (collect$a ?v1)) (fun_app$j ?v1 ?v0))) :named a183)) +(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod_bool_fun$)) (= (fun_app$i (member$ ?v0) (collect$ ?v1)) (fun_app$h ?v1 ?v0))) :named a184)) +(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$) (?v2 A_llist_a_llist_prod$)) (=> (forall ((?v3 A_llist$) (?v4 A_llist$)) (=> (= (pair$ ?v3 ?v4) ?v0) (fun_app$h (fun_app$p (fun_app$q ?v1 ?v3) ?v4) ?v2))) (fun_app$h (fun_app$r (fun_app$aj uncurry$c ?v1) ?v0) ?v2))) :named a185)) +(assert (! (forall ((?v0 A$) (?v1 A_llist_a_llist_a_set_fun_fun$) (?v2 A_llist_a_llist_prod$)) (=> (and (member$b ?v0 (uncurry$e ?v1 ?v2)) (forall ((?v3 A_llist$) (?v4 A_llist$)) (=> (and (= ?v2 (pair$ ?v3 ?v4)) (member$b ?v0 (fun_app$bz (fun_app$ca ?v1 ?v3) ?v4))) false))) false)) :named a186)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_set_fun_fun$) (?v2 A_llist_a_llist_prod$)) (=> (and (member$a ?v0 (uncurry$f ?v1 ?v2)) (forall ((?v3 A_llist$) (?v4 A_llist$)) (=> (and (= ?v2 (pair$ ?v3 ?v4)) (member$a ?v0 (fun_app$cb (fun_app$cc ?v1 ?v3) ?v4))) false))) false)) :named a187)) +(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_set_fun_fun$) (?v2 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$)) (=> (and (fun_app$i (member$ ?v0) (uncurry$g ?v1 ?v2)) (forall ((?v3 A_llist_a_llist_prod$) (?v4 A_llist_a_llist_prod$)) (=> (and (= ?v2 (pair$b ?v3 ?v4)) (fun_app$i (member$ ?v0) (fun_app$x (fun_app$cd ?v1 ?v3) ?v4))) false))) false)) :named a188)) +(assert (! (forall ((?v0 A$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_a_set_fun_fun$) (?v2 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$)) (=> (and (member$b ?v0 (uncurry$h ?v1 ?v2)) (forall ((?v3 A_llist_a_llist_prod$) (?v4 A_llist_a_llist_prod$)) (=> (and (= ?v2 (pair$b ?v3 ?v4)) (member$b ?v0 (fun_app$ce (fun_app$cf ?v1 ?v3) ?v4))) false))) false)) :named a189)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_set_fun_fun$) (?v2 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$)) (=> (and (member$a ?v0 (uncurry$i ?v1 ?v2)) (forall ((?v3 A_llist_a_llist_prod$) (?v4 A_llist_a_llist_prod$)) (=> (and (= ?v2 (pair$b ?v3 ?v4)) (member$a ?v0 (fun_app$cg (fun_app$ch ?v1 ?v3) ?v4))) false))) false)) :named a190)) +(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$) (?v2 A_llist_a_llist_prod$)) (=> (and (fun_app$i (member$ ?v0) (fun_app$x (fun_app$ah uncurry$b ?v1) ?v2)) (forall ((?v3 A_llist$) (?v4 A_llist$)) (=> (and (= ?v2 (pair$ ?v3 ?v4)) (fun_app$i (member$ ?v0) (fun_app$n (fun_app$o ?v1 ?v3) ?v4))) false))) false)) :named a191)) +(assert (! (forall ((?v0 A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$) (?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_prod$)) (=> (and (fun_app$h (fun_app$r (fun_app$aj uncurry$c ?v0) ?v1) ?v2) (forall ((?v3 A_llist$) (?v4 A_llist$)) (=> (and (= ?v1 (pair$ ?v3 ?v4)) (fun_app$h (fun_app$p (fun_app$q ?v0 ?v3) ?v4) ?v2)) false))) false)) :named a192)) +(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$) (?v2 A_llist_a_llist_prod$)) (=> (forall ((?v3 A_llist$) (?v4 A_llist$)) (=> (= (pair$ ?v3 ?v4) ?v0) (fun_app$h (fun_app$p (fun_app$q ?v1 ?v3) ?v4) ?v2))) (fun_app$h (fun_app$r (fun_app$aj uncurry$c ?v1) ?v0) ?v2))) :named a193)) +(assert (! (forall ((?v0 A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$) (?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_prod$)) (=> (and (fun_app$h (fun_app$r (fun_app$aj uncurry$c ?v0) ?v1) ?v2) (forall ((?v3 A_llist$) (?v4 A_llist$)) (=> (and (= ?v1 (pair$ ?v3 ?v4)) (fun_app$h (fun_app$p (fun_app$q ?v0 ?v3) ?v4) ?v2)) false))) false)) :named a194)) +(assert (! (forall ((?v0 A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$) (?v1 A_llist$) (?v2 A_llist$) (?v3 A_llist_a_llist_prod$)) (=> (fun_app$h (fun_app$r (fun_app$aj uncurry$c ?v0) (pair$ ?v1 ?v2)) ?v3) (fun_app$h (fun_app$p (fun_app$q ?v0 ?v1) ?v2) ?v3))) :named a195)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$)) (exists ((?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_prod$)) (= ?v0 (pair$b ?v1 ?v2)))) :named a196)) +(assert (! (forall ((?v0 A_llist_a_llist_prod$)) (exists ((?v1 A_llist$) (?v2 A_llist$)) (= ?v0 (pair$ ?v1 ?v2)))) :named a197)) +(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_prod$) (?v3 A_llist_a_llist_prod$)) (=> (and (= (pair$b ?v0 ?v1) (pair$b ?v2 ?v3)) (=> (and (= ?v0 ?v2) (= ?v1 ?v3)) false)) false)) :named a198)) +(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$) (?v2 A_llist$) (?v3 A_llist$)) (=> (and (= (pair$ ?v0 ?v1) (pair$ ?v2 ?v3)) (=> (and (= ?v0 ?v2) (= ?v1 ?v3)) false)) false)) :named a199)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_prod_bool_fun$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$)) (=> (forall ((?v2 A_llist_a_llist_prod$) (?v3 A_llist_a_llist_prod$)) (fun_app$j ?v0 (pair$b ?v2 ?v3))) (fun_app$j ?v0 ?v1))) :named a200)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_bool_fun$) (?v1 A_llist_a_llist_prod$)) (=> (forall ((?v2 A_llist$) (?v3 A_llist$)) (fun_app$h ?v0 (pair$ ?v2 ?v3))) (fun_app$h ?v0 ?v1))) :named a201)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$)) (=> (forall ((?v1 A_llist_a_llist_prod$) (?v2 A_llist$) (?v3 A_llist$)) (=> (= ?v0 (pair$b ?v1 (pair$ ?v2 ?v3))) false)) false)) :named a202)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_prod_bool_fun$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$)) (=> (forall ((?v2 A_llist_a_llist_prod$) (?v3 A_llist$) (?v4 A_llist$)) (fun_app$j ?v0 (pair$b ?v2 (pair$ ?v3 ?v4)))) (fun_app$j ?v0 ?v1))) :named a203)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$)) (=> (forall ((?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_prod$)) (=> (= ?v0 (pair$b ?v1 ?v2)) false)) false)) :named a204)) +(assert (! (forall ((?v0 A_llist_a_llist_prod$)) (=> (forall ((?v1 A_llist$) (?v2 A_llist$)) (=> (= ?v0 (pair$ ?v1 ?v2)) false)) false)) :named a205)) +(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$)) (=> (= ?v0 ?v1) (= (fun_app$x (fun_app$ah uncurry$b ?v2) ?v0) (fun_app$x (fun_app$ah uncurry$b ?v2) ?v1)))) :named a206)) +(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_a_llist_a_llist_prod_fun_fun$)) (=> (= ?v0 ?v1) (= (fun_app$w (fun_app$ab uncurry$ ?v2) ?v0) (fun_app$w (fun_app$ab uncurry$ ?v2) ?v1)))) :named a207)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$) (?v2 A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$)) (=> (= ?v0 ?v1) (= (fun_app$j (fun_app$al uncurry$d ?v2) ?v0) (fun_app$j (fun_app$al uncurry$d ?v2) ?v1)))) :named a208)) +(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$)) (=> (= ?v0 ?v1) (= (fun_app$r (fun_app$aj uncurry$c ?v2) ?v0) (fun_app$r (fun_app$aj uncurry$c ?v2) ?v1)))) :named a209)) +(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_bool_fun_fun$)) (=> (= ?v0 ?v1) (= (fun_app$h (fun_app$ad uncurry$a ?v2) ?v0) (fun_app$h (fun_app$ad uncurry$a ?v2) ?v1)))) :named a210)) +(assert (! (forall ((?v0 Bool_bool_fun$) (?v1 A_llist_a_llist_bool_fun_fun$) (?v2 A_llist_a_llist_prod$)) (= (fun_app$az ?v0 (fun_app$h (fun_app$ad uncurry$a ?v1) ?v2)) (fun_app$h (fun_app$ad uncurry$a (fun_app$ap (uuj$ ?v0) ?v1)) ?v2))) :named a211)) +(assert (! (forall ((?v0 Bool_a_llist_a_llist_prod_fun$) (?v1 A_llist_a_llist_bool_fun_fun$) (?v2 A_llist_a_llist_prod$)) (= (fun_app$ay ?v0 (fun_app$h (fun_app$ad uncurry$a ?v1) ?v2)) (fun_app$w (fun_app$ab uncurry$ (uuk$ ?v0 ?v1)) ?v2))) :named a212)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_bool_fun$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) (?v2 A_llist_a_llist_prod$)) (= (fun_app$h ?v0 (fun_app$w (fun_app$ab uncurry$ ?v1) ?v2)) (fun_app$h (fun_app$ad uncurry$a (fun_app$ac (uul$ ?v0) ?v1)) ?v2))) :named a213)) +(assert (! (forall ((?v0 Bool_a_llist_a_llist_prod_set_fun$) (?v1 A_llist_a_llist_bool_fun_fun$) (?v2 A_llist_a_llist_prod$)) (= (fun_app$bc ?v0 (fun_app$h (fun_app$ad uncurry$a ?v1) ?v2)) (fun_app$x (fun_app$ah uncurry$b (fun_app$bb (uum$ ?v0) ?v1)) ?v2))) :named a214)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_set_bool_fun$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$) (?v2 A_llist_a_llist_prod$)) (= (fun_app$i ?v0 (fun_app$x (fun_app$ah uncurry$b ?v1) ?v2)) (fun_app$h (fun_app$ad uncurry$a (fun_app$bi (uun$ ?v0) ?v1)) ?v2))) :named a215)) +(assert (! (forall ((?v0 Bool_a_llist_a_llist_prod_bool_fun_fun$) (?v1 A_llist_a_llist_bool_fun_fun$) (?v2 A_llist_a_llist_prod$)) (= (fun_app$be ?v0 (fun_app$h (fun_app$ad uncurry$a ?v1) ?v2)) (fun_app$r (fun_app$aj uncurry$c (fun_app$bd (uuo$ ?v0) ?v1)) ?v2))) :named a216)) +(assert (! (forall ((?v0 Bool_bool_fun$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) (?v2 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$)) (= (fun_app$az ?v0 (fun_app$j (fun_app$al uncurry$d ?v1) ?v2)) (fun_app$j (fun_app$al uncurry$d (fun_app$aq (uup$ ?v0) ?v1)) ?v2))) :named a217)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_bool_fun_bool_fun$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$) (?v2 A_llist_a_llist_prod$)) (= (fun_app$bk ?v0 (fun_app$r (fun_app$aj uncurry$c ?v1) ?v2)) (fun_app$h (fun_app$ad uncurry$a (fun_app$bj (uuq$ ?v0) ?v1)) ?v2))) :named a218)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_fun$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) (?v2 A_llist_a_llist_prod$)) (= (fun_app$w ?v0 (fun_app$w (fun_app$ab uncurry$ ?v1) ?v2)) (fun_app$w (fun_app$ab uncurry$ (uur$ ?v0 ?v1)) ?v2))) :named a219)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_set_a_llist_a_llist_prod_fun$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$) (?v2 A_llist_a_llist_prod$)) (= (fun_app$bh ?v0 (fun_app$x (fun_app$ah uncurry$b ?v1) ?v2)) (fun_app$w (fun_app$ab uncurry$ (uus$ ?v0 ?v1)) ?v2))) :named a220)) +(assert (! (forall ((?v0 Bool_bool_fun$) (?v1 A_llist_a_llist_bool_fun_fun$) (?v2 A_llist_a_llist_prod$)) (= (fun_app$az ?v0 (fun_app$h (fun_app$ad uncurry$a ?v1) ?v2)) (fun_app$h (fun_app$ad uncurry$a (fun_app$ap (uuj$ ?v0) ?v1)) ?v2))) :named a221)) +(assert (! (forall ((?v0 Bool_a_llist_a_llist_prod_fun$) (?v1 A_llist_a_llist_bool_fun_fun$) (?v2 A_llist_a_llist_prod$)) (= (fun_app$ay ?v0 (fun_app$h (fun_app$ad uncurry$a ?v1) ?v2)) (fun_app$w (fun_app$ab uncurry$ (uuk$ ?v0 ?v1)) ?v2))) :named a222)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_bool_fun$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) (?v2 A_llist_a_llist_prod$)) (= (fun_app$h ?v0 (fun_app$w (fun_app$ab uncurry$ ?v1) ?v2)) (fun_app$h (fun_app$ad uncurry$a (fun_app$ac (uul$ ?v0) ?v1)) ?v2))) :named a223)) +(assert (! (forall ((?v0 Bool_a_llist_a_llist_prod_set_fun$) (?v1 A_llist_a_llist_bool_fun_fun$) (?v2 A_llist_a_llist_prod$)) (= (fun_app$bc ?v0 (fun_app$h (fun_app$ad uncurry$a ?v1) ?v2)) (fun_app$x (fun_app$ah uncurry$b (fun_app$bb (uum$ ?v0) ?v1)) ?v2))) :named a224)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_set_bool_fun$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$) (?v2 A_llist_a_llist_prod$)) (= (fun_app$i ?v0 (fun_app$x (fun_app$ah uncurry$b ?v1) ?v2)) (fun_app$h (fun_app$ad uncurry$a (fun_app$bi (uun$ ?v0) ?v1)) ?v2))) :named a225)) +(assert (! (forall ((?v0 Bool_a_llist_a_llist_prod_bool_fun_fun$) (?v1 A_llist_a_llist_bool_fun_fun$) (?v2 A_llist_a_llist_prod$)) (= (fun_app$be ?v0 (fun_app$h (fun_app$ad uncurry$a ?v1) ?v2)) (fun_app$r (fun_app$aj uncurry$c (fun_app$bd (uuo$ ?v0) ?v1)) ?v2))) :named a226)) +(assert (! (forall ((?v0 Bool_bool_fun$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) (?v2 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$)) (= (fun_app$az ?v0 (fun_app$j (fun_app$al uncurry$d ?v1) ?v2)) (fun_app$j (fun_app$al uncurry$d (fun_app$aq (uup$ ?v0) ?v1)) ?v2))) :named a227)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_bool_fun_bool_fun$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$) (?v2 A_llist_a_llist_prod$)) (= (fun_app$bk ?v0 (fun_app$r (fun_app$aj uncurry$c ?v1) ?v2)) (fun_app$h (fun_app$ad uncurry$a (fun_app$bj (uuq$ ?v0) ?v1)) ?v2))) :named a228)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_fun$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) (?v2 A_llist_a_llist_prod$)) (= (fun_app$w ?v0 (fun_app$w (fun_app$ab uncurry$ ?v1) ?v2)) (fun_app$w (fun_app$ab uncurry$ (uur$ ?v0 ?v1)) ?v2))) :named a229)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_set_a_llist_a_llist_prod_fun$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$) (?v2 A_llist_a_llist_prod$)) (= (fun_app$bh ?v0 (fun_app$x (fun_app$ah uncurry$b ?v1) ?v2)) (fun_app$w (fun_app$ab uncurry$ (uus$ ?v0 ?v1)) ?v2))) :named a230)) +(assert (! (forall ((?v0 A_llist_a_llist_bool_fun_fun$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_fun_fun$) (?v2 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$)) (= (fun_app$h (fun_app$ad uncurry$a ?v0) (uncurry$j ?v1 ?v2)) (fun_app$j (fun_app$al uncurry$d (fun_app$ae (uut$ ?v0) ?v1)) ?v2))) :named a231)) +(assert (! (forall ((?v0 A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) (?v2 A_llist_a_llist_prod$)) (= (fun_app$x (fun_app$ah uncurry$b ?v0) (fun_app$w (fun_app$ab uncurry$ ?v1) ?v2)) (fun_app$x (fun_app$ah uncurry$b (fun_app$ag (uuu$ ?v0) ?v1)) ?v2))) :named a232)) +(assert (! (forall ((?v0 A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) (?v2 A_llist_a_llist_prod$)) (= (fun_app$w (fun_app$ab uncurry$ ?v0) (fun_app$w (fun_app$ab uncurry$ ?v1) ?v2)) (fun_app$w (fun_app$ab uncurry$ (uuv$ ?v0 ?v1)) ?v2))) :named a233)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_fun_fun$) (?v2 A_llist_a_llist_prod$)) (= (fun_app$j (fun_app$al uncurry$d ?v0) (uncurry$k ?v1 ?v2)) (fun_app$h (fun_app$ad uncurry$a (fun_app$ak (uuw$ ?v0) ?v1)) ?v2))) :named a234)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_fun_fun$) (?v2 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$)) (= (fun_app$j (fun_app$al uncurry$d ?v0) (uncurry$l ?v1 ?v2)) (fun_app$j (fun_app$al uncurry$d (fun_app$ao (uux$ ?v0) ?v1)) ?v2))) :named a235)) +(assert (! (forall ((?v0 A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) (?v2 A_llist_a_llist_prod$)) (= (fun_app$r (fun_app$aj uncurry$c ?v0) (fun_app$w (fun_app$ab uncurry$ ?v1) ?v2)) (fun_app$r (fun_app$aj uncurry$c (fun_app$ai (uuy$ ?v0) ?v1)) ?v2))) :named a236)) +(assert (! (forall ((?v0 A_llist_a_llist_bool_fun_fun$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) (?v2 A_llist_a_llist_prod$)) (= (fun_app$h (fun_app$ad uncurry$a ?v0) (fun_app$w (fun_app$ab uncurry$ ?v1) ?v2)) (fun_app$h (fun_app$ad uncurry$a (fun_app$ac (uuz$ ?v0) ?v1)) ?v2))) :named a237)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$)) (= (= ?v0 ?v0) (fun_app$j (fun_app$al uncurry$d uva$) ?v0))) :named a238)) +(assert (! (forall ((?v0 A_llist_a_llist_prod$)) (= (= ?v0 ?v0) (fun_app$h (fun_app$ad uncurry$a uvb$) ?v0))) :named a239)) +(assert (! (forall ((?v0 A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$) (?v1 A_llist$) (?v2 A_llist$)) (! (= (fun_app$x (fun_app$ah uncurry$b ?v0) (pair$ ?v1 ?v2)) (fun_app$n (fun_app$o ?v0 ?v1) ?v2)) :pattern ((fun_app$x (fun_app$ah uncurry$b ?v0) (pair$ ?v1 ?v2))))) :named a240)) +(assert (! (forall ((?v0 A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) (?v1 A_llist$) (?v2 A_llist$)) (! (= (fun_app$w (fun_app$ab uncurry$ ?v0) (pair$ ?v1 ?v2)) (fun_app$d (fun_app$e ?v0 ?v1) ?v2)) :pattern ((fun_app$w (fun_app$ab uncurry$ ?v0) (pair$ ?v1 ?v2))))) :named a241)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) (?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_prod$)) (! (= (fun_app$j (fun_app$al uncurry$d ?v0) (pair$b ?v1 ?v2)) (fun_app$h (fun_app$r ?v0 ?v1) ?v2)) :pattern ((fun_app$j (fun_app$al uncurry$d ?v0) (pair$b ?v1 ?v2))))) :named a242)) +(assert (! (forall ((?v0 A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$) (?v1 A_llist$) (?v2 A_llist$)) (! (= (fun_app$r (fun_app$aj uncurry$c ?v0) (pair$ ?v1 ?v2)) (fun_app$p (fun_app$q ?v0 ?v1) ?v2)) :pattern ((fun_app$r (fun_app$aj uncurry$c ?v0) (pair$ ?v1 ?v2))))) :named a243)) +(assert (! (forall ((?v0 A_llist_a_llist_bool_fun_fun$) (?v1 A_llist$) (?v2 A_llist$)) (! (= (fun_app$h (fun_app$ad uncurry$a ?v0) (pair$ ?v1 ?v2)) (fun_app$l (fun_app$m ?v0 ?v1) ?v2)) :pattern ((fun_app$h (fun_app$ad uncurry$a ?v0) (pair$ ?v1 ?v2))))) :named a244)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$)) (=> (and (fun_app$j (fun_app$al uncurry$d ?v0) ?v1) (forall ((?v2 A_llist_a_llist_prod$) (?v3 A_llist_a_llist_prod$)) (=> (and (= ?v1 (pair$b ?v2 ?v3)) (fun_app$h (fun_app$r ?v0 ?v2) ?v3)) false))) false)) :named a245)) +(assert (! (forall ((?v0 A_llist_a_llist_bool_fun_fun$) (?v1 A_llist_a_llist_prod$)) (=> (and (fun_app$h (fun_app$ad uncurry$a ?v0) ?v1) (forall ((?v2 A_llist$) (?v3 A_llist$)) (=> (and (= ?v1 (pair$ ?v2 ?v3)) (fun_app$l (fun_app$m ?v0 ?v2) ?v3)) false))) false)) :named a246)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$)) (=> (forall ((?v2 A_llist_a_llist_prod$) (?v3 A_llist_a_llist_prod$)) (=> (= ?v0 (pair$b ?v2 ?v3)) (fun_app$h (fun_app$r ?v1 ?v2) ?v3))) (fun_app$j (fun_app$al uncurry$d ?v1) ?v0))) :named a247)) +(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_bool_fun_fun$)) (=> (forall ((?v2 A_llist$) (?v3 A_llist$)) (=> (= ?v0 (pair$ ?v2 ?v3)) (fun_app$l (fun_app$m ?v1 ?v2) ?v3))) (fun_app$h (fun_app$ad uncurry$a ?v1) ?v0))) :named a248)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_set_bool_fun$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$) (?v2 A_llist_a_llist_prod$)) (=> (and (fun_app$i ?v0 (fun_app$x (fun_app$ah uncurry$b ?v1) ?v2)) (forall ((?v3 A_llist$) (?v4 A_llist$)) (=> (and (= ?v2 (pair$ ?v3 ?v4)) (fun_app$i ?v0 (fun_app$n (fun_app$o ?v1 ?v3) ?v4))) false))) false)) :named a249)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_bool_fun$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) (?v2 A_llist_a_llist_prod$)) (=> (and (fun_app$h ?v0 (fun_app$w (fun_app$ab uncurry$ ?v1) ?v2)) (forall ((?v3 A_llist$) (?v4 A_llist$)) (=> (and (= ?v2 (pair$ ?v3 ?v4)) (fun_app$h ?v0 (fun_app$d (fun_app$e ?v1 ?v3) ?v4))) false))) false)) :named a250)) +(assert (! (forall ((?v0 Bool_bool_fun$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) (?v2 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$)) (=> (and (fun_app$az ?v0 (fun_app$j (fun_app$al uncurry$d ?v1) ?v2)) (forall ((?v3 A_llist_a_llist_prod$) (?v4 A_llist_a_llist_prod$)) (=> (and (= ?v2 (pair$b ?v3 ?v4)) (fun_app$az ?v0 (fun_app$h (fun_app$r ?v1 ?v3) ?v4))) false))) false)) :named a251)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_bool_fun_bool_fun$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$) (?v2 A_llist_a_llist_prod$)) (=> (and (fun_app$bk ?v0 (fun_app$r (fun_app$aj uncurry$c ?v1) ?v2)) (forall ((?v3 A_llist$) (?v4 A_llist$)) (=> (and (= ?v2 (pair$ ?v3 ?v4)) (fun_app$bk ?v0 (fun_app$p (fun_app$q ?v1 ?v3) ?v4))) false))) false)) :named a252)) +(assert (! (forall ((?v0 Bool_bool_fun$) (?v1 A_llist_a_llist_bool_fun_fun$) (?v2 A_llist_a_llist_prod$)) (=> (and (fun_app$az ?v0 (fun_app$h (fun_app$ad uncurry$a ?v1) ?v2)) (forall ((?v3 A_llist$) (?v4 A_llist$)) (=> (and (= ?v2 (pair$ ?v3 ?v4)) (fun_app$az ?v0 (fun_app$l (fun_app$m ?v1 ?v3) ?v4))) false))) false)) :named a253)) +(assert (! (forall ((?v0 Bool_bool_fun$) (?v1 Bool) (?v2 A_a_llist_bool_fun_fun$) (?v3 A_llist$)) (= (fun_app$az ?v0 (fun_app$l (fun_app$ci (case_llist$ ?v1) ?v2) ?v3)) (and (=> (= ?v3 lNil$) (fun_app$az ?v0 ?v1)) (=> (= ?v3 (lCons$ (lhd$ ?v3) (ltl$ ?v3))) (fun_app$az ?v0 (fun_app$l (fun_app$as ?v2 (lhd$ ?v3)) (ltl$ ?v3))))))) :named a254)) +(assert (! (forall ((?v0 A_llist_bool_fun$) (?v1 A_llist$) (?v2 A_a_llist_a_llist_fun_fun$) (?v3 A_llist$)) (= (fun_app$l ?v0 (fun_app$a (fun_app$cj (case_llist$a ?v1) ?v2) ?v3)) (and (=> (= ?v3 lNil$) (fun_app$l ?v0 ?v1)) (=> (= ?v3 (lCons$ (lhd$ ?v3) (ltl$ ?v3))) (fun_app$l ?v0 (fun_app$a (fun_app$v ?v2 (lhd$ ?v3)) (ltl$ ?v3))))))) :named a255)) +(assert (! (forall ((?v0 A_bool_fun$) (?v1 A$) (?v2 A_a_llist_a_fun_fun$) (?v3 A_llist$)) (= (fun_app$k ?v0 (fun_app$c (fun_app$ck (case_llist$b ?v1) ?v2) ?v3)) (and (=> (= ?v3 lNil$) (fun_app$k ?v0 ?v1)) (=> (= ?v3 (lCons$ (lhd$ ?v3) (ltl$ ?v3))) (fun_app$k ?v0 (fun_app$c (fun_app$au ?v2 (lhd$ ?v3)) (ltl$ ?v3))))))) :named a256)) +(assert (! (forall ((?v0 Bool_bool_fun$) (?v1 Bool) (?v2 A_a_llist_bool_fun_fun$) (?v3 A_llist$)) (= (fun_app$az ?v0 (fun_app$l (fun_app$ci (case_llist$ ?v1) ?v2) ?v3)) (not (or (and (= ?v3 lNil$) (not (fun_app$az ?v0 ?v1))) (and (= ?v3 (lCons$ (lhd$ ?v3) (ltl$ ?v3))) (not (fun_app$az ?v0 (fun_app$l (fun_app$as ?v2 (lhd$ ?v3)) (ltl$ ?v3))))))))) :named a257)) +(assert (! (forall ((?v0 A_llist_bool_fun$) (?v1 A_llist$) (?v2 A_a_llist_a_llist_fun_fun$) (?v3 A_llist$)) (= (fun_app$l ?v0 (fun_app$a (fun_app$cj (case_llist$a ?v1) ?v2) ?v3)) (not (or (and (= ?v3 lNil$) (not (fun_app$l ?v0 ?v1))) (and (= ?v3 (lCons$ (lhd$ ?v3) (ltl$ ?v3))) (not (fun_app$l ?v0 (fun_app$a (fun_app$v ?v2 (lhd$ ?v3)) (ltl$ ?v3))))))))) :named a258)) +(assert (! (forall ((?v0 A_bool_fun$) (?v1 A$) (?v2 A_a_llist_a_fun_fun$) (?v3 A_llist$)) (= (fun_app$k ?v0 (fun_app$c (fun_app$ck (case_llist$b ?v1) ?v2) ?v3)) (not (or (and (= ?v3 lNil$) (not (fun_app$k ?v0 ?v1))) (and (= ?v3 (lCons$ (lhd$ ?v3) (ltl$ ?v3))) (not (fun_app$k ?v0 (fun_app$c (fun_app$au ?v2 (lhd$ ?v3)) (ltl$ ?v3))))))))) :named a259)) +(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$) (?v2 A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$) (?v3 A_llist_a_llist_prod$)) (=> (and (forall ((?v4 A_llist$) (?v5 A_llist$)) (=> (= (pair$ ?v4 ?v5) ?v0) (= (fun_app$n (fun_app$o ?v1 ?v4) ?v5) (fun_app$n (fun_app$o ?v2 ?v4) ?v5)))) (= ?v3 ?v0)) (= (fun_app$x (fun_app$ah uncurry$b ?v1) ?v3) (fun_app$x (fun_app$ah uncurry$b ?v2) ?v0)))) :named a260)) +(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) (?v2 A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) (?v3 A_llist_a_llist_prod$)) (=> (and (forall ((?v4 A_llist$) (?v5 A_llist$)) (=> (= (pair$ ?v4 ?v5) ?v0) (= (fun_app$d (fun_app$e ?v1 ?v4) ?v5) (fun_app$d (fun_app$e ?v2 ?v4) ?v5)))) (= ?v3 ?v0)) (= (fun_app$w (fun_app$ab uncurry$ ?v1) ?v3) (fun_app$w (fun_app$ab uncurry$ ?v2) ?v0)))) :named a261)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) (?v2 A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) (?v3 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$)) (=> (and (forall ((?v4 A_llist_a_llist_prod$) (?v5 A_llist_a_llist_prod$)) (=> (= (pair$b ?v4 ?v5) ?v0) (= (fun_app$h (fun_app$r ?v1 ?v4) ?v5) (fun_app$h (fun_app$r ?v2 ?v4) ?v5)))) (= ?v3 ?v0)) (= (fun_app$j (fun_app$al uncurry$d ?v1) ?v3) (fun_app$j (fun_app$al uncurry$d ?v2) ?v0)))) :named a262)) +(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$) (?v2 A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$) (?v3 A_llist_a_llist_prod$)) (=> (and (forall ((?v4 A_llist$) (?v5 A_llist$)) (=> (= (pair$ ?v4 ?v5) ?v0) (= (fun_app$p (fun_app$q ?v1 ?v4) ?v5) (fun_app$p (fun_app$q ?v2 ?v4) ?v5)))) (= ?v3 ?v0)) (= (fun_app$r (fun_app$aj uncurry$c ?v1) ?v3) (fun_app$r (fun_app$aj uncurry$c ?v2) ?v0)))) :named a263)) +(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_bool_fun_fun$) (?v2 A_llist_a_llist_bool_fun_fun$) (?v3 A_llist_a_llist_prod$)) (=> (and (forall ((?v4 A_llist$) (?v5 A_llist$)) (=> (= (pair$ ?v4 ?v5) ?v0) (= (fun_app$l (fun_app$m ?v1 ?v4) ?v5) (fun_app$l (fun_app$m ?v2 ?v4) ?v5)))) (= ?v3 ?v0)) (= (fun_app$h (fun_app$ad uncurry$a ?v1) ?v3) (fun_app$h (fun_app$ad uncurry$a ?v2) ?v0)))) :named a264)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$)) (= (unfold_llist$ lnull$a uvc$ uvd$ ?v0) ?v0)) :named a265)) +(assert (! (forall ((?v0 A_llist$)) (= (fun_app$a (fun_app$cl (fun_app$cm (unfold_llist$a lnull$) uve$) uvf$) ?v0) ?v0)) :named a266)) +(assert (! (forall ((?v0 Bool) (?v1 A_a_llist_bool_fun_fun$) (?v2 A_llist$)) (! (= (fun_app$l (fun_app$ci (case_llist$ ?v0) ?v1) ?v2) (ite (fun_app$l lnull$ ?v2) ?v0 (fun_app$l (fun_app$as ?v1 (lhd$ ?v2)) (ltl$ ?v2)))) :pattern ((fun_app$l (fun_app$ci (case_llist$ ?v0) ?v1) ?v2)))) :named a267)) +(assert (! (forall ((?v0 A_llist$) (?v1 A_a_llist_a_llist_fun_fun$) (?v2 A_llist$)) (! (= (fun_app$a (fun_app$cj (case_llist$a ?v0) ?v1) ?v2) (ite (fun_app$l lnull$ ?v2) ?v0 (fun_app$a (fun_app$v ?v1 (lhd$ ?v2)) (ltl$ ?v2)))) :pattern ((fun_app$a (fun_app$cj (case_llist$a ?v0) ?v1) ?v2)))) :named a268)) +(assert (! (forall ((?v0 A$) (?v1 A_a_llist_a_fun_fun$) (?v2 A_llist$)) (! (= (fun_app$c (fun_app$ck (case_llist$b ?v0) ?v1) ?v2) (ite (fun_app$l lnull$ ?v2) ?v0 (fun_app$c (fun_app$au ?v1 (lhd$ ?v2)) (ltl$ ?v2)))) :pattern ((fun_app$c (fun_app$ck (case_llist$b ?v0) ?v1) ?v2)))) :named a269)) +(assert (! (forall ((?v0 A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$) (?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_prod$)) (= (fun_app$h (fun_app$r (fun_app$aj uncurry$c ?v0) ?v1) ?v2) (fun_app$h (fun_app$ad uncurry$a (fun_app$y (uvg$ ?v0) ?v2)) ?v1))) :named a270)) +(assert (! (= internal_split$ uncurry$b) :named a271)) +(assert (! (= internal_split$a uncurry$) :named a272)) +(assert (! (= internal_split$b uncurry$d) :named a273)) +(assert (! (= internal_split$c uncurry$c) :named a274)) +(assert (! (= internal_split$d uncurry$a) :named a275)) +(assert (! (forall ((?v0 A_llist_bool_fun$) (?v1 A_llist_a_fun$) (?v2 A_llist_a_llist_fun$) (?v3 A_llist$)) (= (not (fun_app$l lnull$ (fun_app$a (fun_app$cl (fun_app$cm (unfold_llist$a ?v0) ?v1) ?v2) ?v3))) (not (fun_app$l ?v0 ?v3)))) :named a276)) +(assert (! (forall ((?v0 A_llist_bool_fun$) (?v1 A_llist_a_fun$) (?v2 A_llist_a_llist_fun$) (?v3 A_llist$)) (= (fun_app$l lnull$ (fun_app$a (fun_app$cl (fun_app$cm (unfold_llist$a ?v0) ?v1) ?v2) ?v3)) (fun_app$l ?v0 ?v3))) :named a277)) +(assert (! (forall ((?v0 A_llist_bool_fun$) (?v1 A_llist_a_fun$) (?v2 A_llist_a_llist_fun$) (?v3 A_llist$) (?v4 A$) (?v5 A_llist$)) (= (= (fun_app$a (fun_app$cl (fun_app$cm (unfold_llist$a ?v0) ?v1) ?v2) ?v3) (lCons$ ?v4 ?v5)) (and (not (fun_app$l ?v0 ?v3)) (and (= ?v4 (fun_app$c ?v1 ?v3)) (= ?v5 (fun_app$a (fun_app$cl (fun_app$cm (unfold_llist$a ?v0) ?v1) ?v2) (fun_app$a ?v2 ?v3))))))) :named a278)) +(assert (! (forall ((?v0 Bool_bool_fun$) (?v1 Bool) (?v2 A_a_llist_bool_fun_fun$) (?v3 A_llist$)) (= (fun_app$az ?v0 (fun_app$l (fun_app$ci (case_llist$ ?v1) ?v2) ?v3)) (fun_app$l (fun_app$ci (case_llist$ (fun_app$az ?v0 ?v1)) (fun_app$ba (uvh$ ?v0) ?v2)) ?v3))) :named a279)) +(assert (! (forall ((?v0 Bool_a_llist_fun$) (?v1 Bool) (?v2 A_a_llist_bool_fun_fun$) (?v3 A_llist$)) (= (fun_app$ax ?v0 (fun_app$l (fun_app$ci (case_llist$ ?v1) ?v2) ?v3)) (fun_app$a (fun_app$cj (case_llist$a (fun_app$ax ?v0 ?v1)) (fun_app$aw (uvi$ ?v0) ?v2)) ?v3))) :named a280)) +(assert (! (forall ((?v0 Bool_a_fun$) (?v1 Bool) (?v2 A_a_llist_bool_fun_fun$) (?v3 A_llist$)) (= (fun_app$bg ?v0 (fun_app$l (fun_app$ci (case_llist$ ?v1) ?v2) ?v3)) (fun_app$c (fun_app$ck (case_llist$b (fun_app$bg ?v0 ?v1)) (fun_app$bf (uvj$ ?v0) ?v2)) ?v3))) :named a281)) +(assert (! (forall ((?v0 A_llist_bool_fun$) (?v1 A_llist$) (?v2 A_a_llist_a_llist_fun_fun$) (?v3 A_llist$)) (= (fun_app$l ?v0 (fun_app$a (fun_app$cj (case_llist$a ?v1) ?v2) ?v3)) (fun_app$l (fun_app$ci (case_llist$ (fun_app$l ?v0 ?v1)) (fun_app$at (uvk$ ?v0) ?v2)) ?v3))) :named a282)) +(assert (! (forall ((?v0 A_llist_a_llist_fun$) (?v1 A_llist$) (?v2 A_a_llist_a_llist_fun_fun$) (?v3 A_llist$)) (= (fun_app$a ?v0 (fun_app$a (fun_app$cj (case_llist$a ?v1) ?v2) ?v3)) (fun_app$a (fun_app$cj (case_llist$a (fun_app$a ?v0 ?v1)) (fun_app$ar (uvl$ ?v0) ?v2)) ?v3))) :named a283)) +(assert (! (forall ((?v0 A_llist_a_fun$) (?v1 A_llist$) (?v2 A_a_llist_a_llist_fun_fun$) (?v3 A_llist$)) (= (fun_app$c ?v0 (fun_app$a (fun_app$cj (case_llist$a ?v1) ?v2) ?v3)) (fun_app$c (fun_app$ck (case_llist$b (fun_app$c ?v0 ?v1)) (fun_app$av (uvm$ ?v0) ?v2)) ?v3))) :named a284)) +(assert (! (forall ((?v0 A_bool_fun$) (?v1 A$) (?v2 A_a_llist_a_fun_fun$) (?v3 A_llist$)) (= (fun_app$k ?v0 (fun_app$c (fun_app$ck (case_llist$b ?v1) ?v2) ?v3)) (fun_app$l (fun_app$ci (case_llist$ (fun_app$k ?v0 ?v1)) (fun_app$bn (uvn$ ?v0) ?v2)) ?v3))) :named a285)) +(assert (! (forall ((?v0 A_a_llist_fun$) (?v1 A$) (?v2 A_a_llist_a_fun_fun$) (?v3 A_llist$)) (= (fun_app$bm ?v0 (fun_app$c (fun_app$ck (case_llist$b ?v1) ?v2) ?v3)) (fun_app$a (fun_app$cj (case_llist$a (fun_app$bm ?v0 ?v1)) (fun_app$bl (uvo$ ?v0) ?v2)) ?v3))) :named a286)) +(assert (! (forall ((?v0 A_a_fun$) (?v1 A$) (?v2 A_a_llist_a_fun_fun$) (?v3 A_llist$)) (= (fun_app$bp ?v0 (fun_app$c (fun_app$ck (case_llist$b ?v1) ?v2) ?v3)) (fun_app$c (fun_app$ck (case_llist$b (fun_app$bp ?v0 ?v1)) (fun_app$bo (uvp$ ?v0) ?v2)) ?v3))) :named a287)) +(assert (! (forall ((?v0 A_llist_bool_fun$) (?v1 A_llist$) (?v2 A_llist_a_fun$) (?v3 A_llist_a_llist_fun$)) (=> (not (fun_app$l ?v0 ?v1)) (not (fun_app$l lnull$ (fun_app$a (fun_app$cl (fun_app$cm (unfold_llist$a ?v0) ?v2) ?v3) ?v1))))) :named a288)) +(assert (! (forall ((?v0 A_llist_bool_fun$) (?v1 A_llist$) (?v2 A_llist_a_fun$) (?v3 A_llist_a_llist_fun$)) (=> (fun_app$l ?v0 ?v1) (fun_app$l lnull$ (fun_app$a (fun_app$cl (fun_app$cm (unfold_llist$a ?v0) ?v2) ?v3) ?v1)))) :named a289)) +(assert (! (forall ((?v0 A_llist_bool_fun$) (?v1 A_llist$) (?v2 A_llist_a_fun$) (?v3 A_llist_a_llist_fun$)) (=> (not (fun_app$l ?v0 ?v1)) (= (fun_app$a (fun_app$cl (fun_app$cm (unfold_llist$a ?v0) ?v2) ?v3) ?v1) (lCons$ (fun_app$c ?v2 ?v1) (fun_app$a (fun_app$cl (fun_app$cm (unfold_llist$a ?v0) ?v2) ?v3) (fun_app$a ?v3 ?v1)))))) :named a290)) +(assert (! (forall ((?v0 A_llist_bool_fun$) (?v1 A_llist$) (?v2 A_llist_a_fun$) (?v3 A_llist_a_llist_fun$)) (! (=> (fun_app$l ?v0 ?v1) (= (fun_app$a (fun_app$cl (fun_app$cm (unfold_llist$a ?v0) ?v2) ?v3) ?v1) lNil$)) :pattern ((fun_app$a (fun_app$cl (fun_app$cm (unfold_llist$a ?v0) ?v2) ?v3) ?v1)))) :named a291)) +(assert (! (forall ((?v0 A_llist_bool_fun$) (?v1 A_llist$) (?v2 A_llist_a_fun$) (?v3 A_llist_a_llist_fun$)) (=> (not (fun_app$l ?v0 ?v1)) (= (ltl$ (fun_app$a (fun_app$cl (fun_app$cm (unfold_llist$a ?v0) ?v2) ?v3) ?v1)) (fun_app$a (fun_app$cl (fun_app$cm (unfold_llist$a ?v0) ?v2) ?v3) (fun_app$a ?v3 ?v1))))) :named a292)) +(assert (! (forall ((?v0 A_llist_bool_fun$) (?v1 A_llist$) (?v2 A_llist_a_fun$) (?v3 A_llist_a_llist_fun$)) (=> (not (fun_app$l ?v0 ?v1)) (= (lhd$ (fun_app$a (fun_app$cl (fun_app$cm (unfold_llist$a ?v0) ?v2) ?v3) ?v1)) (fun_app$c ?v2 ?v1)))) :named a293)) +(assert (! (forall ((?v0 Bool) (?v1 A_a_llist_bool_fun_fun$) (?v2 A$) (?v3 A_llist$)) (! (= (fun_app$l (fun_app$ci (case_llist$ ?v0) ?v1) (lCons$ ?v2 ?v3)) (fun_app$l (fun_app$as ?v1 ?v2) ?v3)) :pattern ((fun_app$l (fun_app$ci (case_llist$ ?v0) ?v1) (lCons$ ?v2 ?v3))))) :named a294)) +(assert (! (forall ((?v0 A_llist$) (?v1 A_a_llist_a_llist_fun_fun$) (?v2 A$) (?v3 A_llist$)) (! (= (fun_app$a (fun_app$cj (case_llist$a ?v0) ?v1) (lCons$ ?v2 ?v3)) (fun_app$a (fun_app$v ?v1 ?v2) ?v3)) :pattern ((fun_app$a (fun_app$cj (case_llist$a ?v0) ?v1) (lCons$ ?v2 ?v3))))) :named a295)) +(assert (! (forall ((?v0 A$) (?v1 A_a_llist_a_fun_fun$) (?v2 A$) (?v3 A_llist$)) (! (= (fun_app$c (fun_app$ck (case_llist$b ?v0) ?v1) (lCons$ ?v2 ?v3)) (fun_app$c (fun_app$au ?v1 ?v2) ?v3)) :pattern ((fun_app$c (fun_app$ck (case_llist$b ?v0) ?v1) (lCons$ ?v2 ?v3))))) :named a296)) +(assert (! (forall ((?v0 Bool) (?v1 A_a_llist_bool_fun_fun$)) (! (= (fun_app$l (fun_app$ci (case_llist$ ?v0) ?v1) lNil$) ?v0) :pattern ((fun_app$ci (case_llist$ ?v0) ?v1)))) :named a297)) +(assert (! (forall ((?v0 A_llist$) (?v1 A_a_llist_a_llist_fun_fun$)) (! (= (fun_app$a (fun_app$cj (case_llist$a ?v0) ?v1) lNil$) ?v0) :pattern ((fun_app$cj (case_llist$a ?v0) ?v1)))) :named a298)) +(assert (! (forall ((?v0 A$) (?v1 A_a_llist_a_fun_fun$)) (! (= (fun_app$c (fun_app$ck (case_llist$b ?v0) ?v1) lNil$) ?v0) :pattern ((fun_app$ck (case_llist$b ?v0) ?v1)))) :named a299)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$)) (= (not (fun_app$bw lnull$a ?v0)) (fun_app$bw (fun_app$cn (case_llist$c false) uvq$) ?v0))) :named a300)) +(assert (! (forall ((?v0 A_llist$)) (= (not (fun_app$l lnull$ ?v0)) (fun_app$l (fun_app$ci (case_llist$ false) uvr$) ?v0))) :named a301)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$)) (! (= (fun_app$bw lnull$a ?v0) (fun_app$bw (fun_app$cn (case_llist$c true) uvs$) ?v0)) :pattern ((fun_app$bw lnull$a ?v0)))) :named a302)) +(assert (! (forall ((?v0 A_llist$)) (! (= (fun_app$l lnull$ ?v0) (fun_app$l (fun_app$ci (case_llist$ true) uvt$) ?v0)) :pattern ((fun_app$l lnull$ ?v0)))) :named a303)) +(assert (! (forall ((?v0 A_llist_bool_fun$) (?v1 A_llist_a_fun$) (?v2 A_llist_a_llist_fun$) (?v3 A_llist$)) (= (fun_app$a (fun_app$cl (fun_app$cm (unfold_llist$a ?v0) ?v1) ?v2) ?v3) (ite (fun_app$l ?v0 ?v3) lNil$ (lCons$ (fun_app$c ?v1 ?v3) (fun_app$a (fun_app$cl (fun_app$cm (unfold_llist$a ?v0) ?v1) ?v2) (fun_app$a ?v2 ?v3)))))) :named a304)) +(assert (! (forall ((?v0 A_llist_bool_fun$) (?v1 A_llist_a_fun$) (?v2 A_llist_a_llist_fun$) (?v3 A_llist$)) (= (ltl$ (fun_app$a (fun_app$cl (fun_app$cm (unfold_llist$a ?v0) ?v1) ?v2) ?v3)) (ite (fun_app$l ?v0 ?v3) lNil$ (fun_app$a (fun_app$cl (fun_app$cm (unfold_llist$a ?v0) ?v1) ?v2) (fun_app$a ?v2 ?v3))))) :named a305)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$)) (= (ltl$a ?v0) (case_llist$d lNil$a uvu$ ?v0))) :named a306)) +(assert (! (forall ((?v0 A_llist$)) (= (ltl$ ?v0) (fun_app$a (fun_app$cj (case_llist$a lNil$) uvv$) ?v0))) :named a307)) +(assert (! (forall ((?v0 A_llist_a_llist_bool_fun_fun$) (?v1 A_llist$) (?v2 A_llist$)) (! (= (fun_app$h (fun_app$ad internal_split$d ?v0) (pair$ ?v1 ?v2)) (fun_app$l (fun_app$m ?v0 ?v1) ?v2)) :pattern ((fun_app$h (fun_app$ad internal_split$d ?v0) (pair$ ?v1 ?v2))))) :named a308)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$)) (! (= (uncurry$l uvw$ ?v0) ?v0) :pattern ((uncurry$l uvw$ ?v0)))) :named a309)) +(assert (! (forall ((?v0 A_llist_a_llist_prod$)) (! (= (fun_app$w (fun_app$ab uncurry$ uvx$) ?v0) ?v0) :pattern ((fun_app$w (fun_app$ab uncurry$ uvx$) ?v0)))) :named a310)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_prod_set$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_prod_set$)) (= (= (uvy$ ?v0) (uvy$ ?v1)) (= ?v0 ?v1))) :named a311)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_set$) (?v1 A_llist_a_llist_prod_set$)) (= (= (uvz$ ?v0) (uvz$ ?v1)) (= ?v0 ?v1))) :named a312)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$) (?v1 A_llist_a_llist_prod_llist$)) (=> (or (not (fun_app$bw lnull$a ?v0)) (not (fun_app$bw lnull$a ?v1))) (= (lhd$a (fun_app$ (lappend$ ?v0) ?v1)) (case_llist$e (lhd$a ?v1) uwa$ ?v0)))) :named a313)) +(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$)) (=> (or (not (fun_app$l lnull$ ?v0)) (not (fun_app$l lnull$ ?v1))) (= (lhd$ (fun_app$a (lappend$a ?v0) ?v1)) (fun_app$c (fun_app$ck (case_llist$b (lhd$ ?v1)) uwb$) ?v0)))) :named a314)) +(assert (! (forall ((?v0 A_bool_fun$) (?v1 A$) (?v2 A_llist$)) (! (= (fun_app$l (pred_llist$ ?v0) (lCons$ ?v1 ?v2)) (and (fun_app$k ?v0 ?v1) (fun_app$l (pred_llist$ ?v0) ?v2))) :pattern ((fun_app$l (pred_llist$ ?v0) (lCons$ ?v1 ?v2))))) :named a315)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_bool_fun$) (?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_prod_llist$)) (! (= (fun_app$bw (pred_llist$a ?v0) (lCons$a ?v1 ?v2)) (and (fun_app$h ?v0 ?v1) (fun_app$bw (pred_llist$a ?v0) ?v2))) :pattern ((fun_app$bw (pred_llist$a ?v0) (lCons$a ?v1 ?v2))))) :named a316)) +(assert (! (forall ((?v0 A_llist_a_llist_prod$)) (! (= (fun_app$bw (lmember$ ?v0) lNil$a) false) :pattern ((lmember$ ?v0)))) :named a317)) +(assert (! (forall ((?v0 A$)) (! (= (fun_app$l (lmember$a ?v0) lNil$) false) :pattern ((lmember$a ?v0)))) :named a318)) +(assert (! (forall ((?v0 A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$) (?v1 A_llist_a_llist_prod$)) (= (fun_app$x (fun_app$ah uncurry$b (uwc$ ?v0)) (swap$ ?v1)) (fun_app$x (fun_app$ah uncurry$b ?v0) ?v1))) :named a319)) +(assert (! (forall ((?v0 A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) (?v1 A_llist_a_llist_prod$)) (= (fun_app$w (fun_app$ab uncurry$ (uwd$ ?v0)) (swap$ ?v1)) (fun_app$w (fun_app$ab uncurry$ ?v0) ?v1))) :named a320)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$)) (= (fun_app$j (fun_app$al uncurry$d (uwe$ ?v0)) (swap$a ?v1)) (fun_app$j (fun_app$al uncurry$d ?v0) ?v1))) :named a321)) +(assert (! (forall ((?v0 A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$) (?v1 A_llist_a_llist_prod$)) (= (fun_app$r (fun_app$aj uncurry$c (uwf$ ?v0)) (swap$ ?v1)) (fun_app$r (fun_app$aj uncurry$c ?v0) ?v1))) :named a322)) +(assert (! (forall ((?v0 A_llist_a_llist_bool_fun_fun$) (?v1 A_llist_a_llist_prod$)) (= (fun_app$h (fun_app$ad uncurry$a (uwg$ ?v0)) (swap$ ?v1)) (fun_app$h (fun_app$ad uncurry$a ?v0) ?v1))) :named a323)) +(assert (! (forall ((?v0 A$) (?v1 A$) (?v2 A_llist$)) (! (= (fun_app$l (lmember$a ?v0) (lCons$ ?v1 ?v2)) (or (= ?v0 ?v1) (fun_app$l (lmember$a ?v0) ?v2))) :pattern ((fun_app$l (lmember$a ?v0) (lCons$ ?v1 ?v2))))) :named a324)) +(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_prod_llist$)) (! (= (fun_app$bw (lmember$ ?v0) (lCons$a ?v1 ?v2)) (or (= ?v0 ?v1) (fun_app$bw (lmember$ ?v0) ?v2))) :pattern ((fun_app$bw (lmember$ ?v0) (lCons$a ?v1 ?v2))))) :named a325)) +(assert (! (forall ((?v0 A_llist_a_llist_prod$)) (= (swap$ (swap$ ?v0)) ?v0)) :named a326)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$) (?v1 A_llist_a_llist_prod_llist$)) (= (fun_app$bw lnull$a (fun_app$ (lappend$ ?v0) ?v1)) (and (fun_app$bw lnull$a ?v0) (fun_app$bw lnull$a ?v1)))) :named a327)) +(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$)) (= (fun_app$l lnull$ (fun_app$a (lappend$a ?v0) ?v1)) (and (fun_app$l lnull$ ?v0) (fun_app$l lnull$ ?v1)))) :named a328)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$) (?v1 A_llist_a_llist_prod_llist$)) (= (not (fun_app$bw lnull$a (fun_app$ (lappend$ ?v0) ?v1))) (or (not (fun_app$bw lnull$a ?v0)) (not (fun_app$bw lnull$a ?v1))))) :named a329)) +(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$)) (= (not (fun_app$l lnull$ (fun_app$a (lappend$a ?v0) ?v1))) (or (not (fun_app$l lnull$ ?v0)) (not (fun_app$l lnull$ ?v1))))) :named a330)) +(assert (! (forall ((?v0 A$) (?v1 A_llist$) (?v2 A_llist$)) (! (= (fun_app$a (lappend$a (lCons$ ?v0 ?v1)) ?v2) (lCons$ ?v0 (fun_app$a (lappend$a ?v1) ?v2))) :pattern ((fun_app$a (lappend$a (lCons$ ?v0 ?v1)) ?v2)))) :named a331)) +(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod_llist$) (?v2 A_llist_a_llist_prod_llist$)) (! (= (fun_app$ (lappend$ (lCons$a ?v0 ?v1)) ?v2) (lCons$a ?v0 (fun_app$ (lappend$ ?v1) ?v2))) :pattern ((fun_app$ (lappend$ (lCons$a ?v0 ?v1)) ?v2)))) :named a332)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$)) (! (= (fun_app$ (lappend$ lNil$a) ?v0) ?v0) :pattern ((fun_app$ (lappend$ lNil$a) ?v0)))) :named a333)) +(assert (! (forall ((?v0 A_llist$)) (! (= (fun_app$a (lappend$a lNil$) ?v0) ?v0) :pattern ((fun_app$a (lappend$a lNil$) ?v0)))) :named a334)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$)) (! (= (fun_app$ (lappend$ ?v0) lNil$a) ?v0) :pattern ((lappend$ ?v0)))) :named a335)) +(assert (! (forall ((?v0 A_llist$)) (! (= (fun_app$a (lappend$a ?v0) lNil$) ?v0) :pattern ((lappend$a ?v0)))) :named a336)) +(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod$)) (= (swap$a (pair$b ?v0 ?v1)) (pair$b ?v1 ?v0))) :named a337)) +(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$)) (= (swap$ (pair$ ?v0 ?v1)) (pair$ ?v1 ?v0))) :named a338)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$) (?v1 A_llist_a_llist_prod_llist$)) (= (ltl$a (fun_app$ (lappend$ ?v0) ?v1)) (ite (fun_app$bw lnull$a ?v0) (ltl$a ?v1) (fun_app$ (lappend$ (ltl$a ?v0)) ?v1)))) :named a339)) +(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$)) (= (ltl$ (fun_app$a (lappend$a ?v0) ?v1)) (ite (fun_app$l lnull$ ?v0) (ltl$ ?v1) (fun_app$a (lappend$a (ltl$ ?v0)) ?v1)))) :named a340)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$) (?v1 A_llist_a_llist_prod_llist$)) (= (lhd$a (fun_app$ (lappend$ ?v0) ?v1)) (ite (fun_app$bw lnull$a ?v0) (lhd$a ?v1) (lhd$a ?v0)))) :named a341)) +(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$)) (= (lhd$ (fun_app$a (lappend$a ?v0) ?v1)) (ite (fun_app$l lnull$ ?v0) (lhd$ ?v1) (lhd$ ?v0)))) :named a342)) +(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$) (?v2 A_llist$)) (= (fun_app$a (lappend$a (fun_app$a (lappend$a ?v0) ?v1)) ?v2) (fun_app$a (lappend$a ?v0) (fun_app$a (lappend$a ?v1) ?v2)))) :named a343)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$) (?v1 A_llist_a_llist_prod_llist$) (?v2 A_llist_a_llist_prod_llist$)) (= (fun_app$ (lappend$ (fun_app$ (lappend$ ?v0) ?v1)) ?v2) (fun_app$ (lappend$ ?v0) (fun_app$ (lappend$ ?v1) ?v2)))) :named a344)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$) (?v1 A_llist_a_llist_prod_llist$)) (! (=> (fun_app$bw lnull$a ?v0) (= (fun_app$ (lappend$ ?v0) ?v1) ?v1)) :pattern ((fun_app$ (lappend$ ?v0) ?v1)))) :named a345)) +(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$)) (! (=> (fun_app$l lnull$ ?v0) (= (fun_app$a (lappend$a ?v0) ?v1) ?v1)) :pattern ((fun_app$a (lappend$a ?v0) ?v1)))) :named a346)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$) (?v1 A_llist_a_llist_prod_llist$)) (! (=> (fun_app$bw lnull$a ?v0) (= (fun_app$ (lappend$ ?v1) ?v0) ?v1)) :pattern ((fun_app$ (lappend$ ?v1) ?v0)))) :named a347)) +(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$)) (! (=> (fun_app$l lnull$ ?v0) (= (fun_app$a (lappend$a ?v1) ?v0) ?v1)) :pattern ((fun_app$a (lappend$a ?v1) ?v0)))) :named a348)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$) (?v1 A_llist_a_llist_prod_llist$)) (=> (and (fun_app$bw lnull$a ?v0) (fun_app$bw lnull$a ?v1)) (fun_app$bw lnull$a (fun_app$ (lappend$ ?v0) ?v1)))) :named a349)) +(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$)) (=> (and (fun_app$l lnull$ ?v0) (fun_app$l lnull$ ?v1)) (fun_app$l lnull$ (fun_app$a (lappend$a ?v0) ?v1)))) :named a350)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$) (?v1 A_llist_a_llist_prod_llist$)) (=> (or (not (fun_app$bw lnull$a ?v0)) (not (fun_app$bw lnull$a ?v1))) (not (fun_app$bw lnull$a (fun_app$ (lappend$ ?v0) ?v1))))) :named a351)) +(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$)) (=> (or (not (fun_app$l lnull$ ?v0)) (not (fun_app$l lnull$ ?v1))) (not (fun_app$l lnull$ (fun_app$a (lappend$a ?v0) ?v1))))) :named a352)) +(assert (! (= (fun_app$ (lappend$ lNil$a) lNil$a) lNil$a) :named a353)) +(assert (! (= (fun_app$a (lappend$a lNil$) lNil$) lNil$) :named a354)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$) (?v1 A_llist_a_llist_prod_llist$)) (= (= (fun_app$ (lappend$ ?v0) ?v1) lNil$a) (and (= ?v0 lNil$a) (= ?v1 lNil$a)))) :named a355)) +(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$)) (= (= (fun_app$a (lappend$a ?v0) ?v1) lNil$) (and (= ?v0 lNil$) (= ?v1 lNil$)))) :named a356)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$) (?v1 A_llist_a_llist_prod_llist$)) (= (= lNil$a (fun_app$ (lappend$ ?v0) ?v1)) (and (= ?v0 lNil$a) (= ?v1 lNil$a)))) :named a357)) +(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$)) (= (= lNil$ (fun_app$a (lappend$a ?v0) ?v1)) (and (= ?v0 lNil$) (= ?v1 lNil$)))) :named a358)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$) (?v1 A_llist_a_llist_prod_llist$)) (= (fun_app$ (lappend$ ?v0) ?v1) (case_llist$d ?v1 (uwh$ ?v1) ?v0))) :named a359)) +(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$)) (= (fun_app$a (lappend$a ?v0) ?v1) (fun_app$a (fun_app$cj (case_llist$a ?v1) (uwi$ ?v1)) ?v0))) :named a360)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$) (?v1 A_llist_a_llist_prod_llist$)) (! (=> (and (fun_app$bw lnull$a ?v0) (fun_app$bw lnull$a ?v1)) (= (fun_app$ (lappend$ ?v0) ?v1) lNil$a)) :pattern ((fun_app$ (lappend$ ?v0) ?v1)))) :named a361)) +(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$)) (! (=> (and (fun_app$l lnull$ ?v0) (fun_app$l lnull$ ?v1)) (= (fun_app$a (lappend$a ?v0) ?v1) lNil$)) :pattern ((fun_app$a (lappend$a ?v0) ?v1)))) :named a362)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$) (?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_prod_llist$)) (= (fun_app$ (lappend$ (fun_app$ (lappend$ ?v0) (lCons$a ?v1 lNil$a))) ?v2) (fun_app$ (lappend$ ?v0) (lCons$a ?v1 ?v2)))) :named a363)) +(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$)) (=> (not (fun_app$l lnull$ ?v0)) (= (fun_app$a (lappend$a (ltl$ ?v0)) ?v1) (ltl$ (fun_app$a (lappend$a ?v0) ?v1))))) :named a364)) +(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$)) (=> (or (not (fun_app$l lnull$ ?v0)) (not (fun_app$l lnull$ ?v1))) (= (fun_app$a (lappend$a ?v0) ?v1) (lCons$ (fun_app$c (fun_app$ck (case_llist$b (lhd$ ?v1)) uwb$) ?v0) (fun_app$a (fun_app$cj (case_llist$a (fun_app$a (fun_app$cj (case_llist$a undefined$) uvv$) ?v1)) (uwj$ ?v1)) ?v0))))) :named a365)) +(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$)) (=> (or (not (fun_app$l lnull$ ?v0)) (not (fun_app$l lnull$ ?v1))) (= (ltl$ (fun_app$a (lappend$a ?v0) ?v1)) (fun_app$a (fun_app$cj (case_llist$a (fun_app$a (fun_app$cj (case_llist$a undefined$) uvv$) ?v1)) (uwj$ ?v1)) ?v0)))) :named a366)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_set$) (?v1 A_llist_a_llist_fun$)) (= (inv_image$ ?v0 ?v1) (collect$ (fun_app$ad uncurry$a (fun_app$z (uwk$ ?v0) ?v1))))) :named a367)) +(assert (! (forall ((?v0 A_llist_bool_fun$) (?v1 A_llist_a_llist_a_llist_prod_set_fun$)) (= (same_fst$ ?v0 ?v1) (collect$a (fun_app$al uncurry$d (fun_app$aj uncurry$c (fun_app$bt (uwm$ ?v0) ?v1)))))) :named a368)) +(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod_llist$) (?v2 A_llist_a_llist_prod_a_llist_a_llist_prod_llist_bool_fun_fun$)) (=> (and (fun_app$i (member$ ?v0) (lset$ ?v1)) (and (forall ((?v3 A_llist_a_llist_prod_llist$)) (=> (not (fun_app$bw lnull$a ?v3)) (fun_app$bw (fun_app$bx ?v2 (lhd$a ?v3)) ?v3))) (forall ((?v3 A_llist_a_llist_prod_llist$) (?v4 A_llist_a_llist_prod$)) (=> (and (not (fun_app$bw lnull$a ?v3)) (and (fun_app$i (member$ ?v4) (lset$ (ltl$a ?v3))) (fun_app$bw (fun_app$bx ?v2 ?v4) (ltl$a ?v3)))) (fun_app$bw (fun_app$bx ?v2 ?v4) ?v3))))) (fun_app$bw (fun_app$bx ?v2 ?v0) ?v1))) :named a369)) +(assert (! (forall ((?v0 A$) (?v1 A_llist$) (?v2 A_a_llist_bool_fun_fun$)) (=> (and (member$b ?v0 (lset$a ?v1)) (and (forall ((?v3 A_llist$)) (=> (not (fun_app$l lnull$ ?v3)) (fun_app$l (fun_app$as ?v2 (lhd$ ?v3)) ?v3))) (forall ((?v3 A_llist$) (?v4 A$)) (=> (and (not (fun_app$l lnull$ ?v3)) (and (member$b ?v4 (lset$a (ltl$ ?v3))) (fun_app$l (fun_app$as ?v2 ?v4) (ltl$ ?v3)))) (fun_app$l (fun_app$as ?v2 ?v4) ?v3))))) (fun_app$l (fun_app$as ?v2 ?v0) ?v1))) :named a370)) +(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$) (?v2 A_llist_a_llist_prod_set$) (?v3 A_llist_a_llist_fun$)) (= (fun_app$i (member$ (pair$ ?v0 ?v1)) (inv_image$ ?v2 ?v3)) (fun_app$i (member$ (pair$ (fun_app$a ?v3 ?v0) (fun_app$a ?v3 ?v1))) ?v2))) :named a371)) +(assert (! (forall ((?v0 A_llist_bool_fun$) (?v1 A_llist$) (?v2 A_llist$) (?v3 A_llist$) (?v4 A_llist_a_llist_a_llist_prod_set_fun$)) (=> (and (fun_app$l ?v0 ?v1) (fun_app$i (member$ (pair$ ?v2 ?v3)) (fun_app$n ?v4 ?v1))) (member$a (pair$b (pair$ ?v1 ?v2) (pair$ ?v1 ?v3)) (same_fst$ ?v0 ?v4)))) :named a372)) +(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod_llist$)) (fun_app$i (member$ ?v0) (lset$ (lCons$a ?v0 ?v1)))) :named a373)) +(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod_llist$)) (fun_app$i (member$ ?v0) (lset$ (lCons$a ?v0 ?v1)))) :named a374)) +(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod_llist$) (?v2 A_llist_a_llist_prod$)) (=> (fun_app$i (member$ ?v0) (lset$ ?v1)) (fun_app$i (member$ ?v0) (lset$ (lCons$a ?v2 ?v1))))) :named a375)) +(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod_llist$) (?v2 A_llist_a_llist_prod$)) (=> (fun_app$i (member$ ?v0) (lset$ ?v1)) (fun_app$i (member$ ?v0) (lset$ (lCons$a ?v2 ?v1))))) :named a376)) +(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod_llist$)) (=> (and (fun_app$i (member$ ?v0) (lset$ ?v1)) (and (forall ((?v2 A_llist_a_llist_prod_llist$)) (=> (= ?v1 (lCons$a ?v0 ?v2)) false)) (forall ((?v2 A_llist_a_llist_prod$) (?v3 A_llist_a_llist_prod_llist$)) (=> (and (= ?v1 (lCons$a ?v2 ?v3)) (fun_app$i (member$ ?v0) (lset$ ?v3))) false)))) false)) :named a377)) +(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod_llist$) (?v2 A_llist_a_llist_prod_llist_bool_fun$)) (=> (and (fun_app$i (member$ ?v0) (lset$ ?v1)) (and (forall ((?v3 A_llist_a_llist_prod_llist$)) (fun_app$bw ?v2 (lCons$a ?v0 ?v3))) (forall ((?v3 A_llist_a_llist_prod$) (?v4 A_llist_a_llist_prod_llist$)) (=> (and (fun_app$i (member$ ?v0) (lset$ ?v4)) (and (not (= ?v0 ?v3)) (fun_app$bw ?v2 ?v4))) (fun_app$bw ?v2 (lCons$a ?v3 ?v4)))))) (fun_app$bw ?v2 ?v1))) :named a378)) +(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod_llist$) (?v2 A_llist_a_llist_prod_llist_bool_fun$)) (=> (and (fun_app$i (member$ ?v0) (lset$ ?v1)) (and (forall ((?v3 A_llist_a_llist_prod_llist$)) (fun_app$bw ?v2 (lCons$a ?v0 ?v3))) (forall ((?v3 A_llist_a_llist_prod$) (?v4 A_llist_a_llist_prod_llist$)) (=> (and (fun_app$i (member$ ?v0) (lset$ ?v4)) (fun_app$bw ?v2 ?v4)) (fun_app$bw ?v2 (lCons$a ?v3 ?v4)))))) (fun_app$bw ?v2 ?v1))) :named a379)) +(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod_llist$)) (=> (and (fun_app$i (member$ ?v0) (lset$ ?v1)) (and (forall ((?v2 A_llist_a_llist_prod_llist$)) (=> (= ?v1 (lCons$a ?v0 ?v2)) false)) (forall ((?v2 A_llist_a_llist_prod$) (?v3 A_llist_a_llist_prod_llist$)) (=> (and (= ?v1 (lCons$a ?v2 ?v3)) (fun_app$i (member$ ?v0) (lset$ ?v3))) false)))) false)) :named a380)) +(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod_llist$) (?v2 A_llist_a_llist_prod_a_llist_a_llist_prod_llist_bool_fun_fun$)) (=> (and (fun_app$i (member$ ?v0) (lset$ ?v1)) (and (forall ((?v3 A_llist_a_llist_prod$) (?v4 A_llist_a_llist_prod_llist$)) (fun_app$bw (fun_app$bx ?v2 ?v3) (lCons$a ?v3 ?v4))) (forall ((?v3 A_llist_a_llist_prod$) (?v4 A_llist_a_llist_prod_llist$) (?v5 A_llist_a_llist_prod$)) (=> (and (fun_app$i (member$ ?v5) (lset$ ?v4)) (fun_app$bw (fun_app$bx ?v2 ?v5) ?v4)) (fun_app$bw (fun_app$bx ?v2 ?v5) (lCons$a ?v3 ?v4)))))) (fun_app$bw (fun_app$bx ?v2 ?v0) ?v1))) :named a381)) +(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod_llist$)) (=> (fun_app$i (member$ ?v0) (lset$ (ltl$a ?v1))) (fun_app$i (member$ ?v0) (lset$ ?v1)))) :named a382)) +(assert (! (forall ((?v0 A$) (?v1 A_llist$)) (=> (member$b ?v0 (lset$a (ltl$ ?v1))) (member$b ?v0 (lset$a ?v1)))) :named a383)) +(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod_llist$)) (= (fun_app$i (member$ ?v0) (lset$ ?v1)) (fun_app$bw (lmember$ ?v0) ?v1))) :named a384)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$) (?v1 A_llist_a_llist_prod$)) (=> (and (not (fun_app$bw lnull$a ?v0)) (fun_app$i (member$ ?v1) (lset$ (ltl$a ?v0)))) (fun_app$i (member$ ?v1) (lset$ ?v0)))) :named a385)) +(assert (! (forall ((?v0 A_llist$) (?v1 A$)) (=> (and (not (fun_app$l lnull$ ?v0)) (member$b ?v1 (lset$a (ltl$ ?v0)))) (member$b ?v1 (lset$a ?v0)))) :named a386)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$)) (=> (not (fun_app$bw lnull$a ?v0)) (fun_app$i (member$ (lhd$a ?v0)) (lset$ ?v0)))) :named a387)) +(assert (! (forall ((?v0 A_llist$)) (=> (not (fun_app$l lnull$ ?v0)) (member$b (lhd$ ?v0) (lset$a ?v0)))) :named a388)) +(assert (! (forall ((?v0 A_llist$)) (= (lhd$ ?v0) (fun_app$c (fun_app$ck (case_llist$b undefined$a) uwb$) ?v0))) :named a389)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_set$) (?v1 A_llist_a_llist_prod_set$)) (= (lex_prod$ ?v0 ?v1) (collect$a (fun_app$al uncurry$d (fun_app$aj uncurry$c (fun_app$bq (uwo$ ?v0) ?v1)))))) :named a390)) +(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod_llist$)) (=> (fun_app$i (member$ ?v0) (lset$ ?v1)) (exists ((?v2 A_llist_a_llist_prod_llist$) (?v3 A_llist_a_llist_prod_llist$)) (and (= ?v1 (fun_app$ (lappend$ ?v2) (lCons$a ?v0 ?v3))) (and (lfinite$ ?v2) (not (fun_app$i (member$ ?v0) (lset$ ?v2)))))))) :named a391)) +(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod_llist$)) (=> (fun_app$i (member$ ?v0) (lset$ ?v1)) (exists ((?v2 A_llist_a_llist_prod_llist$) (?v3 A_llist_a_llist_prod_llist$)) (and (= ?v1 (fun_app$ (lappend$ ?v2) (lCons$a ?v0 ?v3))) (lfinite$ ?v2))))) :named a392)) +(assert (! (forall ((?v0 A_llist$)) (= (lfinite$a (ltl$ ?v0)) (lfinite$a ?v0))) :named a393)) +(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$) (?v2 A_llist$) (?v3 A_llist$) (?v4 A_llist_a_llist_prod_set$) (?v5 A_llist_a_llist_prod_set$)) (= (member$a (pair$b (pair$ ?v0 ?v1) (pair$ ?v2 ?v3)) (lex_prod$ ?v4 ?v5)) (or (fun_app$i (member$ (pair$ ?v0 ?v2)) ?v4) (and (= ?v0 ?v2) (fun_app$i (member$ (pair$ ?v1 ?v3)) ?v5))))) :named a394)) +(assert (! (forall ((?v0 A_llist$)) (=> (fun_app$l lnull$ ?v0) (lfinite$a ?v0))) :named a395)) +(assert (! (forall ((?v0 A_llist$) (?v1 A_llist_bool_fun$)) (=> (and (lfinite$a ?v0) (and (forall ((?v2 A_llist$)) (=> (fun_app$l lnull$ ?v2) (fun_app$l ?v1 ?v2))) (forall ((?v2 A_llist$)) (=> (and (lfinite$a ?v2) (and (not (fun_app$l lnull$ ?v2)) (fun_app$l ?v1 (ltl$ ?v2)))) (fun_app$l ?v1 ?v2))))) (fun_app$l ?v1 ?v0))) :named a396)) +(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod_llist$) (?v2 A_llist_a_llist_prod_llist$)) (= (fun_app$i (member$ ?v0) (lset$ (fun_app$ (lappend$ ?v1) ?v2))) (or (fun_app$i (member$ ?v0) (lset$ ?v1)) (and (lfinite$ ?v1) (fun_app$i (member$ ?v0) (lset$ ?v2)))))) :named a397)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_bool_fun$) (?v1 A_llist_a_llist_prod_bool_fun$)) (= (collect$ (fun_app$t (uwp$ ?v0) ?v1)) (sup$ (collect$ ?v0) (collect$ ?v1)))) :named a398)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_set$) (?v1 A_llist_a_llist_prod_set$)) (= (sup$ ?v0 ?v1) (collect$ (fun_app$s (uwq$ ?v0) ?v1)))) :named a399)) +(assert (! (forall ((?v0 A_llist_a_llist_bool_fun_fun$) (?v1 A_llist$) (?v2 A_llist$) (?v3 A_a_bool_fun_fun$)) (=> (and (fun_app$l (fun_app$m ?v0 ?v1) ?v2) (forall ((?v4 A_llist$) (?v5 A_llist$)) (=> (fun_app$l (fun_app$m ?v0 ?v4) ?v5) (and (= (fun_app$l lnull$ ?v4) (fun_app$l lnull$ ?v5)) (=> (and (not (fun_app$l lnull$ ?v4)) (not (fun_app$l lnull$ ?v5))) (and (fun_app$k (fun_app$co ?v3 (lhd$ ?v4)) (lhd$ ?v5)) (fun_app$l (fun_app$m ?v0 (ltl$ ?v4)) (ltl$ ?v5)))))))) (fun_app$l (fun_app$m (llist_all2$ ?v3) ?v1) ?v2))) :named a400)) +(assert (! (forall ((?v0 A_a_bool_fun_fun$) (?v1 A_llist$) (?v2 A_llist$)) (= (fun_app$l (fun_app$m (llist_all2$ ?v0) ?v1) ?v2) (and (= (fun_app$l lnull$ ?v1) (fun_app$l lnull$ ?v2)) (=> (and (not (fun_app$l lnull$ ?v1)) (not (fun_app$l lnull$ ?v2))) (and (fun_app$k (fun_app$co ?v0 (lhd$ ?v1)) (lhd$ ?v2)) (fun_app$l (fun_app$m (llist_all2$ ?v0) (ltl$ ?v1)) (ltl$ ?v2))))))) :named a401)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_set$) (?v1 A_llist_a_llist_prod_set$)) (=> (forall ((?v2 A_llist$) (?v3 A_llist$)) (=> (fun_app$i (member$ (pair$ ?v2 ?v3)) ?v0) (fun_app$i (member$ (pair$ ?v2 ?v3)) ?v1))) (fun_app$i (less_eq$ ?v0) ?v1))) :named a402)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) (?v1 A_llist_a_llist_prod_llist$) (?v2 A_llist_a_llist_prod_llist$) (?v3 A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$)) (=> (and (fun_app$bw (fun_app$by (llist_all2$a ?v0) ?v1) ?v2) (forall ((?v4 A_llist_a_llist_prod$) (?v5 A_llist_a_llist_prod$)) (=> (and (fun_app$i (member$ ?v4) (lset$ ?v1)) (and (fun_app$i (member$ ?v5) (lset$ ?v2)) (fun_app$h (fun_app$r ?v0 ?v4) ?v5))) (fun_app$h (fun_app$r ?v3 ?v4) ?v5)))) (fun_app$bw (fun_app$by (llist_all2$a ?v3) ?v1) ?v2))) :named a403)) +(assert (! (forall ((?v0 A_llist$)) (less_eq$a (lset$a (ltl$ ?v0)) (lset$a ?v0))) :named a404)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_set$) (?v1 A_llist_a_llist_prod_bool_fun$) (?v2 A_llist_a_llist_prod_bool_fun$)) (= (fun_app$i (less_eq$ ?v0) (collect$ (fun_app$t (uwr$ ?v1) ?v2))) (and (fun_app$i (less_eq$ ?v0) (collect$ ?v1)) (fun_app$i (less_eq$ ?v0) (collect$ ?v2))))) :named a405)) +(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod_set$) (?v2 A_llist_a_llist_prod_set$) (?v3 A_llist_a_llist_prod_bool_fun$)) (=> (and (fun_app$i (member$ ?v0) ?v1) (fun_app$i (less_eq$ ?v1) (collect$ (fun_app$t (uws$ ?v2) ?v3)))) (fun_app$h ?v3 ?v0))) :named a406)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_set$) (?v1 A_llist_a_llist_prod_set$) (?v2 A_llist_a_llist_prod_bool_fun$) (?v3 A_llist_a_llist_prod_bool_fun$)) (=> (and (fun_app$i (less_eq$ ?v0) ?v1) (forall ((?v4 A_llist_a_llist_prod$)) (=> (and (fun_app$i (member$ ?v4) ?v0) (fun_app$h ?v2 ?v4)) (fun_app$h ?v3 ?v4)))) (fun_app$i (less_eq$ (collect$ (fun_app$t (uws$ ?v0) ?v2))) (collect$ (fun_app$t (uws$ ?v1) ?v3))))) :named a407)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_set$) (?v1 A_llist_a_llist_prod_set$)) (= (fun_app$i (less_eq$ ?v0) ?v1) (fun_app$bk (less_eq$b (uui$ ?v0)) (uui$ ?v1)))) :named a408)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_set$) (?v1 A_llist_a_llist_prod_set$)) (= (fun_app$bk (less_eq$b (uui$ ?v0)) (uui$ ?v1)) (fun_app$i (less_eq$ ?v0) ?v1))) :named a409)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_set$) (?v1 A_llist_a_llist_prod_set$)) (= (less_eq$c (uvz$ ?v0) (uvz$ ?v1)) (fun_app$i (less_eq$ ?v0) ?v1))) :named a410)) +(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$) (?v2 A_llist_a_llist_prod_set$) (?v3 A_llist$)) (=> (and (fun_app$i (member$ (pair$ ?v0 ?v1)) ?v2) (= ?v3 ?v1)) (fun_app$i (member$ (pair$ ?v0 ?v3)) ?v2))) :named a411)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_set$) (?v1 A_llist_a_llist_prod_bool_fun$)) (fun_app$i (less_eq$ (collect$ (fun_app$t (uws$ ?v0) ?v1))) ?v0)) :named a412)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_set$) (?v1 A_llist_a_llist_prod_set$) (?v2 A_llist_a_llist_prod_bool_fun$)) (=> (fun_app$i (less_eq$ ?v0) ?v1) (= (fun_app$i (less_eq$ ?v0) (collect$ (fun_app$t (uws$ ?v1) ?v2))) (forall ((?v3 A_llist_a_llist_prod$)) (=> (fun_app$i (member$ ?v3) ?v0) (fun_app$h ?v2 ?v3)))))) :named a413)) +(assert (! (forall ((?v0 A_llist_a_llist_bool_fun_fun$) (?v1 A_llist_a_llist_bool_fun_fun$)) (=> (less_eq$c ?v0 ?v1) (fun_app$i (less_eq$ (collect$ (fun_app$ad uncurry$a ?v0))) (collect$ (fun_app$ad uncurry$a ?v1))))) :named a414)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_set$) (?v1 A_llist_a_llist_prod_set$)) (=> (and (fun_app$i (less_eq$ ?v0) (collect$ (fun_app$ad uncurry$a (in_rel$ ?v1)))) (=> (fun_app$i (less_eq$ ?v0) ?v1) false)) false)) :named a415)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_set$) (?v1 A_llist$) (?v2 A_llist$)) (! (= (fun_app$l (fun_app$m (in_rel$ ?v0) ?v1) ?v2) (fun_app$i (member$ (pair$ ?v1 ?v2)) ?v0)) :pattern ((fun_app$l (fun_app$m (in_rel$ ?v0) ?v1) ?v2)))) :named a416)) +(assert (! (forall ((?v0 A_llist_a_llist_bool_fun_fun$)) (= (in_rel$ (collect$ (fun_app$ad uncurry$a ?v0))) ?v0)) :named a417)) +(assert (! (forall ((?v0 A_llist_a_llist_prod_set$) (?v1 A_llist_a_llist_prod_set$)) (=> (fun_app$i (less_eq$ ?v0) ?v1) (fun_app$i (less_eq$ ?v0) (collect$ (fun_app$ad uncurry$a (in_rel$ ?v1)))))) :named a418)) +(assert (! (forall ((?v0 A_llist$) (?v1 A_llist_a_llist_prod_a_llist_fun$) (?v2 A_llist_a_llist_prod$) (?v3 A_llist$) (?v4 A_llist_a_llist_prod_a_llist_fun$) (?v5 A_llist_a_llist_prod_set$)) (=> (and (= ?v0 (fun_app$cp ?v1 ?v2)) (and (= ?v3 (fun_app$cp ?v4 ?v2)) (fun_app$i (member$ ?v2) ?v5))) (fun_app$i (member$ (pair$ ?v0 ?v3)) (image2$ ?v5 ?v1 ?v4)))) :named a419)) +(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$)) (= (the$ (fun_app$ad uncurry$a (fun_app$aa (uwt$ ?v0) ?v1))) (pair$ ?v0 ?v1))) :named a420)) +(check-sat) + |