PyRes---1.5.CSA-Sat.s

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

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

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13  % Problem  : SWB026+4 : TPTP v8.1.2. Released v5.2.0.
% 0.07/0.14  % Command  : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35  % Computer : n015.cluster.edu
% 0.14/0.35  % Model    : x86_64 x86_64
% 0.14/0.35  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35  % Memory   : 8042.1875MB
% 0.14/0.35  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35  % CPULimit : 300
% 0.14/0.35  % WCLimit  : 300
% 0.14/0.35  % DateTime : Wed May  8 22:15:38 EDT 2024
% 0.14/0.35  % CPUTime  : 
% 3.32/3.54  % Version:  1.5
% 3.32/3.54  % SZS status CounterSatisfiable
% 3.32/3.54  % SZS output start Saturation
% 3.32/3.54  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/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_subpropertyof_main)).
% 3.32/3.54  fof(c24,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.32/3.54  fof(c26,plain,(![X10]:(![X11]:(![X12]:(![X13]:(~iext(uri_rdfs_subPropertyOf,X10,X11)|((ip(X10)&ip(X11))&(~iext(X10,X12,X13)|iext(X11,X12,X13)))))))),inference(shift_quantors,[status(thm)],[fof(c25,plain,(![X10]:(![X11]:(~iext(uri_rdfs_subPropertyOf,X10,X11)|((ip(X10)&ip(X11))&(![X12]:(![X13]:(~iext(X10,X12,X13)|iext(X11,X12,X13)))))))),inference(variable_rename,[status(thm)],[c24])).])).
% 3.32/3.54  fof(c27,plain,(![X10]:(![X11]:(![X12]:(![X13]:(((~iext(uri_rdfs_subPropertyOf,X10,X11)|ip(X10))&(~iext(uri_rdfs_subPropertyOf,X10,X11)|ip(X11)))&(~iext(uri_rdfs_subPropertyOf,X10,X11)|(~iext(X10,X12,X13)|iext(X11,X12,X13)))))))),inference(distribute,[status(thm)],[c26])).
% 3.32/3.54  cnf(c30,plain,~iext(uri_rdfs_subPropertyOf,X67,X68)|~iext(X67,X66,X69)|iext(X68,X66,X69),inference(split_conjunct,[status(thm)],[c27])).
% 3.32/3.54  fof(rdfs_subpropertyof_reflex,axiom,(![P]:(ip(P)=>iext(uri_rdfs_subPropertyOf,P,P))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_subpropertyof_reflex)).
% 3.32/3.54  fof(c20,plain,(![P]:(~ip(P)|iext(uri_rdfs_subPropertyOf,P,P))),inference(fof_nnf,[status(thm)],[rdfs_subpropertyof_reflex])).
% 3.32/3.54  fof(c21,plain,(![X9]:(~ip(X9)|iext(uri_rdfs_subPropertyOf,X9,X9))),inference(variable_rename,[status(thm)],[c20])).
% 3.32/3.54  cnf(c22,plain,~ip(X54)|iext(uri_rdfs_subPropertyOf,X54,X54),inference(split_conjunct,[status(thm)],[c21])).
% 3.32/3.54  fof(rdf_type_ip,axiom,(![P]:(iext(uri_rdf_type,P,uri_rdf_Property)<=>ip(P))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdf_type_ip)).
% 3.32/3.54  fof(c132,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.32/3.54  fof(c133,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)],[c132])).
% 3.32/3.54  fof(c135,plain,(![X42]:(![X43]:((~iext(uri_rdf_type,X42,uri_rdf_Property)|ip(X42))&(~ip(X43)|iext(uri_rdf_type,X43,uri_rdf_Property))))),inference(shift_quantors,[status(thm)],[fof(c134,plain,((![X42]:(~iext(uri_rdf_type,X42,uri_rdf_Property)|ip(X42)))&(![X43]:(~ip(X43)|iext(uri_rdf_type,X43,uri_rdf_Property)))),inference(variable_rename,[status(thm)],[c133])).])).
% 3.32/3.54  cnf(c136,plain,~iext(uri_rdf_type,X98,uri_rdf_Property)|ip(X98),inference(split_conjunct,[status(thm)],[c135])).
% 3.32/3.54  fof(rdfs_cext_def,axiom,(![X]:(![C]:(iext(uri_rdf_type,X,C)<=>icext(C,X)))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_cext_def)).
% 3.32/3.54  fof(c115,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.32/3.54  fof(c116,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)],[c115])).
% 3.32/3.54  fof(c118,plain,(![X38]:(![X39]:(![X40]:(![X41]:((~iext(uri_rdf_type,X38,X39)|icext(X39,X38))&(~icext(X41,X40)|iext(uri_rdf_type,X40,X41))))))),inference(shift_quantors,[status(thm)],[fof(c117,plain,((![X38]:(![X39]:(~iext(uri_rdf_type,X38,X39)|icext(X39,X38))))&(![X40]:(![X41]:(~icext(X41,X40)|iext(uri_rdf_type,X40,X41))))),inference(variable_rename,[status(thm)],[c116])).])).
% 3.32/3.54  cnf(c120,plain,~icext(X94,X95)|iext(uri_rdf_type,X95,X94),inference(split_conjunct,[status(thm)],[c118])).
% 3.32/3.54  fof(rdfs_range_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_range,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_range_domain)).
% 3.32/3.54  cnf(c57,plain,iext(uri_rdfs_domain,uri_rdfs_range,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_range_domain])).
% 3.32/3.54  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/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_domain_main)).
% 3.32/3.54  fof(c78,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.32/3.54  fof(c79,plain,(![P]:(![C]:(![X]:((~iext(uri_rdfs_domain,P,C)|(![Y]:~iext(P,X,Y)))|icext(C,X))))),inference(shift_quantors,[status(thm)],[c78])).
% 3.32/3.54  fof(c81,plain,(![X31]:(![X32]:(![X33]:(![X34]:((~iext(uri_rdfs_domain,X31,X32)|~iext(X31,X33,X34))|icext(X32,X33)))))),inference(shift_quantors,[status(thm)],[fof(c80,plain,(![X31]:(![X32]:(![X33]:((~iext(uri_rdfs_domain,X31,X32)|(![X34]:~iext(X31,X33,X34)))|icext(X32,X33))))),inference(variable_rename,[status(thm)],[c79])).])).
% 3.32/3.54  cnf(c82,plain,~iext(uri_rdfs_domain,X85,X86)|~iext(X85,X87,X88)|icext(X86,X87),inference(split_conjunct,[status(thm)],[c81])).
% 3.32/3.54  fof(rdfs_annotation_comment_range,axiom,iext(uri_rdfs_range,uri_rdfs_comment,uri_rdfs_Literal),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_comment_range)).
% 3.32/3.54  cnf(c128,plain,iext(uri_rdfs_range,uri_rdfs_comment,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[rdfs_annotation_comment_range])).
% 3.32/3.54  cnf(c425,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X317)|icext(X317,uri_rdfs_comment),inference(resolution,[status(thm)],[c128, c82])).
% 3.32/3.54  cnf(c1312,plain,icext(uri_rdf_Property,uri_rdfs_comment),inference(resolution,[status(thm)],[c425, c57])).
% 3.32/3.54  cnf(c1313,plain,iext(uri_rdf_type,uri_rdfs_comment,uri_rdf_Property),inference(resolution,[status(thm)],[c1312, c120])).
% 3.32/3.54  cnf(c1317,plain,ip(uri_rdfs_comment),inference(resolution,[status(thm)],[c1313, c136])).
% 3.32/3.54  cnf(c1322,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_comment,uri_rdfs_comment),inference(resolution,[status(thm)],[c1317, c22])).
% 3.32/3.54  cnf(c1329,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X653)|iext(X653,uri_rdfs_comment,uri_rdfs_comment),inference(resolution,[status(thm)],[c1322, c30])).
% 3.32/3.54  cnf(c1319,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X651)|iext(X651,uri_rdfs_comment,uri_rdf_Property),inference(resolution,[status(thm)],[c1313, c30])).
% 3.32/3.54  fof(rdfs_annotation_label_range,axiom,iext(uri_rdfs_range,uri_rdfs_label,uri_rdfs_Literal),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_label_range)).
% 3.32/3.54  cnf(c123,plain,iext(uri_rdfs_range,uri_rdfs_label,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[rdfs_annotation_label_range])).
% 3.32/3.54  cnf(c377,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X300)|icext(X300,uri_rdfs_label),inference(resolution,[status(thm)],[c123, c82])).
% 3.32/3.54  cnf(c1282,plain,icext(uri_rdf_Property,uri_rdfs_label),inference(resolution,[status(thm)],[c377, c57])).
% 3.32/3.54  cnf(c1283,plain,iext(uri_rdf_type,uri_rdfs_label,uri_rdf_Property),inference(resolution,[status(thm)],[c1282, c120])).
% 3.32/3.54  cnf(c1288,plain,ip(uri_rdfs_label),inference(resolution,[status(thm)],[c1283, c136])).
% 3.32/3.54  cnf(c1292,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_label,uri_rdfs_label),inference(resolution,[status(thm)],[c1288, c22])).
% 3.32/3.54  cnf(c1300,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X650)|iext(X650,uri_rdfs_label,uri_rdfs_label),inference(resolution,[status(thm)],[c1292, c30])).
% 3.32/3.54  cnf(c1290,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X648)|iext(X648,uri_rdfs_label,uri_rdf_Property),inference(resolution,[status(thm)],[c1283, c30])).
% 3.32/3.54  fof(rdfs_subclassof_reflex,axiom,(![C]:(ic(C)=>iext(uri_rdfs_subClassOf,C,C))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_subclassof_reflex)).
% 3.32/3.54  fof(c35,plain,(![C]:(~ic(C)|iext(uri_rdfs_subClassOf,C,C))),inference(fof_nnf,[status(thm)],[rdfs_subclassof_reflex])).
% 3.32/3.54  fof(c36,plain,(![X17]:(~ic(X17)|iext(uri_rdfs_subClassOf,X17,X17))),inference(variable_rename,[status(thm)],[c35])).
% 3.32/3.54  cnf(c37,plain,~ic(X73)|iext(uri_rdfs_subClassOf,X73,X73),inference(split_conjunct,[status(thm)],[c36])).
% 3.32/3.54  fof(rdfs_ic_def,axiom,(![X]:(ic(X)<=>icext(uri_rdfs_Class,X))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_ic_def)).
% 3.32/3.54  fof(c71,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.32/3.54  fof(c72,plain,((![X]:(~ic(X)|icext(uri_rdfs_Class,X)))&(![X]:(~icext(uri_rdfs_Class,X)|ic(X)))),inference(shift_quantors,[status(thm)],[c71])).
% 3.32/3.54  fof(c74,plain,(![X29]:(![X30]:((~ic(X29)|icext(uri_rdfs_Class,X29))&(~icext(uri_rdfs_Class,X30)|ic(X30))))),inference(shift_quantors,[status(thm)],[fof(c73,plain,((![X29]:(~ic(X29)|icext(uri_rdfs_Class,X29)))&(![X30]:(~icext(uri_rdfs_Class,X30)|ic(X30)))),inference(variable_rename,[status(thm)],[c72])).])).
% 3.32/3.54  cnf(c76,plain,~icext(uri_rdfs_Class,X65)|ic(X65),inference(split_conjunct,[status(thm)],[c74])).
% 3.32/3.54  fof(rdfs_range_range,axiom,iext(uri_rdfs_range,uri_rdfs_range,uri_rdfs_Class),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_range_range)).
% 3.32/3.54  cnf(c53,plain,iext(uri_rdfs_range,uri_rdfs_range,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_range_range])).
% 3.32/3.54  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/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_range_main)).
% 3.32/3.54  fof(c54,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.32/3.54  fof(c55,plain,(![X21]:(![X22]:(![X23]:(![X24]:((~iext(uri_rdfs_range,X21,X22)|~iext(X21,X23,X24))|icext(X22,X24)))))),inference(variable_rename,[status(thm)],[c54])).
% 3.32/3.54  cnf(c56,plain,~iext(uri_rdfs_range,X84,X81)|~iext(X84,X83,X82)|icext(X81,X82),inference(split_conjunct,[status(thm)],[c55])).
% 3.32/3.54  fof(rdfs_collection_rest_range,axiom,iext(uri_rdfs_range,uri_rdf_rest,uri_rdf_List),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_collection_rest_range)).
% 3.32/3.54  cnf(c108,plain,iext(uri_rdfs_range,uri_rdf_rest,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdfs_collection_rest_range])).
% 3.32/3.54  cnf(c350,plain,~iext(uri_rdfs_range,uri_rdfs_range,X280)|icext(X280,uri_rdf_List),inference(resolution,[status(thm)],[c108, c56])).
% 3.32/3.54  cnf(c1242,plain,icext(uri_rdfs_Class,uri_rdf_List),inference(resolution,[status(thm)],[c350, c53])).
% 3.32/3.54  cnf(c1245,plain,ic(uri_rdf_List),inference(resolution,[status(thm)],[c1242, c76])).
% 3.32/3.54  cnf(c1247,plain,iext(uri_rdfs_subClassOf,uri_rdf_List,uri_rdf_List),inference(resolution,[status(thm)],[c1245, c37])).
% 3.32/3.54  cnf(c1271,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X647)|iext(X647,uri_rdf_List,uri_rdf_List),inference(resolution,[status(thm)],[c1247, c30])).
% 3.32/3.54  fof(rdfs_class_instsub_resource,axiom,(![C]:(ic(C)=>iext(uri_rdfs_subClassOf,C,uri_rdfs_Resource))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_class_instsub_resource)).
% 3.32/3.54  fof(c112,plain,(![C]:(~ic(C)|iext(uri_rdfs_subClassOf,C,uri_rdfs_Resource))),inference(fof_nnf,[status(thm)],[rdfs_class_instsub_resource])).
% 3.32/3.54  fof(c113,plain,(![X37]:(~ic(X37)|iext(uri_rdfs_subClassOf,X37,uri_rdfs_Resource))),inference(variable_rename,[status(thm)],[c112])).
% 3.32/3.54  cnf(c114,plain,~ic(X91)|iext(uri_rdfs_subClassOf,X91,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[c113])).
% 3.32/3.54  cnf(c1246,plain,iext(uri_rdfs_subClassOf,uri_rdf_List,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1245, c114])).
% 3.32/3.54  cnf(c1262,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X645)|iext(X645,uri_rdf_List,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1246, c30])).
% 3.32/3.54  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/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_subclassof_trans)).
% 3.32/3.54  fof(c32,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.32/3.54  fof(c33,plain,(![X14]:(![X15]:(![X16]:((~iext(uri_rdfs_subClassOf,X14,X15)|~iext(uri_rdfs_subClassOf,X15,X16))|iext(uri_rdfs_subClassOf,X14,X16))))),inference(variable_rename,[status(thm)],[c32])).
% 3.32/3.54  cnf(c34,plain,~iext(uri_rdfs_subClassOf,X70,X71)|~iext(uri_rdfs_subClassOf,X71,X72)|iext(uri_rdfs_subClassOf,X70,X72),inference(split_conjunct,[status(thm)],[c33])).
% 3.32/3.54  cnf(c1255,plain,~iext(uri_rdfs_subClassOf,X644,uri_rdf_List)|iext(uri_rdfs_subClassOf,X644,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1246, c34])).
% 3.32/3.54  cnf(c1244,plain,iext(uri_rdf_type,uri_rdf_List,uri_rdfs_Class),inference(resolution,[status(thm)],[c1242, c120])).
% 3.32/3.54  cnf(c1253,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X643)|iext(X643,uri_rdf_List,uri_rdfs_Class),inference(resolution,[status(thm)],[c1244, c30])).
% 3.32/3.54  fof(rdfs_collection_rest_domain,axiom,iext(uri_rdfs_domain,uri_rdf_rest,uri_rdf_List),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_collection_rest_domain)).
% 3.32/3.54  cnf(c109,plain,iext(uri_rdfs_domain,uri_rdf_rest,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdfs_collection_rest_domain])).
% 3.32/3.54  fof(testcase_premise_fullish_026_Inferred_Property_Characteristics_I,axiom,(?[BNODE_x1]:(?[BNODE_x2]:(?[BNODE_l1]:(?[BNODE_l2]:(((((((iext(uri_rdfs_domain,uri_ex_p,BNODE_x1)&iext(uri_owl_oneOf,BNODE_x1,BNODE_l1))&iext(uri_rdf_first,BNODE_l1,uri_ex_w))&iext(uri_rdf_rest,BNODE_l1,uri_rdf_nil))&iext(uri_rdfs_range,uri_ex_p,BNODE_x2))&iext(uri_owl_oneOf,BNODE_x2,BNODE_l2))&iext(uri_rdf_first,BNODE_l2,uri_ex_u))&iext(uri_rdf_rest,BNODE_l2,uri_rdf_nil)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', testcase_premise_fullish_026_Inferred_Property_Characteristics_I)).
% 3.32/3.54  fof(c0,plain,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(((((((iext(uri_rdfs_domain,uri_ex_p,X2)&iext(uri_owl_oneOf,X2,X4))&iext(uri_rdf_first,X4,uri_ex_w))&iext(uri_rdf_rest,X4,uri_rdf_nil))&iext(uri_rdfs_range,uri_ex_p,X3))&iext(uri_owl_oneOf,X3,X5))&iext(uri_rdf_first,X5,uri_ex_u))&iext(uri_rdf_rest,X5,uri_rdf_nil)))))),inference(variable_rename,[status(thm)],[testcase_premise_fullish_026_Inferred_Property_Characteristics_I])).
% 3.32/3.54  fof(c1,plain,(((((((iext(uri_rdfs_domain,uri_ex_p,skolem0001)&iext(uri_owl_oneOf,skolem0001,skolem0003))&iext(uri_rdf_first,skolem0003,uri_ex_w))&iext(uri_rdf_rest,skolem0003,uri_rdf_nil))&iext(uri_rdfs_range,uri_ex_p,skolem0002))&iext(uri_owl_oneOf,skolem0002,skolem0004))&iext(uri_rdf_first,skolem0004,uri_ex_u))&iext(uri_rdf_rest,skolem0004,uri_rdf_nil)),inference(skolemize,[status(esa)],[c0])).
% 3.32/3.54  cnf(c9,plain,iext(uri_rdf_rest,skolem0004,uri_rdf_nil),inference(split_conjunct,[status(thm)],[c1])).
% 3.32/3.54  cnf(c313,plain,~iext(uri_rdfs_domain,uri_rdf_rest,X262)|icext(X262,skolem0004),inference(resolution,[status(thm)],[c82, c9])).
% 3.32/3.54  cnf(c1222,plain,icext(uri_rdf_List,skolem0004),inference(resolution,[status(thm)],[c313, c109])).
% 3.32/3.54  cnf(c1223,plain,iext(uri_rdf_type,skolem0004,uri_rdf_List),inference(resolution,[status(thm)],[c1222, c120])).
% 3.32/3.54  cnf(c1228,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X642)|iext(X642,skolem0004,uri_rdf_List),inference(resolution,[status(thm)],[c1223, c30])).
% 3.32/3.54  cnf(c5,plain,iext(uri_rdf_rest,skolem0003,uri_rdf_nil),inference(split_conjunct,[status(thm)],[c1])).
% 3.32/3.54  cnf(c305,plain,~iext(uri_rdfs_domain,uri_rdf_rest,X254)|icext(X254,skolem0003),inference(resolution,[status(thm)],[c82, c5])).
% 3.32/3.54  cnf(c1210,plain,icext(uri_rdf_List,skolem0003),inference(resolution,[status(thm)],[c305, c109])).
% 3.32/3.54  cnf(c1211,plain,iext(uri_rdf_type,skolem0003,uri_rdf_List),inference(resolution,[status(thm)],[c1210, c120])).
% 3.32/3.54  cnf(c1216,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X641)|iext(X641,skolem0003,uri_rdf_List),inference(resolution,[status(thm)],[c1211, c30])).
% 3.32/3.54  fof(rdfs_domain_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_domain_domain)).
% 3.32/3.54  cnf(c83,plain,iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_domain_domain])).
% 3.32/3.54  cnf(c2,plain,iext(uri_rdfs_domain,uri_ex_p,skolem0001),inference(split_conjunct,[status(thm)],[c1])).
% 3.32/3.54  cnf(c289,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X238)|icext(X238,uri_ex_p),inference(resolution,[status(thm)],[c82, c2])).
% 3.32/3.54  cnf(c1181,plain,icext(uri_rdf_Property,uri_ex_p),inference(resolution,[status(thm)],[c289, c83])).
% 3.32/3.54  cnf(c1183,plain,iext(uri_rdf_type,uri_ex_p,uri_rdf_Property),inference(resolution,[status(thm)],[c1181, c120])).
% 3.32/3.54  cnf(c1187,plain,ip(uri_ex_p),inference(resolution,[status(thm)],[c1183, c136])).
% 3.32/3.54  cnf(c1191,plain,iext(uri_rdfs_subPropertyOf,uri_ex_p,uri_ex_p),inference(resolution,[status(thm)],[c1187, c22])).
% 3.32/3.55  cnf(c1199,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X640)|iext(X640,uri_ex_p,uri_ex_p),inference(resolution,[status(thm)],[c1191, c30])).
% 3.32/3.55  cnf(c1189,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X638)|iext(X638,uri_ex_p,uri_rdf_Property),inference(resolution,[status(thm)],[c1183, c30])).
% 3.32/3.55  fof(rdfs_reification_predicate_domain,axiom,iext(uri_rdfs_domain,uri_rdf_predicate,uri_rdfs_Statement),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_reification_predicate_domain)).
% 3.32/3.55  cnf(c50,plain,iext(uri_rdfs_domain,uri_rdf_predicate,uri_rdfs_Statement),inference(split_conjunct,[status(thm)],[rdfs_reification_predicate_domain])).
% 3.32/3.55  cnf(c283,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X232)|icext(X232,uri_rdf_predicate),inference(resolution,[status(thm)],[c82, c50])).
% 3.32/3.55  cnf(c1160,plain,icext(uri_rdf_Property,uri_rdf_predicate),inference(resolution,[status(thm)],[c283, c83])).
% 3.32/3.55  cnf(c1161,plain,iext(uri_rdf_type,uri_rdf_predicate,uri_rdf_Property),inference(resolution,[status(thm)],[c1160, c120])).
% 3.32/3.55  cnf(c1165,plain,ip(uri_rdf_predicate),inference(resolution,[status(thm)],[c1161, c136])).
% 3.32/3.55  cnf(c1170,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_predicate,uri_rdf_predicate),inference(resolution,[status(thm)],[c1165, c22])).
% 3.32/3.55  cnf(c1178,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X637)|iext(X637,uri_rdf_predicate,uri_rdf_predicate),inference(resolution,[status(thm)],[c1170, c30])).
% 3.32/3.55  cnf(c1167,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X635)|iext(X635,uri_rdf_predicate,uri_rdf_Property),inference(resolution,[status(thm)],[c1161, c30])).
% 3.32/3.55  cnf(c6,plain,iext(uri_rdfs_range,uri_ex_p,skolem0002),inference(split_conjunct,[status(thm)],[c1])).
% 3.32/3.55  cnf(c256,plain,~iext(uri_rdfs_range,uri_rdfs_range,X178)|icext(X178,skolem0002),inference(resolution,[status(thm)],[c56, c6])).
% 3.32/3.55  cnf(c1101,plain,icext(uri_rdfs_Class,skolem0002),inference(resolution,[status(thm)],[c256, c53])).
% 3.32/3.55  cnf(c1103,plain,ic(skolem0002),inference(resolution,[status(thm)],[c1101, c76])).
% 3.32/3.55  cnf(c1105,plain,iext(uri_rdfs_subClassOf,skolem0002,skolem0002),inference(resolution,[status(thm)],[c1103, c37])).
% 3.32/3.55  cnf(c1146,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X634)|iext(X634,skolem0002,skolem0002),inference(resolution,[status(thm)],[c1105, c30])).
% 3.32/3.55  cnf(c1104,plain,iext(uri_rdfs_subClassOf,skolem0002,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1103, c114])).
% 3.32/3.55  cnf(c1138,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X632)|iext(X632,skolem0002,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1104, c30])).
% 3.32/3.55  cnf(c1136,plain,~iext(uri_rdfs_subClassOf,X631,skolem0002)|iext(uri_rdfs_subClassOf,X631,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1104, c34])).
% 3.32/3.55  cnf(c1102,plain,iext(uri_rdf_type,skolem0002,uri_rdfs_Class),inference(resolution,[status(thm)],[c1101, c120])).
% 3.32/3.55  cnf(c1130,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X630)|iext(X630,skolem0002,uri_rdfs_Class),inference(resolution,[status(thm)],[c1102, c30])).
% 3.32/3.55  fof(rdfs_domain_range,axiom,iext(uri_rdfs_range,uri_rdfs_domain,uri_rdfs_Class),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_domain_range)).
% 3.32/3.55  cnf(c77,plain,iext(uri_rdfs_range,uri_rdfs_domain,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_domain_range])).
% 3.32/3.55  cnf(c238,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X160)|icext(X160,skolem0001),inference(resolution,[status(thm)],[c56, c2])).
% 3.32/3.55  cnf(c971,plain,icext(uri_rdfs_Class,skolem0001),inference(resolution,[status(thm)],[c238, c77])).
% 3.32/3.55  cnf(c973,plain,ic(skolem0001),inference(resolution,[status(thm)],[c971, c76])).
% 3.32/3.55  cnf(c975,plain,iext(uri_rdfs_subClassOf,skolem0001,skolem0001),inference(resolution,[status(thm)],[c973, c37])).
% 3.32/3.55  cnf(c1124,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X629)|iext(X629,skolem0001,skolem0001),inference(resolution,[status(thm)],[c975, c30])).
% 3.32/3.55  cnf(c974,plain,iext(uri_rdfs_subClassOf,skolem0001,uri_rdfs_Resource),inference(resolution,[status(thm)],[c973, c114])).
% 3.32/3.55  cnf(c1116,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X627)|iext(X627,skolem0001,uri_rdfs_Resource),inference(resolution,[status(thm)],[c974, c30])).
% 3.32/3.55  cnf(c1114,plain,~iext(uri_rdfs_subClassOf,X626,skolem0001)|iext(uri_rdfs_subClassOf,X626,uri_rdfs_Resource),inference(resolution,[status(thm)],[c974, c34])).
% 3.32/3.55  cnf(c972,plain,iext(uri_rdf_type,skolem0001,uri_rdfs_Class),inference(resolution,[status(thm)],[c971, c120])).
% 3.32/3.55  cnf(c1109,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X625)|iext(X625,skolem0001,uri_rdfs_Class),inference(resolution,[status(thm)],[c972, c30])).
% 3.32/3.55  cnf(c232,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X154)|icext(X154,uri_rdfs_Statement),inference(resolution,[status(thm)],[c56, c50])).
% 3.32/3.55  cnf(c917,plain,icext(uri_rdfs_Class,uri_rdfs_Statement),inference(resolution,[status(thm)],[c232, c77])).
% 3.32/3.55  cnf(c919,plain,ic(uri_rdfs_Statement),inference(resolution,[status(thm)],[c917, c76])).
% 3.32/3.55  cnf(c921,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Statement,uri_rdfs_Statement),inference(resolution,[status(thm)],[c919, c37])).
% 3.32/3.55  cnf(c1095,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X624)|iext(X624,uri_rdfs_Statement,uri_rdfs_Statement),inference(resolution,[status(thm)],[c921, c30])).
% 3.32/3.55  cnf(c920,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Statement,uri_rdfs_Resource),inference(resolution,[status(thm)],[c919, c114])).
% 3.32/3.55  cnf(c1086,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X622)|iext(X622,uri_rdfs_Statement,uri_rdfs_Resource),inference(resolution,[status(thm)],[c920, c30])).
% 3.32/3.55  cnf(c1084,plain,~iext(uri_rdfs_subClassOf,X621,uri_rdfs_Statement)|iext(uri_rdfs_subClassOf,X621,uri_rdfs_Resource),inference(resolution,[status(thm)],[c920, c34])).
% 3.32/3.55  cnf(c918,plain,iext(uri_rdf_type,uri_rdfs_Statement,uri_rdfs_Class),inference(resolution,[status(thm)],[c917, c120])).
% 3.32/3.55  cnf(c1079,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X620)|iext(X620,uri_rdfs_Statement,uri_rdfs_Class),inference(resolution,[status(thm)],[c918, c30])).
% 3.32/3.55  cnf(c29,plain,~iext(uri_rdfs_subPropertyOf,X61,X62)|ip(X62),inference(split_conjunct,[status(thm)],[c27])).
% 3.32/3.55  fof(rdfs_container_containermembershipproperty_instsub_member,axiom,(![P]:(icext(uri_rdfs_ContainerMembershipProperty,P)=>iext(uri_rdfs_subPropertyOf,P,uri_rdfs_member))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_containermembershipproperty_instsub_member)).
% 3.32/3.55  fof(c103,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.32/3.55  fof(c104,plain,(![X36]:(~icext(uri_rdfs_ContainerMembershipProperty,X36)|iext(uri_rdfs_subPropertyOf,X36,uri_rdfs_member))),inference(variable_rename,[status(thm)],[c103])).
% 3.32/3.55  cnf(c105,plain,~icext(uri_rdfs_ContainerMembershipProperty,X90)|iext(uri_rdfs_subPropertyOf,X90,uri_rdfs_member),inference(split_conjunct,[status(thm)],[c104])).
% 3.32/3.55  fof(rdfs_container_n_type_002,axiom,iext(uri_rdf_type,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_type_002)).
% 3.32/3.55  cnf(c92,plain,iext(uri_rdf_type,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),inference(split_conjunct,[status(thm)],[rdfs_container_n_type_002])).
% 3.32/3.55  cnf(c119,plain,~iext(uri_rdf_type,X93,X92)|icext(X92,X93),inference(split_conjunct,[status(thm)],[c118])).
% 3.32/3.55  cnf(c392,plain,icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__2),inference(resolution,[status(thm)],[c119, c92])).
% 3.32/3.55  cnf(c397,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__2,uri_rdfs_member),inference(resolution,[status(thm)],[c392, c105])).
% 3.32/3.55  cnf(c773,plain,ip(uri_rdfs_member),inference(resolution,[status(thm)],[c397, c29])).
% 3.32/3.55  cnf(c775,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_member,uri_rdfs_member),inference(resolution,[status(thm)],[c773, c22])).
% 3.32/3.55  cnf(c1070,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X618)|iext(X618,uri_rdfs_member,uri_rdfs_member),inference(resolution,[status(thm)],[c775, c30])).
% 3.32/3.55  cnf(c137,plain,~ip(X99)|iext(uri_rdf_type,X99,uri_rdf_Property),inference(split_conjunct,[status(thm)],[c135])).
% 3.32/3.55  cnf(c774,plain,iext(uri_rdf_type,uri_rdfs_member,uri_rdf_Property),inference(resolution,[status(thm)],[c773, c137])).
% 3.32/3.55  cnf(c1063,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X617)|iext(X617,uri_rdfs_member,uri_rdf_Property),inference(resolution,[status(thm)],[c774, c30])).
% 3.32/3.55  cnf(c75,plain,~ic(X64)|icext(uri_rdfs_Class,X64),inference(split_conjunct,[status(thm)],[c74])).
% 3.32/3.55  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/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_subclassof_main)).
% 3.32/3.55  fof(c39,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.32/3.55  fof(c41,plain,(![X18]:(![X19]:(![X20]:(~iext(uri_rdfs_subClassOf,X18,X19)|((ic(X18)&ic(X19))&(~icext(X18,X20)|icext(X19,X20))))))),inference(shift_quantors,[status(thm)],[fof(c40,plain,(![X18]:(![X19]:(~iext(uri_rdfs_subClassOf,X18,X19)|((ic(X18)&ic(X19))&(![X20]:(~icext(X18,X20)|icext(X19,X20))))))),inference(variable_rename,[status(thm)],[c39])).])).
% 3.32/3.55  fof(c42,plain,(![X18]:(![X19]:(![X20]:(((~iext(uri_rdfs_subClassOf,X18,X19)|ic(X18))&(~iext(uri_rdfs_subClassOf,X18,X19)|ic(X19)))&(~iext(uri_rdfs_subClassOf,X18,X19)|(~icext(X18,X20)|icext(X19,X20))))))),inference(distribute,[status(thm)],[c41])).
% 3.32/3.55  cnf(c44,plain,~iext(uri_rdfs_subClassOf,X76,X77)|ic(X77),inference(split_conjunct,[status(thm)],[c42])).
% 3.32/3.55  fof(rdfs_dat_xmlliteral_sub,axiom,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Literal),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_dat_xmlliteral_sub)).
% 3.32/3.55  cnf(c89,plain,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[rdfs_dat_xmlliteral_sub])).
% 3.32/3.55  cnf(c215,plain,ic(uri_rdfs_Literal),inference(resolution,[status(thm)],[c44, c89])).
% 3.32/3.55  cnf(c367,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Literal,uri_rdfs_Resource),inference(resolution,[status(thm)],[c114, c215])).
% 3.32/3.55  cnf(c675,plain,ic(uri_rdfs_Resource),inference(resolution,[status(thm)],[c367, c44])).
% 3.32/3.55  cnf(c678,plain,icext(uri_rdfs_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c675, c75])).
% 3.32/3.55  cnf(c679,plain,iext(uri_rdf_type,uri_rdfs_Resource,uri_rdfs_Class),inference(resolution,[status(thm)],[c678, c120])).
% 3.32/3.55  cnf(c1057,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X616)|iext(X616,uri_rdfs_Resource,uri_rdfs_Class),inference(resolution,[status(thm)],[c679, c30])).
% 3.32/3.55  cnf(c676,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Resource,uri_rdfs_Resource),inference(resolution,[status(thm)],[c675, c114])).
% 3.32/3.55  cnf(c1051,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X615)|iext(X615,uri_rdfs_Resource,uri_rdfs_Resource),inference(resolution,[status(thm)],[c676, c30])).
% 3.32/3.55  cnf(c7,plain,iext(uri_owl_oneOf,skolem0002,skolem0004),inference(split_conjunct,[status(thm)],[c1])).
% 3.32/3.55  fof(simple_iext_property,axiom,(![S]:(![P]:(![O]:(iext(P,S,O)=>ip(P))))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', simple_iext_property)).
% 3.32/3.55  fof(c152,plain,(![S]:(![P]:(![O]:(~iext(P,S,O)|ip(P))))),inference(fof_nnf,[status(thm)],[simple_iext_property])).
% 3.32/3.55  fof(c153,plain,(![S]:(![P]:((![O]:~iext(P,S,O))|ip(P)))),inference(shift_quantors,[status(thm)],[c152])).
% 3.32/3.55  fof(c155,plain,(![X46]:(![X47]:(![X48]:(~iext(X47,X46,X48)|ip(X47))))),inference(shift_quantors,[status(thm)],[fof(c154,plain,(![X46]:(![X47]:((![X48]:~iext(X47,X46,X48))|ip(X47)))),inference(variable_rename,[status(thm)],[c153])).])).
% 3.32/3.55  cnf(c156,plain,~iext(X102,X101,X100)|ip(X102),inference(split_conjunct,[status(thm)],[c155])).
% 3.32/3.55  cnf(c556,plain,ip(uri_owl_oneOf),inference(resolution,[status(thm)],[c156, c7])).
% 3.32/3.55  cnf(c587,plain,iext(uri_rdfs_subPropertyOf,uri_owl_oneOf,uri_owl_oneOf),inference(resolution,[status(thm)],[c556, c22])).
% 3.32/3.55  cnf(c1041,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X612)|iext(X612,uri_owl_oneOf,uri_owl_oneOf),inference(resolution,[status(thm)],[c587, c30])).
% 3.32/3.55  cnf(c586,plain,iext(uri_rdf_type,uri_owl_oneOf,uri_rdf_Property),inference(resolution,[status(thm)],[c556, c137])).
% 3.32/3.55  cnf(c1033,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X611)|iext(X611,uri_owl_oneOf,uri_rdf_Property),inference(resolution,[status(thm)],[c586, c30])).
% 3.32/3.55  fof(rdfs_annotation_isdefinedby_sub,axiom,iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_isdefinedby_sub)).
% 3.32/3.55  cnf(c125,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_sub])).
% 3.32/3.55  cnf(c537,plain,ip(uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c156, c125])).
% 3.32/3.55  cnf(c585,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c537, c22])).
% 3.32/3.55  cnf(c1025,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X609)|iext(X609,uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c585, c30])).
% 3.32/3.55  cnf(c584,plain,iext(uri_rdf_type,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c537, c137])).
% 3.32/3.55  cnf(c1018,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X608)|iext(X608,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c584, c30])).
% 3.32/3.55  cnf(c532,plain,ip(uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c156, c89])).
% 3.32/3.55  cnf(c583,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c532, c22])).
% 3.32/3.55  cnf(c1008,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X606)|iext(X606,uri_rdfs_subClassOf,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c583, c30])).
% 3.32/3.55  cnf(c582,plain,iext(uri_rdf_type,uri_rdfs_subClassOf,uri_rdf_Property),inference(resolution,[status(thm)],[c532, c137])).
% 3.32/3.55  cnf(c999,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X605)|iext(X605,uri_rdfs_subClassOf,uri_rdf_Property),inference(resolution,[status(thm)],[c582, c30])).
% 3.32/3.55  fof(rdfs_container_n_range_002,axiom,iext(uri_rdfs_range,uri_rdf__2,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_range_002)).
% 3.32/3.55  cnf(c95,plain,iext(uri_rdfs_range,uri_rdf__2,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_range_002])).
% 3.32/3.55  cnf(c512,plain,ip(uri_rdfs_range),inference(resolution,[status(thm)],[c156, c95])).
% 3.32/3.55  cnf(c581,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_range,uri_rdfs_range),inference(resolution,[status(thm)],[c512, c22])).
% 3.32/3.55  cnf(c982,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X603)|iext(X603,uri_rdfs_range,uri_rdfs_range),inference(resolution,[status(thm)],[c581, c30])).
% 3.32/3.55  cnf(c580,plain,iext(uri_rdf_type,uri_rdfs_range,uri_rdf_Property),inference(resolution,[status(thm)],[c512, c137])).
% 3.32/3.55  cnf(c966,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X602)|iext(X602,uri_rdfs_range,uri_rdf_Property),inference(resolution,[status(thm)],[c580, c30])).
% 3.32/3.55  cnf(c510,plain,ip(uri_rdfs_domain),inference(resolution,[status(thm)],[c156, c50])).
% 3.32/3.55  cnf(c579,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,uri_rdfs_domain),inference(resolution,[status(thm)],[c510, c22])).
% 3.32/3.55  cnf(c948,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X600)|iext(X600,uri_rdfs_domain,uri_rdfs_domain),inference(resolution,[status(thm)],[c579, c30])).
% 3.32/3.55  cnf(c578,plain,iext(uri_rdf_type,uri_rdfs_domain,uri_rdf_Property),inference(resolution,[status(thm)],[c510, c137])).
% 3.32/3.55  cnf(c936,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X599)|iext(X599,uri_rdfs_domain,uri_rdf_Property),inference(resolution,[status(thm)],[c578, c30])).
% 3.32/3.55  fof(rdf_collection_first_type,axiom,iext(uri_rdf_type,uri_rdf_first,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdf_collection_first_type)).
% 3.32/3.55  cnf(c146,plain,iext(uri_rdf_type,uri_rdf_first,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_collection_first_type])).
% 3.32/3.55  cnf(c504,plain,ip(uri_rdf_first),inference(resolution,[status(thm)],[c146, c136])).
% 3.32/3.55  cnf(c508,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_first,uri_rdf_first),inference(resolution,[status(thm)],[c504, c22])).
% 3.32/3.55  cnf(c927,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X597)|iext(X597,uri_rdf_first,uri_rdf_first),inference(resolution,[status(thm)],[c508, c30])).
% 3.32/3.55  fof(rdf_collection_rest_type,axiom,iext(uri_rdf_type,uri_rdf_rest,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdf_collection_rest_type)).
% 3.32/3.55  cnf(c144,plain,iext(uri_rdf_type,uri_rdf_rest,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_collection_rest_type])).
% 3.32/3.55  cnf(c490,plain,ip(uri_rdf_rest),inference(resolution,[status(thm)],[c144, c136])).
% 3.32/3.55  cnf(c494,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_rest,uri_rdf_rest),inference(resolution,[status(thm)],[c490, c22])).
% 3.32/3.55  cnf(c910,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X595)|iext(X595,uri_rdf_rest,uri_rdf_rest),inference(resolution,[status(thm)],[c494, c30])).
% 3.32/3.55  fof(rdf_container_n_type_001,axiom,iext(uri_rdf_type,uri_rdf__1,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdf_container_n_type_001)).
% 3.32/3.55  cnf(c143,plain,iext(uri_rdf_type,uri_rdf__1,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_container_n_type_001])).
% 3.32/3.55  cnf(c483,plain,ip(uri_rdf__1),inference(resolution,[status(thm)],[c143, c136])).
% 3.32/3.55  cnf(c487,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__1,uri_rdf__1),inference(resolution,[status(thm)],[c483, c22])).
% 3.32/3.55  cnf(c902,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X593)|iext(X593,uri_rdf__1,uri_rdf__1),inference(resolution,[status(thm)],[c487, c30])).
% 3.32/3.55  fof(rdf_container_n_type_002,axiom,iext(uri_rdf_type,uri_rdf__2,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdf_container_n_type_002)).
% 3.32/3.55  cnf(c142,plain,iext(uri_rdf_type,uri_rdf__2,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_container_n_type_002])).
% 3.32/3.55  cnf(c474,plain,ip(uri_rdf__2),inference(resolution,[status(thm)],[c142, c136])).
% 3.32/3.55  cnf(c478,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__2,uri_rdf__2),inference(resolution,[status(thm)],[c474, c22])).
% 3.32/3.55  cnf(c894,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X591)|iext(X591,uri_rdf__2,uri_rdf__2),inference(resolution,[status(thm)],[c478, c30])).
% 3.32/3.55  fof(rdf_container_n_type_003,axiom,iext(uri_rdf_type,uri_rdf__3,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdf_container_n_type_003)).
% 3.32/3.55  cnf(c141,plain,iext(uri_rdf_type,uri_rdf__3,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_container_n_type_003])).
% 3.32/3.55  cnf(c467,plain,ip(uri_rdf__3),inference(resolution,[status(thm)],[c141, c136])).
% 3.32/3.55  cnf(c471,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__3,uri_rdf__3),inference(resolution,[status(thm)],[c467, c22])).
% 3.32/3.55  cnf(c887,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X589)|iext(X589,uri_rdf__3,uri_rdf__3),inference(resolution,[status(thm)],[c471, c30])).
% 3.32/3.55  fof(rdf_reification_object_type,axiom,iext(uri_rdf_type,uri_rdf_object,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdf_reification_object_type)).
% 3.32/3.55  cnf(c140,plain,iext(uri_rdf_type,uri_rdf_object,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_reification_object_type])).
% 3.32/3.55  cnf(c459,plain,ip(uri_rdf_object),inference(resolution,[status(thm)],[c140, c136])).
% 3.32/3.55  cnf(c463,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_object,uri_rdf_object),inference(resolution,[status(thm)],[c459, c22])).
% 3.32/3.55  cnf(c880,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X587)|iext(X587,uri_rdf_object,uri_rdf_object),inference(resolution,[status(thm)],[c463, c30])).
% 3.32/3.55  cnf(c28,plain,~iext(uri_rdfs_subPropertyOf,X55,X56)|ip(X55),inference(split_conjunct,[status(thm)],[c27])).
% 3.32/3.55  cnf(c383,plain,ip(uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c125, c28])).
% 3.32/3.55  cnf(c454,plain,iext(uri_rdf_type,uri_rdfs_isDefinedBy,uri_rdf_Property),inference(resolution,[status(thm)],[c137, c383])).
% 3.32/3.55  cnf(c873,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X586)|iext(X586,uri_rdfs_isDefinedBy,uri_rdf_Property),inference(resolution,[status(thm)],[c454, c30])).
% 3.32/3.55  cnf(c386,plain,ip(uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c125, c29])).
% 3.32/3.55  cnf(c453,plain,iext(uri_rdf_type,uri_rdfs_seeAlso,uri_rdf_Property),inference(resolution,[status(thm)],[c137, c386])).
% 3.32/3.55  cnf(c866,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X585)|iext(X585,uri_rdfs_seeAlso,uri_rdf_Property),inference(resolution,[status(thm)],[c453, c30])).
% 3.32/3.55  fof(rdf_reification_predicate_type,axiom,iext(uri_rdf_type,uri_rdf_value,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdf_reification_predicate_type)).
% 3.32/3.55  cnf(c139,plain,iext(uri_rdf_type,uri_rdf_value,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_reification_predicate_type])).
% 3.32/3.55  cnf(c447,plain,ip(uri_rdf_value),inference(resolution,[status(thm)],[c139, c136])).
% 3.32/3.55  cnf(c450,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_value,uri_rdf_value),inference(resolution,[status(thm)],[c447, c22])).
% 3.32/3.55  cnf(c859,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X583)|iext(X583,uri_rdf_value,uri_rdf_value),inference(resolution,[status(thm)],[c450, c30])).
% 3.32/3.55  fof(rdf_reification_subject_type,axiom,iext(uri_rdf_type,uri_rdf_subject,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdf_reification_subject_type)).
% 3.32/3.55  cnf(c138,plain,iext(uri_rdf_type,uri_rdf_subject,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_reification_subject_type])).
% 3.32/3.55  cnf(c442,plain,ip(uri_rdf_subject),inference(resolution,[status(thm)],[c136, c138])).
% 3.32/3.55  cnf(c444,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_subject,uri_rdf_subject),inference(resolution,[status(thm)],[c442, c22])).
% 3.32/3.55  cnf(c852,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X581)|iext(X581,uri_rdf_subject,uri_rdf_subject),inference(resolution,[status(thm)],[c444, c30])).
% 3.32/3.55  fof(rdf_value_type,axiom,iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdf_value_type)).
% 3.32/3.55  cnf(c130,plain,iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_value_type])).
% 3.32/3.55  cnf(c441,plain,ip(uri_rdf_type),inference(resolution,[status(thm)],[c136, c130])).
% 3.32/3.55  cnf(c443,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_type,uri_rdf_type),inference(resolution,[status(thm)],[c441, c22])).
% 3.32/3.55  cnf(c842,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X579)|iext(X579,uri_rdf_type,uri_rdf_type),inference(resolution,[status(thm)],[c443, c30])).
% 3.32/3.55  cnf(c43,plain,~iext(uri_rdfs_subClassOf,X74,X75)|ic(X74),inference(split_conjunct,[status(thm)],[c42])).
% 3.32/3.55  fof(rdfs_container_bag_sub,axiom,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Container),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_bag_sub)).
% 3.32/3.55  cnf(c106,plain,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Container),inference(split_conjunct,[status(thm)],[rdfs_container_bag_sub])).
% 3.32/3.55  cnf(c332,plain,ic(uri_rdf_Bag),inference(resolution,[status(thm)],[c106, c43])).
% 3.32/3.55  cnf(c337,plain,icext(uri_rdfs_Class,uri_rdf_Bag),inference(resolution,[status(thm)],[c332, c75])).
% 3.32/3.55  cnf(c414,plain,iext(uri_rdf_type,uri_rdf_Bag,uri_rdfs_Class),inference(resolution,[status(thm)],[c120, c337])).
% 3.32/3.55  cnf(c835,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X578)|iext(X578,uri_rdf_Bag,uri_rdfs_Class),inference(resolution,[status(thm)],[c414, c30])).
% 3.32/3.55  fof(rdfs_container_seq_sub,axiom,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Container),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_seq_sub)).
% 3.32/3.55  cnf(c90,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Container),inference(split_conjunct,[status(thm)],[rdfs_container_seq_sub])).
% 3.32/3.55  cnf(c216,plain,ic(uri_rdfs_Container),inference(resolution,[status(thm)],[c44, c90])).
% 3.32/3.55  cnf(c221,plain,icext(uri_rdfs_Class,uri_rdfs_Container),inference(resolution,[status(thm)],[c216, c75])).
% 3.32/3.55  cnf(c413,plain,iext(uri_rdf_type,uri_rdfs_Container,uri_rdfs_Class),inference(resolution,[status(thm)],[c120, c221])).
% 3.32/3.55  cnf(c830,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X577)|iext(X577,uri_rdfs_Container,uri_rdfs_Class),inference(resolution,[status(thm)],[c413, c30])).
% 3.32/3.55  fof(rdfs_container_alt_sub,axiom,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Container),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_alt_sub)).
% 3.32/3.55  cnf(c107,plain,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Container),inference(split_conjunct,[status(thm)],[rdfs_container_alt_sub])).
% 3.32/3.55  cnf(c342,plain,ic(uri_rdf_Alt),inference(resolution,[status(thm)],[c107, c43])).
% 3.32/3.55  cnf(c347,plain,icext(uri_rdfs_Class,uri_rdf_Alt),inference(resolution,[status(thm)],[c342, c75])).
% 3.32/3.55  cnf(c412,plain,iext(uri_rdf_type,uri_rdf_Alt,uri_rdfs_Class),inference(resolution,[status(thm)],[c120, c347])).
% 3.32/3.55  cnf(c825,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X576)|iext(X576,uri_rdf_Alt,uri_rdfs_Class),inference(resolution,[status(thm)],[c412, c30])).
% 3.32/3.55  fof(rdfs_datatype_sub,axiom,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Class),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_datatype_sub)).
% 3.32/3.55  cnf(c84,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_datatype_sub])).
% 3.32/3.55  cnf(c207,plain,ic(uri_rdfs_Datatype),inference(resolution,[status(thm)],[c43, c84])).
% 3.32/3.55  cnf(c213,plain,icext(uri_rdfs_Class,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c207, c75])).
% 3.32/3.55  cnf(c410,plain,iext(uri_rdf_type,uri_rdfs_Datatype,uri_rdfs_Class),inference(resolution,[status(thm)],[c120, c213])).
% 3.32/3.55  cnf(c820,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X575)|iext(X575,uri_rdfs_Datatype,uri_rdfs_Class),inference(resolution,[status(thm)],[c410, c30])).
% 3.32/3.55  cnf(c219,plain,icext(uri_rdfs_Class,uri_rdfs_Literal),inference(resolution,[status(thm)],[c215, c75])).
% 3.32/3.55  cnf(c408,plain,iext(uri_rdf_type,uri_rdfs_Literal,uri_rdfs_Class),inference(resolution,[status(thm)],[c120, c219])).
% 3.32/3.55  cnf(c815,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X574)|iext(X574,uri_rdfs_Literal,uri_rdfs_Class),inference(resolution,[status(thm)],[c408, c30])).
% 3.32/3.55  fof(rdfs_container_containermembershipproperty_sub,axiom,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_containermembershipproperty_sub)).
% 3.32/3.55  cnf(c102,plain,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_container_containermembershipproperty_sub])).
% 3.32/3.55  cnf(c276,plain,ic(uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c102, c43])).
% 3.32/3.55  cnf(c326,plain,icext(uri_rdfs_Class,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c276, c75])).
% 3.32/3.55  cnf(c405,plain,iext(uri_rdf_type,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Class),inference(resolution,[status(thm)],[c120, c326])).
% 3.32/3.55  cnf(c809,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X573)|iext(X573,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Class),inference(resolution,[status(thm)],[c405, c30])).
% 3.32/3.55  cnf(c205,plain,ic(uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c43, c89])).
% 3.32/3.55  cnf(c209,plain,icext(uri_rdfs_Class,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c205, c75])).
% 3.32/3.55  cnf(c404,plain,iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Class),inference(resolution,[status(thm)],[c120, c209])).
% 3.32/3.55  cnf(c804,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X572)|iext(X572,uri_rdf_XMLLiteral,uri_rdfs_Class),inference(resolution,[status(thm)],[c404, c30])).
% 3.32/3.55  cnf(c217,plain,ic(uri_rdfs_Class),inference(resolution,[status(thm)],[c44, c84])).
% 3.32/3.55  cnf(c223,plain,icext(uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c217, c75])).
% 3.32/3.55  cnf(c402,plain,iext(uri_rdf_type,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c120, c223])).
% 3.32/3.55  cnf(c798,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X571)|iext(X571,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c402, c30])).
% 3.32/3.55  cnf(c206,plain,ic(uri_rdfs_Seq),inference(resolution,[status(thm)],[c43, c90])).
% 3.32/3.55  cnf(c211,plain,icext(uri_rdfs_Class,uri_rdfs_Seq),inference(resolution,[status(thm)],[c206, c75])).
% 3.32/3.55  cnf(c400,plain,iext(uri_rdf_type,uri_rdfs_Seq,uri_rdfs_Class),inference(resolution,[status(thm)],[c120, c211])).
% 3.32/3.55  cnf(c792,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X570)|iext(X570,uri_rdfs_Seq,uri_rdfs_Class),inference(resolution,[status(thm)],[c400, c30])).
% 3.32/3.55  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/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_subpropertyof_trans)).
% 3.32/3.55  fof(c17,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.32/3.55  fof(c18,plain,(![X6]:(![X7]:(![X8]:((~iext(uri_rdfs_subPropertyOf,X6,X7)|~iext(uri_rdfs_subPropertyOf,X7,X8))|iext(uri_rdfs_subPropertyOf,X6,X8))))),inference(variable_rename,[status(thm)],[c17])).
% 3.32/3.55  cnf(c19,plain,~iext(uri_rdfs_subPropertyOf,X51,X53)|~iext(uri_rdfs_subPropertyOf,X53,X52)|iext(uri_rdfs_subPropertyOf,X51,X52),inference(split_conjunct,[status(thm)],[c18])).
% 3.32/3.55  fof(rdfs_container_n_type_001,axiom,iext(uri_rdf_type,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_type_001)).
% 3.32/3.55  cnf(c93,plain,iext(uri_rdf_type,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),inference(split_conjunct,[status(thm)],[rdfs_container_n_type_001])).
% 3.32/3.55  cnf(c395,plain,icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__1),inference(resolution,[status(thm)],[c119, c93])).
% 3.32/3.55  cnf(c399,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__1,uri_rdfs_member),inference(resolution,[status(thm)],[c395, c105])).
% 3.32/3.55  cnf(c788,plain,~iext(uri_rdfs_subPropertyOf,X569,uri_rdf__1)|iext(uri_rdfs_subPropertyOf,X569,uri_rdfs_member),inference(resolution,[status(thm)],[c399, c19])).
% 3.32/3.55  cnf(c785,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X568)|iext(X568,uri_rdf__1,uri_rdfs_member),inference(resolution,[status(thm)],[c399, c30])).
% 3.32/3.55  fof(rdfs_container_n_type_003,axiom,iext(uri_rdf_type,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_type_003)).
% 3.32/3.55  cnf(c91,plain,iext(uri_rdf_type,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),inference(split_conjunct,[status(thm)],[rdfs_container_n_type_003])).
% 3.32/3.55  cnf(c394,plain,icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__3),inference(resolution,[status(thm)],[c119, c91])).
% 3.32/3.55  cnf(c398,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__3,uri_rdfs_member),inference(resolution,[status(thm)],[c394, c105])).
% 3.32/3.55  cnf(c781,plain,~iext(uri_rdfs_subPropertyOf,X567,uri_rdf__3)|iext(uri_rdfs_subPropertyOf,X567,uri_rdfs_member),inference(resolution,[status(thm)],[c398, c19])).
% 3.32/3.55  cnf(c1327,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X566)|icext(X566,uri_rdfs_comment),inference(resolution,[status(thm)],[c1322, c82])).
% 3.32/3.55  cnf(c1323,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X565)|icext(X565,uri_rdfs_comment),inference(resolution,[status(thm)],[c1322, c56])).
% 3.32/3.55  cnf(c778,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X563)|iext(X563,uri_rdf__3,uri_rdfs_member),inference(resolution,[status(thm)],[c398, c30])).
% 3.32/3.55  cnf(c1298,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X561)|icext(X561,uri_rdfs_label),inference(resolution,[status(thm)],[c1292, c82])).
% 3.32/3.55  cnf(c772,plain,~iext(uri_rdfs_subPropertyOf,X560,uri_rdf__2)|iext(uri_rdfs_subPropertyOf,X560,uri_rdfs_member),inference(resolution,[status(thm)],[c397, c19])).
% 3.32/3.55  cnf(c1294,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X559)|icext(X559,uri_rdfs_label),inference(resolution,[status(thm)],[c1292, c56])).
% 3.32/3.55  cnf(c769,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X555)|iext(X555,uri_rdf__2,uri_rdfs_member),inference(resolution,[status(thm)],[c397, c30])).
% 3.32/3.55  cnf(c1265,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X554)|icext(X554,uri_rdf_List),inference(resolution,[status(thm)],[c1247, c56])).
% 3.32/3.55  cnf(c1261,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X553)|icext(X553,uri_rdf_List),inference(resolution,[status(thm)],[c1246, c82])).
% 3.32/3.55  cnf(c390,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_seeAlso,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c386, c22])).
% 3.32/3.55  cnf(c762,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X546)|iext(X546,uri_rdfs_seeAlso,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c390, c30])).
% 3.32/3.55  cnf(c1197,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X543)|icext(X543,uri_ex_p),inference(resolution,[status(thm)],[c1191, c82])).
% 3.32/3.55  cnf(c1193,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X541)|icext(X541,uri_ex_p),inference(resolution,[status(thm)],[c1191, c56])).
% 3.32/3.55  cnf(c389,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c383, c22])).
% 3.32/3.55  cnf(c755,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X538)|iext(X538,uri_rdfs_isDefinedBy,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c389, c30])).
% 3.32/3.55  cnf(c1176,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X537)|icext(X537,uri_rdf_predicate),inference(resolution,[status(thm)],[c1170, c82])).
% 3.32/3.55  cnf(c1172,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X536)|icext(X536,uri_rdf_predicate),inference(resolution,[status(thm)],[c1170, c56])).
% 3.32/3.55  cnf(c376,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Resource),inference(resolution,[status(thm)],[c114, c206])).
% 3.32/3.55  cnf(c749,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X534)|iext(X534,uri_rdfs_Seq,uri_rdfs_Resource),inference(resolution,[status(thm)],[c376, c30])).
% 3.32/3.55  cnf(c1145,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X531)|icext(X531,skolem0002),inference(resolution,[status(thm)],[c1105, c56])).
% 3.32/3.55  cnf(c747,plain,~iext(uri_rdfs_subClassOf,X530,uri_rdfs_Seq)|iext(uri_rdfs_subClassOf,X530,uri_rdfs_Resource),inference(resolution,[status(thm)],[c376, c34])).
% 3.32/3.55  cnf(c1139,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X529)|icext(X529,skolem0002),inference(resolution,[status(thm)],[c1104, c82])).
% 3.32/3.55  cnf(c375,plain,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Resource),inference(resolution,[status(thm)],[c114, c332])).
% 3.32/3.55  cnf(c741,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X526)|iext(X526,uri_rdf_Bag,uri_rdfs_Resource),inference(resolution,[status(thm)],[c375, c30])).
% 3.32/3.55  cnf(c1123,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X523)|icext(X523,skolem0001),inference(resolution,[status(thm)],[c975, c56])).
% 3.32/3.55  cnf(c739,plain,~iext(uri_rdfs_subClassOf,X522,uri_rdf_Bag)|iext(uri_rdfs_subClassOf,X522,uri_rdfs_Resource),inference(resolution,[status(thm)],[c375, c34])).
% 3.32/3.55  cnf(c1117,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X521)|icext(X521,skolem0001),inference(resolution,[status(thm)],[c974, c82])).
% 3.32/3.55  cnf(c374,plain,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Resource),inference(resolution,[status(thm)],[c114, c342])).
% 3.32/3.55  cnf(c733,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X518)|iext(X518,uri_rdf_Alt,uri_rdfs_Resource),inference(resolution,[status(thm)],[c374, c30])).
% 3.32/3.55  cnf(c1094,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X515)|icext(X515,uri_rdfs_Statement),inference(resolution,[status(thm)],[c921, c56])).
% 3.32/3.55  cnf(c731,plain,~iext(uri_rdfs_subClassOf,X514,uri_rdf_Alt)|iext(uri_rdfs_subClassOf,X514,uri_rdfs_Resource),inference(resolution,[status(thm)],[c374, c34])).
% 3.32/3.55  cnf(c1087,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X513)|icext(X513,uri_rdfs_Statement),inference(resolution,[status(thm)],[c920, c82])).
% 3.32/3.55  cnf(c373,plain,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Resource),inference(resolution,[status(thm)],[c114, c205])).
% 3.32/3.55  cnf(c725,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X510)|iext(X510,uri_rdf_XMLLiteral,uri_rdfs_Resource),inference(resolution,[status(thm)],[c373, c30])).
% 3.32/3.55  cnf(c1071,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X508)|icext(X508,uri_rdfs_member),inference(resolution,[status(thm)],[c775, c82])).
% 3.32/3.55  cnf(c723,plain,~iext(uri_rdfs_subClassOf,X506,uri_rdf_XMLLiteral)|iext(uri_rdfs_subClassOf,X506,uri_rdfs_Resource),inference(resolution,[status(thm)],[c373, c34])).
% 3.32/3.55  cnf(c372,plain,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Resource),inference(resolution,[status(thm)],[c114, c276])).
% 3.32/3.55  cnf(c717,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X501)|iext(X501,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Resource),inference(resolution,[status(thm)],[c372, c30])).
% 3.32/3.55  cnf(c1052,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X500)|icext(X500,uri_rdfs_Resource),inference(resolution,[status(thm)],[c676, c82])).
% 3.32/3.55  cnf(c715,plain,~iext(uri_rdfs_subClassOf,X498,uri_rdfs_ContainerMembershipProperty)|iext(uri_rdfs_subClassOf,X498,uri_rdfs_Resource),inference(resolution,[status(thm)],[c372, c34])).
% 3.32/3.55  cnf(c1042,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X497)|icext(X497,uri_owl_oneOf),inference(resolution,[status(thm)],[c587, c82])).
% 3.32/3.55  cnf(c1039,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X496)|icext(X496,uri_owl_oneOf),inference(resolution,[status(thm)],[c587, c56])).
% 3.32/3.55  cnf(c371,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Container,uri_rdfs_Resource),inference(resolution,[status(thm)],[c114, c216])).
% 3.32/3.55  cnf(c709,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X494)|iext(X494,uri_rdfs_Container,uri_rdfs_Resource),inference(resolution,[status(thm)],[c371, c30])).
% 3.32/3.55  cnf(c707,plain,~iext(uri_rdfs_subClassOf,X492,uri_rdfs_Container)|iext(uri_rdfs_subClassOf,X492,uri_rdfs_Resource),inference(resolution,[status(thm)],[c371, c34])).
% 3.32/3.55  cnf(c1026,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X491)|icext(X491,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c585, c82])).
% 3.32/3.55  cnf(c1024,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X490)|icext(X490,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c585, c56])).
% 3.32/3.55  cnf(c370,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Resource),inference(resolution,[status(thm)],[c114, c207])).
% 3.32/3.55  cnf(c701,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X489)|iext(X489,uri_rdfs_Datatype,uri_rdfs_Resource),inference(resolution,[status(thm)],[c370, c30])).
% 3.32/3.55  cnf(c1009,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X486)|icext(X486,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c583, c82])).
% 3.32/3.55  cnf(c699,plain,~iext(uri_rdfs_subClassOf,X485,uri_rdfs_Datatype)|iext(uri_rdfs_subClassOf,X485,uri_rdfs_Resource),inference(resolution,[status(thm)],[c370, c34])).
% 3.32/3.55  cnf(c1006,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X484)|icext(X484,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c583, c56])).
% 3.32/3.55  cnf(c274,plain,ic(uri_rdf_Property),inference(resolution,[status(thm)],[c102, c44])).
% 3.32/3.55  cnf(c369,plain,iext(uri_rdfs_subClassOf,uri_rdf_Property,uri_rdfs_Resource),inference(resolution,[status(thm)],[c114, c274])).
% 3.32/3.55  cnf(c693,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X481)|iext(X481,uri_rdf_Property,uri_rdfs_Resource),inference(resolution,[status(thm)],[c369, c30])).
% 3.32/3.55  cnf(c983,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X480)|icext(X480,uri_rdfs_range),inference(resolution,[status(thm)],[c581, c82])).
% 3.32/3.55  cnf(c691,plain,~iext(uri_rdfs_subClassOf,X479,uri_rdf_Property)|iext(uri_rdfs_subClassOf,X479,uri_rdfs_Resource),inference(resolution,[status(thm)],[c369, c34])).
% 3.32/3.55  cnf(c980,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X478)|icext(X478,uri_rdfs_range),inference(resolution,[status(thm)],[c581, c56])).
% 3.32/3.55  cnf(c368,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c114, c217])).
% 3.32/3.55  cnf(c685,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X475)|iext(X475,uri_rdfs_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c368, c30])).
% 3.32/3.55  cnf(c949,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X474)|icext(X474,uri_rdfs_domain),inference(resolution,[status(thm)],[c579, c82])).
% 3.32/3.55  cnf(c946,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X473)|icext(X473,uri_rdfs_domain),inference(resolution,[status(thm)],[c579, c56])).
% 3.32/3.55  cnf(c683,plain,~iext(uri_rdfs_subClassOf,X472,uri_rdfs_Class)|iext(uri_rdfs_subClassOf,X472,uri_rdfs_Resource),inference(resolution,[status(thm)],[c368, c34])).
% 3.32/3.55  cnf(c928,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X469)|icext(X469,uri_rdf_first),inference(resolution,[status(thm)],[c508, c82])).
% 3.32/3.55  cnf(c672,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X468)|iext(X468,uri_rdfs_Literal,uri_rdfs_Resource),inference(resolution,[status(thm)],[c367, c30])).
% 3.32/3.55  cnf(c926,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X467)|icext(X467,uri_rdf_first),inference(resolution,[status(thm)],[c508, c56])).
% 3.32/3.55  cnf(c670,plain,~iext(uri_rdfs_subClassOf,X466,uri_rdfs_Literal)|iext(uri_rdfs_subClassOf,X466,uri_rdfs_Resource),inference(resolution,[status(thm)],[c367, c34])).
% 3.32/3.55  cnf(c911,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X465)|icext(X465,uri_rdf_rest),inference(resolution,[status(thm)],[c494, c82])).
% 3.32/3.55  cnf(c909,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X464)|icext(X464,uri_rdf_rest),inference(resolution,[status(thm)],[c494, c56])).
% 3.32/3.55  cnf(c346,plain,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdf_Alt),inference(resolution,[status(thm)],[c342, c37])).
% 3.32/3.55  cnf(c664,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X462)|iext(X462,uri_rdf_Alt,uri_rdf_Alt),inference(resolution,[status(thm)],[c346, c30])).
% 3.32/3.55  cnf(c901,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X461)|icext(X461,uri_rdf__1),inference(resolution,[status(thm)],[c487, c56])).
% 3.32/3.55  cnf(c893,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X459)|icext(X459,uri_rdf__2),inference(resolution,[status(thm)],[c478, c56])).
% 3.32/3.55  cnf(c886,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X456)|icext(X456,uri_rdf__3),inference(resolution,[status(thm)],[c471, c56])).
% 3.32/3.55  cnf(c336,plain,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdf_Bag),inference(resolution,[status(thm)],[c332, c37])).
% 3.32/3.55  cnf(c656,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X455)|iext(X455,uri_rdf_Bag,uri_rdf_Bag),inference(resolution,[status(thm)],[c336, c30])).
% 3.32/3.55  cnf(c881,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X454)|icext(X454,uri_rdf_object),inference(resolution,[status(thm)],[c463, c82])).
% 3.32/3.55  cnf(c879,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X453)|icext(X453,uri_rdf_object),inference(resolution,[status(thm)],[c463, c56])).
% 3.32/3.55  cnf(c860,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X447)|icext(X447,uri_rdf_value),inference(resolution,[status(thm)],[c450, c82])).
% 3.32/3.55  cnf(c325,plain,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c276, c37])).
% 3.32/3.55  cnf(c648,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X446)|iext(X446,uri_rdfs_ContainerMembershipProperty,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c325, c30])).
% 3.32/3.55  cnf(c858,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X445)|icext(X445,uri_rdf_value),inference(resolution,[status(thm)],[c450, c56])).
% 3.32/3.55  cnf(c853,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X444)|icext(X444,uri_rdf_subject),inference(resolution,[status(thm)],[c444, c82])).
% 3.32/3.55  cnf(c851,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X442)|icext(X442,uri_rdf_subject),inference(resolution,[status(thm)],[c444, c56])).
% 3.32/3.55  cnf(c843,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X441)|icext(X441,uri_rdf_type),inference(resolution,[status(thm)],[c443, c82])).
% 3.32/3.55  cnf(c280,plain,iext(uri_rdfs_subClassOf,uri_rdf_Property,uri_rdf_Property),inference(resolution,[status(thm)],[c274, c37])).
% 3.32/3.55  cnf(c640,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X440)|iext(X440,uri_rdf_Property,uri_rdf_Property),inference(resolution,[status(thm)],[c280, c30])).
% 3.32/3.55  cnf(c841,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X439)|icext(X439,uri_rdf_type),inference(resolution,[status(thm)],[c443, c56])).
% 3.32/3.55  cnf(c222,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c217, c37])).
% 3.32/3.55  cnf(c632,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X429)|iext(X429,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c222, c30])).
% 3.32/3.55  cnf(c220,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Container,uri_rdfs_Container),inference(resolution,[status(thm)],[c216, c37])).
% 3.32/3.55  cnf(c624,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X418)|iext(X418,uri_rdfs_Container,uri_rdfs_Container),inference(resolution,[status(thm)],[c220, c30])).
% 3.32/3.55  cnf(c786,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X416)|icext(X416,uri_rdf__1),inference(resolution,[status(thm)],[c399, c82])).
% 3.32/3.55  cnf(c779,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X413)|icext(X413,uri_rdf__3),inference(resolution,[status(thm)],[c398, c82])).
% 3.32/3.55  cnf(c770,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X411)|icext(X411,uri_rdf__2),inference(resolution,[status(thm)],[c397, c82])).
% 3.32/3.55  cnf(c218,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Literal,uri_rdfs_Literal),inference(resolution,[status(thm)],[c215, c37])).
% 3.32/3.55  cnf(c616,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X410)|iext(X410,uri_rdfs_Literal,uri_rdfs_Literal),inference(resolution,[status(thm)],[c218, c30])).
% 3.32/3.55  cnf(c768,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X409)|icext(X409,uri_rdfs_member),inference(resolution,[status(thm)],[c397, c56])).
% 3.32/3.55  cnf(c763,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X408)|icext(X408,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c390, c82])).
% 3.32/3.55  cnf(c754,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X404)|icext(X404,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c389, c56])).
% 3.32/3.55  cnf(c212,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c207, c37])).
% 3.32/3.55  cnf(c608,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X402)|iext(X402,uri_rdfs_Datatype,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c212, c30])).
% 3.32/3.55  cnf(c210,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Seq),inference(resolution,[status(thm)],[c206, c37])).
% 3.32/3.55  cnf(c600,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X391)|iext(X391,uri_rdfs_Seq,uri_rdfs_Seq),inference(resolution,[status(thm)],[c210, c30])).
% 3.32/3.55  cnf(c208,plain,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c205, c37])).
% 3.32/3.55  cnf(c592,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X380)|iext(X380,uri_rdf_XMLLiteral,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c208, c30])).
% 3.32/3.55  cnf(c671,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X379)|icext(X379,uri_rdfs_Resource),inference(resolution,[status(thm)],[c367, c56])).
% 3.32/3.55  cnf(c663,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X377)|icext(X377,uri_rdf_Alt),inference(resolution,[status(thm)],[c346, c56])).
% 3.32/3.55  cnf(c655,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X374)|icext(X374,uri_rdf_Bag),inference(resolution,[status(thm)],[c336, c56])).
% 3.32/3.55  cnf(c506,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X372)|iext(X372,uri_rdf_first,uri_rdf_Property),inference(resolution,[status(thm)],[c146, c30])).
% 3.32/3.55  cnf(c647,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X371)|icext(X371,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c325, c56])).
% 3.32/3.55  cnf(c641,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X370)|icext(X370,uri_rdf_Property),inference(resolution,[status(thm)],[c280, c82])).
% 3.32/3.55  fof(rdf_collection_nil_type,axiom,iext(uri_rdf_type,uri_rdf_nil,uri_rdf_List),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdf_collection_nil_type)).
% 3.32/3.55  cnf(c145,plain,iext(uri_rdf_type,uri_rdf_nil,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdf_collection_nil_type])).
% 3.32/3.55  cnf(c500,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X369)|iext(X369,uri_rdf_nil,uri_rdf_List),inference(resolution,[status(thm)],[c145, c30])).
% 3.32/3.55  cnf(c633,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X367)|icext(X367,uri_rdfs_Class),inference(resolution,[status(thm)],[c222, c82])).
% 3.32/3.55  cnf(c492,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X365)|iext(X365,uri_rdf_rest,uri_rdf_Property),inference(resolution,[status(thm)],[c144, c30])).
% 3.32/3.55  cnf(c625,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X364)|icext(X364,uri_rdfs_Container),inference(resolution,[status(thm)],[c220, c82])).
% 3.32/3.55  cnf(c485,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X362)|iext(X362,uri_rdf__1,uri_rdf_Property),inference(resolution,[status(thm)],[c143, c30])).
% 3.32/3.55  cnf(c617,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X361)|icext(X361,uri_rdfs_Literal),inference(resolution,[status(thm)],[c218, c82])).
% 3.32/3.55  cnf(c476,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X358)|iext(X358,uri_rdf__2,uri_rdf_Property),inference(resolution,[status(thm)],[c142, c30])).
% 3.32/3.55  cnf(c607,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X357)|icext(X357,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c212, c56])).
% 3.32/3.55  cnf(c599,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X355)|icext(X355,uri_rdfs_Seq),inference(resolution,[status(thm)],[c210, c56])).
% 3.32/3.55  cnf(c469,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X354)|iext(X354,uri_rdf__3,uri_rdf_Property),inference(resolution,[status(thm)],[c141, c30])).
% 3.32/3.55  cnf(c591,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X352)|icext(X352,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c208, c56])).
% 3.32/3.55  cnf(c461,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X350)|iext(X350,uri_rdf_object,uri_rdf_Property),inference(resolution,[status(thm)],[c140, c30])).
% 3.32/3.55  cnf(c499,plain,~iext(uri_rdfs_range,uri_rdf_type,X348)|icext(X348,uri_rdf_List),inference(resolution,[status(thm)],[c145, c56])).
% 3.32/3.55  cnf(c449,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X346)|iext(X346,uri_rdf_value,uri_rdf_Property),inference(resolution,[status(thm)],[c139, c30])).
% 3.32/3.55  cnf(c439,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X341)|iext(X341,uri_rdf_subject,uri_rdf_Property),inference(resolution,[status(thm)],[c138, c30])).
% 3.32/3.55  cnf(c434,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X336)|iext(X336,uri_rdf_type,uri_rdf_Property),inference(resolution,[status(thm)],[c130, c30])).
% 3.32/3.55  fof(rdfs_annotation_comment_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_comment,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_comment_domain)).
% 3.32/3.55  cnf(c129,plain,iext(uri_rdfs_domain,uri_rdfs_comment,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_comment_domain])).
% 3.32/3.55  cnf(c430,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X331)|iext(X331,uri_rdfs_comment,uri_rdfs_Resource),inference(resolution,[status(thm)],[c129, c30])).
% 3.32/3.55  cnf(c433,plain,~iext(uri_rdfs_range,uri_rdf_type,X328)|icext(X328,uri_rdf_Property),inference(resolution,[status(thm)],[c130, c56])).
% 3.32/3.55  cnf(c427,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X327)|iext(X327,uri_rdfs_comment,uri_rdfs_Literal),inference(resolution,[status(thm)],[c128, c30])).
% 3.32/3.55  cnf(c428,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X324)|icext(X324,uri_rdfs_comment),inference(resolution,[status(thm)],[c129, c82])).
% 3.32/3.55  fof(rdfs_annotation_isdefinedby_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_isdefinedby_domain)).
% 3.32/3.55  cnf(c127,plain,iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_domain])).
% 3.32/3.55  cnf(c424,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X323)|iext(X323,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(resolution,[status(thm)],[c127, c30])).
% 3.32/3.55  fof(rdfs_annotation_isdefinedby_range,axiom,iext(uri_rdfs_range,uri_rdfs_isDefinedBy,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_isdefinedby_range)).
% 3.32/3.55  cnf(c126,plain,iext(uri_rdfs_range,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_range])).
% 3.32/3.55  cnf(c421,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X321)|iext(X321,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(resolution,[status(thm)],[c126, c30])).
% 3.32/3.55  fof(simple_ir,axiom,(![X]:ir(X)),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', simple_ir)).
% 3.32/3.55  fof(c150,plain,(![X45]:ir(X45)),inference(variable_rename,[status(thm)],[simple_ir])).
% 3.32/3.55  cnf(c151,plain,ir(X49),inference(split_conjunct,[status(thm)],[c150])).
% 3.32/3.55  fof(rdfs_ir_def,axiom,(![X]:(ir(X)<=>icext(uri_rdfs_Resource,X))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_ir_def)).
% 3.32/3.55  fof(c65,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.32/3.55  fof(c66,plain,((![X]:(~ir(X)|icext(uri_rdfs_Resource,X)))&(![X]:(~icext(uri_rdfs_Resource,X)|ir(X)))),inference(shift_quantors,[status(thm)],[c65])).
% 3.32/3.55  fof(c68,plain,(![X27]:(![X28]:((~ir(X27)|icext(uri_rdfs_Resource,X27))&(~icext(uri_rdfs_Resource,X28)|ir(X28))))),inference(shift_quantors,[status(thm)],[fof(c67,plain,((![X27]:(~ir(X27)|icext(uri_rdfs_Resource,X27)))&(![X28]:(~icext(uri_rdfs_Resource,X28)|ir(X28)))),inference(variable_rename,[status(thm)],[c66])).])).
% 3.32/3.55  cnf(c69,plain,~ir(X59)|icext(uri_rdfs_Resource,X59),inference(split_conjunct,[status(thm)],[c68])).
% 3.32/3.55  cnf(c158,plain,icext(uri_rdfs_Resource,X60),inference(resolution,[status(thm)],[c69, c151])).
% 3.32/3.55  cnf(c401,plain,iext(uri_rdf_type,X96,uri_rdfs_Resource),inference(resolution,[status(thm)],[c120, c158])).
% 3.32/3.55  cnf(c418,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X318)|iext(X318,X319,uri_rdfs_Resource),inference(resolution,[status(thm)],[c401, c30])).
% 3.32/3.55  cnf(c388,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X316)|iext(X316,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c125, c30])).
% 3.32/3.55  cnf(c422,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X314)|icext(X314,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c127, c82])).
% 3.32/3.55  cnf(c384,plain,~iext(uri_rdfs_subPropertyOf,X312,uri_rdfs_isDefinedBy)|iext(uri_rdfs_subPropertyOf,X312,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c125, c19])).
% 3.32/3.55  cnf(c419,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X311)|icext(X311,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c126, c82])).
% 3.32/3.55  cnf(c417,plain,~iext(uri_rdfs_range,uri_rdf_type,X310)|icext(X310,uri_rdfs_Resource),inference(resolution,[status(thm)],[c401, c56])).
% 3.32/3.55  fof(rdfs_annotation_label_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_label,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_label_domain)).
% 3.32/3.55  cnf(c124,plain,iext(uri_rdfs_domain,uri_rdfs_label,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_label_domain])).
% 3.32/3.55  cnf(c382,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X309)|iext(X309,uri_rdfs_label,uri_rdfs_Resource),inference(resolution,[status(thm)],[c124, c30])).
% 3.32/3.55  cnf(c387,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X308)|icext(X308,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c125, c56])).
% 3.32/3.55  cnf(c385,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X307)|icext(X307,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c125, c82])).
% 3.32/3.55  cnf(c379,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X306)|iext(X306,uri_rdfs_label,uri_rdfs_Literal),inference(resolution,[status(thm)],[c123, c30])).
% 3.32/3.55  cnf(c380,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X304)|icext(X304,uri_rdfs_label),inference(resolution,[status(thm)],[c124, c82])).
% 3.32/3.55  cnf(c378,plain,~iext(uri_rdfs_range,uri_rdfs_range,X303)|icext(X303,uri_rdfs_Literal),inference(resolution,[status(thm)],[c123, c56])).
% 3.32/3.55  fof(rdfs_annotation_seealso_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_seeAlso,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_seealso_domain)).
% 3.32/3.55  cnf(c122,plain,iext(uri_rdfs_domain,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_seealso_domain])).
% 3.32/3.55  cnf(c366,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X302)|iext(X302,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(resolution,[status(thm)],[c122, c30])).
% 3.32/3.55  fof(rdfs_annotation_seealso_range,axiom,iext(uri_rdfs_range,uri_rdfs_seeAlso,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_seealso_range)).
% 3.32/3.55  cnf(c121,plain,iext(uri_rdfs_range,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_seealso_range])).
% 3.32/3.55  cnf(c363,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X301)|iext(X301,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(resolution,[status(thm)],[c121, c30])).
% 3.32/3.55  fof(rdfs_collection_first_domain,axiom,iext(uri_rdfs_domain,uri_rdf_first,uri_rdf_List),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_collection_first_domain)).
% 3.32/3.55  cnf(c111,plain,iext(uri_rdfs_domain,uri_rdf_first,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdfs_collection_first_domain])).
% 3.32/3.55  cnf(c360,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X298)|iext(X298,uri_rdf_first,uri_rdf_List),inference(resolution,[status(thm)],[c111, c30])).
% 3.32/3.55  cnf(c364,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X297)|icext(X297,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c122, c82])).
% 3.32/3.55  cnf(c361,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X295)|icext(X295,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c121, c82])).
% 3.32/3.55  fof(rdfs_collection_first_range,axiom,iext(uri_rdfs_range,uri_rdf_first,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_collection_first_range)).
% 3.32/3.55  cnf(c110,plain,iext(uri_rdfs_range,uri_rdf_first,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_collection_first_range])).
% 3.32/3.55  cnf(c357,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X294)|iext(X294,uri_rdf_first,uri_rdfs_Resource),inference(resolution,[status(thm)],[c110, c30])).
% 3.32/3.55  cnf(c358,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X292)|icext(X292,uri_rdf_first),inference(resolution,[status(thm)],[c111, c82])).
% 3.32/3.55  cnf(c354,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X290)|iext(X290,uri_rdf_rest,uri_rdf_List),inference(resolution,[status(thm)],[c109, c30])).
% 3.32/3.55  cnf(c355,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X289)|icext(X289,uri_rdf_first),inference(resolution,[status(thm)],[c110, c82])).
% 3.32/3.55  cnf(c353,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X288)|icext(X288,uri_rdf_List),inference(resolution,[status(thm)],[c109, c56])).
% 3.32/3.55  cnf(c352,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X287)|icext(X287,uri_rdf_rest),inference(resolution,[status(thm)],[c109, c82])).
% 3.32/3.55  cnf(c351,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X284)|iext(X284,uri_rdf_rest,uri_rdf_List),inference(resolution,[status(thm)],[c108, c30])).
% 3.32/3.55  cnf(c345,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X283)|iext(X283,uri_rdf_Alt,uri_rdfs_Container),inference(resolution,[status(thm)],[c107, c30])).
% 3.32/3.55  cnf(c343,plain,~iext(uri_rdfs_subClassOf,X282,uri_rdf_Alt)|iext(uri_rdfs_subClassOf,X282,uri_rdfs_Container),inference(resolution,[status(thm)],[c107, c34])).
% 3.32/3.55  cnf(c335,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X281)|iext(X281,uri_rdf_Bag,uri_rdfs_Container),inference(resolution,[status(thm)],[c106, c30])).
% 3.32/3.55  cnf(c349,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X279)|icext(X279,uri_rdf_rest),inference(resolution,[status(thm)],[c108, c82])).
% 3.32/3.55  cnf(c333,plain,~iext(uri_rdfs_subClassOf,X277,uri_rdf_Bag)|iext(uri_rdfs_subClassOf,X277,uri_rdfs_Container),inference(resolution,[status(thm)],[c106, c34])).
% 3.32/3.55  cnf(c341,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X276)|icext(X276,uri_rdf_Alt),inference(resolution,[status(thm)],[c107, c82])).
% 3.32/3.55  cnf(c331,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X274)|icext(X274,uri_rdf_Bag),inference(resolution,[status(thm)],[c106, c82])).
% 3.32/3.55  fof(rdfs_type_range,axiom,iext(uri_rdfs_range,uri_rdf_type,uri_rdfs_Class),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_type_range)).
% 3.32/3.55  cnf(c15,plain,iext(uri_rdfs_range,uri_rdf_type,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_type_range])).
% 3.32/3.55  cnf(c324,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X273)|icext(X273,uri_rdf_type),inference(resolution,[status(thm)],[c82, c15])).
% 3.32/3.55  fof(rdfs_value_range,axiom,iext(uri_rdfs_range,uri_rdf_value,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_value_range)).
% 3.32/3.55  cnf(c13,plain,iext(uri_rdfs_range,uri_rdf_value,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_value_range])).
% 3.32/3.55  cnf(c323,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X272)|icext(X272,uri_rdf_value),inference(resolution,[status(thm)],[c82, c13])).
% 3.32/3.55  fof(rdfs_container_n_domain_003,axiom,iext(uri_rdfs_domain,uri_rdf__3,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_domain_003)).
% 3.32/3.55  cnf(c97,plain,iext(uri_rdfs_domain,uri_rdf__3,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_003])).
% 3.32/3.55  cnf(c322,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X271)|icext(X271,uri_rdf__3),inference(resolution,[status(thm)],[c82, c97])).
% 3.32/3.55  fof(rdfs_container_n_domain_002,axiom,iext(uri_rdfs_domain,uri_rdf__2,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_domain_002)).
% 3.32/3.55  cnf(c98,plain,iext(uri_rdfs_domain,uri_rdf__2,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_002])).
% 3.32/3.55  cnf(c321,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X270)|icext(X270,uri_rdf__2),inference(resolution,[status(thm)],[c82, c98])).
% 3.32/3.55  cnf(c320,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X269)|icext(X269,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c82, c84])).
% 3.32/3.55  cnf(c8,plain,iext(uri_rdf_first,skolem0004,uri_ex_u),inference(split_conjunct,[status(thm)],[c1])).
% 3.32/3.55  cnf(c319,plain,~iext(uri_rdfs_domain,uri_rdf_first,X268)|icext(X268,skolem0004),inference(resolution,[status(thm)],[c82, c8])).
% 3.32/3.55  cnf(c4,plain,iext(uri_rdf_first,skolem0003,uri_ex_w),inference(split_conjunct,[status(thm)],[c1])).
% 3.32/3.55  cnf(c317,plain,~iext(uri_rdfs_domain,uri_rdf_first,X266)|icext(X266,skolem0003),inference(resolution,[status(thm)],[c82, c4])).
% 3.32/3.55  cnf(c316,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X265)|icext(X265,uri_rdfs_domain),inference(resolution,[status(thm)],[c82, c77])).
% 3.32/3.55  fof(rdfs_reification_subject_domain,axiom,iext(uri_rdfs_domain,uri_rdf_subject,uri_rdfs_Statement),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_reification_subject_domain)).
% 3.32/3.55  cnf(c48,plain,iext(uri_rdfs_domain,uri_rdf_subject,uri_rdfs_Statement),inference(split_conjunct,[status(thm)],[rdfs_reification_subject_domain])).
% 3.32/3.55  cnf(c315,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X264)|icext(X264,uri_rdf_subject),inference(resolution,[status(thm)],[c82, c48])).
% 3.32/3.55  cnf(c3,plain,iext(uri_owl_oneOf,skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c1])).
% 3.32/3.55  cnf(c314,plain,~iext(uri_rdfs_domain,uri_owl_oneOf,X263)|icext(X263,skolem0001),inference(resolution,[status(thm)],[c82, c3])).
% 3.32/3.55  cnf(c312,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X261)|icext(X261,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c82, c102])).
% 3.32/3.55  cnf(c311,plain,~iext(uri_rdfs_domain,uri_owl_oneOf,X260)|icext(X260,skolem0002),inference(resolution,[status(thm)],[c82, c7])).
% 3.32/3.55  fof(rdfs_reification_predicate_range,axiom,iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_reification_predicate_range)).
% 3.32/3.55  cnf(c49,plain,iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_reification_predicate_range])).
% 3.32/3.55  cnf(c309,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X258)|icext(X258,uri_rdf_predicate),inference(resolution,[status(thm)],[c82, c49])).
% 3.32/3.55  fof(rdfs_container_n_range_003,axiom,iext(uri_rdfs_range,uri_rdf__3,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_range_003)).
% 3.32/3.55  cnf(c94,plain,iext(uri_rdfs_range,uri_rdf__3,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_range_003])).
% 3.32/3.55  cnf(c308,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X257)|icext(X257,uri_rdf__3),inference(resolution,[status(thm)],[c82, c94])).
% 3.32/3.55  cnf(c307,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X256)|icext(X256,uri_ex_p),inference(resolution,[status(thm)],[c82, c6])).
% 3.32/3.55  fof(rdfs_subclassof_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdfs_Class),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_subclassof_domain)).
% 3.32/3.55  cnf(c46,plain,iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_subclassof_domain])).
% 3.32/3.55  cnf(c306,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X255)|icext(X255,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c82, c46])).
% 3.32/3.55  fof(rdfs_reification_subject_range,axiom,iext(uri_rdfs_range,uri_rdf_subject,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_reification_subject_range)).
% 3.32/3.55  cnf(c47,plain,iext(uri_rdfs_range,uri_rdf_subject,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_reification_subject_range])).
% 3.32/3.55  cnf(c304,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X253)|icext(X253,uri_rdf_subject),inference(resolution,[status(thm)],[c82, c47])).
% 3.32/3.55  cnf(c303,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X252)|icext(X252,uri_rdfs_Seq),inference(resolution,[status(thm)],[c82, c90])).
% 3.32/3.55  fof(rdfs_subclassof_range,axiom,iext(uri_rdfs_range,uri_rdfs_subClassOf,uri_rdfs_Class),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_subclassof_range)).
% 3.32/3.55  cnf(c38,plain,iext(uri_rdfs_range,uri_rdfs_subClassOf,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_subclassof_range])).
% 3.32/3.55  cnf(c302,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X251)|icext(X251,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c82, c38])).
% 3.32/3.55  fof(rdfs_container_member_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_member,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_member_domain)).
% 3.32/3.55  cnf(c101,plain,iext(uri_rdfs_domain,uri_rdfs_member,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_member_domain])).
% 3.32/3.55  cnf(c301,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X250)|icext(X250,uri_rdfs_member),inference(resolution,[status(thm)],[c82, c101])).
% 3.32/3.55  cnf(c299,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X248)|icext(X248,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c82, c89])).
% 3.32/3.55  cnf(c298,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X247)|icext(X247,uri_rdfs_range),inference(resolution,[status(thm)],[c82, c57])).
% 3.32/3.55  fof(rdfs_subpropertyof_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_subpropertyof_domain)).
% 3.32/3.55  cnf(c31,plain,iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_subpropertyof_domain])).
% 3.32/3.55  cnf(c296,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X245)|icext(X245,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c82, c31])).
% 3.32/3.55  fof(rdfs_container_n_range_001,axiom,iext(uri_rdfs_range,uri_rdf__1,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_range_001)).
% 3.32/3.55  cnf(c96,plain,iext(uri_rdfs_range,uri_rdf__1,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_range_001])).
% 3.32/3.55  cnf(c295,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X244)|icext(X244,uri_rdf__1),inference(resolution,[status(thm)],[c82, c96])).
% 3.32/3.55  fof(rdfs_type_domain,axiom,iext(uri_rdfs_domain,uri_rdf_type,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_type_domain)).
% 3.32/3.55  cnf(c16,plain,iext(uri_rdfs_domain,uri_rdf_type,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_type_domain])).
% 3.32/3.55  cnf(c294,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X243)|icext(X243,uri_rdf_type),inference(resolution,[status(thm)],[c82, c16])).
% 3.32/3.55  fof(rdfs_container_n_domain_001,axiom,iext(uri_rdfs_domain,uri_rdf__1,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_domain_001)).
% 3.32/3.55  cnf(c99,plain,iext(uri_rdfs_domain,uri_rdf__1,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_001])).
% 3.32/3.55  cnf(c293,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X242)|icext(X242,uri_rdf__1),inference(resolution,[status(thm)],[c82, c99])).
% 3.32/3.55  fof(rdfs_subpropertyof_range,axiom,iext(uri_rdfs_range,uri_rdfs_subPropertyOf,uri_rdf_Property),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_subpropertyof_range)).
% 3.32/3.55  cnf(c23,plain,iext(uri_rdfs_range,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_subpropertyof_range])).
% 3.32/3.55  cnf(c291,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X240)|icext(X240,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c82, c23])).
% 3.32/3.55  fof(rdfs_reification_object_domain,axiom,iext(uri_rdfs_domain,uri_rdf_object,uri_rdfs_Statement),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_reification_object_domain)).
% 3.32/3.55  cnf(c52,plain,iext(uri_rdfs_domain,uri_rdf_object,uri_rdfs_Statement),inference(split_conjunct,[status(thm)],[rdfs_reification_object_domain])).
% 3.32/3.55  cnf(c290,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X239)|icext(X239,uri_rdf_object),inference(resolution,[status(thm)],[c82, c52])).
% 3.32/3.55  fof(rdfs_value_domain,axiom,iext(uri_rdfs_domain,uri_rdf_value,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_value_domain)).
% 3.32/3.55  cnf(c14,plain,iext(uri_rdfs_domain,uri_rdf_value,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_value_domain])).
% 3.32/3.55  cnf(c287,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X236)|icext(X236,uri_rdf_value),inference(resolution,[status(thm)],[c82, c14])).
% 3.32/3.55  fof(rdfs_container_member_range,axiom,iext(uri_rdfs_range,uri_rdfs_member,uri_rdfs_Resource),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_container_member_range)).
% 3.32/3.55  cnf(c100,plain,iext(uri_rdfs_range,uri_rdfs_member,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_member_range])).
% 3.32/3.55  cnf(c286,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X235)|icext(X235,uri_rdfs_member),inference(resolution,[status(thm)],[c82, c100])).
% 3.32/3.55  cnf(c285,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X234)|icext(X234,uri_rdfs_range),inference(resolution,[status(thm)],[c82, c53])).
% 3.32/3.55  cnf(c284,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X233)|icext(X233,uri_rdf__2),inference(resolution,[status(thm)],[c82, c95])).
% 3.32/3.55  cnf(c279,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X231)|iext(X231,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),inference(resolution,[status(thm)],[c102, c30])).
% 3.32/3.55  cnf(c282,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X230)|icext(X230,uri_rdfs_domain),inference(factor,[status(thm)],[c82])).
% 3.32/3.55  cnf(c416,plain,~iext(uri_rdfs_domain,uri_rdf_type,X227)|icext(X227,X228),inference(resolution,[status(thm)],[c401, c82])).
% 3.32/3.55  cnf(c278,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X225)|icext(X225,uri_rdf_Property),inference(resolution,[status(thm)],[c102, c56])).
% 3.32/3.55  cnf(c277,plain,~iext(uri_rdfs_subClassOf,X220,uri_rdfs_ContainerMembershipProperty)|iext(uri_rdfs_subClassOf,X220,uri_rdf_Property),inference(resolution,[status(thm)],[c102, c34])).
% 3.32/3.55  cnf(c45,plain,~iext(uri_rdfs_subClassOf,X78,X80)|~icext(X78,X79)|icext(X80,X79),inference(split_conjunct,[status(thm)],[c42])).
% 3.32/3.55  cnf(c340,plain,~icext(uri_rdf_Alt,X193)|icext(uri_rdfs_Container,X193),inference(resolution,[status(thm)],[c107, c45])).
% 3.32/3.55  cnf(c330,plain,~icext(uri_rdf_Bag,X192)|icext(uri_rdfs_Container,X192),inference(resolution,[status(thm)],[c106, c45])).
% 3.32/3.55  cnf(c268,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X191)|icext(X191,uri_rdfs_Class),inference(resolution,[status(thm)],[c56, c84])).
% 3.32/3.55  cnf(c275,plain,~icext(uri_rdfs_ContainerMembershipProperty,X190)|icext(uri_rdf_Property,X190),inference(resolution,[status(thm)],[c102, c45])).
% 3.32/3.55  cnf(c267,plain,~iext(uri_rdfs_range,uri_rdf_first,X189)|icext(X189,uri_ex_u),inference(resolution,[status(thm)],[c56, c8])).
% 3.32/3.55  cnf(c265,plain,~iext(uri_rdfs_range,uri_rdf_first,X187)|icext(X187,uri_ex_w),inference(resolution,[status(thm)],[c56, c4])).
% 3.32/3.55  cnf(c262,plain,~iext(uri_rdfs_range,uri_owl_oneOf,X184)|icext(X184,skolem0003),inference(resolution,[status(thm)],[c56, c3])).
% 3.32/3.55  cnf(c260,plain,~iext(uri_rdfs_range,uri_owl_oneOf,X182)|icext(X182,skolem0004),inference(resolution,[status(thm)],[c56, c7])).
% 3.32/3.55  cnf(c255,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X177)|icext(X177,uri_rdfs_Class),inference(resolution,[status(thm)],[c56, c46])).
% 3.32/3.55  cnf(c254,plain,~iext(uri_rdfs_range,uri_rdf_rest,X176)|icext(X176,uri_rdf_nil),inference(resolution,[status(thm)],[c56, c5])).
% 3.32/3.55  cnf(c252,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X174)|icext(X174,uri_rdfs_Container),inference(resolution,[status(thm)],[c56, c90])).
% 3.32/3.55  fof(rdfs_property_type,axiom,iext(uri_rdf_type,uri_rdf_Property,uri_rdfs_Class),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_property_type)).
% 3.32/3.55  cnf(c58,plain,iext(uri_rdf_type,uri_rdf_Property,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_property_type])).
% 3.32/3.55  cnf(c249,plain,~iext(uri_rdfs_range,uri_rdf_type,X171)|icext(X171,uri_rdfs_Class),inference(resolution,[status(thm)],[c56, c58])).
% 3.32/3.55  cnf(c248,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X170)|icext(X170,uri_rdfs_Literal),inference(resolution,[status(thm)],[c56, c89])).
% 3.32/3.55  cnf(c1065,plain,icext(uri_rdf_Property,uri_rdfs_member),inference(resolution,[status(thm)],[c774, c119])).
% 3.32/3.55  cnf(c246,plain,~iext(uri_rdfs_range,uri_rdf_type,X168)|icext(X168,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c56, c92])).
% 3.32/3.55  cnf(c1035,plain,icext(uri_rdf_Property,uri_owl_oneOf),inference(resolution,[status(thm)],[c586, c119])).
% 3.32/3.55  cnf(c1020,plain,icext(uri_rdf_Property,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c584, c119])).
% 3.32/3.55  fof(rdfs_dat_xmlliteral_type,axiom,iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Datatype),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_dat_xmlliteral_type)).
% 3.32/3.55  cnf(c88,plain,iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Datatype),inference(split_conjunct,[status(thm)],[rdfs_dat_xmlliteral_type])).
% 3.32/3.55  cnf(c241,plain,~iext(uri_rdfs_range,uri_rdf_type,X163)|icext(X163,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c56, c88])).
% 3.32/3.55  cnf(c1001,plain,icext(uri_rdf_Property,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c582, c119])).
% 3.32/3.55  cnf(c240,plain,~iext(uri_rdfs_range,uri_rdfs_range,X162)|icext(X162,uri_rdf_Property),inference(resolution,[status(thm)],[c56, c23])).
% 3.32/3.55  cnf(c968,plain,icext(uri_rdf_Property,uri_rdfs_range),inference(resolution,[status(thm)],[c580, c119])).
% 3.32/3.56  cnf(c237,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X159)|icext(X159,uri_rdf_Property),inference(resolution,[status(thm)],[c56, c83])).
% 3.32/3.56  cnf(c236,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X158)|icext(X158,uri_rdfs_Resource),inference(resolution,[status(thm)],[c56, c14])).
% 3.32/3.56  cnf(c938,plain,icext(uri_rdf_Property,uri_rdfs_domain),inference(resolution,[status(thm)],[c578, c119])).
% 3.32/3.56  cnf(c234,plain,~iext(uri_rdfs_range,uri_rdfs_range,X156)|icext(X156,uri_rdfs_Class),inference(resolution,[status(thm)],[c56, c53])).
% 3.32/3.56  cnf(c233,plain,~iext(uri_rdfs_range,uri_rdfs_range,X155)|icext(X155,uri_rdfs_Resource),inference(resolution,[status(thm)],[c56, c95])).
% 3.32/3.56  cnf(c231,plain,~iext(uri_rdfs_range,uri_rdfs_range,X153)|icext(X153,X153),inference(factor,[status(thm)],[c56])).
% 3.32/3.56  cnf(c227,plain,~icext(uri_rdfs_Datatype,X152)|icext(uri_rdfs_Class,X152),inference(resolution,[status(thm)],[c45, c84])).
% 3.32/3.56  cnf(c226,plain,~icext(uri_rdfs_Seq,X151)|icext(uri_rdfs_Container,X151),inference(resolution,[status(thm)],[c45, c90])).
% 3.32/3.56  cnf(c225,plain,~icext(uri_rdf_XMLLiteral,X150)|icext(uri_rdfs_Literal,X150),inference(resolution,[status(thm)],[c45, c89])).
% 3.32/3.56  cnf(c204,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X149)|iext(X149,uri_rdfs_member,uri_rdfs_Resource),inference(resolution,[status(thm)],[c101, c30])).
% 3.32/3.56  cnf(c203,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X148)|iext(X148,uri_rdfs_member,uri_rdfs_Resource),inference(resolution,[status(thm)],[c100, c30])).
% 3.32/3.56  cnf(c875,plain,icext(uri_rdf_Property,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c454, c119])).
% 3.32/3.56  cnf(c868,plain,icext(uri_rdf_Property,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c453, c119])).
% 3.32/3.56  cnf(c202,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X147)|iext(X147,uri_rdf__1,uri_rdfs_Resource),inference(resolution,[status(thm)],[c99, c30])).
% 3.32/3.56  cnf(c201,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X146)|iext(X146,uri_rdf__2,uri_rdfs_Resource),inference(resolution,[status(thm)],[c98, c30])).
% 3.32/3.56  cnf(c200,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X145)|iext(X145,uri_rdf__3,uri_rdfs_Resource),inference(resolution,[status(thm)],[c97, c30])).
% 3.32/3.56  cnf(c199,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X144)|iext(X144,uri_rdf__1,uri_rdfs_Resource),inference(resolution,[status(thm)],[c96, c30])).
% 3.32/3.56  cnf(c198,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X143)|iext(X143,uri_rdf__2,uri_rdfs_Resource),inference(resolution,[status(thm)],[c95, c30])).
% 3.32/3.56  cnf(c197,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X142)|iext(X142,uri_rdf__3,uri_rdfs_Resource),inference(resolution,[status(thm)],[c94, c30])).
% 3.32/3.56  cnf(c196,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X141)|iext(X141,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c93, c30])).
% 3.32/3.56  cnf(c195,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X140)|iext(X140,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c92, c30])).
% 3.32/3.56  cnf(c194,plain,~iext(uri_rdfs_subClassOf,X139,uri_rdfs_Datatype)|iext(uri_rdfs_subClassOf,X139,uri_rdfs_Class),inference(resolution,[status(thm)],[c34, c84])).
% 3.32/3.56  cnf(c193,plain,~iext(uri_rdfs_subClassOf,X138,uri_rdfs_Seq)|iext(uri_rdfs_subClassOf,X138,uri_rdfs_Container),inference(resolution,[status(thm)],[c34, c90])).
% 3.32/3.56  cnf(c192,plain,~iext(uri_rdfs_subClassOf,X137,uri_rdf_XMLLiteral)|iext(uri_rdfs_subClassOf,X137,uri_rdfs_Literal),inference(resolution,[status(thm)],[c34, c89])).
% 3.32/3.56  cnf(c190,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X135)|iext(X135,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c91, c30])).
% 3.32/3.56  cnf(c189,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X134)|iext(X134,uri_rdfs_Seq,uri_rdfs_Container),inference(resolution,[status(thm)],[c90, c30])).
% 3.32/3.56  cnf(c188,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X133)|iext(X133,uri_rdf_XMLLiteral,uri_rdfs_Literal),inference(resolution,[status(thm)],[c89, c30])).
% 3.32/3.56  cnf(c187,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X132)|iext(X132,uri_rdf_XMLLiteral,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c88, c30])).
% 3.32/3.56  cnf(c186,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X131)|iext(X131,uri_rdfs_Datatype,uri_rdfs_Class),inference(resolution,[status(thm)],[c84, c30])).
% 3.32/3.56  cnf(c185,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X130)|iext(X130,uri_rdf_type,uri_rdfs_Class),inference(resolution,[status(thm)],[c30, c15])).
% 3.32/3.56  cnf(c184,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X129)|iext(X129,uri_rdf_value,uri_rdfs_Resource),inference(resolution,[status(thm)],[c30, c13])).
% 3.32/3.56  cnf(c183,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_first,X128)|iext(X128,skolem0004,uri_ex_u),inference(resolution,[status(thm)],[c30, c8])).
% 3.32/3.56  cnf(c182,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_first,X127)|iext(X127,skolem0003,uri_ex_w),inference(resolution,[status(thm)],[c30, c4])).
% 3.32/3.56  cnf(c181,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X126)|iext(X126,uri_rdfs_domain,uri_rdfs_Class),inference(resolution,[status(thm)],[c30, c77])).
% 3.32/3.56  cnf(c180,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X125)|iext(X125,uri_rdf_subject,uri_rdfs_Statement),inference(resolution,[status(thm)],[c30, c48])).
% 3.32/3.56  cnf(c179,plain,~iext(uri_rdfs_subPropertyOf,uri_owl_oneOf,X124)|iext(X124,skolem0001,skolem0003),inference(resolution,[status(thm)],[c30, c3])).
% 3.32/3.56  cnf(c178,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X123)|iext(X123,skolem0004,uri_rdf_nil),inference(resolution,[status(thm)],[c30, c9])).
% 3.32/3.56  cnf(c177,plain,~iext(uri_rdfs_subPropertyOf,uri_owl_oneOf,X122)|iext(X122,skolem0002,skolem0004),inference(resolution,[status(thm)],[c30, c7])).
% 3.32/3.56  cnf(c176,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X121)|iext(X121,uri_rdf_predicate,uri_rdfs_Resource),inference(resolution,[status(thm)],[c30, c49])).
% 3.32/3.56  cnf(c175,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X120)|iext(X120,uri_ex_p,skolem0002),inference(resolution,[status(thm)],[c30, c6])).
% 3.32/3.56  cnf(c174,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X119)|iext(X119,uri_rdfs_subClassOf,uri_rdfs_Class),inference(resolution,[status(thm)],[c30, c46])).
% 3.32/3.56  cnf(c173,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X118)|iext(X118,skolem0003,uri_rdf_nil),inference(resolution,[status(thm)],[c30, c5])).
% 3.32/3.56  cnf(c172,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X117)|iext(X117,uri_rdf_subject,uri_rdfs_Resource),inference(resolution,[status(thm)],[c30, c47])).
% 3.32/3.56  cnf(c171,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X116)|iext(X116,uri_rdfs_subClassOf,uri_rdfs_Class),inference(resolution,[status(thm)],[c30, c38])).
% 3.32/3.56  cnf(c170,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X115)|iext(X115,uri_rdf_Property,uri_rdfs_Class),inference(resolution,[status(thm)],[c30, c58])).
% 3.32/3.56  cnf(c169,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X114)|iext(X114,uri_rdfs_range,uri_rdf_Property),inference(resolution,[status(thm)],[c30, c57])).
% 3.32/3.56  cnf(c168,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X113)|iext(X113,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c30, c31])).
% 3.32/3.56  cnf(c167,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X112)|iext(X112,uri_rdf_type,uri_rdfs_Resource),inference(resolution,[status(thm)],[c30, c16])).
% 3.32/3.56  cnf(c166,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X111)|iext(X111,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c30, c23])).
% 3.32/3.56  cnf(c165,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X110)|iext(X110,uri_rdf_object,uri_rdfs_Statement),inference(resolution,[status(thm)],[c30, c52])).
% 3.32/3.56  cnf(c164,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X109)|iext(X109,uri_ex_p,skolem0001),inference(resolution,[status(thm)],[c30, c2])).
% 3.32/3.56  cnf(c163,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X108)|iext(X108,uri_rdfs_domain,uri_rdf_Property),inference(resolution,[status(thm)],[c30, c83])).
% 3.32/3.56  cnf(c162,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X107)|iext(X107,uri_rdf_value,uri_rdfs_Resource),inference(resolution,[status(thm)],[c30, c14])).
% 3.32/3.56  cnf(c161,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X106)|iext(X106,uri_rdfs_range,uri_rdfs_Class),inference(resolution,[status(thm)],[c30, c53])).
% 3.32/3.56  cnf(c160,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X105)|iext(X105,uri_rdf_predicate,uri_rdfs_Statement),inference(resolution,[status(thm)],[c30, c50])).
% 3.32/3.56  cnf(c159,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X104)|iext(X104,uri_rdfs_subPropertyOf,X104),inference(factor,[status(thm)],[c30])).
% 3.32/3.56  cnf(c502,plain,icext(uri_rdf_Property,uri_rdf_first),inference(resolution,[status(thm)],[c146, c119])).
% 3.32/3.56  cnf(c497,plain,icext(uri_rdf_List,uri_rdf_nil),inference(resolution,[status(thm)],[c145, c119])).
% 3.32/3.56  cnf(c488,plain,icext(uri_rdf_Property,uri_rdf_rest),inference(resolution,[status(thm)],[c144, c119])).
% 3.32/3.56  cnf(c481,plain,icext(uri_rdf_Property,uri_rdf__1),inference(resolution,[status(thm)],[c143, c119])).
% 3.32/3.56  cnf(c472,plain,icext(uri_rdf_Property,uri_rdf__2),inference(resolution,[status(thm)],[c142, c119])).
% 3.32/3.56  cnf(c465,plain,icext(uri_rdf_Property,uri_rdf__3),inference(resolution,[status(thm)],[c141, c119])).
% 3.32/3.56  cnf(c457,plain,icext(uri_rdf_Property,uri_rdf_object),inference(resolution,[status(thm)],[c140, c119])).
% 3.32/3.56  cnf(c445,plain,icext(uri_rdf_Property,uri_rdf_value),inference(resolution,[status(thm)],[c139, c119])).
% 3.32/3.56  cnf(c436,plain,icext(uri_rdf_Property,uri_rdf_subject),inference(resolution,[status(thm)],[c138, c119])).
% 3.32/3.56  cnf(c431,plain,icext(uri_rdf_Property,uri_rdf_type),inference(resolution,[status(thm)],[c130, c119])).
% 3.32/3.56  cnf(c391,plain,icext(uri_rdfs_Datatype,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c119, c88])).
% 3.32/3.56  fof(rdfs_datatype_instsub_literal,axiom,(![D]:(icext(uri_rdfs_Datatype,D)=>iext(uri_rdfs_subClassOf,D,uri_rdfs_Literal))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_datatype_instsub_literal)).
% 3.32/3.56  fof(c85,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.32/3.56  fof(c86,plain,(![X35]:(~icext(uri_rdfs_Datatype,X35)|iext(uri_rdfs_subClassOf,X35,uri_rdfs_Literal))),inference(variable_rename,[status(thm)],[c85])).
% 3.32/3.56  cnf(c87,plain,~icext(uri_rdfs_Datatype,X89)|iext(uri_rdfs_subClassOf,X89,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[c86])).
% 3.32/3.56  cnf(c281,plain,icext(uri_rdfs_Class,uri_rdf_Property),inference(resolution,[status(thm)],[c274, c75])).
% 3.32/3.56  fof(rdfs_lv_def,axiom,(![X]:(lv(X)<=>icext(uri_rdfs_Literal,X))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB003+0.ax', rdfs_lv_def)).
% 3.32/3.56  fof(c59,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.32/3.56  fof(c60,plain,((![X]:(~lv(X)|icext(uri_rdfs_Literal,X)))&(![X]:(~icext(uri_rdfs_Literal,X)|lv(X)))),inference(shift_quantors,[status(thm)],[c59])).
% 3.32/3.56  fof(c62,plain,(![X25]:(![X26]:((~lv(X25)|icext(uri_rdfs_Literal,X25))&(~icext(uri_rdfs_Literal,X26)|lv(X26))))),inference(shift_quantors,[status(thm)],[fof(c61,plain,((![X25]:(~lv(X25)|icext(uri_rdfs_Literal,X25)))&(![X26]:(~icext(uri_rdfs_Literal,X26)|lv(X26)))),inference(variable_rename,[status(thm)],[c60])).])).
% 3.32/3.56  cnf(c64,plain,~icext(uri_rdfs_Literal,X58)|lv(X58),inference(split_conjunct,[status(thm)],[c62])).
% 3.32/3.56  cnf(c63,plain,~lv(X57)|icext(uri_rdfs_Literal,X57),inference(split_conjunct,[status(thm)],[c62])).
% 3.32/3.56  fof(testcase_conclusion_fullish_026_Inferred_Property_Characteristics_I,conjecture,iext(uri_rdf_type,uri_ex_p,uri_owl_InverseFunctionalProperty),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', testcase_conclusion_fullish_026_Inferred_Property_Characteristics_I)).
% 3.32/3.56  fof(c10,negated_conjecture,(~iext(uri_rdf_type,uri_ex_p,uri_owl_InverseFunctionalProperty)),inference(assume_negation,[status(cth)],[testcase_conclusion_fullish_026_Inferred_Property_Characteristics_I])).
% 3.32/3.56  fof(c11,negated_conjecture,~iext(uri_rdf_type,uri_ex_p,uri_owl_InverseFunctionalProperty),inference(fof_simplification,[status(thm)],[c10])).
% 3.32/3.56  cnf(c12,negated_conjecture,~iext(uri_rdf_type,uri_ex_p,uri_owl_InverseFunctionalProperty),inference(split_conjunct,[status(thm)],[c11])).
% 3.32/3.56  % SZS output end Saturation
% 3.32/3.56  
% 3.32/3.56  % Initial clauses    : 98
% 3.32/3.56  % Processed clauses  : 578
% 3.32/3.56  % Factors computed   : 5
% 3.32/3.56  % Resolvents computed: 1349
% 3.32/3.56  % Tautologies deleted: 53
% 3.32/3.56  % Forward subsumed   : 821
% 3.32/3.56  % Backward subsumed  : 1
% 3.32/3.56  % -------- CPU Time ---------
% 3.32/3.56  % User time          : 3.169 s
% 3.32/3.56  % System time        : 0.015 s
% 3.32/3.56  % Total time         : 3.184 s
%------------------------------------------------------------------------------