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