src/HOL/SMT/Examples/cert/z3_hol_02

provide standard isabelle make targets;
slightly more accurate dependencies;

(benchmark Isabelle
:extrasorts ( T2 T1 T3)
:extrafuns (
  (uf_2 T1)
  (uf_3 T2)
 )
:extrapreds (
  (up_4 T1 T2)
  (up_1 T1 T2)
 )
:assumption (not (or (iff (up_1 uf_2 uf_3) (and (up_4 uf_2 uf_3) true)) (or (iff (up_1 uf_2 uf_3) true) (iff (up_4 uf_2 uf_3) true))))
:formula true
)