Description of the issue
When launching the attached problem, I get the error in the title of the issue. This happens pretty quickly (before increasing the reintroduction limit) and pretty often in normal mode. I always got it when using -flatten, it may be quicker to debug with that flag on.
I suspect there is a deeper problem that leads to not finding proofs for easy problems, that may be linked or not. It seems like this problem is the shortest, and it should be solved pretty fast (it's clear that it does not need to increase the limit of reintroductions at least) so further investigation is needed.
Flags used
vanilla / -flatten
Small problem file to reproduce the bug
https://tptp.org/cgi-bin/SeeTPTP?Category=Problems&Domain=SYO&File=SYO607+1.p
Version of Goéland where the issue occurs
v.1.2-dev.rc9841dae9e19c823410fa0e003a325f8ac1cd44b
Description of the issue
When launching the attached problem, I get the error in the title of the issue. This happens pretty quickly (before increasing the reintroduction limit) and pretty often in normal mode. I always got it when using
-flatten, it may be quicker to debug with that flag on.I suspect there is a deeper problem that leads to not finding proofs for easy problems, that may be linked or not. It seems like this problem is the shortest, and it should be solved pretty fast (it's clear that it does not need to increase the limit of reintroductions at least) so further investigation is needed.
Flags used
vanilla / -flatten
Small problem file to reproduce the bug
https://tptp.org/cgi-bin/SeeTPTP?Category=Problems&Domain=SYO&File=SYO607+1.p
Version of Goéland where the issue occurs
v.1.2-dev.rc9841dae9e19c823410fa0e003a325f8ac1cd44b