(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)
(declare-const news_letter$_10 V)
(declare-const user$_10 V)
(declare-const news_letter$_11 V)
(declare-const user$_11 V)
(declare-const news_letter$_12 V)
(declare-const user$_12 V)
(declare-const news_letter$_13 V)
(declare-const user$_13 V)
(declare-const news_letter$_14 V)
(declare-const user$_14 V)
(declare-const news_letter$_15 V)
(declare-const user$_15 V)
(declare-const news_letter$_16 V)
(declare-const user$_16 V)
(declare-const news_letter$_17 V)
(declare-const user$_17 V)
(declare-const news_letter$_18 V)
(declare-const user$_18 V)
(declare-const news_letter$_19 V)
(declare-const user$_19 V)
(declare-const news_letter$_20 V)
(declare-const user$_20 V)
(declare-const news_letter$_21 V)
(declare-const user$_21 V)
(declare-const news_letter$_22 V)
(declare-const user$_22 V)
(declare-const news_letter$_23 V)
(declare-const user$_23 V)
(declare-const news_letter$_24 V)
(declare-const user$_24 V)
(declare-const news_letter$_25 V)
(declare-const user$_25 V)
(declare-const news_letter$_26 V)
(declare-const user$_26 V)
(declare-const news_letter$_27 V)
(declare-const user$_27 V)
(declare-const news_letter$_28 V)
(declare-const user$_28 V)
(declare-const news_letter$_29 V)
(declare-const user$_29 V)
(declare-const news_letter$_30 V)
(declare-const user$_30 V)
(declare-const news_letter$_31 V)
(declare-const user$_31 V)
(declare-const news_letter$_32 V)
(declare-const user$_32 V)
(declare-const news_letter$_33 V)
(declare-const user$_33 V)
(declare-const news_letter$_34 V)
(declare-const user$_34 V)
(declare-const news_letter$_35 V)
(declare-const user$_35 V)
(declare-const news_letter$_36 V)
(declare-const user$_36 V)
(declare-const news_letter$_37 V)
(declare-const user$_37 V)
(declare-const news_letter$_38 V)
(declare-const user$_38 V)
(declare-const news_letter$_39 V)
(declare-const user$_39 V)
(declare-const news_letter$_40 V)
(declare-const user$_40 V)
(declare-const news_letter$_41 V)
(declare-const user$_41 V)
(declare-const news_letter$_42 V)
(declare-const user$_42 V)
(declare-const news_letter$_43 V)
(declare-const user$_43 V)
(declare-const news_letter$_44 V)
(declare-const user$_44 V)
(declare-const news_letter$_45 V)
(declare-const user$_45 V)
(declare-const news_letter$_46 V)
(declare-const user$_46 V)
(declare-const news_letter$_47 V)
(declare-const user$_47 V)
(declare-const news_letter$_48 V)
(declare-const user$_48 V)
(declare-const news_letter$_49 V)
(declare-const user$_49 V)
(declare-const news_letter$_50 V)
(declare-const user$_50 V)
(declare-const news_letter$_51 V)
(declare-const user$_51 V)
(declare-const news_letter$_52 V)
(declare-const user$_52 V)
(declare-const news_letter$_53 V)
(declare-const user$_53 V)
(declare-const news_letter$_54 V)
(declare-const user$_54 V)
(declare-const news_letter$_55 V)
(declare-const user$_55 V)
(declare-const news_letter$_56 V)
(declare-const user$_56 V)
(declare-const news_letter$_57 V)
(declare-const user$_57 V)
(declare-const news_letter$_58 V)
(declare-const user$_58 V)
(declare-const news_letter$_59 V)
(declare-const user$_59 V)
(declare-const news_letter$_60 V)
(declare-const user$_60 V)
(declare-const news_letter$_61 V)
(declare-const user$_61 V)
(declare-const news_letter$_62 V)
(declare-const user$_62 V)
(declare-const news_letter$_63 V)
(declare-const user$_63 V)
(declare-const news_letter$_64 V)
(declare-const user$_64 V)
(declare-const news_letter$_65 V)
(declare-const user$_65 V)
(declare-const news_letter$_66 V)
(declare-const user$_66 V)
(declare-const news_letter$_67 V)
(declare-const user$_67 V)
(declare-const news_letter$_68 V)
(declare-const user$_68 V)
(declare-const news_letter$_69 V)
(declare-const user$_69 V)
(declare-const news_letter$_70 V)
(declare-const user$_70 V)
(declare-const news_letter$_71 V)
(declare-const user$_71 V)
(declare-const news_letter$_72 V)
(declare-const user$_72 V)
(declare-const news_letter$_73 V)
(declare-const user$_73 V)
(declare-const news_letter$_74 V)
(declare-const user$_74 V)
(declare-const news_letter$_75 V)
(declare-const user$_75 V)
(declare-const news_letter$_76 V)
(declare-const user$_76 V)
(declare-const news_letter$_77 V)
(declare-const user$_77 V)
(declare-const news_letter$_78 V)
(declare-const user$_78 V)
(declare-const news_letter$_79 V)
(declare-const user$_79 V)
(declare-const news_letter$_80 V)
(declare-const user$_80 V)
(declare-const news_letter$_81 V)
(declare-const user$_81 V)
(declare-const news_letter$_82 V)
(declare-const user$_82 V)
(declare-const news_letter$_83 V)
(declare-const user$_83 V)
(declare-const news_letter$_84 V)
(declare-const user$_84 V)
(declare-const news_letter$_85 V)
(declare-const user$_85 V)
(declare-const news_letter$_86 V)
(declare-const user$_86 V)
(declare-const news_letter$_87 V)
(declare-const user$_87 V)
(declare-const news_letter$_88 V)
(declare-const user$_88 V)
(declare-const news_letter$_89 V)
(declare-const user$_89 V)
(declare-const news_letter$_90 V)
(declare-const user$_90 V)
(declare-const news_letter$_91 V)
(declare-const user$_91 V)
(declare-const news_letter$_92 V)
(declare-const user$_92 V)
(declare-const news_letter$_93 V)
(declare-const user$_93 V)
(declare-const news_letter$_94 V)
(declare-const user$_94 V)
(declare-const news_letter$_95 V)
(declare-const user$_95 V)
(declare-const news_letter$_96 V)
(declare-const user$_96 V)
(declare-const news_letter$_97 V)
(declare-const user$_97 V)
(declare-const news_letter$_98 V)
(declare-const user$_98 V)
(declare-const news_letter$_99 V)
(declare-const user$_99 V)
(assert (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (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))))))))) (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$_10) (= y user$_10)))) (or (Subscriptions x y) (and (= x news_letter$_10) (= y user$_10))))))))) (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$_11) (= y user$_11)))) (or (Subscriptions x y) (and (= x news_letter$_11) (= y user$_11))))))))) (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$_12) (= y user$_12)))) (or (Subscriptions x y) (and (= x news_letter$_12) (= y user$_12))))))))) (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$_13) (= y user$_13)))) (or (Subscriptions x y) (and (= x news_letter$_13) (= y user$_13))))))))) (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$_14) (= y user$_14)))) (or (Subscriptions x y) (and (= x news_letter$_14) (= y user$_14))))))))) (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$_15) (= y user$_15)))) (or (Subscriptions x y) (and (= x news_letter$_15) (= y user$_15))))))))) (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$_16) (= y user$_16)))) (or (Subscriptions x y) (and (= x news_letter$_16) (= y user$_16))))))))) (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$_17) (= y user$_17)))) (or (Subscriptions x y) (and (= x news_letter$_17) (= y user$_17))))))))) (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$_18) (= y user$_18)))) (or (Subscriptions x y) (and (= x news_letter$_18) (= y user$_18))))))))) (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$_19) (= y user$_19)))) (or (Subscriptions x y) (and (= x news_letter$_19) (= y user$_19))))))))) (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$_20) (= y user$_20)))) (or (Subscriptions x y) (and (= x news_letter$_20) (= y user$_20))))))))) (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$_21) (= y user$_21)))) (or (Subscriptions x y) (and (= x news_letter$_21) (= y user$_21))))))))) (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$_22) (= y user$_22)))) (or (Subscriptions x y) (and (= x news_letter$_22) (= y user$_22))))))))) (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$_23) (= y user$_23)))) (or (Subscriptions x y) (and (= x news_letter$_23) (= y user$_23))))))))) (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$_24) (= y user$_24)))) (or (Subscriptions x y) (and (= x news_letter$_24) (= y user$_24))))))))) (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$_25) (= y user$_25)))) (or (Subscriptions x y) (and (= x news_letter$_25) (= y user$_25))))))))) (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$_26) (= y user$_26)))) (or (Subscriptions x y) (and (= x news_letter$_26) (= y user$_26))))))))) (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$_27) (= y user$_27)))) (or (Subscriptions x y) (and (= x news_letter$_27) (= y user$_27))))))))) (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$_28) (= y user$_28)))) (or (Subscriptions x y) (and (= x news_letter$_28) (= y user$_28))))))))) (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$_29) (= y user$_29)))) (or (Subscriptions x y) (and (= x news_letter$_29) (= y user$_29))))))))) (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$_30) (= y user$_30)))) (or (Subscriptions x y) (and (= x news_letter$_30) (= y user$_30))))))))) (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$_31) (= y user$_31)))) (or (Subscriptions x y) (and (= x news_letter$_31) (= y user$_31))))))))) (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$_32) (= y user$_32)))) (or (Subscriptions x y) (and (= x news_letter$_32) (= y user$_32))))))))) (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$_33) (= y user$_33)))) (or (Subscriptions x y) (and (= x news_letter$_33) (= y user$_33))))))))) (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$_34) (= y user$_34)))) (or (Subscriptions x y) (and (= x news_letter$_34) (= y user$_34))))))))) (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$_35) (= y user$_35)))) (or (Subscriptions x y) (and (= x news_letter$_35) (= y user$_35))))))))) (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$_36) (= y user$_36)))) (or (Subscriptions x y) (and (= x news_letter$_36) (= y user$_36))))))))) (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$_37) (= y user$_37)))) (or (Subscriptions x y) (and (= x news_letter$_37) (= y user$_37))))))))) (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$_38) (= y user$_38)))) (or (Subscriptions x y) (and (= x news_letter$_38) (= y user$_38))))))))) (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$_39) (= y user$_39)))) (or (Subscriptions x y) (and (= x news_letter$_39) (= y user$_39))))))))) (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$_40) (= y user$_40)))) (or (Subscriptions x y) (and (= x news_letter$_40) (= y user$_40))))))))) (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$_41) (= y user$_41)))) (or (Subscriptions x y) (and (= x news_letter$_41) (= y user$_41))))))))) (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$_42) (= y user$_42)))) (or (Subscriptions x y) (and (= x news_letter$_42) (= y user$_42))))))))) (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$_43) (= y user$_43)))) (or (Subscriptions x y) (and (= x news_letter$_43) (= y user$_43))))))))) (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$_44) (= y user$_44)))) (or (Subscriptions x y) (and (= x news_letter$_44) (= y user$_44))))))))) (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$_45) (= y user$_45)))) (or (Subscriptions x y) (and (= x news_letter$_45) (= y user$_45))))))))) (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$_46) (= y user$_46)))) (or (Subscriptions x y) (and (= x news_letter$_46) (= y user$_46))))))))) (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$_47) (= y user$_47)))) (or (Subscriptions x y) (and (= x news_letter$_47) (= y user$_47))))))))) (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$_48) (= y user$_48)))) (or (Subscriptions x y) (and (= x news_letter$_48) (= y user$_48))))))))) (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$_49) (= y user$_49)))) (or (Subscriptions x y) (and (= x news_letter$_49) (= y user$_49))))))))) (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$_50) (= y user$_50)))) (or (Subscriptions x y) (and (= x news_letter$_50) (= y user$_50))))))))) (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$_51) (= y user$_51)))) (or (Subscriptions x y) (and (= x news_letter$_51) (= y user$_51))))))))) (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$_52) (= y user$_52)))) (or (Subscriptions x y) (and (= x news_letter$_52) (= y user$_52))))))))) (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$_53) (= y user$_53)))) (or (Subscriptions x y) (and (= x news_letter$_53) (= y user$_53))))))))) (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$_54) (= y user$_54)))) (or (Subscriptions x y) (and (= x news_letter$_54) (= y user$_54))))))))) (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$_55) (= y user$_55)))) (or (Subscriptions x y) (and (= x news_letter$_55) (= y user$_55))))))))) (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$_56) (= y user$_56)))) (or (Subscriptions x y) (and (= x news_letter$_56) (= y user$_56))))))))) (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$_57) (= y user$_57)))) (or (Subscriptions x y) (and (= x news_letter$_57) (= y user$_57))))))))) (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$_58) (= y user$_58)))) (or (Subscriptions x y) (and (= x news_letter$_58) (= y user$_58))))))))) (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$_59) (= y user$_59)))) (or (Subscriptions x y) (and (= x news_letter$_59) (= y user$_59))))))))) (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$_60) (= y user$_60)))) (or (Subscriptions x y) (and (= x news_letter$_60) (= y user$_60))))))))) (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$_61) (= y user$_61)))) (or (Subscriptions x y) (and (= x news_letter$_61) (= y user$_61))))))))) (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$_62) (= y user$_62)))) (or (Subscriptions x y) (and (= x news_letter$_62) (= y user$_62))))))))) (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$_63) (= y user$_63)))) (or (Subscriptions x y) (and (= x news_letter$_63) (= y user$_63))))))))) (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$_64) (= y user$_64)))) (or (Subscriptions x y) (and (= x news_letter$_64) (= y user$_64))))))))) (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$_65) (= y user$_65)))) (or (Subscriptions x y) (and (= x news_letter$_65) (= y user$_65))))))))) (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$_66) (= y user$_66)))) (or (Subscriptions x y) (and (= x news_letter$_66) (= y user$_66))))))))) (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$_67) (= y user$_67)))) (or (Subscriptions x y) (and (= x news_letter$_67) (= y user$_67))))))))) (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$_68) (= y user$_68)))) (or (Subscriptions x y) (and (= x news_letter$_68) (= y user$_68))))))))) (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$_69) (= y user$_69)))) (or (Subscriptions x y) (and (= x news_letter$_69) (= y user$_69))))))))) (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$_70) (= y user$_70)))) (or (Subscriptions x y) (and (= x news_letter$_70) (= y user$_70))))))))) (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$_71) (= y user$_71)))) (or (Subscriptions x y) (and (= x news_letter$_71) (= y user$_71))))))))) (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$_72) (= y user$_72)))) (or (Subscriptions x y) (and (= x news_letter$_72) (= y user$_72))))))))) (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$_73) (= y user$_73)))) (or (Subscriptions x y) (and (= x news_letter$_73) (= y user$_73))))))))) (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$_74) (= y user$_74)))) (or (Subscriptions x y) (and (= x news_letter$_74) (= y user$_74))))))))) (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$_75) (= y user$_75)))) (or (Subscriptions x y) (and (= x news_letter$_75) (= y user$_75))))))))) (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$_76) (= y user$_76)))) (or (Subscriptions x y) (and (= x news_letter$_76) (= y user$_76))))))))) (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$_77) (= y user$_77)))) (or (Subscriptions x y) (and (= x news_letter$_77) (= y user$_77))))))))) (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$_78) (= y user$_78)))) (or (Subscriptions x y) (and (= x news_letter$_78) (= y user$_78))))))))) (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$_79) (= y user$_79)))) (or (Subscriptions x y) (and (= x news_letter$_79) (= y user$_79))))))))) (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$_80) (= y user$_80)))) (or (Subscriptions x y) (and (= x news_letter$_80) (= y user$_80))))))))) (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$_81) (= y user$_81)))) (or (Subscriptions x y) (and (= x news_letter$_81) (= y user$_81))))))))) (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$_82) (= y user$_82)))) (or (Subscriptions x y) (and (= x news_letter$_82) (= y user$_82))))))))) (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$_83) (= y user$_83)))) (or (Subscriptions x y) (and (= x news_letter$_83) (= y user$_83))))))))) (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$_84) (= y user$_84)))) (or (Subscriptions x y) (and (= x news_letter$_84) (= y user$_84))))))))) (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$_85) (= y user$_85)))) (or (Subscriptions x y) (and (= x news_letter$_85) (= y user$_85))))))))) (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$_86) (= y user$_86)))) (or (Subscriptions x y) (and (= x news_letter$_86) (= y user$_86))))))))) (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$_87) (= y user$_87)))) (or (Subscriptions x y) (and (= x news_letter$_87) (= y user$_87))))))))) (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$_88) (= y user$_88)))) (or (Subscriptions x y) (and (= x news_letter$_88) (= y user$_88))))))))) (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$_89) (= y user$_89)))) (or (Subscriptions x y) (and (= x news_letter$_89) (= y user$_89))))))))) (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$_90) (= y user$_90)))) (or (Subscriptions x y) (and (= x news_letter$_90) (= y user$_90))))))))) (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$_91) (= y user$_91)))) (or (Subscriptions x y) (and (= x news_letter$_91) (= y user$_91))))))))) (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$_92) (= y user$_92)))) (or (Subscriptions x y) (and (= x news_letter$_92) (= y user$_92))))))))) (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$_93) (= y user$_93)))) (or (Subscriptions x y) (and (= x news_letter$_93) (= y user$_93))))))))) (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$_94) (= y user$_94)))) (or (Subscriptions x y) (and (= x news_letter$_94) (= y user$_94))))))))) (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$_95) (= y user$_95)))) (or (Subscriptions x y) (and (= x news_letter$_95) (= y user$_95))))))))) (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$_96) (= y user$_96)))) (or (Subscriptions x y) (and (= x news_letter$_96) (= y user$_96))))))))) (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$_97) (= y user$_97)))) (or (Subscriptions x y) (and (= x news_letter$_97) (= y user$_97))))))))) (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$_98) (= y user$_98)))) (or (Subscriptions x y) (and (= x news_letter$_98) (= y user$_98))))))))) (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$_99) (= y user$_99)))) (or (Subscriptions x y) (and (= x news_letter$_99) (= y user$_99))))))))) )
(check-sat)
(get-model)