1 (benchmark Isabelle
2 :extrafuns (
3 (uf_1 Real)
4 (uf_2 Real)
5 )
6 :assumption (not (= (- (* uf_1 (+ 1.0 uf_2)) (* uf_1 (- 1.0 uf_2))) (* (* 2.0 uf_1) uf_2)))
7 :formula true
8 )