formula_list(usable).

        ( all x y ( n(x,y) = n(y,x) )). % 20

        ( all x y ( (n(x,c(y)) = Z) -> (u(x,y) = y) )). % 21a

        ( all x y ( (u(x,y) = y) -> (n(x,c(y)) = Z) )). % 21b

        ( all x y ( (n(x,y) = Z & u(x,y) = U) -> (c(x) = y) )). % 22

        ( all x y ( (c(x) = y) -> (n(x,y) = Z) )). % 23

        ( all x y ( (c(x) = y) -> (u(x,y) = U) )). % 24

end_of_list.