PyRes---1.5.CSA-Sat.s

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

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

% Result   : CounterSatisfiable 3.54s 3.70s
% Output   : Saturation 3.54s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12  % Problem  : SWB024+4 : TPTP v8.1.2. Released v5.2.0.
% 0.06/0.13  % Command  : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.34  % Computer : n020.cluster.edu
% 0.12/0.34  % Model    : x86_64 x86_64
% 0.12/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34  % Memory   : 8042.1875MB
% 0.12/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34  % CPULimit : 300
% 0.12/0.34  % WCLimit  : 300
% 0.12/0.34  % DateTime : Wed May  8 22:13:23 EDT 2024
% 0.12/0.34  % CPUTime  : 
% 3.54/3.70  % Version:  1.5
% 3.54/3.70  % SZS status CounterSatisfiable
% 3.54/3.70  % SZS output start Saturation
% 3.54/3.70  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.54/3.70  fof(c26,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.54/3.70  fof(c28,plain,(![X8]:(![X9]:(![X10]:(![X11]:(~iext(uri_rdfs_subPropertyOf,X8,X9)|((ip(X8)&ip(X9))&(~iext(X8,X10,X11)|iext(X9,X10,X11)))))))),inference(shift_quantors,[status(thm)],[fof(c27,plain,(![X8]:(![X9]:(~iext(uri_rdfs_subPropertyOf,X8,X9)|((ip(X8)&ip(X9))&(![X10]:(![X11]:(~iext(X8,X10,X11)|iext(X9,X10,X11)))))))),inference(variable_rename,[status(thm)],[c26])).])).
% 3.54/3.70  fof(c29,plain,(![X8]:(![X9]:(![X10]:(![X11]:(((~iext(uri_rdfs_subPropertyOf,X8,X9)|ip(X8))&(~iext(uri_rdfs_subPropertyOf,X8,X9)|ip(X9)))&(~iext(uri_rdfs_subPropertyOf,X8,X9)|(~iext(X8,X10,X11)|iext(X9,X10,X11)))))))),inference(distribute,[status(thm)],[c28])).
% 3.54/3.70  cnf(c32,plain,~iext(uri_rdfs_subPropertyOf,X68,X66)|~iext(X68,X65,X67)|iext(X66,X65,X67),inference(split_conjunct,[status(thm)],[c29])).
% 3.54/3.70  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.54/3.70  fof(c22,plain,(![P]:(~ip(P)|iext(uri_rdfs_subPropertyOf,P,P))),inference(fof_nnf,[status(thm)],[rdfs_subpropertyof_reflex])).
% 3.54/3.70  fof(c23,plain,(![X7]:(~ip(X7)|iext(uri_rdfs_subPropertyOf,X7,X7))),inference(variable_rename,[status(thm)],[c22])).
% 3.54/3.70  cnf(c24,plain,~ip(X53)|iext(uri_rdfs_subPropertyOf,X53,X53),inference(split_conjunct,[status(thm)],[c23])).
% 3.54/3.70  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.54/3.70  fof(c134,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.54/3.70  fof(c135,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)],[c134])).
% 3.54/3.70  fof(c137,plain,(![X40]:(![X41]:((~iext(uri_rdf_type,X40,uri_rdf_Property)|ip(X40))&(~ip(X41)|iext(uri_rdf_type,X41,uri_rdf_Property))))),inference(shift_quantors,[status(thm)],[fof(c136,plain,((![X40]:(~iext(uri_rdf_type,X40,uri_rdf_Property)|ip(X40)))&(![X41]:(~ip(X41)|iext(uri_rdf_type,X41,uri_rdf_Property)))),inference(variable_rename,[status(thm)],[c135])).])).
% 3.54/3.70  cnf(c138,plain,~iext(uri_rdf_type,X97,uri_rdf_Property)|ip(X97),inference(split_conjunct,[status(thm)],[c137])).
% 3.54/3.70  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.54/3.70  fof(c117,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.54/3.70  fof(c118,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)],[c117])).
% 3.54/3.70  fof(c120,plain,(![X36]:(![X37]:(![X38]:(![X39]:((~iext(uri_rdf_type,X36,X37)|icext(X37,X36))&(~icext(X39,X38)|iext(uri_rdf_type,X38,X39))))))),inference(shift_quantors,[status(thm)],[fof(c119,plain,((![X36]:(![X37]:(~iext(uri_rdf_type,X36,X37)|icext(X37,X36))))&(![X38]:(![X39]:(~icext(X39,X38)|iext(uri_rdf_type,X38,X39))))),inference(variable_rename,[status(thm)],[c118])).])).
% 3.54/3.70  cnf(c122,plain,~icext(X93,X94)|iext(uri_rdf_type,X94,X93),inference(split_conjunct,[status(thm)],[c120])).
% 3.54/3.70  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.54/3.70  cnf(c59,plain,iext(uri_rdfs_domain,uri_rdfs_range,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_range_domain])).
% 3.54/3.70  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.54/3.70  fof(c80,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.54/3.70  fof(c81,plain,(![P]:(![C]:(![X]:((~iext(uri_rdfs_domain,P,C)|(![Y]:~iext(P,X,Y)))|icext(C,X))))),inference(shift_quantors,[status(thm)],[c80])).
% 3.54/3.70  fof(c83,plain,(![X29]:(![X30]:(![X31]:(![X32]:((~iext(uri_rdfs_domain,X29,X30)|~iext(X29,X31,X32))|icext(X30,X31)))))),inference(shift_quantors,[status(thm)],[fof(c82,plain,(![X29]:(![X30]:(![X31]:((~iext(uri_rdfs_domain,X29,X30)|(![X32]:~iext(X29,X31,X32)))|icext(X30,X31))))),inference(variable_rename,[status(thm)],[c81])).])).
% 3.54/3.70  cnf(c84,plain,~iext(uri_rdfs_domain,X87,X86)|~iext(X87,X84,X85)|icext(X86,X84),inference(split_conjunct,[status(thm)],[c83])).
% 3.54/3.70  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.54/3.70  cnf(c130,plain,iext(uri_rdfs_range,uri_rdfs_comment,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[rdfs_annotation_comment_range])).
% 3.54/3.70  cnf(c451,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X325)|icext(X325,uri_rdfs_comment),inference(resolution,[status(thm)],[c130, c84])).
% 3.54/3.70  cnf(c1393,plain,icext(uri_rdf_Property,uri_rdfs_comment),inference(resolution,[status(thm)],[c451, c59])).
% 3.54/3.70  cnf(c1394,plain,iext(uri_rdf_type,uri_rdfs_comment,uri_rdf_Property),inference(resolution,[status(thm)],[c1393, c122])).
% 3.54/3.70  cnf(c1400,plain,ip(uri_rdfs_comment),inference(resolution,[status(thm)],[c1394, c138])).
% 3.54/3.70  cnf(c1403,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_comment,uri_rdfs_comment),inference(resolution,[status(thm)],[c1400, c24])).
% 3.54/3.70  cnf(c1405,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X686)|iext(X686,uri_rdfs_comment,uri_rdfs_comment),inference(resolution,[status(thm)],[c1403, c32])).
% 3.54/3.70  cnf(c1397,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X685)|iext(X685,uri_rdfs_comment,uri_rdf_Property),inference(resolution,[status(thm)],[c1394, c32])).
% 3.54/3.70  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.54/3.70  cnf(c125,plain,iext(uri_rdfs_range,uri_rdfs_label,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[rdfs_annotation_label_range])).
% 3.54/3.70  cnf(c393,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X307)|icext(X307,uri_rdfs_label),inference(resolution,[status(thm)],[c125, c84])).
% 3.54/3.70  cnf(c1364,plain,icext(uri_rdf_Property,uri_rdfs_label),inference(resolution,[status(thm)],[c393, c59])).
% 3.54/3.70  cnf(c1365,plain,iext(uri_rdf_type,uri_rdfs_label,uri_rdf_Property),inference(resolution,[status(thm)],[c1364, c122])).
% 3.54/3.70  cnf(c1370,plain,ip(uri_rdfs_label),inference(resolution,[status(thm)],[c1365, c138])).
% 3.54/3.70  cnf(c1374,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_label,uri_rdfs_label),inference(resolution,[status(thm)],[c1370, c24])).
% 3.54/3.70  cnf(c1375,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X683)|iext(X683,uri_rdfs_label,uri_rdfs_label),inference(resolution,[status(thm)],[c1374, c32])).
% 3.54/3.70  cnf(c1367,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X682)|iext(X682,uri_rdfs_label,uri_rdf_Property),inference(resolution,[status(thm)],[c1365, c32])).
% 3.54/3.70  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.54/3.70  cnf(c85,plain,iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_domain_domain])).
% 3.54/3.70  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.54/3.70  cnf(c52,plain,iext(uri_rdfs_domain,uri_rdf_predicate,uri_rdfs_Statement),inference(split_conjunct,[status(thm)],[rdfs_reification_predicate_domain])).
% 3.54/3.70  cnf(c317,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X253)|icext(X253,uri_rdf_predicate),inference(resolution,[status(thm)],[c84, c52])).
% 3.54/3.70  cnf(c1310,plain,icext(uri_rdf_Property,uri_rdf_predicate),inference(resolution,[status(thm)],[c317, c85])).
% 3.54/3.70  cnf(c1311,plain,iext(uri_rdf_type,uri_rdf_predicate,uri_rdf_Property),inference(resolution,[status(thm)],[c1310, c122])).
% 3.54/3.70  cnf(c1316,plain,ip(uri_rdf_predicate),inference(resolution,[status(thm)],[c1311, c138])).
% 3.54/3.70  cnf(c1320,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_predicate,uri_rdf_predicate),inference(resolution,[status(thm)],[c1316, c24])).
% 3.54/3.70  cnf(c1322,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X680)|iext(X680,uri_rdf_predicate,uri_rdf_predicate),inference(resolution,[status(thm)],[c1320, c32])).
% 3.54/3.70  cnf(c1313,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X679)|iext(X679,uri_rdf_predicate,uri_rdf_Property),inference(resolution,[status(thm)],[c1311, c32])).
% 3.54/3.70  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.54/3.70  fof(c37,plain,(![C]:(~ic(C)|iext(uri_rdfs_subClassOf,C,C))),inference(fof_nnf,[status(thm)],[rdfs_subclassof_reflex])).
% 3.54/3.70  fof(c38,plain,(![X15]:(~ic(X15)|iext(uri_rdfs_subClassOf,X15,X15))),inference(variable_rename,[status(thm)],[c37])).
% 3.54/3.70  cnf(c39,plain,~ic(X72)|iext(uri_rdfs_subClassOf,X72,X72),inference(split_conjunct,[status(thm)],[c38])).
% 3.54/3.70  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.54/3.70  fof(c73,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.54/3.70  fof(c74,plain,((![X]:(~ic(X)|icext(uri_rdfs_Class,X)))&(![X]:(~icext(uri_rdfs_Class,X)|ic(X)))),inference(shift_quantors,[status(thm)],[c73])).
% 3.54/3.70  fof(c76,plain,(![X27]:(![X28]:((~ic(X27)|icext(uri_rdfs_Class,X27))&(~icext(uri_rdfs_Class,X28)|ic(X28))))),inference(shift_quantors,[status(thm)],[fof(c75,plain,((![X27]:(~ic(X27)|icext(uri_rdfs_Class,X27)))&(![X28]:(~icext(uri_rdfs_Class,X28)|ic(X28)))),inference(variable_rename,[status(thm)],[c74])).])).
% 3.54/3.70  cnf(c78,plain,~icext(uri_rdfs_Class,X62)|ic(X62),inference(split_conjunct,[status(thm)],[c76])).
% 3.54/3.70  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.54/3.70  cnf(c17,plain,iext(uri_rdfs_range,uri_rdf_type,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_type_range])).
% 3.54/3.70  fof(testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties,axiom,(?[BNODE_z]:(((((((iext(uri_rdf_type,uri_ex_hasAncestor,uri_owl_TransitiveProperty)&iext(uri_rdfs_subClassOf,uri_ex_Person,BNODE_z))&iext(uri_rdf_type,BNODE_z,uri_owl_Restriction))&iext(uri_owl_onProperty,BNODE_z,uri_ex_hasAncestor))&iext(uri_owl_minCardinality,BNODE_z,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger)))&iext(uri_rdf_type,uri_ex_alice,uri_ex_Person))&iext(uri_rdf_type,uri_ex_bob,uri_ex_Person))&iext(uri_ex_hasAncestor,uri_ex_alice,uri_ex_bob))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties)).
% 3.54/3.70  fof(c0,plain,((((?[BNODE_z]:((((iext(uri_rdf_type,uri_ex_hasAncestor,uri_owl_TransitiveProperty)&iext(uri_rdfs_subClassOf,uri_ex_Person,BNODE_z))&iext(uri_rdf_type,BNODE_z,uri_owl_Restriction))&iext(uri_owl_onProperty,BNODE_z,uri_ex_hasAncestor))&iext(uri_owl_minCardinality,BNODE_z,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))))&iext(uri_rdf_type,uri_ex_alice,uri_ex_Person))&iext(uri_rdf_type,uri_ex_bob,uri_ex_Person))&iext(uri_ex_hasAncestor,uri_ex_alice,uri_ex_bob)),inference(shift_quantors,[status(thm)],[testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties])).
% 3.54/3.70  fof(c1,plain,((((?[X2]:((((iext(uri_rdf_type,uri_ex_hasAncestor,uri_owl_TransitiveProperty)&iext(uri_rdfs_subClassOf,uri_ex_Person,X2))&iext(uri_rdf_type,X2,uri_owl_Restriction))&iext(uri_owl_onProperty,X2,uri_ex_hasAncestor))&iext(uri_owl_minCardinality,X2,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))))&iext(uri_rdf_type,uri_ex_alice,uri_ex_Person))&iext(uri_rdf_type,uri_ex_bob,uri_ex_Person))&iext(uri_ex_hasAncestor,uri_ex_alice,uri_ex_bob)),inference(variable_rename,[status(thm)],[c0])).
% 3.54/3.70  fof(c2,plain,(((((((iext(uri_rdf_type,uri_ex_hasAncestor,uri_owl_TransitiveProperty)&iext(uri_rdfs_subClassOf,uri_ex_Person,skolem0001))&iext(uri_rdf_type,skolem0001,uri_owl_Restriction))&iext(uri_owl_onProperty,skolem0001,uri_ex_hasAncestor))&iext(uri_owl_minCardinality,skolem0001,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger)))&iext(uri_rdf_type,uri_ex_alice,uri_ex_Person))&iext(uri_rdf_type,uri_ex_bob,uri_ex_Person))&iext(uri_ex_hasAncestor,uri_ex_alice,uri_ex_bob)),inference(skolemize,[status(esa)],[c1])).
% 3.54/3.70  cnf(c3,plain,iext(uri_rdf_type,uri_ex_hasAncestor,uri_owl_TransitiveProperty),inference(split_conjunct,[status(thm)],[c2])).
% 3.54/3.70  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.54/3.70  fof(c56,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.54/3.70  fof(c57,plain,(![X19]:(![X20]:(![X21]:(![X22]:((~iext(uri_rdfs_range,X19,X20)|~iext(X19,X21,X22))|icext(X20,X22)))))),inference(variable_rename,[status(thm)],[c56])).
% 3.54/3.70  cnf(c58,plain,~iext(uri_rdfs_range,X81,X83)|~iext(X81,X82,X80)|icext(X83,X80),inference(split_conjunct,[status(thm)],[c57])).
% 3.54/3.70  cnf(c302,plain,~iext(uri_rdfs_range,uri_rdf_type,X224)|icext(X224,uri_owl_TransitiveProperty),inference(resolution,[status(thm)],[c58, c3])).
% 3.54/3.70  cnf(c1279,plain,icext(uri_rdfs_Class,uri_owl_TransitiveProperty),inference(resolution,[status(thm)],[c302, c17])).
% 3.54/3.70  cnf(c1280,plain,ic(uri_owl_TransitiveProperty),inference(resolution,[status(thm)],[c1279, c78])).
% 3.54/3.70  cnf(c1284,plain,iext(uri_rdfs_subClassOf,uri_owl_TransitiveProperty,uri_owl_TransitiveProperty),inference(resolution,[status(thm)],[c1280, c39])).
% 3.54/3.70  cnf(c1298,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X677)|iext(X677,uri_owl_TransitiveProperty,uri_owl_TransitiveProperty),inference(resolution,[status(thm)],[c1284, c32])).
% 3.54/3.70  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.54/3.70  fof(c34,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.54/3.70  fof(c35,plain,(![X12]:(![X13]:(![X14]:((~iext(uri_rdfs_subClassOf,X12,X13)|~iext(uri_rdfs_subClassOf,X13,X14))|iext(uri_rdfs_subClassOf,X12,X14))))),inference(variable_rename,[status(thm)],[c34])).
% 3.54/3.70  cnf(c36,plain,~iext(uri_rdfs_subClassOf,X69,X70)|~iext(uri_rdfs_subClassOf,X70,X71)|iext(uri_rdfs_subClassOf,X69,X71),inference(split_conjunct,[status(thm)],[c35])).
% 3.54/3.70  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.54/3.70  fof(c114,plain,(![C]:(~ic(C)|iext(uri_rdfs_subClassOf,C,uri_rdfs_Resource))),inference(fof_nnf,[status(thm)],[rdfs_class_instsub_resource])).
% 3.54/3.70  fof(c115,plain,(![X35]:(~ic(X35)|iext(uri_rdfs_subClassOf,X35,uri_rdfs_Resource))),inference(variable_rename,[status(thm)],[c114])).
% 3.54/3.70  cnf(c116,plain,~ic(X90)|iext(uri_rdfs_subClassOf,X90,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[c115])).
% 3.54/3.70  cnf(c1283,plain,iext(uri_rdfs_subClassOf,uri_owl_TransitiveProperty,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1280, c116])).
% 3.54/3.70  cnf(c1295,plain,~iext(uri_rdfs_subClassOf,X676,uri_owl_TransitiveProperty)|iext(uri_rdfs_subClassOf,X676,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1283, c36])).
% 3.54/3.70  cnf(c1290,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X675)|iext(X675,uri_owl_TransitiveProperty,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1283, c32])).
% 3.54/3.70  cnf(c1281,plain,iext(uri_rdf_type,uri_owl_TransitiveProperty,uri_rdfs_Class),inference(resolution,[status(thm)],[c1279, c122])).
% 3.54/3.70  cnf(c1286,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X674)|iext(X674,uri_owl_TransitiveProperty,uri_rdfs_Class),inference(resolution,[status(thm)],[c1281, c32])).
% 3.54/3.70  cnf(c5,plain,iext(uri_rdf_type,skolem0001,uri_owl_Restriction),inference(split_conjunct,[status(thm)],[c2])).
% 3.54/3.70  cnf(c283,plain,~iext(uri_rdfs_range,uri_rdf_type,X185)|icext(X185,uri_owl_Restriction),inference(resolution,[status(thm)],[c58, c5])).
% 3.54/3.70  cnf(c1204,plain,icext(uri_rdfs_Class,uri_owl_Restriction),inference(resolution,[status(thm)],[c283, c17])).
% 3.54/3.70  cnf(c1205,plain,ic(uri_owl_Restriction),inference(resolution,[status(thm)],[c1204, c78])).
% 3.54/3.70  cnf(c1209,plain,iext(uri_rdfs_subClassOf,uri_owl_Restriction,uri_owl_Restriction),inference(resolution,[status(thm)],[c1205, c39])).
% 3.54/3.70  cnf(c1270,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X672)|iext(X672,uri_owl_Restriction,uri_owl_Restriction),inference(resolution,[status(thm)],[c1209, c32])).
% 3.54/3.70  cnf(c1208,plain,iext(uri_rdfs_subClassOf,uri_owl_Restriction,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1205, c116])).
% 3.54/3.70  cnf(c1267,plain,~iext(uri_rdfs_subClassOf,X671,uri_owl_Restriction)|iext(uri_rdfs_subClassOf,X671,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1208, c36])).
% 3.54/3.70  cnf(c1262,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X670)|iext(X670,uri_owl_Restriction,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1208, c32])).
% 3.54/3.70  cnf(c1206,plain,iext(uri_rdf_type,uri_owl_Restriction,uri_rdfs_Class),inference(resolution,[status(thm)],[c1204, c122])).
% 3.54/3.70  cnf(c1258,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X669)|iext(X669,uri_owl_Restriction,uri_rdfs_Class),inference(resolution,[status(thm)],[c1206, c32])).
% 3.54/3.70  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.54/3.70  cnf(c55,plain,iext(uri_rdfs_range,uri_rdfs_range,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_range_range])).
% 3.54/3.70  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.54/3.70  cnf(c110,plain,iext(uri_rdfs_range,uri_rdf_rest,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdfs_collection_rest_range])).
% 3.54/3.70  cnf(c270,plain,~iext(uri_rdfs_range,uri_rdfs_range,X172)|icext(X172,uri_rdf_List),inference(resolution,[status(thm)],[c58, c110])).
% 3.54/3.70  cnf(c1154,plain,icext(uri_rdfs_Class,uri_rdf_List),inference(resolution,[status(thm)],[c270, c55])).
% 3.54/3.70  cnf(c1155,plain,ic(uri_rdf_List),inference(resolution,[status(thm)],[c1154, c78])).
% 3.54/3.70  cnf(c1159,plain,iext(uri_rdfs_subClassOf,uri_rdf_List,uri_rdf_List),inference(resolution,[status(thm)],[c1155, c39])).
% 3.54/3.70  cnf(c1249,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X667)|iext(X667,uri_rdf_List,uri_rdf_List),inference(resolution,[status(thm)],[c1159, c32])).
% 3.54/3.70  cnf(c1158,plain,iext(uri_rdfs_subClassOf,uri_rdf_List,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1155, c116])).
% 3.54/3.70  cnf(c1246,plain,~iext(uri_rdfs_subClassOf,X666,uri_rdf_List)|iext(uri_rdfs_subClassOf,X666,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1158, c36])).
% 3.54/3.70  cnf(c1241,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X665)|iext(X665,uri_rdf_List,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1158, c32])).
% 3.54/3.70  cnf(c1156,plain,iext(uri_rdf_type,uri_rdf_List,uri_rdfs_Class),inference(resolution,[status(thm)],[c1154, c122])).
% 3.54/3.70  cnf(c1237,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X664)|iext(X664,uri_rdf_List,uri_rdfs_Class),inference(resolution,[status(thm)],[c1156, c32])).
% 3.54/3.70  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.54/3.70  cnf(c79,plain,iext(uri_rdfs_range,uri_rdfs_domain,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_domain_range])).
% 3.54/3.70  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.54/3.70  cnf(c50,plain,iext(uri_rdfs_domain,uri_rdf_subject,uri_rdfs_Statement),inference(split_conjunct,[status(thm)],[rdfs_reification_subject_domain])).
% 3.54/3.70  cnf(c266,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X168)|icext(X168,uri_rdfs_Statement),inference(resolution,[status(thm)],[c58, c50])).
% 3.54/3.70  cnf(c1116,plain,icext(uri_rdfs_Class,uri_rdfs_Statement),inference(resolution,[status(thm)],[c266, c79])).
% 3.54/3.70  cnf(c1117,plain,ic(uri_rdfs_Statement),inference(resolution,[status(thm)],[c1116, c78])).
% 3.54/3.70  cnf(c1121,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Statement,uri_rdfs_Statement),inference(resolution,[status(thm)],[c1117, c39])).
% 3.54/3.70  cnf(c1226,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X662)|iext(X662,uri_rdfs_Statement,uri_rdfs_Statement),inference(resolution,[status(thm)],[c1121, c32])).
% 3.54/3.70  cnf(c1120,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Statement,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1117, c116])).
% 3.54/3.70  cnf(c1223,plain,~iext(uri_rdfs_subClassOf,X661,uri_rdfs_Statement)|iext(uri_rdfs_subClassOf,X661,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1120, c36])).
% 3.54/3.70  cnf(c1218,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X660)|iext(X660,uri_rdfs_Statement,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1120, c32])).
% 3.54/3.70  cnf(c1118,plain,iext(uri_rdf_type,uri_rdfs_Statement,uri_rdfs_Class),inference(resolution,[status(thm)],[c1116, c122])).
% 3.54/3.70  cnf(c1214,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X659)|iext(X659,uri_rdfs_Statement,uri_rdfs_Class),inference(resolution,[status(thm)],[c1118, c32])).
% 3.54/3.70  cnf(c9,plain,iext(uri_rdf_type,uri_ex_bob,uri_ex_Person),inference(split_conjunct,[status(thm)],[c2])).
% 3.54/3.70  cnf(c121,plain,~iext(uri_rdf_type,X91,X92)|icext(X92,X91),inference(split_conjunct,[status(thm)],[c120])).
% 3.54/3.70  cnf(c410,plain,icext(uri_ex_Person,uri_ex_bob),inference(resolution,[status(thm)],[c121, c9])).
% 3.54/3.70  cnf(c4,plain,iext(uri_rdfs_subClassOf,uri_ex_Person,skolem0001),inference(split_conjunct,[status(thm)],[c2])).
% 3.54/3.70  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.54/3.70  fof(c41,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.54/3.70  fof(c43,plain,(![X16]:(![X17]:(![X18]:(~iext(uri_rdfs_subClassOf,X16,X17)|((ic(X16)&ic(X17))&(~icext(X16,X18)|icext(X17,X18))))))),inference(shift_quantors,[status(thm)],[fof(c42,plain,(![X16]:(![X17]:(~iext(uri_rdfs_subClassOf,X16,X17)|((ic(X16)&ic(X17))&(![X18]:(~icext(X16,X18)|icext(X17,X18))))))),inference(variable_rename,[status(thm)],[c41])).])).
% 3.54/3.70  fof(c44,plain,(![X16]:(![X17]:(![X18]:(((~iext(uri_rdfs_subClassOf,X16,X17)|ic(X16))&(~iext(uri_rdfs_subClassOf,X16,X17)|ic(X17)))&(~iext(uri_rdfs_subClassOf,X16,X17)|(~icext(X16,X18)|icext(X17,X18))))))),inference(distribute,[status(thm)],[c43])).
% 3.54/3.70  cnf(c47,plain,~iext(uri_rdfs_subClassOf,X79,X78)|~icext(X79,X77)|icext(X78,X77),inference(split_conjunct,[status(thm)],[c44])).
% 3.54/3.70  cnf(c253,plain,~icext(uri_ex_Person,X160)|icext(skolem0001,X160),inference(resolution,[status(thm)],[c47, c4])).
% 3.54/3.70  cnf(c1029,plain,icext(skolem0001,uri_ex_bob),inference(resolution,[status(thm)],[c253, c410])).
% 3.54/3.70  cnf(c1031,plain,iext(uri_rdf_type,uri_ex_bob,skolem0001),inference(resolution,[status(thm)],[c1029, c122])).
% 3.54/3.70  cnf(c1202,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X658)|iext(X658,uri_ex_bob,skolem0001),inference(resolution,[status(thm)],[c1031, c32])).
% 3.54/3.70  cnf(c8,plain,iext(uri_rdf_type,uri_ex_alice,uri_ex_Person),inference(split_conjunct,[status(thm)],[c2])).
% 3.54/3.70  cnf(c408,plain,icext(uri_ex_Person,uri_ex_alice),inference(resolution,[status(thm)],[c121, c8])).
% 3.54/3.70  cnf(c1028,plain,icext(skolem0001,uri_ex_alice),inference(resolution,[status(thm)],[c253, c408])).
% 3.54/3.70  cnf(c1030,plain,iext(uri_rdf_type,uri_ex_alice,skolem0001),inference(resolution,[status(thm)],[c1028, c122])).
% 3.54/3.70  cnf(c1197,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X657)|iext(X657,uri_ex_alice,skolem0001),inference(resolution,[status(thm)],[c1030, c32])).
% 3.54/3.70  cnf(c31,plain,~iext(uri_rdfs_subPropertyOf,X64,X63)|ip(X63),inference(split_conjunct,[status(thm)],[c29])).
% 3.54/3.70  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.54/3.71  fof(c105,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.54/3.71  fof(c106,plain,(![X34]:(~icext(uri_rdfs_ContainerMembershipProperty,X34)|iext(uri_rdfs_subPropertyOf,X34,uri_rdfs_member))),inference(variable_rename,[status(thm)],[c105])).
% 3.54/3.71  cnf(c107,plain,~icext(uri_rdfs_ContainerMembershipProperty,X89)|iext(uri_rdfs_subPropertyOf,X89,uri_rdfs_member),inference(split_conjunct,[status(thm)],[c106])).
% 3.54/3.71  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.54/3.71  cnf(c93,plain,iext(uri_rdf_type,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),inference(split_conjunct,[status(thm)],[rdfs_container_n_type_003])).
% 3.54/3.71  cnf(c411,plain,icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__3),inference(resolution,[status(thm)],[c121, c93])).
% 3.54/3.71  cnf(c434,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__3,uri_rdfs_member),inference(resolution,[status(thm)],[c411, c107])).
% 3.54/3.71  cnf(c890,plain,ip(uri_rdfs_member),inference(resolution,[status(thm)],[c434, c31])).
% 3.54/3.71  cnf(c893,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_member,uri_rdfs_member),inference(resolution,[status(thm)],[c890, c24])).
% 3.54/3.71  cnf(c1185,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X656)|iext(X656,uri_rdfs_member,uri_rdfs_member),inference(resolution,[status(thm)],[c893, c32])).
% 3.54/3.71  cnf(c139,plain,~ip(X98)|iext(uri_rdf_type,X98,uri_rdf_Property),inference(split_conjunct,[status(thm)],[c137])).
% 3.54/3.71  cnf(c892,plain,iext(uri_rdf_type,uri_rdfs_member,uri_rdf_Property),inference(resolution,[status(thm)],[c890, c139])).
% 3.54/3.71  cnf(c1179,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X654)|iext(X654,uri_rdfs_member,uri_rdf_Property),inference(resolution,[status(thm)],[c892, c32])).
% 3.54/3.71  cnf(c77,plain,~ic(X61)|icext(uri_rdfs_Class,X61),inference(split_conjunct,[status(thm)],[c76])).
% 3.54/3.71  cnf(c46,plain,~iext(uri_rdfs_subClassOf,X76,X75)|ic(X75),inference(split_conjunct,[status(thm)],[c44])).
% 3.54/3.71  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.54/3.71  cnf(c109,plain,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Container),inference(split_conjunct,[status(thm)],[rdfs_container_alt_sub])).
% 3.54/3.71  cnf(c45,plain,~iext(uri_rdfs_subClassOf,X74,X73)|ic(X74),inference(split_conjunct,[status(thm)],[c44])).
% 3.54/3.71  cnf(c221,plain,ic(uri_rdf_Alt),inference(resolution,[status(thm)],[c45, c109])).
% 3.54/3.71  cnf(c380,plain,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Resource),inference(resolution,[status(thm)],[c116, c221])).
% 3.54/3.71  cnf(c719,plain,ic(uri_rdfs_Resource),inference(resolution,[status(thm)],[c380, c46])).
% 3.54/3.71  cnf(c721,plain,icext(uri_rdfs_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c719, c77])).
% 3.54/3.71  cnf(c725,plain,iext(uri_rdf_type,uri_rdfs_Resource,uri_rdfs_Class),inference(resolution,[status(thm)],[c721, c122])).
% 3.54/3.71  cnf(c1173,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X653)|iext(X653,uri_rdfs_Resource,uri_rdfs_Class),inference(resolution,[status(thm)],[c725, c32])).
% 3.54/3.71  cnf(c722,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Resource,uri_rdfs_Resource),inference(resolution,[status(thm)],[c719, c116])).
% 3.54/3.71  cnf(c1166,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X652)|iext(X652,uri_rdfs_Resource,uri_rdfs_Resource),inference(resolution,[status(thm)],[c722, c32])).
% 3.54/3.71  cnf(c7,plain,iext(uri_owl_minCardinality,skolem0001,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger)),inference(split_conjunct,[status(thm)],[c2])).
% 3.54/3.71  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.54/3.71  fof(c154,plain,(![S]:(![P]:(![O]:(~iext(P,S,O)|ip(P))))),inference(fof_nnf,[status(thm)],[simple_iext_property])).
% 3.54/3.71  fof(c155,plain,(![S]:(![P]:((![O]:~iext(P,S,O))|ip(P)))),inference(shift_quantors,[status(thm)],[c154])).
% 3.54/3.71  fof(c157,plain,(![X44]:(![X45]:(![X46]:(~iext(X45,X44,X46)|ip(X45))))),inference(shift_quantors,[status(thm)],[fof(c156,plain,(![X44]:(![X45]:((![X46]:~iext(X45,X44,X46))|ip(X45)))),inference(variable_rename,[status(thm)],[c155])).])).
% 3.54/3.71  cnf(c158,plain,~iext(X100,X99,X101)|ip(X100),inference(split_conjunct,[status(thm)],[c157])).
% 3.54/3.71  cnf(c589,plain,ip(uri_owl_minCardinality),inference(resolution,[status(thm)],[c158, c7])).
% 3.54/3.71  cnf(c615,plain,iext(uri_rdfs_subPropertyOf,uri_owl_minCardinality,uri_owl_minCardinality),inference(resolution,[status(thm)],[c589, c24])).
% 3.54/3.71  cnf(c1150,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X650)|iext(X650,uri_owl_minCardinality,uri_owl_minCardinality),inference(resolution,[status(thm)],[c615, c32])).
% 3.54/3.71  cnf(c614,plain,iext(uri_rdf_type,uri_owl_minCardinality,uri_rdf_Property),inference(resolution,[status(thm)],[c589, c139])).
% 3.54/3.71  cnf(c1142,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X648)|iext(X648,uri_owl_minCardinality,uri_rdf_Property),inference(resolution,[status(thm)],[c614, c32])).
% 3.54/3.71  cnf(c10,plain,iext(uri_ex_hasAncestor,uri_ex_alice,uri_ex_bob),inference(split_conjunct,[status(thm)],[c2])).
% 3.54/3.71  cnf(c580,plain,ip(uri_ex_hasAncestor),inference(resolution,[status(thm)],[c158, c10])).
% 3.54/3.71  cnf(c613,plain,iext(uri_rdfs_subPropertyOf,uri_ex_hasAncestor,uri_ex_hasAncestor),inference(resolution,[status(thm)],[c580, c24])).
% 3.54/3.71  cnf(c1133,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X647)|iext(X647,uri_ex_hasAncestor,uri_ex_hasAncestor),inference(resolution,[status(thm)],[c613, c32])).
% 3.54/3.71  cnf(c612,plain,iext(uri_rdf_type,uri_ex_hasAncestor,uri_rdf_Property),inference(resolution,[status(thm)],[c580, c139])).
% 3.54/3.71  cnf(c1126,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X645)|iext(X645,uri_ex_hasAncestor,uri_rdf_Property),inference(resolution,[status(thm)],[c612, c32])).
% 3.54/3.71  cnf(c6,plain,iext(uri_owl_onProperty,skolem0001,uri_ex_hasAncestor),inference(split_conjunct,[status(thm)],[c2])).
% 3.54/3.71  cnf(c562,plain,ip(uri_owl_onProperty),inference(resolution,[status(thm)],[c158, c6])).
% 3.54/3.71  cnf(c611,plain,iext(uri_rdfs_subPropertyOf,uri_owl_onProperty,uri_owl_onProperty),inference(resolution,[status(thm)],[c562, c24])).
% 3.54/3.71  cnf(c1111,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X644)|iext(X644,uri_owl_onProperty,uri_owl_onProperty),inference(resolution,[status(thm)],[c611, c32])).
% 3.54/3.71  cnf(c610,plain,iext(uri_rdf_type,uri_owl_onProperty,uri_rdf_Property),inference(resolution,[status(thm)],[c562, c139])).
% 3.54/3.71  cnf(c1104,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X642)|iext(X642,uri_owl_onProperty,uri_rdf_Property),inference(resolution,[status(thm)],[c610, c32])).
% 3.54/3.71  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.54/3.71  cnf(c127,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_sub])).
% 3.54/3.71  cnf(c560,plain,ip(uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c158, c127])).
% 3.54/3.71  cnf(c609,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c560, c24])).
% 3.54/3.71  cnf(c1095,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X641)|iext(X641,uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c609, c32])).
% 3.54/3.71  cnf(c608,plain,iext(uri_rdf_type,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c560, c139])).
% 3.54/3.71  cnf(c1085,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X639)|iext(X639,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c608, c32])).
% 3.54/3.71  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.54/3.71  cnf(c86,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_datatype_sub])).
% 3.54/3.71  cnf(c554,plain,ip(uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c158, c86])).
% 3.54/3.71  cnf(c607,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c554, c24])).
% 3.54/3.71  cnf(c1077,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X638)|iext(X638,uri_rdfs_subClassOf,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c607, c32])).
% 3.54/3.71  cnf(c606,plain,iext(uri_rdf_type,uri_rdfs_subClassOf,uri_rdf_Property),inference(resolution,[status(thm)],[c554, c139])).
% 3.54/3.71  cnf(c1064,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X636)|iext(X636,uri_rdfs_subClassOf,uri_rdf_Property),inference(resolution,[status(thm)],[c606, c32])).
% 3.54/3.71  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.54/3.71  cnf(c25,plain,iext(uri_rdfs_range,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_subpropertyof_range])).
% 3.54/3.71  cnf(c538,plain,ip(uri_rdfs_range),inference(resolution,[status(thm)],[c158, c25])).
% 3.54/3.71  cnf(c605,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_range,uri_rdfs_range),inference(resolution,[status(thm)],[c538, c24])).
% 3.54/3.71  cnf(c1052,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X635)|iext(X635,uri_rdfs_range,uri_rdfs_range),inference(resolution,[status(thm)],[c605, c32])).
% 3.54/3.71  cnf(c604,plain,iext(uri_rdf_type,uri_rdfs_range,uri_rdf_Property),inference(resolution,[status(thm)],[c538, c139])).
% 3.54/3.71  cnf(c1036,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X633)|iext(X633,uri_rdfs_range,uri_rdf_Property),inference(resolution,[status(thm)],[c604, c32])).
% 3.54/3.71  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.54/3.71  cnf(c48,plain,iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_subclassof_domain])).
% 3.54/3.71  cnf(c534,plain,ip(uri_rdfs_domain),inference(resolution,[status(thm)],[c158, c48])).
% 3.54/3.71  cnf(c603,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,uri_rdfs_domain),inference(resolution,[status(thm)],[c534, c24])).
% 3.54/3.71  cnf(c1021,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X632)|iext(X632,uri_rdfs_domain,uri_rdfs_domain),inference(resolution,[status(thm)],[c603, c32])).
% 3.54/3.71  cnf(c602,plain,iext(uri_rdf_type,uri_rdfs_domain,uri_rdf_Property),inference(resolution,[status(thm)],[c534, c139])).
% 3.54/3.71  cnf(c1003,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X630)|iext(X630,uri_rdfs_domain,uri_rdf_Property),inference(resolution,[status(thm)],[c602, c32])).
% 3.54/3.71  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.54/3.71  cnf(c148,plain,iext(uri_rdf_type,uri_rdf_first,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_collection_first_type])).
% 3.54/3.71  cnf(c530,plain,ip(uri_rdf_first),inference(resolution,[status(thm)],[c148, c138])).
% 3.54/3.71  cnf(c533,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_first,uri_rdf_first),inference(resolution,[status(thm)],[c530, c24])).
% 3.54/3.71  cnf(c995,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X629)|iext(X629,uri_rdf_first,uri_rdf_first),inference(resolution,[status(thm)],[c533, c32])).
% 3.54/3.71  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.54/3.71  cnf(c146,plain,iext(uri_rdf_type,uri_rdf_rest,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_collection_rest_type])).
% 3.54/3.71  cnf(c517,plain,ip(uri_rdf_rest),inference(resolution,[status(thm)],[c146, c138])).
% 3.54/3.71  cnf(c524,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_rest,uri_rdf_rest),inference(resolution,[status(thm)],[c517, c24])).
% 3.54/3.71  cnf(c988,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X627)|iext(X627,uri_rdf_rest,uri_rdf_rest),inference(resolution,[status(thm)],[c524, c32])).
% 3.54/3.71  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.54/3.71  cnf(c145,plain,iext(uri_rdf_type,uri_rdf__1,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_container_n_type_001])).
% 3.54/3.71  cnf(c506,plain,ip(uri_rdf__1),inference(resolution,[status(thm)],[c145, c138])).
% 3.54/3.71  cnf(c511,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__1,uri_rdf__1),inference(resolution,[status(thm)],[c506, c24])).
% 3.54/3.71  cnf(c980,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X625)|iext(X625,uri_rdf__1,uri_rdf__1),inference(resolution,[status(thm)],[c511, c32])).
% 3.54/3.71  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.54/3.71  cnf(c144,plain,iext(uri_rdf_type,uri_rdf__2,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_container_n_type_002])).
% 3.54/3.71  cnf(c501,plain,ip(uri_rdf__2),inference(resolution,[status(thm)],[c144, c138])).
% 3.54/3.71  cnf(c509,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__2,uri_rdf__2),inference(resolution,[status(thm)],[c501, c24])).
% 3.54/3.71  cnf(c973,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X623)|iext(X623,uri_rdf__2,uri_rdf__2),inference(resolution,[status(thm)],[c509, c32])).
% 3.54/3.71  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.54/3.71  cnf(c143,plain,iext(uri_rdf_type,uri_rdf__3,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_container_n_type_003])).
% 3.54/3.71  cnf(c493,plain,ip(uri_rdf__3),inference(resolution,[status(thm)],[c143, c138])).
% 3.54/3.71  cnf(c496,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__3,uri_rdf__3),inference(resolution,[status(thm)],[c493, c24])).
% 3.54/3.71  cnf(c965,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X621)|iext(X621,uri_rdf__3,uri_rdf__3),inference(resolution,[status(thm)],[c496, c32])).
% 3.54/3.71  cnf(c30,plain,~iext(uri_rdfs_subPropertyOf,X60,X59)|ip(X60),inference(split_conjunct,[status(thm)],[c29])).
% 3.54/3.71  cnf(c399,plain,ip(uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c127, c30])).
% 3.54/3.71  cnf(c486,plain,iext(uri_rdf_type,uri_rdfs_isDefinedBy,uri_rdf_Property),inference(resolution,[status(thm)],[c139, c399])).
% 3.54/3.71  cnf(c959,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X619)|iext(X619,uri_rdfs_isDefinedBy,uri_rdf_Property),inference(resolution,[status(thm)],[c486, c32])).
% 3.54/3.71  cnf(c402,plain,ip(uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c127, c31])).
% 3.54/3.71  cnf(c483,plain,iext(uri_rdf_type,uri_rdfs_seeAlso,uri_rdf_Property),inference(resolution,[status(thm)],[c139, c402])).
% 3.54/3.71  cnf(c951,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X618)|iext(X618,uri_rdfs_seeAlso,uri_rdf_Property),inference(resolution,[status(thm)],[c483, c32])).
% 3.54/3.71  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.54/3.71  cnf(c142,plain,iext(uri_rdf_type,uri_rdf_object,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_reification_object_type])).
% 3.54/3.71  cnf(c480,plain,ip(uri_rdf_object),inference(resolution,[status(thm)],[c142, c138])).
% 3.54/3.71  cnf(c482,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_object,uri_rdf_object),inference(resolution,[status(thm)],[c480, c24])).
% 3.54/3.71  cnf(c943,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X617)|iext(X617,uri_rdf_object,uri_rdf_object),inference(resolution,[status(thm)],[c482, c32])).
% 3.54/3.71  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.54/3.71  cnf(c141,plain,iext(uri_rdf_type,uri_rdf_value,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_reification_predicate_type])).
% 3.54/3.71  cnf(c473,plain,ip(uri_rdf_value),inference(resolution,[status(thm)],[c138, c141])).
% 3.54/3.71  cnf(c476,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_value,uri_rdf_value),inference(resolution,[status(thm)],[c473, c24])).
% 3.54/3.71  cnf(c936,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X615)|iext(X615,uri_rdf_value,uri_rdf_value),inference(resolution,[status(thm)],[c476, c32])).
% 3.54/3.71  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.54/3.71  cnf(c140,plain,iext(uri_rdf_type,uri_rdf_subject,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_reification_subject_type])).
% 3.54/3.71  cnf(c472,plain,ip(uri_rdf_subject),inference(resolution,[status(thm)],[c138, c140])).
% 3.54/3.71  cnf(c475,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_subject,uri_rdf_subject),inference(resolution,[status(thm)],[c472, c24])).
% 3.54/3.71  cnf(c929,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X613)|iext(X613,uri_rdf_subject,uri_rdf_subject),inference(resolution,[status(thm)],[c475, c32])).
% 3.54/3.71  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.54/3.71  cnf(c132,plain,iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_value_type])).
% 3.54/3.71  cnf(c471,plain,ip(uri_rdf_type),inference(resolution,[status(thm)],[c138, c132])).
% 3.54/3.71  cnf(c474,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_type,uri_rdf_type),inference(resolution,[status(thm)],[c471, c24])).
% 3.54/3.71  cnf(c919,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X611)|iext(X611,uri_rdf_type,uri_rdf_type),inference(resolution,[status(thm)],[c474, c32])).
% 3.54/3.71  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.54/3.71  cnf(c94,plain,iext(uri_rdf_type,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),inference(split_conjunct,[status(thm)],[rdfs_container_n_type_002])).
% 3.54/3.71  cnf(c414,plain,icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__2),inference(resolution,[status(thm)],[c121, c94])).
% 3.54/3.71  cnf(c439,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__2,uri_rdfs_member),inference(resolution,[status(thm)],[c414, c107])).
% 3.54/3.71  cnf(c906,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X609)|iext(X609,uri_rdf__2,uri_rdfs_member),inference(resolution,[status(thm)],[c439, c32])).
% 3.54/3.71  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.54/3.71  fof(c19,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.54/3.71  fof(c20,plain,(![X4]:(![X5]:(![X6]:((~iext(uri_rdfs_subPropertyOf,X4,X5)|~iext(uri_rdfs_subPropertyOf,X5,X6))|iext(uri_rdfs_subPropertyOf,X4,X6))))),inference(variable_rename,[status(thm)],[c19])).
% 3.54/3.71  cnf(c21,plain,~iext(uri_rdfs_subPropertyOf,X52,X51)|~iext(uri_rdfs_subPropertyOf,X51,X50)|iext(uri_rdfs_subPropertyOf,X52,X50),inference(split_conjunct,[status(thm)],[c20])).
% 3.54/3.71  cnf(c905,plain,~iext(uri_rdfs_subPropertyOf,X608,uri_rdf__2)|iext(uri_rdfs_subPropertyOf,X608,uri_rdfs_member),inference(resolution,[status(thm)],[c439, c21])).
% 3.54/3.71  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.54/3.71  cnf(c95,plain,iext(uri_rdf_type,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),inference(split_conjunct,[status(thm)],[rdfs_container_n_type_001])).
% 3.54/3.71  cnf(c413,plain,icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__1),inference(resolution,[status(thm)],[c121, c95])).
% 3.54/3.71  cnf(c437,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__1,uri_rdfs_member),inference(resolution,[status(thm)],[c413, c107])).
% 3.54/3.71  cnf(c898,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X607)|iext(X607,uri_rdf__1,uri_rdfs_member),inference(resolution,[status(thm)],[c437, c32])).
% 3.54/3.71  cnf(c897,plain,~iext(uri_rdfs_subPropertyOf,X606,uri_rdf__1)|iext(uri_rdfs_subPropertyOf,X606,uri_rdfs_member),inference(resolution,[status(thm)],[c437, c21])).
% 3.54/3.71  cnf(c888,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X605)|iext(X605,uri_rdf__3,uri_rdfs_member),inference(resolution,[status(thm)],[c434, c32])).
% 3.54/3.71  cnf(c887,plain,~iext(uri_rdfs_subPropertyOf,X604,uri_rdf__3)|iext(uri_rdfs_subPropertyOf,X604,uri_rdfs_member),inference(resolution,[status(thm)],[c434, c21])).
% 3.54/3.71  cnf(c218,plain,ic(uri_rdfs_Datatype),inference(resolution,[status(thm)],[c45, c86])).
% 3.54/3.71  cnf(c225,plain,icext(uri_rdfs_Class,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c218, c77])).
% 3.54/3.71  cnf(c432,plain,iext(uri_rdf_type,uri_rdfs_Datatype,uri_rdfs_Class),inference(resolution,[status(thm)],[c122, c225])).
% 3.54/3.71  cnf(c882,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X603)|iext(X603,uri_rdfs_Datatype,uri_rdfs_Class),inference(resolution,[status(thm)],[c432, c32])).
% 3.54/3.71  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.54/3.71  cnf(c91,plain,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[rdfs_dat_xmlliteral_sub])).
% 3.54/3.71  cnf(c237,plain,ic(uri_rdfs_Literal),inference(resolution,[status(thm)],[c46, c91])).
% 3.54/3.71  cnf(c250,plain,icext(uri_rdfs_Class,uri_rdfs_Literal),inference(resolution,[status(thm)],[c237, c77])).
% 3.54/3.71  cnf(c431,plain,iext(uri_rdf_type,uri_rdfs_Literal,uri_rdfs_Class),inference(resolution,[status(thm)],[c122, c250])).
% 3.54/3.71  cnf(c876,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X602)|iext(X602,uri_rdfs_Literal,uri_rdfs_Class),inference(resolution,[status(thm)],[c431, c32])).
% 3.54/3.71  cnf(c238,plain,ic(uri_rdfs_Container),inference(resolution,[status(thm)],[c46, c109])).
% 3.54/3.71  cnf(c259,plain,icext(uri_rdfs_Class,uri_rdfs_Container),inference(resolution,[status(thm)],[c238, c77])).
% 3.54/3.71  cnf(c430,plain,iext(uri_rdf_type,uri_rdfs_Container,uri_rdfs_Class),inference(resolution,[status(thm)],[c122, c259])).
% 3.54/3.71  cnf(c871,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X601)|iext(X601,uri_rdfs_Container,uri_rdfs_Class),inference(resolution,[status(thm)],[c430, c32])).
% 3.54/3.71  cnf(c236,plain,ic(skolem0001),inference(resolution,[status(thm)],[c46, c4])).
% 3.54/3.71  cnf(c248,plain,icext(uri_rdfs_Class,skolem0001),inference(resolution,[status(thm)],[c236, c77])).
% 3.54/3.71  cnf(c428,plain,iext(uri_rdf_type,skolem0001,uri_rdfs_Class),inference(resolution,[status(thm)],[c122, c248])).
% 3.54/3.71  cnf(c866,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X600)|iext(X600,skolem0001,uri_rdfs_Class),inference(resolution,[status(thm)],[c428, c32])).
% 3.54/3.71  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.54/3.71  cnf(c104,plain,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_container_containermembershipproperty_sub])).
% 3.54/3.71  cnf(c223,plain,ic(uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c45, c104])).
% 3.54/3.71  cnf(c242,plain,icext(uri_rdfs_Class,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c223, c77])).
% 3.54/3.71  cnf(c427,plain,iext(uri_rdf_type,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Class),inference(resolution,[status(thm)],[c122, c242])).
% 3.54/3.71  cnf(c861,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X599)|iext(X599,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Class),inference(resolution,[status(thm)],[c427, c32])).
% 3.54/3.71  cnf(c231,plain,icext(uri_rdfs_Class,uri_rdf_Alt),inference(resolution,[status(thm)],[c221, c77])).
% 3.54/3.71  cnf(c425,plain,iext(uri_rdf_type,uri_rdf_Alt,uri_rdfs_Class),inference(resolution,[status(thm)],[c122, c231])).
% 3.54/3.71  cnf(c856,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X598)|iext(X598,uri_rdf_Alt,uri_rdfs_Class),inference(resolution,[status(thm)],[c425, c32])).
% 3.54/3.71  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.54/3.71  cnf(c92,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Container),inference(split_conjunct,[status(thm)],[rdfs_container_seq_sub])).
% 3.54/3.71  cnf(c222,plain,ic(uri_rdfs_Seq),inference(resolution,[status(thm)],[c45, c92])).
% 3.54/3.71  cnf(c233,plain,icext(uri_rdfs_Class,uri_rdfs_Seq),inference(resolution,[status(thm)],[c222, c77])).
% 3.54/3.71  cnf(c424,plain,iext(uri_rdf_type,uri_rdfs_Seq,uri_rdfs_Class),inference(resolution,[status(thm)],[c122, c233])).
% 3.54/3.71  cnf(c851,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X597)|iext(X597,uri_rdfs_Seq,uri_rdfs_Class),inference(resolution,[status(thm)],[c424, c32])).
% 3.54/3.71  cnf(c235,plain,ic(uri_rdfs_Class),inference(resolution,[status(thm)],[c46, c86])).
% 3.54/3.71  cnf(c246,plain,icext(uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c235, c77])).
% 3.54/3.71  cnf(c423,plain,iext(uri_rdf_type,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c122, c246])).
% 3.54/3.71  cnf(c846,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X596)|iext(X596,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c423, c32])).
% 3.54/3.71  cnf(c219,plain,ic(uri_ex_Person),inference(resolution,[status(thm)],[c45, c4])).
% 3.54/3.71  cnf(c227,plain,icext(uri_rdfs_Class,uri_ex_Person),inference(resolution,[status(thm)],[c219, c77])).
% 3.54/3.71  cnf(c422,plain,iext(uri_rdf_type,uri_ex_Person,uri_rdfs_Class),inference(resolution,[status(thm)],[c122, c227])).
% 3.54/3.71  cnf(c841,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X595)|iext(X595,uri_ex_Person,uri_rdfs_Class),inference(resolution,[status(thm)],[c422, c32])).
% 3.54/3.71  cnf(c1410,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X594)|icext(X594,uri_rdfs_comment),inference(resolution,[status(thm)],[c1403, c84])).
% 3.54/3.71  cnf(c1407,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X593)|icext(X593,uri_rdfs_comment),inference(resolution,[status(thm)],[c1403, c58])).
% 3.54/3.71  cnf(c220,plain,ic(uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c45, c91])).
% 3.54/3.71  cnf(c229,plain,icext(uri_rdfs_Class,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c220, c77])).
% 3.54/3.71  cnf(c421,plain,iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Class),inference(resolution,[status(thm)],[c122, c229])).
% 3.54/3.71  cnf(c836,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X592)|iext(X592,uri_rdf_XMLLiteral,uri_rdfs_Class),inference(resolution,[status(thm)],[c421, c32])).
% 3.54/3.71  cnf(c1380,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X589)|icext(X589,uri_rdfs_label),inference(resolution,[status(thm)],[c1374, c84])).
% 3.54/3.71  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.54/3.71  cnf(c108,plain,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Container),inference(split_conjunct,[status(thm)],[rdfs_container_bag_sub])).
% 3.54/3.71  cnf(c224,plain,ic(uri_rdf_Bag),inference(resolution,[status(thm)],[c45, c108])).
% 3.54/3.71  cnf(c244,plain,icext(uri_rdfs_Class,uri_rdf_Bag),inference(resolution,[status(thm)],[c224, c77])).
% 3.54/3.71  cnf(c416,plain,iext(uri_rdf_type,uri_rdf_Bag,uri_rdfs_Class),inference(resolution,[status(thm)],[c122, c244])).
% 3.54/3.71  cnf(c831,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X588)|iext(X588,uri_rdf_Bag,uri_rdfs_Class),inference(resolution,[status(thm)],[c416, c32])).
% 3.54/3.71  cnf(c1377,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X587)|icext(X587,uri_rdfs_label),inference(resolution,[status(thm)],[c1374, c58])).
% 3.54/3.71  cnf(c405,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_seeAlso,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c402, c24])).
% 3.54/3.71  cnf(c824,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X584)|iext(X584,uri_rdfs_seeAlso,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c405, c32])).
% 3.54/3.71  cnf(c1327,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X583)|icext(X583,uri_rdf_predicate),inference(resolution,[status(thm)],[c1320, c84])).
% 3.54/3.71  cnf(c1324,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X582)|icext(X582,uri_rdf_predicate),inference(resolution,[status(thm)],[c1320, c58])).
% 3.54/3.71  cnf(c1301,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X577)|icext(X577,uri_owl_TransitiveProperty),inference(resolution,[status(thm)],[c1284, c58])).
% 3.54/3.71  cnf(c404,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c399, c24])).
% 3.54/3.71  cnf(c817,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X576)|iext(X576,uri_rdfs_isDefinedBy,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c404, c32])).
% 3.54/3.71  cnf(c1296,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X575)|icext(X575,uri_owl_TransitiveProperty),inference(resolution,[status(thm)],[c1283, c84])).
% 3.54/3.71  cnf(c1273,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X569)|icext(X569,uri_owl_Restriction),inference(resolution,[status(thm)],[c1209, c58])).
% 3.54/3.71  cnf(c391,plain,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Resource),inference(resolution,[status(thm)],[c116, c223])).
% 3.54/3.71  cnf(c811,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X568)|iext(X568,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Resource),inference(resolution,[status(thm)],[c391, c32])).
% 3.54/3.71  cnf(c1268,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X567)|icext(X567,uri_owl_Restriction),inference(resolution,[status(thm)],[c1208, c84])).
% 3.54/3.71  cnf(c809,plain,~iext(uri_rdfs_subClassOf,X563,uri_rdfs_ContainerMembershipProperty)|iext(uri_rdfs_subClassOf,X563,uri_rdfs_Resource),inference(resolution,[status(thm)],[c391, c36])).
% 3.54/3.71  cnf(c1252,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X561)|icext(X561,uri_rdf_List),inference(resolution,[status(thm)],[c1159, c58])).
% 3.54/3.71  cnf(c390,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c116, c235])).
% 3.54/3.71  cnf(c803,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X560)|iext(X560,uri_rdfs_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c390, c32])).
% 3.54/3.71  cnf(c1247,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X559)|icext(X559,uri_rdf_List),inference(resolution,[status(thm)],[c1158, c84])).
% 3.54/3.71  cnf(c801,plain,~iext(uri_rdfs_subClassOf,X556,uri_rdfs_Class)|iext(uri_rdfs_subClassOf,X556,uri_rdfs_Resource),inference(resolution,[status(thm)],[c390, c36])).
% 3.54/3.71  cnf(c1229,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X553)|icext(X553,uri_rdfs_Statement),inference(resolution,[status(thm)],[c1121, c58])).
% 3.54/3.71  cnf(c389,plain,iext(uri_rdfs_subClassOf,skolem0001,uri_rdfs_Resource),inference(resolution,[status(thm)],[c116, c236])).
% 3.54/3.71  cnf(c795,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X552)|iext(X552,skolem0001,uri_rdfs_Resource),inference(resolution,[status(thm)],[c389, c32])).
% 3.54/3.71  cnf(c1224,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X551)|icext(X551,uri_rdfs_Statement),inference(resolution,[status(thm)],[c1120, c84])).
% 3.54/3.71  cnf(c793,plain,~iext(uri_rdfs_subClassOf,X549,skolem0001)|iext(uri_rdfs_subClassOf,X549,uri_rdfs_Resource),inference(resolution,[status(thm)],[c389, c36])).
% 3.54/3.71  cnf(c388,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Resource),inference(resolution,[status(thm)],[c116, c218])).
% 3.54/3.71  cnf(c787,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X544)|iext(X544,uri_rdfs_Datatype,uri_rdfs_Resource),inference(resolution,[status(thm)],[c388, c32])).
% 3.54/3.71  cnf(c1198,plain,~iext(uri_rdfs_range,uri_rdf_type,X543)|icext(X543,skolem0001),inference(resolution,[status(thm)],[c1030, c58])).
% 3.54/3.71  cnf(c785,plain,~iext(uri_rdfs_subClassOf,X540,uri_rdfs_Datatype)|iext(uri_rdfs_subClassOf,X540,uri_rdfs_Resource),inference(resolution,[status(thm)],[c388, c36])).
% 3.54/3.71  cnf(c1182,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X539)|icext(X539,uri_rdfs_member),inference(resolution,[status(thm)],[c893, c84])).
% 3.54/3.71  cnf(c387,plain,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Resource),inference(resolution,[status(thm)],[c116, c220])).
% 3.54/3.71  cnf(c779,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X536)|iext(X536,uri_rdf_XMLLiteral,uri_rdfs_Resource),inference(resolution,[status(thm)],[c387, c32])).
% 3.54/3.71  cnf(c777,plain,~iext(uri_rdfs_subClassOf,X532,uri_rdf_XMLLiteral)|iext(uri_rdfs_subClassOf,X532,uri_rdfs_Resource),inference(resolution,[status(thm)],[c387, c36])).
% 3.54/3.71  cnf(c1161,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X531)|icext(X531,uri_rdfs_Resource),inference(resolution,[status(thm)],[c722, c84])).
% 3.54/3.71  cnf(c1153,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X530)|icext(X530,uri_owl_minCardinality),inference(resolution,[status(thm)],[c615, c58])).
% 3.54/3.71  cnf(c386,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Container,uri_rdfs_Resource),inference(resolution,[status(thm)],[c116, c238])).
% 3.54/3.71  cnf(c771,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X529)|iext(X529,uri_rdfs_Container,uri_rdfs_Resource),inference(resolution,[status(thm)],[c386, c32])).
% 3.54/3.71  cnf(c769,plain,~iext(uri_rdfs_subClassOf,X528,uri_rdfs_Container)|iext(uri_rdfs_subClassOf,X528,uri_rdfs_Resource),inference(resolution,[status(thm)],[c386, c36])).
% 3.54/3.71  cnf(c1146,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X527)|icext(X527,uri_owl_minCardinality),inference(resolution,[status(thm)],[c615, c84])).
% 3.54/3.71  cnf(c385,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Resource),inference(resolution,[status(thm)],[c116, c222])).
% 3.54/3.71  cnf(c763,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X524)|iext(X524,uri_rdfs_Seq,uri_rdfs_Resource),inference(resolution,[status(thm)],[c385, c32])).
% 3.54/3.71  cnf(c1136,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X523)|icext(X523,uri_ex_hasAncestor),inference(resolution,[status(thm)],[c613, c58])).
% 3.54/3.71  cnf(c1130,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X522)|icext(X522,uri_ex_hasAncestor),inference(resolution,[status(thm)],[c613, c84])).
% 3.54/3.71  cnf(c761,plain,~iext(uri_rdfs_subClassOf,X520,uri_rdfs_Seq)|iext(uri_rdfs_subClassOf,X520,uri_rdfs_Resource),inference(resolution,[status(thm)],[c385, c36])).
% 3.54/3.71  cnf(c1115,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X518)|icext(X518,uri_owl_onProperty),inference(resolution,[status(thm)],[c611, c58])).
% 3.54/3.71  cnf(c384,plain,iext(uri_rdfs_subClassOf,uri_ex_Person,uri_rdfs_Resource),inference(resolution,[status(thm)],[c116, c219])).
% 3.54/3.71  cnf(c755,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X517)|iext(X517,uri_ex_Person,uri_rdfs_Resource),inference(resolution,[status(thm)],[c384, c32])).
% 3.54/3.71  cnf(c1108,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X516)|icext(X516,uri_owl_onProperty),inference(resolution,[status(thm)],[c611, c84])).
% 3.54/3.71  cnf(c753,plain,~iext(uri_rdfs_subClassOf,X513,uri_ex_Person)|iext(uri_rdfs_subClassOf,X513,uri_rdfs_Resource),inference(resolution,[status(thm)],[c384, c36])).
% 3.54/3.71  cnf(c1098,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X512)|icext(X512,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c609, c58])).
% 3.54/3.71  cnf(c1091,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X511)|icext(X511,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c609, c84])).
% 3.54/3.71  cnf(c383,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Literal,uri_rdfs_Resource),inference(resolution,[status(thm)],[c116, c237])).
% 3.54/3.71  cnf(c747,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X509)|iext(X509,uri_rdfs_Literal,uri_rdfs_Resource),inference(resolution,[status(thm)],[c383, c32])).
% 3.54/3.71  cnf(c1080,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X507)|icext(X507,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c607, c58])).
% 3.54/3.71  cnf(c745,plain,~iext(uri_rdfs_subClassOf,X506,uri_rdfs_Literal)|iext(uri_rdfs_subClassOf,X506,uri_rdfs_Resource),inference(resolution,[status(thm)],[c383, c36])).
% 3.54/3.71  cnf(c1069,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X505)|icext(X505,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c607, c84])).
% 3.54/3.71  cnf(c240,plain,ic(uri_rdf_Property),inference(resolution,[status(thm)],[c46, c104])).
% 3.54/3.71  cnf(c382,plain,iext(uri_rdfs_subClassOf,uri_rdf_Property,uri_rdfs_Resource),inference(resolution,[status(thm)],[c116, c240])).
% 3.54/3.71  cnf(c739,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X502)|iext(X502,uri_rdf_Property,uri_rdfs_Resource),inference(resolution,[status(thm)],[c382, c32])).
% 3.54/3.71  cnf(c1059,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X501)|icext(X501,uri_rdfs_range),inference(resolution,[status(thm)],[c605, c58])).
% 3.54/3.71  cnf(c737,plain,~iext(uri_rdfs_subClassOf,X500,uri_rdf_Property)|iext(uri_rdfs_subClassOf,X500,uri_rdfs_Resource),inference(resolution,[status(thm)],[c382, c36])).
% 3.54/3.71  cnf(c1042,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X499)|icext(X499,uri_rdfs_range),inference(resolution,[status(thm)],[c605, c84])).
% 3.54/3.71  cnf(c381,plain,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Resource),inference(resolution,[status(thm)],[c116, c224])).
% 3.54/3.71  cnf(c731,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X496)|iext(X496,uri_rdf_Bag,uri_rdfs_Resource),inference(resolution,[status(thm)],[c381, c32])).
% 3.54/3.71  cnf(c1027,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X495)|icext(X495,uri_rdfs_domain),inference(resolution,[status(thm)],[c603, c58])).
% 3.54/3.71  cnf(c1008,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X494)|icext(X494,uri_rdfs_domain),inference(resolution,[status(thm)],[c603, c84])).
% 3.54/3.71  cnf(c729,plain,~iext(uri_rdfs_subClassOf,X492,uri_rdf_Bag)|iext(uri_rdfs_subClassOf,X492,uri_rdfs_Resource),inference(resolution,[status(thm)],[c381, c36])).
% 3.54/3.71  cnf(c998,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X490)|icext(X490,uri_rdf_first),inference(resolution,[status(thm)],[c533, c58])).
% 3.54/3.71  cnf(c718,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X489)|iext(X489,uri_rdf_Alt,uri_rdfs_Resource),inference(resolution,[status(thm)],[c380, c32])).
% 3.54/3.71  cnf(c992,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X488)|icext(X488,uri_rdf_first),inference(resolution,[status(thm)],[c533, c84])).
% 3.54/3.71  cnf(c991,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X487)|icext(X487,uri_rdf_rest),inference(resolution,[status(thm)],[c524, c58])).
% 3.54/3.71  cnf(c716,plain,~iext(uri_rdfs_subClassOf,X486,uri_rdf_Alt)|iext(uri_rdfs_subClassOf,X486,uri_rdfs_Resource),inference(resolution,[status(thm)],[c380, c36])).
% 3.54/3.71  cnf(c985,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X485)|icext(X485,uri_rdf_rest),inference(resolution,[status(thm)],[c524, c84])).
% 3.54/3.71  cnf(c983,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X484)|icext(X484,uri_rdf__1),inference(resolution,[status(thm)],[c511, c58])).
% 3.54/3.71  cnf(c262,plain,iext(uri_rdfs_subClassOf,uri_rdf_Property,uri_rdf_Property),inference(resolution,[status(thm)],[c240, c39])).
% 3.54/3.71  cnf(c710,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X482)|iext(X482,uri_rdf_Property,uri_rdf_Property),inference(resolution,[status(thm)],[c262, c32])).
% 3.54/3.71  cnf(c976,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X481)|icext(X481,uri_rdf__2),inference(resolution,[status(thm)],[c509, c58])).
% 3.54/3.71  cnf(c968,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X479)|icext(X479,uri_rdf__3),inference(resolution,[status(thm)],[c496, c58])).
% 3.54/3.71  cnf(c260,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Container,uri_rdfs_Container),inference(resolution,[status(thm)],[c238, c39])).
% 3.54/3.71  cnf(c702,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X473)|iext(X473,uri_rdfs_Container,uri_rdfs_Container),inference(resolution,[status(thm)],[c260, c32])).
% 3.54/3.71  cnf(c946,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X471)|icext(X471,uri_rdf_object),inference(resolution,[status(thm)],[c482, c58])).
% 3.54/3.71  cnf(c940,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X470)|icext(X470,uri_rdf_object),inference(resolution,[status(thm)],[c482, c84])).
% 3.54/3.71  cnf(c939,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X468)|icext(X468,uri_rdf_value),inference(resolution,[status(thm)],[c476, c58])).
% 3.54/3.71  cnf(c933,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X467)|icext(X467,uri_rdf_value),inference(resolution,[status(thm)],[c476, c84])).
% 3.54/3.71  cnf(c251,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Literal,uri_rdfs_Literal),inference(resolution,[status(thm)],[c237, c39])).
% 3.54/3.71  cnf(c694,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X466)|iext(X466,uri_rdfs_Literal,uri_rdfs_Literal),inference(resolution,[status(thm)],[c251, c32])).
% 3.54/3.71  cnf(c932,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X465)|icext(X465,uri_rdf_subject),inference(resolution,[status(thm)],[c475, c58])).
% 3.54/3.71  cnf(c926,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X464)|icext(X464,uri_rdf_subject),inference(resolution,[status(thm)],[c475, c84])).
% 3.54/3.71  cnf(c924,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X462)|icext(X462,uri_rdf_type),inference(resolution,[status(thm)],[c474, c58])).
% 3.54/3.71  cnf(c910,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X461)|icext(X461,uri_rdf_type),inference(resolution,[status(thm)],[c474, c84])).
% 3.54/3.71  cnf(c249,plain,iext(uri_rdfs_subClassOf,skolem0001,skolem0001),inference(resolution,[status(thm)],[c236, c39])).
% 3.54/3.71  cnf(c686,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X459)|iext(X459,skolem0001,skolem0001),inference(resolution,[status(thm)],[c249, c32])).
% 3.54/3.71  cnf(c903,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X458)|icext(X458,uri_rdf__2),inference(resolution,[status(thm)],[c439, c84])).
% 3.54/3.71  cnf(c895,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X456)|icext(X456,uri_rdf__1),inference(resolution,[status(thm)],[c437, c84])).
% 3.54/3.71  cnf(c891,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X454)|icext(X454,uri_rdfs_member),inference(resolution,[status(thm)],[c434, c58])).
% 3.54/3.71  cnf(c885,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X453)|icext(X453,uri_rdf__3),inference(resolution,[status(thm)],[c434, c84])).
% 3.54/3.71  cnf(c247,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c235, c39])).
% 3.54/3.71  cnf(c678,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X452)|iext(X452,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c247, c32])).
% 3.54/3.71  cnf(c245,plain,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdf_Bag),inference(resolution,[status(thm)],[c224, c39])).
% 3.54/3.71  cnf(c670,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X441)|iext(X441,uri_rdf_Bag,uri_rdf_Bag),inference(resolution,[status(thm)],[c245, c32])).
% 3.54/3.71  cnf(c243,plain,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c223, c39])).
% 3.54/3.71  cnf(c662,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X430)|iext(X430,uri_rdfs_ContainerMembershipProperty,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c243, c32])).
% 3.54/3.71  cnf(c821,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X423)|icext(X423,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c405, c84])).
% 3.54/3.71  cnf(c820,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X422)|icext(X422,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c404, c58])).
% 3.54/3.71  cnf(c234,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Seq),inference(resolution,[status(thm)],[c222, c39])).
% 3.54/3.71  cnf(c654,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X421)|iext(X421,uri_rdfs_Seq,uri_rdfs_Seq),inference(resolution,[status(thm)],[c234, c32])).
% 3.54/3.71  cnf(c232,plain,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdf_Alt),inference(resolution,[status(thm)],[c221, c39])).
% 3.54/3.71  cnf(c646,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X410)|iext(X410,uri_rdf_Alt,uri_rdf_Alt),inference(resolution,[status(thm)],[c232, c32])).
% 3.54/3.71  cnf(c230,plain,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c220, c39])).
% 3.54/3.71  cnf(c638,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X399)|iext(X399,uri_rdf_XMLLiteral,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c230, c32])).
% 3.54/3.71  cnf(c720,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X392)|icext(X392,uri_rdfs_Resource),inference(resolution,[status(thm)],[c380, c58])).
% 3.54/3.71  cnf(c228,plain,iext(uri_rdfs_subClassOf,uri_ex_Person,uri_ex_Person),inference(resolution,[status(thm)],[c219, c39])).
% 3.54/3.71  cnf(c630,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X389)|iext(X389,uri_ex_Person,uri_ex_Person),inference(resolution,[status(thm)],[c228, c32])).
% 3.54/3.71  cnf(c705,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X388)|icext(X388,uri_rdf_Property),inference(resolution,[status(thm)],[c262, c84])).
% 3.54/3.71  cnf(c697,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X386)|icext(X386,uri_rdfs_Container),inference(resolution,[status(thm)],[c260, c84])).
% 3.54/3.71  cnf(c689,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X383)|icext(X383,uri_rdfs_Literal),inference(resolution,[status(thm)],[c251, c84])).
% 3.54/3.71  cnf(c226,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c218, c39])).
% 3.54/3.71  cnf(c622,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X381)|iext(X381,uri_rdfs_Datatype,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c226, c32])).
% 3.54/3.71  cnf(c681,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X380)|icext(X380,skolem0001),inference(resolution,[status(thm)],[c249, c84])).
% 3.54/3.71  cnf(c673,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X378)|icext(X378,uri_rdfs_Class),inference(resolution,[status(thm)],[c247, c84])).
% 3.54/3.71  cnf(c672,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X376)|icext(X376,uri_rdf_Bag),inference(resolution,[status(thm)],[c245, c58])).
% 3.54/3.71  cnf(c528,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X374)|iext(X374,uri_rdf_first,uri_rdf_Property),inference(resolution,[status(thm)],[c148, c32])).
% 3.54/3.71  cnf(c664,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X373)|icext(X373,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c243, c58])).
% 3.54/3.71  cnf(c656,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X371)|icext(X371,uri_rdfs_Seq),inference(resolution,[status(thm)],[c234, c58])).
% 3.54/3.71  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.54/3.71  cnf(c147,plain,iext(uri_rdf_type,uri_rdf_nil,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdf_collection_nil_type])).
% 3.54/3.71  cnf(c520,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X370)|iext(X370,uri_rdf_nil,uri_rdf_List),inference(resolution,[status(thm)],[c147, c32])).
% 3.54/3.71  cnf(c648,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X368)|icext(X368,uri_rdf_Alt),inference(resolution,[status(thm)],[c232, c58])).
% 3.54/3.71  cnf(c515,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X366)|iext(X366,uri_rdf_rest,uri_rdf_Property),inference(resolution,[status(thm)],[c146, c32])).
% 3.54/3.71  cnf(c640,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X365)|icext(X365,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c230, c58])).
% 3.54/3.71  cnf(c504,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X363)|iext(X363,uri_rdf__1,uri_rdf_Property),inference(resolution,[status(thm)],[c145, c32])).
% 3.54/3.71  cnf(c632,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X362)|icext(X362,uri_ex_Person),inference(resolution,[status(thm)],[c228, c58])).
% 3.54/3.71  cnf(c624,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X360)|icext(X360,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c226, c58])).
% 3.54/3.71  cnf(c499,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X359)|iext(X359,uri_rdf__2,uri_rdf_Property),inference(resolution,[status(thm)],[c144, c32])).
% 3.54/3.71  cnf(c491,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X355)|iext(X355,uri_rdf__3,uri_rdf_Property),inference(resolution,[status(thm)],[c143, c32])).
% 3.54/3.71  cnf(c522,plain,~iext(uri_rdfs_range,uri_rdf_type,X354)|icext(X354,uri_rdf_List),inference(resolution,[status(thm)],[c147, c58])).
% 3.54/3.71  cnf(c478,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X350)|iext(X350,uri_rdf_object,uri_rdf_Property),inference(resolution,[status(thm)],[c142, c32])).
% 3.54/3.71  cnf(c467,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X345)|iext(X345,uri_rdf_value,uri_rdf_Property),inference(resolution,[status(thm)],[c141, c32])).
% 3.54/3.71  cnf(c462,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X340)|iext(X340,uri_rdf_subject,uri_rdf_Property),inference(resolution,[status(thm)],[c140, c32])).
% 3.54/3.71  cnf(c457,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X335)|iext(X335,uri_rdf_type,uri_rdf_Property),inference(resolution,[status(thm)],[c132, c32])).
% 3.54/3.71  cnf(c459,plain,~iext(uri_rdfs_range,uri_rdf_type,X334)|icext(X334,uri_rdf_Property),inference(resolution,[status(thm)],[c132, c58])).
% 3.54/3.71  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.54/3.71  cnf(c131,plain,iext(uri_rdfs_domain,uri_rdfs_comment,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_comment_domain])).
% 3.54/3.71  cnf(c453,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X331)|iext(X331,uri_rdfs_comment,uri_rdfs_Resource),inference(resolution,[status(thm)],[c131, c32])).
% 3.54/3.71  cnf(c454,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X330)|icext(X330,uri_rdfs_comment),inference(resolution,[status(thm)],[c131, c84])).
% 3.54/3.71  cnf(c450,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X328)|iext(X328,uri_rdfs_comment,uri_rdfs_Literal),inference(resolution,[status(thm)],[c130, c32])).
% 3.54/3.71  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.54/3.71  cnf(c129,plain,iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_domain])).
% 3.54/3.71  cnf(c447,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X327)|iext(X327,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(resolution,[status(thm)],[c129, c32])).
% 3.54/3.71  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.54/3.71  cnf(c128,plain,iext(uri_rdfs_range,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_range])).
% 3.54/3.71  cnf(c444,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X326)|iext(X326,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(resolution,[status(thm)],[c128, c32])).
% 3.54/3.71  fof(simple_ir,axiom,(![X]:ir(X)),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', simple_ir)).
% 3.54/3.71  fof(c152,plain,(![X43]:ir(X43)),inference(variable_rename,[status(thm)],[simple_ir])).
% 3.54/3.71  cnf(c153,plain,ir(X47),inference(split_conjunct,[status(thm)],[c152])).
% 3.54/3.71  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.54/3.71  fof(c67,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.54/3.71  fof(c68,plain,((![X]:(~ir(X)|icext(uri_rdfs_Resource,X)))&(![X]:(~icext(uri_rdfs_Resource,X)|ir(X)))),inference(shift_quantors,[status(thm)],[c67])).
% 3.54/3.71  fof(c70,plain,(![X25]:(![X26]:((~ir(X25)|icext(uri_rdfs_Resource,X25))&(~icext(uri_rdfs_Resource,X26)|ir(X26))))),inference(shift_quantors,[status(thm)],[fof(c69,plain,((![X25]:(~ir(X25)|icext(uri_rdfs_Resource,X25)))&(![X26]:(~icext(uri_rdfs_Resource,X26)|ir(X26)))),inference(variable_rename,[status(thm)],[c68])).])).
% 3.54/3.71  cnf(c71,plain,~ir(X56)|icext(uri_rdfs_Resource,X56),inference(split_conjunct,[status(thm)],[c70])).
% 3.54/3.71  cnf(c161,plain,icext(uri_rdfs_Resource,X57),inference(resolution,[status(thm)],[c71, c153])).
% 3.54/3.71  cnf(c417,plain,iext(uri_rdf_type,X95,uri_rdfs_Resource),inference(resolution,[status(thm)],[c122, c161])).
% 3.54/3.71  cnf(c441,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X321)|iext(X321,X322,uri_rdfs_Resource),inference(resolution,[status(thm)],[c417, c32])).
% 3.54/3.71  cnf(c448,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X320)|icext(X320,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c129, c84])).
% 3.54/3.71  cnf(c445,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X318)|icext(X318,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c128, c84])).
% 3.54/3.71  cnf(c401,plain,~iext(uri_rdfs_subPropertyOf,X317,uri_rdfs_isDefinedBy)|iext(uri_rdfs_subPropertyOf,X317,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c127, c21])).
% 3.54/3.71  cnf(c443,plain,~iext(uri_rdfs_range,uri_rdf_type,X316)|icext(X316,uri_rdfs_Resource),inference(resolution,[status(thm)],[c417, c58])).
% 3.54/3.71  cnf(c403,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X315)|icext(X315,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c127, c58])).
% 3.54/3.71  cnf(c398,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X314)|iext(X314,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c127, c32])).
% 3.54/3.71  cnf(c400,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X313)|icext(X313,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c127, c84])).
% 3.54/3.71  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.54/3.71  cnf(c126,plain,iext(uri_rdfs_domain,uri_rdfs_label,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_label_domain])).
% 3.54/3.71  cnf(c395,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X311)|iext(X311,uri_rdfs_label,uri_rdfs_Resource),inference(resolution,[status(thm)],[c126, c32])).
% 3.54/3.71  cnf(c396,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X310)|icext(X310,uri_rdfs_label),inference(resolution,[status(thm)],[c126, c84])).
% 3.54/3.71  cnf(c394,plain,~iext(uri_rdfs_range,uri_rdfs_range,X309)|icext(X309,uri_rdfs_Literal),inference(resolution,[status(thm)],[c125, c58])).
% 3.54/3.71  cnf(c392,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X308)|iext(X308,uri_rdfs_label,uri_rdfs_Literal),inference(resolution,[status(thm)],[c125, c32])).
% 3.54/3.71  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.54/3.71  cnf(c124,plain,iext(uri_rdfs_domain,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_seealso_domain])).
% 3.54/3.71  cnf(c377,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X306)|iext(X306,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(resolution,[status(thm)],[c124, c32])).
% 3.54/3.71  cnf(c378,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X304)|icext(X304,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c124, c84])).
% 3.54/3.71  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.54/3.71  cnf(c123,plain,iext(uri_rdfs_range,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_seealso_range])).
% 3.54/3.71  cnf(c374,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X302)|iext(X302,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(resolution,[status(thm)],[c123, c32])).
% 3.54/3.71  cnf(c375,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X301)|icext(X301,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c123, c84])).
% 3.54/3.71  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.54/3.71  cnf(c113,plain,iext(uri_rdfs_domain,uri_rdf_first,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdfs_collection_first_domain])).
% 3.54/3.71  cnf(c370,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X299)|iext(X299,uri_rdf_first,uri_rdf_List),inference(resolution,[status(thm)],[c113, c32])).
% 3.54/3.71  cnf(c371,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X298)|icext(X298,uri_rdf_first),inference(resolution,[status(thm)],[c113, c84])).
% 3.54/3.71  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.54/3.71  cnf(c33,plain,iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_subpropertyof_domain])).
% 3.54/3.71  cnf(c361,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X297)|icext(X297,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c84, c33])).
% 3.54/3.71  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.54/3.71  cnf(c98,plain,iext(uri_rdfs_range,uri_rdf__1,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_range_001])).
% 3.54/3.71  cnf(c360,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X296)|icext(X296,uri_rdf__1),inference(resolution,[status(thm)],[c84, c98])).
% 3.54/3.71  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.54/3.71  cnf(c51,plain,iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_reification_predicate_range])).
% 3.54/3.71  cnf(c359,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X295)|icext(X295,uri_rdf_predicate),inference(resolution,[status(thm)],[c84, c51])).
% 3.54/3.71  cnf(c358,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X294)|icext(X294,uri_rdf_type),inference(resolution,[status(thm)],[c84, c17])).
% 3.54/3.71  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.54/3.71  cnf(c16,plain,iext(uri_rdfs_domain,uri_rdf_value,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_value_domain])).
% 3.54/3.71  cnf(c356,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X292)|icext(X292,uri_rdf_value),inference(resolution,[status(thm)],[c84, c16])).
% 3.54/3.71  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.54/3.71  cnf(c18,plain,iext(uri_rdfs_domain,uri_rdf_type,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_type_domain])).
% 3.54/3.71  cnf(c354,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X290)|icext(X290,uri_rdf_type),inference(resolution,[status(thm)],[c84, c18])).
% 3.54/3.71  cnf(c353,plain,~iext(uri_rdfs_domain,uri_owl_minCardinality,X289)|icext(X289,skolem0001),inference(resolution,[status(thm)],[c84, c7])).
% 3.54/3.71  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.54/3.71  cnf(c97,plain,iext(uri_rdfs_range,uri_rdf__2,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_range_002])).
% 3.54/3.71  cnf(c351,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X287)|icext(X287,uri_rdf__2),inference(resolution,[status(thm)],[c84, c97])).
% 3.54/3.71  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.54/3.71  cnf(c49,plain,iext(uri_rdfs_range,uri_rdf_subject,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_reification_subject_range])).
% 3.54/3.71  cnf(c350,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X286)|icext(X286,uri_rdf_subject),inference(resolution,[status(thm)],[c84, c49])).
% 3.54/3.71  cnf(c349,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X285)|icext(X285,uri_rdf_Bag),inference(resolution,[status(thm)],[c84, c108])).
% 3.54/3.71  cnf(c348,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X284)|icext(X284,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c84, c104])).
% 3.54/3.71  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.54/3.71  cnf(c103,plain,iext(uri_rdfs_domain,uri_rdfs_member,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_member_domain])).
% 3.54/3.71  cnf(c347,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X283)|icext(X283,uri_rdfs_member),inference(resolution,[status(thm)],[c84, c103])).
% 3.54/3.71  cnf(c346,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X282)|icext(X282,uri_rdfs_Seq),inference(resolution,[status(thm)],[c84, c92])).
% 3.54/3.71  cnf(c345,plain,~iext(uri_rdfs_domain,uri_ex_hasAncestor,X281)|icext(X281,uri_ex_alice),inference(resolution,[status(thm)],[c84, c10])).
% 3.54/3.71  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.54/3.71  cnf(c100,plain,iext(uri_rdfs_domain,uri_rdf__2,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_002])).
% 3.54/3.71  cnf(c344,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X280)|icext(X280,uri_rdf__2),inference(resolution,[status(thm)],[c84, c100])).
% 3.54/3.71  cnf(c343,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X279)|icext(X279,uri_rdf_Alt),inference(resolution,[status(thm)],[c84, c109])).
% 3.54/3.71  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.54/3.71  cnf(c54,plain,iext(uri_rdfs_domain,uri_rdf_object,uri_rdfs_Statement),inference(split_conjunct,[status(thm)],[rdfs_reification_object_domain])).
% 3.54/3.71  cnf(c341,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X277)|icext(X277,uri_rdf_object),inference(resolution,[status(thm)],[c84, c54])).
% 3.54/3.71  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.54/3.71  cnf(c15,plain,iext(uri_rdfs_range,uri_rdf_value,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_value_range])).
% 3.54/3.71  cnf(c340,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X276)|icext(X276,uri_rdf_value),inference(resolution,[status(thm)],[c84, c15])).
% 3.54/3.71  cnf(c339,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X275)|icext(X275,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c84, c91])).
% 3.54/3.71  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.54/3.71  cnf(c96,plain,iext(uri_rdfs_range,uri_rdf__3,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_range_003])).
% 3.54/3.71  cnf(c337,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X273)|icext(X273,uri_rdf__3),inference(resolution,[status(thm)],[c84, c96])).
% 3.54/3.71  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.54/3.71  cnf(c102,plain,iext(uri_rdfs_range,uri_rdfs_member,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_member_range])).
% 3.54/3.71  cnf(c334,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X270)|icext(X270,uri_rdfs_member),inference(resolution,[status(thm)],[c84, c102])).
% 3.54/3.71  cnf(c331,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X267)|icext(X267,uri_rdfs_range),inference(resolution,[status(thm)],[c84, c55])).
% 3.54/3.71  cnf(c330,plain,~iext(uri_rdfs_domain,uri_owl_onProperty,X266)|icext(X266,skolem0001),inference(resolution,[status(thm)],[c84, c6])).
% 3.54/3.71  cnf(c328,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X264)|icext(X264,uri_rdfs_range),inference(resolution,[status(thm)],[c84, c59])).
% 3.54/3.71  cnf(c327,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X263)|icext(X263,uri_ex_Person),inference(resolution,[status(thm)],[c84, c4])).
% 3.54/3.71  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.54/3.71  cnf(c112,plain,iext(uri_rdfs_range,uri_rdf_first,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_collection_first_range])).
% 3.54/3.71  cnf(c326,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X262)|icext(X262,uri_rdf_first),inference(resolution,[status(thm)],[c84, c112])).
% 3.54/3.71  cnf(c325,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X261)|icext(X261,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c84, c86])).
% 3.54/3.71  cnf(c324,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X260)|icext(X260,uri_rdfs_domain),inference(resolution,[status(thm)],[c84, c79])).
% 3.54/3.71  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.54/3.71  cnf(c101,plain,iext(uri_rdfs_domain,uri_rdf__1,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_001])).
% 3.54/3.71  cnf(c323,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X259)|icext(X259,uri_rdf__1),inference(resolution,[status(thm)],[c84, c101])).
% 3.54/3.71  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.54/3.71  cnf(c99,plain,iext(uri_rdfs_domain,uri_rdf__3,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_003])).
% 3.54/3.71  cnf(c322,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X258)|icext(X258,uri_rdf__3),inference(resolution,[status(thm)],[c84, c99])).
% 3.54/3.71  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.54/3.71  cnf(c111,plain,iext(uri_rdfs_domain,uri_rdf_rest,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdfs_collection_rest_domain])).
% 3.54/3.71  cnf(c321,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X257)|icext(X257,uri_rdf_rest),inference(resolution,[status(thm)],[c84, c111])).
% 3.54/3.71  cnf(c320,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X256)|icext(X256,uri_rdf_rest),inference(resolution,[status(thm)],[c84, c110])).
% 3.54/3.71  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.54/3.71  cnf(c40,plain,iext(uri_rdfs_range,uri_rdfs_subClassOf,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_subclassof_range])).
% 3.54/3.71  cnf(c319,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X255)|icext(X255,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c84, c40])).
% 3.54/3.71  cnf(c318,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X254)|icext(X254,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c84, c25])).
% 3.54/3.71  cnf(c316,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X252)|icext(X252,uri_rdf_subject),inference(resolution,[status(thm)],[c84, c50])).
% 3.54/3.71  cnf(c315,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X251)|icext(X251,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c84, c48])).
% 3.54/3.71  cnf(c314,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X250)|icext(X250,uri_rdfs_domain),inference(factor,[status(thm)],[c84])).
% 3.54/3.71  cnf(c442,plain,~iext(uri_rdfs_domain,uri_rdf_type,X243)|icext(X243,X244),inference(resolution,[status(thm)],[c417, c84])).
% 3.54/3.71  cnf(c303,plain,~iext(uri_rdfs_range,uri_owl_minCardinality,X225)|icext(X225,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger)),inference(resolution,[status(thm)],[c58, c7])).
% 3.54/3.71  cnf(c298,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X201)|icext(X201,uri_rdf_Property),inference(resolution,[status(thm)],[c58, c104])).
% 3.54/3.71  cnf(c295,plain,~iext(uri_rdfs_range,uri_ex_hasAncestor,X197)|icext(X197,uri_ex_bob),inference(resolution,[status(thm)],[c58, c10])).
% 3.54/3.71  cnf(c293,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X195)|icext(X195,uri_rdfs_Container),inference(resolution,[status(thm)],[c58, c109])).
% 3.54/3.71  cnf(c292,plain,~iext(uri_rdfs_range,uri_rdf_type,X194)|icext(X194,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c58, c93])).
% 3.54/3.71  cnf(c289,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X191)|icext(X191,uri_rdfs_Literal),inference(resolution,[status(thm)],[c58, c91])).
% 3.54/3.71  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.54/3.71  cnf(c90,plain,iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Datatype),inference(split_conjunct,[status(thm)],[rdfs_dat_xmlliteral_type])).
% 3.54/3.71  cnf(c286,plain,~iext(uri_rdfs_range,uri_rdf_type,X188)|icext(X188,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c58, c90])).
% 3.54/3.71  cnf(c285,plain,~iext(uri_rdfs_range,uri_rdf_type,X187)|icext(X187,uri_ex_Person),inference(resolution,[status(thm)],[c58, c8])).
% 3.54/3.71  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.54/3.71  cnf(c60,plain,iext(uri_rdf_type,uri_rdf_Property,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_property_type])).
% 3.54/3.71  cnf(c282,plain,~iext(uri_rdfs_range,uri_rdf_type,X184)|icext(X184,uri_rdfs_Class),inference(resolution,[status(thm)],[c58, c60])).
% 3.54/3.71  cnf(c280,plain,~iext(uri_rdfs_range,uri_owl_onProperty,X182)|icext(X182,uri_ex_hasAncestor),inference(resolution,[status(thm)],[c58, c6])).
% 3.54/3.71  cnf(c278,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X180)|icext(X180,uri_rdf_Property),inference(resolution,[status(thm)],[c58, c59])).
% 3.54/3.71  cnf(c277,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X179)|icext(X179,skolem0001),inference(resolution,[status(thm)],[c58, c4])).
% 3.54/3.71  cnf(c276,plain,~iext(uri_rdfs_range,uri_rdfs_range,X178)|icext(X178,uri_rdfs_Resource),inference(resolution,[status(thm)],[c58, c112])).
% 3.54/3.71  cnf(c275,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X177)|icext(X177,uri_rdfs_Class),inference(resolution,[status(thm)],[c58, c86])).
% 3.54/3.71  cnf(c1178,plain,icext(uri_rdf_Property,uri_rdfs_member),inference(resolution,[status(thm)],[c892, c121])).
% 3.54/3.71  cnf(c272,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X174)|icext(X174,uri_rdfs_Resource),inference(resolution,[status(thm)],[c58, c99])).
% 3.54/3.71  cnf(c271,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X173)|icext(X173,uri_rdf_List),inference(resolution,[status(thm)],[c58, c111])).
% 3.54/3.71  cnf(c1141,plain,icext(uri_rdf_Property,uri_owl_minCardinality),inference(resolution,[status(thm)],[c614, c121])).
% 3.54/3.71  cnf(c269,plain,~iext(uri_rdfs_range,uri_rdfs_range,X171)|icext(X171,uri_rdfs_Class),inference(resolution,[status(thm)],[c58, c40])).
% 3.54/3.71  cnf(c268,plain,~iext(uri_rdfs_range,uri_rdfs_range,X170)|icext(X170,uri_rdf_Property),inference(resolution,[status(thm)],[c58, c25])).
% 3.54/3.71  cnf(c1125,plain,icext(uri_rdf_Property,uri_ex_hasAncestor),inference(resolution,[status(thm)],[c612, c121])).
% 3.54/3.71  cnf(c265,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X167)|icext(X167,uri_rdfs_Class),inference(resolution,[status(thm)],[c58, c48])).
% 3.54/3.71  cnf(c1103,plain,icext(uri_rdf_Property,uri_owl_onProperty),inference(resolution,[status(thm)],[c610, c121])).
% 3.54/3.71  cnf(c264,plain,~iext(uri_rdfs_range,uri_rdfs_range,X166)|icext(X166,X166),inference(factor,[status(thm)],[c58])).
% 3.54/3.71  cnf(c258,plain,~icext(uri_rdf_Bag,X165)|icext(uri_rdfs_Container,X165),inference(resolution,[status(thm)],[c47, c108])).
% 3.54/3.71  cnf(c1084,plain,icext(uri_rdf_Property,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c608, c121])).
% 3.54/3.71  cnf(c257,plain,~icext(uri_rdfs_ContainerMembershipProperty,X164)|icext(uri_rdf_Property,X164),inference(resolution,[status(thm)],[c47, c104])).
% 3.54/3.71  cnf(c256,plain,~icext(uri_rdfs_Seq,X163)|icext(uri_rdfs_Container,X163),inference(resolution,[status(thm)],[c47, c92])).
% 3.54/3.71  cnf(c1063,plain,icext(uri_rdf_Property,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c606, c121])).
% 3.54/3.71  cnf(c255,plain,~icext(uri_rdf_Alt,X162)|icext(uri_rdfs_Container,X162),inference(resolution,[status(thm)],[c47, c109])).
% 3.54/3.71  cnf(c1035,plain,icext(uri_rdf_Property,uri_rdfs_range),inference(resolution,[status(thm)],[c604, c121])).
% 3.54/3.71  cnf(c254,plain,~icext(uri_rdf_XMLLiteral,X161)|icext(uri_rdfs_Literal,X161),inference(resolution,[status(thm)],[c47, c91])).
% 3.54/3.71  cnf(c1002,plain,icext(uri_rdf_Property,uri_rdfs_domain),inference(resolution,[status(thm)],[c602, c121])).
% 3.54/3.71  cnf(c252,plain,~icext(uri_rdfs_Datatype,X159)|icext(uri_rdfs_Class,X159),inference(resolution,[status(thm)],[c47, c86])).
% 3.54/3.71  cnf(c217,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X158)|iext(X158,uri_rdf_first,uri_rdfs_Resource),inference(resolution,[status(thm)],[c112, c32])).
% 3.54/3.71  cnf(c216,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X157)|iext(X157,uri_rdf_rest,uri_rdf_List),inference(resolution,[status(thm)],[c111, c32])).
% 3.54/3.71  cnf(c215,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X156)|iext(X156,uri_rdf_rest,uri_rdf_List),inference(resolution,[status(thm)],[c110, c32])).
% 3.54/3.71  cnf(c214,plain,~iext(uri_rdfs_subClassOf,X155,uri_rdf_Alt)|iext(uri_rdfs_subClassOf,X155,uri_rdfs_Container),inference(resolution,[status(thm)],[c109, c36])).
% 3.54/3.71  cnf(c213,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X154)|iext(X154,uri_rdf_Alt,uri_rdfs_Container),inference(resolution,[status(thm)],[c109, c32])).
% 3.54/3.71  cnf(c212,plain,~iext(uri_rdfs_subClassOf,X153,uri_rdf_Bag)|iext(uri_rdfs_subClassOf,X153,uri_rdfs_Container),inference(resolution,[status(thm)],[c108, c36])).
% 3.54/3.71  cnf(c211,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X152)|iext(X152,uri_rdf_Bag,uri_rdfs_Container),inference(resolution,[status(thm)],[c108, c32])).
% 3.54/3.71  cnf(c958,plain,icext(uri_rdf_Property,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c486, c121])).
% 3.54/3.71  cnf(c210,plain,~iext(uri_rdfs_subClassOf,X151,uri_rdfs_ContainerMembershipProperty)|iext(uri_rdfs_subClassOf,X151,uri_rdf_Property),inference(resolution,[status(thm)],[c104, c36])).
% 3.54/3.71  cnf(c950,plain,icext(uri_rdf_Property,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c483, c121])).
% 3.54/3.71  cnf(c209,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X150)|iext(X150,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),inference(resolution,[status(thm)],[c104, c32])).
% 3.54/3.71  cnf(c208,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X149)|iext(X149,uri_rdfs_member,uri_rdfs_Resource),inference(resolution,[status(thm)],[c103, c32])).
% 3.54/3.71  cnf(c207,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X148)|iext(X148,uri_rdfs_member,uri_rdfs_Resource),inference(resolution,[status(thm)],[c102, c32])).
% 3.54/3.71  cnf(c206,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X147)|iext(X147,uri_rdf__1,uri_rdfs_Resource),inference(resolution,[status(thm)],[c101, c32])).
% 3.54/3.71  cnf(c205,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X146)|iext(X146,uri_rdf__2,uri_rdfs_Resource),inference(resolution,[status(thm)],[c100, c32])).
% 3.54/3.71  cnf(c204,plain,~iext(uri_rdfs_subClassOf,X145,uri_rdfs_Seq)|iext(uri_rdfs_subClassOf,X145,uri_rdfs_Container),inference(resolution,[status(thm)],[c36, c92])).
% 3.54/3.71  cnf(c203,plain,~iext(uri_rdfs_subClassOf,X144,uri_rdf_XMLLiteral)|iext(uri_rdfs_subClassOf,X144,uri_rdfs_Literal),inference(resolution,[status(thm)],[c36, c91])).
% 3.54/3.71  cnf(c202,plain,~iext(uri_rdfs_subClassOf,X143,uri_ex_Person)|iext(uri_rdfs_subClassOf,X143,skolem0001),inference(resolution,[status(thm)],[c36, c4])).
% 3.54/3.71  cnf(c201,plain,~iext(uri_rdfs_subClassOf,X142,uri_rdfs_Datatype)|iext(uri_rdfs_subClassOf,X142,uri_rdfs_Class),inference(resolution,[status(thm)],[c36, c86])).
% 3.54/3.71  cnf(c199,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X140)|iext(X140,uri_rdf__3,uri_rdfs_Resource),inference(resolution,[status(thm)],[c99, c32])).
% 3.54/3.71  cnf(c198,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X139)|iext(X139,uri_rdf__1,uri_rdfs_Resource),inference(resolution,[status(thm)],[c98, c32])).
% 3.54/3.71  cnf(c197,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X138)|iext(X138,uri_rdf__2,uri_rdfs_Resource),inference(resolution,[status(thm)],[c97, c32])).
% 3.54/3.72  cnf(c196,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X137)|iext(X137,uri_rdf__3,uri_rdfs_Resource),inference(resolution,[status(thm)],[c96, c32])).
% 3.54/3.72  cnf(c195,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X136)|iext(X136,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c95, c32])).
% 3.54/3.72  cnf(c194,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X135)|iext(X135,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c32, c33])).
% 3.54/3.72  cnf(c193,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X134)|iext(X134,uri_rdf_predicate,uri_rdfs_Resource),inference(resolution,[status(thm)],[c32, c51])).
% 3.54/3.72  cnf(c192,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X133)|iext(X133,uri_rdf_type,uri_rdfs_Class),inference(resolution,[status(thm)],[c32, c17])).
% 3.54/3.72  cnf(c191,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X132)|iext(X132,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c32, c94])).
% 3.54/3.72  cnf(c190,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X131)|iext(X131,uri_rdf_value,uri_rdfs_Resource),inference(resolution,[status(thm)],[c32, c16])).
% 3.54/3.72  cnf(c189,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X130)|iext(X130,uri_rdf_type,uri_rdfs_Resource),inference(resolution,[status(thm)],[c32, c18])).
% 3.54/3.72  cnf(c188,plain,~iext(uri_rdfs_subPropertyOf,uri_owl_minCardinality,X129)|iext(X129,skolem0001,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger)),inference(resolution,[status(thm)],[c32, c7])).
% 3.54/3.72  cnf(c187,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X128)|iext(X128,uri_ex_hasAncestor,uri_owl_TransitiveProperty),inference(resolution,[status(thm)],[c32, c3])).
% 3.54/3.72  cnf(c186,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X127)|iext(X127,uri_rdf_subject,uri_rdfs_Resource),inference(resolution,[status(thm)],[c32, c49])).
% 3.54/3.72  cnf(c185,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X126)|iext(X126,uri_rdfs_Seq,uri_rdfs_Container),inference(resolution,[status(thm)],[c32, c92])).
% 3.54/3.72  cnf(c184,plain,~iext(uri_rdfs_subPropertyOf,uri_ex_hasAncestor,X125)|iext(X125,uri_ex_alice,uri_ex_bob),inference(resolution,[status(thm)],[c32, c10])).
% 3.54/3.72  cnf(c183,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X124)|iext(X124,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c32, c93])).
% 3.54/3.72  cnf(c182,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X123)|iext(X123,uri_rdf_object,uri_rdfs_Statement),inference(resolution,[status(thm)],[c32, c54])).
% 3.54/3.72  cnf(c181,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X122)|iext(X122,uri_rdf_value,uri_rdfs_Resource),inference(resolution,[status(thm)],[c32, c15])).
% 3.54/3.72  cnf(c180,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X121)|iext(X121,uri_rdf_XMLLiteral,uri_rdfs_Literal),inference(resolution,[status(thm)],[c32, c91])).
% 3.54/3.72  cnf(c179,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X120)|iext(X120,uri_ex_bob,uri_ex_Person),inference(resolution,[status(thm)],[c32, c9])).
% 3.54/3.72  cnf(c178,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X119)|iext(X119,uri_rdf_XMLLiteral,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c32, c90])).
% 3.54/3.72  cnf(c177,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X118)|iext(X118,uri_ex_alice,uri_ex_Person),inference(resolution,[status(thm)],[c32, c8])).
% 3.54/3.72  cnf(c176,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X117)|iext(X117,skolem0001,uri_owl_Restriction),inference(resolution,[status(thm)],[c32, c5])).
% 3.54/3.72  cnf(c175,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X116)|iext(X116,uri_rdf_Property,uri_rdfs_Class),inference(resolution,[status(thm)],[c32, c60])).
% 3.54/3.72  cnf(c174,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X115)|iext(X115,uri_rdfs_range,uri_rdfs_Class),inference(resolution,[status(thm)],[c32, c55])).
% 3.54/3.72  cnf(c173,plain,~iext(uri_rdfs_subPropertyOf,uri_owl_onProperty,X114)|iext(X114,skolem0001,uri_ex_hasAncestor),inference(resolution,[status(thm)],[c32, c6])).
% 3.54/3.72  cnf(c527,plain,icext(uri_rdf_Property,uri_rdf_first),inference(resolution,[status(thm)],[c148, c121])).
% 3.54/3.72  cnf(c172,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X113)|iext(X113,uri_rdfs_domain,uri_rdf_Property),inference(resolution,[status(thm)],[c32, c85])).
% 3.54/3.72  cnf(c171,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X112)|iext(X112,uri_rdfs_range,uri_rdf_Property),inference(resolution,[status(thm)],[c32, c59])).
% 3.54/3.72  cnf(c170,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X111)|iext(X111,uri_ex_Person,skolem0001),inference(resolution,[status(thm)],[c32, c4])).
% 3.54/3.72  cnf(c169,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X110)|iext(X110,uri_rdfs_Datatype,uri_rdfs_Class),inference(resolution,[status(thm)],[c32, c86])).
% 3.54/3.72  cnf(c168,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X109)|iext(X109,uri_rdfs_domain,uri_rdfs_Class),inference(resolution,[status(thm)],[c32, c79])).
% 3.54/3.72  cnf(c167,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X108)|iext(X108,uri_rdfs_subClassOf,uri_rdfs_Class),inference(resolution,[status(thm)],[c32, c40])).
% 3.54/3.72  cnf(c166,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X107)|iext(X107,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c32, c25])).
% 3.54/3.72  cnf(c165,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X106)|iext(X106,uri_rdf_predicate,uri_rdfs_Statement),inference(resolution,[status(thm)],[c32, c52])).
% 3.54/3.72  cnf(c164,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X105)|iext(X105,uri_rdf_subject,uri_rdfs_Statement),inference(resolution,[status(thm)],[c32, c50])).
% 3.54/3.72  cnf(c163,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X104)|iext(X104,uri_rdfs_subClassOf,uri_rdfs_Class),inference(resolution,[status(thm)],[c32, c48])).
% 3.54/3.72  cnf(c162,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X103)|iext(X103,uri_rdfs_subPropertyOf,X103),inference(factor,[status(thm)],[c32])).
% 3.54/3.72  fof(testcase_conclusion_fullish_024_Cardinality_Restrictions_on_Complex_Properties,conjecture,(?[BNODE_x]:(iext(uri_ex_hasAncestor,uri_ex_bob,BNODE_x)&iext(uri_ex_hasAncestor,uri_ex_alice,BNODE_x))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', testcase_conclusion_fullish_024_Cardinality_Restrictions_on_Complex_Properties)).
% 3.54/3.72  fof(c11,negated_conjecture,(~(?[BNODE_x]:(iext(uri_ex_hasAncestor,uri_ex_bob,BNODE_x)&iext(uri_ex_hasAncestor,uri_ex_alice,BNODE_x)))),inference(assume_negation,[status(cth)],[testcase_conclusion_fullish_024_Cardinality_Restrictions_on_Complex_Properties])).
% 3.54/3.72  fof(c12,negated_conjecture,(![BNODE_x]:(~iext(uri_ex_hasAncestor,uri_ex_bob,BNODE_x)|~iext(uri_ex_hasAncestor,uri_ex_alice,BNODE_x))),inference(fof_nnf,[status(thm)],[c11])).
% 3.54/3.72  fof(c13,negated_conjecture,(![X3]:(~iext(uri_ex_hasAncestor,uri_ex_bob,X3)|~iext(uri_ex_hasAncestor,uri_ex_alice,X3))),inference(variable_rename,[status(thm)],[c12])).
% 3.54/3.72  cnf(c14,negated_conjecture,~iext(uri_ex_hasAncestor,uri_ex_bob,X49)|~iext(uri_ex_hasAncestor,uri_ex_alice,X49),inference(split_conjunct,[status(thm)],[c13])).
% 3.54/3.72  cnf(c159,plain,~iext(uri_ex_hasAncestor,uri_ex_bob,uri_ex_bob),inference(resolution,[status(thm)],[c14, c10])).
% 3.54/3.72  cnf(c519,plain,icext(uri_rdf_List,uri_rdf_nil),inference(resolution,[status(thm)],[c147, c121])).
% 3.54/3.72  cnf(c514,plain,icext(uri_rdf_Property,uri_rdf_rest),inference(resolution,[status(thm)],[c146, c121])).
% 3.54/3.72  cnf(c503,plain,icext(uri_rdf_Property,uri_rdf__1),inference(resolution,[status(thm)],[c145, c121])).
% 3.54/3.72  cnf(c498,plain,icext(uri_rdf_Property,uri_rdf__2),inference(resolution,[status(thm)],[c144, c121])).
% 3.54/3.72  cnf(c490,plain,icext(uri_rdf_Property,uri_rdf__3),inference(resolution,[status(thm)],[c143, c121])).
% 3.54/3.72  cnf(c477,plain,icext(uri_rdf_Property,uri_rdf_object),inference(resolution,[status(thm)],[c142, c121])).
% 3.54/3.72  cnf(c466,plain,icext(uri_rdf_Property,uri_rdf_value),inference(resolution,[status(thm)],[c141, c121])).
% 3.54/3.72  cnf(c461,plain,icext(uri_rdf_Property,uri_rdf_subject),inference(resolution,[status(thm)],[c140, c121])).
% 3.54/3.72  cnf(c456,plain,icext(uri_rdf_Property,uri_rdf_type),inference(resolution,[status(thm)],[c132, c121])).
% 3.54/3.72  cnf(c412,plain,icext(uri_owl_TransitiveProperty,uri_ex_hasAncestor),inference(resolution,[status(thm)],[c121, c3])).
% 3.54/3.72  cnf(c409,plain,icext(uri_rdfs_Datatype,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c121, c90])).
% 3.54/3.72  cnf(c407,plain,icext(uri_owl_Restriction,skolem0001),inference(resolution,[status(thm)],[c121, c5])).
% 3.54/3.72  cnf(c261,plain,icext(uri_rdfs_Class,uri_rdf_Property),inference(resolution,[status(thm)],[c240, c77])).
% 3.54/3.72  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.54/3.72  fof(c87,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.54/3.72  fof(c88,plain,(![X33]:(~icext(uri_rdfs_Datatype,X33)|iext(uri_rdfs_subClassOf,X33,uri_rdfs_Literal))),inference(variable_rename,[status(thm)],[c87])).
% 3.54/3.72  cnf(c89,plain,~icext(uri_rdfs_Datatype,X88)|iext(uri_rdfs_subClassOf,X88,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[c88])).
% 3.54/3.72  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.54/3.72  fof(c61,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.54/3.72  fof(c62,plain,((![X]:(~lv(X)|icext(uri_rdfs_Literal,X)))&(![X]:(~icext(uri_rdfs_Literal,X)|lv(X)))),inference(shift_quantors,[status(thm)],[c61])).
% 3.54/3.72  fof(c64,plain,(![X23]:(![X24]:((~lv(X23)|icext(uri_rdfs_Literal,X23))&(~icext(uri_rdfs_Literal,X24)|lv(X24))))),inference(shift_quantors,[status(thm)],[fof(c63,plain,((![X23]:(~lv(X23)|icext(uri_rdfs_Literal,X23)))&(![X24]:(~icext(uri_rdfs_Literal,X24)|lv(X24)))),inference(variable_rename,[status(thm)],[c62])).])).
% 3.54/3.72  cnf(c66,plain,~icext(uri_rdfs_Literal,X55)|lv(X55),inference(split_conjunct,[status(thm)],[c64])).
% 3.54/3.72  cnf(c65,plain,~lv(X54)|icext(uri_rdfs_Literal,X54),inference(split_conjunct,[status(thm)],[c64])).
% 3.54/3.72  % SZS output end Saturation
% 3.54/3.72  
% 3.54/3.72  % Initial clauses    : 98
% 3.54/3.72  % Processed clauses  : 610
% 3.54/3.72  % Factors computed   : 5
% 3.54/3.72  % Resolvents computed: 1443
% 3.54/3.72  % Tautologies deleted: 58
% 3.54/3.72  % Forward subsumed   : 878
% 3.54/3.72  % Backward subsumed  : 1
% 3.54/3.72  % -------- CPU Time ---------
% 3.54/3.72  % User time          : 3.355 s
% 3.54/3.72  % System time        : 0.015 s
% 3.54/3.72  % Total time         : 3.370 s
%------------------------------------------------------------------------------