I'd expect a SMT (Satisfiability modulo theory) solver like z3 to work better for this use case, might be worth giving it a try. E.g.

  x = z3.BitVec('x', 32)
  y = z3.BitVec('y', 32)
  i1 = x | y
  i2 = ~(~x | ~y)
  s = z3.Solver()
  s.add(i1 != i2)
  if s.check() == z3.sat:
      print "found counterexample"
      print s.model()
  else:
      print "always equal"