(benchmark reject_nonlinear
:logic QF_LRA
:extrafuns ((n Real))
:status unknown
:formula
(= (/ n n) 1)
)