formulas(sos).
	a(x,x)=x.
	a(x,y)=a(y,x).
	a(x,a(y,z))=a(a(x,y),z).
end_of_list.

formulas(goals).
	all p all q (a(p,a(q,a(p,a(q,a(p,a(q,p))))))=a(p,q)).
end_of_list.