PyRes---1.5.CSA-Sat.s

%------------------------------------------------------------------------------
% File     : PyRes---1.5
% Problem  : SWB013+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:48 EDT 2024

% Result   : CounterSatisfiable 4.55s 4.75s
% Output   : Saturation 4.55s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12  % Problem  : SWB013+4 : TPTP v8.1.2. Released v5.2.0.
% 0.11/0.13  % Command  : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.33  % Computer : n020.cluster.edu
% 0.13/0.33  % Model    : x86_64 x86_64
% 0.13/0.33  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33  % Memory   : 8042.1875MB
% 0.13/0.33  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33  % CPULimit : 300
% 0.13/0.33  % WCLimit  : 300
% 0.13/0.33  % DateTime : Wed May  8 22:02:38 EDT 2024
% 0.13/0.33  % CPUTime  : 
% 4.55/4.75  % Version:  1.5
% 4.55/4.75  % SZS status CounterSatisfiable
% 4.55/4.75  % SZS output start Saturation
% 4.55/4.75  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)).
% 4.55/4.75  fof(c36,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])).
% 4.55/4.75  fof(c38,plain,(![X11]:(![X12]:(![X13]:(![X14]:(~iext(uri_rdfs_subPropertyOf,X11,X12)|((ip(X11)&ip(X12))&(~iext(X11,X13,X14)|iext(X12,X13,X14)))))))),inference(shift_quantors,[status(thm)],[fof(c37,plain,(![X11]:(![X12]:(~iext(uri_rdfs_subPropertyOf,X11,X12)|((ip(X11)&ip(X12))&(![X13]:(![X14]:(~iext(X11,X13,X14)|iext(X12,X13,X14)))))))),inference(variable_rename,[status(thm)],[c36])).])).
% 4.55/4.75  fof(c39,plain,(![X11]:(![X12]:(![X13]:(![X14]:(((~iext(uri_rdfs_subPropertyOf,X11,X12)|ip(X11))&(~iext(uri_rdfs_subPropertyOf,X11,X12)|ip(X12)))&(~iext(uri_rdfs_subPropertyOf,X11,X12)|(~iext(X11,X13,X14)|iext(X12,X13,X14)))))))),inference(distribute,[status(thm)],[c38])).
% 4.55/4.75  cnf(c42,plain,~iext(uri_rdfs_subPropertyOf,X67,X70)|~iext(X67,X69,X68)|iext(X70,X69,X68),inference(split_conjunct,[status(thm)],[c39])).
% 4.55/4.75  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)).
% 4.55/4.75  fof(c32,plain,(![P]:(~ip(P)|iext(uri_rdfs_subPropertyOf,P,P))),inference(fof_nnf,[status(thm)],[rdfs_subpropertyof_reflex])).
% 4.55/4.75  fof(c33,plain,(![X10]:(~ip(X10)|iext(uri_rdfs_subPropertyOf,X10,X10))),inference(variable_rename,[status(thm)],[c32])).
% 4.55/4.75  cnf(c34,plain,~ip(X55)|iext(uri_rdfs_subPropertyOf,X55,X55),inference(split_conjunct,[status(thm)],[c33])).
% 4.55/4.75  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)).
% 4.55/4.75  fof(c144,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])).
% 4.55/4.75  fof(c145,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)],[c144])).
% 4.55/4.75  fof(c147,plain,(![X43]:(![X44]:((~iext(uri_rdf_type,X43,uri_rdf_Property)|ip(X43))&(~ip(X44)|iext(uri_rdf_type,X44,uri_rdf_Property))))),inference(shift_quantors,[status(thm)],[fof(c146,plain,((![X43]:(~iext(uri_rdf_type,X43,uri_rdf_Property)|ip(X43)))&(![X44]:(~ip(X44)|iext(uri_rdf_type,X44,uri_rdf_Property)))),inference(variable_rename,[status(thm)],[c145])).])).
% 4.55/4.75  cnf(c148,plain,~iext(uri_rdf_type,X99,uri_rdf_Property)|ip(X99),inference(split_conjunct,[status(thm)],[c147])).
% 4.55/4.75  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)).
% 4.55/4.75  fof(c127,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])).
% 4.55/4.75  fof(c128,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)],[c127])).
% 4.55/4.75  fof(c130,plain,(![X39]:(![X40]:(![X41]:(![X42]:((~iext(uri_rdf_type,X39,X40)|icext(X40,X39))&(~icext(X42,X41)|iext(uri_rdf_type,X41,X42))))))),inference(shift_quantors,[status(thm)],[fof(c129,plain,((![X39]:(![X40]:(~iext(uri_rdf_type,X39,X40)|icext(X40,X39))))&(![X41]:(![X42]:(~icext(X42,X41)|iext(uri_rdf_type,X41,X42))))),inference(variable_rename,[status(thm)],[c128])).])).
% 4.55/4.75  cnf(c132,plain,~icext(X96,X95)|iext(uri_rdf_type,X95,X96),inference(split_conjunct,[status(thm)],[c130])).
% 4.55/4.75  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)).
% 4.55/4.75  cnf(c69,plain,iext(uri_rdfs_domain,uri_rdfs_range,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_range_domain])).
% 4.55/4.75  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)).
% 4.55/4.75  fof(c90,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])).
% 4.55/4.75  fof(c91,plain,(![P]:(![C]:(![X]:((~iext(uri_rdfs_domain,P,C)|(![Y]:~iext(P,X,Y)))|icext(C,X))))),inference(shift_quantors,[status(thm)],[c90])).
% 4.55/4.75  fof(c93,plain,(![X32]:(![X33]:(![X34]:(![X35]:((~iext(uri_rdfs_domain,X32,X33)|~iext(X32,X34,X35))|icext(X33,X34)))))),inference(shift_quantors,[status(thm)],[fof(c92,plain,(![X32]:(![X33]:(![X34]:((~iext(uri_rdfs_domain,X32,X33)|(![X35]:~iext(X32,X34,X35)))|icext(X33,X34))))),inference(variable_rename,[status(thm)],[c91])).])).
% 4.55/4.75  cnf(c94,plain,~iext(uri_rdfs_domain,X86,X89)|~iext(X86,X87,X88)|icext(X89,X87),inference(split_conjunct,[status(thm)],[c93])).
% 4.55/4.75  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)).
% 4.55/4.75  cnf(c140,plain,iext(uri_rdfs_range,uri_rdfs_comment,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[rdfs_annotation_comment_range])).
% 4.55/4.75  cnf(c502,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X363)|icext(X363,uri_rdfs_comment),inference(resolution,[status(thm)],[c140, c94])).
% 4.55/4.75  cnf(c1595,plain,icext(uri_rdf_Property,uri_rdfs_comment),inference(resolution,[status(thm)],[c502, c69])).
% 4.55/4.75  cnf(c1596,plain,iext(uri_rdf_type,uri_rdfs_comment,uri_rdf_Property),inference(resolution,[status(thm)],[c1595, c132])).
% 4.55/4.75  cnf(c1600,plain,ip(uri_rdfs_comment),inference(resolution,[status(thm)],[c1596, c148])).
% 4.55/4.75  cnf(c1605,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_comment,uri_rdfs_comment),inference(resolution,[status(thm)],[c1600, c34])).
% 4.55/4.75  cnf(c1613,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X776)|iext(X776,uri_rdfs_comment,uri_rdfs_comment),inference(resolution,[status(thm)],[c1605, c42])).
% 4.55/4.75  cnf(c1601,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X774)|iext(X774,uri_rdfs_comment,uri_rdf_Property),inference(resolution,[status(thm)],[c1596, c42])).
% 4.55/4.75  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)).
% 4.55/4.75  cnf(c135,plain,iext(uri_rdfs_range,uri_rdfs_label,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[rdfs_annotation_label_range])).
% 4.55/4.75  cnf(c440,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X346)|icext(X346,uri_rdfs_label),inference(resolution,[status(thm)],[c135, c94])).
% 4.55/4.75  cnf(c1565,plain,icext(uri_rdf_Property,uri_rdfs_label),inference(resolution,[status(thm)],[c440, c69])).
% 4.55/4.75  cnf(c1567,plain,iext(uri_rdf_type,uri_rdfs_label,uri_rdf_Property),inference(resolution,[status(thm)],[c1565, c132])).
% 4.55/4.75  cnf(c1571,plain,ip(uri_rdfs_label),inference(resolution,[status(thm)],[c1567, c148])).
% 4.55/4.75  cnf(c1575,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_label,uri_rdfs_label),inference(resolution,[status(thm)],[c1571, c34])).
% 4.55/4.75  cnf(c1583,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X773)|iext(X773,uri_rdfs_label,uri_rdfs_label),inference(resolution,[status(thm)],[c1575, c42])).
% 4.55/4.75  cnf(c1572,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X771)|iext(X771,uri_rdfs_label,uri_rdf_Property),inference(resolution,[status(thm)],[c1567, c42])).
% 4.55/4.75  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)).
% 4.55/4.75  fof(c44,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])).
% 4.55/4.75  fof(c45,plain,(![X15]:(![X16]:(![X17]:((~iext(uri_rdfs_subClassOf,X15,X16)|~iext(uri_rdfs_subClassOf,X16,X17))|iext(uri_rdfs_subClassOf,X15,X17))))),inference(variable_rename,[status(thm)],[c44])).
% 4.55/4.75  cnf(c46,plain,~iext(uri_rdfs_subClassOf,X73,X72)|~iext(uri_rdfs_subClassOf,X72,X71)|iext(uri_rdfs_subClassOf,X73,X71),inference(split_conjunct,[status(thm)],[c45])).
% 4.55/4.75  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)).
% 4.55/4.75  fof(c124,plain,(![C]:(~ic(C)|iext(uri_rdfs_subClassOf,C,uri_rdfs_Resource))),inference(fof_nnf,[status(thm)],[rdfs_class_instsub_resource])).
% 4.55/4.75  fof(c125,plain,(![X38]:(~ic(X38)|iext(uri_rdfs_subClassOf,X38,uri_rdfs_Resource))),inference(variable_rename,[status(thm)],[c124])).
% 4.55/4.75  cnf(c126,plain,~ic(X92)|iext(uri_rdfs_subClassOf,X92,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[c125])).
% 4.55/4.75  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)).
% 4.55/4.75  fof(c83,plain,(![X]:((~ic(X)|icext(uri_rdfs_Class,X))&(~icext(uri_rdfs_Class,X)|ic(X)))),inference(fof_nnf,[status(thm)],[rdfs_ic_def])).
% 4.55/4.75  fof(c84,plain,((![X]:(~ic(X)|icext(uri_rdfs_Class,X)))&(![X]:(~icext(uri_rdfs_Class,X)|ic(X)))),inference(shift_quantors,[status(thm)],[c83])).
% 4.55/4.75  fof(c86,plain,(![X30]:(![X31]:((~ic(X30)|icext(uri_rdfs_Class,X30))&(~icext(uri_rdfs_Class,X31)|ic(X31))))),inference(shift_quantors,[status(thm)],[fof(c85,plain,((![X30]:(~ic(X30)|icext(uri_rdfs_Class,X30)))&(![X31]:(~icext(uri_rdfs_Class,X31)|ic(X31)))),inference(variable_rename,[status(thm)],[c84])).])).
% 4.55/4.75  cnf(c88,plain,~icext(uri_rdfs_Class,X66)|ic(X66),inference(split_conjunct,[status(thm)],[c86])).
% 4.55/4.75  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)).
% 4.55/4.75  cnf(c65,plain,iext(uri_rdfs_range,uri_rdfs_range,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_range_range])).
% 4.55/4.75  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)).
% 4.55/4.75  fof(c66,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])).
% 4.55/4.75  fof(c67,plain,(![X22]:(![X23]:(![X24]:(![X25]:((~iext(uri_rdfs_range,X22,X23)|~iext(X22,X24,X25))|icext(X23,X25)))))),inference(variable_rename,[status(thm)],[c66])).
% 4.55/4.75  cnf(c68,plain,~iext(uri_rdfs_range,X82,X85)|~iext(X82,X83,X84)|icext(X85,X84),inference(split_conjunct,[status(thm)],[c67])).
% 4.55/4.75  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)).
% 4.55/4.75  cnf(c120,plain,iext(uri_rdfs_range,uri_rdf_rest,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdfs_collection_rest_range])).
% 4.55/4.75  cnf(c411,plain,~iext(uri_rdfs_range,uri_rdfs_range,X325)|icext(X325,uri_rdf_List),inference(resolution,[status(thm)],[c120, c68])).
% 4.55/4.75  cnf(c1524,plain,icext(uri_rdfs_Class,uri_rdf_List),inference(resolution,[status(thm)],[c411, c65])).
% 4.55/4.75  cnf(c1525,plain,ic(uri_rdf_List),inference(resolution,[status(thm)],[c1524, c88])).
% 4.55/4.75  cnf(c1530,plain,iext(uri_rdfs_subClassOf,uri_rdf_List,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1525, c126])).
% 4.55/4.75  cnf(c1553,plain,~iext(uri_rdfs_subClassOf,X770,uri_rdf_List)|iext(uri_rdfs_subClassOf,X770,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1530, c46])).
% 4.55/4.75  cnf(c1552,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X769)|iext(X769,uri_rdf_List,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1530, c42])).
% 4.55/4.75  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)).
% 4.55/4.75  fof(c47,plain,(![C]:(~ic(C)|iext(uri_rdfs_subClassOf,C,C))),inference(fof_nnf,[status(thm)],[rdfs_subclassof_reflex])).
% 4.55/4.75  fof(c48,plain,(![X18]:(~ic(X18)|iext(uri_rdfs_subClassOf,X18,X18))),inference(variable_rename,[status(thm)],[c47])).
% 4.55/4.75  cnf(c49,plain,~ic(X74)|iext(uri_rdfs_subClassOf,X74,X74),inference(split_conjunct,[status(thm)],[c48])).
% 4.55/4.75  cnf(c1529,plain,iext(uri_rdfs_subClassOf,uri_rdf_List,uri_rdf_List),inference(resolution,[status(thm)],[c1525, c49])).
% 4.55/4.75  cnf(c1543,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X767)|iext(X767,uri_rdf_List,uri_rdf_List),inference(resolution,[status(thm)],[c1529, c42])).
% 4.55/4.75  cnf(c1526,plain,iext(uri_rdf_type,uri_rdf_List,uri_rdfs_Class),inference(resolution,[status(thm)],[c1524, c132])).
% 4.55/4.75  cnf(c1534,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X766)|iext(X766,uri_rdf_List,uri_rdfs_Class),inference(resolution,[status(thm)],[c1526, c42])).
% 4.55/4.75  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)).
% 4.55/4.75  cnf(c95,plain,iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_domain_domain])).
% 4.55/4.75  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)).
% 4.55/4.75  cnf(c62,plain,iext(uri_rdfs_domain,uri_rdf_predicate,uri_rdfs_Statement),inference(split_conjunct,[status(thm)],[rdfs_reification_predicate_domain])).
% 4.55/4.75  cnf(c342,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X283)|icext(X283,uri_rdf_predicate),inference(resolution,[status(thm)],[c94, c62])).
% 4.55/4.75  cnf(c1477,plain,icext(uri_rdf_Property,uri_rdf_predicate),inference(resolution,[status(thm)],[c342, c95])).
% 4.55/4.75  cnf(c1478,plain,iext(uri_rdf_type,uri_rdf_predicate,uri_rdf_Property),inference(resolution,[status(thm)],[c1477, c132])).
% 4.55/4.75  cnf(c1482,plain,ip(uri_rdf_predicate),inference(resolution,[status(thm)],[c1478, c148])).
% 4.55/4.75  cnf(c1486,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_predicate,uri_rdf_predicate),inference(resolution,[status(thm)],[c1482, c34])).
% 4.55/4.75  cnf(c1494,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X765)|iext(X765,uri_rdf_predicate,uri_rdf_predicate),inference(resolution,[status(thm)],[c1486, c42])).
% 4.55/4.75  cnf(c1483,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X763)|iext(X763,uri_rdf_predicate,uri_rdf_Property),inference(resolution,[status(thm)],[c1478, c42])).
% 4.55/4.75  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)).
% 4.55/4.75  cnf(c121,plain,iext(uri_rdfs_domain,uri_rdf_rest,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdfs_collection_rest_domain])).
% 4.55/4.75  fof(testcase_premise_fullish_013_Cliques,axiom,(?[BNODE_r]:(?[BNODE_i]:(?[BNODE_l1]:(?[BNODE_l2]:(?[BNODE_l3]:((((((((((((((((((iext(uri_rdf_type,uri_ex_Clique,uri_owl_Class)&iext(uri_rdfs_subPropertyOf,uri_ex_sameCliqueAs,uri_owl_sameAs))&iext(uri_rdfs_range,uri_ex_sameCliqueAs,uri_ex_Clique))&iext(uri_rdfs_subClassOf,uri_ex_Clique,BNODE_r))&iext(uri_rdf_type,BNODE_r,uri_owl_Restriction))&iext(uri_owl_onProperty,BNODE_r,uri_ex_sameCliqueAs))&iext(uri_owl_someValuesFrom,BNODE_r,uri_ex_Clique))&iext(uri_rdf_type,uri_foaf_knows,uri_owl_ObjectProperty))&iext(uri_owl_propertyChainAxiom,uri_foaf_knows,BNODE_l1))&iext(uri_rdf_first,BNODE_l1,uri_rdf_type))&iext(uri_rdf_rest,BNODE_l1,BNODE_l2))&iext(uri_rdf_first,BNODE_l2,uri_ex_sameCliqueAs))&iext(uri_rdf_rest,BNODE_l2,BNODE_l3))&iext(uri_rdf_first,BNODE_l3,BNODE_i))&iext(uri_rdf_rest,BNODE_l3,uri_rdf_nil))&iext(uri_owl_inverseOf,BNODE_i,uri_rdf_type))&iext(uri_rdf_type,uri_ex_JoesGang,uri_ex_Clique))&iext(uri_rdf_type,uri_ex_alice,uri_ex_JoesGang))&iext(uri_rdf_type,uri_ex_bob,uri_ex_JoesGang))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', testcase_premise_fullish_013_Cliques)).
% 4.55/4.75  fof(c0,plain,((((?[BNODE_r]:(?[BNODE_i]:((?[BNODE_l1]:(?[BNODE_l2]:(?[BNODE_l3]:((((((((((((((iext(uri_rdf_type,uri_ex_Clique,uri_owl_Class)&iext(uri_rdfs_subPropertyOf,uri_ex_sameCliqueAs,uri_owl_sameAs))&iext(uri_rdfs_range,uri_ex_sameCliqueAs,uri_ex_Clique))&iext(uri_rdfs_subClassOf,uri_ex_Clique,BNODE_r))&iext(uri_rdf_type,BNODE_r,uri_owl_Restriction))&iext(uri_owl_onProperty,BNODE_r,uri_ex_sameCliqueAs))&iext(uri_owl_someValuesFrom,BNODE_r,uri_ex_Clique))&iext(uri_rdf_type,uri_foaf_knows,uri_owl_ObjectProperty))&iext(uri_owl_propertyChainAxiom,uri_foaf_knows,BNODE_l1))&iext(uri_rdf_first,BNODE_l1,uri_rdf_type))&iext(uri_rdf_rest,BNODE_l1,BNODE_l2))&iext(uri_rdf_first,BNODE_l2,uri_ex_sameCliqueAs))&iext(uri_rdf_rest,BNODE_l2,BNODE_l3))&iext(uri_rdf_first,BNODE_l3,BNODE_i))&iext(uri_rdf_rest,BNODE_l3,uri_rdf_nil)))))&iext(uri_owl_inverseOf,BNODE_i,uri_rdf_type))))&iext(uri_rdf_type,uri_ex_JoesGang,uri_ex_Clique))&iext(uri_rdf_type,uri_ex_alice,uri_ex_JoesGang))&iext(uri_rdf_type,uri_ex_bob,uri_ex_JoesGang)),inference(shift_quantors,[status(thm)],[testcase_premise_fullish_013_Cliques])).
% 4.55/4.75  fof(c1,plain,((((?[X2]:(?[X3]:((?[X4]:(?[X5]:(?[X6]:((((((((((((((iext(uri_rdf_type,uri_ex_Clique,uri_owl_Class)&iext(uri_rdfs_subPropertyOf,uri_ex_sameCliqueAs,uri_owl_sameAs))&iext(uri_rdfs_range,uri_ex_sameCliqueAs,uri_ex_Clique))&iext(uri_rdfs_subClassOf,uri_ex_Clique,X2))&iext(uri_rdf_type,X2,uri_owl_Restriction))&iext(uri_owl_onProperty,X2,uri_ex_sameCliqueAs))&iext(uri_owl_someValuesFrom,X2,uri_ex_Clique))&iext(uri_rdf_type,uri_foaf_knows,uri_owl_ObjectProperty))&iext(uri_owl_propertyChainAxiom,uri_foaf_knows,X4))&iext(uri_rdf_first,X4,uri_rdf_type))&iext(uri_rdf_rest,X4,X5))&iext(uri_rdf_first,X5,uri_ex_sameCliqueAs))&iext(uri_rdf_rest,X5,X6))&iext(uri_rdf_first,X6,X3))&iext(uri_rdf_rest,X6,uri_rdf_nil)))))&iext(uri_owl_inverseOf,X3,uri_rdf_type))))&iext(uri_rdf_type,uri_ex_JoesGang,uri_ex_Clique))&iext(uri_rdf_type,uri_ex_alice,uri_ex_JoesGang))&iext(uri_rdf_type,uri_ex_bob,uri_ex_JoesGang)),inference(variable_rename,[status(thm)],[c0])).
% 4.55/4.75  fof(c2,plain,((((((((((((((((((iext(uri_rdf_type,uri_ex_Clique,uri_owl_Class)&iext(uri_rdfs_subPropertyOf,uri_ex_sameCliqueAs,uri_owl_sameAs))&iext(uri_rdfs_range,uri_ex_sameCliqueAs,uri_ex_Clique))&iext(uri_rdfs_subClassOf,uri_ex_Clique,skolem0001))&iext(uri_rdf_type,skolem0001,uri_owl_Restriction))&iext(uri_owl_onProperty,skolem0001,uri_ex_sameCliqueAs))&iext(uri_owl_someValuesFrom,skolem0001,uri_ex_Clique))&iext(uri_rdf_type,uri_foaf_knows,uri_owl_ObjectProperty))&iext(uri_owl_propertyChainAxiom,uri_foaf_knows,skolem0003))&iext(uri_rdf_first,skolem0003,uri_rdf_type))&iext(uri_rdf_rest,skolem0003,skolem0004))&iext(uri_rdf_first,skolem0004,uri_ex_sameCliqueAs))&iext(uri_rdf_rest,skolem0004,skolem0005))&iext(uri_rdf_first,skolem0005,skolem0002))&iext(uri_rdf_rest,skolem0005,uri_rdf_nil))&iext(uri_owl_inverseOf,skolem0002,uri_rdf_type))&iext(uri_rdf_type,uri_ex_JoesGang,uri_ex_Clique))&iext(uri_rdf_type,uri_ex_alice,uri_ex_JoesGang))&iext(uri_rdf_type,uri_ex_bob,uri_ex_JoesGang)),inference(skolemize,[status(esa)],[c1])).
% 4.55/4.75  cnf(c13,plain,iext(uri_rdf_rest,skolem0003,skolem0004),inference(split_conjunct,[status(thm)],[c2])).
% 4.55/4.75  cnf(c322,plain,~iext(uri_rdfs_domain,uri_rdf_rest,X245)|icext(X245,skolem0003),inference(resolution,[status(thm)],[c94, c13])).
% 4.55/4.75  cnf(c1456,plain,icext(uri_rdf_List,skolem0003),inference(resolution,[status(thm)],[c322, c121])).
% 4.55/4.75  cnf(c1457,plain,iext(uri_rdf_type,skolem0003,uri_rdf_List),inference(resolution,[status(thm)],[c1456, c132])).
% 4.55/4.75  cnf(c1461,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X762)|iext(X762,skolem0003,uri_rdf_List),inference(resolution,[status(thm)],[c1457, c42])).
% 4.55/4.75  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)).
% 4.55/4.75  cnf(c27,plain,iext(uri_rdfs_range,uri_rdf_type,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_type_range])).
% 4.55/4.75  cnf(c7,plain,iext(uri_rdf_type,skolem0001,uri_owl_Restriction),inference(split_conjunct,[status(thm)],[c2])).
% 4.55/4.75  cnf(c316,plain,~iext(uri_rdfs_range,uri_rdf_type,X237)|icext(X237,uri_owl_Restriction),inference(resolution,[status(thm)],[c68, c7])).
% 4.55/4.75  cnf(c1427,plain,icext(uri_rdfs_Class,uri_owl_Restriction),inference(resolution,[status(thm)],[c316, c27])).
% 4.55/4.75  cnf(c1428,plain,ic(uri_owl_Restriction),inference(resolution,[status(thm)],[c1427, c88])).
% 4.55/4.75  cnf(c1432,plain,iext(uri_rdfs_subClassOf,uri_owl_Restriction,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1428, c126])).
% 4.55/4.75  cnf(c1454,plain,~iext(uri_rdfs_subClassOf,X761,uri_owl_Restriction)|iext(uri_rdfs_subClassOf,X761,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1432, c46])).
% 4.55/4.75  cnf(c1453,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X760)|iext(X760,uri_owl_Restriction,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1432, c42])).
% 4.55/4.75  cnf(c1431,plain,iext(uri_rdfs_subClassOf,uri_owl_Restriction,uri_owl_Restriction),inference(resolution,[status(thm)],[c1428, c49])).
% 4.55/4.75  cnf(c1445,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X758)|iext(X758,uri_owl_Restriction,uri_owl_Restriction),inference(resolution,[status(thm)],[c1431, c42])).
% 4.55/4.75  cnf(c1429,plain,iext(uri_rdf_type,uri_owl_Restriction,uri_rdfs_Class),inference(resolution,[status(thm)],[c1427, c132])).
% 4.55/4.75  cnf(c1436,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X757)|iext(X757,uri_owl_Restriction,uri_rdfs_Class),inference(resolution,[status(thm)],[c1429, c42])).
% 4.55/4.75  cnf(c21,plain,iext(uri_rdf_type,uri_ex_bob,uri_ex_JoesGang),inference(split_conjunct,[status(thm)],[c2])).
% 4.55/4.75  cnf(c295,plain,~iext(uri_rdfs_range,uri_rdf_type,X197)|icext(X197,uri_ex_JoesGang),inference(resolution,[status(thm)],[c68, c21])).
% 4.55/4.75  cnf(c1324,plain,icext(uri_rdfs_Class,uri_ex_JoesGang),inference(resolution,[status(thm)],[c295, c27])).
% 4.55/4.75  cnf(c1325,plain,ic(uri_ex_JoesGang),inference(resolution,[status(thm)],[c1324, c88])).
% 4.55/4.75  cnf(c1329,plain,iext(uri_rdfs_subClassOf,uri_ex_JoesGang,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1325, c126])).
% 4.55/4.75  cnf(c1422,plain,~iext(uri_rdfs_subClassOf,X756,uri_ex_JoesGang)|iext(uri_rdfs_subClassOf,X756,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1329, c46])).
% 4.55/4.75  cnf(c1421,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X755)|iext(X755,uri_ex_JoesGang,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1329, c42])).
% 4.55/4.75  cnf(c1328,plain,iext(uri_rdfs_subClassOf,uri_ex_JoesGang,uri_ex_JoesGang),inference(resolution,[status(thm)],[c1325, c49])).
% 4.55/4.75  cnf(c1413,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X753)|iext(X753,uri_ex_JoesGang,uri_ex_JoesGang),inference(resolution,[status(thm)],[c1328, c42])).
% 4.55/4.75  cnf(c1326,plain,iext(uri_rdf_type,uri_ex_JoesGang,uri_rdfs_Class),inference(resolution,[status(thm)],[c1324, c132])).
% 4.55/4.75  cnf(c1405,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X752)|iext(X752,uri_ex_JoesGang,uri_rdfs_Class),inference(resolution,[status(thm)],[c1326, c42])).
% 4.55/4.75  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)).
% 4.55/4.75  cnf(c89,plain,iext(uri_rdfs_range,uri_rdfs_domain,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_domain_range])).
% 4.55/4.75  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)).
% 4.55/4.75  cnf(c64,plain,iext(uri_rdfs_domain,uri_rdf_object,uri_rdfs_Statement),inference(split_conjunct,[status(thm)],[rdfs_reification_object_domain])).
% 4.55/4.75  cnf(c282,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X184)|icext(X184,uri_rdfs_Statement),inference(resolution,[status(thm)],[c68, c64])).
% 4.55/4.75  cnf(c1288,plain,icext(uri_rdfs_Class,uri_rdfs_Statement),inference(resolution,[status(thm)],[c282, c89])).
% 4.55/4.75  cnf(c1289,plain,ic(uri_rdfs_Statement),inference(resolution,[status(thm)],[c1288, c88])).
% 4.55/4.75  cnf(c1293,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Statement,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1289, c126])).
% 4.55/4.75  cnf(c1401,plain,~iext(uri_rdfs_subClassOf,X751,uri_rdfs_Statement)|iext(uri_rdfs_subClassOf,X751,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1293, c46])).
% 4.55/4.75  cnf(c1400,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X750)|iext(X750,uri_rdfs_Statement,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1293, c42])).
% 4.55/4.75  cnf(c1292,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Statement,uri_rdfs_Statement),inference(resolution,[status(thm)],[c1289, c49])).
% 4.55/4.75  cnf(c1392,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X748)|iext(X748,uri_rdfs_Statement,uri_rdfs_Statement),inference(resolution,[status(thm)],[c1292, c42])).
% 4.55/4.75  cnf(c1290,plain,iext(uri_rdf_type,uri_rdfs_Statement,uri_rdfs_Class),inference(resolution,[status(thm)],[c1288, c132])).
% 4.55/4.75  cnf(c1383,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X747)|iext(X747,uri_rdfs_Statement,uri_rdfs_Class),inference(resolution,[status(thm)],[c1290, c42])).
% 4.55/4.75  cnf(c3,plain,iext(uri_rdf_type,uri_ex_Clique,uri_owl_Class),inference(split_conjunct,[status(thm)],[c2])).
% 4.55/4.75  cnf(c278,plain,~iext(uri_rdfs_range,uri_rdf_type,X180)|icext(X180,uri_owl_Class),inference(resolution,[status(thm)],[c68, c3])).
% 4.55/4.75  cnf(c1257,plain,icext(uri_rdfs_Class,uri_owl_Class),inference(resolution,[status(thm)],[c278, c27])).
% 4.55/4.75  cnf(c1259,plain,ic(uri_owl_Class),inference(resolution,[status(thm)],[c1257, c88])).
% 4.55/4.75  cnf(c1263,plain,iext(uri_rdfs_subClassOf,uri_owl_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1259, c126])).
% 4.55/4.75  cnf(c1379,plain,~iext(uri_rdfs_subClassOf,X746,uri_owl_Class)|iext(uri_rdfs_subClassOf,X746,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1263, c46])).
% 4.55/4.75  cnf(c1378,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X745)|iext(X745,uri_owl_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1263, c42])).
% 4.55/4.75  cnf(c1262,plain,iext(uri_rdfs_subClassOf,uri_owl_Class,uri_owl_Class),inference(resolution,[status(thm)],[c1259, c49])).
% 4.55/4.75  cnf(c1369,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X743)|iext(X743,uri_owl_Class,uri_owl_Class),inference(resolution,[status(thm)],[c1262, c42])).
% 4.55/4.75  cnf(c1260,plain,iext(uri_rdf_type,uri_owl_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c1257, c132])).
% 4.55/4.75  cnf(c1360,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X742)|iext(X742,uri_owl_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c1260, c42])).
% 4.55/4.75  cnf(c15,plain,iext(uri_rdf_rest,skolem0004,skolem0005),inference(split_conjunct,[status(thm)],[c2])).
% 4.55/4.75  cnf(c276,plain,~iext(uri_rdfs_range,uri_rdf_rest,X178)|icext(X178,skolem0005),inference(resolution,[status(thm)],[c68, c15])).
% 4.55/4.75  cnf(c1238,plain,icext(uri_rdf_List,skolem0005),inference(resolution,[status(thm)],[c276, c120])).
% 4.55/4.75  cnf(c1240,plain,iext(uri_rdf_type,skolem0005,uri_rdf_List),inference(resolution,[status(thm)],[c1238, c132])).
% 4.55/4.75  cnf(c1355,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X741)|iext(X741,skolem0005,uri_rdf_List),inference(resolution,[status(thm)],[c1240, c42])).
% 4.55/4.75  cnf(c10,plain,iext(uri_rdf_type,uri_foaf_knows,uri_owl_ObjectProperty),inference(split_conjunct,[status(thm)],[c2])).
% 4.55/4.75  cnf(c270,plain,~iext(uri_rdfs_range,uri_rdf_type,X172)|icext(X172,uri_owl_ObjectProperty),inference(resolution,[status(thm)],[c68, c10])).
% 4.55/4.75  cnf(c1172,plain,icext(uri_rdfs_Class,uri_owl_ObjectProperty),inference(resolution,[status(thm)],[c270, c27])).
% 4.55/4.75  cnf(c1174,plain,ic(uri_owl_ObjectProperty),inference(resolution,[status(thm)],[c1172, c88])).
% 4.55/4.75  cnf(c1178,plain,iext(uri_rdfs_subClassOf,uri_owl_ObjectProperty,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1174, c126])).
% 4.55/4.75  cnf(c1350,plain,~iext(uri_rdfs_subClassOf,X740,uri_owl_ObjectProperty)|iext(uri_rdfs_subClassOf,X740,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1178, c46])).
% 4.55/4.75  cnf(c1349,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X739)|iext(X739,uri_owl_ObjectProperty,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1178, c42])).
% 4.55/4.75  cnf(c1177,plain,iext(uri_rdfs_subClassOf,uri_owl_ObjectProperty,uri_owl_ObjectProperty),inference(resolution,[status(thm)],[c1174, c49])).
% 4.55/4.75  cnf(c1341,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X737)|iext(X737,uri_owl_ObjectProperty,uri_owl_ObjectProperty),inference(resolution,[status(thm)],[c1177, c42])).
% 4.55/4.75  cnf(c1175,plain,iext(uri_rdf_type,uri_owl_ObjectProperty,uri_rdfs_Class),inference(resolution,[status(thm)],[c1172, c132])).
% 4.55/4.75  cnf(c1333,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X736)|iext(X736,uri_owl_ObjectProperty,uri_rdfs_Class),inference(resolution,[status(thm)],[c1175, c42])).
% 4.55/4.75  cnf(c268,plain,~iext(uri_rdfs_range,uri_rdf_rest,X170)|icext(X170,skolem0004),inference(resolution,[status(thm)],[c68, c13])).
% 4.55/4.75  cnf(c1151,plain,icext(uri_rdf_List,skolem0004),inference(resolution,[status(thm)],[c268, c120])).
% 4.55/4.75  cnf(c1153,plain,iext(uri_rdf_type,skolem0004,uri_rdf_List),inference(resolution,[status(thm)],[c1151, c132])).
% 4.55/4.75  cnf(c1322,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X735)|iext(X735,skolem0004,uri_rdf_List),inference(resolution,[status(thm)],[c1153, c42])).
% 4.55/4.75  cnf(c19,plain,iext(uri_rdf_type,uri_ex_JoesGang,uri_ex_Clique),inference(split_conjunct,[status(thm)],[c2])).
% 4.55/4.75  cnf(c131,plain,~iext(uri_rdf_type,X93,X94)|icext(X94,X93),inference(split_conjunct,[status(thm)],[c130])).
% 4.55/4.75  cnf(c456,plain,icext(uri_ex_Clique,uri_ex_JoesGang),inference(resolution,[status(thm)],[c131, c19])).
% 4.55/4.75  cnf(c6,plain,iext(uri_rdfs_subClassOf,uri_ex_Clique,skolem0001),inference(split_conjunct,[status(thm)],[c2])).
% 4.55/4.75  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)).
% 4.55/4.75  fof(c51,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])).
% 4.55/4.75  fof(c53,plain,(![X19]:(![X20]:(![X21]:(~iext(uri_rdfs_subClassOf,X19,X20)|((ic(X19)&ic(X20))&(~icext(X19,X21)|icext(X20,X21))))))),inference(shift_quantors,[status(thm)],[fof(c52,plain,(![X19]:(![X20]:(~iext(uri_rdfs_subClassOf,X19,X20)|((ic(X19)&ic(X20))&(![X21]:(~icext(X19,X21)|icext(X20,X21))))))),inference(variable_rename,[status(thm)],[c51])).])).
% 4.55/4.75  fof(c54,plain,(![X19]:(![X20]:(![X21]:(((~iext(uri_rdfs_subClassOf,X19,X20)|ic(X19))&(~iext(uri_rdfs_subClassOf,X19,X20)|ic(X20)))&(~iext(uri_rdfs_subClassOf,X19,X20)|(~icext(X19,X21)|icext(X20,X21))))))),inference(distribute,[status(thm)],[c53])).
% 4.55/4.75  cnf(c57,plain,~iext(uri_rdfs_subClassOf,X81,X79)|~icext(X81,X80)|icext(X79,X80),inference(split_conjunct,[status(thm)],[c54])).
% 4.55/4.75  cnf(c258,plain,~icext(uri_ex_Clique,X163)|icext(skolem0001,X163),inference(resolution,[status(thm)],[c57, c6])).
% 4.55/4.75  cnf(c1079,plain,icext(skolem0001,uri_ex_JoesGang),inference(resolution,[status(thm)],[c258, c456])).
% 4.55/4.75  cnf(c1080,plain,iext(uri_rdf_type,uri_ex_JoesGang,skolem0001),inference(resolution,[status(thm)],[c1079, c132])).
% 4.55/4.75  cnf(c1314,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X734)|iext(X734,uri_ex_JoesGang,skolem0001),inference(resolution,[status(thm)],[c1080, c42])).
% 4.55/4.75  cnf(c41,plain,~iext(uri_rdfs_subPropertyOf,X62,X63)|ip(X63),inference(split_conjunct,[status(thm)],[c39])).
% 4.55/4.75  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)).
% 4.55/4.75  fof(c115,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])).
% 4.55/4.75  fof(c116,plain,(![X37]:(~icext(uri_rdfs_ContainerMembershipProperty,X37)|iext(uri_rdfs_subPropertyOf,X37,uri_rdfs_member))),inference(variable_rename,[status(thm)],[c115])).
% 4.55/4.75  cnf(c117,plain,~icext(uri_rdfs_ContainerMembershipProperty,X91)|iext(uri_rdfs_subPropertyOf,X91,uri_rdfs_member),inference(split_conjunct,[status(thm)],[c116])).
% 4.55/4.75  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)).
% 4.55/4.75  cnf(c104,plain,iext(uri_rdf_type,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),inference(split_conjunct,[status(thm)],[rdfs_container_n_type_002])).
% 4.55/4.75  cnf(c455,plain,icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__2),inference(resolution,[status(thm)],[c131, c104])).
% 4.55/4.75  cnf(c464,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__2,uri_rdfs_member),inference(resolution,[status(thm)],[c455, c117])).
% 4.55/4.75  cnf(c910,plain,ip(uri_rdfs_member),inference(resolution,[status(thm)],[c464, c41])).
% 4.55/4.75  cnf(c917,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_member,uri_rdfs_member),inference(resolution,[status(thm)],[c910, c34])).
% 4.55/4.75  cnf(c1308,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X733)|iext(X733,uri_rdfs_member,uri_rdfs_member),inference(resolution,[status(thm)],[c917, c42])).
% 4.55/4.75  cnf(c149,plain,~ip(X100)|iext(uri_rdf_type,X100,uri_rdf_Property),inference(split_conjunct,[status(thm)],[c147])).
% 4.55/4.75  cnf(c916,plain,iext(uri_rdf_type,uri_rdfs_member,uri_rdf_Property),inference(resolution,[status(thm)],[c910, c149])).
% 4.55/4.75  cnf(c1298,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X731)|iext(X731,uri_rdfs_member,uri_rdf_Property),inference(resolution,[status(thm)],[c916, c42])).
% 4.55/4.75  cnf(c87,plain,~ic(X65)|icext(uri_rdfs_Class,X65),inference(split_conjunct,[status(thm)],[c86])).
% 4.55/4.75  cnf(c56,plain,~iext(uri_rdfs_subClassOf,X78,X77)|ic(X77),inference(split_conjunct,[status(thm)],[c54])).
% 4.55/4.75  cnf(c55,plain,~iext(uri_rdfs_subClassOf,X76,X75)|ic(X76),inference(split_conjunct,[status(thm)],[c54])).
% 4.55/4.75  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)).
% 4.55/4.75  cnf(c119,plain,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Container),inference(split_conjunct,[status(thm)],[rdfs_container_alt_sub])).
% 4.55/4.75  cnf(c399,plain,ic(uri_rdf_Alt),inference(resolution,[status(thm)],[c119, c55])).
% 4.55/4.75  cnf(c424,plain,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Resource),inference(resolution,[status(thm)],[c126, c399])).
% 4.55/4.75  cnf(c798,plain,ic(uri_rdfs_Resource),inference(resolution,[status(thm)],[c424, c56])).
% 4.55/4.75  cnf(c802,plain,icext(uri_rdfs_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c798, c87])).
% 4.55/4.75  cnf(c806,plain,iext(uri_rdf_type,uri_rdfs_Resource,uri_rdfs_Class),inference(resolution,[status(thm)],[c802, c132])).
% 4.55/4.75  cnf(c1286,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X730)|iext(X730,uri_rdfs_Resource,uri_rdfs_Class),inference(resolution,[status(thm)],[c806, c42])).
% 4.55/4.75  cnf(c803,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Resource,uri_rdfs_Resource),inference(resolution,[status(thm)],[c798, c49])).
% 4.55/4.75  cnf(c1280,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X728)|iext(X728,uri_rdfs_Resource,uri_rdfs_Resource),inference(resolution,[status(thm)],[c803, c42])).
% 4.55/4.75  cnf(c18,plain,iext(uri_owl_inverseOf,skolem0002,uri_rdf_type),inference(split_conjunct,[status(thm)],[c2])).
% 4.55/4.75  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)).
% 4.55/4.75  fof(c164,plain,(![S]:(![P]:(![O]:(~iext(P,S,O)|ip(P))))),inference(fof_nnf,[status(thm)],[simple_iext_property])).
% 4.55/4.75  fof(c165,plain,(![S]:(![P]:((![O]:~iext(P,S,O))|ip(P)))),inference(shift_quantors,[status(thm)],[c164])).
% 4.55/4.75  fof(c167,plain,(![X47]:(![X48]:(![X49]:(~iext(X48,X47,X49)|ip(X48))))),inference(shift_quantors,[status(thm)],[fof(c166,plain,(![X47]:(![X48]:((![X49]:~iext(X48,X47,X49))|ip(X48)))),inference(variable_rename,[status(thm)],[c165])).])).
% 4.55/4.75  cnf(c168,plain,~iext(X101,X102,X103)|ip(X101),inference(split_conjunct,[status(thm)],[c167])).
% 4.55/4.75  cnf(c627,plain,ip(uri_owl_inverseOf),inference(resolution,[status(thm)],[c168, c18])).
% 4.55/4.75  cnf(c697,plain,iext(uri_rdfs_subPropertyOf,uri_owl_inverseOf,uri_owl_inverseOf),inference(resolution,[status(thm)],[c627, c34])).
% 4.55/4.75  cnf(c1272,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X727)|iext(X727,uri_owl_inverseOf,uri_owl_inverseOf),inference(resolution,[status(thm)],[c697, c42])).
% 4.55/4.75  cnf(c696,plain,iext(uri_rdf_type,uri_owl_inverseOf,uri_rdf_Property),inference(resolution,[status(thm)],[c627, c149])).
% 4.55/4.75  cnf(c1253,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X725)|iext(X725,uri_owl_inverseOf,uri_rdf_Property),inference(resolution,[status(thm)],[c696, c42])).
% 4.55/4.75  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)).
% 4.55/4.75  cnf(c137,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_sub])).
% 4.55/4.75  cnf(c603,plain,ip(uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c168, c137])).
% 4.55/4.75  cnf(c688,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c603, c34])).
% 4.55/4.75  cnf(c1245,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X724)|iext(X724,uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c688, c42])).
% 4.55/4.75  cnf(c687,plain,iext(uri_rdf_type,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c603, c149])).
% 4.55/4.75  cnf(c1234,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X722)|iext(X722,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c687, c42])).
% 4.55/4.75  cnf(c9,plain,iext(uri_owl_someValuesFrom,skolem0001,uri_ex_Clique),inference(split_conjunct,[status(thm)],[c2])).
% 4.55/4.75  cnf(c601,plain,ip(uri_owl_someValuesFrom),inference(resolution,[status(thm)],[c168, c9])).
% 4.55/4.75  cnf(c686,plain,iext(uri_rdfs_subPropertyOf,uri_owl_someValuesFrom,uri_owl_someValuesFrom),inference(resolution,[status(thm)],[c601, c34])).
% 4.55/4.75  cnf(c1227,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X721)|iext(X721,uri_owl_someValuesFrom,uri_owl_someValuesFrom),inference(resolution,[status(thm)],[c686, c42])).
% 4.55/4.75  cnf(c685,plain,iext(uri_rdf_type,uri_owl_someValuesFrom,uri_rdf_Property),inference(resolution,[status(thm)],[c601, c149])).
% 4.55/4.75  cnf(c1219,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X719)|iext(X719,uri_owl_someValuesFrom,uri_rdf_Property),inference(resolution,[status(thm)],[c685, c42])).
% 4.55/4.75  cnf(c596,plain,ip(uri_rdfs_range),inference(resolution,[status(thm)],[c168, c120])).
% 4.55/4.75  cnf(c676,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_range,uri_rdfs_range),inference(resolution,[status(thm)],[c596, c34])).
% 4.55/4.75  cnf(c1202,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X718)|iext(X718,uri_rdfs_range,uri_rdfs_range),inference(resolution,[status(thm)],[c676, c42])).
% 4.55/4.75  cnf(c675,plain,iext(uri_rdf_type,uri_rdfs_range,uri_rdf_Property),inference(resolution,[status(thm)],[c596, c149])).
% 4.55/4.75  cnf(c1189,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X716)|iext(X716,uri_rdfs_range,uri_rdf_Property),inference(resolution,[status(thm)],[c675, c42])).
% 4.55/4.75  cnf(c8,plain,iext(uri_owl_onProperty,skolem0001,uri_ex_sameCliqueAs),inference(split_conjunct,[status(thm)],[c2])).
% 4.55/4.75  cnf(c595,plain,ip(uri_owl_onProperty),inference(resolution,[status(thm)],[c168, c8])).
% 4.55/4.75  cnf(c674,plain,iext(uri_rdfs_subPropertyOf,uri_owl_onProperty,uri_owl_onProperty),inference(resolution,[status(thm)],[c595, c34])).
% 4.55/4.75  cnf(c1182,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X715)|iext(X715,uri_owl_onProperty,uri_owl_onProperty),inference(resolution,[status(thm)],[c674, c42])).
% 4.55/4.75  cnf(c673,plain,iext(uri_rdf_type,uri_owl_onProperty,uri_rdf_Property),inference(resolution,[status(thm)],[c595, c149])).
% 4.55/4.75  cnf(c1168,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X713)|iext(X713,uri_owl_onProperty,uri_rdf_Property),inference(resolution,[status(thm)],[c673, c42])).
% 4.55/4.75  cnf(c593,plain,ip(uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c168, c6])).
% 4.55/4.75  cnf(c672,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c593, c34])).
% 4.55/4.75  cnf(c1157,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X712)|iext(X712,uri_rdfs_subClassOf,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c672, c42])).
% 4.55/4.75  cnf(c671,plain,iext(uri_rdf_type,uri_rdfs_subClassOf,uri_rdf_Property),inference(resolution,[status(thm)],[c593, c149])).
% 4.55/4.75  cnf(c1147,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X710)|iext(X710,uri_rdfs_subClassOf,uri_rdf_Property),inference(resolution,[status(thm)],[c671, c42])).
% 4.55/4.75  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)).
% 4.55/4.75  cnf(c111,plain,iext(uri_rdfs_domain,uri_rdf__1,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_001])).
% 4.55/4.75  cnf(c589,plain,ip(uri_rdfs_domain),inference(resolution,[status(thm)],[c168, c111])).
% 4.55/4.75  cnf(c670,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,uri_rdfs_domain),inference(resolution,[status(thm)],[c589, c34])).
% 4.55/4.75  cnf(c1130,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X709)|iext(X709,uri_rdfs_domain,uri_rdfs_domain),inference(resolution,[status(thm)],[c670, c42])).
% 4.55/4.75  cnf(c669,plain,iext(uri_rdf_type,uri_rdfs_domain,uri_rdf_Property),inference(resolution,[status(thm)],[c589, c149])).
% 4.55/4.75  cnf(c1120,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X707)|iext(X707,uri_rdfs_domain,uri_rdf_Property),inference(resolution,[status(thm)],[c669, c42])).
% 4.55/4.75  cnf(c11,plain,iext(uri_owl_propertyChainAxiom,uri_foaf_knows,skolem0003),inference(split_conjunct,[status(thm)],[c2])).
% 4.55/4.75  cnf(c588,plain,ip(uri_owl_propertyChainAxiom),inference(resolution,[status(thm)],[c168, c11])).
% 4.55/4.75  cnf(c668,plain,iext(uri_rdfs_subPropertyOf,uri_owl_propertyChainAxiom,uri_owl_propertyChainAxiom),inference(resolution,[status(thm)],[c588, c34])).
% 4.55/4.75  cnf(c1113,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X706)|iext(X706,uri_owl_propertyChainAxiom,uri_owl_propertyChainAxiom),inference(resolution,[status(thm)],[c668, c42])).
% 4.55/4.75  cnf(c667,plain,iext(uri_rdf_type,uri_owl_propertyChainAxiom,uri_rdf_Property),inference(resolution,[status(thm)],[c588, c149])).
% 4.55/4.75  cnf(c1103,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X704)|iext(X704,uri_owl_propertyChainAxiom,uri_rdf_Property),inference(resolution,[status(thm)],[c667, c42])).
% 4.55/4.75  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)).
% 4.55/4.75  cnf(c158,plain,iext(uri_rdf_type,uri_rdf_first,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_collection_first_type])).
% 4.55/4.75  cnf(c579,plain,ip(uri_rdf_first),inference(resolution,[status(thm)],[c158, c148])).
% 4.55/4.75  cnf(c585,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_first,uri_rdf_first),inference(resolution,[status(thm)],[c579, c34])).
% 4.55/4.75  cnf(c1096,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X703)|iext(X703,uri_rdf_first,uri_rdf_first),inference(resolution,[status(thm)],[c585, c42])).
% 4.55/4.75  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)).
% 4.55/4.75  cnf(c156,plain,iext(uri_rdf_type,uri_rdf_rest,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_collection_rest_type])).
% 4.55/4.75  cnf(c564,plain,ip(uri_rdf_rest),inference(resolution,[status(thm)],[c156, c148])).
% 4.55/4.75  cnf(c572,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_rest,uri_rdf_rest),inference(resolution,[status(thm)],[c564, c34])).
% 4.55/4.75  cnf(c1084,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X701)|iext(X701,uri_rdf_rest,uri_rdf_rest),inference(resolution,[status(thm)],[c572, c42])).
% 4.55/4.75  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)).
% 4.55/4.75  cnf(c155,plain,iext(uri_rdf_type,uri_rdf__1,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_container_n_type_001])).
% 4.55/4.75  cnf(c559,plain,ip(uri_rdf__1),inference(resolution,[status(thm)],[c155, c148])).
% 4.55/4.75  cnf(c570,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__1,uri_rdf__1),inference(resolution,[status(thm)],[c559, c34])).
% 4.55/4.75  cnf(c1075,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X699)|iext(X699,uri_rdf__1,uri_rdf__1),inference(resolution,[status(thm)],[c570, c42])).
% 4.55/4.75  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)).
% 4.55/4.75  cnf(c154,plain,iext(uri_rdf_type,uri_rdf__2,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_container_n_type_002])).
% 4.55/4.75  cnf(c548,plain,ip(uri_rdf__2),inference(resolution,[status(thm)],[c154, c148])).
% 4.55/4.75  cnf(c556,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__2,uri_rdf__2),inference(resolution,[status(thm)],[c548, c34])).
% 4.55/4.75  cnf(c1068,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X697)|iext(X697,uri_rdf__2,uri_rdf__2),inference(resolution,[status(thm)],[c556, c42])).
% 4.55/4.75  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)).
% 4.55/4.75  cnf(c153,plain,iext(uri_rdf_type,uri_rdf__3,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_container_n_type_003])).
% 4.55/4.75  cnf(c543,plain,ip(uri_rdf__3),inference(resolution,[status(thm)],[c153, c148])).
% 4.55/4.75  cnf(c554,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__3,uri_rdf__3),inference(resolution,[status(thm)],[c543, c34])).
% 4.55/4.75  cnf(c1061,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X695)|iext(X695,uri_rdf__3,uri_rdf__3),inference(resolution,[status(thm)],[c554, c42])).
% 4.55/4.75  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)).
% 4.55/4.75  cnf(c152,plain,iext(uri_rdf_type,uri_rdf_object,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_reification_object_type])).
% 4.55/4.75  cnf(c535,plain,ip(uri_rdf_object),inference(resolution,[status(thm)],[c152, c148])).
% 4.55/4.75  cnf(c541,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_object,uri_rdf_object),inference(resolution,[status(thm)],[c535, c34])).
% 4.55/4.75  cnf(c1054,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X693)|iext(X693,uri_rdf_object,uri_rdf_object),inference(resolution,[status(thm)],[c541, c42])).
% 4.55/4.75  cnf(c4,plain,iext(uri_rdfs_subPropertyOf,uri_ex_sameCliqueAs,uri_owl_sameAs),inference(split_conjunct,[status(thm)],[c2])).
% 4.55/4.75  cnf(c40,plain,~iext(uri_rdfs_subPropertyOf,X56,X57)|ip(X56),inference(split_conjunct,[status(thm)],[c39])).
% 4.55/4.75  cnf(c171,plain,ip(uri_ex_sameCliqueAs),inference(resolution,[status(thm)],[c40, c4])).
% 4.55/4.75  cnf(c533,plain,iext(uri_rdf_type,uri_ex_sameCliqueAs,uri_rdf_Property),inference(resolution,[status(thm)],[c149, c171])).
% 4.55/4.75  cnf(c1046,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X691)|iext(X691,uri_ex_sameCliqueAs,uri_rdf_Property),inference(resolution,[status(thm)],[c533, c42])).
% 4.55/4.75  cnf(c174,plain,ip(uri_owl_sameAs),inference(resolution,[status(thm)],[c41, c4])).
% 4.55/4.75  cnf(c532,plain,iext(uri_rdf_type,uri_owl_sameAs,uri_rdf_Property),inference(resolution,[status(thm)],[c149, c174])).
% 4.55/4.75  cnf(c1039,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X690)|iext(X690,uri_owl_sameAs,uri_rdf_Property),inference(resolution,[status(thm)],[c532, c42])).
% 4.55/4.75  cnf(c449,plain,ip(uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c137, c40])).
% 4.55/4.75  cnf(c529,plain,iext(uri_rdf_type,uri_rdfs_isDefinedBy,uri_rdf_Property),inference(resolution,[status(thm)],[c149, c449])).
% 4.55/4.75  cnf(c1032,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X689)|iext(X689,uri_rdfs_isDefinedBy,uri_rdf_Property),inference(resolution,[status(thm)],[c529, c42])).
% 4.55/4.75  cnf(c448,plain,ip(uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c137, c41])).
% 4.55/4.75  cnf(c528,plain,iext(uri_rdf_type,uri_rdfs_seeAlso,uri_rdf_Property),inference(resolution,[status(thm)],[c149, c448])).
% 4.55/4.75  cnf(c1024,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X688)|iext(X688,uri_rdfs_seeAlso,uri_rdf_Property),inference(resolution,[status(thm)],[c528, c42])).
% 4.55/4.75  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)).
% 4.55/4.75  cnf(c151,plain,iext(uri_rdf_type,uri_rdf_value,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_reification_predicate_type])).
% 4.55/4.75  cnf(c521,plain,ip(uri_rdf_value),inference(resolution,[status(thm)],[c151, c148])).
% 4.55/4.75  cnf(c526,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_value,uri_rdf_value),inference(resolution,[status(thm)],[c521, c34])).
% 4.55/4.75  cnf(c1017,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X687)|iext(X687,uri_rdf_value,uri_rdf_value),inference(resolution,[status(thm)],[c526, c42])).
% 4.55/4.75  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)).
% 4.55/4.75  cnf(c150,plain,iext(uri_rdf_type,uri_rdf_subject,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_reification_subject_type])).
% 4.55/4.75  cnf(c517,plain,ip(uri_rdf_subject),inference(resolution,[status(thm)],[c148, c150])).
% 4.55/4.75  cnf(c519,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_subject,uri_rdf_subject),inference(resolution,[status(thm)],[c517, c34])).
% 4.55/4.75  cnf(c1009,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X685)|iext(X685,uri_rdf_subject,uri_rdf_subject),inference(resolution,[status(thm)],[c519, c42])).
% 4.55/4.75  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)).
% 4.55/4.75  cnf(c142,plain,iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_value_type])).
% 4.55/4.75  cnf(c516,plain,ip(uri_rdf_type),inference(resolution,[status(thm)],[c148, c142])).
% 4.55/4.75  cnf(c518,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_type,uri_rdf_type),inference(resolution,[status(thm)],[c516, c34])).
% 4.55/4.75  cnf(c994,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X683)|iext(X683,uri_rdf_type,uri_rdf_type),inference(resolution,[status(thm)],[c518, c42])).
% 4.55/4.75  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)).
% 4.55/4.75  cnf(c103,plain,iext(uri_rdf_type,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),inference(split_conjunct,[status(thm)],[rdfs_container_n_type_003])).
% 4.55/4.75  cnf(c461,plain,icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__3),inference(resolution,[status(thm)],[c131, c103])).
% 4.55/4.75  cnf(c492,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__3,uri_rdfs_member),inference(resolution,[status(thm)],[c461, c117])).
% 4.55/4.75  cnf(c985,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X681)|iext(X681,uri_rdf__3,uri_rdfs_member),inference(resolution,[status(thm)],[c492, c42])).
% 4.55/4.75  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)).
% 4.55/4.75  fof(c29,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])).
% 4.55/4.75  fof(c30,plain,(![X7]:(![X8]:(![X9]:((~iext(uri_rdfs_subPropertyOf,X7,X8)|~iext(uri_rdfs_subPropertyOf,X8,X9))|iext(uri_rdfs_subPropertyOf,X7,X9))))),inference(variable_rename,[status(thm)],[c29])).
% 4.55/4.75  cnf(c31,plain,~iext(uri_rdfs_subPropertyOf,X52,X53)|~iext(uri_rdfs_subPropertyOf,X53,X54)|iext(uri_rdfs_subPropertyOf,X52,X54),inference(split_conjunct,[status(thm)],[c30])).
% 4.55/4.75  cnf(c984,plain,~iext(uri_rdfs_subPropertyOf,X680,uri_rdf__3)|iext(uri_rdfs_subPropertyOf,X680,uri_rdfs_member),inference(resolution,[status(thm)],[c492, c31])).
% 4.55/4.75  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)).
% 4.55/4.75  cnf(c105,plain,iext(uri_rdf_type,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),inference(split_conjunct,[status(thm)],[rdfs_container_n_type_001])).
% 4.55/4.75  cnf(c457,plain,icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__1),inference(resolution,[status(thm)],[c131, c105])).
% 4.55/4.75  cnf(c483,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__1,uri_rdfs_member),inference(resolution,[status(thm)],[c457, c117])).
% 4.55/4.75  cnf(c976,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X679)|iext(X679,uri_rdf__1,uri_rdfs_member),inference(resolution,[status(thm)],[c483, c42])).
% 4.55/4.75  cnf(c975,plain,~iext(uri_rdfs_subPropertyOf,X678,uri_rdf__1)|iext(uri_rdfs_subPropertyOf,X678,uri_rdfs_member),inference(resolution,[status(thm)],[c483, c31])).
% 4.55/4.75  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)).
% 4.55/4.75  cnf(c96,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_datatype_sub])).
% 4.55/4.75  cnf(c236,plain,ic(uri_rdfs_Datatype),inference(resolution,[status(thm)],[c55, c96])).
% 4.55/4.75  cnf(c243,plain,icext(uri_rdfs_Class,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c236, c87])).
% 4.55/4.75  cnf(c479,plain,iext(uri_rdf_type,uri_rdfs_Datatype,uri_rdfs_Class),inference(resolution,[status(thm)],[c132, c243])).
% 4.55/4.75  cnf(c969,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X677)|iext(X677,uri_rdfs_Datatype,uri_rdfs_Class),inference(resolution,[status(thm)],[c479, c42])).
% 4.55/4.75  cnf(c405,plain,icext(uri_rdfs_Class,uri_rdf_Alt),inference(resolution,[status(thm)],[c399, c87])).
% 4.55/4.75  cnf(c478,plain,iext(uri_rdf_type,uri_rdf_Alt,uri_rdfs_Class),inference(resolution,[status(thm)],[c132, c405])).
% 4.55/4.75  cnf(c964,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X676)|iext(X676,uri_rdf_Alt,uri_rdfs_Class),inference(resolution,[status(thm)],[c478, c42])).
% 4.55/4.75  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)).
% 4.55/4.75  cnf(c118,plain,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Container),inference(split_conjunct,[status(thm)],[rdfs_container_bag_sub])).
% 4.55/4.75  cnf(c390,plain,ic(uri_rdf_Bag),inference(resolution,[status(thm)],[c118, c55])).
% 4.55/4.75  cnf(c396,plain,icext(uri_rdfs_Class,uri_rdf_Bag),inference(resolution,[status(thm)],[c390, c87])).
% 4.55/4.75  cnf(c476,plain,iext(uri_rdf_type,uri_rdf_Bag,uri_rdfs_Class),inference(resolution,[status(thm)],[c132, c396])).
% 4.55/4.75  cnf(c959,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X675)|iext(X675,uri_rdf_Bag,uri_rdfs_Class),inference(resolution,[status(thm)],[c476, c42])).
% 4.55/4.75  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)).
% 4.55/4.75  cnf(c102,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Container),inference(split_conjunct,[status(thm)],[rdfs_container_seq_sub])).
% 4.55/4.75  cnf(c248,plain,ic(uri_rdfs_Container),inference(resolution,[status(thm)],[c56, c102])).
% 4.55/4.75  cnf(c254,plain,icext(uri_rdfs_Class,uri_rdfs_Container),inference(resolution,[status(thm)],[c248, c87])).
% 4.55/4.75  cnf(c475,plain,iext(uri_rdf_type,uri_rdfs_Container,uri_rdfs_Class),inference(resolution,[status(thm)],[c132, c254])).
% 4.55/4.75  cnf(c954,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X674)|iext(X674,uri_rdfs_Container,uri_rdfs_Class),inference(resolution,[status(thm)],[c475, c42])).
% 4.55/4.75  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)).
% 4.55/4.75  cnf(c101,plain,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[rdfs_dat_xmlliteral_sub])).
% 4.55/4.75  cnf(c234,plain,ic(uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c55, c101])).
% 4.55/4.75  cnf(c239,plain,icext(uri_rdfs_Class,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c234, c87])).
% 4.55/4.75  cnf(c473,plain,iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Class),inference(resolution,[status(thm)],[c132, c239])).
% 4.55/4.75  cnf(c949,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X673)|iext(X673,uri_rdf_XMLLiteral,uri_rdfs_Class),inference(resolution,[status(thm)],[c473, c42])).
% 4.55/4.75  cnf(c246,plain,ic(skolem0001),inference(resolution,[status(thm)],[c56, c6])).
% 4.55/4.75  cnf(c250,plain,icext(uri_rdfs_Class,skolem0001),inference(resolution,[status(thm)],[c246, c87])).
% 4.55/4.75  cnf(c472,plain,iext(uri_rdf_type,skolem0001,uri_rdfs_Class),inference(resolution,[status(thm)],[c132, c250])).
% 4.55/4.75  cnf(c944,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X672)|iext(X672,skolem0001,uri_rdfs_Class),inference(resolution,[status(thm)],[c472, c42])).
% 4.55/4.75  cnf(c235,plain,ic(uri_rdfs_Seq),inference(resolution,[status(thm)],[c55, c102])).
% 4.55/4.75  cnf(c241,plain,icext(uri_rdfs_Class,uri_rdfs_Seq),inference(resolution,[status(thm)],[c235, c87])).
% 4.55/4.75  cnf(c471,plain,iext(uri_rdf_type,uri_rdfs_Seq,uri_rdfs_Class),inference(resolution,[status(thm)],[c132, c241])).
% 4.55/4.75  cnf(c939,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X671)|iext(X671,uri_rdfs_Seq,uri_rdfs_Class),inference(resolution,[status(thm)],[c471, c42])).
% 4.55/4.75  cnf(c1610,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X670)|icext(X670,uri_rdfs_comment),inference(resolution,[status(thm)],[c1605, c68])).
% 4.55/4.75  cnf(c1609,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X669)|icext(X669,uri_rdfs_comment),inference(resolution,[status(thm)],[c1605, c94])).
% 4.55/4.75  cnf(c249,plain,ic(uri_rdfs_Class),inference(resolution,[status(thm)],[c56, c96])).
% 4.55/4.75  cnf(c256,plain,icext(uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c249, c87])).
% 4.55/4.75  cnf(c468,plain,iext(uri_rdf_type,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c132, c256])).
% 4.55/4.75  cnf(c934,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X668)|iext(X668,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c468, c42])).
% 4.55/4.75  cnf(c1580,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X665)|icext(X665,uri_rdfs_label),inference(resolution,[status(thm)],[c1575, c68])).
% 4.55/4.75  cnf(c247,plain,ic(uri_rdfs_Literal),inference(resolution,[status(thm)],[c56, c101])).
% 4.55/4.75  cnf(c252,plain,icext(uri_rdfs_Class,uri_rdfs_Literal),inference(resolution,[status(thm)],[c247, c87])).
% 4.55/4.75  cnf(c467,plain,iext(uri_rdf_type,uri_rdfs_Literal,uri_rdfs_Class),inference(resolution,[status(thm)],[c132, c252])).
% 4.55/4.75  cnf(c929,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X664)|iext(X664,uri_rdfs_Literal,uri_rdfs_Class),inference(resolution,[status(thm)],[c467, c42])).
% 4.55/4.75  cnf(c1579,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X663)|icext(X663,uri_rdfs_label),inference(resolution,[status(thm)],[c1575, c94])).
% 4.55/4.75  cnf(c233,plain,ic(uri_ex_Clique),inference(resolution,[status(thm)],[c55, c6])).
% 4.55/4.75  cnf(c237,plain,icext(uri_rdfs_Class,uri_ex_Clique),inference(resolution,[status(thm)],[c233, c87])).
% 4.55/4.75  cnf(c466,plain,iext(uri_rdf_type,uri_ex_Clique,uri_rdfs_Class),inference(resolution,[status(thm)],[c132, c237])).
% 4.55/4.75  cnf(c924,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X660)|iext(X660,uri_ex_Clique,uri_rdfs_Class),inference(resolution,[status(thm)],[c466, c42])).
% 4.55/4.75  cnf(c1541,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X657)|icext(X657,uri_rdf_List),inference(resolution,[status(thm)],[c1529, c68])).
% 4.55/4.75  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)).
% 4.55/4.75  cnf(c114,plain,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_container_containermembershipproperty_sub])).
% 4.55/4.75  cnf(c377,plain,ic(uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c114, c55])).
% 4.55/4.75  cnf(c383,plain,icext(uri_rdfs_Class,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c377, c87])).
% 4.55/4.75  cnf(c465,plain,iext(uri_rdf_type,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Class),inference(resolution,[status(thm)],[c132, c383])).
% 4.55/4.75  cnf(c919,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X656)|iext(X656,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Class),inference(resolution,[status(thm)],[c465, c42])).
% 4.55/4.75  cnf(c1539,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X655)|icext(X655,uri_rdf_List),inference(resolution,[status(thm)],[c1529, c94])).
% 4.55/4.75  cnf(c912,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X652)|iext(X652,uri_rdf__2,uri_rdfs_member),inference(resolution,[status(thm)],[c464, c42])).
% 4.55/4.75  cnf(c1491,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X651)|icext(X651,uri_rdf_predicate),inference(resolution,[status(thm)],[c1486, c68])).
% 4.55/4.75  cnf(c1490,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X650)|icext(X650,uri_rdf_predicate),inference(resolution,[status(thm)],[c1486, c94])).
% 4.55/4.75  cnf(c911,plain,~iext(uri_rdfs_subPropertyOf,X649,uri_rdf__2)|iext(uri_rdfs_subPropertyOf,X649,uri_rdfs_member),inference(resolution,[status(thm)],[c464, c31])).
% 4.55/4.75  cnf(c463,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c449, c34])).
% 4.55/4.75  cnf(c905,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X644)|iext(X644,uri_rdfs_isDefinedBy,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c463, c42])).
% 4.55/4.75  cnf(c1443,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X641)|icext(X641,uri_owl_Restriction),inference(resolution,[status(thm)],[c1431, c68])).
% 4.55/4.75  cnf(c1441,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X639)|icext(X639,uri_owl_Restriction),inference(resolution,[status(thm)],[c1431, c94])).
% 4.55/4.75  cnf(c451,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_seeAlso,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c448, c34])).
% 4.55/4.75  cnf(c898,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X635)|iext(X635,uri_rdfs_seeAlso,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c451, c42])).
% 4.55/4.75  cnf(c1411,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X633)|icext(X633,uri_ex_JoesGang),inference(resolution,[status(thm)],[c1328, c68])).
% 4.55/4.75  cnf(c1409,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X632)|icext(X632,uri_ex_JoesGang),inference(resolution,[status(thm)],[c1328, c94])).
% 4.55/4.75  cnf(c435,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Literal,uri_rdfs_Resource),inference(resolution,[status(thm)],[c126, c247])).
% 4.55/4.75  cnf(c889,plain,~iext(uri_rdfs_subClassOf,X627,uri_rdfs_Literal)|iext(uri_rdfs_subClassOf,X627,uri_rdfs_Resource),inference(resolution,[status(thm)],[c435, c46])).
% 4.55/4.75  cnf(c1390,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X625)|icext(X625,uri_rdfs_Statement),inference(resolution,[status(thm)],[c1292, c68])).
% 4.55/4.75  cnf(c888,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X624)|iext(X624,uri_rdfs_Literal,uri_rdfs_Resource),inference(resolution,[status(thm)],[c435, c42])).
% 4.55/4.75  cnf(c1388,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X623)|icext(X623,uri_rdfs_Statement),inference(resolution,[status(thm)],[c1292, c94])).
% 4.55/4.75  cnf(c434,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Resource),inference(resolution,[status(thm)],[c126, c236])).
% 4.55/4.75  cnf(c881,plain,~iext(uri_rdfs_subClassOf,X619,uri_rdfs_Datatype)|iext(uri_rdfs_subClassOf,X619,uri_rdfs_Resource),inference(resolution,[status(thm)],[c434, c46])).
% 4.55/4.75  cnf(c1367,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X617)|icext(X617,uri_owl_Class),inference(resolution,[status(thm)],[c1262, c68])).
% 4.55/4.75  cnf(c880,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X616)|iext(X616,uri_rdfs_Datatype,uri_rdfs_Resource),inference(resolution,[status(thm)],[c434, c42])).
% 4.55/4.75  cnf(c1365,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X615)|icext(X615,uri_owl_Class),inference(resolution,[status(thm)],[c1262, c94])).
% 4.55/4.75  cnf(c433,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Resource),inference(resolution,[status(thm)],[c126, c235])).
% 4.55/4.75  cnf(c873,plain,~iext(uri_rdfs_subClassOf,X611,uri_rdfs_Seq)|iext(uri_rdfs_subClassOf,X611,uri_rdfs_Resource),inference(resolution,[status(thm)],[c433, c46])).
% 4.55/4.75  cnf(c872,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X607)|iext(X607,uri_rdfs_Seq,uri_rdfs_Resource),inference(resolution,[status(thm)],[c433, c42])).
% 4.55/4.75  cnf(c1339,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X606)|icext(X606,uri_owl_ObjectProperty),inference(resolution,[status(thm)],[c1177, c68])).
% 4.55/4.75  cnf(c432,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Container,uri_rdfs_Resource),inference(resolution,[status(thm)],[c126, c248])).
% 4.55/4.75  cnf(c865,plain,~iext(uri_rdfs_subClassOf,X605,uri_rdfs_Container)|iext(uri_rdfs_subClassOf,X605,uri_rdfs_Resource),inference(resolution,[status(thm)],[c432, c46])).
% 4.55/4.75  cnf(c1337,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X604)|icext(X604,uri_owl_ObjectProperty),inference(resolution,[status(thm)],[c1177, c94])).
% 4.55/4.75  cnf(c864,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X601)|iext(X601,uri_rdfs_Container,uri_rdfs_Resource),inference(resolution,[status(thm)],[c432, c42])).
% 4.55/4.75  cnf(c431,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c126, c249])).
% 4.55/4.75  cnf(c857,plain,~iext(uri_rdfs_subClassOf,X598,uri_rdfs_Class)|iext(uri_rdfs_subClassOf,X598,uri_rdfs_Resource),inference(resolution,[status(thm)],[c431, c46])).
% 4.55/4.75  cnf(c1313,plain,~iext(uri_rdfs_range,uri_rdf_type,X597)|icext(X597,skolem0001),inference(resolution,[status(thm)],[c1080, c68])).
% 4.55/4.75  cnf(c856,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X594)|iext(X594,uri_rdfs_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c431, c42])).
% 4.55/4.75  cnf(c1304,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X593)|icext(X593,uri_rdfs_member),inference(resolution,[status(thm)],[c917, c94])).
% 4.55/4.75  cnf(c430,plain,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Resource),inference(resolution,[status(thm)],[c126, c390])).
% 4.55/4.75  cnf(c849,plain,~iext(uri_rdfs_subClassOf,X589,uri_rdf_Bag)|iext(uri_rdfs_subClassOf,X589,uri_rdfs_Resource),inference(resolution,[status(thm)],[c430, c46])).
% 4.55/4.75  cnf(c1276,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X586)|icext(X586,uri_rdfs_Resource),inference(resolution,[status(thm)],[c803, c94])).
% 4.55/4.75  cnf(c848,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X585)|iext(X585,uri_rdf_Bag,uri_rdfs_Resource),inference(resolution,[status(thm)],[c430, c42])).
% 4.55/4.75  cnf(c1268,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X584)|icext(X584,uri_owl_inverseOf),inference(resolution,[status(thm)],[c697, c68])).
% 4.55/4.75  cnf(c429,plain,iext(uri_rdfs_subClassOf,skolem0001,uri_rdfs_Resource),inference(resolution,[status(thm)],[c126, c246])).
% 4.55/4.75  cnf(c841,plain,~iext(uri_rdfs_subClassOf,X583,skolem0001)|iext(uri_rdfs_subClassOf,X583,uri_rdfs_Resource),inference(resolution,[status(thm)],[c429, c46])).
% 4.55/4.75  cnf(c1267,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X582)|icext(X582,uri_owl_inverseOf),inference(resolution,[status(thm)],[c697, c94])).
% 4.55/4.75  cnf(c840,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X579)|iext(X579,skolem0001,uri_rdfs_Resource),inference(resolution,[status(thm)],[c429, c42])).
% 4.55/4.76  cnf(c1249,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X578)|icext(X578,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c688, c94])).
% 4.55/4.76  cnf(c1247,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X577)|icext(X577,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c688, c68])).
% 4.55/4.76  cnf(c382,plain,ic(uri_rdf_Property),inference(resolution,[status(thm)],[c114, c56])).
% 4.55/4.76  cnf(c428,plain,iext(uri_rdfs_subClassOf,uri_rdf_Property,uri_rdfs_Resource),inference(resolution,[status(thm)],[c126, c382])).
% 4.55/4.76  cnf(c833,plain,~iext(uri_rdfs_subClassOf,X576,uri_rdf_Property)|iext(uri_rdfs_subClassOf,X576,uri_rdfs_Resource),inference(resolution,[status(thm)],[c428, c46])).
% 4.55/4.76  cnf(c1231,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X573)|icext(X573,uri_owl_someValuesFrom),inference(resolution,[status(thm)],[c686, c94])).
% 4.55/4.76  cnf(c832,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X572)|iext(X572,uri_rdf_Property,uri_rdfs_Resource),inference(resolution,[status(thm)],[c428, c42])).
% 4.55/4.76  cnf(c1228,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X571)|icext(X571,uri_owl_someValuesFrom),inference(resolution,[status(thm)],[c686, c68])).
% 4.55/4.76  cnf(c427,plain,iext(uri_rdfs_subClassOf,uri_ex_Clique,uri_rdfs_Resource),inference(resolution,[status(thm)],[c126, c233])).
% 4.55/4.76  cnf(c825,plain,~iext(uri_rdfs_subClassOf,X568,uri_ex_Clique)|iext(uri_rdfs_subClassOf,X568,uri_rdfs_Resource),inference(resolution,[status(thm)],[c427, c46])).
% 4.55/4.76  cnf(c1211,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X567)|icext(X567,uri_rdfs_range),inference(resolution,[status(thm)],[c676, c94])).
% 4.55/4.76  cnf(c1203,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X566)|icext(X566,uri_rdfs_range),inference(resolution,[status(thm)],[c676, c68])).
% 4.55/4.76  cnf(c824,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X565)|iext(X565,uri_ex_Clique,uri_rdfs_Resource),inference(resolution,[status(thm)],[c427, c42])).
% 4.55/4.76  cnf(c1186,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X562)|icext(X562,uri_owl_onProperty),inference(resolution,[status(thm)],[c674, c94])).
% 4.55/4.76  cnf(c426,plain,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Resource),inference(resolution,[status(thm)],[c126, c377])).
% 4.55/4.76  cnf(c817,plain,~iext(uri_rdfs_subClassOf,X561,uri_rdfs_ContainerMembershipProperty)|iext(uri_rdfs_subClassOf,X561,uri_rdfs_Resource),inference(resolution,[status(thm)],[c426, c46])).
% 4.55/4.76  cnf(c1183,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X560)|icext(X560,uri_owl_onProperty),inference(resolution,[status(thm)],[c674, c68])).
% 4.55/4.76  cnf(c816,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X557)|iext(X557,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Resource),inference(resolution,[status(thm)],[c426, c42])).
% 4.55/4.76  cnf(c1162,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X556)|icext(X556,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c672, c94])).
% 4.55/4.76  cnf(c1158,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X555)|icext(X555,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c672, c68])).
% 4.55/4.76  cnf(c425,plain,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Resource),inference(resolution,[status(thm)],[c126, c234])).
% 4.55/4.76  cnf(c809,plain,~iext(uri_rdfs_subClassOf,X554,uri_rdf_XMLLiteral)|iext(uri_rdfs_subClassOf,X554,uri_rdfs_Resource),inference(resolution,[status(thm)],[c425, c46])).
% 4.55/4.76  cnf(c1140,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X551)|icext(X551,uri_rdfs_domain),inference(resolution,[status(thm)],[c670, c94])).
% 4.55/4.76  cnf(c808,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X550)|iext(X550,uri_rdf_XMLLiteral,uri_rdfs_Resource),inference(resolution,[status(thm)],[c425, c42])).
% 4.55/4.76  cnf(c1133,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X549)|icext(X549,uri_rdfs_domain),inference(resolution,[status(thm)],[c670, c68])).
% 4.55/4.76  cnf(c796,plain,~iext(uri_rdfs_subClassOf,X546,uri_rdf_Alt)|iext(uri_rdfs_subClassOf,X546,uri_rdfs_Resource),inference(resolution,[status(thm)],[c424, c46])).
% 4.55/4.76  cnf(c1116,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X545)|icext(X545,uri_owl_propertyChainAxiom),inference(resolution,[status(thm)],[c668, c94])).
% 4.55/4.76  cnf(c1114,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X544)|icext(X544,uri_owl_propertyChainAxiom),inference(resolution,[status(thm)],[c668, c68])).
% 4.55/4.76  cnf(c795,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X543)|iext(X543,uri_rdf_Alt,uri_rdfs_Resource),inference(resolution,[status(thm)],[c424, c42])).
% 4.55/4.76  cnf(c1100,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X540)|icext(X540,uri_rdf_first),inference(resolution,[status(thm)],[c585, c94])).
% 4.55/4.76  cnf(c1097,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X538)|icext(X538,uri_rdf_first),inference(resolution,[status(thm)],[c585, c68])).
% 4.55/4.76  cnf(c1090,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X537)|icext(X537,uri_rdf_rest),inference(resolution,[status(thm)],[c572, c94])).
% 4.55/4.76  cnf(c406,plain,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdf_Alt),inference(resolution,[status(thm)],[c399, c49])).
% 4.55/4.76  cnf(c787,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X536)|iext(X536,uri_rdf_Alt,uri_rdf_Alt),inference(resolution,[status(thm)],[c406, c42])).
% 4.55/4.76  cnf(c1085,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X535)|icext(X535,uri_rdf_rest),inference(resolution,[status(thm)],[c572, c68])).
% 4.55/4.76  cnf(c1076,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X533)|icext(X533,uri_rdf__1),inference(resolution,[status(thm)],[c570, c68])).
% 4.55/4.76  cnf(c1069,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X530)|icext(X530,uri_rdf__2),inference(resolution,[status(thm)],[c556, c68])).
% 4.55/4.76  cnf(c397,plain,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdf_Bag),inference(resolution,[status(thm)],[c390, c49])).
% 4.55/4.76  cnf(c779,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X528)|iext(X528,uri_rdf_Bag,uri_rdf_Bag),inference(resolution,[status(thm)],[c397, c42])).
% 4.55/4.76  cnf(c1062,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X527)|icext(X527,uri_rdf__3),inference(resolution,[status(thm)],[c554, c68])).
% 4.55/4.76  cnf(c1057,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X526)|icext(X526,uri_rdf_object),inference(resolution,[status(thm)],[c541, c94])).
% 4.55/4.76  cnf(c1055,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X525)|icext(X525,uri_rdf_object),inference(resolution,[status(thm)],[c541, c68])).
% 4.55/4.76  cnf(c386,plain,iext(uri_rdfs_subClassOf,uri_rdf_Property,uri_rdf_Property),inference(resolution,[status(thm)],[c382, c49])).
% 4.55/4.76  cnf(c771,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X519)|iext(X519,uri_rdf_Property,uri_rdf_Property),inference(resolution,[status(thm)],[c386, c42])).
% 4.55/4.76  cnf(c1020,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X513)|icext(X513,uri_rdf_value),inference(resolution,[status(thm)],[c526, c94])).
% 4.55/4.76  cnf(c1018,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X512)|icext(X512,uri_rdf_value),inference(resolution,[status(thm)],[c526, c68])).
% 4.55/4.76  cnf(c384,plain,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c377, c49])).
% 4.55/4.76  cnf(c763,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X511)|iext(X511,uri_rdfs_ContainerMembershipProperty,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c384, c42])).
% 4.55/4.76  cnf(c1012,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X510)|icext(X510,uri_rdf_subject),inference(resolution,[status(thm)],[c519, c94])).
% 4.55/4.76  cnf(c1010,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X509)|icext(X509,uri_rdf_subject),inference(resolution,[status(thm)],[c519, c68])).
% 4.55/4.76  cnf(c1002,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X508)|icext(X508,uri_rdf_type),inference(resolution,[status(thm)],[c518, c94])).
% 4.55/4.76  cnf(c996,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X506)|icext(X506,uri_rdf_type),inference(resolution,[status(thm)],[c518, c68])).
% 4.55/4.76  cnf(c988,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X505)|icext(X505,uri_rdf__3),inference(resolution,[status(thm)],[c492, c94])).
% 4.55/4.76  cnf(c257,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c249, c49])).
% 4.55/4.76  cnf(c755,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X504)|iext(X504,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c257, c42])).
% 4.55/4.76  cnf(c979,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X502)|icext(X502,uri_rdf__1),inference(resolution,[status(thm)],[c483, c94])).
% 4.55/4.76  cnf(c255,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Container,uri_rdfs_Container),inference(resolution,[status(thm)],[c248, c49])).
% 4.55/4.76  cnf(c747,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X494)|iext(X494,uri_rdfs_Container,uri_rdfs_Container),inference(resolution,[status(thm)],[c255, c42])).
% 4.55/4.76  cnf(c253,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Literal,uri_rdfs_Literal),inference(resolution,[status(thm)],[c247, c49])).
% 4.55/4.76  cnf(c739,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X483)|iext(X483,uri_rdfs_Literal,uri_rdfs_Literal),inference(resolution,[status(thm)],[c253, c42])).
% 4.55/4.76  cnf(c251,plain,iext(uri_rdfs_subClassOf,skolem0001,skolem0001),inference(resolution,[status(thm)],[c246, c49])).
% 4.55/4.76  cnf(c731,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X473)|iext(X473,skolem0001,skolem0001),inference(resolution,[status(thm)],[c251, c42])).
% 4.55/4.76  cnf(c915,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X472)|icext(X472,uri_rdf__2),inference(resolution,[status(thm)],[c464, c94])).
% 4.55/4.76  cnf(c913,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X471)|icext(X471,uri_rdfs_member),inference(resolution,[status(thm)],[c464, c68])).
% 4.55/4.76  cnf(c906,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X468)|icext(X468,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c463, c68])).
% 4.55/4.76  cnf(c901,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X467)|icext(X467,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c451, c94])).
% 4.55/4.76  cnf(c244,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c236, c49])).
% 4.55/4.76  cnf(c723,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X465)|iext(X465,uri_rdfs_Datatype,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c244, c42])).
% 4.55/4.76  cnf(c242,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Seq),inference(resolution,[status(thm)],[c235, c49])).
% 4.55/4.76  cnf(c715,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X454)|iext(X454,uri_rdfs_Seq,uri_rdfs_Seq),inference(resolution,[status(thm)],[c242, c42])).
% 4.55/4.76  cnf(c240,plain,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c234, c49])).
% 4.55/4.76  cnf(c707,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X443)|iext(X443,uri_rdf_XMLLiteral,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c240, c42])).
% 4.55/4.76  cnf(c797,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X436)|icext(X436,uri_rdfs_Resource),inference(resolution,[status(thm)],[c424, c68])).
% 4.55/4.76  cnf(c238,plain,iext(uri_rdfs_subClassOf,uri_ex_Clique,uri_ex_Clique),inference(resolution,[status(thm)],[c233, c49])).
% 4.55/4.76  cnf(c699,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X434)|iext(X434,uri_ex_Clique,uri_ex_Clique),inference(resolution,[status(thm)],[c238, c42])).
% 4.55/4.76  cnf(c789,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X433)|icext(X433,uri_rdf_Alt),inference(resolution,[status(thm)],[c406, c68])).
% 4.55/4.76  cnf(c781,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X431)|icext(X431,uri_rdf_Bag),inference(resolution,[status(thm)],[c397, c68])).
% 4.55/4.76  cnf(c777,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X429)|icext(X429,uri_rdf_Property),inference(resolution,[status(thm)],[c386, c94])).
% 4.55/4.76  cnf(c175,plain,iext(uri_rdfs_subPropertyOf,uri_owl_sameAs,uri_owl_sameAs),inference(resolution,[status(thm)],[c174, c34])).
% 4.55/4.76  cnf(c690,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X426)|iext(X426,uri_owl_sameAs,uri_owl_sameAs),inference(resolution,[status(thm)],[c175, c42])).
% 4.55/4.76  cnf(c765,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X425)|icext(X425,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c384, c68])).
% 4.55/4.76  cnf(c761,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X424)|icext(X424,uri_rdfs_Class),inference(resolution,[status(thm)],[c257, c94])).
% 4.55/4.76  cnf(c753,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X421)|icext(X421,uri_rdfs_Container),inference(resolution,[status(thm)],[c255, c94])).
% 4.55/4.76  cnf(c745,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X419)|icext(X419,uri_rdfs_Literal),inference(resolution,[status(thm)],[c253, c94])).
% 4.55/4.76  cnf(c172,plain,iext(uri_rdfs_subPropertyOf,uri_ex_sameCliqueAs,uri_ex_sameCliqueAs),inference(resolution,[status(thm)],[c171, c34])).
% 4.55/4.76  cnf(c678,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X418)|iext(X418,uri_ex_sameCliqueAs,uri_ex_sameCliqueAs),inference(resolution,[status(thm)],[c172, c42])).
% 4.55/4.76  cnf(c737,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X416)|icext(X416,skolem0001),inference(resolution,[status(thm)],[c251, c94])).
% 4.55/4.76  cnf(c580,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X414)|iext(X414,uri_rdf_first,uri_rdf_Property),inference(resolution,[status(thm)],[c158, c42])).
% 4.55/4.76  cnf(c725,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X412)|icext(X412,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c244, c68])).
% 4.55/4.76  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)).
% 4.55/4.76  cnf(c157,plain,iext(uri_rdf_type,uri_rdf_nil,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdf_collection_nil_type])).
% 4.55/4.76  cnf(c575,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X410)|iext(X410,uri_rdf_nil,uri_rdf_List),inference(resolution,[status(thm)],[c157, c42])).
% 4.55/4.76  cnf(c717,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X409)|icext(X409,uri_rdfs_Seq),inference(resolution,[status(thm)],[c242, c68])).
% 4.55/4.76  cnf(c565,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X407)|iext(X407,uri_rdf_rest,uri_rdf_Property),inference(resolution,[status(thm)],[c156, c42])).
% 4.55/4.76  cnf(c709,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X406)|icext(X406,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c240, c68])).
% 4.55/4.76  cnf(c701,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X404)|icext(X404,uri_ex_Clique),inference(resolution,[status(thm)],[c238, c68])).
% 4.55/4.76  cnf(c560,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X403)|iext(X403,uri_rdf__1,uri_rdf_Property),inference(resolution,[status(thm)],[c155, c42])).
% 4.55/4.76  cnf(c691,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X401)|icext(X401,uri_owl_sameAs),inference(resolution,[status(thm)],[c175, c94])).
% 4.55/4.76  cnf(c549,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X400)|iext(X400,uri_rdf__2,uri_rdf_Property),inference(resolution,[status(thm)],[c154, c42])).
% 4.55/4.76  cnf(c680,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X399)|icext(X399,uri_ex_sameCliqueAs),inference(resolution,[status(thm)],[c172, c68])).
% 4.55/4.76  cnf(c544,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X395)|iext(X395,uri_rdf__3,uri_rdf_Property),inference(resolution,[status(thm)],[c153, c42])).
% 4.55/4.76  cnf(c577,plain,~iext(uri_rdfs_range,uri_rdf_type,X394)|icext(X394,uri_rdf_List),inference(resolution,[status(thm)],[c157, c68])).
% 4.55/4.76  cnf(c536,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X391)|iext(X391,uri_rdf_object,uri_rdf_Property),inference(resolution,[status(thm)],[c152, c42])).
% 4.55/4.76  cnf(c522,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X386)|iext(X386,uri_rdf_value,uri_rdf_Property),inference(resolution,[status(thm)],[c151, c42])).
% 4.55/4.76  cnf(c512,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X381)|iext(X381,uri_rdf_subject,uri_rdf_Property),inference(resolution,[status(thm)],[c150, c42])).
% 4.55/4.76  cnf(c507,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X376)|iext(X376,uri_rdf_type,uri_rdf_Property),inference(resolution,[status(thm)],[c142, c42])).
% 4.55/4.76  cnf(c509,plain,~iext(uri_rdfs_range,uri_rdf_type,X374)|icext(X374,uri_rdf_Property),inference(resolution,[status(thm)],[c142, c68])).
% 4.55/4.76  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)).
% 4.55/4.76  cnf(c141,plain,iext(uri_rdfs_domain,uri_rdfs_comment,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_comment_domain])).
% 4.55/4.76  cnf(c504,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X372)|iext(X372,uri_rdfs_comment,uri_rdfs_Resource),inference(resolution,[status(thm)],[c141, c42])).
% 4.55/4.76  cnf(c505,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X370)|icext(X370,uri_rdfs_comment),inference(resolution,[status(thm)],[c141, c94])).
% 4.55/4.76  cnf(c501,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X368)|iext(X368,uri_rdfs_comment,uri_rdfs_Literal),inference(resolution,[status(thm)],[c140, c42])).
% 4.55/4.76  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)).
% 4.55/4.76  cnf(c139,plain,iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_domain])).
% 4.55/4.76  cnf(c498,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X367)|iext(X367,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(resolution,[status(thm)],[c139, c42])).
% 4.55/4.76  fof(simple_ir,axiom,(![X]:ir(X)),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', simple_ir)).
% 4.55/4.76  fof(c162,plain,(![X46]:ir(X46)),inference(variable_rename,[status(thm)],[simple_ir])).
% 4.55/4.76  cnf(c163,plain,ir(X50),inference(split_conjunct,[status(thm)],[c162])).
% 4.55/4.76  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)).
% 4.55/4.76  fof(c77,plain,(![X]:((~ir(X)|icext(uri_rdfs_Resource,X))&(~icext(uri_rdfs_Resource,X)|ir(X)))),inference(fof_nnf,[status(thm)],[rdfs_ir_def])).
% 4.55/4.76  fof(c78,plain,((![X]:(~ir(X)|icext(uri_rdfs_Resource,X)))&(![X]:(~icext(uri_rdfs_Resource,X)|ir(X)))),inference(shift_quantors,[status(thm)],[c77])).
% 4.55/4.76  fof(c80,plain,(![X28]:(![X29]:((~ir(X28)|icext(uri_rdfs_Resource,X28))&(~icext(uri_rdfs_Resource,X29)|ir(X29))))),inference(shift_quantors,[status(thm)],[fof(c79,plain,((![X28]:(~ir(X28)|icext(uri_rdfs_Resource,X28)))&(![X29]:(~icext(uri_rdfs_Resource,X29)|ir(X29)))),inference(variable_rename,[status(thm)],[c78])).])).
% 4.55/4.76  cnf(c81,plain,~ir(X60)|icext(uri_rdfs_Resource,X60),inference(split_conjunct,[status(thm)],[c80])).
% 4.55/4.76  cnf(c173,plain,icext(uri_rdfs_Resource,X61),inference(resolution,[status(thm)],[c81, c163])).
% 4.55/4.76  cnf(c470,plain,iext(uri_rdf_type,X97,uri_rdfs_Resource),inference(resolution,[status(thm)],[c132, c173])).
% 4.55/4.76  cnf(c494,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X364)|iext(X364,X365,uri_rdfs_Resource),inference(resolution,[status(thm)],[c470, c42])).
% 4.55/4.76  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)).
% 4.55/4.76  cnf(c138,plain,iext(uri_rdfs_range,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_range])).
% 4.55/4.76  cnf(c488,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X361)|iext(X361,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(resolution,[status(thm)],[c138, c42])).
% 4.55/4.76  cnf(c499,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X360)|icext(X360,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c139, c94])).
% 4.55/4.76  cnf(c496,plain,~iext(uri_rdfs_range,uri_rdf_type,X359)|icext(X359,uri_rdfs_Resource),inference(resolution,[status(thm)],[c470, c68])).
% 4.55/4.76  cnf(c450,plain,~iext(uri_rdfs_subPropertyOf,X358,uri_rdfs_isDefinedBy)|iext(uri_rdfs_subPropertyOf,X358,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c137, c31])).
% 4.55/4.76  cnf(c489,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X356)|icext(X356,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c138, c94])).
% 4.55/4.76  cnf(c445,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X355)|iext(X355,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c137, c42])).
% 4.55/4.76  cnf(c447,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X354)|icext(X354,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c137, c68])).
% 4.55/4.76  cnf(c446,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X353)|icext(X353,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c137, c94])).
% 4.55/4.76  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)).
% 4.55/4.76  cnf(c136,plain,iext(uri_rdfs_domain,uri_rdfs_label,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_label_domain])).
% 4.55/4.76  cnf(c442,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X351)|iext(X351,uri_rdfs_label,uri_rdfs_Resource),inference(resolution,[status(thm)],[c136, c42])).
% 4.55/4.76  cnf(c443,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X350)|icext(X350,uri_rdfs_label),inference(resolution,[status(thm)],[c136, c94])).
% 4.55/4.76  cnf(c441,plain,~iext(uri_rdfs_range,uri_rdfs_range,X349)|icext(X349,uri_rdfs_Literal),inference(resolution,[status(thm)],[c135, c68])).
% 4.55/4.76  cnf(c439,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X348)|iext(X348,uri_rdfs_label,uri_rdfs_Literal),inference(resolution,[status(thm)],[c135, c42])).
% 4.55/4.76  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)).
% 4.55/4.76  cnf(c134,plain,iext(uri_rdfs_domain,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_seealso_domain])).
% 4.55/4.76  cnf(c436,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X347)|iext(X347,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(resolution,[status(thm)],[c134, c42])).
% 4.55/4.76  cnf(c437,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X344)|icext(X344,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c134, c94])).
% 4.55/4.76  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)).
% 4.55/4.76  cnf(c133,plain,iext(uri_rdfs_range,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_seealso_range])).
% 4.55/4.76  cnf(c421,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X343)|iext(X343,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(resolution,[status(thm)],[c133, c42])).
% 4.55/4.76  cnf(c422,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X341)|icext(X341,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c133, c94])).
% 4.55/4.76  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)).
% 4.55/4.76  cnf(c123,plain,iext(uri_rdfs_domain,uri_rdf_first,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdfs_collection_first_domain])).
% 4.55/4.76  cnf(c418,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X339)|iext(X339,uri_rdf_first,uri_rdf_List),inference(resolution,[status(thm)],[c123, c42])).
% 4.55/4.76  cnf(c419,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X338)|icext(X338,uri_rdf_first),inference(resolution,[status(thm)],[c123, c94])).
% 4.55/4.76  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)).
% 4.55/4.76  cnf(c122,plain,iext(uri_rdfs_range,uri_rdf_first,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_collection_first_range])).
% 4.55/4.76  cnf(c415,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X336)|iext(X336,uri_rdf_first,uri_rdfs_Resource),inference(resolution,[status(thm)],[c122, c42])).
% 4.55/4.76  cnf(c416,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X335)|icext(X335,uri_rdf_first),inference(resolution,[status(thm)],[c122, c94])).
% 4.55/4.76  cnf(c414,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X334)|icext(X334,uri_rdf_List),inference(resolution,[status(thm)],[c121, c68])).
% 4.55/4.76  cnf(c412,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X333)|iext(X333,uri_rdf_rest,uri_rdf_List),inference(resolution,[status(thm)],[c121, c42])).
% 4.55/4.76  cnf(c413,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X332)|icext(X332,uri_rdf_rest),inference(resolution,[status(thm)],[c121, c94])).
% 4.55/4.76  cnf(c409,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X329)|iext(X329,uri_rdf_rest,uri_rdf_List),inference(resolution,[status(thm)],[c120, c42])).
% 4.55/4.76  cnf(c401,plain,~iext(uri_rdfs_subClassOf,X328,uri_rdf_Alt)|iext(uri_rdfs_subClassOf,X328,uri_rdfs_Container),inference(resolution,[status(thm)],[c119, c46])).
% 4.55/4.76  cnf(c398,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X327)|iext(X327,uri_rdf_Alt,uri_rdfs_Container),inference(resolution,[status(thm)],[c119, c42])).
% 4.55/4.76  cnf(c392,plain,~iext(uri_rdfs_subClassOf,X326,uri_rdf_Bag)|iext(uri_rdfs_subClassOf,X326,uri_rdfs_Container),inference(resolution,[status(thm)],[c118, c46])).
% 4.55/4.76  cnf(c410,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X324)|icext(X324,uri_rdf_rest),inference(resolution,[status(thm)],[c120, c94])).
% 4.55/4.76  cnf(c389,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X323)|iext(X323,uri_rdf_Bag,uri_rdfs_Container),inference(resolution,[status(thm)],[c118, c42])).
% 4.55/4.76  cnf(c400,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X321)|icext(X321,uri_rdf_Alt),inference(resolution,[status(thm)],[c119, c94])).
% 4.55/4.76  cnf(c379,plain,~iext(uri_rdfs_subClassOf,X319,uri_rdfs_ContainerMembershipProperty)|iext(uri_rdfs_subClassOf,X319,uri_rdf_Property),inference(resolution,[status(thm)],[c114, c46])).
% 4.55/4.76  cnf(c391,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X318)|icext(X318,uri_rdf_Bag),inference(resolution,[status(thm)],[c118, c94])).
% 4.55/4.76  cnf(c380,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X317)|icext(X317,uri_rdf_Property),inference(resolution,[status(thm)],[c114, c68])).
% 4.55/4.76  cnf(c376,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X316)|iext(X316,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),inference(resolution,[status(thm)],[c114, c42])).
% 4.55/4.76  cnf(c378,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X315)|icext(X315,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c114, c94])).
% 4.55/4.76  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)).
% 4.55/4.76  cnf(c113,plain,iext(uri_rdfs_domain,uri_rdfs_member,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_member_domain])).
% 4.55/4.76  cnf(c373,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X313)|iext(X313,uri_rdfs_member,uri_rdfs_Resource),inference(resolution,[status(thm)],[c113, c42])).
% 4.55/4.76  cnf(c374,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X312)|icext(X312,uri_rdfs_member),inference(resolution,[status(thm)],[c113, c94])).
% 4.55/4.76  cnf(c369,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X310)|icext(X310,uri_rdfs_range),inference(resolution,[status(thm)],[c94, c65])).
% 4.55/4.76  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)).
% 4.55/4.76  cnf(c43,plain,iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_subpropertyof_domain])).
% 4.55/4.76  cnf(c367,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X308)|icext(X308,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c94, c43])).
% 4.55/4.76  cnf(c365,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X306)|icext(X306,uri_rdfs_range),inference(resolution,[status(thm)],[c94, c69])).
% 4.55/4.76  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)).
% 4.55/4.76  cnf(c28,plain,iext(uri_rdfs_domain,uri_rdf_type,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_type_domain])).
% 4.55/4.76  cnf(c364,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X305)|icext(X305,uri_rdf_type),inference(resolution,[status(thm)],[c94, c28])).
% 4.55/4.76  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)).
% 4.55/4.76  cnf(c107,plain,iext(uri_rdfs_range,uri_rdf__2,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_range_002])).
% 4.55/4.76  cnf(c363,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X304)|icext(X304,uri_rdf__2),inference(resolution,[status(thm)],[c94, c107])).
% 4.55/4.76  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)).
% 4.55/4.76  cnf(c50,plain,iext(uri_rdfs_range,uri_rdfs_subClassOf,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_subclassof_range])).
% 4.55/4.76  cnf(c362,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X303)|icext(X303,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c94, c50])).
% 4.55/4.76  cnf(c5,plain,iext(uri_rdfs_range,uri_ex_sameCliqueAs,uri_ex_Clique),inference(split_conjunct,[status(thm)],[c2])).
% 4.55/4.76  cnf(c361,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X302)|icext(X302,uri_ex_sameCliqueAs),inference(resolution,[status(thm)],[c94, c5])).
% 4.55/4.76  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)).
% 4.55/4.76  cnf(c109,plain,iext(uri_rdfs_domain,uri_rdf__3,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_003])).
% 4.55/4.76  cnf(c360,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X301)|icext(X301,uri_rdf__3),inference(resolution,[status(thm)],[c94, c109])).
% 4.55/4.76  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)).
% 4.55/4.76  cnf(c35,plain,iext(uri_rdfs_range,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_subpropertyof_range])).
% 4.55/4.76  cnf(c359,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X300)|icext(X300,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c94, c35])).
% 4.55/4.76  cnf(c358,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X299)|icext(X299,uri_ex_sameCliqueAs),inference(resolution,[status(thm)],[c94, c4])).
% 4.55/4.76  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)).
% 4.55/4.76  cnf(c26,plain,iext(uri_rdfs_domain,uri_rdf_value,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_value_domain])).
% 4.55/4.76  cnf(c357,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X298)|icext(X298,uri_rdf_value),inference(resolution,[status(thm)],[c94, c26])).
% 4.55/4.76  cnf(c356,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X297)|icext(X297,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c94, c96])).
% 4.55/4.76  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)).
% 4.55/4.76  cnf(c110,plain,iext(uri_rdfs_domain,uri_rdf__2,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_002])).
% 4.55/4.76  cnf(c355,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X296)|icext(X296,uri_rdf__2),inference(resolution,[status(thm)],[c94, c110])).
% 4.55/4.76  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)).
% 4.55/4.76  cnf(c106,plain,iext(uri_rdfs_range,uri_rdf__3,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_range_003])).
% 4.55/4.76  cnf(c354,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X295)|icext(X295,uri_rdf__3),inference(resolution,[status(thm)],[c94, c106])).
% 4.55/4.76  cnf(c353,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X294)|icext(X294,uri_rdf_type),inference(resolution,[status(thm)],[c94, c27])).
% 4.55/4.76  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)).
% 4.55/4.76  cnf(c25,plain,iext(uri_rdfs_range,uri_rdf_value,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_value_range])).
% 4.55/4.76  cnf(c352,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X293)|icext(X293,uri_rdf_value),inference(resolution,[status(thm)],[c94, c25])).
% 4.55/4.76  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)).
% 4.55/4.76  cnf(c108,plain,iext(uri_rdfs_range,uri_rdf__1,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_range_001])).
% 4.55/4.76  cnf(c351,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X292)|icext(X292,uri_rdf__1),inference(resolution,[status(thm)],[c94, c108])).
% 4.55/4.76  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)).
% 4.55/4.76  cnf(c61,plain,iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_reification_predicate_range])).
% 4.55/4.76  cnf(c347,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X288)|icext(X288,uri_rdf_predicate),inference(resolution,[status(thm)],[c94, c61])).
% 4.55/4.76  cnf(c346,plain,~iext(uri_rdfs_domain,uri_owl_inverseOf,X287)|icext(X287,skolem0002),inference(resolution,[status(thm)],[c94, c18])).
% 4.55/4.76  cnf(c344,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X285)|icext(X285,uri_rdfs_Seq),inference(resolution,[status(thm)],[c94, c102])).
% 4.55/4.76  cnf(c343,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X284)|icext(X284,uri_rdfs_domain),inference(resolution,[status(thm)],[c94, c89])).
% 4.55/4.76  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)).
% 4.55/4.76  cnf(c60,plain,iext(uri_rdfs_domain,uri_rdf_subject,uri_rdfs_Statement),inference(split_conjunct,[status(thm)],[rdfs_reification_subject_domain])).
% 4.55/4.76  cnf(c340,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X281)|icext(X281,uri_rdf_subject),inference(resolution,[status(thm)],[c94, c60])).
% 4.55/4.76  cnf(c17,plain,iext(uri_rdf_rest,skolem0005,uri_rdf_nil),inference(split_conjunct,[status(thm)],[c2])).
% 4.55/4.76  cnf(c339,plain,~iext(uri_rdfs_domain,uri_rdf_rest,X280)|icext(X280,skolem0005),inference(resolution,[status(thm)],[c94, c17])).
% 4.55/4.76  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)).
% 4.55/4.76  cnf(c59,plain,iext(uri_rdfs_range,uri_rdf_subject,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_reification_subject_range])).
% 4.55/4.76  cnf(c338,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X279)|icext(X279,uri_rdf_subject),inference(resolution,[status(thm)],[c94, c59])).
% 4.55/4.76  cnf(c16,plain,iext(uri_rdf_first,skolem0005,skolem0002),inference(split_conjunct,[status(thm)],[c2])).
% 4.55/4.76  cnf(c337,plain,~iext(uri_rdfs_domain,uri_rdf_first,X278)|icext(X278,skolem0005),inference(resolution,[status(thm)],[c94, c16])).
% 4.55/4.76  cnf(c336,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X277)|icext(X277,uri_rdf_object),inference(resolution,[status(thm)],[c94, c64])).
% 4.55/4.76  cnf(c14,plain,iext(uri_rdf_first,skolem0004,uri_ex_sameCliqueAs),inference(split_conjunct,[status(thm)],[c2])).
% 4.55/4.76  cnf(c335,plain,~iext(uri_rdfs_domain,uri_rdf_first,X276)|icext(X276,skolem0004),inference(resolution,[status(thm)],[c94, c14])).
% 4.55/4.76  cnf(c333,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X274)|icext(X274,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c94, c101])).
% 4.55/4.76  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)).
% 4.55/4.76  cnf(c112,plain,iext(uri_rdfs_range,uri_rdfs_member,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_member_range])).
% 4.55/4.76  cnf(c331,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X272)|icext(X272,uri_rdfs_member),inference(resolution,[status(thm)],[c94, c112])).
% 4.55/4.76  cnf(c330,plain,~iext(uri_rdfs_domain,uri_rdf_rest,X271)|icext(X271,skolem0004),inference(resolution,[status(thm)],[c94, c15])).
% 4.55/4.76  cnf(c329,plain,~iext(uri_rdfs_domain,uri_owl_someValuesFrom,X270)|icext(X270,skolem0001),inference(resolution,[status(thm)],[c94, c9])).
% 4.55/4.76  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)).
% 4.55/4.76  cnf(c58,plain,iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_subclassof_domain])).
% 4.55/4.76  cnf(c327,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X268)|icext(X268,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c94, c58])).
% 4.55/4.76  cnf(c495,plain,~iext(uri_rdfs_domain,uri_rdf_type,X266)|icext(X266,X265),inference(resolution,[status(thm)],[c470, c94])).
% 4.55/4.76  cnf(c12,plain,iext(uri_rdf_first,skolem0003,uri_rdf_type),inference(split_conjunct,[status(thm)],[c2])).
% 4.55/4.76  cnf(c326,plain,~iext(uri_rdfs_domain,uri_rdf_first,X263)|icext(X263,skolem0003),inference(resolution,[status(thm)],[c94, c12])).
% 4.55/4.76  cnf(c325,plain,~iext(uri_rdfs_domain,uri_owl_onProperty,X257)|icext(X257,skolem0001),inference(resolution,[status(thm)],[c94, c8])).
% 4.55/4.76  cnf(c323,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X247)|icext(X247,uri_ex_Clique),inference(resolution,[status(thm)],[c94, c6])).
% 4.55/4.76  cnf(c321,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X240)|icext(X240,uri_rdf__1),inference(resolution,[status(thm)],[c94, c111])).
% 4.55/4.76  cnf(c320,plain,~iext(uri_rdfs_domain,uri_owl_propertyChainAxiom,X239)|icext(X239,uri_foaf_knows),inference(resolution,[status(thm)],[c94, c11])).
% 4.55/4.76  cnf(c319,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X238)|icext(X238,uri_rdfs_domain),inference(factor,[status(thm)],[c94])).
% 4.55/4.76  cnf(c403,plain,~icext(uri_rdf_Alt,X217)|icext(uri_rdfs_Container,X217),inference(resolution,[status(thm)],[c119, c57])).
% 4.55/4.76  cnf(c394,plain,~icext(uri_rdf_Bag,X216)|icext(uri_rdfs_Container,X216),inference(resolution,[status(thm)],[c118, c57])).
% 4.55/4.76  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)).
% 4.55/4.76  cnf(c100,plain,iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Datatype),inference(split_conjunct,[status(thm)],[rdfs_dat_xmlliteral_type])).
% 4.55/4.76  cnf(c312,plain,~iext(uri_rdfs_range,uri_rdf_type,X215)|icext(X215,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c68, c100])).
% 4.55/4.76  cnf(c381,plain,~icext(uri_rdfs_ContainerMembershipProperty,X214)|icext(uri_rdf_Property,X214),inference(resolution,[status(thm)],[c114, c57])).
% 4.55/4.76  cnf(c307,plain,~iext(uri_rdfs_range,uri_rdfs_range,X209)|icext(X209,uri_ex_Clique),inference(resolution,[status(thm)],[c68, c5])).
% 4.55/4.76  cnf(c305,plain,~iext(uri_rdfs_range,uri_rdfs_range,X207)|icext(X207,uri_rdf_Property),inference(resolution,[status(thm)],[c68, c35])).
% 4.55/4.76  cnf(c304,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X206)|icext(X206,uri_owl_sameAs),inference(resolution,[status(thm)],[c68, c4])).
% 4.55/4.76  cnf(c302,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X204)|icext(X204,uri_rdfs_Class),inference(resolution,[status(thm)],[c68, c96])).
% 4.55/4.76  cnf(c294,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X196)|icext(X196,uri_rdf_Property),inference(resolution,[status(thm)],[c68, c95])).
% 4.55/4.76  cnf(c292,plain,~iext(uri_rdfs_range,uri_owl_inverseOf,X194)|icext(X194,uri_rdf_type),inference(resolution,[status(thm)],[c68, c18])).
% 4.55/4.76  cnf(c290,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X192)|icext(X192,uri_rdfs_Container),inference(resolution,[status(thm)],[c68, c102])).
% 4.55/4.76  cnf(c289,plain,~iext(uri_rdfs_range,uri_rdfs_range,X191)|icext(X191,uri_rdfs_Class),inference(resolution,[status(thm)],[c68, c89])).
% 4.55/4.76  cnf(c287,plain,~iext(uri_rdfs_range,uri_rdf_type,X189)|icext(X189,uri_ex_Clique),inference(resolution,[status(thm)],[c68, c19])).
% 4.55/4.76  cnf(c285,plain,~iext(uri_rdfs_range,uri_rdf_rest,X187)|icext(X187,uri_rdf_nil),inference(resolution,[status(thm)],[c68, c17])).
% 4.55/4.76  cnf(c1299,plain,icext(uri_rdf_Property,uri_rdfs_member),inference(resolution,[status(thm)],[c916, c131])).
% 4.55/4.76  cnf(c283,plain,~iext(uri_rdfs_range,uri_rdf_first,X185)|icext(X185,skolem0002),inference(resolution,[status(thm)],[c68, c16])).
% 4.55/4.76  cnf(c281,plain,~iext(uri_rdfs_range,uri_rdf_first,X183)|icext(X183,uri_ex_sameCliqueAs),inference(resolution,[status(thm)],[c68, c14])).
% 4.55/4.76  cnf(c280,plain,~iext(uri_rdfs_range,uri_rdf_type,X182)|icext(X182,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c68, c104])).
% 4.55/4.76  cnf(c279,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X181)|icext(X181,uri_rdfs_Literal),inference(resolution,[status(thm)],[c68, c101])).
% 4.55/4.76  cnf(c1255,plain,icext(uri_rdf_Property,uri_owl_inverseOf),inference(resolution,[status(thm)],[c696, c131])).
% 4.55/4.76  cnf(c277,plain,~iext(uri_rdfs_range,uri_rdfs_range,X179)|icext(X179,uri_rdfs_Resource),inference(resolution,[status(thm)],[c68, c112])).
% 4.55/4.76  cnf(c1236,plain,icext(uri_rdf_Property,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c687, c131])).
% 4.55/4.76  cnf(c275,plain,~iext(uri_rdfs_range,uri_owl_someValuesFrom,X177)|icext(X177,uri_ex_Clique),inference(resolution,[status(thm)],[c68, c9])).
% 4.55/4.76  cnf(c1221,plain,icext(uri_rdf_Property,uri_owl_someValuesFrom),inference(resolution,[status(thm)],[c685, c131])).
% 4.55/4.76  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)).
% 4.55/4.76  cnf(c70,plain,iext(uri_rdf_type,uri_rdf_Property,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_property_type])).
% 4.55/4.76  cnf(c274,plain,~iext(uri_rdfs_range,uri_rdf_type,X176)|icext(X176,uri_rdfs_Class),inference(resolution,[status(thm)],[c68, c70])).
% 4.55/4.76  cnf(c273,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X175)|icext(X175,uri_rdfs_Class),inference(resolution,[status(thm)],[c68, c58])).
% 4.55/4.76  cnf(c1191,plain,icext(uri_rdf_Property,uri_rdfs_range),inference(resolution,[status(thm)],[c675, c131])).
% 4.55/4.76  cnf(c272,plain,~iext(uri_rdfs_range,uri_rdf_first,X174)|icext(X174,uri_rdf_type),inference(resolution,[status(thm)],[c68, c12])).
% 4.55/4.76  cnf(c271,plain,~iext(uri_rdfs_range,uri_owl_onProperty,X173)|icext(X173,uri_ex_sameCliqueAs),inference(resolution,[status(thm)],[c68, c8])).
% 4.55/4.76  cnf(c1170,plain,icext(uri_rdf_Property,uri_owl_onProperty),inference(resolution,[status(thm)],[c673, c131])).
% 4.55/4.76  cnf(c269,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X171)|icext(X171,skolem0001),inference(resolution,[status(thm)],[c68, c6])).
% 4.55/4.76  cnf(c1149,plain,icext(uri_rdf_Property,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c671, c131])).
% 4.55/4.76  cnf(c267,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X169)|icext(X169,uri_rdfs_Resource),inference(resolution,[status(thm)],[c68, c111])).
% 4.55/4.76  cnf(c1122,plain,icext(uri_rdf_Property,uri_rdfs_domain),inference(resolution,[status(thm)],[c669, c131])).
% 4.55/4.76  cnf(c266,plain,~iext(uri_rdfs_range,uri_owl_propertyChainAxiom,X168)|icext(X168,skolem0003),inference(resolution,[status(thm)],[c68, c11])).
% 4.55/4.76  cnf(c265,plain,~iext(uri_rdfs_range,uri_rdfs_range,X167)|icext(X167,X167),inference(factor,[status(thm)],[c68])).
% 4.55/4.76  cnf(c1105,plain,icext(uri_rdf_Property,uri_owl_propertyChainAxiom),inference(resolution,[status(thm)],[c667, c131])).
% 4.55/4.76  cnf(c261,plain,~icext(uri_rdfs_Datatype,X166)|icext(uri_rdfs_Class,X166),inference(resolution,[status(thm)],[c57, c96])).
% 4.55/4.76  cnf(c260,plain,~icext(uri_rdfs_Seq,X165)|icext(uri_rdfs_Container,X165),inference(resolution,[status(thm)],[c57, c102])).
% 4.55/4.76  cnf(c259,plain,~icext(uri_rdf_XMLLiteral,X164)|icext(uri_rdfs_Literal,X164),inference(resolution,[status(thm)],[c57, c101])).
% 4.55/4.76  cnf(c232,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X162)|iext(X162,uri_rdfs_member,uri_rdfs_Resource),inference(resolution,[status(thm)],[c112, c42])).
% 4.55/4.76  cnf(c231,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X161)|iext(X161,uri_rdf__1,uri_rdfs_Resource),inference(resolution,[status(thm)],[c111, c42])).
% 4.55/4.76  cnf(c230,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X160)|iext(X160,uri_rdf__2,uri_rdfs_Resource),inference(resolution,[status(thm)],[c110, c42])).
% 4.55/4.76  cnf(c229,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X159)|iext(X159,uri_rdf__3,uri_rdfs_Resource),inference(resolution,[status(thm)],[c109, c42])).
% 4.55/4.76  cnf(c228,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X158)|iext(X158,uri_rdf__1,uri_rdfs_Resource),inference(resolution,[status(thm)],[c108, c42])).
% 4.55/4.76  cnf(c1048,plain,icext(uri_rdf_Property,uri_ex_sameCliqueAs),inference(resolution,[status(thm)],[c533, c131])).
% 4.55/4.76  cnf(c1041,plain,icext(uri_rdf_Property,uri_owl_sameAs),inference(resolution,[status(thm)],[c532, c131])).
% 4.55/4.76  cnf(c227,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X157)|iext(X157,uri_rdf__2,uri_rdfs_Resource),inference(resolution,[status(thm)],[c107, c42])).
% 4.55/4.76  cnf(c226,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X156)|iext(X156,uri_rdf__3,uri_rdfs_Resource),inference(resolution,[status(thm)],[c106, c42])).
% 4.55/4.76  cnf(c1034,plain,icext(uri_rdf_Property,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c529, c131])).
% 4.55/4.76  cnf(c1026,plain,icext(uri_rdf_Property,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c528, c131])).
% 4.55/4.76  cnf(c225,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X155)|iext(X155,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c105, c42])).
% 4.55/4.76  cnf(c224,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X154)|iext(X154,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c104, c42])).
% 4.55/4.76  cnf(c223,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X153)|iext(X153,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c103, c42])).
% 4.55/4.76  cnf(c222,plain,~iext(uri_rdfs_subClassOf,X152,uri_rdfs_Datatype)|iext(uri_rdfs_subClassOf,X152,uri_rdfs_Class),inference(resolution,[status(thm)],[c46, c96])).
% 4.55/4.76  cnf(c221,plain,~iext(uri_rdfs_subClassOf,X151,uri_rdfs_Seq)|iext(uri_rdfs_subClassOf,X151,uri_rdfs_Container),inference(resolution,[status(thm)],[c46, c102])).
% 4.55/4.76  cnf(c220,plain,~iext(uri_rdfs_subClassOf,X150,uri_rdf_XMLLiteral)|iext(uri_rdfs_subClassOf,X150,uri_rdfs_Literal),inference(resolution,[status(thm)],[c46, c101])).
% 4.55/4.76  cnf(c219,plain,~iext(uri_rdfs_subClassOf,X149,uri_ex_Clique)|iext(uri_rdfs_subClassOf,X149,skolem0001),inference(resolution,[status(thm)],[c46, c6])).
% 4.55/4.76  cnf(c217,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X147)|iext(X147,uri_rdfs_Seq,uri_rdfs_Container),inference(resolution,[status(thm)],[c102, c42])).
% 4.55/4.76  cnf(c216,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X146)|iext(X146,uri_rdf_XMLLiteral,uri_rdfs_Literal),inference(resolution,[status(thm)],[c101, c42])).
% 4.55/4.76  cnf(c215,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X145)|iext(X145,uri_rdf_XMLLiteral,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c100, c42])).
% 4.55/4.76  cnf(c214,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X144)|iext(X144,uri_rdfs_Datatype,uri_rdfs_Class),inference(resolution,[status(thm)],[c96, c42])).
% 4.55/4.76  cnf(c213,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X143)|iext(X143,uri_rdfs_domain,uri_rdf_Property),inference(resolution,[status(thm)],[c95, c42])).
% 4.55/4.76  cnf(c212,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X142)|iext(X142,skolem0001,uri_owl_Restriction),inference(resolution,[status(thm)],[c42, c7])).
% 4.55/4.76  cnf(c211,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X141)|iext(X141,uri_rdfs_range,uri_rdfs_Class),inference(resolution,[status(thm)],[c42, c65])).
% 4.55/4.76  cnf(c210,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X140)|iext(X140,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c42, c43])).
% 4.55/4.76  cnf(c209,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X139)|iext(X139,uri_rdfs_range,uri_rdf_Property),inference(resolution,[status(thm)],[c42, c69])).
% 4.55/4.76  cnf(c208,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X138)|iext(X138,uri_rdf_type,uri_rdfs_Resource),inference(resolution,[status(thm)],[c42, c28])).
% 4.55/4.76  cnf(c207,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X137)|iext(X137,uri_rdfs_subClassOf,uri_rdfs_Class),inference(resolution,[status(thm)],[c42, c50])).
% 4.55/4.76  cnf(c206,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X136)|iext(X136,uri_ex_sameCliqueAs,uri_ex_Clique),inference(resolution,[status(thm)],[c42, c5])).
% 4.55/4.76  cnf(c205,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X135)|iext(X135,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c42, c35])).
% 4.55/4.76  cnf(c204,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X134)|iext(X134,uri_ex_sameCliqueAs,uri_owl_sameAs),inference(resolution,[status(thm)],[c42, c4])).
% 4.55/4.76  cnf(c203,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X133)|iext(X133,uri_rdf_value,uri_rdfs_Resource),inference(resolution,[status(thm)],[c42, c26])).
% 4.55/4.76  cnf(c202,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X132)|iext(X132,uri_rdf_type,uri_rdfs_Class),inference(resolution,[status(thm)],[c42, c27])).
% 4.55/4.76  cnf(c201,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X131)|iext(X131,uri_rdf_value,uri_rdfs_Resource),inference(resolution,[status(thm)],[c42, c25])).
% 4.55/4.76  cnf(c20,plain,iext(uri_rdf_type,uri_ex_alice,uri_ex_JoesGang),inference(split_conjunct,[status(thm)],[c2])).
% 4.55/4.76  cnf(c200,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X130)|iext(X130,uri_ex_alice,uri_ex_JoesGang),inference(resolution,[status(thm)],[c42, c20])).
% 4.55/4.76  cnf(c199,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X129)|iext(X129,uri_ex_bob,uri_ex_JoesGang),inference(resolution,[status(thm)],[c42, c21])).
% 4.55/4.76  cnf(c198,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X128)|iext(X128,uri_rdf_predicate,uri_rdfs_Resource),inference(resolution,[status(thm)],[c42, c61])).
% 4.55/4.76  cnf(c197,plain,~iext(uri_rdfs_subPropertyOf,uri_owl_inverseOf,X127)|iext(X127,skolem0002,uri_rdf_type),inference(resolution,[status(thm)],[c42, c18])).
% 4.55/4.76  cnf(c196,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X126)|iext(X126,uri_rdfs_domain,uri_rdfs_Class),inference(resolution,[status(thm)],[c42, c89])).
% 4.55/4.76  cnf(c195,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X125)|iext(X125,uri_rdf_predicate,uri_rdfs_Statement),inference(resolution,[status(thm)],[c42, c62])).
% 4.55/4.76  cnf(c194,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X124)|iext(X124,uri_ex_JoesGang,uri_ex_Clique),inference(resolution,[status(thm)],[c42, c19])).
% 4.55/4.76  cnf(c193,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X123)|iext(X123,uri_rdf_subject,uri_rdfs_Statement),inference(resolution,[status(thm)],[c42, c60])).
% 4.55/4.76  cnf(c192,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X122)|iext(X122,skolem0005,uri_rdf_nil),inference(resolution,[status(thm)],[c42, c17])).
% 4.55/4.76  cnf(c191,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X121)|iext(X121,uri_rdf_subject,uri_rdfs_Resource),inference(resolution,[status(thm)],[c42, c59])).
% 4.55/4.76  cnf(c190,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_first,X120)|iext(X120,skolem0005,skolem0002),inference(resolution,[status(thm)],[c42, c16])).
% 4.55/4.76  cnf(c189,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X119)|iext(X119,uri_rdf_object,uri_rdfs_Statement),inference(resolution,[status(thm)],[c42, c64])).
% 4.55/4.76  cnf(c188,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_first,X118)|iext(X118,skolem0004,uri_ex_sameCliqueAs),inference(resolution,[status(thm)],[c42, c14])).
% 4.55/4.76  cnf(c187,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X117)|iext(X117,uri_ex_Clique,uri_owl_Class),inference(resolution,[status(thm)],[c42, c3])).
% 4.55/4.76  cnf(c186,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X116)|iext(X116,skolem0004,skolem0005),inference(resolution,[status(thm)],[c42, c15])).
% 4.55/4.76  cnf(c185,plain,~iext(uri_rdfs_subPropertyOf,uri_owl_someValuesFrom,X115)|iext(X115,skolem0001,uri_ex_Clique),inference(resolution,[status(thm)],[c42, c9])).
% 4.55/4.76  cnf(c184,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X114)|iext(X114,uri_rdf_Property,uri_rdfs_Class),inference(resolution,[status(thm)],[c42, c70])).
% 4.55/4.76  cnf(c183,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X113)|iext(X113,uri_rdfs_subClassOf,uri_rdfs_Class),inference(resolution,[status(thm)],[c42, c58])).
% 4.55/4.76  cnf(c182,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_first,X112)|iext(X112,skolem0003,uri_rdf_type),inference(resolution,[status(thm)],[c42, c12])).
% 4.55/4.76  cnf(c181,plain,~iext(uri_rdfs_subPropertyOf,uri_owl_onProperty,X111)|iext(X111,skolem0001,uri_ex_sameCliqueAs),inference(resolution,[status(thm)],[c42, c8])).
% 4.55/4.76  cnf(c180,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X110)|iext(X110,uri_foaf_knows,uri_owl_ObjectProperty),inference(resolution,[status(thm)],[c42, c10])).
% 4.55/4.76  cnf(c179,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X109)|iext(X109,uri_ex_Clique,skolem0001),inference(resolution,[status(thm)],[c42, c6])).
% 4.55/4.76  cnf(c178,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X108)|iext(X108,skolem0003,skolem0004),inference(resolution,[status(thm)],[c42, c13])).
% 4.55/4.76  cnf(c177,plain,~iext(uri_rdfs_subPropertyOf,uri_owl_propertyChainAxiom,X107)|iext(X107,uri_foaf_knows,skolem0003),inference(resolution,[status(thm)],[c42, c11])).
% 4.55/4.76  cnf(c176,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X106)|iext(X106,uri_rdfs_subPropertyOf,X106),inference(factor,[status(thm)],[c42])).
% 4.55/4.76  cnf(c170,plain,~iext(uri_rdfs_subPropertyOf,X105,uri_ex_sameCliqueAs)|iext(uri_rdfs_subPropertyOf,X105,uri_owl_sameAs),inference(resolution,[status(thm)],[c31, c4])).
% 4.55/4.76  cnf(c583,plain,icext(uri_rdf_Property,uri_rdf_first),inference(resolution,[status(thm)],[c158, c131])).
% 4.55/4.76  cnf(c578,plain,icext(uri_rdf_List,uri_rdf_nil),inference(resolution,[status(thm)],[c157, c131])).
% 4.55/4.76  cnf(c568,plain,icext(uri_rdf_Property,uri_rdf_rest),inference(resolution,[status(thm)],[c156, c131])).
% 4.55/4.76  cnf(c563,plain,icext(uri_rdf_Property,uri_rdf__1),inference(resolution,[status(thm)],[c155, c131])).
% 4.55/4.76  cnf(c552,plain,icext(uri_rdf_Property,uri_rdf__2),inference(resolution,[status(thm)],[c154, c131])).
% 4.55/4.76  cnf(c547,plain,icext(uri_rdf_Property,uri_rdf__3),inference(resolution,[status(thm)],[c153, c131])).
% 4.55/4.76  cnf(c539,plain,icext(uri_rdf_Property,uri_rdf_object),inference(resolution,[status(thm)],[c152, c131])).
% 4.55/4.76  cnf(c525,plain,icext(uri_rdf_Property,uri_rdf_value),inference(resolution,[status(thm)],[c151, c131])).
% 4.55/4.76  cnf(c515,plain,icext(uri_rdf_Property,uri_rdf_subject),inference(resolution,[status(thm)],[c150, c131])).
% 4.55/4.76  cnf(c510,plain,icext(uri_rdf_Property,uri_rdf_type),inference(resolution,[status(thm)],[c142, c131])).
% 4.55/4.76  cnf(c462,plain,icext(uri_owl_Restriction,skolem0001),inference(resolution,[status(thm)],[c131, c7])).
% 4.55/4.76  cnf(c460,plain,icext(uri_rdfs_Datatype,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c131, c100])).
% 4.55/4.76  cnf(c459,plain,icext(uri_ex_JoesGang,uri_ex_alice),inference(resolution,[status(thm)],[c131, c20])).
% 4.55/4.76  cnf(c458,plain,icext(uri_ex_JoesGang,uri_ex_bob),inference(resolution,[status(thm)],[c131, c21])).
% 4.55/4.76  cnf(c454,plain,icext(uri_owl_Class,uri_ex_Clique),inference(resolution,[status(thm)],[c131, c3])).
% 4.55/4.76  cnf(c452,plain,icext(uri_owl_ObjectProperty,uri_foaf_knows),inference(resolution,[status(thm)],[c131, c10])).
% 4.55/4.76  cnf(c385,plain,icext(uri_rdfs_Class,uri_rdf_Property),inference(resolution,[status(thm)],[c382, c87])).
% 4.55/4.76  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)).
% 4.55/4.76  fof(c97,plain,(![D]:(~icext(uri_rdfs_Datatype,D)|iext(uri_rdfs_subClassOf,D,uri_rdfs_Literal))),inference(fof_nnf,[status(thm)],[rdfs_datatype_instsub_literal])).
% 4.55/4.76  fof(c98,plain,(![X36]:(~icext(uri_rdfs_Datatype,X36)|iext(uri_rdfs_subClassOf,X36,uri_rdfs_Literal))),inference(variable_rename,[status(thm)],[c97])).
% 4.55/4.76  cnf(c99,plain,~icext(uri_rdfs_Datatype,X90)|iext(uri_rdfs_subClassOf,X90,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[c98])).
% 4.55/4.76  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)).
% 4.55/4.76  fof(c71,plain,(![X]:((~lv(X)|icext(uri_rdfs_Literal,X))&(~icext(uri_rdfs_Literal,X)|lv(X)))),inference(fof_nnf,[status(thm)],[rdfs_lv_def])).
% 4.55/4.76  fof(c72,plain,((![X]:(~lv(X)|icext(uri_rdfs_Literal,X)))&(![X]:(~icext(uri_rdfs_Literal,X)|lv(X)))),inference(shift_quantors,[status(thm)],[c71])).
% 4.55/4.76  fof(c74,plain,(![X26]:(![X27]:((~lv(X26)|icext(uri_rdfs_Literal,X26))&(~icext(uri_rdfs_Literal,X27)|lv(X27))))),inference(shift_quantors,[status(thm)],[fof(c73,plain,((![X26]:(~lv(X26)|icext(uri_rdfs_Literal,X26)))&(![X27]:(~icext(uri_rdfs_Literal,X27)|lv(X27)))),inference(variable_rename,[status(thm)],[c72])).])).
% 4.55/4.76  cnf(c76,plain,~icext(uri_rdfs_Literal,X59)|lv(X59),inference(split_conjunct,[status(thm)],[c74])).
% 4.55/4.76  cnf(c75,plain,~lv(X58)|icext(uri_rdfs_Literal,X58),inference(split_conjunct,[status(thm)],[c74])).
% 4.55/4.76  fof(testcase_conclusion_fullish_013_Cliques,conjecture,iext(uri_foaf_knows,uri_ex_alice,uri_ex_bob),file('/export/starexec/sandbox/benchmark/theBenchmark.p', testcase_conclusion_fullish_013_Cliques)).
% 4.55/4.76  fof(c22,negated_conjecture,(~iext(uri_foaf_knows,uri_ex_alice,uri_ex_bob)),inference(assume_negation,[status(cth)],[testcase_conclusion_fullish_013_Cliques])).
% 4.55/4.76  fof(c23,negated_conjecture,~iext(uri_foaf_knows,uri_ex_alice,uri_ex_bob),inference(fof_simplification,[status(thm)],[c22])).
% 4.55/4.76  cnf(c24,negated_conjecture,~iext(uri_foaf_knows,uri_ex_alice,uri_ex_bob),inference(split_conjunct,[status(thm)],[c23])).
% 4.55/4.76  % SZS output end Saturation
% 4.55/4.76  
% 4.55/4.76  % Initial clauses    : 109
% 4.55/4.76  % Processed clauses  : 705
% 4.55/4.76  % Factors computed   : 5
% 4.55/4.76  % Resolvents computed: 1659
% 4.55/4.76  % Tautologies deleted: 65
% 4.55/4.76  % Forward subsumed   : 1003
% 4.55/4.76  % Backward subsumed  : 2
% 4.55/4.76  % -------- CPU Time ---------
% 4.55/4.76  % User time          : 4.399 s
% 4.55/4.76  % System time        : 0.017 s
% 4.55/4.76  % Total time         : 4.416 s
%------------------------------------------------------------------------------