%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : CSR066+1 : TPTP v8.1.2. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n007.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:33 EDT 2024
% Result : Theorem 0.55s 0.73s
% Output : Refutation 0.55s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : CSR066+1 : TPTP v8.1.2. Released v3.4.0.
% 0.10/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.34 % Computer : n007.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Thu May 9 01:18:08 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.55/0.73 % Version: 1.5
% 0.55/0.73 % SZS status Theorem
% 0.55/0.73 % SZS output start CNFRefutation
% 0.55/0.73 fof(query66,conjecture,(?[X]:(mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_webnjiteducjohnsontreebiochhtm)),c_translation_21))=>(tptp_8_271(X,c_theprototypicalshavingrazor_manual)&tptpcol_16_25972(X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', query66)).
% 0.55/0.73 fof(c0,negated_conjecture,(~(?[X]:(mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_webnjiteducjohnsontreebiochhtm)),c_translation_21))=>(tptp_8_271(X,c_theprototypicalshavingrazor_manual)&tptpcol_16_25972(X))))),inference(assume_negation,[status(cth)],[query66])).
% 0.55/0.73 fof(c1,negated_conjecture,(![X]:(mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_webnjiteducjohnsontreebiochhtm)),c_translation_21))&(~tptp_8_271(X,c_theprototypicalshavingrazor_manual)|~tptpcol_16_25972(X)))),inference(fof_nnf,[status(thm)],[c0])).
% 0.55/0.73 fof(c2,negated_conjecture,(mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_webnjiteducjohnsontreebiochhtm)),c_translation_21))&(![X]:(~tptp_8_271(X,c_theprototypicalshavingrazor_manual)|~tptpcol_16_25972(X)))),inference(shift_quantors,[status(thm)],[c1])).
% 0.55/0.73 fof(c4,negated_conjecture,(![X2]:(mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_webnjiteducjohnsontreebiochhtm)),c_translation_21))&(~tptp_8_271(X2,c_theprototypicalshavingrazor_manual)|~tptpcol_16_25972(X2)))),inference(shift_quantors,[status(thm)],[fof(c3,negated_conjecture,(mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_webnjiteducjohnsontreebiochhtm)),c_translation_21))&(![X2]:(~tptp_8_271(X2,c_theprototypicalshavingrazor_manual)|~tptpcol_16_25972(X2)))),inference(variable_rename,[status(thm)],[c2])).])).
% 0.55/0.73 cnf(c6,negated_conjecture,~tptp_8_271(X140,c_theprototypicalshavingrazor_manual)|~tptpcol_16_25972(X140),inference(split_conjunct,[status(thm)],[c4])).
% 0.55/0.73 fof(just11,axiom,shavingrazor_manual(c_theprototypicalshavingrazor_manual),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just11)).
% 0.55/0.73 cnf(c197,plain,shavingrazor_manual(c_theprototypicalshavingrazor_manual),inference(split_conjunct,[status(thm)],[just11])).
% 0.55/0.73 fof(just9,axiom,(![TERM]:(shavingrazor_manual(TERM)=>tptp_8_271(f_relationexistsallfn(TERM,c_tptp_8_271,c_tptpcol_16_25972,c_shavingrazor_manual),TERM))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just9)).
% 0.55/0.73 fof(c199,plain,(![TERM]:(~shavingrazor_manual(TERM)|tptp_8_271(f_relationexistsallfn(TERM,c_tptp_8_271,c_tptpcol_16_25972,c_shavingrazor_manual),TERM))),inference(fof_nnf,[status(thm)],[just9])).
% 0.55/0.73 fof(c200,plain,(![X131]:(~shavingrazor_manual(X131)|tptp_8_271(f_relationexistsallfn(X131,c_tptp_8_271,c_tptpcol_16_25972,c_shavingrazor_manual),X131))),inference(variable_rename,[status(thm)],[c199])).
% 0.55/0.73 cnf(c201,plain,~shavingrazor_manual(X278)|tptp_8_271(f_relationexistsallfn(X278,c_tptp_8_271,c_tptpcol_16_25972,c_shavingrazor_manual),X278),inference(split_conjunct,[status(thm)],[c200])).
% 0.55/0.73 cnf(c308,plain,tptp_8_271(f_relationexistsallfn(c_theprototypicalshavingrazor_manual,c_tptp_8_271,c_tptpcol_16_25972,c_shavingrazor_manual),c_theprototypicalshavingrazor_manual),inference(resolution,[status(thm)],[c201, c197])).
% 0.55/0.73 cnf(c328,plain,~tptpcol_16_25972(f_relationexistsallfn(c_theprototypicalshavingrazor_manual,c_tptp_8_271,c_tptpcol_16_25972,c_shavingrazor_manual)),inference(resolution,[status(thm)],[c308, c6])).
% 0.55/0.73 fof(just32,axiom,(![X]:(isa(X,c_tptpcol_16_25972)=>tptpcol_16_25972(X))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just32)).
% 0.55/0.73 fof(c126,plain,(![X]:(~isa(X,c_tptpcol_16_25972)|tptpcol_16_25972(X))),inference(fof_nnf,[status(thm)],[just32])).
% 0.55/0.73 fof(c127,plain,(![X87]:(~isa(X87,c_tptpcol_16_25972)|tptpcol_16_25972(X87))),inference(variable_rename,[status(thm)],[c126])).
% 0.55/0.73 cnf(c128,plain,~isa(X224,c_tptpcol_16_25972)|tptpcol_16_25972(X224),inference(split_conjunct,[status(thm)],[c127])).
% 0.55/0.73 fof(just31,axiom,(![X]:(shavingrazor_manual(X)=>isa(X,c_shavingrazor_manual))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just31)).
% 0.55/0.73 fof(c129,plain,(![X]:(~shavingrazor_manual(X)|isa(X,c_shavingrazor_manual))),inference(fof_nnf,[status(thm)],[just31])).
% 0.55/0.73 fof(c130,plain,(![X88]:(~shavingrazor_manual(X88)|isa(X88,c_shavingrazor_manual))),inference(variable_rename,[status(thm)],[c129])).
% 0.55/0.73 cnf(c131,plain,~shavingrazor_manual(X225)|isa(X225,c_shavingrazor_manual),inference(split_conjunct,[status(thm)],[c130])).
% 0.55/0.73 cnf(c261,plain,isa(c_theprototypicalshavingrazor_manual,c_shavingrazor_manual),inference(resolution,[status(thm)],[c131, c197])).
% 0.55/0.73 fof(just10,axiom,relationexistsall(c_tptp_8_271,c_tptpcol_16_25972,c_shavingrazor_manual),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just10)).
% 0.55/0.73 cnf(c198,plain,relationexistsall(c_tptp_8_271,c_tptpcol_16_25972,c_shavingrazor_manual),inference(split_conjunct,[status(thm)],[just10])).
% 0.55/0.73 fof(just4,axiom,(![TERM]:(![INDEPCOL]:(![PRED]:(![DEPCOL]:((isa(TERM,INDEPCOL)&relationexistsall(PRED,DEPCOL,INDEPCOL))=>isa(f_relationexistsallfn(TERM,PRED,DEPCOL,INDEPCOL),DEPCOL)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just4)).
% 0.55/0.73 fof(c206,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)],[just4])).
% 0.55/0.73 fof(c207,plain,(![X132]:(![X133]:(![X134]:(![X135]:((~isa(X132,X133)|~relationexistsall(X134,X135,X133))|isa(f_relationexistsallfn(X132,X134,X135,X133),X135)))))),inference(variable_rename,[status(thm)],[c206])).
% 0.55/0.73 cnf(c208,plain,~isa(X284,X287)|~relationexistsall(X285,X286,X287)|isa(f_relationexistsallfn(X284,X285,X286,X287),X286),inference(split_conjunct,[status(thm)],[c207])).
% 0.55/0.73 cnf(c309,plain,~isa(X299,c_shavingrazor_manual)|isa(f_relationexistsallfn(X299,c_tptp_8_271,c_tptpcol_16_25972,c_shavingrazor_manual),c_tptpcol_16_25972),inference(resolution,[status(thm)],[c208, c198])).
% 0.55/0.73 cnf(c331,plain,isa(f_relationexistsallfn(c_theprototypicalshavingrazor_manual,c_tptp_8_271,c_tptpcol_16_25972,c_shavingrazor_manual),c_tptpcol_16_25972),inference(resolution,[status(thm)],[c309, c261])).
% 0.55/0.73 cnf(c361,plain,tptpcol_16_25972(f_relationexistsallfn(c_theprototypicalshavingrazor_manual,c_tptp_8_271,c_tptpcol_16_25972,c_shavingrazor_manual)),inference(resolution,[status(thm)],[c331, c128])).
% 0.55/0.73 cnf(c362,plain,$false,inference(resolution,[status(thm)],[c361, c328])).
% 0.55/0.73 % SZS output end CNFRefutation
% 0.55/0.73
% 0.55/0.73 % Initial clauses : 75
% 0.55/0.73 % Processed clauses : 124
% 0.55/0.73 % Factors computed : 3
% 0.55/0.73 % Resolvents computed: 149
% 0.55/0.73 % Tautologies deleted: 14
% 0.55/0.73 % Forward subsumed : 73
% 0.55/0.73 % Backward subsumed : 4
% 0.55/0.73 % -------- CPU Time ---------
% 0.55/0.73 % User time : 0.365 s
% 0.55/0.73 % System time : 0.012 s
% 0.55/0.73 % Total time : 0.377 s
%------------------------------------------------------------------------------