Propagation of satisfiability and unsatisfiability does not cover disjunctions and I don't get how propagation works, so I won't touch it yet. So this reverts the only partially implemented Disjunctive ruleEnumerations,
