1 (benchmark Isabelle
2 :extrafuns (
3 (uf_1 Int)
4 )
5 :assumption (< 0 uf_1)
6 :assumption (not (distinct uf_1 (* uf_1 2) (- uf_1 uf_1)))
7 :formula true
8 )