Feature request, timing in milliseconds

[Jean-Luc-Picard-2021]

Hi,

I am quite amazed by your tool, since it not only searches a proof, it also tries to find a counter model at the same time.

I am currently experimenting with a prover on my own, and the best I get in Chrome browser is:

?- prove0('∀p∀q(∀x(x∈p⇔x∈q)⇒p=q) ∧ ∀x(x∈u⇔r(x)) ∧ ∀x(x∈v⇔r(x)) ⇒ u=v', 5, time), !. % Wall 1601 ms, gc 5 ms, 1928801 lips

Would it be possible to show timings in your prover as well. Maybe through some debug option, like opening the tree tool with ?debug=true.

Bye