I’m not an expert here, but it sounds like you’re forcing a first-order logic problem into a propositional logic box. A “native” first-order logic solver like

I’m not an expert here, but it sounds like you’re forcing a first-order logic problem into a propositional logic box. A “native” first-order logic solver like Z3 might be something to try.