set(auto).

list(usable).
x = x.
p(p(f1(x),x,f2(y)),y,p(z,u,p(z,v,v)))=z.
p(B,B,A) != A | p(A,B,B) != A | p(A,B,A) != A | f1(A) != A | f2(A) != A.
end_of_list.