PyRes---1.5.CSA-Sat.s

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

% Computer : n012.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8042.1875MB
% OS       : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Thu May  9 17:42:45 EDT 2024

% Result   : CounterSatisfiable 2.69s 2.92s
% Output   : Saturation 2.69s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.05/0.12  % Problem  : SWB006+4 : TPTP v8.1.2. Released v5.2.0.
% 0.05/0.13  % Command  : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34  % Computer : n012.cluster.edu
% 0.13/0.34  % Model    : x86_64 x86_64
% 0.13/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34  % Memory   : 8042.1875MB
% 0.13/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34  % CPULimit : 300
% 0.13/0.34  % WCLimit  : 300
% 0.13/0.34  % DateTime : Wed May  8 22:08:08 EDT 2024
% 0.13/0.35  % CPUTime  : 
% 2.69/2.92  % Version:  1.5
% 2.69/2.92  % SZS status CounterSatisfiable
% 2.69/2.92  % SZS output start Saturation
% 2.69/2.92  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/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_subpropertyof_main)).
% 2.69/2.92  fof(c19,plain,(![P]:(![Q]:(~iext(uri_rdfs_subPropertyOf,P,Q)|((ip(P)&ip(Q))&(![X]:(![Y]:(~iext(P,X,Y)|iext(Q,X,Y)))))))),inference(fof_nnf,[status(thm)],[rdfs_subpropertyof_main])).
% 2.69/2.92  fof(c21,plain,(![X7]:(![X8]:(![X9]:(![X10]:(~iext(uri_rdfs_subPropertyOf,X7,X8)|((ip(X7)&ip(X8))&(~iext(X7,X9,X10)|iext(X8,X9,X10)))))))),inference(shift_quantors,[status(thm)],[fof(c20,plain,(![X7]:(![X8]:(~iext(uri_rdfs_subPropertyOf,X7,X8)|((ip(X7)&ip(X8))&(![X9]:(![X10]:(~iext(X7,X9,X10)|iext(X8,X9,X10)))))))),inference(variable_rename,[status(thm)],[c19])).])).
% 2.69/2.92  fof(c22,plain,(![X7]:(![X8]:(![X9]:(![X10]:(((~iext(uri_rdfs_subPropertyOf,X7,X8)|ip(X7))&(~iext(uri_rdfs_subPropertyOf,X7,X8)|ip(X8)))&(~iext(uri_rdfs_subPropertyOf,X7,X8)|(~iext(X7,X9,X10)|iext(X8,X9,X10)))))))),inference(distribute,[status(thm)],[c21])).
% 2.69/2.92  cnf(c25,plain,~iext(uri_rdfs_subPropertyOf,X64,X66)|~iext(X64,X65,X63)|iext(X66,X65,X63),inference(split_conjunct,[status(thm)],[c22])).
% 2.69/2.92  fof(rdfs_subpropertyof_reflex,axiom,(![P]:(ip(P)=>iext(uri_rdfs_subPropertyOf,P,P))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_subpropertyof_reflex)).
% 2.69/2.92  fof(c15,plain,(![P]:(~ip(P)|iext(uri_rdfs_subPropertyOf,P,P))),inference(fof_nnf,[status(thm)],[rdfs_subpropertyof_reflex])).
% 2.69/2.92  fof(c16,plain,(![X6]:(~ip(X6)|iext(uri_rdfs_subPropertyOf,X6,X6))),inference(variable_rename,[status(thm)],[c15])).
% 2.69/2.92  cnf(c17,plain,~ip(X51)|iext(uri_rdfs_subPropertyOf,X51,X51),inference(split_conjunct,[status(thm)],[c16])).
% 2.69/2.92  fof(rdf_type_ip,axiom,(![P]:(iext(uri_rdf_type,P,uri_rdf_Property)<=>ip(P))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdf_type_ip)).
% 2.69/2.92  fof(c127,plain,(![P]:((~iext(uri_rdf_type,P,uri_rdf_Property)|ip(P))&(~ip(P)|iext(uri_rdf_type,P,uri_rdf_Property)))),inference(fof_nnf,[status(thm)],[rdf_type_ip])).
% 2.69/2.92  fof(c128,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)],[c127])).
% 2.69/2.92  fof(c130,plain,(![X39]:(![X40]:((~iext(uri_rdf_type,X39,uri_rdf_Property)|ip(X39))&(~ip(X40)|iext(uri_rdf_type,X40,uri_rdf_Property))))),inference(shift_quantors,[status(thm)],[fof(c129,plain,((![X39]:(~iext(uri_rdf_type,X39,uri_rdf_Property)|ip(X39)))&(![X40]:(~ip(X40)|iext(uri_rdf_type,X40,uri_rdf_Property)))),inference(variable_rename,[status(thm)],[c128])).])).
% 2.69/2.92  cnf(c131,plain,~iext(uri_rdf_type,X95,uri_rdf_Property)|ip(X95),inference(split_conjunct,[status(thm)],[c130])).
% 2.69/2.92  fof(rdfs_cext_def,axiom,(![X]:(![C]:(iext(uri_rdf_type,X,C)<=>icext(C,X)))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_cext_def)).
% 2.69/2.92  fof(c110,plain,(![X]:(![C]:((~iext(uri_rdf_type,X,C)|icext(C,X))&(~icext(C,X)|iext(uri_rdf_type,X,C))))),inference(fof_nnf,[status(thm)],[rdfs_cext_def])).
% 2.69/2.92  fof(c111,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)],[c110])).
% 2.69/2.92  fof(c113,plain,(![X35]:(![X36]:(![X37]:(![X38]:((~iext(uri_rdf_type,X35,X36)|icext(X36,X35))&(~icext(X38,X37)|iext(uri_rdf_type,X37,X38))))))),inference(shift_quantors,[status(thm)],[fof(c112,plain,((![X35]:(![X36]:(~iext(uri_rdf_type,X35,X36)|icext(X36,X35))))&(![X37]:(![X38]:(~icext(X38,X37)|iext(uri_rdf_type,X37,X38))))),inference(variable_rename,[status(thm)],[c111])).])).
% 2.69/2.92  cnf(c115,plain,~icext(X91,X92)|iext(uri_rdf_type,X92,X91),inference(split_conjunct,[status(thm)],[c113])).
% 2.69/2.92  fof(rdfs_range_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_range,uri_rdf_Property),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_range_domain)).
% 2.69/2.92  cnf(c52,plain,iext(uri_rdfs_domain,uri_rdfs_range,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_range_domain])).
% 2.69/2.92  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/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_domain_main)).
% 2.69/2.92  fof(c73,plain,(![P]:(![C]:(![X]:(![Y]:((~iext(uri_rdfs_domain,P,C)|~iext(P,X,Y))|icext(C,X)))))),inference(fof_nnf,[status(thm)],[rdfs_domain_main])).
% 2.69/2.92  fof(c74,plain,(![P]:(![C]:(![X]:((~iext(uri_rdfs_domain,P,C)|(![Y]:~iext(P,X,Y)))|icext(C,X))))),inference(shift_quantors,[status(thm)],[c73])).
% 2.69/2.92  fof(c76,plain,(![X28]:(![X29]:(![X30]:(![X31]:((~iext(uri_rdfs_domain,X28,X29)|~iext(X28,X30,X31))|icext(X29,X30)))))),inference(shift_quantors,[status(thm)],[fof(c75,plain,(![X28]:(![X29]:(![X30]:((~iext(uri_rdfs_domain,X28,X29)|(![X31]:~iext(X28,X30,X31)))|icext(X29,X30))))),inference(variable_rename,[status(thm)],[c74])).])).
% 2.69/2.92  cnf(c77,plain,~iext(uri_rdfs_domain,X82,X84)|~iext(X82,X83,X85)|icext(X84,X83),inference(split_conjunct,[status(thm)],[c76])).
% 2.69/2.92  fof(rdfs_annotation_comment_range,axiom,iext(uri_rdfs_range,uri_rdfs_comment,uri_rdfs_Literal),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_comment_range)).
% 2.69/2.92  cnf(c123,plain,iext(uri_rdfs_range,uri_rdfs_comment,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[rdfs_annotation_comment_range])).
% 2.69/2.92  cnf(c407,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X299)|icext(X299,uri_rdfs_comment),inference(resolution,[status(thm)],[c123, c77])).
% 2.69/2.92  cnf(c1192,plain,icext(uri_rdf_Property,uri_rdfs_comment),inference(resolution,[status(thm)],[c407, c52])).
% 2.69/2.92  cnf(c1193,plain,iext(uri_rdf_type,uri_rdfs_comment,uri_rdf_Property),inference(resolution,[status(thm)],[c1192, c115])).
% 2.69/2.92  cnf(c1198,plain,ip(uri_rdfs_comment),inference(resolution,[status(thm)],[c1193, c131])).
% 2.69/2.92  cnf(c1202,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_comment,uri_rdfs_comment),inference(resolution,[status(thm)],[c1198, c17])).
% 2.69/2.92  cnf(c1210,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X596)|iext(X596,uri_rdfs_comment,uri_rdfs_comment),inference(resolution,[status(thm)],[c1202, c25])).
% 2.69/2.92  cnf(c1199,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X594)|iext(X594,uri_rdfs_comment,uri_rdf_Property),inference(resolution,[status(thm)],[c1193, c25])).
% 2.69/2.92  fof(rdfs_annotation_label_range,axiom,iext(uri_rdfs_range,uri_rdfs_label,uri_rdfs_Literal),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_label_range)).
% 2.69/2.92  cnf(c118,plain,iext(uri_rdfs_range,uri_rdfs_label,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[rdfs_annotation_label_range])).
% 2.69/2.92  cnf(c359,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X281)|icext(X281,uri_rdfs_label),inference(resolution,[status(thm)],[c118, c77])).
% 2.69/2.92  cnf(c1164,plain,icext(uri_rdf_Property,uri_rdfs_label),inference(resolution,[status(thm)],[c359, c52])).
% 2.69/2.92  cnf(c1165,plain,iext(uri_rdf_type,uri_rdfs_label,uri_rdf_Property),inference(resolution,[status(thm)],[c1164, c115])).
% 2.69/2.92  cnf(c1170,plain,ip(uri_rdfs_label),inference(resolution,[status(thm)],[c1165, c131])).
% 2.69/2.92  cnf(c1174,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_label,uri_rdfs_label),inference(resolution,[status(thm)],[c1170, c17])).
% 2.69/2.92  cnf(c1181,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X593)|iext(X593,uri_rdfs_label,uri_rdfs_label),inference(resolution,[status(thm)],[c1174, c25])).
% 2.69/2.92  cnf(c1171,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X591)|iext(X591,uri_rdfs_label,uri_rdf_Property),inference(resolution,[status(thm)],[c1165, c25])).
% 2.69/2.92  fof(rdfs_domain_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_Property),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_domain_domain)).
% 2.69/2.92  cnf(c78,plain,iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_domain_domain])).
% 2.69/2.92  fof(rdfs_reification_predicate_domain,axiom,iext(uri_rdfs_domain,uri_rdf_predicate,uri_rdfs_Statement),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_reification_predicate_domain)).
% 2.69/2.92  cnf(c45,plain,iext(uri_rdfs_domain,uri_rdf_predicate,uri_rdfs_Statement),inference(split_conjunct,[status(thm)],[rdfs_reification_predicate_domain])).
% 2.69/2.92  cnf(c289,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X228)|icext(X228,uri_rdf_predicate),inference(resolution,[status(thm)],[c77, c45])).
% 2.69/2.92  cnf(c1108,plain,icext(uri_rdf_Property,uri_rdf_predicate),inference(resolution,[status(thm)],[c289, c78])).
% 2.69/2.92  cnf(c1109,plain,iext(uri_rdf_type,uri_rdf_predicate,uri_rdf_Property),inference(resolution,[status(thm)],[c1108, c115])).
% 2.69/2.92  cnf(c1114,plain,ip(uri_rdf_predicate),inference(resolution,[status(thm)],[c1109, c131])).
% 2.69/2.92  cnf(c1118,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_predicate,uri_rdf_predicate),inference(resolution,[status(thm)],[c1114, c17])).
% 2.69/2.92  cnf(c1125,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X590)|iext(X590,uri_rdf_predicate,uri_rdf_predicate),inference(resolution,[status(thm)],[c1118, c25])).
% 2.69/2.92  cnf(c1115,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X588)|iext(X588,uri_rdf_predicate,uri_rdf_Property),inference(resolution,[status(thm)],[c1109, c25])).
% 2.69/2.92  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/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_subclassof_trans)).
% 2.69/2.92  fof(c27,plain,(![C]:(![D]:(![E]:((~iext(uri_rdfs_subClassOf,C,D)|~iext(uri_rdfs_subClassOf,D,E))|iext(uri_rdfs_subClassOf,C,E))))),inference(fof_nnf,[status(thm)],[rdfs_subclassof_trans])).
% 2.69/2.92  fof(c28,plain,(![X11]:(![X12]:(![X13]:((~iext(uri_rdfs_subClassOf,X11,X12)|~iext(uri_rdfs_subClassOf,X12,X13))|iext(uri_rdfs_subClassOf,X11,X13))))),inference(variable_rename,[status(thm)],[c27])).
% 2.69/2.92  cnf(c29,plain,~iext(uri_rdfs_subClassOf,X68,X69)|~iext(uri_rdfs_subClassOf,X69,X67)|iext(uri_rdfs_subClassOf,X68,X67),inference(split_conjunct,[status(thm)],[c28])).
% 2.69/2.92  fof(rdfs_class_instsub_resource,axiom,(![C]:(ic(C)=>iext(uri_rdfs_subClassOf,C,uri_rdfs_Resource))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_class_instsub_resource)).
% 2.69/2.92  fof(c107,plain,(![C]:(~ic(C)|iext(uri_rdfs_subClassOf,C,uri_rdfs_Resource))),inference(fof_nnf,[status(thm)],[rdfs_class_instsub_resource])).
% 2.69/2.92  fof(c108,plain,(![X34]:(~ic(X34)|iext(uri_rdfs_subClassOf,X34,uri_rdfs_Resource))),inference(variable_rename,[status(thm)],[c107])).
% 2.69/2.92  cnf(c109,plain,~ic(X88)|iext(uri_rdfs_subClassOf,X88,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[c108])).
% 2.69/2.92  fof(rdfs_ic_def,axiom,(![X]:(ic(X)<=>icext(uri_rdfs_Class,X))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_ic_def)).
% 2.69/2.92  fof(c66,plain,(![X]:((~ic(X)|icext(uri_rdfs_Class,X))&(~icext(uri_rdfs_Class,X)|ic(X)))),inference(fof_nnf,[status(thm)],[rdfs_ic_def])).
% 2.69/2.92  fof(c67,plain,((![X]:(~ic(X)|icext(uri_rdfs_Class,X)))&(![X]:(~icext(uri_rdfs_Class,X)|ic(X)))),inference(shift_quantors,[status(thm)],[c66])).
% 2.69/2.92  fof(c69,plain,(![X26]:(![X27]:((~ic(X26)|icext(uri_rdfs_Class,X26))&(~icext(uri_rdfs_Class,X27)|ic(X27))))),inference(shift_quantors,[status(thm)],[fof(c68,plain,((![X26]:(~ic(X26)|icext(uri_rdfs_Class,X26)))&(![X27]:(~icext(uri_rdfs_Class,X27)|ic(X27)))),inference(variable_rename,[status(thm)],[c67])).])).
% 2.69/2.92  cnf(c71,plain,~icext(uri_rdfs_Class,X60)|ic(X60),inference(split_conjunct,[status(thm)],[c69])).
% 2.69/2.92  fof(rdfs_domain_range,axiom,iext(uri_rdfs_range,uri_rdfs_domain,uri_rdfs_Class),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_domain_range)).
% 2.69/2.92  cnf(c72,plain,iext(uri_rdfs_range,uri_rdfs_domain,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_domain_range])).
% 2.69/2.92  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/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_range_main)).
% 2.69/2.92  fof(c49,plain,(![P]:(![C]:(![X]:(![Y]:((~iext(uri_rdfs_range,P,C)|~iext(P,X,Y))|icext(C,Y)))))),inference(fof_nnf,[status(thm)],[rdfs_range_main])).
% 2.69/2.92  fof(c50,plain,(![X18]:(![X19]:(![X20]:(![X21]:((~iext(uri_rdfs_range,X18,X19)|~iext(X18,X20,X21))|icext(X19,X21)))))),inference(variable_rename,[status(thm)],[c49])).
% 2.69/2.92  cnf(c51,plain,~iext(uri_rdfs_range,X81,X79)|~iext(X81,X80,X78)|icext(X79,X78),inference(split_conjunct,[status(thm)],[c50])).
% 2.69/2.92  cnf(c245,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X158)|icext(X158,uri_rdfs_Statement),inference(resolution,[status(thm)],[c51, c45])).
% 2.69/2.92  cnf(c984,plain,icext(uri_rdfs_Class,uri_rdfs_Statement),inference(resolution,[status(thm)],[c245, c72])).
% 2.69/2.92  cnf(c986,plain,ic(uri_rdfs_Statement),inference(resolution,[status(thm)],[c984, c71])).
% 2.69/2.92  cnf(c989,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Statement,uri_rdfs_Resource),inference(resolution,[status(thm)],[c986, c109])).
% 2.69/2.92  cnf(c1099,plain,~iext(uri_rdfs_subClassOf,X587,uri_rdfs_Statement)|iext(uri_rdfs_subClassOf,X587,uri_rdfs_Resource),inference(resolution,[status(thm)],[c989, c29])).
% 2.69/2.92  cnf(c1097,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X586)|iext(X586,uri_rdfs_Statement,uri_rdfs_Resource),inference(resolution,[status(thm)],[c989, c25])).
% 2.69/2.92  fof(rdfs_subclassof_reflex,axiom,(![C]:(ic(C)=>iext(uri_rdfs_subClassOf,C,C))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_subclassof_reflex)).
% 2.69/2.92  fof(c30,plain,(![C]:(~ic(C)|iext(uri_rdfs_subClassOf,C,C))),inference(fof_nnf,[status(thm)],[rdfs_subclassof_reflex])).
% 2.69/2.92  fof(c31,plain,(![X14]:(~ic(X14)|iext(uri_rdfs_subClassOf,X14,X14))),inference(variable_rename,[status(thm)],[c30])).
% 2.69/2.92  cnf(c32,plain,~ic(X70)|iext(uri_rdfs_subClassOf,X70,X70),inference(split_conjunct,[status(thm)],[c31])).
% 2.69/2.92  cnf(c987,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Statement,uri_rdfs_Statement),inference(resolution,[status(thm)],[c986, c32])).
% 2.69/2.92  cnf(c1089,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X584)|iext(X584,uri_rdfs_Statement,uri_rdfs_Statement),inference(resolution,[status(thm)],[c987, c25])).
% 2.69/2.92  cnf(c985,plain,iext(uri_rdf_type,uri_rdfs_Statement,uri_rdfs_Class),inference(resolution,[status(thm)],[c984, c115])).
% 2.69/2.92  cnf(c1083,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X583)|iext(X583,uri_rdfs_Statement,uri_rdfs_Class),inference(resolution,[status(thm)],[c985, c25])).
% 2.69/2.92  fof(rdfs_range_range,axiom,iext(uri_rdfs_range,uri_rdfs_range,uri_rdfs_Class),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_range_range)).
% 2.69/2.92  cnf(c48,plain,iext(uri_rdfs_range,uri_rdfs_range,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_range_range])).
% 2.69/2.92  fof(rdfs_collection_rest_range,axiom,iext(uri_rdfs_range,uri_rdf_rest,uri_rdf_List),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_collection_rest_range)).
% 2.69/2.92  cnf(c103,plain,iext(uri_rdfs_range,uri_rdf_rest,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdfs_collection_rest_range])).
% 2.69/2.92  cnf(c244,plain,~iext(uri_rdfs_range,uri_rdfs_range,X157)|icext(X157,uri_rdf_List),inference(resolution,[status(thm)],[c51, c103])).
% 2.69/2.92  cnf(c965,plain,icext(uri_rdfs_Class,uri_rdf_List),inference(resolution,[status(thm)],[c244, c48])).
% 2.69/2.92  cnf(c967,plain,ic(uri_rdf_List),inference(resolution,[status(thm)],[c965, c71])).
% 2.69/2.92  cnf(c970,plain,iext(uri_rdfs_subClassOf,uri_rdf_List,uri_rdfs_Resource),inference(resolution,[status(thm)],[c967, c109])).
% 2.69/2.92  cnf(c1078,plain,~iext(uri_rdfs_subClassOf,X582,uri_rdf_List)|iext(uri_rdfs_subClassOf,X582,uri_rdfs_Resource),inference(resolution,[status(thm)],[c970, c29])).
% 2.69/2.92  cnf(c1076,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X581)|iext(X581,uri_rdf_List,uri_rdfs_Resource),inference(resolution,[status(thm)],[c970, c25])).
% 2.69/2.92  cnf(c968,plain,iext(uri_rdfs_subClassOf,uri_rdf_List,uri_rdf_List),inference(resolution,[status(thm)],[c967, c32])).
% 2.69/2.92  cnf(c1068,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X579)|iext(X579,uri_rdf_List,uri_rdf_List),inference(resolution,[status(thm)],[c968, c25])).
% 2.69/2.92  cnf(c966,plain,iext(uri_rdf_type,uri_rdf_List,uri_rdfs_Class),inference(resolution,[status(thm)],[c965, c115])).
% 2.69/2.92  cnf(c1062,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X578)|iext(X578,uri_rdf_List,uri_rdfs_Class),inference(resolution,[status(thm)],[c966, c25])).
% 2.69/2.92  cnf(c24,plain,~iext(uri_rdfs_subPropertyOf,X61,X62)|ip(X62),inference(split_conjunct,[status(thm)],[c22])).
% 2.69/2.92  fof(rdfs_container_containermembershipproperty_instsub_member,axiom,(![P]:(icext(uri_rdfs_ContainerMembershipProperty,P)=>iext(uri_rdfs_subPropertyOf,P,uri_rdfs_member))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_containermembershipproperty_instsub_member)).
% 2.69/2.92  fof(c98,plain,(![P]:(~icext(uri_rdfs_ContainerMembershipProperty,P)|iext(uri_rdfs_subPropertyOf,P,uri_rdfs_member))),inference(fof_nnf,[status(thm)],[rdfs_container_containermembershipproperty_instsub_member])).
% 2.69/2.92  fof(c99,plain,(![X33]:(~icext(uri_rdfs_ContainerMembershipProperty,X33)|iext(uri_rdfs_subPropertyOf,X33,uri_rdfs_member))),inference(variable_rename,[status(thm)],[c98])).
% 2.69/2.92  cnf(c100,plain,~icext(uri_rdfs_ContainerMembershipProperty,X87)|iext(uri_rdfs_subPropertyOf,X87,uri_rdfs_member),inference(split_conjunct,[status(thm)],[c99])).
% 2.69/2.92  fof(rdfs_container_n_type_002,axiom,iext(uri_rdf_type,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_type_002)).
% 2.69/2.92  cnf(c87,plain,iext(uri_rdf_type,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),inference(split_conjunct,[status(thm)],[rdfs_container_n_type_002])).
% 2.69/2.92  cnf(c114,plain,~iext(uri_rdf_type,X90,X89)|icext(X89,X90),inference(split_conjunct,[status(thm)],[c113])).
% 2.69/2.92  cnf(c370,plain,icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__2),inference(resolution,[status(thm)],[c114, c87])).
% 2.69/2.92  cnf(c376,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__2,uri_rdfs_member),inference(resolution,[status(thm)],[c370, c100])).
% 2.69/2.92  cnf(c743,plain,ip(uri_rdfs_member),inference(resolution,[status(thm)],[c376, c24])).
% 2.69/2.92  cnf(c750,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_member,uri_rdfs_member),inference(resolution,[status(thm)],[c743, c17])).
% 2.69/2.92  cnf(c1049,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X577)|iext(X577,uri_rdfs_member,uri_rdfs_member),inference(resolution,[status(thm)],[c750, c25])).
% 2.69/2.92  cnf(c132,plain,~ip(X96)|iext(uri_rdf_type,X96,uri_rdf_Property),inference(split_conjunct,[status(thm)],[c130])).
% 2.69/2.92  cnf(c749,plain,iext(uri_rdf_type,uri_rdfs_member,uri_rdf_Property),inference(resolution,[status(thm)],[c743, c132])).
% 2.69/2.92  cnf(c1042,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X575)|iext(X575,uri_rdfs_member,uri_rdf_Property),inference(resolution,[status(thm)],[c749, c25])).
% 2.69/2.92  cnf(c70,plain,~ic(X59)|icext(uri_rdfs_Class,X59),inference(split_conjunct,[status(thm)],[c69])).
% 2.69/2.92  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/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_subclassof_main)).
% 2.69/2.92  fof(c34,plain,(![C]:(![D]:(~iext(uri_rdfs_subClassOf,C,D)|((ic(C)&ic(D))&(![X]:(~icext(C,X)|icext(D,X))))))),inference(fof_nnf,[status(thm)],[rdfs_subclassof_main])).
% 2.69/2.92  fof(c36,plain,(![X15]:(![X16]:(![X17]:(~iext(uri_rdfs_subClassOf,X15,X16)|((ic(X15)&ic(X16))&(~icext(X15,X17)|icext(X16,X17))))))),inference(shift_quantors,[status(thm)],[fof(c35,plain,(![X15]:(![X16]:(~iext(uri_rdfs_subClassOf,X15,X16)|((ic(X15)&ic(X16))&(![X17]:(~icext(X15,X17)|icext(X16,X17))))))),inference(variable_rename,[status(thm)],[c34])).])).
% 2.69/2.92  fof(c37,plain,(![X15]:(![X16]:(![X17]:(((~iext(uri_rdfs_subClassOf,X15,X16)|ic(X15))&(~iext(uri_rdfs_subClassOf,X15,X16)|ic(X16)))&(~iext(uri_rdfs_subClassOf,X15,X16)|(~icext(X15,X17)|icext(X16,X17))))))),inference(distribute,[status(thm)],[c36])).
% 2.69/2.92  cnf(c39,plain,~iext(uri_rdfs_subClassOf,X74,X73)|ic(X73),inference(split_conjunct,[status(thm)],[c37])).
% 2.69/2.92  fof(rdfs_container_bag_sub,axiom,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Container),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_bag_sub)).
% 2.69/2.92  cnf(c101,plain,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Container),inference(split_conjunct,[status(thm)],[rdfs_container_bag_sub])).
% 2.69/2.92  cnf(c38,plain,~iext(uri_rdfs_subClassOf,X72,X71)|ic(X72),inference(split_conjunct,[status(thm)],[c37])).
% 2.69/2.92  cnf(c207,plain,ic(uri_rdf_Bag),inference(resolution,[status(thm)],[c38, c101])).
% 2.69/2.92  cnf(c344,plain,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Resource),inference(resolution,[status(thm)],[c109, c207])).
% 2.69/2.92  cnf(c647,plain,ic(uri_rdfs_Resource),inference(resolution,[status(thm)],[c344, c39])).
% 2.69/2.92  cnf(c652,plain,icext(uri_rdfs_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c647, c70])).
% 2.69/2.92  cnf(c654,plain,iext(uri_rdf_type,uri_rdfs_Resource,uri_rdfs_Class),inference(resolution,[status(thm)],[c652, c115])).
% 2.69/2.92  cnf(c1036,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X574)|iext(X574,uri_rdfs_Resource,uri_rdfs_Class),inference(resolution,[status(thm)],[c654, c25])).
% 2.69/2.92  cnf(c651,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Resource,uri_rdfs_Resource),inference(resolution,[status(thm)],[c647, c32])).
% 2.69/2.92  cnf(c1028,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X572)|iext(X572,uri_rdfs_Resource,uri_rdfs_Resource),inference(resolution,[status(thm)],[c651, c25])).
% 2.69/2.92  fof(rdfs_annotation_isdefinedby_sub,axiom,iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_isdefinedby_sub)).
% 2.69/2.92  cnf(c120,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_sub])).
% 2.69/2.92  fof(simple_iext_property,axiom,(![S]:(![P]:(![O]:(iext(P,S,O)=>ip(P))))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', simple_iext_property)).
% 2.69/2.92  fof(c147,plain,(![S]:(![P]:(![O]:(~iext(P,S,O)|ip(P))))),inference(fof_nnf,[status(thm)],[simple_iext_property])).
% 2.69/2.92  fof(c148,plain,(![S]:(![P]:((![O]:~iext(P,S,O))|ip(P)))),inference(shift_quantors,[status(thm)],[c147])).
% 2.69/2.92  fof(c150,plain,(![X43]:(![X44]:(![X45]:(~iext(X44,X43,X45)|ip(X44))))),inference(shift_quantors,[status(thm)],[fof(c149,plain,(![X43]:(![X44]:((![X45]:~iext(X44,X43,X45))|ip(X44)))),inference(variable_rename,[status(thm)],[c148])).])).
% 2.69/2.92  cnf(c151,plain,~iext(X98,X99,X97)|ip(X98),inference(split_conjunct,[status(thm)],[c150])).
% 2.69/2.92  cnf(c543,plain,ip(uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c151, c120])).
% 2.69/2.92  cnf(c562,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c543, c17])).
% 2.69/2.92  cnf(c1021,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X571)|iext(X571,uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c562, c25])).
% 2.69/2.92  cnf(c561,plain,iext(uri_rdf_type,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c543, c132])).
% 2.69/2.92  cnf(c1013,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X569)|iext(X569,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c561, c25])).
% 2.69/2.92  fof(testcase_premise_fullish_006_Literal_Values_represented_by_URIs_and_Blank_Nodes,axiom,(?[BNODE_x]:((iext(uri_owl_sameAs,uri_ex_u,literal_plain(dat_str_abc))&iext(uri_owl_sameAs,BNODE_x,literal_plain(dat_str_abc)))&iext(uri_owl_sameAs,BNODE_x,uri_ex_w))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', testcase_premise_fullish_006_Literal_Values_represented_by_URIs_and_Blank_Nodes)).
% 2.69/2.92  fof(c0,plain,(?[X2]:((iext(uri_owl_sameAs,uri_ex_u,literal_plain(dat_str_abc))&iext(uri_owl_sameAs,X2,literal_plain(dat_str_abc)))&iext(uri_owl_sameAs,X2,uri_ex_w))),inference(variable_rename,[status(thm)],[testcase_premise_fullish_006_Literal_Values_represented_by_URIs_and_Blank_Nodes])).
% 2.69/2.92  fof(c1,plain,((iext(uri_owl_sameAs,uri_ex_u,literal_plain(dat_str_abc))&iext(uri_owl_sameAs,skolem0001,literal_plain(dat_str_abc)))&iext(uri_owl_sameAs,skolem0001,uri_ex_w)),inference(skolemize,[status(esa)],[c0])).
% 2.69/2.92  cnf(c2,plain,iext(uri_owl_sameAs,uri_ex_u,literal_plain(dat_str_abc)),inference(split_conjunct,[status(thm)],[c1])).
% 2.69/2.92  cnf(c525,plain,ip(uri_owl_sameAs),inference(resolution,[status(thm)],[c151, c2])).
% 2.69/2.92  cnf(c560,plain,iext(uri_rdfs_subPropertyOf,uri_owl_sameAs,uri_owl_sameAs),inference(resolution,[status(thm)],[c525, c17])).
% 2.69/2.92  cnf(c1003,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X568)|iext(X568,uri_owl_sameAs,uri_owl_sameAs),inference(resolution,[status(thm)],[c560, c25])).
% 2.69/2.92  cnf(c559,plain,iext(uri_rdf_type,uri_owl_sameAs,uri_rdf_Property),inference(resolution,[status(thm)],[c525, c132])).
% 2.69/2.92  cnf(c994,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X566)|iext(X566,uri_owl_sameAs,uri_rdf_Property),inference(resolution,[status(thm)],[c559, c25])).
% 2.69/2.92  fof(rdfs_datatype_sub,axiom,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Class),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_datatype_sub)).
% 2.69/2.92  cnf(c79,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_datatype_sub])).
% 2.69/2.92  cnf(c508,plain,ip(uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c151, c79])).
% 2.69/2.92  cnf(c558,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c508, c17])).
% 2.69/2.92  cnf(c977,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X565)|iext(X565,uri_rdfs_subClassOf,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c558, c25])).
% 2.69/2.92  cnf(c557,plain,iext(uri_rdf_type,uri_rdfs_subClassOf,uri_rdf_Property),inference(resolution,[status(thm)],[c508, c132])).
% 2.69/2.92  cnf(c961,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X563)|iext(X563,uri_rdfs_subClassOf,uri_rdf_Property),inference(resolution,[status(thm)],[c557, c25])).
% 2.69/2.92  cnf(c495,plain,ip(uri_rdfs_domain),inference(resolution,[status(thm)],[c151, c45])).
% 2.69/2.92  cnf(c556,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,uri_rdfs_domain),inference(resolution,[status(thm)],[c495, c17])).
% 2.69/2.92  cnf(c950,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X562)|iext(X562,uri_rdfs_domain,uri_rdfs_domain),inference(resolution,[status(thm)],[c556, c25])).
% 2.69/2.92  cnf(c555,plain,iext(uri_rdf_type,uri_rdfs_domain,uri_rdf_Property),inference(resolution,[status(thm)],[c495, c132])).
% 2.69/2.92  cnf(c932,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X560)|iext(X560,uri_rdfs_domain,uri_rdf_Property),inference(resolution,[status(thm)],[c555, c25])).
% 2.69/2.92  cnf(c490,plain,ip(uri_rdfs_range),inference(resolution,[status(thm)],[c151, c103])).
% 2.69/2.92  cnf(c554,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_range,uri_rdfs_range),inference(resolution,[status(thm)],[c490, c17])).
% 2.69/2.92  cnf(c918,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X559)|iext(X559,uri_rdfs_range,uri_rdfs_range),inference(resolution,[status(thm)],[c554, c25])).
% 2.69/2.92  cnf(c553,plain,iext(uri_rdf_type,uri_rdfs_range,uri_rdf_Property),inference(resolution,[status(thm)],[c490, c132])).
% 2.69/2.92  cnf(c905,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X557)|iext(X557,uri_rdfs_range,uri_rdf_Property),inference(resolution,[status(thm)],[c553, c25])).
% 2.69/2.92  fof(rdf_collection_first_type,axiom,iext(uri_rdf_type,uri_rdf_first,uri_rdf_Property),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdf_collection_first_type)).
% 2.69/2.92  cnf(c141,plain,iext(uri_rdf_type,uri_rdf_first,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_collection_first_type])).
% 2.69/2.92  cnf(c484,plain,ip(uri_rdf_first),inference(resolution,[status(thm)],[c141, c131])).
% 2.69/2.92  cnf(c487,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_first,uri_rdf_first),inference(resolution,[status(thm)],[c484, c17])).
% 2.69/2.92  cnf(c895,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X556)|iext(X556,uri_rdf_first,uri_rdf_first),inference(resolution,[status(thm)],[c487, c25])).
% 2.69/2.92  fof(rdf_collection_rest_type,axiom,iext(uri_rdf_type,uri_rdf_rest,uri_rdf_Property),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdf_collection_rest_type)).
% 2.69/2.92  cnf(c139,plain,iext(uri_rdf_type,uri_rdf_rest,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_collection_rest_type])).
% 2.69/2.92  cnf(c469,plain,ip(uri_rdf_rest),inference(resolution,[status(thm)],[c139, c131])).
% 2.69/2.92  cnf(c474,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_rest,uri_rdf_rest),inference(resolution,[status(thm)],[c469, c17])).
% 2.69/2.92  cnf(c887,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X554)|iext(X554,uri_rdf_rest,uri_rdf_rest),inference(resolution,[status(thm)],[c474, c25])).
% 2.69/2.92  fof(rdf_container_n_type_001,axiom,iext(uri_rdf_type,uri_rdf__1,uri_rdf_Property),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdf_container_n_type_001)).
% 2.69/2.92  cnf(c138,plain,iext(uri_rdf_type,uri_rdf__1,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_container_n_type_001])).
% 2.69/2.92  cnf(c464,plain,ip(uri_rdf__1),inference(resolution,[status(thm)],[c138, c131])).
% 2.69/2.92  cnf(c472,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__1,uri_rdf__1),inference(resolution,[status(thm)],[c464, c17])).
% 2.69/2.92  cnf(c880,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X552)|iext(X552,uri_rdf__1,uri_rdf__1),inference(resolution,[status(thm)],[c472, c25])).
% 2.69/2.92  fof(rdf_container_n_type_002,axiom,iext(uri_rdf_type,uri_rdf__2,uri_rdf_Property),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdf_container_n_type_002)).
% 2.69/2.92  cnf(c137,plain,iext(uri_rdf_type,uri_rdf__2,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_container_n_type_002])).
% 2.69/2.92  cnf(c453,plain,ip(uri_rdf__2),inference(resolution,[status(thm)],[c137, c131])).
% 2.69/2.92  cnf(c458,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__2,uri_rdf__2),inference(resolution,[status(thm)],[c453, c17])).
% 2.69/2.92  cnf(c873,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X550)|iext(X550,uri_rdf__2,uri_rdf__2),inference(resolution,[status(thm)],[c458, c25])).
% 2.69/2.92  fof(rdf_container_n_type_003,axiom,iext(uri_rdf_type,uri_rdf__3,uri_rdf_Property),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdf_container_n_type_003)).
% 2.69/2.92  cnf(c136,plain,iext(uri_rdf_type,uri_rdf__3,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_container_n_type_003])).
% 2.69/2.92  cnf(c448,plain,ip(uri_rdf__3),inference(resolution,[status(thm)],[c136, c131])).
% 2.69/2.92  cnf(c456,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__3,uri_rdf__3),inference(resolution,[status(thm)],[c448, c17])).
% 2.69/2.92  cnf(c865,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X548)|iext(X548,uri_rdf__3,uri_rdf__3),inference(resolution,[status(thm)],[c456, c25])).
% 2.69/2.92  fof(rdf_reification_object_type,axiom,iext(uri_rdf_type,uri_rdf_object,uri_rdf_Property),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdf_reification_object_type)).
% 2.69/2.92  cnf(c135,plain,iext(uri_rdf_type,uri_rdf_object,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_reification_object_type])).
% 2.69/2.92  cnf(c440,plain,ip(uri_rdf_object),inference(resolution,[status(thm)],[c135, c131])).
% 2.69/2.92  cnf(c443,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_object,uri_rdf_object),inference(resolution,[status(thm)],[c440, c17])).
% 2.69/2.92  cnf(c857,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X546)|iext(X546,uri_rdf_object,uri_rdf_object),inference(resolution,[status(thm)],[c443, c25])).
% 2.69/2.92  cnf(c363,plain,ip(uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c120, c24])).
% 2.69/2.92  cnf(c435,plain,iext(uri_rdf_type,uri_rdfs_seeAlso,uri_rdf_Property),inference(resolution,[status(thm)],[c132, c363])).
% 2.69/2.92  cnf(c850,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X544)|iext(X544,uri_rdfs_seeAlso,uri_rdf_Property),inference(resolution,[status(thm)],[c435, c25])).
% 2.69/2.92  cnf(c23,plain,~iext(uri_rdfs_subPropertyOf,X56,X57)|ip(X56),inference(split_conjunct,[status(thm)],[c22])).
% 2.69/2.92  cnf(c367,plain,ip(uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c120, c23])).
% 2.69/2.92  cnf(c434,plain,iext(uri_rdf_type,uri_rdfs_isDefinedBy,uri_rdf_Property),inference(resolution,[status(thm)],[c132, c367])).
% 2.69/2.92  cnf(c842,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X543)|iext(X543,uri_rdfs_isDefinedBy,uri_rdf_Property),inference(resolution,[status(thm)],[c434, c25])).
% 2.69/2.92  fof(rdf_reification_predicate_type,axiom,iext(uri_rdf_type,uri_rdf_value,uri_rdf_Property),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdf_reification_predicate_type)).
% 2.69/2.92  cnf(c134,plain,iext(uri_rdf_type,uri_rdf_value,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_reification_predicate_type])).
% 2.69/2.92  cnf(c428,plain,ip(uri_rdf_value),inference(resolution,[status(thm)],[c134, c131])).
% 2.69/2.92  cnf(c430,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_value,uri_rdf_value),inference(resolution,[status(thm)],[c428, c17])).
% 2.69/2.92  cnf(c835,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X542)|iext(X542,uri_rdf_value,uri_rdf_value),inference(resolution,[status(thm)],[c430, c25])).
% 2.69/2.92  fof(rdf_reification_subject_type,axiom,iext(uri_rdf_type,uri_rdf_subject,uri_rdf_Property),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdf_reification_subject_type)).
% 2.69/2.92  cnf(c133,plain,iext(uri_rdf_type,uri_rdf_subject,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_reification_subject_type])).
% 2.69/2.92  cnf(c421,plain,ip(uri_rdf_subject),inference(resolution,[status(thm)],[c131, c133])).
% 2.69/2.92  cnf(c423,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_subject,uri_rdf_subject),inference(resolution,[status(thm)],[c421, c17])).
% 2.69/2.92  cnf(c828,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X540)|iext(X540,uri_rdf_subject,uri_rdf_subject),inference(resolution,[status(thm)],[c423, c25])).
% 2.69/2.92  fof(rdf_value_type,axiom,iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdf_value_type)).
% 2.69/2.93  cnf(c125,plain,iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_value_type])).
% 2.69/2.93  cnf(c420,plain,ip(uri_rdf_type),inference(resolution,[status(thm)],[c131, c125])).
% 2.69/2.93  cnf(c422,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_type,uri_rdf_type),inference(resolution,[status(thm)],[c420, c17])).
% 2.69/2.93  cnf(c819,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X538)|iext(X538,uri_rdf_type,uri_rdf_type),inference(resolution,[status(thm)],[c422, c25])).
% 2.69/2.93  fof(rdfs_container_n_type_001,axiom,iext(uri_rdf_type,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_type_001)).
% 2.69/2.93  cnf(c88,plain,iext(uri_rdf_type,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),inference(split_conjunct,[status(thm)],[rdfs_container_n_type_001])).
% 2.69/2.93  cnf(c374,plain,icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__1),inference(resolution,[status(thm)],[c114, c88])).
% 2.69/2.93  cnf(c394,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__1,uri_rdfs_member),inference(resolution,[status(thm)],[c374, c100])).
% 2.69/2.93  cnf(c809,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X536)|iext(X536,uri_rdf__1,uri_rdfs_member),inference(resolution,[status(thm)],[c394, c25])).
% 2.69/2.93  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/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_subpropertyof_trans)).
% 2.69/2.93  fof(c12,plain,(![P]:(![Q]:(![R]:((~iext(uri_rdfs_subPropertyOf,P,Q)|~iext(uri_rdfs_subPropertyOf,Q,R))|iext(uri_rdfs_subPropertyOf,P,R))))),inference(fof_nnf,[status(thm)],[rdfs_subpropertyof_trans])).
% 2.69/2.93  fof(c13,plain,(![X3]:(![X4]:(![X5]:((~iext(uri_rdfs_subPropertyOf,X3,X4)|~iext(uri_rdfs_subPropertyOf,X4,X5))|iext(uri_rdfs_subPropertyOf,X3,X5))))),inference(variable_rename,[status(thm)],[c12])).
% 2.69/2.93  cnf(c14,plain,~iext(uri_rdfs_subPropertyOf,X48,X49)|~iext(uri_rdfs_subPropertyOf,X49,X50)|iext(uri_rdfs_subPropertyOf,X48,X50),inference(split_conjunct,[status(thm)],[c13])).
% 2.69/2.93  cnf(c808,plain,~iext(uri_rdfs_subPropertyOf,X535,uri_rdf__1)|iext(uri_rdfs_subPropertyOf,X535,uri_rdfs_member),inference(resolution,[status(thm)],[c394, c14])).
% 2.69/2.93  fof(rdfs_container_seq_sub,axiom,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Container),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_seq_sub)).
% 2.69/2.93  cnf(c85,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Container),inference(split_conjunct,[status(thm)],[rdfs_container_seq_sub])).
% 2.69/2.93  cnf(c206,plain,ic(uri_rdfs_Seq),inference(resolution,[status(thm)],[c38, c85])).
% 2.69/2.93  cnf(c216,plain,icext(uri_rdfs_Class,uri_rdfs_Seq),inference(resolution,[status(thm)],[c206, c70])).
% 2.69/2.93  cnf(c391,plain,iext(uri_rdf_type,uri_rdfs_Seq,uri_rdfs_Class),inference(resolution,[status(thm)],[c115, c216])).
% 2.69/2.93  cnf(c803,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X534)|iext(X534,uri_rdfs_Seq,uri_rdfs_Class),inference(resolution,[status(thm)],[c391, c25])).
% 2.69/2.93  cnf(c218,plain,icext(uri_rdfs_Class,uri_rdf_Bag),inference(resolution,[status(thm)],[c207, c70])).
% 2.69/2.93  cnf(c390,plain,iext(uri_rdf_type,uri_rdf_Bag,uri_rdfs_Class),inference(resolution,[status(thm)],[c115, c218])).
% 2.69/2.93  cnf(c798,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X533)|iext(X533,uri_rdf_Bag,uri_rdfs_Class),inference(resolution,[status(thm)],[c390, c25])).
% 2.69/2.93  fof(rdfs_container_alt_sub,axiom,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Container),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_alt_sub)).
% 2.69/2.93  cnf(c102,plain,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Container),inference(split_conjunct,[status(thm)],[rdfs_container_alt_sub])).
% 2.69/2.93  cnf(c208,plain,ic(uri_rdf_Alt),inference(resolution,[status(thm)],[c38, c102])).
% 2.69/2.93  cnf(c226,plain,icext(uri_rdfs_Class,uri_rdf_Alt),inference(resolution,[status(thm)],[c208, c70])).
% 2.69/2.93  cnf(c388,plain,iext(uri_rdf_type,uri_rdf_Alt,uri_rdfs_Class),inference(resolution,[status(thm)],[c115, c226])).
% 2.69/2.93  cnf(c793,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X532)|iext(X532,uri_rdf_Alt,uri_rdfs_Class),inference(resolution,[status(thm)],[c388, c25])).
% 2.69/2.93  cnf(c203,plain,ic(uri_rdfs_Datatype),inference(resolution,[status(thm)],[c38, c79])).
% 2.69/2.93  cnf(c210,plain,icext(uri_rdfs_Class,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c203, c70])).
% 2.69/2.93  cnf(c386,plain,iext(uri_rdf_type,uri_rdfs_Datatype,uri_rdfs_Class),inference(resolution,[status(thm)],[c115, c210])).
% 2.69/2.93  cnf(c787,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X531)|iext(X531,uri_rdfs_Datatype,uri_rdfs_Class),inference(resolution,[status(thm)],[c386, c25])).
% 2.69/2.93  fof(rdfs_dat_xmlliteral_sub,axiom,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Literal),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_dat_xmlliteral_sub)).
% 2.69/2.93  cnf(c84,plain,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[rdfs_dat_xmlliteral_sub])).
% 2.69/2.93  cnf(c204,plain,ic(uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c38, c84])).
% 2.69/2.93  cnf(c212,plain,icext(uri_rdfs_Class,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c204, c70])).
% 2.69/2.93  cnf(c385,plain,iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Class),inference(resolution,[status(thm)],[c115, c212])).
% 2.69/2.93  cnf(c782,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X530)|iext(X530,uri_rdf_XMLLiteral,uri_rdfs_Class),inference(resolution,[status(thm)],[c385, c25])).
% 2.69/2.93  cnf(c220,plain,ic(uri_rdfs_Literal),inference(resolution,[status(thm)],[c39, c84])).
% 2.69/2.93  cnf(c230,plain,icext(uri_rdfs_Class,uri_rdfs_Literal),inference(resolution,[status(thm)],[c220, c70])).
% 2.69/2.93  cnf(c383,plain,iext(uri_rdf_type,uri_rdfs_Literal,uri_rdfs_Class),inference(resolution,[status(thm)],[c115, c230])).
% 2.69/2.93  cnf(c776,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X529)|iext(X529,uri_rdfs_Literal,uri_rdfs_Class),inference(resolution,[status(thm)],[c383, c25])).
% 2.69/2.93  cnf(c219,plain,ic(uri_rdfs_Class),inference(resolution,[status(thm)],[c39, c79])).
% 2.69/2.93  cnf(c228,plain,icext(uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c219, c70])).
% 2.69/2.93  cnf(c382,plain,iext(uri_rdf_type,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c115, c228])).
% 2.69/2.93  cnf(c770,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X528)|iext(X528,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c382, c25])).
% 2.69/2.93  fof(rdfs_container_containermembershipproperty_sub,axiom,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_containermembershipproperty_sub)).
% 2.69/2.93  cnf(c97,plain,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_container_containermembershipproperty_sub])).
% 2.69/2.93  cnf(c205,plain,ic(uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c38, c97])).
% 2.69/2.93  cnf(c214,plain,icext(uri_rdfs_Class,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c205, c70])).
% 2.69/2.93  cnf(c380,plain,iext(uri_rdf_type,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Class),inference(resolution,[status(thm)],[c115, c214])).
% 2.69/2.93  cnf(c765,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X527)|iext(X527,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Class),inference(resolution,[status(thm)],[c380, c25])).
% 2.69/2.93  cnf(c222,plain,ic(uri_rdfs_Container),inference(resolution,[status(thm)],[c39, c85])).
% 2.69/2.93  cnf(c234,plain,icext(uri_rdfs_Class,uri_rdfs_Container),inference(resolution,[status(thm)],[c222, c70])).
% 2.69/2.93  cnf(c379,plain,iext(uri_rdf_type,uri_rdfs_Container,uri_rdfs_Class),inference(resolution,[status(thm)],[c115, c234])).
% 2.69/2.93  cnf(c760,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X526)|iext(X526,uri_rdfs_Container,uri_rdfs_Class),inference(resolution,[status(thm)],[c379, c25])).
% 2.69/2.93  fof(rdfs_container_n_type_003,axiom,iext(uri_rdf_type,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_type_003)).
% 2.69/2.93  cnf(c86,plain,iext(uri_rdf_type,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),inference(split_conjunct,[status(thm)],[rdfs_container_n_type_003])).
% 2.69/2.93  cnf(c372,plain,icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__3),inference(resolution,[status(thm)],[c114, c86])).
% 2.69/2.93  cnf(c378,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__3,uri_rdfs_member),inference(resolution,[status(thm)],[c372, c100])).
% 2.69/2.93  cnf(c754,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X525)|iext(X525,uri_rdf__3,uri_rdfs_member),inference(resolution,[status(thm)],[c378, c25])).
% 2.69/2.93  cnf(c753,plain,~iext(uri_rdfs_subPropertyOf,X524,uri_rdf__3)|iext(uri_rdfs_subPropertyOf,X524,uri_rdfs_member),inference(resolution,[status(thm)],[c378, c14])).
% 2.69/2.93  cnf(c745,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X523)|iext(X523,uri_rdf__2,uri_rdfs_member),inference(resolution,[status(thm)],[c376, c25])).
% 2.69/2.93  cnf(c744,plain,~iext(uri_rdfs_subPropertyOf,X522,uri_rdf__2)|iext(uri_rdfs_subPropertyOf,X522,uri_rdfs_member),inference(resolution,[status(thm)],[c376, c14])).
% 2.69/2.93  cnf(c375,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c367, c17])).
% 2.69/2.93  cnf(c738,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X521)|iext(X521,uri_rdfs_isDefinedBy,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c375, c25])).
% 2.69/2.93  cnf(c1207,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X519)|icext(X519,uri_rdfs_comment),inference(resolution,[status(thm)],[c1202, c77])).
% 2.69/2.93  cnf(c1206,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X518)|icext(X518,uri_rdfs_comment),inference(resolution,[status(thm)],[c1202, c51])).
% 2.69/2.93  cnf(c369,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_seeAlso,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c363, c17])).
% 2.69/2.93  cnf(c731,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X517)|iext(X517,uri_rdfs_seeAlso,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c369, c25])).
% 2.69/2.93  cnf(c1178,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X514)|icext(X514,uri_rdfs_label),inference(resolution,[status(thm)],[c1174, c77])).
% 2.69/2.93  cnf(c1177,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X512)|icext(X512,uri_rdfs_label),inference(resolution,[status(thm)],[c1174, c51])).
% 2.69/2.93  cnf(c221,plain,ic(uri_rdf_Property),inference(resolution,[status(thm)],[c39, c97])).
% 2.69/2.93  cnf(c353,plain,iext(uri_rdfs_subClassOf,uri_rdf_Property,uri_rdfs_Resource),inference(resolution,[status(thm)],[c109, c221])).
% 2.69/2.93  cnf(c725,plain,~iext(uri_rdfs_subClassOf,X509,uri_rdf_Property)|iext(uri_rdfs_subClassOf,X509,uri_rdfs_Resource),inference(resolution,[status(thm)],[c353, c29])).
% 2.69/2.93  cnf(c1122,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X508)|icext(X508,uri_rdf_predicate),inference(resolution,[status(thm)],[c1118, c77])).
% 2.69/2.93  cnf(c1121,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X507)|icext(X507,uri_rdf_predicate),inference(resolution,[status(thm)],[c1118, c51])).
% 2.69/2.93  cnf(c723,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X506)|iext(X506,uri_rdf_Property,uri_rdfs_Resource),inference(resolution,[status(thm)],[c353, c25])).
% 2.69/2.93  cnf(c352,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c109, c219])).
% 2.69/2.93  cnf(c717,plain,~iext(uri_rdfs_subClassOf,X502,uri_rdfs_Class)|iext(uri_rdfs_subClassOf,X502,uri_rdfs_Resource),inference(resolution,[status(thm)],[c352, c29])).
% 2.69/2.93  cnf(c1093,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X500)|icext(X500,uri_rdfs_Statement),inference(resolution,[status(thm)],[c987, c77])).
% 2.69/2.93  cnf(c715,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X499)|iext(X499,uri_rdfs_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c352, c25])).
% 2.69/2.93  cnf(c1092,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X498)|icext(X498,uri_rdfs_Statement),inference(resolution,[status(thm)],[c987, c51])).
% 2.69/2.93  cnf(c351,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Literal,uri_rdfs_Resource),inference(resolution,[status(thm)],[c109, c220])).
% 2.69/2.93  cnf(c709,plain,~iext(uri_rdfs_subClassOf,X495,uri_rdfs_Literal)|iext(uri_rdfs_subClassOf,X495,uri_rdfs_Resource),inference(resolution,[status(thm)],[c351, c29])).
% 2.69/2.93  cnf(c1072,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X492)|icext(X492,uri_rdf_List),inference(resolution,[status(thm)],[c968, c77])).
% 2.69/2.93  cnf(c707,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X491)|iext(X491,uri_rdfs_Literal,uri_rdfs_Resource),inference(resolution,[status(thm)],[c351, c25])).
% 2.69/2.93  cnf(c1071,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X490)|icext(X490,uri_rdf_List),inference(resolution,[status(thm)],[c968, c51])).
% 2.69/2.93  cnf(c350,plain,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Resource),inference(resolution,[status(thm)],[c109, c204])).
% 2.69/2.93  cnf(c701,plain,~iext(uri_rdfs_subClassOf,X487,uri_rdf_XMLLiteral)|iext(uri_rdfs_subClassOf,X487,uri_rdfs_Resource),inference(resolution,[status(thm)],[c350, c29])).
% 2.69/2.93  cnf(c1052,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X486)|icext(X486,uri_rdfs_member),inference(resolution,[status(thm)],[c750, c77])).
% 2.69/2.93  cnf(c699,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X483)|iext(X483,uri_rdf_XMLLiteral,uri_rdfs_Resource),inference(resolution,[status(thm)],[c350, c25])).
% 2.69/2.93  cnf(c349,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Container,uri_rdfs_Resource),inference(resolution,[status(thm)],[c109, c222])).
% 2.69/2.93  cnf(c693,plain,~iext(uri_rdfs_subClassOf,X481,uri_rdfs_Container)|iext(uri_rdfs_subClassOf,X481,uri_rdfs_Resource),inference(resolution,[status(thm)],[c349, c29])).
% 2.69/2.93  cnf(c1032,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X478)|icext(X478,uri_rdfs_Resource),inference(resolution,[status(thm)],[c651, c77])).
% 2.69/2.93  cnf(c691,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X477)|iext(X477,uri_rdfs_Container,uri_rdfs_Resource),inference(resolution,[status(thm)],[c349, c25])).
% 2.69/2.93  cnf(c1024,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X475)|icext(X475,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c562, c77])).
% 2.69/2.93  cnf(c348,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Resource),inference(resolution,[status(thm)],[c109, c206])).
% 2.69/2.93  cnf(c685,plain,~iext(uri_rdfs_subClassOf,X474,uri_rdfs_Seq)|iext(uri_rdfs_subClassOf,X474,uri_rdfs_Resource),inference(resolution,[status(thm)],[c348, c29])).
% 2.69/2.93  cnf(c1022,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X473)|icext(X473,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c562, c51])).
% 2.69/2.93  cnf(c683,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X470)|iext(X470,uri_rdfs_Seq,uri_rdfs_Resource),inference(resolution,[status(thm)],[c348, c25])).
% 2.69/2.93  cnf(c1008,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X469)|icext(X469,uri_owl_sameAs),inference(resolution,[status(thm)],[c560, c77])).
% 2.69/2.93  cnf(c1005,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X468)|icext(X468,uri_owl_sameAs),inference(resolution,[status(thm)],[c560, c51])).
% 2.69/2.93  cnf(c347,plain,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Resource),inference(resolution,[status(thm)],[c109, c208])).
% 2.69/2.93  cnf(c677,plain,~iext(uri_rdfs_subClassOf,X466,uri_rdf_Alt)|iext(uri_rdfs_subClassOf,X466,uri_rdfs_Resource),inference(resolution,[status(thm)],[c347, c29])).
% 2.69/2.93  cnf(c983,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X464)|icext(X464,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c558, c77])).
% 2.69/2.93  cnf(c675,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X463)|iext(X463,uri_rdf_Alt,uri_rdfs_Resource),inference(resolution,[status(thm)],[c347, c25])).
% 2.69/2.93  cnf(c980,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X462)|icext(X462,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c558, c51])).
% 2.69/2.93  cnf(c346,plain,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Resource),inference(resolution,[status(thm)],[c109, c205])).
% 2.69/2.93  cnf(c669,plain,~iext(uri_rdfs_subClassOf,X459,uri_rdfs_ContainerMembershipProperty)|iext(uri_rdfs_subClassOf,X459,uri_rdfs_Resource),inference(resolution,[status(thm)],[c346, c29])).
% 2.69/2.93  cnf(c956,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X458)|icext(X458,uri_rdfs_domain),inference(resolution,[status(thm)],[c556, c77])).
% 2.69/2.93  cnf(c952,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X457)|icext(X457,uri_rdfs_domain),inference(resolution,[status(thm)],[c556, c51])).
% 2.69/2.93  cnf(c667,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X455)|iext(X455,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Resource),inference(resolution,[status(thm)],[c346, c25])).
% 2.69/2.93  cnf(c926,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X453)|icext(X453,uri_rdfs_range),inference(resolution,[status(thm)],[c554, c77])).
% 2.69/2.93  cnf(c345,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Resource),inference(resolution,[status(thm)],[c109, c203])).
% 2.69/2.93  cnf(c661,plain,~iext(uri_rdfs_subClassOf,X452,uri_rdfs_Datatype)|iext(uri_rdfs_subClassOf,X452,uri_rdfs_Resource),inference(resolution,[status(thm)],[c345, c29])).
% 2.69/2.93  cnf(c923,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X451)|icext(X451,uri_rdfs_range),inference(resolution,[status(thm)],[c554, c51])).
% 2.69/2.93  cnf(c659,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X448)|iext(X448,uri_rdfs_Datatype,uri_rdfs_Resource),inference(resolution,[status(thm)],[c345, c25])).
% 2.69/2.93  cnf(c898,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X447)|icext(X447,uri_rdf_first),inference(resolution,[status(thm)],[c487, c77])).
% 2.69/2.93  cnf(c896,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X446)|icext(X446,uri_rdf_first),inference(resolution,[status(thm)],[c487, c51])).
% 2.69/2.93  cnf(c648,plain,~iext(uri_rdfs_subClassOf,X445,uri_rdf_Bag)|iext(uri_rdfs_subClassOf,X445,uri_rdfs_Resource),inference(resolution,[status(thm)],[c344, c29])).
% 2.69/2.93  cnf(c890,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X444)|icext(X444,uri_rdf_rest),inference(resolution,[status(thm)],[c474, c77])).
% 2.69/2.93  cnf(c888,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X443)|icext(X443,uri_rdf_rest),inference(resolution,[status(thm)],[c474, c51])).
% 2.69/2.93  cnf(c646,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X441)|iext(X441,uri_rdf_Bag,uri_rdfs_Resource),inference(resolution,[status(thm)],[c344, c25])).
% 2.69/2.93  cnf(c881,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X440)|icext(X440,uri_rdf__1),inference(resolution,[status(thm)],[c472, c51])).
% 2.69/2.93  cnf(c874,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X438)|icext(X438,uri_rdf__2),inference(resolution,[status(thm)],[c458, c51])).
% 2.69/2.93  cnf(c866,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X435)|icext(X435,uri_rdf__3),inference(resolution,[status(thm)],[c456, c51])).
% 2.69/2.93  cnf(c233,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Container,uri_rdfs_Container),inference(resolution,[status(thm)],[c222, c32])).
% 2.69/2.93  cnf(c638,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X434)|iext(X434,uri_rdfs_Container,uri_rdfs_Container),inference(resolution,[status(thm)],[c233, c25])).
% 2.69/2.93  cnf(c860,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X433)|icext(X433,uri_rdf_object),inference(resolution,[status(thm)],[c443, c77])).
% 2.69/2.93  cnf(c858,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X432)|icext(X432,uri_rdf_object),inference(resolution,[status(thm)],[c443, c51])).
% 2.69/2.93  cnf(c838,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X426)|icext(X426,uri_rdf_value),inference(resolution,[status(thm)],[c430, c77])).
% 2.69/2.93  cnf(c231,plain,iext(uri_rdfs_subClassOf,uri_rdf_Property,uri_rdf_Property),inference(resolution,[status(thm)],[c221, c32])).
% 2.69/2.93  cnf(c630,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X425)|iext(X425,uri_rdf_Property,uri_rdf_Property),inference(resolution,[status(thm)],[c231, c25])).
% 2.69/2.93  cnf(c836,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X424)|icext(X424,uri_rdf_value),inference(resolution,[status(thm)],[c430, c51])).
% 2.69/2.93  cnf(c831,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X423)|icext(X423,uri_rdf_subject),inference(resolution,[status(thm)],[c423, c77])).
% 2.69/2.93  cnf(c829,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X421)|icext(X421,uri_rdf_subject),inference(resolution,[status(thm)],[c423, c51])).
% 2.69/2.93  cnf(c823,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X420)|icext(X420,uri_rdf_type),inference(resolution,[status(thm)],[c422, c77])).
% 2.69/2.93  cnf(c229,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Literal,uri_rdfs_Literal),inference(resolution,[status(thm)],[c220, c32])).
% 2.69/2.93  cnf(c622,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X419)|iext(X419,uri_rdfs_Literal,uri_rdfs_Literal),inference(resolution,[status(thm)],[c229, c25])).
% 2.69/2.93  cnf(c821,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X418)|icext(X418,uri_rdf_type),inference(resolution,[status(thm)],[c422, c51])).
% 2.69/2.93  cnf(c812,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X417)|icext(X417,uri_rdf__1),inference(resolution,[status(thm)],[c394, c77])).
% 2.69/2.93  cnf(c227,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c219, c32])).
% 2.69/2.93  cnf(c614,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X409)|iext(X409,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c227, c25])).
% 2.69/2.93  cnf(c225,plain,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdf_Alt),inference(resolution,[status(thm)],[c208, c32])).
% 2.69/2.93  cnf(c606,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X398)|iext(X398,uri_rdf_Alt,uri_rdf_Alt),inference(resolution,[status(thm)],[c225, c25])).
% 2.69/2.93  cnf(c757,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X392)|icext(X392,uri_rdf__3),inference(resolution,[status(thm)],[c378, c77])).
% 2.69/2.93  cnf(c748,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X390)|icext(X390,uri_rdf__2),inference(resolution,[status(thm)],[c376, c77])).
% 2.69/2.93  cnf(c217,plain,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdf_Bag),inference(resolution,[status(thm)],[c207, c32])).
% 2.69/2.93  cnf(c598,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X389)|iext(X389,uri_rdf_Bag,uri_rdf_Bag),inference(resolution,[status(thm)],[c217, c25])).
% 2.69/2.93  cnf(c746,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X388)|icext(X388,uri_rdfs_member),inference(resolution,[status(thm)],[c376, c51])).
% 2.69/2.93  cnf(c739,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X386)|icext(X386,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c375, c51])).
% 2.69/2.93  cnf(c734,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X384)|icext(X384,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c369, c77])).
% 2.69/2.93  cnf(c215,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Seq),inference(resolution,[status(thm)],[c206, c32])).
% 2.69/2.93  cnf(c590,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X381)|iext(X381,uri_rdfs_Seq,uri_rdfs_Seq),inference(resolution,[status(thm)],[c215, c25])).
% 2.69/2.93  cnf(c213,plain,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c205, c32])).
% 2.69/2.93  cnf(c582,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X370)|iext(X370,uri_rdfs_ContainerMembershipProperty,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c213, c25])).
% 2.69/2.93  cnf(c211,plain,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c204, c32])).
% 2.69/2.93  cnf(c574,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X359)|iext(X359,uri_rdf_XMLLiteral,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c211, c25])).
% 2.69/2.93  cnf(c649,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X358)|icext(X358,uri_rdfs_Resource),inference(resolution,[status(thm)],[c344, c51])).
% 2.69/2.93  cnf(c642,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X357)|icext(X357,uri_rdfs_Container),inference(resolution,[status(thm)],[c233, c77])).
% 2.69/2.93  cnf(c634,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X354)|icext(X354,uri_rdf_Property),inference(resolution,[status(thm)],[c231, c77])).
% 2.69/2.93  cnf(c209,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c203, c32])).
% 2.69/2.93  cnf(c566,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X352)|iext(X352,uri_rdfs_Datatype,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c209, c25])).
% 2.69/2.93  cnf(c626,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X351)|icext(X351,uri_rdfs_Literal),inference(resolution,[status(thm)],[c229, c77])).
% 2.69/2.93  cnf(c618,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X349)|icext(X349,uri_rdfs_Class),inference(resolution,[status(thm)],[c227, c77])).
% 2.69/2.93  cnf(c482,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X348)|iext(X348,uri_rdf_first,uri_rdf_Property),inference(resolution,[status(thm)],[c141, c25])).
% 2.69/2.93  cnf(c609,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X345)|icext(X345,uri_rdf_Alt),inference(resolution,[status(thm)],[c225, c51])).
% 2.69/2.93  fof(rdf_collection_nil_type,axiom,iext(uri_rdf_type,uri_rdf_nil,uri_rdf_List),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdf_collection_nil_type)).
% 2.69/2.93  cnf(c140,plain,iext(uri_rdf_type,uri_rdf_nil,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdf_collection_nil_type])).
% 2.69/2.93  cnf(c478,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X344)|iext(X344,uri_rdf_nil,uri_rdf_List),inference(resolution,[status(thm)],[c140, c25])).
% 2.69/2.93  cnf(c601,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X342)|icext(X342,uri_rdf_Bag),inference(resolution,[status(thm)],[c217, c51])).
% 2.69/2.93  cnf(c467,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X340)|iext(X340,uri_rdf_rest,uri_rdf_Property),inference(resolution,[status(thm)],[c139, c25])).
% 2.69/2.93  cnf(c593,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X339)|icext(X339,uri_rdfs_Seq),inference(resolution,[status(thm)],[c215, c51])).
% 2.69/2.93  cnf(c462,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X337)|iext(X337,uri_rdf__1,uri_rdf_Property),inference(resolution,[status(thm)],[c138, c25])).
% 2.69/2.93  cnf(c585,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X336)|icext(X336,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c213, c51])).
% 2.69/2.93  cnf(c577,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X334)|icext(X334,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c211, c51])).
% 2.69/2.93  cnf(c451,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X333)|iext(X333,uri_rdf__2,uri_rdf_Property),inference(resolution,[status(thm)],[c137, c25])).
% 2.69/2.93  cnf(c569,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X331)|icext(X331,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c209, c51])).
% 2.69/2.93  cnf(c446,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X329)|iext(X329,uri_rdf__3,uri_rdf_Property),inference(resolution,[status(thm)],[c136, c25])).
% 2.69/2.93  cnf(c477,plain,~iext(uri_rdfs_range,uri_rdf_type,X326)|icext(X326,uri_rdf_List),inference(resolution,[status(thm)],[c140, c51])).
% 2.69/2.93  cnf(c438,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X325)|iext(X325,uri_rdf_object,uri_rdf_Property),inference(resolution,[status(thm)],[c135, c25])).
% 2.69/2.93  cnf(c426,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X320)|iext(X320,uri_rdf_value,uri_rdf_Property),inference(resolution,[status(thm)],[c134, c25])).
% 2.69/2.93  cnf(c417,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X315)|iext(X315,uri_rdf_subject,uri_rdf_Property),inference(resolution,[status(thm)],[c133, c25])).
% 2.69/2.93  cnf(c412,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X310)|iext(X310,uri_rdf_type,uri_rdf_Property),inference(resolution,[status(thm)],[c125, c25])).
% 2.69/2.93  fof(rdfs_annotation_comment_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_comment,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_comment_domain)).
% 2.69/2.93  cnf(c124,plain,iext(uri_rdfs_domain,uri_rdfs_comment,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_comment_domain])).
% 2.69/2.93  cnf(c409,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X306)|iext(X306,uri_rdfs_comment,uri_rdfs_Resource),inference(resolution,[status(thm)],[c124, c25])).
% 2.69/2.93  cnf(c411,plain,~iext(uri_rdfs_range,uri_rdf_type,X305)|icext(X305,uri_rdf_Property),inference(resolution,[status(thm)],[c125, c51])).
% 2.69/2.93  cnf(c410,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X304)|icext(X304,uri_rdfs_comment),inference(resolution,[status(thm)],[c124, c77])).
% 2.69/2.93  cnf(c406,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X302)|iext(X302,uri_rdfs_comment,uri_rdfs_Literal),inference(resolution,[status(thm)],[c123, c25])).
% 2.69/2.93  fof(rdfs_annotation_isdefinedby_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_isdefinedby_domain)).
% 2.69/2.93  cnf(c122,plain,iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_domain])).
% 2.69/2.93  cnf(c403,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X301)|iext(X301,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(resolution,[status(thm)],[c122, c25])).
% 2.69/2.93  fof(rdfs_annotation_isdefinedby_range,axiom,iext(uri_rdfs_range,uri_rdfs_isDefinedBy,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_isdefinedby_range)).
% 2.69/2.93  cnf(c121,plain,iext(uri_rdfs_range,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_range])).
% 2.69/2.93  cnf(c400,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X300)|iext(X300,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(resolution,[status(thm)],[c121, c25])).
% 2.69/2.93  fof(simple_ir,axiom,(![X]:ir(X)),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', simple_ir)).
% 2.69/2.93  fof(c145,plain,(![X42]:ir(X42)),inference(variable_rename,[status(thm)],[simple_ir])).
% 2.69/2.93  cnf(c146,plain,ir(X46),inference(split_conjunct,[status(thm)],[c145])).
% 2.69/2.93  fof(rdfs_ir_def,axiom,(![X]:(ir(X)<=>icext(uri_rdfs_Resource,X))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_ir_def)).
% 2.69/2.93  fof(c60,plain,(![X]:((~ir(X)|icext(uri_rdfs_Resource,X))&(~icext(uri_rdfs_Resource,X)|ir(X)))),inference(fof_nnf,[status(thm)],[rdfs_ir_def])).
% 2.69/2.93  fof(c61,plain,((![X]:(~ir(X)|icext(uri_rdfs_Resource,X)))&(![X]:(~icext(uri_rdfs_Resource,X)|ir(X)))),inference(shift_quantors,[status(thm)],[c60])).
% 2.69/2.93  fof(c63,plain,(![X24]:(![X25]:((~ir(X24)|icext(uri_rdfs_Resource,X24))&(~icext(uri_rdfs_Resource,X25)|ir(X25))))),inference(shift_quantors,[status(thm)],[fof(c62,plain,((![X24]:(~ir(X24)|icext(uri_rdfs_Resource,X24)))&(![X25]:(~icext(uri_rdfs_Resource,X25)|ir(X25)))),inference(variable_rename,[status(thm)],[c61])).])).
% 2.69/2.93  cnf(c64,plain,~ir(X54)|icext(uri_rdfs_Resource,X54),inference(split_conjunct,[status(thm)],[c63])).
% 2.69/2.93  cnf(c153,plain,icext(uri_rdfs_Resource,X55),inference(resolution,[status(thm)],[c64, c146])).
% 2.69/2.93  cnf(c389,plain,iext(uri_rdf_type,X93,uri_rdfs_Resource),inference(resolution,[status(thm)],[c115, c153])).
% 2.69/2.93  cnf(c396,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X296)|iext(X296,X295,uri_rdfs_Resource),inference(resolution,[status(thm)],[c389, c25])).
% 2.69/2.93  cnf(c404,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X294)|icext(X294,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c122, c77])).
% 2.69/2.93  cnf(c366,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X292)|iext(X292,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c120, c25])).
% 2.69/2.93  cnf(c401,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X291)|icext(X291,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c121, c77])).
% 2.69/2.93  cnf(c395,plain,~iext(uri_rdfs_range,uri_rdf_type,X289)|icext(X289,uri_rdfs_Resource),inference(resolution,[status(thm)],[c389, c51])).
% 2.69/2.93  cnf(c364,plain,~iext(uri_rdfs_subPropertyOf,X288,uri_rdfs_isDefinedBy)|iext(uri_rdfs_subPropertyOf,X288,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c120, c14])).
% 2.69/2.93  cnf(c368,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X287)|icext(X287,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c120, c77])).
% 2.69/2.93  cnf(c365,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X286)|icext(X286,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c120, c51])).
% 2.69/2.93  fof(rdfs_annotation_label_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_label,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_label_domain)).
% 2.69/2.93  cnf(c119,plain,iext(uri_rdfs_domain,uri_rdfs_label,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_label_domain])).
% 2.69/2.93  cnf(c361,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X285)|iext(X285,uri_rdfs_label,uri_rdfs_Resource),inference(resolution,[status(thm)],[c119, c25])).
% 2.69/2.93  cnf(c362,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X284)|icext(X284,uri_rdfs_label),inference(resolution,[status(thm)],[c119, c77])).
% 2.69/2.93  cnf(c358,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X282)|iext(X282,uri_rdfs_label,uri_rdfs_Literal),inference(resolution,[status(thm)],[c118, c25])).
% 2.69/2.93  fof(rdfs_annotation_seealso_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_seeAlso,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_seealso_domain)).
% 2.69/2.93  cnf(c117,plain,iext(uri_rdfs_domain,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_seealso_domain])).
% 2.69/2.93  cnf(c355,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X280)|iext(X280,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(resolution,[status(thm)],[c117, c25])).
% 2.69/2.93  cnf(c357,plain,~iext(uri_rdfs_range,uri_rdfs_range,X279)|icext(X279,uri_rdfs_Literal),inference(resolution,[status(thm)],[c118, c51])).
% 2.69/2.93  cnf(c356,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X278)|icext(X278,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c117, c77])).
% 2.69/2.93  fof(rdfs_annotation_seealso_range,axiom,iext(uri_rdfs_range,uri_rdfs_seeAlso,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_seealso_range)).
% 2.69/2.93  cnf(c116,plain,iext(uri_rdfs_range,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_seealso_range])).
% 2.69/2.93  cnf(c342,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X277)|iext(X277,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(resolution,[status(thm)],[c116, c25])).
% 2.69/2.93  cnf(c343,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X275)|icext(X275,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c116, c77])).
% 2.69/2.93  fof(rdfs_collection_first_domain,axiom,iext(uri_rdfs_domain,uri_rdf_first,uri_rdf_List),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_collection_first_domain)).
% 2.69/2.93  cnf(c106,plain,iext(uri_rdfs_domain,uri_rdf_first,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdfs_collection_first_domain])).
% 2.69/2.93  cnf(c339,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X273)|iext(X273,uri_rdf_first,uri_rdf_List),inference(resolution,[status(thm)],[c106, c25])).
% 2.69/2.93  cnf(c340,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X272)|icext(X272,uri_rdf_first),inference(resolution,[status(thm)],[c106, c77])).
% 2.69/2.93  fof(rdfs_collection_first_range,axiom,iext(uri_rdfs_range,uri_rdf_first,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_collection_first_range)).
% 2.69/2.93  cnf(c105,plain,iext(uri_rdfs_range,uri_rdf_first,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_collection_first_range])).
% 2.69/2.93  cnf(c336,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X270)|iext(X270,uri_rdf_first,uri_rdfs_Resource),inference(resolution,[status(thm)],[c105, c25])).
% 2.69/2.93  cnf(c337,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X269)|icext(X269,uri_rdf_first),inference(resolution,[status(thm)],[c105, c77])).
% 2.69/2.93  cnf(c328,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X267)|icext(X267,uri_rdfs_domain),inference(resolution,[status(thm)],[c77, c72])).
% 2.69/2.93  fof(rdfs_container_n_range_003,axiom,iext(uri_rdfs_range,uri_rdf__3,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_range_003)).
% 2.69/2.93  cnf(c89,plain,iext(uri_rdfs_range,uri_rdf__3,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_range_003])).
% 2.69/2.93  cnf(c327,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X266)|icext(X266,uri_rdf__3),inference(resolution,[status(thm)],[c77, c89])).
% 2.69/2.93  cnf(c326,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X265)|icext(X265,uri_rdf_Alt),inference(resolution,[status(thm)],[c77, c102])).
% 2.69/2.93  fof(rdfs_container_n_domain_003,axiom,iext(uri_rdfs_domain,uri_rdf__3,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_domain_003)).
% 2.69/2.93  cnf(c92,plain,iext(uri_rdfs_domain,uri_rdf__3,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_003])).
% 2.69/2.93  cnf(c325,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X264)|icext(X264,uri_rdf__3),inference(resolution,[status(thm)],[c77, c92])).
% 2.69/2.93  fof(rdfs_reification_predicate_range,axiom,iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_reification_predicate_range)).
% 2.69/2.93  cnf(c44,plain,iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_reification_predicate_range])).
% 2.69/2.93  cnf(c324,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X263)|icext(X263,uri_rdf_predicate),inference(resolution,[status(thm)],[c77, c44])).
% 2.69/2.93  fof(rdfs_reification_subject_domain,axiom,iext(uri_rdfs_domain,uri_rdf_subject,uri_rdfs_Statement),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_reification_subject_domain)).
% 2.69/2.93  cnf(c43,plain,iext(uri_rdfs_domain,uri_rdf_subject,uri_rdfs_Statement),inference(split_conjunct,[status(thm)],[rdfs_reification_subject_domain])).
% 2.69/2.93  cnf(c322,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X261)|icext(X261,uri_rdf_subject),inference(resolution,[status(thm)],[c77, c43])).
% 2.69/2.93  fof(rdfs_subclassof_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdfs_Class),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_subclassof_domain)).
% 2.69/2.93  cnf(c41,plain,iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_subclassof_domain])).
% 2.69/2.93  cnf(c321,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X260)|icext(X260,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c77, c41])).
% 2.69/2.93  fof(rdfs_container_member_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_member,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_member_domain)).
% 2.69/2.93  cnf(c96,plain,iext(uri_rdfs_domain,uri_rdfs_member,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_member_domain])).
% 2.69/2.93  cnf(c318,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X257)|icext(X257,uri_rdfs_member),inference(resolution,[status(thm)],[c77, c96])).
% 2.69/2.93  fof(rdfs_reification_subject_range,axiom,iext(uri_rdfs_range,uri_rdf_subject,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_reification_subject_range)).
% 2.69/2.93  cnf(c42,plain,iext(uri_rdfs_range,uri_rdf_subject,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_reification_subject_range])).
% 2.69/2.93  cnf(c317,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X256)|icext(X256,uri_rdf_subject),inference(resolution,[status(thm)],[c77, c42])).
% 2.69/2.93  cnf(c316,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X255)|icext(X255,uri_rdf_Bag),inference(resolution,[status(thm)],[c77, c101])).
% 2.69/2.93  cnf(c315,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X254)|icext(X254,uri_rdfs_Seq),inference(resolution,[status(thm)],[c77, c85])).
% 2.69/2.93  cnf(c3,plain,iext(uri_owl_sameAs,skolem0001,literal_plain(dat_str_abc)),inference(split_conjunct,[status(thm)],[c1])).
% 2.69/2.93  cnf(c314,plain,~iext(uri_rdfs_domain,uri_owl_sameAs,X253)|icext(X253,skolem0001),inference(resolution,[status(thm)],[c77, c3])).
% 2.69/2.93  fof(rdfs_type_range,axiom,iext(uri_rdfs_range,uri_rdf_type,uri_rdfs_Class),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_type_range)).
% 2.69/2.93  cnf(c10,plain,iext(uri_rdfs_range,uri_rdf_type,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_type_range])).
% 2.69/2.93  cnf(c313,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X252)|icext(X252,uri_rdf_type),inference(resolution,[status(thm)],[c77, c10])).
% 2.69/2.93  cnf(c312,plain,~iext(uri_rdfs_domain,uri_owl_sameAs,X251)|icext(X251,uri_ex_u),inference(resolution,[status(thm)],[c77, c2])).
% 2.69/2.93  fof(rdfs_reification_object_domain,axiom,iext(uri_rdfs_domain,uri_rdf_object,uri_rdfs_Statement),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_reification_object_domain)).
% 2.69/2.93  cnf(c47,plain,iext(uri_rdfs_domain,uri_rdf_object,uri_rdfs_Statement),inference(split_conjunct,[status(thm)],[rdfs_reification_object_domain])).
% 2.69/2.93  cnf(c310,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X249)|icext(X249,uri_rdf_object),inference(resolution,[status(thm)],[c77, c47])).
% 2.69/2.93  fof(rdfs_subclassof_range,axiom,iext(uri_rdfs_range,uri_rdfs_subClassOf,uri_rdfs_Class),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_subclassof_range)).
% 2.69/2.93  cnf(c33,plain,iext(uri_rdfs_range,uri_rdfs_subClassOf,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_subclassof_range])).
% 2.69/2.93  cnf(c309,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X248)|icext(X248,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c77, c33])).
% 2.69/2.93  fof(rdfs_container_member_range,axiom,iext(uri_rdfs_range,uri_rdfs_member,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_member_range)).
% 2.69/2.93  cnf(c95,plain,iext(uri_rdfs_range,uri_rdfs_member,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_member_range])).
% 2.69/2.93  cnf(c308,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X247)|icext(X247,uri_rdfs_member),inference(resolution,[status(thm)],[c77, c95])).
% 2.69/2.93  fof(rdfs_subpropertyof_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdf_Property),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_subpropertyof_domain)).
% 2.69/2.93  cnf(c26,plain,iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_subpropertyof_domain])).
% 2.69/2.93  cnf(c307,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X246)|icext(X246,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c77, c26])).
% 2.69/2.93  fof(rdfs_container_n_domain_001,axiom,iext(uri_rdfs_domain,uri_rdf__1,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_domain_001)).
% 2.69/2.93  cnf(c94,plain,iext(uri_rdfs_domain,uri_rdf__1,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_001])).
% 2.69/2.93  cnf(c306,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X245)|icext(X245,uri_rdf__1),inference(resolution,[status(thm)],[c77, c94])).
% 2.69/2.93  fof(rdfs_value_domain,axiom,iext(uri_rdfs_domain,uri_rdf_value,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_value_domain)).
% 2.69/2.93  cnf(c9,plain,iext(uri_rdfs_domain,uri_rdf_value,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_value_domain])).
% 2.69/2.93  cnf(c305,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X244)|icext(X244,uri_rdf_value),inference(resolution,[status(thm)],[c77, c9])).
% 2.69/2.93  fof(rdfs_subpropertyof_range,axiom,iext(uri_rdfs_range,uri_rdfs_subPropertyOf,uri_rdf_Property),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_subpropertyof_range)).
% 2.69/2.93  cnf(c18,plain,iext(uri_rdfs_range,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_subpropertyof_range])).
% 2.69/2.93  cnf(c303,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X242)|icext(X242,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c77, c18])).
% 2.69/2.93  fof(rdfs_container_n_range_001,axiom,iext(uri_rdfs_range,uri_rdf__1,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_range_001)).
% 2.69/2.93  cnf(c91,plain,iext(uri_rdfs_range,uri_rdf__1,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_range_001])).
% 2.69/2.93  cnf(c302,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X241)|icext(X241,uri_rdf__1),inference(resolution,[status(thm)],[c77, c91])).
% 2.69/2.93  cnf(c301,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X240)|icext(X240,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c77, c97])).
% 2.69/2.93  cnf(c300,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X239)|icext(X239,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c77, c84])).
% 2.69/2.93  fof(rdfs_collection_rest_domain,axiom,iext(uri_rdfs_domain,uri_rdf_rest,uri_rdf_List),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_collection_rest_domain)).
% 2.69/2.93  cnf(c104,plain,iext(uri_rdfs_domain,uri_rdf_rest,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdfs_collection_rest_domain])).
% 2.69/2.93  cnf(c299,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X238)|icext(X238,uri_rdf_rest),inference(resolution,[status(thm)],[c77, c104])).
% 2.69/2.93  cnf(c298,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X237)|icext(X237,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c77, c79])).
% 2.69/2.93  fof(rdfs_type_domain,axiom,iext(uri_rdfs_domain,uri_rdf_type,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_type_domain)).
% 2.69/2.93  cnf(c11,plain,iext(uri_rdfs_domain,uri_rdf_type,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_type_domain])).
% 2.69/2.93  cnf(c296,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X235)|icext(X235,uri_rdf_type),inference(resolution,[status(thm)],[c77, c11])).
% 2.69/2.93  fof(rdfs_value_range,axiom,iext(uri_rdfs_range,uri_rdf_value,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_value_range)).
% 2.69/2.93  cnf(c8,plain,iext(uri_rdfs_range,uri_rdf_value,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_value_range])).
% 2.69/2.93  cnf(c295,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X234)|icext(X234,uri_rdf_value),inference(resolution,[status(thm)],[c77, c8])).
% 2.69/2.93  fof(rdfs_container_n_domain_002,axiom,iext(uri_rdfs_domain,uri_rdf__2,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_domain_002)).
% 2.69/2.93  cnf(c93,plain,iext(uri_rdfs_domain,uri_rdf__2,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_002])).
% 2.69/2.93  cnf(c294,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X233)|icext(X233,uri_rdf__2),inference(resolution,[status(thm)],[c77, c93])).
% 2.69/2.93  cnf(c293,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X232)|icext(X232,uri_rdfs_range),inference(resolution,[status(thm)],[c77, c52])).
% 2.69/2.93  cnf(c291,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X230)|icext(X230,uri_rdfs_range),inference(resolution,[status(thm)],[c77, c48])).
% 2.69/2.93  fof(rdfs_container_n_range_002,axiom,iext(uri_rdfs_range,uri_rdf__2,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_range_002)).
% 2.69/2.93  cnf(c90,plain,iext(uri_rdfs_range,uri_rdf__2,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_range_002])).
% 2.69/2.93  cnf(c290,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X229)|icext(X229,uri_rdf__2),inference(resolution,[status(thm)],[c77, c90])).
% 2.69/2.93  cnf(c288,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X227)|icext(X227,uri_rdf_rest),inference(resolution,[status(thm)],[c77, c103])).
% 2.69/2.93  cnf(c287,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X226)|icext(X226,uri_rdfs_domain),inference(factor,[status(thm)],[c77])).
% 2.69/2.93  cnf(c277,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X218)|icext(X218,uri_rdfs_Class),inference(resolution,[status(thm)],[c51, c41])).
% 2.69/2.93  fof(rdfs_property_type,axiom,iext(uri_rdf_type,uri_rdf_Property,uri_rdfs_Class),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_property_type)).
% 2.69/2.93  cnf(c53,plain,iext(uri_rdf_type,uri_rdf_Property,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_property_type])).
% 2.69/2.93  cnf(c276,plain,~iext(uri_rdfs_range,uri_rdf_type,X217)|icext(X217,uri_rdfs_Class),inference(resolution,[status(thm)],[c51, c53])).
% 2.69/2.93  cnf(c397,plain,~iext(uri_rdfs_domain,uri_rdf_type,X214)|icext(X214,X215),inference(resolution,[status(thm)],[c389, c77])).
% 2.69/2.93  cnf(c4,plain,iext(uri_owl_sameAs,skolem0001,uri_ex_w),inference(split_conjunct,[status(thm)],[c1])).
% 2.69/2.93  cnf(c275,plain,~iext(uri_rdfs_range,uri_owl_sameAs,X211)|icext(X211,uri_ex_w),inference(resolution,[status(thm)],[c51, c4])).
% 2.69/2.93  cnf(c271,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X190)|icext(X190,uri_rdfs_Container),inference(resolution,[status(thm)],[c51, c85])).
% 2.69/2.93  cnf(c268,plain,~iext(uri_rdfs_range,uri_owl_sameAs,X181)|icext(X181,literal_plain(dat_str_abc)),inference(resolution,[status(thm)],[c51, c2])).
% 2.69/2.93  fof(rdfs_dat_xmlliteral_type,axiom,iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Datatype),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_dat_xmlliteral_type)).
% 2.69/2.93  cnf(c83,plain,iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Datatype),inference(split_conjunct,[status(thm)],[rdfs_dat_xmlliteral_type])).
% 2.69/2.93  cnf(c260,plain,~iext(uri_rdfs_range,uri_rdf_type,X173)|icext(X173,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c51, c83])).
% 2.69/2.93  cnf(c259,plain,~iext(uri_rdfs_range,uri_rdfs_range,X172)|icext(X172,uri_rdf_Property),inference(resolution,[status(thm)],[c51, c18])).
% 2.69/2.93  cnf(c257,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X170)|icext(X170,uri_rdf_Property),inference(resolution,[status(thm)],[c51, c97])).
% 2.69/2.93  cnf(c256,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X169)|icext(X169,uri_rdfs_Literal),inference(resolution,[status(thm)],[c51, c84])).
% 2.69/2.93  cnf(c255,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X168)|icext(X168,uri_rdf_List),inference(resolution,[status(thm)],[c51, c104])).
% 2.69/2.93  cnf(c254,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X167)|icext(X167,uri_rdfs_Class),inference(resolution,[status(thm)],[c51, c79])).
% 2.69/2.93  cnf(c253,plain,~iext(uri_rdfs_range,uri_rdf_type,X166)|icext(X166,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c51, c87])).
% 2.69/2.93  cnf(c1041,plain,icext(uri_rdf_Property,uri_rdfs_member),inference(resolution,[status(thm)],[c749, c114])).
% 2.69/2.93  cnf(c250,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X163)|icext(X163,uri_rdfs_Resource),inference(resolution,[status(thm)],[c51, c93])).
% 2.69/2.93  cnf(c1012,plain,icext(uri_rdf_Property,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c561, c114])).
% 2.69/2.93  cnf(c248,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X161)|icext(X161,uri_rdf_Property),inference(resolution,[status(thm)],[c51, c78])).
% 2.69/2.93  cnf(c247,plain,~iext(uri_rdfs_range,uri_rdfs_range,X160)|icext(X160,uri_rdfs_Class),inference(resolution,[status(thm)],[c51, c48])).
% 2.69/2.93  cnf(c993,plain,icext(uri_rdf_Property,uri_owl_sameAs),inference(resolution,[status(thm)],[c559, c114])).
% 2.69/2.93  cnf(c246,plain,~iext(uri_rdfs_range,uri_rdfs_range,X159)|icext(X159,uri_rdfs_Resource),inference(resolution,[status(thm)],[c51, c90])).
% 2.69/2.93  cnf(c960,plain,icext(uri_rdf_Property,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c557, c114])).
% 2.69/2.93  cnf(c243,plain,~iext(uri_rdfs_range,uri_rdfs_range,X156)|icext(X156,X156),inference(factor,[status(thm)],[c51])).
% 2.69/2.93  cnf(c931,plain,icext(uri_rdf_Property,uri_rdfs_domain),inference(resolution,[status(thm)],[c555, c114])).
% 2.69/2.93  cnf(c40,plain,~iext(uri_rdfs_subClassOf,X77,X76)|~icext(X77,X75)|icext(X76,X75),inference(split_conjunct,[status(thm)],[c37])).
% 2.69/2.93  cnf(c240,plain,~icext(uri_rdf_Alt,X155)|icext(uri_rdfs_Container,X155),inference(resolution,[status(thm)],[c40, c102])).
% 2.69/2.93  cnf(c239,plain,~icext(uri_rdf_Bag,X154)|icext(uri_rdfs_Container,X154),inference(resolution,[status(thm)],[c40, c101])).
% 2.69/2.93  cnf(c904,plain,icext(uri_rdf_Property,uri_rdfs_range),inference(resolution,[status(thm)],[c553, c114])).
% 2.69/2.93  cnf(c238,plain,~icext(uri_rdfs_Seq,X153)|icext(uri_rdfs_Container,X153),inference(resolution,[status(thm)],[c40, c85])).
% 2.69/2.93  cnf(c237,plain,~icext(uri_rdfs_ContainerMembershipProperty,X152)|icext(uri_rdf_Property,X152),inference(resolution,[status(thm)],[c40, c97])).
% 2.69/2.93  cnf(c236,plain,~icext(uri_rdf_XMLLiteral,X151)|icext(uri_rdfs_Literal,X151),inference(resolution,[status(thm)],[c40, c84])).
% 2.69/2.93  cnf(c235,plain,~icext(uri_rdfs_Datatype,X150)|icext(uri_rdfs_Class,X150),inference(resolution,[status(thm)],[c40, c79])).
% 2.69/2.93  cnf(c202,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X149)|iext(X149,uri_rdf_rest,uri_rdf_List),inference(resolution,[status(thm)],[c104, c25])).
% 2.69/2.93  cnf(c201,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X148)|iext(X148,uri_rdf_rest,uri_rdf_List),inference(resolution,[status(thm)],[c103, c25])).
% 2.69/2.93  cnf(c200,plain,~iext(uri_rdfs_subClassOf,X147,uri_rdf_Alt)|iext(uri_rdfs_subClassOf,X147,uri_rdfs_Container),inference(resolution,[status(thm)],[c102, c29])).
% 2.69/2.93  cnf(c199,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X146)|iext(X146,uri_rdf_Alt,uri_rdfs_Container),inference(resolution,[status(thm)],[c102, c25])).
% 2.69/2.93  cnf(c198,plain,~iext(uri_rdfs_subClassOf,X145,uri_rdf_Bag)|iext(uri_rdfs_subClassOf,X145,uri_rdfs_Container),inference(resolution,[status(thm)],[c101, c29])).
% 2.69/2.93  cnf(c849,plain,icext(uri_rdf_Property,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c435, c114])).
% 2.69/2.93  cnf(c197,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X144)|iext(X144,uri_rdf_Bag,uri_rdfs_Container),inference(resolution,[status(thm)],[c101, c25])).
% 2.69/2.93  cnf(c841,plain,icext(uri_rdf_Property,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c434, c114])).
% 2.69/2.93  cnf(c196,plain,~iext(uri_rdfs_subClassOf,X143,uri_rdfs_ContainerMembershipProperty)|iext(uri_rdfs_subClassOf,X143,uri_rdf_Property),inference(resolution,[status(thm)],[c97, c29])).
% 2.69/2.93  cnf(c195,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X142)|iext(X142,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),inference(resolution,[status(thm)],[c97, c25])).
% 2.69/2.93  cnf(c194,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X141)|iext(X141,uri_rdfs_member,uri_rdfs_Resource),inference(resolution,[status(thm)],[c96, c25])).
% 2.69/2.93  cnf(c193,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X140)|iext(X140,uri_rdfs_member,uri_rdfs_Resource),inference(resolution,[status(thm)],[c95, c25])).
% 2.69/2.93  cnf(c192,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X139)|iext(X139,uri_rdf__1,uri_rdfs_Resource),inference(resolution,[status(thm)],[c94, c25])).
% 2.69/2.93  cnf(c191,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X138)|iext(X138,uri_rdf__2,uri_rdfs_Resource),inference(resolution,[status(thm)],[c93, c25])).
% 2.69/2.93  cnf(c190,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X137)|iext(X137,uri_rdf__3,uri_rdfs_Resource),inference(resolution,[status(thm)],[c92, c25])).
% 2.69/2.93  cnf(c189,plain,~iext(uri_rdfs_subClassOf,X136,uri_rdfs_Seq)|iext(uri_rdfs_subClassOf,X136,uri_rdfs_Container),inference(resolution,[status(thm)],[c29, c85])).
% 2.69/2.93  cnf(c188,plain,~iext(uri_rdfs_subClassOf,X135,uri_rdf_XMLLiteral)|iext(uri_rdfs_subClassOf,X135,uri_rdfs_Literal),inference(resolution,[status(thm)],[c29, c84])).
% 2.69/2.93  cnf(c187,plain,~iext(uri_rdfs_subClassOf,X134,uri_rdfs_Datatype)|iext(uri_rdfs_subClassOf,X134,uri_rdfs_Class),inference(resolution,[status(thm)],[c29, c79])).
% 2.69/2.93  cnf(c185,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X132)|iext(X132,uri_rdf__1,uri_rdfs_Resource),inference(resolution,[status(thm)],[c91, c25])).
% 2.69/2.93  cnf(c184,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X131)|iext(X131,uri_rdf__2,uri_rdfs_Resource),inference(resolution,[status(thm)],[c90, c25])).
% 2.69/2.93  cnf(c183,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X130)|iext(X130,uri_rdf__3,uri_rdfs_Resource),inference(resolution,[status(thm)],[c89, c25])).
% 2.69/2.93  cnf(c182,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X129)|iext(X129,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c88, c25])).
% 2.69/2.93  cnf(c181,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X128)|iext(X128,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c87, c25])).
% 2.69/2.93  cnf(c180,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X127)|iext(X127,uri_rdfs_domain,uri_rdfs_Class),inference(resolution,[status(thm)],[c25, c72])).
% 2.69/2.93  cnf(c179,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X126)|iext(X126,uri_rdf_predicate,uri_rdfs_Resource),inference(resolution,[status(thm)],[c25, c44])).
% 2.69/2.93  cnf(c178,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X125)|iext(X125,uri_rdf_subject,uri_rdfs_Statement),inference(resolution,[status(thm)],[c25, c43])).
% 2.69/2.93  cnf(c177,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X124)|iext(X124,uri_rdfs_subClassOf,uri_rdfs_Class),inference(resolution,[status(thm)],[c25, c41])).
% 2.69/2.93  cnf(c176,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X123)|iext(X123,uri_rdf_Property,uri_rdfs_Class),inference(resolution,[status(thm)],[c25, c53])).
% 2.69/2.93  cnf(c175,plain,~iext(uri_rdfs_subPropertyOf,uri_owl_sameAs,X122)|iext(X122,skolem0001,uri_ex_w),inference(resolution,[status(thm)],[c25, c4])).
% 2.69/2.93  cnf(c174,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X121)|iext(X121,uri_rdf_subject,uri_rdfs_Resource),inference(resolution,[status(thm)],[c25, c42])).
% 2.69/2.93  cnf(c173,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X120)|iext(X120,uri_rdfs_Seq,uri_rdfs_Container),inference(resolution,[status(thm)],[c25, c85])).
% 2.69/2.93  cnf(c172,plain,~iext(uri_rdfs_subPropertyOf,uri_owl_sameAs,X119)|iext(X119,skolem0001,literal_plain(dat_str_abc)),inference(resolution,[status(thm)],[c25, c3])).
% 2.69/2.93  cnf(c171,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X118)|iext(X118,uri_rdf_type,uri_rdfs_Class),inference(resolution,[status(thm)],[c25, c10])).
% 2.69/2.93  cnf(c170,plain,~iext(uri_rdfs_subPropertyOf,uri_owl_sameAs,X117)|iext(X117,uri_ex_u,literal_plain(dat_str_abc)),inference(resolution,[status(thm)],[c25, c2])).
% 2.69/2.93  cnf(c169,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X116)|iext(X116,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c25, c86])).
% 2.69/2.93  cnf(c168,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X115)|iext(X115,uri_rdf_object,uri_rdfs_Statement),inference(resolution,[status(thm)],[c25, c47])).
% 2.69/2.93  cnf(c167,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X114)|iext(X114,uri_rdfs_subClassOf,uri_rdfs_Class),inference(resolution,[status(thm)],[c25, c33])).
% 2.69/2.93  cnf(c166,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X113)|iext(X113,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c25, c26])).
% 2.69/2.93  cnf(c165,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X112)|iext(X112,uri_rdf_value,uri_rdfs_Resource),inference(resolution,[status(thm)],[c25, c9])).
% 2.69/2.93  cnf(c164,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X111)|iext(X111,uri_rdf_XMLLiteral,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c25, c83])).
% 2.69/2.93  cnf(c163,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X110)|iext(X110,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c25, c18])).
% 2.69/2.93  cnf(c162,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X109)|iext(X109,uri_rdf_XMLLiteral,uri_rdfs_Literal),inference(resolution,[status(thm)],[c25, c84])).
% 2.69/2.93  cnf(c161,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X108)|iext(X108,uri_rdfs_Datatype,uri_rdfs_Class),inference(resolution,[status(thm)],[c25, c79])).
% 2.69/2.93  cnf(c160,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X107)|iext(X107,uri_rdf_type,uri_rdfs_Resource),inference(resolution,[status(thm)],[c25, c11])).
% 2.69/2.93  cnf(c159,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X106)|iext(X106,uri_rdf_value,uri_rdfs_Resource),inference(resolution,[status(thm)],[c25, c8])).
% 2.69/2.93  cnf(c158,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X105)|iext(X105,uri_rdfs_range,uri_rdf_Property),inference(resolution,[status(thm)],[c25, c52])).
% 2.69/2.93  cnf(c157,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X104)|iext(X104,uri_rdfs_domain,uri_rdf_Property),inference(resolution,[status(thm)],[c25, c78])).
% 2.69/2.93  cnf(c156,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X103)|iext(X103,uri_rdfs_range,uri_rdfs_Class),inference(resolution,[status(thm)],[c25, c48])).
% 2.69/2.93  cnf(c155,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X102)|iext(X102,uri_rdf_predicate,uri_rdfs_Statement),inference(resolution,[status(thm)],[c25, c45])).
% 2.69/2.93  cnf(c154,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X101)|iext(X101,uri_rdfs_subPropertyOf,X101),inference(factor,[status(thm)],[c25])).
% 2.69/2.93  cnf(c485,plain,icext(uri_rdf_Property,uri_rdf_first),inference(resolution,[status(thm)],[c141, c114])).
% 2.69/2.93  cnf(c480,plain,icext(uri_rdf_List,uri_rdf_nil),inference(resolution,[status(thm)],[c140, c114])).
% 2.69/2.93  cnf(c470,plain,icext(uri_rdf_Property,uri_rdf_rest),inference(resolution,[status(thm)],[c139, c114])).
% 2.69/2.93  cnf(c465,plain,icext(uri_rdf_Property,uri_rdf__1),inference(resolution,[status(thm)],[c138, c114])).
% 2.69/2.93  cnf(c454,plain,icext(uri_rdf_Property,uri_rdf__2),inference(resolution,[status(thm)],[c137, c114])).
% 2.69/2.93  cnf(c449,plain,icext(uri_rdf_Property,uri_rdf__3),inference(resolution,[status(thm)],[c136, c114])).
% 2.69/2.93  cnf(c441,plain,icext(uri_rdf_Property,uri_rdf_object),inference(resolution,[status(thm)],[c135, c114])).
% 2.69/2.93  cnf(c429,plain,icext(uri_rdf_Property,uri_rdf_value),inference(resolution,[status(thm)],[c134, c114])).
% 2.69/2.93  cnf(c419,plain,icext(uri_rdf_Property,uri_rdf_subject),inference(resolution,[status(thm)],[c133, c114])).
% 2.69/2.93  cnf(c414,plain,icext(uri_rdf_Property,uri_rdf_type),inference(resolution,[status(thm)],[c125, c114])).
% 2.69/2.93  cnf(c371,plain,icext(uri_rdfs_Datatype,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c114, c83])).
% 2.69/2.93  cnf(c232,plain,icext(uri_rdfs_Class,uri_rdf_Property),inference(resolution,[status(thm)],[c221, c70])).
% 2.69/2.93  fof(rdfs_datatype_instsub_literal,axiom,(![D]:(icext(uri_rdfs_Datatype,D)=>iext(uri_rdfs_subClassOf,D,uri_rdfs_Literal))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_datatype_instsub_literal)).
% 2.69/2.93  fof(c80,plain,(![D]:(~icext(uri_rdfs_Datatype,D)|iext(uri_rdfs_subClassOf,D,uri_rdfs_Literal))),inference(fof_nnf,[status(thm)],[rdfs_datatype_instsub_literal])).
% 2.69/2.93  fof(c81,plain,(![X32]:(~icext(uri_rdfs_Datatype,X32)|iext(uri_rdfs_subClassOf,X32,uri_rdfs_Literal))),inference(variable_rename,[status(thm)],[c80])).
% 2.69/2.93  cnf(c82,plain,~icext(uri_rdfs_Datatype,X86)|iext(uri_rdfs_subClassOf,X86,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[c81])).
% 2.69/2.93  fof(rdfs_lv_def,axiom,(![X]:(lv(X)<=>icext(uri_rdfs_Literal,X))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_lv_def)).
% 2.69/2.93  fof(c54,plain,(![X]:((~lv(X)|icext(uri_rdfs_Literal,X))&(~icext(uri_rdfs_Literal,X)|lv(X)))),inference(fof_nnf,[status(thm)],[rdfs_lv_def])).
% 2.69/2.93  fof(c55,plain,((![X]:(~lv(X)|icext(uri_rdfs_Literal,X)))&(![X]:(~icext(uri_rdfs_Literal,X)|lv(X)))),inference(shift_quantors,[status(thm)],[c54])).
% 2.69/2.93  fof(c57,plain,(![X22]:(![X23]:((~lv(X22)|icext(uri_rdfs_Literal,X22))&(~icext(uri_rdfs_Literal,X23)|lv(X23))))),inference(shift_quantors,[status(thm)],[fof(c56,plain,((![X22]:(~lv(X22)|icext(uri_rdfs_Literal,X22)))&(![X23]:(~icext(uri_rdfs_Literal,X23)|lv(X23)))),inference(variable_rename,[status(thm)],[c55])).])).
% 2.69/2.93  cnf(c59,plain,~icext(uri_rdfs_Literal,X53)|lv(X53),inference(split_conjunct,[status(thm)],[c57])).
% 2.69/2.93  cnf(c58,plain,~lv(X52)|icext(uri_rdfs_Literal,X52),inference(split_conjunct,[status(thm)],[c57])).
% 2.69/2.93  fof(testcase_conclusion_fullish_006_Literal_Values_represented_by_URIs_and_Blank_Nodes,conjecture,iext(uri_owl_sameAs,uri_ex_u,uri_ex_w),file('/export/starexec/sandbox/benchmark/theBenchmark.p', testcase_conclusion_fullish_006_Literal_Values_represented_by_URIs_and_Blank_Nodes)).
% 2.69/2.93  fof(c5,negated_conjecture,(~iext(uri_owl_sameAs,uri_ex_u,uri_ex_w)),inference(assume_negation,[status(cth)],[testcase_conclusion_fullish_006_Literal_Values_represented_by_URIs_and_Blank_Nodes])).
% 2.69/2.93  fof(c6,negated_conjecture,~iext(uri_owl_sameAs,uri_ex_u,uri_ex_w),inference(fof_simplification,[status(thm)],[c5])).
% 2.69/2.93  cnf(c7,negated_conjecture,~iext(uri_owl_sameAs,uri_ex_u,uri_ex_w),inference(split_conjunct,[status(thm)],[c6])).
% 2.69/2.93  % SZS output end Saturation
% 2.69/2.93  
% 2.69/2.93  % Initial clauses    : 93
% 2.69/2.93  % Processed clauses  : 521
% 2.69/2.93  % Factors computed   : 5
% 2.69/2.93  % Resolvents computed: 1215
% 2.69/2.93  % Tautologies deleted: 48
% 2.69/2.93  % Forward subsumed   : 744
% 2.69/2.93  % Backward subsumed  : 1
% 2.69/2.93  % -------- CPU Time ---------
% 2.69/2.93  % User time          : 2.568 s
% 2.69/2.93  % System time        : 0.015 s
% 2.69/2.93  % Total time         : 2.583 s
%------------------------------------------------------------------------------