When running the following vampire proof we see that it gets syntax errors for parenthesis in TPTP3ProofProcessor.parseProofOutput():
line 1:69 missing ')' at ','
line 1:95 extraneous input ')' expecting ').'
Needs further investigation. I could not reproduce the issue on my machine.
Below are the full logs with the errors:
(base) apease@apease-ThinkPad-L14-Gen-1:~/workspace/sigmakee$ java -cp build/classes:lib/* com.articulate.sigma.tp.TheoremProverController -v "(subclass ?x Object)"
TheoremProverController.main({v=[(subclass ?x Object)]})
[KButilities] SIGMA_HOME set to /home/apease/.sigmakee
INFO [KBmanager.initializeOnce()] Initializing KBmanager!
INFO [KBmanager.initializeOnce()] Loading English Lexicons...
INFO [WordNet.initOnce()] Loaded 117659 word senses in 1.524675103 seconds!
INFO [OMWordnet.readOMWfiles()] Loaded Serialized OMW Files in 0.39765021 seconds!
ERROR [VerbNet.readVerbFiles()] no such dir:
INFO [KBmanager.initializeOnce()] Loading from serialized cache...
INFO [KBmanager.initializeOnce()] Building SUMO Term Taxonomy...
INFO [KBmanager.initializeOnce()] Starting TPTP Background Generation...
INFO [KBmanager.cleanupOrphanedSessionDirectories()] No orphaned session directories found
INFO [KBmanager.initializeOnce()] Initialization completed in 2.554553511 seconds!
ATPQuery(VAMPIRE, CUSTOM, FOF, CASC)INFO [TPTPGenerationManager.lambda$startBackgroundGeneration$1()] SUMO.tptp is current! rebuilding axiomKey for incremental patching
INFO [TPTPGenerationManager.generateTHFPlain()] SUMO_plain.thf exists and is current!
INFO [TPTPGenerationManager.generateTHFModal()] SUMO_modal.thf exists and is current:
INFO [TPTPGenerationManager.lambda$startBackgroundGeneration$4()] SUMO_plain.thf generated in 0.016 seconds!
INFO [TPTPGenerationManager.lambda$startBackgroundGeneration$3()] SUMO_modal.thf generated in 0.016 seconds!
Vampire(SUMO, FOF, CASC, false, 30, 1, null)INFO [TPTPGenerationManager.lambda$startBackgroundGeneration$2()] SUMO.tff is current!
VAMPIRE LANGUAGE: fof
Vampire.askVampire((subclass ?x Object))
Vampire.run(SUMO.tptp, [fof(query_0,conjecture,(( ? [V__x] : (s__subclass(V__x,s__Object) ) ))).])
Vampire.getUserAssertions(SUMO, null)
Vampire.writeStatements([fof(query_0,conjecture,(( ? [V__x] : (s__subclass(V__x,s__Object) ) ))).])
Vampire.concatFiles(/home/apease/.sigmakee/KBs/SUMO.tptp, /home/apease/.sigmakee/KBs/temp-stmt.tptp, /home/apease/.sigmakee/KBs/temp-comb.tptp)INFO [SUMOKBtoTPTPKB.tWriteFile()] FormulaAST=48965/48965 expr!=null=48965 totalASTtranslated=48965 (cold=true)
Vampire.run(temp-comb.tptp)
Vampire.createCommandList(temp-comb.tptp)Vampire.run(): command: /home/apease/Programs/vampire/vampire --output_axiom_names on --proof tptp --mode casc -qa plain -t 30 /home/apease/.sigmakee/KBs/temp-comb.tptp
INFO [SUMOKBtoTPTPKB.translateOneFormula()] Using EXPR path for formula=(subclass Organism OrganicObject)
TheoremProverController.main(): Summary=
Vampire (CASC): Theorem in 611ms
Raw prover output:
% Running in auto input_syntax mode. Trying TPTP
% Detected formulas, will run a generic FOF schedule.
% lrs+1011_32_sil=2000:tgt=full:alpa=true:random_seed=3749040290:st=5:i=107:sd=1:qa=plain:ss=included:er=filter_296 on temp-comb for (296ds/107Mi)
% Instruction limit reached!
% ------------------------------
% Version: Vampire 5.0.0 (Release build, commit 84e7291a1 on 2025-12-10 13:35:22 +0000)
% CaDiCaL version: 2.1.3
% Termination reason: Instruction limit
% Termination phase: Property scanning
% Time elapsed: 0.029 s
% Peak memory usage: 17 MB
% Instructions burned: 109 (million)
% lrs+10_2:3_to=lpo:sil=16000:sp=arity:random_seed=2245284825:i=114:bd=all:qa=plain:ss=axioms:sgt=4_296 on temp-comb for (296ds/114Mi)
% Instruction limit reached!
% ------------------------------
% Version: Vampire 5.0.0 (Release build, commit 84e7291a1 on 2025-12-10 13:35:22 +0000)
% CaDiCaL version: 2.1.3
% Termination reason: Instruction limit
% Termination phase: SInE selection
% Time elapsed: 0.030 s
% Peak memory usage: 17 MB
% Instructions burned: 114 (million)
% ott+1011_2_sil=4000:lsd=20:rnwc=on:rp=on:sac=on:newcnf=on:random_seed=1142691385:i=132:kws=arity:qa=plain:er=filter_296 on temp-comb for (296ds/132Mi)
% Instruction limit reached!
% ------------------------------
% Version: Vampire 5.0.0 (Release build, commit 84e7291a1 on 2025-12-10 13:35:22 +0000)
% CaDiCaL version: 2.1.3
% Termination reason: Instruction limit
% Termination phase: Preprocessing 1
% Time elapsed: 0.035 s
% Peak memory usage: 17 MB
% Instructions burned: 132 (million)
% dis+1011_1_slsqr=8,1:sil=2000:spb=units:fd=off:kmz=on:flr=on:sac=on:slsq=on:random_seed=1016059282:st=2:i=121:sd=30:aac=none:ep=RS:qa=plain:ss=axioms:sgt=10_295 on temp-comb for (295ds/121Mi)
% Instruction limit reached!
% ------------------------------
% Version: Vampire 5.0.0 (Release build, commit 84e7291a1 on 2025-12-10 13:35:22 +0000)
% CaDiCaL version: 2.1.3
% Termination reason: Instruction limit
% Termination phase: SInE selection
% Time elapsed: 0.032 s
% Peak memory usage: 17 MB
% Instructions burned: 122 (million)
% lrs+10_1_sil=2000:sos=on:random_seed=4141339551:i=135:sd=2:qa=plain:gtg=position:ss=axioms_295 on temp-comb for (295ds/135Mi)
% Instruction limit reached!
% ------------------------------
% Version: Vampire 5.0.0 (Release build, commit 84e7291a1 on 2025-12-10 13:35:22 +0000)
% CaDiCaL version: 2.1.3
% Termination reason: Instruction limit
% Termination phase: Property scanning
% Time elapsed: 0.034 s
% Peak memory usage: 17 MB
% Instructions burned: 136 (million)
% lrs+1011_1_sil=16000:random_seed=346586930:i=269:sd=10:qa=plain:ss=axioms:sgt=16_295 on temp-comb for (295ds/269Mi)
% Refutation not found, incomplete strategy
% ------------------------------
% Version: Vampire 5.0.0 (Release build, commit 84e7291a1 on 2025-12-10 13:35:22 +0000)
% CaDiCaL version: 2.1.3
% Termination reason: Refutation not found, incomplete strategy
% Time elapsed: 0.028 s
% Peak memory usage: 20 MB
% Instructions burned: 164 (million)
% ------------------------------
% ------------------------------
% dis+1010_4_sil=2000:sos=on:sac=on:random_seed=252885651:i=140:sd=1:qa=plain:ss=axioms_294 on temp-comb for (294ds/140Mi)
% Instruction limit reached!
% ------------------------------
% Version: Vampire 5.0.0 (Release build, commit 84e7291a1 on 2025-12-10 13:35:22 +0000)
% CaDiCaL version: 2.1.3
% Termination reason: Instruction limit
% Termination phase: SInE selection
% Time elapsed: 0.023 s
% Peak memory usage: 17 MB
% Instructions burned: 143 (million)
% ott+11_4:1_bsr=on:slsqr=8,1:to=kbo:sil=4000:spb=goal:slsq=on:random_seed=3285244069:s2pl=on:st=3:s2a=on:i=124:gtgl=4:sd=1:kws=inv_arity:ep=RST:qa=plain:gtg=position:ss=axioms:fsd=on_294 on temp-comb for (294ds/124Mi)
% Instruction limit reached!
% ------------------------------
% Version: Vampire 5.0.0 (Release build, commit 84e7291a1 on 2025-12-10 13:35:22 +0000)
% CaDiCaL version: 2.1.3
% Termination reason: Instruction limit
% Termination phase: Property scanning
% Time elapsed: 0.019 s
% Peak memory usage: 17 MB
% Instructions burned: 129 (million)
% ott+1010_1_to=lpo:sil=32000:fde=none:sos=on:spb=goal_then_units:urr=on:random_seed=4266080600:st=2.5:cts=off:i=297:sd=4:ins=10:qa=plain:gsp=on:ss=axioms_294 on temp-comb for (294ds/297Mi)
% SZS answers Tuple [[s__Organism]|_] for temp-comb
% Solution written to "/tmp/vampire-proof-41261"
% Refutation found. Thanks to Tanya!
% SZS status Theorem for temp-comb
% SZS output start Proof for temp-comb
fof(f12995,axiom,(
s__subclass(s__Organism,s__Object)),
file('/home/apease/.sigmakee/KBs/temp-comb.tptp',kb_SUMO_12995)).
fof(f15018,conjecture,(
? [X0] : s__subclass(X0,s__Object)),
file('/home/apease/.sigmakee/KBs/temp-comb.tptp',query_0)).
fof(f15019,negated_conjecture,(
~? [X0] : s__subclass(X0,s__Object)),
inference(negated_conjecture,[status(cth)],[f15018])).
fof(f15020,plain,(
~? [X0] : (s__subclass(X0,s__Object) & ans0(X0))),
inference(answer_literal_injection,[],[f15019])).
fof(f15100,plain,(
! [X0] : (~s__subclass(X0,s__Object) | ~ans0(X0))),
inference(ennf_transformation,[],[f15020])).
fof(f15115,plain,(
( ! [X0] : (~s__subclass(X0,s__Object) | ~ans0(X0)) )),
inference(cnf_transformation,[],[f15100])).
fof(f15116,plain,(
s__subclass(s__Organism,s__Object)),
inference(cnf_transformation,[],[f12995])).
fof(f15249,plain,(
~ans0(s__Organism)),
inference(resolution,[],[f15115,f15116])).
fof(f15250,plain,(
( ! [X0] : (ans0(X0)) )),
introduced(definition,[],[answer_literal_resolver])).
fof(f15251,plain,(
$false),
inference(unit_resulting_resolution,[],[f15249,f15250])).
% SZS output end Proof for temp-comb
% ------------------------------
% Version: Vampire 5.0.0 (Release build, commit 84e7291a1 on 2025-12-10 13:35:22 +0000)
% CaDiCaL version: 2.1.3
% Termination reason: Refutation
% Time elapsed: 0.034 s
% Peak memory usage: 21 MB
% Instructions burned: 196 (million)
% ------------------------------
% ------------------------------
% Success in time 0.6 s
line 1:69 missing ')' at ','
line 1:95 extraneous input ')' expecting ').'
Bindings:
[Organism]
Binding map:
{}
Proof steps:
10
INFO [TheoremProverController.main()] Query Result: Vampire (CASC): Theorem in 611ms
INFO [TPTPGenerationManager.rebuildAxiomKey()] axiomKey rebuilt in 1.783 seconds — 15017 entries
KButilities.shutDownExecutorService(): Initiating executor shutdown
KButilities.shutDownExecutorService(): ExecutorService shutdown complete
When running the following vampire proof we see that it gets syntax errors for parenthesis in TPTP3ProofProcessor.parseProofOutput():
line 1:69 missing ')' at ','
line 1:95 extraneous input ')' expecting ').'
Needs further investigation. I could not reproduce the issue on my machine.
Below are the full logs with the errors:
(base) apease@apease-ThinkPad-L14-Gen-1:~/workspace/sigmakee$ java -cp build/classes:lib/* com.articulate.sigma.tp.TheoremProverController -v "(subclass ?x Object)"
TheoremProverController.main({v=[(subclass ?x Object)]})
[KButilities] SIGMA_HOME set to /home/apease/.sigmakee
INFO [KBmanager.initializeOnce()] Initializing KBmanager!
INFO [KBmanager.initializeOnce()] Loading English Lexicons...
INFO [WordNet.initOnce()] Loaded 117659 word senses in 1.524675103 seconds!
INFO [OMWordnet.readOMWfiles()] Loaded Serialized OMW Files in 0.39765021 seconds!
ERROR [VerbNet.readVerbFiles()] no such dir:
INFO [KBmanager.initializeOnce()] Loading from serialized cache...
INFO [KBmanager.initializeOnce()] Building SUMO Term Taxonomy...
INFO [KBmanager.initializeOnce()] Starting TPTP Background Generation...
INFO [KBmanager.cleanupOrphanedSessionDirectories()] No orphaned session directories found
INFO [KBmanager.initializeOnce()] Initialization completed in 2.554553511 seconds!
ATPQuery(VAMPIRE, CUSTOM, FOF, CASC)INFO [TPTPGenerationManager.lambda$startBackgroundGeneration$1()] SUMO.tptp is current! rebuilding axiomKey for incremental patching
INFO [TPTPGenerationManager.generateTHFPlain()] SUMO_plain.thf exists and is current!
INFO [TPTPGenerationManager.generateTHFModal()] SUMO_modal.thf exists and is current:
INFO [TPTPGenerationManager.lambda$startBackgroundGeneration$4()] SUMO_plain.thf generated in 0.016 seconds!
INFO [TPTPGenerationManager.lambda$startBackgroundGeneration$3()] SUMO_modal.thf generated in 0.016 seconds!
Vampire(SUMO, FOF, CASC, false, 30, 1, null)INFO [TPTPGenerationManager.lambda$startBackgroundGeneration$2()] SUMO.tff is current!
VAMPIRE LANGUAGE: fof
Vampire.askVampire((subclass ?x Object))
Vampire.run(SUMO.tptp, [fof(query_0,conjecture,(( ? [V__x] : (s__subclass(V__x,s__Object) ) ))).])
Vampire.getUserAssertions(SUMO, null)
Vampire.writeStatements([fof(query_0,conjecture,(( ? [V__x] : (s__subclass(V__x,s__Object) ) ))).])
Vampire.concatFiles(/home/apease/.sigmakee/KBs/SUMO.tptp, /home/apease/.sigmakee/KBs/temp-stmt.tptp, /home/apease/.sigmakee/KBs/temp-comb.tptp)INFO [SUMOKBtoTPTPKB.tWriteFile()] FormulaAST=48965/48965 expr!=null=48965 totalASTtranslated=48965 (cold=true)
Vampire.run(temp-comb.tptp)
Vampire.createCommandList(temp-comb.tptp)Vampire.run(): command: /home/apease/Programs/vampire/vampire --output_axiom_names on --proof tptp --mode casc -qa plain -t 30 /home/apease/.sigmakee/KBs/temp-comb.tptp
INFO [SUMOKBtoTPTPKB.translateOneFormula()] Using EXPR path for formula=(subclass Organism OrganicObject)
TheoremProverController.main(): Summary=
Vampire (CASC): Theorem in 611ms
Raw prover output:
% Running in auto input_syntax mode. Trying TPTP
% Detected formulas, will run a generic FOF schedule.
% lrs+1011_32_sil=2000:tgt=full:alpa=true:random_seed=3749040290:st=5:i=107:sd=1:qa=plain:ss=included:er=filter_296 on temp-comb for (296ds/107Mi)
% Instruction limit reached!
% ------------------------------
% Version: Vampire 5.0.0 (Release build, commit 84e7291a1 on 2025-12-10 13:35:22 +0000)
% CaDiCaL version: 2.1.3
% Termination reason: Instruction limit
% Termination phase: Property scanning
% Time elapsed: 0.029 s
% Peak memory usage: 17 MB
% Instructions burned: 109 (million)
% lrs+10_2:3_to=lpo:sil=16000:sp=arity:random_seed=2245284825:i=114:bd=all:qa=plain:ss=axioms:sgt=4_296 on temp-comb for (296ds/114Mi)
% Instruction limit reached!
% ------------------------------
% Version: Vampire 5.0.0 (Release build, commit 84e7291a1 on 2025-12-10 13:35:22 +0000)
% CaDiCaL version: 2.1.3
% Termination reason: Instruction limit
% Termination phase: SInE selection
% Time elapsed: 0.030 s
% Peak memory usage: 17 MB
% Instructions burned: 114 (million)
% ott+1011_2_sil=4000:lsd=20:rnwc=on:rp=on:sac=on:newcnf=on:random_seed=1142691385:i=132:kws=arity:qa=plain:er=filter_296 on temp-comb for (296ds/132Mi)
% Instruction limit reached!
% ------------------------------
% Version: Vampire 5.0.0 (Release build, commit 84e7291a1 on 2025-12-10 13:35:22 +0000)
% CaDiCaL version: 2.1.3
% Termination reason: Instruction limit
% Termination phase: Preprocessing 1
% Time elapsed: 0.035 s
% Peak memory usage: 17 MB
% Instructions burned: 132 (million)
% dis+1011_1_slsqr=8,1:sil=2000:spb=units:fd=off:kmz=on:flr=on:sac=on:slsq=on:random_seed=1016059282:st=2:i=121:sd=30:aac=none:ep=RS:qa=plain:ss=axioms:sgt=10_295 on temp-comb for (295ds/121Mi)
% Instruction limit reached!
% ------------------------------
% Version: Vampire 5.0.0 (Release build, commit 84e7291a1 on 2025-12-10 13:35:22 +0000)
% CaDiCaL version: 2.1.3
% Termination reason: Instruction limit
% Termination phase: SInE selection
% Time elapsed: 0.032 s
% Peak memory usage: 17 MB
% Instructions burned: 122 (million)
% lrs+10_1_sil=2000:sos=on:random_seed=4141339551:i=135:sd=2:qa=plain:gtg=position:ss=axioms_295 on temp-comb for (295ds/135Mi)
% Instruction limit reached!
% ------------------------------
% Version: Vampire 5.0.0 (Release build, commit 84e7291a1 on 2025-12-10 13:35:22 +0000)
% CaDiCaL version: 2.1.3
% Termination reason: Instruction limit
% Termination phase: Property scanning
% Time elapsed: 0.034 s
% Peak memory usage: 17 MB
% Instructions burned: 136 (million)
% lrs+1011_1_sil=16000:random_seed=346586930:i=269:sd=10:qa=plain:ss=axioms:sgt=16_295 on temp-comb for (295ds/269Mi)
% Refutation not found, incomplete strategy
% ------------------------------
% Version: Vampire 5.0.0 (Release build, commit 84e7291a1 on 2025-12-10 13:35:22 +0000)
% CaDiCaL version: 2.1.3
% Termination reason: Refutation not found, incomplete strategy
% Time elapsed: 0.028 s
% Peak memory usage: 20 MB
% Instructions burned: 164 (million)
% ------------------------------
% ------------------------------
% dis+1010_4_sil=2000:sos=on:sac=on:random_seed=252885651:i=140:sd=1:qa=plain:ss=axioms_294 on temp-comb for (294ds/140Mi)
% Instruction limit reached!
% ------------------------------
% Version: Vampire 5.0.0 (Release build, commit 84e7291a1 on 2025-12-10 13:35:22 +0000)
% CaDiCaL version: 2.1.3
% Termination reason: Instruction limit
% Termination phase: SInE selection
% Time elapsed: 0.023 s
% Peak memory usage: 17 MB
% Instructions burned: 143 (million)
% ott+11_4:1_bsr=on:slsqr=8,1:to=kbo:sil=4000:spb=goal:slsq=on:random_seed=3285244069:s2pl=on:st=3:s2a=on:i=124:gtgl=4:sd=1:kws=inv_arity:ep=RST:qa=plain:gtg=position:ss=axioms:fsd=on_294 on temp-comb for (294ds/124Mi)
% Instruction limit reached!
% ------------------------------
% Version: Vampire 5.0.0 (Release build, commit 84e7291a1 on 2025-12-10 13:35:22 +0000)
% CaDiCaL version: 2.1.3
% Termination reason: Instruction limit
% Termination phase: Property scanning
% Time elapsed: 0.019 s
% Peak memory usage: 17 MB
% Instructions burned: 129 (million)
% ott+1010_1_to=lpo:sil=32000:fde=none:sos=on:spb=goal_then_units:urr=on:random_seed=4266080600:st=2.5:cts=off:i=297:sd=4:ins=10:qa=plain:gsp=on:ss=axioms_294 on temp-comb for (294ds/297Mi)
% SZS answers Tuple [[s__Organism]|_] for temp-comb
% Solution written to "/tmp/vampire-proof-41261"
% Refutation found. Thanks to Tanya!
% SZS status Theorem for temp-comb
% SZS output start Proof for temp-comb
fof(f12995,axiom,(
s__subclass(s__Organism,s__Object)),
file('/home/apease/.sigmakee/KBs/temp-comb.tptp',kb_SUMO_12995)).
fof(f15018,conjecture,(
? [X0] : s__subclass(X0,s__Object)),
file('/home/apease/.sigmakee/KBs/temp-comb.tptp',query_0)).
fof(f15019,negated_conjecture,(
~? [X0] : s__subclass(X0,s__Object)),
inference(negated_conjecture,[status(cth)],[f15018])).
fof(f15020,plain,(
~? [X0] : (s__subclass(X0,s__Object) & ans0(X0))),
inference(answer_literal_injection,[],[f15019])).
fof(f15100,plain,(
! [X0] : (~s__subclass(X0,s__Object) | ~ans0(X0))),
inference(ennf_transformation,[],[f15020])).
fof(f15115,plain,(
( ! [X0] : (~s__subclass(X0,s__Object) | ~ans0(X0)) )),
inference(cnf_transformation,[],[f15100])).
fof(f15116,plain,(
s__subclass(s__Organism,s__Object)),
inference(cnf_transformation,[],[f12995])).
fof(f15249,plain,(
~ans0(s__Organism)),
inference(resolution,[],[f15115,f15116])).
fof(f15250,plain,(
( ! [X0] : (ans0(X0)) )),
introduced(definition,[],[answer_literal_resolver])).
fof(f15251,plain,(
$false),
inference(unit_resulting_resolution,[],[f15249,f15250])).
% SZS output end Proof for temp-comb
% ------------------------------
% Version: Vampire 5.0.0 (Release build, commit 84e7291a1 on 2025-12-10 13:35:22 +0000)
% CaDiCaL version: 2.1.3
% Termination reason: Refutation
% Time elapsed: 0.034 s
% Peak memory usage: 21 MB
% Instructions burned: 196 (million)
% ------------------------------
% ------------------------------
% Success in time 0.6 s
line 1:69 missing ')' at ','
line 1:95 extraneous input ')' expecting ').'
Bindings:
[Organism]
Binding map:
{}
Proof steps:
10
INFO [TheoremProverController.main()] Query Result: Vampire (CASC): Theorem in 611ms
INFO [TPTPGenerationManager.rebuildAxiomKey()] axiomKey rebuilt in 1.783 seconds — 15017 entries
KButilities.shutDownExecutorService(): Initiating executor shutdown
KButilities.shutDownExecutorService(): ExecutorService shutdown complete