PyRes---1.5.CSA-Sat.s

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

% Computer : n007.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:54 EDT 2024

% Result   : CounterSatisfiable 3.66s 3.83s
% Output   : Saturation 3.66s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12  % Problem  : SWB025+4 : TPTP v8.1.2. Released v5.2.0.
% 0.07/0.13  % Command  : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35  % Computer : n007.cluster.edu
% 0.13/0.35  % Model    : x86_64 x86_64
% 0.13/0.35  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35  % Memory   : 8042.1875MB
% 0.13/0.35  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35  % CPULimit : 300
% 0.13/0.35  % WCLimit  : 300
% 0.13/0.35  % DateTime : Wed May  8 22:08:23 EDT 2024
% 0.13/0.35  % CPUTime  : 
% 3.66/3.83  % Version:  1.5
% 3.66/3.83  % SZS status CounterSatisfiable
% 3.66/3.83  % SZS output start Saturation
% 3.66/3.83  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.66/3.83  fof(c32,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.66/3.83  fof(c34,plain,(![X11]:(![X12]:(![X13]:(![X14]:(~iext(uri_rdfs_subPropertyOf,X11,X12)|((ip(X11)&ip(X12))&(~iext(X11,X13,X14)|iext(X12,X13,X14)))))))),inference(shift_quantors,[status(thm)],[fof(c33,plain,(![X11]:(![X12]:(~iext(uri_rdfs_subPropertyOf,X11,X12)|((ip(X11)&ip(X12))&(![X13]:(![X14]:(~iext(X11,X13,X14)|iext(X12,X13,X14)))))))),inference(variable_rename,[status(thm)],[c32])).])).
% 3.66/3.83  fof(c35,plain,(![X11]:(![X12]:(![X13]:(![X14]:(((~iext(uri_rdfs_subPropertyOf,X11,X12)|ip(X11))&(~iext(uri_rdfs_subPropertyOf,X11,X12)|ip(X12)))&(~iext(uri_rdfs_subPropertyOf,X11,X12)|(~iext(X11,X13,X14)|iext(X12,X13,X14)))))))),inference(distribute,[status(thm)],[c34])).
% 3.66/3.83  cnf(c38,plain,~iext(uri_rdfs_subPropertyOf,X70,X69)|~iext(X70,X67,X68)|iext(X69,X67,X68),inference(split_conjunct,[status(thm)],[c35])).
% 3.66/3.83  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.66/3.83  fof(c28,plain,(![P]:(~ip(P)|iext(uri_rdfs_subPropertyOf,P,P))),inference(fof_nnf,[status(thm)],[rdfs_subpropertyof_reflex])).
% 3.66/3.83  fof(c29,plain,(![X10]:(~ip(X10)|iext(uri_rdfs_subPropertyOf,X10,X10))),inference(variable_rename,[status(thm)],[c28])).
% 3.66/3.83  cnf(c30,plain,~ip(X55)|iext(uri_rdfs_subPropertyOf,X55,X55),inference(split_conjunct,[status(thm)],[c29])).
% 3.66/3.83  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.66/3.83  fof(c140,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.66/3.83  fof(c141,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)],[c140])).
% 3.66/3.83  fof(c143,plain,(![X43]:(![X44]:((~iext(uri_rdf_type,X43,uri_rdf_Property)|ip(X43))&(~ip(X44)|iext(uri_rdf_type,X44,uri_rdf_Property))))),inference(shift_quantors,[status(thm)],[fof(c142,plain,((![X43]:(~iext(uri_rdf_type,X43,uri_rdf_Property)|ip(X43)))&(![X44]:(~ip(X44)|iext(uri_rdf_type,X44,uri_rdf_Property)))),inference(variable_rename,[status(thm)],[c141])).])).
% 3.66/3.83  cnf(c144,plain,~iext(uri_rdf_type,X99,uri_rdf_Property)|ip(X99),inference(split_conjunct,[status(thm)],[c143])).
% 3.66/3.83  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.66/3.83  fof(c123,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.66/3.83  fof(c124,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)],[c123])).
% 3.66/3.83  fof(c126,plain,(![X39]:(![X40]:(![X41]:(![X42]:((~iext(uri_rdf_type,X39,X40)|icext(X40,X39))&(~icext(X42,X41)|iext(uri_rdf_type,X41,X42))))))),inference(shift_quantors,[status(thm)],[fof(c125,plain,((![X39]:(![X40]:(~iext(uri_rdf_type,X39,X40)|icext(X40,X39))))&(![X41]:(![X42]:(~icext(X42,X41)|iext(uri_rdf_type,X41,X42))))),inference(variable_rename,[status(thm)],[c124])).])).
% 3.66/3.83  cnf(c128,plain,~icext(X96,X95)|iext(uri_rdf_type,X95,X96),inference(split_conjunct,[status(thm)],[c126])).
% 3.66/3.83  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.66/3.83  cnf(c65,plain,iext(uri_rdfs_domain,uri_rdfs_range,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_range_domain])).
% 3.66/3.83  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.66/3.83  fof(c86,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.66/3.83  fof(c87,plain,(![P]:(![C]:(![X]:((~iext(uri_rdfs_domain,P,C)|(![Y]:~iext(P,X,Y)))|icext(C,X))))),inference(shift_quantors,[status(thm)],[c86])).
% 3.66/3.83  fof(c89,plain,(![X32]:(![X33]:(![X34]:(![X35]:((~iext(uri_rdfs_domain,X32,X33)|~iext(X32,X34,X35))|icext(X33,X34)))))),inference(shift_quantors,[status(thm)],[fof(c88,plain,(![X32]:(![X33]:(![X34]:((~iext(uri_rdfs_domain,X32,X33)|(![X35]:~iext(X32,X34,X35)))|icext(X33,X34))))),inference(variable_rename,[status(thm)],[c87])).])).
% 3.66/3.83  cnf(c90,plain,~iext(uri_rdfs_domain,X89,X86)|~iext(X89,X88,X87)|icext(X86,X88),inference(split_conjunct,[status(thm)],[c89])).
% 3.66/3.83  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.66/3.83  cnf(c136,plain,iext(uri_rdfs_range,uri_rdfs_comment,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[rdfs_annotation_comment_range])).
% 3.66/3.83  cnf(c455,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X338)|icext(X338,uri_rdfs_comment),inference(resolution,[status(thm)],[c136, c90])).
% 3.66/3.83  cnf(c1368,plain,icext(uri_rdf_Property,uri_rdfs_comment),inference(resolution,[status(thm)],[c455, c65])).
% 3.66/3.83  cnf(c1370,plain,iext(uri_rdf_type,uri_rdfs_comment,uri_rdf_Property),inference(resolution,[status(thm)],[c1368, c128])).
% 3.66/3.83  cnf(c1373,plain,ip(uri_rdfs_comment),inference(resolution,[status(thm)],[c1370, c144])).
% 3.66/3.83  cnf(c1378,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_comment,uri_rdfs_comment),inference(resolution,[status(thm)],[c1373, c30])).
% 3.66/3.83  cnf(c1385,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X676)|iext(X676,uri_rdfs_comment,uri_rdfs_comment),inference(resolution,[status(thm)],[c1378, c38])).
% 3.66/3.83  cnf(c1375,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X674)|iext(X674,uri_rdfs_comment,uri_rdf_Property),inference(resolution,[status(thm)],[c1370, c38])).
% 3.66/3.83  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.66/3.83  cnf(c131,plain,iext(uri_rdfs_range,uri_rdfs_label,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[rdfs_annotation_label_range])).
% 3.66/3.83  cnf(c407,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X320)|icext(X320,uri_rdfs_label),inference(resolution,[status(thm)],[c131, c90])).
% 3.66/3.83  cnf(c1339,plain,icext(uri_rdf_Property,uri_rdfs_label),inference(resolution,[status(thm)],[c407, c65])).
% 3.66/3.83  cnf(c1340,plain,iext(uri_rdf_type,uri_rdfs_label,uri_rdf_Property),inference(resolution,[status(thm)],[c1339, c128])).
% 3.66/3.83  cnf(c1343,plain,ip(uri_rdfs_label),inference(resolution,[status(thm)],[c1340, c144])).
% 3.66/3.83  cnf(c1349,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_label,uri_rdfs_label),inference(resolution,[status(thm)],[c1343, c30])).
% 3.66/3.83  cnf(c1356,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X673)|iext(X673,uri_rdfs_label,uri_rdfs_label),inference(resolution,[status(thm)],[c1349, c38])).
% 3.66/3.83  cnf(c1345,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X671)|iext(X671,uri_rdfs_label,uri_rdf_Property),inference(resolution,[status(thm)],[c1340, c38])).
% 3.66/3.83  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.66/3.83  fof(c120,plain,(![C]:(~ic(C)|iext(uri_rdfs_subClassOf,C,uri_rdfs_Resource))),inference(fof_nnf,[status(thm)],[rdfs_class_instsub_resource])).
% 3.66/3.83  fof(c121,plain,(![X38]:(~ic(X38)|iext(uri_rdfs_subClassOf,X38,uri_rdfs_Resource))),inference(variable_rename,[status(thm)],[c120])).
% 3.66/3.83  cnf(c122,plain,~ic(X92)|iext(uri_rdfs_subClassOf,X92,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[c121])).
% 3.66/3.83  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.66/3.83  fof(c79,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.66/3.83  fof(c80,plain,((![X]:(~ic(X)|icext(uri_rdfs_Class,X)))&(![X]:(~icext(uri_rdfs_Class,X)|ic(X)))),inference(shift_quantors,[status(thm)],[c79])).
% 3.66/3.83  fof(c82,plain,(![X30]:(![X31]:((~ic(X30)|icext(uri_rdfs_Class,X30))&(~icext(uri_rdfs_Class,X31)|ic(X31))))),inference(shift_quantors,[status(thm)],[fof(c81,plain,((![X30]:(~ic(X30)|icext(uri_rdfs_Class,X30)))&(![X31]:(~icext(uri_rdfs_Class,X31)|ic(X31)))),inference(variable_rename,[status(thm)],[c80])).])).
% 3.66/3.83  cnf(c84,plain,~icext(uri_rdfs_Class,X66)|ic(X66),inference(split_conjunct,[status(thm)],[c82])).
% 3.66/3.83  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.66/3.83  cnf(c61,plain,iext(uri_rdfs_range,uri_rdfs_range,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_range_range])).
% 3.66/3.83  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.66/3.83  fof(c62,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.66/3.83  fof(c63,plain,(![X22]:(![X23]:(![X24]:(![X25]:((~iext(uri_rdfs_range,X22,X23)|~iext(X22,X24,X25))|icext(X23,X25)))))),inference(variable_rename,[status(thm)],[c62])).
% 3.66/3.83  cnf(c64,plain,~iext(uri_rdfs_range,X82,X85)|~iext(X82,X83,X84)|icext(X85,X84),inference(split_conjunct,[status(thm)],[c63])).
% 3.66/3.83  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.66/3.83  cnf(c116,plain,iext(uri_rdfs_range,uri_rdf_rest,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdfs_collection_rest_range])).
% 3.66/3.83  cnf(c380,plain,~iext(uri_rdfs_range,uri_rdfs_range,X299)|icext(X299,uri_rdf_List),inference(resolution,[status(thm)],[c116, c64])).
% 3.66/3.83  cnf(c1298,plain,icext(uri_rdfs_Class,uri_rdf_List),inference(resolution,[status(thm)],[c380, c61])).
% 3.66/3.83  cnf(c1300,plain,ic(uri_rdf_List),inference(resolution,[status(thm)],[c1298, c84])).
% 3.66/3.83  cnf(c1302,plain,iext(uri_rdfs_subClassOf,uri_rdf_List,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1300, c122])).
% 3.66/3.83  cnf(c1325,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X670)|iext(X670,uri_rdf_List,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1302, c38])).
% 3.66/3.83  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.66/3.83  fof(c40,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.66/3.83  fof(c41,plain,(![X15]:(![X16]:(![X17]:((~iext(uri_rdfs_subClassOf,X15,X16)|~iext(uri_rdfs_subClassOf,X16,X17))|iext(uri_rdfs_subClassOf,X15,X17))))),inference(variable_rename,[status(thm)],[c40])).
% 3.66/3.83  cnf(c42,plain,~iext(uri_rdfs_subClassOf,X73,X71)|~iext(uri_rdfs_subClassOf,X71,X72)|iext(uri_rdfs_subClassOf,X73,X72),inference(split_conjunct,[status(thm)],[c41])).
% 3.66/3.83  cnf(c1323,plain,~iext(uri_rdfs_subClassOf,X669,uri_rdf_List)|iext(uri_rdfs_subClassOf,X669,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1302, c42])).
% 3.66/3.83  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.66/3.83  fof(c43,plain,(![C]:(~ic(C)|iext(uri_rdfs_subClassOf,C,C))),inference(fof_nnf,[status(thm)],[rdfs_subclassof_reflex])).
% 3.66/3.83  fof(c44,plain,(![X18]:(~ic(X18)|iext(uri_rdfs_subClassOf,X18,X18))),inference(variable_rename,[status(thm)],[c43])).
% 3.66/3.83  cnf(c45,plain,~ic(X74)|iext(uri_rdfs_subClassOf,X74,X74),inference(split_conjunct,[status(thm)],[c44])).
% 3.66/3.83  cnf(c1301,plain,iext(uri_rdfs_subClassOf,uri_rdf_List,uri_rdf_List),inference(resolution,[status(thm)],[c1300, c45])).
% 3.66/3.83  cnf(c1316,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X668)|iext(X668,uri_rdf_List,uri_rdf_List),inference(resolution,[status(thm)],[c1301, c38])).
% 3.66/3.83  cnf(c1299,plain,iext(uri_rdf_type,uri_rdf_List,uri_rdfs_Class),inference(resolution,[status(thm)],[c1298, c128])).
% 3.66/3.83  cnf(c1308,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X666)|iext(X666,uri_rdf_List,uri_rdfs_Class),inference(resolution,[status(thm)],[c1299, c38])).
% 3.66/3.83  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.66/3.83  cnf(c119,plain,iext(uri_rdfs_domain,uri_rdf_first,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdfs_collection_first_domain])).
% 3.66/3.83  fof(testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties,axiom,(?[BNODE_l11]:(?[BNODE_l12]:(?[BNODE_l21]:(?[BNODE_l22]:(?[BNODE_l3]:((((((((((((((iext(uri_owl_propertyChainAxiom,uri_ex_hasUncle,BNODE_l11)&iext(uri_rdf_first,BNODE_l11,uri_ex_hasCousin))&iext(uri_rdf_rest,BNODE_l11,BNODE_l12))&iext(uri_rdf_first,BNODE_l12,uri_ex_hasFather))&iext(uri_rdf_rest,BNODE_l12,uri_rdf_nil))&iext(uri_owl_propertyChainAxiom,uri_ex_hasCousin,BNODE_l21))&iext(uri_rdf_first,BNODE_l21,uri_ex_hasUncle))&iext(uri_rdf_rest,BNODE_l21,BNODE_l22))&iext(uri_rdf_first,BNODE_l22,BNODE_l3))&iext(uri_rdf_rest,BNODE_l22,uri_rdf_nil))&iext(uri_owl_inverseOf,BNODE_l3,uri_ex_hasFather))&iext(uri_ex_hasFather,uri_ex_alice,uri_ex_dave))&iext(uri_ex_hasCousin,uri_ex_alice,uri_ex_bob))&iext(uri_ex_hasFather,uri_ex_bob,uri_ex_charly))&iext(uri_ex_hasUncle,uri_ex_bob,uri_ex_dave))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties)).
% 3.66/3.83  fof(c0,plain,(((((?[BNODE_l11]:(?[BNODE_l12]:(?[BNODE_l21]:(?[BNODE_l22]:(?[BNODE_l3]:((((((((((iext(uri_owl_propertyChainAxiom,uri_ex_hasUncle,BNODE_l11)&iext(uri_rdf_first,BNODE_l11,uri_ex_hasCousin))&iext(uri_rdf_rest,BNODE_l11,BNODE_l12))&iext(uri_rdf_first,BNODE_l12,uri_ex_hasFather))&iext(uri_rdf_rest,BNODE_l12,uri_rdf_nil))&iext(uri_owl_propertyChainAxiom,uri_ex_hasCousin,BNODE_l21))&iext(uri_rdf_first,BNODE_l21,uri_ex_hasUncle))&iext(uri_rdf_rest,BNODE_l21,BNODE_l22))&iext(uri_rdf_first,BNODE_l22,BNODE_l3))&iext(uri_rdf_rest,BNODE_l22,uri_rdf_nil))&iext(uri_owl_inverseOf,BNODE_l3,uri_ex_hasFather)))))))&iext(uri_ex_hasFather,uri_ex_alice,uri_ex_dave))&iext(uri_ex_hasCousin,uri_ex_alice,uri_ex_bob))&iext(uri_ex_hasFather,uri_ex_bob,uri_ex_charly))&iext(uri_ex_hasUncle,uri_ex_bob,uri_ex_dave)),inference(shift_quantors,[status(thm)],[testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties])).
% 3.66/3.83  fof(c1,plain,(((((?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:((((((((((iext(uri_owl_propertyChainAxiom,uri_ex_hasUncle,X2)&iext(uri_rdf_first,X2,uri_ex_hasCousin))&iext(uri_rdf_rest,X2,X3))&iext(uri_rdf_first,X3,uri_ex_hasFather))&iext(uri_rdf_rest,X3,uri_rdf_nil))&iext(uri_owl_propertyChainAxiom,uri_ex_hasCousin,X4))&iext(uri_rdf_first,X4,uri_ex_hasUncle))&iext(uri_rdf_rest,X4,X5))&iext(uri_rdf_first,X5,X6))&iext(uri_rdf_rest,X5,uri_rdf_nil))&iext(uri_owl_inverseOf,X6,uri_ex_hasFather)))))))&iext(uri_ex_hasFather,uri_ex_alice,uri_ex_dave))&iext(uri_ex_hasCousin,uri_ex_alice,uri_ex_bob))&iext(uri_ex_hasFather,uri_ex_bob,uri_ex_charly))&iext(uri_ex_hasUncle,uri_ex_bob,uri_ex_dave)),inference(variable_rename,[status(thm)],[c0])).
% 3.66/3.83  fof(c2,plain,((((((((((((((iext(uri_owl_propertyChainAxiom,uri_ex_hasUncle,skolem0001)&iext(uri_rdf_first,skolem0001,uri_ex_hasCousin))&iext(uri_rdf_rest,skolem0001,skolem0002))&iext(uri_rdf_first,skolem0002,uri_ex_hasFather))&iext(uri_rdf_rest,skolem0002,uri_rdf_nil))&iext(uri_owl_propertyChainAxiom,uri_ex_hasCousin,skolem0003))&iext(uri_rdf_first,skolem0003,uri_ex_hasUncle))&iext(uri_rdf_rest,skolem0003,skolem0004))&iext(uri_rdf_first,skolem0004,skolem0005))&iext(uri_rdf_rest,skolem0004,uri_rdf_nil))&iext(uri_owl_inverseOf,skolem0005,uri_ex_hasFather))&iext(uri_ex_hasFather,uri_ex_alice,uri_ex_dave))&iext(uri_ex_hasCousin,uri_ex_alice,uri_ex_bob))&iext(uri_ex_hasFather,uri_ex_bob,uri_ex_charly))&iext(uri_ex_hasUncle,uri_ex_bob,uri_ex_dave)),inference(skolemize,[status(esa)],[c1])).
% 3.66/3.83  cnf(c9,plain,iext(uri_rdf_first,skolem0003,uri_ex_hasUncle),inference(split_conjunct,[status(thm)],[c2])).
% 3.66/3.83  cnf(c336,plain,~iext(uri_rdfs_domain,uri_rdf_first,X276)|icext(X276,skolem0003),inference(resolution,[status(thm)],[c90, c9])).
% 3.66/3.83  cnf(c1274,plain,icext(uri_rdf_List,skolem0003),inference(resolution,[status(thm)],[c336, c119])).
% 3.66/3.83  cnf(c1275,plain,iext(uri_rdf_type,skolem0003,uri_rdf_List),inference(resolution,[status(thm)],[c1274, c128])).
% 3.66/3.83  cnf(c1279,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X665)|iext(X665,skolem0003,uri_rdf_List),inference(resolution,[status(thm)],[c1275, c38])).
% 3.66/3.83  cnf(c4,plain,iext(uri_rdf_first,skolem0001,uri_ex_hasCousin),inference(split_conjunct,[status(thm)],[c2])).
% 3.66/3.83  cnf(c335,plain,~iext(uri_rdfs_domain,uri_rdf_first,X275)|icext(X275,skolem0001),inference(resolution,[status(thm)],[c90, c4])).
% 3.66/3.83  cnf(c1267,plain,icext(uri_rdf_List,skolem0001),inference(resolution,[status(thm)],[c335, c119])).
% 3.66/3.83  cnf(c1268,plain,iext(uri_rdf_type,skolem0001,uri_rdf_List),inference(resolution,[status(thm)],[c1267, c128])).
% 3.66/3.83  cnf(c1272,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X664)|iext(X664,skolem0001,uri_rdf_List),inference(resolution,[status(thm)],[c1268, c38])).
% 3.66/3.83  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.66/3.83  cnf(c57,plain,iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_reification_predicate_range])).
% 3.66/3.83  cnf(c326,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X266)|icext(X266,uri_rdf_predicate),inference(resolution,[status(thm)],[c90, c57])).
% 3.66/3.83  cnf(c1245,plain,icext(uri_rdf_Property,uri_rdf_predicate),inference(resolution,[status(thm)],[c326, c65])).
% 3.66/3.83  cnf(c1246,plain,iext(uri_rdf_type,uri_rdf_predicate,uri_rdf_Property),inference(resolution,[status(thm)],[c1245, c128])).
% 3.66/3.83  cnf(c1249,plain,ip(uri_rdf_predicate),inference(resolution,[status(thm)],[c1246, c144])).
% 3.66/3.83  cnf(c1254,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_predicate,uri_rdf_predicate),inference(resolution,[status(thm)],[c1249, c30])).
% 3.66/3.83  cnf(c1261,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X663)|iext(X663,uri_rdf_predicate,uri_rdf_predicate),inference(resolution,[status(thm)],[c1254, c38])).
% 3.66/3.83  cnf(c1251,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X661)|iext(X661,uri_rdf_predicate,uri_rdf_Property),inference(resolution,[status(thm)],[c1246, c38])).
% 3.66/3.83  cnf(c5,plain,iext(uri_rdf_rest,skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c2])).
% 3.66/3.83  cnf(c284,plain,~iext(uri_rdfs_range,uri_rdf_rest,X215)|icext(X215,skolem0002),inference(resolution,[status(thm)],[c64, c5])).
% 3.66/3.83  cnf(c1212,plain,icext(uri_rdf_List,skolem0002),inference(resolution,[status(thm)],[c284, c116])).
% 3.66/3.83  cnf(c1213,plain,iext(uri_rdf_type,skolem0002,uri_rdf_List),inference(resolution,[status(thm)],[c1212, c128])).
% 3.66/3.83  cnf(c1217,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X660)|iext(X660,skolem0002,uri_rdf_List),inference(resolution,[status(thm)],[c1213, c38])).
% 3.66/3.83  cnf(c10,plain,iext(uri_rdf_rest,skolem0003,skolem0004),inference(split_conjunct,[status(thm)],[c2])).
% 3.66/3.83  cnf(c280,plain,~iext(uri_rdfs_range,uri_rdf_rest,X197)|icext(X197,skolem0004),inference(resolution,[status(thm)],[c64, c10])).
% 3.66/3.83  cnf(c1203,plain,icext(uri_rdf_List,skolem0004),inference(resolution,[status(thm)],[c280, c116])).
% 3.66/3.83  cnf(c1204,plain,iext(uri_rdf_type,skolem0004,uri_rdf_List),inference(resolution,[status(thm)],[c1203, c128])).
% 3.66/3.83  cnf(c1207,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X659)|iext(X659,skolem0004,uri_rdf_List),inference(resolution,[status(thm)],[c1204, c38])).
% 3.66/3.83  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.66/3.83  cnf(c85,plain,iext(uri_rdfs_range,uri_rdfs_domain,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_domain_range])).
% 3.66/3.83  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.66/3.83  cnf(c56,plain,iext(uri_rdfs_domain,uri_rdf_subject,uri_rdfs_Statement),inference(split_conjunct,[status(thm)],[rdfs_reification_subject_domain])).
% 3.66/3.83  cnf(c248,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X163)|icext(X163,uri_rdfs_Statement),inference(resolution,[status(thm)],[c64, c56])).
% 3.66/3.83  cnf(c1023,plain,icext(uri_rdfs_Class,uri_rdfs_Statement),inference(resolution,[status(thm)],[c248, c85])).
% 3.66/3.83  cnf(c1025,plain,ic(uri_rdfs_Statement),inference(resolution,[status(thm)],[c1023, c84])).
% 3.66/3.83  cnf(c1027,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Statement,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1025, c122])).
% 3.66/3.83  cnf(c1193,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X658)|iext(X658,uri_rdfs_Statement,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1027, c38])).
% 3.66/3.83  cnf(c1190,plain,~iext(uri_rdfs_subClassOf,X657,uri_rdfs_Statement)|iext(uri_rdfs_subClassOf,X657,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1027, c42])).
% 3.66/3.83  cnf(c1026,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Statement,uri_rdfs_Statement),inference(resolution,[status(thm)],[c1025, c45])).
% 3.66/3.83  cnf(c1185,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X656)|iext(X656,uri_rdfs_Statement,uri_rdfs_Statement),inference(resolution,[status(thm)],[c1026, c38])).
% 3.66/3.83  cnf(c1024,plain,iext(uri_rdf_type,uri_rdfs_Statement,uri_rdfs_Class),inference(resolution,[status(thm)],[c1023, c128])).
% 3.66/3.83  cnf(c1177,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X654)|iext(X654,uri_rdfs_Statement,uri_rdfs_Class),inference(resolution,[status(thm)],[c1024, c38])).
% 3.66/3.83  cnf(c37,plain,~iext(uri_rdfs_subPropertyOf,X62,X61)|ip(X61),inference(split_conjunct,[status(thm)],[c35])).
% 3.66/3.83  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.66/3.83  fof(c111,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.66/3.83  fof(c112,plain,(![X37]:(~icext(uri_rdfs_ContainerMembershipProperty,X37)|iext(uri_rdfs_subPropertyOf,X37,uri_rdfs_member))),inference(variable_rename,[status(thm)],[c111])).
% 3.66/3.83  cnf(c113,plain,~icext(uri_rdfs_ContainerMembershipProperty,X91)|iext(uri_rdfs_subPropertyOf,X91,uri_rdfs_member),inference(split_conjunct,[status(thm)],[c112])).
% 3.66/3.83  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.66/3.83  cnf(c100,plain,iext(uri_rdf_type,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),inference(split_conjunct,[status(thm)],[rdfs_container_n_type_002])).
% 3.66/3.83  cnf(c127,plain,~iext(uri_rdf_type,X93,X94)|icext(X94,X93),inference(split_conjunct,[status(thm)],[c126])).
% 3.66/3.83  cnf(c419,plain,icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__2),inference(resolution,[status(thm)],[c127, c100])).
% 3.66/3.83  cnf(c425,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__2,uri_rdfs_member),inference(resolution,[status(thm)],[c419, c113])).
% 3.66/3.83  cnf(c813,plain,ip(uri_rdfs_member),inference(resolution,[status(thm)],[c425, c37])).
% 3.66/3.83  cnf(c819,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_member,uri_rdfs_member),inference(resolution,[status(thm)],[c813, c30])).
% 3.66/3.83  cnf(c1173,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X653)|iext(X653,uri_rdfs_member,uri_rdfs_member),inference(resolution,[status(thm)],[c819, c38])).
% 3.66/3.83  cnf(c145,plain,~ip(X100)|iext(uri_rdf_type,X100,uri_rdf_Property),inference(split_conjunct,[status(thm)],[c143])).
% 3.66/3.83  cnf(c818,plain,iext(uri_rdf_type,uri_rdfs_member,uri_rdf_Property),inference(resolution,[status(thm)],[c813, c145])).
% 3.66/3.83  cnf(c1162,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X651)|iext(X651,uri_rdfs_member,uri_rdf_Property),inference(resolution,[status(thm)],[c818, c38])).
% 3.66/3.83  cnf(c83,plain,~ic(X65)|icext(uri_rdfs_Class,X65),inference(split_conjunct,[status(thm)],[c82])).
% 3.66/3.83  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.66/3.83  fof(c47,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.66/3.83  fof(c49,plain,(![X19]:(![X20]:(![X21]:(~iext(uri_rdfs_subClassOf,X19,X20)|((ic(X19)&ic(X20))&(~icext(X19,X21)|icext(X20,X21))))))),inference(shift_quantors,[status(thm)],[fof(c48,plain,(![X19]:(![X20]:(~iext(uri_rdfs_subClassOf,X19,X20)|((ic(X19)&ic(X20))&(![X21]:(~icext(X19,X21)|icext(X20,X21))))))),inference(variable_rename,[status(thm)],[c47])).])).
% 3.66/3.83  fof(c50,plain,(![X19]:(![X20]:(![X21]:(((~iext(uri_rdfs_subClassOf,X19,X20)|ic(X19))&(~iext(uri_rdfs_subClassOf,X19,X20)|ic(X20)))&(~iext(uri_rdfs_subClassOf,X19,X20)|(~icext(X19,X21)|icext(X20,X21))))))),inference(distribute,[status(thm)],[c49])).
% 3.66/3.83  cnf(c52,plain,~iext(uri_rdfs_subClassOf,X77,X78)|ic(X78),inference(split_conjunct,[status(thm)],[c50])).
% 3.66/3.83  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.66/3.83  cnf(c98,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Container),inference(split_conjunct,[status(thm)],[rdfs_container_seq_sub])).
% 3.66/3.83  cnf(c231,plain,ic(uri_rdfs_Container),inference(resolution,[status(thm)],[c52, c98])).
% 3.66/3.83  cnf(c393,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Container,uri_rdfs_Resource),inference(resolution,[status(thm)],[c122, c231])).
% 3.66/3.83  cnf(c712,plain,ic(uri_rdfs_Resource),inference(resolution,[status(thm)],[c393, c52])).
% 3.66/3.83  cnf(c722,plain,icext(uri_rdfs_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c712, c83])).
% 3.66/3.83  cnf(c723,plain,iext(uri_rdf_type,uri_rdfs_Resource,uri_rdfs_Class),inference(resolution,[status(thm)],[c722, c128])).
% 3.66/3.83  cnf(c1157,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X650)|iext(X650,uri_rdfs_Resource,uri_rdfs_Class),inference(resolution,[status(thm)],[c723, c38])).
% 3.66/3.83  cnf(c720,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Resource,uri_rdfs_Resource),inference(resolution,[status(thm)],[c712, c45])).
% 3.66/3.83  cnf(c1152,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X649)|iext(X649,uri_rdfs_Resource,uri_rdfs_Resource),inference(resolution,[status(thm)],[c720, c38])).
% 3.66/3.83  cnf(c14,plain,iext(uri_ex_hasFather,uri_ex_alice,uri_ex_dave),inference(split_conjunct,[status(thm)],[c2])).
% 3.66/3.83  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.66/3.83  fof(c160,plain,(![S]:(![P]:(![O]:(~iext(P,S,O)|ip(P))))),inference(fof_nnf,[status(thm)],[simple_iext_property])).
% 3.66/3.83  fof(c161,plain,(![S]:(![P]:((![O]:~iext(P,S,O))|ip(P)))),inference(shift_quantors,[status(thm)],[c160])).
% 3.66/3.83  fof(c163,plain,(![X47]:(![X48]:(![X49]:(~iext(X48,X47,X49)|ip(X48))))),inference(shift_quantors,[status(thm)],[fof(c162,plain,(![X47]:(![X48]:((![X49]:~iext(X48,X47,X49))|ip(X48)))),inference(variable_rename,[status(thm)],[c161])).])).
% 3.66/3.83  cnf(c164,plain,~iext(X101,X102,X103)|ip(X101),inference(split_conjunct,[status(thm)],[c163])).
% 3.66/3.83  cnf(c609,plain,ip(uri_ex_hasFather),inference(resolution,[status(thm)],[c164, c14])).
% 3.66/3.83  cnf(c631,plain,iext(uri_rdfs_subPropertyOf,uri_ex_hasFather,uri_ex_hasFather),inference(resolution,[status(thm)],[c609, c30])).
% 3.66/3.83  cnf(c1144,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X647)|iext(X647,uri_ex_hasFather,uri_ex_hasFather),inference(resolution,[status(thm)],[c631, c38])).
% 3.66/3.83  cnf(c630,plain,iext(uri_rdf_type,uri_ex_hasFather,uri_rdf_Property),inference(resolution,[status(thm)],[c609, c145])).
% 3.66/3.83  cnf(c1132,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X645)|iext(X645,uri_ex_hasFather,uri_rdf_Property),inference(resolution,[status(thm)],[c630, c38])).
% 3.66/3.83  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.66/3.83  cnf(c133,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_sub])).
% 3.66/3.83  cnf(c562,plain,ip(uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c164, c133])).
% 3.66/3.83  cnf(c629,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c562, c30])).
% 3.66/3.83  cnf(c1128,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X644)|iext(X644,uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c629, c38])).
% 3.66/3.83  cnf(c628,plain,iext(uri_rdf_type,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c562, c145])).
% 3.66/3.83  cnf(c1117,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X642)|iext(X642,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c628, c38])).
% 3.66/3.83  cnf(c17,plain,iext(uri_ex_hasUncle,uri_ex_bob,uri_ex_dave),inference(split_conjunct,[status(thm)],[c2])).
% 3.66/3.83  cnf(c560,plain,ip(uri_ex_hasUncle),inference(resolution,[status(thm)],[c164, c17])).
% 3.66/3.83  cnf(c627,plain,iext(uri_rdfs_subPropertyOf,uri_ex_hasUncle,uri_ex_hasUncle),inference(resolution,[status(thm)],[c560, c30])).
% 3.66/3.83  cnf(c1112,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X641)|iext(X641,uri_ex_hasUncle,uri_ex_hasUncle),inference(resolution,[status(thm)],[c627, c38])).
% 3.66/3.83  cnf(c626,plain,iext(uri_rdf_type,uri_ex_hasUncle,uri_rdf_Property),inference(resolution,[status(thm)],[c560, c145])).
% 3.66/3.83  cnf(c1100,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X639)|iext(X639,uri_ex_hasUncle,uri_rdf_Property),inference(resolution,[status(thm)],[c626, c38])).
% 3.66/3.83  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.66/3.83  cnf(c114,plain,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Container),inference(split_conjunct,[status(thm)],[rdfs_container_bag_sub])).
% 3.66/3.83  cnf(c559,plain,ip(uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c164, c114])).
% 3.66/3.83  cnf(c625,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c559, c30])).
% 3.66/3.83  cnf(c1095,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X638)|iext(X638,uri_rdfs_subClassOf,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c625, c38])).
% 3.66/3.83  cnf(c624,plain,iext(uri_rdf_type,uri_rdfs_subClassOf,uri_rdf_Property),inference(resolution,[status(thm)],[c559, c145])).
% 3.66/3.83  cnf(c1082,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X636)|iext(X636,uri_rdfs_subClassOf,uri_rdf_Property),inference(resolution,[status(thm)],[c624, c38])).
% 3.66/3.83  cnf(c3,plain,iext(uri_owl_propertyChainAxiom,uri_ex_hasUncle,skolem0001),inference(split_conjunct,[status(thm)],[c2])).
% 3.66/3.83  cnf(c547,plain,ip(uri_owl_propertyChainAxiom),inference(resolution,[status(thm)],[c164, c3])).
% 3.66/3.83  cnf(c623,plain,iext(uri_rdfs_subPropertyOf,uri_owl_propertyChainAxiom,uri_owl_propertyChainAxiom),inference(resolution,[status(thm)],[c547, c30])).
% 3.66/3.83  cnf(c1077,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X635)|iext(X635,uri_owl_propertyChainAxiom,uri_owl_propertyChainAxiom),inference(resolution,[status(thm)],[c623, c38])).
% 3.66/3.83  cnf(c622,plain,iext(uri_rdf_type,uri_owl_propertyChainAxiom,uri_rdf_Property),inference(resolution,[status(thm)],[c547, c145])).
% 3.66/3.83  cnf(c1065,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X633)|iext(X633,uri_owl_propertyChainAxiom,uri_rdf_Property),inference(resolution,[status(thm)],[c622, c38])).
% 3.66/3.84  cnf(c15,plain,iext(uri_ex_hasCousin,uri_ex_alice,uri_ex_bob),inference(split_conjunct,[status(thm)],[c2])).
% 3.66/3.84  cnf(c544,plain,ip(uri_ex_hasCousin),inference(resolution,[status(thm)],[c164, c15])).
% 3.66/3.84  cnf(c621,plain,iext(uri_rdfs_subPropertyOf,uri_ex_hasCousin,uri_ex_hasCousin),inference(resolution,[status(thm)],[c544, c30])).
% 3.66/3.84  cnf(c1061,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X632)|iext(X632,uri_ex_hasCousin,uri_ex_hasCousin),inference(resolution,[status(thm)],[c621, c38])).
% 3.66/3.84  cnf(c620,plain,iext(uri_rdf_type,uri_ex_hasCousin,uri_rdf_Property),inference(resolution,[status(thm)],[c544, c145])).
% 3.66/3.84  cnf(c1050,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X630)|iext(X630,uri_ex_hasCousin,uri_rdf_Property),inference(resolution,[status(thm)],[c620, c38])).
% 3.66/3.84  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.66/3.84  cnf(c129,plain,iext(uri_rdfs_range,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_seealso_range])).
% 3.66/3.84  cnf(c543,plain,ip(uri_rdfs_range),inference(resolution,[status(thm)],[c164, c129])).
% 3.66/3.84  cnf(c619,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_range,uri_rdfs_range),inference(resolution,[status(thm)],[c543, c30])).
% 3.66/3.84  cnf(c1043,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X629)|iext(X629,uri_rdfs_range,uri_rdfs_range),inference(resolution,[status(thm)],[c619, c38])).
% 3.66/3.84  cnf(c618,plain,iext(uri_rdf_type,uri_rdfs_range,uri_rdf_Property),inference(resolution,[status(thm)],[c543, c145])).
% 3.66/3.84  cnf(c1018,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X627)|iext(X627,uri_rdfs_range,uri_rdf_Property),inference(resolution,[status(thm)],[c618, c38])).
% 3.66/3.84  cnf(c13,plain,iext(uri_owl_inverseOf,skolem0005,uri_ex_hasFather),inference(split_conjunct,[status(thm)],[c2])).
% 3.66/3.84  cnf(c541,plain,ip(uri_owl_inverseOf),inference(resolution,[status(thm)],[c164, c13])).
% 3.66/3.84  cnf(c617,plain,iext(uri_rdfs_subPropertyOf,uri_owl_inverseOf,uri_owl_inverseOf),inference(resolution,[status(thm)],[c541, c30])).
% 3.66/3.84  cnf(c1014,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X626)|iext(X626,uri_owl_inverseOf,uri_owl_inverseOf),inference(resolution,[status(thm)],[c617, c38])).
% 3.66/3.84  cnf(c616,plain,iext(uri_rdf_type,uri_owl_inverseOf,uri_rdf_Property),inference(resolution,[status(thm)],[c541, c145])).
% 3.66/3.84  cnf(c1002,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X624)|iext(X624,uri_owl_inverseOf,uri_rdf_Property),inference(resolution,[status(thm)],[c616, c38])).
% 3.66/3.84  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.66/3.84  cnf(c54,plain,iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_subclassof_domain])).
% 3.66/3.84  cnf(c539,plain,ip(uri_rdfs_domain),inference(resolution,[status(thm)],[c164, c54])).
% 3.66/3.84  cnf(c615,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,uri_rdfs_domain),inference(resolution,[status(thm)],[c539, c30])).
% 3.66/3.84  cnf(c996,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X623)|iext(X623,uri_rdfs_domain,uri_rdfs_domain),inference(resolution,[status(thm)],[c615, c38])).
% 3.66/3.84  cnf(c614,plain,iext(uri_rdf_type,uri_rdfs_domain,uri_rdf_Property),inference(resolution,[status(thm)],[c539, c145])).
% 3.66/3.84  cnf(c975,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X621)|iext(X621,uri_rdfs_domain,uri_rdf_Property),inference(resolution,[status(thm)],[c614, c38])).
% 3.66/3.84  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.66/3.84  cnf(c154,plain,iext(uri_rdf_type,uri_rdf_first,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_collection_first_type])).
% 3.66/3.84  cnf(c531,plain,ip(uri_rdf_first),inference(resolution,[status(thm)],[c154, c144])).
% 3.66/3.84  cnf(c536,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_first,uri_rdf_first),inference(resolution,[status(thm)],[c531, c30])).
% 3.66/3.84  cnf(c969,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X620)|iext(X620,uri_rdf_first,uri_rdf_first),inference(resolution,[status(thm)],[c536, c38])).
% 3.66/3.84  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.66/3.84  cnf(c152,plain,iext(uri_rdf_type,uri_rdf_rest,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_collection_rest_type])).
% 3.66/3.84  cnf(c516,plain,ip(uri_rdf_rest),inference(resolution,[status(thm)],[c152, c144])).
% 3.66/3.84  cnf(c523,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_rest,uri_rdf_rest),inference(resolution,[status(thm)],[c516, c30])).
% 3.66/3.84  cnf(c958,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X618)|iext(X618,uri_rdf_rest,uri_rdf_rest),inference(resolution,[status(thm)],[c523, c38])).
% 3.66/3.84  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.66/3.84  cnf(c151,plain,iext(uri_rdf_type,uri_rdf__1,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_container_n_type_001])).
% 3.66/3.84  cnf(c511,plain,ip(uri_rdf__1),inference(resolution,[status(thm)],[c151, c144])).
% 3.66/3.84  cnf(c521,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__1,uri_rdf__1),inference(resolution,[status(thm)],[c511, c30])).
% 3.66/3.84  cnf(c948,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X616)|iext(X616,uri_rdf__1,uri_rdf__1),inference(resolution,[status(thm)],[c521, c38])).
% 3.66/3.84  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.66/3.84  cnf(c150,plain,iext(uri_rdf_type,uri_rdf__2,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_container_n_type_002])).
% 3.66/3.84  cnf(c500,plain,ip(uri_rdf__2),inference(resolution,[status(thm)],[c150, c144])).
% 3.66/3.84  cnf(c507,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__2,uri_rdf__2),inference(resolution,[status(thm)],[c500, c30])).
% 3.66/3.84  cnf(c941,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X614)|iext(X614,uri_rdf__2,uri_rdf__2),inference(resolution,[status(thm)],[c507, c38])).
% 3.66/3.84  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.66/3.84  cnf(c149,plain,iext(uri_rdf_type,uri_rdf__3,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_container_n_type_003])).
% 3.66/3.84  cnf(c495,plain,ip(uri_rdf__3),inference(resolution,[status(thm)],[c149, c144])).
% 3.66/3.84  cnf(c505,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__3,uri_rdf__3),inference(resolution,[status(thm)],[c495, c30])).
% 3.66/3.84  cnf(c934,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X612)|iext(X612,uri_rdf__3,uri_rdf__3),inference(resolution,[status(thm)],[c505, c38])).
% 3.66/3.84  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.66/3.84  cnf(c148,plain,iext(uri_rdf_type,uri_rdf_object,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_reification_object_type])).
% 3.66/3.84  cnf(c487,plain,ip(uri_rdf_object),inference(resolution,[status(thm)],[c148, c144])).
% 3.66/3.84  cnf(c492,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_object,uri_rdf_object),inference(resolution,[status(thm)],[c487, c30])).
% 3.66/3.84  cnf(c927,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X610)|iext(X610,uri_rdf_object,uri_rdf_object),inference(resolution,[status(thm)],[c492, c38])).
% 3.66/3.84  cnf(c413,plain,ip(uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c133, c37])).
% 3.66/3.84  cnf(c484,plain,iext(uri_rdf_type,uri_rdfs_seeAlso,uri_rdf_Property),inference(resolution,[status(thm)],[c145, c413])).
% 3.66/3.84  cnf(c917,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X608)|iext(X608,uri_rdfs_seeAlso,uri_rdf_Property),inference(resolution,[status(thm)],[c484, c38])).
% 3.66/3.84  cnf(c36,plain,~iext(uri_rdfs_subPropertyOf,X57,X56)|ip(X57),inference(split_conjunct,[status(thm)],[c35])).
% 3.66/3.84  cnf(c414,plain,ip(uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c133, c36])).
% 3.66/3.84  cnf(c482,plain,iext(uri_rdf_type,uri_rdfs_isDefinedBy,uri_rdf_Property),inference(resolution,[status(thm)],[c145, c414])).
% 3.66/3.84  cnf(c910,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X607)|iext(X607,uri_rdfs_isDefinedBy,uri_rdf_Property),inference(resolution,[status(thm)],[c482, c38])).
% 3.66/3.84  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.66/3.84  cnf(c147,plain,iext(uri_rdf_type,uri_rdf_value,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_reification_predicate_type])).
% 3.66/3.84  cnf(c475,plain,ip(uri_rdf_value),inference(resolution,[status(thm)],[c147, c144])).
% 3.66/3.84  cnf(c479,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_value,uri_rdf_value),inference(resolution,[status(thm)],[c475, c30])).
% 3.66/3.84  cnf(c904,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X606)|iext(X606,uri_rdf_value,uri_rdf_value),inference(resolution,[status(thm)],[c479, c38])).
% 3.66/3.84  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.66/3.84  cnf(c146,plain,iext(uri_rdf_type,uri_rdf_subject,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_reification_subject_type])).
% 3.66/3.84  cnf(c470,plain,ip(uri_rdf_subject),inference(resolution,[status(thm)],[c144, c146])).
% 3.66/3.84  cnf(c472,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_subject,uri_rdf_subject),inference(resolution,[status(thm)],[c470, c30])).
% 3.66/3.84  cnf(c896,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X604)|iext(X604,uri_rdf_subject,uri_rdf_subject),inference(resolution,[status(thm)],[c472, c38])).
% 3.66/3.84  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.66/3.84  cnf(c138,plain,iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_value_type])).
% 3.66/3.84  cnf(c469,plain,ip(uri_rdf_type),inference(resolution,[status(thm)],[c144, c138])).
% 3.66/3.84  cnf(c471,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_type,uri_rdf_type),inference(resolution,[status(thm)],[c469, c30])).
% 3.66/3.84  cnf(c889,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X602)|iext(X602,uri_rdf_type,uri_rdf_type),inference(resolution,[status(thm)],[c471, c38])).
% 3.66/3.84  cnf(c237,plain,icext(uri_rdfs_Class,uri_rdfs_Container),inference(resolution,[status(thm)],[c231, c83])).
% 3.66/3.84  cnf(c443,plain,iext(uri_rdf_type,uri_rdfs_Container,uri_rdfs_Class),inference(resolution,[status(thm)],[c128, c237])).
% 3.66/3.84  cnf(c878,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X600)|iext(X600,uri_rdfs_Container,uri_rdfs_Class),inference(resolution,[status(thm)],[c443, c38])).
% 3.66/3.84  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.66/3.84  cnf(c97,plain,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[rdfs_dat_xmlliteral_sub])).
% 3.66/3.84  cnf(c230,plain,ic(uri_rdfs_Literal),inference(resolution,[status(thm)],[c52, c97])).
% 3.66/3.84  cnf(c235,plain,icext(uri_rdfs_Class,uri_rdfs_Literal),inference(resolution,[status(thm)],[c230, c83])).
% 3.66/3.84  cnf(c442,plain,iext(uri_rdf_type,uri_rdfs_Literal,uri_rdfs_Class),inference(resolution,[status(thm)],[c128, c235])).
% 3.66/3.84  cnf(c872,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X599)|iext(X599,uri_rdfs_Literal,uri_rdfs_Class),inference(resolution,[status(thm)],[c442, c38])).
% 3.66/3.84  cnf(c51,plain,~iext(uri_rdfs_subClassOf,X75,X76)|ic(X75),inference(split_conjunct,[status(thm)],[c50])).
% 3.66/3.84  cnf(c360,plain,ic(uri_rdf_Bag),inference(resolution,[status(thm)],[c114, c51])).
% 3.66/3.84  cnf(c366,plain,icext(uri_rdfs_Class,uri_rdf_Bag),inference(resolution,[status(thm)],[c360, c83])).
% 3.66/3.84  cnf(c441,plain,iext(uri_rdf_type,uri_rdf_Bag,uri_rdfs_Class),inference(resolution,[status(thm)],[c128, c366])).
% 3.66/3.84  cnf(c867,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X598)|iext(X598,uri_rdf_Bag,uri_rdfs_Class),inference(resolution,[status(thm)],[c441, c38])).
% 3.66/3.84  cnf(c221,plain,ic(uri_rdfs_Seq),inference(resolution,[status(thm)],[c51, c98])).
% 3.66/3.84  cnf(c227,plain,icext(uri_rdfs_Class,uri_rdfs_Seq),inference(resolution,[status(thm)],[c221, c83])).
% 3.66/3.84  cnf(c440,plain,iext(uri_rdf_type,uri_rdfs_Seq,uri_rdfs_Class),inference(resolution,[status(thm)],[c128, c227])).
% 3.66/3.84  cnf(c861,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X597)|iext(X597,uri_rdfs_Seq,uri_rdfs_Class),inference(resolution,[status(thm)],[c440, c38])).
% 3.66/3.84  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.66/3.84  cnf(c92,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_datatype_sub])).
% 3.66/3.84  cnf(c229,plain,ic(uri_rdfs_Class),inference(resolution,[status(thm)],[c52, c92])).
% 3.66/3.84  cnf(c233,plain,icext(uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c229, c83])).
% 3.66/3.84  cnf(c439,plain,iext(uri_rdf_type,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c128, c233])).
% 3.66/3.84  cnf(c856,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X596)|iext(X596,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c439, c38])).
% 3.66/3.84  cnf(c220,plain,ic(uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c51, c97])).
% 3.66/3.84  cnf(c225,plain,icext(uri_rdfs_Class,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c220, c83])).
% 3.66/3.84  cnf(c438,plain,iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Class),inference(resolution,[status(thm)],[c128, c225])).
% 3.66/3.84  cnf(c851,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X595)|iext(X595,uri_rdf_XMLLiteral,uri_rdfs_Class),inference(resolution,[status(thm)],[c438, c38])).
% 3.66/3.84  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.66/3.84  cnf(c110,plain,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_container_containermembershipproperty_sub])).
% 3.66/3.84  cnf(c298,plain,ic(uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c110, c51])).
% 3.66/3.84  cnf(c353,plain,icext(uri_rdfs_Class,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c298, c83])).
% 3.66/3.84  cnf(c436,plain,iext(uri_rdf_type,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Class),inference(resolution,[status(thm)],[c128, c353])).
% 3.66/3.84  cnf(c846,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X594)|iext(X594,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Class),inference(resolution,[status(thm)],[c436, c38])).
% 3.66/3.84  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.66/3.84  cnf(c115,plain,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Container),inference(split_conjunct,[status(thm)],[rdfs_container_alt_sub])).
% 3.66/3.84  cnf(c370,plain,ic(uri_rdf_Alt),inference(resolution,[status(thm)],[c115, c51])).
% 3.66/3.84  cnf(c376,plain,icext(uri_rdfs_Class,uri_rdf_Alt),inference(resolution,[status(thm)],[c370, c83])).
% 3.66/3.84  cnf(c434,plain,iext(uri_rdf_type,uri_rdf_Alt,uri_rdfs_Class),inference(resolution,[status(thm)],[c128, c376])).
% 3.66/3.84  cnf(c841,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X593)|iext(X593,uri_rdf_Alt,uri_rdfs_Class),inference(resolution,[status(thm)],[c434, c38])).
% 3.66/3.84  cnf(c1384,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X592)|icext(X592,uri_rdfs_comment),inference(resolution,[status(thm)],[c1378, c90])).
% 3.66/3.84  cnf(c219,plain,ic(uri_rdfs_Datatype),inference(resolution,[status(thm)],[c51, c92])).
% 3.66/3.84  cnf(c223,plain,icext(uri_rdfs_Class,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c219, c83])).
% 3.66/3.84  cnf(c432,plain,iext(uri_rdf_type,uri_rdfs_Datatype,uri_rdfs_Class),inference(resolution,[status(thm)],[c128, c223])).
% 3.66/3.84  cnf(c836,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X591)|iext(X591,uri_rdfs_Datatype,uri_rdfs_Class),inference(resolution,[status(thm)],[c432, c38])).
% 3.66/3.84  cnf(c1381,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X590)|icext(X590,uri_rdfs_comment),inference(resolution,[status(thm)],[c1378, c64])).
% 3.66/3.84  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.66/3.84  cnf(c99,plain,iext(uri_rdf_type,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),inference(split_conjunct,[status(thm)],[rdfs_container_n_type_003])).
% 3.66/3.84  cnf(c421,plain,icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__3),inference(resolution,[status(thm)],[c127, c99])).
% 3.66/3.84  cnf(c427,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__3,uri_rdfs_member),inference(resolution,[status(thm)],[c421, c113])).
% 3.66/3.84  cnf(c832,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X587)|iext(X587,uri_rdf__3,uri_rdfs_member),inference(resolution,[status(thm)],[c427, c38])).
% 3.66/3.84  cnf(c1355,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X586)|icext(X586,uri_rdfs_label),inference(resolution,[status(thm)],[c1349, c90])).
% 3.66/3.84  cnf(c1352,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X585)|icext(X585,uri_rdfs_label),inference(resolution,[status(thm)],[c1349, c64])).
% 3.66/3.84  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.66/3.84  fof(c25,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.66/3.84  fof(c26,plain,(![X7]:(![X8]:(![X9]:((~iext(uri_rdfs_subPropertyOf,X7,X8)|~iext(uri_rdfs_subPropertyOf,X8,X9))|iext(uri_rdfs_subPropertyOf,X7,X9))))),inference(variable_rename,[status(thm)],[c25])).
% 3.66/3.84  cnf(c27,plain,~iext(uri_rdfs_subPropertyOf,X54,X52)|~iext(uri_rdfs_subPropertyOf,X52,X53)|iext(uri_rdfs_subPropertyOf,X54,X53),inference(split_conjunct,[status(thm)],[c26])).
% 3.66/3.84  cnf(c831,plain,~iext(uri_rdfs_subPropertyOf,X584,uri_rdf__3)|iext(uri_rdfs_subPropertyOf,X584,uri_rdfs_member),inference(resolution,[status(thm)],[c427, c27])).
% 3.66/3.84  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.66/3.84  cnf(c101,plain,iext(uri_rdf_type,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),inference(split_conjunct,[status(thm)],[rdfs_container_n_type_001])).
% 3.66/3.84  cnf(c420,plain,icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__1),inference(resolution,[status(thm)],[c127, c101])).
% 3.66/3.84  cnf(c426,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__1,uri_rdfs_member),inference(resolution,[status(thm)],[c420, c113])).
% 3.66/3.84  cnf(c825,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X579)|iext(X579,uri_rdf__1,uri_rdfs_member),inference(resolution,[status(thm)],[c426, c38])).
% 3.66/3.84  cnf(c1315,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X578)|icext(X578,uri_rdf_List),inference(resolution,[status(thm)],[c1301, c90])).
% 3.66/3.84  cnf(c1310,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X577)|icext(X577,uri_rdf_List),inference(resolution,[status(thm)],[c1301, c64])).
% 3.66/3.84  cnf(c824,plain,~iext(uri_rdfs_subPropertyOf,X576,uri_rdf__1)|iext(uri_rdfs_subPropertyOf,X576,uri_rdfs_member),inference(resolution,[status(thm)],[c426, c27])).
% 3.66/3.84  cnf(c816,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X571)|iext(X571,uri_rdf__2,uri_rdfs_member),inference(resolution,[status(thm)],[c425, c38])).
% 3.66/3.84  cnf(c1260,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X568)|icext(X568,uri_rdf_predicate),inference(resolution,[status(thm)],[c1254, c90])).
% 3.66/3.84  cnf(c815,plain,~iext(uri_rdfs_subPropertyOf,X567,uri_rdf__2)|iext(uri_rdfs_subPropertyOf,X567,uri_rdfs_member),inference(resolution,[status(thm)],[c425, c27])).
% 3.66/3.84  cnf(c1257,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X566)|icext(X566,uri_rdf_predicate),inference(resolution,[status(thm)],[c1254, c64])).
% 3.66/3.84  cnf(c424,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c414, c30])).
% 3.66/3.84  cnf(c809,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X563)|iext(X563,uri_rdfs_isDefinedBy,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c424, c38])).
% 3.66/3.84  cnf(c1184,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X555)|icext(X555,uri_rdfs_Statement),inference(resolution,[status(thm)],[c1026, c90])).
% 3.66/3.84  cnf(c418,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_seeAlso,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c413, c30])).
% 3.66/3.84  cnf(c802,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X554)|iext(X554,uri_rdfs_seeAlso,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c418, c38])).
% 3.66/3.84  cnf(c1183,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X553)|icext(X553,uri_rdfs_Statement),inference(resolution,[status(thm)],[c1026, c64])).
% 3.66/3.84  cnf(c1171,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X550)|icext(X550,uri_rdfs_member),inference(resolution,[status(thm)],[c819, c90])).
% 3.66/3.84  cnf(c402,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c122, c229])).
% 3.66/3.84  cnf(c794,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X544)|iext(X544,uri_rdfs_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c402, c38])).
% 3.66/3.84  cnf(c1151,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X542)|icext(X542,uri_rdfs_Resource),inference(resolution,[status(thm)],[c720, c90])).
% 3.66/3.84  cnf(c791,plain,~iext(uri_rdfs_subClassOf,X541,uri_rdfs_Class)|iext(uri_rdfs_subClassOf,X541,uri_rdfs_Resource),inference(resolution,[status(thm)],[c402, c42])).
% 3.66/3.84  cnf(c1142,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X539)|icext(X539,uri_ex_hasFather),inference(resolution,[status(thm)],[c631, c90])).
% 3.66/3.84  cnf(c401,plain,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Resource),inference(resolution,[status(thm)],[c122, c298])).
% 3.66/3.84  cnf(c786,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X538)|iext(X538,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Resource),inference(resolution,[status(thm)],[c401, c38])).
% 3.66/3.84  cnf(c1139,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X537)|icext(X537,uri_ex_hasFather),inference(resolution,[status(thm)],[c631, c64])).
% 3.66/3.84  cnf(c783,plain,~iext(uri_rdfs_subClassOf,X534,uri_rdfs_ContainerMembershipProperty)|iext(uri_rdfs_subClassOf,X534,uri_rdfs_Resource),inference(resolution,[status(thm)],[c401, c42])).
% 3.66/3.84  cnf(c1126,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X533)|icext(X533,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c629, c90])).
% 3.66/3.84  cnf(c1124,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X532)|icext(X532,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c629, c64])).
% 3.66/3.84  cnf(c400,plain,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Resource),inference(resolution,[status(thm)],[c122, c220])).
% 3.66/3.84  cnf(c778,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X530)|iext(X530,uri_rdf_XMLLiteral,uri_rdfs_Resource),inference(resolution,[status(thm)],[c400, c38])).
% 3.66/3.84  cnf(c1109,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X528)|icext(X528,uri_ex_hasUncle),inference(resolution,[status(thm)],[c627, c90])).
% 3.66/3.84  cnf(c775,plain,~iext(uri_rdfs_subClassOf,X527,uri_rdf_XMLLiteral)|iext(uri_rdfs_subClassOf,X527,uri_rdfs_Resource),inference(resolution,[status(thm)],[c400, c42])).
% 3.66/3.84  cnf(c1107,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X526)|icext(X526,uri_ex_hasUncle),inference(resolution,[status(thm)],[c627, c64])).
% 3.66/3.84  cnf(c301,plain,ic(uri_rdf_Property),inference(resolution,[status(thm)],[c110, c52])).
% 3.66/3.84  cnf(c399,plain,iext(uri_rdfs_subClassOf,uri_rdf_Property,uri_rdfs_Resource),inference(resolution,[status(thm)],[c122, c301])).
% 3.66/3.84  cnf(c770,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X523)|iext(X523,uri_rdf_Property,uri_rdfs_Resource),inference(resolution,[status(thm)],[c399, c38])).
% 3.66/3.84  cnf(c1092,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X522)|icext(X522,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c625, c90])).
% 3.66/3.84  cnf(c1090,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X521)|icext(X521,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c625, c64])).
% 3.66/3.84  cnf(c767,plain,~iext(uri_rdfs_subClassOf,X520,uri_rdf_Property)|iext(uri_rdfs_subClassOf,X520,uri_rdfs_Resource),inference(resolution,[status(thm)],[c399, c42])).
% 3.66/3.84  cnf(c1075,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X517)|icext(X517,uri_owl_propertyChainAxiom),inference(resolution,[status(thm)],[c623, c90])).
% 3.66/3.84  cnf(c398,plain,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Resource),inference(resolution,[status(thm)],[c122, c360])).
% 3.66/3.84  cnf(c762,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X516)|iext(X516,uri_rdf_Bag,uri_rdfs_Resource),inference(resolution,[status(thm)],[c398, c38])).
% 3.66/3.84  cnf(c1073,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X515)|icext(X515,uri_owl_propertyChainAxiom),inference(resolution,[status(thm)],[c623, c64])).
% 3.66/3.84  cnf(c759,plain,~iext(uri_rdfs_subClassOf,X512,uri_rdf_Bag)|iext(uri_rdfs_subClassOf,X512,uri_rdfs_Resource),inference(resolution,[status(thm)],[c398, c42])).
% 3.66/3.84  cnf(c1059,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X511)|icext(X511,uri_ex_hasCousin),inference(resolution,[status(thm)],[c621, c90])).
% 3.66/3.84  cnf(c1057,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X510)|icext(X510,uri_ex_hasCousin),inference(resolution,[status(thm)],[c621, c64])).
% 3.66/3.84  cnf(c397,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Resource),inference(resolution,[status(thm)],[c122, c219])).
% 3.66/3.84  cnf(c754,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X509)|iext(X509,uri_rdfs_Datatype,uri_rdfs_Resource),inference(resolution,[status(thm)],[c397, c38])).
% 3.66/3.84  cnf(c1041,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X506)|icext(X506,uri_rdfs_range),inference(resolution,[status(thm)],[c619, c90])).
% 3.66/3.84  cnf(c751,plain,~iext(uri_rdfs_subClassOf,X505,uri_rdfs_Datatype)|iext(uri_rdfs_subClassOf,X505,uri_rdfs_Resource),inference(resolution,[status(thm)],[c397, c42])).
% 3.66/3.84  cnf(c1035,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X504)|icext(X504,uri_rdfs_range),inference(resolution,[status(thm)],[c619, c64])).
% 3.66/3.84  cnf(c396,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Literal,uri_rdfs_Resource),inference(resolution,[status(thm)],[c122, c230])).
% 3.66/3.84  cnf(c746,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X501)|iext(X501,uri_rdfs_Literal,uri_rdfs_Resource),inference(resolution,[status(thm)],[c396, c38])).
% 3.66/3.84  cnf(c1012,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X500)|icext(X500,uri_owl_inverseOf),inference(resolution,[status(thm)],[c617, c90])).
% 3.66/3.84  cnf(c743,plain,~iext(uri_rdfs_subClassOf,X499,uri_rdfs_Literal)|iext(uri_rdfs_subClassOf,X499,uri_rdfs_Resource),inference(resolution,[status(thm)],[c396, c42])).
% 3.66/3.84  cnf(c1010,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X498)|icext(X498,uri_owl_inverseOf),inference(resolution,[status(thm)],[c617, c64])).
% 3.66/3.84  cnf(c395,plain,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Resource),inference(resolution,[status(thm)],[c122, c370])).
% 3.66/3.84  cnf(c738,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X495)|iext(X495,uri_rdf_Alt,uri_rdfs_Resource),inference(resolution,[status(thm)],[c395, c38])).
% 3.66/3.84  cnf(c992,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X494)|icext(X494,uri_rdfs_domain),inference(resolution,[status(thm)],[c615, c90])).
% 3.66/3.84  cnf(c987,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X493)|icext(X493,uri_rdfs_domain),inference(resolution,[status(thm)],[c615, c64])).
% 3.66/3.84  cnf(c735,plain,~iext(uri_rdfs_subClassOf,X491,uri_rdf_Alt)|iext(uri_rdfs_subClassOf,X491,uri_rdfs_Resource),inference(resolution,[status(thm)],[c395, c42])).
% 3.66/3.84  cnf(c967,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X489)|icext(X489,uri_rdf_first),inference(resolution,[status(thm)],[c536, c90])).
% 3.66/3.84  cnf(c394,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Resource),inference(resolution,[status(thm)],[c122, c221])).
% 3.66/3.84  cnf(c730,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X488)|iext(X488,uri_rdfs_Seq,uri_rdfs_Resource),inference(resolution,[status(thm)],[c394, c38])).
% 3.66/3.84  cnf(c964,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X487)|icext(X487,uri_rdf_first),inference(resolution,[status(thm)],[c536, c64])).
% 3.66/3.84  cnf(c956,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X486)|icext(X486,uri_rdf_rest),inference(resolution,[status(thm)],[c523, c90])).
% 3.66/3.84  cnf(c727,plain,~iext(uri_rdfs_subClassOf,X485,uri_rdfs_Seq)|iext(uri_rdfs_subClassOf,X485,uri_rdfs_Resource),inference(resolution,[status(thm)],[c394, c42])).
% 3.66/3.84  cnf(c953,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X484)|icext(X484,uri_rdf_rest),inference(resolution,[status(thm)],[c523, c64])).
% 3.66/3.84  cnf(c944,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X482)|icext(X482,uri_rdf__1),inference(resolution,[status(thm)],[c521, c64])).
% 3.66/3.84  cnf(c717,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X481)|iext(X481,uri_rdfs_Container,uri_rdfs_Resource),inference(resolution,[status(thm)],[c393, c38])).
% 3.66/3.84  cnf(c714,plain,~iext(uri_rdfs_subClassOf,X479,uri_rdfs_Container)|iext(uri_rdfs_subClassOf,X479,uri_rdfs_Resource),inference(resolution,[status(thm)],[c393, c42])).
% 3.66/3.84  cnf(c937,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X478)|icext(X478,uri_rdf__2),inference(resolution,[status(thm)],[c507, c64])).
% 3.66/3.84  cnf(c375,plain,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdf_Alt),inference(resolution,[status(thm)],[c370, c45])).
% 3.66/3.84  cnf(c709,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X476)|iext(X476,uri_rdf_Alt,uri_rdf_Alt),inference(resolution,[status(thm)],[c375, c38])).
% 3.66/3.84  cnf(c930,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X475)|icext(X475,uri_rdf__3),inference(resolution,[status(thm)],[c505, c64])).
% 3.66/3.84  cnf(c925,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X474)|icext(X474,uri_rdf_object),inference(resolution,[status(thm)],[c492, c90])).
% 3.66/3.84  cnf(c923,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X473)|icext(X473,uri_rdf_object),inference(resolution,[status(thm)],[c492, c64])).
% 3.66/3.84  cnf(c365,plain,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdf_Bag),inference(resolution,[status(thm)],[c360, c45])).
% 3.66/3.84  cnf(c701,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X467)|iext(X467,uri_rdf_Bag,uri_rdf_Bag),inference(resolution,[status(thm)],[c365, c38])).
% 3.66/3.84  cnf(c902,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X466)|icext(X466,uri_rdf_value),inference(resolution,[status(thm)],[c479, c90])).
% 3.66/3.84  cnf(c900,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X465)|icext(X465,uri_rdf_value),inference(resolution,[status(thm)],[c479, c64])).
% 3.66/3.84  cnf(c894,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X463)|icext(X463,uri_rdf_subject),inference(resolution,[status(thm)],[c472, c90])).
% 3.66/3.84  cnf(c892,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X462)|icext(X462,uri_rdf_subject),inference(resolution,[status(thm)],[c472, c64])).
% 3.66/3.84  cnf(c354,plain,iext(uri_rdfs_subClassOf,uri_rdf_Property,uri_rdf_Property),inference(resolution,[status(thm)],[c301, c45])).
% 3.66/3.84  cnf(c693,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X461)|iext(X461,uri_rdf_Property,uri_rdf_Property),inference(resolution,[status(thm)],[c354, c38])).
% 3.66/3.84  cnf(c887,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X460)|icext(X460,uri_rdf_type),inference(resolution,[status(thm)],[c471, c90])).
% 3.66/3.84  cnf(c885,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X459)|icext(X459,uri_rdf_type),inference(resolution,[status(thm)],[c471, c64])).
% 3.66/3.84  cnf(c352,plain,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c298, c45])).
% 3.66/3.84  cnf(c685,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X451)|iext(X451,uri_rdfs_ContainerMembershipProperty,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c352, c38])).
% 3.66/3.84  cnf(c236,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Container,uri_rdfs_Container),inference(resolution,[status(thm)],[c231, c45])).
% 3.66/3.84  cnf(c677,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X440)|iext(X440,uri_rdfs_Container,uri_rdfs_Container),inference(resolution,[status(thm)],[c236, c38])).
% 3.66/3.84  cnf(c830,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X436)|icext(X436,uri_rdf__3),inference(resolution,[status(thm)],[c427, c90])).
% 3.66/3.84  cnf(c823,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X433)|icext(X433,uri_rdf__1),inference(resolution,[status(thm)],[c426, c90])).
% 3.66/3.84  cnf(c234,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Literal,uri_rdfs_Literal),inference(resolution,[status(thm)],[c230, c45])).
% 3.66/3.84  cnf(c669,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X431)|iext(X431,uri_rdfs_Literal,uri_rdfs_Literal),inference(resolution,[status(thm)],[c234, c38])).
% 3.66/3.84  cnf(c814,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X430)|icext(X430,uri_rdf__2),inference(resolution,[status(thm)],[c425, c90])).
% 3.66/3.84  cnf(c812,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X429)|icext(X429,uri_rdfs_member),inference(resolution,[status(thm)],[c425, c64])).
% 3.66/3.84  cnf(c805,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X426)|icext(X426,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c424, c64])).
% 3.66/3.84  cnf(c800,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X425)|icext(X425,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c418, c90])).
% 3.66/3.84  cnf(c232,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c229, c45])).
% 3.66/3.84  cnf(c661,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X424)|iext(X424,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c232, c38])).
% 3.66/3.84  cnf(c226,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Seq),inference(resolution,[status(thm)],[c221, c45])).
% 3.66/3.84  cnf(c653,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X413)|iext(X413,uri_rdfs_Seq,uri_rdfs_Seq),inference(resolution,[status(thm)],[c226, c38])).
% 3.66/3.84  cnf(c224,plain,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c220, c45])).
% 3.66/3.84  cnf(c645,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X402)|iext(X402,uri_rdf_XMLLiteral,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c224, c38])).
% 3.66/3.84  cnf(c715,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X399)|icext(X399,uri_rdfs_Resource),inference(resolution,[status(thm)],[c393, c64])).
% 3.66/3.84  cnf(c707,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X396)|icext(X396,uri_rdf_Alt),inference(resolution,[status(thm)],[c375, c64])).
% 3.66/3.84  cnf(c222,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c219, c45])).
% 3.66/3.84  cnf(c637,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X394)|iext(X394,uri_rdfs_Datatype,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c222, c38])).
% 3.66/3.84  cnf(c699,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X393)|icext(X393,uri_rdf_Bag),inference(resolution,[status(thm)],[c365, c64])).
% 3.66/3.84  cnf(c692,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X392)|icext(X392,uri_rdf_Property),inference(resolution,[status(thm)],[c354, c90])).
% 3.66/3.84  cnf(c683,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X388)|icext(X388,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c352, c64])).
% 3.66/3.84  cnf(c676,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X387)|icext(X387,uri_rdfs_Container),inference(resolution,[status(thm)],[c236, c90])).
% 3.66/3.84  cnf(c530,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X386)|iext(X386,uri_rdf_first,uri_rdf_Property),inference(resolution,[status(thm)],[c154, c38])).
% 3.66/3.84  cnf(c668,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X384)|icext(X384,uri_rdfs_Literal),inference(resolution,[status(thm)],[c234, c90])).
% 3.66/3.84  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.66/3.84  cnf(c153,plain,iext(uri_rdf_type,uri_rdf_nil,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdf_collection_nil_type])).
% 3.66/3.84  cnf(c526,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X382)|iext(X382,uri_rdf_nil,uri_rdf_List),inference(resolution,[status(thm)],[c153, c38])).
% 3.66/3.84  cnf(c660,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X381)|icext(X381,uri_rdfs_Class),inference(resolution,[status(thm)],[c232, c90])).
% 3.66/3.84  cnf(c515,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X378)|iext(X378,uri_rdf_rest,uri_rdf_Property),inference(resolution,[status(thm)],[c152, c38])).
% 3.66/3.84  cnf(c651,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X377)|icext(X377,uri_rdfs_Seq),inference(resolution,[status(thm)],[c226, c64])).
% 3.66/3.84  cnf(c510,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X375)|iext(X375,uri_rdf__1,uri_rdf_Property),inference(resolution,[status(thm)],[c151, c38])).
% 3.66/3.84  cnf(c643,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X374)|icext(X374,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c224, c64])).
% 3.66/3.84  cnf(c635,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X372)|icext(X372,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c222, c64])).
% 3.66/3.84  cnf(c499,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X371)|iext(X371,uri_rdf__2,uri_rdf_Property),inference(resolution,[status(thm)],[c150, c38])).
% 3.66/3.84  cnf(c529,plain,~iext(uri_rdfs_range,uri_rdf_type,X368)|icext(X368,uri_rdf_List),inference(resolution,[status(thm)],[c153, c64])).
% 3.66/3.84  cnf(c494,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X367)|iext(X367,uri_rdf__3,uri_rdf_Property),inference(resolution,[status(thm)],[c149, c38])).
% 3.66/3.84  cnf(c486,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X362)|iext(X362,uri_rdf_object,uri_rdf_Property),inference(resolution,[status(thm)],[c148, c38])).
% 3.66/3.84  cnf(c474,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X357)|iext(X357,uri_rdf_value,uri_rdf_Property),inference(resolution,[status(thm)],[c147, c38])).
% 3.66/3.84  cnf(c465,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X352)|iext(X352,uri_rdf_subject,uri_rdf_Property),inference(resolution,[status(thm)],[c146, c38])).
% 3.66/3.84  cnf(c460,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X348)|iext(X348,uri_rdf_type,uri_rdf_Property),inference(resolution,[status(thm)],[c138, c38])).
% 3.66/3.84  cnf(c463,plain,~iext(uri_rdfs_range,uri_rdf_type,X347)|icext(X347,uri_rdf_Property),inference(resolution,[status(thm)],[c138, c64])).
% 3.66/3.84  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.66/3.84  cnf(c137,plain,iext(uri_rdfs_domain,uri_rdfs_comment,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_comment_domain])).
% 3.66/3.84  cnf(c457,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X344)|iext(X344,uri_rdfs_comment,uri_rdfs_Resource),inference(resolution,[status(thm)],[c137, c38])).
% 3.66/3.84  cnf(c458,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X343)|icext(X343,uri_rdfs_comment),inference(resolution,[status(thm)],[c137, c90])).
% 3.66/3.84  cnf(c454,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X341)|iext(X341,uri_rdfs_comment,uri_rdfs_Literal),inference(resolution,[status(thm)],[c136, c38])).
% 3.66/3.84  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.66/3.84  cnf(c135,plain,iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_domain])).
% 3.66/3.84  cnf(c451,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X340)|iext(X340,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(resolution,[status(thm)],[c135, c38])).
% 3.66/3.84  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.66/3.84  cnf(c134,plain,iext(uri_rdfs_range,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_range])).
% 3.66/3.84  cnf(c448,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X339)|iext(X339,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(resolution,[status(thm)],[c134, c38])).
% 3.66/3.84  cnf(c452,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X336)|icext(X336,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c135, c90])).
% 3.66/3.84  fof(simple_ir,axiom,(![X]:ir(X)),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', simple_ir)).
% 3.66/3.84  fof(c158,plain,(![X46]:ir(X46)),inference(variable_rename,[status(thm)],[simple_ir])).
% 3.66/3.84  cnf(c159,plain,ir(X50),inference(split_conjunct,[status(thm)],[c158])).
% 3.66/3.84  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.66/3.84  fof(c73,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.66/3.84  fof(c74,plain,((![X]:(~ir(X)|icext(uri_rdfs_Resource,X)))&(![X]:(~icext(uri_rdfs_Resource,X)|ir(X)))),inference(shift_quantors,[status(thm)],[c73])).
% 3.66/3.84  fof(c76,plain,(![X28]:(![X29]:((~ir(X28)|icext(uri_rdfs_Resource,X28))&(~icext(uri_rdfs_Resource,X29)|ir(X29))))),inference(shift_quantors,[status(thm)],[fof(c75,plain,((![X28]:(~ir(X28)|icext(uri_rdfs_Resource,X28)))&(![X29]:(~icext(uri_rdfs_Resource,X29)|ir(X29)))),inference(variable_rename,[status(thm)],[c74])).])).
% 3.66/3.84  cnf(c77,plain,~ir(X60)|icext(uri_rdfs_Resource,X60),inference(split_conjunct,[status(thm)],[c76])).
% 3.66/3.84  cnf(c166,plain,icext(uri_rdfs_Resource,X63),inference(resolution,[status(thm)],[c77, c159])).
% 3.66/3.84  cnf(c433,plain,iext(uri_rdf_type,X97,uri_rdfs_Resource),inference(resolution,[status(thm)],[c128, c166])).
% 3.66/3.84  cnf(c444,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X333)|iext(X333,X334,uri_rdfs_Resource),inference(resolution,[status(thm)],[c433, c38])).
% 3.66/3.84  cnf(c449,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X331)|icext(X331,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c134, c90])).
% 3.66/3.84  cnf(c416,plain,~iext(uri_rdfs_subPropertyOf,X330,uri_rdfs_isDefinedBy)|iext(uri_rdfs_subPropertyOf,X330,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c133, c27])).
% 3.66/3.84  cnf(c447,plain,~iext(uri_rdfs_range,uri_rdf_type,X329)|icext(X329,uri_rdfs_Resource),inference(resolution,[status(thm)],[c433, c64])).
% 3.66/3.84  cnf(c417,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X328)|icext(X328,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c133, c64])).
% 3.66/3.84  cnf(c412,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X327)|iext(X327,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c133, c38])).
% 3.66/3.84  cnf(c415,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X326)|icext(X326,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c133, c90])).
% 3.66/3.84  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.66/3.84  cnf(c132,plain,iext(uri_rdfs_domain,uri_rdfs_label,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_label_domain])).
% 3.66/3.84  cnf(c410,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X324)|icext(X324,uri_rdfs_label),inference(resolution,[status(thm)],[c132, c90])).
% 3.66/3.84  cnf(c409,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X323)|iext(X323,uri_rdfs_label,uri_rdfs_Resource),inference(resolution,[status(thm)],[c132, c38])).
% 3.66/3.84  cnf(c408,plain,~iext(uri_rdfs_range,uri_rdfs_range,X322)|icext(X322,uri_rdfs_Literal),inference(resolution,[status(thm)],[c131, c64])).
% 3.66/3.84  cnf(c406,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X321)|iext(X321,uri_rdfs_label,uri_rdfs_Literal),inference(resolution,[status(thm)],[c131, c38])).
% 3.66/3.84  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.66/3.84  cnf(c130,plain,iext(uri_rdfs_domain,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_seealso_domain])).
% 3.66/3.84  cnf(c403,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X318)|iext(X318,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(resolution,[status(thm)],[c130, c38])).
% 3.66/3.84  cnf(c404,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X317)|icext(X317,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c130, c90])).
% 3.66/3.84  cnf(c390,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X315)|iext(X315,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(resolution,[status(thm)],[c129, c38])).
% 3.66/3.84  cnf(c391,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X314)|icext(X314,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c129, c90])).
% 3.66/3.84  cnf(c388,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X312)|icext(X312,uri_rdf_first),inference(resolution,[status(thm)],[c119, c90])).
% 3.66/3.84  cnf(c387,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X311)|iext(X311,uri_rdf_first,uri_rdf_List),inference(resolution,[status(thm)],[c119, c38])).
% 3.66/3.84  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.66/3.84  cnf(c118,plain,iext(uri_rdfs_range,uri_rdf_first,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_collection_first_range])).
% 3.66/3.84  cnf(c385,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X309)|icext(X309,uri_rdf_first),inference(resolution,[status(thm)],[c118, c90])).
% 3.66/3.84  cnf(c384,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X308)|iext(X308,uri_rdf_first,uri_rdfs_Resource),inference(resolution,[status(thm)],[c118, c38])).
% 3.66/3.84  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.66/3.84  cnf(c117,plain,iext(uri_rdfs_domain,uri_rdf_rest,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdfs_collection_rest_domain])).
% 3.66/3.84  cnf(c383,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X307)|icext(X307,uri_rdf_List),inference(resolution,[status(thm)],[c117, c64])).
% 3.66/3.84  cnf(c382,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X306)|icext(X306,uri_rdf_rest),inference(resolution,[status(thm)],[c117, c90])).
% 3.66/3.84  cnf(c381,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X304)|iext(X304,uri_rdf_rest,uri_rdf_List),inference(resolution,[status(thm)],[c117, c38])).
% 3.66/3.84  cnf(c378,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X302)|iext(X302,uri_rdf_rest,uri_rdf_List),inference(resolution,[status(thm)],[c116, c38])).
% 3.66/3.84  cnf(c372,plain,~iext(uri_rdfs_subClassOf,X301,uri_rdf_Alt)|iext(uri_rdfs_subClassOf,X301,uri_rdfs_Container),inference(resolution,[status(thm)],[c115, c42])).
% 3.66/3.84  cnf(c369,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X300)|iext(X300,uri_rdf_Alt,uri_rdfs_Container),inference(resolution,[status(thm)],[c115, c38])).
% 3.66/3.84  cnf(c362,plain,~iext(uri_rdfs_subClassOf,X298,uri_rdf_Bag)|iext(uri_rdfs_subClassOf,X298,uri_rdfs_Container),inference(resolution,[status(thm)],[c114, c42])).
% 3.66/3.84  cnf(c379,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X297)|icext(X297,uri_rdf_rest),inference(resolution,[status(thm)],[c116, c90])).
% 3.66/3.84  cnf(c359,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X295)|iext(X295,uri_rdf_Bag,uri_rdfs_Container),inference(resolution,[status(thm)],[c114, c38])).
% 3.66/3.84  cnf(c371,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X294)|icext(X294,uri_rdf_Alt),inference(resolution,[status(thm)],[c115, c90])).
% 3.66/3.84  cnf(c361,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X292)|icext(X292,uri_rdf_Bag),inference(resolution,[status(thm)],[c114, c90])).
% 3.66/3.84  cnf(c351,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X291)|icext(X291,uri_rdfs_Seq),inference(resolution,[status(thm)],[c90, c98])).
% 3.66/3.84  cnf(c16,plain,iext(uri_ex_hasFather,uri_ex_bob,uri_ex_charly),inference(split_conjunct,[status(thm)],[c2])).
% 3.66/3.84  cnf(c349,plain,~iext(uri_rdfs_domain,uri_ex_hasFather,X289)|icext(X289,uri_ex_bob),inference(resolution,[status(thm)],[c90, c16])).
% 3.66/3.84  cnf(c348,plain,~iext(uri_rdfs_domain,uri_ex_hasFather,X288)|icext(X288,uri_ex_alice),inference(resolution,[status(thm)],[c90, c14])).
% 3.66/3.84  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.66/3.84  cnf(c31,plain,iext(uri_rdfs_range,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_subpropertyof_range])).
% 3.66/3.84  cnf(c347,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X287)|icext(X287,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c90, c31])).
% 3.66/3.84  cnf(c346,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X286)|icext(X286,uri_rdfs_range),inference(resolution,[status(thm)],[c90, c65])).
% 3.66/3.84  cnf(c11,plain,iext(uri_rdf_first,skolem0004,skolem0005),inference(split_conjunct,[status(thm)],[c2])).
% 3.66/3.84  cnf(c345,plain,~iext(uri_rdfs_domain,uri_rdf_first,X285)|icext(X285,skolem0004),inference(resolution,[status(thm)],[c90, c11])).
% 3.66/3.84  cnf(c7,plain,iext(uri_rdf_rest,skolem0002,uri_rdf_nil),inference(split_conjunct,[status(thm)],[c2])).
% 3.66/3.84  cnf(c344,plain,~iext(uri_rdfs_domain,uri_rdf_rest,X284)|icext(X284,skolem0002),inference(resolution,[status(thm)],[c90, c7])).
% 3.66/3.84  cnf(c343,plain,~iext(uri_rdfs_domain,uri_rdf_rest,X283)|icext(X283,skolem0001),inference(resolution,[status(thm)],[c90, c5])).
% 3.66/3.84  cnf(c342,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X282)|icext(X282,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c90, c97])).
% 3.66/3.84  cnf(c341,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X281)|icext(X281,uri_rdfs_range),inference(resolution,[status(thm)],[c90, c61])).
% 3.66/3.84  cnf(c12,plain,iext(uri_rdf_rest,skolem0004,uri_rdf_nil),inference(split_conjunct,[status(thm)],[c2])).
% 3.66/3.84  cnf(c340,plain,~iext(uri_rdfs_domain,uri_rdf_rest,X280)|icext(X280,skolem0004),inference(resolution,[status(thm)],[c90, c12])).
% 3.66/3.84  cnf(c339,plain,~iext(uri_rdfs_domain,uri_rdf_rest,X279)|icext(X279,skolem0003),inference(resolution,[status(thm)],[c90, c10])).
% 3.66/3.84  cnf(c6,plain,iext(uri_rdf_first,skolem0002,uri_ex_hasFather),inference(split_conjunct,[status(thm)],[c2])).
% 3.66/3.84  cnf(c338,plain,~iext(uri_rdfs_domain,uri_rdf_first,X278)|icext(X278,skolem0002),inference(resolution,[status(thm)],[c90, c6])).
% 3.66/3.84  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.66/3.84  cnf(c23,plain,iext(uri_rdfs_range,uri_rdf_type,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_type_range])).
% 3.66/3.84  cnf(c337,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X277)|icext(X277,uri_rdf_type),inference(resolution,[status(thm)],[c90, c23])).
% 3.66/3.84  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.66/3.84  cnf(c24,plain,iext(uri_rdfs_domain,uri_rdf_type,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_type_domain])).
% 3.66/3.84  cnf(c334,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X274)|icext(X274,uri_rdf_type),inference(resolution,[status(thm)],[c90, c24])).
% 3.66/3.84  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.66/3.84  cnf(c58,plain,iext(uri_rdfs_domain,uri_rdf_predicate,uri_rdfs_Statement),inference(split_conjunct,[status(thm)],[rdfs_reification_predicate_domain])).
% 3.66/3.84  cnf(c333,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X273)|icext(X273,uri_rdf_predicate),inference(resolution,[status(thm)],[c90, c58])).
% 3.66/3.84  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.66/3.84  cnf(c22,plain,iext(uri_rdfs_domain,uri_rdf_value,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_value_domain])).
% 3.66/3.84  cnf(c331,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X271)|icext(X271,uri_rdf_value),inference(resolution,[status(thm)],[c90, c22])).
% 3.66/3.84  cnf(c8,plain,iext(uri_owl_propertyChainAxiom,uri_ex_hasCousin,skolem0003),inference(split_conjunct,[status(thm)],[c2])).
% 3.66/3.84  cnf(c330,plain,~iext(uri_rdfs_domain,uri_owl_propertyChainAxiom,X270)|icext(X270,uri_ex_hasCousin),inference(resolution,[status(thm)],[c90, c8])).
% 3.66/3.84  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.66/3.84  cnf(c21,plain,iext(uri_rdfs_range,uri_rdf_value,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_value_range])).
% 3.66/3.84  cnf(c329,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X269)|icext(X269,uri_rdf_value),inference(resolution,[status(thm)],[c90, c21])).
% 3.66/3.84  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.66/3.84  cnf(c108,plain,iext(uri_rdfs_range,uri_rdfs_member,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_member_range])).
% 3.66/3.84  cnf(c327,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X267)|icext(X267,uri_rdfs_member),inference(resolution,[status(thm)],[c90, c108])).
% 3.66/3.84  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.66/3.84  cnf(c103,plain,iext(uri_rdfs_range,uri_rdf__2,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_range_002])).
% 3.66/3.84  cnf(c325,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X265)|icext(X265,uri_rdf__2),inference(resolution,[status(thm)],[c90, c103])).
% 3.66/3.84  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.66/3.84  cnf(c107,plain,iext(uri_rdfs_domain,uri_rdf__1,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_001])).
% 3.66/3.84  cnf(c323,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X263)|icext(X263,uri_rdf__1),inference(resolution,[status(thm)],[c90, c107])).
% 3.66/3.84  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.66/3.84  cnf(c106,plain,iext(uri_rdfs_domain,uri_rdf__2,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_002])).
% 3.66/3.84  cnf(c322,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X262)|icext(X262,uri_rdf__2),inference(resolution,[status(thm)],[c90, c106])).
% 3.66/3.84  cnf(c321,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X261)|icext(X261,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c90, c92])).
% 3.66/3.84  cnf(c320,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X260)|icext(X260,uri_rdfs_domain),inference(resolution,[status(thm)],[c90, c85])).
% 3.66/3.84  cnf(c319,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X259)|icext(X259,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c90, c110])).
% 3.66/3.84  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.66/3.84  cnf(c102,plain,iext(uri_rdfs_range,uri_rdf__3,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_range_003])).
% 3.66/3.84  cnf(c318,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X258)|icext(X258,uri_rdf__3),inference(resolution,[status(thm)],[c90, c102])).
% 3.66/3.84  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.66/3.84  cnf(c105,plain,iext(uri_rdfs_domain,uri_rdf__3,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_003])).
% 3.66/3.84  cnf(c317,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X257)|icext(X257,uri_rdf__3),inference(resolution,[status(thm)],[c90, c105])).
% 3.66/3.84  cnf(c316,plain,~iext(uri_rdfs_domain,uri_ex_hasUncle,X256)|icext(X256,uri_ex_bob),inference(resolution,[status(thm)],[c90, c17])).
% 3.66/3.84  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.66/3.84  cnf(c104,plain,iext(uri_rdfs_range,uri_rdf__1,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_range_001])).
% 3.66/3.84  cnf(c315,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X255)|icext(X255,uri_rdf__1),inference(resolution,[status(thm)],[c90, c104])).
% 3.66/3.84  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.66/3.84  cnf(c39,plain,iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_subpropertyof_domain])).
% 3.66/3.84  cnf(c314,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X254)|icext(X254,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c90, c39])).
% 3.66/3.84  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.66/3.84  cnf(c55,plain,iext(uri_rdfs_range,uri_rdf_subject,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_reification_subject_range])).
% 3.66/3.84  cnf(c313,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X253)|icext(X253,uri_rdf_subject),inference(resolution,[status(thm)],[c90, c55])).
% 3.66/3.84  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.66/3.84  cnf(c46,plain,iext(uri_rdfs_range,uri_rdfs_subClassOf,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_subclassof_range])).
% 3.66/3.84  cnf(c311,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X251)|icext(X251,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c90, c46])).
% 3.66/3.84  cnf(c309,plain,~iext(uri_rdfs_domain,uri_owl_propertyChainAxiom,X249)|icext(X249,uri_ex_hasUncle),inference(resolution,[status(thm)],[c90, c3])).
% 3.66/3.84  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.66/3.84  cnf(c60,plain,iext(uri_rdfs_domain,uri_rdf_object,uri_rdfs_Statement),inference(split_conjunct,[status(thm)],[rdfs_reification_object_domain])).
% 3.66/3.84  cnf(c308,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X248)|icext(X248,uri_rdf_object),inference(resolution,[status(thm)],[c90, c60])).
% 3.66/3.84  cnf(c307,plain,~iext(uri_rdfs_domain,uri_ex_hasCousin,X247)|icext(X247,uri_ex_alice),inference(resolution,[status(thm)],[c90, c15])).
% 3.66/3.84  cnf(c306,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X246)|icext(X246,uri_rdf_subject),inference(resolution,[status(thm)],[c90, c56])).
% 3.66/3.84  cnf(c305,plain,~iext(uri_rdfs_domain,uri_owl_inverseOf,X245)|icext(X245,skolem0005),inference(resolution,[status(thm)],[c90, c13])).
% 3.66/3.84  cnf(c299,plain,~iext(uri_rdfs_subClassOf,X244,uri_rdfs_ContainerMembershipProperty)|iext(uri_rdfs_subClassOf,X244,uri_rdf_Property),inference(resolution,[status(thm)],[c110, c42])).
% 3.66/3.84  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.66/3.84  cnf(c109,plain,iext(uri_rdfs_domain,uri_rdfs_member,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_member_domain])).
% 3.66/3.84  cnf(c304,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X243)|icext(X243,uri_rdfs_member),inference(resolution,[status(thm)],[c90, c109])).
% 3.66/3.84  cnf(c303,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X242)|icext(X242,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c90, c54])).
% 3.66/3.84  cnf(c297,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X241)|iext(X241,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),inference(resolution,[status(thm)],[c110, c38])).
% 3.66/3.84  cnf(c302,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X240)|icext(X240,uri_rdfs_domain),inference(factor,[status(thm)],[c90])).
% 3.66/3.84  cnf(c300,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X239)|icext(X239,uri_rdf_Property),inference(resolution,[status(thm)],[c110, c64])).
% 3.66/3.84  cnf(c294,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X238)|iext(X238,uri_rdfs_member,uri_rdfs_Resource),inference(resolution,[status(thm)],[c109, c38])).
% 3.66/3.84  cnf(c292,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X236)|icext(X236,uri_rdfs_Container),inference(resolution,[status(thm)],[c64, c98])).
% 3.66/3.84  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.66/3.84  cnf(c66,plain,iext(uri_rdf_type,uri_rdf_Property,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_property_type])).
% 3.66/3.84  cnf(c291,plain,~iext(uri_rdfs_range,uri_rdf_type,X235)|icext(X235,uri_rdfs_Class),inference(resolution,[status(thm)],[c64, c66])).
% 3.66/3.84  cnf(c290,plain,~iext(uri_rdfs_range,uri_ex_hasFather,X234)|icext(X234,uri_ex_charly),inference(resolution,[status(thm)],[c64, c16])).
% 3.66/3.84  cnf(c289,plain,~iext(uri_rdfs_range,uri_ex_hasFather,X233)|icext(X233,uri_ex_dave),inference(resolution,[status(thm)],[c64, c14])).
% 3.66/3.84  cnf(c288,plain,~iext(uri_rdfs_range,uri_rdfs_range,X232)|icext(X232,uri_rdf_Property),inference(resolution,[status(thm)],[c64, c31])).
% 3.66/3.84  cnf(c446,plain,~iext(uri_rdfs_domain,uri_rdf_type,X229)|icext(X229,X230),inference(resolution,[status(thm)],[c433, c90])).
% 3.66/3.84  cnf(c286,plain,~iext(uri_rdfs_range,uri_rdf_first,X223)|icext(X223,skolem0005),inference(resolution,[status(thm)],[c64, c11])).
% 3.66/3.84  cnf(c283,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X210)|icext(X210,uri_rdfs_Literal),inference(resolution,[status(thm)],[c64, c97])).
% 3.66/3.84  cnf(c281,plain,~iext(uri_rdfs_range,uri_rdf_rest,X199)|icext(X199,uri_rdf_nil),inference(resolution,[status(thm)],[c64, c12])).
% 3.66/3.84  cnf(c53,plain,~iext(uri_rdfs_subClassOf,X80,X81)|~icext(X80,X79)|icext(X81,X79),inference(split_conjunct,[status(thm)],[c50])).
% 3.66/3.84  cnf(c368,plain,~icext(uri_rdf_Alt,X198)|icext(uri_rdfs_Container,X198),inference(resolution,[status(thm)],[c115, c53])).
% 3.66/3.84  cnf(c358,plain,~icext(uri_rdf_Bag,X196)|icext(uri_rdfs_Container,X196),inference(resolution,[status(thm)],[c114, c53])).
% 3.66/3.84  cnf(c279,plain,~iext(uri_rdfs_range,uri_rdf_first,X195)|icext(X195,uri_ex_hasFather),inference(resolution,[status(thm)],[c64, c6])).
% 3.66/3.84  cnf(c296,plain,~icext(uri_rdfs_ContainerMembershipProperty,X194)|icext(uri_rdf_Property,X194),inference(resolution,[status(thm)],[c110, c53])).
% 3.66/3.84  cnf(c277,plain,~iext(uri_rdfs_range,uri_rdf_first,X192)|icext(X192,uri_ex_hasUncle),inference(resolution,[status(thm)],[c64, c9])).
% 3.66/3.84  cnf(c276,plain,~iext(uri_rdfs_range,uri_rdf_first,X191)|icext(X191,uri_ex_hasCousin),inference(resolution,[status(thm)],[c64, c4])).
% 3.66/3.84  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.66/3.84  cnf(c96,plain,iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Datatype),inference(split_conjunct,[status(thm)],[rdfs_dat_xmlliteral_type])).
% 3.66/3.84  cnf(c273,plain,~iext(uri_rdfs_range,uri_rdf_type,X188)|icext(X188,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c64, c96])).
% 3.66/3.84  cnf(c271,plain,~iext(uri_rdfs_range,uri_owl_propertyChainAxiom,X186)|icext(X186,skolem0003),inference(resolution,[status(thm)],[c64, c8])).
% 3.66/3.84  cnf(c1164,plain,icext(uri_rdf_Property,uri_rdfs_member),inference(resolution,[status(thm)],[c818, c127])).
% 3.66/3.84  cnf(c262,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X177)|icext(X177,uri_rdfs_Class),inference(resolution,[status(thm)],[c64, c92])).
% 3.66/3.84  cnf(c259,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X174)|icext(X174,uri_rdfs_Resource),inference(resolution,[status(thm)],[c64, c105])).
% 3.66/3.84  cnf(c1134,plain,icext(uri_rdf_Property,uri_ex_hasFather),inference(resolution,[status(thm)],[c630, c127])).
% 3.66/3.84  cnf(c258,plain,~iext(uri_rdfs_range,uri_ex_hasUncle,X173)|icext(X173,uri_ex_dave),inference(resolution,[status(thm)],[c64, c17])).
% 3.66/3.84  cnf(c1119,plain,icext(uri_rdf_Property,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c628, c127])).
% 3.66/3.84  cnf(c256,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X171)|icext(X171,uri_rdf_Property),inference(resolution,[status(thm)],[c64, c39])).
% 3.66/3.84  cnf(c1102,plain,icext(uri_rdf_Property,uri_ex_hasUncle),inference(resolution,[status(thm)],[c626, c127])).
% 3.66/3.84  cnf(c255,plain,~iext(uri_rdfs_range,uri_rdfs_range,X170)|icext(X170,uri_rdfs_Resource),inference(resolution,[status(thm)],[c64, c55])).
% 3.66/3.84  cnf(c1084,plain,icext(uri_rdf_Property,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c624, c127])).
% 3.66/3.84  cnf(c253,plain,~iext(uri_rdfs_range,uri_rdfs_range,X168)|icext(X168,uri_rdfs_Class),inference(resolution,[status(thm)],[c64, c46])).
% 3.66/3.84  cnf(c252,plain,~iext(uri_rdfs_range,uri_rdf_type,X167)|icext(X167,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c64, c100])).
% 3.66/3.84  cnf(c1067,plain,icext(uri_rdf_Property,uri_owl_propertyChainAxiom),inference(resolution,[status(thm)],[c622, c127])).
% 3.66/3.84  cnf(c251,plain,~iext(uri_rdfs_range,uri_owl_propertyChainAxiom,X166)|icext(X166,skolem0001),inference(resolution,[status(thm)],[c64, c3])).
% 3.66/3.84  cnf(c1052,plain,icext(uri_rdf_Property,uri_ex_hasCousin),inference(resolution,[status(thm)],[c620, c127])).
% 3.66/3.84  cnf(c249,plain,~iext(uri_rdfs_range,uri_ex_hasCousin,X164)|icext(X164,uri_ex_bob),inference(resolution,[status(thm)],[c64, c15])).
% 3.66/3.84  cnf(c1020,plain,icext(uri_rdf_Property,uri_rdfs_range),inference(resolution,[status(thm)],[c618, c127])).
% 3.66/3.84  cnf(c247,plain,~iext(uri_rdfs_range,uri_owl_inverseOf,X162)|icext(X162,uri_ex_hasFather),inference(resolution,[status(thm)],[c64, c13])).
% 3.66/3.84  cnf(c1004,plain,icext(uri_rdf_Property,uri_owl_inverseOf),inference(resolution,[status(thm)],[c616, c127])).
% 3.66/3.84  cnf(c246,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X161)|icext(X161,uri_rdfs_Class),inference(resolution,[status(thm)],[c64, c54])).
% 3.66/3.84  cnf(c245,plain,~iext(uri_rdfs_range,uri_rdfs_range,X160)|icext(X160,X160),inference(factor,[status(thm)],[c64])).
% 3.66/3.84  cnf(c977,plain,icext(uri_rdf_Property,uri_rdfs_domain),inference(resolution,[status(thm)],[c614, c127])).
% 3.66/3.84  cnf(c241,plain,~icext(uri_rdfs_Seq,X159)|icext(uri_rdfs_Container,X159),inference(resolution,[status(thm)],[c53, c98])).
% 3.66/3.84  cnf(c240,plain,~icext(uri_rdf_XMLLiteral,X158)|icext(uri_rdfs_Literal,X158),inference(resolution,[status(thm)],[c53, c97])).
% 3.66/3.84  cnf(c239,plain,~icext(uri_rdfs_Datatype,X157)|icext(uri_rdfs_Class,X157),inference(resolution,[status(thm)],[c53, c92])).
% 3.66/3.84  cnf(c218,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X156)|iext(X156,uri_rdfs_member,uri_rdfs_Resource),inference(resolution,[status(thm)],[c108, c38])).
% 3.66/3.84  cnf(c217,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X155)|iext(X155,uri_rdf__1,uri_rdfs_Resource),inference(resolution,[status(thm)],[c107, c38])).
% 3.66/3.84  cnf(c216,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X154)|iext(X154,uri_rdf__2,uri_rdfs_Resource),inference(resolution,[status(thm)],[c106, c38])).
% 3.66/3.84  cnf(c215,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X153)|iext(X153,uri_rdf__3,uri_rdfs_Resource),inference(resolution,[status(thm)],[c105, c38])).
% 3.66/3.84  cnf(c214,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X152)|iext(X152,uri_rdf__1,uri_rdfs_Resource),inference(resolution,[status(thm)],[c104, c38])).
% 3.66/3.84  cnf(c213,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X151)|iext(X151,uri_rdf__2,uri_rdfs_Resource),inference(resolution,[status(thm)],[c103, c38])).
% 3.66/3.84  cnf(c919,plain,icext(uri_rdf_Property,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c484, c127])).
% 3.66/3.84  cnf(c212,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X150)|iext(X150,uri_rdf__3,uri_rdfs_Resource),inference(resolution,[status(thm)],[c102, c38])).
% 3.66/3.84  cnf(c912,plain,icext(uri_rdf_Property,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c482, c127])).
% 3.66/3.84  cnf(c211,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X149)|iext(X149,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c101, c38])).
% 3.66/3.84  cnf(c210,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X148)|iext(X148,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c100, c38])).
% 3.66/3.84  cnf(c209,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X147)|iext(X147,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c99, c38])).
% 3.66/3.84  cnf(c208,plain,~iext(uri_rdfs_subClassOf,X146,uri_rdfs_Seq)|iext(uri_rdfs_subClassOf,X146,uri_rdfs_Container),inference(resolution,[status(thm)],[c42, c98])).
% 3.66/3.84  cnf(c207,plain,~iext(uri_rdfs_subClassOf,X145,uri_rdf_XMLLiteral)|iext(uri_rdfs_subClassOf,X145,uri_rdfs_Literal),inference(resolution,[status(thm)],[c42, c97])).
% 3.66/3.84  cnf(c206,plain,~iext(uri_rdfs_subClassOf,X144,uri_rdfs_Datatype)|iext(uri_rdfs_subClassOf,X144,uri_rdfs_Class),inference(resolution,[status(thm)],[c42, c92])).
% 3.66/3.84  cnf(c204,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X142)|iext(X142,uri_rdfs_Seq,uri_rdfs_Container),inference(resolution,[status(thm)],[c98, c38])).
% 3.66/3.84  cnf(c203,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X141)|iext(X141,uri_rdf_XMLLiteral,uri_rdfs_Literal),inference(resolution,[status(thm)],[c97, c38])).
% 3.66/3.84  cnf(c202,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X140)|iext(X140,uri_rdf_XMLLiteral,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c96, c38])).
% 3.66/3.84  cnf(c201,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X139)|iext(X139,uri_rdfs_Datatype,uri_rdfs_Class),inference(resolution,[status(thm)],[c92, c38])).
% 3.66/3.84  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.66/3.84  cnf(c91,plain,iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_domain_domain])).
% 3.66/3.84  cnf(c200,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X138)|iext(X138,uri_rdfs_domain,uri_rdf_Property),inference(resolution,[status(thm)],[c91, c38])).
% 3.66/3.84  cnf(c199,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X137)|iext(X137,uri_rdf_Property,uri_rdfs_Class),inference(resolution,[status(thm)],[c38, c66])).
% 3.66/3.84  cnf(c198,plain,~iext(uri_rdfs_subPropertyOf,uri_ex_hasFather,X136)|iext(X136,uri_ex_bob,uri_ex_charly),inference(resolution,[status(thm)],[c38, c16])).
% 3.66/3.84  cnf(c197,plain,~iext(uri_rdfs_subPropertyOf,uri_ex_hasFather,X135)|iext(X135,uri_ex_alice,uri_ex_dave),inference(resolution,[status(thm)],[c38, c14])).
% 3.66/3.84  cnf(c196,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X134)|iext(X134,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c38, c31])).
% 3.66/3.84  cnf(c195,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X133)|iext(X133,uri_rdfs_range,uri_rdf_Property),inference(resolution,[status(thm)],[c38, c65])).
% 3.66/3.84  cnf(c194,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_first,X132)|iext(X132,skolem0004,skolem0005),inference(resolution,[status(thm)],[c38, c11])).
% 3.66/3.84  cnf(c193,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X131)|iext(X131,skolem0002,uri_rdf_nil),inference(resolution,[status(thm)],[c38, c7])).
% 3.66/3.84  cnf(c192,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X130)|iext(X130,skolem0001,skolem0002),inference(resolution,[status(thm)],[c38, c5])).
% 3.66/3.84  cnf(c191,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X129)|iext(X129,uri_rdfs_range,uri_rdfs_Class),inference(resolution,[status(thm)],[c38, c61])).
% 3.66/3.84  cnf(c190,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X128)|iext(X128,skolem0004,uri_rdf_nil),inference(resolution,[status(thm)],[c38, c12])).
% 3.66/3.84  cnf(c189,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X127)|iext(X127,skolem0003,skolem0004),inference(resolution,[status(thm)],[c38, c10])).
% 3.66/3.84  cnf(c188,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_first,X126)|iext(X126,skolem0002,uri_ex_hasFather),inference(resolution,[status(thm)],[c38, c6])).
% 3.66/3.84  cnf(c187,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X125)|iext(X125,uri_rdf_type,uri_rdfs_Class),inference(resolution,[status(thm)],[c38, c23])).
% 3.66/3.84  cnf(c186,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_first,X124)|iext(X124,skolem0003,uri_ex_hasUncle),inference(resolution,[status(thm)],[c38, c9])).
% 3.66/3.84  cnf(c185,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_first,X123)|iext(X123,skolem0001,uri_ex_hasCousin),inference(resolution,[status(thm)],[c38, c4])).
% 3.66/3.84  cnf(c184,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X122)|iext(X122,uri_rdf_type,uri_rdfs_Resource),inference(resolution,[status(thm)],[c38, c24])).
% 3.66/3.84  cnf(c183,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X121)|iext(X121,uri_rdf_predicate,uri_rdfs_Statement),inference(resolution,[status(thm)],[c38, c58])).
% 3.66/3.84  cnf(c182,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X120)|iext(X120,uri_rdf_value,uri_rdfs_Resource),inference(resolution,[status(thm)],[c38, c22])).
% 3.66/3.84  cnf(c181,plain,~iext(uri_rdfs_subPropertyOf,uri_owl_propertyChainAxiom,X119)|iext(X119,uri_ex_hasCousin,skolem0003),inference(resolution,[status(thm)],[c38, c8])).
% 3.66/3.84  cnf(c180,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X118)|iext(X118,uri_rdf_value,uri_rdfs_Resource),inference(resolution,[status(thm)],[c38, c21])).
% 3.66/3.84  cnf(c179,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X117)|iext(X117,uri_rdf_predicate,uri_rdfs_Resource),inference(resolution,[status(thm)],[c38, c57])).
% 3.66/3.84  cnf(c178,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X116)|iext(X116,uri_rdfs_domain,uri_rdfs_Class),inference(resolution,[status(thm)],[c38, c85])).
% 3.66/3.84  cnf(c177,plain,~iext(uri_rdfs_subPropertyOf,uri_ex_hasUncle,X115)|iext(X115,uri_ex_bob,uri_ex_dave),inference(resolution,[status(thm)],[c38, c17])).
% 3.66/3.84  cnf(c176,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X114)|iext(X114,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c38, c39])).
% 3.66/3.84  cnf(c175,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X113)|iext(X113,uri_rdf_subject,uri_rdfs_Resource),inference(resolution,[status(thm)],[c38, c55])).
% 3.66/3.84  cnf(c174,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X112)|iext(X112,uri_rdfs_subClassOf,uri_rdfs_Class),inference(resolution,[status(thm)],[c38, c46])).
% 3.66/3.84  cnf(c173,plain,~iext(uri_rdfs_subPropertyOf,uri_owl_propertyChainAxiom,X111)|iext(X111,uri_ex_hasUncle,skolem0001),inference(resolution,[status(thm)],[c38, c3])).
% 3.66/3.84  cnf(c172,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X110)|iext(X110,uri_rdf_object,uri_rdfs_Statement),inference(resolution,[status(thm)],[c38, c60])).
% 3.66/3.84  cnf(c171,plain,~iext(uri_rdfs_subPropertyOf,uri_ex_hasCousin,X109)|iext(X109,uri_ex_alice,uri_ex_bob),inference(resolution,[status(thm)],[c38, c15])).
% 3.66/3.84  cnf(c170,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X108)|iext(X108,uri_rdf_subject,uri_rdfs_Statement),inference(resolution,[status(thm)],[c38, c56])).
% 3.66/3.84  cnf(c169,plain,~iext(uri_rdfs_subPropertyOf,uri_owl_inverseOf,X107)|iext(X107,skolem0005,uri_ex_hasFather),inference(resolution,[status(thm)],[c38, c13])).
% 3.66/3.84  cnf(c168,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X106)|iext(X106,uri_rdfs_subClassOf,uri_rdfs_Class),inference(resolution,[status(thm)],[c38, c54])).
% 3.66/3.84  cnf(c167,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X105)|iext(X105,uri_rdfs_subPropertyOf,X105),inference(factor,[status(thm)],[c38])).
% 3.66/3.84  cnf(c532,plain,icext(uri_rdf_Property,uri_rdf_first),inference(resolution,[status(thm)],[c154, c127])).
% 3.66/3.84  cnf(c527,plain,icext(uri_rdf_List,uri_rdf_nil),inference(resolution,[status(thm)],[c153, c127])).
% 3.66/3.84  cnf(c517,plain,icext(uri_rdf_Property,uri_rdf_rest),inference(resolution,[status(thm)],[c152, c127])).
% 3.66/3.84  cnf(c512,plain,icext(uri_rdf_Property,uri_rdf__1),inference(resolution,[status(thm)],[c151, c127])).
% 3.66/3.84  cnf(c501,plain,icext(uri_rdf_Property,uri_rdf__2),inference(resolution,[status(thm)],[c150, c127])).
% 3.66/3.84  cnf(c496,plain,icext(uri_rdf_Property,uri_rdf__3),inference(resolution,[status(thm)],[c149, c127])).
% 3.66/3.84  cnf(c488,plain,icext(uri_rdf_Property,uri_rdf_object),inference(resolution,[status(thm)],[c148, c127])).
% 3.66/3.84  cnf(c476,plain,icext(uri_rdf_Property,uri_rdf_value),inference(resolution,[status(thm)],[c147, c127])).
% 3.66/3.84  cnf(c466,plain,icext(uri_rdf_Property,uri_rdf_subject),inference(resolution,[status(thm)],[c146, c127])).
% 3.66/3.84  cnf(c461,plain,icext(uri_rdf_Property,uri_rdf_type),inference(resolution,[status(thm)],[c138, c127])).
% 3.66/3.84  cnf(c422,plain,icext(uri_rdfs_Datatype,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c127, c96])).
% 3.66/3.85  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.66/3.85  fof(c93,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.66/3.85  fof(c94,plain,(![X36]:(~icext(uri_rdfs_Datatype,X36)|iext(uri_rdfs_subClassOf,X36,uri_rdfs_Literal))),inference(variable_rename,[status(thm)],[c93])).
% 3.66/3.85  cnf(c95,plain,~icext(uri_rdfs_Datatype,X90)|iext(uri_rdfs_subClassOf,X90,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[c94])).
% 3.66/3.85  cnf(c355,plain,icext(uri_rdfs_Class,uri_rdf_Property),inference(resolution,[status(thm)],[c301, c83])).
% 3.66/3.85  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.66/3.85  fof(c67,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.66/3.85  fof(c68,plain,((![X]:(~lv(X)|icext(uri_rdfs_Literal,X)))&(![X]:(~icext(uri_rdfs_Literal,X)|lv(X)))),inference(shift_quantors,[status(thm)],[c67])).
% 3.66/3.85  fof(c70,plain,(![X26]:(![X27]:((~lv(X26)|icext(uri_rdfs_Literal,X26))&(~icext(uri_rdfs_Literal,X27)|lv(X27))))),inference(shift_quantors,[status(thm)],[fof(c69,plain,((![X26]:(~lv(X26)|icext(uri_rdfs_Literal,X26)))&(![X27]:(~icext(uri_rdfs_Literal,X27)|lv(X27)))),inference(variable_rename,[status(thm)],[c68])).])).
% 3.66/3.85  cnf(c72,plain,~icext(uri_rdfs_Literal,X59)|lv(X59),inference(split_conjunct,[status(thm)],[c70])).
% 3.66/3.85  cnf(c71,plain,~lv(X58)|icext(uri_rdfs_Literal,X58),inference(split_conjunct,[status(thm)],[c70])).
% 3.66/3.85  fof(testcase_conclusion_fullish_025_Cyclic_Dependencies_between_Complex_Properties,conjecture,(iext(uri_ex_hasUncle,uri_ex_alice,uri_ex_charly)&iext(uri_ex_hasCousin,uri_ex_bob,uri_ex_alice)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', testcase_conclusion_fullish_025_Cyclic_Dependencies_between_Complex_Properties)).
% 3.66/3.85  fof(c18,negated_conjecture,(~(iext(uri_ex_hasUncle,uri_ex_alice,uri_ex_charly)&iext(uri_ex_hasCousin,uri_ex_bob,uri_ex_alice))),inference(assume_negation,[status(cth)],[testcase_conclusion_fullish_025_Cyclic_Dependencies_between_Complex_Properties])).
% 3.66/3.85  fof(c19,negated_conjecture,(~iext(uri_ex_hasUncle,uri_ex_alice,uri_ex_charly)|~iext(uri_ex_hasCousin,uri_ex_bob,uri_ex_alice)),inference(fof_nnf,[status(thm)],[c18])).
% 3.66/3.85  cnf(c20,negated_conjecture,~iext(uri_ex_hasUncle,uri_ex_alice,uri_ex_charly)|~iext(uri_ex_hasCousin,uri_ex_bob,uri_ex_alice),inference(split_conjunct,[status(thm)],[c19])).
% 3.66/3.85  % SZS output end Saturation
% 3.66/3.85  
% 3.66/3.85  % Initial clauses    : 105
% 3.66/3.85  % Processed clauses  : 614
% 3.66/3.85  % Factors computed   : 5
% 3.66/3.85  % Resolvents computed: 1398
% 3.66/3.85  % Tautologies deleted: 52
% 3.66/3.85  % Forward subsumed   : 842
% 3.66/3.85  % Backward subsumed  : 1
% 3.66/3.85  % -------- CPU Time ---------
% 3.66/3.85  % User time          : 3.477 s
% 3.66/3.85  % System time        : 0.014 s
% 3.66/3.85  % Total time         : 3.491 s
%------------------------------------------------------------------------------