1
(benchmark Isabelle
2
:extrasorts ( T1 T2)
3
:extrapreds (
4
(up_1 T1)
5
)
6
:assumption (not (or (forall (?x1 T1) (up_1 ?x1)) (not (forall (?x2 T1) (up_1 ?x2)))))
7
:formula true
8