 This formula is equivalent to \(\forall y(Ny\supset\exists x(Px\land Gxy))\) and further to \(\lnot\exists y\lnot(Ny\supset\exists x(Px\land Gxy))\).  In one or two more steps, we get \(Ny\mid^y(Px\mid^xGxy)\).  (Expressions are considered to be grouped to the left unless parentheses indicate otherwise. E.g., \(Gxy\) is \(((Gx)y)\) not \(G(xy)\) as could have been, perhaps, expected based on the most common way of arranging parentheses in FOL formulas.) Unfortunately, neither \(\mid^x\) nor \(\mid^y\) can be replaced by \(U\) in the last expression. However, if the arguments of \(G\) were permuted then the former reduction could be carried out. One of the combinators, \(\textsf{C}\) does exactly what is needed: \(Gxy\) can be changed to \(\textsf{C}Gyx\) (see the definition of combinators in section 2.1). That is, we have \(Ny\mid^y(Px\mid^x\textsf{C}Gyx)\), and then \(Ny\mid^yUP (\textsf{C}Gy)\).[4]  The expression may give the impression that \(y\) is the last component of \(UP(\textsf{C}Gy)\), which is the second argument of \(\mid^y\), but it  is not so. The grouping within expressions cannot be disregarded, and another combinator, \(\textsf{B}\) is needed to turn \(UP(\textsf{C}Gy)\) into the desired form \(\textsf{B}(UP)(\textsf{C}G)y\).  From \(Ny\mid^y\textsf{B}(UP)(\textsf{C}G)y\), we get \(UN(\textsf{B}(UP) (\textsf{C}G))\) in one more step. This expression is completely free of variables, and it also makes the renaming of bound variables in FOL easily comprehensible: given two sequences of (distinct) variables that are different in their first two elements, the reversal of the above process yields formulas that are (logically equivalent) alphabetic variants of the formula in (#2).