formula_list(usable). % (inclusion appears in disguise) ( all x y z ( u(x,y) = y -> u(k(z,x),k(z,y)) = k(z,y) )). ( all x y z ( u(x,y) = y -> u(c(u(z,y)),c(x)) = c(x) )). ( all x y z ( u(x,y) = y -> u(k(x,z),k(y,z)) = k(y,z) )). end_of_list.