(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
)