diff options
Diffstat (limited to 'test/regress/regress1/ho/auth0068.smt2')
| -rw-r--r-- | test/regress/regress1/ho/auth0068.smt2 | 491 |
1 files changed, 0 insertions, 491 deletions
diff --git a/test/regress/regress1/ho/auth0068.smt2 b/test/regress/regress1/ho/auth0068.smt2 deleted file mode 100644 index eb0bb5d36..000000000 --- a/test/regress/regress1/ho/auth0068.smt2 +++ /dev/null @@ -1,491 +0,0 @@ -; COMMAND-LINE: --uf-ho -; EXPECT: unsat -(set-logic ALL) -(set-info :status unsat) -(declare-sort Msg$ 0) -(declare-sort Nat$ 0) -(declare-sort Agent$ 0) -(declare-sort Event$ 0) -(declare-sort Msg_set$ 0) -(declare-sort Msg_list$ 0) -(declare-sort Agent_set$ 0) -(declare-sort Event_set$ 0) -(declare-sort Agent_list$ 0) -(declare-sort Event_list$ 0) -(declare-sort Event_option$ 0) -(declare-sort Msg_list_set$ 0) -(declare-sort Agent_list_set$ 0) -(declare-sort Event_list_set$ 0) -(declare-sort Event_list_list$ 0) -(declare-fun p$ () (-> Event$ Bool)) -(declare-fun uu$ ((-> Msg$ Bool) (-> Msg$ Bool) Msg$) Bool) -(declare-fun bad$ () Agent_set$) -(declare-fun nil$ () Event_list$) -(declare-fun set$ (Event_list$) Event_set$) -(declare-fun spy$ () Agent$) -(declare-fun uua$ (Event_set$ (-> Event$ Bool) Event$) Bool) -(declare-fun uub$ (Agent_set$ (-> Agent$ Bool) Agent$) Bool) -(declare-fun uuc$ (Msg_set$ (-> Msg$ Bool) Msg$) Bool) -(declare-fun uud$ (Event_set$ Event$) Bool) -(declare-fun uue$ (Agent_set$ Agent$) Bool) -(declare-fun uuf$ (Msg_set$ Msg$) Bool) -(declare-fun uug$ (Event$ Event_list$) Bool) -(declare-fun uuh$ (Event$ Event_list$) Bool) -(declare-fun uui$ ((-> Event$ Bool) Event$ Event$) Bool) -(declare-fun uuj$ (Event_list_set$ Event_list$ Event$) Bool) -(declare-fun uuk$ (Msg$ (-> Msg$ Bool) Msg$) Bool) -(declare-fun uul$ (Msg$ Msg_set$ Msg$) Bool) -(declare-fun uum$ (Event$ Event_set$ Event$) Bool) -(declare-fun uun$ (Agent$ Agent_set$ Agent$) Bool) -(declare-fun uuo$ (Event_list$ Agent$ Agent$ Msg$) Msg_set$) -(declare-fun uup$ (Event_list$ Agent$ Msg$) Msg_set$) -(declare-fun uuq$ (Event_list$ Agent$ Msg$) Msg_set$) -(declare-fun uur$ (Agent$ Event_list$ Agent$ Agent$ Msg$) Msg_set$) -(declare-fun uus$ (Agent$ Event_list$ Agent$ Msg$) Msg_set$) -(declare-fun bind$ (Event_list$ (-> Event$ Event_list$)) Event_list$) -(declare-fun cons$ (Event$ Event_list$) Event_list$) -(declare-fun gets$ (Agent$ Msg$) Event$) -(declare-fun maps$ ((-> Event$ Event_list$)) (-> Event_list$ Event_list$)) -(declare-fun nil$a () Event_list_list$) -(declare-fun nil$b () Msg_list$) -(declare-fun nil$c () Agent_list$) -(declare-fun null$ (Event_list$) Bool) -(declare-fun says$ (Agent$ Agent$ Msg$) Event$) -(declare-fun set$a (Msg_list$) Msg_set$) -(declare-fun set$b (Agent_list$) Agent_set$) -(declare-fun succ$ (Event_list_set$ Event_list$) Event_set$) -(declare-fun cons$a (Event_list$ Event_list_list$) Event_list_list$) -(declare-fun cons$b (Msg$ Msg_list$) Msg_list$) -(declare-fun cons$c (Agent$ Agent_list$) Agent_list$) -(declare-fun knows$ (Agent$ Event_list$) Msg_set$) -(declare-fun notes$ (Agent$ Msg$) Event$) -(declare-fun succ$a (Msg_list_set$ Msg_list$) Msg_set$) -(declare-fun succ$b (Agent_list_set$ Agent_list$) Agent_set$) -(declare-fun append$ (Event_list$ Event_list$) Event_list$) -(declare-fun insert$ (Msg$ Msg_set$) Msg_set$) -(declare-fun member$ (Agent$ Agent_set$) Bool) -(declare-fun splice$ (Event_list$) (-> Event_list$ Event_list$)) -(declare-fun append$a (Msg_list$ Msg_list$) Msg_list$) -(declare-fun append$b (Agent_list$ Agent_list$) Agent_list$) -(declare-fun collect$ ((-> Msg$ Bool)) Msg_set$) -(declare-fun insert$a (Event$) (-> Event_list$ Event_list$)) -(declare-fun insert$b (Event$ Event_set$) Event_set$) -(declare-fun insert$c (Agent$ Agent_set$) Agent_set$) -(declare-fun insert$d (Msg$ Msg_list$) Msg_list$) -(declare-fun insert$e (Agent$ Agent_list$) Agent_list$) -(declare-fun less_eq$ (Msg_set$ Msg_set$) Bool) -(declare-fun list_ex$ ((-> Event$ Bool)) (-> Event_list$ Bool)) -(declare-fun member$a (Msg$ Msg_set$) Bool) -(declare-fun member$b (Event$ Event_set$) Bool) -(declare-fun member$c (Event_list$ Event_list_set$) Bool) -(declare-fun member$d (Event_list$ Event$) Bool) -(declare-fun member$e (Msg_list$ Msg_list_set$) Bool) -(declare-fun member$f (Agent_list$ Agent_list_set$) Bool) -(declare-fun member$g (Msg_list$ Msg$) Bool) -(declare-fun member$h (Agent_list$ Agent$) Bool) -(declare-fun rotate1$ (Event_list$) Event_list$) -(declare-fun subseqs$ (Event_list$) Event_list_list$) -(declare-fun antimono$ ((-> Msg_set$ Msg_set$)) Bool) -(declare-fun collect$a ((-> Event$ Bool)) Event_set$) -(declare-fun collect$b ((-> Agent$ Bool)) Agent_set$) -(declare-fun greatest$ ((-> Msg_set$ Bool)) Msg_set$) -(declare-fun less_eq$a (Event_set$ Event_set$) Bool) -(declare-fun less_eq$b (Agent_set$ Agent_set$) Bool) -(declare-fun less_eq$c ((-> Event$ Bool) (-> Event$ Bool)) Bool) -(declare-fun less_eq$d ((-> Agent$ Bool) (-> Agent$ Bool)) Bool) -(declare-fun less_eq$e ((-> Msg$ Bool) (-> Msg$ Bool)) Bool) -(declare-fun less_eq$f ((-> Bool Msg_set$) (-> Bool Msg_set$)) Bool) -(declare-fun list_all$ ((-> Event$ Bool) Event_list$) Bool) -(declare-fun list_ex$a ((-> Msg$ Bool) Msg_list$) Bool) -(declare-fun list_ex$b ((-> Agent$ Bool) Agent_list$) Bool) -(declare-fun list_ex1$ ((-> Event$ Bool)) (-> Event_list$ Bool)) -(declare-fun case_list$ (Bool (-> Event$ (-> Event_list$ Bool)) Event_list$) Bool) -(declare-fun initState$ (Agent$) Msg_set$) -(declare-fun list_all$a ((-> Msg$ Bool) Msg_list$) Bool) -(declare-fun list_all$b ((-> Agent$ Bool) Agent_list$) Bool) -(declare-fun list_ex1$a ((-> Msg$ Bool) Msg_list$) Bool) -(declare-fun list_ex1$b ((-> Agent$ Bool) Agent_list$) Bool) -(declare-fun takeWhile$ ((-> Event$ Bool) Event_list$) Event_list$) -(declare-fun case_event$ ((-> Agent$ (-> Agent$ (-> Msg$ Msg_set$))) (-> Agent$ (-> Msg$ Msg_set$)) (-> Agent$ (-> Msg$ Msg_set$)) Event$) Msg_set$) -(declare-fun gen_length$ (Nat$) (-> Event_list$ Nat$)) -(declare-fun map_filter$ ((-> Event$ Event_option$)) (-> Event_list$ Event_list$)) -(declare-fun takeWhile$a ((-> Msg$ Bool) Msg_list$) Msg_list$) -(declare-fun takeWhile$b ((-> Agent$ Bool) Agent_list$) Agent_list$) -(declare-fun product_lists$ (Event_list_list$) Event_list_list$) -(assert (! (forall ((?v0 Agent_set$) (?v1 Agent$)) (! (= (uue$ ?v0 ?v1) (member$ ?v1 ?v0)) :pattern ((uue$ ?v0 ?v1)))) :named a0)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg$)) (! (= (uuf$ ?v0 ?v1) (member$a ?v1 ?v0)) :pattern ((uuf$ ?v0 ?v1)))) :named a1)) -(assert (! (forall ((?v0 Event_set$) (?v1 Event$)) (! (= (uud$ ?v0 ?v1) (member$b ?v1 ?v0)) :pattern ((uud$ ?v0 ?v1)))) :named a2)) -(assert (! (forall ((?v0 Event_list$) (?v1 Agent$) (?v2 Msg$)) (! (= (uuq$ ?v0 ?v1 ?v2) (ite (member$ ?v1 bad$) (insert$ ?v2 (knows$ spy$ ?v0)) (knows$ spy$ ?v0))) :pattern ((uuq$ ?v0 ?v1 ?v2)))) :named a3)) -(assert (! (forall ((?v0 Event_list_set$) (?v1 Event_list$) (?v2 Event$)) (! (= (uuj$ ?v0 ?v1 ?v2) (member$c (append$ ?v1 (cons$ ?v2 nil$)) ?v0)) :pattern ((uuj$ ?v0 ?v1 ?v2)))) :named a4)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_set$) (?v2 Agent$)) (! (= (uun$ ?v0 ?v1 ?v2) (or (= ?v2 ?v0) (member$ ?v2 ?v1))) :pattern ((uun$ ?v0 ?v1 ?v2)))) :named a5)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_set$) (?v2 Msg$)) (! (= (uul$ ?v0 ?v1 ?v2) (or (= ?v2 ?v0) (member$a ?v2 ?v1))) :pattern ((uul$ ?v0 ?v1 ?v2)))) :named a6)) -(assert (! (forall ((?v0 Event$) (?v1 Event_set$) (?v2 Event$)) (! (= (uum$ ?v0 ?v1 ?v2) (or (= ?v2 ?v0) (member$b ?v2 ?v1))) :pattern ((uum$ ?v0 ?v1 ?v2)))) :named a7)) -(assert (! (forall ((?v0 Agent_set$) (?v1 (-> Agent$ Bool)) (?v2 Agent$)) (! (= (uub$ ?v0 ?v1 ?v2) (and (member$ ?v2 ?v0) (?v1 ?v2))) :pattern ((uub$ ?v0 ?v1 ?v2)))) :named a8)) -(assert (! (forall ((?v0 Msg_set$) (?v1 (-> Msg$ Bool)) (?v2 Msg$)) (! (= (uuc$ ?v0 ?v1 ?v2) (and (member$a ?v2 ?v0) (?v1 ?v2))) :pattern ((uuc$ ?v0 ?v1 ?v2)))) :named a9)) -(assert (! (forall ((?v0 Event_set$) (?v1 (-> Event$ Bool)) (?v2 Event$)) (! (= (uua$ ?v0 ?v1 ?v2) (and (member$b ?v2 ?v0) (?v1 ?v2))) :pattern ((uua$ ?v0 ?v1 ?v2)))) :named a10)) -(assert (! (forall ((?v0 (-> Msg$ Bool)) (?v1 (-> Msg$ Bool)) (?v2 Msg$)) (! (= (uu$ ?v0 ?v1 ?v2) (and (?v0 ?v2) (?v1 ?v2))) :pattern ((uu$ ?v0 ?v1 ?v2)))) :named a11)) -(assert (! (forall ((?v0 Msg$) (?v1 (-> Msg$ Bool)) (?v2 Msg$)) (! (= (uuk$ ?v0 ?v1 ?v2) (=> (not (= ?v2 ?v0)) (?v1 ?v2))) :pattern ((uuk$ ?v0 ?v1 ?v2)))) :named a12)) -(assert (! (forall ((?v0 (-> Event$ Bool)) (?v1 Event$) (?v2 Event$)) (! (= (uui$ ?v0 ?v1 ?v2) (or (not (?v0 ?v2)) (= ?v1 ?v2))) :pattern ((uui$ ?v0 ?v1 ?v2)))) :named a13)) -(assert (! (forall ((?v0 Event_list$) (?v1 Agent$) (?v2 Msg$)) (! (= (uup$ ?v0 ?v1 ?v2) (knows$ spy$ ?v0)) :pattern ((uup$ ?v0 ?v1 ?v2)))) :named a14)) -(assert (! (forall ((?v0 Agent$) (?v1 Event_list$) (?v2 Agent$) (?v3 Msg$)) (! (= (uus$ ?v0 ?v1 ?v2 ?v3) (ite (= ?v2 ?v0) (insert$ ?v3 (knows$ ?v0 ?v1)) (knows$ ?v0 ?v1))) :pattern ((uus$ ?v0 ?v1 ?v2 ?v3)))) :named a15)) -(assert (! (forall ((?v0 Event_list$) (?v1 Agent$) (?v2 Agent$) (?v3 Msg$)) (! (= (uuo$ ?v0 ?v1 ?v2 ?v3) (insert$ ?v3 (knows$ spy$ ?v0))) :pattern ((uuo$ ?v0 ?v1 ?v2 ?v3)))) :named a16)) -(assert (! (forall ((?v0 Agent$) (?v1 Event_list$) (?v2 Agent$) (?v3 Agent$) (?v4 Msg$)) (! (= (uur$ ?v0 ?v1 ?v2 ?v3 ?v4) (ite (= ?v2 ?v0) (insert$ ?v4 (knows$ ?v0 ?v1)) (knows$ ?v0 ?v1))) :pattern ((uur$ ?v0 ?v1 ?v2 ?v3 ?v4)))) :named a17)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$)) (! (= (uug$ ?v0 ?v1) false) :pattern ((uug$ ?v0 ?v1)))) :named a18)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$)) (! (= (uuh$ ?v0 ?v1) true) :pattern ((uuh$ ?v0 ?v1)))) :named a19)) -(assert (! (not (less_eq$ (knows$ spy$ (takeWhile$ p$ nil$)) (knows$ spy$ nil$))) :named a20)) -(assert (! (forall ((?v0 (-> Event$ Bool)) (?v1 Event_list$)) (= (takeWhile$ ?v0 (takeWhile$ ?v0 ?v1)) (takeWhile$ ?v0 ?v1))) :named a21)) -(assert (! (forall ((?v0 Event_set$) (?v1 Event_set$)) (=> (forall ((?v2 Event$)) (=> (member$b ?v2 ?v0) (member$b ?v2 ?v1))) (less_eq$a ?v0 ?v1))) :named a22)) -(assert (! (forall ((?v0 Agent_set$) (?v1 Agent_set$)) (=> (forall ((?v2 Agent$)) (=> (member$ ?v2 ?v0) (member$ ?v2 ?v1))) (less_eq$b ?v0 ?v1))) :named a23)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$)) (=> (forall ((?v2 Msg$)) (=> (member$a ?v2 ?v0) (member$a ?v2 ?v1))) (less_eq$ ?v0 ?v1))) :named a24)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$)) (=> (and (less_eq$ ?v0 ?v1) (less_eq$ ?v1 ?v0)) (= ?v0 ?v1))) :named a25)) -(assert (! (forall ((?v0 Msg_set$)) (less_eq$ ?v0 ?v0)) :named a26)) -(assert (! (forall ((?v0 (-> Event$ Bool))) (! (= (takeWhile$ ?v0 nil$) nil$) :pattern ((takeWhile$ ?v0)))) :named a27)) -(assert (! (forall ((?v0 Msg_set$) (?v1 (-> Msg$ Bool)) (?v2 (-> Msg$ Bool))) (= (less_eq$ ?v0 (collect$ (uu$ ?v1 ?v2))) (and (less_eq$ ?v0 (collect$ ?v1)) (less_eq$ ?v0 (collect$ ?v2))))) :named a28)) -(assert (! (forall ((?v0 Event$) (?v1 Event_set$) (?v2 Event_set$) (?v3 (-> Event$ Bool))) (=> (and (member$b ?v0 ?v1) (less_eq$a ?v1 (collect$a (uua$ ?v2 ?v3)))) (?v3 ?v0))) :named a29)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_set$) (?v2 Agent_set$) (?v3 (-> Agent$ Bool))) (=> (and (member$ ?v0 ?v1) (less_eq$b ?v1 (collect$b (uub$ ?v2 ?v3)))) (?v3 ?v0))) :named a30)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_set$) (?v2 Msg_set$) (?v3 (-> Msg$ Bool))) (=> (and (member$a ?v0 ?v1) (less_eq$ ?v1 (collect$ (uuc$ ?v2 ?v3)))) (?v3 ?v0))) :named a31)) -(assert (! (forall ((?v0 Event_set$) (?v1 (-> Event$ Bool))) (less_eq$a (collect$a (uua$ ?v0 ?v1)) ?v0)) :named a32)) -(assert (! (forall ((?v0 Agent_set$) (?v1 (-> Agent$ Bool))) (less_eq$b (collect$b (uub$ ?v0 ?v1)) ?v0)) :named a33)) -(assert (! (forall ((?v0 Msg_set$) (?v1 (-> Msg$ Bool))) (less_eq$ (collect$ (uuc$ ?v0 ?v1)) ?v0)) :named a34)) -(assert (! (forall ((?v0 Event_set$) (?v1 Event_set$) (?v2 (-> Event$ Bool)) (?v3 (-> Event$ Bool))) (=> (and (less_eq$a ?v0 ?v1) (forall ((?v4 Event$)) (=> (and (member$b ?v4 ?v0) (?v2 ?v4)) (?v3 ?v4)))) (less_eq$a (collect$a (uua$ ?v0 ?v2)) (collect$a (uua$ ?v1 ?v3))))) :named a35)) -(assert (! (forall ((?v0 Agent_set$) (?v1 Agent_set$) (?v2 (-> Agent$ Bool)) (?v3 (-> Agent$ Bool))) (=> (and (less_eq$b ?v0 ?v1) (forall ((?v4 Agent$)) (=> (and (member$ ?v4 ?v0) (?v2 ?v4)) (?v3 ?v4)))) (less_eq$b (collect$b (uub$ ?v0 ?v2)) (collect$b (uub$ ?v1 ?v3))))) :named a36)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$) (?v2 (-> Msg$ Bool)) (?v3 (-> Msg$ Bool))) (=> (and (less_eq$ ?v0 ?v1) (forall ((?v4 Msg$)) (=> (and (member$a ?v4 ?v0) (?v2 ?v4)) (?v3 ?v4)))) (less_eq$ (collect$ (uuc$ ?v0 ?v2)) (collect$ (uuc$ ?v1 ?v3))))) :named a37)) -(assert (! (forall ((?v0 Event_set$) (?v1 Event_set$) (?v2 (-> Event$ Bool))) (=> (less_eq$a ?v0 ?v1) (= (less_eq$a ?v0 (collect$a (uua$ ?v1 ?v2))) (forall ((?v3 Event$)) (=> (member$b ?v3 ?v0) (?v2 ?v3)))))) :named a38)) -(assert (! (forall ((?v0 Agent_set$) (?v1 Agent_set$) (?v2 (-> Agent$ Bool))) (=> (less_eq$b ?v0 ?v1) (= (less_eq$b ?v0 (collect$b (uub$ ?v1 ?v2))) (forall ((?v3 Agent$)) (=> (member$ ?v3 ?v0) (?v2 ?v3)))))) :named a39)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$) (?v2 (-> Msg$ Bool))) (=> (less_eq$ ?v0 ?v1) (= (less_eq$ ?v0 (collect$ (uuc$ ?v1 ?v2))) (forall ((?v3 Msg$)) (=> (member$a ?v3 ?v0) (?v2 ?v3)))))) :named a40)) -(assert (! (forall ((?v0 Event_list$)) (=> (and (=> (= ?v0 nil$) false) (=> (not (= ?v0 nil$)) false)) false)) :named a41)) -(assert (! (forall ((?v0 Event_set$) (?v1 Event_set$) (?v2 Event$)) (=> (and (less_eq$a ?v0 ?v1) (member$b ?v2 ?v0)) (member$b ?v2 ?v1))) :named a42)) -(assert (! (forall ((?v0 Agent_set$) (?v1 Agent_set$) (?v2 Agent$)) (=> (and (less_eq$b ?v0 ?v1) (member$ ?v2 ?v0)) (member$ ?v2 ?v1))) :named a43)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$) (?v2 Msg$)) (=> (and (less_eq$ ?v0 ?v1) (member$a ?v2 ?v0)) (member$a ?v2 ?v1))) :named a44)) -(assert (! (forall ((?v0 Event_set$) (?v1 Event_set$)) (= (less_eq$a ?v0 ?v1) (less_eq$c (uud$ ?v0) (uud$ ?v1)))) :named a45)) -(assert (! (forall ((?v0 Agent_set$) (?v1 Agent_set$)) (= (less_eq$b ?v0 ?v1) (less_eq$d (uue$ ?v0) (uue$ ?v1)))) :named a46)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$)) (= (less_eq$ ?v0 ?v1) (less_eq$e (uuf$ ?v0) (uuf$ ?v1)))) :named a47)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$)) (=> (and (less_eq$ ?v0 ?v1) (less_eq$ ?v1 ?v0)) (= ?v1 ?v0))) :named a48)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$) (?v2 Msg_set$)) (=> (and (less_eq$ ?v0 ?v1) (less_eq$ ?v2 ?v0)) (less_eq$ ?v2 ?v1))) :named a49)) -(assert (! (forall ((?v0 Msg_set$)) (less_eq$ ?v0 ?v0)) :named a50)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$) (?v2 Msg_set$)) (=> (and (less_eq$ ?v0 ?v1) (less_eq$ ?v1 ?v2)) (less_eq$ ?v0 ?v2))) :named a51)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$)) (=> (and (less_eq$ ?v0 ?v1) (less_eq$ ?v1 ?v0)) (= ?v0 ?v1))) :named a52)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$) (?v2 Msg_set$)) (=> (and (less_eq$ ?v0 ?v1) (= ?v1 ?v2)) (less_eq$ ?v0 ?v2))) :named a53)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$) (?v2 Msg_set$)) (=> (and (= ?v0 ?v1) (less_eq$ ?v1 ?v2)) (less_eq$ ?v0 ?v2))) :named a54)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$)) (! (=> (less_eq$ ?v0 ?v1) (= (less_eq$ ?v1 ?v0) (= ?v1 ?v0))) :pattern ((less_eq$ ?v1 ?v0)))) :named a55)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$) (?v2 Msg_set$)) (=> (and (less_eq$ ?v0 ?v1) (less_eq$ ?v1 ?v2)) (less_eq$ ?v0 ?v2))) :named a56)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$)) (=> (= ?v0 ?v1) (less_eq$ ?v0 ?v1))) :named a57)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$)) (=> (and (less_eq$ ?v0 ?v1) (less_eq$ ?v1 ?v0)) (= ?v0 ?v1))) :named a58)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$)) (= (= ?v0 ?v1) (and (less_eq$ ?v0 ?v1) (less_eq$ ?v1 ?v0)))) :named a59)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$) (?v2 (-> Msg_set$ Msg_set$)) (?v3 Msg_set$)) (=> (and (less_eq$ ?v0 ?v1) (and (= (?v2 ?v1) ?v3) (forall ((?v4 Msg_set$) (?v5 Msg_set$)) (=> (less_eq$ ?v4 ?v5) (less_eq$ (?v2 ?v4) (?v2 ?v5)))))) (less_eq$ (?v2 ?v0) ?v3))) :named a60)) -(assert (! (forall ((?v0 Msg_set$) (?v1 (-> Msg_set$ Msg_set$)) (?v2 Msg_set$) (?v3 Msg_set$)) (=> (and (= ?v0 (?v1 ?v2)) (and (less_eq$ ?v2 ?v3) (forall ((?v4 Msg_set$) (?v5 Msg_set$)) (=> (less_eq$ ?v4 ?v5) (less_eq$ (?v1 ?v4) (?v1 ?v5)))))) (less_eq$ ?v0 (?v1 ?v3)))) :named a61)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$) (?v2 (-> Msg_set$ Msg_set$)) (?v3 Msg_set$)) (=> (and (less_eq$ ?v0 ?v1) (and (less_eq$ (?v2 ?v1) ?v3) (forall ((?v4 Msg_set$) (?v5 Msg_set$)) (=> (less_eq$ ?v4 ?v5) (less_eq$ (?v2 ?v4) (?v2 ?v5)))))) (less_eq$ (?v2 ?v0) ?v3))) :named a62)) -(assert (! (forall ((?v0 Msg_set$) (?v1 (-> Msg_set$ Msg_set$)) (?v2 Msg_set$) (?v3 Msg_set$)) (=> (and (less_eq$ ?v0 (?v1 ?v2)) (and (less_eq$ ?v2 ?v3) (forall ((?v4 Msg_set$) (?v5 Msg_set$)) (=> (less_eq$ ?v4 ?v5) (less_eq$ (?v1 ?v4) (?v1 ?v5)))))) (less_eq$ ?v0 (?v1 ?v3)))) :named a63)) -(assert (! (forall ((?v0 (-> Msg$ Bool)) (?v1 (-> Msg$ Bool))) (= (less_eq$ (collect$ ?v0) (collect$ ?v1)) (forall ((?v2 Msg$)) (=> (?v0 ?v2) (?v1 ?v2))))) :named a64)) -(assert (! (forall ((?v0 Event_set$) (?v1 Event_set$) (?v2 Event$)) (=> (and (less_eq$a ?v0 ?v1) (not (member$b ?v2 ?v1))) (not (member$b ?v2 ?v0)))) :named a65)) -(assert (! (forall ((?v0 Agent_set$) (?v1 Agent_set$) (?v2 Agent$)) (=> (and (less_eq$b ?v0 ?v1) (not (member$ ?v2 ?v1))) (not (member$ ?v2 ?v0)))) :named a66)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$) (?v2 Msg$)) (=> (and (less_eq$ ?v0 ?v1) (not (member$a ?v2 ?v1))) (not (member$a ?v2 ?v0)))) :named a67)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$)) (= (= ?v0 ?v1) (and (less_eq$ ?v0 ?v1) (less_eq$ ?v1 ?v0)))) :named a68)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$) (?v2 Msg_set$)) (=> (and (less_eq$ ?v0 ?v1) (less_eq$ ?v1 ?v2)) (less_eq$ ?v0 ?v2))) :named a69)) -(assert (! (forall ((?v0 (-> Msg$ Bool)) (?v1 (-> Msg$ Bool))) (=> (forall ((?v2 Msg$)) (=> (?v0 ?v2) (?v1 ?v2))) (less_eq$ (collect$ ?v0) (collect$ ?v1)))) :named a70)) -(assert (! (forall ((?v0 Msg_set$)) (less_eq$ ?v0 ?v0)) :named a71)) -(assert (! (forall ((?v0 Event$) (?v1 Event_set$) (?v2 Event_set$)) (=> (and (member$b ?v0 ?v1) (less_eq$a ?v1 ?v2)) (member$b ?v0 ?v2))) :named a72)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_set$) (?v2 Agent_set$)) (=> (and (member$ ?v0 ?v1) (less_eq$b ?v1 ?v2)) (member$ ?v0 ?v2))) :named a73)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_set$) (?v2 Msg_set$)) (=> (and (member$a ?v0 ?v1) (less_eq$ ?v1 ?v2)) (member$a ?v0 ?v2))) :named a74)) -(assert (! (forall ((?v0 Event_set$) (?v1 Event_set$)) (= (less_eq$a ?v0 ?v1) (forall ((?v2 Event$)) (=> (member$b ?v2 ?v0) (member$b ?v2 ?v1))))) :named a75)) -(assert (! (forall ((?v0 Agent_set$) (?v1 Agent_set$)) (= (less_eq$b ?v0 ?v1) (forall ((?v2 Agent$)) (=> (member$ ?v2 ?v0) (member$ ?v2 ?v1))))) :named a76)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$)) (= (less_eq$ ?v0 ?v1) (forall ((?v2 Msg$)) (=> (member$a ?v2 ?v0) (member$a ?v2 ?v1))))) :named a77)) -(assert (! (forall ((?v0 Msg$) (?v1 (-> Msg$ Bool))) (= (member$a ?v0 (collect$ ?v1)) (?v1 ?v0))) :named a78)) -(assert (! (forall ((?v0 Event$) (?v1 (-> Event$ Bool))) (= (member$b ?v0 (collect$a ?v1)) (?v1 ?v0))) :named a79)) -(assert (! (forall ((?v0 Agent$) (?v1 (-> Agent$ Bool))) (= (member$ ?v0 (collect$b ?v1)) (?v1 ?v0))) :named a80)) -(assert (! (forall ((?v0 Msg_set$)) (= (collect$ (uuf$ ?v0)) ?v0)) :named a81)) -(assert (! (forall ((?v0 Event_set$)) (= (collect$a (uud$ ?v0)) ?v0)) :named a82)) -(assert (! (forall ((?v0 Agent_set$)) (= (collect$b (uue$ ?v0)) ?v0)) :named a83)) -(assert (! (forall ((?v0 Event$) (?v1 Event_set$) (?v2 Event_set$)) (=> (and (member$b ?v0 ?v1) (less_eq$a ?v1 ?v2)) (member$b ?v0 ?v2))) :named a84)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_set$) (?v2 Agent_set$)) (=> (and (member$ ?v0 ?v1) (less_eq$b ?v1 ?v2)) (member$ ?v0 ?v2))) :named a85)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_set$) (?v2 Msg_set$)) (=> (and (member$a ?v0 ?v1) (less_eq$ ?v1 ?v2)) (member$a ?v0 ?v2))) :named a86)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$)) (=> (= ?v0 ?v1) (less_eq$ ?v1 ?v0))) :named a87)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$)) (=> (= ?v0 ?v1) (less_eq$ ?v0 ?v1))) :named a88)) -(assert (! (forall ((?v0 Event_set$) (?v1 Event_set$)) (= (less_eq$a ?v0 ?v1) (forall ((?v2 Event$)) (=> (member$b ?v2 ?v0) (member$b ?v2 ?v1))))) :named a89)) -(assert (! (forall ((?v0 Agent_set$) (?v1 Agent_set$)) (= (less_eq$b ?v0 ?v1) (forall ((?v2 Agent$)) (=> (member$ ?v2 ?v0) (member$ ?v2 ?v1))))) :named a90)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$)) (= (less_eq$ ?v0 ?v1) (forall ((?v2 Msg$)) (=> (member$a ?v2 ?v0) (member$a ?v2 ?v1))))) :named a91)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$)) (=> (and (= ?v0 ?v1) (=> (and (less_eq$ ?v0 ?v1) (less_eq$ ?v1 ?v0)) false)) false)) :named a92)) -(assert (! (forall ((?v0 Event_set$) (?v1 Event_set$) (?v2 Event$)) (=> (and (less_eq$a ?v0 ?v1) (and (=> (not (member$b ?v2 ?v0)) false) (=> (member$b ?v2 ?v1) false))) false)) :named a93)) -(assert (! (forall ((?v0 Agent_set$) (?v1 Agent_set$) (?v2 Agent$)) (=> (and (less_eq$b ?v0 ?v1) (and (=> (not (member$ ?v2 ?v0)) false) (=> (member$ ?v2 ?v1) false))) false)) :named a94)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$) (?v2 Msg$)) (=> (and (less_eq$ ?v0 ?v1) (and (=> (not (member$a ?v2 ?v0)) false) (=> (member$a ?v2 ?v1) false))) false)) :named a95)) -(assert (! (forall ((?v0 Event_set$) (?v1 Event_set$) (?v2 Event$)) (=> (and (less_eq$a ?v0 ?v1) (member$b ?v2 ?v0)) (member$b ?v2 ?v1))) :named a96)) -(assert (! (forall ((?v0 Agent_set$) (?v1 Agent_set$) (?v2 Agent$)) (=> (and (less_eq$b ?v0 ?v1) (member$ ?v2 ?v0)) (member$ ?v2 ?v1))) :named a97)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$) (?v2 Msg$)) (=> (and (less_eq$ ?v0 ?v1) (member$a ?v2 ?v0)) (member$a ?v2 ?v1))) :named a98)) -(assert (! (forall ((?v0 Event_set$) (?v1 Event_set$) (?v2 Event$)) (=> (and (less_eq$a ?v0 ?v1) (member$b ?v2 ?v0)) (member$b ?v2 ?v1))) :named a99)) -(assert (! (forall ((?v0 Agent_set$) (?v1 Agent_set$) (?v2 Agent$)) (=> (and (less_eq$b ?v0 ?v1) (member$ ?v2 ?v0)) (member$ ?v2 ?v1))) :named a100)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$) (?v2 Msg$)) (=> (and (less_eq$ ?v0 ?v1) (member$a ?v2 ?v0)) (member$a ?v2 ?v1))) :named a101)) -(assert (! (forall ((?v0 Event_set$) (?v1 Event_set$)) (= (less_eq$c (uud$ ?v0) (uud$ ?v1)) (less_eq$a ?v0 ?v1))) :named a102)) -(assert (! (forall ((?v0 Agent_set$) (?v1 Agent_set$)) (= (less_eq$d (uue$ ?v0) (uue$ ?v1)) (less_eq$b ?v0 ?v1))) :named a103)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$)) (= (less_eq$e (uuf$ ?v0) (uuf$ ?v1)) (less_eq$ ?v0 ?v1))) :named a104)) -(assert (! (forall ((?v0 (-> Event$ Bool))) (! (= (list_ex1$ ?v0 nil$) false) :pattern ((list_ex1$ ?v0)))) :named a105)) -(assert (! (forall ((?v0 (-> Event$ Event_list$))) (! (= (bind$ nil$ ?v0) nil$) :pattern ((bind$ nil$ ?v0)))) :named a106)) -(assert (! (forall ((?v0 (-> Msg_set$ Bool)) (?v1 Msg_set$)) (=> (and (?v0 ?v1) (forall ((?v2 Msg_set$)) (=> (?v0 ?v2) (less_eq$ ?v2 ?v1)))) (= (greatest$ ?v0) ?v1))) :named a107)) -(assert (! (forall ((?v0 (-> Msg_set$ Bool)) (?v1 Msg_set$) (?v2 (-> Msg_set$ Bool))) (=> (and (?v0 ?v1) (and (forall ((?v3 Msg_set$)) (=> (?v0 ?v3) (less_eq$ ?v3 ?v1))) (forall ((?v3 Msg_set$)) (=> (and (?v0 ?v3) (forall ((?v4 Msg_set$)) (=> (?v0 ?v4) (less_eq$ ?v4 ?v3)))) (?v2 ?v3))))) (?v2 (greatest$ ?v0)))) :named a108)) -(assert (! (forall ((?v0 Event$)) (! (= (member$d nil$ ?v0) false) :pattern ((member$d nil$ ?v0)))) :named a109)) -(assert (! (forall ((?v0 (-> Bool Msg_set$)) (?v1 (-> Bool Msg_set$))) (! (= (less_eq$f ?v0 ?v1) (and (less_eq$ (?v0 false) (?v1 false)) (less_eq$ (?v0 true) (?v1 true)))) :pattern ((less_eq$f ?v0 ?v1)))) :named a110)) -(assert (! (forall ((?v0 Nat$)) (! (= (gen_length$ ?v0 nil$) ?v0) :pattern ((gen_length$ ?v0)))) :named a111)) -(assert (! (forall ((?v0 (-> Event$ Event_list$))) (! (= (maps$ ?v0 nil$) nil$) :pattern ((maps$ ?v0)))) :named a112)) -(assert (! (forall ((?v0 Event_list$)) (= (= ?v0 nil$) (null$ ?v0))) :named a113)) -(assert (! (= (null$ nil$) true) :named a114)) -(assert (! (forall ((?v0 Event_list$)) (! (= (splice$ ?v0 nil$) ?v0) :pattern ((splice$ ?v0)))) :named a115)) -(assert (! (forall ((?v0 Event_list$)) (= (= (rotate1$ ?v0) nil$) (= ?v0 nil$))) :named a116)) -(assert (! (forall ((?v0 (-> Event$ Event_option$))) (! (= (map_filter$ ?v0 nil$) nil$) :pattern ((map_filter$ ?v0)))) :named a117)) -(assert (! (forall ((?v0 (-> Msg_set$ Msg_set$)) (?v1 Msg_set$) (?v2 Msg_set$)) (=> (and (antimono$ ?v0) (less_eq$ ?v1 ?v2)) (less_eq$ (?v0 ?v2) (?v0 ?v1)))) :named a118)) -(assert (! (= (rotate1$ nil$) nil$) :named a119)) -(assert (! (forall ((?v0 Event_list$)) (! (= (splice$ nil$ ?v0) ?v0) :pattern ((splice$ nil$ ?v0)))) :named a120)) -(assert (! (forall ((?v0 (-> Msg_set$ Msg_set$))) (= (antimono$ ?v0) (forall ((?v1 Msg_set$) (?v2 Msg_set$)) (=> (less_eq$ ?v1 ?v2) (less_eq$ (?v0 ?v2) (?v0 ?v1)))))) :named a121)) -(assert (! (forall ((?v0 (-> Msg_set$ Msg_set$))) (=> (forall ((?v1 Msg_set$) (?v2 Msg_set$)) (=> (less_eq$ ?v1 ?v2) (less_eq$ (?v0 ?v2) (?v0 ?v1)))) (antimono$ ?v0))) :named a122)) -(assert (! (forall ((?v0 (-> Msg_set$ Msg_set$)) (?v1 Msg_set$) (?v2 Msg_set$)) (=> (and (antimono$ ?v0) (and (less_eq$ ?v1 ?v2) (=> (less_eq$ (?v0 ?v2) (?v0 ?v1)) false))) false)) :named a123)) -(assert (! (forall ((?v0 Event_list$) (?v1 Event_list$) (?v2 Event_list$)) (=> (and (= (splice$ ?v0 ?v1) ?v2) (and (forall ((?v3 Event_list$)) (=> (and (= ?v0 nil$) (and (= ?v1 ?v3) (= ?v2 ?v3))) false)) (and (forall ((?v3 Event$) (?v4 Event_list$)) (=> (and (= ?v0 (cons$ ?v3 ?v4)) (and (= ?v1 nil$) (= ?v2 (cons$ ?v3 ?v4)))) false)) (forall ((?v3 Event$) (?v4 Event_list$) (?v5 Event$) (?v6 Event_list$)) (=> (and (= ?v0 (cons$ ?v3 ?v4)) (and (= ?v1 (cons$ ?v5 ?v6)) (= ?v2 (cons$ ?v3 (cons$ ?v5 (splice$ ?v4 ?v6)))))) false))))) false)) :named a124)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$)) (! (= (splice$ (cons$ ?v0 ?v1) nil$) (cons$ ?v0 ?v1)) :pattern ((cons$ ?v0 ?v1)))) :named a125)) -(assert (! (forall ((?v0 (-> Event$ Bool))) (! (= (list_ex$ ?v0 nil$) false) :pattern ((list_ex$ ?v0)))) :named a126)) -(assert (! (forall ((?v0 Event_list$)) (= (= ?v0 nil$) (case_list$ true uug$ ?v0))) :named a127)) -(assert (! (forall ((?v0 Event_list$)) (= (not (= ?v0 nil$)) (case_list$ false uuh$ ?v0))) :named a128)) -(assert (! (forall ((?v0 Agent$)) (! (= (knows$ ?v0 nil$) (initState$ ?v0)) :pattern ((knows$ ?v0)))) :named a129)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$) (?v2 Event$) (?v3 Event_list$)) (= (= (cons$ ?v0 ?v1) (cons$ ?v2 ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3)))) :named a130)) -(assert (! (forall ((?v0 (-> Event$ Bool)) (?v1 Event$) (?v2 Event_list$)) (! (= (list_ex$ ?v0 (cons$ ?v1 ?v2)) (or (?v0 ?v1) (list_ex$ ?v0 ?v2))) :pattern ((list_ex$ ?v0 (cons$ ?v1 ?v2))))) :named a131)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$)) (not (= (cons$ ?v0 ?v1) ?v1))) :named a132)) -(assert (! (forall ((?v0 Event_list_list$)) (=> (and (=> (= ?v0 nil$a) false) (and (forall ((?v1 Event_list_list$)) (=> (= ?v0 (cons$a nil$ ?v1)) false)) (forall ((?v1 Event$) (?v2 Event_list$) (?v3 Event_list_list$)) (=> (= ?v0 (cons$a (cons$ ?v1 ?v2) ?v3)) false)))) false)) :named a133)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$)) (not (= nil$ (cons$ ?v0 ?v1)))) :named a134)) -(assert (! (forall ((?v0 Event_list$) (?v1 Event$) (?v2 Event_list$)) (=> (= ?v0 (cons$ ?v1 ?v2)) (not (= ?v0 nil$)))) :named a135)) -(assert (! (forall ((?v0 Event_list$)) (=> (and (=> (= ?v0 nil$) false) (forall ((?v1 Event$) (?v2 Event_list$)) (=> (= ?v0 (cons$ ?v1 ?v2)) false))) false)) :named a136)) -(assert (! (forall ((?v0 Event_list$)) (= (not (= ?v0 nil$)) (exists ((?v1 Event$) (?v2 Event_list$)) (= ?v0 (cons$ ?v1 ?v2))))) :named a137)) -(assert (! (forall ((?v0 (-> Event_list$ (-> Event_list$ Bool))) (?v1 Event_list$) (?v2 Event_list$)) (=> (and (?v0 nil$ nil$) (and (forall ((?v3 Event$) (?v4 Event_list$)) (?v0 (cons$ ?v3 ?v4) nil$)) (and (forall ((?v3 Event$) (?v4 Event_list$)) (?v0 nil$ (cons$ ?v3 ?v4))) (forall ((?v3 Event$) (?v4 Event_list$) (?v5 Event$) (?v6 Event_list$)) (=> (?v0 ?v4 ?v6) (?v0 (cons$ ?v3 ?v4) (cons$ ?v5 ?v6))))))) (?v0 ?v1 ?v2))) :named a138)) -(assert (! (forall ((?v0 Event_list$)) (=> (and (=> (= ?v0 nil$) false) (and (forall ((?v1 Event$)) (=> (= ?v0 (cons$ ?v1 nil$)) false)) (forall ((?v1 Event$) (?v2 Event$) (?v3 Event_list$)) (=> (= ?v0 (cons$ ?v1 (cons$ ?v2 ?v3))) false)))) false)) :named a139)) -(assert (! (forall ((?v0 (-> Event_list$ Bool)) (?v1 Event_list$)) (=> (and (?v0 nil$) (and (forall ((?v2 Event$)) (?v0 (cons$ ?v2 nil$))) (forall ((?v2 Event$) (?v3 Event$) (?v4 Event_list$)) (=> (?v0 (cons$ ?v3 ?v4)) (?v0 (cons$ ?v2 (cons$ ?v3 ?v4))))))) (?v0 ?v1))) :named a140)) -(assert (! (forall ((?v0 Event_list$) (?v1 (-> Event_list$ Bool))) (=> (and (not (= ?v0 nil$)) (and (forall ((?v2 Event$)) (?v1 (cons$ ?v2 nil$))) (forall ((?v2 Event$) (?v3 Event_list$)) (=> (and (not (= ?v3 nil$)) (?v1 ?v3)) (?v1 (cons$ ?v2 ?v3)))))) (?v1 ?v0))) :named a141)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$) (?v2 Event$) (?v3 Event_list$)) (! (= (splice$ (cons$ ?v0 ?v1) (cons$ ?v2 ?v3)) (cons$ ?v0 (cons$ ?v2 (splice$ ?v1 ?v3)))) :pattern ((splice$ (cons$ ?v0 ?v1) (cons$ ?v2 ?v3))))) :named a142)) -(assert (! (forall ((?v0 Agent$) (?v1 Event_list$) (?v2 Event$)) (less_eq$ (knows$ ?v0 ?v1) (knows$ ?v0 (cons$ ?v2 ?v1)))) :named a143)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$)) (! (= (null$ (cons$ ?v0 ?v1)) false) :pattern ((cons$ ?v0 ?v1)))) :named a144)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$) (?v2 Event$)) (! (= (member$d (cons$ ?v0 ?v1) ?v2) (or (= ?v0 ?v2) (member$d ?v1 ?v2))) :pattern ((member$d (cons$ ?v0 ?v1) ?v2)))) :named a145)) -(assert (! (forall ((?v0 Agent$) (?v1 Event_list$)) (less_eq$ (initState$ ?v0) (knows$ ?v0 ?v1))) :named a146)) -(assert (! (forall ((?v0 (-> Event$ Bool)) (?v1 Event$) (?v2 Event_list$)) (! (= (takeWhile$ ?v0 (cons$ ?v1 ?v2)) (ite (?v0 ?v1) (cons$ ?v1 (takeWhile$ ?v0 ?v2)) nil$)) :pattern ((takeWhile$ ?v0 (cons$ ?v1 ?v2))))) :named a147)) -(assert (! (forall ((?v0 Event_list$) (?v1 Agent$) (?v2 Msg$)) (less_eq$ (knows$ spy$ ?v0) (knows$ spy$ (cons$ (gets$ ?v1 ?v2) ?v0)))) :named a148)) -(assert (! (forall ((?v0 Event$)) (! (= (insert$a ?v0 nil$) (cons$ ?v0 nil$)) :pattern ((insert$a ?v0)))) :named a149)) -(assert (! (forall ((?v0 Agent$) (?v1 Msg$) (?v2 Event_list$)) (! (= (knows$ spy$ (cons$ (gets$ ?v0 ?v1) ?v2)) (knows$ spy$ ?v2)) :pattern ((cons$ (gets$ ?v0 ?v1) ?v2)))) :named a150)) -(assert (! (forall ((?v0 Event_list$) (?v1 Agent$) (?v2 Msg$)) (less_eq$ (knows$ spy$ ?v0) (knows$ spy$ (cons$ (notes$ ?v1 ?v2) ?v0)))) :named a151)) -(assert (! (forall ((?v0 (-> Event$ Bool)) (?v1 Event$) (?v2 Event_list$)) (= (list_ex1$ ?v0 (cons$ ?v1 ?v2)) (ite (?v0 ?v1) (list_all$ (uui$ ?v0 ?v1) ?v2) (list_ex1$ ?v0 ?v2)))) :named a152)) -(assert (! (forall ((?v0 Agent$) (?v1 Msg$) (?v2 Agent$) (?v3 Msg$)) (= (= (notes$ ?v0 ?v1) (notes$ ?v2 ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3)))) :named a153)) -(assert (! (forall ((?v0 Agent$) (?v1 Msg$) (?v2 Agent$) (?v3 Msg$)) (= (= (gets$ ?v0 ?v1) (gets$ ?v2 ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3)))) :named a154)) -(assert (! (forall ((?v0 (-> Event$ Bool)) (?v1 Event$) (?v2 Event_list$)) (! (= (list_all$ ?v0 (cons$ ?v1 ?v2)) (and (?v0 ?v1) (list_all$ ?v0 ?v2))) :pattern ((list_all$ ?v0 (cons$ ?v1 ?v2))))) :named a155)) -(assert (! (forall ((?v0 (-> Event$ Bool)) (?v1 Event$) (?v2 Event_list$)) (! (= (list_all$ ?v0 (cons$ ?v1 ?v2)) (and (?v0 ?v1) (list_all$ ?v0 ?v2))) :pattern ((list_all$ ?v0 (cons$ ?v1 ?v2))))) :named a156)) -(assert (! (forall ((?v0 (-> Event$ Bool))) (! (= (list_all$ ?v0 nil$) true) :pattern ((list_all$ ?v0)))) :named a157)) -(assert (! (forall ((?v0 Agent$) (?v1 Msg$) (?v2 Agent$) (?v3 Msg$)) (not (= (gets$ ?v0 ?v1) (notes$ ?v2 ?v3)))) :named a158)) -(assert (! (forall ((?v0 (-> Event$ Bool))) (list_all$ ?v0 nil$)) :named a159)) -(assert (! (forall ((?v0 Agent$) (?v1 Event_list$) (?v2 Agent$) (?v3 Msg$)) (less_eq$ (knows$ ?v0 ?v1) (knows$ ?v0 (cons$ (notes$ ?v2 ?v3) ?v1)))) :named a160)) -(assert (! (forall ((?v0 Agent$) (?v1 Event_list$) (?v2 Agent$) (?v3 Msg$)) (less_eq$ (knows$ ?v0 ?v1) (knows$ ?v0 (cons$ (gets$ ?v2 ?v3) ?v1)))) :named a161)) -(assert (! (= (product_lists$ nil$a) (cons$a nil$ nil$a)) :named a162)) -(assert (! (forall ((?v0 Event_list$) (?v1 Agent$) (?v2 Msg$)) (= (knows$ spy$ (append$ ?v0 (cons$ (gets$ ?v1 ?v2) nil$))) (knows$ spy$ ?v0))) :named a163)) -(assert (! (= (subseqs$ nil$) (cons$a nil$ nil$a)) :named a164)) -(assert (! (forall ((?v0 Event_list$) (?v1 Agent$) (?v2 Agent$) (?v3 Msg$)) (less_eq$ (knows$ spy$ ?v0) (knows$ spy$ (cons$ (says$ ?v1 ?v2 ?v3) ?v0)))) :named a165)) -(assert (! (forall ((?v0 Event_list$) (?v1 Event_list$) (?v2 Event_list$)) (= (append$ (append$ ?v0 ?v1) ?v2) (append$ ?v0 (append$ ?v1 ?v2)))) :named a166)) -(assert (! (forall ((?v0 Event_list$) (?v1 Event_list$) (?v2 Event_list$)) (= (append$ (append$ ?v0 ?v1) ?v2) (append$ ?v0 (append$ ?v1 ?v2)))) :named a167)) -(assert (! (forall ((?v0 Event_list$) (?v1 Event_list$) (?v2 Event_list$)) (= (= (append$ ?v0 ?v1) (append$ ?v2 ?v1)) (= ?v0 ?v2))) :named a168)) -(assert (! (forall ((?v0 Event_list$) (?v1 Event_list$) (?v2 Event_list$)) (= (= (append$ ?v0 ?v1) (append$ ?v0 ?v2)) (= ?v1 ?v2))) :named a169)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent$) (?v2 Msg$) (?v3 Agent$) (?v4 Agent$) (?v5 Msg$)) (= (= (says$ ?v0 ?v1 ?v2) (says$ ?v3 ?v4 ?v5)) (and (= ?v0 ?v3) (and (= ?v1 ?v4) (= ?v2 ?v5))))) :named a170)) -(assert (! (forall ((?v0 Event_list$)) (! (= (append$ ?v0 nil$) ?v0) :pattern ((append$ ?v0)))) :named a171)) -(assert (! (forall ((?v0 Event_list$) (?v1 Event_list$)) (= (= (append$ ?v0 ?v1) ?v0) (= ?v1 nil$))) :named a172)) -(assert (! (forall ((?v0 Event_list$) (?v1 Event_list$)) (= (= ?v0 (append$ ?v0 ?v1)) (= ?v1 nil$))) :named a173)) -(assert (! (forall ((?v0 Event_list$) (?v1 Event_list$)) (= (= (append$ ?v0 ?v1) ?v1) (= ?v0 nil$))) :named a174)) -(assert (! (forall ((?v0 Event_list$) (?v1 Event_list$)) (= (= ?v0 (append$ ?v1 ?v0)) (= ?v1 nil$))) :named a175)) -(assert (! (forall ((?v0 Event_list$) (?v1 Event_list$)) (= (= nil$ (append$ ?v0 ?v1)) (and (= ?v0 nil$) (= ?v1 nil$)))) :named a176)) -(assert (! (forall ((?v0 Event_list$) (?v1 Event_list$)) (= (= (append$ ?v0 ?v1) nil$) (and (= ?v0 nil$) (= ?v1 nil$)))) :named a177)) -(assert (! (forall ((?v0 Event_list$)) (! (= (append$ ?v0 nil$) ?v0) :pattern ((append$ ?v0)))) :named a178)) -(assert (! (forall ((?v0 (-> Event$ Bool)) (?v1 Event_list$) (?v2 Event_list$)) (= (list_all$ ?v0 (append$ ?v1 ?v2)) (and (list_all$ ?v0 ?v1) (list_all$ ?v0 ?v2)))) :named a179)) -(assert (! (forall ((?v0 (-> Event$ Bool)) (?v1 Event_list$) (?v2 Event_list$)) (= (list_ex$ ?v0 (append$ ?v1 ?v2)) (or (list_ex$ ?v0 ?v1) (list_ex$ ?v0 ?v2)))) :named a180)) -(assert (! (forall ((?v0 Event_list$) (?v1 Event$) (?v2 Event_list$) (?v3 Event$)) (= (= (append$ ?v0 (cons$ ?v1 nil$)) (append$ ?v2 (cons$ ?v3 nil$))) (and (= ?v0 ?v2) (= ?v1 ?v3)))) :named a181)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$) (?v2 (-> Event$ Event_list$))) (! (= (bind$ (cons$ ?v0 ?v1) ?v2) (append$ (?v2 ?v0) (bind$ ?v1 ?v2))) :pattern ((bind$ (cons$ ?v0 ?v1) ?v2)))) :named a182)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$) (?v2 Event_list$)) (! (= (append$ (cons$ ?v0 ?v1) ?v2) (cons$ ?v0 (append$ ?v1 ?v2))) :pattern ((append$ (cons$ ?v0 ?v1) ?v2)))) :named a183)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$) (?v2 Event_list$) (?v3 Event_list$) (?v4 Event_list$)) (=> (and (= (cons$ ?v0 ?v1) ?v2) (= ?v3 (append$ ?v1 ?v4))) (= (cons$ ?v0 ?v3) (append$ ?v2 ?v4)))) :named a184)) -(assert (! (forall ((?v0 Event_list$)) (! (= (append$ nil$ ?v0) ?v0) :pattern ((append$ nil$ ?v0)))) :named a185)) -(assert (! (forall ((?v0 Event_list$)) (! (= (append$ nil$ ?v0) ?v0) :pattern ((append$ nil$ ?v0)))) :named a186)) -(assert (! (forall ((?v0 Event_list$) (?v1 Event_list$)) (=> (= ?v0 ?v1) (= ?v0 (append$ nil$ ?v1)))) :named a187)) -(assert (! (forall ((?v0 Event_list$) (?v1 Event_list$) (?v2 Event_list$) (?v3 Event_list$) (?v4 Event_list$)) (=> (and (= (append$ ?v0 ?v1) ?v2) (= ?v3 (append$ ?v1 ?v4))) (= (append$ ?v0 ?v3) (append$ ?v2 ?v4)))) :named a188)) -(assert (! (forall ((?v0 Event_list$) (?v1 Event_list$) (?v2 Event_list$) (?v3 Event_list$)) (= (= (append$ ?v0 ?v1) (append$ ?v2 ?v3)) (exists ((?v4 Event_list$)) (or (and (= ?v0 (append$ ?v2 ?v4)) (= (append$ ?v4 ?v1) ?v3)) (and (= (append$ ?v0 ?v4) ?v2) (= ?v1 (append$ ?v4 ?v3))))))) :named a189)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent$) (?v2 Msg$) (?v3 Agent$) (?v4 Msg$)) (not (= (says$ ?v0 ?v1 ?v2) (notes$ ?v3 ?v4)))) :named a190)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent$) (?v2 Msg$) (?v3 Agent$) (?v4 Msg$)) (not (= (says$ ?v0 ?v1 ?v2) (gets$ ?v3 ?v4)))) :named a191)) -(assert (! (forall ((?v0 (-> Event_list$ Bool)) (?v1 Event_list$)) (=> (and (?v0 nil$) (forall ((?v2 Event$) (?v3 Event_list$)) (=> (?v0 ?v3) (?v0 (append$ ?v3 (cons$ ?v2 nil$)))))) (?v0 ?v1))) :named a192)) -(assert (! (forall ((?v0 Event_list$)) (=> (and (=> (= ?v0 nil$) false) (forall ((?v1 Event_list$) (?v2 Event$)) (=> (= ?v0 (append$ ?v1 (cons$ ?v2 nil$))) false))) false)) :named a193)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$) (?v2 Event_list$) (?v3 Event_list$)) (= (= (cons$ ?v0 ?v1) (append$ ?v2 ?v3)) (or (and (= ?v2 nil$) (= (cons$ ?v0 ?v1) ?v3)) (exists ((?v4 Event_list$)) (and (= (cons$ ?v0 ?v4) ?v2) (= ?v1 (append$ ?v4 ?v3))))))) :named a194)) -(assert (! (forall ((?v0 Event_list$) (?v1 Event_list$) (?v2 Event$) (?v3 Event_list$)) (= (= (append$ ?v0 ?v1) (cons$ ?v2 ?v3)) (or (and (= ?v0 nil$) (= ?v1 (cons$ ?v2 ?v3))) (exists ((?v4 Event_list$)) (and (= ?v0 (cons$ ?v2 ?v4)) (= (append$ ?v4 ?v1) ?v3)))))) :named a195)) -(assert (! (forall ((?v0 Event_list$) (?v1 (-> Event_list$ Bool))) (=> (and (not (= ?v0 nil$)) (and (forall ((?v2 Event$)) (?v1 (cons$ ?v2 nil$))) (forall ((?v2 Event$) (?v3 Event_list$)) (=> (and (not (= ?v3 nil$)) (?v1 ?v3)) (?v1 (append$ ?v3 (cons$ ?v2 nil$))))))) (?v1 ?v0))) :named a196)) -(assert (! (forall ((?v0 (-> Event$ Bool)) (?v1 Event$) (?v2 Event_list$) (?v3 Event_list$)) (=> (not (?v0 ?v1)) (= (takeWhile$ ?v0 (append$ ?v2 (cons$ ?v1 ?v3))) (takeWhile$ ?v0 ?v2)))) :named a197)) -(assert (! (forall ((?v0 Event$)) (=> (and (forall ((?v1 Agent$) (?v2 Agent$) (?v3 Msg$)) (=> (= ?v0 (says$ ?v1 ?v2 ?v3)) false)) (and (forall ((?v1 Agent$) (?v2 Msg$)) (=> (= ?v0 (gets$ ?v1 ?v2)) false)) (forall ((?v1 Agent$) (?v2 Msg$)) (=> (= ?v0 (notes$ ?v1 ?v2)) false)))) false)) :named a198)) -(assert (! (forall ((?v0 (-> Event$ Event_list$)) (?v1 Event$) (?v2 Event_list$)) (! (= (maps$ ?v0 (cons$ ?v1 ?v2)) (append$ (?v0 ?v1) (maps$ ?v0 ?v2))) :pattern ((maps$ ?v0 (cons$ ?v1 ?v2))))) :named a199)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$)) (= (rotate1$ (cons$ ?v0 ?v1)) (append$ ?v1 (cons$ ?v0 nil$)))) :named a200)) -(assert (! (forall ((?v0 Agent$) (?v1 Event_list$) (?v2 Agent$) (?v3 Agent$) (?v4 Msg$)) (less_eq$ (knows$ ?v0 ?v1) (knows$ ?v0 (cons$ (says$ ?v2 ?v3 ?v4) ?v1)))) :named a201)) -(assert (! (forall ((?v0 Event_list_set$) (?v1 Event_list$)) (= (succ$ ?v0 ?v1) (collect$a (uuj$ ?v0 ?v1)))) :named a202)) -(assert (! (forall ((?v0 Event_list$) (?v1 Agent$) (?v2 Agent$) (?v3 Msg$)) (= (knows$ spy$ (append$ ?v0 (cons$ (says$ ?v1 ?v2 ?v3) nil$))) (insert$ ?v3 (knows$ spy$ ?v0)))) :named a203)) -(assert (! (forall ((?v0 Msg$) (?v1 Agent$) (?v2 Event_list$)) (=> (and (member$a ?v0 (knows$ ?v1 ?v2)) (not (= ?v1 spy$))) (exists ((?v3 Agent$)) (or (member$b (says$ ?v1 ?v3 ?v0) (set$ ?v2)) (or (member$b (gets$ ?v1 ?v0) (set$ ?v2)) (or (member$b (notes$ ?v1 ?v0) (set$ ?v2)) (member$a ?v0 (initState$ ?v1)))))))) :named a204)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_list_set$) (?v2 Msg_list$)) (=> (member$a ?v0 (succ$a ?v1 ?v2)) (member$e (append$a ?v2 (cons$b ?v0 nil$b)) ?v1))) :named a205)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_list_set$) (?v2 Agent_list$)) (=> (member$ ?v0 (succ$b ?v1 ?v2)) (member$f (append$b ?v2 (cons$c ?v0 nil$c)) ?v1))) :named a206)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list_set$) (?v2 Event_list$)) (=> (member$b ?v0 (succ$ ?v1 ?v2)) (member$c (append$ ?v2 (cons$ ?v0 nil$)) ?v1))) :named a207)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_set$)) (= (insert$ ?v0 (insert$ ?v0 ?v1)) (insert$ ?v0 ?v1))) :named a208)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg$) (?v2 Msg_set$)) (= (member$a ?v0 (insert$ ?v1 ?v2)) (or (= ?v0 ?v1) (member$a ?v0 ?v2)))) :named a209)) -(assert (! (forall ((?v0 Event$) (?v1 Event$) (?v2 Event_set$)) (= (member$b ?v0 (insert$b ?v1 ?v2)) (or (= ?v0 ?v1) (member$b ?v0 ?v2)))) :named a210)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent$) (?v2 Agent_set$)) (= (member$ ?v0 (insert$c ?v1 ?v2)) (or (= ?v0 ?v1) (member$ ?v0 ?v2)))) :named a211)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_set$) (?v2 Msg$)) (=> (=> (not (member$a ?v0 ?v1)) (= ?v0 ?v2)) (member$a ?v0 (insert$ ?v2 ?v1)))) :named a212)) -(assert (! (forall ((?v0 Event$) (?v1 Event_set$) (?v2 Event$)) (=> (=> (not (member$b ?v0 ?v1)) (= ?v0 ?v2)) (member$b ?v0 (insert$b ?v2 ?v1)))) :named a213)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_set$) (?v2 Agent$)) (=> (=> (not (member$ ?v0 ?v1)) (= ?v0 ?v2)) (member$ ?v0 (insert$c ?v2 ?v1)))) :named a214)) -(assert (! (forall ((?v0 Event$) (?v1 Event_set$) (?v2 Event_set$)) (= (less_eq$a (insert$b ?v0 ?v1) ?v2) (and (member$b ?v0 ?v2) (less_eq$a ?v1 ?v2)))) :named a215)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_set$) (?v2 Agent_set$)) (= (less_eq$b (insert$c ?v0 ?v1) ?v2) (and (member$ ?v0 ?v2) (less_eq$b ?v1 ?v2)))) :named a216)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_set$) (?v2 Msg_set$)) (= (less_eq$ (insert$ ?v0 ?v1) ?v2) (and (member$a ?v0 ?v2) (less_eq$ ?v1 ?v2)))) :named a217)) -(assert (! (forall ((?v0 (-> Msg$ Bool)) (?v1 Msg_list$)) (= (= (takeWhile$a ?v0 ?v1) ?v1) (forall ((?v2 Msg$)) (=> (member$a ?v2 (set$a ?v1)) (?v0 ?v2))))) :named a218)) -(assert (! (forall ((?v0 (-> Agent$ Bool)) (?v1 Agent_list$)) (= (= (takeWhile$b ?v0 ?v1) ?v1) (forall ((?v2 Agent$)) (=> (member$ ?v2 (set$b ?v1)) (?v0 ?v2))))) :named a219)) -(assert (! (forall ((?v0 (-> Event$ Bool)) (?v1 Event_list$)) (= (= (takeWhile$ ?v0 ?v1) ?v1) (forall ((?v2 Event$)) (=> (member$b ?v2 (set$ ?v1)) (?v0 ?v2))))) :named a220)) -(assert (! (forall ((?v0 Event_list$)) (= (set$ (rotate1$ ?v0)) (set$ ?v0))) :named a221)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_list$)) (! (=> (member$a ?v0 (set$a ?v1)) (= (insert$d ?v0 ?v1) ?v1)) :pattern ((insert$d ?v0 ?v1)))) :named a222)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_list$)) (! (=> (member$ ?v0 (set$b ?v1)) (= (insert$e ?v0 ?v1) ?v1)) :pattern ((insert$e ?v0 ?v1)))) :named a223)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$)) (! (=> (member$b ?v0 (set$ ?v1)) (= (insert$a ?v0 ?v1) ?v1)) :pattern ((insert$a ?v0 ?v1)))) :named a224)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_list$)) (! (= (set$a (cons$b ?v0 ?v1)) (insert$ ?v0 (set$a ?v1))) :pattern ((cons$b ?v0 ?v1)))) :named a225)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$)) (! (= (set$ (cons$ ?v0 ?v1)) (insert$b ?v0 (set$ ?v1))) :pattern ((cons$ ?v0 ?v1)))) :named a226)) -(assert (! (forall ((?v0 Msg_list$) (?v1 (-> Msg$ Bool)) (?v2 Msg_list$)) (=> (forall ((?v3 Msg$)) (=> (member$a ?v3 (set$a ?v0)) (?v1 ?v3))) (= (takeWhile$a ?v1 (append$a ?v0 ?v2)) (append$a ?v0 (takeWhile$a ?v1 ?v2))))) :named a227)) -(assert (! (forall ((?v0 Agent_list$) (?v1 (-> Agent$ Bool)) (?v2 Agent_list$)) (=> (forall ((?v3 Agent$)) (=> (member$ ?v3 (set$b ?v0)) (?v1 ?v3))) (= (takeWhile$b ?v1 (append$b ?v0 ?v2)) (append$b ?v0 (takeWhile$b ?v1 ?v2))))) :named a228)) -(assert (! (forall ((?v0 Event_list$) (?v1 (-> Event$ Bool)) (?v2 Event_list$)) (=> (forall ((?v3 Event$)) (=> (member$b ?v3 (set$ ?v0)) (?v1 ?v3))) (= (takeWhile$ ?v1 (append$ ?v0 ?v2)) (append$ ?v0 (takeWhile$ ?v1 ?v2))))) :named a229)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_list$) (?v2 (-> Msg$ Bool)) (?v3 Msg_list$)) (=> (and (member$a ?v0 (set$a ?v1)) (not (?v2 ?v0))) (= (takeWhile$a ?v2 (append$a ?v1 ?v3)) (takeWhile$a ?v2 ?v1)))) :named a230)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_list$) (?v2 (-> Agent$ Bool)) (?v3 Agent_list$)) (=> (and (member$ ?v0 (set$b ?v1)) (not (?v2 ?v0))) (= (takeWhile$b ?v2 (append$b ?v1 ?v3)) (takeWhile$b ?v2 ?v1)))) :named a231)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$) (?v2 (-> Event$ Bool)) (?v3 Event_list$)) (=> (and (member$b ?v0 (set$ ?v1)) (not (?v2 ?v0))) (= (takeWhile$ ?v2 (append$ ?v1 ?v3)) (takeWhile$ ?v2 ?v1)))) :named a232)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_list$)) (= (set$a (insert$d ?v0 ?v1)) (insert$ ?v0 (set$a ?v1)))) :named a233)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$)) (= (set$ (insert$a ?v0 ?v1)) (insert$b ?v0 (set$ ?v1)))) :named a234)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_list$)) (! (=> (not (member$a ?v0 (set$a ?v1))) (= (insert$d ?v0 ?v1) (cons$b ?v0 ?v1))) :pattern ((insert$d ?v0 ?v1)))) :named a235)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_list$)) (! (=> (not (member$ ?v0 (set$b ?v1))) (= (insert$e ?v0 ?v1) (cons$c ?v0 ?v1))) :pattern ((insert$e ?v0 ?v1)))) :named a236)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$)) (! (=> (not (member$b ?v0 (set$ ?v1))) (= (insert$a ?v0 ?v1) (cons$ ?v0 ?v1))) :pattern ((insert$a ?v0 ?v1)))) :named a237)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent$) (?v2 Msg$) (?v3 Event_list$)) (! (= (knows$ spy$ (cons$ (says$ ?v0 ?v1 ?v2) ?v3)) (insert$ ?v2 (knows$ spy$ ?v3))) :pattern ((cons$ (says$ ?v0 ?v1 ?v2) ?v3)))) :named a238)) -(assert (! (forall ((?v0 Agent_list$) (?v1 Agent_set$)) (= (less_eq$b (set$b ?v0) ?v1) (forall ((?v2 Agent$)) (=> (member$ ?v2 (set$b ?v0)) (member$ ?v2 ?v1))))) :named a239)) -(assert (! (forall ((?v0 Event_list$) (?v1 Event_set$)) (= (less_eq$a (set$ ?v0) ?v1) (forall ((?v2 Event$)) (=> (member$b ?v2 (set$ ?v0)) (member$b ?v2 ?v1))))) :named a240)) -(assert (! (forall ((?v0 Msg_list$) (?v1 Msg_set$)) (= (less_eq$ (set$a ?v0) ?v1) (forall ((?v2 Msg$)) (=> (member$a ?v2 (set$a ?v0)) (member$a ?v2 ?v1))))) :named a241)) -(assert (! (forall ((?v0 Event$) (?v1 Event_set$) (?v2 Event_set$)) (=> (and (member$b ?v0 ?v1) (less_eq$a ?v2 ?v1)) (less_eq$a (insert$b ?v0 ?v2) ?v1))) :named a242)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_set$) (?v2 Agent_set$)) (=> (and (member$ ?v0 ?v1) (less_eq$b ?v2 ?v1)) (less_eq$b (insert$c ?v0 ?v2) ?v1))) :named a243)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_set$) (?v2 Msg_set$)) (=> (and (member$a ?v0 ?v1) (less_eq$ ?v2 ?v1)) (less_eq$ (insert$ ?v0 ?v2) ?v1))) :named a244)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$) (?v2 Msg$)) (=> (less_eq$ ?v0 ?v1) (less_eq$ ?v0 (insert$ ?v2 ?v1)))) :named a245)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg$)) (less_eq$ ?v0 (insert$ ?v1 ?v0))) :named a246)) -(assert (! (forall ((?v0 Event$) (?v1 Event_set$) (?v2 Event_set$)) (=> (not (member$b ?v0 ?v1)) (= (less_eq$a ?v1 (insert$b ?v0 ?v2)) (less_eq$a ?v1 ?v2)))) :named a247)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_set$) (?v2 Agent_set$)) (=> (not (member$ ?v0 ?v1)) (= (less_eq$b ?v1 (insert$c ?v0 ?v2)) (less_eq$b ?v1 ?v2)))) :named a248)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_set$) (?v2 Msg_set$)) (=> (not (member$a ?v0 ?v1)) (= (less_eq$ ?v1 (insert$ ?v0 ?v2)) (less_eq$ ?v1 ?v2)))) :named a249)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$) (?v2 Msg$)) (=> (less_eq$ ?v0 ?v1) (less_eq$ (insert$ ?v2 ?v0) (insert$ ?v2 ?v1)))) :named a250)) -(assert (! (forall ((?v0 Msg_list$) (?v1 Msg_list$) (?v2 (-> Msg$ Bool)) (?v3 (-> Msg$ Bool))) (=> (and (= ?v0 ?v1) (forall ((?v4 Msg$)) (=> (member$a ?v4 (set$a ?v1)) (= (?v2 ?v4) (?v3 ?v4))))) (= (list_ex$a ?v2 ?v0) (list_ex$a ?v3 ?v1)))) :named a251)) -(assert (! (forall ((?v0 Agent_list$) (?v1 Agent_list$) (?v2 (-> Agent$ Bool)) (?v3 (-> Agent$ Bool))) (=> (and (= ?v0 ?v1) (forall ((?v4 Agent$)) (=> (member$ ?v4 (set$b ?v1)) (= (?v2 ?v4) (?v3 ?v4))))) (= (list_ex$b ?v2 ?v0) (list_ex$b ?v3 ?v1)))) :named a252)) -(assert (! (forall ((?v0 Event_list$) (?v1 Event_list$) (?v2 (-> Event$ Bool)) (?v3 (-> Event$ Bool))) (=> (and (= ?v0 ?v1) (forall ((?v4 Event$)) (=> (member$b ?v4 (set$ ?v1)) (= (?v2 ?v4) (?v3 ?v4))))) (= (list_ex$ ?v2 ?v0) (list_ex$ ?v3 ?v1)))) :named a253)) -(assert (! (forall ((?v0 Msg$) (?v1 (-> Msg$ Bool))) (= (insert$ ?v0 (collect$ ?v1)) (collect$ (uuk$ ?v0 ?v1)))) :named a254)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_set$)) (= (insert$ ?v0 ?v1) (collect$ (uul$ ?v0 ?v1)))) :named a255)) -(assert (! (forall ((?v0 Event$) (?v1 Event_set$)) (= (insert$b ?v0 ?v1) (collect$a (uum$ ?v0 ?v1)))) :named a256)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_set$)) (= (insert$c ?v0 ?v1) (collect$b (uun$ ?v0 ?v1)))) :named a257)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_set$)) (=> (member$a ?v0 ?v1) (exists ((?v2 Msg_set$)) (and (= ?v1 (insert$ ?v0 ?v2)) (not (member$a ?v0 ?v2)))))) :named a258)) -(assert (! (forall ((?v0 Event$) (?v1 Event_set$)) (=> (member$b ?v0 ?v1) (exists ((?v2 Event_set$)) (and (= ?v1 (insert$b ?v0 ?v2)) (not (member$b ?v0 ?v2)))))) :named a259)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_set$)) (=> (member$ ?v0 ?v1) (exists ((?v2 Agent_set$)) (and (= ?v1 (insert$c ?v0 ?v2)) (not (member$ ?v0 ?v2)))))) :named a260)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg$) (?v2 Msg_set$)) (= (insert$ ?v0 (insert$ ?v1 ?v2)) (insert$ ?v1 (insert$ ?v0 ?v2)))) :named a261)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_set$) (?v2 Msg$) (?v3 Msg_set$)) (=> (and (not (member$a ?v0 ?v1)) (not (member$a ?v2 ?v3))) (= (= (insert$ ?v0 ?v1) (insert$ ?v2 ?v3)) (ite (= ?v0 ?v2) (= ?v1 ?v3) (exists ((?v4 Msg_set$)) (and (= ?v1 (insert$ ?v2 ?v4)) (and (not (member$a ?v2 ?v4)) (and (= ?v3 (insert$ ?v0 ?v4)) (not (member$a ?v0 ?v4)))))))))) :named a262)) -(assert (! (forall ((?v0 Event$) (?v1 Event_set$) (?v2 Event$) (?v3 Event_set$)) (=> (and (not (member$b ?v0 ?v1)) (not (member$b ?v2 ?v3))) (= (= (insert$b ?v0 ?v1) (insert$b ?v2 ?v3)) (ite (= ?v0 ?v2) (= ?v1 ?v3) (exists ((?v4 Event_set$)) (and (= ?v1 (insert$b ?v2 ?v4)) (and (not (member$b ?v2 ?v4)) (and (= ?v3 (insert$b ?v0 ?v4)) (not (member$b ?v0 ?v4)))))))))) :named a263)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_set$) (?v2 Agent$) (?v3 Agent_set$)) (=> (and (not (member$ ?v0 ?v1)) (not (member$ ?v2 ?v3))) (= (= (insert$c ?v0 ?v1) (insert$c ?v2 ?v3)) (ite (= ?v0 ?v2) (= ?v1 ?v3) (exists ((?v4 Agent_set$)) (and (= ?v1 (insert$c ?v2 ?v4)) (and (not (member$ ?v2 ?v4)) (and (= ?v3 (insert$c ?v0 ?v4)) (not (member$ ?v0 ?v4)))))))))) :named a264)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_set$)) (! (=> (member$a ?v0 ?v1) (= (insert$ ?v0 ?v1) ?v1)) :pattern ((insert$ ?v0 ?v1)))) :named a265)) -(assert (! (forall ((?v0 Event$) (?v1 Event_set$)) (! (=> (member$b ?v0 ?v1) (= (insert$b ?v0 ?v1) ?v1)) :pattern ((insert$b ?v0 ?v1)))) :named a266)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_set$)) (! (=> (member$ ?v0 ?v1) (= (insert$c ?v0 ?v1) ?v1)) :pattern ((insert$c ?v0 ?v1)))) :named a267)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_set$) (?v2 Msg_set$)) (=> (and (not (member$a ?v0 ?v1)) (not (member$a ?v0 ?v2))) (= (= (insert$ ?v0 ?v1) (insert$ ?v0 ?v2)) (= ?v1 ?v2)))) :named a268)) -(assert (! (forall ((?v0 Event$) (?v1 Event_set$) (?v2 Event_set$)) (=> (and (not (member$b ?v0 ?v1)) (not (member$b ?v0 ?v2))) (= (= (insert$b ?v0 ?v1) (insert$b ?v0 ?v2)) (= ?v1 ?v2)))) :named a269)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_set$) (?v2 Agent_set$)) (=> (and (not (member$ ?v0 ?v1)) (not (member$ ?v0 ?v2))) (= (= (insert$c ?v0 ?v1) (insert$c ?v0 ?v2)) (= ?v1 ?v2)))) :named a270)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_set$)) (=> (and (member$a ?v0 ?v1) (forall ((?v2 Msg_set$)) (=> (and (= ?v1 (insert$ ?v0 ?v2)) (not (member$a ?v0 ?v2))) false))) false)) :named a271)) -(assert (! (forall ((?v0 Event$) (?v1 Event_set$)) (=> (and (member$b ?v0 ?v1) (forall ((?v2 Event_set$)) (=> (and (= ?v1 (insert$b ?v0 ?v2)) (not (member$b ?v0 ?v2))) false))) false)) :named a272)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_set$)) (=> (and (member$ ?v0 ?v1) (forall ((?v2 Agent_set$)) (=> (and (= ?v1 (insert$c ?v0 ?v2)) (not (member$ ?v0 ?v2))) false))) false)) :named a273)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_set$) (?v2 Msg$)) (=> (member$a ?v0 ?v1) (member$a ?v0 (insert$ ?v2 ?v1)))) :named a274)) -(assert (! (forall ((?v0 Event$) (?v1 Event_set$) (?v2 Event$)) (=> (member$b ?v0 ?v1) (member$b ?v0 (insert$b ?v2 ?v1)))) :named a275)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_set$) (?v2 Agent$)) (=> (member$ ?v0 ?v1) (member$ ?v0 (insert$c ?v2 ?v1)))) :named a276)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_set$)) (member$a ?v0 (insert$ ?v0 ?v1))) :named a277)) -(assert (! (forall ((?v0 Event$) (?v1 Event_set$)) (member$b ?v0 (insert$b ?v0 ?v1))) :named a278)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_set$)) (member$ ?v0 (insert$c ?v0 ?v1))) :named a279)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg$) (?v2 Msg_set$)) (=> (and (member$a ?v0 (insert$ ?v1 ?v2)) (and (=> (= ?v0 ?v1) false) (=> (member$a ?v0 ?v2) false))) false)) :named a280)) -(assert (! (forall ((?v0 Event$) (?v1 Event$) (?v2 Event_set$)) (=> (and (member$b ?v0 (insert$b ?v1 ?v2)) (and (=> (= ?v0 ?v1) false) (=> (member$b ?v0 ?v2) false))) false)) :named a281)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent$) (?v2 Agent_set$)) (=> (and (member$ ?v0 (insert$c ?v1 ?v2)) (and (=> (= ?v0 ?v1) false) (=> (member$ ?v0 ?v2) false))) false)) :named a282)) -(assert (! (forall ((?v0 Msg$) (?v1 (-> Msg$ Bool)) (?v2 Msg_list$)) (=> (member$a ?v0 (set$a (takeWhile$a ?v1 ?v2))) (and (member$a ?v0 (set$a ?v2)) (?v1 ?v0)))) :named a283)) -(assert (! (forall ((?v0 Agent$) (?v1 (-> Agent$ Bool)) (?v2 Agent_list$)) (=> (member$ ?v0 (set$b (takeWhile$b ?v1 ?v2))) (and (member$ ?v0 (set$b ?v2)) (?v1 ?v0)))) :named a284)) -(assert (! (forall ((?v0 Event$) (?v1 (-> Event$ Bool)) (?v2 Event_list$)) (=> (member$b ?v0 (set$ (takeWhile$ ?v1 ?v2))) (and (member$b ?v0 (set$ ?v2)) (?v1 ?v0)))) :named a285)) -(assert (! (forall ((?v0 Msg_list$) (?v1 Msg_list$) (?v2 (-> Msg$ Bool)) (?v3 (-> Msg$ Bool))) (=> (and (= ?v0 ?v1) (forall ((?v4 Msg$)) (=> (member$a ?v4 (set$a ?v0)) (= (?v2 ?v4) (?v3 ?v4))))) (= (takeWhile$a ?v2 ?v0) (takeWhile$a ?v3 ?v1)))) :named a286)) -(assert (! (forall ((?v0 Agent_list$) (?v1 Agent_list$) (?v2 (-> Agent$ Bool)) (?v3 (-> Agent$ Bool))) (=> (and (= ?v0 ?v1) (forall ((?v4 Agent$)) (=> (member$ ?v4 (set$b ?v0)) (= (?v2 ?v4) (?v3 ?v4))))) (= (takeWhile$b ?v2 ?v0) (takeWhile$b ?v3 ?v1)))) :named a287)) -(assert (! (forall ((?v0 Event_list$) (?v1 Event_list$) (?v2 (-> Event$ Bool)) (?v3 (-> Event$ Bool))) (=> (and (= ?v0 ?v1) (forall ((?v4 Event$)) (=> (member$b ?v4 (set$ ?v0)) (= (?v2 ?v4) (?v3 ?v4))))) (= (takeWhile$ ?v2 ?v0) (takeWhile$ ?v3 ?v1)))) :named a288)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_list$) (?v2 Msg$)) (=> (member$a ?v0 (set$a ?v1)) (member$a ?v0 (set$a (cons$b ?v2 ?v1))))) :named a289)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_list$) (?v2 Agent$)) (=> (member$ ?v0 (set$b ?v1)) (member$ ?v0 (set$b (cons$c ?v2 ?v1))))) :named a290)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$) (?v2 Event$)) (=> (member$b ?v0 (set$ ?v1)) (member$b ?v0 (set$ (cons$ ?v2 ?v1))))) :named a291)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_list$)) (member$a ?v0 (set$a (cons$b ?v0 ?v1)))) :named a292)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_list$)) (member$ ?v0 (set$b (cons$c ?v0 ?v1)))) :named a293)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$)) (member$b ?v0 (set$ (cons$ ?v0 ?v1)))) :named a294)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg$) (?v2 Msg_list$)) (=> (member$a ?v0 (set$a (cons$b ?v1 ?v2))) (or (= ?v0 ?v1) (member$a ?v0 (set$a ?v2))))) :named a295)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent$) (?v2 Agent_list$)) (=> (member$ ?v0 (set$b (cons$c ?v1 ?v2))) (or (= ?v0 ?v1) (member$ ?v0 (set$b ?v2))))) :named a296)) -(assert (! (forall ((?v0 Event$) (?v1 Event$) (?v2 Event_list$)) (=> (member$b ?v0 (set$ (cons$ ?v1 ?v2))) (or (= ?v0 ?v1) (member$b ?v0 (set$ ?v2))))) :named a297)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_list$)) (=> (and (member$a ?v0 (set$a ?v1)) (and (forall ((?v2 Msg_list$)) (=> (= ?v1 (cons$b ?v0 ?v2)) false)) (forall ((?v2 Msg$) (?v3 Msg_list$)) (=> (and (= ?v1 (cons$b ?v2 ?v3)) (member$a ?v0 (set$a ?v3))) false)))) false)) :named a298)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_list$)) (=> (and (member$ ?v0 (set$b ?v1)) (and (forall ((?v2 Agent_list$)) (=> (= ?v1 (cons$c ?v0 ?v2)) false)) (forall ((?v2 Agent$) (?v3 Agent_list$)) (=> (and (= ?v1 (cons$c ?v2 ?v3)) (member$ ?v0 (set$b ?v3))) false)))) false)) :named a299)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$)) (=> (and (member$b ?v0 (set$ ?v1)) (and (forall ((?v2 Event_list$)) (=> (= ?v1 (cons$ ?v0 ?v2)) false)) (forall ((?v2 Event$) (?v3 Event_list$)) (=> (and (= ?v1 (cons$ ?v2 ?v3)) (member$b ?v0 (set$ ?v3))) false)))) false)) :named a300)) -(assert (! (forall ((?v0 Msg_list$) (?v1 Msg_list$) (?v2 (-> Msg$ Bool)) (?v3 (-> Msg$ Bool))) (=> (and (= ?v0 ?v1) (forall ((?v4 Msg$)) (=> (member$a ?v4 (set$a ?v1)) (= (?v2 ?v4) (?v3 ?v4))))) (= (list_all$a ?v2 ?v0) (list_all$a ?v3 ?v1)))) :named a301)) -(assert (! (forall ((?v0 Agent_list$) (?v1 Agent_list$) (?v2 (-> Agent$ Bool)) (?v3 (-> Agent$ Bool))) (=> (and (= ?v0 ?v1) (forall ((?v4 Agent$)) (=> (member$ ?v4 (set$b ?v1)) (= (?v2 ?v4) (?v3 ?v4))))) (= (list_all$b ?v2 ?v0) (list_all$b ?v3 ?v1)))) :named a302)) -(assert (! (forall ((?v0 Event_list$) (?v1 Event_list$) (?v2 (-> Event$ Bool)) (?v3 (-> Event$ Bool))) (=> (and (= ?v0 ?v1) (forall ((?v4 Event$)) (=> (member$b ?v4 (set$ ?v1)) (= (?v2 ?v4) (?v3 ?v4))))) (= (list_all$ ?v2 ?v0) (list_all$ ?v3 ?v1)))) :named a303)) -(assert (! (forall ((?v0 (-> Msg$ Bool)) (?v1 Msg_list$) (?v2 (-> Msg$ Bool))) (=> (and (list_all$a ?v0 ?v1) (forall ((?v3 Msg$)) (=> (and (member$a ?v3 (set$a ?v1)) (?v0 ?v3)) (?v2 ?v3)))) (list_all$a ?v2 ?v1))) :named a304)) -(assert (! (forall ((?v0 (-> Agent$ Bool)) (?v1 Agent_list$) (?v2 (-> Agent$ Bool))) (=> (and (list_all$b ?v0 ?v1) (forall ((?v3 Agent$)) (=> (and (member$ ?v3 (set$b ?v1)) (?v0 ?v3)) (?v2 ?v3)))) (list_all$b ?v2 ?v1))) :named a305)) -(assert (! (forall ((?v0 (-> Event$ Bool)) (?v1 Event_list$) (?v2 (-> Event$ Bool))) (=> (and (list_all$ ?v0 ?v1) (forall ((?v3 Event$)) (=> (and (member$b ?v3 (set$ ?v1)) (?v0 ?v3)) (?v2 ?v3)))) (list_all$ ?v2 ?v1))) :named a306)) -(assert (! (forall ((?v0 (-> Msg$ Bool)) (?v1 Msg_list$)) (= (list_ex1$a ?v0 ?v1) (exists ((?v2 Msg$)) (and (and (member$a ?v2 (set$a ?v1)) (?v0 ?v2)) (forall ((?v3 Msg$)) (=> (and (member$a ?v3 (set$a ?v1)) (?v0 ?v3)) (= ?v3 ?v2))))))) :named a307)) -(assert (! (forall ((?v0 (-> Agent$ Bool)) (?v1 Agent_list$)) (= (list_ex1$b ?v0 ?v1) (exists ((?v2 Agent$)) (and (and (member$ ?v2 (set$b ?v1)) (?v0 ?v2)) (forall ((?v3 Agent$)) (=> (and (member$ ?v3 (set$b ?v1)) (?v0 ?v3)) (= ?v3 ?v2))))))) :named a308)) -(assert (! (forall ((?v0 (-> Event$ Bool)) (?v1 Event_list$)) (= (list_ex1$ ?v0 ?v1) (exists ((?v2 Event$)) (and (and (member$b ?v2 (set$ ?v1)) (?v0 ?v2)) (forall ((?v3 Event$)) (=> (and (member$b ?v3 (set$ ?v1)) (?v0 ?v3)) (= ?v3 ?v2))))))) :named a309)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_list$)) (= (member$a ?v0 (set$a ?v1)) (member$g ?v1 ?v0))) :named a310)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_list$)) (= (member$ ?v0 (set$b ?v1)) (member$h ?v1 ?v0))) :named a311)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$)) (= (member$b ?v0 (set$ ?v1)) (member$d ?v1 ?v0))) :named a312)) -(assert (! (forall ((?v0 Event_list$) (?v1 Event$)) (less_eq$a (set$ ?v0) (set$ (cons$ ?v1 ?v0)))) :named a313)) -(assert (! (forall ((?v0 Msg_list$) (?v1 Msg$)) (less_eq$ (set$a ?v0) (set$a (cons$b ?v1 ?v0)))) :named a314)) -(assert (! (forall ((?v0 Msg_list$) (?v1 (-> Msg$ Bool))) (= (exists ((?v2 Msg$)) (and (member$a ?v2 (set$a ?v0)) (?v1 ?v2))) (exists ((?v2 Msg_list$) (?v3 Msg$) (?v4 Msg_list$)) (and (= ?v0 (append$a ?v2 (cons$b ?v3 ?v4))) (and (?v1 ?v3) (forall ((?v5 Msg$)) (=> (member$a ?v5 (set$a ?v2)) (not (?v1 ?v5))))))))) :named a315)) -(assert (! (forall ((?v0 Agent_list$) (?v1 (-> Agent$ Bool))) (= (exists ((?v2 Agent$)) (and (member$ ?v2 (set$b ?v0)) (?v1 ?v2))) (exists ((?v2 Agent_list$) (?v3 Agent$) (?v4 Agent_list$)) (and (= ?v0 (append$b ?v2 (cons$c ?v3 ?v4))) (and (?v1 ?v3) (forall ((?v5 Agent$)) (=> (member$ ?v5 (set$b ?v2)) (not (?v1 ?v5))))))))) :named a316)) -(assert (! (forall ((?v0 Event_list$) (?v1 (-> Event$ Bool))) (= (exists ((?v2 Event$)) (and (member$b ?v2 (set$ ?v0)) (?v1 ?v2))) (exists ((?v2 Event_list$) (?v3 Event$) (?v4 Event_list$)) (and (= ?v0 (append$ ?v2 (cons$ ?v3 ?v4))) (and (?v1 ?v3) (forall ((?v5 Event$)) (=> (member$b ?v5 (set$ ?v2)) (not (?v1 ?v5))))))))) :named a317)) -(assert (! (forall ((?v0 Msg_list$) (?v1 (-> Msg$ Bool))) (= (exists ((?v2 Msg$)) (and (member$a ?v2 (set$a ?v0)) (?v1 ?v2))) (exists ((?v2 Msg_list$) (?v3 Msg$) (?v4 Msg_list$)) (and (= ?v0 (append$a ?v2 (cons$b ?v3 ?v4))) (and (?v1 ?v3) (forall ((?v5 Msg$)) (=> (member$a ?v5 (set$a ?v4)) (not (?v1 ?v5))))))))) :named a318)) -(assert (! (forall ((?v0 Agent_list$) (?v1 (-> Agent$ Bool))) (= (exists ((?v2 Agent$)) (and (member$ ?v2 (set$b ?v0)) (?v1 ?v2))) (exists ((?v2 Agent_list$) (?v3 Agent$) (?v4 Agent_list$)) (and (= ?v0 (append$b ?v2 (cons$c ?v3 ?v4))) (and (?v1 ?v3) (forall ((?v5 Agent$)) (=> (member$ ?v5 (set$b ?v4)) (not (?v1 ?v5))))))))) :named a319)) -(assert (! (forall ((?v0 Event_list$) (?v1 (-> Event$ Bool))) (= (exists ((?v2 Event$)) (and (member$b ?v2 (set$ ?v0)) (?v1 ?v2))) (exists ((?v2 Event_list$) (?v3 Event$) (?v4 Event_list$)) (and (= ?v0 (append$ ?v2 (cons$ ?v3 ?v4))) (and (?v1 ?v3) (forall ((?v5 Event$)) (=> (member$b ?v5 (set$ ?v4)) (not (?v1 ?v5))))))))) :named a320)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_list$)) (= (member$a ?v0 (set$a ?v1)) (exists ((?v2 Msg_list$) (?v3 Msg_list$)) (and (= ?v1 (append$a ?v2 (cons$b ?v0 ?v3))) (not (member$a ?v0 (set$a ?v2))))))) :named a321)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_list$)) (= (member$ ?v0 (set$b ?v1)) (exists ((?v2 Agent_list$) (?v3 Agent_list$)) (and (= ?v1 (append$b ?v2 (cons$c ?v0 ?v3))) (not (member$ ?v0 (set$b ?v2))))))) :named a322)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$)) (= (member$b ?v0 (set$ ?v1)) (exists ((?v2 Event_list$) (?v3 Event_list$)) (and (= ?v1 (append$ ?v2 (cons$ ?v0 ?v3))) (not (member$b ?v0 (set$ ?v2))))))) :named a323)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_list$)) (= (member$a ?v0 (set$a ?v1)) (exists ((?v2 Msg_list$) (?v3 Msg_list$)) (and (= ?v1 (append$a ?v2 (cons$b ?v0 ?v3))) (not (member$a ?v0 (set$a ?v3))))))) :named a324)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_list$)) (= (member$ ?v0 (set$b ?v1)) (exists ((?v2 Agent_list$) (?v3 Agent_list$)) (and (= ?v1 (append$b ?v2 (cons$c ?v0 ?v3))) (not (member$ ?v0 (set$b ?v3))))))) :named a325)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$)) (= (member$b ?v0 (set$ ?v1)) (exists ((?v2 Event_list$) (?v3 Event_list$)) (and (= ?v1 (append$ ?v2 (cons$ ?v0 ?v3))) (not (member$b ?v0 (set$ ?v3))))))) :named a326)) -(assert (! (forall ((?v0 Msg_list$) (?v1 (-> Msg$ Bool))) (=> (and (exists ((?v2 Msg$)) (and (member$a ?v2 (set$a ?v0)) (?v1 ?v2))) (forall ((?v2 Msg_list$) (?v3 Msg$) (?v4 Msg_list$)) (=> (and (= ?v0 (append$a ?v2 (cons$b ?v3 ?v4))) (and (?v1 ?v3) (forall ((?v5 Msg$)) (=> (member$a ?v5 (set$a ?v2)) (not (?v1 ?v5)))))) false))) false)) :named a327)) -(assert (! (forall ((?v0 Agent_list$) (?v1 (-> Agent$ Bool))) (=> (and (exists ((?v2 Agent$)) (and (member$ ?v2 (set$b ?v0)) (?v1 ?v2))) (forall ((?v2 Agent_list$) (?v3 Agent$) (?v4 Agent_list$)) (=> (and (= ?v0 (append$b ?v2 (cons$c ?v3 ?v4))) (and (?v1 ?v3) (forall ((?v5 Agent$)) (=> (member$ ?v5 (set$b ?v2)) (not (?v1 ?v5)))))) false))) false)) :named a328)) -(assert (! (forall ((?v0 Event_list$) (?v1 (-> Event$ Bool))) (=> (and (exists ((?v2 Event$)) (and (member$b ?v2 (set$ ?v0)) (?v1 ?v2))) (forall ((?v2 Event_list$) (?v3 Event$) (?v4 Event_list$)) (=> (and (= ?v0 (append$ ?v2 (cons$ ?v3 ?v4))) (and (?v1 ?v3) (forall ((?v5 Event$)) (=> (member$b ?v5 (set$ ?v2)) (not (?v1 ?v5)))))) false))) false)) :named a329)) -(assert (! (forall ((?v0 Msg_list$) (?v1 (-> Msg$ Bool))) (=> (and (exists ((?v2 Msg$)) (and (member$a ?v2 (set$a ?v0)) (?v1 ?v2))) (forall ((?v2 Msg_list$) (?v3 Msg$) (?v4 Msg_list$)) (=> (and (= ?v0 (append$a ?v2 (cons$b ?v3 ?v4))) (and (?v1 ?v3) (forall ((?v5 Msg$)) (=> (member$a ?v5 (set$a ?v4)) (not (?v1 ?v5)))))) false))) false)) :named a330)) -(assert (! (forall ((?v0 Agent_list$) (?v1 (-> Agent$ Bool))) (=> (and (exists ((?v2 Agent$)) (and (member$ ?v2 (set$b ?v0)) (?v1 ?v2))) (forall ((?v2 Agent_list$) (?v3 Agent$) (?v4 Agent_list$)) (=> (and (= ?v0 (append$b ?v2 (cons$c ?v3 ?v4))) (and (?v1 ?v3) (forall ((?v5 Agent$)) (=> (member$ ?v5 (set$b ?v4)) (not (?v1 ?v5)))))) false))) false)) :named a331)) -(assert (! (forall ((?v0 Event_list$) (?v1 (-> Event$ Bool))) (=> (and (exists ((?v2 Event$)) (and (member$b ?v2 (set$ ?v0)) (?v1 ?v2))) (forall ((?v2 Event_list$) (?v3 Event$) (?v4 Event_list$)) (=> (and (= ?v0 (append$ ?v2 (cons$ ?v3 ?v4))) (and (?v1 ?v3) (forall ((?v5 Event$)) (=> (member$b ?v5 (set$ ?v4)) (not (?v1 ?v5)))))) false))) false)) :named a332)) -(assert (! (forall ((?v0 Msg_list$) (?v1 (-> Msg$ Bool))) (=> (exists ((?v2 Msg$)) (and (member$a ?v2 (set$a ?v0)) (?v1 ?v2))) (exists ((?v2 Msg_list$) (?v3 Msg$) (?v4 Msg_list$)) (and (= ?v0 (append$a ?v2 (cons$b ?v3 ?v4))) (and (?v1 ?v3) (forall ((?v5 Msg$)) (=> (member$a ?v5 (set$a ?v2)) (not (?v1 ?v5))))))))) :named a333)) -(assert (! (forall ((?v0 Agent_list$) (?v1 (-> Agent$ Bool))) (=> (exists ((?v2 Agent$)) (and (member$ ?v2 (set$b ?v0)) (?v1 ?v2))) (exists ((?v2 Agent_list$) (?v3 Agent$) (?v4 Agent_list$)) (and (= ?v0 (append$b ?v2 (cons$c ?v3 ?v4))) (and (?v1 ?v3) (forall ((?v5 Agent$)) (=> (member$ ?v5 (set$b ?v2)) (not (?v1 ?v5))))))))) :named a334)) -(assert (! (forall ((?v0 Event_list$) (?v1 (-> Event$ Bool))) (=> (exists ((?v2 Event$)) (and (member$b ?v2 (set$ ?v0)) (?v1 ?v2))) (exists ((?v2 Event_list$) (?v3 Event$) (?v4 Event_list$)) (and (= ?v0 (append$ ?v2 (cons$ ?v3 ?v4))) (and (?v1 ?v3) (forall ((?v5 Event$)) (=> (member$b ?v5 (set$ ?v2)) (not (?v1 ?v5))))))))) :named a335)) -(assert (! (forall ((?v0 Msg_list$) (?v1 (-> Msg$ Bool))) (=> (exists ((?v2 Msg$)) (and (member$a ?v2 (set$a ?v0)) (?v1 ?v2))) (exists ((?v2 Msg_list$) (?v3 Msg$) (?v4 Msg_list$)) (and (= ?v0 (append$a ?v2 (cons$b ?v3 ?v4))) (and (?v1 ?v3) (forall ((?v5 Msg$)) (=> (member$a ?v5 (set$a ?v4)) (not (?v1 ?v5))))))))) :named a336)) -(assert (! (forall ((?v0 Agent_list$) (?v1 (-> Agent$ Bool))) (=> (exists ((?v2 Agent$)) (and (member$ ?v2 (set$b ?v0)) (?v1 ?v2))) (exists ((?v2 Agent_list$) (?v3 Agent$) (?v4 Agent_list$)) (and (= ?v0 (append$b ?v2 (cons$c ?v3 ?v4))) (and (?v1 ?v3) (forall ((?v5 Agent$)) (=> (member$ ?v5 (set$b ?v4)) (not (?v1 ?v5))))))))) :named a337)) -(assert (! (forall ((?v0 Event_list$) (?v1 (-> Event$ Bool))) (=> (exists ((?v2 Event$)) (and (member$b ?v2 (set$ ?v0)) (?v1 ?v2))) (exists ((?v2 Event_list$) (?v3 Event$) (?v4 Event_list$)) (and (= ?v0 (append$ ?v2 (cons$ ?v3 ?v4))) (and (?v1 ?v3) (forall ((?v5 Event$)) (=> (member$b ?v5 (set$ ?v4)) (not (?v1 ?v5))))))))) :named a338)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_list$)) (= (member$a ?v0 (set$a ?v1)) (exists ((?v2 Msg_list$) (?v3 Msg_list$)) (= ?v1 (append$a ?v2 (cons$b ?v0 ?v3)))))) :named a339)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_list$)) (= (member$ ?v0 (set$b ?v1)) (exists ((?v2 Agent_list$) (?v3 Agent_list$)) (= ?v1 (append$b ?v2 (cons$c ?v0 ?v3)))))) :named a340)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$)) (= (member$b ?v0 (set$ ?v1)) (exists ((?v2 Event_list$) (?v3 Event_list$)) (= ?v1 (append$ ?v2 (cons$ ?v0 ?v3)))))) :named a341)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_list$) (?v2 Msg_list$) (?v3 Msg_list$) (?v4 Msg_list$)) (=> (and (not (member$a ?v0 (set$a ?v1))) (not (member$a ?v0 (set$a ?v2)))) (= (= (append$a ?v1 (cons$b ?v0 ?v2)) (append$a ?v3 (cons$b ?v0 ?v4))) (and (= ?v1 ?v3) (= ?v2 ?v4))))) :named a342)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_list$) (?v2 Agent_list$) (?v3 Agent_list$) (?v4 Agent_list$)) (=> (and (not (member$ ?v0 (set$b ?v1))) (not (member$ ?v0 (set$b ?v2)))) (= (= (append$b ?v1 (cons$c ?v0 ?v2)) (append$b ?v3 (cons$c ?v0 ?v4))) (and (= ?v1 ?v3) (= ?v2 ?v4))))) :named a343)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$) (?v2 Event_list$) (?v3 Event_list$) (?v4 Event_list$)) (=> (and (not (member$b ?v0 (set$ ?v1))) (not (member$b ?v0 (set$ ?v2)))) (= (= (append$ ?v1 (cons$ ?v0 ?v2)) (append$ ?v3 (cons$ ?v0 ?v4))) (and (= ?v1 ?v3) (= ?v2 ?v4))))) :named a344)) -(assert (! (forall ((?v0 Msg_list$) (?v1 (-> Msg$ Bool))) (=> (and (exists ((?v2 Msg$)) (and (member$a ?v2 (set$a ?v0)) (?v1 ?v2))) (forall ((?v2 Msg_list$) (?v3 Msg$) (?v4 Msg_list$)) (=> (and (= ?v0 (append$a ?v2 (cons$b ?v3 ?v4))) (?v1 ?v3)) false))) false)) :named a345)) -(assert (! (forall ((?v0 Agent_list$) (?v1 (-> Agent$ Bool))) (=> (and (exists ((?v2 Agent$)) (and (member$ ?v2 (set$b ?v0)) (?v1 ?v2))) (forall ((?v2 Agent_list$) (?v3 Agent$) (?v4 Agent_list$)) (=> (and (= ?v0 (append$b ?v2 (cons$c ?v3 ?v4))) (?v1 ?v3)) false))) false)) :named a346)) -(assert (! (forall ((?v0 Event_list$) (?v1 (-> Event$ Bool))) (=> (and (exists ((?v2 Event$)) (and (member$b ?v2 (set$ ?v0)) (?v1 ?v2))) (forall ((?v2 Event_list$) (?v3 Event$) (?v4 Event_list$)) (=> (and (= ?v0 (append$ ?v2 (cons$ ?v3 ?v4))) (?v1 ?v3)) false))) false)) :named a347)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_list$)) (=> (member$a ?v0 (set$a ?v1)) (exists ((?v2 Msg_list$) (?v3 Msg_list$)) (and (= ?v1 (append$a ?v2 (cons$b ?v0 ?v3))) (not (member$a ?v0 (set$a ?v2))))))) :named a348)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_list$)) (=> (member$ ?v0 (set$b ?v1)) (exists ((?v2 Agent_list$) (?v3 Agent_list$)) (and (= ?v1 (append$b ?v2 (cons$c ?v0 ?v3))) (not (member$ ?v0 (set$b ?v2))))))) :named a349)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$)) (=> (member$b ?v0 (set$ ?v1)) (exists ((?v2 Event_list$) (?v3 Event_list$)) (and (= ?v1 (append$ ?v2 (cons$ ?v0 ?v3))) (not (member$b ?v0 (set$ ?v2))))))) :named a350)) -(assert (! (forall ((?v0 Msg_list$) (?v1 (-> Msg$ Bool))) (=> (exists ((?v2 Msg$)) (and (member$a ?v2 (set$a ?v0)) (?v1 ?v2))) (exists ((?v2 Msg_list$) (?v3 Msg$) (?v4 Msg_list$)) (and (= ?v0 (append$a ?v2 (cons$b ?v3 ?v4))) (?v1 ?v3))))) :named a351)) -(assert (! (forall ((?v0 Agent_list$) (?v1 (-> Agent$ Bool))) (=> (exists ((?v2 Agent$)) (and (member$ ?v2 (set$b ?v0)) (?v1 ?v2))) (exists ((?v2 Agent_list$) (?v3 Agent$) (?v4 Agent_list$)) (and (= ?v0 (append$b ?v2 (cons$c ?v3 ?v4))) (?v1 ?v3))))) :named a352)) -(assert (! (forall ((?v0 Event_list$) (?v1 (-> Event$ Bool))) (=> (exists ((?v2 Event$)) (and (member$b ?v2 (set$ ?v0)) (?v1 ?v2))) (exists ((?v2 Event_list$) (?v3 Event$) (?v4 Event_list$)) (and (= ?v0 (append$ ?v2 (cons$ ?v3 ?v4))) (?v1 ?v3))))) :named a353)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_list$)) (=> (member$a ?v0 (set$a ?v1)) (exists ((?v2 Msg_list$) (?v3 Msg_list$)) (and (= ?v1 (append$a ?v2 (cons$b ?v0 ?v3))) (not (member$a ?v0 (set$a ?v3))))))) :named a354)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_list$)) (=> (member$ ?v0 (set$b ?v1)) (exists ((?v2 Agent_list$) (?v3 Agent_list$)) (and (= ?v1 (append$b ?v2 (cons$c ?v0 ?v3))) (not (member$ ?v0 (set$b ?v3))))))) :named a355)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$)) (=> (member$b ?v0 (set$ ?v1)) (exists ((?v2 Event_list$) (?v3 Event_list$)) (and (= ?v1 (append$ ?v2 (cons$ ?v0 ?v3))) (not (member$b ?v0 (set$ ?v3))))))) :named a356)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_list$)) (=> (member$a ?v0 (set$a ?v1)) (exists ((?v2 Msg_list$) (?v3 Msg_list$)) (= ?v1 (append$a ?v2 (cons$b ?v0 ?v3)))))) :named a357)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_list$)) (=> (member$ ?v0 (set$b ?v1)) (exists ((?v2 Agent_list$) (?v3 Agent_list$)) (= ?v1 (append$b ?v2 (cons$c ?v0 ?v3)))))) :named a358)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$)) (=> (member$b ?v0 (set$ ?v1)) (exists ((?v2 Event_list$) (?v3 Event_list$)) (= ?v1 (append$ ?v2 (cons$ ?v0 ?v3)))))) :named a359)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent$) (?v2 Msg$) (?v3 Event_list$)) (=> (member$b (says$ ?v0 ?v1 ?v2) (set$ ?v3)) (member$a ?v2 (knows$ ?v0 ?v3)))) :named a360)) -(assert (! (forall ((?v0 Agent$) (?v1 Msg$) (?v2 Event_list$)) (=> (member$b (notes$ ?v0 ?v1) (set$ ?v2)) (member$a ?v1 (knows$ ?v0 ?v2)))) :named a361)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_list$)) (! (= (insert$d ?v0 ?v1) (ite (member$a ?v0 (set$a ?v1)) ?v1 (cons$b ?v0 ?v1))) :pattern ((insert$d ?v0 ?v1)))) :named a362)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_list$)) (! (= (insert$e ?v0 ?v1) (ite (member$ ?v0 (set$b ?v1)) ?v1 (cons$c ?v0 ?v1))) :pattern ((insert$e ?v0 ?v1)))) :named a363)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$)) (! (= (insert$a ?v0 ?v1) (ite (member$b ?v0 (set$ ?v1)) ?v1 (cons$ ?v0 ?v1))) :pattern ((insert$a ?v0 ?v1)))) :named a364)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent$) (?v2 Msg$) (?v3 Event_list$)) (=> (member$b (says$ ?v0 ?v1 ?v2) (set$ ?v3)) (member$a ?v2 (knows$ spy$ ?v3)))) :named a365)) -(assert (! (forall ((?v0 Agent$) (?v1 Msg$) (?v2 Event_list$)) (=> (and (not (= ?v0 spy$)) (member$b (gets$ ?v0 ?v1) (set$ ?v2))) (member$a ?v1 (knows$ ?v0 ?v2)))) :named a366)) -(assert (! (forall ((?v0 Msg$) (?v1 Event_list$)) (=> (member$a ?v0 (knows$ spy$ ?v1)) (exists ((?v2 Agent$) (?v3 Agent$)) (or (member$b (says$ ?v2 ?v3 ?v0) (set$ ?v1)) (or (member$b (notes$ ?v2 ?v0) (set$ ?v1)) (member$a ?v0 (initState$ spy$))))))) :named a367)) -(assert (! (forall ((?v0 Msg_list$) (?v1 Msg$) (?v2 Msg_list_set$)) (=> (member$e (append$a ?v0 (cons$b ?v1 nil$b)) ?v2) (member$a ?v1 (succ$a ?v2 ?v0)))) :named a368)) -(assert (! (forall ((?v0 Agent_list$) (?v1 Agent$) (?v2 Agent_list_set$)) (=> (member$f (append$b ?v0 (cons$c ?v1 nil$c)) ?v2) (member$ ?v1 (succ$b ?v2 ?v0)))) :named a369)) -(assert (! (forall ((?v0 Event_list$) (?v1 Event$) (?v2 Event_list_set$)) (=> (member$c (append$ ?v0 (cons$ ?v1 nil$)) ?v2) (member$b ?v1 (succ$ ?v2 ?v0)))) :named a370)) -(assert (! (forall ((?v0 Event_list$) (?v1 Agent$) (?v2 Msg$)) (= (knows$ spy$ (append$ ?v0 (cons$ (notes$ ?v1 ?v2) nil$))) (ite (member$ ?v1 bad$) (insert$ ?v2 (knows$ spy$ ?v0)) (knows$ spy$ ?v0)))) :named a371)) -(assert (! (member$ spy$ bad$) :named a372)) -(assert (! (forall ((?v0 Agent$) (?v1 Msg$) (?v2 Event_list$)) (! (= (knows$ spy$ (cons$ (notes$ ?v0 ?v1) ?v2)) (ite (member$ ?v0 bad$) (insert$ ?v1 (knows$ spy$ ?v2)) (knows$ spy$ ?v2))) :pattern ((cons$ (notes$ ?v0 ?v1) ?v2)))) :named a373)) -(assert (! (forall ((?v0 Agent$) (?v1 Msg$) (?v2 Event_list$)) (=> (and (member$b (notes$ ?v0 ?v1) (set$ ?v2)) (member$ ?v0 bad$)) (member$a ?v1 (knows$ spy$ ?v2)))) :named a374)) -(assert (! (forall ((?v0 Agent$) (?v1 Event$) (?v2 Event_list$)) (= (knows$ ?v0 (cons$ ?v1 ?v2)) (ite (= ?v0 spy$) (case_event$ (uuo$ ?v2) (uup$ ?v2) (uuq$ ?v2) ?v1) (case_event$ (uur$ ?v0 ?v2) (uus$ ?v0 ?v2) (uus$ ?v0 ?v2) ?v1)))) :named a375)) -(check-sat) |