%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SWB005+4 : TPTP v8.1.0. Released v5.2.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n021.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 : 600s
% DateTime : Tue Jul 19 19:20:55 EDT 2022
% Result : CounterSatisfiable 0.20s 0.49s
% Output : Saturation 0.20s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named 67)
% Comments :
%------------------------------------------------------------------------------
cnf(491,plain,
( ~ ic(u)
| ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,v)
| iext(v,u,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[210,89]),
[iquote('0:Res:210.1,89.0')] ).
cnf(490,plain,
( ~ lv(u)
| ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,v)
| iext(v,u,uri_rdfs_Literal) ),
inference(res,[status(thm),theory(equality)],[209,89]),
[iquote('0:Res:209.1,89.0')] ).
cnf(310,plain,
( ~ lv(u)
| ~ iext(uri_rdfs_range,uri_rdf_type,v)
| icext(v,uri_rdfs_Literal) ),
inference(res,[status(thm),theory(equality)],[209,87]),
[iquote('0:Res:209.1,87.0')] ).
cnf(489,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,v,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[208,89]),
[iquote('0:Res:208.0,89.0')] ).
cnf(857,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,u)
| iext(u,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[803,89]),
[iquote('0:Res:803.0,89.0')] ).
cnf(848,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,u)
| iext(u,uri_rdf_Alt,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[802,89]),
[iquote('0:Res:802.0,89.0')] ).
cnf(499,plain,
( ~ ip(u)
| ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,v)
| iext(v,u,u) ),
inference(res,[status(thm),theory(equality)],[80,89]),
[iquote('0:Res:80.1,89.0')] ).
cnf(838,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,u)
| iext(u,uri_rdf_Bag,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[801,89]),
[iquote('0:Res:801.0,89.0')] ).
cnf(829,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,u)
| iext(u,uri_rdfs_Seq,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[800,89]),
[iquote('0:Res:800.0,89.0')] ).
cnf(820,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,u)
| iext(u,uri_rdf_XMLLiteral,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[799,89]),
[iquote('0:Res:799.0,89.0')] ).
cnf(811,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,u)
| iext(u,uri_rdfs_Datatype,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[798,89]),
[iquote('0:Res:798.0,89.0')] ).
cnf(474,plain,
( ~ ic(u)
| ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,v)
| iext(v,u,u) ),
inference(res,[status(thm),theory(equality)],[77,89]),
[iquote('0:Res:77.1,89.0')] ).
cnf(708,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdf_Alt,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[706,89]),
[iquote('0:Res:706.0,89.0')] ).
cnf(700,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdf_Bag,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[693,89]),
[iquote('0:Res:693.0,89.0')] ).
cnf(695,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdfs_Seq,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[691,89]),
[iquote('0:Res:691.0,89.0')] ).
cnf(681,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdfs_comment,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[672,89]),
[iquote('0:Res:672.0,89.0')] ).
cnf(487,plain,
( ~ ip(u)
| ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,v)
| iext(v,u,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[73,89]),
[iquote('0:Res:73.1,89.0')] ).
cnf(675,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdfs_isDefinedBy,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[671,89]),
[iquote('0:Res:671.0,89.0')] ).
cnf(665,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdfs_label,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[662,89]),
[iquote('0:Res:662.0,89.0')] ).
cnf(651,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdfs_range,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[648,89]),
[iquote('0:Res:648.0,89.0')] ).
cnf(640,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdfs_domain,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[637,89]),
[iquote('0:Res:637.0,89.0')] ).
cnf(473,plain,
( ~ ic(u)
| ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,v)
| iext(v,u,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[74,89]),
[iquote('0:Res:74.1,89.0')] ).
cnf(630,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdfs_subClassOf,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[627,89]),
[iquote('0:Res:627.0,89.0')] ).
cnf(621,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdfs_subPropertyOf,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[618,89]),
[iquote('0:Res:618.0,89.0')] ).
cnf(610,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdfs_member,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[607,89]),
[iquote('0:Res:607.0,89.0')] ).
cnf(598,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdf_predicate,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[595,89]),
[iquote('0:Res:595.0,89.0')] ).
cnf(387,plain,
( ~ ip(u)
| ~ iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,v)
| icext(v,u) ),
inference(res,[status(thm),theory(equality)],[80,86]),
[iquote('0:Res:80.1,86.0')] ).
cnf(587,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdfs_seeAlso,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[584,89]),
[iquote('0:Res:584.0,89.0')] ).
cnf(574,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[572,89]),
[iquote('0:Res:572.0,89.0')] ).
cnf(566,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdfs_Container,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[563,89]),
[iquote('0:Res:563.0,89.0')] ).
cnf(557,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdfs_Literal,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[555,89]),
[iquote('0:Res:555.0,89.0')] ).
cnf(363,plain,
( ~ ic(u)
| ~ iext(uri_rdfs_domain,uri_rdfs_subClassOf,v)
| icext(v,u) ),
inference(res,[status(thm),theory(equality)],[74,86]),
[iquote('0:Res:74.1,86.0')] ).
cnf(549,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdfs_Datatype,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[537,89]),
[iquote('0:Res:537.0,89.0')] ).
cnf(544,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdf_List,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[534,89]),
[iquote('0:Res:534.0,89.0')] ).
cnf(539,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdfs_Statement,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[532,89]),
[iquote('0:Res:532.0,89.0')] ).
cnf(520,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdfs_Class,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[518,89]),
[iquote('0:Res:518.0,89.0')] ).
cnf(317,plain,
( ~ ip(u)
| ~ iext(uri_rdfs_range,uri_rdfs_subPropertyOf,v)
| icext(v,u) ),
inference(res,[status(thm),theory(equality)],[80,87]),
[iquote('0:Res:80.1,87.0')] ).
cnf(511,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdfs_Resource,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[509,89]),
[iquote('0:Res:509.0,89.0')] ).
cnf(813,plain,
( ~ iext(uri_rdfs_range,uri_rdfs_subClassOf,u)
| icext(u,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[798,87]),
[iquote('0:Res:798.0,87.0')] ).
cnf(803,plain,
iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Resource),
inference(res,[status(thm),theory(equality)],[29,421]),
[iquote('0:Res:29.0,421.0')] ).
cnf(802,plain,
iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Resource),
inference(res,[status(thm),theory(equality)],[27,421]),
[iquote('0:Res:27.0,421.0')] ).
cnf(294,plain,
( ~ ic(u)
| ~ iext(uri_rdfs_range,uri_rdfs_subClassOf,v)
| icext(v,u) ),
inference(res,[status(thm),theory(equality)],[77,87]),
[iquote('0:Res:77.1,87.0')] ).
cnf(801,plain,
iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Resource),
inference(res,[status(thm),theory(equality)],[28,421]),
[iquote('0:Res:28.0,421.0')] ).
cnf(800,plain,
iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Resource),
inference(res,[status(thm),theory(equality)],[41,421]),
[iquote('0:Res:41.0,421.0')] ).
cnf(799,plain,
iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Resource),
inference(res,[status(thm),theory(equality)],[42,421]),
[iquote('0:Res:42.0,421.0')] ).
cnf(798,plain,
iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Resource),
inference(res,[status(thm),theory(equality)],[44,421]),
[iquote('0:Res:44.0,421.0')] ).
cnf(421,plain,
( ~ iext(uri_rdfs_subClassOf,u,v)
| iext(uri_rdfs_subClassOf,u,uri_rdfs_Resource) ),
inference(mrr,[status(thm)],[419,76]),
[iquote('0:MRR:419.0,76.1')] ).
cnf(503,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_ex,u)
| iext(u,uri_ex_s,uri_ex_o) ),
inference(res,[status(thm),theory(equality)],[2,89]),
[iquote('0:Res:2.0,89.0')] ).
cnf(502,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,u)
| iext(u,uri_rdf__1,uri_rdfs_member) ),
inference(res,[status(thm),theory(equality)],[248,89]),
[iquote('0:Res:248.0,89.0')] ).
cnf(501,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,u)
| iext(u,uri_rdf__2,uri_rdfs_member) ),
inference(res,[status(thm),theory(equality)],[238,89]),
[iquote('0:Res:238.0,89.0')] ).
cnf(500,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,u)
| iext(u,uri_rdf__3,uri_rdfs_member) ),
inference(res,[status(thm),theory(equality)],[236,89]),
[iquote('0:Res:236.0,89.0')] ).
cnf(498,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,u)
| iext(u,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso) ),
inference(res,[status(thm),theory(equality)],[18,89]),
[iquote('0:Res:18.0,89.0')] ).
cnf(497,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_range,u)
| iext(u,uri_rdfs_range,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[49,89]),
[iquote('0:Res:49.0,89.0')] ).
cnf(496,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_range,u)
| iext(u,uri_rdfs_isDefinedBy,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[17,89]),
[iquote('0:Res:17.0,89.0')] ).
cnf(495,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_range,u)
| iext(u,uri_rdfs_comment,uri_rdfs_Literal) ),
inference(res,[status(thm),theory(equality)],[15,89]),
[iquote('0:Res:15.0,89.0')] ).
cnf(494,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_range,u)
| iext(u,uri_rdfs_label,uri_rdfs_Literal) ),
inference(res,[status(thm),theory(equality)],[20,89]),
[iquote('0:Res:20.0,89.0')] ).
cnf(493,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_range,u)
| iext(u,uri_rdf_rest,uri_rdf_List) ),
inference(res,[status(thm),theory(equality)],[26,89]),
[iquote('0:Res:26.0,89.0')] ).
cnf(492,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdf_XMLLiteral,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[428,89]),
[iquote('0:Res:428.0,89.0')] ).
cnf(488,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdf_nil,uri_rdf_List) ),
inference(res,[status(thm),theory(equality)],[4,89]),
[iquote('0:Res:4.0,89.0')] ).
cnf(486,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdf_type,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[13,89]),
[iquote('0:Res:13.0,89.0')] ).
cnf(485,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdf_first,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[3,89]),
[iquote('0:Res:3.0,89.0')] ).
cnf(484,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdf_rest,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[5,89]),
[iquote('0:Res:5.0,89.0')] ).
cnf(483,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdf__1,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[6,89]),
[iquote('0:Res:6.0,89.0')] ).
cnf(482,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdf__2,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[7,89]),
[iquote('0:Res:7.0,89.0')] ).
cnf(481,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdf__3,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[8,89]),
[iquote('0:Res:8.0,89.0')] ).
cnf(480,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdf_object,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[9,89]),
[iquote('0:Res:9.0,89.0')] ).
cnf(479,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdf_value,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[10,89]),
[iquote('0:Res:10.0,89.0')] ).
cnf(478,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdf_subject,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[11,89]),
[iquote('0:Res:11.0,89.0')] ).
cnf(477,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdf__1,uri_rdfs_ContainerMembershipProperty) ),
inference(res,[status(thm),theory(equality)],[38,89]),
[iquote('0:Res:38.0,89.0')] ).
cnf(476,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdf__2,uri_rdfs_ContainerMembershipProperty) ),
inference(res,[status(thm),theory(equality)],[39,89]),
[iquote('0:Res:39.0,89.0')] ).
cnf(475,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdf__3,uri_rdfs_ContainerMembershipProperty) ),
inference(res,[status(thm),theory(equality)],[40,89]),
[iquote('0:Res:40.0,89.0')] ).
cnf(472,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,u)
| iext(u,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[29,89]),
[iquote('0:Res:29.0,89.0')] ).
cnf(471,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,u)
| iext(u,uri_rdf_Alt,uri_rdfs_Container) ),
inference(res,[status(thm),theory(equality)],[27,89]),
[iquote('0:Res:27.0,89.0')] ).
cnf(470,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,u)
| iext(u,uri_rdf_Bag,uri_rdfs_Container) ),
inference(res,[status(thm),theory(equality)],[28,89]),
[iquote('0:Res:28.0,89.0')] ).
cnf(469,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,u)
| iext(u,uri_rdfs_Seq,uri_rdfs_Container) ),
inference(res,[status(thm),theory(equality)],[41,89]),
[iquote('0:Res:41.0,89.0')] ).
cnf(468,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,u)
| iext(u,uri_rdf_XMLLiteral,uri_rdfs_Literal) ),
inference(res,[status(thm),theory(equality)],[42,89]),
[iquote('0:Res:42.0,89.0')] ).
cnf(467,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdf_XMLLiteral,uri_rdfs_Datatype) ),
inference(res,[status(thm),theory(equality)],[43,89]),
[iquote('0:Res:43.0,89.0')] ).
cnf(466,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,u)
| iext(u,uri_rdf_first,uri_rdf_List) ),
inference(res,[status(thm),theory(equality)],[23,89]),
[iquote('0:Res:23.0,89.0')] ).
cnf(465,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,u)
| iext(u,uri_rdf_rest,uri_rdf_List) ),
inference(res,[status(thm),theory(equality)],[25,89]),
[iquote('0:Res:25.0,89.0')] ).
cnf(464,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,u)
| iext(u,uri_rdfs_comment,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[14,89]),
[iquote('0:Res:14.0,89.0')] ).
cnf(463,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,u)
| iext(u,uri_rdfs_isDefinedBy,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[16,89]),
[iquote('0:Res:16.0,89.0')] ).
cnf(462,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,u)
| iext(u,uri_rdfs_label,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[19,89]),
[iquote('0:Res:19.0,89.0')] ).
cnf(461,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,u)
| iext(u,uri_rdfs_seeAlso,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[21,89]),
[iquote('0:Res:21.0,89.0')] ).
cnf(460,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,u)
| iext(u,uri_rdfs_member,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[30,89]),
[iquote('0:Res:30.0,89.0')] ).
cnf(459,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,u)
| iext(u,uri_rdf__1,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[32,89]),
[iquote('0:Res:32.0,89.0')] ).
cnf(458,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,u)
| iext(u,uri_rdf__2,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[33,89]),
[iquote('0:Res:33.0,89.0')] ).
cnf(457,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,u)
| iext(u,uri_rdf__3,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[34,89]),
[iquote('0:Res:34.0,89.0')] ).
cnf(456,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,u)
| iext(u,uri_rdfs_domain,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[45,89]),
[iquote('0:Res:45.0,89.0')] ).
cnf(455,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,u)
| iext(u,uri_rdfs_range,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[48,89]),
[iquote('0:Res:48.0,89.0')] ).
cnf(454,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,u)
| iext(u,uri_rdf_object,uri_rdfs_Statement) ),
inference(res,[status(thm),theory(equality)],[50,89]),
[iquote('0:Res:50.0,89.0')] ).
cnf(453,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,u)
| iext(u,uri_rdf_predicate,uri_rdfs_Statement) ),
inference(res,[status(thm),theory(equality)],[52,89]),
[iquote('0:Res:52.0,89.0')] ).
cnf(452,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,u)
| iext(u,uri_rdf_subject,uri_rdfs_Statement) ),
inference(res,[status(thm),theory(equality)],[54,89]),
[iquote('0:Res:54.0,89.0')] ).
cnf(451,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,u)
| iext(u,uri_rdfs_Datatype,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[44,89]),
[iquote('0:Res:44.0,89.0')] ).
cnf(450,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_range,u)
| iext(u,uri_rdfs_domain,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[46,89]),
[iquote('0:Res:46.0,89.0')] ).
cnf(449,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdf_Property,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[47,89]),
[iquote('0:Res:47.0,89.0')] ).
cnf(448,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,u)
| iext(u,uri_rdfs_subClassOf,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[56,89]),
[iquote('0:Res:56.0,89.0')] ).
cnf(447,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_range,u)
| iext(u,uri_rdfs_subClassOf,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[57,89]),
[iquote('0:Res:57.0,89.0')] ).
cnf(446,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,u)
| iext(u,uri_rdfs_subPropertyOf,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[58,89]),
[iquote('0:Res:58.0,89.0')] ).
cnf(445,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_range,u)
| iext(u,uri_rdfs_subPropertyOf,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[59,89]),
[iquote('0:Res:59.0,89.0')] ).
cnf(444,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,u)
| iext(u,uri_rdf_type,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[60,89]),
[iquote('0:Res:60.0,89.0')] ).
cnf(443,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_range,u)
| iext(u,uri_rdf_type,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[61,89]),
[iquote('0:Res:61.0,89.0')] ).
cnf(442,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_range,u)
| iext(u,uri_rdfs_seeAlso,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[22,89]),
[iquote('0:Res:22.0,89.0')] ).
cnf(441,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_range,u)
| iext(u,uri_rdf_first,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[24,89]),
[iquote('0:Res:24.0,89.0')] ).
cnf(440,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_range,u)
| iext(u,uri_rdfs_member,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[31,89]),
[iquote('0:Res:31.0,89.0')] ).
cnf(439,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_range,u)
| iext(u,uri_rdf__1,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[35,89]),
[iquote('0:Res:35.0,89.0')] ).
cnf(438,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_range,u)
| iext(u,uri_rdf__2,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[36,89]),
[iquote('0:Res:36.0,89.0')] ).
cnf(437,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_range,u)
| iext(u,uri_rdf__3,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[37,89]),
[iquote('0:Res:37.0,89.0')] ).
cnf(436,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_range,u)
| iext(u,uri_rdf_predicate,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[53,89]),
[iquote('0:Res:53.0,89.0')] ).
cnf(435,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_range,u)
| iext(u,uri_rdf_subject,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[55,89]),
[iquote('0:Res:55.0,89.0')] ).
cnf(434,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,u)
| iext(u,uri_rdf_value,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[62,89]),
[iquote('0:Res:62.0,89.0')] ).
cnf(433,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_range,u)
| iext(u,uri_rdf_value,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[63,89]),
[iquote('0:Res:63.0,89.0')] ).
cnf(418,plain,
( ~ iext(uri_rdfs_subClassOf,u,uri_rdfs_ContainerMembershipProperty)
| iext(uri_rdfs_subClassOf,u,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[29,88]),
[iquote('0:Res:29.0,88.0')] ).
cnf(417,plain,
( ~ iext(uri_rdfs_subClassOf,u,uri_rdf_Alt)
| iext(uri_rdfs_subClassOf,u,uri_rdfs_Container) ),
inference(res,[status(thm),theory(equality)],[27,88]),
[iquote('0:Res:27.0,88.0')] ).
cnf(416,plain,
( ~ iext(uri_rdfs_subClassOf,u,uri_rdf_Bag)
| iext(uri_rdfs_subClassOf,u,uri_rdfs_Container) ),
inference(res,[status(thm),theory(equality)],[28,88]),
[iquote('0:Res:28.0,88.0')] ).
cnf(415,plain,
( ~ iext(uri_rdfs_subClassOf,u,uri_rdfs_Seq)
| iext(uri_rdfs_subClassOf,u,uri_rdfs_Container) ),
inference(res,[status(thm),theory(equality)],[41,88]),
[iquote('0:Res:41.0,88.0')] ).
cnf(414,plain,
( ~ iext(uri_rdfs_subClassOf,u,uri_rdf_XMLLiteral)
| iext(uri_rdfs_subClassOf,u,uri_rdfs_Literal) ),
inference(res,[status(thm),theory(equality)],[42,88]),
[iquote('0:Res:42.0,88.0')] ).
cnf(413,plain,
( ~ iext(uri_rdfs_subClassOf,u,uri_rdfs_Datatype)
| iext(uri_rdfs_subClassOf,u,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[44,88]),
[iquote('0:Res:44.0,88.0')] ).
cnf(406,plain,
( ~ iext(uri_rdfs_subPropertyOf,u,uri_rdf__1)
| iext(uri_rdfs_subPropertyOf,u,uri_rdfs_member) ),
inference(res,[status(thm),theory(equality)],[248,90]),
[iquote('0:Res:248.0,90.0')] ).
cnf(400,plain,
( ~ iext(uri_rdfs_subPropertyOf,u,uri_rdf__2)
| iext(uri_rdfs_subPropertyOf,u,uri_rdfs_member) ),
inference(res,[status(thm),theory(equality)],[238,90]),
[iquote('0:Res:238.0,90.0')] ).
cnf(399,plain,
( ~ iext(uri_rdfs_subPropertyOf,u,uri_rdf__3)
| iext(uri_rdfs_subPropertyOf,u,uri_rdfs_member) ),
inference(res,[status(thm),theory(equality)],[236,90]),
[iquote('0:Res:236.0,90.0')] ).
cnf(379,plain,
( ~ iext(uri_rdfs_domain,uri_rdf_type,u)
| icext(u,v) ),
inference(res,[status(thm),theory(equality)],[208,86]),
[iquote('0:Res:208.0,86.0')] ).
cnf(397,plain,
( ~ iext(uri_rdfs_subPropertyOf,u,uri_rdfs_isDefinedBy)
| iext(uri_rdfs_subPropertyOf,u,uri_rdfs_seeAlso) ),
inference(res,[status(thm),theory(equality)],[18,90]),
[iquote('0:Res:18.0,90.0')] ).
cnf(409,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,u)
| icext(u,uri_rdf__1) ),
inference(res,[status(thm),theory(equality)],[248,86]),
[iquote('0:Res:248.0,86.0')] ).
cnf(403,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,u)
| icext(u,uri_rdf__2) ),
inference(res,[status(thm),theory(equality)],[238,86]),
[iquote('0:Res:238.0,86.0')] ).
cnf(395,plain,
( ~ iext(uri_rdfs_range,uri_rdfs_subPropertyOf,u)
| icext(u,uri_rdfs_member) ),
inference(res,[status(thm),theory(equality)],[236,87]),
[iquote('0:Res:236.0,87.0')] ).
cnf(394,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,u)
| icext(u,uri_rdf__3) ),
inference(res,[status(thm),theory(equality)],[236,86]),
[iquote('0:Res:236.0,86.0')] ).
cnf(388,plain,
( ~ iext(uri_rdfs_domain,uri_ex,u)
| icext(u,uri_ex_s) ),
inference(res,[status(thm),theory(equality)],[2,86]),
[iquote('0:Res:2.0,86.0')] ).
cnf(386,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,u)
| icext(u,uri_rdfs_isDefinedBy) ),
inference(res,[status(thm),theory(equality)],[18,86]),
[iquote('0:Res:18.0,86.0')] ).
cnf(385,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_range,u)
| icext(u,uri_rdfs_range) ),
inference(res,[status(thm),theory(equality)],[49,86]),
[iquote('0:Res:49.0,86.0')] ).
cnf(384,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_range,u)
| icext(u,uri_rdfs_isDefinedBy) ),
inference(res,[status(thm),theory(equality)],[17,86]),
[iquote('0:Res:17.0,86.0')] ).
cnf(383,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_range,u)
| icext(u,uri_rdfs_comment) ),
inference(res,[status(thm),theory(equality)],[15,86]),
[iquote('0:Res:15.0,86.0')] ).
cnf(382,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_range,u)
| icext(u,uri_rdfs_label) ),
inference(res,[status(thm),theory(equality)],[20,86]),
[iquote('0:Res:20.0,86.0')] ).
cnf(381,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_range,u)
| icext(u,uri_rdf_rest) ),
inference(res,[status(thm),theory(equality)],[26,86]),
[iquote('0:Res:26.0,86.0')] ).
cnf(362,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_subClassOf,u)
| icext(u,uri_rdfs_ContainerMembershipProperty) ),
inference(res,[status(thm),theory(equality)],[29,86]),
[iquote('0:Res:29.0,86.0')] ).
cnf(706,plain,
iext(uri_rdf_type,uri_rdf_Alt,uri_rdfs_Class),
inference(res,[status(thm),theory(equality)],[704,82]),
[iquote('0:Res:704.0,82.0')] ).
cnf(704,plain,
icext(uri_rdfs_Class,uri_rdf_Alt),
inference(res,[status(thm),theory(equality)],[56,361]),
[iquote('0:Res:56.0,361.0')] ).
cnf(361,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_subClassOf,u)
| icext(u,uri_rdf_Alt) ),
inference(res,[status(thm),theory(equality)],[27,86]),
[iquote('0:Res:27.0,86.0')] ).
cnf(693,plain,
iext(uri_rdf_type,uri_rdf_Bag,uri_rdfs_Class),
inference(res,[status(thm),theory(equality)],[689,82]),
[iquote('0:Res:689.0,82.0')] ).
cnf(691,plain,
iext(uri_rdf_type,uri_rdfs_Seq,uri_rdfs_Class),
inference(res,[status(thm),theory(equality)],[688,82]),
[iquote('0:Res:688.0,82.0')] ).
cnf(689,plain,
icext(uri_rdfs_Class,uri_rdf_Bag),
inference(res,[status(thm),theory(equality)],[56,360]),
[iquote('0:Res:56.0,360.0')] ).
cnf(688,plain,
icext(uri_rdfs_Class,uri_rdfs_Seq),
inference(res,[status(thm),theory(equality)],[56,359]),
[iquote('0:Res:56.0,359.0')] ).
cnf(360,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_subClassOf,u)
| icext(u,uri_rdf_Bag) ),
inference(res,[status(thm),theory(equality)],[28,86]),
[iquote('0:Res:28.0,86.0')] ).
cnf(359,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_subClassOf,u)
| icext(u,uri_rdfs_Seq) ),
inference(res,[status(thm),theory(equality)],[41,86]),
[iquote('0:Res:41.0,86.0')] ).
cnf(358,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_subClassOf,u)
| icext(u,uri_rdf_XMLLiteral) ),
inference(res,[status(thm),theory(equality)],[42,86]),
[iquote('0:Res:42.0,86.0')] ).
cnf(356,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_domain,u)
| icext(u,uri_rdf_first) ),
inference(res,[status(thm),theory(equality)],[23,86]),
[iquote('0:Res:23.0,86.0')] ).
cnf(679,plain,
ip(uri_rdfs_comment),
inference(res,[status(thm),theory(equality)],[672,72]),
[iquote('0:Res:672.0,72.0')] ).
cnf(355,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_domain,u)
| icext(u,uri_rdf_rest) ),
inference(res,[status(thm),theory(equality)],[25,86]),
[iquote('0:Res:25.0,86.0')] ).
cnf(672,plain,
iext(uri_rdf_type,uri_rdfs_comment,uri_rdf_Property),
inference(res,[status(thm),theory(equality)],[670,82]),
[iquote('0:Res:670.0,82.0')] ).
cnf(671,plain,
iext(uri_rdf_type,uri_rdfs_isDefinedBy,uri_rdf_Property),
inference(res,[status(thm),theory(equality)],[669,82]),
[iquote('0:Res:669.0,82.0')] ).
cnf(670,plain,
icext(uri_rdf_Property,uri_rdfs_comment),
inference(res,[status(thm),theory(equality)],[45,354]),
[iquote('0:Res:45.0,354.0')] ).
cnf(669,plain,
icext(uri_rdf_Property,uri_rdfs_isDefinedBy),
inference(res,[status(thm),theory(equality)],[45,353]),
[iquote('0:Res:45.0,353.0')] ).
cnf(354,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_domain,u)
| icext(u,uri_rdfs_comment) ),
inference(res,[status(thm),theory(equality)],[14,86]),
[iquote('0:Res:14.0,86.0')] ).
cnf(353,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_domain,u)
| icext(u,uri_rdfs_isDefinedBy) ),
inference(res,[status(thm),theory(equality)],[16,86]),
[iquote('0:Res:16.0,86.0')] ).
cnf(663,plain,
ip(uri_rdfs_label),
inference(res,[status(thm),theory(equality)],[662,72]),
[iquote('0:Res:662.0,72.0')] ).
cnf(662,plain,
iext(uri_rdf_type,uri_rdfs_label,uri_rdf_Property),
inference(res,[status(thm),theory(equality)],[661,82]),
[iquote('0:Res:661.0,82.0')] ).
cnf(661,plain,
icext(uri_rdf_Property,uri_rdfs_label),
inference(res,[status(thm),theory(equality)],[45,352]),
[iquote('0:Res:45.0,352.0')] ).
cnf(352,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_domain,u)
| icext(u,uri_rdfs_label) ),
inference(res,[status(thm),theory(equality)],[19,86]),
[iquote('0:Res:19.0,86.0')] ).
cnf(351,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_domain,u)
| icext(u,uri_rdfs_seeAlso) ),
inference(res,[status(thm),theory(equality)],[21,86]),
[iquote('0:Res:21.0,86.0')] ).
cnf(350,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_domain,u)
| icext(u,uri_rdfs_member) ),
inference(res,[status(thm),theory(equality)],[30,86]),
[iquote('0:Res:30.0,86.0')] ).
cnf(349,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_domain,u)
| icext(u,uri_rdf__1) ),
inference(res,[status(thm),theory(equality)],[32,86]),
[iquote('0:Res:32.0,86.0')] ).
cnf(348,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_domain,u)
| icext(u,uri_rdf__2) ),
inference(res,[status(thm),theory(equality)],[33,86]),
[iquote('0:Res:33.0,86.0')] ).
cnf(347,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_domain,u)
| icext(u,uri_rdf__3) ),
inference(res,[status(thm),theory(equality)],[34,86]),
[iquote('0:Res:34.0,86.0')] ).
cnf(346,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_domain,u)
| icext(u,uri_rdfs_domain) ),
inference(res,[status(thm),theory(equality)],[45,86]),
[iquote('0:Res:45.0,86.0')] ).
cnf(648,plain,
iext(uri_rdf_type,uri_rdfs_range,uri_rdf_Property),
inference(res,[status(thm),theory(equality)],[647,82]),
[iquote('0:Res:647.0,82.0')] ).
cnf(647,plain,
icext(uri_rdf_Property,uri_rdfs_range),
inference(res,[status(thm),theory(equality)],[45,345]),
[iquote('0:Res:45.0,345.0')] ).
cnf(345,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_domain,u)
| icext(u,uri_rdfs_range) ),
inference(res,[status(thm),theory(equality)],[48,86]),
[iquote('0:Res:48.0,86.0')] ).
cnf(344,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_domain,u)
| icext(u,uri_rdf_object) ),
inference(res,[status(thm),theory(equality)],[50,86]),
[iquote('0:Res:50.0,86.0')] ).
cnf(343,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_domain,u)
| icext(u,uri_rdf_predicate) ),
inference(res,[status(thm),theory(equality)],[52,86]),
[iquote('0:Res:52.0,86.0')] ).
cnf(342,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_domain,u)
| icext(u,uri_rdf_subject) ),
inference(res,[status(thm),theory(equality)],[54,86]),
[iquote('0:Res:54.0,86.0')] ).
cnf(637,plain,
iext(uri_rdf_type,uri_rdfs_domain,uri_rdf_Property),
inference(res,[status(thm),theory(equality)],[635,82]),
[iquote('0:Res:635.0,82.0')] ).
cnf(635,plain,
icext(uri_rdf_Property,uri_rdfs_domain),
inference(res,[status(thm),theory(equality)],[48,340]),
[iquote('0:Res:48.0,340.0')] ).
cnf(341,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_subClassOf,u)
| icext(u,uri_rdfs_Datatype) ),
inference(res,[status(thm),theory(equality)],[44,86]),
[iquote('0:Res:44.0,86.0')] ).
cnf(340,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_range,u)
| icext(u,uri_rdfs_domain) ),
inference(res,[status(thm),theory(equality)],[46,86]),
[iquote('0:Res:46.0,86.0')] ).
cnf(338,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_domain,u)
| icext(u,uri_rdfs_subClassOf) ),
inference(res,[status(thm),theory(equality)],[56,86]),
[iquote('0:Res:56.0,86.0')] ).
cnf(627,plain,
iext(uri_rdf_type,uri_rdfs_subClassOf,uri_rdf_Property),
inference(res,[status(thm),theory(equality)],[626,82]),
[iquote('0:Res:626.0,82.0')] ).
cnf(626,plain,
icext(uri_rdf_Property,uri_rdfs_subClassOf),
inference(res,[status(thm),theory(equality)],[48,337]),
[iquote('0:Res:48.0,337.0')] ).
cnf(337,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_range,u)
| icext(u,uri_rdfs_subClassOf) ),
inference(res,[status(thm),theory(equality)],[57,86]),
[iquote('0:Res:57.0,86.0')] ).
cnf(336,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_domain,u)
| icext(u,uri_rdfs_subPropertyOf) ),
inference(res,[status(thm),theory(equality)],[58,86]),
[iquote('0:Res:58.0,86.0')] ).
cnf(618,plain,
iext(uri_rdf_type,uri_rdfs_subPropertyOf,uri_rdf_Property),
inference(res,[status(thm),theory(equality)],[617,82]),
[iquote('0:Res:617.0,82.0')] ).
cnf(617,plain,
icext(uri_rdf_Property,uri_rdfs_subPropertyOf),
inference(res,[status(thm),theory(equality)],[48,335]),
[iquote('0:Res:48.0,335.0')] ).
cnf(335,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_range,u)
| icext(u,uri_rdfs_subPropertyOf) ),
inference(res,[status(thm),theory(equality)],[59,86]),
[iquote('0:Res:59.0,86.0')] ).
cnf(334,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_domain,u)
| icext(u,uri_rdf_type) ),
inference(res,[status(thm),theory(equality)],[60,86]),
[iquote('0:Res:60.0,86.0')] ).
cnf(333,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_range,u)
| icext(u,uri_rdf_type) ),
inference(res,[status(thm),theory(equality)],[61,86]),
[iquote('0:Res:61.0,86.0')] ).
cnf(332,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_range,u)
| icext(u,uri_rdfs_seeAlso) ),
inference(res,[status(thm),theory(equality)],[22,86]),
[iquote('0:Res:22.0,86.0')] ).
cnf(607,plain,
iext(uri_rdf_type,uri_rdfs_member,uri_rdf_Property),
inference(res,[status(thm),theory(equality)],[605,82]),
[iquote('0:Res:605.0,82.0')] ).
cnf(605,plain,
icext(uri_rdf_Property,uri_rdfs_member),
inference(res,[status(thm),theory(equality)],[48,330]),
[iquote('0:Res:48.0,330.0')] ).
cnf(331,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_range,u)
| icext(u,uri_rdf_first) ),
inference(res,[status(thm),theory(equality)],[24,86]),
[iquote('0:Res:24.0,86.0')] ).
cnf(330,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_range,u)
| icext(u,uri_rdfs_member) ),
inference(res,[status(thm),theory(equality)],[31,86]),
[iquote('0:Res:31.0,86.0')] ).
cnf(329,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_range,u)
| icext(u,uri_rdf__1) ),
inference(res,[status(thm),theory(equality)],[35,86]),
[iquote('0:Res:35.0,86.0')] ).
cnf(328,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_range,u)
| icext(u,uri_rdf__2) ),
inference(res,[status(thm),theory(equality)],[36,86]),
[iquote('0:Res:36.0,86.0')] ).
cnf(596,plain,
ip(uri_rdf_predicate),
inference(res,[status(thm),theory(equality)],[595,72]),
[iquote('0:Res:595.0,72.0')] ).
cnf(327,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_range,u)
| icext(u,uri_rdf__3) ),
inference(res,[status(thm),theory(equality)],[37,86]),
[iquote('0:Res:37.0,86.0')] ).
cnf(595,plain,
iext(uri_rdf_type,uri_rdf_predicate,uri_rdf_Property),
inference(res,[status(thm),theory(equality)],[594,82]),
[iquote('0:Res:594.0,82.0')] ).
cnf(594,plain,
icext(uri_rdf_Property,uri_rdf_predicate),
inference(res,[status(thm),theory(equality)],[48,326]),
[iquote('0:Res:48.0,326.0')] ).
cnf(326,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_range,u)
| icext(u,uri_rdf_predicate) ),
inference(res,[status(thm),theory(equality)],[53,86]),
[iquote('0:Res:53.0,86.0')] ).
cnf(325,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_range,u)
| icext(u,uri_rdf_subject) ),
inference(res,[status(thm),theory(equality)],[55,86]),
[iquote('0:Res:55.0,86.0')] ).
cnf(324,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_domain,u)
| icext(u,uri_rdf_value) ),
inference(res,[status(thm),theory(equality)],[62,86]),
[iquote('0:Res:62.0,86.0')] ).
cnf(323,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_range,u)
| icext(u,uri_rdf_value) ),
inference(res,[status(thm),theory(equality)],[63,86]),
[iquote('0:Res:63.0,86.0')] ).
cnf(318,plain,
( ~ iext(uri_rdfs_range,uri_ex,u)
| icext(u,uri_ex_o) ),
inference(res,[status(thm),theory(equality)],[2,87]),
[iquote('0:Res:2.0,87.0')] ).
cnf(584,plain,
iext(uri_rdf_type,uri_rdfs_seeAlso,uri_rdf_Property),
inference(res,[status(thm),theory(equality)],[583,82]),
[iquote('0:Res:583.0,82.0')] ).
cnf(583,plain,
icext(uri_rdf_Property,uri_rdfs_seeAlso),
inference(res,[status(thm),theory(equality)],[59,316]),
[iquote('0:Res:59.0,316.0')] ).
cnf(316,plain,
( ~ iext(uri_rdfs_range,uri_rdfs_subPropertyOf,u)
| icext(u,uri_rdfs_seeAlso) ),
inference(res,[status(thm),theory(equality)],[18,87]),
[iquote('0:Res:18.0,87.0')] ).
cnf(312,plain,
( ~ iext(uri_rdfs_range,uri_rdfs_range,u)
| icext(u,uri_rdfs_Literal) ),
inference(res,[status(thm),theory(equality)],[20,87]),
[iquote('0:Res:20.0,87.0')] ).
cnf(311,plain,
( ~ iext(uri_rdfs_range,uri_rdfs_range,u)
| icext(u,uri_rdf_List) ),
inference(res,[status(thm),theory(equality)],[26,87]),
[iquote('0:Res:26.0,87.0')] ).
cnf(309,plain,
( ~ iext(uri_rdfs_range,uri_rdf_type,u)
| icext(u,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[208,87]),
[iquote('0:Res:208.0,87.0')] ).
cnf(308,plain,
( ~ iext(uri_rdfs_range,uri_rdf_type,u)
| icext(u,uri_rdf_List) ),
inference(res,[status(thm),theory(equality)],[4,87]),
[iquote('0:Res:4.0,87.0')] ).
cnf(298,plain,
( ~ iext(uri_rdfs_range,uri_rdf_type,u)
| icext(u,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[11,87]),
[iquote('0:Res:11.0,87.0')] ).
cnf(572,plain,
iext(uri_rdf_type,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Class),
inference(res,[status(thm),theory(equality)],[570,82]),
[iquote('0:Res:570.0,82.0')] ).
cnf(570,plain,
icext(uri_rdfs_Class,uri_rdfs_ContainerMembershipProperty),
inference(res,[status(thm),theory(equality)],[61,295]),
[iquote('0:Res:61.0,295.0')] ).
cnf(295,plain,
( ~ iext(uri_rdfs_range,uri_rdf_type,u)
| icext(u,uri_rdfs_ContainerMembershipProperty) ),
inference(res,[status(thm),theory(equality)],[40,87]),
[iquote('0:Res:40.0,87.0')] ).
cnf(563,plain,
iext(uri_rdf_type,uri_rdfs_Container,uri_rdfs_Class),
inference(res,[status(thm),theory(equality)],[561,82]),
[iquote('0:Res:561.0,82.0')] ).
cnf(292,plain,
( ~ iext(uri_rdfs_range,uri_rdfs_subClassOf,u)
| icext(u,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[29,87]),
[iquote('0:Res:29.0,87.0')] ).
cnf(561,plain,
icext(uri_rdfs_Class,uri_rdfs_Container),
inference(res,[status(thm),theory(equality)],[57,289]),
[iquote('0:Res:57.0,289.0')] ).
cnf(289,plain,
( ~ iext(uri_rdfs_range,uri_rdfs_subClassOf,u)
| icext(u,uri_rdfs_Container) ),
inference(res,[status(thm),theory(equality)],[41,87]),
[iquote('0:Res:41.0,87.0')] ).
cnf(555,plain,
iext(uri_rdf_type,uri_rdfs_Literal,uri_rdfs_Class),
inference(res,[status(thm),theory(equality)],[553,82]),
[iquote('0:Res:553.0,82.0')] ).
cnf(553,plain,
icext(uri_rdfs_Class,uri_rdfs_Literal),
inference(res,[status(thm),theory(equality)],[57,288]),
[iquote('0:Res:57.0,288.0')] ).
cnf(288,plain,
( ~ iext(uri_rdfs_range,uri_rdfs_subClassOf,u)
| icext(u,uri_rdfs_Literal) ),
inference(res,[status(thm),theory(equality)],[42,87]),
[iquote('0:Res:42.0,87.0')] ).
cnf(537,plain,
iext(uri_rdf_type,uri_rdfs_Datatype,uri_rdfs_Class),
inference(res,[status(thm),theory(equality)],[535,82]),
[iquote('0:Res:535.0,82.0')] ).
cnf(534,plain,
iext(uri_rdf_type,uri_rdf_List,uri_rdfs_Class),
inference(res,[status(thm),theory(equality)],[530,82]),
[iquote('0:Res:530.0,82.0')] ).
cnf(532,plain,
iext(uri_rdf_type,uri_rdfs_Statement,uri_rdfs_Class),
inference(res,[status(thm),theory(equality)],[529,82]),
[iquote('0:Res:529.0,82.0')] ).
cnf(535,plain,
icext(uri_rdfs_Class,uri_rdfs_Datatype),
inference(res,[status(thm),theory(equality)],[61,287]),
[iquote('0:Res:61.0,287.0')] ).
cnf(287,plain,
( ~ iext(uri_rdfs_range,uri_rdf_type,u)
| icext(u,uri_rdfs_Datatype) ),
inference(res,[status(thm),theory(equality)],[43,87]),
[iquote('0:Res:43.0,87.0')] ).
cnf(533,plain,
ic(uri_rdf_List),
inference(res,[status(thm),theory(equality)],[530,66]),
[iquote('0:Res:530.0,66.0')] ).
cnf(530,plain,
icext(uri_rdfs_Class,uri_rdf_List),
inference(res,[status(thm),theory(equality)],[46,285]),
[iquote('0:Res:46.0,285.0')] ).
cnf(531,plain,
ic(uri_rdfs_Statement),
inference(res,[status(thm),theory(equality)],[529,66]),
[iquote('0:Res:529.0,66.0')] ).
cnf(529,plain,
icext(uri_rdfs_Class,uri_rdfs_Statement),
inference(res,[status(thm),theory(equality)],[46,272]),
[iquote('0:Res:46.0,272.0')] ).
cnf(285,plain,
( ~ iext(uri_rdfs_range,uri_rdfs_domain,u)
| icext(u,uri_rdf_List) ),
inference(res,[status(thm),theory(equality)],[25,87]),
[iquote('0:Res:25.0,87.0')] ).
cnf(272,plain,
( ~ iext(uri_rdfs_range,uri_rdfs_domain,u)
| icext(u,uri_rdfs_Statement) ),
inference(res,[status(thm),theory(equality)],[54,87]),
[iquote('0:Res:54.0,87.0')] ).
cnf(271,plain,
( ~ iext(uri_rdfs_range,uri_rdfs_subClassOf,u)
| icext(u,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[44,87]),
[iquote('0:Res:44.0,87.0')] ).
cnf(269,plain,
( ~ iext(uri_rdfs_range,uri_rdf_type,u)
| icext(u,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[47,87]),
[iquote('0:Res:47.0,87.0')] ).
cnf(268,plain,
( ~ iext(uri_rdfs_range,uri_rdfs_domain,u)
| icext(u,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[56,87]),
[iquote('0:Res:56.0,87.0')] ).
cnf(266,plain,
( ~ iext(uri_rdfs_range,uri_rdfs_domain,u)
| icext(u,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[58,87]),
[iquote('0:Res:58.0,87.0')] ).
cnf(265,plain,
( ~ iext(uri_rdfs_range,uri_rdfs_range,u)
| icext(u,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[59,87]),
[iquote('0:Res:59.0,87.0')] ).
cnf(518,plain,
iext(uri_rdf_type,uri_rdfs_Class,uri_rdfs_Class),
inference(res,[status(thm),theory(equality)],[516,82]),
[iquote('0:Res:516.0,82.0')] ).
cnf(516,plain,
icext(uri_rdfs_Class,uri_rdfs_Class),
inference(res,[status(thm),theory(equality)],[49,263]),
[iquote('0:Res:49.0,263.0')] ).
cnf(263,plain,
( ~ iext(uri_rdfs_range,uri_rdfs_range,u)
| icext(u,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[61,87]),
[iquote('0:Res:61.0,87.0')] ).
cnf(254,plain,
( ~ iext(uri_rdfs_range,uri_rdfs_domain,u)
| icext(u,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[62,87]),
[iquote('0:Res:62.0,87.0')] ).
cnf(509,plain,
iext(uri_rdf_type,uri_rdfs_Resource,uri_rdfs_Class),
inference(res,[status(thm),theory(equality)],[507,82]),
[iquote('0:Res:507.0,82.0')] ).
cnf(507,plain,
icext(uri_rdfs_Class,uri_rdfs_Resource),
inference(res,[status(thm),theory(equality)],[49,253]),
[iquote('0:Res:49.0,253.0')] ).
cnf(253,plain,
( ~ iext(uri_rdfs_range,uri_rdfs_range,u)
| icext(u,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[63,87]),
[iquote('0:Res:63.0,87.0')] ).
cnf(245,plain,
( ~ icext(uri_rdfs_ContainerMembershipProperty,u)
| icext(uri_rdf_Property,u) ),
inference(res,[status(thm),theory(equality)],[29,85]),
[iquote('0:Res:29.0,85.1')] ).
cnf(211,plain,
( ~ iext(uri_rdf_type,uri_ex_o,uri_owl_Thing)
| ~ iext(uri_rdf_type,uri_ex,uri_owl_ObjectProperty)
| ~ iext(uri_rdf_type,uri_ex,uri_rdf_Property)
| ~ iext(uri_rdf_type,uri_ex,uri_owl_Thing)
| ~ iext(uri_rdf_type,uri_ex_s,uri_owl_Thing) ),
inference(mrr,[status(thm)],[91,208]),
[iquote('0:MRR:91.7,91.5,91.1,208.0')] ).
cnf(244,plain,
( ~ icext(uri_rdf_Alt,u)
| icext(uri_rdfs_Container,u) ),
inference(res,[status(thm),theory(equality)],[27,85]),
[iquote('0:Res:27.0,85.1')] ).
cnf(243,plain,
( ~ icext(uri_rdf_Bag,u)
| icext(uri_rdfs_Container,u) ),
inference(res,[status(thm),theory(equality)],[28,85]),
[iquote('0:Res:28.0,85.1')] ).
cnf(242,plain,
( ~ icext(uri_rdfs_Seq,u)
| icext(uri_rdfs_Container,u) ),
inference(res,[status(thm),theory(equality)],[41,85]),
[iquote('0:Res:41.0,85.1')] ).
cnf(241,plain,
( ~ icext(uri_rdf_XMLLiteral,u)
| icext(uri_rdfs_Literal,u) ),
inference(res,[status(thm),theory(equality)],[42,85]),
[iquote('0:Res:42.0,85.1')] ).
cnf(89,axiom,
( ~ iext(u,v,w)
| ~ iext(uri_rdfs_subPropertyOf,u,x)
| iext(x,v,w) ),
file('SWB005+4.p',unknown),
[] ).
cnf(428,plain,
iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Class),
inference(res,[status(thm),theory(equality)],[426,82]),
[iquote('0:Res:426.0,82.0')] ).
cnf(426,plain,
icext(uri_rdfs_Class,uri_rdf_XMLLiteral),
inference(res,[status(thm),theory(equality)],[215,240]),
[iquote('0:Res:215.0,240.0')] ).
cnf(240,plain,
( ~ icext(uri_rdfs_Datatype,u)
| icext(uri_rdfs_Class,u) ),
inference(res,[status(thm),theory(equality)],[44,85]),
[iquote('0:Res:44.0,85.1')] ).
cnf(210,plain,
( ~ ic(u)
| iext(uri_rdf_type,u,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[65,82]),
[iquote('0:Res:65.1,82.0')] ).
cnf(88,axiom,
( ~ iext(uri_rdfs_subClassOf,u,v)
| ~ iext(uri_rdfs_subClassOf,w,u)
| iext(uri_rdfs_subClassOf,w,v) ),
file('SWB005+4.p',unknown),
[] ).
cnf(228,plain,
( ~ ip(u)
| icext(uri_rdf_Property,u) ),
inference(res,[status(thm),theory(equality)],[73,81]),
[iquote('0:Res:73.1,81.0')] ).
cnf(248,plain,
iext(uri_rdfs_subPropertyOf,uri_rdf__1,uri_rdfs_member),
inference(res,[status(thm),theory(equality)],[218,83]),
[iquote('0:Res:218.0,83.0')] ).
cnf(238,plain,
iext(uri_rdfs_subPropertyOf,uri_rdf__2,uri_rdfs_member),
inference(res,[status(thm),theory(equality)],[217,83]),
[iquote('0:Res:217.0,83.0')] ).
cnf(393,plain,
ip(uri_rdfs_member),
inference(res,[status(thm),theory(equality)],[236,79]),
[iquote('0:Res:236.0,79.0')] ).
cnf(90,axiom,
( ~ iext(uri_rdfs_subPropertyOf,u,v)
| ~ iext(uri_rdfs_subPropertyOf,w,u)
| iext(uri_rdfs_subPropertyOf,w,v) ),
file('SWB005+4.p',unknown),
[] ).
cnf(236,plain,
iext(uri_rdfs_subPropertyOf,uri_rdf__3,uri_rdfs_member),
inference(res,[status(thm),theory(equality)],[216,83]),
[iquote('0:Res:216.0,83.0')] ).
cnf(229,plain,
icext(uri_rdf_List,uri_rdf_nil),
inference(res,[status(thm),theory(equality)],[4,81]),
[iquote('0:Res:4.0,81.0')] ).
cnf(227,plain,
icext(uri_rdf_Property,uri_rdf_type),
inference(res,[status(thm),theory(equality)],[13,81]),
[iquote('0:Res:13.0,81.0')] ).
cnf(226,plain,
icext(uri_rdf_Property,uri_rdf_first),
inference(res,[status(thm),theory(equality)],[3,81]),
[iquote('0:Res:3.0,81.0')] ).
cnf(86,axiom,
( ~ iext(u,v,w)
| ~ iext(uri_rdfs_domain,u,x)
| icext(x,v) ),
file('SWB005+4.p',unknown),
[] ).
cnf(225,plain,
icext(uri_rdf_Property,uri_rdf_rest),
inference(res,[status(thm),theory(equality)],[5,81]),
[iquote('0:Res:5.0,81.0')] ).
cnf(224,plain,
icext(uri_rdf_Property,uri_rdf__1),
inference(res,[status(thm),theory(equality)],[6,81]),
[iquote('0:Res:6.0,81.0')] ).
cnf(223,plain,
icext(uri_rdf_Property,uri_rdf__2),
inference(res,[status(thm),theory(equality)],[7,81]),
[iquote('0:Res:7.0,81.0')] ).
cnf(222,plain,
icext(uri_rdf_Property,uri_rdf__3),
inference(res,[status(thm),theory(equality)],[8,81]),
[iquote('0:Res:8.0,81.0')] ).
cnf(87,axiom,
( ~ iext(u,v,w)
| ~ iext(uri_rdfs_range,u,x)
| icext(x,w) ),
file('SWB005+4.p',unknown),
[] ).
cnf(221,plain,
icext(uri_rdf_Property,uri_rdf_object),
inference(res,[status(thm),theory(equality)],[9,81]),
[iquote('0:Res:9.0,81.0')] ).
cnf(220,plain,
icext(uri_rdf_Property,uri_rdf_value),
inference(res,[status(thm),theory(equality)],[10,81]),
[iquote('0:Res:10.0,81.0')] ).
cnf(219,plain,
icext(uri_rdf_Property,uri_rdf_subject),
inference(res,[status(thm),theory(equality)],[11,81]),
[iquote('0:Res:11.0,81.0')] ).
cnf(218,plain,
icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__1),
inference(res,[status(thm),theory(equality)],[38,81]),
[iquote('0:Res:38.0,81.0')] ).
cnf(85,axiom,
( ~ icext(u,v)
| ~ iext(uri_rdfs_subClassOf,u,w)
| icext(w,v) ),
file('SWB005+4.p',unknown),
[] ).
cnf(217,plain,
icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__2),
inference(res,[status(thm),theory(equality)],[39,81]),
[iquote('0:Res:39.0,81.0')] ).
cnf(216,plain,
icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__3),
inference(res,[status(thm),theory(equality)],[40,81]),
[iquote('0:Res:40.0,81.0')] ).
cnf(215,plain,
icext(uri_rdfs_Datatype,uri_rdf_XMLLiteral),
inference(res,[status(thm),theory(equality)],[43,81]),
[iquote('0:Res:43.0,81.0')] ).
cnf(214,plain,
icext(uri_rdfs_Class,uri_rdf_Property),
inference(res,[status(thm),theory(equality)],[47,81]),
[iquote('0:Res:47.0,81.0')] ).
cnf(81,axiom,
( ~ iext(uri_rdf_type,u,v)
| icext(v,u) ),
file('SWB005+4.p',unknown),
[] ).
cnf(209,plain,
( ~ lv(u)
| iext(uri_rdf_type,u,uri_rdfs_Literal) ),
inference(res,[status(thm),theory(equality)],[69,82]),
[iquote('0:Res:69.1,82.0')] ).
cnf(208,plain,
iext(uri_rdf_type,u,uri_rdfs_Resource),
inference(res,[status(thm),theory(equality)],[92,82]),
[iquote('0:Res:92.0,82.0')] ).
cnf(82,axiom,
( ~ icext(u,v)
| iext(uri_rdf_type,v,u) ),
file('SWB005+4.p',unknown),
[] ).
cnf(198,plain,
ic(uri_rdfs_Resource),
inference(ems,[status(thm)],[124,131]),
[iquote('0:EmS:124.0,131.0')] ).
cnf(83,axiom,
( ~ icext(uri_rdfs_ContainerMembershipProperty,u)
| iext(uri_rdfs_subPropertyOf,u,uri_rdfs_member) ),
file('SWB005+4.p',unknown),
[] ).
cnf(197,plain,
ip(uri_ex),
inference(res,[status(thm),theory(equality)],[2,71]),
[iquote('0:Res:2.0,71.0')] ).
cnf(195,plain,
ip(uri_rdfs_subPropertyOf),
inference(res,[status(thm),theory(equality)],[18,71]),
[iquote('0:Res:18.0,71.0')] ).
cnf(152,plain,
ip(uri_rdfs_subClassOf),
inference(res,[status(thm),theory(equality)],[44,71]),
[iquote('0:Res:44.0,71.0')] ).
cnf(84,axiom,
( ~ icext(uri_rdfs_Datatype,u)
| iext(uri_rdfs_subClassOf,u,uri_rdfs_Literal) ),
file('SWB005+4.p',unknown),
[] ).
cnf(135,plain,
ip(uri_rdfs_domain),
inference(res,[status(thm),theory(equality)],[62,71]),
[iquote('0:Res:62.0,71.0')] ).
cnf(134,plain,
ip(uri_rdfs_range),
inference(res,[status(thm),theory(equality)],[63,71]),
[iquote('0:Res:63.0,71.0')] ).
cnf(131,plain,
ic(uri_rdfs_ContainerMembershipProperty),
inference(res,[status(thm),theory(equality)],[29,75]),
[iquote('0:Res:29.0,75.0')] ).
cnf(130,plain,
ic(uri_rdf_Alt),
inference(res,[status(thm),theory(equality)],[27,75]),
[iquote('0:Res:27.0,75.0')] ).
cnf(71,axiom,
( ~ iext(u,v,w)
| ip(u) ),
file('SWB005+4.p',unknown),
[] ).
cnf(129,plain,
ic(uri_rdf_Bag),
inference(res,[status(thm),theory(equality)],[28,75]),
[iquote('0:Res:28.0,75.0')] ).
cnf(128,plain,
ic(uri_rdfs_Seq),
inference(res,[status(thm),theory(equality)],[41,75]),
[iquote('0:Res:41.0,75.0')] ).
cnf(127,plain,
ic(uri_rdf_XMLLiteral),
inference(res,[status(thm),theory(equality)],[42,75]),
[iquote('0:Res:42.0,75.0')] ).
cnf(126,plain,
ic(uri_rdfs_Datatype),
inference(res,[status(thm),theory(equality)],[44,75]),
[iquote('0:Res:44.0,75.0')] ).
cnf(75,axiom,
( ~ iext(uri_rdfs_subClassOf,u,v)
| ic(u) ),
file('SWB005+4.p',unknown),
[] ).
cnf(123,plain,
ic(uri_rdf_Property),
inference(res,[status(thm),theory(equality)],[29,76]),
[iquote('0:Res:29.0,76.0')] ).
cnf(120,plain,
ic(uri_rdfs_Container),
inference(res,[status(thm),theory(equality)],[41,76]),
[iquote('0:Res:41.0,76.0')] ).
cnf(119,plain,
ic(uri_rdfs_Literal),
inference(res,[status(thm),theory(equality)],[42,76]),
[iquote('0:Res:42.0,76.0')] ).
cnf(118,plain,
ic(uri_rdfs_Class),
inference(res,[status(thm),theory(equality)],[44,76]),
[iquote('0:Res:44.0,76.0')] ).
cnf(76,axiom,
( ~ iext(uri_rdfs_subClassOf,u,v)
| ic(v) ),
file('SWB005+4.p',unknown),
[] ).
cnf(116,plain,
ip(uri_rdfs_isDefinedBy),
inference(res,[status(thm),theory(equality)],[18,78]),
[iquote('0:Res:18.0,78.0')] ).
cnf(78,axiom,
( ~ iext(uri_rdfs_subPropertyOf,u,v)
| ip(u) ),
file('SWB005+4.p',unknown),
[] ).
cnf(114,plain,
ip(uri_rdfs_seeAlso),
inference(res,[status(thm),theory(equality)],[18,79]),
[iquote('0:Res:18.0,79.0')] ).
cnf(112,plain,
ip(uri_rdf_type),
inference(res,[status(thm),theory(equality)],[13,72]),
[iquote('0:Res:13.0,72.0')] ).
cnf(79,axiom,
( ~ iext(uri_rdfs_subPropertyOf,u,v)
| ip(v) ),
file('SWB005+4.p',unknown),
[] ).
cnf(111,plain,
ip(uri_rdf_first),
inference(res,[status(thm),theory(equality)],[3,72]),
[iquote('0:Res:3.0,72.0')] ).
cnf(110,plain,
ip(uri_rdf_rest),
inference(res,[status(thm),theory(equality)],[5,72]),
[iquote('0:Res:5.0,72.0')] ).
cnf(109,plain,
ip(uri_rdf__1),
inference(res,[status(thm),theory(equality)],[6,72]),
[iquote('0:Res:6.0,72.0')] ).
cnf(108,plain,
ip(uri_rdf__2),
inference(res,[status(thm),theory(equality)],[7,72]),
[iquote('0:Res:7.0,72.0')] ).
cnf(77,axiom,
( ~ ic(u)
| iext(uri_rdfs_subClassOf,u,u) ),
file('SWB005+4.p',unknown),
[] ).
cnf(107,plain,
ip(uri_rdf__3),
inference(res,[status(thm),theory(equality)],[8,72]),
[iquote('0:Res:8.0,72.0')] ).
cnf(106,plain,
ip(uri_rdf_object),
inference(res,[status(thm),theory(equality)],[9,72]),
[iquote('0:Res:9.0,72.0')] ).
cnf(105,plain,
ip(uri_rdf_value),
inference(res,[status(thm),theory(equality)],[10,72]),
[iquote('0:Res:10.0,72.0')] ).
cnf(104,plain,
ip(uri_rdf_subject),
inference(res,[status(thm),theory(equality)],[11,72]),
[iquote('0:Res:11.0,72.0')] ).
cnf(80,axiom,
( ~ ip(u)
| iext(uri_rdfs_subPropertyOf,u,u) ),
file('SWB005+4.p',unknown),
[] ).
cnf(72,axiom,
( ~ iext(uri_rdf_type,u,uri_rdf_Property)
| ip(u) ),
file('SWB005+4.p',unknown),
[] ).
cnf(73,axiom,
( ~ ip(u)
| iext(uri_rdf_type,u,uri_rdf_Property) ),
file('SWB005+4.p',unknown),
[] ).
cnf(74,axiom,
( ~ ic(u)
| iext(uri_rdfs_subClassOf,u,uri_rdfs_Resource) ),
file('SWB005+4.p',unknown),
[] ).
cnf(66,axiom,
( ~ icext(uri_rdfs_Class,u)
| ic(u) ),
file('SWB005+4.p',unknown),
[] ).
cnf(70,axiom,
( ~ icext(uri_rdfs_Literal,u)
| lv(u) ),
file('SWB005+4.p',unknown),
[] ).
cnf(65,axiom,
( ~ ic(u)
| icext(uri_rdfs_Class,u) ),
file('SWB005+4.p',unknown),
[] ).
cnf(69,axiom,
( ~ lv(u)
| icext(uri_rdfs_Literal,u) ),
file('SWB005+4.p',unknown),
[] ).
cnf(13,axiom,
iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property),
file('SWB005+4.p',unknown),
[] ).
cnf(45,axiom,
iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_Property),
file('SWB005+4.p',unknown),
[] ).
cnf(49,axiom,
iext(uri_rdfs_range,uri_rdfs_range,uri_rdfs_Class),
file('SWB005+4.p',unknown),
[] ).
cnf(2,axiom,
iext(uri_ex,uri_ex_s,uri_ex_o),
file('SWB005+4.p',unknown),
[] ).
cnf(3,axiom,
iext(uri_rdf_type,uri_rdf_first,uri_rdf_Property),
file('SWB005+4.p',unknown),
[] ).
cnf(4,axiom,
iext(uri_rdf_type,uri_rdf_nil,uri_rdf_List),
file('SWB005+4.p',unknown),
[] ).
cnf(5,axiom,
iext(uri_rdf_type,uri_rdf_rest,uri_rdf_Property),
file('SWB005+4.p',unknown),
[] ).
cnf(6,axiom,
iext(uri_rdf_type,uri_rdf__1,uri_rdf_Property),
file('SWB005+4.p',unknown),
[] ).
cnf(7,axiom,
iext(uri_rdf_type,uri_rdf__2,uri_rdf_Property),
file('SWB005+4.p',unknown),
[] ).
cnf(8,axiom,
iext(uri_rdf_type,uri_rdf__3,uri_rdf_Property),
file('SWB005+4.p',unknown),
[] ).
cnf(9,axiom,
iext(uri_rdf_type,uri_rdf_object,uri_rdf_Property),
file('SWB005+4.p',unknown),
[] ).
cnf(10,axiom,
iext(uri_rdf_type,uri_rdf_value,uri_rdf_Property),
file('SWB005+4.p',unknown),
[] ).
cnf(11,axiom,
iext(uri_rdf_type,uri_rdf_subject,uri_rdf_Property),
file('SWB005+4.p',unknown),
[] ).
cnf(14,axiom,
iext(uri_rdfs_domain,uri_rdfs_comment,uri_rdfs_Resource),
file('SWB005+4.p',unknown),
[] ).
cnf(15,axiom,
iext(uri_rdfs_range,uri_rdfs_comment,uri_rdfs_Literal),
file('SWB005+4.p',unknown),
[] ).
cnf(16,axiom,
iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,uri_rdfs_Resource),
file('SWB005+4.p',unknown),
[] ).
cnf(17,axiom,
iext(uri_rdfs_range,uri_rdfs_isDefinedBy,uri_rdfs_Resource),
file('SWB005+4.p',unknown),
[] ).
cnf(18,axiom,
iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),
file('SWB005+4.p',unknown),
[] ).
cnf(19,axiom,
iext(uri_rdfs_domain,uri_rdfs_label,uri_rdfs_Resource),
file('SWB005+4.p',unknown),
[] ).
cnf(20,axiom,
iext(uri_rdfs_range,uri_rdfs_label,uri_rdfs_Literal),
file('SWB005+4.p',unknown),
[] ).
cnf(21,axiom,
iext(uri_rdfs_domain,uri_rdfs_seeAlso,uri_rdfs_Resource),
file('SWB005+4.p',unknown),
[] ).
cnf(22,axiom,
iext(uri_rdfs_range,uri_rdfs_seeAlso,uri_rdfs_Resource),
file('SWB005+4.p',unknown),
[] ).
cnf(23,axiom,
iext(uri_rdfs_domain,uri_rdf_first,uri_rdf_List),
file('SWB005+4.p',unknown),
[] ).
cnf(24,axiom,
iext(uri_rdfs_range,uri_rdf_first,uri_rdfs_Resource),
file('SWB005+4.p',unknown),
[] ).
cnf(25,axiom,
iext(uri_rdfs_domain,uri_rdf_rest,uri_rdf_List),
file('SWB005+4.p',unknown),
[] ).
cnf(26,axiom,
iext(uri_rdfs_range,uri_rdf_rest,uri_rdf_List),
file('SWB005+4.p',unknown),
[] ).
cnf(27,axiom,
iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Container),
file('SWB005+4.p',unknown),
[] ).
cnf(28,axiom,
iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Container),
file('SWB005+4.p',unknown),
[] ).
cnf(29,axiom,
iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),
file('SWB005+4.p',unknown),
[] ).
cnf(30,axiom,
iext(uri_rdfs_domain,uri_rdfs_member,uri_rdfs_Resource),
file('SWB005+4.p',unknown),
[] ).
cnf(31,axiom,
iext(uri_rdfs_range,uri_rdfs_member,uri_rdfs_Resource),
file('SWB005+4.p',unknown),
[] ).
cnf(32,axiom,
iext(uri_rdfs_domain,uri_rdf__1,uri_rdfs_Resource),
file('SWB005+4.p',unknown),
[] ).
cnf(33,axiom,
iext(uri_rdfs_domain,uri_rdf__2,uri_rdfs_Resource),
file('SWB005+4.p',unknown),
[] ).
cnf(34,axiom,
iext(uri_rdfs_domain,uri_rdf__3,uri_rdfs_Resource),
file('SWB005+4.p',unknown),
[] ).
cnf(35,axiom,
iext(uri_rdfs_range,uri_rdf__1,uri_rdfs_Resource),
file('SWB005+4.p',unknown),
[] ).
cnf(36,axiom,
iext(uri_rdfs_range,uri_rdf__2,uri_rdfs_Resource),
file('SWB005+4.p',unknown),
[] ).
cnf(37,axiom,
iext(uri_rdfs_range,uri_rdf__3,uri_rdfs_Resource),
file('SWB005+4.p',unknown),
[] ).
cnf(38,axiom,
iext(uri_rdf_type,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),
file('SWB005+4.p',unknown),
[] ).
cnf(39,axiom,
iext(uri_rdf_type,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),
file('SWB005+4.p',unknown),
[] ).
cnf(40,axiom,
iext(uri_rdf_type,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),
file('SWB005+4.p',unknown),
[] ).
cnf(41,axiom,
iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Container),
file('SWB005+4.p',unknown),
[] ).
cnf(42,axiom,
iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Literal),
file('SWB005+4.p',unknown),
[] ).
cnf(43,axiom,
iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Datatype),
file('SWB005+4.p',unknown),
[] ).
cnf(44,axiom,
iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Class),
file('SWB005+4.p',unknown),
[] ).
cnf(46,axiom,
iext(uri_rdfs_range,uri_rdfs_domain,uri_rdfs_Class),
file('SWB005+4.p',unknown),
[] ).
cnf(47,axiom,
iext(uri_rdf_type,uri_rdf_Property,uri_rdfs_Class),
file('SWB005+4.p',unknown),
[] ).
cnf(48,axiom,
iext(uri_rdfs_domain,uri_rdfs_range,uri_rdf_Property),
file('SWB005+4.p',unknown),
[] ).
cnf(50,axiom,
iext(uri_rdfs_domain,uri_rdf_object,uri_rdfs_Statement),
file('SWB005+4.p',unknown),
[] ).
cnf(52,axiom,
iext(uri_rdfs_domain,uri_rdf_predicate,uri_rdfs_Statement),
file('SWB005+4.p',unknown),
[] ).
cnf(53,axiom,
iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Resource),
file('SWB005+4.p',unknown),
[] ).
cnf(54,axiom,
iext(uri_rdfs_domain,uri_rdf_subject,uri_rdfs_Statement),
file('SWB005+4.p',unknown),
[] ).
cnf(55,axiom,
iext(uri_rdfs_range,uri_rdf_subject,uri_rdfs_Resource),
file('SWB005+4.p',unknown),
[] ).
cnf(56,axiom,
iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdfs_Class),
file('SWB005+4.p',unknown),
[] ).
cnf(57,axiom,
iext(uri_rdfs_range,uri_rdfs_subClassOf,uri_rdfs_Class),
file('SWB005+4.p',unknown),
[] ).
cnf(58,axiom,
iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdf_Property),
file('SWB005+4.p',unknown),
[] ).
cnf(59,axiom,
iext(uri_rdfs_range,uri_rdfs_subPropertyOf,uri_rdf_Property),
file('SWB005+4.p',unknown),
[] ).
cnf(60,axiom,
iext(uri_rdfs_domain,uri_rdf_type,uri_rdfs_Resource),
file('SWB005+4.p',unknown),
[] ).
cnf(61,axiom,
iext(uri_rdfs_range,uri_rdf_type,uri_rdfs_Class),
file('SWB005+4.p',unknown),
[] ).
cnf(62,axiom,
iext(uri_rdfs_domain,uri_rdf_value,uri_rdfs_Resource),
file('SWB005+4.p',unknown),
[] ).
cnf(63,axiom,
iext(uri_rdfs_range,uri_rdf_value,uri_rdfs_Resource),
file('SWB005+4.p',unknown),
[] ).
cnf(92,plain,
icext(uri_rdfs_Resource,u),
inference(mrr,[status(thm)],[67,1]),
[iquote('0:MRR:67.0,1.0')] ).
cnf(1,axiom,
ir(u),
file('SWB005+4.p',unknown),
[] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : SWB005+4 : TPTP v8.1.0. Released v5.2.0.
% 0.07/0.13 % Command : run_spass %d %s
% 0.13/0.35 % Computer : n021.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 600
% 0.13/0.35 % DateTime : Wed Jun 1 06:05:15 EDT 2022
% 0.13/0.35 % CPUTime :
% 0.20/0.49
% 0.20/0.49 SPASS V 3.9
% 0.20/0.49 SPASS beiseite: Completion found.
% 0.20/0.49 % SZS status CounterSatisfiable
% 0.20/0.49 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.20/0.49 SPASS derived 796 clauses, backtracked 0 clauses, performed 0 splits and kept 400 clauses.
% 0.20/0.49 SPASS allocated 98042 KBytes.
% 0.20/0.49 SPASS spent 0:00:00.13 on the problem.
% 0.20/0.49 0:00:00.04 for the input.
% 0.20/0.49 0:00:00.03 for the FLOTTER CNF translation.
% 0.20/0.49 0:00:00.01 for inferences.
% 0.20/0.49 0:00:00.00 for the backtracking.
% 0.20/0.49 0:00:00.03 for the reduction.
% 0.20/0.49
% 0.20/0.49
% 0.20/0.49 The saturated set of worked-off clauses is :
% 0.20/0.49 % SZS output start Saturation
% See solution above
%------------------------------------------------------------------------------