Does the tree tool search shortest proofs?

[Jean-Luc-Picard-2021]

What is the search strategy for proofs? Some iterative deepening. Here is a funny example, where I find a shorter regular proof for FOL with equality, its a validation

proof, not a refutation falsification, so opposite formula signs:

On the other hand the tree tools does one more LL:

https://www.umsu.de/trees/#~6x~6y~6z~6tp%28x,y,z,t%29=p%28y,z,t,x%29~5p%28a,b,c,d%29=p%28c,d,a,b%29

[wo]

Yes, the internal proof search uses iterative deepening, but it doesn't try out all possible proofs of a given size, as that would take prohibitively long. When a proof is found, I try to strip any redundant elements, but the result isn't always the simplest possible proof. The equality reasoner seems to have a preference for closing trees with formulas of the type ~(t=t). I might look into whether this can be changed, but it's not a priority.

[Jean-Luc-Picard-2021]

Ok, I see, it closes with (refl) and not with (ax). In my prover I have ✓, but recently I also wrote whether its (ax) or (refl). Interesting, the different outcome. I am searching first for (ax),

and the for (refl), but neither go into the budget of iterative depening. But (subst) does so, although I have only one counter, and not multiple counters or some such refinement.

BTW: I didn't post some link to make my example reproducible so far, since I was shy, I had only a prover that needed quite some time. But now there is a new prover. It doesn't require

a regular proof. So the (subst) rule now appears earlier:

?- time(prove0('∀x∀y∀z∀t f(x,y,z,t)=f(y,z,t,x)⇒\
f(a,b,c,d)=f(c,d,a,b)', 9, unicode)), !.
1. ∀x ∀y ∀z ∀t f(x, y, z, t) = f(y, z, t, x) ⇒ f(a, b, c, d) = f(c, d, a, b)
2. f(a, b, c, d) = f(c, d, a, b)   (T⇒2 1)
3. ¬∀x ∀y ∀z ∀t f(x, y, z, t) = f(y, z, t, x)   (T⇒1 1)
4. ¬∀y ∀z ∀t f(a, y, z, t) = f(y, z, t, a)   (F∀ 3)
5. ¬∀z ∀t f(a, b, z, t) = f(b, z, t, a)   (F∀ 4)
6. ¬∀t f(a, b, c, t) = f(b, c, t, a)   (F∀ 5)
7. ¬f(a, b, c, d) = f(b, c, d, a)   (F∀ 6)
8. f(b, c, d, a) = f(c, d, a, b)   (F= 2, 7)
9. ¬∀y ∀z ∀t f(b, y, z, t) = f(y, z, t, b)   (F∀ 3)
10. ¬∀z ∀t f(b, c, z, t) = f(c, z, t, b)   (F∀ 9)
11. ¬∀t f(b, c, d, t) = f(c, d, t, b)   (F∀ 10)
12. ¬f(b, c, d, a) = f(c, d, a, b)   (F∀ 11)
   ✓   (ax 12, 8)
% Wall 49 ms, gc 0 ms, 1433877 lips

And it takes only ca 50 ms, but I guess we can even do better.