%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : NUM556+1 : TPTP v5.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %s
% Computer : art11.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 3.00GHz @ 3000MHz
% Memory : 2006MB
% OS : Linux 2.6.31.5-127.fc12.i686.PAE
% CPULimit : 300s
% DateTime : Wed Dec 29 20:09:54 EST 2010
% Result : Theorem 23.70s
% Output : Solution 23.70s
% 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/SystemOnTPTP15331/NUM556+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP15331/NUM556+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP15331/NUM556+1.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 15463
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.02 WC
% PrfWatch: 1.94 CPU 2.03 WC
% PrfWatch: 3.93 CPU 4.03 WC
% PrfWatch: 5.92 CPU 6.04 WC
% PrfWatch: 7.75 CPU 8.05 WC
% PrfWatch: 9.59 CPU 10.05 WC
% PrfWatch: 11.58 CPU 12.06 WC
% PrfWatch: 13.57 CPU 14.07 WC
% PrfWatch: 15.57 CPU 16.07 WC
% # Preprocessing time : 0.023 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% PrfWatch: 17.58 CPU 18.08 WC
% PrfWatch: 19.56 CPU 20.09 WC
% PrfWatch: 21.56 CPU 22.09 WC
% # SZS output start CNFRefutation.
% fof(1, axiom,![X1]:(aSet0(X1)=>![X2]:(aElementOf0(X2,X1)=>aElement0(X2))),file('/tmp/SRASS.s.p', mEOfElem)).
% fof(4, axiom,![X1]:(aSet0(X1)=>![X2]:(aSubsetOf0(X2,X1)<=>(aSet0(X2)&![X3]:(aElementOf0(X3,X2)=>aElementOf0(X3,X1))))),file('/tmp/SRASS.s.p', mDefSub)).
% fof(9, axiom,![X1]:![X2]:((aSet0(X1)&aElement0(X2))=>![X3]:(X3=sdtpldt0(X1,X2)<=>(aSet0(X3)&![X4]:(aElementOf0(X4,X3)<=>(aElement0(X4)&(aElementOf0(X4,X1)|X4=X2)))))),file('/tmp/SRASS.s.p', mDefCons)).
% fof(10, axiom,![X1]:![X2]:((aSet0(X1)&aElement0(X2))=>![X3]:(X3=sdtmndt0(X1,X2)<=>(aSet0(X3)&![X4]:(aElementOf0(X4,X3)<=>((aElement0(X4)&aElementOf0(X4,X1))&~(X4=X2)))))),file('/tmp/SRASS.s.p', mDefDiff)).
% fof(12, axiom,![X1]:![X2]:((aElement0(X1)&aSet0(X2))=>(~(aElementOf0(X1,X2))=>sdtmndt0(sdtpldt0(X2,X1),X1)=X2)),file('/tmp/SRASS.s.p', mDiffCons)).
% fof(13, axiom,![X1]:(aElement0(X1)=>![X2]:((aSet0(X2)&isFinite0(X2))=>isFinite0(sdtpldt0(X2,X1)))),file('/tmp/SRASS.s.p', mFConsSet)).
% fof(14, axiom,![X1]:(aElement0(X1)=>![X2]:((aSet0(X2)&isFinite0(X2))=>isFinite0(sdtmndt0(X2,X1)))),file('/tmp/SRASS.s.p', mFDiffSet)).
% fof(24, axiom,![X1]:(aSet0(X1)=>![X2]:((isFinite0(X1)&aElementOf0(X2,X1))=>szszuzczcdt0(sbrdtbr0(sdtmndt0(X1,X2)))=sbrdtbr0(X1))),file('/tmp/SRASS.s.p', mCardDiff)).
% fof(25, axiom,![X1]:![X2]:((aSet0(X1)&aElementOf0(X2,szNzAzT0))=>![X3]:(X3=slbdtsldtrb0(X1,X2)<=>(aSet0(X3)&![X4]:(aElementOf0(X4,X3)<=>(aSubsetOf0(X4,X1)&sbrdtbr0(X4)=X2))))),file('/tmp/SRASS.s.p', mDefSel)).
% fof(28, axiom,aElementOf0(xk,szNzAzT0),file('/tmp/SRASS.s.p', m__2202)).
% fof(29, axiom,((aSet0(xS)&aSet0(xT))&~(xk=sz00)),file('/tmp/SRASS.s.p', m__2202_02)).
% fof(31, axiom,aElementOf0(xx,xS),file('/tmp/SRASS.s.p', m__2256)).
% fof(32, axiom,aElementOf0(xQ,slbdtsldtrb0(xS,xk)),file('/tmp/SRASS.s.p', m__2270)).
% fof(33, axiom,((aSet0(xQ)&isFinite0(xQ))&sbrdtbr0(xQ)=xk),file('/tmp/SRASS.s.p', m__2291)).
% fof(34, axiom,(aElement0(xy)&aElementOf0(xy,xQ)),file('/tmp/SRASS.s.p', m__2304)).
% fof(37, axiom,xP=sdtpldt0(sdtmndt0(xQ,xy),xx),file('/tmp/SRASS.s.p', m__2357)).
% fof(38, axiom,(~(aElementOf0(xx,sdtmndt0(xQ,xy)))&szszuzczcdt0(sbrdtbr0(sdtmndt0(xQ,xy)))=xk),file('/tmp/SRASS.s.p', m__2411)).
% fof(72, conjecture,(aSubsetOf0(xP,xS)&sbrdtbr0(xP)=xk),file('/tmp/SRASS.s.p', m__)).
% fof(73, negated_conjecture,~((aSubsetOf0(xP,xS)&sbrdtbr0(xP)=xk)),inference(assume_negation,[status(cth)],[72])).
% fof(74, plain,![X1]:![X2]:((aElement0(X1)&aSet0(X2))=>(~(aElementOf0(X1,X2))=>sdtmndt0(sdtpldt0(X2,X1),X1)=X2)),inference(fof_simplification,[status(thm)],[12,theory(equality)])).
% fof(79, plain,(~(aElementOf0(xx,sdtmndt0(xQ,xy)))&szszuzczcdt0(sbrdtbr0(sdtmndt0(xQ,xy)))=xk),inference(fof_simplification,[status(thm)],[38,theory(equality)])).
% fof(88, plain,![X1]:(~(aSet0(X1))|![X2]:(~(aElementOf0(X2,X1))|aElement0(X2))),inference(fof_nnf,[status(thm)],[1])).
% fof(89, plain,![X3]:(~(aSet0(X3))|![X4]:(~(aElementOf0(X4,X3))|aElement0(X4))),inference(variable_rename,[status(thm)],[88])).
% fof(90, plain,![X3]:![X4]:((~(aElementOf0(X4,X3))|aElement0(X4))|~(aSet0(X3))),inference(shift_quantors,[status(thm)],[89])).
% cnf(91,plain,(aElement0(X2)|~aSet0(X1)|~aElementOf0(X2,X1)),inference(split_conjunct,[status(thm)],[90])).
% fof(101, plain,![X1]:(~(aSet0(X1))|![X2]:((~(aSubsetOf0(X2,X1))|(aSet0(X2)&![X3]:(~(aElementOf0(X3,X2))|aElementOf0(X3,X1))))&((~(aSet0(X2))|?[X3]:(aElementOf0(X3,X2)&~(aElementOf0(X3,X1))))|aSubsetOf0(X2,X1)))),inference(fof_nnf,[status(thm)],[4])).
% fof(102, plain,![X4]:(~(aSet0(X4))|![X5]:((~(aSubsetOf0(X5,X4))|(aSet0(X5)&![X6]:(~(aElementOf0(X6,X5))|aElementOf0(X6,X4))))&((~(aSet0(X5))|?[X7]:(aElementOf0(X7,X5)&~(aElementOf0(X7,X4))))|aSubsetOf0(X5,X4)))),inference(variable_rename,[status(thm)],[101])).
% fof(103, plain,![X4]:(~(aSet0(X4))|![X5]:((~(aSubsetOf0(X5,X4))|(aSet0(X5)&![X6]:(~(aElementOf0(X6,X5))|aElementOf0(X6,X4))))&((~(aSet0(X5))|(aElementOf0(esk2_2(X4,X5),X5)&~(aElementOf0(esk2_2(X4,X5),X4))))|aSubsetOf0(X5,X4)))),inference(skolemize,[status(esa)],[102])).
% fof(104, plain,![X4]:![X5]:![X6]:(((((~(aElementOf0(X6,X5))|aElementOf0(X6,X4))&aSet0(X5))|~(aSubsetOf0(X5,X4)))&((~(aSet0(X5))|(aElementOf0(esk2_2(X4,X5),X5)&~(aElementOf0(esk2_2(X4,X5),X4))))|aSubsetOf0(X5,X4)))|~(aSet0(X4))),inference(shift_quantors,[status(thm)],[103])).
% fof(105, plain,![X4]:![X5]:![X6]:(((((~(aElementOf0(X6,X5))|aElementOf0(X6,X4))|~(aSubsetOf0(X5,X4)))|~(aSet0(X4)))&((aSet0(X5)|~(aSubsetOf0(X5,X4)))|~(aSet0(X4))))&((((aElementOf0(esk2_2(X4,X5),X5)|~(aSet0(X5)))|aSubsetOf0(X5,X4))|~(aSet0(X4)))&(((~(aElementOf0(esk2_2(X4,X5),X4))|~(aSet0(X5)))|aSubsetOf0(X5,X4))|~(aSet0(X4))))),inference(distribute,[status(thm)],[104])).
% cnf(106,plain,(aSubsetOf0(X2,X1)|~aSet0(X1)|~aSet0(X2)|~aElementOf0(esk2_2(X1,X2),X1)),inference(split_conjunct,[status(thm)],[105])).
% cnf(107,plain,(aSubsetOf0(X2,X1)|aElementOf0(esk2_2(X1,X2),X2)|~aSet0(X1)|~aSet0(X2)),inference(split_conjunct,[status(thm)],[105])).
% cnf(109,plain,(aElementOf0(X3,X1)|~aSet0(X1)|~aSubsetOf0(X2,X1)|~aElementOf0(X3,X2)),inference(split_conjunct,[status(thm)],[105])).
% fof(123, plain,![X1]:![X2]:((~(aSet0(X1))|~(aElement0(X2)))|![X3]:((~(X3=sdtpldt0(X1,X2))|(aSet0(X3)&![X4]:((~(aElementOf0(X4,X3))|(aElement0(X4)&(aElementOf0(X4,X1)|X4=X2)))&((~(aElement0(X4))|(~(aElementOf0(X4,X1))&~(X4=X2)))|aElementOf0(X4,X3)))))&((~(aSet0(X3))|?[X4]:((~(aElementOf0(X4,X3))|(~(aElement0(X4))|(~(aElementOf0(X4,X1))&~(X4=X2))))&(aElementOf0(X4,X3)|(aElement0(X4)&(aElementOf0(X4,X1)|X4=X2)))))|X3=sdtpldt0(X1,X2)))),inference(fof_nnf,[status(thm)],[9])).
% fof(124, plain,![X5]:![X6]:((~(aSet0(X5))|~(aElement0(X6)))|![X7]:((~(X7=sdtpldt0(X5,X6))|(aSet0(X7)&![X8]:((~(aElementOf0(X8,X7))|(aElement0(X8)&(aElementOf0(X8,X5)|X8=X6)))&((~(aElement0(X8))|(~(aElementOf0(X8,X5))&~(X8=X6)))|aElementOf0(X8,X7)))))&((~(aSet0(X7))|?[X9]:((~(aElementOf0(X9,X7))|(~(aElement0(X9))|(~(aElementOf0(X9,X5))&~(X9=X6))))&(aElementOf0(X9,X7)|(aElement0(X9)&(aElementOf0(X9,X5)|X9=X6)))))|X7=sdtpldt0(X5,X6)))),inference(variable_rename,[status(thm)],[123])).
% fof(125, plain,![X5]:![X6]:((~(aSet0(X5))|~(aElement0(X6)))|![X7]:((~(X7=sdtpldt0(X5,X6))|(aSet0(X7)&![X8]:((~(aElementOf0(X8,X7))|(aElement0(X8)&(aElementOf0(X8,X5)|X8=X6)))&((~(aElement0(X8))|(~(aElementOf0(X8,X5))&~(X8=X6)))|aElementOf0(X8,X7)))))&((~(aSet0(X7))|((~(aElementOf0(esk3_3(X5,X6,X7),X7))|(~(aElement0(esk3_3(X5,X6,X7)))|(~(aElementOf0(esk3_3(X5,X6,X7),X5))&~(esk3_3(X5,X6,X7)=X6))))&(aElementOf0(esk3_3(X5,X6,X7),X7)|(aElement0(esk3_3(X5,X6,X7))&(aElementOf0(esk3_3(X5,X6,X7),X5)|esk3_3(X5,X6,X7)=X6)))))|X7=sdtpldt0(X5,X6)))),inference(skolemize,[status(esa)],[124])).
% fof(126, plain,![X5]:![X6]:![X7]:![X8]:((((((~(aElementOf0(X8,X7))|(aElement0(X8)&(aElementOf0(X8,X5)|X8=X6)))&((~(aElement0(X8))|(~(aElementOf0(X8,X5))&~(X8=X6)))|aElementOf0(X8,X7)))&aSet0(X7))|~(X7=sdtpldt0(X5,X6)))&((~(aSet0(X7))|((~(aElementOf0(esk3_3(X5,X6,X7),X7))|(~(aElement0(esk3_3(X5,X6,X7)))|(~(aElementOf0(esk3_3(X5,X6,X7),X5))&~(esk3_3(X5,X6,X7)=X6))))&(aElementOf0(esk3_3(X5,X6,X7),X7)|(aElement0(esk3_3(X5,X6,X7))&(aElementOf0(esk3_3(X5,X6,X7),X5)|esk3_3(X5,X6,X7)=X6)))))|X7=sdtpldt0(X5,X6)))|(~(aSet0(X5))|~(aElement0(X6)))),inference(shift_quantors,[status(thm)],[125])).
% fof(127, plain,![X5]:![X6]:![X7]:![X8]:(((((((aElement0(X8)|~(aElementOf0(X8,X7)))|~(X7=sdtpldt0(X5,X6)))|(~(aSet0(X5))|~(aElement0(X6))))&((((aElementOf0(X8,X5)|X8=X6)|~(aElementOf0(X8,X7)))|~(X7=sdtpldt0(X5,X6)))|(~(aSet0(X5))|~(aElement0(X6)))))&(((((~(aElementOf0(X8,X5))|~(aElement0(X8)))|aElementOf0(X8,X7))|~(X7=sdtpldt0(X5,X6)))|(~(aSet0(X5))|~(aElement0(X6))))&((((~(X8=X6)|~(aElement0(X8)))|aElementOf0(X8,X7))|~(X7=sdtpldt0(X5,X6)))|(~(aSet0(X5))|~(aElement0(X6))))))&((aSet0(X7)|~(X7=sdtpldt0(X5,X6)))|(~(aSet0(X5))|~(aElement0(X6)))))&(((((((~(aElementOf0(esk3_3(X5,X6,X7),X5))|~(aElement0(esk3_3(X5,X6,X7))))|~(aElementOf0(esk3_3(X5,X6,X7),X7)))|~(aSet0(X7)))|X7=sdtpldt0(X5,X6))|(~(aSet0(X5))|~(aElement0(X6))))&(((((~(esk3_3(X5,X6,X7)=X6)|~(aElement0(esk3_3(X5,X6,X7))))|~(aElementOf0(esk3_3(X5,X6,X7),X7)))|~(aSet0(X7)))|X7=sdtpldt0(X5,X6))|(~(aSet0(X5))|~(aElement0(X6)))))&(((((aElement0(esk3_3(X5,X6,X7))|aElementOf0(esk3_3(X5,X6,X7),X7))|~(aSet0(X7)))|X7=sdtpldt0(X5,X6))|(~(aSet0(X5))|~(aElement0(X6))))&(((((aElementOf0(esk3_3(X5,X6,X7),X5)|esk3_3(X5,X6,X7)=X6)|aElementOf0(esk3_3(X5,X6,X7),X7))|~(aSet0(X7)))|X7=sdtpldt0(X5,X6))|(~(aSet0(X5))|~(aElement0(X6))))))),inference(distribute,[status(thm)],[126])).
% cnf(132,plain,(aSet0(X3)|~aElement0(X1)|~aSet0(X2)|X3!=sdtpldt0(X2,X1)),inference(split_conjunct,[status(thm)],[127])).
% cnf(133,plain,(aElementOf0(X4,X3)|~aElement0(X1)|~aSet0(X2)|X3!=sdtpldt0(X2,X1)|~aElement0(X4)|X4!=X1),inference(split_conjunct,[status(thm)],[127])).
% cnf(135,plain,(X4=X1|aElementOf0(X4,X2)|~aElement0(X1)|~aSet0(X2)|X3!=sdtpldt0(X2,X1)|~aElementOf0(X4,X3)),inference(split_conjunct,[status(thm)],[127])).
% fof(137, plain,![X1]:![X2]:((~(aSet0(X1))|~(aElement0(X2)))|![X3]:((~(X3=sdtmndt0(X1,X2))|(aSet0(X3)&![X4]:((~(aElementOf0(X4,X3))|((aElement0(X4)&aElementOf0(X4,X1))&~(X4=X2)))&(((~(aElement0(X4))|~(aElementOf0(X4,X1)))|X4=X2)|aElementOf0(X4,X3)))))&((~(aSet0(X3))|?[X4]:((~(aElementOf0(X4,X3))|((~(aElement0(X4))|~(aElementOf0(X4,X1)))|X4=X2))&(aElementOf0(X4,X3)|((aElement0(X4)&aElementOf0(X4,X1))&~(X4=X2)))))|X3=sdtmndt0(X1,X2)))),inference(fof_nnf,[status(thm)],[10])).
% fof(138, plain,![X5]:![X6]:((~(aSet0(X5))|~(aElement0(X6)))|![X7]:((~(X7=sdtmndt0(X5,X6))|(aSet0(X7)&![X8]:((~(aElementOf0(X8,X7))|((aElement0(X8)&aElementOf0(X8,X5))&~(X8=X6)))&(((~(aElement0(X8))|~(aElementOf0(X8,X5)))|X8=X6)|aElementOf0(X8,X7)))))&((~(aSet0(X7))|?[X9]:((~(aElementOf0(X9,X7))|((~(aElement0(X9))|~(aElementOf0(X9,X5)))|X9=X6))&(aElementOf0(X9,X7)|((aElement0(X9)&aElementOf0(X9,X5))&~(X9=X6)))))|X7=sdtmndt0(X5,X6)))),inference(variable_rename,[status(thm)],[137])).
% fof(139, plain,![X5]:![X6]:((~(aSet0(X5))|~(aElement0(X6)))|![X7]:((~(X7=sdtmndt0(X5,X6))|(aSet0(X7)&![X8]:((~(aElementOf0(X8,X7))|((aElement0(X8)&aElementOf0(X8,X5))&~(X8=X6)))&(((~(aElement0(X8))|~(aElementOf0(X8,X5)))|X8=X6)|aElementOf0(X8,X7)))))&((~(aSet0(X7))|((~(aElementOf0(esk4_3(X5,X6,X7),X7))|((~(aElement0(esk4_3(X5,X6,X7)))|~(aElementOf0(esk4_3(X5,X6,X7),X5)))|esk4_3(X5,X6,X7)=X6))&(aElementOf0(esk4_3(X5,X6,X7),X7)|((aElement0(esk4_3(X5,X6,X7))&aElementOf0(esk4_3(X5,X6,X7),X5))&~(esk4_3(X5,X6,X7)=X6)))))|X7=sdtmndt0(X5,X6)))),inference(skolemize,[status(esa)],[138])).
% fof(140, plain,![X5]:![X6]:![X7]:![X8]:((((((~(aElementOf0(X8,X7))|((aElement0(X8)&aElementOf0(X8,X5))&~(X8=X6)))&(((~(aElement0(X8))|~(aElementOf0(X8,X5)))|X8=X6)|aElementOf0(X8,X7)))&aSet0(X7))|~(X7=sdtmndt0(X5,X6)))&((~(aSet0(X7))|((~(aElementOf0(esk4_3(X5,X6,X7),X7))|((~(aElement0(esk4_3(X5,X6,X7)))|~(aElementOf0(esk4_3(X5,X6,X7),X5)))|esk4_3(X5,X6,X7)=X6))&(aElementOf0(esk4_3(X5,X6,X7),X7)|((aElement0(esk4_3(X5,X6,X7))&aElementOf0(esk4_3(X5,X6,X7),X5))&~(esk4_3(X5,X6,X7)=X6)))))|X7=sdtmndt0(X5,X6)))|(~(aSet0(X5))|~(aElement0(X6)))),inference(shift_quantors,[status(thm)],[139])).
% fof(141, plain,![X5]:![X6]:![X7]:![X8]:((((((((aElement0(X8)|~(aElementOf0(X8,X7)))|~(X7=sdtmndt0(X5,X6)))|(~(aSet0(X5))|~(aElement0(X6))))&(((aElementOf0(X8,X5)|~(aElementOf0(X8,X7)))|~(X7=sdtmndt0(X5,X6)))|(~(aSet0(X5))|~(aElement0(X6)))))&(((~(X8=X6)|~(aElementOf0(X8,X7)))|~(X7=sdtmndt0(X5,X6)))|(~(aSet0(X5))|~(aElement0(X6)))))&(((((~(aElement0(X8))|~(aElementOf0(X8,X5)))|X8=X6)|aElementOf0(X8,X7))|~(X7=sdtmndt0(X5,X6)))|(~(aSet0(X5))|~(aElement0(X6)))))&((aSet0(X7)|~(X7=sdtmndt0(X5,X6)))|(~(aSet0(X5))|~(aElement0(X6)))))&(((((~(aElementOf0(esk4_3(X5,X6,X7),X7))|((~(aElement0(esk4_3(X5,X6,X7)))|~(aElementOf0(esk4_3(X5,X6,X7),X5)))|esk4_3(X5,X6,X7)=X6))|~(aSet0(X7)))|X7=sdtmndt0(X5,X6))|(~(aSet0(X5))|~(aElement0(X6))))&((((((aElement0(esk4_3(X5,X6,X7))|aElementOf0(esk4_3(X5,X6,X7),X7))|~(aSet0(X7)))|X7=sdtmndt0(X5,X6))|(~(aSet0(X5))|~(aElement0(X6))))&((((aElementOf0(esk4_3(X5,X6,X7),X5)|aElementOf0(esk4_3(X5,X6,X7),X7))|~(aSet0(X7)))|X7=sdtmndt0(X5,X6))|(~(aSet0(X5))|~(aElement0(X6)))))&((((~(esk4_3(X5,X6,X7)=X6)|aElementOf0(esk4_3(X5,X6,X7),X7))|~(aSet0(X7)))|X7=sdtmndt0(X5,X6))|(~(aSet0(X5))|~(aElement0(X6))))))),inference(distribute,[status(thm)],[140])).
% cnf(146,plain,(aSet0(X3)|~aElement0(X1)|~aSet0(X2)|X3!=sdtmndt0(X2,X1)),inference(split_conjunct,[status(thm)],[141])).
% cnf(149,plain,(aElementOf0(X4,X2)|~aElement0(X1)|~aSet0(X2)|X3!=sdtmndt0(X2,X1)|~aElementOf0(X4,X3)),inference(split_conjunct,[status(thm)],[141])).
% fof(155, plain,![X1]:![X2]:((~(aElement0(X1))|~(aSet0(X2)))|(aElementOf0(X1,X2)|sdtmndt0(sdtpldt0(X2,X1),X1)=X2)),inference(fof_nnf,[status(thm)],[74])).
% fof(156, plain,![X3]:![X4]:((~(aElement0(X3))|~(aSet0(X4)))|(aElementOf0(X3,X4)|sdtmndt0(sdtpldt0(X4,X3),X3)=X4)),inference(variable_rename,[status(thm)],[155])).
% cnf(157,plain,(sdtmndt0(sdtpldt0(X1,X2),X2)=X1|aElementOf0(X2,X1)|~aSet0(X1)|~aElement0(X2)),inference(split_conjunct,[status(thm)],[156])).
% fof(158, plain,![X1]:(~(aElement0(X1))|![X2]:((~(aSet0(X2))|~(isFinite0(X2)))|isFinite0(sdtpldt0(X2,X1)))),inference(fof_nnf,[status(thm)],[13])).
% fof(159, plain,![X3]:(~(aElement0(X3))|![X4]:((~(aSet0(X4))|~(isFinite0(X4)))|isFinite0(sdtpldt0(X4,X3)))),inference(variable_rename,[status(thm)],[158])).
% fof(160, plain,![X3]:![X4]:(((~(aSet0(X4))|~(isFinite0(X4)))|isFinite0(sdtpldt0(X4,X3)))|~(aElement0(X3))),inference(shift_quantors,[status(thm)],[159])).
% cnf(161,plain,(isFinite0(sdtpldt0(X2,X1))|~aElement0(X1)|~isFinite0(X2)|~aSet0(X2)),inference(split_conjunct,[status(thm)],[160])).
% fof(162, plain,![X1]:(~(aElement0(X1))|![X2]:((~(aSet0(X2))|~(isFinite0(X2)))|isFinite0(sdtmndt0(X2,X1)))),inference(fof_nnf,[status(thm)],[14])).
% fof(163, plain,![X3]:(~(aElement0(X3))|![X4]:((~(aSet0(X4))|~(isFinite0(X4)))|isFinite0(sdtmndt0(X4,X3)))),inference(variable_rename,[status(thm)],[162])).
% fof(164, plain,![X3]:![X4]:(((~(aSet0(X4))|~(isFinite0(X4)))|isFinite0(sdtmndt0(X4,X3)))|~(aElement0(X3))),inference(shift_quantors,[status(thm)],[163])).
% cnf(165,plain,(isFinite0(sdtmndt0(X2,X1))|~aElement0(X1)|~isFinite0(X2)|~aSet0(X2)),inference(split_conjunct,[status(thm)],[164])).
% fof(201, plain,![X1]:(~(aSet0(X1))|![X2]:((~(isFinite0(X1))|~(aElementOf0(X2,X1)))|szszuzczcdt0(sbrdtbr0(sdtmndt0(X1,X2)))=sbrdtbr0(X1))),inference(fof_nnf,[status(thm)],[24])).
% fof(202, plain,![X3]:(~(aSet0(X3))|![X4]:((~(isFinite0(X3))|~(aElementOf0(X4,X3)))|szszuzczcdt0(sbrdtbr0(sdtmndt0(X3,X4)))=sbrdtbr0(X3))),inference(variable_rename,[status(thm)],[201])).
% fof(203, plain,![X3]:![X4]:(((~(isFinite0(X3))|~(aElementOf0(X4,X3)))|szszuzczcdt0(sbrdtbr0(sdtmndt0(X3,X4)))=sbrdtbr0(X3))|~(aSet0(X3))),inference(shift_quantors,[status(thm)],[202])).
% cnf(204,plain,(szszuzczcdt0(sbrdtbr0(sdtmndt0(X1,X2)))=sbrdtbr0(X1)|~aSet0(X1)|~aElementOf0(X2,X1)|~isFinite0(X1)),inference(split_conjunct,[status(thm)],[203])).
% fof(205, plain,![X1]:![X2]:((~(aSet0(X1))|~(aElementOf0(X2,szNzAzT0)))|![X3]:((~(X3=slbdtsldtrb0(X1,X2))|(aSet0(X3)&![X4]:((~(aElementOf0(X4,X3))|(aSubsetOf0(X4,X1)&sbrdtbr0(X4)=X2))&((~(aSubsetOf0(X4,X1))|~(sbrdtbr0(X4)=X2))|aElementOf0(X4,X3)))))&((~(aSet0(X3))|?[X4]:((~(aElementOf0(X4,X3))|(~(aSubsetOf0(X4,X1))|~(sbrdtbr0(X4)=X2)))&(aElementOf0(X4,X3)|(aSubsetOf0(X4,X1)&sbrdtbr0(X4)=X2))))|X3=slbdtsldtrb0(X1,X2)))),inference(fof_nnf,[status(thm)],[25])).
% fof(206, plain,![X5]:![X6]:((~(aSet0(X5))|~(aElementOf0(X6,szNzAzT0)))|![X7]:((~(X7=slbdtsldtrb0(X5,X6))|(aSet0(X7)&![X8]:((~(aElementOf0(X8,X7))|(aSubsetOf0(X8,X5)&sbrdtbr0(X8)=X6))&((~(aSubsetOf0(X8,X5))|~(sbrdtbr0(X8)=X6))|aElementOf0(X8,X7)))))&((~(aSet0(X7))|?[X9]:((~(aElementOf0(X9,X7))|(~(aSubsetOf0(X9,X5))|~(sbrdtbr0(X9)=X6)))&(aElementOf0(X9,X7)|(aSubsetOf0(X9,X5)&sbrdtbr0(X9)=X6))))|X7=slbdtsldtrb0(X5,X6)))),inference(variable_rename,[status(thm)],[205])).
% fof(207, plain,![X5]:![X6]:((~(aSet0(X5))|~(aElementOf0(X6,szNzAzT0)))|![X7]:((~(X7=slbdtsldtrb0(X5,X6))|(aSet0(X7)&![X8]:((~(aElementOf0(X8,X7))|(aSubsetOf0(X8,X5)&sbrdtbr0(X8)=X6))&((~(aSubsetOf0(X8,X5))|~(sbrdtbr0(X8)=X6))|aElementOf0(X8,X7)))))&((~(aSet0(X7))|((~(aElementOf0(esk6_3(X5,X6,X7),X7))|(~(aSubsetOf0(esk6_3(X5,X6,X7),X5))|~(sbrdtbr0(esk6_3(X5,X6,X7))=X6)))&(aElementOf0(esk6_3(X5,X6,X7),X7)|(aSubsetOf0(esk6_3(X5,X6,X7),X5)&sbrdtbr0(esk6_3(X5,X6,X7))=X6))))|X7=slbdtsldtrb0(X5,X6)))),inference(skolemize,[status(esa)],[206])).
% fof(208, plain,![X5]:![X6]:![X7]:![X8]:((((((~(aElementOf0(X8,X7))|(aSubsetOf0(X8,X5)&sbrdtbr0(X8)=X6))&((~(aSubsetOf0(X8,X5))|~(sbrdtbr0(X8)=X6))|aElementOf0(X8,X7)))&aSet0(X7))|~(X7=slbdtsldtrb0(X5,X6)))&((~(aSet0(X7))|((~(aElementOf0(esk6_3(X5,X6,X7),X7))|(~(aSubsetOf0(esk6_3(X5,X6,X7),X5))|~(sbrdtbr0(esk6_3(X5,X6,X7))=X6)))&(aElementOf0(esk6_3(X5,X6,X7),X7)|(aSubsetOf0(esk6_3(X5,X6,X7),X5)&sbrdtbr0(esk6_3(X5,X6,X7))=X6))))|X7=slbdtsldtrb0(X5,X6)))|(~(aSet0(X5))|~(aElementOf0(X6,szNzAzT0)))),inference(shift_quantors,[status(thm)],[207])).
% fof(209, plain,![X5]:![X6]:![X7]:![X8]:(((((((aSubsetOf0(X8,X5)|~(aElementOf0(X8,X7)))|~(X7=slbdtsldtrb0(X5,X6)))|(~(aSet0(X5))|~(aElementOf0(X6,szNzAzT0))))&(((sbrdtbr0(X8)=X6|~(aElementOf0(X8,X7)))|~(X7=slbdtsldtrb0(X5,X6)))|(~(aSet0(X5))|~(aElementOf0(X6,szNzAzT0)))))&((((~(aSubsetOf0(X8,X5))|~(sbrdtbr0(X8)=X6))|aElementOf0(X8,X7))|~(X7=slbdtsldtrb0(X5,X6)))|(~(aSet0(X5))|~(aElementOf0(X6,szNzAzT0)))))&((aSet0(X7)|~(X7=slbdtsldtrb0(X5,X6)))|(~(aSet0(X5))|~(aElementOf0(X6,szNzAzT0)))))&(((((~(aElementOf0(esk6_3(X5,X6,X7),X7))|(~(aSubsetOf0(esk6_3(X5,X6,X7),X5))|~(sbrdtbr0(esk6_3(X5,X6,X7))=X6)))|~(aSet0(X7)))|X7=slbdtsldtrb0(X5,X6))|(~(aSet0(X5))|~(aElementOf0(X6,szNzAzT0))))&(((((aSubsetOf0(esk6_3(X5,X6,X7),X5)|aElementOf0(esk6_3(X5,X6,X7),X7))|~(aSet0(X7)))|X7=slbdtsldtrb0(X5,X6))|(~(aSet0(X5))|~(aElementOf0(X6,szNzAzT0))))&((((sbrdtbr0(esk6_3(X5,X6,X7))=X6|aElementOf0(esk6_3(X5,X6,X7),X7))|~(aSet0(X7)))|X7=slbdtsldtrb0(X5,X6))|(~(aSet0(X5))|~(aElementOf0(X6,szNzAzT0))))))),inference(distribute,[status(thm)],[208])).
% cnf(216,plain,(aSubsetOf0(X4,X2)|~aElementOf0(X1,szNzAzT0)|~aSet0(X2)|X3!=slbdtsldtrb0(X2,X1)|~aElementOf0(X4,X3)),inference(split_conjunct,[status(thm)],[209])).
% cnf(225,plain,(aElementOf0(xk,szNzAzT0)),inference(split_conjunct,[status(thm)],[28])).
% cnf(228,plain,(aSet0(xS)),inference(split_conjunct,[status(thm)],[29])).
% cnf(231,plain,(aElementOf0(xx,xS)),inference(split_conjunct,[status(thm)],[31])).
% cnf(232,plain,(aElementOf0(xQ,slbdtsldtrb0(xS,xk))),inference(split_conjunct,[status(thm)],[32])).
% cnf(234,plain,(isFinite0(xQ)),inference(split_conjunct,[status(thm)],[33])).
% cnf(235,plain,(aSet0(xQ)),inference(split_conjunct,[status(thm)],[33])).
% cnf(237,plain,(aElement0(xy)),inference(split_conjunct,[status(thm)],[34])).
% cnf(240,plain,(xP=sdtpldt0(sdtmndt0(xQ,xy),xx)),inference(split_conjunct,[status(thm)],[37])).
% cnf(241,plain,(szszuzczcdt0(sbrdtbr0(sdtmndt0(xQ,xy)))=xk),inference(split_conjunct,[status(thm)],[79])).
% cnf(242,plain,(~aElementOf0(xx,sdtmndt0(xQ,xy))),inference(split_conjunct,[status(thm)],[79])).
% fof(371, negated_conjecture,(~(aSubsetOf0(xP,xS))|~(sbrdtbr0(xP)=xk)),inference(fof_nnf,[status(thm)],[73])).
% cnf(372,negated_conjecture,(sbrdtbr0(xP)!=xk|~aSubsetOf0(xP,xS)),inference(split_conjunct,[status(thm)],[371])).
% cnf(381,plain,(aElementOf0(X1,X2)|sdtpldt0(X3,X1)!=X2|~aElement0(X1)|~aSet0(X3)),inference(er,[status(thm)],[133,theory(equality)])).
% cnf(456,plain,(aElement0(xx)|~aSet0(xS)),inference(spm,[status(thm)],[91,231,theory(equality)])).
% cnf(463,plain,(aElement0(xx)|$false),inference(rw,[status(thm)],[456,228,theory(equality)])).
% cnf(464,plain,(aElement0(xx)),inference(cn,[status(thm)],[463,theory(equality)])).
% cnf(514,plain,(aSet0(sdtpldt0(X1,X2))|~aElement0(X2)|~aSet0(X1)),inference(er,[status(thm)],[132,theory(equality)])).
% cnf(518,plain,(aSet0(sdtmndt0(X1,X2))|~aElement0(X2)|~aSet0(X1)),inference(er,[status(thm)],[146,theory(equality)])).
% cnf(524,plain,(isFinite0(xP)|~isFinite0(sdtmndt0(xQ,xy))|~aElement0(xx)|~aSet0(sdtmndt0(xQ,xy))),inference(spm,[status(thm)],[161,240,theory(equality)])).
% cnf(550,plain,(sdtmndt0(xP,xx)=sdtmndt0(xQ,xy)|aElementOf0(xx,sdtmndt0(xQ,xy))|~aElement0(xx)|~aSet0(sdtmndt0(xQ,xy))),inference(spm,[status(thm)],[157,240,theory(equality)])).
% cnf(553,plain,(sdtmndt0(xP,xx)=sdtmndt0(xQ,xy)|~aElement0(xx)|~aSet0(sdtmndt0(xQ,xy))),inference(sr,[status(thm)],[550,242,theory(equality)])).
% cnf(583,plain,(aElementOf0(X1,sdtpldt0(X2,X1))|~aElement0(X1)|~aSet0(X2)),inference(er,[status(thm)],[381,theory(equality)])).
% cnf(706,plain,(aSubsetOf0(X1,X2)|~aElementOf0(X3,szNzAzT0)|~aElementOf0(X1,slbdtsldtrb0(X2,X3))|~aSet0(X2)),inference(er,[status(thm)],[216,theory(equality)])).
% cnf(724,plain,(aElementOf0(X1,X2)|~aElement0(X3)|~aElementOf0(X1,sdtmndt0(X2,X3))|~aSet0(X2)),inference(er,[status(thm)],[149,theory(equality)])).
% cnf(737,plain,(X1=X2|aElementOf0(X2,X3)|~aElement0(X1)|~aElementOf0(X2,sdtpldt0(X3,X1))|~aSet0(X3)),inference(er,[status(thm)],[135,theory(equality)])).
% cnf(1241,plain,(aSet0(xP)|~aElement0(xx)|~aSet0(sdtmndt0(xQ,xy))),inference(spm,[status(thm)],[514,240,theory(equality)])).
% cnf(1243,plain,(aSet0(xP)|$false|~aSet0(sdtmndt0(xQ,xy))),inference(rw,[status(thm)],[1241,464,theory(equality)])).
% cnf(1244,plain,(aSet0(xP)|~aSet0(sdtmndt0(xQ,xy))),inference(cn,[status(thm)],[1243,theory(equality)])).
% cnf(1267,plain,(aSet0(xP)|~aElement0(xy)|~aSet0(xQ)),inference(spm,[status(thm)],[1244,518,theory(equality)])).
% cnf(1269,plain,(aSet0(xP)|$false|~aSet0(xQ)),inference(rw,[status(thm)],[1267,237,theory(equality)])).
% cnf(1270,plain,(aSet0(xP)|$false|$false),inference(rw,[status(thm)],[1269,235,theory(equality)])).
% cnf(1271,plain,(aSet0(xP)),inference(cn,[status(thm)],[1270,theory(equality)])).
% cnf(1517,plain,(aElementOf0(xx,xP)|~aElement0(xx)|~aSet0(sdtmndt0(xQ,xy))),inference(spm,[status(thm)],[583,240,theory(equality)])).
% cnf(1519,plain,(aElementOf0(xx,xP)|$false|~aSet0(sdtmndt0(xQ,xy))),inference(rw,[status(thm)],[1517,464,theory(equality)])).
% cnf(1520,plain,(aElementOf0(xx,xP)|~aSet0(sdtmndt0(xQ,xy))),inference(cn,[status(thm)],[1519,theory(equality)])).
% cnf(1565,plain,(aElementOf0(xx,xP)|~aElement0(xy)|~aSet0(xQ)),inference(spm,[status(thm)],[1520,518,theory(equality)])).
% cnf(1566,plain,(aElementOf0(xx,xP)|$false|~aSet0(xQ)),inference(rw,[status(thm)],[1565,237,theory(equality)])).
% cnf(1567,plain,(aElementOf0(xx,xP)|$false|$false),inference(rw,[status(thm)],[1566,235,theory(equality)])).
% cnf(1568,plain,(aElementOf0(xx,xP)),inference(cn,[status(thm)],[1567,theory(equality)])).
% cnf(2014,plain,(isFinite0(xP)|~isFinite0(sdtmndt0(xQ,xy))|$false|~aSet0(sdtmndt0(xQ,xy))),inference(rw,[status(thm)],[524,464,theory(equality)])).
% cnf(2015,plain,(isFinite0(xP)|~isFinite0(sdtmndt0(xQ,xy))|~aSet0(sdtmndt0(xQ,xy))),inference(cn,[status(thm)],[2014,theory(equality)])).
% cnf(2017,plain,(isFinite0(xP)|~aSet0(sdtmndt0(xQ,xy))|~isFinite0(xQ)|~aElement0(xy)|~aSet0(xQ)),inference(spm,[status(thm)],[2015,165,theory(equality)])).
% cnf(2018,plain,(isFinite0(xP)|~aSet0(sdtmndt0(xQ,xy))|$false|~aElement0(xy)|~aSet0(xQ)),inference(rw,[status(thm)],[2017,234,theory(equality)])).
% cnf(2019,plain,(isFinite0(xP)|~aSet0(sdtmndt0(xQ,xy))|$false|$false|~aSet0(xQ)),inference(rw,[status(thm)],[2018,237,theory(equality)])).
% cnf(2020,plain,(isFinite0(xP)|~aSet0(sdtmndt0(xQ,xy))|$false|$false|$false),inference(rw,[status(thm)],[2019,235,theory(equality)])).
% cnf(2021,plain,(isFinite0(xP)|~aSet0(sdtmndt0(xQ,xy))),inference(cn,[status(thm)],[2020,theory(equality)])).
% cnf(2038,plain,(isFinite0(xP)|~aElement0(xy)|~aSet0(xQ)),inference(spm,[status(thm)],[2021,518,theory(equality)])).
% cnf(2039,plain,(isFinite0(xP)|$false|~aSet0(xQ)),inference(rw,[status(thm)],[2038,237,theory(equality)])).
% cnf(2040,plain,(isFinite0(xP)|$false|$false),inference(rw,[status(thm)],[2039,235,theory(equality)])).
% cnf(2041,plain,(isFinite0(xP)),inference(cn,[status(thm)],[2040,theory(equality)])).
% cnf(2553,plain,(sdtmndt0(xP,xx)=sdtmndt0(xQ,xy)|$false|~aSet0(sdtmndt0(xQ,xy))),inference(rw,[status(thm)],[553,464,theory(equality)])).
% cnf(2554,plain,(sdtmndt0(xP,xx)=sdtmndt0(xQ,xy)|~aSet0(sdtmndt0(xQ,xy))),inference(cn,[status(thm)],[2553,theory(equality)])).
% cnf(2557,plain,(sdtmndt0(xP,xx)=sdtmndt0(xQ,xy)|~aElement0(xy)|~aSet0(xQ)),inference(spm,[status(thm)],[2554,518,theory(equality)])).
% cnf(2558,plain,(sdtmndt0(xP,xx)=sdtmndt0(xQ,xy)|$false|~aSet0(xQ)),inference(rw,[status(thm)],[2557,237,theory(equality)])).
% cnf(2559,plain,(sdtmndt0(xP,xx)=sdtmndt0(xQ,xy)|$false|$false),inference(rw,[status(thm)],[2558,235,theory(equality)])).
% cnf(2560,plain,(sdtmndt0(xP,xx)=sdtmndt0(xQ,xy)),inference(cn,[status(thm)],[2559,theory(equality)])).
% cnf(2566,plain,(szszuzczcdt0(sbrdtbr0(sdtmndt0(xQ,xy)))=sbrdtbr0(xP)|~isFinite0(xP)|~aElementOf0(xx,xP)|~aSet0(xP)),inference(spm,[status(thm)],[204,2560,theory(equality)])).
% cnf(2567,plain,(aSet0(sdtmndt0(xQ,xy))|~aElement0(xx)|~aSet0(xP)),inference(spm,[status(thm)],[518,2560,theory(equality)])).
% cnf(2594,plain,(xk=sbrdtbr0(xP)|~isFinite0(xP)|~aElementOf0(xx,xP)|~aSet0(xP)),inference(rw,[status(thm)],[2566,241,theory(equality)])).
% cnf(2595,plain,(xk=sbrdtbr0(xP)|$false|~aElementOf0(xx,xP)|~aSet0(xP)),inference(rw,[status(thm)],[2594,2041,theory(equality)])).
% cnf(2596,plain,(xk=sbrdtbr0(xP)|$false|$false|~aSet0(xP)),inference(rw,[status(thm)],[2595,1568,theory(equality)])).
% cnf(2597,plain,(xk=sbrdtbr0(xP)|$false|$false|$false),inference(rw,[status(thm)],[2596,1271,theory(equality)])).
% cnf(2598,plain,(xk=sbrdtbr0(xP)),inference(cn,[status(thm)],[2597,theory(equality)])).
% cnf(2599,plain,(aSet0(sdtmndt0(xQ,xy))|$false|~aSet0(xP)),inference(rw,[status(thm)],[2567,464,theory(equality)])).
% cnf(2600,plain,(aSet0(sdtmndt0(xQ,xy))|$false|$false),inference(rw,[status(thm)],[2599,1271,theory(equality)])).
% cnf(2601,plain,(aSet0(sdtmndt0(xQ,xy))),inference(cn,[status(thm)],[2600,theory(equality)])).
% cnf(2646,negated_conjecture,($false|~aSubsetOf0(xP,xS)),inference(rw,[status(thm)],[372,2598,theory(equality)])).
% cnf(2647,negated_conjecture,(~aSubsetOf0(xP,xS)),inference(cn,[status(thm)],[2646,theory(equality)])).
% cnf(5527,plain,(aSubsetOf0(xQ,xS)|~aElementOf0(xk,szNzAzT0)|~aSet0(xS)),inference(spm,[status(thm)],[706,232,theory(equality)])).
% cnf(5539,plain,(aSubsetOf0(xQ,xS)|$false|~aSet0(xS)),inference(rw,[status(thm)],[5527,225,theory(equality)])).
% cnf(5540,plain,(aSubsetOf0(xQ,xS)|$false|$false),inference(rw,[status(thm)],[5539,228,theory(equality)])).
% cnf(5541,plain,(aSubsetOf0(xQ,xS)),inference(cn,[status(thm)],[5540,theory(equality)])).
% cnf(5573,plain,(aElementOf0(X1,xS)|~aElementOf0(X1,xQ)|~aSet0(xS)),inference(spm,[status(thm)],[109,5541,theory(equality)])).
% cnf(5588,plain,(aElementOf0(X1,xS)|~aElementOf0(X1,xQ)|$false),inference(rw,[status(thm)],[5573,228,theory(equality)])).
% cnf(5589,plain,(aElementOf0(X1,xS)|~aElementOf0(X1,xQ)),inference(cn,[status(thm)],[5588,theory(equality)])).
% cnf(5923,plain,(aSubsetOf0(X1,xS)|~aSet0(X1)|~aSet0(xS)|~aElementOf0(esk2_2(xS,X1),xQ)),inference(spm,[status(thm)],[106,5589,theory(equality)])).
% cnf(5937,plain,(aSubsetOf0(X1,xS)|~aSet0(X1)|$false|~aElementOf0(esk2_2(xS,X1),xQ)),inference(rw,[status(thm)],[5923,228,theory(equality)])).
% cnf(5938,plain,(aSubsetOf0(X1,xS)|~aSet0(X1)|~aElementOf0(esk2_2(xS,X1),xQ)),inference(cn,[status(thm)],[5937,theory(equality)])).
% cnf(8984,plain,(xx=X1|aElementOf0(X1,sdtmndt0(xQ,xy))|~aElement0(xx)|~aElementOf0(X1,xP)|~aSet0(sdtmndt0(xQ,xy))),inference(spm,[status(thm)],[737,240,theory(equality)])).
% cnf(8995,plain,(xx=X1|aElementOf0(X1,sdtmndt0(xQ,xy))|$false|~aElementOf0(X1,xP)|~aSet0(sdtmndt0(xQ,xy))),inference(rw,[status(thm)],[8984,464,theory(equality)])).
% cnf(8996,plain,(xx=X1|aElementOf0(X1,sdtmndt0(xQ,xy))|$false|~aElementOf0(X1,xP)|$false),inference(rw,[status(thm)],[8995,2601,theory(equality)])).
% cnf(8997,plain,(xx=X1|aElementOf0(X1,sdtmndt0(xQ,xy))|~aElementOf0(X1,xP)),inference(cn,[status(thm)],[8996,theory(equality)])).
% cnf(11356,plain,(aElementOf0(X1,xQ)|xx=X1|~aElement0(xy)|~aSet0(xQ)|~aElementOf0(X1,xP)),inference(spm,[status(thm)],[724,8997,theory(equality)])).
% cnf(11378,plain,(aElementOf0(X1,xQ)|xx=X1|$false|~aSet0(xQ)|~aElementOf0(X1,xP)),inference(rw,[status(thm)],[11356,237,theory(equality)])).
% cnf(11379,plain,(aElementOf0(X1,xQ)|xx=X1|$false|$false|~aElementOf0(X1,xP)),inference(rw,[status(thm)],[11378,235,theory(equality)])).
% cnf(11380,plain,(aElementOf0(X1,xQ)|xx=X1|~aElementOf0(X1,xP)),inference(cn,[status(thm)],[11379,theory(equality)])).
% cnf(11389,plain,(xx=esk2_2(X1,xP)|aElementOf0(esk2_2(X1,xP),xQ)|aSubsetOf0(xP,X1)|~aSet0(xP)|~aSet0(X1)),inference(spm,[status(thm)],[11380,107,theory(equality)])).
% cnf(11404,plain,(xx=esk2_2(X1,xP)|aElementOf0(esk2_2(X1,xP),xQ)|aSubsetOf0(xP,X1)|$false|~aSet0(X1)),inference(rw,[status(thm)],[11389,1271,theory(equality)])).
% cnf(11405,plain,(xx=esk2_2(X1,xP)|aElementOf0(esk2_2(X1,xP),xQ)|aSubsetOf0(xP,X1)|~aSet0(X1)),inference(cn,[status(thm)],[11404,theory(equality)])).
% cnf(412122,plain,(aSubsetOf0(xP,xS)|esk2_2(xS,xP)=xx|~aSet0(xP)|~aSet0(xS)),inference(spm,[status(thm)],[5938,11405,theory(equality)])).
% cnf(412159,plain,(aSubsetOf0(xP,xS)|esk2_2(xS,xP)=xx|$false|~aSet0(xS)),inference(rw,[status(thm)],[412122,1271,theory(equality)])).
% cnf(412160,plain,(aSubsetOf0(xP,xS)|esk2_2(xS,xP)=xx|$false|$false),inference(rw,[status(thm)],[412159,228,theory(equality)])).
% cnf(412161,plain,(aSubsetOf0(xP,xS)|esk2_2(xS,xP)=xx),inference(cn,[status(thm)],[412160,theory(equality)])).
% cnf(412162,plain,(esk2_2(xS,xP)=xx),inference(sr,[status(thm)],[412161,2647,theory(equality)])).
% cnf(412178,plain,(aSubsetOf0(xP,xS)|~aElementOf0(xx,xS)|~aSet0(xP)|~aSet0(xS)),inference(spm,[status(thm)],[106,412162,theory(equality)])).
% cnf(412258,plain,(aSubsetOf0(xP,xS)|$false|~aSet0(xP)|~aSet0(xS)),inference(rw,[status(thm)],[412178,231,theory(equality)])).
% cnf(412259,plain,(aSubsetOf0(xP,xS)|$false|$false|~aSet0(xS)),inference(rw,[status(thm)],[412258,1271,theory(equality)])).
% cnf(412260,plain,(aSubsetOf0(xP,xS)|$false|$false|$false),inference(rw,[status(thm)],[412259,228,theory(equality)])).
% cnf(412261,plain,(aSubsetOf0(xP,xS)),inference(cn,[status(thm)],[412260,theory(equality)])).
% cnf(412262,plain,($false),inference(sr,[status(thm)],[412261,2647,theory(equality)])).
% cnf(412263,plain,($false),412262,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 24220
% # ...of these trivial : 273
% # ...subsumed : 18632
% # ...remaining for further processing: 5315
% # Other redundant clauses eliminated : 173
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 704
% # Backward-rewritten : 222
% # Generated clauses : 203626
% # ...of the previous two non-trivial : 189700
% # Contextual simplify-reflections : 17314
% # Paramodulations : 202868
% # Factorizations : 20
% # Equation resolutions : 580
% # Current number of processed clauses: 4207
% # Positive orientable unit clauses: 152
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 101
% # Non-unit-clauses : 3954
% # Current number of unprocessed clauses: 144715
% # ...number of literals in the above : 1151585
% # Clause-clause subsumption calls (NU) : 566597
% # Rec. Clause-clause subsumption calls : 211762
% # Unit Clause-clause subsumption calls : 18022
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 133
% # Indexed BW rewrite successes : 100
% # Backwards rewriting index: 2073 leaves, 1.63+/-1.869 terms/leaf
% # Paramod-from index: 848 leaves, 1.25+/-0.810 terms/leaf
% # Paramod-into index: 1513 leaves, 1.50+/-1.511 terms/leaf
% # -------------------------------------------------
% # User time : 15.461 s
% # System time : 0.410 s
% # Total time : 15.871 s
% # Maximum resident set size: 0 pages
% PrfWatch: 22.49 CPU 23.04 WC
% FINAL PrfWatch: 22.49 CPU 23.04 WC
% SZS output end Solution for /tmp/SystemOnTPTP15331/NUM556+1.tptp
%
%------------------------------------------------------------------------------