%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : CSR060+1 : TPTP v8.1.2. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu May 9 17:18:29 EDT 2024
% Result : Theorem 0.76s 0.93s
% Output : Refutation 0.76s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : CSR060+1 : TPTP v8.1.2. Released v3.4.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n006.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Thu May 9 01:40:08 EDT 2024
% 0.13/0.35 % CPUTime :
% 0.76/0.93 % Version: 1.5
% 0.76/0.93 % SZS status Theorem
% 0.76/0.93 % SZS output start CNFRefutation
% 0.76/0.93 fof(query60,conjecture,(?[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)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', query60)).
% 0.76/0.93 fof(c0,negated_conjecture,(~(?[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))))),inference(assume_negation,[status(cth)],[query60])).
% 0.76/0.93 fof(c1,negated_conjecture,(![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)))),inference(fof_nnf,[status(thm)],[c0])).
% 0.76/0.93 fof(c2,negated_conjecture,(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)))),inference(shift_quantors,[status(thm)],[c1])).
% 0.76/0.93 fof(c4,negated_conjecture,(![X2]:(mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988)),c_translation_0_885))&(~tptp_9_51(X2,c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802)|~tptpcol_16_27189(X2)))),inference(shift_quantors,[status(thm)],[fof(c3,negated_conjecture,(mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988)),c_translation_0_885))&(![X2]:(~tptp_9_51(X2,c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802)|~tptpcol_16_27189(X2)))),inference(variable_rename,[status(thm)],[c2])).])).
% 0.76/0.93 cnf(c6,negated_conjecture,~tptp_9_51(X179,c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802)|~tptpcol_16_27189(X179),inference(split_conjunct,[status(thm)],[c4])).
% 0.76/0.93 fof(just15,axiom,isa(c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', just15)).
% 0.76/0.93 cnf(c245,plain,isa(c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)),inference(split_conjunct,[status(thm)],[just15])).
% 0.76/0.93 fof(just13,axiom,(![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))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', just13)).
% 0.76/0.93 fof(c248,plain,(![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))),inference(fof_nnf,[status(thm)],[just13])).
% 0.76/0.93 fof(c249,plain,(![X169]:((~mtvisible(c_currentworlddatacollectormt_nonhomocentric)|~isa(X169,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)))|tptp_9_51(f_relationexistsallfn(X169,c_tptp_9_51,c_tptpcol_16_27189,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)),X169))),inference(variable_rename,[status(thm)],[c248])).
% 0.76/0.93 cnf(c250,plain,~mtvisible(c_currentworlddatacollectormt_nonhomocentric)|~isa(X358,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma))|tptp_9_51(f_relationexistsallfn(X358,c_tptp_9_51,c_tptpcol_16_27189,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)),X358),inference(split_conjunct,[status(thm)],[c249])).
% 0.76/0.93 cnf(c428,plain,~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),inference(resolution,[status(thm)],[c250, c245])).
% 0.76/0.93 fof(just86,axiom,(![SPECMT]:(![GENLMT]:((mtvisible(SPECMT)&genlmt(SPECMT,GENLMT))=>mtvisible(GENLMT)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', just86)).
% 0.76/0.93 fof(c33,plain,(![SPECMT]:(![GENLMT]:((~mtvisible(SPECMT)|~genlmt(SPECMT,GENLMT))|mtvisible(GENLMT)))),inference(fof_nnf,[status(thm)],[just86])).
% 0.76/0.93 fof(c34,plain,(![X16]:(![X17]:((~mtvisible(X16)|~genlmt(X16,X17))|mtvisible(X17)))),inference(variable_rename,[status(thm)],[c33])).
% 0.76/0.93 cnf(c35,plain,~mtvisible(X193)|~genlmt(X193,X194)|mtvisible(X194),inference(split_conjunct,[status(thm)],[c34])).
% 0.76/0.93 fof(just1,axiom,genlmt(c_ldscdemonstrationspindleheadmt,c_currentworlddatacollectormt_nonhomocentric),file('/export/starexec/sandbox/benchmark/theBenchmark.p', just1)).
% 0.76/0.93 cnf(c264,plain,genlmt(c_ldscdemonstrationspindleheadmt,c_currentworlddatacollectormt_nonhomocentric),inference(split_conjunct,[status(thm)],[just1])).
% 0.76/0.93 fof(just91,axiom,(![X]:(![Y]:(![Z]:((genlmt(X,Y)&genlmt(Y,Z))=>genlmt(X,Z))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', just91)).
% 0.76/0.93 fof(c14,plain,(![X]:(![Y]:(![Z]:((~genlmt(X,Y)|~genlmt(Y,Z))|genlmt(X,Z))))),inference(fof_nnf,[status(thm)],[just91])).
% 0.76/0.93 fof(c15,plain,(![X5]:(![X6]:(![X7]:((~genlmt(X5,X6)|~genlmt(X6,X7))|genlmt(X5,X7))))),inference(variable_rename,[status(thm)],[c14])).
% 0.76/0.93 cnf(c16,plain,~genlmt(X185,X184)|~genlmt(X184,X186)|genlmt(X185,X186),inference(split_conjunct,[status(thm)],[c15])).
% 0.76/0.93 cnf(c277,plain,~genlmt(X322,c_ldscdemonstrationspindleheadmt)|genlmt(X322,c_currentworlddatacollectormt_nonhomocentric),inference(resolution,[status(thm)],[c16, c264])).
% 0.76/0.93 fof(just9,axiom,genlmt(c_ldscgeneralcollectormt,c_ldscdemonstrationspindleheadmt),file('/export/starexec/sandbox/benchmark/theBenchmark.p', just9)).
% 0.76/0.93 cnf(c254,plain,genlmt(c_ldscgeneralcollectormt,c_ldscdemonstrationspindleheadmt),inference(split_conjunct,[status(thm)],[just9])).
% 0.76/0.93 cnf(c278,plain,~genlmt(X326,c_ldscgeneralcollectormt)|genlmt(X326,c_ldscdemonstrationspindleheadmt),inference(resolution,[status(thm)],[c16, c254])).
% 0.76/0.93 fof(just5,axiom,genlmt(c_machinelearningspindleheadmt,c_miptdatabase19681997_termsmt),file('/export/starexec/sandbox/benchmark/theBenchmark.p', just5)).
% 0.76/0.93 cnf(c260,plain,genlmt(c_machinelearningspindleheadmt,c_miptdatabase19681997_termsmt),inference(split_conjunct,[status(thm)],[just5])).
% 0.76/0.93 fof(just8,axiom,genlmt(c_miptdatabase19681997_termsmt,c_ldscgeneralcollectormt),file('/export/starexec/sandbox/benchmark/theBenchmark.p', just8)).
% 0.76/0.93 cnf(c255,plain,genlmt(c_miptdatabase19681997_termsmt,c_ldscgeneralcollectormt),inference(split_conjunct,[status(thm)],[just8])).
% 0.76/0.93 cnf(c282,plain,~genlmt(X357,c_miptdatabase19681997_termsmt)|genlmt(X357,c_ldscgeneralcollectormt),inference(resolution,[status(thm)],[c16, c255])).
% 0.76/0.93 cnf(c410,plain,genlmt(c_machinelearningspindleheadmt,c_ldscgeneralcollectormt),inference(resolution,[status(thm)],[c282, c260])).
% 0.76/0.93 cnf(c414,plain,genlmt(c_machinelearningspindleheadmt,c_ldscdemonstrationspindleheadmt),inference(resolution,[status(thm)],[c410, c278])).
% 0.76/0.93 cnf(c420,plain,genlmt(c_machinelearningspindleheadmt,c_currentworlddatacollectormt_nonhomocentric),inference(resolution,[status(thm)],[c414, c277])).
% 0.76/0.93 cnf(c427,plain,~mtvisible(c_machinelearningspindleheadmt)|mtvisible(c_currentworlddatacollectormt_nonhomocentric),inference(resolution,[status(thm)],[c420, c35])).
% 0.76/0.93 cnf(c5,negated_conjecture,mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988)),c_translation_0_885)),inference(split_conjunct,[status(thm)],[c4])).
% 0.76/0.93 fof(just4,axiom,genlmt(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988)),c_translation_0_885),c_machinelearningspindleheadmt),file('/export/starexec/sandbox/benchmark/theBenchmark.p', just4)).
% 0.76/0.93 cnf(c261,plain,genlmt(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988)),c_translation_0_885),c_machinelearningspindleheadmt),inference(split_conjunct,[status(thm)],[just4])).
% 0.76/0.93 cnf(c435,plain,~mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988)),c_translation_0_885))|mtvisible(c_machinelearningspindleheadmt),inference(resolution,[status(thm)],[c261, c35])).
% 0.76/0.93 cnf(c483,plain,mtvisible(c_machinelearningspindleheadmt),inference(resolution,[status(thm)],[c435, c5])).
% 0.76/0.93 cnf(c487,plain,mtvisible(c_currentworlddatacollectormt_nonhomocentric),inference(resolution,[status(thm)],[c483, c427])).
% 0.76/0.93 cnf(c494,plain,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),inference(resolution,[status(thm)],[c487, c428])).
% 0.76/0.93 cnf(c530,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))),inference(resolution,[status(thm)],[c494, c6])).
% 0.76/0.93 fof(just53,axiom,(![X]:(isa(X,c_tptpcol_16_27189)=>tptpcol_16_27189(X))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', just53)).
% 0.76/0.93 fof(c126,plain,(![X]:(~isa(X,c_tptpcol_16_27189)|tptpcol_16_27189(X))),inference(fof_nnf,[status(thm)],[just53])).
% 0.76/0.93 fof(c127,plain,(![X87]:(~isa(X87,c_tptpcol_16_27189)|tptpcol_16_27189(X87))),inference(variable_rename,[status(thm)],[c126])).
% 0.76/0.93 cnf(c128,plain,~isa(X286,c_tptpcol_16_27189)|tptpcol_16_27189(X286),inference(split_conjunct,[status(thm)],[c127])).
% 0.76/0.93 fof(just6,axiom,(![TERM]:(![INDEPCOL]:(![PRED]:(![DEPCOL]:((isa(TERM,INDEPCOL)&relationexistsall(PRED,DEPCOL,INDEPCOL))=>isa(f_relationexistsallfn(TERM,PRED,DEPCOL,INDEPCOL),DEPCOL)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', just6)).
% 0.76/0.93 fof(c257,plain,(![TERM]:(![INDEPCOL]:(![PRED]:(![DEPCOL]:((~isa(TERM,INDEPCOL)|~relationexistsall(PRED,DEPCOL,INDEPCOL))|isa(f_relationexistsallfn(TERM,PRED,DEPCOL,INDEPCOL),DEPCOL)))))),inference(fof_nnf,[status(thm)],[just6])).
% 0.76/0.93 fof(c258,plain,(![X170]:(![X171]:(![X172]:(![X173]:((~isa(X170,X171)|~relationexistsall(X172,X173,X171))|isa(f_relationexistsallfn(X170,X172,X173,X171),X173)))))),inference(variable_rename,[status(thm)],[c257])).
% 0.76/0.93 cnf(c259,plain,~isa(X362,X363)|~relationexistsall(X361,X360,X363)|isa(f_relationexistsallfn(X362,X361,X360,X363),X360),inference(split_conjunct,[status(thm)],[c258])).
% 0.76/0.93 fof(just14,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', just14)).
% 0.76/0.93 fof(c246,plain,(~mtvisible(c_currentworlddatacollectormt_nonhomocentric)|relationexistsall(c_tptp_9_51,c_tptpcol_16_27189,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma))),inference(fof_nnf,[status(thm)],[just14])).
% 0.76/0.93 cnf(c247,plain,~mtvisible(c_currentworlddatacollectormt_nonhomocentric)|relationexistsall(c_tptp_9_51,c_tptpcol_16_27189,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)),inference(split_conjunct,[status(thm)],[c246])).
% 0.76/0.93 cnf(c495,plain,relationexistsall(c_tptp_9_51,c_tptpcol_16_27189,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)),inference(resolution,[status(thm)],[c487, c247])).
% 0.76/0.93 cnf(c522,plain,~isa(X399,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma))|isa(f_relationexistsallfn(X399,c_tptp_9_51,c_tptpcol_16_27189,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)),c_tptpcol_16_27189),inference(resolution,[status(thm)],[c495, c259])).
% 0.76/0.93 cnf(c535,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),inference(resolution,[status(thm)],[c522, c245])).
% 0.76/0.93 cnf(c537,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))),inference(resolution,[status(thm)],[c535, c128])).
% 0.76/0.93 cnf(c539,plain,$false,inference(resolution,[status(thm)],[c537, c530])).
% 0.76/0.93 % SZS output end CNFRefutation
% 0.76/0.93
% 0.76/0.93 % Initial clauses : 96
% 0.76/0.93 % Processed clauses : 194
% 0.76/0.93 % Factors computed : 4
% 0.76/0.93 % Resolvents computed: 272
% 0.76/0.93 % Tautologies deleted: 23
% 0.76/0.93 % Forward subsumed : 152
% 0.76/0.93 % Backward subsumed : 16
% 0.76/0.93 % -------- CPU Time ---------
% 0.76/0.93 % User time : 0.554 s
% 0.76/0.93 % System time : 0.019 s
% 0.76/0.93 % Total time : 0.573 s
%------------------------------------------------------------------------------