search

ontologyportal / sigmakee

Sigma Knowledge Engineering Environment
GNU General Public License v3.0
100 stars 34 forks source link

EProver seems to not working in the apease/sigmakee2018:latest docker, and new docker fails to build #76

Open astroseger opened 1 year ago

astroseger commented 1 year ago

There are two possible problems:

  1. It seems that in apease/sigmakee2018:latest docker EProver is not working (and actually all other proposed reasoners). However it well might be that I'm not using it correctly. I connected to the server (http://localhost:8080/) and went to Ask/Tell menu. Proposed example query (instance ?X Relation) returns nothing. I've also tried the following: (query (equal 13 (MultiplicationFn 3 4))). It also returns nothing.

  2. I've tried to rebuild docker (In order to check reasoner in the master), but it fails with the following message:

    
BUILD FAILED
/sigma/workspace/sigmakee/build.xml:42: The following error occurred while executing this line:
Error reading project file /sigma/workspace/TPTP-ANTLR/build.xml: /sigma/workspace/TPTP-ANTLR/build.xml

Total time: 0 seconds The command '/bin/sh -c apt update && apt -qq install -y ant git make gcc graphviz openjdk-8-jdk-headless && rm -rf /var/lib/apt/lists/* && apt clean -y && apt autoclean -y && mkdir -p $WORKSPACE $PROGRAMS $KBDIR && cd $PROGRAMS && wget 'http://wwwlehre.dhbw-stuttgart.de/~sschulz/WORK/E_DOWNLOAD/V_2.0/E.tgz' && tar xvf E.tgz && cd $PROGRAMS/E && ./configure && make && make install && cd $WORKSPACE && git clone https://github.com/ontologyportal/sigmakee && cd $SIGMA_SRC && sed -i "s/theuser/$ME/g" config.xml && cp config.xml $KBDIR && ant && cd $KBDIR && sed -i "s/.sigmakee/sigmakee/g" config.xml && sed -i 's/~/\'"$SIGMADIR"'/g' config.xml && rm -r $WORKSPACE && chmod -R 777 $SIGMADIR' returned a non-zero code: 1

apease commented 1 year ago

The Docker version of SigmaKEE is very out of date at this point (since 2018) and I haven't been maintaining it. I recommend the 'native' install of SigmaKEE as described in the README. There's a video that can help at https://www.youtube.com/watch?v=ZVW0WllvoUU&t=3s&ab_channel=OntologyTalkwithAdamPease

astroseger commented 1 year ago

@apease thank you for your answer. Indeed native installation works and I've managed to run reasoning via Ask/Tell interface, but only with Vampire, for some reason the EProver option is gray. In README is written that Ask/Tell interface is not well maintained, so there are two questions:

  1. What would be the most "canonical" way to run reasoning in the case when there is an addition to the knowledge base. For example we want to add some "individuals" and make reasoning about them?
  2. Where would be the best place to find some practical examples of relatively complex reasoning with SUMO ontology?
apease commented 1 year ago

Hi Sergey I'm travelling today so I hope to respond in detail tomorrow. Eprover should work with sigma, I'll try to replicate. The tests directory in the sigma repository should provide some more complex examples of reasoning problems.

All the best Adam

On Nov 3, 2022 11:19 AM, Sergey Rodionov @.***> wrote:

@apeasehttps://github.com/apease thank you for your answer. Indeed native installation works and I've managed to run reasoning via Ask/Tell interface, but only with Vampire, for some reason the EProver option is gray. In README is written that Ask/Tell interface is not well maintained, so there are two questions:

  1. What would be the most "canonical" way to run reasoning in the case when there is an addition to the knowledge base. For example we want to add some "individuals" and make reasoning about them?
  2. Where would be the best place to find some practical examples of relatively complex reasoning with SUMO ontology?

— Reply to this email directly, view it on GitHubhttps://github.com/ontologyportal/sigmakee/issues/76#issuecomment-1301954785, or unsubscribehttps://github.com/notifications/unsubscribe-auth/AAQG6HKT4TR3QP6JDS5YEK3WGONUBANCNFSM6AAAAAARTHKHF4. You are receiving this because you were mentioned.Message ID: @.***>

astroseger commented 1 year ago

Hi Adam!

Actually the part of the problem with EProver was because of wrong path to EProver in ~/.sigmakee/KBs/config.xml. If ones strictly follows instruction in README (section Linux Installation) he will get e_ltb_runner in /home/<user>/Programs/E/PROVER/e_ltb_runner, but in config it will be /home/<user>/E/bin/e_ltb_runner.

However, even after this fix, EProver doesn't seem to work.

For the following call :

java -Xmx10g -classpath /home/sumo/workspace/sigmakee/build/sigmakee.jar:/home/sumo/workspace/sigmakee/build/lib/* com.articulate.sigma.KB -ae "(subclass ?X Object)"

return the following (I will post the whole output just in case)

INFO in KB.main()
KB.main(): Note! Not loading lexicons.
Info in KBmanager.initializeOnce()
Info in KBmanager.initializeOnce(): initializing with /home/sumo/.sigmakee/KBs
KBmanager.readConfiguration()
KBmanager.serializedExists(): true
KBmanager.serializedOld(config): 
KBmanager.serializedOld(config): save date: Thu Nov 03 16:04:51 UTC 2022
kbsFilenamesFromXML(): Completed loading KB names
serializedOld(): file /home/sumo/.sigmakee/KBs/english_format.kif was saved on Wed Nov 02 15:46:24 UTC 2022
serializedOld(): file /home/sumo/.sigmakee/KBs/domainEnglishFormat.kif was saved on Wed Nov 02 15:46:24 UTC 2022
serializedOld(): file /home/sumo/.sigmakee/KBs/ArabicCulture.kif was saved on Wed Nov 02 15:46:24 UTC 2022
serializedOld(): file /home/sumo/.sigmakee/KBs/Biography.kif was saved on Wed Nov 02 15:46:24 UTC 2022
serializedOld(): file /home/sumo/.sigmakee/KBs/Cars.kif was saved on Wed Nov 02 15:46:24 UTC 2022
serializedOld(): file /home/sumo/.sigmakee/KBs/Catalog.kif was saved on Wed Nov 02 15:46:24 UTC 2022
serializedOld(): file /home/sumo/.sigmakee/KBs/Communications.kif was saved on Wed Nov 02 15:46:24 UTC 2022
serializedOld(): file /home/sumo/.sigmakee/KBs/CountriesAndRegions.kif was saved on Wed Nov 02 15:46:24 UTC 2022
serializedOld(): file /home/sumo/.sigmakee/KBs/Dining.kif was saved on Wed Nov 02 15:46:24 UTC 2022
serializedOld(): file /home/sumo/.sigmakee/KBs/Economy.kif was saved on Wed Nov 02 15:46:24 UTC 2022
serializedOld(): file /home/sumo/.sigmakee/KBs/engineering.kif was saved on Wed Nov 02 15:46:24 UTC 2022
serializedOld(): file /home/sumo/.sigmakee/KBs/FinancialOntology.kif was saved on Wed Nov 02 15:46:24 UTC 2022
serializedOld(): file /home/sumo/.sigmakee/KBs/Food.kif was saved on Wed Nov 02 15:46:24 UTC 2022
serializedOld(): file /home/sumo/.sigmakee/KBs/Geography.kif was saved on Wed Nov 02 15:46:24 UTC 2022
serializedOld(): file /home/sumo/.sigmakee/KBs/Government.kif was saved on Wed Nov 02 15:46:24 UTC 2022
serializedOld(): file /home/sumo/.sigmakee/KBs/Hotel.kif was saved on Wed Nov 02 15:46:24 UTC 2022
serializedOld(): file /home/sumo/.sigmakee/KBs/Justice.kif was saved on Wed Nov 02 15:46:24 UTC 2022
serializedOld(): file /home/sumo/.sigmakee/KBs/Languages.kif was saved on Wed Nov 02 15:46:24 UTC 2022
serializedOld(): file /home/sumo/.sigmakee/KBs/Law.kif was saved on Wed Nov 02 15:46:24 UTC 2022
serializedOld(): file /home/sumo/.sigmakee/KBs/Media.kif was saved on Wed Nov 02 15:46:24 UTC 2022
serializedOld(): file /home/sumo/.sigmakee/KBs/Merge.kif was saved on Wed Nov 02 15:46:24 UTC 2022
serializedOld(): file /home/sumo/.sigmakee/KBs/Mid-level-ontology.kif was saved on Wed Nov 02 15:46:24 UTC 2022
serializedOld(): file /home/sumo/.sigmakee/KBs/MilitaryDevices.kif was saved on Wed Nov 02 15:46:24 UTC 2022
serializedOld(): file /home/sumo/.sigmakee/KBs/Military.kif was saved on Wed Nov 02 15:46:24 UTC 2022
serializedOld(): file /home/sumo/.sigmakee/KBs/MilitaryPersons.kif was saved on Wed Nov 02 15:46:24 UTC 2022
serializedOld(): file /home/sumo/.sigmakee/KBs/MilitaryProcesses.kif was saved on Wed Nov 02 15:46:24 UTC 2022
serializedOld(): file /home/sumo/.sigmakee/KBs/Music.kif was saved on Wed Nov 02 15:46:24 UTC 2022
serializedOld(): file /home/sumo/.sigmakee/KBs/naics.kif was saved on Wed Nov 02 15:46:24 UTC 2022
serializedOld(): file /home/sumo/.sigmakee/KBs/People.kif was saved on Wed Nov 02 15:46:24 UTC 2022
serializedOld(): file /home/sumo/.sigmakee/KBs/pictureList.kif was saved on Wed Nov 02 15:46:24 UTC 2022
serializedOld(): file /home/sumo/.sigmakee/KBs/pictureList-ImageNet.kif was saved on Wed Nov 02 15:46:24 UTC 2022
serializedOld(): file /home/sumo/.sigmakee/KBs/QoSontology.kif was saved on Wed Nov 02 15:46:24 UTC 2022
serializedOld(): file /home/sumo/.sigmakee/KBs/Sports.kif was saved on Wed Nov 02 15:46:24 UTC 2022
serializedOld(): file /home/sumo/.sigmakee/KBs/TransnationalIssues.kif was saved on Wed Nov 02 15:46:24 UTC 2022
serializedOld(): file /home/sumo/.sigmakee/KBs/Transportation.kif was saved on Wed Nov 02 15:46:24 UTC 2022
serializedOld(): file /home/sumo/.sigmakee/KBs/TransportDetail.kif was saved on Wed Nov 02 15:46:24 UTC 2022
serializedOld(): file /home/sumo/.sigmakee/KBs/UXExperimentalTerms.kif was saved on Wed Nov 02 15:46:24 UTC 2022
serializedOld(): file /home/sumo/.sigmakee/KBs/VirusProteinAndCellPart.kif was saved on Wed Nov 02 15:46:24 UTC 2022
serializedOld(): file /home/sumo/.sigmakee/KBs/Weather.kif was saved on Wed Nov 02 15:46:24 UTC 2022
serializedOld(): file /home/sumo/.sigmakee/KBs/WMD.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.serializedOld(config): returning false (not old)
KBmanager.loadSerialized(): KBmanager has been deserialized 
WordNet.initOnce(): 'disable' is: true
Info in KBmanager.initializeOnce(): initialized is true
KBmanager.initializeOnce(): total init time in seconds: 51
INFO in KB.loadEProver(): Creating new process
KBmanager.tptpOld(config): 
KBmanager.tptpOld(): file SUMO.tptp was saved on Thu Nov 03 17:40:01 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/english_format.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/domainEnglishFormat.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/ArabicCulture.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/Biography.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/Cars.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/Catalog.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/Communications.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/CountriesAndRegions.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/Dining.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/Economy.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/engineering.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/FinancialOntology.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/Food.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/Geography.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/Government.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/Hotel.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/Justice.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/Languages.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/Law.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/Media.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/Merge.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/Mid-level-ontology.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/MilitaryDevices.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/Military.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/MilitaryPersons.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/MilitaryProcesses.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/Music.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/naics.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/People.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/pictureList.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/pictureList-ImageNet.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/QoSontology.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/Sports.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/TransnationalIssues.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/Transportation.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/TransportDetail.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/UXExperimentalTerms.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/VirusProteinAndCellPart.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/Weather.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/WMD.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.infFileOld(config): returning false (not old)
INFO in EProver.writeBatchFile(): writing EBatchConfig.txt with KB file /home/sumo/.sigmakee/KBs/SUMO.tptp
INFO in EProver(): executable: /home/sumo/Programs/E/PROVER/e_ltb_runner
INFO in EProver(): kbFile: /home/sumo/.sigmakee/KBs/SUMO.tptp
EProver(): command: [/home/sumo/Programs/E/PROVER/e_ltb_runner, --interactive, /home/sumo/.sigmakee/KBs/EBatchConfig.txt, /home/sumo/Programs/E/PROVER/eprover]
EProver(): new process: Process[pid=313, exitValue="not exited"]
INFO in KB.loadEProver(): Creating new process
INFO in KB.loadEProver(): terminating old process first

TERMINATING 
DESTROYING the Process Process[pid=313, exitValue="not exited"]

KBmanager.tptpOld(config): 
KBmanager.tptpOld(): file SUMO.tptp was saved on Thu Nov 03 17:40:01 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/english_format.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/domainEnglishFormat.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/ArabicCulture.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/Biography.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/Cars.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/Catalog.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/Communications.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/CountriesAndRegions.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/Dining.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/Economy.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/engineering.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/FinancialOntology.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/Food.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/Geography.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/Government.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/Hotel.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/Justice.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/Languages.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/Law.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/Media.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/Merge.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/Mid-level-ontology.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/MilitaryDevices.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/Military.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/MilitaryPersons.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/MilitaryProcesses.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/Music.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/naics.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/People.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/pictureList.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/pictureList-ImageNet.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/QoSontology.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/Sports.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/TransnationalIssues.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/Transportation.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/TransportDetail.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/UXExperimentalTerms.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/VirusProteinAndCellPart.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/Weather.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.tptpOld(): file /home/sumo/.sigmakee/KBs/WMD.kif was saved on Wed Nov 02 15:46:24 UTC 2022
KBmanager.infFileOld(config): returning false (not old)
INFO in EProver.writeBatchFile(): writing EBatchConfig.txt with KB file /home/sumo/.sigmakee/KBs/SUMO.tptp
INFO in EProver(): executable: /home/sumo/Programs/E/PROVER/e_ltb_runner
INFO in EProver(): kbFile: /home/sumo/.sigmakee/KBs/SUMO.tptp
EProver(): command: [/home/sumo/Programs/E/PROVER/e_ltb_runner, --interactive, /home/sumo/.sigmakee/KBs/EBatchConfig.txt, /home/sumo/Programs/E/PROVER/eprover]
EProver(): new process: Process[pid=315, exitValue="not exited"]
EProver(): command: [/home/sumo/Programs/E/PROVER/e_ltb_runner, --interactive, /home/sumo/.sigmakee/KBs/EBatchConfig.txt, /home/sumo/Programs/E/PROVER/eprover]
EProver(): process: Process[pid=316, exitValue="not exited"]
EProver.submitQuery(): process: Process[pid=316, exitValue="not exited"]

INFO in EProver.submitQuery() write: fof(conj1,conjecture, ( ( ? [V__X] : (s__subclass(V__X,s__Object) ) ) )).

INFO in EProver.submitQuery() write: go.
INFO in EProver.submitQuery(1): line: # Parsing /home/sumo/.sigmakee/KBs/SUMO.tptp
INFO in EProver.submitQuery(1): line: 
INFO in EProver.submitQuery: line: 
INFO in EProver.submitQuery: line: # == WCT:    0s, Solved:    0/   0    ==
INFO in EProver.submitQuery: line: # =============== Batch done ===========
INFO in EProver.submitQuery: line: 
INFO in EProver.submitQuery: line: # Enter job, 'help' or 'quit', followed by 'go.' on a line of its own:
INFO in EProver.submitQuery: line: 
INFO in EProver.submitQuery: line: # Processing started for unnamed_job
INFO in EProver.submitQuery: line: # Filtering for Threshold(10000) (201)
INFO in EProver.submitQuery: line: # Filtering for GSinE(CountFormulas, hypos, 6.000000, 9223372036854775807, 5, 20000, 1.000000) (201)
INFO in EProver.submitQuery: line: # Filtering for GSinE(CountFormulas, hypos, 1.200000, 9223372036854775807, 2, 20000, 1.000000) (201)
INFO in EProver.submitQuery: line: # Filtering for GSinE(CountFormulas, nohypos, 2.000000, 9223372036854775807, 2147483647, 20000, 1.000000) (201)
INFO in EProver.submitQuery: line: # Filtering for GSinE(CountFormulas, hypos, 2.000000, 9223372036854775807, 3, 20000, 1.000000) (201)
INFO in EProver.submitQuery: line: # Filtering for GSinE(CountFormulas, hypos, 1.200000, 9223372036854775807, 2147483647, 100, 1.000000) (201)
INFO in EProver.submitQuery: line: # Filtering for GSinE(CountFormulas, hypos, 5.000000, 9223372036854775807, 4, 20000, 1.000000) (201)
INFO in EProver.submitQuery: line: # Filtering for GSinE(CountFormulas, nohypos, 1.500000, 9223372036854775807, 2147483647, 20000, 1.000000) (201)
INFO in EProver.submitQuery: line: # Filtering for GSinE(CountFormulas, hypos, 1.200000, 9223372036854775807, 2147483647, 500, 1.000000) (201)
INFO in EProver.submitQuery: line: # Filtering for GSinE(CountFormulas, nohypos, 1.200000, 9223372036854775807, 2147483647, 1000, 1.000000) (201)
INFO in EProver.submitQuery: line: # Filtering for GSinE(CountFormulas, nohypos, 1.200000, 9223372036854775807, 2, 20000, 1.000000) (201)
INFO in EProver.submitQuery: line: # Filtering for GSinE(CountFormulas, nohypos, 5.000000, 9223372036854775807, 4, 20000, 1.000000) (201)
INFO in EProver.submitQuery: line: # Filtering for GSinE(CountFormulas, nohypos, 6.000000, 9223372036854775807, 5, 20000, 1.000000) (201)
INFO in EProver.submitQuery: line: # No proof found by Threshold(10000)
INFO in EProver.submitQuery: line: # No proof found by GSinE(CountFormulas, hypos, 6.000000, 9223372036854775807, 5, 20000, 1.000000)
INFO in EProver.submitQuery: line: # No proof found by GSinE(CountFormulas, hypos, 1.200000, 9223372036854775807, 2, 20000, 1.000000)
INFO in EProver.submitQuery: line: # No proof found by GSinE(CountFormulas, nohypos, 2.000000, 9223372036854775807, 2147483647, 20000, 1.000000)
INFO in EProver.submitQuery: line: # No proof found by GSinE(CountFormulas, hypos, 2.000000, 9223372036854775807, 3, 20000, 1.000000)
INFO in EProver.submitQuery: line: # No proof found by GSinE(CountFormulas, hypos, 1.200000, 9223372036854775807, 2147483647, 100, 1.000000)
INFO in EProver.submitQuery: line: # No proof found by GSinE(CountFormulas, hypos, 5.000000, 9223372036854775807, 4, 20000, 1.000000)
INFO in EProver.submitQuery: line: # No proof found by GSinE(CountFormulas, nohypos, 1.500000, 9223372036854775807, 2147483647, 20000, 1.000000)
INFO in EProver.submitQuery: line: # No proof found by GSinE(CountFormulas, hypos, 1.200000, 9223372036854775807, 2147483647, 500, 1.000000)
INFO in EProver.submitQuery: line: # No proof found by GSinE(CountFormulas, nohypos, 1.200000, 9223372036854775807, 2147483647, 1000, 1.000000)
INFO in EProver.submitQuery: line: # No proof found by GSinE(CountFormulas, nohypos, 1.200000, 9223372036854775807, 2, 20000, 1.000000)
INFO in EProver.submitQuery: line: # No proof found by GSinE(CountFormulas, nohypos, 5.000000, 9223372036854775807, 4, 20000, 1.000000)
INFO in EProver.submitQuery: line: # No proof found by GSinE(CountFormulas, nohypos, 6.000000, 9223372036854775807, 5, 20000, 1.000000)
INFO in EProver.submitQuery: line: # SZS status GaveUp for unnamed_job
INFO in EProver.submitQuery: line: 
INFO in EProver.submitQuery: line: # Processing finished for unnamed_job
INFO in EProver.submitQuery: line: 
INFO in EProver.submitQuery: line: # Enter job, 'help' or 'quit', followed by 'go.' on a line of its own:
KB.main(): completed Eprover query with result: 

# == WCT:    0s, Solved:    0/   0    ==
# =============== Batch done ===========

# Enter job, 'help' or 'quit', followed by 'go.' on a line of its own:

# Processing started for unnamed_job
# Filtering for Threshold(10000) (201)
# Filtering for GSinE(CountFormulas, hypos, 6.000000, 9223372036854775807, 5, 20000, 1.000000) (201)
# Filtering for GSinE(CountFormulas, hypos, 1.200000, 9223372036854775807, 2, 20000, 1.000000) (201)
# Filtering for GSinE(CountFormulas, nohypos, 2.000000, 9223372036854775807, 2147483647, 20000, 1.000000) (201)
# Filtering for GSinE(CountFormulas, hypos, 2.000000, 9223372036854775807, 3, 20000, 1.000000) (201)
# Filtering for GSinE(CountFormulas, hypos, 1.200000, 9223372036854775807, 2147483647, 100, 1.000000) (201)
# Filtering for GSinE(CountFormulas, hypos, 5.000000, 9223372036854775807, 4, 20000, 1.000000) (201)
# Filtering for GSinE(CountFormulas, nohypos, 1.500000, 9223372036854775807, 2147483647, 20000, 1.000000) (201)
# Filtering for GSinE(CountFormulas, hypos, 1.200000, 9223372036854775807, 2147483647, 500, 1.000000) (201)
# Filtering for GSinE(CountFormulas, nohypos, 1.200000, 9223372036854775807, 2147483647, 1000, 1.000000) (201)
# Filtering for GSinE(CountFormulas, nohypos, 1.200000, 9223372036854775807, 2, 20000, 1.000000) (201)
# Filtering for GSinE(CountFormulas, nohypos, 5.000000, 9223372036854775807, 4, 20000, 1.000000) (201)
# Filtering for GSinE(CountFormulas, nohypos, 6.000000, 9223372036854775807, 5, 20000, 1.000000) (201)
# No proof found by Threshold(10000)
# No proof found by GSinE(CountFormulas, hypos, 6.000000, 9223372036854775807, 5, 20000, 1.000000)
# No proof found by GSinE(CountFormulas, hypos, 1.200000, 9223372036854775807, 2, 20000, 1.000000)
# No proof found by GSinE(CountFormulas, nohypos, 2.000000, 9223372036854775807, 2147483647, 20000, 1.000000)
# No proof found by GSinE(CountFormulas, hypos, 2.000000, 9223372036854775807, 3, 20000, 1.000000)
# No proof found by GSinE(CountFormulas, hypos, 1.200000, 9223372036854775807, 2147483647, 100, 1.000000)
# No proof found by GSinE(CountFormulas, hypos, 5.000000, 9223372036854775807, 4, 20000, 1.000000)
# No proof found by GSinE(CountFormulas, nohypos, 1.500000, 9223372036854775807, 2147483647, 20000, 1.000000)
# No proof found by GSinE(CountFormulas, hypos, 1.200000, 9223372036854775807, 2147483647, 500, 1.000000)
# No proof found by GSinE(CountFormulas, nohypos, 1.200000, 9223372036854775807, 2147483647, 1000, 1.000000)
# No proof found by GSinE(CountFormulas, nohypos, 1.200000, 9223372036854775807, 2, 20000, 1.000000)
# No proof found by GSinE(CountFormulas, nohypos, 5.000000, 9223372036854775807, 4, 20000, 1.000000)
# No proof found by GSinE(CountFormulas, nohypos, 6.000000, 9223372036854775807, 5, 20000, 1.000000)
# SZS status GaveUp for unnamed_job

# Processing finished for unnamed_job

# Enter job, 'help' or 'quit', followed by 'go.' on a line of its own:
Graph.createGraphBody(): creating file at /home/sumo/Programs/apache-tomcat-8.5.23/webapps/sigma/graph/proof.dot
Graph.createDotGraph(): exec command: /usr/bin/dot /home/sumo/Programs/apache-tomcat-8.5.23/webapps/sigma/graph/proof.dot -Tgif
Graph.createDotGraph(): write image file: /home/sumo/Programs/apache-tomcat-8.5.23/webapps/sigma/graph/proof.gif
KB.main(): binding map: {}
KB.main(): proof with level 1
KB.main(): axiom key size 0
apease commented 1 year ago

Hi Sergey, Yes, as per the README every occurance of 'theuser' needs to be changed to conform to your username/path . But there appears to be an issue that the tptp file isn't getting generated and so the theorem provers have no content to prove on, at least on my installation. I'm worried I might have uploaded a test version that turned off inference. I'm researching this and hope to respond soon.

apease commented 1 year ago

Hi Sergey, I'm not sure what's causing the issue at the moment. Recently, I've been just generating TPTP FOF (of TFF or TFF) from Sigma's command line interface, then running provers directly. It has a shorter workflow than doing things from the GUI. For example java -Xmx14g -classpath /home/apease/workspace/sigmakee/lib/*:/home/apease/workspace/sigmakee/build/classes com.articulate.sigma.trans.SUMOKBtoTPTPKB then add your conjecture in TPTP FOF language to the generated SUMO.tptp file (found in your ~/.sigmakee/KBs dir), as in fof(query_0,conjecture,(( ( ? [VX] : (ssubclass(VX,sObject) ) ) ))). then run vampire, as in

/home/apease/workspace/vampire/vampire --proof tptp -t 30 /home/apease/.sigmakee/KBs/SUMOedited.tptp

Vampire generally is doing better than E for fof queries in recent versions