Write G for the clauses not selected around H. Child A is G AND H, where H is one disjunctive clause: at least one literal of H is true. Child B is G AND all petals P_a AND the unit clauses NOT l for every l in H: all literals of H are false. Every satisfying parent assignment enters exactly one child. Normalize both children without removing declared variables. For example, (x OR y) AND (x OR z) branches into (x), with four assignments on x,y,z, and (NOT x) AND (y) AND (z), with one. Their sum five equals the original count. Omitting NOT x from child B would double-count assignments.