; a = b ^ a = 00000 ^ b = 11111 is UNSAT

(check
(% a var_bv
(% b var_bv
(% f1 (th_holds (= BitVec (a_var_bv a) (a_var_bv b)))
(% f2 (th_holds (= BitVec (a_var_bv a) (a_bv (bvc b0 (bvc b0 (bvc b0 (bvc b0 (bvc b0 bvn))))))))
(% f3 (th_holds (= BitVec (a_var_bv b) (a_bv (bvc b1 (bvc b1 (bvc b1 (bvc b1 (bvc b1 bvn))))))))
(: (holds cln)

(decl_bv_atom_var 5 a (\ ba1
(decl_bv_atom_var 5 b (\ ba2
(decl_bv_atom_const _ (bvc b0 (bvc b0 (bvc b0 (bvc b0 (bvc b0 bvn))))) (\ c (\ ba3
(decl_bv_atom_const _ (bvc b1 (bvc b1 (bvc b1 (bvc b1 (bvc b1 bvn))))) (\ d (\ ba4

(decl_atom (bblast a 4) (\ v1 (\ a1
(decl_atom (bblast b 4) (\ v2 (\ a2

; bitblasting terms
(th_let_pf _ (bv_bbl_var _ _ _ ba1) (\ bt1
(th_let_pf _ (bv_bbl_var _ _ _ ba2) (\ bt2
(th_let_pf _ (bv_bbl_const _ _ _ _ ba3) (\ bt3
(th_let_pf _ (bv_bbl_const _ _ _ _ ba4) (\ bt4

; bitblasting formulas
(th_let_pf _ (bv_bbl_eq _ _ _ _ _ bt1 bt2) (\ bf1
(th_let_pf _ (bv_bbl_eq _ _ _ _ _ bt1 bt3) (\ bf2
(th_let_pf _ (bv_bbl_eq _ _ _ _ _ bt2 bt4) (\ bf3

; CNFication
; a.4 V ~b.4
(satlem _ _
(asf _ _ _ a1 (\ l1
(ast _ _ _ a2 (\ l2
(clausify_false
  (contra _ (impl_elim _ _ l2 (iff_elim_2 _ _ (and_elim_1 _ _ (impl_elim _ _ f1 bf1)))) l1)   ; notice at the intermost we impl_elim, which converts from atom to bit-blasting representation
))))) (\ C2

; ~a.4
(satlem _ _
(ast _ _ _ a1 (\ l1
(clausify_false
  (impl_elim _ _ l1 (iff_elim_1 _ _ (and_elim_1 _ _ (impl_elim _ _ f2 bf2))))
))) (\ C3

; b.4 
(satlem _ _
(asf _ _ _ a2 (\ l2
(clausify_false
  (contra _ (impl_elim _ _ truth (iff_elim_2 _ _ (and_elim_1 _ _ (impl_elim _ _ f3 bf3)))) l2)
))) (\ C6


(satlem_simplify _ _ _ 
(R _ _ (R _ _ C6 C2 v2) C3 v1) (\ x x))

)))))))))))))))))))))))))))))))))))))))))))