The formula (∀x∀y(Rxy→x=y) ∧ ∀x∀y(Rxy↔Ryx) ∧ ∀x∀y∀z(Rxy→Ryz→Rxz)) → ∀x∀y(Rxy→∃z(Rzx∧∃y(Ryz∧Py))→Py) fails to ever validate: it runs well past 10k steps and model size 40 without coming up with an answer. However, rewriting it as (∀x∀y(Rxy↔Ryx) ∧ ∀x∀y∀z(Rxy→Ryz→Rxz) ∧ ∀x∀y(Rxy→x=y)) → ∀x∀y(Rxy→∃z(Rzx∧∃y(Ryz∧Py))→Py) (with the antecedent ∀x∀y(Rxy→x=y) moved to the end) causes it to quickly validate in 42 steps. I'm not sure if this discrepancy comes from some fundamental weakness of the tableau method (an exponential blowup?), or if there's some particular issue with the implementation.