Open Jean-Luc-Picard-2021 opened 4 months ago
The problem occurs in the equality reasoner. The script doesn't seem to be stuck in a loop, but it's exploring too many possibilities, considering deeply nested terms like "[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,[m,[i,ξ4],ξ4],[m,ξ2,ξ3]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]"
.
Need to investigate.
Its a quite difficult problem when attacked brute force. And maybe what you show is a large Skolem term?
You find some timing mesurements here, by a method that works without Skolemization, just as McCune's Mace4 does. The method is without Skolemization and also
without caching, basically a classical DPLL variant, i.e. heavy backtracking which doesn't use much space, only much time:
does this terminate, i.e. model finder https://github.com/trealla-prolog/trealla/issues/533
Ciao Prolog does it in about 4 minutes. McCune himself does it in less than 1 second, according to the Mace4 PDF. Mace4 applies some cell selection
ordering and some symmetry breaking heuristics,
making it not really brute force. Unfortunately I
could not yet replicate these heuristics in Prolog.
I am trying the McCune group example, and I noticed a browser freeze:
Its usually freezing here:
The problem link is:
https://www.umsu.de/trees/#(~6X(m(0,X)=X)~1~6X(m(i(X),X)=0)~1~6X~6Y~6Z(m(m(X,Y),Z)=m(X,m(Y,Z))))~5(m(a,b)=m(b,a))