formula_list(usable). ( k(U,U) = U ). ( ( r(U) = U ) & % (ii)_1 ( r(Z) = Z ) & % (ii)_2 ( r(I) = I ) & % (ii)_3 ( r(D) = D ) ). % (ii)_4 end_of_list.