1 (benchmark Isabelle
2 :extrasorts ( T1)
3 :extrapreds (
4 (up_1)
5 (up_2)
6 )
7 :assumption (and (or up_1 up_2) (not up_1))
8 :assumption (not up_2)
9 :formula true
10 )