Yes, I did evaluate an algorithmic approach similar to the grandparent's approach, although was thinking about it in terms of ruleset normalization (which I thi

Yes, I did evaluate an algorithmic approach similar to the grandparent's approach, although was thinking about it in terms of ruleset normalization (which I think is equivalent to the the algorithm described). I even put a good amount of effort into specifying the algorithm in TLA+! However, the SMT approach really was significantly easier. It also had wonderful second-order effects because learning how to effectively use SMT solvers has been very valuable for my career.