f('u_7_5', (  all X1: all T1: ( s(X1, T1) => r(X1, T1), b(X1, T1) ) ,  all X2:  all T2: ( s(X2, T2) =>  ex T3: ( ~r(X2, T3) <=> f(X2, T2) ) ), f(c, d) =>  ex Z: ~s(c, Z)  ) ).