1:(input ((not #1:(= a a))))
2:(bbvar (#2:(bbT a [#7:(bitof 0 a) #8:(bitof 1 a)])))
3:(bbeq (#3:(= #1 #4:(and #5:(= #7 #7) #6:(= #8 #8)))) 2 2)
4:(equiv2 (#1 (not #4)) 3)
5:(resolution ((not #4)) 1 4)
6:(not_and ((not #5) (not #6)) 5)
7:(equiv_neg1 (#5 (not #7)))
8:(equiv_neg2 (#5 #7))
9:(resolution ((not #6)) 7 8 6)
10:(equiv_neg1 (#6 (not #8)))
11:(equiv_neg2 (#6 #8))
12:(resolution () 10 11 9)