PyRes---1.5.CSA-Sat.s

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

% Computer : n018.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:45 EDT 2024

% Result   : CounterSatisfiable 2.68s 2.89s
% Output   : Saturation 2.73s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12  % Problem  : SWB005+4 : TPTP v8.1.2. Released v5.2.0.
% 0.03/0.13  % Command  : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35  % Computer : n018.cluster.edu
% 0.13/0.35  % Model    : x86_64 x86_64
% 0.13/0.35  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35  % Memory   : 8042.1875MB
% 0.13/0.35  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35  % CPULimit : 300
% 0.13/0.35  % WCLimit  : 300
% 0.13/0.35  % DateTime : Wed May  8 22:07:23 EDT 2024
% 0.13/0.35  % CPUTime  : 
% 2.68/2.89  % Version:  1.5
% 2.68/2.89  % SZS status CounterSatisfiable
% 2.68/2.89  % SZS output start Saturation
% 2.68/2.89  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.68/2.89  fof(c15,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.68/2.89  fof(c17,plain,(![X6]:(![X7]:(![X8]:(![X9]:(~iext(uri_rdfs_subPropertyOf,X6,X7)|((ip(X6)&ip(X7))&(~iext(X6,X8,X9)|iext(X7,X8,X9)))))))),inference(shift_quantors,[status(thm)],[fof(c16,plain,(![X6]:(![X7]:(~iext(uri_rdfs_subPropertyOf,X6,X7)|((ip(X6)&ip(X7))&(![X8]:(![X9]:(~iext(X6,X8,X9)|iext(X7,X8,X9)))))))),inference(variable_rename,[status(thm)],[c15])).])).
% 2.68/2.89  fof(c18,plain,(![X6]:(![X7]:(![X8]:(![X9]:(((~iext(uri_rdfs_subPropertyOf,X6,X7)|ip(X6))&(~iext(uri_rdfs_subPropertyOf,X6,X7)|ip(X7)))&(~iext(uri_rdfs_subPropertyOf,X6,X7)|(~iext(X6,X8,X9)|iext(X7,X8,X9)))))))),inference(distribute,[status(thm)],[c17])).
% 2.68/2.89  cnf(c21,plain,~iext(uri_rdfs_subPropertyOf,X62,X63)|~iext(X62,X64,X65)|iext(X63,X64,X65),inference(split_conjunct,[status(thm)],[c18])).
% 2.68/2.89  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.68/2.89  fof(c11,plain,(![P]:(~ip(P)|iext(uri_rdfs_subPropertyOf,P,P))),inference(fof_nnf,[status(thm)],[rdfs_subpropertyof_reflex])).
% 2.68/2.89  fof(c12,plain,(![X5]:(~ip(X5)|iext(uri_rdfs_subPropertyOf,X5,X5))),inference(variable_rename,[status(thm)],[c11])).
% 2.68/2.89  cnf(c13,plain,~ip(X50)|iext(uri_rdfs_subPropertyOf,X50,X50),inference(split_conjunct,[status(thm)],[c12])).
% 2.68/2.89  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.68/2.89  fof(c123,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.68/2.89  fof(c124,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)],[c123])).
% 2.68/2.89  fof(c126,plain,(![X38]:(![X39]:((~iext(uri_rdf_type,X38,uri_rdf_Property)|ip(X38))&(~ip(X39)|iext(uri_rdf_type,X39,uri_rdf_Property))))),inference(shift_quantors,[status(thm)],[fof(c125,plain,((![X38]:(~iext(uri_rdf_type,X38,uri_rdf_Property)|ip(X38)))&(![X39]:(~ip(X39)|iext(uri_rdf_type,X39,uri_rdf_Property)))),inference(variable_rename,[status(thm)],[c124])).])).
% 2.68/2.89  cnf(c127,plain,~iext(uri_rdf_type,X94,uri_rdf_Property)|ip(X94),inference(split_conjunct,[status(thm)],[c126])).
% 2.68/2.89  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.68/2.89  fof(c106,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.68/2.89  fof(c107,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)],[c106])).
% 2.68/2.89  fof(c109,plain,(![X34]:(![X35]:(![X36]:(![X37]:((~iext(uri_rdf_type,X34,X35)|icext(X35,X34))&(~icext(X37,X36)|iext(uri_rdf_type,X36,X37))))))),inference(shift_quantors,[status(thm)],[fof(c108,plain,((![X34]:(![X35]:(~iext(uri_rdf_type,X34,X35)|icext(X35,X34))))&(![X36]:(![X37]:(~icext(X37,X36)|iext(uri_rdf_type,X36,X37))))),inference(variable_rename,[status(thm)],[c107])).])).
% 2.68/2.89  cnf(c111,plain,~icext(X91,X90)|iext(uri_rdf_type,X90,X91),inference(split_conjunct,[status(thm)],[c109])).
% 2.68/2.89  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.68/2.89  cnf(c48,plain,iext(uri_rdfs_domain,uri_rdfs_range,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_range_domain])).
% 2.68/2.89  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.68/2.89  fof(c69,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.68/2.89  fof(c70,plain,(![P]:(![C]:(![X]:((~iext(uri_rdfs_domain,P,C)|(![Y]:~iext(P,X,Y)))|icext(C,X))))),inference(shift_quantors,[status(thm)],[c69])).
% 2.68/2.89  fof(c72,plain,(![X27]:(![X28]:(![X29]:(![X30]:((~iext(uri_rdfs_domain,X27,X28)|~iext(X27,X29,X30))|icext(X28,X29)))))),inference(shift_quantors,[status(thm)],[fof(c71,plain,(![X27]:(![X28]:(![X29]:((~iext(uri_rdfs_domain,X27,X28)|(![X30]:~iext(X27,X29,X30)))|icext(X28,X29))))),inference(variable_rename,[status(thm)],[c70])).])).
% 2.68/2.89  cnf(c73,plain,~iext(uri_rdfs_domain,X81,X84)|~iext(X81,X82,X83)|icext(X84,X82),inference(split_conjunct,[status(thm)],[c72])).
% 2.68/2.89  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.68/2.89  cnf(c119,plain,iext(uri_rdfs_range,uri_rdfs_comment,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[rdfs_annotation_comment_range])).
% 2.68/2.89  cnf(c397,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X290)|icext(X290,uri_rdfs_comment),inference(resolution,[status(thm)],[c119, c73])).
% 2.68/2.89  cnf(c1178,plain,icext(uri_rdf_Property,uri_rdfs_comment),inference(resolution,[status(thm)],[c397, c48])).
% 2.68/2.89  cnf(c1179,plain,iext(uri_rdf_type,uri_rdfs_comment,uri_rdf_Property),inference(resolution,[status(thm)],[c1178, c111])).
% 2.68/2.89  cnf(c1181,plain,ip(uri_rdfs_comment),inference(resolution,[status(thm)],[c1179, c127])).
% 2.68/2.89  cnf(c1188,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_comment,uri_rdfs_comment),inference(resolution,[status(thm)],[c1181, c13])).
% 2.68/2.89  cnf(c1192,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X589)|iext(X589,uri_rdfs_comment,uri_rdfs_comment),inference(resolution,[status(thm)],[c1188, c21])).
% 2.68/2.89  cnf(c1182,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X587)|iext(X587,uri_rdfs_comment,uri_rdf_Property),inference(resolution,[status(thm)],[c1179, c21])).
% 2.68/2.89  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.68/2.89  cnf(c114,plain,iext(uri_rdfs_range,uri_rdfs_label,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[rdfs_annotation_label_range])).
% 2.68/2.89  cnf(c339,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X274)|icext(X274,uri_rdfs_label),inference(resolution,[status(thm)],[c114, c73])).
% 2.68/2.89  cnf(c1150,plain,icext(uri_rdf_Property,uri_rdfs_label),inference(resolution,[status(thm)],[c339, c48])).
% 2.68/2.89  cnf(c1151,plain,iext(uri_rdf_type,uri_rdfs_label,uri_rdf_Property),inference(resolution,[status(thm)],[c1150, c111])).
% 2.68/2.89  cnf(c1153,plain,ip(uri_rdfs_label),inference(resolution,[status(thm)],[c1151, c127])).
% 2.68/2.89  cnf(c1159,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_label,uri_rdfs_label),inference(resolution,[status(thm)],[c1153, c13])).
% 2.68/2.89  cnf(c1163,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X586)|iext(X586,uri_rdfs_label,uri_rdfs_label),inference(resolution,[status(thm)],[c1159, c21])).
% 2.68/2.89  cnf(c1154,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X584)|iext(X584,uri_rdfs_label,uri_rdf_Property),inference(resolution,[status(thm)],[c1151, c21])).
% 2.68/2.89  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.68/2.89  fof(c26,plain,(![C]:(~ic(C)|iext(uri_rdfs_subClassOf,C,C))),inference(fof_nnf,[status(thm)],[rdfs_subclassof_reflex])).
% 2.68/2.89  fof(c27,plain,(![X13]:(~ic(X13)|iext(uri_rdfs_subClassOf,X13,X13))),inference(variable_rename,[status(thm)],[c26])).
% 2.68/2.89  cnf(c28,plain,~ic(X69)|iext(uri_rdfs_subClassOf,X69,X69),inference(split_conjunct,[status(thm)],[c27])).
% 2.68/2.89  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.68/2.89  fof(c62,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.68/2.89  fof(c63,plain,((![X]:(~ic(X)|icext(uri_rdfs_Class,X)))&(![X]:(~icext(uri_rdfs_Class,X)|ic(X)))),inference(shift_quantors,[status(thm)],[c62])).
% 2.68/2.89  fof(c65,plain,(![X25]:(![X26]:((~ic(X25)|icext(uri_rdfs_Class,X25))&(~icext(uri_rdfs_Class,X26)|ic(X26))))),inference(shift_quantors,[status(thm)],[fof(c64,plain,((![X25]:(~ic(X25)|icext(uri_rdfs_Class,X25)))&(![X26]:(~icext(uri_rdfs_Class,X26)|ic(X26)))),inference(variable_rename,[status(thm)],[c63])).])).
% 2.68/2.89  cnf(c67,plain,~icext(uri_rdfs_Class,X61)|ic(X61),inference(split_conjunct,[status(thm)],[c65])).
% 2.68/2.89  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.68/2.89  cnf(c44,plain,iext(uri_rdfs_range,uri_rdfs_range,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_range_range])).
% 2.68/2.89  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.73/2.89  fof(c45,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.73/2.89  fof(c46,plain,(![X17]:(![X18]:(![X19]:(![X20]:((~iext(uri_rdfs_range,X17,X18)|~iext(X17,X19,X20))|icext(X18,X20)))))),inference(variable_rename,[status(thm)],[c45])).
% 2.73/2.89  cnf(c47,plain,~iext(uri_rdfs_range,X78,X79)|~iext(X78,X77,X80)|icext(X79,X80),inference(split_conjunct,[status(thm)],[c46])).
% 2.73/2.89  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.73/2.89  cnf(c99,plain,iext(uri_rdfs_range,uri_rdf_rest,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdfs_collection_rest_range])).
% 2.73/2.89  cnf(c319,plain,~iext(uri_rdfs_range,uri_rdfs_range,X251)|icext(X251,uri_rdf_List),inference(resolution,[status(thm)],[c99, c47])).
% 2.73/2.89  cnf(c1107,plain,icext(uri_rdfs_Class,uri_rdf_List),inference(resolution,[status(thm)],[c319, c44])).
% 2.73/2.89  cnf(c1108,plain,ic(uri_rdf_List),inference(resolution,[status(thm)],[c1107, c67])).
% 2.73/2.89  cnf(c1112,plain,iext(uri_rdfs_subClassOf,uri_rdf_List,uri_rdf_List),inference(resolution,[status(thm)],[c1108, c28])).
% 2.73/2.89  cnf(c1130,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X582)|iext(X582,uri_rdf_List,uri_rdf_List),inference(resolution,[status(thm)],[c1112, c21])).
% 2.73/2.89  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.73/2.89  fof(c23,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.73/2.89  fof(c24,plain,(![X10]:(![X11]:(![X12]:((~iext(uri_rdfs_subClassOf,X10,X11)|~iext(uri_rdfs_subClassOf,X11,X12))|iext(uri_rdfs_subClassOf,X10,X12))))),inference(variable_rename,[status(thm)],[c23])).
% 2.73/2.89  cnf(c25,plain,~iext(uri_rdfs_subClassOf,X66,X68)|~iext(uri_rdfs_subClassOf,X68,X67)|iext(uri_rdfs_subClassOf,X66,X67),inference(split_conjunct,[status(thm)],[c24])).
% 2.73/2.89  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.73/2.89  fof(c103,plain,(![C]:(~ic(C)|iext(uri_rdfs_subClassOf,C,uri_rdfs_Resource))),inference(fof_nnf,[status(thm)],[rdfs_class_instsub_resource])).
% 2.73/2.89  fof(c104,plain,(![X33]:(~ic(X33)|iext(uri_rdfs_subClassOf,X33,uri_rdfs_Resource))),inference(variable_rename,[status(thm)],[c103])).
% 2.73/2.89  cnf(c105,plain,~ic(X87)|iext(uri_rdfs_subClassOf,X87,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[c104])).
% 2.73/2.89  cnf(c1111,plain,iext(uri_rdfs_subClassOf,uri_rdf_List,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1108, c105])).
% 2.73/2.89  cnf(c1124,plain,~iext(uri_rdfs_subClassOf,X581,uri_rdf_List)|iext(uri_rdfs_subClassOf,X581,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1111, c25])).
% 2.73/2.89  cnf(c1121,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X580)|iext(X580,uri_rdf_List,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1111, c21])).
% 2.73/2.89  cnf(c1109,plain,iext(uri_rdf_type,uri_rdf_List,uri_rdfs_Class),inference(resolution,[status(thm)],[c1107, c111])).
% 2.73/2.89  cnf(c1115,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X579)|iext(X579,uri_rdf_List,uri_rdfs_Class),inference(resolution,[status(thm)],[c1109, c21])).
% 2.73/2.89  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.73/2.89  cnf(c40,plain,iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_reification_predicate_range])).
% 2.73/2.89  cnf(c272,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X220)|icext(X220,uri_rdf_predicate),inference(resolution,[status(thm)],[c73, c40])).
% 2.73/2.89  cnf(c1068,plain,icext(uri_rdf_Property,uri_rdf_predicate),inference(resolution,[status(thm)],[c272, c48])).
% 2.73/2.89  cnf(c1069,plain,iext(uri_rdf_type,uri_rdf_predicate,uri_rdf_Property),inference(resolution,[status(thm)],[c1068, c111])).
% 2.73/2.89  cnf(c1074,plain,ip(uri_rdf_predicate),inference(resolution,[status(thm)],[c1069, c127])).
% 2.73/2.89  cnf(c1077,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_predicate,uri_rdf_predicate),inference(resolution,[status(thm)],[c1074, c13])).
% 2.73/2.89  cnf(c1081,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X578)|iext(X578,uri_rdf_predicate,uri_rdf_predicate),inference(resolution,[status(thm)],[c1077, c21])).
% 2.73/2.89  cnf(c1070,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X576)|iext(X576,uri_rdf_predicate,uri_rdf_Property),inference(resolution,[status(thm)],[c1069, c21])).
% 2.73/2.89  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.73/2.89  cnf(c68,plain,iext(uri_rdfs_range,uri_rdfs_domain,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_domain_range])).
% 2.73/2.89  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.73/2.89  cnf(c43,plain,iext(uri_rdfs_domain,uri_rdf_object,uri_rdfs_Statement),inference(split_conjunct,[status(thm)],[rdfs_reification_object_domain])).
% 2.73/2.89  cnf(c235,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X157)|icext(X157,uri_rdfs_Statement),inference(resolution,[status(thm)],[c47, c43])).
% 2.73/2.89  cnf(c967,plain,icext(uri_rdfs_Class,uri_rdfs_Statement),inference(resolution,[status(thm)],[c235, c68])).
% 2.73/2.89  cnf(c968,plain,ic(uri_rdfs_Statement),inference(resolution,[status(thm)],[c967, c67])).
% 2.73/2.89  cnf(c972,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Statement,uri_rdfs_Statement),inference(resolution,[status(thm)],[c968, c28])).
% 2.73/2.89  cnf(c1052,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X575)|iext(X575,uri_rdfs_Statement,uri_rdfs_Statement),inference(resolution,[status(thm)],[c972, c21])).
% 2.73/2.89  cnf(c971,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Statement,uri_rdfs_Resource),inference(resolution,[status(thm)],[c968, c105])).
% 2.73/2.89  cnf(c1044,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X573)|iext(X573,uri_rdfs_Statement,uri_rdfs_Resource),inference(resolution,[status(thm)],[c971, c21])).
% 2.73/2.89  cnf(c1043,plain,~iext(uri_rdfs_subClassOf,X572,uri_rdfs_Statement)|iext(uri_rdfs_subClassOf,X572,uri_rdfs_Resource),inference(resolution,[status(thm)],[c971, c25])).
% 2.73/2.89  cnf(c969,plain,iext(uri_rdf_type,uri_rdfs_Statement,uri_rdfs_Class),inference(resolution,[status(thm)],[c967, c111])).
% 2.73/2.89  cnf(c1035,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X571)|iext(X571,uri_rdfs_Statement,uri_rdfs_Class),inference(resolution,[status(thm)],[c969, c21])).
% 2.73/2.89  cnf(c20,plain,~iext(uri_rdfs_subPropertyOf,X58,X59)|ip(X59),inference(split_conjunct,[status(thm)],[c18])).
% 2.73/2.89  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.73/2.89  fof(c94,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.73/2.90  fof(c95,plain,(![X32]:(~icext(uri_rdfs_ContainerMembershipProperty,X32)|iext(uri_rdfs_subPropertyOf,X32,uri_rdfs_member))),inference(variable_rename,[status(thm)],[c94])).
% 2.73/2.90  cnf(c96,plain,~icext(uri_rdfs_ContainerMembershipProperty,X86)|iext(uri_rdfs_subPropertyOf,X86,uri_rdfs_member),inference(split_conjunct,[status(thm)],[c95])).
% 2.73/2.90  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.73/2.90  cnf(c84,plain,iext(uri_rdf_type,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),inference(split_conjunct,[status(thm)],[rdfs_container_n_type_001])).
% 2.73/2.90  cnf(c110,plain,~iext(uri_rdf_type,X89,X88)|icext(X88,X89),inference(split_conjunct,[status(thm)],[c109])).
% 2.73/2.90  cnf(c364,plain,icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__1),inference(resolution,[status(thm)],[c110, c84])).
% 2.73/2.90  cnf(c369,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__1,uri_rdfs_member),inference(resolution,[status(thm)],[c364, c96])).
% 2.73/2.90  cnf(c732,plain,ip(uri_rdfs_member),inference(resolution,[status(thm)],[c369, c20])).
% 2.73/2.90  cnf(c740,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_member,uri_rdfs_member),inference(resolution,[status(thm)],[c732, c13])).
% 2.73/2.90  cnf(c1027,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X570)|iext(X570,uri_rdfs_member,uri_rdfs_member),inference(resolution,[status(thm)],[c740, c21])).
% 2.73/2.90  cnf(c128,plain,~ip(X95)|iext(uri_rdf_type,X95,uri_rdf_Property),inference(split_conjunct,[status(thm)],[c126])).
% 2.73/2.90  cnf(c739,plain,iext(uri_rdf_type,uri_rdfs_member,uri_rdf_Property),inference(resolution,[status(thm)],[c732, c128])).
% 2.73/2.90  cnf(c1018,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X568)|iext(X568,uri_rdfs_member,uri_rdf_Property),inference(resolution,[status(thm)],[c739, c21])).
% 2.73/2.90  cnf(c66,plain,~ic(X60)|icext(uri_rdfs_Class,X60),inference(split_conjunct,[status(thm)],[c65])).
% 2.73/2.90  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.73/2.90  fof(c30,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.73/2.90  fof(c32,plain,(![X14]:(![X15]:(![X16]:(~iext(uri_rdfs_subClassOf,X14,X15)|((ic(X14)&ic(X15))&(~icext(X14,X16)|icext(X15,X16))))))),inference(shift_quantors,[status(thm)],[fof(c31,plain,(![X14]:(![X15]:(~iext(uri_rdfs_subClassOf,X14,X15)|((ic(X14)&ic(X15))&(![X16]:(~icext(X14,X16)|icext(X15,X16))))))),inference(variable_rename,[status(thm)],[c30])).])).
% 2.73/2.90  fof(c33,plain,(![X14]:(![X15]:(![X16]:(((~iext(uri_rdfs_subClassOf,X14,X15)|ic(X14))&(~iext(uri_rdfs_subClassOf,X14,X15)|ic(X15)))&(~iext(uri_rdfs_subClassOf,X14,X15)|(~icext(X14,X16)|icext(X15,X16))))))),inference(distribute,[status(thm)],[c32])).
% 2.73/2.90  cnf(c35,plain,~iext(uri_rdfs_subClassOf,X73,X72)|ic(X72),inference(split_conjunct,[status(thm)],[c33])).
% 2.73/2.90  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.73/2.90  cnf(c75,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_datatype_sub])).
% 2.73/2.90  cnf(c34,plain,~iext(uri_rdfs_subClassOf,X71,X70)|ic(X71),inference(split_conjunct,[status(thm)],[c33])).
% 2.73/2.90  cnf(c194,plain,ic(uri_rdfs_Datatype),inference(resolution,[status(thm)],[c34, c75])).
% 2.73/2.90  cnf(c340,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Resource),inference(resolution,[status(thm)],[c105, c194])).
% 2.73/2.90  cnf(c631,plain,ic(uri_rdfs_Resource),inference(resolution,[status(thm)],[c340, c35])).
% 2.73/2.90  cnf(c639,plain,icext(uri_rdfs_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c631, c66])).
% 2.73/2.90  cnf(c643,plain,iext(uri_rdf_type,uri_rdfs_Resource,uri_rdfs_Class),inference(resolution,[status(thm)],[c639, c111])).
% 2.73/2.90  cnf(c1013,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X567)|iext(X567,uri_rdfs_Resource,uri_rdfs_Class),inference(resolution,[status(thm)],[c643, c21])).
% 2.73/2.90  cnf(c640,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Resource,uri_rdfs_Resource),inference(resolution,[status(thm)],[c631, c105])).
% 2.73/2.90  cnf(c1009,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X566)|iext(X566,uri_rdfs_Resource,uri_rdfs_Resource),inference(resolution,[status(thm)],[c640, c21])).
% 2.73/2.90  fof(testcase_premise_fullish_005_Everything_is_a_Resource,axiom,iext(uri_ex_p,uri_ex_s,uri_ex_o),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', testcase_premise_fullish_005_Everything_is_a_Resource)).
% 2.73/2.90  cnf(c0,plain,iext(uri_ex_p,uri_ex_s,uri_ex_o),inference(split_conjunct,[status(thm)],[testcase_premise_fullish_005_Everything_is_a_Resource])).
% 2.73/2.90  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.73/2.90  fof(c143,plain,(![S]:(![P]:(![O]:(~iext(P,S,O)|ip(P))))),inference(fof_nnf,[status(thm)],[simple_iext_property])).
% 2.73/2.90  fof(c144,plain,(![S]:(![P]:((![O]:~iext(P,S,O))|ip(P)))),inference(shift_quantors,[status(thm)],[c143])).
% 2.73/2.90  fof(c146,plain,(![X42]:(![X43]:(![X44]:(~iext(X43,X42,X44)|ip(X43))))),inference(shift_quantors,[status(thm)],[fof(c145,plain,(![X42]:(![X43]:((![X44]:~iext(X43,X42,X44))|ip(X43)))),inference(variable_rename,[status(thm)],[c144])).])).
% 2.73/2.90  cnf(c147,plain,~iext(X96,X98,X97)|ip(X96),inference(split_conjunct,[status(thm)],[c146])).
% 2.73/2.90  cnf(c501,plain,ip(uri_ex_p),inference(resolution,[status(thm)],[c147, c0])).
% 2.73/2.90  cnf(c549,plain,iext(uri_rdfs_subPropertyOf,uri_ex_p,uri_ex_p),inference(resolution,[status(thm)],[c501, c13])).
% 2.73/2.90  cnf(c998,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X564)|iext(X564,uri_ex_p,uri_ex_p),inference(resolution,[status(thm)],[c549, c21])).
% 2.73/2.90  cnf(c548,plain,iext(uri_rdf_type,uri_ex_p,uri_rdf_Property),inference(resolution,[status(thm)],[c501, c128])).
% 2.73/2.90  cnf(c989,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X562)|iext(X562,uri_ex_p,uri_rdf_Property),inference(resolution,[status(thm)],[c548, c21])).
% 2.73/2.90  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.73/2.90  cnf(c116,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_sub])).
% 2.73/2.90  cnf(c487,plain,ip(uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c147, c116])).
% 2.73/2.90  cnf(c547,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c487, c13])).
% 2.73/2.90  cnf(c982,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X561)|iext(X561,uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c547, c21])).
% 2.73/2.90  cnf(c546,plain,iext(uri_rdf_type,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c487, c128])).
% 2.73/2.90  cnf(c973,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X559)|iext(X559,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c546, c21])).
% 2.73/2.90  cnf(c479,plain,ip(uri_rdfs_domain),inference(resolution,[status(thm)],[c147, c48])).
% 2.73/2.90  cnf(c545,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,uri_rdfs_domain),inference(resolution,[status(thm)],[c479, c13])).
% 2.73/2.90  cnf(c955,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X558)|iext(X558,uri_rdfs_domain,uri_rdfs_domain),inference(resolution,[status(thm)],[c545, c21])).
% 2.73/2.90  cnf(c544,plain,iext(uri_rdf_type,uri_rdfs_domain,uri_rdf_Property),inference(resolution,[status(thm)],[c479, c128])).
% 2.73/2.90  cnf(c940,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X556)|iext(X556,uri_rdfs_domain,uri_rdf_Property),inference(resolution,[status(thm)],[c544, c21])).
% 2.73/2.90  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.73/2.90  cnf(c4,plain,iext(uri_rdfs_range,uri_rdf_value,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_value_range])).
% 2.73/2.90  cnf(c478,plain,ip(uri_rdfs_range),inference(resolution,[status(thm)],[c147, c4])).
% 2.73/2.90  cnf(c543,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_range,uri_rdfs_range),inference(resolution,[status(thm)],[c478, c13])).
% 2.73/2.90  cnf(c924,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X555)|iext(X555,uri_rdfs_range,uri_rdfs_range),inference(resolution,[status(thm)],[c543, c21])).
% 2.73/2.90  cnf(c542,plain,iext(uri_rdf_type,uri_rdfs_range,uri_rdf_Property),inference(resolution,[status(thm)],[c478, c128])).
% 2.73/2.90  cnf(c913,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X553)|iext(X553,uri_rdfs_range,uri_rdf_Property),inference(resolution,[status(thm)],[c542, c21])).
% 2.73/2.90  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.73/2.90  cnf(c98,plain,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Container),inference(split_conjunct,[status(thm)],[rdfs_container_alt_sub])).
% 2.73/2.90  cnf(c477,plain,ip(uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c147, c98])).
% 2.73/2.90  cnf(c541,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c477, c13])).
% 2.73/2.90  cnf(c905,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X552)|iext(X552,uri_rdfs_subClassOf,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c541, c21])).
% 2.73/2.90  cnf(c540,plain,iext(uri_rdf_type,uri_rdfs_subClassOf,uri_rdf_Property),inference(resolution,[status(thm)],[c477, c128])).
% 2.73/2.90  cnf(c894,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X550)|iext(X550,uri_rdfs_subClassOf,uri_rdf_Property),inference(resolution,[status(thm)],[c540, c21])).
% 2.73/2.90  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.73/2.90  cnf(c137,plain,iext(uri_rdf_type,uri_rdf_first,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_collection_first_type])).
% 2.73/2.90  cnf(c476,plain,ip(uri_rdf_first),inference(resolution,[status(thm)],[c137, c127])).
% 2.73/2.90  cnf(c539,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_first,uri_rdf_first),inference(resolution,[status(thm)],[c476, c13])).
% 2.73/2.90  cnf(c889,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X549)|iext(X549,uri_rdf_first,uri_rdf_first),inference(resolution,[status(thm)],[c539, c21])).
% 2.73/2.90  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.73/2.90  cnf(c135,plain,iext(uri_rdf_type,uri_rdf_rest,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_collection_rest_type])).
% 2.73/2.90  cnf(c463,plain,ip(uri_rdf_rest),inference(resolution,[status(thm)],[c135, c127])).
% 2.73/2.90  cnf(c465,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_rest,uri_rdf_rest),inference(resolution,[status(thm)],[c463, c13])).
% 2.73/2.90  cnf(c880,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X547)|iext(X547,uri_rdf_rest,uri_rdf_rest),inference(resolution,[status(thm)],[c465, c21])).
% 2.73/2.90  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.73/2.90  cnf(c134,plain,iext(uri_rdf_type,uri_rdf__1,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_container_n_type_001])).
% 2.73/2.90  cnf(c455,plain,ip(uri_rdf__1),inference(resolution,[status(thm)],[c134, c127])).
% 2.73/2.90  cnf(c457,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__1,uri_rdf__1),inference(resolution,[status(thm)],[c455, c13])).
% 2.73/2.90  cnf(c872,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X545)|iext(X545,uri_rdf__1,uri_rdf__1),inference(resolution,[status(thm)],[c457, c21])).
% 2.73/2.90  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.73/2.90  cnf(c133,plain,iext(uri_rdf_type,uri_rdf__2,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_container_n_type_002])).
% 2.73/2.90  cnf(c447,plain,ip(uri_rdf__2),inference(resolution,[status(thm)],[c133, c127])).
% 2.73/2.90  cnf(c449,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__2,uri_rdf__2),inference(resolution,[status(thm)],[c447, c13])).
% 2.73/2.90  cnf(c864,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X543)|iext(X543,uri_rdf__2,uri_rdf__2),inference(resolution,[status(thm)],[c449, c21])).
% 2.73/2.90  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.73/2.90  cnf(c132,plain,iext(uri_rdf_type,uri_rdf__3,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_container_n_type_003])).
% 2.73/2.90  cnf(c439,plain,ip(uri_rdf__3),inference(resolution,[status(thm)],[c132, c127])).
% 2.73/2.90  cnf(c441,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__3,uri_rdf__3),inference(resolution,[status(thm)],[c439, c13])).
% 2.73/2.90  cnf(c856,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X541)|iext(X541,uri_rdf__3,uri_rdf__3),inference(resolution,[status(thm)],[c441, c21])).
% 2.73/2.90  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.73/2.90  cnf(c131,plain,iext(uri_rdf_type,uri_rdf_object,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_reification_object_type])).
% 2.73/2.90  cnf(c426,plain,ip(uri_rdf_object),inference(resolution,[status(thm)],[c131, c127])).
% 2.73/2.90  cnf(c433,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_object,uri_rdf_object),inference(resolution,[status(thm)],[c426, c13])).
% 2.73/2.90  cnf(c847,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X539)|iext(X539,uri_rdf_object,uri_rdf_object),inference(resolution,[status(thm)],[c433, c21])).
% 2.73/2.90  cnf(c355,plain,ip(uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c116, c20])).
% 2.73/2.90  cnf(c429,plain,iext(uri_rdf_type,uri_rdfs_seeAlso,uri_rdf_Property),inference(resolution,[status(thm)],[c128, c355])).
% 2.73/2.90  cnf(c835,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X537)|iext(X537,uri_rdfs_seeAlso,uri_rdf_Property),inference(resolution,[status(thm)],[c429, c21])).
% 2.73/2.90  cnf(c19,plain,~iext(uri_rdfs_subPropertyOf,X51,X52)|ip(X51),inference(split_conjunct,[status(thm)],[c18])).
% 2.73/2.90  cnf(c358,plain,ip(uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c116, c19])).
% 2.73/2.90  cnf(c428,plain,iext(uri_rdf_type,uri_rdfs_isDefinedBy,uri_rdf_Property),inference(resolution,[status(thm)],[c128, c358])).
% 2.73/2.90  cnf(c828,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X536)|iext(X536,uri_rdfs_isDefinedBy,uri_rdf_Property),inference(resolution,[status(thm)],[c428, c21])).
% 2.73/2.90  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.73/2.90  cnf(c121,plain,iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_value_type])).
% 2.73/2.90  cnf(c417,plain,ip(uri_rdf_type),inference(resolution,[status(thm)],[c127, c121])).
% 2.73/2.90  cnf(c420,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_type,uri_rdf_type),inference(resolution,[status(thm)],[c417, c13])).
% 2.73/2.90  cnf(c820,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X535)|iext(X535,uri_rdf_type,uri_rdf_type),inference(resolution,[status(thm)],[c420, c21])).
% 2.73/2.90  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.73/2.90  cnf(c130,plain,iext(uri_rdf_type,uri_rdf_value,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_reification_predicate_type])).
% 2.73/2.90  cnf(c416,plain,ip(uri_rdf_value),inference(resolution,[status(thm)],[c127, c130])).
% 2.73/2.90  cnf(c419,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_value,uri_rdf_value),inference(resolution,[status(thm)],[c416, c13])).
% 2.73/2.90  cnf(c810,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X533)|iext(X533,uri_rdf_value,uri_rdf_value),inference(resolution,[status(thm)],[c419, c21])).
% 2.73/2.90  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.73/2.90  cnf(c129,plain,iext(uri_rdf_type,uri_rdf_subject,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_reification_subject_type])).
% 2.73/2.90  cnf(c415,plain,ip(uri_rdf_subject),inference(resolution,[status(thm)],[c127, c129])).
% 2.73/2.90  cnf(c418,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_subject,uri_rdf_subject),inference(resolution,[status(thm)],[c415, c13])).
% 2.73/2.90  cnf(c803,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X531)|iext(X531,uri_rdf_subject,uri_rdf_subject),inference(resolution,[status(thm)],[c418, c21])).
% 2.73/2.90  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.73/2.90  cnf(c93,plain,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_container_containermembershipproperty_sub])).
% 2.73/2.90  cnf(c192,plain,ic(uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c34, c93])).
% 2.73/2.90  cnf(c197,plain,icext(uri_rdfs_Class,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c192, c66])).
% 2.73/2.90  cnf(c386,plain,iext(uri_rdf_type,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Class),inference(resolution,[status(thm)],[c111, c197])).
% 2.73/2.90  cnf(c796,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X529)|iext(X529,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Class),inference(resolution,[status(thm)],[c386, c21])).
% 2.73/2.90  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.73/2.90  cnf(c97,plain,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Container),inference(split_conjunct,[status(thm)],[rdfs_container_bag_sub])).
% 2.73/2.90  cnf(c304,plain,ic(uri_rdf_Bag),inference(resolution,[status(thm)],[c97, c34])).
% 2.73/2.90  cnf(c306,plain,icext(uri_rdfs_Class,uri_rdf_Bag),inference(resolution,[status(thm)],[c304, c66])).
% 2.73/2.90  cnf(c385,plain,iext(uri_rdf_type,uri_rdf_Bag,uri_rdfs_Class),inference(resolution,[status(thm)],[c111, c306])).
% 2.73/2.90  cnf(c791,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X528)|iext(X528,uri_rdf_Bag,uri_rdfs_Class),inference(resolution,[status(thm)],[c385, c21])).
% 2.73/2.90  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.73/2.90  cnf(c81,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Container),inference(split_conjunct,[status(thm)],[rdfs_container_seq_sub])).
% 2.73/2.90  cnf(c206,plain,ic(uri_rdfs_Container),inference(resolution,[status(thm)],[c35, c81])).
% 2.73/2.90  cnf(c212,plain,icext(uri_rdfs_Class,uri_rdfs_Container),inference(resolution,[status(thm)],[c206, c66])).
% 2.73/2.90  cnf(c383,plain,iext(uri_rdf_type,uri_rdfs_Container,uri_rdfs_Class),inference(resolution,[status(thm)],[c111, c212])).
% 2.73/2.90  cnf(c786,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X527)|iext(X527,uri_rdfs_Container,uri_rdfs_Class),inference(resolution,[status(thm)],[c383, c21])).
% 2.73/2.90  cnf(c314,plain,ic(uri_rdf_Alt),inference(resolution,[status(thm)],[c98, c34])).
% 2.73/2.90  cnf(c316,plain,icext(uri_rdfs_Class,uri_rdf_Alt),inference(resolution,[status(thm)],[c314, c66])).
% 2.73/2.90  cnf(c382,plain,iext(uri_rdf_type,uri_rdf_Alt,uri_rdfs_Class),inference(resolution,[status(thm)],[c111, c316])).
% 2.73/2.90  cnf(c781,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X526)|iext(X526,uri_rdf_Alt,uri_rdfs_Class),inference(resolution,[status(thm)],[c382, c21])).
% 2.73/2.90  cnf(c207,plain,ic(uri_rdfs_Class),inference(resolution,[status(thm)],[c35, c75])).
% 2.73/2.90  cnf(c214,plain,icext(uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c207, c66])).
% 2.73/2.90  cnf(c381,plain,iext(uri_rdf_type,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c111, c214])).
% 2.73/2.90  cnf(c776,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X525)|iext(X525,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c381, c21])).
% 2.73/2.90  cnf(c193,plain,ic(uri_rdfs_Seq),inference(resolution,[status(thm)],[c34, c81])).
% 2.73/2.90  cnf(c199,plain,icext(uri_rdfs_Class,uri_rdfs_Seq),inference(resolution,[status(thm)],[c193, c66])).
% 2.73/2.90  cnf(c379,plain,iext(uri_rdf_type,uri_rdfs_Seq,uri_rdfs_Class),inference(resolution,[status(thm)],[c111, c199])).
% 2.73/2.90  cnf(c771,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X524)|iext(X524,uri_rdfs_Seq,uri_rdfs_Class),inference(resolution,[status(thm)],[c379, c21])).
% 2.73/2.90  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.73/2.90  cnf(c80,plain,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[rdfs_dat_xmlliteral_sub])).
% 2.73/2.90  cnf(c191,plain,ic(uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c34, c80])).
% 2.73/2.90  cnf(c195,plain,icext(uri_rdfs_Class,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c191, c66])).
% 2.73/2.90  cnf(c378,plain,iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Class),inference(resolution,[status(thm)],[c111, c195])).
% 2.73/2.90  cnf(c766,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X523)|iext(X523,uri_rdf_XMLLiteral,uri_rdfs_Class),inference(resolution,[status(thm)],[c378, c21])).
% 2.73/2.90  cnf(c204,plain,ic(uri_rdfs_Literal),inference(resolution,[status(thm)],[c35, c80])).
% 2.73/2.90  cnf(c208,plain,icext(uri_rdfs_Class,uri_rdfs_Literal),inference(resolution,[status(thm)],[c204, c66])).
% 2.73/2.90  cnf(c377,plain,iext(uri_rdf_type,uri_rdfs_Literal,uri_rdfs_Class),inference(resolution,[status(thm)],[c111, c208])).
% 2.73/2.90  cnf(c761,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X522)|iext(X522,uri_rdfs_Literal,uri_rdfs_Class),inference(resolution,[status(thm)],[c377, c21])).
% 2.73/2.90  cnf(c201,plain,icext(uri_rdfs_Class,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c194, c66])).
% 2.73/2.90  cnf(c376,plain,iext(uri_rdf_type,uri_rdfs_Datatype,uri_rdfs_Class),inference(resolution,[status(thm)],[c111, c201])).
% 2.73/2.90  cnf(c756,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X521)|iext(X521,uri_rdfs_Datatype,uri_rdfs_Class),inference(resolution,[status(thm)],[c376, c21])).
% 2.73/2.90  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.73/2.90  cnf(c83,plain,iext(uri_rdf_type,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),inference(split_conjunct,[status(thm)],[rdfs_container_n_type_002])).
% 2.73/2.90  cnf(c367,plain,icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__2),inference(resolution,[status(thm)],[c110, c83])).
% 2.73/2.90  cnf(c372,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__2,uri_rdfs_member),inference(resolution,[status(thm)],[c367, c96])).
% 2.73/2.90  cnf(c751,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X520)|iext(X520,uri_rdf__2,uri_rdfs_member),inference(resolution,[status(thm)],[c372, c21])).
% 2.73/2.90  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.73/2.90  fof(c8,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.73/2.90  fof(c9,plain,(![X2]:(![X3]:(![X4]:((~iext(uri_rdfs_subPropertyOf,X2,X3)|~iext(uri_rdfs_subPropertyOf,X3,X4))|iext(uri_rdfs_subPropertyOf,X2,X4))))),inference(variable_rename,[status(thm)],[c8])).
% 2.73/2.90  cnf(c10,plain,~iext(uri_rdfs_subPropertyOf,X48,X47)|~iext(uri_rdfs_subPropertyOf,X47,X49)|iext(uri_rdfs_subPropertyOf,X48,X49),inference(split_conjunct,[status(thm)],[c9])).
% 2.73/2.90  cnf(c750,plain,~iext(uri_rdfs_subPropertyOf,X519,uri_rdf__2)|iext(uri_rdfs_subPropertyOf,X519,uri_rdfs_member),inference(resolution,[status(thm)],[c372, c10])).
% 2.73/2.90  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.73/2.90  cnf(c82,plain,iext(uri_rdf_type,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),inference(split_conjunct,[status(thm)],[rdfs_container_n_type_003])).
% 2.73/2.90  cnf(c365,plain,icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__3),inference(resolution,[status(thm)],[c110, c82])).
% 2.73/2.90  cnf(c370,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__3,uri_rdfs_member),inference(resolution,[status(thm)],[c365, c96])).
% 2.73/2.90  cnf(c744,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X518)|iext(X518,uri_rdf__3,uri_rdfs_member),inference(resolution,[status(thm)],[c370, c21])).
% 2.73/2.90  cnf(c743,plain,~iext(uri_rdfs_subPropertyOf,X517,uri_rdf__3)|iext(uri_rdfs_subPropertyOf,X517,uri_rdfs_member),inference(resolution,[status(thm)],[c370, c10])).
% 2.73/2.90  cnf(c734,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X516)|iext(X516,uri_rdf__1,uri_rdfs_member),inference(resolution,[status(thm)],[c369, c21])).
% 2.73/2.90  cnf(c733,plain,~iext(uri_rdfs_subPropertyOf,X515,uri_rdf__1)|iext(uri_rdfs_subPropertyOf,X515,uri_rdfs_member),inference(resolution,[status(thm)],[c369, c10])).
% 2.73/2.90  cnf(c360,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c358, c13])).
% 2.73/2.90  cnf(c726,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X514)|iext(X514,uri_rdfs_isDefinedBy,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c360, c21])).
% 2.73/2.90  cnf(c1196,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X512)|icext(X512,uri_rdfs_comment),inference(resolution,[status(thm)],[c1188, c47])).
% 2.73/2.90  cnf(c1193,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X511)|icext(X511,uri_rdfs_comment),inference(resolution,[status(thm)],[c1188, c73])).
% 2.73/2.90  cnf(c359,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_seeAlso,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c355, c13])).
% 2.73/2.90  cnf(c719,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X510)|iext(X510,uri_rdfs_seeAlso,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c359, c21])).
% 2.73/2.90  cnf(c1167,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X507)|icext(X507,uri_rdfs_label),inference(resolution,[status(thm)],[c1159, c47])).
% 2.73/2.90  cnf(c1164,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X505)|icext(X505,uri_rdfs_label),inference(resolution,[status(thm)],[c1159, c73])).
% 2.73/2.90  cnf(c349,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Literal,uri_rdfs_Resource),inference(resolution,[status(thm)],[c105, c204])).
% 2.73/2.90  cnf(c712,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X502)|iext(X502,uri_rdfs_Literal,uri_rdfs_Resource),inference(resolution,[status(thm)],[c349, c21])).
% 2.73/2.90  cnf(c1135,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X501)|icext(X501,uri_rdf_List),inference(resolution,[status(thm)],[c1112, c47])).
% 2.73/2.90  cnf(c711,plain,~iext(uri_rdfs_subClassOf,X498,uri_rdfs_Literal)|iext(uri_rdfs_subClassOf,X498,uri_rdfs_Resource),inference(resolution,[status(thm)],[c349, c25])).
% 2.73/2.90  cnf(c1122,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X497)|icext(X497,uri_rdf_List),inference(resolution,[status(thm)],[c1111, c73])).
% 2.73/2.90  cnf(c348,plain,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Resource),inference(resolution,[status(thm)],[c105, c191])).
% 2.73/2.90  cnf(c704,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X494)|iext(X494,uri_rdf_XMLLiteral,uri_rdfs_Resource),inference(resolution,[status(thm)],[c348, c21])).
% 2.73/2.90  cnf(c1085,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X493)|icext(X493,uri_rdf_predicate),inference(resolution,[status(thm)],[c1077, c73])).
% 2.73/2.90  cnf(c1084,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X492)|icext(X492,uri_rdf_predicate),inference(resolution,[status(thm)],[c1077, c47])).
% 2.73/2.90  cnf(c703,plain,~iext(uri_rdfs_subClassOf,X491,uri_rdf_XMLLiteral)|iext(uri_rdfs_subClassOf,X491,uri_rdfs_Resource),inference(resolution,[status(thm)],[c348, c25])).
% 2.73/2.90  cnf(c347,plain,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Resource),inference(resolution,[status(thm)],[c105, c304])).
% 2.73/2.90  cnf(c696,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X487)|iext(X487,uri_rdf_Bag,uri_rdfs_Resource),inference(resolution,[status(thm)],[c347, c21])).
% 2.73/2.90  cnf(c1054,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X486)|icext(X486,uri_rdfs_Statement),inference(resolution,[status(thm)],[c972, c47])).
% 2.73/2.90  cnf(c1047,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X485)|icext(X485,uri_rdfs_Statement),inference(resolution,[status(thm)],[c971, c73])).
% 2.73/2.90  cnf(c695,plain,~iext(uri_rdfs_subClassOf,X483,uri_rdf_Bag)|iext(uri_rdfs_subClassOf,X483,uri_rdfs_Resource),inference(resolution,[status(thm)],[c347, c25])).
% 2.73/2.90  cnf(c1031,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X480)|icext(X480,uri_rdfs_member),inference(resolution,[status(thm)],[c740, c73])).
% 2.73/2.90  cnf(c346,plain,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Resource),inference(resolution,[status(thm)],[c105, c314])).
% 2.73/2.90  cnf(c688,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X479)|iext(X479,uri_rdf_Alt,uri_rdfs_Resource),inference(resolution,[status(thm)],[c346, c21])).
% 2.73/2.90  cnf(c687,plain,~iext(uri_rdfs_subClassOf,X474,uri_rdf_Alt)|iext(uri_rdfs_subClassOf,X474,uri_rdfs_Resource),inference(resolution,[status(thm)],[c346, c25])).
% 2.73/2.90  cnf(c1012,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X472)|icext(X472,uri_rdfs_Resource),inference(resolution,[status(thm)],[c640, c73])).
% 2.73/2.90  cnf(c345,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Container,uri_rdfs_Resource),inference(resolution,[status(thm)],[c105, c206])).
% 2.73/2.90  cnf(c680,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X470)|iext(X470,uri_rdfs_Container,uri_rdfs_Resource),inference(resolution,[status(thm)],[c345, c21])).
% 2.73/2.90  cnf(c679,plain,~iext(uri_rdfs_subClassOf,X469,uri_rdfs_Container)|iext(uri_rdfs_subClassOf,X469,uri_rdfs_Resource),inference(resolution,[status(thm)],[c345, c25])).
% 2.73/2.90  cnf(c1003,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X468)|icext(X468,uri_ex_p),inference(resolution,[status(thm)],[c549, c73])).
% 2.73/2.90  cnf(c1001,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X467)|icext(X467,uri_ex_p),inference(resolution,[status(thm)],[c549, c47])).
% 2.73/2.90  cnf(c344,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Resource),inference(resolution,[status(thm)],[c105, c193])).
% 2.73/2.90  cnf(c672,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X465)|iext(X465,uri_rdfs_Seq,uri_rdfs_Resource),inference(resolution,[status(thm)],[c344, c21])).
% 2.73/2.90  cnf(c987,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X463)|icext(X463,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c547, c73])).
% 2.73/2.90  cnf(c671,plain,~iext(uri_rdfs_subClassOf,X462,uri_rdfs_Seq)|iext(uri_rdfs_subClassOf,X462,uri_rdfs_Resource),inference(resolution,[status(thm)],[c344, c25])).
% 2.73/2.90  cnf(c986,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X461)|icext(X461,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c547, c47])).
% 2.73/2.90  cnf(c205,plain,ic(uri_rdf_Property),inference(resolution,[status(thm)],[c35, c93])).
% 2.73/2.90  cnf(c343,plain,iext(uri_rdfs_subClassOf,uri_rdf_Property,uri_rdfs_Resource),inference(resolution,[status(thm)],[c105, c205])).
% 2.73/2.90  cnf(c664,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X458)|iext(X458,uri_rdf_Property,uri_rdfs_Resource),inference(resolution,[status(thm)],[c343, c21])).
% 2.73/2.90  cnf(c966,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X457)|icext(X457,uri_rdfs_domain),inference(resolution,[status(thm)],[c545, c73])).
% 2.73/2.90  cnf(c958,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X456)|icext(X456,uri_rdfs_domain),inference(resolution,[status(thm)],[c545, c47])).
% 2.73/2.90  cnf(c663,plain,~iext(uri_rdfs_subClassOf,X455,uri_rdf_Property)|iext(uri_rdfs_subClassOf,X455,uri_rdfs_Resource),inference(resolution,[status(thm)],[c343, c25])).
% 2.73/2.90  cnf(c938,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X452)|icext(X452,uri_rdfs_range),inference(resolution,[status(thm)],[c543, c73])).
% 2.73/2.90  cnf(c342,plain,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Resource),inference(resolution,[status(thm)],[c105, c192])).
% 2.73/2.90  cnf(c656,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X451)|iext(X451,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Resource),inference(resolution,[status(thm)],[c342, c21])).
% 2.73/2.90  cnf(c929,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X450)|icext(X450,uri_rdfs_range),inference(resolution,[status(thm)],[c543, c47])).
% 2.73/2.90  cnf(c655,plain,~iext(uri_rdfs_subClassOf,X447,uri_rdfs_ContainerMembershipProperty)|iext(uri_rdfs_subClassOf,X447,uri_rdfs_Resource),inference(resolution,[status(thm)],[c342, c25])).
% 2.73/2.90  cnf(c911,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X446)|icext(X446,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c541, c73])).
% 2.73/2.90  cnf(c908,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X445)|icext(X445,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c541, c47])).
% 2.73/2.90  cnf(c341,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c105, c207])).
% 2.73/2.90  cnf(c648,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X444)|iext(X444,uri_rdfs_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c341, c21])).
% 2.73/2.90  cnf(c647,plain,~iext(uri_rdfs_subClassOf,X441,uri_rdfs_Class)|iext(uri_rdfs_subClassOf,X441,uri_rdfs_Resource),inference(resolution,[status(thm)],[c341, c25])).
% 2.73/2.90  cnf(c893,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X440)|icext(X440,uri_rdf_first),inference(resolution,[status(thm)],[c539, c73])).
% 2.73/2.90  cnf(c892,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X439)|icext(X439,uri_rdf_first),inference(resolution,[status(thm)],[c539, c47])).
% 2.73/2.90  cnf(c635,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X438)|iext(X438,uri_rdfs_Datatype,uri_rdfs_Resource),inference(resolution,[status(thm)],[c340, c21])).
% 2.73/2.90  cnf(c884,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X437)|icext(X437,uri_rdf_rest),inference(resolution,[status(thm)],[c465, c73])).
% 2.73/2.90  cnf(c883,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X436)|icext(X436,uri_rdf_rest),inference(resolution,[status(thm)],[c465, c47])).
% 2.73/2.90  cnf(c634,plain,~iext(uri_rdfs_subClassOf,X434,uri_rdfs_Datatype)|iext(uri_rdfs_subClassOf,X434,uri_rdfs_Resource),inference(resolution,[status(thm)],[c340, c25])).
% 2.73/2.90  cnf(c875,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X433)|icext(X433,uri_rdf__1),inference(resolution,[status(thm)],[c457, c47])).
% 2.73/2.90  cnf(c317,plain,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdf_Alt),inference(resolution,[status(thm)],[c314, c28])).
% 2.73/2.90  cnf(c627,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X431)|iext(X431,uri_rdf_Alt,uri_rdf_Alt),inference(resolution,[status(thm)],[c317, c21])).
% 2.73/2.90  cnf(c867,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X430)|icext(X430,uri_rdf__2),inference(resolution,[status(thm)],[c449, c47])).
% 2.73/2.90  cnf(c859,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X428)|icext(X428,uri_rdf__3),inference(resolution,[status(thm)],[c441, c47])).
% 2.73/2.90  cnf(c851,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X426)|icext(X426,uri_rdf_object),inference(resolution,[status(thm)],[c433, c73])).
% 2.73/2.90  cnf(c850,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X425)|icext(X425,uri_rdf_object),inference(resolution,[status(thm)],[c433, c47])).
% 2.73/2.90  cnf(c307,plain,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdf_Bag),inference(resolution,[status(thm)],[c304, c28])).
% 2.73/2.90  cnf(c619,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X423)|iext(X423,uri_rdf_Bag,uri_rdf_Bag),inference(resolution,[status(thm)],[c307, c21])).
% 2.73/2.90  cnf(c827,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X419)|icext(X419,uri_rdf_type),inference(resolution,[status(thm)],[c420, c73])).
% 2.73/2.90  cnf(c825,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X417)|icext(X417,uri_rdf_type),inference(resolution,[status(thm)],[c420, c47])).
% 2.73/2.90  cnf(c814,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X416)|icext(X416,uri_rdf_value),inference(resolution,[status(thm)],[c419, c73])).
% 2.73/2.90  cnf(c215,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c207, c28])).
% 2.73/2.90  cnf(c611,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X415)|iext(X415,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c215, c21])).
% 2.73/2.90  cnf(c813,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X414)|icext(X414,uri_rdf_value),inference(resolution,[status(thm)],[c419, c47])).
% 2.73/2.90  cnf(c807,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X413)|icext(X413,uri_rdf_subject),inference(resolution,[status(thm)],[c418, c73])).
% 2.73/2.90  cnf(c806,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X411)|icext(X411,uri_rdf_subject),inference(resolution,[status(thm)],[c418, c47])).
% 2.73/2.90  cnf(c213,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Container,uri_rdfs_Container),inference(resolution,[status(thm)],[c206, c28])).
% 2.73/2.90  cnf(c603,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X407)|iext(X407,uri_rdfs_Container,uri_rdfs_Container),inference(resolution,[status(thm)],[c213, c21])).
% 2.73/2.90  cnf(c211,plain,iext(uri_rdfs_subClassOf,uri_rdf_Property,uri_rdf_Property),inference(resolution,[status(thm)],[c205, c28])).
% 2.73/2.90  cnf(c595,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X396)|iext(X396,uri_rdf_Property,uri_rdf_Property),inference(resolution,[status(thm)],[c211, c21])).
% 2.73/2.90  cnf(c755,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X388)|icext(X388,uri_rdf__2),inference(resolution,[status(thm)],[c372, c73])).
% 2.73/2.90  cnf(c209,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Literal,uri_rdfs_Literal),inference(resolution,[status(thm)],[c204, c28])).
% 2.73/2.90  cnf(c587,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X386)|iext(X386,uri_rdfs_Literal,uri_rdfs_Literal),inference(resolution,[status(thm)],[c209, c21])).
% 2.73/2.90  cnf(c748,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X385)|icext(X385,uri_rdf__3),inference(resolution,[status(thm)],[c370, c73])).
% 2.73/2.90  cnf(c738,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X383)|icext(X383,uri_rdf__1),inference(resolution,[status(thm)],[c369, c73])).
% 2.73/2.90  cnf(c737,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X381)|icext(X381,uri_rdfs_member),inference(resolution,[status(thm)],[c369, c47])).
% 2.73/2.90  cnf(c202,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c194, c28])).
% 2.73/2.90  cnf(c579,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X379)|iext(X379,uri_rdfs_Datatype,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c202, c21])).
% 2.73/2.90  cnf(c729,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X378)|icext(X378,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c360, c47])).
% 2.73/2.90  cnf(c723,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X377)|icext(X377,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c359, c73])).
% 2.73/2.90  cnf(c200,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Seq),inference(resolution,[status(thm)],[c193, c28])).
% 2.73/2.90  cnf(c571,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X369)|iext(X369,uri_rdfs_Seq,uri_rdfs_Seq),inference(resolution,[status(thm)],[c200, c21])).
% 2.73/2.90  cnf(c198,plain,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c192, c28])).
% 2.73/2.90  cnf(c563,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X358)|iext(X358,uri_rdfs_ContainerMembershipProperty,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c198, c21])).
% 2.73/2.90  cnf(c637,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X351)|icext(X351,uri_rdfs_Resource),inference(resolution,[status(thm)],[c340, c47])).
% 2.73/2.90  cnf(c196,plain,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c191, c28])).
% 2.73/2.90  cnf(c555,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X349)|iext(X349,uri_rdf_XMLLiteral,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c196, c21])).
% 2.73/2.90  cnf(c629,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X348)|icext(X348,uri_rdf_Alt),inference(resolution,[status(thm)],[c317, c47])).
% 2.73/2.90  cnf(c621,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X346)|icext(X346,uri_rdf_Bag),inference(resolution,[status(thm)],[c307, c47])).
% 2.73/2.90  cnf(c614,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X344)|icext(X344,uri_rdfs_Class),inference(resolution,[status(thm)],[c215, c73])).
% 2.73/2.90  cnf(c606,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X342)|icext(X342,uri_rdfs_Container),inference(resolution,[status(thm)],[c213, c73])).
% 2.73/2.90  cnf(c473,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X341)|iext(X341,uri_rdf_first,uri_rdf_Property),inference(resolution,[status(thm)],[c137, c21])).
% 2.73/2.90  cnf(c598,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X339)|icext(X339,uri_rdf_Property),inference(resolution,[status(thm)],[c211, c73])).
% 2.73/2.90  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.73/2.90  cnf(c136,plain,iext(uri_rdf_type,uri_rdf_nil,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdf_collection_nil_type])).
% 2.73/2.90  cnf(c468,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X337)|iext(X337,uri_rdf_nil,uri_rdf_List),inference(resolution,[status(thm)],[c136, c21])).
% 2.73/2.90  cnf(c590,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X336)|icext(X336,uri_rdfs_Literal),inference(resolution,[status(thm)],[c209, c73])).
% 2.73/2.90  cnf(c460,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X333)|iext(X333,uri_rdf_rest,uri_rdf_Property),inference(resolution,[status(thm)],[c135, c21])).
% 2.73/2.90  cnf(c581,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X332)|icext(X332,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c202, c47])).
% 2.73/2.90  cnf(c452,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X330)|iext(X330,uri_rdf__1,uri_rdf_Property),inference(resolution,[status(thm)],[c134, c21])).
% 2.73/2.90  cnf(c573,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X329)|icext(X329,uri_rdfs_Seq),inference(resolution,[status(thm)],[c200, c47])).
% 2.73/2.90  cnf(c565,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X327)|icext(X327,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c198, c47])).
% 2.73/2.90  cnf(c444,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X326)|iext(X326,uri_rdf__2,uri_rdf_Property),inference(resolution,[status(thm)],[c133, c21])).
% 2.73/2.90  cnf(c557,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X324)|icext(X324,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c196, c47])).
% 2.73/2.90  cnf(c436,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X322)|iext(X322,uri_rdf__3,uri_rdf_Property),inference(resolution,[status(thm)],[c132, c21])).
% 2.73/2.90  cnf(c467,plain,~iext(uri_rdfs_range,uri_rdf_type,X319)|icext(X319,uri_rdf_List),inference(resolution,[status(thm)],[c136, c47])).
% 2.73/2.90  cnf(c423,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X318)|iext(X318,uri_rdf_object,uri_rdf_Property),inference(resolution,[status(thm)],[c131, c21])).
% 2.73/2.90  cnf(c412,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X313)|iext(X313,uri_rdf_value,uri_rdf_Property),inference(resolution,[status(thm)],[c130, c21])).
% 2.73/2.90  cnf(c407,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X308)|iext(X308,uri_rdf_subject,uri_rdf_Property),inference(resolution,[status(thm)],[c129, c21])).
% 2.73/2.90  cnf(c402,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X303)|iext(X303,uri_rdf_type,uri_rdf_Property),inference(resolution,[status(thm)],[c121, c21])).
% 2.73/2.90  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.73/2.90  cnf(c120,plain,iext(uri_rdfs_domain,uri_rdfs_comment,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_comment_domain])).
% 2.73/2.90  cnf(c399,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X299)|iext(X299,uri_rdfs_comment,uri_rdfs_Resource),inference(resolution,[status(thm)],[c120, c21])).
% 2.73/2.90  cnf(c401,plain,~iext(uri_rdfs_range,uri_rdf_type,X298)|icext(X298,uri_rdf_Property),inference(resolution,[status(thm)],[c121, c47])).
% 2.73/2.90  cnf(c400,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X297)|icext(X297,uri_rdfs_comment),inference(resolution,[status(thm)],[c120, c73])).
% 2.73/2.90  cnf(c396,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X295)|iext(X295,uri_rdfs_comment,uri_rdfs_Literal),inference(resolution,[status(thm)],[c119, c21])).
% 2.73/2.90  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.73/2.90  cnf(c118,plain,iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_domain])).
% 2.73/2.90  cnf(c393,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X294)|iext(X294,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(resolution,[status(thm)],[c118, c21])).
% 2.73/2.90  fof(simple_ir,axiom,(![X]:ir(X)),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', simple_ir)).
% 2.73/2.90  fof(c141,plain,(![X41]:ir(X41)),inference(variable_rename,[status(thm)],[simple_ir])).
% 2.73/2.90  cnf(c142,plain,ir(X45),inference(split_conjunct,[status(thm)],[c141])).
% 2.73/2.90  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.73/2.90  fof(c56,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.73/2.90  fof(c57,plain,((![X]:(~ir(X)|icext(uri_rdfs_Resource,X)))&(![X]:(~icext(uri_rdfs_Resource,X)|ir(X)))),inference(shift_quantors,[status(thm)],[c56])).
% 2.73/2.90  fof(c59,plain,(![X23]:(![X24]:((~ir(X23)|icext(uri_rdfs_Resource,X23))&(~icext(uri_rdfs_Resource,X24)|ir(X24))))),inference(shift_quantors,[status(thm)],[fof(c58,plain,((![X23]:(~ir(X23)|icext(uri_rdfs_Resource,X23)))&(![X24]:(~icext(uri_rdfs_Resource,X24)|ir(X24)))),inference(variable_rename,[status(thm)],[c57])).])).
% 2.73/2.90  cnf(c60,plain,~ir(X55)|icext(uri_rdfs_Resource,X55),inference(split_conjunct,[status(thm)],[c59])).
% 2.73/2.90  cnf(c149,plain,icext(uri_rdfs_Resource,X56),inference(resolution,[status(thm)],[c60, c142])).
% 2.73/2.90  cnf(c384,plain,iext(uri_rdf_type,X92,uri_rdfs_Resource),inference(resolution,[status(thm)],[c111, c149])).
% 2.73/2.90  cnf(c389,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X291)|iext(X291,X292,uri_rdfs_Resource),inference(resolution,[status(thm)],[c384, c21])).
% 2.73/2.90  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.73/2.90  cnf(c117,plain,iext(uri_rdfs_range,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_range])).
% 2.73/2.90  cnf(c362,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X288)|iext(X288,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(resolution,[status(thm)],[c117, c21])).
% 2.73/2.90  cnf(c394,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X287)|icext(X287,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c118, c73])).
% 2.73/2.90  cnf(c357,plain,~iext(uri_rdfs_subPropertyOf,X285,uri_rdfs_isDefinedBy)|iext(uri_rdfs_subPropertyOf,X285,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c116, c10])).
% 2.73/2.90  cnf(c388,plain,~iext(uri_rdfs_range,uri_rdf_type,X284)|icext(X284,uri_rdfs_Resource),inference(resolution,[status(thm)],[c384, c47])).
% 2.73/2.90  cnf(c363,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X283)|icext(X283,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c117, c73])).
% 2.73/2.90  cnf(c354,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X281)|iext(X281,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c116, c21])).
% 2.73/2.90  cnf(c356,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X280)|icext(X280,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c116, c73])).
% 2.73/2.90  cnf(c353,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X279)|icext(X279,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c116, c47])).
% 2.73/2.90  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.73/2.90  cnf(c115,plain,iext(uri_rdfs_domain,uri_rdfs_label,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_label_domain])).
% 2.73/2.90  cnf(c351,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X278)|iext(X278,uri_rdfs_label,uri_rdfs_Resource),inference(resolution,[status(thm)],[c115, c21])).
% 2.73/2.90  cnf(c352,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X277)|icext(X277,uri_rdfs_label),inference(resolution,[status(thm)],[c115, c73])).
% 2.73/2.90  cnf(c338,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X275)|iext(X275,uri_rdfs_label,uri_rdfs_Literal),inference(resolution,[status(thm)],[c114, c21])).
% 2.73/2.90  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.73/2.90  cnf(c113,plain,iext(uri_rdfs_domain,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_seealso_domain])).
% 2.73/2.90  cnf(c335,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X273)|iext(X273,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(resolution,[status(thm)],[c113, c21])).
% 2.73/2.90  cnf(c337,plain,~iext(uri_rdfs_range,uri_rdfs_range,X272)|icext(X272,uri_rdfs_Literal),inference(resolution,[status(thm)],[c114, c47])).
% 2.73/2.90  cnf(c336,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X271)|icext(X271,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c113, c73])).
% 2.73/2.90  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.73/2.90  cnf(c112,plain,iext(uri_rdfs_range,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_seealso_range])).
% 2.73/2.90  cnf(c332,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X270)|iext(X270,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(resolution,[status(thm)],[c112, c21])).
% 2.73/2.90  cnf(c333,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X268)|icext(X268,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c112, c73])).
% 2.73/2.90  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.73/2.90  cnf(c102,plain,iext(uri_rdfs_domain,uri_rdf_first,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdfs_collection_first_domain])).
% 2.73/2.90  cnf(c329,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X266)|iext(X266,uri_rdf_first,uri_rdf_List),inference(resolution,[status(thm)],[c102, c21])).
% 2.73/2.90  cnf(c330,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X265)|icext(X265,uri_rdf_first),inference(resolution,[status(thm)],[c102, c73])).
% 2.73/2.90  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.73/2.90  cnf(c101,plain,iext(uri_rdfs_range,uri_rdf_first,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_collection_first_range])).
% 2.73/2.90  cnf(c326,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X263)|iext(X263,uri_rdf_first,uri_rdfs_Resource),inference(resolution,[status(thm)],[c101, c21])).
% 2.73/2.90  cnf(c327,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X262)|icext(X262,uri_rdf_first),inference(resolution,[status(thm)],[c101, c73])).
% 2.73/2.90  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.73/2.90  cnf(c100,plain,iext(uri_rdfs_domain,uri_rdf_rest,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdfs_collection_rest_domain])).
% 2.73/2.90  cnf(c324,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X260)|icext(X260,uri_rdf_rest),inference(resolution,[status(thm)],[c100, c73])).
% 2.73/2.90  cnf(c323,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X259)|iext(X259,uri_rdf_rest,uri_rdf_List),inference(resolution,[status(thm)],[c100, c21])).
% 2.73/2.90  cnf(c322,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X258)|icext(X258,uri_rdf_List),inference(resolution,[status(thm)],[c100, c47])).
% 2.73/2.90  cnf(c321,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X255)|icext(X255,uri_rdf_rest),inference(resolution,[status(thm)],[c99, c73])).
% 2.73/2.90  cnf(c320,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X254)|iext(X254,uri_rdf_rest,uri_rdf_List),inference(resolution,[status(thm)],[c99, c21])).
% 2.73/2.90  cnf(c311,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X253)|iext(X253,uri_rdf_Alt,uri_rdfs_Container),inference(resolution,[status(thm)],[c98, c21])).
% 2.73/2.90  cnf(c309,plain,~iext(uri_rdfs_subClassOf,X252,uri_rdf_Alt)|iext(uri_rdfs_subClassOf,X252,uri_rdfs_Container),inference(resolution,[status(thm)],[c98, c25])).
% 2.73/2.90  cnf(c301,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X250)|iext(X250,uri_rdf_Bag,uri_rdfs_Container),inference(resolution,[status(thm)],[c97, c21])).
% 2.73/2.90  cnf(c312,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X249)|icext(X249,uri_rdf_Alt),inference(resolution,[status(thm)],[c98, c73])).
% 2.73/2.90  cnf(c302,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X247)|icext(X247,uri_rdf_Bag),inference(resolution,[status(thm)],[c97, c73])).
% 2.73/2.90  cnf(c299,plain,~iext(uri_rdfs_subClassOf,X246,uri_rdf_Bag)|iext(uri_rdfs_subClassOf,X246,uri_rdfs_Container),inference(resolution,[status(thm)],[c97, c25])).
% 2.73/2.90  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.73/2.90  cnf(c88,plain,iext(uri_rdfs_domain,uri_rdf__3,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_003])).
% 2.73/2.90  cnf(c295,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X243)|icext(X243,uri_rdf__3),inference(resolution,[status(thm)],[c73, c88])).
% 2.73/2.90  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.73/2.90  cnf(c90,plain,iext(uri_rdfs_domain,uri_rdf__1,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_001])).
% 2.73/2.90  cnf(c294,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X242)|icext(X242,uri_rdf__1),inference(resolution,[status(thm)],[c73, c90])).
% 2.73/2.90  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.73/2.90  cnf(c22,plain,iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_subpropertyof_domain])).
% 2.73/2.90  cnf(c293,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X241)|icext(X241,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c73, c22])).
% 2.73/2.90  cnf(c292,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X240)|icext(X240,uri_rdfs_range),inference(resolution,[status(thm)],[c73, c44])).
% 2.73/2.90  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.73/2.90  cnf(c89,plain,iext(uri_rdfs_domain,uri_rdf__2,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_002])).
% 2.73/2.90  cnf(c290,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X238)|icext(X238,uri_rdf__2),inference(resolution,[status(thm)],[c73, c89])).
% 2.73/2.90  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.73/2.90  cnf(c87,plain,iext(uri_rdfs_range,uri_rdf__1,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_range_001])).
% 2.73/2.90  cnf(c289,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X237)|icext(X237,uri_rdf__1),inference(resolution,[status(thm)],[c73, c87])).
% 2.73/2.90  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.73/2.90  cnf(c29,plain,iext(uri_rdfs_range,uri_rdfs_subClassOf,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_subclassof_range])).
% 2.73/2.90  cnf(c288,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X236)|icext(X236,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c73, c29])).
% 2.73/2.90  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.73/2.90  cnf(c14,plain,iext(uri_rdfs_range,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_subpropertyof_range])).
% 2.73/2.90  cnf(c287,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X235)|icext(X235,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c73, c14])).
% 2.73/2.90  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.73/2.90  cnf(c7,plain,iext(uri_rdfs_domain,uri_rdf_type,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_type_domain])).
% 2.73/2.90  cnf(c286,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X234)|icext(X234,uri_rdf_type),inference(resolution,[status(thm)],[c73, c7])).
% 2.73/2.90  cnf(c285,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X233)|icext(X233,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c73, c75])).
% 2.73/2.90  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.73/2.90  cnf(c86,plain,iext(uri_rdfs_range,uri_rdf__2,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_range_002])).
% 2.73/2.90  cnf(c284,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X232)|icext(X232,uri_rdf__2),inference(resolution,[status(thm)],[c73, c86])).
% 2.73/2.90  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.73/2.90  cnf(c6,plain,iext(uri_rdfs_range,uri_rdf_type,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_type_range])).
% 2.73/2.90  cnf(c283,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X231)|icext(X231,uri_rdf_type),inference(resolution,[status(thm)],[c73, c6])).
% 2.73/2.90  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.73/2.90  cnf(c85,plain,iext(uri_rdfs_range,uri_rdf__3,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_range_003])).
% 2.73/2.90  cnf(c282,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X230)|icext(X230,uri_rdf__3),inference(resolution,[status(thm)],[c73, c85])).
% 2.73/2.90  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.73/2.90  cnf(c41,plain,iext(uri_rdfs_domain,uri_rdf_predicate,uri_rdfs_Statement),inference(split_conjunct,[status(thm)],[rdfs_reification_predicate_domain])).
% 2.73/2.90  cnf(c278,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X226)|icext(X226,uri_rdf_predicate),inference(resolution,[status(thm)],[c73, c41])).
% 2.73/2.90  cnf(c277,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X225)|icext(X225,uri_rdfs_domain),inference(resolution,[status(thm)],[c73, c68])).
% 2.73/2.90  cnf(c276,plain,~iext(uri_rdfs_domain,uri_ex_p,X224)|icext(X224,uri_ex_s),inference(resolution,[status(thm)],[c73, c0])).
% 2.73/2.90  cnf(c275,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X223)|icext(X223,uri_rdfs_Seq),inference(resolution,[status(thm)],[c73, c81])).
% 2.73/2.90  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.73/2.90  cnf(c39,plain,iext(uri_rdfs_domain,uri_rdf_subject,uri_rdfs_Statement),inference(split_conjunct,[status(thm)],[rdfs_reification_subject_domain])).
% 2.73/2.90  cnf(c274,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X222)|icext(X222,uri_rdf_subject),inference(resolution,[status(thm)],[c73, c39])).
% 2.73/2.90  cnf(c273,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X221)|icext(X221,uri_rdf_object),inference(resolution,[status(thm)],[c73, c43])).
% 2.73/2.90  cnf(c271,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X219)|icext(X219,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c73, c93])).
% 2.73/2.90  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.73/2.90  cnf(c38,plain,iext(uri_rdfs_range,uri_rdf_subject,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_reification_subject_range])).
% 2.73/2.90  cnf(c270,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X218)|icext(X218,uri_rdf_subject),inference(resolution,[status(thm)],[c73, c38])).
% 2.73/2.90  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.73/2.90  cnf(c37,plain,iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_subclassof_domain])).
% 2.73/2.90  cnf(c269,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X217)|icext(X217,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c73, c37])).
% 2.73/2.90  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.73/2.90  cnf(c5,plain,iext(uri_rdfs_domain,uri_rdf_value,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_value_domain])).
% 2.73/2.90  cnf(c268,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X216)|icext(X216,uri_rdf_value),inference(resolution,[status(thm)],[c73, c5])).
% 2.73/2.90  cnf(c267,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X215)|icext(X215,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c73, c80])).
% 2.73/2.90  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.73/2.90  cnf(c92,plain,iext(uri_rdfs_domain,uri_rdfs_member,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_member_domain])).
% 2.73/2.90  cnf(c265,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X213)|icext(X213,uri_rdfs_member),inference(resolution,[status(thm)],[c73, c92])).
% 2.73/2.90  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.73/2.90  cnf(c91,plain,iext(uri_rdfs_range,uri_rdfs_member,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_member_range])).
% 2.73/2.90  cnf(c264,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X212)|icext(X212,uri_rdfs_member),inference(resolution,[status(thm)],[c73, c91])).
% 2.73/2.90  cnf(c263,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X210)|icext(X210,uri_rdfs_range),inference(resolution,[status(thm)],[c73, c48])).
% 2.73/2.90  cnf(c390,plain,~iext(uri_rdfs_domain,uri_rdf_type,X208)|icext(X208,X209),inference(resolution,[status(thm)],[c384, c73])).
% 2.73/2.90  cnf(c262,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X204)|icext(X204,uri_rdf_value),inference(resolution,[status(thm)],[c73, c4])).
% 2.73/2.90  cnf(c261,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X199)|icext(X199,uri_rdfs_domain),inference(factor,[status(thm)],[c73])).
% 2.73/2.90  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.73/2.90  cnf(c49,plain,iext(uri_rdf_type,uri_rdf_Property,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_property_type])).
% 2.73/2.90  cnf(c258,plain,~iext(uri_rdfs_range,uri_rdf_type,X194)|icext(X194,uri_rdfs_Class),inference(resolution,[status(thm)],[c47, c49])).
% 2.73/2.90  cnf(c36,plain,~iext(uri_rdfs_subClassOf,X76,X75)|~icext(X76,X74)|icext(X75,X74),inference(split_conjunct,[status(thm)],[c33])).
% 2.73/2.90  cnf(c315,plain,~icext(uri_rdf_Alt,X179)|icext(uri_rdfs_Container,X179),inference(resolution,[status(thm)],[c98, c36])).
% 2.73/2.90  cnf(c305,plain,~icext(uri_rdf_Bag,X178)|icext(uri_rdfs_Container,X178),inference(resolution,[status(thm)],[c97, c36])).
% 2.73/2.90  cnf(c249,plain,~iext(uri_rdfs_range,uri_rdfs_range,X171)|icext(X171,uri_rdf_Property),inference(resolution,[status(thm)],[c47, c14])).
% 2.73/2.90  cnf(c247,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X169)|icext(X169,uri_rdfs_Class),inference(resolution,[status(thm)],[c47, c75])).
% 2.73/2.90  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.73/2.90  cnf(c79,plain,iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Datatype),inference(split_conjunct,[status(thm)],[rdfs_dat_xmlliteral_type])).
% 2.73/2.90  cnf(c243,plain,~iext(uri_rdfs_range,uri_rdf_type,X165)|icext(X165,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c47, c79])).
% 2.73/2.90  cnf(c1019,plain,icext(uri_rdf_Property,uri_rdfs_member),inference(resolution,[status(thm)],[c739, c110])).
% 2.73/2.90  cnf(c239,plain,~iext(uri_rdfs_range,uri_rdfs_range,X161)|icext(X161,uri_rdfs_Class),inference(resolution,[status(thm)],[c47, c68])).
% 2.73/2.90  cnf(c990,plain,icext(uri_rdf_Property,uri_ex_p),inference(resolution,[status(thm)],[c548, c110])).
% 2.73/2.90  cnf(c238,plain,~iext(uri_rdfs_range,uri_ex_p,X160)|icext(X160,uri_ex_o),inference(resolution,[status(thm)],[c47, c0])).
% 2.73/2.90  cnf(c237,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X159)|icext(X159,uri_rdfs_Container),inference(resolution,[status(thm)],[c47, c81])).
% 2.73/2.90  cnf(c974,plain,icext(uri_rdf_Property,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c546, c110])).
% 2.73/2.90  cnf(c941,plain,icext(uri_rdf_Property,uri_rdfs_domain),inference(resolution,[status(thm)],[c544, c110])).
% 2.73/2.90  cnf(c233,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X155)|icext(X155,uri_rdf_Property),inference(resolution,[status(thm)],[c47, c93])).
% 2.73/2.90  cnf(c914,plain,icext(uri_rdf_Property,uri_rdfs_range),inference(resolution,[status(thm)],[c542, c110])).
% 2.73/2.90  cnf(c231,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X153)|icext(X153,uri_rdfs_Class),inference(resolution,[status(thm)],[c47, c37])).
% 2.73/2.90  cnf(c895,plain,icext(uri_rdf_Property,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c540, c110])).
% 2.73/2.90  cnf(c229,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X151)|icext(X151,uri_rdfs_Literal),inference(resolution,[status(thm)],[c47, c80])).
% 2.73/2.90  cnf(c228,plain,~iext(uri_rdfs_range,uri_rdf_type,X150)|icext(X150,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c47, c84])).
% 2.73/2.90  cnf(c227,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X149)|icext(X149,uri_rdfs_Resource),inference(resolution,[status(thm)],[c47, c92])).
% 2.73/2.90  cnf(c225,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X147)|icext(X147,uri_rdf_Property),inference(resolution,[status(thm)],[c47, c48])).
% 2.73/2.90  cnf(c224,plain,~iext(uri_rdfs_range,uri_rdfs_range,X146)|icext(X146,uri_rdfs_Resource),inference(resolution,[status(thm)],[c47, c4])).
% 2.73/2.90  cnf(c223,plain,~iext(uri_rdfs_range,uri_rdfs_range,X145)|icext(X145,X145),inference(factor,[status(thm)],[c47])).
% 2.73/2.90  cnf(c219,plain,~icext(uri_rdfs_Datatype,X144)|icext(uri_rdfs_Class,X144),inference(resolution,[status(thm)],[c36, c75])).
% 2.73/2.90  cnf(c218,plain,~icext(uri_rdfs_Seq,X143)|icext(uri_rdfs_Container,X143),inference(resolution,[status(thm)],[c36, c81])).
% 2.73/2.90  cnf(c836,plain,icext(uri_rdf_Property,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c429, c110])).
% 2.73/2.90  cnf(c217,plain,~icext(uri_rdfs_ContainerMembershipProperty,X142)|icext(uri_rdf_Property,X142),inference(resolution,[status(thm)],[c36, c93])).
% 2.73/2.90  cnf(c829,plain,icext(uri_rdf_Property,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c428, c110])).
% 2.73/2.90  cnf(c216,plain,~icext(uri_rdf_XMLLiteral,X141)|icext(uri_rdfs_Literal,X141),inference(resolution,[status(thm)],[c36, c80])).
% 2.73/2.90  cnf(c190,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X140)|iext(X140,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),inference(resolution,[status(thm)],[c93, c21])).
% 2.73/2.90  cnf(c189,plain,~iext(uri_rdfs_subClassOf,X139,uri_rdfs_ContainerMembershipProperty)|iext(uri_rdfs_subClassOf,X139,uri_rdf_Property),inference(resolution,[status(thm)],[c93, c25])).
% 2.73/2.90  cnf(c188,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X138)|iext(X138,uri_rdfs_member,uri_rdfs_Resource),inference(resolution,[status(thm)],[c92, c21])).
% 2.73/2.90  cnf(c187,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X137)|iext(X137,uri_rdfs_member,uri_rdfs_Resource),inference(resolution,[status(thm)],[c91, c21])).
% 2.73/2.90  cnf(c186,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X136)|iext(X136,uri_rdf__1,uri_rdfs_Resource),inference(resolution,[status(thm)],[c90, c21])).
% 2.73/2.90  cnf(c185,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X135)|iext(X135,uri_rdf__2,uri_rdfs_Resource),inference(resolution,[status(thm)],[c89, c21])).
% 2.73/2.90  cnf(c184,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X134)|iext(X134,uri_rdf__3,uri_rdfs_Resource),inference(resolution,[status(thm)],[c88, c21])).
% 2.73/2.90  cnf(c183,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X133)|iext(X133,uri_rdf__1,uri_rdfs_Resource),inference(resolution,[status(thm)],[c87, c21])).
% 2.73/2.90  cnf(c182,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X132)|iext(X132,uri_rdf__2,uri_rdfs_Resource),inference(resolution,[status(thm)],[c86, c21])).
% 2.73/2.90  cnf(c181,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X131)|iext(X131,uri_rdf__3,uri_rdfs_Resource),inference(resolution,[status(thm)],[c85, c21])).
% 2.73/2.90  cnf(c180,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X130)|iext(X130,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c84, c21])).
% 2.73/2.90  cnf(c179,plain,~iext(uri_rdfs_subClassOf,X129,uri_rdfs_Datatype)|iext(uri_rdfs_subClassOf,X129,uri_rdfs_Class),inference(resolution,[status(thm)],[c25, c75])).
% 2.73/2.90  cnf(c178,plain,~iext(uri_rdfs_subClassOf,X128,uri_rdfs_Seq)|iext(uri_rdfs_subClassOf,X128,uri_rdfs_Container),inference(resolution,[status(thm)],[c25, c81])).
% 2.73/2.90  cnf(c177,plain,~iext(uri_rdfs_subClassOf,X127,uri_rdf_XMLLiteral)|iext(uri_rdfs_subClassOf,X127,uri_rdfs_Literal),inference(resolution,[status(thm)],[c25, c80])).
% 2.73/2.90  cnf(c175,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X125)|iext(X125,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c83, c21])).
% 2.73/2.90  cnf(c174,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X124)|iext(X124,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c82, c21])).
% 2.73/2.90  cnf(c173,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X123)|iext(X123,uri_rdfs_Seq,uri_rdfs_Container),inference(resolution,[status(thm)],[c81, c21])).
% 2.73/2.90  cnf(c172,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X122)|iext(X122,uri_rdf_XMLLiteral,uri_rdfs_Literal),inference(resolution,[status(thm)],[c80, c21])).
% 2.73/2.90  cnf(c171,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X121)|iext(X121,uri_rdf_XMLLiteral,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c79, c21])).
% 2.73/2.90  cnf(c170,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X120)|iext(X120,uri_rdf_Property,uri_rdfs_Class),inference(resolution,[status(thm)],[c21, c49])).
% 2.73/2.90  cnf(c169,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X119)|iext(X119,uri_rdf_type,uri_rdfs_Resource),inference(resolution,[status(thm)],[c21, c7])).
% 2.73/2.90  cnf(c168,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X118)|iext(X118,uri_rdfs_subClassOf,uri_rdfs_Class),inference(resolution,[status(thm)],[c21, c37])).
% 2.73/2.90  cnf(c167,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X117)|iext(X117,uri_rdf_value,uri_rdfs_Resource),inference(resolution,[status(thm)],[c21, c5])).
% 2.73/2.90  cnf(c166,plain,~iext(uri_rdfs_subPropertyOf,uri_ex_p,X116)|iext(X116,uri_ex_s,uri_ex_o),inference(resolution,[status(thm)],[c21, c0])).
% 2.73/2.90  cnf(c165,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X115)|iext(X115,uri_rdfs_Datatype,uri_rdfs_Class),inference(resolution,[status(thm)],[c21, c75])).
% 2.73/2.90  cnf(c164,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X114)|iext(X114,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c21, c22])).
% 2.73/2.90  cnf(c163,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X113)|iext(X113,uri_rdf_type,uri_rdfs_Class),inference(resolution,[status(thm)],[c21, c6])).
% 2.73/2.90  cnf(c162,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X112)|iext(X112,uri_rdf_subject,uri_rdfs_Statement),inference(resolution,[status(thm)],[c21, c39])).
% 2.73/2.90  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.73/2.90  cnf(c74,plain,iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_domain_domain])).
% 2.73/2.90  cnf(c161,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X111)|iext(X111,uri_rdfs_domain,uri_rdf_Property),inference(resolution,[status(thm)],[c21, c74])).
% 2.73/2.90  cnf(c475,plain,icext(uri_rdf_Property,uri_rdf_first),inference(resolution,[status(thm)],[c137, c110])).
% 2.73/2.90  cnf(c160,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X110)|iext(X110,uri_rdfs_range,uri_rdfs_Class),inference(resolution,[status(thm)],[c21, c44])).
% 2.73/2.90  cnf(c159,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X109)|iext(X109,uri_rdfs_range,uri_rdf_Property),inference(resolution,[status(thm)],[c21, c48])).
% 2.73/2.90  cnf(c158,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X108)|iext(X108,uri_rdf_object,uri_rdfs_Statement),inference(resolution,[status(thm)],[c21, c43])).
% 2.73/2.90  cnf(c157,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X107)|iext(X107,uri_rdf_value,uri_rdfs_Resource),inference(resolution,[status(thm)],[c21, c4])).
% 2.73/2.90  cnf(c156,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X106)|iext(X106,uri_rdfs_subClassOf,uri_rdfs_Class),inference(resolution,[status(thm)],[c21, c29])).
% 2.73/2.90  cnf(c155,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X105)|iext(X105,uri_rdf_predicate,uri_rdfs_Resource),inference(resolution,[status(thm)],[c21, c40])).
% 2.73/2.90  cnf(c154,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X104)|iext(X104,uri_rdf_predicate,uri_rdfs_Statement),inference(resolution,[status(thm)],[c21, c41])).
% 2.73/2.90  cnf(c153,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X103)|iext(X103,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c21, c14])).
% 2.73/2.90  cnf(c152,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X102)|iext(X102,uri_rdf_subject,uri_rdfs_Resource),inference(resolution,[status(thm)],[c21, c38])).
% 2.73/2.90  cnf(c151,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X101)|iext(X101,uri_rdfs_domain,uri_rdfs_Class),inference(resolution,[status(thm)],[c21, c68])).
% 2.73/2.90  cnf(c150,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X100)|iext(X100,uri_rdfs_subPropertyOf,X100),inference(factor,[status(thm)],[c21])).
% 2.73/2.90  cnf(c470,plain,icext(uri_rdf_List,uri_rdf_nil),inference(resolution,[status(thm)],[c136, c110])).
% 2.73/2.90  cnf(c462,plain,icext(uri_rdf_Property,uri_rdf_rest),inference(resolution,[status(thm)],[c135, c110])).
% 2.73/2.90  cnf(c454,plain,icext(uri_rdf_Property,uri_rdf__1),inference(resolution,[status(thm)],[c134, c110])).
% 2.73/2.90  cnf(c446,plain,icext(uri_rdf_Property,uri_rdf__2),inference(resolution,[status(thm)],[c133, c110])).
% 2.73/2.90  cnf(c438,plain,icext(uri_rdf_Property,uri_rdf__3),inference(resolution,[status(thm)],[c132, c110])).
% 2.73/2.90  cnf(c425,plain,icext(uri_rdf_Property,uri_rdf_object),inference(resolution,[status(thm)],[c131, c110])).
% 2.73/2.90  cnf(c414,plain,icext(uri_rdf_Property,uri_rdf_value),inference(resolution,[status(thm)],[c130, c110])).
% 2.73/2.90  cnf(c409,plain,icext(uri_rdf_Property,uri_rdf_subject),inference(resolution,[status(thm)],[c129, c110])).
% 2.73/2.90  cnf(c404,plain,icext(uri_rdf_Property,uri_rdf_type),inference(resolution,[status(thm)],[c121, c110])).
% 2.73/2.91  cnf(c366,plain,icext(uri_rdfs_Datatype,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c110, c79])).
% 2.73/2.91  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.73/2.91  fof(c76,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.73/2.91  fof(c77,plain,(![X31]:(~icext(uri_rdfs_Datatype,X31)|iext(uri_rdfs_subClassOf,X31,uri_rdfs_Literal))),inference(variable_rename,[status(thm)],[c76])).
% 2.73/2.91  cnf(c78,plain,~icext(uri_rdfs_Datatype,X85)|iext(uri_rdfs_subClassOf,X85,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[c77])).
% 2.73/2.91  cnf(c210,plain,icext(uri_rdfs_Class,uri_rdf_Property),inference(resolution,[status(thm)],[c205, c66])).
% 2.73/2.91  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.73/2.91  fof(c50,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.73/2.91  fof(c51,plain,((![X]:(~lv(X)|icext(uri_rdfs_Literal,X)))&(![X]:(~icext(uri_rdfs_Literal,X)|lv(X)))),inference(shift_quantors,[status(thm)],[c50])).
% 2.73/2.91  fof(c53,plain,(![X21]:(![X22]:((~lv(X21)|icext(uri_rdfs_Literal,X21))&(~icext(uri_rdfs_Literal,X22)|lv(X22))))),inference(shift_quantors,[status(thm)],[fof(c52,plain,((![X21]:(~lv(X21)|icext(uri_rdfs_Literal,X21)))&(![X22]:(~icext(uri_rdfs_Literal,X22)|lv(X22)))),inference(variable_rename,[status(thm)],[c51])).])).
% 2.73/2.91  cnf(c55,plain,~icext(uri_rdfs_Literal,X54)|lv(X54),inference(split_conjunct,[status(thm)],[c53])).
% 2.73/2.91  cnf(c54,plain,~lv(X53)|icext(uri_rdfs_Literal,X53),inference(split_conjunct,[status(thm)],[c53])).
% 2.73/2.91  fof(testcase_conclusion_fullish_005_Everything_is_a_Resource,conjecture,(((((((iext(uri_rdf_type,uri_ex_s,uri_rdfs_Resource)&iext(uri_rdf_type,uri_ex_s,uri_owl_Thing))&iext(uri_rdf_type,uri_ex_p,uri_rdfs_Resource))&iext(uri_rdf_type,uri_ex_p,uri_owl_Thing))&iext(uri_rdf_type,uri_ex_p,uri_rdf_Property))&iext(uri_rdf_type,uri_ex_p,uri_owl_ObjectProperty))&iext(uri_rdf_type,uri_ex_o,uri_rdfs_Resource))&iext(uri_rdf_type,uri_ex_o,uri_owl_Thing)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', testcase_conclusion_fullish_005_Everything_is_a_Resource)).
% 2.73/2.91  fof(c1,negated_conjecture,(~(((((((iext(uri_rdf_type,uri_ex_s,uri_rdfs_Resource)&iext(uri_rdf_type,uri_ex_s,uri_owl_Thing))&iext(uri_rdf_type,uri_ex_p,uri_rdfs_Resource))&iext(uri_rdf_type,uri_ex_p,uri_owl_Thing))&iext(uri_rdf_type,uri_ex_p,uri_rdf_Property))&iext(uri_rdf_type,uri_ex_p,uri_owl_ObjectProperty))&iext(uri_rdf_type,uri_ex_o,uri_rdfs_Resource))&iext(uri_rdf_type,uri_ex_o,uri_owl_Thing))),inference(assume_negation,[status(cth)],[testcase_conclusion_fullish_005_Everything_is_a_Resource])).
% 2.73/2.91  fof(c2,negated_conjecture,(((((((~iext(uri_rdf_type,uri_ex_s,uri_rdfs_Resource)|~iext(uri_rdf_type,uri_ex_s,uri_owl_Thing))|~iext(uri_rdf_type,uri_ex_p,uri_rdfs_Resource))|~iext(uri_rdf_type,uri_ex_p,uri_owl_Thing))|~iext(uri_rdf_type,uri_ex_p,uri_rdf_Property))|~iext(uri_rdf_type,uri_ex_p,uri_owl_ObjectProperty))|~iext(uri_rdf_type,uri_ex_o,uri_rdfs_Resource))|~iext(uri_rdf_type,uri_ex_o,uri_owl_Thing)),inference(fof_nnf,[status(thm)],[c1])).
% 2.73/2.91  cnf(c3,negated_conjecture,~iext(uri_rdf_type,uri_ex_s,uri_rdfs_Resource)|~iext(uri_rdf_type,uri_ex_s,uri_owl_Thing)|~iext(uri_rdf_type,uri_ex_p,uri_rdfs_Resource)|~iext(uri_rdf_type,uri_ex_p,uri_owl_Thing)|~iext(uri_rdf_type,uri_ex_p,uri_rdf_Property)|~iext(uri_rdf_type,uri_ex_p,uri_owl_ObjectProperty)|~iext(uri_rdf_type,uri_ex_o,uri_rdfs_Resource)|~iext(uri_rdf_type,uri_ex_o,uri_owl_Thing),inference(split_conjunct,[status(thm)],[c2])).
% 2.73/2.91  % SZS output end Saturation
% 2.73/2.91  
% 2.73/2.91  % Initial clauses    : 91
% 2.73/2.91  % Processed clauses  : 515
% 2.73/2.91  % Factors computed   : 5
% 2.73/2.91  % Resolvents computed: 1205
% 2.73/2.91  % Tautologies deleted: 48
% 2.73/2.91  % Forward subsumed   : 738
% 2.73/2.91  % Backward subsumed  : 1
% 2.73/2.91  % -------- CPU Time ---------
% 2.73/2.91  % User time          : 2.535 s
% 2.73/2.91  % System time        : 0.017 s
% 2.73/2.91  % Total time         : 2.552 s
%------------------------------------------------------------------------------