PyRes---1.5.SAT-Sat.s

%------------------------------------------------------------------------------
% File     : PyRes---1.5
% Problem  : SWB031+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:57 EDT 2024

% Result   : Satisfiable 2.83s 3.02s
% Output   : Saturation 2.83s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.14  % Problem  : SWB031+4 : TPTP v8.1.2. Released v5.2.0.
% 0.04/0.15  % Command  : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36  % Computer : n013.cluster.edu
% 0.14/0.36  % Model    : x86_64 x86_64
% 0.14/0.36  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36  % Memory   : 8042.1875MB
% 0.14/0.36  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36  % CPULimit : 300
% 0.14/0.36  % WCLimit  : 300
% 0.14/0.36  % DateTime : Wed May  8 22:04:53 EDT 2024
% 0.14/0.36  % CPUTime  : 
% 2.83/3.02  % Version:  1.5
% 2.83/3.02  % SZS status Satisfiable
% 2.83/3.02  % SZS output start Saturation
% 2.83/3.02  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.83/3.02  fof(c17,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.83/3.02  fof(c19,plain,(![X8]:(![X9]:(![X10]:(![X11]:(~iext(uri_rdfs_subPropertyOf,X8,X9)|((ip(X8)&ip(X9))&(~iext(X8,X10,X11)|iext(X9,X10,X11)))))))),inference(shift_quantors,[status(thm)],[fof(c18,plain,(![X8]:(![X9]:(~iext(uri_rdfs_subPropertyOf,X8,X9)|((ip(X8)&ip(X9))&(![X10]:(![X11]:(~iext(X8,X10,X11)|iext(X9,X10,X11)))))))),inference(variable_rename,[status(thm)],[c17])).])).
% 2.83/3.02  fof(c20,plain,(![X8]:(![X9]:(![X10]:(![X11]:(((~iext(uri_rdfs_subPropertyOf,X8,X9)|ip(X8))&(~iext(uri_rdfs_subPropertyOf,X8,X9)|ip(X9)))&(~iext(uri_rdfs_subPropertyOf,X8,X9)|(~iext(X8,X10,X11)|iext(X9,X10,X11)))))))),inference(distribute,[status(thm)],[c19])).
% 2.83/3.02  cnf(c23,plain,~iext(uri_rdfs_subPropertyOf,X64,X66)|~iext(X64,X65,X67)|iext(X66,X65,X67),inference(split_conjunct,[status(thm)],[c20])).
% 2.83/3.02  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.83/3.02  fof(c13,plain,(![P]:(~ip(P)|iext(uri_rdfs_subPropertyOf,P,P))),inference(fof_nnf,[status(thm)],[rdfs_subpropertyof_reflex])).
% 2.83/3.02  fof(c14,plain,(![X7]:(~ip(X7)|iext(uri_rdfs_subPropertyOf,X7,X7))),inference(variable_rename,[status(thm)],[c13])).
% 2.83/3.02  cnf(c15,plain,~ip(X52)|iext(uri_rdfs_subPropertyOf,X52,X52),inference(split_conjunct,[status(thm)],[c14])).
% 2.83/3.02  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.83/3.02  fof(c125,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.83/3.02  fof(c126,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)],[c125])).
% 2.83/3.02  fof(c128,plain,(![X40]:(![X41]:((~iext(uri_rdf_type,X40,uri_rdf_Property)|ip(X40))&(~ip(X41)|iext(uri_rdf_type,X41,uri_rdf_Property))))),inference(shift_quantors,[status(thm)],[fof(c127,plain,((![X40]:(~iext(uri_rdf_type,X40,uri_rdf_Property)|ip(X40)))&(![X41]:(~ip(X41)|iext(uri_rdf_type,X41,uri_rdf_Property)))),inference(variable_rename,[status(thm)],[c126])).])).
% 2.83/3.02  cnf(c129,plain,~iext(uri_rdf_type,X96,uri_rdf_Property)|ip(X96),inference(split_conjunct,[status(thm)],[c128])).
% 2.83/3.02  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.83/3.02  fof(c108,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.83/3.02  fof(c109,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)],[c108])).
% 2.83/3.02  fof(c111,plain,(![X36]:(![X37]:(![X38]:(![X39]:((~iext(uri_rdf_type,X36,X37)|icext(X37,X36))&(~icext(X39,X38)|iext(uri_rdf_type,X38,X39))))))),inference(shift_quantors,[status(thm)],[fof(c110,plain,((![X36]:(![X37]:(~iext(uri_rdf_type,X36,X37)|icext(X37,X36))))&(![X38]:(![X39]:(~icext(X39,X38)|iext(uri_rdf_type,X38,X39))))),inference(variable_rename,[status(thm)],[c109])).])).
% 2.83/3.02  cnf(c113,plain,~icext(X93,X92)|iext(uri_rdf_type,X92,X93),inference(split_conjunct,[status(thm)],[c111])).
% 2.83/3.02  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.83/3.02  cnf(c50,plain,iext(uri_rdfs_domain,uri_rdfs_range,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_range_domain])).
% 2.83/3.02  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.83/3.02  fof(c71,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.83/3.02  fof(c72,plain,(![P]:(![C]:(![X]:((~iext(uri_rdfs_domain,P,C)|(![Y]:~iext(P,X,Y)))|icext(C,X))))),inference(shift_quantors,[status(thm)],[c71])).
% 2.83/3.02  fof(c74,plain,(![X29]:(![X30]:(![X31]:(![X32]:((~iext(uri_rdfs_domain,X29,X30)|~iext(X29,X31,X32))|icext(X30,X31)))))),inference(shift_quantors,[status(thm)],[fof(c73,plain,(![X29]:(![X30]:(![X31]:((~iext(uri_rdfs_domain,X29,X30)|(![X32]:~iext(X29,X31,X32)))|icext(X30,X31))))),inference(variable_rename,[status(thm)],[c72])).])).
% 2.83/3.02  cnf(c75,plain,~iext(uri_rdfs_domain,X86,X84)|~iext(X86,X83,X85)|icext(X84,X83),inference(split_conjunct,[status(thm)],[c74])).
% 2.83/3.02  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.83/3.02  cnf(c121,plain,iext(uri_rdfs_range,uri_rdfs_comment,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[rdfs_annotation_comment_range])).
% 2.83/3.02  cnf(c407,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X302)|icext(X302,uri_rdfs_comment),inference(resolution,[status(thm)],[c121, c75])).
% 2.83/3.02  cnf(c1221,plain,icext(uri_rdf_Property,uri_rdfs_comment),inference(resolution,[status(thm)],[c407, c50])).
% 2.83/3.02  cnf(c1223,plain,iext(uri_rdf_type,uri_rdfs_comment,uri_rdf_Property),inference(resolution,[status(thm)],[c1221, c113])).
% 2.83/3.02  cnf(c1229,plain,ip(uri_rdfs_comment),inference(resolution,[status(thm)],[c1223, c129])).
% 2.83/3.02  cnf(c1230,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_comment,uri_rdfs_comment),inference(resolution,[status(thm)],[c1229, c15])).
% 2.83/3.02  cnf(c1239,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X610)|iext(X610,uri_rdfs_comment,uri_rdfs_comment),inference(resolution,[status(thm)],[c1230, c23])).
% 2.83/3.02  cnf(c1228,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X608)|iext(X608,uri_rdfs_comment,uri_rdf_Property),inference(resolution,[status(thm)],[c1223, c23])).
% 2.83/3.02  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.83/3.02  cnf(c116,plain,iext(uri_rdfs_range,uri_rdfs_label,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[rdfs_annotation_label_range])).
% 2.83/3.02  cnf(c359,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X284)|icext(X284,uri_rdfs_label),inference(resolution,[status(thm)],[c116, c75])).
% 2.83/3.02  cnf(c1192,plain,icext(uri_rdf_Property,uri_rdfs_label),inference(resolution,[status(thm)],[c359, c50])).
% 2.83/3.02  cnf(c1193,plain,iext(uri_rdf_type,uri_rdfs_label,uri_rdf_Property),inference(resolution,[status(thm)],[c1192, c113])).
% 2.83/3.02  cnf(c1199,plain,ip(uri_rdfs_label),inference(resolution,[status(thm)],[c1193, c129])).
% 2.83/3.02  cnf(c1201,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_label,uri_rdfs_label),inference(resolution,[status(thm)],[c1199, c15])).
% 2.83/3.02  cnf(c1209,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X607)|iext(X607,uri_rdfs_label,uri_rdfs_label),inference(resolution,[status(thm)],[c1201, c23])).
% 2.83/3.02  cnf(c1198,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X605)|iext(X605,uri_rdfs_label,uri_rdf_Property),inference(resolution,[status(thm)],[c1193, c23])).
% 2.83/3.02  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.83/3.02  fof(c28,plain,(![C]:(~ic(C)|iext(uri_rdfs_subClassOf,C,C))),inference(fof_nnf,[status(thm)],[rdfs_subclassof_reflex])).
% 2.83/3.02  fof(c29,plain,(![X15]:(~ic(X15)|iext(uri_rdfs_subClassOf,X15,X15))),inference(variable_rename,[status(thm)],[c28])).
% 2.83/3.02  cnf(c30,plain,~ic(X71)|iext(uri_rdfs_subClassOf,X71,X71),inference(split_conjunct,[status(thm)],[c29])).
% 2.83/3.02  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.83/3.02  fof(c64,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.83/3.03  fof(c65,plain,((![X]:(~ic(X)|icext(uri_rdfs_Class,X)))&(![X]:(~icext(uri_rdfs_Class,X)|ic(X)))),inference(shift_quantors,[status(thm)],[c64])).
% 2.83/3.03  fof(c67,plain,(![X27]:(![X28]:((~ic(X27)|icext(uri_rdfs_Class,X27))&(~icext(uri_rdfs_Class,X28)|ic(X28))))),inference(shift_quantors,[status(thm)],[fof(c66,plain,((![X27]:(~ic(X27)|icext(uri_rdfs_Class,X27)))&(![X28]:(~icext(uri_rdfs_Class,X28)|ic(X28)))),inference(variable_rename,[status(thm)],[c65])).])).
% 2.83/3.03  cnf(c69,plain,~icext(uri_rdfs_Class,X63)|ic(X63),inference(split_conjunct,[status(thm)],[c67])).
% 2.83/3.03  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.83/3.03  cnf(c46,plain,iext(uri_rdfs_range,uri_rdfs_range,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_range_range])).
% 2.83/3.03  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.83/3.03  fof(c47,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.83/3.03  fof(c48,plain,(![X19]:(![X20]:(![X21]:(![X22]:((~iext(uri_rdfs_range,X19,X20)|~iext(X19,X21,X22))|icext(X20,X22)))))),inference(variable_rename,[status(thm)],[c47])).
% 2.83/3.03  cnf(c49,plain,~iext(uri_rdfs_range,X82,X80)|~iext(X82,X79,X81)|icext(X80,X81),inference(split_conjunct,[status(thm)],[c48])).
% 2.83/3.03  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.83/3.03  cnf(c101,plain,iext(uri_rdfs_range,uri_rdf_rest,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdfs_collection_rest_range])).
% 2.83/3.03  cnf(c332,plain,~iext(uri_rdfs_range,uri_rdfs_range,X263)|icext(X263,uri_rdf_List),inference(resolution,[status(thm)],[c101, c49])).
% 2.83/3.03  cnf(c1151,plain,icext(uri_rdfs_Class,uri_rdf_List),inference(resolution,[status(thm)],[c332, c46])).
% 2.83/3.03  cnf(c1152,plain,ic(uri_rdf_List),inference(resolution,[status(thm)],[c1151, c69])).
% 2.83/3.03  cnf(c1155,plain,iext(uri_rdfs_subClassOf,uri_rdf_List,uri_rdf_List),inference(resolution,[status(thm)],[c1152, c30])).
% 2.83/3.03  cnf(c1177,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X604)|iext(X604,uri_rdf_List,uri_rdf_List),inference(resolution,[status(thm)],[c1155, c23])).
% 2.83/3.03  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.83/3.03  fof(c105,plain,(![C]:(~ic(C)|iext(uri_rdfs_subClassOf,C,uri_rdfs_Resource))),inference(fof_nnf,[status(thm)],[rdfs_class_instsub_resource])).
% 2.83/3.03  fof(c106,plain,(![X35]:(~ic(X35)|iext(uri_rdfs_subClassOf,X35,uri_rdfs_Resource))),inference(variable_rename,[status(thm)],[c105])).
% 2.83/3.03  cnf(c107,plain,~ic(X89)|iext(uri_rdfs_subClassOf,X89,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[c106])).
% 2.83/3.03  cnf(c1154,plain,iext(uri_rdfs_subClassOf,uri_rdf_List,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1152, c107])).
% 2.83/3.03  cnf(c1168,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X602)|iext(X602,uri_rdf_List,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1154, c23])).
% 2.83/3.03  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.83/3.03  fof(c25,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.83/3.03  fof(c26,plain,(![X12]:(![X13]:(![X14]:((~iext(uri_rdfs_subClassOf,X12,X13)|~iext(uri_rdfs_subClassOf,X13,X14))|iext(uri_rdfs_subClassOf,X12,X14))))),inference(variable_rename,[status(thm)],[c25])).
% 2.83/3.03  cnf(c27,plain,~iext(uri_rdfs_subClassOf,X70,X69)|~iext(uri_rdfs_subClassOf,X69,X68)|iext(uri_rdfs_subClassOf,X70,X68),inference(split_conjunct,[status(thm)],[c26])).
% 2.83/3.03  cnf(c1163,plain,~iext(uri_rdfs_subClassOf,X601,uri_rdf_List)|iext(uri_rdfs_subClassOf,X601,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1154, c27])).
% 2.83/3.03  cnf(c1153,plain,iext(uri_rdf_type,uri_rdf_List,uri_rdfs_Class),inference(resolution,[status(thm)],[c1151, c113])).
% 2.83/3.03  cnf(c1162,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X600)|iext(X600,uri_rdf_List,uri_rdfs_Class),inference(resolution,[status(thm)],[c1153, c23])).
% 2.83/3.03  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.83/3.03  cnf(c76,plain,iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_domain_domain])).
% 2.83/3.03  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.83/3.03  cnf(c43,plain,iext(uri_rdfs_domain,uri_rdf_predicate,uri_rdfs_Statement),inference(split_conjunct,[status(thm)],[rdfs_reification_predicate_domain])).
% 2.83/3.03  cnf(c295,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X247)|icext(X247,uri_rdf_predicate),inference(resolution,[status(thm)],[c75, c43])).
% 2.83/3.03  cnf(c1123,plain,icext(uri_rdf_Property,uri_rdf_predicate),inference(resolution,[status(thm)],[c295, c76])).
% 2.83/3.03  cnf(c1124,plain,iext(uri_rdf_type,uri_rdf_predicate,uri_rdf_Property),inference(resolution,[status(thm)],[c1123, c113])).
% 2.83/3.03  cnf(c1130,plain,ip(uri_rdf_predicate),inference(resolution,[status(thm)],[c1124, c129])).
% 2.83/3.03  cnf(c1131,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_predicate,uri_rdf_predicate),inference(resolution,[status(thm)],[c1130, c15])).
% 2.83/3.03  cnf(c1140,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X599)|iext(X599,uri_rdf_predicate,uri_rdf_predicate),inference(resolution,[status(thm)],[c1131, c23])).
% 2.83/3.03  cnf(c1129,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X597)|iext(X597,uri_rdf_predicate,uri_rdf_Property),inference(resolution,[status(thm)],[c1124, c23])).
% 2.83/3.03  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.83/3.03  cnf(c104,plain,iext(uri_rdfs_domain,uri_rdf_first,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdfs_collection_first_domain])).
% 2.83/3.03  fof(testcase_premise_fullish_031_Large_Universe,axiom,(?[BNODE_x]:(?[BNODE_l]:(((iext(uri_owl_equivalentClass,uri_owl_Thing,BNODE_x)&iext(uri_owl_oneOf,BNODE_x,BNODE_l))&iext(uri_rdf_first,BNODE_l,uri_ex_w))&iext(uri_rdf_rest,BNODE_l,uri_rdf_nil)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', testcase_premise_fullish_031_Large_Universe)).
% 2.83/3.03  fof(c0,plain,(?[X2]:(?[X3]:(((iext(uri_owl_equivalentClass,uri_owl_Thing,X2)&iext(uri_owl_oneOf,X2,X3))&iext(uri_rdf_first,X3,uri_ex_w))&iext(uri_rdf_rest,X3,uri_rdf_nil)))),inference(variable_rename,[status(thm)],[testcase_premise_fullish_031_Large_Universe])).
% 2.83/3.03  fof(c1,plain,(((iext(uri_owl_equivalentClass,uri_owl_Thing,skolem0001)&iext(uri_owl_oneOf,skolem0001,skolem0002))&iext(uri_rdf_first,skolem0002,uri_ex_w))&iext(uri_rdf_rest,skolem0002,uri_rdf_nil)),inference(skolemize,[status(esa)],[c0])).
% 2.83/3.03  cnf(c4,plain,iext(uri_rdf_first,skolem0002,uri_ex_w),inference(split_conjunct,[status(thm)],[c1])).
% 2.83/3.03  cnf(c287,plain,~iext(uri_rdfs_domain,uri_rdf_first,X239)|icext(X239,skolem0002),inference(resolution,[status(thm)],[c75, c4])).
% 2.83/3.03  cnf(c1110,plain,icext(uri_rdf_List,skolem0002),inference(resolution,[status(thm)],[c287, c104])).
% 2.83/3.03  cnf(c1111,plain,iext(uri_rdf_type,skolem0002,uri_rdf_List),inference(resolution,[status(thm)],[c1110, c113])).
% 2.83/3.03  cnf(c1116,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X596)|iext(X596,skolem0002,uri_rdf_List),inference(resolution,[status(thm)],[c1111, c23])).
% 2.83/3.03  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.83/3.03  cnf(c70,plain,iext(uri_rdfs_range,uri_rdfs_domain,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_domain_range])).
% 2.83/3.03  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.83/3.03  cnf(c45,plain,iext(uri_rdfs_domain,uri_rdf_object,uri_rdfs_Statement),inference(split_conjunct,[status(thm)],[rdfs_reification_object_domain])).
% 2.83/3.03  cnf(c233,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X160)|icext(X160,uri_rdfs_Statement),inference(resolution,[status(thm)],[c49, c45])).
% 2.83/3.03  cnf(c980,plain,icext(uri_rdfs_Class,uri_rdfs_Statement),inference(resolution,[status(thm)],[c233, c70])).
% 2.83/3.03  cnf(c982,plain,ic(uri_rdfs_Statement),inference(resolution,[status(thm)],[c980, c69])).
% 2.83/3.03  cnf(c985,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Statement,uri_rdfs_Statement),inference(resolution,[status(thm)],[c982, c30])).
% 2.83/3.03  cnf(c1081,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X595)|iext(X595,uri_rdfs_Statement,uri_rdfs_Statement),inference(resolution,[status(thm)],[c985, c23])).
% 2.83/3.03  cnf(c984,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Statement,uri_rdfs_Resource),inference(resolution,[status(thm)],[c982, c107])).
% 2.83/3.03  cnf(c1073,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X593)|iext(X593,uri_rdfs_Statement,uri_rdfs_Resource),inference(resolution,[status(thm)],[c984, c23])).
% 2.83/3.03  cnf(c1070,plain,~iext(uri_rdfs_subClassOf,X592,uri_rdfs_Statement)|iext(uri_rdfs_subClassOf,X592,uri_rdfs_Resource),inference(resolution,[status(thm)],[c984, c27])).
% 2.83/3.03  cnf(c983,plain,iext(uri_rdf_type,uri_rdfs_Statement,uri_rdfs_Class),inference(resolution,[status(thm)],[c980, c113])).
% 2.83/3.03  cnf(c1065,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X591)|iext(X591,uri_rdfs_Statement,uri_rdfs_Class),inference(resolution,[status(thm)],[c983, c23])).
% 2.83/3.03  cnf(c130,plain,~ip(X97)|iext(uri_rdf_type,X97,uri_rdf_Property),inference(split_conjunct,[status(thm)],[c128])).
% 2.83/3.03  cnf(c22,plain,~iext(uri_rdfs_subPropertyOf,X58,X59)|ip(X59),inference(split_conjunct,[status(thm)],[c20])).
% 2.83/3.03  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.83/3.03  fof(c96,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.83/3.03  fof(c97,plain,(![X34]:(~icext(uri_rdfs_ContainerMembershipProperty,X34)|iext(uri_rdfs_subPropertyOf,X34,uri_rdfs_member))),inference(variable_rename,[status(thm)],[c96])).
% 2.83/3.03  cnf(c98,plain,~icext(uri_rdfs_ContainerMembershipProperty,X88)|iext(uri_rdfs_subPropertyOf,X88,uri_rdfs_member),inference(split_conjunct,[status(thm)],[c97])).
% 2.83/3.03  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.83/3.03  cnf(c84,plain,iext(uri_rdf_type,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),inference(split_conjunct,[status(thm)],[rdfs_container_n_type_003])).
% 2.83/3.03  cnf(c112,plain,~iext(uri_rdf_type,X91,X90)|icext(X90,X91),inference(split_conjunct,[status(thm)],[c111])).
% 2.83/3.03  cnf(c372,plain,icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__3),inference(resolution,[status(thm)],[c112, c84])).
% 2.83/3.03  cnf(c377,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__3,uri_rdfs_member),inference(resolution,[status(thm)],[c372, c98])).
% 2.83/3.03  cnf(c753,plain,ip(uri_rdfs_member),inference(resolution,[status(thm)],[c377, c22])).
% 2.83/3.03  cnf(c757,plain,iext(uri_rdf_type,uri_rdfs_member,uri_rdf_Property),inference(resolution,[status(thm)],[c753, c130])).
% 2.83/3.03  cnf(c1055,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X590)|iext(X590,uri_rdfs_member,uri_rdf_Property),inference(resolution,[status(thm)],[c757, c23])).
% 2.83/3.03  cnf(c756,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_member,uri_rdfs_member),inference(resolution,[status(thm)],[c753, c15])).
% 2.83/3.03  cnf(c1050,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X589)|iext(X589,uri_rdfs_member,uri_rdfs_member),inference(resolution,[status(thm)],[c756, c23])).
% 2.83/3.03  cnf(c68,plain,~ic(X62)|icext(uri_rdfs_Class,X62),inference(split_conjunct,[status(thm)],[c67])).
% 2.83/3.03  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.83/3.03  fof(c32,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.83/3.03  fof(c34,plain,(![X16]:(![X17]:(![X18]:(~iext(uri_rdfs_subClassOf,X16,X17)|((ic(X16)&ic(X17))&(~icext(X16,X18)|icext(X17,X18))))))),inference(shift_quantors,[status(thm)],[fof(c33,plain,(![X16]:(![X17]:(~iext(uri_rdfs_subClassOf,X16,X17)|((ic(X16)&ic(X17))&(![X18]:(~icext(X16,X18)|icext(X17,X18))))))),inference(variable_rename,[status(thm)],[c32])).])).
% 2.83/3.03  fof(c35,plain,(![X16]:(![X17]:(![X18]:(((~iext(uri_rdfs_subClassOf,X16,X17)|ic(X16))&(~iext(uri_rdfs_subClassOf,X16,X17)|ic(X17)))&(~iext(uri_rdfs_subClassOf,X16,X17)|(~icext(X16,X18)|icext(X17,X18))))))),inference(distribute,[status(thm)],[c34])).
% 2.83/3.03  cnf(c37,plain,~iext(uri_rdfs_subClassOf,X75,X74)|ic(X74),inference(split_conjunct,[status(thm)],[c35])).
% 2.83/3.03  cnf(c36,plain,~iext(uri_rdfs_subClassOf,X73,X72)|ic(X73),inference(split_conjunct,[status(thm)],[c35])).
% 2.83/3.03  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.83/3.03  cnf(c100,plain,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Container),inference(split_conjunct,[status(thm)],[rdfs_container_alt_sub])).
% 2.83/3.03  cnf(c321,plain,ic(uri_rdf_Alt),inference(resolution,[status(thm)],[c100, c36])).
% 2.83/3.03  cnf(c345,plain,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Resource),inference(resolution,[status(thm)],[c107, c321])).
% 2.83/3.03  cnf(c649,plain,ic(uri_rdfs_Resource),inference(resolution,[status(thm)],[c345, c37])).
% 2.83/3.03  cnf(c657,plain,icext(uri_rdfs_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c649, c68])).
% 2.83/3.03  cnf(c659,plain,iext(uri_rdf_type,uri_rdfs_Resource,uri_rdfs_Class),inference(resolution,[status(thm)],[c657, c113])).
% 2.83/3.03  cnf(c1042,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X587)|iext(X587,uri_rdfs_Resource,uri_rdfs_Class),inference(resolution,[status(thm)],[c659, c23])).
% 2.83/3.03  cnf(c655,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Resource,uri_rdfs_Resource),inference(resolution,[status(thm)],[c649, c107])).
% 2.83/3.03  cnf(c1036,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X586)|iext(X586,uri_rdfs_Resource,uri_rdfs_Resource),inference(resolution,[status(thm)],[c655, c23])).
% 2.83/3.03  cnf(c2,plain,iext(uri_owl_equivalentClass,uri_owl_Thing,skolem0001),inference(split_conjunct,[status(thm)],[c1])).
% 2.83/3.03  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.83/3.03  fof(c145,plain,(![S]:(![P]:(![O]:(~iext(P,S,O)|ip(P))))),inference(fof_nnf,[status(thm)],[simple_iext_property])).
% 2.83/3.03  fof(c146,plain,(![S]:(![P]:((![O]:~iext(P,S,O))|ip(P)))),inference(shift_quantors,[status(thm)],[c145])).
% 2.83/3.03  fof(c148,plain,(![X44]:(![X45]:(![X46]:(~iext(X45,X44,X46)|ip(X45))))),inference(shift_quantors,[status(thm)],[fof(c147,plain,(![X44]:(![X45]:((![X46]:~iext(X45,X44,X46))|ip(X45)))),inference(variable_rename,[status(thm)],[c146])).])).
% 2.83/3.03  cnf(c149,plain,~iext(X100,X99,X98)|ip(X100),inference(split_conjunct,[status(thm)],[c148])).
% 2.83/3.03  cnf(c543,plain,ip(uri_owl_equivalentClass),inference(resolution,[status(thm)],[c149, c2])).
% 2.83/3.03  cnf(c566,plain,iext(uri_rdf_type,uri_owl_equivalentClass,uri_rdf_Property),inference(resolution,[status(thm)],[c543, c130])).
% 2.83/3.03  cnf(c1026,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X584)|iext(X584,uri_owl_equivalentClass,uri_rdf_Property),inference(resolution,[status(thm)],[c566, c23])).
% 2.83/3.03  cnf(c565,plain,iext(uri_rdfs_subPropertyOf,uri_owl_equivalentClass,uri_owl_equivalentClass),inference(resolution,[status(thm)],[c543, c15])).
% 2.83/3.03  cnf(c1021,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X583)|iext(X583,uri_owl_equivalentClass,uri_owl_equivalentClass),inference(resolution,[status(thm)],[c565, c23])).
% 2.83/3.03  cnf(c3,plain,iext(uri_owl_oneOf,skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c1])).
% 2.83/3.03  cnf(c523,plain,ip(uri_owl_oneOf),inference(resolution,[status(thm)],[c149, c3])).
% 2.83/3.03  cnf(c564,plain,iext(uri_rdf_type,uri_owl_oneOf,uri_rdf_Property),inference(resolution,[status(thm)],[c523, c130])).
% 2.83/3.03  cnf(c1011,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X581)|iext(X581,uri_owl_oneOf,uri_rdf_Property),inference(resolution,[status(thm)],[c564, c23])).
% 2.83/3.03  cnf(c563,plain,iext(uri_rdfs_subPropertyOf,uri_owl_oneOf,uri_owl_oneOf),inference(resolution,[status(thm)],[c523, c15])).
% 2.83/3.03  cnf(c1005,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X580)|iext(X580,uri_owl_oneOf,uri_owl_oneOf),inference(resolution,[status(thm)],[c563, c23])).
% 2.83/3.03  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.83/3.03  cnf(c118,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_sub])).
% 2.83/3.03  cnf(c500,plain,ip(uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c149, c118])).
% 2.83/3.03  cnf(c562,plain,iext(uri_rdf_type,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c500, c130])).
% 2.83/3.03  cnf(c996,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X578)|iext(X578,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c562, c23])).
% 2.83/3.03  cnf(c561,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c500, c15])).
% 2.83/3.03  cnf(c991,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X577)|iext(X577,uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c561, c23])).
% 2.83/3.03  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.83/3.03  cnf(c95,plain,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_container_containermembershipproperty_sub])).
% 2.83/3.03  cnf(c495,plain,ip(uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c149, c95])).
% 2.83/3.03  cnf(c560,plain,iext(uri_rdf_type,uri_rdfs_subClassOf,uri_rdf_Property),inference(resolution,[status(thm)],[c495, c130])).
% 2.83/3.03  cnf(c975,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X575)|iext(X575,uri_rdfs_subClassOf,uri_rdf_Property),inference(resolution,[status(thm)],[c560, c23])).
% 2.83/3.03  cnf(c559,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c495, c15])).
% 2.83/3.03  cnf(c967,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X574)|iext(X574,uri_rdfs_subClassOf,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c559, c23])).
% 2.83/3.03  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.83/3.03  cnf(c87,plain,iext(uri_rdfs_range,uri_rdf__3,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_range_003])).
% 2.83/3.03  cnf(c492,plain,ip(uri_rdfs_range),inference(resolution,[status(thm)],[c149, c87])).
% 2.83/3.03  cnf(c558,plain,iext(uri_rdf_type,uri_rdfs_range,uri_rdf_Property),inference(resolution,[status(thm)],[c492, c130])).
% 2.83/3.03  cnf(c957,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X572)|iext(X572,uri_rdfs_range,uri_rdf_Property),inference(resolution,[status(thm)],[c558, c23])).
% 2.83/3.03  cnf(c557,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_range,uri_rdfs_range),inference(resolution,[status(thm)],[c492, c15])).
% 2.83/3.03  cnf(c944,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X571)|iext(X571,uri_rdfs_range,uri_rdfs_range),inference(resolution,[status(thm)],[c557, c23])).
% 2.83/3.03  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.83/3.03  cnf(c117,plain,iext(uri_rdfs_domain,uri_rdfs_label,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_label_domain])).
% 2.83/3.03  cnf(c491,plain,ip(uri_rdfs_domain),inference(resolution,[status(thm)],[c149, c117])).
% 2.83/3.03  cnf(c556,plain,iext(uri_rdf_type,uri_rdfs_domain,uri_rdf_Property),inference(resolution,[status(thm)],[c491, c130])).
% 2.83/3.03  cnf(c929,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X569)|iext(X569,uri_rdfs_domain,uri_rdf_Property),inference(resolution,[status(thm)],[c556, c23])).
% 2.83/3.03  cnf(c555,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,uri_rdfs_domain),inference(resolution,[status(thm)],[c491, c15])).
% 2.83/3.03  cnf(c919,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X568)|iext(X568,uri_rdfs_domain,uri_rdfs_domain),inference(resolution,[status(thm)],[c555, c23])).
% 2.83/3.03  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.83/3.03  cnf(c139,plain,iext(uri_rdf_type,uri_rdf_first,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_collection_first_type])).
% 2.83/3.03  cnf(c484,plain,ip(uri_rdf_first),inference(resolution,[status(thm)],[c139, c129])).
% 2.83/3.03  cnf(c487,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_first,uri_rdf_first),inference(resolution,[status(thm)],[c484, c15])).
% 2.83/3.03  cnf(c905,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X566)|iext(X566,uri_rdf_first,uri_rdf_first),inference(resolution,[status(thm)],[c487, c23])).
% 2.83/3.03  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.83/3.03  cnf(c137,plain,iext(uri_rdf_type,uri_rdf_rest,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_collection_rest_type])).
% 2.83/3.03  cnf(c469,plain,ip(uri_rdf_rest),inference(resolution,[status(thm)],[c137, c129])).
% 2.83/3.03  cnf(c474,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_rest,uri_rdf_rest),inference(resolution,[status(thm)],[c469, c15])).
% 2.83/3.03  cnf(c895,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X564)|iext(X564,uri_rdf_rest,uri_rdf_rest),inference(resolution,[status(thm)],[c474, c23])).
% 2.83/3.03  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.83/3.03  cnf(c136,plain,iext(uri_rdf_type,uri_rdf__1,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_container_n_type_001])).
% 2.83/3.03  cnf(c464,plain,ip(uri_rdf__1),inference(resolution,[status(thm)],[c136, c129])).
% 2.83/3.03  cnf(c472,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__1,uri_rdf__1),inference(resolution,[status(thm)],[c464, c15])).
% 2.83/3.03  cnf(c887,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X562)|iext(X562,uri_rdf__1,uri_rdf__1),inference(resolution,[status(thm)],[c472, c23])).
% 2.83/3.03  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.83/3.03  cnf(c135,plain,iext(uri_rdf_type,uri_rdf__2,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_container_n_type_002])).
% 2.83/3.03  cnf(c453,plain,ip(uri_rdf__2),inference(resolution,[status(thm)],[c135, c129])).
% 2.83/3.03  cnf(c458,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__2,uri_rdf__2),inference(resolution,[status(thm)],[c453, c15])).
% 2.83/3.03  cnf(c878,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X560)|iext(X560,uri_rdf__2,uri_rdf__2),inference(resolution,[status(thm)],[c458, c23])).
% 2.83/3.03  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.83/3.03  cnf(c134,plain,iext(uri_rdf_type,uri_rdf__3,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_container_n_type_003])).
% 2.83/3.03  cnf(c448,plain,ip(uri_rdf__3),inference(resolution,[status(thm)],[c134, c129])).
% 2.83/3.03  cnf(c456,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__3,uri_rdf__3),inference(resolution,[status(thm)],[c448, c15])).
% 2.83/3.03  cnf(c870,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X558)|iext(X558,uri_rdf__3,uri_rdf__3),inference(resolution,[status(thm)],[c456, c23])).
% 2.83/3.03  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.83/3.03  cnf(c133,plain,iext(uri_rdf_type,uri_rdf_object,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_reification_object_type])).
% 2.83/3.03  cnf(c440,plain,ip(uri_rdf_object),inference(resolution,[status(thm)],[c133, c129])).
% 2.83/3.03  cnf(c443,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_object,uri_rdf_object),inference(resolution,[status(thm)],[c440, c15])).
% 2.83/3.03  cnf(c862,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X556)|iext(X556,uri_rdf_object,uri_rdf_object),inference(resolution,[status(thm)],[c443, c23])).
% 2.83/3.03  cnf(c367,plain,ip(uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c118, c22])).
% 2.83/3.03  cnf(c435,plain,iext(uri_rdf_type,uri_rdfs_seeAlso,uri_rdf_Property),inference(resolution,[status(thm)],[c130, c367])).
% 2.83/3.03  cnf(c852,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X554)|iext(X554,uri_rdfs_seeAlso,uri_rdf_Property),inference(resolution,[status(thm)],[c435, c23])).
% 2.83/3.03  cnf(c21,plain,~iext(uri_rdfs_subPropertyOf,X53,X54)|ip(X53),inference(split_conjunct,[status(thm)],[c20])).
% 2.83/3.03  cnf(c368,plain,ip(uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c118, c21])).
% 2.83/3.03  cnf(c433,plain,iext(uri_rdf_type,uri_rdfs_isDefinedBy,uri_rdf_Property),inference(resolution,[status(thm)],[c130, c368])).
% 2.83/3.03  cnf(c845,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X553)|iext(X553,uri_rdfs_isDefinedBy,uri_rdf_Property),inference(resolution,[status(thm)],[c433, c23])).
% 2.83/3.03  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.83/3.03  cnf(c132,plain,iext(uri_rdf_type,uri_rdf_value,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_reification_predicate_type])).
% 2.83/3.03  cnf(c428,plain,ip(uri_rdf_value),inference(resolution,[status(thm)],[c132, c129])).
% 2.83/3.03  cnf(c431,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_value,uri_rdf_value),inference(resolution,[status(thm)],[c428, c15])).
% 2.83/3.03  cnf(c839,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X552)|iext(X552,uri_rdf_value,uri_rdf_value),inference(resolution,[status(thm)],[c431, c23])).
% 2.83/3.03  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.83/3.03  cnf(c131,plain,iext(uri_rdf_type,uri_rdf_subject,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_reification_subject_type])).
% 2.83/3.03  cnf(c422,plain,ip(uri_rdf_subject),inference(resolution,[status(thm)],[c129, c131])).
% 2.83/3.03  cnf(c424,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_subject,uri_rdf_subject),inference(resolution,[status(thm)],[c422, c15])).
% 2.83/3.03  cnf(c832,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X550)|iext(X550,uri_rdf_subject,uri_rdf_subject),inference(resolution,[status(thm)],[c424, c23])).
% 2.83/3.03  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.83/3.03  cnf(c123,plain,iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_value_type])).
% 2.83/3.03  cnf(c421,plain,ip(uri_rdf_type),inference(resolution,[status(thm)],[c129, c123])).
% 2.83/3.03  cnf(c423,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_type,uri_rdf_type),inference(resolution,[status(thm)],[c421, c15])).
% 2.83/3.03  cnf(c824,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X548)|iext(X548,uri_rdf_type,uri_rdf_type),inference(resolution,[status(thm)],[c423, c23])).
% 2.83/3.03  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.83/3.03  cnf(c85,plain,iext(uri_rdf_type,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),inference(split_conjunct,[status(thm)],[rdfs_container_n_type_002])).
% 2.83/3.03  cnf(c375,plain,icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__2),inference(resolution,[status(thm)],[c112, c85])).
% 2.83/3.03  cnf(c394,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__2,uri_rdfs_member),inference(resolution,[status(thm)],[c375, c98])).
% 2.83/3.03  cnf(c813,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X546)|iext(X546,uri_rdf__2,uri_rdfs_member),inference(resolution,[status(thm)],[c394, c23])).
% 2.83/3.03  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.83/3.03  fof(c10,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.83/3.03  fof(c11,plain,(![X4]:(![X5]:(![X6]:((~iext(uri_rdfs_subPropertyOf,X4,X5)|~iext(uri_rdfs_subPropertyOf,X5,X6))|iext(uri_rdfs_subPropertyOf,X4,X6))))),inference(variable_rename,[status(thm)],[c10])).
% 2.83/3.03  cnf(c12,plain,~iext(uri_rdfs_subPropertyOf,X50,X51)|~iext(uri_rdfs_subPropertyOf,X51,X49)|iext(uri_rdfs_subPropertyOf,X50,X49),inference(split_conjunct,[status(thm)],[c11])).
% 2.83/3.03  cnf(c812,plain,~iext(uri_rdfs_subPropertyOf,X545,uri_rdf__2)|iext(uri_rdfs_subPropertyOf,X545,uri_rdfs_member),inference(resolution,[status(thm)],[c394, c12])).
% 2.83/3.03  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.83/3.03  cnf(c82,plain,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[rdfs_dat_xmlliteral_sub])).
% 2.83/3.03  cnf(c204,plain,ic(uri_rdfs_Literal),inference(resolution,[status(thm)],[c37, c82])).
% 2.83/3.03  cnf(c209,plain,icext(uri_rdfs_Class,uri_rdfs_Literal),inference(resolution,[status(thm)],[c204, c68])).
% 2.83/3.03  cnf(c393,plain,iext(uri_rdf_type,uri_rdfs_Literal,uri_rdfs_Class),inference(resolution,[status(thm)],[c113, c209])).
% 2.83/3.03  cnf(c806,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X544)|iext(X544,uri_rdfs_Literal,uri_rdfs_Class),inference(resolution,[status(thm)],[c393, c23])).
% 2.83/3.03  cnf(c328,plain,icext(uri_rdfs_Class,uri_rdf_Alt),inference(resolution,[status(thm)],[c321, c68])).
% 2.83/3.03  cnf(c392,plain,iext(uri_rdf_type,uri_rdf_Alt,uri_rdfs_Class),inference(resolution,[status(thm)],[c113, c328])).
% 2.83/3.03  cnf(c801,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X543)|iext(X543,uri_rdf_Alt,uri_rdfs_Class),inference(resolution,[status(thm)],[c392, c23])).
% 2.83/3.03  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.83/3.03  cnf(c83,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Container),inference(split_conjunct,[status(thm)],[rdfs_container_seq_sub])).
% 2.83/3.03  cnf(c195,plain,ic(uri_rdfs_Seq),inference(resolution,[status(thm)],[c36, c83])).
% 2.83/3.03  cnf(c201,plain,icext(uri_rdfs_Class,uri_rdfs_Seq),inference(resolution,[status(thm)],[c195, c68])).
% 2.83/3.03  cnf(c390,plain,iext(uri_rdf_type,uri_rdfs_Seq,uri_rdfs_Class),inference(resolution,[status(thm)],[c113, c201])).
% 2.83/3.03  cnf(c796,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X542)|iext(X542,uri_rdfs_Seq,uri_rdfs_Class),inference(resolution,[status(thm)],[c390, c23])).
% 2.83/3.03  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.83/3.03  cnf(c77,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_datatype_sub])).
% 2.83/3.03  cnf(c203,plain,ic(uri_rdfs_Class),inference(resolution,[status(thm)],[c37, c77])).
% 2.83/3.03  cnf(c207,plain,icext(uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c203, c68])).
% 2.83/3.03  cnf(c388,plain,iext(uri_rdf_type,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c113, c207])).
% 2.83/3.03  cnf(c791,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X541)|iext(X541,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c388, c23])).
% 2.83/3.03  cnf(c205,plain,ic(uri_rdfs_Container),inference(resolution,[status(thm)],[c37, c83])).
% 2.83/3.03  cnf(c211,plain,icext(uri_rdfs_Class,uri_rdfs_Container),inference(resolution,[status(thm)],[c205, c68])).
% 2.83/3.03  cnf(c386,plain,iext(uri_rdf_type,uri_rdfs_Container,uri_rdfs_Class),inference(resolution,[status(thm)],[c113, c211])).
% 2.83/3.03  cnf(c786,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X540)|iext(X540,uri_rdfs_Container,uri_rdfs_Class),inference(resolution,[status(thm)],[c386, c23])).
% 2.83/3.03  cnf(c260,plain,ic(uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c95, c36])).
% 2.83/3.03  cnf(c305,plain,icext(uri_rdfs_Class,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c260, c68])).
% 2.83/3.03  cnf(c383,plain,iext(uri_rdf_type,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Class),inference(resolution,[status(thm)],[c113, c305])).
% 2.83/3.03  cnf(c781,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X539)|iext(X539,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Class),inference(resolution,[status(thm)],[c383, c23])).
% 2.83/3.03  cnf(c193,plain,ic(uri_rdfs_Datatype),inference(resolution,[status(thm)],[c36, c77])).
% 2.83/3.03  cnf(c197,plain,icext(uri_rdfs_Class,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c193, c68])).
% 2.83/3.03  cnf(c382,plain,iext(uri_rdf_type,uri_rdfs_Datatype,uri_rdfs_Class),inference(resolution,[status(thm)],[c113, c197])).
% 2.83/3.03  cnf(c776,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X538)|iext(X538,uri_rdfs_Datatype,uri_rdfs_Class),inference(resolution,[status(thm)],[c382, c23])).
% 2.83/3.03  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.83/3.03  cnf(c99,plain,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Container),inference(split_conjunct,[status(thm)],[rdfs_container_bag_sub])).
% 2.83/3.03  cnf(c311,plain,ic(uri_rdf_Bag),inference(resolution,[status(thm)],[c99, c36])).
% 2.83/3.03  cnf(c318,plain,icext(uri_rdfs_Class,uri_rdf_Bag),inference(resolution,[status(thm)],[c311, c68])).
% 2.83/3.03  cnf(c381,plain,iext(uri_rdf_type,uri_rdf_Bag,uri_rdfs_Class),inference(resolution,[status(thm)],[c113, c318])).
% 2.83/3.03  cnf(c771,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X537)|iext(X537,uri_rdf_Bag,uri_rdfs_Class),inference(resolution,[status(thm)],[c381, c23])).
% 2.83/3.03  cnf(c194,plain,ic(uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c36, c82])).
% 2.83/3.03  cnf(c199,plain,icext(uri_rdfs_Class,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c194, c68])).
% 2.83/3.03  cnf(c380,plain,iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Class),inference(resolution,[status(thm)],[c113, c199])).
% 2.83/3.03  cnf(c766,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X536)|iext(X536,uri_rdf_XMLLiteral,uri_rdfs_Class),inference(resolution,[status(thm)],[c380, c23])).
% 2.83/3.03  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.83/3.03  cnf(c86,plain,iext(uri_rdf_type,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),inference(split_conjunct,[status(thm)],[rdfs_container_n_type_001])).
% 2.83/3.03  cnf(c374,plain,icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__1),inference(resolution,[status(thm)],[c112, c86])).
% 2.83/3.03  cnf(c379,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__1,uri_rdfs_member),inference(resolution,[status(thm)],[c374, c98])).
% 2.83/3.03  cnf(c761,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X535)|iext(X535,uri_rdf__1,uri_rdfs_member),inference(resolution,[status(thm)],[c379, c23])).
% 2.83/3.03  cnf(c760,plain,~iext(uri_rdfs_subPropertyOf,X534,uri_rdf__1)|iext(uri_rdfs_subPropertyOf,X534,uri_rdfs_member),inference(resolution,[status(thm)],[c379, c12])).
% 2.83/3.03  cnf(c751,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X533)|iext(X533,uri_rdf__3,uri_rdfs_member),inference(resolution,[status(thm)],[c377, c23])).
% 2.83/3.03  cnf(c1237,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X532)|icext(X532,uri_rdfs_comment),inference(resolution,[status(thm)],[c1230, c49])).
% 2.83/3.03  cnf(c750,plain,~iext(uri_rdfs_subPropertyOf,X531,uri_rdf__3)|iext(uri_rdfs_subPropertyOf,X531,uri_rdfs_member),inference(resolution,[status(thm)],[c377, c12])).
% 2.83/3.03  cnf(c1235,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X530)|icext(X530,uri_rdfs_comment),inference(resolution,[status(thm)],[c1230, c75])).
% 2.83/3.03  cnf(c376,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c368, c15])).
% 2.83/3.03  cnf(c743,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X527)|iext(X527,uri_rdfs_isDefinedBy,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c376, c23])).
% 2.83/3.03  cnf(c1207,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X526)|icext(X526,uri_rdfs_label),inference(resolution,[status(thm)],[c1201, c49])).
% 2.83/3.03  cnf(c1205,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X525)|icext(X525,uri_rdfs_label),inference(resolution,[status(thm)],[c1201, c75])).
% 2.83/3.03  cnf(c1176,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X521)|icext(X521,uri_rdf_List),inference(resolution,[status(thm)],[c1155, c49])).
% 2.83/3.03  cnf(c370,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_seeAlso,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c367, c15])).
% 2.83/3.03  cnf(c736,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X519)|iext(X519,uri_rdfs_seeAlso,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c370, c23])).
% 2.83/3.03  cnf(c1165,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X517)|icext(X517,uri_rdf_List),inference(resolution,[status(thm)],[c1154, c75])).
% 2.83/3.03  cnf(c1138,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X513)|icext(X513,uri_rdf_predicate),inference(resolution,[status(thm)],[c1131, c49])).
% 2.83/3.03  cnf(c1136,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X512)|icext(X512,uri_rdf_predicate),inference(resolution,[status(thm)],[c1131, c75])).
% 2.83/3.03  cnf(c354,plain,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Resource),inference(resolution,[status(thm)],[c107, c311])).
% 2.83/3.03  cnf(c728,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X511)|iext(X511,uri_rdf_Bag,uri_rdfs_Resource),inference(resolution,[status(thm)],[c354, c23])).
% 2.83/3.03  cnf(c725,plain,~iext(uri_rdfs_subClassOf,X506,uri_rdf_Bag)|iext(uri_rdfs_subClassOf,X506,uri_rdfs_Resource),inference(resolution,[status(thm)],[c354, c27])).
% 2.83/3.03  cnf(c1080,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X504)|icext(X504,uri_rdfs_Statement),inference(resolution,[status(thm)],[c985, c49])).
% 2.83/3.03  cnf(c353,plain,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Resource),inference(resolution,[status(thm)],[c107, c194])).
% 2.83/3.03  cnf(c720,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X503)|iext(X503,uri_rdf_XMLLiteral,uri_rdfs_Resource),inference(resolution,[status(thm)],[c353, c23])).
% 2.83/3.03  cnf(c1074,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X502)|icext(X502,uri_rdfs_Statement),inference(resolution,[status(thm)],[c984, c75])).
% 2.83/3.03  cnf(c717,plain,~iext(uri_rdfs_subClassOf,X498,uri_rdf_XMLLiteral)|iext(uri_rdfs_subClassOf,X498,uri_rdfs_Resource),inference(resolution,[status(thm)],[c353, c27])).
% 2.83/3.03  cnf(c1051,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X495)|icext(X495,uri_rdfs_member),inference(resolution,[status(thm)],[c756, c75])).
% 2.83/3.03  cnf(c352,plain,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Resource),inference(resolution,[status(thm)],[c107, c260])).
% 2.83/3.03  cnf(c712,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X494)|iext(X494,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Resource),inference(resolution,[status(thm)],[c352, c23])).
% 2.83/3.03  cnf(c709,plain,~iext(uri_rdfs_subClassOf,X490,uri_rdfs_ContainerMembershipProperty)|iext(uri_rdfs_subClassOf,X490,uri_rdfs_Resource),inference(resolution,[status(thm)],[c352, c27])).
% 2.83/3.03  cnf(c1037,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X489)|icext(X489,uri_rdfs_Resource),inference(resolution,[status(thm)],[c655, c75])).
% 2.83/3.03  cnf(c351,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Resource),inference(resolution,[status(thm)],[c107, c193])).
% 2.83/3.03  cnf(c704,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X485)|iext(X485,uri_rdfs_Datatype,uri_rdfs_Resource),inference(resolution,[status(thm)],[c351, c23])).
% 2.83/3.03  cnf(c1022,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X484)|icext(X484,uri_owl_equivalentClass),inference(resolution,[status(thm)],[c565, c75])).
% 2.83/3.03  cnf(c1018,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X483)|icext(X483,uri_owl_equivalentClass),inference(resolution,[status(thm)],[c565, c49])).
% 2.83/3.03  cnf(c701,plain,~iext(uri_rdfs_subClassOf,X482,uri_rdfs_Datatype)|iext(uri_rdfs_subClassOf,X482,uri_rdfs_Resource),inference(resolution,[status(thm)],[c351, c27])).
% 2.83/3.03  cnf(c1006,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X479)|icext(X479,uri_owl_oneOf),inference(resolution,[status(thm)],[c563, c75])).
% 2.83/3.03  cnf(c350,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Literal,uri_rdfs_Resource),inference(resolution,[status(thm)],[c107, c204])).
% 2.83/3.03  cnf(c696,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X478)|iext(X478,uri_rdfs_Literal,uri_rdfs_Resource),inference(resolution,[status(thm)],[c350, c23])).
% 2.83/3.03  cnf(c1002,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X477)|icext(X477,uri_owl_oneOf),inference(resolution,[status(thm)],[c563, c49])).
% 2.83/3.03  cnf(c693,plain,~iext(uri_rdfs_subClassOf,X475,uri_rdfs_Literal)|iext(uri_rdfs_subClassOf,X475,uri_rdfs_Resource),inference(resolution,[status(thm)],[c350, c27])).
% 2.83/3.03  cnf(c992,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X473)|icext(X473,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c561, c75])).
% 2.83/3.03  cnf(c264,plain,ic(uri_rdf_Property),inference(resolution,[status(thm)],[c95, c37])).
% 2.83/3.03  cnf(c349,plain,iext(uri_rdfs_subClassOf,uri_rdf_Property,uri_rdfs_Resource),inference(resolution,[status(thm)],[c107, c264])).
% 2.83/3.03  cnf(c688,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X472)|iext(X472,uri_rdf_Property,uri_rdfs_Resource),inference(resolution,[status(thm)],[c349, c23])).
% 2.83/3.03  cnf(c988,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X471)|icext(X471,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c561, c49])).
% 2.83/3.03  cnf(c685,plain,~iext(uri_rdfs_subClassOf,X468,uri_rdf_Property)|iext(uri_rdfs_subClassOf,X468,uri_rdfs_Resource),inference(resolution,[status(thm)],[c349, c27])).
% 2.83/3.03  cnf(c969,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X467)|icext(X467,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c559, c75])).
% 2.83/3.03  cnf(c964,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X466)|icext(X466,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c559, c49])).
% 2.83/3.03  cnf(c348,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Resource),inference(resolution,[status(thm)],[c107, c195])).
% 2.83/3.03  cnf(c680,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X465)|iext(X465,uri_rdfs_Seq,uri_rdfs_Resource),inference(resolution,[status(thm)],[c348, c23])).
% 2.83/3.03  cnf(c945,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X462)|icext(X462,uri_rdfs_range),inference(resolution,[status(thm)],[c557, c75])).
% 2.83/3.03  cnf(c677,plain,~iext(uri_rdfs_subClassOf,X461,uri_rdfs_Seq)|iext(uri_rdfs_subClassOf,X461,uri_rdfs_Resource),inference(resolution,[status(thm)],[c348, c27])).
% 2.83/3.03  cnf(c937,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X460)|icext(X460,uri_rdfs_range),inference(resolution,[status(thm)],[c557, c49])).
% 2.83/3.03  cnf(c347,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Container,uri_rdfs_Resource),inference(resolution,[status(thm)],[c107, c205])).
% 2.83/3.03  cnf(c672,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X457)|iext(X457,uri_rdfs_Container,uri_rdfs_Resource),inference(resolution,[status(thm)],[c347, c23])).
% 2.83/3.03  cnf(c669,plain,~iext(uri_rdfs_subClassOf,X456,uri_rdfs_Container)|iext(uri_rdfs_subClassOf,X456,uri_rdfs_Resource),inference(resolution,[status(thm)],[c347, c27])).
% 2.83/3.03  cnf(c920,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X455)|icext(X455,uri_rdfs_domain),inference(resolution,[status(thm)],[c555, c75])).
% 2.83/3.03  cnf(c912,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X454)|icext(X454,uri_rdfs_domain),inference(resolution,[status(thm)],[c555, c49])).
% 2.83/3.03  cnf(c346,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c107, c203])).
% 2.83/3.03  cnf(c664,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X453)|iext(X453,uri_rdfs_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c346, c23])).
% 2.83/3.03  cnf(c906,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X452)|icext(X452,uri_rdf_first),inference(resolution,[status(thm)],[c487, c75])).
% 2.83/3.03  cnf(c902,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X451)|icext(X451,uri_rdf_first),inference(resolution,[status(thm)],[c487, c49])).
% 2.83/3.03  cnf(c661,plain,~iext(uri_rdfs_subClassOf,X450,uri_rdfs_Class)|iext(uri_rdfs_subClassOf,X450,uri_rdfs_Resource),inference(resolution,[status(thm)],[c346, c27])).
% 2.83/3.03  cnf(c896,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X449)|icext(X449,uri_rdf_rest),inference(resolution,[status(thm)],[c474, c75])).
% 2.83/3.03  cnf(c892,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X448)|icext(X448,uri_rdf_rest),inference(resolution,[status(thm)],[c474, c49])).
% 2.83/3.03  cnf(c651,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X447)|iext(X447,uri_rdf_Alt,uri_rdfs_Resource),inference(resolution,[status(thm)],[c345, c23])).
% 2.83/3.03  cnf(c884,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X445)|icext(X445,uri_rdf__1),inference(resolution,[status(thm)],[c472, c49])).
% 2.83/3.03  cnf(c648,plain,~iext(uri_rdfs_subClassOf,X443,uri_rdf_Alt)|iext(uri_rdfs_subClassOf,X443,uri_rdfs_Resource),inference(resolution,[status(thm)],[c345, c27])).
% 2.83/3.03  cnf(c875,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X442)|icext(X442,uri_rdf__2),inference(resolution,[status(thm)],[c458, c49])).
% 2.83/3.03  cnf(c327,plain,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdf_Alt),inference(resolution,[status(thm)],[c321, c30])).
% 2.83/3.03  cnf(c643,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X440)|iext(X440,uri_rdf_Alt,uri_rdf_Alt),inference(resolution,[status(thm)],[c327, c23])).
% 2.83/3.03  cnf(c867,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X439)|icext(X439,uri_rdf__3),inference(resolution,[status(thm)],[c456, c49])).
% 2.83/3.03  cnf(c863,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X438)|icext(X438,uri_rdf_object),inference(resolution,[status(thm)],[c443, c75])).
% 2.83/3.03  cnf(c859,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X437)|icext(X437,uri_rdf_object),inference(resolution,[status(thm)],[c443, c49])).
% 2.83/3.03  cnf(c317,plain,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdf_Bag),inference(resolution,[status(thm)],[c311, c30])).
% 2.83/3.03  cnf(c635,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X431)|iext(X431,uri_rdf_Bag,uri_rdf_Bag),inference(resolution,[status(thm)],[c317, c23])).
% 2.83/3.03  cnf(c840,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X430)|icext(X430,uri_rdf_value),inference(resolution,[status(thm)],[c431, c75])).
% 2.83/3.03  cnf(c836,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X429)|icext(X429,uri_rdf_value),inference(resolution,[status(thm)],[c431, c49])).
% 2.83/3.03  cnf(c833,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X427)|icext(X427,uri_rdf_subject),inference(resolution,[status(thm)],[c424, c75])).
% 2.83/3.03  cnf(c829,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X426)|icext(X426,uri_rdf_subject),inference(resolution,[status(thm)],[c424, c49])).
% 2.83/3.03  cnf(c306,plain,iext(uri_rdfs_subClassOf,uri_rdf_Property,uri_rdf_Property),inference(resolution,[status(thm)],[c264, c30])).
% 2.83/3.03  cnf(c627,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X425)|iext(X425,uri_rdf_Property,uri_rdf_Property),inference(resolution,[status(thm)],[c306, c23])).
% 2.83/3.03  cnf(c825,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X424)|icext(X424,uri_rdf_type),inference(resolution,[status(thm)],[c423, c75])).
% 2.83/3.03  cnf(c817,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X423)|icext(X423,uri_rdf_type),inference(resolution,[status(thm)],[c423, c49])).
% 2.83/3.03  cnf(c814,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X422)|icext(X422,uri_rdf__2),inference(resolution,[status(thm)],[c394, c75])).
% 2.83/3.03  cnf(c304,plain,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c260, c30])).
% 2.83/3.03  cnf(c619,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X416)|iext(X416,uri_rdfs_ContainerMembershipProperty,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c304, c23])).
% 2.83/3.03  cnf(c210,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Container,uri_rdfs_Container),inference(resolution,[status(thm)],[c205, c30])).
% 2.83/3.03  cnf(c611,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X405)|iext(X405,uri_rdfs_Container,uri_rdfs_Container),inference(resolution,[status(thm)],[c210, c23])).
% 2.83/3.03  cnf(c762,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X397)|icext(X397,uri_rdf__1),inference(resolution,[status(thm)],[c379, c75])).
% 2.83/3.03  cnf(c208,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Literal,uri_rdfs_Literal),inference(resolution,[status(thm)],[c204, c30])).
% 2.83/3.03  cnf(c603,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X395)|iext(X395,uri_rdfs_Literal,uri_rdfs_Literal),inference(resolution,[status(thm)],[c208, c23])).
% 2.83/3.03  cnf(c752,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X394)|icext(X394,uri_rdf__3),inference(resolution,[status(thm)],[c377, c75])).
% 2.83/3.03  cnf(c748,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X393)|icext(X393,uri_rdfs_member),inference(resolution,[status(thm)],[c377, c49])).
% 2.83/3.03  cnf(c740,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X390)|icext(X390,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c376, c49])).
% 2.83/3.03  cnf(c737,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X389)|icext(X389,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c370, c75])).
% 2.83/3.03  cnf(c206,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c203, c30])).
% 2.83/3.03  cnf(c595,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X388)|iext(X388,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c206, c23])).
% 2.83/3.03  cnf(c200,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Seq),inference(resolution,[status(thm)],[c195, c30])).
% 2.83/3.03  cnf(c587,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X377)|iext(X377,uri_rdfs_Seq,uri_rdfs_Seq),inference(resolution,[status(thm)],[c200, c23])).
% 2.83/3.03  cnf(c198,plain,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c194, c30])).
% 2.83/3.03  cnf(c579,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X366)|iext(X366,uri_rdf_XMLLiteral,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c198, c23])).
% 2.83/3.03  cnf(c650,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X363)|icext(X363,uri_rdfs_Resource),inference(resolution,[status(thm)],[c345, c49])).
% 2.83/3.03  cnf(c642,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X360)|icext(X360,uri_rdf_Alt),inference(resolution,[status(thm)],[c327, c49])).
% 2.83/3.03  cnf(c196,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c193, c30])).
% 2.83/3.03  cnf(c571,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X358)|iext(X358,uri_rdfs_Datatype,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c196, c23])).
% 2.83/3.03  cnf(c634,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X357)|icext(X357,uri_rdf_Bag),inference(resolution,[status(thm)],[c317, c49])).
% 2.83/3.03  cnf(c628,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X356)|icext(X356,uri_rdf_Property),inference(resolution,[status(thm)],[c306, c75])).
% 2.83/3.03  cnf(c618,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X352)|icext(X352,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c304, c49])).
% 2.83/3.03  cnf(c612,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X351)|icext(X351,uri_rdfs_Container),inference(resolution,[status(thm)],[c210, c75])).
% 2.83/3.03  cnf(c483,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X350)|iext(X350,uri_rdf_first,uri_rdf_Property),inference(resolution,[status(thm)],[c139, c23])).
% 2.83/3.03  cnf(c604,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X348)|icext(X348,uri_rdfs_Literal),inference(resolution,[status(thm)],[c208, c75])).
% 2.83/3.03  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.83/3.03  cnf(c138,plain,iext(uri_rdf_type,uri_rdf_nil,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdf_collection_nil_type])).
% 2.83/3.03  cnf(c479,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X346)|iext(X346,uri_rdf_nil,uri_rdf_List),inference(resolution,[status(thm)],[c138, c23])).
% 2.83/3.03  cnf(c596,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X345)|icext(X345,uri_rdfs_Class),inference(resolution,[status(thm)],[c206, c75])).
% 2.83/3.03  cnf(c468,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X342)|iext(X342,uri_rdf_rest,uri_rdf_Property),inference(resolution,[status(thm)],[c137, c23])).
% 2.83/3.03  cnf(c586,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X341)|icext(X341,uri_rdfs_Seq),inference(resolution,[status(thm)],[c200, c49])).
% 2.83/3.03  cnf(c463,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X339)|iext(X339,uri_rdf__1,uri_rdf_Property),inference(resolution,[status(thm)],[c136, c23])).
% 2.83/3.03  cnf(c578,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X338)|icext(X338,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c198, c49])).
% 2.83/3.03  cnf(c570,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X336)|icext(X336,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c196, c49])).
% 2.83/3.03  cnf(c452,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X335)|iext(X335,uri_rdf__2,uri_rdf_Property),inference(resolution,[status(thm)],[c135, c23])).
% 2.83/3.03  cnf(c481,plain,~iext(uri_rdfs_range,uri_rdf_type,X332)|icext(X332,uri_rdf_List),inference(resolution,[status(thm)],[c138, c49])).
% 2.83/3.03  cnf(c447,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X331)|iext(X331,uri_rdf__3,uri_rdf_Property),inference(resolution,[status(thm)],[c134, c23])).
% 2.83/3.03  cnf(c439,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X326)|iext(X326,uri_rdf_object,uri_rdf_Property),inference(resolution,[status(thm)],[c133, c23])).
% 2.83/3.03  cnf(c427,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X321)|iext(X321,uri_rdf_value,uri_rdf_Property),inference(resolution,[status(thm)],[c132, c23])).
% 2.83/3.03  cnf(c418,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X316)|iext(X316,uri_rdf_subject,uri_rdf_Property),inference(resolution,[status(thm)],[c131, c23])).
% 2.83/3.03  cnf(c413,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X312)|iext(X312,uri_rdf_type,uri_rdf_Property),inference(resolution,[status(thm)],[c123, c23])).
% 2.83/3.03  cnf(c415,plain,~iext(uri_rdfs_range,uri_rdf_type,X311)|icext(X311,uri_rdf_Property),inference(resolution,[status(thm)],[c123, c49])).
% 2.83/3.03  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.83/3.03  cnf(c122,plain,iext(uri_rdfs_domain,uri_rdfs_comment,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_comment_domain])).
% 2.83/3.03  cnf(c409,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X308)|iext(X308,uri_rdfs_comment,uri_rdfs_Resource),inference(resolution,[status(thm)],[c122, c23])).
% 2.83/3.03  cnf(c410,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X307)|icext(X307,uri_rdfs_comment),inference(resolution,[status(thm)],[c122, c75])).
% 2.83/3.03  cnf(c406,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X305)|iext(X305,uri_rdfs_comment,uri_rdfs_Literal),inference(resolution,[status(thm)],[c121, c23])).
% 2.83/3.03  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.83/3.03  cnf(c120,plain,iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_domain])).
% 2.83/3.03  cnf(c403,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X304)|iext(X304,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(resolution,[status(thm)],[c120, c23])).
% 2.83/3.03  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.83/3.03  cnf(c119,plain,iext(uri_rdfs_range,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_range])).
% 2.83/3.03  cnf(c400,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X303)|iext(X303,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(resolution,[status(thm)],[c119, c23])).
% 2.83/3.03  cnf(c404,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X300)|icext(X300,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c120, c75])).
% 2.83/3.03  fof(simple_ir,axiom,(![X]:ir(X)),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', simple_ir)).
% 2.83/3.03  fof(c143,plain,(![X43]:ir(X43)),inference(variable_rename,[status(thm)],[simple_ir])).
% 2.83/3.03  cnf(c144,plain,ir(X47),inference(split_conjunct,[status(thm)],[c143])).
% 2.83/3.03  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.83/3.03  fof(c58,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.83/3.03  fof(c59,plain,((![X]:(~ir(X)|icext(uri_rdfs_Resource,X)))&(![X]:(~icext(uri_rdfs_Resource,X)|ir(X)))),inference(shift_quantors,[status(thm)],[c58])).
% 2.83/3.03  fof(c61,plain,(![X25]:(![X26]:((~ir(X25)|icext(uri_rdfs_Resource,X25))&(~icext(uri_rdfs_Resource,X26)|ir(X26))))),inference(shift_quantors,[status(thm)],[fof(c60,plain,((![X25]:(~ir(X25)|icext(uri_rdfs_Resource,X25)))&(![X26]:(~icext(uri_rdfs_Resource,X26)|ir(X26)))),inference(variable_rename,[status(thm)],[c59])).])).
% 2.83/3.03  cnf(c62,plain,~ir(X57)|icext(uri_rdfs_Resource,X57),inference(split_conjunct,[status(thm)],[c61])).
% 2.83/3.03  cnf(c151,plain,icext(uri_rdfs_Resource,X60),inference(resolution,[status(thm)],[c62, c144])).
% 2.83/3.03  cnf(c391,plain,iext(uri_rdf_type,X94,uri_rdfs_Resource),inference(resolution,[status(thm)],[c113, c151])).
% 2.83/3.03  cnf(c397,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X298)|iext(X298,X297,uri_rdfs_Resource),inference(resolution,[status(thm)],[c391, c23])).
% 2.83/3.03  cnf(c401,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X295)|icext(X295,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c119, c75])).
% 2.83/3.03  cnf(c365,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X294)|iext(X294,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c118, c23])).
% 2.83/3.03  cnf(c399,plain,~iext(uri_rdfs_range,uri_rdf_type,X293)|icext(X293,uri_rdfs_Resource),inference(resolution,[status(thm)],[c391, c49])).
% 2.83/3.03  cnf(c369,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X292)|icext(X292,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c118, c49])).
% 2.83/3.03  cnf(c364,plain,~iext(uri_rdfs_subPropertyOf,X291,uri_rdfs_isDefinedBy)|iext(uri_rdfs_subPropertyOf,X291,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c118, c12])).
% 2.83/3.03  cnf(c366,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X290)|icext(X290,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c118, c75])).
% 2.83/3.03  cnf(c362,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X288)|icext(X288,uri_rdfs_label),inference(resolution,[status(thm)],[c117, c75])).
% 2.83/3.03  cnf(c361,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X287)|iext(X287,uri_rdfs_label,uri_rdfs_Resource),inference(resolution,[status(thm)],[c117, c23])).
% 2.83/3.03  cnf(c360,plain,~iext(uri_rdfs_range,uri_rdfs_range,X286)|icext(X286,uri_rdfs_Literal),inference(resolution,[status(thm)],[c116, c49])).
% 2.83/3.03  cnf(c358,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X285)|iext(X285,uri_rdfs_label,uri_rdfs_Literal),inference(resolution,[status(thm)],[c116, c23])).
% 2.83/3.03  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.83/3.03  cnf(c115,plain,iext(uri_rdfs_domain,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_seealso_domain])).
% 2.83/3.03  cnf(c355,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X282)|iext(X282,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(resolution,[status(thm)],[c115, c23])).
% 2.83/3.03  cnf(c356,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X281)|icext(X281,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c115, c75])).
% 2.83/3.03  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.83/3.03  cnf(c114,plain,iext(uri_rdfs_range,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_seealso_range])).
% 2.83/3.03  cnf(c342,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X279)|iext(X279,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(resolution,[status(thm)],[c114, c23])).
% 2.83/3.03  cnf(c343,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X278)|icext(X278,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c114, c75])).
% 2.83/3.03  cnf(c340,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X276)|icext(X276,uri_rdf_first),inference(resolution,[status(thm)],[c104, c75])).
% 2.83/3.03  cnf(c339,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X275)|iext(X275,uri_rdf_first,uri_rdf_List),inference(resolution,[status(thm)],[c104, c23])).
% 2.83/3.03  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.83/3.03  cnf(c103,plain,iext(uri_rdfs_range,uri_rdf_first,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_collection_first_range])).
% 2.83/3.03  cnf(c337,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X273)|icext(X273,uri_rdf_first),inference(resolution,[status(thm)],[c103, c75])).
% 2.83/3.03  cnf(c336,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X272)|iext(X272,uri_rdf_first,uri_rdfs_Resource),inference(resolution,[status(thm)],[c103, c23])).
% 2.83/3.03  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.83/3.03  cnf(c102,plain,iext(uri_rdfs_domain,uri_rdf_rest,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdfs_collection_rest_domain])).
% 2.83/3.03  cnf(c335,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X271)|icext(X271,uri_rdf_List),inference(resolution,[status(thm)],[c102, c49])).
% 2.83/3.03  cnf(c334,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X270)|icext(X270,uri_rdf_rest),inference(resolution,[status(thm)],[c102, c75])).
% 2.83/3.03  cnf(c333,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X268)|iext(X268,uri_rdf_rest,uri_rdf_List),inference(resolution,[status(thm)],[c102, c23])).
% 2.83/3.03  cnf(c330,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X266)|iext(X266,uri_rdf_rest,uri_rdf_List),inference(resolution,[status(thm)],[c101, c23])).
% 2.83/3.03  cnf(c323,plain,~iext(uri_rdfs_subClassOf,X265,uri_rdf_Alt)|iext(uri_rdfs_subClassOf,X265,uri_rdfs_Container),inference(resolution,[status(thm)],[c100, c27])).
% 2.83/3.03  cnf(c320,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X264)|iext(X264,uri_rdf_Alt,uri_rdfs_Container),inference(resolution,[status(thm)],[c100, c23])).
% 2.83/3.03  cnf(c313,plain,~iext(uri_rdfs_subClassOf,X262,uri_rdf_Bag)|iext(uri_rdfs_subClassOf,X262,uri_rdfs_Container),inference(resolution,[status(thm)],[c99, c27])).
% 2.83/3.03  cnf(c331,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X261)|icext(X261,uri_rdf_rest),inference(resolution,[status(thm)],[c101, c75])).
% 2.83/3.03  cnf(c310,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X259)|iext(X259,uri_rdf_Bag,uri_rdfs_Container),inference(resolution,[status(thm)],[c99, c23])).
% 2.83/3.03  cnf(c322,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X258)|icext(X258,uri_rdf_Alt),inference(resolution,[status(thm)],[c100, c75])).
% 2.83/3.03  cnf(c312,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X256)|icext(X256,uri_rdf_Bag),inference(resolution,[status(thm)],[c99, c75])).
% 2.83/3.03  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.83/3.03  cnf(c89,plain,iext(uri_rdfs_range,uri_rdf__1,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_range_001])).
% 2.83/3.03  cnf(c303,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X255)|icext(X255,uri_rdf__1),inference(resolution,[status(thm)],[c75, c89])).
% 2.83/3.03  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.83/3.03  cnf(c42,plain,iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_reification_predicate_range])).
% 2.83/3.03  cnf(c302,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X254)|icext(X254,uri_rdf_predicate),inference(resolution,[status(thm)],[c75, c42])).
% 2.83/3.03  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.83/3.03  cnf(c90,plain,iext(uri_rdfs_domain,uri_rdf__3,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_003])).
% 2.83/3.03  cnf(c301,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X253)|icext(X253,uri_rdf__3),inference(resolution,[status(thm)],[c75, c90])).
% 2.83/3.03  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.83/3.03  cnf(c7,plain,iext(uri_rdfs_domain,uri_rdf_value,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_value_domain])).
% 2.83/3.03  cnf(c299,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X251)|icext(X251,uri_rdf_value),inference(resolution,[status(thm)],[c75, c7])).
% 2.83/3.03  cnf(c298,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X250)|icext(X250,uri_rdfs_range),inference(resolution,[status(thm)],[c75, c46])).
% 2.83/3.03  cnf(c297,plain,~iext(uri_rdfs_domain,uri_owl_equivalentClass,X249)|icext(X249,uri_owl_Thing),inference(resolution,[status(thm)],[c75, c2])).
% 2.83/3.03  cnf(c5,plain,iext(uri_rdf_rest,skolem0002,uri_rdf_nil),inference(split_conjunct,[status(thm)],[c1])).
% 2.83/3.03  cnf(c296,plain,~iext(uri_rdfs_domain,uri_rdf_rest,X248)|icext(X248,skolem0002),inference(resolution,[status(thm)],[c75, c5])).
% 2.83/3.03  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.83/3.03  cnf(c94,plain,iext(uri_rdfs_domain,uri_rdfs_member,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_member_domain])).
% 2.83/3.03  cnf(c294,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X246)|icext(X246,uri_rdfs_member),inference(resolution,[status(thm)],[c75, c94])).
% 2.83/3.03  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.83/3.03  cnf(c16,plain,iext(uri_rdfs_range,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_subpropertyof_range])).
% 2.83/3.03  cnf(c293,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X245)|icext(X245,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c75, c16])).
% 2.83/3.03  cnf(c292,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X244)|icext(X244,uri_rdfs_Seq),inference(resolution,[status(thm)],[c75, c83])).
% 2.83/3.03  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.83/3.03  cnf(c6,plain,iext(uri_rdfs_range,uri_rdf_value,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_value_range])).
% 2.83/3.03  cnf(c291,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X243)|icext(X243,uri_rdf_value),inference(resolution,[status(thm)],[c75, c6])).
% 2.83/3.03  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.83/3.03  cnf(c9,plain,iext(uri_rdfs_domain,uri_rdf_type,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_type_domain])).
% 2.83/3.03  cnf(c289,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X241)|icext(X241,uri_rdf_type),inference(resolution,[status(thm)],[c75, c9])).
% 2.83/3.03  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.83/3.03  cnf(c8,plain,iext(uri_rdfs_range,uri_rdf_type,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_type_range])).
% 2.83/3.03  cnf(c288,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X240)|icext(X240,uri_rdf_type),inference(resolution,[status(thm)],[c75, c8])).
% 2.83/3.03  cnf(c286,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X238)|icext(X238,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c75, c82])).
% 2.83/3.03  cnf(c284,plain,~iext(uri_rdfs_domain,uri_owl_oneOf,X236)|icext(X236,skolem0001),inference(resolution,[status(thm)],[c75, c3])).
% 2.83/3.03  cnf(c283,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X235)|icext(X235,uri_rdfs_domain),inference(resolution,[status(thm)],[c75, c70])).
% 2.83/3.03  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.83/3.03  cnf(c41,plain,iext(uri_rdfs_domain,uri_rdf_subject,uri_rdfs_Statement),inference(split_conjunct,[status(thm)],[rdfs_reification_subject_domain])).
% 2.83/3.03  cnf(c282,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X234)|icext(X234,uri_rdf_subject),inference(resolution,[status(thm)],[c75, c41])).
% 2.83/3.03  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.83/3.03  cnf(c93,plain,iext(uri_rdfs_range,uri_rdfs_member,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_member_range])).
% 2.83/3.03  cnf(c281,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X233)|icext(X233,uri_rdfs_member),inference(resolution,[status(thm)],[c75, c93])).
% 2.83/3.03  cnf(c280,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X232)|icext(X232,uri_rdf_object),inference(resolution,[status(thm)],[c75, c45])).
% 2.83/3.03  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.83/3.03  cnf(c40,plain,iext(uri_rdfs_range,uri_rdf_subject,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_reification_subject_range])).
% 2.83/3.03  cnf(c278,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X230)|icext(X230,uri_rdf_subject),inference(resolution,[status(thm)],[c75, c40])).
% 2.83/3.03  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.83/3.03  cnf(c39,plain,iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_subclassof_domain])).
% 2.83/3.03  cnf(c276,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X228)|icext(X228,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c75, c39])).
% 2.83/3.03  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.83/3.03  cnf(c88,plain,iext(uri_rdfs_range,uri_rdf__2,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_range_002])).
% 2.83/3.03  cnf(c275,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X227)|icext(X227,uri_rdf__2),inference(resolution,[status(thm)],[c75, c88])).
% 2.83/3.03  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.83/3.03  cnf(c24,plain,iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_subpropertyof_domain])).
% 2.83/3.03  cnf(c274,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X226)|icext(X226,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c75, c24])).
% 2.83/3.03  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.83/3.03  cnf(c91,plain,iext(uri_rdfs_domain,uri_rdf__2,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_002])).
% 2.83/3.03  cnf(c273,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X225)|icext(X225,uri_rdf__2),inference(resolution,[status(thm)],[c75, c91])).
% 2.83/3.03  cnf(c271,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X223)|icext(X223,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c75, c77])).
% 2.83/3.03  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.83/3.03  cnf(c31,plain,iext(uri_rdfs_range,uri_rdfs_subClassOf,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_subclassof_range])).
% 2.83/3.03  cnf(c270,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X222)|icext(X222,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c75, c31])).
% 2.83/3.03  cnf(c269,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X221)|icext(X221,uri_rdfs_range),inference(resolution,[status(thm)],[c75, c50])).
% 2.83/3.03  cnf(c268,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X220)|icext(X220,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c75, c95])).
% 2.83/3.03  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.83/3.03  cnf(c92,plain,iext(uri_rdfs_domain,uri_rdf__1,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_001])).
% 2.83/3.03  cnf(c267,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X219)|icext(X219,uri_rdf__1),inference(resolution,[status(thm)],[c75, c92])).
% 2.83/3.03  cnf(c266,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X218)|icext(X218,uri_rdf__3),inference(resolution,[status(thm)],[c75, c87])).
% 2.83/3.03  cnf(c398,plain,~iext(uri_rdfs_domain,uri_rdf_type,X215)|icext(X215,X216),inference(resolution,[status(thm)],[c391, c75])).
% 2.83/3.03  cnf(c265,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X212)|icext(X212,uri_rdfs_domain),inference(factor,[status(thm)],[c75])).
% 2.83/3.03  cnf(c263,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X207)|icext(X207,uri_rdf_Property),inference(resolution,[status(thm)],[c95, c49])).
% 2.83/3.03  cnf(c261,plain,~iext(uri_rdfs_subClassOf,X202,uri_rdfs_ContainerMembershipProperty)|iext(uri_rdfs_subClassOf,X202,uri_rdf_Property),inference(resolution,[status(thm)],[c95, c27])).
% 2.83/3.03  cnf(c259,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X197)|iext(X197,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),inference(resolution,[status(thm)],[c95, c23])).
% 2.83/3.03  cnf(c257,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X186)|iext(X186,uri_rdfs_member,uri_rdfs_Resource),inference(resolution,[status(thm)],[c94, c23])).
% 2.83/3.04  cnf(c38,plain,~iext(uri_rdfs_subClassOf,X78,X77)|~icext(X78,X76)|icext(X77,X76),inference(split_conjunct,[status(thm)],[c35])).
% 2.83/3.04  cnf(c324,plain,~icext(uri_rdf_Alt,X185)|icext(uri_rdfs_Container,X185),inference(resolution,[status(thm)],[c100, c38])).
% 2.83/3.04  cnf(c314,plain,~icext(uri_rdf_Bag,X184)|icext(uri_rdfs_Container,X184),inference(resolution,[status(thm)],[c99, c38])).
% 2.83/3.04  cnf(c262,plain,~icext(uri_rdfs_ContainerMembershipProperty,X182)|icext(uri_rdf_Property,X182),inference(resolution,[status(thm)],[c95, c38])).
% 2.83/3.04  cnf(c249,plain,~iext(uri_rdfs_range,uri_owl_equivalentClass,X176)|icext(X176,skolem0001),inference(resolution,[status(thm)],[c49, c2])).
% 2.83/3.04  cnf(c248,plain,~iext(uri_rdfs_range,uri_rdf_rest,X175)|icext(X175,uri_rdf_nil),inference(resolution,[status(thm)],[c49, c5])).
% 2.83/3.04  cnf(c246,plain,~iext(uri_rdfs_range,uri_rdfs_range,X173)|icext(X173,uri_rdf_Property),inference(resolution,[status(thm)],[c49, c16])).
% 2.83/3.04  cnf(c245,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X172)|icext(X172,uri_rdfs_Container),inference(resolution,[status(thm)],[c49, c83])).
% 2.83/3.04  cnf(c1057,plain,icext(uri_rdf_Property,uri_rdfs_member),inference(resolution,[status(thm)],[c757, c112])).
% 2.83/3.04  cnf(c240,plain,~iext(uri_rdfs_range,uri_rdf_first,X167)|icext(X167,uri_ex_w),inference(resolution,[status(thm)],[c49, c4])).
% 2.83/3.04  cnf(c239,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X166)|icext(X166,uri_rdfs_Literal),inference(resolution,[status(thm)],[c49, c82])).
% 2.83/3.04  cnf(c1028,plain,icext(uri_rdf_Property,uri_owl_equivalentClass),inference(resolution,[status(thm)],[c566, c112])).
% 2.83/3.04  cnf(c237,plain,~iext(uri_rdfs_range,uri_owl_oneOf,X164)|icext(X164,skolem0002),inference(resolution,[status(thm)],[c49, c3])).
% 2.83/3.04  cnf(c1013,plain,icext(uri_rdf_Property,uri_owl_oneOf),inference(resolution,[status(thm)],[c564, c112])).
% 2.83/3.04  cnf(c998,plain,icext(uri_rdf_Property,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c562, c112])).
% 2.83/3.04  cnf(c977,plain,icext(uri_rdf_Property,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c560, c112])).
% 2.83/3.04  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.83/3.04  cnf(c81,plain,iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Datatype),inference(split_conjunct,[status(thm)],[rdfs_dat_xmlliteral_type])).
% 2.83/3.04  cnf(c232,plain,~iext(uri_rdfs_range,uri_rdf_type,X159)|icext(X159,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c49, c81])).
% 2.83/3.04  cnf(c959,plain,icext(uri_rdf_Property,uri_rdfs_range),inference(resolution,[status(thm)],[c558, c112])).
% 2.83/3.04  cnf(c230,plain,~iext(uri_rdfs_range,uri_rdf_type,X157)|icext(X157,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c49, c84])).
% 2.83/3.04  cnf(c931,plain,icext(uri_rdf_Property,uri_rdfs_domain),inference(resolution,[status(thm)],[c556, c112])).
% 2.83/3.04  cnf(c229,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X156)|icext(X156,uri_rdfs_Class),inference(resolution,[status(thm)],[c49, c39])).
% 2.83/3.04  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.83/3.04  cnf(c51,plain,iext(uri_rdf_type,uri_rdf_Property,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_property_type])).
% 2.83/3.04  cnf(c225,plain,~iext(uri_rdfs_range,uri_rdf_type,X152)|icext(X152,uri_rdfs_Class),inference(resolution,[status(thm)],[c49, c51])).
% 2.83/3.04  cnf(c224,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X151)|icext(X151,uri_rdfs_Class),inference(resolution,[status(thm)],[c49, c77])).
% 2.83/3.04  cnf(c223,plain,~iext(uri_rdfs_range,uri_rdfs_range,X150)|icext(X150,uri_rdfs_Class),inference(resolution,[status(thm)],[c49, c31])).
% 2.83/3.04  cnf(c222,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X149)|icext(X149,uri_rdf_Property),inference(resolution,[status(thm)],[c49, c50])).
% 2.83/3.04  cnf(c221,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X148)|icext(X148,uri_rdfs_Resource),inference(resolution,[status(thm)],[c49, c92])).
% 2.83/3.04  cnf(c220,plain,~iext(uri_rdfs_range,uri_rdfs_range,X147)|icext(X147,uri_rdfs_Resource),inference(resolution,[status(thm)],[c49, c87])).
% 2.83/3.04  cnf(c219,plain,~iext(uri_rdfs_range,uri_rdfs_range,X146)|icext(X146,X146),inference(factor,[status(thm)],[c49])).
% 2.83/3.04  cnf(c854,plain,icext(uri_rdf_Property,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c435, c112])).
% 2.83/3.04  cnf(c215,plain,~icext(uri_rdfs_Seq,X145)|icext(uri_rdfs_Container,X145),inference(resolution,[status(thm)],[c38, c83])).
% 2.83/3.04  cnf(c847,plain,icext(uri_rdf_Property,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c433, c112])).
% 2.83/3.04  cnf(c214,plain,~icext(uri_rdf_XMLLiteral,X144)|icext(uri_rdfs_Literal,X144),inference(resolution,[status(thm)],[c38, c82])).
% 2.83/3.04  cnf(c213,plain,~icext(uri_rdfs_Datatype,X143)|icext(uri_rdfs_Class,X143),inference(resolution,[status(thm)],[c38, c77])).
% 2.83/3.04  cnf(c192,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X142)|iext(X142,uri_rdfs_member,uri_rdfs_Resource),inference(resolution,[status(thm)],[c93, c23])).
% 2.83/3.04  cnf(c191,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X141)|iext(X141,uri_rdf__1,uri_rdfs_Resource),inference(resolution,[status(thm)],[c92, c23])).
% 2.83/3.04  cnf(c190,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X140)|iext(X140,uri_rdf__2,uri_rdfs_Resource),inference(resolution,[status(thm)],[c91, c23])).
% 2.83/3.04  cnf(c189,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X139)|iext(X139,uri_rdf__3,uri_rdfs_Resource),inference(resolution,[status(thm)],[c90, c23])).
% 2.83/3.04  cnf(c188,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X138)|iext(X138,uri_rdf__1,uri_rdfs_Resource),inference(resolution,[status(thm)],[c89, c23])).
% 2.83/3.04  cnf(c187,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X137)|iext(X137,uri_rdf__2,uri_rdfs_Resource),inference(resolution,[status(thm)],[c88, c23])).
% 2.83/3.04  cnf(c186,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X136)|iext(X136,uri_rdf__3,uri_rdfs_Resource),inference(resolution,[status(thm)],[c87, c23])).
% 2.83/3.04  cnf(c185,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X135)|iext(X135,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c86, c23])).
% 2.83/3.04  cnf(c184,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X134)|iext(X134,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c85, c23])).
% 2.83/3.04  cnf(c183,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X133)|iext(X133,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c84, c23])).
% 2.83/3.04  cnf(c182,plain,~iext(uri_rdfs_subClassOf,X132,uri_rdfs_Seq)|iext(uri_rdfs_subClassOf,X132,uri_rdfs_Container),inference(resolution,[status(thm)],[c27, c83])).
% 2.83/3.04  cnf(c181,plain,~iext(uri_rdfs_subClassOf,X131,uri_rdf_XMLLiteral)|iext(uri_rdfs_subClassOf,X131,uri_rdfs_Literal),inference(resolution,[status(thm)],[c27, c82])).
% 2.83/3.04  cnf(c180,plain,~iext(uri_rdfs_subClassOf,X130,uri_rdfs_Datatype)|iext(uri_rdfs_subClassOf,X130,uri_rdfs_Class),inference(resolution,[status(thm)],[c27, c77])).
% 2.83/3.04  cnf(c178,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X128)|iext(X128,uri_rdfs_Seq,uri_rdfs_Container),inference(resolution,[status(thm)],[c83, c23])).
% 2.83/3.04  cnf(c177,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X127)|iext(X127,uri_rdf_XMLLiteral,uri_rdfs_Literal),inference(resolution,[status(thm)],[c82, c23])).
% 2.83/3.04  cnf(c176,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X126)|iext(X126,uri_rdf_XMLLiteral,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c81, c23])).
% 2.83/3.04  cnf(c175,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X125)|iext(X125,uri_rdfs_Datatype,uri_rdfs_Class),inference(resolution,[status(thm)],[c77, c23])).
% 2.83/3.04  cnf(c174,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X124)|iext(X124,uri_rdfs_domain,uri_rdf_Property),inference(resolution,[status(thm)],[c76, c23])).
% 2.83/3.04  cnf(c173,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X123)|iext(X123,uri_rdf_predicate,uri_rdfs_Resource),inference(resolution,[status(thm)],[c23, c42])).
% 2.83/3.04  cnf(c172,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X122)|iext(X122,uri_rdf_value,uri_rdfs_Resource),inference(resolution,[status(thm)],[c23, c7])).
% 2.83/3.04  cnf(c171,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X121)|iext(X121,uri_rdfs_range,uri_rdfs_Class),inference(resolution,[status(thm)],[c23, c46])).
% 2.83/3.04  cnf(c170,plain,~iext(uri_rdfs_subPropertyOf,uri_owl_equivalentClass,X120)|iext(X120,uri_owl_Thing,skolem0001),inference(resolution,[status(thm)],[c23, c2])).
% 2.83/3.04  cnf(c169,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X119)|iext(X119,skolem0002,uri_rdf_nil),inference(resolution,[status(thm)],[c23, c5])).
% 2.83/3.04  cnf(c168,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X118)|iext(X118,uri_rdf_predicate,uri_rdfs_Statement),inference(resolution,[status(thm)],[c23, c43])).
% 2.83/3.04  cnf(c167,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X117)|iext(X117,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c23, c16])).
% 2.83/3.04  cnf(c166,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X116)|iext(X116,uri_rdf_value,uri_rdfs_Resource),inference(resolution,[status(thm)],[c23, c6])).
% 2.83/3.04  cnf(c165,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X115)|iext(X115,uri_rdf_type,uri_rdfs_Resource),inference(resolution,[status(thm)],[c23, c9])).
% 2.83/3.04  cnf(c164,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X114)|iext(X114,uri_rdf_type,uri_rdfs_Class),inference(resolution,[status(thm)],[c23, c8])).
% 2.83/3.04  cnf(c163,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_first,X113)|iext(X113,skolem0002,uri_ex_w),inference(resolution,[status(thm)],[c23, c4])).
% 2.83/3.04  cnf(c162,plain,~iext(uri_rdfs_subPropertyOf,uri_owl_oneOf,X112)|iext(X112,skolem0001,skolem0002),inference(resolution,[status(thm)],[c23, c3])).
% 2.83/3.04  cnf(c161,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X111)|iext(X111,uri_rdfs_domain,uri_rdfs_Class),inference(resolution,[status(thm)],[c23, c70])).
% 2.83/3.04  cnf(c160,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X110)|iext(X110,uri_rdf_subject,uri_rdfs_Statement),inference(resolution,[status(thm)],[c23, c41])).
% 2.83/3.04  cnf(c159,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X109)|iext(X109,uri_rdf_object,uri_rdfs_Statement),inference(resolution,[status(thm)],[c23, c45])).
% 2.83/3.04  cnf(c158,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X108)|iext(X108,uri_rdf_subject,uri_rdfs_Resource),inference(resolution,[status(thm)],[c23, c40])).
% 2.83/3.04  cnf(c157,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X107)|iext(X107,uri_rdfs_subClassOf,uri_rdfs_Class),inference(resolution,[status(thm)],[c23, c39])).
% 2.83/3.04  cnf(c156,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X106)|iext(X106,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c23, c24])).
% 2.83/3.04  cnf(c155,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X105)|iext(X105,uri_rdf_Property,uri_rdfs_Class),inference(resolution,[status(thm)],[c23, c51])).
% 2.83/3.04  cnf(c154,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X104)|iext(X104,uri_rdfs_subClassOf,uri_rdfs_Class),inference(resolution,[status(thm)],[c23, c31])).
% 2.83/3.04  cnf(c153,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X103)|iext(X103,uri_rdfs_range,uri_rdf_Property),inference(resolution,[status(thm)],[c23, c50])).
% 2.83/3.04  cnf(c152,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X102)|iext(X102,uri_rdfs_subPropertyOf,X102),inference(factor,[status(thm)],[c23])).
% 2.83/3.04  cnf(c482,plain,icext(uri_rdf_Property,uri_rdf_first),inference(resolution,[status(thm)],[c139, c112])).
% 2.83/3.04  cnf(c478,plain,icext(uri_rdf_List,uri_rdf_nil),inference(resolution,[status(thm)],[c138, c112])).
% 2.83/3.04  cnf(c467,plain,icext(uri_rdf_Property,uri_rdf_rest),inference(resolution,[status(thm)],[c137, c112])).
% 2.83/3.04  cnf(c462,plain,icext(uri_rdf_Property,uri_rdf__1),inference(resolution,[status(thm)],[c136, c112])).
% 2.83/3.04  cnf(c451,plain,icext(uri_rdf_Property,uri_rdf__2),inference(resolution,[status(thm)],[c135, c112])).
% 2.83/3.04  cnf(c446,plain,icext(uri_rdf_Property,uri_rdf__3),inference(resolution,[status(thm)],[c134, c112])).
% 2.83/3.04  cnf(c438,plain,icext(uri_rdf_Property,uri_rdf_object),inference(resolution,[status(thm)],[c133, c112])).
% 2.83/3.04  cnf(c426,plain,icext(uri_rdf_Property,uri_rdf_value),inference(resolution,[status(thm)],[c132, c112])).
% 2.83/3.04  cnf(c417,plain,icext(uri_rdf_Property,uri_rdf_subject),inference(resolution,[status(thm)],[c131, c112])).
% 2.83/3.04  cnf(c412,plain,icext(uri_rdf_Property,uri_rdf_type),inference(resolution,[status(thm)],[c123, c112])).
% 2.83/3.04  cnf(c373,plain,icext(uri_rdfs_Datatype,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c112, c81])).
% 2.83/3.04  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.83/3.04  fof(c78,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.83/3.04  fof(c79,plain,(![X33]:(~icext(uri_rdfs_Datatype,X33)|iext(uri_rdfs_subClassOf,X33,uri_rdfs_Literal))),inference(variable_rename,[status(thm)],[c78])).
% 2.83/3.04  cnf(c80,plain,~icext(uri_rdfs_Datatype,X87)|iext(uri_rdfs_subClassOf,X87,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[c79])).
% 2.83/3.04  cnf(c307,plain,icext(uri_rdfs_Class,uri_rdf_Property),inference(resolution,[status(thm)],[c264, c68])).
% 2.83/3.04  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.83/3.04  fof(c52,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.83/3.04  fof(c53,plain,((![X]:(~lv(X)|icext(uri_rdfs_Literal,X)))&(![X]:(~icext(uri_rdfs_Literal,X)|lv(X)))),inference(shift_quantors,[status(thm)],[c52])).
% 2.83/3.04  fof(c55,plain,(![X23]:(![X24]:((~lv(X23)|icext(uri_rdfs_Literal,X23))&(~icext(uri_rdfs_Literal,X24)|lv(X24))))),inference(shift_quantors,[status(thm)],[fof(c54,plain,((![X23]:(~lv(X23)|icext(uri_rdfs_Literal,X23)))&(![X24]:(~icext(uri_rdfs_Literal,X24)|lv(X24)))),inference(variable_rename,[status(thm)],[c53])).])).
% 2.83/3.04  cnf(c57,plain,~icext(uri_rdfs_Literal,X56)|lv(X56),inference(split_conjunct,[status(thm)],[c55])).
% 2.83/3.04  cnf(c56,plain,~lv(X55)|icext(uri_rdfs_Literal,X55),inference(split_conjunct,[status(thm)],[c55])).
% 2.83/3.04  % SZS output end Saturation
% 2.83/3.04  
% 2.83/3.04  % Initial clauses    : 93
% 2.83/3.04  % Processed clauses  : 537
% 2.83/3.04  % Factors computed   : 5
% 2.83/3.04  % Resolvents computed: 1251
% 2.83/3.04  % Tautologies deleted: 49
% 2.83/3.04  % Forward subsumed   : 763
% 2.83/3.04  % Backward subsumed  : 1
% 2.83/3.04  % -------- CPU Time ---------
% 2.83/3.04  % User time          : 2.658 s
% 2.83/3.04  % System time        : 0.015 s
% 2.83/3.04  % Total time         : 2.673 s
%------------------------------------------------------------------------------