formula_list(usable). % Dedekind's law:

( all x y z v w ( i(n(w,k(n(y,z),v)),n(w,u(k(n(y,z),n(v,x)),k(y,n(v,c(x)))))) )).

( all y v w ( i(n(k(y,v),w),k(n(y,k(w,r(v))),n(v,k(r(y),w)))) )). % !!

( all y v w ( i(n(k(y,v),w),k(y,n(v,k(r(y),w)))) )). % (xv)_1

end_of_list.