Let a⪯b⪯c⪯da⪯b⪯c⪯d be the variable ordering.

ϕ= a&!b&!c&!d|b&!a&!c&!d|c&d|c&!d|d&!a&!c

X={c,d} is the set of quantified variables. Compute the ROBDD of the existential quantification formula ∃X..¬ϕ using the Exists algorithm, and convert the result to Shannon normal form.

How to calculate ¬ϕ?

Is it using the truth table? do we take the DNF?