1 (benchmark Isabelle
2 :extrafuns (
3 (uf_1 Int)
4 )
5 :assumption (not (< (+ uf_1 (+ (mod uf_1 2) (mod uf_1 2))) (+ uf_1 3)))
6 :formula true
7 )