formula_list(usable). ( all x y ( c(k(x,y)) = d(c(x),c(y)) )). % (iii)_1 ( all x y ( c(d(x,y)) = k(c(x),c(y)) )). % (iii)_2 ( all x y ( r(k(x,y)) = k(r(y),r(x)) )). % (iii)_3 == BIX == (i)_6 ( all x y ( r(d(x,y)) = d(r(y),r(x)) )). % (iii)_4 == (i)_5 end_of_list.