Description of the issue
Goeland finds a proof from the attached file without using equality when it is countersat.
Flags used
-dmt
Small problem file to reproduce the bug
- NLP002+1.p from TPTP
- NLP003+1.p from TPTP (not sure whether it's the same problem or not, use -presko to have the proof faster)
Version of Goéland where the issue occurs
master
Preliminary investigations
After some investigations from what I can get from the Rocq proof: it seems to come from the substitutions. Either some of them are dropped and it makes it possible to return that children have unifiable substitutions when they don't, either some variables are wrongly unified. It might be possible to minimize the input files to get a clear look at the bug but I'm not sure about that.
Description of the issue
Goeland finds a proof from the attached file without using equality when it is countersat.
Flags used
-dmt
Small problem file to reproduce the bug
Version of Goéland where the issue occurs
master
Preliminary investigations
After some investigations from what I can get from the Rocq proof: it seems to come from the substitutions. Either some of them are dropped and it makes it possible to return that children have unifiable substitutions when they don't, either some variables are wrongly unified. It might be possible to minimize the input files to get a clear look at the bug but I'm not sure about that.