How to below this First order logic procedure convert Convert them into Conjunctive Normal Form ?
Ɐx [[employee(x) ꓥ ¬[PST(x) ꓦ PWO(x)]] → work(x)]
I strive to do this below step ,
i. S1: Eliminate ↔
This step does not apply as there are no negations in front
ii. S2: Eliminate →
Ɐx [ [employee(x) ꓥ ¬[PST(x) ꓦ PWO(x)]] ꓦ work(x)]
iii. S3: Push negation in
Ɐx [ [employee(x) ꓥ ¬[PST(x) ꓦ PWO(x)]] ꓦ work(x)]
Step ii should read: $$\forall x [\lnot [employee(x) \land ¬[PST(x) \lor PWO(x)]] \lor work(x)]\tag{ii}$$ $$\equiv \forall x[[\lnot employee(x) \lor [PST(x) \lor PWO(x)]] \lor work(x)]\tag{DeMorgan's}$$ $$ \equiv \forall x\big(\lnot employee(x) \lor PST(x) \lor PWO(x) \lor work(x)\big)\tag{associativity}$$
Now, if $x\in\{\text{John}, \text{Julie}, \text{Jessica}\}$, we can write the above in conjunctive normal form as follows:
$$\big(\lnot employee(\text{John}) \lor PST(\text{John}) \lor PWO(\text{John}) \lor work(\text{John})\big) \\ \land \big(\lnot employee(\text{Julie}) \lor PST(\text{Julie}) \lor PWO(\text{Julie}) \lor work(\text{Julie})\big) \\ \land \big(\lnot employee(\text{Jessica}) \lor PST(\text{Jessica}) \lor PWO(\text{Jessica}) \lor work(\text{Jessica})\big)$$
If there are 211 employees, each identified with a unique ID from the set $S= \{1, 2, ..., 210, 211\}$, then we can further consolidate, into conjunctive normal form, as follows.
$\Huge{\land}$ $_{i \in S} \big(\lnot employee(i) \lor PST(i) \lor PWO(i) \lor work(i)\big)$