%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SWB020+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:21:17 EDT 2022
% Result : CounterSatisfiable 0.21s 0.50s
% Output : Saturation 0.21s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named 82)
% Comments :
%------------------------------------------------------------------------------
cnf(555,plain,
( ~ ic(u)
| ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,v)
| iext(v,u,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[232,104]),
[iquote('0:Res:232.1,104.0')] ).
cnf(554,plain,
( ~ lv(u)
| ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,v)
| iext(v,u,uri_rdfs_Literal) ),
inference(res,[status(thm),theory(equality)],[231,104]),
[iquote('0:Res:231.1,104.0')] ).
cnf(345,plain,
( ~ lv(u)
| ~ iext(uri_rdfs_range,uri_rdf_type,v)
| icext(v,uri_rdfs_Literal) ),
inference(res,[status(thm),theory(equality)],[231,102]),
[iquote('0:Res:231.1,102.0')] ).
cnf(563,plain,
( ~ ip(u)
| ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,v)
| iext(v,u,u) ),
inference(res,[status(thm),theory(equality)],[95,104]),
[iquote('0:Res:95.1,104.0')] ).
cnf(553,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,v,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[230,104]),
[iquote('0:Res:230.0,104.0')] ).
cnf(1028,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,u)
| iext(u,uri_ex_d,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[965,104]),
[iquote('0:Res:965.0,104.0')] ).
cnf(1019,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,u)
| iext(u,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[964,104]),
[iquote('0:Res:964.0,104.0')] ).
cnf(1010,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,u)
| iext(u,uri_rdf_Alt,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[963,104]),
[iquote('0:Res:963.0,104.0')] ).
cnf(538,plain,
( ~ ic(u)
| ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,v)
| iext(v,u,u) ),
inference(res,[status(thm),theory(equality)],[92,104]),
[iquote('0:Res:92.1,104.0')] ).
cnf(1000,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,u)
| iext(u,uri_rdf_Bag,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[962,104]),
[iquote('0:Res:962.0,104.0')] ).
cnf(991,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,u)
| iext(u,uri_rdfs_Seq,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[961,104]),
[iquote('0:Res:961.0,104.0')] ).
cnf(982,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,u)
| iext(u,uri_rdf_XMLLiteral,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[960,104]),
[iquote('0:Res:960.0,104.0')] ).
cnf(973,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,u)
| iext(u,uri_rdfs_Datatype,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[959,104]),
[iquote('0:Res:959.0,104.0')] ).
cnf(551,plain,
( ~ ip(u)
| ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,v)
| iext(v,u,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[88,104]),
[iquote('0:Res:88.1,104.0')] ).
cnf(853,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,skc8,uri_rdf_List) ),
inference(res,[status(thm),theory(equality)],[851,104]),
[iquote('0:Res:851.0,104.0')] ).
cnf(842,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,skc13,uri_rdf_List) ),
inference(res,[status(thm),theory(equality)],[840,104]),
[iquote('0:Res:840.0,104.0')] ).
cnf(829,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_ex_d,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[827,104]),
[iquote('0:Res:827.0,104.0')] ).
cnf(820,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdf_Alt,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[813,104]),
[iquote('0:Res:813.0,104.0')] ).
cnf(537,plain,
( ~ ic(u)
| ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,v)
| iext(v,u,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[89,104]),
[iquote('0:Res:89.1,104.0')] ).
cnf(815,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdf_Bag,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[810,104]),
[iquote('0:Res:810.0,104.0')] ).
cnf(804,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdfs_Seq,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[802,104]),
[iquote('0:Res:802.0,104.0')] ).
cnf(794,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdfs_comment,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[790,104]),
[iquote('0:Res:790.0,104.0')] ).
cnf(785,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdfs_isDefinedBy,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[782,104]),
[iquote('0:Res:782.0,104.0')] ).
cnf(436,plain,
( ~ ip(u)
| ~ iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,v)
| icext(v,u) ),
inference(res,[status(thm),theory(equality)],[95,101]),
[iquote('0:Res:95.1,101.0')] ).
cnf(777,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdfs_label,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[774,104]),
[iquote('0:Res:774.0,104.0')] ).
cnf(763,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdfs_range,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[760,104]),
[iquote('0:Res:760.0,104.0')] ).
cnf(751,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdfs_domain,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[748,104]),
[iquote('0:Res:748.0,104.0')] ).
cnf(742,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdfs_subClassOf,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[739,104]),
[iquote('0:Res:739.0,104.0')] ).
cnf(412,plain,
( ~ ic(u)
| ~ iext(uri_rdfs_domain,uri_rdfs_subClassOf,v)
| icext(v,u) ),
inference(res,[status(thm),theory(equality)],[89,101]),
[iquote('0:Res:89.1,101.0')] ).
cnf(733,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdfs_subPropertyOf,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[730,104]),
[iquote('0:Res:730.0,104.0')] ).
cnf(721,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdfs_member,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[718,104]),
[iquote('0:Res:718.0,104.0')] ).
cnf(711,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdf_predicate,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[707,104]),
[iquote('0:Res:707.0,104.0')] ).
cnf(699,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,skc12,uri_rdf_List) ),
inference(res,[status(thm),theory(equality)],[692,104]),
[iquote('0:Res:692.0,104.0')] ).
cnf(352,plain,
( ~ ip(u)
| ~ iext(uri_rdfs_range,uri_rdfs_subPropertyOf,v)
| icext(v,u) ),
inference(res,[status(thm),theory(equality)],[95,102]),
[iquote('0:Res:95.1,102.0')] ).
cnf(694,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,skc11,uri_rdf_List) ),
inference(res,[status(thm),theory(equality)],[690,104]),
[iquote('0:Res:690.0,104.0')] ).
cnf(684,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,skc7,uri_rdf_List) ),
inference(res,[status(thm),theory(equality)],[682,104]),
[iquote('0:Res:682.0,104.0')] ).
cnf(672,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdfs_seeAlso,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[669,104]),
[iquote('0:Res:669.0,104.0')] ).
cnf(659,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[657,104]),
[iquote('0:Res:657.0,104.0')] ).
cnf(329,plain,
( ~ ic(u)
| ~ iext(uri_rdfs_range,uri_rdfs_subClassOf,v)
| icext(v,u) ),
inference(res,[status(thm),theory(equality)],[92,102]),
[iquote('0:Res:92.1,102.0')] ).
cnf(651,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,skc9,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[649,104]),
[iquote('0:Res:649.0,104.0')] ).
cnf(643,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdfs_Container,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[640,104]),
[iquote('0:Res:640.0,104.0')] ).
cnf(634,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdfs_Literal,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[632,104]),
[iquote('0:Res:632.0,104.0')] ).
cnf(626,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdfs_Datatype,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[614,104]),
[iquote('0:Res:614.0,104.0')] ).
cnf(108,plain,
( ~ iext(u,uri_ex_d,uri_ex_c3)
| ~ iext(uri_rdfs_subPropertyOf,u,uri_rdfs_subClassOf) ),
inference(res,[status(thm),theory(equality)],[104,78]),
[iquote('0:Res:104.2,78.0')] ).
cnf(975,plain,
( ~ iext(uri_rdfs_range,uri_rdfs_subClassOf,u)
| icext(u,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[959,102]),
[iquote('0:Res:959.0,102.0')] ).
cnf(965,plain,
iext(uri_rdfs_subClassOf,uri_ex_d,uri_rdfs_Resource),
inference(res,[status(thm),theory(equality)],[8,484]),
[iquote('0:Res:8.0,484.0')] ).
cnf(964,plain,
iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Resource),
inference(res,[status(thm),theory(equality)],[43,484]),
[iquote('0:Res:43.0,484.0')] ).
cnf(963,plain,
iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Resource),
inference(res,[status(thm),theory(equality)],[41,484]),
[iquote('0:Res:41.0,484.0')] ).
cnf(107,plain,
( ~ iext(uri_rdfs_subClassOf,u,uri_ex_c3)
| ~ iext(uri_rdfs_subClassOf,uri_ex_d,u) ),
inference(res,[status(thm),theory(equality)],[103,78]),
[iquote('0:Res:103.2,78.0')] ).
cnf(962,plain,
iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Resource),
inference(res,[status(thm),theory(equality)],[42,484]),
[iquote('0:Res:42.0,484.0')] ).
cnf(961,plain,
iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Resource),
inference(res,[status(thm),theory(equality)],[55,484]),
[iquote('0:Res:55.0,484.0')] ).
cnf(960,plain,
iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Resource),
inference(res,[status(thm),theory(equality)],[56,484]),
[iquote('0:Res:56.0,484.0')] ).
cnf(959,plain,
iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Resource),
inference(res,[status(thm),theory(equality)],[58,484]),
[iquote('0:Res:58.0,484.0')] ).
cnf(484,plain,
( ~ iext(uri_rdfs_subClassOf,u,v)
| iext(uri_rdfs_subClassOf,u,uri_rdfs_Resource) ),
inference(mrr,[status(thm)],[482,91]),
[iquote('0:MRR:482.0,91.1')] ).
cnf(621,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdf_List,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[611,104]),
[iquote('0:Res:611.0,104.0')] ).
cnf(616,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdfs_Statement,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[609,104]),
[iquote('0:Res:609.0,104.0')] ).
cnf(597,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdfs_Class,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[595,104]),
[iquote('0:Res:595.0,104.0')] ).
cnf(588,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdfs_Resource,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[586,104]),
[iquote('0:Res:586.0,104.0')] ).
cnf(580,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_owl_unionOf,u)
| iext(u,uri_ex_c,skc13) ),
inference(res,[status(thm),theory(equality)],[2,104]),
[iquote('0:Res:2.0,104.0')] ).
cnf(579,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_rest,u)
| iext(u,skc13,skc12) ),
inference(res,[status(thm),theory(equality)],[4,104]),
[iquote('0:Res:4.0,104.0')] ).
cnf(578,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_rest,u)
| iext(u,skc12,skc11) ),
inference(res,[status(thm),theory(equality)],[5,104]),
[iquote('0:Res:5.0,104.0')] ).
cnf(577,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_first,u)
| iext(u,skc12,uri_ex_c2) ),
inference(res,[status(thm),theory(equality)],[6,104]),
[iquote('0:Res:6.0,104.0')] ).
cnf(576,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_owl_complementOf,u)
| iext(u,skc10,uri_ex_c2) ),
inference(res,[status(thm),theory(equality)],[7,104]),
[iquote('0:Res:7.0,104.0')] ).
cnf(575,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_owl_intersectionOf,u)
| iext(u,skc9,skc8) ),
inference(res,[status(thm),theory(equality)],[9,104]),
[iquote('0:Res:9.0,104.0')] ).
cnf(574,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_rest,u)
| iext(u,skc8,skc7) ),
inference(res,[status(thm),theory(equality)],[10,104]),
[iquote('0:Res:10.0,104.0')] ).
cnf(573,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_first,u)
| iext(u,skc8,uri_ex_c) ),
inference(res,[status(thm),theory(equality)],[11,104]),
[iquote('0:Res:11.0,104.0')] ).
cnf(572,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_first,u)
| iext(u,skc7,skc10) ),
inference(res,[status(thm),theory(equality)],[12,104]),
[iquote('0:Res:12.0,104.0')] ).
cnf(571,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_rest,u)
| iext(u,skc7,uri_rdf_nil) ),
inference(res,[status(thm),theory(equality)],[13,104]),
[iquote('0:Res:13.0,104.0')] ).
cnf(570,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_first,u)
| iext(u,skc11,uri_ex_c3) ),
inference(res,[status(thm),theory(equality)],[14,104]),
[iquote('0:Res:14.0,104.0')] ).
cnf(569,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_rest,u)
| iext(u,skc11,uri_rdf_nil) ),
inference(res,[status(thm),theory(equality)],[15,104]),
[iquote('0:Res:15.0,104.0')] ).
cnf(568,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_first,u)
| iext(u,skc13,uri_ex_c1) ),
inference(res,[status(thm),theory(equality)],[3,104]),
[iquote('0:Res:3.0,104.0')] ).
cnf(566,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,u)
| iext(u,uri_rdf__1,uri_rdfs_member) ),
inference(res,[status(thm),theory(equality)],[282,104]),
[iquote('0:Res:282.0,104.0')] ).
cnf(565,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,u)
| iext(u,uri_rdf__2,uri_rdfs_member) ),
inference(res,[status(thm),theory(equality)],[271,104]),
[iquote('0:Res:271.0,104.0')] ).
cnf(567,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_owl_disjointWith,u)
| iext(u,uri_ex_d,uri_ex_c1) ),
inference(res,[status(thm),theory(equality)],[16,104]),
[iquote('0:Res:16.0,104.0')] ).
cnf(564,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,u)
| iext(u,uri_rdf__3,uri_rdfs_member) ),
inference(res,[status(thm),theory(equality)],[269,104]),
[iquote('0:Res:269.0,104.0')] ).
cnf(562,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,u)
| iext(u,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso) ),
inference(res,[status(thm),theory(equality)],[32,104]),
[iquote('0:Res:32.0,104.0')] ).
cnf(561,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_range,u)
| iext(u,uri_rdfs_range,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[63,104]),
[iquote('0:Res:63.0,104.0')] ).
cnf(560,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_range,u)
| iext(u,uri_rdfs_isDefinedBy,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[31,104]),
[iquote('0:Res:31.0,104.0')] ).
cnf(559,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_range,u)
| iext(u,uri_rdfs_comment,uri_rdfs_Literal) ),
inference(res,[status(thm),theory(equality)],[29,104]),
[iquote('0:Res:29.0,104.0')] ).
cnf(558,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_range,u)
| iext(u,uri_rdfs_label,uri_rdfs_Literal) ),
inference(res,[status(thm),theory(equality)],[34,104]),
[iquote('0:Res:34.0,104.0')] ).
cnf(557,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_range,u)
| iext(u,uri_rdf_rest,uri_rdf_List) ),
inference(res,[status(thm),theory(equality)],[40,104]),
[iquote('0:Res:40.0,104.0')] ).
cnf(556,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdf_XMLLiteral,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[491,104]),
[iquote('0:Res:491.0,104.0')] ).
cnf(552,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdf_nil,uri_rdf_List) ),
inference(res,[status(thm),theory(equality)],[18,104]),
[iquote('0:Res:18.0,104.0')] ).
cnf(550,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdf_type,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[27,104]),
[iquote('0:Res:27.0,104.0')] ).
cnf(549,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdf_first,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[17,104]),
[iquote('0:Res:17.0,104.0')] ).
cnf(548,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdf_rest,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[19,104]),
[iquote('0:Res:19.0,104.0')] ).
cnf(547,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdf__1,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[20,104]),
[iquote('0:Res:20.0,104.0')] ).
cnf(546,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdf__2,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[21,104]),
[iquote('0:Res:21.0,104.0')] ).
cnf(545,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdf__3,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[22,104]),
[iquote('0:Res:22.0,104.0')] ).
cnf(544,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdf_object,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[23,104]),
[iquote('0:Res:23.0,104.0')] ).
cnf(543,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdf_value,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[24,104]),
[iquote('0:Res:24.0,104.0')] ).
cnf(542,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdf_subject,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[25,104]),
[iquote('0:Res:25.0,104.0')] ).
cnf(541,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdf__1,uri_rdfs_ContainerMembershipProperty) ),
inference(res,[status(thm),theory(equality)],[52,104]),
[iquote('0:Res:52.0,104.0')] ).
cnf(540,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdf__2,uri_rdfs_ContainerMembershipProperty) ),
inference(res,[status(thm),theory(equality)],[53,104]),
[iquote('0:Res:53.0,104.0')] ).
cnf(539,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdf__3,uri_rdfs_ContainerMembershipProperty) ),
inference(res,[status(thm),theory(equality)],[54,104]),
[iquote('0:Res:54.0,104.0')] ).
cnf(536,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,u)
| iext(u,uri_ex_d,skc9) ),
inference(res,[status(thm),theory(equality)],[8,104]),
[iquote('0:Res:8.0,104.0')] ).
cnf(535,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,u)
| iext(u,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[43,104]),
[iquote('0:Res:43.0,104.0')] ).
cnf(534,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,u)
| iext(u,uri_rdf_Alt,uri_rdfs_Container) ),
inference(res,[status(thm),theory(equality)],[41,104]),
[iquote('0:Res:41.0,104.0')] ).
cnf(533,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,u)
| iext(u,uri_rdf_Bag,uri_rdfs_Container) ),
inference(res,[status(thm),theory(equality)],[42,104]),
[iquote('0:Res:42.0,104.0')] ).
cnf(532,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,u)
| iext(u,uri_rdfs_Seq,uri_rdfs_Container) ),
inference(res,[status(thm),theory(equality)],[55,104]),
[iquote('0:Res:55.0,104.0')] ).
cnf(531,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,u)
| iext(u,uri_rdf_XMLLiteral,uri_rdfs_Literal) ),
inference(res,[status(thm),theory(equality)],[56,104]),
[iquote('0:Res:56.0,104.0')] ).
cnf(530,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdf_XMLLiteral,uri_rdfs_Datatype) ),
inference(res,[status(thm),theory(equality)],[57,104]),
[iquote('0:Res:57.0,104.0')] ).
cnf(529,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,u)
| iext(u,uri_rdf_first,uri_rdf_List) ),
inference(res,[status(thm),theory(equality)],[37,104]),
[iquote('0:Res:37.0,104.0')] ).
cnf(528,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,u)
| iext(u,uri_rdf_rest,uri_rdf_List) ),
inference(res,[status(thm),theory(equality)],[39,104]),
[iquote('0:Res:39.0,104.0')] ).
cnf(527,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,u)
| iext(u,uri_rdfs_comment,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[28,104]),
[iquote('0:Res:28.0,104.0')] ).
cnf(526,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,u)
| iext(u,uri_rdfs_isDefinedBy,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[30,104]),
[iquote('0:Res:30.0,104.0')] ).
cnf(525,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,u)
| iext(u,uri_rdfs_label,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[33,104]),
[iquote('0:Res:33.0,104.0')] ).
cnf(524,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,u)
| iext(u,uri_rdfs_seeAlso,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[35,104]),
[iquote('0:Res:35.0,104.0')] ).
cnf(523,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,u)
| iext(u,uri_rdfs_member,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[44,104]),
[iquote('0:Res:44.0,104.0')] ).
cnf(522,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,u)
| iext(u,uri_rdf__1,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[46,104]),
[iquote('0:Res:46.0,104.0')] ).
cnf(521,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,u)
| iext(u,uri_rdf__2,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[47,104]),
[iquote('0:Res:47.0,104.0')] ).
cnf(520,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,u)
| iext(u,uri_rdf__3,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[48,104]),
[iquote('0:Res:48.0,104.0')] ).
cnf(519,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,u)
| iext(u,uri_rdfs_domain,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[59,104]),
[iquote('0:Res:59.0,104.0')] ).
cnf(518,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,u)
| iext(u,uri_rdfs_range,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[62,104]),
[iquote('0:Res:62.0,104.0')] ).
cnf(517,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,u)
| iext(u,uri_rdf_object,uri_rdfs_Statement) ),
inference(res,[status(thm),theory(equality)],[64,104]),
[iquote('0:Res:64.0,104.0')] ).
cnf(516,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,u)
| iext(u,uri_rdf_predicate,uri_rdfs_Statement) ),
inference(res,[status(thm),theory(equality)],[66,104]),
[iquote('0:Res:66.0,104.0')] ).
cnf(515,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,u)
| iext(u,uri_rdf_subject,uri_rdfs_Statement) ),
inference(res,[status(thm),theory(equality)],[68,104]),
[iquote('0:Res:68.0,104.0')] ).
cnf(514,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,u)
| iext(u,uri_rdfs_Datatype,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[58,104]),
[iquote('0:Res:58.0,104.0')] ).
cnf(513,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_range,u)
| iext(u,uri_rdfs_domain,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[60,104]),
[iquote('0:Res:60.0,104.0')] ).
cnf(512,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,u)
| iext(u,uri_rdf_Property,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[61,104]),
[iquote('0:Res:61.0,104.0')] ).
cnf(511,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,u)
| iext(u,uri_rdfs_subClassOf,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[70,104]),
[iquote('0:Res:70.0,104.0')] ).
cnf(510,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_range,u)
| iext(u,uri_rdfs_subClassOf,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[71,104]),
[iquote('0:Res:71.0,104.0')] ).
cnf(509,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,u)
| iext(u,uri_rdfs_subPropertyOf,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[72,104]),
[iquote('0:Res:72.0,104.0')] ).
cnf(508,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_range,u)
| iext(u,uri_rdfs_subPropertyOf,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[73,104]),
[iquote('0:Res:73.0,104.0')] ).
cnf(507,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,u)
| iext(u,uri_rdf_type,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[74,104]),
[iquote('0:Res:74.0,104.0')] ).
cnf(506,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_range,u)
| iext(u,uri_rdf_type,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[75,104]),
[iquote('0:Res:75.0,104.0')] ).
cnf(505,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_range,u)
| iext(u,uri_rdfs_seeAlso,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[36,104]),
[iquote('0:Res:36.0,104.0')] ).
cnf(504,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_range,u)
| iext(u,uri_rdf_first,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[38,104]),
[iquote('0:Res:38.0,104.0')] ).
cnf(503,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_range,u)
| iext(u,uri_rdfs_member,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[45,104]),
[iquote('0:Res:45.0,104.0')] ).
cnf(502,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_range,u)
| iext(u,uri_rdf__1,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[49,104]),
[iquote('0:Res:49.0,104.0')] ).
cnf(501,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_range,u)
| iext(u,uri_rdf__2,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[50,104]),
[iquote('0:Res:50.0,104.0')] ).
cnf(500,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_range,u)
| iext(u,uri_rdf__3,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[51,104]),
[iquote('0:Res:51.0,104.0')] ).
cnf(499,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_range,u)
| iext(u,uri_rdf_predicate,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[67,104]),
[iquote('0:Res:67.0,104.0')] ).
cnf(498,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_range,u)
| iext(u,uri_rdf_subject,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[69,104]),
[iquote('0:Res:69.0,104.0')] ).
cnf(497,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,u)
| iext(u,uri_rdf_value,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[76,104]),
[iquote('0:Res:76.0,104.0')] ).
cnf(496,plain,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_range,u)
| iext(u,uri_rdf_value,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[77,104]),
[iquote('0:Res:77.0,104.0')] ).
cnf(481,plain,
( ~ iext(uri_rdfs_subClassOf,u,uri_ex_d)
| iext(uri_rdfs_subClassOf,u,skc9) ),
inference(res,[status(thm),theory(equality)],[8,103]),
[iquote('0:Res:8.0,103.0')] ).
cnf(480,plain,
( ~ iext(uri_rdfs_subClassOf,u,uri_rdfs_ContainerMembershipProperty)
| iext(uri_rdfs_subClassOf,u,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[43,103]),
[iquote('0:Res:43.0,103.0')] ).
cnf(479,plain,
( ~ iext(uri_rdfs_subClassOf,u,uri_rdf_Alt)
| iext(uri_rdfs_subClassOf,u,uri_rdfs_Container) ),
inference(res,[status(thm),theory(equality)],[41,103]),
[iquote('0:Res:41.0,103.0')] ).
cnf(478,plain,
( ~ iext(uri_rdfs_subClassOf,u,uri_rdf_Bag)
| iext(uri_rdfs_subClassOf,u,uri_rdfs_Container) ),
inference(res,[status(thm),theory(equality)],[42,103]),
[iquote('0:Res:42.0,103.0')] ).
cnf(477,plain,
( ~ iext(uri_rdfs_subClassOf,u,uri_rdfs_Seq)
| iext(uri_rdfs_subClassOf,u,uri_rdfs_Container) ),
inference(res,[status(thm),theory(equality)],[55,103]),
[iquote('0:Res:55.0,103.0')] ).
cnf(476,plain,
( ~ iext(uri_rdfs_subClassOf,u,uri_rdf_XMLLiteral)
| iext(uri_rdfs_subClassOf,u,uri_rdfs_Literal) ),
inference(res,[status(thm),theory(equality)],[56,103]),
[iquote('0:Res:56.0,103.0')] ).
cnf(468,plain,
( ~ iext(uri_rdfs_subPropertyOf,u,uri_rdf__1)
| iext(uri_rdfs_subPropertyOf,u,uri_rdfs_member) ),
inference(res,[status(thm),theory(equality)],[282,105]),
[iquote('0:Res:282.0,105.0')] ).
cnf(475,plain,
( ~ iext(uri_rdfs_subClassOf,u,uri_rdfs_Datatype)
| iext(uri_rdfs_subClassOf,u,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[58,103]),
[iquote('0:Res:58.0,103.0')] ).
cnf(462,plain,
( ~ iext(uri_rdfs_subPropertyOf,u,uri_rdf__2)
| iext(uri_rdfs_subPropertyOf,u,uri_rdfs_member) ),
inference(res,[status(thm),theory(equality)],[271,105]),
[iquote('0:Res:271.0,105.0')] ).
cnf(461,plain,
( ~ iext(uri_rdfs_subPropertyOf,u,uri_rdf__3)
| iext(uri_rdfs_subPropertyOf,u,uri_rdfs_member) ),
inference(res,[status(thm),theory(equality)],[269,105]),
[iquote('0:Res:269.0,105.0')] ).
cnf(428,plain,
( ~ iext(uri_rdfs_domain,uri_rdf_type,u)
| icext(u,v) ),
inference(res,[status(thm),theory(equality)],[230,101]),
[iquote('0:Res:230.0,101.0')] ).
cnf(471,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,u)
| icext(u,uri_rdf__1) ),
inference(res,[status(thm),theory(equality)],[282,101]),
[iquote('0:Res:282.0,101.0')] ).
cnf(459,plain,
( ~ iext(uri_rdfs_subPropertyOf,u,uri_rdfs_isDefinedBy)
| iext(uri_rdfs_subPropertyOf,u,uri_rdfs_seeAlso) ),
inference(res,[status(thm),theory(equality)],[32,105]),
[iquote('0:Res:32.0,105.0')] ).
cnf(465,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,u)
| icext(u,uri_rdf__2) ),
inference(res,[status(thm),theory(equality)],[271,101]),
[iquote('0:Res:271.0,101.0')] ).
cnf(457,plain,
( ~ iext(uri_rdfs_range,uri_rdfs_subPropertyOf,u)
| icext(u,uri_rdfs_member) ),
inference(res,[status(thm),theory(equality)],[269,102]),
[iquote('0:Res:269.0,102.0')] ).
cnf(456,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,u)
| icext(u,uri_rdf__3) ),
inference(res,[status(thm),theory(equality)],[269,101]),
[iquote('0:Res:269.0,101.0')] ).
cnf(450,plain,
( ~ iext(uri_rdfs_domain,uri_owl_unionOf,u)
| icext(u,uri_ex_c) ),
inference(res,[status(thm),theory(equality)],[2,101]),
[iquote('0:Res:2.0,101.0')] ).
cnf(449,plain,
( ~ iext(uri_rdfs_domain,uri_rdf_rest,u)
| icext(u,skc13) ),
inference(res,[status(thm),theory(equality)],[4,101]),
[iquote('0:Res:4.0,101.0')] ).
cnf(448,plain,
( ~ iext(uri_rdfs_domain,uri_rdf_rest,u)
| icext(u,skc12) ),
inference(res,[status(thm),theory(equality)],[5,101]),
[iquote('0:Res:5.0,101.0')] ).
cnf(447,plain,
( ~ iext(uri_rdfs_domain,uri_rdf_first,u)
| icext(u,skc12) ),
inference(res,[status(thm),theory(equality)],[6,101]),
[iquote('0:Res:6.0,101.0')] ).
cnf(446,plain,
( ~ iext(uri_rdfs_domain,uri_owl_complementOf,u)
| icext(u,skc10) ),
inference(res,[status(thm),theory(equality)],[7,101]),
[iquote('0:Res:7.0,101.0')] ).
cnf(445,plain,
( ~ iext(uri_rdfs_domain,uri_owl_intersectionOf,u)
| icext(u,skc9) ),
inference(res,[status(thm),theory(equality)],[9,101]),
[iquote('0:Res:9.0,101.0')] ).
cnf(444,plain,
( ~ iext(uri_rdfs_domain,uri_rdf_rest,u)
| icext(u,skc8) ),
inference(res,[status(thm),theory(equality)],[10,101]),
[iquote('0:Res:10.0,101.0')] ).
cnf(851,plain,
iext(uri_rdf_type,skc8,uri_rdf_List),
inference(res,[status(thm),theory(equality)],[850,97]),
[iquote('0:Res:850.0,97.0')] ).
cnf(850,plain,
icext(uri_rdf_List,skc8),
inference(res,[status(thm),theory(equality)],[37,443]),
[iquote('0:Res:37.0,443.0')] ).
cnf(443,plain,
( ~ iext(uri_rdfs_domain,uri_rdf_first,u)
| icext(u,skc8) ),
inference(res,[status(thm),theory(equality)],[11,101]),
[iquote('0:Res:11.0,101.0')] ).
cnf(442,plain,
( ~ iext(uri_rdfs_domain,uri_rdf_first,u)
| icext(u,skc7) ),
inference(res,[status(thm),theory(equality)],[12,101]),
[iquote('0:Res:12.0,101.0')] ).
cnf(441,plain,
( ~ iext(uri_rdfs_domain,uri_rdf_rest,u)
| icext(u,skc7) ),
inference(res,[status(thm),theory(equality)],[13,101]),
[iquote('0:Res:13.0,101.0')] ).
cnf(440,plain,
( ~ iext(uri_rdfs_domain,uri_rdf_first,u)
| icext(u,skc11) ),
inference(res,[status(thm),theory(equality)],[14,101]),
[iquote('0:Res:14.0,101.0')] ).
cnf(439,plain,
( ~ iext(uri_rdfs_domain,uri_rdf_rest,u)
| icext(u,skc11) ),
inference(res,[status(thm),theory(equality)],[15,101]),
[iquote('0:Res:15.0,101.0')] ).
cnf(840,plain,
iext(uri_rdf_type,skc13,uri_rdf_List),
inference(res,[status(thm),theory(equality)],[839,97]),
[iquote('0:Res:839.0,97.0')] ).
cnf(839,plain,
icext(uri_rdf_List,skc13),
inference(res,[status(thm),theory(equality)],[37,438]),
[iquote('0:Res:37.0,438.0')] ).
cnf(438,plain,
( ~ iext(uri_rdfs_domain,uri_rdf_first,u)
| icext(u,skc13) ),
inference(res,[status(thm),theory(equality)],[3,101]),
[iquote('0:Res:3.0,101.0')] ).
cnf(437,plain,
( ~ iext(uri_rdfs_domain,uri_owl_disjointWith,u)
| icext(u,uri_ex_d) ),
inference(res,[status(thm),theory(equality)],[16,101]),
[iquote('0:Res:16.0,101.0')] ).
cnf(435,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,u)
| icext(u,uri_rdfs_isDefinedBy) ),
inference(res,[status(thm),theory(equality)],[32,101]),
[iquote('0:Res:32.0,101.0')] ).
cnf(434,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_range,u)
| icext(u,uri_rdfs_range) ),
inference(res,[status(thm),theory(equality)],[63,101]),
[iquote('0:Res:63.0,101.0')] ).
cnf(433,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_range,u)
| icext(u,uri_rdfs_isDefinedBy) ),
inference(res,[status(thm),theory(equality)],[31,101]),
[iquote('0:Res:31.0,101.0')] ).
cnf(432,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_range,u)
| icext(u,uri_rdfs_comment) ),
inference(res,[status(thm),theory(equality)],[29,101]),
[iquote('0:Res:29.0,101.0')] ).
cnf(431,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_range,u)
| icext(u,uri_rdfs_label) ),
inference(res,[status(thm),theory(equality)],[34,101]),
[iquote('0:Res:34.0,101.0')] ).
cnf(430,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_range,u)
| icext(u,uri_rdf_rest) ),
inference(res,[status(thm),theory(equality)],[40,101]),
[iquote('0:Res:40.0,101.0')] ).
cnf(827,plain,
iext(uri_rdf_type,uri_ex_d,uri_rdfs_Class),
inference(res,[status(thm),theory(equality)],[825,97]),
[iquote('0:Res:825.0,97.0')] ).
cnf(825,plain,
icext(uri_rdfs_Class,uri_ex_d),
inference(res,[status(thm),theory(equality)],[70,411]),
[iquote('0:Res:70.0,411.0')] ).
cnf(411,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_subClassOf,u)
| icext(u,uri_ex_d) ),
inference(res,[status(thm),theory(equality)],[8,101]),
[iquote('0:Res:8.0,101.0')] ).
cnf(410,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_subClassOf,u)
| icext(u,uri_rdfs_ContainerMembershipProperty) ),
inference(res,[status(thm),theory(equality)],[43,101]),
[iquote('0:Res:43.0,101.0')] ).
cnf(813,plain,
iext(uri_rdf_type,uri_rdf_Alt,uri_rdfs_Class),
inference(res,[status(thm),theory(equality)],[811,97]),
[iquote('0:Res:811.0,97.0')] ).
cnf(810,plain,
iext(uri_rdf_type,uri_rdf_Bag,uri_rdfs_Class),
inference(res,[status(thm),theory(equality)],[808,97]),
[iquote('0:Res:808.0,97.0')] ).
cnf(811,plain,
icext(uri_rdfs_Class,uri_rdf_Alt),
inference(res,[status(thm),theory(equality)],[70,409]),
[iquote('0:Res:70.0,409.0')] ).
cnf(409,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_subClassOf,u)
| icext(u,uri_rdf_Alt) ),
inference(res,[status(thm),theory(equality)],[41,101]),
[iquote('0:Res:41.0,101.0')] ).
cnf(808,plain,
icext(uri_rdfs_Class,uri_rdf_Bag),
inference(res,[status(thm),theory(equality)],[70,408]),
[iquote('0:Res:70.0,408.0')] ).
cnf(408,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_subClassOf,u)
| icext(u,uri_rdf_Bag) ),
inference(res,[status(thm),theory(equality)],[42,101]),
[iquote('0:Res:42.0,101.0')] ).
cnf(802,plain,
iext(uri_rdf_type,uri_rdfs_Seq,uri_rdfs_Class),
inference(res,[status(thm),theory(equality)],[800,97]),
[iquote('0:Res:800.0,97.0')] ).
cnf(800,plain,
icext(uri_rdfs_Class,uri_rdfs_Seq),
inference(res,[status(thm),theory(equality)],[70,407]),
[iquote('0:Res:70.0,407.0')] ).
cnf(407,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_subClassOf,u)
| icext(u,uri_rdfs_Seq) ),
inference(res,[status(thm),theory(equality)],[55,101]),
[iquote('0:Res:55.0,101.0')] ).
cnf(406,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_subClassOf,u)
| icext(u,uri_rdf_XMLLiteral) ),
inference(res,[status(thm),theory(equality)],[56,101]),
[iquote('0:Res:56.0,101.0')] ).
cnf(404,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_domain,u)
| icext(u,uri_rdf_first) ),
inference(res,[status(thm),theory(equality)],[37,101]),
[iquote('0:Res:37.0,101.0')] ).
cnf(792,plain,
ip(uri_rdfs_comment),
inference(res,[status(thm),theory(equality)],[790,87]),
[iquote('0:Res:790.0,87.0')] ).
cnf(790,plain,
iext(uri_rdf_type,uri_rdfs_comment,uri_rdf_Property),
inference(res,[status(thm),theory(equality)],[789,97]),
[iquote('0:Res:789.0,97.0')] ).
cnf(403,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_domain,u)
| icext(u,uri_rdf_rest) ),
inference(res,[status(thm),theory(equality)],[39,101]),
[iquote('0:Res:39.0,101.0')] ).
cnf(789,plain,
icext(uri_rdf_Property,uri_rdfs_comment),
inference(res,[status(thm),theory(equality)],[59,402]),
[iquote('0:Res:59.0,402.0')] ).
cnf(402,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_domain,u)
| icext(u,uri_rdfs_comment) ),
inference(res,[status(thm),theory(equality)],[28,101]),
[iquote('0:Res:28.0,101.0')] ).
cnf(782,plain,
iext(uri_rdf_type,uri_rdfs_isDefinedBy,uri_rdf_Property),
inference(res,[status(thm),theory(equality)],[781,97]),
[iquote('0:Res:781.0,97.0')] ).
cnf(781,plain,
icext(uri_rdf_Property,uri_rdfs_isDefinedBy),
inference(res,[status(thm),theory(equality)],[59,401]),
[iquote('0:Res:59.0,401.0')] ).
cnf(401,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_domain,u)
| icext(u,uri_rdfs_isDefinedBy) ),
inference(res,[status(thm),theory(equality)],[30,101]),
[iquote('0:Res:30.0,101.0')] ).
cnf(775,plain,
ip(uri_rdfs_label),
inference(res,[status(thm),theory(equality)],[774,87]),
[iquote('0:Res:774.0,87.0')] ).
cnf(774,plain,
iext(uri_rdf_type,uri_rdfs_label,uri_rdf_Property),
inference(res,[status(thm),theory(equality)],[773,97]),
[iquote('0:Res:773.0,97.0')] ).
cnf(773,plain,
icext(uri_rdf_Property,uri_rdfs_label),
inference(res,[status(thm),theory(equality)],[59,400]),
[iquote('0:Res:59.0,400.0')] ).
cnf(400,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_domain,u)
| icext(u,uri_rdfs_label) ),
inference(res,[status(thm),theory(equality)],[33,101]),
[iquote('0:Res:33.0,101.0')] ).
cnf(399,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_domain,u)
| icext(u,uri_rdfs_seeAlso) ),
inference(res,[status(thm),theory(equality)],[35,101]),
[iquote('0:Res:35.0,101.0')] ).
cnf(398,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_domain,u)
| icext(u,uri_rdfs_member) ),
inference(res,[status(thm),theory(equality)],[44,101]),
[iquote('0:Res:44.0,101.0')] ).
cnf(397,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_domain,u)
| icext(u,uri_rdf__1) ),
inference(res,[status(thm),theory(equality)],[46,101]),
[iquote('0:Res:46.0,101.0')] ).
cnf(396,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_domain,u)
| icext(u,uri_rdf__2) ),
inference(res,[status(thm),theory(equality)],[47,101]),
[iquote('0:Res:47.0,101.0')] ).
cnf(395,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_domain,u)
| icext(u,uri_rdf__3) ),
inference(res,[status(thm),theory(equality)],[48,101]),
[iquote('0:Res:48.0,101.0')] ).
cnf(394,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_domain,u)
| icext(u,uri_rdfs_domain) ),
inference(res,[status(thm),theory(equality)],[59,101]),
[iquote('0:Res:59.0,101.0')] ).
cnf(760,plain,
iext(uri_rdf_type,uri_rdfs_range,uri_rdf_Property),
inference(res,[status(thm),theory(equality)],[759,97]),
[iquote('0:Res:759.0,97.0')] ).
cnf(759,plain,
icext(uri_rdf_Property,uri_rdfs_range),
inference(res,[status(thm),theory(equality)],[59,393]),
[iquote('0:Res:59.0,393.0')] ).
cnf(393,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_domain,u)
| icext(u,uri_rdfs_range) ),
inference(res,[status(thm),theory(equality)],[62,101]),
[iquote('0:Res:62.0,101.0')] ).
cnf(392,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_domain,u)
| icext(u,uri_rdf_object) ),
inference(res,[status(thm),theory(equality)],[64,101]),
[iquote('0:Res:64.0,101.0')] ).
cnf(391,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_domain,u)
| icext(u,uri_rdf_predicate) ),
inference(res,[status(thm),theory(equality)],[66,101]),
[iquote('0:Res:66.0,101.0')] ).
cnf(390,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_domain,u)
| icext(u,uri_rdf_subject) ),
inference(res,[status(thm),theory(equality)],[68,101]),
[iquote('0:Res:68.0,101.0')] ).
cnf(389,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_subClassOf,u)
| icext(u,uri_rdfs_Datatype) ),
inference(res,[status(thm),theory(equality)],[58,101]),
[iquote('0:Res:58.0,101.0')] ).
cnf(748,plain,
iext(uri_rdf_type,uri_rdfs_domain,uri_rdf_Property),
inference(res,[status(thm),theory(equality)],[747,97]),
[iquote('0:Res:747.0,97.0')] ).
cnf(747,plain,
icext(uri_rdf_Property,uri_rdfs_domain),
inference(res,[status(thm),theory(equality)],[62,388]),
[iquote('0:Res:62.0,388.0')] ).
cnf(388,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_range,u)
| icext(u,uri_rdfs_domain) ),
inference(res,[status(thm),theory(equality)],[60,101]),
[iquote('0:Res:60.0,101.0')] ).
cnf(386,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_domain,u)
| icext(u,uri_rdfs_subClassOf) ),
inference(res,[status(thm),theory(equality)],[70,101]),
[iquote('0:Res:70.0,101.0')] ).
cnf(739,plain,
iext(uri_rdf_type,uri_rdfs_subClassOf,uri_rdf_Property),
inference(res,[status(thm),theory(equality)],[738,97]),
[iquote('0:Res:738.0,97.0')] ).
cnf(738,plain,
icext(uri_rdf_Property,uri_rdfs_subClassOf),
inference(res,[status(thm),theory(equality)],[62,385]),
[iquote('0:Res:62.0,385.0')] ).
cnf(385,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_range,u)
| icext(u,uri_rdfs_subClassOf) ),
inference(res,[status(thm),theory(equality)],[71,101]),
[iquote('0:Res:71.0,101.0')] ).
cnf(384,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_domain,u)
| icext(u,uri_rdfs_subPropertyOf) ),
inference(res,[status(thm),theory(equality)],[72,101]),
[iquote('0:Res:72.0,101.0')] ).
cnf(730,plain,
iext(uri_rdf_type,uri_rdfs_subPropertyOf,uri_rdf_Property),
inference(res,[status(thm),theory(equality)],[729,97]),
[iquote('0:Res:729.0,97.0')] ).
cnf(729,plain,
icext(uri_rdf_Property,uri_rdfs_subPropertyOf),
inference(res,[status(thm),theory(equality)],[62,383]),
[iquote('0:Res:62.0,383.0')] ).
cnf(383,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_range,u)
| icext(u,uri_rdfs_subPropertyOf) ),
inference(res,[status(thm),theory(equality)],[73,101]),
[iquote('0:Res:73.0,101.0')] ).
cnf(382,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_domain,u)
| icext(u,uri_rdf_type) ),
inference(res,[status(thm),theory(equality)],[74,101]),
[iquote('0:Res:74.0,101.0')] ).
cnf(381,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_range,u)
| icext(u,uri_rdf_type) ),
inference(res,[status(thm),theory(equality)],[75,101]),
[iquote('0:Res:75.0,101.0')] ).
cnf(380,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_range,u)
| icext(u,uri_rdfs_seeAlso) ),
inference(res,[status(thm),theory(equality)],[36,101]),
[iquote('0:Res:36.0,101.0')] ).
cnf(379,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_range,u)
| icext(u,uri_rdf_first) ),
inference(res,[status(thm),theory(equality)],[38,101]),
[iquote('0:Res:38.0,101.0')] ).
cnf(718,plain,
iext(uri_rdf_type,uri_rdfs_member,uri_rdf_Property),
inference(res,[status(thm),theory(equality)],[717,97]),
[iquote('0:Res:717.0,97.0')] ).
cnf(717,plain,
icext(uri_rdf_Property,uri_rdfs_member),
inference(res,[status(thm),theory(equality)],[62,378]),
[iquote('0:Res:62.0,378.0')] ).
cnf(378,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_range,u)
| icext(u,uri_rdfs_member) ),
inference(res,[status(thm),theory(equality)],[45,101]),
[iquote('0:Res:45.0,101.0')] ).
cnf(377,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_range,u)
| icext(u,uri_rdf__1) ),
inference(res,[status(thm),theory(equality)],[49,101]),
[iquote('0:Res:49.0,101.0')] ).
cnf(376,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_range,u)
| icext(u,uri_rdf__2) ),
inference(res,[status(thm),theory(equality)],[50,101]),
[iquote('0:Res:50.0,101.0')] ).
cnf(709,plain,
ip(uri_rdf_predicate),
inference(res,[status(thm),theory(equality)],[707,87]),
[iquote('0:Res:707.0,87.0')] ).
cnf(707,plain,
iext(uri_rdf_type,uri_rdf_predicate,uri_rdf_Property),
inference(res,[status(thm),theory(equality)],[706,97]),
[iquote('0:Res:706.0,97.0')] ).
cnf(375,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_range,u)
| icext(u,uri_rdf__3) ),
inference(res,[status(thm),theory(equality)],[51,101]),
[iquote('0:Res:51.0,101.0')] ).
cnf(706,plain,
icext(uri_rdf_Property,uri_rdf_predicate),
inference(res,[status(thm),theory(equality)],[62,374]),
[iquote('0:Res:62.0,374.0')] ).
cnf(374,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_range,u)
| icext(u,uri_rdf_predicate) ),
inference(res,[status(thm),theory(equality)],[67,101]),
[iquote('0:Res:67.0,101.0')] ).
cnf(373,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_range,u)
| icext(u,uri_rdf_subject) ),
inference(res,[status(thm),theory(equality)],[69,101]),
[iquote('0:Res:69.0,101.0')] ).
cnf(372,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_domain,u)
| icext(u,uri_rdf_value) ),
inference(res,[status(thm),theory(equality)],[76,101]),
[iquote('0:Res:76.0,101.0')] ).
cnf(371,plain,
( ~ iext(uri_rdfs_domain,uri_rdfs_range,u)
| icext(u,uri_rdf_value) ),
inference(res,[status(thm),theory(equality)],[77,101]),
[iquote('0:Res:77.0,101.0')] ).
cnf(366,plain,
( ~ iext(uri_rdfs_range,uri_owl_unionOf,u)
| icext(u,skc13) ),
inference(res,[status(thm),theory(equality)],[2,102]),
[iquote('0:Res:2.0,102.0')] ).
cnf(692,plain,
iext(uri_rdf_type,skc12,uri_rdf_List),
inference(res,[status(thm),theory(equality)],[691,97]),
[iquote('0:Res:691.0,97.0')] ).
cnf(690,plain,
iext(uri_rdf_type,skc11,uri_rdf_List),
inference(res,[status(thm),theory(equality)],[689,97]),
[iquote('0:Res:689.0,97.0')] ).
cnf(691,plain,
icext(uri_rdf_List,skc12),
inference(res,[status(thm),theory(equality)],[40,365]),
[iquote('0:Res:40.0,365.0')] ).
cnf(365,plain,
( ~ iext(uri_rdfs_range,uri_rdf_rest,u)
| icext(u,skc12) ),
inference(res,[status(thm),theory(equality)],[4,102]),
[iquote('0:Res:4.0,102.0')] ).
cnf(689,plain,
icext(uri_rdf_List,skc11),
inference(res,[status(thm),theory(equality)],[40,364]),
[iquote('0:Res:40.0,364.0')] ).
cnf(364,plain,
( ~ iext(uri_rdfs_range,uri_rdf_rest,u)
| icext(u,skc11) ),
inference(res,[status(thm),theory(equality)],[5,102]),
[iquote('0:Res:5.0,102.0')] ).
cnf(363,plain,
( ~ iext(uri_rdfs_range,uri_rdf_first,u)
| icext(u,uri_ex_c2) ),
inference(res,[status(thm),theory(equality)],[6,102]),
[iquote('0:Res:6.0,102.0')] ).
cnf(362,plain,
( ~ iext(uri_rdfs_range,uri_owl_complementOf,u)
| icext(u,uri_ex_c2) ),
inference(res,[status(thm),theory(equality)],[7,102]),
[iquote('0:Res:7.0,102.0')] ).
cnf(361,plain,
( ~ iext(uri_rdfs_range,uri_owl_intersectionOf,u)
| icext(u,skc8) ),
inference(res,[status(thm),theory(equality)],[9,102]),
[iquote('0:Res:9.0,102.0')] ).
cnf(682,plain,
iext(uri_rdf_type,skc7,uri_rdf_List),
inference(res,[status(thm),theory(equality)],[681,97]),
[iquote('0:Res:681.0,97.0')] ).
cnf(681,plain,
icext(uri_rdf_List,skc7),
inference(res,[status(thm),theory(equality)],[40,360]),
[iquote('0:Res:40.0,360.0')] ).
cnf(360,plain,
( ~ iext(uri_rdfs_range,uri_rdf_rest,u)
| icext(u,skc7) ),
inference(res,[status(thm),theory(equality)],[10,102]),
[iquote('0:Res:10.0,102.0')] ).
cnf(359,plain,
( ~ iext(uri_rdfs_range,uri_rdf_first,u)
| icext(u,uri_ex_c) ),
inference(res,[status(thm),theory(equality)],[11,102]),
[iquote('0:Res:11.0,102.0')] ).
cnf(358,plain,
( ~ iext(uri_rdfs_range,uri_rdf_first,u)
| icext(u,skc10) ),
inference(res,[status(thm),theory(equality)],[12,102]),
[iquote('0:Res:12.0,102.0')] ).
cnf(356,plain,
( ~ iext(uri_rdfs_range,uri_rdf_first,u)
| icext(u,uri_ex_c3) ),
inference(res,[status(thm),theory(equality)],[14,102]),
[iquote('0:Res:14.0,102.0')] ).
cnf(355,plain,
( ~ iext(uri_rdfs_range,uri_rdf_rest,u)
| icext(u,uri_rdf_nil) ),
inference(res,[status(thm),theory(equality)],[15,102]),
[iquote('0:Res:15.0,102.0')] ).
cnf(354,plain,
( ~ iext(uri_rdfs_range,uri_rdf_first,u)
| icext(u,uri_ex_c1) ),
inference(res,[status(thm),theory(equality)],[3,102]),
[iquote('0:Res:3.0,102.0')] ).
cnf(669,plain,
iext(uri_rdf_type,uri_rdfs_seeAlso,uri_rdf_Property),
inference(res,[status(thm),theory(equality)],[668,97]),
[iquote('0:Res:668.0,97.0')] ).
cnf(353,plain,
( ~ iext(uri_rdfs_range,uri_owl_disjointWith,u)
| icext(u,uri_ex_c1) ),
inference(res,[status(thm),theory(equality)],[16,102]),
[iquote('0:Res:16.0,102.0')] ).
cnf(668,plain,
icext(uri_rdf_Property,uri_rdfs_seeAlso),
inference(res,[status(thm),theory(equality)],[73,351]),
[iquote('0:Res:73.0,351.0')] ).
cnf(351,plain,
( ~ iext(uri_rdfs_range,uri_rdfs_subPropertyOf,u)
| icext(u,uri_rdfs_seeAlso) ),
inference(res,[status(thm),theory(equality)],[32,102]),
[iquote('0:Res:32.0,102.0')] ).
cnf(347,plain,
( ~ iext(uri_rdfs_range,uri_rdfs_range,u)
| icext(u,uri_rdfs_Literal) ),
inference(res,[status(thm),theory(equality)],[34,102]),
[iquote('0:Res:34.0,102.0')] ).
cnf(344,plain,
( ~ iext(uri_rdfs_range,uri_rdf_type,u)
| icext(u,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[230,102]),
[iquote('0:Res:230.0,102.0')] ).
cnf(346,plain,
( ~ iext(uri_rdfs_range,uri_rdfs_range,u)
| icext(u,uri_rdf_List) ),
inference(res,[status(thm),theory(equality)],[40,102]),
[iquote('0:Res:40.0,102.0')] ).
cnf(343,plain,
( ~ iext(uri_rdfs_range,uri_rdf_type,u)
| icext(u,uri_rdf_List) ),
inference(res,[status(thm),theory(equality)],[18,102]),
[iquote('0:Res:18.0,102.0')] ).
cnf(333,plain,
( ~ iext(uri_rdfs_range,uri_rdf_type,u)
| icext(u,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[25,102]),
[iquote('0:Res:25.0,102.0')] ).
cnf(657,plain,
iext(uri_rdf_type,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Class),
inference(res,[status(thm),theory(equality)],[655,97]),
[iquote('0:Res:655.0,97.0')] ).
cnf(655,plain,
icext(uri_rdfs_Class,uri_rdfs_ContainerMembershipProperty),
inference(res,[status(thm),theory(equality)],[75,330]),
[iquote('0:Res:75.0,330.0')] ).
cnf(330,plain,
( ~ iext(uri_rdfs_range,uri_rdf_type,u)
| icext(u,uri_rdfs_ContainerMembershipProperty) ),
inference(res,[status(thm),theory(equality)],[54,102]),
[iquote('0:Res:54.0,102.0')] ).
cnf(649,plain,
iext(uri_rdf_type,skc9,uri_rdfs_Class),
inference(res,[status(thm),theory(equality)],[647,97]),
[iquote('0:Res:647.0,97.0')] ).
cnf(647,plain,
icext(uri_rdfs_Class,skc9),
inference(res,[status(thm),theory(equality)],[71,327]),
[iquote('0:Res:71.0,327.0')] ).
cnf(327,plain,
( ~ iext(uri_rdfs_range,uri_rdfs_subClassOf,u)
| icext(u,skc9) ),
inference(res,[status(thm),theory(equality)],[8,102]),
[iquote('0:Res:8.0,102.0')] ).
cnf(640,plain,
iext(uri_rdf_type,uri_rdfs_Container,uri_rdfs_Class),
inference(res,[status(thm),theory(equality)],[638,97]),
[iquote('0:Res:638.0,97.0')] ).
cnf(326,plain,
( ~ iext(uri_rdfs_range,uri_rdfs_subClassOf,u)
| icext(u,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[43,102]),
[iquote('0:Res:43.0,102.0')] ).
cnf(638,plain,
icext(uri_rdfs_Class,uri_rdfs_Container),
inference(res,[status(thm),theory(equality)],[71,323]),
[iquote('0:Res:71.0,323.0')] ).
cnf(323,plain,
( ~ iext(uri_rdfs_range,uri_rdfs_subClassOf,u)
| icext(u,uri_rdfs_Container) ),
inference(res,[status(thm),theory(equality)],[55,102]),
[iquote('0:Res:55.0,102.0')] ).
cnf(632,plain,
iext(uri_rdf_type,uri_rdfs_Literal,uri_rdfs_Class),
inference(res,[status(thm),theory(equality)],[630,97]),
[iquote('0:Res:630.0,97.0')] ).
cnf(630,plain,
icext(uri_rdfs_Class,uri_rdfs_Literal),
inference(res,[status(thm),theory(equality)],[71,322]),
[iquote('0:Res:71.0,322.0')] ).
cnf(322,plain,
( ~ iext(uri_rdfs_range,uri_rdfs_subClassOf,u)
| icext(u,uri_rdfs_Literal) ),
inference(res,[status(thm),theory(equality)],[56,102]),
[iquote('0:Res:56.0,102.0')] ).
cnf(614,plain,
iext(uri_rdf_type,uri_rdfs_Datatype,uri_rdfs_Class),
inference(res,[status(thm),theory(equality)],[612,97]),
[iquote('0:Res:612.0,97.0')] ).
cnf(611,plain,
iext(uri_rdf_type,uri_rdf_List,uri_rdfs_Class),
inference(res,[status(thm),theory(equality)],[607,97]),
[iquote('0:Res:607.0,97.0')] ).
cnf(609,plain,
iext(uri_rdf_type,uri_rdfs_Statement,uri_rdfs_Class),
inference(res,[status(thm),theory(equality)],[606,97]),
[iquote('0:Res:606.0,97.0')] ).
cnf(612,plain,
icext(uri_rdfs_Class,uri_rdfs_Datatype),
inference(res,[status(thm),theory(equality)],[75,321]),
[iquote('0:Res:75.0,321.0')] ).
cnf(321,plain,
( ~ iext(uri_rdfs_range,uri_rdf_type,u)
| icext(u,uri_rdfs_Datatype) ),
inference(res,[status(thm),theory(equality)],[57,102]),
[iquote('0:Res:57.0,102.0')] ).
cnf(610,plain,
ic(uri_rdf_List),
inference(res,[status(thm),theory(equality)],[607,81]),
[iquote('0:Res:607.0,81.0')] ).
cnf(607,plain,
icext(uri_rdfs_Class,uri_rdf_List),
inference(res,[status(thm),theory(equality)],[60,319]),
[iquote('0:Res:60.0,319.0')] ).
cnf(608,plain,
ic(uri_rdfs_Statement),
inference(res,[status(thm),theory(equality)],[606,81]),
[iquote('0:Res:606.0,81.0')] ).
cnf(606,plain,
icext(uri_rdfs_Class,uri_rdfs_Statement),
inference(res,[status(thm),theory(equality)],[60,306]),
[iquote('0:Res:60.0,306.0')] ).
cnf(319,plain,
( ~ iext(uri_rdfs_range,uri_rdfs_domain,u)
| icext(u,uri_rdf_List) ),
inference(res,[status(thm),theory(equality)],[39,102]),
[iquote('0:Res:39.0,102.0')] ).
cnf(306,plain,
( ~ iext(uri_rdfs_range,uri_rdfs_domain,u)
| icext(u,uri_rdfs_Statement) ),
inference(res,[status(thm),theory(equality)],[68,102]),
[iquote('0:Res:68.0,102.0')] ).
cnf(305,plain,
( ~ iext(uri_rdfs_range,uri_rdfs_subClassOf,u)
| icext(u,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[58,102]),
[iquote('0:Res:58.0,102.0')] ).
cnf(303,plain,
( ~ iext(uri_rdfs_range,uri_rdf_type,u)
| icext(u,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[61,102]),
[iquote('0:Res:61.0,102.0')] ).
cnf(302,plain,
( ~ iext(uri_rdfs_range,uri_rdfs_domain,u)
| icext(u,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[70,102]),
[iquote('0:Res:70.0,102.0')] ).
cnf(300,plain,
( ~ iext(uri_rdfs_range,uri_rdfs_domain,u)
| icext(u,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[72,102]),
[iquote('0:Res:72.0,102.0')] ).
cnf(299,plain,
( ~ iext(uri_rdfs_range,uri_rdfs_range,u)
| icext(u,uri_rdf_Property) ),
inference(res,[status(thm),theory(equality)],[73,102]),
[iquote('0:Res:73.0,102.0')] ).
cnf(595,plain,
iext(uri_rdf_type,uri_rdfs_Class,uri_rdfs_Class),
inference(res,[status(thm),theory(equality)],[593,97]),
[iquote('0:Res:593.0,97.0')] ).
cnf(593,plain,
icext(uri_rdfs_Class,uri_rdfs_Class),
inference(res,[status(thm),theory(equality)],[63,297]),
[iquote('0:Res:63.0,297.0')] ).
cnf(297,plain,
( ~ iext(uri_rdfs_range,uri_rdfs_range,u)
| icext(u,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[75,102]),
[iquote('0:Res:75.0,102.0')] ).
cnf(288,plain,
( ~ iext(uri_rdfs_range,uri_rdfs_domain,u)
| icext(u,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[76,102]),
[iquote('0:Res:76.0,102.0')] ).
cnf(586,plain,
iext(uri_rdf_type,uri_rdfs_Resource,uri_rdfs_Class),
inference(res,[status(thm),theory(equality)],[584,97]),
[iquote('0:Res:584.0,97.0')] ).
cnf(584,plain,
icext(uri_rdfs_Class,uri_rdfs_Resource),
inference(res,[status(thm),theory(equality)],[63,287]),
[iquote('0:Res:63.0,287.0')] ).
cnf(287,plain,
( ~ iext(uri_rdfs_range,uri_rdfs_range,u)
| icext(u,uri_rdfs_Resource) ),
inference(res,[status(thm),theory(equality)],[77,102]),
[iquote('0:Res:77.0,102.0')] ).
cnf(279,plain,
( ~ icext(uri_ex_d,u)
| icext(skc9,u) ),
inference(res,[status(thm),theory(equality)],[8,100]),
[iquote('0:Res:8.0,100.1')] ).
cnf(278,plain,
( ~ icext(uri_rdfs_ContainerMembershipProperty,u)
| icext(uri_rdf_Property,u) ),
inference(res,[status(thm),theory(equality)],[43,100]),
[iquote('0:Res:43.0,100.1')] ).
cnf(277,plain,
( ~ icext(uri_rdf_Alt,u)
| icext(uri_rdfs_Container,u) ),
inference(res,[status(thm),theory(equality)],[41,100]),
[iquote('0:Res:41.0,100.1')] ).
cnf(276,plain,
( ~ icext(uri_rdf_Bag,u)
| icext(uri_rdfs_Container,u) ),
inference(res,[status(thm),theory(equality)],[42,100]),
[iquote('0:Res:42.0,100.1')] ).
cnf(275,plain,
( ~ icext(uri_rdfs_Seq,u)
| icext(uri_rdfs_Container,u) ),
inference(res,[status(thm),theory(equality)],[55,100]),
[iquote('0:Res:55.0,100.1')] ).
cnf(274,plain,
( ~ icext(uri_rdf_XMLLiteral,u)
| icext(uri_rdfs_Literal,u) ),
inference(res,[status(thm),theory(equality)],[56,100]),
[iquote('0:Res:56.0,100.1')] ).
cnf(104,axiom,
( ~ iext(u,v,w)
| ~ iext(uri_rdfs_subPropertyOf,u,x)
| iext(x,v,w) ),
file('SWB020+4.p',unknown),
[] ).
cnf(491,plain,
iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Class),
inference(res,[status(thm),theory(equality)],[489,97]),
[iquote('0:Res:489.0,97.0')] ).
cnf(489,plain,
icext(uri_rdfs_Class,uri_rdf_XMLLiteral),
inference(res,[status(thm),theory(equality)],[248,273]),
[iquote('0:Res:248.0,273.0')] ).
cnf(273,plain,
( ~ icext(uri_rdfs_Datatype,u)
| icext(uri_rdfs_Class,u) ),
inference(res,[status(thm),theory(equality)],[58,100]),
[iquote('0:Res:58.0,100.1')] ).
cnf(232,plain,
( ~ ic(u)
| iext(uri_rdf_type,u,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[80,97]),
[iquote('0:Res:80.1,97.0')] ).
cnf(103,axiom,
( ~ iext(uri_rdfs_subClassOf,u,v)
| ~ iext(uri_rdfs_subClassOf,w,u)
| iext(uri_rdfs_subClassOf,w,v) ),
file('SWB020+4.p',unknown),
[] ).
cnf(261,plain,
( ~ ip(u)
| icext(uri_rdf_Property,u) ),
inference(res,[status(thm),theory(equality)],[88,96]),
[iquote('0:Res:88.1,96.0')] ).
cnf(282,plain,
iext(uri_rdfs_subPropertyOf,uri_rdf__1,uri_rdfs_member),
inference(res,[status(thm),theory(equality)],[251,98]),
[iquote('0:Res:251.0,98.0')] ).
cnf(271,plain,
iext(uri_rdfs_subPropertyOf,uri_rdf__2,uri_rdfs_member),
inference(res,[status(thm),theory(equality)],[250,98]),
[iquote('0:Res:250.0,98.0')] ).
cnf(455,plain,
ip(uri_rdfs_member),
inference(res,[status(thm),theory(equality)],[269,94]),
[iquote('0:Res:269.0,94.0')] ).
cnf(105,axiom,
( ~ iext(uri_rdfs_subPropertyOf,u,v)
| ~ iext(uri_rdfs_subPropertyOf,w,u)
| iext(uri_rdfs_subPropertyOf,w,v) ),
file('SWB020+4.p',unknown),
[] ).
cnf(269,plain,
iext(uri_rdfs_subPropertyOf,uri_rdf__3,uri_rdfs_member),
inference(res,[status(thm),theory(equality)],[249,98]),
[iquote('0:Res:249.0,98.0')] ).
cnf(262,plain,
icext(uri_rdf_List,uri_rdf_nil),
inference(res,[status(thm),theory(equality)],[18,96]),
[iquote('0:Res:18.0,96.0')] ).
cnf(260,plain,
icext(uri_rdf_Property,uri_rdf_type),
inference(res,[status(thm),theory(equality)],[27,96]),
[iquote('0:Res:27.0,96.0')] ).
cnf(259,plain,
icext(uri_rdf_Property,uri_rdf_first),
inference(res,[status(thm),theory(equality)],[17,96]),
[iquote('0:Res:17.0,96.0')] ).
cnf(101,axiom,
( ~ iext(u,v,w)
| ~ iext(uri_rdfs_domain,u,x)
| icext(x,v) ),
file('SWB020+4.p',unknown),
[] ).
cnf(258,plain,
icext(uri_rdf_Property,uri_rdf_rest),
inference(res,[status(thm),theory(equality)],[19,96]),
[iquote('0:Res:19.0,96.0')] ).
cnf(257,plain,
icext(uri_rdf_Property,uri_rdf__1),
inference(res,[status(thm),theory(equality)],[20,96]),
[iquote('0:Res:20.0,96.0')] ).
cnf(256,plain,
icext(uri_rdf_Property,uri_rdf__2),
inference(res,[status(thm),theory(equality)],[21,96]),
[iquote('0:Res:21.0,96.0')] ).
cnf(255,plain,
icext(uri_rdf_Property,uri_rdf__3),
inference(res,[status(thm),theory(equality)],[22,96]),
[iquote('0:Res:22.0,96.0')] ).
cnf(102,axiom,
( ~ iext(u,v,w)
| ~ iext(uri_rdfs_range,u,x)
| icext(x,w) ),
file('SWB020+4.p',unknown),
[] ).
cnf(254,plain,
icext(uri_rdf_Property,uri_rdf_object),
inference(res,[status(thm),theory(equality)],[23,96]),
[iquote('0:Res:23.0,96.0')] ).
cnf(253,plain,
icext(uri_rdf_Property,uri_rdf_value),
inference(res,[status(thm),theory(equality)],[24,96]),
[iquote('0:Res:24.0,96.0')] ).
cnf(252,plain,
icext(uri_rdf_Property,uri_rdf_subject),
inference(res,[status(thm),theory(equality)],[25,96]),
[iquote('0:Res:25.0,96.0')] ).
cnf(251,plain,
icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__1),
inference(res,[status(thm),theory(equality)],[52,96]),
[iquote('0:Res:52.0,96.0')] ).
cnf(100,axiom,
( ~ icext(u,v)
| ~ iext(uri_rdfs_subClassOf,u,w)
| icext(w,v) ),
file('SWB020+4.p',unknown),
[] ).
cnf(250,plain,
icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__2),
inference(res,[status(thm),theory(equality)],[53,96]),
[iquote('0:Res:53.0,96.0')] ).
cnf(249,plain,
icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__3),
inference(res,[status(thm),theory(equality)],[54,96]),
[iquote('0:Res:54.0,96.0')] ).
cnf(248,plain,
icext(uri_rdfs_Datatype,uri_rdf_XMLLiteral),
inference(res,[status(thm),theory(equality)],[57,96]),
[iquote('0:Res:57.0,96.0')] ).
cnf(247,plain,
icext(uri_rdfs_Class,uri_rdf_Property),
inference(res,[status(thm),theory(equality)],[61,96]),
[iquote('0:Res:61.0,96.0')] ).
cnf(96,axiom,
( ~ iext(uri_rdf_type,u,v)
| icext(v,u) ),
file('SWB020+4.p',unknown),
[] ).
cnf(231,plain,
( ~ lv(u)
| iext(uri_rdf_type,u,uri_rdfs_Literal) ),
inference(res,[status(thm),theory(equality)],[84,97]),
[iquote('0:Res:84.1,97.0')] ).
cnf(234,plain,
ic(uri_rdfs_Resource),
inference(ems,[status(thm)],[141,149]),
[iquote('0:EmS:141.0,149.0')] ).
cnf(230,plain,
iext(uri_rdf_type,u,uri_rdfs_Resource),
inference(res,[status(thm),theory(equality)],[106,97]),
[iquote('0:Res:106.0,97.0')] ).
cnf(97,axiom,
( ~ icext(u,v)
| iext(uri_rdf_type,v,u) ),
file('SWB020+4.p',unknown),
[] ).
cnf(229,plain,
ip(uri_owl_unionOf),
inference(res,[status(thm),theory(equality)],[2,86]),
[iquote('0:Res:2.0,86.0')] ).
cnf(225,plain,
ip(uri_owl_complementOf),
inference(res,[status(thm),theory(equality)],[7,86]),
[iquote('0:Res:7.0,86.0')] ).
cnf(224,plain,
ip(uri_owl_intersectionOf),
inference(res,[status(thm),theory(equality)],[9,86]),
[iquote('0:Res:9.0,86.0')] ).
cnf(216,plain,
ip(uri_owl_disjointWith),
inference(res,[status(thm),theory(equality)],[16,86]),
[iquote('0:Res:16.0,86.0')] ).
cnf(98,axiom,
( ~ icext(uri_rdfs_ContainerMembershipProperty,u)
| iext(uri_rdfs_subPropertyOf,u,uri_rdfs_member) ),
file('SWB020+4.p',unknown),
[] ).
cnf(214,plain,
ip(uri_rdfs_subPropertyOf),
inference(res,[status(thm),theory(equality)],[32,86]),
[iquote('0:Res:32.0,86.0')] ).
cnf(170,plain,
ip(uri_rdfs_subClassOf),
inference(res,[status(thm),theory(equality)],[58,86]),
[iquote('0:Res:58.0,86.0')] ).
cnf(153,plain,
ip(uri_rdfs_domain),
inference(res,[status(thm),theory(equality)],[76,86]),
[iquote('0:Res:76.0,86.0')] ).
cnf(152,plain,
ip(uri_rdfs_range),
inference(res,[status(thm),theory(equality)],[77,86]),
[iquote('0:Res:77.0,86.0')] ).
cnf(99,axiom,
( ~ icext(uri_rdfs_Datatype,u)
| iext(uri_rdfs_subClassOf,u,uri_rdfs_Literal) ),
file('SWB020+4.p',unknown),
[] ).
cnf(149,plain,
ic(uri_ex_d),
inference(res,[status(thm),theory(equality)],[8,90]),
[iquote('0:Res:8.0,90.0')] ).
cnf(148,plain,
ic(uri_rdfs_ContainerMembershipProperty),
inference(res,[status(thm),theory(equality)],[43,90]),
[iquote('0:Res:43.0,90.0')] ).
cnf(147,plain,
ic(uri_rdf_Alt),
inference(res,[status(thm),theory(equality)],[41,90]),
[iquote('0:Res:41.0,90.0')] ).
cnf(146,plain,
ic(uri_rdf_Bag),
inference(res,[status(thm),theory(equality)],[42,90]),
[iquote('0:Res:42.0,90.0')] ).
cnf(86,axiom,
( ~ iext(u,v,w)
| ip(u) ),
file('SWB020+4.p',unknown),
[] ).
cnf(145,plain,
ic(uri_rdfs_Seq),
inference(res,[status(thm),theory(equality)],[55,90]),
[iquote('0:Res:55.0,90.0')] ).
cnf(144,plain,
ic(uri_rdf_XMLLiteral),
inference(res,[status(thm),theory(equality)],[56,90]),
[iquote('0:Res:56.0,90.0')] ).
cnf(143,plain,
ic(uri_rdfs_Datatype),
inference(res,[status(thm),theory(equality)],[58,90]),
[iquote('0:Res:58.0,90.0')] ).
cnf(140,plain,
ic(skc9),
inference(res,[status(thm),theory(equality)],[8,91]),
[iquote('0:Res:8.0,91.0')] ).
cnf(90,axiom,
( ~ iext(uri_rdfs_subClassOf,u,v)
| ic(u) ),
file('SWB020+4.p',unknown),
[] ).
cnf(139,plain,
ic(uri_rdf_Property),
inference(res,[status(thm),theory(equality)],[43,91]),
[iquote('0:Res:43.0,91.0')] ).
cnf(136,plain,
ic(uri_rdfs_Container),
inference(res,[status(thm),theory(equality)],[55,91]),
[iquote('0:Res:55.0,91.0')] ).
cnf(135,plain,
ic(uri_rdfs_Literal),
inference(res,[status(thm),theory(equality)],[56,91]),
[iquote('0:Res:56.0,91.0')] ).
cnf(134,plain,
ic(uri_rdfs_Class),
inference(res,[status(thm),theory(equality)],[58,91]),
[iquote('0:Res:58.0,91.0')] ).
cnf(91,axiom,
( ~ iext(uri_rdfs_subClassOf,u,v)
| ic(v) ),
file('SWB020+4.p',unknown),
[] ).
cnf(132,plain,
ip(uri_rdfs_isDefinedBy),
inference(res,[status(thm),theory(equality)],[32,93]),
[iquote('0:Res:32.0,93.0')] ).
cnf(93,axiom,
( ~ iext(uri_rdfs_subPropertyOf,u,v)
| ip(u) ),
file('SWB020+4.p',unknown),
[] ).
cnf(130,plain,
ip(uri_rdfs_seeAlso),
inference(res,[status(thm),theory(equality)],[32,94]),
[iquote('0:Res:32.0,94.0')] ).
cnf(128,plain,
ip(uri_rdf_type),
inference(res,[status(thm),theory(equality)],[27,87]),
[iquote('0:Res:27.0,87.0')] ).
cnf(94,axiom,
( ~ iext(uri_rdfs_subPropertyOf,u,v)
| ip(v) ),
file('SWB020+4.p',unknown),
[] ).
cnf(127,plain,
ip(uri_rdf_first),
inference(res,[status(thm),theory(equality)],[17,87]),
[iquote('0:Res:17.0,87.0')] ).
cnf(126,plain,
ip(uri_rdf_rest),
inference(res,[status(thm),theory(equality)],[19,87]),
[iquote('0:Res:19.0,87.0')] ).
cnf(125,plain,
ip(uri_rdf__1),
inference(res,[status(thm),theory(equality)],[20,87]),
[iquote('0:Res:20.0,87.0')] ).
cnf(124,plain,
ip(uri_rdf__2),
inference(res,[status(thm),theory(equality)],[21,87]),
[iquote('0:Res:21.0,87.0')] ).
cnf(92,axiom,
( ~ ic(u)
| iext(uri_rdfs_subClassOf,u,u) ),
file('SWB020+4.p',unknown),
[] ).
cnf(123,plain,
ip(uri_rdf__3),
inference(res,[status(thm),theory(equality)],[22,87]),
[iquote('0:Res:22.0,87.0')] ).
cnf(122,plain,
ip(uri_rdf_object),
inference(res,[status(thm),theory(equality)],[23,87]),
[iquote('0:Res:23.0,87.0')] ).
cnf(121,plain,
ip(uri_rdf_value),
inference(res,[status(thm),theory(equality)],[24,87]),
[iquote('0:Res:24.0,87.0')] ).
cnf(120,plain,
ip(uri_rdf_subject),
inference(res,[status(thm),theory(equality)],[25,87]),
[iquote('0:Res:25.0,87.0')] ).
cnf(95,axiom,
( ~ ip(u)
| iext(uri_rdfs_subPropertyOf,u,u) ),
file('SWB020+4.p',unknown),
[] ).
cnf(87,axiom,
( ~ iext(uri_rdf_type,u,uri_rdf_Property)
| ip(u) ),
file('SWB020+4.p',unknown),
[] ).
cnf(88,axiom,
( ~ ip(u)
| iext(uri_rdf_type,u,uri_rdf_Property) ),
file('SWB020+4.p',unknown),
[] ).
cnf(89,axiom,
( ~ ic(u)
| iext(uri_rdfs_subClassOf,u,uri_rdfs_Resource) ),
file('SWB020+4.p',unknown),
[] ).
cnf(81,axiom,
( ~ icext(uri_rdfs_Class,u)
| ic(u) ),
file('SWB020+4.p',unknown),
[] ).
cnf(85,axiom,
( ~ icext(uri_rdfs_Literal,u)
| lv(u) ),
file('SWB020+4.p',unknown),
[] ).
cnf(80,axiom,
( ~ ic(u)
| icext(uri_rdfs_Class,u) ),
file('SWB020+4.p',unknown),
[] ).
cnf(84,axiom,
( ~ lv(u)
| icext(uri_rdfs_Literal,u) ),
file('SWB020+4.p',unknown),
[] ).
cnf(78,axiom,
~ iext(uri_rdfs_subClassOf,uri_ex_d,uri_ex_c3),
file('SWB020+4.p',unknown),
[] ).
cnf(27,axiom,
iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property),
file('SWB020+4.p',unknown),
[] ).
cnf(59,axiom,
iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_Property),
file('SWB020+4.p',unknown),
[] ).
cnf(63,axiom,
iext(uri_rdfs_range,uri_rdfs_range,uri_rdfs_Class),
file('SWB020+4.p',unknown),
[] ).
cnf(2,axiom,
iext(uri_owl_unionOf,uri_ex_c,skc13),
file('SWB020+4.p',unknown),
[] ).
cnf(3,axiom,
iext(uri_rdf_first,skc13,uri_ex_c1),
file('SWB020+4.p',unknown),
[] ).
cnf(4,axiom,
iext(uri_rdf_rest,skc13,skc12),
file('SWB020+4.p',unknown),
[] ).
cnf(5,axiom,
iext(uri_rdf_rest,skc12,skc11),
file('SWB020+4.p',unknown),
[] ).
cnf(6,axiom,
iext(uri_rdf_first,skc12,uri_ex_c2),
file('SWB020+4.p',unknown),
[] ).
cnf(7,axiom,
iext(uri_owl_complementOf,skc10,uri_ex_c2),
file('SWB020+4.p',unknown),
[] ).
cnf(8,axiom,
iext(uri_rdfs_subClassOf,uri_ex_d,skc9),
file('SWB020+4.p',unknown),
[] ).
cnf(9,axiom,
iext(uri_owl_intersectionOf,skc9,skc8),
file('SWB020+4.p',unknown),
[] ).
cnf(10,axiom,
iext(uri_rdf_rest,skc8,skc7),
file('SWB020+4.p',unknown),
[] ).
cnf(11,axiom,
iext(uri_rdf_first,skc8,uri_ex_c),
file('SWB020+4.p',unknown),
[] ).
cnf(12,axiom,
iext(uri_rdf_first,skc7,skc10),
file('SWB020+4.p',unknown),
[] ).
cnf(13,axiom,
iext(uri_rdf_rest,skc7,uri_rdf_nil),
file('SWB020+4.p',unknown),
[] ).
cnf(14,axiom,
iext(uri_rdf_first,skc11,uri_ex_c3),
file('SWB020+4.p',unknown),
[] ).
cnf(15,axiom,
iext(uri_rdf_rest,skc11,uri_rdf_nil),
file('SWB020+4.p',unknown),
[] ).
cnf(16,axiom,
iext(uri_owl_disjointWith,uri_ex_d,uri_ex_c1),
file('SWB020+4.p',unknown),
[] ).
cnf(17,axiom,
iext(uri_rdf_type,uri_rdf_first,uri_rdf_Property),
file('SWB020+4.p',unknown),
[] ).
cnf(18,axiom,
iext(uri_rdf_type,uri_rdf_nil,uri_rdf_List),
file('SWB020+4.p',unknown),
[] ).
cnf(19,axiom,
iext(uri_rdf_type,uri_rdf_rest,uri_rdf_Property),
file('SWB020+4.p',unknown),
[] ).
cnf(20,axiom,
iext(uri_rdf_type,uri_rdf__1,uri_rdf_Property),
file('SWB020+4.p',unknown),
[] ).
cnf(21,axiom,
iext(uri_rdf_type,uri_rdf__2,uri_rdf_Property),
file('SWB020+4.p',unknown),
[] ).
cnf(22,axiom,
iext(uri_rdf_type,uri_rdf__3,uri_rdf_Property),
file('SWB020+4.p',unknown),
[] ).
cnf(23,axiom,
iext(uri_rdf_type,uri_rdf_object,uri_rdf_Property),
file('SWB020+4.p',unknown),
[] ).
cnf(24,axiom,
iext(uri_rdf_type,uri_rdf_value,uri_rdf_Property),
file('SWB020+4.p',unknown),
[] ).
cnf(25,axiom,
iext(uri_rdf_type,uri_rdf_subject,uri_rdf_Property),
file('SWB020+4.p',unknown),
[] ).
cnf(28,axiom,
iext(uri_rdfs_domain,uri_rdfs_comment,uri_rdfs_Resource),
file('SWB020+4.p',unknown),
[] ).
cnf(29,axiom,
iext(uri_rdfs_range,uri_rdfs_comment,uri_rdfs_Literal),
file('SWB020+4.p',unknown),
[] ).
cnf(30,axiom,
iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,uri_rdfs_Resource),
file('SWB020+4.p',unknown),
[] ).
cnf(31,axiom,
iext(uri_rdfs_range,uri_rdfs_isDefinedBy,uri_rdfs_Resource),
file('SWB020+4.p',unknown),
[] ).
cnf(32,axiom,
iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),
file('SWB020+4.p',unknown),
[] ).
cnf(33,axiom,
iext(uri_rdfs_domain,uri_rdfs_label,uri_rdfs_Resource),
file('SWB020+4.p',unknown),
[] ).
cnf(34,axiom,
iext(uri_rdfs_range,uri_rdfs_label,uri_rdfs_Literal),
file('SWB020+4.p',unknown),
[] ).
cnf(35,axiom,
iext(uri_rdfs_domain,uri_rdfs_seeAlso,uri_rdfs_Resource),
file('SWB020+4.p',unknown),
[] ).
cnf(36,axiom,
iext(uri_rdfs_range,uri_rdfs_seeAlso,uri_rdfs_Resource),
file('SWB020+4.p',unknown),
[] ).
cnf(37,axiom,
iext(uri_rdfs_domain,uri_rdf_first,uri_rdf_List),
file('SWB020+4.p',unknown),
[] ).
cnf(38,axiom,
iext(uri_rdfs_range,uri_rdf_first,uri_rdfs_Resource),
file('SWB020+4.p',unknown),
[] ).
cnf(39,axiom,
iext(uri_rdfs_domain,uri_rdf_rest,uri_rdf_List),
file('SWB020+4.p',unknown),
[] ).
cnf(40,axiom,
iext(uri_rdfs_range,uri_rdf_rest,uri_rdf_List),
file('SWB020+4.p',unknown),
[] ).
cnf(41,axiom,
iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Container),
file('SWB020+4.p',unknown),
[] ).
cnf(42,axiom,
iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Container),
file('SWB020+4.p',unknown),
[] ).
cnf(43,axiom,
iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),
file('SWB020+4.p',unknown),
[] ).
cnf(44,axiom,
iext(uri_rdfs_domain,uri_rdfs_member,uri_rdfs_Resource),
file('SWB020+4.p',unknown),
[] ).
cnf(45,axiom,
iext(uri_rdfs_range,uri_rdfs_member,uri_rdfs_Resource),
file('SWB020+4.p',unknown),
[] ).
cnf(46,axiom,
iext(uri_rdfs_domain,uri_rdf__1,uri_rdfs_Resource),
file('SWB020+4.p',unknown),
[] ).
cnf(47,axiom,
iext(uri_rdfs_domain,uri_rdf__2,uri_rdfs_Resource),
file('SWB020+4.p',unknown),
[] ).
cnf(48,axiom,
iext(uri_rdfs_domain,uri_rdf__3,uri_rdfs_Resource),
file('SWB020+4.p',unknown),
[] ).
cnf(49,axiom,
iext(uri_rdfs_range,uri_rdf__1,uri_rdfs_Resource),
file('SWB020+4.p',unknown),
[] ).
cnf(50,axiom,
iext(uri_rdfs_range,uri_rdf__2,uri_rdfs_Resource),
file('SWB020+4.p',unknown),
[] ).
cnf(51,axiom,
iext(uri_rdfs_range,uri_rdf__3,uri_rdfs_Resource),
file('SWB020+4.p',unknown),
[] ).
cnf(52,axiom,
iext(uri_rdf_type,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),
file('SWB020+4.p',unknown),
[] ).
cnf(53,axiom,
iext(uri_rdf_type,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),
file('SWB020+4.p',unknown),
[] ).
cnf(54,axiom,
iext(uri_rdf_type,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),
file('SWB020+4.p',unknown),
[] ).
cnf(55,axiom,
iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Container),
file('SWB020+4.p',unknown),
[] ).
cnf(56,axiom,
iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Literal),
file('SWB020+4.p',unknown),
[] ).
cnf(57,axiom,
iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Datatype),
file('SWB020+4.p',unknown),
[] ).
cnf(58,axiom,
iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Class),
file('SWB020+4.p',unknown),
[] ).
cnf(60,axiom,
iext(uri_rdfs_range,uri_rdfs_domain,uri_rdfs_Class),
file('SWB020+4.p',unknown),
[] ).
cnf(61,axiom,
iext(uri_rdf_type,uri_rdf_Property,uri_rdfs_Class),
file('SWB020+4.p',unknown),
[] ).
cnf(62,axiom,
iext(uri_rdfs_domain,uri_rdfs_range,uri_rdf_Property),
file('SWB020+4.p',unknown),
[] ).
cnf(64,axiom,
iext(uri_rdfs_domain,uri_rdf_object,uri_rdfs_Statement),
file('SWB020+4.p',unknown),
[] ).
cnf(66,axiom,
iext(uri_rdfs_domain,uri_rdf_predicate,uri_rdfs_Statement),
file('SWB020+4.p',unknown),
[] ).
cnf(67,axiom,
iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Resource),
file('SWB020+4.p',unknown),
[] ).
cnf(68,axiom,
iext(uri_rdfs_domain,uri_rdf_subject,uri_rdfs_Statement),
file('SWB020+4.p',unknown),
[] ).
cnf(69,axiom,
iext(uri_rdfs_range,uri_rdf_subject,uri_rdfs_Resource),
file('SWB020+4.p',unknown),
[] ).
cnf(70,axiom,
iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdfs_Class),
file('SWB020+4.p',unknown),
[] ).
cnf(71,axiom,
iext(uri_rdfs_range,uri_rdfs_subClassOf,uri_rdfs_Class),
file('SWB020+4.p',unknown),
[] ).
cnf(72,axiom,
iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdf_Property),
file('SWB020+4.p',unknown),
[] ).
cnf(73,axiom,
iext(uri_rdfs_range,uri_rdfs_subPropertyOf,uri_rdf_Property),
file('SWB020+4.p',unknown),
[] ).
cnf(74,axiom,
iext(uri_rdfs_domain,uri_rdf_type,uri_rdfs_Resource),
file('SWB020+4.p',unknown),
[] ).
cnf(75,axiom,
iext(uri_rdfs_range,uri_rdf_type,uri_rdfs_Class),
file('SWB020+4.p',unknown),
[] ).
cnf(76,axiom,
iext(uri_rdfs_domain,uri_rdf_value,uri_rdfs_Resource),
file('SWB020+4.p',unknown),
[] ).
cnf(77,axiom,
iext(uri_rdfs_range,uri_rdf_value,uri_rdfs_Resource),
file('SWB020+4.p',unknown),
[] ).
cnf(106,plain,
icext(uri_rdfs_Resource,u),
inference(mrr,[status(thm)],[82,1]),
[iquote('0:MRR:82.0,1.0')] ).
cnf(1,axiom,
ir(u),
file('SWB020+4.p',unknown),
[] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : SWB020+4 : TPTP v8.1.0. Released v5.2.0.
% 0.03/0.14 % 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 08:47:00 EDT 2022
% 0.13/0.35 % CPUTime :
% 0.21/0.50
% 0.21/0.50 SPASS V 3.9
% 0.21/0.50 SPASS beiseite: Completion found.
% 0.21/0.50 % SZS status CounterSatisfiable
% 0.21/0.50 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.21/0.50 SPASS derived 958 clauses, backtracked 0 clauses, performed 0 splits and kept 486 clauses.
% 0.21/0.50 SPASS allocated 98140 KBytes.
% 0.21/0.50 SPASS spent 0:00:00.14 on the problem.
% 0.21/0.50 0:00:00.04 for the input.
% 0.21/0.50 0:00:00.03 for the FLOTTER CNF translation.
% 0.21/0.50 0:00:00.01 for inferences.
% 0.21/0.50 0:00:00.00 for the backtracking.
% 0.21/0.50 0:00:00.04 for the reduction.
% 0.21/0.50
% 0.21/0.50
% 0.21/0.50 The saturated set of worked-off clauses is :
% 0.21/0.50 % SZS output start Saturation
% See solution above
%------------------------------------------------------------------------------