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.