Smart ep=RSTC skips congruences for introduced symbols for which it shouldn't?

[quickbeam123]

We saturate (and think we are complete) on the following unsat problem via:

./vampire_dbg_master_6968 --decode dis+21_1:10_rp=on:ep=RSTC:ins=1_0 Problems/REL/REL022+2.p -p off
% Running in auto input_syntax mode. Trying TPTP
% SZS status CounterSatisfiable for REL022+2
% # SZS output start Saturation.
% # SZS output end Saturation.
Condition in file Shell/UIHelper.cpp, line 486 violated:
!s_expecting_unsat
----- stack dump -----
Version : Vampire 4.8 (commit ef21e58 on 2023-12-01 08:47:07 +0000)
_start
__libc_start_main
???
main
vampireMode()
Shell::UIHelper::outputResult(std::ostream&)
Debug::Assertion::violated(char const, int, char const)
Debug::Tracer::printStack(std::ostream&)
----- end of stack dump -----

Maybe we are saving too much on the congruence axioms in equality_proxy? Maybe inequality splitting does not mark its new symbol properly? Could this also happen with e.g. GeneralSplitting? How to prevent this from happening in the future when an uninitiated person introduced a new symbol?

[easychair]

The safest way is to add a check on symbol introduction and maybe use an extra bit on symbols to mark that equality proxy was applied. This will guarantee that EP was applied to all symbols and only once. It will also guarantee that the glitch will not happen thanks to a future generation of developers. A

…

On Fri, 8 Dec 2023 at 09:25, Martin Suda ***@***.***> wrote: We saturate (and think we are complete) on the following unsat problem via: ./vampire_dbg_master_6968 --decode dis+21_1:10_rp=on:ep=RSTC:ins=1_0 Problems/REL/REL022+2.p -p off % Running in auto input_syntax mode. Trying TPTP % SZS status CounterSatisfiable for REL022+2 % # SZS output start Saturation. % # SZS output end Saturation. Condition in file Shell/UIHelper.cpp, line 486 violated: !s_expecting_unsat ----- stack dump ----- Version : Vampire 4.8 (commit ef21e58 <ef21e58> on 2023-12-01 08:47:07 +0000) _start __libc_start_main ??? main vampireMode() Shell::UIHelper::outputResult(std::ostream&) Debug::Assertion::violated(char const, int, char const) Debug::Tracer::printStack(std::ostream&) ----- end of stack dump ----- Maybe we are saving too much on the congruence axioms in equality_proxy? Maybe inequality splitting does not mark its new symbol properly? Could this also happen with e.g. GeneralSplitting? How to prevent this from happening in the future when an uninitiated person introduced a new symbol? — Reply to this email directly, view it on GitHub <#509>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABVY4BI7XKBULMUBZHWXSELYILMIHAVCNFSM6AAAAABAML2RMGVHI2DSMVQWIX3LMV43ASLTON2WKOZSGAZTEMRZGU4DCMQ> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[MichaelRawson]

Bug is that inequality splitting marks its symbol (indirectly, which is why I didn't catch it) as naming a formula - which I guess it kinda does. Agree with @easychair that explicitly marking a symbol as safe to skip for equality proxy congruence is the way to go, patch incoming.