(benchmark x
:formula

(and (distinct a b) (= x y))

)