%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LAT385+4 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n015.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:12 EDT 2024
% Result : Theorem 4.29s 4.47s
% Output : Refutation 4.29s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : LAT385+4 : TPTP v8.1.2. Released v4.0.0.
% 0.08/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n015.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Wed May 8 12:51:23 EDT 2024
% 0.14/0.36 % CPUTime :
% 4.29/4.47 % Version: 1.5
% 4.29/4.47 % SZS status Theorem
% 4.29/4.47 % SZS output start CNFRefutation
% 4.29/4.47 fof(m__,conjecture,(?[W0]:(((aElementOf0(W0,xU)&((aElementOf0(W0,xU)&(![W1]:(aElementOf0(W1,xP)=>sdtlseqdt0(W0,W1))))|aLowerBoundOfIn0(W0,xP,xU)))&(![W1]:(((aElementOf0(W1,xU)&(![W2]:(aElementOf0(W2,xP)=>sdtlseqdt0(W1,W2))))&aLowerBoundOfIn0(W1,xP,xU))=>sdtlseqdt0(W1,W0))))|aInfimumOfIn0(W0,xP,xU))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__)).
% 4.29/4.47 fof(c20,negated_conjecture,(~(?[W0]:(((aElementOf0(W0,xU)&((aElementOf0(W0,xU)&(![W1]:(aElementOf0(W1,xP)=>sdtlseqdt0(W0,W1))))|aLowerBoundOfIn0(W0,xP,xU)))&(![W1]:(((aElementOf0(W1,xU)&(![W2]:(aElementOf0(W2,xP)=>sdtlseqdt0(W1,W2))))&aLowerBoundOfIn0(W1,xP,xU))=>sdtlseqdt0(W1,W0))))|aInfimumOfIn0(W0,xP,xU)))),inference(assume_negation,[status(cth)],[m__])).
% 4.29/4.47 fof(c21,negated_conjecture,(![W0]:(((~aElementOf0(W0,xU)|((~aElementOf0(W0,xU)|(?[W1]:(aElementOf0(W1,xP)&~sdtlseqdt0(W0,W1))))&~aLowerBoundOfIn0(W0,xP,xU)))|(?[W1]:(((aElementOf0(W1,xU)&(![W2]:(~aElementOf0(W2,xP)|sdtlseqdt0(W1,W2))))&aLowerBoundOfIn0(W1,xP,xU))&~sdtlseqdt0(W1,W0))))&~aInfimumOfIn0(W0,xP,xU))),inference(fof_nnf,[status(thm)],[c20])).
% 4.29/4.47 fof(c22,negated_conjecture,((![W0]:((~aElementOf0(W0,xU)|((~aElementOf0(W0,xU)|(?[W1]:(aElementOf0(W1,xP)&~sdtlseqdt0(W0,W1))))&~aLowerBoundOfIn0(W0,xP,xU)))|(?[W1]:(((aElementOf0(W1,xU)&(![W2]:(~aElementOf0(W2,xP)|sdtlseqdt0(W1,W2))))&aLowerBoundOfIn0(W1,xP,xU))&~sdtlseqdt0(W1,W0)))))&(![W0]:~aInfimumOfIn0(W0,xP,xU))),inference(shift_quantors,[status(thm)],[c21])).
% 4.29/4.47 fof(c23,negated_conjecture,((![X2]:((~aElementOf0(X2,xU)|((~aElementOf0(X2,xU)|(?[X3]:(aElementOf0(X3,xP)&~sdtlseqdt0(X2,X3))))&~aLowerBoundOfIn0(X2,xP,xU)))|(?[X4]:(((aElementOf0(X4,xU)&(![X5]:(~aElementOf0(X5,xP)|sdtlseqdt0(X4,X5))))&aLowerBoundOfIn0(X4,xP,xU))&~sdtlseqdt0(X4,X2)))))&(![X6]:~aInfimumOfIn0(X6,xP,xU))),inference(variable_rename,[status(thm)],[c22])).
% 4.29/4.47 fof(c25,negated_conjecture,(![X2]:(![X5]:(![X6]:(((~aElementOf0(X2,xU)|((~aElementOf0(X2,xU)|(aElementOf0(skolem0001(X2),xP)&~sdtlseqdt0(X2,skolem0001(X2))))&~aLowerBoundOfIn0(X2,xP,xU)))|(((aElementOf0(skolem0002(X2),xU)&(~aElementOf0(X5,xP)|sdtlseqdt0(skolem0002(X2),X5)))&aLowerBoundOfIn0(skolem0002(X2),xP,xU))&~sdtlseqdt0(skolem0002(X2),X2)))&~aInfimumOfIn0(X6,xP,xU))))),inference(shift_quantors,[status(thm)],[fof(c24,negated_conjecture,((![X2]:((~aElementOf0(X2,xU)|((~aElementOf0(X2,xU)|(aElementOf0(skolem0001(X2),xP)&~sdtlseqdt0(X2,skolem0001(X2))))&~aLowerBoundOfIn0(X2,xP,xU)))|(((aElementOf0(skolem0002(X2),xU)&(![X5]:(~aElementOf0(X5,xP)|sdtlseqdt0(skolem0002(X2),X5))))&aLowerBoundOfIn0(skolem0002(X2),xP,xU))&~sdtlseqdt0(skolem0002(X2),X2))))&(![X6]:~aInfimumOfIn0(X6,xP,xU))),inference(skolemize,[status(esa)],[c23])).])).
% 4.29/4.47 fof(c26,negated_conjecture,(![X2]:(![X5]:(![X6]:((((((((~aElementOf0(X2,xU)|(~aElementOf0(X2,xU)|aElementOf0(skolem0001(X2),xP)))|aElementOf0(skolem0002(X2),xU))&((~aElementOf0(X2,xU)|(~aElementOf0(X2,xU)|aElementOf0(skolem0001(X2),xP)))|(~aElementOf0(X5,xP)|sdtlseqdt0(skolem0002(X2),X5))))&((~aElementOf0(X2,xU)|(~aElementOf0(X2,xU)|aElementOf0(skolem0001(X2),xP)))|aLowerBoundOfIn0(skolem0002(X2),xP,xU)))&((~aElementOf0(X2,xU)|(~aElementOf0(X2,xU)|aElementOf0(skolem0001(X2),xP)))|~sdtlseqdt0(skolem0002(X2),X2)))&(((((~aElementOf0(X2,xU)|(~aElementOf0(X2,xU)|~sdtlseqdt0(X2,skolem0001(X2))))|aElementOf0(skolem0002(X2),xU))&((~aElementOf0(X2,xU)|(~aElementOf0(X2,xU)|~sdtlseqdt0(X2,skolem0001(X2))))|(~aElementOf0(X5,xP)|sdtlseqdt0(skolem0002(X2),X5))))&((~aElementOf0(X2,xU)|(~aElementOf0(X2,xU)|~sdtlseqdt0(X2,skolem0001(X2))))|aLowerBoundOfIn0(skolem0002(X2),xP,xU)))&((~aElementOf0(X2,xU)|(~aElementOf0(X2,xU)|~sdtlseqdt0(X2,skolem0001(X2))))|~sdtlseqdt0(skolem0002(X2),X2))))&(((((~aElementOf0(X2,xU)|~aLowerBoundOfIn0(X2,xP,xU))|aElementOf0(skolem0002(X2),xU))&((~aElementOf0(X2,xU)|~aLowerBoundOfIn0(X2,xP,xU))|(~aElementOf0(X5,xP)|sdtlseqdt0(skolem0002(X2),X5))))&((~aElementOf0(X2,xU)|~aLowerBoundOfIn0(X2,xP,xU))|aLowerBoundOfIn0(skolem0002(X2),xP,xU)))&((~aElementOf0(X2,xU)|~aLowerBoundOfIn0(X2,xP,xU))|~sdtlseqdt0(skolem0002(X2),X2))))&~aInfimumOfIn0(X6,xP,xU))))),inference(distribute,[status(thm)],[c25])).
% 4.29/4.47 cnf(c39,negated_conjecture,~aInfimumOfIn0(X106,xP,xU),inference(split_conjunct,[status(thm)],[c26])).
% 4.29/4.47 fof(m__1244,plain,((aSet0(xP)&(![W0]:((aElementOf0(W0,xP)=>(((aElementOf0(W0,xU)&sdtlseqdt0(sdtlpdtrp0(xf,W0),W0))&(![W1]:(aElementOf0(W1,xT)=>sdtlseqdt0(W1,W0))))&aUpperBoundOfIn0(W0,xT,xU)))&(((aElementOf0(W0,xU)&sdtlseqdt0(sdtlpdtrp0(xf,W0),W0))&((![W1]:(aElementOf0(W1,xT)=>sdtlseqdt0(W1,W0)))|aUpperBoundOfIn0(W0,xT,xU)))=>aElementOf0(W0,xP)))))&xP=cS1241(xU,xf,xT)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__1244)).
% 4.29/4.47 fof(c40,plain,((aSet0(xP)&(![W0]:((~aElementOf0(W0,xP)|(((aElementOf0(W0,xU)&sdtlseqdt0(sdtlpdtrp0(xf,W0),W0))&(![W1]:(~aElementOf0(W1,xT)|sdtlseqdt0(W1,W0))))&aUpperBoundOfIn0(W0,xT,xU)))&(((~aElementOf0(W0,xU)|~sdtlseqdt0(sdtlpdtrp0(xf,W0),W0))|((?[W1]:(aElementOf0(W1,xT)&~sdtlseqdt0(W1,W0)))&~aUpperBoundOfIn0(W0,xT,xU)))|aElementOf0(W0,xP)))))&xP=cS1241(xU,xf,xT)),inference(fof_nnf,[status(thm)],[m__1244])).
% 4.29/4.47 fof(c41,plain,((aSet0(xP)&((![W0]:(~aElementOf0(W0,xP)|(((aElementOf0(W0,xU)&sdtlseqdt0(sdtlpdtrp0(xf,W0),W0))&(![W1]:(~aElementOf0(W1,xT)|sdtlseqdt0(W1,W0))))&aUpperBoundOfIn0(W0,xT,xU))))&(![W0]:(((~aElementOf0(W0,xU)|~sdtlseqdt0(sdtlpdtrp0(xf,W0),W0))|((?[W1]:(aElementOf0(W1,xT)&~sdtlseqdt0(W1,W0)))&~aUpperBoundOfIn0(W0,xT,xU)))|aElementOf0(W0,xP)))))&xP=cS1241(xU,xf,xT)),inference(shift_quantors,[status(thm)],[c40])).
% 4.29/4.47 fof(c42,plain,((aSet0(xP)&((![X7]:(~aElementOf0(X7,xP)|(((aElementOf0(X7,xU)&sdtlseqdt0(sdtlpdtrp0(xf,X7),X7))&(![X8]:(~aElementOf0(X8,xT)|sdtlseqdt0(X8,X7))))&aUpperBoundOfIn0(X7,xT,xU))))&(![X9]:(((~aElementOf0(X9,xU)|~sdtlseqdt0(sdtlpdtrp0(xf,X9),X9))|((?[X10]:(aElementOf0(X10,xT)&~sdtlseqdt0(X10,X9)))&~aUpperBoundOfIn0(X9,xT,xU)))|aElementOf0(X9,xP)))))&xP=cS1241(xU,xf,xT)),inference(variable_rename,[status(thm)],[c41])).
% 4.29/4.47 fof(c44,plain,(![X7]:(![X8]:(![X9]:((aSet0(xP)&((~aElementOf0(X7,xP)|(((aElementOf0(X7,xU)&sdtlseqdt0(sdtlpdtrp0(xf,X7),X7))&(~aElementOf0(X8,xT)|sdtlseqdt0(X8,X7)))&aUpperBoundOfIn0(X7,xT,xU)))&(((~aElementOf0(X9,xU)|~sdtlseqdt0(sdtlpdtrp0(xf,X9),X9))|((aElementOf0(skolem0003(X9),xT)&~sdtlseqdt0(skolem0003(X9),X9))&~aUpperBoundOfIn0(X9,xT,xU)))|aElementOf0(X9,xP))))&xP=cS1241(xU,xf,xT))))),inference(shift_quantors,[status(thm)],[fof(c43,plain,((aSet0(xP)&((![X7]:(~aElementOf0(X7,xP)|(((aElementOf0(X7,xU)&sdtlseqdt0(sdtlpdtrp0(xf,X7),X7))&(![X8]:(~aElementOf0(X8,xT)|sdtlseqdt0(X8,X7))))&aUpperBoundOfIn0(X7,xT,xU))))&(![X9]:(((~aElementOf0(X9,xU)|~sdtlseqdt0(sdtlpdtrp0(xf,X9),X9))|((aElementOf0(skolem0003(X9),xT)&~sdtlseqdt0(skolem0003(X9),X9))&~aUpperBoundOfIn0(X9,xT,xU)))|aElementOf0(X9,xP)))))&xP=cS1241(xU,xf,xT)),inference(skolemize,[status(esa)],[c42])).])).
% 4.29/4.47 fof(c45,plain,(![X7]:(![X8]:(![X9]:((aSet0(xP)&(((((~aElementOf0(X7,xP)|aElementOf0(X7,xU))&(~aElementOf0(X7,xP)|sdtlseqdt0(sdtlpdtrp0(xf,X7),X7)))&(~aElementOf0(X7,xP)|(~aElementOf0(X8,xT)|sdtlseqdt0(X8,X7))))&(~aElementOf0(X7,xP)|aUpperBoundOfIn0(X7,xT,xU)))&(((((~aElementOf0(X9,xU)|~sdtlseqdt0(sdtlpdtrp0(xf,X9),X9))|aElementOf0(skolem0003(X9),xT))|aElementOf0(X9,xP))&(((~aElementOf0(X9,xU)|~sdtlseqdt0(sdtlpdtrp0(xf,X9),X9))|~sdtlseqdt0(skolem0003(X9),X9))|aElementOf0(X9,xP)))&(((~aElementOf0(X9,xU)|~sdtlseqdt0(sdtlpdtrp0(xf,X9),X9))|~aUpperBoundOfIn0(X9,xT,xU))|aElementOf0(X9,xP)))))&xP=cS1241(xU,xf,xT))))),inference(distribute,[status(thm)],[c44])).
% 4.29/4.47 cnf(c46,plain,aSet0(xP),inference(split_conjunct,[status(thm)],[c45])).
% 4.29/4.47 fof(m__1123,plain,((((((((aSet0(xU)&(![W0]:(((aSet0(W0)&(![W1]:(aElementOf0(W1,W0)=>aElementOf0(W1,xU))))|aSubsetOf0(W0,xU))=>(?[W1]:((((((aElementOf0(W1,xU)&aElementOf0(W1,xU))&(![W2]:(aElementOf0(W2,W0)=>sdtlseqdt0(W1,W2))))&aLowerBoundOfIn0(W1,W0,xU))&(![W2]:(((aElementOf0(W2,xU)&(![W3]:(aElementOf0(W3,W0)=>sdtlseqdt0(W2,W3))))|aLowerBoundOfIn0(W2,W0,xU))=>sdtlseqdt0(W2,W1))))&aInfimumOfIn0(W1,W0,xU))&(?[W2]:(((((aElementOf0(W2,xU)&aElementOf0(W2,xU))&(![W3]:(aElementOf0(W3,W0)=>sdtlseqdt0(W3,W2))))&aUpperBoundOfIn0(W2,W0,xU))&(![W3]:(((aElementOf0(W3,xU)&(![W4]:(aElementOf0(W4,W0)=>sdtlseqdt0(W4,W3))))|aUpperBoundOfIn0(W3,W0,xU))=>sdtlseqdt0(W2,W3))))&aSupremumOfIn0(W2,W0,xU))))))))&aCompleteLattice0(xU))&aFunction0(xf))&(![W0]:(![W1]:((aElementOf0(W0,szDzozmdt0(xf))&aElementOf0(W1,szDzozmdt0(xf)))=>(sdtlseqdt0(W0,W1)=>sdtlseqdt0(sdtlpdtrp0(xf,W0),sdtlpdtrp0(xf,W1)))))))&isMonotone0(xf))&szDzozmdt0(xf)=szRzazndt0(xf))&szRzazndt0(xf)=xU)&isOn0(xf,xU)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__1123)).
% 4.29/4.47 fof(c73,plain,((((((((aSet0(xU)&(![W0]:(((aSet0(W0)&(![W1]:(aElementOf0(W1,W0)=>aElementOf0(W1,xU))))|aSubsetOf0(W0,xU))=>(?[W1]:(((((aElementOf0(W1,xU)&(![W2]:(aElementOf0(W2,W0)=>sdtlseqdt0(W1,W2))))&aLowerBoundOfIn0(W1,W0,xU))&(![W2]:(((aElementOf0(W2,xU)&(![W3]:(aElementOf0(W3,W0)=>sdtlseqdt0(W2,W3))))|aLowerBoundOfIn0(W2,W0,xU))=>sdtlseqdt0(W2,W1))))&aInfimumOfIn0(W1,W0,xU))&(?[W2]:((((aElementOf0(W2,xU)&(![W3]:(aElementOf0(W3,W0)=>sdtlseqdt0(W3,W2))))&aUpperBoundOfIn0(W2,W0,xU))&(![W3]:(((aElementOf0(W3,xU)&(![W4]:(aElementOf0(W4,W0)=>sdtlseqdt0(W4,W3))))|aUpperBoundOfIn0(W3,W0,xU))=>sdtlseqdt0(W2,W3))))&aSupremumOfIn0(W2,W0,xU))))))))&aCompleteLattice0(xU))&aFunction0(xf))&(![W0]:(![W1]:((aElementOf0(W0,szDzozmdt0(xf))&aElementOf0(W1,szDzozmdt0(xf)))=>(sdtlseqdt0(W0,W1)=>sdtlseqdt0(sdtlpdtrp0(xf,W0),sdtlpdtrp0(xf,W1)))))))&isMonotone0(xf))&szDzozmdt0(xf)=szRzazndt0(xf))&szRzazndt0(xf)=xU)&isOn0(xf,xU)),inference(fof_simplification,[status(thm)],[m__1123])).
% 4.29/4.47 fof(c74,plain,((((((((aSet0(xU)&(![W0]:(((~aSet0(W0)|(?[W1]:(aElementOf0(W1,W0)&~aElementOf0(W1,xU))))&~aSubsetOf0(W0,xU))|(?[W1]:(((((aElementOf0(W1,xU)&(![W2]:(~aElementOf0(W2,W0)|sdtlseqdt0(W1,W2))))&aLowerBoundOfIn0(W1,W0,xU))&(![W2]:(((~aElementOf0(W2,xU)|(?[W3]:(aElementOf0(W3,W0)&~sdtlseqdt0(W2,W3))))&~aLowerBoundOfIn0(W2,W0,xU))|sdtlseqdt0(W2,W1))))&aInfimumOfIn0(W1,W0,xU))&(?[W2]:((((aElementOf0(W2,xU)&(![W3]:(~aElementOf0(W3,W0)|sdtlseqdt0(W3,W2))))&aUpperBoundOfIn0(W2,W0,xU))&(![W3]:(((~aElementOf0(W3,xU)|(?[W4]:(aElementOf0(W4,W0)&~sdtlseqdt0(W4,W3))))&~aUpperBoundOfIn0(W3,W0,xU))|sdtlseqdt0(W2,W3))))&aSupremumOfIn0(W2,W0,xU))))))))&aCompleteLattice0(xU))&aFunction0(xf))&(![W0]:(![W1]:((~aElementOf0(W0,szDzozmdt0(xf))|~aElementOf0(W1,szDzozmdt0(xf)))|(~sdtlseqdt0(W0,W1)|sdtlseqdt0(sdtlpdtrp0(xf,W0),sdtlpdtrp0(xf,W1)))))))&isMonotone0(xf))&szDzozmdt0(xf)=szRzazndt0(xf))&szRzazndt0(xf)=xU)&isOn0(xf,xU)),inference(fof_nnf,[status(thm)],[c73])).
% 4.29/4.47 fof(c75,plain,((((((((aSet0(xU)&(![W0]:(((~aSet0(W0)|(?[W1]:(aElementOf0(W1,W0)&~aElementOf0(W1,xU))))&~aSubsetOf0(W0,xU))|((?[W1]:((((aElementOf0(W1,xU)&(![W2]:(~aElementOf0(W2,W0)|sdtlseqdt0(W1,W2))))&aLowerBoundOfIn0(W1,W0,xU))&(![W2]:(((~aElementOf0(W2,xU)|(?[W3]:(aElementOf0(W3,W0)&~sdtlseqdt0(W2,W3))))&~aLowerBoundOfIn0(W2,W0,xU))|sdtlseqdt0(W2,W1))))&aInfimumOfIn0(W1,W0,xU)))&(?[W2]:((((aElementOf0(W2,xU)&(![W3]:(~aElementOf0(W3,W0)|sdtlseqdt0(W3,W2))))&aUpperBoundOfIn0(W2,W0,xU))&(![W3]:(((~aElementOf0(W3,xU)|(?[W4]:(aElementOf0(W4,W0)&~sdtlseqdt0(W4,W3))))&~aUpperBoundOfIn0(W3,W0,xU))|sdtlseqdt0(W2,W3))))&aSupremumOfIn0(W2,W0,xU)))))))&aCompleteLattice0(xU))&aFunction0(xf))&(![W0]:(![W1]:((~aElementOf0(W0,szDzozmdt0(xf))|~aElementOf0(W1,szDzozmdt0(xf)))|(~sdtlseqdt0(W0,W1)|sdtlseqdt0(sdtlpdtrp0(xf,W0),sdtlpdtrp0(xf,W1)))))))&isMonotone0(xf))&szDzozmdt0(xf)=szRzazndt0(xf))&szRzazndt0(xf)=xU)&isOn0(xf,xU)),inference(shift_quantors,[status(thm)],[c74])).
% 4.29/4.47 fof(c76,plain,((((((((aSet0(xU)&(![X14]:(((~aSet0(X14)|(?[X15]:(aElementOf0(X15,X14)&~aElementOf0(X15,xU))))&~aSubsetOf0(X14,xU))|((?[X16]:((((aElementOf0(X16,xU)&(![X17]:(~aElementOf0(X17,X14)|sdtlseqdt0(X16,X17))))&aLowerBoundOfIn0(X16,X14,xU))&(![X18]:(((~aElementOf0(X18,xU)|(?[X19]:(aElementOf0(X19,X14)&~sdtlseqdt0(X18,X19))))&~aLowerBoundOfIn0(X18,X14,xU))|sdtlseqdt0(X18,X16))))&aInfimumOfIn0(X16,X14,xU)))&(?[X20]:((((aElementOf0(X20,xU)&(![X21]:(~aElementOf0(X21,X14)|sdtlseqdt0(X21,X20))))&aUpperBoundOfIn0(X20,X14,xU))&(![X22]:(((~aElementOf0(X22,xU)|(?[X23]:(aElementOf0(X23,X14)&~sdtlseqdt0(X23,X22))))&~aUpperBoundOfIn0(X22,X14,xU))|sdtlseqdt0(X20,X22))))&aSupremumOfIn0(X20,X14,xU)))))))&aCompleteLattice0(xU))&aFunction0(xf))&(![X24]:(![X25]:((~aElementOf0(X24,szDzozmdt0(xf))|~aElementOf0(X25,szDzozmdt0(xf)))|(~sdtlseqdt0(X24,X25)|sdtlseqdt0(sdtlpdtrp0(xf,X24),sdtlpdtrp0(xf,X25)))))))&isMonotone0(xf))&szDzozmdt0(xf)=szRzazndt0(xf))&szRzazndt0(xf)=xU)&isOn0(xf,xU)),inference(variable_rename,[status(thm)],[c75])).
% 4.29/4.47 fof(c78,plain,(![X14]:(![X17]:(![X18]:(![X21]:(![X22]:(![X24]:(![X25]:((((((((aSet0(xU)&(((~aSet0(X14)|(aElementOf0(skolem0004(X14),X14)&~aElementOf0(skolem0004(X14),xU)))&~aSubsetOf0(X14,xU))|(((((aElementOf0(skolem0005(X14),xU)&(~aElementOf0(X17,X14)|sdtlseqdt0(skolem0005(X14),X17)))&aLowerBoundOfIn0(skolem0005(X14),X14,xU))&(((~aElementOf0(X18,xU)|(aElementOf0(skolem0006(X14,X18),X14)&~sdtlseqdt0(X18,skolem0006(X14,X18))))&~aLowerBoundOfIn0(X18,X14,xU))|sdtlseqdt0(X18,skolem0005(X14))))&aInfimumOfIn0(skolem0005(X14),X14,xU))&((((aElementOf0(skolem0007(X14),xU)&(~aElementOf0(X21,X14)|sdtlseqdt0(X21,skolem0007(X14))))&aUpperBoundOfIn0(skolem0007(X14),X14,xU))&(((~aElementOf0(X22,xU)|(aElementOf0(skolem0008(X14,X22),X14)&~sdtlseqdt0(skolem0008(X14,X22),X22)))&~aUpperBoundOfIn0(X22,X14,xU))|sdtlseqdt0(skolem0007(X14),X22)))&aSupremumOfIn0(skolem0007(X14),X14,xU)))))&aCompleteLattice0(xU))&aFunction0(xf))&((~aElementOf0(X24,szDzozmdt0(xf))|~aElementOf0(X25,szDzozmdt0(xf)))|(~sdtlseqdt0(X24,X25)|sdtlseqdt0(sdtlpdtrp0(xf,X24),sdtlpdtrp0(xf,X25)))))&isMonotone0(xf))&szDzozmdt0(xf)=szRzazndt0(xf))&szRzazndt0(xf)=xU)&isOn0(xf,xU))))))))),inference(shift_quantors,[status(thm)],[fof(c77,plain,((((((((aSet0(xU)&(![X14]:(((~aSet0(X14)|(aElementOf0(skolem0004(X14),X14)&~aElementOf0(skolem0004(X14),xU)))&~aSubsetOf0(X14,xU))|(((((aElementOf0(skolem0005(X14),xU)&(![X17]:(~aElementOf0(X17,X14)|sdtlseqdt0(skolem0005(X14),X17))))&aLowerBoundOfIn0(skolem0005(X14),X14,xU))&(![X18]:(((~aElementOf0(X18,xU)|(aElementOf0(skolem0006(X14,X18),X14)&~sdtlseqdt0(X18,skolem0006(X14,X18))))&~aLowerBoundOfIn0(X18,X14,xU))|sdtlseqdt0(X18,skolem0005(X14)))))&aInfimumOfIn0(skolem0005(X14),X14,xU))&((((aElementOf0(skolem0007(X14),xU)&(![X21]:(~aElementOf0(X21,X14)|sdtlseqdt0(X21,skolem0007(X14)))))&aUpperBoundOfIn0(skolem0007(X14),X14,xU))&(![X22]:(((~aElementOf0(X22,xU)|(aElementOf0(skolem0008(X14,X22),X14)&~sdtlseqdt0(skolem0008(X14,X22),X22)))&~aUpperBoundOfIn0(X22,X14,xU))|sdtlseqdt0(skolem0007(X14),X22))))&aSupremumOfIn0(skolem0007(X14),X14,xU))))))&aCompleteLattice0(xU))&aFunction0(xf))&(![X24]:(![X25]:((~aElementOf0(X24,szDzozmdt0(xf))|~aElementOf0(X25,szDzozmdt0(xf)))|(~sdtlseqdt0(X24,X25)|sdtlseqdt0(sdtlpdtrp0(xf,X24),sdtlpdtrp0(xf,X25)))))))&isMonotone0(xf))&szDzozmdt0(xf)=szRzazndt0(xf))&szRzazndt0(xf)=xU)&isOn0(xf,xU)),inference(skolemize,[status(esa)],[c76])).])).
% 4.29/4.47 fof(c79,plain,(![X14]:(![X17]:(![X18]:(![X21]:(![X22]:(![X24]:(![X25]:((((((((aSet0(xU)&(((((((((~aSet0(X14)|aElementOf0(skolem0004(X14),X14))|aElementOf0(skolem0005(X14),xU))&((~aSet0(X14)|aElementOf0(skolem0004(X14),X14))|(~aElementOf0(X17,X14)|sdtlseqdt0(skolem0005(X14),X17))))&((~aSet0(X14)|aElementOf0(skolem0004(X14),X14))|aLowerBoundOfIn0(skolem0005(X14),X14,xU)))&((((~aSet0(X14)|aElementOf0(skolem0004(X14),X14))|((~aElementOf0(X18,xU)|aElementOf0(skolem0006(X14,X18),X14))|sdtlseqdt0(X18,skolem0005(X14))))&((~aSet0(X14)|aElementOf0(skolem0004(X14),X14))|((~aElementOf0(X18,xU)|~sdtlseqdt0(X18,skolem0006(X14,X18)))|sdtlseqdt0(X18,skolem0005(X14)))))&((~aSet0(X14)|aElementOf0(skolem0004(X14),X14))|(~aLowerBoundOfIn0(X18,X14,xU)|sdtlseqdt0(X18,skolem0005(X14))))))&((~aSet0(X14)|aElementOf0(skolem0004(X14),X14))|aInfimumOfIn0(skolem0005(X14),X14,xU)))&((((((~aSet0(X14)|aElementOf0(skolem0004(X14),X14))|aElementOf0(skolem0007(X14),xU))&((~aSet0(X14)|aElementOf0(skolem0004(X14),X14))|(~aElementOf0(X21,X14)|sdtlseqdt0(X21,skolem0007(X14)))))&((~aSet0(X14)|aElementOf0(skolem0004(X14),X14))|aUpperBoundOfIn0(skolem0007(X14),X14,xU)))&((((~aSet0(X14)|aElementOf0(skolem0004(X14),X14))|((~aElementOf0(X22,xU)|aElementOf0(skolem0008(X14,X22),X14))|sdtlseqdt0(skolem0007(X14),X22)))&((~aSet0(X14)|aElementOf0(skolem0004(X14),X14))|((~aElementOf0(X22,xU)|~sdtlseqdt0(skolem0008(X14,X22),X22))|sdtlseqdt0(skolem0007(X14),X22))))&((~aSet0(X14)|aElementOf0(skolem0004(X14),X14))|(~aUpperBoundOfIn0(X22,X14,xU)|sdtlseqdt0(skolem0007(X14),X22)))))&((~aSet0(X14)|aElementOf0(skolem0004(X14),X14))|aSupremumOfIn0(skolem0007(X14),X14,xU))))&(((((((~aSet0(X14)|~aElementOf0(skolem0004(X14),xU))|aElementOf0(skolem0005(X14),xU))&((~aSet0(X14)|~aElementOf0(skolem0004(X14),xU))|(~aElementOf0(X17,X14)|sdtlseqdt0(skolem0005(X14),X17))))&((~aSet0(X14)|~aElementOf0(skolem0004(X14),xU))|aLowerBoundOfIn0(skolem0005(X14),X14,xU)))&((((~aSet0(X14)|~aElementOf0(skolem0004(X14),xU))|((~aElementOf0(X18,xU)|aElementOf0(skolem0006(X14,X18),X14))|sdtlseqdt0(X18,skolem0005(X14))))&((~aSet0(X14)|~aElementOf0(skolem0004(X14),xU))|((~aElementOf0(X18,xU)|~sdtlseqdt0(X18,skolem0006(X14,X18)))|sdtlseqdt0(X18,skolem0005(X14)))))&((~aSet0(X14)|~aElementOf0(skolem0004(X14),xU))|(~aLowerBoundOfIn0(X18,X14,xU)|sdtlseqdt0(X18,skolem0005(X14))))))&((~aSet0(X14)|~aElementOf0(skolem0004(X14),xU))|aInfimumOfIn0(skolem0005(X14),X14,xU)))&((((((~aSet0(X14)|~aElementOf0(skolem0004(X14),xU))|aElementOf0(skolem0007(X14),xU))&((~aSet0(X14)|~aElementOf0(skolem0004(X14),xU))|(~aElementOf0(X21,X14)|sdtlseqdt0(X21,skolem0007(X14)))))&((~aSet0(X14)|~aElementOf0(skolem0004(X14),xU))|aUpperBoundOfIn0(skolem0007(X14),X14,xU)))&((((~aSet0(X14)|~aElementOf0(skolem0004(X14),xU))|((~aElementOf0(X22,xU)|aElementOf0(skolem0008(X14,X22),X14))|sdtlseqdt0(skolem0007(X14),X22)))&((~aSet0(X14)|~aElementOf0(skolem0004(X14),xU))|((~aElementOf0(X22,xU)|~sdtlseqdt0(skolem0008(X14,X22),X22))|sdtlseqdt0(skolem0007(X14),X22))))&((~aSet0(X14)|~aElementOf0(skolem0004(X14),xU))|(~aUpperBoundOfIn0(X22,X14,xU)|sdtlseqdt0(skolem0007(X14),X22)))))&((~aSet0(X14)|~aElementOf0(skolem0004(X14),xU))|aSupremumOfIn0(skolem0007(X14),X14,xU)))))&((((((~aSubsetOf0(X14,xU)|aElementOf0(skolem0005(X14),xU))&(~aSubsetOf0(X14,xU)|(~aElementOf0(X17,X14)|sdtlseqdt0(skolem0005(X14),X17))))&(~aSubsetOf0(X14,xU)|aLowerBoundOfIn0(skolem0005(X14),X14,xU)))&(((~aSubsetOf0(X14,xU)|((~aElementOf0(X18,xU)|aElementOf0(skolem0006(X14,X18),X14))|sdtlseqdt0(X18,skolem0005(X14))))&(~aSubsetOf0(X14,xU)|((~aElementOf0(X18,xU)|~sdtlseqdt0(X18,skolem0006(X14,X18)))|sdtlseqdt0(X18,skolem0005(X14)))))&(~aSubsetOf0(X14,xU)|(~aLowerBoundOfIn0(X18,X14,xU)|sdtlseqdt0(X18,skolem0005(X14))))))&(~aSubsetOf0(X14,xU)|aInfimumOfIn0(skolem0005(X14),X14,xU)))&(((((~aSubsetOf0(X14,xU)|aElementOf0(skolem0007(X14),xU))&(~aSubsetOf0(X14,xU)|(~aElementOf0(X21,X14)|sdtlseqdt0(X21,skolem0007(X14)))))&(~aSubsetOf0(X14,xU)|aUpperBoundOfIn0(skolem0007(X14),X14,xU)))&(((~aSubsetOf0(X14,xU)|((~aElementOf0(X22,xU)|aElementOf0(skolem0008(X14,X22),X14))|sdtlseqdt0(skolem0007(X14),X22)))&(~aSubsetOf0(X14,xU)|((~aElementOf0(X22,xU)|~sdtlseqdt0(skolem0008(X14,X22),X22))|sdtlseqdt0(skolem0007(X14),X22))))&(~aSubsetOf0(X14,xU)|(~aUpperBoundOfIn0(X22,X14,xU)|sdtlseqdt0(skolem0007(X14),X22)))))&(~aSubsetOf0(X14,xU)|aSupremumOfIn0(skolem0007(X14),X14,xU))))))&aCompleteLattice0(xU))&aFunction0(xf))&((~aElementOf0(X24,szDzozmdt0(xf))|~aElementOf0(X25,szDzozmdt0(xf)))|(~sdtlseqdt0(X24,X25)|sdtlseqdt0(sdtlpdtrp0(xf,X24),sdtlpdtrp0(xf,X25)))))&isMonotone0(xf))&szDzozmdt0(xf)=szRzazndt0(xf))&szRzazndt0(xf)=xU)&isOn0(xf,xU))))))))),inference(distribute,[status(thm)],[c78])).
% 4.29/4.47 cnf(c101,plain,~aSet0(X299)|~aElementOf0(skolem0004(X299),xU)|aInfimumOfIn0(skolem0005(X299),X299,xU),inference(split_conjunct,[status(thm)],[c79])).
% 4.29/4.47 cnf(c47,plain,~aElementOf0(X156,xP)|aElementOf0(X156,xU),inference(split_conjunct,[status(thm)],[c45])).
% 4.29/4.47 cnf(c87,plain,~aSet0(X256)|aElementOf0(skolem0004(X256),X256)|aInfimumOfIn0(skolem0005(X256),X256,xU),inference(split_conjunct,[status(thm)],[c79])).
% 4.29/4.47 cnf(c774,plain,aElementOf0(skolem0004(xP),xP)|aInfimumOfIn0(skolem0005(xP),xP,xU),inference(resolution,[status(thm)],[c87, c46])).
% 4.29/4.47 cnf(c11293,plain,aElementOf0(skolem0004(xP),xP),inference(resolution,[status(thm)],[c774, c39])).
% 4.29/4.47 cnf(c11309,plain,aElementOf0(skolem0004(xP),xU),inference(resolution,[status(thm)],[c11293, c47])).
% 4.29/4.47 cnf(c11317,plain,~aSet0(xP)|aInfimumOfIn0(skolem0005(xP),xP,xU),inference(resolution,[status(thm)],[c11309, c101])).
% 4.29/4.47 cnf(c11665,plain,aInfimumOfIn0(skolem0005(xP),xP,xU),inference(resolution,[status(thm)],[c11317, c46])).
% 4.29/4.47 cnf(c11669,plain,$false,inference(resolution,[status(thm)],[c11665, c39])).
% 4.29/4.47 % SZS output end CNFRefutation
% 4.29/4.47
% 4.29/4.47 % Initial clauses : 158
% 4.29/4.47 % Processed clauses : 917
% 4.29/4.47 % Factors computed : 52
% 4.29/4.47 % Resolvents computed: 11356
% 4.29/4.47 % Tautologies deleted: 20
% 4.29/4.47 % Forward subsumed : 392
% 4.29/4.47 % Backward subsumed : 80
% 4.29/4.47 % -------- CPU Time ---------
% 4.29/4.47 % User time : 4.071 s
% 4.29/4.47 % System time : 0.039 s
% 4.29/4.47 % Total time : 4.110 s
%------------------------------------------------------------------------------