(set-logic QF_UFLIA)

(declare-fun r () Int)
(declare-fun s () Int)
(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun z () Int)

(declare-fun g (Int) Int)

(declare-fun p1 () Bool)
(declare-fun p2 () Bool)


(assert (or (= r (g x)) p1))
(assert (or (not p2) (= x y)))
(assert (or (= y z) (not p2)))
(assert (or (not (= x z)) (not p1)))
(assert (or p1 (= y z)))
(assert (or (= s (g y)) (not p1)))
(assert (or p1 (distinct r s) (not p2)))