PyRes---1.5.CSA-Sat.s

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

% Computer : n029.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:52 EDT 2024

% Result   : CounterSatisfiable 3.71s 3.90s
% Output   : Saturation 3.71s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13  % Problem  : SWB021+4 : TPTP v8.1.2. Released v5.2.0.
% 0.12/0.14  % Command  : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35  % Computer : n029.cluster.edu
% 0.14/0.35  % Model    : x86_64 x86_64
% 0.14/0.35  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35  % Memory   : 8042.1875MB
% 0.14/0.35  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35  % CPULimit : 300
% 0.14/0.35  % WCLimit  : 300
% 0.14/0.35  % DateTime : Wed May  8 22:03:53 EDT 2024
% 0.14/0.35  % CPUTime  : 
% 3.71/3.90  % Version:  1.5
% 3.71/3.90  % SZS status CounterSatisfiable
% 3.71/3.90  % SZS output start Saturation
% 3.71/3.90  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.71/3.90  fof(c38,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.71/3.90  fof(c40,plain,(![X15]:(![X16]:(![X17]:(![X18]:(~iext(uri_rdfs_subPropertyOf,X15,X16)|((ip(X15)&ip(X16))&(~iext(X15,X17,X18)|iext(X16,X17,X18)))))))),inference(shift_quantors,[status(thm)],[fof(c39,plain,(![X15]:(![X16]:(~iext(uri_rdfs_subPropertyOf,X15,X16)|((ip(X15)&ip(X16))&(![X17]:(![X18]:(~iext(X15,X17,X18)|iext(X16,X17,X18)))))))),inference(variable_rename,[status(thm)],[c38])).])).
% 3.71/3.90  fof(c41,plain,(![X15]:(![X16]:(![X17]:(![X18]:(((~iext(uri_rdfs_subPropertyOf,X15,X16)|ip(X15))&(~iext(uri_rdfs_subPropertyOf,X15,X16)|ip(X16)))&(~iext(uri_rdfs_subPropertyOf,X15,X16)|(~iext(X15,X17,X18)|iext(X16,X17,X18)))))))),inference(distribute,[status(thm)],[c40])).
% 3.71/3.90  cnf(c44,plain,~iext(uri_rdfs_subPropertyOf,X73,X72)|~iext(X73,X74,X71)|iext(X72,X74,X71),inference(split_conjunct,[status(thm)],[c41])).
% 3.71/3.90  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.71/3.90  fof(c34,plain,(![P]:(~ip(P)|iext(uri_rdfs_subPropertyOf,P,P))),inference(fof_nnf,[status(thm)],[rdfs_subpropertyof_reflex])).
% 3.71/3.90  fof(c35,plain,(![X14]:(~ip(X14)|iext(uri_rdfs_subPropertyOf,X14,X14))),inference(variable_rename,[status(thm)],[c34])).
% 3.71/3.90  cnf(c36,plain,~ip(X59)|iext(uri_rdfs_subPropertyOf,X59,X59),inference(split_conjunct,[status(thm)],[c35])).
% 3.71/3.90  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.71/3.90  fof(c146,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.71/3.90  fof(c147,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)],[c146])).
% 3.71/3.90  fof(c149,plain,(![X47]:(![X48]:((~iext(uri_rdf_type,X47,uri_rdf_Property)|ip(X47))&(~ip(X48)|iext(uri_rdf_type,X48,uri_rdf_Property))))),inference(shift_quantors,[status(thm)],[fof(c148,plain,((![X47]:(~iext(uri_rdf_type,X47,uri_rdf_Property)|ip(X47)))&(![X48]:(~ip(X48)|iext(uri_rdf_type,X48,uri_rdf_Property)))),inference(variable_rename,[status(thm)],[c147])).])).
% 3.71/3.90  cnf(c150,plain,~iext(uri_rdf_type,X103,uri_rdf_Property)|ip(X103),inference(split_conjunct,[status(thm)],[c149])).
% 3.71/3.90  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.71/3.90  fof(c129,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.71/3.90  fof(c130,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)],[c129])).
% 3.71/3.90  fof(c132,plain,(![X43]:(![X44]:(![X45]:(![X46]:((~iext(uri_rdf_type,X43,X44)|icext(X44,X43))&(~icext(X46,X45)|iext(uri_rdf_type,X45,X46))))))),inference(shift_quantors,[status(thm)],[fof(c131,plain,((![X43]:(![X44]:(~iext(uri_rdf_type,X43,X44)|icext(X44,X43))))&(![X45]:(![X46]:(~icext(X46,X45)|iext(uri_rdf_type,X45,X46))))),inference(variable_rename,[status(thm)],[c130])).])).
% 3.71/3.90  cnf(c134,plain,~icext(X99,X100)|iext(uri_rdf_type,X100,X99),inference(split_conjunct,[status(thm)],[c132])).
% 3.71/3.90  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.71/3.90  cnf(c71,plain,iext(uri_rdfs_domain,uri_rdfs_range,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_range_domain])).
% 3.71/3.90  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.71/3.90  fof(c92,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.71/3.90  fof(c93,plain,(![P]:(![C]:(![X]:((~iext(uri_rdfs_domain,P,C)|(![Y]:~iext(P,X,Y)))|icext(C,X))))),inference(shift_quantors,[status(thm)],[c92])).
% 3.71/3.90  fof(c95,plain,(![X36]:(![X37]:(![X38]:(![X39]:((~iext(uri_rdfs_domain,X36,X37)|~iext(X36,X38,X39))|icext(X37,X38)))))),inference(shift_quantors,[status(thm)],[fof(c94,plain,(![X36]:(![X37]:(![X38]:((~iext(uri_rdfs_domain,X36,X37)|(![X39]:~iext(X36,X38,X39)))|icext(X37,X38))))),inference(variable_rename,[status(thm)],[c93])).])).
% 3.71/3.90  cnf(c96,plain,~iext(uri_rdfs_domain,X92,X91)|~iext(X92,X90,X93)|icext(X91,X90),inference(split_conjunct,[status(thm)],[c95])).
% 3.71/3.90  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.71/3.90  cnf(c142,plain,iext(uri_rdfs_range,uri_rdfs_comment,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[rdfs_annotation_comment_range])).
% 3.71/3.90  cnf(c483,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X365)|icext(X365,uri_rdfs_comment),inference(resolution,[status(thm)],[c142, c96])).
% 3.71/3.90  cnf(c1406,plain,icext(uri_rdf_Property,uri_rdfs_comment),inference(resolution,[status(thm)],[c483, c71])).
% 3.71/3.90  cnf(c1407,plain,iext(uri_rdf_type,uri_rdfs_comment,uri_rdf_Property),inference(resolution,[status(thm)],[c1406, c134])).
% 3.71/3.90  cnf(c1414,plain,ip(uri_rdfs_comment),inference(resolution,[status(thm)],[c1407, c150])).
% 3.71/3.90  cnf(c1416,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_comment,uri_rdfs_comment),inference(resolution,[status(thm)],[c1414, c36])).
% 3.71/3.90  cnf(c1419,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X694)|iext(X694,uri_rdfs_comment,uri_rdfs_comment),inference(resolution,[status(thm)],[c1416, c44])).
% 3.71/3.90  cnf(c1411,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X693)|iext(X693,uri_rdfs_comment,uri_rdf_Property),inference(resolution,[status(thm)],[c1407, c44])).
% 3.71/3.90  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.71/3.90  cnf(c137,plain,iext(uri_rdfs_range,uri_rdfs_label,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[rdfs_annotation_label_range])).
% 3.71/3.90  cnf(c435,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X345)|icext(X345,uri_rdfs_label),inference(resolution,[status(thm)],[c137, c96])).
% 3.71/3.90  cnf(c1376,plain,icext(uri_rdf_Property,uri_rdfs_label),inference(resolution,[status(thm)],[c435, c71])).
% 3.71/3.90  cnf(c1378,plain,iext(uri_rdf_type,uri_rdfs_label,uri_rdf_Property),inference(resolution,[status(thm)],[c1376, c134])).
% 3.71/3.90  cnf(c1384,plain,ip(uri_rdfs_label),inference(resolution,[status(thm)],[c1378, c150])).
% 3.71/3.90  cnf(c1386,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_label,uri_rdfs_label),inference(resolution,[status(thm)],[c1384, c36])).
% 3.71/3.90  cnf(c1389,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X691)|iext(X691,uri_rdfs_label,uri_rdfs_label),inference(resolution,[status(thm)],[c1386, c44])).
% 3.71/3.90  cnf(c1381,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X690)|iext(X690,uri_rdfs_label,uri_rdf_Property),inference(resolution,[status(thm)],[c1378, c44])).
% 3.71/3.90  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.71/3.90  fof(c49,plain,(![C]:(~ic(C)|iext(uri_rdfs_subClassOf,C,C))),inference(fof_nnf,[status(thm)],[rdfs_subclassof_reflex])).
% 3.71/3.90  fof(c50,plain,(![X22]:(~ic(X22)|iext(uri_rdfs_subClassOf,X22,X22))),inference(variable_rename,[status(thm)],[c49])).
% 3.71/3.90  cnf(c51,plain,~ic(X78)|iext(uri_rdfs_subClassOf,X78,X78),inference(split_conjunct,[status(thm)],[c50])).
% 3.71/3.90  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.71/3.90  fof(c85,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.71/3.90  fof(c86,plain,((![X]:(~ic(X)|icext(uri_rdfs_Class,X)))&(![X]:(~icext(uri_rdfs_Class,X)|ic(X)))),inference(shift_quantors,[status(thm)],[c85])).
% 3.71/3.90  fof(c88,plain,(![X34]:(![X35]:((~ic(X34)|icext(uri_rdfs_Class,X34))&(~icext(uri_rdfs_Class,X35)|ic(X35))))),inference(shift_quantors,[status(thm)],[fof(c87,plain,((![X34]:(~ic(X34)|icext(uri_rdfs_Class,X34)))&(![X35]:(~icext(uri_rdfs_Class,X35)|ic(X35)))),inference(variable_rename,[status(thm)],[c86])).])).
% 3.71/3.90  cnf(c90,plain,~icext(uri_rdfs_Class,X70)|ic(X70),inference(split_conjunct,[status(thm)],[c88])).
% 3.71/3.90  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.71/3.90  cnf(c67,plain,iext(uri_rdfs_range,uri_rdfs_range,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_range_range])).
% 3.71/3.90  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.71/3.90  fof(c68,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.71/3.90  fof(c69,plain,(![X26]:(![X27]:(![X28]:(![X29]:((~iext(uri_rdfs_range,X26,X27)|~iext(X26,X28,X29))|icext(X27,X29)))))),inference(variable_rename,[status(thm)],[c68])).
% 3.71/3.90  cnf(c70,plain,~iext(uri_rdfs_range,X89,X87)|~iext(X89,X86,X88)|icext(X87,X88),inference(split_conjunct,[status(thm)],[c69])).
% 3.71/3.90  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.71/3.90  cnf(c122,plain,iext(uri_rdfs_range,uri_rdf_rest,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdfs_collection_rest_range])).
% 3.71/3.90  cnf(c405,plain,~iext(uri_rdfs_range,uri_rdfs_range,X321)|icext(X321,uri_rdf_List),inference(resolution,[status(thm)],[c122, c70])).
% 3.71/3.90  cnf(c1332,plain,icext(uri_rdfs_Class,uri_rdf_List),inference(resolution,[status(thm)],[c405, c67])).
% 3.71/3.90  cnf(c1333,plain,ic(uri_rdf_List),inference(resolution,[status(thm)],[c1332, c90])).
% 3.71/3.90  cnf(c1338,plain,iext(uri_rdfs_subClassOf,uri_rdf_List,uri_rdf_List),inference(resolution,[status(thm)],[c1333, c51])).
% 3.71/3.90  cnf(c1356,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X689)|iext(X689,uri_rdf_List,uri_rdf_List),inference(resolution,[status(thm)],[c1338, c44])).
% 3.71/3.90  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.71/3.90  fof(c126,plain,(![C]:(~ic(C)|iext(uri_rdfs_subClassOf,C,uri_rdfs_Resource))),inference(fof_nnf,[status(thm)],[rdfs_class_instsub_resource])).
% 3.71/3.90  fof(c127,plain,(![X42]:(~ic(X42)|iext(uri_rdfs_subClassOf,X42,uri_rdfs_Resource))),inference(variable_rename,[status(thm)],[c126])).
% 3.71/3.90  cnf(c128,plain,~ic(X96)|iext(uri_rdfs_subClassOf,X96,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[c127])).
% 3.71/3.90  cnf(c1336,plain,iext(uri_rdfs_subClassOf,uri_rdf_List,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1333, c128])).
% 3.71/3.90  cnf(c1347,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X687)|iext(X687,uri_rdf_List,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1336, c44])).
% 3.71/3.90  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.71/3.90  fof(c46,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.71/3.90  fof(c47,plain,(![X19]:(![X20]:(![X21]:((~iext(uri_rdfs_subClassOf,X19,X20)|~iext(uri_rdfs_subClassOf,X20,X21))|iext(uri_rdfs_subClassOf,X19,X21))))),inference(variable_rename,[status(thm)],[c46])).
% 3.71/3.90  cnf(c48,plain,~iext(uri_rdfs_subClassOf,X75,X76)|~iext(uri_rdfs_subClassOf,X76,X77)|iext(uri_rdfs_subClassOf,X75,X77),inference(split_conjunct,[status(thm)],[c47])).
% 3.71/3.90  cnf(c1346,plain,~iext(uri_rdfs_subClassOf,X686,uri_rdf_List)|iext(uri_rdfs_subClassOf,X686,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1336, c48])).
% 3.71/3.90  cnf(c1334,plain,iext(uri_rdf_type,uri_rdf_List,uri_rdfs_Class),inference(resolution,[status(thm)],[c1332, c134])).
% 3.71/3.90  cnf(c1341,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X685)|iext(X685,uri_rdf_List,uri_rdfs_Class),inference(resolution,[status(thm)],[c1334, c44])).
% 3.71/3.90  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.71/3.90  cnf(c123,plain,iext(uri_rdfs_domain,uri_rdf_rest,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdfs_collection_rest_domain])).
% 3.71/3.90  fof(testcase_premise_fullish_021_Composite_Enumerations,axiom,(?[BNODE_l11]:(?[BNODE_l12]:(?[BNODE_l21]:(?[BNODE_l22]:(?[BNODE_l31]:(?[BNODE_l32]:(?[BNODE_l33]:(?[BNODE_l41]:(?[BNODE_l42]:(((((((((((((((((((((iext(uri_owl_oneOf,uri_ex_c1,BNODE_l11)&iext(uri_rdf_first,BNODE_l11,uri_ex_w1))&iext(uri_rdf_rest,BNODE_l11,BNODE_l12))&iext(uri_rdf_first,BNODE_l12,uri_ex_w2))&iext(uri_rdf_rest,BNODE_l12,uri_rdf_nil))&iext(uri_owl_oneOf,uri_ex_c2,BNODE_l21))&iext(uri_rdf_first,BNODE_l21,uri_ex_w2))&iext(uri_rdf_rest,BNODE_l21,BNODE_l22))&iext(uri_rdf_first,BNODE_l22,uri_ex_w3))&iext(uri_rdf_rest,BNODE_l22,uri_rdf_nil))&iext(uri_owl_oneOf,uri_ex_c3,BNODE_l31))&iext(uri_rdf_first,BNODE_l31,uri_ex_w1))&iext(uri_rdf_rest,BNODE_l31,BNODE_l32))&iext(uri_rdf_first,BNODE_l32,uri_ex_w2))&iext(uri_rdf_rest,BNODE_l32,BNODE_l33))&iext(uri_rdf_first,BNODE_l33,uri_ex_w3))&iext(uri_rdf_rest,BNODE_l33,uri_rdf_nil))&iext(uri_owl_unionOf,uri_ex_c4,BNODE_l41))&iext(uri_rdf_first,BNODE_l41,uri_ex_c1))&iext(uri_rdf_rest,BNODE_l41,BNODE_l42))&iext(uri_rdf_first,BNODE_l42,uri_ex_c2))&iext(uri_rdf_rest,BNODE_l42,uri_rdf_nil))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', testcase_premise_fullish_021_Composite_Enumerations)).
% 3.71/3.90  fof(c0,plain,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:(?[X9]:(?[X10]:(((((((((((((((((((((iext(uri_owl_oneOf,uri_ex_c1,X2)&iext(uri_rdf_first,X2,uri_ex_w1))&iext(uri_rdf_rest,X2,X3))&iext(uri_rdf_first,X3,uri_ex_w2))&iext(uri_rdf_rest,X3,uri_rdf_nil))&iext(uri_owl_oneOf,uri_ex_c2,X4))&iext(uri_rdf_first,X4,uri_ex_w2))&iext(uri_rdf_rest,X4,X5))&iext(uri_rdf_first,X5,uri_ex_w3))&iext(uri_rdf_rest,X5,uri_rdf_nil))&iext(uri_owl_oneOf,uri_ex_c3,X6))&iext(uri_rdf_first,X6,uri_ex_w1))&iext(uri_rdf_rest,X6,X7))&iext(uri_rdf_first,X7,uri_ex_w2))&iext(uri_rdf_rest,X7,X8))&iext(uri_rdf_first,X8,uri_ex_w3))&iext(uri_rdf_rest,X8,uri_rdf_nil))&iext(uri_owl_unionOf,uri_ex_c4,X9))&iext(uri_rdf_first,X9,uri_ex_c1))&iext(uri_rdf_rest,X9,X10))&iext(uri_rdf_first,X10,uri_ex_c2))&iext(uri_rdf_rest,X10,uri_rdf_nil))))))))))),inference(variable_rename,[status(thm)],[testcase_premise_fullish_021_Composite_Enumerations])).
% 3.71/3.90  fof(c1,plain,(((((((((((((((((((((iext(uri_owl_oneOf,uri_ex_c1,skolem0001)&iext(uri_rdf_first,skolem0001,uri_ex_w1))&iext(uri_rdf_rest,skolem0001,skolem0002))&iext(uri_rdf_first,skolem0002,uri_ex_w2))&iext(uri_rdf_rest,skolem0002,uri_rdf_nil))&iext(uri_owl_oneOf,uri_ex_c2,skolem0003))&iext(uri_rdf_first,skolem0003,uri_ex_w2))&iext(uri_rdf_rest,skolem0003,skolem0004))&iext(uri_rdf_first,skolem0004,uri_ex_w3))&iext(uri_rdf_rest,skolem0004,uri_rdf_nil))&iext(uri_owl_oneOf,uri_ex_c3,skolem0005))&iext(uri_rdf_first,skolem0005,uri_ex_w1))&iext(uri_rdf_rest,skolem0005,skolem0006))&iext(uri_rdf_first,skolem0006,uri_ex_w2))&iext(uri_rdf_rest,skolem0006,skolem0007))&iext(uri_rdf_first,skolem0007,uri_ex_w3))&iext(uri_rdf_rest,skolem0007,uri_rdf_nil))&iext(uri_owl_unionOf,uri_ex_c4,skolem0008))&iext(uri_rdf_first,skolem0008,uri_ex_c1))&iext(uri_rdf_rest,skolem0008,skolem0009))&iext(uri_rdf_first,skolem0009,uri_ex_c2))&iext(uri_rdf_rest,skolem0009,uri_rdf_nil)),inference(skolemize,[status(esa)],[c0])).
% 3.71/3.90  cnf(c21,plain,iext(uri_rdf_rest,skolem0008,skolem0009),inference(split_conjunct,[status(thm)],[c1])).
% 3.71/3.90  cnf(c353,plain,~iext(uri_rdfs_domain,uri_rdf_rest,X294)|icext(X294,skolem0008),inference(resolution,[status(thm)],[c96, c21])).
% 3.71/3.90  cnf(c1304,plain,icext(uri_rdf_List,skolem0008),inference(resolution,[status(thm)],[c353, c123])).
% 3.71/3.90  cnf(c1305,plain,iext(uri_rdf_type,skolem0008,uri_rdf_List),inference(resolution,[status(thm)],[c1304, c134])).
% 3.71/3.90  cnf(c1308,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X684)|iext(X684,skolem0008,uri_rdf_List),inference(resolution,[status(thm)],[c1305, c44])).
% 3.71/3.90  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.71/3.90  cnf(c125,plain,iext(uri_rdfs_domain,uri_rdf_first,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdfs_collection_first_domain])).
% 3.71/3.90  cnf(c13,plain,iext(uri_rdf_first,skolem0005,uri_ex_w1),inference(split_conjunct,[status(thm)],[c1])).
% 3.71/3.90  cnf(c341,plain,~iext(uri_rdfs_domain,uri_rdf_first,X282)|icext(X282,skolem0005),inference(resolution,[status(thm)],[c96, c13])).
% 3.71/3.90  cnf(c1288,plain,icext(uri_rdf_List,skolem0005),inference(resolution,[status(thm)],[c341, c125])).
% 3.71/3.90  cnf(c1290,plain,iext(uri_rdf_type,skolem0005,uri_rdf_List),inference(resolution,[status(thm)],[c1288, c134])).
% 3.71/3.90  cnf(c1293,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X683)|iext(X683,skolem0005,uri_rdf_List),inference(resolution,[status(thm)],[c1290, c44])).
% 3.71/3.90  cnf(c8,plain,iext(uri_rdf_first,skolem0003,uri_ex_w2),inference(split_conjunct,[status(thm)],[c1])).
% 3.71/3.90  cnf(c331,plain,~iext(uri_rdfs_domain,uri_rdf_first,X272)|icext(X272,skolem0003),inference(resolution,[status(thm)],[c96, c8])).
% 3.71/3.90  cnf(c1274,plain,icext(uri_rdf_List,skolem0003),inference(resolution,[status(thm)],[c331, c125])).
% 3.71/3.90  cnf(c1275,plain,iext(uri_rdf_type,skolem0003,uri_rdf_List),inference(resolution,[status(thm)],[c1274, c134])).
% 3.71/3.90  cnf(c1278,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X682)|iext(X682,skolem0003,uri_rdf_List),inference(resolution,[status(thm)],[c1275, c44])).
% 3.71/3.90  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.71/3.90  cnf(c63,plain,iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_reification_predicate_range])).
% 3.71/3.90  cnf(c324,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X265)|icext(X265,uri_rdf_predicate),inference(resolution,[status(thm)],[c96, c63])).
% 3.71/3.90  cnf(c1254,plain,icext(uri_rdf_Property,uri_rdf_predicate),inference(resolution,[status(thm)],[c324, c71])).
% 3.71/3.90  cnf(c1255,plain,iext(uri_rdf_type,uri_rdf_predicate,uri_rdf_Property),inference(resolution,[status(thm)],[c1254, c134])).
% 3.71/3.90  cnf(c1261,plain,ip(uri_rdf_predicate),inference(resolution,[status(thm)],[c1255, c150])).
% 3.71/3.90  cnf(c1263,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_predicate,uri_rdf_predicate),inference(resolution,[status(thm)],[c1261, c36])).
% 3.71/3.90  cnf(c1266,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X680)|iext(X680,uri_rdf_predicate,uri_rdf_predicate),inference(resolution,[status(thm)],[c1263, c44])).
% 3.71/3.90  cnf(c1258,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X679)|iext(X679,uri_rdf_predicate,uri_rdf_Property),inference(resolution,[status(thm)],[c1255, c44])).
% 3.71/3.90  cnf(c3,plain,iext(uri_rdf_first,skolem0001,uri_ex_w1),inference(split_conjunct,[status(thm)],[c1])).
% 3.71/3.90  cnf(c317,plain,~iext(uri_rdfs_domain,uri_rdf_first,X257)|icext(X257,skolem0001),inference(resolution,[status(thm)],[c96, c3])).
% 3.71/3.90  cnf(c1240,plain,icext(uri_rdf_List,skolem0001),inference(resolution,[status(thm)],[c317, c125])).
% 3.71/3.90  cnf(c1242,plain,iext(uri_rdf_type,skolem0001,uri_rdf_List),inference(resolution,[status(thm)],[c1240, c134])).
% 3.71/3.90  cnf(c1245,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X678)|iext(X678,skolem0001,uri_rdf_List),inference(resolution,[status(thm)],[c1242, c44])).
% 3.71/3.90  cnf(c16,plain,iext(uri_rdf_rest,skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c1])).
% 3.71/3.90  cnf(c295,plain,~iext(uri_rdfs_range,uri_rdf_rest,X237)|icext(X237,skolem0007),inference(resolution,[status(thm)],[c70, c16])).
% 3.71/3.90  cnf(c1225,plain,icext(uri_rdf_List,skolem0007),inference(resolution,[status(thm)],[c295, c122])).
% 3.71/3.90  cnf(c1226,plain,iext(uri_rdf_type,skolem0007,uri_rdf_List),inference(resolution,[status(thm)],[c1225, c134])).
% 3.71/3.90  cnf(c1229,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X677)|iext(X677,skolem0007,uri_rdf_List),inference(resolution,[status(thm)],[c1226, c44])).
% 3.71/3.90  cnf(c293,plain,~iext(uri_rdfs_range,uri_rdf_rest,X235)|icext(X235,skolem0009),inference(resolution,[status(thm)],[c70, c21])).
% 3.71/3.90  cnf(c1218,plain,icext(uri_rdf_List,skolem0009),inference(resolution,[status(thm)],[c293, c122])).
% 3.71/3.90  cnf(c1219,plain,iext(uri_rdf_type,skolem0009,uri_rdf_List),inference(resolution,[status(thm)],[c1218, c134])).
% 3.71/3.90  cnf(c1222,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X676)|iext(X676,skolem0009,uri_rdf_List),inference(resolution,[status(thm)],[c1219, c44])).
% 3.71/3.90  cnf(c14,plain,iext(uri_rdf_rest,skolem0005,skolem0006),inference(split_conjunct,[status(thm)],[c1])).
% 3.71/3.90  cnf(c286,plain,~iext(uri_rdfs_range,uri_rdf_rest,X206)|icext(X206,skolem0006),inference(resolution,[status(thm)],[c70, c14])).
% 3.71/3.90  cnf(c1209,plain,icext(uri_rdf_List,skolem0006),inference(resolution,[status(thm)],[c286, c122])).
% 3.71/3.90  cnf(c1210,plain,iext(uri_rdf_type,skolem0006,uri_rdf_List),inference(resolution,[status(thm)],[c1209, c134])).
% 3.71/3.90  cnf(c1213,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X675)|iext(X675,skolem0006,uri_rdf_List),inference(resolution,[status(thm)],[c1210, c44])).
% 3.71/3.90  cnf(c9,plain,iext(uri_rdf_rest,skolem0003,skolem0004),inference(split_conjunct,[status(thm)],[c1])).
% 3.71/3.90  cnf(c274,plain,~iext(uri_rdfs_range,uri_rdf_rest,X187)|icext(X187,skolem0004),inference(resolution,[status(thm)],[c70, c9])).
% 3.71/3.90  cnf(c1171,plain,icext(uri_rdf_List,skolem0004),inference(resolution,[status(thm)],[c274, c122])).
% 3.71/3.90  cnf(c1172,plain,iext(uri_rdf_type,skolem0004,uri_rdf_List),inference(resolution,[status(thm)],[c1171, c134])).
% 3.71/3.90  cnf(c1203,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X674)|iext(X674,skolem0004,uri_rdf_List),inference(resolution,[status(thm)],[c1172, c44])).
% 3.71/3.90  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.71/3.90  cnf(c91,plain,iext(uri_rdfs_range,uri_rdfs_domain,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_domain_range])).
% 3.71/3.90  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.71/3.90  cnf(c66,plain,iext(uri_rdfs_domain,uri_rdf_object,uri_rdfs_Statement),inference(split_conjunct,[status(thm)],[rdfs_reification_object_domain])).
% 3.71/3.90  cnf(c264,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X177)|icext(X177,uri_rdfs_Statement),inference(resolution,[status(thm)],[c70, c66])).
% 3.71/3.90  cnf(c1152,plain,icext(uri_rdfs_Class,uri_rdfs_Statement),inference(resolution,[status(thm)],[c264, c91])).
% 3.71/3.90  cnf(c1154,plain,ic(uri_rdfs_Statement),inference(resolution,[status(thm)],[c1152, c90])).
% 3.71/3.90  cnf(c1158,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Statement,uri_rdfs_Statement),inference(resolution,[status(thm)],[c1154, c51])).
% 3.71/3.90  cnf(c1195,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X673)|iext(X673,uri_rdfs_Statement,uri_rdfs_Statement),inference(resolution,[status(thm)],[c1158, c44])).
% 3.71/3.90  cnf(c1156,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Statement,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1154, c128])).
% 3.71/3.90  cnf(c1187,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X671)|iext(X671,uri_rdfs_Statement,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1156, c44])).
% 3.71/3.90  cnf(c1186,plain,~iext(uri_rdfs_subClassOf,X670,uri_rdfs_Statement)|iext(uri_rdfs_subClassOf,X670,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1156, c48])).
% 3.71/3.90  cnf(c1155,plain,iext(uri_rdf_type,uri_rdfs_Statement,uri_rdfs_Class),inference(resolution,[status(thm)],[c1152, c134])).
% 3.71/3.90  cnf(c1182,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X669)|iext(X669,uri_rdfs_Statement,uri_rdfs_Class),inference(resolution,[status(thm)],[c1155, c44])).
% 3.71/3.90  cnf(c4,plain,iext(uri_rdf_rest,skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c1])).
% 3.71/3.90  cnf(c261,plain,~iext(uri_rdfs_range,uri_rdf_rest,X174)|icext(X174,skolem0002),inference(resolution,[status(thm)],[c70, c4])).
% 3.71/3.90  cnf(c1130,plain,icext(uri_rdf_List,skolem0002),inference(resolution,[status(thm)],[c261, c122])).
% 3.71/3.91  cnf(c1131,plain,iext(uri_rdf_type,skolem0002,uri_rdf_List),inference(resolution,[status(thm)],[c1130, c134])).
% 3.71/3.91  cnf(c1177,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X668)|iext(X668,skolem0002,uri_rdf_List),inference(resolution,[status(thm)],[c1131, c44])).
% 3.71/3.91  cnf(c43,plain,~iext(uri_rdfs_subPropertyOf,X65,X64)|ip(X64),inference(split_conjunct,[status(thm)],[c41])).
% 3.71/3.91  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.71/3.91  fof(c117,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.71/3.91  fof(c118,plain,(![X41]:(~icext(uri_rdfs_ContainerMembershipProperty,X41)|iext(uri_rdfs_subPropertyOf,X41,uri_rdfs_member))),inference(variable_rename,[status(thm)],[c117])).
% 3.71/3.91  cnf(c119,plain,~icext(uri_rdfs_ContainerMembershipProperty,X95)|iext(uri_rdfs_subPropertyOf,X95,uri_rdfs_member),inference(split_conjunct,[status(thm)],[c118])).
% 3.71/3.91  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.71/3.91  cnf(c106,plain,iext(uri_rdf_type,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),inference(split_conjunct,[status(thm)],[rdfs_container_n_type_002])).
% 3.71/3.91  cnf(c133,plain,~iext(uri_rdf_type,X98,X97)|icext(X97,X98),inference(split_conjunct,[status(thm)],[c132])).
% 3.71/3.91  cnf(c446,plain,icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__2),inference(resolution,[status(thm)],[c133, c106])).
% 3.71/3.91  cnf(c452,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__2,uri_rdfs_member),inference(resolution,[status(thm)],[c446, c119])).
% 3.71/3.91  cnf(c840,plain,ip(uri_rdfs_member),inference(resolution,[status(thm)],[c452, c43])).
% 3.71/3.91  cnf(c847,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_member,uri_rdfs_member),inference(resolution,[status(thm)],[c840, c36])).
% 3.71/3.91  cnf(c1165,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X667)|iext(X667,uri_rdfs_member,uri_rdfs_member),inference(resolution,[status(thm)],[c847, c44])).
% 3.71/3.91  cnf(c151,plain,~ip(X104)|iext(uri_rdf_type,X104,uri_rdf_Property),inference(split_conjunct,[status(thm)],[c149])).
% 3.71/3.91  cnf(c846,plain,iext(uri_rdf_type,uri_rdfs_member,uri_rdf_Property),inference(resolution,[status(thm)],[c840, c151])).
% 3.71/3.91  cnf(c1151,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X665)|iext(X665,uri_rdfs_member,uri_rdf_Property),inference(resolution,[status(thm)],[c846, c44])).
% 3.71/3.91  cnf(c89,plain,~ic(X69)|icext(uri_rdfs_Class,X69),inference(split_conjunct,[status(thm)],[c88])).
% 3.71/3.91  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.71/3.91  fof(c53,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.71/3.91  fof(c55,plain,(![X23]:(![X24]:(![X25]:(~iext(uri_rdfs_subClassOf,X23,X24)|((ic(X23)&ic(X24))&(~icext(X23,X25)|icext(X24,X25))))))),inference(shift_quantors,[status(thm)],[fof(c54,plain,(![X23]:(![X24]:(~iext(uri_rdfs_subClassOf,X23,X24)|((ic(X23)&ic(X24))&(![X25]:(~icext(X23,X25)|icext(X24,X25))))))),inference(variable_rename,[status(thm)],[c53])).])).
% 3.71/3.91  fof(c56,plain,(![X23]:(![X24]:(![X25]:(((~iext(uri_rdfs_subClassOf,X23,X24)|ic(X23))&(~iext(uri_rdfs_subClassOf,X23,X24)|ic(X24)))&(~iext(uri_rdfs_subClassOf,X23,X24)|(~icext(X23,X25)|icext(X24,X25))))))),inference(distribute,[status(thm)],[c55])).
% 3.71/3.91  cnf(c58,plain,~iext(uri_rdfs_subClassOf,X82,X81)|ic(X81),inference(split_conjunct,[status(thm)],[c56])).
% 3.71/3.91  cnf(c57,plain,~iext(uri_rdfs_subClassOf,X80,X79)|ic(X80),inference(split_conjunct,[status(thm)],[c56])).
% 3.71/3.91  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.71/3.91  cnf(c121,plain,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Container),inference(split_conjunct,[status(thm)],[rdfs_container_alt_sub])).
% 3.71/3.91  cnf(c400,plain,ic(uri_rdf_Alt),inference(resolution,[status(thm)],[c121, c57])).
% 3.71/3.91  cnf(c417,plain,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Resource),inference(resolution,[status(thm)],[c128, c400])).
% 3.71/3.91  cnf(c743,plain,ic(uri_rdfs_Resource),inference(resolution,[status(thm)],[c417, c58])).
% 3.71/3.91  cnf(c749,plain,icext(uri_rdfs_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c743, c89])).
% 3.71/3.91  cnf(c752,plain,iext(uri_rdf_type,uri_rdfs_Resource,uri_rdfs_Class),inference(resolution,[status(thm)],[c749, c134])).
% 3.71/3.91  cnf(c1144,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X664)|iext(X664,uri_rdfs_Resource,uri_rdfs_Class),inference(resolution,[status(thm)],[c752, c44])).
% 3.71/3.91  cnf(c748,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Resource,uri_rdfs_Resource),inference(resolution,[status(thm)],[c743, c128])).
% 3.71/3.91  cnf(c1139,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X663)|iext(X663,uri_rdfs_Resource,uri_rdfs_Resource),inference(resolution,[status(thm)],[c748, c44])).
% 3.71/3.91  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.71/3.91  cnf(c139,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_sub])).
% 3.71/3.91  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.71/3.91  fof(c166,plain,(![S]:(![P]:(![O]:(~iext(P,S,O)|ip(P))))),inference(fof_nnf,[status(thm)],[simple_iext_property])).
% 3.71/3.91  fof(c167,plain,(![S]:(![P]:((![O]:~iext(P,S,O))|ip(P)))),inference(shift_quantors,[status(thm)],[c166])).
% 3.71/3.91  fof(c169,plain,(![X51]:(![X52]:(![X53]:(~iext(X52,X51,X53)|ip(X52))))),inference(shift_quantors,[status(thm)],[fof(c168,plain,(![X51]:(![X52]:((![X53]:~iext(X52,X51,X53))|ip(X52)))),inference(variable_rename,[status(thm)],[c167])).])).
% 3.71/3.91  cnf(c170,plain,~iext(X105,X106,X107)|ip(X105),inference(split_conjunct,[status(thm)],[c169])).
% 3.71/3.91  cnf(c632,plain,ip(uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c170, c139])).
% 3.71/3.91  cnf(c659,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c632, c36])).
% 3.71/3.91  cnf(c1129,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X661)|iext(X661,uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c659, c44])).
% 3.71/3.91  cnf(c658,plain,iext(uri_rdf_type,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c632, c151])).
% 3.71/3.91  cnf(c1119,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X659)|iext(X659,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c658, c44])).
% 3.71/3.91  cnf(c19,plain,iext(uri_owl_unionOf,uri_ex_c4,skolem0008),inference(split_conjunct,[status(thm)],[c1])).
% 3.71/3.91  cnf(c626,plain,ip(uri_owl_unionOf),inference(resolution,[status(thm)],[c170, c19])).
% 3.71/3.91  cnf(c657,plain,iext(uri_rdfs_subPropertyOf,uri_owl_unionOf,uri_owl_unionOf),inference(resolution,[status(thm)],[c626, c36])).
% 3.71/3.91  cnf(c1112,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X658)|iext(X658,uri_owl_unionOf,uri_owl_unionOf),inference(resolution,[status(thm)],[c657, c44])).
% 3.71/3.91  cnf(c656,plain,iext(uri_rdf_type,uri_owl_unionOf,uri_rdf_Property),inference(resolution,[status(thm)],[c626, c151])).
% 3.71/3.91  cnf(c1102,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X656)|iext(X656,uri_owl_unionOf,uri_rdf_Property),inference(resolution,[status(thm)],[c656, c44])).
% 3.71/3.91  cnf(c7,plain,iext(uri_owl_oneOf,uri_ex_c2,skolem0003),inference(split_conjunct,[status(thm)],[c1])).
% 3.71/3.91  cnf(c578,plain,ip(uri_owl_oneOf),inference(resolution,[status(thm)],[c170, c7])).
% 3.71/3.91  cnf(c655,plain,iext(uri_rdfs_subPropertyOf,uri_owl_oneOf,uri_owl_oneOf),inference(resolution,[status(thm)],[c578, c36])).
% 3.71/3.91  cnf(c1093,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X655)|iext(X655,uri_owl_oneOf,uri_owl_oneOf),inference(resolution,[status(thm)],[c655, c44])).
% 3.71/3.91  cnf(c654,plain,iext(uri_rdf_type,uri_owl_oneOf,uri_rdf_Property),inference(resolution,[status(thm)],[c578, c151])).
% 3.71/3.91  cnf(c1083,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X653)|iext(X653,uri_owl_oneOf,uri_rdf_Property),inference(resolution,[status(thm)],[c654, c44])).
% 3.71/3.91  cnf(c576,plain,ip(uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c170, c121])).
% 3.71/3.91  cnf(c653,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c576, c36])).
% 3.71/3.91  cnf(c1077,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X652)|iext(X652,uri_rdfs_subClassOf,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c653, c44])).
% 3.71/3.91  cnf(c652,plain,iext(uri_rdf_type,uri_rdfs_subClassOf,uri_rdf_Property),inference(resolution,[status(thm)],[c576, c151])).
% 3.71/3.91  cnf(c1066,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X650)|iext(X650,uri_rdfs_subClassOf,uri_rdf_Property),inference(resolution,[status(thm)],[c652, c44])).
% 3.71/3.91  cnf(c568,plain,ip(uri_rdfs_range),inference(resolution,[status(thm)],[c170, c67])).
% 3.71/3.91  cnf(c651,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_range,uri_rdfs_range),inference(resolution,[status(thm)],[c568, c36])).
% 3.71/3.91  cnf(c1056,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X649)|iext(X649,uri_rdfs_range,uri_rdfs_range),inference(resolution,[status(thm)],[c651, c44])).
% 3.71/3.91  cnf(c650,plain,iext(uri_rdf_type,uri_rdfs_range,uri_rdf_Property),inference(resolution,[status(thm)],[c568, c151])).
% 3.71/3.91  cnf(c1040,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X647)|iext(X647,uri_rdfs_range,uri_rdf_Property),inference(resolution,[status(thm)],[c650, c44])).
% 3.71/3.91  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.71/3.91  cnf(c28,plain,iext(uri_rdfs_domain,uri_rdf_value,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_value_domain])).
% 3.71/3.91  cnf(c567,plain,ip(uri_rdfs_domain),inference(resolution,[status(thm)],[c170, c28])).
% 3.71/3.91  cnf(c649,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,uri_rdfs_domain),inference(resolution,[status(thm)],[c567, c36])).
% 3.71/3.91  cnf(c1030,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X646)|iext(X646,uri_rdfs_domain,uri_rdfs_domain),inference(resolution,[status(thm)],[c649, c44])).
% 3.71/3.91  cnf(c648,plain,iext(uri_rdf_type,uri_rdfs_domain,uri_rdf_Property),inference(resolution,[status(thm)],[c567, c151])).
% 3.71/3.91  cnf(c1015,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X644)|iext(X644,uri_rdfs_domain,uri_rdf_Property),inference(resolution,[status(thm)],[c648, c44])).
% 3.71/3.91  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.71/3.91  cnf(c160,plain,iext(uri_rdf_type,uri_rdf_first,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_collection_first_type])).
% 3.71/3.91  cnf(c559,plain,ip(uri_rdf_first),inference(resolution,[status(thm)],[c160, c150])).
% 3.71/3.91  cnf(c564,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_first,uri_rdf_first),inference(resolution,[status(thm)],[c559, c36])).
% 3.71/3.91  cnf(c1005,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X643)|iext(X643,uri_rdf_first,uri_rdf_first),inference(resolution,[status(thm)],[c564, c44])).
% 3.71/3.91  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.71/3.91  cnf(c158,plain,iext(uri_rdf_type,uri_rdf_rest,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_collection_rest_type])).
% 3.71/3.91  cnf(c546,plain,ip(uri_rdf_rest),inference(resolution,[status(thm)],[c158, c150])).
% 3.71/3.91  cnf(c551,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_rest,uri_rdf_rest),inference(resolution,[status(thm)],[c546, c36])).
% 3.71/3.91  cnf(c992,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X641)|iext(X641,uri_rdf_rest,uri_rdf_rest),inference(resolution,[status(thm)],[c551, c44])).
% 3.71/3.91  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.71/3.91  cnf(c157,plain,iext(uri_rdf_type,uri_rdf__1,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_container_n_type_001])).
% 3.71/3.91  cnf(c538,plain,ip(uri_rdf__1),inference(resolution,[status(thm)],[c157, c150])).
% 3.71/3.91  cnf(c543,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__1,uri_rdf__1),inference(resolution,[status(thm)],[c538, c36])).
% 3.71/3.91  cnf(c977,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X639)|iext(X639,uri_rdf__1,uri_rdf__1),inference(resolution,[status(thm)],[c543, c44])).
% 3.71/3.91  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.71/3.91  cnf(c156,plain,iext(uri_rdf_type,uri_rdf__2,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_container_n_type_002])).
% 3.71/3.91  cnf(c530,plain,ip(uri_rdf__2),inference(resolution,[status(thm)],[c156, c150])).
% 3.71/3.91  cnf(c535,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__2,uri_rdf__2),inference(resolution,[status(thm)],[c530, c36])).
% 3.71/3.91  cnf(c969,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X637)|iext(X637,uri_rdf__2,uri_rdf__2),inference(resolution,[status(thm)],[c535, c44])).
% 3.71/3.91  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.71/3.91  cnf(c155,plain,iext(uri_rdf_type,uri_rdf__3,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_container_n_type_003])).
% 3.71/3.91  cnf(c522,plain,ip(uri_rdf__3),inference(resolution,[status(thm)],[c155, c150])).
% 3.71/3.91  cnf(c527,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__3,uri_rdf__3),inference(resolution,[status(thm)],[c522, c36])).
% 3.71/3.91  cnf(c961,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X635)|iext(X635,uri_rdf__3,uri_rdf__3),inference(resolution,[status(thm)],[c527, c44])).
% 3.71/3.91  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.71/3.91  cnf(c154,plain,iext(uri_rdf_type,uri_rdf_object,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_reification_object_type])).
% 3.71/3.91  cnf(c514,plain,ip(uri_rdf_object),inference(resolution,[status(thm)],[c154, c150])).
% 3.71/3.91  cnf(c519,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_object,uri_rdf_object),inference(resolution,[status(thm)],[c514, c36])).
% 3.71/3.91  cnf(c953,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X633)|iext(X633,uri_rdf_object,uri_rdf_object),inference(resolution,[status(thm)],[c519, c44])).
% 3.71/3.91  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.71/3.91  cnf(c153,plain,iext(uri_rdf_type,uri_rdf_value,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_reification_predicate_type])).
% 3.71/3.91  cnf(c502,plain,ip(uri_rdf_value),inference(resolution,[status(thm)],[c153, c150])).
% 3.71/3.91  cnf(c511,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_value,uri_rdf_value),inference(resolution,[status(thm)],[c502, c36])).
% 3.71/3.91  cnf(c945,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X631)|iext(X631,uri_rdf_value,uri_rdf_value),inference(resolution,[status(thm)],[c511, c44])).
% 3.71/3.91  cnf(c42,plain,~iext(uri_rdfs_subPropertyOf,X61,X60)|ip(X61),inference(split_conjunct,[status(thm)],[c41])).
% 3.71/3.91  cnf(c440,plain,ip(uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c139, c42])).
% 3.71/3.91  cnf(c507,plain,iext(uri_rdf_type,uri_rdfs_isDefinedBy,uri_rdf_Property),inference(resolution,[status(thm)],[c151, c440])).
% 3.71/3.91  cnf(c936,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X629)|iext(X629,uri_rdfs_isDefinedBy,uri_rdf_Property),inference(resolution,[status(thm)],[c507, c44])).
% 3.71/3.91  cnf(c443,plain,ip(uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c139, c43])).
% 3.71/3.91  cnf(c506,plain,iext(uri_rdf_type,uri_rdfs_seeAlso,uri_rdf_Property),inference(resolution,[status(thm)],[c151, c443])).
% 3.71/3.91  cnf(c928,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X628)|iext(X628,uri_rdfs_seeAlso,uri_rdf_Property),inference(resolution,[status(thm)],[c506, c44])).
% 3.71/3.91  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.71/3.91  cnf(c152,plain,iext(uri_rdf_type,uri_rdf_subject,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_reification_subject_type])).
% 3.71/3.91  cnf(c495,plain,ip(uri_rdf_subject),inference(resolution,[status(thm)],[c152, c150])).
% 3.71/3.91  cnf(c499,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_subject,uri_rdf_subject),inference(resolution,[status(thm)],[c495, c36])).
% 3.71/3.91  cnf(c922,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X627)|iext(X627,uri_rdf_subject,uri_rdf_subject),inference(resolution,[status(thm)],[c499, c44])).
% 3.71/3.91  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.71/3.91  cnf(c144,plain,iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_value_type])).
% 3.71/3.91  cnf(c492,plain,ip(uri_rdf_type),inference(resolution,[status(thm)],[c150, c144])).
% 3.71/3.91  cnf(c493,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_type,uri_rdf_type),inference(resolution,[status(thm)],[c492, c36])).
% 3.71/3.91  cnf(c915,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X625)|iext(X625,uri_rdf_type,uri_rdf_type),inference(resolution,[status(thm)],[c493, c44])).
% 3.71/3.91  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.71/3.91  cnf(c105,plain,iext(uri_rdf_type,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),inference(split_conjunct,[status(thm)],[rdfs_container_n_type_003])).
% 3.71/3.91  cnf(c449,plain,icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__3),inference(resolution,[status(thm)],[c133, c105])).
% 3.71/3.91  cnf(c469,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__3,uri_rdfs_member),inference(resolution,[status(thm)],[c449, c119])).
% 3.71/3.91  cnf(c906,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X623)|iext(X623,uri_rdf__3,uri_rdfs_member),inference(resolution,[status(thm)],[c469, c44])).
% 3.71/3.91  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.71/3.91  fof(c31,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.71/3.91  fof(c32,plain,(![X11]:(![X12]:(![X13]:((~iext(uri_rdfs_subPropertyOf,X11,X12)|~iext(uri_rdfs_subPropertyOf,X12,X13))|iext(uri_rdfs_subPropertyOf,X11,X13))))),inference(variable_rename,[status(thm)],[c31])).
% 3.71/3.91  cnf(c33,plain,~iext(uri_rdfs_subPropertyOf,X56,X58)|~iext(uri_rdfs_subPropertyOf,X58,X57)|iext(uri_rdfs_subPropertyOf,X56,X57),inference(split_conjunct,[status(thm)],[c32])).
% 3.71/3.91  cnf(c904,plain,~iext(uri_rdfs_subPropertyOf,X622,uri_rdf__3)|iext(uri_rdfs_subPropertyOf,X622,uri_rdfs_member),inference(resolution,[status(thm)],[c469, c33])).
% 3.71/3.91  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.71/3.91  cnf(c98,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_datatype_sub])).
% 3.71/3.91  cnf(c243,plain,ic(uri_rdfs_Class),inference(resolution,[status(thm)],[c58, c98])).
% 3.71/3.91  cnf(c248,plain,icext(uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c243, c89])).
% 3.71/3.91  cnf(c466,plain,iext(uri_rdf_type,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c134, c248])).
% 3.71/3.91  cnf(c899,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X621)|iext(X621,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c466, c44])).
% 3.71/3.91  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.71/3.91  cnf(c116,plain,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_container_containermembershipproperty_sub])).
% 3.71/3.91  cnf(c377,plain,ic(uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c116, c57])).
% 3.71/3.91  cnf(c381,plain,icext(uri_rdfs_Class,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c377, c89])).
% 3.71/3.91  cnf(c464,plain,iext(uri_rdf_type,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Class),inference(resolution,[status(thm)],[c134, c381])).
% 3.71/3.91  cnf(c894,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X620)|iext(X620,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Class),inference(resolution,[status(thm)],[c464, c44])).
% 3.71/3.91  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.71/3.91  cnf(c103,plain,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[rdfs_dat_xmlliteral_sub])).
% 3.71/3.91  cnf(c231,plain,ic(uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c57, c103])).
% 3.71/3.91  cnf(c234,plain,icext(uri_rdfs_Class,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c231, c89])).
% 3.71/3.91  cnf(c463,plain,iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Class),inference(resolution,[status(thm)],[c134, c234])).
% 3.71/3.91  cnf(c889,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X619)|iext(X619,uri_rdf_XMLLiteral,uri_rdfs_Class),inference(resolution,[status(thm)],[c463, c44])).
% 3.71/3.91  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.71/3.91  cnf(c104,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Container),inference(split_conjunct,[status(thm)],[rdfs_container_seq_sub])).
% 3.71/3.91  cnf(c232,plain,ic(uri_rdfs_Seq),inference(resolution,[status(thm)],[c57, c104])).
% 3.71/3.91  cnf(c236,plain,icext(uri_rdfs_Class,uri_rdfs_Seq),inference(resolution,[status(thm)],[c232, c89])).
% 3.71/3.91  cnf(c462,plain,iext(uri_rdf_type,uri_rdfs_Seq,uri_rdfs_Class),inference(resolution,[status(thm)],[c134, c236])).
% 3.71/3.91  cnf(c884,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X618)|iext(X618,uri_rdfs_Seq,uri_rdfs_Class),inference(resolution,[status(thm)],[c462, c44])).
% 3.71/3.91  cnf(c233,plain,ic(uri_rdfs_Datatype),inference(resolution,[status(thm)],[c57, c98])).
% 3.71/3.91  cnf(c238,plain,icext(uri_rdfs_Class,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c233, c89])).
% 3.71/3.91  cnf(c459,plain,iext(uri_rdf_type,uri_rdfs_Datatype,uri_rdfs_Class),inference(resolution,[status(thm)],[c134, c238])).
% 3.71/3.91  cnf(c879,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X617)|iext(X617,uri_rdfs_Datatype,uri_rdfs_Class),inference(resolution,[status(thm)],[c459, c44])).
% 3.71/3.91  cnf(c242,plain,ic(uri_rdfs_Container),inference(resolution,[status(thm)],[c58, c104])).
% 3.71/3.91  cnf(c246,plain,icext(uri_rdfs_Class,uri_rdfs_Container),inference(resolution,[status(thm)],[c242, c89])).
% 3.71/3.91  cnf(c458,plain,iext(uri_rdf_type,uri_rdfs_Container,uri_rdfs_Class),inference(resolution,[status(thm)],[c134, c246])).
% 3.71/3.91  cnf(c874,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X616)|iext(X616,uri_rdfs_Container,uri_rdfs_Class),inference(resolution,[status(thm)],[c458, c44])).
% 3.71/3.91  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.71/3.91  cnf(c120,plain,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Container),inference(split_conjunct,[status(thm)],[rdfs_container_bag_sub])).
% 3.71/3.91  cnf(c390,plain,ic(uri_rdf_Bag),inference(resolution,[status(thm)],[c120, c57])).
% 3.71/3.91  cnf(c392,plain,icext(uri_rdfs_Class,uri_rdf_Bag),inference(resolution,[status(thm)],[c390, c89])).
% 3.71/3.91  cnf(c456,plain,iext(uri_rdf_type,uri_rdf_Bag,uri_rdfs_Class),inference(resolution,[status(thm)],[c134, c392])).
% 3.71/3.91  cnf(c869,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X615)|iext(X615,uri_rdf_Bag,uri_rdfs_Class),inference(resolution,[status(thm)],[c456, c44])).
% 3.71/3.91  cnf(c241,plain,ic(uri_rdfs_Literal),inference(resolution,[status(thm)],[c58, c103])).
% 3.71/3.91  cnf(c244,plain,icext(uri_rdfs_Class,uri_rdfs_Literal),inference(resolution,[status(thm)],[c241, c89])).
% 3.71/3.91  cnf(c455,plain,iext(uri_rdf_type,uri_rdfs_Literal,uri_rdfs_Class),inference(resolution,[status(thm)],[c134, c244])).
% 3.71/3.91  cnf(c864,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X614)|iext(X614,uri_rdfs_Literal,uri_rdfs_Class),inference(resolution,[status(thm)],[c455, c44])).
% 3.71/3.91  cnf(c1421,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X613)|icext(X613,uri_rdfs_comment),inference(resolution,[status(thm)],[c1416, c96])).
% 3.71/3.91  cnf(c1420,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X612)|icext(X612,uri_rdfs_comment),inference(resolution,[status(thm)],[c1416, c70])).
% 3.71/3.91  cnf(c402,plain,icext(uri_rdfs_Class,uri_rdf_Alt),inference(resolution,[status(thm)],[c400, c89])).
% 3.71/3.91  cnf(c454,plain,iext(uri_rdf_type,uri_rdf_Alt,uri_rdfs_Class),inference(resolution,[status(thm)],[c134, c402])).
% 3.71/3.91  cnf(c859,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X611)|iext(X611,uri_rdf_Alt,uri_rdfs_Class),inference(resolution,[status(thm)],[c454, c44])).
% 3.71/3.91  cnf(c1391,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X608)|icext(X608,uri_rdfs_label),inference(resolution,[status(thm)],[c1386, c96])).
% 3.71/3.91  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.71/3.91  cnf(c107,plain,iext(uri_rdf_type,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),inference(split_conjunct,[status(thm)],[rdfs_container_n_type_001])).
% 3.71/3.91  cnf(c447,plain,icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__1),inference(resolution,[status(thm)],[c133, c107])).
% 3.71/3.91  cnf(c453,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__1,uri_rdfs_member),inference(resolution,[status(thm)],[c447, c119])).
% 3.71/3.91  cnf(c854,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X607)|iext(X607,uri_rdf__1,uri_rdfs_member),inference(resolution,[status(thm)],[c453, c44])).
% 3.71/3.91  cnf(c1390,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X606)|icext(X606,uri_rdfs_label),inference(resolution,[status(thm)],[c1386, c70])).
% 3.71/3.91  cnf(c852,plain,~iext(uri_rdfs_subPropertyOf,X603,uri_rdf__1)|iext(uri_rdfs_subPropertyOf,X603,uri_rdfs_member),inference(resolution,[status(thm)],[c453, c33])).
% 3.71/3.91  cnf(c1357,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X601)|icext(X601,uri_rdf_List),inference(resolution,[status(thm)],[c1338, c70])).
% 3.71/3.91  cnf(c845,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X600)|iext(X600,uri_rdf__2,uri_rdfs_member),inference(resolution,[status(thm)],[c452, c44])).
% 3.71/3.91  cnf(c1349,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X599)|icext(X599,uri_rdf_List),inference(resolution,[status(thm)],[c1336, c96])).
% 3.71/3.91  cnf(c843,plain,~iext(uri_rdfs_subPropertyOf,X595,uri_rdf__2)|iext(uri_rdfs_subPropertyOf,X595,uri_rdfs_member),inference(resolution,[status(thm)],[c452, c33])).
% 3.71/3.91  cnf(c451,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_seeAlso,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c443, c36])).
% 3.71/3.91  cnf(c838,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X590)|iext(X590,uri_rdfs_seeAlso,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c451, c44])).
% 3.71/3.91  cnf(c1268,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X587)|icext(X587,uri_rdf_predicate),inference(resolution,[status(thm)],[c1263, c96])).
% 3.71/3.91  cnf(c1267,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X585)|icext(X585,uri_rdf_predicate),inference(resolution,[status(thm)],[c1263, c70])).
% 3.71/3.91  cnf(c450,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c440, c36])).
% 3.71/3.91  cnf(c831,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X581)|iext(X581,uri_rdfs_isDefinedBy,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c450, c44])).
% 3.71/3.91  cnf(c426,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Resource),inference(resolution,[status(thm)],[c128, c233])).
% 3.71/3.91  cnf(c824,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X570)|iext(X570,uri_rdfs_Datatype,uri_rdfs_Resource),inference(resolution,[status(thm)],[c426, c44])).
% 3.71/3.91  cnf(c1196,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X568)|icext(X568,uri_rdfs_Statement),inference(resolution,[status(thm)],[c1158, c70])).
% 3.71/3.91  cnf(c823,plain,~iext(uri_rdfs_subClassOf,X567,uri_rdfs_Datatype)|iext(uri_rdfs_subClassOf,X567,uri_rdfs_Resource),inference(resolution,[status(thm)],[c426, c48])).
% 3.71/3.91  cnf(c1189,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X566)|icext(X566,uri_rdfs_Statement),inference(resolution,[status(thm)],[c1156, c96])).
% 3.71/3.91  cnf(c425,plain,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Resource),inference(resolution,[status(thm)],[c128, c377])).
% 3.71/3.91  cnf(c816,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X562)|iext(X562,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Resource),inference(resolution,[status(thm)],[c425, c44])).
% 3.71/3.91  cnf(c1164,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X559)|icext(X559,uri_rdfs_member),inference(resolution,[status(thm)],[c847, c96])).
% 3.71/3.91  cnf(c815,plain,~iext(uri_rdfs_subClassOf,X558,uri_rdfs_ContainerMembershipProperty)|iext(uri_rdfs_subClassOf,X558,uri_rdfs_Resource),inference(resolution,[status(thm)],[c425, c48])).
% 3.71/3.91  cnf(c424,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Container,uri_rdfs_Resource),inference(resolution,[status(thm)],[c128, c242])).
% 3.71/3.91  cnf(c808,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X553)|iext(X553,uri_rdfs_Container,uri_rdfs_Resource),inference(resolution,[status(thm)],[c424, c44])).
% 3.71/3.91  cnf(c807,plain,~iext(uri_rdfs_subClassOf,X551,uri_rdfs_Container)|iext(uri_rdfs_subClassOf,X551,uri_rdfs_Resource),inference(resolution,[status(thm)],[c424, c48])).
% 3.71/3.91  cnf(c1136,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X550)|icext(X550,uri_rdfs_Resource),inference(resolution,[status(thm)],[c748, c96])).
% 3.71/3.91  cnf(c423,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Literal,uri_rdfs_Resource),inference(resolution,[status(thm)],[c128, c241])).
% 3.71/3.91  cnf(c800,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X548)|iext(X548,uri_rdfs_Literal,uri_rdfs_Resource),inference(resolution,[status(thm)],[c423, c44])).
% 3.71/3.91  cnf(c1127,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X547)|icext(X547,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c659, c96])).
% 3.71/3.91  cnf(c1125,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X546)|icext(X546,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c659, c70])).
% 3.71/3.91  cnf(c799,plain,~iext(uri_rdfs_subClassOf,X545,uri_rdfs_Literal)|iext(uri_rdfs_subClassOf,X545,uri_rdfs_Resource),inference(resolution,[status(thm)],[c423, c48])).
% 3.71/3.91  cnf(c1111,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X542)|icext(X542,uri_owl_unionOf),inference(resolution,[status(thm)],[c657, c96])).
% 3.71/3.91  cnf(c375,plain,ic(uri_rdf_Property),inference(resolution,[status(thm)],[c116, c58])).
% 3.71/3.91  cnf(c422,plain,iext(uri_rdfs_subClassOf,uri_rdf_Property,uri_rdfs_Resource),inference(resolution,[status(thm)],[c128, c375])).
% 3.71/3.91  cnf(c792,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X541)|iext(X541,uri_rdf_Property,uri_rdfs_Resource),inference(resolution,[status(thm)],[c422, c44])).
% 3.71/3.91  cnf(c1109,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X540)|icext(X540,uri_owl_unionOf),inference(resolution,[status(thm)],[c657, c70])).
% 3.71/3.91  cnf(c791,plain,~iext(uri_rdfs_subClassOf,X538,uri_rdf_Property)|iext(uri_rdfs_subClassOf,X538,uri_rdfs_Resource),inference(resolution,[status(thm)],[c422, c48])).
% 3.71/3.91  cnf(c1092,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X536)|icext(X536,uri_owl_oneOf),inference(resolution,[status(thm)],[c655, c96])).
% 3.71/3.91  cnf(c421,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c128, c243])).
% 3.71/3.91  cnf(c784,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X535)|iext(X535,uri_rdfs_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c421, c44])).
% 3.71/3.91  cnf(c1090,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X534)|icext(X534,uri_owl_oneOf),inference(resolution,[status(thm)],[c655, c70])).
% 3.71/3.91  cnf(c783,plain,~iext(uri_rdfs_subClassOf,X531,uri_rdfs_Class)|iext(uri_rdfs_subClassOf,X531,uri_rdfs_Resource),inference(resolution,[status(thm)],[c421, c48])).
% 3.71/3.91  cnf(c1075,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X530)|icext(X530,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c653, c96])).
% 3.71/3.91  cnf(c1073,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X529)|icext(X529,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c653, c70])).
% 3.71/3.91  cnf(c420,plain,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Resource),inference(resolution,[status(thm)],[c128, c390])).
% 3.71/3.91  cnf(c776,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X528)|iext(X528,uri_rdf_Bag,uri_rdfs_Resource),inference(resolution,[status(thm)],[c420, c44])).
% 3.71/3.91  cnf(c1052,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X525)|icext(X525,uri_rdfs_range),inference(resolution,[status(thm)],[c651, c96])).
% 3.71/3.91  cnf(c775,plain,~iext(uri_rdfs_subClassOf,X524,uri_rdf_Bag)|iext(uri_rdfs_subClassOf,X524,uri_rdfs_Resource),inference(resolution,[status(thm)],[c420, c48])).
% 3.71/3.91  cnf(c1047,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X523)|icext(X523,uri_rdfs_range),inference(resolution,[status(thm)],[c651, c70])).
% 3.71/3.91  cnf(c419,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Resource),inference(resolution,[status(thm)],[c128, c232])).
% 3.71/3.91  cnf(c768,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X520)|iext(X520,uri_rdfs_Seq,uri_rdfs_Resource),inference(resolution,[status(thm)],[c419, c44])).
% 3.71/3.91  cnf(c1026,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X519)|icext(X519,uri_rdfs_domain),inference(resolution,[status(thm)],[c649, c96])).
% 3.71/3.91  cnf(c1024,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X518)|icext(X518,uri_rdfs_domain),inference(resolution,[status(thm)],[c649, c70])).
% 3.71/3.91  cnf(c767,plain,~iext(uri_rdfs_subClassOf,X517,uri_rdfs_Seq)|iext(uri_rdfs_subClassOf,X517,uri_rdfs_Resource),inference(resolution,[status(thm)],[c419, c48])).
% 3.71/3.91  cnf(c1001,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X514)|icext(X514,uri_rdf_first),inference(resolution,[status(thm)],[c564, c96])).
% 3.71/3.91  cnf(c418,plain,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Resource),inference(resolution,[status(thm)],[c128, c231])).
% 3.71/3.91  cnf(c760,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X513)|iext(X513,uri_rdf_XMLLiteral,uri_rdfs_Resource),inference(resolution,[status(thm)],[c418, c44])).
% 3.71/3.91  cnf(c999,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X512)|icext(X512,uri_rdf_first),inference(resolution,[status(thm)],[c564, c70])).
% 3.71/3.91  cnf(c987,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X511)|icext(X511,uri_rdf_rest),inference(resolution,[status(thm)],[c551, c96])).
% 3.71/3.91  cnf(c759,plain,~iext(uri_rdfs_subClassOf,X510,uri_rdf_XMLLiteral)|iext(uri_rdfs_subClassOf,X510,uri_rdfs_Resource),inference(resolution,[status(thm)],[c418, c48])).
% 3.71/3.91  cnf(c985,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X509)|icext(X509,uri_rdf_rest),inference(resolution,[status(thm)],[c551, c70])).
% 3.71/3.91  cnf(c747,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X507)|iext(X507,uri_rdf_Alt,uri_rdfs_Resource),inference(resolution,[status(thm)],[c417, c44])).
% 3.71/3.91  cnf(c974,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X506)|icext(X506,uri_rdf__1),inference(resolution,[status(thm)],[c543, c70])).
% 3.71/3.91  cnf(c966,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X504)|icext(X504,uri_rdf__2),inference(resolution,[status(thm)],[c535, c70])).
% 3.71/3.91  cnf(c746,plain,~iext(uri_rdfs_subClassOf,X503,uri_rdf_Alt)|iext(uri_rdfs_subClassOf,X503,uri_rdfs_Resource),inference(resolution,[status(thm)],[c417, c48])).
% 3.71/3.91  cnf(c958,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X501)|icext(X501,uri_rdf__3),inference(resolution,[status(thm)],[c527, c70])).
% 3.71/3.91  cnf(c403,plain,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdf_Alt),inference(resolution,[status(thm)],[c400, c51])).
% 3.71/3.91  cnf(c739,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X500)|iext(X500,uri_rdf_Alt,uri_rdf_Alt),inference(resolution,[status(thm)],[c403, c44])).
% 3.71/3.91  cnf(c952,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X499)|icext(X499,uri_rdf_object),inference(resolution,[status(thm)],[c519, c96])).
% 3.71/3.91  cnf(c950,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X498)|icext(X498,uri_rdf_object),inference(resolution,[status(thm)],[c519, c70])).
% 3.71/3.91  cnf(c944,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X497)|icext(X497,uri_rdf_value),inference(resolution,[status(thm)],[c511, c96])).
% 3.71/3.91  cnf(c942,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X495)|icext(X495,uri_rdf_value),inference(resolution,[status(thm)],[c511, c70])).
% 3.71/3.91  cnf(c393,plain,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdf_Bag),inference(resolution,[status(thm)],[c390, c51])).
% 3.71/3.91  cnf(c731,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X492)|iext(X492,uri_rdf_Bag,uri_rdf_Bag),inference(resolution,[status(thm)],[c393, c44])).
% 3.71/3.91  cnf(c921,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X489)|icext(X489,uri_rdf_subject),inference(resolution,[status(thm)],[c499, c96])).
% 3.71/3.91  cnf(c919,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X487)|icext(X487,uri_rdf_subject),inference(resolution,[status(thm)],[c499, c70])).
% 3.71/3.91  cnf(c912,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X486)|icext(X486,uri_rdf_type),inference(resolution,[status(thm)],[c493, c96])).
% 3.71/3.91  cnf(c382,plain,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c377, c51])).
% 3.71/3.91  cnf(c723,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X485)|iext(X485,uri_rdfs_ContainerMembershipProperty,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c382, c44])).
% 3.71/3.91  cnf(c910,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X484)|icext(X484,uri_rdf_type),inference(resolution,[status(thm)],[c493, c70])).
% 3.71/3.91  cnf(c905,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X483)|icext(X483,uri_rdf__3),inference(resolution,[status(thm)],[c469, c96])).
% 3.71/3.91  cnf(c380,plain,iext(uri_rdfs_subClassOf,uri_rdf_Property,uri_rdf_Property),inference(resolution,[status(thm)],[c375, c51])).
% 3.71/3.91  cnf(c715,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X475)|iext(X475,uri_rdf_Property,uri_rdf_Property),inference(resolution,[status(thm)],[c380, c44])).
% 3.71/3.91  cnf(c249,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c243, c51])).
% 3.71/3.91  cnf(c707,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X464)|iext(X464,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c249, c44])).
% 3.71/3.91  cnf(c853,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X458)|icext(X458,uri_rdf__1),inference(resolution,[status(thm)],[c453, c96])).
% 3.71/3.91  cnf(c844,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X456)|icext(X456,uri_rdf__2),inference(resolution,[status(thm)],[c452, c96])).
% 3.71/3.91  cnf(c247,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Container,uri_rdfs_Container),inference(resolution,[status(thm)],[c242, c51])).
% 3.71/3.91  cnf(c699,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X455)|iext(X455,uri_rdfs_Container,uri_rdfs_Container),inference(resolution,[status(thm)],[c247, c44])).
% 3.71/3.91  cnf(c842,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X454)|icext(X454,uri_rdfs_member),inference(resolution,[status(thm)],[c452, c70])).
% 3.71/3.91  cnf(c837,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X453)|icext(X453,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c451, c96])).
% 3.71/3.91  cnf(c828,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X449)|icext(X449,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c450, c70])).
% 3.71/3.91  cnf(c245,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Literal,uri_rdfs_Literal),inference(resolution,[status(thm)],[c241, c51])).
% 3.71/3.91  cnf(c691,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X447)|iext(X447,uri_rdfs_Literal,uri_rdfs_Literal),inference(resolution,[status(thm)],[c245, c44])).
% 3.71/3.91  cnf(c239,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c233, c51])).
% 3.71/3.91  cnf(c683,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X436)|iext(X436,uri_rdfs_Datatype,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c239, c44])).
% 3.71/3.91  cnf(c237,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Seq),inference(resolution,[status(thm)],[c232, c51])).
% 3.71/3.91  cnf(c675,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X425)|iext(X425,uri_rdfs_Seq,uri_rdfs_Seq),inference(resolution,[status(thm)],[c237, c44])).
% 3.71/3.91  cnf(c742,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X424)|icext(X424,uri_rdfs_Resource),inference(resolution,[status(thm)],[c417, c70])).
% 3.71/3.91  cnf(c734,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X422)|icext(X422,uri_rdf_Alt),inference(resolution,[status(thm)],[c403, c70])).
% 3.71/3.91  cnf(c726,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X419)|icext(X419,uri_rdf_Bag),inference(resolution,[status(thm)],[c393, c70])).
% 3.71/3.91  cnf(c235,plain,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c231, c51])).
% 3.71/3.91  cnf(c667,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X417)|iext(X417,uri_rdf_XMLLiteral,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c235, c44])).
% 3.71/3.91  cnf(c718,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X416)|icext(X416,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c382, c70])).
% 3.71/3.91  cnf(c712,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X415)|icext(X415,uri_rdf_Property),inference(resolution,[status(thm)],[c380, c96])).
% 3.71/3.91  cnf(c704,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X412)|icext(X412,uri_rdfs_Class),inference(resolution,[status(thm)],[c249, c96])).
% 3.71/3.91  cnf(c558,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X410)|iext(X410,uri_rdf_first,uri_rdf_Property),inference(resolution,[status(thm)],[c160, c44])).
% 3.71/3.91  cnf(c696,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X409)|icext(X409,uri_rdfs_Container),inference(resolution,[status(thm)],[c247, c96])).
% 3.71/3.91  cnf(c688,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X407)|icext(X407,uri_rdfs_Literal),inference(resolution,[status(thm)],[c245, c96])).
% 3.71/3.91  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.71/3.91  cnf(c159,plain,iext(uri_rdf_type,uri_rdf_nil,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdf_collection_nil_type])).
% 3.71/3.91  cnf(c553,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X406)|iext(X406,uri_rdf_nil,uri_rdf_List),inference(resolution,[status(thm)],[c159, c44])).
% 3.71/3.91  cnf(c678,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X403)|icext(X403,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c239, c70])).
% 3.71/3.91  cnf(c545,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X402)|iext(X402,uri_rdf_rest,uri_rdf_Property),inference(resolution,[status(thm)],[c158, c44])).
% 3.71/3.91  cnf(c670,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X400)|icext(X400,uri_rdfs_Seq),inference(resolution,[status(thm)],[c237, c70])).
% 3.71/3.91  cnf(c537,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X398)|iext(X398,uri_rdf__1,uri_rdf_Property),inference(resolution,[status(thm)],[c157, c44])).
% 3.71/3.91  cnf(c662,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X397)|icext(X397,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c235, c70])).
% 3.71/3.91  cnf(c529,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X394)|iext(X394,uri_rdf__2,uri_rdf_Property),inference(resolution,[status(thm)],[c156, c44])).
% 3.71/3.91  cnf(c554,plain,~iext(uri_rdfs_range,uri_rdf_type,X392)|icext(X392,uri_rdf_List),inference(resolution,[status(thm)],[c159, c70])).
% 3.71/3.91  cnf(c521,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X390)|iext(X390,uri_rdf__3,uri_rdf_Property),inference(resolution,[status(thm)],[c155, c44])).
% 3.71/3.91  cnf(c513,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X385)|iext(X385,uri_rdf_object,uri_rdf_Property),inference(resolution,[status(thm)],[c154, c44])).
% 3.71/3.91  cnf(c501,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X380)|iext(X380,uri_rdf_value,uri_rdf_Property),inference(resolution,[status(thm)],[c153, c44])).
% 3.71/3.91  cnf(c494,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X375)|iext(X375,uri_rdf_subject,uri_rdf_Property),inference(resolution,[status(thm)],[c152, c44])).
% 3.71/3.91  cnf(c488,plain,~iext(uri_rdfs_range,uri_rdf_type,X372)|icext(X372,uri_rdf_Property),inference(resolution,[status(thm)],[c144, c70])).
% 3.71/3.91  cnf(c487,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X371)|iext(X371,uri_rdf_type,uri_rdf_Property),inference(resolution,[status(thm)],[c144, c44])).
% 3.71/3.91  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.71/3.91  cnf(c143,plain,iext(uri_rdfs_domain,uri_rdfs_comment,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_comment_domain])).
% 3.71/3.91  cnf(c486,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X370)|icext(X370,uri_rdfs_comment),inference(resolution,[status(thm)],[c143, c96])).
% 3.71/3.91  cnf(c484,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X368)|iext(X368,uri_rdfs_comment,uri_rdfs_Resource),inference(resolution,[status(thm)],[c143, c44])).
% 3.71/3.91  cnf(c481,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X367)|iext(X367,uri_rdfs_comment,uri_rdfs_Literal),inference(resolution,[status(thm)],[c142, c44])).
% 3.71/3.91  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.71/3.91  cnf(c141,plain,iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_domain])).
% 3.71/3.91  cnf(c478,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X366)|iext(X366,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(resolution,[status(thm)],[c141, c44])).
% 3.71/3.91  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.71/3.91  cnf(c140,plain,iext(uri_rdfs_range,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_range])).
% 3.71/3.91  cnf(c475,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X363)|iext(X363,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(resolution,[status(thm)],[c140, c44])).
% 3.71/3.91  cnf(c480,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X362)|icext(X362,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c141, c96])).
% 3.71/3.91  cnf(c477,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X360)|icext(X360,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c140, c96])).
% 3.71/3.91  fof(simple_ir,axiom,(![X]:ir(X)),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', simple_ir)).
% 3.71/3.91  fof(c164,plain,(![X50]:ir(X50)),inference(variable_rename,[status(thm)],[simple_ir])).
% 3.71/3.91  cnf(c165,plain,ir(X54),inference(split_conjunct,[status(thm)],[c164])).
% 3.71/3.91  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.71/3.91  fof(c79,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.71/3.91  fof(c80,plain,((![X]:(~ir(X)|icext(uri_rdfs_Resource,X)))&(![X]:(~icext(uri_rdfs_Resource,X)|ir(X)))),inference(shift_quantors,[status(thm)],[c79])).
% 3.71/3.91  fof(c82,plain,(![X32]:(![X33]:((~ir(X32)|icext(uri_rdfs_Resource,X32))&(~icext(uri_rdfs_Resource,X33)|ir(X33))))),inference(shift_quantors,[status(thm)],[fof(c81,plain,((![X32]:(~ir(X32)|icext(uri_rdfs_Resource,X32)))&(![X33]:(~icext(uri_rdfs_Resource,X33)|ir(X33)))),inference(variable_rename,[status(thm)],[c80])).])).
% 3.71/3.91  cnf(c83,plain,~ir(X66)|icext(uri_rdfs_Resource,X66),inference(split_conjunct,[status(thm)],[c82])).
% 3.71/3.91  cnf(c172,plain,icext(uri_rdfs_Resource,X67),inference(resolution,[status(thm)],[c83, c165])).
% 3.71/3.91  cnf(c457,plain,iext(uri_rdf_type,X101,uri_rdfs_Resource),inference(resolution,[status(thm)],[c134, c172])).
% 3.71/3.91  cnf(c471,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X357)|iext(X357,X358,uri_rdfs_Resource),inference(resolution,[status(thm)],[c457, c44])).
% 3.71/3.91  cnf(c472,plain,~iext(uri_rdfs_range,uri_rdf_type,X355)|icext(X355,uri_rdfs_Resource),inference(resolution,[status(thm)],[c457, c70])).
% 3.71/3.91  cnf(c442,plain,~iext(uri_rdfs_subPropertyOf,X354,uri_rdfs_isDefinedBy)|iext(uri_rdfs_subPropertyOf,X354,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c139, c33])).
% 3.71/3.91  cnf(c444,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X353)|icext(X353,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c139, c96])).
% 3.71/3.91  cnf(c441,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X352)|icext(X352,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c139, c70])).
% 3.71/3.91  cnf(c439,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X351)|iext(X351,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c139, c44])).
% 3.71/3.91  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.71/3.91  cnf(c138,plain,iext(uri_rdfs_domain,uri_rdfs_label,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_label_domain])).
% 3.71/3.91  cnf(c438,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X350)|icext(X350,uri_rdfs_label),inference(resolution,[status(thm)],[c138, c96])).
% 3.71/3.91  cnf(c436,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X348)|iext(X348,uri_rdfs_label,uri_rdfs_Resource),inference(resolution,[status(thm)],[c138, c44])).
% 3.71/3.91  cnf(c433,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X347)|iext(X347,uri_rdfs_label,uri_rdfs_Literal),inference(resolution,[status(thm)],[c137, c44])).
% 3.71/3.91  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.71/3.91  cnf(c136,plain,iext(uri_rdfs_domain,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_seealso_domain])).
% 3.71/3.91  cnf(c430,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X346)|iext(X346,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(resolution,[status(thm)],[c136, c44])).
% 3.71/3.91  cnf(c434,plain,~iext(uri_rdfs_range,uri_rdfs_range,X344)|icext(X344,uri_rdfs_Literal),inference(resolution,[status(thm)],[c137, c70])).
% 3.71/3.91  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.71/3.91  cnf(c135,plain,iext(uri_rdfs_range,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_seealso_range])).
% 3.71/3.91  cnf(c427,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X343)|iext(X343,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(resolution,[status(thm)],[c135, c44])).
% 3.71/3.91  cnf(c432,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X342)|icext(X342,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c136, c96])).
% 3.71/3.91  cnf(c429,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X340)|icext(X340,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c135, c96])).
% 3.71/3.91  cnf(c414,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X339)|iext(X339,uri_rdf_first,uri_rdf_List),inference(resolution,[status(thm)],[c125, c44])).
% 3.71/3.91  cnf(c416,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X337)|icext(X337,uri_rdf_first),inference(resolution,[status(thm)],[c125, c96])).
% 3.71/3.91  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.71/3.91  cnf(c124,plain,iext(uri_rdfs_range,uri_rdf_first,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_collection_first_range])).
% 3.71/3.91  cnf(c411,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X335)|iext(X335,uri_rdf_first,uri_rdfs_Resource),inference(resolution,[status(thm)],[c124, c44])).
% 3.71/3.91  cnf(c413,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X334)|icext(X334,uri_rdf_first),inference(resolution,[status(thm)],[c124, c96])).
% 3.71/3.91  cnf(c408,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X332)|iext(X332,uri_rdf_rest,uri_rdf_List),inference(resolution,[status(thm)],[c123, c44])).
% 3.71/3.91  cnf(c410,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X331)|icext(X331,uri_rdf_rest),inference(resolution,[status(thm)],[c123, c96])).
% 3.71/3.91  cnf(c409,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X330)|icext(X330,uri_rdf_List),inference(resolution,[status(thm)],[c123, c70])).
% 3.71/3.91  cnf(c404,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X329)|iext(X329,uri_rdf_rest,uri_rdf_List),inference(resolution,[status(thm)],[c122, c44])).
% 3.71/3.91  cnf(c406,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X328)|icext(X328,uri_rdf_rest),inference(resolution,[status(thm)],[c122, c96])).
% 3.71/3.91  cnf(c396,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X325)|iext(X325,uri_rdf_Alt,uri_rdfs_Container),inference(resolution,[status(thm)],[c121, c44])).
% 3.71/3.91  cnf(c395,plain,~iext(uri_rdfs_subClassOf,X324,uri_rdf_Alt)|iext(uri_rdfs_subClassOf,X324,uri_rdfs_Container),inference(resolution,[status(thm)],[c121, c48])).
% 3.71/3.91  cnf(c386,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X323)|iext(X323,uri_rdf_Bag,uri_rdfs_Container),inference(resolution,[status(thm)],[c120, c44])).
% 3.71/3.91  cnf(c385,plain,~iext(uri_rdfs_subClassOf,X322,uri_rdf_Bag)|iext(uri_rdfs_subClassOf,X322,uri_rdfs_Container),inference(resolution,[status(thm)],[c120, c48])).
% 3.71/3.91  cnf(c399,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X320)|icext(X320,uri_rdf_Alt),inference(resolution,[status(thm)],[c121, c96])).
% 3.71/3.91  cnf(c373,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X319)|iext(X319,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),inference(resolution,[status(thm)],[c116, c44])).
% 3.71/3.91  cnf(c389,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X317)|icext(X317,uri_rdf_Bag),inference(resolution,[status(thm)],[c120, c96])).
% 3.71/3.91  cnf(c372,plain,~iext(uri_rdfs_subClassOf,X315,uri_rdfs_ContainerMembershipProperty)|iext(uri_rdfs_subClassOf,X315,uri_rdf_Property),inference(resolution,[status(thm)],[c116, c48])).
% 3.71/3.91  cnf(c376,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X314)|icext(X314,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c116, c96])).
% 3.71/3.91  cnf(c374,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X313)|icext(X313,uri_rdf_Property),inference(resolution,[status(thm)],[c116, c70])).
% 3.71/3.91  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.71/3.91  cnf(c62,plain,iext(uri_rdfs_domain,uri_rdf_subject,uri_rdfs_Statement),inference(split_conjunct,[status(thm)],[rdfs_reification_subject_domain])).
% 3.71/3.91  cnf(c371,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X312)|icext(X312,uri_rdf_subject),inference(resolution,[status(thm)],[c96, c62])).
% 3.71/3.91  cnf(c5,plain,iext(uri_rdf_first,skolem0002,uri_ex_w2),inference(split_conjunct,[status(thm)],[c1])).
% 3.71/3.91  cnf(c370,plain,~iext(uri_rdfs_domain,uri_rdf_first,X311)|icext(X311,skolem0002),inference(resolution,[status(thm)],[c96, c5])).
% 3.71/3.91  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.71/3.91  cnf(c29,plain,iext(uri_rdfs_range,uri_rdf_type,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_type_range])).
% 3.71/3.91  cnf(c369,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X310)|icext(X310,uri_rdf_type),inference(resolution,[status(thm)],[c96, c29])).
% 3.71/3.91  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.71/3.91  cnf(c115,plain,iext(uri_rdfs_domain,uri_rdfs_member,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_member_domain])).
% 3.71/3.91  cnf(c368,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X309)|icext(X309,uri_rdfs_member),inference(resolution,[status(thm)],[c96, c115])).
% 3.71/3.91  cnf(c367,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X308)|icext(X308,uri_rdfs_domain),inference(resolution,[status(thm)],[c96, c91])).
% 3.71/3.91  cnf(c20,plain,iext(uri_rdf_first,skolem0008,uri_ex_c1),inference(split_conjunct,[status(thm)],[c1])).
% 3.71/3.91  cnf(c366,plain,~iext(uri_rdfs_domain,uri_rdf_first,X307)|icext(X307,skolem0008),inference(resolution,[status(thm)],[c96, c20])).
% 3.71/3.91  cnf(c18,plain,iext(uri_rdf_rest,skolem0007,uri_rdf_nil),inference(split_conjunct,[status(thm)],[c1])).
% 3.71/3.91  cnf(c365,plain,~iext(uri_rdfs_domain,uri_rdf_rest,X306)|icext(X306,skolem0007),inference(resolution,[status(thm)],[c96, c18])).
% 3.71/3.91  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.71/3.91  cnf(c27,plain,iext(uri_rdfs_range,uri_rdf_value,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_value_range])).
% 3.71/3.91  cnf(c364,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X305)|icext(X305,uri_rdf_value),inference(resolution,[status(thm)],[c96, c27])).
% 3.71/3.91  cnf(c23,plain,iext(uri_rdf_rest,skolem0009,uri_rdf_nil),inference(split_conjunct,[status(thm)],[c1])).
% 3.71/3.91  cnf(c361,plain,~iext(uri_rdfs_domain,uri_rdf_rest,X302)|icext(X302,skolem0009),inference(resolution,[status(thm)],[c96, c23])).
% 3.71/3.91  cnf(c360,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X301)|icext(X301,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c96, c98])).
% 3.71/3.91  cnf(c359,plain,~iext(uri_rdfs_domain,uri_owl_unionOf,X300)|icext(X300,uri_ex_c4),inference(resolution,[status(thm)],[c96, c19])).
% 3.71/3.91  cnf(c22,plain,iext(uri_rdf_first,skolem0009,uri_ex_c2),inference(split_conjunct,[status(thm)],[c1])).
% 3.71/3.91  cnf(c358,plain,~iext(uri_rdfs_domain,uri_rdf_first,X299)|icext(X299,skolem0009),inference(resolution,[status(thm)],[c96, c22])).
% 3.71/3.91  cnf(c357,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X298)|icext(X298,uri_rdfs_Seq),inference(resolution,[status(thm)],[c96, c104])).
% 3.71/3.91  cnf(c356,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X297)|icext(X297,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c96, c103])).
% 3.71/3.91  cnf(c355,plain,~iext(uri_rdfs_domain,uri_rdf_rest,X296)|icext(X296,skolem0006),inference(resolution,[status(thm)],[c96, c16])).
% 3.71/3.91  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.71/3.91  cnf(c113,plain,iext(uri_rdfs_domain,uri_rdf__1,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_001])).
% 3.71/3.91  cnf(c354,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X295)|icext(X295,uri_rdf__1),inference(resolution,[status(thm)],[c96, c113])).
% 3.71/3.91  cnf(c17,plain,iext(uri_rdf_first,skolem0007,uri_ex_w3),inference(split_conjunct,[status(thm)],[c1])).
% 3.71/3.91  cnf(c352,plain,~iext(uri_rdfs_domain,uri_rdf_first,X293)|icext(X293,skolem0007),inference(resolution,[status(thm)],[c96, c17])).
% 3.71/3.91  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.71/3.91  cnf(c61,plain,iext(uri_rdfs_range,uri_rdf_subject,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_reification_subject_range])).
% 3.71/3.91  cnf(c350,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X291)|icext(X291,uri_rdf_subject),inference(resolution,[status(thm)],[c96, c61])).
% 3.71/3.91  cnf(c15,plain,iext(uri_rdf_first,skolem0006,uri_ex_w2),inference(split_conjunct,[status(thm)],[c1])).
% 3.71/3.91  cnf(c349,plain,~iext(uri_rdfs_domain,uri_rdf_first,X290)|icext(X290,skolem0006),inference(resolution,[status(thm)],[c96, c15])).
% 3.71/3.91  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.71/3.91  cnf(c108,plain,iext(uri_rdfs_range,uri_rdf__3,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_range_003])).
% 3.71/3.91  cnf(c348,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X289)|icext(X289,uri_rdf__3),inference(resolution,[status(thm)],[c96, c108])).
% 3.71/3.91  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.71/3.91  cnf(c60,plain,iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_subclassof_domain])).
% 3.71/3.91  cnf(c347,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X288)|icext(X288,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c96, c60])).
% 3.71/3.91  cnf(c346,plain,~iext(uri_rdfs_domain,uri_rdf_rest,X287)|icext(X287,skolem0005),inference(resolution,[status(thm)],[c96, c14])).
% 3.71/3.91  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.71/3.91  cnf(c45,plain,iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_subpropertyof_domain])).
% 3.71/3.91  cnf(c345,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X286)|icext(X286,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c96, c45])).
% 3.71/3.91  cnf(c12,plain,iext(uri_owl_oneOf,uri_ex_c3,skolem0005),inference(split_conjunct,[status(thm)],[c1])).
% 3.71/3.91  cnf(c344,plain,~iext(uri_rdfs_domain,uri_owl_oneOf,X285)|icext(X285,uri_ex_c3),inference(resolution,[status(thm)],[c96, c12])).
% 3.71/3.91  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.71/3.91  cnf(c112,plain,iext(uri_rdfs_domain,uri_rdf__2,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_002])).
% 3.71/3.91  cnf(c343,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X284)|icext(X284,uri_rdf__2),inference(resolution,[status(thm)],[c96, c112])).
% 3.71/3.91  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.71/3.91  cnf(c52,plain,iext(uri_rdfs_range,uri_rdfs_subClassOf,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_subclassof_range])).
% 3.71/3.91  cnf(c342,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X283)|icext(X283,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c96, c52])).
% 3.71/3.91  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.71/3.91  cnf(c114,plain,iext(uri_rdfs_range,uri_rdfs_member,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_member_range])).
% 3.71/3.91  cnf(c340,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X281)|icext(X281,uri_rdfs_member),inference(resolution,[status(thm)],[c96, c114])).
% 3.71/3.91  cnf(c10,plain,iext(uri_rdf_first,skolem0004,uri_ex_w3),inference(split_conjunct,[status(thm)],[c1])).
% 3.71/3.91  cnf(c338,plain,~iext(uri_rdfs_domain,uri_rdf_first,X279)|icext(X279,skolem0004),inference(resolution,[status(thm)],[c96, c10])).
% 3.71/3.91  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.71/3.91  cnf(c111,plain,iext(uri_rdfs_domain,uri_rdf__3,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_003])).
% 3.71/3.91  cnf(c337,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X278)|icext(X278,uri_rdf__3),inference(resolution,[status(thm)],[c96, c111])).
% 3.71/3.91  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.71/3.91  cnf(c37,plain,iext(uri_rdfs_range,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_subpropertyof_range])).
% 3.71/3.91  cnf(c336,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X277)|icext(X277,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c96, c37])).
% 3.71/3.91  cnf(c11,plain,iext(uri_rdf_rest,skolem0004,uri_rdf_nil),inference(split_conjunct,[status(thm)],[c1])).
% 3.71/3.91  cnf(c335,plain,~iext(uri_rdfs_domain,uri_rdf_rest,X276)|icext(X276,skolem0004),inference(resolution,[status(thm)],[c96, c11])).
% 3.71/3.91  cnf(c2,plain,iext(uri_owl_oneOf,uri_ex_c1,skolem0001),inference(split_conjunct,[status(thm)],[c1])).
% 3.71/3.91  cnf(c334,plain,~iext(uri_rdfs_domain,uri_owl_oneOf,X275)|icext(X275,uri_ex_c1),inference(resolution,[status(thm)],[c96, c2])).
% 3.71/3.91  cnf(c333,plain,~iext(uri_rdfs_domain,uri_rdf_rest,X274)|icext(X274,skolem0003),inference(resolution,[status(thm)],[c96, c9])).
% 3.71/3.91  cnf(c332,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X273)|icext(X273,uri_rdfs_range),inference(resolution,[status(thm)],[c96, c71])).
% 3.71/3.91  cnf(c6,plain,iext(uri_rdf_rest,skolem0002,uri_rdf_nil),inference(split_conjunct,[status(thm)],[c1])).
% 3.71/3.91  cnf(c329,plain,~iext(uri_rdfs_domain,uri_rdf_rest,X270)|icext(X270,skolem0002),inference(resolution,[status(thm)],[c96, c6])).
% 3.71/3.91  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.71/3.91  cnf(c64,plain,iext(uri_rdfs_domain,uri_rdf_predicate,uri_rdfs_Statement),inference(split_conjunct,[status(thm)],[rdfs_reification_predicate_domain])).
% 3.71/3.91  cnf(c327,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X268)|icext(X268,uri_rdf_predicate),inference(resolution,[status(thm)],[c96, c64])).
% 3.71/3.91  cnf(c326,plain,~iext(uri_rdfs_domain,uri_owl_oneOf,X267)|icext(X267,uri_ex_c2),inference(resolution,[status(thm)],[c96, c7])).
% 3.71/3.91  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.71/3.91  cnf(c109,plain,iext(uri_rdfs_range,uri_rdf__2,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_range_002])).
% 3.71/3.91  cnf(c325,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X266)|icext(X266,uri_rdf__2),inference(resolution,[status(thm)],[c96, c109])).
% 3.71/3.91  cnf(c323,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X264)|icext(X264,uri_rdf_object),inference(resolution,[status(thm)],[c96, c66])).
% 3.71/3.91  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.71/3.91  cnf(c110,plain,iext(uri_rdfs_range,uri_rdf__1,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_range_001])).
% 3.71/3.91  cnf(c322,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X263)|icext(X263,uri_rdf__1),inference(resolution,[status(thm)],[c96, c110])).
% 3.71/3.91  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.71/3.91  cnf(c30,plain,iext(uri_rdfs_domain,uri_rdf_type,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_type_domain])).
% 3.71/3.91  cnf(c321,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X262)|icext(X262,uri_rdf_type),inference(resolution,[status(thm)],[c96, c30])).
% 3.71/3.91  cnf(c320,plain,~iext(uri_rdfs_domain,uri_rdf_rest,X261)|icext(X261,skolem0001),inference(resolution,[status(thm)],[c96, c4])).
% 3.71/3.91  cnf(c319,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X260)|icext(X260,uri_rdfs_range),inference(resolution,[status(thm)],[c96, c67])).
% 3.71/3.91  cnf(c318,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X259)|icext(X259,uri_rdf_value),inference(resolution,[status(thm)],[c96, c28])).
% 3.71/3.91  cnf(c314,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X258)|iext(X258,uri_rdfs_member,uri_rdfs_Resource),inference(resolution,[status(thm)],[c115, c44])).
% 3.71/3.91  cnf(c316,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X256)|icext(X256,uri_rdfs_domain),inference(factor,[status(thm)],[c96])).
% 3.71/3.91  cnf(c312,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X254)|iext(X254,uri_rdfs_member,uri_rdfs_Resource),inference(resolution,[status(thm)],[c114, c44])).
% 3.71/3.91  cnf(c306,plain,~iext(uri_rdfs_range,uri_rdf_first,X248)|icext(X248,uri_ex_c1),inference(resolution,[status(thm)],[c70, c20])).
% 3.71/3.91  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.71/3.91  cnf(c102,plain,iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Datatype),inference(split_conjunct,[status(thm)],[rdfs_dat_xmlliteral_type])).
% 3.71/3.91  cnf(c302,plain,~iext(uri_rdfs_range,uri_rdf_type,X244)|icext(X244,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c70, c102])).
% 3.71/3.91  cnf(c300,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X242)|icext(X242,uri_rdfs_Class),inference(resolution,[status(thm)],[c70, c98])).
% 3.71/3.91  cnf(c299,plain,~iext(uri_rdfs_range,uri_owl_unionOf,X241)|icext(X241,skolem0008),inference(resolution,[status(thm)],[c70, c19])).
% 3.71/3.91  cnf(c298,plain,~iext(uri_rdfs_range,uri_rdf_first,X240)|icext(X240,uri_ex_c2),inference(resolution,[status(thm)],[c70, c22])).
% 3.71/3.91  cnf(c297,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X239)|icext(X239,uri_rdfs_Container),inference(resolution,[status(thm)],[c70, c104])).
% 3.71/3.91  cnf(c296,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X238)|icext(X238,uri_rdfs_Literal),inference(resolution,[status(thm)],[c70, c103])).
% 3.71/3.91  cnf(c473,plain,~iext(uri_rdfs_domain,uri_rdf_type,X231)|icext(X231,X230),inference(resolution,[status(thm)],[c457, c96])).
% 3.71/3.91  cnf(c287,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X208)|icext(X208,uri_rdfs_Class),inference(resolution,[status(thm)],[c70, c60])).
% 3.71/3.91  cnf(c59,plain,~iext(uri_rdfs_subClassOf,X85,X84)|~icext(X85,X83)|icext(X84,X83),inference(split_conjunct,[status(thm)],[c56])).
% 3.71/3.91  cnf(c401,plain,~icext(uri_rdf_Alt,X201)|icext(uri_rdfs_Container,X201),inference(resolution,[status(thm)],[c121, c59])).
% 3.71/3.91  cnf(c391,plain,~icext(uri_rdf_Bag,X199)|icext(uri_rdfs_Container,X199),inference(resolution,[status(thm)],[c120, c59])).
% 3.71/3.91  cnf(c378,plain,~icext(uri_rdfs_ContainerMembershipProperty,X198)|icext(uri_rdf_Property,X198),inference(resolution,[status(thm)],[c116, c59])).
% 3.71/3.91  cnf(c284,plain,~iext(uri_rdfs_range,uri_owl_oneOf,X197)|icext(X197,skolem0005),inference(resolution,[status(thm)],[c70, c12])).
% 3.71/3.91  cnf(c279,plain,~iext(uri_rdfs_range,uri_rdf_first,X192)|icext(X192,uri_ex_w3),inference(resolution,[status(thm)],[c70, c10])).
% 3.71/3.91  cnf(c277,plain,~iext(uri_rdfs_range,uri_rdfs_range,X190)|icext(X190,uri_rdf_Property),inference(resolution,[status(thm)],[c70, c37])).
% 3.71/3.91  cnf(c275,plain,~iext(uri_rdfs_range,uri_owl_oneOf,X188)|icext(X188,skolem0001),inference(resolution,[status(thm)],[c70, c2])).
% 3.71/3.91  cnf(c273,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X186)|icext(X186,uri_rdf_Property),inference(resolution,[status(thm)],[c70, c71])).
% 3.71/3.91  cnf(c272,plain,~iext(uri_rdfs_range,uri_rdf_first,X185)|icext(X185,uri_ex_w2),inference(resolution,[status(thm)],[c70, c8])).
% 3.71/3.91  cnf(c271,plain,~iext(uri_rdfs_range,uri_rdf_type,X184)|icext(X184,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c70, c106])).
% 3.71/3.91  cnf(c270,plain,~iext(uri_rdfs_range,uri_rdf_rest,X183)|icext(X183,uri_rdf_nil),inference(resolution,[status(thm)],[c70, c6])).
% 3.71/3.91  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.71/3.91  cnf(c72,plain,iext(uri_rdf_type,uri_rdf_Property,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_property_type])).
% 3.71/3.91  cnf(c269,plain,~iext(uri_rdfs_range,uri_rdf_type,X182)|icext(X182,uri_rdfs_Class),inference(resolution,[status(thm)],[c70, c72])).
% 3.71/3.91  cnf(c267,plain,~iext(uri_rdfs_range,uri_owl_oneOf,X180)|icext(X180,skolem0003),inference(resolution,[status(thm)],[c70, c7])).
% 3.71/3.91  cnf(c1147,plain,icext(uri_rdf_Property,uri_rdfs_member),inference(resolution,[status(thm)],[c846, c133])).
% 3.71/3.91  cnf(c263,plain,~iext(uri_rdfs_range,uri_rdfs_range,X176)|icext(X176,uri_rdfs_Resource),inference(resolution,[status(thm)],[c70, c110])).
% 3.71/3.91  cnf(c1115,plain,icext(uri_rdf_Property,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c658, c133])).
% 3.71/3.91  cnf(c260,plain,~iext(uri_rdfs_range,uri_rdfs_range,X173)|icext(X173,uri_rdfs_Class),inference(resolution,[status(thm)],[c70, c67])).
% 3.71/3.91  cnf(c259,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X172)|icext(X172,uri_rdfs_Resource),inference(resolution,[status(thm)],[c70, c28])).
% 3.71/3.91  cnf(c1098,plain,icext(uri_rdf_Property,uri_owl_unionOf),inference(resolution,[status(thm)],[c656, c133])).
% 3.71/3.91  cnf(c258,plain,~iext(uri_rdfs_range,uri_rdf_first,X171)|icext(X171,uri_ex_w1),inference(resolution,[status(thm)],[c70, c3])).
% 3.71/3.91  cnf(c257,plain,~iext(uri_rdfs_range,uri_rdfs_range,X170)|icext(X170,X170),inference(factor,[status(thm)],[c70])).
% 3.71/3.91  cnf(c1079,plain,icext(uri_rdf_Property,uri_owl_oneOf),inference(resolution,[status(thm)],[c654, c133])).
% 3.71/3.91  cnf(c253,plain,~icext(uri_rdfs_Datatype,X169)|icext(uri_rdfs_Class,X169),inference(resolution,[status(thm)],[c59, c98])).
% 3.71/3.91  cnf(c252,plain,~icext(uri_rdfs_Seq,X168)|icext(uri_rdfs_Container,X168),inference(resolution,[status(thm)],[c59, c104])).
% 3.71/3.91  cnf(c1062,plain,icext(uri_rdf_Property,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c652, c133])).
% 3.71/3.91  cnf(c251,plain,~icext(uri_rdf_XMLLiteral,X167)|icext(uri_rdfs_Literal,X167),inference(resolution,[status(thm)],[c59, c103])).
% 3.71/3.91  cnf(c1036,plain,icext(uri_rdf_Property,uri_rdfs_range),inference(resolution,[status(thm)],[c650, c133])).
% 3.71/3.91  cnf(c230,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X166)|iext(X166,uri_rdf__1,uri_rdfs_Resource),inference(resolution,[status(thm)],[c113, c44])).
% 3.71/3.91  cnf(c229,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X165)|iext(X165,uri_rdf__2,uri_rdfs_Resource),inference(resolution,[status(thm)],[c112, c44])).
% 3.71/3.91  cnf(c1011,plain,icext(uri_rdf_Property,uri_rdfs_domain),inference(resolution,[status(thm)],[c648, c133])).
% 3.71/3.91  cnf(c228,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X164)|iext(X164,uri_rdf__3,uri_rdfs_Resource),inference(resolution,[status(thm)],[c111, c44])).
% 3.71/3.91  cnf(c227,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X163)|iext(X163,uri_rdf__1,uri_rdfs_Resource),inference(resolution,[status(thm)],[c110, c44])).
% 3.71/3.91  cnf(c226,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X162)|iext(X162,uri_rdf__2,uri_rdfs_Resource),inference(resolution,[status(thm)],[c109, c44])).
% 3.71/3.91  cnf(c225,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X161)|iext(X161,uri_rdf__3,uri_rdfs_Resource),inference(resolution,[status(thm)],[c108, c44])).
% 3.71/3.91  cnf(c224,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X160)|iext(X160,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c107, c44])).
% 3.71/3.91  cnf(c223,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X159)|iext(X159,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c106, c44])).
% 3.71/3.91  cnf(c222,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X158)|iext(X158,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c105, c44])).
% 3.71/3.91  cnf(c221,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X157)|iext(X157,uri_rdfs_Seq,uri_rdfs_Container),inference(resolution,[status(thm)],[c104, c44])).
% 3.71/3.91  cnf(c220,plain,~iext(uri_rdfs_subClassOf,X156,uri_rdfs_Seq)|iext(uri_rdfs_subClassOf,X156,uri_rdfs_Container),inference(resolution,[status(thm)],[c104, c48])).
% 3.71/3.91  cnf(c219,plain,~iext(uri_rdfs_subClassOf,X155,uri_rdfs_Datatype)|iext(uri_rdfs_subClassOf,X155,uri_rdfs_Class),inference(resolution,[status(thm)],[c48, c98])).
% 3.71/3.91  cnf(c932,plain,icext(uri_rdf_Property,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c507, c133])).
% 3.71/3.91  cnf(c924,plain,icext(uri_rdf_Property,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c506, c133])).
% 3.71/3.91  cnf(c218,plain,~iext(uri_rdfs_subClassOf,X154,uri_rdf_XMLLiteral)|iext(uri_rdfs_subClassOf,X154,uri_rdfs_Literal),inference(resolution,[status(thm)],[c48, c103])).
% 3.71/3.91  cnf(c216,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X152)|iext(X152,uri_rdf_XMLLiteral,uri_rdfs_Literal),inference(resolution,[status(thm)],[c103, c44])).
% 3.71/3.91  cnf(c215,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X151)|iext(X151,uri_rdf_XMLLiteral,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c102, c44])).
% 3.71/3.91  cnf(c214,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X150)|iext(X150,uri_rdfs_Datatype,uri_rdfs_Class),inference(resolution,[status(thm)],[c98, c44])).
% 3.71/3.91  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.71/3.91  cnf(c97,plain,iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_domain_domain])).
% 3.71/3.91  cnf(c213,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X149)|iext(X149,uri_rdfs_domain,uri_rdf_Property),inference(resolution,[status(thm)],[c97, c44])).
% 3.71/3.91  cnf(c212,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X148)|iext(X148,uri_rdfs_domain,uri_rdfs_Class),inference(resolution,[status(thm)],[c91, c44])).
% 3.71/3.91  cnf(c211,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X147)|iext(X147,uri_rdf_subject,uri_rdfs_Statement),inference(resolution,[status(thm)],[c44, c62])).
% 3.71/3.91  cnf(c210,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_first,X146)|iext(X146,skolem0002,uri_ex_w2),inference(resolution,[status(thm)],[c44, c5])).
% 3.71/3.91  cnf(c209,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X145)|iext(X145,uri_rdf_type,uri_rdfs_Class),inference(resolution,[status(thm)],[c44, c29])).
% 3.71/3.91  cnf(c208,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_first,X144)|iext(X144,skolem0008,uri_ex_c1),inference(resolution,[status(thm)],[c44, c20])).
% 3.71/3.91  cnf(c207,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X143)|iext(X143,skolem0007,uri_rdf_nil),inference(resolution,[status(thm)],[c44, c18])).
% 3.71/3.91  cnf(c206,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X142)|iext(X142,uri_rdf_value,uri_rdfs_Resource),inference(resolution,[status(thm)],[c44, c27])).
% 3.71/3.91  cnf(c205,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X141)|iext(X141,skolem0009,uri_rdf_nil),inference(resolution,[status(thm)],[c44, c23])).
% 3.71/3.91  cnf(c204,plain,~iext(uri_rdfs_subPropertyOf,uri_owl_unionOf,X140)|iext(X140,uri_ex_c4,skolem0008),inference(resolution,[status(thm)],[c44, c19])).
% 3.71/3.91  cnf(c203,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_first,X139)|iext(X139,skolem0009,uri_ex_c2),inference(resolution,[status(thm)],[c44, c22])).
% 3.71/3.91  cnf(c202,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X138)|iext(X138,skolem0006,skolem0007),inference(resolution,[status(thm)],[c44, c16])).
% 3.71/3.91  cnf(c201,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X137)|iext(X137,skolem0008,skolem0009),inference(resolution,[status(thm)],[c44, c21])).
% 3.71/3.91  cnf(c200,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_first,X136)|iext(X136,skolem0007,uri_ex_w3),inference(resolution,[status(thm)],[c44, c17])).
% 3.71/3.91  cnf(c199,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X135)|iext(X135,uri_rdf_subject,uri_rdfs_Resource),inference(resolution,[status(thm)],[c44, c61])).
% 3.71/3.91  cnf(c198,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_first,X134)|iext(X134,skolem0006,uri_ex_w2),inference(resolution,[status(thm)],[c44, c15])).
% 3.71/3.91  cnf(c197,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X133)|iext(X133,uri_rdfs_subClassOf,uri_rdfs_Class),inference(resolution,[status(thm)],[c44, c60])).
% 3.71/3.91  cnf(c196,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X132)|iext(X132,skolem0005,skolem0006),inference(resolution,[status(thm)],[c44, c14])).
% 3.71/3.91  cnf(c195,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X131)|iext(X131,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c44, c45])).
% 3.71/3.91  cnf(c194,plain,~iext(uri_rdfs_subPropertyOf,uri_owl_oneOf,X130)|iext(X130,uri_ex_c3,skolem0005),inference(resolution,[status(thm)],[c44, c12])).
% 3.71/3.91  cnf(c193,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X129)|iext(X129,uri_rdfs_subClassOf,uri_rdfs_Class),inference(resolution,[status(thm)],[c44, c52])).
% 3.71/3.91  cnf(c192,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_first,X128)|iext(X128,skolem0005,uri_ex_w1),inference(resolution,[status(thm)],[c44, c13])).
% 3.71/3.91  cnf(c191,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_first,X127)|iext(X127,skolem0004,uri_ex_w3),inference(resolution,[status(thm)],[c44, c10])).
% 3.71/3.91  cnf(c190,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X126)|iext(X126,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c44, c37])).
% 3.71/3.91  cnf(c189,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X125)|iext(X125,skolem0004,uri_rdf_nil),inference(resolution,[status(thm)],[c44, c11])).
% 3.71/3.91  cnf(c188,plain,~iext(uri_rdfs_subPropertyOf,uri_owl_oneOf,X124)|iext(X124,uri_ex_c1,skolem0001),inference(resolution,[status(thm)],[c44, c2])).
% 3.71/3.91  cnf(c187,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X123)|iext(X123,skolem0003,skolem0004),inference(resolution,[status(thm)],[c44, c9])).
% 3.71/3.91  cnf(c186,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X122)|iext(X122,uri_rdfs_range,uri_rdf_Property),inference(resolution,[status(thm)],[c44, c71])).
% 3.71/3.91  cnf(c185,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_first,X121)|iext(X121,skolem0003,uri_ex_w2),inference(resolution,[status(thm)],[c44, c8])).
% 3.71/3.91  cnf(c184,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X120)|iext(X120,skolem0002,uri_rdf_nil),inference(resolution,[status(thm)],[c44, c6])).
% 3.71/3.91  cnf(c183,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X119)|iext(X119,uri_rdf_Property,uri_rdfs_Class),inference(resolution,[status(thm)],[c44, c72])).
% 3.71/3.91  cnf(c182,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X118)|iext(X118,uri_rdf_predicate,uri_rdfs_Statement),inference(resolution,[status(thm)],[c44, c64])).
% 3.71/3.91  cnf(c181,plain,~iext(uri_rdfs_subPropertyOf,uri_owl_oneOf,X117)|iext(X117,uri_ex_c2,skolem0003),inference(resolution,[status(thm)],[c44, c7])).
% 3.71/3.91  cnf(c180,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X116)|iext(X116,uri_rdf_predicate,uri_rdfs_Resource),inference(resolution,[status(thm)],[c44, c63])).
% 3.71/3.91  cnf(c179,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X115)|iext(X115,uri_rdf_object,uri_rdfs_Statement),inference(resolution,[status(thm)],[c44, c66])).
% 3.71/3.91  cnf(c178,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X114)|iext(X114,uri_rdf_type,uri_rdfs_Resource),inference(resolution,[status(thm)],[c44, c30])).
% 3.71/3.91  cnf(c177,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X113)|iext(X113,skolem0001,skolem0002),inference(resolution,[status(thm)],[c44, c4])).
% 3.71/3.91  cnf(c176,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X112)|iext(X112,uri_rdfs_range,uri_rdfs_Class),inference(resolution,[status(thm)],[c44, c67])).
% 3.71/3.91  cnf(c175,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X111)|iext(X111,uri_rdf_value,uri_rdfs_Resource),inference(resolution,[status(thm)],[c44, c28])).
% 3.71/3.91  cnf(c174,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_first,X110)|iext(X110,skolem0001,uri_ex_w1),inference(resolution,[status(thm)],[c44, c3])).
% 3.71/3.91  cnf(c173,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X109)|iext(X109,uri_rdfs_subPropertyOf,X109),inference(factor,[status(thm)],[c44])).
% 3.71/3.92  cnf(c562,plain,icext(uri_rdf_Property,uri_rdf_first),inference(resolution,[status(thm)],[c160, c133])).
% 3.71/3.92  cnf(c556,plain,icext(uri_rdf_List,uri_rdf_nil),inference(resolution,[status(thm)],[c159, c133])).
% 3.71/3.92  cnf(c549,plain,icext(uri_rdf_Property,uri_rdf_rest),inference(resolution,[status(thm)],[c158, c133])).
% 3.71/3.92  cnf(c541,plain,icext(uri_rdf_Property,uri_rdf__1),inference(resolution,[status(thm)],[c157, c133])).
% 3.71/3.92  cnf(c533,plain,icext(uri_rdf_Property,uri_rdf__2),inference(resolution,[status(thm)],[c156, c133])).
% 3.71/3.92  cnf(c525,plain,icext(uri_rdf_Property,uri_rdf__3),inference(resolution,[status(thm)],[c155, c133])).
% 3.71/3.92  cnf(c517,plain,icext(uri_rdf_Property,uri_rdf_object),inference(resolution,[status(thm)],[c154, c133])).
% 3.71/3.92  cnf(c505,plain,icext(uri_rdf_Property,uri_rdf_value),inference(resolution,[status(thm)],[c153, c133])).
% 3.71/3.92  cnf(c498,plain,icext(uri_rdf_Property,uri_rdf_subject),inference(resolution,[status(thm)],[c152, c133])).
% 3.71/3.92  cnf(c490,plain,icext(uri_rdf_Property,uri_rdf_type),inference(resolution,[status(thm)],[c144, c133])).
% 3.71/3.92  cnf(c448,plain,icext(uri_rdfs_Datatype,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c133, c102])).
% 3.71/3.92  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.71/3.92  fof(c99,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.71/3.92  fof(c100,plain,(![X40]:(~icext(uri_rdfs_Datatype,X40)|iext(uri_rdfs_subClassOf,X40,uri_rdfs_Literal))),inference(variable_rename,[status(thm)],[c99])).
% 3.71/3.92  cnf(c101,plain,~icext(uri_rdfs_Datatype,X94)|iext(uri_rdfs_subClassOf,X94,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[c100])).
% 3.71/3.92  cnf(c379,plain,icext(uri_rdfs_Class,uri_rdf_Property),inference(resolution,[status(thm)],[c375, c89])).
% 3.71/3.92  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.71/3.92  fof(c73,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.71/3.92  fof(c74,plain,((![X]:(~lv(X)|icext(uri_rdfs_Literal,X)))&(![X]:(~icext(uri_rdfs_Literal,X)|lv(X)))),inference(shift_quantors,[status(thm)],[c73])).
% 3.71/3.92  fof(c76,plain,(![X30]:(![X31]:((~lv(X30)|icext(uri_rdfs_Literal,X30))&(~icext(uri_rdfs_Literal,X31)|lv(X31))))),inference(shift_quantors,[status(thm)],[fof(c75,plain,((![X30]:(~lv(X30)|icext(uri_rdfs_Literal,X30)))&(![X31]:(~icext(uri_rdfs_Literal,X31)|lv(X31)))),inference(variable_rename,[status(thm)],[c74])).])).
% 3.71/3.92  cnf(c78,plain,~icext(uri_rdfs_Literal,X63)|lv(X63),inference(split_conjunct,[status(thm)],[c76])).
% 3.71/3.92  cnf(c77,plain,~lv(X62)|icext(uri_rdfs_Literal,X62),inference(split_conjunct,[status(thm)],[c76])).
% 3.71/3.92  fof(testcase_conclusion_fullish_021_Composite_Enumerations,conjecture,iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4),file('/export/starexec/sandbox/benchmark/theBenchmark.p', testcase_conclusion_fullish_021_Composite_Enumerations)).
% 3.71/3.92  fof(c24,negated_conjecture,(~iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4)),inference(assume_negation,[status(cth)],[testcase_conclusion_fullish_021_Composite_Enumerations])).
% 3.71/3.92  fof(c25,negated_conjecture,~iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4),inference(fof_simplification,[status(thm)],[c24])).
% 3.71/3.92  cnf(c26,negated_conjecture,~iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4),inference(split_conjunct,[status(thm)],[c25])).
% 3.71/3.92  % SZS output end Saturation
% 3.71/3.92  
% 3.71/3.92  % Initial clauses    : 112
% 3.71/3.92  % Processed clauses  : 627
% 3.71/3.92  % Factors computed   : 5
% 3.71/3.92  % Resolvents computed: 1422
% 3.71/3.92  % Tautologies deleted: 49
% 3.71/3.92  % Forward subsumed   : 863
% 3.71/3.92  % Backward subsumed  : 1
% 3.71/3.92  % -------- CPU Time ---------
% 3.71/3.92  % User time          : 3.535 s
% 3.71/3.92  % System time        : 0.023 s
% 3.71/3.92  % Total time         : 3.558 s
%------------------------------------------------------------------------------