Instantiation based reasoning for Effectively Propositional Reasoning has been unreasonably effective to classify decidable fragments for pointer manipulating programs and network protocols. Nevertheless, even transitive binary relations pose obstacles to scalability. As a special birthday feature for Mooly, I introduce native support in Z3 for a class of special relations, that capture several classes of binary relations with space-and-time efficient decision procedures.