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