Closing this because we already have improving invariant synthesis with an h2-style algorithm on the radar, and it looks like this one adds nothing new to that discussion.

(This is pie-in-the-sky stuff.)

Jörg notes that in Satellite we don't discover that "power_avail" of a satellite
and "power_on" of an instrument are mutex. The reason is that these are only
mutex because the relation that encodes which instrument is on which satellite
is mutex (i.e., every instrument is on at most one satellite).

To detect this kind of information, we could either try to extend the invariant
synthesis to take this kind of side info into account (which might be hard), do
the analysis on the grounded level (which might be inefficient, especially on
Satellite), or try out a different algorithm (such as Jussi's).