%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NUM458+1 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n025.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:51 EDT 2024
% Result : Theorem 1.53s 1.73s
% Output : Refutation 1.53s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : NUM458+1 : TPTP v8.1.2. Released v4.0.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n025.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 : Wed May 8 15:56:08 EDT 2024
% 0.13/0.35 % CPUTime :
% 1.53/1.73 % Version: 1.5
% 1.53/1.73 % SZS status Theorem
% 1.53/1.73 % SZS output start CNFRefutation
% 1.53/1.73 fof(m__,conjecture,sdtlseqdt0(xm,xm),file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__)).
% 1.53/1.73 fof(c5,negated_conjecture,(~sdtlseqdt0(xm,xm)),inference(assume_negation,[status(cth)],[m__])).
% 1.53/1.73 fof(c6,negated_conjecture,~sdtlseqdt0(xm,xm),inference(fof_simplification,[status(thm)],[c5])).
% 1.53/1.73 cnf(c7,negated_conjecture,~sdtlseqdt0(xm,xm),inference(split_conjunct,[status(thm)],[c6])).
% 1.53/1.73 fof(m__718,plain,aNaturalNumber0(xm),file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__718)).
% 1.53/1.73 cnf(c8,plain,aNaturalNumber0(xm),inference(split_conjunct,[status(thm)],[m__718])).
% 1.53/1.73 fof(mSortsC,axiom,aNaturalNumber0(sz00),file('/export/starexec/sandbox/benchmark/theBenchmark.p', mSortsC)).
% 1.53/1.73 cnf(c84,plain,aNaturalNumber0(sz00),inference(split_conjunct,[status(thm)],[mSortsC])).
% 1.53/1.73 fof(m_AddZero,axiom,(![W0]:(aNaturalNumber0(W0)=>(sdtpldt0(W0,sz00)=W0&W0=sdtpldt0(sz00,W0)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', m_AddZero)).
% 1.53/1.73 fof(c65,plain,(![W0]:(~aNaturalNumber0(W0)|(sdtpldt0(W0,sz00)=W0&W0=sdtpldt0(sz00,W0)))),inference(fof_nnf,[status(thm)],[m_AddZero])).
% 1.53/1.74 fof(c66,plain,(![X30]:(~aNaturalNumber0(X30)|(sdtpldt0(X30,sz00)=X30&X30=sdtpldt0(sz00,X30)))),inference(variable_rename,[status(thm)],[c65])).
% 1.53/1.74 fof(c67,plain,(![X30]:((~aNaturalNumber0(X30)|sdtpldt0(X30,sz00)=X30)&(~aNaturalNumber0(X30)|X30=sdtpldt0(sz00,X30)))),inference(distribute,[status(thm)],[c66])).
% 1.53/1.74 cnf(c68,plain,~aNaturalNumber0(X71)|sdtpldt0(X71,sz00)=X71,inference(split_conjunct,[status(thm)],[c67])).
% 1.53/1.74 cnf(c165,plain,sdtpldt0(xm,sz00)=xm,inference(resolution,[status(thm)],[c68, c8])).
% 1.53/1.74 fof(mDefLE,plain,(![W0]:(![W1]:((aNaturalNumber0(W0)&aNaturalNumber0(W1))=>(sdtlseqdt0(W0,W1)<=>(?[W2]:(aNaturalNumber0(W2)&sdtpldt0(W0,W2)=W1)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', mDefLE)).
% 1.53/1.74 fof(c17,plain,(![W0]:(![W1]:((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|((~sdtlseqdt0(W0,W1)|(?[W2]:(aNaturalNumber0(W2)&sdtpldt0(W0,W2)=W1)))&((![W2]:(~aNaturalNumber0(W2)|sdtpldt0(W0,W2)!=W1))|sdtlseqdt0(W0,W1)))))),inference(fof_nnf,[status(thm)],[mDefLE])).
% 1.53/1.74 fof(c18,plain,(![X6]:(![X7]:((~aNaturalNumber0(X6)|~aNaturalNumber0(X7))|((~sdtlseqdt0(X6,X7)|(?[X8]:(aNaturalNumber0(X8)&sdtpldt0(X6,X8)=X7)))&((![X9]:(~aNaturalNumber0(X9)|sdtpldt0(X6,X9)!=X7))|sdtlseqdt0(X6,X7)))))),inference(variable_rename,[status(thm)],[c17])).
% 1.53/1.74 fof(c20,plain,(![X6]:(![X7]:(![X9]:((~aNaturalNumber0(X6)|~aNaturalNumber0(X7))|((~sdtlseqdt0(X6,X7)|(aNaturalNumber0(skolem0001(X6,X7))&sdtpldt0(X6,skolem0001(X6,X7))=X7))&((~aNaturalNumber0(X9)|sdtpldt0(X6,X9)!=X7)|sdtlseqdt0(X6,X7))))))),inference(shift_quantors,[status(thm)],[fof(c19,plain,(![X6]:(![X7]:((~aNaturalNumber0(X6)|~aNaturalNumber0(X7))|((~sdtlseqdt0(X6,X7)|(aNaturalNumber0(skolem0001(X6,X7))&sdtpldt0(X6,skolem0001(X6,X7))=X7))&((![X9]:(~aNaturalNumber0(X9)|sdtpldt0(X6,X9)!=X7))|sdtlseqdt0(X6,X7)))))),inference(skolemize,[status(esa)],[c18])).])).
% 1.53/1.74 fof(c21,plain,(![X6]:(![X7]:(![X9]:((((~aNaturalNumber0(X6)|~aNaturalNumber0(X7))|(~sdtlseqdt0(X6,X7)|aNaturalNumber0(skolem0001(X6,X7))))&((~aNaturalNumber0(X6)|~aNaturalNumber0(X7))|(~sdtlseqdt0(X6,X7)|sdtpldt0(X6,skolem0001(X6,X7))=X7)))&((~aNaturalNumber0(X6)|~aNaturalNumber0(X7))|((~aNaturalNumber0(X9)|sdtpldt0(X6,X9)!=X7)|sdtlseqdt0(X6,X7))))))),inference(distribute,[status(thm)],[c20])).
% 1.53/1.74 cnf(c24,plain,~aNaturalNumber0(X88)|~aNaturalNumber0(X90)|~aNaturalNumber0(X89)|sdtpldt0(X88,X89)!=X90|sdtlseqdt0(X88,X90),inference(split_conjunct,[status(thm)],[c21])).
% 1.53/1.74 cnf(c277,plain,~aNaturalNumber0(xm)|~aNaturalNumber0(sz00)|sdtlseqdt0(xm,xm),inference(resolution,[status(thm)],[c24, c165])).
% 1.53/1.74 cnf(c4473,plain,~aNaturalNumber0(xm)|sdtlseqdt0(xm,xm),inference(resolution,[status(thm)],[c277, c84])).
% 1.53/1.74 cnf(c4474,plain,sdtlseqdt0(xm,xm),inference(resolution,[status(thm)],[c4473, c8])).
% 1.53/1.74 cnf(c4476,plain,$false,inference(resolution,[status(thm)],[c4474, c7])).
% 1.53/1.74 % SZS output end CNFRefutation
% 1.53/1.74
% 1.53/1.74 % Initial clauses : 41
% 1.53/1.74 % Processed clauses : 290
% 1.53/1.74 % Factors computed : 16
% 1.53/1.74 % Resolvents computed: 4376
% 1.53/1.74 % Tautologies deleted: 3
% 1.53/1.74 % Forward subsumed : 101
% 1.53/1.74 % Backward subsumed : 11
% 1.53/1.74 % -------- CPU Time ---------
% 1.53/1.74 % User time : 1.363 s
% 1.53/1.74 % System time : 0.018 s
% 1.53/1.74 % Total time : 1.381 s
%------------------------------------------------------------------------------