formula_list(usable). % conversion laws
(	all x y ( i(x,y) -> i(r(x),r(y)) )).    % (i)_0
(	all x y ( r(u(x,y)) = u(r(x),r(y)) )).	% (i)_1 == BVIII
(	all x ( r(c(x)) = c(r(x)) ) ).		% (i)_3
(	all x y ( r(n(x,y)) = n(r(x),r(y)) )).  % (i)_2
(	all x ( r(r(x))=x )).                   % (i)_4 == BVII
(	all x y ( r(d(x,y)) = d(r(y),r(x))) ).  % (i)_5
(	all x y ( r(k(x,y)) = k(r(y),r(x))) ).  % (i)_6 == BIX
(	r(I)=I ). % (i)_7a
(	r(Z)=Z ). % (i)_7b
(	r(U)=U ). % (i)_7c
end_of_list.