%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LAT388+4 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n016.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:30:13 EDT 2024
% Result : Theorem 0.47s 0.65s
% Output : Refutation 0.47s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : LAT388+4 : TPTP v8.1.2. Released v4.0.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.34 % Computer : n016.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Wed May 8 12:33:08 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.47/0.65 % Version: 1.5
% 0.47/0.65 % SZS status Theorem
% 0.47/0.65 % SZS output start CNFRefutation
% 0.47/0.65 fof(m__,conjecture,(?[W0]:(((aElementOf0(W0,xS)&((aElementOf0(W0,xS)&(![W1]:(aElementOf0(W1,xT)=>sdtlseqdt0(W1,W0))))|aUpperBoundOfIn0(W0,xT,xS)))&(![W1]:(((aElementOf0(W1,xS)&(![W2]:(aElementOf0(W2,xT)=>sdtlseqdt0(W2,W1))))&aUpperBoundOfIn0(W1,xT,xS))=>sdtlseqdt0(W0,W1))))|aSupremumOfIn0(W0,xT,xS))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__)).
% 0.47/0.65 fof(c20,negated_conjecture,(~(?[W0]:(((aElementOf0(W0,xS)&((aElementOf0(W0,xS)&(![W1]:(aElementOf0(W1,xT)=>sdtlseqdt0(W1,W0))))|aUpperBoundOfIn0(W0,xT,xS)))&(![W1]:(((aElementOf0(W1,xS)&(![W2]:(aElementOf0(W2,xT)=>sdtlseqdt0(W2,W1))))&aUpperBoundOfIn0(W1,xT,xS))=>sdtlseqdt0(W0,W1))))|aSupremumOfIn0(W0,xT,xS)))),inference(assume_negation,[status(cth)],[m__])).
% 0.47/0.65 fof(c21,negated_conjecture,(![W0]:(((~aElementOf0(W0,xS)|((~aElementOf0(W0,xS)|(?[W1]:(aElementOf0(W1,xT)&~sdtlseqdt0(W1,W0))))&~aUpperBoundOfIn0(W0,xT,xS)))|(?[W1]:(((aElementOf0(W1,xS)&(![W2]:(~aElementOf0(W2,xT)|sdtlseqdt0(W2,W1))))&aUpperBoundOfIn0(W1,xT,xS))&~sdtlseqdt0(W0,W1))))&~aSupremumOfIn0(W0,xT,xS))),inference(fof_nnf,[status(thm)],[c20])).
% 0.47/0.65 fof(c22,negated_conjecture,((![W0]:((~aElementOf0(W0,xS)|((~aElementOf0(W0,xS)|(?[W1]:(aElementOf0(W1,xT)&~sdtlseqdt0(W1,W0))))&~aUpperBoundOfIn0(W0,xT,xS)))|(?[W1]:(((aElementOf0(W1,xS)&(![W2]:(~aElementOf0(W2,xT)|sdtlseqdt0(W2,W1))))&aUpperBoundOfIn0(W1,xT,xS))&~sdtlseqdt0(W0,W1)))))&(![W0]:~aSupremumOfIn0(W0,xT,xS))),inference(shift_quantors,[status(thm)],[c21])).
% 0.47/0.65 fof(c23,negated_conjecture,((![X2]:((~aElementOf0(X2,xS)|((~aElementOf0(X2,xS)|(?[X3]:(aElementOf0(X3,xT)&~sdtlseqdt0(X3,X2))))&~aUpperBoundOfIn0(X2,xT,xS)))|(?[X4]:(((aElementOf0(X4,xS)&(![X5]:(~aElementOf0(X5,xT)|sdtlseqdt0(X5,X4))))&aUpperBoundOfIn0(X4,xT,xS))&~sdtlseqdt0(X2,X4)))))&(![X6]:~aSupremumOfIn0(X6,xT,xS))),inference(variable_rename,[status(thm)],[c22])).
% 0.47/0.65 fof(c25,negated_conjecture,(![X2]:(![X5]:(![X6]:(((~aElementOf0(X2,xS)|((~aElementOf0(X2,xS)|(aElementOf0(skolem0001(X2),xT)&~sdtlseqdt0(skolem0001(X2),X2)))&~aUpperBoundOfIn0(X2,xT,xS)))|(((aElementOf0(skolem0002(X2),xS)&(~aElementOf0(X5,xT)|sdtlseqdt0(X5,skolem0002(X2))))&aUpperBoundOfIn0(skolem0002(X2),xT,xS))&~sdtlseqdt0(X2,skolem0002(X2))))&~aSupremumOfIn0(X6,xT,xS))))),inference(shift_quantors,[status(thm)],[fof(c24,negated_conjecture,((![X2]:((~aElementOf0(X2,xS)|((~aElementOf0(X2,xS)|(aElementOf0(skolem0001(X2),xT)&~sdtlseqdt0(skolem0001(X2),X2)))&~aUpperBoundOfIn0(X2,xT,xS)))|(((aElementOf0(skolem0002(X2),xS)&(![X5]:(~aElementOf0(X5,xT)|sdtlseqdt0(X5,skolem0002(X2)))))&aUpperBoundOfIn0(skolem0002(X2),xT,xS))&~sdtlseqdt0(X2,skolem0002(X2)))))&(![X6]:~aSupremumOfIn0(X6,xT,xS))),inference(skolemize,[status(esa)],[c23])).])).
% 0.47/0.65 fof(c26,negated_conjecture,(![X2]:(![X5]:(![X6]:((((((((~aElementOf0(X2,xS)|(~aElementOf0(X2,xS)|aElementOf0(skolem0001(X2),xT)))|aElementOf0(skolem0002(X2),xS))&((~aElementOf0(X2,xS)|(~aElementOf0(X2,xS)|aElementOf0(skolem0001(X2),xT)))|(~aElementOf0(X5,xT)|sdtlseqdt0(X5,skolem0002(X2)))))&((~aElementOf0(X2,xS)|(~aElementOf0(X2,xS)|aElementOf0(skolem0001(X2),xT)))|aUpperBoundOfIn0(skolem0002(X2),xT,xS)))&((~aElementOf0(X2,xS)|(~aElementOf0(X2,xS)|aElementOf0(skolem0001(X2),xT)))|~sdtlseqdt0(X2,skolem0002(X2))))&(((((~aElementOf0(X2,xS)|(~aElementOf0(X2,xS)|~sdtlseqdt0(skolem0001(X2),X2)))|aElementOf0(skolem0002(X2),xS))&((~aElementOf0(X2,xS)|(~aElementOf0(X2,xS)|~sdtlseqdt0(skolem0001(X2),X2)))|(~aElementOf0(X5,xT)|sdtlseqdt0(X5,skolem0002(X2)))))&((~aElementOf0(X2,xS)|(~aElementOf0(X2,xS)|~sdtlseqdt0(skolem0001(X2),X2)))|aUpperBoundOfIn0(skolem0002(X2),xT,xS)))&((~aElementOf0(X2,xS)|(~aElementOf0(X2,xS)|~sdtlseqdt0(skolem0001(X2),X2)))|~sdtlseqdt0(X2,skolem0002(X2)))))&(((((~aElementOf0(X2,xS)|~aUpperBoundOfIn0(X2,xT,xS))|aElementOf0(skolem0002(X2),xS))&((~aElementOf0(X2,xS)|~aUpperBoundOfIn0(X2,xT,xS))|(~aElementOf0(X5,xT)|sdtlseqdt0(X5,skolem0002(X2)))))&((~aElementOf0(X2,xS)|~aUpperBoundOfIn0(X2,xT,xS))|aUpperBoundOfIn0(skolem0002(X2),xT,xS)))&((~aElementOf0(X2,xS)|~aUpperBoundOfIn0(X2,xT,xS))|~sdtlseqdt0(X2,skolem0002(X2)))))&~aSupremumOfIn0(X6,xT,xS))))),inference(distribute,[status(thm)],[c25])).
% 0.47/0.65 cnf(c39,negated_conjecture,~aSupremumOfIn0(X114,xT,xS),inference(split_conjunct,[status(thm)],[c26])).
% 0.47/0.65 fof(m__1330,plain,((((((aElementOf0(xp,szDzozmdt0(xf))&sdtlpdtrp0(xf,xp)=xp)&aFixedPointOf0(xp,xf))&(![W0]:(aElementOf0(W0,xT)=>sdtlseqdt0(W0,xp))))&aUpperBoundOfIn0(xp,xT,xS))&(![W0]:(((aElementOf0(W0,xS)&(![W1]:(aElementOf0(W1,xT)=>sdtlseqdt0(W1,W0))))|aUpperBoundOfIn0(W0,xT,xS))=>sdtlseqdt0(xp,W0))))&aSupremumOfIn0(xp,xT,xS)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__1330)).
% 0.47/0.65 fof(c40,plain,((((((aElementOf0(xp,szDzozmdt0(xf))&sdtlpdtrp0(xf,xp)=xp)&aFixedPointOf0(xp,xf))&(![W0]:(~aElementOf0(W0,xT)|sdtlseqdt0(W0,xp))))&aUpperBoundOfIn0(xp,xT,xS))&(![W0]:(((~aElementOf0(W0,xS)|(?[W1]:(aElementOf0(W1,xT)&~sdtlseqdt0(W1,W0))))&~aUpperBoundOfIn0(W0,xT,xS))|sdtlseqdt0(xp,W0))))&aSupremumOfIn0(xp,xT,xS)),inference(fof_nnf,[status(thm)],[m__1330])).
% 0.47/0.65 fof(c41,plain,((((((aElementOf0(xp,szDzozmdt0(xf))&sdtlpdtrp0(xf,xp)=xp)&aFixedPointOf0(xp,xf))&(![X7]:(~aElementOf0(X7,xT)|sdtlseqdt0(X7,xp))))&aUpperBoundOfIn0(xp,xT,xS))&(![X8]:(((~aElementOf0(X8,xS)|(?[X9]:(aElementOf0(X9,xT)&~sdtlseqdt0(X9,X8))))&~aUpperBoundOfIn0(X8,xT,xS))|sdtlseqdt0(xp,X8))))&aSupremumOfIn0(xp,xT,xS)),inference(variable_rename,[status(thm)],[c40])).
% 0.47/0.65 fof(c43,plain,(![X7]:(![X8]:((((((aElementOf0(xp,szDzozmdt0(xf))&sdtlpdtrp0(xf,xp)=xp)&aFixedPointOf0(xp,xf))&(~aElementOf0(X7,xT)|sdtlseqdt0(X7,xp)))&aUpperBoundOfIn0(xp,xT,xS))&(((~aElementOf0(X8,xS)|(aElementOf0(skolem0003(X8),xT)&~sdtlseqdt0(skolem0003(X8),X8)))&~aUpperBoundOfIn0(X8,xT,xS))|sdtlseqdt0(xp,X8)))&aSupremumOfIn0(xp,xT,xS)))),inference(shift_quantors,[status(thm)],[fof(c42,plain,((((((aElementOf0(xp,szDzozmdt0(xf))&sdtlpdtrp0(xf,xp)=xp)&aFixedPointOf0(xp,xf))&(![X7]:(~aElementOf0(X7,xT)|sdtlseqdt0(X7,xp))))&aUpperBoundOfIn0(xp,xT,xS))&(![X8]:(((~aElementOf0(X8,xS)|(aElementOf0(skolem0003(X8),xT)&~sdtlseqdt0(skolem0003(X8),X8)))&~aUpperBoundOfIn0(X8,xT,xS))|sdtlseqdt0(xp,X8))))&aSupremumOfIn0(xp,xT,xS)),inference(skolemize,[status(esa)],[c41])).])).
% 0.47/0.65 fof(c44,plain,(![X7]:(![X8]:((((((aElementOf0(xp,szDzozmdt0(xf))&sdtlpdtrp0(xf,xp)=xp)&aFixedPointOf0(xp,xf))&(~aElementOf0(X7,xT)|sdtlseqdt0(X7,xp)))&aUpperBoundOfIn0(xp,xT,xS))&((((~aElementOf0(X8,xS)|aElementOf0(skolem0003(X8),xT))|sdtlseqdt0(xp,X8))&((~aElementOf0(X8,xS)|~sdtlseqdt0(skolem0003(X8),X8))|sdtlseqdt0(xp,X8)))&(~aUpperBoundOfIn0(X8,xT,xS)|sdtlseqdt0(xp,X8))))&aSupremumOfIn0(xp,xT,xS)))),inference(distribute,[status(thm)],[c43])).
% 0.47/0.65 cnf(c53,plain,aSupremumOfIn0(xp,xT,xS),inference(split_conjunct,[status(thm)],[c44])).
% 0.47/0.65 cnf(c303,plain,$false,inference(resolution,[status(thm)],[c53, c39])).
% 0.47/0.65 % SZS output end CNFRefutation
% 0.47/0.65
% 0.47/0.65 % Initial clauses : 178
% 0.47/0.65 % Processed clauses : 23
% 0.47/0.65 % Factors computed : 1
% 0.47/0.65 % Resolvents computed: 6
% 0.47/0.65 % Tautologies deleted: 0
% 0.47/0.65 % Forward subsumed : 5
% 0.47/0.65 % Backward subsumed : 0
% 0.47/0.65 % -------- CPU Time ---------
% 0.47/0.65 % User time : 0.290 s
% 0.47/0.65 % System time : 0.016 s
% 0.47/0.65 % Total time : 0.306 s
%------------------------------------------------------------------------------