PyRes---1.5.CSA-Sat.s

%------------------------------------------------------------------------------
% File     : PyRes---1.5
% Problem  : SWB028+4 : TPTP v8.1.2. Released v5.2.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s

% Computer : n027.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:56 EDT 2024

% Result   : CounterSatisfiable 2.99s 3.18s
% Output   : Saturation 2.99s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12  % Problem  : SWB028+4 : TPTP v8.1.2. Released v5.2.0.
% 0.03/0.13  % Command  : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34  % Computer : n027.cluster.edu
% 0.13/0.34  % Model    : x86_64 x86_64
% 0.13/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34  % Memory   : 8042.1875MB
% 0.13/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34  % CPULimit : 300
% 0.13/0.34  % WCLimit  : 300
% 0.13/0.34  % DateTime : Wed May  8 22:07:53 EDT 2024
% 0.13/0.34  % CPUTime  : 
% 2.99/3.18  % Version:  1.5
% 2.99/3.18  % SZS status CounterSatisfiable
% 2.99/3.18  % SZS output start Saturation
% 2.99/3.18  fof(rdfs_subpropertyof_main,axiom,(![P]:(![Q]:(iext(uri_rdfs_subPropertyOf,P,Q)=>((ip(P)&ip(Q))&(![X]:(![Y]:(iext(P,X,Y)=>iext(Q,X,Y)))))))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_subpropertyof_main)).
% 2.99/3.18  fof(c20,plain,(![P]:(![Q]:(~iext(uri_rdfs_subPropertyOf,P,Q)|((ip(P)&ip(Q))&(![X]:(![Y]:(~iext(P,X,Y)|iext(Q,X,Y)))))))),inference(fof_nnf,[status(thm)],[rdfs_subpropertyof_main])).
% 2.99/3.18  fof(c22,plain,(![X7]:(![X8]:(![X9]:(![X10]:(~iext(uri_rdfs_subPropertyOf,X7,X8)|((ip(X7)&ip(X8))&(~iext(X7,X9,X10)|iext(X8,X9,X10)))))))),inference(shift_quantors,[status(thm)],[fof(c21,plain,(![X7]:(![X8]:(~iext(uri_rdfs_subPropertyOf,X7,X8)|((ip(X7)&ip(X8))&(![X9]:(![X10]:(~iext(X7,X9,X10)|iext(X8,X9,X10)))))))),inference(variable_rename,[status(thm)],[c20])).])).
% 2.99/3.18  fof(c23,plain,(![X7]:(![X8]:(![X9]:(![X10]:(((~iext(uri_rdfs_subPropertyOf,X7,X8)|ip(X7))&(~iext(uri_rdfs_subPropertyOf,X7,X8)|ip(X8)))&(~iext(uri_rdfs_subPropertyOf,X7,X8)|(~iext(X7,X9,X10)|iext(X8,X9,X10)))))))),inference(distribute,[status(thm)],[c22])).
% 2.99/3.18  cnf(c26,plain,~iext(uri_rdfs_subPropertyOf,X66,X64)|~iext(X66,X63,X65)|iext(X64,X63,X65),inference(split_conjunct,[status(thm)],[c23])).
% 2.99/3.18  fof(rdfs_subpropertyof_reflex,axiom,(![P]:(ip(P)=>iext(uri_rdfs_subPropertyOf,P,P))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_subpropertyof_reflex)).
% 2.99/3.18  fof(c16,plain,(![P]:(~ip(P)|iext(uri_rdfs_subPropertyOf,P,P))),inference(fof_nnf,[status(thm)],[rdfs_subpropertyof_reflex])).
% 2.99/3.18  fof(c17,plain,(![X6]:(~ip(X6)|iext(uri_rdfs_subPropertyOf,X6,X6))),inference(variable_rename,[status(thm)],[c16])).
% 2.99/3.18  cnf(c18,plain,~ip(X51)|iext(uri_rdfs_subPropertyOf,X51,X51),inference(split_conjunct,[status(thm)],[c17])).
% 2.99/3.18  fof(rdf_type_ip,axiom,(![P]:(iext(uri_rdf_type,P,uri_rdf_Property)<=>ip(P))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdf_type_ip)).
% 2.99/3.18  fof(c128,plain,(![P]:((~iext(uri_rdf_type,P,uri_rdf_Property)|ip(P))&(~ip(P)|iext(uri_rdf_type,P,uri_rdf_Property)))),inference(fof_nnf,[status(thm)],[rdf_type_ip])).
% 2.99/3.18  fof(c129,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)],[c128])).
% 2.99/3.18  fof(c131,plain,(![X39]:(![X40]:((~iext(uri_rdf_type,X39,uri_rdf_Property)|ip(X39))&(~ip(X40)|iext(uri_rdf_type,X40,uri_rdf_Property))))),inference(shift_quantors,[status(thm)],[fof(c130,plain,((![X39]:(~iext(uri_rdf_type,X39,uri_rdf_Property)|ip(X39)))&(![X40]:(~ip(X40)|iext(uri_rdf_type,X40,uri_rdf_Property)))),inference(variable_rename,[status(thm)],[c129])).])).
% 2.99/3.18  cnf(c132,plain,~iext(uri_rdf_type,X95,uri_rdf_Property)|ip(X95),inference(split_conjunct,[status(thm)],[c131])).
% 2.99/3.18  fof(rdfs_cext_def,axiom,(![X]:(![C]:(iext(uri_rdf_type,X,C)<=>icext(C,X)))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_cext_def)).
% 2.99/3.18  fof(c111,plain,(![X]:(![C]:((~iext(uri_rdf_type,X,C)|icext(C,X))&(~icext(C,X)|iext(uri_rdf_type,X,C))))),inference(fof_nnf,[status(thm)],[rdfs_cext_def])).
% 2.99/3.18  fof(c112,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)],[c111])).
% 2.99/3.18  fof(c114,plain,(![X35]:(![X36]:(![X37]:(![X38]:((~iext(uri_rdf_type,X35,X36)|icext(X36,X35))&(~icext(X38,X37)|iext(uri_rdf_type,X37,X38))))))),inference(shift_quantors,[status(thm)],[fof(c113,plain,((![X35]:(![X36]:(~iext(uri_rdf_type,X35,X36)|icext(X36,X35))))&(![X37]:(![X38]:(~icext(X38,X37)|iext(uri_rdf_type,X37,X38))))),inference(variable_rename,[status(thm)],[c112])).])).
% 2.99/3.18  cnf(c116,plain,~icext(X92,X91)|iext(uri_rdf_type,X91,X92),inference(split_conjunct,[status(thm)],[c114])).
% 2.99/3.18  fof(rdfs_range_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_range,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_range_domain)).
% 2.99/3.18  cnf(c53,plain,iext(uri_rdfs_domain,uri_rdfs_range,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_range_domain])).
% 2.99/3.18  fof(rdfs_domain_main,axiom,(![P]:(![C]:(![X]:(![Y]:((iext(uri_rdfs_domain,P,C)&iext(P,X,Y))=>icext(C,X)))))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_domain_main)).
% 2.99/3.18  fof(c74,plain,(![P]:(![C]:(![X]:(![Y]:((~iext(uri_rdfs_domain,P,C)|~iext(P,X,Y))|icext(C,X)))))),inference(fof_nnf,[status(thm)],[rdfs_domain_main])).
% 2.99/3.18  fof(c75,plain,(![P]:(![C]:(![X]:((~iext(uri_rdfs_domain,P,C)|(![Y]:~iext(P,X,Y)))|icext(C,X))))),inference(shift_quantors,[status(thm)],[c74])).
% 2.99/3.18  fof(c77,plain,(![X28]:(![X29]:(![X30]:(![X31]:((~iext(uri_rdfs_domain,X28,X29)|~iext(X28,X30,X31))|icext(X29,X30)))))),inference(shift_quantors,[status(thm)],[fof(c76,plain,(![X28]:(![X29]:(![X30]:((~iext(uri_rdfs_domain,X28,X29)|(![X31]:~iext(X28,X30,X31)))|icext(X29,X30))))),inference(variable_rename,[status(thm)],[c75])).])).
% 2.99/3.18  cnf(c78,plain,~iext(uri_rdfs_domain,X82,X84)|~iext(X82,X83,X85)|icext(X84,X83),inference(split_conjunct,[status(thm)],[c77])).
% 2.99/3.18  fof(rdfs_annotation_comment_range,axiom,iext(uri_rdfs_range,uri_rdfs_comment,uri_rdfs_Literal),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_comment_range)).
% 2.99/3.18  cnf(c124,plain,iext(uri_rdfs_range,uri_rdfs_comment,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[rdfs_annotation_comment_range])).
% 2.99/3.18  cnf(c412,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X303)|icext(X303,uri_rdfs_comment),inference(resolution,[status(thm)],[c124, c78])).
% 2.99/3.18  cnf(c1260,plain,icext(uri_rdf_Property,uri_rdfs_comment),inference(resolution,[status(thm)],[c412, c53])).
% 2.99/3.18  cnf(c1261,plain,iext(uri_rdf_type,uri_rdfs_comment,uri_rdf_Property),inference(resolution,[status(thm)],[c1260, c116])).
% 2.99/3.18  cnf(c1262,plain,ip(uri_rdfs_comment),inference(resolution,[status(thm)],[c1261, c132])).
% 2.99/3.18  cnf(c1270,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_comment,uri_rdfs_comment),inference(resolution,[status(thm)],[c1262, c18])).
% 2.99/3.18  cnf(c1273,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X626)|iext(X626,uri_rdfs_comment,uri_rdfs_comment),inference(resolution,[status(thm)],[c1270, c26])).
% 2.99/3.18  cnf(c1263,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X624)|iext(X624,uri_rdfs_comment,uri_rdf_Property),inference(resolution,[status(thm)],[c1261, c26])).
% 2.99/3.18  fof(rdfs_annotation_label_range,axiom,iext(uri_rdfs_range,uri_rdfs_label,uri_rdfs_Literal),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_label_range)).
% 2.99/3.18  cnf(c119,plain,iext(uri_rdfs_range,uri_rdfs_label,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[rdfs_annotation_label_range])).
% 2.99/3.18  cnf(c362,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X284)|icext(X284,uri_rdfs_label),inference(resolution,[status(thm)],[c119, c78])).
% 2.99/3.18  cnf(c1230,plain,icext(uri_rdf_Property,uri_rdfs_label),inference(resolution,[status(thm)],[c362, c53])).
% 2.99/3.18  cnf(c1232,plain,iext(uri_rdf_type,uri_rdfs_label,uri_rdf_Property),inference(resolution,[status(thm)],[c1230, c116])).
% 2.99/3.18  cnf(c1233,plain,ip(uri_rdfs_label),inference(resolution,[status(thm)],[c1232, c132])).
% 2.99/3.18  cnf(c1240,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_label,uri_rdfs_label),inference(resolution,[status(thm)],[c1233, c18])).
% 2.99/3.18  cnf(c1243,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X623)|iext(X623,uri_rdfs_label,uri_rdfs_label),inference(resolution,[status(thm)],[c1240, c26])).
% 2.99/3.18  cnf(c1234,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X621)|iext(X621,uri_rdfs_label,uri_rdf_Property),inference(resolution,[status(thm)],[c1232, c26])).
% 2.99/3.18  fof(rdfs_subclassof_reflex,axiom,(![C]:(ic(C)=>iext(uri_rdfs_subClassOf,C,C))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_subclassof_reflex)).
% 2.99/3.18  fof(c31,plain,(![C]:(~ic(C)|iext(uri_rdfs_subClassOf,C,C))),inference(fof_nnf,[status(thm)],[rdfs_subclassof_reflex])).
% 2.99/3.18  fof(c32,plain,(![X14]:(~ic(X14)|iext(uri_rdfs_subClassOf,X14,X14))),inference(variable_rename,[status(thm)],[c31])).
% 2.99/3.18  cnf(c33,plain,~ic(X70)|iext(uri_rdfs_subClassOf,X70,X70),inference(split_conjunct,[status(thm)],[c32])).
% 2.99/3.18  fof(rdfs_ic_def,axiom,(![X]:(ic(X)<=>icext(uri_rdfs_Class,X))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_ic_def)).
% 2.99/3.18  fof(c67,plain,(![X]:((~ic(X)|icext(uri_rdfs_Class,X))&(~icext(uri_rdfs_Class,X)|ic(X)))),inference(fof_nnf,[status(thm)],[rdfs_ic_def])).
% 2.99/3.18  fof(c68,plain,((![X]:(~ic(X)|icext(uri_rdfs_Class,X)))&(![X]:(~icext(uri_rdfs_Class,X)|ic(X)))),inference(shift_quantors,[status(thm)],[c67])).
% 2.99/3.18  fof(c70,plain,(![X26]:(![X27]:((~ic(X26)|icext(uri_rdfs_Class,X26))&(~icext(uri_rdfs_Class,X27)|ic(X27))))),inference(shift_quantors,[status(thm)],[fof(c69,plain,((![X26]:(~ic(X26)|icext(uri_rdfs_Class,X26)))&(![X27]:(~icext(uri_rdfs_Class,X27)|ic(X27)))),inference(variable_rename,[status(thm)],[c68])).])).
% 2.99/3.18  cnf(c72,plain,~icext(uri_rdfs_Class,X62)|ic(X62),inference(split_conjunct,[status(thm)],[c70])).
% 2.99/3.18  fof(rdfs_range_range,axiom,iext(uri_rdfs_range,uri_rdfs_range,uri_rdfs_Class),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_range_range)).
% 2.99/3.18  cnf(c49,plain,iext(uri_rdfs_range,uri_rdfs_range,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_range_range])).
% 2.99/3.18  fof(rdfs_range_main,axiom,(![P]:(![C]:(![X]:(![Y]:((iext(uri_rdfs_range,P,C)&iext(P,X,Y))=>icext(C,Y)))))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_range_main)).
% 2.99/3.18  fof(c50,plain,(![P]:(![C]:(![X]:(![Y]:((~iext(uri_rdfs_range,P,C)|~iext(P,X,Y))|icext(C,Y)))))),inference(fof_nnf,[status(thm)],[rdfs_range_main])).
% 2.99/3.18  fof(c51,plain,(![X18]:(![X19]:(![X20]:(![X21]:((~iext(uri_rdfs_range,X18,X19)|~iext(X18,X20,X21))|icext(X19,X21)))))),inference(variable_rename,[status(thm)],[c50])).
% 2.99/3.18  cnf(c52,plain,~iext(uri_rdfs_range,X79,X80)|~iext(X79,X81,X78)|icext(X80,X78),inference(split_conjunct,[status(thm)],[c51])).
% 2.99/3.18  fof(rdfs_collection_rest_range,axiom,iext(uri_rdfs_range,uri_rdf_rest,uri_rdf_List),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_collection_rest_range)).
% 2.99/3.18  cnf(c104,plain,iext(uri_rdfs_range,uri_rdf_rest,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdfs_collection_rest_range])).
% 2.99/3.18  cnf(c334,plain,~iext(uri_rdfs_range,uri_rdfs_range,X263)|icext(X263,uri_rdf_List),inference(resolution,[status(thm)],[c104, c52])).
% 2.99/3.18  cnf(c1189,plain,icext(uri_rdfs_Class,uri_rdf_List),inference(resolution,[status(thm)],[c334, c49])).
% 2.99/3.18  cnf(c1191,plain,ic(uri_rdf_List),inference(resolution,[status(thm)],[c1189, c72])).
% 2.99/3.18  cnf(c1195,plain,iext(uri_rdfs_subClassOf,uri_rdf_List,uri_rdf_List),inference(resolution,[status(thm)],[c1191, c33])).
% 2.99/3.18  cnf(c1211,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X619)|iext(X619,uri_rdf_List,uri_rdf_List),inference(resolution,[status(thm)],[c1195, c26])).
% 2.99/3.18  fof(rdfs_subclassof_trans,axiom,(![C]:(![D]:(![E]:((iext(uri_rdfs_subClassOf,C,D)&iext(uri_rdfs_subClassOf,D,E))=>iext(uri_rdfs_subClassOf,C,E))))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_subclassof_trans)).
% 2.99/3.18  fof(c28,plain,(![C]:(![D]:(![E]:((~iext(uri_rdfs_subClassOf,C,D)|~iext(uri_rdfs_subClassOf,D,E))|iext(uri_rdfs_subClassOf,C,E))))),inference(fof_nnf,[status(thm)],[rdfs_subclassof_trans])).
% 2.99/3.18  fof(c29,plain,(![X11]:(![X12]:(![X13]:((~iext(uri_rdfs_subClassOf,X11,X12)|~iext(uri_rdfs_subClassOf,X12,X13))|iext(uri_rdfs_subClassOf,X11,X13))))),inference(variable_rename,[status(thm)],[c28])).
% 2.99/3.18  cnf(c30,plain,~iext(uri_rdfs_subClassOf,X69,X67)|~iext(uri_rdfs_subClassOf,X67,X68)|iext(uri_rdfs_subClassOf,X69,X68),inference(split_conjunct,[status(thm)],[c29])).
% 2.99/3.18  fof(rdfs_class_instsub_resource,axiom,(![C]:(ic(C)=>iext(uri_rdfs_subClassOf,C,uri_rdfs_Resource))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_class_instsub_resource)).
% 2.99/3.18  fof(c108,plain,(![C]:(~ic(C)|iext(uri_rdfs_subClassOf,C,uri_rdfs_Resource))),inference(fof_nnf,[status(thm)],[rdfs_class_instsub_resource])).
% 2.99/3.18  fof(c109,plain,(![X34]:(~ic(X34)|iext(uri_rdfs_subClassOf,X34,uri_rdfs_Resource))),inference(variable_rename,[status(thm)],[c108])).
% 2.99/3.18  cnf(c110,plain,~ic(X88)|iext(uri_rdfs_subClassOf,X88,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[c109])).
% 2.99/3.18  cnf(c1194,plain,iext(uri_rdfs_subClassOf,uri_rdf_List,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1191, c110])).
% 2.99/3.18  cnf(c1208,plain,~iext(uri_rdfs_subClassOf,X618,uri_rdf_List)|iext(uri_rdfs_subClassOf,X618,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1194, c30])).
% 2.99/3.18  cnf(c1202,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X617)|iext(X617,uri_rdf_List,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1194, c26])).
% 2.99/3.18  cnf(c1190,plain,iext(uri_rdf_type,uri_rdf_List,uri_rdfs_Class),inference(resolution,[status(thm)],[c1189, c116])).
% 2.99/3.18  cnf(c1196,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X616)|iext(X616,uri_rdf_List,uri_rdfs_Class),inference(resolution,[status(thm)],[c1190, c26])).
% 2.99/3.18  fof(rdfs_reification_predicate_range,axiom,iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_reification_predicate_range)).
% 2.99/3.18  cnf(c45,plain,iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_reification_predicate_range])).
% 2.99/3.18  cnf(c270,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X218)|icext(X218,uri_rdf_predicate),inference(resolution,[status(thm)],[c78, c45])).
% 2.99/3.18  cnf(c1143,plain,icext(uri_rdf_Property,uri_rdf_predicate),inference(resolution,[status(thm)],[c270, c53])).
% 2.99/3.18  cnf(c1144,plain,iext(uri_rdf_type,uri_rdf_predicate,uri_rdf_Property),inference(resolution,[status(thm)],[c1143, c116])).
% 2.99/3.18  cnf(c1146,plain,ip(uri_rdf_predicate),inference(resolution,[status(thm)],[c1144, c132])).
% 2.99/3.18  cnf(c1152,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_predicate,uri_rdf_predicate),inference(resolution,[status(thm)],[c1146, c18])).
% 2.99/3.18  cnf(c1159,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X615)|iext(X615,uri_rdf_predicate,uri_rdf_predicate),inference(resolution,[status(thm)],[c1152, c26])).
% 2.99/3.18  cnf(c1149,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X613)|iext(X613,uri_rdf_predicate,uri_rdf_Property),inference(resolution,[status(thm)],[c1144, c26])).
% 2.99/3.18  fof(rdfs_type_range,axiom,iext(uri_rdfs_range,uri_rdf_type,uri_rdfs_Class),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_type_range)).
% 2.99/3.18  cnf(c11,plain,iext(uri_rdfs_range,uri_rdf_type,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_type_range])).
% 2.99/3.18  fof(testcase_premise_fullish_028_Inferred_Property_Characteristics_III,axiom,(?[BNODE_z]:(((iext(uri_owl_equivalentClass,uri_ex_InversesOfFunctionalProperties,BNODE_z)&iext(uri_rdf_type,BNODE_z,uri_owl_Restriction))&iext(uri_owl_onProperty,BNODE_z,uri_owl_inverseOf))&iext(uri_owl_someValuesFrom,BNODE_z,uri_owl_FunctionalProperty))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', testcase_premise_fullish_028_Inferred_Property_Characteristics_III)).
% 2.99/3.18  fof(c0,plain,(?[X2]:(((iext(uri_owl_equivalentClass,uri_ex_InversesOfFunctionalProperties,X2)&iext(uri_rdf_type,X2,uri_owl_Restriction))&iext(uri_owl_onProperty,X2,uri_owl_inverseOf))&iext(uri_owl_someValuesFrom,X2,uri_owl_FunctionalProperty))),inference(variable_rename,[status(thm)],[testcase_premise_fullish_028_Inferred_Property_Characteristics_III])).
% 2.99/3.18  fof(c1,plain,(((iext(uri_owl_equivalentClass,uri_ex_InversesOfFunctionalProperties,skolem0001)&iext(uri_rdf_type,skolem0001,uri_owl_Restriction))&iext(uri_owl_onProperty,skolem0001,uri_owl_inverseOf))&iext(uri_owl_someValuesFrom,skolem0001,uri_owl_FunctionalProperty)),inference(skolemize,[status(esa)],[c0])).
% 2.99/3.18  cnf(c3,plain,iext(uri_rdf_type,skolem0001,uri_owl_Restriction),inference(split_conjunct,[status(thm)],[c1])).
% 2.99/3.18  cnf(c247,plain,~iext(uri_rdfs_range,uri_rdf_type,X170)|icext(X170,uri_owl_Restriction),inference(resolution,[status(thm)],[c52, c3])).
% 2.99/3.18  cnf(c1081,plain,icext(uri_rdfs_Class,uri_owl_Restriction),inference(resolution,[status(thm)],[c247, c11])).
% 2.99/3.18  cnf(c1083,plain,ic(uri_owl_Restriction),inference(resolution,[status(thm)],[c1081, c72])).
% 2.99/3.18  cnf(c1086,plain,iext(uri_rdfs_subClassOf,uri_owl_Restriction,uri_owl_Restriction),inference(resolution,[status(thm)],[c1083, c33])).
% 2.99/3.18  cnf(c1129,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X612)|iext(X612,uri_owl_Restriction,uri_owl_Restriction),inference(resolution,[status(thm)],[c1086, c26])).
% 2.99/3.18  cnf(c1085,plain,iext(uri_rdfs_subClassOf,uri_owl_Restriction,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1083, c110])).
% 2.99/3.18  cnf(c1121,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X610)|iext(X610,uri_owl_Restriction,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1085, c26])).
% 2.99/3.18  cnf(c1119,plain,~iext(uri_rdfs_subClassOf,X609,uri_owl_Restriction)|iext(uri_rdfs_subClassOf,X609,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1085, c30])).
% 2.99/3.18  cnf(c1082,plain,iext(uri_rdf_type,uri_owl_Restriction,uri_rdfs_Class),inference(resolution,[status(thm)],[c1081, c116])).
% 2.99/3.18  cnf(c1114,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X608)|iext(X608,uri_owl_Restriction,uri_rdfs_Class),inference(resolution,[status(thm)],[c1082, c26])).
% 2.99/3.18  fof(rdfs_domain_range,axiom,iext(uri_rdfs_range,uri_rdfs_domain,uri_rdfs_Class),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_domain_range)).
% 2.99/3.18  cnf(c73,plain,iext(uri_rdfs_range,uri_rdfs_domain,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_domain_range])).
% 2.99/3.18  fof(rdfs_reification_object_domain,axiom,iext(uri_rdfs_domain,uri_rdf_object,uri_rdfs_Statement),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_reification_object_domain)).
% 2.99/3.18  cnf(c48,plain,iext(uri_rdfs_domain,uri_rdf_object,uri_rdfs_Statement),inference(split_conjunct,[status(thm)],[rdfs_reification_object_domain])).
% 2.99/3.18  cnf(c228,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X151)|icext(X151,uri_rdfs_Statement),inference(resolution,[status(thm)],[c52, c48])).
% 2.99/3.18  cnf(c906,plain,icext(uri_rdfs_Class,uri_rdfs_Statement),inference(resolution,[status(thm)],[c228, c73])).
% 2.99/3.18  cnf(c908,plain,ic(uri_rdfs_Statement),inference(resolution,[status(thm)],[c906, c72])).
% 2.99/3.18  cnf(c911,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Statement,uri_rdfs_Statement),inference(resolution,[status(thm)],[c908, c33])).
% 2.99/3.18  cnf(c1106,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X607)|iext(X607,uri_rdfs_Statement,uri_rdfs_Statement),inference(resolution,[status(thm)],[c911, c26])).
% 2.99/3.18  cnf(c910,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Statement,uri_rdfs_Resource),inference(resolution,[status(thm)],[c908, c110])).
% 2.99/3.18  cnf(c1098,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X605)|iext(X605,uri_rdfs_Statement,uri_rdfs_Resource),inference(resolution,[status(thm)],[c910, c26])).
% 2.99/3.18  cnf(c1096,plain,~iext(uri_rdfs_subClassOf,X604,uri_rdfs_Statement)|iext(uri_rdfs_subClassOf,X604,uri_rdfs_Resource),inference(resolution,[status(thm)],[c910, c30])).
% 2.99/3.18  cnf(c907,plain,iext(uri_rdf_type,uri_rdfs_Statement,uri_rdfs_Class),inference(resolution,[status(thm)],[c906, c116])).
% 2.99/3.18  cnf(c1091,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X603)|iext(X603,uri_rdfs_Statement,uri_rdfs_Class),inference(resolution,[status(thm)],[c907, c26])).
% 2.99/3.18  cnf(c25,plain,~iext(uri_rdfs_subPropertyOf,X57,X56)|ip(X56),inference(split_conjunct,[status(thm)],[c23])).
% 2.99/3.18  fof(rdfs_container_containermembershipproperty_instsub_member,axiom,(![P]:(icext(uri_rdfs_ContainerMembershipProperty,P)=>iext(uri_rdfs_subPropertyOf,P,uri_rdfs_member))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_containermembershipproperty_instsub_member)).
% 2.99/3.18  fof(c99,plain,(![P]:(~icext(uri_rdfs_ContainerMembershipProperty,P)|iext(uri_rdfs_subPropertyOf,P,uri_rdfs_member))),inference(fof_nnf,[status(thm)],[rdfs_container_containermembershipproperty_instsub_member])).
% 2.99/3.18  fof(c100,plain,(![X33]:(~icext(uri_rdfs_ContainerMembershipProperty,X33)|iext(uri_rdfs_subPropertyOf,X33,uri_rdfs_member))),inference(variable_rename,[status(thm)],[c99])).
% 2.99/3.18  cnf(c101,plain,~icext(uri_rdfs_ContainerMembershipProperty,X87)|iext(uri_rdfs_subPropertyOf,X87,uri_rdfs_member),inference(split_conjunct,[status(thm)],[c100])).
% 2.99/3.18  fof(rdfs_container_n_type_001,axiom,iext(uri_rdf_type,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_type_001)).
% 2.99/3.18  cnf(c89,plain,iext(uri_rdf_type,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),inference(split_conjunct,[status(thm)],[rdfs_container_n_type_001])).
% 2.99/3.18  cnf(c115,plain,~iext(uri_rdf_type,X89,X90)|icext(X90,X89),inference(split_conjunct,[status(thm)],[c114])).
% 2.99/3.18  cnf(c373,plain,icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__1),inference(resolution,[status(thm)],[c115, c89])).
% 2.99/3.18  cnf(c381,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__1,uri_rdfs_member),inference(resolution,[status(thm)],[c373, c101])).
% 2.99/3.18  cnf(c755,plain,ip(uri_rdfs_member),inference(resolution,[status(thm)],[c381, c25])).
% 2.99/3.18  cnf(c763,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_member,uri_rdfs_member),inference(resolution,[status(thm)],[c755, c18])).
% 2.99/3.18  cnf(c1079,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X602)|iext(X602,uri_rdfs_member,uri_rdfs_member),inference(resolution,[status(thm)],[c763, c26])).
% 2.99/3.18  cnf(c133,plain,~ip(X96)|iext(uri_rdf_type,X96,uri_rdf_Property),inference(split_conjunct,[status(thm)],[c131])).
% 2.99/3.18  cnf(c762,plain,iext(uri_rdf_type,uri_rdfs_member,uri_rdf_Property),inference(resolution,[status(thm)],[c755, c133])).
% 2.99/3.18  cnf(c1070,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X600)|iext(X600,uri_rdfs_member,uri_rdf_Property),inference(resolution,[status(thm)],[c762, c26])).
% 2.99/3.18  cnf(c71,plain,~ic(X61)|icext(uri_rdfs_Class,X61),inference(split_conjunct,[status(thm)],[c70])).
% 2.99/3.18  fof(rdfs_subclassof_main,axiom,(![C]:(![D]:(iext(uri_rdfs_subClassOf,C,D)=>((ic(C)&ic(D))&(![X]:(icext(C,X)=>icext(D,X))))))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_subclassof_main)).
% 2.99/3.18  fof(c35,plain,(![C]:(![D]:(~iext(uri_rdfs_subClassOf,C,D)|((ic(C)&ic(D))&(![X]:(~icext(C,X)|icext(D,X))))))),inference(fof_nnf,[status(thm)],[rdfs_subclassof_main])).
% 2.99/3.18  fof(c37,plain,(![X15]:(![X16]:(![X17]:(~iext(uri_rdfs_subClassOf,X15,X16)|((ic(X15)&ic(X16))&(~icext(X15,X17)|icext(X16,X17))))))),inference(shift_quantors,[status(thm)],[fof(c36,plain,(![X15]:(![X16]:(~iext(uri_rdfs_subClassOf,X15,X16)|((ic(X15)&ic(X16))&(![X17]:(~icext(X15,X17)|icext(X16,X17))))))),inference(variable_rename,[status(thm)],[c35])).])).
% 2.99/3.18  fof(c38,plain,(![X15]:(![X16]:(![X17]:(((~iext(uri_rdfs_subClassOf,X15,X16)|ic(X15))&(~iext(uri_rdfs_subClassOf,X15,X16)|ic(X16)))&(~iext(uri_rdfs_subClassOf,X15,X16)|(~icext(X15,X17)|icext(X16,X17))))))),inference(distribute,[status(thm)],[c37])).
% 2.99/3.18  cnf(c40,plain,~iext(uri_rdfs_subClassOf,X74,X73)|ic(X73),inference(split_conjunct,[status(thm)],[c38])).
% 2.99/3.18  cnf(c39,plain,~iext(uri_rdfs_subClassOf,X72,X71)|ic(X72),inference(split_conjunct,[status(thm)],[c38])).
% 2.99/3.18  fof(rdfs_container_bag_sub,axiom,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Container),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_bag_sub)).
% 2.99/3.18  cnf(c102,plain,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Container),inference(split_conjunct,[status(thm)],[rdfs_container_bag_sub])).
% 2.99/3.18  cnf(c317,plain,ic(uri_rdf_Bag),inference(resolution,[status(thm)],[c102, c39])).
% 2.99/3.18  cnf(c345,plain,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Resource),inference(resolution,[status(thm)],[c110, c317])).
% 2.99/3.18  cnf(c654,plain,ic(uri_rdfs_Resource),inference(resolution,[status(thm)],[c345, c40])).
% 2.99/3.18  cnf(c662,plain,icext(uri_rdfs_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c654, c71])).
% 2.99/3.18  cnf(c665,plain,iext(uri_rdf_type,uri_rdfs_Resource,uri_rdfs_Class),inference(resolution,[status(thm)],[c662, c116])).
% 2.99/3.18  cnf(c1064,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X599)|iext(X599,uri_rdfs_Resource,uri_rdfs_Class),inference(resolution,[status(thm)],[c665, c26])).
% 2.99/3.18  cnf(c663,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Resource,uri_rdfs_Resource),inference(resolution,[status(thm)],[c654, c110])).
% 2.99/3.18  cnf(c1057,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X598)|iext(X598,uri_rdfs_Resource,uri_rdfs_Resource),inference(resolution,[status(thm)],[c663, c26])).
% 2.99/3.18  cnf(c2,plain,iext(uri_owl_equivalentClass,uri_ex_InversesOfFunctionalProperties,skolem0001),inference(split_conjunct,[status(thm)],[c1])).
% 2.99/3.18  fof(simple_iext_property,axiom,(![S]:(![P]:(![O]:(iext(P,S,O)=>ip(P))))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', simple_iext_property)).
% 2.99/3.18  fof(c148,plain,(![S]:(![P]:(![O]:(~iext(P,S,O)|ip(P))))),inference(fof_nnf,[status(thm)],[simple_iext_property])).
% 2.99/3.18  fof(c149,plain,(![S]:(![P]:((![O]:~iext(P,S,O))|ip(P)))),inference(shift_quantors,[status(thm)],[c148])).
% 2.99/3.18  fof(c151,plain,(![X43]:(![X44]:(![X45]:(~iext(X44,X43,X45)|ip(X44))))),inference(shift_quantors,[status(thm)],[fof(c150,plain,(![X43]:(![X44]:((![X45]:~iext(X44,X43,X45))|ip(X44)))),inference(variable_rename,[status(thm)],[c149])).])).
% 2.99/3.18  cnf(c152,plain,~iext(X98,X99,X97)|ip(X98),inference(split_conjunct,[status(thm)],[c151])).
% 2.99/3.18  cnf(c553,plain,ip(uri_owl_equivalentClass),inference(resolution,[status(thm)],[c152, c2])).
% 2.99/3.18  cnf(c573,plain,iext(uri_rdfs_subPropertyOf,uri_owl_equivalentClass,uri_owl_equivalentClass),inference(resolution,[status(thm)],[c553, c18])).
% 2.99/3.18  cnf(c1050,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X596)|iext(X596,uri_owl_equivalentClass,uri_owl_equivalentClass),inference(resolution,[status(thm)],[c573, c26])).
% 2.99/3.18  cnf(c572,plain,iext(uri_rdf_type,uri_owl_equivalentClass,uri_rdf_Property),inference(resolution,[status(thm)],[c553, c133])).
% 2.99/3.18  cnf(c1040,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X594)|iext(X594,uri_owl_equivalentClass,uri_rdf_Property),inference(resolution,[status(thm)],[c572, c26])).
% 2.99/3.18  cnf(c5,plain,iext(uri_owl_someValuesFrom,skolem0001,uri_owl_FunctionalProperty),inference(split_conjunct,[status(thm)],[c1])).
% 2.99/3.18  cnf(c549,plain,ip(uri_owl_someValuesFrom),inference(resolution,[status(thm)],[c152, c5])).
% 2.99/3.18  cnf(c571,plain,iext(uri_rdfs_subPropertyOf,uri_owl_someValuesFrom,uri_owl_someValuesFrom),inference(resolution,[status(thm)],[c549, c18])).
% 2.99/3.18  cnf(c1034,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X593)|iext(X593,uri_owl_someValuesFrom,uri_owl_someValuesFrom),inference(resolution,[status(thm)],[c571, c26])).
% 2.99/3.18  cnf(c570,plain,iext(uri_rdf_type,uri_owl_someValuesFrom,uri_rdf_Property),inference(resolution,[status(thm)],[c549, c133])).
% 2.99/3.18  cnf(c1025,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X591)|iext(X591,uri_owl_someValuesFrom,uri_rdf_Property),inference(resolution,[status(thm)],[c570, c26])).
% 2.99/3.18  cnf(c4,plain,iext(uri_owl_onProperty,skolem0001,uri_owl_inverseOf),inference(split_conjunct,[status(thm)],[c1])).
% 2.99/3.18  cnf(c546,plain,ip(uri_owl_onProperty),inference(resolution,[status(thm)],[c152, c4])).
% 2.99/3.18  cnf(c569,plain,iext(uri_rdfs_subPropertyOf,uri_owl_onProperty,uri_owl_onProperty),inference(resolution,[status(thm)],[c546, c18])).
% 2.99/3.18  cnf(c1018,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X590)|iext(X590,uri_owl_onProperty,uri_owl_onProperty),inference(resolution,[status(thm)],[c569, c26])).
% 2.99/3.18  cnf(c568,plain,iext(uri_rdf_type,uri_owl_onProperty,uri_rdf_Property),inference(resolution,[status(thm)],[c546, c133])).
% 2.99/3.18  cnf(c1009,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X588)|iext(X588,uri_owl_onProperty,uri_rdf_Property),inference(resolution,[status(thm)],[c568, c26])).
% 2.99/3.18  fof(rdfs_annotation_isdefinedby_sub,axiom,iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_isdefinedby_sub)).
% 2.99/3.18  cnf(c121,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_sub])).
% 2.99/3.18  cnf(c530,plain,ip(uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c152, c121])).
% 2.99/3.18  cnf(c567,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c530, c18])).
% 2.99/3.18  cnf(c1001,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X587)|iext(X587,uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c567, c26])).
% 2.99/3.18  cnf(c566,plain,iext(uri_rdf_type,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c530, c133])).
% 2.99/3.18  cnf(c993,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X585)|iext(X585,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c566, c26])).
% 2.99/3.18  cnf(c502,plain,ip(uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c152, c102])).
% 2.99/3.18  cnf(c565,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c502, c18])).
% 2.99/3.18  cnf(c985,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X584)|iext(X584,uri_rdfs_subClassOf,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c565, c26])).
% 2.99/3.18  cnf(c564,plain,iext(uri_rdf_type,uri_rdfs_subClassOf,uri_rdf_Property),inference(resolution,[status(thm)],[c502, c133])).
% 2.99/3.18  cnf(c975,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X582)|iext(X582,uri_rdfs_subClassOf,uri_rdf_Property),inference(resolution,[status(thm)],[c564, c26])).
% 2.99/3.18  cnf(c498,plain,ip(uri_rdfs_range),inference(resolution,[status(thm)],[c152, c49])).
% 2.99/3.18  cnf(c563,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_range,uri_rdfs_range),inference(resolution,[status(thm)],[c498, c18])).
% 2.99/3.18  cnf(c969,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X581)|iext(X581,uri_rdfs_range,uri_rdfs_range),inference(resolution,[status(thm)],[c563, c26])).
% 2.99/3.18  cnf(c562,plain,iext(uri_rdf_type,uri_rdfs_range,uri_rdf_Property),inference(resolution,[status(thm)],[c498, c133])).
% 2.99/3.18  cnf(c950,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X579)|iext(X579,uri_rdfs_range,uri_rdf_Property),inference(resolution,[status(thm)],[c562, c26])).
% 2.99/3.18  fof(rdfs_container_n_domain_003,axiom,iext(uri_rdfs_domain,uri_rdf__3,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_domain_003)).
% 2.99/3.18  cnf(c93,plain,iext(uri_rdfs_domain,uri_rdf__3,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_003])).
% 2.99/3.18  cnf(c496,plain,ip(uri_rdfs_domain),inference(resolution,[status(thm)],[c152, c93])).
% 2.99/3.18  cnf(c561,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,uri_rdfs_domain),inference(resolution,[status(thm)],[c496, c18])).
% 2.99/3.18  cnf(c940,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X578)|iext(X578,uri_rdfs_domain,uri_rdfs_domain),inference(resolution,[status(thm)],[c561, c26])).
% 2.99/3.18  cnf(c560,plain,iext(uri_rdf_type,uri_rdfs_domain,uri_rdf_Property),inference(resolution,[status(thm)],[c496, c133])).
% 2.99/3.18  cnf(c923,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X576)|iext(X576,uri_rdfs_domain,uri_rdf_Property),inference(resolution,[status(thm)],[c560, c26])).
% 2.99/3.18  fof(rdf_collection_first_type,axiom,iext(uri_rdf_type,uri_rdf_first,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdf_collection_first_type)).
% 2.99/3.18  cnf(c142,plain,iext(uri_rdf_type,uri_rdf_first,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_collection_first_type])).
% 2.99/3.18  cnf(c490,plain,ip(uri_rdf_first),inference(resolution,[status(thm)],[c142, c132])).
% 2.99/3.18  cnf(c494,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_first,uri_rdf_first),inference(resolution,[status(thm)],[c490, c18])).
% 2.99/3.18  cnf(c917,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X575)|iext(X575,uri_rdf_first,uri_rdf_first),inference(resolution,[status(thm)],[c494, c26])).
% 2.99/3.18  fof(rdf_collection_rest_type,axiom,iext(uri_rdf_type,uri_rdf_rest,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdf_collection_rest_type)).
% 2.99/3.18  cnf(c140,plain,iext(uri_rdf_type,uri_rdf_rest,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_collection_rest_type])).
% 2.99/3.18  cnf(c477,plain,ip(uri_rdf_rest),inference(resolution,[status(thm)],[c140, c132])).
% 2.99/3.18  cnf(c481,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_rest,uri_rdf_rest),inference(resolution,[status(thm)],[c477, c18])).
% 2.99/3.18  cnf(c904,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X573)|iext(X573,uri_rdf_rest,uri_rdf_rest),inference(resolution,[status(thm)],[c481, c26])).
% 2.99/3.18  fof(rdf_container_n_type_001,axiom,iext(uri_rdf_type,uri_rdf__1,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdf_container_n_type_001)).
% 2.99/3.18  cnf(c139,plain,iext(uri_rdf_type,uri_rdf__1,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_container_n_type_001])).
% 2.99/3.18  cnf(c468,plain,ip(uri_rdf__1),inference(resolution,[status(thm)],[c139, c132])).
% 2.99/3.18  cnf(c472,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__1,uri_rdf__1),inference(resolution,[status(thm)],[c468, c18])).
% 2.99/3.18  cnf(c895,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X571)|iext(X571,uri_rdf__1,uri_rdf__1),inference(resolution,[status(thm)],[c472, c26])).
% 2.99/3.18  fof(rdf_container_n_type_002,axiom,iext(uri_rdf_type,uri_rdf__2,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdf_container_n_type_002)).
% 2.99/3.18  cnf(c138,plain,iext(uri_rdf_type,uri_rdf__2,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_container_n_type_002])).
% 2.99/3.18  cnf(c461,plain,ip(uri_rdf__2),inference(resolution,[status(thm)],[c138, c132])).
% 2.99/3.18  cnf(c465,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__2,uri_rdf__2),inference(resolution,[status(thm)],[c461, c18])).
% 2.99/3.18  cnf(c888,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X569)|iext(X569,uri_rdf__2,uri_rdf__2),inference(resolution,[status(thm)],[c465, c26])).
% 2.99/3.18  fof(rdf_container_n_type_003,axiom,iext(uri_rdf_type,uri_rdf__3,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdf_container_n_type_003)).
% 2.99/3.18  cnf(c137,plain,iext(uri_rdf_type,uri_rdf__3,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_container_n_type_003])).
% 2.99/3.18  cnf(c453,plain,ip(uri_rdf__3),inference(resolution,[status(thm)],[c137, c132])).
% 2.99/3.18  cnf(c457,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__3,uri_rdf__3),inference(resolution,[status(thm)],[c453, c18])).
% 2.99/3.18  cnf(c880,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X567)|iext(X567,uri_rdf__3,uri_rdf__3),inference(resolution,[status(thm)],[c457, c26])).
% 2.99/3.18  cnf(c372,plain,ip(uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c121, c25])).
% 2.99/3.18  cnf(c450,plain,iext(uri_rdf_type,uri_rdfs_seeAlso,uri_rdf_Property),inference(resolution,[status(thm)],[c133, c372])).
% 2.99/3.18  cnf(c872,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X565)|iext(X565,uri_rdfs_seeAlso,uri_rdf_Property),inference(resolution,[status(thm)],[c450, c26])).
% 2.99/3.18  cnf(c24,plain,~iext(uri_rdfs_subPropertyOf,X53,X52)|ip(X53),inference(split_conjunct,[status(thm)],[c23])).
% 2.99/3.18  cnf(c369,plain,ip(uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c121, c24])).
% 2.99/3.18  cnf(c447,plain,iext(uri_rdf_type,uri_rdfs_isDefinedBy,uri_rdf_Property),inference(resolution,[status(thm)],[c133, c369])).
% 2.99/3.18  cnf(c863,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X564)|iext(X564,uri_rdfs_isDefinedBy,uri_rdf_Property),inference(resolution,[status(thm)],[c447, c26])).
% 2.99/3.18  fof(rdf_value_type,axiom,iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdf_value_type)).
% 2.99/3.18  cnf(c126,plain,iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_value_type])).
% 2.99/3.18  cnf(c439,plain,ip(uri_rdf_type),inference(resolution,[status(thm)],[c132, c126])).
% 2.99/3.18  cnf(c443,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_type,uri_rdf_type),inference(resolution,[status(thm)],[c439, c18])).
% 2.99/3.18  cnf(c857,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X563)|iext(X563,uri_rdf_type,uri_rdf_type),inference(resolution,[status(thm)],[c443, c26])).
% 2.99/3.18  fof(rdf_reification_object_type,axiom,iext(uri_rdf_type,uri_rdf_object,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdf_reification_object_type)).
% 2.99/3.18  cnf(c136,plain,iext(uri_rdf_type,uri_rdf_object,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_reification_object_type])).
% 2.99/3.18  cnf(c438,plain,ip(uri_rdf_object),inference(resolution,[status(thm)],[c132, c136])).
% 2.99/3.18  cnf(c442,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_object,uri_rdf_object),inference(resolution,[status(thm)],[c438, c18])).
% 2.99/3.18  cnf(c843,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X561)|iext(X561,uri_rdf_object,uri_rdf_object),inference(resolution,[status(thm)],[c442, c26])).
% 2.99/3.18  fof(rdf_reification_subject_type,axiom,iext(uri_rdf_type,uri_rdf_subject,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdf_reification_subject_type)).
% 2.99/3.18  cnf(c134,plain,iext(uri_rdf_type,uri_rdf_subject,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_reification_subject_type])).
% 2.99/3.18  cnf(c437,plain,ip(uri_rdf_subject),inference(resolution,[status(thm)],[c132, c134])).
% 2.99/3.18  cnf(c441,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_subject,uri_rdf_subject),inference(resolution,[status(thm)],[c437, c18])).
% 2.99/3.18  cnf(c836,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X559)|iext(X559,uri_rdf_subject,uri_rdf_subject),inference(resolution,[status(thm)],[c441, c26])).
% 2.99/3.18  fof(rdf_reification_predicate_type,axiom,iext(uri_rdf_type,uri_rdf_value,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdf_reification_predicate_type)).
% 2.99/3.18  cnf(c135,plain,iext(uri_rdf_type,uri_rdf_value,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_reification_predicate_type])).
% 2.99/3.18  cnf(c436,plain,ip(uri_rdf_value),inference(resolution,[status(thm)],[c132, c135])).
% 2.99/3.18  cnf(c440,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_value,uri_rdf_value),inference(resolution,[status(thm)],[c436, c18])).
% 2.99/3.18  cnf(c829,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X557)|iext(X557,uri_rdf_value,uri_rdf_value),inference(resolution,[status(thm)],[c440, c26])).
% 2.99/3.18  fof(rdfs_container_n_type_002,axiom,iext(uri_rdf_type,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_type_002)).
% 2.99/3.18  cnf(c88,plain,iext(uri_rdf_type,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),inference(split_conjunct,[status(thm)],[rdfs_container_n_type_002])).
% 2.99/3.18  cnf(c378,plain,icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__2),inference(resolution,[status(thm)],[c115, c88])).
% 2.99/3.18  cnf(c400,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__2,uri_rdfs_member),inference(resolution,[status(thm)],[c378, c101])).
% 2.99/3.18  cnf(c822,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X555)|iext(X555,uri_rdf__2,uri_rdfs_member),inference(resolution,[status(thm)],[c400, c26])).
% 2.99/3.18  fof(rdfs_subpropertyof_trans,axiom,(![P]:(![Q]:(![R]:((iext(uri_rdfs_subPropertyOf,P,Q)&iext(uri_rdfs_subPropertyOf,Q,R))=>iext(uri_rdfs_subPropertyOf,P,R))))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_subpropertyof_trans)).
% 2.99/3.18  fof(c13,plain,(![P]:(![Q]:(![R]:((~iext(uri_rdfs_subPropertyOf,P,Q)|~iext(uri_rdfs_subPropertyOf,Q,R))|iext(uri_rdfs_subPropertyOf,P,R))))),inference(fof_nnf,[status(thm)],[rdfs_subpropertyof_trans])).
% 2.99/3.18  fof(c14,plain,(![X3]:(![X4]:(![X5]:((~iext(uri_rdfs_subPropertyOf,X3,X4)|~iext(uri_rdfs_subPropertyOf,X4,X5))|iext(uri_rdfs_subPropertyOf,X3,X5))))),inference(variable_rename,[status(thm)],[c13])).
% 2.99/3.18  cnf(c15,plain,~iext(uri_rdfs_subPropertyOf,X50,X49)|~iext(uri_rdfs_subPropertyOf,X49,X48)|iext(uri_rdfs_subPropertyOf,X50,X48),inference(split_conjunct,[status(thm)],[c14])).
% 2.99/3.18  cnf(c819,plain,~iext(uri_rdfs_subPropertyOf,X554,uri_rdf__2)|iext(uri_rdfs_subPropertyOf,X554,uri_rdfs_member),inference(resolution,[status(thm)],[c400, c15])).
% 2.99/3.18  fof(rdfs_container_n_type_003,axiom,iext(uri_rdf_type,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_type_003)).
% 2.99/3.18  cnf(c87,plain,iext(uri_rdf_type,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),inference(split_conjunct,[status(thm)],[rdfs_container_n_type_003])).
% 2.99/3.18  cnf(c376,plain,icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__3),inference(resolution,[status(thm)],[c115, c87])).
% 2.99/3.18  cnf(c397,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__3,uri_rdfs_member),inference(resolution,[status(thm)],[c376, c101])).
% 2.99/3.18  cnf(c815,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X553)|iext(X553,uri_rdf__3,uri_rdfs_member),inference(resolution,[status(thm)],[c397, c26])).
% 2.99/3.18  cnf(c812,plain,~iext(uri_rdfs_subPropertyOf,X552,uri_rdf__3)|iext(uri_rdfs_subPropertyOf,X552,uri_rdfs_member),inference(resolution,[status(thm)],[c397, c15])).
% 2.99/3.18  fof(rdfs_dat_xmlliteral_sub,axiom,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Literal),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_dat_xmlliteral_sub)).
% 2.99/3.18  cnf(c85,plain,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[rdfs_dat_xmlliteral_sub])).
% 2.99/3.18  cnf(c197,plain,ic(uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c39, c85])).
% 2.99/3.18  cnf(c202,plain,icext(uri_rdfs_Class,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c197, c71])).
% 2.99/3.18  cnf(c395,plain,iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Class),inference(resolution,[status(thm)],[c116, c202])).
% 2.99/3.18  cnf(c808,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X551)|iext(X551,uri_rdf_XMLLiteral,uri_rdfs_Class),inference(resolution,[status(thm)],[c395, c26])).
% 2.99/3.18  cnf(c207,plain,ic(uri_rdfs_Literal),inference(resolution,[status(thm)],[c40, c85])).
% 2.99/3.18  cnf(c212,plain,icext(uri_rdfs_Class,uri_rdfs_Literal),inference(resolution,[status(thm)],[c207, c71])).
% 2.99/3.18  cnf(c394,plain,iext(uri_rdf_type,uri_rdfs_Literal,uri_rdfs_Class),inference(resolution,[status(thm)],[c116, c212])).
% 2.99/3.18  cnf(c803,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X550)|iext(X550,uri_rdfs_Literal,uri_rdfs_Class),inference(resolution,[status(thm)],[c394, c26])).
% 2.99/3.18  fof(rdfs_container_seq_sub,axiom,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Container),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_seq_sub)).
% 2.99/3.18  cnf(c86,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Container),inference(split_conjunct,[status(thm)],[rdfs_container_seq_sub])).
% 2.99/3.18  cnf(c205,plain,ic(uri_rdfs_Container),inference(resolution,[status(thm)],[c40, c86])).
% 2.99/3.18  cnf(c208,plain,icext(uri_rdfs_Class,uri_rdfs_Container),inference(resolution,[status(thm)],[c205, c71])).
% 2.99/3.18  cnf(c393,plain,iext(uri_rdf_type,uri_rdfs_Container,uri_rdfs_Class),inference(resolution,[status(thm)],[c116, c208])).
% 2.99/3.18  cnf(c798,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X549)|iext(X549,uri_rdfs_Container,uri_rdfs_Class),inference(resolution,[status(thm)],[c393, c26])).
% 2.99/3.18  fof(rdfs_datatype_sub,axiom,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Class),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_datatype_sub)).
% 2.99/3.18  cnf(c80,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_datatype_sub])).
% 2.99/3.18  cnf(c206,plain,ic(uri_rdfs_Class),inference(resolution,[status(thm)],[c40, c80])).
% 2.99/3.18  cnf(c210,plain,icext(uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c206, c71])).
% 2.99/3.18  cnf(c392,plain,iext(uri_rdf_type,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c116, c210])).
% 2.99/3.18  cnf(c793,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X548)|iext(X548,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c392, c26])).
% 2.99/3.18  cnf(c196,plain,ic(uri_rdfs_Datatype),inference(resolution,[status(thm)],[c39, c80])).
% 2.99/3.18  cnf(c200,plain,icext(uri_rdfs_Class,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c196, c71])).
% 2.99/3.18  cnf(c391,plain,iext(uri_rdf_type,uri_rdfs_Datatype,uri_rdfs_Class),inference(resolution,[status(thm)],[c116, c200])).
% 2.99/3.18  cnf(c788,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X547)|iext(X547,uri_rdfs_Datatype,uri_rdfs_Class),inference(resolution,[status(thm)],[c391, c26])).
% 2.99/3.18  fof(rdfs_container_alt_sub,axiom,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Container),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_alt_sub)).
% 2.99/3.18  cnf(c103,plain,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Container),inference(split_conjunct,[status(thm)],[rdfs_container_alt_sub])).
% 2.99/3.18  cnf(c327,plain,ic(uri_rdf_Alt),inference(resolution,[status(thm)],[c103, c39])).
% 2.99/3.18  cnf(c330,plain,icext(uri_rdfs_Class,uri_rdf_Alt),inference(resolution,[status(thm)],[c327, c71])).
% 2.99/3.18  cnf(c389,plain,iext(uri_rdf_type,uri_rdf_Alt,uri_rdfs_Class),inference(resolution,[status(thm)],[c116, c330])).
% 2.99/3.18  cnf(c783,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X546)|iext(X546,uri_rdf_Alt,uri_rdfs_Class),inference(resolution,[status(thm)],[c389, c26])).
% 2.99/3.18  fof(rdfs_container_containermembershipproperty_sub,axiom,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_containermembershipproperty_sub)).
% 2.99/3.18  cnf(c98,plain,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_container_containermembershipproperty_sub])).
% 2.99/3.18  cnf(c304,plain,ic(uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c98, c39])).
% 2.99/3.18  cnf(c309,plain,icext(uri_rdfs_Class,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c304, c71])).
% 2.99/3.18  cnf(c388,plain,iext(uri_rdf_type,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Class),inference(resolution,[status(thm)],[c116, c309])).
% 2.99/3.18  cnf(c778,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X545)|iext(X545,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Class),inference(resolution,[status(thm)],[c388, c26])).
% 2.99/3.18  cnf(c320,plain,icext(uri_rdfs_Class,uri_rdf_Bag),inference(resolution,[status(thm)],[c317, c71])).
% 2.99/3.18  cnf(c387,plain,iext(uri_rdf_type,uri_rdf_Bag,uri_rdfs_Class),inference(resolution,[status(thm)],[c116, c320])).
% 2.99/3.18  cnf(c773,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X544)|iext(X544,uri_rdf_Bag,uri_rdfs_Class),inference(resolution,[status(thm)],[c387, c26])).
% 2.99/3.18  cnf(c1278,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X543)|icext(X543,uri_rdfs_comment),inference(resolution,[status(thm)],[c1270, c52])).
% 2.99/3.18  cnf(c1274,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X542)|icext(X542,uri_rdfs_comment),inference(resolution,[status(thm)],[c1270, c78])).
% 2.99/3.18  cnf(c195,plain,ic(uri_rdfs_Seq),inference(resolution,[status(thm)],[c39, c86])).
% 2.99/3.18  cnf(c198,plain,icext(uri_rdfs_Class,uri_rdfs_Seq),inference(resolution,[status(thm)],[c195, c71])).
% 2.99/3.18  cnf(c383,plain,iext(uri_rdf_type,uri_rdfs_Seq,uri_rdfs_Class),inference(resolution,[status(thm)],[c116, c198])).
% 2.99/3.18  cnf(c767,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X541)|iext(X541,uri_rdfs_Seq,uri_rdfs_Class),inference(resolution,[status(thm)],[c383, c26])).
% 2.99/3.18  cnf(c1248,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X538)|icext(X538,uri_rdfs_label),inference(resolution,[status(thm)],[c1240, c52])).
% 2.99/3.18  cnf(c760,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X537)|iext(X537,uri_rdf__1,uri_rdfs_member),inference(resolution,[status(thm)],[c381, c26])).
% 2.99/3.18  cnf(c1244,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X536)|icext(X536,uri_rdfs_label),inference(resolution,[status(thm)],[c1240, c78])).
% 2.99/3.18  cnf(c757,plain,~iext(uri_rdfs_subPropertyOf,X533,uri_rdf__1)|iext(uri_rdfs_subPropertyOf,X533,uri_rdfs_member),inference(resolution,[status(thm)],[c381, c15])).
% 2.99/3.18  cnf(c1218,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X532)|icext(X532,uri_rdf_List),inference(resolution,[status(thm)],[c1195, c52])).
% 2.99/3.18  cnf(c380,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_seeAlso,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c372, c18])).
% 2.99/3.18  cnf(c753,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X529)|iext(X529,uri_rdfs_seeAlso,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c380, c26])).
% 2.99/3.18  cnf(c1204,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X528)|icext(X528,uri_rdf_List),inference(resolution,[status(thm)],[c1194, c78])).
% 2.99/3.18  cnf(c1160,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X524)|icext(X524,uri_rdf_predicate),inference(resolution,[status(thm)],[c1152, c52])).
% 2.99/3.18  cnf(c1157,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X523)|icext(X523,uri_rdf_predicate),inference(resolution,[status(thm)],[c1152, c78])).
% 2.99/3.18  cnf(c379,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c369, c18])).
% 2.99/3.18  cnf(c745,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X521)|iext(X521,uri_rdfs_isDefinedBy,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c379, c26])).
% 2.99/3.18  cnf(c1131,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X519)|icext(X519,uri_owl_Restriction),inference(resolution,[status(thm)],[c1086, c52])).
% 2.99/3.18  cnf(c1118,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X515)|icext(X515,uri_owl_Restriction),inference(resolution,[status(thm)],[c1085, c78])).
% 2.99/3.18  cnf(c354,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Resource),inference(resolution,[status(thm)],[c110, c195])).
% 2.99/3.18  cnf(c736,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X512)|iext(X512,uri_rdfs_Seq,uri_rdfs_Resource),inference(resolution,[status(thm)],[c354, c26])).
% 2.99/3.18  cnf(c1108,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X511)|icext(X511,uri_rdfs_Statement),inference(resolution,[status(thm)],[c911, c52])).
% 2.99/3.18  cnf(c734,plain,~iext(uri_rdfs_subClassOf,X508,uri_rdfs_Seq)|iext(uri_rdfs_subClassOf,X508,uri_rdfs_Resource),inference(resolution,[status(thm)],[c354, c30])).
% 2.99/3.18  cnf(c1095,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X507)|icext(X507,uri_rdfs_Statement),inference(resolution,[status(thm)],[c910, c78])).
% 2.99/3.18  cnf(c353,plain,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Resource),inference(resolution,[status(thm)],[c110, c304])).
% 2.99/3.18  cnf(c728,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X504)|iext(X504,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Resource),inference(resolution,[status(thm)],[c353, c26])).
% 2.99/3.18  cnf(c1077,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X502)|icext(X502,uri_rdfs_member),inference(resolution,[status(thm)],[c763, c78])).
% 2.99/3.18  cnf(c726,plain,~iext(uri_rdfs_subClassOf,X500,uri_rdfs_ContainerMembershipProperty)|iext(uri_rdfs_subClassOf,X500,uri_rdfs_Resource),inference(resolution,[status(thm)],[c353, c30])).
% 2.99/3.18  cnf(c352,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c110, c206])).
% 2.99/3.18  cnf(c720,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X495)|iext(X495,uri_rdfs_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c352, c26])).
% 2.99/3.18  cnf(c1054,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X494)|icext(X494,uri_rdfs_Resource),inference(resolution,[status(thm)],[c663, c78])).
% 2.99/3.18  cnf(c718,plain,~iext(uri_rdfs_subClassOf,X493,uri_rdfs_Class)|iext(uri_rdfs_subClassOf,X493,uri_rdfs_Resource),inference(resolution,[status(thm)],[c352, c30])).
% 2.99/3.18  cnf(c1051,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X492)|icext(X492,uri_owl_equivalentClass),inference(resolution,[status(thm)],[c573, c52])).
% 2.99/3.18  cnf(c1048,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X491)|icext(X491,uri_owl_equivalentClass),inference(resolution,[status(thm)],[c573, c78])).
% 2.99/3.18  cnf(c351,plain,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Resource),inference(resolution,[status(thm)],[c110, c327])).
% 2.99/3.18  cnf(c712,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X489)|iext(X489,uri_rdf_Alt,uri_rdfs_Resource),inference(resolution,[status(thm)],[c351, c26])).
% 2.99/3.18  cnf(c1035,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X487)|icext(X487,uri_owl_someValuesFrom),inference(resolution,[status(thm)],[c571, c52])).
% 2.99/3.18  cnf(c710,plain,~iext(uri_rdfs_subClassOf,X486,uri_rdf_Alt)|iext(uri_rdfs_subClassOf,X486,uri_rdfs_Resource),inference(resolution,[status(thm)],[c351, c30])).
% 2.99/3.18  cnf(c1032,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X485)|icext(X485,uri_owl_someValuesFrom),inference(resolution,[status(thm)],[c571, c78])).
% 2.99/3.18  cnf(c350,plain,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Resource),inference(resolution,[status(thm)],[c110, c197])).
% 2.99/3.18  cnf(c704,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X482)|iext(X482,uri_rdf_XMLLiteral,uri_rdfs_Resource),inference(resolution,[status(thm)],[c350, c26])).
% 2.99/3.18  cnf(c1019,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X481)|icext(X481,uri_owl_onProperty),inference(resolution,[status(thm)],[c569, c52])).
% 2.99/3.18  cnf(c1016,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X480)|icext(X480,uri_owl_onProperty),inference(resolution,[status(thm)],[c569, c78])).
% 2.99/3.18  cnf(c702,plain,~iext(uri_rdfs_subClassOf,X478,uri_rdf_XMLLiteral)|iext(uri_rdfs_subClassOf,X478,uri_rdfs_Resource),inference(resolution,[status(thm)],[c350, c30])).
% 2.99/3.18  cnf(c1003,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X476)|icext(X476,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c567, c52])).
% 2.99/3.18  cnf(c302,plain,ic(uri_rdf_Property),inference(resolution,[status(thm)],[c98, c40])).
% 2.99/3.18  cnf(c349,plain,iext(uri_rdfs_subClassOf,uri_rdf_Property,uri_rdfs_Resource),inference(resolution,[status(thm)],[c110, c302])).
% 2.99/3.18  cnf(c696,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X475)|iext(X475,uri_rdf_Property,uri_rdfs_Resource),inference(resolution,[status(thm)],[c349, c26])).
% 2.99/3.18  cnf(c999,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X474)|icext(X474,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c567, c78])).
% 2.99/3.18  cnf(c694,plain,~iext(uri_rdfs_subClassOf,X471,uri_rdf_Property)|iext(uri_rdfs_subClassOf,X471,uri_rdfs_Resource),inference(resolution,[status(thm)],[c349, c30])).
% 2.99/3.18  cnf(c987,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X470)|icext(X470,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c565, c52])).
% 2.99/3.18  cnf(c983,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X469)|icext(X469,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c565, c78])).
% 2.99/3.18  cnf(c348,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Container,uri_rdfs_Resource),inference(resolution,[status(thm)],[c110, c205])).
% 2.99/3.18  cnf(c688,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X468)|iext(X468,uri_rdfs_Container,uri_rdfs_Resource),inference(resolution,[status(thm)],[c348, c26])).
% 2.99/3.18  cnf(c686,plain,~iext(uri_rdfs_subClassOf,X466,uri_rdfs_Container)|iext(uri_rdfs_subClassOf,X466,uri_rdfs_Resource),inference(resolution,[status(thm)],[c348, c30])).
% 2.99/3.18  cnf(c970,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X464)|icext(X464,uri_rdfs_range),inference(resolution,[status(thm)],[c563, c52])).
% 2.99/3.18  cnf(c347,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Resource),inference(resolution,[status(thm)],[c110, c196])).
% 2.99/3.18  cnf(c680,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X463)|iext(X463,uri_rdfs_Datatype,uri_rdfs_Resource),inference(resolution,[status(thm)],[c347, c26])).
% 2.99/3.18  cnf(c967,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X462)|icext(X462,uri_rdfs_range),inference(resolution,[status(thm)],[c563, c78])).
% 2.99/3.18  cnf(c678,plain,~iext(uri_rdfs_subClassOf,X459,uri_rdfs_Datatype)|iext(uri_rdfs_subClassOf,X459,uri_rdfs_Resource),inference(resolution,[status(thm)],[c347, c30])).
% 2.99/3.18  cnf(c944,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X458)|icext(X458,uri_rdfs_domain),inference(resolution,[status(thm)],[c561, c52])).
% 2.99/3.18  cnf(c935,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X457)|icext(X457,uri_rdfs_domain),inference(resolution,[status(thm)],[c561, c78])).
% 2.99/3.18  cnf(c346,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Literal,uri_rdfs_Resource),inference(resolution,[status(thm)],[c110, c207])).
% 2.99/3.18  cnf(c672,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X455)|iext(X455,uri_rdfs_Literal,uri_rdfs_Resource),inference(resolution,[status(thm)],[c346, c26])).
% 2.99/3.18  cnf(c918,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X453)|icext(X453,uri_rdf_first),inference(resolution,[status(thm)],[c494, c52])).
% 2.99/3.18  cnf(c670,plain,~iext(uri_rdfs_subClassOf,X452,uri_rdfs_Literal)|iext(uri_rdfs_subClassOf,X452,uri_rdfs_Resource),inference(resolution,[status(thm)],[c346, c30])).
% 2.99/3.18  cnf(c915,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X451)|icext(X451,uri_rdf_first),inference(resolution,[status(thm)],[c494, c78])).
% 2.99/3.18  cnf(c905,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X450)|icext(X450,uri_rdf_rest),inference(resolution,[status(thm)],[c481, c52])).
% 2.99/3.18  cnf(c659,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X449)|iext(X449,uri_rdf_Bag,uri_rdfs_Resource),inference(resolution,[status(thm)],[c345, c26])).
% 2.99/3.18  cnf(c902,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X448)|icext(X448,uri_rdf_rest),inference(resolution,[status(thm)],[c481, c78])).
% 2.99/3.18  cnf(c896,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X447)|icext(X447,uri_rdf__1),inference(resolution,[status(thm)],[c472, c52])).
% 2.99/3.18  cnf(c657,plain,~iext(uri_rdfs_subClassOf,X446,uri_rdf_Bag)|iext(uri_rdfs_subClassOf,X446,uri_rdfs_Resource),inference(resolution,[status(thm)],[c345, c30])).
% 2.99/3.18  cnf(c889,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X444)|icext(X444,uri_rdf__2),inference(resolution,[status(thm)],[c465, c52])).
% 2.99/3.18  cnf(c331,plain,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdf_Alt),inference(resolution,[status(thm)],[c327, c33])).
% 2.99/3.18  cnf(c651,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X442)|iext(X442,uri_rdf_Alt,uri_rdf_Alt),inference(resolution,[status(thm)],[c331, c26])).
% 2.99/3.18  cnf(c881,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X441)|icext(X441,uri_rdf__3),inference(resolution,[status(thm)],[c457, c52])).
% 2.99/3.18  cnf(c858,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X434)|icext(X434,uri_rdf_type),inference(resolution,[status(thm)],[c443, c52])).
% 2.99/3.18  cnf(c321,plain,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdf_Bag),inference(resolution,[status(thm)],[c317, c33])).
% 2.99/3.18  cnf(c643,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X433)|iext(X433,uri_rdf_Bag,uri_rdf_Bag),inference(resolution,[status(thm)],[c321, c26])).
% 2.99/3.18  cnf(c852,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X432)|icext(X432,uri_rdf_type),inference(resolution,[status(thm)],[c443, c78])).
% 2.99/3.18  cnf(c844,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X431)|icext(X431,uri_rdf_object),inference(resolution,[status(thm)],[c442, c52])).
% 2.99/3.18  cnf(c841,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X429)|icext(X429,uri_rdf_object),inference(resolution,[status(thm)],[c442, c78])).
% 2.99/3.18  cnf(c837,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X428)|icext(X428,uri_rdf_subject),inference(resolution,[status(thm)],[c441, c52])).
% 2.99/3.18  cnf(c310,plain,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c304, c33])).
% 2.99/3.18  cnf(c635,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X427)|iext(X427,uri_rdfs_ContainerMembershipProperty,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c310, c26])).
% 2.99/3.18  cnf(c834,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X426)|icext(X426,uri_rdf_subject),inference(resolution,[status(thm)],[c441, c78])).
% 2.99/3.18  cnf(c830,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X425)|icext(X425,uri_rdf_value),inference(resolution,[status(thm)],[c440, c52])).
% 2.99/3.18  cnf(c827,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X424)|icext(X424,uri_rdf_value),inference(resolution,[status(thm)],[c440, c78])).
% 2.99/3.18  cnf(c820,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X421)|icext(X421,uri_rdf__2),inference(resolution,[status(thm)],[c400, c78])).
% 2.99/3.18  cnf(c308,plain,iext(uri_rdfs_subClassOf,uri_rdf_Property,uri_rdf_Property),inference(resolution,[status(thm)],[c302, c33])).
% 2.99/3.18  cnf(c627,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X419)|iext(X419,uri_rdf_Property,uri_rdf_Property),inference(resolution,[status(thm)],[c308, c26])).
% 2.99/3.18  cnf(c813,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X418)|icext(X418,uri_rdf__3),inference(resolution,[status(thm)],[c397, c78])).
% 2.99/3.18  cnf(c213,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Literal,uri_rdfs_Literal),inference(resolution,[status(thm)],[c207, c33])).
% 2.99/3.18  cnf(c619,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X409)|iext(X409,uri_rdfs_Literal,uri_rdfs_Literal),inference(resolution,[status(thm)],[c213, c26])).
% 2.99/3.18  cnf(c211,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c206, c33])).
% 2.99/3.18  cnf(c611,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X398)|iext(X398,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c211, c26])).
% 2.99/3.18  cnf(c761,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X395)|icext(X395,uri_rdfs_member),inference(resolution,[status(thm)],[c381, c52])).
% 2.99/3.18  cnf(c758,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X393)|icext(X393,uri_rdf__1),inference(resolution,[status(thm)],[c381, c78])).
% 2.99/3.18  cnf(c751,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X391)|icext(X391,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c380, c78])).
% 2.99/3.18  cnf(c209,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Container,uri_rdfs_Container),inference(resolution,[status(thm)],[c205, c33])).
% 2.99/3.18  cnf(c603,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X390)|iext(X390,uri_rdfs_Container,uri_rdfs_Container),inference(resolution,[status(thm)],[c209, c26])).
% 2.99/3.18  cnf(c746,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X389)|icext(X389,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c379, c52])).
% 2.99/3.18  cnf(c203,plain,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c197, c33])).
% 2.99/3.18  cnf(c595,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X380)|iext(X380,uri_rdf_XMLLiteral,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c203, c26])).
% 2.99/3.18  cnf(c201,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c196, c33])).
% 2.99/3.18  cnf(c587,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X369)|iext(X369,uri_rdfs_Datatype,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c201, c26])).
% 2.99/3.18  cnf(c661,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X365)|icext(X365,uri_rdfs_Resource),inference(resolution,[status(thm)],[c345, c52])).
% 2.99/3.18  cnf(c653,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X362)|icext(X362,uri_rdf_Alt),inference(resolution,[status(thm)],[c331, c52])).
% 2.99/3.18  cnf(c199,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Seq),inference(resolution,[status(thm)],[c195, c33])).
% 2.99/3.18  cnf(c579,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X360)|iext(X360,uri_rdfs_Seq,uri_rdfs_Seq),inference(resolution,[status(thm)],[c199, c26])).
% 2.99/3.18  cnf(c645,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X359)|icext(X359,uri_rdf_Bag),inference(resolution,[status(thm)],[c321, c52])).
% 2.99/3.18  cnf(c637,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X357)|icext(X357,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c310, c52])).
% 2.99/3.18  cnf(c624,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X353)|icext(X353,uri_rdf_Property),inference(resolution,[status(thm)],[c308, c78])).
% 2.99/3.18  cnf(c488,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X352)|iext(X352,uri_rdf_first,uri_rdf_Property),inference(resolution,[status(thm)],[c142, c26])).
% 2.99/3.18  cnf(c616,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X350)|icext(X350,uri_rdfs_Literal),inference(resolution,[status(thm)],[c213, c78])).
% 2.99/3.18  fof(rdf_collection_nil_type,axiom,iext(uri_rdf_type,uri_rdf_nil,uri_rdf_List),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdf_collection_nil_type)).
% 2.99/3.18  cnf(c141,plain,iext(uri_rdf_type,uri_rdf_nil,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdf_collection_nil_type])).
% 2.99/3.18  cnf(c482,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X348)|iext(X348,uri_rdf_nil,uri_rdf_List),inference(resolution,[status(thm)],[c141, c26])).
% 2.99/3.18  cnf(c608,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X347)|icext(X347,uri_rdfs_Class),inference(resolution,[status(thm)],[c211, c78])).
% 2.99/3.18  cnf(c475,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X345)|iext(X345,uri_rdf_rest,uri_rdf_Property),inference(resolution,[status(thm)],[c140, c26])).
% 2.99/3.18  cnf(c600,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X344)|icext(X344,uri_rdfs_Container),inference(resolution,[status(thm)],[c209, c78])).
% 2.99/3.18  cnf(c597,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X343)|icext(X343,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c203, c52])).
% 2.99/3.18  cnf(c466,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X341)|iext(X341,uri_rdf__1,uri_rdf_Property),inference(resolution,[status(thm)],[c139, c26])).
% 2.99/3.18  cnf(c589,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X340)|icext(X340,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c201, c52])).
% 2.99/3.18  cnf(c459,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X338)|iext(X338,uri_rdf__2,uri_rdf_Property),inference(resolution,[status(thm)],[c138, c26])).
% 2.99/3.18  cnf(c581,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X337)|icext(X337,uri_rdfs_Seq),inference(resolution,[status(thm)],[c199, c52])).
% 2.99/3.18  cnf(c451,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X333)|iext(X333,uri_rdf__3,uri_rdf_Property),inference(resolution,[status(thm)],[c137, c26])).
% 2.99/3.18  cnf(c484,plain,~iext(uri_rdfs_range,uri_rdf_type,X332)|icext(X332,uri_rdf_List),inference(resolution,[status(thm)],[c141, c52])).
% 2.99/3.18  cnf(c432,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X329)|iext(X329,uri_rdf_object,uri_rdf_Property),inference(resolution,[status(thm)],[c136, c26])).
% 2.99/3.18  cnf(c427,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X324)|iext(X324,uri_rdf_value,uri_rdf_Property),inference(resolution,[status(thm)],[c135, c26])).
% 2.99/3.18  cnf(c422,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X319)|iext(X319,uri_rdf_subject,uri_rdf_Property),inference(resolution,[status(thm)],[c134, c26])).
% 2.99/3.18  cnf(c417,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X314)|iext(X314,uri_rdf_type,uri_rdf_Property),inference(resolution,[status(thm)],[c126, c26])).
% 2.99/3.18  cnf(c419,plain,~iext(uri_rdfs_range,uri_rdf_type,X312)|icext(X312,uri_rdf_Property),inference(resolution,[status(thm)],[c126, c52])).
% 2.99/3.18  fof(rdfs_annotation_comment_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_comment,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_comment_domain)).
% 2.99/3.18  cnf(c125,plain,iext(uri_rdfs_domain,uri_rdfs_comment,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_comment_domain])).
% 2.99/3.18  cnf(c414,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X310)|iext(X310,uri_rdfs_comment,uri_rdfs_Resource),inference(resolution,[status(thm)],[c125, c26])).
% 2.99/3.18  cnf(c415,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X308)|icext(X308,uri_rdfs_comment),inference(resolution,[status(thm)],[c125, c78])).
% 2.99/3.18  cnf(c411,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X306)|iext(X306,uri_rdfs_comment,uri_rdfs_Literal),inference(resolution,[status(thm)],[c124, c26])).
% 2.99/3.18  fof(rdfs_annotation_isdefinedby_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_isdefinedby_domain)).
% 2.99/3.18  cnf(c123,plain,iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_domain])).
% 2.99/3.18  cnf(c408,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X305)|iext(X305,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(resolution,[status(thm)],[c123, c26])).
% 2.99/3.18  fof(rdfs_annotation_isdefinedby_range,axiom,iext(uri_rdfs_range,uri_rdfs_isDefinedBy,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_isdefinedby_range)).
% 2.99/3.18  cnf(c122,plain,iext(uri_rdfs_range,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_range])).
% 2.99/3.18  cnf(c405,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X304)|iext(X304,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(resolution,[status(thm)],[c122, c26])).
% 2.99/3.18  fof(simple_ir,axiom,(![X]:ir(X)),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', simple_ir)).
% 2.99/3.18  fof(c146,plain,(![X42]:ir(X42)),inference(variable_rename,[status(thm)],[simple_ir])).
% 2.99/3.18  cnf(c147,plain,ir(X46),inference(split_conjunct,[status(thm)],[c146])).
% 2.99/3.18  fof(rdfs_ir_def,axiom,(![X]:(ir(X)<=>icext(uri_rdfs_Resource,X))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_ir_def)).
% 2.99/3.18  fof(c61,plain,(![X]:((~ir(X)|icext(uri_rdfs_Resource,X))&(~icext(uri_rdfs_Resource,X)|ir(X)))),inference(fof_nnf,[status(thm)],[rdfs_ir_def])).
% 2.99/3.18  fof(c62,plain,((![X]:(~ir(X)|icext(uri_rdfs_Resource,X)))&(![X]:(~icext(uri_rdfs_Resource,X)|ir(X)))),inference(shift_quantors,[status(thm)],[c61])).
% 2.99/3.18  fof(c64,plain,(![X24]:(![X25]:((~ir(X24)|icext(uri_rdfs_Resource,X24))&(~icext(uri_rdfs_Resource,X25)|ir(X25))))),inference(shift_quantors,[status(thm)],[fof(c63,plain,((![X24]:(~ir(X24)|icext(uri_rdfs_Resource,X24)))&(![X25]:(~icext(uri_rdfs_Resource,X25)|ir(X25)))),inference(variable_rename,[status(thm)],[c62])).])).
% 2.99/3.18  cnf(c65,plain,~ir(X58)|icext(uri_rdfs_Resource,X58),inference(split_conjunct,[status(thm)],[c64])).
% 2.99/3.18  cnf(c154,plain,icext(uri_rdfs_Resource,X59),inference(resolution,[status(thm)],[c65, c147])).
% 2.99/3.18  cnf(c386,plain,iext(uri_rdf_type,X93,uri_rdfs_Resource),inference(resolution,[status(thm)],[c116, c154])).
% 2.99/3.18  cnf(c401,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X300)|iext(X300,X299,uri_rdfs_Resource),inference(resolution,[status(thm)],[c386, c26])).
% 2.99/3.19  cnf(c409,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X298)|icext(X298,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c123, c78])).
% 2.99/3.19  cnf(c371,plain,~iext(uri_rdfs_subPropertyOf,X296,uri_rdfs_isDefinedBy)|iext(uri_rdfs_subPropertyOf,X296,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c121, c15])).
% 2.99/3.19  cnf(c406,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X295)|icext(X295,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c122, c78])).
% 2.99/3.19  cnf(c403,plain,~iext(uri_rdfs_range,uri_rdf_type,X294)|icext(X294,uri_rdfs_Resource),inference(resolution,[status(thm)],[c386, c52])).
% 2.99/3.19  cnf(c367,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X293)|iext(X293,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c121, c26])).
% 2.99/3.19  cnf(c370,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X292)|icext(X292,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c121, c52])).
% 2.99/3.19  cnf(c368,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X291)|icext(X291,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c121, c78])).
% 2.99/3.19  fof(rdfs_annotation_label_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_label,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_label_domain)).
% 2.99/3.19  cnf(c120,plain,iext(uri_rdfs_domain,uri_rdfs_label,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_label_domain])).
% 2.99/3.19  cnf(c364,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X289)|iext(X289,uri_rdfs_label,uri_rdfs_Resource),inference(resolution,[status(thm)],[c120, c26])).
% 2.99/3.19  cnf(c365,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X288)|icext(X288,uri_rdfs_label),inference(resolution,[status(thm)],[c120, c78])).
% 2.99/3.19  cnf(c363,plain,~iext(uri_rdfs_range,uri_rdfs_range,X287)|icext(X287,uri_rdfs_Literal),inference(resolution,[status(thm)],[c119, c52])).
% 2.99/3.19  cnf(c361,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X286)|iext(X286,uri_rdfs_label,uri_rdfs_Literal),inference(resolution,[status(thm)],[c119, c26])).
% 2.99/3.19  fof(rdfs_annotation_seealso_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_seeAlso,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_seealso_domain)).
% 2.99/3.19  cnf(c118,plain,iext(uri_rdfs_domain,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_seealso_domain])).
% 2.99/3.19  cnf(c358,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X285)|iext(X285,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(resolution,[status(thm)],[c118, c26])).
% 2.99/3.19  cnf(c359,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X282)|icext(X282,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c118, c78])).
% 2.99/3.19  fof(rdfs_annotation_seealso_range,axiom,iext(uri_rdfs_range,uri_rdfs_seeAlso,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_seealso_range)).
% 2.99/3.19  cnf(c117,plain,iext(uri_rdfs_range,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_seealso_range])).
% 2.99/3.19  cnf(c355,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X281)|iext(X281,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(resolution,[status(thm)],[c117, c26])).
% 2.99/3.19  cnf(c356,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X279)|icext(X279,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c117, c78])).
% 2.99/3.19  fof(rdfs_collection_first_domain,axiom,iext(uri_rdfs_domain,uri_rdf_first,uri_rdf_List),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_collection_first_domain)).
% 2.99/3.19  cnf(c107,plain,iext(uri_rdfs_domain,uri_rdf_first,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdfs_collection_first_domain])).
% 2.99/3.19  cnf(c342,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X277)|iext(X277,uri_rdf_first,uri_rdf_List),inference(resolution,[status(thm)],[c107, c26])).
% 2.99/3.19  cnf(c343,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X276)|icext(X276,uri_rdf_first),inference(resolution,[status(thm)],[c107, c78])).
% 2.99/3.19  fof(rdfs_collection_first_range,axiom,iext(uri_rdfs_range,uri_rdf_first,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_collection_first_range)).
% 2.99/3.19  cnf(c106,plain,iext(uri_rdfs_range,uri_rdf_first,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_collection_first_range])).
% 2.99/3.19  cnf(c339,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X274)|iext(X274,uri_rdf_first,uri_rdfs_Resource),inference(resolution,[status(thm)],[c106, c26])).
% 2.99/3.19  cnf(c340,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X273)|icext(X273,uri_rdf_first),inference(resolution,[status(thm)],[c106, c78])).
% 2.99/3.19  fof(rdfs_collection_rest_domain,axiom,iext(uri_rdfs_domain,uri_rdf_rest,uri_rdf_List),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_collection_rest_domain)).
% 2.99/3.19  cnf(c105,plain,iext(uri_rdfs_domain,uri_rdf_rest,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdfs_collection_rest_domain])).
% 2.99/3.19  cnf(c338,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X272)|icext(X272,uri_rdf_List),inference(resolution,[status(thm)],[c105, c52])).
% 2.99/3.19  cnf(c336,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X271)|iext(X271,uri_rdf_rest,uri_rdf_List),inference(resolution,[status(thm)],[c105, c26])).
% 2.99/3.19  cnf(c337,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X270)|icext(X270,uri_rdf_rest),inference(resolution,[status(thm)],[c105, c78])).
% 2.99/3.19  cnf(c332,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X267)|iext(X267,uri_rdf_rest,uri_rdf_List),inference(resolution,[status(thm)],[c104, c26])).
% 2.99/3.19  cnf(c329,plain,~iext(uri_rdfs_subClassOf,X266,uri_rdf_Alt)|iext(uri_rdfs_subClassOf,X266,uri_rdfs_Container),inference(resolution,[status(thm)],[c103, c30])).
% 2.99/3.19  cnf(c323,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X265)|iext(X265,uri_rdf_Alt,uri_rdfs_Container),inference(resolution,[status(thm)],[c103, c26])).
% 2.99/3.19  cnf(c319,plain,~iext(uri_rdfs_subClassOf,X264,uri_rdf_Bag)|iext(uri_rdfs_subClassOf,X264,uri_rdfs_Container),inference(resolution,[status(thm)],[c102, c30])).
% 2.99/3.19  cnf(c333,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X262)|icext(X262,uri_rdf_rest),inference(resolution,[status(thm)],[c104, c78])).
% 2.99/3.19  cnf(c313,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X261)|iext(X261,uri_rdf_Bag,uri_rdfs_Container),inference(resolution,[status(thm)],[c102, c26])).
% 2.99/3.19  cnf(c324,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X259)|icext(X259,uri_rdf_Alt),inference(resolution,[status(thm)],[c103, c78])).
% 2.99/3.19  cnf(c306,plain,~iext(uri_rdfs_subClassOf,X257,uri_rdfs_ContainerMembershipProperty)|iext(uri_rdfs_subClassOf,X257,uri_rdf_Property),inference(resolution,[status(thm)],[c98, c30])).
% 2.99/3.19  cnf(c314,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X256)|icext(X256,uri_rdf_Bag),inference(resolution,[status(thm)],[c102, c78])).
% 2.99/3.19  cnf(c305,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X255)|icext(X255,uri_rdf_Property),inference(resolution,[status(thm)],[c98, c52])).
% 2.99/3.19  cnf(c300,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X254)|iext(X254,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),inference(resolution,[status(thm)],[c98, c26])).
% 2.99/3.19  cnf(c301,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X253)|icext(X253,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c98, c78])).
% 2.99/3.19  fof(rdfs_reification_subject_domain,axiom,iext(uri_rdfs_domain,uri_rdf_subject,uri_rdfs_Statement),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_reification_subject_domain)).
% 2.99/3.19  cnf(c44,plain,iext(uri_rdfs_domain,uri_rdf_subject,uri_rdfs_Statement),inference(split_conjunct,[status(thm)],[rdfs_reification_subject_domain])).
% 2.99/3.19  cnf(c299,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X252)|icext(X252,uri_rdf_subject),inference(resolution,[status(thm)],[c78, c44])).
% 2.99/3.19  cnf(c298,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X251)|icext(X251,uri_rdf_type),inference(resolution,[status(thm)],[c78, c11])).
% 2.99/3.19  cnf(c296,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X249)|icext(X249,uri_rdfs_domain),inference(resolution,[status(thm)],[c78, c73])).
% 2.99/3.19  cnf(c295,plain,~iext(uri_rdfs_domain,uri_owl_equivalentClass,X248)|icext(X248,uri_ex_InversesOfFunctionalProperties),inference(resolution,[status(thm)],[c78, c2])).
% 2.99/3.19  fof(rdfs_value_range,axiom,iext(uri_rdfs_range,uri_rdf_value,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_value_range)).
% 2.99/3.19  cnf(c9,plain,iext(uri_rdfs_range,uri_rdf_value,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_value_range])).
% 2.99/3.19  cnf(c294,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X247)|icext(X247,uri_rdf_value),inference(resolution,[status(thm)],[c78, c9])).
% 2.99/3.19  cnf(c293,plain,~iext(uri_rdfs_domain,uri_owl_someValuesFrom,X246)|icext(X246,skolem0001),inference(resolution,[status(thm)],[c78, c5])).
% 2.99/3.19  cnf(c292,plain,~iext(uri_rdfs_domain,uri_owl_onProperty,X245)|icext(X245,skolem0001),inference(resolution,[status(thm)],[c78, c4])).
% 2.99/3.19  cnf(c291,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X244)|icext(X244,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c78, c85])).
% 2.99/3.19  fof(rdfs_reification_subject_range,axiom,iext(uri_rdfs_range,uri_rdf_subject,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_reification_subject_range)).
% 2.99/3.19  cnf(c43,plain,iext(uri_rdfs_range,uri_rdf_subject,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_reification_subject_range])).
% 2.99/3.19  cnf(c287,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X240)|icext(X240,uri_rdf_subject),inference(resolution,[status(thm)],[c78, c43])).
% 2.99/3.19  fof(rdfs_subclassof_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdfs_Class),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_subclassof_domain)).
% 2.99/3.19  cnf(c42,plain,iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_subclassof_domain])).
% 2.99/3.19  cnf(c286,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X239)|icext(X239,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c78, c42])).
% 2.99/3.19  fof(rdfs_subpropertyof_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_subpropertyof_domain)).
% 2.99/3.19  cnf(c27,plain,iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_subpropertyof_domain])).
% 2.99/3.19  cnf(c285,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X238)|icext(X238,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c78, c27])).
% 2.99/3.19  cnf(c284,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X237)|icext(X237,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c78, c80])).
% 2.99/3.19  fof(rdfs_subclassof_range,axiom,iext(uri_rdfs_range,uri_rdfs_subClassOf,uri_rdfs_Class),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_subclassof_range)).
% 2.99/3.19  cnf(c34,plain,iext(uri_rdfs_range,uri_rdfs_subClassOf,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_subclassof_range])).
% 2.99/3.19  cnf(c283,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X236)|icext(X236,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c78, c34])).
% 2.99/3.19  cnf(c282,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X235)|icext(X235,uri_rdfs_Seq),inference(resolution,[status(thm)],[c78, c86])).
% 2.99/3.19  fof(rdfs_container_n_domain_001,axiom,iext(uri_rdfs_domain,uri_rdf__1,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_domain_001)).
% 2.99/3.19  cnf(c95,plain,iext(uri_rdfs_domain,uri_rdf__1,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_001])).
% 2.99/3.19  cnf(c281,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X234)|icext(X234,uri_rdf__1),inference(resolution,[status(thm)],[c78, c95])).
% 2.99/3.19  fof(rdfs_subpropertyof_range,axiom,iext(uri_rdfs_range,uri_rdfs_subPropertyOf,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_subpropertyof_range)).
% 2.99/3.19  cnf(c19,plain,iext(uri_rdfs_range,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_subpropertyof_range])).
% 2.99/3.19  cnf(c280,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X233)|icext(X233,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c78, c19])).
% 2.99/3.19  cnf(c278,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X231)|icext(X231,uri_rdfs_range),inference(resolution,[status(thm)],[c78, c53])).
% 2.99/3.19  fof(rdfs_container_n_range_003,axiom,iext(uri_rdfs_range,uri_rdf__3,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_range_003)).
% 2.99/3.19  cnf(c90,plain,iext(uri_rdfs_range,uri_rdf__3,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_range_003])).
% 2.99/3.19  cnf(c277,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X230)|icext(X230,uri_rdf__3),inference(resolution,[status(thm)],[c78, c90])).
% 2.99/3.19  fof(rdfs_container_n_range_001,axiom,iext(uri_rdfs_range,uri_rdf__1,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_range_001)).
% 2.99/3.19  cnf(c92,plain,iext(uri_rdfs_range,uri_rdf__1,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_range_001])).
% 2.99/3.19  cnf(c276,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X229)|icext(X229,uri_rdf__1),inference(resolution,[status(thm)],[c78, c92])).
% 2.99/3.19  fof(rdfs_container_n_domain_002,axiom,iext(uri_rdfs_domain,uri_rdf__2,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_domain_002)).
% 2.99/3.19  cnf(c94,plain,iext(uri_rdfs_domain,uri_rdf__2,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_002])).
% 2.99/3.19  cnf(c275,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X228)|icext(X228,uri_rdf__2),inference(resolution,[status(thm)],[c78, c94])).
% 2.99/3.19  fof(rdfs_reification_predicate_domain,axiom,iext(uri_rdfs_domain,uri_rdf_predicate,uri_rdfs_Statement),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_reification_predicate_domain)).
% 2.99/3.19  cnf(c46,plain,iext(uri_rdfs_domain,uri_rdf_predicate,uri_rdfs_Statement),inference(split_conjunct,[status(thm)],[rdfs_reification_predicate_domain])).
% 2.99/3.19  cnf(c273,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X225)|icext(X225,uri_rdf_predicate),inference(resolution,[status(thm)],[c78, c46])).
% 2.99/3.19  cnf(c402,plain,~iext(uri_rdfs_domain,uri_rdf_type,X223)|icext(X223,X224),inference(resolution,[status(thm)],[c386, c78])).
% 2.99/3.19  fof(rdfs_container_member_range,axiom,iext(uri_rdfs_range,uri_rdfs_member,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_member_range)).
% 2.99/3.19  cnf(c96,plain,iext(uri_rdfs_range,uri_rdfs_member,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_member_range])).
% 2.99/3.19  cnf(c272,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X220)|icext(X220,uri_rdfs_member),inference(resolution,[status(thm)],[c78, c96])).
% 2.99/3.19  fof(rdfs_container_member_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_member,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_member_domain)).
% 2.99/3.19  cnf(c97,plain,iext(uri_rdfs_domain,uri_rdfs_member,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_member_domain])).
% 2.99/3.19  cnf(c271,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X219)|icext(X219,uri_rdfs_member),inference(resolution,[status(thm)],[c78, c97])).
% 2.99/3.19  cnf(c269,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X213)|icext(X213,uri_rdf_object),inference(resolution,[status(thm)],[c78, c48])).
% 2.99/3.19  fof(rdfs_container_n_range_002,axiom,iext(uri_rdfs_range,uri_rdf__2,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_range_002)).
% 2.99/3.19  cnf(c91,plain,iext(uri_rdfs_range,uri_rdf__2,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_range_002])).
% 2.99/3.19  cnf(c268,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X208)|icext(X208,uri_rdf__2),inference(resolution,[status(thm)],[c78, c91])).
% 2.99/3.19  fof(rdfs_type_domain,axiom,iext(uri_rdfs_domain,uri_rdf_type,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_type_domain)).
% 2.99/3.19  cnf(c12,plain,iext(uri_rdfs_domain,uri_rdf_type,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_type_domain])).
% 2.99/3.19  cnf(c266,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X198)|icext(X198,uri_rdf_type),inference(resolution,[status(thm)],[c78, c12])).
% 2.99/3.19  cnf(c265,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X193)|icext(X193,uri_rdfs_range),inference(resolution,[status(thm)],[c78, c49])).
% 2.99/3.19  cnf(c41,plain,~iext(uri_rdfs_subClassOf,X76,X75)|~icext(X76,X77)|icext(X75,X77),inference(split_conjunct,[status(thm)],[c38])).
% 2.99/3.19  cnf(c326,plain,~icext(uri_rdf_Alt,X189)|icext(uri_rdfs_Container,X189),inference(resolution,[status(thm)],[c103, c41])).
% 2.99/3.19  fof(rdfs_value_domain,axiom,iext(uri_rdfs_domain,uri_rdf_value,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_value_domain)).
% 2.99/3.19  cnf(c10,plain,iext(uri_rdfs_domain,uri_rdf_value,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_value_domain])).
% 2.99/3.19  cnf(c264,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X188)|icext(X188,uri_rdf_value),inference(resolution,[status(thm)],[c78, c10])).
% 2.99/3.19  cnf(c316,plain,~icext(uri_rdf_Bag,X187)|icext(uri_rdfs_Container,X187),inference(resolution,[status(thm)],[c102, c41])).
% 2.99/3.19  cnf(c263,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X186)|icext(X186,uri_rdf__3),inference(resolution,[status(thm)],[c78, c93])).
% 2.99/3.19  cnf(c303,plain,~icext(uri_rdfs_ContainerMembershipProperty,X185)|icext(uri_rdf_Property,X185),inference(resolution,[status(thm)],[c98, c41])).
% 2.99/3.19  cnf(c262,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X184)|icext(X184,uri_rdfs_domain),inference(factor,[status(thm)],[c78])).
% 2.99/3.19  cnf(c260,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X182)|iext(X182,uri_rdfs_member,uri_rdfs_Resource),inference(resolution,[status(thm)],[c97, c26])).
% 2.99/3.19  cnf(c258,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X180)|iext(X180,uri_rdfs_member,uri_rdfs_Resource),inference(resolution,[status(thm)],[c96, c26])).
% 2.99/3.19  cnf(c252,plain,~iext(uri_rdfs_range,uri_owl_equivalentClass,X175)|icext(X175,skolem0001),inference(resolution,[status(thm)],[c52, c2])).
% 2.99/3.19  cnf(c250,plain,~iext(uri_rdfs_range,uri_owl_someValuesFrom,X173)|icext(X173,uri_owl_FunctionalProperty),inference(resolution,[status(thm)],[c52, c5])).
% 2.99/3.19  cnf(c249,plain,~iext(uri_rdfs_range,uri_owl_onProperty,X172)|icext(X172,uri_owl_inverseOf),inference(resolution,[status(thm)],[c52, c4])).
% 2.99/3.19  cnf(c248,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X171)|icext(X171,uri_rdfs_Literal),inference(resolution,[status(thm)],[c52, c85])).
% 2.99/3.19  cnf(c1066,plain,icext(uri_rdf_Property,uri_rdfs_member),inference(resolution,[status(thm)],[c762, c115])).
% 2.99/3.19  fof(rdfs_dat_xmlliteral_type,axiom,iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Datatype),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_dat_xmlliteral_type)).
% 2.99/3.19  cnf(c84,plain,iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Datatype),inference(split_conjunct,[status(thm)],[rdfs_dat_xmlliteral_type])).
% 2.99/3.19  cnf(c245,plain,~iext(uri_rdfs_range,uri_rdf_type,X168)|icext(X168,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c52, c84])).
% 2.99/3.19  cnf(c243,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X166)|icext(X166,uri_rdfs_Class),inference(resolution,[status(thm)],[c52, c42])).
% 2.99/3.19  cnf(c1036,plain,icext(uri_rdf_Property,uri_owl_equivalentClass),inference(resolution,[status(thm)],[c572, c115])).
% 2.99/3.19  cnf(c241,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X164)|icext(X164,uri_rdfs_Class),inference(resolution,[status(thm)],[c52, c80])).
% 2.99/3.19  cnf(c1021,plain,icext(uri_rdf_Property,uri_owl_someValuesFrom),inference(resolution,[status(thm)],[c570, c115])).
% 2.99/3.19  cnf(c239,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X162)|icext(X162,uri_rdfs_Container),inference(resolution,[status(thm)],[c52, c86])).
% 2.99/3.19  cnf(c1005,plain,icext(uri_rdf_Property,uri_owl_onProperty),inference(resolution,[status(thm)],[c568, c115])).
% 2.99/3.19  cnf(c237,plain,~iext(uri_rdfs_range,uri_rdfs_range,X160)|icext(X160,uri_rdf_Property),inference(resolution,[status(thm)],[c52, c19])).
% 2.99/3.19  cnf(c989,plain,icext(uri_rdf_Property,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c566, c115])).
% 2.99/3.19  cnf(c235,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X158)|icext(X158,uri_rdf_Property),inference(resolution,[status(thm)],[c52, c53])).
% 2.99/3.19  cnf(c971,plain,icext(uri_rdf_Property,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c564, c115])).
% 2.99/3.19  cnf(c946,plain,icext(uri_rdf_Property,uri_rdfs_range),inference(resolution,[status(thm)],[c562, c115])).
% 2.99/3.19  cnf(c919,plain,icext(uri_rdf_Property,uri_rdfs_domain),inference(resolution,[status(thm)],[c560, c115])).
% 2.99/3.19  fof(rdfs_property_type,axiom,iext(uri_rdf_type,uri_rdf_Property,uri_rdfs_Class),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_property_type)).
% 2.99/3.19  cnf(c54,plain,iext(uri_rdf_type,uri_rdf_Property,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_property_type])).
% 2.99/3.19  cnf(c231,plain,~iext(uri_rdfs_range,uri_rdf_type,X154)|icext(X154,uri_rdfs_Class),inference(resolution,[status(thm)],[c52, c54])).
% 2.99/3.19  cnf(c227,plain,~iext(uri_rdfs_range,uri_rdfs_range,X150)|icext(X150,uri_rdfs_Resource),inference(resolution,[status(thm)],[c52, c91])).
% 2.99/3.19  cnf(c226,plain,~iext(uri_rdfs_range,uri_rdf_type,X149)|icext(X149,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c52, c89])).
% 2.99/3.19  cnf(c224,plain,~iext(uri_rdfs_range,uri_rdfs_range,X147)|icext(X147,uri_rdfs_Class),inference(resolution,[status(thm)],[c52, c49])).
% 2.99/3.19  cnf(c868,plain,icext(uri_rdf_Property,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c450, c115])).
% 2.99/3.19  cnf(c222,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X145)|icext(X145,uri_rdfs_Resource),inference(resolution,[status(thm)],[c52, c93])).
% 2.99/3.19  cnf(c859,plain,icext(uri_rdf_Property,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c447, c115])).
% 2.99/3.19  cnf(c221,plain,~iext(uri_rdfs_range,uri_rdfs_range,X144)|icext(X144,X144),inference(factor,[status(thm)],[c52])).
% 2.99/3.19  cnf(c217,plain,~icext(uri_rdf_XMLLiteral,X143)|icext(uri_rdfs_Literal,X143),inference(resolution,[status(thm)],[c41, c85])).
% 2.99/3.19  cnf(c216,plain,~icext(uri_rdfs_Datatype,X142)|icext(uri_rdfs_Class,X142),inference(resolution,[status(thm)],[c41, c80])).
% 2.99/3.19  cnf(c215,plain,~icext(uri_rdfs_Seq,X141)|icext(uri_rdfs_Container,X141),inference(resolution,[status(thm)],[c41, c86])).
% 2.99/3.19  cnf(c194,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X140)|iext(X140,uri_rdf__1,uri_rdfs_Resource),inference(resolution,[status(thm)],[c95, c26])).
% 2.99/3.19  cnf(c193,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X139)|iext(X139,uri_rdf__2,uri_rdfs_Resource),inference(resolution,[status(thm)],[c94, c26])).
% 2.99/3.19  cnf(c192,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X138)|iext(X138,uri_rdf__3,uri_rdfs_Resource),inference(resolution,[status(thm)],[c93, c26])).
% 2.99/3.19  cnf(c191,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X137)|iext(X137,uri_rdf__1,uri_rdfs_Resource),inference(resolution,[status(thm)],[c92, c26])).
% 2.99/3.19  cnf(c190,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X136)|iext(X136,uri_rdf__2,uri_rdfs_Resource),inference(resolution,[status(thm)],[c91, c26])).
% 2.99/3.19  cnf(c189,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X135)|iext(X135,uri_rdf__3,uri_rdfs_Resource),inference(resolution,[status(thm)],[c90, c26])).
% 2.99/3.19  cnf(c188,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X134)|iext(X134,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c89, c26])).
% 2.99/3.19  cnf(c187,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X133)|iext(X133,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c88, c26])).
% 2.99/3.19  cnf(c186,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X132)|iext(X132,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c87, c26])).
% 2.99/3.19  cnf(c185,plain,~iext(uri_rdfs_subClassOf,X131,uri_rdfs_Seq)|iext(uri_rdfs_subClassOf,X131,uri_rdfs_Container),inference(resolution,[status(thm)],[c86, c30])).
% 2.99/3.19  cnf(c184,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X130)|iext(X130,uri_rdfs_Seq,uri_rdfs_Container),inference(resolution,[status(thm)],[c86, c26])).
% 2.99/3.19  cnf(c183,plain,~iext(uri_rdfs_subClassOf,X129,uri_rdf_XMLLiteral)|iext(uri_rdfs_subClassOf,X129,uri_rdfs_Literal),inference(resolution,[status(thm)],[c30, c85])).
% 2.99/3.19  cnf(c182,plain,~iext(uri_rdfs_subClassOf,X128,uri_rdfs_Datatype)|iext(uri_rdfs_subClassOf,X128,uri_rdfs_Class),inference(resolution,[status(thm)],[c30, c80])).
% 2.99/3.19  cnf(c180,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X126)|iext(X126,uri_rdf_XMLLiteral,uri_rdfs_Literal),inference(resolution,[status(thm)],[c85, c26])).
% 2.99/3.19  cnf(c179,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X125)|iext(X125,uri_rdf_XMLLiteral,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c84, c26])).
% 2.99/3.19  cnf(c178,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X124)|iext(X124,uri_rdfs_Datatype,uri_rdfs_Class),inference(resolution,[status(thm)],[c80, c26])).
% 2.99/3.19  fof(rdfs_domain_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_domain_domain)).
% 2.99/3.19  cnf(c79,plain,iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_domain_domain])).
% 2.99/3.19  cnf(c177,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X123)|iext(X123,uri_rdfs_domain,uri_rdf_Property),inference(resolution,[status(thm)],[c79, c26])).
% 2.99/3.19  cnf(c176,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X122)|iext(X122,uri_rdfs_domain,uri_rdfs_Class),inference(resolution,[status(thm)],[c73, c26])).
% 2.99/3.19  cnf(c175,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X121)|iext(X121,uri_rdf_subject,uri_rdfs_Statement),inference(resolution,[status(thm)],[c26, c44])).
% 2.99/3.19  cnf(c174,plain,~iext(uri_rdfs_subPropertyOf,uri_owl_onProperty,X120)|iext(X120,skolem0001,uri_owl_inverseOf),inference(resolution,[status(thm)],[c26, c4])).
% 2.99/3.19  cnf(c173,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X119)|iext(X119,uri_rdf_type,uri_rdfs_Class),inference(resolution,[status(thm)],[c26, c11])).
% 2.99/3.19  cnf(c172,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X118)|iext(X118,uri_rdfs_subClassOf,uri_rdfs_Class),inference(resolution,[status(thm)],[c26, c34])).
% 2.99/3.19  cnf(c171,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X117)|iext(X117,uri_rdf_Property,uri_rdfs_Class),inference(resolution,[status(thm)],[c26, c54])).
% 2.99/3.19  cnf(c170,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X116)|iext(X116,uri_rdf_predicate,uri_rdfs_Statement),inference(resolution,[status(thm)],[c26, c46])).
% 2.99/3.19  cnf(c169,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X115)|iext(X115,skolem0001,uri_owl_Restriction),inference(resolution,[status(thm)],[c26, c3])).
% 2.99/3.19  cnf(c168,plain,~iext(uri_rdfs_subPropertyOf,uri_owl_equivalentClass,X114)|iext(X114,uri_ex_InversesOfFunctionalProperties,skolem0001),inference(resolution,[status(thm)],[c26, c2])).
% 2.99/3.19  cnf(c167,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X113)|iext(X113,uri_rdf_object,uri_rdfs_Statement),inference(resolution,[status(thm)],[c26, c48])).
% 2.99/3.19  cnf(c166,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X112)|iext(X112,uri_rdf_predicate,uri_rdfs_Resource),inference(resolution,[status(thm)],[c26, c45])).
% 2.99/3.19  cnf(c165,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X111)|iext(X111,uri_rdf_subject,uri_rdfs_Resource),inference(resolution,[status(thm)],[c26, c43])).
% 2.99/3.19  cnf(c164,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X110)|iext(X110,uri_rdfs_range,uri_rdfs_Class),inference(resolution,[status(thm)],[c26, c49])).
% 2.99/3.19  cnf(c163,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X109)|iext(X109,uri_rdfs_subClassOf,uri_rdfs_Class),inference(resolution,[status(thm)],[c26, c42])).
% 2.99/3.19  cnf(c162,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X108)|iext(X108,uri_rdf_type,uri_rdfs_Resource),inference(resolution,[status(thm)],[c26, c12])).
% 2.99/3.19  cnf(c161,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X107)|iext(X107,uri_rdf_value,uri_rdfs_Resource),inference(resolution,[status(thm)],[c26, c9])).
% 2.99/3.19  cnf(c160,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X106)|iext(X106,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c26, c19])).
% 2.99/3.19  cnf(c159,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X105)|iext(X105,uri_rdf_value,uri_rdfs_Resource),inference(resolution,[status(thm)],[c26, c10])).
% 2.99/3.19  cnf(c158,plain,~iext(uri_rdfs_subPropertyOf,uri_owl_someValuesFrom,X104)|iext(X104,skolem0001,uri_owl_FunctionalProperty),inference(resolution,[status(thm)],[c26, c5])).
% 2.99/3.19  cnf(c157,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X103)|iext(X103,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c26, c27])).
% 2.99/3.19  cnf(c156,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X102)|iext(X102,uri_rdfs_range,uri_rdf_Property),inference(resolution,[status(thm)],[c26, c53])).
% 2.99/3.19  cnf(c155,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X101)|iext(X101,uri_rdfs_subPropertyOf,X101),inference(factor,[status(thm)],[c26])).
% 2.99/3.19  cnf(c492,plain,icext(uri_rdf_Property,uri_rdf_first),inference(resolution,[status(thm)],[c142, c115])).
% 2.99/3.19  cnf(c485,plain,icext(uri_rdf_List,uri_rdf_nil),inference(resolution,[status(thm)],[c141, c115])).
% 2.99/3.19  cnf(c479,plain,icext(uri_rdf_Property,uri_rdf_rest),inference(resolution,[status(thm)],[c140, c115])).
% 2.99/3.19  cnf(c470,plain,icext(uri_rdf_Property,uri_rdf__1),inference(resolution,[status(thm)],[c139, c115])).
% 2.99/3.19  cnf(c463,plain,icext(uri_rdf_Property,uri_rdf__2),inference(resolution,[status(thm)],[c138, c115])).
% 2.99/3.19  cnf(c455,plain,icext(uri_rdf_Property,uri_rdf__3),inference(resolution,[status(thm)],[c137, c115])).
% 2.99/3.19  cnf(c435,plain,icext(uri_rdf_Property,uri_rdf_object),inference(resolution,[status(thm)],[c136, c115])).
% 2.99/3.19  cnf(c430,plain,icext(uri_rdf_Property,uri_rdf_value),inference(resolution,[status(thm)],[c135, c115])).
% 2.99/3.19  cnf(c425,plain,icext(uri_rdf_Property,uri_rdf_subject),inference(resolution,[status(thm)],[c134, c115])).
% 2.99/3.19  cnf(c420,plain,icext(uri_rdf_Property,uri_rdf_type),inference(resolution,[status(thm)],[c126, c115])).
% 2.99/3.19  cnf(c377,plain,icext(uri_owl_Restriction,skolem0001),inference(resolution,[status(thm)],[c115, c3])).
% 2.99/3.19  cnf(c375,plain,icext(uri_rdfs_Datatype,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c115, c84])).
% 2.99/3.19  fof(rdfs_datatype_instsub_literal,axiom,(![D]:(icext(uri_rdfs_Datatype,D)=>iext(uri_rdfs_subClassOf,D,uri_rdfs_Literal))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_datatype_instsub_literal)).
% 2.99/3.19  fof(c81,plain,(![D]:(~icext(uri_rdfs_Datatype,D)|iext(uri_rdfs_subClassOf,D,uri_rdfs_Literal))),inference(fof_nnf,[status(thm)],[rdfs_datatype_instsub_literal])).
% 2.99/3.19  fof(c82,plain,(![X32]:(~icext(uri_rdfs_Datatype,X32)|iext(uri_rdfs_subClassOf,X32,uri_rdfs_Literal))),inference(variable_rename,[status(thm)],[c81])).
% 2.99/3.19  cnf(c83,plain,~icext(uri_rdfs_Datatype,X86)|iext(uri_rdfs_subClassOf,X86,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[c82])).
% 2.99/3.19  cnf(c307,plain,icext(uri_rdfs_Class,uri_rdf_Property),inference(resolution,[status(thm)],[c302, c71])).
% 2.99/3.19  fof(rdfs_lv_def,axiom,(![X]:(lv(X)<=>icext(uri_rdfs_Literal,X))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_lv_def)).
% 2.99/3.19  fof(c55,plain,(![X]:((~lv(X)|icext(uri_rdfs_Literal,X))&(~icext(uri_rdfs_Literal,X)|lv(X)))),inference(fof_nnf,[status(thm)],[rdfs_lv_def])).
% 2.99/3.19  fof(c56,plain,((![X]:(~lv(X)|icext(uri_rdfs_Literal,X)))&(![X]:(~icext(uri_rdfs_Literal,X)|lv(X)))),inference(shift_quantors,[status(thm)],[c55])).
% 2.99/3.19  fof(c58,plain,(![X22]:(![X23]:((~lv(X22)|icext(uri_rdfs_Literal,X22))&(~icext(uri_rdfs_Literal,X23)|lv(X23))))),inference(shift_quantors,[status(thm)],[fof(c57,plain,((![X22]:(~lv(X22)|icext(uri_rdfs_Literal,X22)))&(![X23]:(~icext(uri_rdfs_Literal,X23)|lv(X23)))),inference(variable_rename,[status(thm)],[c56])).])).
% 2.99/3.19  cnf(c60,plain,~icext(uri_rdfs_Literal,X55)|lv(X55),inference(split_conjunct,[status(thm)],[c58])).
% 2.99/3.19  cnf(c59,plain,~lv(X54)|icext(uri_rdfs_Literal,X54),inference(split_conjunct,[status(thm)],[c58])).
% 2.99/3.19  fof(testcase_conclusion_fullish_028_Inferred_Property_Characteristics_III,conjecture,iext(uri_rdfs_subClassOf,uri_ex_InversesOfFunctionalProperties,uri_owl_InverseFunctionalProperty),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', testcase_conclusion_fullish_028_Inferred_Property_Characteristics_III)).
% 2.99/3.19  fof(c6,negated_conjecture,(~iext(uri_rdfs_subClassOf,uri_ex_InversesOfFunctionalProperties,uri_owl_InverseFunctionalProperty)),inference(assume_negation,[status(cth)],[testcase_conclusion_fullish_028_Inferred_Property_Characteristics_III])).
% 2.99/3.19  fof(c7,negated_conjecture,~iext(uri_rdfs_subClassOf,uri_ex_InversesOfFunctionalProperties,uri_owl_InverseFunctionalProperty),inference(fof_simplification,[status(thm)],[c6])).
% 2.99/3.19  cnf(c8,negated_conjecture,~iext(uri_rdfs_subClassOf,uri_ex_InversesOfFunctionalProperties,uri_owl_InverseFunctionalProperty),inference(split_conjunct,[status(thm)],[c7])).
% 2.99/3.19  % SZS output end Saturation
% 2.99/3.19  
% 2.99/3.19  % Initial clauses    : 94
% 2.99/3.19  % Processed clauses  : 555
% 2.99/3.19  % Factors computed   : 5
% 2.99/3.19  % Resolvents computed: 1296
% 2.99/3.19  % Tautologies deleted: 52
% 2.99/3.19  % Forward subsumed   : 788
% 2.99/3.19  % Backward subsumed  : 2
% 2.99/3.19  % -------- CPU Time ---------
% 2.99/3.19  % User time          : 2.831 s
% 2.99/3.19  % System time        : 0.015 s
% 2.99/3.19  % Total time         : 2.846 s
%------------------------------------------------------------------------------