%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : NUM539+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 : art03.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:58:40 EST 2010
% Result : Theorem 1.01s
% Output : Solution 1.01s
% 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/SystemOnTPTP18738/NUM539+2.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP18738/NUM539+2.tptp
% SZS output start Solution for /tmp/SystemOnTPTP18738/NUM539+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 18834
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.02 WC
% # Preprocessing time : 0.020 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(1, axiom,![X1]:(X1=slcrc0<=>(aSet0(X1)&~(?[X2]:aElementOf0(X2,X1)))),file('/tmp/SRASS.s.p', mDefEmp)).
% fof(8, 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(9, 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(10, axiom,(((((((aSet0(xS)&![X1]:(aElementOf0(X1,xS)=>aElementOf0(X1,szNzAzT0)))&aSubsetOf0(xS,szNzAzT0))&aSet0(xT))&![X1]:(aElementOf0(X1,xT)=>aElementOf0(X1,szNzAzT0)))&aSubsetOf0(xT,szNzAzT0))&~((~(?[X1]:aElementOf0(X1,xS))|xS=slcrc0)))&~((~(?[X1]:aElementOf0(X1,xT))|xT=slcrc0))),file('/tmp/SRASS.s.p', m__1779)).
% fof(11, axiom,(((((aElementOf0(szmzizndt0(xS),xS)&![X1]:(aElementOf0(X1,xS)=>sdtlseqdt0(szmzizndt0(xS),X1)))&aElementOf0(szmzizndt0(xS),xT))&aElementOf0(szmzizndt0(xT),xT))&![X1]:(aElementOf0(X1,xT)=>sdtlseqdt0(szmzizndt0(xT),X1)))&aElementOf0(szmzizndt0(xT),xS)),file('/tmp/SRASS.s.p', m__1802)).
% fof(51, conjecture,((aElementOf0(szmzizndt0(xS),xS)&![X1]:(aElementOf0(X1,xS)=>sdtlseqdt0(szmzizndt0(xS),X1)))=>(![X1]:(aElementOf0(X1,xT)=>sdtlseqdt0(szmzizndt0(xS),X1))|szmzizndt0(xS)=szmzizndt0(xT))),file('/tmp/SRASS.s.p', m__)).
% fof(52, negated_conjecture,~(((aElementOf0(szmzizndt0(xS),xS)&![X1]:(aElementOf0(X1,xS)=>sdtlseqdt0(szmzizndt0(xS),X1)))=>(![X1]:(aElementOf0(X1,xT)=>sdtlseqdt0(szmzizndt0(xS),X1))|szmzizndt0(xS)=szmzizndt0(xT)))),inference(assume_negation,[status(cth)],[51])).
% fof(63, plain,![X1]:((~(X1=slcrc0)|(aSet0(X1)&![X2]:~(aElementOf0(X2,X1))))&((~(aSet0(X1))|?[X2]:aElementOf0(X2,X1))|X1=slcrc0)),inference(fof_nnf,[status(thm)],[1])).
% fof(64, plain,![X3]:((~(X3=slcrc0)|(aSet0(X3)&![X4]:~(aElementOf0(X4,X3))))&((~(aSet0(X3))|?[X5]:aElementOf0(X5,X3))|X3=slcrc0)),inference(variable_rename,[status(thm)],[63])).
% fof(65, plain,![X3]:((~(X3=slcrc0)|(aSet0(X3)&![X4]:~(aElementOf0(X4,X3))))&((~(aSet0(X3))|aElementOf0(esk1_1(X3),X3))|X3=slcrc0)),inference(skolemize,[status(esa)],[64])).
% fof(66, plain,![X3]:![X4]:(((~(aElementOf0(X4,X3))&aSet0(X3))|~(X3=slcrc0))&((~(aSet0(X3))|aElementOf0(esk1_1(X3),X3))|X3=slcrc0)),inference(shift_quantors,[status(thm)],[65])).
% fof(67, plain,![X3]:![X4]:(((~(aElementOf0(X4,X3))|~(X3=slcrc0))&(aSet0(X3)|~(X3=slcrc0)))&((~(aSet0(X3))|aElementOf0(esk1_1(X3),X3))|X3=slcrc0)),inference(distribute,[status(thm)],[66])).
% cnf(70,plain,(X1!=slcrc0|~aElementOf0(X2,X1)),inference(split_conjunct,[status(thm)],[67])).
% fof(95, 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)],[8])).
% fof(96, 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)],[95])).
% cnf(97,plain,(sdtlseqdt0(X1,X2)|~sdtlseqdt0(X3,X2)|~sdtlseqdt0(X1,X3)|~aElementOf0(X2,szNzAzT0)|~aElementOf0(X3,szNzAzT0)|~aElementOf0(X1,szNzAzT0)),inference(split_conjunct,[status(thm)],[96])).
% fof(98, 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)],[9])).
% fof(99, 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)],[98])).
% fof(100, 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(esk3_2(X4,X5),X4)&~(sdtlseqdt0(X5,esk3_2(X4,X5)))))|X5=szmzizndt0(X4)))),inference(skolemize,[status(esa)],[99])).
% fof(101, plain,![X4]:![X5]:![X6]:(((((~(aElementOf0(X6,X4))|sdtlseqdt0(X5,X6))&aElementOf0(X5,X4))|~(X5=szmzizndt0(X4)))&((~(aElementOf0(X5,X4))|(aElementOf0(esk3_2(X4,X5),X4)&~(sdtlseqdt0(X5,esk3_2(X4,X5)))))|X5=szmzizndt0(X4)))|(~(aSubsetOf0(X4,szNzAzT0))|X4=slcrc0)),inference(shift_quantors,[status(thm)],[100])).
% fof(102, 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(esk3_2(X4,X5),X4)|~(aElementOf0(X5,X4)))|X5=szmzizndt0(X4))|(~(aSubsetOf0(X4,szNzAzT0))|X4=slcrc0))&(((~(sdtlseqdt0(X5,esk3_2(X4,X5)))|~(aElementOf0(X5,X4)))|X5=szmzizndt0(X4))|(~(aSubsetOf0(X4,szNzAzT0))|X4=slcrc0)))),inference(distribute,[status(thm)],[101])).
% cnf(106,plain,(X1=slcrc0|sdtlseqdt0(X2,X3)|~aSubsetOf0(X1,szNzAzT0)|X2!=szmzizndt0(X1)|~aElementOf0(X3,X1)),inference(split_conjunct,[status(thm)],[102])).
% fof(107, plain,(((((((aSet0(xS)&![X1]:(~(aElementOf0(X1,xS))|aElementOf0(X1,szNzAzT0)))&aSubsetOf0(xS,szNzAzT0))&aSet0(xT))&![X1]:(~(aElementOf0(X1,xT))|aElementOf0(X1,szNzAzT0)))&aSubsetOf0(xT,szNzAzT0))&(?[X1]:aElementOf0(X1,xS)&~(xS=slcrc0)))&(?[X1]:aElementOf0(X1,xT)&~(xT=slcrc0))),inference(fof_nnf,[status(thm)],[10])).
% fof(108, plain,(((((((aSet0(xS)&![X2]:(~(aElementOf0(X2,xS))|aElementOf0(X2,szNzAzT0)))&aSubsetOf0(xS,szNzAzT0))&aSet0(xT))&![X3]:(~(aElementOf0(X3,xT))|aElementOf0(X3,szNzAzT0)))&aSubsetOf0(xT,szNzAzT0))&(?[X4]:aElementOf0(X4,xS)&~(xS=slcrc0)))&(?[X5]:aElementOf0(X5,xT)&~(xT=slcrc0))),inference(variable_rename,[status(thm)],[107])).
% fof(109, plain,(((((((aSet0(xS)&![X2]:(~(aElementOf0(X2,xS))|aElementOf0(X2,szNzAzT0)))&aSubsetOf0(xS,szNzAzT0))&aSet0(xT))&![X3]:(~(aElementOf0(X3,xT))|aElementOf0(X3,szNzAzT0)))&aSubsetOf0(xT,szNzAzT0))&(aElementOf0(esk4_0,xS)&~(xS=slcrc0)))&(aElementOf0(esk5_0,xT)&~(xT=slcrc0))),inference(skolemize,[status(esa)],[108])).
% fof(110, plain,![X2]:![X3]:(((((~(aElementOf0(X3,xT))|aElementOf0(X3,szNzAzT0))&((((~(aElementOf0(X2,xS))|aElementOf0(X2,szNzAzT0))&aSet0(xS))&aSubsetOf0(xS,szNzAzT0))&aSet0(xT)))&aSubsetOf0(xT,szNzAzT0))&(aElementOf0(esk4_0,xS)&~(xS=slcrc0)))&(aElementOf0(esk5_0,xT)&~(xT=slcrc0))),inference(shift_quantors,[status(thm)],[109])).
% cnf(115,plain,(aSubsetOf0(xT,szNzAzT0)),inference(split_conjunct,[status(thm)],[110])).
% cnf(119,plain,(aElementOf0(X1,szNzAzT0)|~aElementOf0(X1,xS)),inference(split_conjunct,[status(thm)],[110])).
% cnf(120,plain,(aElementOf0(X1,szNzAzT0)|~aElementOf0(X1,xT)),inference(split_conjunct,[status(thm)],[110])).
% fof(121, plain,(((((aElementOf0(szmzizndt0(xS),xS)&![X1]:(~(aElementOf0(X1,xS))|sdtlseqdt0(szmzizndt0(xS),X1)))&aElementOf0(szmzizndt0(xS),xT))&aElementOf0(szmzizndt0(xT),xT))&![X1]:(~(aElementOf0(X1,xT))|sdtlseqdt0(szmzizndt0(xT),X1)))&aElementOf0(szmzizndt0(xT),xS)),inference(fof_nnf,[status(thm)],[11])).
% fof(122, plain,(((((aElementOf0(szmzizndt0(xS),xS)&![X2]:(~(aElementOf0(X2,xS))|sdtlseqdt0(szmzizndt0(xS),X2)))&aElementOf0(szmzizndt0(xS),xT))&aElementOf0(szmzizndt0(xT),xT))&![X3]:(~(aElementOf0(X3,xT))|sdtlseqdt0(szmzizndt0(xT),X3)))&aElementOf0(szmzizndt0(xT),xS)),inference(variable_rename,[status(thm)],[121])).
% fof(123, plain,![X2]:![X3]:(((~(aElementOf0(X3,xT))|sdtlseqdt0(szmzizndt0(xT),X3))&((((~(aElementOf0(X2,xS))|sdtlseqdt0(szmzizndt0(xS),X2))&aElementOf0(szmzizndt0(xS),xS))&aElementOf0(szmzizndt0(xS),xT))&aElementOf0(szmzizndt0(xT),xT)))&aElementOf0(szmzizndt0(xT),xS)),inference(shift_quantors,[status(thm)],[122])).
% cnf(124,plain,(aElementOf0(szmzizndt0(xT),xS)),inference(split_conjunct,[status(thm)],[123])).
% cnf(127,plain,(aElementOf0(szmzizndt0(xS),xS)),inference(split_conjunct,[status(thm)],[123])).
% cnf(128,plain,(sdtlseqdt0(szmzizndt0(xS),X1)|~aElementOf0(X1,xS)),inference(split_conjunct,[status(thm)],[123])).
% fof(288, negated_conjecture,((aElementOf0(szmzizndt0(xS),xS)&![X1]:(~(aElementOf0(X1,xS))|sdtlseqdt0(szmzizndt0(xS),X1)))&(?[X1]:(aElementOf0(X1,xT)&~(sdtlseqdt0(szmzizndt0(xS),X1)))&~(szmzizndt0(xS)=szmzizndt0(xT)))),inference(fof_nnf,[status(thm)],[52])).
% fof(289, negated_conjecture,((aElementOf0(szmzizndt0(xS),xS)&![X2]:(~(aElementOf0(X2,xS))|sdtlseqdt0(szmzizndt0(xS),X2)))&(?[X3]:(aElementOf0(X3,xT)&~(sdtlseqdt0(szmzizndt0(xS),X3)))&~(szmzizndt0(xS)=szmzizndt0(xT)))),inference(variable_rename,[status(thm)],[288])).
% fof(290, negated_conjecture,((aElementOf0(szmzizndt0(xS),xS)&![X2]:(~(aElementOf0(X2,xS))|sdtlseqdt0(szmzizndt0(xS),X2)))&((aElementOf0(esk11_0,xT)&~(sdtlseqdt0(szmzizndt0(xS),esk11_0)))&~(szmzizndt0(xS)=szmzizndt0(xT)))),inference(skolemize,[status(esa)],[289])).
% fof(291, negated_conjecture,![X2]:(((~(aElementOf0(X2,xS))|sdtlseqdt0(szmzizndt0(xS),X2))&aElementOf0(szmzizndt0(xS),xS))&((aElementOf0(esk11_0,xT)&~(sdtlseqdt0(szmzizndt0(xS),esk11_0)))&~(szmzizndt0(xS)=szmzizndt0(xT)))),inference(shift_quantors,[status(thm)],[290])).
% cnf(293,negated_conjecture,(~sdtlseqdt0(szmzizndt0(xS),esk11_0)),inference(split_conjunct,[status(thm)],[291])).
% cnf(294,negated_conjecture,(aElementOf0(esk11_0,xT)),inference(split_conjunct,[status(thm)],[291])).
% cnf(301,plain,(sdtlseqdt0(X2,X3)|szmzizndt0(X1)!=X2|~aSubsetOf0(X1,szNzAzT0)|~aElementOf0(X3,X1)),inference(csr,[status(thm)],[106,70])).
% cnf(319,plain,(aElementOf0(szmzizndt0(xT),szNzAzT0)),inference(spm,[status(thm)],[119,124,theory(equality)])).
% cnf(320,plain,(aElementOf0(szmzizndt0(xS),szNzAzT0)),inference(spm,[status(thm)],[119,127,theory(equality)])).
% cnf(321,negated_conjecture,(aElementOf0(esk11_0,szNzAzT0)),inference(spm,[status(thm)],[120,294,theory(equality)])).
% cnf(408,negated_conjecture,(sdtlseqdt0(X1,esk11_0)|szmzizndt0(xT)!=X1|~aSubsetOf0(xT,szNzAzT0)),inference(spm,[status(thm)],[301,294,theory(equality)])).
% cnf(420,negated_conjecture,(sdtlseqdt0(X1,esk11_0)|szmzizndt0(xT)!=X1|$false),inference(rw,[status(thm)],[408,115,theory(equality)])).
% cnf(421,negated_conjecture,(sdtlseqdt0(X1,esk11_0)|szmzizndt0(xT)!=X1),inference(cn,[status(thm)],[420,theory(equality)])).
% cnf(749,negated_conjecture,(sdtlseqdt0(szmzizndt0(xT),esk11_0)),inference(er,[status(thm)],[421,theory(equality)])).
% cnf(750,negated_conjecture,(sdtlseqdt0(X1,esk11_0)|~sdtlseqdt0(X1,szmzizndt0(xT))|~aElementOf0(szmzizndt0(xT),szNzAzT0)|~aElementOf0(esk11_0,szNzAzT0)|~aElementOf0(X1,szNzAzT0)),inference(spm,[status(thm)],[97,749,theory(equality)])).
% cnf(752,negated_conjecture,(sdtlseqdt0(X1,esk11_0)|~sdtlseqdt0(X1,szmzizndt0(xT))|$false|~aElementOf0(esk11_0,szNzAzT0)|~aElementOf0(X1,szNzAzT0)),inference(rw,[status(thm)],[750,319,theory(equality)])).
% cnf(753,negated_conjecture,(sdtlseqdt0(X1,esk11_0)|~sdtlseqdt0(X1,szmzizndt0(xT))|$false|$false|~aElementOf0(X1,szNzAzT0)),inference(rw,[status(thm)],[752,321,theory(equality)])).
% cnf(754,negated_conjecture,(sdtlseqdt0(X1,esk11_0)|~sdtlseqdt0(X1,szmzizndt0(xT))|~aElementOf0(X1,szNzAzT0)),inference(cn,[status(thm)],[753,theory(equality)])).
% cnf(836,negated_conjecture,(sdtlseqdt0(szmzizndt0(xS),esk11_0)|~aElementOf0(szmzizndt0(xS),szNzAzT0)|~aElementOf0(szmzizndt0(xT),xS)),inference(spm,[status(thm)],[754,128,theory(equality)])).
% cnf(849,negated_conjecture,(sdtlseqdt0(szmzizndt0(xS),esk11_0)|$false|~aElementOf0(szmzizndt0(xT),xS)),inference(rw,[status(thm)],[836,320,theory(equality)])).
% cnf(850,negated_conjecture,(sdtlseqdt0(szmzizndt0(xS),esk11_0)|$false|$false),inference(rw,[status(thm)],[849,124,theory(equality)])).
% cnf(851,negated_conjecture,(sdtlseqdt0(szmzizndt0(xS),esk11_0)),inference(cn,[status(thm)],[850,theory(equality)])).
% cnf(852,negated_conjecture,($false),inference(sr,[status(thm)],[851,293,theory(equality)])).
% cnf(853,negated_conjecture,($false),852,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 286
% # ...of these trivial : 14
% # ...subsumed : 36
% # ...remaining for further processing: 236
% # Other redundant clauses eliminated : 12
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 0
% # Backward-rewritten : 0
% # Generated clauses : 347
% # ...of the previous two non-trivial : 299
% # Contextual simplify-reflections : 19
% # Paramodulations : 319
% # Factorizations : 0
% # Equation resolutions : 28
% # Current number of processed clauses: 139
% # Positive orientable unit clauses: 33
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 9
% # Non-unit-clauses : 97
% # Current number of unprocessed clauses: 205
% # ...number of literals in the above : 1047
% # Clause-clause subsumption calls (NU) : 363
% # Rec. Clause-clause subsumption calls : 219
% # Unit Clause-clause subsumption calls : 59
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 0
% # Indexed BW rewrite successes : 0
% # Backwards rewriting index: 126 leaves, 1.29+/-0.862 terms/leaf
% # Paramod-from index: 73 leaves, 1.00+/-0.000 terms/leaf
% # Paramod-into index: 115 leaves, 1.14+/-0.558 terms/leaf
% # -------------------------------------------------
% # User time : 0.045 s
% # System time : 0.002 s
% # Total time : 0.047 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.15 CPU 0.23 WC
% FINAL PrfWatch: 0.15 CPU 0.23 WC
% SZS output end Solution for /tmp/SystemOnTPTP18738/NUM539+2.tptp
%
%------------------------------------------------------------------------------