%
% This is the Wang exq1 problem
%

set(auto).

list(usable).
y=m | p(y,m) | v1=m | v1=y | -p(y,v1) | -p(v1,y).
y=b | -p(y,b) | v=b | v=y | -p(y,v) | -p(v,y).
y=k | y=m | y=b | -p(y,k).
y=m | -p(y,m) | f(y)!=m.
y=m | -p(y,m) | f(y)!=y.
y=m | -p(y,m) | p(y,f(y)).
y=m | -p(y,m) | p(f(y),y).
y=b | p(y,b) | g(y)!=b.
y=b | p(y,b) | g(y)!=y.
y=b | p(y,b) | p(y,g(y)).
y=b | p(y,b) | p(g(y),y).
y=k | y!=m | p(y,k).
y=k | y!=b | p(y,k).
x=x.
x!=y | y=x.
x!=y | y!=z | x=z.
x!=y | -p(x,z) | p(y,z).
x!=y | -p(z,x) | p(z,y).
x!=y | f(x)=f(y).
x!=y | g(x)=g(y).


m!=b.
b!=k.
k!=m.
end_of_list.