%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : RNG097+2 : TPTP v5.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %s
% Computer : art07.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 22:32:46 EST 2010
% Result : Theorem 2.49s
% Output : Solution 2.49s
% 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/SystemOnTPTP5230/RNG097+2.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP5230/RNG097+2.tptp
% SZS output start Solution for /tmp/SystemOnTPTP5230/RNG097+2.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 5326
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.00 WC
% # Preprocessing time : 0.016 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(1, axiom,aElement0(sz10),file('/tmp/SRASS.s.p', mSortsC_01)).
% fof(2, axiom,![X1]:(aElement0(X1)=>aElement0(smndt0(X1))),file('/tmp/SRASS.s.p', mSortsU)).
% fof(3, axiom,![X1]:![X2]:((aElement0(X1)&aElement0(X2))=>aElement0(sdtpldt0(X1,X2))),file('/tmp/SRASS.s.p', mSortsB)).
% fof(4, axiom,![X1]:![X2]:((aElement0(X1)&aElement0(X2))=>aElement0(sdtasdt0(X1,X2))),file('/tmp/SRASS.s.p', mSortsB_02)).
% fof(5, axiom,![X1]:![X2]:((aElement0(X1)&aElement0(X2))=>sdtpldt0(X1,X2)=sdtpldt0(X2,X1)),file('/tmp/SRASS.s.p', mAddComm)).
% fof(6, axiom,![X1]:![X2]:![X3]:(((aElement0(X1)&aElement0(X2))&aElement0(X3))=>sdtpldt0(sdtpldt0(X1,X2),X3)=sdtpldt0(X1,sdtpldt0(X2,X3))),file('/tmp/SRASS.s.p', mAddAsso)).
% fof(7, axiom,![X1]:![X2]:((aElement0(X1)&aElement0(X2))=>sdtasdt0(X1,X2)=sdtasdt0(X2,X1)),file('/tmp/SRASS.s.p', mMulComm)).
% fof(8, axiom,![X1]:![X2]:![X3]:(((aElement0(X1)&aElement0(X2))&aElement0(X3))=>sdtasdt0(sdtasdt0(X1,X2),X3)=sdtasdt0(X1,sdtasdt0(X2,X3))),file('/tmp/SRASS.s.p', mMulAsso)).
% fof(9, axiom,![X1]:(aElement0(X1)=>(sdtasdt0(X1,sz10)=X1&X1=sdtasdt0(sz10,X1))),file('/tmp/SRASS.s.p', mMulUnit)).
% fof(10, axiom,![X1]:![X2]:![X3]:(((aElement0(X1)&aElement0(X2))&aElement0(X3))=>(sdtasdt0(X1,sdtpldt0(X2,X3))=sdtpldt0(sdtasdt0(X1,X2),sdtasdt0(X1,X3))&sdtasdt0(sdtpldt0(X2,X3),X1)=sdtpldt0(sdtasdt0(X2,X1),sdtasdt0(X3,X1)))),file('/tmp/SRASS.s.p', mAMDistr)).
% fof(11, axiom,![X1]:(aElement0(X1)=>(sdtasdt0(smndt0(sz10),X1)=smndt0(X1)&smndt0(X1)=sdtasdt0(X1,smndt0(sz10)))),file('/tmp/SRASS.s.p', mMulMnOne)).
% fof(12, axiom,![X1]:(aSet0(X1)=>![X2]:(aElementOf0(X2,X1)=>aElement0(X2))),file('/tmp/SRASS.s.p', mEOfElem)).
% fof(15, axiom,![X1]:(aIdeal0(X1)<=>(aSet0(X1)&![X2]:(aElementOf0(X2,X1)=>(![X3]:(aElementOf0(X3,X1)=>aElementOf0(sdtpldt0(X2,X3),X1))&![X3]:(aElement0(X3)=>aElementOf0(sdtasdt0(X3,X2),X1)))))),file('/tmp/SRASS.s.p', mDefIdeal)).
% fof(17, axiom,(((((aSet0(xI)&![X1]:(aElementOf0(X1,xI)=>(![X2]:(aElementOf0(X2,xI)=>aElementOf0(sdtpldt0(X1,X2),xI))&![X2]:(aElement0(X2)=>aElementOf0(sdtasdt0(X2,X1),xI)))))&aIdeal0(xI))&aSet0(xJ))&![X1]:(aElementOf0(X1,xJ)=>(![X2]:(aElementOf0(X2,xJ)=>aElementOf0(sdtpldt0(X1,X2),xJ))&![X2]:(aElement0(X2)=>aElementOf0(sdtasdt0(X2,X1),xJ)))))&aIdeal0(xJ)),file('/tmp/SRASS.s.p', m__1205)).
% fof(19, axiom,(aElement0(xx)&aElement0(xy)),file('/tmp/SRASS.s.p', m__1217)).
% fof(20, axiom,((aElementOf0(xa,xI)&aElementOf0(xb,xJ))&sdtpldt0(xa,xb)=sz10),file('/tmp/SRASS.s.p', m__1294)).
% fof(24, axiom,![X1]:(aElement0(X1)=>(sdtpldt0(X1,smndt0(X1))=sz00&sz00=sdtpldt0(smndt0(X1),X1))),file('/tmp/SRASS.s.p', mAddInvr)).
% fof(26, axiom,![X1]:(aElement0(X1)=>(sdtpldt0(X1,sz00)=X1&X1=sdtpldt0(sz00,X1))),file('/tmp/SRASS.s.p', mAddZero)).
% fof(27, axiom,![X1]:(aElement0(X1)=>(sdtasdt0(X1,sz00)=sz00&sz00=sdtasdt0(sz00,X1))),file('/tmp/SRASS.s.p', mMulZero)).
% fof(28, axiom,![X1]:![X2]:((aElement0(X1)&aElement0(X2))=>(sdtasdt0(X1,X2)=sz00=>(X1=sz00|X2=sz00))),file('/tmp/SRASS.s.p', mCancel)).
% fof(29, axiom,~(sz10=sz00),file('/tmp/SRASS.s.p', mUnNeZr)).
% fof(30, axiom,aElement0(sz00),file('/tmp/SRASS.s.p', mSortsC)).
% fof(34, conjecture,aElementOf0(sdtasdt0(xx,sdtpldt0(xb,smndt0(sz10))),xI),file('/tmp/SRASS.s.p', m__)).
% fof(35, negated_conjecture,~(aElementOf0(sdtasdt0(xx,sdtpldt0(xb,smndt0(sz10))),xI)),inference(assume_negation,[status(cth)],[34])).
% fof(38, negated_conjecture,~(aElementOf0(sdtasdt0(xx,sdtpldt0(xb,smndt0(sz10))),xI)),inference(fof_simplification,[status(thm)],[35,theory(equality)])).
% cnf(39,plain,(aElement0(sz10)),inference(split_conjunct,[status(thm)],[1])).
% fof(40, plain,![X1]:(~(aElement0(X1))|aElement0(smndt0(X1))),inference(fof_nnf,[status(thm)],[2])).
% fof(41, plain,![X2]:(~(aElement0(X2))|aElement0(smndt0(X2))),inference(variable_rename,[status(thm)],[40])).
% cnf(42,plain,(aElement0(smndt0(X1))|~aElement0(X1)),inference(split_conjunct,[status(thm)],[41])).
% fof(43, plain,![X1]:![X2]:((~(aElement0(X1))|~(aElement0(X2)))|aElement0(sdtpldt0(X1,X2))),inference(fof_nnf,[status(thm)],[3])).
% fof(44, plain,![X3]:![X4]:((~(aElement0(X3))|~(aElement0(X4)))|aElement0(sdtpldt0(X3,X4))),inference(variable_rename,[status(thm)],[43])).
% cnf(45,plain,(aElement0(sdtpldt0(X1,X2))|~aElement0(X2)|~aElement0(X1)),inference(split_conjunct,[status(thm)],[44])).
% fof(46, plain,![X1]:![X2]:((~(aElement0(X1))|~(aElement0(X2)))|aElement0(sdtasdt0(X1,X2))),inference(fof_nnf,[status(thm)],[4])).
% fof(47, plain,![X3]:![X4]:((~(aElement0(X3))|~(aElement0(X4)))|aElement0(sdtasdt0(X3,X4))),inference(variable_rename,[status(thm)],[46])).
% cnf(48,plain,(aElement0(sdtasdt0(X1,X2))|~aElement0(X2)|~aElement0(X1)),inference(split_conjunct,[status(thm)],[47])).
% fof(49, plain,![X1]:![X2]:((~(aElement0(X1))|~(aElement0(X2)))|sdtpldt0(X1,X2)=sdtpldt0(X2,X1)),inference(fof_nnf,[status(thm)],[5])).
% fof(50, plain,![X3]:![X4]:((~(aElement0(X3))|~(aElement0(X4)))|sdtpldt0(X3,X4)=sdtpldt0(X4,X3)),inference(variable_rename,[status(thm)],[49])).
% cnf(51,plain,(sdtpldt0(X1,X2)=sdtpldt0(X2,X1)|~aElement0(X2)|~aElement0(X1)),inference(split_conjunct,[status(thm)],[50])).
% fof(52, plain,![X1]:![X2]:![X3]:(((~(aElement0(X1))|~(aElement0(X2)))|~(aElement0(X3)))|sdtpldt0(sdtpldt0(X1,X2),X3)=sdtpldt0(X1,sdtpldt0(X2,X3))),inference(fof_nnf,[status(thm)],[6])).
% fof(53, plain,![X4]:![X5]:![X6]:(((~(aElement0(X4))|~(aElement0(X5)))|~(aElement0(X6)))|sdtpldt0(sdtpldt0(X4,X5),X6)=sdtpldt0(X4,sdtpldt0(X5,X6))),inference(variable_rename,[status(thm)],[52])).
% cnf(54,plain,(sdtpldt0(sdtpldt0(X1,X2),X3)=sdtpldt0(X1,sdtpldt0(X2,X3))|~aElement0(X3)|~aElement0(X2)|~aElement0(X1)),inference(split_conjunct,[status(thm)],[53])).
% fof(55, plain,![X1]:![X2]:((~(aElement0(X1))|~(aElement0(X2)))|sdtasdt0(X1,X2)=sdtasdt0(X2,X1)),inference(fof_nnf,[status(thm)],[7])).
% fof(56, plain,![X3]:![X4]:((~(aElement0(X3))|~(aElement0(X4)))|sdtasdt0(X3,X4)=sdtasdt0(X4,X3)),inference(variable_rename,[status(thm)],[55])).
% cnf(57,plain,(sdtasdt0(X1,X2)=sdtasdt0(X2,X1)|~aElement0(X2)|~aElement0(X1)),inference(split_conjunct,[status(thm)],[56])).
% fof(58, plain,![X1]:![X2]:![X3]:(((~(aElement0(X1))|~(aElement0(X2)))|~(aElement0(X3)))|sdtasdt0(sdtasdt0(X1,X2),X3)=sdtasdt0(X1,sdtasdt0(X2,X3))),inference(fof_nnf,[status(thm)],[8])).
% fof(59, plain,![X4]:![X5]:![X6]:(((~(aElement0(X4))|~(aElement0(X5)))|~(aElement0(X6)))|sdtasdt0(sdtasdt0(X4,X5),X6)=sdtasdt0(X4,sdtasdt0(X5,X6))),inference(variable_rename,[status(thm)],[58])).
% cnf(60,plain,(sdtasdt0(sdtasdt0(X1,X2),X3)=sdtasdt0(X1,sdtasdt0(X2,X3))|~aElement0(X3)|~aElement0(X2)|~aElement0(X1)),inference(split_conjunct,[status(thm)],[59])).
% fof(61, plain,![X1]:(~(aElement0(X1))|(sdtasdt0(X1,sz10)=X1&X1=sdtasdt0(sz10,X1))),inference(fof_nnf,[status(thm)],[9])).
% fof(62, plain,![X2]:(~(aElement0(X2))|(sdtasdt0(X2,sz10)=X2&X2=sdtasdt0(sz10,X2))),inference(variable_rename,[status(thm)],[61])).
% fof(63, plain,![X2]:((sdtasdt0(X2,sz10)=X2|~(aElement0(X2)))&(X2=sdtasdt0(sz10,X2)|~(aElement0(X2)))),inference(distribute,[status(thm)],[62])).
% cnf(64,plain,(X1=sdtasdt0(sz10,X1)|~aElement0(X1)),inference(split_conjunct,[status(thm)],[63])).
% cnf(65,plain,(sdtasdt0(X1,sz10)=X1|~aElement0(X1)),inference(split_conjunct,[status(thm)],[63])).
% fof(66, plain,![X1]:![X2]:![X3]:(((~(aElement0(X1))|~(aElement0(X2)))|~(aElement0(X3)))|(sdtasdt0(X1,sdtpldt0(X2,X3))=sdtpldt0(sdtasdt0(X1,X2),sdtasdt0(X1,X3))&sdtasdt0(sdtpldt0(X2,X3),X1)=sdtpldt0(sdtasdt0(X2,X1),sdtasdt0(X3,X1)))),inference(fof_nnf,[status(thm)],[10])).
% fof(67, plain,![X4]:![X5]:![X6]:(((~(aElement0(X4))|~(aElement0(X5)))|~(aElement0(X6)))|(sdtasdt0(X4,sdtpldt0(X5,X6))=sdtpldt0(sdtasdt0(X4,X5),sdtasdt0(X4,X6))&sdtasdt0(sdtpldt0(X5,X6),X4)=sdtpldt0(sdtasdt0(X5,X4),sdtasdt0(X6,X4)))),inference(variable_rename,[status(thm)],[66])).
% fof(68, plain,![X4]:![X5]:![X6]:((sdtasdt0(X4,sdtpldt0(X5,X6))=sdtpldt0(sdtasdt0(X4,X5),sdtasdt0(X4,X6))|((~(aElement0(X4))|~(aElement0(X5)))|~(aElement0(X6))))&(sdtasdt0(sdtpldt0(X5,X6),X4)=sdtpldt0(sdtasdt0(X5,X4),sdtasdt0(X6,X4))|((~(aElement0(X4))|~(aElement0(X5)))|~(aElement0(X6))))),inference(distribute,[status(thm)],[67])).
% cnf(70,plain,(sdtasdt0(X3,sdtpldt0(X2,X1))=sdtpldt0(sdtasdt0(X3,X2),sdtasdt0(X3,X1))|~aElement0(X1)|~aElement0(X2)|~aElement0(X3)),inference(split_conjunct,[status(thm)],[68])).
% fof(71, plain,![X1]:(~(aElement0(X1))|(sdtasdt0(smndt0(sz10),X1)=smndt0(X1)&smndt0(X1)=sdtasdt0(X1,smndt0(sz10)))),inference(fof_nnf,[status(thm)],[11])).
% fof(72, plain,![X2]:(~(aElement0(X2))|(sdtasdt0(smndt0(sz10),X2)=smndt0(X2)&smndt0(X2)=sdtasdt0(X2,smndt0(sz10)))),inference(variable_rename,[status(thm)],[71])).
% fof(73, plain,![X2]:((sdtasdt0(smndt0(sz10),X2)=smndt0(X2)|~(aElement0(X2)))&(smndt0(X2)=sdtasdt0(X2,smndt0(sz10))|~(aElement0(X2)))),inference(distribute,[status(thm)],[72])).
% cnf(75,plain,(sdtasdt0(smndt0(sz10),X1)=smndt0(X1)|~aElement0(X1)),inference(split_conjunct,[status(thm)],[73])).
% fof(76, plain,![X1]:(~(aSet0(X1))|![X2]:(~(aElementOf0(X2,X1))|aElement0(X2))),inference(fof_nnf,[status(thm)],[12])).
% fof(77, plain,![X3]:(~(aSet0(X3))|![X4]:(~(aElementOf0(X4,X3))|aElement0(X4))),inference(variable_rename,[status(thm)],[76])).
% fof(78, plain,![X3]:![X4]:((~(aElementOf0(X4,X3))|aElement0(X4))|~(aSet0(X3))),inference(shift_quantors,[status(thm)],[77])).
% cnf(79,plain,(aElement0(X2)|~aSet0(X1)|~aElementOf0(X2,X1)),inference(split_conjunct,[status(thm)],[78])).
% fof(102, plain,![X1]:((~(aIdeal0(X1))|(aSet0(X1)&![X2]:(~(aElementOf0(X2,X1))|(![X3]:(~(aElementOf0(X3,X1))|aElementOf0(sdtpldt0(X2,X3),X1))&![X3]:(~(aElement0(X3))|aElementOf0(sdtasdt0(X3,X2),X1))))))&((~(aSet0(X1))|?[X2]:(aElementOf0(X2,X1)&(?[X3]:(aElementOf0(X3,X1)&~(aElementOf0(sdtpldt0(X2,X3),X1)))|?[X3]:(aElement0(X3)&~(aElementOf0(sdtasdt0(X3,X2),X1))))))|aIdeal0(X1))),inference(fof_nnf,[status(thm)],[15])).
% fof(103, plain,![X4]:((~(aIdeal0(X4))|(aSet0(X4)&![X5]:(~(aElementOf0(X5,X4))|(![X6]:(~(aElementOf0(X6,X4))|aElementOf0(sdtpldt0(X5,X6),X4))&![X7]:(~(aElement0(X7))|aElementOf0(sdtasdt0(X7,X5),X4))))))&((~(aSet0(X4))|?[X8]:(aElementOf0(X8,X4)&(?[X9]:(aElementOf0(X9,X4)&~(aElementOf0(sdtpldt0(X8,X9),X4)))|?[X10]:(aElement0(X10)&~(aElementOf0(sdtasdt0(X10,X8),X4))))))|aIdeal0(X4))),inference(variable_rename,[status(thm)],[102])).
% fof(104, plain,![X4]:((~(aIdeal0(X4))|(aSet0(X4)&![X5]:(~(aElementOf0(X5,X4))|(![X6]:(~(aElementOf0(X6,X4))|aElementOf0(sdtpldt0(X5,X6),X4))&![X7]:(~(aElement0(X7))|aElementOf0(sdtasdt0(X7,X5),X4))))))&((~(aSet0(X4))|(aElementOf0(esk8_1(X4),X4)&((aElementOf0(esk9_1(X4),X4)&~(aElementOf0(sdtpldt0(esk8_1(X4),esk9_1(X4)),X4)))|(aElement0(esk10_1(X4))&~(aElementOf0(sdtasdt0(esk10_1(X4),esk8_1(X4)),X4))))))|aIdeal0(X4))),inference(skolemize,[status(esa)],[103])).
% fof(105, plain,![X4]:![X5]:![X6]:![X7]:((((((~(aElement0(X7))|aElementOf0(sdtasdt0(X7,X5),X4))&(~(aElementOf0(X6,X4))|aElementOf0(sdtpldt0(X5,X6),X4)))|~(aElementOf0(X5,X4)))&aSet0(X4))|~(aIdeal0(X4)))&((~(aSet0(X4))|(aElementOf0(esk8_1(X4),X4)&((aElementOf0(esk9_1(X4),X4)&~(aElementOf0(sdtpldt0(esk8_1(X4),esk9_1(X4)),X4)))|(aElement0(esk10_1(X4))&~(aElementOf0(sdtasdt0(esk10_1(X4),esk8_1(X4)),X4))))))|aIdeal0(X4))),inference(shift_quantors,[status(thm)],[104])).
% fof(106, plain,![X4]:![X5]:![X6]:![X7]:((((((~(aElement0(X7))|aElementOf0(sdtasdt0(X7,X5),X4))|~(aElementOf0(X5,X4)))|~(aIdeal0(X4)))&(((~(aElementOf0(X6,X4))|aElementOf0(sdtpldt0(X5,X6),X4))|~(aElementOf0(X5,X4)))|~(aIdeal0(X4))))&(aSet0(X4)|~(aIdeal0(X4))))&(((aElementOf0(esk8_1(X4),X4)|~(aSet0(X4)))|aIdeal0(X4))&(((((aElement0(esk10_1(X4))|aElementOf0(esk9_1(X4),X4))|~(aSet0(X4)))|aIdeal0(X4))&(((~(aElementOf0(sdtasdt0(esk10_1(X4),esk8_1(X4)),X4))|aElementOf0(esk9_1(X4),X4))|~(aSet0(X4)))|aIdeal0(X4)))&((((aElement0(esk10_1(X4))|~(aElementOf0(sdtpldt0(esk8_1(X4),esk9_1(X4)),X4)))|~(aSet0(X4)))|aIdeal0(X4))&(((~(aElementOf0(sdtasdt0(esk10_1(X4),esk8_1(X4)),X4))|~(aElementOf0(sdtpldt0(esk8_1(X4),esk9_1(X4)),X4)))|~(aSet0(X4)))|aIdeal0(X4)))))),inference(distribute,[status(thm)],[105])).
% cnf(112,plain,(aSet0(X1)|~aIdeal0(X1)),inference(split_conjunct,[status(thm)],[106])).
% cnf(114,plain,(aElementOf0(sdtasdt0(X3,X2),X1)|~aIdeal0(X1)|~aElementOf0(X2,X1)|~aElement0(X3)),inference(split_conjunct,[status(thm)],[106])).
% fof(118, plain,(((((aSet0(xI)&![X1]:(~(aElementOf0(X1,xI))|(![X2]:(~(aElementOf0(X2,xI))|aElementOf0(sdtpldt0(X1,X2),xI))&![X2]:(~(aElement0(X2))|aElementOf0(sdtasdt0(X2,X1),xI)))))&aIdeal0(xI))&aSet0(xJ))&![X1]:(~(aElementOf0(X1,xJ))|(![X2]:(~(aElementOf0(X2,xJ))|aElementOf0(sdtpldt0(X1,X2),xJ))&![X2]:(~(aElement0(X2))|aElementOf0(sdtasdt0(X2,X1),xJ)))))&aIdeal0(xJ)),inference(fof_nnf,[status(thm)],[17])).
% fof(119, plain,(((((aSet0(xI)&![X3]:(~(aElementOf0(X3,xI))|(![X4]:(~(aElementOf0(X4,xI))|aElementOf0(sdtpldt0(X3,X4),xI))&![X5]:(~(aElement0(X5))|aElementOf0(sdtasdt0(X5,X3),xI)))))&aIdeal0(xI))&aSet0(xJ))&![X6]:(~(aElementOf0(X6,xJ))|(![X7]:(~(aElementOf0(X7,xJ))|aElementOf0(sdtpldt0(X6,X7),xJ))&![X8]:(~(aElement0(X8))|aElementOf0(sdtasdt0(X8,X6),xJ)))))&aIdeal0(xJ)),inference(variable_rename,[status(thm)],[118])).
% fof(120, plain,![X3]:![X4]:![X5]:![X6]:![X7]:![X8]:(((((~(aElement0(X8))|aElementOf0(sdtasdt0(X8,X6),xJ))&(~(aElementOf0(X7,xJ))|aElementOf0(sdtpldt0(X6,X7),xJ)))|~(aElementOf0(X6,xJ)))&((((((~(aElement0(X5))|aElementOf0(sdtasdt0(X5,X3),xI))&(~(aElementOf0(X4,xI))|aElementOf0(sdtpldt0(X3,X4),xI)))|~(aElementOf0(X3,xI)))&aSet0(xI))&aIdeal0(xI))&aSet0(xJ)))&aIdeal0(xJ)),inference(shift_quantors,[status(thm)],[119])).
% fof(121, plain,![X3]:![X4]:![X5]:![X6]:![X7]:![X8]:(((((~(aElement0(X8))|aElementOf0(sdtasdt0(X8,X6),xJ))|~(aElementOf0(X6,xJ)))&((~(aElementOf0(X7,xJ))|aElementOf0(sdtpldt0(X6,X7),xJ))|~(aElementOf0(X6,xJ))))&((((((~(aElement0(X5))|aElementOf0(sdtasdt0(X5,X3),xI))|~(aElementOf0(X3,xI)))&((~(aElementOf0(X4,xI))|aElementOf0(sdtpldt0(X3,X4),xI))|~(aElementOf0(X3,xI))))&aSet0(xI))&aIdeal0(xI))&aSet0(xJ)))&aIdeal0(xJ)),inference(distribute,[status(thm)],[120])).
% cnf(123,plain,(aSet0(xJ)),inference(split_conjunct,[status(thm)],[121])).
% cnf(124,plain,(aIdeal0(xI)),inference(split_conjunct,[status(thm)],[121])).
% cnf(125,plain,(aSet0(xI)),inference(split_conjunct,[status(thm)],[121])).
% cnf(127,plain,(aElementOf0(sdtasdt0(X2,X1),xI)|~aElementOf0(X1,xI)|~aElement0(X2)),inference(split_conjunct,[status(thm)],[121])).
% cnf(139,plain,(aElement0(xx)),inference(split_conjunct,[status(thm)],[19])).
% cnf(140,plain,(sdtpldt0(xa,xb)=sz10),inference(split_conjunct,[status(thm)],[20])).
% cnf(141,plain,(aElementOf0(xb,xJ)),inference(split_conjunct,[status(thm)],[20])).
% cnf(142,plain,(aElementOf0(xa,xI)),inference(split_conjunct,[status(thm)],[20])).
% fof(150, plain,![X1]:(~(aElement0(X1))|(sdtpldt0(X1,smndt0(X1))=sz00&sz00=sdtpldt0(smndt0(X1),X1))),inference(fof_nnf,[status(thm)],[24])).
% fof(151, plain,![X2]:(~(aElement0(X2))|(sdtpldt0(X2,smndt0(X2))=sz00&sz00=sdtpldt0(smndt0(X2),X2))),inference(variable_rename,[status(thm)],[150])).
% fof(152, plain,![X2]:((sdtpldt0(X2,smndt0(X2))=sz00|~(aElement0(X2)))&(sz00=sdtpldt0(smndt0(X2),X2)|~(aElement0(X2)))),inference(distribute,[status(thm)],[151])).
% cnf(153,plain,(sz00=sdtpldt0(smndt0(X1),X1)|~aElement0(X1)),inference(split_conjunct,[status(thm)],[152])).
% cnf(154,plain,(sdtpldt0(X1,smndt0(X1))=sz00|~aElement0(X1)),inference(split_conjunct,[status(thm)],[152])).
% fof(167, plain,![X1]:(~(aElement0(X1))|(sdtpldt0(X1,sz00)=X1&X1=sdtpldt0(sz00,X1))),inference(fof_nnf,[status(thm)],[26])).
% fof(168, plain,![X2]:(~(aElement0(X2))|(sdtpldt0(X2,sz00)=X2&X2=sdtpldt0(sz00,X2))),inference(variable_rename,[status(thm)],[167])).
% fof(169, plain,![X2]:((sdtpldt0(X2,sz00)=X2|~(aElement0(X2)))&(X2=sdtpldt0(sz00,X2)|~(aElement0(X2)))),inference(distribute,[status(thm)],[168])).
% cnf(170,plain,(X1=sdtpldt0(sz00,X1)|~aElement0(X1)),inference(split_conjunct,[status(thm)],[169])).
% cnf(171,plain,(sdtpldt0(X1,sz00)=X1|~aElement0(X1)),inference(split_conjunct,[status(thm)],[169])).
% fof(172, plain,![X1]:(~(aElement0(X1))|(sdtasdt0(X1,sz00)=sz00&sz00=sdtasdt0(sz00,X1))),inference(fof_nnf,[status(thm)],[27])).
% fof(173, plain,![X2]:(~(aElement0(X2))|(sdtasdt0(X2,sz00)=sz00&sz00=sdtasdt0(sz00,X2))),inference(variable_rename,[status(thm)],[172])).
% fof(174, plain,![X2]:((sdtasdt0(X2,sz00)=sz00|~(aElement0(X2)))&(sz00=sdtasdt0(sz00,X2)|~(aElement0(X2)))),inference(distribute,[status(thm)],[173])).
% cnf(175,plain,(sz00=sdtasdt0(sz00,X1)|~aElement0(X1)),inference(split_conjunct,[status(thm)],[174])).
% cnf(176,plain,(sdtasdt0(X1,sz00)=sz00|~aElement0(X1)),inference(split_conjunct,[status(thm)],[174])).
% fof(177, plain,![X1]:![X2]:((~(aElement0(X1))|~(aElement0(X2)))|(~(sdtasdt0(X1,X2)=sz00)|(X1=sz00|X2=sz00))),inference(fof_nnf,[status(thm)],[28])).
% fof(178, plain,![X3]:![X4]:((~(aElement0(X3))|~(aElement0(X4)))|(~(sdtasdt0(X3,X4)=sz00)|(X3=sz00|X4=sz00))),inference(variable_rename,[status(thm)],[177])).
% cnf(179,plain,(X1=sz00|X2=sz00|sdtasdt0(X2,X1)!=sz00|~aElement0(X1)|~aElement0(X2)),inference(split_conjunct,[status(thm)],[178])).
% cnf(180,plain,(sz10!=sz00),inference(split_conjunct,[status(thm)],[29])).
% cnf(181,plain,(aElement0(sz00)),inference(split_conjunct,[status(thm)],[30])).
% cnf(189,negated_conjecture,(~aElementOf0(sdtasdt0(xx,sdtpldt0(xb,smndt0(sz10))),xI)),inference(split_conjunct,[status(thm)],[38])).
% cnf(217,plain,(aElement0(xb)|~aSet0(xJ)),inference(spm,[status(thm)],[79,141,theory(equality)])).
% cnf(218,plain,(aElement0(xa)|~aSet0(xI)),inference(spm,[status(thm)],[79,142,theory(equality)])).
% cnf(224,plain,(aElement0(xb)|$false),inference(rw,[status(thm)],[217,123,theory(equality)])).
% cnf(225,plain,(aElement0(xb)),inference(cn,[status(thm)],[224,theory(equality)])).
% cnf(226,plain,(aElement0(xa)|$false),inference(rw,[status(thm)],[218,125,theory(equality)])).
% cnf(227,plain,(aElement0(xa)),inference(cn,[status(thm)],[226,theory(equality)])).
% cnf(232,negated_conjecture,(~aElementOf0(sdtpldt0(xb,smndt0(sz10)),xI)|~aElement0(xx)),inference(spm,[status(thm)],[189,127,theory(equality)])).
% cnf(241,negated_conjecture,(~aElementOf0(sdtpldt0(xb,smndt0(sz10)),xI)|$false),inference(rw,[status(thm)],[232,139,theory(equality)])).
% cnf(242,negated_conjecture,(~aElementOf0(sdtpldt0(xb,smndt0(sz10)),xI)),inference(cn,[status(thm)],[241,theory(equality)])).
% cnf(387,plain,(aElement0(sdtasdt0(X1,X2))|~aSet0(X3)|~aIdeal0(X3)|~aElementOf0(X2,X3)|~aElement0(X1)),inference(spm,[status(thm)],[79,114,theory(equality)])).
% cnf(419,plain,(sdtpldt0(X1,sdtpldt0(X2,smndt0(sdtpldt0(X1,X2))))=sz00|~aElement0(sdtpldt0(X1,X2))|~aElement0(smndt0(sdtpldt0(X1,X2)))|~aElement0(X2)|~aElement0(X1)),inference(spm,[status(thm)],[154,54,theory(equality)])).
% cnf(428,plain,(sdtpldt0(X1,X2)=sdtpldt0(sz00,sdtpldt0(X1,X2))|~aElement0(X2)|~aElement0(X1)|~aElement0(sz00)),inference(spm,[status(thm)],[54,170,theory(equality)])).
% cnf(432,plain,(sdtpldt0(sz00,X2)=sdtpldt0(smndt0(X1),sdtpldt0(X1,X2))|~aElement0(X2)|~aElement0(X1)|~aElement0(smndt0(X1))),inference(spm,[status(thm)],[54,153,theory(equality)])).
% cnf(439,plain,(sdtpldt0(X1,X2)=sdtpldt0(sz00,sdtpldt0(X1,X2))|~aElement0(X2)|~aElement0(X1)|$false),inference(rw,[status(thm)],[428,181,theory(equality)])).
% cnf(440,plain,(sdtpldt0(X1,X2)=sdtpldt0(sz00,sdtpldt0(X1,X2))|~aElement0(X2)|~aElement0(X1)),inference(cn,[status(thm)],[439,theory(equality)])).
% cnf(446,plain,(sdtasdt0(X1,sdtasdt0(X2,X3))=sdtasdt0(X2,sdtasdt0(X3,X1))|~aElement0(sdtasdt0(X2,X3))|~aElement0(X1)|~aElement0(X3)|~aElement0(X2)),inference(spm,[status(thm)],[57,60,theory(equality)])).
% cnf(450,plain,(aElementOf0(sdtasdt0(X1,sdtasdt0(X2,X3)),xI)|~aElementOf0(X3,xI)|~aElement0(sdtasdt0(X1,X2))|~aElement0(X3)|~aElement0(X2)|~aElement0(X1)),inference(spm,[status(thm)],[127,60,theory(equality)])).
% cnf(456,plain,(sdtasdt0(X1,X2)=sdtasdt0(sz10,sdtasdt0(X1,X2))|~aElement0(X2)|~aElement0(X1)|~aElement0(sz10)),inference(spm,[status(thm)],[60,64,theory(equality)])).
% cnf(459,plain,(sdtasdt0(X1,X2)=sdtasdt0(X1,sdtasdt0(sz10,X2))|~aElement0(X2)|~aElement0(sz10)|~aElement0(X1)),inference(spm,[status(thm)],[60,65,theory(equality)])).
% cnf(468,plain,(sdtasdt0(X1,X2)=sdtasdt0(sz10,sdtasdt0(X1,X2))|~aElement0(X2)|~aElement0(X1)|$false),inference(rw,[status(thm)],[456,39,theory(equality)])).
% cnf(469,plain,(sdtasdt0(X1,X2)=sdtasdt0(sz10,sdtasdt0(X1,X2))|~aElement0(X2)|~aElement0(X1)),inference(cn,[status(thm)],[468,theory(equality)])).
% cnf(472,plain,(sdtasdt0(X1,X2)=sdtasdt0(X1,sdtasdt0(sz10,X2))|~aElement0(X2)|$false|~aElement0(X1)),inference(rw,[status(thm)],[459,39,theory(equality)])).
% cnf(473,plain,(sdtasdt0(X1,X2)=sdtasdt0(X1,sdtasdt0(sz10,X2))|~aElement0(X2)|~aElement0(X1)),inference(cn,[status(thm)],[472,theory(equality)])).
% cnf(482,plain,(sdtpldt0(sdtasdt0(sz00,X1),sz00)=sdtasdt0(sz00,sdtpldt0(X1,X2))|~aElement0(sz00)|~aElement0(X1)|~aElement0(X2)),inference(spm,[status(thm)],[70,175,theory(equality)])).
% cnf(485,plain,(sdtpldt0(sdtasdt0(sz10,X1),X2)=sdtasdt0(sz10,sdtpldt0(X1,X2))|~aElement0(sz10)|~aElement0(X1)|~aElement0(X2)),inference(spm,[status(thm)],[70,64,theory(equality)])).
% cnf(488,plain,(sdtpldt0(sdtasdt0(X1,X2),X1)=sdtasdt0(X1,sdtpldt0(X2,sz10))|~aElement0(X1)|~aElement0(X2)|~aElement0(sz10)),inference(spm,[status(thm)],[70,65,theory(equality)])).
% cnf(500,plain,(sdtpldt0(sdtasdt0(sz00,X1),sz00)=sdtasdt0(sz00,sdtpldt0(X1,X2))|$false|~aElement0(X1)|~aElement0(X2)),inference(rw,[status(thm)],[482,181,theory(equality)])).
% cnf(501,plain,(sdtpldt0(sdtasdt0(sz00,X1),sz00)=sdtasdt0(sz00,sdtpldt0(X1,X2))|~aElement0(X1)|~aElement0(X2)),inference(cn,[status(thm)],[500,theory(equality)])).
% cnf(502,plain,(sdtpldt0(sdtasdt0(sz10,X1),X2)=sdtasdt0(sz10,sdtpldt0(X1,X2))|$false|~aElement0(X1)|~aElement0(X2)),inference(rw,[status(thm)],[485,39,theory(equality)])).
% cnf(503,plain,(sdtpldt0(sdtasdt0(sz10,X1),X2)=sdtasdt0(sz10,sdtpldt0(X1,X2))|~aElement0(X1)|~aElement0(X2)),inference(cn,[status(thm)],[502,theory(equality)])).
% cnf(506,plain,(sdtpldt0(sdtasdt0(X1,X2),X1)=sdtasdt0(X1,sdtpldt0(X2,sz10))|~aElement0(X1)|~aElement0(X2)|$false),inference(rw,[status(thm)],[488,39,theory(equality)])).
% cnf(507,plain,(sdtpldt0(sdtasdt0(X1,X2),X1)=sdtasdt0(X1,sdtpldt0(X2,sz10))|~aElement0(X1)|~aElement0(X2)),inference(cn,[status(thm)],[506,theory(equality)])).
% cnf(1106,plain,(sdtasdt0(sz10,sz00)=sz00|~aElement0(X1)|~aElement0(sz00)),inference(spm,[status(thm)],[469,175,theory(equality)])).
% cnf(1141,plain,(sdtasdt0(sz10,sz00)=sz00|~aElement0(X1)|$false),inference(rw,[status(thm)],[1106,181,theory(equality)])).
% cnf(1142,plain,(sdtasdt0(sz10,sz00)=sz00|~aElement0(X1)),inference(cn,[status(thm)],[1141,theory(equality)])).
% cnf(1152,plain,(sdtasdt0(sz10,sz00)=sz00),inference(spm,[status(thm)],[1142,181,theory(equality)])).
% cnf(1166,plain,(sdtasdt0(sz00,sz10)=sz00|~aElement0(sz10)|~aElement0(sz00)),inference(spm,[status(thm)],[57,1152,theory(equality)])).
% cnf(1181,plain,(sdtasdt0(sz00,sz10)=sz00|$false|~aElement0(sz00)),inference(rw,[status(thm)],[1166,39,theory(equality)])).
% cnf(1182,plain,(sdtasdt0(sz00,sz10)=sz00|$false|$false),inference(rw,[status(thm)],[1181,181,theory(equality)])).
% cnf(1183,plain,(sdtasdt0(sz00,sz10)=sz00),inference(cn,[status(thm)],[1182,theory(equality)])).
% cnf(2379,plain,(sdtasdt0(X1,sdtasdt0(X2,sz10))=sdtasdt0(X1,X2)|~aElement0(X2)|~aElement0(X1)|~aElement0(sz10)),inference(spm,[status(thm)],[473,57,theory(equality)])).
% cnf(2395,plain,(sdtasdt0(X1,sdtasdt0(X2,sz10))=sdtasdt0(X1,X2)|~aElement0(X2)|~aElement0(X1)|$false),inference(rw,[status(thm)],[2379,39,theory(equality)])).
% cnf(2396,plain,(sdtasdt0(X1,sdtasdt0(X2,sz10))=sdtasdt0(X1,X2)|~aElement0(X2)|~aElement0(X1)),inference(cn,[status(thm)],[2395,theory(equality)])).
% cnf(2447,plain,(sdtasdt0(sz10,X1)=sdtasdt0(X1,sz10)|~aElement0(sz10)|~aElement0(X1)),inference(spm,[status(thm)],[469,2396,theory(equality)])).
% cnf(2491,plain,(sdtasdt0(sz10,X1)=sdtasdt0(X1,sz10)|$false|~aElement0(X1)),inference(rw,[status(thm)],[2447,39,theory(equality)])).
% cnf(2492,plain,(sdtasdt0(sz10,X1)=sdtasdt0(X1,sz10)|~aElement0(X1)),inference(cn,[status(thm)],[2491,theory(equality)])).
% cnf(2506,plain,(sz00=X1|sz00=sz10|sdtasdt0(sz10,X1)!=sz00|~aElement0(X1)|~aElement0(sz10)),inference(spm,[status(thm)],[179,2492,theory(equality)])).
% cnf(2531,plain,(aElement0(sdtasdt0(X1,sz10))|~aElement0(X1)|~aElement0(sz10)),inference(spm,[status(thm)],[48,2492,theory(equality)])).
% cnf(2566,plain,(sz00=X1|sz00=sz10|sdtasdt0(sz10,X1)!=sz00|~aElement0(X1)|$false),inference(rw,[status(thm)],[2506,39,theory(equality)])).
% cnf(2567,plain,(sz00=X1|sz00=sz10|sdtasdt0(sz10,X1)!=sz00|~aElement0(X1)),inference(cn,[status(thm)],[2566,theory(equality)])).
% cnf(2568,plain,(sz00=X1|sdtasdt0(sz10,X1)!=sz00|~aElement0(X1)),inference(sr,[status(thm)],[2567,180,theory(equality)])).
% cnf(2614,plain,(aElement0(sdtasdt0(X1,sz10))|~aElement0(X1)|$false),inference(rw,[status(thm)],[2531,39,theory(equality)])).
% cnf(2615,plain,(aElement0(sdtasdt0(X1,sz10))|~aElement0(X1)),inference(cn,[status(thm)],[2614,theory(equality)])).
% cnf(2754,plain,(sz00=sdtasdt0(X1,sz10)|sdtasdt0(sz10,X1)!=sz00|~aElement0(sdtasdt0(X1,sz10))|~aElement0(X1)|~aElement0(sz10)),inference(spm,[status(thm)],[2568,2396,theory(equality)])).
% cnf(2769,plain,(sz00=sdtasdt0(X1,sz10)|sdtasdt0(sz10,X1)!=sz00|~aElement0(sdtasdt0(X1,sz10))|~aElement0(X1)|$false),inference(rw,[status(thm)],[2754,39,theory(equality)])).
% cnf(2770,plain,(sz00=sdtasdt0(X1,sz10)|sdtasdt0(sz10,X1)!=sz00|~aElement0(sdtasdt0(X1,sz10))|~aElement0(X1)),inference(cn,[status(thm)],[2769,theory(equality)])).
% cnf(2896,plain,(sdtasdt0(X1,sz10)=sz00|sdtasdt0(sz10,X1)!=sz00|~aElement0(X1)),inference(csr,[status(thm)],[2770,2615])).
% cnf(2911,plain,(sdtasdt0(X1,sz10)=sz00|X1!=sz00|~aElement0(X1)),inference(spm,[status(thm)],[2896,64,theory(equality)])).
% cnf(2957,plain,(sdtasdt0(sz10,X1)=sz00|~aElement0(X1)|~aElement0(sz10)|X1!=sz00),inference(spm,[status(thm)],[57,2911,theory(equality)])).
% cnf(3029,plain,(sdtasdt0(sz10,X1)=sz00|~aElement0(X1)|$false|X1!=sz00),inference(rw,[status(thm)],[2957,39,theory(equality)])).
% cnf(3030,plain,(sdtasdt0(sz10,X1)=sz00|~aElement0(X1)|X1!=sz00),inference(cn,[status(thm)],[3029,theory(equality)])).
% cnf(3076,plain,(sdtasdt0(sz00,X2)=sdtasdt0(sz10,sdtasdt0(X1,X2))|~aElement0(X2)|~aElement0(X1)|~aElement0(sz10)|X1!=sz00),inference(spm,[status(thm)],[60,3030,theory(equality)])).
% cnf(3153,plain,(sdtasdt0(sz00,X2)=sdtasdt0(sz10,sdtasdt0(X1,X2))|~aElement0(X2)|~aElement0(X1)|$false|X1!=sz00),inference(rw,[status(thm)],[3076,39,theory(equality)])).
% cnf(3154,plain,(sdtasdt0(sz00,X2)=sdtasdt0(sz10,sdtasdt0(X1,X2))|~aElement0(X2)|~aElement0(X1)|X1!=sz00),inference(cn,[status(thm)],[3153,theory(equality)])).
% cnf(4078,plain,(aElement0(sdtasdt0(X1,X2))|~aIdeal0(X3)|~aElementOf0(X2,X3)|~aElement0(X1)),inference(csr,[status(thm)],[387,112])).
% cnf(4092,plain,(aElement0(sdtasdt0(X1,xa))|~aIdeal0(xI)|~aElement0(X1)),inference(spm,[status(thm)],[4078,142,theory(equality)])).
% cnf(4137,plain,(aElement0(sdtasdt0(X1,xa))|$false|~aElement0(X1)),inference(rw,[status(thm)],[4092,124,theory(equality)])).
% cnf(4138,plain,(aElement0(sdtasdt0(X1,xa))|~aElement0(X1)),inference(cn,[status(thm)],[4137,theory(equality)])).
% cnf(4636,plain,(aElement0(smndt0(xa))|~aElement0(smndt0(sz10))|~aElement0(xa)),inference(spm,[status(thm)],[4138,75,theory(equality)])).
% cnf(4640,plain,(aElement0(sdtasdt0(xa,X1))|~aElement0(X1)|~aElement0(xa)),inference(spm,[status(thm)],[4138,57,theory(equality)])).
% cnf(4648,plain,(aElement0(smndt0(xa))|~aElement0(smndt0(sz10))|$false),inference(rw,[status(thm)],[4636,227,theory(equality)])).
% cnf(4649,plain,(aElement0(smndt0(xa))|~aElement0(smndt0(sz10))),inference(cn,[status(thm)],[4648,theory(equality)])).
% cnf(4661,plain,(aElement0(sdtasdt0(xa,X1))|~aElement0(X1)|$false),inference(rw,[status(thm)],[4640,227,theory(equality)])).
% cnf(4662,plain,(aElement0(sdtasdt0(xa,X1))|~aElement0(X1)),inference(cn,[status(thm)],[4661,theory(equality)])).
% cnf(4734,plain,(aElement0(smndt0(xa))|~aElement0(sz10)),inference(spm,[status(thm)],[4649,42,theory(equality)])).
% cnf(4735,plain,(aElement0(smndt0(xa))|$false),inference(rw,[status(thm)],[4734,39,theory(equality)])).
% cnf(4736,plain,(aElement0(smndt0(xa))),inference(cn,[status(thm)],[4735,theory(equality)])).
% cnf(4939,plain,(sdtasdt0(sz10,sz00)=sdtasdt0(sz00,sz00)|X1!=sz00|~aElement0(sz00)|~aElement0(X1)),inference(spm,[status(thm)],[3154,176,theory(equality)])).
% cnf(5026,plain,(sz00=sdtasdt0(sz00,sz00)|X1!=sz00|~aElement0(sz00)|~aElement0(X1)),inference(rw,[status(thm)],[4939,1152,theory(equality)])).
% cnf(5027,plain,(sz00=sdtasdt0(sz00,sz00)|X1!=sz00|$false|~aElement0(X1)),inference(rw,[status(thm)],[5026,181,theory(equality)])).
% cnf(5028,plain,(sz00=sdtasdt0(sz00,sz00)|X1!=sz00|~aElement0(X1)),inference(cn,[status(thm)],[5027,theory(equality)])).
% cnf(5715,plain,(sdtasdt0(sz00,sz00)=sz00),inference(spm,[status(thm)],[5028,181,theory(equality)])).
% cnf(5762,plain,(sdtasdt0(sz00,X1)=sdtasdt0(sz00,sdtasdt0(sz00,X1))|~aElement0(X1)|~aElement0(sz00)),inference(spm,[status(thm)],[60,5715,theory(equality)])).
% cnf(5814,plain,(sdtasdt0(sz00,X1)=sdtasdt0(sz00,sdtasdt0(sz00,X1))|~aElement0(X1)|$false),inference(rw,[status(thm)],[5762,181,theory(equality)])).
% cnf(5815,plain,(sdtasdt0(sz00,X1)=sdtasdt0(sz00,sdtasdt0(sz00,X1))|~aElement0(X1)),inference(cn,[status(thm)],[5814,theory(equality)])).
% cnf(6176,plain,(sdtpldt0(X1,sdtpldt0(X2,smndt0(sdtpldt0(X1,X2))))=sz00|~aElement0(sdtpldt0(X1,X2))|~aElement0(X2)|~aElement0(X1)),inference(csr,[status(thm)],[419,42])).
% cnf(6177,plain,(sdtpldt0(X1,sdtpldt0(X2,smndt0(sdtpldt0(X1,X2))))=sz00|~aElement0(X2)|~aElement0(X1)),inference(csr,[status(thm)],[6176,45])).
% cnf(7429,plain,(sdtpldt0(sz00,sz10)=sz10|~aElement0(xb)|~aElement0(xa)),inference(spm,[status(thm)],[440,140,theory(equality)])).
% cnf(7502,plain,(sdtpldt0(sz00,sz10)=sz10|$false|~aElement0(xa)),inference(rw,[status(thm)],[7429,225,theory(equality)])).
% cnf(7503,plain,(sdtpldt0(sz00,sz10)=sz10|$false|$false),inference(rw,[status(thm)],[7502,227,theory(equality)])).
% cnf(7504,plain,(sdtpldt0(sz00,sz10)=sz10),inference(cn,[status(thm)],[7503,theory(equality)])).
% cnf(8588,plain,(sdtpldt0(smndt0(X1),sdtpldt0(X1,X2))=sdtpldt0(sz00,X2)|~aElement0(X2)|~aElement0(X1)),inference(csr,[status(thm)],[432,42])).
% cnf(8625,plain,(sdtpldt0(smndt0(xa),sz10)=sdtpldt0(sz00,xb)|~aElement0(xb)|~aElement0(xa)),inference(spm,[status(thm)],[8588,140,theory(equality)])).
% cnf(8674,plain,(sdtpldt0(smndt0(xa),sz10)=sdtpldt0(sz00,xb)|$false|~aElement0(xa)),inference(rw,[status(thm)],[8625,225,theory(equality)])).
% cnf(8675,plain,(sdtpldt0(smndt0(xa),sz10)=sdtpldt0(sz00,xb)|$false|$false),inference(rw,[status(thm)],[8674,227,theory(equality)])).
% cnf(8676,plain,(sdtpldt0(smndt0(xa),sz10)=sdtpldt0(sz00,xb)),inference(cn,[status(thm)],[8675,theory(equality)])).
% cnf(8852,plain,(sdtpldt0(sz00,xb)=sdtpldt0(sz10,smndt0(xa))|~aElement0(sz10)|~aElement0(smndt0(xa))),inference(spm,[status(thm)],[51,8676,theory(equality)])).
% cnf(8862,plain,(sdtpldt0(sz00,sdtpldt0(sz00,xb))=sdtpldt0(sz00,xb)|~aElement0(sz10)|~aElement0(smndt0(xa))),inference(spm,[status(thm)],[440,8676,theory(equality)])).
% cnf(8874,plain,(sdtpldt0(sz00,xb)=sdtpldt0(sz10,smndt0(xa))|$false|~aElement0(smndt0(xa))),inference(rw,[status(thm)],[8852,39,theory(equality)])).
% cnf(8875,plain,(sdtpldt0(sz00,xb)=sdtpldt0(sz10,smndt0(xa))|$false|$false),inference(rw,[status(thm)],[8874,4736,theory(equality)])).
% cnf(8876,plain,(sdtpldt0(sz00,xb)=sdtpldt0(sz10,smndt0(xa))),inference(cn,[status(thm)],[8875,theory(equality)])).
% cnf(8889,plain,(sdtpldt0(sz00,sdtpldt0(sz00,xb))=sdtpldt0(sz00,xb)|$false|~aElement0(smndt0(xa))),inference(rw,[status(thm)],[8862,39,theory(equality)])).
% cnf(8890,plain,(sdtpldt0(sz00,sdtpldt0(sz00,xb))=sdtpldt0(sz00,xb)|$false|$false),inference(rw,[status(thm)],[8889,4736,theory(equality)])).
% cnf(8891,plain,(sdtpldt0(sz00,sdtpldt0(sz00,xb))=sdtpldt0(sz00,xb)),inference(cn,[status(thm)],[8890,theory(equality)])).
% cnf(10481,plain,(sdtasdt0(X1,sdtasdt0(X2,X3))=sdtasdt0(X2,sdtasdt0(X3,X1))|~aElement0(X1)|~aElement0(X3)|~aElement0(X2)),inference(csr,[status(thm)],[446,48])).
% cnf(10493,plain,(sdtasdt0(X1,sdtasdt0(sz00,sz00))=sdtasdt0(sz00,X1)|~aElement0(X1)|~aElement0(sz00)),inference(spm,[status(thm)],[5815,10481,theory(equality)])).
% cnf(10714,plain,(sdtasdt0(X1,sz00)=sdtasdt0(sz00,X1)|~aElement0(X1)|~aElement0(sz00)),inference(rw,[status(thm)],[10493,5715,theory(equality)])).
% cnf(10715,plain,(sdtasdt0(X1,sz00)=sdtasdt0(sz00,X1)|~aElement0(X1)|$false),inference(rw,[status(thm)],[10714,181,theory(equality)])).
% cnf(10716,plain,(sdtasdt0(X1,sz00)=sdtasdt0(sz00,X1)|~aElement0(X1)),inference(cn,[status(thm)],[10715,theory(equality)])).
% cnf(11405,plain,(aElement0(sdtasdt0(sz00,xa))|~aElement0(sz00)|~aElement0(xa)),inference(spm,[status(thm)],[4662,10716,theory(equality)])).
% cnf(11573,plain,(aElement0(sdtasdt0(sz00,xa))|$false|~aElement0(xa)),inference(rw,[status(thm)],[11405,181,theory(equality)])).
% cnf(11574,plain,(aElement0(sdtasdt0(sz00,xa))|$false|$false),inference(rw,[status(thm)],[11573,227,theory(equality)])).
% cnf(11575,plain,(aElement0(sdtasdt0(sz00,xa))),inference(cn,[status(thm)],[11574,theory(equality)])).
% cnf(11890,plain,(aElementOf0(sdtasdt0(X1,sdtasdt0(X2,X3)),xI)|~aElementOf0(X3,xI)|~aElement0(X3)|~aElement0(X2)|~aElement0(X1)),inference(csr,[status(thm)],[450,48])).
% cnf(13156,plain,(sdtpldt0(sz00,xb)=xb|~aElement0(xb)),inference(spm,[status(thm)],[8891,170,theory(equality)])).
% cnf(13234,plain,(sdtpldt0(sz00,xb)=xb|$false),inference(rw,[status(thm)],[13156,225,theory(equality)])).
% cnf(13235,plain,(sdtpldt0(sz00,xb)=xb),inference(cn,[status(thm)],[13234,theory(equality)])).
% cnf(13414,plain,(sdtpldt0(sz10,smndt0(xa))=xb),inference(rw,[status(thm)],[8876,13235,theory(equality)])).
% cnf(13492,plain,(sdtpldt0(smndt0(sz10),xb)=sdtpldt0(sz00,smndt0(xa))|~aElement0(smndt0(xa))|~aElement0(sz10)),inference(spm,[status(thm)],[8588,13414,theory(equality)])).
% cnf(13524,plain,(sdtpldt0(smndt0(sz10),xb)=sdtpldt0(sz00,smndt0(xa))|$false|~aElement0(sz10)),inference(rw,[status(thm)],[13492,4736,theory(equality)])).
% cnf(13525,plain,(sdtpldt0(smndt0(sz10),xb)=sdtpldt0(sz00,smndt0(xa))|$false|$false),inference(rw,[status(thm)],[13524,39,theory(equality)])).
% cnf(13526,plain,(sdtpldt0(smndt0(sz10),xb)=sdtpldt0(sz00,smndt0(xa))),inference(cn,[status(thm)],[13525,theory(equality)])).
% cnf(17224,plain,(sdtasdt0(sz00,sz10)=sdtpldt0(sdtasdt0(sz00,xa),sz00)|~aElement0(xa)|~aElement0(xb)),inference(spm,[status(thm)],[501,140,theory(equality)])).
% cnf(17386,plain,(sz00=sdtpldt0(sdtasdt0(sz00,xa),sz00)|~aElement0(xa)|~aElement0(xb)),inference(rw,[status(thm)],[17224,1183,theory(equality)])).
% cnf(17387,plain,(sz00=sdtpldt0(sdtasdt0(sz00,xa),sz00)|$false|~aElement0(xb)),inference(rw,[status(thm)],[17386,227,theory(equality)])).
% cnf(17388,plain,(sz00=sdtpldt0(sdtasdt0(sz00,xa),sz00)|$false|$false),inference(rw,[status(thm)],[17387,225,theory(equality)])).
% cnf(17389,plain,(sz00=sdtpldt0(sdtasdt0(sz00,xa),sz00)),inference(cn,[status(thm)],[17388,theory(equality)])).
% cnf(18280,plain,(sz00=sdtasdt0(sz00,xa)|~aElement0(sdtasdt0(sz00,xa))),inference(spm,[status(thm)],[171,17389,theory(equality)])).
% cnf(18366,plain,(sz00=sdtasdt0(sz00,xa)|$false),inference(rw,[status(thm)],[18280,11575,theory(equality)])).
% cnf(18367,plain,(sz00=sdtasdt0(sz00,xa)),inference(cn,[status(thm)],[18366,theory(equality)])).
% cnf(20500,plain,(sdtpldt0(sdtasdt0(sz00,X1),X1)=sdtasdt0(X1,sdtpldt0(sz00,sz10))|~aElement0(X1)|~aElement0(sz00)),inference(spm,[status(thm)],[507,10716,theory(equality)])).
% cnf(20609,plain,(sdtpldt0(sdtasdt0(sz00,X1),X1)=sdtasdt0(X1,sz10)|~aElement0(X1)|~aElement0(sz00)),inference(rw,[status(thm)],[20500,7504,theory(equality)])).
% cnf(20610,plain,(sdtpldt0(sdtasdt0(sz00,X1),X1)=sdtasdt0(X1,sz10)|~aElement0(X1)|$false),inference(rw,[status(thm)],[20609,181,theory(equality)])).
% cnf(20611,plain,(sdtpldt0(sdtasdt0(sz00,X1),X1)=sdtasdt0(X1,sz10)|~aElement0(X1)),inference(cn,[status(thm)],[20610,theory(equality)])).
% cnf(26395,plain,(sdtpldt0(sz00,xa)=sdtasdt0(xa,sz10)|~aElement0(xa)),inference(spm,[status(thm)],[20611,18367,theory(equality)])).
% cnf(26542,plain,(sdtpldt0(sz00,xa)=sdtasdt0(xa,sz10)|$false),inference(rw,[status(thm)],[26395,227,theory(equality)])).
% cnf(26543,plain,(sdtpldt0(sz00,xa)=sdtasdt0(xa,sz10)),inference(cn,[status(thm)],[26542,theory(equality)])).
% cnf(26815,plain,(sdtpldt0(sz00,xa)=xa|~aElement0(xa)),inference(spm,[status(thm)],[65,26543,theory(equality)])).
% cnf(26959,plain,(sdtpldt0(sz00,xa)=xa|$false),inference(rw,[status(thm)],[26815,227,theory(equality)])).
% cnf(26960,plain,(sdtpldt0(sz00,xa)=xa),inference(cn,[status(thm)],[26959,theory(equality)])).
% cnf(26996,plain,(sdtpldt0(sz00,sdtpldt0(xa,smndt0(xa)))=sz00|~aElement0(xa)|~aElement0(sz00)),inference(spm,[status(thm)],[6177,26960,theory(equality)])).
% cnf(27002,plain,(sdtasdt0(sz10,xa)=sdtpldt0(sdtasdt0(sz10,sz00),xa)|~aElement0(sz00)|~aElement0(xa)),inference(spm,[status(thm)],[503,26960,theory(equality)])).
% cnf(27049,plain,(sdtpldt0(sz00,sdtpldt0(xa,smndt0(xa)))=sz00|$false|~aElement0(sz00)),inference(rw,[status(thm)],[26996,227,theory(equality)])).
% cnf(27050,plain,(sdtpldt0(sz00,sdtpldt0(xa,smndt0(xa)))=sz00|$false|$false),inference(rw,[status(thm)],[27049,181,theory(equality)])).
% cnf(27051,plain,(sdtpldt0(sz00,sdtpldt0(xa,smndt0(xa)))=sz00),inference(cn,[status(thm)],[27050,theory(equality)])).
% cnf(27072,plain,(sdtasdt0(sz10,xa)=xa|~aElement0(sz00)|~aElement0(xa)),inference(rw,[status(thm)],[inference(rw,[status(thm)],[27002,1152,theory(equality)]),26960,theory(equality)])).
% cnf(27073,plain,(sdtasdt0(sz10,xa)=xa|$false|~aElement0(xa)),inference(rw,[status(thm)],[27072,181,theory(equality)])).
% cnf(27074,plain,(sdtasdt0(sz10,xa)=xa|$false|$false),inference(rw,[status(thm)],[27073,227,theory(equality)])).
% cnf(27075,plain,(sdtasdt0(sz10,xa)=xa),inference(cn,[status(thm)],[27074,theory(equality)])).
% cnf(27453,plain,(aElementOf0(sdtasdt0(X1,xa),xI)|~aElementOf0(xa,xI)|~aElement0(xa)|~aElement0(sz10)|~aElement0(X1)),inference(spm,[status(thm)],[11890,27075,theory(equality)])).
% cnf(27575,plain,(aElementOf0(sdtasdt0(X1,xa),xI)|$false|~aElement0(xa)|~aElement0(sz10)|~aElement0(X1)),inference(rw,[status(thm)],[27453,142,theory(equality)])).
% cnf(27576,plain,(aElementOf0(sdtasdt0(X1,xa),xI)|$false|$false|~aElement0(sz10)|~aElement0(X1)),inference(rw,[status(thm)],[27575,227,theory(equality)])).
% cnf(27577,plain,(aElementOf0(sdtasdt0(X1,xa),xI)|$false|$false|$false|~aElement0(X1)),inference(rw,[status(thm)],[27576,39,theory(equality)])).
% cnf(27578,plain,(aElementOf0(sdtasdt0(X1,xa),xI)|~aElement0(X1)),inference(cn,[status(thm)],[27577,theory(equality)])).
% cnf(32462,plain,(aElementOf0(smndt0(xa),xI)|~aElement0(smndt0(sz10))|~aElement0(xa)),inference(spm,[status(thm)],[27578,75,theory(equality)])).
% cnf(32499,plain,(aElementOf0(smndt0(xa),xI)|~aElement0(smndt0(sz10))|$false),inference(rw,[status(thm)],[32462,227,theory(equality)])).
% cnf(32500,plain,(aElementOf0(smndt0(xa),xI)|~aElement0(smndt0(sz10))),inference(cn,[status(thm)],[32499,theory(equality)])).
% cnf(56146,plain,(sz00=sdtpldt0(xa,smndt0(xa))|~aElement0(smndt0(xa))|~aElement0(xa)),inference(spm,[status(thm)],[440,27051,theory(equality)])).
% cnf(56281,plain,(sz00=sdtpldt0(xa,smndt0(xa))|$false|~aElement0(xa)),inference(rw,[status(thm)],[56146,4736,theory(equality)])).
% cnf(56282,plain,(sz00=sdtpldt0(xa,smndt0(xa))|$false|$false),inference(rw,[status(thm)],[56281,227,theory(equality)])).
% cnf(56283,plain,(sz00=sdtpldt0(xa,smndt0(xa))),inference(cn,[status(thm)],[56282,theory(equality)])).
% cnf(56297,plain,(sdtpldt0(smndt0(xa),sz00)=sdtpldt0(sz00,smndt0(xa))|~aElement0(smndt0(xa))|~aElement0(xa)),inference(spm,[status(thm)],[8588,56283,theory(equality)])).
% cnf(56360,plain,(sdtpldt0(smndt0(xa),sz00)=sdtpldt0(sz00,smndt0(xa))|$false|~aElement0(xa)),inference(rw,[status(thm)],[56297,4736,theory(equality)])).
% cnf(56361,plain,(sdtpldt0(smndt0(xa),sz00)=sdtpldt0(sz00,smndt0(xa))|$false|$false),inference(rw,[status(thm)],[56360,227,theory(equality)])).
% cnf(56362,plain,(sdtpldt0(smndt0(xa),sz00)=sdtpldt0(sz00,smndt0(xa))),inference(cn,[status(thm)],[56361,theory(equality)])).
% cnf(57411,plain,(sdtpldt0(sz00,smndt0(xa))=smndt0(xa)|~aElement0(smndt0(xa))),inference(spm,[status(thm)],[171,56362,theory(equality)])).
% cnf(57534,plain,(sdtpldt0(sz00,smndt0(xa))=smndt0(xa)|$false),inference(rw,[status(thm)],[57411,4736,theory(equality)])).
% cnf(57535,plain,(sdtpldt0(sz00,smndt0(xa))=smndt0(xa)),inference(cn,[status(thm)],[57534,theory(equality)])).
% cnf(57608,plain,(sdtpldt0(smndt0(sz10),xb)=smndt0(xa)),inference(rw,[status(thm)],[13526,57535,theory(equality)])).
% cnf(57746,plain,(smndt0(xa)=sdtpldt0(xb,smndt0(sz10))|~aElement0(xb)|~aElement0(smndt0(sz10))),inference(spm,[status(thm)],[51,57608,theory(equality)])).
% cnf(57795,plain,(smndt0(xa)=sdtpldt0(xb,smndt0(sz10))|$false|~aElement0(smndt0(sz10))),inference(rw,[status(thm)],[57746,225,theory(equality)])).
% cnf(57796,plain,(smndt0(xa)=sdtpldt0(xb,smndt0(sz10))|~aElement0(smndt0(sz10))),inference(cn,[status(thm)],[57795,theory(equality)])).
% cnf(59643,negated_conjecture,(~aElementOf0(smndt0(xa),xI)|~aElement0(smndt0(sz10))),inference(spm,[status(thm)],[242,57796,theory(equality)])).
% cnf(59787,negated_conjecture,(~aElement0(smndt0(sz10))),inference(csr,[status(thm)],[59643,32500])).
% cnf(59788,negated_conjecture,(~aElement0(sz10)),inference(spm,[status(thm)],[59787,42,theory(equality)])).
% cnf(59789,negated_conjecture,($false),inference(rw,[status(thm)],[59788,39,theory(equality)])).
% cnf(59790,negated_conjecture,($false),inference(cn,[status(thm)],[59789,theory(equality)])).
% cnf(59791,negated_conjecture,($false),59790,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 2009
% # ...of these trivial : 117
% # ...subsumed : 1141
% # ...remaining for further processing: 751
% # Other redundant clauses eliminated : 8
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 49
% # Backward-rewritten : 77
% # Generated clauses : 21401
% # ...of the previous two non-trivial : 17499
% # Contextual simplify-reflections : 260
% # Paramodulations : 21381
% # Factorizations : 0
% # Equation resolutions : 20
% # Current number of processed clauses: 549
% # Positive orientable unit clauses: 112
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 8
% # Non-unit-clauses : 429
% # Current number of unprocessed clauses: 14241
% # ...number of literals in the above : 67861
% # Clause-clause subsumption calls (NU) : 11869
% # Rec. Clause-clause subsumption calls : 8948
% # Unit Clause-clause subsumption calls : 99
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 30
% # Indexed BW rewrite successes : 25
% # Backwards rewriting index: 537 leaves, 1.37+/-1.387 terms/leaf
% # Paramod-from index: 336 leaves, 1.06+/-0.282 terms/leaf
% # Paramod-into index: 470 leaves, 1.21+/-0.717 terms/leaf
% # -------------------------------------------------
% # User time : 0.836 s
% # System time : 0.033 s
% # Total time : 0.869 s
% # Maximum resident set size: 0 pages
% PrfWatch: 1.66 CPU 1.77 WC
% FINAL PrfWatch: 1.66 CPU 1.77 WC
% SZS output end Solution for /tmp/SystemOnTPTP5230/RNG097+2.tptp
%
%------------------------------------------------------------------------------