# translation of first-order logic to combinatory logic

I am new to combinatory logic, and I am interested in its relationship to first-order logic. In particular, I am wondering if there is a universal translation of first-order logic to combinatory logic with the usual combinators S, K, B, C, I, together with Schonkinfel's combinator U (which stands for disjoint class: UPQ=$\neg\exists x(Px\wedge Qx)$). For instance, given a sentence $\forall y\exists x(Ny\supset (Px\wedge Gxy))$, its translation in CL is $UN\mathrm{B}(UP)(\mathrm{C}G)$ (this example is taken from https://plato.stanford.edu/entries/logic-combinatory/). Is there a universal procedure for translating first-order formulas (and is there a way of translating combinators into first-order formulas)? On this note, I am also curious if the combinator U can be defined in terms of S and K.