%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SWB030+4 : TPTP v8.1.2. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n021.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:57 EDT 2024
% Result : Satisfiable 3.29s 3.47s
% Output : Saturation 3.29s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : SWB030+4 : TPTP v8.1.2. Released v5.2.0.
% 0.04/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n021.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed May 8 22:02:23 EDT 2024
% 0.13/0.35 % CPUTime :
% 3.29/3.47 % Version: 1.5
% 3.29/3.47 % SZS status Satisfiable
% 3.29/3.47 % SZS output start Saturation
% 3.29/3.47 fof(rdfs_subpropertyof_main,axiom,(![P]:(![Q]:(iext(uri_rdfs_subPropertyOf,P,Q)=>((ip(P)&ip(Q))&(![X]:(![Y]:(iext(P,X,Y)=>iext(Q,X,Y)))))))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_subpropertyof_main)).
% 3.29/3.47 fof(c18,plain,(![P]:(![Q]:(~iext(uri_rdfs_subPropertyOf,P,Q)|((ip(P)&ip(Q))&(![X]:(![Y]:(~iext(P,X,Y)|iext(Q,X,Y)))))))),inference(fof_nnf,[status(thm)],[rdfs_subpropertyof_main])).
% 3.29/3.47 fof(c20,plain,(![X7]:(![X8]:(![X9]:(![X10]:(~iext(uri_rdfs_subPropertyOf,X7,X8)|((ip(X7)&ip(X8))&(~iext(X7,X9,X10)|iext(X8,X9,X10)))))))),inference(shift_quantors,[status(thm)],[fof(c19,plain,(![X7]:(![X8]:(~iext(uri_rdfs_subPropertyOf,X7,X8)|((ip(X7)&ip(X8))&(![X9]:(![X10]:(~iext(X7,X9,X10)|iext(X8,X9,X10)))))))),inference(variable_rename,[status(thm)],[c18])).])).
% 3.29/3.47 fof(c21,plain,(![X7]:(![X8]:(![X9]:(![X10]:(((~iext(uri_rdfs_subPropertyOf,X7,X8)|ip(X7))&(~iext(uri_rdfs_subPropertyOf,X7,X8)|ip(X8)))&(~iext(uri_rdfs_subPropertyOf,X7,X8)|(~iext(X7,X9,X10)|iext(X8,X9,X10)))))))),inference(distribute,[status(thm)],[c20])).
% 3.29/3.47 cnf(c24,plain,~iext(uri_rdfs_subPropertyOf,X64,X65)|~iext(X64,X63,X66)|iext(X65,X63,X66),inference(split_conjunct,[status(thm)],[c21])).
% 3.29/3.47 fof(rdfs_subpropertyof_reflex,axiom,(![P]:(ip(P)=>iext(uri_rdfs_subPropertyOf,P,P))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_subpropertyof_reflex)).
% 3.29/3.47 fof(c14,plain,(![P]:(~ip(P)|iext(uri_rdfs_subPropertyOf,P,P))),inference(fof_nnf,[status(thm)],[rdfs_subpropertyof_reflex])).
% 3.29/3.47 fof(c15,plain,(![X6]:(~ip(X6)|iext(uri_rdfs_subPropertyOf,X6,X6))),inference(variable_rename,[status(thm)],[c14])).
% 3.29/3.47 cnf(c16,plain,~ip(X51)|iext(uri_rdfs_subPropertyOf,X51,X51),inference(split_conjunct,[status(thm)],[c15])).
% 3.29/3.47 fof(rdf_type_ip,axiom,(![P]:(iext(uri_rdf_type,P,uri_rdf_Property)<=>ip(P))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdf_type_ip)).
% 3.29/3.47 fof(c126,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])).
% 3.29/3.47 fof(c127,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)],[c126])).
% 3.29/3.47 fof(c129,plain,(![X39]:(![X40]:((~iext(uri_rdf_type,X39,uri_rdf_Property)|ip(X39))&(~ip(X40)|iext(uri_rdf_type,X40,uri_rdf_Property))))),inference(shift_quantors,[status(thm)],[fof(c128,plain,((![X39]:(~iext(uri_rdf_type,X39,uri_rdf_Property)|ip(X39)))&(![X40]:(~ip(X40)|iext(uri_rdf_type,X40,uri_rdf_Property)))),inference(variable_rename,[status(thm)],[c127])).])).
% 3.29/3.47 cnf(c130,plain,~iext(uri_rdf_type,X95,uri_rdf_Property)|ip(X95),inference(split_conjunct,[status(thm)],[c129])).
% 3.29/3.47 fof(rdfs_cext_def,axiom,(![X]:(![C]:(iext(uri_rdf_type,X,C)<=>icext(C,X)))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_cext_def)).
% 3.29/3.47 fof(c109,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])).
% 3.29/3.47 fof(c110,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)],[c109])).
% 3.29/3.47 fof(c112,plain,(![X35]:(![X36]:(![X37]:(![X38]:((~iext(uri_rdf_type,X35,X36)|icext(X36,X35))&(~icext(X38,X37)|iext(uri_rdf_type,X37,X38))))))),inference(shift_quantors,[status(thm)],[fof(c111,plain,((![X35]:(![X36]:(~iext(uri_rdf_type,X35,X36)|icext(X36,X35))))&(![X37]:(![X38]:(~icext(X38,X37)|iext(uri_rdf_type,X37,X38))))),inference(variable_rename,[status(thm)],[c110])).])).
% 3.29/3.47 cnf(c114,plain,~icext(X92,X91)|iext(uri_rdf_type,X91,X92),inference(split_conjunct,[status(thm)],[c112])).
% 3.29/3.47 fof(rdfs_range_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_range,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_range_domain)).
% 3.29/3.47 cnf(c51,plain,iext(uri_rdfs_domain,uri_rdfs_range,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_range_domain])).
% 3.29/3.47 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/Axioms/SWB003+0.ax', rdfs_domain_main)).
% 3.29/3.47 fof(c72,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])).
% 3.29/3.47 fof(c73,plain,(![P]:(![C]:(![X]:((~iext(uri_rdfs_domain,P,C)|(![Y]:~iext(P,X,Y)))|icext(C,X))))),inference(shift_quantors,[status(thm)],[c72])).
% 3.29/3.47 fof(c75,plain,(![X28]:(![X29]:(![X30]:(![X31]:((~iext(uri_rdfs_domain,X28,X29)|~iext(X28,X30,X31))|icext(X29,X30)))))),inference(shift_quantors,[status(thm)],[fof(c74,plain,(![X28]:(![X29]:(![X30]:((~iext(uri_rdfs_domain,X28,X29)|(![X31]:~iext(X28,X30,X31)))|icext(X29,X30))))),inference(variable_rename,[status(thm)],[c73])).])).
% 3.29/3.47 cnf(c76,plain,~iext(uri_rdfs_domain,X85,X83)|~iext(X85,X82,X84)|icext(X83,X82),inference(split_conjunct,[status(thm)],[c75])).
% 3.29/3.47 fof(rdfs_annotation_comment_range,axiom,iext(uri_rdfs_range,uri_rdfs_comment,uri_rdfs_Literal),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_comment_range)).
% 3.29/3.47 cnf(c122,plain,iext(uri_rdfs_range,uri_rdfs_comment,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[rdfs_annotation_comment_range])).
% 3.29/3.47 cnf(c416,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X306)|icext(X306,uri_rdfs_comment),inference(resolution,[status(thm)],[c122, c76])).
% 3.29/3.47 cnf(c1290,plain,icext(uri_rdf_Property,uri_rdfs_comment),inference(resolution,[status(thm)],[c416, c51])).
% 3.29/3.47 cnf(c1292,plain,iext(uri_rdf_type,uri_rdfs_comment,uri_rdf_Property),inference(resolution,[status(thm)],[c1290, c114])).
% 3.29/3.47 cnf(c1296,plain,ip(uri_rdfs_comment),inference(resolution,[status(thm)],[c1292, c130])).
% 3.29/3.47 cnf(c1300,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_comment,uri_rdfs_comment),inference(resolution,[status(thm)],[c1296, c16])).
% 3.29/3.47 cnf(c1307,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X642)|iext(X642,uri_rdfs_comment,uri_rdfs_comment),inference(resolution,[status(thm)],[c1300, c24])).
% 3.29/3.47 cnf(c1297,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X640)|iext(X640,uri_rdfs_comment,uri_rdf_Property),inference(resolution,[status(thm)],[c1292, c24])).
% 3.29/3.47 fof(rdfs_annotation_label_range,axiom,iext(uri_rdfs_range,uri_rdfs_label,uri_rdfs_Literal),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_label_range)).
% 3.29/3.47 cnf(c117,plain,iext(uri_rdfs_range,uri_rdfs_label,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[rdfs_annotation_label_range])).
% 3.29/3.47 cnf(c364,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X290)|icext(X290,uri_rdfs_label),inference(resolution,[status(thm)],[c117, c76])).
% 3.29/3.47 cnf(c1262,plain,icext(uri_rdf_Property,uri_rdfs_label),inference(resolution,[status(thm)],[c364, c51])).
% 3.29/3.47 cnf(c1263,plain,iext(uri_rdf_type,uri_rdfs_label,uri_rdf_Property),inference(resolution,[status(thm)],[c1262, c114])).
% 3.29/3.47 cnf(c1268,plain,ip(uri_rdfs_label),inference(resolution,[status(thm)],[c1263, c130])).
% 3.29/3.47 cnf(c1272,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_label,uri_rdfs_label),inference(resolution,[status(thm)],[c1268, c16])).
% 3.29/3.47 cnf(c1279,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X639)|iext(X639,uri_rdfs_label,uri_rdfs_label),inference(resolution,[status(thm)],[c1272, c24])).
% 3.29/3.47 cnf(c1269,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X637)|iext(X637,uri_rdfs_label,uri_rdf_Property),inference(resolution,[status(thm)],[c1263, c24])).
% 3.29/3.47 fof(rdfs_domain_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_domain_domain)).
% 3.29/3.47 cnf(c77,plain,iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_domain_domain])).
% 3.29/3.47 fof(rdfs_reification_predicate_domain,axiom,iext(uri_rdfs_domain,uri_rdf_predicate,uri_rdfs_Statement),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_reification_predicate_domain)).
% 3.29/3.47 cnf(c44,plain,iext(uri_rdfs_domain,uri_rdf_predicate,uri_rdfs_Statement),inference(split_conjunct,[status(thm)],[rdfs_reification_predicate_domain])).
% 3.29/3.47 cnf(c292,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X236)|icext(X236,uri_rdf_predicate),inference(resolution,[status(thm)],[c76, c44])).
% 3.29/3.47 cnf(c1206,plain,icext(uri_rdf_Property,uri_rdf_predicate),inference(resolution,[status(thm)],[c292, c77])).
% 3.29/3.47 cnf(c1207,plain,iext(uri_rdf_type,uri_rdf_predicate,uri_rdf_Property),inference(resolution,[status(thm)],[c1206, c114])).
% 3.29/3.47 cnf(c1211,plain,ip(uri_rdf_predicate),inference(resolution,[status(thm)],[c1207, c130])).
% 3.29/3.47 cnf(c1215,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_predicate,uri_rdf_predicate),inference(resolution,[status(thm)],[c1211, c16])).
% 3.29/3.47 cnf(c1221,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X636)|iext(X636,uri_rdf_predicate,uri_rdf_predicate),inference(resolution,[status(thm)],[c1215, c24])).
% 3.29/3.47 cnf(c1212,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X634)|iext(X634,uri_rdf_predicate,uri_rdf_Property),inference(resolution,[status(thm)],[c1207, c24])).
% 3.29/3.47 fof(rdfs_class_instsub_resource,axiom,(![C]:(ic(C)=>iext(uri_rdfs_subClassOf,C,uri_rdfs_Resource))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_class_instsub_resource)).
% 3.29/3.47 fof(c106,plain,(![C]:(~ic(C)|iext(uri_rdfs_subClassOf,C,uri_rdfs_Resource))),inference(fof_nnf,[status(thm)],[rdfs_class_instsub_resource])).
% 3.29/3.47 fof(c107,plain,(![X34]:(~ic(X34)|iext(uri_rdfs_subClassOf,X34,uri_rdfs_Resource))),inference(variable_rename,[status(thm)],[c106])).
% 3.29/3.47 cnf(c108,plain,~ic(X88)|iext(uri_rdfs_subClassOf,X88,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[c107])).
% 3.29/3.47 fof(rdfs_ic_def,axiom,(![X]:(ic(X)<=>icext(uri_rdfs_Class,X))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_ic_def)).
% 3.29/3.47 fof(c65,plain,(![X]:((~ic(X)|icext(uri_rdfs_Class,X))&(~icext(uri_rdfs_Class,X)|ic(X)))),inference(fof_nnf,[status(thm)],[rdfs_ic_def])).
% 3.29/3.47 fof(c66,plain,((![X]:(~ic(X)|icext(uri_rdfs_Class,X)))&(![X]:(~icext(uri_rdfs_Class,X)|ic(X)))),inference(shift_quantors,[status(thm)],[c65])).
% 3.29/3.47 fof(c68,plain,(![X26]:(![X27]:((~ic(X26)|icext(uri_rdfs_Class,X26))&(~icext(uri_rdfs_Class,X27)|ic(X27))))),inference(shift_quantors,[status(thm)],[fof(c67,plain,((![X26]:(~ic(X26)|icext(uri_rdfs_Class,X26)))&(![X27]:(~icext(uri_rdfs_Class,X27)|ic(X27)))),inference(variable_rename,[status(thm)],[c66])).])).
% 3.29/3.47 cnf(c70,plain,~icext(uri_rdfs_Class,X60)|ic(X60),inference(split_conjunct,[status(thm)],[c68])).
% 3.29/3.47 fof(rdfs_type_range,axiom,iext(uri_rdfs_range,uri_rdf_type,uri_rdfs_Class),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_type_range)).
% 3.29/3.47 cnf(c9,plain,iext(uri_rdfs_range,uri_rdf_type,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_type_range])).
% 3.29/3.47 fof(testcase_premise_fullish_030_Bad_Class,axiom,(?[BNODE_x]:((((iext(uri_rdf_type,uri_ex_c,uri_owl_Class)&iext(uri_owl_complementOf,uri_ex_c,BNODE_x))&iext(uri_rdf_type,BNODE_x,uri_owl_Restriction))&iext(uri_owl_onProperty,BNODE_x,uri_rdf_type))&iext(uri_owl_hasSelf,BNODE_x,literal_typed(dat_str_true,uri_xsd_boolean)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', testcase_premise_fullish_030_Bad_Class)).
% 3.29/3.47 fof(c0,plain,(?[X2]:((((iext(uri_rdf_type,uri_ex_c,uri_owl_Class)&iext(uri_owl_complementOf,uri_ex_c,X2))&iext(uri_rdf_type,X2,uri_owl_Restriction))&iext(uri_owl_onProperty,X2,uri_rdf_type))&iext(uri_owl_hasSelf,X2,literal_typed(dat_str_true,uri_xsd_boolean)))),inference(variable_rename,[status(thm)],[testcase_premise_fullish_030_Bad_Class])).
% 3.29/3.47 fof(c1,plain,((((iext(uri_rdf_type,uri_ex_c,uri_owl_Class)&iext(uri_owl_complementOf,uri_ex_c,skolem0001))&iext(uri_rdf_type,skolem0001,uri_owl_Restriction))&iext(uri_owl_onProperty,skolem0001,uri_rdf_type))&iext(uri_owl_hasSelf,skolem0001,literal_typed(dat_str_true,uri_xsd_boolean))),inference(skolemize,[status(esa)],[c0])).
% 3.29/3.47 cnf(c2,plain,iext(uri_rdf_type,uri_ex_c,uri_owl_Class),inference(split_conjunct,[status(thm)],[c1])).
% 3.29/3.47 fof(rdfs_range_main,axiom,(![P]:(![C]:(![X]:(![Y]:((iext(uri_rdfs_range,P,C)&iext(P,X,Y))=>icext(C,Y)))))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_range_main)).
% 3.29/3.47 fof(c48,plain,(![P]:(![C]:(![X]:(![Y]:((~iext(uri_rdfs_range,P,C)|~iext(P,X,Y))|icext(C,Y)))))),inference(fof_nnf,[status(thm)],[rdfs_range_main])).
% 3.29/3.47 fof(c49,plain,(![X18]:(![X19]:(![X20]:(![X21]:((~iext(uri_rdfs_range,X18,X19)|~iext(X18,X20,X21))|icext(X19,X21)))))),inference(variable_rename,[status(thm)],[c48])).
% 3.29/3.47 cnf(c50,plain,~iext(uri_rdfs_range,X80,X81)|~iext(X80,X79,X78)|icext(X81,X78),inference(split_conjunct,[status(thm)],[c49])).
% 3.29/3.47 cnf(c273,plain,~iext(uri_rdfs_range,uri_rdf_type,X187)|icext(X187,uri_owl_Class),inference(resolution,[status(thm)],[c50, c2])).
% 3.29/3.47 cnf(c1152,plain,icext(uri_rdfs_Class,uri_owl_Class),inference(resolution,[status(thm)],[c273, c9])).
% 3.29/3.47 cnf(c1154,plain,ic(uri_owl_Class),inference(resolution,[status(thm)],[c1152, c70])).
% 3.29/3.47 cnf(c1157,plain,iext(uri_rdfs_subClassOf,uri_owl_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1154, c108])).
% 3.29/3.47 cnf(c1201,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X633)|iext(X633,uri_owl_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1157, c24])).
% 3.29/3.47 fof(rdfs_subclassof_trans,axiom,(![C]:(![D]:(![E]:((iext(uri_rdfs_subClassOf,C,D)&iext(uri_rdfs_subClassOf,D,E))=>iext(uri_rdfs_subClassOf,C,E))))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_subclassof_trans)).
% 3.29/3.47 fof(c26,plain,(![C]:(![D]:(![E]:((~iext(uri_rdfs_subClassOf,C,D)|~iext(uri_rdfs_subClassOf,D,E))|iext(uri_rdfs_subClassOf,C,E))))),inference(fof_nnf,[status(thm)],[rdfs_subclassof_trans])).
% 3.29/3.47 fof(c27,plain,(![X11]:(![X12]:(![X13]:((~iext(uri_rdfs_subClassOf,X11,X12)|~iext(uri_rdfs_subClassOf,X12,X13))|iext(uri_rdfs_subClassOf,X11,X13))))),inference(variable_rename,[status(thm)],[c26])).
% 3.29/3.47 cnf(c28,plain,~iext(uri_rdfs_subClassOf,X69,X67)|~iext(uri_rdfs_subClassOf,X67,X68)|iext(uri_rdfs_subClassOf,X69,X68),inference(split_conjunct,[status(thm)],[c27])).
% 3.29/3.47 cnf(c1198,plain,~iext(uri_rdfs_subClassOf,X632,uri_owl_Class)|iext(uri_rdfs_subClassOf,X632,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1157, c28])).
% 3.29/3.47 fof(rdfs_subclassof_reflex,axiom,(![C]:(ic(C)=>iext(uri_rdfs_subClassOf,C,C))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_subclassof_reflex)).
% 3.29/3.47 fof(c29,plain,(![C]:(~ic(C)|iext(uri_rdfs_subClassOf,C,C))),inference(fof_nnf,[status(thm)],[rdfs_subclassof_reflex])).
% 3.29/3.47 fof(c30,plain,(![X14]:(~ic(X14)|iext(uri_rdfs_subClassOf,X14,X14))),inference(variable_rename,[status(thm)],[c29])).
% 3.29/3.47 cnf(c31,plain,~ic(X70)|iext(uri_rdfs_subClassOf,X70,X70),inference(split_conjunct,[status(thm)],[c30])).
% 3.29/3.47 cnf(c1156,plain,iext(uri_rdfs_subClassOf,uri_owl_Class,uri_owl_Class),inference(resolution,[status(thm)],[c1154, c31])).
% 3.29/3.47 cnf(c1193,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X631)|iext(X631,uri_owl_Class,uri_owl_Class),inference(resolution,[status(thm)],[c1156, c24])).
% 3.29/3.47 cnf(c1153,plain,iext(uri_rdf_type,uri_owl_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c1152, c114])).
% 3.29/3.47 cnf(c1184,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X629)|iext(X629,uri_owl_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c1153, c24])).
% 3.29/3.47 fof(rdfs_range_range,axiom,iext(uri_rdfs_range,uri_rdfs_range,uri_rdfs_Class),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_range_range)).
% 3.29/3.47 cnf(c47,plain,iext(uri_rdfs_range,uri_rdfs_range,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_range_range])).
% 3.29/3.47 fof(rdfs_collection_rest_range,axiom,iext(uri_rdfs_range,uri_rdf_rest,uri_rdf_List),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_collection_rest_range)).
% 3.29/3.47 cnf(c102,plain,iext(uri_rdfs_range,uri_rdf_rest,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdfs_collection_rest_range])).
% 3.29/3.47 cnf(c255,plain,~iext(uri_rdfs_range,uri_rdfs_range,X169)|icext(X169,uri_rdf_List),inference(resolution,[status(thm)],[c50, c102])).
% 3.29/3.47 cnf(c1097,plain,icext(uri_rdfs_Class,uri_rdf_List),inference(resolution,[status(thm)],[c255, c47])).
% 3.29/3.47 cnf(c1099,plain,ic(uri_rdf_List),inference(resolution,[status(thm)],[c1097, c70])).
% 3.29/3.47 cnf(c1102,plain,iext(uri_rdfs_subClassOf,uri_rdf_List,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1099, c108])).
% 3.29/3.47 cnf(c1179,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X628)|iext(X628,uri_rdf_List,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1102, c24])).
% 3.29/3.47 cnf(c1176,plain,~iext(uri_rdfs_subClassOf,X627,uri_rdf_List)|iext(uri_rdfs_subClassOf,X627,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1102, c28])).
% 3.29/3.47 cnf(c1101,plain,iext(uri_rdfs_subClassOf,uri_rdf_List,uri_rdf_List),inference(resolution,[status(thm)],[c1099, c31])).
% 3.29/3.47 cnf(c1171,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X626)|iext(X626,uri_rdf_List,uri_rdf_List),inference(resolution,[status(thm)],[c1101, c24])).
% 3.29/3.47 cnf(c1098,plain,iext(uri_rdf_type,uri_rdf_List,uri_rdfs_Class),inference(resolution,[status(thm)],[c1097, c114])).
% 3.29/3.47 cnf(c1163,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X624)|iext(X624,uri_rdf_List,uri_rdfs_Class),inference(resolution,[status(thm)],[c1098, c24])).
% 3.29/3.47 cnf(c4,plain,iext(uri_rdf_type,skolem0001,uri_owl_Restriction),inference(split_conjunct,[status(thm)],[c1])).
% 3.29/3.47 cnf(c248,plain,~iext(uri_rdfs_range,uri_rdf_type,X162)|icext(X162,uri_owl_Restriction),inference(resolution,[status(thm)],[c50, c4])).
% 3.29/3.47 cnf(c1037,plain,icext(uri_rdfs_Class,uri_owl_Restriction),inference(resolution,[status(thm)],[c248, c9])).
% 3.29/3.47 cnf(c1040,plain,ic(uri_owl_Restriction),inference(resolution,[status(thm)],[c1037, c70])).
% 3.29/3.47 cnf(c1043,plain,iext(uri_rdfs_subClassOf,uri_owl_Restriction,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1040, c108])).
% 3.29/3.47 cnf(c1151,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X623)|iext(X623,uri_owl_Restriction,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1043, c24])).
% 3.29/3.47 cnf(c1148,plain,~iext(uri_rdfs_subClassOf,X622,uri_owl_Restriction)|iext(uri_rdfs_subClassOf,X622,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1043, c28])).
% 3.29/3.47 cnf(c1042,plain,iext(uri_rdfs_subClassOf,uri_owl_Restriction,uri_owl_Restriction),inference(resolution,[status(thm)],[c1040, c31])).
% 3.29/3.47 cnf(c1142,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X621)|iext(X621,uri_owl_Restriction,uri_owl_Restriction),inference(resolution,[status(thm)],[c1042, c24])).
% 3.29/3.47 cnf(c1039,plain,iext(uri_rdf_type,uri_owl_Restriction,uri_rdfs_Class),inference(resolution,[status(thm)],[c1037, c114])).
% 3.29/3.47 cnf(c1134,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X619)|iext(X619,uri_owl_Restriction,uri_rdfs_Class),inference(resolution,[status(thm)],[c1039, c24])).
% 3.29/3.47 fof(rdfs_domain_range,axiom,iext(uri_rdfs_range,uri_rdfs_domain,uri_rdfs_Class),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_domain_range)).
% 3.29/3.47 cnf(c71,plain,iext(uri_rdfs_range,uri_rdfs_domain,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_domain_range])).
% 3.29/3.47 cnf(c247,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X161)|icext(X161,uri_rdfs_Statement),inference(resolution,[status(thm)],[c50, c44])).
% 3.29/3.47 cnf(c1025,plain,icext(uri_rdfs_Class,uri_rdfs_Statement),inference(resolution,[status(thm)],[c247, c71])).
% 3.29/3.47 cnf(c1027,plain,ic(uri_rdfs_Statement),inference(resolution,[status(thm)],[c1025, c70])).
% 3.29/3.47 cnf(c1030,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Statement,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1027, c108])).
% 3.29/3.47 cnf(c1128,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X618)|iext(X618,uri_rdfs_Statement,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1030, c24])).
% 3.29/3.47 cnf(c1125,plain,~iext(uri_rdfs_subClassOf,X617,uri_rdfs_Statement)|iext(uri_rdfs_subClassOf,X617,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1030, c28])).
% 3.29/3.47 cnf(c1029,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Statement,uri_rdfs_Statement),inference(resolution,[status(thm)],[c1027, c31])).
% 3.29/3.47 cnf(c1120,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X616)|iext(X616,uri_rdfs_Statement,uri_rdfs_Statement),inference(resolution,[status(thm)],[c1029, c24])).
% 3.29/3.47 cnf(c1026,plain,iext(uri_rdf_type,uri_rdfs_Statement,uri_rdfs_Class),inference(resolution,[status(thm)],[c1025, c114])).
% 3.29/3.47 cnf(c1112,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X614)|iext(X614,uri_rdfs_Statement,uri_rdfs_Class),inference(resolution,[status(thm)],[c1026, c24])).
% 3.29/3.47 cnf(c23,plain,~iext(uri_rdfs_subPropertyOf,X61,X62)|ip(X62),inference(split_conjunct,[status(thm)],[c21])).
% 3.29/3.47 fof(rdfs_container_containermembershipproperty_instsub_member,axiom,(![P]:(icext(uri_rdfs_ContainerMembershipProperty,P)=>iext(uri_rdfs_subPropertyOf,P,uri_rdfs_member))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_containermembershipproperty_instsub_member)).
% 3.29/3.47 fof(c97,plain,(![P]:(~icext(uri_rdfs_ContainerMembershipProperty,P)|iext(uri_rdfs_subPropertyOf,P,uri_rdfs_member))),inference(fof_nnf,[status(thm)],[rdfs_container_containermembershipproperty_instsub_member])).
% 3.29/3.47 fof(c98,plain,(![X33]:(~icext(uri_rdfs_ContainerMembershipProperty,X33)|iext(uri_rdfs_subPropertyOf,X33,uri_rdfs_member))),inference(variable_rename,[status(thm)],[c97])).
% 3.29/3.47 cnf(c99,plain,~icext(uri_rdfs_ContainerMembershipProperty,X87)|iext(uri_rdfs_subPropertyOf,X87,uri_rdfs_member),inference(split_conjunct,[status(thm)],[c98])).
% 3.29/3.47 fof(rdfs_container_n_type_003,axiom,iext(uri_rdf_type,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_type_003)).
% 3.29/3.47 cnf(c85,plain,iext(uri_rdf_type,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),inference(split_conjunct,[status(thm)],[rdfs_container_n_type_003])).
% 3.29/3.47 cnf(c113,plain,~iext(uri_rdf_type,X90,X89)|icext(X89,X90),inference(split_conjunct,[status(thm)],[c112])).
% 3.29/3.47 cnf(c375,plain,icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__3),inference(resolution,[status(thm)],[c113, c85])).
% 3.29/3.47 cnf(c383,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__3,uri_rdfs_member),inference(resolution,[status(thm)],[c375, c99])).
% 3.29/3.47 cnf(c761,plain,ip(uri_rdfs_member),inference(resolution,[status(thm)],[c383, c23])).
% 3.29/3.47 cnf(c765,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_member,uri_rdfs_member),inference(resolution,[status(thm)],[c761, c16])).
% 3.29/3.47 cnf(c1096,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X613)|iext(X613,uri_rdfs_member,uri_rdfs_member),inference(resolution,[status(thm)],[c765, c24])).
% 3.29/3.47 cnf(c131,plain,~ip(X96)|iext(uri_rdf_type,X96,uri_rdf_Property),inference(split_conjunct,[status(thm)],[c129])).
% 3.29/3.47 cnf(c764,plain,iext(uri_rdf_type,uri_rdfs_member,uri_rdf_Property),inference(resolution,[status(thm)],[c761, c131])).
% 3.29/3.47 cnf(c1087,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X611)|iext(X611,uri_rdfs_member,uri_rdf_Property),inference(resolution,[status(thm)],[c764, c24])).
% 3.29/3.47 cnf(c69,plain,~ic(X59)|icext(uri_rdfs_Class,X59),inference(split_conjunct,[status(thm)],[c68])).
% 3.29/3.47 fof(rdfs_subclassof_main,axiom,(![C]:(![D]:(iext(uri_rdfs_subClassOf,C,D)=>((ic(C)&ic(D))&(![X]:(icext(C,X)=>icext(D,X))))))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_subclassof_main)).
% 3.29/3.47 fof(c33,plain,(![C]:(![D]:(~iext(uri_rdfs_subClassOf,C,D)|((ic(C)&ic(D))&(![X]:(~icext(C,X)|icext(D,X))))))),inference(fof_nnf,[status(thm)],[rdfs_subclassof_main])).
% 3.29/3.47 fof(c35,plain,(![X15]:(![X16]:(![X17]:(~iext(uri_rdfs_subClassOf,X15,X16)|((ic(X15)&ic(X16))&(~icext(X15,X17)|icext(X16,X17))))))),inference(shift_quantors,[status(thm)],[fof(c34,plain,(![X15]:(![X16]:(~iext(uri_rdfs_subClassOf,X15,X16)|((ic(X15)&ic(X16))&(![X17]:(~icext(X15,X17)|icext(X16,X17))))))),inference(variable_rename,[status(thm)],[c33])).])).
% 3.29/3.47 fof(c36,plain,(![X15]:(![X16]:(![X17]:(((~iext(uri_rdfs_subClassOf,X15,X16)|ic(X15))&(~iext(uri_rdfs_subClassOf,X15,X16)|ic(X16)))&(~iext(uri_rdfs_subClassOf,X15,X16)|(~icext(X15,X17)|icext(X16,X17))))))),inference(distribute,[status(thm)],[c35])).
% 3.29/3.47 cnf(c38,plain,~iext(uri_rdfs_subClassOf,X73,X74)|ic(X74),inference(split_conjunct,[status(thm)],[c36])).
% 3.29/3.47 fof(rdfs_container_bag_sub,axiom,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Container),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_bag_sub)).
% 3.29/3.47 cnf(c100,plain,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Container),inference(split_conjunct,[status(thm)],[rdfs_container_bag_sub])).
% 3.29/3.47 cnf(c37,plain,~iext(uri_rdfs_subClassOf,X71,X72)|ic(X71),inference(split_conjunct,[status(thm)],[c36])).
% 3.29/3.47 cnf(c207,plain,ic(uri_rdf_Bag),inference(resolution,[status(thm)],[c37, c100])).
% 3.29/3.47 cnf(c346,plain,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Resource),inference(resolution,[status(thm)],[c108, c207])).
% 3.29/3.47 cnf(c663,plain,ic(uri_rdfs_Resource),inference(resolution,[status(thm)],[c346, c38])).
% 3.29/3.47 cnf(c666,plain,icext(uri_rdfs_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c663, c69])).
% 3.29/3.47 cnf(c669,plain,iext(uri_rdf_type,uri_rdfs_Resource,uri_rdfs_Class),inference(resolution,[status(thm)],[c666, c114])).
% 3.29/3.47 cnf(c1081,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X610)|iext(X610,uri_rdfs_Resource,uri_rdfs_Class),inference(resolution,[status(thm)],[c669, c24])).
% 3.29/3.47 cnf(c667,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Resource,uri_rdfs_Resource),inference(resolution,[status(thm)],[c663, c31])).
% 3.29/3.47 cnf(c1076,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X609)|iext(X609,uri_rdfs_Resource,uri_rdfs_Resource),inference(resolution,[status(thm)],[c667, c24])).
% 3.29/3.47 fof(rdfs_annotation_isdefinedby_sub,axiom,iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_isdefinedby_sub)).
% 3.29/3.47 cnf(c119,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_sub])).
% 3.29/3.47 fof(simple_iext_property,axiom,(![S]:(![P]:(![O]:(iext(P,S,O)=>ip(P))))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', simple_iext_property)).
% 3.29/3.47 fof(c146,plain,(![S]:(![P]:(![O]:(~iext(P,S,O)|ip(P))))),inference(fof_nnf,[status(thm)],[simple_iext_property])).
% 3.29/3.47 fof(c147,plain,(![S]:(![P]:((![O]:~iext(P,S,O))|ip(P)))),inference(shift_quantors,[status(thm)],[c146])).
% 3.29/3.47 fof(c149,plain,(![X43]:(![X44]:(![X45]:(~iext(X44,X43,X45)|ip(X44))))),inference(shift_quantors,[status(thm)],[fof(c148,plain,(![X43]:(![X44]:((![X45]:~iext(X44,X43,X45))|ip(X44)))),inference(variable_rename,[status(thm)],[c147])).])).
% 3.29/3.47 cnf(c150,plain,~iext(X99,X97,X98)|ip(X99),inference(split_conjunct,[status(thm)],[c149])).
% 3.29/3.47 cnf(c558,plain,ip(uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c150, c119])).
% 3.29/3.47 cnf(c576,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c558, c16])).
% 3.29/3.47 cnf(c1068,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X607)|iext(X607,uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c576, c24])).
% 3.29/3.47 cnf(c575,plain,iext(uri_rdf_type,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c558, c131])).
% 3.29/3.47 cnf(c1058,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X605)|iext(X605,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c575, c24])).
% 3.29/3.47 cnf(c6,plain,iext(uri_owl_hasSelf,skolem0001,literal_typed(dat_str_true,uri_xsd_boolean)),inference(split_conjunct,[status(thm)],[c1])).
% 3.29/3.47 cnf(c528,plain,ip(uri_owl_hasSelf),inference(resolution,[status(thm)],[c150, c6])).
% 3.29/3.47 cnf(c574,plain,iext(uri_rdfs_subPropertyOf,uri_owl_hasSelf,uri_owl_hasSelf),inference(resolution,[status(thm)],[c528, c16])).
% 3.29/3.47 cnf(c1051,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X604)|iext(X604,uri_owl_hasSelf,uri_owl_hasSelf),inference(resolution,[status(thm)],[c574, c24])).
% 3.29/3.47 cnf(c573,plain,iext(uri_rdf_type,uri_owl_hasSelf,uri_rdf_Property),inference(resolution,[status(thm)],[c528, c131])).
% 3.29/3.47 cnf(c1036,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X602)|iext(X602,uri_owl_hasSelf,uri_rdf_Property),inference(resolution,[status(thm)],[c573, c24])).
% 3.29/3.47 fof(rdfs_datatype_sub,axiom,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Class),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_datatype_sub)).
% 3.29/3.47 cnf(c78,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_datatype_sub])).
% 3.29/3.47 cnf(c518,plain,ip(uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c150, c78])).
% 3.29/3.47 cnf(c572,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c518, c16])).
% 3.29/3.47 cnf(c1023,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X601)|iext(X601,uri_rdfs_subClassOf,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c572, c24])).
% 3.29/3.47 cnf(c571,plain,iext(uri_rdf_type,uri_rdfs_subClassOf,uri_rdf_Property),inference(resolution,[status(thm)],[c518, c131])).
% 3.29/3.47 cnf(c1010,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X599)|iext(X599,uri_rdfs_subClassOf,uri_rdf_Property),inference(resolution,[status(thm)],[c571, c24])).
% 3.29/3.47 cnf(c505,plain,ip(uri_rdfs_range),inference(resolution,[status(thm)],[c150, c47])).
% 3.29/3.47 cnf(c570,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_range,uri_rdfs_range),inference(resolution,[status(thm)],[c505, c16])).
% 3.29/3.47 cnf(c1001,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X598)|iext(X598,uri_rdfs_range,uri_rdfs_range),inference(resolution,[status(thm)],[c570, c24])).
% 3.29/3.47 cnf(c569,plain,iext(uri_rdf_type,uri_rdfs_range,uri_rdf_Property),inference(resolution,[status(thm)],[c505, c131])).
% 3.29/3.47 cnf(c982,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X596)|iext(X596,uri_rdfs_range,uri_rdf_Property),inference(resolution,[status(thm)],[c569, c24])).
% 3.29/3.47 cnf(c3,plain,iext(uri_owl_complementOf,uri_ex_c,skolem0001),inference(split_conjunct,[status(thm)],[c1])).
% 3.29/3.47 cnf(c504,plain,ip(uri_owl_complementOf),inference(resolution,[status(thm)],[c150, c3])).
% 3.29/3.47 cnf(c568,plain,iext(uri_rdfs_subPropertyOf,uri_owl_complementOf,uri_owl_complementOf),inference(resolution,[status(thm)],[c504, c16])).
% 3.29/3.47 cnf(c975,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X595)|iext(X595,uri_owl_complementOf,uri_owl_complementOf),inference(resolution,[status(thm)],[c568, c24])).
% 3.29/3.47 cnf(c567,plain,iext(uri_rdf_type,uri_owl_complementOf,uri_rdf_Property),inference(resolution,[status(thm)],[c504, c131])).
% 3.29/3.47 cnf(c966,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X593)|iext(X593,uri_owl_complementOf,uri_rdf_Property),inference(resolution,[status(thm)],[c567, c24])).
% 3.29/3.47 fof(rdfs_container_n_domain_003,axiom,iext(uri_rdfs_domain,uri_rdf__3,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_domain_003)).
% 3.29/3.47 cnf(c91,plain,iext(uri_rdfs_domain,uri_rdf__3,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_003])).
% 3.29/3.47 cnf(c499,plain,ip(uri_rdfs_domain),inference(resolution,[status(thm)],[c150, c91])).
% 3.29/3.47 cnf(c566,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,uri_rdfs_domain),inference(resolution,[status(thm)],[c499, c16])).
% 3.29/3.47 cnf(c960,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X592)|iext(X592,uri_rdfs_domain,uri_rdfs_domain),inference(resolution,[status(thm)],[c566, c24])).
% 3.29/3.47 cnf(c565,plain,iext(uri_rdf_type,uri_rdfs_domain,uri_rdf_Property),inference(resolution,[status(thm)],[c499, c131])).
% 3.29/3.47 cnf(c936,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X590)|iext(X590,uri_rdfs_domain,uri_rdf_Property),inference(resolution,[status(thm)],[c565, c24])).
% 3.29/3.47 cnf(c5,plain,iext(uri_owl_onProperty,skolem0001,uri_rdf_type),inference(split_conjunct,[status(thm)],[c1])).
% 3.29/3.47 cnf(c498,plain,ip(uri_owl_onProperty),inference(resolution,[status(thm)],[c150, c5])).
% 3.29/3.47 cnf(c564,plain,iext(uri_rdfs_subPropertyOf,uri_owl_onProperty,uri_owl_onProperty),inference(resolution,[status(thm)],[c498, c16])).
% 3.29/3.47 cnf(c930,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X589)|iext(X589,uri_owl_onProperty,uri_owl_onProperty),inference(resolution,[status(thm)],[c564, c24])).
% 3.29/3.47 cnf(c563,plain,iext(uri_rdf_type,uri_owl_onProperty,uri_rdf_Property),inference(resolution,[status(thm)],[c498, c131])).
% 3.29/3.47 cnf(c921,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X587)|iext(X587,uri_owl_onProperty,uri_rdf_Property),inference(resolution,[status(thm)],[c563, c24])).
% 3.29/3.47 fof(rdf_collection_first_type,axiom,iext(uri_rdf_type,uri_rdf_first,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdf_collection_first_type)).
% 3.29/3.47 cnf(c140,plain,iext(uri_rdf_type,uri_rdf_first,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_collection_first_type])).
% 3.29/3.47 cnf(c493,plain,ip(uri_rdf_first),inference(resolution,[status(thm)],[c140, c130])).
% 3.29/3.47 cnf(c497,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_first,uri_rdf_first),inference(resolution,[status(thm)],[c493, c16])).
% 3.29/3.47 cnf(c915,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X586)|iext(X586,uri_rdf_first,uri_rdf_first),inference(resolution,[status(thm)],[c497, c24])).
% 3.29/3.47 fof(rdf_collection_rest_type,axiom,iext(uri_rdf_type,uri_rdf_rest,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdf_collection_rest_type)).
% 3.29/3.47 cnf(c138,plain,iext(uri_rdf_type,uri_rdf_rest,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_collection_rest_type])).
% 3.29/3.47 cnf(c480,plain,ip(uri_rdf_rest),inference(resolution,[status(thm)],[c138, c130])).
% 3.29/3.47 cnf(c488,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_rest,uri_rdf_rest),inference(resolution,[status(thm)],[c480, c16])).
% 3.29/3.47 cnf(c907,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X584)|iext(X584,uri_rdf_rest,uri_rdf_rest),inference(resolution,[status(thm)],[c488, c24])).
% 3.29/3.47 fof(rdf_container_n_type_001,axiom,iext(uri_rdf_type,uri_rdf__1,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdf_container_n_type_001)).
% 3.29/3.47 cnf(c137,plain,iext(uri_rdf_type,uri_rdf__1,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_container_n_type_001])).
% 3.29/3.47 cnf(c469,plain,ip(uri_rdf__1),inference(resolution,[status(thm)],[c137, c130])).
% 3.29/3.47 cnf(c475,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__1,uri_rdf__1),inference(resolution,[status(thm)],[c469, c16])).
% 3.29/3.47 cnf(c900,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X582)|iext(X582,uri_rdf__1,uri_rdf__1),inference(resolution,[status(thm)],[c475, c24])).
% 3.29/3.47 fof(rdf_container_n_type_002,axiom,iext(uri_rdf_type,uri_rdf__2,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdf_container_n_type_002)).
% 3.29/3.47 cnf(c136,plain,iext(uri_rdf_type,uri_rdf__2,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_container_n_type_002])).
% 3.29/3.47 cnf(c464,plain,ip(uri_rdf__2),inference(resolution,[status(thm)],[c136, c130])).
% 3.29/3.47 cnf(c473,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__2,uri_rdf__2),inference(resolution,[status(thm)],[c464, c16])).
% 3.29/3.47 cnf(c892,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X580)|iext(X580,uri_rdf__2,uri_rdf__2),inference(resolution,[status(thm)],[c473, c24])).
% 3.29/3.47 fof(rdf_container_n_type_003,axiom,iext(uri_rdf_type,uri_rdf__3,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdf_container_n_type_003)).
% 3.29/3.47 cnf(c135,plain,iext(uri_rdf_type,uri_rdf__3,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_container_n_type_003])).
% 3.29/3.47 cnf(c456,plain,ip(uri_rdf__3),inference(resolution,[status(thm)],[c135, c130])).
% 3.29/3.47 cnf(c460,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__3,uri_rdf__3),inference(resolution,[status(thm)],[c456, c16])).
% 3.29/3.47 cnf(c885,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X578)|iext(X578,uri_rdf__3,uri_rdf__3),inference(resolution,[status(thm)],[c460, c24])).
% 3.29/3.47 cnf(c368,plain,ip(uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c119, c23])).
% 3.29/3.47 cnf(c451,plain,iext(uri_rdf_type,uri_rdfs_seeAlso,uri_rdf_Property),inference(resolution,[status(thm)],[c131, c368])).
% 3.29/3.47 cnf(c876,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X576)|iext(X576,uri_rdfs_seeAlso,uri_rdf_Property),inference(resolution,[status(thm)],[c451, c24])).
% 3.29/3.47 cnf(c22,plain,~iext(uri_rdfs_subPropertyOf,X55,X56)|ip(X55),inference(split_conjunct,[status(thm)],[c21])).
% 3.29/3.47 cnf(c372,plain,ip(uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c119, c22])).
% 3.29/3.47 cnf(c450,plain,iext(uri_rdf_type,uri_rdfs_isDefinedBy,uri_rdf_Property),inference(resolution,[status(thm)],[c131, c372])).
% 3.29/3.47 cnf(c869,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X575)|iext(X575,uri_rdfs_isDefinedBy,uri_rdf_Property),inference(resolution,[status(thm)],[c450, c24])).
% 3.29/3.47 fof(rdf_reification_object_type,axiom,iext(uri_rdf_type,uri_rdf_object,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdf_reification_object_type)).
% 3.29/3.47 cnf(c134,plain,iext(uri_rdf_type,uri_rdf_object,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_reification_object_type])).
% 3.29/3.47 cnf(c443,plain,ip(uri_rdf_object),inference(resolution,[status(thm)],[c134, c130])).
% 3.29/3.47 cnf(c446,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_object,uri_rdf_object),inference(resolution,[status(thm)],[c443, c16])).
% 3.29/3.47 cnf(c862,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X574)|iext(X574,uri_rdf_object,uri_rdf_object),inference(resolution,[status(thm)],[c446, c24])).
% 3.29/3.47 fof(rdf_reification_subject_type,axiom,iext(uri_rdf_type,uri_rdf_subject,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdf_reification_subject_type)).
% 3.29/3.47 cnf(c132,plain,iext(uri_rdf_type,uri_rdf_subject,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_reification_subject_type])).
% 3.29/3.47 cnf(c437,plain,ip(uri_rdf_subject),inference(resolution,[status(thm)],[c130, c132])).
% 3.29/3.47 cnf(c440,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_subject,uri_rdf_subject),inference(resolution,[status(thm)],[c437, c16])).
% 3.29/3.47 cnf(c855,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X572)|iext(X572,uri_rdf_subject,uri_rdf_subject),inference(resolution,[status(thm)],[c440, c24])).
% 3.29/3.47 fof(rdf_reification_predicate_type,axiom,iext(uri_rdf_type,uri_rdf_value,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdf_reification_predicate_type)).
% 3.29/3.47 cnf(c133,plain,iext(uri_rdf_type,uri_rdf_value,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_reification_predicate_type])).
% 3.29/3.47 cnf(c436,plain,ip(uri_rdf_value),inference(resolution,[status(thm)],[c130, c133])).
% 3.29/3.47 cnf(c439,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_value,uri_rdf_value),inference(resolution,[status(thm)],[c436, c16])).
% 3.29/3.47 cnf(c848,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X570)|iext(X570,uri_rdf_value,uri_rdf_value),inference(resolution,[status(thm)],[c439, c24])).
% 3.29/3.47 fof(rdf_value_type,axiom,iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdf_value_type)).
% 3.29/3.47 cnf(c124,plain,iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_value_type])).
% 3.29/3.47 cnf(c435,plain,ip(uri_rdf_type),inference(resolution,[status(thm)],[c130, c124])).
% 3.29/3.47 cnf(c438,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_type,uri_rdf_type),inference(resolution,[status(thm)],[c435, c16])).
% 3.29/3.47 cnf(c840,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X568)|iext(X568,uri_rdf_type,uri_rdf_type),inference(resolution,[status(thm)],[c438, c24])).
% 3.29/3.47 fof(rdfs_container_n_type_001,axiom,iext(uri_rdf_type,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_type_001)).
% 3.29/3.47 cnf(c87,plain,iext(uri_rdf_type,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),inference(split_conjunct,[status(thm)],[rdfs_container_n_type_001])).
% 3.29/3.47 cnf(c380,plain,icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__1),inference(resolution,[status(thm)],[c113, c87])).
% 3.29/3.47 cnf(c403,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__1,uri_rdfs_member),inference(resolution,[status(thm)],[c380, c99])).
% 3.29/3.47 cnf(c827,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X566)|iext(X566,uri_rdf__1,uri_rdfs_member),inference(resolution,[status(thm)],[c403, c24])).
% 3.29/3.47 fof(rdfs_subpropertyof_trans,axiom,(![P]:(![Q]:(![R]:((iext(uri_rdfs_subPropertyOf,P,Q)&iext(uri_rdfs_subPropertyOf,Q,R))=>iext(uri_rdfs_subPropertyOf,P,R))))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_subpropertyof_trans)).
% 3.29/3.47 fof(c11,plain,(![P]:(![Q]:(![R]:((~iext(uri_rdfs_subPropertyOf,P,Q)|~iext(uri_rdfs_subPropertyOf,Q,R))|iext(uri_rdfs_subPropertyOf,P,R))))),inference(fof_nnf,[status(thm)],[rdfs_subpropertyof_trans])).
% 3.29/3.47 fof(c12,plain,(![X3]:(![X4]:(![X5]:((~iext(uri_rdfs_subPropertyOf,X3,X4)|~iext(uri_rdfs_subPropertyOf,X4,X5))|iext(uri_rdfs_subPropertyOf,X3,X5))))),inference(variable_rename,[status(thm)],[c11])).
% 3.29/3.47 cnf(c13,plain,~iext(uri_rdfs_subPropertyOf,X48,X50)|~iext(uri_rdfs_subPropertyOf,X50,X49)|iext(uri_rdfs_subPropertyOf,X48,X49),inference(split_conjunct,[status(thm)],[c12])).
% 3.29/3.47 cnf(c826,plain,~iext(uri_rdfs_subPropertyOf,X565,uri_rdf__1)|iext(uri_rdfs_subPropertyOf,X565,uri_rdfs_member),inference(resolution,[status(thm)],[c403, c13])).
% 3.29/3.47 fof(rdfs_container_n_type_002,axiom,iext(uri_rdf_type,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_type_002)).
% 3.29/3.47 cnf(c86,plain,iext(uri_rdf_type,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),inference(split_conjunct,[status(thm)],[rdfs_container_n_type_002])).
% 3.29/3.47 cnf(c379,plain,icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__2),inference(resolution,[status(thm)],[c113, c86])).
% 3.29/3.47 cnf(c401,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__2,uri_rdfs_member),inference(resolution,[status(thm)],[c379, c99])).
% 3.29/3.47 cnf(c820,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X564)|iext(X564,uri_rdf__2,uri_rdfs_member),inference(resolution,[status(thm)],[c401, c24])).
% 3.29/3.47 cnf(c819,plain,~iext(uri_rdfs_subPropertyOf,X563,uri_rdf__2)|iext(uri_rdfs_subPropertyOf,X563,uri_rdfs_member),inference(resolution,[status(thm)],[c401, c13])).
% 3.29/3.47 cnf(c219,plain,ic(uri_rdfs_Class),inference(resolution,[status(thm)],[c38, c78])).
% 3.29/3.47 cnf(c227,plain,icext(uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c219, c69])).
% 3.29/3.47 cnf(c396,plain,iext(uri_rdf_type,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c114, c227])).
% 3.29/3.47 cnf(c812,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X562)|iext(X562,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c396, c24])).
% 3.29/3.47 fof(rdfs_dat_xmlliteral_sub,axiom,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Literal),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_dat_xmlliteral_sub)).
% 3.29/3.47 cnf(c83,plain,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[rdfs_dat_xmlliteral_sub])).
% 3.29/3.47 cnf(c220,plain,ic(uri_rdfs_Literal),inference(resolution,[status(thm)],[c38, c83])).
% 3.29/3.47 cnf(c229,plain,icext(uri_rdfs_Class,uri_rdfs_Literal),inference(resolution,[status(thm)],[c220, c69])).
% 3.29/3.47 cnf(c395,plain,iext(uri_rdf_type,uri_rdfs_Literal,uri_rdfs_Class),inference(resolution,[status(thm)],[c114, c229])).
% 3.29/3.47 cnf(c806,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X561)|iext(X561,uri_rdfs_Literal,uri_rdfs_Class),inference(resolution,[status(thm)],[c395, c24])).
% 3.29/3.47 cnf(c217,plain,icext(uri_rdfs_Class,uri_rdf_Bag),inference(resolution,[status(thm)],[c207, c69])).
% 3.29/3.47 cnf(c394,plain,iext(uri_rdf_type,uri_rdf_Bag,uri_rdfs_Class),inference(resolution,[status(thm)],[c114, c217])).
% 3.29/3.47 cnf(c801,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X560)|iext(X560,uri_rdf_Bag,uri_rdfs_Class),inference(resolution,[status(thm)],[c394, c24])).
% 3.29/3.47 cnf(c203,plain,ic(uri_rdfs_Datatype),inference(resolution,[status(thm)],[c37, c78])).
% 3.29/3.47 cnf(c209,plain,icext(uri_rdfs_Class,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c203, c69])).
% 3.29/3.47 cnf(c393,plain,iext(uri_rdf_type,uri_rdfs_Datatype,uri_rdfs_Class),inference(resolution,[status(thm)],[c114, c209])).
% 3.29/3.47 cnf(c795,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X559)|iext(X559,uri_rdfs_Datatype,uri_rdfs_Class),inference(resolution,[status(thm)],[c393, c24])).
% 3.29/3.47 fof(rdfs_container_seq_sub,axiom,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Container),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_seq_sub)).
% 3.29/3.47 cnf(c84,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Container),inference(split_conjunct,[status(thm)],[rdfs_container_seq_sub])).
% 3.29/3.47 cnf(c221,plain,ic(uri_rdfs_Container),inference(resolution,[status(thm)],[c38, c84])).
% 3.29/3.47 cnf(c231,plain,icext(uri_rdfs_Class,uri_rdfs_Container),inference(resolution,[status(thm)],[c221, c69])).
% 3.29/3.47 cnf(c391,plain,iext(uri_rdf_type,uri_rdfs_Container,uri_rdfs_Class),inference(resolution,[status(thm)],[c114, c231])).
% 3.29/3.47 cnf(c790,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X558)|iext(X558,uri_rdfs_Container,uri_rdfs_Class),inference(resolution,[status(thm)],[c391, c24])).
% 3.29/3.47 fof(rdfs_container_alt_sub,axiom,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Container),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_alt_sub)).
% 3.29/3.47 cnf(c101,plain,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Container),inference(split_conjunct,[status(thm)],[rdfs_container_alt_sub])).
% 3.29/3.47 cnf(c208,plain,ic(uri_rdf_Alt),inference(resolution,[status(thm)],[c37, c101])).
% 3.29/3.47 cnf(c225,plain,icext(uri_rdfs_Class,uri_rdf_Alt),inference(resolution,[status(thm)],[c208, c69])).
% 3.29/3.47 cnf(c390,plain,iext(uri_rdf_type,uri_rdf_Alt,uri_rdfs_Class),inference(resolution,[status(thm)],[c114, c225])).
% 3.29/3.47 cnf(c785,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X557)|iext(X557,uri_rdf_Alt,uri_rdfs_Class),inference(resolution,[status(thm)],[c390, c24])).
% 3.29/3.47 cnf(c1308,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X556)|icext(X556,uri_rdfs_comment),inference(resolution,[status(thm)],[c1300, c50])).
% 3.29/3.47 cnf(c205,plain,ic(uri_rdfs_Seq),inference(resolution,[status(thm)],[c37, c84])).
% 3.29/3.47 cnf(c213,plain,icext(uri_rdfs_Class,uri_rdfs_Seq),inference(resolution,[status(thm)],[c205, c69])).
% 3.29/3.47 cnf(c389,plain,iext(uri_rdf_type,uri_rdfs_Seq,uri_rdfs_Class),inference(resolution,[status(thm)],[c114, c213])).
% 3.29/3.47 cnf(c780,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X555)|iext(X555,uri_rdfs_Seq,uri_rdfs_Class),inference(resolution,[status(thm)],[c389, c24])).
% 3.29/3.47 cnf(c1302,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X554)|icext(X554,uri_rdfs_comment),inference(resolution,[status(thm)],[c1300, c76])).
% 3.29/3.47 cnf(c204,plain,ic(uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c37, c83])).
% 3.29/3.47 cnf(c211,plain,icext(uri_rdfs_Class,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c204, c69])).
% 3.29/3.47 cnf(c388,plain,iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Class),inference(resolution,[status(thm)],[c114, c211])).
% 3.29/3.47 cnf(c775,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X551)|iext(X551,uri_rdf_XMLLiteral,uri_rdfs_Class),inference(resolution,[status(thm)],[c388, c24])).
% 3.29/3.47 cnf(c1280,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X550)|icext(X550,uri_rdfs_label),inference(resolution,[status(thm)],[c1272, c50])).
% 3.29/3.47 cnf(c1274,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X549)|icext(X549,uri_rdfs_label),inference(resolution,[status(thm)],[c1272, c76])).
% 3.29/3.47 fof(rdfs_container_containermembershipproperty_sub,axiom,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_containermembershipproperty_sub)).
% 3.29/3.47 cnf(c96,plain,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_container_containermembershipproperty_sub])).
% 3.29/3.47 cnf(c206,plain,ic(uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c37, c96])).
% 3.29/3.47 cnf(c215,plain,icext(uri_rdfs_Class,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c206, c69])).
% 3.29/3.47 cnf(c386,plain,iext(uri_rdf_type,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Class),inference(resolution,[status(thm)],[c114, c215])).
% 3.29/3.47 cnf(c770,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X548)|iext(X548,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Class),inference(resolution,[status(thm)],[c386, c24])).
% 3.29/3.47 cnf(c1222,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X545)|icext(X545,uri_rdf_predicate),inference(resolution,[status(thm)],[c1215, c50])).
% 3.29/3.47 cnf(c763,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X544)|iext(X544,uri_rdf__3,uri_rdfs_member),inference(resolution,[status(thm)],[c383, c24])).
% 3.29/3.47 cnf(c1216,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X543)|icext(X543,uri_rdf_predicate),inference(resolution,[status(thm)],[c1215, c76])).
% 3.29/3.47 cnf(c762,plain,~iext(uri_rdfs_subPropertyOf,X540,uri_rdf__3)|iext(uri_rdfs_subPropertyOf,X540,uri_rdfs_member),inference(resolution,[status(thm)],[c383, c13])).
% 3.29/3.47 cnf(c1188,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X537)|icext(X537,uri_owl_Class),inference(resolution,[status(thm)],[c1156, c76])).
% 3.29/3.47 cnf(c382,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c372, c16])).
% 3.29/3.47 cnf(c756,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X536)|iext(X536,uri_rdfs_isDefinedBy,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c382, c24])).
% 3.29/3.47 cnf(c1187,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X535)|icext(X535,uri_owl_Class),inference(resolution,[status(thm)],[c1156, c50])).
% 3.29/3.47 cnf(c1166,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X529)|icext(X529,uri_rdf_List),inference(resolution,[status(thm)],[c1101, c76])).
% 3.29/3.47 cnf(c381,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_seeAlso,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c368, c16])).
% 3.29/3.47 cnf(c749,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X528)|iext(X528,uri_rdfs_seeAlso,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c381, c24])).
% 3.29/3.47 cnf(c1165,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X527)|icext(X527,uri_rdf_List),inference(resolution,[status(thm)],[c1101, c50])).
% 3.29/3.47 cnf(c1137,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X521)|icext(X521,uri_owl_Restriction),inference(resolution,[status(thm)],[c1042, c76])).
% 3.29/3.47 cnf(c1136,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X520)|icext(X520,uri_owl_Restriction),inference(resolution,[status(thm)],[c1042, c50])).
% 3.29/3.47 cnf(c222,plain,ic(uri_rdf_Property),inference(resolution,[status(thm)],[c38, c96])).
% 3.29/3.47 cnf(c355,plain,iext(uri_rdfs_subClassOf,uri_rdf_Property,uri_rdfs_Resource),inference(resolution,[status(thm)],[c108, c222])).
% 3.29/3.47 cnf(c742,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X519)|iext(X519,uri_rdf_Property,uri_rdfs_Resource),inference(resolution,[status(thm)],[c355, c24])).
% 3.29/3.47 cnf(c739,plain,~iext(uri_rdfs_subClassOf,X515,uri_rdf_Property)|iext(uri_rdfs_subClassOf,X515,uri_rdfs_Resource),inference(resolution,[status(thm)],[c355, c28])).
% 3.29/3.47 cnf(c1115,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X513)|icext(X513,uri_rdfs_Statement),inference(resolution,[status(thm)],[c1029, c76])).
% 3.29/3.47 cnf(c354,plain,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Resource),inference(resolution,[status(thm)],[c108, c208])).
% 3.29/3.47 cnf(c734,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X512)|iext(X512,uri_rdf_Alt,uri_rdfs_Resource),inference(resolution,[status(thm)],[c354, c24])).
% 3.29/3.47 cnf(c1114,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X511)|icext(X511,uri_rdfs_Statement),inference(resolution,[status(thm)],[c1029, c50])).
% 3.29/3.47 cnf(c731,plain,~iext(uri_rdfs_subClassOf,X508,uri_rdf_Alt)|iext(uri_rdfs_subClassOf,X508,uri_rdfs_Resource),inference(resolution,[status(thm)],[c354, c28])).
% 3.29/3.47 cnf(c1092,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X507)|icext(X507,uri_rdfs_member),inference(resolution,[status(thm)],[c765, c76])).
% 3.29/3.47 cnf(c353,plain,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Resource),inference(resolution,[status(thm)],[c108, c204])).
% 3.29/3.47 cnf(c726,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X503)|iext(X503,uri_rdf_XMLLiteral,uri_rdfs_Resource),inference(resolution,[status(thm)],[c353, c24])).
% 3.29/3.47 cnf(c1071,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X500)|icext(X500,uri_rdfs_Resource),inference(resolution,[status(thm)],[c667, c76])).
% 3.29/3.47 cnf(c723,plain,~iext(uri_rdfs_subClassOf,X499,uri_rdf_XMLLiteral)|iext(uri_rdfs_subClassOf,X499,uri_rdfs_Resource),inference(resolution,[status(thm)],[c353, c28])).
% 3.29/3.47 cnf(c1063,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X497)|icext(X497,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c576, c76])).
% 3.29/3.47 cnf(c352,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c108, c219])).
% 3.29/3.47 cnf(c718,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X496)|iext(X496,uri_rdfs_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c352, c24])).
% 3.29/3.47 cnf(c1061,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X495)|icext(X495,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c576, c50])).
% 3.29/3.47 cnf(c715,plain,~iext(uri_rdfs_subClassOf,X492,uri_rdfs_Class)|iext(uri_rdfs_subClassOf,X492,uri_rdfs_Resource),inference(resolution,[status(thm)],[c352, c28])).
% 3.29/3.47 cnf(c1046,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X491)|icext(X491,uri_owl_hasSelf),inference(resolution,[status(thm)],[c574, c76])).
% 3.29/3.47 cnf(c351,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Literal,uri_rdfs_Resource),inference(resolution,[status(thm)],[c108, c220])).
% 3.29/3.47 cnf(c710,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X490)|iext(X490,uri_rdfs_Literal,uri_rdfs_Resource),inference(resolution,[status(thm)],[c351, c24])).
% 3.29/3.47 cnf(c1044,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X489)|icext(X489,uri_owl_hasSelf),inference(resolution,[status(thm)],[c574, c50])).
% 3.29/3.47 cnf(c707,plain,~iext(uri_rdfs_subClassOf,X486,uri_rdfs_Literal)|iext(uri_rdfs_subClassOf,X486,uri_rdfs_Resource),inference(resolution,[status(thm)],[c351, c28])).
% 3.29/3.47 cnf(c1016,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X485)|icext(X485,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c572, c76])).
% 3.29/3.47 cnf(c1013,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X484)|icext(X484,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c572, c50])).
% 3.29/3.47 cnf(c350,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Resource),inference(resolution,[status(thm)],[c108, c203])).
% 3.29/3.47 cnf(c702,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X483)|iext(X483,uri_rdfs_Datatype,uri_rdfs_Resource),inference(resolution,[status(thm)],[c350, c24])).
% 3.29/3.47 cnf(c988,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X480)|icext(X480,uri_rdfs_range),inference(resolution,[status(thm)],[c570, c76])).
% 3.29/3.47 cnf(c699,plain,~iext(uri_rdfs_subClassOf,X479,uri_rdfs_Datatype)|iext(uri_rdfs_subClassOf,X479,uri_rdfs_Resource),inference(resolution,[status(thm)],[c350, c28])).
% 3.29/3.47 cnf(c984,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X478)|icext(X478,uri_rdfs_range),inference(resolution,[status(thm)],[c570, c50])).
% 3.29/3.47 cnf(c349,plain,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Resource),inference(resolution,[status(thm)],[c108, c206])).
% 3.29/3.47 cnf(c694,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X475)|iext(X475,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Resource),inference(resolution,[status(thm)],[c349, c24])).
% 3.29/3.47 cnf(c970,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X474)|icext(X474,uri_owl_complementOf),inference(resolution,[status(thm)],[c568, c76])).
% 3.29/3.47 cnf(c968,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X473)|icext(X473,uri_owl_complementOf),inference(resolution,[status(thm)],[c568, c50])).
% 3.29/3.47 cnf(c691,plain,~iext(uri_rdfs_subClassOf,X472,uri_rdfs_ContainerMembershipProperty)|iext(uri_rdfs_subClassOf,X472,uri_rdfs_Resource),inference(resolution,[status(thm)],[c349, c28])).
% 3.29/3.47 cnf(c946,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X469)|icext(X469,uri_rdfs_domain),inference(resolution,[status(thm)],[c566, c76])).
% 3.29/3.47 cnf(c348,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Resource),inference(resolution,[status(thm)],[c108, c205])).
% 3.29/3.47 cnf(c686,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X468)|iext(X468,uri_rdfs_Seq,uri_rdfs_Resource),inference(resolution,[status(thm)],[c348, c24])).
% 3.29/3.47 cnf(c941,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X467)|icext(X467,uri_rdfs_domain),inference(resolution,[status(thm)],[c566, c50])).
% 3.29/3.47 cnf(c683,plain,~iext(uri_rdfs_subClassOf,X464,uri_rdfs_Seq)|iext(uri_rdfs_subClassOf,X464,uri_rdfs_Resource),inference(resolution,[status(thm)],[c348, c28])).
% 3.29/3.47 cnf(c926,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X463)|icext(X463,uri_owl_onProperty),inference(resolution,[status(thm)],[c564, c76])).
% 3.29/3.47 cnf(c924,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X462)|icext(X462,uri_owl_onProperty),inference(resolution,[status(thm)],[c564, c50])).
% 3.29/3.47 cnf(c347,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Container,uri_rdfs_Resource),inference(resolution,[status(thm)],[c108, c221])).
% 3.29/3.47 cnf(c678,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X461)|iext(X461,uri_rdfs_Container,uri_rdfs_Resource),inference(resolution,[status(thm)],[c347, c24])).
% 3.29/3.47 cnf(c675,plain,~iext(uri_rdfs_subClassOf,X459,uri_rdfs_Container)|iext(uri_rdfs_subClassOf,X459,uri_rdfs_Resource),inference(resolution,[status(thm)],[c347, c28])).
% 3.29/3.47 cnf(c911,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X457)|icext(X457,uri_rdf_first),inference(resolution,[status(thm)],[c497, c76])).
% 3.29/3.47 cnf(c665,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X456)|iext(X456,uri_rdf_Bag,uri_rdfs_Resource),inference(resolution,[status(thm)],[c346, c24])).
% 3.29/3.47 cnf(c909,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X455)|icext(X455,uri_rdf_first),inference(resolution,[status(thm)],[c497, c50])).
% 3.29/3.47 cnf(c903,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X454)|icext(X454,uri_rdf_rest),inference(resolution,[status(thm)],[c488, c76])).
% 3.29/3.47 cnf(c662,plain,~iext(uri_rdfs_subClassOf,X453,uri_rdf_Bag)|iext(uri_rdfs_subClassOf,X453,uri_rdfs_Resource),inference(resolution,[status(thm)],[c346, c28])).
% 3.29/3.47 cnf(c901,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X452)|icext(X452,uri_rdf_rest),inference(resolution,[status(thm)],[c488, c50])).
% 3.29/3.47 cnf(c894,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X450)|icext(X450,uri_rdf__1),inference(resolution,[status(thm)],[c475, c50])).
% 3.29/3.47 cnf(c234,plain,iext(uri_rdfs_subClassOf,uri_rdf_Property,uri_rdf_Property),inference(resolution,[status(thm)],[c222, c31])).
% 3.29/3.47 cnf(c657,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X449)|iext(X449,uri_rdf_Property,uri_rdf_Property),inference(resolution,[status(thm)],[c234, c24])).
% 3.29/3.47 cnf(c886,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X447)|icext(X447,uri_rdf__2),inference(resolution,[status(thm)],[c473, c50])).
% 3.29/3.47 cnf(c879,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X444)|icext(X444,uri_rdf__3),inference(resolution,[status(thm)],[c460, c50])).
% 3.29/3.47 cnf(c232,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Container,uri_rdfs_Container),inference(resolution,[status(thm)],[c221, c31])).
% 3.29/3.47 cnf(c649,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X440)|iext(X440,uri_rdfs_Container,uri_rdfs_Container),inference(resolution,[status(thm)],[c232, c24])).
% 3.29/3.47 cnf(c858,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X438)|icext(X438,uri_rdf_object),inference(resolution,[status(thm)],[c446, c76])).
% 3.29/3.47 cnf(c856,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X437)|icext(X437,uri_rdf_object),inference(resolution,[status(thm)],[c446, c50])).
% 3.29/3.47 cnf(c851,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X435)|icext(X435,uri_rdf_subject),inference(resolution,[status(thm)],[c440, c76])).
% 3.29/3.47 cnf(c849,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X434)|icext(X434,uri_rdf_subject),inference(resolution,[status(thm)],[c440, c50])).
% 3.29/3.47 cnf(c230,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Literal,uri_rdfs_Literal),inference(resolution,[status(thm)],[c220, c31])).
% 3.29/3.47 cnf(c641,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X433)|iext(X433,uri_rdfs_Literal,uri_rdfs_Literal),inference(resolution,[status(thm)],[c230, c24])).
% 3.29/3.47 cnf(c844,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X432)|icext(X432,uri_rdf_value),inference(resolution,[status(thm)],[c439, c76])).
% 3.29/3.47 cnf(c842,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X431)|icext(X431,uri_rdf_value),inference(resolution,[status(thm)],[c439, c50])).
% 3.29/3.47 cnf(c830,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X429)|icext(X429,uri_rdf_type),inference(resolution,[status(thm)],[c438, c76])).
% 3.29/3.47 cnf(c828,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X428)|icext(X428,uri_rdf_type),inference(resolution,[status(thm)],[c438, c50])).
% 3.29/3.47 cnf(c228,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c219, c31])).
% 3.29/3.47 cnf(c633,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X427)|iext(X427,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c228, c24])).
% 3.29/3.47 cnf(c823,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X426)|icext(X426,uri_rdf__1),inference(resolution,[status(thm)],[c403, c76])).
% 3.29/3.47 cnf(c816,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X424)|icext(X424,uri_rdf__2),inference(resolution,[status(thm)],[c401, c76])).
% 3.29/3.47 cnf(c226,plain,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdf_Alt),inference(resolution,[status(thm)],[c208, c31])).
% 3.29/3.47 cnf(c625,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X417)|iext(X417,uri_rdf_Alt,uri_rdf_Alt),inference(resolution,[status(thm)],[c226, c24])).
% 3.29/3.47 cnf(c218,plain,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdf_Bag),inference(resolution,[status(thm)],[c207, c31])).
% 3.29/3.47 cnf(c617,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X406)|iext(X406,uri_rdf_Bag,uri_rdf_Bag),inference(resolution,[status(thm)],[c218, c24])).
% 3.29/3.47 cnf(c759,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X399)|icext(X399,uri_rdf__3),inference(resolution,[status(thm)],[c383, c76])).
% 3.29/3.47 cnf(c757,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X398)|icext(X398,uri_rdfs_member),inference(resolution,[status(thm)],[c383, c50])).
% 3.29/3.47 cnf(c216,plain,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c206, c31])).
% 3.29/3.47 cnf(c609,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X397)|iext(X397,uri_rdfs_ContainerMembershipProperty,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c216, c24])).
% 3.29/3.47 cnf(c750,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X395)|icext(X395,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c382, c50])).
% 3.29/3.47 cnf(c745,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X394)|icext(X394,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c381, c76])).
% 3.29/3.47 cnf(c214,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Seq),inference(resolution,[status(thm)],[c205, c31])).
% 3.29/3.47 cnf(c601,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X388)|iext(X388,uri_rdfs_Seq,uri_rdfs_Seq),inference(resolution,[status(thm)],[c214, c24])).
% 3.29/3.47 cnf(c212,plain,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c204, c31])).
% 3.29/3.47 cnf(c593,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X377)|iext(X377,uri_rdf_XMLLiteral,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c212, c24])).
% 3.29/3.47 cnf(c659,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X368)|icext(X368,uri_rdfs_Resource),inference(resolution,[status(thm)],[c346, c50])).
% 3.29/3.47 cnf(c210,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c203, c31])).
% 3.29/3.47 cnf(c585,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X367)|iext(X367,uri_rdfs_Datatype,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c210, c24])).
% 3.29/3.47 cnf(c652,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X366)|icext(X366,uri_rdf_Property),inference(resolution,[status(thm)],[c234, c76])).
% 3.29/3.47 cnf(c644,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X364)|icext(X364,uri_rdfs_Container),inference(resolution,[status(thm)],[c232, c76])).
% 3.29/3.47 cnf(c636,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X361)|icext(X361,uri_rdfs_Literal),inference(resolution,[status(thm)],[c230, c76])).
% 3.29/3.47 cnf(c494,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X359)|iext(X359,uri_rdf_first,uri_rdf_Property),inference(resolution,[status(thm)],[c140, c24])).
% 3.29/3.47 cnf(c628,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X358)|icext(X358,uri_rdfs_Class),inference(resolution,[status(thm)],[c228, c76])).
% 3.29/3.47 fof(rdf_collection_nil_type,axiom,iext(uri_rdf_type,uri_rdf_nil,uri_rdf_List),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdf_collection_nil_type)).
% 3.29/3.47 cnf(c139,plain,iext(uri_rdf_type,uri_rdf_nil,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdf_collection_nil_type])).
% 3.29/3.47 cnf(c485,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X355)|iext(X355,uri_rdf_nil,uri_rdf_List),inference(resolution,[status(thm)],[c139, c24])).
% 3.29/3.47 cnf(c619,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X354)|icext(X354,uri_rdf_Alt),inference(resolution,[status(thm)],[c226, c50])).
% 3.29/3.47 cnf(c481,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X352)|iext(X352,uri_rdf_rest,uri_rdf_Property),inference(resolution,[status(thm)],[c138, c24])).
% 3.29/3.47 cnf(c611,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X351)|icext(X351,uri_rdf_Bag),inference(resolution,[status(thm)],[c218, c50])).
% 3.29/3.47 cnf(c603,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X349)|icext(X349,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c216, c50])).
% 3.29/3.47 cnf(c470,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X348)|iext(X348,uri_rdf__1,uri_rdf_Property),inference(resolution,[status(thm)],[c137, c24])).
% 3.29/3.47 cnf(c595,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X346)|icext(X346,uri_rdfs_Seq),inference(resolution,[status(thm)],[c214, c50])).
% 3.29/3.47 cnf(c465,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X344)|iext(X344,uri_rdf__2,uri_rdf_Property),inference(resolution,[status(thm)],[c136, c24])).
% 3.29/3.47 cnf(c587,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X343)|icext(X343,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c212, c50])).
% 3.29/3.47 cnf(c457,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X341)|iext(X341,uri_rdf__3,uri_rdf_Property),inference(resolution,[status(thm)],[c135, c24])).
% 3.29/3.47 cnf(c579,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X340)|icext(X340,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c210, c50])).
% 3.29/3.47 cnf(c444,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X336)|iext(X336,uri_rdf_object,uri_rdf_Property),inference(resolution,[status(thm)],[c134, c24])).
% 3.29/3.47 cnf(c484,plain,~iext(uri_rdfs_range,uri_rdf_type,X335)|icext(X335,uri_rdf_List),inference(resolution,[status(thm)],[c139, c50])).
% 3.29/3.47 cnf(c432,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X332)|iext(X332,uri_rdf_value,uri_rdf_Property),inference(resolution,[status(thm)],[c133, c24])).
% 3.29/3.47 cnf(c427,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X327)|iext(X327,uri_rdf_subject,uri_rdf_Property),inference(resolution,[status(thm)],[c132, c24])).
% 3.29/3.48 cnf(c422,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X322)|iext(X322,uri_rdf_type,uri_rdf_Property),inference(resolution,[status(thm)],[c124, c24])).
% 3.29/3.48 fof(rdfs_annotation_comment_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_comment,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_comment_domain)).
% 3.29/3.48 cnf(c123,plain,iext(uri_rdfs_domain,uri_rdfs_comment,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_comment_domain])).
% 3.29/3.48 cnf(c418,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X317)|iext(X317,uri_rdfs_comment,uri_rdfs_Resource),inference(resolution,[status(thm)],[c123, c24])).
% 3.29/3.48 cnf(c421,plain,~iext(uri_rdfs_range,uri_rdf_type,X315)|icext(X315,uri_rdf_Property),inference(resolution,[status(thm)],[c124, c50])).
% 3.29/3.48 cnf(c415,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X314)|iext(X314,uri_rdfs_comment,uri_rdfs_Literal),inference(resolution,[status(thm)],[c122, c24])).
% 3.29/3.48 cnf(c419,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X313)|icext(X313,uri_rdfs_comment),inference(resolution,[status(thm)],[c123, c76])).
% 3.29/3.48 fof(rdfs_annotation_isdefinedby_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_isdefinedby_domain)).
% 3.29/3.48 cnf(c121,plain,iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_domain])).
% 3.29/3.48 cnf(c412,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X311)|iext(X311,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(resolution,[status(thm)],[c121, c24])).
% 3.29/3.48 fof(rdfs_annotation_isdefinedby_range,axiom,iext(uri_rdfs_range,uri_rdfs_isDefinedBy,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_isdefinedby_range)).
% 3.29/3.48 cnf(c120,plain,iext(uri_rdfs_range,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_range])).
% 3.29/3.48 cnf(c409,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X310)|iext(X310,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(resolution,[status(thm)],[c120, c24])).
% 3.29/3.48 fof(simple_ir,axiom,(![X]:ir(X)),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', simple_ir)).
% 3.29/3.48 fof(c144,plain,(![X42]:ir(X42)),inference(variable_rename,[status(thm)],[simple_ir])).
% 3.29/3.48 cnf(c145,plain,ir(X46),inference(split_conjunct,[status(thm)],[c144])).
% 3.29/3.48 fof(rdfs_ir_def,axiom,(![X]:(ir(X)<=>icext(uri_rdfs_Resource,X))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_ir_def)).
% 3.29/3.48 fof(c59,plain,(![X]:((~ir(X)|icext(uri_rdfs_Resource,X))&(~icext(uri_rdfs_Resource,X)|ir(X)))),inference(fof_nnf,[status(thm)],[rdfs_ir_def])).
% 3.29/3.48 fof(c60,plain,((![X]:(~ir(X)|icext(uri_rdfs_Resource,X)))&(![X]:(~icext(uri_rdfs_Resource,X)|ir(X)))),inference(shift_quantors,[status(thm)],[c59])).
% 3.29/3.48 fof(c62,plain,(![X24]:(![X25]:((~ir(X24)|icext(uri_rdfs_Resource,X24))&(~icext(uri_rdfs_Resource,X25)|ir(X25))))),inference(shift_quantors,[status(thm)],[fof(c61,plain,((![X24]:(~ir(X24)|icext(uri_rdfs_Resource,X24)))&(![X25]:(~icext(uri_rdfs_Resource,X25)|ir(X25)))),inference(variable_rename,[status(thm)],[c60])).])).
% 3.29/3.48 cnf(c63,plain,~ir(X54)|icext(uri_rdfs_Resource,X54),inference(split_conjunct,[status(thm)],[c62])).
% 3.29/3.48 cnf(c152,plain,icext(uri_rdfs_Resource,X57),inference(resolution,[status(thm)],[c63, c145])).
% 3.29/3.48 cnf(c385,plain,iext(uri_rdf_type,X93,uri_rdfs_Resource),inference(resolution,[status(thm)],[c114, c152])).
% 3.29/3.48 cnf(c406,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X307)|iext(X307,X308,uri_rdfs_Resource),inference(resolution,[status(thm)],[c385, c24])).
% 3.29/3.48 cnf(c413,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X304)|icext(X304,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c121, c76])).
% 3.29/3.48 cnf(c371,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X303)|iext(X303,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c119, c24])).
% 3.29/3.48 cnf(c410,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X301)|icext(X301,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c120, c76])).
% 3.29/3.48 cnf(c369,plain,~iext(uri_rdfs_subPropertyOf,X299,uri_rdfs_isDefinedBy)|iext(uri_rdfs_subPropertyOf,X299,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c119, c13])).
% 3.29/3.48 cnf(c405,plain,~iext(uri_rdfs_range,uri_rdf_type,X298)|icext(X298,uri_rdfs_Resource),inference(resolution,[status(thm)],[c385, c50])).
% 3.29/3.48 cnf(c373,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X297)|icext(X297,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c119, c76])).
% 3.29/3.48 fof(rdfs_annotation_label_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_label,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_label_domain)).
% 3.29/3.48 cnf(c118,plain,iext(uri_rdfs_domain,uri_rdfs_label,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_label_domain])).
% 3.29/3.48 cnf(c366,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X296)|iext(X296,uri_rdfs_label,uri_rdfs_Resource),inference(resolution,[status(thm)],[c118, c24])).
% 3.29/3.48 cnf(c370,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X295)|icext(X295,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c119, c50])).
% 3.29/3.48 cnf(c367,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X294)|icext(X294,uri_rdfs_label),inference(resolution,[status(thm)],[c118, c76])).
% 3.29/3.48 cnf(c363,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X292)|iext(X292,uri_rdfs_label,uri_rdfs_Literal),inference(resolution,[status(thm)],[c117, c24])).
% 3.29/3.48 fof(rdfs_annotation_seealso_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_seeAlso,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_seealso_domain)).
% 3.29/3.48 cnf(c116,plain,iext(uri_rdfs_domain,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_seealso_domain])).
% 3.29/3.48 cnf(c360,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X291)|iext(X291,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(resolution,[status(thm)],[c116, c24])).
% 3.29/3.48 cnf(c362,plain,~iext(uri_rdfs_range,uri_rdfs_range,X289)|icext(X289,uri_rdfs_Literal),inference(resolution,[status(thm)],[c117, c50])).
% 3.29/3.48 fof(rdfs_annotation_seealso_range,axiom,iext(uri_rdfs_range,uri_rdfs_seeAlso,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_seealso_range)).
% 3.29/3.48 cnf(c115,plain,iext(uri_rdfs_range,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_seealso_range])).
% 3.29/3.48 cnf(c357,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X288)|iext(X288,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(resolution,[status(thm)],[c115, c24])).
% 3.29/3.48 cnf(c361,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X287)|icext(X287,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c116, c76])).
% 3.29/3.48 fof(rdfs_collection_first_domain,axiom,iext(uri_rdfs_domain,uri_rdf_first,uri_rdf_List),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_collection_first_domain)).
% 3.29/3.48 cnf(c105,plain,iext(uri_rdfs_domain,uri_rdf_first,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdfs_collection_first_domain])).
% 3.29/3.48 cnf(c344,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X285)|iext(X285,uri_rdf_first,uri_rdf_List),inference(resolution,[status(thm)],[c105, c24])).
% 3.29/3.48 cnf(c358,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X284)|icext(X284,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c115, c76])).
% 3.29/3.48 cnf(c345,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X282)|icext(X282,uri_rdf_first),inference(resolution,[status(thm)],[c105, c76])).
% 3.29/3.48 fof(rdfs_collection_first_range,axiom,iext(uri_rdfs_range,uri_rdf_first,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_collection_first_range)).
% 3.29/3.48 cnf(c104,plain,iext(uri_rdfs_range,uri_rdf_first,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_collection_first_range])).
% 3.29/3.48 cnf(c341,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X281)|iext(X281,uri_rdf_first,uri_rdfs_Resource),inference(resolution,[status(thm)],[c104, c24])).
% 3.29/3.48 cnf(c342,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X279)|icext(X279,uri_rdf_first),inference(resolution,[status(thm)],[c104, c76])).
% 3.29/3.48 fof(rdfs_collection_rest_domain,axiom,iext(uri_rdfs_domain,uri_rdf_rest,uri_rdf_List),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_collection_rest_domain)).
% 3.29/3.48 cnf(c103,plain,iext(uri_rdfs_domain,uri_rdf_rest,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdfs_collection_rest_domain])).
% 3.29/3.48 cnf(c338,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X277)|iext(X277,uri_rdf_rest,uri_rdf_List),inference(resolution,[status(thm)],[c103, c24])).
% 3.29/3.48 cnf(c339,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X276)|icext(X276,uri_rdf_rest),inference(resolution,[status(thm)],[c103, c76])).
% 3.29/3.48 cnf(c337,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X275)|icext(X275,uri_rdf_List),inference(resolution,[status(thm)],[c103, c50])).
% 3.29/3.48 cnf(c329,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X273)|icext(X273,uri_rdfs_domain),inference(resolution,[status(thm)],[c76, c71])).
% 3.29/3.48 fof(rdfs_reification_predicate_range,axiom,iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_reification_predicate_range)).
% 3.29/3.48 cnf(c43,plain,iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_reification_predicate_range])).
% 3.29/3.48 cnf(c328,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X272)|icext(X272,uri_rdf_predicate),inference(resolution,[status(thm)],[c76, c43])).
% 3.29/3.48 cnf(c326,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X270)|icext(X270,uri_rdf_Alt),inference(resolution,[status(thm)],[c76, c101])).
% 3.29/3.48 fof(rdfs_container_n_range_001,axiom,iext(uri_rdfs_range,uri_rdf__1,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_range_001)).
% 3.29/3.48 cnf(c90,plain,iext(uri_rdfs_range,uri_rdf__1,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_range_001])).
% 3.29/3.48 cnf(c325,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X269)|icext(X269,uri_rdf__1),inference(resolution,[status(thm)],[c76, c90])).
% 3.29/3.48 fof(rdfs_container_member_range,axiom,iext(uri_rdfs_range,uri_rdfs_member,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_member_range)).
% 3.29/3.48 cnf(c94,plain,iext(uri_rdfs_range,uri_rdfs_member,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_member_range])).
% 3.29/3.48 cnf(c324,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X268)|icext(X268,uri_rdfs_member),inference(resolution,[status(thm)],[c76, c94])).
% 3.29/3.48 fof(rdfs_reification_subject_domain,axiom,iext(uri_rdfs_domain,uri_rdf_subject,uri_rdfs_Statement),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_reification_subject_domain)).
% 3.29/3.48 cnf(c42,plain,iext(uri_rdfs_domain,uri_rdf_subject,uri_rdfs_Statement),inference(split_conjunct,[status(thm)],[rdfs_reification_subject_domain])).
% 3.29/3.48 cnf(c323,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X267)|icext(X267,uri_rdf_subject),inference(resolution,[status(thm)],[c76, c42])).
% 3.29/3.48 fof(rdfs_subclassof_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdfs_Class),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_subclassof_domain)).
% 3.29/3.48 cnf(c40,plain,iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_subclassof_domain])).
% 3.29/3.48 cnf(c322,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X266)|icext(X266,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c76, c40])).
% 3.29/3.48 fof(rdfs_reification_subject_range,axiom,iext(uri_rdfs_range,uri_rdf_subject,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_reification_subject_range)).
% 3.29/3.48 cnf(c41,plain,iext(uri_rdfs_range,uri_rdf_subject,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_reification_subject_range])).
% 3.29/3.48 cnf(c321,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X265)|icext(X265,uri_rdf_subject),inference(resolution,[status(thm)],[c76, c41])).
% 3.29/3.48 cnf(c320,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X264)|icext(X264,uri_rdf_Bag),inference(resolution,[status(thm)],[c76, c100])).
% 3.29/3.48 cnf(c319,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X263)|icext(X263,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c76, c96])).
% 3.29/3.48 cnf(c317,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X261)|icext(X261,uri_rdfs_Seq),inference(resolution,[status(thm)],[c76, c84])).
% 3.29/3.48 fof(rdfs_subpropertyof_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_subpropertyof_domain)).
% 3.29/3.48 cnf(c25,plain,iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_subpropertyof_domain])).
% 3.29/3.48 cnf(c316,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X260)|icext(X260,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c76, c25])).
% 3.29/3.48 fof(rdfs_container_member_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_member,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_member_domain)).
% 3.29/3.48 cnf(c95,plain,iext(uri_rdfs_domain,uri_rdfs_member,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_member_domain])).
% 3.29/3.48 cnf(c314,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X258)|icext(X258,uri_rdfs_member),inference(resolution,[status(thm)],[c76, c95])).
% 3.29/3.48 fof(rdfs_reification_object_domain,axiom,iext(uri_rdfs_domain,uri_rdf_object,uri_rdfs_Statement),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_reification_object_domain)).
% 3.29/3.48 cnf(c46,plain,iext(uri_rdfs_domain,uri_rdf_object,uri_rdfs_Statement),inference(split_conjunct,[status(thm)],[rdfs_reification_object_domain])).
% 3.29/3.48 cnf(c313,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X257)|icext(X257,uri_rdf_object),inference(resolution,[status(thm)],[c76, c46])).
% 3.29/3.48 fof(rdfs_container_n_domain_001,axiom,iext(uri_rdfs_domain,uri_rdf__1,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_domain_001)).
% 3.29/3.48 cnf(c93,plain,iext(uri_rdfs_domain,uri_rdf__1,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_001])).
% 3.29/3.48 cnf(c312,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X256)|icext(X256,uri_rdf__1),inference(resolution,[status(thm)],[c76, c93])).
% 3.29/3.48 fof(rdfs_subclassof_range,axiom,iext(uri_rdfs_range,uri_rdfs_subClassOf,uri_rdfs_Class),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_subclassof_range)).
% 3.29/3.48 cnf(c32,plain,iext(uri_rdfs_range,uri_rdfs_subClassOf,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_subclassof_range])).
% 3.29/3.48 cnf(c311,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X255)|icext(X255,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c76, c32])).
% 3.29/3.48 cnf(c310,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X254)|icext(X254,uri_rdfs_range),inference(resolution,[status(thm)],[c76, c51])).
% 3.29/3.48 cnf(c309,plain,~iext(uri_rdfs_domain,uri_owl_hasSelf,X253)|icext(X253,skolem0001),inference(resolution,[status(thm)],[c76, c6])).
% 3.29/3.48 fof(rdfs_subpropertyof_range,axiom,iext(uri_rdfs_range,uri_rdfs_subPropertyOf,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_subpropertyof_range)).
% 3.29/3.48 cnf(c17,plain,iext(uri_rdfs_range,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_subpropertyof_range])).
% 3.29/3.48 cnf(c307,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X251)|icext(X251,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c76, c17])).
% 3.29/3.48 cnf(c305,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X249)|icext(X249,uri_rdf_type),inference(resolution,[status(thm)],[c76, c9])).
% 3.29/3.48 cnf(c304,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X248)|icext(X248,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c76, c83])).
% 3.29/3.48 cnf(c303,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X247)|icext(X247,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c76, c78])).
% 3.29/3.48 fof(rdfs_container_n_domain_002,axiom,iext(uri_rdfs_domain,uri_rdf__2,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_domain_002)).
% 3.29/3.48 cnf(c92,plain,iext(uri_rdfs_domain,uri_rdf__2,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_002])).
% 3.29/3.48 cnf(c302,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X246)|icext(X246,uri_rdf__2),inference(resolution,[status(thm)],[c76, c92])).
% 3.29/3.48 fof(rdfs_type_domain,axiom,iext(uri_rdfs_domain,uri_rdf_type,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_type_domain)).
% 3.29/3.48 cnf(c10,plain,iext(uri_rdfs_domain,uri_rdf_type,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_type_domain])).
% 3.29/3.48 cnf(c301,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X245)|icext(X245,uri_rdf_type),inference(resolution,[status(thm)],[c76, c10])).
% 3.29/3.48 cnf(c300,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X244)|icext(X244,uri_rdf_rest),inference(resolution,[status(thm)],[c76, c102])).
% 3.29/3.48 fof(rdfs_container_n_range_002,axiom,iext(uri_rdfs_range,uri_rdf__2,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_range_002)).
% 3.29/3.48 cnf(c89,plain,iext(uri_rdfs_range,uri_rdf__2,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_range_002])).
% 3.29/3.48 cnf(c298,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X242)|icext(X242,uri_rdf__2),inference(resolution,[status(thm)],[c76, c89])).
% 3.29/3.48 fof(rdfs_container_n_range_003,axiom,iext(uri_rdfs_range,uri_rdf__3,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_range_003)).
% 3.29/3.48 cnf(c88,plain,iext(uri_rdfs_range,uri_rdf__3,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_range_003])).
% 3.29/3.48 cnf(c297,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X241)|icext(X241,uri_rdf__3),inference(resolution,[status(thm)],[c76, c88])).
% 3.29/3.48 fof(rdfs_value_range,axiom,iext(uri_rdfs_range,uri_rdf_value,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_value_range)).
% 3.29/3.48 cnf(c7,plain,iext(uri_rdfs_range,uri_rdf_value,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_value_range])).
% 3.29/3.48 cnf(c296,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X240)|icext(X240,uri_rdf_value),inference(resolution,[status(thm)],[c76, c7])).
% 3.29/3.48 cnf(c295,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X239)|icext(X239,uri_rdfs_range),inference(resolution,[status(thm)],[c76, c47])).
% 3.29/3.48 cnf(c294,plain,~iext(uri_rdfs_domain,uri_owl_complementOf,X238)|icext(X238,uri_ex_c),inference(resolution,[status(thm)],[c76, c3])).
% 3.29/3.48 fof(rdfs_value_domain,axiom,iext(uri_rdfs_domain,uri_rdf_value,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_value_domain)).
% 3.29/3.48 cnf(c8,plain,iext(uri_rdfs_domain,uri_rdf_value,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_value_domain])).
% 3.29/3.48 cnf(c291,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X235)|icext(X235,uri_rdf_value),inference(resolution,[status(thm)],[c76, c8])).
% 3.29/3.48 cnf(c290,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X234)|icext(X234,uri_rdf__3),inference(resolution,[status(thm)],[c76, c91])).
% 3.29/3.48 cnf(c289,plain,~iext(uri_rdfs_domain,uri_owl_onProperty,X233)|icext(X233,skolem0001),inference(resolution,[status(thm)],[c76, c5])).
% 3.29/3.48 cnf(c288,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X232)|icext(X232,uri_rdfs_domain),inference(factor,[status(thm)],[c76])).
% 3.29/3.48 cnf(c407,plain,~iext(uri_rdfs_domain,uri_rdf_type,X228)|icext(X228,X229),inference(resolution,[status(thm)],[c385, c76])).
% 3.29/3.48 cnf(c277,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X191)|icext(X191,uri_rdfs_Class),inference(resolution,[status(thm)],[c50, c40])).
% 3.29/3.48 cnf(c274,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X188)|icext(X188,uri_rdf_Property),inference(resolution,[status(thm)],[c50, c96])).
% 3.29/3.48 cnf(c272,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X186)|icext(X186,uri_rdfs_Container),inference(resolution,[status(thm)],[c50, c84])).
% 3.29/3.48 fof(rdfs_property_type,axiom,iext(uri_rdf_type,uri_rdf_Property,uri_rdfs_Class),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_property_type)).
% 3.29/3.48 cnf(c52,plain,iext(uri_rdf_type,uri_rdf_Property,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_property_type])).
% 3.29/3.48 cnf(c270,plain,~iext(uri_rdfs_range,uri_rdf_type,X184)|icext(X184,uri_rdfs_Class),inference(resolution,[status(thm)],[c50, c52])).
% 3.29/3.48 cnf(c264,plain,~iext(uri_rdfs_range,uri_owl_hasSelf,X178)|icext(X178,literal_typed(dat_str_true,uri_xsd_boolean)),inference(resolution,[status(thm)],[c50, c6])).
% 3.29/3.48 fof(rdfs_dat_xmlliteral_type,axiom,iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Datatype),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_dat_xmlliteral_type)).
% 3.29/3.48 cnf(c82,plain,iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Datatype),inference(split_conjunct,[status(thm)],[rdfs_dat_xmlliteral_type])).
% 3.29/3.48 cnf(c263,plain,~iext(uri_rdfs_range,uri_rdf_type,X177)|icext(X177,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c50, c82])).
% 3.29/3.48 cnf(c262,plain,~iext(uri_rdfs_range,uri_rdfs_range,X176)|icext(X176,uri_rdf_Property),inference(resolution,[status(thm)],[c50, c17])).
% 3.29/3.48 cnf(c261,plain,~iext(uri_rdfs_range,uri_rdf_type,X175)|icext(X175,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c50, c85])).
% 3.29/3.48 cnf(c259,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X173)|icext(X173,uri_rdfs_Literal),inference(resolution,[status(thm)],[c50, c83])).
% 3.29/3.48 cnf(c258,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X172)|icext(X172,uri_rdfs_Class),inference(resolution,[status(thm)],[c50, c78])).
% 3.29/3.48 cnf(c1085,plain,icext(uri_rdf_Property,uri_rdfs_member),inference(resolution,[status(thm)],[c764, c113])).
% 3.29/3.48 cnf(c254,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X168)|icext(X168,uri_rdf_Property),inference(resolution,[status(thm)],[c50, c77])).
% 3.29/3.48 cnf(c251,plain,~iext(uri_rdfs_range,uri_rdfs_range,X165)|icext(X165,uri_rdfs_Resource),inference(resolution,[status(thm)],[c50, c7])).
% 3.29/3.48 cnf(c1056,plain,icext(uri_rdf_Property,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c575, c113])).
% 3.29/3.48 cnf(c250,plain,~iext(uri_rdfs_range,uri_rdfs_range,X164)|icext(X164,uri_rdfs_Class),inference(resolution,[status(thm)],[c50, c47])).
% 3.29/3.48 cnf(c249,plain,~iext(uri_rdfs_range,uri_owl_complementOf,X163)|icext(X163,skolem0001),inference(resolution,[status(thm)],[c50, c3])).
% 3.29/3.48 cnf(c1034,plain,icext(uri_rdf_Property,uri_owl_hasSelf),inference(resolution,[status(thm)],[c573, c113])).
% 3.29/3.48 cnf(c1008,plain,icext(uri_rdf_Property,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c571, c113])).
% 3.29/3.48 cnf(c245,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X159)|icext(X159,uri_rdfs_Resource),inference(resolution,[status(thm)],[c50, c91])).
% 3.29/3.48 cnf(c980,plain,icext(uri_rdf_Property,uri_rdfs_range),inference(resolution,[status(thm)],[c569, c113])).
% 3.29/3.48 cnf(c244,plain,~iext(uri_rdfs_range,uri_owl_onProperty,X158)|icext(X158,uri_rdf_type),inference(resolution,[status(thm)],[c50, c5])).
% 3.29/3.48 cnf(c243,plain,~iext(uri_rdfs_range,uri_rdfs_range,X157)|icext(X157,X157),inference(factor,[status(thm)],[c50])).
% 3.29/3.48 cnf(c964,plain,icext(uri_rdf_Property,uri_owl_complementOf),inference(resolution,[status(thm)],[c567, c113])).
% 3.29/3.48 cnf(c39,plain,~iext(uri_rdfs_subClassOf,X75,X76)|~icext(X75,X77)|icext(X76,X77),inference(split_conjunct,[status(thm)],[c36])).
% 3.29/3.48 cnf(c240,plain,~icext(uri_rdf_Alt,X156)|icext(uri_rdfs_Container,X156),inference(resolution,[status(thm)],[c39, c101])).
% 3.29/3.48 cnf(c239,plain,~icext(uri_rdf_Bag,X155)|icext(uri_rdfs_Container,X155),inference(resolution,[status(thm)],[c39, c100])).
% 3.29/3.48 cnf(c934,plain,icext(uri_rdf_Property,uri_rdfs_domain),inference(resolution,[status(thm)],[c565, c113])).
% 3.29/3.48 cnf(c238,plain,~icext(uri_rdfs_ContainerMembershipProperty,X154)|icext(uri_rdf_Property,X154),inference(resolution,[status(thm)],[c39, c96])).
% 3.29/3.48 cnf(c237,plain,~icext(uri_rdfs_Seq,X153)|icext(uri_rdfs_Container,X153),inference(resolution,[status(thm)],[c39, c84])).
% 3.29/3.48 cnf(c919,plain,icext(uri_rdf_Property,uri_owl_onProperty),inference(resolution,[status(thm)],[c563, c113])).
% 3.29/3.48 cnf(c236,plain,~icext(uri_rdf_XMLLiteral,X152)|icext(uri_rdfs_Literal,X152),inference(resolution,[status(thm)],[c39, c83])).
% 3.29/3.48 cnf(c235,plain,~icext(uri_rdfs_Datatype,X151)|icext(uri_rdfs_Class,X151),inference(resolution,[status(thm)],[c39, c78])).
% 3.29/3.48 cnf(c202,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X150)|iext(X150,uri_rdf_rest,uri_rdf_List),inference(resolution,[status(thm)],[c102, c24])).
% 3.29/3.48 cnf(c201,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X149)|iext(X149,uri_rdf_Alt,uri_rdfs_Container),inference(resolution,[status(thm)],[c101, c24])).
% 3.29/3.48 cnf(c200,plain,~iext(uri_rdfs_subClassOf,X148,uri_rdf_Alt)|iext(uri_rdfs_subClassOf,X148,uri_rdfs_Container),inference(resolution,[status(thm)],[c101, c28])).
% 3.29/3.48 cnf(c199,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X147)|iext(X147,uri_rdf_Bag,uri_rdfs_Container),inference(resolution,[status(thm)],[c100, c24])).
% 3.29/3.48 cnf(c198,plain,~iext(uri_rdfs_subClassOf,X146,uri_rdf_Bag)|iext(uri_rdfs_subClassOf,X146,uri_rdfs_Container),inference(resolution,[status(thm)],[c100, c28])).
% 3.29/3.48 cnf(c874,plain,icext(uri_rdf_Property,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c451, c113])).
% 3.29/3.48 cnf(c197,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X145)|iext(X145,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),inference(resolution,[status(thm)],[c96, c24])).
% 3.29/3.48 cnf(c867,plain,icext(uri_rdf_Property,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c450, c113])).
% 3.29/3.48 cnf(c196,plain,~iext(uri_rdfs_subClassOf,X144,uri_rdfs_ContainerMembershipProperty)|iext(uri_rdfs_subClassOf,X144,uri_rdf_Property),inference(resolution,[status(thm)],[c96, c28])).
% 3.29/3.48 cnf(c195,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X143)|iext(X143,uri_rdfs_member,uri_rdfs_Resource),inference(resolution,[status(thm)],[c95, c24])).
% 3.29/3.48 cnf(c194,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X142)|iext(X142,uri_rdfs_member,uri_rdfs_Resource),inference(resolution,[status(thm)],[c94, c24])).
% 3.29/3.48 cnf(c193,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X141)|iext(X141,uri_rdf__1,uri_rdfs_Resource),inference(resolution,[status(thm)],[c93, c24])).
% 3.29/3.48 cnf(c192,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X140)|iext(X140,uri_rdf__2,uri_rdfs_Resource),inference(resolution,[status(thm)],[c92, c24])).
% 3.29/3.48 cnf(c191,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X139)|iext(X139,uri_rdf__3,uri_rdfs_Resource),inference(resolution,[status(thm)],[c91, c24])).
% 3.29/3.48 cnf(c190,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X138)|iext(X138,uri_rdf__1,uri_rdfs_Resource),inference(resolution,[status(thm)],[c90, c24])).
% 3.29/3.48 cnf(c189,plain,~iext(uri_rdfs_subClassOf,X137,uri_rdfs_Seq)|iext(uri_rdfs_subClassOf,X137,uri_rdfs_Container),inference(resolution,[status(thm)],[c28, c84])).
% 3.29/3.48 cnf(c188,plain,~iext(uri_rdfs_subClassOf,X136,uri_rdf_XMLLiteral)|iext(uri_rdfs_subClassOf,X136,uri_rdfs_Literal),inference(resolution,[status(thm)],[c28, c83])).
% 3.29/3.48 cnf(c187,plain,~iext(uri_rdfs_subClassOf,X135,uri_rdfs_Datatype)|iext(uri_rdfs_subClassOf,X135,uri_rdfs_Class),inference(resolution,[status(thm)],[c28, c78])).
% 3.29/3.48 cnf(c185,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X133)|iext(X133,uri_rdf__2,uri_rdfs_Resource),inference(resolution,[status(thm)],[c89, c24])).
% 3.29/3.48 cnf(c184,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X132)|iext(X132,uri_rdf__3,uri_rdfs_Resource),inference(resolution,[status(thm)],[c88, c24])).
% 3.29/3.48 cnf(c183,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X131)|iext(X131,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c87, c24])).
% 3.29/3.48 cnf(c182,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X130)|iext(X130,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c86, c24])).
% 3.29/3.48 cnf(c181,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X129)|iext(X129,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c85, c24])).
% 3.29/3.48 cnf(c180,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X128)|iext(X128,uri_rdfs_domain,uri_rdfs_Class),inference(resolution,[status(thm)],[c24, c71])).
% 3.29/3.48 cnf(c179,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X127)|iext(X127,uri_rdf_predicate,uri_rdfs_Resource),inference(resolution,[status(thm)],[c24, c43])).
% 3.29/3.48 cnf(c178,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X126)|iext(X126,uri_rdf_subject,uri_rdfs_Statement),inference(resolution,[status(thm)],[c24, c42])).
% 3.29/3.48 cnf(c177,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X125)|iext(X125,uri_rdfs_subClassOf,uri_rdfs_Class),inference(resolution,[status(thm)],[c24, c40])).
% 3.29/3.48 cnf(c176,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X124)|iext(X124,uri_rdf_subject,uri_rdfs_Resource),inference(resolution,[status(thm)],[c24, c41])).
% 3.29/3.48 cnf(c175,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X123)|iext(X123,uri_ex_c,uri_owl_Class),inference(resolution,[status(thm)],[c24, c2])).
% 3.29/3.48 cnf(c174,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X122)|iext(X122,uri_rdfs_Seq,uri_rdfs_Container),inference(resolution,[status(thm)],[c24, c84])).
% 3.29/3.48 cnf(c173,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X121)|iext(X121,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c24, c25])).
% 3.29/3.48 cnf(c172,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X120)|iext(X120,uri_rdf_Property,uri_rdfs_Class),inference(resolution,[status(thm)],[c24, c52])).
% 3.29/3.48 cnf(c171,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X119)|iext(X119,uri_rdf_object,uri_rdfs_Statement),inference(resolution,[status(thm)],[c24, c46])).
% 3.29/3.48 cnf(c170,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X118)|iext(X118,uri_rdfs_subClassOf,uri_rdfs_Class),inference(resolution,[status(thm)],[c24, c32])).
% 3.29/3.48 cnf(c169,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X117)|iext(X117,uri_rdfs_range,uri_rdf_Property),inference(resolution,[status(thm)],[c24, c51])).
% 3.29/3.48 cnf(c168,plain,~iext(uri_rdfs_subPropertyOf,uri_owl_hasSelf,X116)|iext(X116,skolem0001,literal_typed(dat_str_true,uri_xsd_boolean)),inference(resolution,[status(thm)],[c24, c6])).
% 3.29/3.48 cnf(c167,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X115)|iext(X115,uri_rdf_XMLLiteral,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c24, c82])).
% 3.29/3.48 cnf(c166,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X114)|iext(X114,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c24, c17])).
% 3.29/3.48 cnf(c165,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X113)|iext(X113,uri_rdf_type,uri_rdfs_Class),inference(resolution,[status(thm)],[c24, c9])).
% 3.29/3.48 cnf(c491,plain,icext(uri_rdf_Property,uri_rdf_first),inference(resolution,[status(thm)],[c140, c113])).
% 3.29/3.48 cnf(c164,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X112)|iext(X112,uri_rdf_XMLLiteral,uri_rdfs_Literal),inference(resolution,[status(thm)],[c24, c83])).
% 3.29/3.48 cnf(c163,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X111)|iext(X111,uri_rdfs_Datatype,uri_rdfs_Class),inference(resolution,[status(thm)],[c24, c78])).
% 3.29/3.48 cnf(c162,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X110)|iext(X110,uri_rdf_type,uri_rdfs_Resource),inference(resolution,[status(thm)],[c24, c10])).
% 3.29/3.48 cnf(c161,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X109)|iext(X109,uri_rdfs_domain,uri_rdf_Property),inference(resolution,[status(thm)],[c24, c77])).
% 3.29/3.48 cnf(c160,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X108)|iext(X108,uri_rdf_value,uri_rdfs_Resource),inference(resolution,[status(thm)],[c24, c7])).
% 3.29/3.48 cnf(c159,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X107)|iext(X107,uri_rdfs_range,uri_rdfs_Class),inference(resolution,[status(thm)],[c24, c47])).
% 3.29/3.48 cnf(c158,plain,~iext(uri_rdfs_subPropertyOf,uri_owl_complementOf,X106)|iext(X106,uri_ex_c,skolem0001),inference(resolution,[status(thm)],[c24, c3])).
% 3.29/3.48 cnf(c157,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X105)|iext(X105,skolem0001,uri_owl_Restriction),inference(resolution,[status(thm)],[c24, c4])).
% 3.29/3.48 cnf(c156,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X104)|iext(X104,uri_rdf_predicate,uri_rdfs_Statement),inference(resolution,[status(thm)],[c24, c44])).
% 3.29/3.48 cnf(c155,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X103)|iext(X103,uri_rdf_value,uri_rdfs_Resource),inference(resolution,[status(thm)],[c24, c8])).
% 3.29/3.48 cnf(c154,plain,~iext(uri_rdfs_subPropertyOf,uri_owl_onProperty,X102)|iext(X102,skolem0001,uri_rdf_type),inference(resolution,[status(thm)],[c24, c5])).
% 3.29/3.48 cnf(c153,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X101)|iext(X101,uri_rdfs_subPropertyOf,X101),inference(factor,[status(thm)],[c24])).
% 3.29/3.48 cnf(c483,plain,icext(uri_rdf_List,uri_rdf_nil),inference(resolution,[status(thm)],[c139, c113])).
% 3.29/3.48 cnf(c478,plain,icext(uri_rdf_Property,uri_rdf_rest),inference(resolution,[status(thm)],[c138, c113])).
% 3.29/3.48 cnf(c467,plain,icext(uri_rdf_Property,uri_rdf__1),inference(resolution,[status(thm)],[c137, c113])).
% 3.29/3.48 cnf(c462,plain,icext(uri_rdf_Property,uri_rdf__2),inference(resolution,[status(thm)],[c136, c113])).
% 3.29/3.48 cnf(c454,plain,icext(uri_rdf_Property,uri_rdf__3),inference(resolution,[status(thm)],[c135, c113])).
% 3.29/3.48 cnf(c441,plain,icext(uri_rdf_Property,uri_rdf_object),inference(resolution,[status(thm)],[c134, c113])).
% 3.29/3.48 cnf(c430,plain,icext(uri_rdf_Property,uri_rdf_value),inference(resolution,[status(thm)],[c133, c113])).
% 3.29/3.48 cnf(c425,plain,icext(uri_rdf_Property,uri_rdf_subject),inference(resolution,[status(thm)],[c132, c113])).
% 3.29/3.48 cnf(c420,plain,icext(uri_rdf_Property,uri_rdf_type),inference(resolution,[status(thm)],[c124, c113])).
% 3.29/3.48 cnf(c378,plain,icext(uri_owl_Class,uri_ex_c),inference(resolution,[status(thm)],[c113, c2])).
% 3.29/3.48 cnf(c376,plain,icext(uri_rdfs_Datatype,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c113, c82])).
% 3.29/3.48 cnf(c374,plain,icext(uri_owl_Restriction,skolem0001),inference(resolution,[status(thm)],[c113, c4])).
% 3.29/3.48 cnf(c233,plain,icext(uri_rdfs_Class,uri_rdf_Property),inference(resolution,[status(thm)],[c222, c69])).
% 3.29/3.48 fof(rdfs_datatype_instsub_literal,axiom,(![D]:(icext(uri_rdfs_Datatype,D)=>iext(uri_rdfs_subClassOf,D,uri_rdfs_Literal))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_datatype_instsub_literal)).
% 3.29/3.48 fof(c79,plain,(![D]:(~icext(uri_rdfs_Datatype,D)|iext(uri_rdfs_subClassOf,D,uri_rdfs_Literal))),inference(fof_nnf,[status(thm)],[rdfs_datatype_instsub_literal])).
% 3.29/3.48 fof(c80,plain,(![X32]:(~icext(uri_rdfs_Datatype,X32)|iext(uri_rdfs_subClassOf,X32,uri_rdfs_Literal))),inference(variable_rename,[status(thm)],[c79])).
% 3.29/3.48 cnf(c81,plain,~icext(uri_rdfs_Datatype,X86)|iext(uri_rdfs_subClassOf,X86,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[c80])).
% 3.29/3.48 fof(rdfs_lv_def,axiom,(![X]:(lv(X)<=>icext(uri_rdfs_Literal,X))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_lv_def)).
% 3.29/3.48 fof(c53,plain,(![X]:((~lv(X)|icext(uri_rdfs_Literal,X))&(~icext(uri_rdfs_Literal,X)|lv(X)))),inference(fof_nnf,[status(thm)],[rdfs_lv_def])).
% 3.29/3.48 fof(c54,plain,((![X]:(~lv(X)|icext(uri_rdfs_Literal,X)))&(![X]:(~icext(uri_rdfs_Literal,X)|lv(X)))),inference(shift_quantors,[status(thm)],[c53])).
% 3.29/3.48 fof(c56,plain,(![X22]:(![X23]:((~lv(X22)|icext(uri_rdfs_Literal,X22))&(~icext(uri_rdfs_Literal,X23)|lv(X23))))),inference(shift_quantors,[status(thm)],[fof(c55,plain,((![X22]:(~lv(X22)|icext(uri_rdfs_Literal,X22)))&(![X23]:(~icext(uri_rdfs_Literal,X23)|lv(X23)))),inference(variable_rename,[status(thm)],[c54])).])).
% 3.29/3.48 cnf(c58,plain,~icext(uri_rdfs_Literal,X53)|lv(X53),inference(split_conjunct,[status(thm)],[c56])).
% 3.29/3.48 cnf(c57,plain,~lv(X52)|icext(uri_rdfs_Literal,X52),inference(split_conjunct,[status(thm)],[c56])).
% 3.29/3.48 % SZS output end Saturation
% 3.29/3.48
% 3.29/3.48 % Initial clauses : 94
% 3.29/3.48 % Processed clauses : 568
% 3.29/3.48 % Factors computed : 5
% 3.29/3.48 % Resolvents computed: 1335
% 3.29/3.48 % Tautologies deleted: 54
% 3.29/3.48 % Forward subsumed : 812
% 3.29/3.48 % Backward subsumed : 1
% 3.29/3.48 % -------- CPU Time ---------
% 3.29/3.48 % User time : 3.109 s
% 3.29/3.48 % System time : 0.018 s
% 3.29/3.48 % Total time : 3.127 s
%------------------------------------------------------------------------------