%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR060+3 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:44:47 AM UTC 2026
% Result : Theorem 36.07s 10.86s
% Output : Refutation 36.07s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 13
% Syntax : Number of formulae : 54 ( 21 unt; 3 def)
% Number of atoms : 105 ( 6 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 97 ( 46 ~; 38 |; 6 &)
% ( 0 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 19 ( 19 usr; 14 con; 0-4 aty)
% Number of variables : 38 ( 36 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f88,axiom,
genlmt(c_machinelearningspindleheadmt,c_ldscdemonstrationspindleheadmt),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_88) ).
fof(f2393,axiom,
genlmt(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988)),c_translation_0_885),c_machinelearningspindleheadmt),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_2393) ).
fof(f3561,axiom,
! [X0] :
( ( mtvisible(c_currentworlddatacollectormt_nonhomocentric)
& isa(X0,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)) )
=> tptp_9_51(f_relationexistsallfn(X0,c_tptp_9_51,c_tptpcol_16_27189,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)),X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_3561) ).
fof(f3562,axiom,
( mtvisible(c_currentworlddatacollectormt_nonhomocentric)
=> relationexistsall(c_tptp_9_51,c_tptpcol_16_27189,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_3562) ).
fof(f3919,axiom,
! [X0,X1,X2,X3] :
( ( isa(X0,X1)
& relationexistsall(X2,X3,X1) )
=> isa(f_relationexistsallfn(X0,X2,X3,X1),X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_3919) ).
fof(f4103,axiom,
isa(c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_4103) ).
fof(f4124,axiom,
genlmt(c_ldscdemonstrationspindleheadmt,c_currentworlddatacollectormt_nonhomocentric),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_4124) ).
fof(f5691,axiom,
! [X0] :
( isa(X0,c_tptpcol_16_27189)
=> tptpcol_16_27189(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_5691) ).
fof(f7997,axiom,
! [X0,X1] :
( ( mtvisible(X0)
& genlmt(X0,X1) )
=> mtvisible(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_7997) ).
fof(f8006,conjecture,
? [X0] :
( mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988)),c_translation_0_885))
=> ( tptp_9_51(X0,c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802)
& tptpcol_16_27189(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',query160) ).
fof(f8007,negated_conjecture,
~ ? [X0] :
( mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988)),c_translation_0_885))
=> ( tptp_9_51(X0,c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802)
& tptpcol_16_27189(X0) ) ),
inference(negated_conjecture,[status(cth)],[f8006]) ).
fof(f10161,plain,
! [X0] :
( tptp_9_51(f_relationexistsallfn(X0,c_tptp_9_51,c_tptpcol_16_27189,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)),X0)
| ~ mtvisible(c_currentworlddatacollectormt_nonhomocentric)
| ~ isa(X0,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)) ),
inference(ennf_transformation,[],[f3561]) ).
fof(f10162,plain,
! [X0] :
( tptp_9_51(f_relationexistsallfn(X0,c_tptp_9_51,c_tptpcol_16_27189,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)),X0)
| ~ mtvisible(c_currentworlddatacollectormt_nonhomocentric)
| ~ isa(X0,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)) ),
inference(flattening,[],[f10161]) ).
fof(f10163,plain,
( relationexistsall(c_tptp_9_51,c_tptpcol_16_27189,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma))
| ~ mtvisible(c_currentworlddatacollectormt_nonhomocentric) ),
inference(ennf_transformation,[],[f3562]) ).
fof(f10300,plain,
! [X0,X1,X2,X3] :
( isa(f_relationexistsallfn(X0,X2,X3,X1),X3)
| ~ isa(X0,X1)
| ~ relationexistsall(X2,X3,X1) ),
inference(ennf_transformation,[],[f3919]) ).
fof(f10301,plain,
! [X0,X1,X2,X3] :
( isa(f_relationexistsallfn(X0,X2,X3,X1),X3)
| ~ isa(X0,X1)
| ~ relationexistsall(X2,X3,X1) ),
inference(flattening,[],[f10300]) ).
fof(f11514,plain,
! [X0] :
( tptpcol_16_27189(X0)
| ~ isa(X0,c_tptpcol_16_27189) ),
inference(ennf_transformation,[],[f5691]) ).
fof(f13390,plain,
! [X0,X1] :
( mtvisible(X1)
| ~ mtvisible(X0)
| ~ genlmt(X0,X1) ),
inference(ennf_transformation,[],[f7997]) ).
fof(f13391,plain,
! [X0,X1] :
( mtvisible(X1)
| ~ mtvisible(X0)
| ~ genlmt(X0,X1) ),
inference(flattening,[],[f13390]) ).
fof(f13400,plain,
! [X0] :
( ( ~ tptp_9_51(X0,c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802)
| ~ tptpcol_16_27189(X0) )
& mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988)),c_translation_0_885)) ),
inference(ennf_transformation,[],[f8007]) ).
fof(f13486,plain,
genlmt(c_machinelearningspindleheadmt,c_ldscdemonstrationspindleheadmt),
inference(cnf_transformation,[],[f88]) ).
fof(f15750,plain,
genlmt(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988)),c_translation_0_885),c_machinelearningspindleheadmt),
inference(cnf_transformation,[],[f2393]) ).
fof(f16902,plain,
! [X0] :
( tptp_9_51(f_relationexistsallfn(X0,c_tptp_9_51,c_tptpcol_16_27189,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)),X0)
| ~ mtvisible(c_currentworlddatacollectormt_nonhomocentric)
| ~ isa(X0,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)) ),
inference(cnf_transformation,[],[f10162]) ).
fof(f16903,plain,
( relationexistsall(c_tptp_9_51,c_tptpcol_16_27189,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma))
| ~ mtvisible(c_currentworlddatacollectormt_nonhomocentric) ),
inference(cnf_transformation,[],[f10163]) ).
fof(f17255,plain,
! [X2,X3,X0,X1] :
( isa(f_relationexistsallfn(X0,X2,X3,X1),X3)
| ~ isa(X0,X1)
| ~ relationexistsall(X2,X3,X1) ),
inference(cnf_transformation,[],[f10301]) ).
fof(f17433,plain,
isa(c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)),
inference(cnf_transformation,[],[f4103]) ).
fof(f17454,plain,
genlmt(c_ldscdemonstrationspindleheadmt,c_currentworlddatacollectormt_nonhomocentric),
inference(cnf_transformation,[],[f4124]) ).
fof(f18809,plain,
! [X0] :
( ~ isa(X0,c_tptpcol_16_27189)
| tptpcol_16_27189(X0) ),
inference(cnf_transformation,[],[f11514]) ).
fof(f20678,plain,
! [X0,X1] :
( ~ genlmt(X0,X1)
| ~ mtvisible(X0)
| mtvisible(X1) ),
inference(cnf_transformation,[],[f13391]) ).
fof(f20687,plain,
mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988)),c_translation_0_885)),
inference(cnf_transformation,[],[f13400]) ).
fof(f20688,plain,
! [X0] :
( ~ tptp_9_51(X0,c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802)
| ~ tptpcol_16_27189(X0) ),
inference(cnf_transformation,[],[f13400]) ).
fof(f20689,definition,
sF0 = f_urlfn(s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f20690,plain,
f_urlfn(s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988) = sF0,
inference(reorient_equations,[],[f20689]) ).
fof(f20691,definition,
sF1 = f_urlreferentfn(sF0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f20692,plain,
f_urlreferentfn(sF0) = sF1,
inference(reorient_equations,[],[f20691]) ).
fof(f20693,definition,
sF2 = f_contentmtofcdafromeventfn(sF1,c_translation_0_885),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f20694,plain,
f_contentmtofcdafromeventfn(sF1,c_translation_0_885) = sF2,
inference(reorient_equations,[],[f20693]) ).
fof(f20695,plain,
mtvisible(sF2),
inference(definition_folding,[],[f20687,f20694,f20692,f20690]) ).
fof(f31859,plain,
( ~ mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988)),c_translation_0_885))
| mtvisible(c_machinelearningspindleheadmt) ),
inference(resolution,[],[f20678,f15750]) ).
fof(f32140,plain,
( ~ mtvisible(c_ldscdemonstrationspindleheadmt)
| mtvisible(c_currentworlddatacollectormt_nonhomocentric) ),
inference(resolution,[],[f20678,f17454]) ).
fof(f32147,plain,
( ~ mtvisible(c_machinelearningspindleheadmt)
| mtvisible(c_ldscdemonstrationspindleheadmt) ),
inference(resolution,[],[f20678,f13486]) ).
fof(f33028,plain,
( ~ mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(sF0),c_translation_0_885))
| mtvisible(c_machinelearningspindleheadmt) ),
inference(forward_demodulation,[],[f31859,f20690]) ).
fof(f33031,plain,
( ~ mtvisible(f_contentmtofcdafromeventfn(sF1,c_translation_0_885))
| mtvisible(c_machinelearningspindleheadmt) ),
inference(forward_demodulation,[],[f33028,f20692]) ).
fof(f33032,plain,
( ~ mtvisible(sF2)
| mtvisible(c_machinelearningspindleheadmt) ),
inference(forward_demodulation,[],[f33031,f20694]) ).
fof(f33033,plain,
mtvisible(c_machinelearningspindleheadmt),
inference(forward_subsumption_resolution,[],[f33032,f20695]) ).
fof(f38808,plain,
! [X2,X0,X1] :
( tptpcol_16_27189(f_relationexistsallfn(X0,X2,c_tptpcol_16_27189,X1))
| ~ relationexistsall(X2,c_tptpcol_16_27189,X1)
| ~ isa(X0,X1) ),
inference(resolution,[],[f17255,f18809]) ).
fof(f40597,plain,
( ~ mtvisible(c_currentworlddatacollectormt_nonhomocentric)
| ~ isa(c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma))
| ~ tptpcol_16_27189(f_relationexistsallfn(c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802,c_tptp_9_51,c_tptpcol_16_27189,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma))) ),
inference(resolution,[],[f16902,f20688]) ).
fof(f40600,plain,
( ~ tptpcol_16_27189(f_relationexistsallfn(c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802,c_tptp_9_51,c_tptpcol_16_27189,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)))
| ~ mtvisible(c_currentworlddatacollectormt_nonhomocentric) ),
inference(forward_subsumption_resolution,[],[f40597,f17433]) ).
fof(f57762,plain,
mtvisible(c_ldscdemonstrationspindleheadmt),
inference(resolution,[],[f32147,f33033]) ).
fof(f57765,plain,
mtvisible(c_currentworlddatacollectormt_nonhomocentric),
inference(resolution,[],[f57762,f32140]) ).
fof(f116210,plain,
( ~ relationexistsall(c_tptp_9_51,c_tptpcol_16_27189,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma))
| ~ isa(c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma))
| ~ mtvisible(c_currentworlddatacollectormt_nonhomocentric) ),
inference(resolution,[],[f38808,f40600]) ).
fof(f116213,plain,
( ~ isa(c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma))
| ~ mtvisible(c_currentworlddatacollectormt_nonhomocentric) ),
inference(forward_subsumption_resolution,[],[f116210,f16903]) ).
fof(f116214,plain,
~ mtvisible(c_currentworlddatacollectormt_nonhomocentric),
inference(forward_subsumption_resolution,[],[f116213,f17433]) ).
fof(f116215,plain,
$false,
inference(forward_subsumption_resolution,[],[f116214,f57765]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR060+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.18 % Computer : n003.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 22:22:58 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.22 Running first-order model finding
% 0.08/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 27.40/4.28 % (2098444)Will run a generic schedule for satisfiability detection.
% 27.40/4.28 % (2098449)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1632256434_2998 on theBenchmark for (2998ds/0Mi)
% 27.40/4.28 % (2098450)% WARNING: option uhcvi not known.
% 27.40/4.28 % (2098450)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3438769079:i=135531:add=off:rawr=on_2998 on theBenchmark for (2998ds/135531Mi)
% 27.40/4.28 % (2098451)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3109928854:i=88024:add=on:rawr=on_2998 on theBenchmark for (2998ds/88024Mi)
% 27.40/4.28 % (2098452)dis+10_1_sil=32000:sp=arity:random_seed=2607620560:i=103:fgj=on_2998 on theBenchmark for (2998ds/103Mi)
% 27.40/4.28 % (2098453)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1670836531:i=116_2998 on theBenchmark for (2998ds/116Mi)
% 27.40/4.28 % (2098454)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=38463725:i=131_2998 on theBenchmark for (2998ds/131Mi)
% 27.40/4.28 % (2098455)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=8333146:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2998 on theBenchmark for (2998ds/159Mi)
% 27.40/4.28 % (2098452)Instruction limit reached!
% 27.40/4.28 % (2098452)------------------------------
% 27.40/4.28 % (2098452)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.40/4.28 % (2098452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.40/4.28 % (2098452)CaDiCaL version: 2.1.3
% 27.40/4.28 % (2098452)Termination reason: Instruction limit
% 27.40/4.28 % (2098452)Termination phase: Saturation
% 27.40/4.28 % (2098452)Time elapsed: 0.062 s
% 27.40/4.28 % (2098452)Peak memory usage: 22 MB
% 27.40/4.28 % (2098452)Instructions burned: 104 (million)
% 27.40/4.28 % (2098454)Instruction limit reached!
% 27.40/4.28 % (2098454)------------------------------
% 27.40/4.28 % (2098454)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.40/4.28 % (2098454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.40/4.28 % (2098454)CaDiCaL version: 2.1.3
% 27.40/4.28 % (2098454)Termination reason: Instruction limit
% 27.40/4.28 % (2098454)Termination phase: Saturation
% 27.40/4.28 % (2098454)Time elapsed: 0.076 s
% 27.40/4.28 % (2098454)Peak memory usage: 23 MB
% 27.40/4.28 % (2098454)Instructions burned: 133 (million)
% 27.40/4.28 % (2098463)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=671955792:i=714:nm=2_2997 on theBenchmark for (2997ds/714Mi)
% 27.40/4.28 % (2098453)Instruction limit reached!
% 27.40/4.28 % (2098453)------------------------------
% 27.40/4.28 % (2098453)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.40/4.28 % (2098453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.40/4.28 % (2098453)CaDiCaL version: 2.1.3
% 27.40/4.28 % (2098453)Termination reason: Instruction limit
% 27.40/4.28 % (2098453)Termination phase: Blocked clause elimination
% 27.40/4.28 % (2098453)Time elapsed: 0.105 s
% 27.40/4.28 % (2098453)Peak memory usage: 23 MB
% 27.40/4.28 % (2098453)Instructions burned: 117 (million)
% 27.40/4.28 % (2098455)Instruction limit reached!
% 27.40/4.28 % (2098455)------------------------------
% 27.40/4.28 % (2098455)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.40/4.28 % (2098455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.40/4.28 % (2098455)CaDiCaL version: 2.1.3
% 27.40/4.28 % (2098455)Termination reason: Instruction limit
% 27.40/4.28 % (2098455)Termination phase: Saturation
% 27.40/4.28 % (2098455)Time elapsed: 0.110 s
% 27.40/4.28 % (2098455)Peak memory usage: 25 MB
% 27.40/4.28 % (2098455)Instructions burned: 159 (million)
% 27.40/4.28 % (2098464)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2131482439:i=131:bd=preordered:fsd=on_2997 on theBenchmark for (2997ds/131Mi)
% 27.40/4.28 % TRYING [1]
% 27.40/4.28 % (2098466)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3312916327:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2997 on theBenchmark for (2997ds/684Mi)
% 27.40/4.28 % (2098467)ott-21_1_sil=16000:fs=off:random_seed=3080660976:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 27.40/4.28 % TRYING [2]
% 27.40/4.28 % TRYING [3]
% 27.40/4.28 % (2098464)Instruction limit reached!
% 27.40/4.28 % (2098464)------------------------------
% 27.40/4.28 % (2098464)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.40/4.28 % (2098464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.07/10.86 % (2098464)CaDiCaL version: 2.1.3
% 36.07/10.86 % (2098464)Termination reason: Instruction limit
% 36.07/10.86 % (2098464)Termination phase: Blocked clause elimination
% 36.07/10.86 % (2098464)Time elapsed: 0.111 s
% 36.07/10.86 % (2098464)Peak memory usage: 23 MB
% 36.07/10.86 % (2098464)Instructions burned: 131 (million)
% 36.07/10.86 % (2098467)Instruction limit reached!
% 36.07/10.86 % (2098467)------------------------------
% 36.07/10.86 % (2098467)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.07/10.86 % (2098467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.07/10.86 % (2098467)CaDiCaL version: 2.1.3
% 36.07/10.86 % (2098467)Termination reason: Instruction limit
% 36.07/10.86 % (2098467)Termination phase: Saturation
% 36.07/10.86 % (2098467)Time elapsed: 0.097 s
% 36.07/10.86 % (2098467)Peak memory usage: 23 MB
% 36.07/10.86 % (2098467)Instructions burned: 180 (million)
% 36.07/10.86 % TRYING [4]
% 36.07/10.86 % (2098471)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4218395291:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 36.07/10.86 % (2098472)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3387585589:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 36.07/10.86 % TRYING [1]
% 36.07/10.86 % TRYING [2]
% 36.07/10.86 % TRYING [3]
% 36.07/10.86 % TRYING [5]
% 36.07/10.86 % (2098463)Instruction limit reached!
% 36.07/10.86 % (2098463)------------------------------
% 36.07/10.86 % (2098463)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.07/10.86 % (2098463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.07/10.86 % (2098463)CaDiCaL version: 2.1.3
% 36.07/10.86 % (2098463)Termination reason: Instruction limit
% 36.07/10.86 % (2098463)Termination phase: Finite model building constraint generation
% 36.07/10.86 % (2098463)Time elapsed: 0.338 s
% 36.07/10.86 % (2098463)Peak memory usage: 40 MB
% 36.07/10.86 % (2098463)Instructions burned: 715 (million)
% 36.07/10.86 % (2098475)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1146201506:i=1179_2994 on theBenchmark for (2994ds/1179Mi)
% 36.07/10.86 % TRYING [1]
% 36.07/10.86 % (2098471)Instruction limit reached!
% 36.07/10.86 % (2098471)------------------------------
% 36.07/10.86 % (2098471)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.07/10.86 % (2098471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.07/10.86 % (2098471)CaDiCaL version: 2.1.3
% 36.07/10.86 % (2098471)Termination reason: Instruction limit
% 36.07/10.86 % (2098471)Termination phase: Saturation
% 36.07/10.86 % (2098471)Time elapsed: 0.242 s
% 36.07/10.86 % (2098471)Peak memory usage: 27 MB
% 36.07/10.86 % (2098471)Instructions burned: 479 (million)
% 36.07/10.86 % (2098466)Instruction limit reached!
% 36.07/10.86 % (2098466)------------------------------
% 36.07/10.86 % (2098466)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.07/10.86 % (2098466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.07/10.86 % (2098466)CaDiCaL version: 2.1.3
% 36.07/10.86 % (2098466)Termination reason: Instruction limit
% 36.07/10.86 % (2098466)Termination phase: Saturation
% 36.07/10.86 % (2098466)Time elapsed: 0.378 s
% 36.07/10.86 % (2098466)Peak memory usage: 35 MB
% 36.07/10.86 % (2098466)Instructions burned: 684 (million)
% 36.07/10.86 % (2098480)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=570433675:i=889:ins=1_2993 on theBenchmark for (2993ds/889Mi)
% 36.07/10.86 % (2098482)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=3192929195:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2993 on theBenchmark for (2993ds/692Mi)
% 36.07/10.86 % TRYING [2]
% 36.07/10.86 % (2098472)Instruction limit reached!
% 36.07/10.86 % (2098472)------------------------------
% 36.07/10.86 % (2098472)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.07/10.86 % (2098472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.07/10.86 % (2098472)CaDiCaL version: 2.1.3
% 36.07/10.86 % (2098472)Termination reason: Instruction limit
% 36.07/10.86 % (2098472)Termination phase: Finite model building SAT solving
% 36.07/10.86 % (2098472)Time elapsed: 0.539 s
% 36.07/10.86 % (2098472)Peak memory usage: 41 MB
% 36.07/10.86 % (2098472)Instructions burned: 866 (million)
% 36.07/10.86 % (2098494)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=4094904700:i=879:kws=inv_precedence:fsr=off_2990 on theBenchmark for (2990ds/879Mi)
% 36.07/10.86 % TRYING [6]
% 36.07/10.86 % (2098482)Instruction limit reached!
% 36.07/10.86 % (2098482)------------------------------
% 36.07/10.86 % (2098482)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.07/10.86 % (2098482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.07/10.86 % (2098482)CaDiCaL version: 2.1.3
% 36.07/10.86 % (2098482)Termination reason: Instruction limit
% 36.07/10.86 % (2098482)Termination phase: Saturation
% 36.07/10.86 % (2098482)Time elapsed: 0.617 s
% 36.07/10.86 % (2098482)Peak memory usage: 39 MB
% 36.07/10.86 % (2098482)Instructions burned: 692 (million)
% 36.07/10.86 % (2098503)fmb+10_1_sil=64000:random_seed=1258987696:i=22061:nm=2:gsp=on_2986 on theBenchmark for (2986ds/22061Mi)
% 36.07/10.86 % (2098480)Instruction limit reached!
% 36.07/10.86 % (2098480)------------------------------
% 36.07/10.86 % (2098480)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.07/10.86 % (2098480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.07/10.86 % (2098480)CaDiCaL version: 2.1.3
% 36.07/10.86 % (2098480)Termination reason: Instruction limit
% 36.07/10.86 % (2098480)Termination phase: Finite model building constraint generation
% 36.07/10.86 % (2098480)Time elapsed: 0.804 s
% 36.07/10.86 % (2098480)Peak memory usage: 91 MB
% 36.07/10.86 % (2098480)Instructions burned: 889 (million)
% 36.07/10.86 % (2098508)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3520099009:i=9515:nm=5_2984 on theBenchmark for (2984ds/9515Mi)
% 36.07/10.86 % (2098494)Instruction limit reached!
% 36.07/10.86 % (2098494)------------------------------
% 36.07/10.86 % (2098494)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.07/10.86 % (2098494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.07/10.86 % (2098494)CaDiCaL version: 2.1.3
% 36.07/10.86 % (2098494)Termination reason: Instruction limit
% 36.07/10.86 % (2098494)Termination phase: Saturation
% 36.07/10.86 % (2098494)Time elapsed: 0.547 s
% 36.07/10.86 % (2098494)Peak memory usage: 32 MB
% 36.07/10.86 % (2098494)Instructions burned: 879 (million)
% 36.07/10.86 % (2098510)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1046445973:fmbsr=1.7:i=920_2984 on theBenchmark for (2984ds/920Mi)
% 36.07/10.86 % (2098475)Instruction limit reached!
% 36.07/10.86 % (2098475)------------------------------
% 36.07/10.86 % (2098475)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.07/10.86 % (2098475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.07/10.86 % (2098475)CaDiCaL version: 2.1.3
% 36.07/10.86 % (2098475)Termination reason: Instruction limit
% 36.07/10.86 % (2098475)Termination phase: Saturation
% 36.07/10.86 % (2098475)Time elapsed: 1.050 s
% 36.07/10.86 % (2098475)Peak memory usage: 44 MB
% 36.07/10.86 % (2098475)Instructions burned: 1179 (million)
% 36.07/10.86 % (2098513)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=4012662048:i=5131_2983 on theBenchmark for (2983ds/5131Mi)
% 36.07/10.86 % TRYING [1]
% 36.07/10.86 % TRYING [2]
% 36.07/10.86 % TRYING [20]
% 36.07/10.86 % TRYING [8]
% 36.07/10.86 % TRYING [7]
% 36.07/10.86 % TRYING [3]
% 36.07/10.86 % (2098510)Instruction limit reached!
% 36.07/10.86 % (2098510)------------------------------
% 36.07/10.86 % (2098510)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.07/10.86 % (2098510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.07/10.86 % (2098510)CaDiCaL version: 2.1.3
% 36.07/10.86 % (2098510)Termination reason: Instruction limit
% 36.07/10.86 % (2098510)Termination phase: Finite model building constraint generation
% 36.07/10.86 % (2098510)Time elapsed: 0.679 s
% 36.07/10.86 % (2098510)Peak memory usage: 60 MB
% 36.07/10.86 % (2098510)Instructions burned: 922 (million)
% 36.07/10.86 % (2098524)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3829445419:i=1472:ins=7:fdi=8:gsp=on_2977 on theBenchmark for (2977ds/1472Mi)
% 36.07/10.86 % TRYING [4]
% 36.07/10.86 % (2098524)Instruction limit reached!
% 36.07/10.86 % (2098524)------------------------------
% 36.07/10.86 % (2098524)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.07/10.86 % (2098524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.07/10.86 % (2098524)CaDiCaL version: 2.1.3
% 36.07/10.86 % (2098524)Termination reason: Instruction limit
% 36.07/10.86 % (2098524)Termination phase: Saturation
% 36.07/10.86 % (2098524)Time elapsed: 1.286 s
% 36.07/10.86 % (2098524)Peak memory usage: 48 MB
% 36.07/10.86 % (2098524)Instructions burned: 1472 (million)
% 36.07/10.86 % (2098534)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2468826709:i=6324_2963 on theBenchmark for (2963ds/6324Mi)
% 36.07/10.86 % (2098534)Cannot represent all propositional literals internally
% 36.07/10.86 % (2098534)Refutation not found, incomplete strategy
% 36.07/10.86 % (2098534)------------------------------
% 36.07/10.86 % (2098534)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.07/10.86 % (2098534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.07/10.86 % (2098534)CaDiCaL version: 2.1.3
% 36.07/10.86 % (2098534)Termination reason: Refutation not found, incomplete strategy
% 36.07/10.86 % (2098534)Time elapsed: 0.402 s
% 36.07/10.86 % (2098534)Peak memory usage: 29 MB
% 36.07/10.86 % (2098534)Instructions burned: 438 (million)
% 36.07/10.86 % (2098534)------------------------------
% 36.07/10.86 % (2098534)------------------------------
% 36.07/10.86 % (2098539)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3252613828:fmbsr=2.30978:i=2174_2959 on theBenchmark for (2959ds/2174Mi)
% 36.07/10.86 % TRYING [16]
% 36.07/10.86 % TRYING [8]
% 36.07/10.86 % (2098539)Instruction limit reached!
% 36.07/10.86 % (2098539)------------------------------
% 36.07/10.86 % (2098539)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.07/10.86 % (2098539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.07/10.86 % (2098539)CaDiCaL version: 2.1.3
% 36.07/10.86 % (2098539)Termination reason: Instruction limit
% 36.07/10.86 % (2098539)Termination phase: Finite model building constraint generation
% 36.07/10.86 % (2098539)Time elapsed: 1.407 s
% 36.07/10.86 % (2098539)Peak memory usage: 121 MB
% 36.07/10.86 % (2098539)Instructions burned: 2175 (million)
% 36.07/10.86 % (2098547)ott-2_1_sil=16000:newcnf=on:random_seed=1309710885:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2944 on theBenchmark for (2944ds/869Mi)
% 36.07/10.86 % (2098513)Instruction limit reached!
% 36.07/10.86 % (2098513)------------------------------
% 36.07/10.86 % (2098513)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.07/10.86 % (2098513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.07/10.86 % (2098513)CaDiCaL version: 2.1.3
% 36.07/10.86 % (2098513)Termination reason: Instruction limit
% 36.07/10.86 % (2098513)Termination phase: Saturation
% 36.07/10.86 % (2098513)Time elapsed: 4.502 s
% 36.07/10.86 % (2098513)Peak memory usage: 115 MB
% 36.07/10.86 % (2098513)Instructions burned: 5131 (million)
% 36.07/10.86 % (2098547)Instruction limit reached!
% 36.07/10.86 % (2098547)------------------------------
% 36.07/10.86 % (2098547)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.07/10.86 % (2098547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.07/10.86 % (2098547)CaDiCaL version: 2.1.3
% 36.07/10.86 % (2098547)Termination reason: Instruction limit
% 36.07/10.86 % (2098547)Termination phase: Saturation
% 36.07/10.86 % (2098547)Time elapsed: 0.672 s
% 36.07/10.86 % (2098547)Peak memory usage: 43 MB
% 36.07/10.86 % (2098547)Instructions burned: 869 (million)
% 36.07/10.86 % (2098553)ott+10_1_sil=32000:tgt=ground:random_seed=2214899421:i=5114:av=off_2937 on theBenchmark for (2937ds/5114Mi)
% 36.07/10.86 % (2098554)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1089381071:i=54282_2937 on theBenchmark for (2937ds/54282Mi)
% 36.07/10.86 % TRYING [1]
% 36.07/10.86 % TRYING [2]
% 36.07/10.86 % TRYING [5]
% 36.07/10.86 % TRYING [3]
% 36.07/10.86 % TRYING [4]
% 36.07/10.86 % TRYING [5]
% 36.07/10.86 % (2098508)Instruction limit reached!
% 36.07/10.86 % (2098508)------------------------------
% 36.07/10.86 % (2098508)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.07/10.86 % (2098508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.07/10.86 % (2098508)CaDiCaL version: 2.1.3
% 36.07/10.86 % (2098508)Termination reason: Instruction limit
% 36.07/10.86 % (2098508)Termination phase: Finite model building constraint generation
% 36.07/10.86 % (2098508)Time elapsed: 6.769 s
% 36.07/10.86 % (2098508)Peak memory usage: 538 MB
% 36.07/10.86 % (2098508)Instructions burned: 9515 (million)
% 36.07/10.86 % (2098565)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1816365047:i=3512:aac=none_2915 on theBenchmark for (2915ds/3512Mi)
% 36.07/10.86 % TRYING [6]
% 36.07/10.86 % (2098553) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2098444-2098553"...
% 36.07/10.86 % (2098553)...printing done.
% 36.07/10.86 % (2098553)Refutation found. Thanks to Tanya!
% 36.07/10.86 % SZS status Theorem for theBenchmark
% 36.07/10.86 % SZS output start Proof for theBenchmark
% See solution above
% 36.07/10.88 % (2098553)------------------------------
% 36.07/10.88 % (2098553)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.07/10.88 % (2098553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.07/10.88 % (2098553)CaDiCaL version: 2.1.3
% 36.07/10.88 % (2098553)Termination reason: Refutation
% 36.07/10.88 % (2098553)Time elapsed: 4.202 s
% 36.07/10.88 % (2098553)Peak memory usage: 68 MB
% 36.07/10.88 % (2098553)Instructions burned: 4657 (million)
% 36.07/10.88 % (2098444)Success in time 10.637 s
% 36.07/10.88 % Vampire exiting
%------------------------------------------------------------------------------