Add ~ rexanuz2nf counterexample and related theorems demonstrating necessity of disjoint variable constraints in ~ rexanuz2

Add ~ rexanuz2nf counterexample and related theorems demonstrating necessity of disjoint variable constraints in ~ rexanuz2 #9122