%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : SWB057+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 : 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 : Fri Mar 4 03:35:42 EST 2011
% Result : Theorem 32.71s
% Output : Solution 32.71s
% 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/SystemOnTPTP11956/SWB057+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% WARNING: TreeLimitedRun lost 0.62s, total lost is 0.62s
% found
% SZS status THM for /tmp/SystemOnTPTP11956/SWB057+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP11956/SWB057+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 12080
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.00 WC
% PrfWatch: 1.92 CPU 2.01 WC
% PrfWatch: 3.92 CPU 4.01 WC
% PrfWatch: 5.90 CPU 6.02 WC
% PrfWatch: 7.90 CPU 8.02 WC
% PrfWatch: 9.89 CPU 10.03 WC
% # Preprocessing time : 0.142 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% PrfWatch: 11.88 CPU 12.03 WC
% PrfWatch: 13.87 CPU 14.04 WC
% PrfWatch: 15.86 CPU 16.04 WC
% # SZS output start CNFRefutation.
% fof(2, axiom,![X1]:![X2]:(iext(uri_owl_differentFrom,X1,X2)<=>~(X1=X2)),file('/tmp/SRASS.s.p', owl_eqdis_differentfrom)).
% fof(6, axiom,?[X3]:((iext(uri_rdf_type,uri_ex_u,X3)&iext(uri_owl_complementOf,X3,uri_ex_c))&iext(uri_rdf_type,uri_ex_w,uri_ex_c)),file('/tmp/SRASS.s.p', premise_rdfbased_sem_eqdis_different_ext)).
% fof(8, axiom,![X1]:![X7]:(iext(uri_rdf_type,X1,X7)<=>icext(X7,X1)),file('/tmp/SRASS.s.p', rdfs_cext_def)).
% fof(40, axiom,![X12]:![X7]:(iext(uri_owl_complementOf,X12,X7)=>((ic(X12)&ic(X7))&![X1]:(icext(X12,X1)<=>~(icext(X7,X1))))),file('/tmp/SRASS.s.p', owl_bool_complementof_class)).
% fof(560, conjecture,iext(uri_owl_differentFrom,uri_ex_w,uri_ex_u),file('/tmp/SRASS.s.p', conclusion_rdfbased_sem_eqdis_different_ext)).
% fof(561, negated_conjecture,~(iext(uri_owl_differentFrom,uri_ex_w,uri_ex_u)),inference(assume_negation,[status(cth)],[560])).
% fof(564, plain,![X12]:![X7]:(iext(uri_owl_complementOf,X12,X7)=>((ic(X12)&ic(X7))&![X1]:(icext(X12,X1)<=>~(icext(X7,X1))))),inference(fof_simplification,[status(thm)],[40,theory(equality)])).
% fof(584, negated_conjecture,~(iext(uri_owl_differentFrom,uri_ex_w,uri_ex_u)),inference(fof_simplification,[status(thm)],[561,theory(equality)])).
% fof(594, plain,![X1]:![X2]:((~(iext(uri_owl_differentFrom,X1,X2))|~(X1=X2))&(X1=X2|iext(uri_owl_differentFrom,X1,X2))),inference(fof_nnf,[status(thm)],[2])).
% fof(595, plain,![X3]:![X4]:((~(iext(uri_owl_differentFrom,X3,X4))|~(X3=X4))&(X3=X4|iext(uri_owl_differentFrom,X3,X4))),inference(variable_rename,[status(thm)],[594])).
% cnf(596,plain,(iext(uri_owl_differentFrom,X1,X2)|X1=X2),inference(split_conjunct,[status(thm)],[595])).
% fof(604, plain,?[X4]:((iext(uri_rdf_type,uri_ex_u,X4)&iext(uri_owl_complementOf,X4,uri_ex_c))&iext(uri_rdf_type,uri_ex_w,uri_ex_c)),inference(variable_rename,[status(thm)],[6])).
% fof(605, plain,((iext(uri_rdf_type,uri_ex_u,esk2_0)&iext(uri_owl_complementOf,esk2_0,uri_ex_c))&iext(uri_rdf_type,uri_ex_w,uri_ex_c)),inference(skolemize,[status(esa)],[604])).
% cnf(606,plain,(iext(uri_rdf_type,uri_ex_w,uri_ex_c)),inference(split_conjunct,[status(thm)],[605])).
% cnf(607,plain,(iext(uri_owl_complementOf,esk2_0,uri_ex_c)),inference(split_conjunct,[status(thm)],[605])).
% cnf(608,plain,(iext(uri_rdf_type,uri_ex_u,esk2_0)),inference(split_conjunct,[status(thm)],[605])).
% fof(612, plain,![X1]:![X7]:((~(iext(uri_rdf_type,X1,X7))|icext(X7,X1))&(~(icext(X7,X1))|iext(uri_rdf_type,X1,X7))),inference(fof_nnf,[status(thm)],[8])).
% fof(613, plain,![X8]:![X9]:((~(iext(uri_rdf_type,X8,X9))|icext(X9,X8))&(~(icext(X9,X8))|iext(uri_rdf_type,X8,X9))),inference(variable_rename,[status(thm)],[612])).
% cnf(615,plain,(icext(X1,X2)|~iext(uri_rdf_type,X2,X1)),inference(split_conjunct,[status(thm)],[613])).
% fof(736, plain,![X12]:![X7]:(~(iext(uri_owl_complementOf,X12,X7))|((ic(X12)&ic(X7))&![X1]:((~(icext(X12,X1))|~(icext(X7,X1)))&(icext(X7,X1)|icext(X12,X1))))),inference(fof_nnf,[status(thm)],[564])).
% fof(737, plain,![X13]:![X14]:(~(iext(uri_owl_complementOf,X13,X14))|((ic(X13)&ic(X14))&![X15]:((~(icext(X13,X15))|~(icext(X14,X15)))&(icext(X14,X15)|icext(X13,X15))))),inference(variable_rename,[status(thm)],[736])).
% fof(738, plain,![X13]:![X14]:![X15]:((((~(icext(X13,X15))|~(icext(X14,X15)))&(icext(X14,X15)|icext(X13,X15)))&(ic(X13)&ic(X14)))|~(iext(uri_owl_complementOf,X13,X14))),inference(shift_quantors,[status(thm)],[737])).
% fof(739, plain,![X13]:![X14]:![X15]:((((~(icext(X13,X15))|~(icext(X14,X15)))|~(iext(uri_owl_complementOf,X13,X14)))&((icext(X14,X15)|icext(X13,X15))|~(iext(uri_owl_complementOf,X13,X14))))&((ic(X13)|~(iext(uri_owl_complementOf,X13,X14)))&(ic(X14)|~(iext(uri_owl_complementOf,X13,X14))))),inference(distribute,[status(thm)],[738])).
% cnf(743,plain,(~iext(uri_owl_complementOf,X1,X2)|~icext(X2,X3)|~icext(X1,X3)),inference(split_conjunct,[status(thm)],[739])).
% cnf(2833,negated_conjecture,(~iext(uri_owl_differentFrom,uri_ex_w,uri_ex_u)),inference(split_conjunct,[status(thm)],[584])).
% cnf(3112,negated_conjecture,(uri_ex_w=uri_ex_u),inference(spm,[status(thm)],[2833,596,theory(equality)])).
% cnf(3854,plain,(icext(esk2_0,uri_ex_u)),inference(spm,[status(thm)],[615,608,theory(equality)])).
% cnf(5227,plain,(~icext(uri_ex_c,X1)|~icext(esk2_0,X1)),inference(spm,[status(thm)],[743,607,theory(equality)])).
% cnf(47648,plain,(iext(uri_rdf_type,uri_ex_u,uri_ex_c)),inference(rw,[status(thm)],[606,3112,theory(equality)])).
% cnf(47910,plain,(icext(uri_ex_c,uri_ex_u)),inference(spm,[status(thm)],[615,47648,theory(equality)])).
% cnf(225755,plain,(~icext(esk2_0,uri_ex_u)),inference(spm,[status(thm)],[5227,47910,theory(equality)])).
% cnf(225791,plain,($false),inference(rw,[status(thm)],[225755,3854,theory(equality)])).
% cnf(225792,plain,($false),inference(cn,[status(thm)],[225791,theory(equality)])).
% cnf(225793,plain,($false),225792,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 12474
% # ...of these trivial : 361
% # ...subsumed : 5018
% # ...remaining for further processing: 7095
% # Other redundant clauses eliminated : 16
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 62
% # Backward-rewritten : 3
% # Generated clauses : 200607
% # ...of the previous two non-trivial : 192617
% # Contextual simplify-reflections : 112
% # Paramodulations : 200579
% # Factorizations : 12
% # Equation resolutions : 16
% # Current number of processed clauses: 5920
% # Positive orientable unit clauses: 2060
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 25
% # Non-unit-clauses : 3835
% # Current number of unprocessed clauses: 181283
% # ...number of literals in the above : 1525171
% # Clause-clause subsumption calls (NU) : 1546815
% # Rec. Clause-clause subsumption calls : 572232
% # Unit Clause-clause subsumption calls : 114718
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 19033
% # Indexed BW rewrite successes : 2
% # Backwards rewriting index: 3152 leaves, 1.57+/-4.885 terms/leaf
% # Paramod-from index: 1809 leaves, 1.49+/-4.781 terms/leaf
% # Paramod-into index: 2744 leaves, 1.46+/-4.080 terms/leaf
% # -------------------------------------------------
% # User time : 11.017 s
% # System time : 0.311 s
% # Total time : 11.328 s
% # Maximum resident set size: 0 pages
% PrfWatch: 16.11 CPU 16.29 WC
% FINAL PrfWatch: 16.11 CPU 16.29 WC
% SZS output end Solution for /tmp/SystemOnTPTP11956/SWB057+1.tptp
%
%------------------------------------------------------------------------------