%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR060+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n001.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 : Thu Sep 24 12:14:54 PM UTC 2026
% Result : Theorem 0.16s 0.60s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR060+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.56 % Computer : n001.cluster.edu
% 0.10/0.56 % Model : x86_64 x86_64
% 0.10/0.56 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.56 % Memory : 8046.5625MB
% 0.10/0.56 % OS : Linux 6.8.0-71-generic
% 0.10/0.56 % CPULimit : 300
% 0.10/0.56 % WCLimit : 300
% 0.10/0.56 % DateTime : Mon Sep 21 14:45:30 UTC 2026
% 0.10/0.56 % CPUTime :
% 0.16/0.58 % Drodi V4.1.1
% 0.16/0.60 % Refutation found
% 0.16/0.60 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.16/0.60 % SZS output start CNFRefutation for theBenchmark
% 0.16/0.60 fof(f1,axiom,(
% 0.16/0.60 genlmt(c_ldscdemonstrationspindleheadmt,c_currentworlddatacollectormt_nonhomocentric) ),
% 0.16/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.60 fof(f4,axiom,(
% 0.16/0.60 genlmt(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988)),c_translation_0_885),c_machinelearningspindleheadmt) ),
% 0.16/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.60 fof(f5,axiom,(
% 0.16/0.60 genlmt(c_machinelearningspindleheadmt,c_miptdatabase19681997_termsmt) ),
% 0.16/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.60 fof(f6,axiom,(
% 0.16/0.60 (! [TERM,INDEPCOL,PRED,DEPCOL] :( ( isa(TERM,INDEPCOL)& relationexistsall(PRED,DEPCOL,INDEPCOL) )=> isa(f_relationexistsallfn(TERM,PRED,DEPCOL,INDEPCOL),DEPCOL) ) )),
% 0.16/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.60 fof(f8,axiom,(
% 0.16/0.60 genlmt(c_miptdatabase19681997_termsmt,c_ldscgeneralcollectormt) ),
% 0.16/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.60 fof(f9,axiom,(
% 0.16/0.60 genlmt(c_ldscgeneralcollectormt,c_ldscdemonstrationspindleheadmt) ),
% 0.16/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.60 fof(f13,axiom,(
% 0.16/0.60 (! [TERM] :( ( mtvisible(c_currentworlddatacollectormt_nonhomocentric)& isa(TERM,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)) )=> tptp_9_51(f_relationexistsallfn(TERM,c_tptp_9_51,c_tptpcol_16_27189,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)),TERM) ) )),
% 0.16/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.60 fof(f14,axiom,(
% 0.16/0.60 ( mtvisible(c_currentworlddatacollectormt_nonhomocentric)=> relationexistsall(c_tptp_9_51,c_tptpcol_16_27189,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)) ) ),
% 0.16/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.60 fof(f15,axiom,(
% 0.16/0.60 isa(c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)) ),
% 0.16/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.60 fof(f53,axiom,(
% 0.16/0.60 (! [X] :( isa(X,c_tptpcol_16_27189)=> tptpcol_16_27189(X) ) )),
% 0.16/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.60 fof(f86,axiom,(
% 0.16/0.60 (! [SPECMT,GENLMT] :( ( mtvisible(SPECMT)& genlmt(SPECMT,GENLMT) )=> mtvisible(GENLMT) ) )),
% 0.16/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.60 fof(f95,conjecture,(
% 0.16/0.60 (? [X] :( mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988)),c_translation_0_885))=> ( tptp_9_51(X,c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802)& tptpcol_16_27189(X) ) ) )),
% 0.16/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.60 fof(f96,negated_conjecture,(
% 0.16/0.60 ~((? [X] :( mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988)),c_translation_0_885))=> ( tptp_9_51(X,c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802)& tptpcol_16_27189(X) ) ) ))),
% 0.16/0.60 inference(negated_conjecture,[status(cth)],[f95])).
% 0.16/0.60 fof(f97,plain,(
% 0.16/0.60 genlmt(c_ldscdemonstrationspindleheadmt,c_currentworlddatacollectormt_nonhomocentric)),
% 0.16/0.60 inference(cnf_transformation,[status(thm)],[f1])).
% 0.16/0.60 fof(f100,plain,(
% 0.16/0.60 genlmt(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988)),c_translation_0_885),c_machinelearningspindleheadmt)),
% 0.16/0.60 inference(cnf_transformation,[status(thm)],[f4])).
% 0.16/0.60 fof(f101,plain,(
% 0.16/0.60 genlmt(c_machinelearningspindleheadmt,c_miptdatabase19681997_termsmt)),
% 0.16/0.60 inference(cnf_transformation,[status(thm)],[f5])).
% 0.16/0.60 fof(f102,plain,(
% 0.16/0.60 ![TERM,INDEPCOL,PRED,DEPCOL]: ((~isa(TERM,INDEPCOL)|~relationexistsall(PRED,DEPCOL,INDEPCOL))|isa(f_relationexistsallfn(TERM,PRED,DEPCOL,INDEPCOL),DEPCOL))),
% 0.16/0.60 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 0.16/0.60 fof(f103,plain,(
% 0.16/0.60 ![X0,X1,X2,X3]: (~isa(X0,X1)|~relationexistsall(X2,X3,X1)|isa(f_relationexistsallfn(X0,X2,X3,X1),X3))),
% 0.16/0.60 inference(cnf_transformation,[status(thm)],[f102])).
% 0.16/0.60 fof(f105,plain,(
% 0.16/0.60 genlmt(c_miptdatabase19681997_termsmt,c_ldscgeneralcollectormt)),
% 0.16/0.60 inference(cnf_transformation,[status(thm)],[f8])).
% 0.16/0.60 fof(f106,plain,(
% 0.16/0.60 genlmt(c_ldscgeneralcollectormt,c_ldscdemonstrationspindleheadmt)),
% 0.16/0.60 inference(cnf_transformation,[status(thm)],[f9])).
% 0.16/0.60 fof(f110,plain,(
% 0.16/0.60 ![TERM]: ((~mtvisible(c_currentworlddatacollectormt_nonhomocentric)|~isa(TERM,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)))|tptp_9_51(f_relationexistsallfn(TERM,c_tptp_9_51,c_tptpcol_16_27189,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)),TERM))),
% 0.16/0.60 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 0.16/0.60 fof(f111,plain,(
% 0.16/0.60 ![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))),
% 0.16/0.60 inference(cnf_transformation,[status(thm)],[f110])).
% 0.16/0.60 fof(f112,plain,(
% 0.16/0.60 ~mtvisible(c_currentworlddatacollectormt_nonhomocentric)|relationexistsall(c_tptp_9_51,c_tptpcol_16_27189,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma))),
% 0.16/0.60 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 0.16/0.60 fof(f113,plain,(
% 0.16/0.60 ~mtvisible(c_currentworlddatacollectormt_nonhomocentric)|relationexistsall(c_tptp_9_51,c_tptpcol_16_27189,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma))),
% 0.16/0.60 inference(cnf_transformation,[status(thm)],[f112])).
% 0.16/0.60 fof(f114,plain,(
% 0.16/0.60 isa(c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma))),
% 0.16/0.60 inference(cnf_transformation,[status(thm)],[f15])).
% 0.16/0.60 fof(f205,plain,(
% 0.16/0.60 ![X]: (~isa(X,c_tptpcol_16_27189)|tptpcol_16_27189(X))),
% 0.16/0.60 inference(pre_NNF_transformation,[status(thm)],[f53])).
% 0.16/0.60 fof(f206,plain,(
% 0.16/0.60 ![X0]: (~isa(X0,c_tptpcol_16_27189)|tptpcol_16_27189(X0))),
% 0.16/0.60 inference(cnf_transformation,[status(thm)],[f205])).
% 0.16/0.60 fof(f266,plain,(
% 0.16/0.60 ![SPECMT,GENLMT]: ((~mtvisible(SPECMT)|~genlmt(SPECMT,GENLMT))|mtvisible(GENLMT))),
% 0.16/0.60 inference(pre_NNF_transformation,[status(thm)],[f86])).
% 0.16/0.60 fof(f267,plain,(
% 0.16/0.60 ![GENLMT]: ((![SPECMT]: (~mtvisible(SPECMT)|~genlmt(SPECMT,GENLMT)))|mtvisible(GENLMT))),
% 0.16/0.60 inference(miniscoping,[status(thm)],[f266])).
% 0.16/0.60 fof(f268,plain,(
% 0.16/0.60 ![X0,X1]: (~mtvisible(X0)|~genlmt(X0,X1)|mtvisible(X1))),
% 0.16/0.60 inference(cnf_transformation,[status(thm)],[f267])).
% 0.16/0.60 fof(f289,plain,(
% 0.16/0.60 (![X]: (mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988)),c_translation_0_885))&(~tptp_9_51(X,c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802)|~tptpcol_16_27189(X))))),
% 0.16/0.60 inference(pre_NNF_transformation,[status(thm)],[f96])).
% 0.16/0.60 fof(f290,plain,(
% 0.16/0.60 mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988)),c_translation_0_885))&(![X]: (~tptp_9_51(X,c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802)|~tptpcol_16_27189(X)))),
% 0.16/0.60 inference(miniscoping,[status(thm)],[f289])).
% 0.16/0.60 fof(f291,plain,(
% 0.16/0.60 mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988)),c_translation_0_885))),
% 0.16/0.60 inference(cnf_transformation,[status(thm)],[f290])).
% 0.16/0.60 fof(f292,plain,(
% 0.16/0.60 ![X0]: (~tptp_9_51(X0,c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802)|~tptpcol_16_27189(X0))),
% 0.16/0.60 inference(cnf_transformation,[status(thm)],[f290])).
% 0.16/0.60 fof(f293,plain,(
% 0.16/0.60 ![X0,X1]: (~relationexistsall(X0,X1,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma))|isa(f_relationexistsallfn(c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802,X0,X1,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)),X1))),
% 0.16/0.60 inference(resolution,[status(thm)],[f103,f114])).
% 0.16/0.60 fof(f294,plain,(
% 0.16/0.60 ~mtvisible(c_machinelearningspindleheadmt)|mtvisible(c_miptdatabase19681997_termsmt)),
% 0.16/0.60 inference(resolution,[status(thm)],[f268,f101])).
% 0.16/0.60 fof(f297,plain,(
% 0.16/0.60 ~mtvisible(c_ldscdemonstrationspindleheadmt)|mtvisible(c_currentworlddatacollectormt_nonhomocentric)),
% 0.16/0.60 inference(resolution,[status(thm)],[f268,f97])).
% 0.16/0.60 fof(f298,plain,(
% 0.16/0.60 ~mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988)),c_translation_0_885))|mtvisible(c_machinelearningspindleheadmt)),
% 0.16/0.60 inference(resolution,[status(thm)],[f268,f100])).
% 0.16/0.60 fof(f299,plain,(
% 0.16/0.60 mtvisible(c_machinelearningspindleheadmt)),
% 0.16/0.60 inference(forward_subsumption_resolution,[status(thm)],[f298,f291])).
% 0.16/0.60 fof(f300,plain,(
% 0.16/0.60 mtvisible(c_miptdatabase19681997_termsmt)),
% 0.16/0.60 inference(forward_subsumption_resolution,[status(thm)],[f294,f299])).
% 0.16/0.60 fof(f301,plain,(
% 0.16/0.60 ~mtvisible(c_miptdatabase19681997_termsmt)|mtvisible(c_ldscgeneralcollectormt)),
% 0.16/0.60 inference(resolution,[status(thm)],[f105,f268])).
% 0.16/0.60 fof(f302,plain,(
% 0.16/0.60 mtvisible(c_ldscgeneralcollectormt)),
% 0.16/0.60 inference(forward_subsumption_resolution,[status(thm)],[f301,f300])).
% 0.16/0.60 fof(f303,plain,(
% 0.16/0.60 ~mtvisible(c_ldscgeneralcollectormt)|mtvisible(c_ldscdemonstrationspindleheadmt)),
% 0.16/0.60 inference(resolution,[status(thm)],[f106,f268])).
% 0.16/0.60 fof(f304,plain,(
% 0.16/0.60 mtvisible(c_ldscdemonstrationspindleheadmt)),
% 0.16/0.60 inference(forward_subsumption_resolution,[status(thm)],[f303,f302])).
% 0.16/0.60 fof(f308,plain,(
% 0.16/0.60 ~mtvisible(c_currentworlddatacollectormt_nonhomocentric)|tptp_9_51(f_relationexistsallfn(c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802,c_tptp_9_51,c_tptpcol_16_27189,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)),c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802)),
% 0.16/0.60 inference(resolution,[status(thm)],[f111,f114])).
% 0.16/0.60 fof(f310,plain,(
% 0.16/0.60 mtvisible(c_currentworlddatacollectormt_nonhomocentric)),
% 0.16/0.60 inference(backward_subsumption_resolution,[status(thm)],[f297,f304])).
% 0.16/0.60 fof(f313,plain,(
% 0.16/0.60 relationexistsall(c_tptp_9_51,c_tptpcol_16_27189,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma))),
% 0.16/0.60 inference(backward_subsumption_resolution,[status(thm)],[f113,f310])).
% 0.16/0.60 fof(f314,plain,(
% 0.16/0.60 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)),
% 0.16/0.60 inference(resolution,[status(thm)],[f313,f293])).
% 0.16/0.60 fof(f316,plain,(
% 0.16/0.60 tptp_9_51(f_relationexistsallfn(c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802,c_tptp_9_51,c_tptpcol_16_27189,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)),c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802)),
% 0.16/0.60 inference(forward_subsumption_resolution,[status(thm)],[f308,f310])).
% 0.16/0.60 fof(f317,plain,(
% 0.16/0.60 ~tptpcol_16_27189(f_relationexistsallfn(c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802,c_tptp_9_51,c_tptpcol_16_27189,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)))),
% 0.16/0.60 inference(resolution,[status(thm)],[f316,f292])).
% 0.16/0.60 fof(f319,plain,(
% 0.16/0.60 tptpcol_16_27189(f_relationexistsallfn(c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802,c_tptp_9_51,c_tptpcol_16_27189,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)))),
% 0.16/0.60 inference(resolution,[status(thm)],[f314,f206])).
% 0.16/0.60 fof(f322,plain,(
% 0.16/0.60 $false),
% 0.16/0.60 inference(forward_subsumption_resolution,[status(thm)],[f319,f317])).
% 0.16/0.60 % SZS output end CNFRefutation for theBenchmark.p
% 0.16/0.63 % Elapsed time: 0.050171 seconds
% 0.16/0.63 % CPU time: 0.151139 seconds
% 0.16/0.63 % Total memory used: 58.691 MB
% 0.16/0.63 % Net memory used: 58.668 MB
%------------------------------------------------------------------------------