1 (benchmark Isabelle
2 :assumption (not (forall (?x1 Int) (?x2 Int) (not (= (+ (* 2 ?x1) 1) (* 2 ?x2)))))
3 :formula true
4 )