(set-option :incremental false)
(set-logic QF_AUFBV)
(declare-fun a () (_ BitVec 32))
(declare-fun b () (_ BitVec 32))
(declare-fun c () (_ BitVec 32))
(declare-fun d () (_ BitVec 32))
(declare-fun e () (_ BitVec 32))
(declare-fun f () (_ BitVec 32))
(assert (= b (bvnot a)))
(assert (= c (bvnot b)))
(assert (= d (bvnot c)))
(assert (= e (bvnot d)))
(assert (= f (bvnot f)))
(assert (= a f))
(check-sat)