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