%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : NUM541+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 : art04.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:16 EST 2010
% Result : Theorem 1.07s
% Output : Solution 1.07s
% 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/SystemOnTPTP19526/NUM541+2.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP19526/NUM541+2.tptp
% SZS output start Solution for /tmp/SystemOnTPTP19526/NUM541+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 19622
% 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,![X1]:![X2]:((aElementOf0(X1,szNzAzT0)&aElementOf0(X2,szNzAzT0))=>(sdtlseqdt0(X1,X2)<=>sdtlseqdt0(szszuzczcdt0(X1),szszuzczcdt0(X2)))),file('/tmp/SRASS.s.p', mSuccLess)).
% fof(4, axiom,![X1]:(aElementOf0(X1,szNzAzT0)=>sdtlseqdt0(X1,szszuzczcdt0(X1))),file('/tmp/SRASS.s.p', mLessSucc)).
% fof(5, axiom,![X1]:(aElementOf0(X1,szNzAzT0)=>sdtlseqdt0(X1,X1)),file('/tmp/SRASS.s.p', mLessRefl)).
% fof(6, axiom,![X1]:![X2]:((aElementOf0(X1,szNzAzT0)&aElementOf0(X2,szNzAzT0))=>((sdtlseqdt0(X1,X2)&sdtlseqdt0(X2,X1))=>X1=X2)),file('/tmp/SRASS.s.p', mLessASymm)).
% fof(7, 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(8, axiom,![X1]:![X2]:((aElementOf0(X1,szNzAzT0)&aElementOf0(X2,szNzAzT0))=>(sdtlseqdt0(X1,X2)|sdtlseqdt0(szszuzczcdt0(X2),X1))),file('/tmp/SRASS.s.p', mLessTotal)).
% fof(9, axiom,(aElementOf0(xm,szNzAzT0)&aElementOf0(xn,szNzAzT0)),file('/tmp/SRASS.s.p', m__1936)).
% fof(10, 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(12, axiom,![X1]:(aElementOf0(X1,szNzAzT0)=>(aElementOf0(szszuzczcdt0(X1),szNzAzT0)&~(szszuzczcdt0(X1)=sz00))),file('/tmp/SRASS.s.p', mSuccNum)).
% fof(54, conjecture,(((sdtlseqdt0(szszuzczcdt0(xm),szszuzczcdt0(xn))&aElementOf0(xm,slbdtrb0(szszuzczcdt0(xn))))=>((sdtlseqdt0(szszuzczcdt0(xm),xn)|aElementOf0(xm,slbdtrb0(xn)))|xm=xn))&(((sdtlseqdt0(szszuzczcdt0(xm),xn)&aElementOf0(xm,slbdtrb0(xn)))|xm=xn)=>(sdtlseqdt0(szszuzczcdt0(xm),szszuzczcdt0(xn))|aElementOf0(xm,slbdtrb0(szszuzczcdt0(xn)))))),file('/tmp/SRASS.s.p', m__)).
% fof(55, negated_conjecture,~((((sdtlseqdt0(szszuzczcdt0(xm),szszuzczcdt0(xn))&aElementOf0(xm,slbdtrb0(szszuzczcdt0(xn))))=>((sdtlseqdt0(szszuzczcdt0(xm),xn)|aElementOf0(xm,slbdtrb0(xn)))|xm=xn))&(((sdtlseqdt0(szszuzczcdt0(xm),xn)&aElementOf0(xm,slbdtrb0(xn)))|xm=xn)=>(sdtlseqdt0(szszuzczcdt0(xm),szszuzczcdt0(xn))|aElementOf0(xm,slbdtrb0(szszuzczcdt0(xn))))))),inference(assume_negation,[status(cth)],[54])).
% 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])).
% fof(72, 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)],[3])).
% fof(73, 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)],[72])).
% fof(74, 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)],[73])).
% cnf(75,plain,(sdtlseqdt0(X2,X1)|~aElementOf0(X1,szNzAzT0)|~aElementOf0(X2,szNzAzT0)|~sdtlseqdt0(szszuzczcdt0(X2),szszuzczcdt0(X1))),inference(split_conjunct,[status(thm)],[74])).
% cnf(76,plain,(sdtlseqdt0(szszuzczcdt0(X2),szszuzczcdt0(X1))|~aElementOf0(X1,szNzAzT0)|~aElementOf0(X2,szNzAzT0)|~sdtlseqdt0(X2,X1)),inference(split_conjunct,[status(thm)],[74])).
% fof(77, plain,![X1]:(~(aElementOf0(X1,szNzAzT0))|sdtlseqdt0(X1,szszuzczcdt0(X1))),inference(fof_nnf,[status(thm)],[4])).
% fof(78, plain,![X2]:(~(aElementOf0(X2,szNzAzT0))|sdtlseqdt0(X2,szszuzczcdt0(X2))),inference(variable_rename,[status(thm)],[77])).
% cnf(79,plain,(sdtlseqdt0(X1,szszuzczcdt0(X1))|~aElementOf0(X1,szNzAzT0)),inference(split_conjunct,[status(thm)],[78])).
% fof(80, plain,![X1]:(~(aElementOf0(X1,szNzAzT0))|sdtlseqdt0(X1,X1)),inference(fof_nnf,[status(thm)],[5])).
% fof(81, plain,![X2]:(~(aElementOf0(X2,szNzAzT0))|sdtlseqdt0(X2,X2)),inference(variable_rename,[status(thm)],[80])).
% cnf(82,plain,(sdtlseqdt0(X1,X1)|~aElementOf0(X1,szNzAzT0)),inference(split_conjunct,[status(thm)],[81])).
% fof(83, plain,![X1]:![X2]:((~(aElementOf0(X1,szNzAzT0))|~(aElementOf0(X2,szNzAzT0)))|((~(sdtlseqdt0(X1,X2))|~(sdtlseqdt0(X2,X1)))|X1=X2)),inference(fof_nnf,[status(thm)],[6])).
% fof(84, plain,![X3]:![X4]:((~(aElementOf0(X3,szNzAzT0))|~(aElementOf0(X4,szNzAzT0)))|((~(sdtlseqdt0(X3,X4))|~(sdtlseqdt0(X4,X3)))|X3=X4)),inference(variable_rename,[status(thm)],[83])).
% cnf(85,plain,(X1=X2|~sdtlseqdt0(X2,X1)|~sdtlseqdt0(X1,X2)|~aElementOf0(X2,szNzAzT0)|~aElementOf0(X1,szNzAzT0)),inference(split_conjunct,[status(thm)],[84])).
% fof(86, 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)],[7])).
% fof(87, 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)],[86])).
% cnf(88,plain,(sdtlseqdt0(X1,X2)|~sdtlseqdt0(X3,X2)|~sdtlseqdt0(X1,X3)|~aElementOf0(X2,szNzAzT0)|~aElementOf0(X3,szNzAzT0)|~aElementOf0(X1,szNzAzT0)),inference(split_conjunct,[status(thm)],[87])).
% fof(89, plain,![X1]:![X2]:((~(aElementOf0(X1,szNzAzT0))|~(aElementOf0(X2,szNzAzT0)))|(sdtlseqdt0(X1,X2)|sdtlseqdt0(szszuzczcdt0(X2),X1))),inference(fof_nnf,[status(thm)],[8])).
% fof(90, plain,![X3]:![X4]:((~(aElementOf0(X3,szNzAzT0))|~(aElementOf0(X4,szNzAzT0)))|(sdtlseqdt0(X3,X4)|sdtlseqdt0(szszuzczcdt0(X4),X3))),inference(variable_rename,[status(thm)],[89])).
% cnf(91,plain,(sdtlseqdt0(szszuzczcdt0(X1),X2)|sdtlseqdt0(X2,X1)|~aElementOf0(X1,szNzAzT0)|~aElementOf0(X2,szNzAzT0)),inference(split_conjunct,[status(thm)],[90])).
% cnf(92,plain,(aElementOf0(xn,szNzAzT0)),inference(split_conjunct,[status(thm)],[9])).
% cnf(93,plain,(aElementOf0(xm,szNzAzT0)),inference(split_conjunct,[status(thm)],[9])).
% fof(94, 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)],[10])).
% fof(95, 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)],[94])).
% fof(96, 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(esk1_2(X4,X5),X5))|(~(aElementOf0(esk1_2(X4,X5),szNzAzT0))|~(sdtlseqdt0(szszuzczcdt0(esk1_2(X4,X5)),X4))))&(aElementOf0(esk1_2(X4,X5),X5)|(aElementOf0(esk1_2(X4,X5),szNzAzT0)&sdtlseqdt0(szszuzczcdt0(esk1_2(X4,X5)),X4)))))|X5=slbdtrb0(X4)))),inference(skolemize,[status(esa)],[95])).
% fof(97, 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(esk1_2(X4,X5),X5))|(~(aElementOf0(esk1_2(X4,X5),szNzAzT0))|~(sdtlseqdt0(szszuzczcdt0(esk1_2(X4,X5)),X4))))&(aElementOf0(esk1_2(X4,X5),X5)|(aElementOf0(esk1_2(X4,X5),szNzAzT0)&sdtlseqdt0(szszuzczcdt0(esk1_2(X4,X5)),X4)))))|X5=slbdtrb0(X4)))|~(aElementOf0(X4,szNzAzT0))),inference(shift_quantors,[status(thm)],[96])).
% fof(98, 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(esk1_2(X4,X5),X5))|(~(aElementOf0(esk1_2(X4,X5),szNzAzT0))|~(sdtlseqdt0(szszuzczcdt0(esk1_2(X4,X5)),X4))))|~(aSet0(X5)))|X5=slbdtrb0(X4))|~(aElementOf0(X4,szNzAzT0)))&(((((aElementOf0(esk1_2(X4,X5),szNzAzT0)|aElementOf0(esk1_2(X4,X5),X5))|~(aSet0(X5)))|X5=slbdtrb0(X4))|~(aElementOf0(X4,szNzAzT0)))&((((sdtlseqdt0(szszuzczcdt0(esk1_2(X4,X5)),X4)|aElementOf0(esk1_2(X4,X5),X5))|~(aSet0(X5)))|X5=slbdtrb0(X4))|~(aElementOf0(X4,szNzAzT0)))))),inference(distribute,[status(thm)],[97])).
% cnf(104,plain,(sdtlseqdt0(szszuzczcdt0(X3),X1)|~aElementOf0(X1,szNzAzT0)|X2!=slbdtrb0(X1)|~aElementOf0(X3,X2)),inference(split_conjunct,[status(thm)],[98])).
% fof(109, plain,![X1]:(~(aElementOf0(X1,szNzAzT0))|(aElementOf0(szszuzczcdt0(X1),szNzAzT0)&~(szszuzczcdt0(X1)=sz00))),inference(fof_nnf,[status(thm)],[12])).
% fof(110, plain,![X2]:(~(aElementOf0(X2,szNzAzT0))|(aElementOf0(szszuzczcdt0(X2),szNzAzT0)&~(szszuzczcdt0(X2)=sz00))),inference(variable_rename,[status(thm)],[109])).
% fof(111, plain,![X2]:((aElementOf0(szszuzczcdt0(X2),szNzAzT0)|~(aElementOf0(X2,szNzAzT0)))&(~(szszuzczcdt0(X2)=sz00)|~(aElementOf0(X2,szNzAzT0)))),inference(distribute,[status(thm)],[110])).
% cnf(113,plain,(aElementOf0(szszuzczcdt0(X1),szNzAzT0)|~aElementOf0(X1,szNzAzT0)),inference(split_conjunct,[status(thm)],[111])).
% fof(289, negated_conjecture,(((sdtlseqdt0(szszuzczcdt0(xm),szszuzczcdt0(xn))&aElementOf0(xm,slbdtrb0(szszuzczcdt0(xn))))&((~(sdtlseqdt0(szszuzczcdt0(xm),xn))&~(aElementOf0(xm,slbdtrb0(xn))))&~(xm=xn)))|(((sdtlseqdt0(szszuzczcdt0(xm),xn)&aElementOf0(xm,slbdtrb0(xn)))|xm=xn)&(~(sdtlseqdt0(szszuzczcdt0(xm),szszuzczcdt0(xn)))&~(aElementOf0(xm,slbdtrb0(szszuzczcdt0(xn))))))),inference(fof_nnf,[status(thm)],[55])).
% fof(290, negated_conjecture,((((((sdtlseqdt0(szszuzczcdt0(xm),xn)|xm=xn)|sdtlseqdt0(szszuzczcdt0(xm),szszuzczcdt0(xn)))&((aElementOf0(xm,slbdtrb0(xn))|xm=xn)|sdtlseqdt0(szszuzczcdt0(xm),szszuzczcdt0(xn))))&((~(sdtlseqdt0(szszuzczcdt0(xm),szszuzczcdt0(xn)))|sdtlseqdt0(szszuzczcdt0(xm),szszuzczcdt0(xn)))&(~(aElementOf0(xm,slbdtrb0(szszuzczcdt0(xn))))|sdtlseqdt0(szszuzczcdt0(xm),szszuzczcdt0(xn)))))&((((sdtlseqdt0(szszuzczcdt0(xm),xn)|xm=xn)|aElementOf0(xm,slbdtrb0(szszuzczcdt0(xn))))&((aElementOf0(xm,slbdtrb0(xn))|xm=xn)|aElementOf0(xm,slbdtrb0(szszuzczcdt0(xn)))))&((~(sdtlseqdt0(szszuzczcdt0(xm),szszuzczcdt0(xn)))|aElementOf0(xm,slbdtrb0(szszuzczcdt0(xn))))&(~(aElementOf0(xm,slbdtrb0(szszuzczcdt0(xn))))|aElementOf0(xm,slbdtrb0(szszuzczcdt0(xn)))))))&((((((sdtlseqdt0(szszuzczcdt0(xm),xn)|xm=xn)|~(sdtlseqdt0(szszuzczcdt0(xm),xn)))&((aElementOf0(xm,slbdtrb0(xn))|xm=xn)|~(sdtlseqdt0(szszuzczcdt0(xm),xn))))&((~(sdtlseqdt0(szszuzczcdt0(xm),szszuzczcdt0(xn)))|~(sdtlseqdt0(szszuzczcdt0(xm),xn)))&(~(aElementOf0(xm,slbdtrb0(szszuzczcdt0(xn))))|~(sdtlseqdt0(szszuzczcdt0(xm),xn)))))&((((sdtlseqdt0(szszuzczcdt0(xm),xn)|xm=xn)|~(aElementOf0(xm,slbdtrb0(xn))))&((aElementOf0(xm,slbdtrb0(xn))|xm=xn)|~(aElementOf0(xm,slbdtrb0(xn)))))&((~(sdtlseqdt0(szszuzczcdt0(xm),szszuzczcdt0(xn)))|~(aElementOf0(xm,slbdtrb0(xn))))&(~(aElementOf0(xm,slbdtrb0(szszuzczcdt0(xn))))|~(aElementOf0(xm,slbdtrb0(xn)))))))&((((sdtlseqdt0(szszuzczcdt0(xm),xn)|xm=xn)|~(xm=xn))&((aElementOf0(xm,slbdtrb0(xn))|xm=xn)|~(xm=xn)))&((~(sdtlseqdt0(szszuzczcdt0(xm),szszuzczcdt0(xn)))|~(xm=xn))&(~(aElementOf0(xm,slbdtrb0(szszuzczcdt0(xn))))|~(xm=xn)))))),inference(distribute,[status(thm)],[289])).
% cnf(292,negated_conjecture,(xm!=xn|~sdtlseqdt0(szszuzczcdt0(xm),szszuzczcdt0(xn))),inference(split_conjunct,[status(thm)],[290])).
% cnf(296,negated_conjecture,(~aElementOf0(xm,slbdtrb0(xn))|~sdtlseqdt0(szszuzczcdt0(xm),szszuzczcdt0(xn))),inference(split_conjunct,[status(thm)],[290])).
% cnf(300,negated_conjecture,(~sdtlseqdt0(szszuzczcdt0(xm),xn)|~sdtlseqdt0(szszuzczcdt0(xm),szszuzczcdt0(xn))),inference(split_conjunct,[status(thm)],[290])).
% cnf(309,negated_conjecture,(sdtlseqdt0(szszuzczcdt0(xm),szszuzczcdt0(xn))|xm=xn|aElementOf0(xm,slbdtrb0(xn))),inference(split_conjunct,[status(thm)],[290])).
% cnf(367,negated_conjecture,(sdtlseqdt0(szszuzczcdt0(xn),xm)|xn!=xm|~aElementOf0(szszuzczcdt0(xn),szNzAzT0)|~aElementOf0(xm,szNzAzT0)),inference(spm,[status(thm)],[292,91,theory(equality)])).
% cnf(368,negated_conjecture,(sdtlseqdt0(szszuzczcdt0(xn),xm)|~aElementOf0(xm,slbdtrb0(xn))|~aElementOf0(szszuzczcdt0(xn),szNzAzT0)|~aElementOf0(xm,szNzAzT0)),inference(spm,[status(thm)],[296,91,theory(equality)])).
% cnf(370,negated_conjecture,(sdtlseqdt0(szszuzczcdt0(xn),xm)|xn!=xm|~aElementOf0(szszuzczcdt0(xn),szNzAzT0)|$false),inference(rw,[status(thm)],[367,93,theory(equality)])).
% cnf(371,negated_conjecture,(sdtlseqdt0(szszuzczcdt0(xn),xm)|xn!=xm|~aElementOf0(szszuzczcdt0(xn),szNzAzT0)),inference(cn,[status(thm)],[370,theory(equality)])).
% cnf(372,negated_conjecture,(sdtlseqdt0(szszuzczcdt0(xn),xm)|~aElementOf0(xm,slbdtrb0(xn))|~aElementOf0(szszuzczcdt0(xn),szNzAzT0)|$false),inference(rw,[status(thm)],[368,93,theory(equality)])).
% cnf(373,negated_conjecture,(sdtlseqdt0(szszuzczcdt0(xn),xm)|~aElementOf0(xm,slbdtrb0(xn))|~aElementOf0(szszuzczcdt0(xn),szNzAzT0)),inference(cn,[status(thm)],[372,theory(equality)])).
% cnf(419,negated_conjecture,(xn!=xm|~sdtlseqdt0(xm,xn)|~aElementOf0(xm,szNzAzT0)|~aElementOf0(xn,szNzAzT0)),inference(spm,[status(thm)],[292,76,theory(equality)])).
% cnf(421,negated_conjecture,(~sdtlseqdt0(szszuzczcdt0(xm),xn)|~sdtlseqdt0(xm,xn)|~aElementOf0(xm,szNzAzT0)|~aElementOf0(xn,szNzAzT0)),inference(spm,[status(thm)],[300,76,theory(equality)])).
% cnf(424,negated_conjecture,(xn!=xm|~sdtlseqdt0(xm,xn)|$false|~aElementOf0(xn,szNzAzT0)),inference(rw,[status(thm)],[419,93,theory(equality)])).
% cnf(425,negated_conjecture,(xn!=xm|~sdtlseqdt0(xm,xn)|$false|$false),inference(rw,[status(thm)],[424,92,theory(equality)])).
% cnf(426,negated_conjecture,(xn!=xm|~sdtlseqdt0(xm,xn)),inference(cn,[status(thm)],[425,theory(equality)])).
% cnf(430,negated_conjecture,(~sdtlseqdt0(szszuzczcdt0(xm),xn)|~sdtlseqdt0(xm,xn)|$false|~aElementOf0(xn,szNzAzT0)),inference(rw,[status(thm)],[421,93,theory(equality)])).
% cnf(431,negated_conjecture,(~sdtlseqdt0(szszuzczcdt0(xm),xn)|~sdtlseqdt0(xm,xn)|$false|$false),inference(rw,[status(thm)],[430,92,theory(equality)])).
% cnf(432,negated_conjecture,(~sdtlseqdt0(szszuzczcdt0(xm),xn)|~sdtlseqdt0(xm,xn)),inference(cn,[status(thm)],[431,theory(equality)])).
% cnf(448,negated_conjecture,(sdtlseqdt0(xm,xn)|xn=xm|aElementOf0(xm,slbdtrb0(xn))|~aElementOf0(xm,szNzAzT0)|~aElementOf0(xn,szNzAzT0)),inference(spm,[status(thm)],[75,309,theory(equality)])).
% cnf(451,negated_conjecture,(sdtlseqdt0(xm,xn)|xn=xm|aElementOf0(xm,slbdtrb0(xn))|$false|~aElementOf0(xn,szNzAzT0)),inference(rw,[status(thm)],[448,93,theory(equality)])).
% cnf(452,negated_conjecture,(sdtlseqdt0(xm,xn)|xn=xm|aElementOf0(xm,slbdtrb0(xn))|$false|$false),inference(rw,[status(thm)],[451,92,theory(equality)])).
% cnf(453,negated_conjecture,(sdtlseqdt0(xm,xn)|xn=xm|aElementOf0(xm,slbdtrb0(xn))),inference(cn,[status(thm)],[452,theory(equality)])).
% cnf(702,negated_conjecture,(sdtlseqdt0(xn,xm)|~sdtlseqdt0(xm,xn)|~aElementOf0(xn,szNzAzT0)|~aElementOf0(xm,szNzAzT0)),inference(spm,[status(thm)],[432,91,theory(equality)])).
% cnf(703,negated_conjecture,(sdtlseqdt0(xn,xm)|~sdtlseqdt0(xm,xn)|$false|~aElementOf0(xm,szNzAzT0)),inference(rw,[status(thm)],[702,92,theory(equality)])).
% cnf(704,negated_conjecture,(sdtlseqdt0(xn,xm)|~sdtlseqdt0(xm,xn)|$false|$false),inference(rw,[status(thm)],[703,93,theory(equality)])).
% cnf(705,negated_conjecture,(sdtlseqdt0(xn,xm)|~sdtlseqdt0(xm,xn)),inference(cn,[status(thm)],[704,theory(equality)])).
% cnf(707,negated_conjecture,(xm=xn|~sdtlseqdt0(xm,xn)|~aElementOf0(xn,szNzAzT0)|~aElementOf0(xm,szNzAzT0)),inference(spm,[status(thm)],[85,705,theory(equality)])).
% cnf(711,negated_conjecture,(xm=xn|~sdtlseqdt0(xm,xn)|$false|~aElementOf0(xm,szNzAzT0)),inference(rw,[status(thm)],[707,92,theory(equality)])).
% cnf(712,negated_conjecture,(xm=xn|~sdtlseqdt0(xm,xn)|$false|$false),inference(rw,[status(thm)],[711,93,theory(equality)])).
% cnf(713,negated_conjecture,(xm=xn|~sdtlseqdt0(xm,xn)),inference(cn,[status(thm)],[712,theory(equality)])).
% cnf(714,negated_conjecture,(~sdtlseqdt0(xm,xn)),inference(csr,[status(thm)],[713,426])).
% cnf(715,negated_conjecture,(xn=xm|aElementOf0(xm,slbdtrb0(xn))),inference(sr,[status(thm)],[453,714,theory(equality)])).
% cnf(719,negated_conjecture,(sdtlseqdt0(szszuzczcdt0(xm),X1)|xn=xm|slbdtrb0(X1)!=slbdtrb0(xn)|~aElementOf0(X1,szNzAzT0)),inference(spm,[status(thm)],[104,715,theory(equality)])).
% cnf(757,negated_conjecture,(sdtlseqdt0(szszuzczcdt0(xn),xm)|xn=xm|~aElementOf0(szszuzczcdt0(xn),szNzAzT0)),inference(spm,[status(thm)],[373,715,theory(equality)])).
% cnf(760,negated_conjecture,(sdtlseqdt0(szszuzczcdt0(xn),xm)|~aElementOf0(szszuzczcdt0(xn),szNzAzT0)),inference(csr,[status(thm)],[757,371])).
% cnf(761,negated_conjecture,(sdtlseqdt0(X1,xm)|~sdtlseqdt0(X1,szszuzczcdt0(xn))|~aElementOf0(szszuzczcdt0(xn),szNzAzT0)|~aElementOf0(xm,szNzAzT0)|~aElementOf0(X1,szNzAzT0)),inference(spm,[status(thm)],[88,760,theory(equality)])).
% cnf(764,negated_conjecture,(sdtlseqdt0(X1,xm)|~sdtlseqdt0(X1,szszuzczcdt0(xn))|~aElementOf0(szszuzczcdt0(xn),szNzAzT0)|$false|~aElementOf0(X1,szNzAzT0)),inference(rw,[status(thm)],[761,93,theory(equality)])).
% cnf(765,negated_conjecture,(sdtlseqdt0(X1,xm)|~sdtlseqdt0(X1,szszuzczcdt0(xn))|~aElementOf0(szszuzczcdt0(xn),szNzAzT0)|~aElementOf0(X1,szNzAzT0)),inference(cn,[status(thm)],[764,theory(equality)])).
% cnf(911,negated_conjecture,(sdtlseqdt0(xn,xm)|~aElementOf0(szszuzczcdt0(xn),szNzAzT0)|~aElementOf0(xn,szNzAzT0)),inference(spm,[status(thm)],[765,79,theory(equality)])).
% cnf(916,negated_conjecture,(sdtlseqdt0(xn,xm)|~aElementOf0(szszuzczcdt0(xn),szNzAzT0)|$false),inference(rw,[status(thm)],[911,92,theory(equality)])).
% cnf(917,negated_conjecture,(sdtlseqdt0(xn,xm)|~aElementOf0(szszuzczcdt0(xn),szNzAzT0)),inference(cn,[status(thm)],[916,theory(equality)])).
% cnf(918,negated_conjecture,(sdtlseqdt0(X1,xm)|~sdtlseqdt0(X1,xn)|~aElementOf0(xn,szNzAzT0)|~aElementOf0(xm,szNzAzT0)|~aElementOf0(X1,szNzAzT0)|~aElementOf0(szszuzczcdt0(xn),szNzAzT0)),inference(spm,[status(thm)],[88,917,theory(equality)])).
% cnf(920,negated_conjecture,(sdtlseqdt0(X1,xm)|~sdtlseqdt0(X1,xn)|$false|~aElementOf0(xm,szNzAzT0)|~aElementOf0(X1,szNzAzT0)|~aElementOf0(szszuzczcdt0(xn),szNzAzT0)),inference(rw,[status(thm)],[918,92,theory(equality)])).
% cnf(921,negated_conjecture,(sdtlseqdt0(X1,xm)|~sdtlseqdt0(X1,xn)|$false|$false|~aElementOf0(X1,szNzAzT0)|~aElementOf0(szszuzczcdt0(xn),szNzAzT0)),inference(rw,[status(thm)],[920,93,theory(equality)])).
% cnf(922,negated_conjecture,(sdtlseqdt0(X1,xm)|~sdtlseqdt0(X1,xn)|~aElementOf0(X1,szNzAzT0)|~aElementOf0(szszuzczcdt0(xn),szNzAzT0)),inference(cn,[status(thm)],[921,theory(equality)])).
% cnf(945,negated_conjecture,(sdtlseqdt0(szszuzczcdt0(xm),xm)|xn=xm|~aElementOf0(szszuzczcdt0(xn),szNzAzT0)|~aElementOf0(szszuzczcdt0(xm),szNzAzT0)|~aElementOf0(xn,szNzAzT0)),inference(spm,[status(thm)],[922,719,theory(equality)])).
% cnf(959,negated_conjecture,(sdtlseqdt0(szszuzczcdt0(xm),xm)|xn=xm|~aElementOf0(szszuzczcdt0(xn),szNzAzT0)|~aElementOf0(szszuzczcdt0(xm),szNzAzT0)|$false),inference(rw,[status(thm)],[945,92,theory(equality)])).
% cnf(960,negated_conjecture,(sdtlseqdt0(szszuzczcdt0(xm),xm)|xn=xm|~aElementOf0(szszuzczcdt0(xn),szNzAzT0)|~aElementOf0(szszuzczcdt0(xm),szNzAzT0)),inference(cn,[status(thm)],[959,theory(equality)])).
% cnf(972,negated_conjecture,(xm=szszuzczcdt0(xm)|xn=xm|~sdtlseqdt0(xm,szszuzczcdt0(xm))|~aElementOf0(szszuzczcdt0(xm),szNzAzT0)|~aElementOf0(xm,szNzAzT0)|~aElementOf0(szszuzczcdt0(xn),szNzAzT0)),inference(spm,[status(thm)],[85,960,theory(equality)])).
% cnf(976,negated_conjecture,(xm=szszuzczcdt0(xm)|xn=xm|~sdtlseqdt0(xm,szszuzczcdt0(xm))|~aElementOf0(szszuzczcdt0(xm),szNzAzT0)|$false|~aElementOf0(szszuzczcdt0(xn),szNzAzT0)),inference(rw,[status(thm)],[972,93,theory(equality)])).
% cnf(977,negated_conjecture,(xm=szszuzczcdt0(xm)|xn=xm|~sdtlseqdt0(xm,szszuzczcdt0(xm))|~aElementOf0(szszuzczcdt0(xm),szNzAzT0)|~aElementOf0(szszuzczcdt0(xn),szNzAzT0)),inference(cn,[status(thm)],[976,theory(equality)])).
% cnf(1040,negated_conjecture,(szszuzczcdt0(xm)=xm|xn=xm|~aElementOf0(szszuzczcdt0(xm),szNzAzT0)|~aElementOf0(szszuzczcdt0(xn),szNzAzT0)|~aElementOf0(xm,szNzAzT0)),inference(spm,[status(thm)],[977,79,theory(equality)])).
% cnf(1041,negated_conjecture,(szszuzczcdt0(xm)=xm|xn=xm|~aElementOf0(szszuzczcdt0(xm),szNzAzT0)|~aElementOf0(szszuzczcdt0(xn),szNzAzT0)|$false),inference(rw,[status(thm)],[1040,93,theory(equality)])).
% cnf(1042,negated_conjecture,(szszuzczcdt0(xm)=xm|xn=xm|~aElementOf0(szszuzczcdt0(xm),szNzAzT0)|~aElementOf0(szszuzczcdt0(xn),szNzAzT0)),inference(cn,[status(thm)],[1041,theory(equality)])).
% cnf(1043,negated_conjecture,(szszuzczcdt0(xm)=xm|xn=xm|~aElementOf0(szszuzczcdt0(xm),szNzAzT0)|~aElementOf0(xn,szNzAzT0)),inference(spm,[status(thm)],[1042,113,theory(equality)])).
% cnf(1044,negated_conjecture,(szszuzczcdt0(xm)=xm|xn=xm|~aElementOf0(szszuzczcdt0(xm),szNzAzT0)|$false),inference(rw,[status(thm)],[1043,92,theory(equality)])).
% cnf(1045,negated_conjecture,(szszuzczcdt0(xm)=xm|xn=xm|~aElementOf0(szszuzczcdt0(xm),szNzAzT0)),inference(cn,[status(thm)],[1044,theory(equality)])).
% cnf(1046,negated_conjecture,(szszuzczcdt0(xm)=xm|xn=xm|~aElementOf0(xm,szNzAzT0)),inference(spm,[status(thm)],[1045,113,theory(equality)])).
% cnf(1047,negated_conjecture,(szszuzczcdt0(xm)=xm|xn=xm|$false),inference(rw,[status(thm)],[1046,93,theory(equality)])).
% cnf(1048,negated_conjecture,(szszuzczcdt0(xm)=xm|xn=xm),inference(cn,[status(thm)],[1047,theory(equality)])).
% cnf(1050,negated_conjecture,(xn=xm|~aElementOf0(xm,szNzAzT0)),inference(spm,[status(thm)],[71,1048,theory(equality)])).
% cnf(1077,negated_conjecture,(xn=xm|$false),inference(rw,[status(thm)],[1050,93,theory(equality)])).
% cnf(1078,negated_conjecture,(xn=xm),inference(cn,[status(thm)],[1077,theory(equality)])).
% cnf(1126,negated_conjecture,(~sdtlseqdt0(xm,xm)),inference(rw,[status(thm)],[714,1078,theory(equality)])).
% cnf(1217,negated_conjecture,(~aElementOf0(xm,szNzAzT0)),inference(spm,[status(thm)],[1126,82,theory(equality)])).
% cnf(1219,negated_conjecture,($false),inference(rw,[status(thm)],[1217,93,theory(equality)])).
% cnf(1220,negated_conjecture,($false),inference(cn,[status(thm)],[1219,theory(equality)])).
% cnf(1221,negated_conjecture,($false),1220,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 323
% # ...of these trivial : 2
% # ...subsumed : 50
% # ...remaining for further processing: 271
% # Other redundant clauses eliminated : 12
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 12
% # Backward-rewritten : 43
% # Generated clauses : 469
% # ...of the previous two non-trivial : 438
% # Contextual simplify-reflections : 57
% # Paramodulations : 441
% # Factorizations : 0
% # Equation resolutions : 28
% # Current number of processed clauses: 112
% # Positive orientable unit clauses: 10
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 3
% # Non-unit-clauses : 99
% # Current number of unprocessed clauses: 216
% # ...number of literals in the above : 1165
% # Clause-clause subsumption calls (NU) : 1092
% # Rec. Clause-clause subsumption calls : 681
% # Unit Clause-clause subsumption calls : 17
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 1
% # Indexed BW rewrite successes : 1
% # Backwards rewriting index: 100 leaves, 1.43+/-1.012 terms/leaf
% # Paramod-from index: 57 leaves, 1.02+/-0.131 terms/leaf
% # Paramod-into index: 93 leaves, 1.22+/-0.670 terms/leaf
% # -------------------------------------------------
% # User time : 0.057 s
% # System time : 0.006 s
% # Total time : 0.063 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.16 CPU 0.26 WC
% FINAL PrfWatch: 0.16 CPU 0.26 WC
% SZS output end Solution for /tmp/SystemOnTPTP19526/NUM541+2.tptp
%
%------------------------------------------------------------------------------