%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : SWB053+1 : TPTP v5.2.0. Released v5.2.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 : Fri Mar 4 03:34:39 EST 2011
% Result : Theorem 25.21s
% Output : Solution 25.21s
% 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/SystemOnTPTP4900/SWB053+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% WARNING: TreeLimitedRun lost 0.72s, total lost is 0.72s
% found
% SZS status THM for /tmp/SystemOnTPTP4900/SWB053+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP4900/SWB053+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 5015
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.00 WC
% PrfWatch: 1.34 CPU 2.01 WC
% PrfWatch: 3.33 CPU 4.01 WC
% PrfWatch: 5.32 CPU 6.02 WC
% # Preprocessing time : 0.144 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% PrfWatch: 7.30 CPU 8.02 WC
% # SZS output start CNFRefutation.
% fof(2, axiom,![X4]:~(icext(uri_owl_Nothing,X4)),file('/tmp/SRASS.s.p', owl_class_nothing_ext)).
% fof(4, axiom,ic(uri_owl_Nothing),file('/tmp/SRASS.s.p', owl_class_nothing_type)).
% fof(6, axiom,![X5]:![X6]:(iext(uri_rdfs_subClassOf,X5,X6)<=>((ic(X5)&ic(X6))&![X4]:(icext(X5,X4)=>icext(X6,X4)))),file('/tmp/SRASS.s.p', owl_rdfsext_subclassof)).
% fof(8, axiom,iext(uri_rdf_type,uri_ex_c,uri_owl_Class),file('/tmp/SRASS.s.p', premise_rdfbased_sem_class_nothing_term)).
% fof(34, axiom,![X4]:(icext(uri_owl_Class,X4)<=>ic(X4)),file('/tmp/SRASS.s.p', owl_class_classowl_ext)).
% fof(41, axiom,![X4]:![X1]:(iext(uri_rdf_type,X4,X1)<=>icext(X1,X4)),file('/tmp/SRASS.s.p', rdfs_cext_def)).
% fof(560, conjecture,iext(uri_rdfs_subClassOf,uri_owl_Nothing,uri_ex_c),file('/tmp/SRASS.s.p', conclusion_rdfbased_sem_class_nothing_term)).
% fof(561, negated_conjecture,~(iext(uri_rdfs_subClassOf,uri_owl_Nothing,uri_ex_c)),inference(assume_negation,[status(cth)],[560])).
% fof(562, plain,![X4]:~(icext(uri_owl_Nothing,X4)),inference(fof_simplification,[status(thm)],[2,theory(equality)])).
% fof(584, negated_conjecture,~(iext(uri_rdfs_subClassOf,uri_owl_Nothing,uri_ex_c)),inference(fof_simplification,[status(thm)],[561,theory(equality)])).
% fof(592, plain,![X5]:~(icext(uri_owl_Nothing,X5)),inference(variable_rename,[status(thm)],[562])).
% cnf(593,plain,(~icext(uri_owl_Nothing,X1)),inference(split_conjunct,[status(thm)],[592])).
% cnf(597,plain,(ic(uri_owl_Nothing)),inference(split_conjunct,[status(thm)],[4])).
% fof(605, plain,![X5]:![X6]:((~(iext(uri_rdfs_subClassOf,X5,X6))|((ic(X5)&ic(X6))&![X4]:(~(icext(X5,X4))|icext(X6,X4))))&(((~(ic(X5))|~(ic(X6)))|?[X4]:(icext(X5,X4)&~(icext(X6,X4))))|iext(uri_rdfs_subClassOf,X5,X6))),inference(fof_nnf,[status(thm)],[6])).
% fof(606, plain,![X7]:![X8]:((~(iext(uri_rdfs_subClassOf,X7,X8))|((ic(X7)&ic(X8))&![X9]:(~(icext(X7,X9))|icext(X8,X9))))&(((~(ic(X7))|~(ic(X8)))|?[X10]:(icext(X7,X10)&~(icext(X8,X10))))|iext(uri_rdfs_subClassOf,X7,X8))),inference(variable_rename,[status(thm)],[605])).
% fof(607, plain,![X7]:![X8]:((~(iext(uri_rdfs_subClassOf,X7,X8))|((ic(X7)&ic(X8))&![X9]:(~(icext(X7,X9))|icext(X8,X9))))&(((~(ic(X7))|~(ic(X8)))|(icext(X7,esk1_2(X7,X8))&~(icext(X8,esk1_2(X7,X8)))))|iext(uri_rdfs_subClassOf,X7,X8))),inference(skolemize,[status(esa)],[606])).
% fof(608, plain,![X7]:![X8]:![X9]:((((~(icext(X7,X9))|icext(X8,X9))&(ic(X7)&ic(X8)))|~(iext(uri_rdfs_subClassOf,X7,X8)))&(((~(ic(X7))|~(ic(X8)))|(icext(X7,esk1_2(X7,X8))&~(icext(X8,esk1_2(X7,X8)))))|iext(uri_rdfs_subClassOf,X7,X8))),inference(shift_quantors,[status(thm)],[607])).
% fof(609, plain,![X7]:![X8]:![X9]:((((~(icext(X7,X9))|icext(X8,X9))|~(iext(uri_rdfs_subClassOf,X7,X8)))&((ic(X7)|~(iext(uri_rdfs_subClassOf,X7,X8)))&(ic(X8)|~(iext(uri_rdfs_subClassOf,X7,X8)))))&(((icext(X7,esk1_2(X7,X8))|(~(ic(X7))|~(ic(X8))))|iext(uri_rdfs_subClassOf,X7,X8))&((~(icext(X8,esk1_2(X7,X8)))|(~(ic(X7))|~(ic(X8))))|iext(uri_rdfs_subClassOf,X7,X8)))),inference(distribute,[status(thm)],[608])).
% cnf(611,plain,(iext(uri_rdfs_subClassOf,X1,X2)|icext(X1,esk1_2(X1,X2))|~ic(X2)|~ic(X1)),inference(split_conjunct,[status(thm)],[609])).
% cnf(618,plain,(iext(uri_rdf_type,uri_ex_c,uri_owl_Class)),inference(split_conjunct,[status(thm)],[8])).
% fof(687, plain,![X4]:((~(icext(uri_owl_Class,X4))|ic(X4))&(~(ic(X4))|icext(uri_owl_Class,X4))),inference(fof_nnf,[status(thm)],[34])).
% fof(688, plain,![X5]:((~(icext(uri_owl_Class,X5))|ic(X5))&(~(ic(X5))|icext(uri_owl_Class,X5))),inference(variable_rename,[status(thm)],[687])).
% cnf(690,plain,(ic(X1)|~icext(uri_owl_Class,X1)),inference(split_conjunct,[status(thm)],[688])).
% fof(716, plain,![X4]:![X1]:((~(iext(uri_rdf_type,X4,X1))|icext(X1,X4))&(~(icext(X1,X4))|iext(uri_rdf_type,X4,X1))),inference(fof_nnf,[status(thm)],[41])).
% fof(717, plain,![X5]:![X6]:((~(iext(uri_rdf_type,X5,X6))|icext(X6,X5))&(~(icext(X6,X5))|iext(uri_rdf_type,X5,X6))),inference(variable_rename,[status(thm)],[716])).
% cnf(719,plain,(icext(X1,X2)|~iext(uri_rdf_type,X2,X1)),inference(split_conjunct,[status(thm)],[717])).
% cnf(2829,negated_conjecture,(~iext(uri_rdfs_subClassOf,uri_owl_Nothing,uri_ex_c)),inference(split_conjunct,[status(thm)],[584])).
% cnf(3871,plain,(icext(uri_owl_Class,uri_ex_c)),inference(spm,[status(thm)],[719,618,theory(equality)])).
% cnf(8166,plain,(iext(uri_rdfs_subClassOf,uri_owl_Nothing,X1)|~ic(X1)|~ic(uri_owl_Nothing)),inference(spm,[status(thm)],[593,611,theory(equality)])).
% cnf(8168,plain,(iext(uri_rdfs_subClassOf,uri_owl_Nothing,X1)|~ic(X1)|$false),inference(rw,[status(thm)],[8166,597,theory(equality)])).
% cnf(8169,plain,(iext(uri_rdfs_subClassOf,uri_owl_Nothing,X1)|~ic(X1)),inference(cn,[status(thm)],[8168,theory(equality)])).
% cnf(48858,plain,(iext(uri_rdfs_subClassOf,uri_owl_Nothing,X1)|~icext(uri_owl_Class,X1)),inference(spm,[status(thm)],[8169,690,theory(equality)])).
% cnf(111598,negated_conjecture,(~icext(uri_owl_Class,uri_ex_c)),inference(spm,[status(thm)],[2829,48858,theory(equality)])).
% cnf(111690,negated_conjecture,($false),inference(rw,[status(thm)],[111598,3871,theory(equality)])).
% cnf(111691,negated_conjecture,($false),inference(cn,[status(thm)],[111690,theory(equality)])).
% cnf(111692,negated_conjecture,($false),111691,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 4367
% # ...of these trivial : 134
% # ...subsumed : 745
% # ...remaining for further processing: 3488
% # Other redundant clauses eliminated : 16
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 6
% # Backward-rewritten : 0
% # Generated clauses : 97072
% # ...of the previous two non-trivial : 93944
% # Contextual simplify-reflections : 88
% # Paramodulations : 97044
% # Factorizations : 12
% # Equation resolutions : 16
% # Current number of processed clauses: 2374
% # Positive orientable unit clauses: 1301
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 21
% # Non-unit-clauses : 1052
% # Current number of unprocessed clauses: 91826
% # ...number of literals in the above : 819871
% # Clause-clause subsumption calls (NU) : 1248952
% # Rec. Clause-clause subsumption calls : 61141
% # Unit Clause-clause subsumption calls : 17562
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 5340
% # Indexed BW rewrite successes : 0
% # Backwards rewriting index: 1794 leaves, 1.65+/-5.133 terms/leaf
% # Paramod-from index: 1178 leaves, 1.32+/-3.577 terms/leaf
% # Paramod-into index: 1626 leaves, 1.40+/-3.371 terms/leaf
% # -------------------------------------------------
% # User time : 5.567 s
% # System time : 0.166 s
% # Total time : 5.733 s
% # Maximum resident set size: 0 pages
% PrfWatch: 8.52 CPU 9.27 WC
% FINAL PrfWatch: 8.52 CPU 9.27 WC
% SZS output end Solution for /tmp/SystemOnTPTP4900/SWB053+1.tptp
%
%------------------------------------------------------------------------------