PyRes---1.5.CSA-Sat.s

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

% Computer : n028.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:55 EDT 2024

% Result   : CounterSatisfiable 3.12s 3.32s
% Output   : Saturation 3.12s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12  % Problem  : SWB027+4 : TPTP v8.1.2. Released v5.2.0.
% 0.07/0.13  % Command  : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.34  % Computer : n028.cluster.edu
% 0.12/0.34  % Model    : x86_64 x86_64
% 0.12/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34  % Memory   : 8042.1875MB
% 0.12/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34  % CPULimit : 300
% 0.12/0.34  % WCLimit  : 300
% 0.12/0.34  % DateTime : Wed May  8 22:03:53 EDT 2024
% 0.12/0.34  % CPUTime  : 
% 3.12/3.32  % Version:  1.5
% 3.12/3.32  % SZS status CounterSatisfiable
% 3.12/3.32  % SZS output start Saturation
% 3.12/3.32  fof(rdfs_subpropertyof_main,axiom,(![P]:(![Q]:(iext(uri_rdfs_subPropertyOf,P,Q)=>((ip(P)&ip(Q))&(![X]:(![Y]:(iext(P,X,Y)=>iext(Q,X,Y)))))))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_subpropertyof_main)).
% 3.12/3.32  fof(c22,plain,(![P]:(![Q]:(~iext(uri_rdfs_subPropertyOf,P,Q)|((ip(P)&ip(Q))&(![X]:(![Y]:(~iext(P,X,Y)|iext(Q,X,Y)))))))),inference(fof_nnf,[status(thm)],[rdfs_subpropertyof_main])).
% 3.12/3.32  fof(c24,plain,(![X9]:(![X10]:(![X11]:(![X12]:(~iext(uri_rdfs_subPropertyOf,X9,X10)|((ip(X9)&ip(X10))&(~iext(X9,X11,X12)|iext(X10,X11,X12)))))))),inference(shift_quantors,[status(thm)],[fof(c23,plain,(![X9]:(![X10]:(~iext(uri_rdfs_subPropertyOf,X9,X10)|((ip(X9)&ip(X10))&(![X11]:(![X12]:(~iext(X9,X11,X12)|iext(X10,X11,X12)))))))),inference(variable_rename,[status(thm)],[c22])).])).
% 3.12/3.32  fof(c25,plain,(![X9]:(![X10]:(![X11]:(![X12]:(((~iext(uri_rdfs_subPropertyOf,X9,X10)|ip(X9))&(~iext(uri_rdfs_subPropertyOf,X9,X10)|ip(X10)))&(~iext(uri_rdfs_subPropertyOf,X9,X10)|(~iext(X9,X11,X12)|iext(X10,X11,X12)))))))),inference(distribute,[status(thm)],[c24])).
% 3.12/3.32  cnf(c28,plain,~iext(uri_rdfs_subPropertyOf,X65,X68)|~iext(X65,X67,X66)|iext(X68,X67,X66),inference(split_conjunct,[status(thm)],[c25])).
% 3.12/3.32  fof(rdfs_subpropertyof_reflex,axiom,(![P]:(ip(P)=>iext(uri_rdfs_subPropertyOf,P,P))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_subpropertyof_reflex)).
% 3.12/3.32  fof(c18,plain,(![P]:(~ip(P)|iext(uri_rdfs_subPropertyOf,P,P))),inference(fof_nnf,[status(thm)],[rdfs_subpropertyof_reflex])).
% 3.12/3.32  fof(c19,plain,(![X8]:(~ip(X8)|iext(uri_rdfs_subPropertyOf,X8,X8))),inference(variable_rename,[status(thm)],[c18])).
% 3.12/3.32  cnf(c20,plain,~ip(X53)|iext(uri_rdfs_subPropertyOf,X53,X53),inference(split_conjunct,[status(thm)],[c19])).
% 3.12/3.32  fof(rdf_type_ip,axiom,(![P]:(iext(uri_rdf_type,P,uri_rdf_Property)<=>ip(P))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdf_type_ip)).
% 3.12/3.32  fof(c130,plain,(![P]:((~iext(uri_rdf_type,P,uri_rdf_Property)|ip(P))&(~ip(P)|iext(uri_rdf_type,P,uri_rdf_Property)))),inference(fof_nnf,[status(thm)],[rdf_type_ip])).
% 3.12/3.32  fof(c131,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)],[c130])).
% 3.12/3.32  fof(c133,plain,(![X41]:(![X42]:((~iext(uri_rdf_type,X41,uri_rdf_Property)|ip(X41))&(~ip(X42)|iext(uri_rdf_type,X42,uri_rdf_Property))))),inference(shift_quantors,[status(thm)],[fof(c132,plain,((![X41]:(~iext(uri_rdf_type,X41,uri_rdf_Property)|ip(X41)))&(![X42]:(~ip(X42)|iext(uri_rdf_type,X42,uri_rdf_Property)))),inference(variable_rename,[status(thm)],[c131])).])).
% 3.12/3.32  cnf(c134,plain,~iext(uri_rdf_type,X97,uri_rdf_Property)|ip(X97),inference(split_conjunct,[status(thm)],[c133])).
% 3.12/3.32  fof(rdfs_cext_def,axiom,(![X]:(![C]:(iext(uri_rdf_type,X,C)<=>icext(C,X)))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_cext_def)).
% 3.12/3.32  fof(c113,plain,(![X]:(![C]:((~iext(uri_rdf_type,X,C)|icext(C,X))&(~icext(C,X)|iext(uri_rdf_type,X,C))))),inference(fof_nnf,[status(thm)],[rdfs_cext_def])).
% 3.12/3.32  fof(c114,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)],[c113])).
% 3.12/3.32  fof(c116,plain,(![X37]:(![X38]:(![X39]:(![X40]:((~iext(uri_rdf_type,X37,X38)|icext(X38,X37))&(~icext(X40,X39)|iext(uri_rdf_type,X39,X40))))))),inference(shift_quantors,[status(thm)],[fof(c115,plain,((![X37]:(![X38]:(~iext(uri_rdf_type,X37,X38)|icext(X38,X37))))&(![X39]:(![X40]:(~icext(X40,X39)|iext(uri_rdf_type,X39,X40))))),inference(variable_rename,[status(thm)],[c114])).])).
% 3.12/3.32  cnf(c118,plain,~icext(X94,X93)|iext(uri_rdf_type,X93,X94),inference(split_conjunct,[status(thm)],[c116])).
% 3.12/3.32  fof(rdfs_range_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_range,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_range_domain)).
% 3.12/3.32  cnf(c55,plain,iext(uri_rdfs_domain,uri_rdfs_range,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_range_domain])).
% 3.12/3.32  fof(rdfs_domain_main,axiom,(![P]:(![C]:(![X]:(![Y]:((iext(uri_rdfs_domain,P,C)&iext(P,X,Y))=>icext(C,X)))))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_domain_main)).
% 3.12/3.32  fof(c76,plain,(![P]:(![C]:(![X]:(![Y]:((~iext(uri_rdfs_domain,P,C)|~iext(P,X,Y))|icext(C,X)))))),inference(fof_nnf,[status(thm)],[rdfs_domain_main])).
% 3.12/3.32  fof(c77,plain,(![P]:(![C]:(![X]:((~iext(uri_rdfs_domain,P,C)|(![Y]:~iext(P,X,Y)))|icext(C,X))))),inference(shift_quantors,[status(thm)],[c76])).
% 3.12/3.32  fof(c79,plain,(![X30]:(![X31]:(![X32]:(![X33]:((~iext(uri_rdfs_domain,X30,X31)|~iext(X30,X32,X33))|icext(X31,X32)))))),inference(shift_quantors,[status(thm)],[fof(c78,plain,(![X30]:(![X31]:(![X32]:((~iext(uri_rdfs_domain,X30,X31)|(![X33]:~iext(X30,X32,X33)))|icext(X31,X32))))),inference(variable_rename,[status(thm)],[c77])).])).
% 3.12/3.32  cnf(c80,plain,~iext(uri_rdfs_domain,X86,X84)|~iext(X86,X87,X85)|icext(X84,X87),inference(split_conjunct,[status(thm)],[c79])).
% 3.12/3.32  fof(rdfs_annotation_comment_range,axiom,iext(uri_rdfs_range,uri_rdfs_comment,uri_rdfs_Literal),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_comment_range)).
% 3.12/3.32  cnf(c126,plain,iext(uri_rdfs_range,uri_rdfs_comment,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[rdfs_annotation_comment_range])).
% 3.12/3.32  cnf(c417,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X306)|icext(X306,uri_rdfs_comment),inference(resolution,[status(thm)],[c126, c80])).
% 3.12/3.32  cnf(c1245,plain,icext(uri_rdf_Property,uri_rdfs_comment),inference(resolution,[status(thm)],[c417, c55])).
% 3.12/3.32  cnf(c1247,plain,iext(uri_rdf_type,uri_rdfs_comment,uri_rdf_Property),inference(resolution,[status(thm)],[c1245, c118])).
% 3.12/3.32  cnf(c1250,plain,ip(uri_rdfs_comment),inference(resolution,[status(thm)],[c1247, c134])).
% 3.12/3.32  cnf(c1255,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_comment,uri_rdfs_comment),inference(resolution,[status(thm)],[c1250, c20])).
% 3.12/3.32  cnf(c1262,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X619)|iext(X619,uri_rdfs_comment,uri_rdfs_comment),inference(resolution,[status(thm)],[c1255, c28])).
% 3.12/3.32  cnf(c1252,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X618)|iext(X618,uri_rdfs_comment,uri_rdf_Property),inference(resolution,[status(thm)],[c1247, c28])).
% 3.12/3.32  fof(rdfs_annotation_label_range,axiom,iext(uri_rdfs_range,uri_rdfs_label,uri_rdfs_Literal),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_label_range)).
% 3.12/3.32  cnf(c121,plain,iext(uri_rdfs_range,uri_rdfs_label,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[rdfs_annotation_label_range])).
% 3.12/3.32  cnf(c359,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X290)|icext(X290,uri_rdfs_label),inference(resolution,[status(thm)],[c121, c80])).
% 3.12/3.32  cnf(c1216,plain,icext(uri_rdf_Property,uri_rdfs_label),inference(resolution,[status(thm)],[c359, c55])).
% 3.12/3.32  cnf(c1217,plain,iext(uri_rdf_type,uri_rdfs_label,uri_rdf_Property),inference(resolution,[status(thm)],[c1216, c118])).
% 3.12/3.32  cnf(c1220,plain,ip(uri_rdfs_label),inference(resolution,[status(thm)],[c1217, c134])).
% 3.12/3.32  cnf(c1226,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_label,uri_rdfs_label),inference(resolution,[status(thm)],[c1220, c20])).
% 3.12/3.32  cnf(c1233,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X616)|iext(X616,uri_rdfs_label,uri_rdfs_label),inference(resolution,[status(thm)],[c1226, c28])).
% 3.12/3.32  cnf(c1222,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X615)|iext(X615,uri_rdfs_label,uri_rdf_Property),inference(resolution,[status(thm)],[c1217, c28])).
% 3.12/3.32  fof(rdfs_subclassof_trans,axiom,(![C]:(![D]:(![E]:((iext(uri_rdfs_subClassOf,C,D)&iext(uri_rdfs_subClassOf,D,E))=>iext(uri_rdfs_subClassOf,C,E))))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_subclassof_trans)).
% 3.12/3.32  fof(c30,plain,(![C]:(![D]:(![E]:((~iext(uri_rdfs_subClassOf,C,D)|~iext(uri_rdfs_subClassOf,D,E))|iext(uri_rdfs_subClassOf,C,E))))),inference(fof_nnf,[status(thm)],[rdfs_subclassof_trans])).
% 3.12/3.32  fof(c31,plain,(![X13]:(![X14]:(![X15]:((~iext(uri_rdfs_subClassOf,X13,X14)|~iext(uri_rdfs_subClassOf,X14,X15))|iext(uri_rdfs_subClassOf,X13,X15))))),inference(variable_rename,[status(thm)],[c30])).
% 3.12/3.32  cnf(c32,plain,~iext(uri_rdfs_subClassOf,X69,X71)|~iext(uri_rdfs_subClassOf,X71,X70)|iext(uri_rdfs_subClassOf,X69,X70),inference(split_conjunct,[status(thm)],[c31])).
% 3.12/3.32  fof(rdfs_class_instsub_resource,axiom,(![C]:(ic(C)=>iext(uri_rdfs_subClassOf,C,uri_rdfs_Resource))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_class_instsub_resource)).
% 3.12/3.32  fof(c110,plain,(![C]:(~ic(C)|iext(uri_rdfs_subClassOf,C,uri_rdfs_Resource))),inference(fof_nnf,[status(thm)],[rdfs_class_instsub_resource])).
% 3.12/3.32  fof(c111,plain,(![X36]:(~ic(X36)|iext(uri_rdfs_subClassOf,X36,uri_rdfs_Resource))),inference(variable_rename,[status(thm)],[c110])).
% 3.12/3.32  cnf(c112,plain,~ic(X90)|iext(uri_rdfs_subClassOf,X90,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[c111])).
% 3.12/3.32  fof(rdfs_ic_def,axiom,(![X]:(ic(X)<=>icext(uri_rdfs_Class,X))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_ic_def)).
% 3.12/3.32  fof(c69,plain,(![X]:((~ic(X)|icext(uri_rdfs_Class,X))&(~icext(uri_rdfs_Class,X)|ic(X)))),inference(fof_nnf,[status(thm)],[rdfs_ic_def])).
% 3.12/3.32  fof(c70,plain,((![X]:(~ic(X)|icext(uri_rdfs_Class,X)))&(![X]:(~icext(uri_rdfs_Class,X)|ic(X)))),inference(shift_quantors,[status(thm)],[c69])).
% 3.12/3.32  fof(c72,plain,(![X28]:(![X29]:((~ic(X28)|icext(uri_rdfs_Class,X28))&(~icext(uri_rdfs_Class,X29)|ic(X29))))),inference(shift_quantors,[status(thm)],[fof(c71,plain,((![X28]:(~ic(X28)|icext(uri_rdfs_Class,X28)))&(![X29]:(~icext(uri_rdfs_Class,X29)|ic(X29)))),inference(variable_rename,[status(thm)],[c70])).])).
% 3.12/3.32  cnf(c74,plain,~icext(uri_rdfs_Class,X64)|ic(X64),inference(split_conjunct,[status(thm)],[c72])).
% 3.12/3.32  fof(rdfs_range_range,axiom,iext(uri_rdfs_range,uri_rdfs_range,uri_rdfs_Class),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_range_range)).
% 3.12/3.32  cnf(c51,plain,iext(uri_rdfs_range,uri_rdfs_range,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_range_range])).
% 3.12/3.32  fof(rdfs_range_main,axiom,(![P]:(![C]:(![X]:(![Y]:((iext(uri_rdfs_range,P,C)&iext(P,X,Y))=>icext(C,Y)))))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_range_main)).
% 3.12/3.32  fof(c52,plain,(![P]:(![C]:(![X]:(![Y]:((~iext(uri_rdfs_range,P,C)|~iext(P,X,Y))|icext(C,Y)))))),inference(fof_nnf,[status(thm)],[rdfs_range_main])).
% 3.12/3.32  fof(c53,plain,(![X20]:(![X21]:(![X22]:(![X23]:((~iext(uri_rdfs_range,X20,X21)|~iext(X20,X22,X23))|icext(X21,X23)))))),inference(variable_rename,[status(thm)],[c52])).
% 3.12/3.32  cnf(c54,plain,~iext(uri_rdfs_range,X81,X83)|~iext(X81,X80,X82)|icext(X83,X82),inference(split_conjunct,[status(thm)],[c53])).
% 3.12/3.32  fof(rdfs_collection_rest_range,axiom,iext(uri_rdfs_range,uri_rdf_rest,uri_rdf_List),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_collection_rest_range)).
% 3.12/3.32  cnf(c106,plain,iext(uri_rdfs_range,uri_rdf_rest,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdfs_collection_rest_range])).
% 3.12/3.32  cnf(c343,plain,~iext(uri_rdfs_range,uri_rdfs_range,X272)|icext(X272,uri_rdf_List),inference(resolution,[status(thm)],[c106, c54])).
% 3.12/3.32  cnf(c1178,plain,icext(uri_rdfs_Class,uri_rdf_List),inference(resolution,[status(thm)],[c343, c51])).
% 3.12/3.32  cnf(c1179,plain,ic(uri_rdf_List),inference(resolution,[status(thm)],[c1178, c74])).
% 3.12/3.32  cnf(c1183,plain,iext(uri_rdfs_subClassOf,uri_rdf_List,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1179, c112])).
% 3.12/3.32  cnf(c1204,plain,~iext(uri_rdfs_subClassOf,X614,uri_rdf_List)|iext(uri_rdfs_subClassOf,X614,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1183, c32])).
% 3.12/3.32  cnf(c1203,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X613)|iext(X613,uri_rdf_List,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1183, c28])).
% 3.12/3.32  fof(rdfs_subclassof_reflex,axiom,(![C]:(ic(C)=>iext(uri_rdfs_subClassOf,C,C))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_subclassof_reflex)).
% 3.12/3.32  fof(c33,plain,(![C]:(~ic(C)|iext(uri_rdfs_subClassOf,C,C))),inference(fof_nnf,[status(thm)],[rdfs_subclassof_reflex])).
% 3.12/3.32  fof(c34,plain,(![X16]:(~ic(X16)|iext(uri_rdfs_subClassOf,X16,X16))),inference(variable_rename,[status(thm)],[c33])).
% 3.12/3.32  cnf(c35,plain,~ic(X72)|iext(uri_rdfs_subClassOf,X72,X72),inference(split_conjunct,[status(thm)],[c34])).
% 3.12/3.32  cnf(c1182,plain,iext(uri_rdfs_subClassOf,uri_rdf_List,uri_rdf_List),inference(resolution,[status(thm)],[c1179, c35])).
% 3.12/3.32  cnf(c1194,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X611)|iext(X611,uri_rdf_List,uri_rdf_List),inference(resolution,[status(thm)],[c1182, c28])).
% 3.12/3.32  cnf(c1180,plain,iext(uri_rdf_type,uri_rdf_List,uri_rdfs_Class),inference(resolution,[status(thm)],[c1178, c118])).
% 3.12/3.32  cnf(c1188,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X610)|iext(X610,uri_rdf_List,uri_rdfs_Class),inference(resolution,[status(thm)],[c1180, c28])).
% 3.12/3.32  fof(rdfs_collection_first_domain,axiom,iext(uri_rdfs_domain,uri_rdf_first,uri_rdf_List),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_collection_first_domain)).
% 3.12/3.32  cnf(c109,plain,iext(uri_rdfs_domain,uri_rdf_first,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdfs_collection_first_domain])).
% 3.12/3.32  fof(testcase_premise_fullish_027_Inferred_Property_Characteristics_II,axiom,(?[BNODE_l1]:(?[BNODE_l2]:(?[BNODE_v]:(((((iext(uri_owl_propertyChainAxiom,uri_owl_sameAs,BNODE_l1)&iext(uri_rdf_first,BNODE_l1,uri_ex_p))&iext(uri_rdf_rest,BNODE_l1,BNODE_l2))&iext(uri_rdf_first,BNODE_l2,BNODE_v))&iext(uri_rdf_rest,BNODE_l2,uri_rdf_nil))&iext(uri_owl_inverseOf,BNODE_v,uri_ex_p))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', testcase_premise_fullish_027_Inferred_Property_Characteristics_II)).
% 3.12/3.32  fof(c0,plain,(?[X2]:(?[X3]:(?[X4]:(((((iext(uri_owl_propertyChainAxiom,uri_owl_sameAs,X2)&iext(uri_rdf_first,X2,uri_ex_p))&iext(uri_rdf_rest,X2,X3))&iext(uri_rdf_first,X3,X4))&iext(uri_rdf_rest,X3,uri_rdf_nil))&iext(uri_owl_inverseOf,X4,uri_ex_p))))),inference(variable_rename,[status(thm)],[testcase_premise_fullish_027_Inferred_Property_Characteristics_II])).
% 3.12/3.32  fof(c1,plain,(((((iext(uri_owl_propertyChainAxiom,uri_owl_sameAs,skolem0001)&iext(uri_rdf_first,skolem0001,uri_ex_p))&iext(uri_rdf_rest,skolem0001,skolem0002))&iext(uri_rdf_first,skolem0002,skolem0003))&iext(uri_rdf_rest,skolem0002,uri_rdf_nil))&iext(uri_owl_inverseOf,skolem0003,uri_ex_p)),inference(skolemize,[status(esa)],[c0])).
% 3.12/3.32  cnf(c3,plain,iext(uri_rdf_first,skolem0001,uri_ex_p),inference(split_conjunct,[status(thm)],[c1])).
% 3.12/3.32  cnf(c289,plain,~iext(uri_rdfs_domain,uri_rdf_first,X229)|icext(X229,skolem0001),inference(resolution,[status(thm)],[c80, c3])).
% 3.12/3.32  cnf(c1138,plain,icext(uri_rdf_List,skolem0001),inference(resolution,[status(thm)],[c289, c109])).
% 3.12/3.32  cnf(c1139,plain,iext(uri_rdf_type,skolem0001,uri_rdf_List),inference(resolution,[status(thm)],[c1138, c118])).
% 3.12/3.32  cnf(c1143,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X609)|iext(X609,skolem0001,uri_rdf_List),inference(resolution,[status(thm)],[c1139, c28])).
% 3.12/3.32  fof(rdfs_reification_predicate_range,axiom,iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_reification_predicate_range)).
% 3.12/3.32  cnf(c47,plain,iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_reification_predicate_range])).
% 3.12/3.32  cnf(c286,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X226)|icext(X226,uri_rdf_predicate),inference(resolution,[status(thm)],[c80, c47])).
% 3.12/3.32  cnf(c1119,plain,icext(uri_rdf_Property,uri_rdf_predicate),inference(resolution,[status(thm)],[c286, c55])).
% 3.12/3.32  cnf(c1120,plain,iext(uri_rdf_type,uri_rdf_predicate,uri_rdf_Property),inference(resolution,[status(thm)],[c1119, c118])).
% 3.12/3.32  cnf(c1123,plain,ip(uri_rdf_predicate),inference(resolution,[status(thm)],[c1120, c134])).
% 3.12/3.32  cnf(c1129,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_predicate,uri_rdf_predicate),inference(resolution,[status(thm)],[c1123, c20])).
% 3.12/3.32  cnf(c1136,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X607)|iext(X607,uri_rdf_predicate,uri_rdf_predicate),inference(resolution,[status(thm)],[c1129, c28])).
% 3.12/3.32  cnf(c1125,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X606)|iext(X606,uri_rdf_predicate,uri_rdf_Property),inference(resolution,[status(thm)],[c1120, c28])).
% 3.12/3.32  cnf(c4,plain,iext(uri_rdf_rest,skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c1])).
% 3.12/3.32  cnf(c252,plain,~iext(uri_rdfs_range,uri_rdf_rest,X167)|icext(X167,skolem0002),inference(resolution,[status(thm)],[c54, c4])).
% 3.12/3.32  cnf(c1060,plain,icext(uri_rdf_List,skolem0002),inference(resolution,[status(thm)],[c252, c106])).
% 3.12/3.32  cnf(c1061,plain,iext(uri_rdf_type,skolem0002,uri_rdf_List),inference(resolution,[status(thm)],[c1060, c118])).
% 3.12/3.32  cnf(c1109,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X605)|iext(X605,skolem0002,uri_rdf_List),inference(resolution,[status(thm)],[c1061, c28])).
% 3.12/3.32  fof(rdfs_domain_range,axiom,iext(uri_rdfs_range,uri_rdfs_domain,uri_rdfs_Class),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_domain_range)).
% 3.12/3.32  cnf(c75,plain,iext(uri_rdfs_range,uri_rdfs_domain,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_domain_range])).
% 3.12/3.32  fof(rdfs_reification_subject_domain,axiom,iext(uri_rdfs_domain,uri_rdf_subject,uri_rdfs_Statement),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_reification_subject_domain)).
% 3.12/3.32  cnf(c46,plain,iext(uri_rdfs_domain,uri_rdf_subject,uri_rdfs_Statement),inference(split_conjunct,[status(thm)],[rdfs_reification_subject_domain])).
% 3.12/3.32  cnf(c243,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X158)|icext(X158,uri_rdfs_Statement),inference(resolution,[status(thm)],[c54, c46])).
% 3.12/3.32  cnf(c977,plain,icext(uri_rdfs_Class,uri_rdfs_Statement),inference(resolution,[status(thm)],[c243, c75])).
% 3.12/3.32  cnf(c978,plain,ic(uri_rdfs_Statement),inference(resolution,[status(thm)],[c977, c74])).
% 3.12/3.32  cnf(c982,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Statement,uri_rdfs_Resource),inference(resolution,[status(thm)],[c978, c112])).
% 3.12/3.32  cnf(c1101,plain,~iext(uri_rdfs_subClassOf,X604,uri_rdfs_Statement)|iext(uri_rdfs_subClassOf,X604,uri_rdfs_Resource),inference(resolution,[status(thm)],[c982, c32])).
% 3.12/3.32  cnf(c1100,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X603)|iext(X603,uri_rdfs_Statement,uri_rdfs_Resource),inference(resolution,[status(thm)],[c982, c28])).
% 3.12/3.32  cnf(c981,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Statement,uri_rdfs_Statement),inference(resolution,[status(thm)],[c978, c35])).
% 3.12/3.32  cnf(c1092,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X601)|iext(X601,uri_rdfs_Statement,uri_rdfs_Statement),inference(resolution,[status(thm)],[c981, c28])).
% 3.12/3.32  cnf(c979,plain,iext(uri_rdf_type,uri_rdfs_Statement,uri_rdfs_Class),inference(resolution,[status(thm)],[c977, c118])).
% 3.12/3.32  cnf(c1087,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X600)|iext(X600,uri_rdfs_Statement,uri_rdfs_Class),inference(resolution,[status(thm)],[c979, c28])).
% 3.12/3.32  cnf(c27,plain,~iext(uri_rdfs_subPropertyOf,X62,X63)|ip(X63),inference(split_conjunct,[status(thm)],[c25])).
% 3.12/3.32  fof(rdfs_container_containermembershipproperty_instsub_member,axiom,(![P]:(icext(uri_rdfs_ContainerMembershipProperty,P)=>iext(uri_rdfs_subPropertyOf,P,uri_rdfs_member))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_containermembershipproperty_instsub_member)).
% 3.12/3.32  fof(c101,plain,(![P]:(~icext(uri_rdfs_ContainerMembershipProperty,P)|iext(uri_rdfs_subPropertyOf,P,uri_rdfs_member))),inference(fof_nnf,[status(thm)],[rdfs_container_containermembershipproperty_instsub_member])).
% 3.12/3.32  fof(c102,plain,(![X35]:(~icext(uri_rdfs_ContainerMembershipProperty,X35)|iext(uri_rdfs_subPropertyOf,X35,uri_rdfs_member))),inference(variable_rename,[status(thm)],[c101])).
% 3.12/3.32  cnf(c103,plain,~icext(uri_rdfs_ContainerMembershipProperty,X89)|iext(uri_rdfs_subPropertyOf,X89,uri_rdfs_member),inference(split_conjunct,[status(thm)],[c102])).
% 3.12/3.32  fof(rdfs_container_n_type_001,axiom,iext(uri_rdf_type,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_type_001)).
% 3.12/3.32  cnf(c91,plain,iext(uri_rdf_type,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),inference(split_conjunct,[status(thm)],[rdfs_container_n_type_001])).
% 3.12/3.32  cnf(c117,plain,~iext(uri_rdf_type,X92,X91)|icext(X91,X92),inference(split_conjunct,[status(thm)],[c116])).
% 3.12/3.32  cnf(c389,plain,icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__1),inference(resolution,[status(thm)],[c117, c91])).
% 3.12/3.32  cnf(c394,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__1,uri_rdfs_member),inference(resolution,[status(thm)],[c389, c103])).
% 3.12/3.32  cnf(c764,plain,ip(uri_rdfs_member),inference(resolution,[status(thm)],[c394, c27])).
% 3.12/3.32  cnf(c767,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_member,uri_rdfs_member),inference(resolution,[status(thm)],[c764, c20])).
% 3.12/3.32  cnf(c1075,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X598)|iext(X598,uri_rdfs_member,uri_rdfs_member),inference(resolution,[status(thm)],[c767, c28])).
% 3.12/3.32  cnf(c135,plain,~ip(X98)|iext(uri_rdf_type,X98,uri_rdf_Property),inference(split_conjunct,[status(thm)],[c133])).
% 3.12/3.32  cnf(c766,plain,iext(uri_rdf_type,uri_rdfs_member,uri_rdf_Property),inference(resolution,[status(thm)],[c764, c135])).
% 3.12/3.32  cnf(c1068,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X597)|iext(X597,uri_rdfs_member,uri_rdf_Property),inference(resolution,[status(thm)],[c766, c28])).
% 3.12/3.32  cnf(c73,plain,~ic(X61)|icext(uri_rdfs_Class,X61),inference(split_conjunct,[status(thm)],[c72])).
% 3.12/3.32  fof(rdfs_subclassof_main,axiom,(![C]:(![D]:(iext(uri_rdfs_subClassOf,C,D)=>((ic(C)&ic(D))&(![X]:(icext(C,X)=>icext(D,X))))))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_subclassof_main)).
% 3.12/3.32  fof(c37,plain,(![C]:(![D]:(~iext(uri_rdfs_subClassOf,C,D)|((ic(C)&ic(D))&(![X]:(~icext(C,X)|icext(D,X))))))),inference(fof_nnf,[status(thm)],[rdfs_subclassof_main])).
% 3.12/3.32  fof(c39,plain,(![X17]:(![X18]:(![X19]:(~iext(uri_rdfs_subClassOf,X17,X18)|((ic(X17)&ic(X18))&(~icext(X17,X19)|icext(X18,X19))))))),inference(shift_quantors,[status(thm)],[fof(c38,plain,(![X17]:(![X18]:(~iext(uri_rdfs_subClassOf,X17,X18)|((ic(X17)&ic(X18))&(![X19]:(~icext(X17,X19)|icext(X18,X19))))))),inference(variable_rename,[status(thm)],[c37])).])).
% 3.12/3.32  fof(c40,plain,(![X17]:(![X18]:(![X19]:(((~iext(uri_rdfs_subClassOf,X17,X18)|ic(X17))&(~iext(uri_rdfs_subClassOf,X17,X18)|ic(X18)))&(~iext(uri_rdfs_subClassOf,X17,X18)|(~icext(X17,X19)|icext(X18,X19))))))),inference(distribute,[status(thm)],[c39])).
% 3.12/3.32  cnf(c42,plain,~iext(uri_rdfs_subClassOf,X76,X75)|ic(X75),inference(split_conjunct,[status(thm)],[c40])).
% 3.12/3.32  fof(rdfs_dat_xmlliteral_sub,axiom,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Literal),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_dat_xmlliteral_sub)).
% 3.12/3.32  cnf(c87,plain,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[rdfs_dat_xmlliteral_sub])).
% 3.12/3.32  cnf(c41,plain,~iext(uri_rdfs_subClassOf,X74,X73)|ic(X74),inference(split_conjunct,[status(thm)],[c40])).
% 3.12/3.32  cnf(c206,plain,ic(uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c41, c87])).
% 3.12/3.32  cnf(c365,plain,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Resource),inference(resolution,[status(thm)],[c112, c206])).
% 3.12/3.32  cnf(c663,plain,ic(uri_rdfs_Resource),inference(resolution,[status(thm)],[c365, c42])).
% 3.12/3.32  cnf(c668,plain,icext(uri_rdfs_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c663, c73])).
% 3.12/3.32  cnf(c672,plain,iext(uri_rdf_type,uri_rdfs_Resource,uri_rdfs_Class),inference(resolution,[status(thm)],[c668, c118])).
% 3.12/3.32  cnf(c1062,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X596)|iext(X596,uri_rdfs_Resource,uri_rdfs_Class),inference(resolution,[status(thm)],[c672, c28])).
% 3.12/3.32  cnf(c669,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Resource,uri_rdfs_Resource),inference(resolution,[status(thm)],[c663, c35])).
% 3.12/3.32  cnf(c1052,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X594)|iext(X594,uri_rdfs_Resource,uri_rdfs_Resource),inference(resolution,[status(thm)],[c669, c28])).
% 3.12/3.32  cnf(c2,plain,iext(uri_owl_propertyChainAxiom,uri_owl_sameAs,skolem0001),inference(split_conjunct,[status(thm)],[c1])).
% 3.12/3.32  fof(simple_iext_property,axiom,(![S]:(![P]:(![O]:(iext(P,S,O)=>ip(P))))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', simple_iext_property)).
% 3.12/3.32  fof(c150,plain,(![S]:(![P]:(![O]:(~iext(P,S,O)|ip(P))))),inference(fof_nnf,[status(thm)],[simple_iext_property])).
% 3.12/3.32  fof(c151,plain,(![S]:(![P]:((![O]:~iext(P,S,O))|ip(P)))),inference(shift_quantors,[status(thm)],[c150])).
% 3.12/3.32  fof(c153,plain,(![X45]:(![X46]:(![X47]:(~iext(X46,X45,X47)|ip(X46))))),inference(shift_quantors,[status(thm)],[fof(c152,plain,(![X45]:(![X46]:((![X47]:~iext(X46,X45,X47))|ip(X46)))),inference(variable_rename,[status(thm)],[c151])).])).
% 3.12/3.32  cnf(c154,plain,~iext(X99,X101,X100)|ip(X99),inference(split_conjunct,[status(thm)],[c153])).
% 3.12/3.32  cnf(c533,plain,ip(uri_owl_propertyChainAxiom),inference(resolution,[status(thm)],[c154, c2])).
% 3.12/3.32  cnf(c578,plain,iext(uri_rdfs_subPropertyOf,uri_owl_propertyChainAxiom,uri_owl_propertyChainAxiom),inference(resolution,[status(thm)],[c533, c20])).
% 3.12/3.32  cnf(c1044,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X592)|iext(X592,uri_owl_propertyChainAxiom,uri_owl_propertyChainAxiom),inference(resolution,[status(thm)],[c578, c28])).
% 3.12/3.32  cnf(c577,plain,iext(uri_rdf_type,uri_owl_propertyChainAxiom,uri_rdf_Property),inference(resolution,[status(thm)],[c533, c135])).
% 3.12/3.32  cnf(c1036,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X591)|iext(X591,uri_owl_propertyChainAxiom,uri_rdf_Property),inference(resolution,[status(thm)],[c577, c28])).
% 3.12/3.32  fof(rdfs_annotation_isdefinedby_sub,axiom,iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_isdefinedby_sub)).
% 3.12/3.32  cnf(c123,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_sub])).
% 3.12/3.32  cnf(c520,plain,ip(uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c154, c123])).
% 3.12/3.32  cnf(c576,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c520, c20])).
% 3.12/3.32  cnf(c1027,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X589)|iext(X589,uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c576, c28])).
% 3.12/3.32  cnf(c575,plain,iext(uri_rdf_type,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c520, c135])).
% 3.12/3.32  cnf(c1019,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X588)|iext(X588,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c575, c28])).
% 3.12/3.32  cnf(c7,plain,iext(uri_owl_inverseOf,skolem0003,uri_ex_p),inference(split_conjunct,[status(thm)],[c1])).
% 3.12/3.32  cnf(c518,plain,ip(uri_owl_inverseOf),inference(resolution,[status(thm)],[c154, c7])).
% 3.12/3.32  cnf(c574,plain,iext(uri_rdfs_subPropertyOf,uri_owl_inverseOf,uri_owl_inverseOf),inference(resolution,[status(thm)],[c518, c20])).
% 3.12/3.32  cnf(c1010,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X586)|iext(X586,uri_owl_inverseOf,uri_owl_inverseOf),inference(resolution,[status(thm)],[c574, c28])).
% 3.12/3.32  cnf(c573,plain,iext(uri_rdf_type,uri_owl_inverseOf,uri_rdf_Property),inference(resolution,[status(thm)],[c518, c135])).
% 3.12/3.32  cnf(c1003,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X585)|iext(X585,uri_owl_inverseOf,uri_rdf_Property),inference(resolution,[status(thm)],[c573, c28])).
% 3.12/3.32  fof(rdfs_datatype_sub,axiom,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Class),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_datatype_sub)).
% 3.12/3.32  cnf(c82,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_datatype_sub])).
% 3.12/3.32  cnf(c512,plain,ip(uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c154, c82])).
% 3.12/3.32  cnf(c572,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c512, c20])).
% 3.12/3.32  cnf(c990,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X583)|iext(X583,uri_rdfs_subClassOf,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c572, c28])).
% 3.12/3.32  cnf(c571,plain,iext(uri_rdf_type,uri_rdfs_subClassOf,uri_rdf_Property),inference(resolution,[status(thm)],[c512, c135])).
% 3.12/3.32  cnf(c983,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X582)|iext(X582,uri_rdfs_subClassOf,uri_rdf_Property),inference(resolution,[status(thm)],[c571, c28])).
% 3.12/3.32  cnf(c503,plain,ip(uri_rdfs_domain),inference(resolution,[status(thm)],[c154, c46])).
% 3.12/3.32  cnf(c570,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,uri_rdfs_domain),inference(resolution,[status(thm)],[c503, c20])).
% 3.12/3.32  cnf(c957,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X580)|iext(X580,uri_rdfs_domain,uri_rdfs_domain),inference(resolution,[status(thm)],[c570, c28])).
% 3.12/3.32  cnf(c569,plain,iext(uri_rdf_type,uri_rdfs_domain,uri_rdf_Property),inference(resolution,[status(thm)],[c503, c135])).
% 3.12/3.32  cnf(c949,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X579)|iext(X579,uri_rdfs_domain,uri_rdf_Property),inference(resolution,[status(thm)],[c569, c28])).
% 3.12/3.32  cnf(c501,plain,ip(uri_rdfs_range),inference(resolution,[status(thm)],[c154, c47])).
% 3.12/3.32  cnf(c568,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_range,uri_rdfs_range),inference(resolution,[status(thm)],[c501, c20])).
% 3.12/3.32  cnf(c930,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X577)|iext(X577,uri_rdfs_range,uri_rdfs_range),inference(resolution,[status(thm)],[c568, c28])).
% 3.12/3.32  cnf(c567,plain,iext(uri_rdf_type,uri_rdfs_range,uri_rdf_Property),inference(resolution,[status(thm)],[c501, c135])).
% 3.12/3.32  cnf(c922,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X576)|iext(X576,uri_rdfs_range,uri_rdf_Property),inference(resolution,[status(thm)],[c567, c28])).
% 3.12/3.32  fof(rdf_collection_first_type,axiom,iext(uri_rdf_type,uri_rdf_first,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdf_collection_first_type)).
% 3.12/3.32  cnf(c144,plain,iext(uri_rdf_type,uri_rdf_first,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_collection_first_type])).
% 3.12/3.32  cnf(c496,plain,ip(uri_rdf_first),inference(resolution,[status(thm)],[c144, c134])).
% 3.12/3.32  cnf(c500,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_first,uri_rdf_first),inference(resolution,[status(thm)],[c496, c20])).
% 3.12/3.32  cnf(c910,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X574)|iext(X574,uri_rdf_first,uri_rdf_first),inference(resolution,[status(thm)],[c500, c28])).
% 3.12/3.32  fof(rdf_collection_rest_type,axiom,iext(uri_rdf_type,uri_rdf_rest,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdf_collection_rest_type)).
% 3.12/3.32  cnf(c142,plain,iext(uri_rdf_type,uri_rdf_rest,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_collection_rest_type])).
% 3.12/3.32  cnf(c483,plain,ip(uri_rdf_rest),inference(resolution,[status(thm)],[c142, c134])).
% 3.12/3.32  cnf(c491,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_rest,uri_rdf_rest),inference(resolution,[status(thm)],[c483, c20])).
% 3.12/3.32  cnf(c901,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X572)|iext(X572,uri_rdf_rest,uri_rdf_rest),inference(resolution,[status(thm)],[c491, c28])).
% 3.12/3.32  fof(rdf_container_n_type_001,axiom,iext(uri_rdf_type,uri_rdf__1,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdf_container_n_type_001)).
% 3.12/3.32  cnf(c141,plain,iext(uri_rdf_type,uri_rdf__1,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_container_n_type_001])).
% 3.12/3.32  cnf(c472,plain,ip(uri_rdf__1),inference(resolution,[status(thm)],[c141, c134])).
% 3.12/3.32  cnf(c478,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__1,uri_rdf__1),inference(resolution,[status(thm)],[c472, c20])).
% 3.12/3.32  cnf(c893,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X570)|iext(X570,uri_rdf__1,uri_rdf__1),inference(resolution,[status(thm)],[c478, c28])).
% 3.12/3.32  fof(rdf_container_n_type_002,axiom,iext(uri_rdf_type,uri_rdf__2,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdf_container_n_type_002)).
% 3.12/3.32  cnf(c140,plain,iext(uri_rdf_type,uri_rdf__2,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_container_n_type_002])).
% 3.12/3.32  cnf(c467,plain,ip(uri_rdf__2),inference(resolution,[status(thm)],[c140, c134])).
% 3.12/3.32  cnf(c476,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__2,uri_rdf__2),inference(resolution,[status(thm)],[c467, c20])).
% 3.12/3.32  cnf(c885,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X568)|iext(X568,uri_rdf__2,uri_rdf__2),inference(resolution,[status(thm)],[c476, c28])).
% 3.12/3.32  fof(rdf_container_n_type_003,axiom,iext(uri_rdf_type,uri_rdf__3,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdf_container_n_type_003)).
% 3.12/3.32  cnf(c139,plain,iext(uri_rdf_type,uri_rdf__3,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_container_n_type_003])).
% 3.12/3.32  cnf(c459,plain,ip(uri_rdf__3),inference(resolution,[status(thm)],[c139, c134])).
% 3.12/3.32  cnf(c463,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__3,uri_rdf__3),inference(resolution,[status(thm)],[c459, c20])).
% 3.12/3.32  cnf(c878,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X566)|iext(X566,uri_rdf__3,uri_rdf__3),inference(resolution,[status(thm)],[c463, c28])).
% 3.12/3.32  cnf(c377,plain,ip(uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c123, c27])).
% 3.12/3.32  cnf(c454,plain,iext(uri_rdf_type,uri_rdfs_seeAlso,uri_rdf_Property),inference(resolution,[status(thm)],[c135, c377])).
% 3.12/3.32  cnf(c870,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X565)|iext(X565,uri_rdfs_seeAlso,uri_rdf_Property),inference(resolution,[status(thm)],[c454, c28])).
% 3.12/3.32  cnf(c26,plain,~iext(uri_rdfs_subPropertyOf,X55,X56)|ip(X55),inference(split_conjunct,[status(thm)],[c25])).
% 3.12/3.32  cnf(c378,plain,ip(uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c123, c26])).
% 3.12/3.32  cnf(c451,plain,iext(uri_rdf_type,uri_rdfs_isDefinedBy,uri_rdf_Property),inference(resolution,[status(thm)],[c135, c378])).
% 3.12/3.32  cnf(c863,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X564)|iext(X564,uri_rdfs_isDefinedBy,uri_rdf_Property),inference(resolution,[status(thm)],[c451, c28])).
% 3.12/3.32  fof(rdf_reification_object_type,axiom,iext(uri_rdf_type,uri_rdf_object,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdf_reification_object_type)).
% 3.12/3.32  cnf(c138,plain,iext(uri_rdf_type,uri_rdf_object,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_reification_object_type])).
% 3.12/3.32  cnf(c446,plain,ip(uri_rdf_object),inference(resolution,[status(thm)],[c138, c134])).
% 3.12/3.32  cnf(c449,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_object,uri_rdf_object),inference(resolution,[status(thm)],[c446, c20])).
% 3.12/3.32  cnf(c856,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X562)|iext(X562,uri_rdf_object,uri_rdf_object),inference(resolution,[status(thm)],[c449, c28])).
% 3.12/3.32  fof(rdf_reification_subject_type,axiom,iext(uri_rdf_type,uri_rdf_subject,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdf_reification_subject_type)).
% 3.12/3.32  cnf(c136,plain,iext(uri_rdf_type,uri_rdf_subject,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_reification_subject_type])).
% 3.12/3.32  cnf(c440,plain,ip(uri_rdf_subject),inference(resolution,[status(thm)],[c134, c136])).
% 3.12/3.32  cnf(c443,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_subject,uri_rdf_subject),inference(resolution,[status(thm)],[c440, c20])).
% 3.12/3.32  cnf(c849,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X560)|iext(X560,uri_rdf_subject,uri_rdf_subject),inference(resolution,[status(thm)],[c443, c28])).
% 3.12/3.32  fof(rdf_value_type,axiom,iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdf_value_type)).
% 3.12/3.32  cnf(c128,plain,iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_value_type])).
% 3.12/3.32  cnf(c439,plain,ip(uri_rdf_type),inference(resolution,[status(thm)],[c134, c128])).
% 3.12/3.32  cnf(c442,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_type,uri_rdf_type),inference(resolution,[status(thm)],[c439, c20])).
% 3.12/3.32  cnf(c837,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X558)|iext(X558,uri_rdf_type,uri_rdf_type),inference(resolution,[status(thm)],[c442, c28])).
% 3.12/3.32  fof(rdf_reification_predicate_type,axiom,iext(uri_rdf_type,uri_rdf_value,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdf_reification_predicate_type)).
% 3.12/3.32  cnf(c137,plain,iext(uri_rdf_type,uri_rdf_value,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_reification_predicate_type])).
% 3.12/3.32  cnf(c438,plain,ip(uri_rdf_value),inference(resolution,[status(thm)],[c134, c137])).
% 3.12/3.32  cnf(c441,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_value,uri_rdf_value),inference(resolution,[status(thm)],[c438, c20])).
% 3.12/3.32  cnf(c830,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X556)|iext(X556,uri_rdf_value,uri_rdf_value),inference(resolution,[status(thm)],[c441, c28])).
% 3.12/3.32  fof(rdfs_container_containermembershipproperty_sub,axiom,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_containermembershipproperty_sub)).
% 3.12/3.32  cnf(c100,plain,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_container_containermembershipproperty_sub])).
% 3.12/3.32  cnf(c208,plain,ic(uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c41, c100])).
% 3.12/3.32  cnf(c216,plain,icext(uri_rdfs_Class,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c208, c73])).
% 3.12/3.32  cnf(c412,plain,iext(uri_rdf_type,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Class),inference(resolution,[status(thm)],[c118, c216])).
% 3.12/3.32  cnf(c825,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X555)|iext(X555,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Class),inference(resolution,[status(thm)],[c412, c28])).
% 3.12/3.32  cnf(c212,plain,icext(uri_rdfs_Class,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c206, c73])).
% 3.12/3.32  cnf(c411,plain,iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Class),inference(resolution,[status(thm)],[c118, c212])).
% 3.12/3.32  cnf(c820,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X554)|iext(X554,uri_rdf_XMLLiteral,uri_rdfs_Class),inference(resolution,[status(thm)],[c411, c28])).
% 3.12/3.32  fof(rdfs_container_seq_sub,axiom,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Container),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_seq_sub)).
% 3.12/3.32  cnf(c88,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Container),inference(split_conjunct,[status(thm)],[rdfs_container_seq_sub])).
% 3.12/3.32  cnf(c222,plain,ic(uri_rdfs_Container),inference(resolution,[status(thm)],[c42, c88])).
% 3.12/3.32  cnf(c229,plain,icext(uri_rdfs_Class,uri_rdfs_Container),inference(resolution,[status(thm)],[c222, c73])).
% 3.12/3.32  cnf(c410,plain,iext(uri_rdf_type,uri_rdfs_Container,uri_rdfs_Class),inference(resolution,[status(thm)],[c118, c229])).
% 3.12/3.32  cnf(c815,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X553)|iext(X553,uri_rdfs_Container,uri_rdfs_Class),inference(resolution,[status(thm)],[c410, c28])).
% 3.12/3.32  cnf(c207,plain,ic(uri_rdfs_Seq),inference(resolution,[status(thm)],[c41, c88])).
% 3.12/3.32  cnf(c214,plain,icext(uri_rdfs_Class,uri_rdfs_Seq),inference(resolution,[status(thm)],[c207, c73])).
% 3.12/3.32  cnf(c409,plain,iext(uri_rdf_type,uri_rdfs_Seq,uri_rdfs_Class),inference(resolution,[status(thm)],[c118, c214])).
% 3.12/3.32  cnf(c810,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X552)|iext(X552,uri_rdfs_Seq,uri_rdfs_Class),inference(resolution,[status(thm)],[c409, c28])).
% 3.12/3.32  cnf(c205,plain,ic(uri_rdfs_Datatype),inference(resolution,[status(thm)],[c41, c82])).
% 3.12/3.32  cnf(c210,plain,icext(uri_rdfs_Class,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c205, c73])).
% 3.12/3.32  cnf(c405,plain,iext(uri_rdf_type,uri_rdfs_Datatype,uri_rdfs_Class),inference(resolution,[status(thm)],[c118, c210])).
% 3.12/3.32  cnf(c804,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X551)|iext(X551,uri_rdfs_Datatype,uri_rdfs_Class),inference(resolution,[status(thm)],[c405, c28])).
% 3.12/3.32  fof(rdfs_container_alt_sub,axiom,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Container),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_alt_sub)).
% 3.12/3.32  cnf(c105,plain,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Container),inference(split_conjunct,[status(thm)],[rdfs_container_alt_sub])).
% 3.12/3.32  cnf(c337,plain,ic(uri_rdf_Alt),inference(resolution,[status(thm)],[c105, c41])).
% 3.12/3.32  cnf(c338,plain,icext(uri_rdfs_Class,uri_rdf_Alt),inference(resolution,[status(thm)],[c337, c73])).
% 3.12/3.32  cnf(c404,plain,iext(uri_rdf_type,uri_rdf_Alt,uri_rdfs_Class),inference(resolution,[status(thm)],[c118, c338])).
% 3.12/3.32  cnf(c799,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X550)|iext(X550,uri_rdf_Alt,uri_rdfs_Class),inference(resolution,[status(thm)],[c404, c28])).
% 3.12/3.32  fof(rdfs_container_bag_sub,axiom,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Container),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_bag_sub)).
% 3.12/3.32  cnf(c104,plain,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Container),inference(split_conjunct,[status(thm)],[rdfs_container_bag_sub])).
% 3.12/3.32  cnf(c209,plain,ic(uri_rdf_Bag),inference(resolution,[status(thm)],[c41, c104])).
% 3.12/3.32  cnf(c218,plain,icext(uri_rdfs_Class,uri_rdf_Bag),inference(resolution,[status(thm)],[c209, c73])).
% 3.12/3.32  cnf(c401,plain,iext(uri_rdf_type,uri_rdf_Bag,uri_rdfs_Class),inference(resolution,[status(thm)],[c118, c218])).
% 3.12/3.32  cnf(c793,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X549)|iext(X549,uri_rdf_Bag,uri_rdfs_Class),inference(resolution,[status(thm)],[c401, c28])).
% 3.12/3.32  cnf(c221,plain,ic(uri_rdfs_Literal),inference(resolution,[status(thm)],[c42, c87])).
% 3.12/3.32  cnf(c227,plain,icext(uri_rdfs_Class,uri_rdfs_Literal),inference(resolution,[status(thm)],[c221, c73])).
% 3.12/3.32  cnf(c399,plain,iext(uri_rdf_type,uri_rdfs_Literal,uri_rdfs_Class),inference(resolution,[status(thm)],[c118, c227])).
% 3.12/3.32  cnf(c787,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X548)|iext(X548,uri_rdfs_Literal,uri_rdfs_Class),inference(resolution,[status(thm)],[c399, c28])).
% 3.12/3.32  cnf(c220,plain,ic(uri_rdfs_Class),inference(resolution,[status(thm)],[c42, c82])).
% 3.12/3.32  cnf(c225,plain,icext(uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c220, c73])).
% 3.12/3.32  cnf(c398,plain,iext(uri_rdf_type,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c118, c225])).
% 3.12/3.32  cnf(c782,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X547)|iext(X547,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c398, c28])).
% 3.12/3.32  fof(rdfs_subpropertyof_trans,axiom,(![P]:(![Q]:(![R]:((iext(uri_rdfs_subPropertyOf,P,Q)&iext(uri_rdfs_subPropertyOf,Q,R))=>iext(uri_rdfs_subPropertyOf,P,R))))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_subpropertyof_trans)).
% 3.12/3.32  fof(c15,plain,(![P]:(![Q]:(![R]:((~iext(uri_rdfs_subPropertyOf,P,Q)|~iext(uri_rdfs_subPropertyOf,Q,R))|iext(uri_rdfs_subPropertyOf,P,R))))),inference(fof_nnf,[status(thm)],[rdfs_subpropertyof_trans])).
% 3.12/3.32  fof(c16,plain,(![X5]:(![X6]:(![X7]:((~iext(uri_rdfs_subPropertyOf,X5,X6)|~iext(uri_rdfs_subPropertyOf,X6,X7))|iext(uri_rdfs_subPropertyOf,X5,X7))))),inference(variable_rename,[status(thm)],[c15])).
% 3.12/3.32  cnf(c17,plain,~iext(uri_rdfs_subPropertyOf,X50,X52)|~iext(uri_rdfs_subPropertyOf,X52,X51)|iext(uri_rdfs_subPropertyOf,X50,X51),inference(split_conjunct,[status(thm)],[c16])).
% 3.12/3.32  fof(rdfs_container_n_type_003,axiom,iext(uri_rdf_type,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_type_003)).
% 3.12/3.32  cnf(c89,plain,iext(uri_rdf_type,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),inference(split_conjunct,[status(thm)],[rdfs_container_n_type_003])).
% 3.12/3.32  cnf(c392,plain,icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__3),inference(resolution,[status(thm)],[c117, c89])).
% 3.12/3.32  cnf(c397,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__3,uri_rdfs_member),inference(resolution,[status(thm)],[c392, c103])).
% 3.12/3.32  cnf(c778,plain,~iext(uri_rdfs_subPropertyOf,X546,uri_rdf__3)|iext(uri_rdfs_subPropertyOf,X546,uri_rdfs_member),inference(resolution,[status(thm)],[c397, c17])).
% 3.12/3.32  cnf(c775,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X545)|iext(X545,uri_rdf__3,uri_rdfs_member),inference(resolution,[status(thm)],[c397, c28])).
% 3.12/3.32  fof(rdfs_container_n_type_002,axiom,iext(uri_rdf_type,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_type_002)).
% 3.12/3.32  cnf(c90,plain,iext(uri_rdf_type,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),inference(split_conjunct,[status(thm)],[rdfs_container_n_type_002])).
% 3.12/3.32  cnf(c391,plain,icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__2),inference(resolution,[status(thm)],[c117, c90])).
% 3.12/3.32  cnf(c396,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__2,uri_rdfs_member),inference(resolution,[status(thm)],[c391, c103])).
% 3.12/3.32  cnf(c771,plain,~iext(uri_rdfs_subPropertyOf,X544,uri_rdf__2)|iext(uri_rdfs_subPropertyOf,X544,uri_rdfs_member),inference(resolution,[status(thm)],[c396, c17])).
% 3.12/3.32  cnf(c768,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X543)|iext(X543,uri_rdf__2,uri_rdfs_member),inference(resolution,[status(thm)],[c396, c28])).
% 3.12/3.32  cnf(c762,plain,~iext(uri_rdfs_subPropertyOf,X542,uri_rdf__1)|iext(uri_rdfs_subPropertyOf,X542,uri_rdfs_member),inference(resolution,[status(thm)],[c394, c17])).
% 3.12/3.32  cnf(c759,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X541)|iext(X541,uri_rdf__1,uri_rdfs_member),inference(resolution,[status(thm)],[c394, c28])).
% 3.12/3.32  cnf(c1261,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X540)|icext(X540,uri_rdfs_comment),inference(resolution,[status(thm)],[c1255, c54])).
% 3.12/3.32  cnf(c1259,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X539)|icext(X539,uri_rdfs_comment),inference(resolution,[status(thm)],[c1255, c80])).
% 3.12/3.32  cnf(c1232,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X535)|icext(X535,uri_rdfs_label),inference(resolution,[status(thm)],[c1226, c54])).
% 3.12/3.32  cnf(c382,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c378, c20])).
% 3.12/3.32  cnf(c752,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X534)|iext(X534,uri_rdfs_isDefinedBy,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c382, c28])).
% 3.12/3.32  cnf(c1230,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X533)|icext(X533,uri_rdfs_label),inference(resolution,[status(thm)],[c1226, c80])).
% 3.12/3.32  cnf(c1193,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X527)|icext(X527,uri_rdf_List),inference(resolution,[status(thm)],[c1182, c54])).
% 3.12/3.32  cnf(c1191,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X526)|icext(X526,uri_rdf_List),inference(resolution,[status(thm)],[c1182, c80])).
% 3.12/3.32  cnf(c381,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_seeAlso,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c377, c20])).
% 3.12/3.32  cnf(c745,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X525)|iext(X525,uri_rdfs_seeAlso,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c381, c28])).
% 3.12/3.32  cnf(c374,plain,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Resource),inference(resolution,[status(thm)],[c112, c208])).
% 3.12/3.32  cnf(c738,plain,~iext(uri_rdfs_subClassOf,X520,uri_rdfs_ContainerMembershipProperty)|iext(uri_rdfs_subClassOf,X520,uri_rdfs_Resource),inference(resolution,[status(thm)],[c374, c32])).
% 3.12/3.32  cnf(c1135,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X519)|icext(X519,uri_rdf_predicate),inference(resolution,[status(thm)],[c1129, c54])).
% 3.12/3.32  cnf(c1133,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X518)|icext(X518,uri_rdf_predicate),inference(resolution,[status(thm)],[c1129, c80])).
% 3.12/3.32  cnf(c737,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X517)|iext(X517,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Resource),inference(resolution,[status(thm)],[c374, c28])).
% 3.12/3.32  cnf(c373,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Container,uri_rdfs_Resource),inference(resolution,[status(thm)],[c112, c222])).
% 3.12/3.32  cnf(c730,plain,~iext(uri_rdfs_subClassOf,X515,uri_rdfs_Container)|iext(uri_rdfs_subClassOf,X515,uri_rdfs_Resource),inference(resolution,[status(thm)],[c373, c32])).
% 3.12/3.32  cnf(c729,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X510)|iext(X510,uri_rdfs_Container,uri_rdfs_Resource),inference(resolution,[status(thm)],[c373, c28])).
% 3.12/3.32  cnf(c1098,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X508)|icext(X508,uri_rdfs_Statement),inference(resolution,[status(thm)],[c981, c54])).
% 3.12/3.32  cnf(c372,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c112, c220])).
% 3.12/3.32  cnf(c722,plain,~iext(uri_rdfs_subClassOf,X507,uri_rdfs_Class)|iext(uri_rdfs_subClassOf,X507,uri_rdfs_Resource),inference(resolution,[status(thm)],[c372, c32])).
% 3.12/3.32  cnf(c1094,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X506)|icext(X506,uri_rdfs_Statement),inference(resolution,[status(thm)],[c981, c80])).
% 3.12/3.32  cnf(c721,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X503)|iext(X503,uri_rdfs_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c372, c28])).
% 3.12/3.32  cnf(c1077,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X501)|icext(X501,uri_rdfs_member),inference(resolution,[status(thm)],[c767, c80])).
% 3.12/3.32  cnf(c371,plain,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Resource),inference(resolution,[status(thm)],[c112, c337])).
% 3.12/3.32  cnf(c714,plain,~iext(uri_rdfs_subClassOf,X499,uri_rdf_Alt)|iext(uri_rdfs_subClassOf,X499,uri_rdfs_Resource),inference(resolution,[status(thm)],[c371, c32])).
% 3.12/3.32  cnf(c713,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X494)|iext(X494,uri_rdf_Alt,uri_rdfs_Resource),inference(resolution,[status(thm)],[c371, c28])).
% 3.12/3.32  cnf(c1054,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X493)|icext(X493,uri_rdfs_Resource),inference(resolution,[status(thm)],[c669, c80])).
% 3.12/3.32  cnf(c1051,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X492)|icext(X492,uri_owl_propertyChainAxiom),inference(resolution,[status(thm)],[c578, c54])).
% 3.12/3.32  cnf(c370,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Resource),inference(resolution,[status(thm)],[c112, c205])).
% 3.12/3.32  cnf(c706,plain,~iext(uri_rdfs_subClassOf,X491,uri_rdfs_Datatype)|iext(uri_rdfs_subClassOf,X491,uri_rdfs_Resource),inference(resolution,[status(thm)],[c370, c32])).
% 3.12/3.32  cnf(c1046,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X490)|icext(X490,uri_owl_propertyChainAxiom),inference(resolution,[status(thm)],[c578, c80])).
% 3.12/3.32  cnf(c705,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X487)|iext(X487,uri_rdfs_Datatype,uri_rdfs_Resource),inference(resolution,[status(thm)],[c370, c28])).
% 3.12/3.32  cnf(c1034,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X486)|icext(X486,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c576, c54])).
% 3.12/3.32  cnf(c369,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Literal,uri_rdfs_Resource),inference(resolution,[status(thm)],[c112, c221])).
% 3.12/3.32  cnf(c698,plain,~iext(uri_rdfs_subClassOf,X485,uri_rdfs_Literal)|iext(uri_rdfs_subClassOf,X485,uri_rdfs_Resource),inference(resolution,[status(thm)],[c369, c32])).
% 3.12/3.32  cnf(c1030,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X484)|icext(X484,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c576, c80])).
% 3.12/3.32  cnf(c697,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X481)|iext(X481,uri_rdfs_Literal,uri_rdfs_Resource),inference(resolution,[status(thm)],[c369, c28])).
% 3.12/3.32  cnf(c1017,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X480)|icext(X480,uri_owl_inverseOf),inference(resolution,[status(thm)],[c574, c54])).
% 3.12/3.32  cnf(c1012,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X479)|icext(X479,uri_owl_inverseOf),inference(resolution,[status(thm)],[c574, c80])).
% 3.12/3.32  cnf(c368,plain,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Resource),inference(resolution,[status(thm)],[c112, c209])).
% 3.12/3.32  cnf(c690,plain,~iext(uri_rdfs_subClassOf,X477,uri_rdf_Bag)|iext(uri_rdfs_subClassOf,X477,uri_rdfs_Resource),inference(resolution,[status(thm)],[c368, c32])).
% 3.12/3.32  cnf(c1001,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X475)|icext(X475,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c572, c54])).
% 3.12/3.32  cnf(c689,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X474)|iext(X474,uri_rdf_Bag,uri_rdfs_Resource),inference(resolution,[status(thm)],[c368, c28])).
% 3.12/3.32  cnf(c995,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X473)|icext(X473,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c572, c80])).
% 3.12/3.32  cnf(c367,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Resource),inference(resolution,[status(thm)],[c112, c207])).
% 3.12/3.32  cnf(c682,plain,~iext(uri_rdfs_subClassOf,X470,uri_rdfs_Seq)|iext(uri_rdfs_subClassOf,X470,uri_rdfs_Resource),inference(resolution,[status(thm)],[c367, c32])).
% 3.12/3.32  cnf(c975,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X469)|icext(X469,uri_rdfs_domain),inference(resolution,[status(thm)],[c570, c54])).
% 3.12/3.32  cnf(c966,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X468)|icext(X468,uri_rdfs_domain),inference(resolution,[status(thm)],[c570, c80])).
% 3.12/3.32  cnf(c681,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X466)|iext(X466,uri_rdfs_Seq,uri_rdfs_Resource),inference(resolution,[status(thm)],[c367, c28])).
% 3.12/3.32  cnf(c946,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X464)|icext(X464,uri_rdfs_range),inference(resolution,[status(thm)],[c568, c54])).
% 3.12/3.32  cnf(c223,plain,ic(uri_rdf_Property),inference(resolution,[status(thm)],[c42, c100])).
% 3.12/3.32  cnf(c366,plain,iext(uri_rdfs_subClassOf,uri_rdf_Property,uri_rdfs_Resource),inference(resolution,[status(thm)],[c112, c223])).
% 3.12/3.32  cnf(c674,plain,~iext(uri_rdfs_subClassOf,X463,uri_rdf_Property)|iext(uri_rdfs_subClassOf,X463,uri_rdfs_Resource),inference(resolution,[status(thm)],[c366, c32])).
% 3.12/3.32  cnf(c937,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X462)|icext(X462,uri_rdfs_range),inference(resolution,[status(thm)],[c568, c80])).
% 3.12/3.32  cnf(c673,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X459)|iext(X459,uri_rdf_Property,uri_rdfs_Resource),inference(resolution,[status(thm)],[c366, c28])).
% 3.12/3.32  cnf(c917,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X458)|icext(X458,uri_rdf_first),inference(resolution,[status(thm)],[c500, c54])).
% 3.12/3.32  cnf(c912,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X457)|icext(X457,uri_rdf_first),inference(resolution,[status(thm)],[c500, c80])).
% 3.12/3.32  cnf(c661,plain,~iext(uri_rdfs_subClassOf,X456,uri_rdf_XMLLiteral)|iext(uri_rdfs_subClassOf,X456,uri_rdfs_Resource),inference(resolution,[status(thm)],[c365, c32])).
% 3.12/3.32  cnf(c909,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X455)|icext(X455,uri_rdf_rest),inference(resolution,[status(thm)],[c491, c54])).
% 3.12/3.32  cnf(c903,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X454)|icext(X454,uri_rdf_rest),inference(resolution,[status(thm)],[c491, c80])).
% 3.12/3.32  cnf(c660,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X453)|iext(X453,uri_rdf_XMLLiteral,uri_rdfs_Resource),inference(resolution,[status(thm)],[c365, c28])).
% 3.12/3.32  cnf(c899,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X452)|icext(X452,uri_rdf__1),inference(resolution,[status(thm)],[c478, c54])).
% 3.12/3.32  cnf(c891,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X450)|icext(X450,uri_rdf__2),inference(resolution,[status(thm)],[c476, c54])).
% 3.12/3.32  cnf(c884,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X447)|icext(X447,uri_rdf__3),inference(resolution,[status(thm)],[c463, c54])).
% 3.12/3.32  cnf(c339,plain,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdf_Alt),inference(resolution,[status(thm)],[c337, c35])).
% 3.12/3.32  cnf(c652,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X445)|iext(X445,uri_rdf_Alt,uri_rdf_Alt),inference(resolution,[status(thm)],[c339, c28])).
% 3.12/3.32  cnf(c862,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X439)|icext(X439,uri_rdf_object),inference(resolution,[status(thm)],[c449, c54])).
% 3.12/3.32  cnf(c858,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X438)|icext(X438,uri_rdf_object),inference(resolution,[status(thm)],[c449, c80])).
% 3.12/3.32  cnf(c232,plain,iext(uri_rdfs_subClassOf,uri_rdf_Property,uri_rdf_Property),inference(resolution,[status(thm)],[c223, c35])).
% 3.12/3.32  cnf(c644,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X437)|iext(X437,uri_rdf_Property,uri_rdf_Property),inference(resolution,[status(thm)],[c232, c28])).
% 3.12/3.32  cnf(c855,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X436)|icext(X436,uri_rdf_subject),inference(resolution,[status(thm)],[c443, c54])).
% 3.12/3.32  cnf(c851,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X435)|icext(X435,uri_rdf_subject),inference(resolution,[status(thm)],[c443, c80])).
% 3.12/3.32  cnf(c848,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X434)|icext(X434,uri_rdf_type),inference(resolution,[status(thm)],[c442, c54])).
% 3.12/3.32  cnf(c841,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X432)|icext(X432,uri_rdf_type),inference(resolution,[status(thm)],[c442, c80])).
% 3.12/3.32  cnf(c836,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X431)|icext(X431,uri_rdf_value),inference(resolution,[status(thm)],[c441, c54])).
% 3.12/3.32  cnf(c230,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Container,uri_rdfs_Container),inference(resolution,[status(thm)],[c222, c35])).
% 3.12/3.32  cnf(c636,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X430)|iext(X430,uri_rdfs_Container,uri_rdfs_Container),inference(resolution,[status(thm)],[c230, c28])).
% 3.12/3.32  cnf(c832,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X429)|icext(X429,uri_rdf_value),inference(resolution,[status(thm)],[c441, c80])).
% 3.12/3.32  cnf(c228,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Literal,uri_rdfs_Literal),inference(resolution,[status(thm)],[c221, c35])).
% 3.12/3.32  cnf(c628,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X420)|iext(X420,uri_rdfs_Literal,uri_rdfs_Literal),inference(resolution,[status(thm)],[c228, c28])).
% 3.12/3.32  cnf(c226,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c220, c35])).
% 3.12/3.32  cnf(c620,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X409)|iext(X409,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c226, c28])).
% 3.12/3.32  cnf(c777,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X405)|icext(X405,uri_rdf__3),inference(resolution,[status(thm)],[c397, c80])).
% 3.12/3.32  cnf(c770,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X402)|icext(X402,uri_rdf__2),inference(resolution,[status(thm)],[c396, c80])).
% 3.12/3.32  cnf(c219,plain,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdf_Bag),inference(resolution,[status(thm)],[c209, c35])).
% 3.12/3.32  cnf(c612,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X401)|iext(X401,uri_rdf_Bag,uri_rdf_Bag),inference(resolution,[status(thm)],[c219, c28])).
% 3.12/3.32  cnf(c765,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X400)|icext(X400,uri_rdfs_member),inference(resolution,[status(thm)],[c394, c54])).
% 3.12/3.32  cnf(c761,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X399)|icext(X399,uri_rdf__1),inference(resolution,[status(thm)],[c394, c80])).
% 3.12/3.32  cnf(c758,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X398)|icext(X398,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c382, c54])).
% 3.12/3.32  cnf(c747,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X394)|icext(X394,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c381, c80])).
% 3.12/3.32  cnf(c217,plain,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c208, c35])).
% 3.12/3.32  cnf(c604,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X393)|iext(X393,uri_rdfs_ContainerMembershipProperty,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c217, c28])).
% 3.12/3.32  cnf(c215,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Seq),inference(resolution,[status(thm)],[c207, c35])).
% 3.12/3.32  cnf(c596,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X382)|iext(X382,uri_rdfs_Seq,uri_rdfs_Seq),inference(resolution,[status(thm)],[c215, c28])).
% 3.12/3.32  cnf(c213,plain,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c206, c35])).
% 3.12/3.32  cnf(c588,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X371)|iext(X371,uri_rdf_XMLLiteral,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c213, c28])).
% 3.12/3.32  cnf(c666,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X370)|icext(X370,uri_rdfs_Resource),inference(resolution,[status(thm)],[c365, c54])).
% 3.12/3.32  cnf(c658,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X368)|icext(X368,uri_rdf_Alt),inference(resolution,[status(thm)],[c339, c54])).
% 3.12/3.32  cnf(c646,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X364)|icext(X364,uri_rdf_Property),inference(resolution,[status(thm)],[c232, c80])).
% 3.12/3.32  cnf(c211,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c205, c35])).
% 3.12/3.32  cnf(c580,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X363)|iext(X363,uri_rdfs_Datatype,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c211, c28])).
% 3.12/3.32  cnf(c638,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X361)|icext(X361,uri_rdfs_Container),inference(resolution,[status(thm)],[c230, c80])).
% 3.12/3.32  cnf(c495,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X359)|iext(X359,uri_rdf_first,uri_rdf_Property),inference(resolution,[status(thm)],[c144, c28])).
% 3.12/3.32  cnf(c630,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X358)|icext(X358,uri_rdfs_Literal),inference(resolution,[status(thm)],[c228, c80])).
% 3.12/3.32  fof(rdf_collection_nil_type,axiom,iext(uri_rdf_type,uri_rdf_nil,uri_rdf_List),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdf_collection_nil_type)).
% 3.12/3.32  cnf(c143,plain,iext(uri_rdf_type,uri_rdf_nil,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdf_collection_nil_type])).
% 3.12/3.32  cnf(c487,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X356)|iext(X356,uri_rdf_nil,uri_rdf_List),inference(resolution,[status(thm)],[c143, c28])).
% 3.12/3.32  cnf(c622,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X355)|icext(X355,uri_rdfs_Class),inference(resolution,[status(thm)],[c226, c80])).
% 3.12/3.32  cnf(c618,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X354)|icext(X354,uri_rdf_Bag),inference(resolution,[status(thm)],[c219, c54])).
% 3.12/3.32  cnf(c482,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X352)|iext(X352,uri_rdf_rest,uri_rdf_Property),inference(resolution,[status(thm)],[c142, c28])).
% 3.12/3.32  cnf(c610,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X351)|icext(X351,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c217, c54])).
% 3.12/3.32  cnf(c471,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X349)|iext(X349,uri_rdf__1,uri_rdf_Property),inference(resolution,[status(thm)],[c141, c28])).
% 3.12/3.32  cnf(c602,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X348)|icext(X348,uri_rdfs_Seq),inference(resolution,[status(thm)],[c215, c54])).
% 3.12/3.32  cnf(c594,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X346)|icext(X346,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c213, c54])).
% 3.12/3.32  cnf(c466,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X345)|iext(X345,uri_rdf__2,uri_rdf_Property),inference(resolution,[status(thm)],[c140, c28])).
% 3.12/3.32  cnf(c586,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X343)|icext(X343,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c211, c54])).
% 3.12/3.32  cnf(c458,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X341)|iext(X341,uri_rdf__3,uri_rdf_Property),inference(resolution,[status(thm)],[c139, c28])).
% 3.12/3.32  cnf(c489,plain,~iext(uri_rdfs_range,uri_rdf_type,X338)|icext(X338,uri_rdf_List),inference(resolution,[status(thm)],[c143, c54])).
% 3.12/3.32  cnf(c445,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X337)|iext(X337,uri_rdf_object,uri_rdf_Property),inference(resolution,[status(thm)],[c138, c28])).
% 3.12/3.32  cnf(c434,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X332)|iext(X332,uri_rdf_value,uri_rdf_Property),inference(resolution,[status(thm)],[c137, c28])).
% 3.12/3.32  cnf(c429,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X327)|iext(X327,uri_rdf_subject,uri_rdf_Property),inference(resolution,[status(thm)],[c136, c28])).
% 3.12/3.32  cnf(c424,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X322)|iext(X322,uri_rdf_type,uri_rdf_Property),inference(resolution,[status(thm)],[c128, c28])).
% 3.12/3.32  fof(rdfs_annotation_comment_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_comment,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_comment_domain)).
% 3.12/3.32  cnf(c127,plain,iext(uri_rdfs_domain,uri_rdfs_comment,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_comment_domain])).
% 3.12/3.32  cnf(c421,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X318)|iext(X318,uri_rdfs_comment,uri_rdfs_Resource),inference(resolution,[status(thm)],[c127, c28])).
% 3.12/3.32  cnf(c426,plain,~iext(uri_rdfs_range,uri_rdf_type,X317)|icext(X317,uri_rdf_Property),inference(resolution,[status(thm)],[c128, c54])).
% 3.12/3.32  cnf(c418,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X314)|iext(X314,uri_rdfs_comment,uri_rdfs_Literal),inference(resolution,[status(thm)],[c126, c28])).
% 3.12/3.32  cnf(c420,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X313)|icext(X313,uri_rdfs_comment),inference(resolution,[status(thm)],[c127, c80])).
% 3.12/3.32  fof(simple_ir,axiom,(![X]:ir(X)),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', simple_ir)).
% 3.12/3.32  fof(c148,plain,(![X44]:ir(X44)),inference(variable_rename,[status(thm)],[simple_ir])).
% 3.12/3.32  cnf(c149,plain,ir(X48),inference(split_conjunct,[status(thm)],[c148])).
% 3.12/3.32  fof(rdfs_ir_def,axiom,(![X]:(ir(X)<=>icext(uri_rdfs_Resource,X))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_ir_def)).
% 3.12/3.32  fof(c63,plain,(![X]:((~ir(X)|icext(uri_rdfs_Resource,X))&(~icext(uri_rdfs_Resource,X)|ir(X)))),inference(fof_nnf,[status(thm)],[rdfs_ir_def])).
% 3.12/3.32  fof(c64,plain,((![X]:(~ir(X)|icext(uri_rdfs_Resource,X)))&(![X]:(~icext(uri_rdfs_Resource,X)|ir(X)))),inference(shift_quantors,[status(thm)],[c63])).
% 3.12/3.32  fof(c66,plain,(![X26]:(![X27]:((~ir(X26)|icext(uri_rdfs_Resource,X26))&(~icext(uri_rdfs_Resource,X27)|ir(X27))))),inference(shift_quantors,[status(thm)],[fof(c65,plain,((![X26]:(~ir(X26)|icext(uri_rdfs_Resource,X26)))&(![X27]:(~icext(uri_rdfs_Resource,X27)|ir(X27)))),inference(variable_rename,[status(thm)],[c64])).])).
% 3.12/3.32  cnf(c67,plain,~ir(X58)|icext(uri_rdfs_Resource,X58),inference(split_conjunct,[status(thm)],[c66])).
% 3.12/3.32  cnf(c156,plain,icext(uri_rdfs_Resource,X59),inference(resolution,[status(thm)],[c67, c149])).
% 3.12/3.32  cnf(c400,plain,iext(uri_rdf_type,X95,uri_rdfs_Resource),inference(resolution,[status(thm)],[c118, c156])).
% 3.12/3.32  cnf(c414,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X310)|iext(X310,X309,uri_rdfs_Resource),inference(resolution,[status(thm)],[c400, c28])).
% 3.12/3.32  fof(rdfs_annotation_isdefinedby_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_isdefinedby_domain)).
% 3.12/3.32  cnf(c125,plain,iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_domain])).
% 3.12/3.32  cnf(c387,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X308)|iext(X308,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(resolution,[status(thm)],[c125, c28])).
% 3.12/3.32  fof(rdfs_annotation_isdefinedby_range,axiom,iext(uri_rdfs_range,uri_rdfs_isDefinedBy,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_isdefinedby_range)).
% 3.12/3.33  cnf(c124,plain,iext(uri_rdfs_range,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_range])).
% 3.12/3.33  cnf(c384,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X307)|iext(X307,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(resolution,[status(thm)],[c124, c28])).
% 3.12/3.33  cnf(c416,plain,~iext(uri_rdfs_range,uri_rdf_type,X305)|icext(X305,uri_rdfs_Resource),inference(resolution,[status(thm)],[c400, c54])).
% 3.12/3.33  cnf(c379,plain,~iext(uri_rdfs_subPropertyOf,X303,uri_rdfs_isDefinedBy)|iext(uri_rdfs_subPropertyOf,X303,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c123, c17])).
% 3.12/3.33  cnf(c386,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X302)|icext(X302,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c125, c80])).
% 3.12/3.33  cnf(c376,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X300)|iext(X300,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c123, c28])).
% 3.12/3.33  cnf(c383,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X299)|icext(X299,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c124, c80])).
% 3.12/3.33  cnf(c380,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X298)|icext(X298,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c123, c54])).
% 3.12/3.33  fof(rdfs_annotation_label_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_label,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_label_domain)).
% 3.12/3.33  cnf(c122,plain,iext(uri_rdfs_domain,uri_rdfs_label,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_label_domain])).
% 3.12/3.33  cnf(c363,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X297)|iext(X297,uri_rdfs_label,uri_rdfs_Resource),inference(resolution,[status(thm)],[c122, c28])).
% 3.12/3.33  cnf(c375,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X296)|icext(X296,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c123, c80])).
% 3.12/3.33  cnf(c362,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X294)|icext(X294,uri_rdfs_label),inference(resolution,[status(thm)],[c122, c80])).
% 3.12/3.33  cnf(c361,plain,~iext(uri_rdfs_range,uri_rdfs_range,X293)|icext(X293,uri_rdfs_Literal),inference(resolution,[status(thm)],[c121, c54])).
% 3.12/3.33  cnf(c360,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X292)|iext(X292,uri_rdfs_label,uri_rdfs_Literal),inference(resolution,[status(thm)],[c121, c28])).
% 3.12/3.33  fof(rdfs_annotation_seealso_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_seeAlso,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_seealso_domain)).
% 3.12/3.33  cnf(c120,plain,iext(uri_rdfs_domain,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_seealso_domain])).
% 3.12/3.33  cnf(c357,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X291)|iext(X291,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(resolution,[status(thm)],[c120, c28])).
% 3.12/3.33  fof(rdfs_annotation_seealso_range,axiom,iext(uri_rdfs_range,uri_rdfs_seeAlso,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_seealso_range)).
% 3.12/3.33  cnf(c119,plain,iext(uri_rdfs_range,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_seealso_range])).
% 3.12/3.33  cnf(c354,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X288)|iext(X288,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(resolution,[status(thm)],[c119, c28])).
% 3.12/3.33  cnf(c356,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X287)|icext(X287,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c120, c80])).
% 3.12/3.33  cnf(c351,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X285)|iext(X285,uri_rdf_first,uri_rdf_List),inference(resolution,[status(thm)],[c109, c28])).
% 3.12/3.33  cnf(c353,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X284)|icext(X284,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c119, c80])).
% 3.12/3.33  cnf(c350,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X282)|icext(X282,uri_rdf_first),inference(resolution,[status(thm)],[c109, c80])).
% 3.12/3.33  fof(rdfs_collection_first_range,axiom,iext(uri_rdfs_range,uri_rdf_first,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_collection_first_range)).
% 3.12/3.33  cnf(c108,plain,iext(uri_rdfs_range,uri_rdf_first,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_collection_first_range])).
% 3.12/3.33  cnf(c348,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X281)|iext(X281,uri_rdf_first,uri_rdfs_Resource),inference(resolution,[status(thm)],[c108, c28])).
% 3.12/3.33  cnf(c347,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X279)|icext(X279,uri_rdf_first),inference(resolution,[status(thm)],[c108, c80])).
% 3.12/3.33  fof(rdfs_collection_rest_domain,axiom,iext(uri_rdfs_domain,uri_rdf_rest,uri_rdf_List),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_collection_rest_domain)).
% 3.12/3.33  cnf(c107,plain,iext(uri_rdfs_domain,uri_rdf_rest,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdfs_collection_rest_domain])).
% 3.12/3.33  cnf(c346,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X277)|icext(X277,uri_rdf_List),inference(resolution,[status(thm)],[c107, c54])).
% 3.12/3.33  cnf(c345,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X275)|iext(X275,uri_rdf_rest,uri_rdf_List),inference(resolution,[status(thm)],[c107, c28])).
% 3.12/3.33  cnf(c344,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X274)|icext(X274,uri_rdf_rest),inference(resolution,[status(thm)],[c107, c80])).
% 3.12/3.33  cnf(c342,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X273)|iext(X273,uri_rdf_rest,uri_rdf_List),inference(resolution,[status(thm)],[c106, c28])).
% 3.12/3.33  cnf(c334,plain,~iext(uri_rdfs_subClassOf,X271,uri_rdf_Alt)|iext(uri_rdfs_subClassOf,X271,uri_rdfs_Container),inference(resolution,[status(thm)],[c105, c32])).
% 3.12/3.33  cnf(c341,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X270)|icext(X270,uri_rdf_rest),inference(resolution,[status(thm)],[c106, c80])).
% 3.12/3.33  cnf(c332,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X268)|iext(X268,uri_rdf_Alt,uri_rdfs_Container),inference(resolution,[status(thm)],[c105, c28])).
% 3.12/3.33  cnf(c331,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X267)|icext(X267,uri_rdf_Alt),inference(resolution,[status(thm)],[c105, c80])).
% 3.12/3.33  cnf(c326,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X266)|icext(X266,uri_rdf_Bag),inference(resolution,[status(thm)],[c80, c104])).
% 3.12/3.33  fof(rdfs_reification_subject_range,axiom,iext(uri_rdfs_range,uri_rdf_subject,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_reification_subject_range)).
% 3.12/3.33  cnf(c45,plain,iext(uri_rdfs_range,uri_rdf_subject,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_reification_subject_range])).
% 3.12/3.33  cnf(c325,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X265)|icext(X265,uri_rdf_subject),inference(resolution,[status(thm)],[c80, c45])).
% 3.12/3.33  cnf(c324,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X264)|icext(X264,uri_rdfs_range),inference(resolution,[status(thm)],[c80, c55])).
% 3.12/3.33  fof(rdfs_container_n_domain_002,axiom,iext(uri_rdfs_domain,uri_rdf__2,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_domain_002)).
% 3.12/3.33  cnf(c96,plain,iext(uri_rdfs_domain,uri_rdf__2,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_002])).
% 3.12/3.33  cnf(c323,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X263)|icext(X263,uri_rdf__2),inference(resolution,[status(thm)],[c80, c96])).
% 3.12/3.33  fof(rdfs_subpropertyof_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_subpropertyof_domain)).
% 3.12/3.33  cnf(c29,plain,iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_subpropertyof_domain])).
% 3.12/3.33  cnf(c322,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X262)|icext(X262,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c80, c29])).
% 3.12/3.33  fof(rdfs_type_domain,axiom,iext(uri_rdfs_domain,uri_rdf_type,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_type_domain)).
% 3.12/3.33  cnf(c14,plain,iext(uri_rdfs_domain,uri_rdf_type,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_type_domain])).
% 3.12/3.33  cnf(c321,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X261)|icext(X261,uri_rdf_type),inference(resolution,[status(thm)],[c80, c14])).
% 3.12/3.33  cnf(c320,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X260)|icext(X260,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c80, c100])).
% 3.12/3.33  fof(rdfs_subpropertyof_range,axiom,iext(uri_rdfs_range,uri_rdfs_subPropertyOf,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_subpropertyof_range)).
% 3.12/3.33  cnf(c21,plain,iext(uri_rdfs_range,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_subpropertyof_range])).
% 3.12/3.33  cnf(c316,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X256)|icext(X256,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c80, c21])).
% 3.12/3.33  fof(rdfs_reification_object_domain,axiom,iext(uri_rdfs_domain,uri_rdf_object,uri_rdfs_Statement),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_reification_object_domain)).
% 3.12/3.33  cnf(c50,plain,iext(uri_rdfs_domain,uri_rdf_object,uri_rdfs_Statement),inference(split_conjunct,[status(thm)],[rdfs_reification_object_domain])).
% 3.12/3.33  cnf(c315,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X255)|icext(X255,uri_rdf_object),inference(resolution,[status(thm)],[c80, c50])).
% 3.12/3.33  fof(rdfs_container_n_range_003,axiom,iext(uri_rdfs_range,uri_rdf__3,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_range_003)).
% 3.12/3.33  cnf(c92,plain,iext(uri_rdfs_range,uri_rdf__3,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_range_003])).
% 3.12/3.33  cnf(c314,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X254)|icext(X254,uri_rdf__3),inference(resolution,[status(thm)],[c80, c92])).
% 3.12/3.33  fof(rdfs_subclassof_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdfs_Class),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_subclassof_domain)).
% 3.12/3.33  cnf(c44,plain,iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_subclassof_domain])).
% 3.12/3.33  cnf(c313,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X253)|icext(X253,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c80, c44])).
% 3.12/3.33  fof(rdfs_container_n_domain_003,axiom,iext(uri_rdfs_domain,uri_rdf__3,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_domain_003)).
% 3.12/3.33  cnf(c95,plain,iext(uri_rdfs_domain,uri_rdf__3,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_003])).
% 3.12/3.33  cnf(c312,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X252)|icext(X252,uri_rdf__3),inference(resolution,[status(thm)],[c80, c95])).
% 3.12/3.33  fof(rdfs_value_domain,axiom,iext(uri_rdfs_domain,uri_rdf_value,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_value_domain)).
% 3.12/3.33  cnf(c12,plain,iext(uri_rdfs_domain,uri_rdf_value,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_value_domain])).
% 3.12/3.33  cnf(c311,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X251)|icext(X251,uri_rdf_value),inference(resolution,[status(thm)],[c80, c12])).
% 3.12/3.33  cnf(c310,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X250)|icext(X250,uri_rdfs_range),inference(resolution,[status(thm)],[c80, c51])).
% 3.12/3.33  fof(rdfs_container_member_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_member,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_member_domain)).
% 3.12/3.33  cnf(c99,plain,iext(uri_rdfs_domain,uri_rdfs_member,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_member_domain])).
% 3.12/3.33  cnf(c309,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X249)|icext(X249,uri_rdfs_member),inference(resolution,[status(thm)],[c80, c99])).
% 3.12/3.33  cnf(c308,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X248)|icext(X248,uri_rdfs_Seq),inference(resolution,[status(thm)],[c80, c88])).
% 3.12/3.33  fof(rdfs_subclassof_range,axiom,iext(uri_rdfs_range,uri_rdfs_subClassOf,uri_rdfs_Class),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_subclassof_range)).
% 3.12/3.33  cnf(c36,plain,iext(uri_rdfs_range,uri_rdfs_subClassOf,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_subclassof_range])).
% 3.12/3.33  cnf(c307,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X247)|icext(X247,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c80, c36])).
% 3.12/3.33  fof(rdfs_type_range,axiom,iext(uri_rdfs_range,uri_rdf_type,uri_rdfs_Class),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_type_range)).
% 3.12/3.33  cnf(c13,plain,iext(uri_rdfs_range,uri_rdf_type,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_type_range])).
% 3.12/3.33  cnf(c306,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X246)|icext(X246,uri_rdf_type),inference(resolution,[status(thm)],[c80, c13])).
% 3.12/3.33  cnf(c305,plain,~iext(uri_rdfs_domain,uri_owl_propertyChainAxiom,X245)|icext(X245,uri_owl_sameAs),inference(resolution,[status(thm)],[c80, c2])).
% 3.12/3.33  fof(rdfs_value_range,axiom,iext(uri_rdfs_range,uri_rdf_value,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_value_range)).
% 3.12/3.33  cnf(c11,plain,iext(uri_rdfs_range,uri_rdf_value,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_value_range])).
% 3.12/3.33  cnf(c304,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X244)|icext(X244,uri_rdf_value),inference(resolution,[status(thm)],[c80, c11])).
% 3.12/3.33  cnf(c302,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X242)|icext(X242,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c80, c87])).
% 3.12/3.33  fof(rdfs_container_n_range_001,axiom,iext(uri_rdfs_range,uri_rdf__1,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_range_001)).
% 3.12/3.33  cnf(c94,plain,iext(uri_rdfs_range,uri_rdf__1,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_range_001])).
% 3.12/3.33  cnf(c301,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X241)|icext(X241,uri_rdf__1),inference(resolution,[status(thm)],[c80, c94])).
% 3.12/3.33  cnf(c6,plain,iext(uri_rdf_rest,skolem0002,uri_rdf_nil),inference(split_conjunct,[status(thm)],[c1])).
% 3.12/3.33  cnf(c300,plain,~iext(uri_rdfs_domain,uri_rdf_rest,X240)|icext(X240,skolem0002),inference(resolution,[status(thm)],[c80, c6])).
% 3.12/3.33  fof(rdfs_container_n_domain_001,axiom,iext(uri_rdfs_domain,uri_rdf__1,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_domain_001)).
% 3.12/3.33  cnf(c97,plain,iext(uri_rdfs_domain,uri_rdf__1,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_001])).
% 3.12/3.33  cnf(c299,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X239)|icext(X239,uri_rdf__1),inference(resolution,[status(thm)],[c80, c97])).
% 3.12/3.33  cnf(c298,plain,~iext(uri_rdfs_domain,uri_owl_inverseOf,X238)|icext(X238,skolem0003),inference(resolution,[status(thm)],[c80, c7])).
% 3.12/3.33  cnf(c296,plain,~iext(uri_rdfs_domain,uri_rdf_rest,X236)|icext(X236,skolem0001),inference(resolution,[status(thm)],[c80, c4])).
% 3.12/3.33  fof(rdfs_container_member_range,axiom,iext(uri_rdfs_range,uri_rdfs_member,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_member_range)).
% 3.12/3.33  cnf(c98,plain,iext(uri_rdfs_range,uri_rdfs_member,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_member_range])).
% 3.12/3.33  cnf(c295,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X235)|icext(X235,uri_rdfs_member),inference(resolution,[status(thm)],[c80, c98])).
% 3.12/3.33  cnf(c294,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X234)|icext(X234,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c80, c82])).
% 3.12/3.33  cnf(c293,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X233)|icext(X233,uri_rdfs_domain),inference(resolution,[status(thm)],[c80, c75])).
% 3.12/3.33  cnf(c5,plain,iext(uri_rdf_first,skolem0002,skolem0003),inference(split_conjunct,[status(thm)],[c1])).
% 3.12/3.33  cnf(c292,plain,~iext(uri_rdfs_domain,uri_rdf_first,X232)|icext(X232,skolem0002),inference(resolution,[status(thm)],[c80, c5])).
% 3.12/3.33  fof(rdfs_container_n_range_002,axiom,iext(uri_rdfs_range,uri_rdf__2,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_range_002)).
% 3.12/3.33  cnf(c93,plain,iext(uri_rdfs_range,uri_rdf__2,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_range_002])).
% 3.12/3.33  cnf(c290,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X230)|icext(X230,uri_rdf__2),inference(resolution,[status(thm)],[c80, c93])).
% 3.12/3.33  fof(rdfs_reification_predicate_domain,axiom,iext(uri_rdfs_domain,uri_rdf_predicate,uri_rdfs_Statement),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_reification_predicate_domain)).
% 3.12/3.33  cnf(c48,plain,iext(uri_rdfs_domain,uri_rdf_predicate,uri_rdfs_Statement),inference(split_conjunct,[status(thm)],[rdfs_reification_predicate_domain])).
% 3.12/3.33  cnf(c288,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X228)|icext(X228,uri_rdf_predicate),inference(resolution,[status(thm)],[c80, c48])).
% 3.12/3.33  cnf(c287,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X227)|icext(X227,uri_rdf_subject),inference(resolution,[status(thm)],[c80, c46])).
% 3.12/3.33  cnf(c285,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X225)|icext(X225,uri_rdfs_domain),inference(factor,[status(thm)],[c80])).
% 3.12/3.33  cnf(c276,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X218)|icext(X218,uri_rdf_Property),inference(resolution,[status(thm)],[c54, c100])).
% 3.12/3.33  cnf(c413,plain,~iext(uri_rdfs_domain,uri_rdf_type,X215)|icext(X215,X216),inference(resolution,[status(thm)],[c400, c80])).
% 3.12/3.33  fof(rdfs_property_type,axiom,iext(uri_rdf_type,uri_rdf_Property,uri_rdfs_Class),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_property_type)).
% 3.12/3.33  cnf(c56,plain,iext(uri_rdf_type,uri_rdf_Property,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_property_type])).
% 3.12/3.33  cnf(c275,plain,~iext(uri_rdfs_range,uri_rdf_type,X213)|icext(X213,uri_rdfs_Class),inference(resolution,[status(thm)],[c54, c56])).
% 3.12/3.33  cnf(c272,plain,~iext(uri_rdfs_range,uri_rdfs_range,X196)|icext(X196,uri_rdf_Property),inference(resolution,[status(thm)],[c54, c21])).
% 3.12/3.33  cnf(c43,plain,~iext(uri_rdfs_subClassOf,X79,X78)|~icext(X79,X77)|icext(X78,X77),inference(split_conjunct,[status(thm)],[c40])).
% 3.12/3.33  cnf(c335,plain,~icext(uri_rdf_Alt,X186)|icext(uri_rdfs_Container,X186),inference(resolution,[status(thm)],[c105, c43])).
% 3.12/3.33  cnf(c269,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X184)|icext(X184,uri_rdfs_Class),inference(resolution,[status(thm)],[c54, c44])).
% 3.12/3.33  cnf(c264,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X179)|icext(X179,uri_rdfs_Container),inference(resolution,[status(thm)],[c54, c88])).
% 3.12/3.33  cnf(c261,plain,~iext(uri_rdfs_range,uri_owl_propertyChainAxiom,X176)|icext(X176,skolem0001),inference(resolution,[status(thm)],[c54, c2])).
% 3.12/3.33  fof(rdfs_dat_xmlliteral_type,axiom,iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Datatype),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_dat_xmlliteral_type)).
% 3.12/3.33  cnf(c86,plain,iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Datatype),inference(split_conjunct,[status(thm)],[rdfs_dat_xmlliteral_type])).
% 3.12/3.33  cnf(c259,plain,~iext(uri_rdfs_range,uri_rdf_type,X174)|icext(X174,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c54, c86])).
% 3.12/3.33  cnf(c258,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X173)|icext(X173,uri_rdfs_Literal),inference(resolution,[status(thm)],[c54, c87])).
% 3.12/3.33  cnf(c256,plain,~iext(uri_rdfs_range,uri_rdf_rest,X171)|icext(X171,uri_rdf_nil),inference(resolution,[status(thm)],[c54, c6])).
% 3.12/3.33  cnf(c255,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X170)|icext(X170,uri_rdfs_Resource),inference(resolution,[status(thm)],[c54, c97])).
% 3.12/3.33  cnf(c1069,plain,icext(uri_rdf_Property,uri_rdfs_member),inference(resolution,[status(thm)],[c766, c117])).
% 3.12/3.33  cnf(c254,plain,~iext(uri_rdfs_range,uri_owl_inverseOf,X169)|icext(X169,uri_ex_p),inference(resolution,[status(thm)],[c54, c7])).
% 3.12/3.33  fof(rdfs_domain_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_domain_domain)).
% 3.12/3.33  cnf(c81,plain,iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_domain_domain])).
% 3.12/3.33  cnf(c253,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X168)|icext(X168,uri_rdf_Property),inference(resolution,[status(thm)],[c54, c81])).
% 3.12/3.33  cnf(c1037,plain,icext(uri_rdf_Property,uri_owl_propertyChainAxiom),inference(resolution,[status(thm)],[c577, c117])).
% 3.12/3.33  cnf(c250,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X165)|icext(X165,uri_rdfs_Class),inference(resolution,[status(thm)],[c54, c82])).
% 3.12/3.33  cnf(c249,plain,~iext(uri_rdfs_range,uri_rdfs_range,X164)|icext(X164,uri_rdfs_Class),inference(resolution,[status(thm)],[c54, c75])).
% 3.12/3.33  cnf(c1020,plain,icext(uri_rdf_Property,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c575, c117])).
% 3.12/3.33  cnf(c248,plain,~iext(uri_rdfs_range,uri_rdf_first,X163)|icext(X163,skolem0003),inference(resolution,[status(thm)],[c54, c5])).
% 3.12/3.33  cnf(c247,plain,~iext(uri_rdfs_range,uri_rdf_type,X162)|icext(X162,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c54, c91])).
% 3.12/3.33  cnf(c1004,plain,icext(uri_rdf_Property,uri_owl_inverseOf),inference(resolution,[status(thm)],[c573, c117])).
% 3.12/3.33  cnf(c245,plain,~iext(uri_rdfs_range,uri_rdf_first,X160)|icext(X160,uri_ex_p),inference(resolution,[status(thm)],[c54, c3])).
% 3.12/3.33  cnf(c984,plain,icext(uri_rdf_Property,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c571, c117])).
% 3.12/3.33  cnf(c950,plain,icext(uri_rdf_Property,uri_rdfs_domain),inference(resolution,[status(thm)],[c569, c117])).
% 3.12/3.33  cnf(c242,plain,~iext(uri_rdfs_range,uri_rdfs_range,X157)|icext(X157,uri_rdfs_Resource),inference(resolution,[status(thm)],[c54, c47])).
% 3.12/3.33  cnf(c241,plain,~iext(uri_rdfs_range,uri_rdfs_range,X156)|icext(X156,X156),inference(factor,[status(thm)],[c54])).
% 3.12/3.33  cnf(c923,plain,icext(uri_rdf_Property,uri_rdfs_range),inference(resolution,[status(thm)],[c567, c117])).
% 3.12/3.33  cnf(c237,plain,~icext(uri_rdf_Bag,X155)|icext(uri_rdfs_Container,X155),inference(resolution,[status(thm)],[c43, c104])).
% 3.12/3.33  cnf(c236,plain,~icext(uri_rdfs_ContainerMembershipProperty,X154)|icext(uri_rdf_Property,X154),inference(resolution,[status(thm)],[c43, c100])).
% 3.12/3.33  cnf(c235,plain,~icext(uri_rdfs_Seq,X153)|icext(uri_rdfs_Container,X153),inference(resolution,[status(thm)],[c43, c88])).
% 3.12/3.33  cnf(c234,plain,~icext(uri_rdf_XMLLiteral,X152)|icext(uri_rdfs_Literal,X152),inference(resolution,[status(thm)],[c43, c87])).
% 3.12/3.33  cnf(c233,plain,~icext(uri_rdfs_Datatype,X151)|icext(uri_rdfs_Class,X151),inference(resolution,[status(thm)],[c43, c82])).
% 3.12/3.33  cnf(c204,plain,~iext(uri_rdfs_subClassOf,X150,uri_rdf_Bag)|iext(uri_rdfs_subClassOf,X150,uri_rdfs_Container),inference(resolution,[status(thm)],[c104, c32])).
% 3.12/3.33  cnf(c203,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X149)|iext(X149,uri_rdf_Bag,uri_rdfs_Container),inference(resolution,[status(thm)],[c104, c28])).
% 3.12/3.33  cnf(c202,plain,~iext(uri_rdfs_subClassOf,X148,uri_rdfs_ContainerMembershipProperty)|iext(uri_rdfs_subClassOf,X148,uri_rdf_Property),inference(resolution,[status(thm)],[c100, c32])).
% 3.12/3.33  cnf(c871,plain,icext(uri_rdf_Property,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c454, c117])).
% 3.12/3.33  cnf(c201,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X147)|iext(X147,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),inference(resolution,[status(thm)],[c100, c28])).
% 3.12/3.33  cnf(c864,plain,icext(uri_rdf_Property,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c451, c117])).
% 3.12/3.33  cnf(c200,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X146)|iext(X146,uri_rdfs_member,uri_rdfs_Resource),inference(resolution,[status(thm)],[c99, c28])).
% 3.12/3.33  cnf(c199,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X145)|iext(X145,uri_rdfs_member,uri_rdfs_Resource),inference(resolution,[status(thm)],[c98, c28])).
% 3.12/3.33  cnf(c198,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X144)|iext(X144,uri_rdf__1,uri_rdfs_Resource),inference(resolution,[status(thm)],[c97, c28])).
% 3.12/3.33  cnf(c197,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X143)|iext(X143,uri_rdf__2,uri_rdfs_Resource),inference(resolution,[status(thm)],[c96, c28])).
% 3.12/3.33  cnf(c196,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X142)|iext(X142,uri_rdf__3,uri_rdfs_Resource),inference(resolution,[status(thm)],[c95, c28])).
% 3.12/3.33  cnf(c195,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X141)|iext(X141,uri_rdf__1,uri_rdfs_Resource),inference(resolution,[status(thm)],[c94, c28])).
% 3.12/3.33  cnf(c194,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X140)|iext(X140,uri_rdf__2,uri_rdfs_Resource),inference(resolution,[status(thm)],[c93, c28])).
% 3.12/3.33  cnf(c193,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X139)|iext(X139,uri_rdf__3,uri_rdfs_Resource),inference(resolution,[status(thm)],[c92, c28])).
% 3.12/3.33  cnf(c192,plain,~iext(uri_rdfs_subClassOf,X138,uri_rdfs_Seq)|iext(uri_rdfs_subClassOf,X138,uri_rdfs_Container),inference(resolution,[status(thm)],[c32, c88])).
% 3.12/3.33  cnf(c191,plain,~iext(uri_rdfs_subClassOf,X137,uri_rdf_XMLLiteral)|iext(uri_rdfs_subClassOf,X137,uri_rdfs_Literal),inference(resolution,[status(thm)],[c32, c87])).
% 3.12/3.33  cnf(c190,plain,~iext(uri_rdfs_subClassOf,X136,uri_rdfs_Datatype)|iext(uri_rdfs_subClassOf,X136,uri_rdfs_Class),inference(resolution,[status(thm)],[c32, c82])).
% 3.12/3.33  cnf(c188,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X134)|iext(X134,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c91, c28])).
% 3.12/3.33  cnf(c187,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X133)|iext(X133,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c90, c28])).
% 3.12/3.33  cnf(c186,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X132)|iext(X132,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c89, c28])).
% 3.12/3.33  cnf(c185,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X131)|iext(X131,uri_rdfs_Seq,uri_rdfs_Container),inference(resolution,[status(thm)],[c88, c28])).
% 3.12/3.33  cnf(c184,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X130)|iext(X130,uri_rdf_XMLLiteral,uri_rdfs_Literal),inference(resolution,[status(thm)],[c87, c28])).
% 3.12/3.33  cnf(c183,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X129)|iext(X129,uri_rdf_subject,uri_rdfs_Resource),inference(resolution,[status(thm)],[c28, c45])).
% 3.12/3.33  cnf(c182,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X128)|iext(X128,uri_rdfs_range,uri_rdf_Property),inference(resolution,[status(thm)],[c28, c55])).
% 3.12/3.33  cnf(c181,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X127)|iext(X127,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c28, c29])).
% 3.12/3.33  cnf(c180,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X126)|iext(X126,uri_rdf_type,uri_rdfs_Resource),inference(resolution,[status(thm)],[c28, c14])).
% 3.12/3.33  cnf(c179,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X125)|iext(X125,uri_rdf_Property,uri_rdfs_Class),inference(resolution,[status(thm)],[c28, c56])).
% 3.12/3.33  cnf(c178,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X124)|iext(X124,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c28, c21])).
% 3.12/3.33  cnf(c177,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X123)|iext(X123,uri_rdf_object,uri_rdfs_Statement),inference(resolution,[status(thm)],[c28, c50])).
% 3.12/3.33  cnf(c176,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X122)|iext(X122,uri_rdfs_subClassOf,uri_rdfs_Class),inference(resolution,[status(thm)],[c28, c44])).
% 3.12/3.33  cnf(c175,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X121)|iext(X121,uri_rdf_value,uri_rdfs_Resource),inference(resolution,[status(thm)],[c28, c12])).
% 3.12/3.33  cnf(c174,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X120)|iext(X120,uri_rdfs_range,uri_rdfs_Class),inference(resolution,[status(thm)],[c28, c51])).
% 3.12/3.33  cnf(c173,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X119)|iext(X119,uri_rdfs_subClassOf,uri_rdfs_Class),inference(resolution,[status(thm)],[c28, c36])).
% 3.12/3.33  cnf(c172,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X118)|iext(X118,uri_rdf_type,uri_rdfs_Class),inference(resolution,[status(thm)],[c28, c13])).
% 3.12/3.33  cnf(c171,plain,~iext(uri_rdfs_subPropertyOf,uri_owl_propertyChainAxiom,X117)|iext(X117,uri_owl_sameAs,skolem0001),inference(resolution,[status(thm)],[c28, c2])).
% 3.12/3.33  cnf(c170,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X116)|iext(X116,uri_rdf_value,uri_rdfs_Resource),inference(resolution,[status(thm)],[c28, c11])).
% 3.12/3.33  cnf(c169,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X115)|iext(X115,uri_rdf_XMLLiteral,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c28, c86])).
% 3.12/3.33  cnf(c497,plain,icext(uri_rdf_Property,uri_rdf_first),inference(resolution,[status(thm)],[c144, c117])).
% 3.12/3.33  cnf(c168,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X114)|iext(X114,skolem0002,uri_rdf_nil),inference(resolution,[status(thm)],[c28, c6])).
% 3.12/3.33  cnf(c167,plain,~iext(uri_rdfs_subPropertyOf,uri_owl_inverseOf,X113)|iext(X113,skolem0003,uri_ex_p),inference(resolution,[status(thm)],[c28, c7])).
% 3.12/3.33  cnf(c166,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X112)|iext(X112,uri_rdfs_domain,uri_rdf_Property),inference(resolution,[status(thm)],[c28, c81])).
% 3.12/3.33  cnf(c165,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X111)|iext(X111,skolem0001,skolem0002),inference(resolution,[status(thm)],[c28, c4])).
% 3.12/3.33  cnf(c164,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X110)|iext(X110,uri_rdfs_Datatype,uri_rdfs_Class),inference(resolution,[status(thm)],[c28, c82])).
% 3.12/3.33  cnf(c163,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X109)|iext(X109,uri_rdfs_domain,uri_rdfs_Class),inference(resolution,[status(thm)],[c28, c75])).
% 3.12/3.33  cnf(c162,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_first,X108)|iext(X108,skolem0002,skolem0003),inference(resolution,[status(thm)],[c28, c5])).
% 3.12/3.33  cnf(c161,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_first,X107)|iext(X107,skolem0001,uri_ex_p),inference(resolution,[status(thm)],[c28, c3])).
% 3.12/3.33  cnf(c160,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X106)|iext(X106,uri_rdf_predicate,uri_rdfs_Statement),inference(resolution,[status(thm)],[c28, c48])).
% 3.12/3.33  cnf(c159,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X105)|iext(X105,uri_rdf_subject,uri_rdfs_Statement),inference(resolution,[status(thm)],[c28, c46])).
% 3.12/3.33  cnf(c158,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X104)|iext(X104,uri_rdf_predicate,uri_rdfs_Resource),inference(resolution,[status(thm)],[c28, c47])).
% 3.12/3.33  cnf(c157,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X103)|iext(X103,uri_rdfs_subPropertyOf,X103),inference(factor,[status(thm)],[c28])).
% 3.12/3.33  cnf(c488,plain,icext(uri_rdf_List,uri_rdf_nil),inference(resolution,[status(thm)],[c143, c117])).
% 3.12/3.33  cnf(c484,plain,icext(uri_rdf_Property,uri_rdf_rest),inference(resolution,[status(thm)],[c142, c117])).
% 3.12/3.33  cnf(c473,plain,icext(uri_rdf_Property,uri_rdf__1),inference(resolution,[status(thm)],[c141, c117])).
% 3.12/3.33  cnf(c468,plain,icext(uri_rdf_Property,uri_rdf__2),inference(resolution,[status(thm)],[c140, c117])).
% 3.12/3.33  cnf(c460,plain,icext(uri_rdf_Property,uri_rdf__3),inference(resolution,[status(thm)],[c139, c117])).
% 3.12/3.33  cnf(c447,plain,icext(uri_rdf_Property,uri_rdf_object),inference(resolution,[status(thm)],[c138, c117])).
% 3.12/3.33  cnf(c435,plain,icext(uri_rdf_Property,uri_rdf_value),inference(resolution,[status(thm)],[c137, c117])).
% 3.12/3.33  cnf(c430,plain,icext(uri_rdf_Property,uri_rdf_subject),inference(resolution,[status(thm)],[c136, c117])).
% 3.12/3.33  cnf(c425,plain,icext(uri_rdf_Property,uri_rdf_type),inference(resolution,[status(thm)],[c128, c117])).
% 3.12/3.33  cnf(c390,plain,icext(uri_rdfs_Datatype,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c117, c86])).
% 3.12/3.33  cnf(c231,plain,icext(uri_rdfs_Class,uri_rdf_Property),inference(resolution,[status(thm)],[c223, c73])).
% 3.12/3.33  fof(rdfs_datatype_instsub_literal,axiom,(![D]:(icext(uri_rdfs_Datatype,D)=>iext(uri_rdfs_subClassOf,D,uri_rdfs_Literal))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_datatype_instsub_literal)).
% 3.12/3.33  fof(c83,plain,(![D]:(~icext(uri_rdfs_Datatype,D)|iext(uri_rdfs_subClassOf,D,uri_rdfs_Literal))),inference(fof_nnf,[status(thm)],[rdfs_datatype_instsub_literal])).
% 3.12/3.33  fof(c84,plain,(![X34]:(~icext(uri_rdfs_Datatype,X34)|iext(uri_rdfs_subClassOf,X34,uri_rdfs_Literal))),inference(variable_rename,[status(thm)],[c83])).
% 3.12/3.33  cnf(c85,plain,~icext(uri_rdfs_Datatype,X88)|iext(uri_rdfs_subClassOf,X88,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[c84])).
% 3.12/3.33  fof(rdfs_lv_def,axiom,(![X]:(lv(X)<=>icext(uri_rdfs_Literal,X))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_lv_def)).
% 3.12/3.33  fof(c57,plain,(![X]:((~lv(X)|icext(uri_rdfs_Literal,X))&(~icext(uri_rdfs_Literal,X)|lv(X)))),inference(fof_nnf,[status(thm)],[rdfs_lv_def])).
% 3.12/3.33  fof(c58,plain,((![X]:(~lv(X)|icext(uri_rdfs_Literal,X)))&(![X]:(~icext(uri_rdfs_Literal,X)|lv(X)))),inference(shift_quantors,[status(thm)],[c57])).
% 3.12/3.33  fof(c60,plain,(![X24]:(![X25]:((~lv(X24)|icext(uri_rdfs_Literal,X24))&(~icext(uri_rdfs_Literal,X25)|lv(X25))))),inference(shift_quantors,[status(thm)],[fof(c59,plain,((![X24]:(~lv(X24)|icext(uri_rdfs_Literal,X24)))&(![X25]:(~icext(uri_rdfs_Literal,X25)|lv(X25)))),inference(variable_rename,[status(thm)],[c58])).])).
% 3.12/3.33  cnf(c62,plain,~icext(uri_rdfs_Literal,X57)|lv(X57),inference(split_conjunct,[status(thm)],[c60])).
% 3.12/3.33  cnf(c61,plain,~lv(X54)|icext(uri_rdfs_Literal,X54),inference(split_conjunct,[status(thm)],[c60])).
% 3.12/3.33  fof(testcase_conclusion_fullish_027_Inferred_Property_Characteristics_II,conjecture,iext(uri_rdf_type,uri_ex_p,uri_owl_InverseFunctionalProperty),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', testcase_conclusion_fullish_027_Inferred_Property_Characteristics_II)).
% 3.12/3.33  fof(c8,negated_conjecture,(~iext(uri_rdf_type,uri_ex_p,uri_owl_InverseFunctionalProperty)),inference(assume_negation,[status(cth)],[testcase_conclusion_fullish_027_Inferred_Property_Characteristics_II])).
% 3.12/3.33  fof(c9,negated_conjecture,~iext(uri_rdf_type,uri_ex_p,uri_owl_InverseFunctionalProperty),inference(fof_simplification,[status(thm)],[c8])).
% 3.12/3.33  cnf(c10,negated_conjecture,~iext(uri_rdf_type,uri_ex_p,uri_owl_InverseFunctionalProperty),inference(split_conjunct,[status(thm)],[c9])).
% 3.12/3.33  % SZS output end Saturation
% 3.12/3.33  
% 3.12/3.33  % Initial clauses    : 96
% 3.12/3.33  % Processed clauses  : 549
% 3.12/3.33  % Factors computed   : 5
% 3.12/3.33  % Resolvents computed: 1272
% 3.12/3.33  % Tautologies deleted: 49
% 3.12/3.33  % Forward subsumed   : 775
% 3.12/3.33  % Backward subsumed  : 1
% 3.12/3.33  % -------- CPU Time ---------
% 3.12/3.33  % User time          : 2.956 s
% 3.12/3.33  % System time        : 0.015 s
% 3.12/3.33  % Total time         : 2.971 s
%------------------------------------------------------------------------------