%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CSR060+3 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n019.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:42:27 AM UTC 2026
% Result : Theorem 21.63s 4.85s
% Output : Refutation 26.40s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 17
% Syntax : Number of formulae : 79 ( 25 unt; 7 def)
% Number of atoms : 156 ( 6 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 145 ( 68 ~; 60 |; 6 &)
% ( 4 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 12 ( 10 usr; 5 prp; 0-3 aty)
% Number of functors : 19 ( 19 usr; 14 con; 0-4 aty)
% Number of variables : 40 ( 0 sgn 38 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f943,axiom,
genlmt(c_machinelearningspindleheadmt,c_analystdatabasemt),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_943) ).
fof(f2393,axiom,
genlmt(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988)),c_translation_0_885),c_machinelearningspindleheadmt),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_2393) ).
fof(f2567,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/sandbox/benchmark/theBenchmark.p',ax2_2567) ).
fof(f2568,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/sandbox/benchmark/theBenchmark.p',ax2_2568) ).
fof(f3332,axiom,
genlmt(c_analystdatabasemt,c_currentworlddatacollectormt_nonhomocentric),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_3332) ).
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/sandbox/benchmark/theBenchmark.p',ax2_3919) ).
fof(f4103,axiom,
isa(c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_4103) ).
fof(f5691,axiom,
! [X0] :
( isa(X0,c_tptpcol_16_27189)
=> tptpcol_16_27189(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_5691) ).
fof(f7997,axiom,
! [X0,X1] :
( ( mtvisible(X0)
& genlmt(X0,X1) )
=> mtvisible(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',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/sandbox/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(f9762,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,[],[f2567]) ).
fof(f9763,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,[],[f9762]) ).
fof(f9764,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,[],[f2568]) ).
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(f14325,plain,
genlmt(c_machinelearningspindleheadmt,c_analystdatabasemt),
inference(cnf_transformation,[],[f943]) ).
fof(f15750,plain,
genlmt(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988)),c_translation_0_885),c_machinelearningspindleheadmt),
inference(cnf_transformation,[],[f2393]) ).
fof(f15922,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,[],[f9763]) ).
fof(f15923,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,[],[f9764]) ).
fof(f16677,plain,
genlmt(c_analystdatabasemt,c_currentworlddatacollectormt_nonhomocentric),
inference(cnf_transformation,[],[f3332]) ).
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(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(f20853,definition,
( spl3_36
<=> mtvisible(c_currentworlddatacollectormt_nonhomocentric) ),
introduced(definition,[new_symbols(definition,[spl3_36])],[avatar_definition]) ).
fof(f20855,plain,
( ~ mtvisible(c_currentworlddatacollectormt_nonhomocentric)
| spl3_36 ),
inference(avatar_component_clause,[],[f20853]) ).
fof(f21521,definition,
( spl3_181
<=> relationexistsall(c_tptp_9_51,c_tptpcol_16_27189,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)) ),
introduced(definition,[new_symbols(definition,[spl3_181])],[avatar_definition]) ).
fof(f21523,plain,
( relationexistsall(c_tptp_9_51,c_tptpcol_16_27189,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma))
| ~ spl3_181 ),
inference(avatar_component_clause,[],[f21521]) ).
fof(f21526,definition,
( spl3_182
<=> ! [X0] :
( tptp_9_51(f_relationexistsallfn(X0,c_tptp_9_51,c_tptpcol_16_27189,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)),X0)
| ~ isa(X0,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)) ) ),
introduced(definition,[new_symbols(definition,[spl3_182])],[avatar_definition]) ).
fof(f21527,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)
| ~ isa(X0,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)) )
| ~ spl3_182 ),
inference(avatar_component_clause,[],[f21526]) ).
fof(f22284,plain,
( ~ spl3_36
| spl3_181 ),
inference(avatar_split_clause,[],[f15923,f21521,f20853]) ).
fof(f22285,plain,
( ~ spl3_36
| spl3_182 ),
inference(avatar_split_clause,[],[f15922,f21526,f20853]) ).
fof(f22847,definition,
( spl3_461
<=> mtvisible(c_analystdatabasemt) ),
introduced(definition,[new_symbols(definition,[spl3_461])],[avatar_definition]) ).
fof(f22848,plain,
( mtvisible(c_analystdatabasemt)
| ~ spl3_461 ),
inference(avatar_component_clause,[],[f22847]) ).
fof(f22849,plain,
( ~ mtvisible(c_analystdatabasemt)
| spl3_461 ),
inference(avatar_component_clause,[],[f22847]) ).
fof(f24412,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(f24423,plain,
( ~ mtvisible(c_analystdatabasemt)
| mtvisible(c_currentworlddatacollectormt_nonhomocentric) ),
inference(resolution,[],[f16677,f20678]) ).
fof(f24436,plain,
( ~ mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988)),c_translation_0_885))
| mtvisible(c_machinelearningspindleheadmt) ),
inference(resolution,[],[f15750,f20678]) ).
fof(f24439,plain,
( ~ mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(sF0),c_translation_0_885))
| mtvisible(c_machinelearningspindleheadmt) ),
inference(forward_demodulation,[],[f24436,f20690]) ).
fof(f24441,plain,
( ~ mtvisible(f_contentmtofcdafromeventfn(sF1,c_translation_0_885))
| mtvisible(c_machinelearningspindleheadmt) ),
inference(forward_demodulation,[],[f24439,f20692]) ).
fof(f24442,plain,
( ~ mtvisible(sF2)
| mtvisible(c_machinelearningspindleheadmt) ),
inference(forward_demodulation,[],[f24441,f20694]) ).
fof(f24443,plain,
mtvisible(c_machinelearningspindleheadmt),
inference(forward_subsumption_resolution,[],[f24442,f20695]) ).
fof(f24454,plain,
( ~ mtvisible(c_machinelearningspindleheadmt)
| mtvisible(c_analystdatabasemt) ),
inference(resolution,[],[f14325,f20678]) ).
fof(f24455,plain,
mtvisible(c_analystdatabasemt),
inference(forward_subsumption_resolution,[],[f24454,f24443]) ).
fof(f24456,plain,
( $false
| spl3_461 ),
inference(forward_subsumption_resolution,[],[f24455,f22849]) ).
fof(f24457,plain,
spl3_461,
inference(avatar_contradiction_clause,[],[f24456]) ).
fof(f24458,plain,
( mtvisible(c_currentworlddatacollectormt_nonhomocentric)
| ~ spl3_461 ),
inference(forward_subsumption_resolution,[],[f24423,f22848]) ).
fof(f24461,plain,
( $false
| spl3_36
| ~ spl3_461 ),
inference(forward_subsumption_resolution,[],[f24458,f20855]) ).
fof(f24462,plain,
( spl3_36
| ~ spl3_461 ),
inference(avatar_contradiction_clause,[],[f24461]) ).
fof(f24465,plain,
( ~ 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)))
| ~ spl3_182 ),
inference(resolution,[],[f21527,f20688]) ).
fof(f24466,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)))
| ~ spl3_182 ),
inference(forward_subsumption_resolution,[],[f24465,f17433]) ).
fof(f24467,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))
| ~ spl3_182 ),
inference(resolution,[],[f24466,f24412]) ).
fof(f24468,plain,
( ~ isa(c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma))
| ~ spl3_181
| ~ spl3_182 ),
inference(forward_subsumption_resolution,[],[f24467,f21523]) ).
fof(f24469,plain,
( $false
| ~ spl3_181
| ~ spl3_182 ),
inference(forward_subsumption_resolution,[],[f24468,f17433]) ).
fof(f24470,plain,
( ~ spl3_181
| ~ spl3_182 ),
inference(avatar_contradiction_clause,[],[f24469]) ).
cnf(s286,plain,
( ~ spl3_36
| spl3_181 ),
inference(sat_conversion,[],[f22284]) ).
cnf(s287,plain,
( ~ spl3_36
| spl3_182 ),
inference(sat_conversion,[],[f22285]) ).
cnf(s700,plain,
spl3_461,
inference(sat_conversion,[],[f24457]) ).
cnf(s701,plain,
( spl3_36
| ~ spl3_461 ),
inference(sat_conversion,[],[f24462]) ).
cnf(s703,plain,
( ~ spl3_181
| ~ spl3_182 ),
inference(sat_conversion,[],[f24470]) ).
cnf(s705,plain,
spl3_36,
inference(rat,[],[s701,s700]) ).
cnf(s734,plain,
spl3_182,
inference(rat,[],[s287,s705]) ).
cnf(s735,plain,
~ spl3_181,
inference(rat,[],[s703,s734]) ).
cnf(s736,plain,
$false,
inference(rat,[],[s286,s735,s705]) ).
fof(f24471,plain,
$false,
inference(avatar_sat_refutation,[],[s736]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : CSR060+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.10 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.28/0.31 % Computer : n019.cluster.edu
% 0.28/0.31 % Model : x86_64 x86_64
% 0.28/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.28/0.31 % Memory : 8046.5625MB
% 0.28/0.31 % OS : Linux 6.8.0-71-generic
% 0.28/0.31 % CPULimit : 300
% 0.28/0.31 % WCLimit : 300
% 0.28/0.31 % DateTime : Mon Sep 28 22:21:18 UTC 2026
% 0.28/0.32 % CPUTime :
% 0.28/0.32 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.28/0.38 Running first-order theorem proving
% 0.28/0.38 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 17.17/3.87 % (342750)Detected formulas, will run a generic FOF schedule.
% 17.17/3.87 % (342758)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3262842902:i=109:sd=1:ins=1:gsp=on:ss=axioms_2998 on theBenchmark for (2998ds/109Mi)
% 17.17/3.87 % (342760)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3857514073:s2a=on:i=139:gtg=position_2998 on theBenchmark for (2998ds/139Mi)
% 17.17/3.87 % (342757)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=4292926334:i=141695:sd=1:nm=32:gsp=on:ss=included_2998 on theBenchmark for (2998ds/141695Mi)
% 17.17/3.87 % (342755)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2338547193:i=141193_2998 on theBenchmark for (2998ds/141193Mi)
% 17.17/3.87 % (342759)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=4007436970:i=119:av=off:ss=axioms_2998 on theBenchmark for (2998ds/119Mi)
% 17.17/3.87 % (342761)dis-21_1_sil=8000:lcm=predicate:random_seed=3193088601:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2998 on theBenchmark for (2998ds/129Mi)
% 17.17/3.87 % (342756)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3362585288:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2998 on theBenchmark for (2998ds/134677Mi)
% 17.17/3.87 % (342758)Refutation not found, incomplete strategy
% 17.17/3.87 % (342758)------------------------------
% 17.17/3.87 % (342758)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.17/3.87 % (342758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.17/3.87 % (342758)CaDiCaL version: 2.1.3
% 17.17/3.87 % (342758)Termination reason: Refutation not found, incomplete strategy
% 17.17/3.87 % (342758)Time elapsed: 0.016 s
% 17.17/3.87 % (342758)Peak memory usage: 93 MB
% 17.17/3.87 % (342758)Instructions burned: 24 (million)
% 17.17/3.87 % (342759)Instruction limit reached!
% 17.17/3.87 % (342759)------------------------------
% 17.17/3.87 % (342759)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.17/3.87 % (342759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.17/3.87 % (342759)CaDiCaL version: 2.1.3
% 17.17/3.87 % (342759)Termination reason: Instruction limit
% 17.17/3.87 % (342759)Termination phase: Saturation
% 17.17/3.87 % (342759)Time elapsed: 0.101 s
% 17.17/3.87 % (342759)Peak memory usage: 93 MB
% 17.17/3.87 % (342759)Instructions burned: 119 (million)
% 17.17/3.87 % (342761)Instruction limit reached!
% 17.17/3.87 % (342761)------------------------------
% 17.17/3.87 % (342761)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.17/3.87 % (342761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.17/3.87 % (342761)CaDiCaL version: 2.1.3
% 17.17/3.87 % (342761)Termination reason: Instruction limit
% 17.17/3.87 % (342761)Termination phase: Saturation
% 17.17/3.87 % (342761)Time elapsed: 0.120 s
% 17.17/3.87 % (342761)Peak memory usage: 94 MB
% 17.17/3.87 % (342761)Instructions burned: 129 (million)
% 17.17/3.87 % (342760)Instruction limit reached!
% 17.17/3.87 % (342760)------------------------------
% 17.17/3.87 % (342760)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.17/3.87 % (342760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.17/3.87 % (342760)CaDiCaL version: 2.1.3
% 17.17/3.87 % (342760)Termination reason: Instruction limit
% 17.17/3.87 % (342760)Termination phase: Property scanning
% 17.17/3.87 % (342760)Time elapsed: 0.137 s
% 17.17/3.87 % (342760)Peak memory usage: 92 MB
% 17.17/3.87 % (342760)Instructions burned: 140 (million)
% 17.17/3.87 % (342758)------------------------------
% 17.17/3.87 % (342758)------------------------------
% 17.17/3.87 % (342769)lrs+10_1_sil=8000:sp=occurrence:random_seed=2451443606:i=285:sd=3:ss=axioms:sgt=8_2994 on theBenchmark for (2994ds/285Mi)
% 17.17/3.87 % (342770)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3864294696:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2994 on theBenchmark for (2994ds/157Mi)
% 17.17/3.87 % (342769)Refutation not found, incomplete strategy
% 17.17/3.87 % (342769)------------------------------
% 17.17/3.87 % (342769)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.17/3.87 % (342769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.17/3.87 % (342769)CaDiCaL version: 2.1.3
% 17.17/3.87 % (342769)Termination reason: Refutation not found, incomplete strategy
% 21.63/4.85 % (342769)Time elapsed: 0.027 s
% 21.63/4.85 % (342769)Peak memory usage: 94 MB
% 21.63/4.85 % (342769)Instructions burned: 21 (million)
% 21.63/4.85 % (342771)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1215343843:i=325:sd=1:ss=axioms:sgt=32_2994 on theBenchmark for (2994ds/325Mi)
% 21.63/4.85 % (342771)Refutation not found, incomplete strategy
% 21.63/4.85 % (342771)------------------------------
% 21.63/4.85 % (342771)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.63/4.85 % (342771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.63/4.85 % (342771)CaDiCaL version: 2.1.3
% 21.63/4.85 % (342771)Termination reason: Refutation not found, incomplete strategy
% 21.63/4.85 % (342771)Time elapsed: 0.026 s
% 21.63/4.85 % (342771)Peak memory usage: 94 MB
% 21.63/4.85 % (342771)Instructions burned: 20 (million)
% 21.63/4.85 % (342770)Refutation not found, incomplete strategy
% 21.63/4.85 % (342770)------------------------------
% 21.63/4.85 % (342770)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.63/4.85 % (342770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.63/4.85 % (342770)CaDiCaL version: 2.1.3
% 21.63/4.85 % (342770)Termination reason: Refutation not found, incomplete strategy
% 21.63/4.85 % (342770)Time elapsed: 0.053 s
% 21.63/4.85 % (342770)Peak memory usage: 94 MB
% 21.63/4.85 % (342770)Instructions burned: 57 (million)
% 21.63/4.85 % (342772)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=2648655002:s2a=on:i=248:s2at=1.23:gtg=position_2993 on theBenchmark for (2993ds/248Mi)
% 21.63/4.85 % (342772)Instruction limit reached!
% 21.63/4.85 % (342772)------------------------------
% 21.63/4.85 % (342772)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.63/4.85 % (342772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.63/4.85 % (342772)CaDiCaL version: 2.1.3
% 21.63/4.85 % (342772)Termination reason: Instruction limit
% 21.63/4.85 % (342772)Termination phase: Saturation
% 21.63/4.85 % (342772)Time elapsed: 0.138 s
% 21.63/4.85 % (342772)Peak memory usage: 99 MB
% 21.63/4.85 % (342772)Instructions burned: 249 (million)
% 21.63/4.85 % (342769)------------------------------
% 21.63/4.85 % (342769)------------------------------
% 21.63/4.85 % (342771)------------------------------
% 21.63/4.85 % (342771)------------------------------
% 21.63/4.85 % (342770)------------------------------
% 21.63/4.85 % (342770)------------------------------
% 21.63/4.85 % (342777)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3181348930:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2989 on theBenchmark for (2989ds/294Mi)
% 21.63/4.85 % (342777)Refutation not found, incomplete strategy
% 21.63/4.85 % (342777)------------------------------
% 21.63/4.85 % (342777)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.63/4.85 % (342777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.63/4.85 % (342777)CaDiCaL version: 2.1.3
% 21.63/4.85 % (342777)Termination reason: Refutation not found, incomplete strategy
% 21.63/4.85 % (342777)Time elapsed: 0.021 s
% 21.63/4.85 % (342777)Peak memory usage: 94 MB
% 21.63/4.85 % (342777)Instructions burned: 35 (million)
% 21.63/4.85 % (342777)------------------------------
% 21.63/4.85 % (342777)------------------------------
% 21.63/4.85 % (342757)Refutation not found, incomplete strategy
% 21.63/4.85 % (342757)------------------------------
% 21.63/4.85 % (342757)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.63/4.85 % (342757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.63/4.85 % (342757)CaDiCaL version: 2.1.3
% 21.63/4.85 % (342757)Termination reason: Refutation not found, incomplete strategy
% 21.63/4.85 % (342757)Time elapsed: 1.106 s
% 21.63/4.85 % (342757)Peak memory usage: 149 MB
% 21.63/4.85 % (342757)Instructions burned: 1046 (million)
% 21.63/4.85 % (342778)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=445733462:i=2350_2987 on theBenchmark for (2987ds/2350Mi)
% 21.63/4.85 % (342780)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2025290134:cts=off:i=113:fsr=off:ss=included:sgt=4_2987 on theBenchmark for (2987ds/113Mi)
% 21.63/4.85 % (342781)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2163983067:i=127:av=off:fsr=off:sup=off_2987 on theBenchmark for (2987ds/127Mi)
% 21.63/4.85 % (342780)Instruction limit reached!
% 21.63/4.85 % (342780)------------------------------
% 21.63/4.85 % (342780)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.63/4.85 % (342780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.63/4.85 % (342780)CaDiCaL version: 2.1.3
% 21.63/4.85 % (342780)Termination reason: Instruction limit
% 21.63/4.85 % (342780)Termination phase: Saturation
% 21.63/4.85 % (342780)Time elapsed: 0.092 s
% 21.63/4.85 % (342780)Peak memory usage: 94 MB
% 21.63/4.85 % (342780)Instructions burned: 114 (million)
% 21.63/4.85 % (342781)Instruction limit reached!
% 21.63/4.85 % (342781)------------------------------
% 21.63/4.85 % (342781)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.63/4.85 % (342781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.63/4.85 % (342781)CaDiCaL version: 2.1.3
% 21.63/4.85 % (342781)Termination reason: Instruction limit
% 21.63/4.85 % (342781)Termination phase: Blocked clause elimination
% 21.63/4.85 % (342781)Time elapsed: 0.131 s
% 21.63/4.85 % (342781)Peak memory usage: 95 MB
% 21.63/4.85 % (342781)Instructions burned: 127 (million)
% 21.63/4.85 % (342782)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1904914185:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2984 on theBenchmark for (2984ds/114Mi)
% 21.63/4.85 % (342782)Instruction limit reached!
% 21.63/4.85 % (342782)------------------------------
% 21.63/4.85 % (342782)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.63/4.85 % (342782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.63/4.85 % (342782)CaDiCaL version: 2.1.3
% 21.63/4.85 % (342782)Termination reason: Instruction limit
% 21.63/4.85 % (342782)Termination phase: Saturation
% 21.63/4.85 % (342782)Time elapsed: 0.060 s
% 21.63/4.85 % (342782)Peak memory usage: 94 MB
% 21.63/4.85 % (342782)Instructions burned: 115 (million)
% 21.63/4.85 % (342757)------------------------------
% 21.63/4.85 % (342757)------------------------------
% 21.63/4.85 % (342786)lrs+10_1_sil=8000:sp=occurrence:random_seed=3862494441:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2983 on theBenchmark for (2983ds/907Mi)
% 21.63/4.85 % (342787)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2801507944:i=437:sd=1:aac=none:ss=included_2982 on theBenchmark for (2982ds/437Mi)
% 21.63/4.85 % (342787)Refutation not found, incomplete strategy
% 21.63/4.85 % (342787)------------------------------
% 21.63/4.85 % (342787)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.63/4.85 % (342787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.63/4.85 % (342787)CaDiCaL version: 2.1.3
% 21.63/4.85 % (342787)Termination reason: Refutation not found, incomplete strategy
% 21.63/4.85 % (342787)Time elapsed: 0.023 s
% 21.63/4.85 % (342787)Peak memory usage: 93 MB
% 21.63/4.85 % (342787)Instructions burned: 18 (million)
% 21.63/4.85 % (342789)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2949680353:i=5202:ss=axioms:sgt=16_2981 on theBenchmark for (2981ds/5202Mi)
% 21.63/4.85 % (342790)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1517726372:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2980 on theBenchmark for (2980ds/134Mi)
% 21.63/4.85 % (342790)Refutation not found, incomplete strategy
% 21.63/4.85 % (342790)------------------------------
% 21.63/4.85 % (342790)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.63/4.85 % (342790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.63/4.85 % (342790)CaDiCaL version: 2.1.3
% 21.63/4.85 % (342790)Termination reason: Refutation not found, incomplete strategy
% 21.63/4.85 % (342790)Time elapsed: 0.029 s
% 21.63/4.85 % (342790)Peak memory usage: 94 MB
% 21.63/4.85 % (342790)Instructions burned: 26 (million)
% 21.63/4.85 % (342787)------------------------------
% 21.63/4.85 % (342787)------------------------------
% 21.63/4.85 % (342790)------------------------------
% 21.63/4.85 % (342790)------------------------------
% 21.63/4.85 % (342795)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=680547481:st=8:i=592:sd=3:ep=RST:ss=axioms_2975 on theBenchmark for (2975ds/592Mi)
% 21.63/4.85 % (342795)Refutation not found, incomplete strategy
% 21.63/4.85 % (342795)------------------------------
% 21.63/4.85 % (342795)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.63/4.85 % (342795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.63/4.85 % (342795)CaDiCaL version: 2.1.3
% 21.63/4.85 % (342795)Termination reason: Refutation not found, incomplete strategy
% 21.63/4.85 % (342795)Time elapsed: 0.024 s
% 21.63/4.85 % (342795)Peak memory usage: 94 MB
% 21.63/4.85 % (342795)Instructions burned: 35 (million)
% 21.63/4.85 % (342786)Instruction limit reached!
% 21.63/4.85 % (342786)------------------------------
% 21.63/4.85 % (342786)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.63/4.85 % (342786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.63/4.85 % (342786)CaDiCaL version: 2.1.3
% 21.63/4.85 % (342786)Termination reason: Instruction limit
% 21.63/4.85 % (342786)Termination phase: Saturation
% 21.63/4.85 % (342786)Time elapsed: 0.884 s
% 21.63/4.85 % (342786)Peak memory usage: 104 MB
% 21.63/4.85 % (342786)Instructions burned: 907 (million)
% 21.63/4.85 % (342795)------------------------------
% 21.63/4.85 % (342795)------------------------------
% 21.63/4.85 % (342796)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1025337002:st=3:i=13193:sd=3:ss=axioms_2973 on theBenchmark for (2973ds/13193Mi)
% 21.63/4.85 % (342798)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=1769513248:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2971 on theBenchmark for (2971ds/125Mi)
% 21.63/4.85 % (342799)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2826081466:i=134:gtgl=5:slsql=off:gtg=exists_sym_2970 on theBenchmark for (2970ds/134Mi)
% 21.63/4.85 % (342755)First to succeed.
% 21.63/4.85 % (342755)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-342750"
% 21.63/4.85 % (342798)Instruction limit reached!
% 21.63/4.85 % (342798)------------------------------
% 21.63/4.85 % (342798)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.63/4.85 % (342798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.63/4.85 % (342798)CaDiCaL version: 2.1.3
% 21.63/4.85 % (342798)Termination reason: Instruction limit
% 21.63/4.85 % (342798)Termination phase: Saturation
% 21.63/4.85 % (342798)Time elapsed: 0.115 s
% 21.63/4.85 % (342798)Peak memory usage: 95 MB
% 21.63/4.85 % (342798)Instructions burned: 126 (million)
% 21.63/4.85 % (342799)Instruction limit reached!
% 21.63/4.85 % (342799)------------------------------
% 21.63/4.85 % (342799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.63/4.85 % (342799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.63/4.85 % (342799)CaDiCaL version: 2.1.3
% 21.63/4.85 % (342799)Termination reason: Instruction limit
% 21.63/4.85 % (342799)Termination phase: Preprocessing 3
% 21.63/4.85 % (342799)Time elapsed: 0.076 s
% 21.63/4.85 % (342799)Peak memory usage: 91 MB
% 21.63/4.85 % (342799)Instructions burned: 134 (million)
% 21.63/4.85 % (342804)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2904826961:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2966 on theBenchmark for (2966ds/431Mi)
% 21.63/4.85 % (342803)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2157117638:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2967 on theBenchmark for (2967ds/141Mi)
% 21.63/4.85 % (342804)Refutation not found, incomplete strategy
% 21.63/4.85 % (342804)------------------------------
% 21.63/4.85 % (342804)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.63/4.85 % (342804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.63/4.85 % (342804)CaDiCaL version: 2.1.3
% 21.63/4.85 % (342804)Termination reason: Refutation not found, incomplete strategy
% 21.63/4.85 % (342804)Time elapsed: 0.015 s
% 21.63/4.85 % (342804)Peak memory usage: 94 MB
% 21.63/4.85 % (342804)Instructions burned: 20 (million)
% 21.63/4.85 % (342803)Refutation not found, incomplete strategy
% 21.63/4.85 % (342803)------------------------------
% 21.63/4.85 % (342803)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.63/4.85 % (342803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.63/4.85 % (342803)CaDiCaL version: 2.1.3
% 21.63/4.85 % (342803)Termination reason: Refutation not found, incomplete strategy
% 21.63/4.85 % (342803)Time elapsed: 0.028 s
% 21.63/4.85 % (342803)Peak memory usage: 94 MB
% 21.63/4.85 % (342803)Instructions burned: 24 (million)
% 21.63/4.85 % (342755)Refutation found. Thanks to Tanya!
% 21.63/4.85 % SZS status Theorem for theBenchmark
% 21.63/4.85 % SZS output start Proof for theBenchmark
% See solution above
% 26.40/5.08 % (342755)------------------------------
% 26.40/5.08 % (342755)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.40/5.08 % (342755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.40/5.08 % (342755)CaDiCaL version: 2.1.3
% 26.40/5.08 % (342755)Termination reason: Refutation
% 26.40/5.08 % (342755)Time elapsed: 2.832 s
% 26.40/5.08 % (342755)Peak memory usage: 200 MB
% 26.40/5.08 % (342755)Instructions burned: 2888 (million)
% 26.40/5.08 % (342755)------------------------------
% 26.40/5.08 % (342755)------------------------------
% 26.40/5.08 % (342750)Success in time 3.716 s
% 26.40/5.08 % Vampire exiting
%------------------------------------------------------------------------------