1% 2% Combinatory Logic. 3% Find a fixed point combinator in the fragment {B, W, S}. 4% UR-resolution. 5% 6 7set(ur_res). 8clear(print_kept). 9set(bird_print). % Output (but not input) in combinatory logic notation. 10assign(fpa_literals, 3). % to save memory 11 12 13list(usable). 14 15x = x. 16x != y | y = x. 17x != y | y != z | x = z. 18x != y | a(x,z) = a(y,z). 19x != y | a(z,x) = a(z,y). 20 21a(a(a(B,x),y),z) = a(x,a(y,z)). 22a(a(W,x),y) = a(a(x,y),y). 23a(a(a(S,x),y),z) = a(a(x,z),a(y,z)). 24 25end_of_list. 26 27% Deny the existence of a fixed point combinator. 28% If a refutation is found, $Ans contains a fixed point combinator. 29 30formula_list(sos). 31-(exists y all x (a(y,x) = a(x,a(y,x)) & -$Ans(y))). 32end_of_list. 33 34list(demodulators). 35a(a(a(B,x),y),z) = a(x,a(y,z)). 36end_of_list. 37 38