DMOR is constructed by turning the formula of De Morgan, which relates to the predicate logic, into inference rules.
Example 1 a1 : not (All x) (f(x)) by ... ;
Example 2 a1 : not (Exist x) (All y) (Exist z) (f(x,y,z)) by .... ;
Example 3 a1 : (Exist x) (not f(x)) by ... ;
Thus, when writing not f(x) in each example, f(x) should not be limited to the function form and any formulas will be acceptable if they do not confuse the operating order (<factor>) by putting not. For instance, [a=b], (All u), (g(u,x)), and not A(x) are acceptable.
Furthermore, the rule DMOR is not necessary because, for example, example 1 above can be substituted by a combination of other rules such as the ones below.
a7 : f(x) by LOGIC (a6) ;
imp False by LOGIC(a1, a5) ;
Therefore, a8 corresponds with a2 of example 1.