PyRes---1.5.CSA-Sat.s

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

% Computer : n013.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.33s 3.60s
% Output   : Saturation 3.43s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12  % Problem  : SWB009+4 : TPTP v8.1.2. Released v5.2.0.
% 0.07/0.13  % Command  : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34  % Computer : n013.cluster.edu
% 0.13/0.34  % Model    : x86_64 x86_64
% 0.13/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34  % Memory   : 8042.1875MB
% 0.13/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34  % CPULimit : 300
% 0.13/0.34  % WCLimit  : 300
% 0.13/0.34  % DateTime : Wed May  8 22:10:53 EDT 2024
% 0.13/0.35  % CPUTime  : 
% 3.33/3.60  % Version:  1.5
% 3.33/3.60  % SZS status CounterSatisfiable
% 3.33/3.60  % SZS output start Saturation
% 3.33/3.60  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.33/3.60  fof(c23,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.33/3.60  fof(c25,plain,(![X8]:(![X9]:(![X10]:(![X11]:(~iext(uri_rdfs_subPropertyOf,X8,X9)|((ip(X8)&ip(X9))&(~iext(X8,X10,X11)|iext(X9,X10,X11)))))))),inference(shift_quantors,[status(thm)],[fof(c24,plain,(![X8]:(![X9]:(~iext(uri_rdfs_subPropertyOf,X8,X9)|((ip(X8)&ip(X9))&(![X10]:(![X11]:(~iext(X8,X10,X11)|iext(X9,X10,X11)))))))),inference(variable_rename,[status(thm)],[c23])).])).
% 3.33/3.60  fof(c26,plain,(![X8]:(![X9]:(![X10]:(![X11]:(((~iext(uri_rdfs_subPropertyOf,X8,X9)|ip(X8))&(~iext(uri_rdfs_subPropertyOf,X8,X9)|ip(X9)))&(~iext(uri_rdfs_subPropertyOf,X8,X9)|(~iext(X8,X10,X11)|iext(X9,X10,X11)))))))),inference(distribute,[status(thm)],[c25])).
% 3.33/3.60  cnf(c29,plain,~iext(uri_rdfs_subPropertyOf,X66,X65)|~iext(X66,X67,X68)|iext(X65,X67,X68),inference(split_conjunct,[status(thm)],[c26])).
% 3.33/3.60  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.33/3.60  fof(c19,plain,(![P]:(~ip(P)|iext(uri_rdfs_subPropertyOf,P,P))),inference(fof_nnf,[status(thm)],[rdfs_subpropertyof_reflex])).
% 3.33/3.60  fof(c20,plain,(![X7]:(~ip(X7)|iext(uri_rdfs_subPropertyOf,X7,X7))),inference(variable_rename,[status(thm)],[c19])).
% 3.33/3.60  cnf(c21,plain,~ip(X53)|iext(uri_rdfs_subPropertyOf,X53,X53),inference(split_conjunct,[status(thm)],[c20])).
% 3.33/3.60  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.33/3.60  fof(c131,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.33/3.60  fof(c132,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)],[c131])).
% 3.33/3.60  fof(c134,plain,(![X40]:(![X41]:((~iext(uri_rdf_type,X40,uri_rdf_Property)|ip(X40))&(~ip(X41)|iext(uri_rdf_type,X41,uri_rdf_Property))))),inference(shift_quantors,[status(thm)],[fof(c133,plain,((![X40]:(~iext(uri_rdf_type,X40,uri_rdf_Property)|ip(X40)))&(![X41]:(~ip(X41)|iext(uri_rdf_type,X41,uri_rdf_Property)))),inference(variable_rename,[status(thm)],[c132])).])).
% 3.33/3.60  cnf(c135,plain,~iext(uri_rdf_type,X97,uri_rdf_Property)|ip(X97),inference(split_conjunct,[status(thm)],[c134])).
% 3.33/3.60  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.33/3.60  fof(c114,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.33/3.60  fof(c115,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)],[c114])).
% 3.33/3.60  fof(c117,plain,(![X36]:(![X37]:(![X38]:(![X39]:((~iext(uri_rdf_type,X36,X37)|icext(X37,X36))&(~icext(X39,X38)|iext(uri_rdf_type,X38,X39))))))),inference(shift_quantors,[status(thm)],[fof(c116,plain,((![X36]:(![X37]:(~iext(uri_rdf_type,X36,X37)|icext(X37,X36))))&(![X38]:(![X39]:(~icext(X39,X38)|iext(uri_rdf_type,X38,X39))))),inference(variable_rename,[status(thm)],[c115])).])).
% 3.33/3.60  cnf(c119,plain,~icext(X94,X93)|iext(uri_rdf_type,X93,X94),inference(split_conjunct,[status(thm)],[c117])).
% 3.33/3.60  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.33/3.60  cnf(c56,plain,iext(uri_rdfs_domain,uri_rdfs_range,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_range_domain])).
% 3.33/3.60  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.33/3.60  fof(c77,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.33/3.60  fof(c78,plain,(![P]:(![C]:(![X]:((~iext(uri_rdfs_domain,P,C)|(![Y]:~iext(P,X,Y)))|icext(C,X))))),inference(shift_quantors,[status(thm)],[c77])).
% 3.33/3.60  fof(c80,plain,(![X29]:(![X30]:(![X31]:(![X32]:((~iext(uri_rdfs_domain,X29,X30)|~iext(X29,X31,X32))|icext(X30,X31)))))),inference(shift_quantors,[status(thm)],[fof(c79,plain,(![X29]:(![X30]:(![X31]:((~iext(uri_rdfs_domain,X29,X30)|(![X32]:~iext(X29,X31,X32)))|icext(X30,X31))))),inference(variable_rename,[status(thm)],[c78])).])).
% 3.33/3.60  cnf(c81,plain,~iext(uri_rdfs_domain,X85,X86)|~iext(X85,X84,X87)|icext(X86,X84),inference(split_conjunct,[status(thm)],[c80])).
% 3.33/3.60  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.33/3.60  cnf(c127,plain,iext(uri_rdfs_range,uri_rdfs_comment,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[rdfs_annotation_comment_range])).
% 3.33/3.60  cnf(c426,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X314)|icext(X314,uri_rdfs_comment),inference(resolution,[status(thm)],[c127, c81])).
% 3.33/3.60  cnf(c1344,plain,icext(uri_rdf_Property,uri_rdfs_comment),inference(resolution,[status(thm)],[c426, c56])).
% 3.33/3.60  cnf(c1346,plain,iext(uri_rdf_type,uri_rdfs_comment,uri_rdf_Property),inference(resolution,[status(thm)],[c1344, c119])).
% 3.33/3.60  cnf(c1352,plain,ip(uri_rdfs_comment),inference(resolution,[status(thm)],[c1346, c135])).
% 3.33/3.60  cnf(c1354,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_comment,uri_rdfs_comment),inference(resolution,[status(thm)],[c1352, c21])).
% 3.33/3.60  cnf(c1359,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X666)|iext(X666,uri_rdfs_comment,uri_rdfs_comment),inference(resolution,[status(thm)],[c1354, c29])).
% 3.33/3.60  cnf(c1349,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X664)|iext(X664,uri_rdfs_comment,uri_rdf_Property),inference(resolution,[status(thm)],[c1346, c29])).
% 3.33/3.60  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.33/3.60  cnf(c122,plain,iext(uri_rdfs_range,uri_rdfs_label,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[rdfs_annotation_label_range])).
% 3.33/3.60  cnf(c360,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X298)|icext(X298,uri_rdfs_label),inference(resolution,[status(thm)],[c122, c81])).
% 3.33/3.60  cnf(c1315,plain,icext(uri_rdf_Property,uri_rdfs_label),inference(resolution,[status(thm)],[c360, c56])).
% 3.33/3.60  cnf(c1316,plain,iext(uri_rdf_type,uri_rdfs_label,uri_rdf_Property),inference(resolution,[status(thm)],[c1315, c119])).
% 3.33/3.60  cnf(c1322,plain,ip(uri_rdfs_label),inference(resolution,[status(thm)],[c1316, c135])).
% 3.33/3.60  cnf(c1325,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_label,uri_rdfs_label),inference(resolution,[status(thm)],[c1322, c21])).
% 3.33/3.60  cnf(c1330,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X663)|iext(X663,uri_rdfs_label,uri_rdfs_label),inference(resolution,[status(thm)],[c1325, c29])).
% 3.33/3.60  cnf(c1319,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X661)|iext(X661,uri_rdfs_label,uri_rdf_Property),inference(resolution,[status(thm)],[c1316, c29])).
% 3.33/3.60  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.33/3.60  fof(c34,plain,(![C]:(~ic(C)|iext(uri_rdfs_subClassOf,C,C))),inference(fof_nnf,[status(thm)],[rdfs_subclassof_reflex])).
% 3.33/3.60  fof(c35,plain,(![X15]:(~ic(X15)|iext(uri_rdfs_subClassOf,X15,X15))),inference(variable_rename,[status(thm)],[c34])).
% 3.33/3.60  cnf(c36,plain,~ic(X72)|iext(uri_rdfs_subClassOf,X72,X72),inference(split_conjunct,[status(thm)],[c35])).
% 3.33/3.60  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.33/3.60  fof(c70,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.33/3.60  fof(c71,plain,((![X]:(~ic(X)|icext(uri_rdfs_Class,X)))&(![X]:(~icext(uri_rdfs_Class,X)|ic(X)))),inference(shift_quantors,[status(thm)],[c70])).
% 3.33/3.60  fof(c73,plain,(![X27]:(![X28]:((~ic(X27)|icext(uri_rdfs_Class,X27))&(~icext(uri_rdfs_Class,X28)|ic(X28))))),inference(shift_quantors,[status(thm)],[fof(c72,plain,((![X27]:(~ic(X27)|icext(uri_rdfs_Class,X27)))&(![X28]:(~icext(uri_rdfs_Class,X28)|ic(X28)))),inference(variable_rename,[status(thm)],[c71])).])).
% 3.33/3.60  cnf(c75,plain,~icext(uri_rdfs_Class,X64)|ic(X64),inference(split_conjunct,[status(thm)],[c73])).
% 3.33/3.60  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.33/3.60  cnf(c52,plain,iext(uri_rdfs_range,uri_rdfs_range,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_range_range])).
% 3.33/3.60  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.33/3.60  fof(c53,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.33/3.60  fof(c54,plain,(![X19]:(![X20]:(![X21]:(![X22]:((~iext(uri_rdfs_range,X19,X20)|~iext(X19,X21,X22))|icext(X20,X22)))))),inference(variable_rename,[status(thm)],[c53])).
% 3.33/3.60  cnf(c55,plain,~iext(uri_rdfs_range,X82,X80)|~iext(X82,X81,X83)|icext(X80,X83),inference(split_conjunct,[status(thm)],[c54])).
% 3.33/3.60  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.33/3.60  cnf(c107,plain,iext(uri_rdfs_range,uri_rdf_rest,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdfs_collection_rest_range])).
% 3.33/3.60  cnf(c343,plain,~iext(uri_rdfs_range,uri_rdfs_range,X280)|icext(X280,uri_rdf_List),inference(resolution,[status(thm)],[c107, c55])).
% 3.33/3.60  cnf(c1277,plain,icext(uri_rdfs_Class,uri_rdf_List),inference(resolution,[status(thm)],[c343, c52])).
% 3.33/3.60  cnf(c1278,plain,ic(uri_rdf_List),inference(resolution,[status(thm)],[c1277, c75])).
% 3.33/3.60  cnf(c1282,plain,iext(uri_rdfs_subClassOf,uri_rdf_List,uri_rdf_List),inference(resolution,[status(thm)],[c1278, c36])).
% 3.33/3.60  cnf(c1300,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X659)|iext(X659,uri_rdf_List,uri_rdf_List),inference(resolution,[status(thm)],[c1282, c29])).
% 3.33/3.60  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.33/3.60  fof(c31,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.33/3.60  fof(c32,plain,(![X12]:(![X13]:(![X14]:((~iext(uri_rdfs_subClassOf,X12,X13)|~iext(uri_rdfs_subClassOf,X13,X14))|iext(uri_rdfs_subClassOf,X12,X14))))),inference(variable_rename,[status(thm)],[c31])).
% 3.33/3.60  cnf(c33,plain,~iext(uri_rdfs_subClassOf,X70,X69)|~iext(uri_rdfs_subClassOf,X69,X71)|iext(uri_rdfs_subClassOf,X70,X71),inference(split_conjunct,[status(thm)],[c32])).
% 3.33/3.60  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.33/3.60  fof(c111,plain,(![C]:(~ic(C)|iext(uri_rdfs_subClassOf,C,uri_rdfs_Resource))),inference(fof_nnf,[status(thm)],[rdfs_class_instsub_resource])).
% 3.33/3.60  fof(c112,plain,(![X35]:(~ic(X35)|iext(uri_rdfs_subClassOf,X35,uri_rdfs_Resource))),inference(variable_rename,[status(thm)],[c111])).
% 3.33/3.60  cnf(c113,plain,~ic(X90)|iext(uri_rdfs_subClassOf,X90,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[c112])).
% 3.33/3.60  cnf(c1281,plain,iext(uri_rdfs_subClassOf,uri_rdf_List,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1278, c113])).
% 3.33/3.60  cnf(c1293,plain,~iext(uri_rdfs_subClassOf,X658,uri_rdf_List)|iext(uri_rdfs_subClassOf,X658,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1281, c33])).
% 3.33/3.60  cnf(c1291,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X657)|iext(X657,uri_rdf_List,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1281, c29])).
% 3.33/3.60  cnf(c1279,plain,iext(uri_rdf_type,uri_rdf_List,uri_rdfs_Class),inference(resolution,[status(thm)],[c1277, c119])).
% 3.33/3.60  cnf(c1286,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X656)|iext(X656,uri_rdf_List,uri_rdfs_Class),inference(resolution,[status(thm)],[c1279, c29])).
% 3.33/3.60  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.33/3.60  cnf(c82,plain,iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_domain_domain])).
% 3.33/3.60  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.33/3.60  cnf(c49,plain,iext(uri_rdfs_domain,uri_rdf_predicate,uri_rdfs_Statement),inference(split_conjunct,[status(thm)],[rdfs_reification_predicate_domain])).
% 3.33/3.60  cnf(c291,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X227)|icext(X227,uri_rdf_predicate),inference(resolution,[status(thm)],[c81, c49])).
% 3.33/3.60  cnf(c1229,plain,icext(uri_rdf_Property,uri_rdf_predicate),inference(resolution,[status(thm)],[c291, c82])).
% 3.33/3.60  cnf(c1230,plain,iext(uri_rdf_type,uri_rdf_predicate,uri_rdf_Property),inference(resolution,[status(thm)],[c1229, c119])).
% 3.33/3.60  cnf(c1236,plain,ip(uri_rdf_predicate),inference(resolution,[status(thm)],[c1230, c135])).
% 3.33/3.60  cnf(c1238,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_predicate,uri_rdf_predicate),inference(resolution,[status(thm)],[c1236, c21])).
% 3.33/3.60  cnf(c1243,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X655)|iext(X655,uri_rdf_predicate,uri_rdf_predicate),inference(resolution,[status(thm)],[c1238, c29])).
% 3.33/3.60  cnf(c1233,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X653)|iext(X653,uri_rdf_predicate,uri_rdf_Property),inference(resolution,[status(thm)],[c1230, c29])).
% 3.33/3.60  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.33/3.60  cnf(c14,plain,iext(uri_rdfs_range,uri_rdf_type,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_type_range])).
% 3.33/3.60  fof(testcase_premise_fullish_009_Existential_Restriction_Entailments,axiom,(?[BNODE_z]:(((((iext(uri_rdf_type,uri_ex_p,uri_owl_ObjectProperty)&iext(uri_rdf_type,uri_ex_c,uri_owl_Class))&iext(uri_rdf_type,uri_ex_s,BNODE_z))&iext(uri_rdf_type,BNODE_z,uri_owl_Restriction))&iext(uri_owl_onProperty,BNODE_z,uri_ex_p))&iext(uri_owl_someValuesFrom,BNODE_z,uri_ex_c))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', testcase_premise_fullish_009_Existential_Restriction_Entailments)).
% 3.33/3.60  fof(c0,plain,(?[X2]:(((((iext(uri_rdf_type,uri_ex_p,uri_owl_ObjectProperty)&iext(uri_rdf_type,uri_ex_c,uri_owl_Class))&iext(uri_rdf_type,uri_ex_s,X2))&iext(uri_rdf_type,X2,uri_owl_Restriction))&iext(uri_owl_onProperty,X2,uri_ex_p))&iext(uri_owl_someValuesFrom,X2,uri_ex_c))),inference(variable_rename,[status(thm)],[testcase_premise_fullish_009_Existential_Restriction_Entailments])).
% 3.33/3.60  fof(c1,plain,(((((iext(uri_rdf_type,uri_ex_p,uri_owl_ObjectProperty)&iext(uri_rdf_type,uri_ex_c,uri_owl_Class))&iext(uri_rdf_type,uri_ex_s,skolem0001))&iext(uri_rdf_type,skolem0001,uri_owl_Restriction))&iext(uri_owl_onProperty,skolem0001,uri_ex_p))&iext(uri_owl_someValuesFrom,skolem0001,uri_ex_c)),inference(skolemize,[status(esa)],[c0])).
% 3.33/3.60  cnf(c2,plain,iext(uri_rdf_type,uri_ex_p,uri_owl_ObjectProperty),inference(split_conjunct,[status(thm)],[c1])).
% 3.33/3.60  cnf(c271,plain,~iext(uri_rdfs_range,uri_rdf_type,X185)|icext(X185,uri_owl_ObjectProperty),inference(resolution,[status(thm)],[c55, c2])).
% 3.33/3.60  cnf(c1131,plain,icext(uri_rdfs_Class,uri_owl_ObjectProperty),inference(resolution,[status(thm)],[c271, c14])).
% 3.33/3.60  cnf(c1132,plain,ic(uri_owl_ObjectProperty),inference(resolution,[status(thm)],[c1131, c75])).
% 3.33/3.60  cnf(c1136,plain,iext(uri_rdfs_subClassOf,uri_owl_ObjectProperty,uri_owl_ObjectProperty),inference(resolution,[status(thm)],[c1132, c36])).
% 3.33/3.60  cnf(c1218,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X651)|iext(X651,uri_owl_ObjectProperty,uri_owl_ObjectProperty),inference(resolution,[status(thm)],[c1136, c29])).
% 3.33/3.60  cnf(c1135,plain,iext(uri_rdfs_subClassOf,uri_owl_ObjectProperty,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1132, c113])).
% 3.33/3.60  cnf(c1212,plain,~iext(uri_rdfs_subClassOf,X650,uri_owl_ObjectProperty)|iext(uri_rdfs_subClassOf,X650,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1135, c33])).
% 3.33/3.60  cnf(c1210,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X649)|iext(X649,uri_owl_ObjectProperty,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1135, c29])).
% 3.33/3.60  cnf(c1133,plain,iext(uri_rdf_type,uri_owl_ObjectProperty,uri_rdfs_Class),inference(resolution,[status(thm)],[c1131, c119])).
% 3.33/3.60  cnf(c1205,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X648)|iext(X648,uri_owl_ObjectProperty,uri_rdfs_Class),inference(resolution,[status(thm)],[c1133, c29])).
% 3.33/3.60  cnf(c4,plain,iext(uri_rdf_type,uri_ex_s,skolem0001),inference(split_conjunct,[status(thm)],[c1])).
% 3.33/3.60  cnf(c260,plain,~iext(uri_rdfs_range,uri_rdf_type,X174)|icext(X174,skolem0001),inference(resolution,[status(thm)],[c55, c4])).
% 3.33/3.60  cnf(c1100,plain,icext(uri_rdfs_Class,skolem0001),inference(resolution,[status(thm)],[c260, c14])).
% 3.33/3.60  cnf(c1101,plain,ic(skolem0001),inference(resolution,[status(thm)],[c1100, c75])).
% 3.33/3.60  cnf(c1105,plain,iext(uri_rdfs_subClassOf,skolem0001,skolem0001),inference(resolution,[status(thm)],[c1101, c36])).
% 3.33/3.60  cnf(c1197,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X646)|iext(X646,skolem0001,skolem0001),inference(resolution,[status(thm)],[c1105, c29])).
% 3.33/3.60  cnf(c1104,plain,iext(uri_rdfs_subClassOf,skolem0001,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1101, c113])).
% 3.33/3.60  cnf(c1191,plain,~iext(uri_rdfs_subClassOf,X645,skolem0001)|iext(uri_rdfs_subClassOf,X645,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1104, c33])).
% 3.33/3.60  cnf(c1189,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X644)|iext(X644,skolem0001,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1104, c29])).
% 3.33/3.60  cnf(c1102,plain,iext(uri_rdf_type,skolem0001,uri_rdfs_Class),inference(resolution,[status(thm)],[c1100, c119])).
% 3.33/3.60  cnf(c1184,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X643)|iext(X643,skolem0001,uri_rdfs_Class),inference(resolution,[status(thm)],[c1102, c29])).
% 3.33/3.60  cnf(c5,plain,iext(uri_rdf_type,skolem0001,uri_owl_Restriction),inference(split_conjunct,[status(thm)],[c1])).
% 3.33/3.60  cnf(c254,plain,~iext(uri_rdfs_range,uri_rdf_type,X168)|icext(X168,uri_owl_Restriction),inference(resolution,[status(thm)],[c55, c5])).
% 3.33/3.60  cnf(c1064,plain,icext(uri_rdfs_Class,uri_owl_Restriction),inference(resolution,[status(thm)],[c254, c14])).
% 3.33/3.60  cnf(c1065,plain,ic(uri_owl_Restriction),inference(resolution,[status(thm)],[c1064, c75])).
% 3.33/3.60  cnf(c1069,plain,iext(uri_rdfs_subClassOf,uri_owl_Restriction,uri_owl_Restriction),inference(resolution,[status(thm)],[c1065, c36])).
% 3.33/3.60  cnf(c1176,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X641)|iext(X641,uri_owl_Restriction,uri_owl_Restriction),inference(resolution,[status(thm)],[c1069, c29])).
% 3.33/3.60  cnf(c1068,plain,iext(uri_rdfs_subClassOf,uri_owl_Restriction,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1065, c113])).
% 3.33/3.60  cnf(c1169,plain,~iext(uri_rdfs_subClassOf,X640,uri_owl_Restriction)|iext(uri_rdfs_subClassOf,X640,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1068, c33])).
% 3.33/3.60  cnf(c1167,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X639)|iext(X639,uri_owl_Restriction,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1068, c29])).
% 3.33/3.60  cnf(c1066,plain,iext(uri_rdf_type,uri_owl_Restriction,uri_rdfs_Class),inference(resolution,[status(thm)],[c1064, c119])).
% 3.33/3.60  cnf(c1162,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X638)|iext(X638,uri_owl_Restriction,uri_rdfs_Class),inference(resolution,[status(thm)],[c1066, c29])).
% 3.33/3.60  cnf(c3,plain,iext(uri_rdf_type,uri_ex_c,uri_owl_Class),inference(split_conjunct,[status(thm)],[c1])).
% 3.33/3.60  cnf(c251,plain,~iext(uri_rdfs_range,uri_rdf_type,X165)|icext(X165,uri_owl_Class),inference(resolution,[status(thm)],[c55, c3])).
% 3.33/3.60  cnf(c1035,plain,icext(uri_rdfs_Class,uri_owl_Class),inference(resolution,[status(thm)],[c251, c14])).
% 3.33/3.60  cnf(c1036,plain,ic(uri_owl_Class),inference(resolution,[status(thm)],[c1035, c75])).
% 3.33/3.60  cnf(c1040,plain,iext(uri_rdfs_subClassOf,uri_owl_Class,uri_owl_Class),inference(resolution,[status(thm)],[c1036, c36])).
% 3.33/3.60  cnf(c1153,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X636)|iext(X636,uri_owl_Class,uri_owl_Class),inference(resolution,[status(thm)],[c1040, c29])).
% 3.33/3.60  cnf(c1039,plain,iext(uri_rdfs_subClassOf,uri_owl_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1036, c113])).
% 3.33/3.60  cnf(c1146,plain,~iext(uri_rdfs_subClassOf,X635,uri_owl_Class)|iext(uri_rdfs_subClassOf,X635,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1039, c33])).
% 3.33/3.60  cnf(c1144,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X634)|iext(X634,uri_owl_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1039, c29])).
% 3.33/3.60  cnf(c1037,plain,iext(uri_rdf_type,uri_owl_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c1035, c119])).
% 3.33/3.60  cnf(c1139,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X633)|iext(X633,uri_owl_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c1037, c29])).
% 3.33/3.60  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.33/3.60  cnf(c76,plain,iext(uri_rdfs_range,uri_rdfs_domain,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_domain_range])).
% 3.33/3.60  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.33/3.60  cnf(c47,plain,iext(uri_rdfs_domain,uri_rdf_subject,uri_rdfs_Statement),inference(split_conjunct,[status(thm)],[rdfs_reification_subject_domain])).
% 3.33/3.60  cnf(c246,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X160)|icext(X160,uri_rdfs_Statement),inference(resolution,[status(thm)],[c55, c47])).
% 3.33/3.60  cnf(c980,plain,icext(uri_rdfs_Class,uri_rdfs_Statement),inference(resolution,[status(thm)],[c246, c76])).
% 3.33/3.60  cnf(c981,plain,ic(uri_rdfs_Statement),inference(resolution,[status(thm)],[c980, c75])).
% 3.33/3.60  cnf(c985,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Statement,uri_rdfs_Statement),inference(resolution,[status(thm)],[c981, c36])).
% 3.33/3.60  cnf(c1123,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X631)|iext(X631,uri_rdfs_Statement,uri_rdfs_Statement),inference(resolution,[status(thm)],[c985, c29])).
% 3.33/3.60  cnf(c984,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Statement,uri_rdfs_Resource),inference(resolution,[status(thm)],[c981, c113])).
% 3.33/3.60  cnf(c1117,plain,~iext(uri_rdfs_subClassOf,X630,uri_rdfs_Statement)|iext(uri_rdfs_subClassOf,X630,uri_rdfs_Resource),inference(resolution,[status(thm)],[c984, c33])).
% 3.33/3.60  cnf(c1115,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X629)|iext(X629,uri_rdfs_Statement,uri_rdfs_Resource),inference(resolution,[status(thm)],[c984, c29])).
% 3.33/3.60  cnf(c982,plain,iext(uri_rdf_type,uri_rdfs_Statement,uri_rdfs_Class),inference(resolution,[status(thm)],[c980, c119])).
% 3.33/3.60  cnf(c1110,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X628)|iext(X628,uri_rdfs_Statement,uri_rdfs_Class),inference(resolution,[status(thm)],[c982, c29])).
% 3.33/3.60  cnf(c28,plain,~iext(uri_rdfs_subPropertyOf,X63,X62)|ip(X62),inference(split_conjunct,[status(thm)],[c26])).
% 3.33/3.60  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.33/3.60  fof(c102,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.33/3.60  fof(c103,plain,(![X34]:(~icext(uri_rdfs_ContainerMembershipProperty,X34)|iext(uri_rdfs_subPropertyOf,X34,uri_rdfs_member))),inference(variable_rename,[status(thm)],[c102])).
% 3.33/3.60  cnf(c104,plain,~icext(uri_rdfs_ContainerMembershipProperty,X89)|iext(uri_rdfs_subPropertyOf,X89,uri_rdfs_member),inference(split_conjunct,[status(thm)],[c103])).
% 3.33/3.60  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.33/3.60  cnf(c91,plain,iext(uri_rdf_type,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),inference(split_conjunct,[status(thm)],[rdfs_container_n_type_002])).
% 3.33/3.60  cnf(c118,plain,~iext(uri_rdf_type,X92,X91)|icext(X91,X92),inference(split_conjunct,[status(thm)],[c117])).
% 3.33/3.60  cnf(c390,plain,icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__2),inference(resolution,[status(thm)],[c118, c91])).
% 3.33/3.60  cnf(c399,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__2,uri_rdfs_member),inference(resolution,[status(thm)],[c390, c104])).
% 3.33/3.60  cnf(c774,plain,ip(uri_rdfs_member),inference(resolution,[status(thm)],[c399, c28])).
% 3.33/3.60  cnf(c776,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_member,uri_rdfs_member),inference(resolution,[status(thm)],[c774, c21])).
% 3.33/3.60  cnf(c1095,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X627)|iext(X627,uri_rdfs_member,uri_rdfs_member),inference(resolution,[status(thm)],[c776, c29])).
% 3.33/3.60  cnf(c136,plain,~ip(X98)|iext(uri_rdf_type,X98,uri_rdf_Property),inference(split_conjunct,[status(thm)],[c134])).
% 3.33/3.60  cnf(c775,plain,iext(uri_rdf_type,uri_rdfs_member,uri_rdf_Property),inference(resolution,[status(thm)],[c774, c136])).
% 3.33/3.60  cnf(c1087,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X625)|iext(X625,uri_rdfs_member,uri_rdf_Property),inference(resolution,[status(thm)],[c775, c29])).
% 3.33/3.60  cnf(c74,plain,~ic(X61)|icext(uri_rdfs_Class,X61),inference(split_conjunct,[status(thm)],[c73])).
% 3.33/3.60  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.33/3.60  fof(c38,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.33/3.60  fof(c40,plain,(![X16]:(![X17]:(![X18]:(~iext(uri_rdfs_subClassOf,X16,X17)|((ic(X16)&ic(X17))&(~icext(X16,X18)|icext(X17,X18))))))),inference(shift_quantors,[status(thm)],[fof(c39,plain,(![X16]:(![X17]:(~iext(uri_rdfs_subClassOf,X16,X17)|((ic(X16)&ic(X17))&(![X18]:(~icext(X16,X18)|icext(X17,X18))))))),inference(variable_rename,[status(thm)],[c38])).])).
% 3.33/3.60  fof(c41,plain,(![X16]:(![X17]:(![X18]:(((~iext(uri_rdfs_subClassOf,X16,X17)|ic(X16))&(~iext(uri_rdfs_subClassOf,X16,X17)|ic(X17)))&(~iext(uri_rdfs_subClassOf,X16,X17)|(~icext(X16,X18)|icext(X17,X18))))))),inference(distribute,[status(thm)],[c40])).
% 3.33/3.60  cnf(c43,plain,~iext(uri_rdfs_subClassOf,X75,X76)|ic(X76),inference(split_conjunct,[status(thm)],[c41])).
% 3.33/3.60  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.33/3.60  cnf(c101,plain,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_container_containermembershipproperty_sub])).
% 3.33/3.60  cnf(c42,plain,~iext(uri_rdfs_subClassOf,X73,X74)|ic(X73),inference(split_conjunct,[status(thm)],[c41])).
% 3.33/3.60  cnf(c209,plain,ic(uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c42, c101])).
% 3.33/3.60  cnf(c366,plain,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Resource),inference(resolution,[status(thm)],[c113, c209])).
% 3.33/3.60  cnf(c674,plain,ic(uri_rdfs_Resource),inference(resolution,[status(thm)],[c366, c43])).
% 3.33/3.60  cnf(c677,plain,icext(uri_rdfs_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c674, c74])).
% 3.33/3.60  cnf(c681,plain,iext(uri_rdf_type,uri_rdfs_Resource,uri_rdfs_Class),inference(resolution,[status(thm)],[c677, c119])).
% 3.33/3.60  cnf(c1081,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X624)|iext(X624,uri_rdfs_Resource,uri_rdfs_Class),inference(resolution,[status(thm)],[c681, c29])).
% 3.33/3.60  cnf(c678,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Resource,uri_rdfs_Resource),inference(resolution,[status(thm)],[c674, c113])).
% 3.33/3.60  cnf(c1072,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X622)|iext(X622,uri_rdfs_Resource,uri_rdfs_Resource),inference(resolution,[status(thm)],[c678, c29])).
% 3.33/3.60  cnf(c6,plain,iext(uri_owl_onProperty,skolem0001,uri_ex_p),inference(split_conjunct,[status(thm)],[c1])).
% 3.33/3.60  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.33/3.60  fof(c151,plain,(![S]:(![P]:(![O]:(~iext(P,S,O)|ip(P))))),inference(fof_nnf,[status(thm)],[simple_iext_property])).
% 3.33/3.60  fof(c152,plain,(![S]:(![P]:((![O]:~iext(P,S,O))|ip(P)))),inference(shift_quantors,[status(thm)],[c151])).
% 3.33/3.60  fof(c154,plain,(![X44]:(![X45]:(![X46]:(~iext(X45,X44,X46)|ip(X45))))),inference(shift_quantors,[status(thm)],[fof(c153,plain,(![X44]:(![X45]:((![X46]:~iext(X45,X44,X46))|ip(X45)))),inference(variable_rename,[status(thm)],[c152])).])).
% 3.33/3.60  cnf(c155,plain,~iext(X101,X99,X100)|ip(X101),inference(split_conjunct,[status(thm)],[c154])).
% 3.33/3.60  cnf(c542,plain,ip(uri_owl_onProperty),inference(resolution,[status(thm)],[c155, c6])).
% 3.33/3.60  cnf(c588,plain,iext(uri_rdfs_subPropertyOf,uri_owl_onProperty,uri_owl_onProperty),inference(resolution,[status(thm)],[c542, c21])).
% 3.33/3.60  cnf(c1060,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X621)|iext(X621,uri_owl_onProperty,uri_owl_onProperty),inference(resolution,[status(thm)],[c588, c29])).
% 3.33/3.60  cnf(c587,plain,iext(uri_rdf_type,uri_owl_onProperty,uri_rdf_Property),inference(resolution,[status(thm)],[c542, c136])).
% 3.33/3.60  cnf(c1051,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X619)|iext(X619,uri_owl_onProperty,uri_rdf_Property),inference(resolution,[status(thm)],[c587, c29])).
% 3.33/3.60  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.33/3.60  cnf(c124,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_sub])).
% 3.33/3.60  cnf(c541,plain,ip(uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c155, c124])).
% 3.33/3.60  cnf(c586,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c541, c21])).
% 3.33/3.60  cnf(c1044,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X618)|iext(X618,uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c586, c29])).
% 3.33/3.60  cnf(c585,plain,iext(uri_rdf_type,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c541, c136])).
% 3.33/3.60  cnf(c1030,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X616)|iext(X616,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c585, c29])).
% 3.33/3.60  cnf(c7,plain,iext(uri_owl_someValuesFrom,skolem0001,uri_ex_c),inference(split_conjunct,[status(thm)],[c1])).
% 3.33/3.60  cnf(c523,plain,ip(uri_owl_someValuesFrom),inference(resolution,[status(thm)],[c155, c7])).
% 3.33/3.60  cnf(c584,plain,iext(uri_rdfs_subPropertyOf,uri_owl_someValuesFrom,uri_owl_someValuesFrom),inference(resolution,[status(thm)],[c523, c21])).
% 3.33/3.60  cnf(c1024,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X615)|iext(X615,uri_owl_someValuesFrom,uri_owl_someValuesFrom),inference(resolution,[status(thm)],[c584, c29])).
% 3.33/3.60  cnf(c583,plain,iext(uri_rdf_type,uri_owl_someValuesFrom,uri_rdf_Property),inference(resolution,[status(thm)],[c523, c136])).
% 3.33/3.60  cnf(c1015,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X613)|iext(X613,uri_owl_someValuesFrom,uri_rdf_Property),inference(resolution,[status(thm)],[c583, c29])).
% 3.33/3.60  cnf(c520,plain,ip(uri_rdfs_domain),inference(resolution,[status(thm)],[c155, c47])).
% 3.33/3.60  cnf(c582,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,uri_rdfs_domain),inference(resolution,[status(thm)],[c520, c21])).
% 3.33/3.60  cnf(c1000,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X612)|iext(X612,uri_rdfs_domain,uri_rdfs_domain),inference(resolution,[status(thm)],[c582, c29])).
% 3.33/3.60  cnf(c581,plain,iext(uri_rdf_type,uri_rdfs_domain,uri_rdf_Property),inference(resolution,[status(thm)],[c520, c136])).
% 3.33/3.60  cnf(c988,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X610)|iext(X610,uri_rdfs_domain,uri_rdf_Property),inference(resolution,[status(thm)],[c581, c29])).
% 3.33/3.60  cnf(c514,plain,ip(uri_rdfs_range),inference(resolution,[status(thm)],[c155, c107])).
% 3.33/3.60  cnf(c580,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_range,uri_rdfs_range),inference(resolution,[status(thm)],[c514, c21])).
% 3.33/3.60  cnf(c967,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X609)|iext(X609,uri_rdfs_range,uri_rdfs_range),inference(resolution,[status(thm)],[c580, c29])).
% 3.33/3.60  cnf(c579,plain,iext(uri_rdf_type,uri_rdfs_range,uri_rdf_Property),inference(resolution,[status(thm)],[c514, c136])).
% 3.33/3.60  cnf(c955,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X607)|iext(X607,uri_rdfs_range,uri_rdf_Property),inference(resolution,[status(thm)],[c579, c29])).
% 3.33/3.60  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.33/3.60  cnf(c105,plain,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Container),inference(split_conjunct,[status(thm)],[rdfs_container_bag_sub])).
% 3.33/3.60  cnf(c511,plain,ip(uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c155, c105])).
% 3.33/3.60  cnf(c578,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c511, c21])).
% 3.33/3.60  cnf(c944,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X606)|iext(X606,uri_rdfs_subClassOf,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c578, c29])).
% 3.33/3.60  cnf(c577,plain,iext(uri_rdf_type,uri_rdfs_subClassOf,uri_rdf_Property),inference(resolution,[status(thm)],[c511, c136])).
% 3.33/3.60  cnf(c934,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X604)|iext(X604,uri_rdfs_subClassOf,uri_rdf_Property),inference(resolution,[status(thm)],[c577, c29])).
% 3.33/3.60  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.33/3.60  cnf(c145,plain,iext(uri_rdf_type,uri_rdf_first,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_collection_first_type])).
% 3.33/3.60  cnf(c507,plain,ip(uri_rdf_first),inference(resolution,[status(thm)],[c145, c135])).
% 3.33/3.60  cnf(c509,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_first,uri_rdf_first),inference(resolution,[status(thm)],[c507, c21])).
% 3.33/3.60  cnf(c927,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X603)|iext(X603,uri_rdf_first,uri_rdf_first),inference(resolution,[status(thm)],[c509, c29])).
% 3.33/3.60  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.33/3.60  cnf(c143,plain,iext(uri_rdf_type,uri_rdf_rest,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_collection_rest_type])).
% 3.33/3.60  cnf(c494,plain,ip(uri_rdf_rest),inference(resolution,[status(thm)],[c143, c135])).
% 3.33/3.60  cnf(c496,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_rest,uri_rdf_rest),inference(resolution,[status(thm)],[c494, c21])).
% 3.33/3.60  cnf(c917,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X601)|iext(X601,uri_rdf_rest,uri_rdf_rest),inference(resolution,[status(thm)],[c496, c29])).
% 3.33/3.60  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.33/3.60  cnf(c142,plain,iext(uri_rdf_type,uri_rdf__1,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_container_n_type_001])).
% 3.33/3.60  cnf(c486,plain,ip(uri_rdf__1),inference(resolution,[status(thm)],[c142, c135])).
% 3.33/3.60  cnf(c488,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__1,uri_rdf__1),inference(resolution,[status(thm)],[c486, c21])).
% 3.33/3.60  cnf(c909,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X599)|iext(X599,uri_rdf__1,uri_rdf__1),inference(resolution,[status(thm)],[c488, c29])).
% 3.33/3.60  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.33/3.60  cnf(c141,plain,iext(uri_rdf_type,uri_rdf__2,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_container_n_type_002])).
% 3.33/3.60  cnf(c478,plain,ip(uri_rdf__2),inference(resolution,[status(thm)],[c141, c135])).
% 3.33/3.60  cnf(c480,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__2,uri_rdf__2),inference(resolution,[status(thm)],[c478, c21])).
% 3.33/3.60  cnf(c902,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X597)|iext(X597,uri_rdf__2,uri_rdf__2),inference(resolution,[status(thm)],[c480, c29])).
% 3.33/3.60  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.33/3.60  cnf(c140,plain,iext(uri_rdf_type,uri_rdf__3,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_container_n_type_003])).
% 3.33/3.60  cnf(c470,plain,ip(uri_rdf__3),inference(resolution,[status(thm)],[c140, c135])).
% 3.33/3.60  cnf(c472,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__3,uri_rdf__3),inference(resolution,[status(thm)],[c470, c21])).
% 3.33/3.60  cnf(c895,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X595)|iext(X595,uri_rdf__3,uri_rdf__3),inference(resolution,[status(thm)],[c472, c29])).
% 3.33/3.60  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.33/3.60  cnf(c139,plain,iext(uri_rdf_type,uri_rdf_object,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_reification_object_type])).
% 3.33/3.60  cnf(c462,plain,ip(uri_rdf_object),inference(resolution,[status(thm)],[c139, c135])).
% 3.33/3.60  cnf(c464,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_object,uri_rdf_object),inference(resolution,[status(thm)],[c462, c21])).
% 3.33/3.60  cnf(c887,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X593)|iext(X593,uri_rdf_object,uri_rdf_object),inference(resolution,[status(thm)],[c464, c29])).
% 3.33/3.60  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.33/3.60  cnf(c138,plain,iext(uri_rdf_type,uri_rdf_value,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_reification_predicate_type])).
% 3.33/3.60  cnf(c450,plain,ip(uri_rdf_value),inference(resolution,[status(thm)],[c138, c135])).
% 3.33/3.60  cnf(c456,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_value,uri_rdf_value),inference(resolution,[status(thm)],[c450, c21])).
% 3.33/3.60  cnf(c880,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X591)|iext(X591,uri_rdf_value,uri_rdf_value),inference(resolution,[status(thm)],[c456, c29])).
% 3.33/3.60  cnf(c27,plain,~iext(uri_rdfs_subPropertyOf,X56,X55)|ip(X56),inference(split_conjunct,[status(thm)],[c26])).
% 3.33/3.60  cnf(c376,plain,ip(uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c124, c27])).
% 3.33/3.60  cnf(c452,plain,iext(uri_rdf_type,uri_rdfs_isDefinedBy,uri_rdf_Property),inference(resolution,[status(thm)],[c136, c376])).
% 3.33/3.60  cnf(c871,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X589)|iext(X589,uri_rdfs_isDefinedBy,uri_rdf_Property),inference(resolution,[status(thm)],[c452, c29])).
% 3.33/3.60  cnf(c381,plain,ip(uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c124, c28])).
% 3.33/3.60  cnf(c451,plain,iext(uri_rdf_type,uri_rdfs_seeAlso,uri_rdf_Property),inference(resolution,[status(thm)],[c136, c381])).
% 3.33/3.60  cnf(c864,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X588)|iext(X588,uri_rdfs_seeAlso,uri_rdf_Property),inference(resolution,[status(thm)],[c451, c29])).
% 3.33/3.60  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.33/3.60  cnf(c137,plain,iext(uri_rdf_type,uri_rdf_subject,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_reification_subject_type])).
% 3.33/3.60  cnf(c443,plain,ip(uri_rdf_subject),inference(resolution,[status(thm)],[c137, c135])).
% 3.33/3.60  cnf(c444,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_subject,uri_rdf_subject),inference(resolution,[status(thm)],[c443, c21])).
% 3.33/3.60  cnf(c858,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X587)|iext(X587,uri_rdf_subject,uri_rdf_subject),inference(resolution,[status(thm)],[c444, c29])).
% 3.33/3.60  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.33/3.60  cnf(c129,plain,iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_value_type])).
% 3.33/3.60  cnf(c437,plain,ip(uri_rdf_type),inference(resolution,[status(thm)],[c135, c129])).
% 3.33/3.60  cnf(c438,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_type,uri_rdf_type),inference(resolution,[status(thm)],[c437, c21])).
% 3.33/3.60  cnf(c843,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X585)|iext(X585,uri_rdf_type,uri_rdf_type),inference(resolution,[status(thm)],[c438, c29])).
% 3.33/3.60  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.33/3.60  cnf(c90,plain,iext(uri_rdf_type,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),inference(split_conjunct,[status(thm)],[rdfs_container_n_type_003])).
% 3.33/3.60  cnf(c398,plain,icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__3),inference(resolution,[status(thm)],[c118, c90])).
% 3.33/3.60  cnf(c421,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__3,uri_rdfs_member),inference(resolution,[status(thm)],[c398, c104])).
% 3.33/3.60  cnf(c835,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X583)|iext(X583,uri_rdf__3,uri_rdfs_member),inference(resolution,[status(thm)],[c421, c29])).
% 3.33/3.60  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.33/3.60  fof(c16,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.33/3.60  fof(c17,plain,(![X4]:(![X5]:(![X6]:((~iext(uri_rdfs_subPropertyOf,X4,X5)|~iext(uri_rdfs_subPropertyOf,X5,X6))|iext(uri_rdfs_subPropertyOf,X4,X6))))),inference(variable_rename,[status(thm)],[c16])).
% 3.33/3.60  cnf(c18,plain,~iext(uri_rdfs_subPropertyOf,X51,X52)|~iext(uri_rdfs_subPropertyOf,X52,X50)|iext(uri_rdfs_subPropertyOf,X51,X50),inference(split_conjunct,[status(thm)],[c17])).
% 3.33/3.60  cnf(c832,plain,~iext(uri_rdfs_subPropertyOf,X582,uri_rdf__3)|iext(uri_rdfs_subPropertyOf,X582,uri_rdfs_member),inference(resolution,[status(thm)],[c421, c18])).
% 3.33/3.60  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.33/3.60  cnf(c89,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Container),inference(split_conjunct,[status(thm)],[rdfs_container_seq_sub])).
% 3.33/3.60  cnf(c210,plain,ic(uri_rdfs_Seq),inference(resolution,[status(thm)],[c42, c89])).
% 3.33/3.60  cnf(c219,plain,icext(uri_rdfs_Class,uri_rdfs_Seq),inference(resolution,[status(thm)],[c210, c74])).
% 3.33/3.60  cnf(c416,plain,iext(uri_rdf_type,uri_rdfs_Seq,uri_rdfs_Class),inference(resolution,[status(thm)],[c119, c219])).
% 3.33/3.60  cnf(c829,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X581)|iext(X581,uri_rdfs_Seq,uri_rdfs_Class),inference(resolution,[status(thm)],[c416, c29])).
% 3.33/3.60  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.33/3.60  cnf(c106,plain,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Container),inference(split_conjunct,[status(thm)],[rdfs_container_alt_sub])).
% 3.33/3.60  cnf(c332,plain,ic(uri_rdf_Alt),inference(resolution,[status(thm)],[c106, c42])).
% 3.33/3.60  cnf(c339,plain,icext(uri_rdfs_Class,uri_rdf_Alt),inference(resolution,[status(thm)],[c332, c74])).
% 3.33/3.60  cnf(c412,plain,iext(uri_rdf_type,uri_rdf_Alt,uri_rdfs_Class),inference(resolution,[status(thm)],[c119, c339])).
% 3.33/3.60  cnf(c824,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X580)|iext(X580,uri_rdf_Alt,uri_rdfs_Class),inference(resolution,[status(thm)],[c412, c29])).
% 3.33/3.60  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.33/3.60  cnf(c88,plain,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[rdfs_dat_xmlliteral_sub])).
% 3.33/3.60  cnf(c222,plain,ic(uri_rdfs_Literal),inference(resolution,[status(thm)],[c43, c88])).
% 3.33/3.60  cnf(c228,plain,icext(uri_rdfs_Class,uri_rdfs_Literal),inference(resolution,[status(thm)],[c222, c74])).
% 3.33/3.60  cnf(c409,plain,iext(uri_rdf_type,uri_rdfs_Literal,uri_rdfs_Class),inference(resolution,[status(thm)],[c119, c228])).
% 3.33/3.60  cnf(c819,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X579)|iext(X579,uri_rdfs_Literal,uri_rdfs_Class),inference(resolution,[status(thm)],[c409, c29])).
% 3.33/3.60  cnf(c207,plain,ic(uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c42, c88])).
% 3.33/3.60  cnf(c213,plain,icext(uri_rdfs_Class,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c207, c74])).
% 3.33/3.60  cnf(c408,plain,iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Class),inference(resolution,[status(thm)],[c119, c213])).
% 3.33/3.60  cnf(c814,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X578)|iext(X578,uri_rdf_XMLLiteral,uri_rdfs_Class),inference(resolution,[status(thm)],[c408, c29])).
% 3.33/3.60  cnf(c206,plain,ic(uri_rdf_Bag),inference(resolution,[status(thm)],[c42, c105])).
% 3.33/3.60  cnf(c211,plain,icext(uri_rdfs_Class,uri_rdf_Bag),inference(resolution,[status(thm)],[c206, c74])).
% 3.33/3.60  cnf(c406,plain,iext(uri_rdf_type,uri_rdf_Bag,uri_rdfs_Class),inference(resolution,[status(thm)],[c119, c211])).
% 3.33/3.60  cnf(c808,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X577)|iext(X577,uri_rdf_Bag,uri_rdfs_Class),inference(resolution,[status(thm)],[c406, c29])).
% 3.33/3.60  cnf(c217,plain,icext(uri_rdfs_Class,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c209, c74])).
% 3.33/3.60  cnf(c405,plain,iext(uri_rdf_type,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Class),inference(resolution,[status(thm)],[c119, c217])).
% 3.33/3.60  cnf(c802,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X576)|iext(X576,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Class),inference(resolution,[status(thm)],[c405, c29])).
% 3.33/3.60  cnf(c1360,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X575)|icext(X575,uri_rdfs_comment),inference(resolution,[status(thm)],[c1354, c55])).
% 3.33/3.60  cnf(c1357,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X574)|icext(X574,uri_rdfs_comment),inference(resolution,[status(thm)],[c1354, c81])).
% 3.33/3.60  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.33/3.60  cnf(c83,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_datatype_sub])).
% 3.33/3.60  cnf(c208,plain,ic(uri_rdfs_Datatype),inference(resolution,[status(thm)],[c42, c83])).
% 3.33/3.60  cnf(c215,plain,icext(uri_rdfs_Class,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c208, c74])).
% 3.33/3.60  cnf(c403,plain,iext(uri_rdf_type,uri_rdfs_Datatype,uri_rdfs_Class),inference(resolution,[status(thm)],[c119, c215])).
% 3.33/3.60  cnf(c797,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X573)|iext(X573,uri_rdfs_Datatype,uri_rdfs_Class),inference(resolution,[status(thm)],[c403, c29])).
% 3.33/3.60  cnf(c1331,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X570)|icext(X570,uri_rdfs_label),inference(resolution,[status(thm)],[c1325, c55])).
% 3.33/3.60  cnf(c223,plain,ic(uri_rdfs_Class),inference(resolution,[status(thm)],[c43, c83])).
% 3.33/3.60  cnf(c230,plain,icext(uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c223, c74])).
% 3.33/3.60  cnf(c402,plain,iext(uri_rdf_type,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c119, c230])).
% 3.33/3.60  cnf(c791,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X569)|iext(X569,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c402, c29])).
% 3.33/3.60  cnf(c1328,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X568)|icext(X568,uri_rdfs_label),inference(resolution,[status(thm)],[c1325, c81])).
% 3.33/3.60  cnf(c221,plain,ic(uri_rdfs_Container),inference(resolution,[status(thm)],[c43, c105])).
% 3.33/3.60  cnf(c226,plain,icext(uri_rdfs_Class,uri_rdfs_Container),inference(resolution,[status(thm)],[c221, c74])).
% 3.33/3.60  cnf(c401,plain,iext(uri_rdf_type,uri_rdfs_Container,uri_rdfs_Class),inference(resolution,[status(thm)],[c119, c226])).
% 3.33/3.60  cnf(c786,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X565)|iext(X565,uri_rdfs_Container,uri_rdfs_Class),inference(resolution,[status(thm)],[c401, c29])).
% 3.33/3.60  cnf(c1301,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X564)|icext(X564,uri_rdf_List),inference(resolution,[status(thm)],[c1282, c55])).
% 3.33/3.60  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.33/3.60  cnf(c92,plain,iext(uri_rdf_type,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),inference(split_conjunct,[status(thm)],[rdfs_container_n_type_001])).
% 3.33/3.60  cnf(c394,plain,icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__1),inference(resolution,[status(thm)],[c118, c92])).
% 3.33/3.60  cnf(c400,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__1,uri_rdfs_member),inference(resolution,[status(thm)],[c394, c104])).
% 3.33/3.60  cnf(c780,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X561)|iext(X561,uri_rdf__1,uri_rdfs_member),inference(resolution,[status(thm)],[c400, c29])).
% 3.33/3.60  cnf(c1289,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X560)|icext(X560,uri_rdf_List),inference(resolution,[status(thm)],[c1281, c81])).
% 3.33/3.60  cnf(c777,plain,~iext(uri_rdfs_subPropertyOf,X557,uri_rdf__1)|iext(uri_rdfs_subPropertyOf,X557,uri_rdfs_member),inference(resolution,[status(thm)],[c400, c18])).
% 3.33/3.60  cnf(c1244,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X556)|icext(X556,uri_rdf_predicate),inference(resolution,[status(thm)],[c1238, c55])).
% 3.33/3.60  cnf(c1241,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X555)|icext(X555,uri_rdf_predicate),inference(resolution,[status(thm)],[c1238, c81])).
% 3.33/3.60  cnf(c771,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X554)|iext(X554,uri_rdf__2,uri_rdfs_member),inference(resolution,[status(thm)],[c399, c29])).
% 3.33/3.60  cnf(c1219,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X551)|icext(X551,uri_owl_ObjectProperty),inference(resolution,[status(thm)],[c1136, c55])).
% 3.33/3.60  cnf(c768,plain,~iext(uri_rdfs_subPropertyOf,X550,uri_rdf__2)|iext(uri_rdfs_subPropertyOf,X550,uri_rdfs_member),inference(resolution,[status(thm)],[c399, c18])).
% 3.33/3.60  cnf(c1208,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X547)|icext(X547,uri_owl_ObjectProperty),inference(resolution,[status(thm)],[c1135, c81])).
% 3.33/3.60  cnf(c383,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_seeAlso,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c381, c21])).
% 3.33/3.60  cnf(c764,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X546)|iext(X546,uri_rdfs_seeAlso,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c383, c29])).
% 3.33/3.60  cnf(c1198,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X543)|icext(X543,skolem0001),inference(resolution,[status(thm)],[c1105, c55])).
% 3.33/3.60  cnf(c1187,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X539)|icext(X539,skolem0001),inference(resolution,[status(thm)],[c1104, c81])).
% 3.33/3.60  cnf(c382,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c376, c21])).
% 3.33/3.60  cnf(c757,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X537)|iext(X537,uri_rdfs_isDefinedBy,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c382, c29])).
% 3.33/3.60  cnf(c1177,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X535)|icext(X535,uri_owl_Restriction),inference(resolution,[status(thm)],[c1069, c55])).
% 3.33/3.60  cnf(c1165,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X531)|icext(X531,uri_owl_Restriction),inference(resolution,[status(thm)],[c1068, c81])).
% 3.33/3.60  cnf(c375,plain,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Resource),inference(resolution,[status(thm)],[c113, c332])).
% 3.33/3.60  cnf(c750,plain,~iext(uri_rdfs_subClassOf,X528,uri_rdf_Alt)|iext(uri_rdfs_subClassOf,X528,uri_rdfs_Resource),inference(resolution,[status(thm)],[c375, c33])).
% 3.33/3.60  cnf(c1154,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X527)|icext(X527,uri_owl_Class),inference(resolution,[status(thm)],[c1040, c55])).
% 3.33/3.60  cnf(c748,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X524)|iext(X524,uri_rdf_Alt,uri_rdfs_Resource),inference(resolution,[status(thm)],[c375, c29])).
% 3.33/3.60  cnf(c1142,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X523)|icext(X523,uri_owl_Class),inference(resolution,[status(thm)],[c1039, c81])).
% 3.33/3.60  cnf(c374,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Resource),inference(resolution,[status(thm)],[c113, c208])).
% 3.33/3.60  cnf(c742,plain,~iext(uri_rdfs_subClassOf,X520,uri_rdfs_Datatype)|iext(uri_rdfs_subClassOf,X520,uri_rdfs_Resource),inference(resolution,[status(thm)],[c374, c33])).
% 3.33/3.60  cnf(c1124,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X519)|icext(X519,uri_rdfs_Statement),inference(resolution,[status(thm)],[c985, c55])).
% 3.33/3.60  cnf(c740,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X516)|iext(X516,uri_rdfs_Datatype,uri_rdfs_Resource),inference(resolution,[status(thm)],[c374, c29])).
% 3.33/3.60  cnf(c1113,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X515)|icext(X515,uri_rdfs_Statement),inference(resolution,[status(thm)],[c984, c81])).
% 3.33/3.60  cnf(c373,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c113, c223])).
% 3.33/3.60  cnf(c734,plain,~iext(uri_rdfs_subClassOf,X513,uri_rdfs_Class)|iext(uri_rdfs_subClassOf,X513,uri_rdfs_Resource),inference(resolution,[status(thm)],[c373, c33])).
% 3.33/3.60  cnf(c1093,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X510)|icext(X510,uri_rdfs_member),inference(resolution,[status(thm)],[c776, c81])).
% 3.33/3.60  cnf(c732,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X509)|iext(X509,uri_rdfs_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c373, c29])).
% 3.33/3.60  cnf(c372,plain,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Resource),inference(resolution,[status(thm)],[c113, c207])).
% 3.33/3.60  cnf(c726,plain,~iext(uri_rdfs_subClassOf,X504,uri_rdf_XMLLiteral)|iext(uri_rdfs_subClassOf,X504,uri_rdfs_Resource),inference(resolution,[status(thm)],[c372, c33])).
% 3.33/3.60  cnf(c1070,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X502)|icext(X502,uri_rdfs_Resource),inference(resolution,[status(thm)],[c678, c81])).
% 3.33/3.60  cnf(c724,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X501)|iext(X501,uri_rdf_XMLLiteral,uri_rdfs_Resource),inference(resolution,[status(thm)],[c372, c29])).
% 3.33/3.60  cnf(c1061,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X500)|icext(X500,uri_owl_onProperty),inference(resolution,[status(thm)],[c588, c55])).
% 3.33/3.60  cnf(c1058,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X499)|icext(X499,uri_owl_onProperty),inference(resolution,[status(thm)],[c588, c81])).
% 3.33/3.60  cnf(c371,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Literal,uri_rdfs_Resource),inference(resolution,[status(thm)],[c113, c222])).
% 3.33/3.60  cnf(c718,plain,~iext(uri_rdfs_subClassOf,X498,uri_rdfs_Literal)|iext(uri_rdfs_subClassOf,X498,uri_rdfs_Resource),inference(resolution,[status(thm)],[c371, c33])).
% 3.33/3.60  cnf(c1045,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X495)|icext(X495,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c586, c55])).
% 3.33/3.60  cnf(c716,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X494)|iext(X494,uri_rdfs_Literal,uri_rdfs_Resource),inference(resolution,[status(thm)],[c371, c29])).
% 3.33/3.60  cnf(c1042,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X493)|icext(X493,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c586, c81])).
% 3.33/3.60  cnf(c224,plain,ic(uri_rdf_Property),inference(resolution,[status(thm)],[c43, c101])).
% 3.33/3.60  cnf(c370,plain,iext(uri_rdfs_subClassOf,uri_rdf_Property,uri_rdfs_Resource),inference(resolution,[status(thm)],[c113, c224])).
% 3.33/3.60  cnf(c710,plain,~iext(uri_rdfs_subClassOf,X491,uri_rdf_Property)|iext(uri_rdfs_subClassOf,X491,uri_rdfs_Resource),inference(resolution,[status(thm)],[c370, c33])).
% 3.33/3.60  cnf(c1025,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X489)|icext(X489,uri_owl_someValuesFrom),inference(resolution,[status(thm)],[c584, c55])).
% 3.33/3.60  cnf(c708,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X488)|iext(X488,uri_rdf_Property,uri_rdfs_Resource),inference(resolution,[status(thm)],[c370, c29])).
% 3.33/3.60  cnf(c1021,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X487)|icext(X487,uri_owl_someValuesFrom),inference(resolution,[status(thm)],[c584, c81])).
% 3.33/3.60  cnf(c369,plain,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Resource),inference(resolution,[status(thm)],[c113, c206])).
% 3.33/3.60  cnf(c702,plain,~iext(uri_rdfs_subClassOf,X484,uri_rdf_Bag)|iext(uri_rdfs_subClassOf,X484,uri_rdfs_Resource),inference(resolution,[status(thm)],[c369, c33])).
% 3.33/3.60  cnf(c1001,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X483)|icext(X483,uri_rdfs_domain),inference(resolution,[status(thm)],[c582, c55])).
% 3.33/3.60  cnf(c996,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X482)|icext(X482,uri_rdfs_domain),inference(resolution,[status(thm)],[c582, c81])).
% 3.33/3.60  cnf(c700,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X480)|iext(X480,uri_rdf_Bag,uri_rdfs_Resource),inference(resolution,[status(thm)],[c369, c29])).
% 3.33/3.60  cnf(c368,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Container,uri_rdfs_Resource),inference(resolution,[status(thm)],[c113, c221])).
% 3.33/3.60  cnf(c694,plain,~iext(uri_rdfs_subClassOf,X478,uri_rdfs_Container)|iext(uri_rdfs_subClassOf,X478,uri_rdfs_Resource),inference(resolution,[status(thm)],[c368, c33])).
% 3.33/3.61  cnf(c968,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X477)|icext(X477,uri_rdfs_range),inference(resolution,[status(thm)],[c580, c55])).
% 3.33/3.61  cnf(c964,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X476)|icext(X476,uri_rdfs_range),inference(resolution,[status(thm)],[c580, c81])).
% 3.33/3.61  cnf(c692,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X475)|iext(X475,uri_rdfs_Container,uri_rdfs_Resource),inference(resolution,[status(thm)],[c368, c29])).
% 3.33/3.61  cnf(c945,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X472)|icext(X472,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c578, c55])).
% 3.33/3.61  cnf(c367,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Resource),inference(resolution,[status(thm)],[c113, c210])).
% 3.33/3.61  cnf(c686,plain,~iext(uri_rdfs_subClassOf,X471,uri_rdfs_Seq)|iext(uri_rdfs_subClassOf,X471,uri_rdfs_Resource),inference(resolution,[status(thm)],[c367, c33])).
% 3.33/3.61  cnf(c941,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X470)|icext(X470,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c578, c81])).
% 3.33/3.61  cnf(c684,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X467)|iext(X467,uri_rdfs_Seq,uri_rdfs_Resource),inference(resolution,[status(thm)],[c367, c29])).
% 3.33/3.61  cnf(c928,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X466)|icext(X466,uri_rdf_first),inference(resolution,[status(thm)],[c509, c55])).
% 3.33/3.61  cnf(c925,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X465)|icext(X465,uri_rdf_first),inference(resolution,[status(thm)],[c509, c81])).
% 3.33/3.61  cnf(c673,plain,~iext(uri_rdfs_subClassOf,X464,uri_rdfs_ContainerMembershipProperty)|iext(uri_rdfs_subClassOf,X464,uri_rdfs_Resource),inference(resolution,[status(thm)],[c366, c33])).
% 3.33/3.61  cnf(c918,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X463)|icext(X463,uri_rdf_rest),inference(resolution,[status(thm)],[c496, c55])).
% 3.33/3.61  cnf(c915,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X462)|icext(X462,uri_rdf_rest),inference(resolution,[status(thm)],[c496, c81])).
% 3.33/3.61  cnf(c671,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X461)|iext(X461,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Resource),inference(resolution,[status(thm)],[c366, c29])).
% 3.33/3.61  cnf(c910,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X460)|icext(X460,uri_rdf__1),inference(resolution,[status(thm)],[c488, c55])).
% 3.33/3.61  cnf(c903,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X458)|icext(X458,uri_rdf__2),inference(resolution,[status(thm)],[c480, c55])).
% 3.33/3.61  cnf(c896,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X455)|icext(X455,uri_rdf__3),inference(resolution,[status(thm)],[c472, c55])).
% 3.33/3.61  cnf(c340,plain,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdf_Alt),inference(resolution,[status(thm)],[c332, c36])).
% 3.33/3.61  cnf(c663,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X453)|iext(X453,uri_rdf_Alt,uri_rdf_Alt),inference(resolution,[status(thm)],[c340, c29])).
% 3.33/3.61  cnf(c888,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X452)|icext(X452,uri_rdf_object),inference(resolution,[status(thm)],[c464, c55])).
% 3.33/3.61  cnf(c885,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X451)|icext(X451,uri_rdf_object),inference(resolution,[status(thm)],[c464, c81])).
% 3.33/3.61  cnf(c881,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X449)|icext(X449,uri_rdf_value),inference(resolution,[status(thm)],[c456, c55])).
% 3.33/3.61  cnf(c878,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X448)|icext(X448,uri_rdf_value),inference(resolution,[status(thm)],[c456, c81])).
% 3.33/3.61  cnf(c233,plain,iext(uri_rdfs_subClassOf,uri_rdf_Property,uri_rdf_Property),inference(resolution,[status(thm)],[c224, c36])).
% 3.33/3.61  cnf(c655,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X446)|iext(X446,uri_rdf_Property,uri_rdf_Property),inference(resolution,[status(thm)],[c233, c29])).
% 3.33/3.61  cnf(c859,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X442)|icext(X442,uri_rdf_subject),inference(resolution,[status(thm)],[c444, c55])).
% 3.33/3.61  cnf(c856,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X440)|icext(X440,uri_rdf_subject),inference(resolution,[status(thm)],[c444, c81])).
% 3.33/3.61  cnf(c844,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X439)|icext(X439,uri_rdf_type),inference(resolution,[status(thm)],[c438, c55])).
% 3.33/3.61  cnf(c231,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c223, c36])).
% 3.33/3.61  cnf(c647,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X438)|iext(X438,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c231, c29])).
% 3.33/3.61  cnf(c840,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X437)|icext(X437,uri_rdf_type),inference(resolution,[status(thm)],[c438, c81])).
% 3.33/3.61  cnf(c833,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X435)|icext(X435,uri_rdf__3),inference(resolution,[status(thm)],[c421, c81])).
% 3.33/3.61  cnf(c229,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Literal,uri_rdfs_Literal),inference(resolution,[status(thm)],[c222, c36])).
% 3.33/3.61  cnf(c639,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X429)|iext(X429,uri_rdfs_Literal,uri_rdfs_Literal),inference(resolution,[status(thm)],[c229, c29])).
% 3.33/3.61  cnf(c227,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Container,uri_rdfs_Container),inference(resolution,[status(thm)],[c221, c36])).
% 3.33/3.61  cnf(c631,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X418)|iext(X418,uri_rdfs_Container,uri_rdfs_Container),inference(resolution,[status(thm)],[c227, c29])).
% 3.33/3.61  cnf(c778,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X410)|icext(X410,uri_rdf__1),inference(resolution,[status(thm)],[c400, c81])).
% 3.33/3.61  cnf(c220,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Seq),inference(resolution,[status(thm)],[c210, c36])).
% 3.33/3.61  cnf(c623,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X409)|iext(X409,uri_rdfs_Seq,uri_rdfs_Seq),inference(resolution,[status(thm)],[c220, c29])).
% 3.33/3.61  cnf(c772,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X408)|icext(X408,uri_rdfs_member),inference(resolution,[status(thm)],[c399, c55])).
% 3.33/3.61  cnf(c769,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X407)|icext(X407,uri_rdf__2),inference(resolution,[status(thm)],[c399, c81])).
% 3.33/3.61  cnf(c762,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X404)|icext(X404,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c383, c81])).
% 3.33/3.61  cnf(c758,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X403)|icext(X403,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c382, c55])).
% 3.33/3.61  cnf(c218,plain,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c209, c36])).
% 3.33/3.61  cnf(c615,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X401)|iext(X401,uri_rdfs_ContainerMembershipProperty,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c218, c29])).
% 3.33/3.61  cnf(c216,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c208, c36])).
% 3.33/3.61  cnf(c607,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X390)|iext(X390,uri_rdfs_Datatype,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c216, c29])).
% 3.33/3.61  cnf(c214,plain,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c207, c36])).
% 3.33/3.61  cnf(c599,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X379)|iext(X379,uri_rdf_XMLLiteral,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c214, c29])).
% 3.33/3.61  cnf(c672,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X378)|icext(X378,uri_rdfs_Resource),inference(resolution,[status(thm)],[c366, c55])).
% 3.33/3.61  cnf(c664,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X376)|icext(X376,uri_rdf_Alt),inference(resolution,[status(thm)],[c340, c55])).
% 3.33/3.61  cnf(c653,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X372)|icext(X372,uri_rdf_Property),inference(resolution,[status(thm)],[c233, c81])).
% 3.33/3.61  cnf(c212,plain,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdf_Bag),inference(resolution,[status(thm)],[c206, c36])).
% 3.33/3.61  cnf(c591,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X371)|iext(X371,uri_rdf_Bag,uri_rdf_Bag),inference(resolution,[status(thm)],[c212, c29])).
% 3.33/3.61  cnf(c645,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X369)|icext(X369,uri_rdfs_Class),inference(resolution,[status(thm)],[c231, c81])).
% 3.33/3.61  cnf(c506,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X367)|iext(X367,uri_rdf_first,uri_rdf_Property),inference(resolution,[status(thm)],[c145, c29])).
% 3.33/3.61  cnf(c637,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X366)|icext(X366,uri_rdfs_Literal),inference(resolution,[status(thm)],[c229, c81])).
% 3.33/3.61  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.33/3.61  cnf(c144,plain,iext(uri_rdf_type,uri_rdf_nil,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdf_collection_nil_type])).
% 3.33/3.61  cnf(c501,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X364)|iext(X364,uri_rdf_nil,uri_rdf_List),inference(resolution,[status(thm)],[c144, c29])).
% 3.33/3.61  cnf(c629,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X363)|icext(X363,uri_rdfs_Container),inference(resolution,[status(thm)],[c227, c81])).
% 3.33/3.61  cnf(c624,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X362)|icext(X362,uri_rdfs_Seq),inference(resolution,[status(thm)],[c220, c55])).
% 3.33/3.61  cnf(c493,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X360)|iext(X360,uri_rdf_rest,uri_rdf_Property),inference(resolution,[status(thm)],[c143, c29])).
% 3.33/3.61  cnf(c616,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X359)|icext(X359,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c218, c55])).
% 3.33/3.61  cnf(c485,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X357)|iext(X357,uri_rdf__1,uri_rdf_Property),inference(resolution,[status(thm)],[c142, c29])).
% 3.33/3.61  cnf(c608,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X356)|icext(X356,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c216, c55])).
% 3.33/3.61  cnf(c600,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X354)|icext(X354,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c214, c55])).
% 3.33/3.61  cnf(c477,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X353)|iext(X353,uri_rdf__2,uri_rdf_Property),inference(resolution,[status(thm)],[c141, c29])).
% 3.33/3.61  cnf(c592,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X351)|icext(X351,uri_rdf_Bag),inference(resolution,[status(thm)],[c212, c55])).
% 3.33/3.61  cnf(c469,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X349)|iext(X349,uri_rdf__3,uri_rdf_Property),inference(resolution,[status(thm)],[c140, c29])).
% 3.33/3.61  cnf(c499,plain,~iext(uri_rdfs_range,uri_rdf_type,X346)|icext(X346,uri_rdf_List),inference(resolution,[status(thm)],[c144, c55])).
% 3.33/3.61  cnf(c461,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X345)|iext(X345,uri_rdf_object,uri_rdf_Property),inference(resolution,[status(thm)],[c139, c29])).
% 3.33/3.61  cnf(c449,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X340)|iext(X340,uri_rdf_value,uri_rdf_Property),inference(resolution,[status(thm)],[c138, c29])).
% 3.33/3.61  cnf(c442,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X335)|iext(X335,uri_rdf_subject,uri_rdf_Property),inference(resolution,[status(thm)],[c137, c29])).
% 3.33/3.61  cnf(c435,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X330)|iext(X330,uri_rdf_type,uri_rdf_Property),inference(resolution,[status(thm)],[c129, c29])).
% 3.33/3.61  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.33/3.61  cnf(c128,plain,iext(uri_rdfs_domain,uri_rdfs_comment,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_comment_domain])).
% 3.33/3.61  cnf(c431,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X326)|iext(X326,uri_rdfs_comment,uri_rdfs_Resource),inference(resolution,[status(thm)],[c128, c29])).
% 3.33/3.61  cnf(c433,plain,~iext(uri_rdfs_range,uri_rdf_type,X325)|icext(X325,uri_rdf_Property),inference(resolution,[status(thm)],[c129, c55])).
% 3.33/3.61  cnf(c428,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X322)|iext(X322,uri_rdfs_comment,uri_rdfs_Literal),inference(resolution,[status(thm)],[c127, c29])).
% 3.33/3.61  cnf(c429,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X321)|icext(X321,uri_rdfs_comment),inference(resolution,[status(thm)],[c128, c81])).
% 3.33/3.61  fof(simple_ir,axiom,(![X]:ir(X)),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', simple_ir)).
% 3.33/3.61  fof(c149,plain,(![X43]:ir(X43)),inference(variable_rename,[status(thm)],[simple_ir])).
% 3.33/3.61  cnf(c150,plain,ir(X47),inference(split_conjunct,[status(thm)],[c149])).
% 3.33/3.61  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.33/3.61  fof(c64,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.33/3.61  fof(c65,plain,((![X]:(~ir(X)|icext(uri_rdfs_Resource,X)))&(![X]:(~icext(uri_rdfs_Resource,X)|ir(X)))),inference(shift_quantors,[status(thm)],[c64])).
% 3.33/3.61  fof(c67,plain,(![X25]:(![X26]:((~ir(X25)|icext(uri_rdfs_Resource,X25))&(~icext(uri_rdfs_Resource,X26)|ir(X26))))),inference(shift_quantors,[status(thm)],[fof(c66,plain,((![X25]:(~ir(X25)|icext(uri_rdfs_Resource,X25)))&(![X26]:(~icext(uri_rdfs_Resource,X26)|ir(X26)))),inference(variable_rename,[status(thm)],[c65])).])).
% 3.33/3.61  cnf(c68,plain,~ir(X58)|icext(uri_rdfs_Resource,X58),inference(split_conjunct,[status(thm)],[c67])).
% 3.33/3.61  cnf(c157,plain,icext(uri_rdfs_Resource,X59),inference(resolution,[status(thm)],[c68, c150])).
% 3.33/3.61  cnf(c413,plain,iext(uri_rdf_type,X95,uri_rdfs_Resource),inference(resolution,[status(thm)],[c119, c157])).
% 3.33/3.61  cnf(c425,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X317)|iext(X317,X318,uri_rdfs_Resource),inference(resolution,[status(thm)],[c413, c29])).
% 3.33/3.61  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.33/3.61  cnf(c126,plain,iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_domain])).
% 3.33/3.61  cnf(c389,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X316)|iext(X316,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(resolution,[status(thm)],[c126, c29])).
% 3.33/3.61  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.33/3.61  cnf(c125,plain,iext(uri_rdfs_range,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_range])).
% 3.33/3.61  cnf(c386,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X315)|iext(X315,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(resolution,[status(thm)],[c125, c29])).
% 3.33/3.61  cnf(c423,plain,~iext(uri_rdfs_range,uri_rdf_type,X313)|icext(X313,uri_rdfs_Resource),inference(resolution,[status(thm)],[c413, c55])).
% 3.33/3.61  cnf(c380,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X311)|iext(X311,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c124, c29])).
% 3.33/3.61  cnf(c387,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X310)|icext(X310,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c126, c81])).
% 3.33/3.61  cnf(c377,plain,~iext(uri_rdfs_subPropertyOf,X308,uri_rdfs_isDefinedBy)|iext(uri_rdfs_subPropertyOf,X308,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c124, c18])).
% 3.33/3.61  cnf(c384,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X307)|icext(X307,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c125, c81])).
% 3.33/3.61  cnf(c379,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X306)|icext(X306,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c124, c55])).
% 3.33/3.61  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.33/3.61  cnf(c123,plain,iext(uri_rdfs_domain,uri_rdfs_label,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_label_domain])).
% 3.33/3.61  cnf(c365,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X305)|iext(X305,uri_rdfs_label,uri_rdfs_Resource),inference(resolution,[status(thm)],[c123, c29])).
% 3.33/3.61  cnf(c378,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X304)|icext(X304,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c124, c81])).
% 3.33/3.61  cnf(c363,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X302)|icext(X302,uri_rdfs_label),inference(resolution,[status(thm)],[c123, c81])).
% 3.33/3.61  cnf(c362,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X301)|iext(X301,uri_rdfs_label,uri_rdfs_Literal),inference(resolution,[status(thm)],[c122, c29])).
% 3.33/3.61  cnf(c361,plain,~iext(uri_rdfs_range,uri_rdfs_range,X300)|icext(X300,uri_rdfs_Literal),inference(resolution,[status(thm)],[c122, c55])).
% 3.33/3.61  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.33/3.61  cnf(c121,plain,iext(uri_rdfs_domain,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_seealso_domain])).
% 3.33/3.61  cnf(c359,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X299)|iext(X299,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(resolution,[status(thm)],[c121, c29])).
% 3.33/3.61  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.33/3.61  cnf(c120,plain,iext(uri_rdfs_range,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_seealso_range])).
% 3.33/3.61  cnf(c356,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X296)|iext(X296,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(resolution,[status(thm)],[c120, c29])).
% 3.33/3.61  cnf(c357,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X295)|icext(X295,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c121, c81])).
% 3.33/3.61  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.33/3.61  cnf(c110,plain,iext(uri_rdfs_domain,uri_rdf_first,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdfs_collection_first_domain])).
% 3.33/3.61  cnf(c353,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X293)|iext(X293,uri_rdf_first,uri_rdf_List),inference(resolution,[status(thm)],[c110, c29])).
% 3.33/3.61  cnf(c354,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X292)|icext(X292,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c120, c81])).
% 3.33/3.61  cnf(c351,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X290)|icext(X290,uri_rdf_first),inference(resolution,[status(thm)],[c110, c81])).
% 3.33/3.61  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.33/3.61  cnf(c109,plain,iext(uri_rdfs_range,uri_rdf_first,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_collection_first_range])).
% 3.33/3.61  cnf(c350,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X289)|iext(X289,uri_rdf_first,uri_rdfs_Resource),inference(resolution,[status(thm)],[c109, c29])).
% 3.33/3.61  cnf(c348,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X287)|icext(X287,uri_rdf_first),inference(resolution,[status(thm)],[c109, c81])).
% 3.33/3.61  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.33/3.61  cnf(c108,plain,iext(uri_rdfs_domain,uri_rdf_rest,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdfs_collection_rest_domain])).
% 3.33/3.61  cnf(c347,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X285)|iext(X285,uri_rdf_rest,uri_rdf_List),inference(resolution,[status(thm)],[c108, c29])).
% 3.33/3.61  cnf(c346,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X283)|icext(X283,uri_rdf_List),inference(resolution,[status(thm)],[c108, c55])).
% 3.33/3.61  cnf(c345,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X282)|icext(X282,uri_rdf_rest),inference(resolution,[status(thm)],[c108, c81])).
% 3.33/3.61  cnf(c344,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X281)|iext(X281,uri_rdf_rest,uri_rdf_List),inference(resolution,[status(thm)],[c107, c29])).
% 3.33/3.61  cnf(c338,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X279)|iext(X279,uri_rdf_Alt,uri_rdfs_Container),inference(resolution,[status(thm)],[c106, c29])).
% 3.33/3.61  cnf(c342,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X278)|icext(X278,uri_rdf_rest),inference(resolution,[status(thm)],[c107, c81])).
% 3.33/3.61  cnf(c335,plain,~iext(uri_rdfs_subClassOf,X276,uri_rdf_Alt)|iext(uri_rdfs_subClassOf,X276,uri_rdfs_Container),inference(resolution,[status(thm)],[c106, c33])).
% 3.33/3.61  cnf(c333,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X275)|icext(X275,uri_rdf_Alt),inference(resolution,[status(thm)],[c106, c81])).
% 3.33/3.61  cnf(c326,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X273)|icext(X273,uri_rdfs_range),inference(resolution,[status(thm)],[c81, c52])).
% 3.33/3.61  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.33/3.61  cnf(c100,plain,iext(uri_rdfs_domain,uri_rdfs_member,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_member_domain])).
% 3.33/3.61  cnf(c325,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X272)|icext(X272,uri_rdfs_member),inference(resolution,[status(thm)],[c81, c100])).
% 3.33/3.61  cnf(c324,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X271)|icext(X271,uri_rdfs_Seq),inference(resolution,[status(thm)],[c81, c89])).
% 3.33/3.61  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.33/3.61  cnf(c37,plain,iext(uri_rdfs_range,uri_rdfs_subClassOf,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_subclassof_range])).
% 3.33/3.61  cnf(c323,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X270)|icext(X270,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c81, c37])).
% 3.33/3.61  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.33/3.61  cnf(c51,plain,iext(uri_rdfs_domain,uri_rdf_object,uri_rdfs_Statement),inference(split_conjunct,[status(thm)],[rdfs_reification_object_domain])).
% 3.33/3.61  cnf(c322,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X269)|icext(X269,uri_rdf_object),inference(resolution,[status(thm)],[c81, c51])).
% 3.33/3.61  cnf(c321,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X268)|icext(X268,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c81, c101])).
% 3.33/3.61  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.33/3.61  cnf(c93,plain,iext(uri_rdfs_range,uri_rdf__3,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_range_003])).
% 3.33/3.61  cnf(c320,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X267)|icext(X267,uri_rdf__3),inference(resolution,[status(thm)],[c81, c93])).
% 3.33/3.61  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.33/3.61  cnf(c45,plain,iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_subclassof_domain])).
% 3.33/3.61  cnf(c319,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X266)|icext(X266,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c81, c45])).
% 3.33/3.61  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.33/3.61  cnf(c97,plain,iext(uri_rdfs_domain,uri_rdf__2,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_002])).
% 3.33/3.61  cnf(c317,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X264)|icext(X264,uri_rdf__2),inference(resolution,[status(thm)],[c81, c97])).
% 3.33/3.61  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.33/3.61  cnf(c30,plain,iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_subpropertyof_domain])).
% 3.33/3.61  cnf(c316,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X263)|icext(X263,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c81, c30])).
% 3.33/3.61  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.33/3.61  cnf(c22,plain,iext(uri_rdfs_range,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_subpropertyof_range])).
% 3.33/3.61  cnf(c314,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X261)|icext(X261,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c81, c22])).
% 3.33/3.61  cnf(c313,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X260)|icext(X260,uri_rdfs_range),inference(resolution,[status(thm)],[c81, c56])).
% 3.33/3.61  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.33/3.61  cnf(c15,plain,iext(uri_rdfs_domain,uri_rdf_type,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_type_domain])).
% 3.33/3.61  cnf(c311,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X258)|icext(X258,uri_rdf_type),inference(resolution,[status(thm)],[c81, c15])).
% 3.33/3.61  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.33/3.61  cnf(c99,plain,iext(uri_rdfs_range,uri_rdfs_member,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_member_range])).
% 3.33/3.61  cnf(c310,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X257)|icext(X257,uri_rdfs_member),inference(resolution,[status(thm)],[c81, c99])).
% 3.33/3.61  cnf(c309,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X256)|icext(X256,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c81, c83])).
% 3.33/3.61  cnf(c308,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X255)|icext(X255,uri_rdfs_domain),inference(resolution,[status(thm)],[c81, c76])).
% 3.33/3.61  cnf(c307,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X254)|icext(X254,uri_rdf_type),inference(resolution,[status(thm)],[c81, c14])).
% 3.33/3.61  cnf(c306,plain,~iext(uri_rdfs_domain,uri_owl_onProperty,X253)|icext(X253,skolem0001),inference(resolution,[status(thm)],[c81, c6])).
% 3.33/3.61  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.33/3.61  cnf(c98,plain,iext(uri_rdfs_domain,uri_rdf__1,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_001])).
% 3.33/3.61  cnf(c303,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X250)|icext(X250,uri_rdf__1),inference(resolution,[status(thm)],[c81, c98])).
% 3.33/3.61  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.33/3.61  cnf(c96,plain,iext(uri_rdfs_domain,uri_rdf__3,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_003])).
% 3.33/3.61  cnf(c301,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X248)|icext(X248,uri_rdf__3),inference(resolution,[status(thm)],[c81, c96])).
% 3.33/3.61  cnf(c300,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X247)|icext(X247,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c81, c88])).
% 3.33/3.61  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.33/3.61  cnf(c13,plain,iext(uri_rdfs_domain,uri_rdf_value,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_value_domain])).
% 3.33/3.61  cnf(c299,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X246)|icext(X246,uri_rdf_value),inference(resolution,[status(thm)],[c81, c13])).
% 3.33/3.61  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.33/3.61  cnf(c12,plain,iext(uri_rdfs_range,uri_rdf_value,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_value_range])).
% 3.33/3.61  cnf(c297,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X244)|icext(X244,uri_rdf_value),inference(resolution,[status(thm)],[c81, c12])).
% 3.33/3.61  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.33/3.61  cnf(c48,plain,iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_reification_predicate_range])).
% 3.33/3.61  cnf(c296,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X243)|icext(X243,uri_rdf_predicate),inference(resolution,[status(thm)],[c81, c48])).
% 3.33/3.61  cnf(c422,plain,~iext(uri_rdfs_domain,uri_rdf_type,X240)|icext(X240,X241),inference(resolution,[status(thm)],[c413, c81])).
% 3.33/3.61  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.33/3.61  cnf(c95,plain,iext(uri_rdfs_range,uri_rdf__1,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_range_001])).
% 3.33/3.61  cnf(c294,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X234)|icext(X234,uri_rdf__1),inference(resolution,[status(thm)],[c81, c95])).
% 3.33/3.61  cnf(c293,plain,~iext(uri_rdfs_domain,uri_owl_someValuesFrom,X229)|icext(X229,skolem0001),inference(resolution,[status(thm)],[c81, c7])).
% 3.33/3.61  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.33/3.61  cnf(c94,plain,iext(uri_rdfs_range,uri_rdf__2,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_range_002])).
% 3.33/3.61  cnf(c292,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X228)|icext(X228,uri_rdf__2),inference(resolution,[status(thm)],[c81, c94])).
% 3.33/3.61  cnf(c290,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X222)|icext(X222,uri_rdf_subject),inference(resolution,[status(thm)],[c81, c47])).
% 3.33/3.61  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.33/3.61  cnf(c46,plain,iext(uri_rdfs_range,uri_rdf_subject,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_reification_subject_range])).
% 3.33/3.61  cnf(c288,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X212)|icext(X212,uri_rdf_subject),inference(resolution,[status(thm)],[c81, c46])).
% 3.33/3.61  cnf(c287,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X207)|icext(X207,uri_rdf_Bag),inference(resolution,[status(thm)],[c81, c105])).
% 3.33/3.61  cnf(c286,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X202)|icext(X202,uri_rdfs_domain),inference(factor,[status(thm)],[c81])).
% 3.33/3.61  cnf(c44,plain,~iext(uri_rdfs_subClassOf,X78,X79)|~icext(X78,X77)|icext(X79,X77),inference(split_conjunct,[status(thm)],[c41])).
% 3.33/3.61  cnf(c336,plain,~icext(uri_rdf_Alt,X198)|icext(uri_rdfs_Container,X198),inference(resolution,[status(thm)],[c106, c44])).
% 3.33/3.61  cnf(c277,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X191)|icext(X191,uri_rdf_Property),inference(resolution,[status(thm)],[c55, c101])).
% 3.33/3.61  cnf(c275,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X189)|icext(X189,uri_rdfs_Class),inference(resolution,[status(thm)],[c55, c45])).
% 3.33/3.61  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.33/3.61  cnf(c57,plain,iext(uri_rdf_type,uri_rdf_Property,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_property_type])).
% 3.33/3.61  cnf(c274,plain,~iext(uri_rdfs_range,uri_rdf_type,X188)|icext(X188,uri_rdfs_Class),inference(resolution,[status(thm)],[c55, c57])).
% 3.33/3.61  cnf(c270,plain,~iext(uri_rdfs_range,uri_rdfs_range,X184)|icext(X184,uri_rdf_Property),inference(resolution,[status(thm)],[c55, c22])).
% 3.33/3.61  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.33/3.61  cnf(c87,plain,iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Datatype),inference(split_conjunct,[status(thm)],[rdfs_dat_xmlliteral_type])).
% 3.33/3.61  cnf(c268,plain,~iext(uri_rdfs_range,uri_rdf_type,X182)|icext(X182,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c55, c87])).
% 3.33/3.61  cnf(c265,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X179)|icext(X179,uri_rdfs_Class),inference(resolution,[status(thm)],[c55, c83])).
% 3.33/3.61  cnf(c263,plain,~iext(uri_rdfs_range,uri_rdfs_range,X177)|icext(X177,uri_rdfs_Class),inference(resolution,[status(thm)],[c55, c14])).
% 3.33/3.61  cnf(c262,plain,~iext(uri_rdfs_range,uri_owl_onProperty,X176)|icext(X176,uri_ex_p),inference(resolution,[status(thm)],[c55, c6])).
% 3.33/3.61  cnf(c258,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X172)|icext(X172,uri_rdf_Property),inference(resolution,[status(thm)],[c55, c82])).
% 3.33/3.61  cnf(c1089,plain,icext(uri_rdf_Property,uri_rdfs_member),inference(resolution,[status(thm)],[c775, c118])).
% 3.33/3.61  cnf(c256,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X170)|icext(X170,uri_rdfs_Literal),inference(resolution,[status(thm)],[c55, c88])).
% 3.33/3.61  cnf(c255,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X169)|icext(X169,uri_rdfs_Resource),inference(resolution,[status(thm)],[c55, c13])).
% 3.33/3.61  cnf(c1053,plain,icext(uri_rdf_Property,uri_owl_onProperty),inference(resolution,[status(thm)],[c587, c118])).
% 3.43/3.61  cnf(c1032,plain,icext(uri_rdf_Property,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c585, c118])).
% 3.43/3.61  cnf(c1017,plain,icext(uri_rdf_Property,uri_owl_someValuesFrom),inference(resolution,[status(thm)],[c583, c118])).
% 3.43/3.61  cnf(c249,plain,~iext(uri_rdfs_range,uri_owl_someValuesFrom,X163)|icext(X163,uri_ex_c),inference(resolution,[status(thm)],[c55, c7])).
% 3.43/3.61  cnf(c990,plain,icext(uri_rdf_Property,uri_rdfs_domain),inference(resolution,[status(thm)],[c581, c118])).
% 3.43/3.61  cnf(c957,plain,icext(uri_rdf_Property,uri_rdfs_range),inference(resolution,[status(thm)],[c579, c118])).
% 3.43/3.61  cnf(c245,plain,~iext(uri_rdfs_range,uri_rdf_type,X159)|icext(X159,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c55, c91])).
% 3.43/3.61  cnf(c244,plain,~iext(uri_rdfs_range,uri_rdfs_range,X158)|icext(X158,uri_rdfs_Resource),inference(resolution,[status(thm)],[c55, c46])).
% 3.43/3.61  cnf(c936,plain,icext(uri_rdf_Property,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c577, c118])).
% 3.43/3.61  cnf(c243,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X157)|icext(X157,uri_rdfs_Container),inference(resolution,[status(thm)],[c55, c105])).
% 3.43/3.61  cnf(c242,plain,~iext(uri_rdfs_range,uri_rdfs_range,X156)|icext(X156,X156),inference(factor,[status(thm)],[c55])).
% 3.43/3.61  cnf(c238,plain,~icext(uri_rdfs_Seq,X155)|icext(uri_rdfs_Container,X155),inference(resolution,[status(thm)],[c44, c89])).
% 3.43/3.61  cnf(c237,plain,~icext(uri_rdfs_ContainerMembershipProperty,X154)|icext(uri_rdf_Property,X154),inference(resolution,[status(thm)],[c44, c101])).
% 3.43/3.61  cnf(c236,plain,~icext(uri_rdfs_Datatype,X153)|icext(uri_rdfs_Class,X153),inference(resolution,[status(thm)],[c44, c83])).
% 3.43/3.61  cnf(c235,plain,~icext(uri_rdf_XMLLiteral,X152)|icext(uri_rdfs_Literal,X152),inference(resolution,[status(thm)],[c44, c88])).
% 3.43/3.61  cnf(c234,plain,~icext(uri_rdf_Bag,X151)|icext(uri_rdfs_Container,X151),inference(resolution,[status(thm)],[c44, c105])).
% 3.43/3.61  cnf(c205,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X150)|iext(X150,uri_rdf_Bag,uri_rdfs_Container),inference(resolution,[status(thm)],[c105, c29])).
% 3.43/3.61  cnf(c204,plain,~iext(uri_rdfs_subClassOf,X149,uri_rdf_Bag)|iext(uri_rdfs_subClassOf,X149,uri_rdfs_Container),inference(resolution,[status(thm)],[c105, c33])).
% 3.43/3.61  cnf(c203,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X148)|iext(X148,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),inference(resolution,[status(thm)],[c101, c29])).
% 3.43/3.61  cnf(c202,plain,~iext(uri_rdfs_subClassOf,X147,uri_rdfs_ContainerMembershipProperty)|iext(uri_rdfs_subClassOf,X147,uri_rdf_Property),inference(resolution,[status(thm)],[c101, c33])).
% 3.43/3.61  cnf(c873,plain,icext(uri_rdf_Property,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c452, c118])).
% 3.43/3.61  cnf(c201,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X146)|iext(X146,uri_rdfs_member,uri_rdfs_Resource),inference(resolution,[status(thm)],[c100, c29])).
% 3.43/3.61  cnf(c866,plain,icext(uri_rdf_Property,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c451, c118])).
% 3.43/3.61  cnf(c200,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X145)|iext(X145,uri_rdfs_member,uri_rdfs_Resource),inference(resolution,[status(thm)],[c99, c29])).
% 3.43/3.61  cnf(c199,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X144)|iext(X144,uri_rdf__1,uri_rdfs_Resource),inference(resolution,[status(thm)],[c98, c29])).
% 3.43/3.61  cnf(c198,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X143)|iext(X143,uri_rdf__2,uri_rdfs_Resource),inference(resolution,[status(thm)],[c97, c29])).
% 3.43/3.61  cnf(c197,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X142)|iext(X142,uri_rdf__3,uri_rdfs_Resource),inference(resolution,[status(thm)],[c96, c29])).
% 3.43/3.61  cnf(c196,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X141)|iext(X141,uri_rdf__1,uri_rdfs_Resource),inference(resolution,[status(thm)],[c95, c29])).
% 3.43/3.61  cnf(c195,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X140)|iext(X140,uri_rdf__2,uri_rdfs_Resource),inference(resolution,[status(thm)],[c94, c29])).
% 3.43/3.61  cnf(c194,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X139)|iext(X139,uri_rdf__3,uri_rdfs_Resource),inference(resolution,[status(thm)],[c93, c29])).
% 3.43/3.61  cnf(c193,plain,~iext(uri_rdfs_subClassOf,X138,uri_rdfs_Seq)|iext(uri_rdfs_subClassOf,X138,uri_rdfs_Container),inference(resolution,[status(thm)],[c33, c89])).
% 3.43/3.61  cnf(c192,plain,~iext(uri_rdfs_subClassOf,X137,uri_rdfs_Datatype)|iext(uri_rdfs_subClassOf,X137,uri_rdfs_Class),inference(resolution,[status(thm)],[c33, c83])).
% 3.43/3.61  cnf(c191,plain,~iext(uri_rdfs_subClassOf,X136,uri_rdf_XMLLiteral)|iext(uri_rdfs_subClassOf,X136,uri_rdfs_Literal),inference(resolution,[status(thm)],[c33, c88])).
% 3.43/3.61  cnf(c189,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X134)|iext(X134,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c92, c29])).
% 3.43/3.61  cnf(c188,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X133)|iext(X133,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c91, c29])).
% 3.43/3.61  cnf(c187,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X132)|iext(X132,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c90, c29])).
% 3.43/3.61  cnf(c186,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X131)|iext(X131,uri_rdfs_Seq,uri_rdfs_Container),inference(resolution,[status(thm)],[c89, c29])).
% 3.43/3.61  cnf(c185,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X130)|iext(X130,uri_rdf_XMLLiteral,uri_rdfs_Literal),inference(resolution,[status(thm)],[c88, c29])).
% 3.43/3.61  cnf(c184,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X129)|iext(X129,uri_rdfs_range,uri_rdfs_Class),inference(resolution,[status(thm)],[c29, c52])).
% 3.43/3.61  cnf(c183,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X128)|iext(X128,uri_rdfs_subClassOf,uri_rdfs_Class),inference(resolution,[status(thm)],[c29, c37])).
% 3.43/3.61  cnf(c182,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X127)|iext(X127,uri_rdf_object,uri_rdfs_Statement),inference(resolution,[status(thm)],[c29, c51])).
% 3.43/3.61  cnf(c181,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X126)|iext(X126,uri_rdfs_subClassOf,uri_rdfs_Class),inference(resolution,[status(thm)],[c29, c45])).
% 3.43/3.61  cnf(c180,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X125)|iext(X125,uri_rdf_Property,uri_rdfs_Class),inference(resolution,[status(thm)],[c29, c57])).
% 3.43/3.61  cnf(c179,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X124)|iext(X124,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c29, c30])).
% 3.43/3.61  cnf(c178,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X123)|iext(X123,uri_ex_p,uri_owl_ObjectProperty),inference(resolution,[status(thm)],[c29, c2])).
% 3.43/3.61  cnf(c177,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X122)|iext(X122,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c29, c22])).
% 3.43/3.61  cnf(c176,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X121)|iext(X121,uri_rdfs_range,uri_rdf_Property),inference(resolution,[status(thm)],[c29, c56])).
% 3.43/3.61  cnf(c175,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X120)|iext(X120,uri_rdf_XMLLiteral,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c29, c87])).
% 3.43/3.61  cnf(c174,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X119)|iext(X119,uri_rdf_type,uri_rdfs_Resource),inference(resolution,[status(thm)],[c29, c15])).
% 3.43/3.61  cnf(c173,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X118)|iext(X118,uri_rdfs_Datatype,uri_rdfs_Class),inference(resolution,[status(thm)],[c29, c83])).
% 3.43/3.61  cnf(c172,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X117)|iext(X117,uri_rdfs_domain,uri_rdfs_Class),inference(resolution,[status(thm)],[c29, c76])).
% 3.43/3.61  cnf(c171,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X116)|iext(X116,uri_rdf_type,uri_rdfs_Class),inference(resolution,[status(thm)],[c29, c14])).
% 3.43/3.61  cnf(c170,plain,~iext(uri_rdfs_subPropertyOf,uri_owl_onProperty,X115)|iext(X115,skolem0001,uri_ex_p),inference(resolution,[status(thm)],[c29, c6])).
% 3.43/3.61  cnf(c169,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X114)|iext(X114,uri_ex_s,skolem0001),inference(resolution,[status(thm)],[c29, c4])).
% 3.43/3.61  cnf(c168,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X113)|iext(X113,uri_rdfs_domain,uri_rdf_Property),inference(resolution,[status(thm)],[c29, c82])).
% 3.43/3.61  cnf(c167,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X112)|iext(X112,uri_rdf_value,uri_rdfs_Resource),inference(resolution,[status(thm)],[c29, c13])).
% 3.43/3.61  cnf(c166,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X111)|iext(X111,skolem0001,uri_owl_Restriction),inference(resolution,[status(thm)],[c29, c5])).
% 3.43/3.61  cnf(c165,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X110)|iext(X110,uri_rdf_value,uri_rdfs_Resource),inference(resolution,[status(thm)],[c29, c12])).
% 3.43/3.61  cnf(c164,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X109)|iext(X109,uri_rdf_predicate,uri_rdfs_Resource),inference(resolution,[status(thm)],[c29, c48])).
% 3.43/3.61  cnf(c163,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X108)|iext(X108,uri_ex_c,uri_owl_Class),inference(resolution,[status(thm)],[c29, c3])).
% 3.43/3.61  cnf(c162,plain,~iext(uri_rdfs_subPropertyOf,uri_owl_someValuesFrom,X107)|iext(X107,skolem0001,uri_ex_c),inference(resolution,[status(thm)],[c29, c7])).
% 3.43/3.61  cnf(c161,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X106)|iext(X106,uri_rdf_predicate,uri_rdfs_Statement),inference(resolution,[status(thm)],[c29, c49])).
% 3.43/3.61  cnf(c160,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X105)|iext(X105,uri_rdf_subject,uri_rdfs_Statement),inference(resolution,[status(thm)],[c29, c47])).
% 3.43/3.61  cnf(c159,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X104)|iext(X104,uri_rdf_subject,uri_rdfs_Resource),inference(resolution,[status(thm)],[c29, c46])).
% 3.43/3.61  cnf(c158,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X103)|iext(X103,uri_rdfs_subPropertyOf,X103),inference(factor,[status(thm)],[c29])).
% 3.43/3.61  cnf(c505,plain,icext(uri_rdf_Property,uri_rdf_first),inference(resolution,[status(thm)],[c145, c118])).
% 3.43/3.61  cnf(c500,plain,icext(uri_rdf_List,uri_rdf_nil),inference(resolution,[status(thm)],[c144, c118])).
% 3.43/3.61  cnf(c492,plain,icext(uri_rdf_Property,uri_rdf_rest),inference(resolution,[status(thm)],[c143, c118])).
% 3.43/3.61  cnf(c484,plain,icext(uri_rdf_Property,uri_rdf__1),inference(resolution,[status(thm)],[c142, c118])).
% 3.43/3.61  cnf(c476,plain,icext(uri_rdf_Property,uri_rdf__2),inference(resolution,[status(thm)],[c141, c118])).
% 3.43/3.61  cnf(c468,plain,icext(uri_rdf_Property,uri_rdf__3),inference(resolution,[status(thm)],[c140, c118])).
% 3.43/3.61  cnf(c460,plain,icext(uri_rdf_Property,uri_rdf_object),inference(resolution,[status(thm)],[c139, c118])).
% 3.43/3.61  cnf(c448,plain,icext(uri_rdf_Property,uri_rdf_value),inference(resolution,[status(thm)],[c138, c118])).
% 3.43/3.61  cnf(c441,plain,icext(uri_rdf_Property,uri_rdf_subject),inference(resolution,[status(thm)],[c137, c118])).
% 3.43/3.61  cnf(c434,plain,icext(uri_rdf_Property,uri_rdf_type),inference(resolution,[status(thm)],[c129, c118])).
% 3.43/3.61  cnf(c396,plain,icext(uri_owl_ObjectProperty,uri_ex_p),inference(resolution,[status(thm)],[c118, c2])).
% 3.43/3.61  cnf(c395,plain,icext(uri_rdfs_Datatype,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c118, c87])).
% 3.43/3.61  cnf(c393,plain,icext(skolem0001,uri_ex_s),inference(resolution,[status(thm)],[c118, c4])).
% 3.43/3.61  cnf(c392,plain,icext(uri_owl_Restriction,skolem0001),inference(resolution,[status(thm)],[c118, c5])).
% 3.43/3.61  cnf(c391,plain,icext(uri_owl_Class,uri_ex_c),inference(resolution,[status(thm)],[c118, c3])).
% 3.43/3.61  cnf(c232,plain,icext(uri_rdfs_Class,uri_rdf_Property),inference(resolution,[status(thm)],[c224, c74])).
% 3.43/3.61  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.43/3.61  fof(c84,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.43/3.61  fof(c85,plain,(![X33]:(~icext(uri_rdfs_Datatype,X33)|iext(uri_rdfs_subClassOf,X33,uri_rdfs_Literal))),inference(variable_rename,[status(thm)],[c84])).
% 3.43/3.61  cnf(c86,plain,~icext(uri_rdfs_Datatype,X88)|iext(uri_rdfs_subClassOf,X88,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[c85])).
% 3.43/3.61  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.43/3.61  fof(c58,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.43/3.61  fof(c59,plain,((![X]:(~lv(X)|icext(uri_rdfs_Literal,X)))&(![X]:(~icext(uri_rdfs_Literal,X)|lv(X)))),inference(shift_quantors,[status(thm)],[c58])).
% 3.43/3.61  fof(c61,plain,(![X23]:(![X24]:((~lv(X23)|icext(uri_rdfs_Literal,X23))&(~icext(uri_rdfs_Literal,X24)|lv(X24))))),inference(shift_quantors,[status(thm)],[fof(c60,plain,((![X23]:(~lv(X23)|icext(uri_rdfs_Literal,X23)))&(![X24]:(~icext(uri_rdfs_Literal,X24)|lv(X24)))),inference(variable_rename,[status(thm)],[c59])).])).
% 3.43/3.61  cnf(c63,plain,~icext(uri_rdfs_Literal,X57)|lv(X57),inference(split_conjunct,[status(thm)],[c61])).
% 3.43/3.61  cnf(c62,plain,~lv(X54)|icext(uri_rdfs_Literal,X54),inference(split_conjunct,[status(thm)],[c61])).
% 3.43/3.61  fof(testcase_conclusion_fullish_009_Existential_Restriction_Entailments,conjecture,(?[BNODE_x]:(iext(uri_ex_p,uri_ex_s,BNODE_x)&iext(uri_rdf_type,BNODE_x,uri_ex_c))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', testcase_conclusion_fullish_009_Existential_Restriction_Entailments)).
% 3.43/3.61  fof(c8,negated_conjecture,(~(?[BNODE_x]:(iext(uri_ex_p,uri_ex_s,BNODE_x)&iext(uri_rdf_type,BNODE_x,uri_ex_c)))),inference(assume_negation,[status(cth)],[testcase_conclusion_fullish_009_Existential_Restriction_Entailments])).
% 3.43/3.61  fof(c9,negated_conjecture,(![BNODE_x]:(~iext(uri_ex_p,uri_ex_s,BNODE_x)|~iext(uri_rdf_type,BNODE_x,uri_ex_c))),inference(fof_nnf,[status(thm)],[c8])).
% 3.43/3.61  fof(c10,negated_conjecture,(![X3]:(~iext(uri_ex_p,uri_ex_s,X3)|~iext(uri_rdf_type,X3,uri_ex_c))),inference(variable_rename,[status(thm)],[c9])).
% 3.43/3.61  cnf(c11,negated_conjecture,~iext(uri_ex_p,uri_ex_s,X49)|~iext(uri_rdf_type,X49,uri_ex_c),inference(split_conjunct,[status(thm)],[c10])).
% 3.43/3.61  % SZS output end Saturation
% 3.43/3.61  
% 3.43/3.61  % Initial clauses    : 96
% 3.43/3.61  % Processed clauses  : 589
% 3.43/3.61  % Factors computed   : 5
% 3.43/3.61  % Resolvents computed: 1392
% 3.43/3.61  % Tautologies deleted: 57
% 3.43/3.61  % Forward subsumed   : 847
% 3.43/3.61  % Backward subsumed  : 3
% 3.43/3.61  % -------- CPU Time ---------
% 3.43/3.61  % User time          : 3.240 s
% 3.43/3.61  % System time        : 0.019 s
% 3.43/3.61  % Total time         : 3.259 s
%------------------------------------------------------------------------------