Hello, Thank you for the thorough documentation on the various theories and logics. I'm wondering if anyone can recommend 'supplementary documentation' that summarizes the computational complexity of the various predominant logics (such as QF_UFLIA) as defined in the standard. All best wishes, Alex