%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NUM545+2 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n008.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:36:08 EDT 2024
% Result : Theorem 0.71s 0.91s
% Output : Refutation 0.71s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13 % Problem : NUM545+2 : TPTP v8.1.2. Released v4.0.0.
% 0.12/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n008.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 17:13:38 EDT 2024
% 0.14/0.35 % CPUTime :
% 0.71/0.91 % Version: 1.5
% 0.71/0.91 % SZS status Theorem
% 0.71/0.91 % SZS output start CNFRefutation
% 0.71/0.91 fof(m__1986,plain,(((aSet0(xS)&(![W0]:(aElementOf0(W0,xS)=>aElementOf0(W0,szNzAzT0))))&aSubsetOf0(xS,szNzAzT0))&isFinite0(xS)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__1986)).
% 0.71/0.91 fof(c50,plain,(((aSet0(xS)&(![W0]:(~aElementOf0(W0,xS)|aElementOf0(W0,szNzAzT0))))&aSubsetOf0(xS,szNzAzT0))&isFinite0(xS)),inference(fof_nnf,[status(thm)],[m__1986])).
% 0.71/0.91 fof(c52,plain,(![X11]:(((aSet0(xS)&(~aElementOf0(X11,xS)|aElementOf0(X11,szNzAzT0)))&aSubsetOf0(xS,szNzAzT0))&isFinite0(xS))),inference(shift_quantors,[status(thm)],[fof(c51,plain,(((aSet0(xS)&(![X11]:(~aElementOf0(X11,xS)|aElementOf0(X11,szNzAzT0))))&aSubsetOf0(xS,szNzAzT0))&isFinite0(xS)),inference(variable_rename,[status(thm)],[c50])).])).
% 0.71/0.91 cnf(c54,plain,~aElementOf0(X167,xS)|aElementOf0(X167,szNzAzT0),inference(split_conjunct,[status(thm)],[c52])).
% 0.71/0.91 fof(mZeroNum,axiom,aElementOf0(sz00,szNzAzT0),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mZeroNum)).
% 0.71/0.91 cnf(c191,plain,aElementOf0(sz00,szNzAzT0),inference(split_conjunct,[status(thm)],[mZeroNum])).
% 0.71/0.91 fof(m__,conjecture,(?[W0]:(aElementOf0(W0,szNzAzT0)&((aSet0(slbdtrb0(W0))&(![W1]:(aElementOf0(W1,slbdtrb0(W0))<=>(aElementOf0(W1,szNzAzT0)&sdtlseqdt0(szszuzczcdt0(W1),W0)))))=>((![W1]:(aElementOf0(W1,xS)=>aElementOf0(W1,slbdtrb0(W0))))|aSubsetOf0(xS,slbdtrb0(W0)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__)).
% 0.71/0.91 fof(c15,negated_conjecture,(~(?[W0]:(aElementOf0(W0,szNzAzT0)&((aSet0(slbdtrb0(W0))&(![W1]:(aElementOf0(W1,slbdtrb0(W0))<=>(aElementOf0(W1,szNzAzT0)&sdtlseqdt0(szszuzczcdt0(W1),W0)))))=>((![W1]:(aElementOf0(W1,xS)=>aElementOf0(W1,slbdtrb0(W0))))|aSubsetOf0(xS,slbdtrb0(W0))))))),inference(assume_negation,[status(cth)],[m__])).
% 0.71/0.91 fof(c16,negated_conjecture,(![W0]:(~aElementOf0(W0,szNzAzT0)|((aSet0(slbdtrb0(W0))&(![W1]:((~aElementOf0(W1,slbdtrb0(W0))|(aElementOf0(W1,szNzAzT0)&sdtlseqdt0(szszuzczcdt0(W1),W0)))&((~aElementOf0(W1,szNzAzT0)|~sdtlseqdt0(szszuzczcdt0(W1),W0))|aElementOf0(W1,slbdtrb0(W0))))))&((?[W1]:(aElementOf0(W1,xS)&~aElementOf0(W1,slbdtrb0(W0))))&~aSubsetOf0(xS,slbdtrb0(W0)))))),inference(fof_nnf,[status(thm)],[c15])).
% 0.71/0.91 fof(c17,negated_conjecture,(![W0]:(~aElementOf0(W0,szNzAzT0)|((aSet0(slbdtrb0(W0))&((![W1]:(~aElementOf0(W1,slbdtrb0(W0))|(aElementOf0(W1,szNzAzT0)&sdtlseqdt0(szszuzczcdt0(W1),W0))))&(![W1]:((~aElementOf0(W1,szNzAzT0)|~sdtlseqdt0(szszuzczcdt0(W1),W0))|aElementOf0(W1,slbdtrb0(W0))))))&((?[W1]:(aElementOf0(W1,xS)&~aElementOf0(W1,slbdtrb0(W0))))&~aSubsetOf0(xS,slbdtrb0(W0)))))),inference(shift_quantors,[status(thm)],[c16])).
% 0.71/0.91 fof(c18,negated_conjecture,(![X2]:(~aElementOf0(X2,szNzAzT0)|((aSet0(slbdtrb0(X2))&((![X3]:(~aElementOf0(X3,slbdtrb0(X2))|(aElementOf0(X3,szNzAzT0)&sdtlseqdt0(szszuzczcdt0(X3),X2))))&(![X4]:((~aElementOf0(X4,szNzAzT0)|~sdtlseqdt0(szszuzczcdt0(X4),X2))|aElementOf0(X4,slbdtrb0(X2))))))&((?[X5]:(aElementOf0(X5,xS)&~aElementOf0(X5,slbdtrb0(X2))))&~aSubsetOf0(xS,slbdtrb0(X2)))))),inference(variable_rename,[status(thm)],[c17])).
% 0.71/0.91 fof(c20,negated_conjecture,(![X2]:(![X3]:(![X4]:(~aElementOf0(X2,szNzAzT0)|((aSet0(slbdtrb0(X2))&((~aElementOf0(X3,slbdtrb0(X2))|(aElementOf0(X3,szNzAzT0)&sdtlseqdt0(szszuzczcdt0(X3),X2)))&((~aElementOf0(X4,szNzAzT0)|~sdtlseqdt0(szszuzczcdt0(X4),X2))|aElementOf0(X4,slbdtrb0(X2)))))&((aElementOf0(skolem0001(X2),xS)&~aElementOf0(skolem0001(X2),slbdtrb0(X2)))&~aSubsetOf0(xS,slbdtrb0(X2)))))))),inference(shift_quantors,[status(thm)],[fof(c19,negated_conjecture,(![X2]:(~aElementOf0(X2,szNzAzT0)|((aSet0(slbdtrb0(X2))&((![X3]:(~aElementOf0(X3,slbdtrb0(X2))|(aElementOf0(X3,szNzAzT0)&sdtlseqdt0(szszuzczcdt0(X3),X2))))&(![X4]:((~aElementOf0(X4,szNzAzT0)|~sdtlseqdt0(szszuzczcdt0(X4),X2))|aElementOf0(X4,slbdtrb0(X2))))))&((aElementOf0(skolem0001(X2),xS)&~aElementOf0(skolem0001(X2),slbdtrb0(X2)))&~aSubsetOf0(xS,slbdtrb0(X2)))))),inference(skolemize,[status(esa)],[c18])).])).
% 0.71/0.91 fof(c21,negated_conjecture,(![X2]:(![X3]:(![X4]:(((~aElementOf0(X2,szNzAzT0)|aSet0(slbdtrb0(X2)))&(((~aElementOf0(X2,szNzAzT0)|(~aElementOf0(X3,slbdtrb0(X2))|aElementOf0(X3,szNzAzT0)))&(~aElementOf0(X2,szNzAzT0)|(~aElementOf0(X3,slbdtrb0(X2))|sdtlseqdt0(szszuzczcdt0(X3),X2))))&(~aElementOf0(X2,szNzAzT0)|((~aElementOf0(X4,szNzAzT0)|~sdtlseqdt0(szszuzczcdt0(X4),X2))|aElementOf0(X4,slbdtrb0(X2))))))&(((~aElementOf0(X2,szNzAzT0)|aElementOf0(skolem0001(X2),xS))&(~aElementOf0(X2,szNzAzT0)|~aElementOf0(skolem0001(X2),slbdtrb0(X2))))&(~aElementOf0(X2,szNzAzT0)|~aSubsetOf0(xS,slbdtrb0(X2)))))))),inference(distribute,[status(thm)],[c20])).
% 0.71/0.91 cnf(c26,negated_conjecture,~aElementOf0(X198,szNzAzT0)|aElementOf0(skolem0001(X198),xS),inference(split_conjunct,[status(thm)],[c21])).
% 0.71/0.91 cnf(c380,plain,aElementOf0(skolem0001(sz00),xS),inference(resolution,[status(thm)],[c26, c191])).
% 0.71/0.91 fof(m__2035,plain,((~((~(?[W0]:aElementOf0(W0,xS)))&xS=slcrc0))=>(((((aElementOf0(szmzazxdt0(xS),xS)&(![W0]:(aElementOf0(W0,xS)=>sdtlseqdt0(W0,szmzazxdt0(xS)))))&aSet0(slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))))&(![W0]:(aElementOf0(W0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))<=>(aElementOf0(W0,szNzAzT0)&sdtlseqdt0(szszuzczcdt0(W0),szszuzczcdt0(szmzazxdt0(xS)))))))&(![W0]:(aElementOf0(W0,xS)=>aElementOf0(W0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))))))&aSubsetOf0(xS,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__2035)).
% 0.71/0.91 fof(c29,plain,(((![W0]:~aElementOf0(W0,xS))&xS=slcrc0)|(((((aElementOf0(szmzazxdt0(xS),xS)&(![W0]:(~aElementOf0(W0,xS)|sdtlseqdt0(W0,szmzazxdt0(xS)))))&aSet0(slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))))&(![W0]:((~aElementOf0(W0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))|(aElementOf0(W0,szNzAzT0)&sdtlseqdt0(szszuzczcdt0(W0),szszuzczcdt0(szmzazxdt0(xS)))))&((~aElementOf0(W0,szNzAzT0)|~sdtlseqdt0(szszuzczcdt0(W0),szszuzczcdt0(szmzazxdt0(xS))))|aElementOf0(W0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))))))&(![W0]:(~aElementOf0(W0,xS)|aElementOf0(W0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))))))&aSubsetOf0(xS,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))))),inference(fof_nnf,[status(thm)],[m__2035])).
% 0.71/0.91 fof(c30,plain,(((![W0]:~aElementOf0(W0,xS))&xS=slcrc0)|(((((aElementOf0(szmzazxdt0(xS),xS)&(![W0]:(~aElementOf0(W0,xS)|sdtlseqdt0(W0,szmzazxdt0(xS)))))&aSet0(slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))))&((![W0]:(~aElementOf0(W0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))|(aElementOf0(W0,szNzAzT0)&sdtlseqdt0(szszuzczcdt0(W0),szszuzczcdt0(szmzazxdt0(xS))))))&(![W0]:((~aElementOf0(W0,szNzAzT0)|~sdtlseqdt0(szszuzczcdt0(W0),szszuzczcdt0(szmzazxdt0(xS))))|aElementOf0(W0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))))))&(![W0]:(~aElementOf0(W0,xS)|aElementOf0(W0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))))))&aSubsetOf0(xS,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))))),inference(shift_quantors,[status(thm)],[c29])).
% 0.71/0.91 fof(c32,plain,(![X6]:(![X7]:(![X8]:(![X9]:(![X10]:((~aElementOf0(X6,xS)&xS=slcrc0)|(((((aElementOf0(szmzazxdt0(xS),xS)&(~aElementOf0(X7,xS)|sdtlseqdt0(X7,szmzazxdt0(xS))))&aSet0(slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))))&((~aElementOf0(X8,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))|(aElementOf0(X8,szNzAzT0)&sdtlseqdt0(szszuzczcdt0(X8),szszuzczcdt0(szmzazxdt0(xS)))))&((~aElementOf0(X9,szNzAzT0)|~sdtlseqdt0(szszuzczcdt0(X9),szszuzczcdt0(szmzazxdt0(xS))))|aElementOf0(X9,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))))))&(~aElementOf0(X10,xS)|aElementOf0(X10,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))))&aSubsetOf0(xS,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))))))))),inference(shift_quantors,[status(thm)],[fof(c31,plain,(((![X6]:~aElementOf0(X6,xS))&xS=slcrc0)|(((((aElementOf0(szmzazxdt0(xS),xS)&(![X7]:(~aElementOf0(X7,xS)|sdtlseqdt0(X7,szmzazxdt0(xS)))))&aSet0(slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))))&((![X8]:(~aElementOf0(X8,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))|(aElementOf0(X8,szNzAzT0)&sdtlseqdt0(szszuzczcdt0(X8),szszuzczcdt0(szmzazxdt0(xS))))))&(![X9]:((~aElementOf0(X9,szNzAzT0)|~sdtlseqdt0(szszuzczcdt0(X9),szszuzczcdt0(szmzazxdt0(xS))))|aElementOf0(X9,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))))))&(![X10]:(~aElementOf0(X10,xS)|aElementOf0(X10,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))))))&aSubsetOf0(xS,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))))),inference(variable_rename,[status(thm)],[c30])).])).
% 0.71/0.91 fof(c33,plain,(![X6]:(![X7]:(![X8]:(![X9]:(![X10]:(((((((~aElementOf0(X6,xS)|aElementOf0(szmzazxdt0(xS),xS))&(~aElementOf0(X6,xS)|(~aElementOf0(X7,xS)|sdtlseqdt0(X7,szmzazxdt0(xS)))))&(~aElementOf0(X6,xS)|aSet0(slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))))&(((~aElementOf0(X6,xS)|(~aElementOf0(X8,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))|aElementOf0(X8,szNzAzT0)))&(~aElementOf0(X6,xS)|(~aElementOf0(X8,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))|sdtlseqdt0(szszuzczcdt0(X8),szszuzczcdt0(szmzazxdt0(xS))))))&(~aElementOf0(X6,xS)|((~aElementOf0(X9,szNzAzT0)|~sdtlseqdt0(szszuzczcdt0(X9),szszuzczcdt0(szmzazxdt0(xS))))|aElementOf0(X9,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))))))&(~aElementOf0(X6,xS)|(~aElementOf0(X10,xS)|aElementOf0(X10,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))))))&(~aElementOf0(X6,xS)|aSubsetOf0(xS,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))))&((((((xS=slcrc0|aElementOf0(szmzazxdt0(xS),xS))&(xS=slcrc0|(~aElementOf0(X7,xS)|sdtlseqdt0(X7,szmzazxdt0(xS)))))&(xS=slcrc0|aSet0(slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))))&(((xS=slcrc0|(~aElementOf0(X8,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))|aElementOf0(X8,szNzAzT0)))&(xS=slcrc0|(~aElementOf0(X8,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))|sdtlseqdt0(szszuzczcdt0(X8),szszuzczcdt0(szmzazxdt0(xS))))))&(xS=slcrc0|((~aElementOf0(X9,szNzAzT0)|~sdtlseqdt0(szszuzczcdt0(X9),szszuzczcdt0(szmzazxdt0(xS))))|aElementOf0(X9,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))))))&(xS=slcrc0|(~aElementOf0(X10,xS)|aElementOf0(X10,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))))))&(xS=slcrc0|aSubsetOf0(xS,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))))))))))),inference(distribute,[status(thm)],[c32])).
% 0.71/0.91 cnf(c34,plain,~aElementOf0(X203,xS)|aElementOf0(szmzazxdt0(xS),xS),inference(split_conjunct,[status(thm)],[c33])).
% 0.71/0.91 cnf(c416,plain,aElementOf0(szmzazxdt0(xS),xS),inference(resolution,[status(thm)],[c34, c380])).
% 0.71/0.91 cnf(c420,plain,aElementOf0(szmzazxdt0(xS),szNzAzT0),inference(resolution,[status(thm)],[c416, c54])).
% 0.71/0.91 fof(mSuccNum,axiom,(![W0]:(aElementOf0(W0,szNzAzT0)=>(aElementOf0(szszuzczcdt0(W0),szNzAzT0)&szszuzczcdt0(W0)!=sz00))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mSuccNum)).
% 0.71/0.91 fof(c186,plain,(![W0]:(~aElementOf0(W0,szNzAzT0)|(aElementOf0(szszuzczcdt0(W0),szNzAzT0)&szszuzczcdt0(W0)!=sz00))),inference(fof_nnf,[status(thm)],[mSuccNum])).
% 0.71/0.91 fof(c187,plain,(![X66]:(~aElementOf0(X66,szNzAzT0)|(aElementOf0(szszuzczcdt0(X66),szNzAzT0)&szszuzczcdt0(X66)!=sz00))),inference(variable_rename,[status(thm)],[c186])).
% 0.71/0.91 fof(c188,plain,(![X66]:((~aElementOf0(X66,szNzAzT0)|aElementOf0(szszuzczcdt0(X66),szNzAzT0))&(~aElementOf0(X66,szNzAzT0)|szszuzczcdt0(X66)!=sz00))),inference(distribute,[status(thm)],[c187])).
% 0.71/0.91 cnf(c189,plain,~aElementOf0(X214,szNzAzT0)|aElementOf0(szszuzczcdt0(X214),szNzAzT0),inference(split_conjunct,[status(thm)],[c188])).
% 0.71/0.91 cnf(c474,plain,aElementOf0(szszuzczcdt0(szmzazxdt0(xS)),szNzAzT0),inference(resolution,[status(thm)],[c189, c420])).
% 0.71/0.91 cnf(c28,negated_conjecture,~aElementOf0(X202,szNzAzT0)|~aSubsetOf0(xS,slbdtrb0(X202)),inference(split_conjunct,[status(thm)],[c21])).
% 0.71/0.91 cnf(c424,plain,aElementOf0(skolem0001(szmzazxdt0(xS)),xS),inference(resolution,[status(thm)],[c420, c26])).
% 0.71/0.91 cnf(c41,plain,~aElementOf0(X217,xS)|aSubsetOf0(xS,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))),inference(split_conjunct,[status(thm)],[c33])).
% 0.71/0.91 cnf(c505,plain,aSubsetOf0(xS,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))),inference(resolution,[status(thm)],[c41, c424])).
% 0.71/0.91 cnf(c846,plain,~aElementOf0(szszuzczcdt0(szmzazxdt0(xS)),szNzAzT0),inference(resolution,[status(thm)],[c505, c28])).
% 0.71/0.91 cnf(c848,plain,$false,inference(resolution,[status(thm)],[c846, c474])).
% 0.71/0.91 % SZS output end CNFRefutation
% 0.71/0.91
% 0.71/0.91 % Initial clauses : 142
% 0.71/0.91 % Processed clauses : 189
% 0.71/0.91 % Factors computed : 5
% 0.71/0.91 % Resolvents computed: 548
% 0.71/0.91 % Tautologies deleted: 10
% 0.71/0.91 % Forward subsumed : 59
% 0.71/0.91 % Backward subsumed : 13
% 0.71/0.91 % -------- CPU Time ---------
% 0.71/0.91 % User time : 0.543 s
% 0.71/0.91 % System time : 0.017 s
% 0.71/0.91 % Total time : 0.560 s
%------------------------------------------------------------------------------