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.