Description: axextb with distinctors instead of distinct variable restrictions. (Contributed by Scott Fenton, 13-Dec-2010)