InferenceTestSuite

[arademaker]

• we need a way to determine the KB to be used. This can be done in the tq file (as discussed in test framework: add extra meta-predicate (ontology ...) that specify the kif files needed. sumo#218) or as a parameter for the command line, specifying one of the KBs listed in the config.xml file. I would prefer the second option.
• we need to avoid the loading of WN and mappings files.

[apease]

Do you have a valid path as referenced below: /home/theuser/workspace/vampire/vampire I'm guessing that should instead be /home/arademaker/workspace/vampire/vampire

[arademaker]

OK, I managed to run

% java -Xmx7g -classpath $SIGMA_CP com.articulate.sigma.InferenceTestSuite -t SP01.kif.tq

But it gives me the output below. I see the Satisfiable message from Vampire the CounterSatisfiable for temp-comb reported by the InferenceTestSuite.inferenceUnitTest but then the last line shows Failure on SP01.kif.tq… why this failure?!

Regarding answer extraction, I suspect we should have a notation for that, right? In the SP01.kif.tq (see branch spatial in the SUMO repo) I didn’t ask for any specific answer

(query (orientation X Z Right))

But after changing it to

(query (orientation ?X C Right))

I didn't have any change in the output...

% # SZS output end Saturation.
% ------------------------------
% Version: Vampire 4.4.0 (commit 3dd0ed0c on 2020-02-04 14:57:07 +0100)
% Termination reason: Satisfiable

% Memory used [KB]: 1279
% Time elapsed: 0.015 s
% ------------------------------
% ------------------------------
% Success in time 14.681 s

Index: 4, Size: 4
InferenceTestSuite.inferenceUnitTest(): bindings: []
InferenceTestSuite.inferenceUnitTest(): bindingMap: {}
InferenceTestSuite.inferenceUnitTest(): proof: []
InferenceTestSuite.inferenceUnitTest(): answers: []
InferenceTestSuite.inferenceUnitTest(): tpp status: CounterSatisfiable for temp-comb

============================
InferenceTestSuite.cmdLineTest() : Failure on SP01.kif.tq

[apease]

I get a proof for this one so it appears to be a configuration issue.

% SZS output end Proof for temp-comb
% ------------------------------
% Version: Vampire 4.4.0 (commit c41a8b5f on 2020-03-31 20:18:58 +0200)
% Termination reason: Refutation

% Memory used [KB]: 22259
% Time elapsed: 0.050 s
% ------------------------------
% ------------------------------
% Success in time 0.509 s

InferenceTestSuite.inferenceUnitTest(): bindings: []
InferenceTestSuite.inferenceUnitTest(): bindingMap: {}
InferenceTestSuite.inferenceUnitTest(): proof: [1. (not
(orientation A C Right)) [] negated_conjecture
...

[apease]

I see that you have changed the query, and it asks about two constants not in the problem. I have

InferenceTestSuite.inferenceUnitTest(): ask: (orientation A C Right)

[apease]

added config.xml option key "loadLexicons" with value "false" to turn off loading lexicons, in latest push 6fb4db2

[arademaker]

I didn't understand the #60 (comment). In https://github.com/ontologyportal/sumo/blob/spatial/tests/SP01.kif.tq the constants A and C are defined. I am using Merge.kif only.

[apease]

Your first query says (query (orientation X Z Right))

[apease]

try using tinySUMO.kif first to see if it works

[arademaker]

I have

<configuration >
  <preference name="sumokbname" value="tiny" />
  ...
  <kb name="full">
    ...
  </kb>
  <kb name="toplevel" >
    <constituent filename="Merge.kif" />
  </kb>

  <kb name="tiny">
    <constituent filename="tinySUMO.kif" />
  </kb>
</configuration>

But I am still getting:

java -Xmx7g -classpath $SIGMA_CP com.articulate.sigma.InferenceTestSuite -t SP01.kif.tq
...
% # SZS output end Saturation.
% ------------------------------
% Version: Vampire 4.4.0 (commit 3dd0ed0c on 2020-02-04 14:57:07 +0100)
% Termination reason: Satisfiable

% Memory used [KB]: 1279
% Time elapsed: 0.013 s
% ------------------------------
% ------------------------------
% Success in time 17.066 s

Index: 4, Size: 4
InferenceTestSuite.inferenceUnitTest(): bindings: []
InferenceTestSuite.inferenceUnitTest(): bindingMap: {}
InferenceTestSuite.inferenceUnitTest(): proof: []
InferenceTestSuite.inferenceUnitTest(): answers: []
InferenceTestSuite.inferenceUnitTest(): tpp status: CounterSatisfiable for temp-comb

============================
InferenceTestSuite.cmdLineTest() : Failure on SP01.kif.tq

[apease]

please pipe your output to a file and send to me privately and I'll try to figure out what might be wrong