PyRes---1.5.SAT-Sat.s

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

% Result   : Satisfiable 3.19s 3.39s
% Output   : Saturation 3.19s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13  % Problem  : SWB019+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:12:53 EDT 2024
% 0.13/0.35  % CPUTime  : 
% 3.19/3.39  % Version:  1.5
% 3.19/3.39  % SZS status Satisfiable
% 3.19/3.39  % SZS output start Saturation
% 3.19/3.39  fof(rdfs_subpropertyof_main,axiom,(![P]:(![Q]:(iext(uri_rdfs_subPropertyOf,P,Q)=>((ip(P)&ip(Q))&(![X]:(![Y]:(iext(P,X,Y)=>iext(Q,X,Y)))))))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_subpropertyof_main)).
% 3.19/3.39  fof(c18,plain,(![P]:(![Q]:(~iext(uri_rdfs_subPropertyOf,P,Q)|((ip(P)&ip(Q))&(![X]:(![Y]:(~iext(P,X,Y)|iext(Q,X,Y)))))))),inference(fof_nnf,[status(thm)],[rdfs_subpropertyof_main])).
% 3.19/3.39  fof(c20,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(c19,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)],[c18])).])).
% 3.19/3.39  fof(c21,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)],[c20])).
% 3.19/3.39  cnf(c24,plain,~iext(uri_rdfs_subPropertyOf,X62,X63)|~iext(X62,X65,X64)|iext(X63,X65,X64),inference(split_conjunct,[status(thm)],[c21])).
% 3.19/3.39  fof(rdfs_cext_def,axiom,(![X]:(![C]:(iext(uri_rdf_type,X,C)<=>icext(C,X)))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_cext_def)).
% 3.19/3.39  fof(c109,plain,(![X]:(![C]:((~iext(uri_rdf_type,X,C)|icext(C,X))&(~icext(C,X)|iext(uri_rdf_type,X,C))))),inference(fof_nnf,[status(thm)],[rdfs_cext_def])).
% 3.19/3.39  fof(c110,plain,((![X]:(![C]:(~iext(uri_rdf_type,X,C)|icext(C,X))))&(![X]:(![C]:(~icext(C,X)|iext(uri_rdf_type,X,C))))),inference(shift_quantors,[status(thm)],[c109])).
% 3.19/3.39  fof(c112,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(c111,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)],[c110])).])).
% 3.19/3.39  cnf(c114,plain,~icext(X91,X90)|iext(uri_rdf_type,X90,X91),inference(split_conjunct,[status(thm)],[c112])).
% 3.19/3.39  fof(rdfs_annotation_label_range,axiom,iext(uri_rdfs_range,uri_rdfs_label,uri_rdfs_Literal),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_label_range)).
% 3.19/3.39  cnf(c117,plain,iext(uri_rdfs_range,uri_rdfs_label,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[rdfs_annotation_label_range])).
% 3.19/3.39  fof(rdfs_range_main,axiom,(![P]:(![C]:(![X]:(![Y]:((iext(uri_rdfs_range,P,C)&iext(P,X,Y))=>icext(C,Y)))))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_range_main)).
% 3.19/3.39  fof(c48,plain,(![P]:(![C]:(![X]:(![Y]:((~iext(uri_rdfs_range,P,C)|~iext(P,X,Y))|icext(C,Y)))))),inference(fof_nnf,[status(thm)],[rdfs_range_main])).
% 3.19/3.39  fof(c49,plain,(![X17]:(![X18]:(![X19]:(![X20]:((~iext(uri_rdfs_range,X17,X18)|~iext(X17,X19,X20))|icext(X18,X20)))))),inference(variable_rename,[status(thm)],[c48])).
% 3.19/3.39  cnf(c50,plain,~iext(uri_rdfs_range,X80,X78)|~iext(X80,X79,X77)|icext(X78,X77),inference(split_conjunct,[status(thm)],[c49])).
% 3.19/3.39  fof(testcase_premise_fullish_019_Disjoint_Annotation_Properties,axiom,((((((iext(uri_rdf_type,uri_skos_prefLabel,uri_owl_AnnotationProperty)&iext(uri_rdfs_subPropertyOf,uri_skos_prefLabel,uri_rdfs_label))&iext(uri_rdf_type,uri_skos_altLabel,uri_owl_AnnotationProperty))&iext(uri_rdfs_subPropertyOf,uri_skos_altLabel,uri_rdfs_label))&iext(uri_owl_propertyDisjointWith,uri_skos_prefLabel,uri_skos_altLabel))&iext(uri_skos_prefLabel,uri_ex_foo,literal_plain(dat_str_foo)))&iext(uri_skos_altLabel,uri_ex_foo,literal_plain(dat_str_foo))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', testcase_premise_fullish_019_Disjoint_Annotation_Properties)).
% 3.19/3.39  cnf(c1,plain,iext(uri_rdfs_subPropertyOf,uri_skos_prefLabel,uri_rdfs_label),inference(split_conjunct,[status(thm)],[testcase_premise_fullish_019_Disjoint_Annotation_Properties])).
% 3.19/3.39  cnf(c5,plain,iext(uri_skos_prefLabel,uri_ex_foo,literal_plain(dat_str_foo)),inference(split_conjunct,[status(thm)],[testcase_premise_fullish_019_Disjoint_Annotation_Properties])).
% 3.19/3.39  cnf(c177,plain,~iext(uri_rdfs_subPropertyOf,uri_skos_prefLabel,X117)|iext(X117,uri_ex_foo,literal_plain(dat_str_foo)),inference(resolution,[status(thm)],[c24, c5])).
% 3.19/3.39  cnf(c689,plain,iext(uri_rdfs_label,uri_ex_foo,literal_plain(dat_str_foo)),inference(resolution,[status(thm)],[c177, c1])).
% 3.19/3.39  cnf(c1181,plain,~iext(uri_rdfs_range,uri_rdfs_label,X627)|icext(X627,literal_plain(dat_str_foo)),inference(resolution,[status(thm)],[c689, c50])).
% 3.19/3.39  cnf(c1475,plain,icext(uri_rdfs_Literal,literal_plain(dat_str_foo)),inference(resolution,[status(thm)],[c1181, c117])).
% 3.19/3.39  cnf(c1476,plain,iext(uri_rdf_type,literal_plain(dat_str_foo),uri_rdfs_Literal),inference(resolution,[status(thm)],[c1475, c114])).
% 3.19/3.39  cnf(c1480,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X642)|iext(X642,literal_plain(dat_str_foo),uri_rdfs_Literal),inference(resolution,[status(thm)],[c1476, c24])).
% 3.19/3.39  fof(rdfs_subpropertyof_reflex,axiom,(![P]:(ip(P)=>iext(uri_rdfs_subPropertyOf,P,P))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_subpropertyof_reflex)).
% 3.19/3.39  fof(c14,plain,(![P]:(~ip(P)|iext(uri_rdfs_subPropertyOf,P,P))),inference(fof_nnf,[status(thm)],[rdfs_subpropertyof_reflex])).
% 3.19/3.39  fof(c15,plain,(![X5]:(~ip(X5)|iext(uri_rdfs_subPropertyOf,X5,X5))),inference(variable_rename,[status(thm)],[c14])).
% 3.19/3.39  cnf(c16,plain,~ip(X52)|iext(uri_rdfs_subPropertyOf,X52,X52),inference(split_conjunct,[status(thm)],[c15])).
% 3.19/3.39  fof(rdf_type_ip,axiom,(![P]:(iext(uri_rdf_type,P,uri_rdf_Property)<=>ip(P))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdf_type_ip)).
% 3.19/3.39  fof(c126,plain,(![P]:((~iext(uri_rdf_type,P,uri_rdf_Property)|ip(P))&(~ip(P)|iext(uri_rdf_type,P,uri_rdf_Property)))),inference(fof_nnf,[status(thm)],[rdf_type_ip])).
% 3.19/3.39  fof(c127,plain,((![P]:(~iext(uri_rdf_type,P,uri_rdf_Property)|ip(P)))&(![P]:(~ip(P)|iext(uri_rdf_type,P,uri_rdf_Property)))),inference(shift_quantors,[status(thm)],[c126])).
% 3.19/3.39  fof(c129,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(c128,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)],[c127])).])).
% 3.19/3.39  cnf(c130,plain,~iext(uri_rdf_type,X94,uri_rdf_Property)|ip(X94),inference(split_conjunct,[status(thm)],[c129])).
% 3.19/3.39  fof(rdfs_range_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_range,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_range_domain)).
% 3.19/3.39  cnf(c51,plain,iext(uri_rdfs_domain,uri_rdfs_range,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_range_domain])).
% 3.19/3.39  fof(rdfs_domain_main,axiom,(![P]:(![C]:(![X]:(![Y]:((iext(uri_rdfs_domain,P,C)&iext(P,X,Y))=>icext(C,X)))))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_domain_main)).
% 3.19/3.39  fof(c72,plain,(![P]:(![C]:(![X]:(![Y]:((~iext(uri_rdfs_domain,P,C)|~iext(P,X,Y))|icext(C,X)))))),inference(fof_nnf,[status(thm)],[rdfs_domain_main])).
% 3.19/3.39  fof(c73,plain,(![P]:(![C]:(![X]:((~iext(uri_rdfs_domain,P,C)|(![Y]:~iext(P,X,Y)))|icext(C,X))))),inference(shift_quantors,[status(thm)],[c72])).
% 3.19/3.39  fof(c75,plain,(![X27]:(![X28]:(![X29]:(![X30]:((~iext(uri_rdfs_domain,X27,X28)|~iext(X27,X29,X30))|icext(X28,X29)))))),inference(shift_quantors,[status(thm)],[fof(c74,plain,(![X27]:(![X28]:(![X29]:((~iext(uri_rdfs_domain,X27,X28)|(![X30]:~iext(X27,X29,X30)))|icext(X28,X29))))),inference(variable_rename,[status(thm)],[c73])).])).
% 3.19/3.39  cnf(c76,plain,~iext(uri_rdfs_domain,X82,X81)|~iext(X82,X84,X83)|icext(X81,X84),inference(split_conjunct,[status(thm)],[c75])).
% 3.19/3.39  fof(rdfs_annotation_comment_range,axiom,iext(uri_rdfs_range,uri_rdfs_comment,uri_rdfs_Literal),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_comment_range)).
% 3.19/3.39  cnf(c122,plain,iext(uri_rdfs_range,uri_rdfs_comment,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[rdfs_annotation_comment_range])).
% 3.19/3.39  cnf(c429,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X310)|icext(X310,uri_rdfs_comment),inference(resolution,[status(thm)],[c122, c76])).
% 3.19/3.39  cnf(c1290,plain,icext(uri_rdf_Property,uri_rdfs_comment),inference(resolution,[status(thm)],[c429, c51])).
% 3.19/3.39  cnf(c1291,plain,iext(uri_rdf_type,uri_rdfs_comment,uri_rdf_Property),inference(resolution,[status(thm)],[c1290, c114])).
% 3.19/3.39  cnf(c1292,plain,ip(uri_rdfs_comment),inference(resolution,[status(thm)],[c1291, c130])).
% 3.19/3.39  cnf(c1300,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_comment,uri_rdfs_comment),inference(resolution,[status(thm)],[c1292, c16])).
% 3.19/3.39  cnf(c1303,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X640)|iext(X640,uri_rdfs_comment,uri_rdfs_comment),inference(resolution,[status(thm)],[c1300, c24])).
% 3.19/3.39  cnf(c1293,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X638)|iext(X638,uri_rdfs_comment,uri_rdf_Property),inference(resolution,[status(thm)],[c1291, c24])).
% 3.19/3.39  fof(rdfs_reification_predicate_range,axiom,iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_reification_predicate_range)).
% 3.19/3.39  cnf(c43,plain,iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_reification_predicate_range])).
% 3.19/3.39  cnf(c335,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X269)|icext(X269,uri_rdf_predicate),inference(resolution,[status(thm)],[c76, c43])).
% 3.19/3.39  cnf(c1243,plain,icext(uri_rdf_Property,uri_rdf_predicate),inference(resolution,[status(thm)],[c335, c51])).
% 3.19/3.39  cnf(c1244,plain,iext(uri_rdf_type,uri_rdf_predicate,uri_rdf_Property),inference(resolution,[status(thm)],[c1243, c114])).
% 3.19/3.39  cnf(c1245,plain,ip(uri_rdf_predicate),inference(resolution,[status(thm)],[c1244, c130])).
% 3.19/3.39  cnf(c1252,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_predicate,uri_rdf_predicate),inference(resolution,[status(thm)],[c1245, c16])).
% 3.19/3.39  cnf(c1255,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X637)|iext(X637,uri_rdf_predicate,uri_rdf_predicate),inference(resolution,[status(thm)],[c1252, c24])).
% 3.19/3.39  cnf(c1246,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X635)|iext(X635,uri_rdf_predicate,uri_rdf_Property),inference(resolution,[status(thm)],[c1244, c24])).
% 3.19/3.39  fof(rdfs_subclassof_reflex,axiom,(![C]:(ic(C)=>iext(uri_rdfs_subClassOf,C,C))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_subclassof_reflex)).
% 3.19/3.39  fof(c29,plain,(![C]:(~ic(C)|iext(uri_rdfs_subClassOf,C,C))),inference(fof_nnf,[status(thm)],[rdfs_subclassof_reflex])).
% 3.19/3.39  fof(c30,plain,(![X13]:(~ic(X13)|iext(uri_rdfs_subClassOf,X13,X13))),inference(variable_rename,[status(thm)],[c29])).
% 3.19/3.39  cnf(c31,plain,~ic(X69)|iext(uri_rdfs_subClassOf,X69,X69),inference(split_conjunct,[status(thm)],[c30])).
% 3.19/3.39  fof(rdfs_ic_def,axiom,(![X]:(ic(X)<=>icext(uri_rdfs_Class,X))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_ic_def)).
% 3.19/3.39  fof(c65,plain,(![X]:((~ic(X)|icext(uri_rdfs_Class,X))&(~icext(uri_rdfs_Class,X)|ic(X)))),inference(fof_nnf,[status(thm)],[rdfs_ic_def])).
% 3.19/3.39  fof(c66,plain,((![X]:(~ic(X)|icext(uri_rdfs_Class,X)))&(![X]:(~icext(uri_rdfs_Class,X)|ic(X)))),inference(shift_quantors,[status(thm)],[c65])).
% 3.19/3.39  fof(c68,plain,(![X25]:(![X26]:((~ic(X25)|icext(uri_rdfs_Class,X25))&(~icext(uri_rdfs_Class,X26)|ic(X26))))),inference(shift_quantors,[status(thm)],[fof(c67,plain,((![X25]:(~ic(X25)|icext(uri_rdfs_Class,X25)))&(![X26]:(~icext(uri_rdfs_Class,X26)|ic(X26)))),inference(variable_rename,[status(thm)],[c66])).])).
% 3.19/3.39  cnf(c70,plain,~icext(uri_rdfs_Class,X57)|ic(X57),inference(split_conjunct,[status(thm)],[c68])).
% 3.19/3.39  fof(rdfs_domain_range,axiom,iext(uri_rdfs_range,uri_rdfs_domain,uri_rdfs_Class),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_domain_range)).
% 3.19/3.39  cnf(c71,plain,iext(uri_rdfs_range,uri_rdfs_domain,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_domain_range])).
% 3.19/3.39  fof(rdfs_reification_subject_domain,axiom,iext(uri_rdfs_domain,uri_rdf_subject,uri_rdfs_Statement),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_reification_subject_domain)).
% 3.19/3.39  cnf(c42,plain,iext(uri_rdfs_domain,uri_rdf_subject,uri_rdfs_Statement),inference(split_conjunct,[status(thm)],[rdfs_reification_subject_domain])).
% 3.19/3.39  cnf(c285,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X214)|icext(X214,uri_rdfs_Statement),inference(resolution,[status(thm)],[c50, c42])).
% 3.19/3.39  cnf(c1187,plain,icext(uri_rdfs_Class,uri_rdfs_Statement),inference(resolution,[status(thm)],[c285, c71])).
% 3.19/3.39  cnf(c1188,plain,ic(uri_rdfs_Statement),inference(resolution,[status(thm)],[c1187, c70])).
% 3.19/3.39  cnf(c1192,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Statement,uri_rdfs_Statement),inference(resolution,[status(thm)],[c1188, c31])).
% 3.19/3.39  cnf(c1208,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X633)|iext(X633,uri_rdfs_Statement,uri_rdfs_Statement),inference(resolution,[status(thm)],[c1192, c24])).
% 3.19/3.39  fof(rdfs_subclassof_trans,axiom,(![C]:(![D]:(![E]:((iext(uri_rdfs_subClassOf,C,D)&iext(uri_rdfs_subClassOf,D,E))=>iext(uri_rdfs_subClassOf,C,E))))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_subclassof_trans)).
% 3.19/3.39  fof(c26,plain,(![C]:(![D]:(![E]:((~iext(uri_rdfs_subClassOf,C,D)|~iext(uri_rdfs_subClassOf,D,E))|iext(uri_rdfs_subClassOf,C,E))))),inference(fof_nnf,[status(thm)],[rdfs_subclassof_trans])).
% 3.19/3.39  fof(c27,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)],[c26])).
% 3.19/3.39  cnf(c28,plain,~iext(uri_rdfs_subClassOf,X67,X68)|~iext(uri_rdfs_subClassOf,X68,X66)|iext(uri_rdfs_subClassOf,X67,X66),inference(split_conjunct,[status(thm)],[c27])).
% 3.19/3.39  fof(rdfs_class_instsub_resource,axiom,(![C]:(ic(C)=>iext(uri_rdfs_subClassOf,C,uri_rdfs_Resource))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_class_instsub_resource)).
% 3.19/3.39  fof(c106,plain,(![C]:(~ic(C)|iext(uri_rdfs_subClassOf,C,uri_rdfs_Resource))),inference(fof_nnf,[status(thm)],[rdfs_class_instsub_resource])).
% 3.19/3.39  fof(c107,plain,(![X33]:(~ic(X33)|iext(uri_rdfs_subClassOf,X33,uri_rdfs_Resource))),inference(variable_rename,[status(thm)],[c106])).
% 3.19/3.39  cnf(c108,plain,~ic(X87)|iext(uri_rdfs_subClassOf,X87,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[c107])).
% 3.19/3.39  cnf(c1191,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Statement,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1188, c108])).
% 3.19/3.39  cnf(c1203,plain,~iext(uri_rdfs_subClassOf,X632,uri_rdfs_Statement)|iext(uri_rdfs_subClassOf,X632,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1191, c28])).
% 3.19/3.39  cnf(c1199,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X631)|iext(X631,uri_rdfs_Statement,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1191, c24])).
% 3.19/3.39  cnf(c1482,plain,~iext(uri_rdfs_range,uri_rdf_type,X630)|icext(X630,uri_rdfs_Literal),inference(resolution,[status(thm)],[c1476, c50])).
% 3.19/3.39  cnf(c1189,plain,iext(uri_rdf_type,uri_rdfs_Statement,uri_rdfs_Class),inference(resolution,[status(thm)],[c1187, c114])).
% 3.19/3.39  cnf(c1193,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X629)|iext(X629,uri_rdfs_Statement,uri_rdfs_Class),inference(resolution,[status(thm)],[c1189, c24])).
% 3.19/3.39  fof(rdfs_lv_def,axiom,(![X]:(lv(X)<=>icext(uri_rdfs_Literal,X))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_lv_def)).
% 3.19/3.39  fof(c53,plain,(![X]:((~lv(X)|icext(uri_rdfs_Literal,X))&(~icext(uri_rdfs_Literal,X)|lv(X)))),inference(fof_nnf,[status(thm)],[rdfs_lv_def])).
% 3.19/3.39  fof(c54,plain,((![X]:(~lv(X)|icext(uri_rdfs_Literal,X)))&(![X]:(~icext(uri_rdfs_Literal,X)|lv(X)))),inference(shift_quantors,[status(thm)],[c53])).
% 3.19/3.39  fof(c56,plain,(![X21]:(![X22]:((~lv(X21)|icext(uri_rdfs_Literal,X21))&(~icext(uri_rdfs_Literal,X22)|lv(X22))))),inference(shift_quantors,[status(thm)],[fof(c55,plain,((![X21]:(~lv(X21)|icext(uri_rdfs_Literal,X21)))&(![X22]:(~icext(uri_rdfs_Literal,X22)|lv(X22)))),inference(variable_rename,[status(thm)],[c54])).])).
% 3.19/3.39  cnf(c58,plain,~icext(uri_rdfs_Literal,X51)|lv(X51),inference(split_conjunct,[status(thm)],[c56])).
% 3.19/3.39  cnf(c1477,plain,lv(literal_plain(dat_str_foo)),inference(resolution,[status(thm)],[c1475, c58])).
% 3.19/3.39  cnf(c1183,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_label,X628)|iext(X628,uri_ex_foo,literal_plain(dat_str_foo)),inference(resolution,[status(thm)],[c689, c24])).
% 3.19/3.39  fof(rdfs_range_range,axiom,iext(uri_rdfs_range,uri_rdfs_range,uri_rdfs_Class),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_range_range)).
% 3.19/3.39  cnf(c47,plain,iext(uri_rdfs_range,uri_rdfs_range,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_range_range])).
% 3.19/3.39  fof(rdfs_collection_rest_range,axiom,iext(uri_rdfs_range,uri_rdf_rest,uri_rdf_List),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_collection_rest_range)).
% 3.19/3.39  cnf(c102,plain,iext(uri_rdfs_range,uri_rdf_rest,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdfs_collection_rest_range])).
% 3.19/3.39  cnf(c267,plain,~iext(uri_rdfs_range,uri_rdfs_range,X173)|icext(X173,uri_rdf_List),inference(resolution,[status(thm)],[c50, c102])).
% 3.19/3.39  cnf(c1130,plain,icext(uri_rdfs_Class,uri_rdf_List),inference(resolution,[status(thm)],[c267, c47])).
% 3.19/3.39  cnf(c1131,plain,ic(uri_rdf_List),inference(resolution,[status(thm)],[c1130, c70])).
% 3.19/3.39  cnf(c1135,plain,iext(uri_rdfs_subClassOf,uri_rdf_List,uri_rdf_List),inference(resolution,[status(thm)],[c1131, c31])).
% 3.19/3.39  cnf(c1179,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X626)|iext(X626,uri_rdf_List,uri_rdf_List),inference(resolution,[status(thm)],[c1135, c24])).
% 3.19/3.39  cnf(c1134,plain,iext(uri_rdfs_subClassOf,uri_rdf_List,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1131, c108])).
% 3.19/3.39  cnf(c1171,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X624)|iext(X624,uri_rdf_List,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1134, c24])).
% 3.19/3.39  cnf(c1167,plain,~iext(uri_rdfs_subClassOf,X623,uri_rdf_List)|iext(uri_rdfs_subClassOf,X623,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1134, c28])).
% 3.19/3.39  cnf(c1132,plain,iext(uri_rdf_type,uri_rdf_List,uri_rdfs_Class),inference(resolution,[status(thm)],[c1130, c114])).
% 3.19/3.39  cnf(c1163,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X622)|iext(X622,uri_rdf_List,uri_rdfs_Class),inference(resolution,[status(thm)],[c1132, c24])).
% 3.19/3.39  fof(rdfs_type_range,axiom,iext(uri_rdfs_range,uri_rdf_type,uri_rdfs_Class),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_type_range)).
% 3.19/3.39  cnf(c9,plain,iext(uri_rdfs_range,uri_rdf_type,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_type_range])).
% 3.19/3.39  cnf(c2,plain,iext(uri_rdf_type,uri_skos_altLabel,uri_owl_AnnotationProperty),inference(split_conjunct,[status(thm)],[testcase_premise_fullish_019_Disjoint_Annotation_Properties])).
% 3.19/3.39  cnf(c259,plain,~iext(uri_rdfs_range,uri_rdf_type,X165)|icext(X165,uri_owl_AnnotationProperty),inference(resolution,[status(thm)],[c50, c2])).
% 3.19/3.39  cnf(c1113,plain,icext(uri_rdfs_Class,uri_owl_AnnotationProperty),inference(resolution,[status(thm)],[c259, c9])).
% 3.19/3.39  cnf(c1115,plain,ic(uri_owl_AnnotationProperty),inference(resolution,[status(thm)],[c1113, c70])).
% 3.19/3.39  cnf(c1119,plain,iext(uri_rdfs_subClassOf,uri_owl_AnnotationProperty,uri_owl_AnnotationProperty),inference(resolution,[status(thm)],[c1115, c31])).
% 3.19/3.39  cnf(c1158,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X621)|iext(X621,uri_owl_AnnotationProperty,uri_owl_AnnotationProperty),inference(resolution,[status(thm)],[c1119, c24])).
% 3.19/3.39  cnf(c1118,plain,iext(uri_rdfs_subClassOf,uri_owl_AnnotationProperty,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1115, c108])).
% 3.19/3.39  cnf(c1150,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X619)|iext(X619,uri_owl_AnnotationProperty,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1118, c24])).
% 3.19/3.39  cnf(c1146,plain,~iext(uri_rdfs_subClassOf,X618,uri_owl_AnnotationProperty)|iext(uri_rdfs_subClassOf,X618,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1118, c28])).
% 3.19/3.39  cnf(c1116,plain,iext(uri_rdf_type,uri_owl_AnnotationProperty,uri_rdfs_Class),inference(resolution,[status(thm)],[c1113, c114])).
% 3.19/3.39  cnf(c1142,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X617)|iext(X617,uri_owl_AnnotationProperty,uri_rdfs_Class),inference(resolution,[status(thm)],[c1116, c24])).
% 3.19/3.39  cnf(c23,plain,~iext(uri_rdfs_subPropertyOf,X60,X61)|ip(X61),inference(split_conjunct,[status(thm)],[c21])).
% 3.19/3.39  fof(rdfs_container_containermembershipproperty_instsub_member,axiom,(![P]:(icext(uri_rdfs_ContainerMembershipProperty,P)=>iext(uri_rdfs_subPropertyOf,P,uri_rdfs_member))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_containermembershipproperty_instsub_member)).
% 3.19/3.39  fof(c97,plain,(![P]:(~icext(uri_rdfs_ContainerMembershipProperty,P)|iext(uri_rdfs_subPropertyOf,P,uri_rdfs_member))),inference(fof_nnf,[status(thm)],[rdfs_container_containermembershipproperty_instsub_member])).
% 3.19/3.39  fof(c98,plain,(![X32]:(~icext(uri_rdfs_ContainerMembershipProperty,X32)|iext(uri_rdfs_subPropertyOf,X32,uri_rdfs_member))),inference(variable_rename,[status(thm)],[c97])).
% 3.19/3.39  cnf(c99,plain,~icext(uri_rdfs_ContainerMembershipProperty,X86)|iext(uri_rdfs_subPropertyOf,X86,uri_rdfs_member),inference(split_conjunct,[status(thm)],[c98])).
% 3.19/3.39  fof(rdfs_container_n_type_003,axiom,iext(uri_rdf_type,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_type_003)).
% 3.19/3.39  cnf(c85,plain,iext(uri_rdf_type,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),inference(split_conjunct,[status(thm)],[rdfs_container_n_type_003])).
% 3.19/3.39  cnf(c113,plain,~iext(uri_rdf_type,X88,X89)|icext(X89,X88),inference(split_conjunct,[status(thm)],[c112])).
% 3.19/3.39  cnf(c390,plain,icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__3),inference(resolution,[status(thm)],[c113, c85])).
% 3.19/3.39  cnf(c398,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__3,uri_rdfs_member),inference(resolution,[status(thm)],[c390, c99])).
% 3.19/3.39  cnf(c806,plain,ip(uri_rdfs_member),inference(resolution,[status(thm)],[c398, c23])).
% 3.19/3.39  cnf(c808,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_member,uri_rdfs_member),inference(resolution,[status(thm)],[c806, c16])).
% 3.19/3.39  cnf(c1125,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X616)|iext(X616,uri_rdfs_member,uri_rdfs_member),inference(resolution,[status(thm)],[c808, c24])).
% 3.19/3.39  cnf(c131,plain,~ip(X95)|iext(uri_rdf_type,X95,uri_rdf_Property),inference(split_conjunct,[status(thm)],[c129])).
% 3.19/3.39  cnf(c807,plain,iext(uri_rdf_type,uri_rdfs_member,uri_rdf_Property),inference(resolution,[status(thm)],[c806, c131])).
% 3.19/3.39  cnf(c1112,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X614)|iext(X614,uri_rdfs_member,uri_rdf_Property),inference(resolution,[status(thm)],[c807, c24])).
% 3.19/3.39  cnf(c69,plain,~ic(X56)|icext(uri_rdfs_Class,X56),inference(split_conjunct,[status(thm)],[c68])).
% 3.19/3.39  fof(rdfs_subclassof_main,axiom,(![C]:(![D]:(iext(uri_rdfs_subClassOf,C,D)=>((ic(C)&ic(D))&(![X]:(icext(C,X)=>icext(D,X))))))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_subclassof_main)).
% 3.19/3.39  fof(c33,plain,(![C]:(![D]:(~iext(uri_rdfs_subClassOf,C,D)|((ic(C)&ic(D))&(![X]:(~icext(C,X)|icext(D,X))))))),inference(fof_nnf,[status(thm)],[rdfs_subclassof_main])).
% 3.19/3.39  fof(c35,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(c34,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)],[c33])).])).
% 3.19/3.39  fof(c36,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)],[c35])).
% 3.19/3.39  cnf(c38,plain,~iext(uri_rdfs_subClassOf,X73,X72)|ic(X72),inference(split_conjunct,[status(thm)],[c36])).
% 3.19/3.39  fof(rdfs_container_containermembershipproperty_sub,axiom,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_containermembershipproperty_sub)).
% 3.19/3.39  cnf(c96,plain,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_container_containermembershipproperty_sub])).
% 3.19/3.39  cnf(c233,plain,ic(uri_rdf_Property),inference(resolution,[status(thm)],[c38, c96])).
% 3.19/3.39  cnf(c361,plain,iext(uri_rdfs_subClassOf,uri_rdf_Property,uri_rdfs_Resource),inference(resolution,[status(thm)],[c108, c233])).
% 3.19/3.39  cnf(c699,plain,ic(uri_rdfs_Resource),inference(resolution,[status(thm)],[c361, c38])).
% 3.19/3.39  cnf(c707,plain,icext(uri_rdfs_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c699, c69])).
% 3.19/3.39  cnf(c711,plain,iext(uri_rdf_type,uri_rdfs_Resource,uri_rdfs_Class),inference(resolution,[status(thm)],[c707, c114])).
% 3.19/3.39  cnf(c1105,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X613)|iext(X613,uri_rdfs_Resource,uri_rdfs_Class),inference(resolution,[status(thm)],[c711, c24])).
% 3.19/3.39  cnf(c708,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Resource,uri_rdfs_Resource),inference(resolution,[status(thm)],[c699, c108])).
% 3.19/3.39  cnf(c1099,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X612)|iext(X612,uri_rdfs_Resource,uri_rdfs_Resource),inference(resolution,[status(thm)],[c708, c24])).
% 3.19/3.39  cnf(c4,plain,iext(uri_owl_propertyDisjointWith,uri_skos_prefLabel,uri_skos_altLabel),inference(split_conjunct,[status(thm)],[testcase_premise_fullish_019_Disjoint_Annotation_Properties])).
% 3.19/3.39  fof(simple_iext_property,axiom,(![S]:(![P]:(![O]:(iext(P,S,O)=>ip(P))))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', simple_iext_property)).
% 3.19/3.39  fof(c146,plain,(![S]:(![P]:(![O]:(~iext(P,S,O)|ip(P))))),inference(fof_nnf,[status(thm)],[simple_iext_property])).
% 3.19/3.39  fof(c147,plain,(![S]:(![P]:((![O]:~iext(P,S,O))|ip(P)))),inference(shift_quantors,[status(thm)],[c146])).
% 3.19/3.39  fof(c149,plain,(![X42]:(![X43]:(![X44]:(~iext(X43,X42,X44)|ip(X43))))),inference(shift_quantors,[status(thm)],[fof(c148,plain,(![X42]:(![X43]:((![X44]:~iext(X43,X42,X44))|ip(X43)))),inference(variable_rename,[status(thm)],[c147])).])).
% 3.19/3.39  cnf(c150,plain,~iext(X97,X96,X98)|ip(X97),inference(split_conjunct,[status(thm)],[c149])).
% 3.19/3.39  cnf(c539,plain,ip(uri_owl_propertyDisjointWith),inference(resolution,[status(thm)],[c150, c4])).
% 3.19/3.39  cnf(c600,plain,iext(uri_rdfs_subPropertyOf,uri_owl_propertyDisjointWith,uri_owl_propertyDisjointWith),inference(resolution,[status(thm)],[c539, c16])).
% 3.19/3.39  cnf(c1089,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X610)|iext(X610,uri_owl_propertyDisjointWith,uri_owl_propertyDisjointWith),inference(resolution,[status(thm)],[c600, c24])).
% 3.19/3.39  cnf(c599,plain,iext(uri_rdf_type,uri_owl_propertyDisjointWith,uri_rdf_Property),inference(resolution,[status(thm)],[c539, c131])).
% 3.19/3.39  cnf(c1080,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X608)|iext(X608,uri_owl_propertyDisjointWith,uri_rdf_Property),inference(resolution,[status(thm)],[c599, c24])).
% 3.19/3.39  cnf(c524,plain,ip(uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c150, c1])).
% 3.19/3.39  cnf(c590,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c524, c16])).
% 3.19/3.39  cnf(c1071,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X607)|iext(X607,uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c590, c24])).
% 3.19/3.39  cnf(c589,plain,iext(uri_rdf_type,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c524, c131])).
% 3.19/3.39  cnf(c1062,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X605)|iext(X605,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c589, c24])).
% 3.19/3.39  fof(rdfs_container_alt_sub,axiom,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Container),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_alt_sub)).
% 3.19/3.39  cnf(c101,plain,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Container),inference(split_conjunct,[status(thm)],[rdfs_container_alt_sub])).
% 3.19/3.39  cnf(c522,plain,ip(uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c150, c101])).
% 3.19/3.39  cnf(c588,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c522, c16])).
% 3.19/3.39  cnf(c1049,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X604)|iext(X604,uri_rdfs_subClassOf,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c588, c24])).
% 3.19/3.39  cnf(c587,plain,iext(uri_rdf_type,uri_rdfs_subClassOf,uri_rdf_Property),inference(resolution,[status(thm)],[c522, c131])).
% 3.19/3.39  cnf(c1039,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X602)|iext(X602,uri_rdfs_subClassOf,uri_rdf_Property),inference(resolution,[status(thm)],[c587, c24])).
% 3.19/3.39  fof(rdfs_annotation_comment_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_comment,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_comment_domain)).
% 3.19/3.39  cnf(c123,plain,iext(uri_rdfs_domain,uri_rdfs_comment,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_comment_domain])).
% 3.19/3.39  cnf(c517,plain,ip(uri_rdfs_domain),inference(resolution,[status(thm)],[c150, c123])).
% 3.19/3.39  cnf(c586,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,uri_rdfs_domain),inference(resolution,[status(thm)],[c517, c16])).
% 3.19/3.39  cnf(c1031,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X601)|iext(X601,uri_rdfs_domain,uri_rdfs_domain),inference(resolution,[status(thm)],[c586, c24])).
% 3.19/3.39  cnf(c585,plain,iext(uri_rdf_type,uri_rdfs_domain,uri_rdf_Property),inference(resolution,[status(thm)],[c517, c131])).
% 3.19/3.39  cnf(c1011,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X599)|iext(X599,uri_rdfs_domain,uri_rdf_Property),inference(resolution,[status(thm)],[c585, c24])).
% 3.19/3.39  fof(rdfs_container_n_range_001,axiom,iext(uri_rdfs_range,uri_rdf__1,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_range_001)).
% 3.19/3.39  cnf(c90,plain,iext(uri_rdfs_range,uri_rdf__1,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_range_001])).
% 3.19/3.39  cnf(c516,plain,ip(uri_rdfs_range),inference(resolution,[status(thm)],[c150, c90])).
% 3.19/3.39  cnf(c584,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_range,uri_rdfs_range),inference(resolution,[status(thm)],[c516, c16])).
% 3.19/3.39  cnf(c1004,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X598)|iext(X598,uri_rdfs_range,uri_rdfs_range),inference(resolution,[status(thm)],[c584, c24])).
% 3.19/3.39  cnf(c583,plain,iext(uri_rdf_type,uri_rdfs_range,uri_rdf_Property),inference(resolution,[status(thm)],[c516, c131])).
% 3.19/3.39  cnf(c984,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X596)|iext(X596,uri_rdfs_range,uri_rdf_Property),inference(resolution,[status(thm)],[c583, c24])).
% 3.19/3.39  fof(rdf_collection_first_type,axiom,iext(uri_rdf_type,uri_rdf_first,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdf_collection_first_type)).
% 3.19/3.39  cnf(c140,plain,iext(uri_rdf_type,uri_rdf_first,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_collection_first_type])).
% 3.19/3.39  cnf(c509,plain,ip(uri_rdf_first),inference(resolution,[status(thm)],[c140, c130])).
% 3.19/3.39  cnf(c515,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_first,uri_rdf_first),inference(resolution,[status(thm)],[c509, c16])).
% 3.19/3.39  cnf(c976,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X595)|iext(X595,uri_rdf_first,uri_rdf_first),inference(resolution,[status(thm)],[c515, c24])).
% 3.19/3.39  fof(rdf_collection_rest_type,axiom,iext(uri_rdf_type,uri_rdf_rest,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdf_collection_rest_type)).
% 3.19/3.39  cnf(c138,plain,iext(uri_rdf_type,uri_rdf_rest,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_collection_rest_type])).
% 3.19/3.39  cnf(c496,plain,ip(uri_rdf_rest),inference(resolution,[status(thm)],[c138, c130])).
% 3.19/3.39  cnf(c506,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_rest,uri_rdf_rest),inference(resolution,[status(thm)],[c496, c16])).
% 3.19/3.39  cnf(c969,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X593)|iext(X593,uri_rdf_rest,uri_rdf_rest),inference(resolution,[status(thm)],[c506, c24])).
% 3.19/3.39  fof(rdf_container_n_type_001,axiom,iext(uri_rdf_type,uri_rdf__1,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdf_container_n_type_001)).
% 3.19/3.39  cnf(c137,plain,iext(uri_rdf_type,uri_rdf__1,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_container_n_type_001])).
% 3.19/3.39  cnf(c485,plain,ip(uri_rdf__1),inference(resolution,[status(thm)],[c137, c130])).
% 3.19/3.39  cnf(c493,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__1,uri_rdf__1),inference(resolution,[status(thm)],[c485, c16])).
% 3.19/3.39  cnf(c961,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X591)|iext(X591,uri_rdf__1,uri_rdf__1),inference(resolution,[status(thm)],[c493, c24])).
% 3.19/3.39  fof(rdf_container_n_type_002,axiom,iext(uri_rdf_type,uri_rdf__2,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdf_container_n_type_002)).
% 3.19/3.39  cnf(c136,plain,iext(uri_rdf_type,uri_rdf__2,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_container_n_type_002])).
% 3.19/3.39  cnf(c480,plain,ip(uri_rdf__2),inference(resolution,[status(thm)],[c136, c130])).
% 3.19/3.39  cnf(c491,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__2,uri_rdf__2),inference(resolution,[status(thm)],[c480, c16])).
% 3.19/3.39  cnf(c954,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X589)|iext(X589,uri_rdf__2,uri_rdf__2),inference(resolution,[status(thm)],[c491, c24])).
% 3.19/3.39  fof(rdf_container_n_type_003,axiom,iext(uri_rdf_type,uri_rdf__3,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdf_container_n_type_003)).
% 3.19/3.39  cnf(c135,plain,iext(uri_rdf_type,uri_rdf__3,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_container_n_type_003])).
% 3.19/3.39  cnf(c472,plain,ip(uri_rdf__3),inference(resolution,[status(thm)],[c135, c130])).
% 3.19/3.39  cnf(c478,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__3,uri_rdf__3),inference(resolution,[status(thm)],[c472, c16])).
% 3.19/3.39  cnf(c946,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X587)|iext(X587,uri_rdf__3,uri_rdf__3),inference(resolution,[status(thm)],[c478, c24])).
% 3.19/3.39  cnf(c159,plain,ip(uri_rdfs_label),inference(resolution,[status(thm)],[c23, c1])).
% 3.19/3.39  cnf(c470,plain,iext(uri_rdf_type,uri_rdfs_label,uri_rdf_Property),inference(resolution,[status(thm)],[c131, c159])).
% 3.19/3.39  cnf(c939,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X585)|iext(X585,uri_rdfs_label,uri_rdf_Property),inference(resolution,[status(thm)],[c470, c24])).
% 3.19/3.39  cnf(c3,plain,iext(uri_rdfs_subPropertyOf,uri_skos_altLabel,uri_rdfs_label),inference(split_conjunct,[status(thm)],[testcase_premise_fullish_019_Disjoint_Annotation_Properties])).
% 3.19/3.39  cnf(c22,plain,~iext(uri_rdfs_subPropertyOf,X58,X59)|ip(X58),inference(split_conjunct,[status(thm)],[c21])).
% 3.19/3.39  cnf(c156,plain,ip(uri_skos_altLabel),inference(resolution,[status(thm)],[c22, c3])).
% 3.19/3.39  cnf(c469,plain,iext(uri_rdf_type,uri_skos_altLabel,uri_rdf_Property),inference(resolution,[status(thm)],[c131, c156])).
% 3.19/3.39  cnf(c932,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X584)|iext(X584,uri_skos_altLabel,uri_rdf_Property),inference(resolution,[status(thm)],[c469, c24])).
% 3.19/3.39  cnf(c155,plain,ip(uri_skos_prefLabel),inference(resolution,[status(thm)],[c22, c1])).
% 3.19/3.39  cnf(c466,plain,iext(uri_rdf_type,uri_skos_prefLabel,uri_rdf_Property),inference(resolution,[status(thm)],[c131, c155])).
% 3.19/3.39  cnf(c925,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X583)|iext(X583,uri_skos_prefLabel,uri_rdf_Property),inference(resolution,[status(thm)],[c466, c24])).
% 3.19/3.39  fof(rdfs_annotation_isdefinedby_sub,axiom,iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_isdefinedby_sub)).
% 3.19/3.39  cnf(c119,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_sub])).
% 3.19/3.39  cnf(c388,plain,ip(uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c119, c22])).
% 3.19/3.39  cnf(c465,plain,iext(uri_rdf_type,uri_rdfs_isDefinedBy,uri_rdf_Property),inference(resolution,[status(thm)],[c131, c388])).
% 3.19/3.39  cnf(c918,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X582)|iext(X582,uri_rdfs_isDefinedBy,uri_rdf_Property),inference(resolution,[status(thm)],[c465, c24])).
% 3.19/3.39  cnf(c385,plain,ip(uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c119, c23])).
% 3.19/3.39  cnf(c464,plain,iext(uri_rdf_type,uri_rdfs_seeAlso,uri_rdf_Property),inference(resolution,[status(thm)],[c131, c385])).
% 3.19/3.39  cnf(c911,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X581)|iext(X581,uri_rdfs_seeAlso,uri_rdf_Property),inference(resolution,[status(thm)],[c464, c24])).
% 3.19/3.39  fof(rdf_reification_object_type,axiom,iext(uri_rdf_type,uri_rdf_object,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdf_reification_object_type)).
% 3.19/3.39  cnf(c134,plain,iext(uri_rdf_type,uri_rdf_object,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_reification_object_type])).
% 3.19/3.39  cnf(c456,plain,ip(uri_rdf_object),inference(resolution,[status(thm)],[c134, c130])).
% 3.19/3.39  cnf(c461,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_object,uri_rdf_object),inference(resolution,[status(thm)],[c456, c16])).
% 3.19/3.39  cnf(c904,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X580)|iext(X580,uri_rdf_object,uri_rdf_object),inference(resolution,[status(thm)],[c461, c24])).
% 3.19/3.39  fof(rdf_value_type,axiom,iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdf_value_type)).
% 3.19/3.39  cnf(c124,plain,iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_value_type])).
% 3.19/3.39  cnf(c452,plain,ip(uri_rdf_type),inference(resolution,[status(thm)],[c130, c124])).
% 3.19/3.39  cnf(c455,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_type,uri_rdf_type),inference(resolution,[status(thm)],[c452, c16])).
% 3.19/3.39  cnf(c896,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X578)|iext(X578,uri_rdf_type,uri_rdf_type),inference(resolution,[status(thm)],[c455, c24])).
% 3.19/3.39  fof(rdf_reification_subject_type,axiom,iext(uri_rdf_type,uri_rdf_subject,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdf_reification_subject_type)).
% 3.19/3.39  cnf(c132,plain,iext(uri_rdf_type,uri_rdf_subject,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_reification_subject_type])).
% 3.19/3.39  cnf(c451,plain,ip(uri_rdf_subject),inference(resolution,[status(thm)],[c130, c132])).
% 3.19/3.39  cnf(c454,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_subject,uri_rdf_subject),inference(resolution,[status(thm)],[c451, c16])).
% 3.19/3.39  cnf(c882,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X576)|iext(X576,uri_rdf_subject,uri_rdf_subject),inference(resolution,[status(thm)],[c454, c24])).
% 3.19/3.39  fof(rdf_reification_predicate_type,axiom,iext(uri_rdf_type,uri_rdf_value,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdf_reification_predicate_type)).
% 3.19/3.39  cnf(c133,plain,iext(uri_rdf_type,uri_rdf_value,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_reification_predicate_type])).
% 3.19/3.39  cnf(c450,plain,ip(uri_rdf_value),inference(resolution,[status(thm)],[c130, c133])).
% 3.19/3.39  cnf(c453,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_value,uri_rdf_value),inference(resolution,[status(thm)],[c450, c16])).
% 3.19/3.39  cnf(c874,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X574)|iext(X574,uri_rdf_value,uri_rdf_value),inference(resolution,[status(thm)],[c453, c24])).
% 3.19/3.39  fof(rdfs_container_n_type_001,axiom,iext(uri_rdf_type,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_type_001)).
% 3.19/3.39  cnf(c87,plain,iext(uri_rdf_type,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),inference(split_conjunct,[status(thm)],[rdfs_container_n_type_001])).
% 3.19/3.39  cnf(c395,plain,icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__1),inference(resolution,[status(thm)],[c113, c87])).
% 3.19/3.39  cnf(c418,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__1,uri_rdfs_member),inference(resolution,[status(thm)],[c395, c99])).
% 3.19/3.39  cnf(c866,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X572)|iext(X572,uri_rdf__1,uri_rdfs_member),inference(resolution,[status(thm)],[c418, c24])).
% 3.19/3.39  fof(rdfs_subpropertyof_trans,axiom,(![P]:(![Q]:(![R]:((iext(uri_rdfs_subPropertyOf,P,Q)&iext(uri_rdfs_subPropertyOf,Q,R))=>iext(uri_rdfs_subPropertyOf,P,R))))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_subpropertyof_trans)).
% 3.19/3.39  fof(c11,plain,(![P]:(![Q]:(![R]:((~iext(uri_rdfs_subPropertyOf,P,Q)|~iext(uri_rdfs_subPropertyOf,Q,R))|iext(uri_rdfs_subPropertyOf,P,R))))),inference(fof_nnf,[status(thm)],[rdfs_subpropertyof_trans])).
% 3.19/3.39  fof(c12,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)],[c11])).
% 3.19/3.39  cnf(c13,plain,~iext(uri_rdfs_subPropertyOf,X49,X47)|~iext(uri_rdfs_subPropertyOf,X47,X48)|iext(uri_rdfs_subPropertyOf,X49,X48),inference(split_conjunct,[status(thm)],[c12])).
% 3.19/3.39  cnf(c861,plain,~iext(uri_rdfs_subPropertyOf,X571,uri_rdf__1)|iext(uri_rdfs_subPropertyOf,X571,uri_rdfs_member),inference(resolution,[status(thm)],[c418, c13])).
% 3.19/3.39  fof(rdfs_container_n_type_002,axiom,iext(uri_rdf_type,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_type_002)).
% 3.19/3.39  cnf(c86,plain,iext(uri_rdf_type,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),inference(split_conjunct,[status(thm)],[rdfs_container_n_type_002])).
% 3.19/3.39  cnf(c393,plain,icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__2),inference(resolution,[status(thm)],[c113, c86])).
% 3.19/3.39  cnf(c414,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__2,uri_rdfs_member),inference(resolution,[status(thm)],[c393, c99])).
% 3.19/3.39  cnf(c859,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X570)|iext(X570,uri_rdf__2,uri_rdfs_member),inference(resolution,[status(thm)],[c414, c24])).
% 3.19/3.39  cnf(c854,plain,~iext(uri_rdfs_subPropertyOf,X569,uri_rdf__2)|iext(uri_rdfs_subPropertyOf,X569,uri_rdfs_member),inference(resolution,[status(thm)],[c414, c13])).
% 3.19/3.39  fof(rdfs_datatype_sub,axiom,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Class),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_datatype_sub)).
% 3.19/3.39  cnf(c78,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_datatype_sub])).
% 3.19/3.39  cnf(c231,plain,ic(uri_rdfs_Class),inference(resolution,[status(thm)],[c38, c78])).
% 3.19/3.39  cnf(c240,plain,icext(uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c231, c69])).
% 3.19/3.39  cnf(c412,plain,iext(uri_rdf_type,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c114, c240])).
% 3.19/3.39  cnf(c853,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X568)|iext(X568,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c412, c24])).
% 3.19/3.39  fof(rdfs_dat_xmlliteral_sub,axiom,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Literal),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_dat_xmlliteral_sub)).
% 3.19/3.39  cnf(c83,plain,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[rdfs_dat_xmlliteral_sub])).
% 3.19/3.39  cnf(c37,plain,~iext(uri_rdfs_subClassOf,X71,X70)|ic(X71),inference(split_conjunct,[status(thm)],[c36])).
% 3.19/3.39  cnf(c216,plain,ic(uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c37, c83])).
% 3.19/3.39  cnf(c224,plain,icext(uri_rdfs_Class,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c216, c69])).
% 3.19/3.39  cnf(c411,plain,iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Class),inference(resolution,[status(thm)],[c114, c224])).
% 3.19/3.39  cnf(c848,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X567)|iext(X567,uri_rdf_XMLLiteral,uri_rdfs_Class),inference(resolution,[status(thm)],[c411, c24])).
% 3.19/3.39  cnf(c232,plain,ic(uri_rdfs_Literal),inference(resolution,[status(thm)],[c38, c83])).
% 3.19/3.39  cnf(c242,plain,icext(uri_rdfs_Class,uri_rdfs_Literal),inference(resolution,[status(thm)],[c232, c69])).
% 3.19/3.39  cnf(c410,plain,iext(uri_rdf_type,uri_rdfs_Literal,uri_rdfs_Class),inference(resolution,[status(thm)],[c114, c242])).
% 3.19/3.39  cnf(c843,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X566)|iext(X566,uri_rdfs_Literal,uri_rdfs_Class),inference(resolution,[status(thm)],[c410, c24])).
% 3.19/3.39  cnf(c214,plain,ic(uri_rdf_Alt),inference(resolution,[status(thm)],[c37, c101])).
% 3.19/3.39  cnf(c220,plain,icext(uri_rdfs_Class,uri_rdf_Alt),inference(resolution,[status(thm)],[c214, c69])).
% 3.19/3.39  cnf(c409,plain,iext(uri_rdf_type,uri_rdf_Alt,uri_rdfs_Class),inference(resolution,[status(thm)],[c114, c220])).
% 3.19/3.39  cnf(c838,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X565)|iext(X565,uri_rdf_Alt,uri_rdfs_Class),inference(resolution,[status(thm)],[c409, c24])).
% 3.19/3.39  fof(rdfs_container_seq_sub,axiom,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Container),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_seq_sub)).
% 3.19/3.39  cnf(c84,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Container),inference(split_conjunct,[status(thm)],[rdfs_container_seq_sub])).
% 3.19/3.39  cnf(c218,plain,ic(uri_rdfs_Seq),inference(resolution,[status(thm)],[c37, c84])).
% 3.19/3.39  cnf(c228,plain,icext(uri_rdfs_Class,uri_rdfs_Seq),inference(resolution,[status(thm)],[c218, c69])).
% 3.19/3.39  cnf(c407,plain,iext(uri_rdf_type,uri_rdfs_Seq,uri_rdfs_Class),inference(resolution,[status(thm)],[c114, c228])).
% 3.19/3.39  cnf(c833,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X564)|iext(X564,uri_rdfs_Seq,uri_rdfs_Class),inference(resolution,[status(thm)],[c407, c24])).
% 3.19/3.39  cnf(c217,plain,ic(uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c37, c96])).
% 3.19/3.39  cnf(c226,plain,icext(uri_rdfs_Class,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c217, c69])).
% 3.19/3.39  cnf(c404,plain,iext(uri_rdf_type,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Class),inference(resolution,[status(thm)],[c114, c226])).
% 3.19/3.39  cnf(c828,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X563)|iext(X563,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Class),inference(resolution,[status(thm)],[c404, c24])).
% 3.19/3.39  cnf(c215,plain,ic(uri_rdfs_Datatype),inference(resolution,[status(thm)],[c37, c78])).
% 3.19/3.39  cnf(c222,plain,icext(uri_rdfs_Class,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c215, c69])).
% 3.19/3.39  cnf(c401,plain,iext(uri_rdf_type,uri_rdfs_Datatype,uri_rdfs_Class),inference(resolution,[status(thm)],[c114, c222])).
% 3.19/3.39  cnf(c823,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X562)|iext(X562,uri_rdfs_Datatype,uri_rdfs_Class),inference(resolution,[status(thm)],[c401, c24])).
% 3.19/3.39  fof(rdfs_container_bag_sub,axiom,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Container),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_bag_sub)).
% 3.19/3.39  cnf(c100,plain,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Container),inference(split_conjunct,[status(thm)],[rdfs_container_bag_sub])).
% 3.19/3.39  cnf(c219,plain,ic(uri_rdf_Bag),inference(resolution,[status(thm)],[c37, c100])).
% 3.19/3.39  cnf(c236,plain,icext(uri_rdfs_Class,uri_rdf_Bag),inference(resolution,[status(thm)],[c219, c69])).
% 3.19/3.39  cnf(c400,plain,iext(uri_rdf_type,uri_rdf_Bag,uri_rdfs_Class),inference(resolution,[status(thm)],[c114, c236])).
% 3.19/3.39  cnf(c818,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X561)|iext(X561,uri_rdf_Bag,uri_rdfs_Class),inference(resolution,[status(thm)],[c400, c24])).
% 3.19/3.39  cnf(c230,plain,ic(uri_rdfs_Container),inference(resolution,[status(thm)],[c38, c101])).
% 3.19/3.39  cnf(c238,plain,icext(uri_rdfs_Class,uri_rdfs_Container),inference(resolution,[status(thm)],[c230, c69])).
% 3.19/3.39  cnf(c399,plain,iext(uri_rdf_type,uri_rdfs_Container,uri_rdfs_Class),inference(resolution,[status(thm)],[c114, c238])).
% 3.19/3.39  cnf(c813,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X560)|iext(X560,uri_rdfs_Container,uri_rdfs_Class),inference(resolution,[status(thm)],[c399, c24])).
% 3.19/3.39  cnf(c805,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X559)|iext(X559,uri_rdf__3,uri_rdfs_member),inference(resolution,[status(thm)],[c398, c24])).
% 3.19/3.39  cnf(c800,plain,~iext(uri_rdfs_subPropertyOf,X558,uri_rdf__3)|iext(uri_rdfs_subPropertyOf,X558,uri_rdfs_member),inference(resolution,[status(thm)],[c398, c13])).
% 3.19/3.39  cnf(c397,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c388, c16])).
% 3.19/3.39  cnf(c798,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X557)|iext(X557,uri_rdfs_isDefinedBy,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c397, c24])).
% 3.19/3.39  cnf(c396,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_seeAlso,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c385, c16])).
% 3.19/3.39  cnf(c791,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X555)|iext(X555,uri_rdfs_seeAlso,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c396, c24])).
% 3.19/3.39  cnf(c1305,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X553)|icext(X553,uri_rdfs_comment),inference(resolution,[status(thm)],[c1300, c76])).
% 3.19/3.39  cnf(c370,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Resource),inference(resolution,[status(thm)],[c108, c215])).
% 3.19/3.39  cnf(c785,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X552)|iext(X552,uri_rdfs_Datatype,uri_rdfs_Resource),inference(resolution,[status(thm)],[c370, c24])).
% 3.19/3.39  cnf(c1304,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X551)|icext(X551,uri_rdfs_comment),inference(resolution,[status(thm)],[c1300, c50])).
% 3.19/3.39  cnf(c781,plain,~iext(uri_rdfs_subClassOf,X548,uri_rdfs_Datatype)|iext(uri_rdfs_subClassOf,X548,uri_rdfs_Resource),inference(resolution,[status(thm)],[c370, c28])).
% 3.19/3.39  cnf(c1257,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X547)|icext(X547,uri_rdf_predicate),inference(resolution,[status(thm)],[c1252, c76])).
% 3.19/3.39  cnf(c1256,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X546)|icext(X546,uri_rdf_predicate),inference(resolution,[status(thm)],[c1252, c50])).
% 3.19/3.39  cnf(c369,plain,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Resource),inference(resolution,[status(thm)],[c108, c219])).
% 3.19/3.39  cnf(c777,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X545)|iext(X545,uri_rdf_Bag,uri_rdfs_Resource),inference(resolution,[status(thm)],[c369, c24])).
% 3.19/3.39  cnf(c773,plain,~iext(uri_rdfs_subClassOf,X541,uri_rdf_Bag)|iext(uri_rdfs_subClassOf,X541,uri_rdfs_Resource),inference(resolution,[status(thm)],[c369, c28])).
% 3.19/3.39  cnf(c1209,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X540)|icext(X540,uri_rdfs_Statement),inference(resolution,[status(thm)],[c1192, c50])).
% 3.19/3.39  cnf(c1202,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X539)|icext(X539,uri_rdfs_Statement),inference(resolution,[status(thm)],[c1191, c76])).
% 3.19/3.39  cnf(c368,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Resource),inference(resolution,[status(thm)],[c108, c218])).
% 3.19/3.39  cnf(c769,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X537)|iext(X537,uri_rdfs_Seq,uri_rdfs_Resource),inference(resolution,[status(thm)],[c368, c24])).
% 3.19/3.39  cnf(c1180,plain,~iext(uri_rdfs_domain,uri_rdfs_label,X534)|icext(X534,uri_ex_foo),inference(resolution,[status(thm)],[c689, c76])).
% 3.19/3.39  cnf(c765,plain,~iext(uri_rdfs_subClassOf,X533,uri_rdfs_Seq)|iext(uri_rdfs_subClassOf,X533,uri_rdfs_Resource),inference(resolution,[status(thm)],[c368, c28])).
% 3.19/3.39  cnf(c1176,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X532)|icext(X532,uri_rdf_List),inference(resolution,[status(thm)],[c1135, c50])).
% 3.19/3.39  cnf(c367,plain,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Resource),inference(resolution,[status(thm)],[c108, c217])).
% 3.19/3.39  cnf(c761,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X529)|iext(X529,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Resource),inference(resolution,[status(thm)],[c367, c24])).
% 3.19/3.39  cnf(c1166,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X528)|icext(X528,uri_rdf_List),inference(resolution,[status(thm)],[c1134, c76])).
% 3.19/3.39  cnf(c757,plain,~iext(uri_rdfs_subClassOf,X525,uri_rdfs_ContainerMembershipProperty)|iext(uri_rdfs_subClassOf,X525,uri_rdfs_Resource),inference(resolution,[status(thm)],[c367, c28])).
% 3.19/3.39  cnf(c1155,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X524)|icext(X524,uri_owl_AnnotationProperty),inference(resolution,[status(thm)],[c1119, c50])).
% 3.19/3.39  cnf(c366,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Literal,uri_rdfs_Resource),inference(resolution,[status(thm)],[c108, c232])).
% 3.19/3.39  cnf(c753,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X521)|iext(X521,uri_rdfs_Literal,uri_rdfs_Resource),inference(resolution,[status(thm)],[c366, c24])).
% 3.19/3.39  cnf(c1145,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X520)|icext(X520,uri_owl_AnnotationProperty),inference(resolution,[status(thm)],[c1118, c76])).
% 3.19/3.39  cnf(c749,plain,~iext(uri_rdfs_subClassOf,X518,uri_rdfs_Literal)|iext(uri_rdfs_subClassOf,X518,uri_rdfs_Resource),inference(resolution,[status(thm)],[c366, c28])).
% 3.19/3.39  cnf(c1121,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X515)|icext(X515,uri_rdfs_member),inference(resolution,[status(thm)],[c808, c76])).
% 3.19/3.39  cnf(c365,plain,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Resource),inference(resolution,[status(thm)],[c108, c214])).
% 3.19/3.39  cnf(c745,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X514)|iext(X514,uri_rdf_Alt,uri_rdfs_Resource),inference(resolution,[status(thm)],[c365, c24])).
% 3.19/3.39  cnf(c741,plain,~iext(uri_rdfs_subClassOf,X509,uri_rdf_Alt)|iext(uri_rdfs_subClassOf,X509,uri_rdfs_Resource),inference(resolution,[status(thm)],[c365, c28])).
% 3.19/3.39  cnf(c1094,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X507)|icext(X507,uri_rdfs_Resource),inference(resolution,[status(thm)],[c708, c76])).
% 3.19/3.39  cnf(c364,plain,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Resource),inference(resolution,[status(thm)],[c108, c216])).
% 3.19/3.39  cnf(c737,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X506)|iext(X506,uri_rdf_XMLLiteral,uri_rdfs_Resource),inference(resolution,[status(thm)],[c364, c24])).
% 3.19/3.39  cnf(c1085,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X505)|icext(X505,uri_owl_propertyDisjointWith),inference(resolution,[status(thm)],[c600, c50])).
% 3.19/3.39  cnf(c1084,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X504)|icext(X504,uri_owl_propertyDisjointWith),inference(resolution,[status(thm)],[c600, c76])).
% 3.19/3.39  cnf(c733,plain,~iext(uri_rdfs_subClassOf,X502,uri_rdf_XMLLiteral)|iext(uri_rdfs_subClassOf,X502,uri_rdfs_Resource),inference(resolution,[status(thm)],[c364, c28])).
% 3.19/3.39  cnf(c1067,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X500)|icext(X500,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c590, c50])).
% 3.19/3.39  cnf(c363,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c108, c231])).
% 3.19/3.39  cnf(c729,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X499)|iext(X499,uri_rdfs_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c363, c24])).
% 3.19/3.39  cnf(c1066,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X498)|icext(X498,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c590, c76])).
% 3.19/3.39  cnf(c725,plain,~iext(uri_rdfs_subClassOf,X495,uri_rdfs_Class)|iext(uri_rdfs_subClassOf,X495,uri_rdfs_Resource),inference(resolution,[status(thm)],[c363, c28])).
% 3.19/3.39  cnf(c1044,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X494)|icext(X494,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c588, c50])).
% 3.19/3.39  cnf(c1042,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X493)|icext(X493,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c588, c76])).
% 3.19/3.39  cnf(c362,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Container,uri_rdfs_Resource),inference(resolution,[status(thm)],[c108, c230])).
% 3.19/3.39  cnf(c719,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X492)|iext(X492,uri_rdfs_Container,uri_rdfs_Resource),inference(resolution,[status(thm)],[c362, c24])).
% 3.19/3.39  cnf(c715,plain,~iext(uri_rdfs_subClassOf,X490,uri_rdfs_Container)|iext(uri_rdfs_subClassOf,X490,uri_rdfs_Resource),inference(resolution,[status(thm)],[c362, c28])).
% 3.19/3.39  cnf(c1024,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X488)|icext(X488,uri_rdfs_domain),inference(resolution,[status(thm)],[c586, c50])).
% 3.19/3.39  cnf(c706,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X487)|iext(X487,uri_rdf_Property,uri_rdfs_Resource),inference(resolution,[status(thm)],[c361, c24])).
% 3.19/3.39  cnf(c1019,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X486)|icext(X486,uri_rdfs_domain),inference(resolution,[status(thm)],[c586, c76])).
% 3.19/3.39  cnf(c702,plain,~iext(uri_rdfs_subClassOf,X483,uri_rdf_Property)|iext(uri_rdfs_subClassOf,X483,uri_rdfs_Resource),inference(resolution,[status(thm)],[c361, c28])).
% 3.19/3.39  cnf(c993,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X482)|icext(X482,uri_rdfs_range),inference(resolution,[status(thm)],[c584, c50])).
% 3.19/3.39  cnf(c989,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X481)|icext(X481,uri_rdfs_range),inference(resolution,[status(thm)],[c584, c76])).
% 3.19/3.39  cnf(c245,plain,iext(uri_rdfs_subClassOf,uri_rdf_Property,uri_rdf_Property),inference(resolution,[status(thm)],[c233, c31])).
% 3.19/3.39  cnf(c698,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X480)|iext(X480,uri_rdf_Property,uri_rdf_Property),inference(resolution,[status(thm)],[c245, c24])).
% 3.19/3.39  cnf(c973,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X477)|icext(X477,uri_rdf_first),inference(resolution,[status(thm)],[c515, c50])).
% 3.19/3.39  cnf(c972,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X475)|icext(X475,uri_rdf_first),inference(resolution,[status(thm)],[c515, c76])).
% 3.19/3.39  cnf(c966,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X474)|icext(X474,uri_rdf_rest),inference(resolution,[status(thm)],[c506, c50])).
% 3.19/3.39  cnf(c243,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Literal,uri_rdfs_Literal),inference(resolution,[status(thm)],[c232, c31])).
% 3.19/3.39  cnf(c688,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X473)|iext(X473,uri_rdfs_Literal,uri_rdfs_Literal),inference(resolution,[status(thm)],[c243, c24])).
% 3.19/3.39  cnf(c965,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X472)|icext(X472,uri_rdf_rest),inference(resolution,[status(thm)],[c506, c76])).
% 3.19/3.39  cnf(c958,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X471)|icext(X471,uri_rdf__1),inference(resolution,[status(thm)],[c493, c50])).
% 3.19/3.39  cnf(c951,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X468)|icext(X468,uri_rdf__2),inference(resolution,[status(thm)],[c491, c50])).
% 3.19/3.39  cnf(c943,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X466)|icext(X466,uri_rdf__3),inference(resolution,[status(thm)],[c478, c50])).
% 3.19/3.39  cnf(c241,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c231, c31])).
% 3.19/3.39  cnf(c680,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X465)|iext(X465,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c241, c24])).
% 3.19/3.40  cnf(c239,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Container,uri_rdfs_Container),inference(resolution,[status(thm)],[c230, c31])).
% 3.19/3.40  cnf(c672,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X454)|iext(X454,uri_rdfs_Container,uri_rdfs_Container),inference(resolution,[status(thm)],[c239, c24])).
% 3.19/3.40  cnf(c901,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X451)|icext(X451,uri_rdf_object),inference(resolution,[status(thm)],[c461, c50])).
% 3.19/3.40  cnf(c900,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X449)|icext(X449,uri_rdf_object),inference(resolution,[status(thm)],[c461, c76])).
% 3.19/3.40  cnf(c891,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X448)|icext(X448,uri_rdf_type),inference(resolution,[status(thm)],[c455, c50])).
% 3.19/3.40  cnf(c237,plain,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdf_Bag),inference(resolution,[status(thm)],[c219, c31])).
% 3.19/3.40  cnf(c664,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X447)|iext(X447,uri_rdf_Bag,uri_rdf_Bag),inference(resolution,[status(thm)],[c237, c24])).
% 3.19/3.40  cnf(c888,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X446)|icext(X446,uri_rdf_type),inference(resolution,[status(thm)],[c455, c76])).
% 3.19/3.40  cnf(c879,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X445)|icext(X445,uri_rdf_subject),inference(resolution,[status(thm)],[c454, c50])).
% 3.19/3.40  cnf(c878,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X444)|icext(X444,uri_rdf_subject),inference(resolution,[status(thm)],[c454, c76])).
% 3.19/3.40  cnf(c871,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X442)|icext(X442,uri_rdf_value),inference(resolution,[status(thm)],[c453, c50])).
% 3.19/3.40  cnf(c870,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X441)|icext(X441,uri_rdf_value),inference(resolution,[status(thm)],[c453, c76])).
% 3.19/3.40  cnf(c229,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Seq),inference(resolution,[status(thm)],[c218, c31])).
% 3.19/3.40  cnf(c656,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X440)|iext(X440,uri_rdfs_Seq,uri_rdfs_Seq),inference(resolution,[status(thm)],[c229, c24])).
% 3.19/3.40  cnf(c862,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X438)|icext(X438,uri_rdf__1),inference(resolution,[status(thm)],[c418, c76])).
% 3.19/3.40  cnf(c855,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X435)|icext(X435,uri_rdf__2),inference(resolution,[status(thm)],[c414, c76])).
% 3.19/3.40  cnf(c227,plain,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c217, c31])).
% 3.19/3.40  cnf(c648,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X431)|iext(X431,uri_rdfs_ContainerMembershipProperty,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c227, c24])).
% 3.19/3.40  cnf(c225,plain,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c216, c31])).
% 3.19/3.40  cnf(c640,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X420)|iext(X420,uri_rdf_XMLLiteral,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c225, c24])).
% 3.19/3.40  cnf(c802,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X412)|icext(X412,uri_rdfs_member),inference(resolution,[status(thm)],[c398, c50])).
% 3.19/3.40  cnf(c223,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c215, c31])).
% 3.19/3.40  cnf(c632,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X411)|iext(X411,uri_rdfs_Datatype,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c223, c24])).
% 3.19/3.40  cnf(c801,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X410)|icext(X410,uri_rdf__3),inference(resolution,[status(thm)],[c398, c76])).
% 3.19/3.40  cnf(c795,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X409)|icext(X409,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c397, c50])).
% 3.19/3.40  cnf(c787,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X405)|icext(X405,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c396, c76])).
% 3.19/3.40  cnf(c221,plain,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdf_Alt),inference(resolution,[status(thm)],[c214, c31])).
% 3.19/3.40  cnf(c624,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X402)|iext(X402,uri_rdf_Alt,uri_rdf_Alt),inference(resolution,[status(thm)],[c221, c24])).
% 3.19/3.40  cnf(c161,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_label,uri_rdfs_label),inference(resolution,[status(thm)],[c159, c16])).
% 3.19/3.40  cnf(c610,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X385)|iext(X385,uri_rdfs_label,uri_rdfs_label),inference(resolution,[status(thm)],[c161, c24])).
% 3.19/3.40  cnf(c703,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X382)|icext(X382,uri_rdfs_Resource),inference(resolution,[status(thm)],[c361, c50])).
% 3.19/3.40  cnf(c693,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X378)|icext(X378,uri_rdf_Property),inference(resolution,[status(thm)],[c245, c76])).
% 3.19/3.40  cnf(c158,plain,iext(uri_rdfs_subPropertyOf,uri_skos_altLabel,uri_skos_altLabel),inference(resolution,[status(thm)],[c156, c16])).
% 3.19/3.40  cnf(c602,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X376)|iext(X376,uri_skos_altLabel,uri_skos_altLabel),inference(resolution,[status(thm)],[c158, c24])).
% 3.19/3.40  cnf(c683,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X375)|icext(X375,uri_rdfs_Literal),inference(resolution,[status(thm)],[c243, c76])).
% 3.19/3.40  cnf(c675,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X373)|icext(X373,uri_rdfs_Class),inference(resolution,[status(thm)],[c241, c76])).
% 3.19/3.40  cnf(c667,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X370)|icext(X370,uri_rdfs_Container),inference(resolution,[status(thm)],[c239, c76])).
% 3.19/3.40  cnf(c157,plain,iext(uri_rdfs_subPropertyOf,uri_skos_prefLabel,uri_skos_prefLabel),inference(resolution,[status(thm)],[c155, c16])).
% 3.19/3.40  cnf(c592,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X369)|iext(X369,uri_skos_prefLabel,uri_skos_prefLabel),inference(resolution,[status(thm)],[c157, c24])).
% 3.19/3.40  cnf(c661,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X368)|icext(X368,uri_rdf_Bag),inference(resolution,[status(thm)],[c237, c50])).
% 3.19/3.40  cnf(c653,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X366)|icext(X366,uri_rdfs_Seq),inference(resolution,[status(thm)],[c229, c50])).
% 3.19/3.40  cnf(c511,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X365)|iext(X365,uri_rdf_first,uri_rdf_Property),inference(resolution,[status(thm)],[c140, c24])).
% 3.19/3.40  cnf(c645,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X363)|icext(X363,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c227, c50])).
% 3.19/3.40  fof(rdf_collection_nil_type,axiom,iext(uri_rdf_type,uri_rdf_nil,uri_rdf_List),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdf_collection_nil_type)).
% 3.19/3.40  cnf(c139,plain,iext(uri_rdf_type,uri_rdf_nil,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdf_collection_nil_type])).
% 3.19/3.40  cnf(c502,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X361)|iext(X361,uri_rdf_nil,uri_rdf_List),inference(resolution,[status(thm)],[c139, c24])).
% 3.19/3.40  cnf(c637,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X360)|icext(X360,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c225, c50])).
% 3.19/3.40  cnf(c498,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X358)|iext(X358,uri_rdf_rest,uri_rdf_Property),inference(resolution,[status(thm)],[c138, c24])).
% 3.19/3.40  cnf(c629,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X357)|icext(X357,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c223, c50])).
% 3.19/3.40  cnf(c621,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X355)|icext(X355,uri_rdf_Alt),inference(resolution,[status(thm)],[c221, c50])).
% 3.19/3.40  cnf(c487,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X354)|iext(X354,uri_rdf__1,uri_rdf_Property),inference(resolution,[status(thm)],[c137, c24])).
% 3.19/3.40  cnf(c609,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X351)|icext(X351,uri_rdfs_label),inference(resolution,[status(thm)],[c161, c76])).
% 3.19/3.40  cnf(c482,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X350)|iext(X350,uri_rdf__2,uri_rdf_Property),inference(resolution,[status(thm)],[c136, c24])).
% 3.19/3.40  cnf(c607,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X349)|icext(X349,uri_skos_altLabel),inference(resolution,[status(thm)],[c158, c50])).
% 3.19/3.40  cnf(c474,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X347)|iext(X347,uri_rdf__3,uri_rdf_Property),inference(resolution,[status(thm)],[c135, c24])).
% 3.19/3.40  cnf(c597,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X346)|icext(X346,uri_skos_prefLabel),inference(resolution,[status(thm)],[c157, c50])).
% 3.19/3.40  cnf(c458,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X342)|iext(X342,uri_rdf_object,uri_rdf_Property),inference(resolution,[status(thm)],[c134, c24])).
% 3.19/3.40  cnf(c504,plain,~iext(uri_rdfs_range,uri_rdf_type,X341)|icext(X341,uri_rdf_List),inference(resolution,[status(thm)],[c139, c50])).
% 3.19/3.40  cnf(c446,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X338)|iext(X338,uri_rdf_value,uri_rdf_Property),inference(resolution,[status(thm)],[c133, c24])).
% 3.19/3.40  cnf(c441,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X333)|iext(X333,uri_rdf_subject,uri_rdf_Property),inference(resolution,[status(thm)],[c132, c24])).
% 3.19/3.40  cnf(c436,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X328)|iext(X328,uri_rdf_type,uri_rdf_Property),inference(resolution,[status(thm)],[c124, c24])).
% 3.19/3.40  cnf(c433,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X323)|iext(X323,uri_rdfs_comment,uri_rdfs_Resource),inference(resolution,[status(thm)],[c123, c24])).
% 3.19/3.40  cnf(c438,plain,~iext(uri_rdfs_range,uri_rdf_type,X321)|icext(X321,uri_rdf_Property),inference(resolution,[status(thm)],[c124, c50])).
% 3.19/3.40  cnf(c430,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X319)|iext(X319,uri_rdfs_comment,uri_rdfs_Literal),inference(resolution,[status(thm)],[c122, c24])).
% 3.19/3.40  cnf(c432,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X317)|icext(X317,uri_rdfs_comment),inference(resolution,[status(thm)],[c123, c76])).
% 3.19/3.40  fof(rdfs_annotation_isdefinedby_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_isdefinedby_domain)).
% 3.19/3.40  cnf(c121,plain,iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_domain])).
% 3.19/3.40  cnf(c427,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X315)|iext(X315,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(resolution,[status(thm)],[c121, c24])).
% 3.19/3.40  fof(rdfs_annotation_isdefinedby_range,axiom,iext(uri_rdfs_range,uri_rdfs_isDefinedBy,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_isdefinedby_range)).
% 3.19/3.40  cnf(c120,plain,iext(uri_rdfs_range,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_range])).
% 3.19/3.40  cnf(c424,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X314)|iext(X314,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(resolution,[status(thm)],[c120, c24])).
% 3.19/3.40  fof(simple_ir,axiom,(![X]:ir(X)),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', simple_ir)).
% 3.19/3.40  fof(c144,plain,(![X41]:ir(X41)),inference(variable_rename,[status(thm)],[simple_ir])).
% 3.19/3.40  cnf(c145,plain,ir(X45),inference(split_conjunct,[status(thm)],[c144])).
% 3.19/3.40  fof(rdfs_ir_def,axiom,(![X]:(ir(X)<=>icext(uri_rdfs_Resource,X))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_ir_def)).
% 3.19/3.40  fof(c59,plain,(![X]:((~ir(X)|icext(uri_rdfs_Resource,X))&(~icext(uri_rdfs_Resource,X)|ir(X)))),inference(fof_nnf,[status(thm)],[rdfs_ir_def])).
% 3.19/3.40  fof(c60,plain,((![X]:(~ir(X)|icext(uri_rdfs_Resource,X)))&(![X]:(~icext(uri_rdfs_Resource,X)|ir(X)))),inference(shift_quantors,[status(thm)],[c59])).
% 3.19/3.40  fof(c62,plain,(![X23]:(![X24]:((~ir(X23)|icext(uri_rdfs_Resource,X23))&(~icext(uri_rdfs_Resource,X24)|ir(X24))))),inference(shift_quantors,[status(thm)],[fof(c61,plain,((![X23]:(~ir(X23)|icext(uri_rdfs_Resource,X23)))&(![X24]:(~icext(uri_rdfs_Resource,X24)|ir(X24)))),inference(variable_rename,[status(thm)],[c60])).])).
% 3.19/3.40  cnf(c63,plain,~ir(X53)|icext(uri_rdfs_Resource,X53),inference(split_conjunct,[status(thm)],[c62])).
% 3.19/3.40  cnf(c154,plain,icext(uri_rdfs_Resource,X54),inference(resolution,[status(thm)],[c63, c145])).
% 3.19/3.40  cnf(c402,plain,iext(uri_rdf_type,X92,uri_rdfs_Resource),inference(resolution,[status(thm)],[c114, c154])).
% 3.19/3.40  cnf(c420,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X312)|iext(X312,X311,uri_rdfs_Resource),inference(resolution,[status(thm)],[c402, c24])).
% 3.19/3.40  cnf(c386,plain,~iext(uri_rdfs_subPropertyOf,X308,uri_rdfs_isDefinedBy)|iext(uri_rdfs_subPropertyOf,X308,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c119, c13])).
% 3.19/3.40  cnf(c426,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X307)|icext(X307,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c121, c76])).
% 3.19/3.40  cnf(c384,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X305)|iext(X305,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c119, c24])).
% 3.19/3.40  cnf(c423,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X304)|icext(X304,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c120, c76])).
% 3.19/3.40  cnf(c422,plain,~iext(uri_rdfs_range,uri_rdf_type,X303)|icext(X303,uri_rdfs_Resource),inference(resolution,[status(thm)],[c402, c50])).
% 3.19/3.40  fof(rdfs_annotation_label_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_label,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_label_domain)).
% 3.19/3.40  cnf(c118,plain,iext(uri_rdfs_domain,uri_rdfs_label,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_label_domain])).
% 3.19/3.40  cnf(c381,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X302)|iext(X302,uri_rdfs_label,uri_rdfs_Resource),inference(resolution,[status(thm)],[c118, c24])).
% 3.19/3.40  cnf(c387,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X301)|icext(X301,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c119, c50])).
% 3.19/3.40  cnf(c383,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X300)|icext(X300,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c119, c76])).
% 3.19/3.40  cnf(c378,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X298)|iext(X298,uri_rdfs_label,uri_rdfs_Literal),inference(resolution,[status(thm)],[c117, c24])).
% 3.19/3.40  cnf(c380,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X297)|icext(X297,uri_rdfs_label),inference(resolution,[status(thm)],[c118, c76])).
% 3.19/3.40  cnf(c379,plain,~iext(uri_rdfs_range,uri_rdfs_range,X296)|icext(X296,uri_rdfs_Literal),inference(resolution,[status(thm)],[c117, c50])).
% 3.19/3.40  fof(rdfs_annotation_seealso_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_seeAlso,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_seealso_domain)).
% 3.19/3.40  cnf(c116,plain,iext(uri_rdfs_domain,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_seealso_domain])).
% 3.19/3.40  cnf(c375,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X295)|iext(X295,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(resolution,[status(thm)],[c116, c24])).
% 3.19/3.40  cnf(c377,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X294)|icext(X294,uri_rdfs_label),inference(resolution,[status(thm)],[c117, c76])).
% 3.19/3.40  fof(rdfs_annotation_seealso_range,axiom,iext(uri_rdfs_range,uri_rdfs_seeAlso,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_seealso_range)).
% 3.19/3.40  cnf(c115,plain,iext(uri_rdfs_range,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_seealso_range])).
% 3.19/3.40  cnf(c372,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X292)|iext(X292,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(resolution,[status(thm)],[c115, c24])).
% 3.19/3.40  cnf(c374,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X291)|icext(X291,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c116, c76])).
% 3.19/3.40  cnf(c371,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X289)|icext(X289,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c115, c76])).
% 3.19/3.40  fof(rdfs_collection_first_domain,axiom,iext(uri_rdfs_domain,uri_rdf_first,uri_rdf_List),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_collection_first_domain)).
% 3.19/3.40  cnf(c105,plain,iext(uri_rdfs_domain,uri_rdf_first,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdfs_collection_first_domain])).
% 3.19/3.40  cnf(c359,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X288)|iext(X288,uri_rdf_first,uri_rdf_List),inference(resolution,[status(thm)],[c105, c24])).
% 3.19/3.40  cnf(c358,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X286)|icext(X286,uri_rdf_first),inference(resolution,[status(thm)],[c105, c76])).
% 3.19/3.40  fof(rdfs_collection_first_range,axiom,iext(uri_rdfs_range,uri_rdf_first,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_collection_first_range)).
% 3.19/3.40  cnf(c104,plain,iext(uri_rdfs_range,uri_rdf_first,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_collection_first_range])).
% 3.19/3.40  cnf(c356,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X284)|iext(X284,uri_rdf_first,uri_rdfs_Resource),inference(resolution,[status(thm)],[c104, c24])).
% 3.19/3.40  cnf(c355,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X283)|icext(X283,uri_rdf_first),inference(resolution,[status(thm)],[c104, c76])).
% 3.19/3.40  fof(rdfs_collection_rest_domain,axiom,iext(uri_rdfs_domain,uri_rdf_rest,uri_rdf_List),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_collection_rest_domain)).
% 3.19/3.40  cnf(c103,plain,iext(uri_rdfs_domain,uri_rdf_rest,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdfs_collection_rest_domain])).
% 3.19/3.40  cnf(c354,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X282)|icext(X282,uri_rdf_List),inference(resolution,[status(thm)],[c103, c50])).
% 3.19/3.40  cnf(c353,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X281)|iext(X281,uri_rdf_rest,uri_rdf_List),inference(resolution,[status(thm)],[c103, c24])).
% 3.19/3.40  cnf(c352,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X280)|icext(X280,uri_rdf_rest),inference(resolution,[status(thm)],[c103, c76])).
% 3.19/3.40  fof(rdfs_container_member_range,axiom,iext(uri_rdfs_range,uri_rdfs_member,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_member_range)).
% 3.19/3.40  cnf(c94,plain,iext(uri_rdfs_range,uri_rdfs_member,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_member_range])).
% 3.19/3.40  cnf(c344,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X278)|icext(X278,uri_rdfs_member),inference(resolution,[status(thm)],[c76, c94])).
% 3.19/3.40  fof(rdfs_container_n_domain_001,axiom,iext(uri_rdfs_domain,uri_rdf__1,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_domain_001)).
% 3.19/3.40  cnf(c93,plain,iext(uri_rdfs_domain,uri_rdf__1,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_001])).
% 3.19/3.40  cnf(c343,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X277)|icext(X277,uri_rdf__1),inference(resolution,[status(thm)],[c76, c93])).
% 3.19/3.40  fof(rdfs_reification_predicate_domain,axiom,iext(uri_rdfs_domain,uri_rdf_predicate,uri_rdfs_Statement),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_reification_predicate_domain)).
% 3.19/3.40  cnf(c44,plain,iext(uri_rdfs_domain,uri_rdf_predicate,uri_rdfs_Statement),inference(split_conjunct,[status(thm)],[rdfs_reification_predicate_domain])).
% 3.19/3.40  cnf(c342,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X276)|icext(X276,uri_rdf_predicate),inference(resolution,[status(thm)],[c76, c44])).
% 3.19/3.40  fof(rdfs_reification_subject_range,axiom,iext(uri_rdfs_range,uri_rdf_subject,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_reification_subject_range)).
% 3.19/3.40  cnf(c41,plain,iext(uri_rdfs_range,uri_rdf_subject,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_reification_subject_range])).
% 3.19/3.40  cnf(c340,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X274)|icext(X274,uri_rdf_subject),inference(resolution,[status(thm)],[c76, c41])).
% 3.19/3.40  fof(rdfs_subclassof_range,axiom,iext(uri_rdfs_range,uri_rdfs_subClassOf,uri_rdfs_Class),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_subclassof_range)).
% 3.19/3.40  cnf(c32,plain,iext(uri_rdfs_range,uri_rdfs_subClassOf,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_subclassof_range])).
% 3.19/3.40  cnf(c339,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X273)|icext(X273,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c76, c32])).
% 3.19/3.40  cnf(c338,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X272)|icext(X272,uri_rdf_Bag),inference(resolution,[status(thm)],[c76, c100])).
% 3.19/3.40  fof(rdfs_reification_object_domain,axiom,iext(uri_rdfs_domain,uri_rdf_object,uri_rdfs_Statement),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_reification_object_domain)).
% 3.19/3.40  cnf(c46,plain,iext(uri_rdfs_domain,uri_rdf_object,uri_rdfs_Statement),inference(split_conjunct,[status(thm)],[rdfs_reification_object_domain])).
% 3.19/3.40  cnf(c336,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X270)|icext(X270,uri_rdf_object),inference(resolution,[status(thm)],[c76, c46])).
% 3.19/3.40  fof(rdfs_subclassof_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdfs_Class),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_subclassof_domain)).
% 3.19/3.40  cnf(c40,plain,iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_subclassof_domain])).
% 3.19/3.40  cnf(c334,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X268)|icext(X268,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c76, c40])).
% 3.19/3.40  cnf(c333,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X267)|icext(X267,uri_rdfs_Seq),inference(resolution,[status(thm)],[c76, c84])).
% 3.19/3.40  cnf(c332,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X266)|icext(X266,uri_rdf_subject),inference(resolution,[status(thm)],[c76, c42])).
% 3.19/3.40  fof(rdfs_container_n_domain_002,axiom,iext(uri_rdfs_domain,uri_rdf__2,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_domain_002)).
% 3.19/3.40  cnf(c92,plain,iext(uri_rdfs_domain,uri_rdf__2,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_002])).
% 3.19/3.40  cnf(c331,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X265)|icext(X265,uri_rdf__2),inference(resolution,[status(thm)],[c76, c92])).
% 3.19/3.40  fof(rdfs_subpropertyof_range,axiom,iext(uri_rdfs_range,uri_rdfs_subPropertyOf,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_subpropertyof_range)).
% 3.19/3.40  cnf(c17,plain,iext(uri_rdfs_range,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_subpropertyof_range])).
% 3.19/3.40  cnf(c329,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X263)|icext(X263,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c76, c17])).
% 3.19/3.40  cnf(c328,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X262)|icext(X262,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c76, c96])).
% 3.19/3.40  cnf(c6,plain,iext(uri_skos_altLabel,uri_ex_foo,literal_plain(dat_str_foo)),inference(split_conjunct,[status(thm)],[testcase_premise_fullish_019_Disjoint_Annotation_Properties])).
% 3.19/3.40  cnf(c327,plain,~iext(uri_rdfs_domain,uri_skos_altLabel,X261)|icext(X261,uri_ex_foo),inference(resolution,[status(thm)],[c76, c6])).
% 3.19/3.40  fof(rdfs_subpropertyof_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_subpropertyof_domain)).
% 3.19/3.40  cnf(c25,plain,iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_subpropertyof_domain])).
% 3.19/3.40  cnf(c326,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X260)|icext(X260,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c76, c25])).
% 3.19/3.40  fof(rdfs_container_member_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_member,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_member_domain)).
% 3.19/3.40  cnf(c95,plain,iext(uri_rdfs_domain,uri_rdfs_member,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_member_domain])).
% 3.19/3.40  cnf(c325,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X259)|icext(X259,uri_rdfs_member),inference(resolution,[status(thm)],[c76, c95])).
% 3.19/3.40  cnf(c324,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X258)|icext(X258,uri_rdfs_range),inference(resolution,[status(thm)],[c76, c51])).
% 3.19/3.40  cnf(c323,plain,~iext(uri_rdfs_domain,uri_skos_prefLabel,X257)|icext(X257,uri_ex_foo),inference(resolution,[status(thm)],[c76, c5])).
% 3.19/3.40  fof(rdfs_type_domain,axiom,iext(uri_rdfs_domain,uri_rdf_type,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_type_domain)).
% 3.19/3.40  cnf(c10,plain,iext(uri_rdfs_domain,uri_rdf_type,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_type_domain])).
% 3.19/3.40  cnf(c321,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X255)|icext(X255,uri_rdf_type),inference(resolution,[status(thm)],[c76, c10])).
% 3.19/3.40  fof(rdfs_container_n_domain_003,axiom,iext(uri_rdfs_domain,uri_rdf__3,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_domain_003)).
% 3.19/3.40  cnf(c91,plain,iext(uri_rdfs_domain,uri_rdf__3,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_003])).
% 3.19/3.40  cnf(c320,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X254)|icext(X254,uri_rdf__3),inference(resolution,[status(thm)],[c76, c91])).
% 3.19/3.40  fof(rdfs_value_domain,axiom,iext(uri_rdfs_domain,uri_rdf_value,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_value_domain)).
% 3.19/3.40  cnf(c8,plain,iext(uri_rdfs_domain,uri_rdf_value,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_value_domain])).
% 3.19/3.40  cnf(c319,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X253)|icext(X253,uri_rdf_value),inference(resolution,[status(thm)],[c76, c8])).
% 3.19/3.40  cnf(c318,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X252)|icext(X252,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c76, c83])).
% 3.19/3.40  fof(rdfs_container_n_range_002,axiom,iext(uri_rdfs_range,uri_rdf__2,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_range_002)).
% 3.19/3.40  cnf(c89,plain,iext(uri_rdfs_range,uri_rdf__2,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_range_002])).
% 3.19/3.40  cnf(c317,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X251)|icext(X251,uri_rdf__2),inference(resolution,[status(thm)],[c76, c89])).
% 3.19/3.40  cnf(c316,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X250)|icext(X250,uri_rdf_type),inference(resolution,[status(thm)],[c76, c9])).
% 3.19/3.40  cnf(c315,plain,~iext(uri_rdfs_domain,uri_owl_propertyDisjointWith,X249)|icext(X249,uri_skos_prefLabel),inference(resolution,[status(thm)],[c76, c4])).
% 3.19/3.40  cnf(c314,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X248)|icext(X248,uri_rdf_rest),inference(resolution,[status(thm)],[c76, c102])).
% 3.19/3.40  fof(rdfs_value_range,axiom,iext(uri_rdfs_range,uri_rdf_value,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_value_range)).
% 3.19/3.40  cnf(c7,plain,iext(uri_rdfs_range,uri_rdf_value,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_value_range])).
% 3.19/3.40  cnf(c312,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X246)|icext(X246,uri_rdf_value),inference(resolution,[status(thm)],[c76, c7])).
% 3.19/3.40  fof(rdfs_container_n_range_003,axiom,iext(uri_rdfs_range,uri_rdf__3,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_range_003)).
% 3.19/3.40  cnf(c88,plain,iext(uri_rdfs_range,uri_rdf__3,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_range_003])).
% 3.19/3.40  cnf(c311,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X245)|icext(X245,uri_rdf__3),inference(resolution,[status(thm)],[c76, c88])).
% 3.19/3.40  cnf(c309,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X243)|icext(X243,uri_skos_altLabel),inference(resolution,[status(thm)],[c76, c3])).
% 3.19/3.40  cnf(c308,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X242)|icext(X242,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c76, c78])).
% 3.19/3.40  cnf(c307,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X241)|icext(X241,uri_rdfs_domain),inference(resolution,[status(thm)],[c76, c71])).
% 3.19/3.40  cnf(c305,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X239)|icext(X239,uri_rdfs_range),inference(resolution,[status(thm)],[c76, c47])).
% 3.19/3.40  cnf(c304,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X238)|icext(X238,uri_skos_prefLabel),inference(resolution,[status(thm)],[c76, c1])).
% 3.19/3.40  cnf(c303,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X237)|icext(X237,uri_rdf_Alt),inference(resolution,[status(thm)],[c76, c101])).
% 3.19/3.40  cnf(c302,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X236)|icext(X236,uri_rdf__1),inference(resolution,[status(thm)],[c76, c90])).
% 3.19/3.40  cnf(c301,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X235)|icext(X235,uri_rdfs_domain),inference(factor,[status(thm)],[c76])).
% 3.19/3.40  fof(rdfs_dat_xmlliteral_type,axiom,iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Datatype),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_dat_xmlliteral_type)).
% 3.19/3.40  cnf(c82,plain,iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Datatype),inference(split_conjunct,[status(thm)],[rdfs_dat_xmlliteral_type])).
% 3.19/3.40  cnf(c294,plain,~iext(uri_rdfs_range,uri_rdf_type,X230)|icext(X230,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c50, c82])).
% 3.19/3.40  cnf(c419,plain,~iext(uri_rdfs_domain,uri_rdf_type,X222)|icext(X222,X223),inference(resolution,[status(thm)],[c402, c76])).
% 3.19/3.40  cnf(c287,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X216)|icext(X216,uri_rdfs_Class),inference(resolution,[status(thm)],[c50, c40])).
% 3.19/3.40  fof(rdfs_property_type,axiom,iext(uri_rdf_type,uri_rdf_Property,uri_rdfs_Class),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_property_type)).
% 3.19/3.40  cnf(c52,plain,iext(uri_rdf_type,uri_rdf_Property,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_property_type])).
% 3.19/3.40  cnf(c283,plain,~iext(uri_rdfs_range,uri_rdf_type,X203)|icext(X203,uri_rdfs_Class),inference(resolution,[status(thm)],[c50, c52])).
% 3.19/3.40  cnf(c282,plain,~iext(uri_rdfs_range,uri_rdfs_range,X200)|icext(X200,uri_rdf_Property),inference(resolution,[status(thm)],[c50, c17])).
% 3.19/3.40  cnf(c281,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X196)|icext(X196,uri_rdf_Property),inference(resolution,[status(thm)],[c50, c96])).
% 3.19/3.40  cnf(c280,plain,~iext(uri_rdfs_range,uri_skos_altLabel,X192)|icext(X192,literal_plain(dat_str_foo)),inference(resolution,[status(thm)],[c50, c6])).
% 3.19/3.40  cnf(c276,plain,~iext(uri_rdfs_range,uri_skos_prefLabel,X182)|icext(X182,literal_plain(dat_str_foo)),inference(resolution,[status(thm)],[c50, c5])).
% 3.19/3.40  cnf(c272,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X178)|icext(X178,uri_rdfs_Resource),inference(resolution,[status(thm)],[c50, c8])).
% 3.19/3.40  cnf(c271,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X177)|icext(X177,uri_rdfs_Literal),inference(resolution,[status(thm)],[c50, c83])).
% 3.19/3.40  cnf(c268,plain,~iext(uri_rdfs_range,uri_owl_propertyDisjointWith,X174)|icext(X174,uri_skos_altLabel),inference(resolution,[status(thm)],[c50, c4])).
% 3.19/3.40  fof(rdfs_domain_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_domain_domain)).
% 3.19/3.40  cnf(c77,plain,iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_domain_domain])).
% 3.19/3.40  cnf(c266,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X172)|icext(X172,uri_rdf_Property),inference(resolution,[status(thm)],[c50, c77])).
% 3.19/3.40  cnf(c263,plain,~iext(uri_rdfs_range,uri_rdf_type,X169)|icext(X169,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c50, c85])).
% 3.19/3.40  cnf(c261,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X167)|icext(X167,uri_rdfs_Class),inference(resolution,[status(thm)],[c50, c78])).
% 3.19/3.40  cnf(c1108,plain,icext(uri_rdf_Property,uri_rdfs_member),inference(resolution,[status(thm)],[c807, c113])).
% 3.19/3.40  cnf(c258,plain,~iext(uri_rdfs_range,uri_rdfs_range,X164)|icext(X164,uri_rdfs_Class),inference(resolution,[status(thm)],[c50, c47])).
% 3.19/3.40  cnf(c257,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X163)|icext(X163,uri_rdfs_label),inference(resolution,[status(thm)],[c50, c1])).
% 3.19/3.40  cnf(c256,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X162)|icext(X162,uri_rdfs_Container),inference(resolution,[status(thm)],[c50, c101])).
% 3.19/3.40  cnf(c255,plain,~iext(uri_rdfs_range,uri_rdfs_range,X161)|icext(X161,uri_rdfs_Resource),inference(resolution,[status(thm)],[c50, c90])).
% 3.19/3.40  cnf(c1076,plain,icext(uri_rdf_Property,uri_owl_propertyDisjointWith),inference(resolution,[status(thm)],[c599, c113])).
% 3.19/3.40  cnf(c254,plain,~iext(uri_rdfs_range,uri_rdfs_range,X160)|icext(X160,X160),inference(factor,[status(thm)],[c50])).
% 3.19/3.40  cnf(c39,plain,~iext(uri_rdfs_subClassOf,X76,X75)|~icext(X76,X74)|icext(X75,X74),inference(split_conjunct,[status(thm)],[c36])).
% 3.19/3.40  cnf(c251,plain,~icext(uri_rdf_Bag,X159)|icext(uri_rdfs_Container,X159),inference(resolution,[status(thm)],[c39, c100])).
% 3.19/3.40  cnf(c1058,plain,icext(uri_rdf_Property,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c589, c113])).
% 3.19/3.40  cnf(c250,plain,~icext(uri_rdfs_Seq,X158)|icext(uri_rdfs_Container,X158),inference(resolution,[status(thm)],[c39, c84])).
% 3.19/3.40  cnf(c249,plain,~icext(uri_rdfs_ContainerMembershipProperty,X157)|icext(uri_rdf_Property,X157),inference(resolution,[status(thm)],[c39, c96])).
% 3.19/3.40  cnf(c1035,plain,icext(uri_rdf_Property,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c587, c113])).
% 3.19/3.40  cnf(c248,plain,~icext(uri_rdf_XMLLiteral,X156)|icext(uri_rdfs_Literal,X156),inference(resolution,[status(thm)],[c39, c83])).
% 3.19/3.40  cnf(c247,plain,~icext(uri_rdfs_Datatype,X155)|icext(uri_rdfs_Class,X155),inference(resolution,[status(thm)],[c39, c78])).
% 3.19/3.40  cnf(c1007,plain,icext(uri_rdf_Property,uri_rdfs_domain),inference(resolution,[status(thm)],[c585, c113])).
% 3.19/3.40  cnf(c246,plain,~icext(uri_rdf_Alt,X154)|icext(uri_rdfs_Container,X154),inference(resolution,[status(thm)],[c39, c101])).
% 3.19/3.40  cnf(c980,plain,icext(uri_rdf_Property,uri_rdfs_range),inference(resolution,[status(thm)],[c583, c113])).
% 3.19/3.40  cnf(c213,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X153)|iext(X153,uri_rdf_rest,uri_rdf_List),inference(resolution,[status(thm)],[c102, c24])).
% 3.19/3.40  cnf(c212,plain,~iext(uri_rdfs_subClassOf,X152,uri_rdf_Alt)|iext(uri_rdfs_subClassOf,X152,uri_rdfs_Container),inference(resolution,[status(thm)],[c101, c28])).
% 3.19/3.40  cnf(c211,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X151)|iext(X151,uri_rdf_Alt,uri_rdfs_Container),inference(resolution,[status(thm)],[c101, c24])).
% 3.19/3.40  cnf(c210,plain,~iext(uri_rdfs_subClassOf,X150,uri_rdf_Bag)|iext(uri_rdfs_subClassOf,X150,uri_rdfs_Container),inference(resolution,[status(thm)],[c100, c28])).
% 3.19/3.40  cnf(c209,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X149)|iext(X149,uri_rdf_Bag,uri_rdfs_Container),inference(resolution,[status(thm)],[c100, c24])).
% 3.19/3.40  cnf(c208,plain,~iext(uri_rdfs_subClassOf,X148,uri_rdfs_ContainerMembershipProperty)|iext(uri_rdfs_subClassOf,X148,uri_rdf_Property),inference(resolution,[status(thm)],[c96, c28])).
% 3.19/3.40  cnf(c207,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X147)|iext(X147,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),inference(resolution,[status(thm)],[c96, c24])).
% 3.19/3.40  cnf(c935,plain,icext(uri_rdf_Property,uri_rdfs_label),inference(resolution,[status(thm)],[c470, c113])).
% 3.19/3.40  cnf(c206,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X146)|iext(X146,uri_rdfs_member,uri_rdfs_Resource),inference(resolution,[status(thm)],[c95, c24])).
% 3.19/3.40  cnf(c928,plain,icext(uri_rdf_Property,uri_skos_altLabel),inference(resolution,[status(thm)],[c469, c113])).
% 3.19/3.40  cnf(c205,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X145)|iext(X145,uri_rdfs_member,uri_rdfs_Resource),inference(resolution,[status(thm)],[c94, c24])).
% 3.19/3.40  cnf(c921,plain,icext(uri_rdf_Property,uri_skos_prefLabel),inference(resolution,[status(thm)],[c466, c113])).
% 3.19/3.40  cnf(c204,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X144)|iext(X144,uri_rdf__1,uri_rdfs_Resource),inference(resolution,[status(thm)],[c93, c24])).
% 3.19/3.40  cnf(c914,plain,icext(uri_rdf_Property,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c465, c113])).
% 3.19/3.40  cnf(c203,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X143)|iext(X143,uri_rdf__2,uri_rdfs_Resource),inference(resolution,[status(thm)],[c92, c24])).
% 3.19/3.40  cnf(c907,plain,icext(uri_rdf_Property,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c464, c113])).
% 3.19/3.40  cnf(c202,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X142)|iext(X142,uri_rdf__3,uri_rdfs_Resource),inference(resolution,[status(thm)],[c91, c24])).
% 3.19/3.40  cnf(c201,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X141)|iext(X141,uri_rdf__1,uri_rdfs_Resource),inference(resolution,[status(thm)],[c90, c24])).
% 3.19/3.40  cnf(c200,plain,~iext(uri_rdfs_subClassOf,X140,uri_rdfs_Seq)|iext(uri_rdfs_subClassOf,X140,uri_rdfs_Container),inference(resolution,[status(thm)],[c28, c84])).
% 3.19/3.40  cnf(c199,plain,~iext(uri_rdfs_subClassOf,X139,uri_rdf_XMLLiteral)|iext(uri_rdfs_subClassOf,X139,uri_rdfs_Literal),inference(resolution,[status(thm)],[c28, c83])).
% 3.19/3.40  cnf(c198,plain,~iext(uri_rdfs_subClassOf,X138,uri_rdfs_Datatype)|iext(uri_rdfs_subClassOf,X138,uri_rdfs_Class),inference(resolution,[status(thm)],[c28, c78])).
% 3.19/3.40  cnf(c196,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X136)|iext(X136,uri_rdf__2,uri_rdfs_Resource),inference(resolution,[status(thm)],[c89, c24])).
% 3.19/3.40  cnf(c195,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X135)|iext(X135,uri_rdf__3,uri_rdfs_Resource),inference(resolution,[status(thm)],[c88, c24])).
% 3.19/3.40  cnf(c194,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X134)|iext(X134,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c87, c24])).
% 3.19/3.40  cnf(c193,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X133)|iext(X133,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c86, c24])).
% 3.19/3.40  cnf(c192,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X132)|iext(X132,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c85, c24])).
% 3.19/3.40  cnf(c191,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X131)|iext(X131,uri_rdf_predicate,uri_rdfs_Statement),inference(resolution,[status(thm)],[c24, c44])).
% 3.19/3.40  cnf(c190,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X130)|iext(X130,uri_rdf_XMLLiteral,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c24, c82])).
% 3.19/3.40  cnf(c189,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X129)|iext(X129,uri_rdf_subject,uri_rdfs_Resource),inference(resolution,[status(thm)],[c24, c41])).
% 3.19/3.40  cnf(c188,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X128)|iext(X128,uri_rdfs_subClassOf,uri_rdfs_Class),inference(resolution,[status(thm)],[c24, c32])).
% 3.19/3.40  cnf(c187,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X127)|iext(X127,uri_rdf_object,uri_rdfs_Statement),inference(resolution,[status(thm)],[c24, c46])).
% 3.19/3.40  cnf(c186,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X126)|iext(X126,uri_rdf_predicate,uri_rdfs_Resource),inference(resolution,[status(thm)],[c24, c43])).
% 3.19/3.40  cnf(c185,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X125)|iext(X125,uri_rdfs_subClassOf,uri_rdfs_Class),inference(resolution,[status(thm)],[c24, c40])).
% 3.19/3.40  cnf(c184,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X124)|iext(X124,uri_rdfs_Seq,uri_rdfs_Container),inference(resolution,[status(thm)],[c24, c84])).
% 3.19/3.40  cnf(c183,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X123)|iext(X123,uri_rdf_subject,uri_rdfs_Statement),inference(resolution,[status(thm)],[c24, c42])).
% 3.19/3.40  cnf(c182,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X122)|iext(X122,uri_rdf_Property,uri_rdfs_Class),inference(resolution,[status(thm)],[c24, c52])).
% 3.19/3.40  cnf(c181,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X121)|iext(X121,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c24, c17])).
% 3.19/3.40  cnf(c180,plain,~iext(uri_rdfs_subPropertyOf,uri_skos_altLabel,X120)|iext(X120,uri_ex_foo,literal_plain(dat_str_foo)),inference(resolution,[status(thm)],[c24, c6])).
% 3.19/3.40  cnf(c179,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X119)|iext(X119,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c24, c25])).
% 3.19/3.40  cnf(c178,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X118)|iext(X118,uri_rdfs_range,uri_rdf_Property),inference(resolution,[status(thm)],[c24, c51])).
% 3.19/3.40  cnf(c0,plain,iext(uri_rdf_type,uri_skos_prefLabel,uri_owl_AnnotationProperty),inference(split_conjunct,[status(thm)],[testcase_premise_fullish_019_Disjoint_Annotation_Properties])).
% 3.19/3.40  cnf(c176,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X116)|iext(X116,uri_skos_prefLabel,uri_owl_AnnotationProperty),inference(resolution,[status(thm)],[c24, c0])).
% 3.19/3.40  cnf(c175,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X115)|iext(X115,uri_rdf_type,uri_rdfs_Resource),inference(resolution,[status(thm)],[c24, c10])).
% 3.19/3.40  cnf(c174,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X114)|iext(X114,uri_rdf_value,uri_rdfs_Resource),inference(resolution,[status(thm)],[c24, c8])).
% 3.19/3.40  cnf(c173,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X113)|iext(X113,uri_rdf_XMLLiteral,uri_rdfs_Literal),inference(resolution,[status(thm)],[c24, c83])).
% 3.19/3.40  cnf(c172,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X112)|iext(X112,uri_rdf_type,uri_rdfs_Class),inference(resolution,[status(thm)],[c24, c9])).
% 3.19/3.40  cnf(c171,plain,~iext(uri_rdfs_subPropertyOf,uri_owl_propertyDisjointWith,X111)|iext(X111,uri_skos_prefLabel,uri_skos_altLabel),inference(resolution,[status(thm)],[c24, c4])).
% 3.19/3.40  cnf(c512,plain,icext(uri_rdf_Property,uri_rdf_first),inference(resolution,[status(thm)],[c140, c113])).
% 3.19/3.40  cnf(c170,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X110)|iext(X110,uri_rdfs_domain,uri_rdf_Property),inference(resolution,[status(thm)],[c24, c77])).
% 3.19/3.40  cnf(c169,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X109)|iext(X109,uri_rdf_value,uri_rdfs_Resource),inference(resolution,[status(thm)],[c24, c7])).
% 3.19/3.40  cnf(c168,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X108)|iext(X108,uri_skos_altLabel,uri_rdfs_label),inference(resolution,[status(thm)],[c24, c3])).
% 3.19/3.40  cnf(c167,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X107)|iext(X107,uri_rdfs_Datatype,uri_rdfs_Class),inference(resolution,[status(thm)],[c24, c78])).
% 3.19/3.40  cnf(c166,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X106)|iext(X106,uri_rdfs_domain,uri_rdfs_Class),inference(resolution,[status(thm)],[c24, c71])).
% 3.19/3.40  cnf(c165,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X105)|iext(X105,uri_skos_altLabel,uri_owl_AnnotationProperty),inference(resolution,[status(thm)],[c24, c2])).
% 3.19/3.40  cnf(c164,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X104)|iext(X104,uri_rdfs_range,uri_rdfs_Class),inference(resolution,[status(thm)],[c24, c47])).
% 3.19/3.40  cnf(c163,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X103)|iext(X103,uri_skos_prefLabel,uri_rdfs_label),inference(resolution,[status(thm)],[c24, c1])).
% 3.19/3.40  cnf(c162,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X102)|iext(X102,uri_rdfs_subPropertyOf,X102),inference(factor,[status(thm)],[c24])).
% 3.19/3.40  cnf(c153,plain,~iext(uri_rdfs_subPropertyOf,X101,uri_skos_prefLabel)|iext(uri_rdfs_subPropertyOf,X101,uri_rdfs_label),inference(resolution,[status(thm)],[c13, c1])).
% 3.19/3.40  cnf(c152,plain,~iext(uri_rdfs_subPropertyOf,X100,uri_skos_altLabel)|iext(uri_rdfs_subPropertyOf,X100,uri_rdfs_label),inference(resolution,[status(thm)],[c13, c3])).
% 3.19/3.40  cnf(c503,plain,icext(uri_rdf_List,uri_rdf_nil),inference(resolution,[status(thm)],[c139, c113])).
% 3.19/3.40  cnf(c499,plain,icext(uri_rdf_Property,uri_rdf_rest),inference(resolution,[status(thm)],[c138, c113])).
% 3.19/3.40  cnf(c488,plain,icext(uri_rdf_Property,uri_rdf__1),inference(resolution,[status(thm)],[c137, c113])).
% 3.19/3.40  cnf(c483,plain,icext(uri_rdf_Property,uri_rdf__2),inference(resolution,[status(thm)],[c136, c113])).
% 3.19/3.40  cnf(c475,plain,icext(uri_rdf_Property,uri_rdf__3),inference(resolution,[status(thm)],[c135, c113])).
% 3.19/3.40  cnf(c459,plain,icext(uri_rdf_Property,uri_rdf_object),inference(resolution,[status(thm)],[c134, c113])).
% 3.19/3.40  cnf(c447,plain,icext(uri_rdf_Property,uri_rdf_value),inference(resolution,[status(thm)],[c133, c113])).
% 3.19/3.40  cnf(c442,plain,icext(uri_rdf_Property,uri_rdf_subject),inference(resolution,[status(thm)],[c132, c113])).
% 3.19/3.40  cnf(c437,plain,icext(uri_rdf_Property,uri_rdf_type),inference(resolution,[status(thm)],[c124, c113])).
% 3.19/3.40  cnf(c394,plain,icext(uri_rdfs_Datatype,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c113, c82])).
% 3.19/3.40  cnf(c391,plain,icext(uri_owl_AnnotationProperty,uri_skos_prefLabel),inference(resolution,[status(thm)],[c113, c0])).
% 3.19/3.40  cnf(c389,plain,icext(uri_owl_AnnotationProperty,uri_skos_altLabel),inference(resolution,[status(thm)],[c113, c2])).
% 3.19/3.40  cnf(c244,plain,icext(uri_rdfs_Class,uri_rdf_Property),inference(resolution,[status(thm)],[c233, c69])).
% 3.19/3.40  fof(rdfs_datatype_instsub_literal,axiom,(![D]:(icext(uri_rdfs_Datatype,D)=>iext(uri_rdfs_subClassOf,D,uri_rdfs_Literal))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_datatype_instsub_literal)).
% 3.19/3.40  fof(c79,plain,(![D]:(~icext(uri_rdfs_Datatype,D)|iext(uri_rdfs_subClassOf,D,uri_rdfs_Literal))),inference(fof_nnf,[status(thm)],[rdfs_datatype_instsub_literal])).
% 3.19/3.40  fof(c80,plain,(![X31]:(~icext(uri_rdfs_Datatype,X31)|iext(uri_rdfs_subClassOf,X31,uri_rdfs_Literal))),inference(variable_rename,[status(thm)],[c79])).
% 3.19/3.40  cnf(c81,plain,~icext(uri_rdfs_Datatype,X85)|iext(uri_rdfs_subClassOf,X85,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[c80])).
% 3.19/3.40  cnf(c57,plain,~lv(X50)|icext(uri_rdfs_Literal,X50),inference(split_conjunct,[status(thm)],[c56])).
% 3.19/3.40  % SZS output end Saturation
% 3.19/3.40  
% 3.19/3.40  % Initial clauses    : 96
% 3.19/3.40  % Processed clauses  : 571
% 3.19/3.40  % Factors computed   : 5
% 3.19/3.40  % Resolvents computed: 1339
% 3.19/3.40  % Tautologies deleted: 52
% 3.19/3.40  % Forward subsumed   : 817
% 3.19/3.40  % Backward subsumed  : 1
% 3.19/3.40  % -------- CPU Time ---------
% 3.19/3.40  % User time          : 3.038 s
% 3.19/3.40  % System time        : 0.008 s
% 3.19/3.40  % Total time         : 3.046 s
%------------------------------------------------------------------------------