assign(max_seconds, 30).

%
%  Combinatory Logic
%  Construct W in terms of S and K.  Wxy = xyy.
%

formulas(sos).

  a(a(a(S,x),y),z) = a(a(x,z),a(y,z)) # label(S).
  a(a(K,x),y) = x # label(K).

end_of_list.

% Don't set(restrict_denials), because the easy proofs
% paramodulate into the denial.

formulas(goals).

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

end_of_list.