1(benchmark pred.smt
2:status unsat
3:logic QF_UF
4:category { crafted }
5
6:extrafuns ((x U))
7:extrafuns ((y U))
8:extrapreds ((f U))
9
10
11
12:formula
13(and
14 (f x)
15 (iff (f x) (f y))
16 (not (f y))
17)
18)
19