formula_list(usable).
	all x y z ( k(x,k(y,z)) = k(k(x,y),z) ).	 % BIV
%	all x y z ( k(u(x,y),z) = u(k(x,z),k(y,z)) ).	 % BV
%	all x ( k(x,I) = x ).	 			 % BVI
	all x ( r(r(x)) = x ).	 			 % BVII
	all x y ( r(u(x,y)) = u(r(x),r(y)) ).	 	 % BVIII
	all x y ( r(k(x,y)) = k(r(y),r(x)) ).	 	 % BIX
%	all x y ( u(k(r(x),c(k(x,y))),c(y)) = c(y) ).	 % BX
end_of_list.