%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : SWB010+2 : TPTP v5.2.0. Released v5.2.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 Feb 16 03:18:28 EST 2011
% Result : Theorem 0.64s
% Output : Solution 0.64s
% 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/SystemOnTPTP1464/SWB010+2.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP1464/SWB010+2.tptp
% SZS output start Solution for /tmp/SystemOnTPTP1464/SWB010+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 1578
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.01 WC
% # Preprocessing time : 0.013 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(2, axiom,![X3]:![X4]:![X5]:((((ir(X4)&ip(X3))&ir(X5))&~(iext(X3,X4,X5)))=>?[X6]:((iext(uri_owl_sourceIndividual,X6,X4)&iext(uri_owl_assertionProperty,X6,X3))&iext(uri_owl_targetIndividual,X6,X5))),file('/tmp/SRASS.s.p', owl_npa_object_fi)).
% fof(3, axiom,![X1]:![X7]:(iext(uri_owl_sourceIndividual,X1,X7)=>(icext(uri_owl_NegativePropertyAssertion,X1)&ir(X7))),file('/tmp/SRASS.s.p', owl_prop_sourceindividual_ext)).
% fof(4, axiom,![X1]:ir(X1),file('/tmp/SRASS.s.p', simple_ir)).
% fof(5, axiom,![X6]:![X3]:![X2]:((iext(uri_owl_allValuesFrom,X6,X2)&iext(uri_owl_onProperty,X6,X3))=>![X1]:(icext(X6,X1)<=>![X7]:(iext(X3,X1,X7)=>icext(X2,X7)))),file('/tmp/SRASS.s.p', owl_restrict_allvaluesfrom)).
% fof(6, axiom,?[X8]:?[X9]:?[X10]:?[X11]:(((((((iext(uri_rdf_type,uri_ex_p,uri_owl_ObjectProperty)&iext(uri_rdf_type,uri_ex_s,X8))&iext(uri_owl_onProperty,X8,uri_ex_p))&iext(uri_owl_allValuesFrom,X8,X9))&iext(uri_owl_complementOf,X9,X10))&iext(uri_owl_oneOf,X10,X11))&iext(uri_rdf_first,X11,uri_ex_o))&iext(uri_rdf_rest,X11,uri_rdf_nil)),file('/tmp/SRASS.s.p', testcase_premise_fullish_010_Negative_Property_Assertions)).
% fof(7, axiom,![X6]:![X12]:![X4]:((iext(uri_rdf_first,X12,X4)&iext(uri_rdf_rest,X12,uri_rdf_nil))=>(iext(uri_owl_oneOf,X6,X12)<=>(ic(X6)&![X1]:(icext(X6,X1)<=>X1=X4)))),file('/tmp/SRASS.s.p', owl_enum_class_001)).
% fof(8, axiom,![X6]:![X2]:(iext(uri_owl_complementOf,X6,X2)=>((ic(X6)&ic(X2))&![X1]:(icext(X6,X1)<=>~(icext(X2,X1))))),file('/tmp/SRASS.s.p', owl_bool_complementof_class)).
% fof(9, axiom,![X1]:![X7]:(iext(uri_owl_onProperty,X1,X7)=>(icext(uri_owl_Restriction,X1)&ip(X7))),file('/tmp/SRASS.s.p', owl_prop_onproperty_ext)).
% fof(10, conjecture,?[X13]:(((iext(uri_rdf_type,X13,uri_owl_NegativePropertyAssertion)&iext(uri_owl_sourceIndividual,X13,uri_ex_s))&iext(uri_owl_assertionProperty,X13,uri_ex_p))&iext(uri_owl_targetIndividual,X13,uri_ex_o)),file('/tmp/SRASS.s.p', testcase_conclusion_fullish_010_Negative_Property_Assertions)).
% fof(11, negated_conjecture,~(?[X13]:(((iext(uri_rdf_type,X13,uri_owl_NegativePropertyAssertion)&iext(uri_owl_sourceIndividual,X13,uri_ex_s))&iext(uri_owl_assertionProperty,X13,uri_ex_p))&iext(uri_owl_targetIndividual,X13,uri_ex_o))),inference(assume_negation,[status(cth)],[10])).
% fof(12, plain,![X3]:![X4]:![X5]:((((ir(X4)&ip(X3))&ir(X5))&~(iext(X3,X4,X5)))=>?[X6]:((iext(uri_owl_sourceIndividual,X6,X4)&iext(uri_owl_assertionProperty,X6,X3))&iext(uri_owl_targetIndividual,X6,X5))),inference(fof_simplification,[status(thm)],[2,theory(equality)])).
% fof(13, plain,![X6]:![X2]:(iext(uri_owl_complementOf,X6,X2)=>((ic(X6)&ic(X2))&![X1]:(icext(X6,X1)<=>~(icext(X2,X1))))),inference(fof_simplification,[status(thm)],[8,theory(equality)])).
% fof(14, 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(15, 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)],[14])).
% cnf(16,plain,(iext(uri_rdf_type,X1,X2)|~icext(X2,X1)),inference(split_conjunct,[status(thm)],[15])).
% cnf(17,plain,(icext(X1,X2)|~iext(uri_rdf_type,X2,X1)),inference(split_conjunct,[status(thm)],[15])).
% fof(18, plain,![X3]:![X4]:![X5]:((((~(ir(X4))|~(ip(X3)))|~(ir(X5)))|iext(X3,X4,X5))|?[X6]:((iext(uri_owl_sourceIndividual,X6,X4)&iext(uri_owl_assertionProperty,X6,X3))&iext(uri_owl_targetIndividual,X6,X5))),inference(fof_nnf,[status(thm)],[12])).
% fof(19, plain,![X7]:![X8]:![X9]:((((~(ir(X8))|~(ip(X7)))|~(ir(X9)))|iext(X7,X8,X9))|?[X10]:((iext(uri_owl_sourceIndividual,X10,X8)&iext(uri_owl_assertionProperty,X10,X7))&iext(uri_owl_targetIndividual,X10,X9))),inference(variable_rename,[status(thm)],[18])).
% fof(20, plain,![X7]:![X8]:![X9]:((((~(ir(X8))|~(ip(X7)))|~(ir(X9)))|iext(X7,X8,X9))|((iext(uri_owl_sourceIndividual,esk1_3(X7,X8,X9),X8)&iext(uri_owl_assertionProperty,esk1_3(X7,X8,X9),X7))&iext(uri_owl_targetIndividual,esk1_3(X7,X8,X9),X9))),inference(skolemize,[status(esa)],[19])).
% fof(21, plain,![X7]:![X8]:![X9]:(((iext(uri_owl_sourceIndividual,esk1_3(X7,X8,X9),X8)|(((~(ir(X8))|~(ip(X7)))|~(ir(X9)))|iext(X7,X8,X9)))&(iext(uri_owl_assertionProperty,esk1_3(X7,X8,X9),X7)|(((~(ir(X8))|~(ip(X7)))|~(ir(X9)))|iext(X7,X8,X9))))&(iext(uri_owl_targetIndividual,esk1_3(X7,X8,X9),X9)|(((~(ir(X8))|~(ip(X7)))|~(ir(X9)))|iext(X7,X8,X9)))),inference(distribute,[status(thm)],[20])).
% cnf(22,plain,(iext(X1,X2,X3)|iext(uri_owl_targetIndividual,esk1_3(X1,X2,X3),X3)|~ir(X3)|~ip(X1)|~ir(X2)),inference(split_conjunct,[status(thm)],[21])).
% cnf(23,plain,(iext(X1,X2,X3)|iext(uri_owl_assertionProperty,esk1_3(X1,X2,X3),X1)|~ir(X3)|~ip(X1)|~ir(X2)),inference(split_conjunct,[status(thm)],[21])).
% cnf(24,plain,(iext(X1,X2,X3)|iext(uri_owl_sourceIndividual,esk1_3(X1,X2,X3),X2)|~ir(X3)|~ip(X1)|~ir(X2)),inference(split_conjunct,[status(thm)],[21])).
% fof(25, plain,![X1]:![X7]:(~(iext(uri_owl_sourceIndividual,X1,X7))|(icext(uri_owl_NegativePropertyAssertion,X1)&ir(X7))),inference(fof_nnf,[status(thm)],[3])).
% fof(26, plain,![X8]:![X9]:(~(iext(uri_owl_sourceIndividual,X8,X9))|(icext(uri_owl_NegativePropertyAssertion,X8)&ir(X9))),inference(variable_rename,[status(thm)],[25])).
% fof(27, plain,![X8]:![X9]:((icext(uri_owl_NegativePropertyAssertion,X8)|~(iext(uri_owl_sourceIndividual,X8,X9)))&(ir(X9)|~(iext(uri_owl_sourceIndividual,X8,X9)))),inference(distribute,[status(thm)],[26])).
% cnf(29,plain,(icext(uri_owl_NegativePropertyAssertion,X1)|~iext(uri_owl_sourceIndividual,X1,X2)),inference(split_conjunct,[status(thm)],[27])).
% fof(30, plain,![X2]:ir(X2),inference(variable_rename,[status(thm)],[4])).
% cnf(31,plain,(ir(X1)),inference(split_conjunct,[status(thm)],[30])).
% fof(32, plain,![X6]:![X3]:![X2]:((~(iext(uri_owl_allValuesFrom,X6,X2))|~(iext(uri_owl_onProperty,X6,X3)))|![X1]:((~(icext(X6,X1))|![X7]:(~(iext(X3,X1,X7))|icext(X2,X7)))&(?[X7]:(iext(X3,X1,X7)&~(icext(X2,X7)))|icext(X6,X1)))),inference(fof_nnf,[status(thm)],[5])).
% fof(33, plain,![X8]:![X9]:![X10]:((~(iext(uri_owl_allValuesFrom,X8,X10))|~(iext(uri_owl_onProperty,X8,X9)))|![X11]:((~(icext(X8,X11))|![X12]:(~(iext(X9,X11,X12))|icext(X10,X12)))&(?[X13]:(iext(X9,X11,X13)&~(icext(X10,X13)))|icext(X8,X11)))),inference(variable_rename,[status(thm)],[32])).
% fof(34, plain,![X8]:![X9]:![X10]:((~(iext(uri_owl_allValuesFrom,X8,X10))|~(iext(uri_owl_onProperty,X8,X9)))|![X11]:((~(icext(X8,X11))|![X12]:(~(iext(X9,X11,X12))|icext(X10,X12)))&((iext(X9,X11,esk2_4(X8,X9,X10,X11))&~(icext(X10,esk2_4(X8,X9,X10,X11))))|icext(X8,X11)))),inference(skolemize,[status(esa)],[33])).
% fof(35, plain,![X8]:![X9]:![X10]:![X11]:![X12]:((((~(iext(X9,X11,X12))|icext(X10,X12))|~(icext(X8,X11)))&((iext(X9,X11,esk2_4(X8,X9,X10,X11))&~(icext(X10,esk2_4(X8,X9,X10,X11))))|icext(X8,X11)))|(~(iext(uri_owl_allValuesFrom,X8,X10))|~(iext(uri_owl_onProperty,X8,X9)))),inference(shift_quantors,[status(thm)],[34])).
% fof(36, plain,![X8]:![X9]:![X10]:![X11]:![X12]:((((~(iext(X9,X11,X12))|icext(X10,X12))|~(icext(X8,X11)))|(~(iext(uri_owl_allValuesFrom,X8,X10))|~(iext(uri_owl_onProperty,X8,X9))))&(((iext(X9,X11,esk2_4(X8,X9,X10,X11))|icext(X8,X11))|(~(iext(uri_owl_allValuesFrom,X8,X10))|~(iext(uri_owl_onProperty,X8,X9))))&((~(icext(X10,esk2_4(X8,X9,X10,X11)))|icext(X8,X11))|(~(iext(uri_owl_allValuesFrom,X8,X10))|~(iext(uri_owl_onProperty,X8,X9)))))),inference(distribute,[status(thm)],[35])).
% cnf(39,plain,(icext(X3,X5)|~iext(uri_owl_onProperty,X1,X2)|~iext(uri_owl_allValuesFrom,X1,X3)|~icext(X1,X4)|~iext(X2,X4,X5)),inference(split_conjunct,[status(thm)],[36])).
% fof(40, plain,?[X12]:?[X13]:?[X14]:?[X15]:(((((((iext(uri_rdf_type,uri_ex_p,uri_owl_ObjectProperty)&iext(uri_rdf_type,uri_ex_s,X12))&iext(uri_owl_onProperty,X12,uri_ex_p))&iext(uri_owl_allValuesFrom,X12,X13))&iext(uri_owl_complementOf,X13,X14))&iext(uri_owl_oneOf,X14,X15))&iext(uri_rdf_first,X15,uri_ex_o))&iext(uri_rdf_rest,X15,uri_rdf_nil)),inference(variable_rename,[status(thm)],[6])).
% fof(41, plain,(((((((iext(uri_rdf_type,uri_ex_p,uri_owl_ObjectProperty)&iext(uri_rdf_type,uri_ex_s,esk3_0))&iext(uri_owl_onProperty,esk3_0,uri_ex_p))&iext(uri_owl_allValuesFrom,esk3_0,esk4_0))&iext(uri_owl_complementOf,esk4_0,esk5_0))&iext(uri_owl_oneOf,esk5_0,esk6_0))&iext(uri_rdf_first,esk6_0,uri_ex_o))&iext(uri_rdf_rest,esk6_0,uri_rdf_nil)),inference(skolemize,[status(esa)],[40])).
% cnf(42,plain,(iext(uri_rdf_rest,esk6_0,uri_rdf_nil)),inference(split_conjunct,[status(thm)],[41])).
% cnf(43,plain,(iext(uri_rdf_first,esk6_0,uri_ex_o)),inference(split_conjunct,[status(thm)],[41])).
% cnf(44,plain,(iext(uri_owl_oneOf,esk5_0,esk6_0)),inference(split_conjunct,[status(thm)],[41])).
% cnf(45,plain,(iext(uri_owl_complementOf,esk4_0,esk5_0)),inference(split_conjunct,[status(thm)],[41])).
% cnf(46,plain,(iext(uri_owl_allValuesFrom,esk3_0,esk4_0)),inference(split_conjunct,[status(thm)],[41])).
% cnf(47,plain,(iext(uri_owl_onProperty,esk3_0,uri_ex_p)),inference(split_conjunct,[status(thm)],[41])).
% cnf(48,plain,(iext(uri_rdf_type,uri_ex_s,esk3_0)),inference(split_conjunct,[status(thm)],[41])).
% fof(50, plain,![X6]:![X12]:![X4]:((~(iext(uri_rdf_first,X12,X4))|~(iext(uri_rdf_rest,X12,uri_rdf_nil)))|((~(iext(uri_owl_oneOf,X6,X12))|(ic(X6)&![X1]:((~(icext(X6,X1))|X1=X4)&(~(X1=X4)|icext(X6,X1)))))&((~(ic(X6))|?[X1]:((~(icext(X6,X1))|~(X1=X4))&(icext(X6,X1)|X1=X4)))|iext(uri_owl_oneOf,X6,X12)))),inference(fof_nnf,[status(thm)],[7])).
% fof(51, plain,![X13]:![X14]:![X15]:((~(iext(uri_rdf_first,X14,X15))|~(iext(uri_rdf_rest,X14,uri_rdf_nil)))|((~(iext(uri_owl_oneOf,X13,X14))|(ic(X13)&![X16]:((~(icext(X13,X16))|X16=X15)&(~(X16=X15)|icext(X13,X16)))))&((~(ic(X13))|?[X17]:((~(icext(X13,X17))|~(X17=X15))&(icext(X13,X17)|X17=X15)))|iext(uri_owl_oneOf,X13,X14)))),inference(variable_rename,[status(thm)],[50])).
% fof(52, plain,![X13]:![X14]:![X15]:((~(iext(uri_rdf_first,X14,X15))|~(iext(uri_rdf_rest,X14,uri_rdf_nil)))|((~(iext(uri_owl_oneOf,X13,X14))|(ic(X13)&![X16]:((~(icext(X13,X16))|X16=X15)&(~(X16=X15)|icext(X13,X16)))))&((~(ic(X13))|((~(icext(X13,esk7_3(X13,X14,X15)))|~(esk7_3(X13,X14,X15)=X15))&(icext(X13,esk7_3(X13,X14,X15))|esk7_3(X13,X14,X15)=X15)))|iext(uri_owl_oneOf,X13,X14)))),inference(skolemize,[status(esa)],[51])).
% fof(53, plain,![X13]:![X14]:![X15]:![X16]:((((((~(icext(X13,X16))|X16=X15)&(~(X16=X15)|icext(X13,X16)))&ic(X13))|~(iext(uri_owl_oneOf,X13,X14)))&((~(ic(X13))|((~(icext(X13,esk7_3(X13,X14,X15)))|~(esk7_3(X13,X14,X15)=X15))&(icext(X13,esk7_3(X13,X14,X15))|esk7_3(X13,X14,X15)=X15)))|iext(uri_owl_oneOf,X13,X14)))|(~(iext(uri_rdf_first,X14,X15))|~(iext(uri_rdf_rest,X14,uri_rdf_nil)))),inference(shift_quantors,[status(thm)],[52])).
% fof(54, plain,![X13]:![X14]:![X15]:![X16]:((((((~(icext(X13,X16))|X16=X15)|~(iext(uri_owl_oneOf,X13,X14)))|(~(iext(uri_rdf_first,X14,X15))|~(iext(uri_rdf_rest,X14,uri_rdf_nil))))&(((~(X16=X15)|icext(X13,X16))|~(iext(uri_owl_oneOf,X13,X14)))|(~(iext(uri_rdf_first,X14,X15))|~(iext(uri_rdf_rest,X14,uri_rdf_nil)))))&((ic(X13)|~(iext(uri_owl_oneOf,X13,X14)))|(~(iext(uri_rdf_first,X14,X15))|~(iext(uri_rdf_rest,X14,uri_rdf_nil)))))&(((((~(icext(X13,esk7_3(X13,X14,X15)))|~(esk7_3(X13,X14,X15)=X15))|~(ic(X13)))|iext(uri_owl_oneOf,X13,X14))|(~(iext(uri_rdf_first,X14,X15))|~(iext(uri_rdf_rest,X14,uri_rdf_nil))))&((((icext(X13,esk7_3(X13,X14,X15))|esk7_3(X13,X14,X15)=X15)|~(ic(X13)))|iext(uri_owl_oneOf,X13,X14))|(~(iext(uri_rdf_first,X14,X15))|~(iext(uri_rdf_rest,X14,uri_rdf_nil)))))),inference(distribute,[status(thm)],[53])).
% cnf(58,plain,(icext(X3,X4)|~iext(uri_rdf_rest,X1,uri_rdf_nil)|~iext(uri_rdf_first,X1,X2)|~iext(uri_owl_oneOf,X3,X1)|X4!=X2),inference(split_conjunct,[status(thm)],[54])).
% fof(60, plain,![X6]:![X2]:(~(iext(uri_owl_complementOf,X6,X2))|((ic(X6)&ic(X2))&![X1]:((~(icext(X6,X1))|~(icext(X2,X1)))&(icext(X2,X1)|icext(X6,X1))))),inference(fof_nnf,[status(thm)],[13])).
% fof(61, plain,![X7]:![X8]:(~(iext(uri_owl_complementOf,X7,X8))|((ic(X7)&ic(X8))&![X9]:((~(icext(X7,X9))|~(icext(X8,X9)))&(icext(X8,X9)|icext(X7,X9))))),inference(variable_rename,[status(thm)],[60])).
% fof(62, plain,![X7]:![X8]:![X9]:((((~(icext(X7,X9))|~(icext(X8,X9)))&(icext(X8,X9)|icext(X7,X9)))&(ic(X7)&ic(X8)))|~(iext(uri_owl_complementOf,X7,X8))),inference(shift_quantors,[status(thm)],[61])).
% fof(63, plain,![X7]:![X8]:![X9]:((((~(icext(X7,X9))|~(icext(X8,X9)))|~(iext(uri_owl_complementOf,X7,X8)))&((icext(X8,X9)|icext(X7,X9))|~(iext(uri_owl_complementOf,X7,X8))))&((ic(X7)|~(iext(uri_owl_complementOf,X7,X8)))&(ic(X8)|~(iext(uri_owl_complementOf,X7,X8))))),inference(distribute,[status(thm)],[62])).
% cnf(67,plain,(~iext(uri_owl_complementOf,X1,X2)|~icext(X2,X3)|~icext(X1,X3)),inference(split_conjunct,[status(thm)],[63])).
% fof(68, plain,![X1]:![X7]:(~(iext(uri_owl_onProperty,X1,X7))|(icext(uri_owl_Restriction,X1)&ip(X7))),inference(fof_nnf,[status(thm)],[9])).
% fof(69, plain,![X8]:![X9]:(~(iext(uri_owl_onProperty,X8,X9))|(icext(uri_owl_Restriction,X8)&ip(X9))),inference(variable_rename,[status(thm)],[68])).
% fof(70, plain,![X8]:![X9]:((icext(uri_owl_Restriction,X8)|~(iext(uri_owl_onProperty,X8,X9)))&(ip(X9)|~(iext(uri_owl_onProperty,X8,X9)))),inference(distribute,[status(thm)],[69])).
% cnf(71,plain,(ip(X2)|~iext(uri_owl_onProperty,X1,X2)),inference(split_conjunct,[status(thm)],[70])).
% fof(73, negated_conjecture,![X13]:(((~(iext(uri_rdf_type,X13,uri_owl_NegativePropertyAssertion))|~(iext(uri_owl_sourceIndividual,X13,uri_ex_s)))|~(iext(uri_owl_assertionProperty,X13,uri_ex_p)))|~(iext(uri_owl_targetIndividual,X13,uri_ex_o))),inference(fof_nnf,[status(thm)],[11])).
% fof(74, negated_conjecture,![X14]:(((~(iext(uri_rdf_type,X14,uri_owl_NegativePropertyAssertion))|~(iext(uri_owl_sourceIndividual,X14,uri_ex_s)))|~(iext(uri_owl_assertionProperty,X14,uri_ex_p)))|~(iext(uri_owl_targetIndividual,X14,uri_ex_o))),inference(variable_rename,[status(thm)],[73])).
% cnf(75,negated_conjecture,(~iext(uri_owl_targetIndividual,X1,uri_ex_o)|~iext(uri_owl_assertionProperty,X1,uri_ex_p)|~iext(uri_owl_sourceIndividual,X1,uri_ex_s)|~iext(uri_rdf_type,X1,uri_owl_NegativePropertyAssertion)),inference(split_conjunct,[status(thm)],[74])).
% cnf(77,plain,(iext(X1,X2,X3)|iext(uri_owl_sourceIndividual,esk1_3(X1,X2,X3),X2)|$false|$false|~ip(X1)),inference(rw,[status(thm)],[inference(rw,[status(thm)],[24,31,theory(equality)]),31,theory(equality)]),['unfolding']).
% cnf(78,plain,(iext(X1,X2,X3)|iext(uri_owl_assertionProperty,esk1_3(X1,X2,X3),X1)|$false|$false|~ip(X1)),inference(rw,[status(thm)],[inference(rw,[status(thm)],[23,31,theory(equality)]),31,theory(equality)]),['unfolding']).
% cnf(79,plain,(iext(X1,X2,X3)|iext(uri_owl_targetIndividual,esk1_3(X1,X2,X3),X3)|$false|$false|~ip(X1)),inference(rw,[status(thm)],[inference(rw,[status(thm)],[22,31,theory(equality)]),31,theory(equality)]),['unfolding']).
% cnf(80,plain,(~icext(esk5_0,X1)|~icext(esk4_0,X1)),inference(spm,[status(thm)],[67,45,theory(equality)])).
% cnf(82,plain,(ip(uri_ex_p)),inference(spm,[status(thm)],[71,47,theory(equality)])).
% cnf(89,plain,(icext(uri_owl_NegativePropertyAssertion,esk1_3(X1,X2,X3))|iext(X1,X2,X3)|~ip(X1)),inference(spm,[status(thm)],[29,77,theory(equality)])).
% cnf(90,negated_conjecture,(iext(X1,X2,uri_ex_o)|~iext(uri_rdf_type,esk1_3(X1,X2,uri_ex_o),uri_owl_NegativePropertyAssertion)|~iext(uri_owl_sourceIndividual,esk1_3(X1,X2,uri_ex_o),uri_ex_s)|~iext(uri_owl_assertionProperty,esk1_3(X1,X2,uri_ex_o),uri_ex_p)|~ip(X1)),inference(spm,[status(thm)],[75,79,theory(equality)])).
% cnf(101,plain,(icext(X1,X2)|~iext(uri_rdf_rest,X3,uri_rdf_nil)|~iext(uri_owl_oneOf,X1,X3)|~iext(uri_rdf_first,X3,X2)),inference(er,[status(thm)],[58,theory(equality)])).
% cnf(104,plain,(icext(esk4_0,X1)|~icext(esk3_0,X2)|~iext(uri_owl_onProperty,esk3_0,X3)|~iext(X3,X2,X1)),inference(spm,[status(thm)],[39,46,theory(equality)])).
% cnf(145,plain,(iext(uri_rdf_type,esk1_3(X1,X2,X3),uri_owl_NegativePropertyAssertion)|iext(X1,X2,X3)|~ip(X1)),inference(spm,[status(thm)],[16,89,theory(equality)])).
% cnf(158,plain,(icext(X1,X2)|~iext(uri_owl_oneOf,X1,esk6_0)|~iext(uri_rdf_first,esk6_0,X2)),inference(spm,[status(thm)],[101,42,theory(equality)])).
% cnf(159,plain,(~icext(esk4_0,X1)|~iext(uri_owl_oneOf,esk5_0,esk6_0)|~iext(uri_rdf_first,esk6_0,X1)),inference(spm,[status(thm)],[80,158,theory(equality)])).
% cnf(165,plain,(~icext(esk4_0,X1)|$false|~iext(uri_rdf_first,esk6_0,X1)),inference(rw,[status(thm)],[159,44,theory(equality)])).
% cnf(166,plain,(~icext(esk4_0,X1)|~iext(uri_rdf_first,esk6_0,X1)),inference(cn,[status(thm)],[165,theory(equality)])).
% cnf(168,negated_conjecture,(iext(X1,X2,uri_ex_o)|~ip(X1)|~iext(uri_owl_sourceIndividual,esk1_3(X1,X2,uri_ex_o),uri_ex_s)|~iext(uri_owl_assertionProperty,esk1_3(X1,X2,uri_ex_o),uri_ex_p)),inference(csr,[status(thm)],[90,145])).
% cnf(169,negated_conjecture,(iext(uri_ex_p,X1,uri_ex_o)|~ip(uri_ex_p)|~iext(uri_owl_sourceIndividual,esk1_3(uri_ex_p,X1,uri_ex_o),uri_ex_s)),inference(spm,[status(thm)],[168,78,theory(equality)])).
% cnf(170,negated_conjecture,(iext(uri_ex_p,X1,uri_ex_o)|$false|~iext(uri_owl_sourceIndividual,esk1_3(uri_ex_p,X1,uri_ex_o),uri_ex_s)),inference(rw,[status(thm)],[169,82,theory(equality)])).
% cnf(171,negated_conjecture,(iext(uri_ex_p,X1,uri_ex_o)|~iext(uri_owl_sourceIndividual,esk1_3(uri_ex_p,X1,uri_ex_o),uri_ex_s)),inference(cn,[status(thm)],[170,theory(equality)])).
% cnf(173,plain,(~iext(uri_rdf_first,esk6_0,X1)|~iext(uri_rdf_type,X1,esk4_0)),inference(spm,[status(thm)],[166,17,theory(equality)])).
% cnf(191,plain,(icext(esk4_0,X1)|~icext(esk3_0,X2)|~iext(uri_ex_p,X2,X1)),inference(spm,[status(thm)],[104,47,theory(equality)])).
% cnf(240,negated_conjecture,(iext(uri_ex_p,uri_ex_s,uri_ex_o)|~ip(uri_ex_p)),inference(spm,[status(thm)],[171,77,theory(equality)])).
% cnf(241,negated_conjecture,(iext(uri_ex_p,uri_ex_s,uri_ex_o)|$false),inference(rw,[status(thm)],[240,82,theory(equality)])).
% cnf(242,negated_conjecture,(iext(uri_ex_p,uri_ex_s,uri_ex_o)),inference(cn,[status(thm)],[241,theory(equality)])).
% cnf(243,negated_conjecture,(icext(esk4_0,uri_ex_o)|~icext(esk3_0,uri_ex_s)),inference(spm,[status(thm)],[191,242,theory(equality)])).
% cnf(244,negated_conjecture,(iext(uri_rdf_type,uri_ex_o,esk4_0)|~icext(esk3_0,uri_ex_s)),inference(spm,[status(thm)],[16,243,theory(equality)])).
% cnf(249,negated_conjecture,(iext(uri_rdf_type,uri_ex_o,esk4_0)|~iext(uri_rdf_type,uri_ex_s,esk3_0)),inference(spm,[status(thm)],[244,17,theory(equality)])).
% cnf(255,negated_conjecture,(iext(uri_rdf_type,uri_ex_o,esk4_0)|$false),inference(rw,[status(thm)],[249,48,theory(equality)])).
% cnf(256,negated_conjecture,(iext(uri_rdf_type,uri_ex_o,esk4_0)),inference(cn,[status(thm)],[255,theory(equality)])).
% cnf(257,negated_conjecture,(~iext(uri_rdf_first,esk6_0,uri_ex_o)),inference(spm,[status(thm)],[173,256,theory(equality)])).
% cnf(259,negated_conjecture,($false),inference(rw,[status(thm)],[257,43,theory(equality)])).
% cnf(260,negated_conjecture,($false),inference(cn,[status(thm)],[259,theory(equality)])).
% cnf(261,negated_conjecture,($false),260,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 103
% # ...of these trivial : 0
% # ...subsumed : 16
% # ...remaining for further processing: 87
% # Other redundant clauses eliminated : 1
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 2
% # Backward-rewritten : 1
% # Generated clauses : 146
% # ...of the previous two non-trivial : 140
% # Contextual simplify-reflections : 4
% # Paramodulations : 145
% # Factorizations : 0
% # Equation resolutions : 1
% # Current number of processed clauses: 83
% # Positive orientable unit clauses: 15
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 1
% # Non-unit-clauses : 67
% # Current number of unprocessed clauses: 60
% # ...number of literals in the above : 311
% # Clause-clause subsumption calls (NU) : 185
% # Rec. Clause-clause subsumption calls : 107
% # Unit Clause-clause subsumption calls : 15
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 1
% # Indexed BW rewrite successes : 1
% # Backwards rewriting index: 79 leaves, 1.63+/-1.503 terms/leaf
% # Paramod-from index: 31 leaves, 1.13+/-0.707 terms/leaf
% # Paramod-into index: 72 leaves, 1.24+/-0.677 terms/leaf
% # -------------------------------------------------
% # User time : 0.018 s
% # System time : 0.005 s
% # Total time : 0.023 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.13 CPU 0.21 WC
% FINAL PrfWatch: 0.13 CPU 0.21 WC
% SZS output end Solution for /tmp/SystemOnTPTP1464/SWB010+2.tptp
%
%------------------------------------------------------------------------------