%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : CSR060+5 : TPTP v5.0.0. Bugfixed v3.5.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : art06.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 2018MB
% OS : Linux 2.6.26.8-57.fc8
% CPULimit : 300s
% DateTime : Sat Dec 25 06:34:00 EST 2010
% Result : Theorem 211.97s
% Output : CNFRefutation 219.19s
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----ERROR: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % SZS status Started for /home/graph/tptp/TPTP/Problems/CSR/CSR060+5.p
% --creating new selector for [CSR002+4.ax]
% -running prover on /tmp/tmp1AkQu_/sel_CSR060+5.p_1 with time limit 29
% -prover status CounterSatisfiable
% -running prover on /tmp/tmp1AkQu_/sel_CSR060+5.p_2 with time limit 60
% -prover status CounterSatisfiable
% --creating new selector for [CSR002+4.ax]
% -running prover on /tmp/tmp1AkQu_/sel_CSR060+5.p_3 with time limit 80
% -prover status CounterSatisfiable
% --creating new selector for [CSR002+4.ax]
% -running prover on /tmp/tmp1AkQu_/sel_CSR060+5.p_4 with time limit 85
% -prover status Theorem
% Problem CSR060+5.p solved in phase 3.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/CSR/CSR060+5.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/CSR/CSR060+5.p
% Solved 1 out of 1.
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(984, axiom,genlmt(c_machinelearningspindleheadmt,c_analystdatabasemt),file('/tmp/tmp1AkQu_/sel_CSR060+5.p_4', ax4_79089)).
% fof(1691, axiom,![X6]:(isa(X6,c_tptpcol_16_27189)=>tptpcol_16_27189(X6)),file('/tmp/tmp1AkQu_/sel_CSR060+5.p_4', ax4_521482)).
% fof(2567, axiom,(mtvisible(c_currentworlddatacollectormt_nonhomocentric)=>relationexistsall(c_tptp_9_51,c_tptpcol_16_27189,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma))),file('/tmp/tmp1AkQu_/sel_CSR060+5.p_4', ax4_237077)).
% fof(2967, axiom,genlmt(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988)),c_translation_0_885),c_machinelearningspindleheadmt),file('/tmp/tmp1AkQu_/sel_CSR060+5.p_4', ax4_25671)).
% fof(3479, axiom,genlmt(c_analystdatabasemt,c_currentworlddatacollectormt_nonhomocentric),file('/tmp/tmp1AkQu_/sel_CSR060+5.p_4', ax4_4153)).
% fof(4383, axiom,![X14]:![X15]:![X16]:![X17]:((isa(X14,X15)&relationexistsall(X16,X17,X15))=>isa(f_relationexistsallfn(X14,X16,X17,X15),X17)),file('/tmp/tmp1AkQu_/sel_CSR060+5.p_4', ax4_112328)).
% fof(4763, axiom,![X14]:((mtvisible(c_currentworlddatacollectormt_nonhomocentric)&isa(X14,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)))=>tptp_9_51(f_relationexistsallfn(X14,c_tptp_9_51,c_tptpcol_16_27189,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)),X14)),file('/tmp/tmp1AkQu_/sel_CSR060+5.p_4', ax4_11796)).
% fof(5373, axiom,isa(c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)),file('/tmp/tmp1AkQu_/sel_CSR060+5.p_4', ax4_307671)).
% fof(6036, axiom,![X18]:![X19]:((mtvisible(X18)&genlmt(X18,X19))=>mtvisible(X19)),file('/tmp/tmp1AkQu_/sel_CSR060+5.p_4', ax4_540220)).
% fof(8908, conjecture,?[X6]:(mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988)),c_translation_0_885))=>(tptp_9_51(X6,c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802)&tptpcol_16_27189(X6))),file('/tmp/tmp1AkQu_/sel_CSR060+5.p_4', query260)).
% fof(8909, negated_conjecture,~(?[X6]:(mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988)),c_translation_0_885))=>(tptp_9_51(X6,c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802)&tptpcol_16_27189(X6)))),inference(assume_negation,[status(cth)],[8908])).
% cnf(10459,plain,(genlmt(c_machinelearningspindleheadmt,c_analystdatabasemt)),inference(split_conjunct,[status(thm)],[984])).
% fof(11567, plain,![X6]:(~(isa(X6,c_tptpcol_16_27189))|tptpcol_16_27189(X6)),inference(fof_nnf,[status(thm)],[1691])).
% fof(11568, plain,![X7]:(~(isa(X7,c_tptpcol_16_27189))|tptpcol_16_27189(X7)),inference(variable_rename,[status(thm)],[11567])).
% cnf(11569,plain,(tptpcol_16_27189(X1)|~isa(X1,c_tptpcol_16_27189)),inference(split_conjunct,[status(thm)],[11568])).
% fof(12944, 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)],[2567])).
% cnf(12945,plain,(relationexistsall(c_tptp_9_51,c_tptpcol_16_27189,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma))|~mtvisible(c_currentworlddatacollectormt_nonhomocentric)),inference(split_conjunct,[status(thm)],[12944])).
% cnf(13542,plain,(genlmt(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988)),c_translation_0_885),c_machinelearningspindleheadmt)),inference(split_conjunct,[status(thm)],[2967])).
% cnf(14312,plain,(genlmt(c_analystdatabasemt,c_currentworlddatacollectormt_nonhomocentric)),inference(split_conjunct,[status(thm)],[3479])).
% fof(15742, plain,![X14]:![X15]:![X16]:![X17]:((~(isa(X14,X15))|~(relationexistsall(X16,X17,X15)))|isa(f_relationexistsallfn(X14,X16,X17,X15),X17)),inference(fof_nnf,[status(thm)],[4383])).
% fof(15743, plain,![X18]:![X19]:![X20]:![X21]:((~(isa(X18,X19))|~(relationexistsall(X20,X21,X19)))|isa(f_relationexistsallfn(X18,X20,X21,X19),X21)),inference(variable_rename,[status(thm)],[15742])).
% cnf(15744,plain,(isa(f_relationexistsallfn(X1,X2,X3,X4),X3)|~relationexistsall(X2,X3,X4)|~isa(X1,X4)),inference(split_conjunct,[status(thm)],[15743])).
% fof(16317, plain,![X14]:((~(mtvisible(c_currentworlddatacollectormt_nonhomocentric))|~(isa(X14,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma))))|tptp_9_51(f_relationexistsallfn(X14,c_tptp_9_51,c_tptpcol_16_27189,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)),X14)),inference(fof_nnf,[status(thm)],[4763])).
% fof(16318, plain,![X15]:((~(mtvisible(c_currentworlddatacollectormt_nonhomocentric))|~(isa(X15,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma))))|tptp_9_51(f_relationexistsallfn(X15,c_tptp_9_51,c_tptpcol_16_27189,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)),X15)),inference(variable_rename,[status(thm)],[16317])).
% cnf(16319,plain,(tptp_9_51(f_relationexistsallfn(X1,c_tptp_9_51,c_tptpcol_16_27189,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)),X1)|~isa(X1,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma))|~mtvisible(c_currentworlddatacollectormt_nonhomocentric)),inference(split_conjunct,[status(thm)],[16318])).
% cnf(17280,plain,(isa(c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma))),inference(split_conjunct,[status(thm)],[5373])).
% fof(18255, plain,![X18]:![X19]:((~(mtvisible(X18))|~(genlmt(X18,X19)))|mtvisible(X19)),inference(fof_nnf,[status(thm)],[6036])).
% fof(18256, plain,![X20]:![X21]:((~(mtvisible(X20))|~(genlmt(X20,X21)))|mtvisible(X21)),inference(variable_rename,[status(thm)],[18255])).
% cnf(18257,plain,(mtvisible(X1)|~genlmt(X2,X1)|~mtvisible(X2)),inference(split_conjunct,[status(thm)],[18256])).
% fof(22695, negated_conjecture,![X6]:(mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988)),c_translation_0_885))&(~(tptp_9_51(X6,c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802))|~(tptpcol_16_27189(X6)))),inference(fof_nnf,[status(thm)],[8909])).
% fof(22696, negated_conjecture,![X7]:(mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988)),c_translation_0_885))&(~(tptp_9_51(X7,c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802))|~(tptpcol_16_27189(X7)))),inference(variable_rename,[status(thm)],[22695])).
% cnf(22697,negated_conjecture,(~tptpcol_16_27189(X1)|~tptp_9_51(X1,c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802)),inference(split_conjunct,[status(thm)],[22696])).
% cnf(22698,negated_conjecture,(mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988)),c_translation_0_885))),inference(split_conjunct,[status(thm)],[22696])).
% cnf(23136,negated_conjecture,(~tptp_9_51(X1,c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802)|~isa(X1,c_tptpcol_16_27189)),inference(spm,[status(thm)],[22697,11569,theory(equality)])).
% cnf(23349,plain,(mtvisible(c_analystdatabasemt)|~mtvisible(c_machinelearningspindleheadmt)),inference(spm,[status(thm)],[18257,10459,theory(equality)])).
% cnf(23386,plain,(mtvisible(c_currentworlddatacollectormt_nonhomocentric)|~mtvisible(c_analystdatabasemt)),inference(spm,[status(thm)],[18257,14312,theory(equality)])).
% cnf(25920,plain,(mtvisible(c_machinelearningspindleheadmt)|~mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988)),c_tr
% anslation_0_885))),inference(spm,[status(thm)],[18257,13542,theory(equality)])).
% cnf(25923,plain,(mtvisible(c_machinelearningspindleheadmt)|$false),inference(rw,[status(thm)],[25920,22698,theory(equality)])).
% cnf(25924,plain,(mtvisible(c_machinelearningspindleheadmt)),inference(cn,[status(thm)],[25923,theory(equality)])).
% cnf(57516,plain,(mtvisible(c_analystdatabasemt)|$false),inference(rw,[status(thm)],[23349,25924,theory(equality)])).
% cnf(57517,plain,(mtvisible(c_analystdatabasemt)),inference(cn,[status(thm)],[57516,theory(equality)])).
% cnf(57691,plain,(mtvisible(c_currentworlddatacollectormt_nonhomocentric)|$false),inference(rw,[status(thm)],[23386,57517,theory(equality)])).
% cnf(57692,plain,(mtvisible(c_currentworlddatacollectormt_nonhomocentric)),inference(cn,[status(thm)],[57691,theory(equality)])).
% cnf(57693,plain,(tptp_9_51(f_relationexistsallfn(X1,c_tptp_9_51,c_tptpcol_16_27189,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)),X1)|$false|~isa(X1,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma))),inference(rw,[status(thm)],[16319,57692,theory(equality)])).
% cnf(57694,plain,(tptp_9_51(f_relationexistsallfn(X1,c_tptp_9_51,c_tptpcol_16_27189,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)),X1)|~isa(X1,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma))),inference(cn,[status(thm)],[57693,theory(equality)])).
% cnf(57695,plain,(relationexistsall(c_tptp_9_51,c_tptpcol_16_27189,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma))|$false),inference(rw,[status(thm)],[12945,57692,theory(equality)])).
% cnf(57696,plain,(relationexistsall(c_tptp_9_51,c_tptpcol_16_27189,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma))),inference(cn,[status(thm)],[57695,theory(equality)])).
% cnf(57876,negated_conjecture,(~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)|~isa(c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma))),inference(spm,[status(thm)],[23136,57694,theory(equality)])).
% cnf(57877,negated_conjecture,(~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)|$false),inference(rw,[status(thm)],[57876,17280,theory(equality)])).
% cnf(57878,negated_conjecture,(~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(cn,[status(thm)],[57877,theory(equality)])).
% cnf(68213,negated_conjecture,(~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))),inference(spm,[status(thm)],[57878,15744,theory(equality)])).
% cnf(68214,negated_conjecture,($false|~isa(c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma))),inference(rw,[status(thm)],[68213,57696,theory(equality)])).
% cnf(68215,negated_conjecture,($false|$false),inference(rw,[status(thm)],[68214,17280,theory(equality)])).
% cnf(68216,negated_conjecture,($false),inference(cn,[status(thm)],[68215,theory(equality)])).
% cnf(68217,negated_conjecture,($false),68216,['proof']).
% # SZS output end CNFRefutation
%
%------------------------------------------------------------------------------