%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SWB027+2 : TPTP v8.1.2. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n012.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu May 9 17:42:55 EDT 2024
% Result : Theorem 19.51s 19.72s
% Output : Refutation 19.51s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SWB027+2 : TPTP v8.1.2. Released v5.2.0.
% 0.03/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.35 % Computer : n012.cluster.edu
% 0.12/0.35 % Model : x86_64 x86_64
% 0.12/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.35 % Memory : 8042.1875MB
% 0.12/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.35 % CPULimit : 300
% 0.12/0.35 % WCLimit : 300
% 0.12/0.35 % DateTime : Wed May 8 22:13:38 EDT 2024
% 0.12/0.35 % CPUTime :
% 19.51/19.72 % Version: 1.5
% 19.51/19.72 % SZS status Theorem
% 19.51/19.72 % SZS output start CNFRefutation
% 19.51/19.72 fof(testcase_conclusion_fullish_027_Inferred_Property_Characteristics_II,conjecture,iext(uri_rdf_type,uri_ex_p,uri_owl_InverseFunctionalProperty),file('/export/starexec/sandbox/benchmark/theBenchmark.p', testcase_conclusion_fullish_027_Inferred_Property_Characteristics_II)).
% 19.51/19.72 fof(c11,negated_conjecture,(~iext(uri_rdf_type,uri_ex_p,uri_owl_InverseFunctionalProperty)),inference(assume_negation,[status(cth)],[testcase_conclusion_fullish_027_Inferred_Property_Characteristics_II])).
% 19.51/19.72 fof(c12,negated_conjecture,~iext(uri_rdf_type,uri_ex_p,uri_owl_InverseFunctionalProperty),inference(fof_simplification,[status(thm)],[c11])).
% 19.51/19.72 cnf(c13,negated_conjecture,~iext(uri_rdf_type,uri_ex_p,uri_owl_InverseFunctionalProperty),inference(split_conjunct,[status(thm)],[c12])).
% 19.51/19.72 fof(rdfs_cext_def,axiom,(![X]:(![C]:(iext(uri_rdf_type,X,C)<=>icext(C,X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', rdfs_cext_def)).
% 19.51/19.72 fof(c55,plain,(![X]:(![C]:((~iext(uri_rdf_type,X,C)|icext(C,X))&(~icext(C,X)|iext(uri_rdf_type,X,C))))),inference(fof_nnf,[status(thm)],[rdfs_cext_def])).
% 19.51/19.72 fof(c56,plain,((![X]:(![C]:(~iext(uri_rdf_type,X,C)|icext(C,X))))&(![X]:(![C]:(~icext(C,X)|iext(uri_rdf_type,X,C))))),inference(shift_quantors,[status(thm)],[c55])).
% 19.51/19.72 fof(c58,plain,(![X38]:(![X39]:(![X40]:(![X41]:((~iext(uri_rdf_type,X38,X39)|icext(X39,X38))&(~icext(X41,X40)|iext(uri_rdf_type,X40,X41))))))),inference(shift_quantors,[status(thm)],[fof(c57,plain,((![X38]:(![X39]:(~iext(uri_rdf_type,X38,X39)|icext(X39,X38))))&(![X40]:(![X41]:(~icext(X41,X40)|iext(uri_rdf_type,X40,X41))))),inference(variable_rename,[status(thm)],[c56])).])).
% 19.51/19.72 cnf(c60,plain,~icext(X83,X82)|iext(uri_rdf_type,X82,X83),inference(split_conjunct,[status(thm)],[c58])).
% 19.51/19.72 fof(testcase_premise_fullish_027_Inferred_Property_Characteristics_II,axiom,(?[BNODE_l1]:(?[BNODE_l2]:(?[BNODE_v]:(((((iext(uri_owl_propertyChainAxiom,uri_owl_sameAs,BNODE_l1)&iext(uri_rdf_first,BNODE_l1,uri_ex_p))&iext(uri_rdf_rest,BNODE_l1,BNODE_l2))&iext(uri_rdf_first,BNODE_l2,BNODE_v))&iext(uri_rdf_rest,BNODE_l2,uri_rdf_nil))&iext(uri_owl_inverseOf,BNODE_v,uri_ex_p))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', testcase_premise_fullish_027_Inferred_Property_Characteristics_II)).
% 19.51/19.72 fof(c3,plain,(?[X2]:(?[X3]:(?[X4]:(((((iext(uri_owl_propertyChainAxiom,uri_owl_sameAs,X2)&iext(uri_rdf_first,X2,uri_ex_p))&iext(uri_rdf_rest,X2,X3))&iext(uri_rdf_first,X3,X4))&iext(uri_rdf_rest,X3,uri_rdf_nil))&iext(uri_owl_inverseOf,X4,uri_ex_p))))),inference(variable_rename,[status(thm)],[testcase_premise_fullish_027_Inferred_Property_Characteristics_II])).
% 19.51/19.72 fof(c4,plain,(((((iext(uri_owl_propertyChainAxiom,uri_owl_sameAs,skolem0001)&iext(uri_rdf_first,skolem0001,uri_ex_p))&iext(uri_rdf_rest,skolem0001,skolem0002))&iext(uri_rdf_first,skolem0002,skolem0003))&iext(uri_rdf_rest,skolem0002,uri_rdf_nil))&iext(uri_owl_inverseOf,skolem0003,uri_ex_p)),inference(skolemize,[status(esa)],[c3])).
% 19.51/19.72 cnf(c10,plain,iext(uri_owl_inverseOf,skolem0003,uri_ex_p),inference(split_conjunct,[status(thm)],[c4])).
% 19.51/19.72 fof(owl_inv,axiom,(![P1]:(![P2]:(iext(uri_owl_inverseOf,P1,P2)<=>((ip(P1)&ip(P2))&(![X]:(![Y]:(iext(P1,X,Y)<=>iext(P2,Y,X)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', owl_inv)).
% 19.51/19.72 fof(c14,plain,(![P1]:(![P2]:((~iext(uri_owl_inverseOf,P1,P2)|((ip(P1)&ip(P2))&(![X]:(![Y]:((~iext(P1,X,Y)|iext(P2,Y,X))&(~iext(P2,Y,X)|iext(P1,X,Y)))))))&(((~ip(P1)|~ip(P2))|(?[X]:(?[Y]:((~iext(P1,X,Y)|~iext(P2,Y,X))&(iext(P1,X,Y)|iext(P2,Y,X))))))|iext(uri_owl_inverseOf,P1,P2))))),inference(fof_nnf,[status(thm)],[owl_inv])).
% 19.51/19.72 fof(c15,plain,((![P1]:(![P2]:(~iext(uri_owl_inverseOf,P1,P2)|((ip(P1)&ip(P2))&((![X]:(![Y]:(~iext(P1,X,Y)|iext(P2,Y,X))))&(![X]:(![Y]:(~iext(P2,Y,X)|iext(P1,X,Y)))))))))&(![P1]:(![P2]:(((~ip(P1)|~ip(P2))|(?[X]:(?[Y]:((~iext(P1,X,Y)|~iext(P2,Y,X))&(iext(P1,X,Y)|iext(P2,Y,X))))))|iext(uri_owl_inverseOf,P1,P2))))),inference(shift_quantors,[status(thm)],[c14])).
% 19.51/19.72 fof(c16,plain,((![X5]:(![X6]:(~iext(uri_owl_inverseOf,X5,X6)|((ip(X5)&ip(X6))&((![X7]:(![X8]:(~iext(X5,X7,X8)|iext(X6,X8,X7))))&(![X9]:(![X10]:(~iext(X6,X10,X9)|iext(X5,X9,X10)))))))))&(![X11]:(![X12]:(((~ip(X11)|~ip(X12))|(?[X13]:(?[X14]:((~iext(X11,X13,X14)|~iext(X12,X14,X13))&(iext(X11,X13,X14)|iext(X12,X14,X13))))))|iext(uri_owl_inverseOf,X11,X12))))),inference(variable_rename,[status(thm)],[c15])).
% 19.51/19.72 fof(c18,plain,(![X5]:(![X6]:(![X7]:(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:((~iext(uri_owl_inverseOf,X5,X6)|((ip(X5)&ip(X6))&((~iext(X5,X7,X8)|iext(X6,X8,X7))&(~iext(X6,X10,X9)|iext(X5,X9,X10)))))&(((~ip(X11)|~ip(X12))|((~iext(X11,skolem0004(X11,X12),skolem0005(X11,X12))|~iext(X12,skolem0005(X11,X12),skolem0004(X11,X12)))&(iext(X11,skolem0004(X11,X12),skolem0005(X11,X12))|iext(X12,skolem0005(X11,X12),skolem0004(X11,X12)))))|iext(uri_owl_inverseOf,X11,X12))))))))))),inference(shift_quantors,[status(thm)],[fof(c17,plain,((![X5]:(![X6]:(~iext(uri_owl_inverseOf,X5,X6)|((ip(X5)&ip(X6))&((![X7]:(![X8]:(~iext(X5,X7,X8)|iext(X6,X8,X7))))&(![X9]:(![X10]:(~iext(X6,X10,X9)|iext(X5,X9,X10)))))))))&(![X11]:(![X12]:(((~ip(X11)|~ip(X12))|((~iext(X11,skolem0004(X11,X12),skolem0005(X11,X12))|~iext(X12,skolem0005(X11,X12),skolem0004(X11,X12)))&(iext(X11,skolem0004(X11,X12),skolem0005(X11,X12))|iext(X12,skolem0005(X11,X12),skolem0004(X11,X12)))))|iext(uri_owl_inverseOf,X11,X12))))),inference(skolemize,[status(esa)],[c16])).])).
% 19.51/19.72 fof(c19,plain,(![X5]:(![X6]:(![X7]:(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:((((~iext(uri_owl_inverseOf,X5,X6)|ip(X5))&(~iext(uri_owl_inverseOf,X5,X6)|ip(X6)))&((~iext(uri_owl_inverseOf,X5,X6)|(~iext(X5,X7,X8)|iext(X6,X8,X7)))&(~iext(uri_owl_inverseOf,X5,X6)|(~iext(X6,X10,X9)|iext(X5,X9,X10)))))&((((~ip(X11)|~ip(X12))|(~iext(X11,skolem0004(X11,X12),skolem0005(X11,X12))|~iext(X12,skolem0005(X11,X12),skolem0004(X11,X12))))|iext(uri_owl_inverseOf,X11,X12))&(((~ip(X11)|~ip(X12))|(iext(X11,skolem0004(X11,X12),skolem0005(X11,X12))|iext(X12,skolem0005(X11,X12),skolem0004(X11,X12))))|iext(uri_owl_inverseOf,X11,X12)))))))))))),inference(distribute,[status(thm)],[c18])).
% 19.51/19.72 cnf(c21,plain,~iext(uri_owl_inverseOf,X65,X66)|ip(X66),inference(split_conjunct,[status(thm)],[c19])).
% 19.51/19.72 cnf(c71,plain,ip(uri_ex_p),inference(resolution,[status(thm)],[c21, c10])).
% 19.51/19.72 fof(owl_char_inversefunctional,axiom,(![P]:(icext(uri_owl_InverseFunctionalProperty,P)<=>(ip(P)&(![X1]:(![X2]:(![Y]:((iext(P,X1,Y)&iext(P,X2,Y))=>X1=X2))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', owl_char_inversefunctional)).
% 19.51/19.72 fof(c26,plain,(![P]:((~icext(uri_owl_InverseFunctionalProperty,P)|(ip(P)&(![X1]:(![X2]:(![Y]:((~iext(P,X1,Y)|~iext(P,X2,Y))|X1=X2))))))&((~ip(P)|(?[X1]:(?[X2]:(?[Y]:((iext(P,X1,Y)&iext(P,X2,Y))&X1!=X2)))))|icext(uri_owl_InverseFunctionalProperty,P)))),inference(fof_nnf,[status(thm)],[owl_char_inversefunctional])).
% 19.51/19.72 fof(c27,plain,((![P]:(~icext(uri_owl_InverseFunctionalProperty,P)|(ip(P)&(![X1]:(![X2]:((![Y]:(~iext(P,X1,Y)|~iext(P,X2,Y)))|X1=X2))))))&(![P]:((~ip(P)|(?[X1]:(?[X2]:((?[Y]:(iext(P,X1,Y)&iext(P,X2,Y)))&X1!=X2))))|icext(uri_owl_InverseFunctionalProperty,P)))),inference(shift_quantors,[status(thm)],[c26])).
% 19.51/19.72 fof(c28,plain,((![X15]:(~icext(uri_owl_InverseFunctionalProperty,X15)|(ip(X15)&(![X16]:(![X17]:((![X18]:(~iext(X15,X16,X18)|~iext(X15,X17,X18)))|X16=X17))))))&(![X19]:((~ip(X19)|(?[X20]:(?[X21]:((?[X22]:(iext(X19,X20,X22)&iext(X19,X21,X22)))&X20!=X21))))|icext(uri_owl_InverseFunctionalProperty,X19)))),inference(variable_rename,[status(thm)],[c27])).
% 19.51/19.72 fof(c30,plain,(![X15]:(![X16]:(![X17]:(![X18]:(![X19]:((~icext(uri_owl_InverseFunctionalProperty,X15)|(ip(X15)&((~iext(X15,X16,X18)|~iext(X15,X17,X18))|X16=X17)))&((~ip(X19)|((iext(X19,skolem0006(X19),skolem0008(X19))&iext(X19,skolem0007(X19),skolem0008(X19)))&skolem0006(X19)!=skolem0007(X19)))|icext(uri_owl_InverseFunctionalProperty,X19)))))))),inference(shift_quantors,[status(thm)],[fof(c29,plain,((![X15]:(~icext(uri_owl_InverseFunctionalProperty,X15)|(ip(X15)&(![X16]:(![X17]:((![X18]:(~iext(X15,X16,X18)|~iext(X15,X17,X18)))|X16=X17))))))&(![X19]:((~ip(X19)|((iext(X19,skolem0006(X19),skolem0008(X19))&iext(X19,skolem0007(X19),skolem0008(X19)))&skolem0006(X19)!=skolem0007(X19)))|icext(uri_owl_InverseFunctionalProperty,X19)))),inference(skolemize,[status(esa)],[c28])).])).
% 19.51/19.72 fof(c31,plain,(![X15]:(![X16]:(![X17]:(![X18]:(![X19]:(((~icext(uri_owl_InverseFunctionalProperty,X15)|ip(X15))&(~icext(uri_owl_InverseFunctionalProperty,X15)|((~iext(X15,X16,X18)|~iext(X15,X17,X18))|X16=X17)))&((((~ip(X19)|iext(X19,skolem0006(X19),skolem0008(X19)))|icext(uri_owl_InverseFunctionalProperty,X19))&((~ip(X19)|iext(X19,skolem0007(X19),skolem0008(X19)))|icext(uri_owl_InverseFunctionalProperty,X19)))&((~ip(X19)|skolem0006(X19)!=skolem0007(X19))|icext(uri_owl_InverseFunctionalProperty,X19))))))))),inference(distribute,[status(thm)],[c30])).
% 19.51/19.72 cnf(c36,plain,~ip(X117)|skolem0006(X117)!=skolem0007(X117)|icext(uri_owl_InverseFunctionalProperty,X117),inference(split_conjunct,[status(thm)],[c31])).
% 19.51/19.72 cnf(symmetry,axiom,X43!=X44|X44=X43,theory(equality)).
% 19.51/19.72 fof(owl_eqdis_sameas,axiom,(![X]:(![Y]:(iext(uri_owl_sameAs,X,Y)<=>X=Y))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', owl_eqdis_sameas)).
% 19.51/19.72 fof(c49,plain,(![X]:(![Y]:((~iext(uri_owl_sameAs,X,Y)|X=Y)&(X!=Y|iext(uri_owl_sameAs,X,Y))))),inference(fof_nnf,[status(thm)],[owl_eqdis_sameas])).
% 19.51/19.72 fof(c50,plain,((![X]:(![Y]:(~iext(uri_owl_sameAs,X,Y)|X=Y)))&(![X]:(![Y]:(X!=Y|iext(uri_owl_sameAs,X,Y))))),inference(shift_quantors,[status(thm)],[c49])).
% 19.51/19.72 fof(c52,plain,(![X34]:(![X35]:(![X36]:(![X37]:((~iext(uri_owl_sameAs,X34,X35)|X34=X35)&(X36!=X37|iext(uri_owl_sameAs,X36,X37))))))),inference(shift_quantors,[status(thm)],[fof(c51,plain,((![X34]:(![X35]:(~iext(uri_owl_sameAs,X34,X35)|X34=X35)))&(![X36]:(![X37]:(X36!=X37|iext(uri_owl_sameAs,X36,X37))))),inference(variable_rename,[status(thm)],[c50])).])).
% 19.51/19.72 cnf(c53,plain,~iext(uri_owl_sameAs,X70,X71)|X70=X71,inference(split_conjunct,[status(thm)],[c52])).
% 19.51/19.72 cnf(c6,plain,iext(uri_rdf_first,skolem0001,uri_ex_p),inference(split_conjunct,[status(thm)],[c4])).
% 19.51/19.72 cnf(c7,plain,iext(uri_rdf_rest,skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c4])).
% 19.51/19.72 cnf(c8,plain,iext(uri_rdf_first,skolem0002,skolem0003),inference(split_conjunct,[status(thm)],[c4])).
% 19.51/19.72 cnf(c9,plain,iext(uri_rdf_rest,skolem0002,uri_rdf_nil),inference(split_conjunct,[status(thm)],[c4])).
% 19.51/19.72 cnf(c5,plain,iext(uri_owl_propertyChainAxiom,uri_owl_sameAs,skolem0001),inference(split_conjunct,[status(thm)],[c4])).
% 19.51/19.72 cnf(c35,plain,~ip(X121)|iext(X121,skolem0007(X121),skolem0008(X121))|icext(uri_owl_InverseFunctionalProperty,X121),inference(split_conjunct,[status(thm)],[c31])).
% 19.51/19.72 cnf(c105,plain,iext(uri_ex_p,skolem0007(uri_ex_p),skolem0008(uri_ex_p))|icext(uri_owl_InverseFunctionalProperty,uri_ex_p),inference(resolution,[status(thm)],[c35, c71])).
% 19.51/19.72 cnf(c168,plain,iext(uri_ex_p,skolem0007(uri_ex_p),skolem0008(uri_ex_p))|iext(uri_rdf_type,uri_ex_p,uri_owl_InverseFunctionalProperty),inference(resolution,[status(thm)],[c105, c60])).
% 19.51/19.72 cnf(c242,plain,iext(uri_ex_p,skolem0007(uri_ex_p),skolem0008(uri_ex_p)),inference(resolution,[status(thm)],[c168, c13])).
% 19.51/19.72 fof(owl_chain_002,axiom,(![P]:(![S1]:(![P1]:(![S2]:(![P2]:((((iext(uri_rdf_first,S1,P1)&iext(uri_rdf_rest,S1,S2))&iext(uri_rdf_first,S2,P2))&iext(uri_rdf_rest,S2,uri_rdf_nil))=>(iext(uri_owl_propertyChainAxiom,P,S1)<=>(((ip(P)&ip(P1))&ip(P2))&(![Y0]:(![Y1]:(![Y2]:((iext(P1,Y0,Y1)&iext(P2,Y1,Y2))=>iext(P,Y0,Y2))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', owl_chain_002)).
% 19.51/19.72 fof(c37,plain,(![P]:(![S1]:(![P1]:(![S2]:(![P2]:((((~iext(uri_rdf_first,S1,P1)|~iext(uri_rdf_rest,S1,S2))|~iext(uri_rdf_first,S2,P2))|~iext(uri_rdf_rest,S2,uri_rdf_nil))|((~iext(uri_owl_propertyChainAxiom,P,S1)|(((ip(P)&ip(P1))&ip(P2))&(![Y0]:(![Y1]:(![Y2]:((~iext(P1,Y0,Y1)|~iext(P2,Y1,Y2))|iext(P,Y0,Y2)))))))&((((~ip(P)|~ip(P1))|~ip(P2))|(?[Y0]:(?[Y1]:(?[Y2]:((iext(P1,Y0,Y1)&iext(P2,Y1,Y2))&~iext(P,Y0,Y2))))))|iext(uri_owl_propertyChainAxiom,P,S1))))))))),inference(fof_nnf,[status(thm)],[owl_chain_002])).
% 19.51/19.72 fof(c38,plain,(![X23]:(![X24]:(![X25]:(![X26]:(![X27]:((((~iext(uri_rdf_first,X24,X25)|~iext(uri_rdf_rest,X24,X26))|~iext(uri_rdf_first,X26,X27))|~iext(uri_rdf_rest,X26,uri_rdf_nil))|((~iext(uri_owl_propertyChainAxiom,X23,X24)|(((ip(X23)&ip(X25))&ip(X27))&(![X28]:(![X29]:(![X30]:((~iext(X25,X28,X29)|~iext(X27,X29,X30))|iext(X23,X28,X30)))))))&((((~ip(X23)|~ip(X25))|~ip(X27))|(?[X31]:(?[X32]:(?[X33]:((iext(X25,X31,X32)&iext(X27,X32,X33))&~iext(X23,X31,X33))))))|iext(uri_owl_propertyChainAxiom,X23,X24))))))))),inference(variable_rename,[status(thm)],[c37])).
% 19.51/19.72 fof(c40,plain,(![X23]:(![X24]:(![X25]:(![X26]:(![X27]:(![X28]:(![X29]:(![X30]:((((~iext(uri_rdf_first,X24,X25)|~iext(uri_rdf_rest,X24,X26))|~iext(uri_rdf_first,X26,X27))|~iext(uri_rdf_rest,X26,uri_rdf_nil))|((~iext(uri_owl_propertyChainAxiom,X23,X24)|(((ip(X23)&ip(X25))&ip(X27))&((~iext(X25,X28,X29)|~iext(X27,X29,X30))|iext(X23,X28,X30))))&((((~ip(X23)|~ip(X25))|~ip(X27))|((iext(X25,skolem0009(X23,X24,X25,X26,X27),skolem0010(X23,X24,X25,X26,X27))&iext(X27,skolem0010(X23,X24,X25,X26,X27),skolem0011(X23,X24,X25,X26,X27)))&~iext(X23,skolem0009(X23,X24,X25,X26,X27),skolem0011(X23,X24,X25,X26,X27))))|iext(uri_owl_propertyChainAxiom,X23,X24)))))))))))),inference(shift_quantors,[status(thm)],[fof(c39,plain,(![X23]:(![X24]:(![X25]:(![X26]:(![X27]:((((~iext(uri_rdf_first,X24,X25)|~iext(uri_rdf_rest,X24,X26))|~iext(uri_rdf_first,X26,X27))|~iext(uri_rdf_rest,X26,uri_rdf_nil))|((~iext(uri_owl_propertyChainAxiom,X23,X24)|(((ip(X23)&ip(X25))&ip(X27))&(![X28]:(![X29]:(![X30]:((~iext(X25,X28,X29)|~iext(X27,X29,X30))|iext(X23,X28,X30)))))))&((((~ip(X23)|~ip(X25))|~ip(X27))|((iext(X25,skolem0009(X23,X24,X25,X26,X27),skolem0010(X23,X24,X25,X26,X27))&iext(X27,skolem0010(X23,X24,X25,X26,X27),skolem0011(X23,X24,X25,X26,X27)))&~iext(X23,skolem0009(X23,X24,X25,X26,X27),skolem0011(X23,X24,X25,X26,X27))))|iext(uri_owl_propertyChainAxiom,X23,X24))))))))),inference(skolemize,[status(esa)],[c38])).])).
% 19.51/19.72 fof(c41,plain,(![X23]:(![X24]:(![X25]:(![X26]:(![X27]:(![X28]:(![X29]:(![X30]:((((((((~iext(uri_rdf_first,X24,X25)|~iext(uri_rdf_rest,X24,X26))|~iext(uri_rdf_first,X26,X27))|~iext(uri_rdf_rest,X26,uri_rdf_nil))|(~iext(uri_owl_propertyChainAxiom,X23,X24)|ip(X23)))&((((~iext(uri_rdf_first,X24,X25)|~iext(uri_rdf_rest,X24,X26))|~iext(uri_rdf_first,X26,X27))|~iext(uri_rdf_rest,X26,uri_rdf_nil))|(~iext(uri_owl_propertyChainAxiom,X23,X24)|ip(X25))))&((((~iext(uri_rdf_first,X24,X25)|~iext(uri_rdf_rest,X24,X26))|~iext(uri_rdf_first,X26,X27))|~iext(uri_rdf_rest,X26,uri_rdf_nil))|(~iext(uri_owl_propertyChainAxiom,X23,X24)|ip(X27))))&((((~iext(uri_rdf_first,X24,X25)|~iext(uri_rdf_rest,X24,X26))|~iext(uri_rdf_first,X26,X27))|~iext(uri_rdf_rest,X26,uri_rdf_nil))|(~iext(uri_owl_propertyChainAxiom,X23,X24)|((~iext(X25,X28,X29)|~iext(X27,X29,X30))|iext(X23,X28,X30)))))&((((((~iext(uri_rdf_first,X24,X25)|~iext(uri_rdf_rest,X24,X26))|~iext(uri_rdf_first,X26,X27))|~iext(uri_rdf_rest,X26,uri_rdf_nil))|((((~ip(X23)|~ip(X25))|~ip(X27))|iext(X25,skolem0009(X23,X24,X25,X26,X27),skolem0010(X23,X24,X25,X26,X27)))|iext(uri_owl_propertyChainAxiom,X23,X24)))&((((~iext(uri_rdf_first,X24,X25)|~iext(uri_rdf_rest,X24,X26))|~iext(uri_rdf_first,X26,X27))|~iext(uri_rdf_rest,X26,uri_rdf_nil))|((((~ip(X23)|~ip(X25))|~ip(X27))|iext(X27,skolem0010(X23,X24,X25,X26,X27),skolem0011(X23,X24,X25,X26,X27)))|iext(uri_owl_propertyChainAxiom,X23,X24))))&((((~iext(uri_rdf_first,X24,X25)|~iext(uri_rdf_rest,X24,X26))|~iext(uri_rdf_first,X26,X27))|~iext(uri_rdf_rest,X26,uri_rdf_nil))|((((~ip(X23)|~ip(X25))|~ip(X27))|~iext(X23,skolem0009(X23,X24,X25,X26,X27),skolem0011(X23,X24,X25,X26,X27)))|iext(uri_owl_propertyChainAxiom,X23,X24))))))))))))),inference(distribute,[status(thm)],[c40])).
% 19.51/19.72 cnf(c45,plain,~iext(uri_rdf_first,X165,X168)|~iext(uri_rdf_rest,X165,X164)|~iext(uri_rdf_first,X164,X167)|~iext(uri_rdf_rest,X164,uri_rdf_nil)|~iext(uri_owl_propertyChainAxiom,X166,X165)|~iext(X168,X161,X163)|~iext(X167,X163,X162)|iext(X166,X161,X162),inference(split_conjunct,[status(thm)],[c41])).
% 19.51/19.72 cnf(c23,plain,~iext(uri_owl_inverseOf,X84,X86)|~iext(X86,X87,X85)|iext(X84,X85,X87),inference(split_conjunct,[status(thm)],[c19])).
% 19.51/19.72 cnf(c34,plain,~ip(X120)|iext(X120,skolem0006(X120),skolem0008(X120))|icext(uri_owl_InverseFunctionalProperty,X120),inference(split_conjunct,[status(thm)],[c31])).
% 19.51/19.72 cnf(c103,plain,iext(uri_ex_p,skolem0006(uri_ex_p),skolem0008(uri_ex_p))|icext(uri_owl_InverseFunctionalProperty,uri_ex_p),inference(resolution,[status(thm)],[c34, c71])).
% 19.51/19.72 cnf(c150,plain,iext(uri_ex_p,skolem0006(uri_ex_p),skolem0008(uri_ex_p))|iext(uri_rdf_type,uri_ex_p,uri_owl_InverseFunctionalProperty),inference(resolution,[status(thm)],[c103, c60])).
% 19.51/19.72 cnf(c203,plain,iext(uri_ex_p,skolem0006(uri_ex_p),skolem0008(uri_ex_p)),inference(resolution,[status(thm)],[c150, c13])).
% 19.51/19.72 cnf(c211,plain,~iext(uri_owl_inverseOf,X225,uri_ex_p)|iext(X225,skolem0008(uri_ex_p),skolem0006(uri_ex_p)),inference(resolution,[status(thm)],[c203, c23])).
% 19.51/19.72 cnf(c215,plain,iext(skolem0003,skolem0008(uri_ex_p),skolem0006(uri_ex_p)),inference(resolution,[status(thm)],[c211, c10])).
% 19.51/19.72 cnf(c222,plain,~iext(uri_rdf_first,X518,X519)|~iext(uri_rdf_rest,X518,X516)|~iext(uri_rdf_first,X516,skolem0003)|~iext(uri_rdf_rest,X516,uri_rdf_nil)|~iext(uri_owl_propertyChainAxiom,X517,X518)|~iext(X519,X515,skolem0008(uri_ex_p))|iext(X517,X515,skolem0006(uri_ex_p)),inference(resolution,[status(thm)],[c215, c45])).
% 19.51/19.72 cnf(c928,plain,~iext(uri_rdf_first,X2493,uri_ex_p)|~iext(uri_rdf_rest,X2493,X2492)|~iext(uri_rdf_first,X2492,skolem0003)|~iext(uri_rdf_rest,X2492,uri_rdf_nil)|~iext(uri_owl_propertyChainAxiom,X2494,X2493)|iext(X2494,skolem0007(uri_ex_p),skolem0006(uri_ex_p)),inference(resolution,[status(thm)],[c222, c242])).
% 19.51/19.72 cnf(c11333,plain,~iext(uri_rdf_first,skolem0001,uri_ex_p)|~iext(uri_rdf_rest,skolem0001,X2495)|~iext(uri_rdf_first,X2495,skolem0003)|~iext(uri_rdf_rest,X2495,uri_rdf_nil)|iext(uri_owl_sameAs,skolem0007(uri_ex_p),skolem0006(uri_ex_p)),inference(resolution,[status(thm)],[c928, c5])).
% 19.51/19.72 cnf(c11334,plain,~iext(uri_rdf_first,skolem0001,uri_ex_p)|~iext(uri_rdf_rest,skolem0001,skolem0002)|~iext(uri_rdf_first,skolem0002,skolem0003)|iext(uri_owl_sameAs,skolem0007(uri_ex_p),skolem0006(uri_ex_p)),inference(resolution,[status(thm)],[c11333, c9])).
% 19.51/19.72 cnf(c11335,plain,~iext(uri_rdf_first,skolem0001,uri_ex_p)|~iext(uri_rdf_rest,skolem0001,skolem0002)|iext(uri_owl_sameAs,skolem0007(uri_ex_p),skolem0006(uri_ex_p)),inference(resolution,[status(thm)],[c11334, c8])).
% 19.51/19.72 cnf(c11336,plain,~iext(uri_rdf_first,skolem0001,uri_ex_p)|iext(uri_owl_sameAs,skolem0007(uri_ex_p),skolem0006(uri_ex_p)),inference(resolution,[status(thm)],[c11335, c7])).
% 19.51/19.72 cnf(c11337,plain,iext(uri_owl_sameAs,skolem0007(uri_ex_p),skolem0006(uri_ex_p)),inference(resolution,[status(thm)],[c11336, c6])).
% 19.51/19.72 cnf(c11350,plain,skolem0007(uri_ex_p)=skolem0006(uri_ex_p),inference(resolution,[status(thm)],[c11337, c53])).
% 19.51/19.72 cnf(c11358,plain,skolem0006(uri_ex_p)=skolem0007(uri_ex_p),inference(resolution,[status(thm)],[c11350, symmetry])).
% 19.51/19.72 cnf(c11441,plain,~ip(uri_ex_p)|icext(uri_owl_InverseFunctionalProperty,uri_ex_p),inference(resolution,[status(thm)],[c11358, c36])).
% 19.51/19.72 cnf(c11444,plain,icext(uri_owl_InverseFunctionalProperty,uri_ex_p),inference(resolution,[status(thm)],[c11441, c71])).
% 19.51/19.72 cnf(c11445,plain,iext(uri_rdf_type,uri_ex_p,uri_owl_InverseFunctionalProperty),inference(resolution,[status(thm)],[c11444, c60])).
% 19.51/19.72 cnf(c11464,plain,$false,inference(resolution,[status(thm)],[c11445, c13])).
% 19.51/19.72 % SZS output end CNFRefutation
% 19.51/19.72
% 19.51/19.72 % Initial clauses : 35
% 19.51/19.72 % Processed clauses : 1207
% 19.51/19.72 % Factors computed : 128
% 19.51/19.72 % Resolvents computed: 11322
% 19.51/19.72 % Tautologies deleted: 13
% 19.51/19.72 % Forward subsumed : 934
% 19.51/19.72 % Backward subsumed : 96
% 19.51/19.72 % -------- CPU Time ---------
% 19.51/19.72 % User time : 19.298 s
% 19.51/19.72 % System time : 0.051 s
% 19.51/19.72 % Total time : 19.349 s
%------------------------------------------------------------------------------