[Rules] Add well-formness conditions relating to `NOT`

[afs]

A variables that does not appear to the left of NOT (i.e first appears in NOT) should not be allowed to the right of NOT.

Such a variable is not bound in a solution resulting from the NOT.

(It could be allowed if such variables are treated as different, i.e. the same name but a different variable due to scoping.)