Updates related to finite model finding and (co)datatypes. Bug fix enumerator and codatatype rewriter, further simplify fmc.

4 files changed, 952 insertions, 3 deletions

diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am
index 370096a1e..48b732f26 100644
--- a/test/regress/regress0/fmf/Makefile.am
+++ b/test/regress/regress0/fmf/Makefile.am
@@ -49,7 +49,8 @@ TESTS =	\
 	jasmin-cdt-crash.smt2 \
 	loopy_coda.smt2 \
 	fmc_unsound_model.smt2 \
-	am-bad-model.cvc
+	am-bad-model.cvc \
+	nun-0208-to.cvc
 
 
 EXTRA_DIST = $(TESTS)
diff --git a/test/regress/regress0/fmf/nun-0208-to.smt2 b/test/regress/regress0/fmf/nun-0208-to.smt2
new file mode 100644
index 000000000..f831af1f2
--- /dev/null
+++ b/test/regress/regress0/fmf/nun-0208-to.smt2
@@ -0,0 +1,180 @@
+; COMMAND-LINE: --finite-model-find
+; EXPECT: sat
+  (set-logic ALL_SUPPORTED)
+  (declare-sort b__ 0)
+  (declare-fun __nun_card_witness_0_ () b__)
+  (declare-sort a__ 0)
+  (declare-fun __nun_card_witness_1_ () a__)
+  (declare-datatypes ()
+     ((prod__ (Pair__ (_select_Pair___0 a__) (_select_Pair___1 b__)))))
+  (declare-datatypes ()
+     ((list2__
+         (Cons2__ (_select_Cons2___0 prod__) (_select_Cons2___1 list2__)) 
+         (Nil2__ ))))
+  (declare-datatypes ()
+     ((list__ (Cons__ (_select_Cons___0 a__) (_select_Cons___1 list__)) 
+         (Nil__ ))))
+  (declare-datatypes ()
+     ((list1__ (Cons1__ (_select_Cons1___0 b__) (_select_Cons1___1 list1__)) 
+         (Nil1__ ))))
+  (declare-sort G_zip__ 0)
+  (declare-fun __nun_card_witness_2_ () G_zip__)
+  (declare-fun zip__ (list__ list1__) list2__)
+  (declare-fun proj_G_zip__0_ (G_zip__) list__)
+  (declare-fun proj_G_zip__1_ (G_zip__) list1__)
+  (assert
+   (forall ((a/166 G_zip__))
+      (and
+       (= (zip__ (proj_G_zip__0_ a/166) (proj_G_zip__1_ a/166))
+        (ite (is-Cons1__ (proj_G_zip__1_ a/166))
+          (ite (is-Cons__ (proj_G_zip__0_ a/166))
+            (Cons2__
+             (Pair__ (_select_Cons___0 (proj_G_zip__0_ a/166)) 
+              (_select_Cons1___0 (proj_G_zip__1_ a/166))) 
+             (zip__ (_select_Cons___1 (proj_G_zip__0_ a/166)) 
+              (_select_Cons1___1 (proj_G_zip__1_ a/166))))
+            Nil2__)
+          Nil2__)) 
+       (=> (is-Cons1__ (proj_G_zip__1_ a/166))
+        (=> (is-Cons__ (proj_G_zip__0_ a/166))
+         (exists ((a/168 G_zip__))
+            (and
+             (= (_select_Cons1___1 (proj_G_zip__1_ a/166))
+              (proj_G_zip__1_ a/168)) 
+             (= (_select_Cons___1 (proj_G_zip__0_ a/166))
+              (proj_G_zip__0_ a/168)))))))))
+  (declare-datatypes () ((nat__ (Suc__ (_select_Suc___0 nat__)) (zero__ ))))
+  (declare-sort G_replicate__ 0)
+  (declare-fun __nun_card_witness_3_ () G_replicate__)
+  (declare-fun replicate__ (nat__ a__) list__)
+  (declare-fun proj_G_replicate__0_ (G_replicate__) nat__)
+  (declare-fun proj_G_replicate__1_ (G_replicate__) a__)
+  (assert
+   (forall ((a/169 G_replicate__))
+      (and
+       (=
+        (replicate__ (proj_G_replicate__0_ a/169) 
+         (proj_G_replicate__1_ a/169))
+        (ite (is-Suc__ (proj_G_replicate__0_ a/169))
+          (Cons__ (proj_G_replicate__1_ a/169) 
+           (replicate__ (_select_Suc___0 (proj_G_replicate__0_ a/169)) 
+            (proj_G_replicate__1_ a/169)))
+          Nil__)) 
+       (=> (is-Suc__ (proj_G_replicate__0_ a/169))
+        (exists ((a/171 G_replicate__))
+           (and
+            (= (proj_G_replicate__1_ a/169) (proj_G_replicate__1_ a/171)) 
+            (= (_select_Suc___0 (proj_G_replicate__0_ a/169))
+             (proj_G_replicate__0_ a/171))))))))
+  (declare-fun j__ () nat__)
+  (declare-fun x__ () a__)
+  (declare-sort G_replicate1__ 0)
+  (declare-fun __nun_card_witness_4_ () G_replicate1__)
+  (declare-fun replicate1__ (nat__ b__) list1__)
+  (declare-fun proj_G_replicate1__0_ (G_replicate1__) nat__)
+  (declare-fun proj_G_replicate1__1_ (G_replicate1__) b__)
+  (assert
+   (forall ((a/172 G_replicate1__))
+      (and
+       (=
+        (replicate1__ (proj_G_replicate1__0_ a/172) 
+         (proj_G_replicate1__1_ a/172))
+        (ite (is-Suc__ (proj_G_replicate1__0_ a/172))
+          (Cons1__ (proj_G_replicate1__1_ a/172) 
+           (replicate1__ (_select_Suc___0 (proj_G_replicate1__0_ a/172)) 
+            (proj_G_replicate1__1_ a/172)))
+          Nil1__)) 
+       (=> (is-Suc__ (proj_G_replicate1__0_ a/172))
+        (exists ((a/174 G_replicate1__))
+           (and
+            (= (proj_G_replicate1__1_ a/172) (proj_G_replicate1__1_ a/174)) 
+            (= (_select_Suc___0 (proj_G_replicate1__0_ a/172))
+             (proj_G_replicate1__0_ a/174))))))))
+  (declare-fun y__ () b__)
+  (declare-sort G_replicate2__ 0)
+  (declare-fun __nun_card_witness_5_ () G_replicate2__)
+  (declare-fun replicate2__ (nat__ prod__) list2__)
+  (declare-fun proj_G_replicate2__0_ (G_replicate2__) nat__)
+  (declare-fun proj_G_replicate2__1_ (G_replicate2__) prod__)
+  (assert
+   (forall ((a/175 G_replicate2__))
+      (and
+       (=
+        (replicate2__ (proj_G_replicate2__0_ a/175) 
+         (proj_G_replicate2__1_ a/175))
+        (ite (is-Suc__ (proj_G_replicate2__0_ a/175))
+          (Cons2__ (proj_G_replicate2__1_ a/175) 
+           (replicate2__ (_select_Suc___0 (proj_G_replicate2__0_ a/175)) 
+            (proj_G_replicate2__1_ a/175)))
+          Nil2__)) 
+       (=> (is-Suc__ (proj_G_replicate2__0_ a/175))
+        (exists ((a/177 G_replicate2__))
+           (and
+            (= (proj_G_replicate2__1_ a/175) (proj_G_replicate2__1_ a/177)) 
+            (= (_select_Suc___0 (proj_G_replicate2__0_ a/175))
+             (proj_G_replicate2__0_ a/177))))))))
+  (declare-sort G_less__eq__ 0)
+  (declare-fun __nun_card_witness_6_ () G_less__eq__)
+  (declare-fun less__eq__ (nat__ nat__) Bool)
+  (declare-fun proj_G_less__eq__0_ (G_less__eq__) nat__)
+  (declare-fun proj_G_less__eq__1_ (G_less__eq__) nat__)
+  (assert
+   (forall ((a/178 G_less__eq__))
+      (and
+       (=
+        (less__eq__ (proj_G_less__eq__0_ a/178) (proj_G_less__eq__1_ a/178))
+        (=> (is-Suc__ (proj_G_less__eq__0_ a/178))
+         (and (is-Suc__ (proj_G_less__eq__1_ a/178)) 
+          (less__eq__ (_select_Suc___0 (proj_G_less__eq__0_ a/178)) 
+           (_select_Suc___0 (proj_G_less__eq__1_ a/178)))))) 
+       (exists ((a/182 G_less__eq__))
+          (and
+           (= (_select_Suc___0 (proj_G_less__eq__1_ a/178))
+            (proj_G_less__eq__1_ a/182)) 
+           (= (_select_Suc___0 (proj_G_less__eq__0_ a/178))
+            (proj_G_less__eq__0_ a/182)))))))
+  (declare-sort G_min__ 0)
+  (declare-fun __nun_card_witness_7_ () G_min__)
+  (declare-fun min__ (nat__ nat__) nat__)
+  (declare-fun proj_G_min__0_ (G_min__) nat__)
+  (declare-fun proj_G_min__1_ (G_min__) nat__)
+  (assert
+   (forall ((a/183 G_min__))
+      (and
+       (= (min__ (proj_G_min__0_ a/183) (proj_G_min__1_ a/183))
+        (ite (less__eq__ (proj_G_min__0_ a/183) (proj_G_min__1_ a/183))
+          (proj_G_min__0_ a/183) (proj_G_min__1_ a/183))) 
+       (exists ((a/184 G_less__eq__))
+          (and (= (proj_G_min__1_ a/183) (proj_G_less__eq__1_ a/184)) 
+           (= (proj_G_min__0_ a/183) (proj_G_less__eq__0_ a/184)))))))
+  (declare-fun i__ () nat__)
+  (assert
+   (not
+    (=>
+     (and
+      (exists ((a/212 G_min__))
+         (and (= i__ (proj_G_min__1_ a/212)) (= i__ (proj_G_min__0_ a/212)))) 
+      (exists ((a/208 G_replicate2__))
+         (and (= (Pair__ x__ y__) (proj_G_replicate2__1_ a/208)) 
+          (= (min__ i__ i__) (proj_G_replicate2__0_ a/208)) 
+          (exists ((a/210 G_min__))
+             (and (= i__ (proj_G_min__1_ a/210)) 
+              (= i__ (proj_G_min__0_ a/210)))))) 
+      (exists ((a/199 G_zip__))
+         (and (= (replicate1__ j__ y__) (proj_G_zip__1_ a/199)) 
+          (exists ((a/202 G_replicate1__))
+             (and (= y__ (proj_G_replicate1__1_ a/202)) 
+              (= j__ (proj_G_replicate1__0_ a/202)))) 
+          (= (replicate__ j__ x__) (proj_G_zip__0_ a/199)) 
+          (exists ((a/203 G_replicate__))
+             (and (= x__ (proj_G_replicate__1_ a/203)) 
+              (= j__ (proj_G_replicate__0_ a/203)))))) 
+      (exists ((a/207 G_replicate1__))
+         (and (= y__ (proj_G_replicate1__1_ a/207)) 
+          (= j__ (proj_G_replicate1__0_ a/207)))) 
+      (exists ((a/206 G_replicate__))
+         (and (= x__ (proj_G_replicate__1_ a/206)) 
+          (= j__ (proj_G_replicate__0_ a/206)))))
+     (= (replicate2__ (min__ i__ i__) (Pair__ x__ y__))
+      (zip__ (replicate__ j__ x__) (replicate1__ j__ y__))))))
+  (check-sat)
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am
index 7178710cb..3fff9b0de 100644
--- a/test/regress/regress0/quantifiers/Makefile.am
+++ b/test/regress/regress0/quantifiers/Makefile.am
@@ -41,7 +41,7 @@ TESTS =	\
 	symmetric_unsat_7.smt2 \
 	javafe.ast.StmtVec.009.smt2 \
 	ARI176e1.smt2 \
-        bi-artm-s.smt2 \
+  bi-artm-s.smt2 \
 	simp-typ-test.smt2 \
 	macros-int-real.smt2 \
 	stream-x2014-09-18-unsat.smt2 \
@@ -64,7 +64,8 @@ TESTS =	\
 	ari056.smt2 \
 	ext-ex-deq-trigger.smt2 \
 	matching-lia-1arg.smt2 \
-	RND_4_16.smt2
+	RND_4_16.smt2 \
+  cdt-0208-to.smt2
 
 
 # regression can be solved with --finite-model-find --fmf-inst-engine
diff --git a/test/regress/regress0/quantifiers/cdt-0208-to.smt2 b/test/regress/regress0/quantifiers/cdt-0208-to.smt2
new file mode 100644
index 000000000..a458cea64
--- /dev/null
+++ b/test/regress/regress0/quantifiers/cdt-0208-to.smt2
@@ -0,0 +1,767 @@
+; COMMAND-LINE: --full-saturate-quant
+; EXPECT: unsat
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+(declare-sort A$ 0)
+(declare-sort A_set$ 0)
+(declare-sort A_a_fun$ 0)
+(declare-sort A_bool_fun$ 0)
+(declare-sort Bool_a_fun$ 0)
+(declare-sort A_a_llist_fun$ 0)
+(declare-sort A_llist_a_fun$ 0)
+(declare-sort Bool_bool_fun$ 0)
+(declare-sort A_a_bool_fun_fun$ 0)
+(declare-sort A_llist_bool_fun$ 0)
+(declare-sort Bool_a_llist_fun$ 0)
+(declare-sort A_llist_a_set_fun$ 0)
+(declare-sort A_a_llist_a_fun_fun$ 0)
+(declare-sort A_llist_a_llist_fun$ 0)
+(declare-sort A_a_llist_bool_fun_fun$ 0)
+(declare-sort A_llist_a_llist_prod_set$ 0)
+(declare-sort A_a_llist_a_llist_fun_fun$ 0)
+(declare-sort A_llist_a_llist_bool_fun_fun$ 0)
+(declare-sort A_llist_a_llist_a_set_fun_fun$ 0)
+(declare-sort A_llist_a_llist_prod_bool_fun$ 0)
+(declare-sort Bool_a_llist_a_llist_prod_fun$ 0)
+(declare-sort A_llist_a_llist_prod_a_set_fun$ 0)
+(declare-sort A_llist_a_llist_a_llist_prod_fun$ 0)
+(declare-sort A_llist_a_llist_prod_a_llist_fun$ 0)
+(declare-sort A_llist_a_llist_prod_set_bool_fun$ 0)
+(declare-sort Bool_a_llist_a_llist_prod_set_fun$ 0)
+(declare-sort A_llist_a_llist_prod_llist_bool_fun$ 0)
+(declare-sort A_llist_a_llist_a_llist_prod_set_fun$ 0)
+(declare-sort A_a_llist_a_fun_fun_a_llist_a_fun_fun$ 0)
+(declare-sort A_llist_a_llist_prod_bool_fun_bool_fun$ 0)
+(declare-sort Bool_a_llist_a_llist_prod_bool_fun_fun$ 0)
+(declare-sort A_llist_a_llist_a_llist_bool_fun_fun_fun$ 0)
+(declare-sort A_llist_a_llist_a_llist_prod_bool_fun_fun$ 0)
+(declare-sort A_a_llist_a_fun_fun_a_a_llist_a_fun_fun_fun$ 0)
+(declare-sort A_a_llist_bool_fun_fun_a_llist_bool_fun_fun$ 0)
+(declare-sort A_llist_a_llist_fun_a_llist_a_llist_fun_fun$ 0)
+(declare-sort A_llist_a_llist_a_llist_a_llist_prod_fun_fun$ 0)
+(declare-sort A_llist_a_llist_prod_a_llist_a_llist_prod_fun$ 0)
+(declare-sort A_a_llist_a_fun_fun_a_a_llist_bool_fun_fun_fun$ 0)
+(declare-sort A_a_llist_bool_fun_fun_a_a_llist_a_fun_fun_fun$ 0)
+(declare-sort A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$ 0)
+(declare-sort A_a_llist_a_fun_fun_a_a_llist_a_llist_fun_fun_fun$ 0)
+(declare-sort A_a_llist_a_llist_fun_fun_a_a_llist_a_fun_fun_fun$ 0)
+(declare-sort A_a_llist_a_llist_fun_fun_a_llist_a_llist_fun_fun$ 0)
+(declare-sort A_a_llist_bool_fun_fun_a_a_llist_bool_fun_fun_fun$ 0)
+(declare-sort A_llist_a_llist_prod_a_llist_a_llist_prod_set_fun$ 0)
+(declare-sort A_llist_a_llist_prod_set_a_llist_a_llist_prod_fun$ 0)
+(declare-sort A_llist_a_llist_prod_a_llist_a_llist_prod_prod_set$ 0)
+(declare-sort A_llist_a_llist_prod_llist_a_llist_a_llist_prod_fun$ 0)
+(declare-sort A_a_llist_a_llist_fun_fun_a_a_llist_bool_fun_fun_fun$ 0)
+(declare-sort A_a_llist_bool_fun_fun_a_a_llist_a_llist_fun_fun_fun$ 0)
+(declare-sort A_llist_a_llist_a_llist_a_llist_bool_fun_fun_fun_fun$ 0)
+(declare-sort A_llist_a_llist_fun_a_llist_a_llist_bool_fun_fun_fun$ 0)
+(declare-sort A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$ 0)
+(declare-sort A_llist_a_llist_prod_a_llist_a_llist_bool_fun_fun_fun$ 0)
+(declare-sort A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$ 0)
+(declare-sort A_a_llist_a_llist_fun_fun_a_a_llist_a_llist_fun_fun_fun$ 0)
+(declare-sort A_llist_a_llist_prod_a_llist_a_llist_prod_a_set_fun_fun$ 0)
+(declare-sort A_llist_a_llist_prod_a_llist_a_llist_prod_prod_bool_fun$ 0)
+(declare-sort A_llist_a_llist_prod_llist_a_llist_a_llist_prod_llist_fun$ 0)
+(declare-sort A_llist_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_fun$ 0)
+(declare-sort A_llist_a_llist_prod_set_a_llist_a_llist_prod_bool_fun_fun$ 0)
+(declare-sort A_llist_a_llist_prod_a_llist_a_llist_prod_llist_bool_fun_fun$ 0)
+(declare-sort A_llist_a_fun_a_llist_a_llist_fun_a_llist_a_llist_fun_fun_fun$ 0)
+(declare-sort A_llist_a_llist_bool_fun_fun_a_llist_a_llist_bool_fun_fun_fun$ 0)
+(declare-sort A_llist_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_set_fun$ 0)
+(declare-sort A_llist_a_llist_bool_fun_fun_a_llist_a_llist_prod_bool_fun_fun$ 0)
+(declare-sort A_llist_a_llist_prod_llist_a_llist_a_llist_prod_llist_prod_set$ 0)
+(declare-sort A_llist_a_llist_prod_bool_fun_a_llist_a_llist_prod_bool_fun_fun$ 0)
+(declare-sort A_llist_a_llist_prod_llist_a_llist_a_llist_prod_llist_bool_fun_fun$ 0)
+(declare-sort A_llist_a_llist_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_fun_fun$ 0)
+(declare-sort A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_fun_fun$ 0)
+(declare-sort A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_fun$ 0)
+(declare-sort A_llist_a_llist_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_set_fun_fun$ 0)
+(declare-sort A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_set_fun_fun$ 0)
+(declare-sort A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_set_fun$ 0)
+(declare-sort A_llist_a_llist_prod_a_llist_a_llist_prod_llist_a_llist_a_llist_prod_fun_fun$ 0)
+(declare-sort A_llist_a_llist_a_llist_a_llist_prod_fun_fun_a_llist_a_llist_bool_fun_fun_fun$ 0)
+(declare-sort A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun_a_llist_a_llist_bool_fun_fun_fun$ 0)
+(declare-sort A_llist_a_llist_bool_fun_fun_a_llist_a_llist_a_llist_a_llist_prod_set_fun_fun_fun$ 0)
+(declare-sort A_llist_a_llist_prod_set_a_llist_a_llist_a_llist_a_llist_bool_fun_fun_fun_fun_fun$ 0)
+(declare-sort A_llist_a_llist_prod_a_llist_a_llist_prod_llist_a_llist_a_llist_prod_llist_fun_fun$ 0)
+(declare-sort A_llist_a_llist_prod_set_a_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun_fun$ 0)
+(declare-sort A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun_a_llist_a_llist_bool_fun_fun_fun$ 0)
+(declare-sort A_llist_a_llist_bool_fun_fun_a_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun_fun$ 0)
+(declare-sort A_llist_a_llist_a_llist_prod_set_fun_a_llist_a_llist_a_llist_a_llist_bool_fun_fun_fun_fun_fun$ 0)
+(declare-sort A_llist_a_llist_a_llist_a_llist_prod_fun_fun_a_llist_a_llist_prod_a_llist_a_llist_prod_fun_fun$ 0)
+(declare-sort A_llist_a_llist_a_llist_prod_set_fun_a_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun_fun$ 0)
+(declare-sort A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_fun_fun$ 0)
+(declare-sort A_llist_a_llist_a_llist_a_llist_prod_fun_fun_a_llist_a_llist_a_llist_a_llist_prod_set_fun_fun_fun$ 0)
+(declare-sort A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_set_fun_fun$ 0)
+(declare-sort A_llist_a_llist_prod_a_llist_a_llist_prod_llist_bool_fun_fun_a_llist_a_llist_prod_llist_bool_fun_fun$ 0)
+(declare-sort A_llist_a_llist_a_llist_a_llist_prod_fun_fun_a_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun_fun$ 0)
+(declare-sort A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun_a_llist_a_llist_prod_a_llist_a_llist_prod_set_fun_fun$ 0)
+(declare-sort A_llist_a_llist_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_fun_fun_a_llist_a_llist_bool_fun_fun_fun$ 0)
+(declare-sort A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun_a_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun_fun$ 0)
+(declare-sort A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun_a_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun_fun$ 0)
+(declare-sort A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_bool_fun_fun$ 0)
+(declare-sort A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_fun_fun_a_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun_fun$ 0)
+(declare-sort A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_fun_fun_a_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun_fun$ 0)
+(declare-codatatypes () ((A_llist$ (lNil$) (lCons$ (lhd$ A$) (ltl$ A_llist$)))))
+(declare-datatypes () ((A_llist_a_llist_prod$ (pair$ (fst$ A_llist$) (snd$ A_llist$)))))
+(declare-codatatypes () ((A_llist_a_llist_prod_llist$ (lNil$a) (lCons$a (lhd$a A_llist_a_llist_prod$) (ltl$a A_llist_a_llist_prod_llist$)))))
+(declare-datatypes () ((A_llist_a_llist_prod_llist_a_llist_a_llist_prod_llist_prod$ (pair$a (fst$a A_llist_a_llist_prod_llist$) (snd$a A_llist_a_llist_prod_llist$)))
+  (A_llist_a_llist_prod_a_llist_a_llist_prod_prod$ (pair$b (fst$b A_llist_a_llist_prod$) (snd$b A_llist_a_llist_prod$)))))
+(declare-fun p$ () A_llist_a_llist_bool_fun_fun$)
+(declare-fun uu$ (Bool) A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun_a_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun_fun$)
+(declare-fun xs$ () A_llist$)
+(declare-fun ys$ () A_llist$)
+(declare-fun sup$ (A_llist_a_llist_prod_set$ A_llist_a_llist_prod_set$) A_llist_a_llist_prod_set$)
+(declare-fun the$ (A_llist_a_llist_prod_bool_fun$) A_llist_a_llist_prod$)
+(declare-fun uua$ (Bool) A_llist_a_llist_bool_fun_fun_a_llist_a_llist_bool_fun_fun_fun$)
+(declare-fun uub$ (A_llist_a_llist_prod_a_llist_a_llist_prod_set_fun$) A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$)
+(declare-fun uuc$ (A_llist_a_llist_prod_a_llist_a_llist_prod_fun$) A_llist_a_llist_a_llist_a_llist_prod_fun_fun$)
+(declare-fun uud$ (A_llist_a_llist_prod_a_llist_a_llist_prod_prod_bool_fun$) A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$)
+(declare-fun uue$ (A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$)
+(declare-fun uuf$ (A_llist_a_llist_prod_bool_fun$) A_llist_a_llist_bool_fun_fun$)
+(declare-fun uug$ (A_set$) A_bool_fun$)
+(declare-fun uuh$ (A_llist_a_llist_prod_a_llist_a_llist_prod_prod_set$) A_llist_a_llist_prod_a_llist_a_llist_prod_prod_bool_fun$)
+(declare-fun uui$ (A_llist_a_llist_prod_set$) A_llist_a_llist_prod_bool_fun$)
+(declare-fun uuj$ (Bool_bool_fun$) A_llist_a_llist_bool_fun_fun_a_llist_a_llist_bool_fun_fun_fun$)
+(declare-fun uuk$ (Bool_a_llist_a_llist_prod_fun$ A_llist_a_llist_bool_fun_fun$) A_llist_a_llist_a_llist_a_llist_prod_fun_fun$)
+(declare-fun uul$ (A_llist_a_llist_prod_bool_fun$) A_llist_a_llist_a_llist_a_llist_prod_fun_fun_a_llist_a_llist_bool_fun_fun_fun$)
+(declare-fun uum$ (Bool_a_llist_a_llist_prod_set_fun$) A_llist_a_llist_bool_fun_fun_a_llist_a_llist_a_llist_a_llist_prod_set_fun_fun_fun$)
+(declare-fun uun$ (A_llist_a_llist_prod_set_bool_fun$) A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun_a_llist_a_llist_bool_fun_fun_fun$)
+(declare-fun uuo$ (Bool_a_llist_a_llist_prod_bool_fun_fun$) A_llist_a_llist_bool_fun_fun_a_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun_fun$)
+(declare-fun uup$ (Bool_bool_fun$) A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun_a_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun_fun$)
+(declare-fun uuq$ (A_llist_a_llist_prod_bool_fun_bool_fun$) A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun_a_llist_a_llist_bool_fun_fun_fun$)
+(declare-fun uur$ (A_llist_a_llist_prod_a_llist_a_llist_prod_fun$ A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) A_llist_a_llist_a_llist_a_llist_prod_fun_fun$)
+(declare-fun uus$ (A_llist_a_llist_prod_set_a_llist_a_llist_prod_fun$ A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$) A_llist_a_llist_a_llist_a_llist_prod_fun_fun$)
+(declare-fun uut$ (A_llist_a_llist_bool_fun_fun$) A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_fun_fun_a_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun_fun$)
+(declare-fun uuu$ (A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$) A_llist_a_llist_a_llist_a_llist_prod_fun_fun_a_llist_a_llist_a_llist_a_llist_prod_set_fun_fun_fun$)
+(declare-fun uuv$ (A_llist_a_llist_a_llist_a_llist_prod_fun_fun$ A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) A_llist_a_llist_a_llist_a_llist_prod_fun_fun$)
+(declare-fun uuw$ (A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) A_llist_a_llist_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_fun_fun_a_llist_a_llist_bool_fun_fun_fun$)
+(declare-fun uux$ (A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_fun_fun_a_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun_fun$)
+(declare-fun uuy$ (A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$) A_llist_a_llist_a_llist_a_llist_prod_fun_fun_a_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun_fun$)
+(declare-fun uuz$ (A_llist_a_llist_bool_fun_fun$) A_llist_a_llist_a_llist_a_llist_prod_fun_fun_a_llist_a_llist_bool_fun_fun_fun$)
+(declare-fun uva$ () A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$)
+(declare-fun uvb$ () A_llist_a_llist_bool_fun_fun$)
+(declare-fun uvc$ () A_llist_a_llist_prod_llist_a_llist_a_llist_prod_fun$)
+(declare-fun uvd$ () A_llist_a_llist_prod_llist_a_llist_a_llist_prod_llist_fun$)
+(declare-fun uve$ () A_llist_a_fun$)
+(declare-fun uvf$ () A_llist_a_llist_fun$)
+(declare-fun uvg$ (A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$) A_llist_a_llist_prod_a_llist_a_llist_bool_fun_fun_fun$)
+(declare-fun uvh$ (Bool_bool_fun$) A_a_llist_bool_fun_fun_a_a_llist_bool_fun_fun_fun$)
+(declare-fun uvi$ (Bool_a_llist_fun$) A_a_llist_bool_fun_fun_a_a_llist_a_llist_fun_fun_fun$)
+(declare-fun uvj$ (Bool_a_fun$) A_a_llist_bool_fun_fun_a_a_llist_a_fun_fun_fun$)
+(declare-fun uvk$ (A_llist_bool_fun$) A_a_llist_a_llist_fun_fun_a_a_llist_bool_fun_fun_fun$)
+(declare-fun uvl$ (A_llist_a_llist_fun$) A_a_llist_a_llist_fun_fun_a_a_llist_a_llist_fun_fun_fun$)
+(declare-fun uvm$ (A_llist_a_fun$) A_a_llist_a_llist_fun_fun_a_a_llist_a_fun_fun_fun$)
+(declare-fun uvn$ (A_bool_fun$) A_a_llist_a_fun_fun_a_a_llist_bool_fun_fun_fun$)
+(declare-fun uvo$ (A_a_llist_fun$) A_a_llist_a_fun_fun_a_a_llist_a_llist_fun_fun_fun$)
+(declare-fun uvp$ (A_a_fun$) A_a_llist_a_fun_fun_a_a_llist_a_fun_fun_fun$)
+(declare-fun uvq$ () A_llist_a_llist_prod_a_llist_a_llist_prod_llist_bool_fun_fun$)
+(declare-fun uvr$ () A_a_llist_bool_fun_fun$)
+(declare-fun uvs$ () A_llist_a_llist_prod_a_llist_a_llist_prod_llist_bool_fun_fun$)
+(declare-fun uvt$ () A_a_llist_bool_fun_fun$)
+(declare-fun uvu$ () A_llist_a_llist_prod_a_llist_a_llist_prod_llist_a_llist_a_llist_prod_llist_fun_fun$)
+(declare-fun uvv$ () A_a_llist_a_llist_fun_fun$)
+(declare-fun uvw$ () A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_fun_fun$)
+(declare-fun uvx$ () A_llist_a_llist_a_llist_a_llist_prod_fun_fun$)
+(declare-fun uvy$ (A_llist_a_llist_prod_a_llist_a_llist_prod_prod_set$) A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$)
+(declare-fun uvz$ (A_llist_a_llist_prod_set$) A_llist_a_llist_bool_fun_fun$)
+(declare-fun uwa$ () A_llist_a_llist_prod_a_llist_a_llist_prod_llist_a_llist_a_llist_prod_fun_fun$)
+(declare-fun uwb$ () A_a_llist_a_fun_fun$)
+(declare-fun uwc$ (A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$) A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$)
+(declare-fun uwd$ (A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) A_llist_a_llist_a_llist_a_llist_prod_fun_fun$)
+(declare-fun uwe$ (A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$)
+(declare-fun uwf$ (A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$) A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$)
+(declare-fun uwg$ (A_llist_a_llist_bool_fun_fun$) A_llist_a_llist_bool_fun_fun$)
+(declare-fun uwh$ (A_llist_a_llist_prod_llist$) A_llist_a_llist_prod_a_llist_a_llist_prod_llist_a_llist_a_llist_prod_llist_fun_fun$)
+(declare-fun uwi$ (A_llist$) A_a_llist_a_llist_fun_fun$)
+(declare-fun uwj$ (A_llist$) A_a_llist_a_llist_fun_fun$)
+(declare-fun uwk$ (A_llist_a_llist_prod_set$) A_llist_a_llist_fun_a_llist_a_llist_bool_fun_fun_fun$)
+(declare-fun uwl$ (A_llist_bool_fun$) A_llist_a_llist_a_llist_prod_set_fun_a_llist_a_llist_a_llist_a_llist_bool_fun_fun_fun_fun_fun$)
+(declare-fun uwm$ (A_llist_bool_fun$) A_llist_a_llist_a_llist_prod_set_fun_a_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun_fun$)
+(declare-fun uwn$ (A_llist_a_llist_prod_set$) A_llist_a_llist_prod_set_a_llist_a_llist_a_llist_a_llist_bool_fun_fun_fun_fun_fun$)
+(declare-fun uwo$ (A_llist_a_llist_prod_set$) A_llist_a_llist_prod_set_a_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun_fun$)
+(declare-fun uwp$ (A_llist_a_llist_prod_bool_fun$) A_llist_a_llist_prod_bool_fun_a_llist_a_llist_prod_bool_fun_fun$)
+(declare-fun uwq$ (A_llist_a_llist_prod_set$) A_llist_a_llist_prod_set_a_llist_a_llist_prod_bool_fun_fun$)
+(declare-fun uwr$ (A_llist_a_llist_prod_bool_fun$) A_llist_a_llist_prod_bool_fun_a_llist_a_llist_prod_bool_fun_fun$)
+(declare-fun uws$ (A_llist_a_llist_prod_set$) A_llist_a_llist_prod_bool_fun_a_llist_a_llist_prod_bool_fun_fun$)
+(declare-fun uwt$ (A_llist$) A_llist_a_llist_a_llist_bool_fun_fun_fun$)
+(declare-fun lset$ (A_llist_a_llist_prod_llist$) A_llist_a_llist_prod_set$)
+(declare-fun swap$ (A_llist_a_llist_prod$) A_llist_a_llist_prod$)
+(declare-fun lnull$ () A_llist_bool_fun$)
+(declare-fun lset$a (A_llist$) A_set$)
+(declare-fun swap$a (A_llist_a_llist_prod_a_llist_a_llist_prod_prod$) A_llist_a_llist_prod_a_llist_a_llist_prod_prod$)
+(declare-fun image2$ (A_llist_a_llist_prod_set$ A_llist_a_llist_prod_a_llist_fun$ A_llist_a_llist_prod_a_llist_fun$) A_llist_a_llist_prod_set$)
+(declare-fun in_rel$ (A_llist_a_llist_prod_set$) A_llist_a_llist_bool_fun_fun$)
+(declare-fun lnull$a () A_llist_a_llist_prod_llist_bool_fun$)
+(declare-fun member$ (A_llist_a_llist_prod$) A_llist_a_llist_prod_set_bool_fun$)
+(declare-fun collect$ (A_llist_a_llist_prod_bool_fun$) A_llist_a_llist_prod_set$)
+(declare-fun fun_app$ (A_llist_a_llist_prod_llist_a_llist_a_llist_prod_llist_fun$ A_llist_a_llist_prod_llist$) A_llist_a_llist_prod_llist$)
+(declare-fun lappend$ (A_llist_a_llist_prod_llist$) A_llist_a_llist_prod_llist_a_llist_a_llist_prod_llist_fun$)
+(declare-fun less_eq$ (A_llist_a_llist_prod_set$) A_llist_a_llist_prod_set_bool_fun$)
+(declare-fun lfinite$ (A_llist_a_llist_prod_llist$) Bool)
+(declare-fun lmember$ (A_llist_a_llist_prod$) A_llist_a_llist_prod_llist_bool_fun$)
+(declare-fun lprefix$ (A_llist$) A_llist_bool_fun$)
+(declare-fun member$a (A_llist_a_llist_prod_a_llist_a_llist_prod_prod$ A_llist_a_llist_prod_a_llist_a_llist_prod_prod_set$) Bool)
+(declare-fun member$b (A$ A_set$) Bool)
+(declare-fun member$c (A_llist_a_llist_prod_llist_a_llist_a_llist_prod_llist_prod$ A_llist_a_llist_prod_llist_a_llist_a_llist_prod_llist_prod_set$) Bool)
+(declare-fun uncurry$ () A_llist_a_llist_a_llist_a_llist_prod_fun_fun_a_llist_a_llist_prod_a_llist_a_llist_prod_fun_fun$)
+(declare-fun collect$a (A_llist_a_llist_prod_a_llist_a_llist_prod_prod_bool_fun$) A_llist_a_llist_prod_a_llist_a_llist_prod_prod_set$)
+(declare-fun collect$b (A_bool_fun$) A_set$)
+(declare-fun fun_app$a (A_llist_a_llist_fun$ A_llist$) A_llist$)
+(declare-fun fun_app$b (A_llist_a_llist_prod_llist_a_llist_a_llist_prod_fun$ A_llist_a_llist_prod_llist$) A_llist_a_llist_prod$)
+(declare-fun fun_app$c (A_llist_a_fun$ A_llist$) A$)
+(declare-fun fun_app$d (A_llist_a_llist_a_llist_prod_fun$ A_llist$) A_llist_a_llist_prod$)
+(declare-fun fun_app$e (A_llist_a_llist_a_llist_a_llist_prod_fun_fun$ A_llist$) A_llist_a_llist_a_llist_prod_fun$)
+(declare-fun fun_app$f (A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_fun$ A_llist_a_llist_prod$) A_llist_a_llist_prod_a_llist_a_llist_prod_prod$)
+(declare-fun fun_app$g (A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_fun_fun$ A_llist_a_llist_prod$) A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_fun$)
+(declare-fun fun_app$h (A_llist_a_llist_prod_bool_fun$ A_llist_a_llist_prod$) Bool)
+(declare-fun fun_app$i (A_llist_a_llist_prod_set_bool_fun$ A_llist_a_llist_prod_set$) Bool)
+(declare-fun fun_app$j (A_llist_a_llist_prod_a_llist_a_llist_prod_prod_bool_fun$ A_llist_a_llist_prod_a_llist_a_llist_prod_prod$) Bool)
+(declare-fun fun_app$k (A_bool_fun$ A$) Bool)
+(declare-fun fun_app$l (A_llist_bool_fun$ A_llist$) Bool)
+(declare-fun fun_app$m (A_llist_a_llist_bool_fun_fun$ A_llist$) A_llist_bool_fun$)
+(declare-fun fun_app$n (A_llist_a_llist_a_llist_prod_set_fun$ A_llist$) A_llist_a_llist_prod_set$)
+(declare-fun fun_app$o (A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$ A_llist$) A_llist_a_llist_a_llist_prod_set_fun$)
+(declare-fun fun_app$p (A_llist_a_llist_a_llist_prod_bool_fun_fun$ A_llist$) A_llist_a_llist_prod_bool_fun$)
+(declare-fun fun_app$q (A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$ A_llist$) A_llist_a_llist_a_llist_prod_bool_fun_fun$)
+(declare-fun fun_app$r (A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$ A_llist_a_llist_prod$) A_llist_a_llist_prod_bool_fun$)
+(declare-fun fun_app$s (A_llist_a_llist_prod_set_a_llist_a_llist_prod_bool_fun_fun$ A_llist_a_llist_prod_set$) A_llist_a_llist_prod_bool_fun$)
+(declare-fun fun_app$t (A_llist_a_llist_prod_bool_fun_a_llist_a_llist_prod_bool_fun_fun$ A_llist_a_llist_prod_bool_fun$) A_llist_a_llist_prod_bool_fun$)
+(declare-fun fun_app$u (A_llist_a_llist_prod_a_llist_a_llist_prod_llist_a_llist_a_llist_prod_llist_fun_fun$ A_llist_a_llist_prod$) A_llist_a_llist_prod_llist_a_llist_a_llist_prod_llist_fun$)
+(declare-fun fun_app$v (A_a_llist_a_llist_fun_fun$ A$) A_llist_a_llist_fun$)
+(declare-fun fun_app$w (A_llist_a_llist_prod_a_llist_a_llist_prod_fun$ A_llist_a_llist_prod$) A_llist_a_llist_prod$)
+(declare-fun fun_app$x (A_llist_a_llist_prod_a_llist_a_llist_prod_set_fun$ A_llist_a_llist_prod$) A_llist_a_llist_prod_set$)
+(declare-fun fun_app$y (A_llist_a_llist_prod_a_llist_a_llist_bool_fun_fun_fun$ A_llist_a_llist_prod$) A_llist_a_llist_bool_fun_fun$)
+(declare-fun fun_app$z (A_llist_a_llist_fun_a_llist_a_llist_bool_fun_fun_fun$ A_llist_a_llist_fun$) A_llist_a_llist_bool_fun_fun$)
+(declare-fun lappend$a (A_llist$) A_llist_a_llist_fun$)
+(declare-fun less_eq$a (A_set$ A_set$) Bool)
+(declare-fun less_eq$b (A_llist_a_llist_prod_bool_fun$) A_llist_a_llist_prod_bool_fun_bool_fun$)
+(declare-fun less_eq$c (A_llist_a_llist_bool_fun_fun$ A_llist_a_llist_bool_fun_fun$) Bool)
+(declare-fun lex_prod$ (A_llist_a_llist_prod_set$ A_llist_a_llist_prod_set$) A_llist_a_llist_prod_a_llist_a_llist_prod_prod_set$)
+(declare-fun lfinite$a (A_llist$) Bool)
+(declare-fun lmember$a (A$) A_llist_bool_fun$)
+(declare-fun lprefix$a (A_llist_a_llist_prod_llist$) A_llist_a_llist_prod_llist_bool_fun$)
+(declare-fun same_fst$ (A_llist_bool_fun$ A_llist_a_llist_a_llist_prod_set_fun$) A_llist_a_llist_prod_a_llist_a_llist_prod_prod_set$)
+(declare-fun uncurry$a () A_llist_a_llist_bool_fun_fun_a_llist_a_llist_prod_bool_fun_fun$)
+(declare-fun uncurry$b () A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun_a_llist_a_llist_prod_a_llist_a_llist_prod_set_fun_fun$)
+(declare-fun uncurry$c () A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun_a_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun_fun$)
+(declare-fun uncurry$d () A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_bool_fun_fun$)
+(declare-fun uncurry$e (A_llist_a_llist_a_set_fun_fun$ A_llist_a_llist_prod$) A_set$)
+(declare-fun uncurry$f (A_llist_a_llist_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_set_fun_fun$ A_llist_a_llist_prod$) A_llist_a_llist_prod_a_llist_a_llist_prod_prod_set$)
+(declare-fun uncurry$g (A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_set_fun_fun$ A_llist_a_llist_prod_a_llist_a_llist_prod_prod$) A_llist_a_llist_prod_set$)
+(declare-fun uncurry$h (A_llist_a_llist_prod_a_llist_a_llist_prod_a_set_fun_fun$ A_llist_a_llist_prod_a_llist_a_llist_prod_prod$) A_set$)
+(declare-fun uncurry$i (A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_set_fun_fun$ A_llist_a_llist_prod_a_llist_a_llist_prod_prod$) A_llist_a_llist_prod_a_llist_a_llist_prod_prod_set$)
+(declare-fun uncurry$j (A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_fun_fun$ A_llist_a_llist_prod_a_llist_a_llist_prod_prod$) A_llist_a_llist_prod$)
+(declare-fun uncurry$k (A_llist_a_llist_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_fun_fun$ A_llist_a_llist_prod$) A_llist_a_llist_prod_a_llist_a_llist_prod_prod$)
+(declare-fun uncurry$l (A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_fun_fun$ A_llist_a_llist_prod_a_llist_a_llist_prod_prod$) A_llist_a_llist_prod_a_llist_a_llist_prod_prod$)
+(declare-fun fun_app$aa (A_llist_a_llist_a_llist_bool_fun_fun_fun$ A_llist$) A_llist_a_llist_bool_fun_fun$)
+(declare-fun fun_app$ab (A_llist_a_llist_a_llist_a_llist_prod_fun_fun_a_llist_a_llist_prod_a_llist_a_llist_prod_fun_fun$ A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) A_llist_a_llist_prod_a_llist_a_llist_prod_fun$)
+(declare-fun fun_app$ac (A_llist_a_llist_a_llist_a_llist_prod_fun_fun_a_llist_a_llist_bool_fun_fun_fun$ A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) A_llist_a_llist_bool_fun_fun$)
+(declare-fun fun_app$ad (A_llist_a_llist_bool_fun_fun_a_llist_a_llist_prod_bool_fun_fun$ A_llist_a_llist_bool_fun_fun$) A_llist_a_llist_prod_bool_fun$)
+(declare-fun fun_app$ae (A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_fun_fun_a_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun_fun$ A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_fun_fun$) A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$)
+(declare-fun fun_app$af (A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_fun_fun$ A_llist_a_llist_prod$) A_llist_a_llist_prod_a_llist_a_llist_prod_fun$)
+(declare-fun fun_app$ag (A_llist_a_llist_a_llist_a_llist_prod_fun_fun_a_llist_a_llist_a_llist_a_llist_prod_set_fun_fun_fun$ A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$)
+(declare-fun fun_app$ah (A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun_a_llist_a_llist_prod_a_llist_a_llist_prod_set_fun_fun$ A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$) A_llist_a_llist_prod_a_llist_a_llist_prod_set_fun$)
+(declare-fun fun_app$ai (A_llist_a_llist_a_llist_a_llist_prod_fun_fun_a_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun_fun$ A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$)
+(declare-fun fun_app$aj (A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun_a_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun_fun$ A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$) A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$)
+(declare-fun fun_app$ak (A_llist_a_llist_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_fun_fun_a_llist_a_llist_bool_fun_fun_fun$ A_llist_a_llist_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_fun_fun$) A_llist_a_llist_bool_fun_fun$)
+(declare-fun fun_app$al (A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_bool_fun_fun$ A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) A_llist_a_llist_prod_a_llist_a_llist_prod_prod_bool_fun$)
+(declare-fun fun_app$am (A_llist_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_fun$ A_llist$) A_llist_a_llist_prod_a_llist_a_llist_prod_prod$)
+(declare-fun fun_app$an (A_llist_a_llist_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_fun_fun$ A_llist$) A_llist_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_fun$)
+(declare-fun fun_app$ao (A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_fun_fun_a_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun_fun$ A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_fun_fun$) A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$)
+(declare-fun fun_app$ap (A_llist_a_llist_bool_fun_fun_a_llist_a_llist_bool_fun_fun_fun$ A_llist_a_llist_bool_fun_fun$) A_llist_a_llist_bool_fun_fun$)
+(declare-fun fun_app$aq (A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun_a_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun_fun$ A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$)
+(declare-fun fun_app$ar (A_a_llist_a_llist_fun_fun_a_a_llist_a_llist_fun_fun_fun$ A_a_llist_a_llist_fun_fun$) A_a_llist_a_llist_fun_fun$)
+(declare-fun fun_app$as (A_a_llist_bool_fun_fun$ A$) A_llist_bool_fun$)
+(declare-fun fun_app$at (A_a_llist_a_llist_fun_fun_a_a_llist_bool_fun_fun_fun$ A_a_llist_a_llist_fun_fun$) A_a_llist_bool_fun_fun$)
+(declare-fun fun_app$au (A_a_llist_a_fun_fun$ A$) A_llist_a_fun$)
+(declare-fun fun_app$av (A_a_llist_a_llist_fun_fun_a_a_llist_a_fun_fun_fun$ A_a_llist_a_llist_fun_fun$) A_a_llist_a_fun_fun$)
+(declare-fun fun_app$aw (A_a_llist_bool_fun_fun_a_a_llist_a_llist_fun_fun_fun$ A_a_llist_bool_fun_fun$) A_a_llist_a_llist_fun_fun$)
+(declare-fun fun_app$ax (Bool_a_llist_fun$ Bool) A_llist$)
+(declare-fun fun_app$ay (Bool_a_llist_a_llist_prod_fun$ Bool) A_llist_a_llist_prod$)
+(declare-fun fun_app$az (Bool_bool_fun$ Bool) Bool)
+(declare-fun fun_app$ba (A_a_llist_bool_fun_fun_a_a_llist_bool_fun_fun_fun$ A_a_llist_bool_fun_fun$) A_a_llist_bool_fun_fun$)
+(declare-fun fun_app$bb (A_llist_a_llist_bool_fun_fun_a_llist_a_llist_a_llist_a_llist_prod_set_fun_fun_fun$ A_llist_a_llist_bool_fun_fun$) A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$)
+(declare-fun fun_app$bc (Bool_a_llist_a_llist_prod_set_fun$ Bool) A_llist_a_llist_prod_set$)
+(declare-fun fun_app$bd (A_llist_a_llist_bool_fun_fun_a_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun_fun$ A_llist_a_llist_bool_fun_fun$) A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$)
+(declare-fun fun_app$be (Bool_a_llist_a_llist_prod_bool_fun_fun$ Bool) A_llist_a_llist_prod_bool_fun$)
+(declare-fun fun_app$bf (A_a_llist_bool_fun_fun_a_a_llist_a_fun_fun_fun$ A_a_llist_bool_fun_fun$) A_a_llist_a_fun_fun$)
+(declare-fun fun_app$bg (Bool_a_fun$ Bool) A$)
+(declare-fun fun_app$bh (A_llist_a_llist_prod_set_a_llist_a_llist_prod_fun$ A_llist_a_llist_prod_set$) A_llist_a_llist_prod$)
+(declare-fun fun_app$bi (A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun_a_llist_a_llist_bool_fun_fun_fun$ A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$) A_llist_a_llist_bool_fun_fun$)
+(declare-fun fun_app$bj (A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun_a_llist_a_llist_bool_fun_fun_fun$ A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$) A_llist_a_llist_bool_fun_fun$)
+(declare-fun fun_app$bk (A_llist_a_llist_prod_bool_fun_bool_fun$ A_llist_a_llist_prod_bool_fun$) Bool)
+(declare-fun fun_app$bl (A_a_llist_a_fun_fun_a_a_llist_a_llist_fun_fun_fun$ A_a_llist_a_fun_fun$) A_a_llist_a_llist_fun_fun$)
+(declare-fun fun_app$bm (A_a_llist_fun$ A$) A_llist$)
+(declare-fun fun_app$bn (A_a_llist_a_fun_fun_a_a_llist_bool_fun_fun_fun$ A_a_llist_a_fun_fun$) A_a_llist_bool_fun_fun$)
+(declare-fun fun_app$bo (A_a_llist_a_fun_fun_a_a_llist_a_fun_fun_fun$ A_a_llist_a_fun_fun$) A_a_llist_a_fun_fun$)
+(declare-fun fun_app$bp (A_a_fun$ A$) A$)
+(declare-fun fun_app$bq (A_llist_a_llist_prod_set_a_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun_fun$ A_llist_a_llist_prod_set$) A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$)
+(declare-fun fun_app$br (A_llist_a_llist_a_llist_a_llist_bool_fun_fun_fun_fun$ A_llist$) A_llist_a_llist_a_llist_bool_fun_fun_fun$)
+(declare-fun fun_app$bs (A_llist_a_llist_prod_set_a_llist_a_llist_a_llist_a_llist_bool_fun_fun_fun_fun_fun$ A_llist_a_llist_prod_set$) A_llist_a_llist_a_llist_a_llist_bool_fun_fun_fun_fun$)
+(declare-fun fun_app$bt (A_llist_a_llist_a_llist_prod_set_fun_a_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun_fun$ A_llist_a_llist_a_llist_prod_set_fun$) A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$)
+(declare-fun fun_app$bu (A_llist_a_llist_a_llist_prod_set_fun_a_llist_a_llist_a_llist_a_llist_bool_fun_fun_fun_fun_fun$ A_llist_a_llist_a_llist_prod_set_fun$) A_llist_a_llist_a_llist_a_llist_bool_fun_fun_fun_fun$)
+(declare-fun fun_app$bv (A_llist_a_llist_prod_a_llist_a_llist_prod_llist_a_llist_a_llist_prod_fun_fun$ A_llist_a_llist_prod$) A_llist_a_llist_prod_llist_a_llist_a_llist_prod_fun$)
+(declare-fun fun_app$bw (A_llist_a_llist_prod_llist_bool_fun$ A_llist_a_llist_prod_llist$) Bool)
+(declare-fun fun_app$bx (A_llist_a_llist_prod_a_llist_a_llist_prod_llist_bool_fun_fun$ A_llist_a_llist_prod$) A_llist_a_llist_prod_llist_bool_fun$)
+(declare-fun fun_app$by (A_llist_a_llist_prod_llist_a_llist_a_llist_prod_llist_bool_fun_fun$ A_llist_a_llist_prod_llist$) A_llist_a_llist_prod_llist_bool_fun$)
+(declare-fun fun_app$bz (A_llist_a_set_fun$ A_llist$) A_set$)
+(declare-fun fun_app$ca (A_llist_a_llist_a_set_fun_fun$ A_llist$) A_llist_a_set_fun$)
+(declare-fun fun_app$cb (A_llist_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_set_fun$ A_llist$) A_llist_a_llist_prod_a_llist_a_llist_prod_prod_set$)
+(declare-fun fun_app$cc (A_llist_a_llist_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_set_fun_fun$ A_llist$) A_llist_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_set_fun$)
+(declare-fun fun_app$cd (A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_set_fun_fun$ A_llist_a_llist_prod$) A_llist_a_llist_prod_a_llist_a_llist_prod_set_fun$)
+(declare-fun fun_app$ce (A_llist_a_llist_prod_a_set_fun$ A_llist_a_llist_prod$) A_set$)
+(declare-fun fun_app$cf (A_llist_a_llist_prod_a_llist_a_llist_prod_a_set_fun_fun$ A_llist_a_llist_prod$) A_llist_a_llist_prod_a_set_fun$)
+(declare-fun fun_app$cg (A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_set_fun$ A_llist_a_llist_prod$) A_llist_a_llist_prod_a_llist_a_llist_prod_prod_set$)
+(declare-fun fun_app$ch (A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_set_fun_fun$ A_llist_a_llist_prod$) A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_set_fun$)
+(declare-fun fun_app$ci (A_a_llist_bool_fun_fun_a_llist_bool_fun_fun$ A_a_llist_bool_fun_fun$) A_llist_bool_fun$)
+(declare-fun fun_app$cj (A_a_llist_a_llist_fun_fun_a_llist_a_llist_fun_fun$ A_a_llist_a_llist_fun_fun$) A_llist_a_llist_fun$)
+(declare-fun fun_app$ck (A_a_llist_a_fun_fun_a_llist_a_fun_fun$ A_a_llist_a_fun_fun$) A_llist_a_fun$)
+(declare-fun fun_app$cl (A_llist_a_llist_fun_a_llist_a_llist_fun_fun$ A_llist_a_llist_fun$) A_llist_a_llist_fun$)
+(declare-fun fun_app$cm (A_llist_a_fun_a_llist_a_llist_fun_a_llist_a_llist_fun_fun_fun$ A_llist_a_fun$) A_llist_a_llist_fun_a_llist_a_llist_fun_fun$)
+(declare-fun fun_app$cn (A_llist_a_llist_prod_a_llist_a_llist_prod_llist_bool_fun_fun_a_llist_a_llist_prod_llist_bool_fun_fun$ A_llist_a_llist_prod_a_llist_a_llist_prod_llist_bool_fun_fun$) A_llist_a_llist_prod_llist_bool_fun$)
+(declare-fun fun_app$co (A_a_bool_fun_fun$ A$) A_bool_fun$)
+(declare-fun fun_app$cp (A_llist_a_llist_prod_a_llist_fun$ A_llist_a_llist_prod$) A_llist$)
+(declare-fun inv_image$ (A_llist_a_llist_prod_set$ A_llist_a_llist_fun$) A_llist_a_llist_prod_set$)
+(declare-fun undefined$ () A_llist$)
+(declare-fun case_llist$ (Bool) A_a_llist_bool_fun_fun_a_llist_bool_fun_fun$)
+(declare-fun llist_all2$ (A_a_bool_fun_fun$) A_llist_a_llist_bool_fun_fun$)
+(declare-fun pred_llist$ (A_bool_fun$) A_llist_bool_fun$)
+(declare-fun undefined$a () A$)
+(declare-fun case_llist$a (A_llist$) A_a_llist_a_llist_fun_fun_a_llist_a_llist_fun_fun$)
+(declare-fun case_llist$b (A$) A_a_llist_a_fun_fun_a_llist_a_fun_fun$)
+(declare-fun case_llist$c (Bool) A_llist_a_llist_prod_a_llist_a_llist_prod_llist_bool_fun_fun_a_llist_a_llist_prod_llist_bool_fun_fun$)
+(declare-fun case_llist$d (A_llist_a_llist_prod_llist$ A_llist_a_llist_prod_a_llist_a_llist_prod_llist_a_llist_a_llist_prod_llist_fun_fun$ A_llist_a_llist_prod_llist$) A_llist_a_llist_prod_llist$)
+(declare-fun case_llist$e (A_llist_a_llist_prod$ A_llist_a_llist_prod_a_llist_a_llist_prod_llist_a_llist_a_llist_prod_fun_fun$ A_llist_a_llist_prod_llist$) A_llist_a_llist_prod$)
+(declare-fun llist_all2$a (A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) A_llist_a_llist_prod_llist_a_llist_a_llist_prod_llist_bool_fun_fun$)
+(declare-fun pred_llist$a (A_llist_a_llist_prod_bool_fun$) A_llist_a_llist_prod_llist_bool_fun$)
+(declare-fun unfold_llist$ (A_llist_a_llist_prod_llist_bool_fun$ A_llist_a_llist_prod_llist_a_llist_a_llist_prod_fun$ A_llist_a_llist_prod_llist_a_llist_a_llist_prod_llist_fun$ A_llist_a_llist_prod_llist$) A_llist_a_llist_prod_llist$)
+(declare-fun unfold_llist$a (A_llist_bool_fun$) A_llist_a_fun_a_llist_a_llist_fun_a_llist_a_llist_fun_fun_fun$)
+(declare-fun internal_split$ () A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun_a_llist_a_llist_prod_a_llist_a_llist_prod_set_fun_fun$)
+(declare-fun internal_split$a () A_llist_a_llist_a_llist_a_llist_prod_fun_fun_a_llist_a_llist_prod_a_llist_a_llist_prod_fun_fun$)
+(declare-fun internal_split$b () A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_bool_fun_fun$)
+(declare-fun internal_split$c () A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun_a_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun_fun$)
+(declare-fun internal_split$d () A_llist_a_llist_bool_fun_fun_a_llist_a_llist_prod_bool_fun_fun$)
+(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$)) (! (= (fun_app$ uvd$ ?v0) (ltl$a ?v0)) :pattern ((fun_app$ uvd$ ?v0)))) :named a0))
+(assert (! (forall ((?v0 A_llist$)) (! (= (fun_app$a uvf$ ?v0) (ltl$ ?v0)) :pattern ((fun_app$a uvf$ ?v0)))) :named a1))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$)) (! (= (fun_app$b uvc$ ?v0) (lhd$a ?v0)) :pattern ((fun_app$b uvc$ ?v0)))) :named a2))
+(assert (! (forall ((?v0 A_llist$)) (! (= (fun_app$c uve$ ?v0) (lhd$ ?v0)) :pattern ((fun_app$c uve$ ?v0)))) :named a3))
+(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$)) (! (= (fun_app$d (fun_app$e uvx$ ?v0) ?v1) (pair$ ?v0 ?v1)) :pattern ((fun_app$d (fun_app$e uvx$ ?v0) ?v1)))) :named a4))
+(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod$)) (! (= (fun_app$f (fun_app$g uvw$ ?v0) ?v1) (pair$b ?v0 ?v1)) :pattern ((fun_app$f (fun_app$g uvw$ ?v0) ?v1)))) :named a5))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_set$) (?v1 A_llist_a_llist_prod$)) (! (= (fun_app$h (uui$ ?v0) ?v1) (fun_app$i (member$ ?v1) ?v0)) :pattern ((fun_app$h (uui$ ?v0) ?v1)))) :named a6))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_prod_set$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$)) (! (= (fun_app$j (uuh$ ?v0) ?v1) (member$a ?v1 ?v0)) :pattern ((fun_app$j (uuh$ ?v0) ?v1)))) :named a7))
+(assert (! (forall ((?v0 A_set$) (?v1 A$)) (! (= (fun_app$k (uug$ ?v0) ?v1) (member$b ?v1 ?v0)) :pattern ((fun_app$k (uug$ ?v0) ?v1)))) :named a8))
+(assert (! (forall ((?v0 A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) (?v1 A_llist$) (?v2 A_llist$)) (! (= (fun_app$d (fun_app$e (uwd$ ?v0) ?v1) ?v2) (fun_app$d (fun_app$e ?v0 ?v2) ?v1)) :pattern ((fun_app$d (fun_app$e (uwd$ ?v0) ?v1) ?v2)))) :named a9))
+(assert (! (forall ((?v0 A_llist_a_llist_bool_fun_fun$) (?v1 A_llist$) (?v2 A_llist$)) (! (= (fun_app$l (fun_app$m (uwg$ ?v0) ?v1) ?v2) (fun_app$l (fun_app$m ?v0 ?v2) ?v1)) :pattern ((fun_app$l (fun_app$m (uwg$ ?v0) ?v1) ?v2)))) :named a10))
+(assert (! (forall ((?v0 A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$) (?v1 A_llist$) (?v2 A_llist$)) (! (= (fun_app$n (fun_app$o (uwc$ ?v0) ?v1) ?v2) (fun_app$n (fun_app$o ?v0 ?v2) ?v1)) :pattern ((fun_app$n (fun_app$o (uwc$ ?v0) ?v1) ?v2)))) :named a11))
+(assert (! (forall ((?v0 A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$) (?v1 A_llist$) (?v2 A_llist$)) (! (= (fun_app$p (fun_app$q (uwf$ ?v0) ?v1) ?v2) (fun_app$p (fun_app$q ?v0 ?v2) ?v1)) :pattern ((fun_app$p (fun_app$q (uwf$ ?v0) ?v1) ?v2)))) :named a12))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) (?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_prod$)) (! (= (fun_app$h (fun_app$r (uwe$ ?v0) ?v1) ?v2) (fun_app$h (fun_app$r ?v0 ?v2) ?v1)) :pattern ((fun_app$h (fun_app$r (uwe$ ?v0) ?v1) ?v2)))) :named a13))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_set$) (?v1 A_llist_a_llist_prod_set$) (?v2 A_llist_a_llist_prod$)) (! (= (fun_app$h (fun_app$s (uwq$ ?v0) ?v1) ?v2) (or (fun_app$i (member$ ?v2) ?v0) (fun_app$i (member$ ?v2) ?v1))) :pattern ((fun_app$h (fun_app$s (uwq$ ?v0) ?v1) ?v2)))) :named a14))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_set$) (?v1 A_llist_a_llist_prod_bool_fun$) (?v2 A_llist_a_llist_prod$)) (! (= (fun_app$h (fun_app$t (uws$ ?v0) ?v1) ?v2) (and (fun_app$i (member$ ?v2) ?v0) (fun_app$h ?v1 ?v2))) :pattern ((fun_app$h (fun_app$t (uws$ ?v0) ?v1) ?v2)))) :named a15))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_set$) (?v1 A_llist$) (?v2 A_llist$)) (! (= (fun_app$l (fun_app$m (uvz$ ?v0) ?v1) ?v2) (fun_app$i (member$ (pair$ ?v1 ?v2)) ?v0)) :pattern ((fun_app$l (fun_app$m (uvz$ ?v0) ?v1) ?v2)))) :named a16))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_prod_set$) (?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_prod$)) (! (= (fun_app$h (fun_app$r (uvy$ ?v0) ?v1) ?v2) (member$a (pair$b ?v1 ?v2) ?v0)) :pattern ((fun_app$h (fun_app$r (uvy$ ?v0) ?v1) ?v2)))) :named a17))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_bool_fun$) (?v1 A_llist_a_llist_prod_bool_fun$) (?v2 A_llist_a_llist_prod$)) (! (= (fun_app$h (fun_app$t (uwp$ ?v0) ?v1) ?v2) (or (fun_app$h ?v0 ?v2) (fun_app$h ?v1 ?v2))) :pattern ((fun_app$h (fun_app$t (uwp$ ?v0) ?v1) ?v2)))) :named a18))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_bool_fun$) (?v1 A_llist_a_llist_prod_bool_fun$) (?v2 A_llist_a_llist_prod$)) (! (= (fun_app$h (fun_app$t (uwr$ ?v0) ?v1) ?v2) (and (fun_app$h ?v0 ?v2) (fun_app$h ?v1 ?v2))) :pattern ((fun_app$h (fun_app$t (uwr$ ?v0) ?v1) ?v2)))) :named a19))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$) (?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_prod_llist$)) (! (= (fun_app$ (fun_app$u (uwh$ ?v0) ?v1) ?v2) (lCons$a ?v1 (fun_app$ (lappend$ ?v2) ?v0))) :pattern ((fun_app$ (fun_app$u (uwh$ ?v0) ?v1) ?v2)))) :named a20))
+(assert (! (forall ((?v0 A_llist$) (?v1 A$) (?v2 A_llist$)) (! (= (fun_app$a (fun_app$v (uwi$ ?v0) ?v1) ?v2) (lCons$ ?v1 (fun_app$a (lappend$a ?v2) ?v0))) :pattern ((fun_app$a (fun_app$v (uwi$ ?v0) ?v1) ?v2)))) :named a21))
+(assert (! (forall ((?v0 A_llist$) (?v1 A$) (?v2 A_llist$)) (! (= (fun_app$a (fun_app$v (uwj$ ?v0) ?v1) ?v2) (fun_app$a (lappend$a ?v2) ?v0)) :pattern ((fun_app$a (fun_app$v (uwj$ ?v0) ?v1) ?v2)))) :named a22))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_fun$) (?v1 A_llist$) (?v2 A_llist$)) (! (= (fun_app$d (fun_app$e (uuc$ ?v0) ?v1) ?v2) (fun_app$w ?v0 (pair$ ?v1 ?v2))) :pattern ((fun_app$d (fun_app$e (uuc$ ?v0) ?v1) ?v2)))) :named a23))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_bool_fun$) (?v1 A_llist$) (?v2 A_llist$)) (! (= (fun_app$l (fun_app$m (uuf$ ?v0) ?v1) ?v2) (fun_app$h ?v0 (pair$ ?v1 ?v2))) :pattern ((fun_app$l (fun_app$m (uuf$ ?v0) ?v1) ?v2)))) :named a24))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_set_fun$) (?v1 A_llist$) (?v2 A_llist$)) (! (= (fun_app$n (fun_app$o (uub$ ?v0) ?v1) ?v2) (fun_app$x ?v0 (pair$ ?v1 ?v2))) :pattern ((fun_app$n (fun_app$o (uub$ ?v0) ?v1) ?v2)))) :named a25))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) (?v1 A_llist$) (?v2 A_llist$)) (! (= (fun_app$p (fun_app$q (uue$ ?v0) ?v1) ?v2) (fun_app$r ?v0 (pair$ ?v1 ?v2))) :pattern ((fun_app$p (fun_app$q (uue$ ?v0) ?v1) ?v2)))) :named a26))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_prod_bool_fun$) (?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_prod$)) (! (= (fun_app$h (fun_app$r (uud$ ?v0) ?v1) ?v2) (fun_app$j ?v0 (pair$b ?v1 ?v2))) :pattern ((fun_app$h (fun_app$r (uud$ ?v0) ?v1) ?v2)))) :named a27))
+(assert (! (forall ((?v0 A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$) (?v1 A_llist_a_llist_prod$) (?v2 A_llist$) (?v3 A_llist$)) (! (= (fun_app$l (fun_app$m (fun_app$y (uvg$ ?v0) ?v1) ?v2) ?v3) (fun_app$h (fun_app$p (fun_app$q ?v0 ?v2) ?v3) ?v1)) :pattern ((fun_app$l (fun_app$m (fun_app$y (uvg$ ?v0) ?v1) ?v2) ?v3)))) :named a28))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_set$) (?v1 A_llist_a_llist_fun$) (?v2 A_llist$) (?v3 A_llist$)) (! (= (fun_app$l (fun_app$m (fun_app$z (uwk$ ?v0) ?v1) ?v2) ?v3) (fun_app$i (member$ (pair$ (fun_app$a ?v1 ?v2) (fun_app$a ?v1 ?v3))) ?v0)) :pattern ((fun_app$l (fun_app$m (fun_app$z (uwk$ ?v0) ?v1) ?v2) ?v3)))) :named a29))
+(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$) (?v2 A_llist$) (?v3 A_llist$)) (! (= (fun_app$l (fun_app$m (fun_app$aa (uwt$ ?v0) ?v1) ?v2) ?v3) (and (= ?v0 ?v2) (= ?v1 ?v3))) :pattern ((fun_app$l (fun_app$m (fun_app$aa (uwt$ ?v0) ?v1) ?v2) ?v3)))) :named a30))
+(assert (! (forall ((?v0 A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) (?v2 A_llist$) (?v3 A_llist$)) (! (= (fun_app$d (fun_app$e (uuv$ ?v0 ?v1) ?v2) ?v3) (fun_app$w (fun_app$ab uncurry$ ?v0) (fun_app$d (fun_app$e ?v1 ?v2) ?v3))) :pattern ((fun_app$d (fun_app$e (uuv$ ?v0 ?v1) ?v2) ?v3)))) :named a31))
+(assert (! (forall ((?v0 A_llist_a_llist_bool_fun_fun$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) (?v2 A_llist$) (?v3 A_llist$)) (! (= (fun_app$l (fun_app$m (fun_app$ac (uuz$ ?v0) ?v1) ?v2) ?v3) (fun_app$h (fun_app$ad uncurry$a ?v0) (fun_app$d (fun_app$e ?v1 ?v2) ?v3))) :pattern ((fun_app$l (fun_app$m (fun_app$ac (uuz$ ?v0) ?v1) ?v2) ?v3)))) :named a32))
+(assert (! (forall ((?v0 A_llist_a_llist_bool_fun_fun$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_fun_fun$) (?v2 A_llist_a_llist_prod$) (?v3 A_llist_a_llist_prod$)) (! (= (fun_app$h (fun_app$r (fun_app$ae (uut$ ?v0) ?v1) ?v2) ?v3) (fun_app$h (fun_app$ad uncurry$a ?v0) (fun_app$w (fun_app$af ?v1 ?v2) ?v3))) :pattern ((fun_app$h (fun_app$r (fun_app$ae (uut$ ?v0) ?v1) ?v2) ?v3)))) :named a33))
+(assert (! (forall ((?v0 A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) (?v2 A_llist$) (?v3 A_llist$)) (! (= (fun_app$n (fun_app$o (fun_app$ag (uuu$ ?v0) ?v1) ?v2) ?v3) (fun_app$x (fun_app$ah uncurry$b ?v0) (fun_app$d (fun_app$e ?v1 ?v2) ?v3))) :pattern ((fun_app$n (fun_app$o (fun_app$ag (uuu$ ?v0) ?v1) ?v2) ?v3)))) :named a34))
+(assert (! (forall ((?v0 A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) (?v2 A_llist$) (?v3 A_llist$)) (! (= (fun_app$p (fun_app$q (fun_app$ai (uuy$ ?v0) ?v1) ?v2) ?v3) (fun_app$r (fun_app$aj uncurry$c ?v0) (fun_app$d (fun_app$e ?v1 ?v2) ?v3))) :pattern ((fun_app$p (fun_app$q (fun_app$ai (uuy$ ?v0) ?v1) ?v2) ?v3)))) :named a35))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_fun_fun$) (?v2 A_llist$) (?v3 A_llist$)) (! (= (fun_app$l (fun_app$m (fun_app$ak (uuw$ ?v0) ?v1) ?v2) ?v3) (fun_app$j (fun_app$al uncurry$d ?v0) (fun_app$am (fun_app$an ?v1 ?v2) ?v3))) :pattern ((fun_app$l (fun_app$m (fun_app$ak (uuw$ ?v0) ?v1) ?v2) ?v3)))) :named a36))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_fun_fun$) (?v2 A_llist_a_llist_prod$) (?v3 A_llist_a_llist_prod$)) (! (= (fun_app$h (fun_app$r (fun_app$ao (uux$ ?v0) ?v1) ?v2) ?v3) (fun_app$j (fun_app$al uncurry$d ?v0) (fun_app$f (fun_app$g ?v1 ?v2) ?v3))) :pattern ((fun_app$h (fun_app$r (fun_app$ao (uux$ ?v0) ?v1) ?v2) ?v3)))) :named a37))
+(assert (! (forall ((?v0 Bool) (?v1 A_llist_a_llist_bool_fun_fun$) (?v2 A_llist$) (?v3 A_llist$)) (! (= (fun_app$l (fun_app$m (fun_app$ap (uua$ ?v0) ?v1) ?v2) ?v3) (and ?v0 (fun_app$l (fun_app$m ?v1 ?v2) ?v3))) :pattern ((fun_app$l (fun_app$m (fun_app$ap (uua$ ?v0) ?v1) ?v2) ?v3)))) :named a38))
+(assert (! (forall ((?v0 Bool) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) (?v2 A_llist_a_llist_prod$) (?v3 A_llist_a_llist_prod$)) (! (= (fun_app$h (fun_app$r (fun_app$aq (uu$ ?v0) ?v1) ?v2) ?v3) (and ?v0 (fun_app$h (fun_app$r ?v1 ?v2) ?v3))) :pattern ((fun_app$h (fun_app$r (fun_app$aq (uu$ ?v0) ?v1) ?v2) ?v3)))) :named a39))
+(assert (! (forall ((?v0 A_llist_a_llist_fun$) (?v1 A_a_llist_a_llist_fun_fun$) (?v2 A$) (?v3 A_llist$)) (! (= (fun_app$a (fun_app$v (fun_app$ar (uvl$ ?v0) ?v1) ?v2) ?v3) (fun_app$a ?v0 (fun_app$a (fun_app$v ?v1 ?v2) ?v3))) :pattern ((fun_app$a (fun_app$v (fun_app$ar (uvl$ ?v0) ?v1) ?v2) ?v3)))) :named a40))
+(assert (! (forall ((?v0 A_llist_bool_fun$) (?v1 A_a_llist_a_llist_fun_fun$) (?v2 A$) (?v3 A_llist$)) (! (= (fun_app$l (fun_app$as (fun_app$at (uvk$ ?v0) ?v1) ?v2) ?v3) (fun_app$l ?v0 (fun_app$a (fun_app$v ?v1 ?v2) ?v3))) :pattern ((fun_app$l (fun_app$as (fun_app$at (uvk$ ?v0) ?v1) ?v2) ?v3)))) :named a41))
+(assert (! (forall ((?v0 A_llist_a_fun$) (?v1 A_a_llist_a_llist_fun_fun$) (?v2 A$) (?v3 A_llist$)) (! (= (fun_app$c (fun_app$au (fun_app$av (uvm$ ?v0) ?v1) ?v2) ?v3) (fun_app$c ?v0 (fun_app$a (fun_app$v ?v1 ?v2) ?v3))) :pattern ((fun_app$c (fun_app$au (fun_app$av (uvm$ ?v0) ?v1) ?v2) ?v3)))) :named a42))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_fun$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) (?v2 A_llist$) (?v3 A_llist$)) (! (= (fun_app$d (fun_app$e (uur$ ?v0 ?v1) ?v2) ?v3) (fun_app$w ?v0 (fun_app$d (fun_app$e ?v1 ?v2) ?v3))) :pattern ((fun_app$d (fun_app$e (uur$ ?v0 ?v1) ?v2) ?v3)))) :named a43))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_bool_fun$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) (?v2 A_llist$) (?v3 A_llist$)) (! (= (fun_app$l (fun_app$m (fun_app$ac (uul$ ?v0) ?v1) ?v2) ?v3) (fun_app$h ?v0 (fun_app$d (fun_app$e ?v1 ?v2) ?v3))) :pattern ((fun_app$l (fun_app$m (fun_app$ac (uul$ ?v0) ?v1) ?v2) ?v3)))) :named a44))
+(assert (! (forall ((?v0 Bool_a_llist_fun$) (?v1 A_a_llist_bool_fun_fun$) (?v2 A$) (?v3 A_llist$)) (! (= (fun_app$a (fun_app$v (fun_app$aw (uvi$ ?v0) ?v1) ?v2) ?v3) (fun_app$ax ?v0 (fun_app$l (fun_app$as ?v1 ?v2) ?v3))) :pattern ((fun_app$a (fun_app$v (fun_app$aw (uvi$ ?v0) ?v1) ?v2) ?v3)))) :named a45))
+(assert (! (forall ((?v0 Bool_a_llist_a_llist_prod_fun$) (?v1 A_llist_a_llist_bool_fun_fun$) (?v2 A_llist$) (?v3 A_llist$)) (! (= (fun_app$d (fun_app$e (uuk$ ?v0 ?v1) ?v2) ?v3) (fun_app$ay ?v0 (fun_app$l (fun_app$m ?v1 ?v2) ?v3))) :pattern ((fun_app$d (fun_app$e (uuk$ ?v0 ?v1) ?v2) ?v3)))) :named a46))
+(assert (! (forall ((?v0 Bool_bool_fun$) (?v1 A_llist_a_llist_bool_fun_fun$) (?v2 A_llist$) (?v3 A_llist$)) (! (= (fun_app$l (fun_app$m (fun_app$ap (uuj$ ?v0) ?v1) ?v2) ?v3) (fun_app$az ?v0 (fun_app$l (fun_app$m ?v1 ?v2) ?v3))) :pattern ((fun_app$l (fun_app$m (fun_app$ap (uuj$ ?v0) ?v1) ?v2) ?v3)))) :named a47))
+(assert (! (forall ((?v0 Bool_bool_fun$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) (?v2 A_llist_a_llist_prod$) (?v3 A_llist_a_llist_prod$)) (! (= (fun_app$h (fun_app$r (fun_app$aq (uup$ ?v0) ?v1) ?v2) ?v3) (fun_app$az ?v0 (fun_app$h (fun_app$r ?v1 ?v2) ?v3))) :pattern ((fun_app$h (fun_app$r (fun_app$aq (uup$ ?v0) ?v1) ?v2) ?v3)))) :named a48))
+(assert (! (forall ((?v0 Bool_bool_fun$) (?v1 A_a_llist_bool_fun_fun$) (?v2 A$) (?v3 A_llist$)) (! (= (fun_app$l (fun_app$as (fun_app$ba (uvh$ ?v0) ?v1) ?v2) ?v3) (fun_app$az ?v0 (fun_app$l (fun_app$as ?v1 ?v2) ?v3))) :pattern ((fun_app$l (fun_app$as (fun_app$ba (uvh$ ?v0) ?v1) ?v2) ?v3)))) :named a49))
+(assert (! (forall ((?v0 Bool_a_llist_a_llist_prod_set_fun$) (?v1 A_llist_a_llist_bool_fun_fun$) (?v2 A_llist$) (?v3 A_llist$)) (! (= (fun_app$n (fun_app$o (fun_app$bb (uum$ ?v0) ?v1) ?v2) ?v3) (fun_app$bc ?v0 (fun_app$l (fun_app$m ?v1 ?v2) ?v3))) :pattern ((fun_app$n (fun_app$o (fun_app$bb (uum$ ?v0) ?v1) ?v2) ?v3)))) :named a50))
+(assert (! (forall ((?v0 Bool_a_llist_a_llist_prod_bool_fun_fun$) (?v1 A_llist_a_llist_bool_fun_fun$) (?v2 A_llist$) (?v3 A_llist$)) (! (= (fun_app$p (fun_app$q (fun_app$bd (uuo$ ?v0) ?v1) ?v2) ?v3) (fun_app$be ?v0 (fun_app$l (fun_app$m ?v1 ?v2) ?v3))) :pattern ((fun_app$p (fun_app$q (fun_app$bd (uuo$ ?v0) ?v1) ?v2) ?v3)))) :named a51))
+(assert (! (forall ((?v0 Bool_a_fun$) (?v1 A_a_llist_bool_fun_fun$) (?v2 A$) (?v3 A_llist$)) (! (= (fun_app$c (fun_app$au (fun_app$bf (uvj$ ?v0) ?v1) ?v2) ?v3) (fun_app$bg ?v0 (fun_app$l (fun_app$as ?v1 ?v2) ?v3))) :pattern ((fun_app$c (fun_app$au (fun_app$bf (uvj$ ?v0) ?v1) ?v2) ?v3)))) :named a52))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_set_a_llist_a_llist_prod_fun$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$) (?v2 A_llist$) (?v3 A_llist$)) (! (= (fun_app$d (fun_app$e (uus$ ?v0 ?v1) ?v2) ?v3) (fun_app$bh ?v0 (fun_app$n (fun_app$o ?v1 ?v2) ?v3))) :pattern ((fun_app$d (fun_app$e (uus$ ?v0 ?v1) ?v2) ?v3)))) :named a53))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_set_bool_fun$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$) (?v2 A_llist$) (?v3 A_llist$)) (! (= (fun_app$l (fun_app$m (fun_app$bi (uun$ ?v0) ?v1) ?v2) ?v3) (fun_app$i ?v0 (fun_app$n (fun_app$o ?v1 ?v2) ?v3))) :pattern ((fun_app$l (fun_app$m (fun_app$bi (uun$ ?v0) ?v1) ?v2) ?v3)))) :named a54))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_bool_fun_bool_fun$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$) (?v2 A_llist$) (?v3 A_llist$)) (! (= (fun_app$l (fun_app$m (fun_app$bj (uuq$ ?v0) ?v1) ?v2) ?v3) (fun_app$bk ?v0 (fun_app$p (fun_app$q ?v1 ?v2) ?v3))) :pattern ((fun_app$l (fun_app$m (fun_app$bj (uuq$ ?v0) ?v1) ?v2) ?v3)))) :named a55))
+(assert (! (forall ((?v0 A_a_llist_fun$) (?v1 A_a_llist_a_fun_fun$) (?v2 A$) (?v3 A_llist$)) (! (= (fun_app$a (fun_app$v (fun_app$bl (uvo$ ?v0) ?v1) ?v2) ?v3) (fun_app$bm ?v0 (fun_app$c (fun_app$au ?v1 ?v2) ?v3))) :pattern ((fun_app$a (fun_app$v (fun_app$bl (uvo$ ?v0) ?v1) ?v2) ?v3)))) :named a56))
+(assert (! (forall ((?v0 A_bool_fun$) (?v1 A_a_llist_a_fun_fun$) (?v2 A$) (?v3 A_llist$)) (! (= (fun_app$l (fun_app$as (fun_app$bn (uvn$ ?v0) ?v1) ?v2) ?v3) (fun_app$k ?v0 (fun_app$c (fun_app$au ?v1 ?v2) ?v3))) :pattern ((fun_app$l (fun_app$as (fun_app$bn (uvn$ ?v0) ?v1) ?v2) ?v3)))) :named a57))
+(assert (! (forall ((?v0 A_a_fun$) (?v1 A_a_llist_a_fun_fun$) (?v2 A$) (?v3 A_llist$)) (! (= (fun_app$c (fun_app$au (fun_app$bo (uvp$ ?v0) ?v1) ?v2) ?v3) (fun_app$bp ?v0 (fun_app$c (fun_app$au ?v1 ?v2) ?v3))) :pattern ((fun_app$c (fun_app$au (fun_app$bo (uvp$ ?v0) ?v1) ?v2) ?v3)))) :named a58))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_set$) (?v1 A_llist_a_llist_prod_set$) (?v2 A_llist$) (?v3 A_llist$)) (! (= (fun_app$p (fun_app$q (fun_app$bq (uwo$ ?v0) ?v1) ?v2) ?v3) (fun_app$ad uncurry$a (fun_app$aa (fun_app$br (fun_app$bs (uwn$ ?v0) ?v1) ?v2) ?v3))) :pattern ((fun_app$p (fun_app$q (fun_app$bq (uwo$ ?v0) ?v1) ?v2) ?v3)))) :named a59))
+(assert (! (forall ((?v0 A_llist_bool_fun$) (?v1 A_llist_a_llist_a_llist_prod_set_fun$) (?v2 A_llist$) (?v3 A_llist$)) (! (= (fun_app$p (fun_app$q (fun_app$bt (uwm$ ?v0) ?v1) ?v2) ?v3) (fun_app$ad uncurry$a (fun_app$aa (fun_app$br (fun_app$bu (uwl$ ?v0) ?v1) ?v2) ?v3))) :pattern ((fun_app$p (fun_app$q (fun_app$bt (uwm$ ?v0) ?v1) ?v2) ?v3)))) :named a60))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_set$) (?v1 A_llist_a_llist_prod_set$) (?v2 A_llist$) (?v3 A_llist$) (?v4 A_llist$) (?v5 A_llist$)) (! (= (fun_app$l (fun_app$m (fun_app$aa (fun_app$br (fun_app$bs (uwn$ ?v0) ?v1) ?v2) ?v3) ?v4) ?v5) (or (fun_app$i (member$ (pair$ ?v2 ?v4)) ?v0) (and (= ?v2 ?v4) (fun_app$i (member$ (pair$ ?v3 ?v5)) ?v1)))) :pattern ((fun_app$l (fun_app$m (fun_app$aa (fun_app$br (fun_app$bs (uwn$ ?v0) ?v1) ?v2) ?v3) ?v4) ?v5)))) :named a61))
+(assert (! (forall ((?v0 A_llist_bool_fun$) (?v1 A_llist_a_llist_a_llist_prod_set_fun$) (?v2 A_llist$) (?v3 A_llist$) (?v4 A_llist$) (?v5 A_llist$)) (! (= (fun_app$l (fun_app$m (fun_app$aa (fun_app$br (fun_app$bu (uwl$ ?v0) ?v1) ?v2) ?v3) ?v4) ?v5) (and (= ?v2 ?v4) (and (fun_app$l ?v0 ?v4) (fun_app$i (member$ (pair$ ?v3 ?v5)) (fun_app$n ?v1 ?v4))))) :pattern ((fun_app$l (fun_app$m (fun_app$aa (fun_app$br (fun_app$bu (uwl$ ?v0) ?v1) ?v2) ?v3) ?v4) ?v5)))) :named a62))
+(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod_llist$)) (! (= (fun_app$b (fun_app$bv uwa$ ?v0) ?v1) ?v0) :pattern ((fun_app$b (fun_app$bv uwa$ ?v0) ?v1)))) :named a63))
+(assert (! (forall ((?v0 A$) (?v1 A_llist$)) (! (= (fun_app$c (fun_app$au uwb$ ?v0) ?v1) ?v0) :pattern ((fun_app$c (fun_app$au uwb$ ?v0) ?v1)))) :named a64))
+(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod_llist$)) (! (= (fun_app$ (fun_app$u uvu$ ?v0) ?v1) ?v1) :pattern ((fun_app$ (fun_app$u uvu$ ?v0) ?v1)))) :named a65))
+(assert (! (forall ((?v0 A$) (?v1 A_llist$)) (! (= (fun_app$a (fun_app$v uvv$ ?v0) ?v1) ?v1) :pattern ((fun_app$a (fun_app$v uvv$ ?v0) ?v1)))) :named a66))
+(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod_llist$)) (! (= (fun_app$bw (fun_app$bx uvs$ ?v0) ?v1) false) :pattern ((fun_app$bw (fun_app$bx uvs$ ?v0) ?v1)))) :named a67))
+(assert (! (forall ((?v0 A$) (?v1 A_llist$)) (! (= (fun_app$l (fun_app$as uvt$ ?v0) ?v1) false) :pattern ((fun_app$l (fun_app$as uvt$ ?v0) ?v1)))) :named a68))
+(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$)) (! (= (fun_app$l (fun_app$m uvb$ ?v0) ?v1) true) :pattern ((fun_app$l (fun_app$m uvb$ ?v0) ?v1)))) :named a69))
+(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod_llist$)) (! (= (fun_app$bw (fun_app$bx uvq$ ?v0) ?v1) true) :pattern ((fun_app$bw (fun_app$bx uvq$ ?v0) ?v1)))) :named a70))
+(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod$)) (! (= (fun_app$h (fun_app$r uva$ ?v0) ?v1) true) :pattern ((fun_app$h (fun_app$r uva$ ?v0) ?v1)))) :named a71))
+(assert (! (forall ((?v0 A$) (?v1 A_llist$)) (! (= (fun_app$l (fun_app$as uvr$ ?v0) ?v1) true) :pattern ((fun_app$l (fun_app$as uvr$ ?v0) ?v1)))) :named a72))
+(assert (! (not (fun_app$l (lprefix$ xs$) ys$)) :named a73))
+(assert (! (fun_app$l (fun_app$m p$ xs$) ys$) :named a74))
+(assert (! (fun_app$i (member$ (pair$ xs$ ys$)) (collect$ (fun_app$ad uncurry$a p$))) :named a75))
+(assert (! (forall ((?v0 A_llist$)) (fun_app$l (lprefix$ lNil$) ?v0)) :named a76))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$) (?v1 A_llist_a_llist_prod_llist$) (?v2 A_llist_a_llist_prod$)) (=> (fun_app$bw (lprefix$a ?v0) ?v1) (fun_app$bw (lprefix$a (lCons$a ?v2 ?v0)) (lCons$a ?v2 ?v1)))) :named a77))
+(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$) (?v2 A$)) (=> (fun_app$l (lprefix$ ?v0) ?v1) (fun_app$l (lprefix$ (lCons$ ?v2 ?v0)) (lCons$ ?v2 ?v1)))) :named a78))
+(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$)) (=> (fun_app$l (fun_app$m p$ ?v0) ?v1) (and (=> (fun_app$l lnull$ ?v1) (fun_app$l lnull$ ?v0)) (=> (and (not (fun_app$l lnull$ ?v0)) (not (fun_app$l lnull$ ?v1))) (and (= (lhd$ ?v0) (lhd$ ?v1)) (or (fun_app$l (fun_app$m p$ (ltl$ ?v0)) (ltl$ ?v1)) (fun_app$l (lprefix$ (ltl$ ?v0)) (ltl$ ?v1)))))))) :named a79))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$) (?v1 A_llist_a_llist_prod_llist$)) (= (fun_app$bw (lprefix$a ?v0) ?v1) (or (exists ((?v2 A_llist_a_llist_prod_llist$)) (and (= ?v0 lNil$a) (= ?v1 ?v2))) (exists ((?v2 A_llist_a_llist_prod_llist$) (?v3 A_llist_a_llist_prod_llist$) (?v4 A_llist_a_llist_prod$)) (and (= ?v0 (lCons$a ?v4 ?v2)) (and (= ?v1 (lCons$a ?v4 ?v3)) (fun_app$bw (lprefix$a ?v2) ?v3))))))) :named a80))
+(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$)) (= (fun_app$l (lprefix$ ?v0) ?v1) (or (exists ((?v2 A_llist$)) (and (= ?v0 lNil$) (= ?v1 ?v2))) (exists ((?v2 A_llist$) (?v3 A_llist$) (?v4 A$)) (and (= ?v0 (lCons$ ?v4 ?v2)) (and (= ?v1 (lCons$ ?v4 ?v3)) (fun_app$l (lprefix$ ?v2) ?v3))))))) :named a81))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$) (?v1 A_llist_a_llist_prod_llist$)) (=> (and (fun_app$bw (lprefix$a ?v0) ?v1) (and (forall ((?v2 A_llist_a_llist_prod_llist$)) (=> (and (= ?v0 lNil$a) (= ?v1 ?v2)) false)) (forall ((?v2 A_llist_a_llist_prod_llist$) (?v3 A_llist_a_llist_prod_llist$) (?v4 A_llist_a_llist_prod$)) (=> (and (= ?v0 (lCons$a ?v4 ?v2)) (and (= ?v1 (lCons$a ?v4 ?v3)) (fun_app$bw (lprefix$a ?v2) ?v3))) false)))) false)) :named a82))
+(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$)) (=> (and (fun_app$l (lprefix$ ?v0) ?v1) (and (forall ((?v2 A_llist$)) (=> (and (= ?v0 lNil$) (= ?v1 ?v2)) false)) (forall ((?v2 A_llist$) (?v3 A_llist$) (?v4 A$)) (=> (and (= ?v0 (lCons$ ?v4 ?v2)) (and (= ?v1 (lCons$ ?v4 ?v3)) (fun_app$l (lprefix$ ?v2) ?v3))) false)))) false)) :named a83))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_llist_a_llist_a_llist_prod_llist_bool_fun_fun$) (?v1 A_llist_a_llist_prod_llist$) (?v2 A_llist_a_llist_prod_llist$)) (=> (and (fun_app$bw (fun_app$by ?v0 ?v1) ?v2) (forall ((?v3 A_llist_a_llist_prod_llist$) (?v4 A_llist_a_llist_prod_llist$)) (=> (fun_app$bw (fun_app$by ?v0 ?v3) ?v4) (or (exists ((?v5 A_llist_a_llist_prod_llist$)) (and (= ?v3 lNil$a) (= ?v4 ?v5))) (exists ((?v5 A_llist_a_llist_prod_llist$) (?v6 A_llist_a_llist_prod_llist$) (?v7 A_llist_a_llist_prod$)) (and (= ?v3 (lCons$a ?v7 ?v5)) (and (= ?v4 (lCons$a ?v7 ?v6)) (or (fun_app$bw (fun_app$by ?v0 ?v5) ?v6) (fun_app$bw (lprefix$a ?v5) ?v6))))))))) (fun_app$bw (lprefix$a ?v1) ?v2))) :named a84))
+(assert (! (forall ((?v0 A_llist_a_llist_bool_fun_fun$) (?v1 A_llist$) (?v2 A_llist$)) (=> (and (fun_app$l (fun_app$m ?v0 ?v1) ?v2) (forall ((?v3 A_llist$) (?v4 A_llist$)) (=> (fun_app$l (fun_app$m ?v0 ?v3) ?v4) (or (exists ((?v5 A_llist$)) (and (= ?v3 lNil$) (= ?v4 ?v5))) (exists ((?v5 A_llist$) (?v6 A_llist$) (?v7 A$)) (and (= ?v3 (lCons$ ?v7 ?v5)) (and (= ?v4 (lCons$ ?v7 ?v6)) (or (fun_app$l (fun_app$m ?v0 ?v5) ?v6) (fun_app$l (lprefix$ ?v5) ?v6))))))))) (fun_app$l (lprefix$ ?v1) ?v2))) :named a85))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$) (?v1 A_llist_a_llist_prod_llist$) (?v2 A_llist_a_llist_prod_llist_a_llist_a_llist_prod_llist_prod_set$)) (=> (and (member$c (pair$a ?v0 ?v1) ?v2) (forall ((?v3 A_llist_a_llist_prod_llist$) (?v4 A_llist_a_llist_prod_llist$)) (=> (member$c (pair$a ?v3 ?v4) ?v2) (or (fun_app$bw lnull$a ?v3) (exists ((?v5 A_llist_a_llist_prod$) (?v6 A_llist_a_llist_prod_llist$) (?v7 A_llist_a_llist_prod_llist$)) (and (= ?v3 (lCons$a ?v5 ?v6)) (and (= ?v4 (lCons$a ?v5 ?v7)) (or (member$c (pair$a ?v6 ?v7) ?v2) (fun_app$bw (lprefix$a ?v6) ?v7))))))))) (fun_app$bw (lprefix$a ?v0) ?v1))) :named a86))
+(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$) (?v2 A_llist_a_llist_prod_set$)) (=> (and (fun_app$i (member$ (pair$ ?v0 ?v1)) ?v2) (forall ((?v3 A_llist$) (?v4 A_llist$)) (=> (fun_app$i (member$ (pair$ ?v3 ?v4)) ?v2) (or (fun_app$l lnull$ ?v3) (exists ((?v5 A$) (?v6 A_llist$) (?v7 A_llist$)) (and (= ?v3 (lCons$ ?v5 ?v6)) (and (= ?v4 (lCons$ ?v5 ?v7)) (or (fun_app$i (member$ (pair$ ?v6 ?v7)) ?v2) (fun_app$l (lprefix$ ?v6) ?v7))))))))) (fun_app$l (lprefix$ ?v0) ?v1))) :named a87))
+(assert (! (forall ((?v0 A$) (?v1 A_llist$) (?v2 A$) (?v3 A_llist$)) (= (= (lCons$ ?v0 ?v1) (lCons$ ?v2 ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3)))) :named a88))
+(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod_llist$) (?v2 A_llist_a_llist_prod$) (?v3 A_llist_a_llist_prod_llist$)) (= (= (lCons$a ?v0 ?v1) (lCons$a ?v2 ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3)))) :named a89))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$)) (=> (not (fun_app$bw lnull$a ?v0)) (= (lCons$a (lhd$a ?v0) (ltl$a ?v0)) ?v0))) :named a90))
+(assert (! (forall ((?v0 A_llist$)) (=> (not (fun_app$l lnull$ ?v0)) (= (lCons$ (lhd$ ?v0) (ltl$ ?v0)) ?v0))) :named a91))
+(assert (! (forall ((?v0 A_llist$)) (= (not (= ?v0 lNil$)) (exists ((?v1 A$) (?v2 A_llist$)) (= ?v0 (lCons$ ?v1 ?v2))))) :named a92))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$)) (= (not (= ?v0 lNil$a)) (exists ((?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_prod_llist$)) (= ?v0 (lCons$a ?v1 ?v2))))) :named a93))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$)) (= (not (fun_app$bw lnull$a ?v0)) (exists ((?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_prod_llist$)) (= ?v0 (lCons$a ?v1 ?v2))))) :named a94))
+(assert (! (forall ((?v0 A_llist$)) (= (not (fun_app$l lnull$ ?v0)) (exists ((?v1 A$) (?v2 A_llist$)) (= ?v0 (lCons$ ?v1 ?v2))))) :named a95))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$)) (! (= (fun_app$bw lnull$a ?v0) (= ?v0 lNil$a)) :pattern ((fun_app$bw lnull$a ?v0)))) :named a96))
+(assert (! (forall ((?v0 A_llist$)) (! (= (fun_app$l lnull$ ?v0) (= ?v0 lNil$)) :pattern ((fun_app$l lnull$ ?v0)))) :named a97))
+(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod_llist$)) (! (= (lhd$a (lCons$a ?v0 ?v1)) ?v0) :pattern ((lCons$a ?v0 ?v1)))) :named a98))
+(assert (! (forall ((?v0 A$) (?v1 A_llist$)) (! (= (lhd$ (lCons$ ?v0 ?v1)) ?v0) :pattern ((lCons$ ?v0 ?v1)))) :named a99))
+(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod_llist$)) (! (= (ltl$a (lCons$a ?v0 ?v1)) ?v1) :pattern ((lCons$a ?v0 ?v1)))) :named a100))
+(assert (! (forall ((?v0 A$) (?v1 A_llist$)) (! (= (ltl$ (lCons$ ?v0 ?v1)) ?v1) :pattern ((lCons$ ?v0 ?v1)))) :named a101))
+(assert (! (= (ltl$a lNil$a) lNil$a) :named a102))
+(assert (! (= (ltl$ lNil$) lNil$) :named a103))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$)) (=> (and (=> (= ?v0 lNil$a) false) (=> (= ?v0 (lCons$a (lhd$a ?v0) (ltl$a ?v0))) false)) false)) :named a104))
+(assert (! (forall ((?v0 A_llist$)) (=> (and (=> (= ?v0 lNil$) false) (=> (= ?v0 (lCons$ (lhd$ ?v0) (ltl$ ?v0))) false)) false)) :named a105))
+(assert (! (forall ((?v0 A_llist$)) (=> (and (=> (= ?v0 lNil$) false) (forall ((?v1 A$) (?v2 A_llist$)) (=> (= ?v0 (lCons$ ?v1 ?v2)) false))) false)) :named a106))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$)) (=> (and (=> (= ?v0 lNil$a) false) (forall ((?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_prod_llist$)) (=> (= ?v0 (lCons$a ?v1 ?v2)) false))) false)) :named a107))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$) (?v1 A_llist_a_llist_prod_llist$)) (=> (and (=> (and (fun_app$bw lnull$a ?v0) (fun_app$bw lnull$a ?v1)) false) (=> (or (not (fun_app$bw lnull$a ?v0)) (not (fun_app$bw lnull$a ?v1))) false)) false)) :named a108))
+(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$)) (=> (and (=> (and (fun_app$l lnull$ ?v0) (fun_app$l lnull$ ?v1)) false) (=> (or (not (fun_app$l lnull$ ?v0)) (not (fun_app$l lnull$ ?v1))) false)) false)) :named a109))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$)) (=> (and (=> (fun_app$bw lnull$a ?v0) false) (=> (not (fun_app$bw lnull$a ?v0)) false)) false)) :named a110))
+(assert (! (forall ((?v0 A_llist$)) (=> (and (=> (fun_app$l lnull$ ?v0) false) (=> (not (fun_app$l lnull$ ?v0)) false)) false)) :named a111))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$) (?v1 A_llist_a_llist_prod_llist$)) (=> (and (= (fun_app$bw lnull$a ?v0) (fun_app$bw lnull$a ?v1)) (=> (and (not (fun_app$bw lnull$a ?v0)) (not (fun_app$bw lnull$a ?v1))) (and (= (lhd$a ?v0) (lhd$a ?v1)) (= (ltl$a ?v0) (ltl$a ?v1))))) (= ?v0 ?v1))) :named a112))
+(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$)) (=> (and (= (fun_app$l lnull$ ?v0) (fun_app$l lnull$ ?v1)) (=> (and (not (fun_app$l lnull$ ?v0)) (not (fun_app$l lnull$ ?v1))) (and (= (lhd$ ?v0) (lhd$ ?v1)) (= (ltl$ ?v0) (ltl$ ?v1))))) (= ?v0 ?v1))) :named a113))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$) (?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_prod_llist$)) (=> (= ?v0 (lCons$a ?v1 ?v2)) (and (not (= ?v0 lNil$a)) (and (= (lhd$a ?v0) ?v1) (= (ltl$a ?v0) ?v2))))) :named a114))
+(assert (! (forall ((?v0 A_llist$) (?v1 A$) (?v2 A_llist$)) (=> (= ?v0 (lCons$ ?v1 ?v2)) (and (not (= ?v0 lNil$)) (and (= (lhd$ ?v0) ?v1) (= (ltl$ ?v0) ?v2))))) :named a115))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$) (?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_prod_llist$)) (=> (= ?v0 (lCons$a ?v1 ?v2)) (not (fun_app$bw lnull$a ?v0)))) :named a116))
+(assert (! (forall ((?v0 A_llist$) (?v1 A$) (?v2 A_llist$)) (=> (= ?v0 (lCons$ ?v1 ?v2)) (not (fun_app$l lnull$ ?v0)))) :named a117))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$)) (=> (= ?v0 lNil$a) (fun_app$bw lnull$a ?v0))) :named a118))
+(assert (! (forall ((?v0 A_llist$)) (=> (= ?v0 lNil$) (fun_app$l lnull$ ?v0))) :named a119))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$)) (=> (fun_app$bw lnull$a ?v0) (= ?v0 lNil$a))) :named a120))
+(assert (! (forall ((?v0 A_llist$)) (=> (fun_app$l lnull$ ?v0) (= ?v0 lNil$))) :named a121))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$)) (=> (fun_app$bw lnull$a ?v0) (fun_app$bw lnull$a (ltl$a ?v0)))) :named a122))
+(assert (! (forall ((?v0 A_llist$)) (=> (fun_app$l lnull$ ?v0) (fun_app$l lnull$ (ltl$ ?v0)))) :named a123))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_llist_a_llist_a_llist_prod_llist_bool_fun_fun$) (?v1 A_llist_a_llist_prod_llist$) (?v2 A_llist_a_llist_prod_llist$)) (=> (and (fun_app$bw (fun_app$by ?v0 ?v1) ?v2) (forall ((?v3 A_llist_a_llist_prod_llist$) (?v4 A_llist_a_llist_prod_llist$)) (=> (fun_app$bw (fun_app$by ?v0 ?v3) ?v4) (and (= (fun_app$bw lnull$a ?v3) (fun_app$bw lnull$a ?v4)) (=> (and (not (fun_app$bw lnull$a ?v3)) (not (fun_app$bw lnull$a ?v4))) (and (= (lhd$a ?v3) (lhd$a ?v4)) (or (fun_app$bw (fun_app$by ?v0 (ltl$a ?v3)) (ltl$a ?v4)) (= (ltl$a ?v3) (ltl$a ?v4))))))))) (= ?v1 ?v2))) :named a124))
+(assert (! (forall ((?v0 A_llist_a_llist_bool_fun_fun$) (?v1 A_llist$) (?v2 A_llist$)) (=> (and (fun_app$l (fun_app$m ?v0 ?v1) ?v2) (forall ((?v3 A_llist$) (?v4 A_llist$)) (=> (fun_app$l (fun_app$m ?v0 ?v3) ?v4) (and (= (fun_app$l lnull$ ?v3) (fun_app$l lnull$ ?v4)) (=> (and (not (fun_app$l lnull$ ?v3)) (not (fun_app$l lnull$ ?v4))) (and (= (lhd$ ?v3) (lhd$ ?v4)) (or (fun_app$l (fun_app$m ?v0 (ltl$ ?v3)) (ltl$ ?v4)) (= (ltl$ ?v3) (ltl$ ?v4))))))))) (= ?v1 ?v2))) :named a125))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_llist_a_llist_a_llist_prod_llist_bool_fun_fun$) (?v1 A_llist_a_llist_prod_llist$) (?v2 A_llist_a_llist_prod_llist$)) (=> (and (fun_app$bw (fun_app$by ?v0 ?v1) ?v2) (forall ((?v3 A_llist_a_llist_prod_llist$) (?v4 A_llist_a_llist_prod_llist$)) (=> (fun_app$bw (fun_app$by ?v0 ?v3) ?v4) (and (= (fun_app$bw lnull$a ?v3) (fun_app$bw lnull$a ?v4)) (=> (and (not (fun_app$bw lnull$a ?v3)) (not (fun_app$bw lnull$a ?v4))) (and (= (lhd$a ?v3) (lhd$a ?v4)) (fun_app$bw (fun_app$by ?v0 (ltl$a ?v3)) (ltl$a ?v4)))))))) (= ?v1 ?v2))) :named a126))
+(assert (! (forall ((?v0 A_llist_a_llist_bool_fun_fun$) (?v1 A_llist$) (?v2 A_llist$)) (=> (and (fun_app$l (fun_app$m ?v0 ?v1) ?v2) (forall ((?v3 A_llist$) (?v4 A_llist$)) (=> (fun_app$l (fun_app$m ?v0 ?v3) ?v4) (and (= (fun_app$l lnull$ ?v3) (fun_app$l lnull$ ?v4)) (=> (and (not (fun_app$l lnull$ ?v3)) (not (fun_app$l lnull$ ?v4))) (and (= (lhd$ ?v3) (lhd$ ?v4)) (fun_app$l (fun_app$m ?v0 (ltl$ ?v3)) (ltl$ ?v4)))))))) (= ?v1 ?v2))) :named a127))
+(assert (! (forall ((?v0 A$) (?v1 A_llist$)) (not (= lNil$ (lCons$ ?v0 ?v1)))) :named a128))
+(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod_llist$)) (not (= lNil$a (lCons$a ?v0 ?v1)))) :named a129))
+(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod_llist$)) (not (fun_app$bw lnull$a (lCons$a ?v0 ?v1)))) :named a130))
+(assert (! (forall ((?v0 A$) (?v1 A_llist$)) (not (fun_app$l lnull$ (lCons$ ?v0 ?v1)))) :named a131))
+(assert (! (fun_app$bw lnull$a lNil$a) :named a132))
+(assert (! (fun_app$l lnull$ lNil$) :named a133))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$)) (=> (forall ((?v2 A_llist_a_llist_prod$) (?v3 A_llist_a_llist_prod$)) (=> (= ?v0 (pair$b ?v2 ?v3)) (fun_app$h (fun_app$r ?v1 ?v2) ?v3))) (fun_app$j (fun_app$al uncurry$d ?v1) ?v0))) :named a134))
+(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_bool_fun_fun$)) (=> (forall ((?v2 A_llist$) (?v3 A_llist$)) (=> (= ?v0 (pair$ ?v2 ?v3)) (fun_app$l (fun_app$m ?v1 ?v2) ?v3))) (fun_app$h (fun_app$ad uncurry$a ?v1) ?v0))) :named a135))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) (?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_prod$)) (=> (fun_app$h (fun_app$r ?v0 ?v1) ?v2) (fun_app$j (fun_app$al uncurry$d ?v0) (pair$b ?v1 ?v2)))) :named a136))
+(assert (! (forall ((?v0 A_llist_a_llist_bool_fun_fun$) (?v1 A_llist$) (?v2 A_llist$)) (=> (fun_app$l (fun_app$m ?v0 ?v1) ?v2) (fun_app$h (fun_app$ad uncurry$a ?v0) (pair$ ?v1 ?v2)))) :named a137))
+(assert (! (forall ((?v0 A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$) (?v1 A_llist$) (?v2 A_llist$)) (! (= (fun_app$x (fun_app$ah uncurry$b ?v0) (pair$ ?v1 ?v2)) (fun_app$n (fun_app$o ?v0 ?v1) ?v2)) :pattern ((fun_app$x (fun_app$ah uncurry$b ?v0) (pair$ ?v1 ?v2))))) :named a138))
+(assert (! (forall ((?v0 A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) (?v1 A_llist$) (?v2 A_llist$)) (! (= (fun_app$w (fun_app$ab uncurry$ ?v0) (pair$ ?v1 ?v2)) (fun_app$d (fun_app$e ?v0 ?v1) ?v2)) :pattern ((fun_app$w (fun_app$ab uncurry$ ?v0) (pair$ ?v1 ?v2))))) :named a139))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) (?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_prod$)) (! (= (fun_app$j (fun_app$al uncurry$d ?v0) (pair$b ?v1 ?v2)) (fun_app$h (fun_app$r ?v0 ?v1) ?v2)) :pattern ((fun_app$j (fun_app$al uncurry$d ?v0) (pair$b ?v1 ?v2))))) :named a140))
+(assert (! (forall ((?v0 A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$) (?v1 A_llist$) (?v2 A_llist$)) (! (= (fun_app$r (fun_app$aj uncurry$c ?v0) (pair$ ?v1 ?v2)) (fun_app$p (fun_app$q ?v0 ?v1) ?v2)) :pattern ((fun_app$r (fun_app$aj uncurry$c ?v0) (pair$ ?v1 ?v2))))) :named a141))
+(assert (! (forall ((?v0 A_llist_a_llist_bool_fun_fun$) (?v1 A_llist$) (?v2 A_llist$)) (! (= (fun_app$h (fun_app$ad uncurry$a ?v0) (pair$ ?v1 ?v2)) (fun_app$l (fun_app$m ?v0 ?v1) ?v2)) :pattern ((fun_app$h (fun_app$ad uncurry$a ?v0) (pair$ ?v1 ?v2))))) :named a142))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) (?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_prod$)) (=> (fun_app$h (fun_app$r ?v0 ?v1) ?v2) (fun_app$j (fun_app$al uncurry$d ?v0) (pair$b ?v1 ?v2)))) :named a143))
+(assert (! (forall ((?v0 A_llist_a_llist_bool_fun_fun$) (?v1 A_llist$) (?v2 A_llist$)) (=> (fun_app$l (fun_app$m ?v0 ?v1) ?v2) (fun_app$h (fun_app$ad uncurry$a ?v0) (pair$ ?v1 ?v2)))) :named a144))
+(assert (! (forall ((?v0 Bool) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) (?v2 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$)) (= (fun_app$j (fun_app$al uncurry$d (fun_app$aq (uu$ ?v0) ?v1)) ?v2) (and ?v0 (fun_app$j (fun_app$al uncurry$d ?v1) ?v2)))) :named a145))
+(assert (! (forall ((?v0 Bool) (?v1 A_llist_a_llist_bool_fun_fun$) (?v2 A_llist_a_llist_prod$)) (= (fun_app$h (fun_app$ad uncurry$a (fun_app$ap (uua$ ?v0) ?v1)) ?v2) (and ?v0 (fun_app$h (fun_app$ad uncurry$a ?v1) ?v2)))) :named a146))
+(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_prod$) (?v3 A_llist_a_llist_prod$)) (= (= (pair$b ?v0 ?v1) (pair$b ?v2 ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3)))) :named a147))
+(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$) (?v2 A_llist$) (?v3 A_llist$)) (= (= (pair$ ?v0 ?v1) (pair$ ?v2 ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3)))) :named a148))
+(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_prod$) (?v3 A_llist_a_llist_prod$)) (= (= (pair$b ?v0 ?v1) (pair$b ?v2 ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3)))) :named a149))
+(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$) (?v2 A_llist$) (?v3 A_llist$)) (= (= (pair$ ?v0 ?v1) (pair$ ?v2 ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3)))) :named a150))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) (?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_prod$)) (=> (fun_app$j (fun_app$al uncurry$d ?v0) (pair$b ?v1 ?v2)) (fun_app$h (fun_app$r ?v0 ?v1) ?v2))) :named a151))
+(assert (! (forall ((?v0 A_llist_a_llist_bool_fun_fun$) (?v1 A_llist$) (?v2 A_llist$)) (=> (fun_app$h (fun_app$ad uncurry$a ?v0) (pair$ ?v1 ?v2)) (fun_app$l (fun_app$m ?v0 ?v1) ?v2))) :named a152))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$)) (=> (and (fun_app$j (fun_app$al uncurry$d ?v0) ?v1) (forall ((?v2 A_llist_a_llist_prod$) (?v3 A_llist_a_llist_prod$)) (=> (and (= ?v1 (pair$b ?v2 ?v3)) (fun_app$h (fun_app$r ?v0 ?v2) ?v3)) false))) false)) :named a153))
+(assert (! (forall ((?v0 A_llist_a_llist_bool_fun_fun$) (?v1 A_llist_a_llist_prod$)) (=> (and (fun_app$h (fun_app$ad uncurry$a ?v0) ?v1) (forall ((?v2 A_llist$) (?v3 A_llist$)) (=> (and (= ?v1 (pair$ ?v2 ?v3)) (fun_app$l (fun_app$m ?v0 ?v2) ?v3)) false))) false)) :named a154))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_set_fun$)) (= (fun_app$ah uncurry$b (uub$ ?v0)) ?v0)) :named a155))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_fun$)) (= (fun_app$ab uncurry$ (uuc$ ?v0)) ?v0)) :named a156))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_prod_bool_fun$)) (= (fun_app$al uncurry$d (uud$ ?v0)) ?v0)) :named a157))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$)) (= (fun_app$aj uncurry$c (uue$ ?v0)) ?v0)) :named a158))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_bool_fun$)) (= (fun_app$ad uncurry$a (uuf$ ?v0)) ?v0)) :named a159))
+(assert (! (forall ((?v0 A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_set_fun$)) (=> (forall ((?v2 A_llist$) (?v3 A_llist$)) (= (fun_app$n (fun_app$o ?v0 ?v2) ?v3) (fun_app$x ?v1 (pair$ ?v2 ?v3)))) (= (fun_app$ah uncurry$b ?v0) ?v1))) :named a160))
+(assert (! (forall ((?v0 A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_fun$)) (=> (forall ((?v2 A_llist$) (?v3 A_llist$)) (= (fun_app$d (fun_app$e ?v0 ?v2) ?v3) (fun_app$w ?v1 (pair$ ?v2 ?v3)))) (= (fun_app$ab uncurry$ ?v0) ?v1))) :named a161))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_prod_bool_fun$)) (=> (forall ((?v2 A_llist_a_llist_prod$) (?v3 A_llist_a_llist_prod$)) (= (fun_app$h (fun_app$r ?v0 ?v2) ?v3) (fun_app$j ?v1 (pair$b ?v2 ?v3)))) (= (fun_app$al uncurry$d ?v0) ?v1))) :named a162))
+(assert (! (forall ((?v0 A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$)) (=> (forall ((?v2 A_llist$) (?v3 A_llist$)) (= (fun_app$p (fun_app$q ?v0 ?v2) ?v3) (fun_app$r ?v1 (pair$ ?v2 ?v3)))) (= (fun_app$aj uncurry$c ?v0) ?v1))) :named a163))
+(assert (! (forall ((?v0 A_llist_a_llist_bool_fun_fun$) (?v1 A_llist_a_llist_prod_bool_fun$)) (=> (forall ((?v2 A_llist$) (?v3 A_llist$)) (= (fun_app$l (fun_app$m ?v0 ?v2) ?v3) (fun_app$h ?v1 (pair$ ?v2 ?v3)))) (= (fun_app$ad uncurry$a ?v0) ?v1))) :named a164))
+(assert (! (forall ((?v0 A$) (?v1 A_llist_a_llist_a_set_fun_fun$) (?v2 A_llist$) (?v3 A_llist$)) (=> (member$b ?v0 (fun_app$bz (fun_app$ca ?v1 ?v2) ?v3)) (member$b ?v0 (uncurry$e ?v1 (pair$ ?v2 ?v3))))) :named a165))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_set_fun_fun$) (?v2 A_llist$) (?v3 A_llist$)) (=> (member$a ?v0 (fun_app$cb (fun_app$cc ?v1 ?v2) ?v3)) (member$a ?v0 (uncurry$f ?v1 (pair$ ?v2 ?v3))))) :named a166))
+(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_set_fun_fun$) (?v2 A_llist_a_llist_prod$) (?v3 A_llist_a_llist_prod$)) (=> (fun_app$i (member$ ?v0) (fun_app$x (fun_app$cd ?v1 ?v2) ?v3)) (fun_app$i (member$ ?v0) (uncurry$g ?v1 (pair$b ?v2 ?v3))))) :named a167))
+(assert (! (forall ((?v0 A$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_a_set_fun_fun$) (?v2 A_llist_a_llist_prod$) (?v3 A_llist_a_llist_prod$)) (=> (member$b ?v0 (fun_app$ce (fun_app$cf ?v1 ?v2) ?v3)) (member$b ?v0 (uncurry$h ?v1 (pair$b ?v2 ?v3))))) :named a168))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_set_fun_fun$) (?v2 A_llist_a_llist_prod$) (?v3 A_llist_a_llist_prod$)) (=> (member$a ?v0 (fun_app$cg (fun_app$ch ?v1 ?v2) ?v3)) (member$a ?v0 (uncurry$i ?v1 (pair$b ?v2 ?v3))))) :named a169))
+(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$) (?v2 A_llist$) (?v3 A_llist$)) (=> (fun_app$i (member$ ?v0) (fun_app$n (fun_app$o ?v1 ?v2) ?v3)) (fun_app$i (member$ ?v0) (fun_app$x (fun_app$ah uncurry$b ?v1) (pair$ ?v2 ?v3))))) :named a170))
+(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A$) (?v2 A_llist_a_llist_a_set_fun_fun$)) (=> (forall ((?v3 A_llist$) (?v4 A_llist$)) (=> (= ?v0 (pair$ ?v3 ?v4)) (member$b ?v1 (fun_app$bz (fun_app$ca ?v2 ?v3) ?v4)))) (member$b ?v1 (uncurry$e ?v2 ?v0)))) :named a171))
+(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$) (?v2 A_llist_a_llist_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_set_fun_fun$)) (=> (forall ((?v3 A_llist$) (?v4 A_llist$)) (=> (= ?v0 (pair$ ?v3 ?v4)) (member$a ?v1 (fun_app$cb (fun_app$cc ?v2 ?v3) ?v4)))) (member$a ?v1 (uncurry$f ?v2 ?v0)))) :named a172))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$) (?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_set_fun_fun$)) (=> (forall ((?v3 A_llist_a_llist_prod$) (?v4 A_llist_a_llist_prod$)) (=> (= ?v0 (pair$b ?v3 ?v4)) (fun_app$i (member$ ?v1) (fun_app$x (fun_app$cd ?v2 ?v3) ?v4)))) (fun_app$i (member$ ?v1) (uncurry$g ?v2 ?v0)))) :named a173))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$) (?v1 A$) (?v2 A_llist_a_llist_prod_a_llist_a_llist_prod_a_set_fun_fun$)) (=> (forall ((?v3 A_llist_a_llist_prod$) (?v4 A_llist_a_llist_prod$)) (=> (= ?v0 (pair$b ?v3 ?v4)) (member$b ?v1 (fun_app$ce (fun_app$cf ?v2 ?v3) ?v4)))) (member$b ?v1 (uncurry$h ?v2 ?v0)))) :named a174))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$) (?v2 A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_set_fun_fun$)) (=> (forall ((?v3 A_llist_a_llist_prod$) (?v4 A_llist_a_llist_prod$)) (=> (= ?v0 (pair$b ?v3 ?v4)) (member$a ?v1 (fun_app$cg (fun_app$ch ?v2 ?v3) ?v4)))) (member$a ?v1 (uncurry$i ?v2 ?v0)))) :named a175))
+(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$)) (=> (forall ((?v3 A_llist$) (?v4 A_llist$)) (=> (= ?v0 (pair$ ?v3 ?v4)) (fun_app$i (member$ ?v1) (fun_app$n (fun_app$o ?v2 ?v3) ?v4)))) (fun_app$i (member$ ?v1) (fun_app$x (fun_app$ah uncurry$b ?v2) ?v0)))) :named a176))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_prod_bool_fun$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_prod_bool_fun$)) (=> (forall ((?v2 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$)) (= (fun_app$j ?v0 ?v2) (fun_app$j ?v1 ?v2))) (= (collect$a ?v0) (collect$a ?v1)))) :named a177))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_bool_fun$) (?v1 A_llist_a_llist_prod_bool_fun$)) (=> (forall ((?v2 A_llist_a_llist_prod$)) (= (fun_app$h ?v0 ?v2) (fun_app$h ?v1 ?v2))) (= (collect$ ?v0) (collect$ ?v1)))) :named a178))
+(assert (! (forall ((?v0 A_set$)) (= (collect$b (uug$ ?v0)) ?v0)) :named a179))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_prod_set$)) (= (collect$a (uuh$ ?v0)) ?v0)) :named a180))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_set$)) (= (collect$ (uui$ ?v0)) ?v0)) :named a181))
+(assert (! (forall ((?v0 A$) (?v1 A_bool_fun$)) (= (member$b ?v0 (collect$b ?v1)) (fun_app$k ?v1 ?v0))) :named a182))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_prod_bool_fun$)) (= (member$a ?v0 (collect$a ?v1)) (fun_app$j ?v1 ?v0))) :named a183))
+(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod_bool_fun$)) (= (fun_app$i (member$ ?v0) (collect$ ?v1)) (fun_app$h ?v1 ?v0))) :named a184))
+(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$) (?v2 A_llist_a_llist_prod$)) (=> (forall ((?v3 A_llist$) (?v4 A_llist$)) (=> (= (pair$ ?v3 ?v4) ?v0) (fun_app$h (fun_app$p (fun_app$q ?v1 ?v3) ?v4) ?v2))) (fun_app$h (fun_app$r (fun_app$aj uncurry$c ?v1) ?v0) ?v2))) :named a185))
+(assert (! (forall ((?v0 A$) (?v1 A_llist_a_llist_a_set_fun_fun$) (?v2 A_llist_a_llist_prod$)) (=> (and (member$b ?v0 (uncurry$e ?v1 ?v2)) (forall ((?v3 A_llist$) (?v4 A_llist$)) (=> (and (= ?v2 (pair$ ?v3 ?v4)) (member$b ?v0 (fun_app$bz (fun_app$ca ?v1 ?v3) ?v4))) false))) false)) :named a186))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_set_fun_fun$) (?v2 A_llist_a_llist_prod$)) (=> (and (member$a ?v0 (uncurry$f ?v1 ?v2)) (forall ((?v3 A_llist$) (?v4 A_llist$)) (=> (and (= ?v2 (pair$ ?v3 ?v4)) (member$a ?v0 (fun_app$cb (fun_app$cc ?v1 ?v3) ?v4))) false))) false)) :named a187))
+(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_set_fun_fun$) (?v2 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$)) (=> (and (fun_app$i (member$ ?v0) (uncurry$g ?v1 ?v2)) (forall ((?v3 A_llist_a_llist_prod$) (?v4 A_llist_a_llist_prod$)) (=> (and (= ?v2 (pair$b ?v3 ?v4)) (fun_app$i (member$ ?v0) (fun_app$x (fun_app$cd ?v1 ?v3) ?v4))) false))) false)) :named a188))
+(assert (! (forall ((?v0 A$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_a_set_fun_fun$) (?v2 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$)) (=> (and (member$b ?v0 (uncurry$h ?v1 ?v2)) (forall ((?v3 A_llist_a_llist_prod$) (?v4 A_llist_a_llist_prod$)) (=> (and (= ?v2 (pair$b ?v3 ?v4)) (member$b ?v0 (fun_app$ce (fun_app$cf ?v1 ?v3) ?v4))) false))) false)) :named a189))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_set_fun_fun$) (?v2 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$)) (=> (and (member$a ?v0 (uncurry$i ?v1 ?v2)) (forall ((?v3 A_llist_a_llist_prod$) (?v4 A_llist_a_llist_prod$)) (=> (and (= ?v2 (pair$b ?v3 ?v4)) (member$a ?v0 (fun_app$cg (fun_app$ch ?v1 ?v3) ?v4))) false))) false)) :named a190))
+(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$) (?v2 A_llist_a_llist_prod$)) (=> (and (fun_app$i (member$ ?v0) (fun_app$x (fun_app$ah uncurry$b ?v1) ?v2)) (forall ((?v3 A_llist$) (?v4 A_llist$)) (=> (and (= ?v2 (pair$ ?v3 ?v4)) (fun_app$i (member$ ?v0) (fun_app$n (fun_app$o ?v1 ?v3) ?v4))) false))) false)) :named a191))
+(assert (! (forall ((?v0 A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$) (?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_prod$)) (=> (and (fun_app$h (fun_app$r (fun_app$aj uncurry$c ?v0) ?v1) ?v2) (forall ((?v3 A_llist$) (?v4 A_llist$)) (=> (and (= ?v1 (pair$ ?v3 ?v4)) (fun_app$h (fun_app$p (fun_app$q ?v0 ?v3) ?v4) ?v2)) false))) false)) :named a192))
+(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$) (?v2 A_llist_a_llist_prod$)) (=> (forall ((?v3 A_llist$) (?v4 A_llist$)) (=> (= (pair$ ?v3 ?v4) ?v0) (fun_app$h (fun_app$p (fun_app$q ?v1 ?v3) ?v4) ?v2))) (fun_app$h (fun_app$r (fun_app$aj uncurry$c ?v1) ?v0) ?v2))) :named a193))
+(assert (! (forall ((?v0 A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$) (?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_prod$)) (=> (and (fun_app$h (fun_app$r (fun_app$aj uncurry$c ?v0) ?v1) ?v2) (forall ((?v3 A_llist$) (?v4 A_llist$)) (=> (and (= ?v1 (pair$ ?v3 ?v4)) (fun_app$h (fun_app$p (fun_app$q ?v0 ?v3) ?v4) ?v2)) false))) false)) :named a194))
+(assert (! (forall ((?v0 A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$) (?v1 A_llist$) (?v2 A_llist$) (?v3 A_llist_a_llist_prod$)) (=> (fun_app$h (fun_app$r (fun_app$aj uncurry$c ?v0) (pair$ ?v1 ?v2)) ?v3) (fun_app$h (fun_app$p (fun_app$q ?v0 ?v1) ?v2) ?v3))) :named a195))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$)) (exists ((?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_prod$)) (= ?v0 (pair$b ?v1 ?v2)))) :named a196))
+(assert (! (forall ((?v0 A_llist_a_llist_prod$)) (exists ((?v1 A_llist$) (?v2 A_llist$)) (= ?v0 (pair$ ?v1 ?v2)))) :named a197))
+(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_prod$) (?v3 A_llist_a_llist_prod$)) (=> (and (= (pair$b ?v0 ?v1) (pair$b ?v2 ?v3)) (=> (and (= ?v0 ?v2) (= ?v1 ?v3)) false)) false)) :named a198))
+(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$) (?v2 A_llist$) (?v3 A_llist$)) (=> (and (= (pair$ ?v0 ?v1) (pair$ ?v2 ?v3)) (=> (and (= ?v0 ?v2) (= ?v1 ?v3)) false)) false)) :named a199))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_prod_bool_fun$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$)) (=> (forall ((?v2 A_llist_a_llist_prod$) (?v3 A_llist_a_llist_prod$)) (fun_app$j ?v0 (pair$b ?v2 ?v3))) (fun_app$j ?v0 ?v1))) :named a200))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_bool_fun$) (?v1 A_llist_a_llist_prod$)) (=> (forall ((?v2 A_llist$) (?v3 A_llist$)) (fun_app$h ?v0 (pair$ ?v2 ?v3))) (fun_app$h ?v0 ?v1))) :named a201))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$)) (=> (forall ((?v1 A_llist_a_llist_prod$) (?v2 A_llist$) (?v3 A_llist$)) (=> (= ?v0 (pair$b ?v1 (pair$ ?v2 ?v3))) false)) false)) :named a202))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_prod_bool_fun$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$)) (=> (forall ((?v2 A_llist_a_llist_prod$) (?v3 A_llist$) (?v4 A_llist$)) (fun_app$j ?v0 (pair$b ?v2 (pair$ ?v3 ?v4)))) (fun_app$j ?v0 ?v1))) :named a203))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$)) (=> (forall ((?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_prod$)) (=> (= ?v0 (pair$b ?v1 ?v2)) false)) false)) :named a204))
+(assert (! (forall ((?v0 A_llist_a_llist_prod$)) (=> (forall ((?v1 A_llist$) (?v2 A_llist$)) (=> (= ?v0 (pair$ ?v1 ?v2)) false)) false)) :named a205))
+(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$)) (=> (= ?v0 ?v1) (= (fun_app$x (fun_app$ah uncurry$b ?v2) ?v0) (fun_app$x (fun_app$ah uncurry$b ?v2) ?v1)))) :named a206))
+(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_a_llist_a_llist_prod_fun_fun$)) (=> (= ?v0 ?v1) (= (fun_app$w (fun_app$ab uncurry$ ?v2) ?v0) (fun_app$w (fun_app$ab uncurry$ ?v2) ?v1)))) :named a207))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$) (?v2 A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$)) (=> (= ?v0 ?v1) (= (fun_app$j (fun_app$al uncurry$d ?v2) ?v0) (fun_app$j (fun_app$al uncurry$d ?v2) ?v1)))) :named a208))
+(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$)) (=> (= ?v0 ?v1) (= (fun_app$r (fun_app$aj uncurry$c ?v2) ?v0) (fun_app$r (fun_app$aj uncurry$c ?v2) ?v1)))) :named a209))
+(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_bool_fun_fun$)) (=> (= ?v0 ?v1) (= (fun_app$h (fun_app$ad uncurry$a ?v2) ?v0) (fun_app$h (fun_app$ad uncurry$a ?v2) ?v1)))) :named a210))
+(assert (! (forall ((?v0 Bool_bool_fun$) (?v1 A_llist_a_llist_bool_fun_fun$) (?v2 A_llist_a_llist_prod$)) (= (fun_app$az ?v0 (fun_app$h (fun_app$ad uncurry$a ?v1) ?v2)) (fun_app$h (fun_app$ad uncurry$a (fun_app$ap (uuj$ ?v0) ?v1)) ?v2))) :named a211))
+(assert (! (forall ((?v0 Bool_a_llist_a_llist_prod_fun$) (?v1 A_llist_a_llist_bool_fun_fun$) (?v2 A_llist_a_llist_prod$)) (= (fun_app$ay ?v0 (fun_app$h (fun_app$ad uncurry$a ?v1) ?v2)) (fun_app$w (fun_app$ab uncurry$ (uuk$ ?v0 ?v1)) ?v2))) :named a212))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_bool_fun$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) (?v2 A_llist_a_llist_prod$)) (= (fun_app$h ?v0 (fun_app$w (fun_app$ab uncurry$ ?v1) ?v2)) (fun_app$h (fun_app$ad uncurry$a (fun_app$ac (uul$ ?v0) ?v1)) ?v2))) :named a213))
+(assert (! (forall ((?v0 Bool_a_llist_a_llist_prod_set_fun$) (?v1 A_llist_a_llist_bool_fun_fun$) (?v2 A_llist_a_llist_prod$)) (= (fun_app$bc ?v0 (fun_app$h (fun_app$ad uncurry$a ?v1) ?v2)) (fun_app$x (fun_app$ah uncurry$b (fun_app$bb (uum$ ?v0) ?v1)) ?v2))) :named a214))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_set_bool_fun$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$) (?v2 A_llist_a_llist_prod$)) (= (fun_app$i ?v0 (fun_app$x (fun_app$ah uncurry$b ?v1) ?v2)) (fun_app$h (fun_app$ad uncurry$a (fun_app$bi (uun$ ?v0) ?v1)) ?v2))) :named a215))
+(assert (! (forall ((?v0 Bool_a_llist_a_llist_prod_bool_fun_fun$) (?v1 A_llist_a_llist_bool_fun_fun$) (?v2 A_llist_a_llist_prod$)) (= (fun_app$be ?v0 (fun_app$h (fun_app$ad uncurry$a ?v1) ?v2)) (fun_app$r (fun_app$aj uncurry$c (fun_app$bd (uuo$ ?v0) ?v1)) ?v2))) :named a216))
+(assert (! (forall ((?v0 Bool_bool_fun$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) (?v2 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$)) (= (fun_app$az ?v0 (fun_app$j (fun_app$al uncurry$d ?v1) ?v2)) (fun_app$j (fun_app$al uncurry$d (fun_app$aq (uup$ ?v0) ?v1)) ?v2))) :named a217))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_bool_fun_bool_fun$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$) (?v2 A_llist_a_llist_prod$)) (= (fun_app$bk ?v0 (fun_app$r (fun_app$aj uncurry$c ?v1) ?v2)) (fun_app$h (fun_app$ad uncurry$a (fun_app$bj (uuq$ ?v0) ?v1)) ?v2))) :named a218))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_fun$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) (?v2 A_llist_a_llist_prod$)) (= (fun_app$w ?v0 (fun_app$w (fun_app$ab uncurry$ ?v1) ?v2)) (fun_app$w (fun_app$ab uncurry$ (uur$ ?v0 ?v1)) ?v2))) :named a219))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_set_a_llist_a_llist_prod_fun$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$) (?v2 A_llist_a_llist_prod$)) (= (fun_app$bh ?v0 (fun_app$x (fun_app$ah uncurry$b ?v1) ?v2)) (fun_app$w (fun_app$ab uncurry$ (uus$ ?v0 ?v1)) ?v2))) :named a220))
+(assert (! (forall ((?v0 Bool_bool_fun$) (?v1 A_llist_a_llist_bool_fun_fun$) (?v2 A_llist_a_llist_prod$)) (= (fun_app$az ?v0 (fun_app$h (fun_app$ad uncurry$a ?v1) ?v2)) (fun_app$h (fun_app$ad uncurry$a (fun_app$ap (uuj$ ?v0) ?v1)) ?v2))) :named a221))
+(assert (! (forall ((?v0 Bool_a_llist_a_llist_prod_fun$) (?v1 A_llist_a_llist_bool_fun_fun$) (?v2 A_llist_a_llist_prod$)) (= (fun_app$ay ?v0 (fun_app$h (fun_app$ad uncurry$a ?v1) ?v2)) (fun_app$w (fun_app$ab uncurry$ (uuk$ ?v0 ?v1)) ?v2))) :named a222))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_bool_fun$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) (?v2 A_llist_a_llist_prod$)) (= (fun_app$h ?v0 (fun_app$w (fun_app$ab uncurry$ ?v1) ?v2)) (fun_app$h (fun_app$ad uncurry$a (fun_app$ac (uul$ ?v0) ?v1)) ?v2))) :named a223))
+(assert (! (forall ((?v0 Bool_a_llist_a_llist_prod_set_fun$) (?v1 A_llist_a_llist_bool_fun_fun$) (?v2 A_llist_a_llist_prod$)) (= (fun_app$bc ?v0 (fun_app$h (fun_app$ad uncurry$a ?v1) ?v2)) (fun_app$x (fun_app$ah uncurry$b (fun_app$bb (uum$ ?v0) ?v1)) ?v2))) :named a224))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_set_bool_fun$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$) (?v2 A_llist_a_llist_prod$)) (= (fun_app$i ?v0 (fun_app$x (fun_app$ah uncurry$b ?v1) ?v2)) (fun_app$h (fun_app$ad uncurry$a (fun_app$bi (uun$ ?v0) ?v1)) ?v2))) :named a225))
+(assert (! (forall ((?v0 Bool_a_llist_a_llist_prod_bool_fun_fun$) (?v1 A_llist_a_llist_bool_fun_fun$) (?v2 A_llist_a_llist_prod$)) (= (fun_app$be ?v0 (fun_app$h (fun_app$ad uncurry$a ?v1) ?v2)) (fun_app$r (fun_app$aj uncurry$c (fun_app$bd (uuo$ ?v0) ?v1)) ?v2))) :named a226))
+(assert (! (forall ((?v0 Bool_bool_fun$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) (?v2 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$)) (= (fun_app$az ?v0 (fun_app$j (fun_app$al uncurry$d ?v1) ?v2)) (fun_app$j (fun_app$al uncurry$d (fun_app$aq (uup$ ?v0) ?v1)) ?v2))) :named a227))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_bool_fun_bool_fun$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$) (?v2 A_llist_a_llist_prod$)) (= (fun_app$bk ?v0 (fun_app$r (fun_app$aj uncurry$c ?v1) ?v2)) (fun_app$h (fun_app$ad uncurry$a (fun_app$bj (uuq$ ?v0) ?v1)) ?v2))) :named a228))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_fun$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) (?v2 A_llist_a_llist_prod$)) (= (fun_app$w ?v0 (fun_app$w (fun_app$ab uncurry$ ?v1) ?v2)) (fun_app$w (fun_app$ab uncurry$ (uur$ ?v0 ?v1)) ?v2))) :named a229))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_set_a_llist_a_llist_prod_fun$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$) (?v2 A_llist_a_llist_prod$)) (= (fun_app$bh ?v0 (fun_app$x (fun_app$ah uncurry$b ?v1) ?v2)) (fun_app$w (fun_app$ab uncurry$ (uus$ ?v0 ?v1)) ?v2))) :named a230))
+(assert (! (forall ((?v0 A_llist_a_llist_bool_fun_fun$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_fun_fun$) (?v2 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$)) (= (fun_app$h (fun_app$ad uncurry$a ?v0) (uncurry$j ?v1 ?v2)) (fun_app$j (fun_app$al uncurry$d (fun_app$ae (uut$ ?v0) ?v1)) ?v2))) :named a231))
+(assert (! (forall ((?v0 A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) (?v2 A_llist_a_llist_prod$)) (= (fun_app$x (fun_app$ah uncurry$b ?v0) (fun_app$w (fun_app$ab uncurry$ ?v1) ?v2)) (fun_app$x (fun_app$ah uncurry$b (fun_app$ag (uuu$ ?v0) ?v1)) ?v2))) :named a232))
+(assert (! (forall ((?v0 A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) (?v2 A_llist_a_llist_prod$)) (= (fun_app$w (fun_app$ab uncurry$ ?v0) (fun_app$w (fun_app$ab uncurry$ ?v1) ?v2)) (fun_app$w (fun_app$ab uncurry$ (uuv$ ?v0 ?v1)) ?v2))) :named a233))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_fun_fun$) (?v2 A_llist_a_llist_prod$)) (= (fun_app$j (fun_app$al uncurry$d ?v0) (uncurry$k ?v1 ?v2)) (fun_app$h (fun_app$ad uncurry$a (fun_app$ak (uuw$ ?v0) ?v1)) ?v2))) :named a234))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_a_llist_a_llist_prod_prod_fun_fun$) (?v2 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$)) (= (fun_app$j (fun_app$al uncurry$d ?v0) (uncurry$l ?v1 ?v2)) (fun_app$j (fun_app$al uncurry$d (fun_app$ao (uux$ ?v0) ?v1)) ?v2))) :named a235))
+(assert (! (forall ((?v0 A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) (?v2 A_llist_a_llist_prod$)) (= (fun_app$r (fun_app$aj uncurry$c ?v0) (fun_app$w (fun_app$ab uncurry$ ?v1) ?v2)) (fun_app$r (fun_app$aj uncurry$c (fun_app$ai (uuy$ ?v0) ?v1)) ?v2))) :named a236))
+(assert (! (forall ((?v0 A_llist_a_llist_bool_fun_fun$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) (?v2 A_llist_a_llist_prod$)) (= (fun_app$h (fun_app$ad uncurry$a ?v0) (fun_app$w (fun_app$ab uncurry$ ?v1) ?v2)) (fun_app$h (fun_app$ad uncurry$a (fun_app$ac (uuz$ ?v0) ?v1)) ?v2))) :named a237))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$)) (= (= ?v0 ?v0) (fun_app$j (fun_app$al uncurry$d uva$) ?v0))) :named a238))
+(assert (! (forall ((?v0 A_llist_a_llist_prod$)) (= (= ?v0 ?v0) (fun_app$h (fun_app$ad uncurry$a uvb$) ?v0))) :named a239))
+(assert (! (forall ((?v0 A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$) (?v1 A_llist$) (?v2 A_llist$)) (! (= (fun_app$x (fun_app$ah uncurry$b ?v0) (pair$ ?v1 ?v2)) (fun_app$n (fun_app$o ?v0 ?v1) ?v2)) :pattern ((fun_app$x (fun_app$ah uncurry$b ?v0) (pair$ ?v1 ?v2))))) :named a240))
+(assert (! (forall ((?v0 A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) (?v1 A_llist$) (?v2 A_llist$)) (! (= (fun_app$w (fun_app$ab uncurry$ ?v0) (pair$ ?v1 ?v2)) (fun_app$d (fun_app$e ?v0 ?v1) ?v2)) :pattern ((fun_app$w (fun_app$ab uncurry$ ?v0) (pair$ ?v1 ?v2))))) :named a241))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) (?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_prod$)) (! (= (fun_app$j (fun_app$al uncurry$d ?v0) (pair$b ?v1 ?v2)) (fun_app$h (fun_app$r ?v0 ?v1) ?v2)) :pattern ((fun_app$j (fun_app$al uncurry$d ?v0) (pair$b ?v1 ?v2))))) :named a242))
+(assert (! (forall ((?v0 A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$) (?v1 A_llist$) (?v2 A_llist$)) (! (= (fun_app$r (fun_app$aj uncurry$c ?v0) (pair$ ?v1 ?v2)) (fun_app$p (fun_app$q ?v0 ?v1) ?v2)) :pattern ((fun_app$r (fun_app$aj uncurry$c ?v0) (pair$ ?v1 ?v2))))) :named a243))
+(assert (! (forall ((?v0 A_llist_a_llist_bool_fun_fun$) (?v1 A_llist$) (?v2 A_llist$)) (! (= (fun_app$h (fun_app$ad uncurry$a ?v0) (pair$ ?v1 ?v2)) (fun_app$l (fun_app$m ?v0 ?v1) ?v2)) :pattern ((fun_app$h (fun_app$ad uncurry$a ?v0) (pair$ ?v1 ?v2))))) :named a244))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$)) (=> (and (fun_app$j (fun_app$al uncurry$d ?v0) ?v1) (forall ((?v2 A_llist_a_llist_prod$) (?v3 A_llist_a_llist_prod$)) (=> (and (= ?v1 (pair$b ?v2 ?v3)) (fun_app$h (fun_app$r ?v0 ?v2) ?v3)) false))) false)) :named a245))
+(assert (! (forall ((?v0 A_llist_a_llist_bool_fun_fun$) (?v1 A_llist_a_llist_prod$)) (=> (and (fun_app$h (fun_app$ad uncurry$a ?v0) ?v1) (forall ((?v2 A_llist$) (?v3 A_llist$)) (=> (and (= ?v1 (pair$ ?v2 ?v3)) (fun_app$l (fun_app$m ?v0 ?v2) ?v3)) false))) false)) :named a246))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$)) (=> (forall ((?v2 A_llist_a_llist_prod$) (?v3 A_llist_a_llist_prod$)) (=> (= ?v0 (pair$b ?v2 ?v3)) (fun_app$h (fun_app$r ?v1 ?v2) ?v3))) (fun_app$j (fun_app$al uncurry$d ?v1) ?v0))) :named a247))
+(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_bool_fun_fun$)) (=> (forall ((?v2 A_llist$) (?v3 A_llist$)) (=> (= ?v0 (pair$ ?v2 ?v3)) (fun_app$l (fun_app$m ?v1 ?v2) ?v3))) (fun_app$h (fun_app$ad uncurry$a ?v1) ?v0))) :named a248))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_set_bool_fun$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$) (?v2 A_llist_a_llist_prod$)) (=> (and (fun_app$i ?v0 (fun_app$x (fun_app$ah uncurry$b ?v1) ?v2)) (forall ((?v3 A_llist$) (?v4 A_llist$)) (=> (and (= ?v2 (pair$ ?v3 ?v4)) (fun_app$i ?v0 (fun_app$n (fun_app$o ?v1 ?v3) ?v4))) false))) false)) :named a249))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_bool_fun$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) (?v2 A_llist_a_llist_prod$)) (=> (and (fun_app$h ?v0 (fun_app$w (fun_app$ab uncurry$ ?v1) ?v2)) (forall ((?v3 A_llist$) (?v4 A_llist$)) (=> (and (= ?v2 (pair$ ?v3 ?v4)) (fun_app$h ?v0 (fun_app$d (fun_app$e ?v1 ?v3) ?v4))) false))) false)) :named a250))
+(assert (! (forall ((?v0 Bool_bool_fun$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) (?v2 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$)) (=> (and (fun_app$az ?v0 (fun_app$j (fun_app$al uncurry$d ?v1) ?v2)) (forall ((?v3 A_llist_a_llist_prod$) (?v4 A_llist_a_llist_prod$)) (=> (and (= ?v2 (pair$b ?v3 ?v4)) (fun_app$az ?v0 (fun_app$h (fun_app$r ?v1 ?v3) ?v4))) false))) false)) :named a251))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_bool_fun_bool_fun$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$) (?v2 A_llist_a_llist_prod$)) (=> (and (fun_app$bk ?v0 (fun_app$r (fun_app$aj uncurry$c ?v1) ?v2)) (forall ((?v3 A_llist$) (?v4 A_llist$)) (=> (and (= ?v2 (pair$ ?v3 ?v4)) (fun_app$bk ?v0 (fun_app$p (fun_app$q ?v1 ?v3) ?v4))) false))) false)) :named a252))
+(assert (! (forall ((?v0 Bool_bool_fun$) (?v1 A_llist_a_llist_bool_fun_fun$) (?v2 A_llist_a_llist_prod$)) (=> (and (fun_app$az ?v0 (fun_app$h (fun_app$ad uncurry$a ?v1) ?v2)) (forall ((?v3 A_llist$) (?v4 A_llist$)) (=> (and (= ?v2 (pair$ ?v3 ?v4)) (fun_app$az ?v0 (fun_app$l (fun_app$m ?v1 ?v3) ?v4))) false))) false)) :named a253))
+(assert (! (forall ((?v0 Bool_bool_fun$) (?v1 Bool) (?v2 A_a_llist_bool_fun_fun$) (?v3 A_llist$)) (= (fun_app$az ?v0 (fun_app$l (fun_app$ci (case_llist$ ?v1) ?v2) ?v3)) (and (=> (= ?v3 lNil$) (fun_app$az ?v0 ?v1)) (=> (= ?v3 (lCons$ (lhd$ ?v3) (ltl$ ?v3))) (fun_app$az ?v0 (fun_app$l (fun_app$as ?v2 (lhd$ ?v3)) (ltl$ ?v3))))))) :named a254))
+(assert (! (forall ((?v0 A_llist_bool_fun$) (?v1 A_llist$) (?v2 A_a_llist_a_llist_fun_fun$) (?v3 A_llist$)) (= (fun_app$l ?v0 (fun_app$a (fun_app$cj (case_llist$a ?v1) ?v2) ?v3)) (and (=> (= ?v3 lNil$) (fun_app$l ?v0 ?v1)) (=> (= ?v3 (lCons$ (lhd$ ?v3) (ltl$ ?v3))) (fun_app$l ?v0 (fun_app$a (fun_app$v ?v2 (lhd$ ?v3)) (ltl$ ?v3))))))) :named a255))
+(assert (! (forall ((?v0 A_bool_fun$) (?v1 A$) (?v2 A_a_llist_a_fun_fun$) (?v3 A_llist$)) (= (fun_app$k ?v0 (fun_app$c (fun_app$ck (case_llist$b ?v1) ?v2) ?v3)) (and (=> (= ?v3 lNil$) (fun_app$k ?v0 ?v1)) (=> (= ?v3 (lCons$ (lhd$ ?v3) (ltl$ ?v3))) (fun_app$k ?v0 (fun_app$c (fun_app$au ?v2 (lhd$ ?v3)) (ltl$ ?v3))))))) :named a256))
+(assert (! (forall ((?v0 Bool_bool_fun$) (?v1 Bool) (?v2 A_a_llist_bool_fun_fun$) (?v3 A_llist$)) (= (fun_app$az ?v0 (fun_app$l (fun_app$ci (case_llist$ ?v1) ?v2) ?v3)) (not (or (and (= ?v3 lNil$) (not (fun_app$az ?v0 ?v1))) (and (= ?v3 (lCons$ (lhd$ ?v3) (ltl$ ?v3))) (not (fun_app$az ?v0 (fun_app$l (fun_app$as ?v2 (lhd$ ?v3)) (ltl$ ?v3))))))))) :named a257))
+(assert (! (forall ((?v0 A_llist_bool_fun$) (?v1 A_llist$) (?v2 A_a_llist_a_llist_fun_fun$) (?v3 A_llist$)) (= (fun_app$l ?v0 (fun_app$a (fun_app$cj (case_llist$a ?v1) ?v2) ?v3)) (not (or (and (= ?v3 lNil$) (not (fun_app$l ?v0 ?v1))) (and (= ?v3 (lCons$ (lhd$ ?v3) (ltl$ ?v3))) (not (fun_app$l ?v0 (fun_app$a (fun_app$v ?v2 (lhd$ ?v3)) (ltl$ ?v3))))))))) :named a258))
+(assert (! (forall ((?v0 A_bool_fun$) (?v1 A$) (?v2 A_a_llist_a_fun_fun$) (?v3 A_llist$)) (= (fun_app$k ?v0 (fun_app$c (fun_app$ck (case_llist$b ?v1) ?v2) ?v3)) (not (or (and (= ?v3 lNil$) (not (fun_app$k ?v0 ?v1))) (and (= ?v3 (lCons$ (lhd$ ?v3) (ltl$ ?v3))) (not (fun_app$k ?v0 (fun_app$c (fun_app$au ?v2 (lhd$ ?v3)) (ltl$ ?v3))))))))) :named a259))
+(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$) (?v2 A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$) (?v3 A_llist_a_llist_prod$)) (=> (and (forall ((?v4 A_llist$) (?v5 A_llist$)) (=> (= (pair$ ?v4 ?v5) ?v0) (= (fun_app$n (fun_app$o ?v1 ?v4) ?v5) (fun_app$n (fun_app$o ?v2 ?v4) ?v5)))) (= ?v3 ?v0)) (= (fun_app$x (fun_app$ah uncurry$b ?v1) ?v3) (fun_app$x (fun_app$ah uncurry$b ?v2) ?v0)))) :named a260))
+(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) (?v2 A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) (?v3 A_llist_a_llist_prod$)) (=> (and (forall ((?v4 A_llist$) (?v5 A_llist$)) (=> (= (pair$ ?v4 ?v5) ?v0) (= (fun_app$d (fun_app$e ?v1 ?v4) ?v5) (fun_app$d (fun_app$e ?v2 ?v4) ?v5)))) (= ?v3 ?v0)) (= (fun_app$w (fun_app$ab uncurry$ ?v1) ?v3) (fun_app$w (fun_app$ab uncurry$ ?v2) ?v0)))) :named a261))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) (?v2 A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) (?v3 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$)) (=> (and (forall ((?v4 A_llist_a_llist_prod$) (?v5 A_llist_a_llist_prod$)) (=> (= (pair$b ?v4 ?v5) ?v0) (= (fun_app$h (fun_app$r ?v1 ?v4) ?v5) (fun_app$h (fun_app$r ?v2 ?v4) ?v5)))) (= ?v3 ?v0)) (= (fun_app$j (fun_app$al uncurry$d ?v1) ?v3) (fun_app$j (fun_app$al uncurry$d ?v2) ?v0)))) :named a262))
+(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$) (?v2 A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$) (?v3 A_llist_a_llist_prod$)) (=> (and (forall ((?v4 A_llist$) (?v5 A_llist$)) (=> (= (pair$ ?v4 ?v5) ?v0) (= (fun_app$p (fun_app$q ?v1 ?v4) ?v5) (fun_app$p (fun_app$q ?v2 ?v4) ?v5)))) (= ?v3 ?v0)) (= (fun_app$r (fun_app$aj uncurry$c ?v1) ?v3) (fun_app$r (fun_app$aj uncurry$c ?v2) ?v0)))) :named a263))
+(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_bool_fun_fun$) (?v2 A_llist_a_llist_bool_fun_fun$) (?v3 A_llist_a_llist_prod$)) (=> (and (forall ((?v4 A_llist$) (?v5 A_llist$)) (=> (= (pair$ ?v4 ?v5) ?v0) (= (fun_app$l (fun_app$m ?v1 ?v4) ?v5) (fun_app$l (fun_app$m ?v2 ?v4) ?v5)))) (= ?v3 ?v0)) (= (fun_app$h (fun_app$ad uncurry$a ?v1) ?v3) (fun_app$h (fun_app$ad uncurry$a ?v2) ?v0)))) :named a264))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$)) (= (unfold_llist$ lnull$a uvc$ uvd$ ?v0) ?v0)) :named a265))
+(assert (! (forall ((?v0 A_llist$)) (= (fun_app$a (fun_app$cl (fun_app$cm (unfold_llist$a lnull$) uve$) uvf$) ?v0) ?v0)) :named a266))
+(assert (! (forall ((?v0 Bool) (?v1 A_a_llist_bool_fun_fun$) (?v2 A_llist$)) (! (= (fun_app$l (fun_app$ci (case_llist$ ?v0) ?v1) ?v2) (ite (fun_app$l lnull$ ?v2) ?v0 (fun_app$l (fun_app$as ?v1 (lhd$ ?v2)) (ltl$ ?v2)))) :pattern ((fun_app$l (fun_app$ci (case_llist$ ?v0) ?v1) ?v2)))) :named a267))
+(assert (! (forall ((?v0 A_llist$) (?v1 A_a_llist_a_llist_fun_fun$) (?v2 A_llist$)) (! (= (fun_app$a (fun_app$cj (case_llist$a ?v0) ?v1) ?v2) (ite (fun_app$l lnull$ ?v2) ?v0 (fun_app$a (fun_app$v ?v1 (lhd$ ?v2)) (ltl$ ?v2)))) :pattern ((fun_app$a (fun_app$cj (case_llist$a ?v0) ?v1) ?v2)))) :named a268))
+(assert (! (forall ((?v0 A$) (?v1 A_a_llist_a_fun_fun$) (?v2 A_llist$)) (! (= (fun_app$c (fun_app$ck (case_llist$b ?v0) ?v1) ?v2) (ite (fun_app$l lnull$ ?v2) ?v0 (fun_app$c (fun_app$au ?v1 (lhd$ ?v2)) (ltl$ ?v2)))) :pattern ((fun_app$c (fun_app$ck (case_llist$b ?v0) ?v1) ?v2)))) :named a269))
+(assert (! (forall ((?v0 A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$) (?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_prod$)) (= (fun_app$h (fun_app$r (fun_app$aj uncurry$c ?v0) ?v1) ?v2) (fun_app$h (fun_app$ad uncurry$a (fun_app$y (uvg$ ?v0) ?v2)) ?v1))) :named a270))
+(assert (! (= internal_split$ uncurry$b) :named a271))
+(assert (! (= internal_split$a uncurry$) :named a272))
+(assert (! (= internal_split$b uncurry$d) :named a273))
+(assert (! (= internal_split$c uncurry$c) :named a274))
+(assert (! (= internal_split$d uncurry$a) :named a275))
+(assert (! (forall ((?v0 A_llist_bool_fun$) (?v1 A_llist_a_fun$) (?v2 A_llist_a_llist_fun$) (?v3 A_llist$)) (= (not (fun_app$l lnull$ (fun_app$a (fun_app$cl (fun_app$cm (unfold_llist$a ?v0) ?v1) ?v2) ?v3))) (not (fun_app$l ?v0 ?v3)))) :named a276))
+(assert (! (forall ((?v0 A_llist_bool_fun$) (?v1 A_llist_a_fun$) (?v2 A_llist_a_llist_fun$) (?v3 A_llist$)) (= (fun_app$l lnull$ (fun_app$a (fun_app$cl (fun_app$cm (unfold_llist$a ?v0) ?v1) ?v2) ?v3)) (fun_app$l ?v0 ?v3))) :named a277))
+(assert (! (forall ((?v0 A_llist_bool_fun$) (?v1 A_llist_a_fun$) (?v2 A_llist_a_llist_fun$) (?v3 A_llist$) (?v4 A$) (?v5 A_llist$)) (= (= (fun_app$a (fun_app$cl (fun_app$cm (unfold_llist$a ?v0) ?v1) ?v2) ?v3) (lCons$ ?v4 ?v5)) (and (not (fun_app$l ?v0 ?v3)) (and (= ?v4 (fun_app$c ?v1 ?v3)) (= ?v5 (fun_app$a (fun_app$cl (fun_app$cm (unfold_llist$a ?v0) ?v1) ?v2) (fun_app$a ?v2 ?v3))))))) :named a278))
+(assert (! (forall ((?v0 Bool_bool_fun$) (?v1 Bool) (?v2 A_a_llist_bool_fun_fun$) (?v3 A_llist$)) (= (fun_app$az ?v0 (fun_app$l (fun_app$ci (case_llist$ ?v1) ?v2) ?v3)) (fun_app$l (fun_app$ci (case_llist$ (fun_app$az ?v0 ?v1)) (fun_app$ba (uvh$ ?v0) ?v2)) ?v3))) :named a279))
+(assert (! (forall ((?v0 Bool_a_llist_fun$) (?v1 Bool) (?v2 A_a_llist_bool_fun_fun$) (?v3 A_llist$)) (= (fun_app$ax ?v0 (fun_app$l (fun_app$ci (case_llist$ ?v1) ?v2) ?v3)) (fun_app$a (fun_app$cj (case_llist$a (fun_app$ax ?v0 ?v1)) (fun_app$aw (uvi$ ?v0) ?v2)) ?v3))) :named a280))
+(assert (! (forall ((?v0 Bool_a_fun$) (?v1 Bool) (?v2 A_a_llist_bool_fun_fun$) (?v3 A_llist$)) (= (fun_app$bg ?v0 (fun_app$l (fun_app$ci (case_llist$ ?v1) ?v2) ?v3)) (fun_app$c (fun_app$ck (case_llist$b (fun_app$bg ?v0 ?v1)) (fun_app$bf (uvj$ ?v0) ?v2)) ?v3))) :named a281))
+(assert (! (forall ((?v0 A_llist_bool_fun$) (?v1 A_llist$) (?v2 A_a_llist_a_llist_fun_fun$) (?v3 A_llist$)) (= (fun_app$l ?v0 (fun_app$a (fun_app$cj (case_llist$a ?v1) ?v2) ?v3)) (fun_app$l (fun_app$ci (case_llist$ (fun_app$l ?v0 ?v1)) (fun_app$at (uvk$ ?v0) ?v2)) ?v3))) :named a282))
+(assert (! (forall ((?v0 A_llist_a_llist_fun$) (?v1 A_llist$) (?v2 A_a_llist_a_llist_fun_fun$) (?v3 A_llist$)) (= (fun_app$a ?v0 (fun_app$a (fun_app$cj (case_llist$a ?v1) ?v2) ?v3)) (fun_app$a (fun_app$cj (case_llist$a (fun_app$a ?v0 ?v1)) (fun_app$ar (uvl$ ?v0) ?v2)) ?v3))) :named a283))
+(assert (! (forall ((?v0 A_llist_a_fun$) (?v1 A_llist$) (?v2 A_a_llist_a_llist_fun_fun$) (?v3 A_llist$)) (= (fun_app$c ?v0 (fun_app$a (fun_app$cj (case_llist$a ?v1) ?v2) ?v3)) (fun_app$c (fun_app$ck (case_llist$b (fun_app$c ?v0 ?v1)) (fun_app$av (uvm$ ?v0) ?v2)) ?v3))) :named a284))
+(assert (! (forall ((?v0 A_bool_fun$) (?v1 A$) (?v2 A_a_llist_a_fun_fun$) (?v3 A_llist$)) (= (fun_app$k ?v0 (fun_app$c (fun_app$ck (case_llist$b ?v1) ?v2) ?v3)) (fun_app$l (fun_app$ci (case_llist$ (fun_app$k ?v0 ?v1)) (fun_app$bn (uvn$ ?v0) ?v2)) ?v3))) :named a285))
+(assert (! (forall ((?v0 A_a_llist_fun$) (?v1 A$) (?v2 A_a_llist_a_fun_fun$) (?v3 A_llist$)) (= (fun_app$bm ?v0 (fun_app$c (fun_app$ck (case_llist$b ?v1) ?v2) ?v3)) (fun_app$a (fun_app$cj (case_llist$a (fun_app$bm ?v0 ?v1)) (fun_app$bl (uvo$ ?v0) ?v2)) ?v3))) :named a286))
+(assert (! (forall ((?v0 A_a_fun$) (?v1 A$) (?v2 A_a_llist_a_fun_fun$) (?v3 A_llist$)) (= (fun_app$bp ?v0 (fun_app$c (fun_app$ck (case_llist$b ?v1) ?v2) ?v3)) (fun_app$c (fun_app$ck (case_llist$b (fun_app$bp ?v0 ?v1)) (fun_app$bo (uvp$ ?v0) ?v2)) ?v3))) :named a287))
+(assert (! (forall ((?v0 A_llist_bool_fun$) (?v1 A_llist$) (?v2 A_llist_a_fun$) (?v3 A_llist_a_llist_fun$)) (=> (not (fun_app$l ?v0 ?v1)) (not (fun_app$l lnull$ (fun_app$a (fun_app$cl (fun_app$cm (unfold_llist$a ?v0) ?v2) ?v3) ?v1))))) :named a288))
+(assert (! (forall ((?v0 A_llist_bool_fun$) (?v1 A_llist$) (?v2 A_llist_a_fun$) (?v3 A_llist_a_llist_fun$)) (=> (fun_app$l ?v0 ?v1) (fun_app$l lnull$ (fun_app$a (fun_app$cl (fun_app$cm (unfold_llist$a ?v0) ?v2) ?v3) ?v1)))) :named a289))
+(assert (! (forall ((?v0 A_llist_bool_fun$) (?v1 A_llist$) (?v2 A_llist_a_fun$) (?v3 A_llist_a_llist_fun$)) (=> (not (fun_app$l ?v0 ?v1)) (= (fun_app$a (fun_app$cl (fun_app$cm (unfold_llist$a ?v0) ?v2) ?v3) ?v1) (lCons$ (fun_app$c ?v2 ?v1) (fun_app$a (fun_app$cl (fun_app$cm (unfold_llist$a ?v0) ?v2) ?v3) (fun_app$a ?v3 ?v1)))))) :named a290))
+(assert (! (forall ((?v0 A_llist_bool_fun$) (?v1 A_llist$) (?v2 A_llist_a_fun$) (?v3 A_llist_a_llist_fun$)) (! (=> (fun_app$l ?v0 ?v1) (= (fun_app$a (fun_app$cl (fun_app$cm (unfold_llist$a ?v0) ?v2) ?v3) ?v1) lNil$)) :pattern ((fun_app$a (fun_app$cl (fun_app$cm (unfold_llist$a ?v0) ?v2) ?v3) ?v1)))) :named a291))
+(assert (! (forall ((?v0 A_llist_bool_fun$) (?v1 A_llist$) (?v2 A_llist_a_fun$) (?v3 A_llist_a_llist_fun$)) (=> (not (fun_app$l ?v0 ?v1)) (= (ltl$ (fun_app$a (fun_app$cl (fun_app$cm (unfold_llist$a ?v0) ?v2) ?v3) ?v1)) (fun_app$a (fun_app$cl (fun_app$cm (unfold_llist$a ?v0) ?v2) ?v3) (fun_app$a ?v3 ?v1))))) :named a292))
+(assert (! (forall ((?v0 A_llist_bool_fun$) (?v1 A_llist$) (?v2 A_llist_a_fun$) (?v3 A_llist_a_llist_fun$)) (=> (not (fun_app$l ?v0 ?v1)) (= (lhd$ (fun_app$a (fun_app$cl (fun_app$cm (unfold_llist$a ?v0) ?v2) ?v3) ?v1)) (fun_app$c ?v2 ?v1)))) :named a293))
+(assert (! (forall ((?v0 Bool) (?v1 A_a_llist_bool_fun_fun$) (?v2 A$) (?v3 A_llist$)) (! (= (fun_app$l (fun_app$ci (case_llist$ ?v0) ?v1) (lCons$ ?v2 ?v3)) (fun_app$l (fun_app$as ?v1 ?v2) ?v3)) :pattern ((fun_app$l (fun_app$ci (case_llist$ ?v0) ?v1) (lCons$ ?v2 ?v3))))) :named a294))
+(assert (! (forall ((?v0 A_llist$) (?v1 A_a_llist_a_llist_fun_fun$) (?v2 A$) (?v3 A_llist$)) (! (= (fun_app$a (fun_app$cj (case_llist$a ?v0) ?v1) (lCons$ ?v2 ?v3)) (fun_app$a (fun_app$v ?v1 ?v2) ?v3)) :pattern ((fun_app$a (fun_app$cj (case_llist$a ?v0) ?v1) (lCons$ ?v2 ?v3))))) :named a295))
+(assert (! (forall ((?v0 A$) (?v1 A_a_llist_a_fun_fun$) (?v2 A$) (?v3 A_llist$)) (! (= (fun_app$c (fun_app$ck (case_llist$b ?v0) ?v1) (lCons$ ?v2 ?v3)) (fun_app$c (fun_app$au ?v1 ?v2) ?v3)) :pattern ((fun_app$c (fun_app$ck (case_llist$b ?v0) ?v1) (lCons$ ?v2 ?v3))))) :named a296))
+(assert (! (forall ((?v0 Bool) (?v1 A_a_llist_bool_fun_fun$)) (! (= (fun_app$l (fun_app$ci (case_llist$ ?v0) ?v1) lNil$) ?v0) :pattern ((fun_app$ci (case_llist$ ?v0) ?v1)))) :named a297))
+(assert (! (forall ((?v0 A_llist$) (?v1 A_a_llist_a_llist_fun_fun$)) (! (= (fun_app$a (fun_app$cj (case_llist$a ?v0) ?v1) lNil$) ?v0) :pattern ((fun_app$cj (case_llist$a ?v0) ?v1)))) :named a298))
+(assert (! (forall ((?v0 A$) (?v1 A_a_llist_a_fun_fun$)) (! (= (fun_app$c (fun_app$ck (case_llist$b ?v0) ?v1) lNil$) ?v0) :pattern ((fun_app$ck (case_llist$b ?v0) ?v1)))) :named a299))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$)) (= (not (fun_app$bw lnull$a ?v0)) (fun_app$bw (fun_app$cn (case_llist$c false) uvq$) ?v0))) :named a300))
+(assert (! (forall ((?v0 A_llist$)) (= (not (fun_app$l lnull$ ?v0)) (fun_app$l (fun_app$ci (case_llist$ false) uvr$) ?v0))) :named a301))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$)) (! (= (fun_app$bw lnull$a ?v0) (fun_app$bw (fun_app$cn (case_llist$c true) uvs$) ?v0)) :pattern ((fun_app$bw lnull$a ?v0)))) :named a302))
+(assert (! (forall ((?v0 A_llist$)) (! (= (fun_app$l lnull$ ?v0) (fun_app$l (fun_app$ci (case_llist$ true) uvt$) ?v0)) :pattern ((fun_app$l lnull$ ?v0)))) :named a303))
+(assert (! (forall ((?v0 A_llist_bool_fun$) (?v1 A_llist_a_fun$) (?v2 A_llist_a_llist_fun$) (?v3 A_llist$)) (= (fun_app$a (fun_app$cl (fun_app$cm (unfold_llist$a ?v0) ?v1) ?v2) ?v3) (ite (fun_app$l ?v0 ?v3) lNil$ (lCons$ (fun_app$c ?v1 ?v3) (fun_app$a (fun_app$cl (fun_app$cm (unfold_llist$a ?v0) ?v1) ?v2) (fun_app$a ?v2 ?v3)))))) :named a304))
+(assert (! (forall ((?v0 A_llist_bool_fun$) (?v1 A_llist_a_fun$) (?v2 A_llist_a_llist_fun$) (?v3 A_llist$)) (= (ltl$ (fun_app$a (fun_app$cl (fun_app$cm (unfold_llist$a ?v0) ?v1) ?v2) ?v3)) (ite (fun_app$l ?v0 ?v3) lNil$ (fun_app$a (fun_app$cl (fun_app$cm (unfold_llist$a ?v0) ?v1) ?v2) (fun_app$a ?v2 ?v3))))) :named a305))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$)) (= (ltl$a ?v0) (case_llist$d lNil$a uvu$ ?v0))) :named a306))
+(assert (! (forall ((?v0 A_llist$)) (= (ltl$ ?v0) (fun_app$a (fun_app$cj (case_llist$a lNil$) uvv$) ?v0))) :named a307))
+(assert (! (forall ((?v0 A_llist_a_llist_bool_fun_fun$) (?v1 A_llist$) (?v2 A_llist$)) (! (= (fun_app$h (fun_app$ad internal_split$d ?v0) (pair$ ?v1 ?v2)) (fun_app$l (fun_app$m ?v0 ?v1) ?v2)) :pattern ((fun_app$h (fun_app$ad internal_split$d ?v0) (pair$ ?v1 ?v2))))) :named a308))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$)) (! (= (uncurry$l uvw$ ?v0) ?v0) :pattern ((uncurry$l uvw$ ?v0)))) :named a309))
+(assert (! (forall ((?v0 A_llist_a_llist_prod$)) (! (= (fun_app$w (fun_app$ab uncurry$ uvx$) ?v0) ?v0) :pattern ((fun_app$w (fun_app$ab uncurry$ uvx$) ?v0)))) :named a310))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_prod_set$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_prod_set$)) (= (= (uvy$ ?v0) (uvy$ ?v1)) (= ?v0 ?v1))) :named a311))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_set$) (?v1 A_llist_a_llist_prod_set$)) (= (= (uvz$ ?v0) (uvz$ ?v1)) (= ?v0 ?v1))) :named a312))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$) (?v1 A_llist_a_llist_prod_llist$)) (=> (or (not (fun_app$bw lnull$a ?v0)) (not (fun_app$bw lnull$a ?v1))) (= (lhd$a (fun_app$ (lappend$ ?v0) ?v1)) (case_llist$e (lhd$a ?v1) uwa$ ?v0)))) :named a313))
+(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$)) (=> (or (not (fun_app$l lnull$ ?v0)) (not (fun_app$l lnull$ ?v1))) (= (lhd$ (fun_app$a (lappend$a ?v0) ?v1)) (fun_app$c (fun_app$ck (case_llist$b (lhd$ ?v1)) uwb$) ?v0)))) :named a314))
+(assert (! (forall ((?v0 A_bool_fun$) (?v1 A$) (?v2 A_llist$)) (! (= (fun_app$l (pred_llist$ ?v0) (lCons$ ?v1 ?v2)) (and (fun_app$k ?v0 ?v1) (fun_app$l (pred_llist$ ?v0) ?v2))) :pattern ((fun_app$l (pred_llist$ ?v0) (lCons$ ?v1 ?v2))))) :named a315))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_bool_fun$) (?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_prod_llist$)) (! (= (fun_app$bw (pred_llist$a ?v0) (lCons$a ?v1 ?v2)) (and (fun_app$h ?v0 ?v1) (fun_app$bw (pred_llist$a ?v0) ?v2))) :pattern ((fun_app$bw (pred_llist$a ?v0) (lCons$a ?v1 ?v2))))) :named a316))
+(assert (! (forall ((?v0 A_llist_a_llist_prod$)) (! (= (fun_app$bw (lmember$ ?v0) lNil$a) false) :pattern ((lmember$ ?v0)))) :named a317))
+(assert (! (forall ((?v0 A$)) (! (= (fun_app$l (lmember$a ?v0) lNil$) false) :pattern ((lmember$a ?v0)))) :named a318))
+(assert (! (forall ((?v0 A_llist_a_llist_a_llist_a_llist_prod_set_fun_fun$) (?v1 A_llist_a_llist_prod$)) (= (fun_app$x (fun_app$ah uncurry$b (uwc$ ?v0)) (swap$ ?v1)) (fun_app$x (fun_app$ah uncurry$b ?v0) ?v1))) :named a319))
+(assert (! (forall ((?v0 A_llist_a_llist_a_llist_a_llist_prod_fun_fun$) (?v1 A_llist_a_llist_prod$)) (= (fun_app$w (fun_app$ab uncurry$ (uwd$ ?v0)) (swap$ ?v1)) (fun_app$w (fun_app$ab uncurry$ ?v0) ?v1))) :named a320))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) (?v1 A_llist_a_llist_prod_a_llist_a_llist_prod_prod$)) (= (fun_app$j (fun_app$al uncurry$d (uwe$ ?v0)) (swap$a ?v1)) (fun_app$j (fun_app$al uncurry$d ?v0) ?v1))) :named a321))
+(assert (! (forall ((?v0 A_llist_a_llist_a_llist_a_llist_prod_bool_fun_fun_fun$) (?v1 A_llist_a_llist_prod$)) (= (fun_app$r (fun_app$aj uncurry$c (uwf$ ?v0)) (swap$ ?v1)) (fun_app$r (fun_app$aj uncurry$c ?v0) ?v1))) :named a322))
+(assert (! (forall ((?v0 A_llist_a_llist_bool_fun_fun$) (?v1 A_llist_a_llist_prod$)) (= (fun_app$h (fun_app$ad uncurry$a (uwg$ ?v0)) (swap$ ?v1)) (fun_app$h (fun_app$ad uncurry$a ?v0) ?v1))) :named a323))
+(assert (! (forall ((?v0 A$) (?v1 A$) (?v2 A_llist$)) (! (= (fun_app$l (lmember$a ?v0) (lCons$ ?v1 ?v2)) (or (= ?v0 ?v1) (fun_app$l (lmember$a ?v0) ?v2))) :pattern ((fun_app$l (lmember$a ?v0) (lCons$ ?v1 ?v2))))) :named a324))
+(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_prod_llist$)) (! (= (fun_app$bw (lmember$ ?v0) (lCons$a ?v1 ?v2)) (or (= ?v0 ?v1) (fun_app$bw (lmember$ ?v0) ?v2))) :pattern ((fun_app$bw (lmember$ ?v0) (lCons$a ?v1 ?v2))))) :named a325))
+(assert (! (forall ((?v0 A_llist_a_llist_prod$)) (= (swap$ (swap$ ?v0)) ?v0)) :named a326))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$) (?v1 A_llist_a_llist_prod_llist$)) (= (fun_app$bw lnull$a (fun_app$ (lappend$ ?v0) ?v1)) (and (fun_app$bw lnull$a ?v0) (fun_app$bw lnull$a ?v1)))) :named a327))
+(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$)) (= (fun_app$l lnull$ (fun_app$a (lappend$a ?v0) ?v1)) (and (fun_app$l lnull$ ?v0) (fun_app$l lnull$ ?v1)))) :named a328))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$) (?v1 A_llist_a_llist_prod_llist$)) (= (not (fun_app$bw lnull$a (fun_app$ (lappend$ ?v0) ?v1))) (or (not (fun_app$bw lnull$a ?v0)) (not (fun_app$bw lnull$a ?v1))))) :named a329))
+(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$)) (= (not (fun_app$l lnull$ (fun_app$a (lappend$a ?v0) ?v1))) (or (not (fun_app$l lnull$ ?v0)) (not (fun_app$l lnull$ ?v1))))) :named a330))
+(assert (! (forall ((?v0 A$) (?v1 A_llist$) (?v2 A_llist$)) (! (= (fun_app$a (lappend$a (lCons$ ?v0 ?v1)) ?v2) (lCons$ ?v0 (fun_app$a (lappend$a ?v1) ?v2))) :pattern ((fun_app$a (lappend$a (lCons$ ?v0 ?v1)) ?v2)))) :named a331))
+(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod_llist$) (?v2 A_llist_a_llist_prod_llist$)) (! (= (fun_app$ (lappend$ (lCons$a ?v0 ?v1)) ?v2) (lCons$a ?v0 (fun_app$ (lappend$ ?v1) ?v2))) :pattern ((fun_app$ (lappend$ (lCons$a ?v0 ?v1)) ?v2)))) :named a332))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$)) (! (= (fun_app$ (lappend$ lNil$a) ?v0) ?v0) :pattern ((fun_app$ (lappend$ lNil$a) ?v0)))) :named a333))
+(assert (! (forall ((?v0 A_llist$)) (! (= (fun_app$a (lappend$a lNil$) ?v0) ?v0) :pattern ((fun_app$a (lappend$a lNil$) ?v0)))) :named a334))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$)) (! (= (fun_app$ (lappend$ ?v0) lNil$a) ?v0) :pattern ((lappend$ ?v0)))) :named a335))
+(assert (! (forall ((?v0 A_llist$)) (! (= (fun_app$a (lappend$a ?v0) lNil$) ?v0) :pattern ((lappend$a ?v0)))) :named a336))
+(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod$)) (= (swap$a (pair$b ?v0 ?v1)) (pair$b ?v1 ?v0))) :named a337))
+(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$)) (= (swap$ (pair$ ?v0 ?v1)) (pair$ ?v1 ?v0))) :named a338))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$) (?v1 A_llist_a_llist_prod_llist$)) (= (ltl$a (fun_app$ (lappend$ ?v0) ?v1)) (ite (fun_app$bw lnull$a ?v0) (ltl$a ?v1) (fun_app$ (lappend$ (ltl$a ?v0)) ?v1)))) :named a339))
+(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$)) (= (ltl$ (fun_app$a (lappend$a ?v0) ?v1)) (ite (fun_app$l lnull$ ?v0) (ltl$ ?v1) (fun_app$a (lappend$a (ltl$ ?v0)) ?v1)))) :named a340))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$) (?v1 A_llist_a_llist_prod_llist$)) (= (lhd$a (fun_app$ (lappend$ ?v0) ?v1)) (ite (fun_app$bw lnull$a ?v0) (lhd$a ?v1) (lhd$a ?v0)))) :named a341))
+(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$)) (= (lhd$ (fun_app$a (lappend$a ?v0) ?v1)) (ite (fun_app$l lnull$ ?v0) (lhd$ ?v1) (lhd$ ?v0)))) :named a342))
+(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$) (?v2 A_llist$)) (= (fun_app$a (lappend$a (fun_app$a (lappend$a ?v0) ?v1)) ?v2) (fun_app$a (lappend$a ?v0) (fun_app$a (lappend$a ?v1) ?v2)))) :named a343))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$) (?v1 A_llist_a_llist_prod_llist$) (?v2 A_llist_a_llist_prod_llist$)) (= (fun_app$ (lappend$ (fun_app$ (lappend$ ?v0) ?v1)) ?v2) (fun_app$ (lappend$ ?v0) (fun_app$ (lappend$ ?v1) ?v2)))) :named a344))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$) (?v1 A_llist_a_llist_prod_llist$)) (! (=> (fun_app$bw lnull$a ?v0) (= (fun_app$ (lappend$ ?v0) ?v1) ?v1)) :pattern ((fun_app$ (lappend$ ?v0) ?v1)))) :named a345))
+(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$)) (! (=> (fun_app$l lnull$ ?v0) (= (fun_app$a (lappend$a ?v0) ?v1) ?v1)) :pattern ((fun_app$a (lappend$a ?v0) ?v1)))) :named a346))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$) (?v1 A_llist_a_llist_prod_llist$)) (! (=> (fun_app$bw lnull$a ?v0) (= (fun_app$ (lappend$ ?v1) ?v0) ?v1)) :pattern ((fun_app$ (lappend$ ?v1) ?v0)))) :named a347))
+(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$)) (! (=> (fun_app$l lnull$ ?v0) (= (fun_app$a (lappend$a ?v1) ?v0) ?v1)) :pattern ((fun_app$a (lappend$a ?v1) ?v0)))) :named a348))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$) (?v1 A_llist_a_llist_prod_llist$)) (=> (and (fun_app$bw lnull$a ?v0) (fun_app$bw lnull$a ?v1)) (fun_app$bw lnull$a (fun_app$ (lappend$ ?v0) ?v1)))) :named a349))
+(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$)) (=> (and (fun_app$l lnull$ ?v0) (fun_app$l lnull$ ?v1)) (fun_app$l lnull$ (fun_app$a (lappend$a ?v0) ?v1)))) :named a350))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$) (?v1 A_llist_a_llist_prod_llist$)) (=> (or (not (fun_app$bw lnull$a ?v0)) (not (fun_app$bw lnull$a ?v1))) (not (fun_app$bw lnull$a (fun_app$ (lappend$ ?v0) ?v1))))) :named a351))
+(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$)) (=> (or (not (fun_app$l lnull$ ?v0)) (not (fun_app$l lnull$ ?v1))) (not (fun_app$l lnull$ (fun_app$a (lappend$a ?v0) ?v1))))) :named a352))
+(assert (! (= (fun_app$ (lappend$ lNil$a) lNil$a) lNil$a) :named a353))
+(assert (! (= (fun_app$a (lappend$a lNil$) lNil$) lNil$) :named a354))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$) (?v1 A_llist_a_llist_prod_llist$)) (= (= (fun_app$ (lappend$ ?v0) ?v1) lNil$a) (and (= ?v0 lNil$a) (= ?v1 lNil$a)))) :named a355))
+(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$)) (= (= (fun_app$a (lappend$a ?v0) ?v1) lNil$) (and (= ?v0 lNil$) (= ?v1 lNil$)))) :named a356))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$) (?v1 A_llist_a_llist_prod_llist$)) (= (= lNil$a (fun_app$ (lappend$ ?v0) ?v1)) (and (= ?v0 lNil$a) (= ?v1 lNil$a)))) :named a357))
+(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$)) (= (= lNil$ (fun_app$a (lappend$a ?v0) ?v1)) (and (= ?v0 lNil$) (= ?v1 lNil$)))) :named a358))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$) (?v1 A_llist_a_llist_prod_llist$)) (= (fun_app$ (lappend$ ?v0) ?v1) (case_llist$d ?v1 (uwh$ ?v1) ?v0))) :named a359))
+(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$)) (= (fun_app$a (lappend$a ?v0) ?v1) (fun_app$a (fun_app$cj (case_llist$a ?v1) (uwi$ ?v1)) ?v0))) :named a360))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$) (?v1 A_llist_a_llist_prod_llist$)) (! (=> (and (fun_app$bw lnull$a ?v0) (fun_app$bw lnull$a ?v1)) (= (fun_app$ (lappend$ ?v0) ?v1) lNil$a)) :pattern ((fun_app$ (lappend$ ?v0) ?v1)))) :named a361))
+(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$)) (! (=> (and (fun_app$l lnull$ ?v0) (fun_app$l lnull$ ?v1)) (= (fun_app$a (lappend$a ?v0) ?v1) lNil$)) :pattern ((fun_app$a (lappend$a ?v0) ?v1)))) :named a362))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$) (?v1 A_llist_a_llist_prod$) (?v2 A_llist_a_llist_prod_llist$)) (= (fun_app$ (lappend$ (fun_app$ (lappend$ ?v0) (lCons$a ?v1 lNil$a))) ?v2) (fun_app$ (lappend$ ?v0) (lCons$a ?v1 ?v2)))) :named a363))
+(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$)) (=> (not (fun_app$l lnull$ ?v0)) (= (fun_app$a (lappend$a (ltl$ ?v0)) ?v1) (ltl$ (fun_app$a (lappend$a ?v0) ?v1))))) :named a364))
+(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$)) (=> (or (not (fun_app$l lnull$ ?v0)) (not (fun_app$l lnull$ ?v1))) (= (fun_app$a (lappend$a ?v0) ?v1) (lCons$ (fun_app$c (fun_app$ck (case_llist$b (lhd$ ?v1)) uwb$) ?v0) (fun_app$a (fun_app$cj (case_llist$a (fun_app$a (fun_app$cj (case_llist$a undefined$) uvv$) ?v1)) (uwj$ ?v1)) ?v0))))) :named a365))
+(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$)) (=> (or (not (fun_app$l lnull$ ?v0)) (not (fun_app$l lnull$ ?v1))) (= (ltl$ (fun_app$a (lappend$a ?v0) ?v1)) (fun_app$a (fun_app$cj (case_llist$a (fun_app$a (fun_app$cj (case_llist$a undefined$) uvv$) ?v1)) (uwj$ ?v1)) ?v0)))) :named a366))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_set$) (?v1 A_llist_a_llist_fun$)) (= (inv_image$ ?v0 ?v1) (collect$ (fun_app$ad uncurry$a (fun_app$z (uwk$ ?v0) ?v1))))) :named a367))
+(assert (! (forall ((?v0 A_llist_bool_fun$) (?v1 A_llist_a_llist_a_llist_prod_set_fun$)) (= (same_fst$ ?v0 ?v1) (collect$a (fun_app$al uncurry$d (fun_app$aj uncurry$c (fun_app$bt (uwm$ ?v0) ?v1)))))) :named a368))
+(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod_llist$) (?v2 A_llist_a_llist_prod_a_llist_a_llist_prod_llist_bool_fun_fun$)) (=> (and (fun_app$i (member$ ?v0) (lset$ ?v1)) (and (forall ((?v3 A_llist_a_llist_prod_llist$)) (=> (not (fun_app$bw lnull$a ?v3)) (fun_app$bw (fun_app$bx ?v2 (lhd$a ?v3)) ?v3))) (forall ((?v3 A_llist_a_llist_prod_llist$) (?v4 A_llist_a_llist_prod$)) (=> (and (not (fun_app$bw lnull$a ?v3)) (and (fun_app$i (member$ ?v4) (lset$ (ltl$a ?v3))) (fun_app$bw (fun_app$bx ?v2 ?v4) (ltl$a ?v3)))) (fun_app$bw (fun_app$bx ?v2 ?v4) ?v3))))) (fun_app$bw (fun_app$bx ?v2 ?v0) ?v1))) :named a369))
+(assert (! (forall ((?v0 A$) (?v1 A_llist$) (?v2 A_a_llist_bool_fun_fun$)) (=> (and (member$b ?v0 (lset$a ?v1)) (and (forall ((?v3 A_llist$)) (=> (not (fun_app$l lnull$ ?v3)) (fun_app$l (fun_app$as ?v2 (lhd$ ?v3)) ?v3))) (forall ((?v3 A_llist$) (?v4 A$)) (=> (and (not (fun_app$l lnull$ ?v3)) (and (member$b ?v4 (lset$a (ltl$ ?v3))) (fun_app$l (fun_app$as ?v2 ?v4) (ltl$ ?v3)))) (fun_app$l (fun_app$as ?v2 ?v4) ?v3))))) (fun_app$l (fun_app$as ?v2 ?v0) ?v1))) :named a370))
+(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$) (?v2 A_llist_a_llist_prod_set$) (?v3 A_llist_a_llist_fun$)) (= (fun_app$i (member$ (pair$ ?v0 ?v1)) (inv_image$ ?v2 ?v3)) (fun_app$i (member$ (pair$ (fun_app$a ?v3 ?v0) (fun_app$a ?v3 ?v1))) ?v2))) :named a371))
+(assert (! (forall ((?v0 A_llist_bool_fun$) (?v1 A_llist$) (?v2 A_llist$) (?v3 A_llist$) (?v4 A_llist_a_llist_a_llist_prod_set_fun$)) (=> (and (fun_app$l ?v0 ?v1) (fun_app$i (member$ (pair$ ?v2 ?v3)) (fun_app$n ?v4 ?v1))) (member$a (pair$b (pair$ ?v1 ?v2) (pair$ ?v1 ?v3)) (same_fst$ ?v0 ?v4)))) :named a372))
+(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod_llist$)) (fun_app$i (member$ ?v0) (lset$ (lCons$a ?v0 ?v1)))) :named a373))
+(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod_llist$)) (fun_app$i (member$ ?v0) (lset$ (lCons$a ?v0 ?v1)))) :named a374))
+(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod_llist$) (?v2 A_llist_a_llist_prod$)) (=> (fun_app$i (member$ ?v0) (lset$ ?v1)) (fun_app$i (member$ ?v0) (lset$ (lCons$a ?v2 ?v1))))) :named a375))
+(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod_llist$) (?v2 A_llist_a_llist_prod$)) (=> (fun_app$i (member$ ?v0) (lset$ ?v1)) (fun_app$i (member$ ?v0) (lset$ (lCons$a ?v2 ?v1))))) :named a376))
+(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod_llist$)) (=> (and (fun_app$i (member$ ?v0) (lset$ ?v1)) (and (forall ((?v2 A_llist_a_llist_prod_llist$)) (=> (= ?v1 (lCons$a ?v0 ?v2)) false)) (forall ((?v2 A_llist_a_llist_prod$) (?v3 A_llist_a_llist_prod_llist$)) (=> (and (= ?v1 (lCons$a ?v2 ?v3)) (fun_app$i (member$ ?v0) (lset$ ?v3))) false)))) false)) :named a377))
+(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod_llist$) (?v2 A_llist_a_llist_prod_llist_bool_fun$)) (=> (and (fun_app$i (member$ ?v0) (lset$ ?v1)) (and (forall ((?v3 A_llist_a_llist_prod_llist$)) (fun_app$bw ?v2 (lCons$a ?v0 ?v3))) (forall ((?v3 A_llist_a_llist_prod$) (?v4 A_llist_a_llist_prod_llist$)) (=> (and (fun_app$i (member$ ?v0) (lset$ ?v4)) (and (not (= ?v0 ?v3)) (fun_app$bw ?v2 ?v4))) (fun_app$bw ?v2 (lCons$a ?v3 ?v4)))))) (fun_app$bw ?v2 ?v1))) :named a378))
+(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod_llist$) (?v2 A_llist_a_llist_prod_llist_bool_fun$)) (=> (and (fun_app$i (member$ ?v0) (lset$ ?v1)) (and (forall ((?v3 A_llist_a_llist_prod_llist$)) (fun_app$bw ?v2 (lCons$a ?v0 ?v3))) (forall ((?v3 A_llist_a_llist_prod$) (?v4 A_llist_a_llist_prod_llist$)) (=> (and (fun_app$i (member$ ?v0) (lset$ ?v4)) (fun_app$bw ?v2 ?v4)) (fun_app$bw ?v2 (lCons$a ?v3 ?v4)))))) (fun_app$bw ?v2 ?v1))) :named a379))
+(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod_llist$)) (=> (and (fun_app$i (member$ ?v0) (lset$ ?v1)) (and (forall ((?v2 A_llist_a_llist_prod_llist$)) (=> (= ?v1 (lCons$a ?v0 ?v2)) false)) (forall ((?v2 A_llist_a_llist_prod$) (?v3 A_llist_a_llist_prod_llist$)) (=> (and (= ?v1 (lCons$a ?v2 ?v3)) (fun_app$i (member$ ?v0) (lset$ ?v3))) false)))) false)) :named a380))
+(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod_llist$) (?v2 A_llist_a_llist_prod_a_llist_a_llist_prod_llist_bool_fun_fun$)) (=> (and (fun_app$i (member$ ?v0) (lset$ ?v1)) (and (forall ((?v3 A_llist_a_llist_prod$) (?v4 A_llist_a_llist_prod_llist$)) (fun_app$bw (fun_app$bx ?v2 ?v3) (lCons$a ?v3 ?v4))) (forall ((?v3 A_llist_a_llist_prod$) (?v4 A_llist_a_llist_prod_llist$) (?v5 A_llist_a_llist_prod$)) (=> (and (fun_app$i (member$ ?v5) (lset$ ?v4)) (fun_app$bw (fun_app$bx ?v2 ?v5) ?v4)) (fun_app$bw (fun_app$bx ?v2 ?v5) (lCons$a ?v3 ?v4)))))) (fun_app$bw (fun_app$bx ?v2 ?v0) ?v1))) :named a381))
+(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod_llist$)) (=> (fun_app$i (member$ ?v0) (lset$ (ltl$a ?v1))) (fun_app$i (member$ ?v0) (lset$ ?v1)))) :named a382))
+(assert (! (forall ((?v0 A$) (?v1 A_llist$)) (=> (member$b ?v0 (lset$a (ltl$ ?v1))) (member$b ?v0 (lset$a ?v1)))) :named a383))
+(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod_llist$)) (= (fun_app$i (member$ ?v0) (lset$ ?v1)) (fun_app$bw (lmember$ ?v0) ?v1))) :named a384))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$) (?v1 A_llist_a_llist_prod$)) (=> (and (not (fun_app$bw lnull$a ?v0)) (fun_app$i (member$ ?v1) (lset$ (ltl$a ?v0)))) (fun_app$i (member$ ?v1) (lset$ ?v0)))) :named a385))
+(assert (! (forall ((?v0 A_llist$) (?v1 A$)) (=> (and (not (fun_app$l lnull$ ?v0)) (member$b ?v1 (lset$a (ltl$ ?v0)))) (member$b ?v1 (lset$a ?v0)))) :named a386))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_llist$)) (=> (not (fun_app$bw lnull$a ?v0)) (fun_app$i (member$ (lhd$a ?v0)) (lset$ ?v0)))) :named a387))
+(assert (! (forall ((?v0 A_llist$)) (=> (not (fun_app$l lnull$ ?v0)) (member$b (lhd$ ?v0) (lset$a ?v0)))) :named a388))
+(assert (! (forall ((?v0 A_llist$)) (= (lhd$ ?v0) (fun_app$c (fun_app$ck (case_llist$b undefined$a) uwb$) ?v0))) :named a389))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_set$) (?v1 A_llist_a_llist_prod_set$)) (= (lex_prod$ ?v0 ?v1) (collect$a (fun_app$al uncurry$d (fun_app$aj uncurry$c (fun_app$bq (uwo$ ?v0) ?v1)))))) :named a390))
+(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod_llist$)) (=> (fun_app$i (member$ ?v0) (lset$ ?v1)) (exists ((?v2 A_llist_a_llist_prod_llist$) (?v3 A_llist_a_llist_prod_llist$)) (and (= ?v1 (fun_app$ (lappend$ ?v2) (lCons$a ?v0 ?v3))) (and (lfinite$ ?v2) (not (fun_app$i (member$ ?v0) (lset$ ?v2)))))))) :named a391))
+(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod_llist$)) (=> (fun_app$i (member$ ?v0) (lset$ ?v1)) (exists ((?v2 A_llist_a_llist_prod_llist$) (?v3 A_llist_a_llist_prod_llist$)) (and (= ?v1 (fun_app$ (lappend$ ?v2) (lCons$a ?v0 ?v3))) (lfinite$ ?v2))))) :named a392))
+(assert (! (forall ((?v0 A_llist$)) (= (lfinite$a (ltl$ ?v0)) (lfinite$a ?v0))) :named a393))
+(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$) (?v2 A_llist$) (?v3 A_llist$) (?v4 A_llist_a_llist_prod_set$) (?v5 A_llist_a_llist_prod_set$)) (= (member$a (pair$b (pair$ ?v0 ?v1) (pair$ ?v2 ?v3)) (lex_prod$ ?v4 ?v5)) (or (fun_app$i (member$ (pair$ ?v0 ?v2)) ?v4) (and (= ?v0 ?v2) (fun_app$i (member$ (pair$ ?v1 ?v3)) ?v5))))) :named a394))
+(assert (! (forall ((?v0 A_llist$)) (=> (fun_app$l lnull$ ?v0) (lfinite$a ?v0))) :named a395))
+(assert (! (forall ((?v0 A_llist$) (?v1 A_llist_bool_fun$)) (=> (and (lfinite$a ?v0) (and (forall ((?v2 A_llist$)) (=> (fun_app$l lnull$ ?v2) (fun_app$l ?v1 ?v2))) (forall ((?v2 A_llist$)) (=> (and (lfinite$a ?v2) (and (not (fun_app$l lnull$ ?v2)) (fun_app$l ?v1 (ltl$ ?v2)))) (fun_app$l ?v1 ?v2))))) (fun_app$l ?v1 ?v0))) :named a396))
+(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod_llist$) (?v2 A_llist_a_llist_prod_llist$)) (= (fun_app$i (member$ ?v0) (lset$ (fun_app$ (lappend$ ?v1) ?v2))) (or (fun_app$i (member$ ?v0) (lset$ ?v1)) (and (lfinite$ ?v1) (fun_app$i (member$ ?v0) (lset$ ?v2)))))) :named a397))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_bool_fun$) (?v1 A_llist_a_llist_prod_bool_fun$)) (= (collect$ (fun_app$t (uwp$ ?v0) ?v1)) (sup$ (collect$ ?v0) (collect$ ?v1)))) :named a398))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_set$) (?v1 A_llist_a_llist_prod_set$)) (= (sup$ ?v0 ?v1) (collect$ (fun_app$s (uwq$ ?v0) ?v1)))) :named a399))
+(assert (! (forall ((?v0 A_llist_a_llist_bool_fun_fun$) (?v1 A_llist$) (?v2 A_llist$) (?v3 A_a_bool_fun_fun$)) (=> (and (fun_app$l (fun_app$m ?v0 ?v1) ?v2) (forall ((?v4 A_llist$) (?v5 A_llist$)) (=> (fun_app$l (fun_app$m ?v0 ?v4) ?v5) (and (= (fun_app$l lnull$ ?v4) (fun_app$l lnull$ ?v5)) (=> (and (not (fun_app$l lnull$ ?v4)) (not (fun_app$l lnull$ ?v5))) (and (fun_app$k (fun_app$co ?v3 (lhd$ ?v4)) (lhd$ ?v5)) (fun_app$l (fun_app$m ?v0 (ltl$ ?v4)) (ltl$ ?v5)))))))) (fun_app$l (fun_app$m (llist_all2$ ?v3) ?v1) ?v2))) :named a400))
+(assert (! (forall ((?v0 A_a_bool_fun_fun$) (?v1 A_llist$) (?v2 A_llist$)) (= (fun_app$l (fun_app$m (llist_all2$ ?v0) ?v1) ?v2) (and (= (fun_app$l lnull$ ?v1) (fun_app$l lnull$ ?v2)) (=> (and (not (fun_app$l lnull$ ?v1)) (not (fun_app$l lnull$ ?v2))) (and (fun_app$k (fun_app$co ?v0 (lhd$ ?v1)) (lhd$ ?v2)) (fun_app$l (fun_app$m (llist_all2$ ?v0) (ltl$ ?v1)) (ltl$ ?v2))))))) :named a401))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_set$) (?v1 A_llist_a_llist_prod_set$)) (=> (forall ((?v2 A_llist$) (?v3 A_llist$)) (=> (fun_app$i (member$ (pair$ ?v2 ?v3)) ?v0) (fun_app$i (member$ (pair$ ?v2 ?v3)) ?v1))) (fun_app$i (less_eq$ ?v0) ?v1))) :named a402))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$) (?v1 A_llist_a_llist_prod_llist$) (?v2 A_llist_a_llist_prod_llist$) (?v3 A_llist_a_llist_prod_a_llist_a_llist_prod_bool_fun_fun$)) (=> (and (fun_app$bw (fun_app$by (llist_all2$a ?v0) ?v1) ?v2) (forall ((?v4 A_llist_a_llist_prod$) (?v5 A_llist_a_llist_prod$)) (=> (and (fun_app$i (member$ ?v4) (lset$ ?v1)) (and (fun_app$i (member$ ?v5) (lset$ ?v2)) (fun_app$h (fun_app$r ?v0 ?v4) ?v5))) (fun_app$h (fun_app$r ?v3 ?v4) ?v5)))) (fun_app$bw (fun_app$by (llist_all2$a ?v3) ?v1) ?v2))) :named a403))
+(assert (! (forall ((?v0 A_llist$)) (less_eq$a (lset$a (ltl$ ?v0)) (lset$a ?v0))) :named a404))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_set$) (?v1 A_llist_a_llist_prod_bool_fun$) (?v2 A_llist_a_llist_prod_bool_fun$)) (= (fun_app$i (less_eq$ ?v0) (collect$ (fun_app$t (uwr$ ?v1) ?v2))) (and (fun_app$i (less_eq$ ?v0) (collect$ ?v1)) (fun_app$i (less_eq$ ?v0) (collect$ ?v2))))) :named a405))
+(assert (! (forall ((?v0 A_llist_a_llist_prod$) (?v1 A_llist_a_llist_prod_set$) (?v2 A_llist_a_llist_prod_set$) (?v3 A_llist_a_llist_prod_bool_fun$)) (=> (and (fun_app$i (member$ ?v0) ?v1) (fun_app$i (less_eq$ ?v1) (collect$ (fun_app$t (uws$ ?v2) ?v3)))) (fun_app$h ?v3 ?v0))) :named a406))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_set$) (?v1 A_llist_a_llist_prod_set$) (?v2 A_llist_a_llist_prod_bool_fun$) (?v3 A_llist_a_llist_prod_bool_fun$)) (=> (and (fun_app$i (less_eq$ ?v0) ?v1) (forall ((?v4 A_llist_a_llist_prod$)) (=> (and (fun_app$i (member$ ?v4) ?v0) (fun_app$h ?v2 ?v4)) (fun_app$h ?v3 ?v4)))) (fun_app$i (less_eq$ (collect$ (fun_app$t (uws$ ?v0) ?v2))) (collect$ (fun_app$t (uws$ ?v1) ?v3))))) :named a407))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_set$) (?v1 A_llist_a_llist_prod_set$)) (= (fun_app$i (less_eq$ ?v0) ?v1) (fun_app$bk (less_eq$b (uui$ ?v0)) (uui$ ?v1)))) :named a408))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_set$) (?v1 A_llist_a_llist_prod_set$)) (= (fun_app$bk (less_eq$b (uui$ ?v0)) (uui$ ?v1)) (fun_app$i (less_eq$ ?v0) ?v1))) :named a409))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_set$) (?v1 A_llist_a_llist_prod_set$)) (= (less_eq$c (uvz$ ?v0) (uvz$ ?v1)) (fun_app$i (less_eq$ ?v0) ?v1))) :named a410))
+(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$) (?v2 A_llist_a_llist_prod_set$) (?v3 A_llist$)) (=> (and (fun_app$i (member$ (pair$ ?v0 ?v1)) ?v2) (= ?v3 ?v1)) (fun_app$i (member$ (pair$ ?v0 ?v3)) ?v2))) :named a411))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_set$) (?v1 A_llist_a_llist_prod_bool_fun$)) (fun_app$i (less_eq$ (collect$ (fun_app$t (uws$ ?v0) ?v1))) ?v0)) :named a412))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_set$) (?v1 A_llist_a_llist_prod_set$) (?v2 A_llist_a_llist_prod_bool_fun$)) (=> (fun_app$i (less_eq$ ?v0) ?v1) (= (fun_app$i (less_eq$ ?v0) (collect$ (fun_app$t (uws$ ?v1) ?v2))) (forall ((?v3 A_llist_a_llist_prod$)) (=> (fun_app$i (member$ ?v3) ?v0) (fun_app$h ?v2 ?v3)))))) :named a413))
+(assert (! (forall ((?v0 A_llist_a_llist_bool_fun_fun$) (?v1 A_llist_a_llist_bool_fun_fun$)) (=> (less_eq$c ?v0 ?v1) (fun_app$i (less_eq$ (collect$ (fun_app$ad uncurry$a ?v0))) (collect$ (fun_app$ad uncurry$a ?v1))))) :named a414))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_set$) (?v1 A_llist_a_llist_prod_set$)) (=> (and (fun_app$i (less_eq$ ?v0) (collect$ (fun_app$ad uncurry$a (in_rel$ ?v1)))) (=> (fun_app$i (less_eq$ ?v0) ?v1) false)) false)) :named a415))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_set$) (?v1 A_llist$) (?v2 A_llist$)) (! (= (fun_app$l (fun_app$m (in_rel$ ?v0) ?v1) ?v2) (fun_app$i (member$ (pair$ ?v1 ?v2)) ?v0)) :pattern ((fun_app$l (fun_app$m (in_rel$ ?v0) ?v1) ?v2)))) :named a416))
+(assert (! (forall ((?v0 A_llist_a_llist_bool_fun_fun$)) (= (in_rel$ (collect$ (fun_app$ad uncurry$a ?v0))) ?v0)) :named a417))
+(assert (! (forall ((?v0 A_llist_a_llist_prod_set$) (?v1 A_llist_a_llist_prod_set$)) (=> (fun_app$i (less_eq$ ?v0) ?v1) (fun_app$i (less_eq$ ?v0) (collect$ (fun_app$ad uncurry$a (in_rel$ ?v1)))))) :named a418))
+(assert (! (forall ((?v0 A_llist$) (?v1 A_llist_a_llist_prod_a_llist_fun$) (?v2 A_llist_a_llist_prod$) (?v3 A_llist$) (?v4 A_llist_a_llist_prod_a_llist_fun$) (?v5 A_llist_a_llist_prod_set$)) (=> (and (= ?v0 (fun_app$cp ?v1 ?v2)) (and (= ?v3 (fun_app$cp ?v4 ?v2)) (fun_app$i (member$ ?v2) ?v5))) (fun_app$i (member$ (pair$ ?v0 ?v3)) (image2$ ?v5 ?v1 ?v4)))) :named a419))
+(assert (! (forall ((?v0 A_llist$) (?v1 A_llist$)) (= (the$ (fun_app$ad uncurry$a (fun_app$aa (uwt$ ?v0) ?v1))) (pair$ ?v0 ?v1))) :named a420))
+(check-sat)
+