Step 5: T3-Rules

In this step remaining and-s are pushed upwards in the syntax tree over the or-s as much as possible. The rules are listed in Table 9. Note that n is the cardinality of the set I and atleast(n) i  is the same as the indexed and. This step can be applied more than once to force a CNF before subtrees are cut.

Rule Operator replaced by

40 x   (y z) (x y) (x z)
40a (y z)   x (y x) (z x)
41 x   atleast(n)i yi atleast(n)i (x yi)
41a atleast(n)i yi   x atleast(n)i (yi x)

Table 9: T3-Rules