(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)
(assert (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) (= y user)))) (or (Subscriptions x y) (and (= x news_letter) (= y user)))))))) )
(check-sat)
(get-model)