formula_list(usable). % siblings of Schroeder's cycle law

( all x y z ( n(y,k(x,n(z,c(k(r(x),y)))))=Z )).

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

( all x y z ( n(y,k(n(x,c(k(y,r(z)))),z)) = Z )).

end_of_list.