We consider the problem of rationalizing choice data by a preference satisfying an arbitrary collection of invariance axioms. Examples of such axioms include quasilinearity, homotheticity, independence-type axioms for mixture spaces, constant relative/absolute risk and ambiguity aversion axioms, stationarity for dated rewards or consumption streams, separability, and many others. We provide necessary and sufficient conditions for invariant rationalizability via a novel approach which relies on tools from the theoretical computer science literature on automated theorem proving. We also establish a generalization of the Dushnik-Miller theorem, which we use to give a complete description of the out-of-sample predictions generated by the data under any such collection of axioms.