I have two Presburger formulas A and B such that A∧B≡False. From these I need to find "simpler" formula A′ (as simple as I can make it) such that A→A′ and A′∧B≡False. Is there any simple way to automate this for largish formulas in Mathematica? The formulas start off in sum of products form, with thousands of products and less than 20 variables. I'm already using FullSimplify to simplify A and B preserving equivalence, but I need to go even simpler, hence this weaker set of conditions.