%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SWB026+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 0.62s 0.86s
% Output : Refutation 0.62s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SWB026+2 : TPTP v8.1.2. Released v5.2.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n012.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Wed May 8 22:04:38 EDT 2024
% 0.13/0.35 % CPUTime :
% 0.62/0.86 % Version: 1.5
% 0.62/0.86 % SZS status Theorem
% 0.62/0.86 % SZS output start CNFRefutation
% 0.62/0.86 fof(testcase_conclusion_fullish_026_Inferred_Property_Characteristics_I,conjecture,iext(uri_rdf_type,uri_ex_p,uri_owl_InverseFunctionalProperty),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', testcase_conclusion_fullish_026_Inferred_Property_Characteristics_I)).
% 0.62/0.86 fof(c14,negated_conjecture,(~iext(uri_rdf_type,uri_ex_p,uri_owl_InverseFunctionalProperty)),inference(assume_negation,[status(cth)],[testcase_conclusion_fullish_026_Inferred_Property_Characteristics_I])).
% 0.62/0.86 fof(c15,negated_conjecture,~iext(uri_rdf_type,uri_ex_p,uri_owl_InverseFunctionalProperty),inference(fof_simplification,[status(thm)],[c14])).
% 0.62/0.86 cnf(c16,negated_conjecture,~iext(uri_rdf_type,uri_ex_p,uri_owl_InverseFunctionalProperty),inference(split_conjunct,[status(thm)],[c15])).
% 0.62/0.86 fof(rdfs_cext_def,axiom,(![X]:(![C]:(iext(uri_rdf_type,X,C)<=>icext(C,X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', rdfs_cext_def)).
% 0.62/0.86 fof(c45,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])).
% 0.62/0.86 fof(c46,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)],[c45])).
% 0.62/0.86 fof(c48,plain,(![X24]:(![X25]:(![X26]:(![X27]:((~iext(uri_rdf_type,X24,X25)|icext(X25,X24))&(~icext(X27,X26)|iext(uri_rdf_type,X26,X27))))))),inference(shift_quantors,[status(thm)],[fof(c47,plain,((![X24]:(![X25]:(~iext(uri_rdf_type,X24,X25)|icext(X25,X24))))&(![X26]:(![X27]:(~icext(X27,X26)|iext(uri_rdf_type,X26,X27))))),inference(variable_rename,[status(thm)],[c46])).])).
% 0.62/0.86 cnf(c50,plain,~icext(X60,X59)|iext(uri_rdf_type,X59,X60),inference(split_conjunct,[status(thm)],[c48])).
% 0.62/0.86 fof(rdf_type_ip,axiom,(![P]:(iext(uri_rdf_type,P,uri_rdf_Property)<=>ip(P))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', rdf_type_ip)).
% 0.62/0.86 fof(c51,plain,(![P]:((~iext(uri_rdf_type,P,uri_rdf_Property)|ip(P))&(~ip(P)|iext(uri_rdf_type,P,uri_rdf_Property)))),inference(fof_nnf,[status(thm)],[rdf_type_ip])).
% 0.62/0.86 fof(c52,plain,((![P]:(~iext(uri_rdf_type,P,uri_rdf_Property)|ip(P)))&(![P]:(~ip(P)|iext(uri_rdf_type,P,uri_rdf_Property)))),inference(shift_quantors,[status(thm)],[c51])).
% 0.62/0.86 fof(c54,plain,(![X28]:(![X29]:((~iext(uri_rdf_type,X28,uri_rdf_Property)|ip(X28))&(~ip(X29)|iext(uri_rdf_type,X29,uri_rdf_Property))))),inference(shift_quantors,[status(thm)],[fof(c53,plain,((![X28]:(~iext(uri_rdf_type,X28,uri_rdf_Property)|ip(X28)))&(![X29]:(~ip(X29)|iext(uri_rdf_type,X29,uri_rdf_Property)))),inference(variable_rename,[status(thm)],[c52])).])).
% 0.62/0.86 cnf(c55,plain,~iext(uri_rdf_type,X61,uri_rdf_Property)|ip(X61),inference(split_conjunct,[status(thm)],[c54])).
% 0.62/0.86 fof(rdfs_domain_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', rdfs_domain_domain)).
% 0.62/0.86 cnf(c39,plain,iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_domain_domain])).
% 0.62/0.86 fof(testcase_premise_fullish_026_Inferred_Property_Characteristics_I,axiom,(?[BNODE_x1]:(?[BNODE_x2]:(?[BNODE_l1]:(?[BNODE_l2]:(((((((iext(uri_rdfs_domain,uri_ex_p,BNODE_x1)&iext(uri_owl_oneOf,BNODE_x1,BNODE_l1))&iext(uri_rdf_first,BNODE_l1,uri_ex_w))&iext(uri_rdf_rest,BNODE_l1,uri_rdf_nil))&iext(uri_rdfs_range,uri_ex_p,BNODE_x2))&iext(uri_owl_oneOf,BNODE_x2,BNODE_l2))&iext(uri_rdf_first,BNODE_l2,uri_ex_u))&iext(uri_rdf_rest,BNODE_l2,uri_rdf_nil)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', testcase_premise_fullish_026_Inferred_Property_Characteristics_I)).
% 0.62/0.86 fof(c4,plain,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(((((((iext(uri_rdfs_domain,uri_ex_p,X2)&iext(uri_owl_oneOf,X2,X4))&iext(uri_rdf_first,X4,uri_ex_w))&iext(uri_rdf_rest,X4,uri_rdf_nil))&iext(uri_rdfs_range,uri_ex_p,X3))&iext(uri_owl_oneOf,X3,X5))&iext(uri_rdf_first,X5,uri_ex_u))&iext(uri_rdf_rest,X5,uri_rdf_nil)))))),inference(variable_rename,[status(thm)],[testcase_premise_fullish_026_Inferred_Property_Characteristics_I])).
% 0.62/0.86 fof(c5,plain,(((((((iext(uri_rdfs_domain,uri_ex_p,skolem0001)&iext(uri_owl_oneOf,skolem0001,skolem0003))&iext(uri_rdf_first,skolem0003,uri_ex_w))&iext(uri_rdf_rest,skolem0003,uri_rdf_nil))&iext(uri_rdfs_range,uri_ex_p,skolem0002))&iext(uri_owl_oneOf,skolem0002,skolem0004))&iext(uri_rdf_first,skolem0004,uri_ex_u))&iext(uri_rdf_rest,skolem0004,uri_rdf_nil)),inference(skolemize,[status(esa)],[c4])).
% 0.62/0.86 cnf(c6,plain,iext(uri_rdfs_domain,uri_ex_p,skolem0001),inference(split_conjunct,[status(thm)],[c5])).
% 0.62/0.86 fof(rdfs_domain_main,axiom,(![P]:(![C]:(![X]:(![Y]:((iext(uri_rdfs_domain,P,C)&iext(P,X,Y))=>icext(C,X)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', rdfs_domain_main)).
% 0.62/0.86 fof(c40,plain,(![P]:(![C]:(![X]:(![Y]:((~iext(uri_rdfs_domain,P,C)|~iext(P,X,Y))|icext(C,X)))))),inference(fof_nnf,[status(thm)],[rdfs_domain_main])).
% 0.62/0.86 fof(c41,plain,(![P]:(![C]:(![X]:((~iext(uri_rdfs_domain,P,C)|(![Y]:~iext(P,X,Y)))|icext(C,X))))),inference(shift_quantors,[status(thm)],[c40])).
% 0.62/0.86 fof(c43,plain,(![X20]:(![X21]:(![X22]:(![X23]:((~iext(uri_rdfs_domain,X20,X21)|~iext(X20,X22,X23))|icext(X21,X22)))))),inference(shift_quantors,[status(thm)],[fof(c42,plain,(![X20]:(![X21]:(![X22]:((~iext(uri_rdfs_domain,X20,X21)|(![X23]:~iext(X20,X22,X23)))|icext(X21,X22))))),inference(variable_rename,[status(thm)],[c41])).])).
% 0.62/0.86 cnf(c44,plain,~iext(uri_rdfs_domain,X65,X64)|~iext(X65,X63,X66)|icext(X64,X63),inference(split_conjunct,[status(thm)],[c43])).
% 0.62/0.86 cnf(c77,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X79)|icext(X79,uri_ex_p),inference(resolution,[status(thm)],[c44, c6])).
% 0.62/0.86 cnf(c102,plain,icext(uri_rdf_Property,uri_ex_p),inference(resolution,[status(thm)],[c77, c39])).
% 0.62/0.86 cnf(c103,plain,iext(uri_rdf_type,uri_ex_p,uri_rdf_Property),inference(resolution,[status(thm)],[c102, c50])).
% 0.62/0.86 cnf(c105,plain,ip(uri_ex_p),inference(resolution,[status(thm)],[c103, c55])).
% 0.62/0.86 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/sandbox2/benchmark/theBenchmark.p', owl_char_inversefunctional)).
% 0.62/0.86 fof(c17,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])).
% 0.62/0.86 fof(c18,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)],[c17])).
% 0.62/0.86 fof(c19,plain,((![X6]:(~icext(uri_owl_InverseFunctionalProperty,X6)|(ip(X6)&(![X7]:(![X8]:((![X9]:(~iext(X6,X7,X9)|~iext(X6,X8,X9)))|X7=X8))))))&(![X10]:((~ip(X10)|(?[X11]:(?[X12]:((?[X13]:(iext(X10,X11,X13)&iext(X10,X12,X13)))&X11!=X12))))|icext(uri_owl_InverseFunctionalProperty,X10)))),inference(variable_rename,[status(thm)],[c18])).
% 0.62/0.86 fof(c21,plain,(![X6]:(![X7]:(![X8]:(![X9]:(![X10]:((~icext(uri_owl_InverseFunctionalProperty,X6)|(ip(X6)&((~iext(X6,X7,X9)|~iext(X6,X8,X9))|X7=X8)))&((~ip(X10)|((iext(X10,skolem0005(X10),skolem0007(X10))&iext(X10,skolem0006(X10),skolem0007(X10)))&skolem0005(X10)!=skolem0006(X10)))|icext(uri_owl_InverseFunctionalProperty,X10)))))))),inference(shift_quantors,[status(thm)],[fof(c20,plain,((![X6]:(~icext(uri_owl_InverseFunctionalProperty,X6)|(ip(X6)&(![X7]:(![X8]:((![X9]:(~iext(X6,X7,X9)|~iext(X6,X8,X9)))|X7=X8))))))&(![X10]:((~ip(X10)|((iext(X10,skolem0005(X10),skolem0007(X10))&iext(X10,skolem0006(X10),skolem0007(X10)))&skolem0005(X10)!=skolem0006(X10)))|icext(uri_owl_InverseFunctionalProperty,X10)))),inference(skolemize,[status(esa)],[c19])).])).
% 0.62/0.86 fof(c22,plain,(![X6]:(![X7]:(![X8]:(![X9]:(![X10]:(((~icext(uri_owl_InverseFunctionalProperty,X6)|ip(X6))&(~icext(uri_owl_InverseFunctionalProperty,X6)|((~iext(X6,X7,X9)|~iext(X6,X8,X9))|X7=X8)))&((((~ip(X10)|iext(X10,skolem0005(X10),skolem0007(X10)))|icext(uri_owl_InverseFunctionalProperty,X10))&((~ip(X10)|iext(X10,skolem0006(X10),skolem0007(X10)))|icext(uri_owl_InverseFunctionalProperty,X10)))&((~ip(X10)|skolem0005(X10)!=skolem0006(X10))|icext(uri_owl_InverseFunctionalProperty,X10))))))))),inference(distribute,[status(thm)],[c21])).
% 0.62/0.86 cnf(c27,plain,~ip(X80)|skolem0005(X80)!=skolem0006(X80)|icext(uri_owl_InverseFunctionalProperty,X80),inference(split_conjunct,[status(thm)],[c22])).
% 0.62/0.86 cnf(symmetry,axiom,X32!=X31|X31=X32,theory(equality)).
% 0.62/0.86 cnf(transitivity,axiom,X36!=X35|X35!=X34|X36=X34,theory(equality)).
% 0.62/0.86 cnf(c8,plain,iext(uri_rdf_first,skolem0003,uri_ex_w),inference(split_conjunct,[status(thm)],[c5])).
% 0.62/0.86 cnf(c9,plain,iext(uri_rdf_rest,skolem0003,uri_rdf_nil),inference(split_conjunct,[status(thm)],[c5])).
% 0.62/0.86 cnf(c7,plain,iext(uri_owl_oneOf,skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c5])).
% 0.62/0.86 fof(owl_enum_class_001,axiom,(![Z]:(![S1]:(![A1]:((iext(uri_rdf_first,S1,A1)&iext(uri_rdf_rest,S1,uri_rdf_nil))=>(iext(uri_owl_oneOf,Z,S1)<=>(ic(Z)&(![X]:(icext(Z,X)<=>X=A1)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', owl_enum_class_001)).
% 0.62/0.86 fof(c28,plain,(![Z]:(![S1]:(![A1]:((~iext(uri_rdf_first,S1,A1)|~iext(uri_rdf_rest,S1,uri_rdf_nil))|((~iext(uri_owl_oneOf,Z,S1)|(ic(Z)&(![X]:((~icext(Z,X)|X=A1)&(X!=A1|icext(Z,X))))))&((~ic(Z)|(?[X]:((~icext(Z,X)|X!=A1)&(icext(Z,X)|X=A1))))|iext(uri_owl_oneOf,Z,S1))))))),inference(fof_nnf,[status(thm)],[owl_enum_class_001])).
% 0.62/0.86 fof(c29,plain,(![Z]:(![S1]:(![A1]:((~iext(uri_rdf_first,S1,A1)|~iext(uri_rdf_rest,S1,uri_rdf_nil))|((~iext(uri_owl_oneOf,Z,S1)|(ic(Z)&((![X]:(~icext(Z,X)|X=A1))&(![X]:(X!=A1|icext(Z,X))))))&((~ic(Z)|(?[X]:((~icext(Z,X)|X!=A1)&(icext(Z,X)|X=A1))))|iext(uri_owl_oneOf,Z,S1))))))),inference(shift_quantors,[status(thm)],[c28])).
% 0.62/0.86 fof(c30,plain,(![X14]:(![X15]:(![X16]:((~iext(uri_rdf_first,X15,X16)|~iext(uri_rdf_rest,X15,uri_rdf_nil))|((~iext(uri_owl_oneOf,X14,X15)|(ic(X14)&((![X17]:(~icext(X14,X17)|X17=X16))&(![X18]:(X18!=X16|icext(X14,X18))))))&((~ic(X14)|(?[X19]:((~icext(X14,X19)|X19!=X16)&(icext(X14,X19)|X19=X16))))|iext(uri_owl_oneOf,X14,X15))))))),inference(variable_rename,[status(thm)],[c29])).
% 0.62/0.86 fof(c32,plain,(![X14]:(![X15]:(![X16]:(![X17]:(![X18]:((~iext(uri_rdf_first,X15,X16)|~iext(uri_rdf_rest,X15,uri_rdf_nil))|((~iext(uri_owl_oneOf,X14,X15)|(ic(X14)&((~icext(X14,X17)|X17=X16)&(X18!=X16|icext(X14,X18)))))&((~ic(X14)|((~icext(X14,skolem0008(X14,X15,X16))|skolem0008(X14,X15,X16)!=X16)&(icext(X14,skolem0008(X14,X15,X16))|skolem0008(X14,X15,X16)=X16)))|iext(uri_owl_oneOf,X14,X15))))))))),inference(shift_quantors,[status(thm)],[fof(c31,plain,(![X14]:(![X15]:(![X16]:((~iext(uri_rdf_first,X15,X16)|~iext(uri_rdf_rest,X15,uri_rdf_nil))|((~iext(uri_owl_oneOf,X14,X15)|(ic(X14)&((![X17]:(~icext(X14,X17)|X17=X16))&(![X18]:(X18!=X16|icext(X14,X18))))))&((~ic(X14)|((~icext(X14,skolem0008(X14,X15,X16))|skolem0008(X14,X15,X16)!=X16)&(icext(X14,skolem0008(X14,X15,X16))|skolem0008(X14,X15,X16)=X16)))|iext(uri_owl_oneOf,X14,X15))))))),inference(skolemize,[status(esa)],[c30])).])).
% 0.62/0.86 fof(c33,plain,(![X14]:(![X15]:(![X16]:(![X17]:(![X18]:((((~iext(uri_rdf_first,X15,X16)|~iext(uri_rdf_rest,X15,uri_rdf_nil))|(~iext(uri_owl_oneOf,X14,X15)|ic(X14)))&(((~iext(uri_rdf_first,X15,X16)|~iext(uri_rdf_rest,X15,uri_rdf_nil))|(~iext(uri_owl_oneOf,X14,X15)|(~icext(X14,X17)|X17=X16)))&((~iext(uri_rdf_first,X15,X16)|~iext(uri_rdf_rest,X15,uri_rdf_nil))|(~iext(uri_owl_oneOf,X14,X15)|(X18!=X16|icext(X14,X18))))))&(((~iext(uri_rdf_first,X15,X16)|~iext(uri_rdf_rest,X15,uri_rdf_nil))|((~ic(X14)|(~icext(X14,skolem0008(X14,X15,X16))|skolem0008(X14,X15,X16)!=X16))|iext(uri_owl_oneOf,X14,X15)))&((~iext(uri_rdf_first,X15,X16)|~iext(uri_rdf_rest,X15,uri_rdf_nil))|((~ic(X14)|(icext(X14,skolem0008(X14,X15,X16))|skolem0008(X14,X15,X16)=X16))|iext(uri_owl_oneOf,X14,X15)))))))))),inference(distribute,[status(thm)],[c32])).
% 0.62/0.86 cnf(c35,plain,~iext(uri_rdf_first,X97,X95)|~iext(uri_rdf_rest,X97,uri_rdf_nil)|~iext(uri_owl_oneOf,X96,X97)|~icext(X96,X98)|X98=X95,inference(split_conjunct,[status(thm)],[c33])).
% 0.62/0.86 cnf(c118,plain,~iext(uri_rdf_first,skolem0003,X198)|~iext(uri_rdf_rest,skolem0003,uri_rdf_nil)|~icext(skolem0001,X197)|X197=X198,inference(resolution,[status(thm)],[c35, c7])).
% 0.62/0.86 cnf(c232,plain,~iext(uri_rdf_first,skolem0003,X205)|~icext(skolem0001,X204)|X204=X205,inference(resolution,[status(thm)],[c118, c9])).
% 0.62/0.86 cnf(c242,plain,~icext(skolem0001,X206)|X206=uri_ex_w,inference(resolution,[status(thm)],[c232, c8])).
% 0.62/0.86 cnf(c25,plain,~ip(X72)|iext(X72,skolem0005(X72),skolem0007(X72))|icext(uri_owl_InverseFunctionalProperty,X72),inference(split_conjunct,[status(thm)],[c22])).
% 0.62/0.86 cnf(c110,plain,iext(uri_ex_p,skolem0005(uri_ex_p),skolem0007(uri_ex_p))|icext(uri_owl_InverseFunctionalProperty,uri_ex_p),inference(resolution,[status(thm)],[c105, c25])).
% 0.62/0.86 cnf(c175,plain,icext(uri_owl_InverseFunctionalProperty,uri_ex_p)|~iext(uri_rdfs_domain,uri_ex_p,X244)|icext(X244,skolem0005(uri_ex_p)),inference(resolution,[status(thm)],[c110, c44])).
% 0.62/0.86 cnf(c345,plain,icext(uri_owl_InverseFunctionalProperty,uri_ex_p)|icext(skolem0001,skolem0005(uri_ex_p)),inference(resolution,[status(thm)],[c175, c6])).
% 0.62/0.86 cnf(c346,plain,icext(skolem0001,skolem0005(uri_ex_p))|iext(uri_rdf_type,uri_ex_p,uri_owl_InverseFunctionalProperty),inference(resolution,[status(thm)],[c345, c50])).
% 0.62/0.86 cnf(c377,plain,icext(skolem0001,skolem0005(uri_ex_p)),inference(resolution,[status(thm)],[c346, c16])).
% 0.62/0.86 cnf(c380,plain,skolem0005(uri_ex_p)=uri_ex_w,inference(resolution,[status(thm)],[c377, c242])).
% 0.62/0.86 cnf(c385,plain,uri_ex_w=skolem0005(uri_ex_p),inference(resolution,[status(thm)],[c380, symmetry])).
% 0.62/0.86 cnf(c394,plain,X253!=uri_ex_w|X253=skolem0005(uri_ex_p),inference(resolution,[status(thm)],[c385, transitivity])).
% 0.62/0.86 cnf(c26,plain,~ip(X78)|iext(X78,skolem0006(X78),skolem0007(X78))|icext(uri_owl_InverseFunctionalProperty,X78),inference(split_conjunct,[status(thm)],[c22])).
% 0.62/0.86 cnf(c111,plain,iext(uri_ex_p,skolem0006(uri_ex_p),skolem0007(uri_ex_p))|icext(uri_owl_InverseFunctionalProperty,uri_ex_p),inference(resolution,[status(thm)],[c105, c26])).
% 0.62/0.86 cnf(c185,plain,iext(uri_ex_p,skolem0006(uri_ex_p),skolem0007(uri_ex_p))|iext(uri_rdf_type,uri_ex_p,uri_owl_InverseFunctionalProperty),inference(resolution,[status(thm)],[c111, c50])).
% 0.62/0.86 cnf(c439,plain,iext(uri_ex_p,skolem0006(uri_ex_p),skolem0007(uri_ex_p)),inference(resolution,[status(thm)],[c185, c16])).
% 0.62/0.86 cnf(c442,plain,~iext(uri_rdfs_domain,uri_ex_p,X263)|icext(X263,skolem0006(uri_ex_p)),inference(resolution,[status(thm)],[c439, c44])).
% 0.62/0.86 cnf(c452,plain,icext(skolem0001,skolem0006(uri_ex_p)),inference(resolution,[status(thm)],[c442, c6])).
% 0.62/0.86 cnf(c455,plain,skolem0006(uri_ex_p)=uri_ex_w,inference(resolution,[status(thm)],[c452, c242])).
% 0.62/0.86 cnf(c456,plain,skolem0006(uri_ex_p)=skolem0005(uri_ex_p),inference(resolution,[status(thm)],[c455, c394])).
% 0.62/0.86 cnf(c477,plain,skolem0005(uri_ex_p)=skolem0006(uri_ex_p),inference(resolution,[status(thm)],[c456, symmetry])).
% 0.62/0.86 cnf(c484,plain,~ip(uri_ex_p)|icext(uri_owl_InverseFunctionalProperty,uri_ex_p),inference(resolution,[status(thm)],[c477, c27])).
% 0.62/0.86 cnf(c486,plain,icext(uri_owl_InverseFunctionalProperty,uri_ex_p),inference(resolution,[status(thm)],[c484, c105])).
% 0.62/0.86 cnf(c487,plain,iext(uri_rdf_type,uri_ex_p,uri_owl_InverseFunctionalProperty),inference(resolution,[status(thm)],[c486, c50])).
% 0.62/0.86 cnf(c494,plain,$false,inference(resolution,[status(thm)],[c487, c16])).
% 0.62/0.86 % SZS output end CNFRefutation
% 0.62/0.86
% 0.62/0.86 % Initial clauses : 32
% 0.62/0.86 % Processed clauses : 205
% 0.62/0.86 % Factors computed : 4
% 0.62/0.86 % Resolvents computed: 443
% 0.62/0.86 % Tautologies deleted: 8
% 0.62/0.86 % Forward subsumed : 99
% 0.62/0.86 % Backward subsumed : 25
% 0.62/0.86 % -------- CPU Time ---------
% 0.62/0.86 % User time : 0.489 s
% 0.62/0.86 % System time : 0.011 s
% 0.62/0.86 % Total time : 0.500 s
%------------------------------------------------------------------------------