(declare-sort V 0)
(declare-fun Letter (V) Bool)
(declare-fun User (V) Bool)
(declare-fun Subscriptions (V V) Bool)
(declare-fun Letter_ (V) Bool)
(declare-fun User_ (V) Bool)
(declare-fun Subscriptions_ (V V) Bool)
(declare-const news_letter V)
(declare-const user V)
(declare-const news_letter$_0 V)
(declare-const user$_0 V)
(declare-const news_letter$_1 V)
(declare-const user$_1 V)
(declare-const news_letter$_2 V)
(declare-const user$_2 V)
(declare-const news_letter$_3 V)
(declare-const user$_3 V)
(declare-const news_letter$_4 V)
(declare-const user$_4 V)
(declare-const news_letter$_5 V)
(declare-const user$_5 V)
(declare-const news_letter$_6 V)
(declare-const user$_6 V)
(declare-const news_letter$_7 V)
(declare-const user$_7 V)
(declare-const news_letter$_8 V)
(declare-const user$_8 V)
(declare-const news_letter$_9 V)
(declare-const user$_9 V)
(assert (or (or (or (or (or (or (or (or (or (not (=> (and (and (and (and (exists ((x V)) (forall ((y V)) (=> (exists ((x V)) (Subscriptions x y)) (Subscriptions x y)))) (forall ((x V)) (forall ((y V)) (=> (Subscriptions y x) (User x))))) (forall ((x V)) (forall ((y V)) (=> (Subscriptions y x) (Letter y))))) (forall ((x V)) (=> (User x) (exists ((y V)) (Subscriptions y x))))) (forall ((x V)) (=> (Letter x) (exists ((y V)) (Subscriptions x y))))) (exists ((x V)) (forall ((y V)) (=> (exists ((x V)) (or (Subscriptions x y) (and (= x news_letter$_0) (= y user$_0)))) (or (Subscriptions x y) (and (= x news_letter$_0) (= y user$_0)))))))) (not (=> (and (and (and (and (exists ((x V)) (forall ((y V)) (=> (exists ((x V)) (Subscriptions x y)) (Subscriptions x y)))) (forall ((x V)) (forall ((y V)) (=> (Subscriptions y x) (User x))))) (forall ((x V)) (forall ((y V)) (=> (Subscriptions y x) (Letter y))))) (forall ((x V)) (=> (User x) (exists ((y V)) (Subscriptions y x))))) (forall ((x V)) (=> (Letter x) (exists ((y V)) (Subscriptions x y))))) (exists ((x V)) (forall ((y V)) (=> (exists ((x V)) (or (Subscriptions x y) (and (= x news_letter$_1) (= y user$_1)))) (or (Subscriptions x y) (and (= x news_letter$_1) (= y user$_1))))))))) (not (=> (and (and (and (and (exists ((x V)) (forall ((y V)) (=> (exists ((x V)) (Subscriptions x y)) (Subscriptions x y)))) (forall ((x V)) (forall ((y V)) (=> (Subscriptions y x) (User x))))) (forall ((x V)) (forall ((y V)) (=> (Subscriptions y x) (Letter y))))) (forall ((x V)) (=> (User x) (exists ((y V)) (Subscriptions y x))))) (forall ((x V)) (=> (Letter x) (exists ((y V)) (Subscriptions x y))))) (exists ((x V)) (forall ((y V)) (=> (exists ((x V)) (or (Subscriptions x y) (and (= x news_letter$_2) (= y user$_2)))) (or (Subscriptions x y) (and (= x news_letter$_2) (= y user$_2))))))))) (not (=> (and (and (and (and (exists ((x V)) (forall ((y V)) (=> (exists ((x V)) (Subscriptions x y)) (Subscriptions x y)))) (forall ((x V)) (forall ((y V)) (=> (Subscriptions y x) (User x))))) (forall ((x V)) (forall ((y V)) (=> (Subscriptions y x) (Letter y))))) (forall ((x V)) (=> (User x) (exists ((y V)) (Subscriptions y x))))) (forall ((x V)) (=> (Letter x) (exists ((y V)) (Subscriptions x y))))) (exists ((x V)) (forall ((y V)) (=> (exists ((x V)) (or (Subscriptions x y) (and (= x news_letter$_3) (= y user$_3)))) (or (Subscriptions x y) (and (= x news_letter$_3) (= y user$_3))))))))) (not (=> (and (and (and (and (exists ((x V)) (forall ((y V)) (=> (exists ((x V)) (Subscriptions x y)) (Subscriptions x y)))) (forall ((x V)) (forall ((y V)) (=> (Subscriptions y x) (User x))))) (forall ((x V)) (forall ((y V)) (=> (Subscriptions y x) (Letter y))))) (forall ((x V)) (=> (User x) (exists ((y V)) (Subscriptions y x))))) (forall ((x V)) (=> (Letter x) (exists ((y V)) (Subscriptions x y))))) (exists ((x V)) (forall ((y V)) (=> (exists ((x V)) (or (Subscriptions x y) (and (= x news_letter$_4) (= y user$_4)))) (or (Subscriptions x y) (and (= x news_letter$_4) (= y user$_4))))))))) (not (=> (and (and (and (and (exists ((x V)) (forall ((y V)) (=> (exists ((x V)) (Subscriptions x y)) (Subscriptions x y)))) (forall ((x V)) (forall ((y V)) (=> (Subscriptions y x) (User x))))) (forall ((x V)) (forall ((y V)) (=> (Subscriptions y x) (Letter y))))) (forall ((x V)) (=> (User x) (exists ((y V)) (Subscriptions y x))))) (forall ((x V)) (=> (Letter x) (exists ((y V)) (Subscriptions x y))))) (exists ((x V)) (forall ((y V)) (=> (exists ((x V)) (or (Subscriptions x y) (and (= x news_letter$_5) (= y user$_5)))) (or (Subscriptions x y) (and (= x news_letter$_5) (= y user$_5))))))))) (not (=> (and (and (and (and (exists ((x V)) (forall ((y V)) (=> (exists ((x V)) (Subscriptions x y)) (Subscriptions x y)))) (forall ((x V)) (forall ((y V)) (=> (Subscriptions y x) (User x))))) (forall ((x V)) (forall ((y V)) (=> (Subscriptions y x) (Letter y))))) (forall ((x V)) (=> (User x) (exists ((y V)) (Subscriptions y x))))) (forall ((x V)) (=> (Letter x) (exists ((y V)) (Subscriptions x y))))) (exists ((x V)) (forall ((y V)) (=> (exists ((x V)) (or (Subscriptions x y) (and (= x news_letter$_6) (= y user$_6)))) (or (Subscriptions x y) (and (= x news_letter$_6) (= y user$_6))))))))) (not (=> (and (and (and (and (exists ((x V)) (forall ((y V)) (=> (exists ((x V)) (Subscriptions x y)) (Subscriptions x y)))) (forall ((x V)) (forall ((y V)) (=> (Subscriptions y x) (User x))))) (forall ((x V)) (forall ((y V)) (=> (Subscriptions y x) (Letter y))))) (forall ((x V)) (=> (User x) (exists ((y V)) (Subscriptions y x))))) (forall ((x V)) (=> (Letter x) (exists ((y V)) (Subscriptions x y))))) (exists ((x V)) (forall ((y V)) (=> (exists ((x V)) (or (Subscriptions x y) (and (= x news_letter$_7) (= y user$_7)))) (or (Subscriptions x y) (and (= x news_letter$_7) (= y user$_7))))))))) (not (=> (and (and (and (and (exists ((x V)) (forall ((y V)) (=> (exists ((x V)) (Subscriptions x y)) (Subscriptions x y)))) (forall ((x V)) (forall ((y V)) (=> (Subscriptions y x) (User x))))) (forall ((x V)) (forall ((y V)) (=> (Subscriptions y x) (Letter y))))) (forall ((x V)) (=> (User x) (exists ((y V)) (Subscriptions y x))))) (forall ((x V)) (=> (Letter x) (exists ((y V)) (Subscriptions x y))))) (exists ((x V)) (forall ((y V)) (=> (exists ((x V)) (or (Subscriptions x y) (and (= x news_letter$_8) (= y user$_8)))) (or (Subscriptions x y) (and (= x news_letter$_8) (= y user$_8))))))))) (not (=> (and (and (and (and (exists ((x V)) (forall ((y V)) (=> (exists ((x V)) (Subscriptions x y)) (Subscriptions x y)))) (forall ((x V)) (forall ((y V)) (=> (Subscriptions y x) (User x))))) (forall ((x V)) (forall ((y V)) (=> (Subscriptions y x) (Letter y))))) (forall ((x V)) (=> (User x) (exists ((y V)) (Subscriptions y x))))) (forall ((x V)) (=> (Letter x) (exists ((y V)) (Subscriptions x y))))) (exists ((x V)) (forall ((y V)) (=> (exists ((x V)) (or (Subscriptions x y) (and (= x news_letter$_9) (= y user$_9)))) (or (Subscriptions x y) (and (= x news_letter$_9) (= y user$_9))))))))) )
(check-sat)
(get-model)