%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NUM464+2 : TPTP v8.1.2. Released v4.0.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:35:53 EDT 2024
% Result : Theorem 4.35s 4.52s
% Output : Refutation 4.35s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : NUM464+2 : TPTP v8.1.2. Released v4.0.0.
% 0.07/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 : Wed May 8 16:56:23 EDT 2024
% 0.12/0.34 % CPUTime :
% 4.35/4.52 % Version: 1.5
% 4.35/4.52 % SZS status Theorem
% 4.35/4.52 % SZS output start CNFRefutation
% 4.35/4.52 fof(m__,conjecture,(xm!=sz00=>((?[W0]:(aNaturalNumber0(W0)&sdtpldt0(sz10,W0)=xm))|sdtlseqdt0(sz10,xm))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__)).
% 4.35/4.52 fof(c5,negated_conjecture,(~(xm!=sz00=>((?[W0]:(aNaturalNumber0(W0)&sdtpldt0(sz10,W0)=xm))|sdtlseqdt0(sz10,xm)))),inference(assume_negation,[status(cth)],[m__])).
% 4.35/4.52 fof(c6,negated_conjecture,(xm!=sz00&((![W0]:(~aNaturalNumber0(W0)|sdtpldt0(sz10,W0)!=xm))&~sdtlseqdt0(sz10,xm))),inference(fof_nnf,[status(thm)],[c5])).
% 4.35/4.52 fof(c8,negated_conjecture,(![X2]:(xm!=sz00&((~aNaturalNumber0(X2)|sdtpldt0(sz10,X2)!=xm)&~sdtlseqdt0(sz10,xm)))),inference(shift_quantors,[status(thm)],[fof(c7,negated_conjecture,(xm!=sz00&((![X2]:(~aNaturalNumber0(X2)|sdtpldt0(sz10,X2)!=xm))&~sdtlseqdt0(sz10,xm))),inference(variable_rename,[status(thm)],[c6])).])).
% 4.35/4.52 cnf(c11,negated_conjecture,~sdtlseqdt0(sz10,xm),inference(split_conjunct,[status(thm)],[c8])).
% 4.35/4.52 cnf(reflexivity,axiom,X56=X56,theory(equality)).
% 4.35/4.52 fof(m__987,plain,(aNaturalNumber0(xm)&aNaturalNumber0(xn)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__987)).
% 4.35/4.52 cnf(c12,plain,aNaturalNumber0(xm),inference(split_conjunct,[status(thm)],[m__987])).
% 4.35/4.52 fof(mLERefl,axiom,(![W0]:(aNaturalNumber0(W0)=>sdtlseqdt0(W0,W0))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', mLERefl)).
% 4.35/4.52 fof(c45,plain,(![W0]:(~aNaturalNumber0(W0)|sdtlseqdt0(W0,W0))),inference(fof_nnf,[status(thm)],[mLERefl])).
% 4.35/4.52 fof(c46,plain,(![X17]:(~aNaturalNumber0(X17)|sdtlseqdt0(X17,X17))),inference(variable_rename,[status(thm)],[c45])).
% 4.35/4.52 cnf(c47,plain,~aNaturalNumber0(X63)|sdtlseqdt0(X63,X63),inference(split_conjunct,[status(thm)],[c46])).
% 4.35/4.52 cnf(c132,plain,sdtlseqdt0(xm,xm),inference(resolution,[status(thm)],[c47, c12])).
% 4.35/4.52 cnf(c4,axiom,X84!=X85|X83!=X86|~sdtlseqdt0(X84,X83)|sdtlseqdt0(X85,X86),theory(equality)).
% 4.35/4.52 cnf(c193,plain,xm!=X285|xm!=X284|sdtlseqdt0(X285,X284),inference(resolution,[status(thm)],[c4, c132])).
% 4.35/4.52 cnf(c7730,plain,xm!=X293|sdtlseqdt0(X293,xm),inference(resolution,[status(thm)],[c193, reflexivity])).
% 4.35/4.52 cnf(c9,negated_conjecture,xm!=sz00,inference(split_conjunct,[status(thm)],[c8])).
% 4.35/4.52 fof(mLENTr,axiom,(![W0]:(aNaturalNumber0(W0)=>((W0=sz00|W0=sz10)|(sz10!=W0&sdtlseqdt0(sz10,W0))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', mLENTr)).
% 4.35/4.52 fof(c14,plain,(![W0]:(~aNaturalNumber0(W0)|((W0=sz00|W0=sz10)|(sz10!=W0&sdtlseqdt0(sz10,W0))))),inference(fof_nnf,[status(thm)],[mLENTr])).
% 4.35/4.52 fof(c15,plain,(![X3]:(~aNaturalNumber0(X3)|((X3=sz00|X3=sz10)|(sz10!=X3&sdtlseqdt0(sz10,X3))))),inference(variable_rename,[status(thm)],[c14])).
% 4.35/4.52 fof(c16,plain,(![X3]:((~aNaturalNumber0(X3)|((X3=sz00|X3=sz10)|sz10!=X3))&(~aNaturalNumber0(X3)|((X3=sz00|X3=sz10)|sdtlseqdt0(sz10,X3))))),inference(distribute,[status(thm)],[c15])).
% 4.35/4.52 cnf(c18,plain,~aNaturalNumber0(X91)|X91=sz00|X91=sz10|sdtlseqdt0(sz10,X91),inference(split_conjunct,[status(thm)],[c16])).
% 4.35/4.52 cnf(c249,plain,xm=sz00|xm=sz10|sdtlseqdt0(sz10,xm),inference(resolution,[status(thm)],[c18, c12])).
% 4.35/4.52 cnf(c13083,plain,xm=sz10|sdtlseqdt0(sz10,xm),inference(resolution,[status(thm)],[c249, c9])).
% 4.35/4.52 cnf(c13215,plain,sdtlseqdt0(sz10,xm),inference(resolution,[status(thm)],[c13083, c7730])).
% 4.35/4.52 cnf(c13270,plain,$false,inference(resolution,[status(thm)],[c13215, c11])).
% 4.35/4.52 % SZS output end CNFRefutation
% 4.35/4.52
% 4.35/4.52 % Initial clauses : 59
% 4.35/4.52 % Processed clauses : 553
% 4.35/4.52 % Factors computed : 23
% 4.35/4.52 % Resolvents computed: 13125
% 4.35/4.52 % Tautologies deleted: 4
% 4.35/4.52 % Forward subsumed : 129
% 4.35/4.52 % Backward subsumed : 12
% 4.35/4.52 % -------- CPU Time ---------
% 4.35/4.52 % User time : 4.115 s
% 4.35/4.52 % System time : 0.042 s
% 4.35/4.52 % Total time : 4.157 s
%------------------------------------------------------------------------------