fof(barber,conjecture, ?[X]: ![Y]: (~ s(Y,Y) => s(X,Y)) => ?[Z]: s(Z,Z) ).