S4 Formula Infinite Loop Bug

[hebozhe]

Infinitely regresses: □(□(□A → □(□B ∨ □C)) ↔ □(□(□A → □B) ∨ □(□A → □C)))

Proves Invalid: □(□(□A → □(□B ∨ □C)) → □(□(□A → □B) ∨ □(□A → □C)))

Proves Valid: □(□(□(□A → □B) ∨ □(□A → □C)) → □(□A → □(□B ∨ □C)))

For ease of reading, the subformulae are □(□(□A → □B) ∨ □(□A → □C)) and □(□A → □(□B ∨ □C)).

This is the Gratz translation of intuitionistic formulae, hence all of the squares.

[wo]

Thanks. I'm very busy this week. Can I just double-check: the formula is S4-invalid, but you think the prover is stuck in a loop trying to realize this (when 'reflexive' and 'transitive' are checked)? I suspect it's not actually stuck in a loop, it's just that the modelfinder is painfully slow for non-trivial modal formulas.

[hebozhe]

It appears never to stop, though I only factored the time relative to the time it took to find the countermodel in invalid conditional. If anything, it's space for an optimization.