%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NUM476+2 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n013.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:55 EDT 2024
% Result : Theorem 195.27s 195.46s
% Output : Refutation 195.27s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : NUM476+2 : TPTP v8.1.2. Released v4.0.0.
% 0.07/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.36 % Computer : n013.cluster.edu
% 0.15/0.36 % Model : x86_64 x86_64
% 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.36 % Memory : 8042.1875MB
% 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.36 % CPULimit : 300
% 0.15/0.36 % WCLimit : 300
% 0.15/0.36 % DateTime : Wed May 8 16:53:23 EDT 2024
% 0.15/0.36 % CPUTime :
% 195.27/195.46 % Version: 1.5
% 195.27/195.46 % SZS status Theorem
% 195.27/195.46 % SZS output start CNFRefutation
% 195.27/195.46 fof(m__,conjecture,((xl!=sz00=>(?[W0]:(((aNaturalNumber0(W0)&xm=sdtasdt0(xl,W0))&W0=sdtsldt0(xm,xl))&(?[W1]:(((((aNaturalNumber0(W1)&sdtpldt0(xm,xn)=sdtasdt0(xl,W1))&W1=sdtsldt0(sdtpldt0(xm,xn),xl))&(?[W2]:(aNaturalNumber0(W2)&sdtpldt0(W0,W2)=W1)))&sdtlseqdt0(W0,W1))&(?[W2]:((((aNaturalNumber0(W2)&sdtpldt0(W0,W2)=W1)&W2=sdtmndt0(W1,W0))&sdtpldt0(sdtasdt0(xl,W0),sdtasdt0(xl,W2))=sdtpldt0(sdtasdt0(xl,W0),xn))&xn=sdtasdt0(xl,W2))))))))=>((?[W0]:(aNaturalNumber0(W0)&xn=sdtasdt0(xl,W0)))|doDivides0(xl,xn))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__)).
% 195.27/195.46 fof(c8,negated_conjecture,(~((xl!=sz00=>(?[W0]:(((aNaturalNumber0(W0)&xm=sdtasdt0(xl,W0))&W0=sdtsldt0(xm,xl))&(?[W1]:(((((aNaturalNumber0(W1)&sdtpldt0(xm,xn)=sdtasdt0(xl,W1))&W1=sdtsldt0(sdtpldt0(xm,xn),xl))&(?[W2]:(aNaturalNumber0(W2)&sdtpldt0(W0,W2)=W1)))&sdtlseqdt0(W0,W1))&(?[W2]:((((aNaturalNumber0(W2)&sdtpldt0(W0,W2)=W1)&W2=sdtmndt0(W1,W0))&sdtpldt0(sdtasdt0(xl,W0),sdtasdt0(xl,W2))=sdtpldt0(sdtasdt0(xl,W0),xn))&xn=sdtasdt0(xl,W2))))))))=>((?[W0]:(aNaturalNumber0(W0)&xn=sdtasdt0(xl,W0)))|doDivides0(xl,xn)))),inference(assume_negation,[status(cth)],[m__])).
% 195.27/195.46 fof(c9,negated_conjecture,((xl=sz00|(?[W0]:(((aNaturalNumber0(W0)&xm=sdtasdt0(xl,W0))&W0=sdtsldt0(xm,xl))&(?[W1]:(((((aNaturalNumber0(W1)&sdtpldt0(xm,xn)=sdtasdt0(xl,W1))&W1=sdtsldt0(sdtpldt0(xm,xn),xl))&(?[W2]:(aNaturalNumber0(W2)&sdtpldt0(W0,W2)=W1)))&sdtlseqdt0(W0,W1))&(?[W2]:((((aNaturalNumber0(W2)&sdtpldt0(W0,W2)=W1)&W2=sdtmndt0(W1,W0))&sdtpldt0(sdtasdt0(xl,W0),sdtasdt0(xl,W2))=sdtpldt0(sdtasdt0(xl,W0),xn))&xn=sdtasdt0(xl,W2))))))))&((![W0]:(~aNaturalNumber0(W0)|xn!=sdtasdt0(xl,W0)))&~doDivides0(xl,xn))),inference(fof_nnf,[status(thm)],[c8])).
% 195.27/195.46 fof(c10,negated_conjecture,((xl=sz00|(?[X2]:(((aNaturalNumber0(X2)&xm=sdtasdt0(xl,X2))&X2=sdtsldt0(xm,xl))&(?[X3]:(((((aNaturalNumber0(X3)&sdtpldt0(xm,xn)=sdtasdt0(xl,X3))&X3=sdtsldt0(sdtpldt0(xm,xn),xl))&(?[X4]:(aNaturalNumber0(X4)&sdtpldt0(X2,X4)=X3)))&sdtlseqdt0(X2,X3))&(?[X5]:((((aNaturalNumber0(X5)&sdtpldt0(X2,X5)=X3)&X5=sdtmndt0(X3,X2))&sdtpldt0(sdtasdt0(xl,X2),sdtasdt0(xl,X5))=sdtpldt0(sdtasdt0(xl,X2),xn))&xn=sdtasdt0(xl,X5))))))))&((![X6]:(~aNaturalNumber0(X6)|xn!=sdtasdt0(xl,X6)))&~doDivides0(xl,xn))),inference(variable_rename,[status(thm)],[c9])).
% 195.27/195.46 fof(c12,negated_conjecture,(![X6]:((xl=sz00|(((aNaturalNumber0(skolem0001)&xm=sdtasdt0(xl,skolem0001))&skolem0001=sdtsldt0(xm,xl))&(((((aNaturalNumber0(skolem0002)&sdtpldt0(xm,xn)=sdtasdt0(xl,skolem0002))&skolem0002=sdtsldt0(sdtpldt0(xm,xn),xl))&(aNaturalNumber0(skolem0003)&sdtpldt0(skolem0001,skolem0003)=skolem0002))&sdtlseqdt0(skolem0001,skolem0002))&((((aNaturalNumber0(skolem0004)&sdtpldt0(skolem0001,skolem0004)=skolem0002)&skolem0004=sdtmndt0(skolem0002,skolem0001))&sdtpldt0(sdtasdt0(xl,skolem0001),sdtasdt0(xl,skolem0004))=sdtpldt0(sdtasdt0(xl,skolem0001),xn))&xn=sdtasdt0(xl,skolem0004)))))&((~aNaturalNumber0(X6)|xn!=sdtasdt0(xl,X6))&~doDivides0(xl,xn)))),inference(shift_quantors,[status(thm)],[fof(c11,negated_conjecture,((xl=sz00|(((aNaturalNumber0(skolem0001)&xm=sdtasdt0(xl,skolem0001))&skolem0001=sdtsldt0(xm,xl))&(((((aNaturalNumber0(skolem0002)&sdtpldt0(xm,xn)=sdtasdt0(xl,skolem0002))&skolem0002=sdtsldt0(sdtpldt0(xm,xn),xl))&(aNaturalNumber0(skolem0003)&sdtpldt0(skolem0001,skolem0003)=skolem0002))&sdtlseqdt0(skolem0001,skolem0002))&((((aNaturalNumber0(skolem0004)&sdtpldt0(skolem0001,skolem0004)=skolem0002)&skolem0004=sdtmndt0(skolem0002,skolem0001))&sdtpldt0(sdtasdt0(xl,skolem0001),sdtasdt0(xl,skolem0004))=sdtpldt0(sdtasdt0(xl,skolem0001),xn))&xn=sdtasdt0(xl,skolem0004)))))&((![X6]:(~aNaturalNumber0(X6)|xn!=sdtasdt0(xl,X6)))&~doDivides0(xl,xn))),inference(skolemize,[status(esa)],[c10])).])).
% 195.27/195.46 fof(c13,negated_conjecture,(![X6]:(((((xl=sz00|aNaturalNumber0(skolem0001))&(xl=sz00|xm=sdtasdt0(xl,skolem0001)))&(xl=sz00|skolem0001=sdtsldt0(xm,xl)))&((((((xl=sz00|aNaturalNumber0(skolem0002))&(xl=sz00|sdtpldt0(xm,xn)=sdtasdt0(xl,skolem0002)))&(xl=sz00|skolem0002=sdtsldt0(sdtpldt0(xm,xn),xl)))&((xl=sz00|aNaturalNumber0(skolem0003))&(xl=sz00|sdtpldt0(skolem0001,skolem0003)=skolem0002)))&(xl=sz00|sdtlseqdt0(skolem0001,skolem0002)))&(((((xl=sz00|aNaturalNumber0(skolem0004))&(xl=sz00|sdtpldt0(skolem0001,skolem0004)=skolem0002))&(xl=sz00|skolem0004=sdtmndt0(skolem0002,skolem0001)))&(xl=sz00|sdtpldt0(sdtasdt0(xl,skolem0001),sdtasdt0(xl,skolem0004))=sdtpldt0(sdtasdt0(xl,skolem0001),xn)))&(xl=sz00|xn=sdtasdt0(xl,skolem0004)))))&((~aNaturalNumber0(X6)|xn!=sdtasdt0(xl,X6))&~doDivides0(xl,xn)))),inference(distribute,[status(thm)],[c12])).
% 195.27/195.46 cnf(c29,negated_conjecture,~doDivides0(xl,xn),inference(split_conjunct,[status(thm)],[c13])).
% 195.27/195.46 cnf(reflexivity,axiom,X80=X80,theory(equality)).
% 195.27/195.46 fof(m__1324_04,plain,((((?[W0]:(aNaturalNumber0(W0)&xm=sdtasdt0(xl,W0)))&doDivides0(xl,xm))&(?[W0]:(aNaturalNumber0(W0)&sdtpldt0(xm,xn)=sdtasdt0(xl,W0))))&doDivides0(xl,sdtpldt0(xm,xn))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__1324_04)).
% 195.27/195.46 fof(c30,plain,((((?[X7]:(aNaturalNumber0(X7)&xm=sdtasdt0(xl,X7)))&doDivides0(xl,xm))&(?[X8]:(aNaturalNumber0(X8)&sdtpldt0(xm,xn)=sdtasdt0(xl,X8))))&doDivides0(xl,sdtpldt0(xm,xn))),inference(variable_rename,[status(thm)],[m__1324_04])).
% 195.27/195.46 fof(c31,plain,((((aNaturalNumber0(skolem0005)&xm=sdtasdt0(xl,skolem0005))&doDivides0(xl,xm))&(aNaturalNumber0(skolem0006)&sdtpldt0(xm,xn)=sdtasdt0(xl,skolem0006)))&doDivides0(xl,sdtpldt0(xm,xn))),inference(skolemize,[status(esa)],[c30])).
% 195.27/195.46 cnf(c37,plain,doDivides0(xl,sdtpldt0(xm,xn)),inference(split_conjunct,[status(thm)],[c31])).
% 195.27/195.46 cnf(c7,axiom,X119!=X122|X121!=X120|~doDivides0(X119,X121)|doDivides0(X122,X120),theory(equality)).
% 195.27/195.46 cnf(c316,plain,xl!=X441|sdtpldt0(xm,xn)!=X442|doDivides0(X441,X442),inference(resolution,[status(thm)],[c7, c37])).
% 195.27/195.46 cnf(transitivity,axiom,X83!=X85|X85!=X84|X83=X84,theory(equality)).
% 195.27/195.46 cnf(symmetry,axiom,X81!=X82|X82=X81,theory(equality)).
% 195.27/195.46 fof(m__1324,plain,((aNaturalNumber0(xl)&aNaturalNumber0(xm))&aNaturalNumber0(xn)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__1324)).
% 195.27/195.46 cnf(c40,plain,aNaturalNumber0(xn),inference(split_conjunct,[status(thm)],[m__1324])).
% 195.27/195.46 fof(m_AddZero,axiom,(![W0]:(aNaturalNumber0(W0)=>(sdtpldt0(W0,sz00)=W0&W0=sdtpldt0(sz00,W0)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', m_AddZero)).
% 195.27/195.46 fof(c161,plain,(![W0]:(~aNaturalNumber0(W0)|(sdtpldt0(W0,sz00)=W0&W0=sdtpldt0(sz00,W0)))),inference(fof_nnf,[status(thm)],[m_AddZero])).
% 195.27/195.46 fof(c162,plain,(![X70]:(~aNaturalNumber0(X70)|(sdtpldt0(X70,sz00)=X70&X70=sdtpldt0(sz00,X70)))),inference(variable_rename,[status(thm)],[c161])).
% 195.27/195.46 fof(c163,plain,(![X70]:((~aNaturalNumber0(X70)|sdtpldt0(X70,sz00)=X70)&(~aNaturalNumber0(X70)|X70=sdtpldt0(sz00,X70)))),inference(distribute,[status(thm)],[c162])).
% 195.27/195.46 cnf(c165,plain,~aNaturalNumber0(X147)|X147=sdtpldt0(sz00,X147),inference(split_conjunct,[status(thm)],[c163])).
% 195.27/195.46 cnf(c905,plain,xn=sdtpldt0(sz00,xn),inference(resolution,[status(thm)],[c165, c40])).
% 195.27/195.46 cnf(c924,plain,sdtpldt0(sz00,xn)=xn,inference(resolution,[status(thm)],[c905, symmetry])).
% 195.27/195.46 cnf(c988,plain,X1084!=sdtpldt0(sz00,xn)|X1084=xn,inference(resolution,[status(thm)],[c924, transitivity])).
% 195.27/195.46 cnf(c0,axiom,X88!=X91|X90!=X89|sdtpldt0(X88,X90)=sdtpldt0(X91,X89),theory(equality)).
% 195.27/195.46 cnf(c194,plain,X266!=X264|sdtpldt0(X266,X265)=sdtpldt0(X264,X265),inference(resolution,[status(thm)],[c0, reflexivity])).
% 195.27/195.46 cnf(c33,plain,xm=sdtasdt0(xl,skolem0005),inference(split_conjunct,[status(thm)],[c31])).
% 195.27/195.46 cnf(c240,plain,sdtasdt0(xl,skolem0005)=xm,inference(resolution,[status(thm)],[c33, symmetry])).
% 195.27/195.46 cnf(c280,plain,X412!=sdtasdt0(xl,skolem0005)|X412=xm,inference(resolution,[status(thm)],[c240, transitivity])).
% 195.27/195.46 cnf(c23,negated_conjecture,xl=sz00|aNaturalNumber0(skolem0004),inference(split_conjunct,[status(thm)],[c13])).
% 195.27/195.46 cnf(c27,negated_conjecture,xl=sz00|xn=sdtasdt0(xl,skolem0004),inference(split_conjunct,[status(thm)],[c13])).
% 195.27/195.46 cnf(c28,negated_conjecture,~aNaturalNumber0(X125)|xn!=sdtasdt0(xl,X125),inference(split_conjunct,[status(thm)],[c13])).
% 195.27/195.46 cnf(c748,plain,~aNaturalNumber0(skolem0004)|xl=sz00,inference(resolution,[status(thm)],[c28, c27])).
% 195.27/195.46 cnf(c757,plain,xl=sz00,inference(resolution,[status(thm)],[c748, c23])).
% 195.27/195.46 cnf(c764,plain,sz00=xl,inference(resolution,[status(thm)],[c757, symmetry])).
% 195.27/195.46 cnf(c1,axiom,X92!=X95|X94!=X93|sdtasdt0(X92,X94)=sdtasdt0(X95,X93),theory(equality)).
% 195.27/195.46 cnf(c196,plain,X275!=X273|sdtasdt0(X275,X274)=sdtasdt0(X273,X274),inference(resolution,[status(thm)],[c1, reflexivity])).
% 195.27/195.46 cnf(c4055,plain,sdtasdt0(sz00,X611)=sdtasdt0(xl,X611),inference(resolution,[status(thm)],[c196, c764])).
% 195.27/195.46 cnf(c39408,plain,sdtasdt0(sz00,skolem0005)=xm,inference(resolution,[status(thm)],[c4055, c280])).
% 195.27/195.46 cnf(c39534,plain,xm=sdtasdt0(sz00,skolem0005),inference(resolution,[status(thm)],[c39408, symmetry])).
% 195.27/195.46 cnf(c32,plain,aNaturalNumber0(skolem0005),inference(split_conjunct,[status(thm)],[c31])).
% 195.27/195.46 fof(m_MulZero,axiom,(![W0]:(aNaturalNumber0(W0)=>(sdtasdt0(W0,sz00)=sz00&sz00=sdtasdt0(sz00,W0)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', m_MulZero)).
% 195.27/195.46 fof(c145,plain,(![W0]:(~aNaturalNumber0(W0)|(sdtasdt0(W0,sz00)=sz00&sz00=sdtasdt0(sz00,W0)))),inference(fof_nnf,[status(thm)],[m_MulZero])).
% 195.27/195.46 fof(c146,plain,(![X63]:(~aNaturalNumber0(X63)|(sdtasdt0(X63,sz00)=sz00&sz00=sdtasdt0(sz00,X63)))),inference(variable_rename,[status(thm)],[c145])).
% 195.27/195.46 fof(c147,plain,(![X63]:((~aNaturalNumber0(X63)|sdtasdt0(X63,sz00)=sz00)&(~aNaturalNumber0(X63)|sz00=sdtasdt0(sz00,X63)))),inference(distribute,[status(thm)],[c146])).
% 195.27/195.46 cnf(c149,plain,~aNaturalNumber0(X189)|sz00=sdtasdt0(sz00,X189),inference(split_conjunct,[status(thm)],[c147])).
% 195.27/195.46 cnf(c1418,plain,sz00=sdtasdt0(sz00,skolem0005),inference(resolution,[status(thm)],[c149, c32])).
% 195.27/195.46 cnf(c1475,plain,sdtasdt0(sz00,skolem0005)=sz00,inference(resolution,[status(thm)],[c1418, symmetry])).
% 195.27/195.46 cnf(c1521,plain,X1251!=sdtasdt0(sz00,skolem0005)|X1251=sz00,inference(resolution,[status(thm)],[c1475, transitivity])).
% 195.27/195.46 cnf(c135614,plain,xm=sz00,inference(resolution,[status(thm)],[c1521, c39534])).
% 195.27/195.46 cnf(c135847,plain,sdtpldt0(xm,X1524)=sdtpldt0(sz00,X1524),inference(resolution,[status(thm)],[c135614, c194])).
% 195.27/195.46 cnf(c218456,plain,sdtpldt0(xm,xn)=xn,inference(resolution,[status(thm)],[c135847, c988])).
% 195.27/195.46 cnf(c220294,plain,xl!=X1527|doDivides0(X1527,xn),inference(resolution,[status(thm)],[c218456, c316])).
% 195.27/195.46 cnf(c222760,plain,doDivides0(xl,xn),inference(resolution,[status(thm)],[c220294, reflexivity])).
% 195.27/195.46 cnf(c222806,plain,$false,inference(resolution,[status(thm)],[c222760, c29])).
% 195.27/195.46 % SZS output end CNFRefutation
% 195.27/195.46
% 195.27/195.46 % Initial clauses : 93
% 195.27/195.46 % Processed clauses : 3125
% 195.27/195.46 % Factors computed : 34
% 195.27/195.46 % Resolvents computed: 222594
% 195.27/195.46 % Tautologies deleted: 6
% 195.27/195.46 % Forward subsumed : 1523
% 195.27/195.46 % Backward subsumed : 150
% 195.27/195.46 % -------- CPU Time ---------
% 195.27/195.46 % User time : 194.685 s
% 195.27/195.46 % System time : 0.421 s
% 195.27/195.46 % Total time : 195.106 s
%------------------------------------------------------------------------------