(benchmark x
:formula

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

)