1
(benchmark Isabelle
2
:extrafuns (
3
(uf_1 Int)
4
(uf_2 Int)
5
(uf_3 Int)
6
)
7
:assumption (not (= (* uf_1 (+ (+ uf_2 1) uf_3)) (+ (* uf_1 uf_2) (* uf_1 (+ uf_3 1)))))
8
:formula true
9