PyRes---1.5.CSA-Sat.s

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

% Computer : n015.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:53 EDT 2024

% Result   : CounterSatisfiable 3.93s 4.10s
% Output   : Saturation 3.93s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12  % Problem  : SWB022+4 : TPTP v8.1.2. Released v5.2.0.
% 0.11/0.13  % Command  : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34  % Computer : n015.cluster.edu
% 0.13/0.34  % Model    : x86_64 x86_64
% 0.13/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34  % Memory   : 8042.1875MB
% 0.13/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34  % CPULimit : 300
% 0.13/0.34  % WCLimit  : 300
% 0.13/0.34  % DateTime : Wed May  8 22:01:23 EDT 2024
% 0.13/0.34  % CPUTime  : 
% 3.93/4.10  % Version:  1.5
% 3.93/4.10  % SZS status CounterSatisfiable
% 3.93/4.10  % SZS output start Saturation
% 3.93/4.10  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.93/4.10  fof(c35,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.93/4.10  fof(c37,plain,(![X14]:(![X15]:(![X16]:(![X17]:(~iext(uri_rdfs_subPropertyOf,X14,X15)|((ip(X14)&ip(X15))&(~iext(X14,X16,X17)|iext(X15,X16,X17)))))))),inference(shift_quantors,[status(thm)],[fof(c36,plain,(![X14]:(![X15]:(~iext(uri_rdfs_subPropertyOf,X14,X15)|((ip(X14)&ip(X15))&(![X16]:(![X17]:(~iext(X14,X16,X17)|iext(X15,X16,X17)))))))),inference(variable_rename,[status(thm)],[c35])).])).
% 3.93/4.10  fof(c38,plain,(![X14]:(![X15]:(![X16]:(![X17]:(((~iext(uri_rdfs_subPropertyOf,X14,X15)|ip(X14))&(~iext(uri_rdfs_subPropertyOf,X14,X15)|ip(X15)))&(~iext(uri_rdfs_subPropertyOf,X14,X15)|(~iext(X14,X16,X17)|iext(X15,X16,X17)))))))),inference(distribute,[status(thm)],[c37])).
% 3.93/4.10  cnf(c41,plain,~iext(uri_rdfs_subPropertyOf,X72,X70)|~iext(X72,X73,X71)|iext(X70,X73,X71),inference(split_conjunct,[status(thm)],[c38])).
% 3.93/4.10  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.93/4.10  fof(c31,plain,(![P]:(~ip(P)|iext(uri_rdfs_subPropertyOf,P,P))),inference(fof_nnf,[status(thm)],[rdfs_subpropertyof_reflex])).
% 3.93/4.10  fof(c32,plain,(![X13]:(~ip(X13)|iext(uri_rdfs_subPropertyOf,X13,X13))),inference(variable_rename,[status(thm)],[c31])).
% 3.93/4.10  cnf(c33,plain,~ip(X58)|iext(uri_rdfs_subPropertyOf,X58,X58),inference(split_conjunct,[status(thm)],[c32])).
% 3.93/4.10  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.93/4.10  fof(c143,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.93/4.10  fof(c144,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)],[c143])).
% 3.93/4.10  fof(c146,plain,(![X46]:(![X47]:((~iext(uri_rdf_type,X46,uri_rdf_Property)|ip(X46))&(~ip(X47)|iext(uri_rdf_type,X47,uri_rdf_Property))))),inference(shift_quantors,[status(thm)],[fof(c145,plain,((![X46]:(~iext(uri_rdf_type,X46,uri_rdf_Property)|ip(X46)))&(![X47]:(~ip(X47)|iext(uri_rdf_type,X47,uri_rdf_Property)))),inference(variable_rename,[status(thm)],[c144])).])).
% 3.93/4.10  cnf(c147,plain,~iext(uri_rdf_type,X102,uri_rdf_Property)|ip(X102),inference(split_conjunct,[status(thm)],[c146])).
% 3.93/4.10  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.93/4.10  fof(c126,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.93/4.10  fof(c127,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)],[c126])).
% 3.93/4.10  fof(c129,plain,(![X42]:(![X43]:(![X44]:(![X45]:((~iext(uri_rdf_type,X42,X43)|icext(X43,X42))&(~icext(X45,X44)|iext(uri_rdf_type,X44,X45))))))),inference(shift_quantors,[status(thm)],[fof(c128,plain,((![X42]:(![X43]:(~iext(uri_rdf_type,X42,X43)|icext(X43,X42))))&(![X44]:(![X45]:(~icext(X45,X44)|iext(uri_rdf_type,X44,X45))))),inference(variable_rename,[status(thm)],[c127])).])).
% 3.93/4.10  cnf(c131,plain,~icext(X98,X99)|iext(uri_rdf_type,X99,X98),inference(split_conjunct,[status(thm)],[c129])).
% 3.93/4.10  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.93/4.10  cnf(c68,plain,iext(uri_rdfs_domain,uri_rdfs_range,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_range_domain])).
% 3.93/4.10  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.93/4.10  fof(c89,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.93/4.10  fof(c90,plain,(![P]:(![C]:(![X]:((~iext(uri_rdfs_domain,P,C)|(![Y]:~iext(P,X,Y)))|icext(C,X))))),inference(shift_quantors,[status(thm)],[c89])).
% 3.93/4.10  fof(c92,plain,(![X35]:(![X36]:(![X37]:(![X38]:((~iext(uri_rdfs_domain,X35,X36)|~iext(X35,X37,X38))|icext(X36,X37)))))),inference(shift_quantors,[status(thm)],[fof(c91,plain,(![X35]:(![X36]:(![X37]:((~iext(uri_rdfs_domain,X35,X36)|(![X38]:~iext(X35,X37,X38)))|icext(X36,X37))))),inference(variable_rename,[status(thm)],[c90])).])).
% 3.93/4.10  cnf(c93,plain,~iext(uri_rdfs_domain,X91,X90)|~iext(X91,X92,X89)|icext(X90,X92),inference(split_conjunct,[status(thm)],[c92])).
% 3.93/4.10  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.93/4.10  cnf(c139,plain,iext(uri_rdfs_range,uri_rdfs_comment,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[rdfs_annotation_comment_range])).
% 3.93/4.10  cnf(c476,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X356)|icext(X356,uri_rdfs_comment),inference(resolution,[status(thm)],[c139, c93])).
% 3.93/4.10  cnf(c1427,plain,icext(uri_rdf_Property,uri_rdfs_comment),inference(resolution,[status(thm)],[c476, c68])).
% 3.93/4.10  cnf(c1428,plain,iext(uri_rdf_type,uri_rdfs_comment,uri_rdf_Property),inference(resolution,[status(thm)],[c1427, c131])).
% 3.93/4.10  cnf(c1432,plain,ip(uri_rdfs_comment),inference(resolution,[status(thm)],[c1428, c147])).
% 3.93/4.10  cnf(c1436,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_comment,uri_rdfs_comment),inference(resolution,[status(thm)],[c1432, c33])).
% 3.93/4.10  cnf(c1441,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X702)|iext(X702,uri_rdfs_comment,uri_rdfs_comment),inference(resolution,[status(thm)],[c1436, c41])).
% 3.93/4.10  cnf(c1431,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X701)|iext(X701,uri_rdfs_comment,uri_rdf_Property),inference(resolution,[status(thm)],[c1428, c41])).
% 3.93/4.10  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.93/4.10  cnf(c134,plain,iext(uri_rdfs_range,uri_rdfs_label,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[rdfs_annotation_label_range])).
% 3.93/4.10  cnf(c426,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X337)|icext(X337,uri_rdfs_label),inference(resolution,[status(thm)],[c134, c93])).
% 3.93/4.10  cnf(c1397,plain,icext(uri_rdf_Property,uri_rdfs_label),inference(resolution,[status(thm)],[c426, c68])).
% 3.93/4.10  cnf(c1398,plain,iext(uri_rdf_type,uri_rdfs_label,uri_rdf_Property),inference(resolution,[status(thm)],[c1397, c131])).
% 3.93/4.10  cnf(c1403,plain,ip(uri_rdfs_label),inference(resolution,[status(thm)],[c1398, c147])).
% 3.93/4.10  cnf(c1406,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_label,uri_rdfs_label),inference(resolution,[status(thm)],[c1403, c33])).
% 3.93/4.10  cnf(c1412,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X699)|iext(X699,uri_rdfs_label,uri_rdfs_label),inference(resolution,[status(thm)],[c1406, c41])).
% 3.93/4.10  cnf(c1402,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X698)|iext(X698,uri_rdfs_label,uri_rdf_Property),inference(resolution,[status(thm)],[c1398, c41])).
% 3.93/4.10  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.93/4.10  fof(c46,plain,(![C]:(~ic(C)|iext(uri_rdfs_subClassOf,C,C))),inference(fof_nnf,[status(thm)],[rdfs_subclassof_reflex])).
% 3.93/4.10  fof(c47,plain,(![X21]:(~ic(X21)|iext(uri_rdfs_subClassOf,X21,X21))),inference(variable_rename,[status(thm)],[c46])).
% 3.93/4.10  cnf(c48,plain,~ic(X77)|iext(uri_rdfs_subClassOf,X77,X77),inference(split_conjunct,[status(thm)],[c47])).
% 3.93/4.10  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.93/4.10  fof(c82,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.93/4.10  fof(c83,plain,((![X]:(~ic(X)|icext(uri_rdfs_Class,X)))&(![X]:(~icext(uri_rdfs_Class,X)|ic(X)))),inference(shift_quantors,[status(thm)],[c82])).
% 3.93/4.10  fof(c85,plain,(![X33]:(![X34]:((~ic(X33)|icext(uri_rdfs_Class,X33))&(~icext(uri_rdfs_Class,X34)|ic(X34))))),inference(shift_quantors,[status(thm)],[fof(c84,plain,((![X33]:(~ic(X33)|icext(uri_rdfs_Class,X33)))&(![X34]:(~icext(uri_rdfs_Class,X34)|ic(X34)))),inference(variable_rename,[status(thm)],[c83])).])).
% 3.93/4.10  cnf(c87,plain,~icext(uri_rdfs_Class,X69)|ic(X69),inference(split_conjunct,[status(thm)],[c85])).
% 3.93/4.10  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.93/4.10  cnf(c64,plain,iext(uri_rdfs_range,uri_rdfs_range,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_range_range])).
% 3.93/4.10  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.93/4.10  fof(c65,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.93/4.10  fof(c66,plain,(![X25]:(![X26]:(![X27]:(![X28]:((~iext(uri_rdfs_range,X25,X26)|~iext(X25,X27,X28))|icext(X26,X28)))))),inference(variable_rename,[status(thm)],[c65])).
% 3.93/4.10  cnf(c67,plain,~iext(uri_rdfs_range,X87,X86)|~iext(X87,X85,X88)|icext(X86,X88),inference(split_conjunct,[status(thm)],[c66])).
% 3.93/4.10  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.93/4.10  cnf(c119,plain,iext(uri_rdfs_range,uri_rdf_rest,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdfs_collection_rest_range])).
% 3.93/4.10  cnf(c400,plain,~iext(uri_rdfs_range,uri_rdfs_range,X317)|icext(X317,uri_rdf_List),inference(resolution,[status(thm)],[c119, c67])).
% 3.93/4.10  cnf(c1357,plain,icext(uri_rdfs_Class,uri_rdf_List),inference(resolution,[status(thm)],[c400, c64])).
% 3.93/4.10  cnf(c1359,plain,ic(uri_rdf_List),inference(resolution,[status(thm)],[c1357, c87])).
% 3.93/4.10  cnf(c1363,plain,iext(uri_rdfs_subClassOf,uri_rdf_List,uri_rdf_List),inference(resolution,[status(thm)],[c1359, c48])).
% 3.93/4.10  cnf(c1383,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X696)|iext(X696,uri_rdf_List,uri_rdf_List),inference(resolution,[status(thm)],[c1363, c41])).
% 3.93/4.10  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.93/4.10  fof(c43,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.93/4.10  fof(c44,plain,(![X18]:(![X19]:(![X20]:((~iext(uri_rdfs_subClassOf,X18,X19)|~iext(uri_rdfs_subClassOf,X19,X20))|iext(uri_rdfs_subClassOf,X18,X20))))),inference(variable_rename,[status(thm)],[c43])).
% 3.93/4.10  cnf(c45,plain,~iext(uri_rdfs_subClassOf,X74,X75)|~iext(uri_rdfs_subClassOf,X75,X76)|iext(uri_rdfs_subClassOf,X74,X76),inference(split_conjunct,[status(thm)],[c44])).
% 3.93/4.10  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.93/4.10  fof(c123,plain,(![C]:(~ic(C)|iext(uri_rdfs_subClassOf,C,uri_rdfs_Resource))),inference(fof_nnf,[status(thm)],[rdfs_class_instsub_resource])).
% 3.93/4.10  fof(c124,plain,(![X41]:(~ic(X41)|iext(uri_rdfs_subClassOf,X41,uri_rdfs_Resource))),inference(variable_rename,[status(thm)],[c123])).
% 3.93/4.10  cnf(c125,plain,~ic(X95)|iext(uri_rdfs_subClassOf,X95,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[c124])).
% 3.93/4.10  cnf(c1361,plain,iext(uri_rdfs_subClassOf,uri_rdf_List,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1359, c125])).
% 3.93/4.10  cnf(c1376,plain,~iext(uri_rdfs_subClassOf,X695,uri_rdf_List)|iext(uri_rdfs_subClassOf,X695,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1361, c45])).
% 3.93/4.10  cnf(c1374,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X694)|iext(X694,uri_rdf_List,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1361, c41])).
% 3.93/4.10  cnf(c1360,plain,iext(uri_rdf_type,uri_rdf_List,uri_rdfs_Class),inference(resolution,[status(thm)],[c1357, c131])).
% 3.93/4.10  cnf(c1366,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X693)|iext(X693,uri_rdf_List,uri_rdfs_Class),inference(resolution,[status(thm)],[c1360, c41])).
% 3.93/4.10  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.93/4.10  cnf(c122,plain,iext(uri_rdfs_domain,uri_rdf_first,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdfs_collection_first_domain])).
% 3.93/4.10  fof(testcase_premise_fullish_022_List_Member_Access,axiom,(?[BNODE_pL]:(?[BNODE_l11]:(?[BNODE_l12]:(?[BNODE_l21]:(?[BNODE_l22]:(?[BNODE_l31]:(?[BNODE_l32]:(?[BNODE_l33]:((((((((((((((((((iext(uri_rdfs_subPropertyOf,uri_skos_memberList,BNODE_pL)&iext(uri_owl_propertyChainAxiom,uri_skos_member,BNODE_l11))&iext(uri_rdf_first,BNODE_l11,BNODE_pL))&iext(uri_rdf_rest,BNODE_l11,BNODE_l12))&iext(uri_rdf_first,BNODE_l12,uri_rdf_first))&iext(uri_rdf_rest,BNODE_l12,uri_rdf_nil))&iext(uri_owl_propertyChainAxiom,BNODE_pL,BNODE_l21))&iext(uri_rdf_first,BNODE_l21,BNODE_pL))&iext(uri_rdf_rest,BNODE_l21,BNODE_l22))&iext(uri_rdf_first,BNODE_l22,uri_rdf_rest))&iext(uri_rdf_rest,BNODE_l22,uri_rdf_nil))&iext(uri_rdf_type,uri_ex_MyOrderedCollection,uri_skos_OrderedCollection))&iext(uri_skos_memberList,uri_ex_MyOrderedCollection,BNODE_l31))&iext(uri_rdf_first,BNODE_l31,uri_ex_X))&iext(uri_rdf_rest,BNODE_l31,BNODE_l32))&iext(uri_rdf_first,BNODE_l32,uri_ex_Y))&iext(uri_rdf_rest,BNODE_l32,BNODE_l33))&iext(uri_rdf_first,BNODE_l33,uri_ex_Z))&iext(uri_rdf_rest,BNODE_l33,uri_rdf_nil)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', testcase_premise_fullish_022_List_Member_Access)).
% 3.93/4.10  fof(c0,plain,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:(?[X9]:((((((((((((((((((iext(uri_rdfs_subPropertyOf,uri_skos_memberList,X2)&iext(uri_owl_propertyChainAxiom,uri_skos_member,X3))&iext(uri_rdf_first,X3,X2))&iext(uri_rdf_rest,X3,X4))&iext(uri_rdf_first,X4,uri_rdf_first))&iext(uri_rdf_rest,X4,uri_rdf_nil))&iext(uri_owl_propertyChainAxiom,X2,X5))&iext(uri_rdf_first,X5,X2))&iext(uri_rdf_rest,X5,X6))&iext(uri_rdf_first,X6,uri_rdf_rest))&iext(uri_rdf_rest,X6,uri_rdf_nil))&iext(uri_rdf_type,uri_ex_MyOrderedCollection,uri_skos_OrderedCollection))&iext(uri_skos_memberList,uri_ex_MyOrderedCollection,X7))&iext(uri_rdf_first,X7,uri_ex_X))&iext(uri_rdf_rest,X7,X8))&iext(uri_rdf_first,X8,uri_ex_Y))&iext(uri_rdf_rest,X8,X9))&iext(uri_rdf_first,X9,uri_ex_Z))&iext(uri_rdf_rest,X9,uri_rdf_nil)))))))))),inference(variable_rename,[status(thm)],[testcase_premise_fullish_022_List_Member_Access])).
% 3.93/4.10  fof(c1,plain,((((((((((((((((((iext(uri_rdfs_subPropertyOf,uri_skos_memberList,skolem0001)&iext(uri_owl_propertyChainAxiom,uri_skos_member,skolem0002))&iext(uri_rdf_first,skolem0002,skolem0001))&iext(uri_rdf_rest,skolem0002,skolem0003))&iext(uri_rdf_first,skolem0003,uri_rdf_first))&iext(uri_rdf_rest,skolem0003,uri_rdf_nil))&iext(uri_owl_propertyChainAxiom,skolem0001,skolem0004))&iext(uri_rdf_first,skolem0004,skolem0001))&iext(uri_rdf_rest,skolem0004,skolem0005))&iext(uri_rdf_first,skolem0005,uri_rdf_rest))&iext(uri_rdf_rest,skolem0005,uri_rdf_nil))&iext(uri_rdf_type,uri_ex_MyOrderedCollection,uri_skos_OrderedCollection))&iext(uri_skos_memberList,uri_ex_MyOrderedCollection,skolem0006))&iext(uri_rdf_first,skolem0006,uri_ex_X))&iext(uri_rdf_rest,skolem0006,skolem0007))&iext(uri_rdf_first,skolem0007,uri_ex_Y))&iext(uri_rdf_rest,skolem0007,skolem0008))&iext(uri_rdf_first,skolem0008,uri_ex_Z))&iext(uri_rdf_rest,skolem0008,uri_rdf_nil)),inference(skolemize,[status(esa)],[c0])).
% 3.93/4.10  cnf(c15,plain,iext(uri_rdf_first,skolem0006,uri_ex_X),inference(split_conjunct,[status(thm)],[c1])).
% 3.93/4.10  cnf(c353,plain,~iext(uri_rdfs_domain,uri_rdf_first,X291)|icext(X291,skolem0006),inference(resolution,[status(thm)],[c93, c15])).
% 3.93/4.10  cnf(c1327,plain,icext(uri_rdf_List,skolem0006),inference(resolution,[status(thm)],[c353, c122])).
% 3.93/4.10  cnf(c1328,plain,iext(uri_rdf_type,skolem0006,uri_rdf_List),inference(resolution,[status(thm)],[c1327, c131])).
% 3.93/4.11  cnf(c1331,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X692)|iext(X692,skolem0006,uri_rdf_List),inference(resolution,[status(thm)],[c1328, c41])).
% 3.93/4.11  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.93/4.11  cnf(c94,plain,iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_domain_domain])).
% 3.93/4.11  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.93/4.11  cnf(c61,plain,iext(uri_rdfs_domain,uri_rdf_predicate,uri_rdfs_Statement),inference(split_conjunct,[status(thm)],[rdfs_reification_predicate_domain])).
% 3.93/4.11  cnf(c342,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X280)|icext(X280,uri_rdf_predicate),inference(resolution,[status(thm)],[c93, c61])).
% 3.93/4.11  cnf(c1305,plain,icext(uri_rdf_Property,uri_rdf_predicate),inference(resolution,[status(thm)],[c342, c94])).
% 3.93/4.11  cnf(c1306,plain,iext(uri_rdf_type,uri_rdf_predicate,uri_rdf_Property),inference(resolution,[status(thm)],[c1305, c131])).
% 3.93/4.11  cnf(c1310,plain,ip(uri_rdf_predicate),inference(resolution,[status(thm)],[c1306, c147])).
% 3.93/4.11  cnf(c1313,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_predicate,uri_rdf_predicate),inference(resolution,[status(thm)],[c1310, c33])).
% 3.93/4.11  cnf(c1318,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X690)|iext(X690,uri_rdf_predicate,uri_rdf_predicate),inference(resolution,[status(thm)],[c1313, c41])).
% 3.93/4.11  cnf(c1309,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X689)|iext(X689,uri_rdf_predicate,uri_rdf_Property),inference(resolution,[status(thm)],[c1306, c41])).
% 3.93/4.11  cnf(c9,plain,iext(uri_rdf_first,skolem0004,skolem0001),inference(split_conjunct,[status(thm)],[c1])).
% 3.93/4.11  cnf(c331,plain,~iext(uri_rdfs_domain,uri_rdf_first,X269)|icext(X269,skolem0004),inference(resolution,[status(thm)],[c93, c9])).
% 3.93/4.11  cnf(c1289,plain,icext(uri_rdf_List,skolem0004),inference(resolution,[status(thm)],[c331, c122])).
% 3.93/4.11  cnf(c1290,plain,iext(uri_rdf_type,skolem0004,uri_rdf_List),inference(resolution,[status(thm)],[c1289, c131])).
% 3.93/4.11  cnf(c1294,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X688)|iext(X688,skolem0004,uri_rdf_List),inference(resolution,[status(thm)],[c1290, c41])).
% 3.93/4.11  cnf(c4,plain,iext(uri_rdf_first,skolem0002,skolem0001),inference(split_conjunct,[status(thm)],[c1])).
% 3.93/4.11  cnf(c325,plain,~iext(uri_rdfs_domain,uri_rdf_first,X263)|icext(X263,skolem0002),inference(resolution,[status(thm)],[c93, c4])).
% 3.93/4.11  cnf(c1278,plain,icext(uri_rdf_List,skolem0002),inference(resolution,[status(thm)],[c325, c122])).
% 3.93/4.11  cnf(c1279,plain,iext(uri_rdf_type,skolem0002,uri_rdf_List),inference(resolution,[status(thm)],[c1278, c131])).
% 3.93/4.11  cnf(c1282,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X687)|iext(X687,skolem0002,uri_rdf_List),inference(resolution,[status(thm)],[c1279, c41])).
% 3.93/4.11  cnf(c18,plain,iext(uri_rdf_rest,skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c1])).
% 3.93/4.11  cnf(c296,plain,~iext(uri_rdfs_range,uri_rdf_rest,X238)|icext(X238,skolem0008),inference(resolution,[status(thm)],[c67, c18])).
% 3.93/4.11  cnf(c1254,plain,icext(uri_rdf_List,skolem0008),inference(resolution,[status(thm)],[c296, c119])).
% 3.93/4.11  cnf(c1255,plain,iext(uri_rdf_type,skolem0008,uri_rdf_List),inference(resolution,[status(thm)],[c1254, c131])).
% 3.93/4.11  cnf(c1263,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X686)|iext(X686,skolem0008,uri_rdf_List),inference(resolution,[status(thm)],[c1255, c41])).
% 3.93/4.11  cnf(c16,plain,iext(uri_rdf_rest,skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c1])).
% 3.93/4.11  cnf(c295,plain,~iext(uri_rdfs_range,uri_rdf_rest,X237)|icext(X237,skolem0007),inference(resolution,[status(thm)],[c67, c16])).
% 3.93/4.11  cnf(c1252,plain,icext(uri_rdf_List,skolem0007),inference(resolution,[status(thm)],[c295, c119])).
% 3.93/4.11  cnf(c1253,plain,iext(uri_rdf_type,skolem0007,uri_rdf_List),inference(resolution,[status(thm)],[c1252, c131])).
% 3.93/4.11  cnf(c1258,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X685)|iext(X685,skolem0007,uri_rdf_List),inference(resolution,[status(thm)],[c1253, c41])).
% 3.93/4.11  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.93/4.11  cnf(c26,plain,iext(uri_rdfs_range,uri_rdf_type,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_type_range])).
% 3.93/4.11  cnf(c13,plain,iext(uri_rdf_type,uri_ex_MyOrderedCollection,uri_skos_OrderedCollection),inference(split_conjunct,[status(thm)],[c1])).
% 3.93/4.11  cnf(c291,plain,~iext(uri_rdfs_range,uri_rdf_type,X230)|icext(X230,uri_skos_OrderedCollection),inference(resolution,[status(thm)],[c67, c13])).
% 3.93/4.11  cnf(c1224,plain,icext(uri_rdfs_Class,uri_skos_OrderedCollection),inference(resolution,[status(thm)],[c291, c26])).
% 3.93/4.11  cnf(c1225,plain,ic(uri_skos_OrderedCollection),inference(resolution,[status(thm)],[c1224, c87])).
% 3.93/4.11  cnf(c1229,plain,iext(uri_rdfs_subClassOf,uri_skos_OrderedCollection,uri_skos_OrderedCollection),inference(resolution,[status(thm)],[c1225, c48])).
% 3.93/4.11  cnf(c1248,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X683)|iext(X683,uri_skos_OrderedCollection,uri_skos_OrderedCollection),inference(resolution,[status(thm)],[c1229, c41])).
% 3.93/4.11  cnf(c1227,plain,iext(uri_rdfs_subClassOf,uri_skos_OrderedCollection,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1225, c125])).
% 3.93/4.11  cnf(c1242,plain,~iext(uri_rdfs_subClassOf,X682,uri_skos_OrderedCollection)|iext(uri_rdfs_subClassOf,X682,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1227, c45])).
% 3.93/4.11  cnf(c1240,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X681)|iext(X681,uri_skos_OrderedCollection,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1227, c41])).
% 3.93/4.11  cnf(c1226,plain,iext(uri_rdf_type,uri_skos_OrderedCollection,uri_rdfs_Class),inference(resolution,[status(thm)],[c1224, c131])).
% 3.93/4.11  cnf(c1232,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X680)|iext(X680,uri_skos_OrderedCollection,uri_rdfs_Class),inference(resolution,[status(thm)],[c1226, c41])).
% 3.93/4.11  cnf(c5,plain,iext(uri_rdf_rest,skolem0002,skolem0003),inference(split_conjunct,[status(thm)],[c1])).
% 3.93/4.11  cnf(c277,plain,~iext(uri_rdfs_range,uri_rdf_rest,X188)|icext(X188,skolem0003),inference(resolution,[status(thm)],[c67, c5])).
% 3.93/4.11  cnf(c1183,plain,icext(uri_rdf_List,skolem0003),inference(resolution,[status(thm)],[c277, c119])).
% 3.93/4.11  cnf(c1184,plain,iext(uri_rdf_type,skolem0003,uri_rdf_List),inference(resolution,[status(thm)],[c1183, c131])).
% 3.93/4.11  cnf(c1215,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X679)|iext(X679,skolem0003,uri_rdf_List),inference(resolution,[status(thm)],[c1184, c41])).
% 3.93/4.11  cnf(c10,plain,iext(uri_rdf_rest,skolem0004,skolem0005),inference(split_conjunct,[status(thm)],[c1])).
% 3.93/4.11  cnf(c274,plain,~iext(uri_rdfs_range,uri_rdf_rest,X185)|icext(X185,skolem0005),inference(resolution,[status(thm)],[c67, c10])).
% 3.93/4.11  cnf(c1180,plain,icext(uri_rdf_List,skolem0005),inference(resolution,[status(thm)],[c274, c119])).
% 3.93/4.11  cnf(c1181,plain,iext(uri_rdf_type,skolem0005,uri_rdf_List),inference(resolution,[status(thm)],[c1180, c131])).
% 3.93/4.11  cnf(c1210,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X678)|iext(X678,skolem0005,uri_rdf_List),inference(resolution,[status(thm)],[c1181, c41])).
% 3.93/4.11  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.93/4.11  cnf(c88,plain,iext(uri_rdfs_range,uri_rdfs_domain,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_domain_range])).
% 3.93/4.11  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.93/4.11  cnf(c63,plain,iext(uri_rdfs_domain,uri_rdf_object,uri_rdfs_Statement),inference(split_conjunct,[status(thm)],[rdfs_reification_object_domain])).
% 3.93/4.11  cnf(c269,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X180)|icext(X180,uri_rdfs_Statement),inference(resolution,[status(thm)],[c67, c63])).
% 3.93/4.11  cnf(c1172,plain,icext(uri_rdfs_Class,uri_rdfs_Statement),inference(resolution,[status(thm)],[c269, c88])).
% 3.93/4.11  cnf(c1173,plain,ic(uri_rdfs_Statement),inference(resolution,[status(thm)],[c1172, c87])).
% 3.93/4.11  cnf(c1177,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Statement,uri_rdfs_Statement),inference(resolution,[status(thm)],[c1173, c48])).
% 3.93/4.11  cnf(c1204,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X676)|iext(X676,uri_rdfs_Statement,uri_rdfs_Statement),inference(resolution,[status(thm)],[c1177, c41])).
% 3.93/4.11  cnf(c1175,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Statement,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1173, c125])).
% 3.93/4.11  cnf(c1197,plain,~iext(uri_rdfs_subClassOf,X675,uri_rdfs_Statement)|iext(uri_rdfs_subClassOf,X675,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1175, c45])).
% 3.93/4.11  cnf(c1195,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X674)|iext(X674,uri_rdfs_Statement,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1175, c41])).
% 3.93/4.11  cnf(c1174,plain,iext(uri_rdf_type,uri_rdfs_Statement,uri_rdfs_Class),inference(resolution,[status(thm)],[c1172, c131])).
% 3.93/4.11  cnf(c1188,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X673)|iext(X673,uri_rdfs_Statement,uri_rdfs_Class),inference(resolution,[status(thm)],[c1174, c41])).
% 3.93/4.11  cnf(c148,plain,~ip(X103)|iext(uri_rdf_type,X103,uri_rdf_Property),inference(split_conjunct,[status(thm)],[c146])).
% 3.93/4.11  cnf(c40,plain,~iext(uri_rdfs_subPropertyOf,X66,X65)|ip(X65),inference(split_conjunct,[status(thm)],[c38])).
% 3.93/4.11  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.93/4.11  fof(c114,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.93/4.11  fof(c115,plain,(![X40]:(~icext(uri_rdfs_ContainerMembershipProperty,X40)|iext(uri_rdfs_subPropertyOf,X40,uri_rdfs_member))),inference(variable_rename,[status(thm)],[c114])).
% 3.93/4.11  cnf(c116,plain,~icext(uri_rdfs_ContainerMembershipProperty,X94)|iext(uri_rdfs_subPropertyOf,X94,uri_rdfs_member),inference(split_conjunct,[status(thm)],[c115])).
% 3.93/4.11  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.93/4.11  cnf(c103,plain,iext(uri_rdf_type,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),inference(split_conjunct,[status(thm)],[rdfs_container_n_type_002])).
% 3.93/4.11  cnf(c130,plain,~iext(uri_rdf_type,X96,X97)|icext(X97,X96),inference(split_conjunct,[status(thm)],[c129])).
% 3.93/4.11  cnf(c441,plain,icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__2),inference(resolution,[status(thm)],[c130, c103])).
% 3.93/4.11  cnf(c447,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__2,uri_rdfs_member),inference(resolution,[status(thm)],[c441, c116])).
% 3.93/4.11  cnf(c849,plain,ip(uri_rdfs_member),inference(resolution,[status(thm)],[c447, c40])).
% 3.93/4.11  cnf(c856,plain,iext(uri_rdf_type,uri_rdfs_member,uri_rdf_Property),inference(resolution,[status(thm)],[c849, c148])).
% 3.93/4.11  cnf(c1167,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X672)|iext(X672,uri_rdfs_member,uri_rdf_Property),inference(resolution,[status(thm)],[c856, c41])).
% 3.93/4.11  cnf(c855,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_member,uri_rdfs_member),inference(resolution,[status(thm)],[c849, c33])).
% 3.93/4.11  cnf(c1160,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X671)|iext(X671,uri_rdfs_member,uri_rdfs_member),inference(resolution,[status(thm)],[c855, c41])).
% 3.93/4.11  cnf(c86,plain,~ic(X68)|icext(uri_rdfs_Class,X68),inference(split_conjunct,[status(thm)],[c85])).
% 3.93/4.11  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.93/4.11  fof(c50,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.93/4.11  fof(c52,plain,(![X22]:(![X23]:(![X24]:(~iext(uri_rdfs_subClassOf,X22,X23)|((ic(X22)&ic(X23))&(~icext(X22,X24)|icext(X23,X24))))))),inference(shift_quantors,[status(thm)],[fof(c51,plain,(![X22]:(![X23]:(~iext(uri_rdfs_subClassOf,X22,X23)|((ic(X22)&ic(X23))&(![X24]:(~icext(X22,X24)|icext(X23,X24))))))),inference(variable_rename,[status(thm)],[c50])).])).
% 3.93/4.11  fof(c53,plain,(![X22]:(![X23]:(![X24]:(((~iext(uri_rdfs_subClassOf,X22,X23)|ic(X22))&(~iext(uri_rdfs_subClassOf,X22,X23)|ic(X23)))&(~iext(uri_rdfs_subClassOf,X22,X23)|(~icext(X22,X24)|icext(X23,X24))))))),inference(distribute,[status(thm)],[c52])).
% 3.93/4.11  cnf(c55,plain,~iext(uri_rdfs_subClassOf,X80,X81)|ic(X81),inference(split_conjunct,[status(thm)],[c53])).
% 3.93/4.11  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.93/4.11  cnf(c100,plain,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[rdfs_dat_xmlliteral_sub])).
% 3.93/4.11  cnf(c54,plain,~iext(uri_rdfs_subClassOf,X78,X79)|ic(X78),inference(split_conjunct,[status(thm)],[c53])).
% 3.93/4.11  cnf(c231,plain,ic(uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c54, c100])).
% 3.93/4.11  cnf(c413,plain,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Resource),inference(resolution,[status(thm)],[c125, c231])).
% 3.93/4.11  cnf(c751,plain,ic(uri_rdfs_Resource),inference(resolution,[status(thm)],[c413, c55])).
% 3.93/4.11  cnf(c758,plain,icext(uri_rdfs_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c751, c86])).
% 3.93/4.11  cnf(c761,plain,iext(uri_rdf_type,uri_rdfs_Resource,uri_rdfs_Class),inference(resolution,[status(thm)],[c758, c131])).
% 3.93/4.11  cnf(c1152,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X669)|iext(X669,uri_rdfs_Resource,uri_rdfs_Class),inference(resolution,[status(thm)],[c761, c41])).
% 3.93/4.11  cnf(c757,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Resource,uri_rdfs_Resource),inference(resolution,[status(thm)],[c751, c125])).
% 3.93/4.11  cnf(c1147,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X668)|iext(X668,uri_rdfs_Resource,uri_rdfs_Resource),inference(resolution,[status(thm)],[c757, c41])).
% 3.93/4.11  cnf(c2,plain,iext(uri_rdfs_subPropertyOf,uri_skos_memberList,skolem0001),inference(split_conjunct,[status(thm)],[c1])).
% 3.93/4.11  cnf(c14,plain,iext(uri_skos_memberList,uri_ex_MyOrderedCollection,skolem0006),inference(split_conjunct,[status(thm)],[c1])).
% 3.93/4.11  cnf(c196,plain,~iext(uri_rdfs_subPropertyOf,uri_skos_memberList,X130)|iext(X130,uri_ex_MyOrderedCollection,skolem0006),inference(resolution,[status(thm)],[c41, c14])).
% 3.93/4.11  cnf(c748,plain,iext(skolem0001,uri_ex_MyOrderedCollection,skolem0006),inference(resolution,[status(thm)],[c196, c2])).
% 3.93/4.11  cnf(c1138,plain,~iext(uri_rdfs_subPropertyOf,skolem0001,X666)|iext(X666,uri_ex_MyOrderedCollection,skolem0006),inference(resolution,[status(thm)],[c748, c41])).
% 3.93/4.11  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.93/4.11  cnf(c136,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_sub])).
% 3.93/4.11  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.93/4.11  fof(c163,plain,(![S]:(![P]:(![O]:(~iext(P,S,O)|ip(P))))),inference(fof_nnf,[status(thm)],[simple_iext_property])).
% 3.93/4.11  fof(c164,plain,(![S]:(![P]:((![O]:~iext(P,S,O))|ip(P)))),inference(shift_quantors,[status(thm)],[c163])).
% 3.93/4.11  fof(c166,plain,(![X50]:(![X51]:(![X52]:(~iext(X51,X50,X52)|ip(X51))))),inference(shift_quantors,[status(thm)],[fof(c165,plain,(![X50]:(![X51]:((![X52]:~iext(X51,X50,X52))|ip(X51)))),inference(variable_rename,[status(thm)],[c164])).])).
% 3.93/4.11  cnf(c167,plain,~iext(X104,X105,X106)|ip(X104),inference(split_conjunct,[status(thm)],[c166])).
% 3.93/4.11  cnf(c584,plain,ip(uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c167, c136])).
% 3.93/4.11  cnf(c666,plain,iext(uri_rdf_type,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c584, c148])).
% 3.93/4.11  cnf(c1132,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X665)|iext(X665,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c666, c41])).
% 3.93/4.11  cnf(c665,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c584, c33])).
% 3.93/4.11  cnf(c1126,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X664)|iext(X664,uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c665, c41])).
% 3.93/4.11  cnf(c3,plain,iext(uri_owl_propertyChainAxiom,uri_skos_member,skolem0002),inference(split_conjunct,[status(thm)],[c1])).
% 3.93/4.11  cnf(c576,plain,ip(uri_owl_propertyChainAxiom),inference(resolution,[status(thm)],[c167, c3])).
% 3.93/4.11  cnf(c657,plain,iext(uri_rdf_type,uri_owl_propertyChainAxiom,uri_rdf_Property),inference(resolution,[status(thm)],[c576, c148])).
% 3.93/4.11  cnf(c1115,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X662)|iext(X662,uri_owl_propertyChainAxiom,uri_rdf_Property),inference(resolution,[status(thm)],[c657, c41])).
% 3.93/4.11  cnf(c656,plain,iext(uri_rdfs_subPropertyOf,uri_owl_propertyChainAxiom,uri_owl_propertyChainAxiom),inference(resolution,[status(thm)],[c576, c33])).
% 3.93/4.11  cnf(c1107,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X661)|iext(X661,uri_owl_propertyChainAxiom,uri_owl_propertyChainAxiom),inference(resolution,[status(thm)],[c656, c41])).
% 3.93/4.11  cnf(c568,plain,ip(uri_rdfs_domain),inference(resolution,[status(thm)],[c167, c68])).
% 3.93/4.11  cnf(c647,plain,iext(uri_rdf_type,uri_rdfs_domain,uri_rdf_Property),inference(resolution,[status(thm)],[c568, c148])).
% 3.93/4.11  cnf(c1097,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X659)|iext(X659,uri_rdfs_domain,uri_rdf_Property),inference(resolution,[status(thm)],[c647, c41])).
% 3.93/4.11  cnf(c646,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,uri_rdfs_domain),inference(resolution,[status(thm)],[c568, c33])).
% 3.93/4.11  cnf(c1090,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X658)|iext(X658,uri_rdfs_domain,uri_rdfs_domain),inference(resolution,[status(thm)],[c646, c41])).
% 3.93/4.11  cnf(c564,plain,ip(uri_rdfs_range),inference(resolution,[status(thm)],[c167, c134])).
% 3.93/4.11  cnf(c645,plain,iext(uri_rdf_type,uri_rdfs_range,uri_rdf_Property),inference(resolution,[status(thm)],[c564, c148])).
% 3.93/4.11  cnf(c1070,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X656)|iext(X656,uri_rdfs_range,uri_rdf_Property),inference(resolution,[status(thm)],[c645, c41])).
% 3.93/4.11  cnf(c644,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_range,uri_rdfs_range),inference(resolution,[status(thm)],[c564, c33])).
% 3.93/4.11  cnf(c1064,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X655)|iext(X655,uri_rdfs_range,uri_rdfs_range),inference(resolution,[status(thm)],[c644, c41])).
% 3.93/4.11  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.93/4.11  cnf(c117,plain,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Container),inference(split_conjunct,[status(thm)],[rdfs_container_bag_sub])).
% 3.93/4.11  cnf(c563,plain,ip(uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c167, c117])).
% 3.93/4.11  cnf(c643,plain,iext(uri_rdf_type,uri_rdfs_subClassOf,uri_rdf_Property),inference(resolution,[status(thm)],[c563, c148])).
% 3.93/4.11  cnf(c1044,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X653)|iext(X653,uri_rdfs_subClassOf,uri_rdf_Property),inference(resolution,[status(thm)],[c643, c41])).
% 3.93/4.11  cnf(c642,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c563, c33])).
% 3.93/4.11  cnf(c1038,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X652)|iext(X652,uri_rdfs_subClassOf,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c642, c41])).
% 3.93/4.11  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.93/4.11  cnf(c157,plain,iext(uri_rdf_type,uri_rdf_first,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_collection_first_type])).
% 3.93/4.11  cnf(c557,plain,ip(uri_rdf_first),inference(resolution,[status(thm)],[c157, c147])).
% 3.93/4.11  cnf(c560,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_first,uri_rdf_first),inference(resolution,[status(thm)],[c557, c33])).
% 3.93/4.11  cnf(c1028,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X650)|iext(X650,uri_rdf_first,uri_rdf_first),inference(resolution,[status(thm)],[c560, c41])).
% 3.93/4.11  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.93/4.11  cnf(c155,plain,iext(uri_rdf_type,uri_rdf_rest,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_collection_rest_type])).
% 3.93/4.11  cnf(c544,plain,ip(uri_rdf_rest),inference(resolution,[status(thm)],[c155, c147])).
% 3.93/4.11  cnf(c547,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_rest,uri_rdf_rest),inference(resolution,[status(thm)],[c544, c33])).
% 3.93/4.11  cnf(c1014,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X648)|iext(X648,uri_rdf_rest,uri_rdf_rest),inference(resolution,[status(thm)],[c547, c41])).
% 3.93/4.11  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.93/4.11  cnf(c154,plain,iext(uri_rdf_type,uri_rdf__1,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_container_n_type_001])).
% 3.93/4.11  cnf(c536,plain,ip(uri_rdf__1),inference(resolution,[status(thm)],[c154, c147])).
% 3.93/4.11  cnf(c539,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__1,uri_rdf__1),inference(resolution,[status(thm)],[c536, c33])).
% 3.93/4.11  cnf(c1000,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X646)|iext(X646,uri_rdf__1,uri_rdf__1),inference(resolution,[status(thm)],[c539, c41])).
% 3.93/4.11  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.93/4.11  cnf(c153,plain,iext(uri_rdf_type,uri_rdf__2,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_container_n_type_002])).
% 3.93/4.11  cnf(c528,plain,ip(uri_rdf__2),inference(resolution,[status(thm)],[c153, c147])).
% 3.93/4.11  cnf(c531,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__2,uri_rdf__2),inference(resolution,[status(thm)],[c528, c33])).
% 3.93/4.11  cnf(c993,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X644)|iext(X644,uri_rdf__2,uri_rdf__2),inference(resolution,[status(thm)],[c531, c41])).
% 3.93/4.11  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.93/4.11  cnf(c152,plain,iext(uri_rdf_type,uri_rdf__3,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_container_n_type_003])).
% 3.93/4.11  cnf(c520,plain,ip(uri_rdf__3),inference(resolution,[status(thm)],[c152, c147])).
% 3.93/4.11  cnf(c523,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__3,uri_rdf__3),inference(resolution,[status(thm)],[c520, c33])).
% 3.93/4.11  cnf(c986,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X642)|iext(X642,uri_rdf__3,uri_rdf__3),inference(resolution,[status(thm)],[c523, c41])).
% 3.93/4.11  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.93/4.11  cnf(c151,plain,iext(uri_rdf_type,uri_rdf_object,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_reification_object_type])).
% 3.93/4.11  cnf(c512,plain,ip(uri_rdf_object),inference(resolution,[status(thm)],[c151, c147])).
% 3.93/4.11  cnf(c515,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_object,uri_rdf_object),inference(resolution,[status(thm)],[c512, c33])).
% 3.93/4.11  cnf(c978,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X640)|iext(X640,uri_rdf_object,uri_rdf_object),inference(resolution,[status(thm)],[c515, c41])).
% 3.93/4.11  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.93/4.11  cnf(c150,plain,iext(uri_rdf_type,uri_rdf_value,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_reification_predicate_type])).
% 3.93/4.11  cnf(c498,plain,ip(uri_rdf_value),inference(resolution,[status(thm)],[c150, c147])).
% 3.93/4.11  cnf(c507,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_value,uri_rdf_value),inference(resolution,[status(thm)],[c498, c33])).
% 3.93/4.11  cnf(c969,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X638)|iext(X638,uri_rdf_value,uri_rdf_value),inference(resolution,[status(thm)],[c507, c41])).
% 3.93/4.11  cnf(c39,plain,~iext(uri_rdfs_subPropertyOf,X60,X59)|ip(X60),inference(split_conjunct,[status(thm)],[c38])).
% 3.93/4.11  cnf(c170,plain,ip(uri_skos_memberList),inference(resolution,[status(thm)],[c39, c2])).
% 3.93/4.11  cnf(c506,plain,iext(uri_rdf_type,uri_skos_memberList,uri_rdf_Property),inference(resolution,[status(thm)],[c148, c170])).
% 3.93/4.11  cnf(c961,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X636)|iext(X636,uri_skos_memberList,uri_rdf_Property),inference(resolution,[status(thm)],[c506, c41])).
% 3.93/4.11  cnf(c173,plain,ip(skolem0001),inference(resolution,[status(thm)],[c40, c2])).
% 3.93/4.11  cnf(c505,plain,iext(uri_rdf_type,skolem0001,uri_rdf_Property),inference(resolution,[status(thm)],[c148, c173])).
% 3.93/4.11  cnf(c953,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X635)|iext(X635,skolem0001,uri_rdf_Property),inference(resolution,[status(thm)],[c505, c41])).
% 3.93/4.11  cnf(c433,plain,ip(uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c136, c40])).
% 3.93/4.11  cnf(c503,plain,iext(uri_rdf_type,uri_rdfs_seeAlso,uri_rdf_Property),inference(resolution,[status(thm)],[c148, c433])).
% 3.93/4.11  cnf(c945,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X634)|iext(X634,uri_rdfs_seeAlso,uri_rdf_Property),inference(resolution,[status(thm)],[c503, c41])).
% 3.93/4.11  cnf(c434,plain,ip(uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c136, c39])).
% 3.93/4.11  cnf(c502,plain,iext(uri_rdf_type,uri_rdfs_isDefinedBy,uri_rdf_Property),inference(resolution,[status(thm)],[c148, c434])).
% 3.93/4.11  cnf(c937,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X633)|iext(X633,uri_rdfs_isDefinedBy,uri_rdf_Property),inference(resolution,[status(thm)],[c502, c41])).
% 3.93/4.11  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.93/4.11  cnf(c149,plain,iext(uri_rdf_type,uri_rdf_subject,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_reification_subject_type])).
% 3.93/4.11  cnf(c491,plain,ip(uri_rdf_subject),inference(resolution,[status(thm)],[c149, c147])).
% 3.93/4.11  cnf(c494,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_subject,uri_rdf_subject),inference(resolution,[status(thm)],[c491, c33])).
% 3.93/4.11  cnf(c931,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X632)|iext(X632,uri_rdf_subject,uri_rdf_subject),inference(resolution,[status(thm)],[c494, c41])).
% 3.93/4.11  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.93/4.11  cnf(c141,plain,iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_value_type])).
% 3.93/4.11  cnf(c487,plain,ip(uri_rdf_type),inference(resolution,[status(thm)],[c147, c141])).
% 3.93/4.11  cnf(c488,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_type,uri_rdf_type),inference(resolution,[status(thm)],[c487, c33])).
% 3.93/4.11  cnf(c924,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X630)|iext(X630,uri_rdf_type,uri_rdf_type),inference(resolution,[status(thm)],[c488, c41])).
% 3.93/4.11  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.93/4.11  cnf(c102,plain,iext(uri_rdf_type,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),inference(split_conjunct,[status(thm)],[rdfs_container_n_type_003])).
% 3.93/4.11  cnf(c443,plain,icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__3),inference(resolution,[status(thm)],[c130, c102])).
% 3.93/4.11  cnf(c463,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__3,uri_rdfs_member),inference(resolution,[status(thm)],[c443, c116])).
% 3.93/4.11  cnf(c914,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X628)|iext(X628,uri_rdf__3,uri_rdfs_member),inference(resolution,[status(thm)],[c463, c41])).
% 3.93/4.11  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.93/4.11  fof(c28,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.93/4.11  fof(c29,plain,(![X10]:(![X11]:(![X12]:((~iext(uri_rdfs_subPropertyOf,X10,X11)|~iext(uri_rdfs_subPropertyOf,X11,X12))|iext(uri_rdfs_subPropertyOf,X10,X12))))),inference(variable_rename,[status(thm)],[c28])).
% 3.93/4.11  cnf(c30,plain,~iext(uri_rdfs_subPropertyOf,X57,X55)|~iext(uri_rdfs_subPropertyOf,X55,X56)|iext(uri_rdfs_subPropertyOf,X57,X56),inference(split_conjunct,[status(thm)],[c29])).
% 3.93/4.11  cnf(c912,plain,~iext(uri_rdfs_subPropertyOf,X627,uri_rdf__3)|iext(uri_rdfs_subPropertyOf,X627,uri_rdfs_member),inference(resolution,[status(thm)],[c463, c30])).
% 3.93/4.11  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.93/4.11  cnf(c95,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_datatype_sub])).
% 3.93/4.11  cnf(c243,plain,ic(uri_rdfs_Class),inference(resolution,[status(thm)],[c55, c95])).
% 3.93/4.11  cnf(c248,plain,icext(uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c243, c86])).
% 3.93/4.11  cnf(c461,plain,iext(uri_rdf_type,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c131, c248])).
% 3.93/4.11  cnf(c907,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X626)|iext(X626,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c461, c41])).
% 3.93/4.11  cnf(c381,plain,ic(uri_rdf_Bag),inference(resolution,[status(thm)],[c117, c54])).
% 3.93/4.11  cnf(c385,plain,icext(uri_rdfs_Class,uri_rdf_Bag),inference(resolution,[status(thm)],[c381, c86])).
% 3.93/4.11  cnf(c458,plain,iext(uri_rdf_type,uri_rdf_Bag,uri_rdfs_Class),inference(resolution,[status(thm)],[c131, c385])).
% 3.93/4.11  cnf(c902,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X625)|iext(X625,uri_rdf_Bag,uri_rdfs_Class),inference(resolution,[status(thm)],[c458, c41])).
% 3.93/4.11  cnf(c234,plain,icext(uri_rdfs_Class,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c231, c86])).
% 3.93/4.11  cnf(c457,plain,iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Class),inference(resolution,[status(thm)],[c131, c234])).
% 3.93/4.11  cnf(c897,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X624)|iext(X624,uri_rdf_XMLLiteral,uri_rdfs_Class),inference(resolution,[status(thm)],[c457, c41])).
% 3.93/4.11  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.93/4.11  cnf(c118,plain,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Container),inference(split_conjunct,[status(thm)],[rdfs_container_alt_sub])).
% 3.93/4.11  cnf(c391,plain,ic(uri_rdf_Alt),inference(resolution,[status(thm)],[c118, c54])).
% 3.93/4.11  cnf(c395,plain,icext(uri_rdfs_Class,uri_rdf_Alt),inference(resolution,[status(thm)],[c391, c86])).
% 3.93/4.11  cnf(c456,plain,iext(uri_rdf_type,uri_rdf_Alt,uri_rdfs_Class),inference(resolution,[status(thm)],[c131, c395])).
% 3.93/4.11  cnf(c892,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X623)|iext(X623,uri_rdf_Alt,uri_rdfs_Class),inference(resolution,[status(thm)],[c456, c41])).
% 3.93/4.11  cnf(c233,plain,ic(uri_rdfs_Datatype),inference(resolution,[status(thm)],[c54, c95])).
% 3.93/4.11  cnf(c238,plain,icext(uri_rdfs_Class,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c233, c86])).
% 3.93/4.11  cnf(c455,plain,iext(uri_rdf_type,uri_rdfs_Datatype,uri_rdfs_Class),inference(resolution,[status(thm)],[c131, c238])).
% 3.93/4.11  cnf(c887,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X622)|iext(X622,uri_rdfs_Datatype,uri_rdfs_Class),inference(resolution,[status(thm)],[c455, c41])).
% 3.93/4.11  cnf(c241,plain,ic(uri_rdfs_Literal),inference(resolution,[status(thm)],[c55, c100])).
% 3.93/4.11  cnf(c244,plain,icext(uri_rdfs_Class,uri_rdfs_Literal),inference(resolution,[status(thm)],[c241, c86])).
% 3.93/4.11  cnf(c453,plain,iext(uri_rdf_type,uri_rdfs_Literal,uri_rdfs_Class),inference(resolution,[status(thm)],[c131, c244])).
% 3.93/4.11  cnf(c882,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X621)|iext(X621,uri_rdfs_Literal,uri_rdfs_Class),inference(resolution,[status(thm)],[c453, c41])).
% 3.93/4.11  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.93/4.11  cnf(c101,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Container),inference(split_conjunct,[status(thm)],[rdfs_container_seq_sub])).
% 3.93/4.11  cnf(c242,plain,ic(uri_rdfs_Container),inference(resolution,[status(thm)],[c55, c101])).
% 3.93/4.11  cnf(c246,plain,icext(uri_rdfs_Class,uri_rdfs_Container),inference(resolution,[status(thm)],[c242, c86])).
% 3.93/4.11  cnf(c452,plain,iext(uri_rdf_type,uri_rdfs_Container,uri_rdfs_Class),inference(resolution,[status(thm)],[c131, c246])).
% 3.93/4.11  cnf(c877,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X620)|iext(X620,uri_rdfs_Container,uri_rdfs_Class),inference(resolution,[status(thm)],[c452, c41])).
% 3.93/4.11  cnf(c232,plain,ic(uri_rdfs_Seq),inference(resolution,[status(thm)],[c54, c101])).
% 3.93/4.11  cnf(c236,plain,icext(uri_rdfs_Class,uri_rdfs_Seq),inference(resolution,[status(thm)],[c232, c86])).
% 3.93/4.11  cnf(c451,plain,iext(uri_rdf_type,uri_rdfs_Seq,uri_rdfs_Class),inference(resolution,[status(thm)],[c131, c236])).
% 3.93/4.11  cnf(c872,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X619)|iext(X619,uri_rdfs_Seq,uri_rdfs_Class),inference(resolution,[status(thm)],[c451, c41])).
% 3.93/4.11  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.93/4.11  cnf(c113,plain,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_container_containermembershipproperty_sub])).
% 3.93/4.11  cnf(c314,plain,ic(uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c113, c54])).
% 3.93/4.11  cnf(c374,plain,icext(uri_rdfs_Class,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c314, c86])).
% 3.93/4.11  cnf(c449,plain,iext(uri_rdf_type,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Class),inference(resolution,[status(thm)],[c131, c374])).
% 3.93/4.11  cnf(c867,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X618)|iext(X618,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Class),inference(resolution,[status(thm)],[c449, c41])).
% 3.93/4.11  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.93/4.11  cnf(c104,plain,iext(uri_rdf_type,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),inference(split_conjunct,[status(thm)],[rdfs_container_n_type_001])).
% 3.93/4.11  cnf(c442,plain,icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__1),inference(resolution,[status(thm)],[c130, c104])).
% 3.93/4.11  cnf(c448,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__1,uri_rdfs_member),inference(resolution,[status(thm)],[c442, c116])).
% 3.93/4.11  cnf(c862,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X617)|iext(X617,uri_rdf__1,uri_rdfs_member),inference(resolution,[status(thm)],[c448, c41])).
% 3.93/4.11  cnf(c860,plain,~iext(uri_rdfs_subPropertyOf,X616,uri_rdf__1)|iext(uri_rdfs_subPropertyOf,X616,uri_rdfs_member),inference(resolution,[status(thm)],[c448, c30])).
% 3.93/4.11  cnf(c1444,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X615)|icext(X615,uri_rdfs_comment),inference(resolution,[status(thm)],[c1436, c93])).
% 3.93/4.11  cnf(c853,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X614)|iext(X614,uri_rdf__2,uri_rdfs_member),inference(resolution,[status(thm)],[c447, c41])).
% 3.93/4.11  cnf(c1440,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X613)|icext(X613,uri_rdfs_comment),inference(resolution,[status(thm)],[c1436, c67])).
% 3.93/4.11  cnf(c851,plain,~iext(uri_rdfs_subPropertyOf,X610,uri_rdf__2)|iext(uri_rdfs_subPropertyOf,X610,uri_rdfs_member),inference(resolution,[status(thm)],[c447, c30])).
% 3.93/4.11  cnf(c1415,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X609)|icext(X609,uri_rdfs_label),inference(resolution,[status(thm)],[c1406, c93])).
% 3.93/4.11  cnf(c1411,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X608)|icext(X608,uri_rdfs_label),inference(resolution,[status(thm)],[c1406, c67])).
% 3.93/4.11  cnf(c445,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c434, c33])).
% 3.93/4.11  cnf(c846,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X606)|iext(X606,uri_rdfs_isDefinedBy,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c445, c41])).
% 3.93/4.11  cnf(c1381,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X603)|icext(X603,uri_rdf_List),inference(resolution,[status(thm)],[c1363, c67])).
% 3.93/4.11  cnf(c1377,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X601)|icext(X601,uri_rdf_List),inference(resolution,[status(thm)],[c1361, c93])).
% 3.93/4.11  cnf(c438,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_seeAlso,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c433, c33])).
% 3.93/4.11  cnf(c839,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X597)|iext(X597,uri_rdfs_seeAlso,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c438, c41])).
% 3.93/4.11  cnf(c1321,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X594)|icext(X594,uri_rdf_predicate),inference(resolution,[status(thm)],[c1313, c93])).
% 3.93/4.11  cnf(c1317,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X592)|icext(X592,uri_rdf_predicate),inference(resolution,[status(thm)],[c1313, c67])).
% 3.93/4.11  cnf(c312,plain,ic(uri_rdf_Property),inference(resolution,[status(thm)],[c113, c55])).
% 3.93/4.11  cnf(c422,plain,iext(uri_rdfs_subClassOf,uri_rdf_Property,uri_rdfs_Resource),inference(resolution,[status(thm)],[c125, c312])).
% 3.93/4.11  cnf(c832,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X588)|iext(X588,uri_rdf_Property,uri_rdfs_Resource),inference(resolution,[status(thm)],[c422, c41])).
% 3.93/4.11  cnf(c831,plain,~iext(uri_rdfs_subClassOf,X584,uri_rdf_Property)|iext(uri_rdfs_subClassOf,X584,uri_rdfs_Resource),inference(resolution,[status(thm)],[c422, c45])).
% 3.93/4.11  cnf(c421,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Resource),inference(resolution,[status(thm)],[c125, c233])).
% 3.93/4.11  cnf(c824,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X579)|iext(X579,uri_rdfs_Datatype,uri_rdfs_Resource),inference(resolution,[status(thm)],[c421, c41])).
% 3.93/4.11  cnf(c1246,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X577)|icext(X577,uri_skos_OrderedCollection),inference(resolution,[status(thm)],[c1229, c67])).
% 3.93/4.11  cnf(c823,plain,~iext(uri_rdfs_subClassOf,X576,uri_rdfs_Datatype)|iext(uri_rdfs_subClassOf,X576,uri_rdfs_Resource),inference(resolution,[status(thm)],[c421, c45])).
% 3.93/4.11  cnf(c1243,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X575)|icext(X575,uri_skos_OrderedCollection),inference(resolution,[status(thm)],[c1227, c93])).
% 3.93/4.11  cnf(c420,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Resource),inference(resolution,[status(thm)],[c125, c232])).
% 3.93/4.11  cnf(c816,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X571)|iext(X571,uri_rdfs_Seq,uri_rdfs_Resource),inference(resolution,[status(thm)],[c420, c41])).
% 3.93/4.11  cnf(c815,plain,~iext(uri_rdfs_subClassOf,X566,uri_rdfs_Seq)|iext(uri_rdfs_subClassOf,X566,uri_rdfs_Resource),inference(resolution,[status(thm)],[c420, c45])).
% 3.93/4.11  cnf(c1202,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X564)|icext(X564,uri_rdfs_Statement),inference(resolution,[status(thm)],[c1177, c67])).
% 3.93/4.11  cnf(c419,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c125, c243])).
% 3.93/4.11  cnf(c808,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X563)|iext(X563,uri_rdfs_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c419, c41])).
% 3.93/4.11  cnf(c1198,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X562)|icext(X562,uri_rdfs_Statement),inference(resolution,[status(thm)],[c1175, c93])).
% 3.93/4.11  cnf(c807,plain,~iext(uri_rdfs_subClassOf,X559,uri_rdfs_Class)|iext(uri_rdfs_subClassOf,X559,uri_rdfs_Resource),inference(resolution,[status(thm)],[c419, c45])).
% 3.93/4.11  cnf(c418,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Container,uri_rdfs_Resource),inference(resolution,[status(thm)],[c125, c242])).
% 3.93/4.11  cnf(c800,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X554)|iext(X554,uri_rdfs_Container,uri_rdfs_Resource),inference(resolution,[status(thm)],[c418, c41])).
% 3.93/4.11  cnf(c799,plain,~iext(uri_rdfs_subClassOf,X553,uri_rdfs_Container)|iext(uri_rdfs_subClassOf,X553,uri_rdfs_Resource),inference(resolution,[status(thm)],[c418, c45])).
% 3.93/4.11  cnf(c1159,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X552)|icext(X552,uri_rdfs_member),inference(resolution,[status(thm)],[c855, c93])).
% 3.93/4.11  cnf(c417,plain,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Resource),inference(resolution,[status(thm)],[c125, c391])).
% 3.93/4.11  cnf(c792,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X548)|iext(X548,uri_rdf_Alt,uri_rdfs_Resource),inference(resolution,[status(thm)],[c417, c41])).
% 3.93/4.11  cnf(c1145,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X547)|icext(X547,uri_rdfs_Resource),inference(resolution,[status(thm)],[c757, c93])).
% 3.93/4.11  cnf(c1139,plain,~iext(uri_rdfs_range,skolem0001,X546)|icext(X546,skolem0006),inference(resolution,[status(thm)],[c748, c67])).
% 3.93/4.11  cnf(c1137,plain,~iext(uri_rdfs_domain,skolem0001,X545)|icext(X545,uri_ex_MyOrderedCollection),inference(resolution,[status(thm)],[c748, c93])).
% 3.93/4.11  cnf(c791,plain,~iext(uri_rdfs_subClassOf,X544,uri_rdf_Alt)|iext(uri_rdfs_subClassOf,X544,uri_rdfs_Resource),inference(resolution,[status(thm)],[c417, c45])).
% 3.93/4.11  cnf(c1127,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X541)|icext(X541,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c665, c67])).
% 3.93/4.11  cnf(c416,plain,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Resource),inference(resolution,[status(thm)],[c125, c314])).
% 3.93/4.11  cnf(c784,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X540)|iext(X540,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Resource),inference(resolution,[status(thm)],[c416, c41])).
% 3.93/4.11  cnf(c1125,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X539)|icext(X539,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c665, c93])).
% 3.93/4.11  cnf(c783,plain,~iext(uri_rdfs_subClassOf,X536,uri_rdfs_ContainerMembershipProperty)|iext(uri_rdfs_subClassOf,X536,uri_rdfs_Resource),inference(resolution,[status(thm)],[c416, c45])).
% 3.93/4.11  cnf(c1108,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X535)|icext(X535,uri_owl_propertyChainAxiom),inference(resolution,[status(thm)],[c656, c67])).
% 3.93/4.11  cnf(c1106,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X534)|icext(X534,uri_owl_propertyChainAxiom),inference(resolution,[status(thm)],[c656, c93])).
% 3.93/4.11  cnf(c415,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Literal,uri_rdfs_Resource),inference(resolution,[status(thm)],[c125, c241])).
% 3.93/4.11  cnf(c776,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X533)|iext(X533,uri_rdfs_Literal,uri_rdfs_Resource),inference(resolution,[status(thm)],[c415, c41])).
% 3.93/4.11  cnf(c775,plain,~iext(uri_rdfs_subClassOf,X530,uri_rdfs_Literal)|iext(uri_rdfs_subClassOf,X530,uri_rdfs_Resource),inference(resolution,[status(thm)],[c415, c45])).
% 3.93/4.11  cnf(c1091,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X529)|icext(X529,uri_rdfs_domain),inference(resolution,[status(thm)],[c646, c67])).
% 3.93/4.11  cnf(c1089,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X528)|icext(X528,uri_rdfs_domain),inference(resolution,[status(thm)],[c646, c93])).
% 3.93/4.11  cnf(c414,plain,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Resource),inference(resolution,[status(thm)],[c125, c381])).
% 3.93/4.11  cnf(c768,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X526)|iext(X526,uri_rdf_Bag,uri_rdfs_Resource),inference(resolution,[status(thm)],[c414, c41])).
% 3.93/4.11  cnf(c1065,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X524)|icext(X524,uri_rdfs_range),inference(resolution,[status(thm)],[c644, c67])).
% 3.93/4.11  cnf(c767,plain,~iext(uri_rdfs_subClassOf,X523,uri_rdf_Bag)|iext(uri_rdfs_subClassOf,X523,uri_rdfs_Resource),inference(resolution,[status(thm)],[c414, c45])).
% 3.93/4.11  cnf(c1062,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X522)|icext(X522,uri_rdfs_range),inference(resolution,[status(thm)],[c644, c93])).
% 3.93/4.11  cnf(c755,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X519)|iext(X519,uri_rdf_XMLLiteral,uri_rdfs_Resource),inference(resolution,[status(thm)],[c413, c41])).
% 3.93/4.11  cnf(c1039,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X518)|icext(X518,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c642, c67])).
% 3.93/4.11  cnf(c1037,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X517)|icext(X517,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c642, c93])).
% 3.93/4.11  cnf(c754,plain,~iext(uri_rdfs_subClassOf,X516,uri_rdf_XMLLiteral)|iext(uri_rdfs_subClassOf,X516,uri_rdfs_Resource),inference(resolution,[status(thm)],[c413, c45])).
% 3.93/4.11  cnf(c1029,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X515)|icext(X515,uri_rdf_first),inference(resolution,[status(thm)],[c560, c67])).
% 3.93/4.11  cnf(c1027,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X514)|icext(X514,uri_rdf_first),inference(resolution,[status(thm)],[c560, c93])).
% 3.93/4.11  cnf(c396,plain,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdf_Alt),inference(resolution,[status(thm)],[c391, c48])).
% 3.93/4.11  cnf(c745,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X513)|iext(X513,uri_rdf_Alt,uri_rdf_Alt),inference(resolution,[status(thm)],[c396, c41])).
% 3.93/4.11  cnf(c1015,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X512)|icext(X512,uri_rdf_rest),inference(resolution,[status(thm)],[c547, c67])).
% 3.93/4.11  cnf(c1013,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X511)|icext(X511,uri_rdf_rest),inference(resolution,[status(thm)],[c547, c93])).
% 3.93/4.11  cnf(c1001,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X510)|icext(X510,uri_rdf__1),inference(resolution,[status(thm)],[c539, c67])).
% 3.93/4.11  cnf(c994,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X507)|icext(X507,uri_rdf__2),inference(resolution,[status(thm)],[c531, c67])).
% 3.93/4.11  cnf(c386,plain,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdf_Bag),inference(resolution,[status(thm)],[c381, c48])).
% 3.93/4.11  cnf(c737,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X505)|iext(X505,uri_rdf_Bag,uri_rdf_Bag),inference(resolution,[status(thm)],[c386, c41])).
% 3.93/4.11  cnf(c987,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X504)|icext(X504,uri_rdf__3),inference(resolution,[status(thm)],[c523, c67])).
% 3.93/4.11  cnf(c979,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X502)|icext(X502,uri_rdf_object),inference(resolution,[status(thm)],[c515, c67])).
% 3.93/4.11  cnf(c977,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X500)|icext(X500,uri_rdf_object),inference(resolution,[status(thm)],[c515, c93])).
% 3.93/4.11  cnf(c970,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X499)|icext(X499,uri_rdf_value),inference(resolution,[status(thm)],[c507, c67])).
% 3.93/4.11  cnf(c375,plain,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c314, c48])).
% 3.93/4.11  cnf(c729,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X498)|iext(X498,uri_rdfs_ContainerMembershipProperty,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c375, c41])).
% 3.93/4.11  cnf(c968,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X497)|icext(X497,uri_rdf_value),inference(resolution,[status(thm)],[c507, c93])).
% 3.93/4.11  cnf(c373,plain,iext(uri_rdfs_subClassOf,uri_rdf_Property,uri_rdf_Property),inference(resolution,[status(thm)],[c312, c48])).
% 3.93/4.11  cnf(c721,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X488)|iext(X488,uri_rdf_Property,uri_rdf_Property),inference(resolution,[status(thm)],[c373, c41])).
% 3.93/4.11  cnf(c932,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X486)|icext(X486,uri_rdf_subject),inference(resolution,[status(thm)],[c494, c67])).
% 3.93/4.11  cnf(c930,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X485)|icext(X485,uri_rdf_subject),inference(resolution,[status(thm)],[c494, c93])).
% 3.93/4.11  cnf(c925,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X483)|icext(X483,uri_rdf_type),inference(resolution,[status(thm)],[c488, c67])).
% 3.93/4.11  cnf(c923,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X482)|icext(X482,uri_rdf_type),inference(resolution,[status(thm)],[c488, c93])).
% 3.93/4.11  cnf(c249,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c243, c48])).
% 3.93/4.11  cnf(c713,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X481)|iext(X481,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c249, c41])).
% 3.93/4.11  cnf(c913,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X479)|icext(X479,uri_rdf__3),inference(resolution,[status(thm)],[c463, c93])).
% 3.93/4.11  cnf(c247,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Container,uri_rdfs_Container),inference(resolution,[status(thm)],[c242, c48])).
% 3.93/4.11  cnf(c705,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X471)|iext(X471,uri_rdfs_Container,uri_rdfs_Container),inference(resolution,[status(thm)],[c247, c41])).
% 3.93/4.11  cnf(c245,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Literal,uri_rdfs_Literal),inference(resolution,[status(thm)],[c241, c48])).
% 3.93/4.11  cnf(c697,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X460)|iext(X460,uri_rdfs_Literal,uri_rdfs_Literal),inference(resolution,[status(thm)],[c245, c41])).
% 3.93/4.11  cnf(c861,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X454)|icext(X454,uri_rdf__1),inference(resolution,[status(thm)],[c448, c93])).
% 3.93/4.11  cnf(c854,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X453)|icext(X453,uri_rdfs_member),inference(resolution,[status(thm)],[c447, c67])).
% 3.93/4.11  cnf(c239,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c233, c48])).
% 3.93/4.11  cnf(c689,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X452)|iext(X452,uri_rdfs_Datatype,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c239, c41])).
% 3.93/4.11  cnf(c852,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X451)|icext(X451,uri_rdf__2),inference(resolution,[status(thm)],[c447, c93])).
% 3.93/4.11  cnf(c847,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X450)|icext(X450,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c445, c67])).
% 3.93/4.11  cnf(c838,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X446)|icext(X446,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c438, c93])).
% 3.93/4.11  cnf(c237,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Seq),inference(resolution,[status(thm)],[c232, c48])).
% 3.93/4.11  cnf(c681,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X443)|iext(X443,uri_rdfs_Seq,uri_rdfs_Seq),inference(resolution,[status(thm)],[c237, c41])).
% 3.93/4.11  cnf(c235,plain,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c231, c48])).
% 3.93/4.11  cnf(c673,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X432)|iext(X432,uri_rdf_XMLLiteral,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c235, c41])).
% 3.93/4.11  cnf(c756,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X423)|icext(X423,uri_rdfs_Resource),inference(resolution,[status(thm)],[c413, c67])).
% 3.93/4.11  cnf(c174,plain,iext(uri_rdfs_subPropertyOf,skolem0001,skolem0001),inference(resolution,[status(thm)],[c173, c33])).
% 3.93/4.11  cnf(c663,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X422)|iext(X422,skolem0001,skolem0001),inference(resolution,[status(thm)],[c174, c41])).
% 3.93/4.11  cnf(c746,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X420)|icext(X420,uri_rdf_Alt),inference(resolution,[status(thm)],[c396, c67])).
% 3.93/4.11  cnf(c738,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X417)|icext(X417,uri_rdf_Bag),inference(resolution,[status(thm)],[c386, c67])).
% 3.93/4.11  cnf(c730,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X415)|icext(X415,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c375, c67])).
% 3.93/4.11  cnf(c171,plain,iext(uri_rdfs_subPropertyOf,uri_skos_memberList,uri_skos_memberList),inference(resolution,[status(thm)],[c170, c33])).
% 3.93/4.11  cnf(c654,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X414)|iext(X414,uri_skos_memberList,uri_skos_memberList),inference(resolution,[status(thm)],[c171, c41])).
% 3.93/4.11  cnf(c719,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X411)|icext(X411,uri_rdf_Property),inference(resolution,[status(thm)],[c373, c93])).
% 3.93/4.11  cnf(c711,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X408)|icext(X408,uri_rdfs_Class),inference(resolution,[status(thm)],[c249, c93])).
% 3.93/4.11  cnf(c558,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X406)|iext(X406,uri_rdf_first,uri_rdf_Property),inference(resolution,[status(thm)],[c157, c41])).
% 3.93/4.11  cnf(c703,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X405)|icext(X405,uri_rdfs_Container),inference(resolution,[status(thm)],[c247, c93])).
% 3.93/4.11  cnf(c695,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X403)|icext(X403,uri_rdfs_Literal),inference(resolution,[status(thm)],[c245, c93])).
% 3.93/4.11  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.93/4.11  cnf(c156,plain,iext(uri_rdf_type,uri_rdf_nil,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdf_collection_nil_type])).
% 3.93/4.11  cnf(c552,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X402)|iext(X402,uri_rdf_nil,uri_rdf_List),inference(resolution,[status(thm)],[c156, c41])).
% 3.93/4.11  cnf(c690,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X401)|icext(X401,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c239, c67])).
% 3.93/4.11  cnf(c545,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X399)|iext(X399,uri_rdf_rest,uri_rdf_Property),inference(resolution,[status(thm)],[c155, c41])).
% 3.93/4.11  cnf(c682,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X398)|icext(X398,uri_rdfs_Seq),inference(resolution,[status(thm)],[c237, c67])).
% 3.93/4.11  cnf(c674,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X396)|icext(X396,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c235, c67])).
% 3.93/4.11  cnf(c537,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X395)|iext(X395,uri_rdf__1,uri_rdf_Property),inference(resolution,[status(thm)],[c154, c41])).
% 3.93/4.11  cnf(c658,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X392)|icext(X392,skolem0001),inference(resolution,[status(thm)],[c174, c93])).
% 3.93/4.11  cnf(c529,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X391)|iext(X391,uri_rdf__2,uri_rdf_Property),inference(resolution,[status(thm)],[c153, c41])).
% 3.93/4.11  cnf(c655,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X390)|icext(X390,uri_skos_memberList),inference(resolution,[status(thm)],[c171, c67])).
% 3.93/4.11  cnf(c521,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X387)|iext(X387,uri_rdf__3,uri_rdf_Property),inference(resolution,[status(thm)],[c152, c41])).
% 3.93/4.11  cnf(c553,plain,~iext(uri_rdfs_range,uri_rdf_type,X385)|icext(X385,uri_rdf_List),inference(resolution,[status(thm)],[c156, c67])).
% 3.93/4.11  cnf(c513,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X383)|iext(X383,uri_rdf_object,uri_rdf_Property),inference(resolution,[status(thm)],[c151, c41])).
% 3.93/4.11  cnf(c499,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X378)|iext(X378,uri_rdf_value,uri_rdf_Property),inference(resolution,[status(thm)],[c150, c41])).
% 3.93/4.11  cnf(c492,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X373)|iext(X373,uri_rdf_subject,uri_rdf_Property),inference(resolution,[status(thm)],[c149, c41])).
% 3.93/4.11  cnf(c484,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X368)|iext(X368,uri_rdf_type,uri_rdf_Property),inference(resolution,[status(thm)],[c141, c41])).
% 3.93/4.11  cnf(c485,plain,~iext(uri_rdfs_range,uri_rdf_type,X365)|icext(X365,uri_rdf_Property),inference(resolution,[status(thm)],[c141, c67])).
% 3.93/4.11  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.93/4.11  cnf(c140,plain,iext(uri_rdfs_domain,uri_rdfs_comment,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_comment_domain])).
% 3.93/4.11  cnf(c480,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X364)|iext(X364,uri_rdfs_comment,uri_rdfs_Resource),inference(resolution,[status(thm)],[c140, c41])).
% 3.93/4.11  cnf(c479,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X361)|icext(X361,uri_rdfs_comment),inference(resolution,[status(thm)],[c140, c93])).
% 3.93/4.11  cnf(c477,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X360)|iext(X360,uri_rdfs_comment,uri_rdfs_Literal),inference(resolution,[status(thm)],[c139, c41])).
% 3.93/4.11  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.93/4.11  cnf(c138,plain,iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_domain])).
% 3.93/4.11  cnf(c474,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X358)|iext(X358,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(resolution,[status(thm)],[c138, c41])).
% 3.93/4.11  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.93/4.11  cnf(c137,plain,iext(uri_rdfs_range,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_range])).
% 3.93/4.11  cnf(c471,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X357)|iext(X357,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(resolution,[status(thm)],[c137, c41])).
% 3.93/4.11  fof(simple_ir,axiom,(![X]:ir(X)),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', simple_ir)).
% 3.93/4.11  fof(c161,plain,(![X49]:ir(X49)),inference(variable_rename,[status(thm)],[simple_ir])).
% 3.93/4.11  cnf(c162,plain,ir(X53),inference(split_conjunct,[status(thm)],[c161])).
% 3.93/4.11  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.93/4.11  fof(c76,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.93/4.11  fof(c77,plain,((![X]:(~ir(X)|icext(uri_rdfs_Resource,X)))&(![X]:(~icext(uri_rdfs_Resource,X)|ir(X)))),inference(shift_quantors,[status(thm)],[c76])).
% 3.93/4.11  fof(c79,plain,(![X31]:(![X32]:((~ir(X31)|icext(uri_rdfs_Resource,X31))&(~icext(uri_rdfs_Resource,X32)|ir(X32))))),inference(shift_quantors,[status(thm)],[fof(c78,plain,((![X31]:(~ir(X31)|icext(uri_rdfs_Resource,X31)))&(![X32]:(~icext(uri_rdfs_Resource,X32)|ir(X32)))),inference(variable_rename,[status(thm)],[c77])).])).
% 3.93/4.11  cnf(c80,plain,~ir(X63)|icext(uri_rdfs_Resource,X63),inference(split_conjunct,[status(thm)],[c79])).
% 3.93/4.11  cnf(c172,plain,icext(uri_rdfs_Resource,X64),inference(resolution,[status(thm)],[c80, c162])).
% 3.93/4.11  cnf(c460,plain,iext(uri_rdf_type,X100,uri_rdfs_Resource),inference(resolution,[status(thm)],[c131, c172])).
% 3.93/4.11  cnf(c468,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X353)|iext(X353,X354,uri_rdfs_Resource),inference(resolution,[status(thm)],[c460, c41])).
% 3.93/4.11  cnf(c473,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X351)|icext(X351,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c138, c93])).
% 3.93/4.11  cnf(c436,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X349)|iext(X349,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c136, c41])).
% 3.93/4.11  cnf(c470,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X348)|icext(X348,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c137, c93])).
% 3.93/4.11  cnf(c469,plain,~iext(uri_rdfs_range,uri_rdf_type,X347)|icext(X347,uri_rdfs_Resource),inference(resolution,[status(thm)],[c460, c67])).
% 3.93/4.11  cnf(c435,plain,~iext(uri_rdfs_subPropertyOf,X346,uri_rdfs_isDefinedBy)|iext(uri_rdfs_subPropertyOf,X346,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c136, c30])).
% 3.93/4.11  cnf(c437,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X345)|icext(X345,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c136, c67])).
% 3.93/4.11  cnf(c432,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X344)|icext(X344,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c136, c93])).
% 3.93/4.11  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.93/4.11  cnf(c135,plain,iext(uri_rdfs_domain,uri_rdfs_label,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_label_domain])).
% 3.93/4.11  cnf(c430,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X343)|iext(X343,uri_rdfs_label,uri_rdfs_Resource),inference(resolution,[status(thm)],[c135, c41])).
% 3.93/4.11  cnf(c429,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X341)|icext(X341,uri_rdfs_label),inference(resolution,[status(thm)],[c135, c93])).
% 3.93/4.11  cnf(c428,plain,~iext(uri_rdfs_range,uri_rdfs_range,X340)|icext(X340,uri_rdfs_Literal),inference(resolution,[status(thm)],[c134, c67])).
% 3.93/4.11  cnf(c427,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X339)|iext(X339,uri_rdfs_label,uri_rdfs_Literal),inference(resolution,[status(thm)],[c134, c41])).
% 3.93/4.11  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.93/4.11  cnf(c133,plain,iext(uri_rdfs_domain,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_seealso_domain])).
% 3.93/4.11  cnf(c424,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X338)|iext(X338,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(resolution,[status(thm)],[c133, c41])).
% 3.93/4.11  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.93/4.11  cnf(c132,plain,iext(uri_rdfs_range,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_seealso_range])).
% 3.93/4.11  cnf(c411,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X335)|iext(X335,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(resolution,[status(thm)],[c132, c41])).
% 3.93/4.11  cnf(c423,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X334)|icext(X334,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c133, c93])).
% 3.93/4.11  cnf(c410,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X332)|icext(X332,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c132, c93])).
% 3.93/4.11  cnf(c408,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X331)|iext(X331,uri_rdf_first,uri_rdf_List),inference(resolution,[status(thm)],[c122, c41])).
% 3.93/4.11  cnf(c407,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X329)|icext(X329,uri_rdf_first),inference(resolution,[status(thm)],[c122, c93])).
% 3.93/4.11  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.93/4.11  cnf(c121,plain,iext(uri_rdfs_range,uri_rdf_first,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_collection_first_range])).
% 3.93/4.11  cnf(c405,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X327)|iext(X327,uri_rdf_first,uri_rdfs_Resource),inference(resolution,[status(thm)],[c121, c41])).
% 3.93/4.11  cnf(c404,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X326)|icext(X326,uri_rdf_first),inference(resolution,[status(thm)],[c121, c93])).
% 3.93/4.11  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.93/4.11  cnf(c120,plain,iext(uri_rdfs_domain,uri_rdf_rest,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdfs_collection_rest_domain])).
% 3.93/4.11  cnf(c403,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X325)|icext(X325,uri_rdf_List),inference(resolution,[status(thm)],[c120, c67])).
% 3.93/4.11  cnf(c402,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X324)|iext(X324,uri_rdf_rest,uri_rdf_List),inference(resolution,[status(thm)],[c120, c41])).
% 3.93/4.11  cnf(c401,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X321)|icext(X321,uri_rdf_rest),inference(resolution,[status(thm)],[c120, c93])).
% 3.93/4.11  cnf(c399,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X320)|iext(X320,uri_rdf_rest,uri_rdf_List),inference(resolution,[status(thm)],[c119, c41])).
% 3.93/4.11  cnf(c393,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X319)|iext(X319,uri_rdf_Alt,uri_rdfs_Container),inference(resolution,[status(thm)],[c118, c41])).
% 3.93/4.11  cnf(c392,plain,~iext(uri_rdfs_subClassOf,X318,uri_rdf_Alt)|iext(uri_rdfs_subClassOf,X318,uri_rdfs_Container),inference(resolution,[status(thm)],[c118, c45])).
% 3.93/4.11  cnf(c398,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X316)|icext(X316,uri_rdf_rest),inference(resolution,[status(thm)],[c119, c93])).
% 3.93/4.11  cnf(c383,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X314)|iext(X314,uri_rdf_Bag,uri_rdfs_Container),inference(resolution,[status(thm)],[c117, c41])).
% 3.93/4.11  cnf(c390,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X313)|icext(X313,uri_rdf_Alt),inference(resolution,[status(thm)],[c118, c93])).
% 3.93/4.11  cnf(c382,plain,~iext(uri_rdfs_subClassOf,X311,uri_rdf_Bag)|iext(uri_rdfs_subClassOf,X311,uri_rdfs_Container),inference(resolution,[status(thm)],[c117, c45])).
% 3.93/4.11  cnf(c380,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X310)|icext(X310,uri_rdf_Bag),inference(resolution,[status(thm)],[c117, c93])).
% 3.93/4.11  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.93/4.11  cnf(c49,plain,iext(uri_rdfs_range,uri_rdfs_subClassOf,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_subclassof_range])).
% 3.93/4.11  cnf(c371,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X309)|icext(X309,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c93, c49])).
% 3.93/4.11  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.93/4.11  cnf(c24,plain,iext(uri_rdfs_range,uri_rdf_value,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_value_range])).
% 3.93/4.11  cnf(c370,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X308)|icext(X308,uri_rdf_value),inference(resolution,[status(thm)],[c93, c24])).
% 3.93/4.11  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.93/4.11  cnf(c111,plain,iext(uri_rdfs_range,uri_rdfs_member,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_member_range])).
% 3.93/4.11  cnf(c369,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X307)|icext(X307,uri_rdfs_member),inference(resolution,[status(thm)],[c93, c111])).
% 3.93/4.11  cnf(c19,plain,iext(uri_rdf_first,skolem0008,uri_ex_Z),inference(split_conjunct,[status(thm)],[c1])).
% 3.93/4.11  cnf(c368,plain,~iext(uri_rdfs_domain,uri_rdf_first,X306)|icext(X306,skolem0008),inference(resolution,[status(thm)],[c93, c19])).
% 3.93/4.11  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.93/4.11  cnf(c27,plain,iext(uri_rdfs_domain,uri_rdf_type,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_type_domain])).
% 3.93/4.11  cnf(c367,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X305)|icext(X305,uri_rdf_type),inference(resolution,[status(thm)],[c93, c27])).
% 3.93/4.11  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.93/4.11  cnf(c25,plain,iext(uri_rdfs_domain,uri_rdf_value,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_value_domain])).
% 3.93/4.11  cnf(c366,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X304)|icext(X304,uri_rdf_value),inference(resolution,[status(thm)],[c93, c25])).
% 3.93/4.11  cnf(c365,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X303)|icext(X303,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c93, c95])).
% 3.93/4.11  cnf(c20,plain,iext(uri_rdf_rest,skolem0008,uri_rdf_nil),inference(split_conjunct,[status(thm)],[c1])).
% 3.93/4.11  cnf(c364,plain,~iext(uri_rdfs_domain,uri_rdf_rest,X302)|icext(X302,skolem0008),inference(resolution,[status(thm)],[c93, c20])).
% 3.93/4.11  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.93/4.11  cnf(c34,plain,iext(uri_rdfs_range,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_subpropertyof_range])).
% 3.93/4.11  cnf(c363,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X301)|icext(X301,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c93, c34])).
% 3.93/4.11  cnf(c362,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X300)|icext(X300,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c93, c113])).
% 3.93/4.11  cnf(c361,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X299)|icext(X299,uri_rdf_type),inference(resolution,[status(thm)],[c93, c26])).
% 3.93/4.11  cnf(c17,plain,iext(uri_rdf_first,skolem0007,uri_ex_Y),inference(split_conjunct,[status(thm)],[c1])).
% 3.93/4.11  cnf(c360,plain,~iext(uri_rdfs_domain,uri_rdf_first,X298)|icext(X298,skolem0007),inference(resolution,[status(thm)],[c93, c17])).
% 3.93/4.11  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.93/4.11  cnf(c110,plain,iext(uri_rdfs_domain,uri_rdf__1,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_001])).
% 3.93/4.11  cnf(c359,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X297)|icext(X297,uri_rdf__1),inference(resolution,[status(thm)],[c93, c110])).
% 3.93/4.11  cnf(c358,plain,~iext(uri_rdfs_domain,uri_rdf_rest,X296)|icext(X296,skolem0007),inference(resolution,[status(thm)],[c93, c18])).
% 3.93/4.11  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.93/4.11  cnf(c112,plain,iext(uri_rdfs_domain,uri_rdfs_member,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_member_domain])).
% 3.93/4.11  cnf(c357,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X295)|icext(X295,uri_rdfs_member),inference(resolution,[status(thm)],[c93, c112])).
% 3.93/4.11  cnf(c356,plain,~iext(uri_rdfs_domain,uri_rdf_rest,X294)|icext(X294,skolem0006),inference(resolution,[status(thm)],[c93, c16])).
% 3.93/4.11  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.93/4.11  cnf(c107,plain,iext(uri_rdfs_range,uri_rdf__1,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_range_001])).
% 3.93/4.11  cnf(c355,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X293)|icext(X293,uri_rdf__1),inference(resolution,[status(thm)],[c93, c107])).
% 3.93/4.11  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.93/4.11  cnf(c105,plain,iext(uri_rdfs_range,uri_rdf__3,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_range_003])).
% 3.93/4.11  cnf(c354,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X292)|icext(X292,uri_rdf__3),inference(resolution,[status(thm)],[c93, c105])).
% 3.93/4.11  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.93/4.11  cnf(c109,plain,iext(uri_rdfs_domain,uri_rdf__2,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_002])).
% 3.93/4.11  cnf(c351,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X289)|icext(X289,uri_rdf__2),inference(resolution,[status(thm)],[c93, c109])).
% 3.93/4.11  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.93/4.11  cnf(c108,plain,iext(uri_rdfs_domain,uri_rdf__3,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_003])).
% 3.93/4.11  cnf(c350,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X288)|icext(X288,uri_rdf__3),inference(resolution,[status(thm)],[c93, c108])).
% 3.93/4.11  cnf(c348,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X286)|icext(X286,uri_skos_memberList),inference(resolution,[status(thm)],[c93, c2])).
% 3.93/4.11  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.93/4.11  cnf(c60,plain,iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_reification_predicate_range])).
% 3.93/4.11  cnf(c347,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X285)|icext(X285,uri_rdf_predicate),inference(resolution,[status(thm)],[c93, c60])).
% 3.93/4.11  cnf(c346,plain,~iext(uri_rdfs_domain,uri_skos_memberList,X284)|icext(X284,uri_ex_MyOrderedCollection),inference(resolution,[status(thm)],[c93, c14])).
% 3.93/4.11  cnf(c344,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X282)|icext(X282,uri_rdfs_domain),inference(resolution,[status(thm)],[c93, c88])).
% 3.93/4.11  cnf(c11,plain,iext(uri_rdf_first,skolem0005,uri_rdf_rest),inference(split_conjunct,[status(thm)],[c1])).
% 3.93/4.11  cnf(c341,plain,~iext(uri_rdfs_domain,uri_rdf_first,X279)|icext(X279,skolem0005),inference(resolution,[status(thm)],[c93, c11])).
% 3.93/4.11  cnf(c7,plain,iext(uri_rdf_rest,skolem0003,uri_rdf_nil),inference(split_conjunct,[status(thm)],[c1])).
% 3.93/4.11  cnf(c339,plain,~iext(uri_rdfs_domain,uri_rdf_rest,X277)|icext(X277,skolem0003),inference(resolution,[status(thm)],[c93, c7])).
% 3.93/4.11  cnf(c338,plain,~iext(uri_rdfs_domain,uri_rdf_rest,X276)|icext(X276,skolem0002),inference(resolution,[status(thm)],[c93, c5])).
% 3.93/4.11  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.93/4.11  cnf(c58,plain,iext(uri_rdfs_range,uri_rdf_subject,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_reification_subject_range])).
% 3.93/4.11  cnf(c337,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X275)|icext(X275,uri_rdf_subject),inference(resolution,[status(thm)],[c93, c58])).
% 3.93/4.11  cnf(c12,plain,iext(uri_rdf_rest,skolem0005,uri_rdf_nil),inference(split_conjunct,[status(thm)],[c1])).
% 3.93/4.11  cnf(c336,plain,~iext(uri_rdfs_domain,uri_rdf_rest,X274)|icext(X274,skolem0005),inference(resolution,[status(thm)],[c93, c12])).
% 3.93/4.11  cnf(c335,plain,~iext(uri_rdfs_domain,uri_rdf_rest,X273)|icext(X273,skolem0004),inference(resolution,[status(thm)],[c93, c10])).
% 3.93/4.11  cnf(c6,plain,iext(uri_rdf_first,skolem0003,uri_rdf_first),inference(split_conjunct,[status(thm)],[c1])).
% 3.93/4.11  cnf(c334,plain,~iext(uri_rdfs_domain,uri_rdf_first,X272)|icext(X272,skolem0003),inference(resolution,[status(thm)],[c93, c6])).
% 3.93/4.11  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.93/4.11  cnf(c106,plain,iext(uri_rdfs_range,uri_rdf__2,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_range_002])).
% 3.93/4.11  cnf(c333,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X271)|icext(X271,uri_rdf__2),inference(resolution,[status(thm)],[c93, c106])).
% 3.93/4.11  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.93/4.11  cnf(c59,plain,iext(uri_rdfs_domain,uri_rdf_subject,uri_rdfs_Statement),inference(split_conjunct,[status(thm)],[rdfs_reification_subject_domain])).
% 3.93/4.11  cnf(c332,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X270)|icext(X270,uri_rdf_subject),inference(resolution,[status(thm)],[c93, c59])).
% 3.93/4.11  cnf(c330,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X268)|icext(X268,uri_rdf_object),inference(resolution,[status(thm)],[c93, c63])).
% 3.93/4.11  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.93/4.11  cnf(c57,plain,iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_subclassof_domain])).
% 3.93/4.11  cnf(c329,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X267)|icext(X267,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c93, c57])).
% 3.93/4.11  cnf(c328,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X266)|icext(X266,uri_rdfs_Seq),inference(resolution,[status(thm)],[c93, c101])).
% 3.93/4.11  cnf(c8,plain,iext(uri_owl_propertyChainAxiom,skolem0001,skolem0004),inference(split_conjunct,[status(thm)],[c1])).
% 3.93/4.11  cnf(c327,plain,~iext(uri_rdfs_domain,uri_owl_propertyChainAxiom,X265)|icext(X265,skolem0001),inference(resolution,[status(thm)],[c93, c8])).
% 3.93/4.11  cnf(c326,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X264)|icext(X264,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c93, c100])).
% 3.93/4.11  cnf(c324,plain,~iext(uri_rdfs_domain,uri_owl_propertyChainAxiom,X262)|icext(X262,uri_skos_member),inference(resolution,[status(thm)],[c93, c3])).
% 3.93/4.11  cnf(c322,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X260)|icext(X260,uri_rdfs_range),inference(resolution,[status(thm)],[c93, c64])).
% 3.93/4.11  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.93/4.11  cnf(c42,plain,iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_subpropertyof_domain])).
% 3.93/4.11  cnf(c321,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X259)|icext(X259,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c93, c42])).
% 3.93/4.11  cnf(c316,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X258)|iext(X258,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),inference(resolution,[status(thm)],[c113, c41])).
% 3.93/4.11  cnf(c319,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X256)|icext(X256,uri_rdfs_range),inference(resolution,[status(thm)],[c93, c68])).
% 3.93/4.11  cnf(c315,plain,~iext(uri_rdfs_subClassOf,X255,uri_rdfs_ContainerMembershipProperty)|iext(uri_rdfs_subClassOf,X255,uri_rdf_Property),inference(resolution,[status(thm)],[c113, c45])).
% 3.93/4.11  cnf(c318,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X254)|icext(X254,uri_rdfs_domain),inference(factor,[status(thm)],[c93])).
% 3.93/4.11  cnf(c317,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X253)|icext(X253,uri_rdf_Property),inference(resolution,[status(thm)],[c113, c67])).
% 3.93/4.11  cnf(c310,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X251)|iext(X251,uri_rdfs_member,uri_rdfs_Resource),inference(resolution,[status(thm)],[c112, c41])).
% 3.93/4.11  cnf(c305,plain,~iext(uri_rdfs_range,uri_rdf_first,X247)|icext(X247,uri_ex_Z),inference(resolution,[status(thm)],[c67, c19])).
% 3.93/4.11  cnf(c302,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X244)|icext(X244,uri_rdfs_Class),inference(resolution,[status(thm)],[c67, c95])).
% 3.93/4.11  cnf(c300,plain,~iext(uri_rdfs_range,uri_rdfs_range,X242)|icext(X242,uri_rdf_Property),inference(resolution,[status(thm)],[c67, c34])).
% 3.93/4.11  cnf(c298,plain,~iext(uri_rdfs_range,uri_rdf_first,X240)|icext(X240,uri_ex_Y),inference(resolution,[status(thm)],[c67, c17])).
% 3.93/4.11  cnf(c292,plain,~iext(uri_rdfs_range,uri_rdf_first,X232)|icext(X232,uri_ex_X),inference(resolution,[status(thm)],[c67, c15])).
% 3.93/4.11  cnf(c466,plain,~iext(uri_rdfs_domain,uri_rdf_type,X229)|icext(X229,X228),inference(resolution,[status(thm)],[c460, c93])).
% 3.93/4.11  cnf(c289,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X218)|icext(X218,uri_rdfs_Resource),inference(resolution,[status(thm)],[c67, c108])).
% 3.93/4.11  cnf(c287,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X207)|icext(X207,skolem0001),inference(resolution,[status(thm)],[c67, c2])).
% 3.93/4.11  cnf(c56,plain,~iext(uri_rdfs_subClassOf,X82,X83)|~icext(X82,X84)|icext(X83,X84),inference(split_conjunct,[status(thm)],[c53])).
% 3.93/4.11  cnf(c389,plain,~icext(uri_rdf_Alt,X199)|icext(uri_rdfs_Container,X199),inference(resolution,[status(thm)],[c118, c56])).
% 3.93/4.11  cnf(c379,plain,~icext(uri_rdf_Bag,X198)|icext(uri_rdfs_Container,X198),inference(resolution,[status(thm)],[c117, c56])).
% 3.93/4.11  cnf(c285,plain,~iext(uri_rdfs_range,uri_skos_memberList,X197)|icext(X197,skolem0006),inference(resolution,[status(thm)],[c67, c14])).
% 3.93/4.11  cnf(c313,plain,~icext(uri_rdfs_ContainerMembershipProperty,X196)|icext(uri_rdf_Property,X196),inference(resolution,[status(thm)],[c113, c56])).
% 3.93/4.12  cnf(c282,plain,~iext(uri_rdfs_range,uri_rdf_type,X193)|icext(X193,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c67, c103])).
% 3.93/4.12  cnf(c280,plain,~iext(uri_rdfs_range,uri_rdf_first,X191)|icext(X191,uri_rdf_rest),inference(resolution,[status(thm)],[c67, c11])).
% 3.93/4.12  cnf(c275,plain,~iext(uri_rdfs_range,uri_rdf_rest,X186)|icext(X186,uri_rdf_nil),inference(resolution,[status(thm)],[c67, c12])).
% 3.93/4.12  cnf(c273,plain,~iext(uri_rdfs_range,uri_rdf_first,X184)|icext(X184,uri_rdf_first),inference(resolution,[status(thm)],[c67, c6])).
% 3.93/4.12  cnf(c272,plain,~iext(uri_rdfs_range,uri_rdfs_range,X183)|icext(X183,uri_rdfs_Resource),inference(resolution,[status(thm)],[c67, c106])).
% 3.93/4.12  cnf(c268,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X179)|icext(X179,uri_rdfs_Class),inference(resolution,[status(thm)],[c67, c57])).
% 3.93/4.12  cnf(c267,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X178)|icext(X178,uri_rdfs_Container),inference(resolution,[status(thm)],[c67, c101])).
% 3.93/4.12  cnf(c266,plain,~iext(uri_rdfs_range,uri_owl_propertyChainAxiom,X177)|icext(X177,skolem0004),inference(resolution,[status(thm)],[c67, c8])).
% 3.93/4.12  cnf(c1165,plain,icext(uri_rdf_Property,uri_rdfs_member),inference(resolution,[status(thm)],[c856, c130])).
% 3.93/4.12  cnf(c265,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X176)|icext(X176,uri_rdfs_Literal),inference(resolution,[status(thm)],[c67, c100])).
% 3.93/4.12  cnf(c264,plain,~iext(uri_rdfs_range,uri_rdf_first,X175)|icext(X175,skolem0001),inference(resolution,[status(thm)],[c67, c4])).
% 3.93/4.12  cnf(c263,plain,~iext(uri_rdfs_range,uri_owl_propertyChainAxiom,X174)|icext(X174,skolem0002),inference(resolution,[status(thm)],[c67, c3])).
% 3.93/4.12  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.93/4.12  cnf(c69,plain,iext(uri_rdf_type,uri_rdf_Property,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_property_type])).
% 3.93/4.12  cnf(c262,plain,~iext(uri_rdfs_range,uri_rdf_type,X173)|icext(X173,uri_rdfs_Class),inference(resolution,[status(thm)],[c67, c69])).
% 3.93/4.12  cnf(c1130,plain,icext(uri_rdf_Property,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c666, c130])).
% 3.93/4.12  cnf(c261,plain,~iext(uri_rdfs_range,uri_rdfs_range,X172)|icext(X172,uri_rdfs_Class),inference(resolution,[status(thm)],[c67, c64])).
% 3.93/4.12  cnf(c1113,plain,icext(uri_rdf_Property,uri_owl_propertyChainAxiom),inference(resolution,[status(thm)],[c657, c130])).
% 3.93/4.12  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.93/4.12  cnf(c99,plain,iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Datatype),inference(split_conjunct,[status(thm)],[rdfs_dat_xmlliteral_type])).
% 3.93/4.12  cnf(c259,plain,~iext(uri_rdfs_range,uri_rdf_type,X170)|icext(X170,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c67, c99])).
% 3.93/4.12  cnf(c258,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X169)|icext(X169,uri_rdf_Property),inference(resolution,[status(thm)],[c67, c68])).
% 3.93/4.12  cnf(c1095,plain,icext(uri_rdf_Property,uri_rdfs_domain),inference(resolution,[status(thm)],[c647, c130])).
% 3.93/4.12  cnf(c257,plain,~iext(uri_rdfs_range,uri_rdfs_range,X168)|icext(X168,X168),inference(factor,[status(thm)],[c67])).
% 3.93/4.12  cnf(c253,plain,~icext(uri_rdfs_Datatype,X167)|icext(uri_rdfs_Class,X167),inference(resolution,[status(thm)],[c56, c95])).
% 3.93/4.12  cnf(c1068,plain,icext(uri_rdf_Property,uri_rdfs_range),inference(resolution,[status(thm)],[c645, c130])).
% 3.93/4.12  cnf(c252,plain,~icext(uri_rdfs_Seq,X166)|icext(uri_rdfs_Container,X166),inference(resolution,[status(thm)],[c56, c101])).
% 3.93/4.12  cnf(c251,plain,~icext(uri_rdf_XMLLiteral,X165)|icext(uri_rdfs_Literal,X165),inference(resolution,[status(thm)],[c56, c100])).
% 3.93/4.12  cnf(c1042,plain,icext(uri_rdf_Property,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c643, c130])).
% 3.93/4.12  cnf(c230,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X164)|iext(X164,uri_rdfs_member,uri_rdfs_Resource),inference(resolution,[status(thm)],[c111, c41])).
% 3.93/4.12  cnf(c229,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X163)|iext(X163,uri_rdf__1,uri_rdfs_Resource),inference(resolution,[status(thm)],[c110, c41])).
% 3.93/4.12  cnf(c228,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X162)|iext(X162,uri_rdf__2,uri_rdfs_Resource),inference(resolution,[status(thm)],[c109, c41])).
% 3.93/4.12  cnf(c227,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X161)|iext(X161,uri_rdf__3,uri_rdfs_Resource),inference(resolution,[status(thm)],[c108, c41])).
% 3.93/4.12  cnf(c226,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X160)|iext(X160,uri_rdf__1,uri_rdfs_Resource),inference(resolution,[status(thm)],[c107, c41])).
% 3.93/4.12  cnf(c225,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X159)|iext(X159,uri_rdf__2,uri_rdfs_Resource),inference(resolution,[status(thm)],[c106, c41])).
% 3.93/4.12  cnf(c224,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X158)|iext(X158,uri_rdf__3,uri_rdfs_Resource),inference(resolution,[status(thm)],[c105, c41])).
% 3.93/4.12  cnf(c223,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X157)|iext(X157,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c104, c41])).
% 3.93/4.12  cnf(c222,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X156)|iext(X156,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c103, c41])).
% 3.93/4.12  cnf(c221,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X155)|iext(X155,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c102, c41])).
% 3.93/4.12  cnf(c959,plain,icext(uri_rdf_Property,uri_skos_memberList),inference(resolution,[status(thm)],[c506, c130])).
% 3.93/4.12  cnf(c220,plain,~iext(uri_rdfs_subClassOf,X154,uri_rdfs_Datatype)|iext(uri_rdfs_subClassOf,X154,uri_rdfs_Class),inference(resolution,[status(thm)],[c45, c95])).
% 3.93/4.12  cnf(c951,plain,icext(uri_rdf_Property,skolem0001),inference(resolution,[status(thm)],[c505, c130])).
% 3.93/4.12  cnf(c219,plain,~iext(uri_rdfs_subClassOf,X153,uri_rdfs_Seq)|iext(uri_rdfs_subClassOf,X153,uri_rdfs_Container),inference(resolution,[status(thm)],[c45, c101])).
% 3.93/4.12  cnf(c943,plain,icext(uri_rdf_Property,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c503, c130])).
% 3.93/4.12  cnf(c935,plain,icext(uri_rdf_Property,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c502, c130])).
% 3.93/4.12  cnf(c218,plain,~iext(uri_rdfs_subClassOf,X152,uri_rdf_XMLLiteral)|iext(uri_rdfs_subClassOf,X152,uri_rdfs_Literal),inference(resolution,[status(thm)],[c45, c100])).
% 3.93/4.12  cnf(c216,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X150)|iext(X150,uri_rdfs_Seq,uri_rdfs_Container),inference(resolution,[status(thm)],[c101, c41])).
% 3.93/4.12  cnf(c215,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X149)|iext(X149,uri_rdf_XMLLiteral,uri_rdfs_Literal),inference(resolution,[status(thm)],[c100, c41])).
% 3.93/4.12  cnf(c214,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X148)|iext(X148,uri_rdf_XMLLiteral,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c99, c41])).
% 3.93/4.12  cnf(c213,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X147)|iext(X147,uri_rdfs_Datatype,uri_rdfs_Class),inference(resolution,[status(thm)],[c95, c41])).
% 3.93/4.12  cnf(c212,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X146)|iext(X146,uri_rdfs_domain,uri_rdf_Property),inference(resolution,[status(thm)],[c94, c41])).
% 3.93/4.12  cnf(c211,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X145)|iext(X145,uri_rdfs_subClassOf,uri_rdfs_Class),inference(resolution,[status(thm)],[c41, c49])).
% 3.93/4.12  cnf(c210,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X144)|iext(X144,uri_rdf_value,uri_rdfs_Resource),inference(resolution,[status(thm)],[c41, c24])).
% 3.93/4.12  cnf(c209,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_first,X143)|iext(X143,skolem0008,uri_ex_Z),inference(resolution,[status(thm)],[c41, c19])).
% 3.93/4.12  cnf(c208,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X142)|iext(X142,uri_rdf_type,uri_rdfs_Resource),inference(resolution,[status(thm)],[c41, c27])).
% 3.93/4.12  cnf(c207,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X141)|iext(X141,uri_rdf_value,uri_rdfs_Resource),inference(resolution,[status(thm)],[c41, c25])).
% 3.93/4.12  cnf(c206,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X140)|iext(X140,skolem0008,uri_rdf_nil),inference(resolution,[status(thm)],[c41, c20])).
% 3.93/4.12  cnf(c205,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X139)|iext(X139,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c41, c34])).
% 3.93/4.12  cnf(c204,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X138)|iext(X138,uri_rdf_type,uri_rdfs_Class),inference(resolution,[status(thm)],[c41, c26])).
% 3.93/4.12  cnf(c203,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_first,X137)|iext(X137,skolem0007,uri_ex_Y),inference(resolution,[status(thm)],[c41, c17])).
% 3.93/4.12  cnf(c202,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X136)|iext(X136,skolem0007,skolem0008),inference(resolution,[status(thm)],[c41, c18])).
% 3.93/4.12  cnf(c201,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X135)|iext(X135,skolem0006,skolem0007),inference(resolution,[status(thm)],[c41, c16])).
% 3.93/4.12  cnf(c200,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_first,X134)|iext(X134,skolem0006,uri_ex_X),inference(resolution,[status(thm)],[c41, c15])).
% 3.93/4.12  cnf(c199,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X133)|iext(X133,uri_ex_MyOrderedCollection,uri_skos_OrderedCollection),inference(resolution,[status(thm)],[c41, c13])).
% 3.93/4.12  cnf(c198,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X132)|iext(X132,uri_skos_memberList,skolem0001),inference(resolution,[status(thm)],[c41, c2])).
% 3.93/4.12  cnf(c197,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X131)|iext(X131,uri_rdf_predicate,uri_rdfs_Resource),inference(resolution,[status(thm)],[c41, c60])).
% 3.93/4.12  cnf(c195,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X129)|iext(X129,uri_rdfs_domain,uri_rdfs_Class),inference(resolution,[status(thm)],[c41, c88])).
% 3.93/4.12  cnf(c194,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X128)|iext(X128,uri_rdf_predicate,uri_rdfs_Statement),inference(resolution,[status(thm)],[c41, c61])).
% 3.93/4.12  cnf(c193,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_first,X127)|iext(X127,skolem0005,uri_rdf_rest),inference(resolution,[status(thm)],[c41, c11])).
% 3.93/4.12  cnf(c192,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X126)|iext(X126,skolem0003,uri_rdf_nil),inference(resolution,[status(thm)],[c41, c7])).
% 3.93/4.12  cnf(c191,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X125)|iext(X125,skolem0002,skolem0003),inference(resolution,[status(thm)],[c41, c5])).
% 3.93/4.12  cnf(c190,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X124)|iext(X124,uri_rdf_subject,uri_rdfs_Resource),inference(resolution,[status(thm)],[c41, c58])).
% 3.93/4.12  cnf(c189,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X123)|iext(X123,skolem0005,uri_rdf_nil),inference(resolution,[status(thm)],[c41, c12])).
% 3.93/4.12  cnf(c188,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X122)|iext(X122,skolem0004,skolem0005),inference(resolution,[status(thm)],[c41, c10])).
% 3.93/4.12  cnf(c187,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_first,X121)|iext(X121,skolem0003,uri_rdf_first),inference(resolution,[status(thm)],[c41, c6])).
% 3.93/4.12  cnf(c186,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X120)|iext(X120,uri_rdf_subject,uri_rdfs_Statement),inference(resolution,[status(thm)],[c41, c59])).
% 3.93/4.12  cnf(c185,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_first,X119)|iext(X119,skolem0004,skolem0001),inference(resolution,[status(thm)],[c41, c9])).
% 3.93/4.12  cnf(c184,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X118)|iext(X118,uri_rdf_object,uri_rdfs_Statement),inference(resolution,[status(thm)],[c41, c63])).
% 3.93/4.12  cnf(c183,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X117)|iext(X117,uri_rdfs_subClassOf,uri_rdfs_Class),inference(resolution,[status(thm)],[c41, c57])).
% 3.93/4.12  cnf(c182,plain,~iext(uri_rdfs_subPropertyOf,uri_owl_propertyChainAxiom,X116)|iext(X116,skolem0001,skolem0004),inference(resolution,[status(thm)],[c41, c8])).
% 3.93/4.12  cnf(c181,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_first,X115)|iext(X115,skolem0002,skolem0001),inference(resolution,[status(thm)],[c41, c4])).
% 3.93/4.12  cnf(c180,plain,~iext(uri_rdfs_subPropertyOf,uri_owl_propertyChainAxiom,X114)|iext(X114,uri_skos_member,skolem0002),inference(resolution,[status(thm)],[c41, c3])).
% 3.93/4.12  cnf(c179,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X113)|iext(X113,uri_rdf_Property,uri_rdfs_Class),inference(resolution,[status(thm)],[c41, c69])).
% 3.93/4.12  cnf(c178,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X112)|iext(X112,uri_rdfs_range,uri_rdfs_Class),inference(resolution,[status(thm)],[c41, c64])).
% 3.93/4.12  cnf(c177,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X111)|iext(X111,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c41, c42])).
% 3.93/4.12  cnf(c176,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X110)|iext(X110,uri_rdfs_range,uri_rdf_Property),inference(resolution,[status(thm)],[c41, c68])).
% 3.93/4.12  cnf(c175,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X109)|iext(X109,uri_rdfs_subPropertyOf,X109),inference(factor,[status(thm)],[c41])).
% 3.93/4.12  cnf(c169,plain,~iext(uri_rdfs_subPropertyOf,X108,uri_skos_memberList)|iext(uri_rdfs_subPropertyOf,X108,skolem0001),inference(resolution,[status(thm)],[c30, c2])).
% 3.93/4.12  cnf(c556,plain,icext(uri_rdf_Property,uri_rdf_first),inference(resolution,[status(thm)],[c157, c130])).
% 3.93/4.12  cnf(c551,plain,icext(uri_rdf_List,uri_rdf_nil),inference(resolution,[status(thm)],[c156, c130])).
% 3.93/4.12  cnf(c543,plain,icext(uri_rdf_Property,uri_rdf_rest),inference(resolution,[status(thm)],[c155, c130])).
% 3.93/4.12  cnf(c535,plain,icext(uri_rdf_Property,uri_rdf__1),inference(resolution,[status(thm)],[c154, c130])).
% 3.93/4.12  cnf(c527,plain,icext(uri_rdf_Property,uri_rdf__2),inference(resolution,[status(thm)],[c153, c130])).
% 3.93/4.12  cnf(c519,plain,icext(uri_rdf_Property,uri_rdf__3),inference(resolution,[status(thm)],[c152, c130])).
% 3.93/4.12  cnf(c511,plain,icext(uri_rdf_Property,uri_rdf_object),inference(resolution,[status(thm)],[c151, c130])).
% 3.93/4.12  cnf(c497,plain,icext(uri_rdf_Property,uri_rdf_value),inference(resolution,[status(thm)],[c150, c130])).
% 3.93/4.12  cnf(c490,plain,icext(uri_rdf_Property,uri_rdf_subject),inference(resolution,[status(thm)],[c149, c130])).
% 3.93/4.12  cnf(c483,plain,icext(uri_rdf_Property,uri_rdf_type),inference(resolution,[status(thm)],[c141, c130])).
% 3.93/4.12  cnf(c444,plain,icext(uri_skos_OrderedCollection,uri_ex_MyOrderedCollection),inference(resolution,[status(thm)],[c130, c13])).
% 3.93/4.12  cnf(c439,plain,icext(uri_rdfs_Datatype,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c130, c99])).
% 3.93/4.12  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.93/4.12  fof(c96,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.93/4.12  fof(c97,plain,(![X39]:(~icext(uri_rdfs_Datatype,X39)|iext(uri_rdfs_subClassOf,X39,uri_rdfs_Literal))),inference(variable_rename,[status(thm)],[c96])).
% 3.93/4.12  cnf(c98,plain,~icext(uri_rdfs_Datatype,X93)|iext(uri_rdfs_subClassOf,X93,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[c97])).
% 3.93/4.12  cnf(c372,plain,icext(uri_rdfs_Class,uri_rdf_Property),inference(resolution,[status(thm)],[c312, c86])).
% 3.93/4.12  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.93/4.12  fof(c70,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.93/4.12  fof(c71,plain,((![X]:(~lv(X)|icext(uri_rdfs_Literal,X)))&(![X]:(~icext(uri_rdfs_Literal,X)|lv(X)))),inference(shift_quantors,[status(thm)],[c70])).
% 3.93/4.12  fof(c73,plain,(![X29]:(![X30]:((~lv(X29)|icext(uri_rdfs_Literal,X29))&(~icext(uri_rdfs_Literal,X30)|lv(X30))))),inference(shift_quantors,[status(thm)],[fof(c72,plain,((![X29]:(~lv(X29)|icext(uri_rdfs_Literal,X29)))&(![X30]:(~icext(uri_rdfs_Literal,X30)|lv(X30)))),inference(variable_rename,[status(thm)],[c71])).])).
% 3.93/4.12  cnf(c75,plain,~icext(uri_rdfs_Literal,X62)|lv(X62),inference(split_conjunct,[status(thm)],[c73])).
% 3.93/4.12  cnf(c74,plain,~lv(X61)|icext(uri_rdfs_Literal,X61),inference(split_conjunct,[status(thm)],[c73])).
% 3.93/4.12  fof(testcase_conclusion_fullish_022_List_Member_Access,conjecture,((iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_X)&iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_Y))&iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_Z)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', testcase_conclusion_fullish_022_List_Member_Access)).
% 3.93/4.12  fof(c21,negated_conjecture,(~((iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_X)&iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_Y))&iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_Z))),inference(assume_negation,[status(cth)],[testcase_conclusion_fullish_022_List_Member_Access])).
% 3.93/4.12  fof(c22,negated_conjecture,((~iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_X)|~iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_Y))|~iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_Z)),inference(fof_nnf,[status(thm)],[c21])).
% 3.93/4.12  cnf(c23,negated_conjecture,~iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_X)|~iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_Y)|~iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_Z),inference(split_conjunct,[status(thm)],[c22])).
% 3.93/4.12  % SZS output end Saturation
% 3.93/4.12  
% 3.93/4.12  % Initial clauses    : 109
% 3.93/4.12  % Processed clauses  : 635
% 3.93/4.12  % Factors computed   : 5
% 3.93/4.12  % Resolvents computed: 1454
% 3.93/4.12  % Tautologies deleted: 52
% 3.93/4.12  % Forward subsumed   : 881
% 3.93/4.12  % Backward subsumed  : 1
% 3.93/4.12  % -------- CPU Time ---------
% 3.93/4.12  % User time          : 3.761 s
% 3.93/4.12  % System time        : 0.014 s
% 3.93/4.12  % Total time         : 3.775 s
%------------------------------------------------------------------------------