Consider the following premises. R(a_12) -> q_6. ~q_6. p <-> S(a_12). forall z: S(z) <-> R(z). Can we infer p from them?
 From forall z: S(z) <-> R(z) we can infer S(a_12) <-> R(a_12). From R(a_12) -> q_6, ~q_6 we can infer ~R(a_12). From S(a_12) <-> R(a_12), ~R(a_12) we can infer ~S(a_12). Finally, from p <-> S(a_12), ~S(a_12) we can infer ~p, which contradicts p. Therefore, the answer is no.