Simplify outputs $false, maybe wrongly.

[jonaprieto]

With the following problem:

$ cat problem.tptp
fof(goal, conjecture, (((p <=> q) <=> r) <=> (p <=> (q <=> r)))).

I am getting this with Metis

$ metis --version
metis 2.3.1 (release 20161108)
$ metis --show proof problem.tptp
...
fof(normalize_2_0, plain, (~ p & (~ q <=> ~ r) & (~ p <=> (~ q <=> ~ r))),
    inference(canonicalize, [], [negate_2_0])).

fof(normalize_2_1, plain, (~ p <=> (~ q <=> ~ r)),
    inference(conjunct, [], [normalize_2_0])).

fof(normalize_2_2, plain, (~ q <=> ~ r),
    inference(conjunct, [], [normalize_2_0])).

fof(normalize_2_3, plain, (~ p), inference(conjunct, [], [normalize_2_0])).

fof(normalize_2_4, plain, ($false),
    inference(simplify, [],
              [normalize_2_1, normalize_2_2, normalize_2_3])).
...

I do not know how simplify deduces $false in this case, maybe I am forgetting something.
Anyway, I am taking this chance to ask you about this inference? how it works.

Thanks in advance.

CC` @asr

[asr]

$ metis --version
metis 2.3.1 (release 20161108)

2.3.1? I got 2.3.

[gilith]

Thank you for reporting this: the root-cause was a bug in the printing of the proof, specifically in the conversion of Xor sets to Iff lists. I've pushed and released a fixed version of Metis, and now the output looks like this:

$ metis --version
metis 2.3 (release 20170315)
$ metis --show proof problem.tptp
...
fof(normalize_2_0, plain, (~ p & (~ q <=> ~ r) & (~ p <=> (~ q <=> r))),
    inference(canonicalize, [], [negate_2_0])).

fof(normalize_2_1, plain, (~ p <=> (~ q <=> r)),
    inference(conjunct, [], [normalize_2_0])).

fof(normalize_2_2, plain, (~ q <=> ~ r),
    inference(conjunct, [], [normalize_2_0])).

fof(normalize_2_3, plain, (~ p), inference(conjunct, [], [normalize_2_0])).

fof(normalize_2_4, plain, ($false),
    inference(simplify, [],
              [normalize_2_1, normalize_2_2, normalize_2_3])).
...

Now it's clear how Metis derived $false in this subgoal.

Cheers,

Joe

[jonaprieto]

Thanks Joe.