removed the Nitpick code that loaded the "Nitpick" theory explicitly if it's not already loaded, because this didn't work properly and is of doubtful value
(benchmark Isabelle
:extrasorts ( T1 T2)
:extrafuns (
(uf_2 T1)
(uf_3 T1)
)
:extrapreds (
(up_1 T1)
)
:assumption (if_then_else (up_1 uf_2) (not (exists (?x1 T1) (up_1 ?x1))) (forall (?x2 T1) (not (up_1 ?x2))))
:assumption (not (implies (up_1 uf_2) (up_1 uf_3)))
:formula true
)