formula_list(usable).

( all x ( i(k(r(x),c(x)),D) )). % (xi)_4

( all x ( i(I,d(c(x),r(x))) )). % (xi)_1

end_of_list.