%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SWB008+4 : TPTP v9.0.0. Released v5.2.0. % Transfm : none % Format : tptp:raw % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %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 : 300s % DateTime : Wed Apr 9 09:15:47 PM UTC 2025 % Result : CounterSatisfiable 11.22s 3.98s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SWB008+4 : TPTP v9.0.0. Released v5.2.0. % 0.06/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.12/0.34 % Computer : n021.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Wed Apr 9 00:55:14 EDT 2025 % 0.12/0.34 % CPUTime : % 11.22/3.98 % 11.22/3.98 % SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 11.22/3.98 % 11.22/3.98 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 11.53/3.99 %$ iext > icext > lv > ir > ip > ic > #nlpp > literal_plain > uri_rdfs_subPropertyOf > uri_rdfs_subClassOf > uri_rdfs_seeAlso > uri_rdfs_range > uri_rdfs_member > uri_rdfs_label > uri_rdfs_isDefinedBy > uri_rdfs_domain > uri_rdfs_comment > uri_rdfs_Statement > uri_rdfs_Seq > uri_rdfs_Resource > uri_rdfs_Literal > uri_rdfs_Datatype > uri_rdfs_ContainerMembershipProperty > uri_rdfs_Container > uri_rdfs_Class > uri_rdf_value > uri_rdf_type > uri_rdf_subject > uri_rdf_rest > uri_rdf_predicate > uri_rdf_object > uri_rdf_nil > uri_rdf_first > uri_rdf__3 > uri_rdf__2 > uri_rdf__1 > uri_rdf_XMLLiteral > uri_rdf_Property > uri_rdf_List > uri_rdf_Bag > uri_rdf_Alt > uri_owl_sameAs > uri_owl_InverseFunctionalProperty > uri_owl_DatatypeProperty > uri_foaf_mbox_sha1sum > uri_ex_robert > uri_ex_bob > dat_str_xyz % 11.53/3.99 % 11.53/3.99 %Foreground sorts: % 11.53/3.99 % 11.53/3.99 % 11.53/3.99 %Background operators: % 11.53/3.99 % 11.53/3.99 % 11.53/3.99 %Foreground operators: % 11.53/3.99 tff(uri_owl_InverseFunctionalProperty, type, uri_owl_InverseFunctionalProperty: $i). % 11.53/3.99 tff(uri_rdfs_Datatype, type, uri_rdfs_Datatype: $i). % 11.53/3.99 tff(uri_rdfs_ContainerMembershipProperty, type, uri_rdfs_ContainerMembershipProperty: $i). % 11.53/3.99 tff(uri_rdfs_Resource, type, uri_rdfs_Resource: $i). % 11.53/3.99 tff(uri_rdf_Property, type, uri_rdf_Property: $i). % 11.53/3.99 tff(uri_rdf_subject, type, uri_rdf_subject: $i). % 11.53/3.99 tff(uri_rdf_type, type, uri_rdf_type: $i). % 11.53/3.99 tff(uri_rdfs_subPropertyOf, type, uri_rdfs_subPropertyOf: $i). % 11.53/3.99 tff(uri_rdfs_seeAlso, type, uri_rdfs_seeAlso: $i). % 11.53/3.99 tff(uri_rdfs_range, type, uri_rdfs_range: $i). % 11.53/3.99 tff(uri_rdf_XMLLiteral, type, uri_rdf_XMLLiteral: $i). % 11.53/3.99 tff(uri_rdf_List, type, uri_rdf_List: $i). % 11.53/3.99 tff(uri_rdf_first, type, uri_rdf_first: $i). % 11.53/3.99 tff(uri_rdf_predicate, type, uri_rdf_predicate: $i). % 11.53/3.99 tff(dat_str_xyz, type, dat_str_xyz: $i). % 11.53/3.99 tff(uri_ex_bob, type, uri_ex_bob: $i). % 11.53/3.99 tff(uri_rdf__3, type, uri_rdf__3: $i). % 11.53/3.99 tff(icext, type, icext: ($i * $i) > $o). % 11.53/3.99 tff(uri_rdf_value, type, uri_rdf_value: $i). % 11.53/3.99 tff(ip, type, ip: $i > $o). % 11.53/3.99 tff(uri_rdfs_Statement, type, uri_rdfs_Statement: $i). % 11.53/3.99 tff(uri_rdf__1, type, uri_rdf__1: $i). % 11.53/3.99 tff(lv, type, lv: $i > $o). % 11.53/3.99 tff(ir, type, ir: $i > $o). % 11.53/3.99 tff(uri_rdf_rest, type, uri_rdf_rest: $i). % 11.53/3.99 tff(uri_rdfs_label, type, uri_rdfs_label: $i). % 11.53/3.99 tff(uri_rdfs_Container, type, uri_rdfs_Container: $i). % 11.53/3.99 tff(ic, type, ic: $i > $o). % 11.53/3.99 tff(uri_ex_robert, type, uri_ex_robert: $i). % 11.53/3.99 tff(uri_rdfs_subClassOf, type, uri_rdfs_subClassOf: $i). % 11.53/3.99 tff(uri_foaf_mbox_sha1sum, type, uri_foaf_mbox_sha1sum: $i). % 11.53/3.99 tff(uri_owl_sameAs, type, uri_owl_sameAs: $i). % 11.53/3.99 tff(uri_rdf_object, type, uri_rdf_object: $i). % 11.53/3.99 tff(uri_rdfs_Class, type, uri_rdfs_Class: $i). % 11.53/3.99 tff(uri_rdfs_Seq, type, uri_rdfs_Seq: $i). % 11.53/3.99 tff(iext, type, iext: ($i * $i * $i) > $o). % 11.53/3.99 tff(uri_owl_DatatypeProperty, type, uri_owl_DatatypeProperty: $i). % 11.53/3.99 tff(uri_rdfs_member, type, uri_rdfs_member: $i). % 11.53/3.99 tff(uri_rdf_Bag, type, uri_rdf_Bag: $i). % 11.53/3.99 tff(uri_rdf__2, type, uri_rdf__2: $i). % 11.53/3.99 tff(uri_rdfs_comment, type, uri_rdfs_comment: $i). % 11.53/3.99 tff(uri_rdfs_Literal, type, uri_rdfs_Literal: $i). % 11.53/3.99 tff(uri_rdf_Alt, type, uri_rdf_Alt: $i). % 11.53/3.99 tff(uri_rdf_nil, type, uri_rdf_nil: $i). % 11.53/3.99 tff(literal_plain, type, literal_plain: $i > $i). % 11.53/3.99 tff(uri_rdfs_isDefinedBy, type, uri_rdfs_isDefinedBy: $i). % 11.53/3.99 tff(uri_rdfs_domain, type, uri_rdfs_domain: $i). % 11.53/3.99 % 11.53/3.99 %Saturated clause set: % 11.53/3.99 tff(c_9137, plain, (![P_87]: (~iext(uri_rdfs_subPropertyOf, uri_foaf_mbox_sha1sum, P_87) | ~iext(uri_rdfs_subPropertyOf, P_87, uri_rdfs_isDefinedBy)))). % 11.53/3.99 tff(c_4932, plain, (![Q_32, Q_291]: (iext(Q_32, uri_ex_bob, literal_plain(dat_str_xyz)) | ~iext(uri_rdfs_subPropertyOf, Q_291, Q_32) | ~iext(uri_rdfs_subPropertyOf, uri_foaf_mbox_sha1sum, Q_291)))). % 11.53/3.99 tff(c_6243, plain, (![Q_32, C_327]: (iext(Q_32, C_327, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_327, uri_rdfs_Datatype)))). % 11.53/3.99 tff(c_7699, plain, (![Q_32, C_354]: (iext(Q_32, C_354, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_354, uri_rdfs_ContainerMembershipProperty)))). % 11.53/3.99 tff(c_7700, plain, (![C_28, C_354]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, C_354) | ~iext(uri_rdfs_subClassOf, C_354, uri_rdfs_ContainerMembershipProperty)))). % 11.53/3.99 tff(c_6244, plain, (![C_28, C_327]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, C_327) | ~iext(uri_rdfs_subClassOf, C_327, uri_rdfs_Datatype)))). % 11.53/3.99 tff(c_8891, plain, (![C_80]: (~iext(uri_rdfs_range, uri_foaf_mbox_sha1sum, C_80) | ~iext(uri_rdfs_subClassOf, C_80, uri_rdf_Bag)))). % 11.53/3.99 tff(c_7197, plain, (![Q_32, C_338]: (iext(Q_32, C_338, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_338, uri_rdf_Alt)))). % 11.53/3.99 tff(c_8867, plain, (![C_80]: (~iext(uri_rdfs_range, uri_foaf_mbox_sha1sum, C_80) | ~iext(uri_rdfs_subClassOf, C_80, uri_rdf_XMLLiteral)))). % 11.53/3.99 tff(c_7198, plain, (![C_28, C_338]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, C_338) | ~iext(uri_rdfs_subClassOf, C_338, uri_rdf_Alt)))). % 11.53/3.99 tff(c_6582, plain, (![C_28, C_332]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, C_332) | ~iext(uri_rdfs_subClassOf, C_332, uri_rdf_Bag)))). % 11.53/3.99 tff(c_6885, plain, (![C_28, C_336]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, C_336) | ~iext(uri_rdfs_subClassOf, C_336, uri_rdf_XMLLiteral)))). % 11.53/3.99 tff(c_8579, plain, (![C_80]: (~iext(uri_rdfs_range, uri_foaf_mbox_sha1sum, C_80) | ~iext(uri_rdfs_subClassOf, C_80, uri_rdf_Alt)))). % 11.53/3.99 tff(c_6884, plain, (![Q_32, C_336]: (iext(Q_32, C_336, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_336, uri_rdf_XMLLiteral)))). % 11.53/3.99 tff(c_8563, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_foaf_mbox_sha1sum))). % 11.53/3.99 tff(c_8545, plain, (![P_10]: (~iext(uri_rdfs_subPropertyOf, uri_foaf_mbox_sha1sum, P_10) | ~icext(uri_rdfs_ContainerMembershipProperty, P_10)))). % 11.53/3.99 tff(c_8544, plain, (~iext(uri_rdfs_subPropertyOf, uri_foaf_mbox_sha1sum, uri_rdfs_isDefinedBy))). % 11.53/3.99 tff(c_5029, plain, (![Q_32, Q_302]: (iext(Q_32, uri_ex_robert, literal_plain(dat_str_xyz)) | ~iext(uri_rdfs_subPropertyOf, Q_302, Q_32) | ~iext(uri_rdfs_subPropertyOf, uri_foaf_mbox_sha1sum, Q_302)))). % 11.53/3.99 tff(c_6581, plain, (![Q_32, C_332]: (iext(Q_32, C_332, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_332, uri_rdf_Bag)))). % 11.53/4.00 tff(c_4465, plain, (![Q_32, C_276]: (iext(Q_32, C_276, uri_rdfs_Container) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_276, uri_rdf_Bag)))). % 11.53/4.00 tff(c_4466, plain, (![C_28, C_276]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Container) | ~iext(uri_rdfs_subClassOf, C_28, C_276) | ~iext(uri_rdfs_subClassOf, C_276, uri_rdf_Bag)))). % 11.53/4.00 tff(c_8404, plain, (![D_11]: (~iext(uri_rdfs_range, uri_foaf_mbox_sha1sum, D_11) | ~icext(uri_rdfs_Datatype, D_11)))). % 11.53/4.00 tff(c_8403, plain, (~iext(uri_rdfs_range, uri_foaf_mbox_sha1sum, uri_rdf_Alt))). % 11.53/4.00 tff(c_8387, plain, (~iext(uri_rdfs_range, uri_foaf_mbox_sha1sum, uri_rdf_Bag))). % 11.53/4.00 tff(c_4080, plain, (![Q_32, P_265]: (iext(Q_32, P_265, uri_rdfs_seeAlso) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_32) | ~iext(uri_rdfs_subPropertyOf, P_265, uri_rdfs_isDefinedBy)))). % 11.53/4.00 tff(c_8386, plain, (~iext(uri_rdfs_range, uri_foaf_mbox_sha1sum, uri_rdfs_Seq))). % 11.53/4.00 tff(c_8385, plain, (~iext(uri_rdfs_range, uri_foaf_mbox_sha1sum, uri_rdf_XMLLiteral))). % 11.53/4.00 tff(c_3531, plain, (![D_24, C_253]: (icext(D_24, literal_plain(dat_str_xyz)) | ~iext(uri_rdfs_subClassOf, C_253, D_24) | ~iext(uri_rdfs_range, uri_foaf_mbox_sha1sum, C_253)))). % 11.53/4.00 tff(c_8290, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_member, uri_rdfs_isDefinedBy))). % 11.53/4.00 tff(c_4079, plain, (![P_38, P_265]: (iext(uri_rdfs_subPropertyOf, P_38, uri_rdfs_seeAlso) | ~iext(uri_rdfs_subPropertyOf, P_38, P_265) | ~iext(uri_rdfs_subPropertyOf, P_265, uri_rdfs_isDefinedBy)))). % 11.53/4.00 tff(c_3789, plain, (![C_28, C_256]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Container) | ~iext(uri_rdfs_subClassOf, C_28, C_256) | ~iext(uri_rdfs_subClassOf, C_256, uri_rdf_Alt)))). % 11.53/4.00 tff(c_8180, plain, (~iext(uri_rdfs_subPropertyOf, uri_foaf_mbox_sha1sum, uri_rdfs_label))). % 11.53/4.00 tff(c_8179, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Container, uri_rdf_XMLLiteral))). % 11.53/4.00 tff(c_8178, plain, (~iext(uri_rdfs_subPropertyOf, uri_foaf_mbox_sha1sum, uri_rdfs_comment))). % 11.53/4.00 tff(c_4785, plain, (![C_28, C_282]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Literal) | ~iext(uri_rdfs_subClassOf, C_28, C_282) | ~iext(uri_rdfs_subClassOf, C_282, uri_rdf_XMLLiteral)))). % 11.53/4.00 tff(c_4934, plain, (![C_20, Q_291]: (icext(C_20, literal_plain(dat_str_xyz)) | ~iext(uri_rdfs_range, Q_291, C_20) | ~iext(uri_rdfs_subPropertyOf, uri_foaf_mbox_sha1sum, Q_291)))). % 11.53/4.00 tff(c_3788, plain, (![Q_32, C_256]: (iext(Q_32, C_256, uri_rdfs_Container) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_256, uri_rdf_Alt)))). % 11.53/4.00 tff(c_4784, plain, (![Q_32, C_282]: (iext(Q_32, C_282, uri_rdfs_Literal) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_282, uri_rdf_XMLLiteral)))). % 11.53/4.00 tff(c_5946, plain, (![C_28, D_326]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, D_326) | ~icext(uri_rdfs_Datatype, D_326)))). % 11.53/4.00 tff(c_5945, plain, (![Q_32, D_326]: (iext(Q_32, D_326, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~icext(uri_rdfs_Datatype, D_326)))). % 11.53/4.00 tff(c_4935, plain, (![C_13, Q_291]: (icext(C_13, uri_ex_bob) | ~iext(uri_rdfs_domain, Q_291, C_13) | ~iext(uri_rdfs_subPropertyOf, uri_foaf_mbox_sha1sum, Q_291)))). % 11.53/4.00 tff(c_7807, plain, (~iext(uri_rdfs_subPropertyOf, uri_foaf_mbox_sha1sum, uri_rdf_rest))). % 11.53/4.00 tff(c_7806, plain, (~iext(uri_rdfs_subPropertyOf, uri_foaf_mbox_sha1sum, uri_rdf_predicate))). % 11.53/4.00 tff(c_7805, plain, (~iext(uri_rdfs_subPropertyOf, uri_foaf_mbox_sha1sum, uri_rdf_first))). % 11.53/4.00 tff(c_7804, plain, (~iext(uri_rdfs_subPropertyOf, uri_foaf_mbox_sha1sum, uri_rdfs_domain))). % 11.53/4.00 tff(c_7803, plain, (~iext(uri_rdfs_subPropertyOf, uri_foaf_mbox_sha1sum, uri_rdfs_range))). % 11.53/4.00 tff(c_7802, plain, (~iext(uri_rdfs_subPropertyOf, uri_foaf_mbox_sha1sum, uri_rdf_object))). % 11.53/4.00 tff(c_7801, plain, (~iext(uri_rdfs_subPropertyOf, uri_foaf_mbox_sha1sum, uri_rdf_subject))). % 11.53/4.00 tff(c_5032, plain, (![C_13, Q_302]: (icext(C_13, uri_ex_robert) | ~iext(uri_rdfs_domain, Q_302, C_13) | ~iext(uri_rdfs_subPropertyOf, uri_foaf_mbox_sha1sum, Q_302)))). % 11.53/4.00 tff(c_7724, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdf_Bag))). % 11.53/4.00 tff(c_7723, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdf_Alt))). % 11.53/4.00 tff(c_5599, plain, (![Q_32]: (iext(Q_32, uri_rdf_Bag, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32)))). % 11.53/4.00 tff(c_5531, plain, (![C_28]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, uri_rdfs_ContainerMembershipProperty)))). % 11.53/4.00 tff(c_5567, plain, (![Q_32]: (iext(Q_32, uri_rdfs_Datatype, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32)))). % 11.53/4.00 tff(c_1374, plain, (![Q_83, P_10]: (iext(Q_83, P_10, uri_rdfs_member) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_83) | ~icext(uri_rdfs_ContainerMembershipProperty, P_10)))). % 11.53/4.00 tff(c_5484, plain, (![C_28]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Seq)))). % 11.53/4.00 tff(c_1372, plain, (![Q_83, D_11]: (iext(Q_83, D_11, uri_rdfs_Literal) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_83) | ~icext(uri_rdfs_Datatype, D_11)))). % 11.53/4.00 tff(c_7353, plain, (~icext(uri_rdfs_Datatype, uri_rdfs_Container))). % 11.53/4.00 tff(c_1217, plain, (![C_80, D_11]: (iext(uri_rdfs_subClassOf, C_80, uri_rdfs_Literal) | ~iext(uri_rdfs_subClassOf, C_80, D_11) | ~icext(uri_rdfs_Datatype, D_11)))). % 11.53/4.00 tff(c_5646, plain, (![Q_32]: (iext(Q_32, uri_rdf_Alt, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32)))). % 11.53/4.00 tff(c_1373, plain, (![Q_83, X_7, C_8]: (iext(Q_83, X_7, C_8) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83) | ~icext(C_8, X_7)))). % 11.53/4.00 tff(c_5451, plain, (![Q_32]: (iext(Q_32, uri_rdf_XMLLiteral, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32)))). % 11.53/4.00 tff(c_7227, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdfs_seeAlso))). % 11.53/4.00 tff(c_1452, plain, (![P_87, P_10]: (iext(uri_rdfs_subPropertyOf, P_87, uri_rdfs_member) | ~iext(uri_rdfs_subPropertyOf, P_87, P_10) | ~icext(uri_rdfs_ContainerMembershipProperty, P_10)))). % 11.53/4.00 tff(c_5403, plain, (![C_80]: (iext(uri_rdfs_subClassOf, C_80, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_80, uri_rdf_Alt)))). % 11.53/4.00 tff(c_5483, plain, (![Q_32]: (iext(Q_32, uri_rdfs_Seq, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32)))). % 11.53/4.00 tff(c_5397, plain, (![C_80]: (iext(uri_rdfs_subClassOf, C_80, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_80, uri_rdf_XMLLiteral)))). % 11.53/4.00 tff(c_911, plain, (![C_72, X_7, C_8]: (icext(C_72, X_7) | ~iext(uri_rdfs_domain, uri_rdf_type, C_72) | ~icext(C_8, X_7)))). % 11.53/4.00 tff(c_5400, plain, (![C_80]: (iext(uri_rdfs_subClassOf, C_80, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_80, uri_rdf_Bag)))). % 11.53/4.00 tff(c_5530, plain, (![Q_32]: (iext(Q_32, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32)))). % 11.53/4.00 tff(c_6255, plain, (![P_329]: (icext(uri_rdf_Property, P_329) | ~icext(uri_rdfs_ContainerMembershipProperty, P_329)))). % 11.53/4.00 tff(c_912, plain, (![C_72, P_10]: (icext(C_72, P_10) | ~iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_72) | ~icext(uri_rdfs_ContainerMembershipProperty, P_10)))). % 11.53/4.00 tff(c_5568, plain, (![C_28]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Datatype)))). % 11.53/4.00 tff(c_5406, plain, (![D_11]: (iext(uri_rdfs_subClassOf, D_11, uri_rdfs_Resource) | ~icext(uri_rdfs_Datatype, D_11)))). % 11.53/4.00 tff(c_5361, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, uri_rdfs_isDefinedBy))). % 11.53/4.00 tff(c_5428, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Resource))). % 11.53/4.00 tff(c_1378, plain, (![Q_83, C_27]: (iext(Q_83, C_27, C_27) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_83) | ~ic(C_27)))). % 11.53/4.00 tff(c_5425, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Resource))). % 11.53/4.00 tff(c_5422, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Resource))). % 11.53/4.00 tff(c_5419, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Resource))). % 11.53/4.00 tff(c_5416, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Resource))). % 11.53/4.00 tff(c_5413, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Resource))). % 11.53/4.01 tff(c_1218, plain, (![C_80, C_9]: (iext(uri_rdfs_subClassOf, C_80, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_80, C_9) | ~ic(C_9)))). % 11.53/4.01 tff(c_1377, plain, (![Q_83, C_9]: (iext(Q_83, C_9, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_83) | ~ic(C_9)))). % 11.53/4.01 tff(c_5345, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, uri_rdfs_isDefinedBy))). % 11.53/4.01 tff(c_5333, plain, (![D_318]: (icext(uri_rdfs_Class, D_318) | ~icext(uri_rdfs_Datatype, D_318)))). % 11.53/4.01 tff(c_910, plain, (![C_72, D_11]: (icext(C_72, D_11) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_72) | ~icext(uri_rdfs_Datatype, D_11)))). % 11.53/4.01 tff(c_5238, plain, (![C_76]: (icext(uri_rdfs_Class, C_76) | ~iext(uri_rdfs_range, uri_foaf_mbox_sha1sum, C_76)))). % 11.53/4.01 tff(c_5144, plain, (![C_312, X_313]: (icext(uri_rdfs_Class, C_312) | ~icext(C_312, X_313)))). % 11.53/4.01 tff(c_1126, plain, (![C_76, C_8, X_7]: (icext(C_76, C_8) | ~iext(uri_rdfs_range, uri_rdf_type, C_76) | ~icext(C_8, X_7)))). % 11.53/4.01 tff(c_1376, plain, (![Q_83, P_6]: (iext(Q_83, P_6, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83) | ~ip(P_6)))). % 11.53/4.01 tff(c_5119, plain, (![C_76]: (icext(C_76, uri_rdfs_member) | ~iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_76)))). % 11.53/4.01 tff(c_5113, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy))). % 11.53/4.01 tff(c_5112, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, uri_rdfs_isDefinedBy))). % 11.53/4.01 tff(c_5111, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdf_type, uri_rdfs_isDefinedBy))). % 11.53/4.01 tff(c_1375, plain, (![Q_83, P_37]: (iext(Q_83, P_37, P_37) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_83) | ~ip(P_37)))). % 11.53/4.01 tff(c_1598, plain, (![D_24, P_92]: (icext(D_24, P_92) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24) | ~ip(P_92)))). % 11.53/4.01 tff(c_5060, plain, (![C_76]: (icext(C_76, uri_rdfs_Resource) | ~iext(uri_rdfs_range, uri_rdfs_subClassOf, C_76)))). % 11.53/4.01 tff(c_1380, plain, (![Q_83]: (iext(Q_83, uri_ex_robert, literal_plain(dat_str_xyz)) | ~iext(uri_rdfs_subPropertyOf, uri_foaf_mbox_sha1sum, Q_83)))). % 11.53/4.01 tff(c_1128, plain, (![C_76, P_37]: (icext(C_76, P_37) | ~iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_76) | ~ip(P_37)))). % 11.53/4.01 tff(c_765, plain, (![D_69, X_16]: (icext(D_69, X_16) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_69) | ~ic(X_16)))). % 11.53/4.01 tff(c_915, plain, (![C_72, C_9]: (icext(C_72, C_9) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_72) | ~ic(C_9)))). % 11.53/4.01 tff(c_1131, plain, (![C_76, C_27]: (icext(C_76, C_27) | ~iext(uri_rdfs_range, uri_rdfs_subClassOf, C_76) | ~ic(C_27)))). % 11.53/4.01 tff(c_4950, plain, (~iext(uri_rdfs_subPropertyOf, uri_foaf_mbox_sha1sum, uri_rdf_type))). % 11.53/4.01 tff(c_914, plain, (![C_72, P_6]: (icext(C_72, P_6) | ~iext(uri_rdfs_domain, uri_rdf_type, C_72) | ~ip(P_6)))). % 11.53/4.01 tff(c_4943, plain, (~iext(uri_rdfs_subPropertyOf, uri_foaf_mbox_sha1sum, uri_rdfs_subClassOf))). % 11.53/4.01 tff(c_4942, plain, (~iext(uri_rdfs_subPropertyOf, uri_foaf_mbox_sha1sum, uri_rdfs_subPropertyOf))). % 11.53/4.01 tff(c_1379, plain, (![Q_83]: (iext(Q_83, uri_ex_bob, literal_plain(dat_str_xyz)) | ~iext(uri_rdfs_subPropertyOf, uri_foaf_mbox_sha1sum, Q_83)))). % 11.53/4.01 tff(c_4865, plain, (~iext(uri_rdfs_subClassOf, uri_owl_DatatypeProperty, uri_rdf_XMLLiteral))). % 11.53/4.01 tff(c_764, plain, (![D_69, X_18]: (icext(D_69, X_18) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Literal, D_69) | ~lv(X_18)))). % 11.53/4.01 tff(c_4864, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdf_XMLLiteral))). % 11.53/4.01 tff(c_4863, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdf_XMLLiteral))). % 11.53/4.01 tff(c_913, plain, (![C_72, P_37]: (icext(C_72, P_37) | ~iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_72) | ~ip(P_37)))). % 11.53/4.01 tff(c_1425, plain, (![Q_83]: (iext(Q_83, uri_rdfs_isDefinedBy, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))). % 11.53/4.01 tff(c_4843, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdfs_subPropertyOf))). % 11.53/4.01 tff(c_1423, plain, (![Q_83]: (iext(Q_83, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_83)))). % 11.53/4.01 tff(c_4827, plain, (~iext(uri_rdfs_subClassOf, uri_owl_InverseFunctionalProperty, uri_rdf_XMLLiteral))). % 11.53/4.01 tff(c_4811, plain, (~iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdf_XMLLiteral))). % 11.53/4.01 tff(c_1409, plain, (![Q_83]: (iext(Q_83, uri_rdf__1, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))). % 11.53/4.01 tff(c_4810, plain, (~iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdf_XMLLiteral))). % 11.53/4.01 tff(c_4794, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdf_XMLLiteral))). % 11.53/4.01 tff(c_1422, plain, (![Q_83]: (iext(Q_83, uri_rdf_predicate, uri_rdfs_Statement) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))). % 11.53/4.01 tff(c_4793, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Resource, uri_rdf_XMLLiteral))). % 11.53/4.01 tff(c_1220, plain, (![C_80]: (iext(uri_rdfs_subClassOf, C_80, uri_rdfs_Literal) | ~iext(uri_rdfs_subClassOf, C_80, uri_rdf_XMLLiteral)))). % 11.53/4.01 tff(c_4556, plain, (~iext(uri_rdfs_subClassOf, uri_owl_InverseFunctionalProperty, uri_rdf_Bag))). % 11.53/4.01 tff(c_4555, plain, (~iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdf_Bag))). % 11.53/4.01 tff(c_4539, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdf_Bag))). % 11.53/4.01 tff(c_1383, plain, (![Q_83]: (iext(Q_83, uri_rdfs_range, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))). % 11.53/4.01 tff(c_1399, plain, (![Q_83]: (iext(Q_83, uri_rdf__1, uri_rdfs_ContainerMembershipProperty) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))). % 11.53/4.01 tff(c_4523, plain, (~iext(uri_rdfs_subClassOf, uri_owl_DatatypeProperty, uri_rdf_Bag))). % 11.53/4.01 tff(c_4507, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdf_Bag))). % 11.53/4.01 tff(c_1438, plain, (![Q_83]: (iext(Q_83, uri_rdf_type, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))). % 11.53/4.01 tff(c_1416, plain, (![Q_83]: (iext(Q_83, uri_rdf_rest, uri_rdf_List) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))). % 11.53/4.01 tff(c_4491, plain, (~iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdf_Bag))). % 11.53/4.01 tff(c_1414, plain, (![Q_83]: (iext(Q_83, uri_rdfs_subClassOf, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))). % 11.53/4.01 tff(c_4475, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdf_Bag))). % 11.53/4.01 tff(c_4474, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Resource, uri_rdf_Bag))). % 11.53/4.01 tff(c_1224, plain, (![C_80]: (iext(uri_rdfs_subClassOf, C_80, uri_rdfs_Container) | ~iext(uri_rdfs_subClassOf, C_80, uri_rdf_Bag)))). % 11.53/4.01 tff(c_1381, plain, (![Q_83]: (iext(Q_83, uri_rdf__3, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))). % 11.53/4.01 tff(c_1426, plain, (![Q_83]: (iext(Q_83, uri_rdf__2, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))). % 11.53/4.01 tff(c_1396, plain, (![Q_83]: (iext(Q_83, uri_rdf__3, uri_rdfs_ContainerMembershipProperty) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))). % 11.53/4.01 tff(c_1437, plain, (![Q_83]: (iext(Q_83, uri_rdf_object, uri_rdfs_Statement) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))). % 11.53/4.01 tff(c_1387, plain, (![Q_83]: (iext(Q_83, uri_rdf_value, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))). % 11.53/4.01 tff(c_1398, plain, (![Q_83]: (iext(Q_83, uri_rdfs_range, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))). % 11.53/4.01 tff(c_1427, plain, (![Q_83]: (iext(Q_83, uri_rdfs_domain, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))). % 11.53/4.01 tff(c_1429, plain, (![Q_83]: (iext(Q_83, uri_rdf_predicate, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))). % 11.53/4.01 tff(c_1403, plain, (![Q_83]: (iext(Q_83, uri_rdf__2, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))). % 11.53/4.01 tff(c_1419, plain, (![Q_83]: (iext(Q_83, uri_rdfs_member, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))). % 11.53/4.01 tff(c_1454, plain, (![P_87]: (iext(uri_rdfs_subPropertyOf, P_87, uri_rdfs_seeAlso) | ~iext(uri_rdfs_subPropertyOf, P_87, uri_rdfs_isDefinedBy)))). % 11.53/4.01 tff(c_1436, plain, (![Q_83]: (iext(Q_83, uri_rdfs_domain, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))). % 11.53/4.01 tff(c_1428, plain, (![Q_83]: (iext(Q_83, uri_rdf__2, uri_rdfs_ContainerMembershipProperty) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))). % 11.53/4.01 tff(c_3870, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdf_Alt))). % 11.53/4.01 tff(c_1401, plain, (![Q_83]: (iext(Q_83, uri_rdf__3, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))). % 11.53/4.01 tff(c_3847, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdf_Alt))). % 11.53/4.01 tff(c_1400, plain, (![Q_83]: (iext(Q_83, uri_rdf_first, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))). % 11.53/4.02 tff(c_1404, plain, (![Q_83]: (iext(Q_83, uri_rdf__3, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))). % 11.53/4.02 tff(c_3835, plain, (~iext(uri_rdfs_subClassOf, uri_owl_InverseFunctionalProperty, uri_rdf_Alt))). % 11.53/4.02 tff(c_1410, plain, (![Q_83]: (iext(Q_83, uri_rdf_subject, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))). % 11.53/4.02 tff(c_3823, plain, (~iext(uri_rdfs_subClassOf, uri_owl_DatatypeProperty, uri_rdf_Alt))). % 11.53/4.02 tff(c_3822, plain, (~iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdf_Alt))). % 11.53/4.02 tff(c_1393, plain, (![Q_83]: (iext(Q_83, uri_rdfs_Seq, uri_rdfs_Container) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_83)))). % 11.53/4.02 tff(c_3810, plain, (~iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdf_Alt))). % 11.53/4.02 tff(c_1402, plain, (![Q_83]: (iext(Q_83, uri_rdfs_seeAlso, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))). % 11.53/4.02 tff(c_3798, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdf_Alt))). % 11.53/4.02 tff(c_3797, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Resource, uri_rdf_Alt))). % 11.53/4.02 tff(c_1225, plain, (![C_80]: (iext(uri_rdfs_subClassOf, C_80, uri_rdfs_Container) | ~iext(uri_rdfs_subClassOf, C_80, uri_rdf_Alt)))). % 11.53/4.02 tff(c_1435, plain, (![Q_83]: (iext(Q_83, uri_rdfs_subPropertyOf, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))). % 11.53/4.02 tff(c_3549, plain, (~iext(uri_rdfs_range, uri_foaf_mbox_sha1sum, uri_rdfs_Datatype))). % 11.53/4.02 tff(c_3537, plain, (~iext(uri_rdfs_range, uri_foaf_mbox_sha1sum, uri_rdf_Property))). % 11.53/4.02 tff(c_1413, plain, (![Q_83]: (iext(Q_83, uri_rdfs_Datatype, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_83)))). % 11.53/4.02 tff(c_3536, plain, (~iext(uri_rdfs_range, uri_foaf_mbox_sha1sum, uri_rdfs_Class))). % 11.53/4.02 tff(c_3535, plain, (~iext(uri_rdfs_range, uri_foaf_mbox_sha1sum, uri_rdfs_Literal))). % 11.53/4.02 tff(c_3534, plain, (~iext(uri_rdfs_range, uri_foaf_mbox_sha1sum, uri_rdfs_ContainerMembershipProperty))). % 11.53/4.02 tff(c_1133, plain, (![C_76]: (icext(C_76, literal_plain(dat_str_xyz)) | ~iext(uri_rdfs_range, uri_foaf_mbox_sha1sum, C_76)))). % 11.53/4.02 tff(c_1384, plain, (![Q_83]: (iext(Q_83, uri_rdf__1, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))). % 11.53/4.02 tff(c_1412, plain, (![Q_83]: (iext(Q_83, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_83)))). % 11.53/4.02 tff(c_1408, plain, (![Q_83]: (iext(Q_83, uri_rdf_rest, uri_rdf_List) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))). % 11.53/4.02 tff(c_1432, plain, (![Q_83]: (iext(Q_83, uri_rdf_value, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))). % 11.53/4.02 tff(c_1418, plain, (![Q_83]: (iext(Q_83, uri_rdf_subject, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))). % 11.53/4.02 tff(c_1430, plain, (![Q_83]: (iext(Q_83, uri_rdfs_seeAlso, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))). % 11.53/4.02 tff(c_1415, plain, (![Q_83]: (iext(Q_83, uri_rdfs_isDefinedBy, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))). % 11.53/4.02 tff(c_1405, plain, (![Q_83]: (iext(Q_83, uri_rdf_type, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))). % 11.53/4.02 tff(c_1392, plain, (![Q_83]: (iext(Q_83, uri_rdf_Property, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))). % 11.53/4.02 tff(c_1382, plain, (![Q_83]: (iext(Q_83, uri_rdf_subject, uri_rdfs_Statement) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))). % 11.53/4.02 tff(c_1386, plain, (![Q_83]: (iext(Q_83, uri_rdf_rest, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))). % 11.53/4.02 tff(c_1222, plain, (![C_80]: (iext(uri_rdfs_subClassOf, C_80, uri_rdf_Property) | ~iext(uri_rdfs_subClassOf, C_80, uri_rdfs_ContainerMembershipProperty)))). % 11.53/4.02 tff(c_1389, plain, (![Q_83]: (iext(Q_83, uri_rdf_XMLLiteral, uri_rdfs_Literal) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_83)))). % 11.53/4.02 tff(c_1390, plain, (![Q_83]: (iext(Q_83, uri_rdfs_subClassOf, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))). % 11.53/4.02 tff(c_1388, plain, (![Q_83]: (iext(Q_83, uri_foaf_mbox_sha1sum, uri_owl_InverseFunctionalProperty) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))). % 11.53/4.02 tff(c_1431, plain, (![Q_83]: (iext(Q_83, uri_rdf_first, uri_rdf_List) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))). % 11.53/4.02 tff(c_1421, plain, (![Q_83]: (iext(Q_83, uri_rdf_Alt, uri_rdfs_Container) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_83)))). % 11.53/4.02 tff(c_1433, plain, (![Q_83]: (iext(Q_83, uri_rdfs_label, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))). % 11.53/4.02 tff(c_1394, plain, (![Q_83]: (iext(Q_83, uri_foaf_mbox_sha1sum, uri_owl_DatatypeProperty) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))). % 11.53/4.02 tff(c_1406, plain, (![Q_83]: (iext(Q_83, uri_rdf_value, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))). % 11.53/4.02 tff(c_1391, plain, (![Q_83]: (iext(Q_83, uri_rdf__2, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))). % 11.53/4.02 tff(c_1417, plain, (![Q_83]: (iext(Q_83, uri_rdf__1, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))). % 11.53/4.02 tff(c_1395, plain, (![Q_83]: (iext(Q_83, uri_rdfs_subPropertyOf, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))). % 11.53/4.02 tff(c_1385, plain, (![Q_83]: (iext(Q_83, uri_rdfs_comment, uri_rdfs_Literal) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))). % 11.53/4.02 tff(c_1439, plain, (![Q_83]: (iext(Q_83, uri_rdf_first, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))). % 11.53/4.02 tff(c_1223, plain, (![C_80]: (iext(uri_rdfs_subClassOf, C_80, uri_rdfs_Class) | ~iext(uri_rdfs_subClassOf, C_80, uri_rdfs_Datatype)))). % 11.53/4.02 tff(c_1434, plain, (![Q_83]: (iext(Q_83, uri_rdfs_member, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))). % 11.53/4.02 tff(c_1411, plain, (![Q_83]: (iext(Q_83, uri_rdf_object, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))). % 11.53/4.02 tff(c_1660, plain, (![D_24]: (icext(D_24, uri_rdfs_domain) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))). % 11.53/4.02 tff(c_1940, plain, (![D_24]: (icext(D_24, uri_rdfs_Class) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))). % 11.53/4.02 tff(c_1923, plain, (![D_24]: (icext(D_24, uri_rdfs_subPropertyOf) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))). % 11.53/4.02 tff(c_1440, plain, (![Q_83]: (iext(Q_83, uri_rdf_nil, uri_rdf_List) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))). % 11.53/4.02 tff(c_1773, plain, (![D_24]: (icext(D_24, uri_rdfs_member) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))). % 11.53/4.02 tff(c_1909, plain, (![D_24]: (icext(D_24, uri_owl_DatatypeProperty) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))). % 11.53/4.02 tff(c_1635, plain, (![D_24]: (icext(D_24, uri_rdfs_subClassOf) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))). % 11.53/4.02 tff(c_1859, plain, (![D_24]: (icext(D_24, uri_rdfs_Seq) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))). % 11.53/4.02 tff(c_1730, plain, (![D_24]: (icext(D_24, uri_rdfs_label) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))). % 11.53/4.02 tff(c_1784, plain, (![D_24]: (icext(D_24, uri_rdfs_Literal) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))). % 11.53/4.02 tff(c_1815, plain, (![D_24]: (icext(D_24, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))). % 11.53/4.02 tff(c_2991, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdfs_domain))). % 11.53/4.02 tff(c_1424, plain, (![Q_83]: (iext(Q_83, uri_rdfs_comment, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))). % 11.53/4.02 tff(c_1847, plain, (![D_24]: (icext(D_24, uri_owl_InverseFunctionalProperty) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))). % 11.53/4.02 tff(c_1686, plain, (![D_24]: (icext(D_24, uri_rdfs_isDefinedBy) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))). % 11.53/4.02 tff(c_1953, plain, (![D_24]: (icext(D_24, uri_rdf_XMLLiteral) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))). % 11.53/4.02 tff(c_2040, plain, (![D_24]: (icext(D_24, uri_rdfs_comment) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))). % 11.53/4.02 tff(c_1699, plain, (![D_24]: (icext(D_24, uri_rdfs_range) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))). % 11.53/4.02 tff(c_1828, plain, (![D_24]: (icext(D_24, uri_rdfs_ContainerMembershipProperty) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))). % 11.53/4.02 tff(c_1759, plain, (![D_24]: (icext(D_24, uri_rdf_List) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))). % 11.53/4.02 tff(c_2839, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdfs_range))). % 11.53/4.02 tff(c_1407, plain, (![Q_83]: (iext(Q_83, uri_rdfs_label, uri_rdfs_Literal) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))). % 11.53/4.02 tff(c_1966, plain, (![D_24]: (icext(D_24, uri_rdfs_Datatype) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))). % 11.53/4.02 tff(c_1872, plain, (![D_24]: (icext(D_24, uri_rdf_Bag) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))). % 11.53/4.02 tff(c_2027, plain, (![D_24]: (icext(D_24, uri_rdfs_Statement) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))). % 11.53/4.02 tff(c_2204, plain, (![D_24]: (icext(D_24, uri_rdfs_seeAlso) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))). % 11.53/4.02 tff(c_2227, plain, (![D_24]: (icext(D_24, uri_rdfs_Container) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))). % 11.53/4.02 tff(c_2058, plain, (![D_24]: (icext(D_24, uri_rdf_predicate) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))). % 11.53/4.02 tff(c_2123, plain, (![D_24]: (icext(D_24, uri_rdf_Alt) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))). % 11.53/4.02 tff(c_1507, plain, (![D_24]: (icext(D_24, uri_rdf__3) | ~iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_24)))). % 11.53/4.02 tff(c_1513, plain, (![D_24]: (icext(D_24, uri_rdf_rest) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))). % 11.53/4.02 tff(c_1221, plain, (![C_80]: (iext(uri_rdfs_subClassOf, C_80, uri_rdfs_Container) | ~iext(uri_rdfs_subClassOf, C_80, uri_rdfs_Seq)))). % 11.53/4.02 tff(c_2634, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdfs_subClassOf))). % 11.53/4.02 tff(c_2633, plain, (~icext(uri_rdfs_Datatype, uri_rdfs_Datatype))). % 11.53/4.02 tff(c_2607, plain, (~icext(uri_rdfs_Datatype, uri_owl_InverseFunctionalProperty))). % 11.53/4.02 tff(c_1519, plain, (![D_24]: (icext(D_24, uri_rdf_XMLLiteral) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, D_24)))). % 11.53/4.02 tff(c_1504, plain, (![D_24]: (icext(D_24, uri_foaf_mbox_sha1sum) | ~iext(uri_rdfs_subClassOf, uri_owl_InverseFunctionalProperty, D_24)))). % 11.53/4.02 tff(c_2575, plain, (~icext(uri_rdfs_Datatype, uri_rdf_List))). % 11.53/4.03 tff(c_1420, plain, (![Q_83]: (iext(Q_83, uri_rdf_Bag, uri_rdfs_Container) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_83)))). % 11.53/4.03 tff(c_1490, plain, (![D_24]: (icext(D_24, uri_rdf_nil) | ~iext(uri_rdfs_subClassOf, uri_rdf_List, D_24)))). % 11.53/4.03 tff(c_1484, plain, (![D_24]: (icext(D_24, uri_rdf__1) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))). % 11.53/4.03 tff(c_1481, plain, (![D_24]: (icext(D_24, uri_rdf__1) | ~iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_24)))). % 11.53/4.03 tff(c_2489, plain, (~icext(uri_rdfs_Datatype, uri_owl_DatatypeProperty))). % 11.53/4.03 tff(c_1478, plain, (![D_24]: (icext(D_24, uri_rdf_type) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))). % 11.53/4.03 tff(c_1516, plain, (![D_24]: (icext(D_24, uri_foaf_mbox_sha1sum) | ~iext(uri_rdfs_subClassOf, uri_owl_DatatypeProperty, D_24)))). % 11.53/4.03 tff(c_1469, plain, (![D_24]: (icext(D_24, uri_rdf__2) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))). % 11.53/4.03 tff(c_1397, plain, (![Q_83]: (iext(Q_83, uri_rdf_type, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))). % 11.53/4.03 tff(c_1472, plain, (![D_24]: (icext(D_24, uri_rdf_subject) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))). % 11.53/4.03 tff(c_1501, plain, (![D_24]: (icext(D_24, uri_rdf_object) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))). % 11.53/4.03 tff(c_2397, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdf_type))). % 11.53/4.03 tff(c_2396, plain, (~icext(uri_rdfs_Datatype, uri_rdfs_Class))). % 11.53/4.03 tff(c_1496, plain, (![D_24]: (icext(D_24, uri_rdf_Property) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))). % 11.53/4.03 tff(c_2375, plain, (~icext(uri_rdfs_Datatype, uri_rdfs_ContainerMembershipProperty))). % 11.53/4.03 tff(c_1441, plain, (![Q_83]: (iext(Q_83, uri_rdf_XMLLiteral, uri_rdfs_Datatype) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))). % 11.53/4.03 tff(c_1487, plain, (![D_24]: (icext(D_24, uri_rdf__2) | ~iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_24)))). % 11.53/4.03 tff(c_1510, plain, (![D_24]: (icext(D_24, uri_rdf_value) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))). % 11.53/4.03 tff(c_1466, plain, (![D_24]: (icext(D_24, uri_rdf__3) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))). % 11.53/4.03 tff(c_2298, plain, (~icext(uri_rdfs_Datatype, uri_rdf_Property))). % 11.53/4.03 tff(c_1475, plain, (![D_24]: (icext(D_24, uri_rdf_first) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))). % 11.53/4.03 tff(c_956, plain, (![C_72]: (icext(C_72, uri_rdf_subject) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_72)))). % 11.53/4.03 tff(c_949, plain, (![C_72]: (icext(C_72, uri_rdf_object) | ~iext(uri_rdfs_domain, uri_rdf_type, C_72)))). % 11.53/4.03 tff(c_1176, plain, (![C_76]: (icext(C_76, uri_rdfs_seeAlso) | ~iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_76)))). % 11.53/4.03 tff(c_965, plain, (![C_72]: (icext(C_72, uri_rdfs_domain) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_72)))). % 11.53/4.03 tff(c_922, plain, (![C_72]: (icext(C_72, uri_rdf__1) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_72)))). % 11.53/4.03 tff(c_968, plain, (![C_72]: (icext(C_72, uri_rdfs_seeAlso) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_72)))). % 11.53/4.03 tff(c_950, plain, (![C_72]: (icext(C_72, uri_rdfs_ContainerMembershipProperty) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_72)))). % 11.53/4.03 tff(c_1145, plain, (![C_76]: (icext(C_76, uri_rdfs_Class) | ~iext(uri_rdfs_range, uri_rdf_type, C_76)))). % 11.53/4.03 tff(c_2221, plain, (icext(uri_rdfs_Class, uri_rdfs_Container))). % 11.53/4.03 tff(c_1174, plain, (![C_76]: (icext(C_76, uri_rdfs_Container) | ~iext(uri_rdfs_range, uri_rdfs_subClassOf, C_76)))). % 11.53/4.03 tff(c_1142, plain, (![C_76]: (icext(C_76, uri_rdfs_Literal) | ~iext(uri_rdfs_range, uri_rdfs_subClassOf, C_76)))). % 11.53/4.03 tff(c_1169, plain, (![C_76]: (icext(C_76, uri_rdf_List) | ~iext(uri_rdfs_range, uri_rdfs_range, C_76)))). % 11.53/4.03 tff(c_2196, plain, (icext(uri_rdf_Property, uri_rdfs_seeAlso))). % 11.53/4.03 tff(c_940, plain, (![C_72]: (icext(C_72, uri_rdfs_seeAlso) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_72)))). % 11.53/4.03 tff(c_954, plain, (![C_72]: (icext(C_72, uri_rdf_rest) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_72)))). % 11.53/4.03 tff(c_1166, plain, (![C_76]: (icext(C_76, uri_rdfs_Class) | ~iext(uri_rdfs_range, uri_rdfs_subClassOf, C_76)))). % 11.53/4.03 tff(c_962, plain, (![C_72]: (icext(C_72, uri_rdfs_comment) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_72)))). % 11.53/4.03 tff(c_953, plain, (![C_72]: (icext(C_72, uri_rdfs_isDefinedBy) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_72)))). % 11.53/4.03 tff(c_943, plain, (![C_72]: (icext(C_72, uri_rdf_type) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_72)))). % 11.53/4.03 tff(c_977, plain, (![C_72]: (icext(C_72, uri_rdf_first) | ~iext(uri_rdfs_domain, uri_rdf_type, C_72)))). % 11.53/4.03 tff(c_945, plain, (![C_72]: (icext(C_72, uri_rdfs_label) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_72)))). % 11.53/4.03 tff(c_1165, plain, (![C_76]: (icext(C_76, uri_rdf_Property) | ~iext(uri_rdfs_range, uri_rdfs_subClassOf, C_76)))). % 11.53/4.03 tff(c_930, plain, (![C_72]: (icext(C_72, uri_rdf_Property) | ~iext(uri_rdfs_domain, uri_rdf_type, C_72)))). % 11.53/4.03 tff(c_1194, plain, (![C_76]: (icext(C_76, uri_rdfs_Datatype) | ~iext(uri_rdfs_range, uri_rdf_type, C_76)))). % 11.53/4.03 tff(c_924, plain, (![C_72]: (icext(C_72, uri_rdf_rest) | ~iext(uri_rdfs_domain, uri_rdf_type, C_72)))). % 11.53/4.03 tff(c_2117, plain, (icext(uri_rdfs_Class, uri_rdf_Alt))). % 11.53/4.03 tff(c_959, plain, (![C_72]: (icext(C_72, uri_rdf_Alt) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_72)))). % 11.53/4.03 tff(c_963, plain, (![C_72]: (icext(C_72, uri_rdfs_isDefinedBy) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_72)))). % 11.53/4.03 tff(c_970, plain, (![C_72]: (icext(C_72, uri_rdf_value) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_72)))). % 11.53/4.03 tff(c_1143, plain, (![C_76]: (icext(C_76, uri_rdfs_Class) | ~iext(uri_rdfs_range, uri_rdfs_domain, C_76)))). % 11.53/4.03 tff(c_920, plain, (![C_72]: (icext(C_72, uri_rdf_subject) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_72)))). % 11.53/4.03 tff(c_964, plain, (![C_72]: (icext(C_72, uri_rdf__2) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_72)))). % 11.53/4.03 tff(c_921, plain, (![C_72]: (icext(C_72, uri_rdfs_range) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_72)))). % 11.53/4.03 tff(c_935, plain, (![C_72]: (icext(C_72, uri_rdf_type) | ~iext(uri_rdfs_domain, uri_rdf_type, C_72)))). % 11.53/4.03 tff(c_933, plain, (![C_72]: (icext(C_72, uri_rdfs_subPropertyOf) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_72)))). % 11.53/4.03 tff(c_2057, plain, (ip(uri_rdf_predicate))). % 11.53/4.03 tff(c_967, plain, (![C_72]: (icext(C_72, uri_rdf_predicate) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_72)))). % 11.53/4.03 tff(c_2051, plain, (icext(uri_rdf_Property, uri_rdf_predicate))). % 11.53/4.03 tff(c_960, plain, (![C_72]: (icext(C_72, uri_rdf_predicate) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_72)))). % 11.53/4.03 tff(c_979, plain, (![C_72]: (icext(C_72, uri_rdf_XMLLiteral) | ~iext(uri_rdfs_domain, uri_rdf_type, C_72)))). % 11.53/4.03 tff(c_2039, plain, (ip(uri_rdfs_comment))). % 11.53/4.03 tff(c_2033, plain, (icext(uri_rdf_Property, uri_rdfs_comment))). % 11.53/4.03 tff(c_923, plain, (![C_72]: (icext(C_72, uri_rdfs_comment) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_72)))). % 11.53/4.03 tff(c_2028, plain, (ic(uri_rdfs_Statement))). % 11.53/4.03 tff(c_2021, plain, (icext(uri_rdfs_Class, uri_rdfs_Statement))). % 11.53/4.03 tff(c_1135, plain, (![C_76]: (icext(C_76, uri_rdfs_Statement) | ~iext(uri_rdfs_range, uri_rdfs_domain, C_76)))). % 11.53/4.03 tff(c_925, plain, (![C_72]: (icext(C_72, uri_rdf_value) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_72)))). % 11.53/4.03 tff(c_946, plain, (![C_72]: (icext(C_72, uri_rdf_rest) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_72)))). % 11.53/4.03 tff(c_944, plain, (![C_72]: (icext(C_72, uri_rdf_value) | ~iext(uri_rdfs_domain, uri_rdf_type, C_72)))). % 11.53/4.03 tff(c_1193, plain, (![C_76]: (icext(C_76, uri_rdf_List) | ~iext(uri_rdfs_range, uri_rdf_type, C_76)))). % 11.53/4.03 tff(c_928, plain, (![C_72]: (icext(C_72, uri_rdfs_subClassOf) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_72)))). % 11.53/4.03 tff(c_1178, plain, (![C_76]: (icext(C_76, uri_rdfs_Resource) | ~iext(uri_rdfs_range, uri_rdfs_range, C_76)))). % 11.53/4.03 tff(c_972, plain, (![C_72]: (icext(C_72, uri_rdfs_member) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_72)))). % 11.53/4.03 tff(c_976, plain, (![C_72]: (icext(C_72, uri_rdf_type) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_72)))). % 11.53/4.03 tff(c_1960, plain, (icext(uri_rdfs_Class, uri_rdfs_Datatype))). % 11.53/4.03 tff(c_951, plain, (![C_72]: (icext(C_72, uri_rdfs_Datatype) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_72)))). % 11.53/4.03 tff(c_1947, plain, (icext(uri_rdfs_Class, uri_rdf_XMLLiteral))). % 11.53/4.03 tff(c_927, plain, (![C_72]: (icext(C_72, uri_rdf_XMLLiteral) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_72)))). % 11.53/4.03 tff(c_1934, plain, (icext(uri_rdfs_Class, uri_rdfs_Class))). % 11.53/4.03 tff(c_1167, plain, (![C_76]: (icext(C_76, uri_rdfs_Class) | ~iext(uri_rdfs_range, uri_rdfs_range, C_76)))). % 11.53/4.03 tff(c_966, plain, (![C_72]: (icext(C_72, uri_rdf__2) | ~iext(uri_rdfs_domain, uri_rdf_type, C_72)))). % 11.53/4.03 tff(c_1915, plain, (icext(uri_rdf_Property, uri_rdfs_subPropertyOf))). % 11.53/4.03 tff(c_973, plain, (![C_72]: (icext(C_72, uri_rdfs_subPropertyOf) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_72)))). % 11.53/4.03 tff(c_1910, plain, (ic(uri_owl_DatatypeProperty))). % 11.53/4.03 tff(c_1903, plain, (icext(uri_rdfs_Class, uri_owl_DatatypeProperty))). % 11.53/4.03 tff(c_1147, plain, (![C_76]: (icext(C_76, uri_owl_DatatypeProperty) | ~iext(uri_rdfs_range, uri_rdf_type, C_76)))). % 11.53/4.03 tff(c_1189, plain, (![C_76]: (icext(C_76, uri_rdf_Property) | ~iext(uri_rdfs_range, uri_rdfs_domain, C_76)))). % 11.53/4.03 tff(c_1148, plain, (![C_76]: (icext(C_76, uri_rdf_Property) | ~iext(uri_rdfs_range, uri_rdfs_range, C_76)))). % 11.53/4.03 tff(c_934, plain, (![C_72]: (icext(C_72, uri_rdf__3) | ~iext(uri_rdfs_domain, uri_rdf_type, C_72)))). % 11.53/4.03 tff(c_978, plain, (![C_72]: (icext(C_72, uri_rdf_nil) | ~iext(uri_rdfs_domain, uri_rdf_type, C_72)))). % 11.53/4.03 tff(c_1866, plain, (icext(uri_rdfs_Class, uri_rdf_Bag))). % 11.53/4.03 tff(c_958, plain, (![C_72]: (icext(C_72, uri_rdf_Bag) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_72)))). % 11.53/4.03 tff(c_1853, plain, (icext(uri_rdfs_Class, uri_rdfs_Seq))). % 11.53/4.03 tff(c_1848, plain, (ic(uri_owl_InverseFunctionalProperty))). % 11.53/4.03 tff(c_931, plain, (![C_72]: (icext(C_72, uri_rdfs_Seq) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_72)))). % 11.53/4.03 tff(c_1841, plain, (icext(uri_rdfs_Class, uri_owl_InverseFunctionalProperty))). % 11.53/4.03 tff(c_1141, plain, (![C_76]: (icext(C_76, uri_owl_InverseFunctionalProperty) | ~iext(uri_rdfs_range, uri_rdf_type, C_76)))). % 11.53/4.03 tff(c_941, plain, (![C_72]: (icext(C_72, uri_rdf__2) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_72)))). % 11.53/4.03 tff(c_1822, plain, (icext(uri_rdfs_Class, uri_rdfs_ContainerMembershipProperty))). % 11.53/4.03 tff(c_1149, plain, (![C_76]: (icext(C_76, uri_rdfs_ContainerMembershipProperty) | ~iext(uri_rdfs_range, uri_rdf_type, C_76)))). % 11.53/4.03 tff(c_1804, plain, (~icext(uri_rdfs_Datatype, uri_rdfs_Resource))). % 11.53/4.03 tff(c_1809, plain, (icext(uri_rdfs_Class, uri_rdfs_Resource))). % 11.53/4.03 tff(c_1185, plain, (![C_76]: (icext(C_76, uri_rdfs_Resource) | ~iext(uri_rdfs_range, uri_rdfs_domain, C_76)))). % 11.53/4.03 tff(c_766, plain, (![D_69, X_17]: (icext(D_69, X_17) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Resource, D_69)))). % 11.53/4.03 tff(c_1778, plain, (icext(uri_rdfs_Class, uri_rdfs_Literal))). % 11.53/4.04 tff(c_1138, plain, (![C_76]: (icext(C_76, uri_rdfs_Literal) | ~iext(uri_rdfs_range, uri_rdfs_range, C_76)))). % 11.53/4.04 tff(c_1765, plain, (icext(uri_rdf_Property, uri_rdfs_member))). % 11.53/4.04 tff(c_957, plain, (![C_72]: (icext(C_72, uri_rdfs_member) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_72)))). % 11.53/4.04 tff(c_1760, plain, (ic(uri_rdf_List))). % 11.53/4.04 tff(c_1747, plain, (icext(uri_rdfs_Class, uri_rdf_List))). % 11.53/4.04 tff(c_969, plain, (![C_72]: (icext(C_72, uri_rdf_first) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_72)))). % 11.53/4.04 tff(c_1184, plain, (![C_76]: (icext(C_76, uri_rdf_List) | ~iext(uri_rdfs_range, uri_rdfs_domain, C_76)))). % 11.53/4.04 tff(c_939, plain, (![C_72]: (icext(C_72, uri_rdf__3) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_72)))). % 11.53/4.04 tff(c_948, plain, (![C_72]: (icext(C_72, uri_rdf_subject) | ~iext(uri_rdfs_domain, uri_rdf_type, C_72)))). % 11.53/4.04 tff(c_1729, plain, (ip(uri_rdfs_label))). % 11.53/4.04 tff(c_1723, plain, (icext(uri_rdf_Property, uri_rdfs_label))). % 11.53/4.04 tff(c_971, plain, (![C_72]: (icext(C_72, uri_rdfs_label) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_72)))). % 11.53/4.04 tff(c_947, plain, (![C_72]: (icext(C_72, uri_rdf__1) | ~iext(uri_rdfs_domain, uri_rdf_type, C_72)))). % 11.53/4.04 tff(c_955, plain, (![C_72]: (icext(C_72, uri_rdf__1) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_72)))). % 11.53/4.04 tff(c_1139, plain, (![C_76]: (icext(C_76, uri_rdf_Property) | ~iext(uri_rdfs_range, uri_rdf_type, C_76)))). % 11.53/4.04 tff(c_917, plain, (![C_72]: (icext(C_72, uri_ex_bob) | ~iext(uri_rdfs_domain, uri_foaf_mbox_sha1sum, C_72)))). % 11.53/4.04 tff(c_1691, plain, (icext(uri_rdf_Property, uri_rdfs_range))). % 11.53/4.04 tff(c_936, plain, (![C_72]: (icext(C_72, uri_rdfs_range) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_72)))). % 11.53/4.04 tff(c_1678, plain, (icext(uri_rdf_Property, uri_rdfs_isDefinedBy))). % 11.53/4.04 tff(c_961, plain, (![C_72]: (icext(C_72, uri_rdfs_isDefinedBy) | ~iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_72)))). % 11.53/4.04 tff(c_919, plain, (![C_72]: (icext(C_72, uri_rdf__3) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_72)))). % 11.53/4.04 tff(c_932, plain, (![C_72]: (icext(C_72, uri_foaf_mbox_sha1sum) | ~iext(uri_rdfs_domain, uri_rdf_type, C_72)))). % 11.53/4.04 tff(c_918, plain, (![C_72]: (icext(C_72, uri_ex_robert) | ~iext(uri_rdfs_domain, uri_foaf_mbox_sha1sum, C_72)))). % 11.53/4.04 tff(c_1646, plain, (icext(uri_rdf_Property, uri_rdfs_domain))). % 11.53/4.04 tff(c_938, plain, (![C_72]: (icext(C_72, uri_rdf_first) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_72)))). % 11.53/4.04 tff(c_974, plain, (![C_72]: (icext(C_72, uri_rdfs_domain) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_72)))). % 11.53/4.04 tff(c_975, plain, (![C_72]: (icext(C_72, uri_rdf_object) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_72)))). % 11.53/4.04 tff(c_1627, plain, (icext(uri_rdf_Property, uri_rdfs_subClassOf))). % 11.53/4.04 tff(c_952, plain, (![C_72]: (icext(C_72, uri_rdfs_subClassOf) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_72)))). % 11.53/4.04 tff(c_640, plain, (![P_63]: (ip(P_63) | ~icext(uri_rdfs_ContainerMembershipProperty, P_63)))). % 11.53/4.04 tff(c_1605, plain, (ip(uri_rdfs_member))). % 11.53/4.04 tff(c_717, plain, (![P_6]: (icext(uri_rdf_Property, P_6) | ~ip(P_6)))). % 11.53/4.04 tff(c_653, plain, (![X_64]: (ip(X_64) | ~icext(uri_rdf_Property, X_64)))). % 11.53/4.04 tff(c_751, plain, (![D_68]: (ic(D_68) | ~icext(uri_rdfs_Datatype, D_68)))). % 11.53/4.04 tff(c_1538, plain, (ic(uri_rdfs_Resource))). % 11.53/4.04 tff(c_734, plain, (icext(uri_rdfs_Datatype, uri_rdf_XMLLiteral))). % 11.53/4.04 tff(c_722, plain, (icext(uri_owl_DatatypeProperty, uri_foaf_mbox_sha1sum))). % 11.53/4.04 tff(c_718, plain, (icext(uri_rdf_Property, uri_rdf_rest))). % 11.53/4.04 tff(c_727, plain, (icext(uri_rdf_Property, uri_rdf_value))). % 11.53/4.04 tff(c_723, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__3))). % 11.53/4.04 tff(c_719, plain, (icext(uri_owl_InverseFunctionalProperty, uri_foaf_mbox_sha1sum))). % 11.53/4.04 tff(c_730, plain, (icext(uri_rdf_Property, uri_rdf_object))). % 11.53/4.04 tff(c_721, plain, (icext(uri_rdfs_Class, uri_rdf_Property))). % 11.53/4.04 tff(c_733, plain, (icext(uri_rdf_List, uri_rdf_nil))). % 11.53/4.04 tff(c_731, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__2))). % 11.53/4.04 tff(c_728, plain, (icext(uri_rdf_Property, uri_rdf__1))). % 11.53/4.04 tff(c_725, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__1))). % 11.53/4.04 tff(c_724, plain, (icext(uri_rdf_Property, uri_rdf_type))). % 11.53/4.04 tff(c_732, plain, (icext(uri_rdf_Property, uri_rdf_first))). % 11.53/4.04 tff(c_729, plain, (icext(uri_rdf_Property, uri_rdf_subject))). % 11.53/4.04 tff(c_720, plain, (icext(uri_rdf_Property, uri_rdf__2))). % 11.53/4.04 tff(c_726, plain, (icext(uri_rdf_Property, uri_rdf__3))). % 11.53/4.04 tff(c_170, plain, (![P_38, R_40, Q_39]: (iext(uri_rdfs_subPropertyOf, P_38, R_40) | ~iext(uri_rdfs_subPropertyOf, Q_39, R_40) | ~iext(uri_rdfs_subPropertyOf, P_38, Q_39)))). % 11.53/4.04 tff(c_160, plain, (![Q_32, X_35, Y_36, P_31]: (iext(Q_32, X_35, Y_36) | ~iext(P_31, X_35, Y_36) | ~iext(uri_rdfs_subPropertyOf, P_31, Q_32)))). % 11.53/4.04 tff(c_156, plain, (![C_28, E_30, D_29]: (iext(uri_rdfs_subClassOf, C_28, E_30) | ~iext(uri_rdfs_subClassOf, D_29, E_30) | ~iext(uri_rdfs_subClassOf, C_28, D_29)))). % 11.53/4.04 tff(c_128, plain, (![C_20, Y_22, P_19, X_21]: (icext(C_20, Y_22) | ~iext(P_19, X_21, Y_22) | ~iext(uri_rdfs_range, P_19, C_20)))). % 11.53/4.04 tff(c_590, plain, (ip(uri_rdfs_subPropertyOf))). % 11.53/4.04 tff(c_108, plain, (![C_13, X_14, P_12, Y_15]: (icext(C_13, X_14) | ~iext(P_12, X_14, Y_15) | ~iext(uri_rdfs_domain, P_12, C_13)))). % 11.53/4.04 tff(c_551, plain, (ip(uri_rdfs_subClassOf))). % 11.53/4.04 tff(c_146, plain, (![D_24, X_26, C_23]: (icext(D_24, X_26) | ~icext(C_23, X_26) | ~iext(uri_rdfs_subClassOf, C_23, D_24)))). % 11.53/4.04 tff(c_102, plain, (![D_11]: (iext(uri_rdfs_subClassOf, D_11, uri_rdfs_Literal) | ~icext(uri_rdfs_Datatype, D_11)))). % 11.53/4.04 tff(c_52, plain, (![C_8, X_7]: (icext(C_8, X_7) | ~iext(uri_rdf_type, X_7, C_8)))). % 11.53/4.04 tff(c_286, plain, (ip(uri_rdf_value))). % 11.53/4.04 tff(c_54, plain, (![X_7, C_8]: (iext(uri_rdf_type, X_7, C_8) | ~icext(C_8, X_7)))). % 11.53/4.04 tff(c_290, plain, (ip(uri_rdf_first))). % 11.53/4.04 tff(c_70, plain, (![P_10]: (iext(uri_rdfs_subPropertyOf, P_10, uri_rdfs_member) | ~icext(uri_rdfs_ContainerMembershipProperty, P_10)))). % 11.53/4.04 tff(c_603, plain, (ip(uri_rdfs_domain))). % 11.53/4.04 tff(c_534, plain, (ip(uri_foaf_mbox_sha1sum))). % 11.53/4.04 tff(c_542, plain, (ip(uri_rdfs_range))). % 11.53/4.04 tff(c_168, plain, (![P_37]: (iext(uri_rdfs_subPropertyOf, P_37, P_37) | ~ip(P_37)))). % 11.53/4.04 tff(c_318, plain, (ic(uri_rdfs_Literal))). % 11.53/4.04 tff(c_283, plain, (ip(uri_rdf__2))). % 11.53/4.04 tff(c_285, plain, (ip(uri_rdf__3))). % 11.53/4.04 tff(c_2, plain, (![P_2, S_1, O_3]: (ip(P_2) | ~iext(P_2, S_1, O_3)))). % 11.53/4.04 tff(c_320, plain, (ic(uri_rdf_Property))). % 11.53/4.04 tff(c_284, plain, (ip(uri_rdf_type))). % 11.53/4.04 tff(c_321, plain, (ic(uri_rdfs_Class))). % 11.53/4.04 tff(c_289, plain, (ip(uri_rdf_object))). % 11.53/4.04 tff(c_28, plain, (![P_6]: (iext(uri_rdf_type, P_6, uri_rdf_Property) | ~ip(P_6)))). % 11.53/4.04 tff(c_322, plain, (ic(uri_rdfs_Container))). % 11.53/4.04 tff(c_287, plain, (ip(uri_rdf__1))). % 11.53/4.04 tff(c_288, plain, (ip(uri_rdf_subject))). % 11.53/4.04 tff(c_148, plain, (![D_24, C_23]: (ic(D_24) | ~iext(uri_rdfs_subClassOf, C_23, D_24)))). % 11.53/4.04 tff(c_282, plain, (ip(uri_rdf_rest))). % 11.53/4.04 tff(c_26, plain, (![P_6]: (ip(P_6) | ~iext(uri_rdf_type, P_6, uri_rdf_Property)))). % 11.53/4.04 tff(c_253, plain, (ip(uri_rdfs_seeAlso))). % 11.53/4.04 tff(c_248, plain, (ip(uri_rdfs_isDefinedBy))). % 11.53/4.04 tff(c_240, plain, (ic(uri_rdfs_ContainerMembershipProperty))). % 11.53/4.04 tff(c_162, plain, (![Q_32, P_31]: (ip(Q_32) | ~iext(uri_rdfs_subPropertyOf, P_31, Q_32)))). % 11.53/4.04 tff(c_241, plain, (ic(uri_rdfs_Datatype))). % 11.53/4.04 tff(c_242, plain, (ic(uri_rdf_Bag))). % 11.53/4.04 tff(c_239, plain, (ic(uri_rdfs_Seq))). % 11.53/4.04 tff(c_164, plain, (![P_31, Q_32]: (ip(P_31) | ~iext(uri_rdfs_subPropertyOf, P_31, Q_32)))). % 11.53/4.04 tff(c_243, plain, (ic(uri_rdf_Alt))). % 11.53/4.04 tff(c_238, plain, (ic(uri_rdf_XMLLiteral))). % 11.53/4.04 tff(c_150, plain, (![C_23, D_24]: (ic(C_23) | ~iext(uri_rdfs_subClassOf, C_23, D_24)))). % 11.53/4.04 tff(c_56, plain, (![C_9]: (iext(uri_rdfs_subClassOf, C_9, uri_rdfs_Resource) | ~ic(C_9)))). % 11.53/4.04 tff(c_154, plain, (![C_27]: (iext(uri_rdfs_subClassOf, C_27, C_27) | ~ic(C_27)))). % 11.53/4.04 tff(c_120, plain, (![X_18]: (icext(uri_rdfs_Literal, X_18) | ~lv(X_18)))). % 11.53/4.04 tff(c_112, plain, (![X_16]: (icext(uri_rdfs_Class, X_16) | ~ic(X_16)))). % 11.53/4.04 tff(c_122, plain, (![X_18]: (lv(X_18) | ~icext(uri_rdfs_Literal, X_18)))). % 11.53/4.04 tff(c_184, plain, (iext(uri_foaf_mbox_sha1sum, uri_ex_bob, literal_plain(dat_str_xyz)))). % 11.53/4.04 tff(c_182, plain, (iext(uri_foaf_mbox_sha1sum, uri_ex_robert, literal_plain(dat_str_xyz)))). % 11.53/4.04 tff(c_114, plain, (![X_16]: (ic(X_16) | ~icext(uri_rdfs_Class, X_16)))). % 11.53/4.04 tff(c_82, plain, (iext(uri_rdfs_domain, uri_rdf__3, uri_rdfs_Resource))). % 11.53/4.04 tff(c_140, plain, (iext(uri_rdfs_domain, uri_rdf_subject, uri_rdfs_Statement))). % 11.53/4.04 tff(c_130, plain, (iext(uri_rdfs_range, uri_rdfs_range, uri_rdfs_Class))). % 11.53/4.04 tff(c_78, plain, (iext(uri_rdfs_domain, uri_rdf__1, uri_rdfs_Resource))). % 11.53/4.04 tff(c_36, plain, (iext(uri_rdfs_range, uri_rdfs_comment, uri_rdfs_Literal))). % 11.53/4.04 tff(c_12, plain, (iext(uri_rdf_type, uri_rdf_rest, uri_rdf_Property))). % 11.53/4.04 tff(c_178, plain, (iext(uri_rdfs_range, uri_rdf_value, uri_rdfs_Resource))). % 11.53/4.04 tff(c_186, plain, (iext(uri_rdf_type, uri_foaf_mbox_sha1sum, uri_owl_InverseFunctionalProperty))). % 11.53/4.04 tff(c_98, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Literal))). % 11.53/4.04 tff(c_144, plain, (iext(uri_rdfs_domain, uri_rdfs_subClassOf, uri_rdfs_Class))). % 11.53/4.04 tff(c_16, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdf_Property))). % 11.53/4.04 tff(c_124, plain, (iext(uri_rdf_type, uri_rdf_Property, uri_rdfs_Class))). % 11.53/4.04 tff(c_96, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Container))). % 11.53/4.04 tff(c_188, plain, (iext(uri_rdf_type, uri_foaf_mbox_sha1sum, uri_owl_DatatypeProperty))). % 11.53/4.04 tff(c_166, plain, (iext(uri_rdfs_range, uri_rdfs_subPropertyOf, uri_rdf_Property))). % 11.53/4.04 tff(c_94, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdfs_ContainerMembershipProperty))). % 11.53/4.04 tff(c_32, plain, (iext(uri_rdf_type, uri_rdf_type, uri_rdf_Property))). % 11.53/4.04 tff(c_126, plain, (iext(uri_rdfs_domain, uri_rdfs_range, uri_rdf_Property))). % 11.53/4.04 tff(c_90, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdfs_ContainerMembershipProperty))). % 11.53/4.04 tff(c_60, plain, (iext(uri_rdfs_range, uri_rdf_first, uri_rdfs_Resource))). % 11.53/4.04 tff(c_88, plain, (iext(uri_rdfs_range, uri_rdf__3, uri_rdfs_Resource))). % 11.53/4.04 tff(c_48, plain, (iext(uri_rdfs_domain, uri_rdfs_seeAlso, uri_rdfs_Resource))). % 11.53/4.04 tff(c_86, plain, (iext(uri_rdfs_range, uri_rdf__2, uri_rdfs_Resource))). % 11.53/4.04 tff(c_18, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdf_Property))). % 11.53/4.04 tff(c_172, plain, (iext(uri_rdfs_domain, uri_rdf_type, uri_rdfs_Resource))). % 11.53/4.04 tff(c_22, plain, (iext(uri_rdf_type, uri_rdf_value, uri_rdf_Property))). % 11.53/4.05 tff(c_46, plain, (iext(uri_rdfs_range, uri_rdfs_label, uri_rdfs_Literal))). % 11.53/4.05 tff(c_62, plain, (iext(uri_rdfs_domain, uri_rdf_rest, uri_rdf_List))). % 11.53/4.05 tff(c_14, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdf_Property))). % 11.53/4.05 tff(c_24, plain, (iext(uri_rdf_type, uri_rdf_subject, uri_rdf_Property))). % 11.53/4.05 tff(c_20, plain, (iext(uri_rdf_type, uri_rdf_object, uri_rdf_Property))). % 11.53/4.05 tff(c_72, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property))). % 11.53/4.05 tff(c_104, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Class))). % 11.53/4.05 tff(c_152, plain, (iext(uri_rdfs_range, uri_rdfs_subClassOf, uri_rdfs_Class))). % 11.53/4.05 tff(c_38, plain, (iext(uri_rdfs_domain, uri_rdfs_isDefinedBy, uri_rdfs_Resource))). % 11.53/4.05 tff(c_64, plain, (iext(uri_rdfs_range, uri_rdf_rest, uri_rdf_List))). % 11.53/4.05 tff(c_84, plain, (iext(uri_rdfs_range, uri_rdf__1, uri_rdfs_Resource))). % 11.53/4.05 tff(c_142, plain, (iext(uri_rdfs_range, uri_rdf_subject, uri_rdfs_Resource))). % 11.53/4.05 tff(c_76, plain, (iext(uri_rdfs_range, uri_rdfs_member, uri_rdfs_Resource))). % 11.53/4.05 tff(c_68, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Container))). % 11.53/4.05 tff(c_66, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Container))). % 11.53/4.05 tff(c_136, plain, (iext(uri_rdfs_domain, uri_rdf_predicate, uri_rdfs_Statement))). % 11.53/4.05 tff(c_42, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso))). % 11.53/4.05 tff(c_34, plain, (iext(uri_rdfs_domain, uri_rdfs_comment, uri_rdfs_Resource))). % 11.53/4.05 tff(c_40, plain, (iext(uri_rdfs_range, uri_rdfs_isDefinedBy, uri_rdfs_Resource))). % 11.53/4.05 tff(c_80, plain, (iext(uri_rdfs_domain, uri_rdf__2, uri_rdfs_Resource))). % 11.53/4.05 tff(c_110, plain, (iext(uri_rdfs_range, uri_rdfs_domain, uri_rdfs_Class))). % 11.53/4.05 tff(c_92, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdfs_ContainerMembershipProperty))). % 11.53/4.05 tff(c_138, plain, (iext(uri_rdfs_range, uri_rdf_predicate, uri_rdfs_Resource))). % 11.53/4.05 tff(c_50, plain, (iext(uri_rdfs_range, uri_rdfs_seeAlso, uri_rdfs_Resource))). % 11.53/4.05 tff(c_58, plain, (iext(uri_rdfs_domain, uri_rdf_first, uri_rdf_List))). % 11.53/4.05 tff(c_176, plain, (iext(uri_rdfs_domain, uri_rdf_value, uri_rdfs_Resource))). % 11.53/4.05 tff(c_44, plain, (iext(uri_rdfs_domain, uri_rdfs_label, uri_rdfs_Resource))). % 11.53/4.05 tff(c_74, plain, (iext(uri_rdfs_domain, uri_rdfs_member, uri_rdfs_Resource))). % 11.53/4.05 tff(c_180, plain, (~iext(uri_owl_sameAs, uri_ex_bob, uri_ex_robert))). % 11.53/4.05 tff(c_158, plain, (iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, uri_rdf_Property))). % 11.53/4.05 tff(c_106, plain, (iext(uri_rdfs_domain, uri_rdfs_domain, uri_rdf_Property))). % 11.53/4.05 tff(c_132, plain, (iext(uri_rdfs_domain, uri_rdf_object, uri_rdfs_Statement))). % 11.53/4.05 tff(c_174, plain, (iext(uri_rdfs_range, uri_rdf_type, uri_rdfs_Class))). % 11.53/4.05 tff(c_8, plain, (iext(uri_rdf_type, uri_rdf_first, uri_rdf_Property))). % 11.53/4.05 tff(c_10, plain, (iext(uri_rdf_type, uri_rdf_nil, uri_rdf_List))). % 11.53/4.05 tff(c_100, plain, (iext(uri_rdf_type, uri_rdf_XMLLiteral, uri_rdfs_Datatype))). % 11.53/4.05 tff(c_193, plain, (![X_17]: (icext(uri_rdfs_Resource, X_17)))). % 11.53/4.05 tff(c_4, plain, (![X_4]: (ir(X_4)))). % 11.53/4.05 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 11.53/4.05 %------------------------------------------------------------------------------