%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SWB015-10 : TPTP v9.0.0. Released v7.3.0. % Transfm : none % Format : tptp:raw % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n020.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:50 PM UTC 2025 % Result : Satisfiable 28.66s 17.96s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.02/0.12 % Problem : SWB015-10 : TPTP v9.0.0. Released v7.3.0. % 0.02/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.13/0.34 % Computer : n020.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:57:04 EDT 2025 % 0.13/0.34 % CPUTime : % 28.66/17.96 % 28.66/17.96 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 28.66/17.96 % 28.66/17.96 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 28.66/17.98 %$ ifeq > 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 > true % 28.66/17.98 % 28.66/17.98 %Foreground sorts: % 28.66/17.98 % 28.66/17.98 % 28.66/17.98 %Background operators: % 28.66/17.98 % 28.66/17.98 % 28.66/17.98 %Foreground operators: % 28.66/17.98 tff(uri_rdfs_Datatype, type, uri_rdfs_Datatype: $i). % 28.66/17.98 tff(uri_rdfs_ContainerMembershipProperty, type, uri_rdfs_ContainerMembershipProperty: $i). % 28.66/17.98 tff(uri_rdfs_Resource, type, uri_rdfs_Resource: $i). % 28.66/17.98 tff(uri_rdf_Property, type, uri_rdf_Property: $i). % 28.66/17.98 tff(uri_rdf_subject, type, uri_rdf_subject: $i). % 28.66/17.98 tff(uri_rdf_type, type, uri_rdf_type: $i). % 28.66/17.98 tff(uri_rdfs_subPropertyOf, type, uri_rdfs_subPropertyOf: $i). % 28.66/17.98 tff(uri_rdfs_seeAlso, type, uri_rdfs_seeAlso: $i). % 28.66/17.98 tff(icext, type, icext: ($i * $i) > $i). % 28.66/17.98 tff(uri_rdfs_range, type, uri_rdfs_range: $i). % 28.66/17.98 tff(uri_rdf_XMLLiteral, type, uri_rdf_XMLLiteral: $i). % 28.66/17.98 tff(uri_rdf_List, type, uri_rdf_List: $i). % 28.66/17.98 tff(uri_rdf_first, type, uri_rdf_first: $i). % 28.66/17.98 tff(uri_rdf_predicate, type, uri_rdf_predicate: $i). % 28.66/17.98 tff(ir, type, ir: $i > $i). % 28.66/17.98 tff(lv, type, lv: $i > $i). % 28.66/17.98 tff(uri_rdf__3, type, uri_rdf__3: $i). % 28.66/17.98 tff(uri_rdf_value, type, uri_rdf_value: $i). % 28.66/17.98 tff(ic, type, ic: $i > $i). % 28.66/17.98 tff(uri_rdfs_Statement, type, uri_rdfs_Statement: $i). % 28.66/17.98 tff(uri_rdf__1, type, uri_rdf__1: $i). % 28.66/17.98 tff(iext, type, iext: ($i * $i * $i) > $i). % 28.66/17.98 tff(uri_rdf_rest, type, uri_rdf_rest: $i). % 28.66/17.98 tff(uri_rdfs_label, type, uri_rdfs_label: $i). % 28.66/17.98 tff(uri_rdfs_Container, type, uri_rdfs_Container: $i). % 28.66/17.98 tff(uri_rdfs_subClassOf, type, uri_rdfs_subClassOf: $i). % 28.66/17.98 tff(uri_owl_sameAs, type, uri_owl_sameAs: $i). % 28.66/17.98 tff(uri_rdf_object, type, uri_rdf_object: $i). % 28.66/17.98 tff(ip, type, ip: $i > $i). % 28.66/17.98 tff(uri_rdfs_Class, type, uri_rdfs_Class: $i). % 28.66/17.98 tff(uri_rdfs_Seq, type, uri_rdfs_Seq: $i). % 28.66/17.98 tff(uri_rdfs_member, type, uri_rdfs_member: $i). % 28.66/17.98 tff(uri_rdf_Bag, type, uri_rdf_Bag: $i). % 28.66/17.98 tff(uri_rdf__2, type, uri_rdf__2: $i). % 28.66/17.98 tff(uri_rdfs_comment, type, uri_rdfs_comment: $i). % 28.66/17.98 tff(uri_rdfs_Literal, type, uri_rdfs_Literal: $i). % 28.66/17.98 tff(true, type, true: $i). % 28.66/17.98 tff(uri_rdf_Alt, type, uri_rdf_Alt: $i). % 28.66/17.98 tff(uri_rdf_nil, type, uri_rdf_nil: $i). % 28.66/17.98 tff(uri_rdfs_isDefinedBy, type, uri_rdfs_isDefinedBy: $i). % 28.66/17.98 tff(uri_rdfs_domain, type, uri_rdfs_domain: $i). % 28.66/17.98 tff(ifeq, type, ifeq: ($i * $i * $i * $i) > $i). % 28.66/17.98 % 28.66/17.98 %Saturated clause set: % 28.66/17.98 tff(c_11631, 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))). % 28.66/17.98 tff(c_11628, 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))). % 28.66/17.98 tff(c_11801, 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))). % 28.66/17.98 tff(c_13586, 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))). % 28.66/17.98 tff(c_13014, 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))). % 28.66/17.98 tff(c_61634, plain, (![X_1130, Y_1131]: (ifeq(iext(uri_rdfs_comment, X_1130, Y_1131), true, iext(uri_rdfs_comment, X_1130, Y_1131), true)=true))). % 28.66/17.98 tff(c_61496, plain, (![X_1125, Y_1126]: (ifeq(iext(uri_rdfs_label, X_1125, Y_1126), true, iext(uri_rdfs_label, X_1125, Y_1126), true)=true))). % 28.66/17.98 tff(c_14185, 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))). % 28.66/17.98 tff(c_61469, plain, (![X_1121, Y_1122]: (ifeq(iext(uri_rdf_predicate, X_1121, Y_1122), true, iext(uri_rdf_predicate, X_1121, Y_1122), true)=true))). % 28.66/17.98 tff(c_61440, plain, (![X_1117, Y_1118]: (ifeq(iext(uri_rdfs_member, X_1117, Y_1118), true, iext(uri_rdfs_member, X_1117, Y_1118), true)=true))). % 28.66/17.98 tff(c_11476, 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))). % 28.66/17.98 tff(c_11409, 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))). % 28.66/17.98 tff(c_4694, 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))). % 28.66/17.98 tff(c_4691, 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))). % 28.66/17.98 tff(c_11574, 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))). % 28.66/17.98 tff(c_60591, plain, (![C_1108]: (ifeq(iext(uri_rdfs_subClassOf, C_1108, uri_rdfs_Statement), true, iext(uri_rdfs_subClassOf, C_1108, uri_rdfs_Resource), true)=true))). % 28.66/17.98 tff(c_11223, 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))). % 28.66/17.98 tff(c_11289, 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))). % 28.66/17.98 tff(c_12807, 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))). % 28.66/17.98 tff(c_12920, 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))). % 28.66/17.98 tff(c_60000, plain, (![C_1102]: (ifeq(iext(uri_rdfs_subClassOf, C_1102, uri_rdf_List), true, iext(uri_rdfs_subClassOf, C_1102, uri_rdfs_Resource), true)=true))). % 28.66/17.98 tff(c_10340, 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))). % 28.66/17.98 tff(c_4905, 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))). % 28.66/17.98 tff(c_10930, 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))). % 28.66/17.98 tff(c_10737, 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))). % 28.66/17.98 tff(c_10882, 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))). % 28.66/17.98 tff(c_4902, 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))). % 28.66/17.98 tff(c_8213, 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))). % 28.66/17.98 tff(c_10343, 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))). % 28.66/17.98 tff(c_11147, 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))). % 28.66/17.98 tff(c_7796, 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))). % 28.66/17.98 tff(c_7214, 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))). % 28.66/17.98 tff(c_11053, 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))). % 28.66/17.98 tff(c_10977, 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))). % 28.66/17.98 tff(c_10786, 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))). % 28.66/17.99 tff(c_7211, 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))). % 28.66/17.99 tff(c_7799, 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))). % 28.66/17.99 tff(c_11100, 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))). % 28.66/17.99 tff(c_10834, 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))). % 28.66/17.99 tff(c_8210, 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))). % 28.66/17.99 tff(c_10654, 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))). % 28.66/17.99 tff(c_12487, 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))). % 28.66/17.99 tff(c_13378, 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))). % 28.66/17.99 tff(c_12610, 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))). % 28.66/17.99 tff(c_14063, 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))). % 28.66/17.99 tff(c_4022, 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))). % 28.66/17.99 tff(c_56466, plain, (![X_1062, Y_1063]: (ifeq(iext(uri_rdfs_subClassOf, X_1062, Y_1063), true, iext(uri_rdfs_subClassOf, X_1062, Y_1063), true)=true))). % 28.66/17.99 tff(c_56439, plain, (![X_1058, Y_1059]: (ifeq(iext(uri_rdf__2, X_1058, Y_1059), true, iext(uri_rdfs_member, X_1058, Y_1059), true)=true))). % 28.66/17.99 tff(c_9467, 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))). % 28.66/17.99 tff(c_6246, 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))). % 28.66/17.99 tff(c_9755, 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))). % 28.66/17.99 tff(c_55836, plain, (![P_1051]: (ifeq(iext(uri_rdfs_subPropertyOf, P_1051, uri_rdf__2), true, iext(uri_rdfs_subPropertyOf, P_1051, uri_rdfs_member), true)=true))). % 28.66/17.99 tff(c_55697, plain, (![C_1049]: (ifeq(iext(uri_rdfs_subClassOf, C_1049, uri_rdfs_Seq), true, iext(uri_rdfs_subClassOf, C_1049, uri_rdfs_Resource), true)=true))). % 28.66/17.99 tff(c_9242, 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))). % 28.66/17.99 tff(c_6623, 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))). % 28.66/17.99 tff(c_8834, 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))). % 28.66/17.99 tff(c_55333, plain, (![X_1042, Y_1043]: (ifeq(iext(uri_rdf_value, X_1042, Y_1043), true, iext(uri_rdf_value, X_1042, Y_1043), true)=true))). % 28.66/17.99 tff(c_55306, plain, (![X_1038, Y_1039]: (ifeq(iext(uri_rdf_subject, X_1038, Y_1039), true, iext(uri_rdf_subject, X_1038, Y_1039), true)=true))). % 28.66/17.99 tff(c_4119, 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))). % 28.66/17.99 tff(c_8156, 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))). % 28.66/17.99 tff(c_6138, 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))). % 28.66/17.99 tff(c_3881, 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))). % 28.66/17.99 tff(c_5838, 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))). % 28.66/17.99 tff(c_4263, 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))). % 28.66/17.99 tff(c_10196, 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))). % 28.66/17.99 tff(c_9892, 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))). % 28.66/17.99 tff(c_53738, plain, (![X_1023, Y_1024]: (ifeq(iext(uri_rdf_type, X_1023, Y_1024), true, iext(uri_rdf_type, X_1023, Y_1024), true)=true))). % 28.66/17.99 tff(c_10258, 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))). % 28.66/17.99 tff(c_7937, 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))). % 28.66/17.99 tff(c_53378, plain, (![C_1019]: (ifeq(iext(uri_rdfs_subClassOf, C_1019, uri_rdfs_Datatype), true, iext(uri_rdfs_subClassOf, C_1019, uri_rdfs_Resource), true)=true))). % 28.66/17.99 tff(c_10102, 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))). % 28.66/17.99 tff(c_4116, 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))). % 28.66/17.99 tff(c_6543, 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))). % 28.66/17.99 tff(c_4172, 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))). % 28.66/17.99 tff(c_52541, plain, (![C_1009]: (ifeq(iext(uri_rdfs_subClassOf, C_1009, uri_rdfs_Class), true, iext(uri_rdfs_subClassOf, C_1009, uri_rdfs_Resource), true)=true))). % 28.66/17.99 tff(c_52514, plain, (![X_1005, Y_1006]: (ifeq(iext(uri_rdf_first, X_1005, Y_1006), true, iext(uri_rdf_first, X_1005, Y_1006), true)=true))). % 28.66/17.99 tff(c_3878, 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))). % 28.66/17.99 tff(c_51795, plain, (![X_999, Y_1000]: (ifeq(iext(uri_rdfs_subPropertyOf, X_999, Y_1000), true, iext(uri_rdfs_subPropertyOf, X_999, Y_1000), true)=true))). % 28.66/17.99 tff(c_3935, 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))). % 28.66/17.99 tff(c_6715, 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))). % 28.66/17.99 tff(c_10042, 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))). % 28.66/17.99 tff(c_4769, 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))). % 28.66/17.99 tff(c_50692, plain, (![C_986]: (ifeq(iext(uri_rdfs_subClassOf, C_986, uri_rdf_Alt), true, iext(uri_rdfs_subClassOf, C_986, uri_rdfs_Resource), true)=true))). % 28.66/17.99 tff(c_50679, plain, (![X_984, Y_985]: (ifeq(iext(uri_rdf__2, X_984, Y_985), true, iext(uri_rdf__2, X_984, Y_985), true)=true))). % 28.66/17.99 tff(c_7676, 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))). % 28.66/17.99 tff(c_6365, 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))). % 28.66/17.99 tff(c_4851, 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))). % 28.66/17.99 tff(c_5014, 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))). % 28.66/17.99 tff(c_4169, 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))). % 28.66/17.99 tff(c_4946, 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))). % 28.66/17.99 tff(c_5994, 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))). % 28.66/17.99 tff(c_49587, plain, (![X_970, Y_971]: (ifeq(iext(uri_rdf_object, X_970, Y_971), true, iext(uri_rdf_object, X_970, Y_971), true)=true))). % 28.66/17.99 tff(c_8000, 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))). % 28.66/17.99 tff(c_5904, 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))). % 28.66/17.99 tff(c_7430, 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))). % 28.66/18.00 tff(c_5329, 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))). % 28.66/18.00 tff(c_3977, 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))). % 28.66/18.00 tff(c_48544, plain, (![X_956, Y_957]: (ifeq(iext(uri_rdf__3, X_956, Y_957), true, iext(uri_rdf__3, X_956, Y_957), true)=true))). % 28.66/18.00 tff(c_6797, 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))). % 28.66/18.00 tff(c_7742, 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))). % 28.66/18.00 tff(c_4217, 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))). % 28.66/18.00 tff(c_4214, 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))). % 28.66/18.00 tff(c_7342, 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))). % 28.66/18.00 tff(c_47525, plain, (![C_945]: (ifeq(iext(uri_rdfs_subClassOf, C_945, uri_rdfs_Literal), true, iext(uri_rdfs_subClassOf, C_945, uri_rdfs_Resource), true)=true))). % 28.66/18.00 tff(c_4260, 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))). % 28.66/18.00 tff(c_7846, 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))). % 28.66/18.00 tff(c_4073, 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))). % 28.66/18.00 tff(c_3980, 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))). % 28.66/18.00 tff(c_46883, plain, (![C_936]: (ifeq(iext(uri_rdfs_subClassOf, C_936, uri_rdfs_ContainerMembershipProperty), true, iext(uri_rdfs_subClassOf, C_936, uri_rdfs_Resource), true)=true))). % 28.66/18.00 tff(c_46856, plain, (![X_932, Y_933]: (ifeq(iext(uri_rdf_rest, X_932, Y_933), true, iext(uri_rdf_rest, X_932, Y_933), true)=true))). % 28.66/18.00 tff(c_8060, 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))). % 28.66/18.00 tff(c_5208, 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))). % 28.66/18.00 tff(c_5512, 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))). % 28.66/18.00 tff(c_7522, 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))). % 28.66/18.00 tff(c_4025, 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))). % 28.66/18.00 tff(c_7157, 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))). % 28.66/18.00 tff(c_45243, plain, (![C_917]: (ifeq(iext(uri_rdfs_subClassOf, C_917, uri_rdf_Property), true, iext(uri_rdfs_subClassOf, C_917, uri_rdfs_Resource), true)=true))). % 28.66/18.00 tff(c_4501, 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))). % 28.66/18.00 tff(c_44812, plain, (![X_912, Y_913]: (ifeq(iext(uri_rdfs_range, X_912, Y_913), true, iext(uri_rdfs_range, X_912, Y_913), true)=true))). % 28.66/18.00 tff(c_44743, plain, (![P_910]: (ifeq(iext(uri_rdfs_subPropertyOf, P_910, uri_rdf__1), true, iext(uri_rdfs_subPropertyOf, P_910, uri_rdfs_member), true)=true))). % 28.66/18.00 tff(c_5679, 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))). % 28.66/18.00 tff(c_9830, 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))). % 28.66/18.00 tff(c_43941, plain, (![X_900, Y_901]: (ifeq(iext(uri_rdf__1, X_900, Y_901), true, iext(uri_rdfs_member, X_900, Y_901), true)=true))). % 28.66/18.00 tff(c_43467, plain, (![P_894]: (ifeq(iext(uri_rdfs_subPropertyOf, P_894, uri_rdf__3), true, iext(uri_rdfs_subPropertyOf, P_894, uri_rdfs_member), true)=true))). % 28.66/18.00 tff(c_43136, plain, (![X_890, Y_891]: (ifeq(iext(uri_rdfs_domain, X_890, Y_891), true, iext(uri_rdfs_domain, X_890, Y_891), true)=true))). % 28.66/18.00 tff(c_42890, plain, (![X_884, Y_885]: (ifeq(iext(uri_rdfs_seeAlso, X_884, Y_885), true, iext(uri_rdfs_seeAlso, X_884, Y_885), true)=true))). % 28.66/18.00 tff(c_4076, 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))). % 28.66/18.00 tff(c_3932, 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))). % 28.66/18.00 tff(c_6426, 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))). % 28.66/18.00 tff(c_42223, plain, (![X_873, Y_874]: (ifeq(iext(uri_rdf__1, X_873, Y_874), true, iext(uri_rdf__1, X_873, Y_874), true)=true))). % 28.66/18.00 tff(c_42085, plain, (![C_871]: (ifeq(iext(uri_rdfs_subClassOf, C_871, uri_rdf_XMLLiteral), true, iext(uri_rdfs_subClassOf, C_871, uri_rdfs_Resource), true)=true))). % 28.66/18.00 tff(c_42058, plain, (![X_867, Y_868]: (ifeq(iext(uri_rdfs_isDefinedBy, X_867, Y_868), true, iext(uri_rdfs_isDefinedBy, X_867, Y_868), true)=true))). % 28.66/18.00 tff(c_42031, plain, (![X_863, Y_864]: (ifeq(iext(uri_rdf__3, X_863, Y_864), true, iext(uri_rdfs_member, X_863, Y_864), true)=true))). % 28.66/18.00 tff(c_5130, 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))). % 28.66/18.00 tff(c_8990, 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))). % 28.66/18.00 tff(c_10483, 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))). % 28.66/18.00 tff(c_41335, plain, (![C_856]: (ifeq(iext(uri_rdfs_subClassOf, C_856, uri_rdfs_Container), true, iext(uri_rdfs_subClassOf, C_856, uri_rdfs_Resource), true)=true))). % 28.66/18.00 tff(c_41195, plain, (![C_854]: (ifeq(iext(uri_rdfs_subClassOf, C_854, uri_rdf_Bag), true, iext(uri_rdfs_subClassOf, C_854, uri_rdfs_Resource), true)=true))). % 28.66/18.00 tff(c_12286, 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))). % 28.66/18.00 tff(c_4444, plain, (![P_47, X_137]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, X_137, uri_rdfs_Resource), true, true, true), true)=true))). % 28.66/18.00 tff(c_8664, 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))). % 28.66/18.00 tff(c_12289, 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))). % 28.66/18.00 tff(c_13881, 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))). % 28.66/18.00 tff(c_8661, 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))). % 28.66/18.00 tff(c_12563, 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))). % 28.66/18.00 tff(c_12566, 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))). % 28.66/18.00 tff(c_5455, 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))). % 28.66/18.00 tff(c_13334, 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))). % 28.66/18.00 tff(c_13884, 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))). % 28.66/18.00 tff(c_5452, 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))). % 28.66/18.00 tff(c_13331, 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))). % 28.66/18.00 tff(c_3770, 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))). % 28.66/18.00 tff(c_3691, 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))). % 28.66/18.00 tff(c_3313, 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))). % 28.66/18.00 tff(c_3810, 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))). % 28.66/18.00 tff(c_3568, 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))). % 28.66/18.00 tff(c_3350, 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))). % 28.66/18.00 tff(c_3644, 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))). % 28.66/18.00 tff(c_3607, 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))). % 28.66/18.00 tff(c_3353, 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))). % 28.66/18.00 tff(c_3571, 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))). % 28.66/18.00 tff(c_3767, 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))). % 28.66/18.00 tff(c_3392, 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))). % 28.66/18.00 tff(c_3226, 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))). % 28.66/18.00 tff(c_3517, 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))). % 28.66/18.00 tff(c_3432, 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))). % 28.66/18.00 tff(c_3267, 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))). % 28.66/18.01 tff(c_3647, 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))). % 28.66/18.01 tff(c_3264, 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))). % 28.66/18.01 tff(c_3520, 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))). % 28.66/18.01 tff(c_3476, 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))). % 28.66/18.01 tff(c_3389, 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))). % 28.66/18.01 tff(c_3610, 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))). % 28.66/18.01 tff(c_3479, 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))). % 28.66/18.01 tff(c_3316, 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))). % 28.66/18.01 tff(c_3728, 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))). % 28.66/18.01 tff(c_3688, 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))). % 28.66/18.01 tff(c_3223, 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))). % 28.66/18.01 tff(c_3813, 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))). % 28.66/18.01 tff(c_3435, 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))). % 28.66/18.01 tff(c_3731, 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))). % 28.66/18.01 tff(c_1624, 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))). % 28.66/18.01 tff(c_1947, 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))). % 28.66/18.01 tff(c_2670, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf_Property, uri_rdfs_Class), true, true, true), true)=true))). % 28.66/18.01 tff(c_2511, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf_rest, uri_rdf_Property), true, true, true), true)=true))). % 28.66/18.01 tff(c_2529, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdfs_comment, uri_rdfs_Resource), true, true, true), true)=true))). % 28.66/18.01 tff(c_2628, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_subClassOf), true, ifeq(iext(P_106, uri_rdfs_Seq, uri_rdfs_Container), true, true, true), true)=true))). % 28.66/18.01 tff(c_2712, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdfs_seeAlso, uri_rdfs_Resource), true, true, true), true)=true))). % 28.66/18.01 tff(c_2463, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf_nil, uri_rdf_List), true, true, true), true)=true))). % 28.66/18.01 tff(c_2640, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdfs_member, uri_rdfs_Resource), true, true, true), true)=true))). % 28.66/18.01 tff(c_33570, plain, (![C_752]: (ifeq(iext(uri_rdfs_subClassOf, C_752, uri_rdfs_ContainerMembershipProperty), true, iext(uri_rdfs_subClassOf, C_752, uri_rdf_Property), true)=true))). % 28.66/18.01 tff(c_33545, plain, (![C_751]: (ifeq(iext(uri_rdfs_subClassOf, C_751, uri_rdf_XMLLiteral), true, iext(uri_rdfs_subClassOf, C_751, uri_rdfs_Literal), true)=true))). % 28.66/18.01 tff(c_2457, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdf__2, uri_rdfs_Resource), true, true, true), true)=true))). % 28.66/18.01 tff(c_2586, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdfs_comment, uri_rdfs_Literal), true, true, true), true)=true))). % 28.66/18.01 tff(c_2592, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdf_type, uri_rdfs_Resource), true, true, true), true)=true))). % 28.66/18.01 tff(c_2748, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdfs_seeAlso, uri_rdfs_Resource), true, true, true), true)=true))). % 28.66/18.01 tff(c_2469, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdfs_subPropertyOf, uri_rdf_Property), true, true, true), true)=true))). % 28.66/18.01 tff(c_2646, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf_subject, uri_rdf_Property), true, true, true), true)=true))). % 28.66/18.01 tff(c_2562, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdfs_domain, uri_rdfs_Class), true, true, true), true)=true))). % 28.66/18.01 tff(c_32716, plain, (![X_740, Y_741]: (ifeq(iext(uri_rdfs_isDefinedBy, X_740, Y_741), true, iext(uri_rdfs_seeAlso, X_740, Y_741), true)=true))). % 28.66/18.01 tff(c_2574, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf__1, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 28.66/18.01 tff(c_32555, plain, (![C_737]: (ifeq(iext(uri_rdfs_subClassOf, C_737, uri_rdfs_Datatype), true, iext(uri_rdfs_subClassOf, C_737, uri_rdfs_Class), true)=true))). % 28.66/18.01 tff(c_2730, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdfs_label, uri_rdfs_Literal), true, true, true), true)=true))). % 28.66/18.01 tff(c_2556, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdf_subject, uri_rdfs_Statement), true, true, true), true)=true))). % 28.66/18.01 tff(c_2652, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdf_first, uri_rdf_List), true, true, true), true)=true))). % 28.66/18.01 tff(c_2634, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdfs_subClassOf, uri_rdfs_Class), true, true, true), true)=true))). % 28.66/18.01 tff(c_2706, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_subClassOf), true, ifeq(iext(P_106, uri_rdfs_Datatype, uri_rdfs_Class), true, true, true), true)=true))). % 28.66/18.01 tff(c_2676, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdf_first, uri_rdfs_Resource), true, true, true), true)=true))). % 28.66/18.01 tff(c_2616, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf_XMLLiteral, uri_rdfs_Datatype), true, true, true), true)=true))). % 28.66/18.01 tff(c_2754, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdfs_subPropertyOf, uri_rdf_Property), true, true, true), true)=true))). % 28.66/18.01 tff(c_31586, plain, (![C_727]: (ifeq(iext(uri_rdfs_subClassOf, C_727, uri_rdf_Alt), true, iext(uri_rdfs_subClassOf, C_727, uri_rdfs_Container), true)=true))). % 28.66/18.01 tff(c_2523, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdf_predicate, uri_rdfs_Resource), true, true, true), true)=true))). % 28.66/18.01 tff(c_2544, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdfs_range, uri_rdf_Property), true, true, true), true)=true))). % 28.66/18.01 tff(c_2505, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true, true, true), true)=true))). % 28.66/18.01 tff(c_2415, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true, true, true), true)=true))). % 28.66/18.01 tff(c_2421, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_subClassOf), true, ifeq(iext(P_106, uri_rdf_XMLLiteral, uri_rdfs_Literal), true, true, true), true)=true))). % 28.66/18.01 tff(c_2580, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf_value, uri_rdf_Property), true, true, true), true)=true))). % 28.66/18.01 tff(c_2475, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdf__1, uri_rdfs_Resource), true, true, true), true)=true))). % 28.66/18.01 tff(c_2682, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_subClassOf), true, ifeq(iext(P_106, uri_rdf_Bag, uri_rdfs_Container), true, true, true), true)=true))). % 28.66/18.01 tff(c_2487, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdf__3, uri_rdfs_Resource), true, true, true), true)=true))). % 28.66/18.01 tff(c_2742, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdfs_label, uri_rdfs_Resource), true, true, true), true)=true))). % 28.66/18.01 tff(c_2664, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdfs_domain, uri_rdf_Property), true, true, true), true)=true))). % 28.66/18.01 tff(c_2445, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdf_predicate, uri_rdfs_Statement), true, true, true), true)=true))). % 28.66/18.01 tff(c_2622, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdf_rest, uri_rdf_List), true, true, true), true)=true))). % 28.66/18.01 tff(c_2550, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf_object, uri_rdf_Property), true, true, true), true)=true))). % 28.66/18.01 tff(c_29921, plain, (![D_711]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_711), true, icext(D_711, uri_rdfs_member), true)=true))). % 28.66/18.01 tff(c_29855, plain, (![D_709]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_709), true, icext(D_709, uri_rdfs_Resource), true)=true))). % 28.66/18.01 tff(c_2724, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf_first, uri_rdf_Property), true, true, true), true)=true))). % 28.66/18.01 tff(c_29678, plain, (![D_706]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_706), true, icext(D_706, uri_rdfs_subClassOf), true)=true))). % 28.66/18.01 tff(c_29610, plain, (![D_704]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_704), true, icext(D_704, uri_rdfs_subPropertyOf), true)=true))). % 28.66/18.01 tff(c_2517, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf__2, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 28.66/18.01 tff(c_29433, plain, (![D_701]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_701), true, icext(D_701, uri_rdfs_domain), true)=true))). % 28.66/18.01 tff(c_29367, plain, (![D_699]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_699), true, icext(D_699, uri_rdfs_seeAlso), true)=true))). % 28.66/18.01 tff(c_2658, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdf_subject, uri_rdfs_Resource), true, true, true), true)=true))). % 28.66/18.01 tff(c_29185, plain, (![D_696]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_696), true, icext(D_696, uri_rdfs_isDefinedBy), true)=true))). % 28.66/18.01 tff(c_29091, plain, (![D_694]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_694), true, icext(D_694, uri_rdfs_Class), true)=true))). % 28.66/18.01 tff(c_2493, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdfs_range, uri_rdfs_Class), true, true, true), true)=true))). % 28.66/18.01 tff(c_28912, plain, (![D_691]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_691), true, icext(D_691, uri_rdf_Bag), true)=true))). % 28.66/18.01 tff(c_28837, plain, (![D_689]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_689), true, icext(D_689, uri_rdf_XMLLiteral), true)=true))). % 28.66/18.01 tff(c_28769, plain, (![C_687]: (ifeq(iext(uri_rdfs_subClassOf, C_687, uri_rdfs_Seq), true, iext(uri_rdfs_subClassOf, C_687, uri_rdfs_Container), true)=true))). % 28.66/18.01 tff(c_28704, plain, (![D_685]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_685), true, icext(D_685, uri_rdfs_Seq), true)=true))). % 28.66/18.01 tff(c_28636, plain, (![D_683]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_683), true, icext(D_683, uri_rdfs_ContainerMembershipProperty), true)=true))). % 28.66/18.01 tff(c_2427, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdf_value, uri_rdfs_Resource), true, true, true), true)=true))). % 28.66/18.01 tff(c_28450, plain, (![D_680]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_680), true, icext(D_680, uri_rdfs_Container), true)=true))). % 28.66/18.01 tff(c_28384, plain, (![D_678]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_678), true, icext(D_678, uri_rdfs_Literal), true)=true))). % 28.66/18.01 tff(c_28318, plain, (![D_676]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_676), true, icext(D_676, uri_rdfs_Datatype), true)=true))). % 28.66/18.01 tff(c_2718, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf__3, uri_rdf_Property), true, true, true), true)=true))). % 28.66/18.01 tff(c_28141, plain, (![D_673]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_673), true, icext(D_673, uri_rdf_Alt), true)=true))). % 28.66/18.01 tff(c_28074, plain, (![D_671]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_671), true, icext(D_671, uri_rdfs_comment), true)=true))). % 28.66/18.01 tff(c_28007, plain, (![C_669]: (ifeq(iext(uri_rdfs_subClassOf, C_669, uri_rdf_Bag), true, iext(uri_rdfs_subClassOf, C_669, uri_rdfs_Container), true)=true))). % 28.66/18.01 tff(c_27940, plain, (![D_667]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_667), true, icext(D_667, uri_rdf_List), true)=true))). % 28.66/18.01 tff(c_27874, plain, (![D_665]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_665), true, icext(D_665, uri_rdfs_Statement), true)=true))). % 28.66/18.01 tff(c_27698, plain, (![D_662]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_662), true, icext(D_662, uri_rdfs_label), true)=true))). % 28.66/18.01 tff(c_2610, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf__3, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 28.66/18.01 tff(c_27632, plain, (![D_660]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_660), true, icext(D_660, uri_rdfs_range), true)=true))). % 28.66/18.01 tff(c_27566, plain, (![D_658]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_658), true, icext(D_658, uri_rdf_predicate), true)=true))). % 28.66/18.01 tff(c_27381, plain, (![D_655]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_655), true, icext(D_655, uri_rdf_subject), true)=true))). % 28.66/18.01 tff(c_2451, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdf__2, uri_rdfs_Resource), true, true, true), true)=true))). % 28.66/18.01 tff(c_11820, 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))). % 28.66/18.01 tff(c_27269, plain, (![D_651]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_651), true, icext(D_651, uri_rdf__1), true)=true))). % 28.66/18.01 tff(c_14216, 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))). % 28.66/18.01 tff(c_13045, 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))). % 28.66/18.01 tff(c_2439, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdf__3, uri_rdfs_Resource), true, true, true), true)=true))). % 28.66/18.01 tff(c_13617, 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))). % 28.66/18.01 tff(c_11599, 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))). % 28.66/18.01 tff(c_11513, 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))). % 28.66/18.02 tff(c_11443, 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))). % 28.66/18.02 tff(c_12842, 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))). % 28.66/18.02 tff(c_2760, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdf_type, uri_rdfs_Class), true, true, true), true)=true))). % 28.66/18.02 tff(c_12954, 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))). % 28.66/18.02 tff(c_11257, 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))). % 28.66/18.02 tff(c_12841, 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))). % 28.66/18.02 tff(c_26709, plain, (![D_633]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_633), true, icext(D_633, uri_rdf__2), true)=true))). % 28.66/18.02 tff(c_11324, 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))). % 28.66/18.02 tff(c_11323, 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))). % 28.66/18.02 tff(c_2538, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_subPropertyOf), true, ifeq(iext(P_106, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso), true, true, true), true)=true))). % 28.66/18.02 tff(c_11072, 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))). % 28.66/18.02 tff(c_10996, 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))). % 28.66/18.02 tff(c_10949, 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))). % 28.66/18.02 tff(c_10805, 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))). % 28.66/18.02 tff(c_10756, 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))). % 28.66/18.02 tff(c_10901, 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))). % 28.66/18.02 tff(c_11166, 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))). % 28.66/18.02 tff(c_2736, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdf_rest, uri_rdf_List), true, true, true), true)=true))). % 28.66/18.02 tff(c_11119, 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))). % 28.66/18.02 tff(c_10853, 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))). % 28.66/18.02 tff(c_13403, 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))). % 28.66/18.02 tff(c_14088, 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))). % 28.66/18.02 tff(c_12635, 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))). % 28.66/18.02 tff(c_12506, 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))). % 28.66/18.02 tff(c_10673, 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))). % 28.66/18.02 tff(c_6748, 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))). % 28.66/18.02 tff(c_2694, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf__2, uri_rdf_Property), true, true, true), true)=true))). % 28.66/18.02 tff(c_8868, 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))). % 28.66/18.02 tff(c_9277, 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))). % 28.66/18.02 tff(c_9861, 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))). % 28.66/18.02 tff(c_2604, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdfs_subClassOf, uri_rdfs_Class), true, true, true), true)=true))). % 28.66/18.02 tff(c_6024, 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))). % 28.66/18.02 tff(c_6171, 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))). % 28.66/18.02 tff(c_6460, 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))). % 28.66/18.02 tff(c_5713, 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))). % 28.66/18.02 tff(c_6831, 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))). % 28.66/18.02 tff(c_8031, 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))). % 28.66/18.02 tff(c_7967, 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))). % 28.66/18.02 tff(c_25417, plain, (![D_589]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_589), true, icext(D_589, uri_rdf_rest), true)=true))). % 28.66/18.02 tff(c_6276, 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))). % 28.66/18.02 tff(c_5542, 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))). % 28.66/18.02 tff(c_9862, 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))). % 28.66/18.02 tff(c_2433, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdf_object, uri_rdfs_Statement), true, true, true), true)=true))). % 28.66/18.02 tff(c_5241, 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))). % 28.66/18.02 tff(c_4535, 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))). % 28.66/18.02 tff(c_6576, 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))). % 28.66/18.02 tff(c_5934, 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))). % 28.66/18.02 tff(c_10067, 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))). % 28.66/18.02 tff(c_7767, 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))). % 28.66/18.02 tff(c_9789, 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))). % 28.66/18.02 tff(c_2688, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_subClassOf), true, ifeq(iext(P_106, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property), true, true, true), true)=true))). % 28.66/18.02 tff(c_8094, 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))). % 28.66/18.02 tff(c_4876, 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))). % 28.66/18.02 tff(c_9927, 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))). % 28.66/18.02 tff(c_24851, plain, (![D_571]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_571), true, icext(D_571, uri_rdf__1), true)=true))). % 28.66/18.02 tff(c_6749, 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))). % 28.66/18.02 tff(c_7877, 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))). % 28.66/18.02 tff(c_2481, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdf__1, uri_rdfs_Resource), true, true, true), true)=true))). % 28.66/18.02 tff(c_8093, 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))). % 28.66/18.02 tff(c_10133, 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))). % 28.66/18.02 tff(c_9499, 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))). % 28.66/18.02 tff(c_24539, plain, (![D_562]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_562), true, icext(D_562, uri_rdf_type), true)=true))). % 28.66/18.02 tff(c_4803, 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))). % 28.66/18.02 tff(c_8181, 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))). % 28.66/18.02 tff(c_2409, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdf_value, uri_rdfs_Resource), true, true, true), true)=true))). % 28.66/18.02 tff(c_9926, 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))). % 28.66/18.02 tff(c_24211, plain, (![D_553]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_553), true, icext(D_553, uri_rdf_Property), true)=true))). % 28.66/18.02 tff(c_4534, 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))). % 28.66/18.02 tff(c_9276, 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))). % 28.66/18.02 tff(c_9022, 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))). % 28.66/18.02 tff(c_6396, 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))). % 28.66/18.02 tff(c_24012, plain, (![D_545]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_545), true, icext(D_545, uri_rdf_nil), true)=true))). % 28.66/18.02 tff(c_23938, plain, (![P_542]: (ifeq(iext(uri_rdfs_subPropertyOf, P_542, uri_rdfs_isDefinedBy), true, iext(uri_rdfs_subPropertyOf, P_542, uri_rdfs_seeAlso), true)=true))). % 28.66/18.02 tff(c_5871, 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))). % 28.66/18.02 tff(c_6277, 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))). % 28.66/18.02 tff(c_4976, 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))). % 28.66/18.02 tff(c_7553, 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))). % 28.66/18.02 tff(c_7710, 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))). % 28.66/18.02 tff(c_6830, 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))). % 28.66/18.02 tff(c_5163, 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))). % 28.66/18.02 tff(c_2568, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf_type, uri_rdf_Property), true, true, true), true)=true))). % 28.66/18.02 tff(c_5044, 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))). % 28.66/18.02 tff(c_10517, 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))). % 28.66/18.02 tff(c_5365, 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))). % 28.66/18.02 tff(c_10227, 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))). % 28.66/18.02 tff(c_5242, 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))). % 28.66/18.02 tff(c_5045, 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))). % 28.66/18.02 tff(c_4802, 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))). % 28.66/18.02 tff(c_2499, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdfs_member, uri_rdfs_Resource), true, true, true), true)=true))). % 28.66/18.02 tff(c_10283, 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))). % 28.66/18.02 tff(c_7182, 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))). % 28.66/18.02 tff(c_5712, 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))). % 28.66/18.02 tff(c_6461, 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))). % 28.66/18.02 tff(c_6657, 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))). % 28.66/18.02 tff(c_2700, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf__1, uri_rdf_Property), true, true, true), true)=true))). % 28.66/18.02 tff(c_7372, 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))). % 28.66/18.02 tff(c_22956, plain, (![D_510]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_510), true, icext(D_510, uri_rdf_value), true)=true))). % 28.66/18.02 tff(c_7462, 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))). % 28.66/18.02 tff(c_4464, plain, (![Q_48, X_137]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, X_137, uri_rdfs_Resource), true)=true))). % 28.66/18.02 tff(c_2598, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_subClassOf), true, ifeq(iext(P_106, uri_rdf_Alt, uri_rdfs_Container), true, true, true), true)=true))). % 28.66/18.02 tff(c_2808, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf_Property, uri_rdfs_Class), true)=true))). % 28.66/18.02 tff(c_2817, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf_first, uri_rdf_Property), true)=true))). % 28.66/18.02 tff(c_2781, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true)=true))). % 28.66/18.02 tff(c_2812, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf__2, uri_rdf_Property), true)=true))). % 28.66/18.02 tff(c_2809, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdf_first, uri_rdfs_Resource), true)=true))). % 28.66/18.02 tff(c_2772, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdf__2, uri_rdfs_Resource), true)=true))). % 28.66/18.02 tff(c_2815, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdfs_seeAlso, uri_rdfs_Resource), true)=true))). % 28.66/18.02 tff(c_2776, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdf__1, uri_rdfs_Resource), true)=true))). % 28.66/18.02 tff(c_2340, plain, (![E_104]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, E_104), true, iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, E_104), true)=true))). % 28.66/18.02 tff(c_2820, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdfs_label, uri_rdfs_Resource), true)=true))). % 28.66/18.02 tff(c_2765, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdf_value, uri_rdfs_Resource), true)=true))). % 28.66/18.02 tff(c_2794, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdfs_comment, uri_rdfs_Literal), true)=true))). % 28.66/18.02 tff(c_22329, plain, (![D_491]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_491), true, icext(D_491, uri_rdf__3), true)=true))). % 28.66/18.02 tff(c_2816, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf__3, uri_rdf_Property), true)=true))). % 28.66/18.02 tff(c_2775, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdfs_subPropertyOf, uri_rdf_Property), true)=true))). % 28.66/18.02 tff(c_2814, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_107), true, iext(Q_107, uri_rdfs_Datatype, uri_rdfs_Class), true)=true))). % 28.66/18.03 tff(c_2810, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_107), true, iext(Q_107, uri_rdf_Bag, uri_rdfs_Container), true)=true))). % 28.98/18.03 tff(c_2822, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdfs_subPropertyOf, uri_rdf_Property), true)=true))). % 28.98/18.03 tff(c_2786, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_107), true, iext(Q_107, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso), true)=true))). % 28.98/18.03 tff(c_2337, plain, (![E_104]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_104), true, iext(uri_rdfs_subClassOf, uri_rdf_Alt, E_104), true)=true))). % 28.98/18.03 tff(c_22126, plain, (![D_482]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_482), true, icext(D_482, uri_rdf_first), true)=true))). % 28.98/18.03 tff(c_2790, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdfs_domain, uri_rdfs_Class), true)=true))). % 28.98/18.03 tff(c_2819, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdf_rest, uri_rdf_List), true)=true))). % 28.98/18.03 tff(c_2767, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_107), true, iext(Q_107, uri_rdf_XMLLiteral, uri_rdfs_Literal), true)=true))). % 28.98/18.03 tff(c_2336, plain, (![E_104]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Literal, E_104), true, iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, E_104), true)=true))). % 28.98/18.03 tff(c_2777, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdf__1, uri_rdfs_Resource), true)=true))). % 28.98/18.03 tff(c_2785, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdfs_comment, uri_rdfs_Resource), true)=true))). % 28.98/18.03 tff(c_2813, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf__1, uri_rdf_Property), true)=true))). % 28.98/18.03 tff(c_2784, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdf_predicate, uri_rdfs_Resource), true)=true))). % 28.98/18.03 tff(c_2341, plain, (![E_104]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, E_104), true, iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, E_104), true)=true))). % 28.98/18.03 tff(c_2805, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdf_first, uri_rdf_List), true)=true))). % 28.98/18.03 tff(c_2792, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf__1, uri_rdfs_ContainerMembershipProperty), true)=true))). % 28.98/18.03 tff(c_2798, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf__3, uri_rdfs_ContainerMembershipProperty), true)=true))). % 28.98/18.03 tff(c_2800, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdf_rest, uri_rdf_List), true)=true))). % 28.98/18.03 tff(c_2818, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdfs_label, uri_rdfs_Literal), true)=true))). % 28.98/18.03 tff(c_2802, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdfs_subClassOf, uri_rdfs_Class), true)=true))). % 28.98/18.03 tff(c_2821, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdfs_seeAlso, uri_rdfs_Resource), true)=true))). % 28.98/18.03 tff(c_2773, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdf__2, uri_rdfs_Resource), true)=true))). % 28.98/18.03 tff(c_2796, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_107), true, iext(Q_107, uri_rdf_Alt, uri_rdfs_Container), true)=true))). % 28.98/18.03 tff(c_2770, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdf__3, uri_rdfs_Resource), true)=true))). % 28.98/18.03 tff(c_2799, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf_XMLLiteral, uri_rdfs_Datatype), true)=true))). % 28.98/18.03 tff(c_2338, plain, (![E_104]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_104), true, iext(uri_rdfs_subClassOf, uri_rdfs_Seq, E_104), true)=true))). % 28.98/18.03 tff(c_2806, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdf_subject, uri_rdfs_Resource), true)=true))). % 28.98/18.03 tff(c_2766, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true)=true))). % 28.98/18.03 tff(c_2780, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdfs_member, uri_rdfs_Resource), true)=true))). % 28.98/18.03 tff(c_2823, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdf_type, uri_rdfs_Class), true)=true))). % 28.98/18.03 tff(c_21550, plain, (![D_455]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_455), true, icext(D_455, uri_rdf__2), true)=true))). % 28.98/18.03 tff(c_13621, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_label), true)=true))). % 28.98/18.03 tff(c_2804, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf_subject, uri_rdf_Property), true)=true))). % 28.98/18.03 tff(c_13620, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_label), true)=true))). % 28.98/18.03 tff(c_13048, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_predicate), true)=true))). % 28.98/18.03 tff(c_13049, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_predicate), true)=true))). % 28.98/18.03 tff(c_14219, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_comment), true)=true))). % 28.98/18.03 tff(c_14220, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_comment), true)=true))). % 28.98/18.03 tff(c_11517, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Resource), true)=true))). % 28.98/18.03 tff(c_2789, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdf_subject, uri_rdfs_Statement), true)=true))). % 28.98/18.03 tff(c_11447, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_member), true)=true))). % 28.98/18.03 tff(c_21247, plain, (![D_443]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_443), true, icext(D_443, uri_rdf_object), true)=true))). % 28.98/18.03 tff(c_12957, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Statement), true)=true))). % 28.98/18.03 tff(c_12845, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Statement), true)=true))). % 28.98/18.03 tff(c_2791, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf_type, uri_rdf_Property), true)=true))). % 28.98/18.03 tff(c_11260, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_List), true)=true))). % 28.98/18.03 tff(c_11261, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdf_List), true)=true))). % 28.98/18.03 tff(c_2271, plain, (![R_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_seeAlso, R_101), true, iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, R_101), true)=true))). % 28.98/18.03 tff(c_21010, plain, (![D_435]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, D_435), true, icext(D_435, uri_rdf_XMLLiteral), true)=true))). % 28.98/18.03 tff(c_2803, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdfs_member, uri_rdfs_Resource), true)=true))). % 28.98/18.03 tff(c_2783, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf__2, uri_rdfs_ContainerMembershipProperty), true)=true))). % 28.98/18.03 tff(c_20874, plain, (![D_431]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_431), true, icext(D_431, uri_rdf__3), true)=true))). % 28.98/18.03 tff(c_2778, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdf__3, uri_rdfs_Resource), true)=true))). % 28.98/18.03 tff(c_10137, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_seeAlso), true)=true))). % 28.98/18.03 tff(c_20670, plain, (![C_89, X_61]: (ifeq(icext(C_89, X_61), true, true, true)=true))). % 28.98/18.03 tff(c_7970, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_rest), true)=true))). % 28.98/18.03 tff(c_9026, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_object), true)=true))). % 28.98/18.03 tff(c_2811, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_107), true, iext(Q_107, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property), true)=true))). % 28.98/18.03 tff(c_20233, plain, (![D_420, X_421]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, D_420), true, icext(D_420, X_421), true)=true))). % 28.98/18.03 tff(c_7712, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Datatype), true)=true))). % 28.98/18.03 tff(c_9025, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_object), true)=true))). % 28.98/18.03 tff(c_9502, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_range), true)=true))). % 28.98/18.03 tff(c_2782, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf_rest, uri_rdf_Property), true)=true))). % 28.98/18.03 tff(c_9503, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_range), true)=true))). % 28.98/18.03 tff(c_5544, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_domain), true)=true))). % 28.98/18.03 tff(c_19752, plain, (![X_410, Y_411]: (ifeq(iext(uri_rdfs_range, X_410, Y_411), true, icext(uri_rdf_Property, X_410), true)=true))). % 28.98/18.03 tff(c_6174, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Class), true)=true))). % 28.98/18.03 tff(c_4978, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_value), true)=true))). % 28.98/18.03 tff(c_2797, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdfs_subClassOf, uri_rdfs_Class), true)=true))). % 28.98/18.03 tff(c_8035, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_subClassOf), true)=true))). % 28.98/18.03 tff(c_19263, plain, (![X_402, Y_403]: (ifeq(iext(uri_rdfs_domain, X_402, Y_403), true, icext(uri_rdf_Property, X_402), true)=true))). % 28.98/18.03 tff(c_7881, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_subject), true)=true))). % 28.98/18.03 tff(c_2339, plain, (![E_104]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_104), true, iext(uri_rdfs_subClassOf, uri_rdf_Bag, E_104), true)=true))). % 28.98/18.03 tff(c_18878, plain, (![X_396, Y_397]: (ifeq(iext(uri_rdfs_range, X_396, Y_397), true, icext(uri_rdfs_Class, Y_397), true)=true))). % 28.98/18.03 tff(c_7880, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_subject), true)=true))). % 28.98/18.03 tff(c_2801, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_107), true, iext(Q_107, uri_rdfs_Seq, uri_rdfs_Container), true)=true))). % 28.98/18.03 tff(c_10230, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__2), true)=true))). % 28.98/18.03 tff(c_18232, plain, (![X_388, Y_389]: (ifeq(iext(uri_rdfs_subClassOf, X_388, Y_389), true, icext(uri_rdfs_Class, X_388), true)=true))). % 28.98/18.03 tff(c_8034, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_subClassOf), true)=true))). % 28.98/18.03 tff(c_6661, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Container), true)=true))). % 28.98/18.03 tff(c_2779, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdfs_range, uri_rdfs_Class), true)=true))). % 28.98/18.03 tff(c_17656, plain, (![X_380, Y_381]: (ifeq(iext(uri_rdfs_subClassOf, X_380, Y_381), true, icext(uri_rdfs_Class, Y_381), true)=true))). % 28.98/18.03 tff(c_6578, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_Bag), true)=true))). % 28.98/18.03 tff(c_6398, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_first), true)=true))). % 28.98/18.03 tff(c_2768, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdf_value, uri_rdfs_Resource), true)=true))). % 28.98/18.03 tff(c_9792, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_XMLLiteral), true)=true))). % 28.98/18.03 tff(c_5936, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_type), true)=true))). % 28.98/18.03 tff(c_17474, plain, (![X_371, Y_372]: (ifeq(iext(uri_rdf_rest, X_371, Y_372), true, icext(uri_rdf_List, X_371), true)=true))). % 28.98/18.03 tff(c_7465, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__3), true)=true))). % 28.98/18.03 tff(c_2788, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf_object, uri_rdf_Property), true)=true))). % 28.98/18.03 tff(c_6399, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_first), true)=true))). % 28.98/18.03 tff(c_8871, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_ContainerMembershipProperty), true)=true))). % 28.98/18.03 tff(c_16997, plain, (![X_363, Y_364]: (ifeq(iext(uri_rdfs_subPropertyOf, X_363, Y_364), true, icext(uri_rdf_Property, X_363), true)=true))). % 28.98/18.03 tff(c_7374, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__1), true)=true))). % 28.98/18.03 tff(c_2793, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf_value, uri_rdf_Property), true)=true))). % 28.98/18.03 tff(c_7555, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_subPropertyOf), true)=true))). % 28.98/18.03 tff(c_16888, plain, (![X_356, Y_357]: (ifeq(iext(uri_rdf_object, X_356, Y_357), true, icext(uri_rdfs_Statement, X_356), true)=true))). % 28.98/18.03 tff(c_2787, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdfs_range, uri_rdf_Property), true)=true))). % 28.98/18.03 tff(c_5047, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__2), true)=true))). % 28.98/18.03 tff(c_16795, plain, (![X_350, Y_351]: (ifeq(iext(uri_rdf_first, X_350, Y_351), true, icext(uri_rdf_List, X_350), true)=true))). % 28.98/18.03 tff(c_6026, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_isDefinedBy), true)=true))). % 28.98/18.03 tff(c_2807, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdfs_domain, uri_rdf_Property), true)=true))). % 28.98/18.03 tff(c_5165, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_Alt), true)=true))). % 28.98/18.03 tff(c_5545, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_domain), true)=true))). % 28.98/18.03 tff(c_16656, plain, (![X_342, Y_343]: (ifeq(iext(uri_rdfs_label, X_342, Y_343), true, icext(uri_rdfs_Literal, Y_343), true)=true))). % 28.98/18.03 tff(c_5874, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdf_Property), true)=true))). % 28.98/18.03 tff(c_2774, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf_nil, uri_rdf_List), true)=true))). % 28.98/18.03 tff(c_7375, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__1), true)=true))). % 28.98/18.03 tff(c_7556, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_subPropertyOf), true)=true))). % 28.98/18.03 tff(c_16103, plain, (![X_334, Y_335]: (ifeq(iext(uri_rdf_type, X_334, Y_335), true, icext(uri_rdfs_Class, Y_335), true)=true))). % 28.98/18.03 tff(c_5368, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Literal), true)=true))). % 28.98/18.03 tff(c_10520, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Seq), true)=true))). % 28.98/18.03 tff(c_2795, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdf_type, uri_rdfs_Resource), true)=true))). % 28.98/18.03 tff(c_6278, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_member), true)=true))). % 28.98/18.03 tff(c_15973, plain, (![X_326, Y_327]: (ifeq(iext(uri_rdfs_comment, X_326, Y_327), true, icext(uri_rdfs_Literal, Y_327), true)=true))). % 28.98/18.03 tff(c_4979, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_value), true)=true))). % 28.98/18.03 tff(c_5937, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_type), true)=true))). % 28.98/18.03 tff(c_2769, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdf_object, uri_rdfs_Statement), true)=true))). % 28.98/18.03 tff(c_7969, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_rest), true)=true))). % 28.98/18.03 tff(c_9865, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__3), true)=true))). % 28.98/18.03 tff(c_6832, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Resource), true)=true))). % 28.98/18.03 tff(c_15796, plain, (![X_316, Y_317]: (ifeq(iext(uri_rdf_predicate, X_316, Y_317), true, icext(uri_rdfs_Statement, X_316), true)=true))). % 28.98/18.03 tff(c_4465, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_29), true, icext(C_29, uri_rdfs_Resource), true)=true))). % 28.98/18.03 tff(c_4466, plain, (![C_19, X_137]: (ifeq(iext(uri_rdfs_domain, uri_rdf_type, C_19), true, icext(C_19, X_137), true)=true))). % 28.98/18.03 tff(c_2771, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdf_predicate, uri_rdfs_Statement), true)=true))). % 28.98/18.03 tff(c_1861, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdf_value), true)=true))). % 28.98/18.04 tff(c_1927, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_seeAlso), true)=true))). % 28.98/18.04 tff(c_15081, plain, (![X_304, Y_305]: (ifeq(iext(uri_rdfs_subPropertyOf, X_304, Y_305), true, icext(uri_rdf_Property, Y_305), true)=true))). % 28.98/18.04 tff(c_1877, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf__1), true)=true))). % 28.98/18.04 tff(c_1897, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_comment), true)=true))). % 28.98/18.04 tff(c_1905, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_93), true, icext(C_93, uri_rdfs_Seq), true)=true))). % 28.98/18.04 tff(c_1928, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_subPropertyOf), true)=true))). % 28.98/18.04 tff(c_2231, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdf_Property), true)=true))). % 28.98/18.04 tff(c_1926, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_label), true)=true))). % 28.98/18.04 tff(c_1914, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_93), true, icext(C_93, uri_rdf_Bag), true)=true))). % 28.98/18.04 tff(c_1889, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_93), true, icext(C_93, uri_rdfs_isDefinedBy), true)=true))). % 28.98/18.04 tff(c_1870, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf_predicate), true)=true))). % 28.98/18.04 tff(c_14438, plain, (![X_285, Y_286]: (ifeq(iext(uri_rdfs_domain, X_285, Y_286), true, icext(uri_rdfs_Class, Y_286), true)=true))). % 28.98/18.04 tff(c_1863, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_isDefinedBy), true)=true))). % 28.98/18.04 tff(c_1869, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf__3), true)=true))). % 28.98/18.04 tff(c_2184, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_97), true, icext(C_97, uri_rdfs_Literal), true)=true))). % 28.98/18.04 tff(c_1909, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf_first), true)=true))). % 28.98/18.04 tff(c_1872, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf__2), true)=true))). % 28.98/18.04 tff(c_1929, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdf_type), true)=true))). % 28.98/18.04 tff(c_1915, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_93), true, icext(C_93, uri_rdfs_ContainerMembershipProperty), true)=true))). % 28.98/18.04 tff(c_1893, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_domain), true)=true))). % 28.98/18.04 tff(c_1867, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf_object), true)=true))). % 28.98/18.04 tff(c_2248, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_97), true, icext(C_97, uri_rdf_Property), true)=true))). % 28.98/18.04 tff(c_1879, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdf__3), true)=true))). % 28.98/18.04 tff(c_14165, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_comment, uri_rdfs_comment)=true)). % 28.98/18.04 tff(c_1907, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_member), true)=true))). % 28.98/18.04 tff(c_14099, plain, (ip(uri_rdfs_comment)=true)). % 28.98/18.04 tff(c_14046, plain, (iext(uri_rdf_type, uri_rdfs_comment, uri_rdf_Property)=true)). % 28.98/18.04 tff(c_1875, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_subPropertyOf), true)=true))). % 28.98/18.04 tff(c_13855, plain, (icext(uri_rdf_Property, uri_rdfs_comment)=true)). % 28.98/18.04 tff(c_1888, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_comment), true)=true))). % 28.98/18.04 tff(c_1918, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_93), true, icext(C_93, uri_rdfs_Datatype), true)=true))). % 28.98/18.04 tff(c_13245, plain, (![X_261, Y_262]: (ifeq(iext(uri_rdf_subject, X_261, Y_262), true, icext(uri_rdfs_Statement, X_261), true)=true))). % 28.98/18.04 tff(c_1901, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_subClassOf), true)=true))). % 28.98/18.04 tff(c_1906, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_subClassOf), true)=true))). % 28.98/18.04 tff(c_1920, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_seeAlso), true)=true))). % 28.98/18.04 tff(c_2208, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_97), true, icext(C_97, uri_rdfs_seeAlso), true)=true))). % 28.98/18.04 tff(c_1880, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_range), true)=true))). % 28.98/18.04 tff(c_1911, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_domain), true)=true))). % 28.98/18.04 tff(c_13566, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_label, uri_rdfs_label)=true)). % 28.98/18.04 tff(c_13414, plain, (ip(uri_rdfs_label)=true)). % 28.98/18.04 tff(c_13361, plain, (iext(uri_rdf_type, uri_rdfs_label, uri_rdf_Property)=true)). % 28.98/18.04 tff(c_13305, plain, (icext(uri_rdf_Property, uri_rdfs_label)=true)). % 28.98/18.04 tff(c_1923, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_label), true)=true))). % 28.98/18.04 tff(c_2232, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_97), true, icext(C_97, uri_rdfs_Class), true)=true))). % 28.98/18.04 tff(c_2192, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_97), true, icext(C_97, uri_rdf_List), true)=true))). % 28.98/18.04 tff(c_2204, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_97), true, icext(C_97, uri_rdfs_ContainerMembershipProperty), true)=true))). % 28.98/18.04 tff(c_1899, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf_type), true)=true))). % 28.98/18.04 tff(c_1882, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_member), true)=true))). % 28.98/18.04 tff(c_2236, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_97), true, icext(C_97, uri_rdf_Property), true)=true))). % 28.98/18.04 tff(c_2218, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_97), true, icext(C_97, uri_rdfs_Container), true)=true))). % 28.98/18.04 tff(c_12959, plain, (![X_33]: (ifeq(icext(uri_rdfs_Statement, X_33), true, icext(uri_rdfs_Statement, X_33), true)=true))). % 28.98/18.04 tff(c_12994, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_predicate, uri_rdf_predicate)=true)). % 28.98/18.04 tff(c_1883, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_isDefinedBy), true)=true))). % 28.98/18.04 tff(c_12903, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Statement, uri_rdfs_Statement)=true)). % 28.98/18.04 tff(c_12790, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Statement, uri_rdfs_Resource)=true)). % 28.98/18.04 tff(c_12646, plain, (ip(uri_rdf_predicate)=true)). % 28.98/18.04 tff(c_12593, plain, (iext(uri_rdf_type, uri_rdf_predicate, uri_rdf_Property)=true)). % 28.98/18.04 tff(c_12537, plain, (icext(uri_rdf_Property, uri_rdf_predicate)=true)). % 28.98/18.04 tff(c_1886, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdf_predicate), true)=true))). % 28.98/18.04 tff(c_12470, plain, (iext(uri_rdf_type, uri_rdfs_Statement, uri_rdfs_Class)=true)). % 28.98/18.04 tff(c_12327, plain, (ic(uri_rdfs_Statement)=true)). % 28.98/18.04 tff(c_12260, plain, (icext(uri_rdfs_Class, uri_rdfs_Statement)=true)). % 28.98/18.04 tff(c_2186, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdfs_Statement), true)=true))). % 28.98/18.04 tff(c_11262, plain, (![X_33]: (ifeq(icext(uri_rdf_List, X_33), true, icext(uri_rdf_List, X_33), true)=true))). % 28.98/18.04 tff(c_8873, plain, (![X_33]: (ifeq(icext(uri_rdfs_ContainerMembershipProperty, X_33), true, icext(uri_rdfs_ContainerMembershipProperty, X_33), true)=true))). % 28.98/18.04 tff(c_11848, plain, (![X_232, Y_233]: (ifeq(iext(uri_rdf_rest, X_232, Y_233), true, icext(uri_rdf_List, Y_233), true)=true))). % 28.98/18.04 tff(c_6662, plain, (![X_33]: (ifeq(icext(uri_rdfs_Container, X_33), true, icext(uri_rdfs_Container, X_33), true)=true))). % 28.98/18.04 tff(c_5875, plain, (![X_33]: (ifeq(icext(uri_rdf_Property, X_33), true, icext(uri_rdf_Property, X_33), true)=true))). % 28.98/18.04 tff(c_7714, plain, (![X_33]: (ifeq(icext(uri_rdfs_Datatype, X_33), true, icext(uri_rdfs_Datatype, X_33), true)=true))). % 28.98/18.04 tff(c_6175, plain, (![X_33]: (ifeq(icext(uri_rdfs_Class, X_33), true, icext(uri_rdfs_Class, X_33), true)=true))). % 28.98/18.04 tff(c_5369, plain, (![X_33]: (ifeq(icext(uri_rdfs_Literal, X_33), true, icext(uri_rdfs_Literal, X_33), true)=true))). % 28.98/18.04 tff(c_6580, plain, (![X_33]: (ifeq(icext(uri_rdf_Bag, X_33), true, icext(uri_rdf_Bag, X_33), true)=true))). % 28.98/18.04 tff(c_5167, plain, (![X_33]: (ifeq(icext(uri_rdf_Alt, X_33), true, icext(uri_rdf_Alt, X_33), true)=true))). % 28.98/18.04 tff(c_10522, plain, (![X_33]: (ifeq(icext(uri_rdfs_Seq, X_33), true, icext(uri_rdfs_Seq, X_33), true)=true))). % 28.98/18.04 tff(c_9794, plain, (![X_33]: (ifeq(icext(uri_rdf_XMLLiteral, X_33), true, icext(uri_rdf_XMLLiteral, X_33), true)=true))). % 28.98/18.04 tff(c_11759, plain, (iext(uri_rdf_type, uri_rdfs_Resource, uri_rdfs_Class)=true)). % 28.98/18.04 tff(c_1910, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdf_subject), true)=true))). % 28.98/18.04 tff(c_11611, plain, (icext(uri_rdf_Property, uri_rdfs_member)=true)). % 28.98/18.04 tff(c_11557, plain, (iext(uri_rdf_type, uri_rdfs_member, uri_rdf_Property)=true)). % 28.98/18.04 tff(c_11459, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Resource, uri_rdfs_Resource)=true)). % 28.98/18.04 tff(c_11364, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_member, uri_rdfs_member)=true)). % 28.98/18.04 tff(c_2243, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_97), true, icext(C_97, uri_rdfs_Literal), true)=true))). % 28.98/18.04 tff(c_11272, plain, (iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdfs_Resource)=true)). % 28.98/18.04 tff(c_11206, plain, (iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdf_List)=true)). % 28.98/18.04 tff(c_1873, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdf__2), true)=true))). % 28.98/18.04 tff(c_11130, plain, (iext(uri_rdf_type, uri_rdfs_Literal, uri_rdfs_Class)=true)). % 28.98/18.04 tff(c_11083, plain, (iext(uri_rdf_type, uri_rdf_Bag, uri_rdfs_Class)=true)). % 28.98/18.04 tff(c_11036, plain, (iext(uri_rdf_type, uri_rdfs_Container, uri_rdfs_Class)=true)). % 28.98/18.04 tff(c_10960, plain, (iext(uri_rdf_type, uri_rdf_XMLLiteral, uri_rdfs_Class)=true)). % 28.98/18.04 tff(c_10913, plain, (iext(uri_rdf_type, uri_rdf_Alt, uri_rdfs_Class)=true)). % 28.98/18.04 tff(c_10865, plain, (iext(uri_rdf_type, uri_rdfs_Seq, uri_rdfs_Class)=true)). % 28.98/18.04 tff(c_10817, plain, (iext(uri_rdf_type, uri_rdfs_Datatype, uri_rdfs_Class)=true)). % 28.98/18.04 tff(c_10769, plain, (iext(uri_rdf_type, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Class)=true)). % 28.98/18.04 tff(c_10720, plain, (iext(uri_rdf_type, uri_rdfs_Class, uri_rdfs_Class)=true)). % 28.98/18.04 tff(c_2226, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_97), true, icext(C_97, uri_rdfs_Resource), true)=true))). % 28.98/18.04 tff(c_10637, plain, (iext(uri_rdf_type, uri_rdf_List, uri_rdfs_Class)=true)). % 28.98/18.04 tff(c_1191, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_range, S_5, O_6), true, true, true)=true))). % 28.98/18.04 tff(c_10466, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Seq)=true)). % 28.98/18.04 tff(c_10323, plain, (icext(uri_rdf_Property, uri_rdfs_isDefinedBy)=true)). % 28.98/18.04 tff(c_1878, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdf__1), true)=true))). % 28.98/18.04 tff(c_10241, plain, (iext(uri_rdf_type, uri_rdfs_isDefinedBy, uri_rdf_Property)=true)). % 28.98/18.04 tff(c_10176, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__2, uri_rdf__2)=true)). % 28.98/18.04 tff(c_2244, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_97), true, icext(C_97, uri_rdf_List), true)=true))). % 28.98/18.04 tff(c_10082, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_seeAlso, uri_rdfs_seeAlso)=true)). % 28.98/18.04 tff(c_10025, plain, (iext(uri_rdf_type, uri_rdfs_range, uri_rdf_Property)=true)). % 28.98/18.04 tff(c_1864, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_93), true, icext(C_93, uri_rdf_XMLLiteral), true)=true))). % 28.98/18.04 tff(c_9875, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdfs_Resource)=true)). % 28.98/18.04 tff(c_9810, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__3, uri_rdfs_member)=true)). % 28.98/18.04 tff(c_9738, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdf_XMLLiteral)=true)). % 28.98/18.04 tff(c_1892, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf_subject), true)=true))). % 28.98/18.04 tff(c_2958, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_subPropertyOf, S_5, O_6), true, true, true)=true))). % 28.98/18.04 tff(c_9445, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_range, uri_rdfs_range)=true)). % 28.98/18.04 tff(c_3049, plain, (![S_5, O_6]: (ifeq(iext(uri_rdf_rest, S_5, O_6), true, true, true)=true))). % 28.98/18.04 tff(c_2215, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_97), true, icext(C_97, uri_rdf_Property), true)=true))). % 28.98/18.04 tff(c_9225, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Resource)=true)). % 28.98/18.04 tff(c_1924, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdf_rest), true)=true))). % 28.98/18.04 tff(c_8968, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_object, uri_rdf_object)=true)). % 28.98/18.04 tff(c_8817, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdfs_ContainerMembershipProperty)=true)). % 28.98/18.04 tff(c_8694, plain, (ic(uri_rdf_List)=true)). % 28.98/18.04 tff(c_8643, plain, (icext(uri_rdfs_Class, uri_rdf_List)=true)). % 28.98/18.04 tff(c_2222, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdf_List), true)=true))). % 28.98/18.04 tff(c_1280, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_subClassOf, S_5, O_6), true, true, true)=true))). % 28.98/18.04 tff(c_8193, plain, (icext(uri_rdf_Property, uri_rdfs_subClassOf)=true)). % 28.98/18.04 tff(c_8139, plain, (iext(uri_rdf_type, uri_rdfs_subClassOf, uri_rdf_Property)=true)). % 28.98/18.04 tff(c_1904, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf_rest), true)=true))). % 28.98/18.04 tff(c_8045, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Resource)=true)). % 28.98/18.04 tff(c_7980, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, uri_rdfs_subClassOf)=true)). % 28.98/18.04 tff(c_7919, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_rest, uri_rdf_rest)=true)). % 28.98/18.04 tff(c_2239, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_97), true, icext(C_97, uri_rdfs_Class), true)=true))). % 28.98/18.04 tff(c_7826, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_subject, uri_rdf_subject)=true)). % 28.98/18.04 tff(c_7779, plain, (icext(uri_rdf_Property, uri_rdfs_seeAlso)=true)). % 28.98/18.04 tff(c_7724, plain, (iext(uri_rdf_type, uri_rdfs_seeAlso, uri_rdf_Property)=true)). % 28.98/18.04 tff(c_7659, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Datatype)=true)). % 28.98/18.04 tff(c_7502, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf)=true)). % 28.98/18.04 tff(c_2224, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdfs_Class), true)=true))). % 28.98/18.04 tff(c_7408, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__3, uri_rdf__3)=true)). % 28.98/18.04 tff(c_7324, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__1, uri_rdf__1)=true)). % 28.98/18.04 tff(c_7194, plain, (icext(uri_rdf_Property, uri_rdfs_domain)=true)). % 28.98/18.04 tff(c_7140, plain, (iext(uri_rdf_type, uri_rdfs_domain, uri_rdf_Property)=true)). % 28.98/18.04 tff(c_1900, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_93), true, icext(C_93, uri_rdf_Alt), true)=true))). % 28.98/18.04 tff(c_2199, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_97), true, icext(C_97, uri_rdfs_Class), true)=true))). % 28.98/18.04 tff(c_6782, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Resource)=true)). % 28.98/18.04 tff(c_6700, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Resource)=true)). % 28.98/18.04 tff(c_2221, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_97), true, icext(C_97, uri_rdfs_Datatype), true)=true))). % 28.98/18.04 tff(c_6606, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Container, uri_rdfs_Container)=true)). % 28.98/18.04 tff(c_6528, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdf_Bag)=true)). % 28.98/18.04 tff(c_2183, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdfs_Resource), true)=true))). % 28.98/18.04 tff(c_6409, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Container, uri_rdfs_Resource)=true)). % 28.98/18.04 tff(c_6345, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_first, uri_rdf_first)=true)). % 28.98/18.04 tff(c_6228, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__1, uri_rdfs_member)=true)). % 28.98/18.04 tff(c_6099, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdfs_Class)=true)). % 28.98/18.04 tff(c_1913, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdf_first), true)=true))). % 28.98/18.04 tff(c_5976, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, uri_rdfs_isDefinedBy)=true)). % 28.98/18.04 tff(c_1866, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf_value), true)=true))). % 28.98/18.04 tff(c_5886, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_type, uri_rdf_type)=true)). % 28.98/18.04 tff(c_5823, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdf_Property)=true)). % 28.98/18.04 tff(c_5664, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdfs_Resource)=true)). % 28.98/18.04 tff(c_1125, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_domain, S_5, O_6), true, true, true)=true))). % 28.98/18.04 tff(c_5494, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, uri_rdfs_domain)=true)). % 28.98/18.04 tff(c_5432, plain, (icext(uri_rdf_Property, uri_rdfs_range)=true)). % 28.98/18.04 tff(c_1890, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_range), true)=true))). % 28.98/18.04 tff(c_5262, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdfs_Literal)=true)). % 28.98/18.05 tff(c_1575, plain, (![X_90]: (ifeq(icext(uri_rdfs_ContainerMembershipProperty, X_90), true, icext(uri_rdf_Property, X_90), true)=true))). % 28.98/18.05 tff(c_5193, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Resource)=true)). % 28.98/18.05 tff(c_5108, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdf_Alt)=true)). % 28.98/18.05 tff(c_1572, plain, (![X_90]: (ifeq(icext(uri_rdf_Alt, X_90), true, icext(uri_rdfs_Container, X_90), true)=true))). % 28.98/18.05 tff(c_2931, plain, (![S_5, O_6]: (ifeq(iext(uri_rdf_object, S_5, O_6), true, true, true)=true))). % 28.98/18.05 tff(c_5056, plain, (ip(uri_rdfs_member)=true)). % 28.98/18.05 tff(c_4989, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__2, uri_rdfs_member)=true)). % 28.98/18.05 tff(c_1573, plain, (![X_90]: (ifeq(icext(uri_rdfs_Seq, X_90), true, icext(uri_rdfs_Container, X_90), true)=true))). % 28.98/18.05 tff(c_4928, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_value, uri_rdf_value)=true)). % 28.98/18.05 tff(c_4888, plain, (icext(uri_rdf_Property, uri_rdfs_subPropertyOf)=true)). % 28.98/18.05 tff(c_4827, plain, (iext(uri_rdf_type, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 28.98/18.05 tff(c_1574, plain, (![X_90]: (ifeq(icext(uri_rdf_Bag, X_90), true, icext(uri_rdfs_Container, X_90), true)=true))). % 28.98/18.05 tff(c_4754, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Resource)=true)). % 28.98/18.05 tff(c_1571, plain, (![X_90]: (ifeq(icext(uri_rdf_XMLLiteral, X_90), true, icext(uri_rdfs_Literal, X_90), true)=true))). % 28.98/18.05 tff(c_4674, plain, (icext(uri_rdfs_Class, uri_rdfs_Resource)=true)). % 28.98/18.05 tff(c_1576, plain, (![X_90]: (ifeq(icext(uri_rdfs_Datatype, X_90), true, icext(uri_rdfs_Class, X_90), true)=true))). % 28.98/18.05 tff(c_4547, plain, (ic(uri_rdfs_Resource)=true)). % 28.98/18.05 tff(c_4486, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdfs_Resource)=true)). % 28.98/18.05 tff(c_2201, plain, (![X_98, Y_99]: (ifeq(iext(uri_rdfs_isDefinedBy, X_98, Y_99), true, true, true)=true))). % 28.98/18.05 tff(c_4424, plain, (![X_136]: (iext(uri_rdf_type, X_136, uri_rdfs_Resource)=true))). % 28.98/18.05 tff(c_1925, plain, (![X_94, Y_95]: (ifeq(iext(uri_rdfs_label, X_94, Y_95), true, true, true)=true))). % 28.98/18.05 tff(c_1887, plain, (![X_94, Y_95]: (ifeq(iext(uri_rdfs_comment, X_94, Y_95), true, true, true)=true))). % 28.98/18.05 tff(c_2233, plain, (![X_98, Y_99]: (ifeq(iext(uri_rdf_first, X_98, Y_99), true, true, true)=true))). % 28.98/18.05 tff(c_1876, plain, (![X_94, Y_95]: (ifeq(iext(uri_rdf__1, X_94, Y_95), true, true, true)=true))). % 28.98/18.05 tff(c_1898, plain, (![X_94, Y_95]: (ifeq(iext(uri_rdf_type, X_94, Y_95), true, true, true)=true))). % 28.98/18.05 tff(c_2229, plain, (![X_98, Y_99]: (ifeq(iext(uri_rdf_subject, X_98, Y_99), true, true, true)=true))). % 28.98/18.05 tff(c_2205, plain, (![X_98, Y_99]: (ifeq(iext(uri_rdf_predicate, X_98, Y_99), true, true, true)=true))). % 28.98/18.05 tff(c_2190, plain, (![X_98, Y_99]: (ifeq(iext(uri_rdf__2, X_98, Y_99), true, true, true)=true))). % 28.98/18.05 tff(c_2197, plain, (![X_98, Y_99]: (ifeq(iext(uri_rdf__3, X_98, Y_99), true, true, true)=true))). % 28.98/18.05 tff(c_4246, plain, (icext(uri_rdfs_Class, uri_rdfs_Container)=true)). % 28.98/18.05 tff(c_4200, plain, (icext(uri_rdfs_Class, uri_rdfs_Literal)=true)). % 28.98/18.05 tff(c_4148, plain, (icext(uri_rdfs_Class, uri_rdf_Alt)=true)). % 28.98/18.05 tff(c_2246, plain, (![X_98, Y_99]: (ifeq(iext(uri_rdfs_seeAlso, X_98, Y_99), true, true, true)=true))). % 28.98/18.05 tff(c_4104, plain, (icext(uri_rdfs_Class, uri_rdf_Bag)=true)). % 28.98/18.05 tff(c_4059, plain, (icext(uri_rdfs_Class, uri_rdfs_Datatype)=true)). % 28.98/18.05 tff(c_4008, plain, (icext(uri_rdfs_Class, uri_rdfs_ContainerMembershipProperty)=true)). % 28.98/18.05 tff(c_3963, plain, (icext(uri_rdfs_Class, uri_rdf_XMLLiteral)=true)). % 28.98/18.05 tff(c_3913, plain, (icext(uri_rdfs_Class, uri_rdfs_Seq)=true)). % 28.98/18.05 tff(c_2225, plain, (![X_98, Y_99]: (ifeq(iext(uri_rdfs_member, X_98, Y_99), true, true, true)=true))). % 28.98/18.05 tff(c_3864, plain, (icext(uri_rdfs_Class, uri_rdfs_Class)=true)). % 28.98/18.05 tff(c_1865, plain, (![X_94, Y_95]: (ifeq(iext(uri_rdf_value, X_94, Y_95), true, true, true)=true))). % 28.98/18.05 tff(c_3796, plain, (icext(uri_rdf_Property, uri_rdf_first)=true)). % 28.98/18.05 tff(c_3753, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__1)=true)). % 28.98/18.05 tff(c_3714, plain, (icext(uri_rdf_Property, uri_rdf__2)=true)). % 28.98/18.05 tff(c_3674, plain, (icext(uri_rdf_List, uri_rdf_nil)=true)). % 28.98/18.05 tff(c_3632, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__2)=true)). % 28.98/18.05 tff(c_3593, plain, (icext(uri_rdf_Property, uri_rdf_type)=true)). % 28.98/18.05 tff(c_3554, plain, (icext(uri_rdf_Property, uri_rdf_object)=true)). % 28.98/18.05 tff(c_3505, plain, (icext(uri_rdfs_Class, uri_rdf_Property)=true)). % 28.98/18.05 tff(c_3462, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__3)=true)). % 28.98/18.05 tff(c_3418, plain, (icext(uri_rdfs_Datatype, uri_rdf_XMLLiteral)=true)). % 28.98/18.05 tff(c_3375, plain, (icext(uri_rdf_Property, uri_rdf_rest)=true)). % 28.98/18.05 tff(c_3338, plain, (icext(uri_rdf_Property, uri_rdf_value)=true)). % 28.98/18.05 tff(c_3297, plain, (icext(uri_rdf_Property, uri_rdf__1)=true)). % 28.98/18.05 tff(c_3252, plain, (icext(uri_rdf_Property, uri_rdf__3)=true)). % 28.98/18.05 tff(c_3211, plain, (icext(uri_rdf_Property, uri_rdf_subject)=true)). % 28.98/18.05 tff(c_3150, plain, (ip(uri_rdf_subject)=true)). % 28.98/18.05 tff(c_3111, plain, (ip(uri_rdf_value)=true)). % 28.98/18.05 tff(c_3074, plain, (ic(uri_rdf_XMLLiteral)=true)). % 28.98/18.05 tff(c_3031, plain, (ip(uri_rdf_rest)=true)). % 28.98/18.05 tff(c_2988, plain, (ip(uri_rdf__2)=true)). % 28.98/18.05 tff(c_2914, plain, (ip(uri_rdfs_subPropertyOf)=true)). % 28.98/18.05 tff(c_2904, plain, (ip(uri_rdf_object)=true)). % 28.98/18.05 tff(c_2866, plain, (ic(uri_rdf_Property)=true)). % 28.98/18.05 tff(c_2386, plain, (ip(uri_rdf_first)=true)). % 28.98/18.05 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))). % 28.98/18.05 tff(c_2345, plain, (ip(uri_rdf__1)=true)). % 28.98/18.05 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))). % 28.98/18.05 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))). % 28.98/18.05 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))). % 28.98/18.05 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))). % 28.98/18.05 tff(c_1582, plain, (ic(uri_rdfs_Datatype)=true)). % 28.98/18.05 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))). % 28.98/18.05 tff(c_1450, plain, (ip(uri_rdf__3)=true)). % 28.98/18.05 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))). % 28.98/18.05 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))). % 28.98/18.05 tff(c_1399, plain, (ip(uri_rdf_type)=true)). % 28.98/18.05 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))). % 28.98/18.05 tff(c_1356, plain, (ic(uri_rdf_Alt)=true)). % 28.98/18.05 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))). % 28.98/18.05 tff(c_1265, plain, (ip(uri_rdfs_subClassOf)=true)). % 28.98/18.05 tff(c_30, plain, (![P_10]: (ifeq(iext(uri_rdf_type, P_10, uri_rdf_Property), true, ip(P_10), true)=true))). % 28.98/18.05 tff(c_1179, plain, (ip(uri_rdfs_range)=true)). % 28.98/18.05 tff(c_58, plain, (![C_15]: (ifeq(ic(C_15), true, iext(uri_rdfs_subClassOf, C_15, uri_rdfs_Resource), true)=true))). % 28.98/18.05 tff(c_1113, plain, (ip(uri_rdfs_domain)=true)). % 28.98/18.05 tff(c_156, plain, (![C_39]: (ifeq(ic(C_39), true, iext(uri_rdfs_subClassOf, C_39, C_39), true)=true))). % 28.98/18.05 tff(c_1056, plain, (ip(uri_rdfs_seeAlso)=true)). % 28.98/18.05 tff(c_1027, plain, (ic(uri_rdfs_Seq)=true)). % 28.98/18.05 tff(c_4, plain, (![P_4, S_5, O_6]: (ifeq(iext(P_4, S_5, O_6), true, ip(P_4), true)=true))). % 28.98/18.05 tff(c_784, plain, (ic(uri_rdfs_ContainerMembershipProperty)=true)). % 28.98/18.05 tff(c_170, plain, (![P_51]: (ifeq(ip(P_51), true, iext(uri_rdfs_subPropertyOf, P_51, P_51), true)=true))). % 28.98/18.05 tff(c_751, plain, (ic(uri_rdf_Bag)=true)). % 28.98/18.05 tff(c_162, plain, (![P_43, Q_44]: (ifeq(iext(uri_rdfs_subPropertyOf, P_43, Q_44), true, ip(Q_44), true)=true))). % 28.98/18.05 tff(c_152, plain, (![C_37, D_38]: (ifeq(iext(uri_rdfs_subClassOf, C_37, D_38), true, ic(C_37), true)=true))). % 28.98/18.05 tff(c_657, plain, (ip(uri_rdfs_isDefinedBy)=true)). % 28.98/18.05 tff(c_631, plain, (ic(uri_rdfs_Class)=true)). % 28.98/18.05 tff(c_164, plain, (![P_45, Q_46]: (ifeq(iext(uri_rdfs_subPropertyOf, P_45, Q_46), true, ip(P_45), true)=true))). % 28.98/18.05 tff(c_595, plain, (ic(uri_rdfs_Container)=true)). % 28.98/18.05 tff(c_28, plain, (![P_9]: (ifeq(ip(P_9), true, iext(uri_rdf_type, P_9, uri_rdf_Property), true)=true))). % 28.98/18.05 tff(c_535, plain, (ic(uri_rdfs_Literal)=true)). % 28.98/18.05 tff(c_150, plain, (![C_35, D_36]: (ifeq(iext(uri_rdfs_subClassOf, C_35, D_36), true, ic(D_36), true)=true))). % 28.98/18.05 tff(c_116, plain, (![X_23]: (ifeq(icext(uri_rdfs_Class, X_23), true, ic(X_23), true)=true))). % 28.98/18.05 tff(c_114, plain, (![X_22]: (ifeq(ic(X_22), true, icext(uri_rdfs_Class, X_22), true)=true))). % 28.98/18.05 tff(c_124, plain, (![X_27]: (ifeq(lv(X_27), true, icext(uri_rdfs_Literal, X_27), true)=true))). % 28.98/18.05 tff(c_459, plain, (![X_61]: (icext(uri_rdfs_Resource, X_61)=true))). % 28.98/18.05 tff(c_122, plain, (![X_26]: (ifeq(icext(uri_rdfs_Literal, X_26), true, lv(X_26), true)=true))). % 28.98/18.05 tff(c_187, plain, (![X_8]: (ifeq(lv(X_8), true, true, true)=true))). % 28.98/18.05 tff(c_2, plain, (![A_1, B_2, C_3]: (ifeq(A_1, A_1, B_2, C_3)=B_2))). % 28.98/18.05 tff(c_180, plain, (iext(uri_rdfs_range, uri_rdf_value, uri_rdfs_Resource)=true)). % 28.98/18.05 tff(c_40, plain, (iext(uri_rdfs_domain, uri_rdfs_isDefinedBy, uri_rdfs_Resource)=true)). % 28.98/18.05 tff(c_100, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Literal)=true)). % 28.98/18.05 tff(c_178, plain, (iext(uri_rdfs_domain, uri_rdf_value, uri_rdfs_Resource)=true)). % 28.98/18.05 tff(c_134, plain, (iext(uri_rdfs_domain, uri_rdf_object, uri_rdfs_Statement)=true)). % 28.98/18.05 tff(c_84, plain, (iext(uri_rdfs_domain, uri_rdf__3, uri_rdfs_Resource)=true)). % 28.98/18.05 tff(c_138, plain, (iext(uri_rdfs_domain, uri_rdf_predicate, uri_rdfs_Statement)=true)). % 28.98/18.05 tff(c_82, plain, (iext(uri_rdfs_domain, uri_rdf__2, uri_rdfs_Resource)=true)). % 28.98/18.05 tff(c_88, plain, (iext(uri_rdfs_range, uri_rdf__2, uri_rdfs_Resource)=true)). % 28.98/18.05 tff(c_12, plain, (iext(uri_rdf_type, uri_rdf_nil, uri_rdf_List)=true)). % 28.98/18.05 tff(c_160, plain, (iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 28.98/18.05 tff(c_80, plain, (iext(uri_rdfs_domain, uri_rdf__1, uri_rdfs_Resource)=true)). % 28.98/18.05 tff(c_86, plain, (iext(uri_rdfs_range, uri_rdf__1, uri_rdfs_Resource)=true)). % 28.98/18.05 tff(c_90, plain, (iext(uri_rdfs_range, uri_rdf__3, uri_rdfs_Resource)=true)). % 28.98/18.05 tff(c_132, plain, (iext(uri_rdfs_range, uri_rdfs_range, uri_rdfs_Class)=true)). % 28.98/18.05 tff(c_76, plain, (iext(uri_rdfs_domain, uri_rdfs_member, uri_rdfs_Resource)=true)). % 28.98/18.05 tff(c_42, plain, (iext(uri_rdfs_range, uri_rdfs_isDefinedBy, uri_rdfs_Resource)=true)). % 28.98/18.05 tff(c_14, plain, (iext(uri_rdf_type, uri_rdf_rest, uri_rdf_Property)=true)). % 28.98/18.05 tff(c_94, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdfs_ContainerMembershipProperty)=true)). % 28.98/18.05 tff(c_140, plain, (iext(uri_rdfs_range, uri_rdf_predicate, uri_rdfs_Resource)=true)). % 28.98/18.05 tff(c_36, plain, (iext(uri_rdfs_domain, uri_rdfs_comment, uri_rdfs_Resource)=true)). % 28.98/18.05 tff(c_44, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso)=true)). % 28.98/18.05 tff(c_128, plain, (iext(uri_rdfs_domain, uri_rdfs_range, uri_rdf_Property)=true)). % 28.98/18.05 tff(c_22, plain, (iext(uri_rdf_type, uri_rdf_object, uri_rdf_Property)=true)). % 28.98/18.05 tff(c_142, plain, (iext(uri_rdfs_domain, uri_rdf_subject, uri_rdfs_Statement)=true)). % 28.98/18.05 tff(c_112, plain, (iext(uri_rdfs_range, uri_rdfs_domain, uri_rdfs_Class)=true)). % 28.98/18.05 tff(c_34, plain, (iext(uri_rdf_type, uri_rdf_type, uri_rdf_Property)=true)). % 28.98/18.05 tff(c_92, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdfs_ContainerMembershipProperty)=true)). % 28.98/18.05 tff(c_24, plain, (iext(uri_rdf_type, uri_rdf_value, uri_rdf_Property)=true)). % 28.98/18.05 tff(c_38, plain, (iext(uri_rdfs_range, uri_rdfs_comment, uri_rdfs_Literal)=true)). % 28.98/18.05 tff(c_174, plain, (iext(uri_rdfs_domain, uri_rdf_type, uri_rdfs_Resource)=true)). % 28.98/18.05 tff(c_68, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Container)=true)). % 28.98/18.05 tff(c_154, plain, (iext(uri_rdfs_range, uri_rdfs_subClassOf, uri_rdfs_Class)=true)). % 28.98/18.05 tff(c_96, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdfs_ContainerMembershipProperty)=true)). % 28.98/18.05 tff(c_102, plain, (iext(uri_rdf_type, uri_rdf_XMLLiteral, uri_rdfs_Datatype)=true)). % 28.98/18.05 tff(c_64, plain, (iext(uri_rdfs_domain, uri_rdf_rest, uri_rdf_List)=true)). % 28.98/18.05 tff(c_98, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Container)=true)). % 28.98/18.05 tff(c_146, plain, (iext(uri_rdfs_domain, uri_rdfs_subClassOf, uri_rdfs_Class)=true)). % 28.98/18.05 tff(c_78, plain, (iext(uri_rdfs_range, uri_rdfs_member, uri_rdfs_Resource)=true)). % 28.98/18.05 tff(c_26, plain, (iext(uri_rdf_type, uri_rdf_subject, uri_rdf_Property)=true)). % 28.98/18.05 tff(c_60, plain, (iext(uri_rdfs_domain, uri_rdf_first, uri_rdf_List)=true)). % 28.98/18.05 tff(c_144, plain, (iext(uri_rdfs_range, uri_rdf_subject, uri_rdfs_Resource)=true)). % 28.98/18.05 tff(c_108, plain, (iext(uri_rdfs_domain, uri_rdfs_domain, uri_rdf_Property)=true)). % 28.98/18.05 tff(c_126, plain, (iext(uri_rdf_type, uri_rdf_Property, uri_rdfs_Class)=true)). % 28.98/18.05 tff(c_62, plain, (iext(uri_rdfs_range, uri_rdf_first, uri_rdfs_Resource)=true)). % 28.98/18.05 tff(c_70, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Container)=true)). % 28.98/18.05 tff(c_74, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property)=true)). % 28.98/18.05 tff(c_18, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdf_Property)=true)). % 28.98/18.05 tff(c_16, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdf_Property)=true)). % 28.98/18.05 tff(c_106, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Class)=true)). % 28.98/18.05 tff(c_50, plain, (iext(uri_rdfs_domain, uri_rdfs_seeAlso, uri_rdfs_Resource)=true)). % 28.98/18.05 tff(c_20, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdf_Property)=true)). % 28.98/18.05 tff(c_10, plain, (iext(uri_rdf_type, uri_rdf_first, uri_rdf_Property)=true)). % 28.98/18.05 tff(c_48, plain, (iext(uri_rdfs_range, uri_rdfs_label, uri_rdfs_Literal)=true)). % 28.98/18.05 tff(c_66, plain, (iext(uri_rdfs_range, uri_rdf_rest, uri_rdf_List)=true)). % 28.98/18.05 tff(c_46, plain, (iext(uri_rdfs_domain, uri_rdfs_label, uri_rdfs_Resource)=true)). % 28.98/18.05 tff(c_52, plain, (iext(uri_rdfs_range, uri_rdfs_seeAlso, uri_rdfs_Resource)=true)). % 28.98/18.05 tff(c_168, plain, (iext(uri_rdfs_range, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 28.98/18.05 tff(c_176, plain, (iext(uri_rdfs_range, uri_rdf_type, uri_rdfs_Class)=true)). % 28.98/18.05 tff(c_182, plain, (iext(uri_owl_sameAs, uri_owl_sameAs, uri_owl_sameAs)!=true)). % 28.98/18.05 tff(c_6, plain, (![X_7]: (ir(X_7)=true))). % 28.98/18.05 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 28.98/18.05 %------------------------------------------------------------------------------