%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NUM432+3 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n028.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:47 EDT 2024
% Result : Theorem 1.97s 2.15s
% Output : Refutation 1.97s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.13/0.13 % Problem : NUM432+3 : TPTP v8.1.2. Released v4.0.0.
% 0.13/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n028.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Wed May 8 16:16:07 EDT 2024
% 0.14/0.35 % CPUTime :
% 1.97/2.15 % Version: 1.5
% 1.97/2.15 % SZS status Theorem
% 1.97/2.15 % SZS output start CNFRefutation
% 1.97/2.15 fof(m__,conjecture,(((?[W0]:(aInteger0(W0)&sdtasdt0(xq,W0)=sdtpldt0(xa,smndt0(xc))))|aDivisorOf0(xq,sdtpldt0(xa,smndt0(xc))))|sdteqdtlpzmzozddtrp0(xa,xc,xq)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__)).
% 1.97/2.15 fof(c6,negated_conjecture,(~(((?[W0]:(aInteger0(W0)&sdtasdt0(xq,W0)=sdtpldt0(xa,smndt0(xc))))|aDivisorOf0(xq,sdtpldt0(xa,smndt0(xc))))|sdteqdtlpzmzozddtrp0(xa,xc,xq))),inference(assume_negation,[status(cth)],[m__])).
% 1.97/2.15 fof(c7,negated_conjecture,(((![W0]:(~aInteger0(W0)|sdtasdt0(xq,W0)!=sdtpldt0(xa,smndt0(xc))))&~aDivisorOf0(xq,sdtpldt0(xa,smndt0(xc))))&~sdteqdtlpzmzozddtrp0(xa,xc,xq)),inference(fof_nnf,[status(thm)],[c6])).
% 1.97/2.15 fof(c9,negated_conjecture,(![X2]:(((~aInteger0(X2)|sdtasdt0(xq,X2)!=sdtpldt0(xa,smndt0(xc)))&~aDivisorOf0(xq,sdtpldt0(xa,smndt0(xc))))&~sdteqdtlpzmzozddtrp0(xa,xc,xq))),inference(shift_quantors,[status(thm)],[fof(c8,negated_conjecture,(((![X2]:(~aInteger0(X2)|sdtasdt0(xq,X2)!=sdtpldt0(xa,smndt0(xc))))&~aDivisorOf0(xq,sdtpldt0(xa,smndt0(xc))))&~sdteqdtlpzmzozddtrp0(xa,xc,xq)),inference(variable_rename,[status(thm)],[c7])).])).
% 1.97/2.15 cnf(c10,negated_conjecture,~aInteger0(X80)|sdtasdt0(xq,X80)!=sdtpldt0(xa,smndt0(xc)),inference(split_conjunct,[status(thm)],[c9])).
% 1.97/2.15 fof(m__924,plain,sdtasdt0(xq,sdtpldt0(xn,xm))=sdtpldt0(xa,smndt0(xc)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__924)).
% 1.97/2.15 cnf(c13,plain,sdtasdt0(xq,sdtpldt0(xn,xm))=sdtpldt0(xa,smndt0(xc)),inference(split_conjunct,[status(thm)],[m__924])).
% 1.97/2.15 cnf(c215,plain,~aInteger0(sdtpldt0(xn,xm)),inference(resolution,[status(thm)],[c13, c10])).
% 1.97/2.15 fof(m__876,plain,(aInteger0(xn)&sdtasdt0(xq,xn)=sdtpldt0(xa,smndt0(xb))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__876)).
% 1.97/2.15 cnf(c16,plain,aInteger0(xn),inference(split_conjunct,[status(thm)],[m__876])).
% 1.97/2.15 fof(m__899,plain,(aInteger0(xm)&sdtasdt0(xq,xm)=sdtpldt0(xb,smndt0(xc))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__899)).
% 1.97/2.15 cnf(c14,plain,aInteger0(xm),inference(split_conjunct,[status(thm)],[m__899])).
% 1.97/2.15 fof(mIntPlus,axiom,(![W0]:(![W1]:((aInteger0(W0)&aInteger0(W1))=>aInteger0(sdtpldt0(W0,W1))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mIntPlus)).
% 1.97/2.15 fof(c103,plain,(![W0]:(![W1]:((~aInteger0(W0)|~aInteger0(W1))|aInteger0(sdtpldt0(W0,W1))))),inference(fof_nnf,[status(thm)],[mIntPlus])).
% 1.97/2.15 fof(c104,plain,(![X40]:(![X41]:((~aInteger0(X40)|~aInteger0(X41))|aInteger0(sdtpldt0(X40,X41))))),inference(variable_rename,[status(thm)],[c103])).
% 1.97/2.15 cnf(c105,plain,~aInteger0(X134)|~aInteger0(X133)|aInteger0(sdtpldt0(X134,X133)),inference(split_conjunct,[status(thm)],[c104])).
% 1.97/2.15 cnf(c1717,plain,~aInteger0(X163)|aInteger0(sdtpldt0(X163,xm)),inference(resolution,[status(thm)],[c105, c14])).
% 1.97/2.15 cnf(c7265,plain,aInteger0(sdtpldt0(xn,xm)),inference(resolution,[status(thm)],[c1717, c16])).
% 1.97/2.15 cnf(c7590,plain,$false,inference(resolution,[status(thm)],[c7265, c215])).
% 1.97/2.15 % SZS output end CNFRefutation
% 1.97/2.15
% 1.97/2.15 % Initial clauses : 62
% 1.97/2.15 % Processed clauses : 373
% 1.97/2.15 % Factors computed : 16
% 1.97/2.15 % Resolvents computed: 7496
% 1.97/2.15 % Tautologies deleted: 3
% 1.97/2.15 % Forward subsumed : 66
% 1.97/2.15 % Backward subsumed : 0
% 1.97/2.15 % -------- CPU Time ---------
% 1.97/2.15 % User time : 1.778 s
% 1.97/2.15 % System time : 0.015 s
% 1.97/2.15 % Total time : 1.793 s
%------------------------------------------------------------------------------