%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SWB029+4 : TPTP v8.1.0. Released v5.2.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n024.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:21:34 EDT 2022
% Result : CounterSatisfiable 0.21s 0.51s
% Output : Saturation 0.21s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named 76)
% Comments :
%------------------------------------------------------------------------------
cnf(539,plain,
( ~ ic(u)
| ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,v)
| iext(v,u,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[228,98]),
[iquote('0:Res:228.1,98.0')] ).
cnf(521,plain,
( ~ lv(u)
| ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,v)
| iext(v,u,uri_rdfs_Literal) ),
inference(res,[status(thm),theory(equality)],[227,98]),
[iquote('0:Res:227.1,98.0')] ).
cnf(459,plain,
( ~ lv(u)
| ~ iext(uri_rdfs_range,uri_rdf_type,v)
| icext(v,uri_rdfs_Literal) ),
inference(res,[status(thm),theory(equality)],[227,96]),
[iquote('0:Res:227.1,96.0')] ).
cnf(520,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,v,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[226,98]),
[iquote('0:Res:226.0,98.0')] ).
cnf(528,plain,
( ~ ip(u)
| ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,v)
| iext(v,u,u) ),
inference(res,[status(thm),theory(equality)],[89,98]),
[iquote('0:Res:89.1,98.0')] ).
cnf(949,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,u)
| iext(u,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[896,98]),
[iquote('0:Res:896.0,98.0')] ).
cnf(940,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,u)
| iext(u,uri_rdf_Alt,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[895,98]),
[iquote('0:Res:895.0,98.0')] ).
cnf(931,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,u)
| iext(u,uri_rdf_Bag,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[894,98]),
[iquote('0:Res:894.0,98.0')] ).
cnf(922,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,u)
| iext(u,uri_rdfs_Seq,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[893,98]),
[iquote('0:Res:893.0,98.0')] ).
cnf(502,plain,
( ~ ic(u)
| ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,v)
| iext(v,u,u) ),
inference(res,[status(thm),theory(equality)],[86,98]),
[iquote('0:Res:86.1,98.0')] ).
cnf(913,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,u)
| iext(u,uri_rdf_XMLLiteral,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[892,98]),
[iquote('0:Res:892.0,98.0')] ).
cnf(904,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,u)
| iext(u,uri_rdfs_Datatype,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[891,98]),
[iquote('0:Res:891.0,98.0')] ).
cnf(797,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,skc5,uri_rdf_List) ),
inference(res,[status(thm),theory(equality)],[795,98]),
[iquote('0:Res:795.0,98.0')] ).
cnf(782,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdf_Alt,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[779,98]),
[iquote('0:Res:779.0,98.0')] ).
cnf(515,plain,
( ~ ip(u)
| ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,v)
| iext(v,u,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[82,98]),
[iquote('0:Res:82.1,98.0')] ).
cnf(773,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdf_Bag,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[771,98]),
[iquote('0:Res:771.0,98.0')] ).
cnf(765,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdfs_Seq,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[763,98]),
[iquote('0:Res:763.0,98.0')] ).
cnf(754,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdfs_comment,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[751,98]),
[iquote('0:Res:751.0,98.0')] ).
cnf(746,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdfs_isDefinedBy,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[737,98]),
[iquote('0:Res:737.0,98.0')] ).
cnf(501,plain,
( ~ ic(u)
| ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,v)
| iext(v,u,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[83,98]),
[iquote('0:Res:83.1,98.0')] ).
cnf(740,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdfs_label,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[735,98]),
[iquote('0:Res:735.0,98.0')] ).
cnf(725,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdfs_range,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[722,98]),
[iquote('0:Res:722.0,98.0')] ).
cnf(712,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdfs_domain,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[709,98]),
[iquote('0:Res:709.0,98.0')] ).
cnf(704,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdfs_subClassOf,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[700,98]),
[iquote('0:Res:700.0,98.0')] ).
cnf(414,plain,
( ~ ip(u)
| ~ iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,v)
| icext(v,u) ),
inference(res,[status(thm),theory(equality)],[89,95]),
[iquote('0:Res:89.1,95.0')] ).
cnf(695,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdfs_subPropertyOf,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[692,98]),
[iquote('0:Res:692.0,98.0')] ).
cnf(682,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdfs_member,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[679,98]),
[iquote('0:Res:679.0,98.0')] ).
cnf(671,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdf_predicate,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[668,98]),
[iquote('0:Res:668.0,98.0')] ).
cnf(659,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,skc4,uri_rdf_List) ),
inference(res,[status(thm),theory(equality)],[657,98]),
[iquote('0:Res:657.0,98.0')] ).
cnf(388,plain,
( ~ ic(u)
| ~ iext(uri_rdfs_domain,uri_rdfs_subClassOf,v)
| icext(v,u) ),
inference(res,[status(thm),theory(equality)],[83,95]),
[iquote('0:Res:83.1,95.0')] ).
cnf(650,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdfs_seeAlso,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[647,98]),
[iquote('0:Res:647.0,98.0')] ).
cnf(640,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,skc6,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[638,98]),
[iquote('0:Res:638.0,98.0')] ).
cnf(631,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_owl_Class,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[629,98]),
[iquote('0:Res:629.0,98.0')] ).
cnf(621,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[619,98]),
[iquote('0:Res:619.0,98.0')] ).
cnf(337,plain,
( ~ ip(u)
| ~ iext(uri_rdfs_range,uri_rdfs_subPropertyOf,v)
| icext(v,u) ),
inference(res,[status(thm),theory(equality)],[89,96]),
[iquote('0:Res:89.1,96.0')] ).
cnf(612,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdfs_Container,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[605,98]),
[iquote('0:Res:605.0,98.0')] ).
cnf(607,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdfs_Literal,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[602,98]),
[iquote('0:Res:602.0,98.0')] ).
cnf(596,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdfs_Datatype,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[594,98]),
[iquote('0:Res:594.0,98.0')] ).
cnf(588,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdf_List,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[581,98]),
[iquote('0:Res:581.0,98.0')] ).
cnf(312,plain,
( ~ ic(u)
| ~ iext(uri_rdfs_range,uri_rdfs_subClassOf,v)
| icext(v,u) ),
inference(res,[status(thm),theory(equality)],[86,96]),
[iquote('0:Res:86.1,96.0')] ).
cnf(583,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdfs_Statement,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[578,98]),
[iquote('0:Res:578.0,98.0')] ).
cnf(906,plain,
( ~ iext(uri_rdfs_range,uri_rdfs_subClassOf,u)
| icext(u,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[891,96]),
[iquote('0:Res:891.0,96.0')] ).
cnf(896,plain,
iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Resource),
inference(res,[status(thm),theory(equality)],[37,443]),
[iquote('0:Res:37.0,443.0')] ).
cnf(895,plain,
iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Resource),
inference(res,[status(thm),theory(equality)],[35,443]),
[iquote('0:Res:35.0,443.0')] ).
cnf(102,plain,
( ~ iext(u,uri_ex_w,uri_ex_B)
| ~ iext(uri_rdfs_subPropertyOf,u,uri_rdf_type) ),
inference(res,[status(thm),theory(equality)],[98,72]),
[iquote('0:Res:98.2,72.0')] ).
cnf(894,plain,
iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Resource),
inference(res,[status(thm),theory(equality)],[36,443]),
[iquote('0:Res:36.0,443.0')] ).
cnf(893,plain,
iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Resource),
inference(res,[status(thm),theory(equality)],[49,443]),
[iquote('0:Res:49.0,443.0')] ).
cnf(892,plain,
iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Resource),
inference(res,[status(thm),theory(equality)],[50,443]),
[iquote('0:Res:50.0,443.0')] ).
cnf(891,plain,
iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Resource),
inference(res,[status(thm),theory(equality)],[52,443]),
[iquote('0:Res:52.0,443.0')] ).
cnf(443,plain,
( ~ iext(uri_rdfs_subClassOf,u,v)
| iext(uri_rdfs_subClassOf,u,uri_rdfs_Resource) ),
inference(mrr,[status(thm)],[441,85]),
[iquote('0:MRR:441.0,85.1')] ).
cnf(568,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdfs_Class,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[566,98]),
[iquote('0:Res:566.0,98.0')] ).
cnf(558,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdfs_Resource,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[556,98]),
[iquote('0:Res:556.0,98.0')] ).
cnf(547,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdf_XMLLiteral,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[545,98]),
[iquote('0:Res:545.0,98.0')] ).
cnf(537,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_owl_complementOf,u)
| iext(u,skc7,uri_ex_A) ),
inference(res,[status(thm),theory(equality)],[2,98]),
[iquote('0:Res:2.0,98.0')] ).
cnf(536,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_first,u)
| iext(u,skc5,uri_ex_A) ),
inference(res,[status(thm),theory(equality)],[4,98]),
[iquote('0:Res:4.0,98.0')] ).
cnf(535,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_rest,u)
| iext(u,skc5,skc4) ),
inference(res,[status(thm),theory(equality)],[5,98]),
[iquote('0:Res:5.0,98.0')] ).
cnf(534,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_owl_intersectionOf,u)
| iext(u,skc6,skc5) ),
inference(res,[status(thm),theory(equality)],[6,98]),
[iquote('0:Res:6.0,98.0')] ).
cnf(533,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_rest,u)
| iext(u,skc4,uri_rdf_nil) ),
inference(res,[status(thm),theory(equality)],[7,98]),
[iquote('0:Res:7.0,98.0')] ).
cnf(531,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,u)
| iext(u,uri_rdf__1,uri_rdfs_member) ),
inference(res,[status(thm),theory(equality)],[266,98]),
[iquote('0:Res:266.0,98.0')] ).
cnf(532,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_first,u)
| iext(u,skc4,skc7) ),
inference(res,[status(thm),theory(equality)],[8,98]),
[iquote('0:Res:8.0,98.0')] ).
cnf(530,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,u)
| iext(u,uri_rdf__2,uri_rdfs_member) ),
inference(res,[status(thm),theory(equality)],[256,98]),
[iquote('0:Res:256.0,98.0')] ).
cnf(529,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,u)
| iext(u,uri_rdf__3,uri_rdfs_member) ),
inference(res,[status(thm),theory(equality)],[254,98]),
[iquote('0:Res:254.0,98.0')] ).
cnf(527,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,u)
| iext(u,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso) ),
inference(res,[status(thm),theory(equality)],[26,98]),
[iquote('0:Res:26.0,98.0')] ).
cnf(526,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_range,u)
| iext(u,uri_rdfs_range,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[57,98]),
[iquote('0:Res:57.0,98.0')] ).
cnf(525,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_range,u)
| iext(u,uri_rdfs_isDefinedBy,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[25,98]),
[iquote('0:Res:25.0,98.0')] ).
cnf(524,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_range,u)
| iext(u,uri_rdfs_comment,uri_rdfs_Literal) ),
inference(res,[status(thm),theory(equality)],[23,98]),
[iquote('0:Res:23.0,98.0')] ).
cnf(523,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_range,u)
| iext(u,uri_rdfs_label,uri_rdfs_Literal) ),
inference(res,[status(thm),theory(equality)],[28,98]),
[iquote('0:Res:28.0,98.0')] ).
cnf(522,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_range,u)
| iext(u,uri_rdf_rest,uri_rdf_List) ),
inference(res,[status(thm),theory(equality)],[34,98]),
[iquote('0:Res:34.0,98.0')] ).
cnf(519,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_ex_w,skc6) ),
inference(res,[status(thm),theory(equality)],[3,98]),
[iquote('0:Res:3.0,98.0')] ).
cnf(518,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_ex_A,uri_owl_Class) ),
inference(res,[status(thm),theory(equality)],[9,98]),
[iquote('0:Res:9.0,98.0')] ).
cnf(517,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_ex_B,uri_owl_Class) ),
inference(res,[status(thm),theory(equality)],[10,98]),
[iquote('0:Res:10.0,98.0')] ).
cnf(516,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdf_nil,uri_rdf_List) ),
inference(res,[status(thm),theory(equality)],[12,98]),
[iquote('0:Res:12.0,98.0')] ).
cnf(514,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdf_type,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[21,98]),
[iquote('0:Res:21.0,98.0')] ).
cnf(513,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdf_first,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[11,98]),
[iquote('0:Res:11.0,98.0')] ).
cnf(512,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdf_rest,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[13,98]),
[iquote('0:Res:13.0,98.0')] ).
cnf(511,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdf__1,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[14,98]),
[iquote('0:Res:14.0,98.0')] ).
cnf(510,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdf__2,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[15,98]),
[iquote('0:Res:15.0,98.0')] ).
cnf(509,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdf__3,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[16,98]),
[iquote('0:Res:16.0,98.0')] ).
cnf(508,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdf_object,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[17,98]),
[iquote('0:Res:17.0,98.0')] ).
cnf(507,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdf_value,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[18,98]),
[iquote('0:Res:18.0,98.0')] ).
cnf(506,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdf_subject,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[19,98]),
[iquote('0:Res:19.0,98.0')] ).
cnf(505,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdf__1,uri_rdfs_ContainerMembershipProperty) ),
inference(res,[status(thm),theory(equality)],[46,98]),
[iquote('0:Res:46.0,98.0')] ).
cnf(504,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdf__2,uri_rdfs_ContainerMembershipProperty) ),
inference(res,[status(thm),theory(equality)],[47,98]),
[iquote('0:Res:47.0,98.0')] ).
cnf(503,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdf__3,uri_rdfs_ContainerMembershipProperty) ),
inference(res,[status(thm),theory(equality)],[48,98]),
[iquote('0:Res:48.0,98.0')] ).
cnf(500,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,u)
| iext(u,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[37,98]),
[iquote('0:Res:37.0,98.0')] ).
cnf(499,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,u)
| iext(u,uri_rdf_Alt,uri_rdfs_Container) ),
inference(res,[status(thm),theory(equality)],[35,98]),
[iquote('0:Res:35.0,98.0')] ).
cnf(498,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,u)
| iext(u,uri_rdf_Bag,uri_rdfs_Container) ),
inference(res,[status(thm),theory(equality)],[36,98]),
[iquote('0:Res:36.0,98.0')] ).
cnf(497,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,u)
| iext(u,uri_rdfs_Seq,uri_rdfs_Container) ),
inference(res,[status(thm),theory(equality)],[49,98]),
[iquote('0:Res:49.0,98.0')] ).
cnf(496,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,u)
| iext(u,uri_rdf_XMLLiteral,uri_rdfs_Literal) ),
inference(res,[status(thm),theory(equality)],[50,98]),
[iquote('0:Res:50.0,98.0')] ).
cnf(495,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdf_XMLLiteral,uri_rdfs_Datatype) ),
inference(res,[status(thm),theory(equality)],[51,98]),
[iquote('0:Res:51.0,98.0')] ).
cnf(494,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,u)
| iext(u,uri_rdf_first,uri_rdf_List) ),
inference(res,[status(thm),theory(equality)],[31,98]),
[iquote('0:Res:31.0,98.0')] ).
cnf(493,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,u)
| iext(u,uri_rdf_rest,uri_rdf_List) ),
inference(res,[status(thm),theory(equality)],[33,98]),
[iquote('0:Res:33.0,98.0')] ).
cnf(492,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,u)
| iext(u,uri_rdfs_comment,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[22,98]),
[iquote('0:Res:22.0,98.0')] ).
cnf(491,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,u)
| iext(u,uri_rdfs_isDefinedBy,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[24,98]),
[iquote('0:Res:24.0,98.0')] ).
cnf(490,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,u)
| iext(u,uri_rdfs_label,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[27,98]),
[iquote('0:Res:27.0,98.0')] ).
cnf(489,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,u)
| iext(u,uri_rdfs_seeAlso,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[29,98]),
[iquote('0:Res:29.0,98.0')] ).
cnf(488,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,u)
| iext(u,uri_rdfs_member,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[38,98]),
[iquote('0:Res:38.0,98.0')] ).
cnf(487,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,u)
| iext(u,uri_rdf__1,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[40,98]),
[iquote('0:Res:40.0,98.0')] ).
cnf(486,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,u)
| iext(u,uri_rdf__2,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[41,98]),
[iquote('0:Res:41.0,98.0')] ).
cnf(485,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,u)
| iext(u,uri_rdf__3,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[42,98]),
[iquote('0:Res:42.0,98.0')] ).
cnf(484,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,u)
| iext(u,uri_rdfs_domain,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[53,98]),
[iquote('0:Res:53.0,98.0')] ).
cnf(483,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,u)
| iext(u,uri_rdfs_range,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[56,98]),
[iquote('0:Res:56.0,98.0')] ).
cnf(482,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,u)
| iext(u,uri_rdf_object,uri_rdfs_Statement) ),
inference(res,[status(thm),theory(equality)],[58,98]),
[iquote('0:Res:58.0,98.0')] ).
cnf(481,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,u)
| iext(u,uri_rdf_predicate,uri_rdfs_Statement) ),
inference(res,[status(thm),theory(equality)],[60,98]),
[iquote('0:Res:60.0,98.0')] ).
cnf(480,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,u)
| iext(u,uri_rdf_subject,uri_rdfs_Statement) ),
inference(res,[status(thm),theory(equality)],[62,98]),
[iquote('0:Res:62.0,98.0')] ).
cnf(479,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,u)
| iext(u,uri_rdfs_Datatype,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[52,98]),
[iquote('0:Res:52.0,98.0')] ).
cnf(478,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_range,u)
| iext(u,uri_rdfs_domain,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[54,98]),
[iquote('0:Res:54.0,98.0')] ).
cnf(477,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdf_Property,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[55,98]),
[iquote('0:Res:55.0,98.0')] ).
cnf(476,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,u)
| iext(u,uri_rdfs_subClassOf,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[64,98]),
[iquote('0:Res:64.0,98.0')] ).
cnf(475,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_range,u)
| iext(u,uri_rdfs_subClassOf,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[65,98]),
[iquote('0:Res:65.0,98.0')] ).
cnf(474,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,u)
| iext(u,uri_rdfs_subPropertyOf,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[66,98]),
[iquote('0:Res:66.0,98.0')] ).
cnf(473,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_range,u)
| iext(u,uri_rdfs_subPropertyOf,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[67,98]),
[iquote('0:Res:67.0,98.0')] ).
cnf(472,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,u)
| iext(u,uri_rdf_type,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[68,98]),
[iquote('0:Res:68.0,98.0')] ).
cnf(471,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_range,u)
| iext(u,uri_rdf_type,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[69,98]),
[iquote('0:Res:69.0,98.0')] ).
cnf(470,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_range,u)
| iext(u,uri_rdfs_seeAlso,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[30,98]),
[iquote('0:Res:30.0,98.0')] ).
cnf(469,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_range,u)
| iext(u,uri_rdf_first,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[32,98]),
[iquote('0:Res:32.0,98.0')] ).
cnf(468,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_range,u)
| iext(u,uri_rdfs_member,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[39,98]),
[iquote('0:Res:39.0,98.0')] ).
cnf(467,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_range,u)
| iext(u,uri_rdf__1,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[43,98]),
[iquote('0:Res:43.0,98.0')] ).
cnf(466,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_range,u)
| iext(u,uri_rdf__2,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[44,98]),
[iquote('0:Res:44.0,98.0')] ).
cnf(465,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_range,u)
| iext(u,uri_rdf__3,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[45,98]),
[iquote('0:Res:45.0,98.0')] ).
cnf(464,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_range,u)
| iext(u,uri_rdf_predicate,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[61,98]),
[iquote('0:Res:61.0,98.0')] ).
cnf(463,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_range,u)
| iext(u,uri_rdf_subject,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[63,98]),
[iquote('0:Res:63.0,98.0')] ).
cnf(462,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,u)
| iext(u,uri_rdf_value,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[70,98]),
[iquote('0:Res:70.0,98.0')] ).
cnf(450,plain,
( ~ iext(uri_rdfs_subPropertyOf,u,uri_rdf__1)
| iext(uri_rdfs_subPropertyOf,u,uri_rdfs_member) ),
inference(res,[status(thm),theory(equality)],[266,99]),
[iquote('0:Res:266.0,99.0')] ).
cnf(461,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_range,u)
| iext(u,uri_rdf_value,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[71,98]),
[iquote('0:Res:71.0,98.0')] ).
cnf(444,plain,
( ~ iext(uri_rdfs_subPropertyOf,u,uri_rdf__2)
| iext(uri_rdfs_subPropertyOf,u,uri_rdfs_member) ),
inference(res,[status(thm),theory(equality)],[256,99]),
[iquote('0:Res:256.0,99.0')] ).
cnf(440,plain,
( ~ iext(uri_rdfs_subClassOf,u,uri_rdfs_ContainerMembershipProperty)
| iext(uri_rdfs_subClassOf,u,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[37,97]),
[iquote('0:Res:37.0,97.0')] ).
cnf(439,plain,
( ~ iext(uri_rdfs_subClassOf,u,uri_rdf_Alt)
| iext(uri_rdfs_subClassOf,u,uri_rdfs_Container) ),
inference(res,[status(thm),theory(equality)],[35,97]),
[iquote('0:Res:35.0,97.0')] ).
cnf(438,plain,
( ~ iext(uri_rdfs_subClassOf,u,uri_rdf_Bag)
| iext(uri_rdfs_subClassOf,u,uri_rdfs_Container) ),
inference(res,[status(thm),theory(equality)],[36,97]),
[iquote('0:Res:36.0,97.0')] ).
cnf(437,plain,
( ~ iext(uri_rdfs_subClassOf,u,uri_rdfs_Seq)
| iext(uri_rdfs_subClassOf,u,uri_rdfs_Container) ),
inference(res,[status(thm),theory(equality)],[49,97]),
[iquote('0:Res:49.0,97.0')] ).
cnf(436,plain,
( ~ iext(uri_rdfs_subClassOf,u,uri_rdf_XMLLiteral)
| iext(uri_rdfs_subClassOf,u,uri_rdfs_Literal) ),
inference(res,[status(thm),theory(equality)],[50,97]),
[iquote('0:Res:50.0,97.0')] ).
cnf(435,plain,
( ~ iext(uri_rdfs_subClassOf,u,uri_rdfs_Datatype)
| iext(uri_rdfs_subClassOf,u,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[52,97]),
[iquote('0:Res:52.0,97.0')] ).
cnf(429,plain,
( ~ iext(uri_rdfs_subPropertyOf,u,uri_rdf__3)
| iext(uri_rdfs_subPropertyOf,u,uri_rdfs_member) ),
inference(res,[status(thm),theory(equality)],[254,99]),
[iquote('0:Res:254.0,99.0')] ).
cnf(407,plain,
( ~ iext(uri_rdfs_domain,uri_rdf_type,u)
| icext(u,v) ),
inference(res,[status(thm),theory(equality)],[226,95]),
[iquote('0:Res:226.0,95.0')] ).
cnf(425,plain,
( ~ iext(uri_rdfs_subPropertyOf,u,uri_rdfs_isDefinedBy)
| iext(uri_rdfs_subPropertyOf,u,uri_rdfs_seeAlso) ),
inference(res,[status(thm),theory(equality)],[26,99]),
[iquote('0:Res:26.0,99.0')] ).
cnf(453,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,u)
| icext(u,uri_rdf__1) ),
inference(res,[status(thm),theory(equality)],[266,95]),
[iquote('0:Res:266.0,95.0')] ).
cnf(447,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,u)
| icext(u,uri_rdf__2) ),
inference(res,[status(thm),theory(equality)],[256,95]),
[iquote('0:Res:256.0,95.0')] ).
cnf(433,plain,
( ~ iext(uri_rdfs_range,uri_rdfs_subPropertyOf,u)
| icext(u,uri_rdfs_member) ),
inference(res,[status(thm),theory(equality)],[254,96]),
[iquote('0:Res:254.0,96.0')] ).
cnf(432,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,u)
| icext(u,uri_rdf__3) ),
inference(res,[status(thm),theory(equality)],[254,95]),
[iquote('0:Res:254.0,95.0')] ).
cnf(420,plain,
( ~ iext(uri_rdfs_domain,uri_owl_complementOf,u)
| icext(u,skc7) ),
inference(res,[status(thm),theory(equality)],[2,95]),
[iquote('0:Res:2.0,95.0')] ).
cnf(419,plain,
( ~ iext(uri_rdfs_domain,uri_rdf_first,u)
| icext(u,skc5) ),
inference(res,[status(thm),theory(equality)],[4,95]),
[iquote('0:Res:4.0,95.0')] ).
cnf(795,plain,
iext(uri_rdf_type,skc5,uri_rdf_List),
inference(res,[status(thm),theory(equality)],[794,91]),
[iquote('0:Res:794.0,91.0')] ).
cnf(794,plain,
icext(uri_rdf_List,skc5),
inference(res,[status(thm),theory(equality)],[33,418]),
[iquote('0:Res:33.0,418.0')] ).
cnf(418,plain,
( ~ iext(uri_rdfs_domain,uri_rdf_rest,u)
| icext(u,skc5) ),
inference(res,[status(thm),theory(equality)],[5,95]),
[iquote('0:Res:5.0,95.0')] ).
cnf(417,plain,
( ~ iext(uri_rdfs_domain,uri_owl_intersectionOf,u)
| icext(u,skc6) ),
inference(res,[status(thm),theory(equality)],[6,95]),
[iquote('0:Res:6.0,95.0')] ).
cnf(416,plain,
( ~ iext(uri_rdfs_domain,uri_rdf_rest,u)
| icext(u,skc4) ),
inference(res,[status(thm),theory(equality)],[7,95]),
[iquote('0:Res:7.0,95.0')] ).
cnf(415,plain,
( ~ iext(uri_rdfs_domain,uri_rdf_first,u)
| icext(u,skc4) ),
inference(res,[status(thm),theory(equality)],[8,95]),
[iquote('0:Res:8.0,95.0')] ).
cnf(413,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,u)
| icext(u,uri_rdfs_isDefinedBy) ),
inference(res,[status(thm),theory(equality)],[26,95]),
[iquote('0:Res:26.0,95.0')] ).
cnf(412,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_range,u)
| icext(u,uri_rdfs_range) ),
inference(res,[status(thm),theory(equality)],[57,95]),
[iquote('0:Res:57.0,95.0')] ).
cnf(411,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_range,u)
| icext(u,uri_rdfs_isDefinedBy) ),
inference(res,[status(thm),theory(equality)],[25,95]),
[iquote('0:Res:25.0,95.0')] ).
cnf(410,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_range,u)
| icext(u,uri_rdfs_comment) ),
inference(res,[status(thm),theory(equality)],[23,95]),
[iquote('0:Res:23.0,95.0')] ).
cnf(409,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_range,u)
| icext(u,uri_rdfs_label) ),
inference(res,[status(thm),theory(equality)],[28,95]),
[iquote('0:Res:28.0,95.0')] ).
cnf(408,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_range,u)
| icext(u,uri_rdf_rest) ),
inference(res,[status(thm),theory(equality)],[34,95]),
[iquote('0:Res:34.0,95.0')] ).
cnf(779,plain,
iext(uri_rdf_type,uri_rdf_Alt,uri_rdfs_Class),
inference(res,[status(thm),theory(equality)],[777,91]),
[iquote('0:Res:777.0,91.0')] ).
cnf(387,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_subClassOf,u)
| icext(u,uri_rdfs_ContainerMembershipProperty) ),
inference(res,[status(thm),theory(equality)],[37,95]),
[iquote('0:Res:37.0,95.0')] ).
cnf(777,plain,
icext(uri_rdfs_Class,uri_rdf_Alt),
inference(res,[status(thm),theory(equality)],[64,386]),
[iquote('0:Res:64.0,386.0')] ).
cnf(386,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_subClassOf,u)
| icext(u,uri_rdf_Alt) ),
inference(res,[status(thm),theory(equality)],[35,95]),
[iquote('0:Res:35.0,95.0')] ).
cnf(771,plain,
iext(uri_rdf_type,uri_rdf_Bag,uri_rdfs_Class),
inference(res,[status(thm),theory(equality)],[769,91]),
[iquote('0:Res:769.0,91.0')] ).
cnf(769,plain,
icext(uri_rdfs_Class,uri_rdf_Bag),
inference(res,[status(thm),theory(equality)],[64,385]),
[iquote('0:Res:64.0,385.0')] ).
cnf(385,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_subClassOf,u)
| icext(u,uri_rdf_Bag) ),
inference(res,[status(thm),theory(equality)],[36,95]),
[iquote('0:Res:36.0,95.0')] ).
cnf(763,plain,
iext(uri_rdf_type,uri_rdfs_Seq,uri_rdfs_Class),
inference(res,[status(thm),theory(equality)],[761,91]),
[iquote('0:Res:761.0,91.0')] ).
cnf(761,plain,
icext(uri_rdfs_Class,uri_rdfs_Seq),
inference(res,[status(thm),theory(equality)],[64,384]),
[iquote('0:Res:64.0,384.0')] ).
cnf(384,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_subClassOf,u)
| icext(u,uri_rdfs_Seq) ),
inference(res,[status(thm),theory(equality)],[49,95]),
[iquote('0:Res:49.0,95.0')] ).
cnf(383,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_subClassOf,u)
| icext(u,uri_rdf_XMLLiteral) ),
inference(res,[status(thm),theory(equality)],[50,95]),
[iquote('0:Res:50.0,95.0')] ).
cnf(381,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_domain,u)
| icext(u,uri_rdf_first) ),
inference(res,[status(thm),theory(equality)],[31,95]),
[iquote('0:Res:31.0,95.0')] ).
cnf(380,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_domain,u)
| icext(u,uri_rdf_rest) ),
inference(res,[status(thm),theory(equality)],[33,95]),
[iquote('0:Res:33.0,95.0')] ).
cnf(752,plain,
ip(uri_rdfs_comment),
inference(res,[status(thm),theory(equality)],[751,81]),
[iquote('0:Res:751.0,81.0')] ).
cnf(751,plain,
iext(uri_rdf_type,uri_rdfs_comment,uri_rdf_Property),
inference(res,[status(thm),theory(equality)],[750,91]),
[iquote('0:Res:750.0,91.0')] ).
cnf(750,plain,
icext(uri_rdf_Property,uri_rdfs_comment),
inference(res,[status(thm),theory(equality)],[53,379]),
[iquote('0:Res:53.0,379.0')] ).
cnf(379,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_domain,u)
| icext(u,uri_rdfs_comment) ),
inference(res,[status(thm),theory(equality)],[22,95]),
[iquote('0:Res:22.0,95.0')] ).
cnf(737,plain,
iext(uri_rdf_type,uri_rdfs_isDefinedBy,uri_rdf_Property),
inference(res,[status(thm),theory(equality)],[736,91]),
[iquote('0:Res:736.0,91.0')] ).
cnf(738,plain,
ip(uri_rdfs_label),
inference(res,[status(thm),theory(equality)],[735,81]),
[iquote('0:Res:735.0,81.0')] ).
cnf(735,plain,
iext(uri_rdf_type,uri_rdfs_label,uri_rdf_Property),
inference(res,[status(thm),theory(equality)],[734,91]),
[iquote('0:Res:734.0,91.0')] ).
cnf(736,plain,
icext(uri_rdf_Property,uri_rdfs_isDefinedBy),
inference(res,[status(thm),theory(equality)],[53,378]),
[iquote('0:Res:53.0,378.0')] ).
cnf(378,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_domain,u)
| icext(u,uri_rdfs_isDefinedBy) ),
inference(res,[status(thm),theory(equality)],[24,95]),
[iquote('0:Res:24.0,95.0')] ).
cnf(734,plain,
icext(uri_rdf_Property,uri_rdfs_label),
inference(res,[status(thm),theory(equality)],[53,377]),
[iquote('0:Res:53.0,377.0')] ).
cnf(377,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_domain,u)
| icext(u,uri_rdfs_label) ),
inference(res,[status(thm),theory(equality)],[27,95]),
[iquote('0:Res:27.0,95.0')] ).
cnf(376,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_domain,u)
| icext(u,uri_rdfs_seeAlso) ),
inference(res,[status(thm),theory(equality)],[29,95]),
[iquote('0:Res:29.0,95.0')] ).
cnf(375,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_domain,u)
| icext(u,uri_rdfs_member) ),
inference(res,[status(thm),theory(equality)],[38,95]),
[iquote('0:Res:38.0,95.0')] ).
cnf(374,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_domain,u)
| icext(u,uri_rdf__1) ),
inference(res,[status(thm),theory(equality)],[40,95]),
[iquote('0:Res:40.0,95.0')] ).
cnf(373,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_domain,u)
| icext(u,uri_rdf__2) ),
inference(res,[status(thm),theory(equality)],[41,95]),
[iquote('0:Res:41.0,95.0')] ).
cnf(372,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_domain,u)
| icext(u,uri_rdf__3) ),
inference(res,[status(thm),theory(equality)],[42,95]),
[iquote('0:Res:42.0,95.0')] ).
cnf(722,plain,
iext(uri_rdf_type,uri_rdfs_range,uri_rdf_Property),
inference(res,[status(thm),theory(equality)],[720,91]),
[iquote('0:Res:720.0,91.0')] ).
cnf(720,plain,
icext(uri_rdf_Property,uri_rdfs_range),
inference(res,[status(thm),theory(equality)],[53,370]),
[iquote('0:Res:53.0,370.0')] ).
cnf(371,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_domain,u)
| icext(u,uri_rdfs_domain) ),
inference(res,[status(thm),theory(equality)],[53,95]),
[iquote('0:Res:53.0,95.0')] ).
cnf(370,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_domain,u)
| icext(u,uri_rdfs_range) ),
inference(res,[status(thm),theory(equality)],[56,95]),
[iquote('0:Res:56.0,95.0')] ).
cnf(369,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_domain,u)
| icext(u,uri_rdf_object) ),
inference(res,[status(thm),theory(equality)],[58,95]),
[iquote('0:Res:58.0,95.0')] ).
cnf(368,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_domain,u)
| icext(u,uri_rdf_predicate) ),
inference(res,[status(thm),theory(equality)],[60,95]),
[iquote('0:Res:60.0,95.0')] ).
cnf(367,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_domain,u)
| icext(u,uri_rdf_subject) ),
inference(res,[status(thm),theory(equality)],[62,95]),
[iquote('0:Res:62.0,95.0')] ).
cnf(366,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_subClassOf,u)
| icext(u,uri_rdfs_Datatype) ),
inference(res,[status(thm),theory(equality)],[52,95]),
[iquote('0:Res:52.0,95.0')] ).
cnf(709,plain,
iext(uri_rdf_type,uri_rdfs_domain,uri_rdf_Property),
inference(res,[status(thm),theory(equality)],[708,91]),
[iquote('0:Res:708.0,91.0')] ).
cnf(708,plain,
icext(uri_rdf_Property,uri_rdfs_domain),
inference(res,[status(thm),theory(equality)],[56,365]),
[iquote('0:Res:56.0,365.0')] ).
cnf(365,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_range,u)
| icext(u,uri_rdfs_domain) ),
inference(res,[status(thm),theory(equality)],[54,95]),
[iquote('0:Res:54.0,95.0')] ).
cnf(700,plain,
iext(uri_rdf_type,uri_rdfs_subClassOf,uri_rdf_Property),
inference(res,[status(thm),theory(equality)],[699,91]),
[iquote('0:Res:699.0,91.0')] ).
cnf(363,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_domain,u)
| icext(u,uri_rdfs_subClassOf) ),
inference(res,[status(thm),theory(equality)],[64,95]),
[iquote('0:Res:64.0,95.0')] ).
cnf(699,plain,
icext(uri_rdf_Property,uri_rdfs_subClassOf),
inference(res,[status(thm),theory(equality)],[56,362]),
[iquote('0:Res:56.0,362.0')] ).
cnf(362,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_range,u)
| icext(u,uri_rdfs_subClassOf) ),
inference(res,[status(thm),theory(equality)],[65,95]),
[iquote('0:Res:65.0,95.0')] ).
cnf(692,plain,
iext(uri_rdf_type,uri_rdfs_subPropertyOf,uri_rdf_Property),
inference(res,[status(thm),theory(equality)],[690,91]),
[iquote('0:Res:690.0,91.0')] ).
cnf(690,plain,
icext(uri_rdf_Property,uri_rdfs_subPropertyOf),
inference(res,[status(thm),theory(equality)],[56,360]),
[iquote('0:Res:56.0,360.0')] ).
cnf(361,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_domain,u)
| icext(u,uri_rdfs_subPropertyOf) ),
inference(res,[status(thm),theory(equality)],[66,95]),
[iquote('0:Res:66.0,95.0')] ).
cnf(360,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_range,u)
| icext(u,uri_rdfs_subPropertyOf) ),
inference(res,[status(thm),theory(equality)],[67,95]),
[iquote('0:Res:67.0,95.0')] ).
cnf(359,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_domain,u)
| icext(u,uri_rdf_type) ),
inference(res,[status(thm),theory(equality)],[68,95]),
[iquote('0:Res:68.0,95.0')] ).
cnf(358,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_range,u)
| icext(u,uri_rdf_type) ),
inference(res,[status(thm),theory(equality)],[69,95]),
[iquote('0:Res:69.0,95.0')] ).
cnf(357,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_range,u)
| icext(u,uri_rdfs_seeAlso) ),
inference(res,[status(thm),theory(equality)],[30,95]),
[iquote('0:Res:30.0,95.0')] ).
cnf(356,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_range,u)
| icext(u,uri_rdf_first) ),
inference(res,[status(thm),theory(equality)],[32,95]),
[iquote('0:Res:32.0,95.0')] ).
cnf(679,plain,
iext(uri_rdf_type,uri_rdfs_member,uri_rdf_Property),
inference(res,[status(thm),theory(equality)],[678,91]),
[iquote('0:Res:678.0,91.0')] ).
cnf(678,plain,
icext(uri_rdf_Property,uri_rdfs_member),
inference(res,[status(thm),theory(equality)],[56,355]),
[iquote('0:Res:56.0,355.0')] ).
cnf(355,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_range,u)
| icext(u,uri_rdfs_member) ),
inference(res,[status(thm),theory(equality)],[39,95]),
[iquote('0:Res:39.0,95.0')] ).
cnf(354,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_range,u)
| icext(u,uri_rdf__1) ),
inference(res,[status(thm),theory(equality)],[43,95]),
[iquote('0:Res:43.0,95.0')] ).
cnf(353,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_range,u)
| icext(u,uri_rdf__2) ),
inference(res,[status(thm),theory(equality)],[44,95]),
[iquote('0:Res:44.0,95.0')] ).
cnf(352,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_range,u)
| icext(u,uri_rdf__3) ),
inference(res,[status(thm),theory(equality)],[45,95]),
[iquote('0:Res:45.0,95.0')] ).
cnf(669,plain,
ip(uri_rdf_predicate),
inference(res,[status(thm),theory(equality)],[668,81]),
[iquote('0:Res:668.0,81.0')] ).
cnf(668,plain,
iext(uri_rdf_type,uri_rdf_predicate,uri_rdf_Property),
inference(res,[status(thm),theory(equality)],[667,91]),
[iquote('0:Res:667.0,91.0')] ).
cnf(667,plain,
icext(uri_rdf_Property,uri_rdf_predicate),
inference(res,[status(thm),theory(equality)],[56,351]),
[iquote('0:Res:56.0,351.0')] ).
cnf(351,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_range,u)
| icext(u,uri_rdf_predicate) ),
inference(res,[status(thm),theory(equality)],[61,95]),
[iquote('0:Res:61.0,95.0')] ).
cnf(350,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_range,u)
| icext(u,uri_rdf_subject) ),
inference(res,[status(thm),theory(equality)],[63,95]),
[iquote('0:Res:63.0,95.0')] ).
cnf(349,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_domain,u)
| icext(u,uri_rdf_value) ),
inference(res,[status(thm),theory(equality)],[70,95]),
[iquote('0:Res:70.0,95.0')] ).
cnf(348,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_range,u)
| icext(u,uri_rdf_value) ),
inference(res,[status(thm),theory(equality)],[71,95]),
[iquote('0:Res:71.0,95.0')] ).
cnf(343,plain,
( ~ iext(uri_rdfs_range,uri_owl_complementOf,u)
| icext(u,uri_ex_A) ),
inference(res,[status(thm),theory(equality)],[2,96]),
[iquote('0:Res:2.0,96.0')] ).
cnf(342,plain,
( ~ iext(uri_rdfs_range,uri_rdf_first,u)
| icext(u,uri_ex_A) ),
inference(res,[status(thm),theory(equality)],[4,96]),
[iquote('0:Res:4.0,96.0')] ).
cnf(657,plain,
iext(uri_rdf_type,skc4,uri_rdf_List),
inference(res,[status(thm),theory(equality)],[656,91]),
[iquote('0:Res:656.0,91.0')] ).
cnf(656,plain,
icext(uri_rdf_List,skc4),
inference(res,[status(thm),theory(equality)],[34,341]),
[iquote('0:Res:34.0,341.0')] ).
cnf(341,plain,
( ~ iext(uri_rdfs_range,uri_rdf_rest,u)
| icext(u,skc4) ),
inference(res,[status(thm),theory(equality)],[5,96]),
[iquote('0:Res:5.0,96.0')] ).
cnf(340,plain,
( ~ iext(uri_rdfs_range,uri_owl_intersectionOf,u)
| icext(u,skc5) ),
inference(res,[status(thm),theory(equality)],[6,96]),
[iquote('0:Res:6.0,96.0')] ).
cnf(339,plain,
( ~ iext(uri_rdfs_range,uri_rdf_rest,u)
| icext(u,uri_rdf_nil) ),
inference(res,[status(thm),theory(equality)],[7,96]),
[iquote('0:Res:7.0,96.0')] ).
cnf(338,plain,
( ~ iext(uri_rdfs_range,uri_rdf_first,u)
| icext(u,skc7) ),
inference(res,[status(thm),theory(equality)],[8,96]),
[iquote('0:Res:8.0,96.0')] ).
cnf(647,plain,
iext(uri_rdf_type,uri_rdfs_seeAlso,uri_rdf_Property),
inference(res,[status(thm),theory(equality)],[646,91]),
[iquote('0:Res:646.0,91.0')] ).
cnf(646,plain,
icext(uri_rdf_Property,uri_rdfs_seeAlso),
inference(res,[status(thm),theory(equality)],[67,336]),
[iquote('0:Res:67.0,336.0')] ).
cnf(336,plain,
( ~ iext(uri_rdfs_range,uri_rdfs_subPropertyOf,u)
| icext(u,uri_rdfs_seeAlso) ),
inference(res,[status(thm),theory(equality)],[26,96]),
[iquote('0:Res:26.0,96.0')] ).
cnf(332,plain,
( ~ iext(uri_rdfs_range,uri_rdfs_range,u)
| icext(u,uri_rdfs_Literal) ),
inference(res,[status(thm),theory(equality)],[28,96]),
[iquote('0:Res:28.0,96.0')] ).
cnf(330,plain,
( ~ iext(uri_rdfs_range,uri_rdf_type,u)
| icext(u,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[226,96]),
[iquote('0:Res:226.0,96.0')] ).
cnf(638,plain,
iext(uri_rdf_type,skc6,uri_rdfs_Class),
inference(res,[status(thm),theory(equality)],[635,91]),
[iquote('0:Res:635.0,91.0')] ).
cnf(637,plain,
ic(skc6),
inference(res,[status(thm),theory(equality)],[635,75]),
[iquote('0:Res:635.0,75.0')] ).
cnf(635,plain,
icext(uri_rdfs_Class,skc6),
inference(res,[status(thm),theory(equality)],[69,329]),
[iquote('0:Res:69.0,329.0')] ).
cnf(331,plain,
( ~ iext(uri_rdfs_range,uri_rdfs_range,u)
| icext(u,uri_rdf_List) ),
inference(res,[status(thm),theory(equality)],[34,96]),
[iquote('0:Res:34.0,96.0')] ).
cnf(329,plain,
( ~ iext(uri_rdfs_range,uri_rdf_type,u)
| icext(u,skc6) ),
inference(res,[status(thm),theory(equality)],[3,96]),
[iquote('0:Res:3.0,96.0')] ).
cnf(629,plain,
iext(uri_rdf_type,uri_owl_Class,uri_rdfs_Class),
inference(res,[status(thm),theory(equality)],[627,91]),
[iquote('0:Res:627.0,91.0')] ).
cnf(628,plain,
ic(uri_owl_Class),
inference(res,[status(thm),theory(equality)],[627,75]),
[iquote('0:Res:627.0,75.0')] ).
cnf(627,plain,
icext(uri_rdfs_Class,uri_owl_Class),
inference(res,[status(thm),theory(equality)],[69,327]),
[iquote('0:Res:69.0,327.0')] ).
cnf(327,plain,
( ~ iext(uri_rdfs_range,uri_rdf_type,u)
| icext(u,uri_owl_Class) ),
inference(res,[status(thm),theory(equality)],[10,96]),
[iquote('0:Res:10.0,96.0')] ).
cnf(326,plain,
( ~ iext(uri_rdfs_range,uri_rdf_type,u)
| icext(u,uri_rdf_List) ),
inference(res,[status(thm),theory(equality)],[12,96]),
[iquote('0:Res:12.0,96.0')] ).
cnf(316,plain,
( ~ iext(uri_rdfs_range,uri_rdf_type,u)
| icext(u,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[19,96]),
[iquote('0:Res:19.0,96.0')] ).
cnf(619,plain,
iext(uri_rdf_type,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Class),
inference(res,[status(thm),theory(equality)],[617,91]),
[iquote('0:Res:617.0,91.0')] ).
cnf(617,plain,
icext(uri_rdfs_Class,uri_rdfs_ContainerMembershipProperty),
inference(res,[status(thm),theory(equality)],[69,313]),
[iquote('0:Res:69.0,313.0')] ).
cnf(313,plain,
( ~ iext(uri_rdfs_range,uri_rdf_type,u)
| icext(u,uri_rdfs_ContainerMembershipProperty) ),
inference(res,[status(thm),theory(equality)],[48,96]),
[iquote('0:Res:48.0,96.0')] ).
cnf(310,plain,
( ~ iext(uri_rdfs_range,uri_rdfs_subClassOf,u)
| icext(u,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[37,96]),
[iquote('0:Res:37.0,96.0')] ).
cnf(605,plain,
iext(uri_rdf_type,uri_rdfs_Container,uri_rdfs_Class),
inference(res,[status(thm),theory(equality)],[603,91]),
[iquote('0:Res:603.0,91.0')] ).
cnf(602,plain,
iext(uri_rdf_type,uri_rdfs_Literal,uri_rdfs_Class),
inference(res,[status(thm),theory(equality)],[600,91]),
[iquote('0:Res:600.0,91.0')] ).
cnf(603,plain,
icext(uri_rdfs_Class,uri_rdfs_Container),
inference(res,[status(thm),theory(equality)],[65,307]),
[iquote('0:Res:65.0,307.0')] ).
cnf(307,plain,
( ~ iext(uri_rdfs_range,uri_rdfs_subClassOf,u)
| icext(u,uri_rdfs_Container) ),
inference(res,[status(thm),theory(equality)],[49,96]),
[iquote('0:Res:49.0,96.0')] ).
cnf(600,plain,
icext(uri_rdfs_Class,uri_rdfs_Literal),
inference(res,[status(thm),theory(equality)],[65,306]),
[iquote('0:Res:65.0,306.0')] ).
cnf(306,plain,
( ~ iext(uri_rdfs_range,uri_rdfs_subClassOf,u)
| icext(u,uri_rdfs_Literal) ),
inference(res,[status(thm),theory(equality)],[50,96]),
[iquote('0:Res:50.0,96.0')] ).
cnf(594,plain,
iext(uri_rdf_type,uri_rdfs_Datatype,uri_rdfs_Class),
inference(res,[status(thm),theory(equality)],[592,91]),
[iquote('0:Res:592.0,91.0')] ).
cnf(592,plain,
icext(uri_rdfs_Class,uri_rdfs_Datatype),
inference(res,[status(thm),theory(equality)],[69,305]),
[iquote('0:Res:69.0,305.0')] ).
cnf(305,plain,
( ~ iext(uri_rdfs_range,uri_rdf_type,u)
| icext(u,uri_rdfs_Datatype) ),
inference(res,[status(thm),theory(equality)],[51,96]),
[iquote('0:Res:51.0,96.0')] ).
cnf(581,plain,
iext(uri_rdf_type,uri_rdf_List,uri_rdfs_Class),
inference(res,[status(thm),theory(equality)],[579,91]),
[iquote('0:Res:579.0,91.0')] ).
cnf(578,plain,
iext(uri_rdf_type,uri_rdfs_Statement,uri_rdfs_Class),
inference(res,[status(thm),theory(equality)],[576,91]),
[iquote('0:Res:576.0,91.0')] ).
cnf(580,plain,
ic(uri_rdf_List),
inference(res,[status(thm),theory(equality)],[579,75]),
[iquote('0:Res:579.0,75.0')] ).
cnf(579,plain,
icext(uri_rdfs_Class,uri_rdf_List),
inference(res,[status(thm),theory(equality)],[54,303]),
[iquote('0:Res:54.0,303.0')] ).
cnf(303,plain,
( ~ iext(uri_rdfs_range,uri_rdfs_domain,u)
| icext(u,uri_rdf_List) ),
inference(res,[status(thm),theory(equality)],[33,96]),
[iquote('0:Res:33.0,96.0')] ).
cnf(577,plain,
ic(uri_rdfs_Statement),
inference(res,[status(thm),theory(equality)],[576,75]),
[iquote('0:Res:576.0,75.0')] ).
cnf(576,plain,
icext(uri_rdfs_Class,uri_rdfs_Statement),
inference(res,[status(thm),theory(equality)],[54,290]),
[iquote('0:Res:54.0,290.0')] ).
cnf(290,plain,
( ~ iext(uri_rdfs_range,uri_rdfs_domain,u)
| icext(u,uri_rdfs_Statement) ),
inference(res,[status(thm),theory(equality)],[62,96]),
[iquote('0:Res:62.0,96.0')] ).
cnf(289,plain,
( ~ iext(uri_rdfs_range,uri_rdfs_subClassOf,u)
| icext(u,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[52,96]),
[iquote('0:Res:52.0,96.0')] ).
cnf(287,plain,
( ~ iext(uri_rdfs_range,uri_rdf_type,u)
| icext(u,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[55,96]),
[iquote('0:Res:55.0,96.0')] ).
cnf(286,plain,
( ~ iext(uri_rdfs_range,uri_rdfs_domain,u)
| icext(u,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[64,96]),
[iquote('0:Res:64.0,96.0')] ).
cnf(284,plain,
( ~ iext(uri_rdfs_range,uri_rdfs_domain,u)
| icext(u,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[66,96]),
[iquote('0:Res:66.0,96.0')] ).
cnf(566,plain,
iext(uri_rdf_type,uri_rdfs_Class,uri_rdfs_Class),
inference(res,[status(thm),theory(equality)],[563,91]),
[iquote('0:Res:563.0,91.0')] ).
cnf(563,plain,
icext(uri_rdfs_Class,uri_rdfs_Class),
inference(res,[status(thm),theory(equality)],[57,281]),
[iquote('0:Res:57.0,281.0')] ).
cnf(283,plain,
( ~ iext(uri_rdfs_range,uri_rdfs_range,u)
| icext(u,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[67,96]),
[iquote('0:Res:67.0,96.0')] ).
cnf(281,plain,
( ~ iext(uri_rdfs_range,uri_rdfs_range,u)
| icext(u,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[69,96]),
[iquote('0:Res:69.0,96.0')] ).
cnf(272,plain,
( ~ iext(uri_rdfs_range,uri_rdfs_domain,u)
| icext(u,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[70,96]),
[iquote('0:Res:70.0,96.0')] ).
cnf(556,plain,
iext(uri_rdf_type,uri_rdfs_Resource,uri_rdfs_Class),
inference(res,[status(thm),theory(equality)],[554,91]),
[iquote('0:Res:554.0,91.0')] ).
cnf(554,plain,
icext(uri_rdfs_Class,uri_rdfs_Resource),
inference(res,[status(thm),theory(equality)],[57,271]),
[iquote('0:Res:57.0,271.0')] ).
cnf(271,plain,
( ~ iext(uri_rdfs_range,uri_rdfs_range,u)
| icext(u,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[71,96]),
[iquote('0:Res:71.0,96.0')] ).
cnf(263,plain,
( ~ icext(uri_rdfs_ContainerMembershipProperty,u)
| icext(uri_rdf_Property,u) ),
inference(res,[status(thm),theory(equality)],[37,94]),
[iquote('0:Res:37.0,94.1')] ).
cnf(262,plain,
( ~ icext(uri_rdf_Alt,u)
| icext(uri_rdfs_Container,u) ),
inference(res,[status(thm),theory(equality)],[35,94]),
[iquote('0:Res:35.0,94.1')] ).
cnf(261,plain,
( ~ icext(uri_rdf_Bag,u)
| icext(uri_rdfs_Container,u) ),
inference(res,[status(thm),theory(equality)],[36,94]),
[iquote('0:Res:36.0,94.1')] ).
cnf(260,plain,
( ~ icext(uri_rdfs_Seq,u)
| icext(uri_rdfs_Container,u) ),
inference(res,[status(thm),theory(equality)],[49,94]),
[iquote('0:Res:49.0,94.1')] ).
cnf(259,plain,
( ~ icext(uri_rdf_XMLLiteral,u)
| icext(uri_rdfs_Literal,u) ),
inference(res,[status(thm),theory(equality)],[50,94]),
[iquote('0:Res:50.0,94.1')] ).
cnf(545,plain,
iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Class),
inference(res,[status(thm),theory(equality)],[543,91]),
[iquote('0:Res:543.0,91.0')] ).
cnf(543,plain,
icext(uri_rdfs_Class,uri_rdf_XMLLiteral),
inference(res,[status(thm),theory(equality)],[231,258]),
[iquote('0:Res:231.0,258.0')] ).
cnf(258,plain,
( ~ icext(uri_rdfs_Datatype,u)
| icext(uri_rdfs_Class,u) ),
inference(res,[status(thm),theory(equality)],[52,94]),
[iquote('0:Res:52.0,94.1')] ).
cnf(228,plain,
( ~ ic(u)
| iext(uri_rdf_type,u,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[74,91]),
[iquote('0:Res:74.1,91.0')] ).
cnf(98,axiom,
( ~ iext(u,v,w)
| ~ iext(uri_rdfs_subPropertyOf,u,x)
| iext(x,v,w) ),
file('SWB029+4.p',unknown),
[] ).
cnf(227,plain,
( ~ lv(u)
| iext(uri_rdf_type,u,uri_rdfs_Literal) ),
inference(res,[status(thm),theory(equality)],[78,91]),
[iquote('0:Res:78.1,91.0')] ).
cnf(244,plain,
( ~ ip(u)
| icext(uri_rdf_Property,u) ),
inference(res,[status(thm),theory(equality)],[82,90]),
[iquote('0:Res:82.1,90.0')] ).
cnf(266,plain,
iext(uri_rdfs_subPropertyOf,uri_rdf__1,uri_rdfs_member),
inference(res,[status(thm),theory(equality)],[234,92]),
[iquote('0:Res:234.0,92.0')] ).
cnf(256,plain,
iext(uri_rdfs_subPropertyOf,uri_rdf__2,uri_rdfs_member),
inference(res,[status(thm),theory(equality)],[233,92]),
[iquote('0:Res:233.0,92.0')] ).
cnf(97,axiom,
( ~ iext(uri_rdfs_subClassOf,u,v)
| ~ iext(uri_rdfs_subClassOf,w,u)
| iext(uri_rdfs_subClassOf,w,v) ),
file('SWB029+4.p',unknown),
[] ).
cnf(431,plain,
ip(uri_rdfs_member),
inference(res,[status(thm),theory(equality)],[254,88]),
[iquote('0:Res:254.0,88.0')] ).
cnf(254,plain,
iext(uri_rdfs_subPropertyOf,uri_rdf__3,uri_rdfs_member),
inference(res,[status(thm),theory(equality)],[232,92]),
[iquote('0:Res:232.0,92.0')] ).
cnf(248,plain,
icext(skc6,uri_ex_w),
inference(res,[status(thm),theory(equality)],[3,90]),
[iquote('0:Res:3.0,90.0')] ).
cnf(247,plain,
icext(uri_owl_Class,uri_ex_A),
inference(res,[status(thm),theory(equality)],[9,90]),
[iquote('0:Res:9.0,90.0')] ).
cnf(99,axiom,
( ~ iext(uri_rdfs_subPropertyOf,u,v)
| ~ iext(uri_rdfs_subPropertyOf,w,u)
| iext(uri_rdfs_subPropertyOf,w,v) ),
file('SWB029+4.p',unknown),
[] ).
cnf(246,plain,
icext(uri_owl_Class,uri_ex_B),
inference(res,[status(thm),theory(equality)],[10,90]),
[iquote('0:Res:10.0,90.0')] ).
cnf(245,plain,
icext(uri_rdf_List,uri_rdf_nil),
inference(res,[status(thm),theory(equality)],[12,90]),
[iquote('0:Res:12.0,90.0')] ).
cnf(243,plain,
icext(uri_rdf_Property,uri_rdf_type),
inference(res,[status(thm),theory(equality)],[21,90]),
[iquote('0:Res:21.0,90.0')] ).
cnf(242,plain,
icext(uri_rdf_Property,uri_rdf_first),
inference(res,[status(thm),theory(equality)],[11,90]),
[iquote('0:Res:11.0,90.0')] ).
cnf(95,axiom,
( ~ iext(u,v,w)
| ~ iext(uri_rdfs_domain,u,x)
| icext(x,v) ),
file('SWB029+4.p',unknown),
[] ).
cnf(241,plain,
icext(uri_rdf_Property,uri_rdf_rest),
inference(res,[status(thm),theory(equality)],[13,90]),
[iquote('0:Res:13.0,90.0')] ).
cnf(240,plain,
icext(uri_rdf_Property,uri_rdf__1),
inference(res,[status(thm),theory(equality)],[14,90]),
[iquote('0:Res:14.0,90.0')] ).
cnf(239,plain,
icext(uri_rdf_Property,uri_rdf__2),
inference(res,[status(thm),theory(equality)],[15,90]),
[iquote('0:Res:15.0,90.0')] ).
cnf(238,plain,
icext(uri_rdf_Property,uri_rdf__3),
inference(res,[status(thm),theory(equality)],[16,90]),
[iquote('0:Res:16.0,90.0')] ).
cnf(96,axiom,
( ~ iext(u,v,w)
| ~ iext(uri_rdfs_range,u,x)
| icext(x,w) ),
file('SWB029+4.p',unknown),
[] ).
cnf(237,plain,
icext(uri_rdf_Property,uri_rdf_object),
inference(res,[status(thm),theory(equality)],[17,90]),
[iquote('0:Res:17.0,90.0')] ).
cnf(236,plain,
icext(uri_rdf_Property,uri_rdf_value),
inference(res,[status(thm),theory(equality)],[18,90]),
[iquote('0:Res:18.0,90.0')] ).
cnf(235,plain,
icext(uri_rdf_Property,uri_rdf_subject),
inference(res,[status(thm),theory(equality)],[19,90]),
[iquote('0:Res:19.0,90.0')] ).
cnf(234,plain,
icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__1),
inference(res,[status(thm),theory(equality)],[46,90]),
[iquote('0:Res:46.0,90.0')] ).
cnf(94,axiom,
( ~ icext(u,v)
| ~ iext(uri_rdfs_subClassOf,u,w)
| icext(w,v) ),
file('SWB029+4.p',unknown),
[] ).
cnf(233,plain,
icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__2),
inference(res,[status(thm),theory(equality)],[47,90]),
[iquote('0:Res:47.0,90.0')] ).
cnf(232,plain,
icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__3),
inference(res,[status(thm),theory(equality)],[48,90]),
[iquote('0:Res:48.0,90.0')] ).
cnf(231,plain,
icext(uri_rdfs_Datatype,uri_rdf_XMLLiteral),
inference(res,[status(thm),theory(equality)],[51,90]),
[iquote('0:Res:51.0,90.0')] ).
cnf(230,plain,
icext(uri_rdfs_Class,uri_rdf_Property),
inference(res,[status(thm),theory(equality)],[55,90]),
[iquote('0:Res:55.0,90.0')] ).
cnf(90,axiom,
( ~ iext(uri_rdf_type,u,v)
| icext(v,u) ),
file('SWB029+4.p',unknown),
[] ).
cnf(226,plain,
iext(uri_rdf_type,u,uri_rdfs_Resource),
inference(res,[status(thm),theory(equality)],[100,91]),
[iquote('0:Res:100.0,91.0')] ).
cnf(91,axiom,
( ~ icext(u,v)
| iext(uri_rdf_type,v,u) ),
file('SWB029+4.p',unknown),
[] ).
cnf(216,plain,
ic(uri_rdfs_Resource),
inference(ems,[status(thm)],[134,141]),
[iquote('0:EmS:134.0,141.0')] ).
cnf(92,axiom,
( ~ icext(uri_rdfs_ContainerMembershipProperty,u)
| iext(uri_rdfs_subPropertyOf,u,uri_rdfs_member) ),
file('SWB029+4.p',unknown),
[] ).
cnf(215,plain,
ip(uri_owl_complementOf),
inference(res,[status(thm),theory(equality)],[2,80]),
[iquote('0:Res:2.0,80.0')] ).
cnf(212,plain,
ip(uri_owl_intersectionOf),
inference(res,[status(thm),theory(equality)],[6,80]),
[iquote('0:Res:6.0,80.0')] ).
cnf(208,plain,
ip(uri_rdfs_subPropertyOf),
inference(res,[status(thm),theory(equality)],[26,80]),
[iquote('0:Res:26.0,80.0')] ).
cnf(162,plain,
ip(uri_rdfs_subClassOf),
inference(res,[status(thm),theory(equality)],[52,80]),
[iquote('0:Res:52.0,80.0')] ).
cnf(93,axiom,
( ~ icext(uri_rdfs_Datatype,u)
| iext(uri_rdfs_subClassOf,u,uri_rdfs_Literal) ),
file('SWB029+4.p',unknown),
[] ).
cnf(145,plain,
ip(uri_rdfs_domain),
inference(res,[status(thm),theory(equality)],[70,80]),
[iquote('0:Res:70.0,80.0')] ).
cnf(144,plain,
ip(uri_rdfs_range),
inference(res,[status(thm),theory(equality)],[71,80]),
[iquote('0:Res:71.0,80.0')] ).
cnf(141,plain,
ic(uri_rdfs_ContainerMembershipProperty),
inference(res,[status(thm),theory(equality)],[37,84]),
[iquote('0:Res:37.0,84.0')] ).
cnf(140,plain,
ic(uri_rdf_Alt),
inference(res,[status(thm),theory(equality)],[35,84]),
[iquote('0:Res:35.0,84.0')] ).
cnf(80,axiom,
( ~ iext(u,v,w)
| ip(u) ),
file('SWB029+4.p',unknown),
[] ).
cnf(139,plain,
ic(uri_rdf_Bag),
inference(res,[status(thm),theory(equality)],[36,84]),
[iquote('0:Res:36.0,84.0')] ).
cnf(138,plain,
ic(uri_rdfs_Seq),
inference(res,[status(thm),theory(equality)],[49,84]),
[iquote('0:Res:49.0,84.0')] ).
cnf(137,plain,
ic(uri_rdf_XMLLiteral),
inference(res,[status(thm),theory(equality)],[50,84]),
[iquote('0:Res:50.0,84.0')] ).
cnf(136,plain,
ic(uri_rdfs_Datatype),
inference(res,[status(thm),theory(equality)],[52,84]),
[iquote('0:Res:52.0,84.0')] ).
cnf(84,axiom,
( ~ iext(uri_rdfs_subClassOf,u,v)
| ic(u) ),
file('SWB029+4.p',unknown),
[] ).
cnf(133,plain,
ic(uri_rdf_Property),
inference(res,[status(thm),theory(equality)],[37,85]),
[iquote('0:Res:37.0,85.0')] ).
cnf(130,plain,
ic(uri_rdfs_Container),
inference(res,[status(thm),theory(equality)],[49,85]),
[iquote('0:Res:49.0,85.0')] ).
cnf(129,plain,
ic(uri_rdfs_Literal),
inference(res,[status(thm),theory(equality)],[50,85]),
[iquote('0:Res:50.0,85.0')] ).
cnf(128,plain,
ic(uri_rdfs_Class),
inference(res,[status(thm),theory(equality)],[52,85]),
[iquote('0:Res:52.0,85.0')] ).
cnf(85,axiom,
( ~ iext(uri_rdfs_subClassOf,u,v)
| ic(v) ),
file('SWB029+4.p',unknown),
[] ).
cnf(126,plain,
ip(uri_rdfs_isDefinedBy),
inference(res,[status(thm),theory(equality)],[26,87]),
[iquote('0:Res:26.0,87.0')] ).
cnf(87,axiom,
( ~ iext(uri_rdfs_subPropertyOf,u,v)
| ip(u) ),
file('SWB029+4.p',unknown),
[] ).
cnf(124,plain,
ip(uri_rdfs_seeAlso),
inference(res,[status(thm),theory(equality)],[26,88]),
[iquote('0:Res:26.0,88.0')] ).
cnf(122,plain,
ip(uri_rdf_type),
inference(res,[status(thm),theory(equality)],[21,81]),
[iquote('0:Res:21.0,81.0')] ).
cnf(88,axiom,
( ~ iext(uri_rdfs_subPropertyOf,u,v)
| ip(v) ),
file('SWB029+4.p',unknown),
[] ).
cnf(121,plain,
ip(uri_rdf_first),
inference(res,[status(thm),theory(equality)],[11,81]),
[iquote('0:Res:11.0,81.0')] ).
cnf(120,plain,
ip(uri_rdf_rest),
inference(res,[status(thm),theory(equality)],[13,81]),
[iquote('0:Res:13.0,81.0')] ).
cnf(119,plain,
ip(uri_rdf__1),
inference(res,[status(thm),theory(equality)],[14,81]),
[iquote('0:Res:14.0,81.0')] ).
cnf(118,plain,
ip(uri_rdf__2),
inference(res,[status(thm),theory(equality)],[15,81]),
[iquote('0:Res:15.0,81.0')] ).
cnf(86,axiom,
( ~ ic(u)
| iext(uri_rdfs_subClassOf,u,u) ),
file('SWB029+4.p',unknown),
[] ).
cnf(117,plain,
ip(uri_rdf__3),
inference(res,[status(thm),theory(equality)],[16,81]),
[iquote('0:Res:16.0,81.0')] ).
cnf(116,plain,
ip(uri_rdf_object),
inference(res,[status(thm),theory(equality)],[17,81]),
[iquote('0:Res:17.0,81.0')] ).
cnf(115,plain,
ip(uri_rdf_value),
inference(res,[status(thm),theory(equality)],[18,81]),
[iquote('0:Res:18.0,81.0')] ).
cnf(114,plain,
ip(uri_rdf_subject),
inference(res,[status(thm),theory(equality)],[19,81]),
[iquote('0:Res:19.0,81.0')] ).
cnf(89,axiom,
( ~ ip(u)
| iext(uri_rdfs_subPropertyOf,u,u) ),
file('SWB029+4.p',unknown),
[] ).
cnf(81,axiom,
( ~ iext(uri_rdf_type,u,uri_rdf_Property)
| ip(u) ),
file('SWB029+4.p',unknown),
[] ).
cnf(82,axiom,
( ~ ip(u)
| iext(uri_rdf_type,u,uri_rdf_Property) ),
file('SWB029+4.p',unknown),
[] ).
cnf(83,axiom,
( ~ ic(u)
| iext(uri_rdfs_subClassOf,u,uri_rdfs_Resource) ),
file('SWB029+4.p',unknown),
[] ).
cnf(75,axiom,
( ~ icext(uri_rdfs_Class,u)
| ic(u) ),
file('SWB029+4.p',unknown),
[] ).
cnf(79,axiom,
( ~ icext(uri_rdfs_Literal,u)
| lv(u) ),
file('SWB029+4.p',unknown),
[] ).
cnf(74,axiom,
( ~ ic(u)
| icext(uri_rdfs_Class,u) ),
file('SWB029+4.p',unknown),
[] ).
cnf(78,axiom,
( ~ lv(u)
| icext(uri_rdfs_Literal,u) ),
file('SWB029+4.p',unknown),
[] ).
cnf(72,axiom,
~ iext(uri_rdf_type,uri_ex_w,uri_ex_B),
file('SWB029+4.p',unknown),
[] ).
cnf(101,plain,
~ icext(uri_ex_B,uri_ex_w),
inference(res,[status(thm),theory(equality)],[91,72]),
[iquote('0:Res:91.1,72.0')] ).
cnf(21,axiom,
iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property),
file('SWB029+4.p',unknown),
[] ).
cnf(53,axiom,
iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_Property),
file('SWB029+4.p',unknown),
[] ).
cnf(57,axiom,
iext(uri_rdfs_range,uri_rdfs_range,uri_rdfs_Class),
file('SWB029+4.p',unknown),
[] ).
cnf(2,axiom,
iext(uri_owl_complementOf,skc7,uri_ex_A),
file('SWB029+4.p',unknown),
[] ).
cnf(3,axiom,
iext(uri_rdf_type,uri_ex_w,skc6),
file('SWB029+4.p',unknown),
[] ).
cnf(4,axiom,
iext(uri_rdf_first,skc5,uri_ex_A),
file('SWB029+4.p',unknown),
[] ).
cnf(5,axiom,
iext(uri_rdf_rest,skc5,skc4),
file('SWB029+4.p',unknown),
[] ).
cnf(6,axiom,
iext(uri_owl_intersectionOf,skc6,skc5),
file('SWB029+4.p',unknown),
[] ).
cnf(7,axiom,
iext(uri_rdf_rest,skc4,uri_rdf_nil),
file('SWB029+4.p',unknown),
[] ).
cnf(8,axiom,
iext(uri_rdf_first,skc4,skc7),
file('SWB029+4.p',unknown),
[] ).
cnf(9,axiom,
iext(uri_rdf_type,uri_ex_A,uri_owl_Class),
file('SWB029+4.p',unknown),
[] ).
cnf(10,axiom,
iext(uri_rdf_type,uri_ex_B,uri_owl_Class),
file('SWB029+4.p',unknown),
[] ).
cnf(11,axiom,
iext(uri_rdf_type,uri_rdf_first,uri_rdf_Property),
file('SWB029+4.p',unknown),
[] ).
cnf(12,axiom,
iext(uri_rdf_type,uri_rdf_nil,uri_rdf_List),
file('SWB029+4.p',unknown),
[] ).
cnf(13,axiom,
iext(uri_rdf_type,uri_rdf_rest,uri_rdf_Property),
file('SWB029+4.p',unknown),
[] ).
cnf(14,axiom,
iext(uri_rdf_type,uri_rdf__1,uri_rdf_Property),
file('SWB029+4.p',unknown),
[] ).
cnf(15,axiom,
iext(uri_rdf_type,uri_rdf__2,uri_rdf_Property),
file('SWB029+4.p',unknown),
[] ).
cnf(16,axiom,
iext(uri_rdf_type,uri_rdf__3,uri_rdf_Property),
file('SWB029+4.p',unknown),
[] ).
cnf(17,axiom,
iext(uri_rdf_type,uri_rdf_object,uri_rdf_Property),
file('SWB029+4.p',unknown),
[] ).
cnf(18,axiom,
iext(uri_rdf_type,uri_rdf_value,uri_rdf_Property),
file('SWB029+4.p',unknown),
[] ).
cnf(19,axiom,
iext(uri_rdf_type,uri_rdf_subject,uri_rdf_Property),
file('SWB029+4.p',unknown),
[] ).
cnf(22,axiom,
iext(uri_rdfs_domain,uri_rdfs_comment,uri_rdfs_Resource),
file('SWB029+4.p',unknown),
[] ).
cnf(23,axiom,
iext(uri_rdfs_range,uri_rdfs_comment,uri_rdfs_Literal),
file('SWB029+4.p',unknown),
[] ).
cnf(24,axiom,
iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,uri_rdfs_Resource),
file('SWB029+4.p',unknown),
[] ).
cnf(25,axiom,
iext(uri_rdfs_range,uri_rdfs_isDefinedBy,uri_rdfs_Resource),
file('SWB029+4.p',unknown),
[] ).
cnf(26,axiom,
iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),
file('SWB029+4.p',unknown),
[] ).
cnf(27,axiom,
iext(uri_rdfs_domain,uri_rdfs_label,uri_rdfs_Resource),
file('SWB029+4.p',unknown),
[] ).
cnf(28,axiom,
iext(uri_rdfs_range,uri_rdfs_label,uri_rdfs_Literal),
file('SWB029+4.p',unknown),
[] ).
cnf(29,axiom,
iext(uri_rdfs_domain,uri_rdfs_seeAlso,uri_rdfs_Resource),
file('SWB029+4.p',unknown),
[] ).
cnf(30,axiom,
iext(uri_rdfs_range,uri_rdfs_seeAlso,uri_rdfs_Resource),
file('SWB029+4.p',unknown),
[] ).
cnf(31,axiom,
iext(uri_rdfs_domain,uri_rdf_first,uri_rdf_List),
file('SWB029+4.p',unknown),
[] ).
cnf(32,axiom,
iext(uri_rdfs_range,uri_rdf_first,uri_rdfs_Resource),
file('SWB029+4.p',unknown),
[] ).
cnf(33,axiom,
iext(uri_rdfs_domain,uri_rdf_rest,uri_rdf_List),
file('SWB029+4.p',unknown),
[] ).
cnf(34,axiom,
iext(uri_rdfs_range,uri_rdf_rest,uri_rdf_List),
file('SWB029+4.p',unknown),
[] ).
cnf(35,axiom,
iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Container),
file('SWB029+4.p',unknown),
[] ).
cnf(36,axiom,
iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Container),
file('SWB029+4.p',unknown),
[] ).
cnf(37,axiom,
iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),
file('SWB029+4.p',unknown),
[] ).
cnf(38,axiom,
iext(uri_rdfs_domain,uri_rdfs_member,uri_rdfs_Resource),
file('SWB029+4.p',unknown),
[] ).
cnf(39,axiom,
iext(uri_rdfs_range,uri_rdfs_member,uri_rdfs_Resource),
file('SWB029+4.p',unknown),
[] ).
cnf(40,axiom,
iext(uri_rdfs_domain,uri_rdf__1,uri_rdfs_Resource),
file('SWB029+4.p',unknown),
[] ).
cnf(41,axiom,
iext(uri_rdfs_domain,uri_rdf__2,uri_rdfs_Resource),
file('SWB029+4.p',unknown),
[] ).
cnf(42,axiom,
iext(uri_rdfs_domain,uri_rdf__3,uri_rdfs_Resource),
file('SWB029+4.p',unknown),
[] ).
cnf(43,axiom,
iext(uri_rdfs_range,uri_rdf__1,uri_rdfs_Resource),
file('SWB029+4.p',unknown),
[] ).
cnf(44,axiom,
iext(uri_rdfs_range,uri_rdf__2,uri_rdfs_Resource),
file('SWB029+4.p',unknown),
[] ).
cnf(45,axiom,
iext(uri_rdfs_range,uri_rdf__3,uri_rdfs_Resource),
file('SWB029+4.p',unknown),
[] ).
cnf(46,axiom,
iext(uri_rdf_type,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),
file('SWB029+4.p',unknown),
[] ).
cnf(47,axiom,
iext(uri_rdf_type,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),
file('SWB029+4.p',unknown),
[] ).
cnf(48,axiom,
iext(uri_rdf_type,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),
file('SWB029+4.p',unknown),
[] ).
cnf(49,axiom,
iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Container),
file('SWB029+4.p',unknown),
[] ).
cnf(50,axiom,
iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Literal),
file('SWB029+4.p',unknown),
[] ).
cnf(51,axiom,
iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Datatype),
file('SWB029+4.p',unknown),
[] ).
cnf(52,axiom,
iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Class),
file('SWB029+4.p',unknown),
[] ).
cnf(54,axiom,
iext(uri_rdfs_range,uri_rdfs_domain,uri_rdfs_Class),
file('SWB029+4.p',unknown),
[] ).
cnf(55,axiom,
iext(uri_rdf_type,uri_rdf_Property,uri_rdfs_Class),
file('SWB029+4.p',unknown),
[] ).
cnf(56,axiom,
iext(uri_rdfs_domain,uri_rdfs_range,uri_rdf_Property),
file('SWB029+4.p',unknown),
[] ).
cnf(58,axiom,
iext(uri_rdfs_domain,uri_rdf_object,uri_rdfs_Statement),
file('SWB029+4.p',unknown),
[] ).
cnf(60,axiom,
iext(uri_rdfs_domain,uri_rdf_predicate,uri_rdfs_Statement),
file('SWB029+4.p',unknown),
[] ).
cnf(61,axiom,
iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Resource),
file('SWB029+4.p',unknown),
[] ).
cnf(62,axiom,
iext(uri_rdfs_domain,uri_rdf_subject,uri_rdfs_Statement),
file('SWB029+4.p',unknown),
[] ).
cnf(63,axiom,
iext(uri_rdfs_range,uri_rdf_subject,uri_rdfs_Resource),
file('SWB029+4.p',unknown),
[] ).
cnf(64,axiom,
iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdfs_Class),
file('SWB029+4.p',unknown),
[] ).
cnf(65,axiom,
iext(uri_rdfs_range,uri_rdfs_subClassOf,uri_rdfs_Class),
file('SWB029+4.p',unknown),
[] ).
cnf(66,axiom,
iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdf_Property),
file('SWB029+4.p',unknown),
[] ).
cnf(67,axiom,
iext(uri_rdfs_range,uri_rdfs_subPropertyOf,uri_rdf_Property),
file('SWB029+4.p',unknown),
[] ).
cnf(68,axiom,
iext(uri_rdfs_domain,uri_rdf_type,uri_rdfs_Resource),
file('SWB029+4.p',unknown),
[] ).
cnf(69,axiom,
iext(uri_rdfs_range,uri_rdf_type,uri_rdfs_Class),
file('SWB029+4.p',unknown),
[] ).
cnf(70,axiom,
iext(uri_rdfs_domain,uri_rdf_value,uri_rdfs_Resource),
file('SWB029+4.p',unknown),
[] ).
cnf(71,axiom,
iext(uri_rdfs_range,uri_rdf_value,uri_rdfs_Resource),
file('SWB029+4.p',unknown),
[] ).
cnf(100,plain,
icext(uri_rdfs_Resource,u),
inference(mrr,[status(thm)],[76,1]),
[iquote('0:MRR:76.0,1.0')] ).
cnf(1,axiom,
ir(u),
file('SWB029+4.p',unknown),
[] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : SWB029+4 : TPTP v8.1.0. Released v5.2.0.
% 0.04/0.14 % Command : run_spass %d %s
% 0.14/0.36 % Computer : n024.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 600
% 0.14/0.36 % DateTime : Wed Jun 1 13:41:36 EDT 2022
% 0.14/0.36 % CPUTime :
% 0.21/0.51
% 0.21/0.51 SPASS V 3.9
% 0.21/0.51 SPASS beiseite: Completion found.
% 0.21/0.51 % SZS status CounterSatisfiable
% 0.21/0.51 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.21/0.51 SPASS derived 883 clauses, backtracked 0 clauses, performed 0 splits and kept 450 clauses.
% 0.21/0.51 SPASS allocated 98093 KBytes.
% 0.21/0.51 SPASS spent 0:00:00.15 on the problem.
% 0.21/0.51 0:00:00.03 for the input.
% 0.21/0.51 0:00:00.03 for the FLOTTER CNF translation.
% 0.21/0.51 0:00:00.01 for inferences.
% 0.21/0.51 0:00:00.00 for the backtracking.
% 0.21/0.51 0:00:00.04 for the reduction.
% 0.21/0.51
% 0.21/0.51
% 0.21/0.51 The saturated set of worked-off clauses is :
% 0.21/0.51 % SZS output start Saturation
% See solution above
%------------------------------------------------------------------------------