Bad saturation on `SYO500_8.008`

[MichaelRawson]

Strategy can be minimised to -drc encompass -foolp on -kws precedence -spb units (Otter or DISCOUNT also work for reproducibility). Playing around with the options gets you a proof (!). I guess that some combination of these options is subtly incomplete, but we don't know about it yet.

[quickbeam123]

Funnily, finite model finding finds a model of size 3 and then crashes. But that's probably a different bug:

./vampire Problems/SYO/SYO500_8.008.p -sa fmb -foolp on 
% Running in auto input_syntax mode. Trying TPTP
Detected minimum model sizes of [1]
Detected maximum model sizes of [34]
TRYING [1]
TRYING [2]
TRYING [3]
Finite Model Found!
% SZS status CounterSatisfiable for SYO500_8.008
Condition n < _size in file ./Lib/DArray.hpp, line 105 was violated, as:
n == 1
_size == 0

[quickbeam123]

"Works" equally well on the smaller Problems/SYO/SYO500_8.002.p

[quickbeam123]

The problem is likely that

[SA] forward reduce: 3. ($true != $false) [fool axiom]
      replaced by 166. ($true != bG6) <- (~3) [forward demodulation 3,161]
     using 161. ($false = bG6) <- (~3) [trivial inequality removal 160]

showing that $false is not the smallest constant.

show_ordering reveals that it is the smallest in the precedence

% function precedences, smallest symbols first (line format: `<name> <arity>`) 
% ===== begin of function precedences ===== 
% $$false 0
% $$true 0
% bG0 0
% bG1 0
...

but not regarding the symbol weights

% Weights of function (line format: `<name> <arity> <weight>`)
% ===== begin of function weights ===== 
% bG0 0 1
% bG1 0 2
% bG2 0 3
% bG3 0 4
% bG4 0 5
% bG5 0 6
% bG6 0 7
% bG7 0 8
% $$false 0 9
% $$true 0 10
...

Shall a KBO expert fix this? ;)

[MichaelRawson]

Shall a KBO expert fix this? ;)

Is it a bird? Is it a plane? It's @mezpusz with his mighty convenient KBO superpowers (and recent patch series).

[quickbeam123]

Actually, I think it's @joe-hauns 's code which does the setting up (and the nice printing in show_ordering). And I already worked with it too.

[quickbeam123]

I think I have it... (PR incoming)

[joe-hauns]

The problem is likely that

[SA] forward reduce: 3. ($true != $false) [fool axiom]
      replaced by 166. ($true != bG6) <- (~3) [forward demodulation 3,161]
     using 161. ($false = bG6) <- (~3) [trivial inequality removal 160]

showing that $false is not the smallest constant.

Do we assume that $false is the least constant somewhere?

[mezpusz]

Apart from the fact that $false should be least in the precedence and -kws precedence incorrectly captures this and puts $false on top instead, is it really the case that we lose any properties of the simplification ordering? Or is it some FOOL-related inference that is in conflict with the simplification ordering?

[mezpusz]

We use FOOLParamodulation but it is a generating inference, so it shouldn't affect completeness, right? Am I missing something?

[quickbeam123]

FoolParamodulation is deliberately restricted paramidulation with forall Z, X=true | X = false, which we never add explicitly. It's only complete when all > true > false.

[mezpusz]

Thanks for the explanation, now it makes sense!