A(x) => H(x)
D(x,y) => ~H(y)
B(x,y) ^ C(x,y) => A(x)