formula_list(usable).

(	all x y z ( i(x,y) -> i(k(x,z),k(y,z)) )). % (vii)_1

(	all x y z ( i(x,y) -> i(k(z,x),k(z,y)) )). % (vii)_2

(	all x y z ( i(x,y) -> i(d(x,z),d(y,z)) )). % (vii)_3

(	all x y z ( i(x,y) -> i(d(z,x),d(z,y)) )). % (vii)_4

(	all x y ( i(x,y) -> i(r(x),r(y)) )).       % (vii)_5

end_of_list.