There is a bug in the tree pruning function.

[billvanyo]

The following exercise is from Raymond Smullyan's book First-Order Logic

         ((∀x)((F(x) ∧ G(x)) ⊃ H(x)) ⊃ (∃x)(F(x) ∧ ¬G(x))) 1=premise
               ((∀x)(F(x) ⊃ G(x)) ∨ (∀x)(F(x) ⊃ H(x))) 2=premise
      ¬((∀x)((F(x) ∧ H(x)) ⊃ G(x)) ⊃ (∃x)((F(x) ∧ G(x)) ∧ ¬H(x))) 3=¬goal

For reference, a proof can be generated here:
https://www.umsu.de/trees/#((((%E2%88%80x((Fx%E2%88%A7Gx)%E2%86%92Hx))%E2%86%92(%E2%88%83x(Fx%E2%88%A7%C2%ACGx)))%E2%88%A7((%E2%88%80x(Fx%E2%86%92Gx))%E2%88%A8(%E2%88%80x(Fx%E2%86%92Hx))))%E2%86%92((%E2%88%80x((Fx%E2%88%A7Hx)%E2%86%92Gx))%E2%86%92(%E2%88%83x((Fx%E2%88%A7Gx)%E2%88%A7%C2%ACHx))))

With the Clojure code, this can be proved with:

(def fmla1 '((forall x (((F x) and (G x)) imp (H x))) imp (exists x ((F x) and (not (G x))))))
(def fmla2 '((forall x ((F x) imp (G x))) or (forall x ((F x) imp (H x)))))
(def fmla3 '((forall x (((F x) and (H x)) imp (G x))) imp (exists x (((F x) and (G x)) and (not (H x))))))
(def tabrs (init-tableau (list fmla1 fmla2) fmla3))
(attempt-proof tabrs 252)

It finds the proof, but too much gets removed during pruning.
To see the unpruned proof, I added the following to attempt-proof right after (print-tree printable-tree):

(spit "tree.txt" (with-out-str (print-tree (convert-tree-map (:tree-map tableau) (:subst closing-subst)))))

The resulting file (the unpruned proof) is attached: tree.txt

The pruned tree is printing as:

          ((∀x)((F(x) ∧ G(x)) ⊃ H(x)) ⊃ (∃x)(F(x) ∧ ¬G(x))) 1=premise
               ((∀x)(F(x) ⊃ G(x)) ∨ (∀x)(F(x) ⊃ H(x))) 2=premise
      ¬((∀x)((F(x) ∧ H(x)) ⊃ G(x)) ⊃ (∃x)((F(x) ∧ G(x)) ∧ ¬H(x))) 3=¬goal
                       (∀X)((F(x) ∧ H(x)) ⊃ G(x)) 4=α₁.3
                      ¬(∃x)((F(x) ∧ G(x)) ∧ ¬H(x)) 5=α₂.3
                        ((F(X₄) ∧ H(X₄)) ⊃ G(X₄)) 6=γ.4
                       ¬((F(X₃) ∧ G(X₃)) ∧ ¬H(X₃)) 7=γ.5
                 ┌─────────────────────┴─────────────────────┐
 ¬(∀x)((F(x) ∧ G(x)) ⊃ H(x)) 8=β₁.1              (∃x)(F(x) ∧ ¬G(x)) 9=β₂.1
 ¬((F(X₃) ∧ G(X₃)) ⊃ H(X₃)) 10=δ.8                (F(X₄) ∧ ¬G(X₄)) 11=δ.9
      (F(X₃) ∧ G(X₃)) 12=α₁.10                         F(X₄) 14=α₁.11
          ¬H(X₃) 13=α₂.10                             ¬G(X₄) 15=α₂.11
           F(X₃) 16=α₁.12                     ┌──────────────┴──────────────┐
           G(X₃) 17=α₂.12         (∀x)(F(x) ⊃ G(x)) 18=β₁.2     (∀x)(F(x) ⊃ H(x)) 19=β₂.2
     (∀x)(F(x) ⊃ H(x)) 23=β₂.2     (F(X₄) ⊃ G(X₄)) 20=γ.18       (F(X₄) ⊃ H(X₄)) 21=γ.19
      (F(X₃) ⊃ H(X₃)) 29=γ.23                                   ┌───────────┴───────────┐
                                                     ¬(F(X₄) ∧ H(X₄)) 26=β₁.6     G(X₄) 27=β₂.6