PyRes---1.5.CSA-Sat.s

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

% Computer : n019.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8042.1875MB
% OS       : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Thu May  9 17:42:52 EDT 2024

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

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.09/0.13  % Problem  : SWB020+4 : TPTP v8.1.2. Released v5.2.0.
% 0.09/0.14  % Command  : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.34  % Computer : n019.cluster.edu
% 0.14/0.34  % Model    : x86_64 x86_64
% 0.14/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34  % Memory   : 8042.1875MB
% 0.14/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34  % CPULimit : 300
% 0.14/0.34  % WCLimit  : 300
% 0.14/0.34  % DateTime : Wed May  8 22:09:38 EDT 2024
% 0.14/0.35  % CPUTime  : 
% 3.64/3.82  % Version:  1.5
% 3.64/3.82  % SZS status CounterSatisfiable
% 3.64/3.82  % SZS output start Saturation
% 3.64/3.82  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.64/3.82  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.64/3.82  fof(c34,plain,(![X13]:(![X14]:(![X15]:(![X16]:(~iext(uri_rdfs_subPropertyOf,X13,X14)|((ip(X13)&ip(X14))&(~iext(X13,X15,X16)|iext(X14,X15,X16)))))))),inference(shift_quantors,[status(thm)],[fof(c33,plain,(![X13]:(![X14]:(~iext(uri_rdfs_subPropertyOf,X13,X14)|((ip(X13)&ip(X14))&(![X15]:(![X16]:(~iext(X13,X15,X16)|iext(X14,X15,X16)))))))),inference(variable_rename,[status(thm)],[c32])).])).
% 3.64/3.82  fof(c35,plain,(![X13]:(![X14]:(![X15]:(![X16]:(((~iext(uri_rdfs_subPropertyOf,X13,X14)|ip(X13))&(~iext(uri_rdfs_subPropertyOf,X13,X14)|ip(X14)))&(~iext(uri_rdfs_subPropertyOf,X13,X14)|(~iext(X13,X15,X16)|iext(X14,X15,X16)))))))),inference(distribute,[status(thm)],[c34])).
% 3.64/3.82  cnf(c38,plain,~iext(uri_rdfs_subPropertyOf,X72,X71)|~iext(X72,X70,X69)|iext(X71,X70,X69),inference(split_conjunct,[status(thm)],[c35])).
% 3.64/3.82  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.64/3.82  fof(c28,plain,(![P]:(~ip(P)|iext(uri_rdfs_subPropertyOf,P,P))),inference(fof_nnf,[status(thm)],[rdfs_subpropertyof_reflex])).
% 3.64/3.82  fof(c29,plain,(![X12]:(~ip(X12)|iext(uri_rdfs_subPropertyOf,X12,X12))),inference(variable_rename,[status(thm)],[c28])).
% 3.64/3.82  cnf(c30,plain,~ip(X57)|iext(uri_rdfs_subPropertyOf,X57,X57),inference(split_conjunct,[status(thm)],[c29])).
% 3.64/3.82  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.64/3.82  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.64/3.82  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.64/3.82  fof(c143,plain,(![X45]:(![X46]:((~iext(uri_rdf_type,X45,uri_rdf_Property)|ip(X45))&(~ip(X46)|iext(uri_rdf_type,X46,uri_rdf_Property))))),inference(shift_quantors,[status(thm)],[fof(c142,plain,((![X45]:(~iext(uri_rdf_type,X45,uri_rdf_Property)|ip(X45)))&(![X46]:(~ip(X46)|iext(uri_rdf_type,X46,uri_rdf_Property)))),inference(variable_rename,[status(thm)],[c141])).])).
% 3.64/3.82  cnf(c144,plain,~iext(uri_rdf_type,X101,uri_rdf_Property)|ip(X101),inference(split_conjunct,[status(thm)],[c143])).
% 3.64/3.82  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.64/3.82  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.64/3.82  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.64/3.82  fof(c126,plain,(![X41]:(![X42]:(![X43]:(![X44]:((~iext(uri_rdf_type,X41,X42)|icext(X42,X41))&(~icext(X44,X43)|iext(uri_rdf_type,X43,X44))))))),inference(shift_quantors,[status(thm)],[fof(c125,plain,((![X41]:(![X42]:(~iext(uri_rdf_type,X41,X42)|icext(X42,X41))))&(![X43]:(![X44]:(~icext(X44,X43)|iext(uri_rdf_type,X43,X44))))),inference(variable_rename,[status(thm)],[c124])).])).
% 3.64/3.82  cnf(c128,plain,~icext(X98,X97)|iext(uri_rdf_type,X97,X98),inference(split_conjunct,[status(thm)],[c126])).
% 3.64/3.82  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.64/3.82  cnf(c65,plain,iext(uri_rdfs_domain,uri_rdfs_range,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_range_domain])).
% 3.64/3.82  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.64/3.82  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.64/3.82  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.64/3.82  fof(c89,plain,(![X34]:(![X35]:(![X36]:(![X37]:((~iext(uri_rdfs_domain,X34,X35)|~iext(X34,X36,X37))|icext(X35,X36)))))),inference(shift_quantors,[status(thm)],[fof(c88,plain,(![X34]:(![X35]:(![X36]:((~iext(uri_rdfs_domain,X34,X35)|(![X37]:~iext(X34,X36,X37)))|icext(X35,X36))))),inference(variable_rename,[status(thm)],[c87])).])).
% 3.64/3.82  cnf(c90,plain,~iext(uri_rdfs_domain,X90,X88)|~iext(X90,X91,X89)|icext(X88,X91),inference(split_conjunct,[status(thm)],[c89])).
% 3.64/3.82  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.64/3.82  cnf(c136,plain,iext(uri_rdfs_range,uri_rdfs_comment,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[rdfs_annotation_comment_range])).
% 3.64/3.82  cnf(c468,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X343)|icext(X343,uri_rdfs_comment),inference(resolution,[status(thm)],[c136, c90])).
% 3.64/3.82  cnf(c1420,plain,icext(uri_rdf_Property,uri_rdfs_comment),inference(resolution,[status(thm)],[c468, c65])).
% 3.64/3.82  cnf(c1421,plain,iext(uri_rdf_type,uri_rdfs_comment,uri_rdf_Property),inference(resolution,[status(thm)],[c1420, c128])).
% 3.64/3.82  cnf(c1426,plain,ip(uri_rdfs_comment),inference(resolution,[status(thm)],[c1421, c144])).
% 3.64/3.82  cnf(c1429,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_comment,uri_rdfs_comment),inference(resolution,[status(thm)],[c1426, c30])).
% 3.64/3.82  cnf(c1432,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X701)|iext(X701,uri_rdfs_comment,uri_rdfs_comment),inference(resolution,[status(thm)],[c1429, c38])).
% 3.64/3.82  cnf(c1423,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X700)|iext(X700,uri_rdfs_comment,uri_rdf_Property),inference(resolution,[status(thm)],[c1421, c38])).
% 3.64/3.82  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.64/3.82  cnf(c131,plain,iext(uri_rdfs_range,uri_rdfs_label,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[rdfs_annotation_label_range])).
% 3.64/3.82  cnf(c418,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X326)|icext(X326,uri_rdfs_label),inference(resolution,[status(thm)],[c131, c90])).
% 3.64/3.82  cnf(c1390,plain,icext(uri_rdf_Property,uri_rdfs_label),inference(resolution,[status(thm)],[c418, c65])).
% 3.64/3.82  cnf(c1391,plain,iext(uri_rdf_type,uri_rdfs_label,uri_rdf_Property),inference(resolution,[status(thm)],[c1390, c128])).
% 3.64/3.82  cnf(c1397,plain,ip(uri_rdfs_label),inference(resolution,[status(thm)],[c1391, c144])).
% 3.64/3.82  cnf(c1400,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_label,uri_rdfs_label),inference(resolution,[status(thm)],[c1397, c30])).
% 3.64/3.82  cnf(c1403,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X698)|iext(X698,uri_rdfs_label,uri_rdfs_label),inference(resolution,[status(thm)],[c1400, c38])).
% 3.64/3.82  cnf(c1394,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X697)|iext(X697,uri_rdfs_label,uri_rdf_Property),inference(resolution,[status(thm)],[c1391, c38])).
% 3.64/3.82  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.64/3.82  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.64/3.82  fof(c41,plain,(![X17]:(![X18]:(![X19]:((~iext(uri_rdfs_subClassOf,X17,X18)|~iext(uri_rdfs_subClassOf,X18,X19))|iext(uri_rdfs_subClassOf,X17,X19))))),inference(variable_rename,[status(thm)],[c40])).
% 3.64/3.82  cnf(c42,plain,~iext(uri_rdfs_subClassOf,X75,X74)|~iext(uri_rdfs_subClassOf,X74,X73)|iext(uri_rdfs_subClassOf,X75,X73),inference(split_conjunct,[status(thm)],[c41])).
% 3.64/3.82  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.64/3.82  fof(c120,plain,(![C]:(~ic(C)|iext(uri_rdfs_subClassOf,C,uri_rdfs_Resource))),inference(fof_nnf,[status(thm)],[rdfs_class_instsub_resource])).
% 3.64/3.82  fof(c121,plain,(![X40]:(~ic(X40)|iext(uri_rdfs_subClassOf,X40,uri_rdfs_Resource))),inference(variable_rename,[status(thm)],[c120])).
% 3.64/3.82  cnf(c122,plain,~ic(X94)|iext(uri_rdfs_subClassOf,X94,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[c121])).
% 3.64/3.82  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.64/3.82  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.64/3.82  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.64/3.82  fof(c82,plain,(![X32]:(![X33]:((~ic(X32)|icext(uri_rdfs_Class,X32))&(~icext(uri_rdfs_Class,X33)|ic(X33))))),inference(shift_quantors,[status(thm)],[fof(c81,plain,((![X32]:(~ic(X32)|icext(uri_rdfs_Class,X32)))&(![X33]:(~icext(uri_rdfs_Class,X33)|ic(X33)))),inference(variable_rename,[status(thm)],[c80])).])).
% 3.64/3.82  cnf(c84,plain,~icext(uri_rdfs_Class,X68)|ic(X68),inference(split_conjunct,[status(thm)],[c82])).
% 3.64/3.82  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.64/3.82  cnf(c61,plain,iext(uri_rdfs_range,uri_rdfs_range,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_range_range])).
% 3.64/3.82  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.64/3.82  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.64/3.82  fof(c63,plain,(![X24]:(![X25]:(![X26]:(![X27]:((~iext(uri_rdfs_range,X24,X25)|~iext(X24,X26,X27))|icext(X25,X27)))))),inference(variable_rename,[status(thm)],[c62])).
% 3.64/3.82  cnf(c64,plain,~iext(uri_rdfs_range,X87,X84)|~iext(X87,X86,X85)|icext(X84,X85),inference(split_conjunct,[status(thm)],[c63])).
% 3.64/3.82  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.64/3.82  cnf(c116,plain,iext(uri_rdfs_range,uri_rdf_rest,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdfs_collection_rest_range])).
% 3.64/3.82  cnf(c389,plain,~iext(uri_rdfs_range,uri_rdfs_range,X305)|icext(X305,uri_rdf_List),inference(resolution,[status(thm)],[c116, c64])).
% 3.64/3.82  cnf(c1349,plain,icext(uri_rdfs_Class,uri_rdf_List),inference(resolution,[status(thm)],[c389, c61])).
% 3.64/3.82  cnf(c1350,plain,ic(uri_rdf_List),inference(resolution,[status(thm)],[c1349, c84])).
% 3.64/3.82  cnf(c1353,plain,iext(uri_rdfs_subClassOf,uri_rdf_List,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1350, c122])).
% 3.64/3.82  cnf(c1375,plain,~iext(uri_rdfs_subClassOf,X696,uri_rdf_List)|iext(uri_rdfs_subClassOf,X696,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1353, c42])).
% 3.64/3.82  cnf(c1371,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X695)|iext(X695,uri_rdf_List,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1353, c38])).
% 3.64/3.82  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.64/3.82  fof(c43,plain,(![C]:(~ic(C)|iext(uri_rdfs_subClassOf,C,C))),inference(fof_nnf,[status(thm)],[rdfs_subclassof_reflex])).
% 3.64/3.82  fof(c44,plain,(![X20]:(~ic(X20)|iext(uri_rdfs_subClassOf,X20,X20))),inference(variable_rename,[status(thm)],[c43])).
% 3.64/3.82  cnf(c45,plain,~ic(X76)|iext(uri_rdfs_subClassOf,X76,X76),inference(split_conjunct,[status(thm)],[c44])).
% 3.64/3.82  cnf(c1352,plain,iext(uri_rdfs_subClassOf,uri_rdf_List,uri_rdf_List),inference(resolution,[status(thm)],[c1350, c45])).
% 3.64/3.82  cnf(c1362,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X693)|iext(X693,uri_rdf_List,uri_rdf_List),inference(resolution,[status(thm)],[c1352, c38])).
% 3.64/3.82  cnf(c1351,plain,iext(uri_rdf_type,uri_rdf_List,uri_rdfs_Class),inference(resolution,[status(thm)],[c1349, c128])).
% 3.64/3.82  cnf(c1357,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X692)|iext(X692,uri_rdf_List,uri_rdfs_Class),inference(resolution,[status(thm)],[c1351, c38])).
% 3.64/3.82  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.64/3.82  cnf(c117,plain,iext(uri_rdfs_domain,uri_rdf_rest,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdfs_collection_rest_domain])).
% 3.64/3.82  fof(testcase_premise_fullish_020_Logical_Complications,axiom,(?[BNODE_xs]:(?[BNODE_xc]:(?[BNODE_lu1]:(?[BNODE_lu2]:(?[BNODE_lu3]:(?[BNODE_li1]:(?[BNODE_li2]:((((((((((((((iext(uri_owl_unionOf,uri_ex_c,BNODE_lu1)&iext(uri_rdf_first,BNODE_lu1,uri_ex_c1))&iext(uri_rdf_rest,BNODE_lu1,BNODE_lu2))&iext(uri_rdf_first,BNODE_lu2,uri_ex_c2))&iext(uri_rdf_rest,BNODE_lu2,BNODE_lu3))&iext(uri_rdf_first,BNODE_lu3,uri_ex_c3))&iext(uri_rdf_rest,BNODE_lu3,uri_rdf_nil))&iext(uri_owl_disjointWith,uri_ex_d,uri_ex_c1))&iext(uri_rdfs_subClassOf,uri_ex_d,BNODE_xs))&iext(uri_owl_intersectionOf,BNODE_xs,BNODE_li1))&iext(uri_rdf_first,BNODE_li1,uri_ex_c))&iext(uri_rdf_rest,BNODE_li1,BNODE_li2))&iext(uri_rdf_first,BNODE_li2,BNODE_xc))&iext(uri_rdf_rest,BNODE_li2,uri_rdf_nil))&iext(uri_owl_complementOf,BNODE_xc,uri_ex_c2))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', testcase_premise_fullish_020_Logical_Complications)).
% 3.64/3.82  fof(c0,plain,(?[BNODE_xs]:(?[BNODE_xc]:((?[BNODE_lu1]:(?[BNODE_lu2]:(?[BNODE_lu3]:(?[BNODE_li1]:(?[BNODE_li2]:(((((((((((((iext(uri_owl_unionOf,uri_ex_c,BNODE_lu1)&iext(uri_rdf_first,BNODE_lu1,uri_ex_c1))&iext(uri_rdf_rest,BNODE_lu1,BNODE_lu2))&iext(uri_rdf_first,BNODE_lu2,uri_ex_c2))&iext(uri_rdf_rest,BNODE_lu2,BNODE_lu3))&iext(uri_rdf_first,BNODE_lu3,uri_ex_c3))&iext(uri_rdf_rest,BNODE_lu3,uri_rdf_nil))&iext(uri_owl_disjointWith,uri_ex_d,uri_ex_c1))&iext(uri_rdfs_subClassOf,uri_ex_d,BNODE_xs))&iext(uri_owl_intersectionOf,BNODE_xs,BNODE_li1))&iext(uri_rdf_first,BNODE_li1,uri_ex_c))&iext(uri_rdf_rest,BNODE_li1,BNODE_li2))&iext(uri_rdf_first,BNODE_li2,BNODE_xc))&iext(uri_rdf_rest,BNODE_li2,uri_rdf_nil)))))))&iext(uri_owl_complementOf,BNODE_xc,uri_ex_c2)))),inference(shift_quantors,[status(thm)],[testcase_premise_fullish_020_Logical_Complications])).
% 3.64/3.82  fof(c1,plain,(?[X2]:(?[X3]:((?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:(((((((((((((iext(uri_owl_unionOf,uri_ex_c,X4)&iext(uri_rdf_first,X4,uri_ex_c1))&iext(uri_rdf_rest,X4,X5))&iext(uri_rdf_first,X5,uri_ex_c2))&iext(uri_rdf_rest,X5,X6))&iext(uri_rdf_first,X6,uri_ex_c3))&iext(uri_rdf_rest,X6,uri_rdf_nil))&iext(uri_owl_disjointWith,uri_ex_d,uri_ex_c1))&iext(uri_rdfs_subClassOf,uri_ex_d,X2))&iext(uri_owl_intersectionOf,X2,X7))&iext(uri_rdf_first,X7,uri_ex_c))&iext(uri_rdf_rest,X7,X8))&iext(uri_rdf_first,X8,X3))&iext(uri_rdf_rest,X8,uri_rdf_nil)))))))&iext(uri_owl_complementOf,X3,uri_ex_c2)))),inference(variable_rename,[status(thm)],[c0])).
% 3.64/3.82  fof(c2,plain,((((((((((((((iext(uri_owl_unionOf,uri_ex_c,skolem0003)&iext(uri_rdf_first,skolem0003,uri_ex_c1))&iext(uri_rdf_rest,skolem0003,skolem0004))&iext(uri_rdf_first,skolem0004,uri_ex_c2))&iext(uri_rdf_rest,skolem0004,skolem0005))&iext(uri_rdf_first,skolem0005,uri_ex_c3))&iext(uri_rdf_rest,skolem0005,uri_rdf_nil))&iext(uri_owl_disjointWith,uri_ex_d,uri_ex_c1))&iext(uri_rdfs_subClassOf,uri_ex_d,skolem0001))&iext(uri_owl_intersectionOf,skolem0001,skolem0006))&iext(uri_rdf_first,skolem0006,uri_ex_c))&iext(uri_rdf_rest,skolem0006,skolem0007))&iext(uri_rdf_first,skolem0007,skolem0002))&iext(uri_rdf_rest,skolem0007,uri_rdf_nil))&iext(uri_owl_complementOf,skolem0002,uri_ex_c2)),inference(skolemize,[status(esa)],[c1])).
% 3.64/3.82  cnf(c14,plain,iext(uri_rdf_rest,skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c2])).
% 3.64/3.82  cnf(c328,plain,~iext(uri_rdfs_domain,uri_rdf_rest,X271)|icext(X271,skolem0006),inference(resolution,[status(thm)],[c90, c14])).
% 3.64/3.82  cnf(c1317,plain,icext(uri_rdf_List,skolem0006),inference(resolution,[status(thm)],[c328, c117])).
% 3.64/3.82  cnf(c1318,plain,iext(uri_rdf_type,skolem0006,uri_rdf_List),inference(resolution,[status(thm)],[c1317, c128])).
% 3.64/3.82  cnf(c1320,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X691)|iext(X691,skolem0006,uri_rdf_List),inference(resolution,[status(thm)],[c1318, c38])).
% 3.64/3.82  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.64/3.82  cnf(c119,plain,iext(uri_rdfs_domain,uri_rdf_first,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdfs_collection_first_domain])).
% 3.64/3.82  cnf(c4,plain,iext(uri_rdf_first,skolem0003,uri_ex_c1),inference(split_conjunct,[status(thm)],[c2])).
% 3.64/3.82  cnf(c313,plain,~iext(uri_rdfs_domain,uri_rdf_first,X256)|icext(X256,skolem0003),inference(resolution,[status(thm)],[c90, c4])).
% 3.64/3.82  cnf(c1300,plain,icext(uri_rdf_List,skolem0003),inference(resolution,[status(thm)],[c313, c119])).
% 3.64/3.82  cnf(c1301,plain,iext(uri_rdf_type,skolem0003,uri_rdf_List),inference(resolution,[status(thm)],[c1300, c128])).
% 3.64/3.82  cnf(c1303,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X690)|iext(X690,skolem0003,uri_rdf_List),inference(resolution,[status(thm)],[c1301, c38])).
% 3.64/3.82  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.64/3.82  cnf(c91,plain,iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_domain_domain])).
% 3.64/3.82  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.64/3.82  cnf(c58,plain,iext(uri_rdfs_domain,uri_rdf_predicate,uri_rdfs_Statement),inference(split_conjunct,[status(thm)],[rdfs_reification_predicate_domain])).
% 3.64/3.82  cnf(c303,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X246)|icext(X246,uri_rdf_predicate),inference(resolution,[status(thm)],[c90, c58])).
% 3.64/3.82  cnf(c1275,plain,icext(uri_rdf_Property,uri_rdf_predicate),inference(resolution,[status(thm)],[c303, c91])).
% 3.64/3.82  cnf(c1276,plain,iext(uri_rdf_type,uri_rdf_predicate,uri_rdf_Property),inference(resolution,[status(thm)],[c1275, c128])).
% 3.64/3.82  cnf(c1281,plain,ip(uri_rdf_predicate),inference(resolution,[status(thm)],[c1276, c144])).
% 3.64/3.82  cnf(c1285,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_predicate,uri_rdf_predicate),inference(resolution,[status(thm)],[c1281, c30])).
% 3.64/3.82  cnf(c1288,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X688)|iext(X688,uri_rdf_predicate,uri_rdf_predicate),inference(resolution,[status(thm)],[c1285, c38])).
% 3.64/3.82  cnf(c1278,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X687)|iext(X687,uri_rdf_predicate,uri_rdf_Property),inference(resolution,[status(thm)],[c1276, c38])).
% 3.64/3.82  cnf(c278,plain,~iext(uri_rdfs_range,uri_rdf_rest,X190)|icext(X190,skolem0007),inference(resolution,[status(thm)],[c64, c14])).
% 3.64/3.82  cnf(c1240,plain,icext(uri_rdf_List,skolem0007),inference(resolution,[status(thm)],[c278, c116])).
% 3.64/3.82  cnf(c1241,plain,iext(uri_rdf_type,skolem0007,uri_rdf_List),inference(resolution,[status(thm)],[c1240, c128])).
% 3.64/3.82  cnf(c1265,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X686)|iext(X686,skolem0007,uri_rdf_List),inference(resolution,[status(thm)],[c1241, c38])).
% 3.64/3.82  cnf(c7,plain,iext(uri_rdf_rest,skolem0004,skolem0005),inference(split_conjunct,[status(thm)],[c2])).
% 3.64/3.82  cnf(c275,plain,~iext(uri_rdfs_range,uri_rdf_rest,X187)|icext(X187,skolem0005),inference(resolution,[status(thm)],[c64, c7])).
% 3.64/3.82  cnf(c1224,plain,icext(uri_rdf_List,skolem0005),inference(resolution,[status(thm)],[c275, c116])).
% 3.64/3.82  cnf(c1225,plain,iext(uri_rdf_type,skolem0005,uri_rdf_List),inference(resolution,[status(thm)],[c1224, c128])).
% 3.64/3.82  cnf(c1260,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X685)|iext(X685,skolem0005,uri_rdf_List),inference(resolution,[status(thm)],[c1225, c38])).
% 3.64/3.82  cnf(c5,plain,iext(uri_rdf_rest,skolem0003,skolem0004),inference(split_conjunct,[status(thm)],[c2])).
% 3.64/3.82  cnf(c274,plain,~iext(uri_rdfs_range,uri_rdf_rest,X186)|icext(X186,skolem0004),inference(resolution,[status(thm)],[c64, c5])).
% 3.64/3.82  cnf(c1222,plain,icext(uri_rdf_List,skolem0004),inference(resolution,[status(thm)],[c274, c116])).
% 3.64/3.82  cnf(c1223,plain,iext(uri_rdf_type,skolem0004,uri_rdf_List),inference(resolution,[status(thm)],[c1222, c128])).
% 3.64/3.82  cnf(c1255,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X684)|iext(X684,skolem0004,uri_rdf_List),inference(resolution,[status(thm)],[c1223, c38])).
% 3.64/3.82  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.64/3.82  cnf(c85,plain,iext(uri_rdfs_range,uri_rdfs_domain,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_domain_range])).
% 3.64/3.82  cnf(c253,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X165)|icext(X165,uri_rdfs_Statement),inference(resolution,[status(thm)],[c64, c58])).
% 3.64/3.82  cnf(c1031,plain,icext(uri_rdfs_Class,uri_rdfs_Statement),inference(resolution,[status(thm)],[c253, c85])).
% 3.64/3.82  cnf(c1032,plain,ic(uri_rdfs_Statement),inference(resolution,[status(thm)],[c1031, c84])).
% 3.64/3.82  cnf(c1035,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Statement,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1032, c122])).
% 3.64/3.82  cnf(c1247,plain,~iext(uri_rdfs_subClassOf,X683,uri_rdfs_Statement)|iext(uri_rdfs_subClassOf,X683,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1035, c42])).
% 3.64/3.82  cnf(c1243,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X682)|iext(X682,uri_rdfs_Statement,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1035, c38])).
% 3.64/3.82  cnf(c1034,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Statement,uri_rdfs_Statement),inference(resolution,[status(thm)],[c1032, c45])).
% 3.64/3.82  cnf(c1233,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X680)|iext(X680,uri_rdfs_Statement,uri_rdfs_Statement),inference(resolution,[status(thm)],[c1034, c38])).
% 3.64/3.82  cnf(c1033,plain,iext(uri_rdf_type,uri_rdfs_Statement,uri_rdfs_Class),inference(resolution,[status(thm)],[c1031, c128])).
% 3.64/3.82  cnf(c1228,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X679)|iext(X679,uri_rdfs_Statement,uri_rdfs_Class),inference(resolution,[status(thm)],[c1033, c38])).
% 3.64/3.82  cnf(c37,plain,~iext(uri_rdfs_subPropertyOf,X64,X63)|ip(X63),inference(split_conjunct,[status(thm)],[c35])).
% 3.64/3.82  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.64/3.82  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.64/3.82  fof(c112,plain,(![X39]:(~icext(uri_rdfs_ContainerMembershipProperty,X39)|iext(uri_rdfs_subPropertyOf,X39,uri_rdfs_member))),inference(variable_rename,[status(thm)],[c111])).
% 3.64/3.82  cnf(c113,plain,~icext(uri_rdfs_ContainerMembershipProperty,X93)|iext(uri_rdfs_subPropertyOf,X93,uri_rdfs_member),inference(split_conjunct,[status(thm)],[c112])).
% 3.64/3.82  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.64/3.82  cnf(c100,plain,iext(uri_rdf_type,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),inference(split_conjunct,[status(thm)],[rdfs_container_n_type_002])).
% 3.64/3.82  cnf(c127,plain,~iext(uri_rdf_type,X95,X96)|icext(X96,X95),inference(split_conjunct,[status(thm)],[c126])).
% 3.64/3.82  cnf(c432,plain,icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__2),inference(resolution,[status(thm)],[c127, c100])).
% 3.64/3.82  cnf(c437,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__2,uri_rdfs_member),inference(resolution,[status(thm)],[c432, c113])).
% 3.64/3.82  cnf(c859,plain,ip(uri_rdfs_member),inference(resolution,[status(thm)],[c437, c37])).
% 3.64/3.82  cnf(c863,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_member,uri_rdfs_member),inference(resolution,[status(thm)],[c859, c30])).
% 3.64/3.82  cnf(c1216,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X677)|iext(X677,uri_rdfs_member,uri_rdfs_member),inference(resolution,[status(thm)],[c863, c38])).
% 3.64/3.82  cnf(c145,plain,~ip(X102)|iext(uri_rdf_type,X102,uri_rdf_Property),inference(split_conjunct,[status(thm)],[c143])).
% 3.64/3.82  cnf(c862,plain,iext(uri_rdf_type,uri_rdfs_member,uri_rdf_Property),inference(resolution,[status(thm)],[c859, c145])).
% 3.64/3.82  cnf(c1208,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X676)|iext(X676,uri_rdfs_member,uri_rdf_Property),inference(resolution,[status(thm)],[c862, c38])).
% 3.64/3.82  cnf(c83,plain,~ic(X67)|icext(uri_rdfs_Class,X67),inference(split_conjunct,[status(thm)],[c82])).
% 3.64/3.82  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.64/3.82  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.64/3.82  fof(c49,plain,(![X21]:(![X22]:(![X23]:(~iext(uri_rdfs_subClassOf,X21,X22)|((ic(X21)&ic(X22))&(~icext(X21,X23)|icext(X22,X23))))))),inference(shift_quantors,[status(thm)],[fof(c48,plain,(![X21]:(![X22]:(~iext(uri_rdfs_subClassOf,X21,X22)|((ic(X21)&ic(X22))&(![X23]:(~icext(X21,X23)|icext(X22,X23))))))),inference(variable_rename,[status(thm)],[c47])).])).
% 3.64/3.82  fof(c50,plain,(![X21]:(![X22]:(![X23]:(((~iext(uri_rdfs_subClassOf,X21,X22)|ic(X21))&(~iext(uri_rdfs_subClassOf,X21,X22)|ic(X22)))&(~iext(uri_rdfs_subClassOf,X21,X22)|(~icext(X21,X23)|icext(X22,X23))))))),inference(distribute,[status(thm)],[c49])).
% 3.64/3.82  cnf(c52,plain,~iext(uri_rdfs_subClassOf,X80,X79)|ic(X79),inference(split_conjunct,[status(thm)],[c50])).
% 3.64/3.82  cnf(c51,plain,~iext(uri_rdfs_subClassOf,X78,X77)|ic(X78),inference(split_conjunct,[status(thm)],[c50])).
% 3.64/3.82  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.64/3.82  cnf(c110,plain,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_container_containermembershipproperty_sub])).
% 3.64/3.82  cnf(c361,plain,ic(uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c110, c51])).
% 3.64/3.82  cnf(c403,plain,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Resource),inference(resolution,[status(thm)],[c122, c361])).
% 3.64/3.82  cnf(c744,plain,ic(uri_rdfs_Resource),inference(resolution,[status(thm)],[c403, c52])).
% 3.64/3.82  cnf(c750,plain,icext(uri_rdfs_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c744, c83])).
% 3.64/3.82  cnf(c752,plain,iext(uri_rdf_type,uri_rdfs_Resource,uri_rdfs_Class),inference(resolution,[status(thm)],[c750, c128])).
% 3.64/3.82  cnf(c1203,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X675)|iext(X675,uri_rdfs_Resource,uri_rdfs_Class),inference(resolution,[status(thm)],[c752, c38])).
% 3.64/3.82  cnf(c748,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Resource,uri_rdfs_Resource),inference(resolution,[status(thm)],[c744, c45])).
% 3.64/3.82  cnf(c1196,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X673)|iext(X673,uri_rdfs_Resource,uri_rdfs_Resource),inference(resolution,[status(thm)],[c748, c38])).
% 3.64/3.82  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.64/3.82  cnf(c133,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_sub])).
% 3.64/3.82  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.64/3.82  fof(c160,plain,(![S]:(![P]:(![O]:(~iext(P,S,O)|ip(P))))),inference(fof_nnf,[status(thm)],[simple_iext_property])).
% 3.64/3.82  fof(c161,plain,(![S]:(![P]:((![O]:~iext(P,S,O))|ip(P)))),inference(shift_quantors,[status(thm)],[c160])).
% 3.64/3.82  fof(c163,plain,(![X49]:(![X50]:(![X51]:(~iext(X50,X49,X51)|ip(X50))))),inference(shift_quantors,[status(thm)],[fof(c162,plain,(![X49]:(![X50]:((![X51]:~iext(X50,X49,X51))|ip(X50)))),inference(variable_rename,[status(thm)],[c161])).])).
% 3.64/3.82  cnf(c164,plain,~iext(X104,X105,X103)|ip(X104),inference(split_conjunct,[status(thm)],[c163])).
% 3.64/3.82  cnf(c617,plain,ip(uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c164, c133])).
% 3.64/3.82  cnf(c643,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c617, c30])).
% 3.64/3.82  cnf(c1187,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X671)|iext(X671,uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c643, c38])).
% 3.64/3.82  cnf(c642,plain,iext(uri_rdf_type,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c617, c145])).
% 3.64/3.82  cnf(c1180,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X670)|iext(X670,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c642, c38])).
% 3.64/3.82  cnf(c17,plain,iext(uri_owl_complementOf,skolem0002,uri_ex_c2),inference(split_conjunct,[status(thm)],[c2])).
% 3.64/3.82  cnf(c615,plain,ip(uri_owl_complementOf),inference(resolution,[status(thm)],[c164, c17])).
% 3.64/3.82  cnf(c641,plain,iext(uri_rdfs_subPropertyOf,uri_owl_complementOf,uri_owl_complementOf),inference(resolution,[status(thm)],[c615, c30])).
% 3.64/3.82  cnf(c1171,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X668)|iext(X668,uri_owl_complementOf,uri_owl_complementOf),inference(resolution,[status(thm)],[c641, c38])).
% 3.64/3.82  cnf(c640,plain,iext(uri_rdf_type,uri_owl_complementOf,uri_rdf_Property),inference(resolution,[status(thm)],[c615, c145])).
% 3.64/3.82  cnf(c1164,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X667)|iext(X667,uri_owl_complementOf,uri_rdf_Property),inference(resolution,[status(thm)],[c640, c38])).
% 3.64/3.82  cnf(c3,plain,iext(uri_owl_unionOf,uri_ex_c,skolem0003),inference(split_conjunct,[status(thm)],[c2])).
% 3.64/3.82  cnf(c604,plain,ip(uri_owl_unionOf),inference(resolution,[status(thm)],[c164, c3])).
% 3.64/3.82  cnf(c639,plain,iext(uri_rdfs_subPropertyOf,uri_owl_unionOf,uri_owl_unionOf),inference(resolution,[status(thm)],[c604, c30])).
% 3.64/3.82  cnf(c1155,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X665)|iext(X665,uri_owl_unionOf,uri_owl_unionOf),inference(resolution,[status(thm)],[c639, c38])).
% 3.64/3.82  cnf(c638,plain,iext(uri_rdf_type,uri_owl_unionOf,uri_rdf_Property),inference(resolution,[status(thm)],[c604, c145])).
% 3.64/3.82  cnf(c1148,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X664)|iext(X664,uri_owl_unionOf,uri_rdf_Property),inference(resolution,[status(thm)],[c638, c38])).
% 3.64/3.82  cnf(c12,plain,iext(uri_owl_intersectionOf,skolem0001,skolem0006),inference(split_conjunct,[status(thm)],[c2])).
% 3.64/3.82  cnf(c579,plain,ip(uri_owl_intersectionOf),inference(resolution,[status(thm)],[c164, c12])).
% 3.64/3.82  cnf(c637,plain,iext(uri_rdfs_subPropertyOf,uri_owl_intersectionOf,uri_owl_intersectionOf),inference(resolution,[status(thm)],[c579, c30])).
% 3.64/3.82  cnf(c1139,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X662)|iext(X662,uri_owl_intersectionOf,uri_owl_intersectionOf),inference(resolution,[status(thm)],[c637, c38])).
% 3.64/3.82  cnf(c636,plain,iext(uri_rdf_type,uri_owl_intersectionOf,uri_rdf_Property),inference(resolution,[status(thm)],[c579, c145])).
% 3.64/3.82  cnf(c1131,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X661)|iext(X661,uri_owl_intersectionOf,uri_rdf_Property),inference(resolution,[status(thm)],[c636, c38])).
% 3.64/3.82  cnf(c10,plain,iext(uri_owl_disjointWith,uri_ex_d,uri_ex_c1),inference(split_conjunct,[status(thm)],[c2])).
% 3.64/3.82  cnf(c576,plain,ip(uri_owl_disjointWith),inference(resolution,[status(thm)],[c164, c10])).
% 3.64/3.82  cnf(c635,plain,iext(uri_rdfs_subPropertyOf,uri_owl_disjointWith,uri_owl_disjointWith),inference(resolution,[status(thm)],[c576, c30])).
% 3.64/3.82  cnf(c1122,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X659)|iext(X659,uri_owl_disjointWith,uri_owl_disjointWith),inference(resolution,[status(thm)],[c635, c38])).
% 3.64/3.82  cnf(c634,plain,iext(uri_rdf_type,uri_owl_disjointWith,uri_rdf_Property),inference(resolution,[status(thm)],[c576, c145])).
% 3.64/3.82  cnf(c1114,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X658)|iext(X658,uri_owl_disjointWith,uri_rdf_Property),inference(resolution,[status(thm)],[c634, c38])).
% 3.64/3.82  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.64/3.82  cnf(c97,plain,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[rdfs_dat_xmlliteral_sub])).
% 3.64/3.82  cnf(c555,plain,ip(uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c164, c97])).
% 3.64/3.82  cnf(c633,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c555, c30])).
% 3.64/3.82  cnf(c1103,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X656)|iext(X656,uri_rdfs_subClassOf,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c633, c38])).
% 3.64/3.82  cnf(c632,plain,iext(uri_rdf_type,uri_rdfs_subClassOf,uri_rdf_Property),inference(resolution,[status(thm)],[c555, c145])).
% 3.64/3.82  cnf(c1094,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X655)|iext(X655,uri_rdfs_subClassOf,uri_rdf_Property),inference(resolution,[status(thm)],[c632, c38])).
% 3.64/3.82  cnf(c554,plain,ip(uri_rdfs_range),inference(resolution,[status(thm)],[c164, c61])).
% 3.64/3.82  cnf(c631,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_range,uri_rdfs_range),inference(resolution,[status(thm)],[c554, c30])).
% 3.64/3.82  cnf(c1075,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X653)|iext(X653,uri_rdfs_range,uri_rdfs_range),inference(resolution,[status(thm)],[c631, c38])).
% 3.64/3.82  cnf(c630,plain,iext(uri_rdf_type,uri_rdfs_range,uri_rdf_Property),inference(resolution,[status(thm)],[c554, c145])).
% 3.64/3.82  cnf(c1066,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X652)|iext(X652,uri_rdfs_range,uri_rdf_Property),inference(resolution,[status(thm)],[c630, c38])).
% 3.64/3.82  cnf(c553,plain,ip(uri_rdfs_domain),inference(resolution,[status(thm)],[c164, c58])).
% 3.64/3.82  cnf(c629,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,uri_rdfs_domain),inference(resolution,[status(thm)],[c553, c30])).
% 3.64/3.82  cnf(c1048,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X650)|iext(X650,uri_rdfs_domain,uri_rdfs_domain),inference(resolution,[status(thm)],[c629, c38])).
% 3.64/3.82  cnf(c628,plain,iext(uri_rdf_type,uri_rdfs_domain,uri_rdf_Property),inference(resolution,[status(thm)],[c553, c145])).
% 3.64/3.82  cnf(c1038,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X649)|iext(X649,uri_rdfs_domain,uri_rdf_Property),inference(resolution,[status(thm)],[c628, c38])).
% 3.64/3.82  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.64/3.82  cnf(c154,plain,iext(uri_rdf_type,uri_rdf_first,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_collection_first_type])).
% 3.64/3.82  cnf(c544,plain,ip(uri_rdf_first),inference(resolution,[status(thm)],[c154, c144])).
% 3.64/3.82  cnf(c550,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_first,uri_rdf_first),inference(resolution,[status(thm)],[c544, c30])).
% 3.64/3.82  cnf(c1020,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X647)|iext(X647,uri_rdf_first,uri_rdf_first),inference(resolution,[status(thm)],[c550, c38])).
% 3.64/3.82  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.64/3.82  cnf(c152,plain,iext(uri_rdf_type,uri_rdf_rest,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_collection_rest_type])).
% 3.64/3.82  cnf(c529,plain,ip(uri_rdf_rest),inference(resolution,[status(thm)],[c152, c144])).
% 3.64/3.82  cnf(c537,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_rest,uri_rdf_rest),inference(resolution,[status(thm)],[c529, c30])).
% 3.64/3.82  cnf(c1006,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X645)|iext(X645,uri_rdf_rest,uri_rdf_rest),inference(resolution,[status(thm)],[c537, c38])).
% 3.64/3.82  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.64/3.82  cnf(c151,plain,iext(uri_rdf_type,uri_rdf__1,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_container_n_type_001])).
% 3.64/3.82  cnf(c524,plain,ip(uri_rdf__1),inference(resolution,[status(thm)],[c151, c144])).
% 3.64/3.82  cnf(c535,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__1,uri_rdf__1),inference(resolution,[status(thm)],[c524, c30])).
% 3.64/3.82  cnf(c999,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X643)|iext(X643,uri_rdf__1,uri_rdf__1),inference(resolution,[status(thm)],[c535, c38])).
% 3.64/3.82  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.64/3.82  cnf(c150,plain,iext(uri_rdf_type,uri_rdf__2,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_container_n_type_002])).
% 3.64/3.82  cnf(c513,plain,ip(uri_rdf__2),inference(resolution,[status(thm)],[c150, c144])).
% 3.64/3.82  cnf(c521,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__2,uri_rdf__2),inference(resolution,[status(thm)],[c513, c30])).
% 3.64/3.82  cnf(c992,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X641)|iext(X641,uri_rdf__2,uri_rdf__2),inference(resolution,[status(thm)],[c521, c38])).
% 3.64/3.82  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.64/3.82  cnf(c149,plain,iext(uri_rdf_type,uri_rdf__3,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_container_n_type_003])).
% 3.64/3.82  cnf(c508,plain,ip(uri_rdf__3),inference(resolution,[status(thm)],[c149, c144])).
% 3.64/3.82  cnf(c519,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__3,uri_rdf__3),inference(resolution,[status(thm)],[c508, c30])).
% 3.64/3.82  cnf(c985,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X639)|iext(X639,uri_rdf__3,uri_rdf__3),inference(resolution,[status(thm)],[c519, c38])).
% 3.64/3.82  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.64/3.82  cnf(c148,plain,iext(uri_rdf_type,uri_rdf_object,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_reification_object_type])).
% 3.64/3.82  cnf(c500,plain,ip(uri_rdf_object),inference(resolution,[status(thm)],[c148, c144])).
% 3.64/3.82  cnf(c506,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_object,uri_rdf_object),inference(resolution,[status(thm)],[c500, c30])).
% 3.64/3.82  cnf(c978,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X637)|iext(X637,uri_rdf_object,uri_rdf_object),inference(resolution,[status(thm)],[c506, c38])).
% 3.64/3.82  cnf(c426,plain,ip(uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c133, c37])).
% 3.64/3.82  cnf(c496,plain,iext(uri_rdf_type,uri_rdfs_seeAlso,uri_rdf_Property),inference(resolution,[status(thm)],[c145, c426])).
% 3.64/3.82  cnf(c971,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X636)|iext(X636,uri_rdfs_seeAlso,uri_rdf_Property),inference(resolution,[status(thm)],[c496, c38])).
% 3.64/3.82  cnf(c36,plain,~iext(uri_rdfs_subPropertyOf,X59,X58)|ip(X59),inference(split_conjunct,[status(thm)],[c35])).
% 3.64/3.82  cnf(c427,plain,ip(uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c133, c36])).
% 3.64/3.82  cnf(c494,plain,iext(uri_rdf_type,uri_rdfs_isDefinedBy,uri_rdf_Property),inference(resolution,[status(thm)],[c145, c427])).
% 3.64/3.82  cnf(c964,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X635)|iext(X635,uri_rdfs_isDefinedBy,uri_rdf_Property),inference(resolution,[status(thm)],[c494, c38])).
% 3.64/3.82  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.64/3.82  cnf(c147,plain,iext(uri_rdf_type,uri_rdf_value,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_reification_predicate_type])).
% 3.64/3.82  cnf(c488,plain,ip(uri_rdf_value),inference(resolution,[status(thm)],[c147, c144])).
% 3.64/3.82  cnf(c493,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_value,uri_rdf_value),inference(resolution,[status(thm)],[c488, c30])).
% 3.64/3.82  cnf(c957,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X633)|iext(X633,uri_rdf_value,uri_rdf_value),inference(resolution,[status(thm)],[c493, c38])).
% 3.64/3.82  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.64/3.82  cnf(c138,plain,iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_value_type])).
% 3.64/3.82  cnf(c484,plain,ip(uri_rdf_type),inference(resolution,[status(thm)],[c144, c138])).
% 3.64/3.82  cnf(c486,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_type,uri_rdf_type),inference(resolution,[status(thm)],[c484, c30])).
% 3.64/3.82  cnf(c945,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X631)|iext(X631,uri_rdf_type,uri_rdf_type),inference(resolution,[status(thm)],[c486, c38])).
% 3.64/3.82  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.64/3.83  cnf(c146,plain,iext(uri_rdf_type,uri_rdf_subject,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_reification_subject_type])).
% 3.64/3.83  cnf(c483,plain,ip(uri_rdf_subject),inference(resolution,[status(thm)],[c144, c146])).
% 3.64/3.83  cnf(c485,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_subject,uri_rdf_subject),inference(resolution,[status(thm)],[c483, c30])).
% 3.64/3.83  cnf(c938,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X629)|iext(X629,uri_rdf_subject,uri_rdf_subject),inference(resolution,[status(thm)],[c485, c38])).
% 3.64/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.64/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.64/3.83  cnf(c221,plain,ic(uri_rdfs_Seq),inference(resolution,[status(thm)],[c51, c98])).
% 3.64/3.83  cnf(c227,plain,icext(uri_rdfs_Class,uri_rdfs_Seq),inference(resolution,[status(thm)],[c221, c83])).
% 3.64/3.83  cnf(c455,plain,iext(uri_rdf_type,uri_rdfs_Seq,uri_rdfs_Class),inference(resolution,[status(thm)],[c128, c227])).
% 3.64/3.83  cnf(c933,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X628)|iext(X628,uri_rdfs_Seq,uri_rdfs_Class),inference(resolution,[status(thm)],[c455, c38])).
% 3.64/3.83  cnf(c220,plain,ic(uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c51, c97])).
% 3.64/3.83  cnf(c225,plain,icext(uri_rdfs_Class,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c220, c83])).
% 3.64/3.83  cnf(c454,plain,iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Class),inference(resolution,[status(thm)],[c128, c225])).
% 3.64/3.83  cnf(c928,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X627)|iext(X627,uri_rdf_XMLLiteral,uri_rdfs_Class),inference(resolution,[status(thm)],[c454, c38])).
% 3.64/3.83  cnf(c11,plain,iext(uri_rdfs_subClassOf,uri_ex_d,skolem0001),inference(split_conjunct,[status(thm)],[c2])).
% 3.64/3.83  cnf(c222,plain,ic(uri_ex_d),inference(resolution,[status(thm)],[c51, c11])).
% 3.64/3.83  cnf(c229,plain,icext(uri_rdfs_Class,uri_ex_d),inference(resolution,[status(thm)],[c222, c83])).
% 3.64/3.83  cnf(c452,plain,iext(uri_rdf_type,uri_ex_d,uri_rdfs_Class),inference(resolution,[status(thm)],[c128, c229])).
% 3.64/3.83  cnf(c923,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X626)|iext(X626,uri_ex_d,uri_rdfs_Class),inference(resolution,[status(thm)],[c452, c38])).
% 3.64/3.83  cnf(c233,plain,ic(uri_rdfs_Literal),inference(resolution,[status(thm)],[c52, c97])).
% 3.64/3.83  cnf(c238,plain,icext(uri_rdfs_Class,uri_rdfs_Literal),inference(resolution,[status(thm)],[c233, c83])).
% 3.64/3.83  cnf(c449,plain,iext(uri_rdf_type,uri_rdfs_Literal,uri_rdfs_Class),inference(resolution,[status(thm)],[c128, c238])).
% 3.64/3.83  cnf(c918,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X625)|iext(X625,uri_rdfs_Literal,uri_rdfs_Class),inference(resolution,[status(thm)],[c449, c38])).
% 3.64/3.83  cnf(c235,plain,ic(skolem0001),inference(resolution,[status(thm)],[c52, c11])).
% 3.64/3.83  cnf(c242,plain,icext(uri_rdfs_Class,skolem0001),inference(resolution,[status(thm)],[c235, c83])).
% 3.64/3.83  cnf(c448,plain,iext(uri_rdf_type,skolem0001,uri_rdfs_Class),inference(resolution,[status(thm)],[c128, c242])).
% 3.64/3.83  cnf(c912,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X624)|iext(X624,skolem0001,uri_rdfs_Class),inference(resolution,[status(thm)],[c448, c38])).
% 3.64/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.64/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.64/3.83  cnf(c374,plain,ic(uri_rdf_Bag),inference(resolution,[status(thm)],[c114, c51])).
% 3.64/3.83  cnf(c376,plain,icext(uri_rdfs_Class,uri_rdf_Bag),inference(resolution,[status(thm)],[c374, c83])).
% 3.64/3.83  cnf(c446,plain,iext(uri_rdf_type,uri_rdf_Bag,uri_rdfs_Class),inference(resolution,[status(thm)],[c128, c376])).
% 3.64/3.83  cnf(c906,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X623)|iext(X623,uri_rdf_Bag,uri_rdfs_Class),inference(resolution,[status(thm)],[c446, c38])).
% 3.64/3.83  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.64/3.83  cnf(c92,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_datatype_sub])).
% 3.64/3.83  cnf(c236,plain,ic(uri_rdfs_Class),inference(resolution,[status(thm)],[c52, c92])).
% 3.64/3.83  cnf(c244,plain,icext(uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c236, c83])).
% 3.64/3.83  cnf(c445,plain,iext(uri_rdf_type,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c128, c244])).
% 3.64/3.83  cnf(c901,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X622)|iext(X622,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c445, c38])).
% 3.64/3.83  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.64/3.83  cnf(c115,plain,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Container),inference(split_conjunct,[status(thm)],[rdfs_container_alt_sub])).
% 3.64/3.83  cnf(c383,plain,ic(uri_rdf_Alt),inference(resolution,[status(thm)],[c115, c51])).
% 3.64/3.83  cnf(c385,plain,icext(uri_rdfs_Class,uri_rdf_Alt),inference(resolution,[status(thm)],[c383, c83])).
% 3.64/3.83  cnf(c444,plain,iext(uri_rdf_type,uri_rdf_Alt,uri_rdfs_Class),inference(resolution,[status(thm)],[c128, c385])).
% 3.64/3.83  cnf(c895,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X621)|iext(X621,uri_rdf_Alt,uri_rdfs_Class),inference(resolution,[status(thm)],[c444, c38])).
% 3.64/3.83  cnf(c223,plain,ic(uri_rdfs_Datatype),inference(resolution,[status(thm)],[c51, c92])).
% 3.64/3.83  cnf(c231,plain,icext(uri_rdfs_Class,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c223, c83])).
% 3.64/3.83  cnf(c443,plain,iext(uri_rdf_type,uri_rdfs_Datatype,uri_rdfs_Class),inference(resolution,[status(thm)],[c128, c231])).
% 3.64/3.83  cnf(c889,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X620)|iext(X620,uri_rdfs_Datatype,uri_rdfs_Class),inference(resolution,[status(thm)],[c443, c38])).
% 3.64/3.83  cnf(c365,plain,icext(uri_rdfs_Class,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c361, c83])).
% 3.64/3.83  cnf(c442,plain,iext(uri_rdf_type,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Class),inference(resolution,[status(thm)],[c128, c365])).
% 3.64/3.83  cnf(c884,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X619)|iext(X619,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Class),inference(resolution,[status(thm)],[c442, c38])).
% 3.64/3.83  cnf(c234,plain,ic(uri_rdfs_Container),inference(resolution,[status(thm)],[c52, c98])).
% 3.64/3.83  cnf(c240,plain,icext(uri_rdfs_Class,uri_rdfs_Container),inference(resolution,[status(thm)],[c234, c83])).
% 3.64/3.83  cnf(c440,plain,iext(uri_rdf_type,uri_rdfs_Container,uri_rdfs_Class),inference(resolution,[status(thm)],[c128, c240])).
% 3.64/3.83  cnf(c879,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X618)|iext(X618,uri_rdfs_Container,uri_rdfs_Class),inference(resolution,[status(thm)],[c440, c38])).
% 3.64/3.83  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.64/3.83  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.64/3.83  fof(c26,plain,(![X9]:(![X10]:(![X11]:((~iext(uri_rdfs_subPropertyOf,X9,X10)|~iext(uri_rdfs_subPropertyOf,X10,X11))|iext(uri_rdfs_subPropertyOf,X9,X11))))),inference(variable_rename,[status(thm)],[c25])).
% 3.64/3.83  cnf(c27,plain,~iext(uri_rdfs_subPropertyOf,X54,X56)|~iext(uri_rdfs_subPropertyOf,X56,X55)|iext(uri_rdfs_subPropertyOf,X54,X55),inference(split_conjunct,[status(thm)],[c26])).
% 3.64/3.83  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.64/3.83  cnf(c99,plain,iext(uri_rdf_type,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),inference(split_conjunct,[status(thm)],[rdfs_container_n_type_003])).
% 3.64/3.83  cnf(c434,plain,icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__3),inference(resolution,[status(thm)],[c127, c99])).
% 3.64/3.83  cnf(c439,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__3,uri_rdfs_member),inference(resolution,[status(thm)],[c434, c113])).
% 3.64/3.83  cnf(c877,plain,~iext(uri_rdfs_subPropertyOf,X617,uri_rdf__3)|iext(uri_rdfs_subPropertyOf,X617,uri_rdfs_member),inference(resolution,[status(thm)],[c439, c27])).
% 3.64/3.83  cnf(c872,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X616)|iext(X616,uri_rdf__3,uri_rdfs_member),inference(resolution,[status(thm)],[c439, c38])).
% 3.64/3.83  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.64/3.83  cnf(c101,plain,iext(uri_rdf_type,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),inference(split_conjunct,[status(thm)],[rdfs_container_n_type_001])).
% 3.64/3.83  cnf(c433,plain,icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__1),inference(resolution,[status(thm)],[c127, c101])).
% 3.64/3.83  cnf(c438,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__1,uri_rdfs_member),inference(resolution,[status(thm)],[c433, c113])).
% 3.64/3.83  cnf(c870,plain,~iext(uri_rdfs_subPropertyOf,X615,uri_rdf__1)|iext(uri_rdfs_subPropertyOf,X615,uri_rdfs_member),inference(resolution,[status(thm)],[c438, c27])).
% 3.64/3.83  cnf(c865,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X614)|iext(X614,uri_rdf__1,uri_rdfs_member),inference(resolution,[status(thm)],[c438, c38])).
% 3.64/3.83  cnf(c861,plain,~iext(uri_rdfs_subPropertyOf,X613,uri_rdf__2)|iext(uri_rdfs_subPropertyOf,X613,uri_rdfs_member),inference(resolution,[status(thm)],[c437, c27])).
% 3.64/3.83  cnf(c856,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X612)|iext(X612,uri_rdf__2,uri_rdfs_member),inference(resolution,[status(thm)],[c437, c38])).
% 3.64/3.83  cnf(c1433,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X610)|icext(X610,uri_rdfs_comment),inference(resolution,[status(thm)],[c1429, c90])).
% 3.64/3.83  cnf(c1431,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X609)|icext(X609,uri_rdfs_comment),inference(resolution,[status(thm)],[c1429, c64])).
% 3.64/3.83  cnf(c436,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c427, c30])).
% 3.64/3.83  cnf(c849,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X607)|iext(X607,uri_rdfs_isDefinedBy,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c436, c38])).
% 3.64/3.83  cnf(c1404,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X605)|icext(X605,uri_rdfs_label),inference(resolution,[status(thm)],[c1400, c90])).
% 3.64/3.83  cnf(c1402,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X604)|icext(X604,uri_rdfs_label),inference(resolution,[status(thm)],[c1400, c64])).
% 3.64/3.83  cnf(c430,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_seeAlso,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c426, c30])).
% 3.64/3.83  cnf(c842,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X598)|iext(X598,uri_rdfs_seeAlso,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c430, c38])).
% 3.64/3.83  cnf(c1363,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X597)|icext(X597,uri_rdf_List),inference(resolution,[status(thm)],[c1352, c90])).
% 3.64/3.83  cnf(c1361,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X596)|icext(X596,uri_rdf_List),inference(resolution,[status(thm)],[c1352, c64])).
% 3.64/3.83  cnf(c414,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Resource),inference(resolution,[status(thm)],[c122, c223])).
% 3.64/3.83  cnf(c838,plain,~iext(uri_rdfs_subClassOf,X595,uri_rdfs_Datatype)|iext(uri_rdfs_subClassOf,X595,uri_rdfs_Resource),inference(resolution,[status(thm)],[c414, c42])).
% 3.64/3.83  cnf(c835,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X590)|iext(X590,uri_rdfs_Datatype,uri_rdfs_Resource),inference(resolution,[status(thm)],[c414, c38])).
% 3.64/3.83  cnf(c1289,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X587)|icext(X587,uri_rdf_predicate),inference(resolution,[status(thm)],[c1285, c90])).
% 3.64/3.83  cnf(c413,plain,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Resource),inference(resolution,[status(thm)],[c122, c220])).
% 3.64/3.83  cnf(c830,plain,~iext(uri_rdfs_subClassOf,X586,uri_rdf_XMLLiteral)|iext(uri_rdfs_subClassOf,X586,uri_rdfs_Resource),inference(resolution,[status(thm)],[c413, c42])).
% 3.64/3.83  cnf(c1287,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X585)|icext(X585,uri_rdf_predicate),inference(resolution,[status(thm)],[c1285, c64])).
% 3.64/3.83  cnf(c827,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X582)|iext(X582,uri_rdf_XMLLiteral,uri_rdfs_Resource),inference(resolution,[status(thm)],[c413, c38])).
% 3.64/3.83  cnf(c412,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Resource),inference(resolution,[status(thm)],[c122, c221])).
% 3.64/3.83  cnf(c822,plain,~iext(uri_rdfs_subClassOf,X577,uri_rdfs_Seq)|iext(uri_rdfs_subClassOf,X577,uri_rdfs_Resource),inference(resolution,[status(thm)],[c412, c42])).
% 3.64/3.83  cnf(c819,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X572)|iext(X572,uri_rdfs_Seq,uri_rdfs_Resource),inference(resolution,[status(thm)],[c412, c38])).
% 3.64/3.83  cnf(c1234,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X571)|icext(X571,uri_rdfs_Statement),inference(resolution,[status(thm)],[c1034, c90])).
% 3.64/3.83  cnf(c411,plain,iext(uri_rdfs_subClassOf,skolem0001,uri_rdfs_Resource),inference(resolution,[status(thm)],[c122, c235])).
% 3.64/3.83  cnf(c814,plain,~iext(uri_rdfs_subClassOf,X570,skolem0001)|iext(uri_rdfs_subClassOf,X570,uri_rdfs_Resource),inference(resolution,[status(thm)],[c411, c42])).
% 3.64/3.83  cnf(c1232,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X569)|icext(X569,uri_rdfs_Statement),inference(resolution,[status(thm)],[c1034, c64])).
% 3.64/3.83  cnf(c811,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X566)|iext(X566,skolem0001,uri_rdfs_Resource),inference(resolution,[status(thm)],[c411, c38])).
% 3.64/3.83  cnf(c1218,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X565)|icext(X565,uri_rdfs_member),inference(resolution,[status(thm)],[c863, c90])).
% 3.64/3.83  cnf(c357,plain,ic(uri_rdf_Property),inference(resolution,[status(thm)],[c110, c52])).
% 3.64/3.83  cnf(c410,plain,iext(uri_rdfs_subClassOf,uri_rdf_Property,uri_rdfs_Resource),inference(resolution,[status(thm)],[c122, c357])).
% 3.64/3.83  cnf(c806,plain,~iext(uri_rdfs_subClassOf,X562,uri_rdf_Property)|iext(uri_rdfs_subClassOf,X562,uri_rdfs_Resource),inference(resolution,[status(thm)],[c410, c42])).
% 3.64/3.83  cnf(c803,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X558)|iext(X558,uri_rdf_Property,uri_rdfs_Resource),inference(resolution,[status(thm)],[c410, c38])).
% 3.64/3.83  cnf(c1197,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X557)|icext(X557,uri_rdfs_Resource),inference(resolution,[status(thm)],[c748, c90])).
% 3.64/3.83  cnf(c409,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Container,uri_rdfs_Resource),inference(resolution,[status(thm)],[c122, c234])).
% 3.64/3.83  cnf(c798,plain,~iext(uri_rdfs_subClassOf,X556,uri_rdfs_Container)|iext(uri_rdfs_subClassOf,X556,uri_rdfs_Resource),inference(resolution,[status(thm)],[c409, c42])).
% 3.64/3.83  cnf(c1190,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X554)|icext(X554,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c643, c90])).
% 3.64/3.83  cnf(c795,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X553)|iext(X553,uri_rdfs_Container,uri_rdfs_Resource),inference(resolution,[status(thm)],[c409, c38])).
% 3.64/3.83  cnf(c1186,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X552)|icext(X552,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c643, c64])).
% 3.64/3.83  cnf(c408,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Literal,uri_rdfs_Resource),inference(resolution,[status(thm)],[c122, c233])).
% 3.64/3.83  cnf(c790,plain,~iext(uri_rdfs_subClassOf,X549,uri_rdfs_Literal)|iext(uri_rdfs_subClassOf,X549,uri_rdfs_Resource),inference(resolution,[status(thm)],[c408, c42])).
% 3.64/3.83  cnf(c1173,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X548)|icext(X548,uri_owl_complementOf),inference(resolution,[status(thm)],[c641, c90])).
% 3.64/3.83  cnf(c1170,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X547)|icext(X547,uri_owl_complementOf),inference(resolution,[status(thm)],[c641, c64])).
% 3.64/3.83  cnf(c787,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X546)|iext(X546,uri_rdfs_Literal,uri_rdfs_Resource),inference(resolution,[status(thm)],[c408, c38])).
% 3.64/3.83  cnf(c1158,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X543)|icext(X543,uri_owl_unionOf),inference(resolution,[status(thm)],[c639, c90])).
% 3.64/3.83  cnf(c407,plain,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Resource),inference(resolution,[status(thm)],[c122, c383])).
% 3.64/3.83  cnf(c782,plain,~iext(uri_rdfs_subClassOf,X542,uri_rdf_Alt)|iext(uri_rdfs_subClassOf,X542,uri_rdfs_Resource),inference(resolution,[status(thm)],[c407, c42])).
% 3.64/3.83  cnf(c1154,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X541)|icext(X541,uri_owl_unionOf),inference(resolution,[status(thm)],[c639, c64])).
% 3.64/3.83  cnf(c779,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X538)|iext(X538,uri_rdf_Alt,uri_rdfs_Resource),inference(resolution,[status(thm)],[c407, c38])).
% 3.64/3.83  cnf(c1142,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X537)|icext(X537,uri_owl_intersectionOf),inference(resolution,[status(thm)],[c637, c90])).
% 3.64/3.83  cnf(c1138,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X536)|icext(X536,uri_owl_intersectionOf),inference(resolution,[status(thm)],[c637, c64])).
% 3.64/3.83  cnf(c406,plain,iext(uri_rdfs_subClassOf,uri_ex_d,uri_rdfs_Resource),inference(resolution,[status(thm)],[c122, c222])).
% 3.64/3.83  cnf(c774,plain,~iext(uri_rdfs_subClassOf,X535,uri_ex_d)|iext(uri_rdfs_subClassOf,X535,uri_rdfs_Resource),inference(resolution,[status(thm)],[c406, c42])).
% 3.64/3.83  cnf(c1125,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X532)|icext(X532,uri_owl_disjointWith),inference(resolution,[status(thm)],[c635, c90])).
% 3.64/3.83  cnf(c771,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X531)|iext(X531,uri_ex_d,uri_rdfs_Resource),inference(resolution,[status(thm)],[c406, c38])).
% 3.64/3.83  cnf(c1121,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X530)|icext(X530,uri_owl_disjointWith),inference(resolution,[status(thm)],[c635, c64])).
% 3.64/3.83  cnf(c405,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c122, c236])).
% 3.64/3.83  cnf(c766,plain,~iext(uri_rdfs_subClassOf,X528,uri_rdfs_Class)|iext(uri_rdfs_subClassOf,X528,uri_rdfs_Resource),inference(resolution,[status(thm)],[c405, c42])).
% 3.64/3.83  cnf(c1107,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X526)|icext(X526,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c633, c90])).
% 3.64/3.83  cnf(c763,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X525)|iext(X525,uri_rdfs_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c405, c38])).
% 3.64/3.83  cnf(c1102,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X524)|icext(X524,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c633, c64])).
% 3.64/3.83  cnf(c404,plain,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Resource),inference(resolution,[status(thm)],[c122, c374])).
% 3.64/3.83  cnf(c758,plain,~iext(uri_rdfs_subClassOf,X521,uri_rdf_Bag)|iext(uri_rdfs_subClassOf,X521,uri_rdfs_Resource),inference(resolution,[status(thm)],[c404, c42])).
% 3.64/3.83  cnf(c1078,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X520)|icext(X520,uri_rdfs_range),inference(resolution,[status(thm)],[c631, c90])).
% 3.64/3.83  cnf(c1073,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X519)|icext(X519,uri_rdfs_range),inference(resolution,[status(thm)],[c631, c64])).
% 3.64/3.83  cnf(c755,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X517)|iext(X517,uri_rdf_Bag,uri_rdfs_Resource),inference(resolution,[status(thm)],[c404, c38])).
% 3.64/3.83  cnf(c1053,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X515)|icext(X515,uri_rdfs_domain),inference(resolution,[status(thm)],[c629, c90])).
% 3.64/3.83  cnf(c745,plain,~iext(uri_rdfs_subClassOf,X514,uri_rdfs_ContainerMembershipProperty)|iext(uri_rdfs_subClassOf,X514,uri_rdfs_Resource),inference(resolution,[status(thm)],[c403, c42])).
% 3.64/3.83  cnf(c1045,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X513)|icext(X513,uri_rdfs_domain),inference(resolution,[status(thm)],[c629, c64])).
% 3.64/3.83  cnf(c742,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X510)|iext(X510,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Resource),inference(resolution,[status(thm)],[c403, c38])).
% 3.64/3.83  cnf(c1025,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X509)|icext(X509,uri_rdf_first),inference(resolution,[status(thm)],[c550, c90])).
% 3.64/3.83  cnf(c1019,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X508)|icext(X508,uri_rdf_first),inference(resolution,[status(thm)],[c550, c64])).
% 3.64/3.83  cnf(c1010,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X507)|icext(X507,uri_rdf_rest),inference(resolution,[status(thm)],[c537, c90])).
% 3.64/3.83  cnf(c1005,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X505)|icext(X505,uri_rdf_rest),inference(resolution,[status(thm)],[c537, c64])).
% 3.64/3.83  cnf(c384,plain,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdf_Alt),inference(resolution,[status(thm)],[c383, c45])).
% 3.64/3.83  cnf(c734,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X503)|iext(X503,uri_rdf_Alt,uri_rdf_Alt),inference(resolution,[status(thm)],[c384, c38])).
% 3.64/3.83  cnf(c998,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X502)|icext(X502,uri_rdf__1),inference(resolution,[status(thm)],[c535, c64])).
% 3.64/3.83  cnf(c991,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X500)|icext(X500,uri_rdf__2),inference(resolution,[status(thm)],[c521, c64])).
% 3.64/3.83  cnf(c984,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X497)|icext(X497,uri_rdf__3),inference(resolution,[status(thm)],[c519, c64])).
% 3.64/3.83  cnf(c980,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X496)|icext(X496,uri_rdf_object),inference(resolution,[status(thm)],[c506, c90])).
% 3.64/3.83  cnf(c375,plain,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdf_Bag),inference(resolution,[status(thm)],[c374, c45])).
% 3.64/3.83  cnf(c726,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X495)|iext(X495,uri_rdf_Bag,uri_rdf_Bag),inference(resolution,[status(thm)],[c375, c38])).
% 3.64/3.83  cnf(c977,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X494)|icext(X494,uri_rdf_object),inference(resolution,[status(thm)],[c506, c64])).
% 3.64/3.83  cnf(c959,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X488)|icext(X488,uri_rdf_value),inference(resolution,[status(thm)],[c493, c90])).
% 3.64/3.83  cnf(c364,plain,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c361, c45])).
% 3.64/3.83  cnf(c718,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X487)|iext(X487,uri_rdfs_ContainerMembershipProperty,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c364, c38])).
% 3.64/3.83  cnf(c956,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X486)|icext(X486,uri_rdf_value),inference(resolution,[status(thm)],[c493, c64])).
% 3.64/3.83  cnf(c949,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X485)|icext(X485,uri_rdf_type),inference(resolution,[status(thm)],[c486, c90])).
% 3.64/3.83  cnf(c944,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X484)|icext(X484,uri_rdf_type),inference(resolution,[status(thm)],[c486, c64])).
% 3.64/3.83  cnf(c940,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X482)|icext(X482,uri_rdf_subject),inference(resolution,[status(thm)],[c485, c90])).
% 3.64/3.83  cnf(c937,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X481)|icext(X481,uri_rdf_subject),inference(resolution,[status(thm)],[c485, c64])).
% 3.64/3.83  cnf(c362,plain,iext(uri_rdfs_subClassOf,uri_rdf_Property,uri_rdf_Property),inference(resolution,[status(thm)],[c357, c45])).
% 3.64/3.83  cnf(c710,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X480)|iext(X480,uri_rdf_Property,uri_rdf_Property),inference(resolution,[status(thm)],[c362, c38])).
% 3.64/3.83  cnf(c243,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c236, c45])).
% 3.64/3.83  cnf(c702,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X469)|iext(X469,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c243, c38])).
% 3.64/3.83  cnf(c241,plain,iext(uri_rdfs_subClassOf,skolem0001,skolem0001),inference(resolution,[status(thm)],[c235, c45])).
% 3.64/3.83  cnf(c694,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X458)|iext(X458,skolem0001,skolem0001),inference(resolution,[status(thm)],[c241, c38])).
% 3.64/3.83  cnf(c874,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X452)|icext(X452,uri_rdf__3),inference(resolution,[status(thm)],[c439, c90])).
% 3.64/3.83  cnf(c867,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X450)|icext(X450,uri_rdf__1),inference(resolution,[status(thm)],[c438, c90])).
% 3.64/3.83  cnf(c239,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Container,uri_rdfs_Container),inference(resolution,[status(thm)],[c234, c45])).
% 3.64/3.83  cnf(c686,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X449)|iext(X449,uri_rdfs_Container,uri_rdfs_Container),inference(resolution,[status(thm)],[c239, c38])).
% 3.64/3.83  cnf(c858,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X447)|icext(X447,uri_rdf__2),inference(resolution,[status(thm)],[c437, c90])).
% 3.64/3.83  cnf(c855,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X446)|icext(X446,uri_rdfs_member),inference(resolution,[status(thm)],[c437, c64])).
% 3.64/3.83  cnf(c848,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X443)|icext(X443,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c436, c64])).
% 3.64/3.83  cnf(c237,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Literal,uri_rdfs_Literal),inference(resolution,[status(thm)],[c233, c45])).
% 3.64/3.83  cnf(c678,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X442)|iext(X442,uri_rdfs_Literal,uri_rdfs_Literal),inference(resolution,[status(thm)],[c237, c38])).
% 3.64/3.83  cnf(c844,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X441)|icext(X441,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c430, c90])).
% 3.64/3.83  cnf(c230,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c223, c45])).
% 3.64/3.83  cnf(c670,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X431)|iext(X431,uri_rdfs_Datatype,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c230, c38])).
% 3.64/3.83  cnf(c228,plain,iext(uri_rdfs_subClassOf,uri_ex_d,uri_ex_d),inference(resolution,[status(thm)],[c222, c45])).
% 3.64/3.83  cnf(c662,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X420)|iext(X420,uri_ex_d,uri_ex_d),inference(resolution,[status(thm)],[c228, c38])).
% 3.64/3.83  cnf(c740,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X411)|icext(X411,uri_rdfs_Resource),inference(resolution,[status(thm)],[c403, c64])).
% 3.64/3.83  cnf(c226,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Seq),inference(resolution,[status(thm)],[c221, c45])).
% 3.64/3.83  cnf(c654,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X410)|iext(X410,uri_rdfs_Seq,uri_rdfs_Seq),inference(resolution,[status(thm)],[c226, c38])).
% 3.64/3.83  cnf(c732,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X408)|icext(X408,uri_rdf_Alt),inference(resolution,[status(thm)],[c384, c64])).
% 3.64/3.83  cnf(c724,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X405)|icext(X405,uri_rdf_Bag),inference(resolution,[status(thm)],[c375, c64])).
% 3.64/3.83  cnf(c716,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X403)|icext(X403,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c364, c64])).
% 3.64/3.83  cnf(c224,plain,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c220, c45])).
% 3.64/3.83  cnf(c646,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X402)|iext(X402,uri_rdf_XMLLiteral,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c224, c38])).
% 3.64/3.83  cnf(c711,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X401)|icext(X401,uri_rdf_Property),inference(resolution,[status(thm)],[c362, c90])).
% 3.64/3.83  cnf(c547,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X399)|iext(X399,uri_rdf_first,uri_rdf_Property),inference(resolution,[status(thm)],[c154, c38])).
% 3.64/3.83  cnf(c703,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X398)|icext(X398,uri_rdfs_Class),inference(resolution,[status(thm)],[c243, c90])).
% 3.64/3.83  cnf(c695,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X396)|icext(X396,skolem0001),inference(resolution,[status(thm)],[c241, c90])).
% 3.64/3.83  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.64/3.83  cnf(c153,plain,iext(uri_rdf_type,uri_rdf_nil,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdf_collection_nil_type])).
% 3.64/3.83  cnf(c542,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X395)|iext(X395,uri_rdf_nil,uri_rdf_List),inference(resolution,[status(thm)],[c153, c38])).
% 3.64/3.83  cnf(c687,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X393)|icext(X393,uri_rdfs_Container),inference(resolution,[status(thm)],[c239, c90])).
% 3.64/3.83  cnf(c532,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X391)|iext(X391,uri_rdf_rest,uri_rdf_Property),inference(resolution,[status(thm)],[c152, c38])).
% 3.64/3.83  cnf(c679,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X390)|icext(X390,uri_rdfs_Literal),inference(resolution,[status(thm)],[c237, c90])).
% 3.64/3.83  cnf(c527,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X387)|iext(X387,uri_rdf__1,uri_rdf_Property),inference(resolution,[status(thm)],[c151, c38])).
% 3.64/3.83  cnf(c668,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X386)|icext(X386,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c230, c64])).
% 3.64/3.83  cnf(c516,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X384)|iext(X384,uri_rdf__2,uri_rdf_Property),inference(resolution,[status(thm)],[c150, c38])).
% 3.64/3.83  cnf(c660,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X383)|icext(X383,uri_ex_d),inference(resolution,[status(thm)],[c228, c64])).
% 3.64/3.83  cnf(c652,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X381)|icext(X381,uri_rdfs_Seq),inference(resolution,[status(thm)],[c226, c64])).
% 3.64/3.83  cnf(c511,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X380)|iext(X380,uri_rdf__3,uri_rdf_Property),inference(resolution,[status(thm)],[c149, c38])).
% 3.64/3.83  cnf(c644,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X378)|icext(X378,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c224, c64])).
% 3.64/3.83  cnf(c503,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X376)|iext(X376,uri_rdf_object,uri_rdf_Property),inference(resolution,[status(thm)],[c148, c38])).
% 3.64/3.83  cnf(c541,plain,~iext(uri_rdfs_range,uri_rdf_type,X374)|icext(X374,uri_rdf_List),inference(resolution,[status(thm)],[c153, c64])).
% 3.64/3.83  cnf(c491,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X372)|iext(X372,uri_rdf_value,uri_rdf_Property),inference(resolution,[status(thm)],[c147, c38])).
% 3.64/3.83  cnf(c481,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X367)|iext(X367,uri_rdf_subject,uri_rdf_Property),inference(resolution,[status(thm)],[c146, c38])).
% 3.64/3.83  cnf(c476,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X362)|iext(X362,uri_rdf_type,uri_rdf_Property),inference(resolution,[status(thm)],[c138, c38])).
% 3.64/3.83  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.64/3.83  cnf(c137,plain,iext(uri_rdfs_domain,uri_rdfs_comment,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_comment_domain])).
% 3.64/3.83  cnf(c473,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X357)|iext(X357,uri_rdfs_comment,uri_rdfs_Resource),inference(resolution,[status(thm)],[c137, c38])).
% 3.64/3.83  cnf(c475,plain,~iext(uri_rdfs_range,uri_rdf_type,X354)|icext(X354,uri_rdf_Property),inference(resolution,[status(thm)],[c138, c64])).
% 3.64/3.83  cnf(c470,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X353)|iext(X353,uri_rdfs_comment,uri_rdfs_Literal),inference(resolution,[status(thm)],[c136, c38])).
% 3.64/3.83  cnf(c471,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X350)|icext(X350,uri_rdfs_comment),inference(resolution,[status(thm)],[c137, c90])).
% 3.64/3.83  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.64/3.83  cnf(c135,plain,iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_domain])).
% 3.64/3.83  cnf(c467,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X349)|iext(X349,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(resolution,[status(thm)],[c135, c38])).
% 3.64/3.83  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.64/3.83  cnf(c134,plain,iext(uri_rdfs_range,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_range])).
% 3.64/3.83  cnf(c464,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X347)|iext(X347,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(resolution,[status(thm)],[c134, c38])).
% 3.64/3.83  fof(simple_ir,axiom,(![X]:ir(X)),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', simple_ir)).
% 3.64/3.83  fof(c158,plain,(![X48]:ir(X48)),inference(variable_rename,[status(thm)],[simple_ir])).
% 3.64/3.83  cnf(c159,plain,ir(X52),inference(split_conjunct,[status(thm)],[c158])).
% 3.64/3.83  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.64/3.83  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.64/3.83  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.64/3.83  fof(c76,plain,(![X30]:(![X31]:((~ir(X30)|icext(uri_rdfs_Resource,X30))&(~icext(uri_rdfs_Resource,X31)|ir(X31))))),inference(shift_quantors,[status(thm)],[fof(c75,plain,((![X30]:(~ir(X30)|icext(uri_rdfs_Resource,X30)))&(![X31]:(~icext(uri_rdfs_Resource,X31)|ir(X31)))),inference(variable_rename,[status(thm)],[c74])).])).
% 3.64/3.83  cnf(c77,plain,~ir(X62)|icext(uri_rdfs_Resource,X62),inference(split_conjunct,[status(thm)],[c76])).
% 3.64/3.83  cnf(c166,plain,icext(uri_rdfs_Resource,X65),inference(resolution,[status(thm)],[c77, c159])).
% 3.64/3.83  cnf(c451,plain,iext(uri_rdf_type,X99,uri_rdfs_Resource),inference(resolution,[status(thm)],[c128, c166])).
% 3.64/3.83  cnf(c460,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X345)|iext(X345,X344,uri_rdfs_Resource),inference(resolution,[status(thm)],[c451, c38])).
% 3.64/3.83  cnf(c429,plain,~iext(uri_rdfs_subPropertyOf,X342,uri_rdfs_isDefinedBy)|iext(uri_rdfs_subPropertyOf,X342,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c133, c27])).
% 3.64/3.83  cnf(c465,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X340)|icext(X340,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c135, c90])).
% 3.64/3.83  cnf(c428,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X338)|iext(X338,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c133, c38])).
% 3.64/3.83  cnf(c462,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X337)|icext(X337,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c134, c90])).
% 3.64/3.83  cnf(c459,plain,~iext(uri_rdfs_range,uri_rdf_type,X336)|icext(X336,uri_rdfs_Resource),inference(resolution,[status(thm)],[c451, c64])).
% 3.64/3.83  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.64/3.83  cnf(c132,plain,iext(uri_rdfs_domain,uri_rdfs_label,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_label_domain])).
% 3.64/3.83  cnf(c423,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X335)|iext(X335,uri_rdfs_label,uri_rdfs_Resource),inference(resolution,[status(thm)],[c132, c38])).
% 3.64/3.83  cnf(c425,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X334)|icext(X334,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c133, c64])).
% 3.64/3.83  cnf(c424,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X333)|icext(X333,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c133, c90])).
% 3.64/3.83  cnf(c420,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X332)|iext(X332,uri_rdfs_label,uri_rdfs_Literal),inference(resolution,[status(thm)],[c131, c38])).
% 3.64/3.83  cnf(c421,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X330)|icext(X330,uri_rdfs_label),inference(resolution,[status(thm)],[c132, c90])).
% 3.64/3.83  cnf(c419,plain,~iext(uri_rdfs_range,uri_rdfs_range,X329)|icext(X329,uri_rdfs_Literal),inference(resolution,[status(thm)],[c131, c64])).
% 3.64/3.83  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.64/3.83  cnf(c130,plain,iext(uri_rdfs_domain,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_seealso_domain])).
% 3.64/3.83  cnf(c417,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X328)|iext(X328,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(resolution,[status(thm)],[c130, c38])).
% 3.64/3.83  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.64/3.83  cnf(c129,plain,iext(uri_rdfs_range,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_seealso_range])).
% 3.64/3.83  cnf(c402,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X327)|iext(X327,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(resolution,[status(thm)],[c129, c38])).
% 3.64/3.83  cnf(c399,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X324)|iext(X324,uri_rdf_first,uri_rdf_List),inference(resolution,[status(thm)],[c119, c38])).
% 3.64/3.83  cnf(c415,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X323)|icext(X323,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c130, c90])).
% 3.64/3.83  cnf(c400,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X321)|icext(X321,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c129, c90])).
% 3.64/3.83  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.64/3.83  cnf(c118,plain,iext(uri_rdfs_range,uri_rdf_first,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_collection_first_range])).
% 3.64/3.83  cnf(c396,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X320)|iext(X320,uri_rdf_first,uri_rdfs_Resource),inference(resolution,[status(thm)],[c118, c38])).
% 3.64/3.83  cnf(c397,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X318)|icext(X318,uri_rdf_first),inference(resolution,[status(thm)],[c119, c90])).
% 3.64/3.83  cnf(c393,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X316)|iext(X316,uri_rdf_rest,uri_rdf_List),inference(resolution,[status(thm)],[c117, c38])).
% 3.64/3.83  cnf(c394,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X315)|icext(X315,uri_rdf_first),inference(resolution,[status(thm)],[c118, c90])).
% 3.64/3.83  cnf(c392,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X314)|icext(X314,uri_rdf_List),inference(resolution,[status(thm)],[c117, c64])).
% 3.64/3.83  cnf(c390,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X313)|iext(X313,uri_rdf_rest,uri_rdf_List),inference(resolution,[status(thm)],[c116, c38])).
% 3.64/3.83  cnf(c391,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X312)|icext(X312,uri_rdf_rest),inference(resolution,[status(thm)],[c117, c90])).
% 3.64/3.83  cnf(c382,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X309)|iext(X309,uri_rdf_Alt,uri_rdfs_Container),inference(resolution,[status(thm)],[c115, c38])).
% 3.64/3.83  cnf(c381,plain,~iext(uri_rdfs_subClassOf,X308,uri_rdf_Alt)|iext(uri_rdfs_subClassOf,X308,uri_rdfs_Container),inference(resolution,[status(thm)],[c115, c42])).
% 3.64/3.83  cnf(c373,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X307)|iext(X307,uri_rdf_Bag,uri_rdfs_Container),inference(resolution,[status(thm)],[c114, c38])).
% 3.64/3.83  cnf(c372,plain,~iext(uri_rdfs_subClassOf,X306,uri_rdf_Bag)|iext(uri_rdfs_subClassOf,X306,uri_rdfs_Container),inference(resolution,[status(thm)],[c114, c42])).
% 3.64/3.83  cnf(c360,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X304)|iext(X304,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),inference(resolution,[status(thm)],[c110, c38])).
% 3.64/3.83  cnf(c388,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X303)|icext(X303,uri_rdf_rest),inference(resolution,[status(thm)],[c116, c90])).
% 3.64/3.83  cnf(c377,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X301)|icext(X301,uri_rdf_Alt),inference(resolution,[status(thm)],[c115, c90])).
% 3.64/3.83  cnf(c359,plain,~iext(uri_rdfs_subClassOf,X300,uri_rdfs_ContainerMembershipProperty)|iext(uri_rdfs_subClassOf,X300,uri_rdf_Property),inference(resolution,[status(thm)],[c110, c42])).
% 3.64/3.83  cnf(c368,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X298)|icext(X298,uri_rdf_Bag),inference(resolution,[status(thm)],[c114, c90])).
% 3.64/3.83  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.64/3.83  cnf(c109,plain,iext(uri_rdfs_domain,uri_rdfs_member,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_member_domain])).
% 3.64/3.83  cnf(c354,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X297)|iext(X297,uri_rdfs_member,uri_rdfs_Resource),inference(resolution,[status(thm)],[c109, c38])).
% 3.64/3.83  cnf(c356,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X296)|icext(X296,uri_rdf_Property),inference(resolution,[status(thm)],[c110, c64])).
% 3.64/3.83  cnf(c355,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X295)|icext(X295,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c110, c90])).
% 3.64/3.83  cnf(c352,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X293)|icext(X293,uri_rdfs_member),inference(resolution,[status(thm)],[c109, c90])).
% 3.64/3.83  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.64/3.83  cnf(c23,plain,iext(uri_rdfs_range,uri_rdf_type,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_type_range])).
% 3.64/3.83  cnf(c349,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X292)|icext(X292,uri_rdf_type),inference(resolution,[status(thm)],[c90, c23])).
% 3.64/3.83  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.64/3.83  cnf(c21,plain,iext(uri_rdfs_range,uri_rdf_value,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_value_range])).
% 3.64/3.83  cnf(c348,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X291)|icext(X291,uri_rdf_value),inference(resolution,[status(thm)],[c90, c21])).
% 3.64/3.83  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.64/3.83  cnf(c24,plain,iext(uri_rdfs_domain,uri_rdf_type,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_type_domain])).
% 3.64/3.83  cnf(c347,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X290)|icext(X290,uri_rdf_type),inference(resolution,[status(thm)],[c90, c24])).
% 3.64/3.83  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.64/3.83  cnf(c22,plain,iext(uri_rdfs_domain,uri_rdf_value,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_value_domain])).
% 3.64/3.83  cnf(c345,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X288)|icext(X288,uri_rdf_value),inference(resolution,[status(thm)],[c90, c22])).
% 3.64/3.83  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.64/3.83  cnf(c107,plain,iext(uri_rdfs_domain,uri_rdf__1,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_001])).
% 3.64/3.83  cnf(c344,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X287)|icext(X287,uri_rdf__1),inference(resolution,[status(thm)],[c90, c107])).
% 3.64/3.83  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.64/3.83  cnf(c106,plain,iext(uri_rdfs_domain,uri_rdf__2,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_002])).
% 3.64/3.83  cnf(c343,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X286)|icext(X286,uri_rdf__2),inference(resolution,[status(thm)],[c90, c106])).
% 3.64/3.83  cnf(c342,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X285)|icext(X285,uri_rdfs_domain),inference(resolution,[status(thm)],[c90, c85])).
% 3.64/3.83  cnf(c340,plain,~iext(uri_rdfs_domain,uri_owl_complementOf,X283)|icext(X283,skolem0002),inference(resolution,[status(thm)],[c90, c17])).
% 3.64/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.64/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.64/3.83  cnf(c339,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X282)|icext(X282,uri_rdf_predicate),inference(resolution,[status(thm)],[c90, c57])).
% 3.64/3.83  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.64/3.83  cnf(c103,plain,iext(uri_rdfs_range,uri_rdf__2,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_range_002])).
% 3.64/3.83  cnf(c338,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X281)|icext(X281,uri_rdf__2),inference(resolution,[status(thm)],[c90, c103])).
% 3.64/3.83  cnf(c337,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X280)|icext(X280,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c90, c92])).
% 3.64/3.83  cnf(c16,plain,iext(uri_rdf_rest,skolem0007,uri_rdf_nil),inference(split_conjunct,[status(thm)],[c2])).
% 3.64/3.83  cnf(c336,plain,~iext(uri_rdfs_domain,uri_rdf_rest,X279)|icext(X279,skolem0007),inference(resolution,[status(thm)],[c90, c16])).
% 3.64/3.83  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.64/3.83  cnf(c105,plain,iext(uri_rdfs_domain,uri_rdf__3,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_003])).
% 3.64/3.83  cnf(c335,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X278)|icext(X278,uri_rdf__3),inference(resolution,[status(thm)],[c90, c105])).
% 3.64/3.83  cnf(c334,plain,~iext(uri_rdfs_domain,uri_owl_unionOf,X277)|icext(X277,uri_ex_c),inference(resolution,[status(thm)],[c90, c3])).
% 3.64/3.83  cnf(c15,plain,iext(uri_rdf_first,skolem0007,skolem0002),inference(split_conjunct,[status(thm)],[c2])).
% 3.64/3.83  cnf(c332,plain,~iext(uri_rdfs_domain,uri_rdf_first,X275)|icext(X275,skolem0007),inference(resolution,[status(thm)],[c90, c15])).
% 3.64/3.83  cnf(c13,plain,iext(uri_rdf_first,skolem0006,uri_ex_c),inference(split_conjunct,[status(thm)],[c2])).
% 3.64/3.83  cnf(c331,plain,~iext(uri_rdfs_domain,uri_rdf_first,X274)|icext(X274,skolem0006),inference(resolution,[status(thm)],[c90, c13])).
% 3.64/3.83  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.64/3.83  cnf(c104,plain,iext(uri_rdfs_range,uri_rdf__1,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_range_001])).
% 3.64/3.83  cnf(c330,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X273)|icext(X273,uri_rdf__1),inference(resolution,[status(thm)],[c90, c104])).
% 3.64/3.83  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.64/3.83  cnf(c102,plain,iext(uri_rdfs_range,uri_rdf__3,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_range_003])).
% 3.64/3.83  cnf(c329,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X272)|icext(X272,uri_rdf__3),inference(resolution,[status(thm)],[c90, c102])).
% 3.64/3.83  cnf(c327,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X270)|icext(X270,uri_ex_d),inference(resolution,[status(thm)],[c90, c11])).
% 3.64/3.83  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.64/3.83  cnf(c46,plain,iext(uri_rdfs_range,uri_rdfs_subClassOf,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_subclassof_range])).
% 3.64/3.83  cnf(c326,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X269)|icext(X269,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c90, c46])).
% 3.64/3.83  cnf(c325,plain,~iext(uri_rdfs_domain,uri_rdf_rest,X268)|icext(X268,skolem0004),inference(resolution,[status(thm)],[c90, c7])).
% 3.64/3.83  cnf(c324,plain,~iext(uri_rdfs_domain,uri_rdf_rest,X267)|icext(X267,skolem0003),inference(resolution,[status(thm)],[c90, c5])).
% 3.64/3.83  cnf(c322,plain,~iext(uri_rdfs_domain,uri_owl_intersectionOf,X265)|icext(X265,skolem0001),inference(resolution,[status(thm)],[c90, c12])).
% 3.64/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.64/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.64/3.83  cnf(c320,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X263)|icext(X263,uri_rdf_subject),inference(resolution,[status(thm)],[c90, c56])).
% 3.64/3.83  cnf(c319,plain,~iext(uri_rdfs_domain,uri_owl_disjointWith,X262)|icext(X262,uri_ex_d),inference(resolution,[status(thm)],[c90, c10])).
% 3.64/3.83  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.64/3.83  cnf(c39,plain,iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_subpropertyof_domain])).
% 3.64/3.83  cnf(c318,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X261)|icext(X261,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c90, c39])).
% 3.64/3.83  cnf(c6,plain,iext(uri_rdf_first,skolem0004,uri_ex_c2),inference(split_conjunct,[status(thm)],[c2])).
% 3.64/3.83  cnf(c317,plain,~iext(uri_rdfs_domain,uri_rdf_first,X260)|icext(X260,skolem0004),inference(resolution,[status(thm)],[c90, c6])).
% 3.64/3.83  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.64/3.83  cnf(c55,plain,iext(uri_rdfs_range,uri_rdf_subject,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_reification_subject_range])).
% 3.64/3.83  cnf(c316,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X259)|icext(X259,uri_rdf_subject),inference(resolution,[status(thm)],[c90, c55])).
% 3.64/3.83  cnf(c9,plain,iext(uri_rdf_rest,skolem0005,uri_rdf_nil),inference(split_conjunct,[status(thm)],[c2])).
% 3.64/3.83  cnf(c315,plain,~iext(uri_rdfs_domain,uri_rdf_rest,X258)|icext(X258,skolem0005),inference(resolution,[status(thm)],[c90, c9])).
% 3.64/3.83  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.64/3.83  cnf(c60,plain,iext(uri_rdfs_domain,uri_rdf_object,uri_rdfs_Statement),inference(split_conjunct,[status(thm)],[rdfs_reification_object_domain])).
% 3.64/3.83  cnf(c314,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X257)|icext(X257,uri_rdf_object),inference(resolution,[status(thm)],[c90, c60])).
% 3.64/3.83  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.64/3.83  cnf(c54,plain,iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_subclassof_domain])).
% 3.64/3.83  cnf(c312,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X255)|icext(X255,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c90, c54])).
% 3.64/3.83  cnf(c8,plain,iext(uri_rdf_first,skolem0005,uri_ex_c3),inference(split_conjunct,[status(thm)],[c2])).
% 3.64/3.83  cnf(c311,plain,~iext(uri_rdfs_domain,uri_rdf_first,X254)|icext(X254,skolem0005),inference(resolution,[status(thm)],[c90, c8])).
% 3.64/3.83  cnf(c310,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X253)|icext(X253,uri_rdfs_Seq),inference(resolution,[status(thm)],[c90, c98])).
% 3.64/3.83  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.64/3.83  cnf(c31,plain,iext(uri_rdfs_range,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_subpropertyof_range])).
% 3.64/3.83  cnf(c308,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X251)|icext(X251,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c90, c31])).
% 3.64/3.83  cnf(c307,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X250)|icext(X250,uri_rdfs_range),inference(resolution,[status(thm)],[c90, c65])).
% 3.64/3.83  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.64/3.83  cnf(c108,plain,iext(uri_rdfs_range,uri_rdfs_member,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_member_range])).
% 3.64/3.83  cnf(c306,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X249)|icext(X249,uri_rdfs_member),inference(resolution,[status(thm)],[c90, c108])).
% 3.64/3.83  cnf(c305,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X248)|icext(X248,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c90, c97])).
% 3.64/3.83  cnf(c304,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X247)|icext(X247,uri_rdfs_range),inference(resolution,[status(thm)],[c90, c61])).
% 3.64/3.83  cnf(c302,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X245)|icext(X245,uri_rdfs_domain),inference(factor,[status(thm)],[c90])).
% 3.64/3.83  cnf(c458,plain,~iext(uri_rdfs_domain,uri_rdf_type,X241)|icext(X241,X240),inference(resolution,[status(thm)],[c451, c90])).
% 3.64/3.83  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.64/3.83  cnf(c96,plain,iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Datatype),inference(split_conjunct,[status(thm)],[rdfs_dat_xmlliteral_type])).
% 3.64/3.83  cnf(c296,plain,~iext(uri_rdfs_range,uri_rdf_type,X232)|icext(X232,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c64, c96])).
% 3.64/3.83  cnf(c53,plain,~iext(uri_rdfs_subClassOf,X83,X82)|~icext(X83,X81)|icext(X82,X81),inference(split_conjunct,[status(thm)],[c50])).
% 3.64/3.83  cnf(c380,plain,~icext(uri_rdf_Alt,X206)|icext(uri_rdfs_Container,X206),inference(resolution,[status(thm)],[c115, c53])).
% 3.64/3.83  cnf(c371,plain,~icext(uri_rdf_Bag,X205)|icext(uri_rdfs_Container,X205),inference(resolution,[status(thm)],[c114, c53])).
% 3.64/3.83  cnf(c358,plain,~icext(uri_rdfs_ContainerMembershipProperty,X203)|icext(uri_rdf_Property,X203),inference(resolution,[status(thm)],[c110, c53])).
% 3.64/3.83  cnf(c290,plain,~iext(uri_rdfs_range,uri_owl_complementOf,X202)|icext(X202,uri_ex_c2),inference(resolution,[status(thm)],[c64, c17])).
% 3.64/3.83  cnf(c287,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X199)|icext(X199,uri_rdfs_Class),inference(resolution,[status(thm)],[c64, c92])).
% 3.64/3.83  cnf(c285,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X197)|icext(X197,uri_rdfs_Resource),inference(resolution,[status(thm)],[c64, c105])).
% 3.64/3.83  cnf(c284,plain,~iext(uri_rdfs_range,uri_owl_unionOf,X196)|icext(X196,skolem0003),inference(resolution,[status(thm)],[c64, c3])).
% 3.64/3.83  cnf(c282,plain,~iext(uri_rdfs_range,uri_rdf_first,X194)|icext(X194,skolem0002),inference(resolution,[status(thm)],[c64, c15])).
% 3.64/3.83  cnf(c281,plain,~iext(uri_rdfs_range,uri_rdf_first,X193)|icext(X193,uri_ex_c),inference(resolution,[status(thm)],[c64, c13])).
% 3.64/3.83  cnf(c277,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X189)|icext(X189,skolem0001),inference(resolution,[status(thm)],[c64, c11])).
% 3.64/3.83  cnf(c272,plain,~iext(uri_rdfs_range,uri_owl_intersectionOf,X184)|icext(X184,skolem0006),inference(resolution,[status(thm)],[c64, c12])).
% 3.64/3.83  cnf(c1209,plain,icext(uri_rdf_Property,uri_rdfs_member),inference(resolution,[status(thm)],[c862, c127])).
% 3.64/3.83  cnf(c271,plain,~iext(uri_rdfs_range,uri_rdf_type,X183)|icext(X183,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c64, c100])).
% 3.64/3.83  cnf(c269,plain,~iext(uri_rdfs_range,uri_owl_disjointWith,X181)|icext(X181,uri_ex_c1),inference(resolution,[status(thm)],[c64, c10])).
% 3.64/3.83  cnf(c1181,plain,icext(uri_rdf_Property,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c642, c127])).
% 3.64/3.83  cnf(c267,plain,~iext(uri_rdfs_range,uri_rdf_first,X179)|icext(X179,uri_ex_c2),inference(resolution,[status(thm)],[c64, c6])).
% 3.64/3.83  cnf(c1165,plain,icext(uri_rdf_Property,uri_owl_complementOf),inference(resolution,[status(thm)],[c640, c127])).
% 3.64/3.83  cnf(c265,plain,~iext(uri_rdfs_range,uri_rdf_rest,X177)|icext(X177,uri_rdf_nil),inference(resolution,[status(thm)],[c64, c9])).
% 3.64/3.83  cnf(c1149,plain,icext(uri_rdf_Property,uri_owl_unionOf),inference(resolution,[status(thm)],[c638, c127])).
% 3.64/3.83  cnf(c263,plain,~iext(uri_rdfs_range,uri_rdf_first,X175)|icext(X175,uri_ex_c1),inference(resolution,[status(thm)],[c64, c4])).
% 3.64/3.83  cnf(c1132,plain,icext(uri_rdf_Property,uri_owl_intersectionOf),inference(resolution,[status(thm)],[c636, c127])).
% 3.64/3.83  cnf(c262,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X174)|icext(X174,uri_rdfs_Class),inference(resolution,[status(thm)],[c64, c54])).
% 3.64/3.83  cnf(c261,plain,~iext(uri_rdfs_range,uri_rdf_first,X173)|icext(X173,uri_ex_c3),inference(resolution,[status(thm)],[c64, c8])).
% 3.64/3.83  cnf(c1115,plain,icext(uri_rdf_Property,uri_owl_disjointWith),inference(resolution,[status(thm)],[c634, c127])).
% 3.64/3.83  cnf(c260,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X172)|icext(X172,uri_rdfs_Container),inference(resolution,[status(thm)],[c64, c98])).
% 3.64/3.83  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.64/3.83  cnf(c66,plain,iext(uri_rdf_type,uri_rdf_Property,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_property_type])).
% 3.64/3.83  cnf(c259,plain,~iext(uri_rdfs_range,uri_rdf_type,X171)|icext(X171,uri_rdfs_Class),inference(resolution,[status(thm)],[c64, c66])).
% 3.64/3.83  cnf(c1095,plain,icext(uri_rdf_Property,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c632, c127])).
% 3.64/3.83  cnf(c258,plain,~iext(uri_rdfs_range,uri_rdfs_range,X170)|icext(X170,uri_rdf_Property),inference(resolution,[status(thm)],[c64, c31])).
% 3.64/3.83  cnf(c257,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X169)|icext(X169,uri_rdf_Property),inference(resolution,[status(thm)],[c64, c65])).
% 3.64/3.83  cnf(c1067,plain,icext(uri_rdf_Property,uri_rdfs_range),inference(resolution,[status(thm)],[c630, c127])).
% 3.64/3.83  cnf(c256,plain,~iext(uri_rdfs_range,uri_rdfs_range,X168)|icext(X168,uri_rdfs_Resource),inference(resolution,[status(thm)],[c64, c108])).
% 3.64/3.83  cnf(c255,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X167)|icext(X167,uri_rdfs_Literal),inference(resolution,[status(thm)],[c64, c97])).
% 3.64/3.83  cnf(c1039,plain,icext(uri_rdf_Property,uri_rdfs_domain),inference(resolution,[status(thm)],[c628, c127])).
% 3.64/3.83  cnf(c254,plain,~iext(uri_rdfs_range,uri_rdfs_range,X166)|icext(X166,uri_rdfs_Class),inference(resolution,[status(thm)],[c64, c61])).
% 3.64/3.83  cnf(c252,plain,~iext(uri_rdfs_range,uri_rdfs_range,X164)|icext(X164,X164),inference(factor,[status(thm)],[c64])).
% 3.64/3.83  cnf(c248,plain,~icext(uri_rdfs_Datatype,X163)|icext(uri_rdfs_Class,X163),inference(resolution,[status(thm)],[c53, c92])).
% 3.64/3.83  cnf(c247,plain,~icext(uri_ex_d,X162)|icext(skolem0001,X162),inference(resolution,[status(thm)],[c53, c11])).
% 3.64/3.83  cnf(c246,plain,~icext(uri_rdfs_Seq,X161)|icext(uri_rdfs_Container,X161),inference(resolution,[status(thm)],[c53, c98])).
% 3.64/3.83  cnf(c245,plain,~icext(uri_rdf_XMLLiteral,X160)|icext(uri_rdfs_Literal,X160),inference(resolution,[status(thm)],[c53, c97])).
% 3.64/3.83  cnf(c219,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X159)|iext(X159,uri_rdfs_member,uri_rdfs_Resource),inference(resolution,[status(thm)],[c108, c38])).
% 3.64/3.83  cnf(c218,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X158)|iext(X158,uri_rdf__1,uri_rdfs_Resource),inference(resolution,[status(thm)],[c107, c38])).
% 3.64/3.83  cnf(c217,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X157)|iext(X157,uri_rdf__2,uri_rdfs_Resource),inference(resolution,[status(thm)],[c106, c38])).
% 3.64/3.83  cnf(c972,plain,icext(uri_rdf_Property,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c496, c127])).
% 3.64/3.83  cnf(c216,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X156)|iext(X156,uri_rdf__3,uri_rdfs_Resource),inference(resolution,[status(thm)],[c105, c38])).
% 3.64/3.83  cnf(c965,plain,icext(uri_rdf_Property,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c494, c127])).
% 3.64/3.83  cnf(c215,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X155)|iext(X155,uri_rdf__1,uri_rdfs_Resource),inference(resolution,[status(thm)],[c104, c38])).
% 3.64/3.83  cnf(c214,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X154)|iext(X154,uri_rdf__2,uri_rdfs_Resource),inference(resolution,[status(thm)],[c103, c38])).
% 3.64/3.83  cnf(c213,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X153)|iext(X153,uri_rdf__3,uri_rdfs_Resource),inference(resolution,[status(thm)],[c102, c38])).
% 3.64/3.83  cnf(c212,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X152)|iext(X152,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c101, c38])).
% 3.64/3.83  cnf(c211,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X151)|iext(X151,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c100, c38])).
% 3.64/3.83  cnf(c210,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X150)|iext(X150,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c99, c38])).
% 3.64/3.83  cnf(c209,plain,~iext(uri_rdfs_subClassOf,X149,uri_rdfs_Datatype)|iext(uri_rdfs_subClassOf,X149,uri_rdfs_Class),inference(resolution,[status(thm)],[c42, c92])).
% 3.64/3.83  cnf(c208,plain,~iext(uri_rdfs_subClassOf,X148,uri_ex_d)|iext(uri_rdfs_subClassOf,X148,skolem0001),inference(resolution,[status(thm)],[c42, c11])).
% 3.64/3.83  cnf(c207,plain,~iext(uri_rdfs_subClassOf,X147,uri_rdfs_Seq)|iext(uri_rdfs_subClassOf,X147,uri_rdfs_Container),inference(resolution,[status(thm)],[c42, c98])).
% 3.64/3.83  cnf(c206,plain,~iext(uri_rdfs_subClassOf,X146,uri_rdf_XMLLiteral)|iext(uri_rdfs_subClassOf,X146,uri_rdfs_Literal),inference(resolution,[status(thm)],[c42, c97])).
% 3.64/3.83  cnf(c204,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X144)|iext(X144,uri_rdfs_Seq,uri_rdfs_Container),inference(resolution,[status(thm)],[c98, c38])).
% 3.64/3.83  cnf(c203,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X143)|iext(X143,uri_rdf_XMLLiteral,uri_rdfs_Literal),inference(resolution,[status(thm)],[c97, c38])).
% 3.64/3.83  cnf(c202,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X142)|iext(X142,uri_rdf_XMLLiteral,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c96, c38])).
% 3.64/3.83  cnf(c201,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X141)|iext(X141,uri_rdfs_Datatype,uri_rdfs_Class),inference(resolution,[status(thm)],[c92, c38])).
% 3.64/3.83  cnf(c200,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X140)|iext(X140,uri_rdfs_domain,uri_rdf_Property),inference(resolution,[status(thm)],[c91, c38])).
% 3.64/3.83  cnf(c199,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X139)|iext(X139,uri_rdf_type,uri_rdfs_Class),inference(resolution,[status(thm)],[c38, c23])).
% 3.64/3.83  cnf(c198,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X138)|iext(X138,uri_rdf_value,uri_rdfs_Resource),inference(resolution,[status(thm)],[c38, c21])).
% 3.64/3.83  cnf(c197,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X137)|iext(X137,uri_rdf_type,uri_rdfs_Resource),inference(resolution,[status(thm)],[c38, c24])).
% 3.64/3.83  cnf(c196,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X136)|iext(X136,uri_rdf_value,uri_rdfs_Resource),inference(resolution,[status(thm)],[c38, c22])).
% 3.64/3.83  cnf(c195,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X135)|iext(X135,uri_rdfs_domain,uri_rdfs_Class),inference(resolution,[status(thm)],[c38, c85])).
% 3.64/3.83  cnf(c194,plain,~iext(uri_rdfs_subPropertyOf,uri_owl_complementOf,X134)|iext(X134,skolem0002,uri_ex_c2),inference(resolution,[status(thm)],[c38, c17])).
% 3.64/3.83  cnf(c193,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X133)|iext(X133,uri_rdf_predicate,uri_rdfs_Resource),inference(resolution,[status(thm)],[c38, c57])).
% 3.64/3.83  cnf(c192,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X132)|iext(X132,skolem0007,uri_rdf_nil),inference(resolution,[status(thm)],[c38, c16])).
% 3.64/3.83  cnf(c191,plain,~iext(uri_rdfs_subPropertyOf,uri_owl_unionOf,X131)|iext(X131,uri_ex_c,skolem0003),inference(resolution,[status(thm)],[c38, c3])).
% 3.64/3.83  cnf(c190,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_first,X130)|iext(X130,skolem0007,skolem0002),inference(resolution,[status(thm)],[c38, c15])).
% 3.64/3.83  cnf(c189,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_first,X129)|iext(X129,skolem0006,uri_ex_c),inference(resolution,[status(thm)],[c38, c13])).
% 3.64/3.83  cnf(c188,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X128)|iext(X128,skolem0006,skolem0007),inference(resolution,[status(thm)],[c38, c14])).
% 3.64/3.83  cnf(c187,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X127)|iext(X127,uri_ex_d,skolem0001),inference(resolution,[status(thm)],[c38, c11])).
% 3.64/3.83  cnf(c186,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X126)|iext(X126,uri_rdfs_subClassOf,uri_rdfs_Class),inference(resolution,[status(thm)],[c38, c46])).
% 3.64/3.83  cnf(c185,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X125)|iext(X125,skolem0004,skolem0005),inference(resolution,[status(thm)],[c38, c7])).
% 3.64/3.83  cnf(c184,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X124)|iext(X124,skolem0003,skolem0004),inference(resolution,[status(thm)],[c38, c5])).
% 3.64/3.83  cnf(c183,plain,~iext(uri_rdfs_subPropertyOf,uri_owl_intersectionOf,X123)|iext(X123,skolem0001,skolem0006),inference(resolution,[status(thm)],[c38, c12])).
% 3.64/3.83  cnf(c182,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X122)|iext(X122,uri_rdf_subject,uri_rdfs_Statement),inference(resolution,[status(thm)],[c38, c56])).
% 3.64/3.83  cnf(c181,plain,~iext(uri_rdfs_subPropertyOf,uri_owl_disjointWith,X121)|iext(X121,uri_ex_d,uri_ex_c1),inference(resolution,[status(thm)],[c38, c10])).
% 3.64/3.83  cnf(c180,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X120)|iext(X120,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c38, c39])).
% 3.64/3.83  cnf(c179,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_first,X119)|iext(X119,skolem0004,uri_ex_c2),inference(resolution,[status(thm)],[c38, c6])).
% 3.64/3.83  cnf(c178,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X118)|iext(X118,uri_rdf_subject,uri_rdfs_Resource),inference(resolution,[status(thm)],[c38, c55])).
% 3.64/3.83  cnf(c177,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X117)|iext(X117,skolem0005,uri_rdf_nil),inference(resolution,[status(thm)],[c38, c9])).
% 3.64/3.83  cnf(c176,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X116)|iext(X116,uri_rdf_object,uri_rdfs_Statement),inference(resolution,[status(thm)],[c38, c60])).
% 3.64/3.83  cnf(c175,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_first,X115)|iext(X115,skolem0003,uri_ex_c1),inference(resolution,[status(thm)],[c38, c4])).
% 3.64/3.83  cnf(c174,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X114)|iext(X114,uri_rdfs_subClassOf,uri_rdfs_Class),inference(resolution,[status(thm)],[c38, c54])).
% 3.64/3.83  cnf(c173,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_first,X113)|iext(X113,skolem0005,uri_ex_c3),inference(resolution,[status(thm)],[c38, c8])).
% 3.64/3.83  cnf(c172,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X112)|iext(X112,uri_rdf_Property,uri_rdfs_Class),inference(resolution,[status(thm)],[c38, c66])).
% 3.64/3.83  cnf(c171,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X111)|iext(X111,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c38, c31])).
% 3.64/3.83  cnf(c170,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X110)|iext(X110,uri_rdfs_range,uri_rdf_Property),inference(resolution,[status(thm)],[c38, c65])).
% 3.64/3.83  cnf(c169,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X109)|iext(X109,uri_rdfs_range,uri_rdfs_Class),inference(resolution,[status(thm)],[c38, c61])).
% 3.64/3.83  cnf(c168,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X108)|iext(X108,uri_rdf_predicate,uri_rdfs_Statement),inference(resolution,[status(thm)],[c38, c58])).
% 3.64/3.83  cnf(c167,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X107)|iext(X107,uri_rdfs_subPropertyOf,X107),inference(factor,[status(thm)],[c38])).
% 3.64/3.83  cnf(c548,plain,icext(uri_rdf_Property,uri_rdf_first),inference(resolution,[status(thm)],[c154, c127])).
% 3.64/3.83  cnf(c543,plain,icext(uri_rdf_List,uri_rdf_nil),inference(resolution,[status(thm)],[c153, c127])).
% 3.64/3.83  cnf(c533,plain,icext(uri_rdf_Property,uri_rdf_rest),inference(resolution,[status(thm)],[c152, c127])).
% 3.64/3.83  cnf(c528,plain,icext(uri_rdf_Property,uri_rdf__1),inference(resolution,[status(thm)],[c151, c127])).
% 3.64/3.83  cnf(c517,plain,icext(uri_rdf_Property,uri_rdf__2),inference(resolution,[status(thm)],[c150, c127])).
% 3.64/3.83  cnf(c512,plain,icext(uri_rdf_Property,uri_rdf__3),inference(resolution,[status(thm)],[c149, c127])).
% 3.64/3.83  cnf(c504,plain,icext(uri_rdf_Property,uri_rdf_object),inference(resolution,[status(thm)],[c148, c127])).
% 3.64/3.83  cnf(c492,plain,icext(uri_rdf_Property,uri_rdf_value),inference(resolution,[status(thm)],[c147, c127])).
% 3.64/3.83  cnf(c482,plain,icext(uri_rdf_Property,uri_rdf_subject),inference(resolution,[status(thm)],[c146, c127])).
% 3.64/3.83  cnf(c477,plain,icext(uri_rdf_Property,uri_rdf_type),inference(resolution,[status(thm)],[c138, c127])).
% 3.64/3.83  cnf(c435,plain,icext(uri_rdfs_Datatype,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c127, c96])).
% 3.64/3.83  cnf(c363,plain,icext(uri_rdfs_Class,uri_rdf_Property),inference(resolution,[status(thm)],[c357, c83])).
% 3.64/3.83  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.64/3.83  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.64/3.83  fof(c94,plain,(![X38]:(~icext(uri_rdfs_Datatype,X38)|iext(uri_rdfs_subClassOf,X38,uri_rdfs_Literal))),inference(variable_rename,[status(thm)],[c93])).
% 3.64/3.83  cnf(c95,plain,~icext(uri_rdfs_Datatype,X92)|iext(uri_rdfs_subClassOf,X92,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[c94])).
% 3.64/3.83  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.64/3.83  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.64/3.83  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.64/3.83  fof(c70,plain,(![X28]:(![X29]:((~lv(X28)|icext(uri_rdfs_Literal,X28))&(~icext(uri_rdfs_Literal,X29)|lv(X29))))),inference(shift_quantors,[status(thm)],[fof(c69,plain,((![X28]:(~lv(X28)|icext(uri_rdfs_Literal,X28)))&(![X29]:(~icext(uri_rdfs_Literal,X29)|lv(X29)))),inference(variable_rename,[status(thm)],[c68])).])).
% 3.64/3.83  cnf(c72,plain,~icext(uri_rdfs_Literal,X61)|lv(X61),inference(split_conjunct,[status(thm)],[c70])).
% 3.64/3.83  cnf(c71,plain,~lv(X60)|icext(uri_rdfs_Literal,X60),inference(split_conjunct,[status(thm)],[c70])).
% 3.64/3.83  fof(testcase_conclusion_fullish_020_Logical_Complications,conjecture,iext(uri_rdfs_subClassOf,uri_ex_d,uri_ex_c3),file('/export/starexec/sandbox/benchmark/theBenchmark.p', testcase_conclusion_fullish_020_Logical_Complications)).
% 3.64/3.83  fof(c18,negated_conjecture,(~iext(uri_rdfs_subClassOf,uri_ex_d,uri_ex_c3)),inference(assume_negation,[status(cth)],[testcase_conclusion_fullish_020_Logical_Complications])).
% 3.64/3.83  fof(c19,negated_conjecture,~iext(uri_rdfs_subClassOf,uri_ex_d,uri_ex_c3),inference(fof_simplification,[status(thm)],[c18])).
% 3.64/3.83  cnf(c20,negated_conjecture,~iext(uri_rdfs_subClassOf,uri_ex_d,uri_ex_c3),inference(split_conjunct,[status(thm)],[c19])).
% 3.64/3.83  % SZS output end Saturation
% 3.64/3.83  
% 3.64/3.83  % Initial clauses    : 105
% 3.64/3.83  % Processed clauses  : 631
% 3.64/3.83  % Factors computed   : 5
% 3.64/3.83  % Resolvents computed: 1459
% 3.64/3.83  % Tautologies deleted: 55
% 3.64/3.83  % Forward subsumed   : 883
% 3.64/3.83  % Backward subsumed  : 1
% 3.64/3.83  % -------- CPU Time ---------
% 3.64/3.83  % User time          : 3.456 s
% 3.64/3.83  % System time        : 0.018 s
% 3.64/3.83  % Total time         : 3.475 s
%------------------------------------------------------------------------------