%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SWB011+4 : TPTP v8.1.2. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n013.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:47 EDT 2024
% Result : Satisfiable 2.99s 3.16s
% Output : Saturation 2.99s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : SWB011+4 : TPTP v8.1.2. Released v5.2.0.
% 0.14/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.36 % Computer : n013.cluster.edu
% 0.15/0.36 % Model : x86_64 x86_64
% 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.36 % Memory : 8042.1875MB
% 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.36 % CPULimit : 300
% 0.15/0.36 % WCLimit : 300
% 0.15/0.36 % DateTime : Wed May 8 22:10:23 EDT 2024
% 0.22/0.36 % CPUTime :
% 2.99/3.16 % Version: 1.5
% 2.99/3.16 % SZS status Satisfiable
% 2.99/3.16 % SZS output start Saturation
% 2.99/3.16 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)).
% 2.99/3.16 fof(c14,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])).
% 2.99/3.16 fof(c16,plain,(![X6]:(![X7]:(![X8]:(![X9]:(~iext(uri_rdfs_subPropertyOf,X6,X7)|((ip(X6)&ip(X7))&(~iext(X6,X8,X9)|iext(X7,X8,X9)))))))),inference(shift_quantors,[status(thm)],[fof(c15,plain,(![X6]:(![X7]:(~iext(uri_rdfs_subPropertyOf,X6,X7)|((ip(X6)&ip(X7))&(![X8]:(![X9]:(~iext(X6,X8,X9)|iext(X7,X8,X9)))))))),inference(variable_rename,[status(thm)],[c14])).])).
% 2.99/3.16 fof(c17,plain,(![X6]:(![X7]:(![X8]:(![X9]:(((~iext(uri_rdfs_subPropertyOf,X6,X7)|ip(X6))&(~iext(uri_rdfs_subPropertyOf,X6,X7)|ip(X7)))&(~iext(uri_rdfs_subPropertyOf,X6,X7)|(~iext(X6,X8,X9)|iext(X7,X8,X9)))))))),inference(distribute,[status(thm)],[c16])).
% 2.99/3.16 cnf(c20,plain,~iext(uri_rdfs_subPropertyOf,X65,X64)|~iext(X65,X62,X63)|iext(X64,X62,X63),inference(split_conjunct,[status(thm)],[c17])).
% 2.99/3.16 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)).
% 2.99/3.16 fof(c10,plain,(![P]:(~ip(P)|iext(uri_rdfs_subPropertyOf,P,P))),inference(fof_nnf,[status(thm)],[rdfs_subpropertyof_reflex])).
% 2.99/3.16 fof(c11,plain,(![X5]:(~ip(X5)|iext(uri_rdfs_subPropertyOf,X5,X5))),inference(variable_rename,[status(thm)],[c10])).
% 2.99/3.16 cnf(c12,plain,~ip(X50)|iext(uri_rdfs_subPropertyOf,X50,X50),inference(split_conjunct,[status(thm)],[c11])).
% 2.99/3.16 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)).
% 2.99/3.16 fof(c122,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])).
% 2.99/3.16 fof(c123,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)],[c122])).
% 2.99/3.16 fof(c125,plain,(![X38]:(![X39]:((~iext(uri_rdf_type,X38,uri_rdf_Property)|ip(X38))&(~ip(X39)|iext(uri_rdf_type,X39,uri_rdf_Property))))),inference(shift_quantors,[status(thm)],[fof(c124,plain,((![X38]:(~iext(uri_rdf_type,X38,uri_rdf_Property)|ip(X38)))&(![X39]:(~ip(X39)|iext(uri_rdf_type,X39,uri_rdf_Property)))),inference(variable_rename,[status(thm)],[c123])).])).
% 2.99/3.16 cnf(c126,plain,~iext(uri_rdf_type,X94,uri_rdf_Property)|ip(X94),inference(split_conjunct,[status(thm)],[c125])).
% 2.99/3.16 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)).
% 2.99/3.16 fof(c105,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])).
% 2.99/3.16 fof(c106,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)],[c105])).
% 2.99/3.16 fof(c108,plain,(![X34]:(![X35]:(![X36]:(![X37]:((~iext(uri_rdf_type,X34,X35)|icext(X35,X34))&(~icext(X37,X36)|iext(uri_rdf_type,X36,X37))))))),inference(shift_quantors,[status(thm)],[fof(c107,plain,((![X34]:(![X35]:(~iext(uri_rdf_type,X34,X35)|icext(X35,X34))))&(![X36]:(![X37]:(~icext(X37,X36)|iext(uri_rdf_type,X36,X37))))),inference(variable_rename,[status(thm)],[c106])).])).
% 2.99/3.16 cnf(c110,plain,~icext(X90,X91)|iext(uri_rdf_type,X91,X90),inference(split_conjunct,[status(thm)],[c108])).
% 2.99/3.16 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)).
% 2.99/3.16 cnf(c47,plain,iext(uri_rdfs_domain,uri_rdfs_range,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_range_domain])).
% 2.99/3.16 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)).
% 2.99/3.16 fof(c68,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])).
% 2.99/3.16 fof(c69,plain,(![P]:(![C]:(![X]:((~iext(uri_rdfs_domain,P,C)|(![Y]:~iext(P,X,Y)))|icext(C,X))))),inference(shift_quantors,[status(thm)],[c68])).
% 2.99/3.16 fof(c71,plain,(![X27]:(![X28]:(![X29]:(![X30]:((~iext(uri_rdfs_domain,X27,X28)|~iext(X27,X29,X30))|icext(X28,X29)))))),inference(shift_quantors,[status(thm)],[fof(c70,plain,(![X27]:(![X28]:(![X29]:((~iext(uri_rdfs_domain,X27,X28)|(![X30]:~iext(X27,X29,X30)))|icext(X28,X29))))),inference(variable_rename,[status(thm)],[c69])).])).
% 2.99/3.16 cnf(c72,plain,~iext(uri_rdfs_domain,X83,X81)|~iext(X83,X82,X84)|icext(X81,X82),inference(split_conjunct,[status(thm)],[c71])).
% 2.99/3.16 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)).
% 2.99/3.16 cnf(c118,plain,iext(uri_rdfs_range,uri_rdfs_comment,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[rdfs_annotation_comment_range])).
% 2.99/3.16 cnf(c404,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X297)|icext(X297,uri_rdfs_comment),inference(resolution,[status(thm)],[c118, c72])).
% 2.99/3.16 cnf(c1245,plain,icext(uri_rdf_Property,uri_rdfs_comment),inference(resolution,[status(thm)],[c404, c47])).
% 2.99/3.16 cnf(c1247,plain,iext(uri_rdf_type,uri_rdfs_comment,uri_rdf_Property),inference(resolution,[status(thm)],[c1245, c110])).
% 2.99/3.16 cnf(c1253,plain,ip(uri_rdfs_comment),inference(resolution,[status(thm)],[c1247, c126])).
% 2.99/3.16 cnf(c1254,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_comment,uri_rdfs_comment),inference(resolution,[status(thm)],[c1253, c12])).
% 2.99/3.16 cnf(c1260,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X620)|iext(X620,uri_rdfs_comment,uri_rdfs_comment),inference(resolution,[status(thm)],[c1254, c20])).
% 2.99/3.16 cnf(c1251,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X619)|iext(X619,uri_rdfs_comment,uri_rdf_Property),inference(resolution,[status(thm)],[c1247, c20])).
% 2.99/3.16 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)).
% 2.99/3.16 cnf(c113,plain,iext(uri_rdfs_range,uri_rdfs_label,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[rdfs_annotation_label_range])).
% 2.99/3.16 cnf(c352,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X281)|icext(X281,uri_rdfs_label),inference(resolution,[status(thm)],[c113, c72])).
% 2.99/3.16 cnf(c1216,plain,icext(uri_rdf_Property,uri_rdfs_label),inference(resolution,[status(thm)],[c352, c47])).
% 2.99/3.16 cnf(c1217,plain,iext(uri_rdf_type,uri_rdfs_label,uri_rdf_Property),inference(resolution,[status(thm)],[c1216, c110])).
% 2.99/3.16 cnf(c1223,plain,ip(uri_rdfs_label),inference(resolution,[status(thm)],[c1217, c126])).
% 2.99/3.16 cnf(c1225,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_label,uri_rdfs_label),inference(resolution,[status(thm)],[c1223, c12])).
% 2.99/3.16 cnf(c1230,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X617)|iext(X617,uri_rdfs_label,uri_rdfs_label),inference(resolution,[status(thm)],[c1225, c20])).
% 2.99/3.16 cnf(c1221,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X616)|iext(X616,uri_rdfs_label,uri_rdf_Property),inference(resolution,[status(thm)],[c1217, c20])).
% 2.99/3.16 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)).
% 2.99/3.16 fof(c25,plain,(![C]:(~ic(C)|iext(uri_rdfs_subClassOf,C,C))),inference(fof_nnf,[status(thm)],[rdfs_subclassof_reflex])).
% 2.99/3.16 fof(c26,plain,(![X13]:(~ic(X13)|iext(uri_rdfs_subClassOf,X13,X13))),inference(variable_rename,[status(thm)],[c25])).
% 2.99/3.16 cnf(c27,plain,~ic(X69)|iext(uri_rdfs_subClassOf,X69,X69),inference(split_conjunct,[status(thm)],[c26])).
% 2.99/3.16 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)).
% 2.99/3.16 fof(c61,plain,(![X]:((~ic(X)|icext(uri_rdfs_Class,X))&(~icext(uri_rdfs_Class,X)|ic(X)))),inference(fof_nnf,[status(thm)],[rdfs_ic_def])).
% 2.99/3.16 fof(c62,plain,((![X]:(~ic(X)|icext(uri_rdfs_Class,X)))&(![X]:(~icext(uri_rdfs_Class,X)|ic(X)))),inference(shift_quantors,[status(thm)],[c61])).
% 2.99/3.16 fof(c64,plain,(![X25]:(![X26]:((~ic(X25)|icext(uri_rdfs_Class,X25))&(~icext(uri_rdfs_Class,X26)|ic(X26))))),inference(shift_quantors,[status(thm)],[fof(c63,plain,((![X25]:(~ic(X25)|icext(uri_rdfs_Class,X25)))&(![X26]:(~icext(uri_rdfs_Class,X26)|ic(X26)))),inference(variable_rename,[status(thm)],[c62])).])).
% 2.99/3.16 cnf(c66,plain,~icext(uri_rdfs_Class,X61)|ic(X61),inference(split_conjunct,[status(thm)],[c64])).
% 2.99/3.16 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)).
% 2.99/3.16 cnf(c43,plain,iext(uri_rdfs_range,uri_rdfs_range,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_range_range])).
% 2.99/3.16 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)).
% 2.99/3.16 fof(c44,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])).
% 2.99/3.16 fof(c45,plain,(![X17]:(![X18]:(![X19]:(![X20]:((~iext(uri_rdfs_range,X17,X18)|~iext(X17,X19,X20))|icext(X18,X20)))))),inference(variable_rename,[status(thm)],[c44])).
% 2.99/3.16 cnf(c46,plain,~iext(uri_rdfs_range,X79,X80)|~iext(X79,X78,X77)|icext(X80,X77),inference(split_conjunct,[status(thm)],[c45])).
% 2.99/3.16 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)).
% 2.99/3.16 cnf(c98,plain,iext(uri_rdfs_range,uri_rdf_rest,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdfs_collection_rest_range])).
% 2.99/3.16 cnf(c325,plain,~iext(uri_rdfs_range,uri_rdfs_range,X261)|icext(X261,uri_rdf_List),inference(resolution,[status(thm)],[c98, c46])).
% 2.99/3.16 cnf(c1176,plain,icext(uri_rdfs_Class,uri_rdf_List),inference(resolution,[status(thm)],[c325, c43])).
% 2.99/3.16 cnf(c1178,plain,ic(uri_rdf_List),inference(resolution,[status(thm)],[c1176, c66])).
% 2.99/3.16 cnf(c1182,plain,iext(uri_rdfs_subClassOf,uri_rdf_List,uri_rdf_List),inference(resolution,[status(thm)],[c1178, c27])).
% 2.99/3.16 cnf(c1203,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X614)|iext(X614,uri_rdf_List,uri_rdf_List),inference(resolution,[status(thm)],[c1182, c20])).
% 2.99/3.16 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)).
% 2.99/3.16 fof(c22,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])).
% 2.99/3.16 fof(c23,plain,(![X10]:(![X11]:(![X12]:((~iext(uri_rdfs_subClassOf,X10,X11)|~iext(uri_rdfs_subClassOf,X11,X12))|iext(uri_rdfs_subClassOf,X10,X12))))),inference(variable_rename,[status(thm)],[c22])).
% 2.99/3.16 cnf(c24,plain,~iext(uri_rdfs_subClassOf,X67,X68)|~iext(uri_rdfs_subClassOf,X68,X66)|iext(uri_rdfs_subClassOf,X67,X66),inference(split_conjunct,[status(thm)],[c23])).
% 2.99/3.16 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)).
% 2.99/3.16 fof(c102,plain,(![C]:(~ic(C)|iext(uri_rdfs_subClassOf,C,uri_rdfs_Resource))),inference(fof_nnf,[status(thm)],[rdfs_class_instsub_resource])).
% 2.99/3.16 fof(c103,plain,(![X33]:(~ic(X33)|iext(uri_rdfs_subClassOf,X33,uri_rdfs_Resource))),inference(variable_rename,[status(thm)],[c102])).
% 2.99/3.16 cnf(c104,plain,~ic(X87)|iext(uri_rdfs_subClassOf,X87,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[c103])).
% 2.99/3.16 cnf(c1180,plain,iext(uri_rdfs_subClassOf,uri_rdf_List,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1178, c104])).
% 2.99/3.16 cnf(c1196,plain,~iext(uri_rdfs_subClassOf,X613,uri_rdf_List)|iext(uri_rdfs_subClassOf,X613,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1180, c24])).
% 2.99/3.16 cnf(c1194,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X612)|iext(X612,uri_rdf_List,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1180, c20])).
% 2.99/3.16 cnf(c1177,plain,iext(uri_rdf_type,uri_rdf_List,uri_rdfs_Class),inference(resolution,[status(thm)],[c1176, c110])).
% 2.99/3.16 cnf(c1186,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X611)|iext(X611,uri_rdf_List,uri_rdfs_Class),inference(resolution,[status(thm)],[c1177, c20])).
% 2.99/3.16 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)).
% 2.99/3.16 cnf(c39,plain,iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_reification_predicate_range])).
% 2.99/3.16 cnf(c271,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X226)|icext(X226,uri_rdf_predicate),inference(resolution,[status(thm)],[c72, c39])).
% 2.99/3.16 cnf(c1134,plain,icext(uri_rdf_Property,uri_rdf_predicate),inference(resolution,[status(thm)],[c271, c47])).
% 2.99/3.16 cnf(c1135,plain,iext(uri_rdf_type,uri_rdf_predicate,uri_rdf_Property),inference(resolution,[status(thm)],[c1134, c110])).
% 2.99/3.16 cnf(c1138,plain,ip(uri_rdf_predicate),inference(resolution,[status(thm)],[c1135, c126])).
% 2.99/3.16 cnf(c1142,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_predicate,uri_rdf_predicate),inference(resolution,[status(thm)],[c1138, c12])).
% 2.99/3.16 cnf(c1148,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X609)|iext(X609,uri_rdf_predicate,uri_rdf_predicate),inference(resolution,[status(thm)],[c1142, c20])).
% 2.99/3.16 cnf(c1141,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X608)|iext(X608,uri_rdf_predicate,uri_rdf_Property),inference(resolution,[status(thm)],[c1135, c20])).
% 2.99/3.16 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)).
% 2.99/3.16 cnf(c5,plain,iext(uri_rdfs_range,uri_rdf_type,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_type_range])).
% 2.99/3.16 fof(testcase_premise_fullish_011_Entity_Types_as_Classes,axiom,((iext(uri_owl_disjointWith,uri_owl_Class,uri_owl_ObjectProperty)&iext(uri_rdf_type,uri_ex_x,uri_owl_Class))&iext(uri_rdf_type,uri_ex_x,uri_owl_ObjectProperty)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', testcase_premise_fullish_011_Entity_Types_as_Classes)).
% 2.99/3.16 cnf(c2,plain,iext(uri_rdf_type,uri_ex_x,uri_owl_ObjectProperty),inference(split_conjunct,[status(thm)],[testcase_premise_fullish_011_Entity_Types_as_Classes])).
% 2.99/3.16 cnf(c229,plain,~iext(uri_rdfs_range,uri_rdf_type,X157)|icext(X157,uri_owl_ObjectProperty),inference(resolution,[status(thm)],[c46, c2])).
% 2.99/3.16 cnf(c951,plain,icext(uri_rdfs_Class,uri_owl_ObjectProperty),inference(resolution,[status(thm)],[c229, c5])).
% 2.99/3.16 cnf(c953,plain,ic(uri_owl_ObjectProperty),inference(resolution,[status(thm)],[c951, c66])).
% 2.99/3.16 cnf(c956,plain,iext(uri_rdfs_subClassOf,uri_owl_ObjectProperty,uri_owl_ObjectProperty),inference(resolution,[status(thm)],[c953, c27])).
% 2.99/3.16 cnf(c1117,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X607)|iext(X607,uri_owl_ObjectProperty,uri_owl_ObjectProperty),inference(resolution,[status(thm)],[c956, c20])).
% 2.99/3.16 cnf(c954,plain,iext(uri_rdfs_subClassOf,uri_owl_ObjectProperty,uri_rdfs_Resource),inference(resolution,[status(thm)],[c953, c104])).
% 2.99/3.16 cnf(c1109,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X605)|iext(X605,uri_owl_ObjectProperty,uri_rdfs_Resource),inference(resolution,[status(thm)],[c954, c20])).
% 2.99/3.16 cnf(c1102,plain,~iext(uri_rdfs_subClassOf,X604,uri_owl_ObjectProperty)|iext(uri_rdfs_subClassOf,X604,uri_rdfs_Resource),inference(resolution,[status(thm)],[c954, c24])).
% 2.99/3.16 cnf(c952,plain,iext(uri_rdf_type,uri_owl_ObjectProperty,uri_rdfs_Class),inference(resolution,[status(thm)],[c951, c110])).
% 2.99/3.16 cnf(c1101,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X603)|iext(X603,uri_owl_ObjectProperty,uri_rdfs_Class),inference(resolution,[status(thm)],[c952, c20])).
% 2.99/3.16 cnf(c1,plain,iext(uri_rdf_type,uri_ex_x,uri_owl_Class),inference(split_conjunct,[status(thm)],[testcase_premise_fullish_011_Entity_Types_as_Classes])).
% 2.99/3.16 cnf(c226,plain,~iext(uri_rdfs_range,uri_rdf_type,X154)|icext(X154,uri_owl_Class),inference(resolution,[status(thm)],[c46, c1])).
% 2.99/3.16 cnf(c917,plain,icext(uri_rdfs_Class,uri_owl_Class),inference(resolution,[status(thm)],[c226, c5])).
% 2.99/3.16 cnf(c919,plain,ic(uri_owl_Class),inference(resolution,[status(thm)],[c917, c66])).
% 2.99/3.16 cnf(c922,plain,iext(uri_rdfs_subClassOf,uri_owl_Class,uri_owl_Class),inference(resolution,[status(thm)],[c919, c27])).
% 2.99/3.16 cnf(c1095,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X602)|iext(X602,uri_owl_Class,uri_owl_Class),inference(resolution,[status(thm)],[c922, c20])).
% 2.99/3.16 cnf(c920,plain,iext(uri_rdfs_subClassOf,uri_owl_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c919, c104])).
% 2.99/3.16 cnf(c1087,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X600)|iext(X600,uri_owl_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c920, c20])).
% 2.99/3.16 cnf(c1080,plain,~iext(uri_rdfs_subClassOf,X599,uri_owl_Class)|iext(uri_rdfs_subClassOf,X599,uri_rdfs_Resource),inference(resolution,[status(thm)],[c920, c24])).
% 2.99/3.16 cnf(c918,plain,iext(uri_rdf_type,uri_owl_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c917, c110])).
% 2.99/3.16 cnf(c1079,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X598)|iext(X598,uri_owl_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c918, c20])).
% 2.99/3.16 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)).
% 2.99/3.16 cnf(c67,plain,iext(uri_rdfs_range,uri_rdfs_domain,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_domain_range])).
% 2.99/3.16 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)).
% 2.99/3.16 cnf(c42,plain,iext(uri_rdfs_domain,uri_rdf_object,uri_rdfs_Statement),inference(split_conjunct,[status(thm)],[rdfs_reification_object_domain])).
% 2.99/3.16 cnf(c220,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X148)|icext(X148,uri_rdfs_Statement),inference(resolution,[status(thm)],[c46, c42])).
% 2.99/3.16 cnf(c879,plain,icext(uri_rdfs_Class,uri_rdfs_Statement),inference(resolution,[status(thm)],[c220, c67])).
% 2.99/3.16 cnf(c881,plain,ic(uri_rdfs_Statement),inference(resolution,[status(thm)],[c879, c66])).
% 2.99/3.16 cnf(c884,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Statement,uri_rdfs_Statement),inference(resolution,[status(thm)],[c881, c27])).
% 2.99/3.16 cnf(c1074,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X597)|iext(X597,uri_rdfs_Statement,uri_rdfs_Statement),inference(resolution,[status(thm)],[c884, c20])).
% 2.99/3.16 cnf(c882,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Statement,uri_rdfs_Resource),inference(resolution,[status(thm)],[c881, c104])).
% 2.99/3.16 cnf(c1066,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X595)|iext(X595,uri_rdfs_Statement,uri_rdfs_Resource),inference(resolution,[status(thm)],[c882, c20])).
% 2.99/3.16 cnf(c1059,plain,~iext(uri_rdfs_subClassOf,X594,uri_rdfs_Statement)|iext(uri_rdfs_subClassOf,X594,uri_rdfs_Resource),inference(resolution,[status(thm)],[c882, c24])).
% 2.99/3.16 cnf(c880,plain,iext(uri_rdf_type,uri_rdfs_Statement,uri_rdfs_Class),inference(resolution,[status(thm)],[c879, c110])).
% 2.99/3.16 cnf(c1058,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X593)|iext(X593,uri_rdfs_Statement,uri_rdfs_Class),inference(resolution,[status(thm)],[c880, c20])).
% 2.99/3.16 cnf(c127,plain,~ip(X95)|iext(uri_rdf_type,X95,uri_rdf_Property),inference(split_conjunct,[status(thm)],[c125])).
% 2.99/3.16 cnf(c19,plain,~iext(uri_rdfs_subPropertyOf,X58,X57)|ip(X57),inference(split_conjunct,[status(thm)],[c17])).
% 2.99/3.16 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)).
% 2.99/3.16 fof(c93,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])).
% 2.99/3.16 fof(c94,plain,(![X32]:(~icext(uri_rdfs_ContainerMembershipProperty,X32)|iext(uri_rdfs_subPropertyOf,X32,uri_rdfs_member))),inference(variable_rename,[status(thm)],[c93])).
% 2.99/3.16 cnf(c95,plain,~icext(uri_rdfs_ContainerMembershipProperty,X86)|iext(uri_rdfs_subPropertyOf,X86,uri_rdfs_member),inference(split_conjunct,[status(thm)],[c94])).
% 2.99/3.16 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)).
% 2.99/3.16 cnf(c82,plain,iext(uri_rdf_type,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),inference(split_conjunct,[status(thm)],[rdfs_container_n_type_002])).
% 2.99/3.16 cnf(c109,plain,~iext(uri_rdf_type,X88,X89)|icext(X89,X88),inference(split_conjunct,[status(thm)],[c108])).
% 2.99/3.16 cnf(c366,plain,icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__2),inference(resolution,[status(thm)],[c109, c82])).
% 2.99/3.16 cnf(c373,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__2,uri_rdfs_member),inference(resolution,[status(thm)],[c366, c95])).
% 2.99/3.16 cnf(c744,plain,ip(uri_rdfs_member),inference(resolution,[status(thm)],[c373, c19])).
% 2.99/3.16 cnf(c752,plain,iext(uri_rdf_type,uri_rdfs_member,uri_rdf_Property),inference(resolution,[status(thm)],[c744, c127])).
% 2.99/3.16 cnf(c1052,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X592)|iext(X592,uri_rdfs_member,uri_rdf_Property),inference(resolution,[status(thm)],[c752, c20])).
% 2.99/3.16 cnf(c751,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_member,uri_rdfs_member),inference(resolution,[status(thm)],[c744, c12])).
% 2.99/3.16 cnf(c1046,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X591)|iext(X591,uri_rdfs_member,uri_rdfs_member),inference(resolution,[status(thm)],[c751, c20])).
% 2.99/3.16 cnf(c65,plain,~ic(X60)|icext(uri_rdfs_Class,X60),inference(split_conjunct,[status(thm)],[c64])).
% 2.99/3.16 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)).
% 2.99/3.16 fof(c29,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])).
% 2.99/3.16 fof(c31,plain,(![X14]:(![X15]:(![X16]:(~iext(uri_rdfs_subClassOf,X14,X15)|((ic(X14)&ic(X15))&(~icext(X14,X16)|icext(X15,X16))))))),inference(shift_quantors,[status(thm)],[fof(c30,plain,(![X14]:(![X15]:(~iext(uri_rdfs_subClassOf,X14,X15)|((ic(X14)&ic(X15))&(![X16]:(~icext(X14,X16)|icext(X15,X16))))))),inference(variable_rename,[status(thm)],[c29])).])).
% 2.99/3.16 fof(c32,plain,(![X14]:(![X15]:(![X16]:(((~iext(uri_rdfs_subClassOf,X14,X15)|ic(X14))&(~iext(uri_rdfs_subClassOf,X14,X15)|ic(X15)))&(~iext(uri_rdfs_subClassOf,X14,X15)|(~icext(X14,X16)|icext(X15,X16))))))),inference(distribute,[status(thm)],[c31])).
% 2.99/3.16 cnf(c34,plain,~iext(uri_rdfs_subClassOf,X72,X73)|ic(X73),inference(split_conjunct,[status(thm)],[c32])).
% 2.99/3.16 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)).
% 2.99/3.16 cnf(c79,plain,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[rdfs_dat_xmlliteral_sub])).
% 2.99/3.16 cnf(c200,plain,ic(uri_rdfs_Literal),inference(resolution,[status(thm)],[c34, c79])).
% 2.99/3.16 cnf(c342,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Literal,uri_rdfs_Resource),inference(resolution,[status(thm)],[c104, c200])).
% 2.99/3.16 cnf(c645,plain,ic(uri_rdfs_Resource),inference(resolution,[status(thm)],[c342, c34])).
% 2.99/3.16 cnf(c651,plain,icext(uri_rdfs_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c645, c65])).
% 2.99/3.16 cnf(c653,plain,iext(uri_rdf_type,uri_rdfs_Resource,uri_rdfs_Class),inference(resolution,[status(thm)],[c651, c110])).
% 2.99/3.16 cnf(c1037,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X589)|iext(X589,uri_rdfs_Resource,uri_rdfs_Class),inference(resolution,[status(thm)],[c653, c20])).
% 2.99/3.16 cnf(c650,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Resource,uri_rdfs_Resource),inference(resolution,[status(thm)],[c645, c104])).
% 2.99/3.16 cnf(c1032,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X588)|iext(X588,uri_rdfs_Resource,uri_rdfs_Resource),inference(resolution,[status(thm)],[c650, c20])).
% 2.99/3.16 cnf(c0,plain,iext(uri_owl_disjointWith,uri_owl_Class,uri_owl_ObjectProperty),inference(split_conjunct,[status(thm)],[testcase_premise_fullish_011_Entity_Types_as_Classes])).
% 2.99/3.16 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)).
% 2.99/3.16 fof(c142,plain,(![S]:(![P]:(![O]:(~iext(P,S,O)|ip(P))))),inference(fof_nnf,[status(thm)],[simple_iext_property])).
% 2.99/3.16 fof(c143,plain,(![S]:(![P]:((![O]:~iext(P,S,O))|ip(P)))),inference(shift_quantors,[status(thm)],[c142])).
% 2.99/3.16 fof(c145,plain,(![X42]:(![X43]:(![X44]:(~iext(X43,X42,X44)|ip(X43))))),inference(shift_quantors,[status(thm)],[fof(c144,plain,(![X42]:(![X43]:((![X44]:~iext(X43,X42,X44))|ip(X43)))),inference(variable_rename,[status(thm)],[c143])).])).
% 2.99/3.16 cnf(c146,plain,~iext(X98,X96,X97)|ip(X98),inference(split_conjunct,[status(thm)],[c145])).
% 2.99/3.16 cnf(c545,plain,ip(uri_owl_disjointWith),inference(resolution,[status(thm)],[c146, c0])).
% 2.99/3.16 cnf(c561,plain,iext(uri_rdf_type,uri_owl_disjointWith,uri_rdf_Property),inference(resolution,[status(thm)],[c545, c127])).
% 2.99/3.16 cnf(c1023,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X586)|iext(X586,uri_owl_disjointWith,uri_rdf_Property),inference(resolution,[status(thm)],[c561, c20])).
% 2.99/3.16 cnf(c560,plain,iext(uri_rdfs_subPropertyOf,uri_owl_disjointWith,uri_owl_disjointWith),inference(resolution,[status(thm)],[c545, c12])).
% 2.99/3.16 cnf(c1016,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X585)|iext(X585,uri_owl_disjointWith,uri_owl_disjointWith),inference(resolution,[status(thm)],[c560, c20])).
% 2.99/3.16 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)).
% 2.99/3.16 cnf(c92,plain,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_container_containermembershipproperty_sub])).
% 2.99/3.16 cnf(c494,plain,ip(uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c146, c92])).
% 2.99/3.16 cnf(c559,plain,iext(uri_rdf_type,uri_rdfs_subClassOf,uri_rdf_Property),inference(resolution,[status(thm)],[c494, c127])).
% 2.99/3.16 cnf(c1006,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X583)|iext(X583,uri_rdfs_subClassOf,uri_rdf_Property),inference(resolution,[status(thm)],[c559, c20])).
% 2.99/3.16 cnf(c558,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c494, c12])).
% 2.99/3.16 cnf(c1000,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X582)|iext(X582,uri_rdfs_subClassOf,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c558, c20])).
% 2.99/3.16 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)).
% 2.99/3.16 cnf(c114,plain,iext(uri_rdfs_domain,uri_rdfs_label,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_label_domain])).
% 2.99/3.16 cnf(c493,plain,ip(uri_rdfs_domain),inference(resolution,[status(thm)],[c146, c114])).
% 2.99/3.16 cnf(c557,plain,iext(uri_rdf_type,uri_rdfs_domain,uri_rdf_Property),inference(resolution,[status(thm)],[c493, c127])).
% 2.99/3.16 cnf(c989,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X580)|iext(X580,uri_rdfs_domain,uri_rdf_Property),inference(resolution,[status(thm)],[c557, c20])).
% 2.99/3.16 cnf(c556,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,uri_rdfs_domain),inference(resolution,[status(thm)],[c493, c12])).
% 2.99/3.16 cnf(c983,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X579)|iext(X579,uri_rdfs_domain,uri_rdfs_domain),inference(resolution,[status(thm)],[c556, c20])).
% 2.99/3.16 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)).
% 2.99/3.16 cnf(c90,plain,iext(uri_rdfs_range,uri_rdfs_member,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_member_range])).
% 2.99/3.16 cnf(c490,plain,ip(uri_rdfs_range),inference(resolution,[status(thm)],[c146, c90])).
% 2.99/3.16 cnf(c555,plain,iext(uri_rdf_type,uri_rdfs_range,uri_rdf_Property),inference(resolution,[status(thm)],[c490, c127])).
% 2.99/3.16 cnf(c962,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X577)|iext(X577,uri_rdfs_range,uri_rdf_Property),inference(resolution,[status(thm)],[c555, c20])).
% 2.99/3.16 cnf(c554,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_range,uri_rdfs_range),inference(resolution,[status(thm)],[c490, c12])).
% 2.99/3.16 cnf(c950,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X576)|iext(X576,uri_rdfs_range,uri_rdfs_range),inference(resolution,[status(thm)],[c554, c20])).
% 2.99/3.16 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)).
% 2.99/3.16 cnf(c115,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_sub])).
% 2.99/3.16 cnf(c489,plain,ip(uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c146, c115])).
% 2.99/3.16 cnf(c553,plain,iext(uri_rdf_type,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c489, c127])).
% 2.99/3.16 cnf(c929,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X574)|iext(X574,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c553, c20])).
% 2.99/3.16 cnf(c552,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c489, c12])).
% 2.99/3.16 cnf(c916,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X573)|iext(X573,uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c552, c20])).
% 2.99/3.16 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)).
% 2.99/3.16 cnf(c136,plain,iext(uri_rdf_type,uri_rdf_first,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_collection_first_type])).
% 2.99/3.16 cnf(c481,plain,ip(uri_rdf_first),inference(resolution,[status(thm)],[c136, c126])).
% 2.99/3.16 cnf(c486,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_first,uri_rdf_first),inference(resolution,[status(thm)],[c481, c12])).
% 2.99/3.16 cnf(c907,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X571)|iext(X571,uri_rdf_first,uri_rdf_first),inference(resolution,[status(thm)],[c486, c20])).
% 2.99/3.16 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)).
% 2.99/3.16 cnf(c134,plain,iext(uri_rdf_type,uri_rdf_rest,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_collection_rest_type])).
% 2.99/3.16 cnf(c468,plain,ip(uri_rdf_rest),inference(resolution,[status(thm)],[c134, c126])).
% 2.99/3.16 cnf(c473,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_rest,uri_rdf_rest),inference(resolution,[status(thm)],[c468, c12])).
% 2.99/3.16 cnf(c900,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X569)|iext(X569,uri_rdf_rest,uri_rdf_rest),inference(resolution,[status(thm)],[c473, c20])).
% 2.99/3.16 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)).
% 2.99/3.16 cnf(c133,plain,iext(uri_rdf_type,uri_rdf__1,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_container_n_type_001])).
% 2.99/3.16 cnf(c460,plain,ip(uri_rdf__1),inference(resolution,[status(thm)],[c133, c126])).
% 2.99/3.16 cnf(c465,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__1,uri_rdf__1),inference(resolution,[status(thm)],[c460, c12])).
% 2.99/3.16 cnf(c892,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X567)|iext(X567,uri_rdf__1,uri_rdf__1),inference(resolution,[status(thm)],[c465, c20])).
% 2.99/3.16 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)).
% 2.99/3.16 cnf(c132,plain,iext(uri_rdf_type,uri_rdf__2,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_container_n_type_002])).
% 2.99/3.16 cnf(c452,plain,ip(uri_rdf__2),inference(resolution,[status(thm)],[c132, c126])).
% 2.99/3.16 cnf(c457,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__2,uri_rdf__2),inference(resolution,[status(thm)],[c452, c12])).
% 2.99/3.16 cnf(c878,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X565)|iext(X565,uri_rdf__2,uri_rdf__2),inference(resolution,[status(thm)],[c457, c20])).
% 2.99/3.16 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)).
% 2.99/3.16 cnf(c131,plain,iext(uri_rdf_type,uri_rdf__3,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_container_n_type_003])).
% 2.99/3.16 cnf(c444,plain,ip(uri_rdf__3),inference(resolution,[status(thm)],[c131, c126])).
% 2.99/3.16 cnf(c449,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__3,uri_rdf__3),inference(resolution,[status(thm)],[c444, c12])).
% 2.99/3.16 cnf(c870,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X563)|iext(X563,uri_rdf__3,uri_rdf__3),inference(resolution,[status(thm)],[c449, c20])).
% 2.99/3.16 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)).
% 2.99/3.16 cnf(c130,plain,iext(uri_rdf_type,uri_rdf_object,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_reification_object_type])).
% 2.99/3.16 cnf(c436,plain,ip(uri_rdf_object),inference(resolution,[status(thm)],[c130, c126])).
% 2.99/3.16 cnf(c441,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_object,uri_rdf_object),inference(resolution,[status(thm)],[c436, c12])).
% 2.99/3.16 cnf(c862,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X561)|iext(X561,uri_rdf_object,uri_rdf_object),inference(resolution,[status(thm)],[c441, c20])).
% 2.99/3.16 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)).
% 2.99/3.16 cnf(c129,plain,iext(uri_rdf_type,uri_rdf_value,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_reification_predicate_type])).
% 2.99/3.16 cnf(c424,plain,ip(uri_rdf_value),inference(resolution,[status(thm)],[c129, c126])).
% 2.99/3.16 cnf(c433,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_value,uri_rdf_value),inference(resolution,[status(thm)],[c424, c12])).
% 2.99/3.16 cnf(c854,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X559)|iext(X559,uri_rdf_value,uri_rdf_value),inference(resolution,[status(thm)],[c433, c20])).
% 2.99/3.16 cnf(c360,plain,ip(uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c115, c19])).
% 2.99/3.16 cnf(c432,plain,iext(uri_rdf_type,uri_rdfs_seeAlso,uri_rdf_Property),inference(resolution,[status(thm)],[c127, c360])).
% 2.99/3.16 cnf(c846,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X557)|iext(X557,uri_rdfs_seeAlso,uri_rdf_Property),inference(resolution,[status(thm)],[c432, c20])).
% 2.99/3.16 cnf(c18,plain,~iext(uri_rdfs_subPropertyOf,X52,X51)|ip(X52),inference(split_conjunct,[status(thm)],[c17])).
% 2.99/3.16 cnf(c358,plain,ip(uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c115, c18])).
% 2.99/3.16 cnf(c430,plain,iext(uri_rdf_type,uri_rdfs_isDefinedBy,uri_rdf_Property),inference(resolution,[status(thm)],[c127, c358])).
% 2.99/3.16 cnf(c838,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X556)|iext(X556,uri_rdfs_isDefinedBy,uri_rdf_Property),inference(resolution,[status(thm)],[c430, c20])).
% 2.99/3.16 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)).
% 2.99/3.16 cnf(c128,plain,iext(uri_rdf_type,uri_rdf_subject,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_reification_subject_type])).
% 2.99/3.16 cnf(c417,plain,ip(uri_rdf_subject),inference(resolution,[status(thm)],[c128, c126])).
% 2.99/3.16 cnf(c422,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_subject,uri_rdf_subject),inference(resolution,[status(thm)],[c417, c12])).
% 2.99/3.16 cnf(c832,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X555)|iext(X555,uri_rdf_subject,uri_rdf_subject),inference(resolution,[status(thm)],[c422, c20])).
% 2.99/3.16 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)).
% 2.99/3.16 cnf(c120,plain,iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_value_type])).
% 2.99/3.16 cnf(c415,plain,ip(uri_rdf_type),inference(resolution,[status(thm)],[c126, c120])).
% 2.99/3.16 cnf(c416,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_type,uri_rdf_type),inference(resolution,[status(thm)],[c415, c12])).
% 2.99/3.16 cnf(c824,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X553)|iext(X553,uri_rdf_type,uri_rdf_type),inference(resolution,[status(thm)],[c416, c20])).
% 2.99/3.16 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)).
% 2.99/3.16 cnf(c81,plain,iext(uri_rdf_type,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),inference(split_conjunct,[status(thm)],[rdfs_container_n_type_003])).
% 2.99/3.16 cnf(c371,plain,icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__3),inference(resolution,[status(thm)],[c109, c81])).
% 2.99/3.16 cnf(c392,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__3,uri_rdfs_member),inference(resolution,[status(thm)],[c371, c95])).
% 2.99/3.16 cnf(c811,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X551)|iext(X551,uri_rdf__3,uri_rdfs_member),inference(resolution,[status(thm)],[c392, c20])).
% 2.99/3.16 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)).
% 2.99/3.16 fof(c7,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])).
% 2.99/3.16 fof(c8,plain,(![X2]:(![X3]:(![X4]:((~iext(uri_rdfs_subPropertyOf,X2,X3)|~iext(uri_rdfs_subPropertyOf,X3,X4))|iext(uri_rdfs_subPropertyOf,X2,X4))))),inference(variable_rename,[status(thm)],[c7])).
% 2.99/3.16 cnf(c9,plain,~iext(uri_rdfs_subPropertyOf,X49,X48)|~iext(uri_rdfs_subPropertyOf,X48,X47)|iext(uri_rdfs_subPropertyOf,X49,X47),inference(split_conjunct,[status(thm)],[c8])).
% 2.99/3.16 cnf(c808,plain,~iext(uri_rdfs_subPropertyOf,X550,uri_rdf__3)|iext(uri_rdfs_subPropertyOf,X550,uri_rdfs_member),inference(resolution,[status(thm)],[c392, c9])).
% 2.99/3.16 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)).
% 2.99/3.16 cnf(c80,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Container),inference(split_conjunct,[status(thm)],[rdfs_container_seq_sub])).
% 2.99/3.16 cnf(c202,plain,ic(uri_rdfs_Container),inference(resolution,[status(thm)],[c34, c80])).
% 2.99/3.16 cnf(c207,plain,icext(uri_rdfs_Class,uri_rdfs_Container),inference(resolution,[status(thm)],[c202, c65])).
% 2.99/3.16 cnf(c390,plain,iext(uri_rdf_type,uri_rdfs_Container,uri_rdfs_Class),inference(resolution,[status(thm)],[c110, c207])).
% 2.99/3.16 cnf(c804,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X549)|iext(X549,uri_rdfs_Container,uri_rdfs_Class),inference(resolution,[status(thm)],[c390, c20])).
% 2.99/3.16 cnf(c33,plain,~iext(uri_rdfs_subClassOf,X70,X71)|ic(X70),inference(split_conjunct,[status(thm)],[c32])).
% 2.99/3.16 cnf(c192,plain,ic(uri_rdfs_Seq),inference(resolution,[status(thm)],[c33, c80])).
% 2.99/3.16 cnf(c197,plain,icext(uri_rdfs_Class,uri_rdfs_Seq),inference(resolution,[status(thm)],[c192, c65])).
% 2.99/3.16 cnf(c387,plain,iext(uri_rdf_type,uri_rdfs_Seq,uri_rdfs_Class),inference(resolution,[status(thm)],[c110, c197])).
% 2.99/3.16 cnf(c799,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X548)|iext(X548,uri_rdfs_Seq,uri_rdfs_Class),inference(resolution,[status(thm)],[c387, c20])).
% 2.99/3.16 cnf(c203,plain,icext(uri_rdfs_Class,uri_rdfs_Literal),inference(resolution,[status(thm)],[c200, c65])).
% 2.99/3.16 cnf(c384,plain,iext(uri_rdf_type,uri_rdfs_Literal,uri_rdfs_Class),inference(resolution,[status(thm)],[c110, c203])).
% 2.99/3.16 cnf(c794,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X547)|iext(X547,uri_rdfs_Literal,uri_rdfs_Class),inference(resolution,[status(thm)],[c384, c20])).
% 2.99/3.16 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)).
% 2.99/3.16 cnf(c74,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_datatype_sub])).
% 2.99/3.16 cnf(c201,plain,ic(uri_rdfs_Class),inference(resolution,[status(thm)],[c34, c74])).
% 2.99/3.16 cnf(c205,plain,icext(uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c201, c65])).
% 2.99/3.16 cnf(c383,plain,iext(uri_rdf_type,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c110, c205])).
% 2.99/3.16 cnf(c789,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X546)|iext(X546,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c383, c20])).
% 2.99/3.16 cnf(c191,plain,ic(uri_rdfs_Datatype),inference(resolution,[status(thm)],[c33, c74])).
% 2.99/3.16 cnf(c195,plain,icext(uri_rdfs_Class,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c191, c65])).
% 2.99/3.16 cnf(c382,plain,iext(uri_rdf_type,uri_rdfs_Datatype,uri_rdfs_Class),inference(resolution,[status(thm)],[c110, c195])).
% 2.99/3.16 cnf(c784,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X545)|iext(X545,uri_rdfs_Datatype,uri_rdfs_Class),inference(resolution,[status(thm)],[c382, c20])).
% 2.99/3.16 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)).
% 2.99/3.16 cnf(c96,plain,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Container),inference(split_conjunct,[status(thm)],[rdfs_container_bag_sub])).
% 2.99/3.16 cnf(c306,plain,ic(uri_rdf_Bag),inference(resolution,[status(thm)],[c96, c33])).
% 2.99/3.16 cnf(c311,plain,icext(uri_rdfs_Class,uri_rdf_Bag),inference(resolution,[status(thm)],[c306, c65])).
% 2.99/3.16 cnf(c379,plain,iext(uri_rdf_type,uri_rdf_Bag,uri_rdfs_Class),inference(resolution,[status(thm)],[c110, c311])).
% 2.99/3.16 cnf(c779,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X544)|iext(X544,uri_rdf_Bag,uri_rdfs_Class),inference(resolution,[status(thm)],[c379, c20])).
% 2.99/3.16 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)).
% 2.99/3.16 cnf(c97,plain,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Container),inference(split_conjunct,[status(thm)],[rdfs_container_alt_sub])).
% 2.99/3.16 cnf(c316,plain,ic(uri_rdf_Alt),inference(resolution,[status(thm)],[c97, c33])).
% 2.99/3.16 cnf(c321,plain,icext(uri_rdfs_Class,uri_rdf_Alt),inference(resolution,[status(thm)],[c316, c65])).
% 2.99/3.16 cnf(c378,plain,iext(uri_rdf_type,uri_rdf_Alt,uri_rdfs_Class),inference(resolution,[status(thm)],[c110, c321])).
% 2.99/3.16 cnf(c774,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X543)|iext(X543,uri_rdf_Alt,uri_rdfs_Class),inference(resolution,[status(thm)],[c378, c20])).
% 2.99/3.16 cnf(c256,plain,ic(uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c92, c33])).
% 2.99/3.16 cnf(c300,plain,icext(uri_rdfs_Class,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c256, c65])).
% 2.99/3.16 cnf(c377,plain,iext(uri_rdf_type,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Class),inference(resolution,[status(thm)],[c110, c300])).
% 2.99/3.16 cnf(c769,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X542)|iext(X542,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Class),inference(resolution,[status(thm)],[c377, c20])).
% 2.99/3.16 cnf(c190,plain,ic(uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c33, c79])).
% 2.99/3.16 cnf(c193,plain,icext(uri_rdfs_Class,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c190, c65])).
% 2.99/3.16 cnf(c376,plain,iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Class),inference(resolution,[status(thm)],[c110, c193])).
% 2.99/3.16 cnf(c764,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X541)|iext(X541,uri_rdf_XMLLiteral,uri_rdfs_Class),inference(resolution,[status(thm)],[c376, c20])).
% 2.99/3.16 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)).
% 2.99/3.16 cnf(c83,plain,iext(uri_rdf_type,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),inference(split_conjunct,[status(thm)],[rdfs_container_n_type_001])).
% 2.99/3.16 cnf(c370,plain,icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__1),inference(resolution,[status(thm)],[c109, c83])).
% 2.99/3.16 cnf(c375,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__1,uri_rdfs_member),inference(resolution,[status(thm)],[c370, c95])).
% 2.99/3.16 cnf(c759,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X540)|iext(X540,uri_rdf__1,uri_rdfs_member),inference(resolution,[status(thm)],[c375, c20])).
% 2.99/3.16 cnf(c756,plain,~iext(uri_rdfs_subPropertyOf,X539,uri_rdf__1)|iext(uri_rdfs_subPropertyOf,X539,uri_rdfs_member),inference(resolution,[status(thm)],[c375, c9])).
% 2.99/3.16 cnf(c749,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X538)|iext(X538,uri_rdf__2,uri_rdfs_member),inference(resolution,[status(thm)],[c373, c20])).
% 2.99/3.16 cnf(c1258,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X537)|icext(X537,uri_rdfs_comment),inference(resolution,[status(thm)],[c1254, c72])).
% 2.99/3.16 cnf(c746,plain,~iext(uri_rdfs_subPropertyOf,X536,uri_rdf__2)|iext(uri_rdfs_subPropertyOf,X536,uri_rdfs_member),inference(resolution,[status(thm)],[c373, c9])).
% 2.99/3.16 cnf(c1257,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X535)|icext(X535,uri_rdfs_comment),inference(resolution,[status(thm)],[c1254, c46])).
% 2.99/3.16 cnf(c365,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_seeAlso,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c360, c12])).
% 2.99/3.16 cnf(c741,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X532)|iext(X532,uri_rdfs_seeAlso,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c365, c20])).
% 2.99/3.16 cnf(c1228,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X531)|icext(X531,uri_rdfs_label),inference(resolution,[status(thm)],[c1225, c72])).
% 2.99/3.16 cnf(c1227,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X530)|icext(X530,uri_rdfs_label),inference(resolution,[status(thm)],[c1225, c46])).
% 2.99/3.16 cnf(c1200,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X525)|icext(X525,uri_rdf_List),inference(resolution,[status(thm)],[c1182, c46])).
% 2.99/3.16 cnf(c364,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c358, c12])).
% 2.99/3.16 cnf(c734,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X524)|iext(X524,uri_rdfs_isDefinedBy,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c364, c20])).
% 2.99/3.16 cnf(c1192,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X523)|icext(X523,uri_rdf_List),inference(resolution,[status(thm)],[c1180, c72])).
% 2.99/3.16 cnf(c1146,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X518)|icext(X518,uri_rdf_predicate),inference(resolution,[status(thm)],[c1142, c72])).
% 2.99/3.16 cnf(c1145,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X517)|icext(X517,uri_rdf_predicate),inference(resolution,[status(thm)],[c1142, c46])).
% 2.99/3.16 cnf(c351,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Resource),inference(resolution,[status(thm)],[c104, c192])).
% 2.99/3.16 cnf(c726,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X516)|iext(X516,uri_rdfs_Seq,uri_rdfs_Resource),inference(resolution,[status(thm)],[c351, c20])).
% 2.99/3.16 cnf(c719,plain,~iext(uri_rdfs_subClassOf,X512,uri_rdfs_Seq)|iext(uri_rdfs_subClassOf,X512,uri_rdfs_Resource),inference(resolution,[status(thm)],[c351, c24])).
% 2.99/3.16 cnf(c1115,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X511)|icext(X511,uri_owl_ObjectProperty),inference(resolution,[status(thm)],[c956, c46])).
% 2.99/3.16 cnf(c1108,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X510)|icext(X510,uri_owl_ObjectProperty),inference(resolution,[status(thm)],[c954, c72])).
% 2.99/3.16 cnf(c350,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Resource),inference(resolution,[status(thm)],[c104, c191])).
% 2.99/3.16 cnf(c718,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X508)|iext(X508,uri_rdfs_Datatype,uri_rdfs_Resource),inference(resolution,[status(thm)],[c350, c20])).
% 2.99/3.16 cnf(c711,plain,~iext(uri_rdfs_subClassOf,X504,uri_rdfs_Datatype)|iext(uri_rdfs_subClassOf,X504,uri_rdfs_Resource),inference(resolution,[status(thm)],[c350, c24])).
% 2.99/3.16 cnf(c1093,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X503)|icext(X503,uri_owl_Class),inference(resolution,[status(thm)],[c922, c46])).
% 2.99/3.16 cnf(c1086,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X502)|icext(X502,uri_owl_Class),inference(resolution,[status(thm)],[c920, c72])).
% 2.99/3.16 cnf(c349,plain,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Resource),inference(resolution,[status(thm)],[c104, c316])).
% 2.99/3.16 cnf(c710,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X500)|iext(X500,uri_rdf_Alt,uri_rdfs_Resource),inference(resolution,[status(thm)],[c349, c20])).
% 2.99/3.16 cnf(c703,plain,~iext(uri_rdfs_subClassOf,X496,uri_rdf_Alt)|iext(uri_rdfs_subClassOf,X496,uri_rdfs_Resource),inference(resolution,[status(thm)],[c349, c24])).
% 2.99/3.16 cnf(c1072,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X495)|icext(X495,uri_rdfs_Statement),inference(resolution,[status(thm)],[c884, c46])).
% 2.99/3.16 cnf(c1065,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X494)|icext(X494,uri_rdfs_Statement),inference(resolution,[status(thm)],[c882, c72])).
% 2.99/3.16 cnf(c348,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Container,uri_rdfs_Resource),inference(resolution,[status(thm)],[c104, c202])).
% 2.99/3.16 cnf(c702,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X492)|iext(X492,uri_rdfs_Container,uri_rdfs_Resource),inference(resolution,[status(thm)],[c348, c20])).
% 2.99/3.16 cnf(c695,plain,~iext(uri_rdfs_subClassOf,X490,uri_rdfs_Container)|iext(uri_rdfs_subClassOf,X490,uri_rdfs_Resource),inference(resolution,[status(thm)],[c348, c24])).
% 2.99/3.16 cnf(c347,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c104, c201])).
% 2.99/3.16 cnf(c694,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X486)|iext(X486,uri_rdfs_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c347, c20])).
% 2.99/3.16 cnf(c1045,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X485)|icext(X485,uri_rdfs_member),inference(resolution,[status(thm)],[c751, c72])).
% 2.99/3.16 cnf(c687,plain,~iext(uri_rdfs_subClassOf,X482,uri_rdfs_Class)|iext(uri_rdfs_subClassOf,X482,uri_rdfs_Resource),inference(resolution,[status(thm)],[c347, c24])).
% 2.99/3.16 cnf(c1031,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X480)|icext(X480,uri_rdfs_Resource),inference(resolution,[status(thm)],[c650, c72])).
% 2.99/3.16 cnf(c346,plain,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Resource),inference(resolution,[status(thm)],[c104, c190])).
% 2.99/3.16 cnf(c686,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X478)|iext(X478,uri_rdf_XMLLiteral,uri_rdfs_Resource),inference(resolution,[status(thm)],[c346, c20])).
% 2.99/3.16 cnf(c1015,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X475)|icext(X475,uri_owl_disjointWith),inference(resolution,[status(thm)],[c560, c72])).
% 2.99/3.16 cnf(c679,plain,~iext(uri_rdfs_subClassOf,X474,uri_rdf_XMLLiteral)|iext(uri_rdfs_subClassOf,X474,uri_rdfs_Resource),inference(resolution,[status(thm)],[c346, c24])).
% 2.99/3.16 cnf(c1014,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X473)|icext(X473,uri_owl_disjointWith),inference(resolution,[status(thm)],[c560, c46])).
% 2.99/3.16 cnf(c345,plain,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Resource),inference(resolution,[status(thm)],[c104, c306])).
% 2.99/3.16 cnf(c678,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X470)|iext(X470,uri_rdf_Bag,uri_rdfs_Resource),inference(resolution,[status(thm)],[c345, c20])).
% 2.99/3.16 cnf(c999,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X469)|icext(X469,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c558, c72])).
% 2.99/3.16 cnf(c998,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X468)|icext(X468,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c558, c46])).
% 2.99/3.16 cnf(c671,plain,~iext(uri_rdfs_subClassOf,X467,uri_rdf_Bag)|iext(uri_rdfs_subClassOf,X467,uri_rdfs_Resource),inference(resolution,[status(thm)],[c345, c24])).
% 2.99/3.16 cnf(c981,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X464)|icext(X464,uri_rdfs_domain),inference(resolution,[status(thm)],[c556, c72])).
% 2.99/3.16 cnf(c344,plain,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Resource),inference(resolution,[status(thm)],[c104, c256])).
% 2.99/3.16 cnf(c670,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X463)|iext(X463,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Resource),inference(resolution,[status(thm)],[c344, c20])).
% 2.99/3.16 cnf(c979,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X462)|icext(X462,uri_rdfs_domain),inference(resolution,[status(thm)],[c556, c46])).
% 2.99/3.16 cnf(c663,plain,~iext(uri_rdfs_subClassOf,X459,uri_rdfs_ContainerMembershipProperty)|iext(uri_rdfs_subClassOf,X459,uri_rdfs_Resource),inference(resolution,[status(thm)],[c344, c24])).
% 2.99/3.16 cnf(c949,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X458)|icext(X458,uri_rdfs_range),inference(resolution,[status(thm)],[c554, c72])).
% 2.99/3.16 cnf(c948,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X457)|icext(X457,uri_rdfs_range),inference(resolution,[status(thm)],[c554, c46])).
% 2.99/3.16 cnf(c255,plain,ic(uri_rdf_Property),inference(resolution,[status(thm)],[c92, c34])).
% 2.99/3.16 cnf(c343,plain,iext(uri_rdfs_subClassOf,uri_rdf_Property,uri_rdfs_Resource),inference(resolution,[status(thm)],[c104, c255])).
% 2.99/3.16 cnf(c662,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X456)|iext(X456,uri_rdf_Property,uri_rdfs_Resource),inference(resolution,[status(thm)],[c343, c20])).
% 2.99/3.16 cnf(c655,plain,~iext(uri_rdfs_subClassOf,X453,uri_rdf_Property)|iext(uri_rdfs_subClassOf,X453,uri_rdfs_Resource),inference(resolution,[status(thm)],[c343, c24])).
% 2.99/3.16 cnf(c915,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X452)|icext(X452,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c552, c72])).
% 2.99/3.16 cnf(c913,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X451)|icext(X451,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c552, c46])).
% 2.99/3.16 cnf(c649,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X450)|iext(X450,uri_rdfs_Literal,uri_rdfs_Resource),inference(resolution,[status(thm)],[c342, c20])).
% 2.99/3.16 cnf(c906,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X449)|icext(X449,uri_rdf_first),inference(resolution,[status(thm)],[c486, c72])).
% 2.99/3.16 cnf(c905,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X448)|icext(X448,uri_rdf_first),inference(resolution,[status(thm)],[c486, c46])).
% 2.99/3.16 cnf(c642,plain,~iext(uri_rdfs_subClassOf,X447,uri_rdfs_Literal)|iext(uri_rdfs_subClassOf,X447,uri_rdfs_Resource),inference(resolution,[status(thm)],[c342, c24])).
% 2.99/3.16 cnf(c899,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X446)|icext(X446,uri_rdf_rest),inference(resolution,[status(thm)],[c473, c72])).
% 2.99/3.16 cnf(c898,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X445)|icext(X445,uri_rdf_rest),inference(resolution,[status(thm)],[c473, c46])).
% 2.99/3.16 cnf(c322,plain,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdf_Alt),inference(resolution,[status(thm)],[c316, c27])).
% 2.99/3.16 cnf(c641,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X444)|iext(X444,uri_rdf_Alt,uri_rdf_Alt),inference(resolution,[status(thm)],[c322, c20])).
% 2.99/3.16 cnf(c890,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X442)|icext(X442,uri_rdf__1),inference(resolution,[status(thm)],[c465, c46])).
% 2.99/3.16 cnf(c876,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X439)|icext(X439,uri_rdf__2),inference(resolution,[status(thm)],[c457, c46])).
% 2.99/3.16 cnf(c868,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X437)|icext(X437,uri_rdf__3),inference(resolution,[status(thm)],[c449, c46])).
% 2.99/3.16 cnf(c312,plain,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdf_Bag),inference(resolution,[status(thm)],[c306, c27])).
% 2.99/3.16 cnf(c633,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X436)|iext(X436,uri_rdf_Bag,uri_rdf_Bag),inference(resolution,[status(thm)],[c312, c20])).
% 2.99/3.16 cnf(c861,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X435)|icext(X435,uri_rdf_object),inference(resolution,[status(thm)],[c441, c72])).
% 2.99/3.16 cnf(c860,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X434)|icext(X434,uri_rdf_object),inference(resolution,[status(thm)],[c441, c46])).
% 2.99/3.16 cnf(c853,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X432)|icext(X432,uri_rdf_value),inference(resolution,[status(thm)],[c433, c72])).
% 2.99/3.16 cnf(c852,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X431)|icext(X431,uri_rdf_value),inference(resolution,[status(thm)],[c433, c46])).
% 2.99/3.16 cnf(c301,plain,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c256, c27])).
% 2.99/3.16 cnf(c625,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X429)|iext(X429,uri_rdfs_ContainerMembershipProperty,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c301, c20])).
% 2.99/3.16 cnf(c831,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X425)|icext(X425,uri_rdf_subject),inference(resolution,[status(thm)],[c422, c72])).
% 2.99/3.16 cnf(c830,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X423)|icext(X423,uri_rdf_subject),inference(resolution,[status(thm)],[c422, c46])).
% 2.99/3.16 cnf(c823,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X422)|icext(X422,uri_rdf_type),inference(resolution,[status(thm)],[c416, c72])).
% 2.99/3.16 cnf(c261,plain,iext(uri_rdfs_subClassOf,uri_rdf_Property,uri_rdf_Property),inference(resolution,[status(thm)],[c255, c27])).
% 2.99/3.16 cnf(c617,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X421)|iext(X421,uri_rdf_Property,uri_rdf_Property),inference(resolution,[status(thm)],[c261, c20])).
% 2.99/3.17 cnf(c822,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X420)|icext(X420,uri_rdf_type),inference(resolution,[status(thm)],[c416, c46])).
% 2.99/3.17 cnf(c810,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X419)|icext(X419,uri_rdf__3),inference(resolution,[status(thm)],[c392, c72])).
% 2.99/3.17 cnf(c208,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Container,uri_rdfs_Container),inference(resolution,[status(thm)],[c202, c27])).
% 2.99/3.17 cnf(c609,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X412)|iext(X412,uri_rdfs_Container,uri_rdfs_Container),inference(resolution,[status(thm)],[c208, c20])).
% 2.99/3.17 cnf(c206,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c201, c27])).
% 2.99/3.17 cnf(c601,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X401)|iext(X401,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c206, c20])).
% 2.99/3.17 cnf(c758,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X394)|icext(X394,uri_rdf__1),inference(resolution,[status(thm)],[c375, c72])).
% 2.99/3.17 cnf(c204,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Literal,uri_rdfs_Literal),inference(resolution,[status(thm)],[c200, c27])).
% 2.99/3.17 cnf(c593,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X392)|iext(X392,uri_rdfs_Literal,uri_rdfs_Literal),inference(resolution,[status(thm)],[c204, c20])).
% 2.99/3.17 cnf(c748,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X391)|icext(X391,uri_rdf__2),inference(resolution,[status(thm)],[c373, c72])).
% 2.99/3.17 cnf(c747,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X390)|icext(X390,uri_rdfs_member),inference(resolution,[status(thm)],[c373, c46])).
% 2.99/3.17 cnf(c740,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X389)|icext(X389,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c365, c72])).
% 2.99/3.17 cnf(c732,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X385)|icext(X385,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c364, c46])).
% 2.99/3.17 cnf(c198,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Seq),inference(resolution,[status(thm)],[c192, c27])).
% 2.99/3.17 cnf(c585,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X384)|iext(X384,uri_rdfs_Seq,uri_rdfs_Seq),inference(resolution,[status(thm)],[c198, c20])).
% 2.99/3.17 cnf(c196,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c191, c27])).
% 2.99/3.17 cnf(c577,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X373)|iext(X373,uri_rdfs_Datatype,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c196, c20])).
% 2.99/3.17 cnf(c194,plain,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c190, c27])).
% 2.99/3.17 cnf(c569,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X362)|iext(X362,uri_rdf_XMLLiteral,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c194, c20])).
% 2.99/3.17 cnf(c647,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X360)|icext(X360,uri_rdfs_Resource),inference(resolution,[status(thm)],[c342, c46])).
% 2.99/3.17 cnf(c639,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X357)|icext(X357,uri_rdf_Alt),inference(resolution,[status(thm)],[c322, c46])).
% 2.99/3.17 cnf(c631,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X355)|icext(X355,uri_rdf_Bag),inference(resolution,[status(thm)],[c312, c46])).
% 2.99/3.17 cnf(c485,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X354)|iext(X354,uri_rdf_first,uri_rdf_Property),inference(resolution,[status(thm)],[c136, c20])).
% 2.99/3.17 cnf(c623,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X352)|icext(X352,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c301, c46])).
% 2.99/3.17 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)).
% 2.99/3.17 cnf(c135,plain,iext(uri_rdf_type,uri_rdf_nil,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdf_collection_nil_type])).
% 2.99/3.17 cnf(c479,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X351)|iext(X351,uri_rdf_nil,uri_rdf_List),inference(resolution,[status(thm)],[c135, c20])).
% 2.99/3.17 cnf(c616,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X350)|icext(X350,uri_rdf_Property),inference(resolution,[status(thm)],[c261, c72])).
% 2.99/3.17 cnf(c608,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X348)|icext(X348,uri_rdfs_Container),inference(resolution,[status(thm)],[c208, c72])).
% 2.99/3.17 cnf(c472,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X347)|iext(X347,uri_rdf_rest,uri_rdf_Property),inference(resolution,[status(thm)],[c134, c20])).
% 2.99/3.17 cnf(c600,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X345)|icext(X345,uri_rdfs_Class),inference(resolution,[status(thm)],[c206, c72])).
% 2.99/3.17 cnf(c464,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X343)|iext(X343,uri_rdf__1,uri_rdf_Property),inference(resolution,[status(thm)],[c133, c20])).
% 2.99/3.17 cnf(c592,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X342)|icext(X342,uri_rdfs_Literal),inference(resolution,[status(thm)],[c204, c72])).
% 2.99/3.17 cnf(c456,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X339)|iext(X339,uri_rdf__2,uri_rdf_Property),inference(resolution,[status(thm)],[c132, c20])).
% 2.99/3.17 cnf(c583,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X338)|icext(X338,uri_rdfs_Seq),inference(resolution,[status(thm)],[c198, c46])).
% 2.99/3.17 cnf(c448,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X336)|iext(X336,uri_rdf__3,uri_rdf_Property),inference(resolution,[status(thm)],[c131, c20])).
% 2.99/3.17 cnf(c575,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X335)|icext(X335,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c196, c46])).
% 2.99/3.17 cnf(c567,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X333)|icext(X333,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c194, c46])).
% 2.99/3.17 cnf(c440,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X332)|iext(X332,uri_rdf_object,uri_rdf_Property),inference(resolution,[status(thm)],[c130, c20])).
% 2.99/3.17 cnf(c477,plain,~iext(uri_rdfs_range,uri_rdf_type,X329)|icext(X329,uri_rdf_List),inference(resolution,[status(thm)],[c135, c46])).
% 2.99/3.17 cnf(c428,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X328)|iext(X328,uri_rdf_value,uri_rdf_Property),inference(resolution,[status(thm)],[c129, c20])).
% 2.99/3.17 cnf(c421,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X323)|iext(X323,uri_rdf_subject,uri_rdf_Property),inference(resolution,[status(thm)],[c128, c20])).
% 2.99/3.17 cnf(c413,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X318)|iext(X318,uri_rdf_type,uri_rdf_Property),inference(resolution,[status(thm)],[c120, c20])).
% 2.99/3.17 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)).
% 2.99/3.17 cnf(c119,plain,iext(uri_rdfs_domain,uri_rdfs_comment,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_comment_domain])).
% 2.99/3.17 cnf(c409,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X313)|iext(X313,uri_rdfs_comment,uri_rdfs_Resource),inference(resolution,[status(thm)],[c119, c20])).
% 2.99/3.17 cnf(c406,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X309)|iext(X309,uri_rdfs_comment,uri_rdfs_Literal),inference(resolution,[status(thm)],[c118, c20])).
% 2.99/3.17 cnf(c411,plain,~iext(uri_rdfs_range,uri_rdf_type,X308)|icext(X308,uri_rdf_Property),inference(resolution,[status(thm)],[c120, c46])).
% 2.99/3.17 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)).
% 2.99/3.17 cnf(c117,plain,iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_domain])).
% 2.99/3.17 cnf(c403,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X305)|iext(X305,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(resolution,[status(thm)],[c117, c20])).
% 2.99/3.17 cnf(c407,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X304)|icext(X304,uri_rdfs_comment),inference(resolution,[status(thm)],[c119, c72])).
% 2.99/3.17 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)).
% 2.99/3.17 cnf(c116,plain,iext(uri_rdfs_range,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_range])).
% 2.99/3.17 cnf(c400,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X302)|iext(X302,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(resolution,[status(thm)],[c116, c20])).
% 2.99/3.17 fof(simple_ir,axiom,(![X]:ir(X)),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', simple_ir)).
% 2.99/3.17 fof(c140,plain,(![X41]:ir(X41)),inference(variable_rename,[status(thm)],[simple_ir])).
% 2.99/3.17 cnf(c141,plain,ir(X45),inference(split_conjunct,[status(thm)],[c140])).
% 2.99/3.17 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)).
% 2.99/3.17 fof(c55,plain,(![X]:((~ir(X)|icext(uri_rdfs_Resource,X))&(~icext(uri_rdfs_Resource,X)|ir(X)))),inference(fof_nnf,[status(thm)],[rdfs_ir_def])).
% 2.99/3.17 fof(c56,plain,((![X]:(~ir(X)|icext(uri_rdfs_Resource,X)))&(![X]:(~icext(uri_rdfs_Resource,X)|ir(X)))),inference(shift_quantors,[status(thm)],[c55])).
% 2.99/3.17 fof(c58,plain,(![X23]:(![X24]:((~ir(X23)|icext(uri_rdfs_Resource,X23))&(~icext(uri_rdfs_Resource,X24)|ir(X24))))),inference(shift_quantors,[status(thm)],[fof(c57,plain,((![X23]:(~ir(X23)|icext(uri_rdfs_Resource,X23)))&(![X24]:(~icext(uri_rdfs_Resource,X24)|ir(X24)))),inference(variable_rename,[status(thm)],[c56])).])).
% 2.99/3.17 cnf(c59,plain,~ir(X55)|icext(uri_rdfs_Resource,X55),inference(split_conjunct,[status(thm)],[c58])).
% 2.99/3.17 cnf(c148,plain,icext(uri_rdfs_Resource,X56),inference(resolution,[status(thm)],[c59, c141])).
% 2.99/3.17 cnf(c391,plain,iext(uri_rdf_type,X92,uri_rdfs_Resource),inference(resolution,[status(thm)],[c110, c148])).
% 2.99/3.17 cnf(c397,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X300)|iext(X300,X299,uri_rdfs_Resource),inference(resolution,[status(thm)],[c391, c20])).
% 2.99/3.17 cnf(c363,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X298)|iext(X298,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c115, c20])).
% 2.99/3.17 cnf(c401,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X295)|icext(X295,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c117, c72])).
% 2.99/3.17 cnf(c359,plain,~iext(uri_rdfs_subPropertyOf,X294,uri_rdfs_isDefinedBy)|iext(uri_rdfs_subPropertyOf,X294,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c115, c9])).
% 2.99/3.17 cnf(c398,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X292)|icext(X292,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c116, c72])).
% 2.99/3.17 cnf(c357,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X291)|iext(X291,uri_rdfs_label,uri_rdfs_Resource),inference(resolution,[status(thm)],[c114, c20])).
% 2.99/3.17 cnf(c395,plain,~iext(uri_rdfs_range,uri_rdf_type,X290)|icext(X290,uri_rdfs_Resource),inference(resolution,[status(thm)],[c391, c46])).
% 2.99/3.17 cnf(c362,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X289)|icext(X289,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c115, c46])).
% 2.99/3.17 cnf(c354,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X288)|iext(X288,uri_rdfs_label,uri_rdfs_Literal),inference(resolution,[status(thm)],[c113, c20])).
% 2.99/3.17 cnf(c361,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X287)|icext(X287,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c115, c72])).
% 2.99/3.17 cnf(c355,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X285)|icext(X285,uri_rdfs_label),inference(resolution,[status(thm)],[c114, c72])).
% 2.99/3.17 cnf(c353,plain,~iext(uri_rdfs_range,uri_rdfs_range,X284)|icext(X284,uri_rdfs_Literal),inference(resolution,[status(thm)],[c113, c46])).
% 2.99/3.17 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)).
% 2.99/3.17 cnf(c112,plain,iext(uri_rdfs_domain,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_seealso_domain])).
% 2.99/3.17 cnf(c341,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X283)|iext(X283,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(resolution,[status(thm)],[c112, c20])).
% 2.99/3.17 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)).
% 2.99/3.17 cnf(c111,plain,iext(uri_rdfs_range,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_seealso_range])).
% 2.99/3.17 cnf(c338,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X282)|iext(X282,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(resolution,[status(thm)],[c111, c20])).
% 2.99/3.17 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)).
% 2.99/3.17 cnf(c101,plain,iext(uri_rdfs_domain,uri_rdf_first,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdfs_collection_first_domain])).
% 2.99/3.17 cnf(c335,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X279)|iext(X279,uri_rdf_first,uri_rdf_List),inference(resolution,[status(thm)],[c101, c20])).
% 2.99/3.17 cnf(c339,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X278)|icext(X278,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c112, c72])).
% 2.99/3.17 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)).
% 2.99/3.17 cnf(c100,plain,iext(uri_rdfs_range,uri_rdf_first,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_collection_first_range])).
% 2.99/3.17 cnf(c332,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X276)|iext(X276,uri_rdf_first,uri_rdfs_Resource),inference(resolution,[status(thm)],[c100, c20])).
% 2.99/3.17 cnf(c336,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X275)|icext(X275,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c111, c72])).
% 2.99/3.17 cnf(c333,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X273)|icext(X273,uri_rdf_first),inference(resolution,[status(thm)],[c101, c72])).
% 2.99/3.17 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)).
% 2.99/3.17 cnf(c99,plain,iext(uri_rdfs_domain,uri_rdf_rest,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdfs_collection_rest_domain])).
% 2.99/3.17 cnf(c329,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X272)|iext(X272,uri_rdf_rest,uri_rdf_List),inference(resolution,[status(thm)],[c99, c20])).
% 2.99/3.17 cnf(c330,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X270)|icext(X270,uri_rdf_first),inference(resolution,[status(thm)],[c100, c72])).
% 2.99/3.17 cnf(c328,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X269)|icext(X269,uri_rdf_List),inference(resolution,[status(thm)],[c99, c46])).
% 2.99/3.17 cnf(c327,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X268)|icext(X268,uri_rdf_rest),inference(resolution,[status(thm)],[c99, c72])).
% 2.99/3.17 cnf(c326,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X265)|iext(X265,uri_rdf_rest,uri_rdf_List),inference(resolution,[status(thm)],[c98, c20])).
% 2.99/3.17 cnf(c320,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X264)|iext(X264,uri_rdf_Alt,uri_rdfs_Container),inference(resolution,[status(thm)],[c97, c20])).
% 2.99/3.17 cnf(c318,plain,~iext(uri_rdfs_subClassOf,X263,uri_rdf_Alt)|iext(uri_rdfs_subClassOf,X263,uri_rdfs_Container),inference(resolution,[status(thm)],[c97, c24])).
% 2.99/3.17 cnf(c310,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X262)|iext(X262,uri_rdf_Bag,uri_rdfs_Container),inference(resolution,[status(thm)],[c96, c20])).
% 2.99/3.17 cnf(c324,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X260)|icext(X260,uri_rdf_rest),inference(resolution,[status(thm)],[c98, c72])).
% 2.99/3.17 cnf(c308,plain,~iext(uri_rdfs_subClassOf,X259,uri_rdf_Bag)|iext(uri_rdfs_subClassOf,X259,uri_rdfs_Container),inference(resolution,[status(thm)],[c96, c24])).
% 2.99/3.17 cnf(c317,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X257)|icext(X257,uri_rdf_Alt),inference(resolution,[status(thm)],[c97, c72])).
% 2.99/3.17 cnf(c307,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X255)|icext(X255,uri_rdf_Bag),inference(resolution,[status(thm)],[c96, c72])).
% 2.99/3.17 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)).
% 2.99/3.17 cnf(c86,plain,iext(uri_rdfs_range,uri_rdf__1,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_range_001])).
% 2.99/3.17 cnf(c299,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X254)|icext(X254,uri_rdf__1),inference(resolution,[status(thm)],[c72, c86])).
% 2.99/3.17 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)).
% 2.99/3.17 cnf(c28,plain,iext(uri_rdfs_range,uri_rdfs_subClassOf,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_subclassof_range])).
% 2.99/3.17 cnf(c298,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X253)|icext(X253,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c72, c28])).
% 2.99/3.17 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)).
% 2.99/3.17 cnf(c89,plain,iext(uri_rdfs_domain,uri_rdf__1,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_001])).
% 2.99/3.17 cnf(c297,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X252)|icext(X252,uri_rdf__1),inference(resolution,[status(thm)],[c72, c89])).
% 2.99/3.17 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)).
% 2.99/3.17 cnf(c88,plain,iext(uri_rdfs_domain,uri_rdf__2,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_002])).
% 2.99/3.17 cnf(c296,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X251)|icext(X251,uri_rdf__2),inference(resolution,[status(thm)],[c72, c88])).
% 2.99/3.17 cnf(c295,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X250)|icext(X250,uri_rdfs_range),inference(resolution,[status(thm)],[c72, c47])).
% 2.99/3.17 cnf(c294,plain,~iext(uri_rdfs_domain,uri_owl_disjointWith,X249)|icext(X249,uri_owl_Class),inference(resolution,[status(thm)],[c72, c0])).
% 2.99/3.17 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)).
% 2.99/3.17 cnf(c87,plain,iext(uri_rdfs_domain,uri_rdf__3,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_003])).
% 2.99/3.17 cnf(c292,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X247)|icext(X247,uri_rdf__3),inference(resolution,[status(thm)],[c72, c87])).
% 2.99/3.17 cnf(c291,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X246)|icext(X246,uri_rdfs_range),inference(resolution,[status(thm)],[c72, c43])).
% 2.99/3.17 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)).
% 2.99/3.17 cnf(c85,plain,iext(uri_rdfs_range,uri_rdf__2,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_range_002])).
% 2.99/3.17 cnf(c290,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X245)|icext(X245,uri_rdf__2),inference(resolution,[status(thm)],[c72, c85])).
% 2.99/3.17 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)).
% 2.99/3.17 cnf(c21,plain,iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_subpropertyof_domain])).
% 2.99/3.17 cnf(c289,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X244)|icext(X244,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c72, c21])).
% 2.99/3.17 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)).
% 2.99/3.17 cnf(c6,plain,iext(uri_rdfs_domain,uri_rdf_type,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_type_domain])).
% 2.99/3.17 cnf(c288,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X243)|icext(X243,uri_rdf_type),inference(resolution,[status(thm)],[c72, c6])).
% 2.99/3.17 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)).
% 2.99/3.17 cnf(c40,plain,iext(uri_rdfs_domain,uri_rdf_predicate,uri_rdfs_Statement),inference(split_conjunct,[status(thm)],[rdfs_reification_predicate_domain])).
% 2.99/3.17 cnf(c287,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X242)|icext(X242,uri_rdf_predicate),inference(resolution,[status(thm)],[c72, c40])).
% 2.99/3.17 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)).
% 2.99/3.17 cnf(c84,plain,iext(uri_rdfs_range,uri_rdf__3,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_range_003])).
% 2.99/3.17 cnf(c286,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X241)|icext(X241,uri_rdf__3),inference(resolution,[status(thm)],[c72, c84])).
% 2.99/3.17 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)).
% 2.99/3.17 cnf(c13,plain,iext(uri_rdfs_range,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_subpropertyof_range])).
% 2.99/3.17 cnf(c285,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X240)|icext(X240,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c72, c13])).
% 2.99/3.17 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)).
% 2.99/3.17 cnf(c4,plain,iext(uri_rdfs_domain,uri_rdf_value,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_value_domain])).
% 2.99/3.17 cnf(c282,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X237)|icext(X237,uri_rdf_value),inference(resolution,[status(thm)],[c72, c4])).
% 2.99/3.17 cnf(c281,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X236)|icext(X236,uri_rdfs_Seq),inference(resolution,[status(thm)],[c72, c80])).
% 2.99/3.17 cnf(c280,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X235)|icext(X235,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c72, c74])).
% 2.99/3.17 cnf(c279,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X234)|icext(X234,uri_rdf_type),inference(resolution,[status(thm)],[c72, c5])).
% 2.99/3.17 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)).
% 2.99/3.17 cnf(c3,plain,iext(uri_rdfs_range,uri_rdf_value,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_value_range])).
% 2.99/3.17 cnf(c277,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X232)|icext(X232,uri_rdf_value),inference(resolution,[status(thm)],[c72, c3])).
% 2.99/3.17 cnf(c275,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X230)|icext(X230,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c72, c79])).
% 2.99/3.17 cnf(c274,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X229)|icext(X229,uri_rdfs_domain),inference(resolution,[status(thm)],[c72, c67])).
% 2.99/3.17 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)).
% 2.99/3.17 cnf(c91,plain,iext(uri_rdfs_domain,uri_rdfs_member,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_member_domain])).
% 2.99/3.17 cnf(c272,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X227)|icext(X227,uri_rdfs_member),inference(resolution,[status(thm)],[c72, c91])).
% 2.99/3.17 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)).
% 2.99/3.17 cnf(c38,plain,iext(uri_rdfs_domain,uri_rdf_subject,uri_rdfs_Statement),inference(split_conjunct,[status(thm)],[rdfs_reification_subject_domain])).
% 2.99/3.17 cnf(c270,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X225)|icext(X225,uri_rdf_subject),inference(resolution,[status(thm)],[c72, c38])).
% 2.99/3.17 cnf(c394,plain,~iext(uri_rdfs_domain,uri_rdf_type,X222)|icext(X222,X223),inference(resolution,[status(thm)],[c391, c72])).
% 2.99/3.17 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)).
% 2.99/3.17 cnf(c36,plain,iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_subclassof_domain])).
% 2.99/3.17 cnf(c268,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X216)|icext(X216,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c72, c36])).
% 2.99/3.17 cnf(c267,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X211)|icext(X211,uri_rdf_object),inference(resolution,[status(thm)],[c72, c42])).
% 2.99/3.17 cnf(c266,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X206)|icext(X206,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c72, c92])).
% 2.99/3.17 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)).
% 2.99/3.17 cnf(c37,plain,iext(uri_rdfs_range,uri_rdf_subject,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_reification_subject_range])).
% 2.99/3.17 cnf(c264,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X196)|icext(X196,uri_rdf_subject),inference(resolution,[status(thm)],[c72, c37])).
% 2.99/3.17 cnf(c263,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X191)|icext(X191,uri_rdfs_member),inference(resolution,[status(thm)],[c72, c90])).
% 2.99/3.17 cnf(c35,plain,~iext(uri_rdfs_subClassOf,X74,X76)|~icext(X74,X75)|icext(X76,X75),inference(split_conjunct,[status(thm)],[c32])).
% 2.99/3.17 cnf(c314,plain,~icext(uri_rdf_Alt,X187)|icext(uri_rdfs_Container,X187),inference(resolution,[status(thm)],[c97, c35])).
% 2.99/3.17 cnf(c262,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X186)|icext(X186,uri_rdfs_domain),inference(factor,[status(thm)],[c72])).
% 2.99/3.17 cnf(c304,plain,~icext(uri_rdf_Bag,X185)|icext(uri_rdfs_Container,X185),inference(resolution,[status(thm)],[c96, c35])).
% 2.99/3.17 cnf(c259,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X184)|iext(X184,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),inference(resolution,[status(thm)],[c92, c20])).
% 2.99/3.17 cnf(c258,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X183)|icext(X183,uri_rdf_Property),inference(resolution,[status(thm)],[c92, c46])).
% 2.99/3.17 cnf(c257,plain,~iext(uri_rdfs_subClassOf,X182,uri_rdfs_ContainerMembershipProperty)|iext(uri_rdfs_subClassOf,X182,uri_rdf_Property),inference(resolution,[status(thm)],[c92, c24])).
% 2.99/3.17 cnf(c254,plain,~icext(uri_rdfs_ContainerMembershipProperty,X181)|icext(uri_rdf_Property,X181),inference(resolution,[status(thm)],[c92, c35])).
% 2.99/3.17 cnf(c247,plain,~iext(uri_rdfs_range,uri_owl_disjointWith,X175)|icext(X175,uri_owl_ObjectProperty),inference(resolution,[status(thm)],[c46, c0])).
% 2.99/3.17 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)).
% 2.99/3.17 cnf(c48,plain,iext(uri_rdf_type,uri_rdf_Property,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_property_type])).
% 2.99/3.17 cnf(c246,plain,~iext(uri_rdfs_range,uri_rdf_type,X174)|icext(X174,uri_rdfs_Class),inference(resolution,[status(thm)],[c46, c48])).
% 2.99/3.17 cnf(c1047,plain,icext(uri_rdf_Property,uri_rdfs_member),inference(resolution,[status(thm)],[c752, c109])).
% 2.99/3.17 cnf(c238,plain,~iext(uri_rdfs_range,uri_rdfs_range,X166)|icext(X166,uri_rdf_Property),inference(resolution,[status(thm)],[c46, c13])).
% 2.99/3.17 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)).
% 2.99/3.17 cnf(c73,plain,iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_domain_domain])).
% 2.99/3.17 cnf(c237,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X165)|icext(X165,uri_rdf_Property),inference(resolution,[status(thm)],[c46, c73])).
% 2.99/3.17 cnf(c1018,plain,icext(uri_rdf_Property,uri_owl_disjointWith),inference(resolution,[status(thm)],[c561, c109])).
% 2.99/3.17 cnf(c234,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X162)|icext(X162,uri_rdfs_Container),inference(resolution,[status(thm)],[c46, c80])).
% 2.99/3.17 cnf(c1001,plain,icext(uri_rdf_Property,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c559, c109])).
% 2.99/3.17 cnf(c233,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X161)|icext(X161,uri_rdfs_Class),inference(resolution,[status(thm)],[c46, c74])).
% 2.99/3.17 cnf(c984,plain,icext(uri_rdf_Property,uri_rdfs_domain),inference(resolution,[status(thm)],[c557, c109])).
% 2.99/3.17 cnf(c957,plain,icext(uri_rdf_Property,uri_rdfs_range),inference(resolution,[status(thm)],[c555, c109])).
% 2.99/3.17 cnf(c228,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X156)|icext(X156,uri_rdfs_Literal),inference(resolution,[status(thm)],[c46, c79])).
% 2.99/3.17 cnf(c924,plain,icext(uri_rdf_Property,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c553, c109])).
% 2.99/3.17 cnf(c227,plain,~iext(uri_rdfs_range,uri_rdfs_range,X155)|icext(X155,uri_rdfs_Class),inference(resolution,[status(thm)],[c46, c67])).
% 2.99/3.17 cnf(c225,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X153)|icext(X153,uri_rdfs_Resource),inference(resolution,[status(thm)],[c46, c91])).
% 2.99/3.17 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)).
% 2.99/3.17 cnf(c78,plain,iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Datatype),inference(split_conjunct,[status(thm)],[rdfs_dat_xmlliteral_type])).
% 2.99/3.17 cnf(c222,plain,~iext(uri_rdfs_range,uri_rdf_type,X150)|icext(X150,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c46, c78])).
% 2.99/3.17 cnf(c221,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X149)|icext(X149,uri_rdfs_Class),inference(resolution,[status(thm)],[c46, c36])).
% 2.99/3.17 cnf(c219,plain,~iext(uri_rdfs_range,uri_rdf_type,X147)|icext(X147,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c46, c82])).
% 2.99/3.17 cnf(c217,plain,~iext(uri_rdfs_range,uri_rdfs_range,X145)|icext(X145,uri_rdfs_Resource),inference(resolution,[status(thm)],[c46, c90])).
% 2.99/3.17 cnf(c216,plain,~iext(uri_rdfs_range,uri_rdfs_range,X144)|icext(X144,X144),inference(factor,[status(thm)],[c46])).
% 2.99/3.17 cnf(c841,plain,icext(uri_rdf_Property,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c432, c109])).
% 2.99/3.17 cnf(c212,plain,~icext(uri_rdfs_Seq,X143)|icext(uri_rdfs_Container,X143),inference(resolution,[status(thm)],[c35, c80])).
% 2.99/3.17 cnf(c211,plain,~icext(uri_rdfs_Datatype,X142)|icext(uri_rdfs_Class,X142),inference(resolution,[status(thm)],[c35, c74])).
% 2.99/3.17 cnf(c833,plain,icext(uri_rdf_Property,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c430, c109])).
% 2.99/3.17 cnf(c210,plain,~icext(uri_rdf_XMLLiteral,X141)|icext(uri_rdfs_Literal,X141),inference(resolution,[status(thm)],[c35, c79])).
% 2.99/3.17 cnf(c189,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X140)|iext(X140,uri_rdfs_member,uri_rdfs_Resource),inference(resolution,[status(thm)],[c91, c20])).
% 2.99/3.17 cnf(c188,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X139)|iext(X139,uri_rdfs_member,uri_rdfs_Resource),inference(resolution,[status(thm)],[c90, c20])).
% 2.99/3.17 cnf(c187,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X138)|iext(X138,uri_rdf__1,uri_rdfs_Resource),inference(resolution,[status(thm)],[c89, c20])).
% 2.99/3.17 cnf(c186,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X137)|iext(X137,uri_rdf__2,uri_rdfs_Resource),inference(resolution,[status(thm)],[c88, c20])).
% 2.99/3.17 cnf(c185,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X136)|iext(X136,uri_rdf__3,uri_rdfs_Resource),inference(resolution,[status(thm)],[c87, c20])).
% 2.99/3.17 cnf(c184,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X135)|iext(X135,uri_rdf__1,uri_rdfs_Resource),inference(resolution,[status(thm)],[c86, c20])).
% 2.99/3.17 cnf(c183,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X134)|iext(X134,uri_rdf__2,uri_rdfs_Resource),inference(resolution,[status(thm)],[c85, c20])).
% 2.99/3.17 cnf(c182,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X133)|iext(X133,uri_rdf__3,uri_rdfs_Resource),inference(resolution,[status(thm)],[c84, c20])).
% 2.99/3.17 cnf(c181,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X132)|iext(X132,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c83, c20])).
% 2.99/3.17 cnf(c180,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X131)|iext(X131,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c82, c20])).
% 2.99/3.17 cnf(c179,plain,~iext(uri_rdfs_subClassOf,X130,uri_rdfs_Seq)|iext(uri_rdfs_subClassOf,X130,uri_rdfs_Container),inference(resolution,[status(thm)],[c24, c80])).
% 2.99/3.17 cnf(c178,plain,~iext(uri_rdfs_subClassOf,X129,uri_rdfs_Datatype)|iext(uri_rdfs_subClassOf,X129,uri_rdfs_Class),inference(resolution,[status(thm)],[c24, c74])).
% 2.99/3.17 cnf(c177,plain,~iext(uri_rdfs_subClassOf,X128,uri_rdf_XMLLiteral)|iext(uri_rdfs_subClassOf,X128,uri_rdfs_Literal),inference(resolution,[status(thm)],[c24, c79])).
% 2.99/3.17 cnf(c175,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X126)|iext(X126,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c81, c20])).
% 2.99/3.17 cnf(c174,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X125)|iext(X125,uri_rdfs_Seq,uri_rdfs_Container),inference(resolution,[status(thm)],[c80, c20])).
% 2.99/3.17 cnf(c173,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X124)|iext(X124,uri_rdf_XMLLiteral,uri_rdfs_Literal),inference(resolution,[status(thm)],[c79, c20])).
% 2.99/3.17 cnf(c172,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X123)|iext(X123,uri_rdf_XMLLiteral,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c78, c20])).
% 2.99/3.17 cnf(c171,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X122)|iext(X122,uri_rdfs_Datatype,uri_rdfs_Class),inference(resolution,[status(thm)],[c74, c20])).
% 2.99/3.17 cnf(c170,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X121)|iext(X121,uri_rdfs_subClassOf,uri_rdfs_Class),inference(resolution,[status(thm)],[c20, c28])).
% 2.99/3.17 cnf(c169,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X120)|iext(X120,uri_rdfs_range,uri_rdf_Property),inference(resolution,[status(thm)],[c20, c47])).
% 2.99/3.17 cnf(c168,plain,~iext(uri_rdfs_subPropertyOf,uri_owl_disjointWith,X119)|iext(X119,uri_owl_Class,uri_owl_ObjectProperty),inference(resolution,[status(thm)],[c20, c0])).
% 2.99/3.17 cnf(c167,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X118)|iext(X118,uri_rdf_Property,uri_rdfs_Class),inference(resolution,[status(thm)],[c20, c48])).
% 2.99/3.17 cnf(c166,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X117)|iext(X117,uri_rdfs_range,uri_rdfs_Class),inference(resolution,[status(thm)],[c20, c43])).
% 2.99/3.17 cnf(c165,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X116)|iext(X116,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c20, c21])).
% 2.99/3.17 cnf(c164,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X115)|iext(X115,uri_rdf_type,uri_rdfs_Resource),inference(resolution,[status(thm)],[c20, c6])).
% 2.99/3.17 cnf(c163,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X114)|iext(X114,uri_rdf_predicate,uri_rdfs_Statement),inference(resolution,[status(thm)],[c20, c40])).
% 2.99/3.17 cnf(c162,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X113)|iext(X113,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c20, c13])).
% 2.99/3.17 cnf(c161,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X112)|iext(X112,uri_rdfs_domain,uri_rdf_Property),inference(resolution,[status(thm)],[c20, c73])).
% 2.99/3.17 cnf(c160,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X111)|iext(X111,uri_rdf_value,uri_rdfs_Resource),inference(resolution,[status(thm)],[c20, c4])).
% 2.99/3.17 cnf(c159,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X110)|iext(X110,uri_rdf_type,uri_rdfs_Class),inference(resolution,[status(thm)],[c20, c5])).
% 2.99/3.17 cnf(c158,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X109)|iext(X109,uri_rdf_value,uri_rdfs_Resource),inference(resolution,[status(thm)],[c20, c3])).
% 2.99/3.17 cnf(c157,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X108)|iext(X108,uri_ex_x,uri_owl_ObjectProperty),inference(resolution,[status(thm)],[c20, c2])).
% 2.99/3.17 cnf(c156,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X107)|iext(X107,uri_rdfs_domain,uri_rdfs_Class),inference(resolution,[status(thm)],[c20, c67])).
% 2.99/3.17 cnf(c155,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X106)|iext(X106,uri_ex_x,uri_owl_Class),inference(resolution,[status(thm)],[c20, c1])).
% 2.99/3.17 cnf(c154,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X105)|iext(X105,uri_rdf_predicate,uri_rdfs_Resource),inference(resolution,[status(thm)],[c20, c39])).
% 2.99/3.17 cnf(c153,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X104)|iext(X104,uri_rdf_subject,uri_rdfs_Statement),inference(resolution,[status(thm)],[c20, c38])).
% 2.99/3.17 cnf(c152,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X103)|iext(X103,uri_rdfs_subClassOf,uri_rdfs_Class),inference(resolution,[status(thm)],[c20, c36])).
% 2.99/3.17 cnf(c151,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X102)|iext(X102,uri_rdf_object,uri_rdfs_Statement),inference(resolution,[status(thm)],[c20, c42])).
% 2.99/3.17 cnf(c150,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X101)|iext(X101,uri_rdf_subject,uri_rdfs_Resource),inference(resolution,[status(thm)],[c20, c37])).
% 2.99/3.17 cnf(c149,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X100)|iext(X100,uri_rdfs_subPropertyOf,X100),inference(factor,[status(thm)],[c20])).
% 2.99/3.17 cnf(c484,plain,icext(uri_rdf_Property,uri_rdf_first),inference(resolution,[status(thm)],[c136, c109])).
% 2.99/3.17 cnf(c478,plain,icext(uri_rdf_List,uri_rdf_nil),inference(resolution,[status(thm)],[c135, c109])).
% 2.99/3.17 cnf(c471,plain,icext(uri_rdf_Property,uri_rdf_rest),inference(resolution,[status(thm)],[c134, c109])).
% 2.99/3.17 cnf(c463,plain,icext(uri_rdf_Property,uri_rdf__1),inference(resolution,[status(thm)],[c133, c109])).
% 2.99/3.17 cnf(c455,plain,icext(uri_rdf_Property,uri_rdf__2),inference(resolution,[status(thm)],[c132, c109])).
% 2.99/3.17 cnf(c447,plain,icext(uri_rdf_Property,uri_rdf__3),inference(resolution,[status(thm)],[c131, c109])).
% 2.99/3.17 cnf(c439,plain,icext(uri_rdf_Property,uri_rdf_object),inference(resolution,[status(thm)],[c130, c109])).
% 2.99/3.17 cnf(c427,plain,icext(uri_rdf_Property,uri_rdf_value),inference(resolution,[status(thm)],[c129, c109])).
% 2.99/3.17 cnf(c420,plain,icext(uri_rdf_Property,uri_rdf_subject),inference(resolution,[status(thm)],[c128, c109])).
% 2.99/3.17 cnf(c412,plain,icext(uri_rdf_Property,uri_rdf_type),inference(resolution,[status(thm)],[c120, c109])).
% 2.99/3.17 cnf(c369,plain,icext(uri_owl_ObjectProperty,uri_ex_x),inference(resolution,[status(thm)],[c109, c2])).
% 2.99/3.17 cnf(c368,plain,icext(uri_owl_Class,uri_ex_x),inference(resolution,[status(thm)],[c109, c1])).
% 2.99/3.17 cnf(c367,plain,icext(uri_rdfs_Datatype,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c109, c78])).
% 2.99/3.17 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)).
% 2.99/3.17 fof(c75,plain,(![D]:(~icext(uri_rdfs_Datatype,D)|iext(uri_rdfs_subClassOf,D,uri_rdfs_Literal))),inference(fof_nnf,[status(thm)],[rdfs_datatype_instsub_literal])).
% 2.99/3.17 fof(c76,plain,(![X31]:(~icext(uri_rdfs_Datatype,X31)|iext(uri_rdfs_subClassOf,X31,uri_rdfs_Literal))),inference(variable_rename,[status(thm)],[c75])).
% 2.99/3.17 cnf(c77,plain,~icext(uri_rdfs_Datatype,X85)|iext(uri_rdfs_subClassOf,X85,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[c76])).
% 2.99/3.17 cnf(c260,plain,icext(uri_rdfs_Class,uri_rdf_Property),inference(resolution,[status(thm)],[c255, c65])).
% 2.99/3.17 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)).
% 2.99/3.17 fof(c49,plain,(![X]:((~lv(X)|icext(uri_rdfs_Literal,X))&(~icext(uri_rdfs_Literal,X)|lv(X)))),inference(fof_nnf,[status(thm)],[rdfs_lv_def])).
% 2.99/3.17 fof(c50,plain,((![X]:(~lv(X)|icext(uri_rdfs_Literal,X)))&(![X]:(~icext(uri_rdfs_Literal,X)|lv(X)))),inference(shift_quantors,[status(thm)],[c49])).
% 2.99/3.17 fof(c52,plain,(![X21]:(![X22]:((~lv(X21)|icext(uri_rdfs_Literal,X21))&(~icext(uri_rdfs_Literal,X22)|lv(X22))))),inference(shift_quantors,[status(thm)],[fof(c51,plain,((![X21]:(~lv(X21)|icext(uri_rdfs_Literal,X21)))&(![X22]:(~icext(uri_rdfs_Literal,X22)|lv(X22)))),inference(variable_rename,[status(thm)],[c50])).])).
% 2.99/3.17 cnf(c54,plain,~icext(uri_rdfs_Literal,X54)|lv(X54),inference(split_conjunct,[status(thm)],[c52])).
% 2.99/3.17 cnf(c53,plain,~lv(X53)|icext(uri_rdfs_Literal,X53),inference(split_conjunct,[status(thm)],[c52])).
% 2.99/3.17 % SZS output end Saturation
% 2.99/3.17
% 2.99/3.17 % Initial clauses : 92
% 2.99/3.17 % Processed clauses : 546
% 2.99/3.17 % Factors computed : 5
% 2.99/3.17 % Resolvents computed: 1287
% 2.99/3.17 % Tautologies deleted: 52
% 2.99/3.17 % Forward subsumed : 786
% 2.99/3.17 % Backward subsumed : 3
% 2.99/3.17 % -------- CPU Time ---------
% 2.99/3.17 % User time : 2.791 s
% 2.99/3.17 % System time : 0.016 s
% 2.99/3.17 % Total time : 2.807 s
%------------------------------------------------------------------------------