PyRes---1.5.CSA-Sat.s

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

% Computer : n011.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:47 EDT 2024

% Result   : CounterSatisfiable 3.46s 3.64s
% Output   : Saturation 3.46s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13  % Problem  : SWB010+4 : TPTP v8.1.2. Released v5.2.0.
% 0.12/0.13  % Command  : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35  % Computer : n011.cluster.edu
% 0.13/0.35  % Model    : x86_64 x86_64
% 0.13/0.35  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35  % Memory   : 8042.1875MB
% 0.13/0.35  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35  % CPULimit : 300
% 0.13/0.35  % WCLimit  : 300
% 0.13/0.35  % DateTime : Wed May  8 22:09:23 EDT 2024
% 0.13/0.35  % CPUTime  : 
% 3.46/3.64  % Version:  1.5
% 3.46/3.64  % SZS status CounterSatisfiable
% 3.46/3.64  % SZS output start Saturation
% 3.46/3.64  fof(rdfs_subpropertyof_main,axiom,(![P]:(![Q]:(iext(uri_rdfs_subPropertyOf,P,Q)=>((ip(P)&ip(Q))&(![X]:(![Y]:(iext(P,X,Y)=>iext(Q,X,Y)))))))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_subpropertyof_main)).
% 3.46/3.64  fof(c25,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.46/3.64  fof(c27,plain,(![X11]:(![X12]:(![X13]:(![X14]:(~iext(uri_rdfs_subPropertyOf,X11,X12)|((ip(X11)&ip(X12))&(~iext(X11,X13,X14)|iext(X12,X13,X14)))))))),inference(shift_quantors,[status(thm)],[fof(c26,plain,(![X11]:(![X12]:(~iext(uri_rdfs_subPropertyOf,X11,X12)|((ip(X11)&ip(X12))&(![X13]:(![X14]:(~iext(X11,X13,X14)|iext(X12,X13,X14)))))))),inference(variable_rename,[status(thm)],[c25])).])).
% 3.46/3.64  fof(c28,plain,(![X11]:(![X12]:(![X13]:(![X14]:(((~iext(uri_rdfs_subPropertyOf,X11,X12)|ip(X11))&(~iext(uri_rdfs_subPropertyOf,X11,X12)|ip(X12)))&(~iext(uri_rdfs_subPropertyOf,X11,X12)|(~iext(X11,X13,X14)|iext(X12,X13,X14)))))))),inference(distribute,[status(thm)],[c27])).
% 3.46/3.64  cnf(c31,plain,~iext(uri_rdfs_subPropertyOf,X69,X68)|~iext(X69,X70,X71)|iext(X68,X70,X71),inference(split_conjunct,[status(thm)],[c28])).
% 3.46/3.64  fof(rdfs_subpropertyof_reflex,axiom,(![P]:(ip(P)=>iext(uri_rdfs_subPropertyOf,P,P))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_subpropertyof_reflex)).
% 3.46/3.64  fof(c21,plain,(![P]:(~ip(P)|iext(uri_rdfs_subPropertyOf,P,P))),inference(fof_nnf,[status(thm)],[rdfs_subpropertyof_reflex])).
% 3.46/3.64  fof(c22,plain,(![X10]:(~ip(X10)|iext(uri_rdfs_subPropertyOf,X10,X10))),inference(variable_rename,[status(thm)],[c21])).
% 3.46/3.64  cnf(c23,plain,~ip(X56)|iext(uri_rdfs_subPropertyOf,X56,X56),inference(split_conjunct,[status(thm)],[c22])).
% 3.46/3.64  fof(rdf_type_ip,axiom,(![P]:(iext(uri_rdf_type,P,uri_rdf_Property)<=>ip(P))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdf_type_ip)).
% 3.46/3.64  fof(c133,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.46/3.64  fof(c134,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)],[c133])).
% 3.46/3.64  fof(c136,plain,(![X43]:(![X44]:((~iext(uri_rdf_type,X43,uri_rdf_Property)|ip(X43))&(~ip(X44)|iext(uri_rdf_type,X44,uri_rdf_Property))))),inference(shift_quantors,[status(thm)],[fof(c135,plain,((![X43]:(~iext(uri_rdf_type,X43,uri_rdf_Property)|ip(X43)))&(![X44]:(~ip(X44)|iext(uri_rdf_type,X44,uri_rdf_Property)))),inference(variable_rename,[status(thm)],[c134])).])).
% 3.46/3.64  cnf(c137,plain,~iext(uri_rdf_type,X100,uri_rdf_Property)|ip(X100),inference(split_conjunct,[status(thm)],[c136])).
% 3.46/3.64  fof(rdfs_cext_def,axiom,(![X]:(![C]:(iext(uri_rdf_type,X,C)<=>icext(C,X)))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_cext_def)).
% 3.46/3.64  fof(c116,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.46/3.64  fof(c117,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)],[c116])).
% 3.46/3.64  fof(c119,plain,(![X39]:(![X40]:(![X41]:(![X42]:((~iext(uri_rdf_type,X39,X40)|icext(X40,X39))&(~icext(X42,X41)|iext(uri_rdf_type,X41,X42))))))),inference(shift_quantors,[status(thm)],[fof(c118,plain,((![X39]:(![X40]:(~iext(uri_rdf_type,X39,X40)|icext(X40,X39))))&(![X41]:(![X42]:(~icext(X42,X41)|iext(uri_rdf_type,X41,X42))))),inference(variable_rename,[status(thm)],[c117])).])).
% 3.46/3.64  cnf(c121,plain,~icext(X96,X97)|iext(uri_rdf_type,X97,X96),inference(split_conjunct,[status(thm)],[c119])).
% 3.46/3.64  fof(rdfs_range_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_range,uri_rdf_Property),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_range_domain)).
% 3.46/3.64  cnf(c58,plain,iext(uri_rdfs_domain,uri_rdfs_range,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_range_domain])).
% 3.46/3.64  fof(rdfs_domain_main,axiom,(![P]:(![C]:(![X]:(![Y]:((iext(uri_rdfs_domain,P,C)&iext(P,X,Y))=>icext(C,X)))))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_domain_main)).
% 3.46/3.64  fof(c79,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.46/3.64  fof(c80,plain,(![P]:(![C]:(![X]:((~iext(uri_rdfs_domain,P,C)|(![Y]:~iext(P,X,Y)))|icext(C,X))))),inference(shift_quantors,[status(thm)],[c79])).
% 3.46/3.64  fof(c82,plain,(![X32]:(![X33]:(![X34]:(![X35]:((~iext(uri_rdfs_domain,X32,X33)|~iext(X32,X34,X35))|icext(X33,X34)))))),inference(shift_quantors,[status(thm)],[fof(c81,plain,(![X32]:(![X33]:(![X34]:((~iext(uri_rdfs_domain,X32,X33)|(![X35]:~iext(X32,X34,X35)))|icext(X33,X34))))),inference(variable_rename,[status(thm)],[c80])).])).
% 3.46/3.64  cnf(c83,plain,~iext(uri_rdfs_domain,X90,X89)|~iext(X90,X88,X87)|icext(X89,X88),inference(split_conjunct,[status(thm)],[c82])).
% 3.46/3.64  fof(rdfs_annotation_comment_range,axiom,iext(uri_rdfs_range,uri_rdfs_comment,uri_rdfs_Literal),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_comment_range)).
% 3.46/3.64  cnf(c129,plain,iext(uri_rdfs_range,uri_rdfs_comment,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[rdfs_annotation_comment_range])).
% 3.46/3.64  cnf(c430,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X319)|icext(X319,uri_rdfs_comment),inference(resolution,[status(thm)],[c129, c83])).
% 3.46/3.64  cnf(c1338,plain,icext(uri_rdf_Property,uri_rdfs_comment),inference(resolution,[status(thm)],[c430, c58])).
% 3.46/3.64  cnf(c1339,plain,iext(uri_rdf_type,uri_rdfs_comment,uri_rdf_Property),inference(resolution,[status(thm)],[c1338, c121])).
% 3.46/3.64  cnf(c1346,plain,ip(uri_rdfs_comment),inference(resolution,[status(thm)],[c1339, c137])).
% 3.46/3.64  cnf(c1347,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_comment,uri_rdfs_comment),inference(resolution,[status(thm)],[c1346, c23])).
% 3.46/3.64  cnf(c1351,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X666)|iext(X666,uri_rdfs_comment,uri_rdfs_comment),inference(resolution,[status(thm)],[c1347, c31])).
% 3.46/3.64  cnf(c1342,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X664)|iext(X664,uri_rdfs_comment,uri_rdf_Property),inference(resolution,[status(thm)],[c1339, c31])).
% 3.46/3.64  fof(rdfs_annotation_label_range,axiom,iext(uri_rdfs_range,uri_rdfs_label,uri_rdfs_Literal),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_label_range)).
% 3.46/3.64  cnf(c124,plain,iext(uri_rdfs_range,uri_rdfs_label,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[rdfs_annotation_label_range])).
% 3.46/3.64  cnf(c378,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X303)|icext(X303,uri_rdfs_label),inference(resolution,[status(thm)],[c124, c83])).
% 3.46/3.64  cnf(c1309,plain,icext(uri_rdf_Property,uri_rdfs_label),inference(resolution,[status(thm)],[c378, c58])).
% 3.46/3.64  cnf(c1310,plain,iext(uri_rdf_type,uri_rdfs_label,uri_rdf_Property),inference(resolution,[status(thm)],[c1309, c121])).
% 3.46/3.64  cnf(c1316,plain,ip(uri_rdfs_label),inference(resolution,[status(thm)],[c1310, c137])).
% 3.46/3.64  cnf(c1318,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_label,uri_rdfs_label),inference(resolution,[status(thm)],[c1316, c23])).
% 3.46/3.64  cnf(c1321,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X663)|iext(X663,uri_rdfs_label,uri_rdfs_label),inference(resolution,[status(thm)],[c1318, c31])).
% 3.46/3.64  cnf(c1312,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X661)|iext(X661,uri_rdfs_label,uri_rdf_Property),inference(resolution,[status(thm)],[c1310, c31])).
% 3.46/3.64  fof(rdfs_subclassof_reflex,axiom,(![C]:(ic(C)=>iext(uri_rdfs_subClassOf,C,C))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_subclassof_reflex)).
% 3.46/3.64  fof(c36,plain,(![C]:(~ic(C)|iext(uri_rdfs_subClassOf,C,C))),inference(fof_nnf,[status(thm)],[rdfs_subclassof_reflex])).
% 3.46/3.64  fof(c37,plain,(![X18]:(~ic(X18)|iext(uri_rdfs_subClassOf,X18,X18))),inference(variable_rename,[status(thm)],[c36])).
% 3.46/3.64  cnf(c38,plain,~ic(X75)|iext(uri_rdfs_subClassOf,X75,X75),inference(split_conjunct,[status(thm)],[c37])).
% 3.46/3.64  fof(rdfs_ic_def,axiom,(![X]:(ic(X)<=>icext(uri_rdfs_Class,X))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_ic_def)).
% 3.46/3.64  fof(c72,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.46/3.64  fof(c73,plain,((![X]:(~ic(X)|icext(uri_rdfs_Class,X)))&(![X]:(~icext(uri_rdfs_Class,X)|ic(X)))),inference(shift_quantors,[status(thm)],[c72])).
% 3.46/3.64  fof(c75,plain,(![X30]:(![X31]:((~ic(X30)|icext(uri_rdfs_Class,X30))&(~icext(uri_rdfs_Class,X31)|ic(X31))))),inference(shift_quantors,[status(thm)],[fof(c74,plain,((![X30]:(~ic(X30)|icext(uri_rdfs_Class,X30)))&(![X31]:(~icext(uri_rdfs_Class,X31)|ic(X31)))),inference(variable_rename,[status(thm)],[c73])).])).
% 3.46/3.64  cnf(c77,plain,~icext(uri_rdfs_Class,X67)|ic(X67),inference(split_conjunct,[status(thm)],[c75])).
% 3.46/3.64  fof(rdfs_range_range,axiom,iext(uri_rdfs_range,uri_rdfs_range,uri_rdfs_Class),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_range_range)).
% 3.46/3.64  cnf(c54,plain,iext(uri_rdfs_range,uri_rdfs_range,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_range_range])).
% 3.46/3.64  fof(rdfs_range_main,axiom,(![P]:(![C]:(![X]:(![Y]:((iext(uri_rdfs_range,P,C)&iext(P,X,Y))=>icext(C,Y)))))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_range_main)).
% 3.46/3.64  fof(c55,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.46/3.64  fof(c56,plain,(![X22]:(![X23]:(![X24]:(![X25]:((~iext(uri_rdfs_range,X22,X23)|~iext(X22,X24,X25))|icext(X23,X25)))))),inference(variable_rename,[status(thm)],[c55])).
% 3.46/3.64  cnf(c57,plain,~iext(uri_rdfs_range,X86,X85)|~iext(X86,X84,X83)|icext(X85,X83),inference(split_conjunct,[status(thm)],[c56])).
% 3.46/3.64  fof(rdfs_collection_rest_range,axiom,iext(uri_rdfs_range,uri_rdf_rest,uri_rdf_List),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_collection_rest_range)).
% 3.46/3.64  cnf(c109,plain,iext(uri_rdfs_range,uri_rdf_rest,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdfs_collection_rest_range])).
% 3.46/3.64  cnf(c351,plain,~iext(uri_rdfs_range,uri_rdfs_range,X283)|icext(X283,uri_rdf_List),inference(resolution,[status(thm)],[c109, c57])).
% 3.46/3.64  cnf(c1269,plain,icext(uri_rdfs_Class,uri_rdf_List),inference(resolution,[status(thm)],[c351, c54])).
% 3.46/3.64  cnf(c1271,plain,ic(uri_rdf_List),inference(resolution,[status(thm)],[c1269, c77])).
% 3.46/3.64  cnf(c1273,plain,iext(uri_rdfs_subClassOf,uri_rdf_List,uri_rdf_List),inference(resolution,[status(thm)],[c1271, c38])).
% 3.46/3.64  cnf(c1290,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X659)|iext(X659,uri_rdf_List,uri_rdf_List),inference(resolution,[status(thm)],[c1273, c31])).
% 3.46/3.64  fof(rdfs_subclassof_trans,axiom,(![C]:(![D]:(![E]:((iext(uri_rdfs_subClassOf,C,D)&iext(uri_rdfs_subClassOf,D,E))=>iext(uri_rdfs_subClassOf,C,E))))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_subclassof_trans)).
% 3.46/3.64  fof(c33,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.46/3.64  fof(c34,plain,(![X15]:(![X16]:(![X17]:((~iext(uri_rdfs_subClassOf,X15,X16)|~iext(uri_rdfs_subClassOf,X16,X17))|iext(uri_rdfs_subClassOf,X15,X17))))),inference(variable_rename,[status(thm)],[c33])).
% 3.46/3.64  cnf(c35,plain,~iext(uri_rdfs_subClassOf,X73,X74)|~iext(uri_rdfs_subClassOf,X74,X72)|iext(uri_rdfs_subClassOf,X73,X72),inference(split_conjunct,[status(thm)],[c34])).
% 3.46/3.64  fof(rdfs_class_instsub_resource,axiom,(![C]:(ic(C)=>iext(uri_rdfs_subClassOf,C,uri_rdfs_Resource))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_class_instsub_resource)).
% 3.46/3.64  fof(c113,plain,(![C]:(~ic(C)|iext(uri_rdfs_subClassOf,C,uri_rdfs_Resource))),inference(fof_nnf,[status(thm)],[rdfs_class_instsub_resource])).
% 3.46/3.64  fof(c114,plain,(![X38]:(~ic(X38)|iext(uri_rdfs_subClassOf,X38,uri_rdfs_Resource))),inference(variable_rename,[status(thm)],[c113])).
% 3.46/3.64  cnf(c115,plain,~ic(X93)|iext(uri_rdfs_subClassOf,X93,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[c114])).
% 3.46/3.64  cnf(c1272,plain,iext(uri_rdfs_subClassOf,uri_rdf_List,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1271, c115])).
% 3.46/3.64  cnf(c1287,plain,~iext(uri_rdfs_subClassOf,X658,uri_rdf_List)|iext(uri_rdfs_subClassOf,X658,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1272, c35])).
% 3.46/3.64  cnf(c1281,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X657)|iext(X657,uri_rdf_List,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1272, c31])).
% 3.46/3.64  cnf(c1270,plain,iext(uri_rdf_type,uri_rdf_List,uri_rdfs_Class),inference(resolution,[status(thm)],[c1269, c121])).
% 3.46/3.64  cnf(c1277,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X656)|iext(X656,uri_rdf_List,uri_rdfs_Class),inference(resolution,[status(thm)],[c1270, c31])).
% 3.46/3.64  fof(rdfs_domain_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_Property),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_domain_domain)).
% 3.46/3.64  cnf(c84,plain,iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_domain_domain])).
% 3.46/3.64  fof(rdfs_reification_predicate_domain,axiom,iext(uri_rdfs_domain,uri_rdf_predicate,uri_rdfs_Statement),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_reification_predicate_domain)).
% 3.46/3.64  cnf(c51,plain,iext(uri_rdfs_domain,uri_rdf_predicate,uri_rdfs_Statement),inference(split_conjunct,[status(thm)],[rdfs_reification_predicate_domain])).
% 3.46/3.64  cnf(c306,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X256)|icext(X256,uri_rdf_predicate),inference(resolution,[status(thm)],[c83, c51])).
% 3.46/3.64  cnf(c1232,plain,icext(uri_rdf_Property,uri_rdf_predicate),inference(resolution,[status(thm)],[c306, c84])).
% 3.46/3.64  cnf(c1233,plain,iext(uri_rdf_type,uri_rdf_predicate,uri_rdf_Property),inference(resolution,[status(thm)],[c1232, c121])).
% 3.46/3.64  cnf(c1239,plain,ip(uri_rdf_predicate),inference(resolution,[status(thm)],[c1233, c137])).
% 3.46/3.64  cnf(c1240,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_predicate,uri_rdf_predicate),inference(resolution,[status(thm)],[c1239, c23])).
% 3.46/3.64  cnf(c1244,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X655)|iext(X655,uri_rdf_predicate,uri_rdf_predicate),inference(resolution,[status(thm)],[c1240, c31])).
% 3.46/3.64  cnf(c1235,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X653)|iext(X653,uri_rdf_predicate,uri_rdf_Property),inference(resolution,[status(thm)],[c1233, c31])).
% 3.46/3.64  fof(rdfs_collection_rest_domain,axiom,iext(uri_rdfs_domain,uri_rdf_rest,uri_rdf_List),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_collection_rest_domain)).
% 3.46/3.64  cnf(c110,plain,iext(uri_rdfs_domain,uri_rdf_rest,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdfs_collection_rest_domain])).
% 3.46/3.64  fof(testcase_premise_fullish_010_Negative_Property_Assertions,axiom,(?[BNODE_x1]:(?[BNODE_x2]:(?[BNODE_x3]:(?[BNODE_x4]:(((((((iext(uri_rdf_type,uri_ex_p,uri_owl_ObjectProperty)&iext(uri_rdf_type,uri_ex_s,BNODE_x1))&iext(uri_owl_onProperty,BNODE_x1,uri_ex_p))&iext(uri_owl_allValuesFrom,BNODE_x1,BNODE_x2))&iext(uri_owl_complementOf,BNODE_x2,BNODE_x3))&iext(uri_owl_oneOf,BNODE_x3,BNODE_x4))&iext(uri_rdf_first,BNODE_x4,uri_ex_o))&iext(uri_rdf_rest,BNODE_x4,uri_rdf_nil)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', testcase_premise_fullish_010_Negative_Property_Assertions)).
% 3.46/3.64  fof(c0,plain,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(((((((iext(uri_rdf_type,uri_ex_p,uri_owl_ObjectProperty)&iext(uri_rdf_type,uri_ex_s,X2))&iext(uri_owl_onProperty,X2,uri_ex_p))&iext(uri_owl_allValuesFrom,X2,X3))&iext(uri_owl_complementOf,X3,X4))&iext(uri_owl_oneOf,X4,X5))&iext(uri_rdf_first,X5,uri_ex_o))&iext(uri_rdf_rest,X5,uri_rdf_nil)))))),inference(variable_rename,[status(thm)],[testcase_premise_fullish_010_Negative_Property_Assertions])).
% 3.46/3.64  fof(c1,plain,(((((((iext(uri_rdf_type,uri_ex_p,uri_owl_ObjectProperty)&iext(uri_rdf_type,uri_ex_s,skolem0001))&iext(uri_owl_onProperty,skolem0001,uri_ex_p))&iext(uri_owl_allValuesFrom,skolem0001,skolem0002))&iext(uri_owl_complementOf,skolem0002,skolem0003))&iext(uri_owl_oneOf,skolem0003,skolem0004))&iext(uri_rdf_first,skolem0004,uri_ex_o))&iext(uri_rdf_rest,skolem0004,uri_rdf_nil)),inference(skolemize,[status(esa)],[c0])).
% 3.46/3.64  cnf(c9,plain,iext(uri_rdf_rest,skolem0004,uri_rdf_nil),inference(split_conjunct,[status(thm)],[c1])).
% 3.46/3.64  cnf(c305,plain,~iext(uri_rdfs_domain,uri_rdf_rest,X255)|icext(X255,skolem0004),inference(resolution,[status(thm)],[c83, c9])).
% 3.46/3.64  cnf(c1225,plain,icext(uri_rdf_List,skolem0004),inference(resolution,[status(thm)],[c305, c110])).
% 3.46/3.64  cnf(c1226,plain,iext(uri_rdf_type,skolem0004,uri_rdf_List),inference(resolution,[status(thm)],[c1225, c121])).
% 3.46/3.65  cnf(c1228,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X652)|iext(X652,skolem0004,uri_rdf_List),inference(resolution,[status(thm)],[c1226, c31])).
% 3.46/3.65  fof(rdfs_type_range,axiom,iext(uri_rdfs_range,uri_rdf_type,uri_rdfs_Class),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_type_range)).
% 3.46/3.65  cnf(c16,plain,iext(uri_rdfs_range,uri_rdf_type,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_type_range])).
% 3.46/3.65  cnf(c2,plain,iext(uri_rdf_type,uri_ex_p,uri_owl_ObjectProperty),inference(split_conjunct,[status(thm)],[c1])).
% 3.46/3.65  cnf(c261,plain,~iext(uri_rdfs_range,uri_rdf_type,X184)|icext(X184,uri_owl_ObjectProperty),inference(resolution,[status(thm)],[c57, c2])).
% 3.46/3.65  cnf(c1153,plain,icext(uri_rdfs_Class,uri_owl_ObjectProperty),inference(resolution,[status(thm)],[c261, c16])).
% 3.46/3.65  cnf(c1155,plain,ic(uri_owl_ObjectProperty),inference(resolution,[status(thm)],[c1153, c77])).
% 3.46/3.65  cnf(c1157,plain,iext(uri_rdfs_subClassOf,uri_owl_ObjectProperty,uri_owl_ObjectProperty),inference(resolution,[status(thm)],[c1155, c38])).
% 3.46/3.65  cnf(c1201,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X650)|iext(X650,uri_owl_ObjectProperty,uri_owl_ObjectProperty),inference(resolution,[status(thm)],[c1157, c31])).
% 3.46/3.65  cnf(c1156,plain,iext(uri_rdfs_subClassOf,uri_owl_ObjectProperty,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1155, c115])).
% 3.46/3.65  cnf(c1194,plain,~iext(uri_rdfs_subClassOf,X649,uri_owl_ObjectProperty)|iext(uri_rdfs_subClassOf,X649,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1156, c35])).
% 3.46/3.65  cnf(c1193,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X648)|iext(X648,uri_owl_ObjectProperty,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1156, c31])).
% 3.46/3.65  cnf(c1154,plain,iext(uri_rdf_type,uri_owl_ObjectProperty,uri_rdfs_Class),inference(resolution,[status(thm)],[c1153, c121])).
% 3.46/3.65  cnf(c1186,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X647)|iext(X647,uri_owl_ObjectProperty,uri_rdfs_Class),inference(resolution,[status(thm)],[c1154, c31])).
% 3.46/3.65  fof(rdfs_domain_range,axiom,iext(uri_rdfs_range,uri_rdfs_domain,uri_rdfs_Class),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_domain_range)).
% 3.46/3.65  cnf(c78,plain,iext(uri_rdfs_range,uri_rdfs_domain,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_domain_range])).
% 3.46/3.65  cnf(c254,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X177)|icext(X177,uri_rdfs_Statement),inference(resolution,[status(thm)],[c57, c51])).
% 3.46/3.65  cnf(c1123,plain,icext(uri_rdfs_Class,uri_rdfs_Statement),inference(resolution,[status(thm)],[c254, c78])).
% 3.46/3.65  cnf(c1126,plain,ic(uri_rdfs_Statement),inference(resolution,[status(thm)],[c1123, c77])).
% 3.46/3.65  cnf(c1128,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Statement,uri_rdfs_Statement),inference(resolution,[status(thm)],[c1126, c38])).
% 3.46/3.65  cnf(c1180,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X645)|iext(X645,uri_rdfs_Statement,uri_rdfs_Statement),inference(resolution,[status(thm)],[c1128, c31])).
% 3.46/3.65  cnf(c1127,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Statement,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1126, c115])).
% 3.46/3.65  cnf(c1173,plain,~iext(uri_rdfs_subClassOf,X644,uri_rdfs_Statement)|iext(uri_rdfs_subClassOf,X644,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1127, c35])).
% 3.46/3.65  cnf(c1172,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X643)|iext(X643,uri_rdfs_Statement,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1127, c31])).
% 3.46/3.65  cnf(c1125,plain,iext(uri_rdf_type,uri_rdfs_Statement,uri_rdfs_Class),inference(resolution,[status(thm)],[c1123, c121])).
% 3.46/3.65  cnf(c1165,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X642)|iext(X642,uri_rdfs_Statement,uri_rdfs_Class),inference(resolution,[status(thm)],[c1125, c31])).
% 3.46/3.65  cnf(c3,plain,iext(uri_rdf_type,uri_ex_s,skolem0001),inference(split_conjunct,[status(thm)],[c1])).
% 3.46/3.65  cnf(c236,plain,~iext(uri_rdfs_range,uri_rdf_type,X159)|icext(X159,skolem0001),inference(resolution,[status(thm)],[c57, c3])).
% 3.46/3.65  cnf(c940,plain,icext(uri_rdfs_Class,skolem0001),inference(resolution,[status(thm)],[c236, c16])).
% 3.46/3.65  cnf(c942,plain,ic(skolem0001),inference(resolution,[status(thm)],[c940, c77])).
% 3.46/3.65  cnf(c944,plain,iext(uri_rdfs_subClassOf,skolem0001,skolem0001),inference(resolution,[status(thm)],[c942, c38])).
% 3.46/3.65  cnf(c1150,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X640)|iext(X640,skolem0001,skolem0001),inference(resolution,[status(thm)],[c944, c31])).
% 3.46/3.65  cnf(c943,plain,iext(uri_rdfs_subClassOf,skolem0001,uri_rdfs_Resource),inference(resolution,[status(thm)],[c942, c115])).
% 3.46/3.65  cnf(c1143,plain,~iext(uri_rdfs_subClassOf,X639,skolem0001)|iext(uri_rdfs_subClassOf,X639,uri_rdfs_Resource),inference(resolution,[status(thm)],[c943, c35])).
% 3.46/3.65  cnf(c1142,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X638)|iext(X638,skolem0001,uri_rdfs_Resource),inference(resolution,[status(thm)],[c943, c31])).
% 3.46/3.65  cnf(c941,plain,iext(uri_rdf_type,skolem0001,uri_rdfs_Class),inference(resolution,[status(thm)],[c940, c121])).
% 3.46/3.65  cnf(c1135,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X637)|iext(X637,skolem0001,uri_rdfs_Class),inference(resolution,[status(thm)],[c941, c31])).
% 3.46/3.65  cnf(c138,plain,~ip(X101)|iext(uri_rdf_type,X101,uri_rdf_Property),inference(split_conjunct,[status(thm)],[c136])).
% 3.46/3.65  cnf(c30,plain,~iext(uri_rdfs_subPropertyOf,X64,X63)|ip(X63),inference(split_conjunct,[status(thm)],[c28])).
% 3.46/3.65  fof(rdfs_container_containermembershipproperty_instsub_member,axiom,(![P]:(icext(uri_rdfs_ContainerMembershipProperty,P)=>iext(uri_rdfs_subPropertyOf,P,uri_rdfs_member))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_containermembershipproperty_instsub_member)).
% 3.46/3.65  fof(c104,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.46/3.65  fof(c105,plain,(![X37]:(~icext(uri_rdfs_ContainerMembershipProperty,X37)|iext(uri_rdfs_subPropertyOf,X37,uri_rdfs_member))),inference(variable_rename,[status(thm)],[c104])).
% 3.46/3.65  cnf(c106,plain,~icext(uri_rdfs_ContainerMembershipProperty,X92)|iext(uri_rdfs_subPropertyOf,X92,uri_rdfs_member),inference(split_conjunct,[status(thm)],[c105])).
% 3.46/3.65  fof(rdfs_container_n_type_002,axiom,iext(uri_rdf_type,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_type_002)).
% 3.46/3.65  cnf(c93,plain,iext(uri_rdf_type,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),inference(split_conjunct,[status(thm)],[rdfs_container_n_type_002])).
% 3.46/3.65  cnf(c120,plain,~iext(uri_rdf_type,X94,X95)|icext(X95,X94),inference(split_conjunct,[status(thm)],[c119])).
% 3.46/3.65  cnf(c394,plain,icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__2),inference(resolution,[status(thm)],[c120, c93])).
% 3.46/3.65  cnf(c400,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__2,uri_rdfs_member),inference(resolution,[status(thm)],[c394, c106])).
% 3.46/3.65  cnf(c784,plain,ip(uri_rdfs_member),inference(resolution,[status(thm)],[c400, c30])).
% 3.46/3.65  cnf(c786,plain,iext(uri_rdf_type,uri_rdfs_member,uri_rdf_Property),inference(resolution,[status(thm)],[c784, c138])).
% 3.46/3.65  cnf(c1121,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X636)|iext(X636,uri_rdfs_member,uri_rdf_Property),inference(resolution,[status(thm)],[c786, c31])).
% 3.46/3.65  cnf(c785,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_member,uri_rdfs_member),inference(resolution,[status(thm)],[c784, c23])).
% 3.46/3.65  cnf(c1112,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X635)|iext(X635,uri_rdfs_member,uri_rdfs_member),inference(resolution,[status(thm)],[c785, c31])).
% 3.46/3.65  cnf(c76,plain,~ic(X66)|icext(uri_rdfs_Class,X66),inference(split_conjunct,[status(thm)],[c75])).
% 3.46/3.65  fof(rdfs_subclassof_main,axiom,(![C]:(![D]:(iext(uri_rdfs_subClassOf,C,D)=>((ic(C)&ic(D))&(![X]:(icext(C,X)=>icext(D,X))))))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_subclassof_main)).
% 3.46/3.65  fof(c40,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.46/3.65  fof(c42,plain,(![X19]:(![X20]:(![X21]:(~iext(uri_rdfs_subClassOf,X19,X20)|((ic(X19)&ic(X20))&(~icext(X19,X21)|icext(X20,X21))))))),inference(shift_quantors,[status(thm)],[fof(c41,plain,(![X19]:(![X20]:(~iext(uri_rdfs_subClassOf,X19,X20)|((ic(X19)&ic(X20))&(![X21]:(~icext(X19,X21)|icext(X20,X21))))))),inference(variable_rename,[status(thm)],[c40])).])).
% 3.46/3.65  fof(c43,plain,(![X19]:(![X20]:(![X21]:(((~iext(uri_rdfs_subClassOf,X19,X20)|ic(X19))&(~iext(uri_rdfs_subClassOf,X19,X20)|ic(X20)))&(~iext(uri_rdfs_subClassOf,X19,X20)|(~icext(X19,X21)|icext(X20,X21))))))),inference(distribute,[status(thm)],[c42])).
% 3.46/3.65  cnf(c45,plain,~iext(uri_rdfs_subClassOf,X79,X78)|ic(X78),inference(split_conjunct,[status(thm)],[c43])).
% 3.46/3.65  fof(rdfs_container_seq_sub,axiom,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Container),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_seq_sub)).
% 3.46/3.65  cnf(c91,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Container),inference(split_conjunct,[status(thm)],[rdfs_container_seq_sub])).
% 3.46/3.65  cnf(c44,plain,~iext(uri_rdfs_subClassOf,X77,X76)|ic(X77),inference(split_conjunct,[status(thm)],[c43])).
% 3.46/3.65  cnf(c208,plain,ic(uri_rdfs_Seq),inference(resolution,[status(thm)],[c44, c91])).
% 3.46/3.65  cnf(c368,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Resource),inference(resolution,[status(thm)],[c115, c208])).
% 3.46/3.65  cnf(c683,plain,ic(uri_rdfs_Resource),inference(resolution,[status(thm)],[c368, c45])).
% 3.46/3.65  cnf(c689,plain,icext(uri_rdfs_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c683, c76])).
% 3.46/3.65  cnf(c690,plain,iext(uri_rdf_type,uri_rdfs_Resource,uri_rdfs_Class),inference(resolution,[status(thm)],[c689, c121])).
% 3.46/3.65  cnf(c1106,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X633)|iext(X633,uri_rdfs_Resource,uri_rdfs_Class),inference(resolution,[status(thm)],[c690, c31])).
% 3.46/3.65  cnf(c687,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Resource,uri_rdfs_Resource),inference(resolution,[status(thm)],[c683, c115])).
% 3.46/3.65  cnf(c1100,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X631)|iext(X631,uri_rdfs_Resource,uri_rdfs_Resource),inference(resolution,[status(thm)],[c687, c31])).
% 3.46/3.65  fof(rdfs_annotation_isdefinedby_sub,axiom,iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_isdefinedby_sub)).
% 3.46/3.65  cnf(c126,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_sub])).
% 3.46/3.65  fof(simple_iext_property,axiom,(![S]:(![P]:(![O]:(iext(P,S,O)=>ip(P))))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', simple_iext_property)).
% 3.46/3.65  fof(c153,plain,(![S]:(![P]:(![O]:(~iext(P,S,O)|ip(P))))),inference(fof_nnf,[status(thm)],[simple_iext_property])).
% 3.46/3.65  fof(c154,plain,(![S]:(![P]:((![O]:~iext(P,S,O))|ip(P)))),inference(shift_quantors,[status(thm)],[c153])).
% 3.46/3.65  fof(c156,plain,(![X47]:(![X48]:(![X49]:(~iext(X48,X47,X49)|ip(X48))))),inference(shift_quantors,[status(thm)],[fof(c155,plain,(![X47]:(![X48]:((![X49]:~iext(X48,X47,X49))|ip(X48)))),inference(variable_rename,[status(thm)],[c154])).])).
% 3.46/3.65  cnf(c157,plain,~iext(X104,X103,X102)|ip(X104),inference(split_conjunct,[status(thm)],[c156])).
% 3.46/3.65  cnf(c573,plain,ip(uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c157, c126])).
% 3.46/3.65  cnf(c598,plain,iext(uri_rdf_type,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c573, c138])).
% 3.46/3.65  cnf(c1092,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X630)|iext(X630,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c598, c31])).
% 3.46/3.65  cnf(c597,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c573, c23])).
% 3.46/3.65  cnf(c1084,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X629)|iext(X629,uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c597, c31])).
% 3.46/3.65  cnf(c6,plain,iext(uri_owl_complementOf,skolem0002,skolem0003),inference(split_conjunct,[status(thm)],[c1])).
% 3.46/3.65  cnf(c544,plain,ip(uri_owl_complementOf),inference(resolution,[status(thm)],[c157, c6])).
% 3.46/3.65  cnf(c596,plain,iext(uri_rdf_type,uri_owl_complementOf,uri_rdf_Property),inference(resolution,[status(thm)],[c544, c138])).
% 3.46/3.65  cnf(c1077,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X627)|iext(X627,uri_owl_complementOf,uri_rdf_Property),inference(resolution,[status(thm)],[c596, c31])).
% 3.46/3.65  cnf(c595,plain,iext(uri_rdfs_subPropertyOf,uri_owl_complementOf,uri_owl_complementOf),inference(resolution,[status(thm)],[c544, c23])).
% 3.46/3.65  cnf(c1068,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X626)|iext(X626,uri_owl_complementOf,uri_owl_complementOf),inference(resolution,[status(thm)],[c595, c31])).
% 3.46/3.65  cnf(c7,plain,iext(uri_owl_oneOf,skolem0003,skolem0004),inference(split_conjunct,[status(thm)],[c1])).
% 3.46/3.65  cnf(c536,plain,ip(uri_owl_oneOf),inference(resolution,[status(thm)],[c157, c7])).
% 3.46/3.65  cnf(c594,plain,iext(uri_rdf_type,uri_owl_oneOf,uri_rdf_Property),inference(resolution,[status(thm)],[c536, c138])).
% 3.46/3.65  cnf(c1060,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X624)|iext(X624,uri_owl_oneOf,uri_rdf_Property),inference(resolution,[status(thm)],[c594, c31])).
% 3.46/3.65  cnf(c593,plain,iext(uri_rdfs_subPropertyOf,uri_owl_oneOf,uri_owl_oneOf),inference(resolution,[status(thm)],[c536, c23])).
% 3.46/3.65  cnf(c1051,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X623)|iext(X623,uri_owl_oneOf,uri_owl_oneOf),inference(resolution,[status(thm)],[c593, c31])).
% 3.46/3.65  cnf(c5,plain,iext(uri_owl_allValuesFrom,skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c1])).
% 3.46/3.65  cnf(c533,plain,ip(uri_owl_allValuesFrom),inference(resolution,[status(thm)],[c157, c5])).
% 3.46/3.65  cnf(c592,plain,iext(uri_rdf_type,uri_owl_allValuesFrom,uri_rdf_Property),inference(resolution,[status(thm)],[c533, c138])).
% 3.46/3.65  cnf(c1045,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X621)|iext(X621,uri_owl_allValuesFrom,uri_rdf_Property),inference(resolution,[status(thm)],[c592, c31])).
% 3.46/3.65  cnf(c591,plain,iext(uri_rdfs_subPropertyOf,uri_owl_allValuesFrom,uri_owl_allValuesFrom),inference(resolution,[status(thm)],[c533, c23])).
% 3.46/3.65  cnf(c1037,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X620)|iext(X620,uri_owl_allValuesFrom,uri_owl_allValuesFrom),inference(resolution,[status(thm)],[c591, c31])).
% 3.46/3.65  cnf(c4,plain,iext(uri_owl_onProperty,skolem0001,uri_ex_p),inference(split_conjunct,[status(thm)],[c1])).
% 3.46/3.65  cnf(c527,plain,ip(uri_owl_onProperty),inference(resolution,[status(thm)],[c157, c4])).
% 3.46/3.65  cnf(c590,plain,iext(uri_rdf_type,uri_owl_onProperty,uri_rdf_Property),inference(resolution,[status(thm)],[c527, c138])).
% 3.46/3.65  cnf(c1030,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X618)|iext(X618,uri_owl_onProperty,uri_rdf_Property),inference(resolution,[status(thm)],[c590, c31])).
% 3.46/3.65  cnf(c589,plain,iext(uri_rdfs_subPropertyOf,uri_owl_onProperty,uri_owl_onProperty),inference(resolution,[status(thm)],[c527, c23])).
% 3.46/3.65  cnf(c1022,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X617)|iext(X617,uri_owl_onProperty,uri_owl_onProperty),inference(resolution,[status(thm)],[c589, c31])).
% 3.46/3.65  fof(rdfs_container_bag_sub,axiom,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Container),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_bag_sub)).
% 3.46/3.65  cnf(c107,plain,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Container),inference(split_conjunct,[status(thm)],[rdfs_container_bag_sub])).
% 3.46/3.65  cnf(c517,plain,ip(uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c157, c107])).
% 3.46/3.65  cnf(c588,plain,iext(uri_rdf_type,uri_rdfs_subClassOf,uri_rdf_Property),inference(resolution,[status(thm)],[c517, c138])).
% 3.46/3.65  cnf(c1015,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X615)|iext(X615,uri_rdfs_subClassOf,uri_rdf_Property),inference(resolution,[status(thm)],[c588, c31])).
% 3.46/3.65  cnf(c587,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c517, c23])).
% 3.46/3.65  cnf(c1007,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X614)|iext(X614,uri_rdfs_subClassOf,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c587, c31])).
% 3.46/3.65  fof(rdfs_value_domain,axiom,iext(uri_rdfs_domain,uri_rdf_value,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_value_domain)).
% 3.46/3.65  cnf(c15,plain,iext(uri_rdfs_domain,uri_rdf_value,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_value_domain])).
% 3.46/3.65  cnf(c516,plain,ip(uri_rdfs_domain),inference(resolution,[status(thm)],[c157, c15])).
% 3.46/3.65  cnf(c586,plain,iext(uri_rdf_type,uri_rdfs_domain,uri_rdf_Property),inference(resolution,[status(thm)],[c516, c138])).
% 3.46/3.65  cnf(c998,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X612)|iext(X612,uri_rdfs_domain,uri_rdf_Property),inference(resolution,[status(thm)],[c586, c31])).
% 3.46/3.65  cnf(c585,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,uri_rdfs_domain),inference(resolution,[status(thm)],[c516, c23])).
% 3.46/3.65  cnf(c985,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X611)|iext(X611,uri_rdfs_domain,uri_rdfs_domain),inference(resolution,[status(thm)],[c585, c31])).
% 3.46/3.65  fof(rdfs_container_n_range_002,axiom,iext(uri_rdfs_range,uri_rdf__2,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_range_002)).
% 3.46/3.65  cnf(c96,plain,iext(uri_rdfs_range,uri_rdf__2,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_range_002])).
% 3.46/3.65  cnf(c515,plain,ip(uri_rdfs_range),inference(resolution,[status(thm)],[c157, c96])).
% 3.46/3.65  cnf(c584,plain,iext(uri_rdf_type,uri_rdfs_range,uri_rdf_Property),inference(resolution,[status(thm)],[c515, c138])).
% 3.46/3.65  cnf(c971,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X609)|iext(X609,uri_rdfs_range,uri_rdf_Property),inference(resolution,[status(thm)],[c584, c31])).
% 3.46/3.65  cnf(c583,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_range,uri_rdfs_range),inference(resolution,[status(thm)],[c515, c23])).
% 3.46/3.65  cnf(c960,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X608)|iext(X608,uri_rdfs_range,uri_rdfs_range),inference(resolution,[status(thm)],[c583, c31])).
% 3.46/3.65  fof(rdf_collection_first_type,axiom,iext(uri_rdf_type,uri_rdf_first,uri_rdf_Property),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdf_collection_first_type)).
% 3.46/3.65  cnf(c147,plain,iext(uri_rdf_type,uri_rdf_first,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_collection_first_type])).
% 3.46/3.65  cnf(c510,plain,ip(uri_rdf_first),inference(resolution,[status(thm)],[c147, c137])).
% 3.46/3.65  cnf(c512,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_first,uri_rdf_first),inference(resolution,[status(thm)],[c510, c23])).
% 3.46/3.65  cnf(c935,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X606)|iext(X606,uri_rdf_first,uri_rdf_first),inference(resolution,[status(thm)],[c512, c31])).
% 3.46/3.65  fof(rdf_collection_rest_type,axiom,iext(uri_rdf_type,uri_rdf_rest,uri_rdf_Property),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdf_collection_rest_type)).
% 3.46/3.65  cnf(c145,plain,iext(uri_rdf_type,uri_rdf_rest,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_collection_rest_type])).
% 3.46/3.65  cnf(c497,plain,ip(uri_rdf_rest),inference(resolution,[status(thm)],[c145, c137])).
% 3.46/3.65  cnf(c499,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_rest,uri_rdf_rest),inference(resolution,[status(thm)],[c497, c23])).
% 3.46/3.65  cnf(c926,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X604)|iext(X604,uri_rdf_rest,uri_rdf_rest),inference(resolution,[status(thm)],[c499, c31])).
% 3.46/3.65  fof(rdf_container_n_type_001,axiom,iext(uri_rdf_type,uri_rdf__1,uri_rdf_Property),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdf_container_n_type_001)).
% 3.46/3.65  cnf(c144,plain,iext(uri_rdf_type,uri_rdf__1,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_container_n_type_001])).
% 3.46/3.65  cnf(c489,plain,ip(uri_rdf__1),inference(resolution,[status(thm)],[c144, c137])).
% 3.46/3.65  cnf(c491,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__1,uri_rdf__1),inference(resolution,[status(thm)],[c489, c23])).
% 3.46/3.65  cnf(c917,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X602)|iext(X602,uri_rdf__1,uri_rdf__1),inference(resolution,[status(thm)],[c491, c31])).
% 3.46/3.65  fof(rdf_container_n_type_002,axiom,iext(uri_rdf_type,uri_rdf__2,uri_rdf_Property),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdf_container_n_type_002)).
% 3.46/3.65  cnf(c143,plain,iext(uri_rdf_type,uri_rdf__2,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_container_n_type_002])).
% 3.46/3.65  cnf(c481,plain,ip(uri_rdf__2),inference(resolution,[status(thm)],[c143, c137])).
% 3.46/3.65  cnf(c483,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__2,uri_rdf__2),inference(resolution,[status(thm)],[c481, c23])).
% 3.46/3.65  cnf(c909,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X600)|iext(X600,uri_rdf__2,uri_rdf__2),inference(resolution,[status(thm)],[c483, c31])).
% 3.46/3.65  fof(rdf_container_n_type_003,axiom,iext(uri_rdf_type,uri_rdf__3,uri_rdf_Property),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdf_container_n_type_003)).
% 3.46/3.65  cnf(c142,plain,iext(uri_rdf_type,uri_rdf__3,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_container_n_type_003])).
% 3.46/3.65  cnf(c473,plain,ip(uri_rdf__3),inference(resolution,[status(thm)],[c142, c137])).
% 3.46/3.65  cnf(c475,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__3,uri_rdf__3),inference(resolution,[status(thm)],[c473, c23])).
% 3.46/3.65  cnf(c902,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X598)|iext(X598,uri_rdf__3,uri_rdf__3),inference(resolution,[status(thm)],[c475, c31])).
% 3.46/3.65  fof(rdf_reification_object_type,axiom,iext(uri_rdf_type,uri_rdf_object,uri_rdf_Property),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdf_reification_object_type)).
% 3.46/3.65  cnf(c141,plain,iext(uri_rdf_type,uri_rdf_object,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_reification_object_type])).
% 3.46/3.65  cnf(c465,plain,ip(uri_rdf_object),inference(resolution,[status(thm)],[c141, c137])).
% 3.46/3.65  cnf(c467,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_object,uri_rdf_object),inference(resolution,[status(thm)],[c465, c23])).
% 3.46/3.65  cnf(c894,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X596)|iext(X596,uri_rdf_object,uri_rdf_object),inference(resolution,[status(thm)],[c467, c31])).
% 3.46/3.65  fof(rdf_reification_predicate_type,axiom,iext(uri_rdf_type,uri_rdf_value,uri_rdf_Property),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdf_reification_predicate_type)).
% 3.46/3.65  cnf(c140,plain,iext(uri_rdf_type,uri_rdf_value,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_reification_predicate_type])).
% 3.46/3.65  cnf(c453,plain,ip(uri_rdf_value),inference(resolution,[status(thm)],[c140, c137])).
% 3.46/3.65  cnf(c459,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_value,uri_rdf_value),inference(resolution,[status(thm)],[c453, c23])).
% 3.46/3.65  cnf(c887,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X594)|iext(X594,uri_rdf_value,uri_rdf_value),inference(resolution,[status(thm)],[c459, c31])).
% 3.46/3.65  cnf(c29,plain,~iext(uri_rdfs_subPropertyOf,X58,X57)|ip(X58),inference(split_conjunct,[status(thm)],[c28])).
% 3.46/3.65  cnf(c389,plain,ip(uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c126, c29])).
% 3.46/3.65  cnf(c458,plain,iext(uri_rdf_type,uri_rdfs_isDefinedBy,uri_rdf_Property),inference(resolution,[status(thm)],[c138, c389])).
% 3.46/3.65  cnf(c881,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X592)|iext(X592,uri_rdfs_isDefinedBy,uri_rdf_Property),inference(resolution,[status(thm)],[c458, c31])).
% 3.46/3.65  cnf(c388,plain,ip(uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c126, c30])).
% 3.46/3.65  cnf(c455,plain,iext(uri_rdf_type,uri_rdfs_seeAlso,uri_rdf_Property),inference(resolution,[status(thm)],[c138, c388])).
% 3.46/3.65  cnf(c874,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X591)|iext(X591,uri_rdfs_seeAlso,uri_rdf_Property),inference(resolution,[status(thm)],[c455, c31])).
% 3.46/3.65  fof(rdf_reification_subject_type,axiom,iext(uri_rdf_type,uri_rdf_subject,uri_rdf_Property),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdf_reification_subject_type)).
% 3.46/3.65  cnf(c139,plain,iext(uri_rdf_type,uri_rdf_subject,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_reification_subject_type])).
% 3.46/3.65  cnf(c446,plain,ip(uri_rdf_subject),inference(resolution,[status(thm)],[c139, c137])).
% 3.46/3.65  cnf(c448,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_subject,uri_rdf_subject),inference(resolution,[status(thm)],[c446, c23])).
% 3.46/3.65  cnf(c866,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X590)|iext(X590,uri_rdf_subject,uri_rdf_subject),inference(resolution,[status(thm)],[c448, c31])).
% 3.46/3.65  fof(rdf_value_type,axiom,iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdf_value_type)).
% 3.46/3.65  cnf(c131,plain,iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_value_type])).
% 3.46/3.65  cnf(c441,plain,ip(uri_rdf_type),inference(resolution,[status(thm)],[c137, c131])).
% 3.46/3.65  cnf(c442,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_type,uri_rdf_type),inference(resolution,[status(thm)],[c441, c23])).
% 3.46/3.65  cnf(c858,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X588)|iext(X588,uri_rdf_type,uri_rdf_type),inference(resolution,[status(thm)],[c442, c31])).
% 3.46/3.65  fof(rdfs_container_n_type_003,axiom,iext(uri_rdf_type,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_type_003)).
% 3.46/3.65  cnf(c92,plain,iext(uri_rdf_type,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),inference(split_conjunct,[status(thm)],[rdfs_container_n_type_003])).
% 3.46/3.65  cnf(c398,plain,icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__3),inference(resolution,[status(thm)],[c120, c92])).
% 3.46/3.65  cnf(c419,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__3,uri_rdfs_member),inference(resolution,[status(thm)],[c398, c106])).
% 3.46/3.65  cnf(c845,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X586)|iext(X586,uri_rdf__3,uri_rdfs_member),inference(resolution,[status(thm)],[c419, c31])).
% 3.46/3.65  fof(rdfs_subpropertyof_trans,axiom,(![P]:(![Q]:(![R]:((iext(uri_rdfs_subPropertyOf,P,Q)&iext(uri_rdfs_subPropertyOf,Q,R))=>iext(uri_rdfs_subPropertyOf,P,R))))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_subpropertyof_trans)).
% 3.46/3.65  fof(c18,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.46/3.65  fof(c19,plain,(![X7]:(![X8]:(![X9]:((~iext(uri_rdfs_subPropertyOf,X7,X8)|~iext(uri_rdfs_subPropertyOf,X8,X9))|iext(uri_rdfs_subPropertyOf,X7,X9))))),inference(variable_rename,[status(thm)],[c18])).
% 3.46/3.65  cnf(c20,plain,~iext(uri_rdfs_subPropertyOf,X53,X54)|~iext(uri_rdfs_subPropertyOf,X54,X55)|iext(uri_rdfs_subPropertyOf,X53,X55),inference(split_conjunct,[status(thm)],[c19])).
% 3.46/3.65  cnf(c844,plain,~iext(uri_rdfs_subPropertyOf,X585,uri_rdf__3)|iext(uri_rdfs_subPropertyOf,X585,uri_rdfs_member),inference(resolution,[status(thm)],[c419, c20])).
% 3.46/3.65  fof(rdfs_container_n_type_001,axiom,iext(uri_rdf_type,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_type_001)).
% 3.46/3.65  cnf(c94,plain,iext(uri_rdf_type,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),inference(split_conjunct,[status(thm)],[rdfs_container_n_type_001])).
% 3.46/3.65  cnf(c397,plain,icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__1),inference(resolution,[status(thm)],[c120, c94])).
% 3.46/3.65  cnf(c417,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__1,uri_rdfs_member),inference(resolution,[status(thm)],[c397, c106])).
% 3.46/3.65  cnf(c838,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X584)|iext(X584,uri_rdf__1,uri_rdfs_member),inference(resolution,[status(thm)],[c417, c31])).
% 3.46/3.65  cnf(c837,plain,~iext(uri_rdfs_subPropertyOf,X583,uri_rdf__1)|iext(uri_rdfs_subPropertyOf,X583,uri_rdfs_member),inference(resolution,[status(thm)],[c417, c20])).
% 3.46/3.65  cnf(c218,plain,ic(uri_rdfs_Container),inference(resolution,[status(thm)],[c45, c91])).
% 3.46/3.65  cnf(c224,plain,icext(uri_rdfs_Class,uri_rdfs_Container),inference(resolution,[status(thm)],[c218, c76])).
% 3.46/3.65  cnf(c415,plain,iext(uri_rdf_type,uri_rdfs_Container,uri_rdfs_Class),inference(resolution,[status(thm)],[c121, c224])).
% 3.46/3.65  cnf(c833,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X582)|iext(X582,uri_rdfs_Container,uri_rdfs_Class),inference(resolution,[status(thm)],[c415, c31])).
% 3.46/3.65  fof(rdfs_container_containermembershipproperty_sub,axiom,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_containermembershipproperty_sub)).
% 3.46/3.65  cnf(c103,plain,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_container_containermembershipproperty_sub])).
% 3.46/3.65  cnf(c277,plain,ic(uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c103, c44])).
% 3.46/3.65  cnf(c282,plain,icext(uri_rdfs_Class,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c277, c76])).
% 3.46/3.65  cnf(c414,plain,iext(uri_rdf_type,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Class),inference(resolution,[status(thm)],[c121, c282])).
% 3.46/3.65  cnf(c828,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X581)|iext(X581,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Class),inference(resolution,[status(thm)],[c414, c31])).
% 3.46/3.65  cnf(c214,plain,icext(uri_rdfs_Class,uri_rdfs_Seq),inference(resolution,[status(thm)],[c208, c76])).
% 3.46/3.65  cnf(c413,plain,iext(uri_rdf_type,uri_rdfs_Seq,uri_rdfs_Class),inference(resolution,[status(thm)],[c121, c214])).
% 3.46/3.65  cnf(c823,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X580)|iext(X580,uri_rdfs_Seq,uri_rdfs_Class),inference(resolution,[status(thm)],[c413, c31])).
% 3.46/3.65  fof(rdfs_datatype_sub,axiom,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Class),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_datatype_sub)).
% 3.46/3.65  cnf(c85,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_datatype_sub])).
% 3.46/3.65  cnf(c216,plain,ic(uri_rdfs_Class),inference(resolution,[status(thm)],[c45, c85])).
% 3.46/3.65  cnf(c220,plain,icext(uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c216, c76])).
% 3.46/3.65  cnf(c412,plain,iext(uri_rdf_type,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c121, c220])).
% 3.46/3.65  cnf(c818,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X579)|iext(X579,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c412, c31])).
% 3.46/3.65  fof(rdfs_dat_xmlliteral_sub,axiom,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Literal),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_dat_xmlliteral_sub)).
% 3.46/3.65  cnf(c90,plain,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[rdfs_dat_xmlliteral_sub])).
% 3.46/3.65  cnf(c207,plain,ic(uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c44, c90])).
% 3.46/3.65  cnf(c212,plain,icext(uri_rdfs_Class,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c207, c76])).
% 3.46/3.65  cnf(c410,plain,iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Class),inference(resolution,[status(thm)],[c121, c212])).
% 3.46/3.65  cnf(c812,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X578)|iext(X578,uri_rdf_XMLLiteral,uri_rdfs_Class),inference(resolution,[status(thm)],[c410, c31])).
% 3.46/3.65  cnf(c1355,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X577)|icext(X577,uri_rdfs_comment),inference(resolution,[status(thm)],[c1347, c83])).
% 3.46/3.65  cnf(c1353,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X576)|icext(X576,uri_rdfs_comment),inference(resolution,[status(thm)],[c1347, c57])).
% 3.46/3.65  cnf(c206,plain,ic(uri_rdfs_Datatype),inference(resolution,[status(thm)],[c44, c85])).
% 3.46/3.65  cnf(c210,plain,icext(uri_rdfs_Class,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c206, c76])).
% 3.46/3.65  cnf(c409,plain,iext(uri_rdf_type,uri_rdfs_Datatype,uri_rdfs_Class),inference(resolution,[status(thm)],[c121, c210])).
% 3.46/3.65  cnf(c807,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X574)|iext(X574,uri_rdfs_Datatype,uri_rdfs_Class),inference(resolution,[status(thm)],[c409, c31])).
% 3.46/3.65  cnf(c1325,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X572)|icext(X572,uri_rdfs_label),inference(resolution,[status(thm)],[c1318, c83])).
% 3.46/3.65  cnf(c333,plain,ic(uri_rdf_Bag),inference(resolution,[status(thm)],[c107, c44])).
% 3.46/3.65  cnf(c338,plain,icext(uri_rdfs_Class,uri_rdf_Bag),inference(resolution,[status(thm)],[c333, c76])).
% 3.46/3.65  cnf(c407,plain,iext(uri_rdf_type,uri_rdf_Bag,uri_rdfs_Class),inference(resolution,[status(thm)],[c121, c338])).
% 3.46/3.65  cnf(c801,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X571)|iext(X571,uri_rdf_Bag,uri_rdfs_Class),inference(resolution,[status(thm)],[c407, c31])).
% 3.46/3.65  cnf(c1323,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X570)|icext(X570,uri_rdfs_label),inference(resolution,[status(thm)],[c1318, c57])).
% 3.46/3.65  fof(rdfs_container_alt_sub,axiom,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Container),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_alt_sub)).
% 3.46/3.65  cnf(c108,plain,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Container),inference(split_conjunct,[status(thm)],[rdfs_container_alt_sub])).
% 3.46/3.65  cnf(c343,plain,ic(uri_rdf_Alt),inference(resolution,[status(thm)],[c108, c44])).
% 3.46/3.65  cnf(c348,plain,icext(uri_rdfs_Class,uri_rdf_Alt),inference(resolution,[status(thm)],[c343, c76])).
% 3.46/3.65  cnf(c405,plain,iext(uri_rdf_type,uri_rdf_Alt,uri_rdfs_Class),inference(resolution,[status(thm)],[c121, c348])).
% 3.46/3.65  cnf(c795,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X566)|iext(X566,uri_rdf_Alt,uri_rdfs_Class),inference(resolution,[status(thm)],[c405, c31])).
% 3.46/3.65  cnf(c1291,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X565)|icext(X565,uri_rdf_List),inference(resolution,[status(thm)],[c1273, c57])).
% 3.46/3.65  cnf(c1284,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X564)|icext(X564,uri_rdf_List),inference(resolution,[status(thm)],[c1272, c83])).
% 3.46/3.65  cnf(c217,plain,ic(uri_rdfs_Literal),inference(resolution,[status(thm)],[c45, c90])).
% 3.46/3.65  cnf(c222,plain,icext(uri_rdfs_Class,uri_rdfs_Literal),inference(resolution,[status(thm)],[c217, c76])).
% 3.46/3.65  cnf(c402,plain,iext(uri_rdf_type,uri_rdfs_Literal,uri_rdfs_Class),inference(resolution,[status(thm)],[c121, c222])).
% 3.46/3.65  cnf(c790,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X563)|iext(X563,uri_rdfs_Literal,uri_rdfs_Class),inference(resolution,[status(thm)],[c402, c31])).
% 3.46/3.65  cnf(c781,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X559)|iext(X559,uri_rdf__2,uri_rdfs_member),inference(resolution,[status(thm)],[c400, c31])).
% 3.46/3.65  cnf(c1248,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X558)|icext(X558,uri_rdf_predicate),inference(resolution,[status(thm)],[c1240, c83])).
% 3.46/3.65  cnf(c1246,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X557)|icext(X557,uri_rdf_predicate),inference(resolution,[status(thm)],[c1240, c57])).
% 3.46/3.65  cnf(c780,plain,~iext(uri_rdfs_subPropertyOf,X555,uri_rdf__2)|iext(uri_rdfs_subPropertyOf,X555,uri_rdfs_member),inference(resolution,[status(thm)],[c400, c20])).
% 3.46/3.65  cnf(c391,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c389, c23])).
% 3.46/3.65  cnf(c774,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X551)|iext(X551,uri_rdfs_isDefinedBy,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c391, c31])).
% 3.46/3.65  cnf(c1203,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X550)|icext(X550,uri_owl_ObjectProperty),inference(resolution,[status(thm)],[c1157, c57])).
% 3.46/3.65  cnf(c1189,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X547)|icext(X547,uri_owl_ObjectProperty),inference(resolution,[status(thm)],[c1156, c83])).
% 3.46/3.65  cnf(c1182,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X543)|icext(X543,uri_rdfs_Statement),inference(resolution,[status(thm)],[c1128, c57])).
% 3.46/3.65  cnf(c390,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_seeAlso,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c388, c23])).
% 3.46/3.65  cnf(c767,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X542)|iext(X542,uri_rdfs_seeAlso,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c390, c31])).
% 3.46/3.65  cnf(c1168,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X539)|icext(X539,uri_rdfs_Statement),inference(resolution,[status(thm)],[c1127, c83])).
% 3.46/3.65  cnf(c377,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Container,uri_rdfs_Resource),inference(resolution,[status(thm)],[c115, c218])).
% 3.46/3.65  cnf(c762,plain,~iext(uri_rdfs_subClassOf,X535,uri_rdfs_Container)|iext(uri_rdfs_subClassOf,X535,uri_rdfs_Resource),inference(resolution,[status(thm)],[c377, c35])).
% 3.46/3.65  cnf(c1152,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X534)|icext(X534,skolem0001),inference(resolution,[status(thm)],[c944, c57])).
% 3.46/3.65  cnf(c761,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X531)|iext(X531,uri_rdfs_Container,uri_rdfs_Resource),inference(resolution,[status(thm)],[c377, c31])).
% 3.46/3.65  cnf(c1138,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X530)|icext(X530,skolem0001),inference(resolution,[status(thm)],[c943, c83])).
% 3.46/3.65  cnf(c376,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Literal,uri_rdfs_Resource),inference(resolution,[status(thm)],[c115, c217])).
% 3.46/3.65  cnf(c754,plain,~iext(uri_rdfs_subClassOf,X528,uri_rdfs_Literal)|iext(uri_rdfs_subClassOf,X528,uri_rdfs_Resource),inference(resolution,[status(thm)],[c376, c35])).
% 3.46/3.65  cnf(c753,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X523)|iext(X523,uri_rdfs_Literal,uri_rdfs_Resource),inference(resolution,[status(thm)],[c376, c31])).
% 3.46/3.65  cnf(c1109,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X522)|icext(X522,uri_rdfs_member),inference(resolution,[status(thm)],[c785, c83])).
% 3.46/3.65  cnf(c375,plain,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Resource),inference(resolution,[status(thm)],[c115, c343])).
% 3.46/3.65  cnf(c746,plain,~iext(uri_rdfs_subClassOf,X519,uri_rdf_Alt)|iext(uri_rdfs_subClassOf,X519,uri_rdfs_Resource),inference(resolution,[status(thm)],[c375, c35])).
% 3.46/3.65  cnf(c1096,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X517)|icext(X517,uri_rdfs_Resource),inference(resolution,[status(thm)],[c687, c83])).
% 3.46/3.65  cnf(c745,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X515)|iext(X515,uri_rdf_Alt,uri_rdfs_Resource),inference(resolution,[status(thm)],[c375, c31])).
% 3.46/3.65  cnf(c1086,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X513)|icext(X513,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c597, c57])).
% 3.46/3.65  cnf(c374,plain,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Resource),inference(resolution,[status(thm)],[c115, c333])).
% 3.46/3.65  cnf(c738,plain,~iext(uri_rdfs_subClassOf,X512,uri_rdf_Bag)|iext(uri_rdfs_subClassOf,X512,uri_rdfs_Resource),inference(resolution,[status(thm)],[c374, c35])).
% 3.46/3.65  cnf(c1080,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X511)|icext(X511,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c597, c83])).
% 3.46/3.65  cnf(c737,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X508)|iext(X508,uri_rdf_Bag,uri_rdfs_Resource),inference(resolution,[status(thm)],[c374, c31])).
% 3.46/3.65  cnf(c1070,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X507)|icext(X507,uri_owl_complementOf),inference(resolution,[status(thm)],[c595, c57])).
% 3.46/3.65  cnf(c1064,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X506)|icext(X506,uri_owl_complementOf),inference(resolution,[status(thm)],[c595, c83])).
% 3.46/3.65  cnf(c373,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Resource),inference(resolution,[status(thm)],[c115, c206])).
% 3.46/3.65  cnf(c730,plain,~iext(uri_rdfs_subClassOf,X504,uri_rdfs_Datatype)|iext(uri_rdfs_subClassOf,X504,uri_rdfs_Resource),inference(resolution,[status(thm)],[c373, c35])).
% 3.46/3.65  cnf(c1054,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X502)|icext(X502,uri_owl_oneOf),inference(resolution,[status(thm)],[c593, c57])).
% 3.46/3.65  cnf(c729,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X501)|iext(X501,uri_rdfs_Datatype,uri_rdfs_Resource),inference(resolution,[status(thm)],[c373, c31])).
% 3.46/3.65  cnf(c1048,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X500)|icext(X500,uri_owl_oneOf),inference(resolution,[status(thm)],[c593, c83])).
% 3.46/3.65  cnf(c279,plain,ic(uri_rdf_Property),inference(resolution,[status(thm)],[c103, c45])).
% 3.46/3.65  cnf(c372,plain,iext(uri_rdfs_subClassOf,uri_rdf_Property,uri_rdfs_Resource),inference(resolution,[status(thm)],[c115, c279])).
% 3.46/3.65  cnf(c722,plain,~iext(uri_rdfs_subClassOf,X497,uri_rdf_Property)|iext(uri_rdfs_subClassOf,X497,uri_rdfs_Resource),inference(resolution,[status(thm)],[c372, c35])).
% 3.46/3.65  cnf(c1039,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X496)|icext(X496,uri_owl_allValuesFrom),inference(resolution,[status(thm)],[c591, c57])).
% 3.46/3.65  cnf(c1033,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X495)|icext(X495,uri_owl_allValuesFrom),inference(resolution,[status(thm)],[c591, c83])).
% 3.46/3.65  cnf(c721,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X494)|iext(X494,uri_rdf_Property,uri_rdfs_Resource),inference(resolution,[status(thm)],[c372, c31])).
% 3.46/3.65  cnf(c371,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c115, c216])).
% 3.46/3.65  cnf(c714,plain,~iext(uri_rdfs_subClassOf,X491,uri_rdfs_Class)|iext(uri_rdfs_subClassOf,X491,uri_rdfs_Resource),inference(resolution,[status(thm)],[c371, c35])).
% 3.46/3.65  cnf(c1024,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X490)|icext(X490,uri_owl_onProperty),inference(resolution,[status(thm)],[c589, c57])).
% 3.46/3.65  cnf(c1018,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X489)|icext(X489,uri_owl_onProperty),inference(resolution,[status(thm)],[c589, c83])).
% 3.46/3.65  cnf(c713,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X487)|iext(X487,uri_rdfs_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c371, c31])).
% 3.46/3.65  cnf(c1009,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X485)|icext(X485,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c587, c57])).
% 3.46/3.65  cnf(c370,plain,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Resource),inference(resolution,[status(thm)],[c115, c207])).
% 3.46/3.65  cnf(c706,plain,~iext(uri_rdfs_subClassOf,X484,uri_rdf_XMLLiteral)|iext(uri_rdfs_subClassOf,X484,uri_rdfs_Resource),inference(resolution,[status(thm)],[c370, c35])).
% 3.46/3.65  cnf(c1001,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X483)|icext(X483,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c587, c83])).
% 3.46/3.65  cnf(c705,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X480)|iext(X480,uri_rdf_XMLLiteral,uri_rdfs_Resource),inference(resolution,[status(thm)],[c370, c31])).
% 3.46/3.65  cnf(c990,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X479)|icext(X479,uri_rdfs_domain),inference(resolution,[status(thm)],[c585, c57])).
% 3.46/3.65  cnf(c974,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X478)|icext(X478,uri_rdfs_domain),inference(resolution,[status(thm)],[c585, c83])).
% 3.46/3.65  cnf(c369,plain,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Resource),inference(resolution,[status(thm)],[c115, c277])).
% 3.46/3.65  cnf(c698,plain,~iext(uri_rdfs_subClassOf,X476,uri_rdfs_ContainerMembershipProperty)|iext(uri_rdfs_subClassOf,X476,uri_rdfs_Resource),inference(resolution,[status(thm)],[c369, c35])).
% 3.46/3.65  cnf(c964,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X474)|icext(X474,uri_rdfs_range),inference(resolution,[status(thm)],[c583, c57])).
% 3.46/3.65  cnf(c697,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X473)|iext(X473,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Resource),inference(resolution,[status(thm)],[c369, c31])).
% 3.46/3.65  cnf(c947,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X472)|icext(X472,uri_rdfs_range),inference(resolution,[status(thm)],[c583, c83])).
% 3.46/3.65  cnf(c938,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X471)|icext(X471,uri_rdf_first),inference(resolution,[status(thm)],[c512, c57])).
% 3.46/3.65  cnf(c685,plain,~iext(uri_rdfs_subClassOf,X470,uri_rdfs_Seq)|iext(uri_rdfs_subClassOf,X470,uri_rdfs_Resource),inference(resolution,[status(thm)],[c368, c35])).
% 3.46/3.65  cnf(c932,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X469)|icext(X469,uri_rdf_first),inference(resolution,[status(thm)],[c512, c83])).
% 3.46/3.65  cnf(c928,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X468)|icext(X468,uri_rdf_rest),inference(resolution,[status(thm)],[c499, c57])).
% 3.46/3.65  cnf(c684,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X467)|iext(X467,uri_rdfs_Seq,uri_rdfs_Resource),inference(resolution,[status(thm)],[c368, c31])).
% 3.46/3.65  cnf(c922,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X466)|icext(X466,uri_rdf_rest),inference(resolution,[status(thm)],[c499, c83])).
% 3.46/3.65  cnf(c919,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X465)|icext(X465,uri_rdf__1),inference(resolution,[status(thm)],[c491, c57])).
% 3.46/3.65  cnf(c911,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X462)|icext(X462,uri_rdf__2),inference(resolution,[status(thm)],[c483, c57])).
% 3.46/3.65  cnf(c904,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X460)|icext(X460,uri_rdf__3),inference(resolution,[status(thm)],[c475, c57])).
% 3.46/3.65  cnf(c347,plain,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdf_Alt),inference(resolution,[status(thm)],[c343, c38])).
% 3.46/3.65  cnf(c676,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X459)|iext(X459,uri_rdf_Alt,uri_rdf_Alt),inference(resolution,[status(thm)],[c347, c31])).
% 3.46/3.65  cnf(c896,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X457)|icext(X457,uri_rdf_object),inference(resolution,[status(thm)],[c467, c57])).
% 3.46/3.65  cnf(c891,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X456)|icext(X456,uri_rdf_object),inference(resolution,[status(thm)],[c467, c83])).
% 3.46/3.65  cnf(c889,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X454)|icext(X454,uri_rdf_value),inference(resolution,[status(thm)],[c459, c57])).
% 3.46/3.65  cnf(c884,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X453)|icext(X453,uri_rdf_value),inference(resolution,[status(thm)],[c459, c83])).
% 3.46/3.65  cnf(c337,plain,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdf_Bag),inference(resolution,[status(thm)],[c333, c38])).
% 3.46/3.65  cnf(c668,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X452)|iext(X452,uri_rdf_Bag,uri_rdf_Bag),inference(resolution,[status(thm)],[c337, c31])).
% 3.46/3.65  cnf(c868,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X446)|icext(X446,uri_rdf_subject),inference(resolution,[status(thm)],[c448, c57])).
% 3.46/3.65  cnf(c863,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X445)|icext(X445,uri_rdf_subject),inference(resolution,[status(thm)],[c448, c83])).
% 3.46/3.65  cnf(c326,plain,iext(uri_rdfs_subClassOf,uri_rdf_Property,uri_rdf_Property),inference(resolution,[status(thm)],[c279, c38])).
% 3.46/3.65  cnf(c660,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X444)|iext(X444,uri_rdf_Property,uri_rdf_Property),inference(resolution,[status(thm)],[c326, c31])).
% 3.46/3.65  cnf(c861,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X443)|icext(X443,uri_rdf_type),inference(resolution,[status(thm)],[c442, c57])).
% 3.46/3.65  cnf(c849,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X442)|icext(X442,uri_rdf_type),inference(resolution,[status(thm)],[c442, c83])).
% 3.46/3.65  cnf(c842,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X439)|icext(X439,uri_rdf__3),inference(resolution,[status(thm)],[c419, c83])).
% 3.46/3.65  cnf(c835,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X437)|icext(X437,uri_rdf__1),inference(resolution,[status(thm)],[c417, c83])).
% 3.46/3.65  cnf(c281,plain,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c277, c38])).
% 3.46/3.65  cnf(c652,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X436)|iext(X436,uri_rdfs_ContainerMembershipProperty,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c281, c31])).
% 3.46/3.65  cnf(c223,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Container,uri_rdfs_Container),inference(resolution,[status(thm)],[c218, c38])).
% 3.46/3.65  cnf(c644,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X425)|iext(X425,uri_rdfs_Container,uri_rdfs_Container),inference(resolution,[status(thm)],[c223, c31])).
% 3.46/3.65  cnf(c221,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Literal,uri_rdfs_Literal),inference(resolution,[status(thm)],[c217, c38])).
% 3.46/3.65  cnf(c636,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X414)|iext(X414,uri_rdfs_Literal,uri_rdfs_Literal),inference(resolution,[status(thm)],[c221, c31])).
% 3.46/3.65  cnf(c783,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X413)|icext(X413,uri_rdfs_member),inference(resolution,[status(thm)],[c400, c57])).
% 3.46/3.65  cnf(c778,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X412)|icext(X412,uri_rdf__2),inference(resolution,[status(thm)],[c400, c83])).
% 3.46/3.65  cnf(c776,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X410)|icext(X410,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c391, c57])).
% 3.46/3.65  cnf(c219,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c216, c38])).
% 3.46/3.65  cnf(c628,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X407)|iext(X407,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c219, c31])).
% 3.46/3.65  cnf(c764,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X406)|icext(X406,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c390, c83])).
% 3.46/3.65  cnf(c213,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Seq),inference(resolution,[status(thm)],[c208, c38])).
% 3.46/3.65  cnf(c620,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X396)|iext(X396,uri_rdfs_Seq,uri_rdfs_Seq),inference(resolution,[status(thm)],[c213, c31])).
% 3.46/3.65  cnf(c211,plain,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c207, c38])).
% 3.46/3.65  cnf(c612,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X385)|iext(X385,uri_rdf_XMLLiteral,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c211, c31])).
% 3.46/3.65  cnf(c686,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X383)|icext(X383,uri_rdfs_Resource),inference(resolution,[status(thm)],[c368, c57])).
% 3.46/3.65  cnf(c678,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X380)|icext(X380,uri_rdf_Alt),inference(resolution,[status(thm)],[c347, c57])).
% 3.46/3.65  cnf(c670,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X378)|icext(X378,uri_rdf_Bag),inference(resolution,[status(thm)],[c337, c57])).
% 3.46/3.65  cnf(c209,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c206, c38])).
% 3.46/3.65  cnf(c604,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X377)|iext(X377,uri_rdfs_Datatype,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c209, c31])).
% 3.46/3.65  cnf(c656,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X374)|icext(X374,uri_rdf_Property),inference(resolution,[status(thm)],[c326, c83])).
% 3.46/3.65  cnf(c511,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X373)|iext(X373,uri_rdf_first,uri_rdf_Property),inference(resolution,[status(thm)],[c147, c31])).
% 3.46/3.65  cnf(c654,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X372)|icext(X372,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c281, c57])).
% 3.46/3.65  fof(rdf_collection_nil_type,axiom,iext(uri_rdf_type,uri_rdf_nil,uri_rdf_List),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdf_collection_nil_type)).
% 3.46/3.65  cnf(c146,plain,iext(uri_rdf_type,uri_rdf_nil,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdf_collection_nil_type])).
% 3.46/3.65  cnf(c505,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X369)|iext(X369,uri_rdf_nil,uri_rdf_List),inference(resolution,[status(thm)],[c146, c31])).
% 3.46/3.65  cnf(c640,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X368)|icext(X368,uri_rdfs_Container),inference(resolution,[status(thm)],[c223, c83])).
% 3.46/3.65  cnf(c498,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X366)|iext(X366,uri_rdf_rest,uri_rdf_Property),inference(resolution,[status(thm)],[c145, c31])).
% 3.46/3.65  cnf(c632,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X365)|icext(X365,uri_rdfs_Literal),inference(resolution,[status(thm)],[c221, c83])).
% 3.46/3.65  cnf(c624,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X363)|icext(X363,uri_rdfs_Class),inference(resolution,[status(thm)],[c219, c83])).
% 3.46/3.65  cnf(c490,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X362)|iext(X362,uri_rdf__1,uri_rdf_Property),inference(resolution,[status(thm)],[c144, c31])).
% 3.46/3.65  cnf(c622,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X361)|icext(X361,uri_rdfs_Seq),inference(resolution,[status(thm)],[c213, c57])).
% 3.46/3.65  cnf(c482,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X359)|iext(X359,uri_rdf__2,uri_rdf_Property),inference(resolution,[status(thm)],[c143, c31])).
% 3.46/3.65  cnf(c614,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X358)|icext(X358,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c211, c57])).
% 3.46/3.65  cnf(c606,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X356)|icext(X356,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c209, c57])).
% 3.46/3.65  cnf(c474,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X355)|iext(X355,uri_rdf__3,uri_rdf_Property),inference(resolution,[status(thm)],[c142, c31])).
% 3.46/3.65  cnf(c466,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X351)|iext(X351,uri_rdf_object,uri_rdf_Property),inference(resolution,[status(thm)],[c141, c31])).
% 3.46/3.65  cnf(c504,plain,~iext(uri_rdfs_range,uri_rdf_type,X350)|icext(X350,uri_rdf_List),inference(resolution,[status(thm)],[c146, c57])).
% 3.46/3.65  cnf(c454,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X346)|iext(X346,uri_rdf_value,uri_rdf_Property),inference(resolution,[status(thm)],[c140, c31])).
% 3.46/3.65  cnf(c447,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X341)|iext(X341,uri_rdf_subject,uri_rdf_Property),inference(resolution,[status(thm)],[c139, c31])).
% 3.46/3.65  cnf(c439,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X336)|iext(X336,uri_rdf_type,uri_rdf_Property),inference(resolution,[status(thm)],[c131, c31])).
% 3.46/3.65  fof(rdfs_annotation_comment_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_comment,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_comment_domain)).
% 3.46/3.65  cnf(c130,plain,iext(uri_rdfs_domain,uri_rdfs_comment,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_comment_domain])).
% 3.46/3.65  cnf(c435,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X331)|iext(X331,uri_rdfs_comment,uri_rdfs_Resource),inference(resolution,[status(thm)],[c130, c31])).
% 3.46/3.65  cnf(c438,plain,~iext(uri_rdfs_range,uri_rdf_type,X330)|icext(X330,uri_rdf_Property),inference(resolution,[status(thm)],[c131, c57])).
% 3.46/3.65  cnf(c432,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X327)|iext(X327,uri_rdfs_comment,uri_rdfs_Literal),inference(resolution,[status(thm)],[c129, c31])).
% 3.46/3.65  cnf(c433,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X326)|icext(X326,uri_rdfs_comment),inference(resolution,[status(thm)],[c130, c83])).
% 3.46/3.65  fof(rdfs_annotation_isdefinedby_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_isdefinedby_domain)).
% 3.46/3.65  cnf(c128,plain,iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_domain])).
% 3.46/3.65  cnf(c429,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X324)|iext(X324,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(resolution,[status(thm)],[c128, c31])).
% 3.46/3.65  fof(rdfs_annotation_isdefinedby_range,axiom,iext(uri_rdfs_range,uri_rdfs_isDefinedBy,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_isdefinedby_range)).
% 3.46/3.65  cnf(c127,plain,iext(uri_rdfs_range,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_range])).
% 3.46/3.65  cnf(c426,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X323)|iext(X323,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(resolution,[status(thm)],[c127, c31])).
% 3.46/3.65  fof(simple_ir,axiom,(![X]:ir(X)),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', simple_ir)).
% 3.46/3.65  fof(c151,plain,(![X46]:ir(X46)),inference(variable_rename,[status(thm)],[simple_ir])).
% 3.46/3.65  cnf(c152,plain,ir(X50),inference(split_conjunct,[status(thm)],[c151])).
% 3.46/3.65  fof(rdfs_ir_def,axiom,(![X]:(ir(X)<=>icext(uri_rdfs_Resource,X))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_ir_def)).
% 3.46/3.65  fof(c66,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.46/3.65  fof(c67,plain,((![X]:(~ir(X)|icext(uri_rdfs_Resource,X)))&(![X]:(~icext(uri_rdfs_Resource,X)|ir(X)))),inference(shift_quantors,[status(thm)],[c66])).
% 3.46/3.65  fof(c69,plain,(![X28]:(![X29]:((~ir(X28)|icext(uri_rdfs_Resource,X28))&(~icext(uri_rdfs_Resource,X29)|ir(X29))))),inference(shift_quantors,[status(thm)],[fof(c68,plain,((![X28]:(~ir(X28)|icext(uri_rdfs_Resource,X28)))&(![X29]:(~icext(uri_rdfs_Resource,X29)|ir(X29)))),inference(variable_rename,[status(thm)],[c67])).])).
% 3.46/3.65  cnf(c70,plain,~ir(X61)|icext(uri_rdfs_Resource,X61),inference(split_conjunct,[status(thm)],[c69])).
% 3.46/3.65  cnf(c159,plain,icext(uri_rdfs_Resource,X62),inference(resolution,[status(thm)],[c70, c152])).
% 3.46/3.65  cnf(c403,plain,iext(uri_rdf_type,X98,uri_rdfs_Resource),inference(resolution,[status(thm)],[c121, c159])).
% 3.46/3.65  cnf(c423,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X321)|iext(X321,X320,uri_rdfs_Resource),inference(resolution,[status(thm)],[c403, c31])).
% 3.46/3.65  cnf(c387,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X317)|iext(X317,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c126, c31])).
% 3.46/3.65  cnf(c427,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X316)|icext(X316,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c128, c83])).
% 3.46/3.65  cnf(c424,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X314)|icext(X314,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c127, c83])).
% 3.46/3.65  cnf(c386,plain,~iext(uri_rdfs_subPropertyOf,X313,uri_rdfs_isDefinedBy)|iext(uri_rdfs_subPropertyOf,X313,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c126, c20])).
% 3.46/3.65  cnf(c422,plain,~iext(uri_rdfs_range,uri_rdf_type,X312)|icext(X312,uri_rdfs_Resource),inference(resolution,[status(thm)],[c403, c57])).
% 3.46/3.65  cnf(c385,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X311)|icext(X311,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c126, c57])).
% 3.46/3.65  fof(rdfs_annotation_label_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_label,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_label_domain)).
% 3.46/3.65  cnf(c125,plain,iext(uri_rdfs_domain,uri_rdfs_label,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_label_domain])).
% 3.46/3.65  cnf(c383,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X310)|iext(X310,uri_rdfs_label,uri_rdfs_Resource),inference(resolution,[status(thm)],[c125, c31])).
% 3.46/3.65  cnf(c384,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X309)|icext(X309,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c126, c83])).
% 3.46/3.65  cnf(c380,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X307)|iext(X307,uri_rdfs_label,uri_rdfs_Literal),inference(resolution,[status(thm)],[c124, c31])).
% 3.46/3.65  cnf(c381,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X306)|icext(X306,uri_rdfs_label),inference(resolution,[status(thm)],[c125, c83])).
% 3.46/3.65  cnf(c379,plain,~iext(uri_rdfs_range,uri_rdfs_range,X305)|icext(X305,uri_rdfs_Literal),inference(resolution,[status(thm)],[c124, c57])).
% 3.46/3.65  fof(rdfs_annotation_seealso_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_seeAlso,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_seealso_domain)).
% 3.46/3.65  cnf(c123,plain,iext(uri_rdfs_domain,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_seealso_domain])).
% 3.46/3.65  cnf(c367,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X304)|iext(X304,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(resolution,[status(thm)],[c123, c31])).
% 3.46/3.65  fof(rdfs_annotation_seealso_range,axiom,iext(uri_rdfs_range,uri_rdfs_seeAlso,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_seealso_range)).
% 3.46/3.65  cnf(c122,plain,iext(uri_rdfs_range,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_seealso_range])).
% 3.46/3.65  cnf(c364,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X302)|iext(X302,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(resolution,[status(thm)],[c122, c31])).
% 3.46/3.65  cnf(c365,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X300)|icext(X300,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c123, c83])).
% 3.46/3.65  fof(rdfs_collection_first_domain,axiom,iext(uri_rdfs_domain,uri_rdf_first,uri_rdf_List),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_collection_first_domain)).
% 3.46/3.65  cnf(c112,plain,iext(uri_rdfs_domain,uri_rdf_first,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdfs_collection_first_domain])).
% 3.46/3.65  cnf(c361,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X298)|iext(X298,uri_rdf_first,uri_rdf_List),inference(resolution,[status(thm)],[c112, c31])).
% 3.46/3.65  cnf(c362,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X297)|icext(X297,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c122, c83])).
% 3.46/3.65  fof(rdfs_collection_first_range,axiom,iext(uri_rdfs_range,uri_rdf_first,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_collection_first_range)).
% 3.46/3.65  cnf(c111,plain,iext(uri_rdfs_range,uri_rdf_first,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_collection_first_range])).
% 3.46/3.65  cnf(c358,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X295)|iext(X295,uri_rdf_first,uri_rdfs_Resource),inference(resolution,[status(thm)],[c111, c31])).
% 3.46/3.65  cnf(c359,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X294)|icext(X294,uri_rdf_first),inference(resolution,[status(thm)],[c112, c83])).
% 3.46/3.65  cnf(c356,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X292)|icext(X292,uri_rdf_first),inference(resolution,[status(thm)],[c111, c83])).
% 3.46/3.65  cnf(c355,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X291)|iext(X291,uri_rdf_rest,uri_rdf_List),inference(resolution,[status(thm)],[c110, c31])).
% 3.46/3.65  cnf(c354,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X290)|icext(X290,uri_rdf_List),inference(resolution,[status(thm)],[c110, c57])).
% 3.46/3.65  cnf(c353,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X287)|icext(X287,uri_rdf_rest),inference(resolution,[status(thm)],[c110, c83])).
% 3.46/3.65  cnf(c352,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X286)|iext(X286,uri_rdf_rest,uri_rdf_List),inference(resolution,[status(thm)],[c109, c31])).
% 3.46/3.65  cnf(c346,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X285)|iext(X285,uri_rdf_Alt,uri_rdfs_Container),inference(resolution,[status(thm)],[c108, c31])).
% 3.46/3.65  cnf(c344,plain,~iext(uri_rdfs_subClassOf,X284,uri_rdf_Alt)|iext(uri_rdfs_subClassOf,X284,uri_rdfs_Container),inference(resolution,[status(thm)],[c108, c35])).
% 3.46/3.65  cnf(c336,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X282)|iext(X282,uri_rdf_Bag,uri_rdfs_Container),inference(resolution,[status(thm)],[c107, c31])).
% 3.46/3.65  cnf(c350,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X281)|icext(X281,uri_rdf_rest),inference(resolution,[status(thm)],[c109, c83])).
% 3.46/3.65  cnf(c341,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X279)|icext(X279,uri_rdf_Alt),inference(resolution,[status(thm)],[c108, c83])).
% 3.46/3.65  cnf(c334,plain,~iext(uri_rdfs_subClassOf,X278,uri_rdf_Bag)|iext(uri_rdfs_subClassOf,X278,uri_rdfs_Container),inference(resolution,[status(thm)],[c107, c35])).
% 3.46/3.65  cnf(c331,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X276)|icext(X276,uri_rdf_Bag),inference(resolution,[status(thm)],[c107, c83])).
% 3.46/3.65  fof(rdfs_container_n_range_003,axiom,iext(uri_rdfs_range,uri_rdf__3,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_range_003)).
% 3.46/3.65  cnf(c95,plain,iext(uri_rdfs_range,uri_rdf__3,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_range_003])).
% 3.46/3.65  cnf(c325,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X275)|icext(X275,uri_rdf__3),inference(resolution,[status(thm)],[c83, c95])).
% 3.46/3.65  fof(rdfs_reification_predicate_range,axiom,iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_reification_predicate_range)).
% 3.46/3.65  cnf(c50,plain,iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_reification_predicate_range])).
% 3.46/3.65  cnf(c323,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X273)|icext(X273,uri_rdf_predicate),inference(resolution,[status(thm)],[c83, c50])).
% 3.46/3.65  fof(rdfs_container_n_domain_003,axiom,iext(uri_rdfs_domain,uri_rdf__3,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_domain_003)).
% 3.46/3.65  cnf(c98,plain,iext(uri_rdfs_domain,uri_rdf__3,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_003])).
% 3.46/3.65  cnf(c322,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X272)|icext(X272,uri_rdf__3),inference(resolution,[status(thm)],[c83, c98])).
% 3.46/3.65  fof(rdfs_reification_subject_range,axiom,iext(uri_rdfs_range,uri_rdf_subject,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_reification_subject_range)).
% 3.46/3.65  cnf(c48,plain,iext(uri_rdfs_range,uri_rdf_subject,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_reification_subject_range])).
% 3.46/3.65  cnf(c321,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X271)|icext(X271,uri_rdf_subject),inference(resolution,[status(thm)],[c83, c48])).
% 3.46/3.65  fof(rdfs_reification_subject_domain,axiom,iext(uri_rdfs_domain,uri_rdf_subject,uri_rdfs_Statement),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_reification_subject_domain)).
% 3.46/3.65  cnf(c49,plain,iext(uri_rdfs_domain,uri_rdf_subject,uri_rdfs_Statement),inference(split_conjunct,[status(thm)],[rdfs_reification_subject_domain])).
% 3.46/3.65  cnf(c319,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X269)|icext(X269,uri_rdf_subject),inference(resolution,[status(thm)],[c83, c49])).
% 3.46/3.65  cnf(c318,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X268)|icext(X268,uri_rdfs_Seq),inference(resolution,[status(thm)],[c83, c91])).
% 3.46/3.65  fof(rdfs_reification_object_domain,axiom,iext(uri_rdfs_domain,uri_rdf_object,uri_rdfs_Statement),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_reification_object_domain)).
% 3.46/3.65  cnf(c53,plain,iext(uri_rdfs_domain,uri_rdf_object,uri_rdfs_Statement),inference(split_conjunct,[status(thm)],[rdfs_reification_object_domain])).
% 3.46/3.65  cnf(c317,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X267)|icext(X267,uri_rdf_object),inference(resolution,[status(thm)],[c83, c53])).
% 3.46/3.65  fof(rdfs_subclassof_range,axiom,iext(uri_rdfs_range,uri_rdfs_subClassOf,uri_rdfs_Class),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_subclassof_range)).
% 3.46/3.65  cnf(c39,plain,iext(uri_rdfs_range,uri_rdfs_subClassOf,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_subclassof_range])).
% 3.46/3.65  cnf(c316,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X266)|icext(X266,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c83, c39])).
% 3.46/3.65  fof(rdfs_subclassof_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdfs_Class),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_subclassof_domain)).
% 3.46/3.65  cnf(c47,plain,iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_subclassof_domain])).
% 3.46/3.65  cnf(c315,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X265)|icext(X265,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c83, c47])).
% 3.46/3.65  cnf(c314,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X264)|icext(X264,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c83, c90])).
% 3.46/3.65  fof(rdfs_container_member_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_member,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_member_domain)).
% 3.46/3.65  cnf(c102,plain,iext(uri_rdfs_domain,uri_rdfs_member,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_member_domain])).
% 3.46/3.65  cnf(c312,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X262)|icext(X262,uri_rdfs_member),inference(resolution,[status(thm)],[c83, c102])).
% 3.46/3.65  fof(rdfs_container_member_range,axiom,iext(uri_rdfs_range,uri_rdfs_member,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_member_range)).
% 3.46/3.65  cnf(c101,plain,iext(uri_rdfs_range,uri_rdfs_member,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_member_range])).
% 3.46/3.65  cnf(c311,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X261)|icext(X261,uri_rdfs_member),inference(resolution,[status(thm)],[c83, c101])).
% 3.46/3.65  cnf(c309,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X259)|icext(X259,uri_rdfs_range),inference(resolution,[status(thm)],[c83, c54])).
% 3.46/3.65  fof(rdfs_value_range,axiom,iext(uri_rdfs_range,uri_rdf_value,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_value_range)).
% 3.46/3.65  cnf(c14,plain,iext(uri_rdfs_range,uri_rdf_value,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_value_range])).
% 3.46/3.65  cnf(c308,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X258)|icext(X258,uri_rdf_value),inference(resolution,[status(thm)],[c83, c14])).
% 3.46/3.65  cnf(c8,plain,iext(uri_rdf_first,skolem0004,uri_ex_o),inference(split_conjunct,[status(thm)],[c1])).
% 3.46/3.65  cnf(c307,plain,~iext(uri_rdfs_domain,uri_rdf_first,X257)|icext(X257,skolem0004),inference(resolution,[status(thm)],[c83, c8])).
% 3.46/3.65  fof(rdfs_subpropertyof_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdf_Property),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_subpropertyof_domain)).
% 3.46/3.65  cnf(c32,plain,iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_subpropertyof_domain])).
% 3.46/3.65  cnf(c303,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X253)|icext(X253,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c83, c32])).
% 3.46/3.65  fof(rdfs_container_n_domain_001,axiom,iext(uri_rdfs_domain,uri_rdf__1,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_domain_001)).
% 3.46/3.65  cnf(c100,plain,iext(uri_rdfs_domain,uri_rdf__1,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_001])).
% 3.46/3.65  cnf(c302,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X252)|icext(X252,uri_rdf__1),inference(resolution,[status(thm)],[c83, c100])).
% 3.46/3.65  cnf(c301,plain,~iext(uri_rdfs_domain,uri_owl_complementOf,X251)|icext(X251,skolem0002),inference(resolution,[status(thm)],[c83, c6])).
% 3.46/3.65  fof(rdfs_subpropertyof_range,axiom,iext(uri_rdfs_range,uri_rdfs_subPropertyOf,uri_rdf_Property),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_subpropertyof_range)).
% 3.46/3.65  cnf(c24,plain,iext(uri_rdfs_range,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_subpropertyof_range])).
% 3.46/3.65  cnf(c299,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X249)|icext(X249,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c83, c24])).
% 3.46/3.65  cnf(c298,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X248)|icext(X248,uri_rdf_type),inference(resolution,[status(thm)],[c83, c16])).
% 3.46/3.65  cnf(c297,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X247)|icext(X247,uri_rdfs_range),inference(resolution,[status(thm)],[c83, c58])).
% 3.46/3.65  cnf(c296,plain,~iext(uri_rdfs_domain,uri_owl_oneOf,X246)|icext(X246,skolem0003),inference(resolution,[status(thm)],[c83, c7])).
% 3.46/3.65  cnf(c295,plain,~iext(uri_rdfs_domain,uri_owl_allValuesFrom,X245)|icext(X245,skolem0001),inference(resolution,[status(thm)],[c83, c5])).
% 3.46/3.65  fof(rdfs_container_n_range_001,axiom,iext(uri_rdfs_range,uri_rdf__1,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_range_001)).
% 3.46/3.65  cnf(c97,plain,iext(uri_rdfs_range,uri_rdf__1,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_range_001])).
% 3.46/3.65  cnf(c294,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X244)|icext(X244,uri_rdf__1),inference(resolution,[status(thm)],[c83, c97])).
% 3.46/3.65  fof(rdfs_type_domain,axiom,iext(uri_rdfs_domain,uri_rdf_type,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_type_domain)).
% 3.46/3.65  cnf(c17,plain,iext(uri_rdfs_domain,uri_rdf_type,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_type_domain])).
% 3.46/3.65  cnf(c293,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X243)|icext(X243,uri_rdf_type),inference(resolution,[status(thm)],[c83, c17])).
% 3.46/3.65  fof(rdfs_container_n_domain_002,axiom,iext(uri_rdfs_domain,uri_rdf__2,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_domain_002)).
% 3.46/3.65  cnf(c99,plain,iext(uri_rdfs_domain,uri_rdf__2,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_002])).
% 3.46/3.65  cnf(c292,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X242)|icext(X242,uri_rdf__2),inference(resolution,[status(thm)],[c83, c99])).
% 3.46/3.65  cnf(c291,plain,~iext(uri_rdfs_domain,uri_owl_onProperty,X241)|icext(X241,skolem0001),inference(resolution,[status(thm)],[c83, c4])).
% 3.46/3.65  cnf(c290,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X240)|icext(X240,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c83, c85])).
% 3.46/3.65  cnf(c289,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X239)|icext(X239,uri_rdfs_domain),inference(resolution,[status(thm)],[c83, c78])).
% 3.46/3.65  cnf(c421,plain,~iext(uri_rdfs_domain,uri_rdf_type,X235)|icext(X235,X236),inference(resolution,[status(thm)],[c403, c83])).
% 3.46/3.65  cnf(c287,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X234)|icext(X234,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c83, c103])).
% 3.46/3.65  cnf(c285,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X223)|icext(X223,uri_rdf_value),inference(resolution,[status(thm)],[c83, c15])).
% 3.46/3.65  cnf(c284,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X218)|icext(X218,uri_rdf__2),inference(resolution,[status(thm)],[c83, c96])).
% 3.46/3.65  cnf(c283,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X213)|icext(X213,uri_rdfs_domain),inference(factor,[status(thm)],[c83])).
% 3.46/3.65  cnf(c280,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X208)|iext(X208,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),inference(resolution,[status(thm)],[c103, c31])).
% 3.46/3.65  cnf(c278,plain,~iext(uri_rdfs_subClassOf,X203,uri_rdfs_ContainerMembershipProperty)|iext(uri_rdfs_subClassOf,X203,uri_rdf_Property),inference(resolution,[status(thm)],[c103, c35])).
% 3.46/3.65  cnf(c46,plain,~iext(uri_rdfs_subClassOf,X82,X80)|~icext(X82,X81)|icext(X80,X81),inference(split_conjunct,[status(thm)],[c43])).
% 3.46/3.65  cnf(c340,plain,~icext(uri_rdf_Alt,X200)|icext(uri_rdfs_Container,X200),inference(resolution,[status(thm)],[c108, c46])).
% 3.46/3.65  cnf(c330,plain,~icext(uri_rdf_Bag,X199)|icext(uri_rdfs_Container,X199),inference(resolution,[status(thm)],[c107, c46])).
% 3.46/3.65  cnf(c276,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X198)|icext(X198,uri_rdf_Property),inference(resolution,[status(thm)],[c103, c57])).
% 3.46/3.65  cnf(c275,plain,~icext(uri_rdfs_ContainerMembershipProperty,X197)|icext(uri_rdf_Property,X197),inference(resolution,[status(thm)],[c103, c46])).
% 3.46/3.65  cnf(c266,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X189)|icext(X189,uri_rdfs_Container),inference(resolution,[status(thm)],[c57, c91])).
% 3.46/3.65  cnf(c263,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X186)|icext(X186,uri_rdfs_Class),inference(resolution,[status(thm)],[c57, c47])).
% 3.46/3.65  cnf(c262,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X185)|icext(X185,uri_rdfs_Literal),inference(resolution,[status(thm)],[c57, c90])).
% 3.46/3.65  fof(rdfs_property_type,axiom,iext(uri_rdf_type,uri_rdf_Property,uri_rdfs_Class),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_property_type)).
% 3.46/3.65  cnf(c59,plain,iext(uri_rdf_type,uri_rdf_Property,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_property_type])).
% 3.46/3.65  cnf(c258,plain,~iext(uri_rdfs_range,uri_rdf_type,X181)|icext(X181,uri_rdfs_Class),inference(resolution,[status(thm)],[c57, c59])).
% 3.46/3.65  cnf(c255,plain,~iext(uri_rdfs_range,uri_rdf_first,X178)|icext(X178,uri_ex_o),inference(resolution,[status(thm)],[c57, c8])).
% 3.46/3.65  cnf(c1117,plain,icext(uri_rdf_Property,uri_rdfs_member),inference(resolution,[status(thm)],[c786, c120])).
% 3.46/3.65  cnf(c253,plain,~iext(uri_rdfs_range,uri_rdf_rest,X176)|icext(X176,uri_rdf_nil),inference(resolution,[status(thm)],[c57, c9])).
% 3.46/3.65  cnf(c252,plain,~iext(uri_rdfs_range,uri_rdf_type,X175)|icext(X175,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c57, c93])).
% 3.46/3.66  cnf(c1088,plain,icext(uri_rdf_Property,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c598, c120])).
% 3.46/3.66  cnf(c1073,plain,icext(uri_rdf_Property,uri_owl_complementOf),inference(resolution,[status(thm)],[c596, c120])).
% 3.46/3.66  cnf(c249,plain,~iext(uri_rdfs_range,uri_owl_complementOf,X172)|icext(X172,skolem0003),inference(resolution,[status(thm)],[c57, c6])).
% 3.46/3.66  fof(rdfs_dat_xmlliteral_type,axiom,iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Datatype),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_dat_xmlliteral_type)).
% 3.46/3.66  cnf(c89,plain,iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Datatype),inference(split_conjunct,[status(thm)],[rdfs_dat_xmlliteral_type])).
% 3.46/3.66  cnf(c248,plain,~iext(uri_rdfs_range,uri_rdf_type,X171)|icext(X171,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c57, c89])).
% 3.46/3.66  cnf(c1056,plain,icext(uri_rdf_Property,uri_owl_oneOf),inference(resolution,[status(thm)],[c594, c120])).
% 3.46/3.66  cnf(c247,plain,~iext(uri_rdfs_range,uri_rdfs_range,X170)|icext(X170,uri_rdf_Property),inference(resolution,[status(thm)],[c57, c24])).
% 3.46/3.66  cnf(c1041,plain,icext(uri_rdf_Property,uri_owl_allValuesFrom),inference(resolution,[status(thm)],[c592, c120])).
% 3.46/3.66  cnf(c244,plain,~iext(uri_rdfs_range,uri_owl_oneOf,X167)|icext(X167,skolem0004),inference(resolution,[status(thm)],[c57, c7])).
% 3.46/3.66  cnf(c1026,plain,icext(uri_rdf_Property,uri_owl_onProperty),inference(resolution,[status(thm)],[c590, c120])).
% 3.46/3.66  cnf(c243,plain,~iext(uri_rdfs_range,uri_owl_allValuesFrom,X166)|icext(X166,skolem0002),inference(resolution,[status(thm)],[c57, c5])).
% 3.46/3.66  cnf(c1011,plain,icext(uri_rdf_Property,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c588, c120])).
% 3.46/3.66  cnf(c994,plain,icext(uri_rdf_Property,uri_rdfs_domain),inference(resolution,[status(thm)],[c586, c120])).
% 3.46/3.66  cnf(c967,plain,icext(uri_rdf_Property,uri_rdfs_range),inference(resolution,[status(thm)],[c584, c120])).
% 3.46/3.66  cnf(c239,plain,~iext(uri_rdfs_range,uri_owl_onProperty,X162)|icext(X162,uri_ex_p),inference(resolution,[status(thm)],[c57, c4])).
% 3.46/3.66  cnf(c238,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X161)|icext(X161,uri_rdfs_Class),inference(resolution,[status(thm)],[c57, c85])).
% 3.46/3.66  cnf(c237,plain,~iext(uri_rdfs_range,uri_rdfs_range,X160)|icext(X160,uri_rdfs_Class),inference(resolution,[status(thm)],[c57, c78])).
% 3.46/3.66  cnf(c235,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X158)|icext(X158,uri_rdf_Property),inference(resolution,[status(thm)],[c57, c84])).
% 3.46/3.66  cnf(c234,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X157)|icext(X157,uri_rdfs_Resource),inference(resolution,[status(thm)],[c57, c15])).
% 3.46/3.66  cnf(c233,plain,~iext(uri_rdfs_range,uri_rdfs_range,X156)|icext(X156,uri_rdfs_Resource),inference(resolution,[status(thm)],[c57, c96])).
% 3.46/3.66  cnf(c232,plain,~iext(uri_rdfs_range,uri_rdfs_range,X155)|icext(X155,X155),inference(factor,[status(thm)],[c57])).
% 3.46/3.66  cnf(c228,plain,~icext(uri_rdfs_Seq,X154)|icext(uri_rdfs_Container,X154),inference(resolution,[status(thm)],[c46, c91])).
% 3.46/3.66  cnf(c227,plain,~icext(uri_rdf_XMLLiteral,X153)|icext(uri_rdfs_Literal,X153),inference(resolution,[status(thm)],[c46, c90])).
% 3.46/3.66  cnf(c226,plain,~icext(uri_rdfs_Datatype,X152)|icext(uri_rdfs_Class,X152),inference(resolution,[status(thm)],[c46, c85])).
% 3.46/3.66  cnf(c205,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X151)|iext(X151,uri_rdfs_member,uri_rdfs_Resource),inference(resolution,[status(thm)],[c102, c31])).
% 3.46/3.66  cnf(c204,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X150)|iext(X150,uri_rdfs_member,uri_rdfs_Resource),inference(resolution,[status(thm)],[c101, c31])).
% 3.46/3.66  cnf(c877,plain,icext(uri_rdf_Property,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c458, c120])).
% 3.46/3.66  cnf(c203,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X149)|iext(X149,uri_rdf__1,uri_rdfs_Resource),inference(resolution,[status(thm)],[c100, c31])).
% 3.46/3.66  cnf(c870,plain,icext(uri_rdf_Property,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c455, c120])).
% 3.46/3.66  cnf(c202,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X148)|iext(X148,uri_rdf__2,uri_rdfs_Resource),inference(resolution,[status(thm)],[c99, c31])).
% 3.46/3.66  cnf(c201,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X147)|iext(X147,uri_rdf__3,uri_rdfs_Resource),inference(resolution,[status(thm)],[c98, c31])).
% 3.46/3.66  cnf(c200,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X146)|iext(X146,uri_rdf__1,uri_rdfs_Resource),inference(resolution,[status(thm)],[c97, c31])).
% 3.46/3.66  cnf(c199,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X145)|iext(X145,uri_rdf__2,uri_rdfs_Resource),inference(resolution,[status(thm)],[c96, c31])).
% 3.46/3.66  cnf(c198,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X144)|iext(X144,uri_rdf__3,uri_rdfs_Resource),inference(resolution,[status(thm)],[c95, c31])).
% 3.46/3.66  cnf(c197,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X143)|iext(X143,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c94, c31])).
% 3.46/3.66  cnf(c196,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X142)|iext(X142,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c93, c31])).
% 3.46/3.66  cnf(c195,plain,~iext(uri_rdfs_subClassOf,X141,uri_rdfs_Seq)|iext(uri_rdfs_subClassOf,X141,uri_rdfs_Container),inference(resolution,[status(thm)],[c35, c91])).
% 3.46/3.66  cnf(c194,plain,~iext(uri_rdfs_subClassOf,X140,uri_rdf_XMLLiteral)|iext(uri_rdfs_subClassOf,X140,uri_rdfs_Literal),inference(resolution,[status(thm)],[c35, c90])).
% 3.46/3.66  cnf(c193,plain,~iext(uri_rdfs_subClassOf,X139,uri_rdfs_Datatype)|iext(uri_rdfs_subClassOf,X139,uri_rdfs_Class),inference(resolution,[status(thm)],[c35, c85])).
% 3.46/3.66  cnf(c191,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X137)|iext(X137,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c92, c31])).
% 3.46/3.66  cnf(c190,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X136)|iext(X136,uri_rdfs_Seq,uri_rdfs_Container),inference(resolution,[status(thm)],[c91, c31])).
% 3.46/3.66  cnf(c189,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X135)|iext(X135,uri_rdf_XMLLiteral,uri_rdfs_Literal),inference(resolution,[status(thm)],[c90, c31])).
% 3.46/3.66  cnf(c188,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X134)|iext(X134,uri_rdf_XMLLiteral,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c89, c31])).
% 3.46/3.66  cnf(c187,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X133)|iext(X133,uri_rdfs_Datatype,uri_rdfs_Class),inference(resolution,[status(thm)],[c85, c31])).
% 3.46/3.66  cnf(c186,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X132)|iext(X132,uri_rdf_predicate,uri_rdfs_Resource),inference(resolution,[status(thm)],[c31, c50])).
% 3.46/3.66  cnf(c185,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X131)|iext(X131,uri_rdf_subject,uri_rdfs_Resource),inference(resolution,[status(thm)],[c31, c48])).
% 3.46/3.66  cnf(c184,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X130)|iext(X130,uri_rdf_subject,uri_rdfs_Statement),inference(resolution,[status(thm)],[c31, c49])).
% 3.46/3.66  cnf(c183,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X129)|iext(X129,uri_rdf_object,uri_rdfs_Statement),inference(resolution,[status(thm)],[c31, c53])).
% 3.46/3.66  cnf(c182,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X128)|iext(X128,uri_rdfs_subClassOf,uri_rdfs_Class),inference(resolution,[status(thm)],[c31, c39])).
% 3.46/3.66  cnf(c181,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X127)|iext(X127,uri_rdfs_subClassOf,uri_rdfs_Class),inference(resolution,[status(thm)],[c31, c47])).
% 3.46/3.66  cnf(c180,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X126)|iext(X126,uri_ex_p,uri_owl_ObjectProperty),inference(resolution,[status(thm)],[c31, c2])).
% 3.46/3.66  cnf(c179,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X125)|iext(X125,uri_rdf_Property,uri_rdfs_Class),inference(resolution,[status(thm)],[c31, c59])).
% 3.46/3.66  cnf(c178,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X124)|iext(X124,uri_rdfs_range,uri_rdfs_Class),inference(resolution,[status(thm)],[c31, c54])).
% 3.46/3.66  cnf(c177,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X123)|iext(X123,uri_rdf_value,uri_rdfs_Resource),inference(resolution,[status(thm)],[c31, c14])).
% 3.46/3.66  cnf(c176,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_first,X122)|iext(X122,skolem0004,uri_ex_o),inference(resolution,[status(thm)],[c31, c8])).
% 3.46/3.66  cnf(c175,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X121)|iext(X121,uri_rdf_predicate,uri_rdfs_Statement),inference(resolution,[status(thm)],[c31, c51])).
% 3.46/3.66  cnf(c174,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X120)|iext(X120,skolem0004,uri_rdf_nil),inference(resolution,[status(thm)],[c31, c9])).
% 3.46/3.66  cnf(c173,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X119)|iext(X119,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c31, c32])).
% 3.46/3.66  cnf(c172,plain,~iext(uri_rdfs_subPropertyOf,uri_owl_complementOf,X118)|iext(X118,skolem0002,skolem0003),inference(resolution,[status(thm)],[c31, c6])).
% 3.46/3.66  cnf(c171,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X117)|iext(X117,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c31, c24])).
% 3.46/3.66  cnf(c170,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X116)|iext(X116,uri_rdf_type,uri_rdfs_Class),inference(resolution,[status(thm)],[c31, c16])).
% 3.46/3.66  cnf(c169,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X115)|iext(X115,uri_rdfs_range,uri_rdf_Property),inference(resolution,[status(thm)],[c31, c58])).
% 3.46/3.66  cnf(c168,plain,~iext(uri_rdfs_subPropertyOf,uri_owl_oneOf,X114)|iext(X114,skolem0003,skolem0004),inference(resolution,[status(thm)],[c31, c7])).
% 3.46/3.66  cnf(c167,plain,~iext(uri_rdfs_subPropertyOf,uri_owl_allValuesFrom,X113)|iext(X113,skolem0001,skolem0002),inference(resolution,[status(thm)],[c31, c5])).
% 3.46/3.66  cnf(c166,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X112)|iext(X112,uri_rdf_type,uri_rdfs_Resource),inference(resolution,[status(thm)],[c31, c17])).
% 3.46/3.66  cnf(c165,plain,~iext(uri_rdfs_subPropertyOf,uri_owl_onProperty,X111)|iext(X111,skolem0001,uri_ex_p),inference(resolution,[status(thm)],[c31, c4])).
% 3.46/3.66  cnf(c164,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X110)|iext(X110,uri_rdfs_domain,uri_rdfs_Class),inference(resolution,[status(thm)],[c31, c78])).
% 3.46/3.66  cnf(c163,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X109)|iext(X109,uri_ex_s,skolem0001),inference(resolution,[status(thm)],[c31, c3])).
% 3.46/3.66  cnf(c162,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X108)|iext(X108,uri_rdfs_domain,uri_rdf_Property),inference(resolution,[status(thm)],[c31, c84])).
% 3.46/3.66  cnf(c161,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X107)|iext(X107,uri_rdf_value,uri_rdfs_Resource),inference(resolution,[status(thm)],[c31, c15])).
% 3.46/3.66  cnf(c160,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X106)|iext(X106,uri_rdfs_subPropertyOf,X106),inference(factor,[status(thm)],[c31])).
% 3.46/3.66  cnf(c507,plain,icext(uri_rdf_Property,uri_rdf_first),inference(resolution,[status(thm)],[c147, c120])).
% 3.46/3.66  cnf(c502,plain,icext(uri_rdf_List,uri_rdf_nil),inference(resolution,[status(thm)],[c146, c120])).
% 3.46/3.66  cnf(c494,plain,icext(uri_rdf_Property,uri_rdf_rest),inference(resolution,[status(thm)],[c145, c120])).
% 3.46/3.66  cnf(c486,plain,icext(uri_rdf_Property,uri_rdf__1),inference(resolution,[status(thm)],[c144, c120])).
% 3.46/3.66  cnf(c478,plain,icext(uri_rdf_Property,uri_rdf__2),inference(resolution,[status(thm)],[c143, c120])).
% 3.46/3.66  cnf(c470,plain,icext(uri_rdf_Property,uri_rdf__3),inference(resolution,[status(thm)],[c142, c120])).
% 3.46/3.66  cnf(c462,plain,icext(uri_rdf_Property,uri_rdf_object),inference(resolution,[status(thm)],[c141, c120])).
% 3.46/3.66  cnf(c450,plain,icext(uri_rdf_Property,uri_rdf_value),inference(resolution,[status(thm)],[c140, c120])).
% 3.46/3.66  cnf(c443,plain,icext(uri_rdf_Property,uri_rdf_subject),inference(resolution,[status(thm)],[c139, c120])).
% 3.46/3.66  cnf(c436,plain,icext(uri_rdf_Property,uri_rdf_type),inference(resolution,[status(thm)],[c131, c120])).
% 3.46/3.66  cnf(c396,plain,icext(uri_owl_ObjectProperty,uri_ex_p),inference(resolution,[status(thm)],[c120, c2])).
% 3.46/3.66  cnf(c393,plain,icext(uri_rdfs_Datatype,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c120, c89])).
% 3.46/3.66  cnf(c392,plain,icext(skolem0001,uri_ex_s),inference(resolution,[status(thm)],[c120, c3])).
% 3.46/3.66  fof(rdfs_datatype_instsub_literal,axiom,(![D]:(icext(uri_rdfs_Datatype,D)=>iext(uri_rdfs_subClassOf,D,uri_rdfs_Literal))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_datatype_instsub_literal)).
% 3.46/3.66  fof(c86,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.46/3.66  fof(c87,plain,(![X36]:(~icext(uri_rdfs_Datatype,X36)|iext(uri_rdfs_subClassOf,X36,uri_rdfs_Literal))),inference(variable_rename,[status(thm)],[c86])).
% 3.46/3.66  cnf(c88,plain,~icext(uri_rdfs_Datatype,X91)|iext(uri_rdfs_subClassOf,X91,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[c87])).
% 3.46/3.66  cnf(c327,plain,icext(uri_rdfs_Class,uri_rdf_Property),inference(resolution,[status(thm)],[c279, c76])).
% 3.46/3.66  fof(rdfs_lv_def,axiom,(![X]:(lv(X)<=>icext(uri_rdfs_Literal,X))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_lv_def)).
% 3.46/3.66  fof(c60,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.46/3.66  fof(c61,plain,((![X]:(~lv(X)|icext(uri_rdfs_Literal,X)))&(![X]:(~icext(uri_rdfs_Literal,X)|lv(X)))),inference(shift_quantors,[status(thm)],[c60])).
% 3.46/3.66  fof(c63,plain,(![X26]:(![X27]:((~lv(X26)|icext(uri_rdfs_Literal,X26))&(~icext(uri_rdfs_Literal,X27)|lv(X27))))),inference(shift_quantors,[status(thm)],[fof(c62,plain,((![X26]:(~lv(X26)|icext(uri_rdfs_Literal,X26)))&(![X27]:(~icext(uri_rdfs_Literal,X27)|lv(X27)))),inference(variable_rename,[status(thm)],[c61])).])).
% 3.46/3.66  cnf(c65,plain,~icext(uri_rdfs_Literal,X60)|lv(X60),inference(split_conjunct,[status(thm)],[c63])).
% 3.46/3.66  cnf(c64,plain,~lv(X59)|icext(uri_rdfs_Literal,X59),inference(split_conjunct,[status(thm)],[c63])).
% 3.46/3.66  fof(testcase_conclusion_fullish_010_Negative_Property_Assertions,conjecture,(?[BNODE_z]:(((iext(uri_rdf_type,BNODE_z,uri_owl_NegativePropertyAssertion)&iext(uri_owl_sourceIndividual,BNODE_z,uri_ex_s))&iext(uri_owl_assertionProperty,BNODE_z,uri_ex_p))&iext(uri_owl_targetIndividual,BNODE_z,uri_ex_o))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', testcase_conclusion_fullish_010_Negative_Property_Assertions)).
% 3.46/3.66  fof(c10,negated_conjecture,(~(?[BNODE_z]:(((iext(uri_rdf_type,BNODE_z,uri_owl_NegativePropertyAssertion)&iext(uri_owl_sourceIndividual,BNODE_z,uri_ex_s))&iext(uri_owl_assertionProperty,BNODE_z,uri_ex_p))&iext(uri_owl_targetIndividual,BNODE_z,uri_ex_o)))),inference(assume_negation,[status(cth)],[testcase_conclusion_fullish_010_Negative_Property_Assertions])).
% 3.46/3.66  fof(c11,negated_conjecture,(![BNODE_z]:(((~iext(uri_rdf_type,BNODE_z,uri_owl_NegativePropertyAssertion)|~iext(uri_owl_sourceIndividual,BNODE_z,uri_ex_s))|~iext(uri_owl_assertionProperty,BNODE_z,uri_ex_p))|~iext(uri_owl_targetIndividual,BNODE_z,uri_ex_o))),inference(fof_nnf,[status(thm)],[c10])).
% 3.46/3.66  fof(c12,negated_conjecture,(![X6]:(((~iext(uri_rdf_type,X6,uri_owl_NegativePropertyAssertion)|~iext(uri_owl_sourceIndividual,X6,uri_ex_s))|~iext(uri_owl_assertionProperty,X6,uri_ex_p))|~iext(uri_owl_targetIndividual,X6,uri_ex_o))),inference(variable_rename,[status(thm)],[c11])).
% 3.46/3.66  cnf(c13,negated_conjecture,~iext(uri_rdf_type,X52,uri_owl_NegativePropertyAssertion)|~iext(uri_owl_sourceIndividual,X52,uri_ex_s)|~iext(uri_owl_assertionProperty,X52,uri_ex_p)|~iext(uri_owl_targetIndividual,X52,uri_ex_o),inference(split_conjunct,[status(thm)],[c12])).
% 3.46/3.66  % SZS output end Saturation
% 3.46/3.66  
% 3.46/3.66  % Initial clauses    : 98
% 3.46/3.66  % Processed clauses  : 592
% 3.46/3.66  % Factors computed   : 5
% 3.46/3.66  % Resolvents computed: 1381
% 3.46/3.66  % Tautologies deleted: 55
% 3.46/3.66  % Forward subsumed   : 837
% 3.46/3.66  % Backward subsumed  : 1
% 3.46/3.66  % -------- CPU Time ---------
% 3.46/3.66  % User time          : 3.281 s
% 3.46/3.66  % System time        : 0.020 s
% 3.46/3.66  % Total time         : 3.301 s
%------------------------------------------------------------------------------