5-3-tableau.dot (888B)
1 graph g { 2 a [label="* (¬ ◇ ¬ p ∧ ◇ ¬ q), ¬ ◇ (p ∧ ¬ q)", xlabel="1"] 3 b [label="◇ (p ∧ ¬ q) * ¬ ◇ ¬ p ∧ ◇ ¬ q", xlabel="1"]; a -- b 4 5 la [label="◇ (p ∧ ¬ q) * ¬ ◇ ¬ p", xlabel="1"]; a -- la 6 lb [label="◇ (p ∧ ¬ q), ◇ ¬ p *", xlabel="1"]; la -- lb 7 8 lla [label="p ∧ ¬ q *", xlabel="2"]; lb -- lla [style="dashed"] 9 llb [label="p, ¬ q *", xlabel="2"]; lla -- llb 10 llc [label="{p * q | does not close}", xlabel="2", shape="record"]; llb -- llc 11 12 lra [label="{¬ p * | does not close}", xlabel="3", shape="record"]; lb -- lra [style="dashed"] 13 14 ra [label="◇ (p ∧ ¬ q) * ◇ ¬ q", xlabel="1"]; b -- ra 15 rb [label="p ∧ ¬ q * ¬ q", xlabel="4"]; ra -- rb [style="dashed"] 16 rc [label="p ∧ ¬ q, q *", xlabel="4"]; rb -- rc 17 rd [label="p, ¬ q, q *", xlabel="4"]; rc -- rd 18 re [label="{p, q * q | closes}", xlabel="4", shape="record"]; rd -- re 19 } 20