(benchmark autogen
  :logic AUF
  :extrapreds ((s_2 Int)
               (s Int Int))
  :formula
(and
  (forall (?p Int) (forall (?q Int) (implies (s_2 ?p) (not (s ?p ?q)))))
  (not (forall (?r Int) (forall (?q Int) (implies (s_2 ?r) (not (s ?r ?q)))))))
  :status unknown
)
