Remove Automatic Evaluation

- [X] Stop auto eval for Xor
- [X] Stop auto eval for ITE
- [x] Stop auto eval for Not
- [X] to_nnf
- [x] is_nnf
- [X] is_literal for predicates
- [x] Tests
- [x] Documentation
Don't confuse `Atom` (the class) with logical atom. 

We should think about what we really want to be a logical atom. For instance, should `Q.positive(x)` be a logical atom (or `Eq(x, y)`)? I think so, as otherwise something like `Q.positive(x) | Q.negative(x)` would not be in CNF, depending on how we define CNF.