checkers fails to backtrack to correct branch

[shaolintl]

Using ELPI in the gandalf2017 branch, when running:
./prover-elpi.sh modtab-min-1

we get the following attached files
min.txt
max.txt

The problem is that in max.txt we store lind (lind eind) and decide on it
In min.txt we store lind (lind X) but we never decide on something of the form lind (lind _) instead, we keep trying the same ones over and over again:

+++ dec inCtxt (lind (rind (lind X0))) (p (q1 x5))
+++ dec inCtxt relind (n (rel zero x5))
+++ dec inCtxt (rind (lind X0)) (d+ (all x6 \ n (rel zero x6) !-! p (q1 x6)))

[shaolintl]

the text in the file shows only storing and deciding. I removed the rest

[shaolintl]

Same problem also with Teyjus, see attached files. So the problem is in our program. Maybe we should introduce some cuts.
max2.txt
min2.txt

[shaolintl]

I think I have found the problem. It seems to be related to the fact that we dont place a decide bound when we dont use a decision tree. The result is that some decides, such as on forall, are happening infinitely often. The solution is to place a decide bound on at least the forall, and probably on all formulas. The number might be that we can use the diamond box relation to see how many times we might need to decide?

[emmevolpe]

Yes. I think we can set a bound related to the formula to prove.
Why is the \forall worse than the other operators?

[shaolintl]

I am not sure if it is worse. The decide entered a loop when it encountered the forall. Instead of failing on the branch, it just decided again. It didnt happen for the other decided formulas.

[shaolintl]

@emmevolpe What do you think should be the decide depth? One for all formulas except exists which we determine according to the diamond-box relation in the certificate?

[shaolintl]

@emmevolpe waiting for your reply for the above. Right now, the value is fixed to 2 for all nodes which is enough for the example. The example is running through now with a variable for the decide tree.