%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : SWB009+3 : 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 Feb 25 03:16:26 EST 2011
% Result : Theorem 6.44s
% Output : Solution 6.44s
% 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/SystemOnTPTP16865/SWB009+3.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP16865/SWB009+3.tptp
% SZS output start Solution for /tmp/SystemOnTPTP16865/SWB009+3.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 16953
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.01 WC
% PrfWatch: 1.93 CPU 2.01 WC
% PrfWatch: 3.92 CPU 4.02 WC
% # Preprocessing time : 0.034 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(1, axiom,![X1]:![X2]:(iext(uri_rdf_type,X1,X2)<=>icext(X2,X1)),file('/tmp/SRASS.s.p', rdfs_cext_def)).
% fof(7, axiom,?[X6]:(((((iext(uri_rdf_type,uri_ex_p,uri_owl_ObjectProperty)&iext(uri_rdf_type,uri_ex_c,uri_owl_Class))&iext(uri_rdf_type,uri_ex_s,X6))&iext(uri_rdf_type,X6,uri_owl_Restriction))&iext(uri_owl_onProperty,X6,uri_ex_p))&iext(uri_owl_someValuesFrom,X6,uri_ex_c)),file('/tmp/SRASS.s.p', testcase_premise_fullish_009_Existential_Restriction_Entailments)).
% fof(8, axiom,![X7]:![X4]:![X2]:((iext(uri_owl_someValuesFrom,X7,X2)&iext(uri_owl_onProperty,X7,X4))=>![X1]:(icext(X7,X1)<=>?[X8]:(iext(X4,X1,X8)&icext(X2,X8)))),file('/tmp/SRASS.s.p', owl_restrict_somevaluesfrom)).
% fof(140, conjecture,?[X22]:(iext(uri_ex_p,uri_ex_s,X22)&iext(uri_rdf_type,X22,uri_ex_c)),file('/tmp/SRASS.s.p', testcase_conclusion_fullish_009_Existential_Restriction_Entailments)).
% fof(141, negated_conjecture,~(?[X22]:(iext(uri_ex_p,uri_ex_s,X22)&iext(uri_rdf_type,X22,uri_ex_c))),inference(assume_negation,[status(cth)],[140])).
% fof(145, plain,![X1]:![X2]:((~(iext(uri_rdf_type,X1,X2))|icext(X2,X1))&(~(icext(X2,X1))|iext(uri_rdf_type,X1,X2))),inference(fof_nnf,[status(thm)],[1])).
% fof(146, plain,![X3]:![X4]:((~(iext(uri_rdf_type,X3,X4))|icext(X4,X3))&(~(icext(X4,X3))|iext(uri_rdf_type,X3,X4))),inference(variable_rename,[status(thm)],[145])).
% cnf(147,plain,(iext(uri_rdf_type,X1,X2)|~icext(X2,X1)),inference(split_conjunct,[status(thm)],[146])).
% cnf(148,plain,(icext(X1,X2)|~iext(uri_rdf_type,X2,X1)),inference(split_conjunct,[status(thm)],[146])).
% fof(159, plain,?[X7]:(((((iext(uri_rdf_type,uri_ex_p,uri_owl_ObjectProperty)&iext(uri_rdf_type,uri_ex_c,uri_owl_Class))&iext(uri_rdf_type,uri_ex_s,X7))&iext(uri_rdf_type,X7,uri_owl_Restriction))&iext(uri_owl_onProperty,X7,uri_ex_p))&iext(uri_owl_someValuesFrom,X7,uri_ex_c)),inference(variable_rename,[status(thm)],[7])).
% fof(160, plain,(((((iext(uri_rdf_type,uri_ex_p,uri_owl_ObjectProperty)&iext(uri_rdf_type,uri_ex_c,uri_owl_Class))&iext(uri_rdf_type,uri_ex_s,esk2_0))&iext(uri_rdf_type,esk2_0,uri_owl_Restriction))&iext(uri_owl_onProperty,esk2_0,uri_ex_p))&iext(uri_owl_someValuesFrom,esk2_0,uri_ex_c)),inference(skolemize,[status(esa)],[159])).
% cnf(161,plain,(iext(uri_owl_someValuesFrom,esk2_0,uri_ex_c)),inference(split_conjunct,[status(thm)],[160])).
% cnf(162,plain,(iext(uri_owl_onProperty,esk2_0,uri_ex_p)),inference(split_conjunct,[status(thm)],[160])).
% cnf(164,plain,(iext(uri_rdf_type,uri_ex_s,esk2_0)),inference(split_conjunct,[status(thm)],[160])).
% fof(167, plain,![X7]:![X4]:![X2]:((~(iext(uri_owl_someValuesFrom,X7,X2))|~(iext(uri_owl_onProperty,X7,X4)))|![X1]:((~(icext(X7,X1))|?[X8]:(iext(X4,X1,X8)&icext(X2,X8)))&(![X8]:(~(iext(X4,X1,X8))|~(icext(X2,X8)))|icext(X7,X1)))),inference(fof_nnf,[status(thm)],[8])).
% fof(168, plain,![X9]:![X10]:![X11]:((~(iext(uri_owl_someValuesFrom,X9,X11))|~(iext(uri_owl_onProperty,X9,X10)))|![X12]:((~(icext(X9,X12))|?[X13]:(iext(X10,X12,X13)&icext(X11,X13)))&(![X14]:(~(iext(X10,X12,X14))|~(icext(X11,X14)))|icext(X9,X12)))),inference(variable_rename,[status(thm)],[167])).
% fof(169, plain,![X9]:![X10]:![X11]:((~(iext(uri_owl_someValuesFrom,X9,X11))|~(iext(uri_owl_onProperty,X9,X10)))|![X12]:((~(icext(X9,X12))|(iext(X10,X12,esk3_4(X9,X10,X11,X12))&icext(X11,esk3_4(X9,X10,X11,X12))))&(![X14]:(~(iext(X10,X12,X14))|~(icext(X11,X14)))|icext(X9,X12)))),inference(skolemize,[status(esa)],[168])).
% fof(170, plain,![X9]:![X10]:![X11]:![X12]:![X14]:((((~(iext(X10,X12,X14))|~(icext(X11,X14)))|icext(X9,X12))&(~(icext(X9,X12))|(iext(X10,X12,esk3_4(X9,X10,X11,X12))&icext(X11,esk3_4(X9,X10,X11,X12)))))|(~(iext(uri_owl_someValuesFrom,X9,X11))|~(iext(uri_owl_onProperty,X9,X10)))),inference(shift_quantors,[status(thm)],[169])).
% fof(171, plain,![X9]:![X10]:![X11]:![X12]:![X14]:((((~(iext(X10,X12,X14))|~(icext(X11,X14)))|icext(X9,X12))|(~(iext(uri_owl_someValuesFrom,X9,X11))|~(iext(uri_owl_onProperty,X9,X10))))&(((iext(X10,X12,esk3_4(X9,X10,X11,X12))|~(icext(X9,X12)))|(~(iext(uri_owl_someValuesFrom,X9,X11))|~(iext(uri_owl_onProperty,X9,X10))))&((icext(X11,esk3_4(X9,X10,X11,X12))|~(icext(X9,X12)))|(~(iext(uri_owl_someValuesFrom,X9,X11))|~(iext(uri_owl_onProperty,X9,X10)))))),inference(distribute,[status(thm)],[170])).
% cnf(172,plain,(icext(X3,esk3_4(X1,X2,X3,X4))|~iext(uri_owl_onProperty,X1,X2)|~iext(uri_owl_someValuesFrom,X1,X3)|~icext(X1,X4)),inference(split_conjunct,[status(thm)],[171])).
% cnf(173,plain,(iext(X2,X4,esk3_4(X1,X2,X3,X4))|~iext(uri_owl_onProperty,X1,X2)|~iext(uri_owl_someValuesFrom,X1,X3)|~icext(X1,X4)),inference(split_conjunct,[status(thm)],[171])).
% fof(600, negated_conjecture,![X22]:(~(iext(uri_ex_p,uri_ex_s,X22))|~(iext(uri_rdf_type,X22,uri_ex_c))),inference(fof_nnf,[status(thm)],[141])).
% fof(601, negated_conjecture,![X23]:(~(iext(uri_ex_p,uri_ex_s,X23))|~(iext(uri_rdf_type,X23,uri_ex_c))),inference(variable_rename,[status(thm)],[600])).
% cnf(602,negated_conjecture,(~iext(uri_rdf_type,X1,uri_ex_c)|~iext(uri_ex_p,uri_ex_s,X1)),inference(split_conjunct,[status(thm)],[601])).
% cnf(688,plain,(icext(esk2_0,uri_ex_s)),inference(spm,[status(thm)],[148,164,theory(equality)])).
% cnf(1491,negated_conjecture,(~iext(uri_rdf_type,esk3_4(X1,uri_ex_p,X2,uri_ex_s),uri_ex_c)|~icext(X1,uri_ex_s)|~iext(uri_owl_onProperty,X1,uri_ex_p)|~iext(uri_owl_someValuesFrom,X1,X2)),inference(spm,[status(thm)],[602,173,theory(equality)])).
% cnf(15728,negated_conjecture,(~icext(X1,uri_ex_s)|~iext(uri_owl_onProperty,X1,uri_ex_p)|~iext(uri_owl_someValuesFrom,X1,X2)|~icext(uri_ex_c,esk3_4(X1,uri_ex_p,X2,uri_ex_s))),inference(spm,[status(thm)],[1491,147,theory(equality)])).
% cnf(46674,negated_conjecture,(~icext(X1,uri_ex_s)|~iext(uri_owl_onProperty,X1,uri_ex_p)|~iext(uri_owl_someValuesFrom,X1,uri_ex_c)),inference(spm,[status(thm)],[15728,172,theory(equality)])).
% cnf(46675,negated_conjecture,(~icext(esk2_0,uri_ex_s)|~iext(uri_owl_onProperty,esk2_0,uri_ex_p)),inference(spm,[status(thm)],[46674,161,theory(equality)])).
% cnf(46676,negated_conjecture,($false|~iext(uri_owl_onProperty,esk2_0,uri_ex_p)),inference(rw,[status(thm)],[46675,688,theory(equality)])).
% cnf(46677,negated_conjecture,($false|$false),inference(rw,[status(thm)],[46676,162,theory(equality)])).
% cnf(46678,negated_conjecture,($false),inference(cn,[status(thm)],[46677,theory(equality)])).
% cnf(46679,negated_conjecture,($false),46678,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 12566
% # ...of these trivial : 199
% # ...subsumed : 5696
% # ...remaining for further processing: 6671
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 405
% # Backward-rewritten : 1
% # Generated clauses : 36331
% # ...of the previous two non-trivial : 30647
% # Contextual simplify-reflections : 2471
% # Paramodulations : 36331
% # Factorizations : 0
% # Equation resolutions : 0
% # Current number of processed clauses: 6053
% # Positive orientable unit clauses: 408
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 1
% # Non-unit-clauses : 5644
% # Current number of unprocessed clauses: 17975
% # ...number of literals in the above : 107560
% # Clause-clause subsumption calls (NU) : 824251
% # Rec. Clause-clause subsumption calls : 530547
% # Unit Clause-clause subsumption calls : 719
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 361
% # Indexed BW rewrite successes : 1
% # Backwards rewriting index: 1755 leaves, 1.89+/-3.180 terms/leaf
% # Paramod-from index: 990 leaves, 1.67+/-1.965 terms/leaf
% # Paramod-into index: 1533 leaves, 1.66+/-2.140 terms/leaf
% # -------------------------------------------------
% # User time : 4.724 s
% # System time : 0.086 s
% # Total time : 4.810 s
% # Maximum resident set size: 0 pages
% PrfWatch: 5.42 CPU 5.52 WC
% FINAL PrfWatch: 5.42 CPU 5.52 WC
% SZS output end Solution for /tmp/SystemOnTPTP16865/SWB009+3.tptp
%
%------------------------------------------------------------------------------