%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SWB004+2 : TPTP v8.1.2. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n015.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:44 EDT 2024
% Result : Theorem 18.04s 18.24s
% Output : Refutation 18.04s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : SWB004+2 : TPTP v8.1.2. Released v5.2.0.
% 0.08/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n015.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Wed May 8 22:12:08 EDT 2024
% 0.14/0.36 % CPUTime :
% 18.04/18.24 % Version: 1.5
% 18.04/18.24 % SZS status Theorem
% 18.04/18.24 % SZS output start CNFRefutation
% 18.04/18.24 fof(simple_ir,axiom,(![X]:ir(X)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', simple_ir)).
% 18.04/18.24 fof(c63,plain,(![X28]:ir(X28)),inference(variable_rename,[status(thm)],[simple_ir])).
% 18.04/18.24 cnf(c64,plain,ir(X29),inference(split_conjunct,[status(thm)],[c63])).
% 18.04/18.24 fof(owl_class_thing_ext,axiom,(![X]:(icext(uri_owl_Thing,X)<=>ir(X))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', owl_class_thing_ext)).
% 18.04/18.24 fof(c26,plain,(![X]:((~icext(uri_owl_Thing,X)|ir(X))&(~ir(X)|icext(uri_owl_Thing,X)))),inference(fof_nnf,[status(thm)],[owl_class_thing_ext])).
% 18.04/18.24 fof(c27,plain,((![X]:(~icext(uri_owl_Thing,X)|ir(X)))&(![X]:(~ir(X)|icext(uri_owl_Thing,X)))),inference(shift_quantors,[status(thm)],[c26])).
% 18.04/18.24 fof(c29,plain,(![X15]:(![X16]:((~icext(uri_owl_Thing,X15)|ir(X15))&(~ir(X16)|icext(uri_owl_Thing,X16))))),inference(shift_quantors,[status(thm)],[fof(c28,plain,((![X15]:(~icext(uri_owl_Thing,X15)|ir(X15)))&(![X16]:(~ir(X16)|icext(uri_owl_Thing,X16)))),inference(variable_rename,[status(thm)],[c27])).])).
% 18.04/18.24 cnf(c31,plain,~ir(X32)|icext(uri_owl_Thing,X32),inference(split_conjunct,[status(thm)],[c29])).
% 18.04/18.24 cnf(c65,plain,icext(uri_owl_Thing,X33),inference(resolution,[status(thm)],[c31, c64])).
% 18.04/18.24 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)).
% 18.04/18.24 fof(c57,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])).
% 18.04/18.24 fof(c58,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)],[c57])).
% 18.04/18.24 fof(c60,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(c59,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)],[c58])).])).
% 18.04/18.24 cnf(c62,plain,~icext(X58,X59)|iext(uri_rdf_type,X59,X58),inference(split_conjunct,[status(thm)],[c60])).
% 18.04/18.24 cnf(c89,plain,iext(uri_rdf_type,X62,uri_owl_Thing),inference(resolution,[status(thm)],[c62, c65])).
% 18.04/18.24 fof(owl_class_classowl_type,axiom,ic(uri_owl_Class),file('/export/starexec/sandbox/benchmark/theBenchmark.p', owl_class_classowl_type)).
% 18.04/18.24 cnf(c53,plain,ic(uri_owl_Class),inference(split_conjunct,[status(thm)],[owl_class_classowl_type])).
% 18.04/18.24 fof(owl_class_classowl_ext,axiom,(![X]:(icext(uri_owl_Class,X)<=>ic(X))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', owl_class_classowl_ext)).
% 18.04/18.24 fof(c47,plain,(![X]:((~icext(uri_owl_Class,X)|ic(X))&(~ic(X)|icext(uri_owl_Class,X)))),inference(fof_nnf,[status(thm)],[owl_class_classowl_ext])).
% 18.04/18.24 fof(c48,plain,((![X]:(~icext(uri_owl_Class,X)|ic(X)))&(![X]:(~ic(X)|icext(uri_owl_Class,X)))),inference(shift_quantors,[status(thm)],[c47])).
% 18.04/18.24 fof(c50,plain,(![X21]:(![X22]:((~icext(uri_owl_Class,X21)|ic(X21))&(~ic(X22)|icext(uri_owl_Class,X22))))),inference(shift_quantors,[status(thm)],[fof(c49,plain,((![X21]:(~icext(uri_owl_Class,X21)|ic(X21)))&(![X22]:(~ic(X22)|icext(uri_owl_Class,X22)))),inference(variable_rename,[status(thm)],[c48])).])).
% 18.04/18.24 cnf(c52,plain,~ic(X46)|icext(uri_owl_Class,X46),inference(split_conjunct,[status(thm)],[c50])).
% 18.04/18.24 cnf(c75,plain,icext(uri_owl_Class,uri_owl_Class),inference(resolution,[status(thm)],[c52, c53])).
% 18.04/18.24 cnf(c91,plain,iext(uri_rdf_type,uri_owl_Class,uri_owl_Class),inference(resolution,[status(thm)],[c62, c75])).
% 18.04/18.24 fof(owl_class_thing_type,axiom,ic(uri_owl_Thing),file('/export/starexec/sandbox/benchmark/theBenchmark.p', owl_class_thing_type)).
% 18.04/18.24 cnf(c32,plain,ic(uri_owl_Thing),inference(split_conjunct,[status(thm)],[owl_class_thing_type])).
% 18.04/18.24 fof(owl_rdfsext_subclassof,axiom,(![C1]:(![C2]:(iext(uri_rdfs_subClassOf,C1,C2)<=>((ic(C1)&ic(C2))&(![X]:(icext(C1,X)=>icext(C2,X))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', owl_rdfsext_subclassof)).
% 18.04/18.24 fof(c15,plain,(![C1]:(![C2]:((~iext(uri_rdfs_subClassOf,C1,C2)|((ic(C1)&ic(C2))&(![X]:(~icext(C1,X)|icext(C2,X)))))&(((~ic(C1)|~ic(C2))|(?[X]:(icext(C1,X)&~icext(C2,X))))|iext(uri_rdfs_subClassOf,C1,C2))))),inference(fof_nnf,[status(thm)],[owl_rdfsext_subclassof])).
% 18.04/18.24 fof(c16,plain,((![C1]:(![C2]:(~iext(uri_rdfs_subClassOf,C1,C2)|((ic(C1)&ic(C2))&(![X]:(~icext(C1,X)|icext(C2,X)))))))&(![C1]:(![C2]:(((~ic(C1)|~ic(C2))|(?[X]:(icext(C1,X)&~icext(C2,X))))|iext(uri_rdfs_subClassOf,C1,C2))))),inference(shift_quantors,[status(thm)],[c15])).
% 18.04/18.24 fof(c17,plain,((![X9]:(![X10]:(~iext(uri_rdfs_subClassOf,X9,X10)|((ic(X9)&ic(X10))&(![X11]:(~icext(X9,X11)|icext(X10,X11)))))))&(![X12]:(![X13]:(((~ic(X12)|~ic(X13))|(?[X14]:(icext(X12,X14)&~icext(X13,X14))))|iext(uri_rdfs_subClassOf,X12,X13))))),inference(variable_rename,[status(thm)],[c16])).
% 18.04/18.24 fof(c19,plain,(![X9]:(![X10]:(![X11]:(![X12]:(![X13]:((~iext(uri_rdfs_subClassOf,X9,X10)|((ic(X9)&ic(X10))&(~icext(X9,X11)|icext(X10,X11))))&(((~ic(X12)|~ic(X13))|(icext(X12,skolem0002(X12,X13))&~icext(X13,skolem0002(X12,X13))))|iext(uri_rdfs_subClassOf,X12,X13)))))))),inference(shift_quantors,[status(thm)],[fof(c18,plain,((![X9]:(![X10]:(~iext(uri_rdfs_subClassOf,X9,X10)|((ic(X9)&ic(X10))&(![X11]:(~icext(X9,X11)|icext(X10,X11)))))))&(![X12]:(![X13]:(((~ic(X12)|~ic(X13))|(icext(X12,skolem0002(X12,X13))&~icext(X13,skolem0002(X12,X13))))|iext(uri_rdfs_subClassOf,X12,X13))))),inference(skolemize,[status(esa)],[c17])).])).
% 18.04/18.24 fof(c20,plain,(![X9]:(![X10]:(![X11]:(![X12]:(![X13]:((((~iext(uri_rdfs_subClassOf,X9,X10)|ic(X9))&(~iext(uri_rdfs_subClassOf,X9,X10)|ic(X10)))&(~iext(uri_rdfs_subClassOf,X9,X10)|(~icext(X9,X11)|icext(X10,X11))))&((((~ic(X12)|~ic(X13))|icext(X12,skolem0002(X12,X13)))|iext(uri_rdfs_subClassOf,X12,X13))&(((~ic(X12)|~ic(X13))|~icext(X13,skolem0002(X12,X13)))|iext(uri_rdfs_subClassOf,X12,X13))))))))),inference(distribute,[status(thm)],[c19])).
% 18.04/18.24 cnf(c25,plain,~ic(X70)|~ic(X69)|~icext(X69,skolem0002(X70,X69))|iext(uri_rdfs_subClassOf,X70,X69),inference(split_conjunct,[status(thm)],[c20])).
% 18.04/18.24 cnf(c111,plain,~ic(X71)|~ic(uri_owl_Thing)|iext(uri_rdfs_subClassOf,X71,uri_owl_Thing),inference(resolution,[status(thm)],[c25, c65])).
% 18.04/18.24 cnf(c114,plain,~ic(X72)|iext(uri_rdfs_subClassOf,X72,uri_owl_Thing),inference(resolution,[status(thm)],[c111, c32])).
% 18.04/18.24 cnf(c116,plain,iext(uri_rdfs_subClassOf,uri_owl_Class,uri_owl_Thing),inference(resolution,[status(thm)],[c114, c53])).
% 18.04/18.24 fof(testcase_conclusion_fullish_004_Axiomatic_Triples,conjecture,((((iext(uri_rdf_type,uri_owl_Class,uri_owl_Thing)&iext(uri_rdf_type,uri_owl_Class,uri_owl_Class))&iext(uri_rdfs_subClassOf,uri_owl_Class,uri_owl_Thing))&iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class))&iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_owl_Class)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', testcase_conclusion_fullish_004_Axiomatic_Triples)).
% 18.04/18.24 fof(c0,negated_conjecture,(~((((iext(uri_rdf_type,uri_owl_Class,uri_owl_Thing)&iext(uri_rdf_type,uri_owl_Class,uri_owl_Class))&iext(uri_rdfs_subClassOf,uri_owl_Class,uri_owl_Thing))&iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class))&iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_owl_Class))),inference(assume_negation,[status(cth)],[testcase_conclusion_fullish_004_Axiomatic_Triples])).
% 18.04/18.24 fof(c1,negated_conjecture,((((~iext(uri_rdf_type,uri_owl_Class,uri_owl_Thing)|~iext(uri_rdf_type,uri_owl_Class,uri_owl_Class))|~iext(uri_rdfs_subClassOf,uri_owl_Class,uri_owl_Thing))|~iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class))|~iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_owl_Class)),inference(fof_nnf,[status(thm)],[c0])).
% 18.04/18.24 cnf(c2,negated_conjecture,~iext(uri_rdf_type,uri_owl_Class,uri_owl_Thing)|~iext(uri_rdf_type,uri_owl_Class,uri_owl_Class)|~iext(uri_rdfs_subClassOf,uri_owl_Class,uri_owl_Thing)|~iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class)|~iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_owl_Class),inference(split_conjunct,[status(thm)],[c1])).
% 18.04/18.24 fof(owl_class_datatype_type,axiom,ic(uri_rdfs_Datatype),file('/export/starexec/sandbox/benchmark/theBenchmark.p', owl_class_datatype_type)).
% 18.04/18.24 cnf(c39,plain,ic(uri_rdfs_Datatype),inference(split_conjunct,[status(thm)],[owl_class_datatype_type])).
% 18.04/18.25 fof(owl_parts_idc_cond_set,axiom,(![X]:(idc(X)=>ic(X))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', owl_parts_idc_cond_set)).
% 18.04/18.25 fof(c54,plain,(![X]:(~idc(X)|ic(X))),inference(fof_nnf,[status(thm)],[owl_parts_idc_cond_set])).
% 18.04/18.25 fof(c55,plain,(![X23]:(~idc(X23)|ic(X23))),inference(variable_rename,[status(thm)],[c54])).
% 18.04/18.25 cnf(c56,plain,~idc(X30)|ic(X30),inference(split_conjunct,[status(thm)],[c55])).
% 18.04/18.25 fof(owl_class_datatype_ext,axiom,(![X]:(icext(uri_rdfs_Datatype,X)<=>idc(X))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', owl_class_datatype_ext)).
% 18.04/18.25 fof(c33,plain,(![X]:((~icext(uri_rdfs_Datatype,X)|idc(X))&(~idc(X)|icext(uri_rdfs_Datatype,X)))),inference(fof_nnf,[status(thm)],[owl_class_datatype_ext])).
% 18.04/18.25 fof(c34,plain,((![X]:(~icext(uri_rdfs_Datatype,X)|idc(X)))&(![X]:(~idc(X)|icext(uri_rdfs_Datatype,X)))),inference(shift_quantors,[status(thm)],[c33])).
% 18.04/18.25 fof(c36,plain,(![X17]:(![X18]:((~icext(uri_rdfs_Datatype,X17)|idc(X17))&(~idc(X18)|icext(uri_rdfs_Datatype,X18))))),inference(shift_quantors,[status(thm)],[fof(c35,plain,((![X17]:(~icext(uri_rdfs_Datatype,X17)|idc(X17)))&(![X18]:(~idc(X18)|icext(uri_rdfs_Datatype,X18)))),inference(variable_rename,[status(thm)],[c34])).])).
% 18.04/18.25 cnf(c37,plain,~icext(uri_rdfs_Datatype,X34)|idc(X34),inference(split_conjunct,[status(thm)],[c36])).
% 18.04/18.25 cnf(c24,plain,~ic(X68)|~ic(X67)|icext(X68,skolem0002(X68,X67))|iext(uri_rdfs_subClassOf,X68,X67),inference(split_conjunct,[status(thm)],[c20])).
% 18.04/18.25 cnf(c105,plain,~ic(X87)|icext(X87,skolem0002(X87,uri_owl_Class))|iext(uri_rdfs_subClassOf,X87,uri_owl_Class),inference(resolution,[status(thm)],[c24, c53])).
% 18.04/18.25 cnf(c161,plain,icext(uri_rdfs_Datatype,skolem0002(uri_rdfs_Datatype,uri_owl_Class))|iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_owl_Class),inference(resolution,[status(thm)],[c105, c39])).
% 18.04/18.25 cnf(c343,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_owl_Class)|idc(skolem0002(uri_rdfs_Datatype,uri_owl_Class)),inference(resolution,[status(thm)],[c161, c37])).
% 18.04/18.25 cnf(c353,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_owl_Class)|ic(skolem0002(uri_rdfs_Datatype,uri_owl_Class)),inference(resolution,[status(thm)],[c343, c56])).
% 18.04/18.25 cnf(c367,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_owl_Class)|icext(uri_owl_Class,skolem0002(uri_rdfs_Datatype,uri_owl_Class)),inference(resolution,[status(thm)],[c353, c52])).
% 18.04/18.25 cnf(c542,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_owl_Class)|~ic(uri_rdfs_Datatype)|~ic(uri_owl_Class),inference(resolution,[status(thm)],[c367, c25])).
% 18.04/18.25 cnf(c545,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_owl_Class)|~ic(uri_rdfs_Datatype),inference(resolution,[status(thm)],[c542, c53])).
% 18.04/18.25 cnf(c546,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_owl_Class),inference(resolution,[status(thm)],[c545, c39])).
% 18.04/18.25 cnf(c547,plain,~iext(uri_rdf_type,uri_owl_Class,uri_owl_Thing)|~iext(uri_rdf_type,uri_owl_Class,uri_owl_Class)|~iext(uri_rdfs_subClassOf,uri_owl_Class,uri_owl_Thing)|~iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c546, c2])).
% 18.04/18.25 fof(owl_class_classrdfs_type,axiom,ic(uri_rdfs_Class),file('/export/starexec/sandbox/benchmark/theBenchmark.p', owl_class_classrdfs_type)).
% 18.04/18.25 cnf(c46,plain,ic(uri_rdfs_Class),inference(split_conjunct,[status(thm)],[owl_class_classrdfs_type])).
% 18.04/18.25 fof(owl_eqdis_equivalentclass,axiom,(![C1]:(![C2]:(iext(uri_owl_equivalentClass,C1,C2)<=>((ic(C1)&ic(C2))&(![X]:(icext(C1,X)<=>icext(C2,X))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', owl_eqdis_equivalentclass)).
% 18.04/18.25 fof(c3,plain,(![C1]:(![C2]:((~iext(uri_owl_equivalentClass,C1,C2)|((ic(C1)&ic(C2))&(![X]:((~icext(C1,X)|icext(C2,X))&(~icext(C2,X)|icext(C1,X))))))&(((~ic(C1)|~ic(C2))|(?[X]:((~icext(C1,X)|~icext(C2,X))&(icext(C1,X)|icext(C2,X)))))|iext(uri_owl_equivalentClass,C1,C2))))),inference(fof_nnf,[status(thm)],[owl_eqdis_equivalentclass])).
% 18.04/18.25 fof(c4,plain,((![C1]:(![C2]:(~iext(uri_owl_equivalentClass,C1,C2)|((ic(C1)&ic(C2))&((![X]:(~icext(C1,X)|icext(C2,X)))&(![X]:(~icext(C2,X)|icext(C1,X))))))))&(![C1]:(![C2]:(((~ic(C1)|~ic(C2))|(?[X]:((~icext(C1,X)|~icext(C2,X))&(icext(C1,X)|icext(C2,X)))))|iext(uri_owl_equivalentClass,C1,C2))))),inference(shift_quantors,[status(thm)],[c3])).
% 18.04/18.25 fof(c5,plain,((![X2]:(![X3]:(~iext(uri_owl_equivalentClass,X2,X3)|((ic(X2)&ic(X3))&((![X4]:(~icext(X2,X4)|icext(X3,X4)))&(![X5]:(~icext(X3,X5)|icext(X2,X5))))))))&(![X6]:(![X7]:(((~ic(X6)|~ic(X7))|(?[X8]:((~icext(X6,X8)|~icext(X7,X8))&(icext(X6,X8)|icext(X7,X8)))))|iext(uri_owl_equivalentClass,X6,X7))))),inference(variable_rename,[status(thm)],[c4])).
% 18.04/18.25 fof(c7,plain,(![X2]:(![X3]:(![X4]:(![X5]:(![X6]:(![X7]:((~iext(uri_owl_equivalentClass,X2,X3)|((ic(X2)&ic(X3))&((~icext(X2,X4)|icext(X3,X4))&(~icext(X3,X5)|icext(X2,X5)))))&(((~ic(X6)|~ic(X7))|((~icext(X6,skolem0001(X6,X7))|~icext(X7,skolem0001(X6,X7)))&(icext(X6,skolem0001(X6,X7))|icext(X7,skolem0001(X6,X7)))))|iext(uri_owl_equivalentClass,X6,X7))))))))),inference(shift_quantors,[status(thm)],[fof(c6,plain,((![X2]:(![X3]:(~iext(uri_owl_equivalentClass,X2,X3)|((ic(X2)&ic(X3))&((![X4]:(~icext(X2,X4)|icext(X3,X4)))&(![X5]:(~icext(X3,X5)|icext(X2,X5))))))))&(![X6]:(![X7]:(((~ic(X6)|~ic(X7))|((~icext(X6,skolem0001(X6,X7))|~icext(X7,skolem0001(X6,X7)))&(icext(X6,skolem0001(X6,X7))|icext(X7,skolem0001(X6,X7)))))|iext(uri_owl_equivalentClass,X6,X7))))),inference(skolemize,[status(esa)],[c5])).])).
% 18.04/18.25 fof(c8,plain,(![X2]:(![X3]:(![X4]:(![X5]:(![X6]:(![X7]:((((~iext(uri_owl_equivalentClass,X2,X3)|ic(X2))&(~iext(uri_owl_equivalentClass,X2,X3)|ic(X3)))&((~iext(uri_owl_equivalentClass,X2,X3)|(~icext(X2,X4)|icext(X3,X4)))&(~iext(uri_owl_equivalentClass,X2,X3)|(~icext(X3,X5)|icext(X2,X5)))))&((((~ic(X6)|~ic(X7))|(~icext(X6,skolem0001(X6,X7))|~icext(X7,skolem0001(X6,X7))))|iext(uri_owl_equivalentClass,X6,X7))&(((~ic(X6)|~ic(X7))|(icext(X6,skolem0001(X6,X7))|icext(X7,skolem0001(X6,X7))))|iext(uri_owl_equivalentClass,X6,X7)))))))))),inference(distribute,[status(thm)],[c7])).
% 18.04/18.25 cnf(c14,plain,~ic(X61)|~ic(X60)|icext(X61,skolem0001(X61,X60))|icext(X60,skolem0001(X61,X60))|iext(uri_owl_equivalentClass,X61,X60),inference(split_conjunct,[status(thm)],[c8])).
% 18.04/18.25 cnf(c94,plain,~ic(X79)|icext(X79,skolem0001(X79,uri_rdfs_Class))|icext(uri_rdfs_Class,skolem0001(X79,uri_rdfs_Class))|iext(uri_owl_equivalentClass,X79,uri_rdfs_Class),inference(resolution,[status(thm)],[c14, c46])).
% 18.04/18.25 cnf(c138,plain,icext(uri_owl_Class,skolem0001(uri_owl_Class,uri_rdfs_Class))|icext(uri_rdfs_Class,skolem0001(uri_owl_Class,uri_rdfs_Class))|iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c94, c53])).
% 18.04/18.25 cnf(c23,plain,~iext(uri_rdfs_subClassOf,X66,X64)|~icext(X66,X65)|icext(X64,X65),inference(split_conjunct,[status(thm)],[c20])).
% 18.04/18.25 fof(owl_class_classrdfs_ext,axiom,(![X]:(icext(uri_rdfs_Class,X)<=>ic(X))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', owl_class_classrdfs_ext)).
% 18.04/18.25 fof(c40,plain,(![X]:((~icext(uri_rdfs_Class,X)|ic(X))&(~ic(X)|icext(uri_rdfs_Class,X)))),inference(fof_nnf,[status(thm)],[owl_class_classrdfs_ext])).
% 18.04/18.25 fof(c41,plain,((![X]:(~icext(uri_rdfs_Class,X)|ic(X)))&(![X]:(~ic(X)|icext(uri_rdfs_Class,X)))),inference(shift_quantors,[status(thm)],[c40])).
% 18.04/18.25 fof(c43,plain,(![X19]:(![X20]:((~icext(uri_rdfs_Class,X19)|ic(X19))&(~ic(X20)|icext(uri_rdfs_Class,X20))))),inference(shift_quantors,[status(thm)],[fof(c42,plain,((![X19]:(~icext(uri_rdfs_Class,X19)|ic(X19)))&(![X20]:(~ic(X20)|icext(uri_rdfs_Class,X20)))),inference(variable_rename,[status(thm)],[c41])).])).
% 18.04/18.25 cnf(c44,plain,~icext(uri_rdfs_Class,X38)|ic(X38),inference(split_conjunct,[status(thm)],[c43])).
% 18.04/18.25 cnf(c158,plain,icext(uri_rdfs_Class,skolem0002(uri_rdfs_Class,uri_owl_Class))|iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_owl_Class),inference(resolution,[status(thm)],[c105, c46])).
% 18.04/18.25 cnf(c301,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_owl_Class)|ic(skolem0002(uri_rdfs_Class,uri_owl_Class)),inference(resolution,[status(thm)],[c158, c44])).
% 18.04/18.25 cnf(c317,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_owl_Class)|icext(uri_owl_Class,skolem0002(uri_rdfs_Class,uri_owl_Class)),inference(resolution,[status(thm)],[c301, c52])).
% 18.04/18.25 cnf(c470,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_owl_Class)|~ic(uri_rdfs_Class)|~ic(uri_owl_Class),inference(resolution,[status(thm)],[c317, c25])).
% 18.04/18.25 cnf(c484,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_owl_Class)|~ic(uri_rdfs_Class),inference(resolution,[status(thm)],[c470, c53])).
% 18.04/18.25 cnf(c485,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_owl_Class),inference(resolution,[status(thm)],[c484, c46])).
% 18.04/18.25 cnf(c487,plain,~icext(uri_rdfs_Class,X106)|icext(uri_owl_Class,X106),inference(resolution,[status(thm)],[c485, c23])).
% 18.04/18.25 cnf(c493,plain,icext(uri_owl_Class,skolem0001(uri_owl_Class,uri_rdfs_Class))|iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c487, c138])).
% 18.04/18.25 cnf(c13,plain,~ic(X51)|~ic(X50)|~icext(X51,skolem0001(X51,X50))|~icext(X50,skolem0001(X51,X50))|iext(uri_owl_equivalentClass,X51,X50),inference(split_conjunct,[status(thm)],[c8])).
% 18.04/18.25 cnf(c45,plain,~ic(X39)|icext(uri_rdfs_Class,X39),inference(split_conjunct,[status(thm)],[c43])).
% 18.04/18.25 cnf(c51,plain,~icext(uri_owl_Class,X45)|ic(X45),inference(split_conjunct,[status(thm)],[c50])).
% 18.04/18.25 cnf(c104,plain,~ic(X86)|icext(X86,skolem0002(X86,uri_rdfs_Class))|iext(uri_rdfs_subClassOf,X86,uri_rdfs_Class),inference(resolution,[status(thm)],[c24, c46])).
% 18.04/18.25 cnf(c155,plain,icext(uri_owl_Class,skolem0002(uri_owl_Class,uri_rdfs_Class))|iext(uri_rdfs_subClassOf,uri_owl_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c104, c53])).
% 18.04/18.25 cnf(c275,plain,iext(uri_rdfs_subClassOf,uri_owl_Class,uri_rdfs_Class)|ic(skolem0002(uri_owl_Class,uri_rdfs_Class)),inference(resolution,[status(thm)],[c155, c51])).
% 18.04/18.25 cnf(c293,plain,iext(uri_rdfs_subClassOf,uri_owl_Class,uri_rdfs_Class)|icext(uri_rdfs_Class,skolem0002(uri_owl_Class,uri_rdfs_Class)),inference(resolution,[status(thm)],[c275, c45])).
% 18.04/18.25 cnf(c427,plain,iext(uri_rdfs_subClassOf,uri_owl_Class,uri_rdfs_Class)|~ic(uri_owl_Class)|~ic(uri_rdfs_Class),inference(resolution,[status(thm)],[c293, c25])).
% 18.04/18.25 cnf(c429,plain,iext(uri_rdfs_subClassOf,uri_owl_Class,uri_rdfs_Class)|~ic(uri_owl_Class),inference(resolution,[status(thm)],[c427, c46])).
% 18.04/18.25 cnf(c430,plain,iext(uri_rdfs_subClassOf,uri_owl_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c429, c53])).
% 18.04/18.25 cnf(c432,plain,~icext(uri_owl_Class,X102)|icext(uri_rdfs_Class,X102),inference(resolution,[status(thm)],[c430, c23])).
% 18.04/18.25 cnf(c438,plain,icext(uri_rdfs_Class,skolem0001(uri_owl_Class,uri_rdfs_Class))|iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c432, c138])).
% 18.04/18.25 cnf(c1596,plain,iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class)|~ic(uri_owl_Class)|~ic(uri_rdfs_Class)|~icext(uri_owl_Class,skolem0001(uri_owl_Class,uri_rdfs_Class)),inference(resolution,[status(thm)],[c438, c13])).
% 18.04/18.25 cnf(c17878,plain,iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class)|~ic(uri_owl_Class)|~ic(uri_rdfs_Class),inference(resolution,[status(thm)],[c1596, c493])).
% 18.04/18.25 cnf(c17879,plain,iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class)|~ic(uri_owl_Class),inference(resolution,[status(thm)],[c17878, c46])).
% 18.04/18.25 cnf(c17880,plain,iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c17879, c53])).
% 18.04/18.25 cnf(c17885,plain,~iext(uri_rdf_type,uri_owl_Class,uri_owl_Thing)|~iext(uri_rdf_type,uri_owl_Class,uri_owl_Class)|~iext(uri_rdfs_subClassOf,uri_owl_Class,uri_owl_Thing),inference(resolution,[status(thm)],[c17880, c547])).
% 18.04/18.25 cnf(c17926,plain,~iext(uri_rdf_type,uri_owl_Class,uri_owl_Thing)|~iext(uri_rdf_type,uri_owl_Class,uri_owl_Class),inference(resolution,[status(thm)],[c17885, c116])).
% 18.04/18.25 cnf(c17927,plain,~iext(uri_rdf_type,uri_owl_Class,uri_owl_Thing),inference(resolution,[status(thm)],[c17926, c91])).
% 18.04/18.25 cnf(c17928,plain,$false,inference(resolution,[status(thm)],[c17927, c89])).
% 18.04/18.25 % SZS output end CNFRefutation
% 18.04/18.25
% 18.04/18.25 % Initial clauses : 28
% 18.04/18.25 % Processed clauses : 992
% 18.04/18.25 % Factors computed : 4
% 18.04/18.25 % Resolvents computed: 17860
% 18.04/18.25 % Tautologies deleted: 27
% 18.04/18.25 % Forward subsumed : 3403
% 18.04/18.25 % Backward subsumed : 118
% 18.04/18.25 % -------- CPU Time ---------
% 18.04/18.25 % User time : 17.826 s
% 18.04/18.25 % System time : 0.055 s
% 18.04/18.25 % Total time : 17.881 s
%------------------------------------------------------------------------------