(benchmark x
:formula

(not
(implies 
  (and
    (= x 1)
    (= y 2)
  )
  (and
    (= x 1)
    (= y 2)
  )
)
)
)