%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SWB035+1 : TPTP v8.1.2. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n014.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:58 EDT 2024
% Result : Satisfiable 2.76s 3.00s
% Output : Saturation 2.83s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SWB035+1 : TPTP v8.1.2. Released v5.2.0.
% 0.03/0.12 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.34 % Computer : n014.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Wed May 8 22:13:23 EDT 2024
% 0.12/0.34 % CPUTime :
% 2.76/3.00 % Version: 1.5
% 2.76/3.00 % SZS status Satisfiable
% 2.76/3.00 % SZS output start Saturation
% 2.76/3.00 fof(rdfs_subpropertyof_main,axiom,(![P]:(![Q]:(iext(uri_rdfs_subPropertyOf,P,Q)=>((ip(P)&ip(Q))&(![X]:(![Y]:(iext(P,X,Y)=>iext(Q,X,Y)))))))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_subpropertyof_main)).
% 2.76/3.00 fof(c11,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])).
% 2.76/3.00 fof(c13,plain,(![X6]:(![X7]:(![X8]:(![X9]:(~iext(uri_rdfs_subPropertyOf,X6,X7)|((ip(X6)&ip(X7))&(~iext(X6,X8,X9)|iext(X7,X8,X9)))))))),inference(shift_quantors,[status(thm)],[fof(c12,plain,(![X6]:(![X7]:(~iext(uri_rdfs_subPropertyOf,X6,X7)|((ip(X6)&ip(X7))&(![X8]:(![X9]:(~iext(X6,X8,X9)|iext(X7,X8,X9)))))))),inference(variable_rename,[status(thm)],[c11])).])).
% 2.76/3.00 fof(c14,plain,(![X6]:(![X7]:(![X8]:(![X9]:(((~iext(uri_rdfs_subPropertyOf,X6,X7)|ip(X6))&(~iext(uri_rdfs_subPropertyOf,X6,X7)|ip(X7)))&(~iext(uri_rdfs_subPropertyOf,X6,X7)|(~iext(X6,X8,X9)|iext(X7,X8,X9)))))))),inference(distribute,[status(thm)],[c13])).
% 2.76/3.00 cnf(c17,plain,~iext(uri_rdfs_subPropertyOf,X65,X64)|~iext(X65,X63,X62)|iext(X64,X63,X62),inference(split_conjunct,[status(thm)],[c14])).
% 2.76/3.00 fof(rdfs_subpropertyof_reflex,axiom,(![P]:(ip(P)=>iext(uri_rdfs_subPropertyOf,P,P))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_subpropertyof_reflex)).
% 2.76/3.00 fof(c7,plain,(![P]:(~ip(P)|iext(uri_rdfs_subPropertyOf,P,P))),inference(fof_nnf,[status(thm)],[rdfs_subpropertyof_reflex])).
% 2.76/3.00 fof(c8,plain,(![X5]:(~ip(X5)|iext(uri_rdfs_subPropertyOf,X5,X5))),inference(variable_rename,[status(thm)],[c7])).
% 2.76/3.00 cnf(c9,plain,~ip(X50)|iext(uri_rdfs_subPropertyOf,X50,X50),inference(split_conjunct,[status(thm)],[c8])).
% 2.76/3.00 fof(rdf_type_ip,axiom,(![P]:(iext(uri_rdf_type,P,uri_rdf_Property)<=>ip(P))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdf_type_ip)).
% 2.76/3.00 fof(c119,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])).
% 2.76/3.00 fof(c120,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)],[c119])).
% 2.76/3.00 fof(c122,plain,(![X38]:(![X39]:((~iext(uri_rdf_type,X38,uri_rdf_Property)|ip(X38))&(~ip(X39)|iext(uri_rdf_type,X39,uri_rdf_Property))))),inference(shift_quantors,[status(thm)],[fof(c121,plain,((![X38]:(~iext(uri_rdf_type,X38,uri_rdf_Property)|ip(X38)))&(![X39]:(~ip(X39)|iext(uri_rdf_type,X39,uri_rdf_Property)))),inference(variable_rename,[status(thm)],[c120])).])).
% 2.76/3.00 cnf(c123,plain,~iext(uri_rdf_type,X94,uri_rdf_Property)|ip(X94),inference(split_conjunct,[status(thm)],[c122])).
% 2.76/3.00 fof(rdfs_cext_def,axiom,(![X]:(![C]:(iext(uri_rdf_type,X,C)<=>icext(C,X)))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_cext_def)).
% 2.76/3.00 fof(c102,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])).
% 2.76/3.00 fof(c103,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)],[c102])).
% 2.76/3.00 fof(c105,plain,(![X34]:(![X35]:(![X36]:(![X37]:((~iext(uri_rdf_type,X34,X35)|icext(X35,X34))&(~icext(X37,X36)|iext(uri_rdf_type,X36,X37))))))),inference(shift_quantors,[status(thm)],[fof(c104,plain,((![X34]:(![X35]:(~iext(uri_rdf_type,X34,X35)|icext(X35,X34))))&(![X36]:(![X37]:(~icext(X37,X36)|iext(uri_rdf_type,X36,X37))))),inference(variable_rename,[status(thm)],[c103])).])).
% 2.76/3.00 cnf(c107,plain,~icext(X90,X91)|iext(uri_rdf_type,X91,X90),inference(split_conjunct,[status(thm)],[c105])).
% 2.76/3.00 fof(rdfs_range_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_range,uri_rdf_Property),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_range_domain)).
% 2.76/3.00 cnf(c44,plain,iext(uri_rdfs_domain,uri_rdfs_range,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_range_domain])).
% 2.76/3.00 fof(rdfs_domain_main,axiom,(![P]:(![C]:(![X]:(![Y]:((iext(uri_rdfs_domain,P,C)&iext(P,X,Y))=>icext(C,X)))))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_domain_main)).
% 2.76/3.00 fof(c65,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])).
% 2.76/3.00 fof(c66,plain,(![P]:(![C]:(![X]:((~iext(uri_rdfs_domain,P,C)|(![Y]:~iext(P,X,Y)))|icext(C,X))))),inference(shift_quantors,[status(thm)],[c65])).
% 2.76/3.00 fof(c68,plain,(![X27]:(![X28]:(![X29]:(![X30]:((~iext(uri_rdfs_domain,X27,X28)|~iext(X27,X29,X30))|icext(X28,X29)))))),inference(shift_quantors,[status(thm)],[fof(c67,plain,(![X27]:(![X28]:(![X29]:((~iext(uri_rdfs_domain,X27,X28)|(![X30]:~iext(X27,X29,X30)))|icext(X28,X29))))),inference(variable_rename,[status(thm)],[c66])).])).
% 2.76/3.00 cnf(c69,plain,~iext(uri_rdfs_domain,X82,X83)|~iext(X82,X84,X81)|icext(X83,X84),inference(split_conjunct,[status(thm)],[c68])).
% 2.76/3.00 fof(rdfs_annotation_comment_range,axiom,iext(uri_rdfs_range,uri_rdfs_comment,uri_rdfs_Literal),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_comment_range)).
% 2.76/3.00 cnf(c115,plain,iext(uri_rdfs_range,uri_rdfs_comment,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[rdfs_annotation_comment_range])).
% 2.76/3.00 cnf(c361,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X284)|icext(X284,uri_rdfs_comment),inference(resolution,[status(thm)],[c115, c69])).
% 2.76/3.00 cnf(c1150,plain,icext(uri_rdf_Property,uri_rdfs_comment),inference(resolution,[status(thm)],[c361, c44])).
% 2.76/3.00 cnf(c1152,plain,iext(uri_rdf_type,uri_rdfs_comment,uri_rdf_Property),inference(resolution,[status(thm)],[c1150, c107])).
% 2.76/3.00 cnf(c1157,plain,ip(uri_rdfs_comment),inference(resolution,[status(thm)],[c1152, c123])).
% 2.76/3.00 cnf(c1160,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_comment,uri_rdfs_comment),inference(resolution,[status(thm)],[c1157, c9])).
% 2.76/3.00 cnf(c1163,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X578)|iext(X578,uri_rdfs_comment,uri_rdfs_comment),inference(resolution,[status(thm)],[c1160, c17])).
% 2.76/3.00 cnf(c1154,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X577)|iext(X577,uri_rdfs_comment,uri_rdf_Property),inference(resolution,[status(thm)],[c1152, c17])).
% 2.76/3.01 fof(rdfs_annotation_label_range,axiom,iext(uri_rdfs_range,uri_rdfs_label,uri_rdfs_Literal),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_label_range)).
% 2.76/3.01 cnf(c110,plain,iext(uri_rdfs_range,uri_rdfs_label,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[rdfs_annotation_label_range])).
% 2.76/3.01 cnf(c331,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X270)|icext(X270,uri_rdfs_label),inference(resolution,[status(thm)],[c110, c69])).
% 2.76/3.01 cnf(c1124,plain,icext(uri_rdf_Property,uri_rdfs_label),inference(resolution,[status(thm)],[c331, c44])).
% 2.76/3.01 cnf(c1125,plain,iext(uri_rdf_type,uri_rdfs_label,uri_rdf_Property),inference(resolution,[status(thm)],[c1124, c107])).
% 2.76/3.01 cnf(c1130,plain,ip(uri_rdfs_label),inference(resolution,[status(thm)],[c1125, c123])).
% 2.76/3.01 cnf(c1134,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_label,uri_rdfs_label),inference(resolution,[status(thm)],[c1130, c9])).
% 2.76/3.01 cnf(c1136,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X575)|iext(X575,uri_rdfs_label,uri_rdfs_label),inference(resolution,[status(thm)],[c1134, c17])).
% 2.76/3.01 cnf(c1127,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X574)|iext(X574,uri_rdfs_label,uri_rdf_Property),inference(resolution,[status(thm)],[c1125, c17])).
% 2.76/3.01 fof(rdfs_subclassof_reflex,axiom,(![C]:(ic(C)=>iext(uri_rdfs_subClassOf,C,C))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_subclassof_reflex)).
% 2.76/3.01 fof(c22,plain,(![C]:(~ic(C)|iext(uri_rdfs_subClassOf,C,C))),inference(fof_nnf,[status(thm)],[rdfs_subclassof_reflex])).
% 2.76/3.01 fof(c23,plain,(![X13]:(~ic(X13)|iext(uri_rdfs_subClassOf,X13,X13))),inference(variable_rename,[status(thm)],[c22])).
% 2.76/3.01 cnf(c24,plain,~ic(X69)|iext(uri_rdfs_subClassOf,X69,X69),inference(split_conjunct,[status(thm)],[c23])).
% 2.76/3.01 fof(rdfs_ic_def,axiom,(![X]:(ic(X)<=>icext(uri_rdfs_Class,X))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_ic_def)).
% 2.76/3.01 fof(c58,plain,(![X]:((~ic(X)|icext(uri_rdfs_Class,X))&(~icext(uri_rdfs_Class,X)|ic(X)))),inference(fof_nnf,[status(thm)],[rdfs_ic_def])).
% 2.76/3.01 fof(c59,plain,((![X]:(~ic(X)|icext(uri_rdfs_Class,X)))&(![X]:(~icext(uri_rdfs_Class,X)|ic(X)))),inference(shift_quantors,[status(thm)],[c58])).
% 2.76/3.01 fof(c61,plain,(![X25]:(![X26]:((~ic(X25)|icext(uri_rdfs_Class,X25))&(~icext(uri_rdfs_Class,X26)|ic(X26))))),inference(shift_quantors,[status(thm)],[fof(c60,plain,((![X25]:(~ic(X25)|icext(uri_rdfs_Class,X25)))&(![X26]:(~icext(uri_rdfs_Class,X26)|ic(X26)))),inference(variable_rename,[status(thm)],[c59])).])).
% 2.76/3.01 cnf(c63,plain,~icext(uri_rdfs_Class,X59)|ic(X59),inference(split_conjunct,[status(thm)],[c61])).
% 2.76/3.01 fof(rdfs_range_range,axiom,iext(uri_rdfs_range,uri_rdfs_range,uri_rdfs_Class),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_range_range)).
% 2.76/3.01 cnf(c40,plain,iext(uri_rdfs_range,uri_rdfs_range,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_range_range])).
% 2.76/3.01 fof(rdfs_range_main,axiom,(![P]:(![C]:(![X]:(![Y]:((iext(uri_rdfs_range,P,C)&iext(P,X,Y))=>icext(C,Y)))))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_range_main)).
% 2.76/3.01 fof(c41,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])).
% 2.76/3.01 fof(c42,plain,(![X17]:(![X18]:(![X19]:(![X20]:((~iext(uri_rdfs_range,X17,X18)|~iext(X17,X19,X20))|icext(X18,X20)))))),inference(variable_rename,[status(thm)],[c41])).
% 2.76/3.01 cnf(c43,plain,~iext(uri_rdfs_range,X78,X77)|~iext(X78,X79,X80)|icext(X77,X80),inference(split_conjunct,[status(thm)],[c42])).
% 2.76/3.01 fof(rdfs_collection_rest_range,axiom,iext(uri_rdfs_range,uri_rdf_rest,uri_rdf_List),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_collection_rest_range)).
% 2.76/3.01 cnf(c95,plain,iext(uri_rdfs_range,uri_rdf_rest,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdfs_collection_rest_range])).
% 2.76/3.01 cnf(c312,plain,~iext(uri_rdfs_range,uri_rdfs_range,X250)|icext(X250,uri_rdf_List),inference(resolution,[status(thm)],[c95, c43])).
% 2.76/3.01 cnf(c1084,plain,icext(uri_rdfs_Class,uri_rdf_List),inference(resolution,[status(thm)],[c312, c40])).
% 2.76/3.01 cnf(c1086,plain,ic(uri_rdf_List),inference(resolution,[status(thm)],[c1084, c63])).
% 2.76/3.01 cnf(c1088,plain,iext(uri_rdfs_subClassOf,uri_rdf_List,uri_rdf_List),inference(resolution,[status(thm)],[c1086, c24])).
% 2.76/3.01 cnf(c1108,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X572)|iext(X572,uri_rdf_List,uri_rdf_List),inference(resolution,[status(thm)],[c1088, c17])).
% 2.76/3.01 fof(rdfs_subclassof_trans,axiom,(![C]:(![D]:(![E]:((iext(uri_rdfs_subClassOf,C,D)&iext(uri_rdfs_subClassOf,D,E))=>iext(uri_rdfs_subClassOf,C,E))))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_subclassof_trans)).
% 2.76/3.01 fof(c19,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])).
% 2.76/3.01 fof(c20,plain,(![X10]:(![X11]:(![X12]:((~iext(uri_rdfs_subClassOf,X10,X11)|~iext(uri_rdfs_subClassOf,X11,X12))|iext(uri_rdfs_subClassOf,X10,X12))))),inference(variable_rename,[status(thm)],[c19])).
% 2.76/3.01 cnf(c21,plain,~iext(uri_rdfs_subClassOf,X66,X68)|~iext(uri_rdfs_subClassOf,X68,X67)|iext(uri_rdfs_subClassOf,X66,X67),inference(split_conjunct,[status(thm)],[c20])).
% 2.76/3.01 fof(rdfs_class_instsub_resource,axiom,(![C]:(ic(C)=>iext(uri_rdfs_subClassOf,C,uri_rdfs_Resource))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_class_instsub_resource)).
% 2.76/3.01 fof(c99,plain,(![C]:(~ic(C)|iext(uri_rdfs_subClassOf,C,uri_rdfs_Resource))),inference(fof_nnf,[status(thm)],[rdfs_class_instsub_resource])).
% 2.76/3.01 fof(c100,plain,(![X33]:(~ic(X33)|iext(uri_rdfs_subClassOf,X33,uri_rdfs_Resource))),inference(variable_rename,[status(thm)],[c99])).
% 2.76/3.01 cnf(c101,plain,~ic(X87)|iext(uri_rdfs_subClassOf,X87,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[c100])).
% 2.76/3.01 cnf(c1087,plain,iext(uri_rdfs_subClassOf,uri_rdf_List,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1086, c101])).
% 2.76/3.01 cnf(c1102,plain,~iext(uri_rdfs_subClassOf,X571,uri_rdf_List)|iext(uri_rdfs_subClassOf,X571,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1087, c21])).
% 2.76/3.01 cnf(c1100,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X570)|iext(X570,uri_rdf_List,uri_rdfs_Resource),inference(resolution,[status(thm)],[c1087, c17])).
% 2.76/3.01 cnf(c1085,plain,iext(uri_rdf_type,uri_rdf_List,uri_rdfs_Class),inference(resolution,[status(thm)],[c1084, c107])).
% 2.76/3.01 cnf(c1092,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X569)|iext(X569,uri_rdf_List,uri_rdfs_Class),inference(resolution,[status(thm)],[c1085, c17])).
% 2.76/3.01 fof(rdfs_domain_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_Property),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_domain_domain)).
% 2.76/3.01 cnf(c70,plain,iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_domain_domain])).
% 2.76/3.01 fof(rdfs_reification_predicate_domain,axiom,iext(uri_rdfs_domain,uri_rdf_predicate,uri_rdfs_Statement),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_reification_predicate_domain)).
% 2.76/3.01 cnf(c37,plain,iext(uri_rdfs_domain,uri_rdf_predicate,uri_rdfs_Statement),inference(split_conjunct,[status(thm)],[rdfs_reification_predicate_domain])).
% 2.76/3.01 cnf(c273,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X217)|icext(X217,uri_rdf_predicate),inference(resolution,[status(thm)],[c69, c37])).
% 2.76/3.01 cnf(c1041,plain,icext(uri_rdf_Property,uri_rdf_predicate),inference(resolution,[status(thm)],[c273, c70])).
% 2.76/3.01 cnf(c1042,plain,iext(uri_rdf_type,uri_rdf_predicate,uri_rdf_Property),inference(resolution,[status(thm)],[c1041, c107])).
% 2.76/3.01 cnf(c1045,plain,ip(uri_rdf_predicate),inference(resolution,[status(thm)],[c1042, c123])).
% 2.76/3.01 cnf(c1050,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_predicate,uri_rdf_predicate),inference(resolution,[status(thm)],[c1045, c9])).
% 2.76/3.01 cnf(c1056,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X568)|iext(X568,uri_rdf_predicate,uri_rdf_predicate),inference(resolution,[status(thm)],[c1050, c17])).
% 2.76/3.01 cnf(c1047,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X566)|iext(X566,uri_rdf_predicate,uri_rdf_Property),inference(resolution,[status(thm)],[c1042, c17])).
% 2.76/3.01 fof(rdfs_domain_range,axiom,iext(uri_rdfs_range,uri_rdfs_domain,uri_rdfs_Class),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_domain_range)).
% 2.76/3.01 cnf(c64,plain,iext(uri_rdfs_range,uri_rdfs_domain,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_domain_range])).
% 2.76/3.01 fof(rdfs_reification_subject_domain,axiom,iext(uri_rdfs_domain,uri_rdf_subject,uri_rdfs_Statement),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_reification_subject_domain)).
% 2.76/3.01 cnf(c35,plain,iext(uri_rdfs_domain,uri_rdf_subject,uri_rdfs_Statement),inference(split_conjunct,[status(thm)],[rdfs_reification_subject_domain])).
% 2.76/3.01 cnf(c231,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X151)|icext(X151,uri_rdfs_Statement),inference(resolution,[status(thm)],[c43, c35])).
% 2.76/3.01 cnf(c887,plain,icext(uri_rdfs_Class,uri_rdfs_Statement),inference(resolution,[status(thm)],[c231, c64])).
% 2.76/3.01 cnf(c890,plain,ic(uri_rdfs_Statement),inference(resolution,[status(thm)],[c887, c63])).
% 2.76/3.01 cnf(c892,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Statement,uri_rdfs_Statement),inference(resolution,[status(thm)],[c890, c24])).
% 2.76/3.01 cnf(c1030,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X565)|iext(X565,uri_rdfs_Statement,uri_rdfs_Statement),inference(resolution,[status(thm)],[c892, c17])).
% 2.76/3.01 cnf(c891,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Statement,uri_rdfs_Resource),inference(resolution,[status(thm)],[c890, c101])).
% 2.76/3.01 cnf(c1022,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X563)|iext(X563,uri_rdfs_Statement,uri_rdfs_Resource),inference(resolution,[status(thm)],[c891, c17])).
% 2.76/3.01 cnf(c1016,plain,~iext(uri_rdfs_subClassOf,X562,uri_rdfs_Statement)|iext(uri_rdfs_subClassOf,X562,uri_rdfs_Resource),inference(resolution,[status(thm)],[c891, c21])).
% 2.76/3.01 cnf(c889,plain,iext(uri_rdf_type,uri_rdfs_Statement,uri_rdfs_Class),inference(resolution,[status(thm)],[c887, c107])).
% 2.76/3.01 cnf(c1014,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X561)|iext(X561,uri_rdfs_Statement,uri_rdfs_Class),inference(resolution,[status(thm)],[c889, c17])).
% 2.76/3.01 cnf(c16,plain,~iext(uri_rdfs_subPropertyOf,X61,X60)|ip(X60),inference(split_conjunct,[status(thm)],[c14])).
% 2.76/3.01 fof(rdfs_container_containermembershipproperty_instsub_member,axiom,(![P]:(icext(uri_rdfs_ContainerMembershipProperty,P)=>iext(uri_rdfs_subPropertyOf,P,uri_rdfs_member))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_containermembershipproperty_instsub_member)).
% 2.76/3.01 fof(c90,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])).
% 2.76/3.01 fof(c91,plain,(![X32]:(~icext(uri_rdfs_ContainerMembershipProperty,X32)|iext(uri_rdfs_subPropertyOf,X32,uri_rdfs_member))),inference(variable_rename,[status(thm)],[c90])).
% 2.76/3.01 cnf(c92,plain,~icext(uri_rdfs_ContainerMembershipProperty,X86)|iext(uri_rdfs_subPropertyOf,X86,uri_rdfs_member),inference(split_conjunct,[status(thm)],[c91])).
% 2.76/3.01 fof(rdfs_container_n_type_002,axiom,iext(uri_rdf_type,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_type_002)).
% 2.76/3.01 cnf(c79,plain,iext(uri_rdf_type,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),inference(split_conjunct,[status(thm)],[rdfs_container_n_type_002])).
% 2.76/3.01 cnf(c106,plain,~iext(uri_rdf_type,X88,X89)|icext(X89,X88),inference(split_conjunct,[status(thm)],[c105])).
% 2.76/3.01 cnf(c363,plain,icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__2),inference(resolution,[status(thm)],[c106, c79])).
% 2.76/3.01 cnf(c368,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__2,uri_rdfs_member),inference(resolution,[status(thm)],[c363, c92])).
% 2.76/3.01 cnf(c723,plain,ip(uri_rdfs_member),inference(resolution,[status(thm)],[c368, c16])).
% 2.76/3.01 cnf(c729,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_member,uri_rdfs_member),inference(resolution,[status(thm)],[c723, c9])).
% 2.76/3.01 cnf(c1007,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X560)|iext(X560,uri_rdfs_member,uri_rdfs_member),inference(resolution,[status(thm)],[c729, c17])).
% 2.76/3.01 cnf(c124,plain,~ip(X95)|iext(uri_rdf_type,X95,uri_rdf_Property),inference(split_conjunct,[status(thm)],[c122])).
% 2.76/3.01 cnf(c728,plain,iext(uri_rdf_type,uri_rdfs_member,uri_rdf_Property),inference(resolution,[status(thm)],[c723, c124])).
% 2.76/3.01 cnf(c1000,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X558)|iext(X558,uri_rdfs_member,uri_rdf_Property),inference(resolution,[status(thm)],[c728, c17])).
% 2.76/3.01 cnf(c62,plain,~ic(X58)|icext(uri_rdfs_Class,X58),inference(split_conjunct,[status(thm)],[c61])).
% 2.76/3.01 fof(rdfs_subclassof_main,axiom,(![C]:(![D]:(iext(uri_rdfs_subClassOf,C,D)=>((ic(C)&ic(D))&(![X]:(icext(C,X)=>icext(D,X))))))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_subclassof_main)).
% 2.76/3.01 fof(c26,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])).
% 2.76/3.01 fof(c28,plain,(![X14]:(![X15]:(![X16]:(~iext(uri_rdfs_subClassOf,X14,X15)|((ic(X14)&ic(X15))&(~icext(X14,X16)|icext(X15,X16))))))),inference(shift_quantors,[status(thm)],[fof(c27,plain,(![X14]:(![X15]:(~iext(uri_rdfs_subClassOf,X14,X15)|((ic(X14)&ic(X15))&(![X16]:(~icext(X14,X16)|icext(X15,X16))))))),inference(variable_rename,[status(thm)],[c26])).])).
% 2.76/3.01 fof(c29,plain,(![X14]:(![X15]:(![X16]:(((~iext(uri_rdfs_subClassOf,X14,X15)|ic(X14))&(~iext(uri_rdfs_subClassOf,X14,X15)|ic(X15)))&(~iext(uri_rdfs_subClassOf,X14,X15)|(~icext(X14,X16)|icext(X15,X16))))))),inference(distribute,[status(thm)],[c28])).
% 2.76/3.01 cnf(c31,plain,~iext(uri_rdfs_subClassOf,X73,X72)|ic(X72),inference(split_conjunct,[status(thm)],[c29])).
% 2.76/3.01 fof(rdfs_container_bag_sub,axiom,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Container),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_bag_sub)).
% 2.76/3.01 cnf(c93,plain,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Container),inference(split_conjunct,[status(thm)],[rdfs_container_bag_sub])).
% 2.76/3.01 cnf(c206,plain,ic(uri_rdfs_Container),inference(resolution,[status(thm)],[c31, c93])).
% 2.76/3.01 cnf(c342,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Container,uri_rdfs_Resource),inference(resolution,[status(thm)],[c101, c206])).
% 2.76/3.01 cnf(c622,plain,ic(uri_rdfs_Resource),inference(resolution,[status(thm)],[c342, c31])).
% 2.76/3.01 cnf(c631,plain,icext(uri_rdfs_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c622, c62])).
% 2.76/3.01 cnf(c632,plain,iext(uri_rdf_type,uri_rdfs_Resource,uri_rdfs_Class),inference(resolution,[status(thm)],[c631, c107])).
% 2.76/3.01 cnf(c994,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X557)|iext(X557,uri_rdfs_Resource,uri_rdfs_Class),inference(resolution,[status(thm)],[c632, c17])).
% 2.76/3.01 cnf(c629,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Resource,uri_rdfs_Resource),inference(resolution,[status(thm)],[c622, c101])).
% 2.76/3.01 cnf(c987,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X556)|iext(X556,uri_rdfs_Resource,uri_rdfs_Resource),inference(resolution,[status(thm)],[c629, c17])).
% 2.76/3.01 fof(rdfs_annotation_isdefinedby_sub,axiom,iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_isdefinedby_sub)).
% 2.76/3.01 cnf(c112,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_sub])).
% 2.76/3.01 fof(simple_iext_property,axiom,(![S]:(![P]:(![O]:(iext(P,S,O)=>ip(P))))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', simple_iext_property)).
% 2.76/3.01 fof(c139,plain,(![S]:(![P]:(![O]:(~iext(P,S,O)|ip(P))))),inference(fof_nnf,[status(thm)],[simple_iext_property])).
% 2.76/3.01 fof(c140,plain,(![S]:(![P]:((![O]:~iext(P,S,O))|ip(P)))),inference(shift_quantors,[status(thm)],[c139])).
% 2.76/3.01 fof(c142,plain,(![X42]:(![X43]:(![X44]:(~iext(X43,X42,X44)|ip(X43))))),inference(shift_quantors,[status(thm)],[fof(c141,plain,(![X42]:(![X43]:((![X44]:~iext(X43,X42,X44))|ip(X43)))),inference(variable_rename,[status(thm)],[c140])).])).
% 2.76/3.01 cnf(c143,plain,~iext(X97,X96,X98)|ip(X97),inference(split_conjunct,[status(thm)],[c142])).
% 2.76/3.01 cnf(c530,plain,ip(uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c143, c112])).
% 2.76/3.01 cnf(c540,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c530, c9])).
% 2.76/3.01 cnf(c976,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X554)|iext(X554,uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c540, c17])).
% 2.76/3.01 cnf(c539,plain,iext(uri_rdf_type,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c530, c124])).
% 2.76/3.01 cnf(c968,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X552)|iext(X552,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c539, c17])).
% 2.76/3.01 cnf(c479,plain,ip(uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c143, c93])).
% 2.76/3.01 cnf(c538,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c479, c9])).
% 2.76/3.01 cnf(c957,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X551)|iext(X551,uri_rdfs_subClassOf,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c538, c17])).
% 2.76/3.01 cnf(c537,plain,iext(uri_rdf_type,uri_rdfs_subClassOf,uri_rdf_Property),inference(resolution,[status(thm)],[c479, c124])).
% 2.76/3.01 cnf(c946,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X549)|iext(X549,uri_rdfs_subClassOf,uri_rdf_Property),inference(resolution,[status(thm)],[c537, c17])).
% 2.76/3.01 cnf(c474,plain,ip(uri_rdfs_range),inference(resolution,[status(thm)],[c143, c64])).
% 2.76/3.01 cnf(c536,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_range,uri_rdfs_range),inference(resolution,[status(thm)],[c474, c9])).
% 2.76/3.01 cnf(c933,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X548)|iext(X548,uri_rdfs_range,uri_rdfs_range),inference(resolution,[status(thm)],[c536, c17])).
% 2.76/3.01 cnf(c535,plain,iext(uri_rdf_type,uri_rdfs_range,uri_rdf_Property),inference(resolution,[status(thm)],[c474, c124])).
% 2.76/3.01 cnf(c920,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X546)|iext(X546,uri_rdfs_range,uri_rdf_Property),inference(resolution,[status(thm)],[c535, c17])).
% 2.76/3.01 cnf(c473,plain,ip(uri_rdfs_domain),inference(resolution,[status(thm)],[c143, c35])).
% 2.76/3.01 cnf(c534,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,uri_rdfs_domain),inference(resolution,[status(thm)],[c473, c9])).
% 2.76/3.01 cnf(c904,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X545)|iext(X545,uri_rdfs_domain,uri_rdfs_domain),inference(resolution,[status(thm)],[c534, c17])).
% 2.76/3.01 cnf(c533,plain,iext(uri_rdf_type,uri_rdfs_domain,uri_rdf_Property),inference(resolution,[status(thm)],[c473, c124])).
% 2.76/3.01 cnf(c885,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X543)|iext(X543,uri_rdfs_domain,uri_rdf_Property),inference(resolution,[status(thm)],[c533, c17])).
% 2.76/3.01 fof(rdf_collection_first_type,axiom,iext(uri_rdf_type,uri_rdf_first,uri_rdf_Property),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdf_collection_first_type)).
% 2.76/3.01 cnf(c133,plain,iext(uri_rdf_type,uri_rdf_first,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_collection_first_type])).
% 2.76/3.01 cnf(c469,plain,ip(uri_rdf_first),inference(resolution,[status(thm)],[c133, c123])).
% 2.76/3.01 cnf(c471,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_first,uri_rdf_first),inference(resolution,[status(thm)],[c469, c9])).
% 2.76/3.01 cnf(c874,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X542)|iext(X542,uri_rdf_first,uri_rdf_first),inference(resolution,[status(thm)],[c471, c17])).
% 2.76/3.01 fof(rdf_collection_rest_type,axiom,iext(uri_rdf_type,uri_rdf_rest,uri_rdf_Property),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdf_collection_rest_type)).
% 2.76/3.01 cnf(c131,plain,iext(uri_rdf_type,uri_rdf_rest,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_collection_rest_type])).
% 2.76/3.01 cnf(c456,plain,ip(uri_rdf_rest),inference(resolution,[status(thm)],[c131, c123])).
% 2.76/3.01 cnf(c458,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_rest,uri_rdf_rest),inference(resolution,[status(thm)],[c456, c9])).
% 2.76/3.01 cnf(c867,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X540)|iext(X540,uri_rdf_rest,uri_rdf_rest),inference(resolution,[status(thm)],[c458, c17])).
% 2.76/3.01 fof(rdf_container_n_type_001,axiom,iext(uri_rdf_type,uri_rdf__1,uri_rdf_Property),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdf_container_n_type_001)).
% 2.76/3.01 cnf(c130,plain,iext(uri_rdf_type,uri_rdf__1,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_container_n_type_001])).
% 2.76/3.01 cnf(c447,plain,ip(uri_rdf__1),inference(resolution,[status(thm)],[c130, c123])).
% 2.76/3.01 cnf(c449,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__1,uri_rdf__1),inference(resolution,[status(thm)],[c447, c9])).
% 2.76/3.01 cnf(c860,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X538)|iext(X538,uri_rdf__1,uri_rdf__1),inference(resolution,[status(thm)],[c449, c17])).
% 2.76/3.01 fof(rdf_container_n_type_002,axiom,iext(uri_rdf_type,uri_rdf__2,uri_rdf_Property),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdf_container_n_type_002)).
% 2.76/3.01 cnf(c129,plain,iext(uri_rdf_type,uri_rdf__2,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_container_n_type_002])).
% 2.76/3.01 cnf(c440,plain,ip(uri_rdf__2),inference(resolution,[status(thm)],[c129, c123])).
% 2.76/3.01 cnf(c442,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__2,uri_rdf__2),inference(resolution,[status(thm)],[c440, c9])).
% 2.76/3.01 cnf(c852,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X536)|iext(X536,uri_rdf__2,uri_rdf__2),inference(resolution,[status(thm)],[c442, c17])).
% 2.76/3.01 fof(rdf_container_n_type_003,axiom,iext(uri_rdf_type,uri_rdf__3,uri_rdf_Property),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdf_container_n_type_003)).
% 2.76/3.01 cnf(c128,plain,iext(uri_rdf_type,uri_rdf__3,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_container_n_type_003])).
% 2.76/3.01 cnf(c432,plain,ip(uri_rdf__3),inference(resolution,[status(thm)],[c128, c123])).
% 2.76/3.01 cnf(c434,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__3,uri_rdf__3),inference(resolution,[status(thm)],[c432, c9])).
% 2.76/3.01 cnf(c845,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X534)|iext(X534,uri_rdf__3,uri_rdf__3),inference(resolution,[status(thm)],[c434, c17])).
% 2.76/3.01 cnf(c339,plain,ip(uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c112, c16])).
% 2.76/3.01 cnf(c425,plain,iext(uri_rdf_type,uri_rdfs_seeAlso,uri_rdf_Property),inference(resolution,[status(thm)],[c124, c339])).
% 2.76/3.01 cnf(c838,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X532)|iext(X532,uri_rdfs_seeAlso,uri_rdf_Property),inference(resolution,[status(thm)],[c425, c17])).
% 2.76/3.01 cnf(c15,plain,~iext(uri_rdfs_subPropertyOf,X54,X53)|ip(X54),inference(split_conjunct,[status(thm)],[c14])).
% 2.76/3.01 cnf(c336,plain,ip(uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c112, c15])).
% 2.76/3.01 cnf(c424,plain,iext(uri_rdf_type,uri_rdfs_isDefinedBy,uri_rdf_Property),inference(resolution,[status(thm)],[c124, c336])).
% 2.76/3.01 cnf(c830,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X531)|iext(X531,uri_rdfs_isDefinedBy,uri_rdf_Property),inference(resolution,[status(thm)],[c424, c17])).
% 2.76/3.01 fof(rdf_reification_object_type,axiom,iext(uri_rdf_type,uri_rdf_object,uri_rdf_Property),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdf_reification_object_type)).
% 2.76/3.01 cnf(c127,plain,iext(uri_rdf_type,uri_rdf_object,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_reification_object_type])).
% 2.76/3.01 cnf(c416,plain,ip(uri_rdf_object),inference(resolution,[status(thm)],[c123, c127])).
% 2.76/3.01 cnf(c420,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_object,uri_rdf_object),inference(resolution,[status(thm)],[c416, c9])).
% 2.76/3.01 cnf(c823,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X530)|iext(X530,uri_rdf_object,uri_rdf_object),inference(resolution,[status(thm)],[c420, c17])).
% 2.76/3.01 fof(rdf_reification_subject_type,axiom,iext(uri_rdf_type,uri_rdf_subject,uri_rdf_Property),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdf_reification_subject_type)).
% 2.76/3.01 cnf(c125,plain,iext(uri_rdf_type,uri_rdf_subject,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_reification_subject_type])).
% 2.76/3.01 cnf(c415,plain,ip(uri_rdf_subject),inference(resolution,[status(thm)],[c123, c125])).
% 2.76/3.01 cnf(c419,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_subject,uri_rdf_subject),inference(resolution,[status(thm)],[c415, c9])).
% 2.76/3.01 cnf(c815,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X528)|iext(X528,uri_rdf_subject,uri_rdf_subject),inference(resolution,[status(thm)],[c419, c17])).
% 2.76/3.01 fof(rdf_value_type,axiom,iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdf_value_type)).
% 2.76/3.01 cnf(c117,plain,iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_value_type])).
% 2.76/3.01 cnf(c414,plain,ip(uri_rdf_type),inference(resolution,[status(thm)],[c123, c117])).
% 2.76/3.01 cnf(c418,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_type,uri_rdf_type),inference(resolution,[status(thm)],[c414, c9])).
% 2.76/3.01 cnf(c804,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X526)|iext(X526,uri_rdf_type,uri_rdf_type),inference(resolution,[status(thm)],[c418, c17])).
% 2.76/3.01 fof(rdf_reification_predicate_type,axiom,iext(uri_rdf_type,uri_rdf_value,uri_rdf_Property),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdf_reification_predicate_type)).
% 2.76/3.01 cnf(c126,plain,iext(uri_rdf_type,uri_rdf_value,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdf_reification_predicate_type])).
% 2.76/3.01 cnf(c413,plain,ip(uri_rdf_value),inference(resolution,[status(thm)],[c123, c126])).
% 2.76/3.01 cnf(c417,plain,iext(uri_rdfs_subPropertyOf,uri_rdf_value,uri_rdf_value),inference(resolution,[status(thm)],[c413, c9])).
% 2.76/3.01 cnf(c795,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X524)|iext(X524,uri_rdf_value,uri_rdf_value),inference(resolution,[status(thm)],[c417, c17])).
% 2.76/3.01 fof(rdfs_dat_xmlliteral_sub,axiom,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Literal),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_dat_xmlliteral_sub)).
% 2.76/3.01 cnf(c76,plain,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[rdfs_dat_xmlliteral_sub])).
% 2.76/3.01 cnf(c210,plain,ic(uri_rdfs_Literal),inference(resolution,[status(thm)],[c31, c76])).
% 2.76/3.01 cnf(c225,plain,icext(uri_rdfs_Class,uri_rdfs_Literal),inference(resolution,[status(thm)],[c210, c62])).
% 2.76/3.01 cnf(c386,plain,iext(uri_rdf_type,uri_rdfs_Literal,uri_rdfs_Class),inference(resolution,[status(thm)],[c107, c225])).
% 2.76/3.01 cnf(c789,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X522)|iext(X522,uri_rdfs_Literal,uri_rdfs_Class),inference(resolution,[status(thm)],[c386, c17])).
% 2.76/3.01 fof(rdfs_container_seq_sub,axiom,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Container),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_seq_sub)).
% 2.76/3.01 cnf(c77,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Container),inference(split_conjunct,[status(thm)],[rdfs_container_seq_sub])).
% 2.76/3.01 cnf(c30,plain,~iext(uri_rdfs_subClassOf,X71,X70)|ic(X71),inference(split_conjunct,[status(thm)],[c29])).
% 2.76/3.01 cnf(c192,plain,ic(uri_rdfs_Seq),inference(resolution,[status(thm)],[c30, c77])).
% 2.76/3.01 cnf(c201,plain,icext(uri_rdfs_Class,uri_rdfs_Seq),inference(resolution,[status(thm)],[c192, c62])).
% 2.76/3.01 cnf(c381,plain,iext(uri_rdf_type,uri_rdfs_Seq,uri_rdfs_Class),inference(resolution,[status(thm)],[c107, c201])).
% 2.76/3.01 cnf(c784,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X521)|iext(X521,uri_rdfs_Seq,uri_rdfs_Class),inference(resolution,[status(thm)],[c381, c17])).
% 2.76/3.01 fof(rdfs_datatype_sub,axiom,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Class),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_datatype_sub)).
% 2.76/3.01 cnf(c71,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_datatype_sub])).
% 2.76/3.01 cnf(c191,plain,ic(uri_rdfs_Datatype),inference(resolution,[status(thm)],[c30, c71])).
% 2.76/3.01 cnf(c199,plain,icext(uri_rdfs_Class,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c191, c62])).
% 2.76/3.01 cnf(c380,plain,iext(uri_rdf_type,uri_rdfs_Datatype,uri_rdfs_Class),inference(resolution,[status(thm)],[c107, c199])).
% 2.76/3.01 cnf(c779,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X520)|iext(X520,uri_rdfs_Datatype,uri_rdfs_Class),inference(resolution,[status(thm)],[c380, c17])).
% 2.76/3.01 cnf(c190,plain,ic(uri_rdf_Bag),inference(resolution,[status(thm)],[c30, c93])).
% 2.76/3.01 cnf(c197,plain,icext(uri_rdfs_Class,uri_rdf_Bag),inference(resolution,[status(thm)],[c190, c62])).
% 2.76/3.01 cnf(c379,plain,iext(uri_rdf_type,uri_rdf_Bag,uri_rdfs_Class),inference(resolution,[status(thm)],[c107, c197])).
% 2.76/3.01 cnf(c774,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X519)|iext(X519,uri_rdf_Bag,uri_rdfs_Class),inference(resolution,[status(thm)],[c379, c17])).
% 2.76/3.01 cnf(c194,plain,ic(uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c30, c76])).
% 2.76/3.01 cnf(c205,plain,icext(uri_rdfs_Class,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c194, c62])).
% 2.76/3.01 cnf(c378,plain,iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Class),inference(resolution,[status(thm)],[c107, c205])).
% 2.76/3.01 cnf(c769,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X518)|iext(X518,uri_rdf_XMLLiteral,uri_rdfs_Class),inference(resolution,[status(thm)],[c378, c17])).
% 2.76/3.01 cnf(c215,plain,icext(uri_rdfs_Class,uri_rdfs_Container),inference(resolution,[status(thm)],[c206, c62])).
% 2.76/3.01 cnf(c377,plain,iext(uri_rdf_type,uri_rdfs_Container,uri_rdfs_Class),inference(resolution,[status(thm)],[c107, c215])).
% 2.76/3.01 cnf(c764,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X517)|iext(X517,uri_rdfs_Container,uri_rdfs_Class),inference(resolution,[status(thm)],[c377, c17])).
% 2.76/3.01 fof(rdfs_container_alt_sub,axiom,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Container),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_alt_sub)).
% 2.76/3.01 cnf(c94,plain,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Container),inference(split_conjunct,[status(thm)],[rdfs_container_alt_sub])).
% 2.76/3.01 cnf(c193,plain,ic(uri_rdf_Alt),inference(resolution,[status(thm)],[c30, c94])).
% 2.76/3.01 cnf(c203,plain,icext(uri_rdfs_Class,uri_rdf_Alt),inference(resolution,[status(thm)],[c193, c62])).
% 2.76/3.01 cnf(c376,plain,iext(uri_rdf_type,uri_rdf_Alt,uri_rdfs_Class),inference(resolution,[status(thm)],[c107, c203])).
% 2.76/3.01 cnf(c759,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X516)|iext(X516,uri_rdf_Alt,uri_rdfs_Class),inference(resolution,[status(thm)],[c376, c17])).
% 2.76/3.01 fof(rdfs_container_containermembershipproperty_sub,axiom,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_containermembershipproperty_sub)).
% 2.76/3.01 cnf(c89,plain,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_container_containermembershipproperty_sub])).
% 2.76/3.01 cnf(c195,plain,ic(uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c30, c89])).
% 2.76/3.01 cnf(c213,plain,icext(uri_rdfs_Class,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c195, c62])).
% 2.76/3.01 cnf(c374,plain,iext(uri_rdf_type,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Class),inference(resolution,[status(thm)],[c107, c213])).
% 2.76/3.01 cnf(c754,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X515)|iext(X515,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Class),inference(resolution,[status(thm)],[c374, c17])).
% 2.76/3.01 cnf(c207,plain,ic(uri_rdfs_Class),inference(resolution,[status(thm)],[c31, c71])).
% 2.76/3.01 cnf(c217,plain,icext(uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c207, c62])).
% 2.76/3.01 cnf(c373,plain,iext(uri_rdf_type,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c107, c217])).
% 2.76/3.01 cnf(c749,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X514)|iext(X514,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c373, c17])).
% 2.76/3.01 fof(rdfs_container_n_type_003,axiom,iext(uri_rdf_type,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_type_003)).
% 2.76/3.01 cnf(c78,plain,iext(uri_rdf_type,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),inference(split_conjunct,[status(thm)],[rdfs_container_n_type_003])).
% 2.76/3.01 cnf(c367,plain,icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__3),inference(resolution,[status(thm)],[c106, c78])).
% 2.76/3.01 cnf(c371,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__3,uri_rdfs_member),inference(resolution,[status(thm)],[c367, c92])).
% 2.76/3.01 cnf(c742,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X513)|iext(X513,uri_rdf__3,uri_rdfs_member),inference(resolution,[status(thm)],[c371, c17])).
% 2.76/3.01 fof(rdfs_subpropertyof_trans,axiom,(![P]:(![Q]:(![R]:((iext(uri_rdfs_subPropertyOf,P,Q)&iext(uri_rdfs_subPropertyOf,Q,R))=>iext(uri_rdfs_subPropertyOf,P,R))))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_subpropertyof_trans)).
% 2.76/3.01 fof(c4,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])).
% 2.76/3.01 fof(c5,plain,(![X2]:(![X3]:(![X4]:((~iext(uri_rdfs_subPropertyOf,X2,X3)|~iext(uri_rdfs_subPropertyOf,X3,X4))|iext(uri_rdfs_subPropertyOf,X2,X4))))),inference(variable_rename,[status(thm)],[c4])).
% 2.76/3.01 cnf(c6,plain,~iext(uri_rdfs_subPropertyOf,X47,X49)|~iext(uri_rdfs_subPropertyOf,X49,X48)|iext(uri_rdfs_subPropertyOf,X47,X48),inference(split_conjunct,[status(thm)],[c5])).
% 2.76/3.01 cnf(c741,plain,~iext(uri_rdfs_subPropertyOf,X512,uri_rdf__3)|iext(uri_rdfs_subPropertyOf,X512,uri_rdfs_member),inference(resolution,[status(thm)],[c371, c6])).
% 2.76/3.01 fof(rdfs_container_n_type_001,axiom,iext(uri_rdf_type,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_type_001)).
% 2.76/3.01 cnf(c80,plain,iext(uri_rdf_type,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),inference(split_conjunct,[status(thm)],[rdfs_container_n_type_001])).
% 2.76/3.01 cnf(c365,plain,icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__1),inference(resolution,[status(thm)],[c106, c80])).
% 2.76/3.01 cnf(c370,plain,iext(uri_rdfs_subPropertyOf,uri_rdf__1,uri_rdfs_member),inference(resolution,[status(thm)],[c365, c92])).
% 2.76/3.01 cnf(c735,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X511)|iext(X511,uri_rdf__1,uri_rdfs_member),inference(resolution,[status(thm)],[c370, c17])).
% 2.76/3.01 cnf(c734,plain,~iext(uri_rdfs_subPropertyOf,X510,uri_rdf__1)|iext(uri_rdfs_subPropertyOf,X510,uri_rdfs_member),inference(resolution,[status(thm)],[c370, c6])).
% 2.76/3.01 cnf(c725,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X509)|iext(X509,uri_rdf__2,uri_rdfs_member),inference(resolution,[status(thm)],[c368, c17])).
% 2.76/3.01 cnf(c724,plain,~iext(uri_rdfs_subPropertyOf,X508,uri_rdf__2)|iext(uri_rdfs_subPropertyOf,X508,uri_rdfs_member),inference(resolution,[status(thm)],[c368, c6])).
% 2.76/3.01 cnf(c353,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_seeAlso,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c339, c9])).
% 2.76/3.01 cnf(c717,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X507)|iext(X507,uri_rdfs_seeAlso,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c353, c17])).
% 2.76/3.01 cnf(c352,plain,iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c336, c9])).
% 2.76/3.01 cnf(c710,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X505)|iext(X505,uri_rdfs_isDefinedBy,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c352, c17])).
% 2.76/3.01 cnf(c1166,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X503)|icext(X503,uri_rdfs_comment),inference(resolution,[status(thm)],[c1160, c43])).
% 2.76/3.01 cnf(c351,plain,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Resource),inference(resolution,[status(thm)],[c101, c190])).
% 2.76/3.01 cnf(c704,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X502)|iext(X502,uri_rdf_Bag,uri_rdfs_Resource),inference(resolution,[status(thm)],[c351, c17])).
% 2.76/3.01 cnf(c1162,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X501)|icext(X501,uri_rdfs_comment),inference(resolution,[status(thm)],[c1160, c69])).
% 2.76/3.01 cnf(c698,plain,~iext(uri_rdfs_subClassOf,X498,uri_rdf_Bag)|iext(uri_rdfs_subClassOf,X498,uri_rdfs_Resource),inference(resolution,[status(thm)],[c351, c21])).
% 2.76/3.01 cnf(c1139,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X497)|icext(X497,uri_rdfs_label),inference(resolution,[status(thm)],[c1134, c43])).
% 2.76/3.01 cnf(c1135,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X496)|icext(X496,uri_rdfs_label),inference(resolution,[status(thm)],[c1134, c69])).
% 2.76/3.01 cnf(c350,plain,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Resource),inference(resolution,[status(thm)],[c101, c194])).
% 2.76/3.01 cnf(c696,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X494)|iext(X494,uri_rdf_XMLLiteral,uri_rdfs_Resource),inference(resolution,[status(thm)],[c350, c17])).
% 2.76/3.01 cnf(c1112,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X492)|icext(X492,uri_rdf_List),inference(resolution,[status(thm)],[c1088, c43])).
% 2.76/3.01 cnf(c690,plain,~iext(uri_rdfs_subClassOf,X490,uri_rdf_XMLLiteral)|iext(uri_rdfs_subClassOf,X490,uri_rdfs_Resource),inference(resolution,[status(thm)],[c350, c21])).
% 2.76/3.01 cnf(c1099,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X488)|icext(X488,uri_rdf_List),inference(resolution,[status(thm)],[c1087, c69])).
% 2.76/3.01 cnf(c349,plain,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Resource),inference(resolution,[status(thm)],[c101, c193])).
% 2.76/3.01 cnf(c688,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X486)|iext(X486,uri_rdf_Alt,uri_rdfs_Resource),inference(resolution,[status(thm)],[c349, c17])).
% 2.76/3.01 cnf(c1053,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X484)|icext(X484,uri_rdf_predicate),inference(resolution,[status(thm)],[c1050, c43])).
% 2.76/3.01 cnf(c682,plain,~iext(uri_rdfs_subClassOf,X483,uri_rdf_Alt)|iext(uri_rdfs_subClassOf,X483,uri_rdfs_Resource),inference(resolution,[status(thm)],[c349, c21])).
% 2.76/3.01 cnf(c1052,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X482)|icext(X482,uri_rdf_predicate),inference(resolution,[status(thm)],[c1050, c69])).
% 2.76/3.01 cnf(c348,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Literal,uri_rdfs_Resource),inference(resolution,[status(thm)],[c101, c210])).
% 2.76/3.01 cnf(c680,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X479)|iext(X479,uri_rdfs_Literal,uri_rdfs_Resource),inference(resolution,[status(thm)],[c348, c17])).
% 2.76/3.01 cnf(c1029,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X478)|icext(X478,uri_rdfs_Statement),inference(resolution,[status(thm)],[c892, c43])).
% 2.76/3.01 cnf(c674,plain,~iext(uri_rdfs_subClassOf,X475,uri_rdfs_Literal)|iext(uri_rdfs_subClassOf,X475,uri_rdfs_Resource),inference(resolution,[status(thm)],[c348, c21])).
% 2.76/3.01 cnf(c1019,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X474)|icext(X474,uri_rdfs_Statement),inference(resolution,[status(thm)],[c891, c69])).
% 2.76/3.01 cnf(c347,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Resource),inference(resolution,[status(thm)],[c101, c192])).
% 2.76/3.01 cnf(c672,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X471)|iext(X471,uri_rdfs_Seq,uri_rdfs_Resource),inference(resolution,[status(thm)],[c347, c17])).
% 2.76/3.01 cnf(c1003,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X469)|icext(X469,uri_rdfs_member),inference(resolution,[status(thm)],[c729, c69])).
% 2.76/3.01 cnf(c666,plain,~iext(uri_rdfs_subClassOf,X467,uri_rdfs_Seq)|iext(uri_rdfs_subClassOf,X467,uri_rdfs_Resource),inference(resolution,[status(thm)],[c347, c21])).
% 2.76/3.01 cnf(c346,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c101, c207])).
% 2.76/3.01 cnf(c664,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X462)|iext(X462,uri_rdfs_Class,uri_rdfs_Resource),inference(resolution,[status(thm)],[c346, c17])).
% 2.76/3.01 cnf(c984,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X461)|icext(X461,uri_rdfs_Resource),inference(resolution,[status(thm)],[c629, c69])).
% 2.76/3.01 cnf(c658,plain,~iext(uri_rdfs_subClassOf,X460,uri_rdfs_Class)|iext(uri_rdfs_subClassOf,X460,uri_rdfs_Resource),inference(resolution,[status(thm)],[c346, c21])).
% 2.76/3.01 cnf(c973,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X459)|icext(X459,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c540, c43])).
% 2.76/3.01 cnf(c972,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X458)|icext(X458,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c540, c69])).
% 2.76/3.01 cnf(c345,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Resource),inference(resolution,[status(thm)],[c101, c191])).
% 2.76/3.01 cnf(c656,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X456)|iext(X456,uri_rdfs_Datatype,uri_rdfs_Resource),inference(resolution,[status(thm)],[c345, c17])).
% 2.76/3.01 cnf(c953,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X454)|icext(X454,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c538, c43])).
% 2.76/3.01 cnf(c650,plain,~iext(uri_rdfs_subClassOf,X453,uri_rdfs_Datatype)|iext(uri_rdfs_subClassOf,X453,uri_rdfs_Resource),inference(resolution,[status(thm)],[c345, c21])).
% 2.76/3.01 cnf(c951,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X452)|icext(X452,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c538, c69])).
% 2.76/3.01 cnf(c211,plain,ic(uri_rdf_Property),inference(resolution,[status(thm)],[c31, c89])).
% 2.76/3.01 cnf(c344,plain,iext(uri_rdfs_subClassOf,uri_rdf_Property,uri_rdfs_Resource),inference(resolution,[status(thm)],[c101, c211])).
% 2.76/3.01 cnf(c648,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X449)|iext(X449,uri_rdf_Property,uri_rdfs_Resource),inference(resolution,[status(thm)],[c344, c17])).
% 2.76/3.01 cnf(c928,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X448)|icext(X448,uri_rdfs_range),inference(resolution,[status(thm)],[c536, c43])).
% 2.76/3.01 cnf(c924,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X447)|icext(X447,uri_rdfs_range),inference(resolution,[status(thm)],[c536, c69])).
% 2.76/3.01 cnf(c642,plain,~iext(uri_rdfs_subClassOf,X446,uri_rdf_Property)|iext(uri_rdfs_subClassOf,X446,uri_rdfs_Resource),inference(resolution,[status(thm)],[c344, c21])).
% 2.76/3.01 cnf(c898,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X443)|icext(X443,uri_rdfs_domain),inference(resolution,[status(thm)],[c534, c43])).
% 2.76/3.01 cnf(c343,plain,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Resource),inference(resolution,[status(thm)],[c101, c195])).
% 2.76/3.01 cnf(c640,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X442)|iext(X442,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Resource),inference(resolution,[status(thm)],[c343, c17])).
% 2.76/3.01 cnf(c895,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X441)|icext(X441,uri_rdfs_domain),inference(resolution,[status(thm)],[c534, c69])).
% 2.76/3.01 cnf(c634,plain,~iext(uri_rdfs_subClassOf,X438,uri_rdfs_ContainerMembershipProperty)|iext(uri_rdfs_subClassOf,X438,uri_rdfs_Resource),inference(resolution,[status(thm)],[c343, c21])).
% 2.76/3.01 cnf(c871,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X437)|icext(X437,uri_rdf_first),inference(resolution,[status(thm)],[c471, c43])).
% 2.76/3.01 cnf(c870,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X436)|icext(X436,uri_rdf_first),inference(resolution,[status(thm)],[c471, c69])).
% 2.76/3.01 cnf(c627,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X435)|iext(X435,uri_rdfs_Container,uri_rdfs_Resource),inference(resolution,[status(thm)],[c342, c17])).
% 2.76/3.01 cnf(c621,plain,~iext(uri_rdfs_subClassOf,X434,uri_rdfs_Container)|iext(uri_rdfs_subClassOf,X434,uri_rdfs_Resource),inference(resolution,[status(thm)],[c342, c21])).
% 2.76/3.01 cnf(c864,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X433)|icext(X433,uri_rdf_rest),inference(resolution,[status(thm)],[c458, c43])).
% 2.76/3.01 cnf(c863,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X432)|icext(X432,uri_rdf_rest),inference(resolution,[status(thm)],[c458, c69])).
% 2.76/3.01 cnf(c226,plain,iext(uri_rdfs_subClassOf,uri_rdf_Property,uri_rdf_Property),inference(resolution,[status(thm)],[c211, c24])).
% 2.76/3.01 cnf(c619,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X431)|iext(X431,uri_rdf_Property,uri_rdf_Property),inference(resolution,[status(thm)],[c226, c17])).
% 2.76/3.01 cnf(c857,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X430)|icext(X430,uri_rdf__1),inference(resolution,[status(thm)],[c449, c43])).
% 2.76/3.01 cnf(c849,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X428)|icext(X428,uri_rdf__2),inference(resolution,[status(thm)],[c442, c43])).
% 2.76/3.01 cnf(c842,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X425)|icext(X425,uri_rdf__3),inference(resolution,[status(thm)],[c434, c43])).
% 2.76/3.01 cnf(c224,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Literal,uri_rdfs_Literal),inference(resolution,[status(thm)],[c210, c24])).
% 2.76/3.01 cnf(c611,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X422)|iext(X422,uri_rdfs_Literal,uri_rdfs_Literal),inference(resolution,[status(thm)],[c224, c17])).
% 2.76/3.01 cnf(c820,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X418)|icext(X418,uri_rdf_object),inference(resolution,[status(thm)],[c420, c43])).
% 2.76/3.01 cnf(c819,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X416)|icext(X416,uri_rdf_object),inference(resolution,[status(thm)],[c420, c69])).
% 2.76/3.01 cnf(c812,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X415)|icext(X415,uri_rdf_subject),inference(resolution,[status(thm)],[c419, c43])).
% 2.76/3.01 cnf(c216,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c207, c24])).
% 2.76/3.01 cnf(c603,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X414)|iext(X414,uri_rdfs_Class,uri_rdfs_Class),inference(resolution,[status(thm)],[c216, c17])).
% 2.76/3.01 cnf(c811,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X413)|icext(X413,uri_rdf_subject),inference(resolution,[status(thm)],[c419, c69])).
% 2.76/3.01 cnf(c801,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X412)|icext(X412,uri_rdf_type),inference(resolution,[status(thm)],[c418, c43])).
% 2.76/3.01 cnf(c800,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X410)|icext(X410,uri_rdf_type),inference(resolution,[status(thm)],[c418, c69])).
% 2.76/3.01 cnf(c792,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X409)|icext(X409,uri_rdf_value),inference(resolution,[status(thm)],[c417, c43])).
% 2.76/3.01 cnf(c214,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Container,uri_rdfs_Container),inference(resolution,[status(thm)],[c206, c24])).
% 2.76/3.01 cnf(c595,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X408)|iext(X408,uri_rdfs_Container,uri_rdfs_Container),inference(resolution,[status(thm)],[c214, c17])).
% 2.76/3.01 cnf(c791,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X407)|icext(X407,uri_rdf_value),inference(resolution,[status(thm)],[c417, c69])).
% 2.76/3.01 cnf(c212,plain,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c195, c24])).
% 2.76/3.01 cnf(c587,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X397)|iext(X397,uri_rdfs_ContainerMembershipProperty,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c212, c17])).
% 2.76/3.01 cnf(c204,plain,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c194, c24])).
% 2.76/3.01 cnf(c579,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X386)|iext(X386,uri_rdf_XMLLiteral,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c204, c17])).
% 2.76/3.01 cnf(c738,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X383)|icext(X383,uri_rdf__3),inference(resolution,[status(thm)],[c371, c69])).
% 2.76/3.01 cnf(c731,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X380)|icext(X380,uri_rdf__1),inference(resolution,[status(thm)],[c370, c69])).
% 2.76/3.01 cnf(c722,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X379)|icext(X379,uri_rdfs_member),inference(resolution,[status(thm)],[c368, c43])).
% 2.76/3.01 cnf(c202,plain,iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdf_Alt),inference(resolution,[status(thm)],[c193, c24])).
% 2.76/3.01 cnf(c571,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X378)|iext(X378,uri_rdf_Alt,uri_rdf_Alt),inference(resolution,[status(thm)],[c202, c17])).
% 2.76/3.01 cnf(c721,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X377)|icext(X377,uri_rdf__2),inference(resolution,[status(thm)],[c368, c69])).
% 2.76/3.01 cnf(c713,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X375)|icext(X375,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c353, c69])).
% 2.76/3.01 cnf(c707,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X373)|icext(X373,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c352, c43])).
% 2.76/3.01 cnf(c200,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Seq),inference(resolution,[status(thm)],[c192, c24])).
% 2.76/3.01 cnf(c563,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X370)|iext(X370,uri_rdfs_Seq,uri_rdfs_Seq),inference(resolution,[status(thm)],[c200, c17])).
% 2.76/3.01 cnf(c198,plain,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c191, c24])).
% 2.76/3.01 cnf(c555,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X359)|iext(X359,uri_rdfs_Datatype,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c198, c17])).
% 2.76/3.01 cnf(c196,plain,iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdf_Bag),inference(resolution,[status(thm)],[c190, c24])).
% 2.76/3.01 cnf(c547,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X349)|iext(X349,uri_rdf_Bag,uri_rdf_Bag),inference(resolution,[status(thm)],[c196, c17])).
% 2.76/3.01 cnf(c626,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X348)|icext(X348,uri_rdfs_Resource),inference(resolution,[status(thm)],[c342, c43])).
% 2.76/3.01 cnf(c616,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X345)|icext(X345,uri_rdf_Property),inference(resolution,[status(thm)],[c226, c69])).
% 2.76/3.01 cnf(c608,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X342)|icext(X342,uri_rdfs_Literal),inference(resolution,[status(thm)],[c224, c69])).
% 2.76/3.01 cnf(c468,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X340)|iext(X340,uri_rdf_first,uri_rdf_Property),inference(resolution,[status(thm)],[c133, c17])).
% 2.76/3.01 cnf(c600,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X339)|icext(X339,uri_rdfs_Class),inference(resolution,[status(thm)],[c216, c69])).
% 2.76/3.01 fof(rdf_collection_nil_type,axiom,iext(uri_rdf_type,uri_rdf_nil,uri_rdf_List),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdf_collection_nil_type)).
% 2.76/3.01 cnf(c132,plain,iext(uri_rdf_type,uri_rdf_nil,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdf_collection_nil_type])).
% 2.76/3.01 cnf(c462,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X337)|iext(X337,uri_rdf_nil,uri_rdf_List),inference(resolution,[status(thm)],[c132, c17])).
% 2.76/3.01 cnf(c592,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X336)|icext(X336,uri_rdfs_Container),inference(resolution,[status(thm)],[c214, c69])).
% 2.76/3.01 cnf(c586,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X335)|icext(X335,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c212, c43])).
% 2.76/3.01 cnf(c455,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X333)|iext(X333,uri_rdf_rest,uri_rdf_Property),inference(resolution,[status(thm)],[c131, c17])).
% 2.76/3.01 cnf(c578,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X332)|icext(X332,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c204, c43])).
% 2.76/3.01 cnf(c446,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X330)|iext(X330,uri_rdf__1,uri_rdf_Property),inference(resolution,[status(thm)],[c130, c17])).
% 2.76/3.01 cnf(c570,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X329)|icext(X329,uri_rdf_Alt),inference(resolution,[status(thm)],[c202, c43])).
% 2.76/3.01 cnf(c562,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X327)|icext(X327,uri_rdfs_Seq),inference(resolution,[status(thm)],[c200, c43])).
% 2.76/3.01 cnf(c439,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X326)|iext(X326,uri_rdf__2,uri_rdf_Property),inference(resolution,[status(thm)],[c129, c17])).
% 2.76/3.01 cnf(c554,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X324)|icext(X324,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c198, c43])).
% 2.76/3.01 cnf(c431,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X322)|iext(X322,uri_rdf__3,uri_rdf_Property),inference(resolution,[status(thm)],[c128, c17])).
% 2.76/3.01 cnf(c546,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X321)|icext(X321,uri_rdf_Bag),inference(resolution,[status(thm)],[c196, c43])).
% 2.76/3.01 cnf(c412,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X318)|iext(X318,uri_rdf_object,uri_rdf_Property),inference(resolution,[status(thm)],[c127, c17])).
% 2.76/3.01 cnf(c460,plain,~iext(uri_rdfs_range,uri_rdf_type,X315)|icext(X315,uri_rdf_List),inference(resolution,[status(thm)],[c132, c43])).
% 2.76/3.01 cnf(c407,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X314)|iext(X314,uri_rdf_value,uri_rdf_Property),inference(resolution,[status(thm)],[c126, c17])).
% 2.76/3.01 cnf(c402,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X309)|iext(X309,uri_rdf_subject,uri_rdf_Property),inference(resolution,[status(thm)],[c125, c17])).
% 2.76/3.01 cnf(c397,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X304)|iext(X304,uri_rdf_type,uri_rdf_Property),inference(resolution,[status(thm)],[c117, c17])).
% 2.76/3.01 fof(rdfs_annotation_comment_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_comment,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_comment_domain)).
% 2.76/3.01 cnf(c116,plain,iext(uri_rdfs_domain,uri_rdfs_comment,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_comment_domain])).
% 2.76/3.01 cnf(c393,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X299)|iext(X299,uri_rdfs_comment,uri_rdfs_Resource),inference(resolution,[status(thm)],[c116, c17])).
% 2.76/3.01 fof(simple_ir,axiom,(![X]:ir(X)),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', simple_ir)).
% 2.76/3.01 fof(c137,plain,(![X41]:ir(X41)),inference(variable_rename,[status(thm)],[simple_ir])).
% 2.76/3.01 cnf(c138,plain,ir(X45),inference(split_conjunct,[status(thm)],[c137])).
% 2.76/3.01 fof(rdfs_ir_def,axiom,(![X]:(ir(X)<=>icext(uri_rdfs_Resource,X))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_ir_def)).
% 2.83/3.01 fof(c52,plain,(![X]:((~ir(X)|icext(uri_rdfs_Resource,X))&(~icext(uri_rdfs_Resource,X)|ir(X)))),inference(fof_nnf,[status(thm)],[rdfs_ir_def])).
% 2.83/3.01 fof(c53,plain,((![X]:(~ir(X)|icext(uri_rdfs_Resource,X)))&(![X]:(~icext(uri_rdfs_Resource,X)|ir(X)))),inference(shift_quantors,[status(thm)],[c52])).
% 2.83/3.01 fof(c55,plain,(![X23]:(![X24]:((~ir(X23)|icext(uri_rdfs_Resource,X23))&(~icext(uri_rdfs_Resource,X24)|ir(X24))))),inference(shift_quantors,[status(thm)],[fof(c54,plain,((![X23]:(~ir(X23)|icext(uri_rdfs_Resource,X23)))&(![X24]:(~icext(uri_rdfs_Resource,X24)|ir(X24)))),inference(variable_rename,[status(thm)],[c53])).])).
% 2.83/3.01 cnf(c56,plain,~ir(X55)|icext(uri_rdfs_Resource,X55),inference(split_conjunct,[status(thm)],[c55])).
% 2.83/3.01 cnf(c145,plain,icext(uri_rdfs_Resource,X56),inference(resolution,[status(thm)],[c56, c138])).
% 2.83/3.01 cnf(c372,plain,iext(uri_rdf_type,X92,uri_rdfs_Resource),inference(resolution,[status(thm)],[c107, c145])).
% 2.83/3.01 cnf(c390,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X294)|iext(X294,X293,uri_rdfs_Resource),inference(resolution,[status(thm)],[c372, c17])).
% 2.83/3.01 cnf(c395,plain,~iext(uri_rdfs_range,uri_rdf_type,X292)|icext(X292,uri_rdf_Property),inference(resolution,[status(thm)],[c117, c43])).
% 2.83/3.01 cnf(c392,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X291)|icext(X291,uri_rdfs_comment),inference(resolution,[status(thm)],[c116, c69])).
% 2.83/3.01 cnf(c362,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X289)|iext(X289,uri_rdfs_comment,uri_rdfs_Literal),inference(resolution,[status(thm)],[c115, c17])).
% 2.83/3.01 cnf(c388,plain,~iext(uri_rdfs_range,uri_rdf_type,X288)|icext(X288,uri_rdfs_Resource),inference(resolution,[status(thm)],[c372, c43])).
% 2.83/3.01 fof(rdfs_annotation_isdefinedby_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_isdefinedby_domain)).
% 2.83/3.01 cnf(c114,plain,iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_domain])).
% 2.83/3.01 cnf(c359,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X287)|iext(X287,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(resolution,[status(thm)],[c114, c17])).
% 2.83/3.01 fof(rdfs_annotation_isdefinedby_range,axiom,iext(uri_rdfs_range,uri_rdfs_isDefinedBy,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_isdefinedby_range)).
% 2.83/3.01 cnf(c113,plain,iext(uri_rdfs_range,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_range])).
% 2.83/3.01 cnf(c356,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X286)|iext(X286,uri_rdfs_isDefinedBy,uri_rdfs_Resource),inference(resolution,[status(thm)],[c113, c17])).
% 2.83/3.01 cnf(c341,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X285)|iext(X285,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c112, c17])).
% 2.83/3.01 cnf(c358,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X282)|icext(X282,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c114, c69])).
% 2.83/3.01 cnf(c340,plain,~iext(uri_rdfs_subPropertyOf,X281,uri_rdfs_isDefinedBy)|iext(uri_rdfs_subPropertyOf,X281,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c112, c6])).
% 2.83/3.01 cnf(c355,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X279)|icext(X279,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c113, c69])).
% 2.83/3.01 fof(rdfs_annotation_label_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_label,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_label_domain)).
% 2.83/3.01 cnf(c111,plain,iext(uri_rdfs_domain,uri_rdfs_label,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_label_domain])).
% 2.83/3.01 cnf(c335,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X277)|iext(X277,uri_rdfs_label,uri_rdfs_Resource),inference(resolution,[status(thm)],[c111, c17])).
% 2.83/3.01 cnf(c338,plain,~iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X276)|icext(X276,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c112, c69])).
% 2.83/3.01 cnf(c337,plain,~iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X275)|icext(X275,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c112, c43])).
% 2.83/3.01 cnf(c334,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X274)|icext(X274,uri_rdfs_label),inference(resolution,[status(thm)],[c111, c69])).
% 2.83/3.01 cnf(c332,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X272)|iext(X272,uri_rdfs_label,uri_rdfs_Literal),inference(resolution,[status(thm)],[c110, c17])).
% 2.83/3.01 fof(rdfs_annotation_seealso_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_seeAlso,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_seealso_domain)).
% 2.83/3.01 cnf(c109,plain,iext(uri_rdfs_domain,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_seealso_domain])).
% 2.83/3.01 cnf(c329,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X271)|iext(X271,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(resolution,[status(thm)],[c109, c17])).
% 2.83/3.01 fof(rdfs_annotation_seealso_range,axiom,iext(uri_rdfs_range,uri_rdfs_seeAlso,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_annotation_seealso_range)).
% 2.83/3.01 cnf(c108,plain,iext(uri_rdfs_range,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_annotation_seealso_range])).
% 2.83/3.01 cnf(c326,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X269)|iext(X269,uri_rdfs_seeAlso,uri_rdfs_Resource),inference(resolution,[status(thm)],[c108, c17])).
% 2.83/3.01 cnf(c330,plain,~iext(uri_rdfs_range,uri_rdfs_range,X268)|icext(X268,uri_rdfs_Literal),inference(resolution,[status(thm)],[c110, c43])).
% 2.83/3.01 cnf(c328,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X267)|icext(X267,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c109, c69])).
% 2.83/3.01 fof(rdfs_collection_first_domain,axiom,iext(uri_rdfs_domain,uri_rdf_first,uri_rdf_List),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_collection_first_domain)).
% 2.83/3.01 cnf(c98,plain,iext(uri_rdfs_domain,uri_rdf_first,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdfs_collection_first_domain])).
% 2.83/3.01 cnf(c323,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X266)|iext(X266,uri_rdf_first,uri_rdf_List),inference(resolution,[status(thm)],[c98, c17])).
% 2.83/3.01 cnf(c325,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X264)|icext(X264,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c108, c69])).
% 2.83/3.01 fof(rdfs_collection_first_range,axiom,iext(uri_rdfs_range,uri_rdf_first,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_collection_first_range)).
% 2.83/3.01 cnf(c97,plain,iext(uri_rdfs_range,uri_rdf_first,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_collection_first_range])).
% 2.83/3.01 cnf(c320,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X262)|iext(X262,uri_rdf_first,uri_rdfs_Resource),inference(resolution,[status(thm)],[c97, c17])).
% 2.83/3.01 cnf(c322,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X261)|icext(X261,uri_rdf_first),inference(resolution,[status(thm)],[c98, c69])).
% 2.83/3.01 fof(rdfs_collection_rest_domain,axiom,iext(uri_rdfs_domain,uri_rdf_rest,uri_rdf_List),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_collection_rest_domain)).
% 2.83/3.01 cnf(c96,plain,iext(uri_rdfs_domain,uri_rdf_rest,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdfs_collection_rest_domain])).
% 2.83/3.01 cnf(c317,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X259)|iext(X259,uri_rdf_rest,uri_rdf_List),inference(resolution,[status(thm)],[c96, c17])).
% 2.83/3.01 cnf(c319,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X258)|icext(X258,uri_rdf_first),inference(resolution,[status(thm)],[c97, c69])).
% 2.83/3.01 cnf(c316,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X254)|icext(X254,uri_rdf_rest),inference(resolution,[status(thm)],[c96, c69])).
% 2.83/3.01 cnf(c315,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X253)|icext(X253,uri_rdf_List),inference(resolution,[status(thm)],[c96, c43])).
% 2.83/3.01 cnf(c314,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X252)|iext(X252,uri_rdf_rest,uri_rdf_List),inference(resolution,[status(thm)],[c95, c17])).
% 2.83/3.01 cnf(c313,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X251)|icext(X251,uri_rdf_rest),inference(resolution,[status(thm)],[c95, c69])).
% 2.83/3.01 fof(rdfs_reification_predicate_range,axiom,iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_reification_predicate_range)).
% 2.83/3.01 cnf(c36,plain,iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_reification_predicate_range])).
% 2.83/3.01 cnf(c305,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X249)|icext(X249,uri_rdf_predicate),inference(resolution,[status(thm)],[c69, c36])).
% 2.83/3.01 cnf(c303,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X247)|icext(X247,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c69, c89])).
% 2.83/3.01 fof(rdfs_container_n_domain_003,axiom,iext(uri_rdfs_domain,uri_rdf__3,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_domain_003)).
% 2.83/3.01 cnf(c84,plain,iext(uri_rdfs_domain,uri_rdf__3,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_003])).
% 2.83/3.01 cnf(c302,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X246)|icext(X246,uri_rdf__3),inference(resolution,[status(thm)],[c69, c84])).
% 2.83/3.01 fof(rdfs_subclassof_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdfs_Class),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_subclassof_domain)).
% 2.83/3.01 cnf(c33,plain,iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_subclassof_domain])).
% 2.83/3.01 cnf(c301,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X245)|icext(X245,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c69, c33])).
% 2.83/3.01 fof(rdfs_reification_subject_range,axiom,iext(uri_rdfs_range,uri_rdf_subject,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_reification_subject_range)).
% 2.83/3.01 cnf(c34,plain,iext(uri_rdfs_range,uri_rdf_subject,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_reification_subject_range])).
% 2.83/3.01 cnf(c300,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X244)|icext(X244,uri_rdf_subject),inference(resolution,[status(thm)],[c69, c34])).
% 2.83/3.01 fof(rdfs_container_member_range,axiom,iext(uri_rdfs_range,uri_rdfs_member,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_member_range)).
% 2.83/3.01 cnf(c87,plain,iext(uri_rdfs_range,uri_rdfs_member,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_member_range])).
% 2.83/3.01 cnf(c299,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X243)|icext(X243,uri_rdfs_member),inference(resolution,[status(thm)],[c69, c87])).
% 2.83/3.01 fof(rdfs_container_n_domain_002,axiom,iext(uri_rdfs_domain,uri_rdf__2,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_domain_002)).
% 2.83/3.01 cnf(c85,plain,iext(uri_rdfs_domain,uri_rdf__2,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_002])).
% 2.83/3.01 cnf(c298,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X242)|icext(X242,uri_rdf__2),inference(resolution,[status(thm)],[c69, c85])).
% 2.83/3.01 fof(rdfs_subpropertyof_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdf_Property),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_subpropertyof_domain)).
% 2.83/3.01 cnf(c18,plain,iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_subpropertyof_domain])).
% 2.83/3.01 cnf(c297,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X241)|icext(X241,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c69, c18])).
% 2.83/3.01 fof(rdfs_container_member_domain,axiom,iext(uri_rdfs_domain,uri_rdfs_member,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_member_domain)).
% 2.83/3.01 cnf(c88,plain,iext(uri_rdfs_domain,uri_rdfs_member,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_member_domain])).
% 2.83/3.01 cnf(c296,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X240)|icext(X240,uri_rdfs_member),inference(resolution,[status(thm)],[c69, c88])).
% 2.83/3.01 fof(rdfs_value_range,axiom,iext(uri_rdfs_range,uri_rdf_value,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_value_range)).
% 2.83/3.01 cnf(c0,plain,iext(uri_rdfs_range,uri_rdf_value,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_value_range])).
% 2.83/3.01 cnf(c295,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X239)|icext(X239,uri_rdf_value),inference(resolution,[status(thm)],[c69, c0])).
% 2.83/3.01 fof(rdfs_subclassof_range,axiom,iext(uri_rdfs_range,uri_rdfs_subClassOf,uri_rdfs_Class),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_subclassof_range)).
% 2.83/3.01 cnf(c25,plain,iext(uri_rdfs_range,uri_rdfs_subClassOf,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_subclassof_range])).
% 2.83/3.01 cnf(c293,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X237)|icext(X237,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c69, c25])).
% 2.83/3.01 cnf(c292,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X236)|icext(X236,uri_rdfs_range),inference(resolution,[status(thm)],[c69, c44])).
% 2.83/3.01 fof(rdfs_container_n_range_003,axiom,iext(uri_rdfs_range,uri_rdf__3,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_range_003)).
% 2.83/3.01 cnf(c81,plain,iext(uri_rdfs_range,uri_rdf__3,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_range_003])).
% 2.83/3.01 cnf(c291,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X235)|icext(X235,uri_rdf__3),inference(resolution,[status(thm)],[c69, c81])).
% 2.83/3.01 fof(rdfs_subpropertyof_range,axiom,iext(uri_rdfs_range,uri_rdfs_subPropertyOf,uri_rdf_Property),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_subpropertyof_range)).
% 2.83/3.01 cnf(c10,plain,iext(uri_rdfs_range,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(split_conjunct,[status(thm)],[rdfs_subpropertyof_range])).
% 2.83/3.01 cnf(c290,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X234)|icext(X234,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c69, c10])).
% 2.83/3.01 fof(rdfs_container_n_range_001,axiom,iext(uri_rdfs_range,uri_rdf__1,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_range_001)).
% 2.83/3.01 cnf(c83,plain,iext(uri_rdfs_range,uri_rdf__1,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_range_001])).
% 2.83/3.01 cnf(c289,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X233)|icext(X233,uri_rdf__1),inference(resolution,[status(thm)],[c69, c83])).
% 2.83/3.01 fof(rdfs_type_domain,axiom,iext(uri_rdfs_domain,uri_rdf_type,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_type_domain)).
% 2.83/3.01 cnf(c3,plain,iext(uri_rdfs_domain,uri_rdf_type,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_type_domain])).
% 2.83/3.01 cnf(c288,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X232)|icext(X232,uri_rdf_type),inference(resolution,[status(thm)],[c69, c3])).
% 2.83/3.01 cnf(c287,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X231)|icext(X231,uri_rdfs_range),inference(resolution,[status(thm)],[c69, c40])).
% 2.83/3.01 fof(rdfs_type_range,axiom,iext(uri_rdfs_range,uri_rdf_type,uri_rdfs_Class),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_type_range)).
% 2.83/3.01 cnf(c2,plain,iext(uri_rdfs_range,uri_rdf_type,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_type_range])).
% 2.83/3.01 cnf(c286,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X230)|icext(X230,uri_rdf_type),inference(resolution,[status(thm)],[c69, c2])).
% 2.83/3.01 fof(rdfs_reification_object_domain,axiom,iext(uri_rdfs_domain,uri_rdf_object,uri_rdfs_Statement),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_reification_object_domain)).
% 2.83/3.01 cnf(c39,plain,iext(uri_rdfs_domain,uri_rdf_object,uri_rdfs_Statement),inference(split_conjunct,[status(thm)],[rdfs_reification_object_domain])).
% 2.83/3.01 cnf(c285,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X229)|icext(X229,uri_rdf_object),inference(resolution,[status(thm)],[c69, c39])).
% 2.83/3.01 cnf(c284,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X228)|icext(X228,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c69, c76])).
% 2.83/3.01 cnf(c283,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X227)|icext(X227,uri_rdf_Alt),inference(resolution,[status(thm)],[c69, c94])).
% 2.83/3.01 cnf(c281,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X225)|icext(X225,uri_rdfs_Seq),inference(resolution,[status(thm)],[c69, c77])).
% 2.83/3.01 fof(rdfs_value_domain,axiom,iext(uri_rdfs_domain,uri_rdf_value,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_value_domain)).
% 2.83/3.01 cnf(c1,plain,iext(uri_rdfs_domain,uri_rdf_value,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_value_domain])).
% 2.83/3.01 cnf(c280,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X224)|icext(X224,uri_rdf_value),inference(resolution,[status(thm)],[c69, c1])).
% 2.83/3.01 cnf(c277,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X221)|icext(X221,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c69, c71])).
% 2.83/3.01 cnf(c276,plain,~iext(uri_rdfs_domain,uri_rdfs_subClassOf,X220)|icext(X220,uri_rdf_Bag),inference(resolution,[status(thm)],[c69, c93])).
% 2.83/3.01 fof(rdfs_container_n_range_002,axiom,iext(uri_rdfs_range,uri_rdf__2,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_range_002)).
% 2.83/3.01 cnf(c82,plain,iext(uri_rdfs_range,uri_rdf__2,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_range_002])).
% 2.83/3.01 cnf(c274,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X218)|icext(X218,uri_rdf__2),inference(resolution,[status(thm)],[c69, c82])).
% 2.83/3.01 fof(rdfs_container_n_domain_001,axiom,iext(uri_rdfs_domain,uri_rdf__1,uri_rdfs_Resource),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_container_n_domain_001)).
% 2.83/3.01 cnf(c86,plain,iext(uri_rdfs_domain,uri_rdf__1,uri_rdfs_Resource),inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_001])).
% 2.83/3.02 cnf(c272,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X216)|icext(X216,uri_rdf__1),inference(resolution,[status(thm)],[c69, c86])).
% 2.83/3.02 cnf(c271,plain,~iext(uri_rdfs_domain,uri_rdfs_range,X215)|icext(X215,uri_rdfs_domain),inference(resolution,[status(thm)],[c69, c64])).
% 2.83/3.02 cnf(c270,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X214)|icext(X214,uri_rdf_subject),inference(resolution,[status(thm)],[c69, c35])).
% 2.83/3.02 cnf(c269,plain,~iext(uri_rdfs_domain,uri_rdfs_domain,X213)|icext(X213,uri_rdfs_domain),inference(factor,[status(thm)],[c69])).
% 2.83/3.02 cnf(c264,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X210)|icext(X210,uri_rdf_Property),inference(resolution,[status(thm)],[c43, c89])).
% 2.83/3.02 cnf(c262,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X208)|icext(X208,uri_rdfs_Class),inference(resolution,[status(thm)],[c43, c33])).
% 2.83/3.02 cnf(c389,plain,~iext(uri_rdfs_domain,uri_rdf_type,X203)|icext(X203,X204),inference(resolution,[status(thm)],[c372, c69])).
% 2.83/3.02 fof(rdfs_property_type,axiom,iext(uri_rdf_type,uri_rdf_Property,uri_rdfs_Class),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_property_type)).
% 2.83/3.02 cnf(c45,plain,iext(uri_rdf_type,uri_rdf_Property,uri_rdfs_Class),inference(split_conjunct,[status(thm)],[rdfs_property_type])).
% 2.83/3.02 cnf(c255,plain,~iext(uri_rdfs_range,uri_rdf_type,X175)|icext(X175,uri_rdfs_Class),inference(resolution,[status(thm)],[c43, c45])).
% 2.83/3.02 cnf(c251,plain,~iext(uri_rdfs_range,uri_rdfs_range,X171)|icext(X171,uri_rdf_Property),inference(resolution,[status(thm)],[c43, c10])).
% 2.83/3.02 cnf(c245,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X165)|icext(X165,uri_rdfs_Literal),inference(resolution,[status(thm)],[c43, c76])).
% 2.83/3.02 cnf(c996,plain,icext(uri_rdf_Property,uri_rdfs_member),inference(resolution,[status(thm)],[c728, c106])).
% 2.83/3.02 fof(rdfs_dat_xmlliteral_type,axiom,iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Datatype),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_dat_xmlliteral_type)).
% 2.83/3.02 cnf(c75,plain,iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Datatype),inference(split_conjunct,[status(thm)],[rdfs_dat_xmlliteral_type])).
% 2.83/3.02 cnf(c240,plain,~iext(uri_rdfs_range,uri_rdf_type,X160)|icext(X160,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c43, c75])).
% 2.83/3.02 cnf(c239,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X159)|icext(X159,uri_rdf_Property),inference(resolution,[status(thm)],[c43, c70])).
% 2.83/3.02 cnf(c238,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X158)|icext(X158,uri_rdfs_Class),inference(resolution,[status(thm)],[c43, c71])).
% 2.83/3.02 cnf(c964,plain,icext(uri_rdf_Property,uri_rdfs_subPropertyOf),inference(resolution,[status(thm)],[c539, c106])).
% 2.83/3.02 cnf(c237,plain,~iext(uri_rdfs_range,uri_rdfs_subClassOf,X157)|icext(X157,uri_rdfs_Container),inference(resolution,[status(thm)],[c43, c93])).
% 2.83/3.02 cnf(c236,plain,~iext(uri_rdfs_range,uri_rdf_type,X156)|icext(X156,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c43, c79])).
% 2.83/3.02 cnf(c942,plain,icext(uri_rdf_Property,uri_rdfs_subClassOf),inference(resolution,[status(thm)],[c537, c106])).
% 2.83/3.02 cnf(c235,plain,~iext(uri_rdfs_range,uri_rdfs_range,X155)|icext(X155,uri_rdfs_Resource),inference(resolution,[status(thm)],[c43, c82])).
% 2.83/3.02 cnf(c916,plain,icext(uri_rdf_Property,uri_rdfs_range),inference(resolution,[status(thm)],[c535, c106])).
% 2.83/3.02 cnf(c233,plain,~iext(uri_rdfs_range,uri_rdfs_domain,X153)|icext(X153,uri_rdfs_Resource),inference(resolution,[status(thm)],[c43, c86])).
% 2.83/3.02 cnf(c232,plain,~iext(uri_rdfs_range,uri_rdfs_range,X152)|icext(X152,uri_rdfs_Class),inference(resolution,[status(thm)],[c43, c64])).
% 2.83/3.02 cnf(c881,plain,icext(uri_rdf_Property,uri_rdfs_domain),inference(resolution,[status(thm)],[c533, c106])).
% 2.83/3.02 cnf(c230,plain,~iext(uri_rdfs_range,uri_rdfs_range,X150)|icext(X150,X150),inference(factor,[status(thm)],[c43])).
% 2.83/3.02 cnf(c32,plain,~iext(uri_rdfs_subClassOf,X76,X74)|~icext(X76,X75)|icext(X74,X75),inference(split_conjunct,[status(thm)],[c29])).
% 2.83/3.02 cnf(c223,plain,~icext(uri_rdfs_ContainerMembershipProperty,X149)|icext(uri_rdf_Property,X149),inference(resolution,[status(thm)],[c32, c89])).
% 2.83/3.02 cnf(c222,plain,~icext(uri_rdf_XMLLiteral,X148)|icext(uri_rdfs_Literal,X148),inference(resolution,[status(thm)],[c32, c76])).
% 2.83/3.02 cnf(c221,plain,~icext(uri_rdf_Alt,X147)|icext(uri_rdfs_Container,X147),inference(resolution,[status(thm)],[c32, c94])).
% 2.83/3.02 cnf(c220,plain,~icext(uri_rdfs_Seq,X146)|icext(uri_rdfs_Container,X146),inference(resolution,[status(thm)],[c32, c77])).
% 2.83/3.02 cnf(c219,plain,~icext(uri_rdfs_Datatype,X145)|icext(uri_rdfs_Class,X145),inference(resolution,[status(thm)],[c32, c71])).
% 2.83/3.02 cnf(c218,plain,~icext(uri_rdf_Bag,X144)|icext(uri_rdfs_Container,X144),inference(resolution,[status(thm)],[c32, c93])).
% 2.83/3.02 cnf(c189,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X143)|iext(X143,uri_rdf_Alt,uri_rdfs_Container),inference(resolution,[status(thm)],[c94, c17])).
% 2.83/3.02 cnf(c834,plain,icext(uri_rdf_Property,uri_rdfs_seeAlso),inference(resolution,[status(thm)],[c425, c106])).
% 2.83/3.02 cnf(c826,plain,icext(uri_rdf_Property,uri_rdfs_isDefinedBy),inference(resolution,[status(thm)],[c424, c106])).
% 2.83/3.02 cnf(c188,plain,~iext(uri_rdfs_subClassOf,X142,uri_rdf_Alt)|iext(uri_rdfs_subClassOf,X142,uri_rdfs_Container),inference(resolution,[status(thm)],[c94, c21])).
% 2.83/3.02 cnf(c187,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X141)|iext(X141,uri_rdf_Bag,uri_rdfs_Container),inference(resolution,[status(thm)],[c93, c17])).
% 2.83/3.02 cnf(c186,plain,~iext(uri_rdfs_subClassOf,X140,uri_rdf_Bag)|iext(uri_rdfs_subClassOf,X140,uri_rdfs_Container),inference(resolution,[status(thm)],[c93, c21])).
% 2.83/3.02 cnf(c185,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X139)|iext(X139,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),inference(resolution,[status(thm)],[c89, c17])).
% 2.83/3.02 cnf(c184,plain,~iext(uri_rdfs_subClassOf,X138,uri_rdfs_ContainerMembershipProperty)|iext(uri_rdfs_subClassOf,X138,uri_rdf_Property),inference(resolution,[status(thm)],[c89, c21])).
% 2.83/3.02 cnf(c183,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X137)|iext(X137,uri_rdfs_member,uri_rdfs_Resource),inference(resolution,[status(thm)],[c88, c17])).
% 2.83/3.02 cnf(c182,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X136)|iext(X136,uri_rdfs_member,uri_rdfs_Resource),inference(resolution,[status(thm)],[c87, c17])).
% 2.83/3.02 cnf(c181,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X135)|iext(X135,uri_rdf__1,uri_rdfs_Resource),inference(resolution,[status(thm)],[c86, c17])).
% 2.83/3.02 cnf(c180,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X134)|iext(X134,uri_rdf__2,uri_rdfs_Resource),inference(resolution,[status(thm)],[c85, c17])).
% 2.83/3.02 cnf(c179,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X133)|iext(X133,uri_rdf__3,uri_rdfs_Resource),inference(resolution,[status(thm)],[c84, c17])).
% 2.83/3.02 cnf(c178,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X132)|iext(X132,uri_rdf__1,uri_rdfs_Resource),inference(resolution,[status(thm)],[c83, c17])).
% 2.83/3.02 cnf(c177,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X131)|iext(X131,uri_rdf__2,uri_rdfs_Resource),inference(resolution,[status(thm)],[c82, c17])).
% 2.83/3.02 cnf(c176,plain,~iext(uri_rdfs_subClassOf,X130,uri_rdf_XMLLiteral)|iext(uri_rdfs_subClassOf,X130,uri_rdfs_Literal),inference(resolution,[status(thm)],[c21, c76])).
% 2.83/3.02 cnf(c175,plain,~iext(uri_rdfs_subClassOf,X129,uri_rdfs_Seq)|iext(uri_rdfs_subClassOf,X129,uri_rdfs_Container),inference(resolution,[status(thm)],[c21, c77])).
% 2.83/3.02 cnf(c174,plain,~iext(uri_rdfs_subClassOf,X128,uri_rdfs_Datatype)|iext(uri_rdfs_subClassOf,X128,uri_rdfs_Class),inference(resolution,[status(thm)],[c21, c71])).
% 2.83/3.02 cnf(c172,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X126)|iext(X126,uri_rdf__3,uri_rdfs_Resource),inference(resolution,[status(thm)],[c81, c17])).
% 2.83/3.02 cnf(c171,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X125)|iext(X125,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c80, c17])).
% 2.83/3.02 cnf(c170,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X124)|iext(X124,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c79, c17])).
% 2.83/3.02 cnf(c169,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X123)|iext(X123,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),inference(resolution,[status(thm)],[c78, c17])).
% 2.83/3.02 cnf(c168,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X122)|iext(X122,uri_rdfs_Seq,uri_rdfs_Container),inference(resolution,[status(thm)],[c77, c17])).
% 2.83/3.02 cnf(c167,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X121)|iext(X121,uri_rdf_predicate,uri_rdfs_Resource),inference(resolution,[status(thm)],[c17, c36])).
% 2.83/3.02 cnf(c166,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X120)|iext(X120,uri_rdfs_subClassOf,uri_rdfs_Class),inference(resolution,[status(thm)],[c17, c33])).
% 2.83/3.02 cnf(c165,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X119)|iext(X119,uri_rdf_subject,uri_rdfs_Resource),inference(resolution,[status(thm)],[c17, c34])).
% 2.83/3.02 cnf(c164,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X118)|iext(X118,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c17, c18])).
% 2.83/3.02 cnf(c163,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X117)|iext(X117,uri_rdf_value,uri_rdfs_Resource),inference(resolution,[status(thm)],[c17, c0])).
% 2.83/3.02 cnf(c162,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X116)|iext(X116,uri_rdf_Property,uri_rdfs_Class),inference(resolution,[status(thm)],[c17, c45])).
% 2.83/3.02 cnf(c161,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X115)|iext(X115,uri_rdfs_subClassOf,uri_rdfs_Class),inference(resolution,[status(thm)],[c17, c25])).
% 2.83/3.02 cnf(c160,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X114)|iext(X114,uri_rdfs_range,uri_rdf_Property),inference(resolution,[status(thm)],[c17, c44])).
% 2.83/3.02 cnf(c159,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X113)|iext(X113,uri_rdfs_subPropertyOf,uri_rdf_Property),inference(resolution,[status(thm)],[c17, c10])).
% 2.83/3.02 cnf(c158,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X112)|iext(X112,uri_rdf_type,uri_rdfs_Resource),inference(resolution,[status(thm)],[c17, c3])).
% 2.83/3.02 cnf(c157,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X111)|iext(X111,uri_rdfs_range,uri_rdfs_Class),inference(resolution,[status(thm)],[c17, c40])).
% 2.83/3.02 cnf(c156,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X110)|iext(X110,uri_rdf_type,uri_rdfs_Class),inference(resolution,[status(thm)],[c17, c2])).
% 2.83/3.02 cnf(c155,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X109)|iext(X109,uri_rdf_object,uri_rdfs_Statement),inference(resolution,[status(thm)],[c17, c39])).
% 2.83/3.02 cnf(c154,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X108)|iext(X108,uri_rdf_XMLLiteral,uri_rdfs_Literal),inference(resolution,[status(thm)],[c17, c76])).
% 2.83/3.02 cnf(c153,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X107)|iext(X107,uri_rdf_value,uri_rdfs_Resource),inference(resolution,[status(thm)],[c17, c1])).
% 2.83/3.02 cnf(c152,plain,~iext(uri_rdfs_subPropertyOf,uri_rdf_type,X106)|iext(X106,uri_rdf_XMLLiteral,uri_rdfs_Datatype),inference(resolution,[status(thm)],[c17, c75])).
% 2.83/3.02 cnf(c151,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X105)|iext(X105,uri_rdfs_domain,uri_rdf_Property),inference(resolution,[status(thm)],[c17, c70])).
% 2.83/3.02 cnf(c150,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X104)|iext(X104,uri_rdfs_Datatype,uri_rdfs_Class),inference(resolution,[status(thm)],[c17, c71])).
% 2.83/3.02 cnf(c149,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X103)|iext(X103,uri_rdf_predicate,uri_rdfs_Statement),inference(resolution,[status(thm)],[c17, c37])).
% 2.83/3.02 cnf(c148,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X102)|iext(X102,uri_rdfs_domain,uri_rdfs_Class),inference(resolution,[status(thm)],[c17, c64])).
% 2.83/3.02 cnf(c147,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X101)|iext(X101,uri_rdf_subject,uri_rdfs_Statement),inference(resolution,[status(thm)],[c17, c35])).
% 2.83/3.02 cnf(c146,plain,~iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X100)|iext(X100,uri_rdfs_subPropertyOf,X100),inference(factor,[status(thm)],[c17])).
% 2.83/3.02 cnf(c465,plain,icext(uri_rdf_Property,uri_rdf_first),inference(resolution,[status(thm)],[c133, c106])).
% 2.83/3.02 cnf(c459,plain,icext(uri_rdf_List,uri_rdf_nil),inference(resolution,[status(thm)],[c132, c106])).
% 2.83/3.02 cnf(c452,plain,icext(uri_rdf_Property,uri_rdf_rest),inference(resolution,[status(thm)],[c131, c106])).
% 2.83/3.02 cnf(c443,plain,icext(uri_rdf_Property,uri_rdf__1),inference(resolution,[status(thm)],[c130, c106])).
% 2.83/3.02 cnf(c436,plain,icext(uri_rdf_Property,uri_rdf__2),inference(resolution,[status(thm)],[c129, c106])).
% 2.83/3.02 cnf(c428,plain,icext(uri_rdf_Property,uri_rdf__3),inference(resolution,[status(thm)],[c128, c106])).
% 2.83/3.02 cnf(c409,plain,icext(uri_rdf_Property,uri_rdf_object),inference(resolution,[status(thm)],[c127, c106])).
% 2.83/3.02 cnf(c404,plain,icext(uri_rdf_Property,uri_rdf_value),inference(resolution,[status(thm)],[c126, c106])).
% 2.83/3.02 cnf(c399,plain,icext(uri_rdf_Property,uri_rdf_subject),inference(resolution,[status(thm)],[c125, c106])).
% 2.83/3.02 cnf(c394,plain,icext(uri_rdf_Property,uri_rdf_type),inference(resolution,[status(thm)],[c117, c106])).
% 2.83/3.02 cnf(c364,plain,icext(uri_rdfs_Datatype,uri_rdf_XMLLiteral),inference(resolution,[status(thm)],[c106, c75])).
% 2.83/3.02 cnf(c227,plain,icext(uri_rdfs_Class,uri_rdf_Property),inference(resolution,[status(thm)],[c211, c62])).
% 2.83/3.02 fof(rdfs_datatype_instsub_literal,axiom,(![D]:(icext(uri_rdfs_Datatype,D)=>iext(uri_rdfs_subClassOf,D,uri_rdfs_Literal))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_datatype_instsub_literal)).
% 2.83/3.02 fof(c72,plain,(![D]:(~icext(uri_rdfs_Datatype,D)|iext(uri_rdfs_subClassOf,D,uri_rdfs_Literal))),inference(fof_nnf,[status(thm)],[rdfs_datatype_instsub_literal])).
% 2.83/3.02 fof(c73,plain,(![X31]:(~icext(uri_rdfs_Datatype,X31)|iext(uri_rdfs_subClassOf,X31,uri_rdfs_Literal))),inference(variable_rename,[status(thm)],[c72])).
% 2.83/3.02 cnf(c74,plain,~icext(uri_rdfs_Datatype,X85)|iext(uri_rdfs_subClassOf,X85,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[c73])).
% 2.83/3.02 fof(rdfs_lv_def,axiom,(![X]:(lv(X)<=>icext(uri_rdfs_Literal,X))),file('/export/starexec/sandbox/benchmark/Axioms/SWB003+0.ax', rdfs_lv_def)).
% 2.83/3.02 fof(c46,plain,(![X]:((~lv(X)|icext(uri_rdfs_Literal,X))&(~icext(uri_rdfs_Literal,X)|lv(X)))),inference(fof_nnf,[status(thm)],[rdfs_lv_def])).
% 2.83/3.02 fof(c47,plain,((![X]:(~lv(X)|icext(uri_rdfs_Literal,X)))&(![X]:(~icext(uri_rdfs_Literal,X)|lv(X)))),inference(shift_quantors,[status(thm)],[c46])).
% 2.83/3.02 fof(c49,plain,(![X21]:(![X22]:((~lv(X21)|icext(uri_rdfs_Literal,X21))&(~icext(uri_rdfs_Literal,X22)|lv(X22))))),inference(shift_quantors,[status(thm)],[fof(c48,plain,((![X21]:(~lv(X21)|icext(uri_rdfs_Literal,X21)))&(![X22]:(~icext(uri_rdfs_Literal,X22)|lv(X22)))),inference(variable_rename,[status(thm)],[c47])).])).
% 2.83/3.02 cnf(c51,plain,~icext(uri_rdfs_Literal,X52)|lv(X52),inference(split_conjunct,[status(thm)],[c49])).
% 2.83/3.02 cnf(c50,plain,~lv(X51)|icext(uri_rdfs_Literal,X51),inference(split_conjunct,[status(thm)],[c49])).
% 2.83/3.02 % SZS output end Saturation
% 2.83/3.02
% 2.83/3.02 % Initial clauses : 89
% 2.83/3.02 % Processed clauses : 502
% 2.83/3.02 % Factors computed : 5
% 2.83/3.02 % Resolvents computed: 1180
% 2.83/3.02 % Tautologies deleted: 47
% 2.83/3.02 % Forward subsumed : 725
% 2.83/3.02 % Backward subsumed : 1
% 2.83/3.02 % -------- CPU Time ---------
% 2.83/3.02 % User time : 2.624 s
% 2.83/3.02 % System time : 0.022 s
% 2.83/3.02 % Total time : 2.646 s
%------------------------------------------------------------------------------