Consider the following premises. forall y_1: Q(y_1) <-> R(y_1). R(j_4) <-> R_12(h). forall x_12: ~R_12(x_12). Can we infer Q(j_4) from them?
 From forall x_12: ~R_12(x_12) we can infer ~R_12(h). From forall y_1: Q(y_1) <-> R(y_1) we can infer Q(j_4) <-> R(j_4). From R(j_4) <-> R_12(h), ~R_12(h) we can infer ~R(j_4). Finally, from Q(j_4) <-> R(j_4), ~R(j_4) we can infer ~Q(j_4), which contradicts Q(j_4). Therefore, the answer is no.