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