(set-logic QF_UF)

(declare-fun x () Bool)
(declare-fun y () Bool)
(declare-fun z () Bool)



(assert
  (not
    (and
      (or x y z)
      (and (=> x y)  (or y z)))))

(check-sat)
(get-model)
(exit)