formula_list(usable). ( all x (n(x,x) = x )). % 28 end_of_list.