%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SWB004+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:45 PM UTC 2025 % Result : CounterSatisfiable 11.69s 3.83s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SWB004+4 : TPTP v9.0.0. Released v5.2.0. % 0.03/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.33 % Computer : n021.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Wed Apr 9 00:53:14 EDT 2025 % 0.12/0.34 % CPUTime : % 11.69/3.83 % 11.69/3.83 % SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 11.69/3.83 % 11.69/3.83 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 11.76/3.84 %$ iext > icext > lv > ir > ip > ic > #nlpp > 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_equivalentClass > uri_owl_Thing > uri_owl_Class % 11.76/3.84 % 11.76/3.84 %Foreground sorts: % 11.76/3.84 % 11.76/3.84 % 11.76/3.84 %Background operators: % 11.76/3.84 % 11.76/3.84 % 11.76/3.84 %Foreground operators: % 11.76/3.84 tff(uri_rdfs_Datatype, type, uri_rdfs_Datatype: $i). % 11.76/3.84 tff(uri_rdfs_ContainerMembershipProperty, type, uri_rdfs_ContainerMembershipProperty: $i). % 11.76/3.84 tff(uri_rdfs_Resource, type, uri_rdfs_Resource: $i). % 11.76/3.84 tff(uri_rdf_Property, type, uri_rdf_Property: $i). % 11.76/3.84 tff(uri_rdf_subject, type, uri_rdf_subject: $i). % 11.76/3.84 tff(uri_owl_equivalentClass, type, uri_owl_equivalentClass: $i). % 11.76/3.84 tff(uri_rdf_type, type, uri_rdf_type: $i). % 11.76/3.84 tff(uri_rdfs_subPropertyOf, type, uri_rdfs_subPropertyOf: $i). % 11.76/3.84 tff(uri_rdfs_seeAlso, type, uri_rdfs_seeAlso: $i). % 11.76/3.84 tff(uri_rdfs_range, type, uri_rdfs_range: $i). % 11.76/3.84 tff(uri_rdf_XMLLiteral, type, uri_rdf_XMLLiteral: $i). % 11.76/3.84 tff(uri_rdf_List, type, uri_rdf_List: $i). % 11.76/3.84 tff(uri_rdf_first, type, uri_rdf_first: $i). % 11.76/3.84 tff(uri_rdf_predicate, type, uri_rdf_predicate: $i). % 11.76/3.84 tff(uri_owl_Thing, type, uri_owl_Thing: $i). % 11.76/3.84 tff(uri_rdf__3, type, uri_rdf__3: $i). % 11.76/3.84 tff(icext, type, icext: ($i * $i) > $o). % 11.76/3.84 tff(uri_rdf_value, type, uri_rdf_value: $i). % 11.76/3.84 tff(ip, type, ip: $i > $o). % 11.76/3.84 tff(uri_rdfs_Statement, type, uri_rdfs_Statement: $i). % 11.76/3.84 tff(uri_rdf__1, type, uri_rdf__1: $i). % 11.76/3.84 tff(lv, type, lv: $i > $o). % 11.76/3.84 tff(ir, type, ir: $i > $o). % 11.76/3.84 tff(uri_rdf_rest, type, uri_rdf_rest: $i). % 11.76/3.84 tff(uri_rdfs_label, type, uri_rdfs_label: $i). % 11.76/3.84 tff(uri_rdfs_Container, type, uri_rdfs_Container: $i). % 11.76/3.84 tff(ic, type, ic: $i > $o). % 11.76/3.84 tff(uri_rdfs_subClassOf, type, uri_rdfs_subClassOf: $i). % 11.76/3.84 tff(uri_rdf_object, type, uri_rdf_object: $i). % 11.76/3.84 tff(uri_rdfs_Class, type, uri_rdfs_Class: $i). % 11.76/3.84 tff(uri_rdfs_Seq, type, uri_rdfs_Seq: $i). % 11.76/3.84 tff(uri_owl_Class, type, uri_owl_Class: $i). % 11.76/3.84 tff(iext, type, iext: ($i * $i * $i) > $o). % 11.76/3.84 tff(uri_rdfs_member, type, uri_rdfs_member: $i). % 11.76/3.84 tff(uri_rdf_Bag, type, uri_rdf_Bag: $i). % 11.76/3.84 tff(uri_rdf__2, type, uri_rdf__2: $i). % 11.76/3.84 tff(uri_rdfs_comment, type, uri_rdfs_comment: $i). % 11.76/3.84 tff(uri_rdfs_Literal, type, uri_rdfs_Literal: $i). % 11.76/3.84 tff(uri_rdf_Alt, type, uri_rdf_Alt: $i). % 11.76/3.84 tff(uri_rdf_nil, type, uri_rdf_nil: $i). % 11.76/3.84 tff(uri_rdfs_isDefinedBy, type, uri_rdfs_isDefinedBy: $i). % 11.76/3.84 tff(uri_rdfs_domain, type, uri_rdfs_domain: $i). % 11.76/3.84 % 11.76/3.84 %Saturated clause set: % 11.76/3.84 tff(c_6848, plain, (![C_28, C_318]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, C_318) | ~iext(uri_rdfs_subClassOf, C_318, uri_rdfs_Datatype)))). % 11.76/3.84 tff(c_5448, plain, (![C_28, C_310]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, C_310) | ~iext(uri_rdfs_subClassOf, C_310, uri_rdfs_ContainerMembershipProperty)))). % 11.76/3.84 tff(c_5449, plain, (![Q_32, C_310]: (iext(Q_32, C_310, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_310, uri_rdfs_ContainerMembershipProperty)))). % 11.76/3.84 tff(c_6849, plain, (![Q_32, C_318]: (iext(Q_32, C_318, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_318, uri_rdfs_Datatype)))). % 11.76/3.84 tff(c_6544, plain, (![C_28, C_314]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, C_314) | ~iext(uri_rdfs_subClassOf, C_314, uri_rdf_XMLLiteral)))). % 11.76/3.85 tff(c_6270, plain, (![C_28, C_313]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, C_313) | ~iext(uri_rdfs_subClassOf, C_313, uri_rdf_Bag)))). % 11.76/3.85 tff(c_5996, plain, (![C_28, C_312]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, C_312) | ~iext(uri_rdfs_subClassOf, C_312, uri_rdf_Alt)))). % 11.76/3.85 tff(c_6545, plain, (![Q_32, C_314]: (iext(Q_32, C_314, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_314, uri_rdf_XMLLiteral)))). % 11.76/3.85 tff(c_5997, plain, (![Q_32, C_312]: (iext(Q_32, C_312, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_312, uri_rdf_Alt)))). % 11.76/3.85 tff(c_6271, plain, (![Q_32, C_313]: (iext(Q_32, C_313, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_313, uri_rdf_Bag)))). % 11.76/3.85 tff(c_7520, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_member, uri_rdfs_isDefinedBy))). % 11.76/3.85 tff(c_3539, plain, (![P_38, P_234]: (iext(uri_rdfs_subPropertyOf, P_38, uri_rdfs_seeAlso) | ~iext(uri_rdfs_subPropertyOf, P_38, P_234) | ~iext(uri_rdfs_subPropertyOf, P_234, uri_rdfs_isDefinedBy)))). % 11.76/3.85 tff(c_3415, plain, (![C_28, C_233]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Container) | ~iext(uri_rdfs_subClassOf, C_28, C_233) | ~iext(uri_rdfs_subClassOf, C_233, uri_rdf_Alt)))). % 11.76/3.85 tff(c_4208, plain, (![Q_32, C_251]: (iext(Q_32, C_251, uri_rdfs_Container) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_251, uri_rdf_Bag)))). % 11.76/3.85 tff(c_4207, plain, (![C_28, C_251]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Container) | ~iext(uri_rdfs_subClassOf, C_28, C_251) | ~iext(uri_rdfs_subClassOf, C_251, uri_rdf_Bag)))). % 11.76/3.85 tff(c_3416, plain, (![Q_32, C_233]: (iext(Q_32, C_233, uri_rdfs_Container) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_233, uri_rdf_Alt)))). % 11.76/3.85 tff(c_7317, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Container, uri_rdf_XMLLiteral))). % 11.76/3.85 tff(c_3940, plain, (![C_28, C_247]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Literal) | ~iext(uri_rdfs_subClassOf, C_28, C_247) | ~iext(uri_rdfs_subClassOf, C_247, uri_rdf_XMLLiteral)))). % 11.76/3.85 tff(c_3941, plain, (![Q_32, C_247]: (iext(Q_32, C_247, uri_rdfs_Literal) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_247, uri_rdf_XMLLiteral)))). % 11.76/3.85 tff(c_3538, plain, (![Q_32, P_234]: (iext(Q_32, P_234, uri_rdfs_seeAlso) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_32) | ~iext(uri_rdfs_subPropertyOf, P_234, uri_rdfs_isDefinedBy)))). % 11.76/3.85 tff(c_5722, plain, (![C_28, D_311]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, D_311) | ~icext(uri_rdfs_Datatype, D_311)))). % 11.76/3.85 tff(c_5723, plain, (![Q_32, D_311]: (iext(Q_32, D_311, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~icext(uri_rdfs_Datatype, D_311)))). % 11.76/3.85 tff(c_7110, plain, (~icext(uri_rdfs_Datatype, uri_rdfs_Container))). % 11.76/3.85 tff(c_1386, plain, (![C_87, D_11]: (iext(uri_rdfs_subClassOf, C_87, uri_rdfs_Literal) | ~iext(uri_rdfs_subClassOf, C_87, D_11) | ~icext(uri_rdfs_Datatype, D_11)))). % 11.76/3.85 tff(c_1296, 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.76/3.85 tff(c_1298, 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.76/3.85 tff(c_7004, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdfs_seeAlso))). % 11.76/3.85 tff(c_1157, plain, (![P_80, P_10]: (iext(uri_rdfs_subPropertyOf, P_80, uri_rdfs_member) | ~iext(uri_rdfs_subPropertyOf, P_80, P_10) | ~icext(uri_rdfs_ContainerMembershipProperty, P_10)))). % 11.76/3.85 tff(c_1297, 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.76/3.85 tff(c_6960, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdf_Bag))). % 11.76/3.85 tff(c_1300, 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.76/3.85 tff(c_4825, plain, (![Q_32]: (iext(Q_32, uri_rdf_XMLLiteral, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32)))). % 11.76/3.85 tff(c_6928, plain, (![P_325]: (icext(uri_rdf_Property, P_325) | ~icext(uri_rdfs_ContainerMembershipProperty, P_325)))). % 11.76/3.85 tff(c_1079, plain, (![C_76, P_10]: (icext(C_76, P_10) | ~iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_76) | ~icext(uri_rdfs_ContainerMembershipProperty, P_10)))). % 11.76/3.85 tff(c_4894, plain, (![Q_32]: (iext(Q_32, uri_rdfs_Datatype, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32)))). % 11.76/3.85 tff(c_4926, plain, (![Q_32]: (iext(Q_32, uri_rdfs_Seq, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32)))). % 11.76/3.85 tff(c_4925, plain, (![C_28]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Seq)))). % 11.76/3.85 tff(c_5009, plain, (![Q_32]: (iext(Q_32, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32)))). % 11.76/3.85 tff(c_4958, plain, (![Q_32]: (iext(Q_32, uri_rdf_Bag, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32)))). % 11.76/3.85 tff(c_4893, plain, (![C_28]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Datatype)))). % 11.76/3.85 tff(c_4857, plain, (![Q_32]: (iext(Q_32, uri_rdf_Alt, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32)))). % 11.76/3.85 tff(c_1302, 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.76/3.85 tff(c_4773, plain, (![C_87]: (iext(uri_rdfs_subClassOf, C_87, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_87, uri_rdf_XMLLiteral)))). % 11.76/3.85 tff(c_4770, plain, (![C_87]: (iext(uri_rdfs_subClassOf, C_87, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_87, uri_rdf_Bag)))). % 11.76/3.85 tff(c_4776, plain, (![C_87]: (iext(uri_rdfs_subClassOf, C_87, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_87, uri_rdf_Alt)))). % 11.76/3.85 tff(c_4779, plain, (![D_11]: (iext(uri_rdfs_subClassOf, D_11, uri_rdfs_Resource) | ~icext(uri_rdfs_Datatype, D_11)))). % 11.76/3.85 tff(c_5008, plain, (![C_28]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, uri_rdfs_ContainerMembershipProperty)))). % 11.76/3.85 tff(c_4970, plain, (![C_306, X_307]: (icext(uri_rdfs_Class, C_306) | ~icext(C_306, X_307)))). % 11.76/3.85 tff(c_4742, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdf_Alt))). % 11.76/3.85 tff(c_4801, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Resource))). % 11.76/3.85 tff(c_879, plain, (![C_72, C_8, X_7]: (icext(C_72, C_8) | ~iext(uri_rdfs_range, uri_rdf_type, C_72) | ~icext(C_8, X_7)))). % 11.76/3.85 tff(c_4798, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Resource))). % 11.76/3.85 tff(c_4795, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Resource))). % 11.76/3.86 tff(c_4792, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Resource))). % 11.76/3.86 tff(c_4789, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Resource))). % 11.76/3.86 tff(c_4786, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Resource))). % 11.76/3.86 tff(c_1388, plain, (![C_87, C_9]: (iext(uri_rdfs_subClassOf, C_87, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_87, C_9) | ~ic(C_9)))). % 11.76/3.86 tff(c_1080, plain, (![C_76, X_7, C_8]: (icext(C_76, X_7) | ~iext(uri_rdfs_domain, uri_rdf_type, C_76) | ~icext(C_8, X_7)))). % 11.76/3.86 tff(c_1301, 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.76/3.86 tff(c_4715, plain, (![C_72]: (icext(C_72, uri_rdfs_member) | ~iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_72)))). % 11.76/3.86 tff(c_4703, plain, (![D_295]: (icext(uri_rdfs_Class, D_295) | ~icext(uri_rdfs_Datatype, D_295)))). % 11.76/3.86 tff(c_1081, plain, (![C_76, D_11]: (icext(C_76, D_11) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_76) | ~icext(uri_rdfs_Datatype, D_11)))). % 11.76/3.86 tff(c_4699, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy))). % 11.76/3.86 tff(c_1487, plain, (![D_24, P_91]: (icext(D_24, P_91) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24) | ~ip(P_91)))). % 11.76/3.86 tff(c_1299, 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.76/3.86 tff(c_1083, plain, (![C_76, P_37]: (icext(C_76, P_37) | ~iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_76) | ~ip(P_37)))). % 11.76/3.86 tff(c_883, plain, (![C_72, C_27]: (icext(C_72, C_27) | ~iext(uri_rdfs_range, uri_rdfs_subClassOf, C_72) | ~ic(C_27)))). % 11.76/3.86 tff(c_882, plain, (![C_72, P_37]: (icext(C_72, P_37) | ~iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_72) | ~ip(P_37)))). % 11.76/3.86 tff(c_1082, plain, (![C_76, P_6]: (icext(C_76, P_6) | ~iext(uri_rdfs_domain, uri_rdf_type, C_76) | ~ip(P_6)))). % 11.76/3.86 tff(c_4631, plain, (![C_72]: (icext(C_72, uri_rdfs_Resource) | ~iext(uri_rdfs_range, uri_rdfs_subClassOf, C_72)))). % 11.76/3.86 tff(c_4611, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdf_type, uri_rdfs_isDefinedBy))). % 11.76/3.86 tff(c_1084, plain, (![C_76, C_27]: (icext(C_76, C_27) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_76) | ~ic(C_27)))). % 11.76/3.86 tff(c_739, plain, (![D_69, X_16]: (icext(D_69, X_16) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_69) | ~ic(X_16)))). % 11.76/3.86 tff(c_738, plain, (![D_69, X_18]: (icext(D_69, X_18) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Literal, D_69) | ~lv(X_18)))). % 11.76/3.86 tff(c_4548, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, uri_rdfs_isDefinedBy))). % 11.76/3.86 tff(c_4547, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, uri_rdfs_isDefinedBy))). % 11.76/3.86 tff(c_4546, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, uri_rdfs_isDefinedBy))). % 11.76/3.86 tff(c_1346, plain, (![Q_83]: (iext(Q_83, uri_rdfs_comment, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))). % 11.76/3.86 tff(c_1357, plain, (![Q_83]: (iext(Q_83, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_83)))). % 11.76/3.86 tff(c_1394, plain, (![C_87]: (iext(uri_rdfs_subClassOf, C_87, uri_rdf_Property) | ~iext(uri_rdfs_subClassOf, C_87, uri_rdfs_ContainerMembershipProperty)))). % 11.76/3.86 tff(c_1313, plain, (![Q_83]: (iext(Q_83, uri_rdf__2, uri_rdfs_ContainerMembershipProperty) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))). % 11.76/3.86 tff(c_1324, plain, (![Q_83]: (iext(Q_83, uri_rdfs_member, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))). % 11.76/3.86 tff(c_1360, plain, (![Q_83]: (iext(Q_83, uri_rdf__3, uri_rdfs_ContainerMembershipProperty) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))). % 11.76/3.86 tff(c_1345, plain, (![Q_83]: (iext(Q_83, uri_rdf_value, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))). % 11.76/3.86 tff(c_1319, plain, (![Q_83]: (iext(Q_83, uri_rdfs_subPropertyOf, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))). % 11.76/3.86 tff(c_1325, plain, (![Q_83]: (iext(Q_83, uri_rdf__3, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))). % 11.76/3.86 tff(c_1322, plain, (![Q_83]: (iext(Q_83, uri_rdf__1, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))). % 11.76/3.86 tff(c_1391, plain, (![C_87]: (iext(uri_rdfs_subClassOf, C_87, uri_rdfs_Class) | ~iext(uri_rdfs_subClassOf, C_87, uri_rdfs_Datatype)))). % 11.76/3.86 tff(c_1347, plain, (![Q_83]: (iext(Q_83, uri_rdf_rest, uri_rdf_List) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))). % 11.76/3.86 tff(c_1341, plain, (![Q_83]: (iext(Q_83, uri_rdfs_comment, uri_rdfs_Literal) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))). % 11.76/3.86 tff(c_1328, plain, (![Q_83]: (iext(Q_83, uri_rdfs_subPropertyOf, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))). % 11.76/3.86 tff(c_1312, plain, (![Q_83]: (iext(Q_83, uri_rdf__1, uri_rdfs_ContainerMembershipProperty) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))). % 11.76/3.86 tff(c_1306, plain, (![Q_83]: (iext(Q_83, uri_rdf_XMLLiteral, uri_rdfs_Literal) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_83)))). % 11.76/3.86 tff(c_1330, plain, (![Q_83]: (iext(Q_83, uri_rdf_Property, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))). % 11.76/3.86 tff(c_4304, plain, (~iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdf_Bag))). % 11.76/3.86 tff(c_1348, plain, (![Q_83]: (iext(Q_83, uri_rdf_rest, uri_rdf_List) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))). % 11.76/3.86 tff(c_4288, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdf_Bag))). % 11.76/3.86 tff(c_1361, plain, (![Q_83]: (iext(Q_83, uri_rdf_subject, uri_rdfs_Statement) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))). % 11.76/3.86 tff(c_4264, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdf_Bag))). % 11.76/3.86 tff(c_1392, plain, (![C_87]: (iext(uri_rdfs_subClassOf, C_87, uri_rdfs_Container) | ~iext(uri_rdfs_subClassOf, C_87, uri_rdfs_Seq)))). % 11.76/3.86 tff(c_4263, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdf_Bag))). % 11.76/3.86 tff(c_1358, plain, (![Q_83]: (iext(Q_83, uri_rdf_nil, uri_rdf_List) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))). % 11.76/3.86 tff(c_4232, plain, (~iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdf_Bag))). % 11.76/3.86 tff(c_1332, plain, (![Q_83]: (iext(Q_83, uri_rdf_object, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))). % 11.76/3.86 tff(c_1337, plain, (![Q_83]: (iext(Q_83, uri_rdf_Alt, uri_rdfs_Container) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_83)))). % 11.76/3.86 tff(c_4216, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Resource, uri_rdf_Bag))). % 11.76/3.86 tff(c_1393, plain, (![C_87]: (iext(uri_rdfs_subClassOf, C_87, uri_rdfs_Container) | ~iext(uri_rdfs_subClassOf, C_87, uri_rdf_Bag)))). % 11.76/3.86 tff(c_3999, plain, (~iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdf_XMLLiteral))). % 11.76/3.86 tff(c_1323, plain, (![Q_83]: (iext(Q_83, uri_rdfs_seeAlso, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))). % 11.76/3.86 tff(c_3983, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdf_XMLLiteral))). % 11.76/3.86 tff(c_3967, plain, (~iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdf_XMLLiteral))). % 11.76/3.86 tff(c_1314, plain, (![Q_83]: (iext(Q_83, uri_rdf_rest, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))). % 11.76/3.86 tff(c_3966, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdf_XMLLiteral))). % 11.76/3.86 tff(c_3965, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdf_XMLLiteral))). % 11.76/3.86 tff(c_1326, plain, (![Q_83]: (iext(Q_83, uri_rdf_type, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))). % 11.76/3.86 tff(c_3949, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Resource, uri_rdf_XMLLiteral))). % 11.76/3.87 tff(c_1389, plain, (![C_87]: (iext(uri_rdfs_subClassOf, C_87, uri_rdfs_Literal) | ~iext(uri_rdfs_subClassOf, C_87, uri_rdf_XMLLiteral)))). % 11.76/3.87 tff(c_1318, plain, (![Q_83]: (iext(Q_83, uri_rdf_value, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))). % 11.76/3.87 tff(c_1315, plain, (![Q_83]: (iext(Q_83, uri_rdf__3, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))). % 11.76/3.87 tff(c_1308, plain, (![Q_83]: (iext(Q_83, uri_rdfs_label, uri_rdfs_Literal) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))). % 11.76/3.87 tff(c_1350, plain, (![Q_83]: (iext(Q_83, uri_rdfs_domain, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))). % 11.76/3.87 tff(c_1329, plain, (![Q_83]: (iext(Q_83, uri_rdfs_seeAlso, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))). % 11.76/3.87 tff(c_1342, plain, (![Q_83]: (iext(Q_83, uri_rdf_value, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))). % 11.76/3.87 tff(c_1356, plain, (![Q_83]: (iext(Q_83, uri_rdfs_domain, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))). % 11.76/3.87 tff(c_1343, plain, (![Q_83]: (iext(Q_83, uri_rdf_first, uri_rdf_List) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))). % 11.76/3.87 tff(c_3612, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdf_Alt))). % 11.76/3.87 tff(c_1352, plain, (![Q_83]: (iext(Q_83, uri_rdfs_range, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))). % 11.76/3.87 tff(c_1304, plain, (![Q_83]: (iext(Q_83, uri_rdf_XMLLiteral, uri_rdfs_Datatype) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))). % 11.76/3.87 tff(c_3581, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdf_Alt))). % 11.76/3.87 tff(c_1334, plain, (![Q_83]: (iext(Q_83, uri_rdf_object, uri_rdfs_Statement) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))). % 11.76/3.87 tff(c_3565, plain, (~iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdf_Alt))). % 11.76/3.87 tff(c_3549, plain, (~iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdf_Alt))). % 11.76/3.87 tff(c_1338, plain, (![Q_83]: (iext(Q_83, uri_rdf_first, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))). % 11.76/3.87 tff(c_3548, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdf_Alt))). % 11.76/3.87 tff(c_3547, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Resource, uri_rdf_Alt))). % 11.76/3.87 tff(c_1159, plain, (![P_80]: (iext(uri_rdfs_subPropertyOf, P_80, uri_rdfs_seeAlso) | ~iext(uri_rdfs_subPropertyOf, P_80, uri_rdfs_isDefinedBy)))). % 11.76/3.87 tff(c_1390, plain, (![C_87]: (iext(uri_rdfs_subClassOf, C_87, uri_rdfs_Container) | ~iext(uri_rdfs_subClassOf, C_87, uri_rdf_Alt)))). % 11.76/3.87 tff(c_1305, plain, (![Q_83]: (iext(Q_83, uri_rdfs_member, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))). % 11.76/3.87 tff(c_1344, plain, (![Q_83]: (iext(Q_83, uri_rdfs_Seq, uri_rdfs_Container) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_83)))). % 11.76/3.87 tff(c_1333, plain, (![Q_83]: (iext(Q_83, uri_rdf_subject, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))). % 11.76/3.87 tff(c_1317, plain, (![Q_83]: (iext(Q_83, uri_rdf_predicate, uri_rdfs_Statement) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))). % 11.76/3.87 tff(c_1353, plain, (![Q_83]: (iext(Q_83, uri_rdf_Bag, uri_rdfs_Container) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_83)))). % 11.76/3.87 tff(c_1349, plain, (![Q_83]: (iext(Q_83, uri_rdfs_isDefinedBy, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))). % 11.76/3.87 tff(c_1321, plain, (![Q_83]: (iext(Q_83, uri_rdf_subject, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))). % 11.76/3.87 tff(c_3119, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdfs_subClassOf))). % 11.76/3.87 tff(c_1310, plain, (![Q_83]: (iext(Q_83, uri_rdf__2, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))). % 11.76/3.87 tff(c_1339, plain, (![Q_83]: (iext(Q_83, uri_rdfs_Datatype, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_83)))). % 11.76/3.87 tff(c_1311, plain, (![Q_83]: (iext(Q_83, uri_rdf__3, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))). % 11.76/3.87 tff(c_1331, plain, (![Q_83]: (iext(Q_83, uri_rdfs_subClassOf, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))). % 11.76/3.87 tff(c_1303, plain, (![Q_83]: (iext(Q_83, uri_rdf_type, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))). % 11.76/3.87 tff(c_1351, plain, (![Q_83]: (iext(Q_83, uri_rdfs_subClassOf, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))). % 11.76/3.87 tff(c_1355, plain, (![Q_83]: (iext(Q_83, uri_rdf__1, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))). % 11.76/3.87 tff(c_1336, plain, (![Q_83]: (iext(Q_83, uri_rdfs_label, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))). % 11.76/3.87 tff(c_3030, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdfs_subPropertyOf))). % 11.76/3.87 tff(c_1340, plain, (![Q_83]: (iext(Q_83, uri_rdfs_range, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))). % 11.76/3.87 tff(c_1335, plain, (![Q_83]: (iext(Q_83, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_83)))). % 11.76/3.87 tff(c_1354, plain, (![Q_83]: (iext(Q_83, uri_rdf__2, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))). % 11.76/3.87 tff(c_1327, plain, (![Q_83]: (iext(Q_83, uri_rdf_type, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))). % 11.76/3.87 tff(c_1904, plain, (![D_24]: (icext(D_24, uri_rdfs_domain) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))). % 11.76/3.87 tff(c_1741, plain, (![D_24]: (icext(D_24, uri_rdfs_Literal) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))). % 11.76/3.87 tff(c_1618, plain, (![D_24]: (icext(D_24, uri_rdf_List) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))). % 11.76/3.87 tff(c_1675, plain, (![D_24]: (icext(D_24, uri_rdfs_isDefinedBy) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))). % 11.76/3.87 tff(c_1710, plain, (![D_24]: (icext(D_24, uri_rdfs_Statement) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))). % 11.76/3.87 tff(c_1724, plain, (![D_24]: (icext(D_24, uri_rdfs_member) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))). % 11.76/3.87 tff(c_1824, plain, (![D_24]: (icext(D_24, uri_rdfs_seeAlso) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))). % 11.76/3.87 tff(c_1760, plain, (![D_24]: (icext(D_24, uri_rdfs_Container) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))). % 11.76/3.87 tff(c_1693, plain, (![D_24]: (icext(D_24, uri_rdf_predicate) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))). % 11.76/3.87 tff(c_1307, plain, (![Q_83]: (iext(Q_83, uri_rdf__1, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))). % 11.76/3.87 tff(c_1787, plain, (![D_24]: (icext(D_24, uri_rdfs_range) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))). % 11.76/3.87 tff(c_1599, plain, (![D_24]: (icext(D_24, uri_rdfs_ContainerMembershipProperty) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))). % 11.76/3.87 tff(c_1630, plain, (![D_24]: (icext(D_24, uri_rdfs_Datatype) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))). % 11.76/3.87 tff(c_1854, plain, (![D_24]: (icext(D_24, uri_rdfs_comment) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))). % 11.76/3.87 tff(c_1580, plain, (![D_24]: (icext(D_24, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))). % 11.76/3.87 tff(c_1989, plain, (![D_24]: (icext(D_24, uri_rdfs_Seq) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))). % 11.76/3.87 tff(c_1883, plain, (![D_24]: (icext(D_24, uri_rdf_Alt) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))). % 11.76/3.87 tff(c_2665, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdf_type))). % 11.76/3.87 tff(c_1359, plain, (![Q_83]: (iext(Q_83, uri_rdf_first, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))). % 11.76/3.87 tff(c_2065, plain, (![D_24]: (icext(D_24, uri_rdfs_subClassOf) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))). % 11.76/3.87 tff(c_1951, plain, (![D_24]: (icext(D_24, uri_rdf_XMLLiteral) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))). % 11.76/3.87 tff(c_2050, plain, (![D_24]: (icext(D_24, uri_rdf_Bag) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))). % 11.76/3.87 tff(c_1561, plain, (![D_24]: (icext(D_24, uri_rdfs_Class) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))). % 11.76/3.87 tff(c_2107, plain, (![D_24]: (icext(D_24, uri_rdfs_label) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))). % 11.76/3.87 tff(c_1972, plain, (![D_24]: (icext(D_24, uri_rdfs_subPropertyOf) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))). % 11.76/3.87 tff(c_2533, plain, (~icext(uri_rdfs_Datatype, uri_rdfs_Datatype))). % 11.76/3.87 tff(c_1413, plain, (![D_24]: (icext(D_24, uri_rdf_XMLLiteral) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, D_24)))). % 11.76/3.87 tff(c_1320, plain, (![Q_83]: (iext(Q_83, uri_rdf__2, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))). % 11.76/3.87 tff(c_1404, plain, (![D_24]: (icext(D_24, uri_rdf__3) | ~iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_24)))). % 11.76/3.87 tff(c_1433, plain, (![D_24]: (icext(D_24, uri_rdf_first) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))). % 11.76/3.87 tff(c_1439, plain, (![D_24]: (icext(D_24, uri_rdf_rest) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))). % 11.76/3.87 tff(c_2431, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdfs_domain))). % 11.76/3.87 tff(c_1427, plain, (![D_24]: (icext(D_24, uri_rdf__3) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))). % 11.76/3.87 tff(c_1445, plain, (![D_24]: (icext(D_24, uri_rdf_subject) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))). % 11.76/3.87 tff(c_1436, plain, (![D_24]: (icext(D_24, uri_rdf__2) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))). % 11.76/3.87 tff(c_1448, plain, (![D_24]: (icext(D_24, uri_rdf_type) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))). % 11.76/3.87 tff(c_1309, plain, (![Q_83]: (iext(Q_83, uri_rdfs_isDefinedBy, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))). % 11.76/3.87 tff(c_1416, plain, (![D_24]: (icext(D_24, uri_rdf__2) | ~iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_24)))). % 11.76/3.87 tff(c_2314, plain, (~icext(uri_rdfs_Datatype, uri_rdfs_ContainerMembershipProperty))). % 11.76/3.87 tff(c_1442, plain, (![D_24]: (icext(D_24, uri_rdf__1) | ~iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_24)))). % 11.76/3.87 tff(c_2268, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdfs_range))). % 11.76/3.87 tff(c_1407, plain, (![D_24]: (icext(D_24, uri_rdf_object) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))). % 11.76/3.88 tff(c_1410, plain, (![D_24]: (icext(D_24, uri_rdf_value) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))). % 11.76/3.88 tff(c_2236, plain, (~icext(uri_rdfs_Datatype, uri_rdf_Property))). % 11.76/3.88 tff(c_1316, plain, (![Q_83]: (iext(Q_83, uri_rdf_predicate, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))). % 11.76/3.88 tff(c_1401, plain, (![D_24]: (icext(D_24, uri_rdf__1) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))). % 11.76/3.88 tff(c_2215, plain, (~icext(uri_rdfs_Datatype, uri_rdf_List))). % 11.76/3.88 tff(c_2194, plain, (~icext(uri_rdfs_Datatype, uri_rdfs_Class))). % 11.76/3.88 tff(c_1430, plain, (![D_24]: (icext(D_24, uri_rdf_nil) | ~iext(uri_rdfs_subClassOf, uri_rdf_List, D_24)))). % 11.76/3.88 tff(c_1422, plain, (![D_24]: (icext(D_24, uri_rdf_Property) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))). % 11.76/3.88 tff(c_1093, plain, (![C_76]: (icext(C_76, uri_rdf__2) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_76)))). % 11.76/3.88 tff(c_1131, plain, (![C_76]: (icext(C_76, uri_rdf_rest) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_76)))). % 11.76/3.88 tff(c_1114, plain, (![C_76]: (icext(C_76, uri_rdfs_subClassOf) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_76)))). % 11.76/3.88 tff(c_1142, plain, (![C_76]: (icext(C_76, uri_rdf_first) | ~iext(uri_rdfs_domain, uri_rdf_type, C_76)))). % 11.76/3.88 tff(c_1123, plain, (![C_76]: (icext(C_76, uri_rdfs_range) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_76)))). % 11.76/3.88 tff(c_1091, plain, (![C_76]: (icext(C_76, uri_rdfs_label) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_76)))). % 11.76/3.88 tff(c_917, plain, (![C_72]: (icext(C_72, uri_rdfs_seeAlso) | ~iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_72)))). % 11.76/3.88 tff(c_1126, plain, (![C_76]: (icext(C_76, uri_rdf_first) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_76)))). % 11.76/3.88 tff(c_1130, plain, (![C_76]: (icext(C_76, uri_rdf_rest) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_76)))). % 11.76/3.88 tff(c_1106, plain, (![C_76]: (icext(C_76, uri_rdfs_seeAlso) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_76)))). % 11.76/3.88 tff(c_1125, plain, (![C_76]: (icext(C_76, uri_rdf_value) | ~iext(uri_rdfs_domain, uri_rdf_type, C_76)))). % 11.76/3.88 tff(c_2106, plain, (ip(uri_rdfs_label))). % 11.76/3.88 tff(c_2100, plain, (icext(uri_rdf_Property, uri_rdfs_label))). % 11.76/3.88 tff(c_1119, plain, (![C_76]: (icext(C_76, uri_rdfs_label) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_76)))). % 11.76/3.88 tff(c_1139, plain, (![C_76]: (icext(C_76, uri_rdfs_domain) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_76)))). % 11.76/3.88 tff(c_1121, plain, (![C_76]: (icext(C_76, uri_rdf_first) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_76)))). % 11.76/3.88 tff(c_1118, plain, (![C_76]: (icext(C_76, uri_rdfs_isDefinedBy) | ~iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_76)))). % 11.76/3.88 tff(c_1102, plain, (![C_76]: (icext(C_76, uri_rdfs_subPropertyOf) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_76)))). % 11.76/3.88 tff(c_912, plain, (![C_72]: (icext(C_72, uri_rdfs_Class) | ~iext(uri_rdfs_range, uri_rdf_type, C_72)))). % 11.76/3.88 tff(c_2057, plain, (icext(uri_rdf_Property, uri_rdfs_subClassOf))). % 11.76/3.88 tff(c_1134, plain, (![C_76]: (icext(C_76, uri_rdfs_subClassOf) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_76)))). % 11.76/3.88 tff(c_2044, plain, (icext(uri_rdfs_Class, uri_rdf_Bag))). % 11.76/3.88 tff(c_1136, plain, (![C_76]: (icext(C_76, uri_rdf_Bag) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_76)))). % 11.76/3.88 tff(c_1124, plain, (![C_76]: (icext(C_76, uri_rdfs_comment) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_76)))). % 11.76/3.88 tff(c_1143, plain, (![C_76]: (icext(C_76, uri_rdf__3) | ~iext(uri_rdfs_domain, uri_rdf_type, C_76)))). % 11.76/3.88 tff(c_940, plain, (![C_72]: (icext(C_72, uri_rdf_List) | ~iext(uri_rdfs_range, uri_rdf_type, C_72)))). % 11.76/3.88 tff(c_1132, plain, (![C_76]: (icext(C_76, uri_rdfs_isDefinedBy) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_76)))). % 11.76/3.88 tff(c_921, plain, (![C_72]: (icext(C_72, uri_rdfs_Class) | ~iext(uri_rdfs_range, uri_rdfs_subClassOf, C_72)))). % 11.76/3.88 tff(c_933, plain, (![C_72]: (icext(C_72, uri_rdfs_Class) | ~iext(uri_rdfs_range, uri_rdfs_domain, C_72)))). % 11.76/3.88 tff(c_1140, plain, (![C_76]: (icext(C_76, uri_rdfs_ContainerMembershipProperty) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_76)))). % 11.76/3.88 tff(c_1094, plain, (![C_76]: (icext(C_76, uri_rdf__3) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_76)))). % 11.76/3.88 tff(c_1983, plain, (icext(uri_rdfs_Class, uri_rdfs_Seq))). % 11.76/3.88 tff(c_1127, plain, (![C_76]: (icext(C_76, uri_rdfs_Seq) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_76)))). % 11.76/3.88 tff(c_1141, plain, (![C_76]: (icext(C_76, uri_rdf_nil) | ~iext(uri_rdfs_domain, uri_rdf_type, C_76)))). % 11.76/3.88 tff(c_1964, plain, (icext(uri_rdf_Property, uri_rdfs_subPropertyOf))). % 11.76/3.88 tff(c_1111, plain, (![C_76]: (icext(C_76, uri_rdfs_subPropertyOf) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_76)))). % 11.76/3.88 tff(c_1113, plain, (![C_76]: (icext(C_76, uri_rdf_Property) | ~iext(uri_rdfs_domain, uri_rdf_type, C_76)))). % 11.76/3.88 tff(c_1945, plain, (icext(uri_rdfs_Class, uri_rdf_XMLLiteral))). % 11.76/3.88 tff(c_1089, plain, (![C_76]: (icext(C_76, uri_rdf_XMLLiteral) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_76)))). % 11.76/3.88 tff(c_1101, plain, (![C_76]: (icext(C_76, uri_rdf_value) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_76)))). % 11.76/3.88 tff(c_1097, plain, (![C_76]: (icext(C_76, uri_rdf_rest) | ~iext(uri_rdfs_domain, uri_rdf_type, C_76)))). % 11.76/3.88 tff(c_1107, plain, (![C_76]: (icext(C_76, uri_rdfs_member) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_76)))). % 11.76/3.88 tff(c_1098, plain, (![C_76]: (icext(C_76, uri_rdf__3) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_76)))). % 11.76/3.88 tff(c_1105, plain, (![C_76]: (icext(C_76, uri_rdf__1) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_76)))). % 11.76/3.88 tff(c_1099, plain, (![C_76]: (icext(C_76, uri_rdf_predicate) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_76)))). % 11.76/3.88 tff(c_1896, plain, (icext(uri_rdf_Property, uri_rdfs_domain))). % 11.76/3.88 tff(c_1133, plain, (![C_76]: (icext(C_76, uri_rdfs_domain) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_76)))). % 11.76/3.88 tff(c_1103, plain, (![C_76]: (icext(C_76, uri_rdf__2) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_76)))). % 11.76/3.88 tff(c_1877, plain, (icext(uri_rdfs_Class, uri_rdf_Alt))). % 11.76/3.88 tff(c_1120, plain, (![C_76]: (icext(C_76, uri_rdf_Alt) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_76)))). % 11.76/3.88 tff(c_888, plain, (![C_72]: (icext(C_72, uri_rdfs_Literal) | ~iext(uri_rdfs_range, uri_rdfs_subClassOf, C_72)))). % 11.76/3.88 tff(c_929, plain, (![C_72]: (icext(C_72, uri_rdf_List) | ~iext(uri_rdfs_range, uri_rdfs_range, C_72)))). % 11.76/3.88 tff(c_1090, plain, (![C_76]: (icext(C_76, uri_rdf__1) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_76)))). % 11.76/3.88 tff(c_1853, plain, (ip(uri_rdfs_comment))). % 11.76/3.88 tff(c_1847, plain, (icext(uri_rdf_Property, uri_rdfs_comment))). % 11.76/3.88 tff(c_1129, plain, (![C_76]: (icext(C_76, uri_rdfs_comment) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_76)))). % 11.76/3.88 tff(c_1086, plain, (![C_76]: (icext(C_76, uri_rdf_type) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_76)))). % 11.76/3.88 tff(c_1095, plain, (![C_76]: (icext(C_76, uri_rdf__1) | ~iext(uri_rdfs_domain, uri_rdf_type, C_76)))). % 11.76/3.88 tff(c_886, plain, (![C_72]: (icext(C_72, uri_rdfs_Datatype) | ~iext(uri_rdfs_range, uri_rdf_type, C_72)))). % 11.76/3.88 tff(c_1816, plain, (icext(uri_rdf_Property, uri_rdfs_seeAlso))). % 11.76/3.88 tff(c_1112, plain, (![C_76]: (icext(C_76, uri_rdfs_seeAlso) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_76)))). % 11.76/3.88 tff(c_1128, plain, (![C_76]: (icext(C_76, uri_rdf_value) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_76)))). % 11.76/3.88 tff(c_1104, plain, (![C_76]: (icext(C_76, uri_rdf_subject) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_76)))). % 11.76/3.88 tff(c_901, plain, (![C_72]: (icext(C_72, uri_rdf_Property) | ~iext(uri_rdfs_range, uri_rdfs_range, C_72)))). % 11.76/3.88 tff(c_939, plain, (![C_72]: (icext(C_72, uri_rdf_Property) | ~iext(uri_rdfs_range, uri_rdfs_subClassOf, C_72)))). % 11.76/3.88 tff(c_1779, plain, (icext(uri_rdf_Property, uri_rdfs_range))). % 11.76/3.88 tff(c_1135, plain, (![C_76]: (icext(C_76, uri_rdfs_range) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_76)))). % 11.76/3.88 tff(c_1115, plain, (![C_76]: (icext(C_76, uri_rdf_object) | ~iext(uri_rdfs_domain, uri_rdf_type, C_76)))). % 11.76/3.88 tff(c_1116, plain, (![C_76]: (icext(C_76, uri_rdf_subject) | ~iext(uri_rdfs_domain, uri_rdf_type, C_76)))). % 11.76/3.88 tff(c_1754, plain, (icext(uri_rdfs_Class, uri_rdfs_Container))). % 11.76/3.88 tff(c_935, plain, (![C_72]: (icext(C_72, uri_rdfs_Container) | ~iext(uri_rdfs_range, uri_rdfs_subClassOf, C_72)))). % 11.76/3.88 tff(c_906, plain, (![C_72]: (icext(C_72, uri_rdfs_Resource) | ~iext(uri_rdfs_range, uri_rdfs_range, C_72)))). % 11.76/3.88 tff(c_1729, plain, (icext(uri_rdfs_Class, uri_rdfs_Literal))). % 11.76/3.88 tff(c_1110, plain, (![C_76]: (icext(C_76, uri_rdf_type) | ~iext(uri_rdfs_domain, uri_rdf_type, C_76)))). % 11.76/3.88 tff(c_890, plain, (![C_72]: (icext(C_72, uri_rdfs_Literal) | ~iext(uri_rdfs_range, uri_rdfs_range, C_72)))). % 11.76/3.88 tff(c_1716, plain, (icext(uri_rdf_Property, uri_rdfs_member))). % 11.76/3.88 tff(c_1088, plain, (![C_76]: (icext(C_76, uri_rdfs_member) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_76)))). % 11.76/3.88 tff(c_1711, plain, (ic(uri_rdfs_Statement))). % 11.76/3.88 tff(c_1704, plain, (icext(uri_rdfs_Class, uri_rdfs_Statement))). % 11.76/3.88 tff(c_916, plain, (![C_72]: (icext(C_72, uri_rdfs_Statement) | ~iext(uri_rdfs_range, uri_rdfs_domain, C_72)))). % 11.76/3.88 tff(c_922, plain, (![C_72]: (icext(C_72, uri_rdf_Property) | ~iext(uri_rdfs_range, uri_rdfs_domain, C_72)))). % 11.76/3.88 tff(c_1692, plain, (ip(uri_rdf_predicate))). % 11.76/3.88 tff(c_1686, plain, (icext(uri_rdf_Property, uri_rdf_predicate))). % 11.76/3.88 tff(c_1100, plain, (![C_76]: (icext(C_76, uri_rdf_predicate) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_76)))). % 11.76/3.88 tff(c_1144, plain, (![C_76]: (icext(C_76, uri_rdf_subject) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_76)))). % 11.76/3.88 tff(c_1667, plain, (icext(uri_rdf_Property, uri_rdfs_isDefinedBy))). % 11.76/3.88 tff(c_1092, plain, (![C_76]: (icext(C_76, uri_rdfs_isDefinedBy) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_76)))). % 11.76/3.88 tff(c_1109, plain, (![C_76]: (icext(C_76, uri_rdf_type) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_76)))). % 11.76/3.88 tff(c_1656, plain, (~icext(uri_rdfs_Datatype, uri_rdfs_Resource))). % 11.76/3.88 tff(c_740, plain, (![D_69, X_17]: (icext(D_69, X_17) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Resource, D_69)))). % 11.76/3.88 tff(c_1087, plain, (![C_76]: (icext(C_76, uri_rdf_XMLLiteral) | ~iext(uri_rdfs_domain, uri_rdf_type, C_76)))). % 11.76/3.88 tff(c_1624, plain, (icext(uri_rdfs_Class, uri_rdfs_Datatype))). % 11.76/3.88 tff(c_1122, plain, (![C_76]: (icext(C_76, uri_rdfs_Datatype) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_76)))). % 11.76/3.88 tff(c_1619, plain, (ic(uri_rdf_List))). % 11.76/3.88 tff(c_1612, plain, (icext(uri_rdfs_Class, uri_rdf_List))). % 11.76/3.88 tff(c_930, plain, (![C_72]: (icext(C_72, uri_rdf_List) | ~iext(uri_rdfs_range, uri_rdfs_domain, C_72)))). % 11.76/3.88 tff(c_1117, plain, (![C_76]: (icext(C_76, uri_rdf_object) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_76)))). % 11.76/3.88 tff(c_1593, plain, (icext(uri_rdfs_Class, uri_rdfs_ContainerMembershipProperty))). % 11.76/3.88 tff(c_894, plain, (![C_72]: (icext(C_72, uri_rdfs_ContainerMembershipProperty) | ~iext(uri_rdfs_range, uri_rdf_type, C_72)))). % 11.76/3.88 tff(c_1137, plain, (![C_76]: (icext(C_76, uri_rdf__2) | ~iext(uri_rdfs_domain, uri_rdf_type, C_76)))). % 11.76/3.88 tff(c_1574, plain, (icext(uri_rdfs_Class, uri_rdfs_Resource))). % 11.76/3.88 tff(c_887, plain, (![C_72]: (icext(C_72, uri_rdfs_Resource) | ~iext(uri_rdfs_range, uri_rdfs_domain, C_72)))). % 11.76/3.88 tff(c_936, plain, (![C_72]: (icext(C_72, uri_rdf_Property) | ~iext(uri_rdfs_range, uri_rdf_type, C_72)))). % 11.76/3.88 tff(c_1555, plain, (icext(uri_rdfs_Class, uri_rdfs_Class))). % 11.76/3.88 tff(c_885, plain, (![C_72]: (icext(C_72, uri_rdfs_Class) | ~iext(uri_rdfs_range, uri_rdfs_range, C_72)))). % 11.76/3.89 tff(c_613, plain, (![D_63]: (ic(D_63) | ~icext(uri_rdfs_Datatype, D_63)))). % 11.76/3.89 tff(c_632, plain, (![X_64]: (ip(X_64) | ~icext(uri_rdf_Property, X_64)))). % 11.76/3.89 tff(c_1493, plain, (ip(uri_rdfs_member))). % 11.76/3.89 tff(c_691, plain, (![P_6]: (icext(uri_rdf_Property, P_6) | ~ip(P_6)))). % 11.76/3.89 tff(c_724, plain, (![P_68]: (ip(P_68) | ~icext(uri_rdfs_ContainerMembershipProperty, P_68)))). % 11.76/3.89 tff(c_1464, plain, (ic(uri_rdfs_Resource))). % 11.76/3.89 tff(c_697, plain, (icext(uri_rdf_Property, uri_rdf_type))). % 11.76/3.89 tff(c_700, plain, (icext(uri_rdf_Property, uri_rdf_subject))). % 11.76/3.89 tff(c_693, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__1))). % 11.76/3.89 tff(c_695, plain, (icext(uri_rdf_Property, uri_rdf_rest))). % 11.76/3.89 tff(c_702, plain, (icext(uri_rdf_Property, uri_rdf__2))). % 11.76/3.89 tff(c_705, plain, (icext(uri_rdf_Property, uri_rdf_first))). % 11.76/3.89 tff(c_704, plain, (icext(uri_rdf_List, uri_rdf_nil))). % 11.76/3.89 tff(c_696, plain, (icext(uri_rdf_Property, uri_rdf__3))). % 11.76/3.89 tff(c_698, plain, (icext(uri_rdfs_Class, uri_rdf_Property))). % 11.76/3.89 tff(c_694, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__2))). % 11.76/3.89 tff(c_692, plain, (icext(uri_rdfs_Datatype, uri_rdf_XMLLiteral))). % 11.76/3.89 tff(c_701, plain, (icext(uri_rdf_Property, uri_rdf_value))). % 11.76/3.89 tff(c_699, plain, (icext(uri_rdf_Property, uri_rdf_object))). % 11.76/3.89 tff(c_706, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__3))). % 11.76/3.89 tff(c_703, plain, (icext(uri_rdf_Property, uri_rdf__1))). % 11.76/3.89 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.76/3.89 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.76/3.89 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.76/3.89 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.76/3.89 tff(c_523, plain, (ic(uri_rdfs_Class))). % 11.76/3.89 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.76/3.89 tff(c_521, plain, (ic(uri_rdfs_Literal))). % 11.76/3.89 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.76/3.89 tff(c_70, plain, (![P_10]: (iext(uri_rdfs_subPropertyOf, P_10, uri_rdfs_member) | ~icext(uri_rdfs_ContainerMembershipProperty, P_10)))). % 11.76/3.89 tff(c_633, plain, (~icext(uri_owl_Thing, uri_owl_Class))). % 11.76/3.89 tff(c_233, plain, (ip(uri_rdf_object))). % 11.76/3.89 tff(c_52, plain, (![C_8, X_7]: (icext(C_8, X_7) | ~iext(uri_rdf_type, X_7, C_8)))). % 11.76/3.89 tff(c_556, plain, (ic(uri_rdfs_Seq))). % 11.76/3.89 tff(c_54, plain, (![X_7, C_8]: (iext(uri_rdf_type, X_7, C_8) | ~icext(C_8, X_7)))). % 11.76/3.89 tff(c_555, plain, (ic(uri_rdfs_Datatype))). % 11.76/3.89 tff(c_102, plain, (![D_11]: (iext(uri_rdfs_subClassOf, D_11, uri_rdfs_Literal) | ~icext(uri_rdfs_Datatype, D_11)))). % 11.76/3.89 tff(c_494, plain, (ip(uri_rdfs_isDefinedBy))). % 11.76/3.89 tff(c_28, plain, (![P_6]: (iext(uri_rdf_type, P_6, uri_rdf_Property) | ~ip(P_6)))). % 11.76/3.89 tff(c_472, plain, (ip(uri_rdfs_subClassOf))). % 11.76/3.89 tff(c_454, plain, (ip(uri_rdfs_subPropertyOf))). % 11.76/3.89 tff(c_438, plain, (ip(uri_rdfs_range))). % 11.76/3.89 tff(c_168, plain, (![P_37]: (iext(uri_rdfs_subPropertyOf, P_37, P_37) | ~ip(P_37)))). % 11.76/3.89 tff(c_553, plain, (ic(uri_rdf_XMLLiteral))). % 11.76/3.89 tff(c_554, plain, (ic(uri_rdf_Alt))). % 11.76/3.89 tff(c_154, plain, (![C_27]: (iext(uri_rdfs_subClassOf, C_27, C_27) | ~ic(C_27)))). % 11.76/3.89 tff(c_557, plain, (ic(uri_rdf_Bag))). % 11.76/3.89 tff(c_558, plain, (ic(uri_rdfs_ContainerMembershipProperty))). % 11.76/3.89 tff(c_150, plain, (![C_23, D_24]: (ic(C_23) | ~iext(uri_rdfs_subClassOf, C_23, D_24)))). % 11.76/3.89 tff(c_525, plain, (ic(uri_rdfs_Container))). % 11.76/3.89 tff(c_526, plain, (ic(uri_rdf_Property))). % 11.76/3.89 tff(c_148, plain, (![D_24, C_23]: (ic(D_24) | ~iext(uri_rdfs_subClassOf, C_23, D_24)))). % 11.76/3.89 tff(c_164, plain, (![P_31, Q_32]: (ip(P_31) | ~iext(uri_rdfs_subPropertyOf, P_31, Q_32)))). % 11.76/3.89 tff(c_424, plain, (ip(uri_rdfs_domain))). % 11.76/3.89 tff(c_56, plain, (![C_9]: (iext(uri_rdfs_subClassOf, C_9, uri_rdfs_Resource) | ~ic(C_9)))). % 11.76/3.89 tff(c_479, plain, (ip(uri_rdf_type))). % 11.76/3.89 tff(c_237, plain, (ip(uri_rdf__1))). % 11.76/3.89 tff(c_234, plain, (ip(uri_rdf_subject))). % 11.76/3.89 tff(c_2, plain, (![P_2, S_1, O_3]: (ip(P_2) | ~iext(P_2, S_1, O_3)))). % 11.76/3.89 tff(c_235, plain, (ip(uri_rdf_value))). % 11.76/3.89 tff(c_236, plain, (ip(uri_rdf__2))). % 11.76/3.89 tff(c_238, plain, (ip(uri_rdf_first))). % 11.76/3.89 tff(c_243, plain, (ip(uri_rdfs_seeAlso))). % 11.76/3.89 tff(c_231, plain, (ip(uri_rdf__3))). % 11.76/3.89 tff(c_162, plain, (![Q_32, P_31]: (ip(Q_32) | ~iext(uri_rdfs_subPropertyOf, P_31, Q_32)))). % 11.76/3.89 tff(c_230, plain, (ip(uri_rdf_rest))). % 11.76/3.89 tff(c_26, plain, (![P_6]: (ip(P_6) | ~iext(uri_rdf_type, P_6, uri_rdf_Property)))). % 11.76/3.89 tff(c_114, plain, (![X_16]: (ic(X_16) | ~icext(uri_rdfs_Class, X_16)))). % 11.76/3.89 tff(c_120, plain, (![X_18]: (icext(uri_rdfs_Literal, X_18) | ~lv(X_18)))). % 11.76/3.89 tff(c_122, plain, (![X_18]: (lv(X_18) | ~icext(uri_rdfs_Literal, X_18)))). % 11.76/3.89 tff(c_112, plain, (![X_16]: (icext(uri_rdfs_Class, X_16) | ~ic(X_16)))). % 11.76/3.89 tff(c_174, plain, (iext(uri_rdfs_range, uri_rdf_type, uri_rdfs_Class))). % 11.76/3.89 tff(c_100, plain, (iext(uri_rdf_type, uri_rdf_XMLLiteral, uri_rdfs_Datatype))). % 11.76/3.89 tff(c_74, plain, (iext(uri_rdfs_domain, uri_rdfs_member, uri_rdfs_Resource))). % 11.76/3.89 tff(c_98, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Literal))). % 11.76/3.89 tff(c_84, plain, (iext(uri_rdfs_range, uri_rdf__1, uri_rdfs_Resource))). % 11.76/3.89 tff(c_46, plain, (iext(uri_rdfs_range, uri_rdfs_label, uri_rdfs_Literal))). % 11.76/3.89 tff(c_38, plain, (iext(uri_rdfs_domain, uri_rdfs_isDefinedBy, uri_rdfs_Resource))). % 11.76/3.89 tff(c_86, plain, (iext(uri_rdfs_range, uri_rdf__2, uri_rdfs_Resource))). % 11.76/3.89 tff(c_88, plain, (iext(uri_rdfs_range, uri_rdf__3, uri_rdfs_Resource))). % 11.76/3.89 tff(c_90, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdfs_ContainerMembershipProperty))). % 11.76/3.89 tff(c_92, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdfs_ContainerMembershipProperty))). % 11.76/3.89 tff(c_12, plain, (iext(uri_rdf_type, uri_rdf_rest, uri_rdf_Property))). % 11.76/3.89 tff(c_82, plain, (iext(uri_rdfs_domain, uri_rdf__3, uri_rdfs_Resource))). % 11.76/3.89 tff(c_138, plain, (iext(uri_rdfs_range, uri_rdf_predicate, uri_rdfs_Resource))). % 11.76/3.89 tff(c_136, plain, (iext(uri_rdfs_domain, uri_rdf_predicate, uri_rdfs_Statement))). % 11.76/3.89 tff(c_176, plain, (iext(uri_rdfs_domain, uri_rdf_value, uri_rdfs_Resource))). % 11.76/3.89 tff(c_166, plain, (iext(uri_rdfs_range, uri_rdfs_subPropertyOf, uri_rdf_Property))). % 11.76/3.89 tff(c_80, plain, (iext(uri_rdfs_domain, uri_rdf__2, uri_rdfs_Resource))). % 11.76/3.89 tff(c_142, plain, (iext(uri_rdfs_range, uri_rdf_subject, uri_rdfs_Resource))). % 11.76/3.89 tff(c_78, plain, (iext(uri_rdfs_domain, uri_rdf__1, uri_rdfs_Resource))). % 11.76/3.89 tff(c_48, plain, (iext(uri_rdfs_domain, uri_rdfs_seeAlso, uri_rdfs_Resource))). % 11.76/3.89 tff(c_76, plain, (iext(uri_rdfs_range, uri_rdfs_member, uri_rdfs_Resource))). % 11.76/3.89 tff(c_18, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdf_Property))). % 11.76/3.89 tff(c_172, plain, (iext(uri_rdfs_domain, uri_rdf_type, uri_rdfs_Resource))). % 11.76/3.89 tff(c_32, plain, (iext(uri_rdf_type, uri_rdf_type, uri_rdf_Property))). % 11.76/3.89 tff(c_158, plain, (iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, uri_rdf_Property))). % 11.76/3.89 tff(c_50, plain, (iext(uri_rdfs_range, uri_rdfs_seeAlso, uri_rdfs_Resource))). % 11.76/3.89 tff(c_124, plain, (iext(uri_rdf_type, uri_rdf_Property, uri_rdfs_Class))). % 11.76/3.89 tff(c_152, plain, (iext(uri_rdfs_range, uri_rdfs_subClassOf, uri_rdfs_Class))). % 11.76/3.89 tff(c_20, plain, (iext(uri_rdf_type, uri_rdf_object, uri_rdf_Property))). % 11.76/3.89 tff(c_24, plain, (iext(uri_rdf_type, uri_rdf_subject, uri_rdf_Property))). % 11.76/3.89 tff(c_132, plain, (iext(uri_rdfs_domain, uri_rdf_object, uri_rdfs_Statement))). % 11.76/3.89 tff(c_42, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso))). % 11.76/3.89 tff(c_44, plain, (iext(uri_rdfs_domain, uri_rdfs_label, uri_rdfs_Resource))). % 11.76/3.89 tff(c_66, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Container))). % 11.76/3.89 tff(c_60, plain, (iext(uri_rdfs_range, uri_rdf_first, uri_rdfs_Resource))). % 11.76/3.89 tff(c_104, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Class))). % 11.76/3.89 tff(c_126, plain, (iext(uri_rdfs_domain, uri_rdfs_range, uri_rdf_Property))). % 11.76/3.89 tff(c_36, plain, (iext(uri_rdfs_range, uri_rdfs_comment, uri_rdfs_Literal))). % 11.76/3.89 tff(c_22, plain, (iext(uri_rdf_type, uri_rdf_value, uri_rdf_Property))). % 11.76/3.89 tff(c_58, plain, (iext(uri_rdfs_domain, uri_rdf_first, uri_rdf_List))). % 11.76/3.89 tff(c_96, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Container))). % 11.76/3.89 tff(c_178, plain, (iext(uri_rdfs_range, uri_rdf_value, uri_rdfs_Resource))). % 11.76/3.89 tff(c_189, plain, (~iext(uri_rdf_type, uri_owl_Class, uri_owl_Thing))). % 11.76/3.89 tff(c_34, plain, (iext(uri_rdfs_domain, uri_rdfs_comment, uri_rdfs_Resource))). % 11.76/3.89 tff(c_64, plain, (iext(uri_rdfs_range, uri_rdf_rest, uri_rdf_List))). % 11.76/3.89 tff(c_62, plain, (iext(uri_rdfs_domain, uri_rdf_rest, uri_rdf_List))). % 11.76/3.89 tff(c_40, plain, (iext(uri_rdfs_range, uri_rdfs_isDefinedBy, uri_rdfs_Resource))). % 11.76/3.89 tff(c_110, plain, (iext(uri_rdfs_range, uri_rdfs_domain, uri_rdfs_Class))). % 11.76/3.89 tff(c_144, plain, (iext(uri_rdfs_domain, uri_rdfs_subClassOf, uri_rdfs_Class))). % 11.76/3.89 tff(c_130, plain, (iext(uri_rdfs_range, uri_rdfs_range, uri_rdfs_Class))). % 11.76/3.89 tff(c_68, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Container))). % 11.76/3.89 tff(c_16, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdf_Property))). % 11.76/3.89 tff(c_14, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdf_Property))). % 11.76/3.89 tff(c_106, plain, (iext(uri_rdfs_domain, uri_rdfs_domain, uri_rdf_Property))). % 11.76/3.89 tff(c_72, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property))). % 11.76/3.89 tff(c_10, plain, (iext(uri_rdf_type, uri_rdf_nil, uri_rdf_List))). % 11.76/3.89 tff(c_8, plain, (iext(uri_rdf_type, uri_rdf_first, uri_rdf_Property))). % 11.76/3.89 tff(c_94, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdfs_ContainerMembershipProperty))). % 11.76/3.89 tff(c_140, plain, (iext(uri_rdfs_domain, uri_rdf_subject, uri_rdfs_Statement))). % 11.76/3.89 tff(c_185, plain, (![X_17]: (icext(uri_rdfs_Resource, X_17)))). % 11.76/3.89 tff(c_4, plain, (![X_4]: (ir(X_4)))). % 11.76/3.89 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 11.76/3.89 %------------------------------------------------------------------------------