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