formulas(sos).

% combinator B

 a(a(a(B,x),y),z) = a(x,a(y,z)) # label(B).

% combinator W

 a(a(W,x),y) = a(a(x,y),y) # label(W).

end_of_list.

formulas(sos).

% denial of the existence of a fixed point combinator

a(y,f(y)) != a(f(y),a(y,f(y))) # answer(y).

end_of_list.