%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NUM482+1 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n014.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:56 EDT 2024
% Result : Theorem 5.93s 6.17s
% Output : Refutation 5.93s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.14 % Problem : NUM482+1 : TPTP v8.1.2. Released v4.0.0.
% 0.10/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.37 % Computer : n014.cluster.edu
% 0.15/0.37 % Model : x86_64 x86_64
% 0.15/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.37 % Memory : 8042.1875MB
% 0.15/0.37 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.37 % CPULimit : 300
% 0.15/0.37 % WCLimit : 300
% 0.15/0.37 % DateTime : Wed May 8 16:49:53 EDT 2024
% 0.15/0.37 % CPUTime :
% 5.93/6.17 % Version: 1.5
% 5.93/6.17 % SZS status Theorem
% 5.93/6.17 % SZS output start CNFRefutation
% 5.93/6.17 fof(m__1716,plain,aNaturalNumber0(xk),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__1716)).
% 5.93/6.17 cnf(c24,plain,aNaturalNumber0(xk),inference(split_conjunct,[status(thm)],[m__1716])).
% 5.93/6.17 fof(m__,conjecture,(isPrime0(xk)=>(?[W0]:((aNaturalNumber0(W0)&doDivides0(W0,xk))&isPrime0(W0)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__)).
% 5.93/6.17 fof(c9,negated_conjecture,(~(isPrime0(xk)=>(?[W0]:((aNaturalNumber0(W0)&doDivides0(W0,xk))&isPrime0(W0))))),inference(assume_negation,[status(cth)],[m__])).
% 5.93/6.17 fof(c10,negated_conjecture,(isPrime0(xk)&(![W0]:((~aNaturalNumber0(W0)|~doDivides0(W0,xk))|~isPrime0(W0)))),inference(fof_nnf,[status(thm)],[c9])).
% 5.93/6.17 fof(c12,negated_conjecture,(![X2]:(isPrime0(xk)&((~aNaturalNumber0(X2)|~doDivides0(X2,xk))|~isPrime0(X2)))),inference(shift_quantors,[status(thm)],[fof(c11,negated_conjecture,(isPrime0(xk)&(![X2]:((~aNaturalNumber0(X2)|~doDivides0(X2,xk))|~isPrime0(X2)))),inference(variable_rename,[status(thm)],[c10])).])).
% 5.93/6.17 cnf(c13,negated_conjecture,isPrime0(xk),inference(split_conjunct,[status(thm)],[c12])).
% 5.93/6.17 cnf(c14,negated_conjecture,~aNaturalNumber0(X112)|~doDivides0(X112,xk)|~isPrime0(X112),inference(split_conjunct,[status(thm)],[c12])).
% 5.93/6.17 fof(mSortsC_01,axiom,(aNaturalNumber0(sz10)&sz10!=sz00),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mSortsC_01)).
% 5.93/6.17 cnf(c184,plain,aNaturalNumber0(sz10),inference(split_conjunct,[status(thm)],[mSortsC_01])).
% 5.93/6.17 cnf(symmetry,axiom,X88!=X89|X89=X88,theory(equality)).
% 5.93/6.17 fof(m_MulUnit,axiom,(![W0]:(aNaturalNumber0(W0)=>(sdtasdt0(W0,sz10)=W0&W0=sdtasdt0(sz10,W0)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m_MulUnit)).
% 5.93/6.17 fof(c156,plain,(![W0]:(~aNaturalNumber0(W0)|(sdtasdt0(W0,sz10)=W0&W0=sdtasdt0(sz10,W0)))),inference(fof_nnf,[status(thm)],[m_MulUnit])).
% 5.93/6.17 fof(c157,plain,(![X71]:(~aNaturalNumber0(X71)|(sdtasdt0(X71,sz10)=X71&X71=sdtasdt0(sz10,X71)))),inference(variable_rename,[status(thm)],[c156])).
% 5.93/6.17 fof(c158,plain,(![X71]:((~aNaturalNumber0(X71)|sdtasdt0(X71,sz10)=X71)&(~aNaturalNumber0(X71)|X71=sdtasdt0(sz10,X71)))),inference(distribute,[status(thm)],[c157])).
% 5.93/6.17 cnf(c159,plain,~aNaturalNumber0(X119)|sdtasdt0(X119,sz10)=X119,inference(split_conjunct,[status(thm)],[c158])).
% 5.93/6.17 cnf(c206,plain,sdtasdt0(xk,sz10)=xk,inference(resolution,[status(thm)],[c159, c24])).
% 5.93/6.17 cnf(c217,plain,xk=sdtasdt0(xk,sz10),inference(resolution,[status(thm)],[c206, symmetry])).
% 5.93/6.17 fof(mDefDiv,plain,(![W0]:(![W1]:((aNaturalNumber0(W0)&aNaturalNumber0(W1))=>(doDivides0(W0,W1)<=>(?[W2]:(aNaturalNumber0(W2)&W1=sdtasdt0(W0,W2))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mDefDiv)).
% 5.93/6.17 fof(c61,plain,(![W0]:(![W1]:((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|((~doDivides0(W0,W1)|(?[W2]:(aNaturalNumber0(W2)&W1=sdtasdt0(W0,W2))))&((![W2]:(~aNaturalNumber0(W2)|W1!=sdtasdt0(W0,W2)))|doDivides0(W0,W1)))))),inference(fof_nnf,[status(thm)],[mDefDiv])).
% 5.93/6.17 fof(c62,plain,(![X26]:(![X27]:((~aNaturalNumber0(X26)|~aNaturalNumber0(X27))|((~doDivides0(X26,X27)|(?[X28]:(aNaturalNumber0(X28)&X27=sdtasdt0(X26,X28))))&((![X29]:(~aNaturalNumber0(X29)|X27!=sdtasdt0(X26,X29)))|doDivides0(X26,X27)))))),inference(variable_rename,[status(thm)],[c61])).
% 5.93/6.17 fof(c64,plain,(![X26]:(![X27]:(![X29]:((~aNaturalNumber0(X26)|~aNaturalNumber0(X27))|((~doDivides0(X26,X27)|(aNaturalNumber0(skolem0003(X26,X27))&X27=sdtasdt0(X26,skolem0003(X26,X27))))&((~aNaturalNumber0(X29)|X27!=sdtasdt0(X26,X29))|doDivides0(X26,X27))))))),inference(shift_quantors,[status(thm)],[fof(c63,plain,(![X26]:(![X27]:((~aNaturalNumber0(X26)|~aNaturalNumber0(X27))|((~doDivides0(X26,X27)|(aNaturalNumber0(skolem0003(X26,X27))&X27=sdtasdt0(X26,skolem0003(X26,X27))))&((![X29]:(~aNaturalNumber0(X29)|X27!=sdtasdt0(X26,X29)))|doDivides0(X26,X27)))))),inference(skolemize,[status(esa)],[c62])).])).
% 5.93/6.17 fof(c65,plain,(![X26]:(![X27]:(![X29]:((((~aNaturalNumber0(X26)|~aNaturalNumber0(X27))|(~doDivides0(X26,X27)|aNaturalNumber0(skolem0003(X26,X27))))&((~aNaturalNumber0(X26)|~aNaturalNumber0(X27))|(~doDivides0(X26,X27)|X27=sdtasdt0(X26,skolem0003(X26,X27)))))&((~aNaturalNumber0(X26)|~aNaturalNumber0(X27))|((~aNaturalNumber0(X29)|X27!=sdtasdt0(X26,X29))|doDivides0(X26,X27))))))),inference(distribute,[status(thm)],[c64])).
% 5.93/6.17 cnf(c68,plain,~aNaturalNumber0(X192)|~aNaturalNumber0(X191)|~aNaturalNumber0(X190)|X191!=sdtasdt0(X192,X190)|doDivides0(X192,X191),inference(split_conjunct,[status(thm)],[c65])).
% 5.93/6.17 cnf(c847,plain,~aNaturalNumber0(xk)|~aNaturalNumber0(sz10)|doDivides0(xk,xk),inference(resolution,[status(thm)],[c68, c217])).
% 5.93/6.17 cnf(c24001,plain,~aNaturalNumber0(xk)|doDivides0(xk,xk),inference(resolution,[status(thm)],[c847, c184])).
% 5.93/6.17 cnf(c24002,plain,doDivides0(xk,xk),inference(resolution,[status(thm)],[c24001, c24])).
% 5.93/6.17 cnf(c24005,plain,~aNaturalNumber0(xk)|~isPrime0(xk),inference(resolution,[status(thm)],[c24002, c14])).
% 5.93/6.17 cnf(c24012,plain,~aNaturalNumber0(xk),inference(resolution,[status(thm)],[c24005, c13])).
% 5.93/6.17 cnf(c24013,plain,$false,inference(resolution,[status(thm)],[c24012, c24])).
% 5.93/6.17 % SZS output end CNFRefutation
% 5.93/6.17
% 5.93/6.17 % Initial clauses : 87
% 5.93/6.17 % Processed clauses : 657
% 5.93/6.17 % Factors computed : 26
% 5.93/6.17 % Resolvents computed: 23862
% 5.93/6.17 % Tautologies deleted: 6
% 5.93/6.17 % Forward subsumed : 129
% 5.93/6.17 % Backward subsumed : 24
% 5.93/6.17 % -------- CPU Time ---------
% 5.93/6.17 % User time : 5.734 s
% 5.93/6.17 % System time : 0.045 s
% 5.93/6.17 % Total time : 5.779 s
%------------------------------------------------------------------------------