%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SWB007-10 : TPTP v9.0.0. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n015.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:46 PM UTC 2025 % Result : Satisfiable 31.40s 21.20s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SWB007-10 : TPTP v9.0.0. Released v7.5.0. % 0.07/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.13/0.34 % Computer : n015.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Wed Apr 9 00:53:50 EDT 2025 % 0.13/0.34 % CPUTime : % 31.40/21.19 % 31.40/21.20 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 31.40/21.20 % 31.40/21.20 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 31.40/21.21 %$ ifeq > tuple > iext > icext > #nlpp > lv > ir > ip > ic > 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_ex_w > uri_ex_p > uri_ex_c2 > uri_ex_c1 > uri_ex_c > true % 31.40/21.21 % 31.40/21.21 %Foreground sorts: % 31.40/21.21 % 31.40/21.21 % 31.40/21.21 %Background operators: % 31.40/21.21 % 31.40/21.21 % 31.40/21.21 %Foreground operators: % 31.40/21.21 tff(uri_rdfs_Datatype, type, uri_rdfs_Datatype: $i). % 31.40/21.21 tff(uri_rdfs_ContainerMembershipProperty, type, uri_rdfs_ContainerMembershipProperty: $i). % 31.40/21.21 tff(uri_rdfs_Resource, type, uri_rdfs_Resource: $i). % 31.40/21.21 tff(uri_rdf_Property, type, uri_rdf_Property: $i). % 31.40/21.21 tff(uri_rdf_subject, type, uri_rdf_subject: $i). % 31.40/21.21 tff(tuple, type, tuple: ($i * $i * $i) > $i). % 31.40/21.21 tff(uri_rdf_type, type, uri_rdf_type: $i). % 31.40/21.21 tff(uri_rdfs_subPropertyOf, type, uri_rdfs_subPropertyOf: $i). % 31.40/21.21 tff(uri_rdfs_seeAlso, type, uri_rdfs_seeAlso: $i). % 31.40/21.21 tff(icext, type, icext: ($i * $i) > $i). % 31.40/21.21 tff(uri_rdfs_range, type, uri_rdfs_range: $i). % 31.40/21.21 tff(uri_rdf_XMLLiteral, type, uri_rdf_XMLLiteral: $i). % 31.40/21.21 tff(uri_rdf_List, type, uri_rdf_List: $i). % 31.40/21.21 tff(uri_rdf_first, type, uri_rdf_first: $i). % 31.40/21.21 tff(uri_rdf_predicate, type, uri_rdf_predicate: $i). % 31.40/21.21 tff(uri_ex_c2, type, uri_ex_c2: $i). % 31.40/21.21 tff(ir, type, ir: $i > $i). % 31.40/21.21 tff(lv, type, lv: $i > $i). % 31.40/21.21 tff(uri_ex_c, type, uri_ex_c: $i). % 31.40/21.21 tff(uri_rdf__3, type, uri_rdf__3: $i). % 31.40/21.21 tff(uri_rdf_value, type, uri_rdf_value: $i). % 31.40/21.21 tff(ic, type, ic: $i > $i). % 31.40/21.21 tff(uri_rdfs_Statement, type, uri_rdfs_Statement: $i). % 31.40/21.21 tff(uri_ex_p, type, uri_ex_p: $i). % 31.40/21.21 tff(uri_rdf__1, type, uri_rdf__1: $i). % 31.40/21.21 tff(iext, type, iext: ($i * $i * $i) > $i). % 31.40/21.21 tff(uri_ex_w, type, uri_ex_w: $i). % 31.40/21.21 tff(uri_rdf_rest, type, uri_rdf_rest: $i). % 31.40/21.21 tff(uri_rdfs_label, type, uri_rdfs_label: $i). % 31.40/21.21 tff(uri_rdfs_Container, type, uri_rdfs_Container: $i). % 31.40/21.21 tff(uri_rdfs_subClassOf, type, uri_rdfs_subClassOf: $i). % 31.40/21.21 tff(uri_owl_sameAs, type, uri_owl_sameAs: $i). % 31.40/21.21 tff(uri_rdf_object, type, uri_rdf_object: $i). % 31.40/21.21 tff(ip, type, ip: $i > $i). % 31.40/21.21 tff(uri_rdfs_Class, type, uri_rdfs_Class: $i). % 31.40/21.21 tff(uri_rdfs_Seq, type, uri_rdfs_Seq: $i). % 31.40/21.21 tff(uri_ex_c1, type, uri_ex_c1: $i). % 31.40/21.21 tff(uri_rdfs_member, type, uri_rdfs_member: $i). % 31.40/21.21 tff(uri_rdf_Bag, type, uri_rdf_Bag: $i). % 31.40/21.21 tff(uri_rdf__2, type, uri_rdf__2: $i). % 31.40/21.21 tff(uri_rdfs_comment, type, uri_rdfs_comment: $i). % 31.40/21.21 tff(uri_rdfs_Literal, type, uri_rdfs_Literal: $i). % 31.40/21.21 tff(true, type, true: $i). % 31.40/21.21 tff(uri_rdf_Alt, type, uri_rdf_Alt: $i). % 31.40/21.21 tff(uri_rdf_nil, type, uri_rdf_nil: $i). % 31.40/21.21 tff(uri_rdfs_isDefinedBy, type, uri_rdfs_isDefinedBy: $i). % 31.40/21.21 tff(uri_rdfs_domain, type, uri_rdfs_domain: $i). % 31.40/21.21 tff(ifeq, type, ifeq: ($i * $i * $i * $i) > $i). % 31.40/21.21 % 31.40/21.21 %Saturated clause set: % 31.40/21.22 tff(c_12973, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_rdfs_member), true, true, true), true)=true))). % 31.40/21.22 tff(c_12976, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_rdfs_member, Y_21), true, true, true), true)=true))). % 31.40/21.22 tff(c_13299, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdfs_Resource, uri_rdfs_Class), true, true, true), true)=true))). % 31.40/21.22 tff(c_71134, plain, (![X_1231, Y_1232]: (ifeq(iext(uri_rdf_predicate, X_1231, Y_1232), true, iext(uri_rdf_predicate, X_1231, Y_1232), true)=true))). % 31.40/21.22 tff(c_70987, plain, (![X_1226, Y_1227]: (ifeq(iext(uri_rdfs_label, X_1226, Y_1227), true, iext(uri_rdfs_label, X_1226, Y_1227), true)=true))). % 31.40/21.22 tff(c_14489, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_rdf_predicate, uri_rdf_predicate), true, true, true), true)=true))). % 31.40/21.22 tff(c_70959, plain, (![X_1222, Y_1223]: (ifeq(iext(uri_ex_p, X_1222, Y_1223), true, iext(uri_ex_p, X_1222, Y_1223), true)=true))). % 31.40/21.22 tff(c_15565, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_ex_p, uri_ex_p), true, true, true), true)=true))). % 31.40/21.22 tff(c_13156, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_rdfs_label, uri_rdfs_label), true, true, true), true)=true))). % 31.40/21.22 tff(c_70572, plain, (![X_1215, Y_1216]: (ifeq(iext(uri_rdfs_comment, X_1215, Y_1216), true, iext(uri_rdfs_comment, X_1215, Y_1216), true)=true))). % 31.40/21.22 tff(c_13246, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_rdfs_comment, uri_rdfs_comment), true, true, true), true)=true))). % 31.40/21.22 tff(c_12847, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_rdfs_Resource, uri_rdfs_Resource), true, true, true), true)=true))). % 31.40/21.22 tff(c_70417, plain, (![X_1210, Y_1211]: (ifeq(iext(uri_rdfs_member, X_1210, Y_1211), true, iext(uri_rdfs_member, X_1210, Y_1211), true)=true))). % 31.40/21.22 tff(c_12790, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_rdfs_member, uri_rdfs_member), true, true, true), true)=true))). % 31.40/21.22 tff(c_5148, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, uri_rdfs_Resource), true, true, true), true)=true))). % 31.40/21.22 tff(c_12919, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdfs_member, uri_rdf_Property), true, true, true), true)=true))). % 31.40/21.22 tff(c_5151, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, uri_rdfs_Resource, Y_21), true, true, true), true)=true))). % 31.40/21.22 tff(c_12430, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_rdf_List, uri_rdfs_Resource), true, true, true), true)=true))). % 31.40/21.22 tff(c_12571, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_rdfs_Statement, uri_rdfs_Statement), true, true, true), true)=true))). % 31.40/21.22 tff(c_69375, plain, (![C_1200]: (ifeq(iext(uri_rdfs_subClassOf, C_1200, uri_rdf_List), true, iext(uri_rdfs_subClassOf, C_1200, uri_rdfs_Resource), true)=true))). % 31.40/21.22 tff(c_12363, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_rdf_List, uri_rdf_List), true, true, true), true)=true))). % 31.40/21.22 tff(c_69100, plain, (![C_1197]: (ifeq(iext(uri_rdfs_subClassOf, C_1197, uri_rdfs_Statement), true, iext(uri_rdfs_subClassOf, C_1197, uri_rdfs_Resource), true)=true))). % 31.40/21.22 tff(c_12637, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_rdfs_Statement, uri_rdfs_Resource), true, true, true), true)=true))). % 31.40/21.22 tff(c_11748, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdf_Alt, uri_rdfs_Class), true, true, true), true)=true))). % 31.40/21.22 tff(c_8777, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_owl_sameAs, Y_21), true, true, true), true)=true))). % 31.40/21.22 tff(c_8774, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_owl_sameAs), true, true, true), true)=true))). % 31.40/21.22 tff(c_12285, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdf_Bag, uri_rdfs_Class), true, true, true), true)=true))). % 31.40/21.22 tff(c_12017, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_ex_c1, uri_rdfs_Class), true, true, true), true)=true))). % 31.40/21.22 tff(c_6522, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_rdfs_range, Y_21), true, true, true), true)=true))). % 31.40/21.22 tff(c_9933, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_rdfs_seeAlso), true, true, true), true)=true))). % 31.40/21.22 tff(c_12188, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_ex_c, uri_rdfs_Class), true, true, true), true)=true))). % 31.40/21.22 tff(c_12139, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdf_XMLLiteral, uri_rdfs_Class), true, true, true), true)=true))). % 31.40/21.22 tff(c_11795, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Class), true, true, true), true)=true))). % 31.40/21.22 tff(c_11968, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdfs_Container, uri_rdfs_Class), true, true, true), true)=true))). % 31.40/21.22 tff(c_11921, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdfs_Seq, uri_rdfs_Class), true, true, true), true)=true))). % 31.40/21.22 tff(c_7286, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_rdfs_subPropertyOf), true, true, true), true)=true))). % 31.40/21.22 tff(c_12237, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdfs_Datatype, uri_rdfs_Class), true, true, true), true)=true))). % 31.40/21.22 tff(c_12066, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdfs_Class, uri_rdfs_Class), true, true, true), true)=true))). % 31.40/21.22 tff(c_9936, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_rdfs_seeAlso, Y_21), true, true, true), true)=true))). % 31.40/21.22 tff(c_11873, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdfs_Literal, uri_rdfs_Class), true, true, true), true)=true))). % 31.40/21.22 tff(c_6519, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_rdfs_range), true, true, true), true)=true))). % 31.40/21.22 tff(c_7289, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_rdfs_subPropertyOf, Y_21), true, true, true), true)=true))). % 31.40/21.22 tff(c_11473, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdfs_label, uri_rdf_Property), true, true, true), true)=true))). % 31.40/21.22 tff(c_15430, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_ex_p, uri_rdf_Property), true, true, true), true)=true))). % 31.40/21.22 tff(c_11619, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdfs_comment, uri_rdf_Property), true, true, true), true)=true))). % 31.40/21.22 tff(c_11426, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdfs_Statement, uri_rdfs_Class), true, true, true), true)=true))). % 31.40/21.22 tff(c_14251, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdf_predicate, uri_rdf_Property), true, true, true), true)=true))). % 31.40/21.22 tff(c_11568, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdf_List, uri_rdfs_Class), true, true, true), true)=true))). % 31.40/21.22 tff(c_7232, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdfs_subPropertyOf, uri_rdf_Property), true, true, true), true)=true))). % 31.53/21.22 tff(c_65714, plain, (![X_1158, Y_1159]: (ifeq(iext(uri_rdf_rest, X_1158, Y_1159), true, iext(uri_rdf_rest, X_1158, Y_1159), true)=true))). % 31.53/21.22 tff(c_4567, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, uri_rdfs_Datatype, Y_21), true, true, true), true)=true))). % 31.53/21.22 tff(c_8949, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Resource), true, true, true), true)=true))). % 31.53/21.22 tff(c_4258, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, uri_rdfs_Class, Y_21), true, true, true), true)=true))). % 31.53/21.23 tff(c_65292, plain, (![X_1149, Y_1150]: (ifeq(iext(uri_rdf__3, X_1149, Y_1150), true, iext(uri_rdfs_member, X_1149, Y_1150), true)=true))). % 31.53/21.23 tff(c_6439, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdfs_range, uri_rdf_Property), true, true, true), true)=true))). % 31.53/21.23 tff(c_9879, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdfs_seeAlso, uri_rdf_Property), true, true, true), true)=true))). % 31.53/21.23 tff(c_65018, plain, (![X_1143, Y_1144]: (ifeq(iext(uri_rdf_first, X_1143, Y_1144), true, iext(uri_rdf_first, X_1143, Y_1144), true)=true))). % 31.53/21.23 tff(c_64990, plain, (![X_1139, Y_1140]: (ifeq(iext(uri_rdf_value, X_1139, Y_1140), true, iext(uri_rdf_value, X_1139, Y_1140), true)=true))). % 31.53/21.23 tff(c_64827, plain, (![C_1137]: (ifeq(iext(uri_rdfs_subClassOf, C_1137, uri_rdfs_Class), true, iext(uri_rdfs_subClassOf, C_1137, uri_rdfs_Resource), true)=true))). % 31.53/21.23 tff(c_64495, plain, (![X_1133, Y_1134]: (ifeq(iext(uri_rdfs_range, X_1133, Y_1134), true, iext(uri_rdfs_range, X_1133, Y_1134), true)=true))). % 31.53/21.23 tff(c_4418, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, uri_rdfs_Literal), true, true, true), true)=true))). % 31.53/21.23 tff(c_9083, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_rdf_Alt, uri_rdfs_Resource), true, true, true), true)=true))). % 31.53/21.23 tff(c_4421, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, uri_rdfs_Literal, Y_21), true, true, true), true)=true))). % 31.53/21.23 tff(c_7449, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_rdf_type, uri_rdf_type), true, true, true), true)=true))). % 31.53/21.23 tff(c_4617, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, uri_rdfs_Container), true, true, true), true)=true))). % 31.53/21.23 tff(c_8280, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdfs_isDefinedBy, uri_rdf_Property), true, true, true), true)=true))). % 31.53/21.23 tff(c_4168, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, uri_rdf_XMLLiteral, Y_21), true, true, true), true)=true))). % 31.53/21.23 tff(c_4208, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, uri_rdf_Bag), true, true, true), true)=true))). % 31.53/21.23 tff(c_10794, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_ex_c, uri_ex_c), true, true, true), true)=true))). % 31.53/21.23 tff(c_7726, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_rdf_XMLLiteral, uri_rdf_XMLLiteral), true, true, true), true)=true))). % 31.53/21.23 tff(c_5303, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_rdf_Alt, uri_rdf_Alt), true, true, true), true)=true))). % 31.53/21.23 tff(c_62916, plain, (![C_1115]: (ifeq(iext(uri_rdfs_subClassOf, C_1115, uri_rdfs_Seq), true, iext(uri_rdfs_subClassOf, C_1115, uri_rdfs_Resource), true)=true))). % 31.53/21.23 tff(c_10611, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_rdfs_range, uri_rdfs_range), true, true, true), true)=true))). % 31.53/21.23 tff(c_62641, plain, (![C_1112]: (ifeq(iext(uri_rdfs_subClassOf, C_1112, uri_rdfs_Datatype), true, iext(uri_rdfs_subClassOf, C_1112, uri_rdfs_Resource), true)=true))). % 31.53/21.23 tff(c_8882, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_rdf_Property, uri_rdf_Property), true, true, true), true)=true))). % 31.53/21.23 tff(c_8695, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_owl_sameAs, uri_rdf_Property), true, true, true), true)=true))). % 31.53/21.23 tff(c_8517, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_rdf_XMLLiteral, uri_rdfs_Resource), true, true, true), true)=true))). % 31.53/21.23 tff(c_61499, plain, (![X_1104, Y_1105]: (ifeq(iext(uri_rdfs_subClassOf, X_1104, Y_1105), true, iext(uri_rdfs_subClassOf, X_1104, Y_1105), true)=true))). % 31.53/21.23 tff(c_61422, plain, (![C_1103]: (ifeq(iext(uri_rdfs_subClassOf, C_1103, uri_ex_c), true, iext(uri_rdfs_subClassOf, C_1103, uri_rdfs_Resource), true)=true))). % 31.53/21.23 tff(c_6281, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_rdfs_Container, uri_rdfs_Container), true, true, true), true)=true))). % 31.53/21.23 tff(c_10664, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_rdfs_Seq, uri_rdfs_Resource), true, true, true), true)=true))). % 31.53/21.23 tff(c_5226, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_ex_c, uri_rdfs_Resource), true, true, true), true)=true))). % 31.53/21.23 tff(c_4517, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, uri_ex_c1), true, true, true), true)=true))). % 31.53/21.23 tff(c_5384, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf), true, true, true), true)=true))). % 31.53/21.23 tff(c_4211, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, uri_rdf_Bag, Y_21), true, true, true), true)=true))). % 31.53/21.23 tff(c_4620, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, uri_rdfs_Container, Y_21), true, true, true), true)=true))). % 31.53/21.23 tff(c_8133, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_rdf_value, uri_rdf_value), true, true, true), true)=true))). % 31.53/21.23 tff(c_5560, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_rdfs_seeAlso, uri_rdfs_seeAlso), true, true, true), true)=true))). % 31.53/21.23 tff(c_10378, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_rdfs_Container, uri_rdfs_Resource), true, true, true), true)=true))). % 31.53/21.23 tff(c_6727, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_rdf_Property, uri_rdfs_Resource), true, true, true), true)=true))). % 31.53/21.23 tff(c_58985, plain, (![X_1081, Y_1082]: (ifeq(iext(uri_rdfs_subPropertyOf, X_1081, Y_1082), true, iext(uri_rdfs_subPropertyOf, X_1081, Y_1082), true)=true))). % 31.53/21.23 tff(c_9677, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_rdf_first, uri_rdf_first), true, true, true), true)=true))). % 31.53/21.23 tff(c_58838, plain, (![X_1076, Y_1077]: (ifeq(iext(uri_rdfs_seeAlso, X_1076, Y_1077), true, iext(uri_rdfs_seeAlso, X_1076, Y_1077), true)=true))). % 31.53/21.23 tff(c_9300, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_rdf__3, uri_rdfs_member), true, true, true), true)=true))). % 31.53/21.23 tff(c_58464, plain, (![X_1069, Y_1070]: (ifeq(iext(uri_rdfs_isDefinedBy, X_1069, Y_1070), true, iext(uri_rdfs_isDefinedBy, X_1069, Y_1070), true)=true))). % 31.53/21.23 tff(c_6902, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_rdfs_Literal, uri_rdfs_Literal), true, true, true), true)=true))). % 31.53/21.23 tff(c_8438, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_rdf__3, uri_rdf__3), true, true, true), true)=true))). % 31.53/21.23 tff(c_8372, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_rdfs_domain, uri_rdfs_domain), true, true, true), true)=true))). % 31.53/21.23 tff(c_4307, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 31.53/21.23 tff(c_5804, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_rdf_Bag, uri_rdfs_Resource), true, true, true), true)=true))). % 31.53/21.23 tff(c_7986, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_rdf__1, uri_rdfs_member), true, true, true), true)=true))). % 31.53/21.23 tff(c_4913, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_rdfs_ContainerMembershipProperty, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 31.53/21.23 tff(c_57432, plain, (![C_1059]: (ifeq(iext(uri_rdfs_subClassOf, C_1059, uri_rdfs_Literal), true, iext(uri_rdfs_subClassOf, C_1059, uri_rdfs_Resource), true)=true))). % 31.53/21.23 tff(c_4564, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, uri_rdfs_Datatype), true, true, true), true)=true))). % 31.53/21.23 tff(c_4477, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, uri_rdfs_Seq, Y_21), true, true, true), true)=true))). % 31.53/21.23 tff(c_4310, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, uri_rdfs_ContainerMembershipProperty, Y_21), true, true, true), true)=true))). % 31.53/21.23 tff(c_7652, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_rdfs_isDefinedBy, uri_rdfs_isDefinedBy), true, true, true), true)=true))). % 31.53/21.23 tff(c_5679, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_rdf_rest, uri_rdf_rest), true, true, true), true)=true))). % 31.53/21.23 tff(c_11368, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_rdf_subject, uri_rdf_subject), true, true, true), true)=true))). % 31.53/21.23 tff(c_56499, plain, (![C_1048]: (ifeq(iext(uri_rdfs_subClassOf, C_1048, uri_ex_c1), true, iext(uri_rdfs_subClassOf, C_1048, uri_rdfs_Resource), true)=true))). % 31.53/21.23 tff(c_56344, plain, (![C_1046]: (ifeq(iext(uri_rdfs_subClassOf, C_1046, uri_rdf_Alt), true, iext(uri_rdfs_subClassOf, C_1046, uri_rdfs_Resource), true)=true))). % 31.53/21.23 tff(c_4474, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, uri_rdfs_Seq), true, true, true), true)=true))). % 31.53/21.23 tff(c_56185, plain, (![X_1040, Y_1041]: (ifeq(iext(uri_rdf_subject, X_1040, Y_1041), true, iext(uri_rdf_subject, X_1040, Y_1041), true)=true))). % 31.53/21.23 tff(c_56158, plain, (![X_1036, Y_1037]: (ifeq(iext(uri_rdf__2, X_1036, Y_1037), true, iext(uri_rdfs_member, X_1036, Y_1037), true)=true))). % 31.53/21.23 tff(c_56091, plain, (![P_1034]: (ifeq(iext(uri_rdfs_subPropertyOf, P_1034, uri_rdf__3), true, iext(uri_rdfs_subPropertyOf, P_1034, uri_rdfs_member), true)=true))). % 31.53/21.23 tff(c_10323, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdfs_subClassOf, uri_rdf_Property), true, true, true), true)=true))). % 31.53/21.23 tff(c_55904, plain, (![P_1031]: (ifeq(iext(uri_rdfs_subPropertyOf, P_1031, uri_rdf__1), true, iext(uri_rdfs_subPropertyOf, P_1031, uri_rdfs_member), true)=true))). % 31.53/21.23 tff(c_4359, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, uri_ex_c, Y_21), true, true, true), true)=true))). % 31.53/21.24 tff(c_11224, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_rdfs_Class, uri_rdfs_Class), true, true, true), true)=true))). % 31.53/21.24 tff(c_55075, plain, (![P_1023]: (ifeq(iext(uri_rdfs_subPropertyOf, P_1023, uri_rdf__2), true, iext(uri_rdfs_subPropertyOf, P_1023, uri_rdfs_member), true)=true))). % 31.53/21.24 tff(c_54138, plain, (![X_1012, Y_1013]: (ifeq(iext(uri_owl_sameAs, X_1012, Y_1013), true, iext(uri_owl_sameAs, X_1012, Y_1013), true)=true))). % 31.53/21.24 tff(c_54111, plain, (![X_1008, Y_1009]: (ifeq(iext(uri_rdf__3, X_1008, Y_1009), true, iext(uri_rdf__3, X_1008, Y_1009), true)=true))). % 31.53/21.24 tff(c_54084, plain, (![X_1004, Y_1005]: (ifeq(iext(uri_rdf_object, X_1004, Y_1005), true, iext(uri_rdf_object, X_1004, Y_1005), true)=true))). % 31.53/21.24 tff(c_10243, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_rdf_object, uri_rdf_object), true, true, true), true)=true))). % 31.53/21.24 tff(c_9233, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_rdf__2, uri_rdf__2), true, true, true), true)=true))). % 31.53/21.24 tff(c_10862, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_ex_c1, uri_rdfs_Resource), true, true, true), true)=true))). % 31.53/21.24 tff(c_53014, plain, (![C_995]: (ifeq(iext(uri_rdfs_subClassOf, C_995, uri_rdf_Property), true, iext(uri_rdfs_subClassOf, C_995, uri_rdfs_Resource), true)=true))). % 31.53/21.24 tff(c_52859, plain, (![C_993]: (ifeq(iext(uri_rdfs_subClassOf, C_993, uri_rdfs_ContainerMembershipProperty), true, iext(uri_rdfs_subClassOf, C_993, uri_rdfs_Resource), true)=true))). % 31.53/21.24 tff(c_52832, plain, (![X_989, Y_990]: (ifeq(iext(uri_rdf__1, X_989, Y_990), true, iext(uri_rdfs_member, X_989, Y_990), true)=true))). % 31.53/21.24 tff(c_52681, plain, (![X_984, Y_985]: (ifeq(iext(uri_rdf__1, X_984, Y_985), true, iext(uri_rdf__1, X_984, Y_985), true)=true))). % 31.53/21.24 tff(c_10099, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdfs_domain, uri_rdf_Property), true, true, true), true)=true))). % 31.53/21.24 tff(c_4115, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, uri_rdf_Alt), true, true, true), true)=true))). % 31.53/21.24 tff(c_9541, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_rdf__2, uri_rdfs_member), true, true, true), true)=true))). % 31.53/21.24 tff(c_8629, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_ex_c1, uri_ex_c1), true, true, true), true)=true))). % 31.53/21.24 tff(c_9612, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_rdfs_subClassOf, uri_rdfs_subClassOf), true, true, true), true)=true))). % 31.53/21.24 tff(c_4356, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, uri_ex_c), true, true, true), true)=true))). % 31.53/21.24 tff(c_10533, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_rdfs_Datatype, uri_rdfs_Datatype), true, true, true), true)=true))). % 31.53/21.24 tff(c_51183, plain, (![C_970]: (ifeq(iext(uri_rdfs_subClassOf, C_970, uri_rdf_Bag), true, iext(uri_rdfs_subClassOf, C_970, uri_rdfs_Resource), true)=true))). % 31.53/21.24 tff(c_7528, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_rdfs_Datatype, uri_rdfs_Resource), true, true, true), true)=true))). % 31.53/21.24 tff(c_4255, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, uri_rdfs_Class), true, true, true), true)=true))). % 31.53/21.24 tff(c_50127, plain, (![X_963, Y_964]: (ifeq(iext(uri_rdf_type, X_963, Y_964), true, iext(uri_rdf_type, X_963, Y_964), true)=true))). % 31.53/21.24 tff(c_49455, plain, (![C_958]: (ifeq(iext(uri_rdfs_subClassOf, C_958, uri_rdfs_Container), true, iext(uri_rdfs_subClassOf, C_958, uri_rdfs_Resource), true)=true))). % 31.53/21.24 tff(c_4520, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, uri_ex_c1, Y_21), true, true, true), true)=true))). % 31.53/21.24 tff(c_4118, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, uri_rdf_Alt, Y_21), true, true, true), true)=true))). % 31.53/21.24 tff(c_48218, plain, (![X_945, Y_946]: (ifeq(iext(uri_rdfs_domain, X_945, Y_946), true, iext(uri_rdfs_domain, X_945, Y_946), true)=true))). % 31.53/21.24 tff(c_4165, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, uri_rdf_XMLLiteral), true, true, true), true)=true))). % 31.53/21.24 tff(c_7910, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_owl_sameAs, uri_owl_sameAs), true, true, true), true)=true))). % 31.53/21.24 tff(c_11290, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_rdf_Bag, uri_rdf_Bag), true, true, true), true)=true))). % 31.53/21.24 tff(c_9730, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_rdfs_Literal, uri_rdfs_Resource), true, true, true), true)=true))). % 31.53/21.24 tff(c_47166, plain, (![X_932, Y_933]: (ifeq(iext(uri_rdf__2, X_932, Y_933), true, iext(uri_rdf__2, X_932, Y_933), true)=true))). % 31.53/21.24 tff(c_7109, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_rdfs_Seq, uri_rdfs_Seq), true, true, true), true)=true))). % 31.53/21.24 tff(c_46891, plain, (![C_929]: (ifeq(iext(uri_rdfs_subClassOf, C_929, uri_rdf_XMLLiteral), true, iext(uri_rdfs_subClassOf, C_929, uri_rdfs_Resource), true)=true))). % 31.53/21.24 tff(c_8227, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_rdf__1, uri_rdf__1), true, true, true), true)=true))). % 31.53/21.24 tff(c_5000, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_rdfs_Class, uri_rdfs_Resource), true, true, true), true)=true))). % 31.53/21.24 tff(c_10954, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, uri_rdfs_Statement, Y_21), true, true, true), true)=true))). % 31.53/21.24 tff(c_6794, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_rdfs_domain), true, true, true), true)=true))). % 31.53/21.24 tff(c_5970, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, uri_rdf_List), true, true, true), true)=true))). % 31.53/21.24 tff(c_6121, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_rdfs_isDefinedBy), true, true, true), true)=true))). % 31.53/21.24 tff(c_7798, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_rdfs_comment, Y_21), true, true, true), true)=true))). % 31.53/21.24 tff(c_6124, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_rdfs_isDefinedBy, Y_21), true, true, true), true)=true))). % 31.53/21.24 tff(c_15257, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_ex_p), true, true, true), true)=true))). % 31.53/21.24 tff(c_9376, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_rdfs_label), true, true, true), true)=true))). % 31.53/21.24 tff(c_6228, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_rdfs_subClassOf, Y_21), true, true, true), true)=true))). % 31.53/21.24 tff(c_14204, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_rdf_predicate), true, true, true), true)=true))). % 31.53/21.24 tff(c_10951, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, uri_rdfs_Statement), true, true, true), true)=true))). % 31.53/21.24 tff(c_6225, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_rdfs_subClassOf), true, true, true), true)=true))). % 31.53/21.24 tff(c_9379, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_rdfs_label, Y_21), true, true, true), true)=true))). % 31.53/21.24 tff(c_5973, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, uri_rdf_List, Y_21), true, true, true), true)=true))). % 31.53/21.24 tff(c_6797, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_rdfs_domain, Y_21), true, true, true), true)=true))). % 31.53/21.24 tff(c_4802, plain, (![P_47, X_139]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, X_139, uri_rdfs_Resource), true, true, true), true)=true))). % 31.53/21.24 tff(c_7795, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_rdfs_comment), true, true, true), true)=true))). % 31.53/21.24 tff(c_14207, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_rdf_predicate, Y_21), true, true, true), true)=true))). % 31.53/21.24 tff(c_15260, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_ex_p, Y_21), true, true, true), true)=true))). % 31.53/21.24 tff(c_3623, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_rdf_type, Y_21), true, true, true), true)=true))). % 31.53/21.24 tff(c_3586, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_rdf_first, Y_21), true, true, true), true)=true))). % 31.53/21.24 tff(c_3789, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_rdf_object), true, true, true), true)=true))). % 31.53/21.24 tff(c_3657, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_rdf_rest), true, true, true), true)=true))). % 31.53/21.24 tff(c_3994, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_ContainerMembershipProperty), true, ifeq(iext(P_18, uri_rdf__3, Y_21), true, true, true), true)=true))). % 31.53/21.24 tff(c_3538, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_List), true, ifeq(iext(P_28, X_30, uri_rdf_nil), true, true, true), true)=true))). % 31.53/21.24 tff(c_3660, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_rdf_rest, Y_21), true, true, true), true)=true))). % 31.53/21.24 tff(c_3873, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_rdf__3), true, true, true), true)=true))). % 31.53/21.24 tff(c_3583, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_rdf_first), true, true, true), true)=true))). % 31.53/21.24 tff(c_3991, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_ContainerMembershipProperty), true, ifeq(iext(P_28, X_30, uri_rdf__3), true, true, true), true)=true))). % 31.53/21.24 tff(c_3741, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Datatype), true, ifeq(iext(P_28, X_30, uri_rdf_XMLLiteral), true, true, true), true)=true))). % 31.53/21.24 tff(c_3913, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_rdf__2, Y_21), true, true, true), true)=true))). % 31.53/21.24 tff(c_3792, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_rdf_object, Y_21), true, true, true), true)=true))). % 31.53/21.24 tff(c_3841, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, uri_rdf_Property, Y_21), true, true, true), true)=true))). % 31.53/21.24 tff(c_3513, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_rdf_subject, Y_21), true, true, true), true)=true))). % 31.53/21.24 tff(c_3510, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_rdf_subject), true, true, true), true)=true))). % 31.53/21.24 tff(c_3541, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_List), true, ifeq(iext(P_18, uri_rdf_nil, Y_21), true, true, true), true)=true))). % 31.53/21.24 tff(c_4039, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_rdf__1, Y_21), true, true, true), true)=true))). % 31.53/21.24 tff(c_3876, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_rdf__3, Y_21), true, true, true), true)=true))). % 31.53/21.24 tff(c_3952, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_ContainerMembershipProperty), true, ifeq(iext(P_18, uri_rdf__1, Y_21), true, true, true), true)=true))). % 31.53/21.24 tff(c_3449, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_ContainerMembershipProperty), true, ifeq(iext(P_18, uri_rdf__2, Y_21), true, true, true), true)=true))). % 31.53/21.24 tff(c_4079, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_rdf_value, Y_21), true, true, true), true)=true))). % 31.53/21.24 tff(c_3702, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_ex_c1), true, ifeq(iext(P_28, X_30, uri_ex_w), true, true, true), true)=true))). % 31.53/21.24 tff(c_4036, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_rdf__1), true, true, true), true)=true))). % 31.53/21.24 tff(c_3949, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_ContainerMembershipProperty), true, ifeq(iext(P_28, X_30, uri_rdf__1), true, true, true), true)=true))). % 31.53/21.24 tff(c_3838, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, uri_rdf_Property), true, true, true), true)=true))). % 31.53/21.24 tff(c_3446, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_ContainerMembershipProperty), true, ifeq(iext(P_28, X_30, uri_rdf__2), true, true, true), true)=true))). % 31.53/21.24 tff(c_3910, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_rdf__2), true, true, true), true)=true))). % 31.53/21.24 tff(c_3744, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Datatype), true, ifeq(iext(P_18, uri_rdf_XMLLiteral, Y_21), true, true, true), true)=true))). % 31.53/21.24 tff(c_4076, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_rdf_value), true, true, true), true)=true))). % 31.53/21.24 tff(c_3620, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_rdf_type), true, true, true), true)=true))). % 31.53/21.24 tff(c_3705, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_ex_c1), true, ifeq(iext(P_18, uri_ex_w, Y_21), true, true, true), true)=true))). % 31.53/21.24 tff(c_2036, plain, (![P_96, X_98, X_61]: (ifeq(iext(uri_rdfs_range, P_96, uri_rdfs_Resource), true, ifeq(iext(P_96, X_98, X_61), true, true, true), true)=true))). % 31.53/21.25 tff(c_1650, plain, (![P_92, X_61, Y_95]: (ifeq(iext(uri_rdfs_domain, P_92, uri_rdfs_Resource), true, ifeq(iext(P_92, X_61, Y_95), true, true, true), true)=true))). % 31.53/21.25 tff(c_2743, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_domain), true, ifeq(iext(P_103, uri_rdf_rest, uri_rdf_List), true, true, true), true)=true))). % 31.53/21.25 tff(c_37837, plain, (![X_812, Y_813]: (ifeq(iext(uri_rdfs_isDefinedBy, X_812, Y_813), true, iext(uri_rdfs_seeAlso, X_812, Y_813), true)=true))). % 31.53/21.25 tff(c_2803, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_subClassOf), true, ifeq(iext(P_103, uri_rdf_Alt, uri_rdfs_Container), true, true, true), true)=true))). % 31.53/21.25 tff(c_2707, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdf_type), true, ifeq(iext(P_103, uri_rdf__3, uri_rdf_Property), true, true, true), true)=true))). % 31.53/21.25 tff(c_2554, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdf_type), true, ifeq(iext(P_103, uri_rdf_rest, uri_rdf_Property), true, true, true), true)=true))). % 31.53/21.25 tff(c_2731, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_domain), true, ifeq(iext(P_103, uri_rdfs_member, uri_rdfs_Resource), true, true, true), true)=true))). % 31.53/21.25 tff(c_2875, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdf_type), true, ifeq(iext(P_103, uri_rdf_first, uri_rdf_Property), true, true, true), true)=true))). % 31.53/21.25 tff(c_2626, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_range), true, ifeq(iext(P_103, uri_rdfs_label, uri_rdfs_Literal), true, true, true), true)=true))). % 31.53/21.25 tff(c_2905, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_domain), true, ifeq(iext(P_103, uri_rdfs_subPropertyOf, uri_rdf_Property), true, true, true), true)=true))). % 31.53/21.25 tff(c_2614, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_domain), true, ifeq(iext(P_103, uri_rdfs_label, uri_rdfs_Resource), true, true, true), true)=true))). % 31.53/21.25 tff(c_2857, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_subClassOf), true, ifeq(iext(P_103, uri_rdfs_Datatype, uri_rdfs_Class), true, true, true), true)=true))). % 31.53/21.25 tff(c_2791, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_domain), true, ifeq(iext(P_103, uri_rdf_object, uri_rdfs_Statement), true, true, true), true)=true))). % 31.53/21.25 tff(c_2773, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_range), true, ifeq(iext(P_103, uri_rdfs_member, uri_rdfs_Resource), true, true, true), true)=true))). % 31.53/21.25 tff(c_2650, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdf_type), true, ifeq(iext(P_103, uri_rdf_value, uri_rdf_Property), true, true, true), true)=true))). % 31.53/21.25 tff(c_36166, plain, (![C_797]: (ifeq(iext(uri_rdfs_subClassOf, C_797, uri_rdf_Bag), true, iext(uri_rdfs_subClassOf, C_797, uri_rdfs_Container), true)=true))). % 31.53/21.25 tff(c_2620, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_range), true, ifeq(iext(P_103, uri_rdfs_subPropertyOf, uri_rdf_Property), true, true, true), true)=true))). % 31.53/21.25 tff(c_36115, plain, (![C_795]: (ifeq(iext(uri_rdfs_subClassOf, C_795, uri_rdfs_ContainerMembershipProperty), true, iext(uri_rdfs_subClassOf, C_795, uri_rdf_Property), true)=true))). % 31.53/21.25 tff(c_2851, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_range), true, ifeq(iext(P_103, uri_rdfs_seeAlso, uri_rdfs_Resource), true, true, true), true)=true))). % 31.53/21.25 tff(c_2572, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_range), true, ifeq(iext(P_103, uri_rdf_subject, uri_rdfs_Resource), true, true, true), true)=true))). % 31.53/21.25 tff(c_2713, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_domain), true, ifeq(iext(P_103, uri_rdf_predicate, uri_rdfs_Statement), true, true, true), true)=true))). % 31.53/21.25 tff(c_2584, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_subClassOf), true, ifeq(iext(P_103, uri_rdfs_Seq, uri_rdfs_Container), true, true, true), true)=true))). % 31.53/21.25 tff(c_2737, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_range), true, ifeq(iext(P_103, uri_rdf__1, uri_rdfs_Resource), true, true, true), true)=true))). % 31.53/21.25 tff(c_2797, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_subClassOf), true, ifeq(iext(P_103, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property), true, true, true), true)=true))). % 31.53/21.25 tff(c_35321, plain, (![C_787]: (ifeq(iext(uri_rdfs_subClassOf, C_787, uri_rdfs_Datatype), true, iext(uri_rdfs_subClassOf, C_787, uri_rdfs_Class), true)=true))). % 31.53/21.25 tff(c_2833, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_range), true, ifeq(iext(P_103, uri_rdfs_range, uri_rdfs_Class), true, true, true), true)=true))). % 31.53/21.25 tff(c_2638, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdf_type), true, ifeq(iext(P_103, uri_rdf__2, uri_rdf_Property), true, true, true), true)=true))). % 31.53/21.25 tff(c_2761, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_domain), true, ifeq(iext(P_103, uri_rdf__2, uri_rdfs_Resource), true, true, true), true)=true))). % 31.53/21.25 tff(c_2815, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_domain), true, ifeq(iext(P_103, uri_rdf__1, uri_rdfs_Resource), true, true, true), true)=true))). % 31.53/21.25 tff(c_2821, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_domain), true, ifeq(iext(P_103, uri_rdf_type, uri_rdfs_Resource), true, true, true), true)=true))). % 31.53/21.25 tff(c_2719, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdf_type), true, ifeq(iext(P_103, uri_rdf_XMLLiteral, uri_rdfs_Datatype), true, true, true), true)=true))). % 31.53/21.25 tff(c_2917, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_subClassOf), true, ifeq(iext(P_103, uri_ex_c, uri_ex_c1), true, true, true), true)=true))). % 31.53/21.25 tff(c_2542, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_range), true, ifeq(iext(P_103, uri_rdfs_subClassOf, uri_rdfs_Class), true, true, true), true)=true))). % 31.53/21.25 tff(c_2632, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdf_type), true, ifeq(iext(P_103, uri_rdf_object, uri_rdf_Property), true, true, true), true)=true))). % 31.53/21.25 tff(c_2839, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_domain), true, ifeq(iext(P_103, uri_rdf_value, uri_rdfs_Resource), true, true, true), true)=true))). % 31.53/21.25 tff(c_34017, plain, (![C_775]: (ifeq(iext(uri_rdfs_subClassOf, C_775, uri_rdfs_Seq), true, iext(uri_rdfs_subClassOf, C_775, uri_rdfs_Container), true)=true))). % 31.53/21.25 tff(c_2893, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_range), true, ifeq(iext(P_103, uri_rdf_first, uri_rdfs_Resource), true, true, true), true)=true))). % 31.53/21.25 tff(c_2845, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_range), true, ifeq(iext(P_103, uri_rdfs_comment, uri_rdfs_Literal), true, true, true), true)=true))). % 31.53/21.25 tff(c_2809, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_domain), true, ifeq(iext(P_103, uri_rdfs_subClassOf, uri_rdfs_Class), true, true, true), true)=true))). % 31.53/21.25 tff(c_2548, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdf_type), true, ifeq(iext(P_103, uri_rdf_subject, uri_rdf_Property), true, true, true), true)=true))). % 31.53/21.25 tff(c_2827, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_subClassOf), true, ifeq(iext(P_103, uri_rdf_Bag, uri_rdfs_Container), true, true, true), true)=true))). % 31.53/21.25 tff(c_2695, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdf_type), true, ifeq(iext(P_103, uri_rdf_type, uri_rdf_Property), true, true, true), true)=true))). % 31.53/21.25 tff(c_2869, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_domain), true, ifeq(iext(P_103, uri_rdf_first, uri_rdf_List), true, true, true), true)=true))). % 31.53/21.25 tff(c_2899, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdf_type), true, ifeq(iext(P_103, uri_rdf_Property, uri_rdfs_Class), true, true, true), true)=true))). % 31.53/21.25 tff(c_2596, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdf_type), true, ifeq(iext(P_103, uri_rdf__3, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 31.53/21.25 tff(c_2644, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_range), true, ifeq(iext(P_103, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true, true, true), true)=true))). % 31.53/21.25 tff(c_2749, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_domain), true, ifeq(iext(P_103, uri_rdfs_comment, uri_rdfs_Resource), true, true, true), true)=true))). % 31.53/21.25 tff(c_32606, plain, (![D_762]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_762), true, icext(D_762, uri_rdfs_member), true)=true))). % 31.53/21.25 tff(c_32540, plain, (![D_760]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_760), true, icext(D_760, uri_rdfs_Resource), true)=true))). % 31.53/21.25 tff(c_32474, plain, (![D_758]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_758), true, icext(D_758, uri_rdfs_seeAlso), true)=true))). % 31.53/21.25 tff(c_2566, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdf_type), true, ifeq(iext(P_103, uri_rdf__2, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 31.53/21.25 tff(c_32288, plain, (![D_755]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_755), true, icext(D_755, uri_rdfs_subPropertyOf), true)=true))). % 31.53/21.25 tff(c_32221, plain, (![D_753]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_753), true, icext(D_753, uri_rdfs_range), true)=true))). % 31.53/21.25 tff(c_32031, plain, (![D_750]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_750), true, icext(D_750, uri_owl_sameAs), true)=true))). % 31.53/21.25 tff(c_2863, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_range), true, ifeq(iext(P_103, uri_rdf_rest, uri_rdf_List), true, true, true), true)=true))). % 31.53/21.25 tff(c_31964, plain, (![D_748]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_748), true, icext(D_748, uri_ex_c), true)=true))). % 31.53/21.25 tff(c_31895, plain, (![D_746]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_746), true, icext(D_746, uri_rdf_Bag), true)=true))). % 31.53/21.25 tff(c_31829, plain, (![D_744]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_744), true, icext(D_744, uri_rdfs_ContainerMembershipProperty), true)=true))). % 31.53/21.25 tff(c_31762, plain, (![D_742]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_742), true, icext(D_742, uri_rdfs_Container), true)=true))). % 31.53/21.25 tff(c_2725, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_domain), true, ifeq(iext(P_103, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true, true, true), true)=true))). % 31.53/21.25 tff(c_31566, plain, (![D_739]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_739), true, icext(D_739, uri_rdf_Alt), true)=true))). % 31.53/21.25 tff(c_31471, plain, (![D_737]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_737), true, icext(D_737, uri_rdfs_Class), true)=true))). % 31.53/21.25 tff(c_31420, plain, (![P_735]: (ifeq(iext(uri_rdfs_subPropertyOf, P_735, uri_rdfs_isDefinedBy), true, iext(uri_rdfs_subPropertyOf, P_735, uri_rdfs_seeAlso), true)=true))). % 31.53/21.25 tff(c_31350, plain, (![D_733]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_733), true, icext(D_733, uri_rdfs_Datatype), true)=true))). % 31.53/21.25 tff(c_2785, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_owl_sameAs), true, ifeq(iext(P_103, uri_ex_c1, uri_ex_c2), true, true, true), true)=true))). % 31.53/21.25 tff(c_31163, plain, (![D_730]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_730), true, icext(D_730, uri_ex_c1), true)=true))). % 31.53/21.25 tff(c_31097, plain, (![D_728]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_728), true, icext(D_728, uri_rdfs_Literal), true)=true))). % 31.53/21.25 tff(c_31023, plain, (![D_726]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_726), true, icext(D_726, uri_rdf_XMLLiteral), true)=true))). % 31.53/21.25 tff(c_2608, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_range), true, ifeq(iext(P_103, uri_rdf__3, uri_rdfs_Resource), true, true, true), true)=true))). % 31.53/21.25 tff(c_30828, plain, (![D_723]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_723), true, icext(D_723, uri_rdfs_Seq), true)=true))). % 31.53/21.25 tff(c_30762, plain, (![D_721]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_721), true, icext(D_721, uri_rdfs_comment), true)=true))). % 31.53/21.25 tff(c_30696, plain, (![D_719]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_719), true, icext(D_719, uri_rdfs_isDefinedBy), true)=true))). % 31.53/21.25 tff(c_2656, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_range), true, ifeq(iext(P_103, uri_rdf__2, uri_rdfs_Resource), true, true, true), true)=true))). % 31.53/21.25 tff(c_30501, plain, (![D_716]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_716), true, icext(D_716, uri_rdf_predicate), true)=true))). % 31.53/21.25 tff(c_30435, plain, (![D_714]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_714), true, icext(D_714, uri_rdfs_subClassOf), true)=true))). % 31.53/21.25 tff(c_30369, plain, (![D_712]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_712), true, icext(D_712, uri_ex_p), true)=true))). % 31.53/21.25 tff(c_2602, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdf_type), true, ifeq(iext(P_103, uri_rdf__1, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 31.53/21.25 tff(c_30183, plain, (![D_709]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_709), true, icext(D_709, uri_rdfs_Statement), true)=true))). % 31.53/21.25 tff(c_30116, plain, (![D_707]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_707), true, icext(D_707, uri_rdf_List), true)=true))). % 31.53/21.25 tff(c_30050, plain, (![D_705]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_705), true, icext(D_705, uri_rdfs_label), true)=true))). % 31.53/21.25 tff(c_2683, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_range), true, ifeq(iext(P_103, uri_rdf_predicate, uri_rdfs_Resource), true, true, true), true)=true))). % 31.53/21.25 tff(c_29859, plain, (![D_702]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_702), true, icext(D_702, uri_rdfs_domain), true)=true))). % 31.53/21.25 tff(c_13318, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_rdfs_Resource, uri_rdfs_Class), true)=true))). % 31.53/21.25 tff(c_15589, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_ex_p, uri_ex_p), true)=true))). % 31.53/21.25 tff(c_2671, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_subPropertyOf), true, ifeq(iext(P_103, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso), true, true, true), true)=true))). % 31.53/21.25 tff(c_13270, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_rdfs_comment, uri_rdfs_comment), true)=true))). % 31.53/21.25 tff(c_13180, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_rdfs_label, uri_rdfs_label), true)=true))). % 31.53/21.25 tff(c_14513, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_rdf_predicate, uri_rdf_predicate), true)=true))). % 31.53/21.25 tff(c_12884, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_rdfs_Resource, uri_rdfs_Resource), true)=true))). % 31.53/21.25 tff(c_12944, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_rdfs_member, uri_rdf_Property), true)=true))). % 31.53/21.25 tff(c_2779, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_range), true, ifeq(iext(P_103, uri_rdfs_domain, uri_rdfs_Class), true, true, true), true)=true))). % 31.53/21.25 tff(c_12817, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_rdfs_member, uri_rdfs_member), true)=true))). % 31.53/21.25 tff(c_12605, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_rdfs_Statement, uri_rdfs_Statement), true)=true))). % 31.53/21.25 tff(c_29256, plain, (![D_683]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_683), true, icext(D_683, uri_rdf__1), true)=true))). % 31.53/21.25 tff(c_12672, plain, (![E_41]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, E_41), true, iext(uri_rdfs_subClassOf, uri_rdfs_Statement, E_41), true)=true))). % 31.53/21.25 tff(c_12465, plain, (![E_41]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, E_41), true, iext(uri_rdfs_subClassOf, uri_rdf_List, E_41), true)=true))). % 31.53/21.25 tff(c_12671, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_rdfs_Statement, uri_rdfs_Resource), true)=true))). % 31.53/21.25 tff(c_2578, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_domain), true, ifeq(iext(P_103, uri_rdfs_seeAlso, uri_rdfs_Resource), true, true, true), true)=true))). % 31.53/21.25 tff(c_12464, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_rdf_List, uri_rdfs_Resource), true)=true))). % 31.53/21.25 tff(c_12397, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_rdf_List, uri_rdf_List), true)=true))). % 31.53/21.25 tff(c_28937, plain, (![D_674]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_674), true, icext(D_674, uri_rdf_subject), true)=true))). % 31.53/21.25 tff(c_12256, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_rdfs_Datatype, uri_rdfs_Class), true)=true))). % 31.53/21.25 tff(c_12036, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_ex_c1, uri_rdfs_Class), true)=true))). % 31.53/21.25 tff(c_12304, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_rdf_Bag, uri_rdfs_Class), true)=true))). % 31.53/21.25 tff(c_12085, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_rdfs_Class, uri_rdfs_Class), true)=true))). % 31.53/21.25 tff(c_11940, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_rdfs_Seq, uri_rdfs_Class), true)=true))). % 31.53/21.26 tff(c_28740, plain, (![D_666]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_666), true, icext(D_666, uri_rdf__3), true)=true))). % 31.53/21.26 tff(c_12207, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_ex_c, uri_rdfs_Class), true)=true))). % 31.53/21.26 tff(c_28674, plain, (![C_663]: (ifeq(iext(uri_rdfs_subClassOf, C_663, uri_ex_c), true, iext(uri_rdfs_subClassOf, C_663, uri_ex_c1), true)=true))). % 31.53/21.26 tff(c_11814, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Class), true)=true))). % 31.53/21.26 tff(c_11767, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_rdf_Alt, uri_rdfs_Class), true)=true))). % 31.53/21.26 tff(c_12158, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_rdf_XMLLiteral, uri_rdfs_Class), true)=true))). % 31.53/21.26 tff(c_11892, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_rdfs_Literal, uri_rdfs_Class), true)=true))). % 31.53/21.26 tff(c_11987, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_rdfs_Container, uri_rdfs_Class), true)=true))). % 31.53/21.26 tff(c_11498, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_rdfs_label, uri_rdf_Property), true)=true))). % 31.53/21.26 tff(c_28532, plain, (![C_655]: (ifeq(iext(uri_rdfs_subClassOf, C_655, uri_rdf_XMLLiteral), true, iext(uri_rdfs_subClassOf, C_655, uri_rdfs_Literal), true)=true))). % 31.53/21.26 tff(c_11587, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_rdf_List, uri_rdfs_Class), true)=true))). % 31.53/21.26 tff(c_11445, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_rdfs_Statement, uri_rdfs_Class), true)=true))). % 31.53/21.26 tff(c_14276, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_rdf_predicate, uri_rdf_Property), true)=true))). % 31.53/21.26 tff(c_15455, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_ex_p, uri_rdf_Property), true)=true))). % 31.53/21.26 tff(c_11644, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_rdfs_comment, uri_rdf_Property), true)=true))). % 31.53/21.26 tff(c_5838, plain, (![E_41]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, E_41), true, iext(uri_rdfs_subClassOf, uri_rdf_Bag, E_41), true)=true))). % 31.53/21.26 tff(c_7143, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_rdfs_Seq, uri_rdfs_Seq), true)=true))). % 31.53/21.26 tff(c_2911, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_range), true, ifeq(iext(P_103, uri_rdf_type, uri_rdfs_Class), true, true, true), true)=true))). % 31.53/21.26 tff(c_10348, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_rdfs_subClassOf, uri_rdf_Property), true)=true))). % 31.53/21.26 tff(c_10413, plain, (![E_41]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, E_41), true, iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_41), true)=true))). % 31.53/21.26 tff(c_9257, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_rdf__2, uri_rdf__2), true)=true))). % 31.53/21.26 tff(c_9765, plain, (![E_41]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, E_41), true, iext(uri_rdfs_subClassOf, uri_rdfs_Literal, E_41), true)=true))). % 31.53/21.26 tff(c_8008, plain, (![R_53]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_member, R_53), true, iext(uri_rdfs_subPropertyOf, uri_rdf__1, R_53), true)=true))). % 31.53/21.26 tff(c_5336, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_rdf_Alt, uri_rdf_Alt), true)=true))). % 31.53/21.26 tff(c_7676, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_rdfs_isDefinedBy, uri_rdfs_isDefinedBy), true)=true))). % 31.53/21.26 tff(c_9563, plain, (![R_53]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_member, R_53), true, iext(uri_rdfs_subPropertyOf, uri_rdf__2, R_53), true)=true))). % 31.53/21.26 tff(c_5406, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf), true)=true))). % 31.53/21.26 tff(c_10897, plain, (![E_41]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, E_41), true, iext(uri_rdfs_subClassOf, uri_ex_c1, E_41), true)=true))). % 31.53/21.26 tff(c_27988, plain, (![D_633]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_633), true, icext(D_633, uri_rdf_value), true)=true))). % 31.53/21.26 tff(c_27890, plain, (![C_630]: (ifeq(iext(uri_rdfs_subClassOf, C_630, uri_rdf_Alt), true, iext(uri_rdfs_subClassOf, C_630, uri_rdfs_Container), true)=true))). % 31.53/21.26 tff(c_5035, plain, (![E_41]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, E_41), true, iext(uri_rdfs_subClassOf, uri_rdfs_Class, E_41), true)=true))). % 31.53/21.26 tff(c_8157, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_rdf_value, uri_rdf_value), true)=true))). % 31.53/21.26 tff(c_9117, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_rdf_Alt, uri_rdfs_Resource), true)=true))). % 31.53/21.26 tff(c_8984, plain, (![E_41]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, E_41), true, iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, E_41), true)=true))). % 31.53/21.26 tff(c_2590, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdf_type), true, ifeq(iext(P_103, uri_ex_w, uri_ex_c1), true, true, true), true)=true))). % 31.69/21.26 tff(c_8916, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_rdf_Property, uri_rdf_Property), true)=true))). % 31.69/21.26 tff(c_10267, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_rdf_object, uri_rdf_object), true)=true))). % 31.69/21.26 tff(c_8010, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_rdf__1, uri_rdfs_member), true)=true))). % 31.69/21.26 tff(c_4946, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_rdfs_ContainerMembershipProperty, uri_rdfs_ContainerMembershipProperty), true)=true))). % 31.69/21.26 tff(c_11258, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_rdfs_Class, uri_rdfs_Class), true)=true))). % 31.69/21.26 tff(c_10896, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_ex_c1, uri_rdfs_Resource), true)=true))). % 31.69/21.26 tff(c_9764, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_rdfs_Literal, uri_rdfs_Resource), true)=true))). % 31.69/21.26 tff(c_2701, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_domain), true, ifeq(iext(P_103, uri_rdf__3, uri_rdfs_Resource), true, true, true), true)=true))). % 31.69/21.26 tff(c_9904, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_rdfs_seeAlso, uri_rdf_Property), true)=true))). % 31.69/21.26 tff(c_9324, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_rdf__3, uri_rdfs_member), true)=true))). % 31.69/21.26 tff(c_8251, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_rdf__1, uri_rdf__1), true)=true))). % 31.69/21.26 tff(c_2677, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_domain), true, ifeq(iext(P_103, uri_rdfs_domain, uri_rdf_Property), true, true, true), true)=true))). % 31.69/21.26 tff(c_8983, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Resource), true)=true))). % 31.69/21.26 tff(c_26839, plain, (![D_598]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_598), true, icext(D_598, uri_rdf_nil), true)=true))). % 31.69/21.26 tff(c_5034, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_rdfs_Class, uri_rdfs_Resource), true)=true))). % 31.69/21.26 tff(c_8305, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_rdfs_isDefinedBy, uri_rdf_Property), true)=true))). % 31.69/21.26 tff(c_10699, plain, (![E_41]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, E_41), true, iext(uri_rdfs_subClassOf, uri_rdfs_Seq, E_41), true)=true))). % 31.69/21.26 tff(c_2767, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdf_type), true, ifeq(iext(P_103, uri_rdf__1, uri_rdf_Property), true, true, true), true)=true))). % 31.69/21.26 tff(c_5260, plain, (![E_41]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, E_41), true, iext(uri_rdfs_subClassOf, uri_ex_c, E_41), true)=true))). % 31.69/21.26 tff(c_26510, plain, (![D_589]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_589), true, icext(D_589, uri_rdf_first), true)=true))). % 31.69/21.26 tff(c_5837, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_rdf_Bag, uri_rdfs_Resource), true)=true))). % 31.69/21.26 tff(c_8396, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_rdfs_domain, uri_rdfs_domain), true)=true))). % 31.69/21.26 tff(c_2755, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_range), true, ifeq(iext(P_103, uri_ex_p, uri_ex_c1), true, true, true), true)=true))). % 31.69/21.26 tff(c_6761, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_rdf_Property, uri_rdfs_Resource), true)=true))). % 31.69/21.26 tff(c_11392, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_rdf_subject, uri_rdf_subject), true)=true))). % 31.69/21.26 tff(c_7760, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_rdf_XMLLiteral, uri_rdf_XMLLiteral), true)=true))). % 31.69/21.26 tff(c_9322, plain, (![R_53]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_member, R_53), true, iext(uri_rdfs_subPropertyOf, uri_rdf__3, R_53), true)=true))). % 31.69/21.26 tff(c_5259, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_ex_c, uri_rdfs_Resource), true)=true))). % 31.69/21.26 tff(c_9565, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_rdf__2, uri_rdfs_member), true)=true))). % 31.69/21.26 tff(c_7473, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_rdf_type, uri_rdf_type), true)=true))). % 31.69/21.26 tff(c_2881, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdf_type), true, ifeq(iext(P_103, uri_rdf_nil, uri_rdf_List), true, true, true), true)=true))). % 31.69/21.26 tff(c_9701, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_rdf_first, uri_rdf_first), true)=true))). % 31.69/21.26 tff(c_8551, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_rdf_XMLLiteral, uri_rdfs_Resource), true)=true))). % 31.69/21.26 tff(c_9636, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_rdfs_subClassOf, uri_rdfs_subClassOf), true)=true))). % 31.69/21.26 tff(c_8552, plain, (![E_41]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, E_41), true, iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, E_41), true)=true))). % 31.69/21.26 tff(c_10124, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_rdfs_domain, uri_rdf_Property), true)=true))). % 31.69/21.26 tff(c_10567, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_rdfs_Datatype, uri_rdfs_Datatype), true)=true))). % 31.69/21.26 tff(c_8720, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_owl_sameAs, uri_rdf_Property), true)=true))). % 31.69/21.26 tff(c_8663, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_ex_c1, uri_ex_c1), true)=true))). % 31.69/21.26 tff(c_25731, plain, (![D_563]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_563), true, icext(D_563, uri_rdf__2), true)=true))). % 31.69/21.26 tff(c_10698, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_rdfs_Seq, uri_rdfs_Resource), true)=true))). % 31.69/21.26 tff(c_7934, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_owl_sameAs, uri_owl_sameAs), true)=true))). % 31.69/21.26 tff(c_7563, plain, (![E_41]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, E_41), true, iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, E_41), true)=true))). % 31.69/21.26 tff(c_2689, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_domain), true, ifeq(iext(P_103, uri_rdf_subject, uri_rdfs_Statement), true, true, true), true)=true))). % 31.69/21.26 tff(c_7562, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_rdfs_Datatype, uri_rdfs_Resource), true)=true))). % 31.69/21.26 tff(c_5701, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_rdf_rest, uri_rdf_rest), true)=true))). % 31.69/21.26 tff(c_25413, plain, (![D_554]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_554), true, icext(D_554, uri_rdf__2), true)=true))). % 31.69/21.26 tff(c_6316, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_rdfs_Container, uri_rdfs_Container), true)=true))). % 31.69/21.26 tff(c_10412, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_rdfs_Container, uri_rdfs_Resource), true)=true))). % 31.69/21.26 tff(c_2662, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_subClassOf), true, ifeq(iext(P_103, uri_rdf_XMLLiteral, uri_rdfs_Literal), true, true, true), true)=true))). % 31.69/21.26 tff(c_6762, plain, (![E_41]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, E_41), true, iext(uri_rdfs_subClassOf, uri_rdf_Property, E_41), true)=true))). % 31.69/21.26 tff(c_5583, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_rdfs_seeAlso, uri_rdfs_seeAlso), true)=true))). % 31.69/21.26 tff(c_6939, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_rdfs_Literal, uri_rdfs_Literal), true)=true))). % 31.69/21.26 tff(c_25112, plain, (![D_545]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_545), true, icext(D_545, uri_rdf__1), true)=true))). % 31.69/21.26 tff(c_10635, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_rdfs_range, uri_rdfs_range), true)=true))). % 31.69/21.26 tff(c_9118, plain, (![E_41]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, E_41), true, iext(uri_rdfs_subClassOf, uri_rdf_Alt, E_41), true)=true))). % 31.69/21.26 tff(c_2887, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_domain), true, ifeq(iext(P_103, uri_rdfs_range, uri_rdf_Property), true, true, true), true)=true))). % 31.69/21.26 tff(c_7257, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_rdfs_subPropertyOf, uri_rdf_Property), true)=true))). % 31.69/21.26 tff(c_8462, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_rdf__3, uri_rdf__3), true)=true))). % 31.69/21.26 tff(c_11324, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_rdf_Bag, uri_rdf_Bag), true)=true))). % 31.69/21.26 tff(c_6464, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_rdfs_range, uri_rdf_Property), true)=true))). % 31.69/21.26 tff(c_10828, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_ex_c, uri_ex_c), true)=true))). % 31.69/21.26 tff(c_2560, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_range), true, ifeq(iext(P_103, uri_rdf_value, uri_rdfs_Resource), true, true, true), true)=true))). % 31.69/21.26 tff(c_4822, plain, (![Q_48, X_139]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, X_139, uri_rdfs_Resource), true)=true))). % 31.69/21.26 tff(c_2976, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_104), true, iext(Q_104, uri_rdf_nil, uri_rdf_List), true)=true))). % 31.69/21.26 tff(c_2961, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_104), true, iext(Q_104, uri_rdf_object, uri_rdfs_Statement), true)=true))). % 31.69/21.26 tff(c_24356, plain, (![D_526]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_526), true, icext(D_526, uri_rdf_type), true)=true))). % 31.69/21.26 tff(c_2972, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_104), true, iext(Q_104, uri_rdfs_Datatype, uri_rdfs_Class), true)=true))). % 31.69/21.26 tff(c_2929, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_104), true, iext(Q_104, uri_rdf__3, uri_rdfs_ContainerMembershipProperty), true)=true))). % 31.69/21.26 tff(c_2974, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_104), true, iext(Q_104, uri_rdf_first, uri_rdf_List), true)=true))). % 31.69/21.26 tff(c_2932, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_104), true, iext(Q_104, uri_rdfs_label, uri_rdfs_Resource), true)=true))). % 31.69/21.26 tff(c_2937, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_104), true, iext(Q_104, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true)=true))). % 31.69/21.26 tff(c_2965, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_104), true, iext(Q_104, uri_rdf__1, uri_rdfs_Resource), true)=true))). % 31.69/21.26 tff(c_2947, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_104), true, iext(Q_104, uri_rdf__3, uri_rdf_Property), true)=true))). % 31.69/21.26 tff(c_2928, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_104), true, iext(Q_104, uri_ex_w, uri_ex_c1), true)=true))). % 31.69/21.26 tff(c_2963, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_104), true, iext(Q_104, uri_rdf_Alt, uri_rdfs_Container), true)=true))). % 31.69/21.26 tff(c_2980, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_104), true, iext(Q_104, uri_rdfs_subPropertyOf, uri_rdf_Property), true)=true))). % 31.69/21.26 tff(c_2936, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_104), true, iext(Q_104, uri_rdf__2, uri_rdf_Property), true)=true))). % 31.69/21.26 tff(c_2951, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_104), true, iext(Q_104, uri_rdfs_member, uri_rdfs_Resource), true)=true))). % 31.69/21.26 tff(c_2459, plain, (![E_101]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_101), true, iext(uri_rdfs_subClassOf, uri_rdf_Alt, E_101), true)=true))). % 31.69/21.26 tff(c_2977, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_104), true, iext(Q_104, uri_rdfs_range, uri_rdf_Property), true)=true))). % 31.69/21.26 tff(c_2949, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_104), true, iext(Q_104, uri_rdf_XMLLiteral, uri_rdfs_Datatype), true)=true))). % 31.69/21.26 tff(c_2930, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_104), true, iext(Q_104, uri_rdf__1, uri_rdfs_ContainerMembershipProperty), true)=true))). % 31.69/21.26 tff(c_23989, plain, (![D_508]: (ifeq(iext(uri_rdfs_subClassOf, uri_ex_c1, D_508), true, icext(D_508, uri_ex_w), true)=true))). % 31.69/21.26 tff(c_2978, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_104), true, iext(Q_104, uri_rdf_first, uri_rdfs_Resource), true)=true))). % 31.69/21.27 tff(c_2941, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_104), true, iext(Q_104, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso), true)=true))). % 31.69/21.27 tff(c_2950, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_104), true, iext(Q_104, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true)=true))). % 31.69/21.27 tff(c_2964, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_104), true, iext(Q_104, uri_rdfs_subClassOf, uri_rdfs_Class), true)=true))). % 31.69/21.27 tff(c_2460, plain, (![E_101]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_101), true, iext(uri_rdfs_subClassOf, uri_rdf_Bag, E_101), true)=true))). % 31.69/21.27 tff(c_2954, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_104), true, iext(Q_104, uri_rdfs_comment, uri_rdfs_Resource), true)=true))). % 31.69/21.27 tff(c_2957, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_104), true, iext(Q_104, uri_rdf__1, uri_rdf_Property), true)=true))). % 31.69/21.27 tff(c_23783, plain, (![D_499]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_499), true, icext(D_499, uri_rdf_object), true)=true))). % 31.69/21.27 tff(c_2953, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_104), true, iext(Q_104, uri_rdf_rest, uri_rdf_List), true)=true))). % 31.69/21.27 tff(c_2926, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_104), true, iext(Q_104, uri_rdfs_seeAlso, uri_rdfs_Resource), true)=true))). % 31.69/21.27 tff(c_2960, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_owl_sameAs, Q_104), true, iext(Q_104, uri_ex_c1, uri_ex_c2), true)=true))). % 31.69/21.27 tff(c_2935, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_104), true, iext(Q_104, uri_rdf_object, uri_rdf_Property), true)=true))). % 31.69/21.27 tff(c_2962, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_104), true, iext(Q_104, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property), true)=true))). % 31.69/21.27 tff(c_2955, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_104), true, iext(Q_104, uri_ex_p, uri_ex_c1), true)=true))). % 31.69/21.27 tff(c_2924, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_104), true, iext(Q_104, uri_rdf__2, uri_rdfs_ContainerMembershipProperty), true)=true))). % 31.69/21.27 tff(c_2945, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_104), true, iext(Q_104, uri_rdf_type, uri_rdf_Property), true)=true))). % 31.69/21.27 tff(c_2940, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_104), true, iext(Q_104, uri_rdf_XMLLiteral, uri_rdfs_Literal), true)=true))). % 31.69/21.27 tff(c_2457, plain, (![E_101]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Literal, E_101), true, iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, E_101), true)=true))). % 31.69/21.27 tff(c_2970, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_104), true, iext(Q_104, uri_rdfs_comment, uri_rdfs_Literal), true)=true))). % 31.69/21.27 tff(c_2973, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_104), true, iext(Q_104, uri_rdf_rest, uri_rdf_List), true)=true))). % 31.69/21.27 tff(c_2975, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_104), true, iext(Q_104, uri_rdf_first, uri_rdf_Property), true)=true))). % 31.69/21.27 tff(c_2981, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_104), true, iext(Q_104, uri_rdf_type, uri_rdfs_Class), true)=true))). % 31.69/21.27 tff(c_2462, plain, (![E_101]: (ifeq(iext(uri_rdfs_subClassOf, uri_ex_c1, E_101), true, iext(uri_rdfs_subClassOf, uri_ex_c, E_101), true)=true))). % 31.69/21.27 tff(c_2946, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_104), true, iext(Q_104, uri_rdf__3, uri_rdfs_Resource), true)=true))). % 31.69/21.27 tff(c_2942, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_104), true, iext(Q_104, uri_rdfs_domain, uri_rdf_Property), true)=true))). % 31.69/21.27 tff(c_2969, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_104), true, iext(Q_104, uri_rdf_value, uri_rdfs_Resource), true)=true))). % 31.69/21.27 tff(c_2967, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_104), true, iext(Q_104, uri_rdf_Bag, uri_rdfs_Container), true)=true))). % 31.69/21.27 tff(c_2923, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_104), true, iext(Q_104, uri_rdf_value, uri_rdfs_Resource), true)=true))). % 31.69/21.27 tff(c_2956, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_104), true, iext(Q_104, uri_rdf__2, uri_rdfs_Resource), true)=true))). % 31.69/21.27 tff(c_2982, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_104), true, iext(Q_104, uri_ex_c, uri_ex_c1), true)=true))). % 31.69/21.27 tff(c_2971, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_104), true, iext(Q_104, uri_rdfs_seeAlso, uri_rdfs_Resource), true)=true))). % 31.69/21.27 tff(c_14515, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_predicate), true)=true))). % 31.69/21.27 tff(c_14514, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_predicate), true)=true))). % 31.69/21.27 tff(c_15590, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_ex_p), true)=true))). % 31.69/21.27 tff(c_15591, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_ex_p), true)=true))). % 31.69/21.27 tff(c_13182, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_label), true)=true))). % 31.69/21.27 tff(c_2939, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_104), true, iext(Q_104, uri_rdf__2, uri_rdfs_Resource), true)=true))). % 31.69/21.27 tff(c_13181, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_label), true)=true))). % 31.69/21.27 tff(c_13271, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_comment), true)=true))). % 31.69/21.27 tff(c_13272, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_comment), true)=true))). % 31.69/21.27 tff(c_23033, plain, (![D_465]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_465), true, icext(D_465, uri_rdf_Property), true)=true))). % 31.69/21.27 tff(c_12888, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Resource), true)=true))). % 31.69/21.27 tff(c_12819, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_member), true)=true))). % 31.69/21.27 tff(c_2979, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_104), true, iext(Q_104, uri_rdf_Property, uri_rdfs_Class), true)=true))). % 31.69/21.27 tff(c_12400, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_List), true)=true))). % 31.69/21.27 tff(c_22858, plain, (![D_459]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, D_459), true, icext(D_459, uri_rdf_XMLLiteral), true)=true))). % 31.69/21.27 tff(c_2934, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_104), true, iext(Q_104, uri_rdfs_label, uri_rdfs_Literal), true)=true))). % 31.69/21.27 tff(c_12401, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdf_List), true)=true))). % 31.69/21.27 tff(c_12608, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Statement), true)=true))). % 31.69/21.27 tff(c_12609, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Statement), true)=true))). % 31.69/21.27 tff(c_22699, plain, (![D_453]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_453), true, icext(D_453, uri_rdf_rest), true)=true))). % 31.69/21.27 tff(c_3010, plain, (![R_108]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_seeAlso, R_108), true, iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, R_108), true)=true))). % 31.69/21.27 tff(c_2938, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_104), true, iext(Q_104, uri_rdf_value, uri_rdf_Property), true)=true))). % 31.69/21.27 tff(c_2920, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_104), true, iext(Q_104, uri_rdfs_subClassOf, uri_rdfs_Class), true)=true))). % 31.69/21.27 tff(c_22548, plain, (![D_448]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_448), true, icext(D_448, uri_rdf__3), true)=true))). % 31.69/21.27 tff(c_2921, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_104), true, iext(Q_104, uri_rdf_subject, uri_rdf_Property), true)=true))). % 31.69/21.27 tff(c_22356, plain, (![C_89, X_61]: (ifeq(icext(C_89, X_61), true, true, true)=true))). % 31.69/21.27 tff(c_2461, plain, (![E_101]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, E_101), true, iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, E_101), true)=true))). % 31.69/21.27 tff(c_9702, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_first), true)=true))). % 31.69/21.27 tff(c_21891, plain, (![D_439, X_440]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, D_439), true, icext(D_439, X_440), true)=true))). % 31.69/21.27 tff(c_2968, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_104), true, iext(Q_104, uri_rdfs_range, uri_rdfs_Class), true)=true))). % 31.69/21.27 tff(c_9258, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__2), true)=true))). % 31.69/21.27 tff(c_21420, plain, (![X_433, Y_434]: (ifeq(iext(uri_rdfs_subPropertyOf, X_433, Y_434), true, icext(uri_rdf_Property, X_433), true)=true))). % 31.69/21.27 tff(c_2943, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_104), true, iext(Q_104, uri_rdf_predicate, uri_rdfs_Resource), true)=true))). % 31.69/21.27 tff(c_20805, plain, (![X_427, Y_428]: (ifeq(iext(uri_rdfs_subClassOf, X_427, Y_428), true, icext(uri_rdfs_Class, Y_428), true)=true))). % 31.69/21.27 tff(c_7146, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Seq), true)=true))). % 31.69/21.27 tff(c_2931, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_104), true, iext(Q_104, uri_rdf__3, uri_rdfs_Resource), true)=true))). % 31.69/21.27 tff(c_9637, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_subClassOf), true)=true))). % 31.69/21.27 tff(c_20695, plain, (![X_420, Y_421]: (ifeq(iext(uri_rdfs_comment, X_420, Y_421), true, icext(uri_rdfs_Literal, Y_421), true)=true))). % 31.69/21.27 tff(c_10636, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_range), true)=true))). % 31.69/21.27 tff(c_2456, plain, (![E_101]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_101), true, iext(uri_rdfs_subClassOf, uri_rdfs_Seq, E_101), true)=true))). % 31.69/21.27 tff(c_7763, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_XMLLiteral), true)=true))). % 31.69/21.27 tff(c_20282, plain, (![X_413, Y_414]: (ifeq(iext(uri_rdfs_domain, X_413, Y_414), true, icext(uri_rdfs_Class, Y_414), true)=true))). % 31.69/21.27 tff(c_7936, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_owl_sameAs), true)=true))). % 31.69/21.27 tff(c_2458, plain, (![E_101]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, E_101), true, iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, E_101), true)=true))). % 31.69/21.27 tff(c_8398, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_domain), true)=true))). % 31.69/21.27 tff(c_9703, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_first), true)=true))). % 31.69/21.27 tff(c_8012, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__1), true)=true))). % 31.69/21.27 tff(c_20117, plain, (![X_404, Y_405]: (ifeq(iext(uri_rdfs_label, X_404, Y_405), true, icext(uri_rdfs_Literal, Y_405), true)=true))). % 31.69/21.27 tff(c_5585, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_seeAlso), true)=true))). % 31.69/21.27 tff(c_2959, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_104), true, iext(Q_104, uri_rdfs_domain, uri_rdfs_Class), true)=true))). % 31.69/21.27 tff(c_8159, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_value), true)=true))). % 31.69/21.27 tff(c_10269, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_object), true)=true))). % 31.69/21.27 tff(c_19972, plain, (![X_396, Y_397]: (ifeq(iext(uri_rdf_rest, X_396, Y_397), true, icext(uri_rdf_List, X_396), true)=true))). % 31.69/21.27 tff(c_11393, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_subject), true)=true))). % 31.69/21.27 tff(c_2927, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_104), true, iext(Q_104, uri_rdfs_Seq, uri_rdfs_Container), true)=true))). % 31.69/21.27 tff(c_8252, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__1), true)=true))). % 31.69/21.27 tff(c_7475, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_type), true)=true))). % 31.69/21.27 tff(c_19835, plain, (![X_388, Y_389]: (ifeq(iext(uri_ex_p, X_388, Y_389), true, icext(uri_ex_c1, Y_389), true)=true))). % 31.69/21.27 tff(c_2922, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_104), true, iext(Q_104, uri_rdf_rest, uri_rdf_Property), true)=true))). % 31.69/21.27 tff(c_8667, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_ex_c1), true)=true))). % 31.69/21.27 tff(c_10416, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Container), true)=true))). % 31.69/21.27 tff(c_19109, plain, (![X_380, Y_381]: (ifeq(iext(uri_rdfs_subClassOf, X_380, Y_381), true, icext(uri_rdfs_Class, X_380), true)=true))). % 31.69/21.27 tff(c_8463, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__3), true)=true))). % 31.69/21.27 tff(c_4948, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_ContainerMembershipProperty), true)=true))). % 31.69/21.27 tff(c_2952, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_104), true, iext(Q_104, uri_rdf__1, uri_rdfs_Resource), true)=true))). % 31.69/21.27 tff(c_10268, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_object), true)=true))). % 31.69/21.27 tff(c_5338, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_Alt), true)=true))). % 31.69/21.27 tff(c_8397, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_domain), true)=true))). % 31.69/21.27 tff(c_18555, plain, (![X_370, Y_371]: (ifeq(iext(uri_rdfs_domain, X_370, Y_371), true, icext(uri_rdf_Property, X_370), true)=true))). % 31.69/21.27 tff(c_5038, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Class), true)=true))). % 31.69/21.27 tff(c_5703, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_rest), true)=true))). % 31.69/21.27 tff(c_2966, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_104), true, iext(Q_104, uri_rdf_type, uri_rdfs_Resource), true)=true))). % 31.69/21.27 tff(c_9259, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__2), true)=true))). % 31.69/21.27 tff(c_9638, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_subClassOf), true)=true))). % 31.69/21.27 tff(c_8158, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_value), true)=true))). % 31.69/21.27 tff(c_18365, plain, (![X_360, Y_361]: (ifeq(iext(uri_rdf_first, X_360, Y_361), true, icext(uri_rdf_List, X_360), true)=true))). % 31.69/21.27 tff(c_8464, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__3), true)=true))). % 31.69/21.27 tff(c_10570, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Datatype), true)=true))). % 31.69/21.27 tff(c_2958, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_104), true, iext(Q_104, uri_rdfs_member, uri_rdfs_Resource), true)=true))). % 31.69/21.27 tff(c_6943, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Literal), true)=true))). % 31.69/21.27 tff(c_17751, plain, (![X_352, Y_353]: (ifeq(iext(uri_rdf_type, X_352, Y_353), true, icext(uri_rdfs_Class, Y_353), true)=true))). % 31.69/21.27 tff(c_5407, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_subPropertyOf), true)=true))). % 31.69/21.27 tff(c_6765, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdf_Property), true)=true))). % 31.69/21.27 tff(c_2948, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_104), true, iext(Q_104, uri_rdf_predicate, uri_rdfs_Statement), true)=true))). % 31.69/21.27 tff(c_7677, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_isDefinedBy), true)=true))). % 31.69/21.27 tff(c_10637, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_range), true)=true))). % 31.69/21.27 tff(c_17590, plain, (![X_343, Y_344]: (ifeq(iext(uri_rdf_object, X_343, Y_344), true, icext(uri_rdfs_Statement, X_343), true)=true))). % 31.69/21.27 tff(c_8011, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_member), true)=true))). % 31.69/21.27 tff(c_7474, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_type), true)=true))). % 31.69/21.27 tff(c_2944, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_104), true, iext(Q_104, uri_rdf_subject, uri_rdfs_Statement), true)=true))). % 31.69/21.27 tff(c_7935, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_owl_sameAs), true)=true))). % 31.69/21.27 tff(c_17145, plain, (![X_335, Y_336]: (ifeq(iext(uri_rdfs_range, X_335, Y_336), true, icext(uri_rdf_Property, X_335), true)=true))). % 31.69/21.27 tff(c_5839, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Resource), true)=true))). % 31.69/21.27 tff(c_10831, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_ex_c), true)=true))). % 31.69/21.27 tff(c_2925, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_104), true, iext(Q_104, uri_rdf_subject, uri_rdfs_Resource), true)=true))). % 31.69/21.27 tff(c_16719, plain, (![X_328, Y_329]: (ifeq(iext(uri_rdfs_range, X_328, Y_329), true, icext(uri_rdfs_Class, Y_329), true)=true))). % 31.69/21.27 tff(c_11394, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_subject), true)=true))). % 31.69/21.27 tff(c_11327, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_Bag), true)=true))). % 31.69/21.27 tff(c_2933, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_104), true, iext(Q_104, uri_rdfs_subPropertyOf, uri_rdf_Property), true)=true))). % 31.69/21.27 tff(c_5408, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_subPropertyOf), true)=true))). % 31.69/21.27 tff(c_5702, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_rest), true)=true))). % 31.69/21.27 tff(c_4824, plain, (![C_19, X_139]: (ifeq(iext(uri_rdfs_domain, uri_rdf_type, C_19), true, icext(C_19, X_139), true)=true))). % 31.69/21.27 tff(c_15985, plain, (![X_317, Y_318]: (ifeq(iext(uri_rdfs_subPropertyOf, X_317, Y_318), true, icext(uri_rdf_Property, Y_318), true)=true))). % 31.69/21.27 tff(c_4823, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_29), true, icext(C_29, uri_rdfs_Resource), true)=true))). % 31.69/21.27 tff(c_1944, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_member), true)=true))). % 31.69/21.27 tff(c_1967, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdf_first), true)=true))). % 31.69/21.27 tff(c_1969, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_subPropertyOf), true)=true))). % 31.69/21.27 tff(c_1956, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_range), true)=true))). % 31.69/21.27 tff(c_1915, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_label), true)=true))). % 31.69/21.27 tff(c_1954, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf_type), true)=true))). % 31.69/21.27 tff(c_2335, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_97), true, icext(C_97, uri_rdf_Property), true)=true))). % 31.69/21.27 tff(c_1914, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_subPropertyOf), true)=true))). % 31.69/21.27 tff(c_2347, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_97), true, icext(C_97, uri_rdf_List), true)=true))). % 31.69/21.27 tff(c_15098, plain, (![X_290, Y_291]: (ifeq(iext(uri_rdf_subject, X_290, Y_291), true, icext(uri_rdfs_Statement, X_290), true)=true))). % 31.69/21.27 tff(c_1937, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf_rest), true)=true))). % 31.69/21.27 tff(c_2333, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_owl_sameAs, C_97), true, icext(C_97, uri_ex_c2), true)=true))). % 31.69/21.27 tff(c_1933, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_isDefinedBy), true)=true))). % 31.69/21.27 tff(c_15518, plain, (![S_5, O_6]: (ifeq(iext(uri_ex_p, S_5, O_6), true, true, true)=true))). % 31.69/21.27 tff(c_15536, plain, (iext(uri_rdfs_subPropertyOf, uri_ex_p, uri_ex_p)=true)). % 31.69/21.28 tff(c_15495, plain, (ip(uri_ex_p)=true)). % 31.69/21.28 tff(c_1939, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_comment), true)=true))). % 31.69/21.28 tff(c_15413, plain, (iext(uri_rdf_type, uri_ex_p, uri_rdf_Property)=true)). % 31.69/21.28 tff(c_15231, plain, (icext(uri_rdf_Property, uri_ex_p)=true)). % 31.69/21.28 tff(c_1940, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_ex_p), true)=true))). % 31.69/21.28 tff(c_2310, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_97), true, icext(C_97, uri_rdfs_Literal), true)=true))). % 31.69/21.28 tff(c_1924, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdf_predicate), true)=true))). % 31.69/21.28 tff(c_2350, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_97), true, icext(C_97, uri_rdf_List), true)=true))). % 31.69/21.28 tff(c_2337, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdfs_Class), true)=true))). % 31.69/21.28 tff(c_2311, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_97), true, icext(C_97, uri_rdfs_seeAlso), true)=true))). % 31.69/21.28 tff(c_1904, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdf_subject), true)=true))). % 31.69/21.28 tff(c_1935, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_member), true)=true))). % 31.69/21.28 tff(c_1925, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf_subject), true)=true))). % 31.69/21.28 tff(c_1958, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf_value), true)=true))). % 31.69/21.28 tff(c_2301, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_97), true, icext(C_97, uri_rdf_Property), true)=true))). % 31.69/21.28 tff(c_1971, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_93), true, icext(C_93, uri_ex_c), true)=true))). % 31.69/21.28 tff(c_1948, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_93), true, icext(C_93, uri_rdfs_ContainerMembershipProperty), true)=true))). % 31.69/21.28 tff(c_14639, plain, (![X_270, Y_271]: (ifeq(iext(uri_rdf_rest, X_270, Y_271), true, icext(uri_rdf_List, Y_271), true)=true))). % 31.69/21.28 tff(c_2354, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_97), true, icext(C_97, uri_rdfs_Class), true)=true))). % 31.69/21.28 tff(c_1911, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdf__3), true)=true))). % 31.69/21.28 tff(c_2346, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_97), true, icext(C_97, uri_rdfs_Class), true)=true))). % 31.69/21.28 tff(c_1970, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdf_type), true)=true))). % 31.69/21.28 tff(c_1952, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf__1), true)=true))). % 31.69/21.28 tff(c_1946, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_owl_sameAs, C_93), true, icext(C_93, uri_ex_c1), true)=true))). % 31.69/21.28 tff(c_14460, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_predicate, uri_rdf_predicate)=true)). % 31.69/21.28 tff(c_14291, plain, (ip(uri_rdf_predicate)=true)). % 31.69/21.28 tff(c_14234, plain, (iext(uri_rdf_type, uri_rdf_predicate, uri_rdf_Property)=true)). % 31.69/21.28 tff(c_14178, plain, (icext(uri_rdf_Property, uri_rdf_predicate)=true)). % 31.69/21.28 tff(c_1930, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf_predicate), true)=true))). % 31.69/21.28 tff(c_1960, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_seeAlso), true)=true))). % 31.69/21.28 tff(c_1955, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_93), true, icext(C_93, uri_rdf_Bag), true)=true))). % 31.69/21.28 tff(c_1966, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_range), true)=true))). % 31.69/21.28 tff(c_1906, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_seeAlso), true)=true))). % 31.69/21.28 tff(c_2327, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_97), true, icext(C_97, uri_ex_c1), true)=true))). % 31.69/21.28 tff(c_1907, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_93), true, icext(C_93, uri_rdfs_Seq), true)=true))). % 31.69/21.28 tff(c_2357, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_97), true, icext(C_97, uri_ex_c1), true)=true))). % 31.69/21.28 tff(c_2295, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_97), true, icext(C_97, uri_ex_c1), true)=true))). % 31.69/21.28 tff(c_1902, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdf_value), true)=true))). % 31.69/21.28 tff(c_2302, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_97), true, icext(C_97, uri_rdfs_Literal), true)=true))). % 31.69/21.28 tff(c_2320, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_97), true, icext(C_97, uri_rdfs_Datatype), true)=true))). % 31.69/21.28 tff(c_12610, plain, (![X_33]: (ifeq(icext(uri_rdfs_Statement, X_33), true, icext(uri_rdfs_Statement, X_33), true)=true))). % 31.69/21.28 tff(c_13408, plain, (![X_237, Y_238]: (ifeq(iext(uri_rdf_predicate, X_237, Y_238), true, icext(uri_rdfs_Statement, X_237), true)=true))). % 31.69/21.28 tff(c_12402, plain, (![X_33]: (ifeq(icext(uri_rdf_List, X_33), true, icext(uri_rdf_List, X_33), true)=true))). % 31.69/21.28 tff(c_11263, plain, (![X_33]: (ifeq(icext(uri_rdfs_Class, X_33), true, icext(uri_rdfs_Class, X_33), true)=true))). % 31.69/21.28 tff(c_5340, plain, (![X_33]: (ifeq(icext(uri_rdf_Alt, X_33), true, icext(uri_rdf_Alt, X_33), true)=true))). % 31.69/21.28 tff(c_1949, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_93), true, icext(C_93, uri_rdf_Alt), true)=true))). % 31.69/21.28 tff(c_10833, plain, (![X_33]: (ifeq(icext(uri_ex_c, X_33), true, icext(uri_ex_c, X_33), true)=true))). % 31.69/21.28 tff(c_8921, plain, (![X_33]: (ifeq(icext(uri_rdf_Property, X_33), true, icext(uri_rdf_Property, X_33), true)=true))). % 31.69/21.28 tff(c_10572, plain, (![X_33]: (ifeq(icext(uri_rdfs_Datatype, X_33), true, icext(uri_rdfs_Datatype, X_33), true)=true))). % 31.69/21.28 tff(c_4950, plain, (![X_33]: (ifeq(icext(uri_rdfs_ContainerMembershipProperty, X_33), true, icext(uri_rdfs_ContainerMembershipProperty, X_33), true)=true))). % 31.69/21.28 tff(c_7765, plain, (![X_33]: (ifeq(icext(uri_rdf_XMLLiteral, X_33), true, icext(uri_rdf_XMLLiteral, X_33), true)=true))). % 31.69/21.28 tff(c_8668, plain, (![X_33]: (ifeq(icext(uri_ex_c1, X_33), true, icext(uri_ex_c1, X_33), true)=true))). % 31.69/21.28 tff(c_11329, plain, (![X_33]: (ifeq(icext(uri_rdf_Bag, X_33), true, icext(uri_rdf_Bag, X_33), true)=true))). % 31.69/21.28 tff(c_6321, plain, (![X_33]: (ifeq(icext(uri_rdfs_Container, X_33), true, icext(uri_rdfs_Container, X_33), true)=true))). % 31.69/21.28 tff(c_1921, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_93), true, icext(C_93, uri_rdf_XMLLiteral), true)=true))). % 31.69/21.28 tff(c_6944, plain, (![X_33]: (ifeq(icext(uri_rdfs_Literal, X_33), true, icext(uri_rdfs_Literal, X_33), true)=true))). % 31.69/21.28 tff(c_7148, plain, (![X_33]: (ifeq(icext(uri_rdfs_Seq, X_33), true, icext(uri_rdfs_Seq, X_33), true)=true))). % 31.69/21.28 tff(c_13282, plain, (iext(uri_rdf_type, uri_rdfs_Resource, uri_rdfs_Class)=true)). % 31.69/21.28 tff(c_13217, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_comment, uri_rdfs_comment)=true)). % 31.69/21.28 tff(c_1961, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_93), true, icext(C_93, uri_rdfs_Datatype), true)=true))). % 31.69/21.28 tff(c_13127, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_label, uri_rdfs_label)=true)). % 31.69/21.28 tff(c_12956, plain, (icext(uri_rdf_Property, uri_rdfs_member)=true)). % 31.69/21.28 tff(c_12902, plain, (iext(uri_rdf_type, uri_rdfs_member, uri_rdf_Property)=true)). % 31.69/21.28 tff(c_12830, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Resource, uri_rdfs_Resource)=true)). % 31.69/21.28 tff(c_12761, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_member, uri_rdfs_member)=true)). % 31.69/21.28 tff(c_12620, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Statement, uri_rdfs_Resource)=true)). % 31.69/21.28 tff(c_12554, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Statement, uri_rdfs_Statement)=true)). % 31.69/21.28 tff(c_12413, plain, (iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdfs_Resource)=true)). % 31.69/21.28 tff(c_12346, plain, (iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdf_List)=true)). % 31.69/21.28 tff(c_12268, plain, (iext(uri_rdf_type, uri_rdf_Bag, uri_rdfs_Class)=true)). % 31.69/21.28 tff(c_12220, plain, (iext(uri_rdf_type, uri_rdfs_Datatype, uri_rdfs_Class)=true)). % 31.69/21.28 tff(c_12171, plain, (iext(uri_rdf_type, uri_ex_c, uri_rdfs_Class)=true)). % 31.69/21.28 tff(c_12122, plain, (iext(uri_rdf_type, uri_rdf_XMLLiteral, uri_rdfs_Class)=true)). % 31.69/21.28 tff(c_1918, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_isDefinedBy), true)=true))). % 31.69/21.28 tff(c_12049, plain, (iext(uri_rdf_type, uri_rdfs_Class, uri_rdfs_Class)=true)). % 31.69/21.28 tff(c_12000, plain, (iext(uri_rdf_type, uri_ex_c1, uri_rdfs_Class)=true)). % 31.69/21.28 tff(c_11951, plain, (iext(uri_rdf_type, uri_rdfs_Container, uri_rdfs_Class)=true)). % 31.69/21.28 tff(c_11904, plain, (iext(uri_rdf_type, uri_rdfs_Seq, uri_rdfs_Class)=true)). % 31.69/21.28 tff(c_11856, plain, (iext(uri_rdf_type, uri_rdfs_Literal, uri_rdfs_Class)=true)). % 31.69/21.28 tff(c_1942, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf__2), true)=true))). % 31.69/21.28 tff(c_11778, plain, (iext(uri_rdf_type, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Class)=true)). % 31.69/21.28 tff(c_11731, plain, (iext(uri_rdf_type, uri_rdf_Alt, uri_rdfs_Class)=true)). % 31.69/21.28 tff(c_1923, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_domain), true)=true))). % 31.69/21.28 tff(c_11659, plain, (ip(uri_rdfs_comment)=true)). % 31.69/21.28 tff(c_11602, plain, (iext(uri_rdf_type, uri_rdfs_comment, uri_rdf_Property)=true)). % 31.69/21.28 tff(c_11551, plain, (iext(uri_rdf_type, uri_rdf_List, uri_rdfs_Class)=true)). % 31.69/21.28 tff(c_11510, plain, (ip(uri_rdfs_label)=true)). % 31.69/21.28 tff(c_11456, plain, (iext(uri_rdf_type, uri_rdfs_label, uri_rdf_Property)=true)). % 31.69/21.28 tff(c_11409, plain, (iext(uri_rdf_type, uri_rdfs_Statement, uri_rdfs_Class)=true)). % 31.69/21.28 tff(c_11339, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_subject, uri_rdf_subject)=true)). % 31.69/21.28 tff(c_11273, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdf_Bag)=true)). % 31.69/21.28 tff(c_11207, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdfs_Class)=true)). % 31.69/21.28 tff(c_10989, plain, (ic(uri_rdfs_Statement)=true)). % 31.69/21.28 tff(c_10931, plain, (icext(uri_rdfs_Class, uri_rdfs_Statement)=true)). % 31.69/21.28 tff(c_2334, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdfs_Statement), true)=true))). % 31.69/21.28 tff(c_10845, plain, (iext(uri_rdfs_subClassOf, uri_ex_c1, uri_rdfs_Resource)=true)). % 31.69/21.28 tff(c_10777, plain, (iext(uri_rdfs_subClassOf, uri_ex_c, uri_ex_c)=true)). % 31.69/21.28 tff(c_10647, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Resource)=true)). % 31.69/21.28 tff(c_10582, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_range, uri_rdfs_range)=true)). % 31.69/21.28 tff(c_10516, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Datatype)=true)). % 31.69/21.28 tff(c_1962, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdf_rest), true)=true))). % 31.69/21.28 tff(c_10361, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Container, uri_rdfs_Resource)=true)). % 31.69/21.28 tff(c_10306, plain, (iext(uri_rdf_type, uri_rdfs_subClassOf, uri_rdf_Property)=true)). % 31.69/21.28 tff(c_1963, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf_first), true)=true))). % 31.69/21.28 tff(c_10214, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_object, uri_rdf_object)=true)). % 31.69/21.28 tff(c_945, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_domain, S_5, O_6), true, true, true)=true))). % 31.69/21.28 tff(c_10082, plain, (iext(uri_rdf_type, uri_rdfs_domain, uri_rdf_Property)=true)). % 31.69/21.28 tff(c_1920, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdf__2), true)=true))). % 31.69/21.28 tff(c_9916, plain, (icext(uri_rdf_Property, uri_rdfs_seeAlso)=true)). % 31.69/21.28 tff(c_9862, plain, (iext(uri_rdf_type, uri_rdfs_seeAlso, uri_rdf_Property)=true)). % 31.69/21.28 tff(c_1936, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdf__1), true)=true))). % 31.69/21.28 tff(c_9713, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdfs_Resource)=true)). % 31.69/21.28 tff(c_9648, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_first, uri_rdf_first)=true)). % 31.69/21.28 tff(c_9583, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, uri_rdfs_subClassOf)=true)). % 31.69/21.28 tff(c_9512, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__2, uri_rdfs_member)=true)). % 31.69/21.28 tff(c_9356, plain, (icext(uri_rdf_Property, uri_rdfs_label)=true)). % 31.69/21.28 tff(c_1913, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_label), true)=true))). % 31.69/21.28 tff(c_9271, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__3, uri_rdfs_member)=true)). % 31.69/21.28 tff(c_9204, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__2, uri_rdf__2)=true)). % 31.69/21.28 tff(c_1950, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_subClassOf), true)=true))). % 31.69/21.28 tff(c_9066, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Resource)=true)). % 31.69/21.28 tff(c_8932, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Resource)=true)). % 31.69/21.28 tff(c_8865, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdf_Property)=true)). % 31.69/21.28 tff(c_8757, plain, (icext(uri_rdf_Property, uri_owl_sameAs)=true)). % 31.69/21.28 tff(c_1947, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf_object), true)=true))). % 31.69/21.28 tff(c_8678, plain, (iext(uri_rdf_type, uri_owl_sameAs, uri_rdf_Property)=true)). % 31.69/21.28 tff(c_8612, plain, (iext(uri_rdfs_subClassOf, uri_ex_c1, uri_ex_c1)=true)). % 31.69/21.28 tff(c_2372, plain, (![S_5, O_6]: (ifeq(iext(uri_rdf_object, S_5, O_6), true, true, true)=true))). % 31.69/21.28 tff(c_8475, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Resource)=true)). % 31.69/21.28 tff(c_8409, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__3, uri_rdf__3)=true)). % 31.69/21.28 tff(c_8343, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, uri_rdfs_domain)=true)). % 31.69/21.28 tff(c_2355, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdf_Property), true)=true))). % 31.69/21.28 tff(c_8263, plain, (iext(uri_rdf_type, uri_rdfs_isDefinedBy, uri_rdf_Property)=true)). % 31.69/21.28 tff(c_8198, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__1, uri_rdf__1)=true)). % 31.69/21.28 tff(c_2309, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_97), true, icext(C_97, uri_rdfs_Resource), true)=true))). % 31.69/21.28 tff(c_8104, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_value, uri_rdf_value)=true)). % 31.69/21.28 tff(c_8021, plain, (ip(uri_rdfs_member)=true)). % 31.69/21.28 tff(c_7957, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__1, uri_rdfs_member)=true)). % 31.69/21.28 tff(c_3404, plain, (![S_5, O_6]: (ifeq(iext(uri_owl_sameAs, S_5, O_6), true, true, true)=true))). % 31.69/21.28 tff(c_7881, plain, (iext(uri_rdfs_subPropertyOf, uri_owl_sameAs, uri_owl_sameAs)=true)). % 31.69/21.28 tff(c_7775, plain, (icext(uri_rdf_Property, uri_rdfs_comment)=true)). % 31.69/21.28 tff(c_7689, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdf_XMLLiteral)=true)). % 31.69/21.28 tff(c_1959, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_comment), true)=true))). % 31.69/21.28 tff(c_7623, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, uri_rdfs_isDefinedBy)=true)). % 31.69/21.28 tff(c_7486, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Resource)=true)). % 31.69/21.28 tff(c_2332, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_97), true, icext(C_97, uri_rdfs_Class), true)=true))). % 31.69/21.28 tff(c_7420, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_type, uri_rdf_type)=true)). % 31.69/21.28 tff(c_2297, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_97), true, icext(C_97, uri_rdfs_ContainerMembershipProperty), true)=true))). % 31.69/21.28 tff(c_2487, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_subPropertyOf, S_5, O_6), true, true, true)=true))). % 31.69/21.28 tff(c_7269, plain, (icext(uri_rdf_Property, uri_rdfs_subPropertyOf)=true)). % 31.69/21.28 tff(c_7215, plain, (iext(uri_rdf_type, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 31.69/21.28 tff(c_2322, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdfs_Resource), true)=true))). % 31.69/21.28 tff(c_7092, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Seq)=true)). % 31.69/21.28 tff(c_1029, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_subClassOf, S_5, O_6), true, true, true)=true))). % 31.69/21.28 tff(c_1928, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf__3), true)=true))). % 31.69/21.28 tff(c_6885, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdfs_Literal)=true)). % 31.69/21.28 tff(c_6776, plain, (icext(uri_rdf_Property, uri_rdfs_domain)=true)). % 31.69/21.28 tff(c_6690, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdfs_Resource)=true)). % 31.69/21.28 tff(c_1945, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_domain), true)=true))). % 31.69/21.28 tff(c_1220, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_range, S_5, O_6), true, true, true)=true))). % 31.69/21.28 tff(c_6479, plain, (icext(uri_rdf_Property, uri_rdfs_range)=true)). % 31.69/21.28 tff(c_2340, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_97), true, icext(C_97, uri_rdfs_Container), true)=true))). % 31.69/21.28 tff(c_6422, plain, (iext(uri_rdf_type, uri_rdfs_range, uri_rdf_Property)=true)). % 31.69/21.28 tff(c_2318, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_97), true, icext(C_97, uri_rdf_Property), true)=true))). % 31.69/21.28 tff(c_6262, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Container, uri_rdfs_Container)=true)). % 31.69/21.28 tff(c_6207, plain, (icext(uri_rdf_Property, uri_rdfs_subClassOf)=true)). % 31.69/21.28 tff(c_1899, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_subClassOf), true)=true))). % 31.69/21.28 tff(c_6103, plain, (icext(uri_rdf_Property, uri_rdfs_isDefinedBy)=true)). % 31.69/21.28 tff(c_1922, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_93), true, icext(C_93, uri_rdfs_isDefinedBy), true)=true))). % 31.69/21.28 tff(c_6007, plain, (ic(uri_rdf_List)=true)). % 31.69/21.28 tff(c_5950, plain, (icext(uri_rdfs_Class, uri_rdf_List)=true)). % 31.69/21.28 tff(c_2325, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdf_List), true)=true))). % 31.69/21.28 tff(c_1600, plain, (![X_90]: (ifeq(icext(uri_ex_c, X_90), true, icext(uri_ex_c1, X_90), true)=true))). % 31.69/21.28 tff(c_5789, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Resource)=true)). % 31.69/21.28 tff(c_1599, plain, (![X_90]: (ifeq(icext(uri_rdfs_Datatype, X_90), true, icext(uri_rdfs_Class, X_90), true)=true))). % 31.69/21.28 tff(c_5652, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_rest, uri_rdf_rest)=true)). % 31.69/21.28 tff(c_1596, plain, (![X_90]: (ifeq(icext(uri_rdfs_ContainerMembershipProperty, X_90), true, icext(uri_rdf_Property, X_90), true)=true))). % 31.69/21.28 tff(c_5531, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_seeAlso, uri_rdfs_seeAlso)=true)). % 31.69/21.28 tff(c_5350, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf)=true)). % 31.69/21.28 tff(c_1595, plain, (![X_90]: (ifeq(icext(uri_rdf_XMLLiteral, X_90), true, icext(uri_rdfs_Literal, X_90), true)=true))). % 31.69/21.28 tff(c_5288, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdf_Alt)=true)). % 31.69/21.28 tff(c_5211, plain, (iext(uri_rdfs_subClassOf, uri_ex_c, uri_rdfs_Resource)=true)). % 31.69/21.28 tff(c_1594, plain, (![X_90]: (ifeq(icext(uri_rdfs_Seq, X_90), true, icext(uri_rdfs_Container, X_90), true)=true))). % 31.69/21.28 tff(c_5134, plain, (icext(uri_rdfs_Class, uri_rdfs_Resource)=true)). % 31.69/21.28 tff(c_5055, plain, (ic(uri_rdfs_Resource)=true)). % 31.69/21.28 tff(c_1598, plain, (![X_90]: (ifeq(icext(uri_rdf_Bag, X_90), true, icext(uri_rdfs_Container, X_90), true)=true))). % 31.69/21.28 tff(c_4983, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdfs_Resource)=true)). % 31.69/21.28 tff(c_4898, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdfs_ContainerMembershipProperty)=true)). % 31.69/21.28 tff(c_828, plain, (![S_5, O_6]: (ifeq(iext(uri_rdf_rest, S_5, O_6), true, true, true)=true))). % 31.69/21.28 tff(c_1597, plain, (![X_90]: (ifeq(icext(uri_rdf_Alt, X_90), true, icext(uri_rdfs_Container, X_90), true)=true))). % 31.69/21.28 tff(c_4782, plain, (![X_138]: (iext(uri_rdf_type, X_138, uri_rdfs_Resource)=true))). % 31.69/21.28 tff(c_1953, plain, (![X_94, Y_95]: (ifeq(iext(uri_rdf_type, X_94, Y_95), true, true, true)=true))). % 31.69/21.28 tff(c_1912, plain, (![X_94, Y_95]: (ifeq(iext(uri_rdfs_label, X_94, Y_95), true, true, true)=true))). % 31.69/21.28 tff(c_1932, plain, (![X_94, Y_95]: (ifeq(iext(uri_rdfs_isDefinedBy, X_94, Y_95), true, true, true)=true))). % 31.69/21.28 tff(c_2352, plain, (![X_98, Y_99]: (ifeq(iext(uri_rdf_first, X_98, Y_99), true, true, true)=true))). % 31.69/21.28 tff(c_2291, plain, (![X_98, Y_99]: (ifeq(iext(uri_rdf_subject, X_98, Y_99), true, true, true)=true))). % 31.69/21.28 tff(c_1941, plain, (![X_94, Y_95]: (ifeq(iext(uri_rdf__2, X_94, Y_95), true, true, true)=true))). % 31.69/21.28 tff(c_1938, plain, (![X_94, Y_95]: (ifeq(iext(uri_rdfs_comment, X_94, Y_95), true, true, true)=true))). % 31.69/21.28 tff(c_1905, plain, (![X_94, Y_95]: (ifeq(iext(uri_rdfs_seeAlso, X_94, Y_95), true, true, true)=true))). % 31.69/21.28 tff(c_4603, plain, (icext(uri_rdfs_Class, uri_rdfs_Container)=true)). % 31.69/21.28 tff(c_1927, plain, (![X_94, Y_95]: (ifeq(iext(uri_rdf__3, X_94, Y_95), true, true, true)=true))). % 31.69/21.28 tff(c_4550, plain, (icext(uri_rdfs_Class, uri_rdfs_Datatype)=true)). % 31.69/21.28 tff(c_4505, plain, (icext(uri_rdfs_Class, uri_ex_c1)=true)). % 31.69/21.28 tff(c_4453, plain, (icext(uri_rdfs_Class, uri_rdfs_Seq)=true)). % 31.69/21.28 tff(c_2330, plain, (![X_98, Y_99]: (ifeq(iext(uri_rdfs_member, X_98, Y_99), true, true, true)=true))). % 31.69/21.28 tff(c_4404, plain, (icext(uri_rdfs_Class, uri_rdfs_Literal)=true)). % 31.69/21.28 tff(c_2288, plain, (![X_98, Y_99]: (ifeq(iext(uri_rdf_value, X_98, Y_99), true, true, true)=true))). % 31.69/21.28 tff(c_4344, plain, (icext(uri_rdfs_Class, uri_ex_c)=true)). % 31.69/21.28 tff(c_4293, plain, (icext(uri_rdfs_Class, uri_rdfs_ContainerMembershipProperty)=true)). % 31.69/21.28 tff(c_1951, plain, (![X_94, Y_95]: (ifeq(iext(uri_rdf__1, X_94, Y_95), true, true, true)=true))). % 31.69/21.28 tff(c_4243, plain, (icext(uri_rdfs_Class, uri_rdfs_Class)=true)). % 31.69/21.29 tff(c_4196, plain, (icext(uri_rdfs_Class, uri_rdf_Bag)=true)). % 31.69/21.29 tff(c_4146, plain, (icext(uri_rdfs_Class, uri_rdf_XMLLiteral)=true)). % 31.69/21.29 tff(c_2313, plain, (![X_98, Y_99]: (ifeq(iext(uri_rdf_predicate, X_98, Y_99), true, true, true)=true))). % 31.69/21.29 tff(c_4103, plain, (icext(uri_rdfs_Class, uri_rdf_Alt)=true)). % 31.69/21.29 tff(c_4062, plain, (icext(uri_rdf_Property, uri_rdf_value)=true)). % 31.69/21.29 tff(c_4022, plain, (icext(uri_rdf_Property, uri_rdf__1)=true)). % 31.69/21.29 tff(c_3976, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__3)=true)). % 31.69/21.29 tff(c_3935, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__1)=true)). % 31.69/21.29 tff(c_3898, plain, (icext(uri_rdf_Property, uri_rdf__2)=true)). % 31.69/21.29 tff(c_3824, plain, (icext(uri_rdf_Property, uri_rdf__3)=true)). % 31.69/21.29 tff(c_3814, plain, (icext(uri_rdfs_Class, uri_rdf_Property)=true)). % 31.69/21.29 tff(c_3775, plain, (icext(uri_rdf_Property, uri_rdf_object)=true)). % 31.69/21.29 tff(c_3726, plain, (icext(uri_rdfs_Datatype, uri_rdf_XMLLiteral)=true)). % 31.69/21.29 tff(c_3690, plain, (icext(uri_ex_c1, uri_ex_w)=true)). % 31.69/21.29 tff(c_3645, plain, (icext(uri_rdf_Property, uri_rdf_rest)=true)). % 31.69/21.29 tff(c_3608, plain, (icext(uri_rdf_Property, uri_rdf_type)=true)). % 31.69/21.29 tff(c_3569, plain, (icext(uri_rdf_Property, uri_rdf_first)=true)). % 31.69/21.29 tff(c_3496, plain, (icext(uri_rdf_List, uri_rdf_nil)=true)). % 31.69/21.29 tff(c_3486, plain, (icext(uri_rdf_Property, uri_rdf_subject)=true)). % 31.69/21.29 tff(c_3434, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__2)=true)). % 31.69/21.29 tff(c_3383, plain, (ip(uri_owl_sameAs)=true)). % 31.69/21.29 tff(c_3344, plain, (ip(uri_rdf__1)=true)). % 31.69/21.29 tff(c_3301, plain, (ip(uri_rdf_value)=true)). % 31.69/21.29 tff(c_3266, plain, (ic(uri_rdfs_Class)=true)). % 31.69/21.29 tff(c_3221, plain, (ic(uri_rdfs_Literal)=true)). % 31.69/21.29 tff(c_3180, plain, (ip(uri_rdf__3)=true)). % 31.69/21.29 tff(c_3135, plain, (ic(uri_ex_c)=true)). % 31.69/21.29 tff(c_3094, plain, (ip(uri_rdfs_isDefinedBy)=true)). % 31.69/21.29 tff(c_3054, plain, (ic(uri_rdfs_Datatype)=true)). % 31.69/21.29 tff(c_3017, plain, (ic(uri_rdf_Alt)=true)). % 31.69/21.29 tff(c_172, plain, (![Q_52, R_53, P_54]: (ifeq(iext(uri_rdfs_subPropertyOf, Q_52, R_53), true, ifeq(iext(uri_rdfs_subPropertyOf, P_54, Q_52), true, iext(uri_rdfs_subPropertyOf, P_54, R_53), true), true)=true))). % 31.69/21.29 tff(c_166, plain, (![P_47, Q_48, X_49, Y_50]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, Q_48), true, ifeq(iext(P_47, X_49, Y_50), true, iext(Q_48, X_49, Y_50), true), true)=true))). % 31.69/21.29 tff(c_2501, plain, (ic(uri_rdfs_Seq)=true)). % 31.69/21.29 tff(c_2466, plain, (ip(uri_rdfs_subPropertyOf)=true)). % 31.69/21.29 tff(c_158, plain, (![D_40, E_41, C_42]: (ifeq(iext(uri_rdfs_subClassOf, D_40, E_41), true, ifeq(iext(uri_rdfs_subClassOf, C_42, D_40), true, iext(uri_rdfs_subClassOf, C_42, E_41), true), true)=true))). % 31.69/21.29 tff(c_2018, plain, (ip(uri_rdf_object)=true)). % 31.69/21.29 tff(c_130, plain, (![P_28, C_29, X_30, Y_31]: (ifeq(iext(uri_rdfs_range, P_28, C_29), true, ifeq(iext(P_28, X_30, Y_31), true, icext(C_29, Y_31), true), true)=true))). % 31.69/21.29 tff(c_1979, plain, (ip(uri_rdf__2)=true)). % 31.69/21.29 tff(c_110, plain, (![P_18, C_19, X_20, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, C_19), true, ifeq(iext(P_18, X_20, Y_21), true, icext(C_19, X_20), true), true)=true))). % 31.69/21.29 tff(c_1604, plain, (ip(uri_rdf_subject)=true)). % 31.69/21.29 tff(c_148, plain, (![C_32, X_33, D_34]: (ifeq(icext(C_32, X_33), true, ifeq(iext(uri_rdfs_subClassOf, C_32, D_34), true, icext(D_34, X_33), true), true)=true))). % 31.69/21.29 tff(c_190, plain, (tuple(iext(uri_rdfs_subClassOf, uri_ex_c, uri_ex_c2), iext(uri_rdf_type, uri_ex_w, uri_ex_c2), iext(uri_rdfs_range, uri_ex_p, uri_ex_c2))!=tuple(true, true, true))). % 31.69/21.29 tff(c_1520, plain, (ic(uri_rdf_Property)=true)). % 31.69/21.29 tff(c_104, plain, (![D_17]: (ifeq(icext(uri_rdfs_Datatype, D_17), true, iext(uri_rdfs_subClassOf, D_17, uri_rdfs_Literal), true)=true))). % 31.69/21.29 tff(c_1473, plain, (ic(uri_rdfs_Container)=true)). % 31.69/21.29 tff(c_54, plain, (![C_11, X_12]: (ifeq(icext(C_11, X_12), true, iext(uri_rdf_type, X_12, C_11), true)=true))). % 31.69/21.29 tff(c_72, plain, (![P_16]: (ifeq(icext(uri_rdfs_ContainerMembershipProperty, P_16), true, iext(uri_rdfs_subPropertyOf, P_16, uri_rdfs_member), true)=true))). % 31.69/21.29 tff(c_1370, plain, (ic(uri_rdfs_ContainerMembershipProperty)=true)). % 31.69/21.29 tff(c_56, plain, (![X_13, C_14]: (ifeq(iext(uri_rdf_type, X_13, C_14), true, icext(C_14, X_13), true)=true))). % 31.69/21.29 tff(c_1276, plain, (ic(uri_ex_c1)=true)). % 31.69/21.29 tff(c_150, plain, (![C_35, D_36]: (ifeq(iext(uri_rdfs_subClassOf, C_35, D_36), true, ic(D_36), true)=true))). % 31.69/21.29 tff(c_1199, plain, (ip(uri_rdfs_range)=true)). % 31.69/21.29 tff(c_164, plain, (![P_45, Q_46]: (ifeq(iext(uri_rdfs_subPropertyOf, P_45, Q_46), true, ip(P_45), true)=true))). % 31.69/21.29 tff(c_1118, plain, (ic(uri_rdf_Bag)=true)). % 31.69/21.29 tff(c_156, plain, (![C_39]: (ifeq(ic(C_39), true, iext(uri_rdfs_subClassOf, C_39, C_39), true)=true))). % 31.69/21.29 tff(c_1070, plain, (ic(uri_rdf_XMLLiteral)=true)). % 31.69/21.29 tff(c_170, plain, (![P_51]: (ifeq(ip(P_51), true, iext(uri_rdfs_subPropertyOf, P_51, P_51), true)=true))). % 31.69/21.29 tff(c_1014, plain, (ip(uri_rdfs_subClassOf)=true)). % 31.69/21.29 tff(c_28, plain, (![P_9]: (ifeq(ip(P_9), true, iext(uri_rdf_type, P_9, uri_rdf_Property), true)=true))). % 31.69/21.29 tff(c_933, plain, (ip(uri_rdfs_domain)=true)). % 31.69/21.29 tff(c_58, plain, (![C_15]: (ifeq(ic(C_15), true, iext(uri_rdfs_subClassOf, C_15, uri_rdfs_Resource), true)=true))). % 31.69/21.29 tff(c_898, plain, (ip(uri_rdf_first)=true)). % 31.69/21.29 tff(c_152, plain, (![C_37, D_38]: (ifeq(iext(uri_rdfs_subClassOf, C_37, D_38), true, ic(C_37), true)=true))). % 31.69/21.29 tff(c_843, plain, (ip(uri_rdf_type)=true)). % 31.69/21.29 tff(c_816, plain, (ip(uri_rdf_rest)=true)). % 31.69/21.29 tff(c_4, plain, (![P_4, S_5, O_6]: (ifeq(iext(P_4, S_5, O_6), true, ip(P_4), true)=true))). % 31.69/21.29 tff(c_578, plain, (ip(uri_rdfs_seeAlso)=true)). % 31.69/21.29 tff(c_30, plain, (![P_10]: (ifeq(iext(uri_rdf_type, P_10, uri_rdf_Property), true, ip(P_10), true)=true))). % 31.69/21.29 tff(c_162, plain, (![P_43, Q_44]: (ifeq(iext(uri_rdfs_subPropertyOf, P_43, Q_44), true, ip(Q_44), true)=true))). % 31.69/21.29 tff(c_124, plain, (![X_27]: (ifeq(lv(X_27), true, icext(uri_rdfs_Literal, X_27), true)=true))). % 31.69/21.29 tff(c_114, plain, (![X_22]: (ifeq(ic(X_22), true, icext(uri_rdfs_Class, X_22), true)=true))). % 31.69/21.29 tff(c_116, plain, (![X_23]: (ifeq(icext(uri_rdfs_Class, X_23), true, ic(X_23), true)=true))). % 31.69/21.29 tff(c_122, plain, (![X_26]: (ifeq(icext(uri_rdfs_Literal, X_26), true, lv(X_26), true)=true))). % 31.69/21.29 tff(c_483, plain, (![X_61]: (icext(uri_rdfs_Resource, X_61)=true))). % 31.69/21.29 tff(c_195, plain, (![X_8]: (ifeq(lv(X_8), true, true, true)=true))). % 31.69/21.29 tff(c_2, plain, (![A_1, B_2, C_3]: (ifeq(A_1, A_1, B_2, C_3)=B_2))). % 31.69/21.29 tff(c_154, plain, (iext(uri_rdfs_range, uri_rdfs_subClassOf, uri_rdfs_Class)=true)). % 31.69/21.29 tff(c_26, plain, (iext(uri_rdf_type, uri_rdf_subject, uri_rdf_Property)=true)). % 31.69/21.29 tff(c_14, plain, (iext(uri_rdf_type, uri_rdf_rest, uri_rdf_Property)=true)). % 31.69/21.29 tff(c_180, plain, (iext(uri_rdfs_range, uri_rdf_value, uri_rdfs_Resource)=true)). % 31.69/21.29 tff(c_94, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdfs_ContainerMembershipProperty)=true)). % 31.69/21.29 tff(c_144, plain, (iext(uri_rdfs_range, uri_rdf_subject, uri_rdfs_Resource)=true)). % 31.69/21.29 tff(c_50, plain, (iext(uri_rdfs_domain, uri_rdfs_seeAlso, uri_rdfs_Resource)=true)). % 31.69/21.29 tff(c_98, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Container)=true)). % 31.69/21.29 tff(c_186, plain, (iext(uri_rdf_type, uri_ex_w, uri_ex_c1)=true)). % 31.69/21.29 tff(c_96, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdfs_ContainerMembershipProperty)=true)). % 31.69/21.29 tff(c_92, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdfs_ContainerMembershipProperty)=true)). % 31.69/21.29 tff(c_90, plain, (iext(uri_rdfs_range, uri_rdf__3, uri_rdfs_Resource)=true)). % 31.69/21.29 tff(c_46, plain, (iext(uri_rdfs_domain, uri_rdfs_label, uri_rdfs_Resource)=true)). % 31.69/21.29 tff(c_168, plain, (iext(uri_rdfs_range, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 31.69/21.29 tff(c_48, plain, (iext(uri_rdfs_range, uri_rdfs_label, uri_rdfs_Literal)=true)). % 31.69/21.29 tff(c_22, plain, (iext(uri_rdf_type, uri_rdf_object, uri_rdf_Property)=true)). % 31.69/21.29 tff(c_18, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdf_Property)=true)). % 31.69/21.29 tff(c_42, plain, (iext(uri_rdfs_range, uri_rdfs_isDefinedBy, uri_rdfs_Resource)=true)). % 31.69/21.29 tff(c_24, plain, (iext(uri_rdf_type, uri_rdf_value, uri_rdf_Property)=true)). % 31.69/21.29 tff(c_88, plain, (iext(uri_rdfs_range, uri_rdf__2, uri_rdfs_Resource)=true)). % 31.69/21.29 tff(c_100, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Literal)=true)). % 31.69/21.29 tff(c_44, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso)=true)). % 31.69/21.29 tff(c_108, plain, (iext(uri_rdfs_domain, uri_rdfs_domain, uri_rdf_Property)=true)). % 31.69/21.29 tff(c_140, plain, (iext(uri_rdfs_range, uri_rdf_predicate, uri_rdfs_Resource)=true)). % 31.69/21.29 tff(c_142, plain, (iext(uri_rdfs_domain, uri_rdf_subject, uri_rdfs_Statement)=true)). % 31.69/21.29 tff(c_34, plain, (iext(uri_rdf_type, uri_rdf_type, uri_rdf_Property)=true)). % 31.69/21.29 tff(c_84, plain, (iext(uri_rdfs_domain, uri_rdf__3, uri_rdfs_Resource)=true)). % 31.69/21.29 tff(c_20, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdf_Property)=true)). % 31.69/21.29 tff(c_138, plain, (iext(uri_rdfs_domain, uri_rdf_predicate, uri_rdfs_Statement)=true)). % 31.69/21.29 tff(c_102, plain, (iext(uri_rdf_type, uri_rdf_XMLLiteral, uri_rdfs_Datatype)=true)). % 31.69/21.29 tff(c_40, plain, (iext(uri_rdfs_domain, uri_rdfs_isDefinedBy, uri_rdfs_Resource)=true)). % 31.69/21.29 tff(c_76, plain, (iext(uri_rdfs_domain, uri_rdfs_member, uri_rdfs_Resource)=true)). % 31.69/21.29 tff(c_86, plain, (iext(uri_rdfs_range, uri_rdf__1, uri_rdfs_Resource)=true)). % 31.69/21.29 tff(c_64, plain, (iext(uri_rdfs_domain, uri_rdf_rest, uri_rdf_List)=true)). % 31.69/21.29 tff(c_36, plain, (iext(uri_rdfs_domain, uri_rdfs_comment, uri_rdfs_Resource)=true)). % 31.69/21.29 tff(c_184, plain, (iext(uri_rdfs_range, uri_ex_p, uri_ex_c1)=true)). % 31.69/21.29 tff(c_82, plain, (iext(uri_rdfs_domain, uri_rdf__2, uri_rdfs_Resource)=true)). % 31.69/21.29 tff(c_16, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdf_Property)=true)). % 31.69/21.29 tff(c_78, plain, (iext(uri_rdfs_range, uri_rdfs_member, uri_rdfs_Resource)=true)). % 31.69/21.29 tff(c_112, plain, (iext(uri_rdfs_range, uri_rdfs_domain, uri_rdfs_Class)=true)). % 31.69/21.29 tff(c_182, plain, (iext(uri_owl_sameAs, uri_ex_c1, uri_ex_c2)=true)). % 31.69/21.29 tff(c_134, plain, (iext(uri_rdfs_domain, uri_rdf_object, uri_rdfs_Statement)=true)). % 31.69/21.29 tff(c_74, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property)=true)). % 31.69/21.29 tff(c_68, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Container)=true)). % 31.69/21.29 tff(c_146, plain, (iext(uri_rdfs_domain, uri_rdfs_subClassOf, uri_rdfs_Class)=true)). % 31.69/21.29 tff(c_80, plain, (iext(uri_rdfs_domain, uri_rdf__1, uri_rdfs_Resource)=true)). % 31.69/21.29 tff(c_174, plain, (iext(uri_rdfs_domain, uri_rdf_type, uri_rdfs_Resource)=true)). % 31.69/21.29 tff(c_70, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Container)=true)). % 31.69/21.29 tff(c_132, plain, (iext(uri_rdfs_range, uri_rdfs_range, uri_rdfs_Class)=true)). % 31.69/21.29 tff(c_178, plain, (iext(uri_rdfs_domain, uri_rdf_value, uri_rdfs_Resource)=true)). % 31.69/21.29 tff(c_38, plain, (iext(uri_rdfs_range, uri_rdfs_comment, uri_rdfs_Literal)=true)). % 31.69/21.29 tff(c_52, plain, (iext(uri_rdfs_range, uri_rdfs_seeAlso, uri_rdfs_Resource)=true)). % 31.69/21.29 tff(c_106, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Class)=true)). % 31.69/21.29 tff(c_66, plain, (iext(uri_rdfs_range, uri_rdf_rest, uri_rdf_List)=true)). % 31.69/21.29 tff(c_60, plain, (iext(uri_rdfs_domain, uri_rdf_first, uri_rdf_List)=true)). % 31.69/21.29 tff(c_10, plain, (iext(uri_rdf_type, uri_rdf_first, uri_rdf_Property)=true)). % 31.69/21.29 tff(c_12, plain, (iext(uri_rdf_type, uri_rdf_nil, uri_rdf_List)=true)). % 31.69/21.29 tff(c_128, plain, (iext(uri_rdfs_domain, uri_rdfs_range, uri_rdf_Property)=true)). % 31.69/21.29 tff(c_62, plain, (iext(uri_rdfs_range, uri_rdf_first, uri_rdfs_Resource)=true)). % 31.69/21.29 tff(c_126, plain, (iext(uri_rdf_type, uri_rdf_Property, uri_rdfs_Class)=true)). % 31.69/21.29 tff(c_160, plain, (iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 31.69/21.29 tff(c_176, plain, (iext(uri_rdfs_range, uri_rdf_type, uri_rdfs_Class)=true)). % 31.69/21.29 tff(c_188, plain, (iext(uri_rdfs_subClassOf, uri_ex_c, uri_ex_c1)=true)). % 31.69/21.29 tff(c_6, plain, (![X_7]: (ir(X_7)=true))). % 31.69/21.29 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 31.69/21.29 %------------------------------------------------------------------------------