formula_list(usable). ( all x y ( i(k(r(n(x,d(c(x),I))),y),k(r(x),y)) )). end_of_list.