Add disjunctions for free variables
Disjunctions for free variables are dealt with by splitting into multiple clauses, e.g. Szymanski. These blocks could be grouped into disjunctions for the variables. For such a disjunction we generate one predicate for deadlock, trap, or flow and therefore might be able to deal with larger systems. First benchmark could be Szymanski because it feels just slightly out of reach for now.