No proof when the conjecture is $true

[jonaprieto]

Joe,

The output of the current version outputs nothing for true conjecture
like in the following file:

$ cat basic-01.tptp
fof(goal, conjecture, $true).
$ metis --version
metis 2.4 (release 20180810)
$ metis basic-01.tptp
% SZS status Theorem for basic-01.tptp

This used to be different. If we use a previous version we got something different
like the following (I'm using here my online-atps tool to call SystemOnTPTP, which
has Metis v2.4. Surely, an outdated version).

$ online-atps --version-atp=online-metis
Metis---2.4

And ...

$ online-atps --atp=online-metis test/prop-pack/problems/basic/basic-01.tptp
....
% SZS output start CNFRefutation for /tmp/SystemOnTPTPFormReply11095/SOT_A4iF9J
fof(goal, conjecture, ($true)).

fof(subgoal_0, plain, ($true), inference(strip, [], [goal])).

fof(negate_0_0, plain, (~ $true), inference(negate, [], [subgoal_0])).

fof(normalize_0_0, plain, ($false),
    inference(canonicalize, [], [negate_0_0])).

cnf(refute_0_0, plain, ($false),
    inference(canonicalize, [], [normalize_0_0])).
% SZS output end CNFRefutation for /tmp/SystemOnTPTPFormReply11095/SOT_A4iF9J
...

[gilith]

By default Metis only reports the status of a problem:

$ metis TRUE.tptp 
% SZS status Theorem for TRUE.tptp

You can also ask it to output proofs like so:

$ metis --show proof TRUE.tptp 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% SZS status Theorem for TRUE.tptp

% SZS output start CNFRefutation for TRUE.tptp
fof(goal, conjecture, ($true)).

fof(subgoal_0, plain, ($true), inference(strip, [], [goal])).

fof(negate_0_0, plain, (~ $true), inference(negate, [], [subgoal_0])).

fof(normalize_0_0, plain, ($false),
    inference(canonicalize, [], [negate_0_0])).

cnf(refute_0_0, plain, ($false),
    inference(canonicalize, [], [normalize_0_0])).
% SZS output end CNFRefutation for TRUE.tptp

I assume that is how Metis is configured on SystemOnTPTP, but I don't know how to check this.

[gilith]

Actually, the calling invocation is right on the front page of SystemOnTPTP:

metis --show proof --show saturation %s

This confirms the arguments needed to output the proof (or saturating model for invalid conjectures).

[jonaprieto]

Ops! but of course, I forgot the arguments.
Sorry. It's been a while since the last time I used Metis.
It'll update my settings.