%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : LAT385+4 : TPTP v5.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %s
% Computer : art05.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 2018MB
% OS : Linux 2.6.26.8-57.fc8
% CPULimit : 300s
% DateTime : Wed Dec 29 13:20:38 EST 2010
% Result : Theorem 0.97s
% Output : Solution 0.97s
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----ERROR: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Reading problem from /tmp/SystemOnTPTP1898/LAT385+4.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP1898/LAT385+4.tptp
% SZS output start Solution for /tmp/SystemOnTPTP1898/LAT385+4.tptp
% TreeLimitedRun: ----------------------------------------------------------
% TreeLimitedRun: /home/graph/tptp/Systems/EP---1.2/eproof --print-statistics -xAuto -tAuto --cpu-limit=60 --proof-time-unlimited --memory-limit=Auto --tstp-in --tstp-out /tmp/SRASS.s.p
% TreeLimitedRun: CPU time limit is 60s
% TreeLimitedRun: WC time limit is 120s
% TreeLimitedRun: PID is 2009
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.01 WC
% # Preprocessing time : 0.020 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(15, axiom,((((((((aSet0(xU)&![X1]:(((aSet0(X1)&![X2]:(aElementOf0(X2,X1)=>aElementOf0(X2,xU)))|aSubsetOf0(X1,xU))=>?[X2]:((((((aElementOf0(X2,xU)&aElementOf0(X2,xU))&![X3]:(aElementOf0(X3,X1)=>sdtlseqdt0(X2,X3)))&aLowerBoundOfIn0(X2,X1,xU))&![X3]:(((aElementOf0(X3,xU)&![X4]:(aElementOf0(X4,X1)=>sdtlseqdt0(X3,X4)))|aLowerBoundOfIn0(X3,X1,xU))=>sdtlseqdt0(X3,X2)))&aInfimumOfIn0(X2,X1,xU))&?[X3]:(((((aElementOf0(X3,xU)&aElementOf0(X3,xU))&![X4]:(aElementOf0(X4,X1)=>sdtlseqdt0(X4,X3)))&aUpperBoundOfIn0(X3,X1,xU))&![X4]:(((aElementOf0(X4,xU)&![X5]:(aElementOf0(X5,X1)=>sdtlseqdt0(X5,X4)))|aUpperBoundOfIn0(X4,X1,xU))=>sdtlseqdt0(X3,X4)))&aSupremumOfIn0(X3,X1,xU)))))&aCompleteLattice0(xU))&aFunction0(xf))&![X1]:![X2]:((aElementOf0(X1,szDzozmdt0(xf))&aElementOf0(X2,szDzozmdt0(xf)))=>(sdtlseqdt0(X1,X2)=>sdtlseqdt0(sdtlpdtrp0(xf,X1),sdtlpdtrp0(xf,X2)))))&isMonotone0(xf))&szDzozmdt0(xf)=szRzazndt0(xf))&szRzazndt0(xf)=xU)&isOn0(xf,xU)),file('/tmp/SRASS.s.p', m__1123)).
% fof(18, axiom,((aSet0(xP)&![X1]:((aElementOf0(X1,xP)=>(((aElementOf0(X1,xU)&sdtlseqdt0(sdtlpdtrp0(xf,X1),X1))&![X2]:(aElementOf0(X2,xT)=>sdtlseqdt0(X2,X1)))&aUpperBoundOfIn0(X1,xT,xU)))&(((aElementOf0(X1,xU)&sdtlseqdt0(sdtlpdtrp0(xf,X1),X1))&(![X2]:(aElementOf0(X2,xT)=>sdtlseqdt0(X2,X1))|aUpperBoundOfIn0(X1,xT,xU)))=>aElementOf0(X1,xP))))&xP=cS1241(xU,xf,xT)),file('/tmp/SRASS.s.p', m__1244)).
% fof(28, conjecture,?[X1]:(((aElementOf0(X1,xU)&((aElementOf0(X1,xU)&![X2]:(aElementOf0(X2,xP)=>sdtlseqdt0(X1,X2)))|aLowerBoundOfIn0(X1,xP,xU)))&![X2]:(((aElementOf0(X2,xU)&![X3]:(aElementOf0(X3,xP)=>sdtlseqdt0(X2,X3)))&aLowerBoundOfIn0(X2,xP,xU))=>sdtlseqdt0(X2,X1)))|aInfimumOfIn0(X1,xP,xU)),file('/tmp/SRASS.s.p', m__)).
% fof(29, negated_conjecture,~(?[X1]:(((aElementOf0(X1,xU)&((aElementOf0(X1,xU)&![X2]:(aElementOf0(X2,xP)=>sdtlseqdt0(X1,X2)))|aLowerBoundOfIn0(X1,xP,xU)))&![X2]:(((aElementOf0(X2,xU)&![X3]:(aElementOf0(X3,xP)=>sdtlseqdt0(X2,X3)))&aLowerBoundOfIn0(X2,xP,xU))=>sdtlseqdt0(X2,X1)))|aInfimumOfIn0(X1,xP,xU))),inference(assume_negation,[status(cth)],[28])).
% fof(30, plain,((((((((aSet0(xU)&![X1]:(((aSet0(X1)&![X2]:(aElementOf0(X2,X1)=>aElementOf0(X2,xU)))|aSubsetOf0(X1,xU))=>?[X2]:(((((aElementOf0(X2,xU)&![X3]:(aElementOf0(X3,X1)=>sdtlseqdt0(X2,X3)))&aLowerBoundOfIn0(X2,X1,xU))&![X3]:(((aElementOf0(X3,xU)&![X4]:(aElementOf0(X4,X1)=>sdtlseqdt0(X3,X4)))|aLowerBoundOfIn0(X3,X1,xU))=>sdtlseqdt0(X3,X2)))&aInfimumOfIn0(X2,X1,xU))&?[X3]:((((aElementOf0(X3,xU)&![X4]:(aElementOf0(X4,X1)=>sdtlseqdt0(X4,X3)))&aUpperBoundOfIn0(X3,X1,xU))&![X4]:(((aElementOf0(X4,xU)&![X5]:(aElementOf0(X5,X1)=>sdtlseqdt0(X5,X4)))|aUpperBoundOfIn0(X4,X1,xU))=>sdtlseqdt0(X3,X4)))&aSupremumOfIn0(X3,X1,xU)))))&aCompleteLattice0(xU))&aFunction0(xf))&![X1]:![X2]:((aElementOf0(X1,szDzozmdt0(xf))&aElementOf0(X2,szDzozmdt0(xf)))=>(sdtlseqdt0(X1,X2)=>sdtlseqdt0(sdtlpdtrp0(xf,X1),sdtlpdtrp0(xf,X2)))))&isMonotone0(xf))&szDzozmdt0(xf)=szRzazndt0(xf))&szRzazndt0(xf)=xU)&isOn0(xf,xU)),inference(fof_simplification,[status(thm)],[15,theory(equality)])).
% fof(35, plain,![X1]:(epred1_1(X1)=>?[X2]:(((((aElementOf0(X2,xU)&![X3]:(aElementOf0(X3,X1)=>sdtlseqdt0(X2,X3)))&aLowerBoundOfIn0(X2,X1,xU))&![X3]:(((aElementOf0(X3,xU)&![X4]:(aElementOf0(X4,X1)=>sdtlseqdt0(X3,X4)))|aLowerBoundOfIn0(X3,X1,xU))=>sdtlseqdt0(X3,X2)))&aInfimumOfIn0(X2,X1,xU))&?[X3]:((((aElementOf0(X3,xU)&![X4]:(aElementOf0(X4,X1)=>sdtlseqdt0(X4,X3)))&aUpperBoundOfIn0(X3,X1,xU))&![X4]:(((aElementOf0(X4,xU)&![X5]:(aElementOf0(X5,X1)=>sdtlseqdt0(X5,X4)))|aUpperBoundOfIn0(X4,X1,xU))=>sdtlseqdt0(X3,X4)))&aSupremumOfIn0(X3,X1,xU)))),introduced(definition)).
% fof(36, plain,((((((((aSet0(xU)&![X1]:(((aSet0(X1)&![X2]:(aElementOf0(X2,X1)=>aElementOf0(X2,xU)))|aSubsetOf0(X1,xU))=>epred1_1(X1)))&aCompleteLattice0(xU))&aFunction0(xf))&![X1]:![X2]:((aElementOf0(X1,szDzozmdt0(xf))&aElementOf0(X2,szDzozmdt0(xf)))=>(sdtlseqdt0(X1,X2)=>sdtlseqdt0(sdtlpdtrp0(xf,X1),sdtlpdtrp0(xf,X2)))))&isMonotone0(xf))&szDzozmdt0(xf)=szRzazndt0(xf))&szRzazndt0(xf)=xU)&isOn0(xf,xU)),inference(apply_def,[status(esa)],[30,35,theory(equality)])).
% fof(135, plain,((((((((aSet0(xU)&![X1]:(((~(aSet0(X1))|?[X2]:(aElementOf0(X2,X1)&~(aElementOf0(X2,xU))))&~(aSubsetOf0(X1,xU)))|epred1_1(X1)))&aCompleteLattice0(xU))&aFunction0(xf))&![X1]:![X2]:((~(aElementOf0(X1,szDzozmdt0(xf)))|~(aElementOf0(X2,szDzozmdt0(xf))))|(~(sdtlseqdt0(X1,X2))|sdtlseqdt0(sdtlpdtrp0(xf,X1),sdtlpdtrp0(xf,X2)))))&isMonotone0(xf))&szDzozmdt0(xf)=szRzazndt0(xf))&szRzazndt0(xf)=xU)&isOn0(xf,xU)),inference(fof_nnf,[status(thm)],[36])).
% fof(136, plain,((((((((aSet0(xU)&![X3]:(((~(aSet0(X3))|?[X4]:(aElementOf0(X4,X3)&~(aElementOf0(X4,xU))))&~(aSubsetOf0(X3,xU)))|epred1_1(X3)))&aCompleteLattice0(xU))&aFunction0(xf))&![X5]:![X6]:((~(aElementOf0(X5,szDzozmdt0(xf)))|~(aElementOf0(X6,szDzozmdt0(xf))))|(~(sdtlseqdt0(X5,X6))|sdtlseqdt0(sdtlpdtrp0(xf,X5),sdtlpdtrp0(xf,X6)))))&isMonotone0(xf))&szDzozmdt0(xf)=szRzazndt0(xf))&szRzazndt0(xf)=xU)&isOn0(xf,xU)),inference(variable_rename,[status(thm)],[135])).
% fof(137, plain,((((((((aSet0(xU)&![X3]:(((~(aSet0(X3))|(aElementOf0(esk11_1(X3),X3)&~(aElementOf0(esk11_1(X3),xU))))&~(aSubsetOf0(X3,xU)))|epred1_1(X3)))&aCompleteLattice0(xU))&aFunction0(xf))&![X5]:![X6]:((~(aElementOf0(X5,szDzozmdt0(xf)))|~(aElementOf0(X6,szDzozmdt0(xf))))|(~(sdtlseqdt0(X5,X6))|sdtlseqdt0(sdtlpdtrp0(xf,X5),sdtlpdtrp0(xf,X6)))))&isMonotone0(xf))&szDzozmdt0(xf)=szRzazndt0(xf))&szRzazndt0(xf)=xU)&isOn0(xf,xU)),inference(skolemize,[status(esa)],[136])).
% fof(138, plain,![X3]:![X5]:![X6]:(((((((~(aElementOf0(X5,szDzozmdt0(xf)))|~(aElementOf0(X6,szDzozmdt0(xf))))|(~(sdtlseqdt0(X5,X6))|sdtlseqdt0(sdtlpdtrp0(xf,X5),sdtlpdtrp0(xf,X6))))&((((((~(aSet0(X3))|(aElementOf0(esk11_1(X3),X3)&~(aElementOf0(esk11_1(X3),xU))))&~(aSubsetOf0(X3,xU)))|epred1_1(X3))&aSet0(xU))&aCompleteLattice0(xU))&aFunction0(xf)))&isMonotone0(xf))&szDzozmdt0(xf)=szRzazndt0(xf))&szRzazndt0(xf)=xU)&isOn0(xf,xU)),inference(shift_quantors,[status(thm)],[137])).
% fof(139, plain,![X3]:![X5]:![X6]:(((((((~(aElementOf0(X5,szDzozmdt0(xf)))|~(aElementOf0(X6,szDzozmdt0(xf))))|(~(sdtlseqdt0(X5,X6))|sdtlseqdt0(sdtlpdtrp0(xf,X5),sdtlpdtrp0(xf,X6))))&(((((((aElementOf0(esk11_1(X3),X3)|~(aSet0(X3)))|epred1_1(X3))&((~(aElementOf0(esk11_1(X3),xU))|~(aSet0(X3)))|epred1_1(X3)))&(~(aSubsetOf0(X3,xU))|epred1_1(X3)))&aSet0(xU))&aCompleteLattice0(xU))&aFunction0(xf)))&isMonotone0(xf))&szDzozmdt0(xf)=szRzazndt0(xf))&szRzazndt0(xf)=xU)&isOn0(xf,xU)),inference(distribute,[status(thm)],[138])).
% cnf(148,plain,(epred1_1(X1)|~aSet0(X1)|~aElementOf0(esk11_1(X1),xU)),inference(split_conjunct,[status(thm)],[139])).
% cnf(149,plain,(epred1_1(X1)|aElementOf0(esk11_1(X1),X1)|~aSet0(X1)),inference(split_conjunct,[status(thm)],[139])).
% fof(168, plain,((aSet0(xP)&![X1]:((~(aElementOf0(X1,xP))|(((aElementOf0(X1,xU)&sdtlseqdt0(sdtlpdtrp0(xf,X1),X1))&![X2]:(~(aElementOf0(X2,xT))|sdtlseqdt0(X2,X1)))&aUpperBoundOfIn0(X1,xT,xU)))&(((~(aElementOf0(X1,xU))|~(sdtlseqdt0(sdtlpdtrp0(xf,X1),X1)))|(?[X2]:(aElementOf0(X2,xT)&~(sdtlseqdt0(X2,X1)))&~(aUpperBoundOfIn0(X1,xT,xU))))|aElementOf0(X1,xP))))&xP=cS1241(xU,xf,xT)),inference(fof_nnf,[status(thm)],[18])).
% fof(169, plain,((aSet0(xP)&![X3]:((~(aElementOf0(X3,xP))|(((aElementOf0(X3,xU)&sdtlseqdt0(sdtlpdtrp0(xf,X3),X3))&![X4]:(~(aElementOf0(X4,xT))|sdtlseqdt0(X4,X3)))&aUpperBoundOfIn0(X3,xT,xU)))&(((~(aElementOf0(X3,xU))|~(sdtlseqdt0(sdtlpdtrp0(xf,X3),X3)))|(?[X5]:(aElementOf0(X5,xT)&~(sdtlseqdt0(X5,X3)))&~(aUpperBoundOfIn0(X3,xT,xU))))|aElementOf0(X3,xP))))&xP=cS1241(xU,xf,xT)),inference(variable_rename,[status(thm)],[168])).
% fof(170, plain,((aSet0(xP)&![X3]:((~(aElementOf0(X3,xP))|(((aElementOf0(X3,xU)&sdtlseqdt0(sdtlpdtrp0(xf,X3),X3))&![X4]:(~(aElementOf0(X4,xT))|sdtlseqdt0(X4,X3)))&aUpperBoundOfIn0(X3,xT,xU)))&(((~(aElementOf0(X3,xU))|~(sdtlseqdt0(sdtlpdtrp0(xf,X3),X3)))|((aElementOf0(esk12_1(X3),xT)&~(sdtlseqdt0(esk12_1(X3),X3)))&~(aUpperBoundOfIn0(X3,xT,xU))))|aElementOf0(X3,xP))))&xP=cS1241(xU,xf,xT)),inference(skolemize,[status(esa)],[169])).
% fof(171, plain,![X3]:![X4]:(((((((~(aElementOf0(X4,xT))|sdtlseqdt0(X4,X3))&(aElementOf0(X3,xU)&sdtlseqdt0(sdtlpdtrp0(xf,X3),X3)))&aUpperBoundOfIn0(X3,xT,xU))|~(aElementOf0(X3,xP)))&(((~(aElementOf0(X3,xU))|~(sdtlseqdt0(sdtlpdtrp0(xf,X3),X3)))|((aElementOf0(esk12_1(X3),xT)&~(sdtlseqdt0(esk12_1(X3),X3)))&~(aUpperBoundOfIn0(X3,xT,xU))))|aElementOf0(X3,xP)))&aSet0(xP))&xP=cS1241(xU,xf,xT)),inference(shift_quantors,[status(thm)],[170])).
% fof(172, plain,![X3]:![X4]:(((((((~(aElementOf0(X4,xT))|sdtlseqdt0(X4,X3))|~(aElementOf0(X3,xP)))&((aElementOf0(X3,xU)|~(aElementOf0(X3,xP)))&(sdtlseqdt0(sdtlpdtrp0(xf,X3),X3)|~(aElementOf0(X3,xP)))))&(aUpperBoundOfIn0(X3,xT,xU)|~(aElementOf0(X3,xP))))&((((aElementOf0(esk12_1(X3),xT)|(~(aElementOf0(X3,xU))|~(sdtlseqdt0(sdtlpdtrp0(xf,X3),X3))))|aElementOf0(X3,xP))&((~(sdtlseqdt0(esk12_1(X3),X3))|(~(aElementOf0(X3,xU))|~(sdtlseqdt0(sdtlpdtrp0(xf,X3),X3))))|aElementOf0(X3,xP)))&((~(aUpperBoundOfIn0(X3,xT,xU))|(~(aElementOf0(X3,xU))|~(sdtlseqdt0(sdtlpdtrp0(xf,X3),X3))))|aElementOf0(X3,xP))))&aSet0(xP))&xP=cS1241(xU,xf,xT)),inference(distribute,[status(thm)],[171])).
% cnf(174,plain,(aSet0(xP)),inference(split_conjunct,[status(thm)],[172])).
% cnf(180,plain,(aElementOf0(X1,xU)|~aElementOf0(X1,xP)),inference(split_conjunct,[status(thm)],[172])).
% fof(210, negated_conjecture,![X1]:(((~(aElementOf0(X1,xU))|((~(aElementOf0(X1,xU))|?[X2]:(aElementOf0(X2,xP)&~(sdtlseqdt0(X1,X2))))&~(aLowerBoundOfIn0(X1,xP,xU))))|?[X2]:(((aElementOf0(X2,xU)&![X3]:(~(aElementOf0(X3,xP))|sdtlseqdt0(X2,X3)))&aLowerBoundOfIn0(X2,xP,xU))&~(sdtlseqdt0(X2,X1))))&~(aInfimumOfIn0(X1,xP,xU))),inference(fof_nnf,[status(thm)],[29])).
% fof(211, negated_conjecture,![X4]:(((~(aElementOf0(X4,xU))|((~(aElementOf0(X4,xU))|?[X5]:(aElementOf0(X5,xP)&~(sdtlseqdt0(X4,X5))))&~(aLowerBoundOfIn0(X4,xP,xU))))|?[X6]:(((aElementOf0(X6,xU)&![X7]:(~(aElementOf0(X7,xP))|sdtlseqdt0(X6,X7)))&aLowerBoundOfIn0(X6,xP,xU))&~(sdtlseqdt0(X6,X4))))&~(aInfimumOfIn0(X4,xP,xU))),inference(variable_rename,[status(thm)],[210])).
% fof(212, negated_conjecture,![X4]:(((~(aElementOf0(X4,xU))|((~(aElementOf0(X4,xU))|(aElementOf0(esk14_1(X4),xP)&~(sdtlseqdt0(X4,esk14_1(X4)))))&~(aLowerBoundOfIn0(X4,xP,xU))))|(((aElementOf0(esk15_1(X4),xU)&![X7]:(~(aElementOf0(X7,xP))|sdtlseqdt0(esk15_1(X4),X7)))&aLowerBoundOfIn0(esk15_1(X4),xP,xU))&~(sdtlseqdt0(esk15_1(X4),X4))))&~(aInfimumOfIn0(X4,xP,xU))),inference(skolemize,[status(esa)],[211])).
% fof(213, negated_conjecture,![X4]:![X7]:((((((~(aElementOf0(X7,xP))|sdtlseqdt0(esk15_1(X4),X7))&aElementOf0(esk15_1(X4),xU))&aLowerBoundOfIn0(esk15_1(X4),xP,xU))&~(sdtlseqdt0(esk15_1(X4),X4)))|(~(aElementOf0(X4,xU))|((~(aElementOf0(X4,xU))|(aElementOf0(esk14_1(X4),xP)&~(sdtlseqdt0(X4,esk14_1(X4)))))&~(aLowerBoundOfIn0(X4,xP,xU)))))&~(aInfimumOfIn0(X4,xP,xU))),inference(shift_quantors,[status(thm)],[212])).
% fof(214, negated_conjecture,![X4]:![X7]:(((((((((aElementOf0(esk14_1(X4),xP)|~(aElementOf0(X4,xU)))|~(aElementOf0(X4,xU)))|(~(aElementOf0(X7,xP))|sdtlseqdt0(esk15_1(X4),X7)))&(((~(sdtlseqdt0(X4,esk14_1(X4)))|~(aElementOf0(X4,xU)))|~(aElementOf0(X4,xU)))|(~(aElementOf0(X7,xP))|sdtlseqdt0(esk15_1(X4),X7))))&((~(aLowerBoundOfIn0(X4,xP,xU))|~(aElementOf0(X4,xU)))|(~(aElementOf0(X7,xP))|sdtlseqdt0(esk15_1(X4),X7))))&(((((aElementOf0(esk14_1(X4),xP)|~(aElementOf0(X4,xU)))|~(aElementOf0(X4,xU)))|aElementOf0(esk15_1(X4),xU))&(((~(sdtlseqdt0(X4,esk14_1(X4)))|~(aElementOf0(X4,xU)))|~(aElementOf0(X4,xU)))|aElementOf0(esk15_1(X4),xU)))&((~(aLowerBoundOfIn0(X4,xP,xU))|~(aElementOf0(X4,xU)))|aElementOf0(esk15_1(X4),xU))))&(((((aElementOf0(esk14_1(X4),xP)|~(aElementOf0(X4,xU)))|~(aElementOf0(X4,xU)))|aLowerBoundOfIn0(esk15_1(X4),xP,xU))&(((~(sdtlseqdt0(X4,esk14_1(X4)))|~(aElementOf0(X4,xU)))|~(aElementOf0(X4,xU)))|aLowerBoundOfIn0(esk15_1(X4),xP,xU)))&((~(aLowerBoundOfIn0(X4,xP,xU))|~(aElementOf0(X4,xU)))|aLowerBoundOfIn0(esk15_1(X4),xP,xU))))&(((((aElementOf0(esk14_1(X4),xP)|~(aElementOf0(X4,xU)))|~(aElementOf0(X4,xU)))|~(sdtlseqdt0(esk15_1(X4),X4)))&(((~(sdtlseqdt0(X4,esk14_1(X4)))|~(aElementOf0(X4,xU)))|~(aElementOf0(X4,xU)))|~(sdtlseqdt0(esk15_1(X4),X4))))&((~(aLowerBoundOfIn0(X4,xP,xU))|~(aElementOf0(X4,xU)))|~(sdtlseqdt0(esk15_1(X4),X4)))))&~(aInfimumOfIn0(X4,xP,xU))),inference(distribute,[status(thm)],[213])).
% cnf(215,negated_conjecture,(~aInfimumOfIn0(X1,xP,xU)),inference(split_conjunct,[status(thm)],[214])).
% fof(228, plain,![X1]:(~(epred1_1(X1))|?[X2]:(((((aElementOf0(X2,xU)&![X3]:(~(aElementOf0(X3,X1))|sdtlseqdt0(X2,X3)))&aLowerBoundOfIn0(X2,X1,xU))&![X3]:(((~(aElementOf0(X3,xU))|?[X4]:(aElementOf0(X4,X1)&~(sdtlseqdt0(X3,X4))))&~(aLowerBoundOfIn0(X3,X1,xU)))|sdtlseqdt0(X3,X2)))&aInfimumOfIn0(X2,X1,xU))&?[X3]:((((aElementOf0(X3,xU)&![X4]:(~(aElementOf0(X4,X1))|sdtlseqdt0(X4,X3)))&aUpperBoundOfIn0(X3,X1,xU))&![X4]:(((~(aElementOf0(X4,xU))|?[X5]:(aElementOf0(X5,X1)&~(sdtlseqdt0(X5,X4))))&~(aUpperBoundOfIn0(X4,X1,xU)))|sdtlseqdt0(X3,X4)))&aSupremumOfIn0(X3,X1,xU)))),inference(fof_nnf,[status(thm)],[35])).
% fof(229, plain,![X6]:(~(epred1_1(X6))|?[X7]:(((((aElementOf0(X7,xU)&![X8]:(~(aElementOf0(X8,X6))|sdtlseqdt0(X7,X8)))&aLowerBoundOfIn0(X7,X6,xU))&![X9]:(((~(aElementOf0(X9,xU))|?[X10]:(aElementOf0(X10,X6)&~(sdtlseqdt0(X9,X10))))&~(aLowerBoundOfIn0(X9,X6,xU)))|sdtlseqdt0(X9,X7)))&aInfimumOfIn0(X7,X6,xU))&?[X11]:((((aElementOf0(X11,xU)&![X12]:(~(aElementOf0(X12,X6))|sdtlseqdt0(X12,X11)))&aUpperBoundOfIn0(X11,X6,xU))&![X13]:(((~(aElementOf0(X13,xU))|?[X14]:(aElementOf0(X14,X6)&~(sdtlseqdt0(X14,X13))))&~(aUpperBoundOfIn0(X13,X6,xU)))|sdtlseqdt0(X11,X13)))&aSupremumOfIn0(X11,X6,xU)))),inference(variable_rename,[status(thm)],[228])).
% fof(230, plain,![X6]:(~(epred1_1(X6))|(((((aElementOf0(esk16_1(X6),xU)&![X8]:(~(aElementOf0(X8,X6))|sdtlseqdt0(esk16_1(X6),X8)))&aLowerBoundOfIn0(esk16_1(X6),X6,xU))&![X9]:(((~(aElementOf0(X9,xU))|(aElementOf0(esk17_2(X6,X9),X6)&~(sdtlseqdt0(X9,esk17_2(X6,X9)))))&~(aLowerBoundOfIn0(X9,X6,xU)))|sdtlseqdt0(X9,esk16_1(X6))))&aInfimumOfIn0(esk16_1(X6),X6,xU))&((((aElementOf0(esk18_1(X6),xU)&![X12]:(~(aElementOf0(X12,X6))|sdtlseqdt0(X12,esk18_1(X6))))&aUpperBoundOfIn0(esk18_1(X6),X6,xU))&![X13]:(((~(aElementOf0(X13,xU))|(aElementOf0(esk19_2(X6,X13),X6)&~(sdtlseqdt0(esk19_2(X6,X13),X13))))&~(aUpperBoundOfIn0(X13,X6,xU)))|sdtlseqdt0(esk18_1(X6),X13)))&aSupremumOfIn0(esk18_1(X6),X6,xU)))),inference(skolemize,[status(esa)],[229])).
% fof(231, plain,![X6]:![X8]:![X9]:![X12]:![X13]:(((((((~(aElementOf0(X13,xU))|(aElementOf0(esk19_2(X6,X13),X6)&~(sdtlseqdt0(esk19_2(X6,X13),X13))))&~(aUpperBoundOfIn0(X13,X6,xU)))|sdtlseqdt0(esk18_1(X6),X13))&(((~(aElementOf0(X12,X6))|sdtlseqdt0(X12,esk18_1(X6)))&aElementOf0(esk18_1(X6),xU))&aUpperBoundOfIn0(esk18_1(X6),X6,xU)))&aSupremumOfIn0(esk18_1(X6),X6,xU))&(((((~(aElementOf0(X9,xU))|(aElementOf0(esk17_2(X6,X9),X6)&~(sdtlseqdt0(X9,esk17_2(X6,X9)))))&~(aLowerBoundOfIn0(X9,X6,xU)))|sdtlseqdt0(X9,esk16_1(X6)))&(((~(aElementOf0(X8,X6))|sdtlseqdt0(esk16_1(X6),X8))&aElementOf0(esk16_1(X6),xU))&aLowerBoundOfIn0(esk16_1(X6),X6,xU)))&aInfimumOfIn0(esk16_1(X6),X6,xU)))|~(epred1_1(X6))),inference(shift_quantors,[status(thm)],[230])).
% fof(232, plain,![X6]:![X8]:![X9]:![X12]:![X13]:((((((((aElementOf0(esk19_2(X6,X13),X6)|~(aElementOf0(X13,xU)))|sdtlseqdt0(esk18_1(X6),X13))|~(epred1_1(X6)))&(((~(sdtlseqdt0(esk19_2(X6,X13),X13))|~(aElementOf0(X13,xU)))|sdtlseqdt0(esk18_1(X6),X13))|~(epred1_1(X6))))&((~(aUpperBoundOfIn0(X13,X6,xU))|sdtlseqdt0(esk18_1(X6),X13))|~(epred1_1(X6))))&((((~(aElementOf0(X12,X6))|sdtlseqdt0(X12,esk18_1(X6)))|~(epred1_1(X6)))&(aElementOf0(esk18_1(X6),xU)|~(epred1_1(X6))))&(aUpperBoundOfIn0(esk18_1(X6),X6,xU)|~(epred1_1(X6)))))&(aSupremumOfIn0(esk18_1(X6),X6,xU)|~(epred1_1(X6))))&(((((((aElementOf0(esk17_2(X6,X9),X6)|~(aElementOf0(X9,xU)))|sdtlseqdt0(X9,esk16_1(X6)))|~(epred1_1(X6)))&(((~(sdtlseqdt0(X9,esk17_2(X6,X9)))|~(aElementOf0(X9,xU)))|sdtlseqdt0(X9,esk16_1(X6)))|~(epred1_1(X6))))&((~(aLowerBoundOfIn0(X9,X6,xU))|sdtlseqdt0(X9,esk16_1(X6)))|~(epred1_1(X6))))&((((~(aElementOf0(X8,X6))|sdtlseqdt0(esk16_1(X6),X8))|~(epred1_1(X6)))&(aElementOf0(esk16_1(X6),xU)|~(epred1_1(X6))))&(aLowerBoundOfIn0(esk16_1(X6),X6,xU)|~(epred1_1(X6)))))&(aInfimumOfIn0(esk16_1(X6),X6,xU)|~(epred1_1(X6))))),inference(distribute,[status(thm)],[231])).
% cnf(233,plain,(aInfimumOfIn0(esk16_1(X1),X1,xU)|~epred1_1(X1)),inference(split_conjunct,[status(thm)],[232])).
% cnf(293,plain,(aElementOf0(esk11_1(xP),xU)|epred1_1(xP)|~aSet0(xP)),inference(spm,[status(thm)],[180,149,theory(equality)])).
% cnf(300,plain,(aElementOf0(esk11_1(xP),xU)|epred1_1(xP)|$false),inference(rw,[status(thm)],[293,174,theory(equality)])).
% cnf(301,plain,(aElementOf0(esk11_1(xP),xU)|epred1_1(xP)),inference(cn,[status(thm)],[300,theory(equality)])).
% cnf(363,negated_conjecture,(~epred1_1(xP)),inference(spm,[status(thm)],[215,233,theory(equality)])).
% cnf(826,plain,(aElementOf0(esk11_1(xP),xU)),inference(sr,[status(thm)],[301,363,theory(equality)])).
% cnf(848,plain,(epred1_1(xP)|~aSet0(xP)),inference(spm,[status(thm)],[148,826,theory(equality)])).
% cnf(857,plain,(epred1_1(xP)|$false),inference(rw,[status(thm)],[848,174,theory(equality)])).
% cnf(858,plain,(epred1_1(xP)),inference(cn,[status(thm)],[857,theory(equality)])).
% cnf(859,plain,($false),inference(sr,[status(thm)],[858,363,theory(equality)])).
% cnf(860,plain,($false),859,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 138
% # ...of these trivial : 0
% # ...subsumed : 4
% # ...remaining for further processing: 134
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 0
% # Backward-rewritten : 0
% # Generated clauses : 292
% # ...of the previous two non-trivial : 266
% # Contextual simplify-reflections : 7
% # Paramodulations : 290
% # Factorizations : 0
% # Equation resolutions : 2
% # Current number of processed clauses: 134
% # Positive orientable unit clauses: 19
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 3
% # Non-unit-clauses : 112
% # Current number of unprocessed clauses: 234
% # ...number of literals in the above : 787
% # Clause-clause subsumption calls (NU) : 220
% # Rec. Clause-clause subsumption calls : 105
% # Unit Clause-clause subsumption calls : 47
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 0
% # Indexed BW rewrite successes : 0
% # Backwards rewriting index: 160 leaves, 1.29+/-0.847 terms/leaf
% # Paramod-from index: 44 leaves, 1.00+/-0.000 terms/leaf
% # Paramod-into index: 110 leaves, 1.22+/-0.693 terms/leaf
% # -------------------------------------------------
% # User time : 0.034 s
% # System time : 0.005 s
% # Total time : 0.039 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.14 CPU 0.21 WC
% FINAL PrfWatch: 0.14 CPU 0.21 WC
% SZS output end Solution for /tmp/SystemOnTPTP1898/LAT385+4.tptp
%
%------------------------------------------------------------------------------