Either optimise the decision procedure (it leaves a lot of duplicates or tautologies) ; or only call it on simplified environments and formulas. Might help solve #33 #38 #39.