%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : NUM592+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 : art11.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 3.00GHz @ 3000MHz
% Memory : 2006MB
% OS : Linux 2.6.31.5-127.fc12.i686.PAE
% CPULimit : 300s
% DateTime : Wed Dec 29 20:31:30 EST 2010
% Result : Theorem 1.50s
% Output : Solution 1.50s
% 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/SystemOnTPTP4063/NUM592+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP4063/NUM592+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP4063/NUM592+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 4195
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.01 WC
% # Preprocessing time : 0.030 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(48, axiom,(xY=sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))&xd=sdtlpdtrp0(xC,xi)),file('/tmp/SRASS.s.p', m__4448_02)).
% fof(50, axiom,(((aElementOf0(xu,xT)&aSubsetOf0(xX,xY))&isCountable0(xX))&![X1]:((aSet0(X1)&aElementOf0(X1,slbdtsldtrb0(xX,xk)))=>sdtlpdtrp0(xd,X1)=xu)),file('/tmp/SRASS.s.p', m__4545)).
% fof(94, conjecture,?[X1]:(aElementOf0(X1,xT)&?[X2]:((aSubsetOf0(X2,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))&isCountable0(X2))&![X3]:((aSet0(X3)&aElementOf0(X3,slbdtsldtrb0(X2,xk)))=>sdtlpdtrp0(sdtlpdtrp0(xC,xi),X3)=X1))),file('/tmp/SRASS.s.p', m__)).
% fof(95, negated_conjecture,~(?[X1]:(aElementOf0(X1,xT)&?[X2]:((aSubsetOf0(X2,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))&isCountable0(X2))&![X3]:((aSet0(X3)&aElementOf0(X3,slbdtsldtrb0(X2,xk)))=>sdtlpdtrp0(sdtlpdtrp0(xC,xi),X3)=X1)))),inference(assume_negation,[status(cth)],[94])).
% cnf(293,plain,(xd=sdtlpdtrp0(xC,xi)),inference(split_conjunct,[status(thm)],[48])).
% cnf(294,plain,(xY=sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))),inference(split_conjunct,[status(thm)],[48])).
% fof(300, plain,(((aElementOf0(xu,xT)&aSubsetOf0(xX,xY))&isCountable0(xX))&![X1]:((~(aSet0(X1))|~(aElementOf0(X1,slbdtsldtrb0(xX,xk))))|sdtlpdtrp0(xd,X1)=xu)),inference(fof_nnf,[status(thm)],[50])).
% fof(301, plain,(((aElementOf0(xu,xT)&aSubsetOf0(xX,xY))&isCountable0(xX))&![X2]:((~(aSet0(X2))|~(aElementOf0(X2,slbdtsldtrb0(xX,xk))))|sdtlpdtrp0(xd,X2)=xu)),inference(variable_rename,[status(thm)],[300])).
% fof(302, plain,![X2]:(((~(aSet0(X2))|~(aElementOf0(X2,slbdtsldtrb0(xX,xk))))|sdtlpdtrp0(xd,X2)=xu)&((aElementOf0(xu,xT)&aSubsetOf0(xX,xY))&isCountable0(xX))),inference(shift_quantors,[status(thm)],[301])).
% cnf(303,plain,(isCountable0(xX)),inference(split_conjunct,[status(thm)],[302])).
% cnf(304,plain,(aSubsetOf0(xX,xY)),inference(split_conjunct,[status(thm)],[302])).
% cnf(305,plain,(aElementOf0(xu,xT)),inference(split_conjunct,[status(thm)],[302])).
% cnf(306,plain,(sdtlpdtrp0(xd,X1)=xu|~aElementOf0(X1,slbdtsldtrb0(xX,xk))|~aSet0(X1)),inference(split_conjunct,[status(thm)],[302])).
% fof(526, negated_conjecture,![X1]:(~(aElementOf0(X1,xT))|![X2]:((~(aSubsetOf0(X2,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))|~(isCountable0(X2)))|?[X3]:((aSet0(X3)&aElementOf0(X3,slbdtsldtrb0(X2,xk)))&~(sdtlpdtrp0(sdtlpdtrp0(xC,xi),X3)=X1)))),inference(fof_nnf,[status(thm)],[95])).
% fof(527, negated_conjecture,![X4]:(~(aElementOf0(X4,xT))|![X5]:((~(aSubsetOf0(X5,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))|~(isCountable0(X5)))|?[X6]:((aSet0(X6)&aElementOf0(X6,slbdtsldtrb0(X5,xk)))&~(sdtlpdtrp0(sdtlpdtrp0(xC,xi),X6)=X4)))),inference(variable_rename,[status(thm)],[526])).
% fof(528, negated_conjecture,![X4]:(~(aElementOf0(X4,xT))|![X5]:((~(aSubsetOf0(X5,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))|~(isCountable0(X5)))|((aSet0(esk22_2(X4,X5))&aElementOf0(esk22_2(X4,X5),slbdtsldtrb0(X5,xk)))&~(sdtlpdtrp0(sdtlpdtrp0(xC,xi),esk22_2(X4,X5))=X4)))),inference(skolemize,[status(esa)],[527])).
% fof(529, negated_conjecture,![X4]:![X5]:(((~(aSubsetOf0(X5,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))|~(isCountable0(X5)))|((aSet0(esk22_2(X4,X5))&aElementOf0(esk22_2(X4,X5),slbdtsldtrb0(X5,xk)))&~(sdtlpdtrp0(sdtlpdtrp0(xC,xi),esk22_2(X4,X5))=X4)))|~(aElementOf0(X4,xT))),inference(shift_quantors,[status(thm)],[528])).
% fof(530, negated_conjecture,![X4]:![X5]:((((aSet0(esk22_2(X4,X5))|(~(aSubsetOf0(X5,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))|~(isCountable0(X5))))|~(aElementOf0(X4,xT)))&((aElementOf0(esk22_2(X4,X5),slbdtsldtrb0(X5,xk))|(~(aSubsetOf0(X5,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))|~(isCountable0(X5))))|~(aElementOf0(X4,xT))))&((~(sdtlpdtrp0(sdtlpdtrp0(xC,xi),esk22_2(X4,X5))=X4)|(~(aSubsetOf0(X5,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))|~(isCountable0(X5))))|~(aElementOf0(X4,xT)))),inference(distribute,[status(thm)],[529])).
% cnf(531,negated_conjecture,(~aElementOf0(X1,xT)|~isCountable0(X2)|~aSubsetOf0(X2,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))|sdtlpdtrp0(sdtlpdtrp0(xC,xi),esk22_2(X1,X2))!=X1),inference(split_conjunct,[status(thm)],[530])).
% cnf(532,negated_conjecture,(aElementOf0(esk22_2(X1,X2),slbdtsldtrb0(X2,xk))|~aElementOf0(X1,xT)|~isCountable0(X2)|~aSubsetOf0(X2,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))),inference(split_conjunct,[status(thm)],[530])).
% cnf(533,negated_conjecture,(aSet0(esk22_2(X1,X2))|~aElementOf0(X1,xT)|~isCountable0(X2)|~aSubsetOf0(X2,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))),inference(split_conjunct,[status(thm)],[530])).
% cnf(540,negated_conjecture,(aSet0(esk22_2(X1,X2))|~isCountable0(X2)|~aElementOf0(X1,xT)|~aSubsetOf0(X2,xY)),inference(rw,[status(thm)],[533,294,theory(equality)])).
% cnf(544,negated_conjecture,(aElementOf0(esk22_2(X1,X2),slbdtsldtrb0(X2,xk))|~isCountable0(X2)|~aElementOf0(X1,xT)|~aSubsetOf0(X2,xY)),inference(rw,[status(thm)],[532,294,theory(equality)])).
% cnf(549,negated_conjecture,(sdtlpdtrp0(xd,esk22_2(X1,X2))!=X1|~isCountable0(X2)|~aElementOf0(X1,xT)|~aSubsetOf0(X2,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))),inference(rw,[status(thm)],[531,293,theory(equality)])).
% cnf(550,negated_conjecture,(sdtlpdtrp0(xd,esk22_2(X1,X2))!=X1|~isCountable0(X2)|~aElementOf0(X1,xT)|~aSubsetOf0(X2,xY)),inference(rw,[status(thm)],[549,294,theory(equality)])).
% cnf(823,negated_conjecture,(sdtlpdtrp0(xd,esk22_2(X1,xX))=xu|~aSet0(esk22_2(X1,xX))|~aElementOf0(X1,xT)|~aSubsetOf0(xX,xY)|~isCountable0(xX)),inference(spm,[status(thm)],[306,544,theory(equality)])).
% cnf(825,negated_conjecture,(sdtlpdtrp0(xd,esk22_2(X1,xX))=xu|~aSet0(esk22_2(X1,xX))|~aElementOf0(X1,xT)|$false|~isCountable0(xX)),inference(rw,[status(thm)],[823,304,theory(equality)])).
% cnf(826,negated_conjecture,(sdtlpdtrp0(xd,esk22_2(X1,xX))=xu|~aSet0(esk22_2(X1,xX))|~aElementOf0(X1,xT)|$false|$false),inference(rw,[status(thm)],[825,303,theory(equality)])).
% cnf(827,negated_conjecture,(sdtlpdtrp0(xd,esk22_2(X1,xX))=xu|~aSet0(esk22_2(X1,xX))|~aElementOf0(X1,xT)),inference(cn,[status(thm)],[826,theory(equality)])).
% cnf(3405,negated_conjecture,(xu!=X1|~aElementOf0(X1,xT)|~aSubsetOf0(xX,xY)|~isCountable0(xX)|~aSet0(esk22_2(X1,xX))),inference(spm,[status(thm)],[550,827,theory(equality)])).
% cnf(3413,negated_conjecture,(xu!=X1|~aElementOf0(X1,xT)|$false|~isCountable0(xX)|~aSet0(esk22_2(X1,xX))),inference(rw,[status(thm)],[3405,304,theory(equality)])).
% cnf(3414,negated_conjecture,(xu!=X1|~aElementOf0(X1,xT)|$false|$false|~aSet0(esk22_2(X1,xX))),inference(rw,[status(thm)],[3413,303,theory(equality)])).
% cnf(3415,negated_conjecture,(xu!=X1|~aElementOf0(X1,xT)|~aSet0(esk22_2(X1,xX))),inference(cn,[status(thm)],[3414,theory(equality)])).
% cnf(3447,negated_conjecture,(xu!=X1|~aElementOf0(X1,xT)|~aSubsetOf0(xX,xY)|~isCountable0(xX)),inference(spm,[status(thm)],[3415,540,theory(equality)])).
% cnf(3448,negated_conjecture,(xu!=X1|~aElementOf0(X1,xT)|$false|~isCountable0(xX)),inference(rw,[status(thm)],[3447,304,theory(equality)])).
% cnf(3449,negated_conjecture,(xu!=X1|~aElementOf0(X1,xT)|$false|$false),inference(rw,[status(thm)],[3448,303,theory(equality)])).
% cnf(3450,negated_conjecture,(xu!=X1|~aElementOf0(X1,xT)),inference(cn,[status(thm)],[3449,theory(equality)])).
% cnf(3458,negated_conjecture,($false),inference(spm,[status(thm)],[3450,305,theory(equality)])).
% cnf(3471,negated_conjecture,($false),3458,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 767
% # ...of these trivial : 7
% # ...subsumed : 163
% # ...remaining for further processing: 597
% # Other redundant clauses eliminated : 13
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 4
% # Backward-rewritten : 3
% # Generated clauses : 1585
% # ...of the previous two non-trivial : 1444
% # Contextual simplify-reflections : 100
% # Paramodulations : 1533
% # Factorizations : 0
% # Equation resolutions : 49
% # Current number of processed clauses: 401
% # Positive orientable unit clauses: 77
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 23
% # Non-unit-clauses : 301
% # Current number of unprocessed clauses: 1035
% # ...number of literals in the above : 5594
% # Clause-clause subsumption calls (NU) : 4395
% # Rec. Clause-clause subsumption calls : 2014
% # Unit Clause-clause subsumption calls : 1187
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 2
% # Indexed BW rewrite successes : 2
% # Backwards rewriting index: 425 leaves, 1.23+/-0.793 terms/leaf
% # Paramod-from index: 209 leaves, 1.01+/-0.097 terms/leaf
% # Paramod-into index: 368 leaves, 1.13+/-0.507 terms/leaf
% # -------------------------------------------------
% # User time : 0.142 s
% # System time : 0.008 s
% # Total time : 0.150 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.29 CPU 0.36 WC
% FINAL PrfWatch: 0.29 CPU 0.36 WC
% SZS output end Solution for /tmp/SystemOnTPTP4063/NUM592+1.tptp
%
%------------------------------------------------------------------------------