%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NUM590+3 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n027.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:15 EDT 2024
% Result : Theorem 38.36s 38.55s
% Output : Refutation 38.36s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : NUM590+3 : TPTP v8.1.2. Released v4.0.0.
% 0.06/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n027.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed May 8 16:30:08 EDT 2024
% 0.13/0.34 % CPUTime :
% 38.36/38.55 % Version: 1.5
% 38.36/38.55 % SZS status Theorem
% 38.36/38.55 % SZS output start CNFRefutation
% 38.36/38.55 fof(m__,conjecture,((![W0]:(aElementOf0(W0,xY)=>aElementOf0(W0,szNzAzT0)))|aSubsetOf0(xY,szNzAzT0)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__)).
% 38.36/38.55 fof(c23,negated_conjecture,(~((![W0]:(aElementOf0(W0,xY)=>aElementOf0(W0,szNzAzT0)))|aSubsetOf0(xY,szNzAzT0))),inference(assume_negation,[status(cth)],[m__])).
% 38.36/38.55 fof(c24,negated_conjecture,((?[W0]:(aElementOf0(W0,xY)&~aElementOf0(W0,szNzAzT0)))&~aSubsetOf0(xY,szNzAzT0)),inference(fof_nnf,[status(thm)],[c23])).
% 38.36/38.55 fof(c25,negated_conjecture,((?[X2]:(aElementOf0(X2,xY)&~aElementOf0(X2,szNzAzT0)))&~aSubsetOf0(xY,szNzAzT0)),inference(variable_rename,[status(thm)],[c24])).
% 38.36/38.55 fof(c26,negated_conjecture,((aElementOf0(skolem0001,xY)&~aElementOf0(skolem0001,szNzAzT0))&~aSubsetOf0(xY,szNzAzT0)),inference(skolemize,[status(esa)],[c25])).
% 38.36/38.55 cnf(c28,negated_conjecture,~aElementOf0(skolem0001,szNzAzT0),inference(split_conjunct,[status(thm)],[c26])).
% 38.36/38.55 fof(m__4448,plain,aElementOf0(xi,szNzAzT0),file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__4448)).
% 38.36/38.55 cnf(c44,plain,aElementOf0(xi,szNzAzT0),inference(split_conjunct,[status(thm)],[m__4448])).
% 38.36/38.55 cnf(c27,negated_conjecture,aElementOf0(skolem0001,xY),inference(split_conjunct,[status(thm)],[c26])).
% 38.36/38.55 fof(m__4448_02,plain,(((((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))&(![W0]:(aElementOf0(W0,sdtlpdtrp0(xN,xi))=>sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0))))&aSet0(xY))&(![W0]:(aElementOf0(W0,xY)<=>((aElement0(W0)&aElementOf0(W0,sdtlpdtrp0(xN,xi)))&W0!=szmzizndt0(sdtlpdtrp0(xN,xi))))))&xY=sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))&xd=sdtlpdtrp0(xC,xi)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__4448_02)).
% 38.36/38.55 fof(c30,plain,(((((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))&(![W0]:(~aElementOf0(W0,sdtlpdtrp0(xN,xi))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0))))&aSet0(xY))&(![W0]:((~aElementOf0(W0,xY)|((aElement0(W0)&aElementOf0(W0,sdtlpdtrp0(xN,xi)))&W0!=szmzizndt0(sdtlpdtrp0(xN,xi))))&(((~aElement0(W0)|~aElementOf0(W0,sdtlpdtrp0(xN,xi)))|W0=szmzizndt0(sdtlpdtrp0(xN,xi)))|aElementOf0(W0,xY)))))&xY=sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))&xd=sdtlpdtrp0(xC,xi)),inference(fof_nnf,[status(thm)],[m__4448_02])).
% 38.36/38.55 fof(c31,plain,(((((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))&(![W0]:(~aElementOf0(W0,sdtlpdtrp0(xN,xi))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0))))&aSet0(xY))&((![W0]:(~aElementOf0(W0,xY)|((aElement0(W0)&aElementOf0(W0,sdtlpdtrp0(xN,xi)))&W0!=szmzizndt0(sdtlpdtrp0(xN,xi)))))&(![W0]:(((~aElement0(W0)|~aElementOf0(W0,sdtlpdtrp0(xN,xi)))|W0=szmzizndt0(sdtlpdtrp0(xN,xi)))|aElementOf0(W0,xY)))))&xY=sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))&xd=sdtlpdtrp0(xC,xi)),inference(shift_quantors,[status(thm)],[c30])).
% 38.36/38.55 fof(c33,plain,(![X3]:(![X4]:(![X5]:(((((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))&(~aElementOf0(X3,sdtlpdtrp0(xN,xi))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X3)))&aSet0(xY))&((~aElementOf0(X4,xY)|((aElement0(X4)&aElementOf0(X4,sdtlpdtrp0(xN,xi)))&X4!=szmzizndt0(sdtlpdtrp0(xN,xi))))&(((~aElement0(X5)|~aElementOf0(X5,sdtlpdtrp0(xN,xi)))|X5=szmzizndt0(sdtlpdtrp0(xN,xi)))|aElementOf0(X5,xY))))&xY=sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))&xd=sdtlpdtrp0(xC,xi))))),inference(shift_quantors,[status(thm)],[fof(c32,plain,(((((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))&(![X3]:(~aElementOf0(X3,sdtlpdtrp0(xN,xi))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X3))))&aSet0(xY))&((![X4]:(~aElementOf0(X4,xY)|((aElement0(X4)&aElementOf0(X4,sdtlpdtrp0(xN,xi)))&X4!=szmzizndt0(sdtlpdtrp0(xN,xi)))))&(![X5]:(((~aElement0(X5)|~aElementOf0(X5,sdtlpdtrp0(xN,xi)))|X5=szmzizndt0(sdtlpdtrp0(xN,xi)))|aElementOf0(X5,xY)))))&xY=sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))&xd=sdtlpdtrp0(xC,xi)),inference(variable_rename,[status(thm)],[c31])).])).
% 38.36/38.55 fof(c34,plain,(![X3]:(![X4]:(![X5]:(((((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))&(~aElementOf0(X3,sdtlpdtrp0(xN,xi))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X3)))&aSet0(xY))&((((~aElementOf0(X4,xY)|aElement0(X4))&(~aElementOf0(X4,xY)|aElementOf0(X4,sdtlpdtrp0(xN,xi))))&(~aElementOf0(X4,xY)|X4!=szmzizndt0(sdtlpdtrp0(xN,xi))))&(((~aElement0(X5)|~aElementOf0(X5,sdtlpdtrp0(xN,xi)))|X5=szmzizndt0(sdtlpdtrp0(xN,xi)))|aElementOf0(X5,xY))))&xY=sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))&xd=sdtlpdtrp0(xC,xi))))),inference(distribute,[status(thm)],[c33])).
% 38.36/38.55 cnf(c39,plain,~aElementOf0(X362,xY)|aElementOf0(X362,sdtlpdtrp0(xN,xi)),inference(split_conjunct,[status(thm)],[c34])).
% 38.36/38.55 cnf(c5449,plain,aElementOf0(skolem0001,sdtlpdtrp0(xN,xi)),inference(resolution,[status(thm)],[c39, c27])).
% 38.36/38.55 fof(m__3671,plain,(![W0]:(aElementOf0(W0,szNzAzT0)=>(((aSet0(sdtlpdtrp0(xN,W0))&(![W1]:(aElementOf0(W1,sdtlpdtrp0(xN,W0))=>aElementOf0(W1,szNzAzT0))))&aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0))&isCountable0(sdtlpdtrp0(xN,W0))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__3671)).
% 38.36/38.55 fof(c708,plain,(![W0]:(~aElementOf0(W0,szNzAzT0)|(((aSet0(sdtlpdtrp0(xN,W0))&(![W1]:(~aElementOf0(W1,sdtlpdtrp0(xN,W0))|aElementOf0(W1,szNzAzT0))))&aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0))&isCountable0(sdtlpdtrp0(xN,W0))))),inference(fof_nnf,[status(thm)],[m__3671])).
% 38.36/38.55 fof(c710,plain,(![X57]:(![X58]:(~aElementOf0(X57,szNzAzT0)|(((aSet0(sdtlpdtrp0(xN,X57))&(~aElementOf0(X58,sdtlpdtrp0(xN,X57))|aElementOf0(X58,szNzAzT0)))&aSubsetOf0(sdtlpdtrp0(xN,X57),szNzAzT0))&isCountable0(sdtlpdtrp0(xN,X57)))))),inference(shift_quantors,[status(thm)],[fof(c709,plain,(![X57]:(~aElementOf0(X57,szNzAzT0)|(((aSet0(sdtlpdtrp0(xN,X57))&(![X58]:(~aElementOf0(X58,sdtlpdtrp0(xN,X57))|aElementOf0(X58,szNzAzT0))))&aSubsetOf0(sdtlpdtrp0(xN,X57),szNzAzT0))&isCountable0(sdtlpdtrp0(xN,X57))))),inference(variable_rename,[status(thm)],[c708])).])).
% 38.36/38.55 fof(c711,plain,(![X57]:(![X58]:((((~aElementOf0(X57,szNzAzT0)|aSet0(sdtlpdtrp0(xN,X57)))&(~aElementOf0(X57,szNzAzT0)|(~aElementOf0(X58,sdtlpdtrp0(xN,X57))|aElementOf0(X58,szNzAzT0))))&(~aElementOf0(X57,szNzAzT0)|aSubsetOf0(sdtlpdtrp0(xN,X57),szNzAzT0)))&(~aElementOf0(X57,szNzAzT0)|isCountable0(sdtlpdtrp0(xN,X57)))))),inference(distribute,[status(thm)],[c710])).
% 38.36/38.55 cnf(c713,plain,~aElementOf0(X3044,szNzAzT0)|~aElementOf0(X3043,sdtlpdtrp0(xN,X3044))|aElementOf0(X3043,szNzAzT0),inference(split_conjunct,[status(thm)],[c711])).
% 38.36/38.55 cnf(c23606,plain,~aElementOf0(xi,szNzAzT0)|aElementOf0(skolem0001,szNzAzT0),inference(resolution,[status(thm)],[c713, c5449])).
% 38.36/38.55 cnf(c23608,plain,aElementOf0(skolem0001,szNzAzT0),inference(resolution,[status(thm)],[c23606, c44])).
% 38.36/38.55 cnf(c23613,plain,$false,inference(resolution,[status(thm)],[c23608, c28])).
% 38.36/38.55 % SZS output end CNFRefutation
% 38.36/38.55
% 38.36/38.55 % Initial clauses : 4848
% 38.36/38.55 % Processed clauses : 2929
% 38.36/38.55 % Factors computed : 154
% 38.36/38.55 % Resolvents computed: 18351
% 38.36/38.55 % Tautologies deleted: 29
% 38.36/38.55 % Forward subsumed : 974
% 38.36/38.55 % Backward subsumed : 371
% 38.36/38.55 % -------- CPU Time ---------
% 38.36/38.55 % User time : 38.100 s
% 38.36/38.55 % System time : 0.094 s
% 38.36/38.55 % Total time : 38.194 s
%------------------------------------------------------------------------------