%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SWB012+4 : TPTP v8.1.2. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n019.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu May 9 17:42:48 EDT 2024
% Result : CounterSatisfiable 3.83s 4.02s
% Output : Saturation 3.83s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : SWB012+4 : TPTP v8.1.2. Released v5.2.0.
% 0.08/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n019.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Wed May 8 22:09:08 EDT 2024
% 0.13/0.35 % CPUTime :
% 3.83/4.02 % Version: 1.5
% 3.83/4.02 % SZS status CounterSatisfiable
% 3.83/4.02 % SZS output start Saturation
% 3.83/4.02 fof(rdfs_subpropertyof_main,axiom,(![P]:(![Q]:(iext(uri_rdfs_subPropertyOf,P,Q)=>((ip(P)&ip(Q))&(![X]:(![Y]:(iext(P,X,Y)=>iext(Q,X,Y)))))))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_subpropertyof_main)).
% 3.83/4.02 fof(c30,plain,(![P]:(![Q]:(~iext(uri_rdfs_subPropertyOf,P,Q)|((ip(P)&ip(Q))&(![X]:(![Y]:(~iext(P,X,Y)|iext(Q,X,Y)))))))),inference(fof_nnf,[status(thm)],[rdfs_subpropertyof_main])).
% 3.83/4.02 fof(c32,plain,(![X10]:(![X11]:(![X12]:(![X13]:(~iext(uri_rdfs_subPropertyOf,X10,X11)|((ip(X10)&ip(X11))&(~iext(X10,X12,X13)|iext(X11,X12,X13)))))))),inference(shift_quantors,[status(thm)],[fof(c31,plain,(![X10]:(![X11]:(~iext(uri_rdfs_subPropertyOf,X10,X11)|((ip(X10)&ip(X11))&(![X12]:(![X13]:(~iext(X10,X12,X13)|iext(X11,X12,X13)))))))),inference(variable_rename,[status(thm)],[c30])).])).
% 3.83/4.02 fof(c33,plain,(![X10]:(![X11]:(![X12]:(![X13]:(((~iext(uri_rdfs_subPropertyOf,X10,X11)|ip(X10))&(~iext(uri_rdfs_subPropertyOf,X10,X11)|ip(X11)))&(~iext(uri_rdfs_subPropertyOf,X10,X11)|(~iext(X10,X12,X13)|iext(X11,X12,X13)))))))),inference(distribute,[status(thm)],[c32])).
% 3.83/4.02 cnf(c36,plain,~iext(uri_rdfs_subPropertyOf,X66,X68)|~iext(X66,X69,X67)|iext(X68,X69,X67),inference(split_conjunct,[status(thm)],[c33])).
% 3.83/4.02 fof(rdfs_subpropertyof_reflex,axiom,(![P]:(ip(P)=>iext(uri_rdfs_subPropertyOf,P,P))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_subpropertyof_reflex)).
% 3.83/4.02 fof(c26,plain,(![P]:(~ip(P)|iext(uri_rdfs_subPropertyOf,P,P))),inference(fof_nnf,[status(thm)],[rdfs_subpropertyof_reflex])).
% 3.83/4.02 fof(c27,plain,(![X9]:(~ip(X9)|iext(uri_rdfs_subPropertyOf,X9,X9))),inference(variable_rename,[status(thm)],[c26])).
% 3.83/4.02 cnf(c28,plain,~ip(X55)|iext(uri_rdfs_subPropertyOf,X55,X55),inference(split_conjunct,[status(thm)],[c27])).
% 3.83/4.02 fof(rdf_type_ip,axiom,(![P]:(iext(uri_rdf_type,P,uri_rdf_Property)<=>ip(P))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdf_type_ip)).
% 3.83/4.02 fof(c138,plain,(![P]:((~iext(uri_rdf_type,P,uri_rdf_Property)|ip(P))&(~ip(P)|iext(uri_rdf_type,P,uri_rdf_Property)))),inference(fof_nnf,[status(thm)],[rdf_type_ip])).
% 3.83/4.02 fof(c139,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)],[c138])).
% 3.83/4.02 fof(c141,plain,(![X42]:(![X43]:((~iext(uri_rdf_type,X42,uri_rdf_Property)|ip(X42))&(~ip(X43)|iext(uri_rdf_type,X43,uri_rdf_Property))))),inference(shift_quantors,[status(thm)],[fof(c140,plain,((![X42]:(~iext(uri_rdf_type,X42,uri_rdf_Property)|ip(X42)))&(![X43]:(~ip(X43)|iext(uri_rdf_type,X43,uri_rdf_Property)))),inference(variable_rename,[status(thm)],[c139])).])).
% 3.83/4.02 cnf(c142,plain,~iext(uri_rdf_type,X98,uri_rdf_Property)|ip(X98),inference(split_conjunct,[status(thm)],[c141])).
% 3.83/4.02 fof(rdfs_cext_def,axiom,(![X]:(![C]:(iext(uri_rdf_type,X,C)<=>icext(C,X)))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_cext_def)).
% 3.83/4.02 fof(c121,plain,(![X]:(![C]:((~iext(uri_rdf_type,X,C)|icext(C,X))&(~icext(C,X)|iext(uri_rdf_type,X,C))))),inference(fof_nnf,[status(thm)],[rdfs_cext_def])).
% 3.83/4.02 fof(c122,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)],[c121])).
% 3.83/4.02 fof(c124,plain,(![X38]:(![X39]:(![X40]:(![X41]:((~iext(uri_rdf_type,X38,X39)|icext(X39,X38))&(~icext(X41,X40)|iext(uri_rdf_type,X40,X41))))))),inference(shift_quantors,[status(thm)],[fof(c123,plain,((![X38]:(![X39]:(~iext(uri_rdf_type,X38,X39)|icext(X39,X38))))&(![X40]:(![X41]:(~icext(X41,X40)|iext(uri_rdf_type,X40,X41))))),inference(variable_rename,[status(thm)],[c122])).])).
% 3.83/4.02 cnf(c126,plain,~icext(X94,X95)|iext(uri_rdf_type,X95,X94),inference(split_conjunct,[status(thm)],[c124])).
% 3.83/4.02 fof(rdfs_range_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_range,uri_rdf_Property),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_range_domain)).
% 3.83/4.02 cnf(c63,plain,iext(uri_rdfs_domain,uri_rdfs_range,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_range_domain])).
% 3.83/4.02 fof(rdfs_domain_main,axiom,(![P]:(![C]:(![X]:(![Y]:((iext(uri_rdfs_domain,P,C)&iext(P,X,Y))=>icext(C,X)))))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_domain_main)).
% 3.83/4.02 fof(c84,plain,(![P]:(![C]:(![X]:(![Y]:((~iext(uri_rdfs_domain,P,C)|~iext(P,X,Y))|icext(C,X)))))),inference(fof_nnf,[status(thm)],[rdfs_domain_main])).
% 3.83/4.02 fof(c85,plain,(![P]:(![C]:(![X]:((~iext(uri_rdfs_domain,P,C)|(![Y]:~iext(P,X,Y)))|icext(C,X))))),inference(shift_quantors,[status(thm)],[c84])).
% 3.83/4.02 fof(c87,plain,(![X31]:(![X32]:(![X33]:(![X34]:((~iext(uri_rdfs_domain,X31,X32)|~iext(X31,X33,X34))|icext(X32,X33)))))),inference(shift_quantors,[status(thm)],[fof(c86,plain,(![X31]:(![X32]:(![X33]:((~iext(uri_rdfs_domain,X31,X32)|(![X34]:~iext(X31,X33,X34)))|icext(X32,X33))))),inference(variable_rename,[status(thm)],[c85])).])).
% 3.83/4.02 cnf(c88,plain,~iext(uri_rdfs_domain,X88,X85)|~iext(X88,X87,X86)|icext(X85,X87),inference(split_conjunct,[status(thm)],[c87])).
% 3.83/4.02 fof(rdfs_annotation_comment_range,axiom,iext(uri_rdfs_range,uri_rdfs_comment,uri_rdfs_Literal),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_comment_range)).
% 3.83/4.02 cnf(c134,plain,iext(uri_rdfs_range,uri_rdfs_comment,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[rdfs_annotation_comment_range])).
% 3.83/4.02 cnf(c452,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X335)|icext(X335,uri_rdfs_comment),inference(resolution,[status(thm)],[c134, c88])).
% 3.83/4.02 cnf(c1418,plain,icext(uri_rdf_Property,uri_rdfs_comment),inference(resolution,[status(thm)],[c452, c63])).
% 3.83/4.02 cnf(c1419,plain,iext(uri_rdf_type,uri_rdfs_comment,uri_rdf_Property),inference(resolution,[status(thm)],[c1418, c126])).
% 3.83/4.02 cnf(c1425,plain,ip(uri_rdfs_comment),inference(resolution,[status(thm)],[c1419, c142])).
% 3.83/4.02 cnf(c1427,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_comment,uri_rdfs_comment),inference(resolution,[status(thm)],[c1425, c28])).
% 3.83/4.02 cnf(c1435,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X698)|iext(X698,uri_rdfs_comment,uri_rdfs_comment),inference(resolution,[status(thm)],[c1427, c36])).
% 3.83/4.02 cnf(c1423,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X696)|iext(X696,uri_rdfs_comment,uri_rdf_Property),inference(resolution,[status(thm)],[c1419, c36])).
% 3.83/4.02 fof(rdfs_annotation_label_range,axiom,iext(uri_rdfs_range,uri_rdfs_label,uri_rdfs_Literal),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_label_range)).
% 3.83/4.02 cnf(c129,plain,iext(uri_rdfs_range,uri_rdfs_label,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[rdfs_annotation_label_range])).
% 3.83/4.02 cnf(c388,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X318)|icext(X318,uri_rdfs_label),inference(resolution,[status(thm)],[c129, c88])).
% 3.83/4.02 cnf(c1388,plain,icext(uri_rdf_Property,uri_rdfs_label),inference(resolution,[status(thm)],[c388, c63])).
% 3.83/4.02 cnf(c1389,plain,iext(uri_rdf_type,uri_rdfs_label,uri_rdf_Property),inference(resolution,[status(thm)],[c1388, c126])).
% 3.83/4.02 cnf(c1396,plain,ip(uri_rdfs_label),inference(resolution,[status(thm)],[c1389, c142])).
% 3.83/4.02 cnf(c1397,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_label,uri_rdfs_label),inference(resolution,[status(thm)],[c1396, c28])).
% 3.83/4.02 cnf(c1406,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X695)|iext(X695,uri_rdfs_label,uri_rdfs_label),inference(resolution,[status(thm)],[c1397, c36])).
% 3.83/4.02 cnf(c1394,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X693)|iext(X693,uri_rdfs_label,uri_rdf_Property),inference(resolution,[status(thm)],[c1389, c36])).
% 3.83/4.02 fof(rdfs_collection_first_domain,axiom,iext(uri_rdfs_domain,uri_rdf_first,uri_rdf_List),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_collection_first_domain)).
% 3.83/4.02 cnf(c117,plain,iext(uri_rdfs_domain,uri_rdf_first,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdfs_collection_first_domain])).
% 3.83/4.02 fof(testcase_premise_fullish_012_Template_Class,axiom,(?[BNODE_l1]:(?[BNODE_l2]:(?[BNODE_l3]:(?[BNODE_r]:((((((((((((iext(uri_rdf_type,uri_foaf_Person,uri_owl_Class)&iext(uri_owl_intersectionOf,uri_ex_PersonAttribute,BNODE_l1))&iext(uri_rdf_first,BNODE_l1,uri_owl_DatatypeProperty))&iext(uri_rdf_rest,BNODE_l1,BNODE_l2))&iext(uri_rdf_first,BNODE_l2,uri_owl_FunctionalProperty))&iext(uri_rdf_rest,BNODE_l2,BNODE_l3))&iext(uri_rdf_first,BNODE_l3,BNODE_r))&iext(uri_rdf_rest,BNODE_l3,uri_rdf_nil))&iext(uri_rdf_type,BNODE_r,uri_owl_Restriction))&iext(uri_owl_onProperty,BNODE_r,uri_rdfs_domain))&iext(uri_owl_hasValue,BNODE_r,uri_foaf_Person))&iext(uri_rdf_type,uri_ex_name,uri_ex_PersonAttribute))&iext(uri_ex_name,uri_ex_alice,literal_plain(dat_str_alice))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', testcase_premise_fullish_012_Template_Class)).
% 3.83/4.02 fof(c0,plain,(((?[BNODE_l1]:(?[BNODE_l2]:(?[BNODE_l3]:(?[BNODE_r]:((((((((((iext(uri_rdf_type,uri_foaf_Person,uri_owl_Class)&iext(uri_owl_intersectionOf,uri_ex_PersonAttribute,BNODE_l1))&iext(uri_rdf_first,BNODE_l1,uri_owl_DatatypeProperty))&iext(uri_rdf_rest,BNODE_l1,BNODE_l2))&iext(uri_rdf_first,BNODE_l2,uri_owl_FunctionalProperty))&iext(uri_rdf_rest,BNODE_l2,BNODE_l3))&iext(uri_rdf_first,BNODE_l3,BNODE_r))&iext(uri_rdf_rest,BNODE_l3,uri_rdf_nil))&iext(uri_rdf_type,BNODE_r,uri_owl_Restriction))&iext(uri_owl_onProperty,BNODE_r,uri_rdfs_domain))&iext(uri_owl_hasValue,BNODE_r,uri_foaf_Person))))))&iext(uri_rdf_type,uri_ex_name,uri_ex_PersonAttribute))&iext(uri_ex_name,uri_ex_alice,literal_plain(dat_str_alice))),inference(shift_quantors,[status(thm)],[testcase_premise_fullish_012_Template_Class])).
% 3.83/4.02 fof(c1,plain,(((?[X2]:(?[X3]:(?[X4]:(?[X5]:((((((((((iext(uri_rdf_type,uri_foaf_Person,uri_owl_Class)&iext(uri_owl_intersectionOf,uri_ex_PersonAttribute,X2))&iext(uri_rdf_first,X2,uri_owl_DatatypeProperty))&iext(uri_rdf_rest,X2,X3))&iext(uri_rdf_first,X3,uri_owl_FunctionalProperty))&iext(uri_rdf_rest,X3,X4))&iext(uri_rdf_first,X4,X5))&iext(uri_rdf_rest,X4,uri_rdf_nil))&iext(uri_rdf_type,X5,uri_owl_Restriction))&iext(uri_owl_onProperty,X5,uri_rdfs_domain))&iext(uri_owl_hasValue,X5,uri_foaf_Person))))))&iext(uri_rdf_type,uri_ex_name,uri_ex_PersonAttribute))&iext(uri_ex_name,uri_ex_alice,literal_plain(dat_str_alice))),inference(variable_rename,[status(thm)],[c0])).
% 3.83/4.02 fof(c2,plain,((((((((((((iext(uri_rdf_type,uri_foaf_Person,uri_owl_Class)&iext(uri_owl_intersectionOf,uri_ex_PersonAttribute,skolem0001))&iext(uri_rdf_first,skolem0001,uri_owl_DatatypeProperty))&iext(uri_rdf_rest,skolem0001,skolem0002))&iext(uri_rdf_first,skolem0002,uri_owl_FunctionalProperty))&iext(uri_rdf_rest,skolem0002,skolem0003))&iext(uri_rdf_first,skolem0003,skolem0004))&iext(uri_rdf_rest,skolem0003,uri_rdf_nil))&iext(uri_rdf_type,skolem0004,uri_owl_Restriction))&iext(uri_owl_onProperty,skolem0004,uri_rdfs_domain))&iext(uri_owl_hasValue,skolem0004,uri_foaf_Person))&iext(uri_rdf_type,uri_ex_name,uri_ex_PersonAttribute))&iext(uri_ex_name,uri_ex_alice,literal_plain(dat_str_alice))),inference(skolemize,[status(esa)],[c1])).
% 3.83/4.02 cnf(c5,plain,iext(uri_rdf_first,skolem0001,uri_owl_DatatypeProperty),inference(split_conjunct,[status(thm)],[c2])).
% 3.83/4.02 cnf(c361,plain,~iext(uri_rdfs_domain,uri_rdf_first,X298)|icext(X298,skolem0001),inference(resolution,[status(thm)],[c88, c5])).
% 3.83/4.02 cnf(c1368,plain,icext(uri_rdf_List,skolem0001),inference(resolution,[status(thm)],[c361, c117])).
% 3.83/4.02 cnf(c1369,plain,iext(uri_rdf_type,skolem0001,uri_rdf_List),inference(resolution,[status(thm)],[c1368, c126])).
% 3.83/4.02 cnf(c1373,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X692)|iext(X692,skolem0001,uri_rdf_List),inference(resolution,[status(thm)],[c1369, c36])).
% 3.83/4.02 fof(rdfs_domain_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_Property),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_domain_domain)).
% 3.83/4.02 cnf(c89,plain,iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_domain_domain])).
% 3.83/4.02 fof(rdfs_reification_predicate_domain,axiom,iext(uri_rdfs_domain,uri_rdf_predicate,uri_rdfs_Statement),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_reification_predicate_domain)).
% 3.83/4.02 cnf(c56,plain,iext(uri_rdfs_domain,uri_rdf_predicate,uri_rdfs_Statement),inference(split_conjunct,[status(thm)],[rdfs_reification_predicate_domain])).
% 3.83/4.02 cnf(c331,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X268)|icext(X268,uri_rdf_predicate),inference(resolution,[status(thm)],[c88, c56])).
% 3.83/4.02 cnf(c1329,plain,icext(uri_rdf_Property,uri_rdf_predicate),inference(resolution,[status(thm)],[c331, c89])).
% 3.83/4.02 cnf(c1330,plain,iext(uri_rdf_type,uri_rdf_predicate,uri_rdf_Property),inference(resolution,[status(thm)],[c1329, c126])).
% 3.83/4.02 cnf(c1336,plain,ip(uri_rdf_predicate),inference(resolution,[status(thm)],[c1330, c142])).
% 3.83/4.02 cnf(c1337,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_predicate,uri_rdf_predicate),inference(resolution,[status(thm)],[c1336, c28])).
% 3.83/4.02 cnf(c1345,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X691)|iext(X691,uri_rdf_predicate,uri_rdf_predicate),inference(resolution,[status(thm)],[c1337, c36])).
% 3.83/4.02 cnf(c1334,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X689)|iext(X689,uri_rdf_predicate,uri_rdf_Property),inference(resolution,[status(thm)],[c1330, c36])).
% 3.83/4.02 fof(rdfs_collection_rest_range,axiom,iext(uri_rdfs_range,uri_rdf_rest,uri_rdf_List),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_collection_rest_range)).
% 3.83/4.02 cnf(c114,plain,iext(uri_rdfs_range,uri_rdf_rest,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdfs_collection_rest_range])).
% 3.83/4.02 cnf(c8,plain,iext(uri_rdf_rest,skolem0002,skolem0003),inference(split_conjunct,[status(thm)],[c2])).
% 3.83/4.02 fof(rdfs_range_main,axiom,(![P]:(![C]:(![X]:(![Y]:((iext(uri_rdfs_range,P,C)&iext(P,X,Y))=>icext(C,Y)))))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_range_main)).
% 3.83/4.02 fof(c60,plain,(![P]:(![C]:(![X]:(![Y]:((~iext(uri_rdfs_range,P,C)|~iext(P,X,Y))|icext(C,Y)))))),inference(fof_nnf,[status(thm)],[rdfs_range_main])).
% 3.83/4.02 fof(c61,plain,(![X21]:(![X22]:(![X23]:(![X24]:((~iext(uri_rdfs_range,X21,X22)|~iext(X21,X23,X24))|icext(X22,X24)))))),inference(variable_rename,[status(thm)],[c60])).
% 3.83/4.02 cnf(c62,plain,~iext(uri_rdfs_range,X84,X82)|~iext(X84,X81,X83)|icext(X82,X83),inference(split_conjunct,[status(thm)],[c61])).
% 3.83/4.02 cnf(c319,plain,~iext(uri_rdfs_range,uri_rdf_rest,X256)|icext(X256,skolem0003),inference(resolution,[status(thm)],[c62, c8])).
% 3.83/4.02 cnf(c1289,plain,icext(uri_rdf_List,skolem0003),inference(resolution,[status(thm)],[c319, c114])).
% 3.83/4.02 cnf(c1295,plain,iext(uri_rdf_type,skolem0003,uri_rdf_List),inference(resolution,[status(thm)],[c1289, c126])).
% 3.83/4.02 cnf(c1323,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X688)|iext(X688,skolem0003,uri_rdf_List),inference(resolution,[status(thm)],[c1295, c36])).
% 3.83/4.02 fof(rdfs_subclassof_reflex,axiom,(![C]:(ic(C)=>iext(uri_rdfs_subClassOf,C,C))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_subclassof_reflex)).
% 3.83/4.02 fof(c41,plain,(![C]:(~ic(C)|iext(uri_rdfs_subClassOf,C,C))),inference(fof_nnf,[status(thm)],[rdfs_subclassof_reflex])).
% 3.83/4.02 fof(c42,plain,(![X17]:(~ic(X17)|iext(uri_rdfs_subClassOf,X17,X17))),inference(variable_rename,[status(thm)],[c41])).
% 3.83/4.02 cnf(c43,plain,~ic(X73)|iext(uri_rdfs_subClassOf,X73,X73),inference(split_conjunct,[status(thm)],[c42])).
% 3.83/4.02 fof(rdfs_ic_def,axiom,(![X]:(ic(X)<=>icext(uri_rdfs_Class,X))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_ic_def)).
% 3.83/4.02 fof(c77,plain,(![X]:((~ic(X)|icext(uri_rdfs_Class,X))&(~icext(uri_rdfs_Class,X)|ic(X)))),inference(fof_nnf,[status(thm)],[rdfs_ic_def])).
% 3.83/4.02 fof(c78,plain,((![X]:(~ic(X)|icext(uri_rdfs_Class,X)))&(![X]:(~icext(uri_rdfs_Class,X)|ic(X)))),inference(shift_quantors,[status(thm)],[c77])).
% 3.83/4.02 fof(c80,plain,(![X29]:(![X30]:((~ic(X29)|icext(uri_rdfs_Class,X29))&(~icext(uri_rdfs_Class,X30)|ic(X30))))),inference(shift_quantors,[status(thm)],[fof(c79,plain,((![X29]:(~ic(X29)|icext(uri_rdfs_Class,X29)))&(![X30]:(~icext(uri_rdfs_Class,X30)|ic(X30)))),inference(variable_rename,[status(thm)],[c78])).])).
% 3.83/4.02 cnf(c82,plain,~icext(uri_rdfs_Class,X63)|ic(X63),inference(split_conjunct,[status(thm)],[c80])).
% 3.83/4.02 fof(rdfs_type_range,axiom,iext(uri_rdfs_range,uri_rdf_type,uri_rdfs_Class),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_type_range)).
% 3.83/4.02 cnf(c21,plain,iext(uri_rdfs_range,uri_rdf_type,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_type_range])).
% 3.83/4.02 cnf(c3,plain,iext(uri_rdf_type,uri_foaf_Person,uri_owl_Class),inference(split_conjunct,[status(thm)],[c2])).
% 3.83/4.02 cnf(c318,plain,~iext(uri_rdfs_range,uri_rdf_type,X255)|icext(X255,uri_owl_Class),inference(resolution,[status(thm)],[c62, c3])).
% 3.83/4.02 cnf(c1288,plain,icext(uri_rdfs_Class,uri_owl_Class),inference(resolution,[status(thm)],[c318, c21])).
% 3.83/4.02 cnf(c1291,plain,ic(uri_owl_Class),inference(resolution,[status(thm)],[c1288, c82])).
% 3.83/4.02 cnf(c1294,plain,iext(uri_rdfs_subClassOf,uri_owl_Class,uri_owl_Class),inference(resolution,[status(thm)],[c1291, c43])).
% 3.83/4.02 cnf(c1317,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X687)|iext(X687,uri_owl_Class,uri_owl_Class),inference(resolution,[status(thm)],[c1294, c36])).
% 3.83/4.02 fof(rdfs_class_instsub_resource,axiom,(![C]:(ic(C)=>iext(uri_rdfs_subClassOf,C,uri_rdfs_Resource))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_class_instsub_resource)).
% 3.83/4.02 fof(c118,plain,(![C]:(~ic(C)|iext(uri_rdfs_subClassOf,C,uri_rdfs_Resource))),inference(fof_nnf,[status(thm)],[rdfs_class_instsub_resource])).
% 3.83/4.02 fof(c119,plain,(![X37]:(~ic(X37)|iext(uri_rdfs_subClassOf,X37,uri_rdfs_Resource))),inference(variable_rename,[status(thm)],[c118])).
% 3.83/4.02 cnf(c120,plain,~ic(X91)|iext(uri_rdfs_subClassOf,X91,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[c119])).
% 3.83/4.02 cnf(c1292,plain,iext(uri_rdfs_subClassOf,uri_owl_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1291, c120])).
% 3.83/4.02 cnf(c1308,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X685)|iext(X685,uri_owl_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1292, c36])).
% 3.83/4.02 fof(rdfs_subclassof_trans,axiom,(![C]:(![D]:(![E]:((iext(uri_rdfs_subClassOf,C,D)&iext(uri_rdfs_subClassOf,D,E))=>iext(uri_rdfs_subClassOf,C,E))))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_subclassof_trans)).
% 3.83/4.02 fof(c38,plain,(![C]:(![D]:(![E]:((~iext(uri_rdfs_subClassOf,C,D)|~iext(uri_rdfs_subClassOf,D,E))|iext(uri_rdfs_subClassOf,C,E))))),inference(fof_nnf,[status(thm)],[rdfs_subclassof_trans])).
% 3.83/4.02 fof(c39,plain,(![X14]:(![X15]:(![X16]:((~iext(uri_rdfs_subClassOf,X14,X15)|~iext(uri_rdfs_subClassOf,X15,X16))|iext(uri_rdfs_subClassOf,X14,X16))))),inference(variable_rename,[status(thm)],[c38])).
% 3.83/4.02 cnf(c40,plain,~iext(uri_rdfs_subClassOf,X70,X71)|~iext(uri_rdfs_subClassOf,X71,X72)|iext(uri_rdfs_subClassOf,X70,X72),inference(split_conjunct,[status(thm)],[c39])).
% 3.83/4.02 cnf(c1302,plain,~iext(uri_rdfs_subClassOf,X684,uri_owl_Class)|iext(uri_rdfs_subClassOf,X684,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1292, c40])).
% 3.83/4.02 cnf(c1290,plain,iext(uri_rdf_type,uri_owl_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c1288, c126])).
% 3.83/4.02 cnf(c1299,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X683)|iext(X683,uri_owl_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c1290, c36])).
% 3.83/4.02 cnf(c6,plain,iext(uri_rdf_rest,skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c2])).
% 3.83/4.02 cnf(c317,plain,~iext(uri_rdfs_range,uri_rdf_rest,X254)|icext(X254,skolem0002),inference(resolution,[status(thm)],[c62, c6])).
% 3.83/4.02 cnf(c1281,plain,icext(uri_rdf_List,skolem0002),inference(resolution,[status(thm)],[c317, c114])).
% 3.83/4.02 cnf(c1282,plain,iext(uri_rdf_type,skolem0002,uri_rdf_List),inference(resolution,[status(thm)],[c1281, c126])).
% 3.83/4.02 cnf(c1286,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X682)|iext(X682,skolem0002,uri_rdf_List),inference(resolution,[status(thm)],[c1282, c36])).
% 3.83/4.02 cnf(c14,plain,iext(uri_rdf_type,uri_ex_name,uri_ex_PersonAttribute),inference(split_conjunct,[status(thm)],[c2])).
% 3.83/4.02 cnf(c281,plain,~iext(uri_rdfs_range,uri_rdf_type,X186)|icext(X186,uri_ex_PersonAttribute),inference(resolution,[status(thm)],[c62, c14])).
% 3.83/4.02 cnf(c1175,plain,icext(uri_rdfs_Class,uri_ex_PersonAttribute),inference(resolution,[status(thm)],[c281, c21])).
% 3.83/4.02 cnf(c1177,plain,ic(uri_ex_PersonAttribute),inference(resolution,[status(thm)],[c1175, c82])).
% 3.83/4.02 cnf(c1180,plain,iext(uri_rdfs_subClassOf,uri_ex_PersonAttribute,uri_ex_PersonAttribute),inference(resolution,[status(thm)],[c1177, c43])).
% 3.83/4.02 cnf(c1270,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X681)|iext(X681,uri_ex_PersonAttribute,uri_ex_PersonAttribute),inference(resolution,[status(thm)],[c1180, c36])).
% 3.83/4.02 cnf(c1178,plain,iext(uri_rdfs_subClassOf,uri_ex_PersonAttribute,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1177, c120])).
% 3.83/4.02 cnf(c1262,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X679)|iext(X679,uri_ex_PersonAttribute,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1178, c36])).
% 3.83/4.02 cnf(c1256,plain,~iext(uri_rdfs_subClassOf,X678,uri_ex_PersonAttribute)|iext(uri_rdfs_subClassOf,X678,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1178, c40])).
% 3.83/4.02 cnf(c1176,plain,iext(uri_rdf_type,uri_ex_PersonAttribute,uri_rdfs_Class),inference(resolution,[status(thm)],[c1175, c126])).
% 3.83/4.02 cnf(c1254,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X677)|iext(X677,uri_ex_PersonAttribute,uri_rdfs_Class),inference(resolution,[status(thm)],[c1176, c36])).
% 3.83/4.02 cnf(c11,plain,iext(uri_rdf_type,skolem0004,uri_owl_Restriction),inference(split_conjunct,[status(thm)],[c2])).
% 3.83/4.02 cnf(c270,plain,~iext(uri_rdfs_range,uri_rdf_type,X175)|icext(X175,uri_owl_Restriction),inference(resolution,[status(thm)],[c62, c11])).
% 3.83/4.02 cnf(c1160,plain,icext(uri_rdfs_Class,uri_owl_Restriction),inference(resolution,[status(thm)],[c270, c21])).
% 3.83/4.02 cnf(c1162,plain,ic(uri_owl_Restriction),inference(resolution,[status(thm)],[c1160, c82])).
% 3.83/4.02 cnf(c1165,plain,iext(uri_rdfs_subClassOf,uri_owl_Restriction,uri_owl_Restriction),inference(resolution,[status(thm)],[c1162, c43])).
% 3.83/4.02 cnf(c1248,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X676)|iext(X676,uri_owl_Restriction,uri_owl_Restriction),inference(resolution,[status(thm)],[c1165, c36])).
% 3.83/4.02 cnf(c1163,plain,iext(uri_rdfs_subClassOf,uri_owl_Restriction,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1162, c120])).
% 3.83/4.02 cnf(c1239,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X674)|iext(X674,uri_owl_Restriction,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1163, c36])).
% 3.83/4.02 cnf(c1233,plain,~iext(uri_rdfs_subClassOf,X673,uri_owl_Restriction)|iext(uri_rdfs_subClassOf,X673,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1163, c40])).
% 3.83/4.02 cnf(c1161,plain,iext(uri_rdf_type,uri_owl_Restriction,uri_rdfs_Class),inference(resolution,[status(thm)],[c1160, c126])).
% 3.83/4.02 cnf(c1231,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X672)|iext(X672,uri_owl_Restriction,uri_rdfs_Class),inference(resolution,[status(thm)],[c1161, c36])).
% 3.83/4.02 fof(rdfs_domain_range,axiom,iext(uri_rdfs_range,uri_rdfs_domain,uri_rdfs_Class),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_domain_range)).
% 3.83/4.02 cnf(c83,plain,iext(uri_rdfs_range,uri_rdfs_domain,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_domain_range])).
% 3.83/4.02 fof(rdfs_reification_subject_domain,axiom,iext(uri_rdfs_domain,uri_rdf_subject,uri_rdfs_Statement),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_reification_subject_domain)).
% 3.83/4.02 cnf(c54,plain,iext(uri_rdfs_domain,uri_rdf_subject,uri_rdfs_Statement),inference(split_conjunct,[status(thm)],[rdfs_reification_subject_domain])).
% 3.83/4.02 cnf(c269,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X174)|icext(X174,uri_rdfs_Statement),inference(resolution,[status(thm)],[c62, c54])).
% 3.83/4.02 cnf(c1147,plain,icext(uri_rdfs_Class,uri_rdfs_Statement),inference(resolution,[status(thm)],[c269, c83])).
% 3.83/4.02 cnf(c1149,plain,ic(uri_rdfs_Statement),inference(resolution,[status(thm)],[c1147, c82])).
% 3.83/4.02 cnf(c1152,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Statement,uri_rdfs_Statement),inference(resolution,[status(thm)],[c1149, c43])).
% 3.83/4.02 cnf(c1226,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X671)|iext(X671,uri_rdfs_Statement,uri_rdfs_Statement),inference(resolution,[status(thm)],[c1152, c36])).
% 3.83/4.02 cnf(c1150,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Statement,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1149, c120])).
% 3.83/4.02 cnf(c1218,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X669)|iext(X669,uri_rdfs_Statement,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1150, c36])).
% 3.83/4.02 cnf(c1212,plain,~iext(uri_rdfs_subClassOf,X668,uri_rdfs_Statement)|iext(uri_rdfs_subClassOf,X668,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1150, c40])).
% 3.83/4.02 cnf(c1148,plain,iext(uri_rdf_type,uri_rdfs_Statement,uri_rdfs_Class),inference(resolution,[status(thm)],[c1147, c126])).
% 3.83/4.02 cnf(c1210,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X667)|iext(X667,uri_rdfs_Statement,uri_rdfs_Class),inference(resolution,[status(thm)],[c1148, c36])).
% 3.83/4.02 cnf(c268,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X173)|icext(X173,uri_rdf_List),inference(resolution,[status(thm)],[c62, c117])).
% 3.83/4.02 cnf(c1141,plain,icext(uri_rdfs_Class,uri_rdf_List),inference(resolution,[status(thm)],[c268, c83])).
% 3.83/4.02 cnf(c1143,plain,ic(uri_rdf_List),inference(resolution,[status(thm)],[c1141, c82])).
% 3.83/4.02 cnf(c1146,plain,iext(uri_rdfs_subClassOf,uri_rdf_List,uri_rdf_List),inference(resolution,[status(thm)],[c1143, c43])).
% 3.83/4.02 cnf(c1205,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X666)|iext(X666,uri_rdf_List,uri_rdf_List),inference(resolution,[status(thm)],[c1146, c36])).
% 3.83/4.02 cnf(c1144,plain,iext(uri_rdfs_subClassOf,uri_rdf_List,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1143, c120])).
% 3.83/4.02 cnf(c1197,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X664)|iext(X664,uri_rdf_List,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1144, c36])).
% 3.83/4.02 cnf(c1191,plain,~iext(uri_rdfs_subClassOf,X663,uri_rdf_List)|iext(uri_rdfs_subClassOf,X663,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1144, c40])).
% 3.83/4.02 cnf(c1142,plain,iext(uri_rdf_type,uri_rdf_List,uri_rdfs_Class),inference(resolution,[status(thm)],[c1141, c126])).
% 3.83/4.02 cnf(c1188,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X662)|iext(X662,uri_rdf_List,uri_rdfs_Class),inference(resolution,[status(thm)],[c1142, c36])).
% 3.83/4.02 cnf(c143,plain,~ip(X99)|iext(uri_rdf_type,X99,uri_rdf_Property),inference(split_conjunct,[status(thm)],[c141])).
% 3.83/4.02 cnf(c35,plain,~iext(uri_rdfs_subPropertyOf,X64,X65)|ip(X65),inference(split_conjunct,[status(thm)],[c33])).
% 3.83/4.02 fof(rdfs_container_containermembershipproperty_instsub_member,axiom,(![P]:(icext(uri_rdfs_ContainerMembershipProperty,P)=>iext(uri_rdfs_subPropertyOf,P,uri_rdfs_member))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_containermembershipproperty_instsub_member)).
% 3.83/4.02 fof(c109,plain,(![P]:(~icext(uri_rdfs_ContainerMembershipProperty,P)|iext(uri_rdfs_subPropertyOf,P,uri_rdfs_member))),inference(fof_nnf,[status(thm)],[rdfs_container_containermembershipproperty_instsub_member])).
% 3.83/4.02 fof(c110,plain,(![X36]:(~icext(uri_rdfs_ContainerMembershipProperty,X36)|iext(uri_rdfs_subPropertyOf,X36,uri_rdfs_member))),inference(variable_rename,[status(thm)],[c109])).
% 3.83/4.02 cnf(c111,plain,~icext(uri_rdfs_ContainerMembershipProperty,X90)|iext(uri_rdfs_subPropertyOf,X90,uri_rdfs_member),inference(split_conjunct,[status(thm)],[c110])).
% 3.83/4.02 fof(rdfs_container_n_type_003,axiom,iext(uri_rdf_type,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_type_003)).
% 3.83/4.02 cnf(c97,plain,iext(uri_rdf_type,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),inference(split_conjunct,[status(thm)],[rdfs_container_n_type_003])).
% 3.83/4.02 cnf(c125,plain,~iext(uri_rdf_type,X93,X92)|icext(X92,X93),inference(split_conjunct,[status(thm)],[c124])).
% 3.83/4.02 cnf(c419,plain,icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__3),inference(resolution,[status(thm)],[c125, c97])).
% 3.83/4.02 cnf(c424,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__3,uri_rdfs_member),inference(resolution,[status(thm)],[c419, c111])).
% 3.83/4.02 cnf(c810,plain,ip(uri_rdfs_member),inference(resolution,[status(thm)],[c424, c35])).
% 3.83/4.02 cnf(c813,plain,iext(uri_rdf_type,uri_rdfs_member,uri_rdf_Property),inference(resolution,[status(thm)],[c810, c143])).
% 3.83/4.02 cnf(c1167,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X661)|iext(X661,uri_rdfs_member,uri_rdf_Property),inference(resolution,[status(thm)],[c813, c36])).
% 3.83/4.02 cnf(c812,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_member,uri_rdfs_member),inference(resolution,[status(thm)],[c810, c28])).
% 3.83/4.02 cnf(c1153,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X659)|iext(X659,uri_rdfs_member,uri_rdfs_member),inference(resolution,[status(thm)],[c812, c36])).
% 3.83/4.02 cnf(c81,plain,~ic(X60)|icext(uri_rdfs_Class,X60),inference(split_conjunct,[status(thm)],[c80])).
% 3.83/4.02 fof(rdfs_subclassof_main,axiom,(![C]:(![D]:(iext(uri_rdfs_subClassOf,C,D)=>((ic(C)&ic(D))&(![X]:(icext(C,X)=>icext(D,X))))))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_subclassof_main)).
% 3.83/4.02 fof(c45,plain,(![C]:(![D]:(~iext(uri_rdfs_subClassOf,C,D)|((ic(C)&ic(D))&(![X]:(~icext(C,X)|icext(D,X))))))),inference(fof_nnf,[status(thm)],[rdfs_subclassof_main])).
% 3.83/4.02 fof(c47,plain,(![X18]:(![X19]:(![X20]:(~iext(uri_rdfs_subClassOf,X18,X19)|((ic(X18)&ic(X19))&(~icext(X18,X20)|icext(X19,X20))))))),inference(shift_quantors,[status(thm)],[fof(c46,plain,(![X18]:(![X19]:(~iext(uri_rdfs_subClassOf,X18,X19)|((ic(X18)&ic(X19))&(![X20]:(~icext(X18,X20)|icext(X19,X20))))))),inference(variable_rename,[status(thm)],[c45])).])).
% 3.83/4.02 fof(c48,plain,(![X18]:(![X19]:(![X20]:(((~iext(uri_rdfs_subClassOf,X18,X19)|ic(X18))&(~iext(uri_rdfs_subClassOf,X18,X19)|ic(X19)))&(~iext(uri_rdfs_subClassOf,X18,X19)|(~icext(X18,X20)|icext(X19,X20))))))),inference(distribute,[status(thm)],[c47])).
% 3.83/4.02 cnf(c50,plain,~iext(uri_rdfs_subClassOf,X76,X77)|ic(X77),inference(split_conjunct,[status(thm)],[c48])).
% 3.83/4.02 fof(rdfs_container_containermembershipproperty_sub,axiom,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_containermembershipproperty_sub)).
% 3.83/4.02 cnf(c108,plain,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_container_containermembershipproperty_sub])).
% 3.83/4.02 cnf(c242,plain,ic(uri_rdf_Property),inference(resolution,[status(thm)],[c50, c108])).
% 3.83/4.02 cnf(c391,plain,iext(uri_rdfs_subClassOf,uri_rdf_Property,uri_rdfs_Resource),inference(resolution,[status(thm)],[c120, c242])).
% 3.83/4.02 cnf(c710,plain,ic(uri_rdfs_Resource),inference(resolution,[status(thm)],[c391, c50])).
% 3.83/4.02 cnf(c715,plain,icext(uri_rdfs_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c710, c81])).
% 3.83/4.02 cnf(c717,plain,iext(uri_rdf_type,uri_rdfs_Resource,uri_rdfs_Class),inference(resolution,[status(thm)],[c715, c126])).
% 3.83/4.02 cnf(c1136,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X658)|iext(X658,uri_rdfs_Resource,uri_rdfs_Class),inference(resolution,[status(thm)],[c717, c36])).
% 3.83/4.02 cnf(c714,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Resource,uri_rdfs_Resource),inference(resolution,[status(thm)],[c710, c120])).
% 3.83/4.02 cnf(c1127,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X656)|iext(X656,uri_rdfs_Resource,uri_rdfs_Resource),inference(resolution,[status(thm)],[c714, c36])).
% 3.83/4.02 cnf(c4,plain,iext(uri_owl_intersectionOf,uri_ex_PersonAttribute,skolem0001),inference(split_conjunct,[status(thm)],[c2])).
% 3.83/4.02 fof(simple_iext_property,axiom,(![S]:(![P]:(![O]:(iext(P,S,O)=>ip(P))))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', simple_iext_property)).
% 3.83/4.02 fof(c158,plain,(![S]:(![P]:(![O]:(~iext(P,S,O)|ip(P))))),inference(fof_nnf,[status(thm)],[simple_iext_property])).
% 3.83/4.02 fof(c159,plain,(![S]:(![P]:((![O]:~iext(P,S,O))|ip(P)))),inference(shift_quantors,[status(thm)],[c158])).
% 3.83/4.02 fof(c161,plain,(![X46]:(![X47]:(![X48]:(~iext(X47,X46,X48)|ip(X47))))),inference(shift_quantors,[status(thm)],[fof(c160,plain,(![X46]:(![X47]:((![X48]:~iext(X47,X46,X48))|ip(X47)))),inference(variable_rename,[status(thm)],[c159])).])).
% 3.83/4.02 cnf(c162,plain,~iext(X100,X101,X102)|ip(X100),inference(split_conjunct,[status(thm)],[c161])).
% 3.83/4.02 cnf(c593,plain,ip(uri_owl_intersectionOf),inference(resolution,[status(thm)],[c162, c4])).
% 3.83/4.02 cnf(c625,plain,iext(uri_rdf_type,uri_owl_intersectionOf,uri_rdf_Property),inference(resolution,[status(thm)],[c593, c143])).
% 3.83/4.02 cnf(c1119,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X655)|iext(X655,uri_owl_intersectionOf,uri_rdf_Property),inference(resolution,[status(thm)],[c625, c36])).
% 3.83/4.02 cnf(c624,plain,iext(uri_rdfs_subPropertyOf,uri_owl_intersectionOf,uri_owl_intersectionOf),inference(resolution,[status(thm)],[c593, c28])).
% 3.83/4.02 cnf(c1111,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X653)|iext(X653,uri_owl_intersectionOf,uri_owl_intersectionOf),inference(resolution,[status(thm)],[c624, c36])).
% 3.83/4.02 cnf(c15,plain,iext(uri_ex_name,uri_ex_alice,literal_plain(dat_str_alice)),inference(split_conjunct,[status(thm)],[c2])).
% 3.83/4.02 cnf(c573,plain,ip(uri_ex_name),inference(resolution,[status(thm)],[c162, c15])).
% 3.83/4.02 cnf(c623,plain,iext(uri_rdf_type,uri_ex_name,uri_rdf_Property),inference(resolution,[status(thm)],[c573, c143])).
% 3.83/4.02 cnf(c1104,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X652)|iext(X652,uri_ex_name,uri_rdf_Property),inference(resolution,[status(thm)],[c623, c36])).
% 3.83/4.02 cnf(c622,plain,iext(uri_rdfs_subPropertyOf,uri_ex_name,uri_ex_name),inference(resolution,[status(thm)],[c573, c28])).
% 3.83/4.02 cnf(c1096,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X650)|iext(X650,uri_ex_name,uri_ex_name),inference(resolution,[status(thm)],[c622, c36])).
% 3.83/4.02 cnf(c570,plain,ip(uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c162, c108])).
% 3.83/4.02 cnf(c621,plain,iext(uri_rdf_type,uri_rdfs_subClassOf,uri_rdf_Property),inference(resolution,[status(thm)],[c570, c143])).
% 3.83/4.02 cnf(c1089,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X649)|iext(X649,uri_rdfs_subClassOf,uri_rdf_Property),inference(resolution,[status(thm)],[c621, c36])).
% 3.83/4.02 cnf(c620,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c570, c28])).
% 3.83/4.02 cnf(c1076,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X647)|iext(X647,uri_rdfs_subClassOf,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c620, c36])).
% 3.83/4.02 fof(rdfs_annotation_isdefinedby_sub,axiom,iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_isdefinedby_sub)).
% 3.83/4.02 cnf(c131,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_sub])).
% 3.83/4.02 cnf(c564,plain,ip(uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c162, c131])).
% 3.83/4.02 cnf(c619,plain,iext(uri_rdf_type,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c564, c143])).
% 3.83/4.02 cnf(c1068,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X646)|iext(X646,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c619, c36])).
% 3.83/4.02 cnf(c618,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c564, c28])).
% 3.83/4.02 cnf(c1057,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X644)|iext(X644,uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c618, c36])).
% 3.83/4.02 cnf(c13,plain,iext(uri_owl_hasValue,skolem0004,uri_foaf_Person),inference(split_conjunct,[status(thm)],[c2])).
% 3.83/4.02 cnf(c550,plain,ip(uri_owl_hasValue),inference(resolution,[status(thm)],[c162, c13])).
% 3.83/4.02 cnf(c617,plain,iext(uri_rdf_type,uri_owl_hasValue,uri_rdf_Property),inference(resolution,[status(thm)],[c550, c143])).
% 3.83/4.02 cnf(c1049,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X643)|iext(X643,uri_owl_hasValue,uri_rdf_Property),inference(resolution,[status(thm)],[c617, c36])).
% 3.83/4.02 cnf(c616,plain,iext(uri_rdfs_subPropertyOf,uri_owl_hasValue,uri_owl_hasValue),inference(resolution,[status(thm)],[c550, c28])).
% 3.83/4.02 cnf(c1041,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X641)|iext(X641,uri_owl_hasValue,uri_owl_hasValue),inference(resolution,[status(thm)],[c616, c36])).
% 3.83/4.02 cnf(c12,plain,iext(uri_owl_onProperty,skolem0004,uri_rdfs_domain),inference(split_conjunct,[status(thm)],[c2])).
% 3.83/4.02 cnf(c547,plain,ip(uri_owl_onProperty),inference(resolution,[status(thm)],[c162, c12])).
% 3.83/4.02 cnf(c615,plain,iext(uri_rdf_type,uri_owl_onProperty,uri_rdf_Property),inference(resolution,[status(thm)],[c547, c143])).
% 3.83/4.02 cnf(c1032,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X640)|iext(X640,uri_owl_onProperty,uri_rdf_Property),inference(resolution,[status(thm)],[c615, c36])).
% 3.83/4.02 cnf(c614,plain,iext(uri_rdfs_subPropertyOf,uri_owl_onProperty,uri_owl_onProperty),inference(resolution,[status(thm)],[c547, c28])).
% 3.83/4.02 cnf(c1024,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X638)|iext(X638,uri_owl_onProperty,uri_owl_onProperty),inference(resolution,[status(thm)],[c614, c36])).
% 3.83/4.02 fof(rdfs_annotation_seealso_range,axiom,iext(uri_rdfs_range,uri_rdfs_seeAlso,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_seealso_range)).
% 3.83/4.02 cnf(c127,plain,iext(uri_rdfs_range,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_seealso_range])).
% 3.83/4.02 cnf(c543,plain,ip(uri_rdfs_range),inference(resolution,[status(thm)],[c162, c127])).
% 3.83/4.02 cnf(c613,plain,iext(uri_rdf_type,uri_rdfs_range,uri_rdf_Property),inference(resolution,[status(thm)],[c543, c143])).
% 3.83/4.02 cnf(c1016,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X637)|iext(X637,uri_rdfs_range,uri_rdf_Property),inference(resolution,[status(thm)],[c613, c36])).
% 3.83/4.02 cnf(c612,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_range,uri_rdfs_range),inference(resolution,[status(thm)],[c543, c28])).
% 3.83/4.02 cnf(c997,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X635)|iext(X635,uri_rdfs_range,uri_rdfs_range),inference(resolution,[status(thm)],[c612, c36])).
% 3.83/4.02 fof(rdfs_container_n_domain_003,axiom,iext(uri_rdfs_domain,uri_rdf__3,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_domain_003)).
% 3.83/4.02 cnf(c103,plain,iext(uri_rdfs_domain,uri_rdf__3,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_003])).
% 3.83/4.02 cnf(c537,plain,ip(uri_rdfs_domain),inference(resolution,[status(thm)],[c162, c103])).
% 3.83/4.02 cnf(c611,plain,iext(uri_rdf_type,uri_rdfs_domain,uri_rdf_Property),inference(resolution,[status(thm)],[c537, c143])).
% 3.83/4.02 cnf(c989,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X634)|iext(X634,uri_rdfs_domain,uri_rdf_Property),inference(resolution,[status(thm)],[c611, c36])).
% 3.83/4.02 cnf(c610,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,uri_rdfs_domain),inference(resolution,[status(thm)],[c537, c28])).
% 3.83/4.02 cnf(c971,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X632)|iext(X632,uri_rdfs_domain,uri_rdfs_domain),inference(resolution,[status(thm)],[c610, c36])).
% 3.83/4.02 fof(rdf_collection_first_type,axiom,iext(uri_rdf_type,uri_rdf_first,uri_rdf_Property),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdf_collection_first_type)).
% 3.83/4.02 cnf(c152,plain,iext(uri_rdf_type,uri_rdf_first,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_collection_first_type])).
% 3.83/4.02 cnf(c530,plain,ip(uri_rdf_first),inference(resolution,[status(thm)],[c152, c142])).
% 3.83/4.02 cnf(c534,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_first,uri_rdf_first),inference(resolution,[status(thm)],[c530, c28])).
% 3.83/4.02 cnf(c958,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X630)|iext(X630,uri_rdf_first,uri_rdf_first),inference(resolution,[status(thm)],[c534, c36])).
% 3.83/4.02 fof(rdf_collection_rest_type,axiom,iext(uri_rdf_type,uri_rdf_rest,uri_rdf_Property),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdf_collection_rest_type)).
% 3.83/4.02 cnf(c150,plain,iext(uri_rdf_type,uri_rdf_rest,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_collection_rest_type])).
% 3.83/4.02 cnf(c517,plain,ip(uri_rdf_rest),inference(resolution,[status(thm)],[c150, c142])).
% 3.83/4.02 cnf(c521,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_rest,uri_rdf_rest),inference(resolution,[status(thm)],[c517, c28])).
% 3.83/4.02 cnf(c948,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X628)|iext(X628,uri_rdf_rest,uri_rdf_rest),inference(resolution,[status(thm)],[c521, c36])).
% 3.83/4.02 fof(rdf_container_n_type_001,axiom,iext(uri_rdf_type,uri_rdf__1,uri_rdf_Property),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdf_container_n_type_001)).
% 3.83/4.02 cnf(c149,plain,iext(uri_rdf_type,uri_rdf__1,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_container_n_type_001])).
% 3.83/4.02 cnf(c509,plain,ip(uri_rdf__1),inference(resolution,[status(thm)],[c149, c142])).
% 3.83/4.02 cnf(c513,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__1,uri_rdf__1),inference(resolution,[status(thm)],[c509, c28])).
% 3.83/4.02 cnf(c940,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X626)|iext(X626,uri_rdf__1,uri_rdf__1),inference(resolution,[status(thm)],[c513, c36])).
% 3.83/4.02 fof(rdf_container_n_type_002,axiom,iext(uri_rdf_type,uri_rdf__2,uri_rdf_Property),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdf_container_n_type_002)).
% 3.83/4.02 cnf(c148,plain,iext(uri_rdf_type,uri_rdf__2,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_container_n_type_002])).
% 3.83/4.02 cnf(c501,plain,ip(uri_rdf__2),inference(resolution,[status(thm)],[c148, c142])).
% 3.83/4.02 cnf(c505,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__2,uri_rdf__2),inference(resolution,[status(thm)],[c501, c28])).
% 3.83/4.02 cnf(c933,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X624)|iext(X624,uri_rdf__2,uri_rdf__2),inference(resolution,[status(thm)],[c505, c36])).
% 3.83/4.02 fof(rdf_container_n_type_003,axiom,iext(uri_rdf_type,uri_rdf__3,uri_rdf_Property),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdf_container_n_type_003)).
% 3.83/4.02 cnf(c147,plain,iext(uri_rdf_type,uri_rdf__3,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_container_n_type_003])).
% 3.83/4.02 cnf(c493,plain,ip(uri_rdf__3),inference(resolution,[status(thm)],[c147, c142])).
% 3.83/4.03 cnf(c497,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__3,uri_rdf__3),inference(resolution,[status(thm)],[c493, c28])).
% 3.83/4.03 cnf(c926,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X622)|iext(X622,uri_rdf__3,uri_rdf__3),inference(resolution,[status(thm)],[c497, c36])).
% 3.83/4.03 fof(rdf_reification_object_type,axiom,iext(uri_rdf_type,uri_rdf_object,uri_rdf_Property),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdf_reification_object_type)).
% 3.83/4.03 cnf(c146,plain,iext(uri_rdf_type,uri_rdf_object,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_reification_object_type])).
% 3.83/4.03 cnf(c485,plain,ip(uri_rdf_object),inference(resolution,[status(thm)],[c146, c142])).
% 3.83/4.03 cnf(c489,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_object,uri_rdf_object),inference(resolution,[status(thm)],[c485, c28])).
% 3.83/4.03 cnf(c918,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X620)|iext(X620,uri_rdf_object,uri_rdf_object),inference(resolution,[status(thm)],[c489, c36])).
% 3.83/4.03 fof(rdf_reification_predicate_type,axiom,iext(uri_rdf_type,uri_rdf_value,uri_rdf_Property),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdf_reification_predicate_type)).
% 3.83/4.03 cnf(c145,plain,iext(uri_rdf_type,uri_rdf_value,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_reification_predicate_type])).
% 3.83/4.03 cnf(c473,plain,ip(uri_rdf_value),inference(resolution,[status(thm)],[c145, c142])).
% 3.83/4.03 cnf(c481,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_value,uri_rdf_value),inference(resolution,[status(thm)],[c473, c28])).
% 3.83/4.03 cnf(c910,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X618)|iext(X618,uri_rdf_value,uri_rdf_value),inference(resolution,[status(thm)],[c481, c36])).
% 3.83/4.03 cnf(c34,plain,~iext(uri_rdfs_subPropertyOf,X61,X62)|ip(X61),inference(split_conjunct,[status(thm)],[c33])).
% 3.83/4.03 cnf(c407,plain,ip(uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c131, c34])).
% 3.83/4.03 cnf(c480,plain,iext(uri_rdf_type,uri_rdfs_isDefinedBy,uri_rdf_Property),inference(resolution,[status(thm)],[c143, c407])).
% 3.83/4.03 cnf(c902,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X617)|iext(X617,uri_rdfs_isDefinedBy,uri_rdf_Property),inference(resolution,[status(thm)],[c480, c36])).
% 3.83/4.03 cnf(c406,plain,ip(uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c131, c35])).
% 3.83/4.03 cnf(c479,plain,iext(uri_rdf_type,uri_rdfs_seeAlso,uri_rdf_Property),inference(resolution,[status(thm)],[c143, c406])).
% 3.83/4.03 cnf(c895,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X616)|iext(X616,uri_rdfs_seeAlso,uri_rdf_Property),inference(resolution,[status(thm)],[c479, c36])).
% 3.83/4.03 fof(rdf_reification_subject_type,axiom,iext(uri_rdf_type,uri_rdf_subject,uri_rdf_Property),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdf_reification_subject_type)).
% 3.83/4.03 cnf(c144,plain,iext(uri_rdf_type,uri_rdf_subject,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_reification_subject_type])).
% 3.83/4.03 cnf(c466,plain,ip(uri_rdf_subject),inference(resolution,[status(thm)],[c144, c142])).
% 3.83/4.03 cnf(c470,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_subject,uri_rdf_subject),inference(resolution,[status(thm)],[c466, c28])).
% 3.83/4.03 cnf(c888,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X614)|iext(X614,uri_rdf_subject,uri_rdf_subject),inference(resolution,[status(thm)],[c470, c36])).
% 3.83/4.03 fof(rdf_value_type,axiom,iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdf_value_type)).
% 3.83/4.03 cnf(c136,plain,iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_value_type])).
% 3.83/4.03 cnf(c463,plain,ip(uri_rdf_type),inference(resolution,[status(thm)],[c142, c136])).
% 3.83/4.03 cnf(c464,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_type,uri_rdf_type),inference(resolution,[status(thm)],[c463, c28])).
% 3.83/4.03 cnf(c873,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X612)|iext(X612,uri_rdf_type,uri_rdf_type),inference(resolution,[status(thm)],[c464, c36])).
% 3.83/4.03 fof(rdfs_subpropertyof_trans,axiom,(![P]:(![Q]:(![R]:((iext(uri_rdfs_subPropertyOf,P,Q)&iext(uri_rdfs_subPropertyOf,Q,R))=>iext(uri_rdfs_subPropertyOf,P,R))))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_subpropertyof_trans)).
% 3.83/4.03 fof(c23,plain,(![P]:(![Q]:(![R]:((~iext(uri_rdfs_subPropertyOf,P,Q)|~iext(uri_rdfs_subPropertyOf,Q,R))|iext(uri_rdfs_subPropertyOf,P,R))))),inference(fof_nnf,[status(thm)],[rdfs_subpropertyof_trans])).
% 3.83/4.03 fof(c24,plain,(![X6]:(![X7]:(![X8]:((~iext(uri_rdfs_subPropertyOf,X6,X7)|~iext(uri_rdfs_subPropertyOf,X7,X8))|iext(uri_rdfs_subPropertyOf,X6,X8))))),inference(variable_rename,[status(thm)],[c23])).
% 3.83/4.03 cnf(c25,plain,~iext(uri_rdfs_subPropertyOf,X53,X51)|~iext(uri_rdfs_subPropertyOf,X51,X52)|iext(uri_rdfs_subPropertyOf,X53,X52),inference(split_conjunct,[status(thm)],[c24])).
% 3.83/4.03 fof(rdfs_container_n_type_002,axiom,iext(uri_rdf_type,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_type_002)).
% 3.83/4.03 cnf(c98,plain,iext(uri_rdf_type,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),inference(split_conjunct,[status(thm)],[rdfs_container_n_type_002])).
% 3.83/4.03 cnf(c421,plain,icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__2),inference(resolution,[status(thm)],[c125, c98])).
% 3.83/4.03 cnf(c443,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__2,uri_rdfs_member),inference(resolution,[status(thm)],[c421, c111])).
% 3.83/4.03 cnf(c868,plain,~iext(uri_rdfs_subPropertyOf,X611,uri_rdf__2)|iext(uri_rdfs_subPropertyOf,X611,uri_rdfs_member),inference(resolution,[status(thm)],[c443, c25])).
% 3.83/4.03 cnf(c866,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X610)|iext(X610,uri_rdf__2,uri_rdfs_member),inference(resolution,[status(thm)],[c443, c36])).
% 3.83/4.03 fof(rdfs_container_n_type_001,axiom,iext(uri_rdf_type,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_type_001)).
% 3.83/4.03 cnf(c99,plain,iext(uri_rdf_type,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),inference(split_conjunct,[status(thm)],[rdfs_container_n_type_001])).
% 3.83/4.03 cnf(c420,plain,icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__1),inference(resolution,[status(thm)],[c125, c99])).
% 3.83/4.03 cnf(c441,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__1,uri_rdfs_member),inference(resolution,[status(thm)],[c420, c111])).
% 3.83/4.03 cnf(c861,plain,~iext(uri_rdfs_subPropertyOf,X609,uri_rdf__1)|iext(uri_rdfs_subPropertyOf,X609,uri_rdfs_member),inference(resolution,[status(thm)],[c441, c25])).
% 3.83/4.03 cnf(c859,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X608)|iext(X608,uri_rdf__1,uri_rdfs_member),inference(resolution,[status(thm)],[c441, c36])).
% 3.83/4.03 fof(rdfs_container_alt_sub,axiom,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Container),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_alt_sub)).
% 3.83/4.03 cnf(c113,plain,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Container),inference(split_conjunct,[status(thm)],[rdfs_container_alt_sub])).
% 3.83/4.03 cnf(c244,plain,ic(uri_rdfs_Container),inference(resolution,[status(thm)],[c50, c113])).
% 3.83/4.03 cnf(c254,plain,icext(uri_rdfs_Class,uri_rdfs_Container),inference(resolution,[status(thm)],[c244, c81])).
% 3.83/4.03 cnf(c439,plain,iext(uri_rdf_type,uri_rdfs_Container,uri_rdfs_Class),inference(resolution,[status(thm)],[c126, c254])).
% 3.83/4.03 cnf(c854,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X607)|iext(X607,uri_rdfs_Container,uri_rdfs_Class),inference(resolution,[status(thm)],[c439, c36])).
% 3.83/4.03 cnf(c1434,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X606)|icext(X606,uri_rdfs_comment),inference(resolution,[status(thm)],[c1427, c62])).
% 3.83/4.03 fof(rdfs_dat_xmlliteral_sub,axiom,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Literal),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_dat_xmlliteral_sub)).
% 3.83/4.03 cnf(c95,plain,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[rdfs_dat_xmlliteral_sub])).
% 3.83/4.03 cnf(c246,plain,ic(uri_rdfs_Literal),inference(resolution,[status(thm)],[c50, c95])).
% 3.83/4.03 cnf(c262,plain,icext(uri_rdfs_Class,uri_rdfs_Literal),inference(resolution,[status(thm)],[c246, c81])).
% 3.83/4.03 cnf(c438,plain,iext(uri_rdf_type,uri_rdfs_Literal,uri_rdfs_Class),inference(resolution,[status(thm)],[c126, c262])).
% 3.83/4.03 cnf(c849,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X605)|iext(X605,uri_rdfs_Literal,uri_rdfs_Class),inference(resolution,[status(thm)],[c438, c36])).
% 3.83/4.03 cnf(c1432,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X604)|icext(X604,uri_rdfs_comment),inference(resolution,[status(thm)],[c1427, c88])).
% 3.83/4.03 fof(rdfs_container_seq_sub,axiom,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Container),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_seq_sub)).
% 3.83/4.03 cnf(c96,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Container),inference(split_conjunct,[status(thm)],[rdfs_container_seq_sub])).
% 3.83/4.03 cnf(c49,plain,~iext(uri_rdfs_subClassOf,X74,X75)|ic(X74),inference(split_conjunct,[status(thm)],[c48])).
% 3.83/4.03 cnf(c231,plain,ic(uri_rdfs_Seq),inference(resolution,[status(thm)],[c49, c96])).
% 3.83/4.03 cnf(c248,plain,icext(uri_rdfs_Class,uri_rdfs_Seq),inference(resolution,[status(thm)],[c231, c81])).
% 3.83/4.03 cnf(c435,plain,iext(uri_rdf_type,uri_rdfs_Seq,uri_rdfs_Class),inference(resolution,[status(thm)],[c126, c248])).
% 3.83/4.03 cnf(c844,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X601)|iext(X601,uri_rdfs_Seq,uri_rdfs_Class),inference(resolution,[status(thm)],[c435, c36])).
% 3.83/4.03 cnf(c1405,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X600)|icext(X600,uri_rdfs_label),inference(resolution,[status(thm)],[c1397, c62])).
% 3.83/4.03 cnf(c1403,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X599)|icext(X599,uri_rdfs_label),inference(resolution,[status(thm)],[c1397, c88])).
% 3.83/4.03 cnf(c230,plain,ic(uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c49, c95])).
% 3.83/4.03 cnf(c240,plain,icext(uri_rdfs_Class,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c230, c81])).
% 3.83/4.03 cnf(c433,plain,iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Class),inference(resolution,[status(thm)],[c126, c240])).
% 3.83/4.03 cnf(c839,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X597)|iext(X597,uri_rdf_XMLLiteral,uri_rdfs_Class),inference(resolution,[status(thm)],[c433, c36])).
% 3.83/4.03 fof(rdfs_datatype_sub,axiom,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Class),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_datatype_sub)).
% 3.83/4.03 cnf(c90,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_datatype_sub])).
% 3.83/4.03 cnf(c243,plain,ic(uri_rdfs_Class),inference(resolution,[status(thm)],[c50, c90])).
% 3.83/4.03 cnf(c252,plain,icext(uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c243, c81])).
% 3.83/4.03 cnf(c432,plain,iext(uri_rdf_type,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c126, c252])).
% 3.83/4.03 cnf(c834,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X593)|iext(X593,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c432, c36])).
% 3.83/4.03 cnf(c1344,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X592)|icext(X592,uri_rdf_predicate),inference(resolution,[status(thm)],[c1337, c62])).
% 3.83/4.03 cnf(c1342,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X591)|icext(X591,uri_rdf_predicate),inference(resolution,[status(thm)],[c1337, c88])).
% 3.83/4.03 cnf(c227,plain,ic(uri_rdfs_Datatype),inference(resolution,[status(thm)],[c49, c90])).
% 3.83/4.03 cnf(c234,plain,icext(uri_rdfs_Class,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c227, c81])).
% 3.83/4.03 cnf(c430,plain,iext(uri_rdf_type,uri_rdfs_Datatype,uri_rdfs_Class),inference(resolution,[status(thm)],[c126, c234])).
% 3.83/4.03 cnf(c829,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X589)|iext(X589,uri_rdfs_Datatype,uri_rdfs_Class),inference(resolution,[status(thm)],[c430, c36])).
% 3.83/4.03 cnf(c228,plain,ic(uri_rdf_Alt),inference(resolution,[status(thm)],[c49, c113])).
% 3.83/4.03 cnf(c236,plain,icext(uri_rdfs_Class,uri_rdf_Alt),inference(resolution,[status(thm)],[c228, c81])).
% 3.83/4.03 cnf(c429,plain,iext(uri_rdf_type,uri_rdf_Alt,uri_rdfs_Class),inference(resolution,[status(thm)],[c126, c236])).
% 3.83/4.03 cnf(c824,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X585)|iext(X585,uri_rdf_Alt,uri_rdfs_Class),inference(resolution,[status(thm)],[c429, c36])).
% 3.83/4.03 cnf(c1316,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X584)|icext(X584,uri_owl_Class),inference(resolution,[status(thm)],[c1294, c62])).
% 3.83/4.03 fof(rdfs_container_bag_sub,axiom,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Container),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_bag_sub)).
% 3.83/4.03 cnf(c112,plain,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Container),inference(split_conjunct,[status(thm)],[rdfs_container_bag_sub])).
% 3.83/4.03 cnf(c229,plain,ic(uri_rdf_Bag),inference(resolution,[status(thm)],[c49, c112])).
% 3.83/4.03 cnf(c238,plain,icext(uri_rdfs_Class,uri_rdf_Bag),inference(resolution,[status(thm)],[c229, c81])).
% 3.83/4.03 cnf(c426,plain,iext(uri_rdf_type,uri_rdf_Bag,uri_rdfs_Class),inference(resolution,[status(thm)],[c126, c238])).
% 3.83/4.03 cnf(c819,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X581)|iext(X581,uri_rdf_Bag,uri_rdfs_Class),inference(resolution,[status(thm)],[c426, c36])).
% 3.83/4.03 cnf(c1304,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X580)|icext(X580,uri_owl_Class),inference(resolution,[status(thm)],[c1292, c88])).
% 3.83/4.03 cnf(c226,plain,ic(uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c49, c108])).
% 3.83/4.03 cnf(c232,plain,icext(uri_rdfs_Class,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c226, c81])).
% 3.83/4.03 cnf(c425,plain,iext(uri_rdf_type,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Class),inference(resolution,[status(thm)],[c126, c232])).
% 3.83/4.03 cnf(c814,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X576)|iext(X576,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Class),inference(resolution,[status(thm)],[c425, c36])).
% 3.83/4.03 cnf(c1269,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X574)|icext(X574,uri_ex_PersonAttribute),inference(resolution,[status(thm)],[c1180, c62])).
% 3.83/4.03 cnf(c807,plain,~iext(uri_rdfs_subPropertyOf,X572,uri_rdf__3)|iext(uri_rdfs_subPropertyOf,X572,uri_rdfs_member),inference(resolution,[status(thm)],[c424, c25])).
% 3.83/4.03 cnf(c1258,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X570)|icext(X570,uri_ex_PersonAttribute),inference(resolution,[status(thm)],[c1178, c88])).
% 3.83/4.03 cnf(c805,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X568)|iext(X568,uri_rdf__3,uri_rdfs_member),inference(resolution,[status(thm)],[c424, c36])).
% 3.83/4.03 cnf(c1247,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X566)|icext(X566,uri_owl_Restriction),inference(resolution,[status(thm)],[c1165, c62])).
% 3.83/4.03 cnf(c1235,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X562)|icext(X562,uri_owl_Restriction),inference(resolution,[status(thm)],[c1163, c88])).
% 3.83/4.03 cnf(c411,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c407, c28])).
% 3.83/4.03 cnf(c798,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X559)|iext(X559,uri_rdfs_isDefinedBy,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c411, c36])).
% 3.83/4.03 cnf(c1225,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X558)|icext(X558,uri_rdfs_Statement),inference(resolution,[status(thm)],[c1152, c62])).
% 3.83/4.03 cnf(c1214,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X554)|icext(X554,uri_rdfs_Statement),inference(resolution,[status(thm)],[c1150, c88])).
% 3.83/4.03 cnf(c410,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_seeAlso,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c406, c28])).
% 3.83/4.03 cnf(c791,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X551)|iext(X551,uri_rdfs_seeAlso,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c410, c36])).
% 3.83/4.03 cnf(c1204,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X550)|icext(X550,uri_rdf_List),inference(resolution,[status(thm)],[c1146, c62])).
% 3.83/4.03 cnf(c400,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Resource),inference(resolution,[status(thm)],[c120, c231])).
% 3.83/4.03 cnf(c788,plain,~iext(uri_rdfs_subClassOf,X547,uri_rdfs_Seq)|iext(uri_rdfs_subClassOf,X547,uri_rdfs_Resource),inference(resolution,[status(thm)],[c400, c40])).
% 3.83/4.03 cnf(c1193,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X546)|icext(X546,uri_rdf_List),inference(resolution,[status(thm)],[c1144, c88])).
% 3.83/4.03 cnf(c783,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X542)|iext(X542,uri_rdfs_Seq,uri_rdfs_Resource),inference(resolution,[status(thm)],[c400, c36])).
% 3.83/4.03 cnf(c1157,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X539)|icext(X539,uri_rdfs_member),inference(resolution,[status(thm)],[c812, c88])).
% 3.83/4.03 cnf(c399,plain,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Resource),inference(resolution,[status(thm)],[c120, c229])).
% 3.83/4.03 cnf(c780,plain,~iext(uri_rdfs_subClassOf,X538,uri_rdf_Bag)|iext(uri_rdfs_subClassOf,X538,uri_rdfs_Resource),inference(resolution,[status(thm)],[c399, c40])).
% 3.83/4.03 cnf(c775,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X534)|iext(X534,uri_rdf_Bag,uri_rdfs_Resource),inference(resolution,[status(thm)],[c399, c36])).
% 3.83/4.03 cnf(c1130,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X533)|icext(X533,uri_rdfs_Resource),inference(resolution,[status(thm)],[c714, c88])).
% 3.83/4.03 cnf(c398,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c120, c243])).
% 3.83/4.03 cnf(c772,plain,~iext(uri_rdfs_subClassOf,X530,uri_rdfs_Class)|iext(uri_rdfs_subClassOf,X530,uri_rdfs_Resource),inference(resolution,[status(thm)],[c398, c40])).
% 3.83/4.03 cnf(c1118,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X529)|icext(X529,uri_owl_intersectionOf),inference(resolution,[status(thm)],[c624, c62])).
% 3.83/4.03 cnf(c1116,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X528)|icext(X528,uri_owl_intersectionOf),inference(resolution,[status(thm)],[c624, c88])).
% 3.83/4.03 cnf(c767,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X527)|iext(X527,uri_rdfs_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c398, c36])).
% 3.83/4.03 cnf(c1103,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X524)|icext(X524,uri_ex_name),inference(resolution,[status(thm)],[c622, c62])).
% 3.83/4.03 cnf(c397,plain,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Resource),inference(resolution,[status(thm)],[c120, c226])).
% 3.83/4.03 cnf(c764,plain,~iext(uri_rdfs_subClassOf,X523,uri_rdfs_ContainerMembershipProperty)|iext(uri_rdfs_subClassOf,X523,uri_rdfs_Resource),inference(resolution,[status(thm)],[c397, c40])).
% 3.83/4.03 cnf(c1101,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X522)|icext(X522,uri_ex_name),inference(resolution,[status(thm)],[c622, c88])).
% 3.83/4.03 cnf(c759,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X519)|iext(X519,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Resource),inference(resolution,[status(thm)],[c397, c36])).
% 3.83/4.03 cnf(c1088,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X518)|icext(X518,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c620, c62])).
% 3.83/4.03 cnf(c1083,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X517)|icext(X517,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c620, c88])).
% 3.83/4.03 cnf(c396,plain,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Resource),inference(resolution,[status(thm)],[c120, c230])).
% 3.83/4.03 cnf(c756,plain,~iext(uri_rdfs_subClassOf,X516,uri_rdf_XMLLiteral)|iext(uri_rdfs_subClassOf,X516,uri_rdfs_Resource),inference(resolution,[status(thm)],[c396, c40])).
% 3.83/4.03 cnf(c1064,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X513)|icext(X513,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c618, c62])).
% 3.83/4.03 cnf(c751,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X512)|iext(X512,uri_rdf_XMLLiteral,uri_rdfs_Resource),inference(resolution,[status(thm)],[c396, c36])).
% 3.83/4.03 cnf(c1062,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X511)|icext(X511,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c618, c88])).
% 3.83/4.03 cnf(c395,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Literal,uri_rdfs_Resource),inference(resolution,[status(thm)],[c120, c246])).
% 3.83/4.03 cnf(c748,plain,~iext(uri_rdfs_subClassOf,X509,uri_rdfs_Literal)|iext(uri_rdfs_subClassOf,X509,uri_rdfs_Resource),inference(resolution,[status(thm)],[c395, c40])).
% 3.83/4.03 cnf(c1047,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X507)|icext(X507,uri_owl_hasValue),inference(resolution,[status(thm)],[c616, c62])).
% 3.83/4.03 cnf(c743,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X506)|iext(X506,uri_rdfs_Literal,uri_rdfs_Resource),inference(resolution,[status(thm)],[c395, c36])).
% 3.83/4.03 cnf(c1045,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X505)|icext(X505,uri_owl_hasValue),inference(resolution,[status(thm)],[c616, c88])).
% 3.83/4.03 cnf(c394,plain,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Resource),inference(resolution,[status(thm)],[c120, c228])).
% 3.83/4.03 cnf(c740,plain,~iext(uri_rdfs_subClassOf,X502,uri_rdf_Alt)|iext(uri_rdfs_subClassOf,X502,uri_rdfs_Resource),inference(resolution,[status(thm)],[c394, c40])).
% 3.83/4.03 cnf(c1031,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X501)|icext(X501,uri_owl_onProperty),inference(resolution,[status(thm)],[c614, c62])).
% 3.83/4.03 cnf(c1029,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X500)|icext(X500,uri_owl_onProperty),inference(resolution,[status(thm)],[c614, c88])).
% 3.83/4.03 cnf(c735,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X498)|iext(X498,uri_rdf_Alt,uri_rdfs_Resource),inference(resolution,[status(thm)],[c394, c36])).
% 3.83/4.03 cnf(c393,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Container,uri_rdfs_Resource),inference(resolution,[status(thm)],[c120, c244])).
% 3.83/4.03 cnf(c732,plain,~iext(uri_rdfs_subClassOf,X496,uri_rdfs_Container)|iext(uri_rdfs_subClassOf,X496,uri_rdfs_Resource),inference(resolution,[status(thm)],[c393, c40])).
% 3.83/4.03 cnf(c1014,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X495)|icext(X495,uri_rdfs_range),inference(resolution,[status(thm)],[c612, c62])).
% 3.83/4.03 cnf(c1009,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X494)|icext(X494,uri_rdfs_range),inference(resolution,[status(thm)],[c612, c88])).
% 3.83/4.03 cnf(c727,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X493)|iext(X493,uri_rdfs_Container,uri_rdfs_Resource),inference(resolution,[status(thm)],[c393, c36])).
% 3.83/4.03 cnf(c988,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X490)|icext(X490,uri_rdfs_domain),inference(resolution,[status(thm)],[c610, c62])).
% 3.83/4.03 cnf(c392,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Resource),inference(resolution,[status(thm)],[c120, c227])).
% 3.83/4.03 cnf(c724,plain,~iext(uri_rdfs_subClassOf,X489,uri_rdfs_Datatype)|iext(uri_rdfs_subClassOf,X489,uri_rdfs_Resource),inference(resolution,[status(thm)],[c392, c40])).
% 3.83/4.03 cnf(c981,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X488)|icext(X488,uri_rdfs_domain),inference(resolution,[status(thm)],[c610, c88])).
% 3.83/4.03 cnf(c967,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X487)|icext(X487,uri_rdf_first),inference(resolution,[status(thm)],[c534, c62])).
% 3.83/4.03 cnf(c719,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X486)|iext(X486,uri_rdfs_Datatype,uri_rdfs_Resource),inference(resolution,[status(thm)],[c392, c36])).
% 3.83/4.03 cnf(c965,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X485)|icext(X485,uri_rdf_first),inference(resolution,[status(thm)],[c534, c88])).
% 3.83/4.03 cnf(c711,plain,~iext(uri_rdfs_subClassOf,X484,uri_rdf_Property)|iext(uri_rdfs_subClassOf,X484,uri_rdfs_Resource),inference(resolution,[status(thm)],[c391, c40])).
% 3.83/4.03 cnf(c957,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X483)|icext(X483,uri_rdf_rest),inference(resolution,[status(thm)],[c521, c62])).
% 3.83/4.03 cnf(c953,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X482)|icext(X482,uri_rdf_rest),inference(resolution,[status(thm)],[c521, c88])).
% 3.83/4.03 cnf(c706,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X481)|iext(X481,uri_rdf_Property,uri_rdfs_Resource),inference(resolution,[status(thm)],[c391, c36])).
% 3.83/4.03 cnf(c946,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X480)|icext(X480,uri_rdf__1),inference(resolution,[status(thm)],[c513, c62])).
% 3.83/4.03 cnf(c939,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X478)|icext(X478,uri_rdf__2),inference(resolution,[status(thm)],[c505, c62])).
% 3.83/4.03 cnf(c932,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X475)|icext(X475,uri_rdf__3),inference(resolution,[status(thm)],[c497, c62])).
% 3.83/4.03 cnf(c263,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Literal,uri_rdfs_Literal),inference(resolution,[status(thm)],[c246, c43])).
% 3.83/4.03 cnf(c698,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X473)|iext(X473,uri_rdfs_Literal,uri_rdfs_Literal),inference(resolution,[status(thm)],[c263, c36])).
% 3.83/4.03 cnf(c924,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X472)|icext(X472,uri_rdf_object),inference(resolution,[status(thm)],[c489, c62])).
% 3.83/4.03 cnf(c922,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X471)|icext(X471,uri_rdf_object),inference(resolution,[status(thm)],[c489, c88])).
% 3.83/4.03 cnf(c916,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X470)|icext(X470,uri_rdf_value),inference(resolution,[status(thm)],[c481, c62])).
% 3.83/4.03 cnf(c914,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X468)|icext(X468,uri_rdf_value),inference(resolution,[status(thm)],[c481, c88])).
% 3.83/4.03 cnf(c255,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Container,uri_rdfs_Container),inference(resolution,[status(thm)],[c244, c43])).
% 3.83/4.03 cnf(c690,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X465)|iext(X465,uri_rdfs_Container,uri_rdfs_Container),inference(resolution,[status(thm)],[c255, c36])).
% 3.83/4.03 cnf(c894,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X462)|icext(X462,uri_rdf_subject),inference(resolution,[status(thm)],[c470, c62])).
% 3.83/4.03 cnf(c892,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X460)|icext(X460,uri_rdf_subject),inference(resolution,[status(thm)],[c470, c88])).
% 3.83/4.03 cnf(c886,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X459)|icext(X459,uri_rdf_type),inference(resolution,[status(thm)],[c464, c62])).
% 3.83/4.03 cnf(c253,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c243, c43])).
% 3.83/4.03 cnf(c682,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X458)|iext(X458,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c253, c36])).
% 3.83/4.03 cnf(c882,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X457)|icext(X457,uri_rdf_type),inference(resolution,[status(thm)],[c464, c88])).
% 3.83/4.03 cnf(c870,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X455)|icext(X455,uri_rdf__2),inference(resolution,[status(thm)],[c443, c88])).
% 3.83/4.03 cnf(c863,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X452)|icext(X452,uri_rdf__1),inference(resolution,[status(thm)],[c441, c88])).
% 3.83/4.03 cnf(c251,plain,iext(uri_rdfs_subClassOf,uri_rdf_Property,uri_rdf_Property),inference(resolution,[status(thm)],[c242, c43])).
% 3.83/4.03 cnf(c674,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X449)|iext(X449,uri_rdf_Property,uri_rdf_Property),inference(resolution,[status(thm)],[c251, c36])).
% 3.83/4.03 cnf(c249,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Seq),inference(resolution,[status(thm)],[c231, c43])).
% 3.83/4.03 cnf(c666,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X438)|iext(X438,uri_rdfs_Seq,uri_rdfs_Seq),inference(resolution,[status(thm)],[c249, c36])).
% 3.83/4.03 cnf(c811,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X429)|icext(X429,uri_rdfs_member),inference(resolution,[status(thm)],[c424, c62])).
% 3.83/4.03 cnf(c241,plain,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c230, c43])).
% 3.83/4.03 cnf(c658,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X428)|iext(X428,uri_rdf_XMLLiteral,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c241, c36])).
% 3.83/4.03 cnf(c809,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X427)|icext(X427,uri_rdf__3),inference(resolution,[status(thm)],[c424, c88])).
% 3.83/4.03 cnf(c804,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X426)|icext(X426,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c411, c62])).
% 3.83/4.03 cnf(c795,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X422)|icext(X422,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c410, c88])).
% 3.83/4.03 cnf(c239,plain,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdf_Bag),inference(resolution,[status(thm)],[c229, c43])).
% 3.83/4.03 cnf(c650,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X420)|iext(X420,uri_rdf_Bag,uri_rdf_Bag),inference(resolution,[status(thm)],[c239, c36])).
% 3.83/4.03 cnf(c237,plain,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdf_Alt),inference(resolution,[status(thm)],[c228, c43])).
% 3.83/4.03 cnf(c642,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X409)|iext(X409,uri_rdf_Alt,uri_rdf_Alt),inference(resolution,[status(thm)],[c237, c36])).
% 3.83/4.03 cnf(c235,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c227, c43])).
% 3.83/4.03 cnf(c634,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X399)|iext(X399,uri_rdfs_Datatype,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c235, c36])).
% 3.83/4.03 cnf(c712,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X398)|icext(X398,uri_rdfs_Resource),inference(resolution,[status(thm)],[c391, c62])).
% 3.83/4.03 cnf(c701,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X395)|icext(X395,uri_rdfs_Literal),inference(resolution,[status(thm)],[c263, c88])).
% 3.83/4.03 cnf(c693,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X392)|icext(X392,uri_rdfs_Container),inference(resolution,[status(thm)],[c255, c88])).
% 3.83/4.03 cnf(c233,plain,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c226, c43])).
% 3.83/4.03 cnf(c626,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X390)|iext(X390,uri_rdfs_ContainerMembershipProperty,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c233, c36])).
% 3.83/4.03 cnf(c685,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X389)|icext(X389,uri_rdfs_Class),inference(resolution,[status(thm)],[c253, c88])).
% 3.83/4.03 cnf(c531,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X387)|iext(X387,uri_rdf_first,uri_rdf_Property),inference(resolution,[status(thm)],[c152, c36])).
% 3.83/4.03 cnf(c677,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X386)|icext(X386,uri_rdf_Property),inference(resolution,[status(thm)],[c251, c88])).
% 3.83/4.03 cnf(c672,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X385)|icext(X385,uri_rdfs_Seq),inference(resolution,[status(thm)],[c249, c62])).
% 3.83/4.03 fof(rdf_collection_nil_type,axiom,iext(uri_rdf_type,uri_rdf_nil,uri_rdf_List),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdf_collection_nil_type)).
% 3.83/4.03 cnf(c151,plain,iext(uri_rdf_type,uri_rdf_nil,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdf_collection_nil_type])).
% 3.83/4.03 cnf(c525,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X383)|iext(X383,uri_rdf_nil,uri_rdf_List),inference(resolution,[status(thm)],[c151, c36])).
% 3.83/4.03 cnf(c664,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X382)|icext(X382,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c241, c62])).
% 3.83/4.03 cnf(c518,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X380)|iext(X380,uri_rdf_rest,uri_rdf_Property),inference(resolution,[status(thm)],[c150, c36])).
% 3.83/4.03 cnf(c656,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X379)|icext(X379,uri_rdf_Bag),inference(resolution,[status(thm)],[c239, c62])).
% 3.83/4.03 cnf(c648,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X377)|icext(X377,uri_rdf_Alt),inference(resolution,[status(thm)],[c237, c62])).
% 3.83/4.03 cnf(c510,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X376)|iext(X376,uri_rdf__1,uri_rdf_Property),inference(resolution,[status(thm)],[c149, c36])).
% 3.83/4.03 cnf(c640,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X374)|icext(X374,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c235, c62])).
% 3.83/4.03 cnf(c502,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X372)|iext(X372,uri_rdf__2,uri_rdf_Property),inference(resolution,[status(thm)],[c148, c36])).
% 3.83/4.03 cnf(c632,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X371)|icext(X371,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c233, c62])).
% 3.83/4.03 cnf(c494,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X368)|iext(X368,uri_rdf__3,uri_rdf_Property),inference(resolution,[status(thm)],[c147, c36])).
% 3.83/4.03 cnf(c527,plain,~iext(uri_rdfs_range,uri_rdf_type,X366)|icext(X366,uri_rdf_List),inference(resolution,[status(thm)],[c151, c62])).
% 3.83/4.03 cnf(c486,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X364)|iext(X364,uri_rdf_object,uri_rdf_Property),inference(resolution,[status(thm)],[c146, c36])).
% 3.83/4.03 cnf(c474,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X359)|iext(X359,uri_rdf_value,uri_rdf_Property),inference(resolution,[status(thm)],[c145, c36])).
% 3.83/4.03 cnf(c467,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X354)|iext(X354,uri_rdf_subject,uri_rdf_Property),inference(resolution,[status(thm)],[c144, c36])).
% 3.83/4.03 cnf(c459,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X349)|iext(X349,uri_rdf_type,uri_rdf_Property),inference(resolution,[status(thm)],[c136, c36])).
% 3.83/4.03 cnf(c461,plain,~iext(uri_rdfs_range,uri_rdf_type,X346)|icext(X346,uri_rdf_Property),inference(resolution,[status(thm)],[c136, c62])).
% 3.83/4.03 fof(rdfs_annotation_comment_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_comment,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_comment_domain)).
% 3.83/4.03 cnf(c135,plain,iext(uri_rdfs_domain,uri_rdfs_comment,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_comment_domain])).
% 3.83/4.03 cnf(c456,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X345)|iext(X345,uri_rdfs_comment,uri_rdfs_Resource),inference(resolution,[status(thm)],[c135, c36])).
% 3.83/4.03 cnf(c455,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X342)|icext(X342,uri_rdfs_comment),inference(resolution,[status(thm)],[c135, c88])).
% 3.83/4.03 cnf(c453,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X341)|iext(X341,uri_rdfs_comment,uri_rdfs_Literal),inference(resolution,[status(thm)],[c134, c36])).
% 3.83/4.03 fof(rdfs_annotation_isdefinedby_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_isdefinedby_domain)).
% 3.83/4.03 cnf(c133,plain,iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_domain])).
% 3.83/4.03 cnf(c450,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X339)|iext(X339,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(resolution,[status(thm)],[c133, c36])).
% 3.83/4.03 fof(simple_ir,axiom,(![X]:ir(X)),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', simple_ir)).
% 3.83/4.03 fof(c156,plain,(![X45]:ir(X45)),inference(variable_rename,[status(thm)],[simple_ir])).
% 3.83/4.03 cnf(c157,plain,ir(X49),inference(split_conjunct,[status(thm)],[c156])).
% 3.83/4.03 fof(rdfs_ir_def,axiom,(![X]:(ir(X)<=>icext(uri_rdfs_Resource,X))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_ir_def)).
% 3.83/4.03 fof(c71,plain,(![X]:((~ir(X)|icext(uri_rdfs_Resource,X))&(~icext(uri_rdfs_Resource,X)|ir(X)))),inference(fof_nnf,[status(thm)],[rdfs_ir_def])).
% 3.83/4.03 fof(c72,plain,((![X]:(~ir(X)|icext(uri_rdfs_Resource,X)))&(![X]:(~icext(uri_rdfs_Resource,X)|ir(X)))),inference(shift_quantors,[status(thm)],[c71])).
% 3.83/4.03 fof(c74,plain,(![X27]:(![X28]:((~ir(X27)|icext(uri_rdfs_Resource,X27))&(~icext(uri_rdfs_Resource,X28)|ir(X28))))),inference(shift_quantors,[status(thm)],[fof(c73,plain,((![X27]:(~ir(X27)|icext(uri_rdfs_Resource,X27)))&(![X28]:(~icext(uri_rdfs_Resource,X28)|ir(X28)))),inference(variable_rename,[status(thm)],[c72])).])).
% 3.83/4.03 cnf(c75,plain,~ir(X57)|icext(uri_rdfs_Resource,X57),inference(split_conjunct,[status(thm)],[c74])).
% 3.83/4.03 cnf(c164,plain,icext(uri_rdfs_Resource,X58),inference(resolution,[status(thm)],[c75, c157])).
% 3.83/4.03 cnf(c428,plain,iext(uri_rdf_type,X96,uri_rdfs_Resource),inference(resolution,[status(thm)],[c126, c164])).
% 3.83/4.03 cnf(c446,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X337)|iext(X337,X336,uri_rdfs_Resource),inference(resolution,[status(thm)],[c428, c36])).
% 3.83/4.03 fof(rdfs_annotation_isdefinedby_range,axiom,iext(uri_rdfs_range,uri_rdfs_isDefinedBy,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_isdefinedby_range)).
% 3.83/4.03 cnf(c132,plain,iext(uri_rdfs_range,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_range])).
% 3.83/4.03 cnf(c413,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X334)|iext(X334,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(resolution,[status(thm)],[c132, c36])).
% 3.83/4.03 cnf(c449,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X332)|icext(X332,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c133, c88])).
% 3.83/4.03 cnf(c409,plain,~iext(uri_rdfs_subPropertyOf,X331,uri_rdfs_isDefinedBy)|iext(uri_rdfs_subPropertyOf,X331,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c131, c25])).
% 3.83/4.03 cnf(c448,plain,~iext(uri_rdfs_range,uri_rdf_type,X330)|icext(X330,uri_rdfs_Resource),inference(resolution,[status(thm)],[c428, c62])).
% 3.83/4.03 cnf(c412,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X328)|icext(X328,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c132, c88])).
% 3.83/4.03 cnf(c405,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X327)|iext(X327,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c131, c36])).
% 3.83/4.03 cnf(c408,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X326)|icext(X326,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c131, c62])).
% 3.83/4.03 cnf(c404,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X325)|icext(X325,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c131, c88])).
% 3.83/4.03 fof(rdfs_annotation_label_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_label,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_label_domain)).
% 3.83/4.03 cnf(c130,plain,iext(uri_rdfs_domain,uri_rdfs_label,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_label_domain])).
% 3.83/4.03 cnf(c402,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X324)|iext(X324,uri_rdfs_label,uri_rdfs_Resource),inference(resolution,[status(thm)],[c130, c36])).
% 3.83/4.03 cnf(c401,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X322)|icext(X322,uri_rdfs_label),inference(resolution,[status(thm)],[c130, c88])).
% 3.83/4.03 cnf(c390,plain,~iext(uri_rdfs_range,uri_rdfs_range,X321)|icext(X321,uri_rdfs_Literal),inference(resolution,[status(thm)],[c129, c62])).
% 3.83/4.03 cnf(c389,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X320)|iext(X320,uri_rdfs_label,uri_rdfs_Literal),inference(resolution,[status(thm)],[c129, c36])).
% 3.83/4.03 fof(rdfs_annotation_seealso_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_seeAlso,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_seealso_domain)).
% 3.83/4.03 cnf(c128,plain,iext(uri_rdfs_domain,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_seealso_domain])).
% 3.83/4.03 cnf(c386,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X319)|iext(X319,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(resolution,[status(thm)],[c128, c36])).
% 3.83/4.03 cnf(c383,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X316)|iext(X316,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(resolution,[status(thm)],[c127, c36])).
% 3.83/4.03 cnf(c385,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X315)|icext(X315,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c128, c88])).
% 3.83/4.03 cnf(c382,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X313)|icext(X313,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c127, c88])).
% 3.83/4.03 cnf(c375,plain,~iext(uri_rdfs_domain,uri_rdf_rest,X312)|icext(X312,skolem0002),inference(resolution,[status(thm)],[c88, c8])).
% 3.83/4.03 cnf(c373,plain,~iext(uri_rdfs_domain,uri_rdf_rest,X310)|icext(X310,skolem0001),inference(resolution,[status(thm)],[c88, c6])).
% 3.83/4.03 fof(rdfs_reification_subject_range,axiom,iext(uri_rdfs_range,uri_rdf_subject,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_reification_subject_range)).
% 3.83/4.03 cnf(c53,plain,iext(uri_rdfs_range,uri_rdf_subject,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_reification_subject_range])).
% 3.83/4.03 cnf(c372,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X309)|icext(X309,uri_rdf_subject),inference(resolution,[status(thm)],[c88, c53])).
% 3.83/4.03 cnf(c9,plain,iext(uri_rdf_first,skolem0003,skolem0004),inference(split_conjunct,[status(thm)],[c2])).
% 3.83/4.03 cnf(c370,plain,~iext(uri_rdfs_domain,uri_rdf_first,X307)|icext(X307,skolem0003),inference(resolution,[status(thm)],[c88, c9])).
% 3.83/4.03 cnf(c369,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X306)|icext(X306,uri_rdfs_Seq),inference(resolution,[status(thm)],[c88, c96])).
% 3.83/4.03 cnf(c7,plain,iext(uri_rdf_first,skolem0002,uri_owl_FunctionalProperty),inference(split_conjunct,[status(thm)],[c2])).
% 3.83/4.03 cnf(c368,plain,~iext(uri_rdfs_domain,uri_rdf_first,X305)|icext(X305,skolem0002),inference(resolution,[status(thm)],[c88, c7])).
% 3.83/4.03 fof(rdfs_collection_rest_domain,axiom,iext(uri_rdfs_domain,uri_rdf_rest,uri_rdf_List),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_collection_rest_domain)).
% 3.83/4.03 cnf(c115,plain,iext(uri_rdfs_domain,uri_rdf_rest,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdfs_collection_rest_domain])).
% 3.83/4.03 cnf(c367,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X304)|icext(X304,uri_rdf_rest),inference(resolution,[status(thm)],[c88, c115])).
% 3.83/4.03 fof(rdfs_container_n_range_002,axiom,iext(uri_rdfs_range,uri_rdf__2,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_range_002)).
% 3.83/4.03 cnf(c101,plain,iext(uri_rdfs_range,uri_rdf__2,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_range_002])).
% 3.83/4.03 cnf(c365,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X302)|icext(X302,uri_rdf__2),inference(resolution,[status(thm)],[c88, c101])).
% 3.83/4.03 fof(rdfs_container_n_range_003,axiom,iext(uri_rdfs_range,uri_rdf__3,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_range_003)).
% 3.83/4.03 cnf(c100,plain,iext(uri_rdfs_range,uri_rdf__3,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_range_003])).
% 3.83/4.03 cnf(c363,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X300)|icext(X300,uri_rdf__3),inference(resolution,[status(thm)],[c88, c100])).
% 3.83/4.03 fof(rdfs_container_n_domain_001,axiom,iext(uri_rdfs_domain,uri_rdf__1,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_domain_001)).
% 3.83/4.03 cnf(c105,plain,iext(uri_rdfs_domain,uri_rdf__1,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_001])).
% 3.83/4.03 cnf(c362,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X299)|icext(X299,uri_rdf__1),inference(resolution,[status(thm)],[c88, c105])).
% 3.83/4.03 fof(rdfs_container_n_range_001,axiom,iext(uri_rdfs_range,uri_rdf__1,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_range_001)).
% 3.83/4.03 cnf(c102,plain,iext(uri_rdfs_range,uri_rdf__1,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_range_001])).
% 3.83/4.03 cnf(c360,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X297)|icext(X297,uri_rdf__1),inference(resolution,[status(thm)],[c88, c102])).
% 3.83/4.03 cnf(c359,plain,~iext(uri_rdfs_domain,uri_owl_intersectionOf,X296)|icext(X296,uri_ex_PersonAttribute),inference(resolution,[status(thm)],[c88, c4])).
% 3.83/4.03 cnf(c357,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X294)|icext(X294,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c88, c95])).
% 3.83/4.03 cnf(c356,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X293)|icext(X293,uri_rdf_rest),inference(resolution,[status(thm)],[c88, c114])).
% 3.83/4.03 cnf(c355,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X292)|icext(X292,uri_rdf_Bag),inference(resolution,[status(thm)],[c88, c112])).
% 3.83/4.03 cnf(c353,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X290)|icext(X290,uri_rdfs_range),inference(resolution,[status(thm)],[c88, c63])).
% 3.83/4.03 fof(rdfs_range_range,axiom,iext(uri_rdfs_range,uri_rdfs_range,uri_rdfs_Class),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_range_range)).
% 3.83/4.03 cnf(c59,plain,iext(uri_rdfs_range,uri_rdfs_range,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_range_range])).
% 3.83/4.03 cnf(c351,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X288)|icext(X288,uri_rdfs_range),inference(resolution,[status(thm)],[c88, c59])).
% 3.83/4.03 cnf(c350,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X287)|icext(X287,uri_rdf_Alt),inference(resolution,[status(thm)],[c88, c113])).
% 3.83/4.03 cnf(c349,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X286)|icext(X286,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c88, c90])).
% 3.83/4.03 fof(rdfs_reification_predicate_range,axiom,iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_reification_predicate_range)).
% 3.83/4.03 cnf(c55,plain,iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_reification_predicate_range])).
% 3.83/4.03 cnf(c348,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X285)|icext(X285,uri_rdf_predicate),inference(resolution,[status(thm)],[c88, c55])).
% 3.83/4.03 fof(rdfs_subclassof_range,axiom,iext(uri_rdfs_range,uri_rdfs_subClassOf,uri_rdfs_Class),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_subclassof_range)).
% 3.83/4.03 cnf(c44,plain,iext(uri_rdfs_range,uri_rdfs_subClassOf,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_subclassof_range])).
% 3.83/4.03 cnf(c347,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X284)|icext(X284,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c88, c44])).
% 3.83/4.03 cnf(c346,plain,~iext(uri_rdfs_domain,uri_ex_name,X283)|icext(X283,uri_ex_alice),inference(resolution,[status(thm)],[c88, c15])).
% 3.83/4.03 fof(rdfs_value_domain,axiom,iext(uri_rdfs_domain,uri_rdf_value,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_value_domain)).
% 3.83/4.03 cnf(c20,plain,iext(uri_rdfs_domain,uri_rdf_value,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_value_domain])).
% 3.83/4.03 cnf(c345,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X282)|icext(X282,uri_rdf_value),inference(resolution,[status(thm)],[c88, c20])).
% 3.83/4.03 cnf(c344,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X281)|icext(X281,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c88, c108])).
% 3.83/4.03 fof(rdfs_reification_object_domain,axiom,iext(uri_rdfs_domain,uri_rdf_object,uri_rdfs_Statement),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_reification_object_domain)).
% 3.83/4.03 cnf(c58,plain,iext(uri_rdfs_domain,uri_rdf_object,uri_rdfs_Statement),inference(split_conjunct,[status(thm)],[rdfs_reification_object_domain])).
% 3.83/4.03 cnf(c343,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X280)|icext(X280,uri_rdf_object),inference(resolution,[status(thm)],[c88, c58])).
% 3.83/4.03 fof(rdfs_subclassof_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdfs_Class),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_subclassof_domain)).
% 3.83/4.03 cnf(c52,plain,iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_subclassof_domain])).
% 3.83/4.03 cnf(c342,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X279)|icext(X279,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c88, c52])).
% 3.83/4.03 fof(rdfs_subpropertyof_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdf_Property),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_subpropertyof_domain)).
% 3.83/4.03 cnf(c37,plain,iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_subpropertyof_domain])).
% 3.83/4.03 cnf(c341,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X278)|icext(X278,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c88, c37])).
% 3.83/4.03 cnf(c340,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X277)|icext(X277,uri_rdf_type),inference(resolution,[status(thm)],[c88, c21])).
% 3.83/4.03 cnf(c339,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X276)|icext(X276,uri_rdfs_domain),inference(resolution,[status(thm)],[c88, c83])).
% 3.83/4.03 fof(rdfs_subpropertyof_range,axiom,iext(uri_rdfs_range,uri_rdfs_subPropertyOf,uri_rdf_Property),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_subpropertyof_range)).
% 3.83/4.03 cnf(c29,plain,iext(uri_rdfs_range,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_subpropertyof_range])).
% 3.83/4.03 cnf(c338,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X275)|icext(X275,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c88, c29])).
% 3.83/4.03 fof(rdfs_container_member_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_member,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_member_domain)).
% 3.83/4.03 cnf(c107,plain,iext(uri_rdfs_domain,uri_rdfs_member,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_member_domain])).
% 3.83/4.03 cnf(c336,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X273)|icext(X273,uri_rdfs_member),inference(resolution,[status(thm)],[c88, c107])).
% 3.83/4.03 fof(rdfs_type_domain,axiom,iext(uri_rdfs_domain,uri_rdf_type,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_type_domain)).
% 3.83/4.03 cnf(c22,plain,iext(uri_rdfs_domain,uri_rdf_type,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_type_domain])).
% 3.83/4.03 cnf(c335,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X272)|icext(X272,uri_rdf_type),inference(resolution,[status(thm)],[c88, c22])).
% 3.83/4.03 fof(rdfs_value_range,axiom,iext(uri_rdfs_range,uri_rdf_value,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_value_range)).
% 3.83/4.03 cnf(c19,plain,iext(uri_rdfs_range,uri_rdf_value,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_value_range])).
% 3.83/4.03 cnf(c334,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X271)|icext(X271,uri_rdf_value),inference(resolution,[status(thm)],[c88, c19])).
% 3.83/4.03 fof(rdfs_container_n_domain_002,axiom,iext(uri_rdfs_domain,uri_rdf__2,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_domain_002)).
% 3.83/4.03 cnf(c104,plain,iext(uri_rdfs_domain,uri_rdf__2,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_002])).
% 3.83/4.03 cnf(c333,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X270)|icext(X270,uri_rdf__2),inference(resolution,[status(thm)],[c88, c104])).
% 3.83/4.03 cnf(c332,plain,~iext(uri_rdfs_domain,uri_owl_hasValue,X269)|icext(X269,skolem0004),inference(resolution,[status(thm)],[c88, c13])).
% 3.83/4.03 fof(rdfs_container_member_range,axiom,iext(uri_rdfs_range,uri_rdfs_member,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_member_range)).
% 3.83/4.03 cnf(c106,plain,iext(uri_rdfs_range,uri_rdfs_member,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_member_range])).
% 3.83/4.03 cnf(c330,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X267)|icext(X267,uri_rdfs_member),inference(resolution,[status(thm)],[c88, c106])).
% 3.83/4.03 cnf(c329,plain,~iext(uri_rdfs_domain,uri_owl_onProperty,X266)|icext(X266,skolem0004),inference(resolution,[status(thm)],[c88, c12])).
% 3.83/4.03 fof(rdfs_collection_first_range,axiom,iext(uri_rdfs_range,uri_rdf_first,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_collection_first_range)).
% 3.83/4.03 cnf(c116,plain,iext(uri_rdfs_range,uri_rdf_first,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_collection_first_range])).
% 3.83/4.03 cnf(c328,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X265)|icext(X265,uri_rdf_first),inference(resolution,[status(thm)],[c88, c116])).
% 3.83/4.03 cnf(c10,plain,iext(uri_rdf_rest,skolem0003,uri_rdf_nil),inference(split_conjunct,[status(thm)],[c2])).
% 3.83/4.03 cnf(c327,plain,~iext(uri_rdfs_domain,uri_rdf_rest,X264)|icext(X264,skolem0003),inference(resolution,[status(thm)],[c88, c10])).
% 3.83/4.03 cnf(c325,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X260)|icext(X260,uri_rdf_subject),inference(resolution,[status(thm)],[c88, c54])).
% 3.83/4.03 cnf(c324,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X259)|icext(X259,uri_rdf_first),inference(resolution,[status(thm)],[c88, c117])).
% 3.83/4.03 cnf(c323,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X258)|icext(X258,uri_rdf__3),inference(resolution,[status(thm)],[c88, c103])).
% 3.83/4.03 cnf(c322,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X257)|icext(X257,uri_rdfs_domain),inference(factor,[status(thm)],[c88])).
% 3.83/4.03 cnf(c314,plain,~iext(uri_rdfs_range,uri_rdf_first,X251)|icext(X251,skolem0004),inference(resolution,[status(thm)],[c62, c9])).
% 3.83/4.03 cnf(c312,plain,~iext(uri_rdfs_range,uri_rdf_first,X249)|icext(X249,uri_owl_FunctionalProperty),inference(resolution,[status(thm)],[c62, c7])).
% 3.83/4.03 cnf(c308,plain,~iext(uri_rdfs_range,uri_rdf_type,X245)|icext(X245,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c62, c97])).
% 3.83/4.03 cnf(c305,plain,~iext(uri_rdfs_range,uri_rdf_first,X242)|icext(X242,uri_owl_DatatypeProperty),inference(resolution,[status(thm)],[c62, c5])).
% 3.83/4.03 cnf(c445,plain,~iext(uri_rdfs_domain,uri_rdf_type,X238)|icext(X238,X239),inference(resolution,[status(thm)],[c428, c88])).
% 3.83/4.03 cnf(c303,plain,~iext(uri_rdfs_range,uri_owl_intersectionOf,X233)|icext(X233,skolem0001),inference(resolution,[status(thm)],[c62, c4])).
% 3.83/4.03 fof(rdfs_property_type,axiom,iext(uri_rdf_type,uri_rdf_Property,uri_rdfs_Class),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_property_type)).
% 3.83/4.03 cnf(c64,plain,iext(uri_rdf_type,uri_rdf_Property,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_property_type])).
% 3.83/4.03 cnf(c302,plain,~iext(uri_rdfs_range,uri_rdf_type,X228)|icext(X228,uri_rdfs_Class),inference(resolution,[status(thm)],[c62, c64])).
% 3.83/4.03 cnf(c301,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X224)|icext(X224,uri_rdfs_Literal),inference(resolution,[status(thm)],[c62, c95])).
% 3.83/4.03 cnf(c300,plain,~iext(uri_rdfs_range,uri_rdfs_range,X219)|icext(X219,uri_rdf_List),inference(resolution,[status(thm)],[c62, c114])).
% 3.83/4.03 fof(rdfs_dat_xmlliteral_type,axiom,iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Datatype),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_dat_xmlliteral_type)).
% 3.83/4.03 cnf(c94,plain,iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Datatype),inference(split_conjunct,[status(thm)],[rdfs_dat_xmlliteral_type])).
% 3.83/4.03 cnf(c298,plain,~iext(uri_rdfs_range,uri_rdf_type,X208)|icext(X208,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c62, c94])).
% 3.83/4.03 cnf(c294,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X199)|icext(X199,uri_rdfs_Container),inference(resolution,[status(thm)],[c62, c113])).
% 3.83/4.03 cnf(c293,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X198)|icext(X198,uri_rdfs_Class),inference(resolution,[status(thm)],[c62, c90])).
% 3.83/4.03 cnf(c290,plain,~iext(uri_rdfs_range,uri_ex_name,X195)|icext(X195,literal_plain(dat_str_alice)),inference(resolution,[status(thm)],[c62, c15])).
% 3.83/4.03 cnf(c288,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X193)|icext(X193,uri_rdf_Property),inference(resolution,[status(thm)],[c62, c108])).
% 3.83/4.03 cnf(c286,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X191)|icext(X191,uri_rdfs_Class),inference(resolution,[status(thm)],[c62, c52])).
% 3.83/4.03 cnf(c285,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X190)|icext(X190,uri_rdf_Property),inference(resolution,[status(thm)],[c62, c37])).
% 3.83/4.03 cnf(c283,plain,~iext(uri_rdfs_range,uri_rdfs_range,X188)|icext(X188,uri_rdfs_Class),inference(resolution,[status(thm)],[c62, c83])).
% 3.83/4.03 cnf(c282,plain,~iext(uri_rdfs_range,uri_rdfs_range,X187)|icext(X187,uri_rdf_Property),inference(resolution,[status(thm)],[c62, c29])).
% 3.83/4.03 cnf(c276,plain,~iext(uri_rdfs_range,uri_owl_hasValue,X181)|icext(X181,uri_foaf_Person),inference(resolution,[status(thm)],[c62, c13])).
% 3.83/4.03 cnf(c273,plain,~iext(uri_rdfs_range,uri_owl_onProperty,X178)|icext(X178,uri_rdfs_domain),inference(resolution,[status(thm)],[c62, c12])).
% 3.83/4.03 cnf(c272,plain,~iext(uri_rdfs_range,uri_rdfs_range,X177)|icext(X177,uri_rdfs_Resource),inference(resolution,[status(thm)],[c62, c116])).
% 3.83/4.03 cnf(c1169,plain,icext(uri_rdf_Property,uri_rdfs_member),inference(resolution,[status(thm)],[c813, c125])).
% 3.83/4.03 cnf(c271,plain,~iext(uri_rdfs_range,uri_rdf_rest,X176)|icext(X176,uri_rdf_nil),inference(resolution,[status(thm)],[c62, c10])).
% 3.83/4.03 cnf(c267,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X172)|icext(X172,uri_rdfs_Resource),inference(resolution,[status(thm)],[c62, c103])).
% 3.83/4.03 cnf(c1121,plain,icext(uri_rdf_Property,uri_owl_intersectionOf),inference(resolution,[status(thm)],[c625, c125])).
% 3.83/4.03 cnf(c266,plain,~iext(uri_rdfs_range,uri_rdfs_range,X171)|icext(X171,X171),inference(factor,[status(thm)],[c62])).
% 3.83/4.03 cnf(c51,plain,~iext(uri_rdfs_subClassOf,X79,X80)|~icext(X79,X78)|icext(X80,X78),inference(split_conjunct,[status(thm)],[c48])).
% 3.83/4.03 cnf(c261,plain,~icext(uri_rdfs_Seq,X170)|icext(uri_rdfs_Container,X170),inference(resolution,[status(thm)],[c51, c96])).
% 3.83/4.03 cnf(c1106,plain,icext(uri_rdf_Property,uri_ex_name),inference(resolution,[status(thm)],[c623, c125])).
% 3.83/4.03 cnf(c260,plain,~icext(uri_rdf_XMLLiteral,X169)|icext(uri_rdfs_Literal,X169),inference(resolution,[status(thm)],[c51, c95])).
% 3.83/4.03 cnf(c1091,plain,icext(uri_rdf_Property,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c621, c125])).
% 3.83/4.03 cnf(c259,plain,~icext(uri_rdf_Bag,X168)|icext(uri_rdfs_Container,X168),inference(resolution,[status(thm)],[c51, c112])).
% 3.83/4.03 cnf(c258,plain,~icext(uri_rdf_Alt,X167)|icext(uri_rdfs_Container,X167),inference(resolution,[status(thm)],[c51, c113])).
% 3.83/4.03 cnf(c1070,plain,icext(uri_rdf_Property,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c619, c125])).
% 3.83/4.03 cnf(c257,plain,~icext(uri_rdfs_Datatype,X166)|icext(uri_rdfs_Class,X166),inference(resolution,[status(thm)],[c51, c90])).
% 3.83/4.03 cnf(c256,plain,~icext(uri_rdfs_ContainerMembershipProperty,X165)|icext(uri_rdf_Property,X165),inference(resolution,[status(thm)],[c51, c108])).
% 3.83/4.03 cnf(c1051,plain,icext(uri_rdf_Property,uri_owl_hasValue),inference(resolution,[status(thm)],[c617, c125])).
% 3.83/4.03 cnf(c225,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X164)|iext(X164,uri_rdf_first,uri_rdf_List),inference(resolution,[status(thm)],[c117, c36])).
% 3.83/4.03 cnf(c224,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X163)|iext(X163,uri_rdf_first,uri_rdfs_Resource),inference(resolution,[status(thm)],[c116, c36])).
% 3.83/4.03 cnf(c1034,plain,icext(uri_rdf_Property,uri_owl_onProperty),inference(resolution,[status(thm)],[c615, c125])).
% 3.83/4.03 cnf(c223,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X162)|iext(X162,uri_rdf_rest,uri_rdf_List),inference(resolution,[status(thm)],[c115, c36])).
% 3.83/4.03 cnf(c222,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X161)|iext(X161,uri_rdf_rest,uri_rdf_List),inference(resolution,[status(thm)],[c114, c36])).
% 3.83/4.03 cnf(c1018,plain,icext(uri_rdf_Property,uri_rdfs_range),inference(resolution,[status(thm)],[c613, c125])).
% 3.83/4.03 cnf(c221,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X160)|iext(X160,uri_rdf_Alt,uri_rdfs_Container),inference(resolution,[status(thm)],[c113, c36])).
% 3.83/4.03 cnf(c991,plain,icext(uri_rdf_Property,uri_rdfs_domain),inference(resolution,[status(thm)],[c611, c125])).
% 3.83/4.03 cnf(c220,plain,~iext(uri_rdfs_subClassOf,X159,uri_rdf_Alt)|iext(uri_rdfs_subClassOf,X159,uri_rdfs_Container),inference(resolution,[status(thm)],[c113, c40])).
% 3.83/4.03 cnf(c219,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X158)|iext(X158,uri_rdf_Bag,uri_rdfs_Container),inference(resolution,[status(thm)],[c112, c36])).
% 3.83/4.03 cnf(c218,plain,~iext(uri_rdfs_subClassOf,X157,uri_rdf_Bag)|iext(uri_rdfs_subClassOf,X157,uri_rdfs_Container),inference(resolution,[status(thm)],[c112, c40])).
% 3.83/4.03 cnf(c217,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X156)|iext(X156,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),inference(resolution,[status(thm)],[c108, c36])).
% 3.83/4.03 cnf(c216,plain,~iext(uri_rdfs_subClassOf,X155,uri_rdfs_ContainerMembershipProperty)|iext(uri_rdfs_subClassOf,X155,uri_rdf_Property),inference(resolution,[status(thm)],[c108, c40])).
% 3.83/4.03 cnf(c215,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X154)|iext(X154,uri_rdfs_member,uri_rdfs_Resource),inference(resolution,[status(thm)],[c107, c36])).
% 3.83/4.03 cnf(c214,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X153)|iext(X153,uri_rdfs_member,uri_rdfs_Resource),inference(resolution,[status(thm)],[c106, c36])).
% 3.83/4.03 cnf(c213,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X152)|iext(X152,uri_rdf__1,uri_rdfs_Resource),inference(resolution,[status(thm)],[c105, c36])).
% 3.83/4.03 cnf(c212,plain,~iext(uri_rdfs_subClassOf,X151,uri_rdfs_Seq)|iext(uri_rdfs_subClassOf,X151,uri_rdfs_Container),inference(resolution,[status(thm)],[c40, c96])).
% 3.83/4.03 cnf(c211,plain,~iext(uri_rdfs_subClassOf,X150,uri_rdf_XMLLiteral)|iext(uri_rdfs_subClassOf,X150,uri_rdfs_Literal),inference(resolution,[status(thm)],[c40, c95])).
% 3.83/4.03 cnf(c904,plain,icext(uri_rdf_Property,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c480, c125])).
% 3.83/4.03 cnf(c210,plain,~iext(uri_rdfs_subClassOf,X149,uri_rdfs_Datatype)|iext(uri_rdfs_subClassOf,X149,uri_rdfs_Class),inference(resolution,[status(thm)],[c40, c90])).
% 3.83/4.03 cnf(c897,plain,icext(uri_rdf_Property,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c479, c125])).
% 3.83/4.03 cnf(c208,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X147)|iext(X147,uri_rdf__2,uri_rdfs_Resource),inference(resolution,[status(thm)],[c104, c36])).
% 3.83/4.03 cnf(c207,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X146)|iext(X146,uri_rdf__3,uri_rdfs_Resource),inference(resolution,[status(thm)],[c103, c36])).
% 3.83/4.03 cnf(c206,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X145)|iext(X145,uri_rdf__1,uri_rdfs_Resource),inference(resolution,[status(thm)],[c102, c36])).
% 3.83/4.03 cnf(c205,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X144)|iext(X144,uri_rdf__2,uri_rdfs_Resource),inference(resolution,[status(thm)],[c101, c36])).
% 3.83/4.03 cnf(c204,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X143)|iext(X143,uri_rdf__3,uri_rdfs_Resource),inference(resolution,[status(thm)],[c100, c36])).
% 3.83/4.03 cnf(c203,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X142)|iext(X142,skolem0002,skolem0003),inference(resolution,[status(thm)],[c36, c8])).
% 3.83/4.03 cnf(c202,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X141)|iext(X141,uri_foaf_Person,uri_owl_Class),inference(resolution,[status(thm)],[c36, c3])).
% 3.83/4.03 cnf(c201,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X140)|iext(X140,skolem0001,skolem0002),inference(resolution,[status(thm)],[c36, c6])).
% 3.83/4.03 cnf(c200,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X139)|iext(X139,uri_rdf_subject,uri_rdfs_Resource),inference(resolution,[status(thm)],[c36, c53])).
% 3.83/4.03 cnf(c199,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X138)|iext(X138,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c36, c98])).
% 3.83/4.03 cnf(c198,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_first,X137)|iext(X137,skolem0003,skolem0004),inference(resolution,[status(thm)],[c36, c9])).
% 3.83/4.03 cnf(c197,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X136)|iext(X136,uri_rdfs_Seq,uri_rdfs_Container),inference(resolution,[status(thm)],[c36, c96])).
% 3.83/4.03 cnf(c196,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_first,X135)|iext(X135,skolem0002,uri_owl_FunctionalProperty),inference(resolution,[status(thm)],[c36, c7])).
% 3.83/4.03 cnf(c195,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X134)|iext(X134,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c36, c99])).
% 3.83/4.03 cnf(c194,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X133)|iext(X133,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c36, c97])).
% 3.83/4.03 cnf(c193,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_first,X132)|iext(X132,skolem0001,uri_owl_DatatypeProperty),inference(resolution,[status(thm)],[c36, c5])).
% 3.83/4.03 cnf(c192,plain,~iext(uri_rdfs_subPropertyOf,uri_owl_intersectionOf,X131)|iext(X131,uri_ex_PersonAttribute,skolem0001),inference(resolution,[status(thm)],[c36, c4])).
% 3.83/4.03 cnf(c191,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X130)|iext(X130,uri_rdf_Property,uri_rdfs_Class),inference(resolution,[status(thm)],[c36, c64])).
% 3.83/4.03 cnf(c190,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X129)|iext(X129,uri_rdf_XMLLiteral,uri_rdfs_Literal),inference(resolution,[status(thm)],[c36, c95])).
% 3.83/4.03 cnf(c189,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X128)|iext(X128,uri_rdf_XMLLiteral,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c36, c94])).
% 3.83/4.03 cnf(c188,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X127)|iext(X127,uri_rdfs_range,uri_rdf_Property),inference(resolution,[status(thm)],[c36, c63])).
% 3.83/4.03 cnf(c187,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X126)|iext(X126,uri_rdfs_domain,uri_rdf_Property),inference(resolution,[status(thm)],[c36, c89])).
% 3.83/4.03 cnf(c186,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X125)|iext(X125,uri_rdfs_range,uri_rdfs_Class),inference(resolution,[status(thm)],[c36, c59])).
% 3.83/4.03 cnf(c185,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X124)|iext(X124,uri_rdfs_Datatype,uri_rdfs_Class),inference(resolution,[status(thm)],[c36, c90])).
% 3.83/4.03 cnf(c184,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X123)|iext(X123,uri_rdf_predicate,uri_rdfs_Resource),inference(resolution,[status(thm)],[c36, c55])).
% 3.83/4.03 cnf(c183,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X122)|iext(X122,uri_rdfs_subClassOf,uri_rdfs_Class),inference(resolution,[status(thm)],[c36, c44])).
% 3.83/4.03 cnf(c182,plain,~iext(uri_rdfs_subPropertyOf,uri_ex_name,X121)|iext(X121,uri_ex_alice,literal_plain(dat_str_alice)),inference(resolution,[status(thm)],[c36, c15])).
% 3.83/4.03 cnf(c181,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X120)|iext(X120,uri_rdf_value,uri_rdfs_Resource),inference(resolution,[status(thm)],[c36, c20])).
% 3.83/4.03 cnf(c180,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X119)|iext(X119,uri_rdf_object,uri_rdfs_Statement),inference(resolution,[status(thm)],[c36, c58])).
% 3.83/4.03 cnf(c179,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X118)|iext(X118,uri_rdfs_subClassOf,uri_rdfs_Class),inference(resolution,[status(thm)],[c36, c52])).
% 3.83/4.03 cnf(c178,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X117)|iext(X117,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c36, c37])).
% 3.83/4.03 cnf(c177,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X116)|iext(X116,uri_rdf_type,uri_rdfs_Class),inference(resolution,[status(thm)],[c36, c21])).
% 3.83/4.03 cnf(c176,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X115)|iext(X115,uri_rdfs_domain,uri_rdfs_Class),inference(resolution,[status(thm)],[c36, c83])).
% 3.83/4.03 cnf(c175,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X114)|iext(X114,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c36, c29])).
% 3.83/4.03 cnf(c174,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X113)|iext(X113,uri_ex_name,uri_ex_PersonAttribute),inference(resolution,[status(thm)],[c36, c14])).
% 3.83/4.03 cnf(c173,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X112)|iext(X112,uri_rdf_type,uri_rdfs_Resource),inference(resolution,[status(thm)],[c36, c22])).
% 3.83/4.03 cnf(c172,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X111)|iext(X111,uri_rdf_value,uri_rdfs_Resource),inference(resolution,[status(thm)],[c36, c19])).
% 3.83/4.03 cnf(c171,plain,~iext(uri_rdfs_subPropertyOf,uri_owl_hasValue,X110)|iext(X110,skolem0004,uri_foaf_Person),inference(resolution,[status(thm)],[c36, c13])).
% 3.83/4.03 cnf(c170,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X109)|iext(X109,uri_rdf_predicate,uri_rdfs_Statement),inference(resolution,[status(thm)],[c36, c56])).
% 3.83/4.03 cnf(c169,plain,~iext(uri_rdfs_subPropertyOf,uri_owl_onProperty,X108)|iext(X108,skolem0004,uri_rdfs_domain),inference(resolution,[status(thm)],[c36, c12])).
% 3.83/4.03 cnf(c168,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X107)|iext(X107,skolem0003,uri_rdf_nil),inference(resolution,[status(thm)],[c36, c10])).
% 3.83/4.03 cnf(c167,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X106)|iext(X106,skolem0004,uri_owl_Restriction),inference(resolution,[status(thm)],[c36, c11])).
% 3.83/4.03 cnf(c166,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X105)|iext(X105,uri_rdf_subject,uri_rdfs_Statement),inference(resolution,[status(thm)],[c36, c54])).
% 3.83/4.03 cnf(c165,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X104)|iext(X104,uri_rdfs_subPropertyOf,X104),inference(factor,[status(thm)],[c36])).
% 3.83/4.03 cnf(c532,plain,icext(uri_rdf_Property,uri_rdf_first),inference(resolution,[status(thm)],[c152, c125])).
% 3.83/4.03 cnf(c526,plain,icext(uri_rdf_List,uri_rdf_nil),inference(resolution,[status(thm)],[c151, c125])).
% 3.83/4.03 cnf(c519,plain,icext(uri_rdf_Property,uri_rdf_rest),inference(resolution,[status(thm)],[c150, c125])).
% 3.83/4.03 cnf(c511,plain,icext(uri_rdf_Property,uri_rdf__1),inference(resolution,[status(thm)],[c149, c125])).
% 3.83/4.03 cnf(c503,plain,icext(uri_rdf_Property,uri_rdf__2),inference(resolution,[status(thm)],[c148, c125])).
% 3.83/4.03 cnf(c495,plain,icext(uri_rdf_Property,uri_rdf__3),inference(resolution,[status(thm)],[c147, c125])).
% 3.83/4.03 cnf(c487,plain,icext(uri_rdf_Property,uri_rdf_object),inference(resolution,[status(thm)],[c146, c125])).
% 3.83/4.03 cnf(c475,plain,icext(uri_rdf_Property,uri_rdf_value),inference(resolution,[status(thm)],[c145, c125])).
% 3.83/4.03 cnf(c468,plain,icext(uri_rdf_Property,uri_rdf_subject),inference(resolution,[status(thm)],[c144, c125])).
% 3.83/4.03 cnf(c460,plain,icext(uri_rdf_Property,uri_rdf_type),inference(resolution,[status(thm)],[c136, c125])).
% 3.83/4.03 cnf(c422,plain,icext(uri_owl_Class,uri_foaf_Person),inference(resolution,[status(thm)],[c125, c3])).
% 3.83/4.03 cnf(c417,plain,icext(uri_rdfs_Datatype,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c125, c94])).
% 3.83/4.03 cnf(c416,plain,icext(uri_ex_PersonAttribute,uri_ex_name),inference(resolution,[status(thm)],[c125, c14])).
% 3.83/4.03 cnf(c415,plain,icext(uri_owl_Restriction,skolem0004),inference(resolution,[status(thm)],[c125, c11])).
% 3.83/4.03 fof(rdfs_datatype_instsub_literal,axiom,(![D]:(icext(uri_rdfs_Datatype,D)=>iext(uri_rdfs_subClassOf,D,uri_rdfs_Literal))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_datatype_instsub_literal)).
% 3.83/4.03 fof(c91,plain,(![D]:(~icext(uri_rdfs_Datatype,D)|iext(uri_rdfs_subClassOf,D,uri_rdfs_Literal))),inference(fof_nnf,[status(thm)],[rdfs_datatype_instsub_literal])).
% 3.83/4.03 fof(c92,plain,(![X35]:(~icext(uri_rdfs_Datatype,X35)|iext(uri_rdfs_subClassOf,X35,uri_rdfs_Literal))),inference(variable_rename,[status(thm)],[c91])).
% 3.83/4.03 cnf(c93,plain,~icext(uri_rdfs_Datatype,X89)|iext(uri_rdfs_subClassOf,X89,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[c92])).
% 3.83/4.03 cnf(c250,plain,icext(uri_rdfs_Class,uri_rdf_Property),inference(resolution,[status(thm)],[c242, c81])).
% 3.83/4.03 fof(rdfs_lv_def,axiom,(![X]:(lv(X)<=>icext(uri_rdfs_Literal,X))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_lv_def)).
% 3.83/4.03 fof(c65,plain,(![X]:((~lv(X)|icext(uri_rdfs_Literal,X))&(~icext(uri_rdfs_Literal,X)|lv(X)))),inference(fof_nnf,[status(thm)],[rdfs_lv_def])).
% 3.83/4.03 fof(c66,plain,((![X]:(~lv(X)|icext(uri_rdfs_Literal,X)))&(![X]:(~icext(uri_rdfs_Literal,X)|lv(X)))),inference(shift_quantors,[status(thm)],[c65])).
% 3.83/4.03 fof(c68,plain,(![X25]:(![X26]:((~lv(X25)|icext(uri_rdfs_Literal,X25))&(~icext(uri_rdfs_Literal,X26)|lv(X26))))),inference(shift_quantors,[status(thm)],[fof(c67,plain,((![X25]:(~lv(X25)|icext(uri_rdfs_Literal,X25)))&(![X26]:(~icext(uri_rdfs_Literal,X26)|lv(X26)))),inference(variable_rename,[status(thm)],[c66])).])).
% 3.83/4.03 cnf(c70,plain,~icext(uri_rdfs_Literal,X56)|lv(X56),inference(split_conjunct,[status(thm)],[c68])).
% 3.83/4.03 cnf(c69,plain,~lv(X54)|icext(uri_rdfs_Literal,X54),inference(split_conjunct,[status(thm)],[c68])).
% 3.83/4.03 fof(testcase_conclusion_fullish_012_Template_Class,conjecture,(iext(uri_rdf_type,uri_ex_name,uri_owl_FunctionalProperty)&iext(uri_rdf_type,uri_ex_alice,uri_foaf_Person)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', testcase_conclusion_fullish_012_Template_Class)).
% 3.83/4.03 fof(c16,negated_conjecture,(~(iext(uri_rdf_type,uri_ex_name,uri_owl_FunctionalProperty)&iext(uri_rdf_type,uri_ex_alice,uri_foaf_Person))),inference(assume_negation,[status(cth)],[testcase_conclusion_fullish_012_Template_Class])).
% 3.83/4.03 fof(c17,negated_conjecture,(~iext(uri_rdf_type,uri_ex_name,uri_owl_FunctionalProperty)|~iext(uri_rdf_type,uri_ex_alice,uri_foaf_Person)),inference(fof_nnf,[status(thm)],[c16])).
% 3.83/4.03 cnf(c18,negated_conjecture,~iext(uri_rdf_type,uri_ex_name,uri_owl_FunctionalProperty)|~iext(uri_rdf_type,uri_ex_alice,uri_foaf_Person),inference(split_conjunct,[status(thm)],[c17])).
% 3.83/4.03 % SZS output end Saturation
% 3.83/4.03
% 3.83/4.03 % Initial clauses : 103
% 3.83/4.03 % Processed clauses : 629
% 3.83/4.03 % Factors computed : 5
% 3.83/4.03 % Resolvents computed: 1463
% 3.83/4.03 % Tautologies deleted: 57
% 3.83/4.03 % Forward subsumed : 885
% 3.83/4.03 % Backward subsumed : 1
% 3.83/4.03 % -------- CPU Time ---------
% 3.83/4.03 % User time : 3.666 s
% 3.83/4.03 % System time : 0.012 s
% 3.83/4.03 % Total time : 3.678 s
%------------------------------------------------------------------------------