(benchmark qnt_12
  :logic UNKNOWN
  :extrafuns ((a Int) (b Int) (z Int) (f Int Int))
  :extrapreds ((p Int) (q Int Int) (r Int))
  :status unsat
  :formula
  (and
    (forall (?x Int) (implies (and (p ?x) (q (f a) ?x)) (r ?x)))
    (forall (?x Int) (implies (and (p ?x) (r ?x)) (= ?x z)))
    (p a)
    (q (f a) a)
    (<= (- b z) 0)
    (<= (- z b) 0)
    (not (= a b))
  )
  :status unsat
)
