%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : NUM541+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 : 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 19:59:09 EST 2010
% Result : Theorem 2.18s
% Output : Solution 2.18s
% 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/SystemOnTPTP16039/NUM541+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP16039/NUM541+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP16039/NUM541+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 16135
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.00 WC
% # Preprocessing time : 0.022 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(2, axiom,![X1]:(aElementOf0(X1,szNzAzT0)=>~(X1=szszuzczcdt0(X1))),file('/tmp/SRASS.s.p', mNatNSucc)).
% fof(3, axiom,(aElementOf0(xm,szNzAzT0)&aElementOf0(xn,szNzAzT0)),file('/tmp/SRASS.s.p', m__1936)).
% fof(4, axiom,![X1]:(aElementOf0(X1,szNzAzT0)=>(aElementOf0(szszuzczcdt0(X1),szNzAzT0)&~(szszuzczcdt0(X1)=sz00))),file('/tmp/SRASS.s.p', mSuccNum)).
% fof(5, axiom,![X1]:(aElementOf0(X1,szNzAzT0)=>(X1=sz00|?[X2]:(aElementOf0(X2,szNzAzT0)&X1=szszuzczcdt0(X2)))),file('/tmp/SRASS.s.p', mNatExtra)).
% fof(6, axiom,![X1]:(aElementOf0(X1,szNzAzT0)=>![X2]:(X2=slbdtrb0(X1)<=>(aSet0(X2)&![X3]:(aElementOf0(X3,X2)<=>(aElementOf0(X3,szNzAzT0)&sdtlseqdt0(szszuzczcdt0(X3),X1)))))),file('/tmp/SRASS.s.p', mDefSeg)).
% fof(8, axiom,![X1]:![X2]:((aElementOf0(X1,szNzAzT0)&aElementOf0(X2,szNzAzT0))=>(sdtlseqdt0(X1,X2)<=>sdtlseqdt0(szszuzczcdt0(X1),szszuzczcdt0(X2)))),file('/tmp/SRASS.s.p', mSuccLess)).
% fof(9, axiom,![X1]:(aElementOf0(X1,szNzAzT0)=>sdtlseqdt0(X1,szszuzczcdt0(X1))),file('/tmp/SRASS.s.p', mLessSucc)).
% fof(10, axiom,![X1]:![X2]:((aElementOf0(X1,szNzAzT0)&aElementOf0(X2,szNzAzT0))=>(sdtlseqdt0(X1,X2)|sdtlseqdt0(szszuzczcdt0(X2),X1))),file('/tmp/SRASS.s.p', mLessTotal)).
% fof(11, axiom,![X1]:![X2]:((aElementOf0(X1,szNzAzT0)&aElementOf0(X2,szNzAzT0))=>((sdtlseqdt0(X1,X2)&sdtlseqdt0(X2,X1))=>X1=X2)),file('/tmp/SRASS.s.p', mLessASymm)).
% fof(14, axiom,![X1]:![X2]:![X3]:(((aElementOf0(X1,szNzAzT0)&aElementOf0(X2,szNzAzT0))&aElementOf0(X3,szNzAzT0))=>((sdtlseqdt0(X1,X2)&sdtlseqdt0(X2,X3))=>sdtlseqdt0(X1,X3))),file('/tmp/SRASS.s.p', mLessTrans)).
% fof(15, axiom,aElementOf0(sz00,szNzAzT0),file('/tmp/SRASS.s.p', mZeroNum)).
% fof(16, axiom,![X1]:(aElementOf0(X1,szNzAzT0)=>~(sdtlseqdt0(szszuzczcdt0(X1),sz00))),file('/tmp/SRASS.s.p', mNoScLessZr)).
% fof(17, axiom,slbdtrb0(sz00)=slcrc0,file('/tmp/SRASS.s.p', mSegZero)).
% fof(18, axiom,![X1]:(X1=slcrc0<=>(aSet0(X1)&~(?[X2]:aElementOf0(X2,X1)))),file('/tmp/SRASS.s.p', mDefEmp)).
% fof(22, axiom,![X1]:(aElementOf0(X1,szNzAzT0)=>sdtlseqdt0(sz00,X1)),file('/tmp/SRASS.s.p', mZeroLess)).
% fof(24, axiom,![X1]:(aSet0(X1)=>aSubsetOf0(X1,X1)),file('/tmp/SRASS.s.p', mSubRefl)).
% fof(32, axiom,![X1]:((aSubsetOf0(X1,szNzAzT0)&~(X1=slcrc0))=>![X2]:(X2=szmzizndt0(X1)<=>(aElementOf0(X2,X1)&![X3]:(aElementOf0(X3,X1)=>sdtlseqdt0(X2,X3))))),file('/tmp/SRASS.s.p', mDefMin)).
% fof(40, axiom,(aSet0(szNzAzT0)&isCountable0(szNzAzT0)),file('/tmp/SRASS.s.p', mNATSet)).
% fof(54, conjecture,(aElementOf0(xm,slbdtrb0(szszuzczcdt0(xn)))<=>(aElementOf0(xm,slbdtrb0(xn))|xm=xn)),file('/tmp/SRASS.s.p', m__)).
% fof(55, negated_conjecture,~((aElementOf0(xm,slbdtrb0(szszuzczcdt0(xn)))<=>(aElementOf0(xm,slbdtrb0(xn))|xm=xn))),inference(assume_negation,[status(cth)],[54])).
% fof(56, plain,![X1]:(aElementOf0(X1,szNzAzT0)=>~(sdtlseqdt0(szszuzczcdt0(X1),sz00))),inference(fof_simplification,[status(thm)],[16,theory(equality)])).
% fof(69, plain,![X1]:(~(aElementOf0(X1,szNzAzT0))|~(X1=szszuzczcdt0(X1))),inference(fof_nnf,[status(thm)],[2])).
% fof(70, plain,![X2]:(~(aElementOf0(X2,szNzAzT0))|~(X2=szszuzczcdt0(X2))),inference(variable_rename,[status(thm)],[69])).
% cnf(71,plain,(X1!=szszuzczcdt0(X1)|~aElementOf0(X1,szNzAzT0)),inference(split_conjunct,[status(thm)],[70])).
% cnf(72,plain,(aElementOf0(xn,szNzAzT0)),inference(split_conjunct,[status(thm)],[3])).
% cnf(73,plain,(aElementOf0(xm,szNzAzT0)),inference(split_conjunct,[status(thm)],[3])).
% fof(74, plain,![X1]:(~(aElementOf0(X1,szNzAzT0))|(aElementOf0(szszuzczcdt0(X1),szNzAzT0)&~(szszuzczcdt0(X1)=sz00))),inference(fof_nnf,[status(thm)],[4])).
% fof(75, plain,![X2]:(~(aElementOf0(X2,szNzAzT0))|(aElementOf0(szszuzczcdt0(X2),szNzAzT0)&~(szszuzczcdt0(X2)=sz00))),inference(variable_rename,[status(thm)],[74])).
% fof(76, plain,![X2]:((aElementOf0(szszuzczcdt0(X2),szNzAzT0)|~(aElementOf0(X2,szNzAzT0)))&(~(szszuzczcdt0(X2)=sz00)|~(aElementOf0(X2,szNzAzT0)))),inference(distribute,[status(thm)],[75])).
% cnf(78,plain,(aElementOf0(szszuzczcdt0(X1),szNzAzT0)|~aElementOf0(X1,szNzAzT0)),inference(split_conjunct,[status(thm)],[76])).
% fof(79, plain,![X1]:(~(aElementOf0(X1,szNzAzT0))|(X1=sz00|?[X2]:(aElementOf0(X2,szNzAzT0)&X1=szszuzczcdt0(X2)))),inference(fof_nnf,[status(thm)],[5])).
% fof(80, plain,![X3]:(~(aElementOf0(X3,szNzAzT0))|(X3=sz00|?[X4]:(aElementOf0(X4,szNzAzT0)&X3=szszuzczcdt0(X4)))),inference(variable_rename,[status(thm)],[79])).
% fof(81, plain,![X3]:(~(aElementOf0(X3,szNzAzT0))|(X3=sz00|(aElementOf0(esk1_1(X3),szNzAzT0)&X3=szszuzczcdt0(esk1_1(X3))))),inference(skolemize,[status(esa)],[80])).
% fof(82, plain,![X3]:(((aElementOf0(esk1_1(X3),szNzAzT0)|X3=sz00)|~(aElementOf0(X3,szNzAzT0)))&((X3=szszuzczcdt0(esk1_1(X3))|X3=sz00)|~(aElementOf0(X3,szNzAzT0)))),inference(distribute,[status(thm)],[81])).
% cnf(83,plain,(X1=sz00|X1=szszuzczcdt0(esk1_1(X1))|~aElementOf0(X1,szNzAzT0)),inference(split_conjunct,[status(thm)],[82])).
% cnf(84,plain,(X1=sz00|aElementOf0(esk1_1(X1),szNzAzT0)|~aElementOf0(X1,szNzAzT0)),inference(split_conjunct,[status(thm)],[82])).
% fof(85, plain,![X1]:(~(aElementOf0(X1,szNzAzT0))|![X2]:((~(X2=slbdtrb0(X1))|(aSet0(X2)&![X3]:((~(aElementOf0(X3,X2))|(aElementOf0(X3,szNzAzT0)&sdtlseqdt0(szszuzczcdt0(X3),X1)))&((~(aElementOf0(X3,szNzAzT0))|~(sdtlseqdt0(szszuzczcdt0(X3),X1)))|aElementOf0(X3,X2)))))&((~(aSet0(X2))|?[X3]:((~(aElementOf0(X3,X2))|(~(aElementOf0(X3,szNzAzT0))|~(sdtlseqdt0(szszuzczcdt0(X3),X1))))&(aElementOf0(X3,X2)|(aElementOf0(X3,szNzAzT0)&sdtlseqdt0(szszuzczcdt0(X3),X1)))))|X2=slbdtrb0(X1)))),inference(fof_nnf,[status(thm)],[6])).
% fof(86, plain,![X4]:(~(aElementOf0(X4,szNzAzT0))|![X5]:((~(X5=slbdtrb0(X4))|(aSet0(X5)&![X6]:((~(aElementOf0(X6,X5))|(aElementOf0(X6,szNzAzT0)&sdtlseqdt0(szszuzczcdt0(X6),X4)))&((~(aElementOf0(X6,szNzAzT0))|~(sdtlseqdt0(szszuzczcdt0(X6),X4)))|aElementOf0(X6,X5)))))&((~(aSet0(X5))|?[X7]:((~(aElementOf0(X7,X5))|(~(aElementOf0(X7,szNzAzT0))|~(sdtlseqdt0(szszuzczcdt0(X7),X4))))&(aElementOf0(X7,X5)|(aElementOf0(X7,szNzAzT0)&sdtlseqdt0(szszuzczcdt0(X7),X4)))))|X5=slbdtrb0(X4)))),inference(variable_rename,[status(thm)],[85])).
% fof(87, plain,![X4]:(~(aElementOf0(X4,szNzAzT0))|![X5]:((~(X5=slbdtrb0(X4))|(aSet0(X5)&![X6]:((~(aElementOf0(X6,X5))|(aElementOf0(X6,szNzAzT0)&sdtlseqdt0(szszuzczcdt0(X6),X4)))&((~(aElementOf0(X6,szNzAzT0))|~(sdtlseqdt0(szszuzczcdt0(X6),X4)))|aElementOf0(X6,X5)))))&((~(aSet0(X5))|((~(aElementOf0(esk2_2(X4,X5),X5))|(~(aElementOf0(esk2_2(X4,X5),szNzAzT0))|~(sdtlseqdt0(szszuzczcdt0(esk2_2(X4,X5)),X4))))&(aElementOf0(esk2_2(X4,X5),X5)|(aElementOf0(esk2_2(X4,X5),szNzAzT0)&sdtlseqdt0(szszuzczcdt0(esk2_2(X4,X5)),X4)))))|X5=slbdtrb0(X4)))),inference(skolemize,[status(esa)],[86])).
% fof(88, plain,![X4]:![X5]:![X6]:((((((~(aElementOf0(X6,X5))|(aElementOf0(X6,szNzAzT0)&sdtlseqdt0(szszuzczcdt0(X6),X4)))&((~(aElementOf0(X6,szNzAzT0))|~(sdtlseqdt0(szszuzczcdt0(X6),X4)))|aElementOf0(X6,X5)))&aSet0(X5))|~(X5=slbdtrb0(X4)))&((~(aSet0(X5))|((~(aElementOf0(esk2_2(X4,X5),X5))|(~(aElementOf0(esk2_2(X4,X5),szNzAzT0))|~(sdtlseqdt0(szszuzczcdt0(esk2_2(X4,X5)),X4))))&(aElementOf0(esk2_2(X4,X5),X5)|(aElementOf0(esk2_2(X4,X5),szNzAzT0)&sdtlseqdt0(szszuzczcdt0(esk2_2(X4,X5)),X4)))))|X5=slbdtrb0(X4)))|~(aElementOf0(X4,szNzAzT0))),inference(shift_quantors,[status(thm)],[87])).
% fof(89, plain,![X4]:![X5]:![X6]:(((((((aElementOf0(X6,szNzAzT0)|~(aElementOf0(X6,X5)))|~(X5=slbdtrb0(X4)))|~(aElementOf0(X4,szNzAzT0)))&(((sdtlseqdt0(szszuzczcdt0(X6),X4)|~(aElementOf0(X6,X5)))|~(X5=slbdtrb0(X4)))|~(aElementOf0(X4,szNzAzT0))))&((((~(aElementOf0(X6,szNzAzT0))|~(sdtlseqdt0(szszuzczcdt0(X6),X4)))|aElementOf0(X6,X5))|~(X5=slbdtrb0(X4)))|~(aElementOf0(X4,szNzAzT0))))&((aSet0(X5)|~(X5=slbdtrb0(X4)))|~(aElementOf0(X4,szNzAzT0))))&(((((~(aElementOf0(esk2_2(X4,X5),X5))|(~(aElementOf0(esk2_2(X4,X5),szNzAzT0))|~(sdtlseqdt0(szszuzczcdt0(esk2_2(X4,X5)),X4))))|~(aSet0(X5)))|X5=slbdtrb0(X4))|~(aElementOf0(X4,szNzAzT0)))&(((((aElementOf0(esk2_2(X4,X5),szNzAzT0)|aElementOf0(esk2_2(X4,X5),X5))|~(aSet0(X5)))|X5=slbdtrb0(X4))|~(aElementOf0(X4,szNzAzT0)))&((((sdtlseqdt0(szszuzczcdt0(esk2_2(X4,X5)),X4)|aElementOf0(esk2_2(X4,X5),X5))|~(aSet0(X5)))|X5=slbdtrb0(X4))|~(aElementOf0(X4,szNzAzT0)))))),inference(distribute,[status(thm)],[88])).
% cnf(94,plain,(aElementOf0(X3,X2)|~aElementOf0(X1,szNzAzT0)|X2!=slbdtrb0(X1)|~sdtlseqdt0(szszuzczcdt0(X3),X1)|~aElementOf0(X3,szNzAzT0)),inference(split_conjunct,[status(thm)],[89])).
% cnf(95,plain,(sdtlseqdt0(szszuzczcdt0(X3),X1)|~aElementOf0(X1,szNzAzT0)|X2!=slbdtrb0(X1)|~aElementOf0(X3,X2)),inference(split_conjunct,[status(thm)],[89])).
% fof(100, plain,![X1]:![X2]:((~(aElementOf0(X1,szNzAzT0))|~(aElementOf0(X2,szNzAzT0)))|((~(sdtlseqdt0(X1,X2))|sdtlseqdt0(szszuzczcdt0(X1),szszuzczcdt0(X2)))&(~(sdtlseqdt0(szszuzczcdt0(X1),szszuzczcdt0(X2)))|sdtlseqdt0(X1,X2)))),inference(fof_nnf,[status(thm)],[8])).
% fof(101, plain,![X3]:![X4]:((~(aElementOf0(X3,szNzAzT0))|~(aElementOf0(X4,szNzAzT0)))|((~(sdtlseqdt0(X3,X4))|sdtlseqdt0(szszuzczcdt0(X3),szszuzczcdt0(X4)))&(~(sdtlseqdt0(szszuzczcdt0(X3),szszuzczcdt0(X4)))|sdtlseqdt0(X3,X4)))),inference(variable_rename,[status(thm)],[100])).
% fof(102, plain,![X3]:![X4]:(((~(sdtlseqdt0(X3,X4))|sdtlseqdt0(szszuzczcdt0(X3),szszuzczcdt0(X4)))|(~(aElementOf0(X3,szNzAzT0))|~(aElementOf0(X4,szNzAzT0))))&((~(sdtlseqdt0(szszuzczcdt0(X3),szszuzczcdt0(X4)))|sdtlseqdt0(X3,X4))|(~(aElementOf0(X3,szNzAzT0))|~(aElementOf0(X4,szNzAzT0))))),inference(distribute,[status(thm)],[101])).
% cnf(103,plain,(sdtlseqdt0(X2,X1)|~aElementOf0(X1,szNzAzT0)|~aElementOf0(X2,szNzAzT0)|~sdtlseqdt0(szszuzczcdt0(X2),szszuzczcdt0(X1))),inference(split_conjunct,[status(thm)],[102])).
% cnf(104,plain,(sdtlseqdt0(szszuzczcdt0(X2),szszuzczcdt0(X1))|~aElementOf0(X1,szNzAzT0)|~aElementOf0(X2,szNzAzT0)|~sdtlseqdt0(X2,X1)),inference(split_conjunct,[status(thm)],[102])).
% fof(105, plain,![X1]:(~(aElementOf0(X1,szNzAzT0))|sdtlseqdt0(X1,szszuzczcdt0(X1))),inference(fof_nnf,[status(thm)],[9])).
% fof(106, plain,![X2]:(~(aElementOf0(X2,szNzAzT0))|sdtlseqdt0(X2,szszuzczcdt0(X2))),inference(variable_rename,[status(thm)],[105])).
% cnf(107,plain,(sdtlseqdt0(X1,szszuzczcdt0(X1))|~aElementOf0(X1,szNzAzT0)),inference(split_conjunct,[status(thm)],[106])).
% fof(108, plain,![X1]:![X2]:((~(aElementOf0(X1,szNzAzT0))|~(aElementOf0(X2,szNzAzT0)))|(sdtlseqdt0(X1,X2)|sdtlseqdt0(szszuzczcdt0(X2),X1))),inference(fof_nnf,[status(thm)],[10])).
% fof(109, plain,![X3]:![X4]:((~(aElementOf0(X3,szNzAzT0))|~(aElementOf0(X4,szNzAzT0)))|(sdtlseqdt0(X3,X4)|sdtlseqdt0(szszuzczcdt0(X4),X3))),inference(variable_rename,[status(thm)],[108])).
% cnf(110,plain,(sdtlseqdt0(szszuzczcdt0(X1),X2)|sdtlseqdt0(X2,X1)|~aElementOf0(X1,szNzAzT0)|~aElementOf0(X2,szNzAzT0)),inference(split_conjunct,[status(thm)],[109])).
% fof(111, plain,![X1]:![X2]:((~(aElementOf0(X1,szNzAzT0))|~(aElementOf0(X2,szNzAzT0)))|((~(sdtlseqdt0(X1,X2))|~(sdtlseqdt0(X2,X1)))|X1=X2)),inference(fof_nnf,[status(thm)],[11])).
% fof(112, plain,![X3]:![X4]:((~(aElementOf0(X3,szNzAzT0))|~(aElementOf0(X4,szNzAzT0)))|((~(sdtlseqdt0(X3,X4))|~(sdtlseqdt0(X4,X3)))|X3=X4)),inference(variable_rename,[status(thm)],[111])).
% cnf(113,plain,(X1=X2|~sdtlseqdt0(X2,X1)|~sdtlseqdt0(X1,X2)|~aElementOf0(X2,szNzAzT0)|~aElementOf0(X1,szNzAzT0)),inference(split_conjunct,[status(thm)],[112])).
% fof(120, plain,![X1]:![X2]:![X3]:(((~(aElementOf0(X1,szNzAzT0))|~(aElementOf0(X2,szNzAzT0)))|~(aElementOf0(X3,szNzAzT0)))|((~(sdtlseqdt0(X1,X2))|~(sdtlseqdt0(X2,X3)))|sdtlseqdt0(X1,X3))),inference(fof_nnf,[status(thm)],[14])).
% fof(121, plain,![X4]:![X5]:![X6]:(((~(aElementOf0(X4,szNzAzT0))|~(aElementOf0(X5,szNzAzT0)))|~(aElementOf0(X6,szNzAzT0)))|((~(sdtlseqdt0(X4,X5))|~(sdtlseqdt0(X5,X6)))|sdtlseqdt0(X4,X6))),inference(variable_rename,[status(thm)],[120])).
% cnf(122,plain,(sdtlseqdt0(X1,X2)|~sdtlseqdt0(X3,X2)|~sdtlseqdt0(X1,X3)|~aElementOf0(X2,szNzAzT0)|~aElementOf0(X3,szNzAzT0)|~aElementOf0(X1,szNzAzT0)),inference(split_conjunct,[status(thm)],[121])).
% cnf(123,plain,(aElementOf0(sz00,szNzAzT0)),inference(split_conjunct,[status(thm)],[15])).
% fof(124, plain,![X1]:(~(aElementOf0(X1,szNzAzT0))|~(sdtlseqdt0(szszuzczcdt0(X1),sz00))),inference(fof_nnf,[status(thm)],[56])).
% fof(125, plain,![X2]:(~(aElementOf0(X2,szNzAzT0))|~(sdtlseqdt0(szszuzczcdt0(X2),sz00))),inference(variable_rename,[status(thm)],[124])).
% cnf(126,plain,(~sdtlseqdt0(szszuzczcdt0(X1),sz00)|~aElementOf0(X1,szNzAzT0)),inference(split_conjunct,[status(thm)],[125])).
% cnf(127,plain,(slbdtrb0(sz00)=slcrc0),inference(split_conjunct,[status(thm)],[17])).
% fof(128, plain,![X1]:((~(X1=slcrc0)|(aSet0(X1)&![X2]:~(aElementOf0(X2,X1))))&((~(aSet0(X1))|?[X2]:aElementOf0(X2,X1))|X1=slcrc0)),inference(fof_nnf,[status(thm)],[18])).
% fof(129, plain,![X3]:((~(X3=slcrc0)|(aSet0(X3)&![X4]:~(aElementOf0(X4,X3))))&((~(aSet0(X3))|?[X5]:aElementOf0(X5,X3))|X3=slcrc0)),inference(variable_rename,[status(thm)],[128])).
% fof(130, plain,![X3]:((~(X3=slcrc0)|(aSet0(X3)&![X4]:~(aElementOf0(X4,X3))))&((~(aSet0(X3))|aElementOf0(esk3_1(X3),X3))|X3=slcrc0)),inference(skolemize,[status(esa)],[129])).
% fof(131, plain,![X3]:![X4]:(((~(aElementOf0(X4,X3))&aSet0(X3))|~(X3=slcrc0))&((~(aSet0(X3))|aElementOf0(esk3_1(X3),X3))|X3=slcrc0)),inference(shift_quantors,[status(thm)],[130])).
% fof(132, plain,![X3]:![X4]:(((~(aElementOf0(X4,X3))|~(X3=slcrc0))&(aSet0(X3)|~(X3=slcrc0)))&((~(aSet0(X3))|aElementOf0(esk3_1(X3),X3))|X3=slcrc0)),inference(distribute,[status(thm)],[131])).
% cnf(135,plain,(X1!=slcrc0|~aElementOf0(X2,X1)),inference(split_conjunct,[status(thm)],[132])).
% fof(147, plain,![X1]:(~(aElementOf0(X1,szNzAzT0))|sdtlseqdt0(sz00,X1)),inference(fof_nnf,[status(thm)],[22])).
% fof(148, plain,![X2]:(~(aElementOf0(X2,szNzAzT0))|sdtlseqdt0(sz00,X2)),inference(variable_rename,[status(thm)],[147])).
% cnf(149,plain,(sdtlseqdt0(sz00,X1)|~aElementOf0(X1,szNzAzT0)),inference(split_conjunct,[status(thm)],[148])).
% fof(152, plain,![X1]:(~(aSet0(X1))|aSubsetOf0(X1,X1)),inference(fof_nnf,[status(thm)],[24])).
% fof(153, plain,![X2]:(~(aSet0(X2))|aSubsetOf0(X2,X2)),inference(variable_rename,[status(thm)],[152])).
% cnf(154,plain,(aSubsetOf0(X1,X1)|~aSet0(X1)),inference(split_conjunct,[status(thm)],[153])).
% fof(201, plain,![X1]:((~(aSubsetOf0(X1,szNzAzT0))|X1=slcrc0)|![X2]:((~(X2=szmzizndt0(X1))|(aElementOf0(X2,X1)&![X3]:(~(aElementOf0(X3,X1))|sdtlseqdt0(X2,X3))))&((~(aElementOf0(X2,X1))|?[X3]:(aElementOf0(X3,X1)&~(sdtlseqdt0(X2,X3))))|X2=szmzizndt0(X1)))),inference(fof_nnf,[status(thm)],[32])).
% fof(202, plain,![X4]:((~(aSubsetOf0(X4,szNzAzT0))|X4=slcrc0)|![X5]:((~(X5=szmzizndt0(X4))|(aElementOf0(X5,X4)&![X6]:(~(aElementOf0(X6,X4))|sdtlseqdt0(X5,X6))))&((~(aElementOf0(X5,X4))|?[X7]:(aElementOf0(X7,X4)&~(sdtlseqdt0(X5,X7))))|X5=szmzizndt0(X4)))),inference(variable_rename,[status(thm)],[201])).
% fof(203, plain,![X4]:((~(aSubsetOf0(X4,szNzAzT0))|X4=slcrc0)|![X5]:((~(X5=szmzizndt0(X4))|(aElementOf0(X5,X4)&![X6]:(~(aElementOf0(X6,X4))|sdtlseqdt0(X5,X6))))&((~(aElementOf0(X5,X4))|(aElementOf0(esk6_2(X4,X5),X4)&~(sdtlseqdt0(X5,esk6_2(X4,X5)))))|X5=szmzizndt0(X4)))),inference(skolemize,[status(esa)],[202])).
% fof(204, plain,![X4]:![X5]:![X6]:(((((~(aElementOf0(X6,X4))|sdtlseqdt0(X5,X6))&aElementOf0(X5,X4))|~(X5=szmzizndt0(X4)))&((~(aElementOf0(X5,X4))|(aElementOf0(esk6_2(X4,X5),X4)&~(sdtlseqdt0(X5,esk6_2(X4,X5)))))|X5=szmzizndt0(X4)))|(~(aSubsetOf0(X4,szNzAzT0))|X4=slcrc0)),inference(shift_quantors,[status(thm)],[203])).
% fof(205, plain,![X4]:![X5]:![X6]:(((((~(aElementOf0(X6,X4))|sdtlseqdt0(X5,X6))|~(X5=szmzizndt0(X4)))|(~(aSubsetOf0(X4,szNzAzT0))|X4=slcrc0))&((aElementOf0(X5,X4)|~(X5=szmzizndt0(X4)))|(~(aSubsetOf0(X4,szNzAzT0))|X4=slcrc0)))&((((aElementOf0(esk6_2(X4,X5),X4)|~(aElementOf0(X5,X4)))|X5=szmzizndt0(X4))|(~(aSubsetOf0(X4,szNzAzT0))|X4=slcrc0))&(((~(sdtlseqdt0(X5,esk6_2(X4,X5)))|~(aElementOf0(X5,X4)))|X5=szmzizndt0(X4))|(~(aSubsetOf0(X4,szNzAzT0))|X4=slcrc0)))),inference(distribute,[status(thm)],[204])).
% cnf(208,plain,(X1=slcrc0|aElementOf0(X2,X1)|~aSubsetOf0(X1,szNzAzT0)|X2!=szmzizndt0(X1)),inference(split_conjunct,[status(thm)],[205])).
% cnf(209,plain,(X1=slcrc0|sdtlseqdt0(X2,X3)|~aSubsetOf0(X1,szNzAzT0)|X2!=szmzizndt0(X1)|~aElementOf0(X3,X1)),inference(split_conjunct,[status(thm)],[205])).
% cnf(239,plain,(aSet0(szNzAzT0)),inference(split_conjunct,[status(thm)],[40])).
% fof(289, negated_conjecture,((~(aElementOf0(xm,slbdtrb0(szszuzczcdt0(xn))))|(~(aElementOf0(xm,slbdtrb0(xn)))&~(xm=xn)))&(aElementOf0(xm,slbdtrb0(szszuzczcdt0(xn)))|(aElementOf0(xm,slbdtrb0(xn))|xm=xn))),inference(fof_nnf,[status(thm)],[55])).
% fof(290, negated_conjecture,(((~(aElementOf0(xm,slbdtrb0(xn)))|~(aElementOf0(xm,slbdtrb0(szszuzczcdt0(xn)))))&(~(xm=xn)|~(aElementOf0(xm,slbdtrb0(szszuzczcdt0(xn))))))&(aElementOf0(xm,slbdtrb0(szszuzczcdt0(xn)))|(aElementOf0(xm,slbdtrb0(xn))|xm=xn))),inference(distribute,[status(thm)],[289])).
% cnf(291,negated_conjecture,(xm=xn|aElementOf0(xm,slbdtrb0(xn))|aElementOf0(xm,slbdtrb0(szszuzczcdt0(xn)))),inference(split_conjunct,[status(thm)],[290])).
% cnf(292,negated_conjecture,(~aElementOf0(xm,slbdtrb0(szszuzczcdt0(xn)))|xm!=xn),inference(split_conjunct,[status(thm)],[290])).
% cnf(293,negated_conjecture,(~aElementOf0(xm,slbdtrb0(szszuzczcdt0(xn)))|~aElementOf0(xm,slbdtrb0(xn))),inference(split_conjunct,[status(thm)],[290])).
% cnf(298,plain,(sdtlseqdt0(X2,X3)|szmzizndt0(X1)!=X2|~aSubsetOf0(X1,szNzAzT0)|~aElementOf0(X3,X1)),inference(csr,[status(thm)],[209,135])).
% cnf(316,plain,(slcrc0!=szNzAzT0),inference(spm,[status(thm)],[135,123,theory(equality)])).
% cnf(354,plain,(sdtlseqdt0(esk1_1(X1),X1)|sz00=X1|~aElementOf0(esk1_1(X1),szNzAzT0)|~aElementOf0(X1,szNzAzT0)),inference(spm,[status(thm)],[107,83,theory(equality)])).
% cnf(392,plain,(slcrc0=X1|aElementOf0(szmzizndt0(X1),X1)|~aSubsetOf0(X1,szNzAzT0)),inference(er,[status(thm)],[208,theory(equality)])).
% cnf(400,plain,(sdtlseqdt0(szszuzczcdt0(X1),X2)|sz00=X2|~sdtlseqdt0(X1,esk1_1(X2))|~aElementOf0(X1,szNzAzT0)|~aElementOf0(esk1_1(X2),szNzAzT0)|~aElementOf0(X2,szNzAzT0)),inference(spm,[status(thm)],[104,83,theory(equality)])).
% cnf(401,plain,(sdtlseqdt0(X1,szszuzczcdt0(X2))|sz00=X1|~sdtlseqdt0(esk1_1(X1),X2)|~aElementOf0(esk1_1(X1),szNzAzT0)|~aElementOf0(X2,szNzAzT0)|~aElementOf0(X1,szNzAzT0)),inference(spm,[status(thm)],[104,83,theory(equality)])).
% cnf(402,plain,(sdtlseqdt0(X1,esk1_1(X2))|sz00=X2|~sdtlseqdt0(szszuzczcdt0(X1),X2)|~aElementOf0(X1,szNzAzT0)|~aElementOf0(esk1_1(X2),szNzAzT0)|~aElementOf0(X2,szNzAzT0)),inference(spm,[status(thm)],[103,83,theory(equality)])).
% cnf(413,negated_conjecture,(sdtlseqdt0(szszuzczcdt0(xm),X1)|xn=xm|aElementOf0(xm,slbdtrb0(xn))|slbdtrb0(X1)!=slbdtrb0(szszuzczcdt0(xn))|~aElementOf0(X1,szNzAzT0)),inference(spm,[status(thm)],[95,291,theory(equality)])).
% cnf(438,plain,(aElementOf0(X1,X2)|slbdtrb0(szszuzczcdt0(X3))!=X2|~aElementOf0(X1,szNzAzT0)|~aElementOf0(szszuzczcdt0(X3),szNzAzT0)|~sdtlseqdt0(X1,X3)|~aElementOf0(X3,szNzAzT0)),inference(spm,[status(thm)],[94,104,theory(equality)])).
% cnf(439,plain,(aElementOf0(X1,X2)|sdtlseqdt0(X3,X1)|slbdtrb0(X3)!=X2|~aElementOf0(X1,szNzAzT0)|~aElementOf0(X3,szNzAzT0)),inference(spm,[status(thm)],[94,110,theory(equality)])).
% cnf(451,plain,(sdtlseqdt0(X1,sz00)|szmzizndt0(szNzAzT0)!=X1|~aSubsetOf0(szNzAzT0,szNzAzT0)),inference(spm,[status(thm)],[298,123,theory(equality)])).
% cnf(452,plain,(sdtlseqdt0(X1,xn)|szmzizndt0(szNzAzT0)!=X1|~aSubsetOf0(szNzAzT0,szNzAzT0)),inference(spm,[status(thm)],[298,72,theory(equality)])).
% cnf(472,plain,(X1=sz00|~sdtlseqdt0(X1,sz00)|~aElementOf0(sz00,szNzAzT0)|~aElementOf0(X1,szNzAzT0)),inference(spm,[status(thm)],[113,149,theory(equality)])).
% cnf(473,plain,(szszuzczcdt0(X1)=szszuzczcdt0(X2)|~sdtlseqdt0(szszuzczcdt0(X1),szszuzczcdt0(X2))|~aElementOf0(szszuzczcdt0(X2),szNzAzT0)|~aElementOf0(szszuzczcdt0(X1),szNzAzT0)|~sdtlseqdt0(X2,X1)|~aElementOf0(X2,szNzAzT0)|~aElementOf0(X1,szNzAzT0)),inference(spm,[status(thm)],[113,104,theory(equality)])).
% cnf(474,plain,(X1=szszuzczcdt0(X2)|sdtlseqdt0(X1,X2)|~sdtlseqdt0(X1,szszuzczcdt0(X2))|~aElementOf0(szszuzczcdt0(X2),szNzAzT0)|~aElementOf0(X1,szNzAzT0)|~aElementOf0(X2,szNzAzT0)),inference(spm,[status(thm)],[113,110,theory(equality)])).
% cnf(475,plain,(szszuzczcdt0(X1)=X1|~sdtlseqdt0(szszuzczcdt0(X1),X1)|~aElementOf0(X1,szNzAzT0)|~aElementOf0(szszuzczcdt0(X1),szNzAzT0)),inference(spm,[status(thm)],[113,107,theory(equality)])).
% cnf(476,plain,(X1=sz00|~sdtlseqdt0(X1,sz00)|$false|~aElementOf0(X1,szNzAzT0)),inference(rw,[status(thm)],[472,123,theory(equality)])).
% cnf(477,plain,(X1=sz00|~sdtlseqdt0(X1,sz00)|~aElementOf0(X1,szNzAzT0)),inference(cn,[status(thm)],[476,theory(equality)])).
% cnf(581,plain,(sdtlseqdt0(X1,X2)|~sdtlseqdt0(X1,sz00)|~aElementOf0(sz00,szNzAzT0)|~aElementOf0(X2,szNzAzT0)|~aElementOf0(X1,szNzAzT0)),inference(spm,[status(thm)],[122,149,theory(equality)])).
% cnf(582,plain,(sdtlseqdt0(X1,szszuzczcdt0(X2))|~sdtlseqdt0(X1,szszuzczcdt0(X3))|~aElementOf0(szszuzczcdt0(X3),szNzAzT0)|~aElementOf0(szszuzczcdt0(X2),szNzAzT0)|~aElementOf0(X1,szNzAzT0)|~sdtlseqdt0(X3,X2)|~aElementOf0(X3,szNzAzT0)|~aElementOf0(X2,szNzAzT0)),inference(spm,[status(thm)],[122,104,theory(equality)])).
% cnf(583,plain,(sdtlseqdt0(X1,X2)|sdtlseqdt0(X2,X3)|~sdtlseqdt0(X1,szszuzczcdt0(X3))|~aElementOf0(szszuzczcdt0(X3),szNzAzT0)|~aElementOf0(X2,szNzAzT0)|~aElementOf0(X1,szNzAzT0)|~aElementOf0(X3,szNzAzT0)),inference(spm,[status(thm)],[122,110,theory(equality)])).
% cnf(586,plain,(sdtlseqdt0(X1,X2)|~sdtlseqdt0(X1,sz00)|$false|~aElementOf0(X2,szNzAzT0)|~aElementOf0(X1,szNzAzT0)),inference(rw,[status(thm)],[581,123,theory(equality)])).
% cnf(587,plain,(sdtlseqdt0(X1,X2)|~sdtlseqdt0(X1,sz00)|~aElementOf0(X2,szNzAzT0)|~aElementOf0(X1,szNzAzT0)),inference(cn,[status(thm)],[586,theory(equality)])).
% cnf(714,plain,(sz00=X1|sdtlseqdt0(esk1_1(X1),X1)|~aElementOf0(X1,szNzAzT0)),inference(csr,[status(thm)],[354,84])).
% cnf(747,plain,(sdtlseqdt0(szmzizndt0(szNzAzT0),sz00)|~aSubsetOf0(szNzAzT0,szNzAzT0)),inference(er,[status(thm)],[451,theory(equality)])).
% cnf(750,plain,(szmzizndt0(szNzAzT0)=sz00|~aElementOf0(szmzizndt0(szNzAzT0),szNzAzT0)|~aSubsetOf0(szNzAzT0,szNzAzT0)),inference(spm,[status(thm)],[477,747,theory(equality)])).
% cnf(798,plain,(szmzizndt0(szNzAzT0)=sz00|slcrc0=szNzAzT0|~aSubsetOf0(szNzAzT0,szNzAzT0)),inference(spm,[status(thm)],[750,392,theory(equality)])).
% cnf(801,plain,(szmzizndt0(szNzAzT0)=sz00|~aSubsetOf0(szNzAzT0,szNzAzT0)),inference(sr,[status(thm)],[798,316,theory(equality)])).
% cnf(802,plain,(slcrc0=szNzAzT0|aElementOf0(X1,szNzAzT0)|sz00!=X1|~aSubsetOf0(szNzAzT0,szNzAzT0)),inference(spm,[status(thm)],[208,801,theory(equality)])).
% cnf(806,plain,(sdtlseqdt0(X1,sz00)|sz00!=X1|~aSubsetOf0(szNzAzT0,szNzAzT0)),inference(spm,[status(thm)],[451,801,theory(equality)])).
% cnf(807,plain,(sdtlseqdt0(X1,xn)|sz00!=X1|~aSubsetOf0(szNzAzT0,szNzAzT0)),inference(spm,[status(thm)],[452,801,theory(equality)])).
% cnf(810,plain,(sdtlseqdt0(sz00,sz00)|~aSubsetOf0(szNzAzT0,szNzAzT0)),inference(spm,[status(thm)],[747,801,theory(equality)])).
% cnf(811,plain,(aElementOf0(X1,szNzAzT0)|sz00!=X1|~aSubsetOf0(szNzAzT0,szNzAzT0)),inference(sr,[status(thm)],[802,316,theory(equality)])).
% cnf(848,plain,(sdtlseqdt0(sz00,sz00)|~aSet0(szNzAzT0)),inference(spm,[status(thm)],[810,154,theory(equality)])).
% cnf(850,plain,(sdtlseqdt0(sz00,sz00)|$false),inference(rw,[status(thm)],[848,239,theory(equality)])).
% cnf(851,plain,(sdtlseqdt0(sz00,sz00)),inference(cn,[status(thm)],[850,theory(equality)])).
% cnf(898,plain,(aElementOf0(X1,szNzAzT0)|sz00!=X1|~aSet0(szNzAzT0)),inference(spm,[status(thm)],[811,154,theory(equality)])).
% cnf(900,plain,(aElementOf0(X1,szNzAzT0)|sz00!=X1|$false),inference(rw,[status(thm)],[898,239,theory(equality)])).
% cnf(901,plain,(aElementOf0(X1,szNzAzT0)|sz00!=X1),inference(cn,[status(thm)],[900,theory(equality)])).
% cnf(915,plain,(sdtlseqdt0(X1,X2)|szmzizndt0(szNzAzT0)!=X1|~aSubsetOf0(szNzAzT0,szNzAzT0)|sz00!=X2),inference(spm,[status(thm)],[298,901,theory(equality)])).
% cnf(970,plain,(sdtlseqdt0(X1,xn)|sz00!=X1|~aSet0(szNzAzT0)),inference(spm,[status(thm)],[807,154,theory(equality)])).
% cnf(972,plain,(sdtlseqdt0(X1,xn)|sz00!=X1|$false),inference(rw,[status(thm)],[970,239,theory(equality)])).
% cnf(973,plain,(sdtlseqdt0(X1,xn)|sz00!=X1),inference(cn,[status(thm)],[972,theory(equality)])).
% cnf(980,plain,(xn=X1|~sdtlseqdt0(xn,X1)|~aElementOf0(X1,szNzAzT0)|~aElementOf0(xn,szNzAzT0)|sz00!=X1),inference(spm,[status(thm)],[113,973,theory(equality)])).
% cnf(987,plain,(xn=X1|~sdtlseqdt0(xn,X1)|~aElementOf0(X1,szNzAzT0)|$false|sz00!=X1),inference(rw,[status(thm)],[980,72,theory(equality)])).
% cnf(988,plain,(xn=X1|~sdtlseqdt0(xn,X1)|~aElementOf0(X1,szNzAzT0)|sz00!=X1),inference(cn,[status(thm)],[987,theory(equality)])).
% cnf(989,plain,(xn=X1|sz00!=X1|~sdtlseqdt0(xn,X1)),inference(csr,[status(thm)],[988,901])).
% cnf(1009,plain,(sz00=X2|sdtlseqdt0(szszuzczcdt0(X1),X2)|~sdtlseqdt0(X1,esk1_1(X2))|~aElementOf0(X2,szNzAzT0)|~aElementOf0(X1,szNzAzT0)),inference(csr,[status(thm)],[400,84])).
% cnf(1011,plain,(sz00=X1|sdtlseqdt0(szszuzczcdt0(sz00),X1)|~aElementOf0(sz00,szNzAzT0)|~aElementOf0(X1,szNzAzT0)|~aElementOf0(esk1_1(X1),szNzAzT0)),inference(spm,[status(thm)],[1009,149,theory(equality)])).
% cnf(1019,plain,(sz00=X1|sdtlseqdt0(szszuzczcdt0(sz00),X1)|$false|~aElementOf0(X1,szNzAzT0)|~aElementOf0(esk1_1(X1),szNzAzT0)),inference(rw,[status(thm)],[1011,123,theory(equality)])).
% cnf(1020,plain,(sz00=X1|sdtlseqdt0(szszuzczcdt0(sz00),X1)|~aElementOf0(X1,szNzAzT0)|~aElementOf0(esk1_1(X1),szNzAzT0)),inference(cn,[status(thm)],[1019,theory(equality)])).
% cnf(1053,plain,(sdtlseqdt0(X1,sz00)|sz00!=X1|~aSet0(szNzAzT0)),inference(spm,[status(thm)],[806,154,theory(equality)])).
% cnf(1055,plain,(sdtlseqdt0(X1,sz00)|sz00!=X1|$false),inference(rw,[status(thm)],[1053,239,theory(equality)])).
% cnf(1056,plain,(sdtlseqdt0(X1,sz00)|sz00!=X1),inference(cn,[status(thm)],[1055,theory(equality)])).
% cnf(1059,plain,(sz00=X1|sdtlseqdt0(X1,szszuzczcdt0(X2))|~sdtlseqdt0(esk1_1(X1),X2)|~aElementOf0(X2,szNzAzT0)|~aElementOf0(X1,szNzAzT0)),inference(csr,[status(thm)],[401,84])).
% cnf(1062,plain,(sz00=X1|sdtlseqdt0(X1,szszuzczcdt0(xn))|~aElementOf0(xn,szNzAzT0)|~aElementOf0(X1,szNzAzT0)|sz00!=esk1_1(X1)),inference(spm,[status(thm)],[1059,973,theory(equality)])).
% cnf(1070,plain,(sz00=X1|sdtlseqdt0(X1,szszuzczcdt0(xn))|$false|~aElementOf0(X1,szNzAzT0)|sz00!=esk1_1(X1)),inference(rw,[status(thm)],[1062,72,theory(equality)])).
% cnf(1071,plain,(sz00=X1|sdtlseqdt0(X1,szszuzczcdt0(xn))|~aElementOf0(X1,szNzAzT0)|sz00!=esk1_1(X1)),inference(cn,[status(thm)],[1070,theory(equality)])).
% cnf(1107,plain,(sz00=X2|sdtlseqdt0(X1,esk1_1(X2))|~sdtlseqdt0(szszuzczcdt0(X1),X2)|~aElementOf0(X2,szNzAzT0)|~aElementOf0(X1,szNzAzT0)),inference(csr,[status(thm)],[402,84])).
% cnf(1324,plain,(sdtlseqdt0(X1,X2)|sz00!=X1|sz00!=X2|~aSubsetOf0(szNzAzT0,szNzAzT0)),inference(spm,[status(thm)],[915,801,theory(equality)])).
% cnf(1356,negated_conjecture,(xn=xm|sdtlseqdt0(szszuzczcdt0(xm),szszuzczcdt0(xn))|aElementOf0(xm,slbdtrb0(xn))|~aElementOf0(szszuzczcdt0(xn),szNzAzT0)),inference(er,[status(thm)],[413,theory(equality)])).
% cnf(1380,negated_conjecture,(sdtlseqdt0(xm,xn)|xn=xm|aElementOf0(xm,slbdtrb0(xn))|~aElementOf0(xm,szNzAzT0)|~aElementOf0(xn,szNzAzT0)|~aElementOf0(szszuzczcdt0(xn),szNzAzT0)),inference(spm,[status(thm)],[103,1356,theory(equality)])).
% cnf(1383,negated_conjecture,(sdtlseqdt0(xm,xn)|xn=xm|aElementOf0(xm,slbdtrb0(xn))|$false|~aElementOf0(xn,szNzAzT0)|~aElementOf0(szszuzczcdt0(xn),szNzAzT0)),inference(rw,[status(thm)],[1380,73,theory(equality)])).
% cnf(1384,negated_conjecture,(sdtlseqdt0(xm,xn)|xn=xm|aElementOf0(xm,slbdtrb0(xn))|$false|$false|~aElementOf0(szszuzczcdt0(xn),szNzAzT0)),inference(rw,[status(thm)],[1383,72,theory(equality)])).
% cnf(1385,negated_conjecture,(sdtlseqdt0(xm,xn)|xn=xm|aElementOf0(xm,slbdtrb0(xn))|~aElementOf0(szszuzczcdt0(xn),szNzAzT0)),inference(cn,[status(thm)],[1384,theory(equality)])).
% cnf(1389,negated_conjecture,(sdtlseqdt0(szszuzczcdt0(xm),X1)|xn=xm|sdtlseqdt0(xm,xn)|slbdtrb0(X1)!=slbdtrb0(xn)|~aElementOf0(X1,szNzAzT0)|~aElementOf0(szszuzczcdt0(xn),szNzAzT0)),inference(spm,[status(thm)],[95,1385,theory(equality)])).
% cnf(1474,plain,(szszuzczcdt0(X1)=X1|~sdtlseqdt0(szszuzczcdt0(X1),X1)|~aElementOf0(X1,szNzAzT0)),inference(csr,[status(thm)],[475,78])).
% cnf(1475,plain,(~sdtlseqdt0(szszuzczcdt0(X1),X1)|~aElementOf0(X1,szNzAzT0)),inference(csr,[status(thm)],[1474,71])).
% cnf(1476,plain,(sz00=X1|~sdtlseqdt0(X1,esk1_1(X1))|~aElementOf0(esk1_1(X1),szNzAzT0)|~aElementOf0(X1,szNzAzT0)),inference(spm,[status(thm)],[1475,83,theory(equality)])).
% cnf(1481,plain,(~aElementOf0(sz00,szNzAzT0)|sz00!=szszuzczcdt0(sz00)),inference(spm,[status(thm)],[1475,1056,theory(equality)])).
% cnf(1496,plain,($false|sz00!=szszuzczcdt0(sz00)),inference(rw,[status(thm)],[1481,123,theory(equality)])).
% cnf(1497,plain,(sz00!=szszuzczcdt0(sz00)),inference(cn,[status(thm)],[1496,theory(equality)])).
% cnf(1621,plain,(sz00=X1|sdtlseqdt0(szszuzczcdt0(sz00),X1)|~aElementOf0(X1,szNzAzT0)),inference(csr,[status(thm)],[1020,84])).
% cnf(1646,plain,(sdtlseqdt0(X1,X2)|sz00!=X1|sz00!=X2|~aSet0(szNzAzT0)),inference(spm,[status(thm)],[1324,154,theory(equality)])).
% cnf(1648,plain,(sdtlseqdt0(X1,X2)|sz00!=X1|sz00!=X2|$false),inference(rw,[status(thm)],[1646,239,theory(equality)])).
% cnf(1649,plain,(sdtlseqdt0(X1,X2)|sz00!=X1|sz00!=X2),inference(cn,[status(thm)],[1648,theory(equality)])).
% cnf(1932,plain,(aElementOf0(X1,X2)|slbdtrb0(szszuzczcdt0(X3))!=X2|~sdtlseqdt0(X1,X3)|~aElementOf0(X3,szNzAzT0)|~aElementOf0(X1,szNzAzT0)),inference(csr,[status(thm)],[438,78])).
% cnf(1933,plain,(aElementOf0(X1,slbdtrb0(szszuzczcdt0(X2)))|~sdtlseqdt0(X1,X2)|~aElementOf0(X1,szNzAzT0)|~aElementOf0(X2,szNzAzT0)),inference(er,[status(thm)],[1932,theory(equality)])).
% cnf(1973,plain,(sdtlseqdt0(X1,X2)|aElementOf0(X2,slbdtrb0(X1))|~aElementOf0(X2,szNzAzT0)|~aElementOf0(X1,szNzAzT0)),inference(er,[status(thm)],[439,theory(equality)])).
% cnf(2242,negated_conjecture,(xn!=xm|~sdtlseqdt0(xm,xn)|~aElementOf0(xm,szNzAzT0)|~aElementOf0(xn,szNzAzT0)),inference(spm,[status(thm)],[292,1933,theory(equality)])).
% cnf(2243,negated_conjecture,(~aElementOf0(xm,slbdtrb0(xn))|~sdtlseqdt0(xm,xn)|~aElementOf0(xm,szNzAzT0)|~aElementOf0(xn,szNzAzT0)),inference(spm,[status(thm)],[293,1933,theory(equality)])).
% cnf(2252,negated_conjecture,(xn!=xm|~sdtlseqdt0(xm,xn)|$false|~aElementOf0(xn,szNzAzT0)),inference(rw,[status(thm)],[2242,73,theory(equality)])).
% cnf(2253,negated_conjecture,(xn!=xm|~sdtlseqdt0(xm,xn)|$false|$false),inference(rw,[status(thm)],[2252,72,theory(equality)])).
% cnf(2254,negated_conjecture,(xn!=xm|~sdtlseqdt0(xm,xn)),inference(cn,[status(thm)],[2253,theory(equality)])).
% cnf(2255,negated_conjecture,(~aElementOf0(xm,slbdtrb0(xn))|~sdtlseqdt0(xm,xn)|$false|~aElementOf0(xn,szNzAzT0)),inference(rw,[status(thm)],[2243,73,theory(equality)])).
% cnf(2256,negated_conjecture,(~aElementOf0(xm,slbdtrb0(xn))|~sdtlseqdt0(xm,xn)|$false|$false),inference(rw,[status(thm)],[2255,72,theory(equality)])).
% cnf(2257,negated_conjecture,(~aElementOf0(xm,slbdtrb0(xn))|~sdtlseqdt0(xm,xn)),inference(cn,[status(thm)],[2256,theory(equality)])).
% cnf(2260,negated_conjecture,(xn!=xm|sz00!=xm),inference(spm,[status(thm)],[2254,973,theory(equality)])).
% cnf(2338,negated_conjecture,(sdtlseqdt0(xn,xm)|~sdtlseqdt0(xm,xn)|~aElementOf0(xm,szNzAzT0)|~aElementOf0(xn,szNzAzT0)),inference(spm,[status(thm)],[2257,1973,theory(equality)])).
% cnf(2342,negated_conjecture,(sdtlseqdt0(xn,xm)|~sdtlseqdt0(xm,xn)|$false|~aElementOf0(xn,szNzAzT0)),inference(rw,[status(thm)],[2338,73,theory(equality)])).
% cnf(2343,negated_conjecture,(sdtlseqdt0(xn,xm)|~sdtlseqdt0(xm,xn)|$false|$false),inference(rw,[status(thm)],[2342,72,theory(equality)])).
% cnf(2344,negated_conjecture,(sdtlseqdt0(xn,xm)|~sdtlseqdt0(xm,xn)),inference(cn,[status(thm)],[2343,theory(equality)])).
% cnf(2348,negated_conjecture,(xm=xn|~sdtlseqdt0(xm,xn)|~aElementOf0(xn,szNzAzT0)|~aElementOf0(xm,szNzAzT0)),inference(spm,[status(thm)],[113,2344,theory(equality)])).
% cnf(2351,negated_conjecture,(xn=xm|sz00!=xm|~sdtlseqdt0(xm,xn)),inference(spm,[status(thm)],[989,2344,theory(equality)])).
% cnf(2355,negated_conjecture,(xm=xn|~sdtlseqdt0(xm,xn)|$false|~aElementOf0(xm,szNzAzT0)),inference(rw,[status(thm)],[2348,72,theory(equality)])).
% cnf(2356,negated_conjecture,(xm=xn|~sdtlseqdt0(xm,xn)|$false|$false),inference(rw,[status(thm)],[2355,73,theory(equality)])).
% cnf(2357,negated_conjecture,(xm=xn|~sdtlseqdt0(xm,xn)),inference(cn,[status(thm)],[2356,theory(equality)])).
% cnf(2363,negated_conjecture,(~sdtlseqdt0(xm,xn)),inference(csr,[status(thm)],[2357,2254])).
% cnf(2370,negated_conjecture,(xn=xm|xm!=sz00),inference(csr,[status(thm)],[2351,973])).
% cnf(2371,negated_conjecture,(xm!=sz00),inference(csr,[status(thm)],[2370,2260])).
% cnf(2626,plain,(sdtlseqdt0(X1,X2)|~aElementOf0(X2,szNzAzT0)|~aElementOf0(X1,szNzAzT0)|sz00!=X1),inference(spm,[status(thm)],[587,1649,theory(equality)])).
% cnf(2679,plain,(sdtlseqdt0(X1,X2)|sz00!=X1|~aElementOf0(X2,szNzAzT0)),inference(csr,[status(thm)],[2626,901])).
% cnf(3197,plain,(szszuzczcdt0(X1)=szszuzczcdt0(X2)|~sdtlseqdt0(szszuzczcdt0(X1),szszuzczcdt0(X2))|~sdtlseqdt0(X2,X1)|~aElementOf0(szszuzczcdt0(X2),szNzAzT0)|~aElementOf0(X2,szNzAzT0)|~aElementOf0(X1,szNzAzT0)),inference(csr,[status(thm)],[473,78])).
% cnf(3198,plain,(szszuzczcdt0(X1)=szszuzczcdt0(X2)|~sdtlseqdt0(szszuzczcdt0(X1),szszuzczcdt0(X2))|~sdtlseqdt0(X2,X1)|~aElementOf0(X2,szNzAzT0)|~aElementOf0(X1,szNzAzT0)),inference(csr,[status(thm)],[3197,78])).
% cnf(3241,plain,(X1=szszuzczcdt0(X2)|sdtlseqdt0(X1,X2)|~sdtlseqdt0(X1,szszuzczcdt0(X2))|~aElementOf0(X1,szNzAzT0)|~aElementOf0(X2,szNzAzT0)),inference(csr,[status(thm)],[474,78])).
% cnf(3861,plain,(sz00=X1|~sdtlseqdt0(X1,esk1_1(X1))|~aElementOf0(X1,szNzAzT0)),inference(csr,[status(thm)],[1476,84])).
% cnf(3870,plain,(sz00=szszuzczcdt0(sz00)|sz00=esk1_1(szszuzczcdt0(sz00))|~aElementOf0(szszuzczcdt0(sz00),szNzAzT0)|~aElementOf0(esk1_1(szszuzczcdt0(sz00)),szNzAzT0)),inference(spm,[status(thm)],[3861,1621,theory(equality)])).
% cnf(3880,plain,(esk1_1(szszuzczcdt0(sz00))=sz00|~aElementOf0(szszuzczcdt0(sz00),szNzAzT0)|~aElementOf0(esk1_1(szszuzczcdt0(sz00)),szNzAzT0)),inference(sr,[status(thm)],[3870,1497,theory(equality)])).
% cnf(3945,plain,(esk1_1(szszuzczcdt0(sz00))=sz00|sz00=szszuzczcdt0(sz00)|~aElementOf0(szszuzczcdt0(sz00),szNzAzT0)),inference(spm,[status(thm)],[3880,84,theory(equality)])).
% cnf(3947,plain,(esk1_1(szszuzczcdt0(sz00))=sz00|~aElementOf0(szszuzczcdt0(sz00),szNzAzT0)),inference(sr,[status(thm)],[3945,1497,theory(equality)])).
% cnf(3963,plain,(sz00=szszuzczcdt0(sz00)|sdtlseqdt0(szszuzczcdt0(sz00),szszuzczcdt0(xn))|~aElementOf0(szszuzczcdt0(sz00),szNzAzT0)),inference(spm,[status(thm)],[1071,3947,theory(equality)])).
% cnf(3986,plain,(sdtlseqdt0(szszuzczcdt0(sz00),szszuzczcdt0(xn))|~aElementOf0(szszuzczcdt0(sz00),szNzAzT0)),inference(sr,[status(thm)],[3963,1497,theory(equality)])).
% cnf(4030,plain,(szszuzczcdt0(sz00)=szszuzczcdt0(xn)|~sdtlseqdt0(xn,sz00)|~aElementOf0(xn,szNzAzT0)|~aElementOf0(sz00,szNzAzT0)|~aElementOf0(szszuzczcdt0(sz00),szNzAzT0)),inference(spm,[status(thm)],[3198,3986,theory(equality)])).
% cnf(4040,plain,(szszuzczcdt0(sz00)=szszuzczcdt0(xn)|~sdtlseqdt0(xn,sz00)|$false|~aElementOf0(sz00,szNzAzT0)|~aElementOf0(szszuzczcdt0(sz00),szNzAzT0)),inference(rw,[status(thm)],[4030,72,theory(equality)])).
% cnf(4041,plain,(szszuzczcdt0(sz00)=szszuzczcdt0(xn)|~sdtlseqdt0(xn,sz00)|$false|$false|~aElementOf0(szszuzczcdt0(sz00),szNzAzT0)),inference(rw,[status(thm)],[4040,123,theory(equality)])).
% cnf(4042,plain,(szszuzczcdt0(sz00)=szszuzczcdt0(xn)|~sdtlseqdt0(xn,sz00)|~aElementOf0(szszuzczcdt0(sz00),szNzAzT0)),inference(cn,[status(thm)],[4041,theory(equality)])).
% cnf(4099,plain,(szszuzczcdt0(xn)=szszuzczcdt0(sz00)|~sdtlseqdt0(xn,sz00)|~aElementOf0(sz00,szNzAzT0)),inference(spm,[status(thm)],[4042,78,theory(equality)])).
% cnf(4100,plain,(szszuzczcdt0(xn)=szszuzczcdt0(sz00)|~sdtlseqdt0(xn,sz00)|$false),inference(rw,[status(thm)],[4099,123,theory(equality)])).
% cnf(4101,plain,(szszuzczcdt0(xn)=szszuzczcdt0(sz00)|~sdtlseqdt0(xn,sz00)),inference(cn,[status(thm)],[4100,theory(equality)])).
% cnf(4122,plain,(aElementOf0(szszuzczcdt0(sz00),szNzAzT0)|~aElementOf0(xn,szNzAzT0)|~sdtlseqdt0(xn,sz00)),inference(spm,[status(thm)],[78,4101,theory(equality)])).
% cnf(4185,plain,(aElementOf0(szszuzczcdt0(sz00),szNzAzT0)|$false|~sdtlseqdt0(xn,sz00)),inference(rw,[status(thm)],[4122,72,theory(equality)])).
% cnf(4186,plain,(aElementOf0(szszuzczcdt0(sz00),szNzAzT0)|~sdtlseqdt0(xn,sz00)),inference(cn,[status(thm)],[4185,theory(equality)])).
% cnf(6969,plain,(sdtlseqdt0(X1,szszuzczcdt0(X2))|~sdtlseqdt0(X1,szszuzczcdt0(X3))|~sdtlseqdt0(X3,X2)|~aElementOf0(szszuzczcdt0(X3),szNzAzT0)|~aElementOf0(X1,szNzAzT0)|~aElementOf0(X3,szNzAzT0)|~aElementOf0(X2,szNzAzT0)),inference(csr,[status(thm)],[582,78])).
% cnf(6970,plain,(sdtlseqdt0(X1,szszuzczcdt0(X2))|~sdtlseqdt0(X1,szszuzczcdt0(X3))|~sdtlseqdt0(X3,X2)|~aElementOf0(X1,szNzAzT0)|~aElementOf0(X3,szNzAzT0)|~aElementOf0(X2,szNzAzT0)),inference(csr,[status(thm)],[6969,78])).
% cnf(7092,plain,(sdtlseqdt0(X1,X2)|sdtlseqdt0(X2,X3)|~sdtlseqdt0(X1,szszuzczcdt0(X3))|~aElementOf0(X2,szNzAzT0)|~aElementOf0(X1,szNzAzT0)|~aElementOf0(X3,szNzAzT0)),inference(csr,[status(thm)],[583,78])).
% cnf(7139,plain,(sdtlseqdt0(X1,X2)|sdtlseqdt0(X2,X1)|~aElementOf0(X1,szNzAzT0)|~aElementOf0(X2,szNzAzT0)),inference(spm,[status(thm)],[7092,107,theory(equality)])).
% cnf(7930,plain,(sdtlseqdt0(X1,xn)|sdtlseqdt0(xn,X1)|~aElementOf0(X1,szNzAzT0)),inference(spm,[status(thm)],[7139,72,theory(equality)])).
% cnf(7931,plain,(sdtlseqdt0(X1,xm)|sdtlseqdt0(xm,X1)|~aElementOf0(X1,szNzAzT0)),inference(spm,[status(thm)],[7139,73,theory(equality)])).
% cnf(8038,plain,(sdtlseqdt0(xn,xm)|sdtlseqdt0(xm,xn)),inference(spm,[status(thm)],[7930,73,theory(equality)])).
% cnf(8053,plain,(sdtlseqdt0(xn,xm)),inference(sr,[status(thm)],[8038,2363,theory(equality)])).
% cnf(8060,plain,(sdtlseqdt0(X1,xm)|~sdtlseqdt0(X1,xn)|~aElementOf0(xn,szNzAzT0)|~aElementOf0(xm,szNzAzT0)|~aElementOf0(X1,szNzAzT0)),inference(spm,[status(thm)],[122,8053,theory(equality)])).
% cnf(8075,plain,(sdtlseqdt0(X1,xm)|~sdtlseqdt0(X1,xn)|$false|~aElementOf0(xm,szNzAzT0)|~aElementOf0(X1,szNzAzT0)),inference(rw,[status(thm)],[8060,72,theory(equality)])).
% cnf(8076,plain,(sdtlseqdt0(X1,xm)|~sdtlseqdt0(X1,xn)|$false|$false|~aElementOf0(X1,szNzAzT0)),inference(rw,[status(thm)],[8075,73,theory(equality)])).
% cnf(8077,plain,(sdtlseqdt0(X1,xm)|~sdtlseqdt0(X1,xn)|~aElementOf0(X1,szNzAzT0)),inference(cn,[status(thm)],[8076,theory(equality)])).
% cnf(8352,plain,(sdtlseqdt0(esk1_1(xn),xm)|sz00=xn|~aElementOf0(esk1_1(xn),szNzAzT0)|~aElementOf0(xn,szNzAzT0)),inference(spm,[status(thm)],[8077,714,theory(equality)])).
% cnf(8389,plain,(sdtlseqdt0(esk1_1(xn),xm)|sz00=xn|~aElementOf0(esk1_1(xn),szNzAzT0)|$false),inference(rw,[status(thm)],[8352,72,theory(equality)])).
% cnf(8390,plain,(sdtlseqdt0(esk1_1(xn),xm)|sz00=xn|~aElementOf0(esk1_1(xn),szNzAzT0)),inference(cn,[status(thm)],[8389,theory(equality)])).
% cnf(8483,plain,(sdtlseqdt0(xm,xm)),inference(spm,[status(thm)],[7931,73,theory(equality)])).
% cnf(8485,plain,(sdtlseqdt0(xm,szszuzczcdt0(X1))|sdtlseqdt0(szszuzczcdt0(X1),xm)|~aElementOf0(X1,szNzAzT0)),inference(spm,[status(thm)],[7931,78,theory(equality)])).
% cnf(8913,plain,(sz00=xn|sdtlseqdt0(xn,szszuzczcdt0(xm))|~aElementOf0(xm,szNzAzT0)|~aElementOf0(xn,szNzAzT0)|~aElementOf0(esk1_1(xn),szNzAzT0)),inference(spm,[status(thm)],[1059,8390,theory(equality)])).
% cnf(8921,plain,(sz00=xn|sdtlseqdt0(xn,szszuzczcdt0(xm))|$false|~aElementOf0(xn,szNzAzT0)|~aElementOf0(esk1_1(xn),szNzAzT0)),inference(rw,[status(thm)],[8913,73,theory(equality)])).
% cnf(8922,plain,(sz00=xn|sdtlseqdt0(xn,szszuzczcdt0(xm))|$false|$false|~aElementOf0(esk1_1(xn),szNzAzT0)),inference(rw,[status(thm)],[8921,72,theory(equality)])).
% cnf(8923,plain,(sz00=xn|sdtlseqdt0(xn,szszuzczcdt0(xm))|~aElementOf0(esk1_1(xn),szNzAzT0)),inference(cn,[status(thm)],[8922,theory(equality)])).
% cnf(8934,plain,(xn=sz00|sdtlseqdt0(xn,szszuzczcdt0(xm))|~aElementOf0(xn,szNzAzT0)),inference(spm,[status(thm)],[8923,84,theory(equality)])).
% cnf(8940,plain,(xn=sz00|sdtlseqdt0(xn,szszuzczcdt0(xm))|$false),inference(rw,[status(thm)],[8934,72,theory(equality)])).
% cnf(8941,plain,(xn=sz00|sdtlseqdt0(xn,szszuzczcdt0(xm))),inference(cn,[status(thm)],[8940,theory(equality)])).
% cnf(8948,plain,(sdtlseqdt0(xn,szszuzczcdt0(X1))|xn=sz00|~sdtlseqdt0(xm,X1)|~aElementOf0(xn,szNzAzT0)|~aElementOf0(xm,szNzAzT0)|~aElementOf0(X1,szNzAzT0)),inference(spm,[status(thm)],[6970,8941,theory(equality)])).
% cnf(8967,plain,(sdtlseqdt0(xn,szszuzczcdt0(X1))|xn=sz00|~sdtlseqdt0(xm,X1)|$false|~aElementOf0(xm,szNzAzT0)|~aElementOf0(X1,szNzAzT0)),inference(rw,[status(thm)],[8948,72,theory(equality)])).
% cnf(8968,plain,(sdtlseqdt0(xn,szszuzczcdt0(X1))|xn=sz00|~sdtlseqdt0(xm,X1)|$false|$false|~aElementOf0(X1,szNzAzT0)),inference(rw,[status(thm)],[8967,73,theory(equality)])).
% cnf(8969,plain,(sdtlseqdt0(xn,szszuzczcdt0(X1))|xn=sz00|~sdtlseqdt0(xm,X1)|~aElementOf0(X1,szNzAzT0)),inference(cn,[status(thm)],[8968,theory(equality)])).
% cnf(9609,plain,(sdtlseqdt0(xm,szszuzczcdt0(xm))|~aElementOf0(xm,szNzAzT0)),inference(spm,[status(thm)],[1475,8485,theory(equality)])).
% cnf(9623,plain,(sdtlseqdt0(xm,szszuzczcdt0(xm))|$false),inference(rw,[status(thm)],[9609,73,theory(equality)])).
% cnf(9624,plain,(sdtlseqdt0(xm,szszuzczcdt0(xm))),inference(cn,[status(thm)],[9623,theory(equality)])).
% cnf(9633,plain,(sdtlseqdt0(xm,szszuzczcdt0(X1))|~sdtlseqdt0(xm,X1)|~aElementOf0(xm,szNzAzT0)|~aElementOf0(X1,szNzAzT0)),inference(spm,[status(thm)],[6970,9624,theory(equality)])).
% cnf(9652,plain,(sdtlseqdt0(xm,szszuzczcdt0(X1))|~sdtlseqdt0(xm,X1)|$false|~aElementOf0(X1,szNzAzT0)),inference(rw,[status(thm)],[9633,73,theory(equality)])).
% cnf(9653,plain,(sdtlseqdt0(xm,szszuzczcdt0(X1))|~sdtlseqdt0(xm,X1)|~aElementOf0(X1,szNzAzT0)),inference(cn,[status(thm)],[9652,theory(equality)])).
% cnf(9950,plain,(xn=szszuzczcdt0(X1)|sdtlseqdt0(xn,X1)|xn=sz00|~aElementOf0(xn,szNzAzT0)|~aElementOf0(X1,szNzAzT0)|~sdtlseqdt0(xm,X1)),inference(spm,[status(thm)],[3241,8969,theory(equality)])).
% cnf(9974,plain,(xn=szszuzczcdt0(X1)|sdtlseqdt0(xn,X1)|xn=sz00|$false|~aElementOf0(X1,szNzAzT0)|~sdtlseqdt0(xm,X1)),inference(rw,[status(thm)],[9950,72,theory(equality)])).
% cnf(9975,plain,(xn=szszuzczcdt0(X1)|sdtlseqdt0(xn,X1)|xn=sz00|~aElementOf0(X1,szNzAzT0)|~sdtlseqdt0(xm,X1)),inference(cn,[status(thm)],[9974,theory(equality)])).
% cnf(10034,plain,(szszuzczcdt0(X1)=xn|sdtlseqdt0(xn,X1)|~sdtlseqdt0(xm,X1)|~aElementOf0(X1,szNzAzT0)),inference(csr,[status(thm)],[9975,2679])).
% cnf(10223,plain,(sdtlseqdt0(xm,xn)|sdtlseqdt0(xn,X1)|~sdtlseqdt0(xm,X1)|~aElementOf0(X1,szNzAzT0)),inference(spm,[status(thm)],[9653,10034,theory(equality)])).
% cnf(10664,plain,(sdtlseqdt0(xn,X1)|~sdtlseqdt0(xm,X1)|~aElementOf0(X1,szNzAzT0)),inference(sr,[status(thm)],[10223,2363,theory(equality)])).
% cnf(10668,plain,(sz00=xn|~aElementOf0(xn,szNzAzT0)|~sdtlseqdt0(xm,esk1_1(xn))|~aElementOf0(esk1_1(xn),szNzAzT0)),inference(spm,[status(thm)],[3861,10664,theory(equality)])).
% cnf(10701,plain,(sz00=xn|$false|~sdtlseqdt0(xm,esk1_1(xn))|~aElementOf0(esk1_1(xn),szNzAzT0)),inference(rw,[status(thm)],[10668,72,theory(equality)])).
% cnf(10702,plain,(sz00=xn|~sdtlseqdt0(xm,esk1_1(xn))|~aElementOf0(esk1_1(xn),szNzAzT0)),inference(cn,[status(thm)],[10701,theory(equality)])).
% cnf(10848,plain,(xn=sz00|~aElementOf0(esk1_1(xn),szNzAzT0)|~sdtlseqdt0(szszuzczcdt0(xm),xn)|~aElementOf0(xm,szNzAzT0)|~aElementOf0(xn,szNzAzT0)),inference(spm,[status(thm)],[10702,1107,theory(equality)])).
% cnf(10857,plain,(xn=sz00|~aElementOf0(esk1_1(xn),szNzAzT0)|~sdtlseqdt0(szszuzczcdt0(xm),xn)|$false|~aElementOf0(xn,szNzAzT0)),inference(rw,[status(thm)],[10848,73,theory(equality)])).
% cnf(10858,plain,(xn=sz00|~aElementOf0(esk1_1(xn),szNzAzT0)|~sdtlseqdt0(szszuzczcdt0(xm),xn)|$false|$false),inference(rw,[status(thm)],[10857,72,theory(equality)])).
% cnf(10859,plain,(xn=sz00|~aElementOf0(esk1_1(xn),szNzAzT0)|~sdtlseqdt0(szszuzczcdt0(xm),xn)),inference(cn,[status(thm)],[10858,theory(equality)])).
% cnf(10871,plain,(xn=sz00|~sdtlseqdt0(szszuzczcdt0(xm),xn)|~aElementOf0(xn,szNzAzT0)),inference(spm,[status(thm)],[10859,84,theory(equality)])).
% cnf(10877,plain,(xn=sz00|~sdtlseqdt0(szszuzczcdt0(xm),xn)|$false),inference(rw,[status(thm)],[10871,72,theory(equality)])).
% cnf(10878,plain,(xn=sz00|~sdtlseqdt0(szszuzczcdt0(xm),xn)),inference(cn,[status(thm)],[10877,theory(equality)])).
% cnf(20972,negated_conjecture,(sdtlseqdt0(szszuzczcdt0(xm),X1)|xn=xm|slbdtrb0(X1)!=slbdtrb0(xn)|~aElementOf0(X1,szNzAzT0)|~aElementOf0(szszuzczcdt0(xn),szNzAzT0)),inference(sr,[status(thm)],[1389,2363,theory(equality)])).
% cnf(21009,negated_conjecture,(xn=xm|~aElementOf0(xm,szNzAzT0)|slbdtrb0(sz00)!=slbdtrb0(xn)|~aElementOf0(szszuzczcdt0(xn),szNzAzT0)|~aElementOf0(sz00,szNzAzT0)),inference(spm,[status(thm)],[126,20972,theory(equality)])).
% cnf(21012,negated_conjecture,(xn=sz00|xn=xm|~aElementOf0(szszuzczcdt0(xn),szNzAzT0)|~aElementOf0(xn,szNzAzT0)),inference(spm,[status(thm)],[10878,20972,theory(equality)])).
% cnf(21053,negated_conjecture,(xn=xm|$false|slbdtrb0(sz00)!=slbdtrb0(xn)|~aElementOf0(szszuzczcdt0(xn),szNzAzT0)|~aElementOf0(sz00,szNzAzT0)),inference(rw,[status(thm)],[21009,73,theory(equality)])).
% cnf(21054,negated_conjecture,(xn=xm|$false|slcrc0!=slbdtrb0(xn)|~aElementOf0(szszuzczcdt0(xn),szNzAzT0)|~aElementOf0(sz00,szNzAzT0)),inference(rw,[status(thm)],[21053,127,theory(equality)])).
% cnf(21055,negated_conjecture,(xn=xm|$false|slcrc0!=slbdtrb0(xn)|~aElementOf0(szszuzczcdt0(xn),szNzAzT0)|$false),inference(rw,[status(thm)],[21054,123,theory(equality)])).
% cnf(21056,negated_conjecture,(xn=xm|slcrc0!=slbdtrb0(xn)|~aElementOf0(szszuzczcdt0(xn),szNzAzT0)),inference(cn,[status(thm)],[21055,theory(equality)])).
% cnf(21062,negated_conjecture,(xn=sz00|xn=xm|~aElementOf0(szszuzczcdt0(xn),szNzAzT0)|$false),inference(rw,[status(thm)],[21012,72,theory(equality)])).
% cnf(21063,negated_conjecture,(xn=sz00|xn=xm|~aElementOf0(szszuzczcdt0(xn),szNzAzT0)),inference(cn,[status(thm)],[21062,theory(equality)])).
% cnf(21084,negated_conjecture,(xn=xm|xn=sz00|~aElementOf0(xn,szNzAzT0)),inference(spm,[status(thm)],[21063,78,theory(equality)])).
% cnf(21085,negated_conjecture,(xn=xm|xn=sz00|$false),inference(rw,[status(thm)],[21084,72,theory(equality)])).
% cnf(21086,negated_conjecture,(xn=xm|xn=sz00),inference(cn,[status(thm)],[21085,theory(equality)])).
% cnf(21126,negated_conjecture,(xn=sz00|~sdtlseqdt0(xm,xm)),inference(spm,[status(thm)],[2254,21086,theory(equality)])).
% cnf(21289,negated_conjecture,(xn=sz00|$false),inference(rw,[status(thm)],[21126,8483,theory(equality)])).
% cnf(21290,negated_conjecture,(xn=sz00),inference(cn,[status(thm)],[21289,theory(equality)])).
% cnf(21348,negated_conjecture,(sz00=xm|slbdtrb0(xn)!=slcrc0|~aElementOf0(szszuzczcdt0(xn),szNzAzT0)),inference(rw,[status(thm)],[21056,21290,theory(equality)])).
% cnf(21349,negated_conjecture,(sz00=xm|$false|~aElementOf0(szszuzczcdt0(xn),szNzAzT0)),inference(rw,[status(thm)],[inference(rw,[status(thm)],[21348,21290,theory(equality)]),127,theory(equality)])).
% cnf(21350,negated_conjecture,(sz00=xm|$false|~aElementOf0(szszuzczcdt0(sz00),szNzAzT0)),inference(rw,[status(thm)],[21349,21290,theory(equality)])).
% cnf(21351,negated_conjecture,(sz00=xm|~aElementOf0(szszuzczcdt0(sz00),szNzAzT0)),inference(cn,[status(thm)],[21350,theory(equality)])).
% cnf(21352,negated_conjecture,(~aElementOf0(szszuzczcdt0(sz00),szNzAzT0)),inference(sr,[status(thm)],[21351,2371,theory(equality)])).
% cnf(21881,plain,(aElementOf0(szszuzczcdt0(sz00),szNzAzT0)|$false),inference(rw,[status(thm)],[inference(rw,[status(thm)],[4186,21290,theory(equality)]),851,theory(equality)])).
% cnf(21882,plain,(aElementOf0(szszuzczcdt0(sz00),szNzAzT0)),inference(cn,[status(thm)],[21881,theory(equality)])).
% cnf(22330,negated_conjecture,($false),inference(rw,[status(thm)],[21352,21882,theory(equality)])).
% cnf(22331,negated_conjecture,($false),inference(cn,[status(thm)],[22330,theory(equality)])).
% cnf(22332,negated_conjecture,($false),22331,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 2790
% # ...of these trivial : 107
% # ...subsumed : 1514
% # ...remaining for further processing: 1169
% # Other redundant clauses eliminated : 13
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 155
% # Backward-rewritten : 388
% # Generated clauses : 10820
% # ...of the previous two non-trivial : 9912
% # Contextual simplify-reflections : 1864
% # Paramodulations : 10678
% # Factorizations : 1
% # Equation resolutions : 138
% # Current number of processed clauses: 529
% # Positive orientable unit clauses: 29
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 12
% # Non-unit-clauses : 488
% # Current number of unprocessed clauses: 3399
% # ...number of literals in the above : 23020
% # Clause-clause subsumption calls (NU) : 38075
% # Rec. Clause-clause subsumption calls : 19178
% # Unit Clause-clause subsumption calls : 250
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 12
% # Indexed BW rewrite successes : 11
% # Backwards rewriting index: 458 leaves, 1.39+/-0.963 terms/leaf
% # Paramod-from index: 172 leaves, 1.08+/-0.305 terms/leaf
% # Paramod-into index: 292 leaves, 1.33+/-0.897 terms/leaf
% # -------------------------------------------------
% # User time : 0.841 s
% # System time : 0.023 s
% # Total time : 0.864 s
% # Maximum resident set size: 0 pages
% PrfWatch: 1.27 CPU 1.38 WC
% FINAL PrfWatch: 1.27 CPU 1.38 WC
% SZS output end Solution for /tmp/SystemOnTPTP16039/NUM541+1.tptp
%
%------------------------------------------------------------------------------