diff options
Diffstat (limited to 'test/regress/regress0/quantifiers/cdt-0208-to.smt2')
| -rw-r--r-- | test/regress/regress0/quantifiers/cdt-0208-to.smt2 | 767 |
1 files changed, 0 insertions, 767 deletions
diff --git a/test/regress/regress0/quantifiers/cdt-0208-to.smt2 b/test/regress/regress0/quantifiers/cdt-0208-to.smt2 deleted file mode 100644 index 9eff608bb..000000000 --- a/test/regress/regress0/quantifiers/cdt-0208-to.smt2 +++ /dev/null @@ -1,767 +0,0 @@ -; COMMAND-LINE: --full-saturate-quant --lang=smt2.5 -; 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) - |