(declare-sort V 0)
(declare-datatypes () ((B$2 _0@2 _1@2) (B$3 _0@3 _1@3 _2@3)))
(declare-fun ReviewerBids (V V) Bool)
(declare-fun ReviewerAssignments (V V) Bool)
(declare-fun G (V) Bool)
(declare-fun Authors (V V) Bool)
(declare-fun Papers (V V B$3 B$3) Bool)
(declare-fun Reviewers (V V B$2) Bool)
(declare-fun Conflicts (V V) Bool)
(declare-fun ReviewerBids_ (V V) Bool)
(declare-fun ReviewerAssignments_ (V V) Bool)
(declare-fun G_ (V) Bool)
(declare-fun Authors_ (V V) Bool)
(declare-fun Papers_0_0 (V V) Bool)
(declare-fun Papers_0_1 (V V) Bool)
(declare-fun Papers_0_2 (V V) Bool)
(declare-fun Papers_1_0 (V V) Bool)
(declare-fun Papers_1_1 (V V) Bool)
(declare-fun Papers_1_2 (V V) Bool)
(declare-fun Papers_2_0 (V V) Bool)
(declare-fun Papers_2_1 (V V) Bool)
(declare-fun Papers_2_2 (V V) Bool)
(declare-fun Reviewers_0 (V V) Bool)
(declare-fun Reviewers_1 (V V) Bool)
(declare-fun Conflicts_ (V V) Bool)
(declare-const currentUser V)
(declare-const bidId V)
(assert (not (=> (and (and (forall ((x V)) (forall ((y V)) (=> (ReviewerBids x y) (not (Conflicts x y))))) (forall ((x V)) (forall ((y V)) (=> (ReviewerAssignments x y) (not (Conflicts x y)))))) (forall ((x V)) (iff (G x) (exists ((y V)) (or (or (or (or (and (Papers_0_0 x y) (not (Conflicts currentUser x))) (and (Papers_0_1 x y) (not (Conflicts currentUser x)))) (and (Papers_0_2 x y) (not (Conflicts currentUser x)))) (or (or (and (Papers_1_0 x y) (not (Conflicts currentUser x))) (and (Papers_1_1 x y) (not (Conflicts currentUser x)))) (and (Papers_1_2 x y) (not (Conflicts currentUser x))))) (or (or (and (Papers_2_0 x y) (not (Conflicts currentUser x))) (and (Papers_2_1 x y) (not (Conflicts currentUser x)))) (and (Papers_2_2 x y) (not (Conflicts currentUser x))))))))) (or (and (exists ((x V)) (and (= x bidId) (G x))) (and (forall ((x V)) (forall ((y V)) (=> (or (ReviewerBids x y) (and (= x currentUser) (= y bidId))) (not (Conflicts x y))))) (forall ((x V)) (forall ((y V)) (=> (ReviewerAssignments x y) (not (Conflicts x y))))))) (and (not (exists ((x V)) (and (= x bidId) (G x)))) (and (forall ((x V)) (forall ((y V)) (=> (ReviewerBids x y) (not (Conflicts x y))))) (forall ((x V)) (forall ((y V)) (=> (ReviewerAssignments x y) (not (Conflicts x y)))))))))) )
(check-sat)
(get-model)