%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CSR060+2 : 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 : n018.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 4.28s 1.80s
% Output : Refutation 0.34s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 17
% Syntax : Number of formulae : 80 ( 22 unt; 5 def)
% Number of atoms : 187 ( 0 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 204 ( 97 ~; 89 |; 6 &)
% ( 5 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 12 ( 11 usr; 6 prp; 0-3 aty)
% Number of functors : 18 ( 18 usr; 13 con; 0-4 aty)
% Number of variables : 64 ( 0 sgn 62 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f52,axiom,
genlmt(c_miptdatabase19681997_termsmt,c_ldscgeneralcollectormt),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_52) ).
fof(f58,axiom,
genlmt(c_machinelearningspindleheadmt,c_miptdatabase19681997_termsmt),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_58) ).
fof(f59,axiom,
genlmt(c_ldscdemonstrationspindleheadmt,c_currentworlddatacollectormt_nonhomocentric),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_59) ).
fof(f64,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',ax1_64) ).
fof(f87,axiom,
genlmt(c_ldscgeneralcollectormt,c_ldscdemonstrationspindleheadmt),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_87) ).
fof(f226,axiom,
isa(c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_226) ).
fof(f247,axiom,
genlmt(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988)),c_translation_0_885),c_machinelearningspindleheadmt),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_247) ).
fof(f308,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',ax1_308) ).
fof(f309,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',ax1_309) ).
fof(f618,axiom,
! [X0] :
( isa(X0,c_tptpcol_16_27189)
=> tptpcol_16_27189(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_618) ).
fof(f1123,axiom,
! [X0,X1] :
( ( mtvisible(X0)
& genlmt(X0,X1) )
=> mtvisible(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_1123) ).
fof(f1132,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',query110) ).
fof(f1133,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)],[f1132]) ).
fof(f1221,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,[],[f1133]) ).
fof(f1222,plain,
! [X0,X1] :
( mtvisible(X1)
| ~ mtvisible(X0)
| ~ genlmt(X0,X1) ),
inference(ennf_transformation,[],[f1123]) ).
fof(f1223,plain,
! [X0,X1] :
( mtvisible(X1)
| ~ mtvisible(X0)
| ~ genlmt(X0,X1) ),
inference(flattening,[],[f1222]) ).
fof(f1226,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,[],[f308]) ).
fof(f1227,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,[],[f1226]) ).
fof(f1229,plain,
! [X0] :
( tptpcol_16_27189(X0)
| ~ isa(X0,c_tptpcol_16_27189) ),
inference(ennf_transformation,[],[f618]) ).
fof(f1253,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,[],[f309]) ).
fof(f1255,plain,
! [X0,X1,X2,X3] :
( isa(f_relationexistsallfn(X0,X2,X3,X1),X3)
| ~ isa(X0,X1)
| ~ relationexistsall(X2,X3,X1) ),
inference(ennf_transformation,[],[f64]) ).
fof(f1256,plain,
! [X0,X1,X2,X3] :
( isa(f_relationexistsallfn(X0,X2,X3,X1),X3)
| ~ isa(X0,X1)
| ~ relationexistsall(X2,X3,X1) ),
inference(flattening,[],[f1255]) ).
fof(f1319,plain,
mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988)),c_translation_0_885)),
inference(cnf_transformation,[],[f1221]) ).
fof(f1320,plain,
! [X0] :
( ~ tptpcol_16_27189(X0)
| ~ tptp_9_51(X0,c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802) ),
inference(cnf_transformation,[],[f1221]) ).
fof(f1323,plain,
! [X0,X1] :
( mtvisible(X1)
| ~ mtvisible(X0)
| ~ genlmt(X0,X1) ),
inference(cnf_transformation,[],[f1223]) ).
fof(f1325,plain,
genlmt(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988)),c_translation_0_885),c_machinelearningspindleheadmt),
inference(cnf_transformation,[],[f247]) ).
fof(f1329,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,[],[f1227]) ).
fof(f1331,plain,
! [X0] :
( tptpcol_16_27189(X0)
| ~ isa(X0,c_tptpcol_16_27189) ),
inference(cnf_transformation,[],[f1229]) ).
fof(f1333,plain,
isa(c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)),
inference(cnf_transformation,[],[f226]) ).
fof(f1351,plain,
genlmt(c_machinelearningspindleheadmt,c_miptdatabase19681997_termsmt),
inference(cnf_transformation,[],[f58]) ).
fof(f1359,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,[],[f1253]) ).
fof(f1360,plain,
genlmt(c_ldscdemonstrationspindleheadmt,c_currentworlddatacollectormt_nonhomocentric),
inference(cnf_transformation,[],[f59]) ).
fof(f1363,plain,
! [X2,X3,X0,X1] :
( ~ relationexistsall(X2,X3,X1)
| ~ isa(X0,X1)
| isa(f_relationexistsallfn(X0,X2,X3,X1),X3) ),
inference(cnf_transformation,[],[f1256]) ).
fof(f1396,plain,
genlmt(c_miptdatabase19681997_termsmt,c_ldscgeneralcollectormt),
inference(cnf_transformation,[],[f52]) ).
fof(f1413,plain,
genlmt(c_ldscgeneralcollectormt,c_ldscdemonstrationspindleheadmt),
inference(cnf_transformation,[],[f87]) ).
fof(f1477,definition,
( spl0_10
<=> mtvisible(c_currentworlddatacollectormt_nonhomocentric) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f1478,plain,
( ~ mtvisible(c_currentworlddatacollectormt_nonhomocentric)
| spl0_10 ),
inference(avatar_component_clause,[],[f1477]) ).
fof(f1480,definition,
( spl0_11
<=> relationexistsall(c_tptp_9_51,c_tptpcol_16_27189,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f1481,plain,
( relationexistsall(c_tptp_9_51,c_tptpcol_16_27189,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma))
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f1480]) ).
fof(f1482,plain,
( ~ spl0_10
| spl0_11 ),
inference(avatar_split_clause,[],[f1359,f1480,f1477]) ).
fof(f1484,definition,
( spl0_12
<=> ! [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,[spl0_12])],[avatar_definition]) ).
fof(f1485,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)) )
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f1484]) ).
fof(f1486,plain,
( ~ spl0_10
| spl0_12 ),
inference(avatar_split_clause,[],[f1329,f1484,f1477]) ).
fof(f1490,plain,
! [X0] :
( ~ tptp_9_51(X0,c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802)
| ~ isa(X0,c_tptpcol_16_27189) ),
inference(resolution,[],[f1331,f1320]) ).
fof(f1557,plain,
( ! [X0] :
( ~ mtvisible(X0)
| ~ genlmt(X0,c_currentworlddatacollectormt_nonhomocentric) )
| spl0_10 ),
inference(resolution,[],[f1323,f1478]) ).
fof(f1564,plain,
( ! [X0,X1] :
( ~ mtvisible(X1)
| ~ genlmt(X0,c_currentworlddatacollectormt_nonhomocentric)
| ~ genlmt(X1,X0) )
| spl0_10 ),
inference(resolution,[],[f1557,f1323]) ).
fof(f1574,plain,
( ! [X2,X0,X1] :
( ~ mtvisible(X2)
| ~ genlmt(X1,X0)
| ~ genlmt(X0,c_currentworlddatacollectormt_nonhomocentric)
| ~ genlmt(X2,X1) )
| spl0_10 ),
inference(resolution,[],[f1564,f1323]) ).
fof(f1587,plain,
( ! [X2,X3,X0,X1] :
( ~ mtvisible(X3)
| ~ genlmt(X1,c_currentworlddatacollectormt_nonhomocentric)
| ~ genlmt(X2,X0)
| ~ genlmt(X0,X1)
| ~ genlmt(X3,X2) )
| spl0_10 ),
inference(resolution,[],[f1574,f1323]) ).
fof(f1623,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ mtvisible(X4)
| ~ genlmt(X1,X2)
| ~ genlmt(X2,X0)
| ~ genlmt(X3,X1)
| ~ genlmt(X0,c_currentworlddatacollectormt_nonhomocentric)
| ~ genlmt(X4,X3) )
| spl0_10 ),
inference(resolution,[],[f1587,f1323]) ).
fof(f1676,plain,
( ! [X2,X3,X0,X1] :
( ~ genlmt(X0,X1)
| ~ genlmt(X1,X2)
| ~ genlmt(X3,X0)
| ~ genlmt(X2,c_currentworlddatacollectormt_nonhomocentric)
| ~ genlmt(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988)),c_translation_0_885),X3) )
| spl0_10 ),
inference(resolution,[],[f1623,f1319]) ).
fof(f1800,plain,
( ! [X2,X0,X1] :
( ~ genlmt(X0,X1)
| ~ genlmt(X1,X2)
| ~ genlmt(c_machinelearningspindleheadmt,X0)
| ~ genlmt(X2,c_currentworlddatacollectormt_nonhomocentric) )
| spl0_10 ),
inference(resolution,[],[f1325,f1676]) ).
fof(f1894,plain,
( ! [X0,X1] :
( ~ genlmt(X0,X1)
| ~ genlmt(X1,c_ldscdemonstrationspindleheadmt)
| ~ genlmt(c_machinelearningspindleheadmt,X0) )
| spl0_10 ),
inference(resolution,[],[f1800,f1360]) ).
fof(f1916,plain,
( ! [X0] :
( ~ genlmt(X0,c_ldscgeneralcollectormt)
| ~ genlmt(c_machinelearningspindleheadmt,X0) )
| spl0_10 ),
inference(resolution,[],[f1894,f1413]) ).
fof(f1920,plain,
( ~ genlmt(c_machinelearningspindleheadmt,c_miptdatabase19681997_termsmt)
| spl0_10 ),
inference(resolution,[],[f1916,f1396]) ).
fof(f1922,plain,
( $false
| spl0_10 ),
inference(resolution,[],[f1920,f1351]) ).
fof(f1923,plain,
spl0_10,
inference(avatar_contradiction_clause,[],[f1922]) ).
fof(f1930,plain,
( ~ isa(c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma))
| ~ isa(f_relationexistsallfn(c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802,c_tptp_9_51,c_tptpcol_16_27189,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)),c_tptpcol_16_27189)
| ~ spl0_12 ),
inference(resolution,[],[f1485,f1490]) ).
fof(f1932,definition,
( spl0_30
<=> isa(f_relationexistsallfn(c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802,c_tptp_9_51,c_tptpcol_16_27189,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)),c_tptpcol_16_27189) ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f1933,plain,
( ~ isa(f_relationexistsallfn(c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802,c_tptp_9_51,c_tptpcol_16_27189,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)),c_tptpcol_16_27189)
| spl0_30 ),
inference(avatar_component_clause,[],[f1932]) ).
fof(f1935,definition,
( spl0_31
<=> isa(c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)) ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f1936,plain,
( ~ isa(c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma))
| spl0_31 ),
inference(avatar_component_clause,[],[f1935]) ).
fof(f1937,plain,
( ~ spl0_30
| ~ spl0_31
| ~ spl0_12 ),
inference(avatar_split_clause,[],[f1930,f1484,f1935,f1932]) ).
fof(f3221,plain,
( ! [X0] :
( isa(f_relationexistsallfn(X0,c_tptp_9_51,c_tptpcol_16_27189,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)),c_tptpcol_16_27189)
| ~ isa(X0,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)) )
| ~ spl0_11 ),
inference(resolution,[],[f1363,f1481]) ).
fof(f3223,plain,
( ~ isa(c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma))
| ~ spl0_11
| spl0_30 ),
inference(resolution,[],[f3221,f1933]) ).
fof(f3224,plain,
( ~ spl0_31
| ~ spl0_11
| spl0_30 ),
inference(avatar_split_clause,[],[f3223,f1932,f1480,f1935]) ).
fof(f3225,plain,
( $false
| spl0_31 ),
inference(resolution,[],[f1936,f1333]) ).
fof(f3226,plain,
spl0_31,
inference(avatar_contradiction_clause,[],[f3225]) ).
cnf(s6,plain,
( ~ spl0_10
| spl0_11 ),
inference(sat_conversion,[],[f1482]) ).
cnf(s7,plain,
( ~ spl0_10
| spl0_12 ),
inference(sat_conversion,[],[f1486]) ).
cnf(s27,plain,
spl0_10,
inference(sat_conversion,[],[f1923]) ).
cnf(s28,plain,
( ~ spl0_12
| ~ spl0_30
| ~ spl0_31 ),
inference(sat_conversion,[],[f1937]) ).
cnf(s62,plain,
( ~ spl0_11
| spl0_30
| ~ spl0_31 ),
inference(sat_conversion,[],[f3224]) ).
cnf(s63,plain,
spl0_31,
inference(sat_conversion,[],[f3226]) ).
cnf(s64,plain,
( ~ spl0_11
| spl0_30 ),
inference(rat,[],[s62,s63]) ).
cnf(s66,plain,
( ~ spl0_12
| ~ spl0_30 ),
inference(rat,[],[s28,s63]) ).
cnf(s67,plain,
spl0_12,
inference(rat,[],[s7,s27]) ).
cnf(s68,plain,
~ spl0_30,
inference(rat,[],[s66,s67]) ).
cnf(s69,plain,
~ spl0_11,
inference(rat,[],[s64,s68]) ).
cnf(s70,plain,
$false,
inference(rat,[],[s6,s69,s27]) ).
fof(f3227,plain,
$false,
inference(avatar_sat_refutation,[],[s70]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : CSR060+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.09 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.27/0.31 % Computer : n018.cluster.edu
% 0.27/0.31 % Model : x86_64 x86_64
% 0.27/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.27/0.31 % Memory : 8046.5625MB
% 0.27/0.31 % OS : Linux 6.8.0-71-generic
% 0.27/0.31 % CPULimit : 300
% 0.27/0.31 % WCLimit : 300
% 0.27/0.31 % DateTime : Mon Sep 28 22:23:25 UTC 2026
% 0.27/0.31 % CPUTime :
% 0.27/0.31 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.27/0.36 Running first-order theorem proving
% 0.27/0.36 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
% 4.28/1.80 % (3861454)Detected formulas, will run a generic FOF schedule.
% 4.28/1.80 % (3861461)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=801720401:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 4.28/1.80 % (3861459)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=2514342830:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 4.28/1.80 % (3861464)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=573881784:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 4.28/1.80 % (3861462)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=136391827:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 4.28/1.80 % (3861465)dis-21_1_sil=8000:lcm=predicate:random_seed=1234040871:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 4.28/1.80 % (3861463)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2314023511:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 4.28/1.80 % (3861460)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=3256506649:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 4.28/1.80 % (3861462)Refutation not found, incomplete strategy
% 4.28/1.80 % (3861462)------------------------------
% 4.28/1.80 % (3861462)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.28/1.80 % (3861462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.28/1.80 % (3861462)CaDiCaL version: 2.1.3
% 4.28/1.80 % (3861462)Termination reason: Refutation not found, incomplete strategy
% 4.28/1.80 % (3861462)Time elapsed: 0.004 s
% 4.28/1.80 % (3861462)Peak memory usage: 88 MB
% 4.28/1.80 % (3861462)Instructions burned: 3 (million)
% 4.28/1.80 % (3861465)First to succeed.
% 4.28/1.80 % (3861465)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3861454"
% 4.28/1.80 % (3861463)Instruction limit reached!
% 4.28/1.80 % (3861463)------------------------------
% 4.28/1.80 % (3861463)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.28/1.80 % (3861463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.28/1.80 % (3861463)CaDiCaL version: 2.1.3
% 4.28/1.80 % (3861463)Termination reason: Instruction limit
% 4.28/1.80 % (3861463)Termination phase: Saturation
% 4.28/1.80 % (3861463)Time elapsed: 0.080 s
% 4.28/1.80 % (3861463)Peak memory usage: 88 MB
% 4.28/1.80 % (3861463)Instructions burned: 119 (million)
% 4.28/1.80 % (3861464)Instruction limit reached!
% 4.28/1.80 % (3861464)------------------------------
% 4.28/1.80 % (3861464)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.28/1.80 % (3861464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.28/1.80 % (3861464)CaDiCaL version: 2.1.3
% 4.28/1.80 % (3861464)Termination reason: Instruction limit
% 4.28/1.80 % (3861464)Termination phase: Saturation
% 4.28/1.80 % (3861464)Time elapsed: 0.112 s
% 4.28/1.80 % (3861464)Peak memory usage: 90 MB
% 4.28/1.80 % (3861464)Instructions burned: 139 (million)
% 4.28/1.80 % (3861473)lrs+10_1_sil=8000:sp=occurrence:random_seed=3813188736:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi)
% 4.28/1.80 % (3861462)------------------------------
% 4.28/1.80 % (3861462)------------------------------
% 4.28/1.80 % (3861473)Refutation not found, incomplete strategy
% 4.28/1.80 % (3861473)------------------------------
% 4.28/1.80 % (3861473)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.28/1.80 % (3861473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.28/1.80 % (3861473)CaDiCaL version: 2.1.3
% 4.28/1.80 % (3861473)Termination reason: Refutation not found, incomplete strategy
% 4.28/1.80 % (3861473)Time elapsed: 0.008 s
% 4.28/1.80 % (3861473)Peak memory usage: 89 MB
% 4.28/1.80 % (3861473)Instructions burned: 6 (million)
% 4.28/1.80 % (3861474)lrs+10_1_sil=32000:urr=on:br=off:random_seed=4069361588:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 4.28/1.80 % (3861474)Refutation not found, incomplete strategy
% 4.28/1.80 % (3861474)------------------------------
% 4.28/1.80 % (3861474)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.28/1.80 % (3861474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.28/1.80 % (3861474)CaDiCaL version: 2.1.3
% 4.28/1.80 % (3861474)Termination reason: Refutation not found, incomplete strategy
% 4.28/1.80 % (3861474)Time elapsed: 0.009 s
% 4.28/1.80 % (3861474)Peak memory usage: 89 MB
% 4.28/1.80 % (3861474)Instructions burned: 8 (million)
% 4.28/1.80 % (3861465)Refutation found. Thanks to Tanya!
% 4.28/1.80 % SZS status Theorem for theBenchmark
% 4.28/1.80 % SZS output start Proof for theBenchmark
% See solution above
% 0.34/2.16 % (3861465)------------------------------
% 0.34/2.16 % (3861465)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.34/2.16 % (3861465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.34/2.16 % (3861465)CaDiCaL version: 2.1.3
% 0.34/2.16 % (3861465)Termination reason: Refutation
% 0.34/2.16 % (3861465)Time elapsed: 0.073 s
% 0.34/2.16 % (3861465)Peak memory usage: 90 MB
% 0.34/2.16 % (3861465)Instructions burned: 83 (million)
% 0.34/2.16 % (3861465)------------------------------
% 0.34/2.16 % (3861465)------------------------------
% 0.34/2.16 % (3861454)Success in time 0.767 s
% 0.34/2.16 % Vampire exiting
%------------------------------------------------------------------------------