Let $A$, $B$, $C$ and $D$ be finite sets of integers. In addition, we have a supply of Boolean variables $a$ and $b$ with two subscripts. Then, let us define
$$Z(m) = \bigvee_{i \in A} ( a_{i,m-1} \wedge \bigwedge_{(i,j) \in B \times B} (\bigvee_{m' \in C} a_{j,m'} \vee \bigvee_{m' \in D} b_{j,m'} ) ).$$
I want to express $Z(m)$ in conjunctive normal form (CNF), i.e., as an AND of ORs. The Wikipedia description of the process looks overly general for me to digest, but as a start, there are no implications or NOTs to get rid of. But now, especially getting rid of the very first "big OR" that ranges over $A$ looks difficult.
As you can maybe guess, my original $Z(m)$ is a bit more complicated, but I've tried to distill it into a case that is much simpler yet I can't solve it. How do I convert $Z(m)$ to CNF?