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