The provability check detects that ⊢ ?!⊥ is not provable thus turning turnstile into red.
Double-click on turnstile runs the automated prover which diverges and concludes "do not know" thus turning turnstile to gray.
The automated prover should not be called when the sequent is already checked as not provable.
The provability check detects that
⊢ ?!⊥is not provable thus turning turnstile into red. Double-click on turnstile runs the automated prover which diverges and concludes "do not know" thus turning turnstile to gray. The automated prover should not be called when the sequent is already checked as not provable.