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.