%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : NUM558+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 : art06.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 20:06:01 EST 2010
% Result : Theorem 1.34s
% Output : Solution 1.34s
% 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/SystemOnTPTP15968/NUM558+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP15968/NUM558+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP15968/NUM558+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 16064
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.01 WC
% # Preprocessing time : 0.023 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # 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(19, 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(22, axiom,aElementOf0(xk,szNzAzT0),file('/tmp/SRASS.s.p', m__2202)).
% fof(23, axiom,((aSet0(xS)&aSet0(xT))&~(xk=sz00)),file('/tmp/SRASS.s.p', m__2202_02)).
% fof(24, axiom,(aSubsetOf0(slbdtsldtrb0(xS,xk),slbdtsldtrb0(xT,xk))&~(slbdtsldtrb0(xS,xk)=slcrc0)),file('/tmp/SRASS.s.p', m__2227)).
% fof(25, axiom,aElementOf0(xx,xS),file('/tmp/SRASS.s.p', m__2256)).
% fof(27, axiom,((aSet0(xQ)&isFinite0(xQ))&sbrdtbr0(xQ)=xk),file('/tmp/SRASS.s.p', m__2291)).
% fof(28, axiom,(aElement0(xy)&aElementOf0(xy,xQ)),file('/tmp/SRASS.s.p', m__2304)).
% fof(31, axiom,xP=sdtpldt0(sdtmndt0(xQ,xy),xx),file('/tmp/SRASS.s.p', m__2357)).
% fof(32, axiom,aElementOf0(xP,slbdtsldtrb0(xS,xk)),file('/tmp/SRASS.s.p', m__2378)).
% fof(72, conjecture,aElementOf0(xx,xT),file('/tmp/SRASS.s.p', m__)).
% fof(73, negated_conjecture,~(aElementOf0(xx,xT)),inference(assume_negation,[status(cth)],[72])).
% fof(87, negated_conjecture,~(aElementOf0(xx,xT)),inference(fof_simplification,[status(thm)],[73,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(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(133,plain,(aElementOf0(X4,X3)|~aElement0(X1)|~aSet0(X2)|X3!=sdtpldt0(X2,X1)|~aElement0(X4)|X4!=X1),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])).
% fof(180, 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)],[19])).
% fof(181, 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)],[180])).
% fof(182, 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(esk5_3(X5,X6,X7),X7))|(~(aSubsetOf0(esk5_3(X5,X6,X7),X5))|~(sbrdtbr0(esk5_3(X5,X6,X7))=X6)))&(aElementOf0(esk5_3(X5,X6,X7),X7)|(aSubsetOf0(esk5_3(X5,X6,X7),X5)&sbrdtbr0(esk5_3(X5,X6,X7))=X6))))|X7=slbdtsldtrb0(X5,X6)))),inference(skolemize,[status(esa)],[181])).
% fof(183, 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(esk5_3(X5,X6,X7),X7))|(~(aSubsetOf0(esk5_3(X5,X6,X7),X5))|~(sbrdtbr0(esk5_3(X5,X6,X7))=X6)))&(aElementOf0(esk5_3(X5,X6,X7),X7)|(aSubsetOf0(esk5_3(X5,X6,X7),X5)&sbrdtbr0(esk5_3(X5,X6,X7))=X6))))|X7=slbdtsldtrb0(X5,X6)))|(~(aSet0(X5))|~(aElementOf0(X6,szNzAzT0)))),inference(shift_quantors,[status(thm)],[182])).
% fof(184, 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(esk5_3(X5,X6,X7),X7))|(~(aSubsetOf0(esk5_3(X5,X6,X7),X5))|~(sbrdtbr0(esk5_3(X5,X6,X7))=X6)))|~(aSet0(X7)))|X7=slbdtsldtrb0(X5,X6))|(~(aSet0(X5))|~(aElementOf0(X6,szNzAzT0))))&(((((aSubsetOf0(esk5_3(X5,X6,X7),X5)|aElementOf0(esk5_3(X5,X6,X7),X7))|~(aSet0(X7)))|X7=slbdtsldtrb0(X5,X6))|(~(aSet0(X5))|~(aElementOf0(X6,szNzAzT0))))&((((sbrdtbr0(esk5_3(X5,X6,X7))=X6|aElementOf0(esk5_3(X5,X6,X7),X7))|~(aSet0(X7)))|X7=slbdtsldtrb0(X5,X6))|(~(aSet0(X5))|~(aElementOf0(X6,szNzAzT0))))))),inference(distribute,[status(thm)],[183])).
% cnf(188,plain,(aSet0(X3)|~aElementOf0(X1,szNzAzT0)|~aSet0(X2)|X3!=slbdtsldtrb0(X2,X1)),inference(split_conjunct,[status(thm)],[184])).
% cnf(191,plain,(aSubsetOf0(X4,X2)|~aElementOf0(X1,szNzAzT0)|~aSet0(X2)|X3!=slbdtsldtrb0(X2,X1)|~aElementOf0(X4,X3)),inference(split_conjunct,[status(thm)],[184])).
% cnf(200,plain,(aElementOf0(xk,szNzAzT0)),inference(split_conjunct,[status(thm)],[22])).
% cnf(202,plain,(aSet0(xT)),inference(split_conjunct,[status(thm)],[23])).
% cnf(203,plain,(aSet0(xS)),inference(split_conjunct,[status(thm)],[23])).
% cnf(205,plain,(aSubsetOf0(slbdtsldtrb0(xS,xk),slbdtsldtrb0(xT,xk))),inference(split_conjunct,[status(thm)],[24])).
% cnf(206,plain,(aElementOf0(xx,xS)),inference(split_conjunct,[status(thm)],[25])).
% cnf(210,plain,(aSet0(xQ)),inference(split_conjunct,[status(thm)],[27])).
% cnf(212,plain,(aElement0(xy)),inference(split_conjunct,[status(thm)],[28])).
% cnf(215,plain,(xP=sdtpldt0(sdtmndt0(xQ,xy),xx)),inference(split_conjunct,[status(thm)],[31])).
% cnf(216,plain,(aElementOf0(xP,slbdtsldtrb0(xS,xk))),inference(split_conjunct,[status(thm)],[32])).
% cnf(370,negated_conjecture,(~aElementOf0(xx,xT)),inference(split_conjunct,[status(thm)],[87])).
% cnf(377,plain,(aElementOf0(X1,X2)|sdtpldt0(X3,X1)!=X2|~aElement0(X1)|~aSet0(X3)),inference(er,[status(thm)],[133,theory(equality)])).
% cnf(431,plain,(aElement0(xx)|~aSet0(xS)),inference(spm,[status(thm)],[91,206,theory(equality)])).
% cnf(441,plain,(aElement0(xx)|$false),inference(rw,[status(thm)],[431,203,theory(equality)])).
% cnf(442,plain,(aElement0(xx)),inference(cn,[status(thm)],[441,theory(equality)])).
% cnf(506,plain,(aElementOf0(X1,slbdtsldtrb0(xT,xk))|~aElementOf0(X1,slbdtsldtrb0(xS,xk))|~aSet0(slbdtsldtrb0(xT,xk))),inference(spm,[status(thm)],[109,205,theory(equality)])).
% cnf(517,plain,(aElementOf0(X1,sdtpldt0(X2,X1))|~aElement0(X1)|~aSet0(X2)),inference(er,[status(thm)],[377,theory(equality)])).
% cnf(522,plain,(aSet0(slbdtsldtrb0(X1,X2))|~aElementOf0(X2,szNzAzT0)|~aSet0(X1)),inference(er,[status(thm)],[188,theory(equality)])).
% cnf(525,plain,(aSet0(sdtmndt0(X1,X2))|~aElement0(X2)|~aSet0(X1)),inference(er,[status(thm)],[146,theory(equality)])).
% cnf(685,plain,(aSubsetOf0(X1,X2)|~aElementOf0(X3,szNzAzT0)|~aElementOf0(X1,slbdtsldtrb0(X2,X3))|~aSet0(X2)),inference(er,[status(thm)],[191,theory(equality)])).
% cnf(1055,plain,(aElementOf0(xx,xP)|~aElement0(xx)|~aSet0(sdtmndt0(xQ,xy))),inference(spm,[status(thm)],[517,215,theory(equality)])).
% cnf(1057,plain,(aElementOf0(xx,xP)|$false|~aSet0(sdtmndt0(xQ,xy))),inference(rw,[status(thm)],[1055,442,theory(equality)])).
% cnf(1058,plain,(aElementOf0(xx,xP)|~aSet0(sdtmndt0(xQ,xy))),inference(cn,[status(thm)],[1057,theory(equality)])).
% cnf(1186,plain,(aElementOf0(xx,xP)|~aElement0(xy)|~aSet0(xQ)),inference(spm,[status(thm)],[1058,525,theory(equality)])).
% cnf(1194,plain,(aElementOf0(xx,xP)|$false|~aSet0(xQ)),inference(rw,[status(thm)],[1186,212,theory(equality)])).
% cnf(1195,plain,(aElementOf0(xx,xP)|$false|$false),inference(rw,[status(thm)],[1194,210,theory(equality)])).
% cnf(1196,plain,(aElementOf0(xx,xP)),inference(cn,[status(thm)],[1195,theory(equality)])).
% cnf(3993,plain,(aSubsetOf0(X1,xT)|~aElementOf0(xk,szNzAzT0)|~aSet0(xT)|~aElementOf0(X1,slbdtsldtrb0(xS,xk))|~aSet0(slbdtsldtrb0(xT,xk))),inference(spm,[status(thm)],[685,506,theory(equality)])).
% cnf(4000,plain,(aSubsetOf0(X1,xT)|$false|~aSet0(xT)|~aElementOf0(X1,slbdtsldtrb0(xS,xk))|~aSet0(slbdtsldtrb0(xT,xk))),inference(rw,[status(thm)],[3993,200,theory(equality)])).
% cnf(4001,plain,(aSubsetOf0(X1,xT)|$false|$false|~aElementOf0(X1,slbdtsldtrb0(xS,xk))|~aSet0(slbdtsldtrb0(xT,xk))),inference(rw,[status(thm)],[4000,202,theory(equality)])).
% cnf(4002,plain,(aSubsetOf0(X1,xT)|~aElementOf0(X1,slbdtsldtrb0(xS,xk))|~aSet0(slbdtsldtrb0(xT,xk))),inference(cn,[status(thm)],[4001,theory(equality)])).
% cnf(5757,plain,(aSubsetOf0(xP,xT)|~aSet0(slbdtsldtrb0(xT,xk))),inference(spm,[status(thm)],[4002,216,theory(equality)])).
% cnf(5771,plain,(aSubsetOf0(xP,xT)|~aElementOf0(xk,szNzAzT0)|~aSet0(xT)),inference(spm,[status(thm)],[5757,522,theory(equality)])).
% cnf(5772,plain,(aSubsetOf0(xP,xT)|$false|~aSet0(xT)),inference(rw,[status(thm)],[5771,200,theory(equality)])).
% cnf(5773,plain,(aSubsetOf0(xP,xT)|$false|$false),inference(rw,[status(thm)],[5772,202,theory(equality)])).
% cnf(5774,plain,(aSubsetOf0(xP,xT)),inference(cn,[status(thm)],[5773,theory(equality)])).
% cnf(5843,plain,(aElementOf0(X1,xT)|~aElementOf0(X1,xP)|~aSet0(xT)),inference(spm,[status(thm)],[109,5774,theory(equality)])).
% cnf(5862,plain,(aElementOf0(X1,xT)|~aElementOf0(X1,xP)|$false),inference(rw,[status(thm)],[5843,202,theory(equality)])).
% cnf(5863,plain,(aElementOf0(X1,xT)|~aElementOf0(X1,xP)),inference(cn,[status(thm)],[5862,theory(equality)])).
% cnf(5871,negated_conjecture,(~aElementOf0(xx,xP)),inference(spm,[status(thm)],[370,5863,theory(equality)])).
% cnf(5887,negated_conjecture,($false),inference(rw,[status(thm)],[5871,1196,theory(equality)])).
% cnf(5888,negated_conjecture,($false),inference(cn,[status(thm)],[5887,theory(equality)])).
% cnf(5889,negated_conjecture,($false),5888,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 1239
% # ...of these trivial : 25
% # ...subsumed : 504
% # ...remaining for further processing: 710
% # Other redundant clauses eliminated : 14
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 39
% # Backward-rewritten : 23
% # Generated clauses : 3041
% # ...of the previous two non-trivial : 2747
% # Contextual simplify-reflections : 446
% # Paramodulations : 2974
% # Factorizations : 0
% # Equation resolutions : 64
% # Current number of processed clauses: 523
% # Positive orientable unit clauses: 44
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 26
% # Non-unit-clauses : 453
% # Current number of unprocessed clauses: 1578
% # ...number of literals in the above : 9713
% # Clause-clause subsumption calls (NU) : 10606
% # Rec. Clause-clause subsumption calls : 5802
% # Unit Clause-clause subsumption calls : 810
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 17
% # Indexed BW rewrite successes : 15
% # Backwards rewriting index: 399 leaves, 1.28+/-0.813 terms/leaf
% # Paramod-from index: 193 leaves, 1.04+/-0.199 terms/leaf
% # Paramod-into index: 339 leaves, 1.20+/-0.663 terms/leaf
% # -------------------------------------------------
% # User time : 0.241 s
% # System time : 0.011 s
% # Total time : 0.252 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.43 CPU 0.49 WC
% FINAL PrfWatch: 0.43 CPU 0.49 WC
% SZS output end Solution for /tmp/SystemOnTPTP15968/NUM558+1.tptp
%
%------------------------------------------------------------------------------