%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SWB004-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/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n015.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Apr 9 09:15:44 PM UTC 2025 % Result : Satisfiable 26.67s 17.04s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.09/0.13 % Problem : SWB004-10 : TPTP v9.0.0. Released v7.3.0. % 0.09/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.13/0.34 % Computer : n015.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Wed Apr 9 00:52:20 EDT 2025 % 0.13/0.35 % CPUTime : % 26.67/17.04 % 26.67/17.04 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 26.67/17.04 % 26.67/17.04 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 26.67/17.06 %$ tuple > 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_equivalentClass > uri_owl_Thing > uri_owl_Class > true % 26.67/17.06 % 26.67/17.06 %Foreground sorts: % 26.67/17.06 % 26.67/17.06 % 26.67/17.06 %Background operators: % 26.67/17.06 % 26.67/17.06 % 26.67/17.06 %Foreground operators: % 26.67/17.06 tff(uri_rdfs_Datatype, type, uri_rdfs_Datatype: $i). % 26.67/17.06 tff(uri_rdfs_ContainerMembershipProperty, type, uri_rdfs_ContainerMembershipProperty: $i). % 26.67/17.06 tff(uri_rdfs_Resource, type, uri_rdfs_Resource: $i). % 26.67/17.06 tff(uri_rdf_Property, type, uri_rdf_Property: $i). % 26.67/17.06 tff(uri_rdf_subject, type, uri_rdf_subject: $i). % 26.67/17.06 tff(uri_owl_equivalentClass, type, uri_owl_equivalentClass: $i). % 26.67/17.06 tff(uri_rdf_type, type, uri_rdf_type: $i). % 26.67/17.06 tff(uri_rdfs_subPropertyOf, type, uri_rdfs_subPropertyOf: $i). % 26.67/17.06 tff(uri_rdfs_seeAlso, type, uri_rdfs_seeAlso: $i). % 26.67/17.06 tff(icext, type, icext: ($i * $i) > $i). % 26.67/17.06 tff(uri_rdfs_range, type, uri_rdfs_range: $i). % 26.67/17.06 tff(uri_rdf_XMLLiteral, type, uri_rdf_XMLLiteral: $i). % 26.67/17.06 tff(uri_rdf_List, type, uri_rdf_List: $i). % 26.67/17.06 tff(uri_rdf_first, type, uri_rdf_first: $i). % 26.67/17.06 tff(uri_rdf_predicate, type, uri_rdf_predicate: $i). % 26.67/17.06 tff(ir, type, ir: $i > $i). % 26.67/17.06 tff(lv, type, lv: $i > $i). % 26.67/17.06 tff(uri_owl_Thing, type, uri_owl_Thing: $i). % 26.67/17.06 tff(uri_rdf__3, type, uri_rdf__3: $i). % 26.67/17.06 tff(uri_rdf_value, type, uri_rdf_value: $i). % 26.67/17.06 tff(ic, type, ic: $i > $i). % 26.67/17.06 tff(uri_rdfs_Statement, type, uri_rdfs_Statement: $i). % 26.67/17.06 tff(uri_rdf__1, type, uri_rdf__1: $i). % 26.67/17.06 tff(iext, type, iext: ($i * $i * $i) > $i). % 26.67/17.06 tff(uri_rdf_rest, type, uri_rdf_rest: $i). % 26.67/17.06 tff(uri_rdfs_label, type, uri_rdfs_label: $i). % 26.67/17.06 tff(uri_rdfs_Container, type, uri_rdfs_Container: $i). % 26.67/17.06 tff(uri_rdfs_subClassOf, type, uri_rdfs_subClassOf: $i). % 26.67/17.06 tff(uri_rdf_object, type, uri_rdf_object: $i). % 26.67/17.06 tff(ip, type, ip: $i > $i). % 26.67/17.06 tff(uri_rdfs_Class, type, uri_rdfs_Class: $i). % 26.67/17.06 tff(uri_rdfs_Seq, type, uri_rdfs_Seq: $i). % 26.67/17.06 tff(uri_owl_Class, type, uri_owl_Class: $i). % 26.67/17.06 tff(uri_rdfs_member, type, uri_rdfs_member: $i). % 26.67/17.06 tff(uri_rdf_Bag, type, uri_rdf_Bag: $i). % 26.67/17.06 tff(uri_rdf__2, type, uri_rdf__2: $i). % 26.67/17.06 tff(uri_rdfs_comment, type, uri_rdfs_comment: $i). % 26.67/17.06 tff(uri_rdfs_Literal, type, uri_rdfs_Literal: $i). % 26.67/17.06 tff(true, type, true: $i). % 26.67/17.06 tff(uri_rdf_Alt, type, uri_rdf_Alt: $i). % 26.67/17.06 tff(uri_rdf_nil, type, uri_rdf_nil: $i). % 26.67/17.06 tff(tuple, type, tuple: ($i * $i * $i * $i * $i) > $i). % 26.67/17.06 tff(uri_rdfs_isDefinedBy, type, uri_rdfs_isDefinedBy: $i). % 26.67/17.06 tff(uri_rdfs_domain, type, uri_rdfs_domain: $i). % 26.67/17.06 tff(ifeq, type, ifeq: ($i * $i * $i * $i) > $i). % 26.67/17.06 % 26.67/17.06 %Saturated clause set: % 26.67/17.06 tff(c_11874, 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))). % 26.67/17.06 tff(c_58986, plain, (![X_1105, Y_1106]: (ifeq(iext(uri_rdfs_label, X_1105, Y_1106), true, iext(uri_rdfs_label, X_1105, Y_1106), true)=true))). % 26.67/17.06 tff(c_11666, 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))). % 26.67/17.06 tff(c_58848, plain, (![X_1100, Y_1101]: (ifeq(iext(uri_rdf_predicate, X_1100, Y_1101), true, iext(uri_rdf_predicate, X_1100, Y_1101), true)=true))). % 26.67/17.06 tff(c_11731, 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))). % 26.67/17.06 tff(c_11796, 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))). % 26.67/17.06 tff(c_58599, plain, (![X_1094, Y_1095]: (ifeq(iext(uri_rdfs_comment, X_1094, Y_1095), true, iext(uri_rdfs_comment, X_1094, Y_1095), true)=true))). % 26.67/17.06 tff(c_4839, 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))). % 26.67/17.06 tff(c_11492, 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))). % 26.67/17.06 tff(c_11589, 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))). % 26.67/17.06 tff(c_4836, 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))). % 26.67/17.06 tff(c_57972, plain, (![X_1084, Y_1085]: (ifeq(iext(uri_rdfs_member, X_1084, Y_1085), true, iext(uri_rdfs_member, X_1084, Y_1085), true)=true))). % 26.67/17.06 tff(c_11391, 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))). % 26.67/17.06 tff(c_11300, 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))). % 26.67/17.06 tff(c_13210, 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))). % 26.67/17.06 tff(c_57496, plain, (![C_1079]: (ifeq(iext(uri_rdfs_subClassOf, C_1079, uri_rdf_List), true, iext(uri_rdfs_subClassOf, C_1079, uri_rdfs_Resource), true)=true))). % 26.67/17.06 tff(c_13090, 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))). % 26.67/17.06 tff(c_57242, plain, (![C_1076]: (ifeq(iext(uri_rdfs_subClassOf, C_1076, uri_rdfs_Statement), true, iext(uri_rdfs_subClassOf, C_1076, uri_rdfs_Resource), true)=true))). % 26.67/17.06 tff(c_9513, 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))). % 26.67/17.06 tff(c_6689, 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))). % 26.67/17.06 tff(c_11069, 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))). % 26.67/17.06 tff(c_8067, 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))). % 26.67/17.06 tff(c_8064, 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))). % 26.67/17.07 tff(c_5461, 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))). % 26.67/17.07 tff(c_11243, 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))). % 26.67/17.07 tff(c_10946, 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))). % 26.67/17.07 tff(c_10899, 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))). % 26.67/17.07 tff(c_9975, 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))). % 26.67/17.07 tff(c_10993, 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))). % 26.67/17.07 tff(c_6686, 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))). % 26.67/17.07 tff(c_9972, 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))). % 26.67/17.07 tff(c_5458, 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))). % 26.67/17.07 tff(c_11163, 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))). % 26.67/17.07 tff(c_9510, 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))). % 26.67/17.07 tff(c_10780, 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))). % 26.67/17.07 tff(c_11116, 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))). % 26.67/17.07 tff(c_10827, 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))). % 26.67/17.07 tff(c_10580, 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))). % 26.67/17.07 tff(c_10533, 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))). % 26.67/17.07 tff(c_13031, 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))). % 26.67/17.07 tff(c_10142, 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))). % 26.67/17.07 tff(c_10197, 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))). % 26.67/17.07 tff(c_10680, 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))). % 26.67/17.07 tff(c_54288, plain, (![P_1039]: (ifeq(iext(uri_rdfs_subPropertyOf, P_1039, uri_rdf__3), true, iext(uri_rdfs_subPropertyOf, P_1039, uri_rdfs_member), true)=true))). % 26.67/17.07 tff(c_54141, plain, (![C_1037]: (ifeq(iext(uri_rdfs_subClassOf, C_1037, uri_rdf_Property), true, iext(uri_rdfs_subClassOf, C_1037, uri_rdfs_Resource), true)=true))). % 26.67/17.07 tff(c_53978, plain, (![C_1035]: (ifeq(iext(uri_rdfs_subClassOf, C_1035, uri_rdfs_Container), true, iext(uri_rdfs_subClassOf, C_1035, uri_rdfs_Resource), true)=true))). % 26.67/17.07 tff(c_8124, 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))). % 26.67/17.07 tff(c_4212, 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))). % 26.67/17.07 tff(c_4577, 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))). % 26.67/17.07 tff(c_3908, 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))). % 26.67/17.07 tff(c_53374, plain, (![C_1027]: (ifeq(iext(uri_rdfs_subClassOf, C_1027, uri_rdf_XMLLiteral), true, iext(uri_rdfs_subClassOf, C_1027, uri_rdfs_Resource), true)=true))). % 26.67/17.07 tff(c_7982, 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))). % 26.67/17.07 tff(c_4265, 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))). % 26.67/17.07 tff(c_6241, 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))). % 26.67/17.07 tff(c_3954, 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))). % 26.67/17.07 tff(c_3951, 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))). % 26.67/17.07 tff(c_8415, 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))). % 26.67/17.07 tff(c_5925, 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))). % 26.67/17.07 tff(c_9671, 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))). % 26.67/17.07 tff(c_52326, plain, (![X_1012, Y_1013]: (ifeq(iext(uri_rdf__3, X_1012, Y_1013), true, iext(uri_rdf__3, X_1012, Y_1013), true)=true))). % 26.67/17.07 tff(c_5144, 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))). % 26.67/17.07 tff(c_9918, 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))). % 26.67/17.07 tff(c_7264, 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))). % 26.67/17.07 tff(c_6556, 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))). % 26.67/17.07 tff(c_5003, 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))). % 26.67/17.07 tff(c_9394, 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))). % 26.67/17.07 tff(c_5603, 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))). % 26.67/17.07 tff(c_4306, 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))). % 26.67/17.07 tff(c_6978, 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))). % 26.67/17.07 tff(c_51276, plain, (![X_998, Y_999]: (ifeq(iext(uri_rdfs_isDefinedBy, X_998, Y_999), true, iext(uri_rdfs_isDefinedBy, X_998, Y_999), true)=true))). % 26.67/17.07 tff(c_51248, plain, (![X_994, Y_995]: (ifeq(iext(uri_rdf__1, X_994, Y_995), true, iext(uri_rdfs_member, X_994, Y_995), true)=true))). % 26.67/17.07 tff(c_8283, 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))). % 26.67/17.07 tff(c_3905, 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))). % 26.67/17.07 tff(c_50980, plain, (![X_987, Y_988]: (ifeq(iext(uri_rdf_rest, X_987, Y_988), true, iext(uri_rdf_rest, X_987, Y_988), true)=true))). % 26.67/17.07 tff(c_7929, 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))). % 26.67/17.07 tff(c_5706, 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))). % 26.67/17.07 tff(c_50729, plain, (![X_981, Y_982]: (ifeq(iext(uri_rdf__2, X_981, Y_982), true, iext(uri_rdf__2, X_981, Y_982), true)=true))). % 26.67/17.07 tff(c_4149, 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))). % 26.67/17.07 tff(c_50456, plain, (![C_977]: (ifeq(iext(uri_rdfs_subClassOf, C_977, uri_rdf_Bag), true, iext(uri_rdfs_subClassOf, C_977, uri_rdfs_Resource), true)=true))). % 26.67/17.07 tff(c_4516, 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))). % 26.67/17.08 tff(c_49826, plain, (![X_972, Y_973]: (ifeq(iext(uri_rdfs_subPropertyOf, X_972, Y_973), true, iext(uri_rdfs_subPropertyOf, X_972, Y_973), true)=true))). % 26.67/17.08 tff(c_49644, plain, (![P_969]: (ifeq(iext(uri_rdfs_subPropertyOf, P_969, uri_rdf__2), true, iext(uri_rdfs_subPropertyOf, P_969, uri_rdfs_member), true)=true))). % 26.67/17.08 tff(c_9819, 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))). % 26.67/17.08 tff(c_49505, plain, (![C_967]: (ifeq(iext(uri_rdfs_subClassOf, C_967, uri_rdf_Alt), true, iext(uri_rdfs_subClassOf, C_967, uri_rdfs_Resource), true)=true))). % 26.67/17.08 tff(c_48795, plain, (![X_962, Y_963]: (ifeq(iext(uri_rdf_type, X_962, Y_963), true, iext(uri_rdf_type, X_962, Y_963), true)=true))). % 26.67/17.08 tff(c_48722, plain, (![C_961]: (ifeq(iext(uri_rdfs_subClassOf, C_961, uri_rdfs_Literal), true, iext(uri_rdfs_subClassOf, C_961, uri_rdfs_Resource), true)=true))). % 26.67/17.08 tff(c_8801, 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))). % 26.67/17.08 tff(c_8348, 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))). % 26.67/17.08 tff(c_48183, plain, (![X_953, Y_954]: (ifeq(iext(uri_rdf__3, X_953, Y_954), true, iext(uri_rdfs_member, X_953, Y_954), true)=true))). % 26.67/17.08 tff(c_8869, 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))). % 26.67/17.08 tff(c_47660, plain, (![C_948]: (ifeq(iext(uri_rdfs_subClassOf, C_948, uri_rdfs_Datatype), true, iext(uri_rdfs_subClassOf, C_948, uri_rdfs_Resource), true)=true))). % 26.67/17.08 tff(c_4146, 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))). % 26.67/17.08 tff(c_9736, 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))). % 26.67/17.08 tff(c_6635, 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))). % 26.67/17.08 tff(c_4678, 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))). % 26.67/17.08 tff(c_6498, 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))). % 26.67/17.08 tff(c_5839, 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))). % 26.67/17.08 tff(c_8483, 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))). % 26.67/17.08 tff(c_8189, 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))). % 26.67/17.08 tff(c_7544, 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))). % 26.67/17.08 tff(c_4000, 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))). % 26.67/17.08 tff(c_4051, 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))). % 26.67/17.08 tff(c_45124, plain, (![C_924]: (ifeq(iext(uri_rdfs_subClassOf, C_924, uri_rdfs_Class), true, iext(uri_rdfs_subClassOf, C_924, uri_rdfs_Resource), true)=true))). % 26.67/17.08 tff(c_4309, 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))). % 26.67/17.08 tff(c_44671, plain, (![X_918, Y_919]: (ifeq(iext(uri_rdfs_domain, X_918, Y_919), true, iext(uri_rdfs_domain, X_918, Y_919), true)=true))). % 26.67/17.08 tff(c_7780, 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))). % 26.67/17.08 tff(c_4103, 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))). % 26.67/17.08 tff(c_8932, 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))). % 26.67/17.08 tff(c_44279, plain, (![X_910, Y_911]: (ifeq(iext(uri_rdf__2, X_910, Y_911), true, iext(uri_rdfs_member, X_910, Y_911), true)=true))). % 26.67/17.08 tff(c_44211, plain, (![P_908]: (ifeq(iext(uri_rdfs_subPropertyOf, P_908, uri_rdf__1), true, iext(uri_rdfs_subPropertyOf, P_908, uri_rdfs_member), true)=true))). % 26.67/17.08 tff(c_4100, 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))). % 26.67/17.08 tff(c_8579, 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))). % 26.67/17.08 tff(c_6887, 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))). % 26.67/17.08 tff(c_4262, 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))). % 26.67/17.08 tff(c_43436, plain, (![X_896, Y_897]: (ifeq(iext(uri_rdf__1, X_896, Y_897), true, iext(uri_rdf__1, X_896, Y_897), true)=true))). % 26.67/17.08 tff(c_43409, plain, (![X_892, Y_893]: (ifeq(iext(uri_rdfs_seeAlso, X_892, Y_893), true, iext(uri_rdfs_seeAlso, X_892, Y_893), true)=true))). % 26.67/17.08 tff(c_3997, 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))). % 26.67/17.08 tff(c_6134, 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))). % 26.67/17.08 tff(c_43033, plain, (![C_887]: (ifeq(iext(uri_rdfs_subClassOf, C_887, uri_rdfs_ContainerMembershipProperty), true, iext(uri_rdfs_subClassOf, C_887, uri_rdfs_Resource), true)=true))). % 26.67/17.08 tff(c_4048, 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))). % 26.67/17.08 tff(c_42879, plain, (![X_881, Y_882]: (ifeq(iext(uri_rdf_first, X_881, Y_882), true, iext(uri_rdf_first, X_881, Y_882), true)=true))). % 26.67/17.08 tff(c_9328, 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))). % 26.67/17.08 tff(c_4209, 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))). % 26.67/17.08 tff(c_6379, 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))). % 26.67/17.08 tff(c_5072, 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))). % 26.67/17.08 tff(c_42107, plain, (![X_872, Y_873]: (ifeq(iext(uri_rdfs_range, X_872, Y_873), true, iext(uri_rdfs_range, X_872, Y_873), true)=true))). % 26.67/17.08 tff(c_41804, plain, (![X_866, Y_867]: (ifeq(iext(uri_rdf_value, X_866, Y_867), true, iext(uri_rdf_value, X_866, Y_867), true)=true))). % 26.67/17.08 tff(c_5389, 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))). % 26.67/17.08 tff(c_9456, 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))). % 26.67/17.08 tff(c_41435, plain, (![C_862]: (ifeq(iext(uri_rdfs_subClassOf, C_862, uri_rdfs_Seq), true, iext(uri_rdfs_subClassOf, C_862, uri_rdfs_Resource), true)=true))). % 26.67/17.08 tff(c_9232, 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))). % 26.67/17.08 tff(c_41297, plain, (![X_857, Y_858]: (ifeq(iext(uri_rdf_object, X_857, Y_858), true, iext(uri_rdf_object, X_857, Y_858), true)=true))). % 26.67/17.08 tff(c_7043, 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))). % 26.67/17.08 tff(c_40606, plain, (![X_852, Y_853]: (ifeq(iext(uri_rdfs_subClassOf, X_852, Y_853), true, iext(uri_rdfs_subClassOf, X_852, Y_853), true)=true))). % 26.67/17.08 tff(c_40578, plain, (![X_848, Y_849]: (ifeq(iext(uri_rdf_subject, X_848, Y_849), true, iext(uri_rdf_subject, X_848, Y_849), true)=true))). % 26.67/17.08 tff(c_6027, 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))). % 26.67/17.08 tff(c_5781, 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))). % 26.67/17.08 tff(c_12829, 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))). % 26.67/17.08 tff(c_10319, 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))). % 26.91/17.08 tff(c_6796, 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))). % 26.91/17.08 tff(c_7678, 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))). % 26.91/17.08 tff(c_5778, 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))). % 26.91/17.08 tff(c_12826, 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))). % 26.91/17.08 tff(c_5504, 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))). % 26.91/17.08 tff(c_6799, 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))). % 26.91/17.08 tff(c_6317, 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))). % 26.91/17.08 tff(c_6314, 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))). % 26.91/17.09 tff(c_4441, plain, (![P_47, X_136]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, X_136, uri_rdfs_Resource), true, true, true), true)=true))). % 26.91/17.09 tff(c_7681, 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))). % 26.91/17.09 tff(c_10322, 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))). % 26.91/17.09 tff(c_5501, 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))). % 26.91/17.09 tff(c_3344, 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))). % 26.91/17.09 tff(c_3721, 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))). % 26.91/17.09 tff(c_3802, 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))). % 26.91/17.09 tff(c_3252, 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))). % 26.91/17.09 tff(c_3587, 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))). % 26.91/17.09 tff(c_3631, 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))). % 26.91/17.09 tff(c_3551, 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))). % 26.91/17.09 tff(c_3249, 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))). % 26.91/17.09 tff(c_3292, 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))). % 26.91/17.09 tff(c_3678, 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))). % 26.91/17.09 tff(c_3387, 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))). % 26.91/17.09 tff(c_3760, 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))). % 26.91/17.09 tff(c_3473, 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))). % 26.91/17.09 tff(c_3390, 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))). % 26.91/17.09 tff(c_3347, 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))). % 26.91/17.09 tff(c_3799, 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))). % 26.91/17.09 tff(c_3511, 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))). % 26.91/17.09 tff(c_3438, 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))). % 26.91/17.09 tff(c_3441, 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))). % 26.91/17.09 tff(c_3590, 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))). % 26.91/17.09 tff(c_3724, 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))). % 26.91/17.09 tff(c_3289, 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))). % 26.91/17.09 tff(c_3634, 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))). % 26.91/17.09 tff(c_3508, 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))). % 26.91/17.09 tff(c_3763, 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))). % 26.93/17.09 tff(c_3211, 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))). % 26.93/17.09 tff(c_3681, 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))). % 26.93/17.09 tff(c_3470, 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))). % 26.93/17.09 tff(c_3548, 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))). % 26.93/17.09 tff(c_3208, 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))). % 26.93/17.09 tff(c_1555, plain, (![P_91, X_93, X_60]: (ifeq(iext(uri_rdfs_range, P_91, uri_rdfs_Resource), true, ifeq(iext(P_91, X_93, X_60), true, true, true), true)=true))). % 26.93/17.09 tff(c_1908, plain, (![P_95, X_60, Y_98]: (ifeq(iext(uri_rdfs_domain, P_95, uri_rdfs_Resource), true, ifeq(iext(P_95, X_60, Y_98), true, true, true), true)=true))). % 26.93/17.09 tff(c_2437, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_domain), true, ifeq(iext(P_99, uri_rdf_type, uri_rdfs_Resource), true, true, true), true)=true))). % 26.93/17.09 tff(c_2461, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_range), true, ifeq(iext(P_99, uri_rdfs_member, uri_rdfs_Resource), true, true, true), true)=true))). % 26.93/17.09 tff(c_2449, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_range), true, ifeq(iext(P_99, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true, true, true), true)=true))). % 26.93/17.09 tff(c_2308, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_domain), true, ifeq(iext(P_99, uri_rdf__1, uri_rdfs_Resource), true, true, true), true)=true))). % 26.93/17.09 tff(c_2419, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_range), true, ifeq(iext(P_99, uri_rdf_subject, uri_rdfs_Resource), true, true, true), true)=true))). % 26.93/17.09 tff(c_2347, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdf_type), true, ifeq(iext(P_99, uri_rdf__2, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 26.93/17.09 tff(c_2485, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_domain), true, ifeq(iext(P_99, uri_rdfs_domain, uri_rdf_Property), true, true, true), true)=true))). % 26.93/17.09 tff(c_2575, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_range), true, ifeq(iext(P_99, uri_rdfs_domain, uri_rdfs_Class), true, true, true), true)=true))). % 26.93/17.09 tff(c_2332, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdf_type), true, ifeq(iext(P_99, uri_rdf_rest, uri_rdf_Property), true, true, true), true)=true))). % 26.93/17.09 tff(c_2521, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdf_type), true, ifeq(iext(P_99, uri_rdf__1, uri_rdf_Property), true, true, true), true)=true))). % 26.93/17.09 tff(c_2527, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_subClassOf), true, ifeq(iext(P_99, uri_rdfs_Datatype, uri_rdfs_Class), true, true, true), true)=true))). % 26.93/17.09 tff(c_2353, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_range), true, ifeq(iext(P_99, uri_rdfs_label, uri_rdfs_Literal), true, true, true), true)=true))). % 26.93/17.09 tff(c_2587, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_range), true, ifeq(iext(P_99, uri_rdf_value, uri_rdfs_Resource), true, true, true), true)=true))). % 26.93/17.09 tff(c_2581, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_range), true, ifeq(iext(P_99, uri_rdfs_subPropertyOf, uri_rdf_Property), true, true, true), true)=true))). % 26.93/17.09 tff(c_31820, plain, (![X_733, Y_734]: (ifeq(iext(uri_rdfs_isDefinedBy, X_733, Y_734), true, iext(uri_rdfs_seeAlso, X_733, Y_734), true)=true))). % 26.93/17.09 tff(c_2467, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdf_type), true, ifeq(iext(P_99, uri_rdf_type, uri_rdf_Property), true, true, true), true)=true))). % 26.93/17.09 tff(c_2515, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdf_type), true, ifeq(iext(P_99, uri_rdf__2, uri_rdf_Property), true, true, true), true)=true))). % 26.93/17.09 tff(c_2278, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_domain), true, ifeq(iext(P_99, uri_rdf_value, uri_rdfs_Resource), true, true, true), true)=true))). % 26.93/17.09 tff(c_2389, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_domain), true, ifeq(iext(P_99, uri_rdfs_label, uri_rdfs_Resource), true, true, true), true)=true))). % 26.93/17.09 tff(c_2266, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_range), true, ifeq(iext(P_99, uri_rdf__3, uri_rdfs_Resource), true, true, true), true)=true))). % 26.93/17.09 tff(c_2260, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_domain), true, ifeq(iext(P_99, uri_rdf_predicate, uri_rdfs_Statement), true, true, true), true)=true))). % 26.93/17.09 tff(c_2509, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_subClassOf), true, ifeq(iext(P_99, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property), true, true, true), true)=true))). % 26.93/17.09 tff(c_2395, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_range), true, ifeq(iext(P_99, uri_rdfs_comment, uri_rdfs_Literal), true, true, true), true)=true))). % 26.93/17.09 tff(c_2479, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_subClassOf), true, ifeq(iext(P_99, uri_rdfs_Seq, uri_rdfs_Container), true, true, true), true)=true))). % 26.93/17.09 tff(c_2272, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_domain), true, ifeq(iext(P_99, uri_rdf__3, uri_rdfs_Resource), true, true, true), true)=true))). % 26.93/17.09 tff(c_2248, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_range), true, ifeq(iext(P_99, uri_rdf__2, uri_rdfs_Resource), true, true, true), true)=true))). % 26.93/17.09 tff(c_2443, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_domain), true, ifeq(iext(P_99, uri_rdf_rest, uri_rdf_List), true, true, true), true)=true))). % 26.93/17.09 tff(c_2341, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_subPropertyOf), true, ifeq(iext(P_99, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso), true, true, true), true)=true))). % 26.93/17.09 tff(c_2377, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdf_type), true, ifeq(iext(P_99, uri_rdf_subject, uri_rdf_Property), true, true, true), true)=true))). % 26.93/17.09 tff(c_30181, plain, (![C_717]: (ifeq(iext(uri_rdfs_subClassOf, C_717, uri_rdfs_ContainerMembershipProperty), true, iext(uri_rdfs_subClassOf, C_717, uri_rdf_Property), true)=true))). % 26.93/17.09 tff(c_2302, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_range), true, ifeq(iext(P_99, uri_rdf__1, uri_rdfs_Resource), true, true, true), true)=true))). % 26.93/17.09 tff(c_2359, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdf_type), true, ifeq(iext(P_99, uri_rdf_object, uri_rdf_Property), true, true, true), true)=true))). % 26.93/17.09 tff(c_2314, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_range), true, ifeq(iext(P_99, uri_rdfs_range, uri_rdfs_Class), true, true, true), true)=true))). % 26.93/17.09 tff(c_29774, plain, (![C_712]: (ifeq(iext(uri_rdfs_subClassOf, C_712, uri_rdf_Alt), true, iext(uri_rdfs_subClassOf, C_712, uri_rdfs_Container), true)=true))). % 26.93/17.09 tff(c_2545, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdf_type), true, ifeq(iext(P_99, uri_rdf_first, uri_rdf_Property), true, true, true), true)=true))). % 26.93/17.09 tff(c_2254, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_domain), true, ifeq(iext(P_99, uri_rdf_object, uri_rdfs_Statement), true, true, true), true)=true))). % 26.93/17.09 tff(c_29487, plain, (![C_708]: (ifeq(iext(uri_rdfs_subClassOf, C_708, uri_rdfs_Seq), true, iext(uri_rdfs_subClassOf, C_708, uri_rdfs_Container), true)=true))). % 26.93/17.09 tff(c_2539, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdf_type), true, ifeq(iext(P_99, uri_rdf_value, uri_rdf_Property), true, true, true), true)=true))). % 26.93/17.09 tff(c_2491, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdf_type), true, ifeq(iext(P_99, uri_rdf_Property, uri_rdfs_Class), true, true, true), true)=true))). % 26.93/17.09 tff(c_2290, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_domain), true, ifeq(iext(P_99, uri_rdfs_subPropertyOf, uri_rdf_Property), true, true, true), true)=true))). % 26.93/17.09 tff(c_2296, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_domain), true, ifeq(iext(P_99, uri_rdf__2, uri_rdfs_Resource), true, true, true), true)=true))). % 26.93/17.09 tff(c_2563, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_domain), true, ifeq(iext(P_99, uri_rdfs_seeAlso, uri_rdfs_Resource), true, true, true), true)=true))). % 26.93/17.10 tff(c_28843, plain, (![D_701]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_701), true, icext(D_701, uri_rdfs_Resource), true)=true))). % 26.93/17.10 tff(c_28777, plain, (![D_699]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_699), true, icext(D_699, uri_rdfs_subClassOf), true)=true))). % 26.93/17.10 tff(c_2383, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_range), true, ifeq(iext(P_99, uri_rdf_predicate, uri_rdfs_Resource), true, true, true), true)=true))). % 26.93/17.10 tff(c_28593, plain, (![D_696]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_696), true, icext(D_696, uri_rdfs_range), true)=true))). % 26.93/17.10 tff(c_28527, plain, (![D_694]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_694), true, icext(D_694, uri_rdfs_domain), true)=true))). % 26.93/17.10 tff(c_28461, plain, (![D_692]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_692), true, icext(D_692, uri_rdfs_subPropertyOf), true)=true))). % 26.93/17.10 tff(c_28394, plain, (![D_690]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_690), true, icext(D_690, uri_rdfs_isDefinedBy), true)=true))). % 26.93/17.10 tff(c_28326, plain, (![D_688]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_688), true, icext(D_688, uri_rdf_Alt), true)=true))). % 26.93/17.10 tff(c_28259, plain, (![C_686]: (ifeq(iext(uri_rdfs_subClassOf, C_686, uri_rdf_Bag), true, iext(uri_rdfs_subClassOf, C_686, uri_rdfs_Container), true)=true))). % 26.93/17.10 tff(c_28192, plain, (![D_684]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_684), true, icext(D_684, uri_rdf_Bag), true)=true))). % 26.93/17.10 tff(c_28118, plain, (![D_682]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_682), true, icext(D_682, uri_rdf_XMLLiteral), true)=true))). % 26.93/17.10 tff(c_2320, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdf_type), true, ifeq(iext(P_99, uri_rdf__1, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 26.93/17.10 tff(c_27941, plain, (![D_679]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_679), true, icext(D_679, uri_rdfs_ContainerMembershipProperty), true)=true))). % 26.93/17.10 tff(c_27875, plain, (![D_677]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_677), true, icext(D_677, uri_rdfs_Literal), true)=true))). % 26.93/17.10 tff(c_27693, plain, (![D_674]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_674), true, icext(D_674, uri_rdfs_Seq), true)=true))). % 26.93/17.10 tff(c_2425, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_range), true, ifeq(iext(P_99, uri_rdfs_subClassOf, uri_rdfs_Class), true, true, true), true)=true))). % 26.93/17.10 tff(c_27624, plain, (![D_672]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_672), true, icext(D_672, uri_rdfs_Datatype), true)=true))). % 26.93/17.10 tff(c_27443, plain, (![D_669]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_669), true, icext(D_669, uri_rdfs_Container), true)=true))). % 26.93/17.10 tff(c_2497, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_range), true, ifeq(iext(P_99, uri_rdf_first, uri_rdfs_Resource), true, true, true), true)=true))). % 26.93/17.10 tff(c_27349, plain, (![D_667]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_667), true, icext(D_667, uri_rdfs_Class), true)=true))). % 26.93/17.10 tff(c_27283, plain, (![D_665]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_665), true, icext(D_665, uri_rdfs_label), true)=true))). % 26.93/17.10 tff(c_2473, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdf_type), true, ifeq(iext(P_99, uri_rdf_XMLLiteral, uri_rdfs_Datatype), true, true, true), true)=true))). % 26.93/17.10 tff(c_27104, plain, (![D_662]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_662), true, icext(D_662, uri_rdfs_comment), true)=true))). % 26.93/17.10 tff(c_27038, plain, (![D_660]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_660), true, icext(D_660, uri_rdf_List), true)=true))). % 26.93/17.10 tff(c_26969, plain, (![D_658]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_658), true, icext(D_658, uri_rdf_predicate), true)=true))). % 26.93/17.10 tff(c_26903, plain, (![D_656]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_656), true, icext(D_656, uri_rdfs_Statement), true)=true))). % 26.93/17.10 tff(c_26837, plain, (![D_654]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_654), true, icext(D_654, uri_rdfs_member), true)=true))). % 26.93/17.10 tff(c_2569, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_range), true, ifeq(iext(P_99, uri_rdfs_seeAlso, uri_rdfs_Resource), true, true, true), true)=true))). % 26.93/17.10 tff(c_26652, plain, (![D_651]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_651), true, icext(D_651, uri_rdfs_seeAlso), true)=true))). % 26.93/17.10 tff(c_26586, plain, (![D_649]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_649), true, icext(D_649, uri_rdf_first), true)=true))). % 26.93/17.10 tff(c_11893, 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))). % 26.93/17.10 tff(c_2533, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_domain), true, ifeq(iext(P_99, uri_rdf_first, uri_rdf_List), true, true, true), true)=true))). % 26.93/17.10 tff(c_11820, 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))). % 26.93/17.10 tff(c_11690, 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))). % 26.93/17.10 tff(c_11755, 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))). % 26.93/17.10 tff(c_11519, 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))). % 26.93/17.10 tff(c_2407, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_domain), true, ifeq(iext(P_99, uri_rdf_subject, uri_rdfs_Statement), true, true, true), true)=true))). % 26.93/17.10 tff(c_11619, 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))). % 26.93/17.10 tff(c_13118, 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))). % 26.93/17.10 tff(c_13238, 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))). % 26.93/17.10 tff(c_11327, 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))). % 26.93/17.10 tff(c_11416, 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))). % 26.93/17.10 tff(c_26002, plain, (![P_629]: (ifeq(iext(uri_rdfs_subPropertyOf, P_629, uri_rdfs_isDefinedBy), true, iext(uri_rdfs_subPropertyOf, P_629, uri_rdfs_seeAlso), true)=true))). % 26.93/17.10 tff(c_11418, 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))). % 26.93/17.10 tff(c_13116, 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))). % 26.93/17.10 tff(c_25858, plain, (![D_624]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_624), true, icext(D_624, uri_rdf__3), true)=true))). % 26.93/17.10 tff(c_10918, 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))). % 26.93/17.10 tff(c_11182, 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))). % 26.93/17.10 tff(c_10965, 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))). % 26.93/17.10 tff(c_2455, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_domain), true, ifeq(iext(P_99, uri_rdfs_subClassOf, uri_rdfs_Class), true, true, true), true)=true))). % 26.93/17.10 tff(c_11262, 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))). % 26.93/17.10 tff(c_11135, 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))). % 26.93/17.10 tff(c_11012, 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))). % 26.93/17.10 tff(c_11088, 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))). % 26.93/17.10 tff(c_10799, 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))). % 26.93/17.10 tff(c_10846, 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))). % 26.93/17.10 tff(c_10222, 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))). % 26.93/17.10 tff(c_10605, 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))). % 26.93/17.10 tff(c_2242, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_domain), true, ifeq(iext(P_99, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true, true, true), true)=true))). % 26.93/17.10 tff(c_10705, 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))). % 26.93/17.10 tff(c_10552, 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))). % 26.93/17.10 tff(c_13050, 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))). % 26.93/17.10 tff(c_25340, plain, (![D_606]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_606), true, icext(D_606, uri_rdf_type), true)=true))). % 26.93/17.10 tff(c_10167, 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))). % 26.93/17.10 tff(c_2557, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_range), true, ifeq(iext(P_99, uri_rdf_rest, uri_rdf_List), true, true, true), true)=true))). % 26.93/17.10 tff(c_4703, 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))). % 26.93/17.10 tff(c_24977, plain, (![D_597]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, D_597), true, icext(D_597, uri_rdf_XMLLiteral), true)=true))). % 26.93/17.10 tff(c_9761, 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))). % 26.93/17.10 tff(c_7065, 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))). % 26.93/17.10 tff(c_5414, 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))). % 26.93/17.10 tff(c_2503, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_subClassOf), true, ifeq(iext(P_99, uri_rdf_Bag, uri_rdfs_Container), true, true, true), true)=true))). % 26.93/17.10 tff(c_5950, 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))). % 27.00/17.10 tff(c_4598, 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))). % 27.00/17.10 tff(c_8007, 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))). % 27.00/17.10 tff(c_6265, 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))). % 27.00/17.10 tff(c_5097, 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))). % 27.00/17.10 tff(c_2551, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdf_type), true, ifeq(iext(P_99, uri_rdf__3, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 27.00/17.10 tff(c_7953, 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))). % 27.00/17.10 tff(c_9844, 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))). % 27.00/17.10 tff(c_24379, plain, (![D_579]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_579), true, icext(D_579, uri_rdf__1), true)=true))). % 27.00/17.10 tff(c_24305, plain, (![C_576]: (ifeq(iext(uri_rdfs_subClassOf, C_576, uri_rdf_XMLLiteral), true, iext(uri_rdfs_subClassOf, C_576, uri_rdfs_Literal), true)=true))). % 27.00/17.10 tff(c_6051, 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))). % 27.00/17.10 tff(c_9763, 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))). % 27.00/17.10 tff(c_24173, plain, (![D_571]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_571), true, icext(D_571, uri_rdf_Property), true)=true))). % 27.00/17.10 tff(c_6581, 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))). % 27.00/17.10 tff(c_5028, 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))). % 27.00/17.10 tff(c_2371, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_subClassOf), true, ifeq(iext(P_99, uri_rdf_Alt, uri_rdfs_Container), true, true, true), true)=true))). % 27.00/17.10 tff(c_4538, 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))). % 27.00/17.10 tff(c_8507, 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))). % 27.00/17.10 tff(c_8307, 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))). % 27.00/17.10 tff(c_8603, 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))). % 27.00/17.10 tff(c_6052, 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))). % 27.00/17.10 tff(c_6520, 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))). % 27.00/17.10 tff(c_7288, 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))). % 27.00/17.10 tff(c_2413, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_range), true, ifeq(iext(P_99, uri_rdf_type, uri_rdfs_Class), true, true, true), true)=true))). % 27.00/17.10 tff(c_8213, 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))). % 27.00/17.10 tff(c_6660, 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))). % 27.00/17.10 tff(c_23578, plain, (![D_553]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_553), true, icext(D_553, uri_rdf__1), true)=true))). % 27.00/17.10 tff(c_5729, 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))). % 27.00/17.10 tff(c_9481, 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))). % 27.00/17.10 tff(c_2326, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_domain), true, ifeq(iext(P_99, uri_rdfs_member, uri_rdfs_Resource), true, true, true), true)=true))). % 27.00/17.11 tff(c_8893, 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))). % 27.00/17.11 tff(c_5632, 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))). % 27.00/17.11 tff(c_7805, 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))). % 27.00/17.11 tff(c_23279, plain, (![D_544]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_544), true, icext(D_544, uri_rdf_rest), true)=true))). % 27.00/17.11 tff(c_7003, 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))). % 27.00/17.11 tff(c_23213, plain, (![C_541]: (ifeq(iext(uri_rdfs_subClassOf, C_541, uri_rdfs_Datatype), true, iext(uri_rdfs_subClassOf, C_541, uri_rdfs_Class), true)=true))). % 27.00/17.11 tff(c_4599, 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))). % 27.00/17.11 tff(c_7569, 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))). % 27.00/17.11 tff(c_6912, 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))). % 27.00/17.11 tff(c_8441, 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))). % 27.00/17.11 tff(c_6404, 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))). % 27.00/17.11 tff(c_9355, 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))). % 27.00/17.11 tff(c_2284, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdf_type), true, ifeq(iext(P_99, uri_rdf_nil, uri_rdf_List), true, true, true), true)=true))). % 27.00/17.11 tff(c_5949, 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))). % 27.00/17.11 tff(c_7807, 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))). % 27.00/17.11 tff(c_7289, 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))). % 27.00/17.11 tff(c_22812, plain, (![D_527]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_527), true, icext(D_527, uri_rdf__2), true)=true))). % 27.00/17.11 tff(c_4702, 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))). % 27.00/17.11 tff(c_9421, 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))). % 27.00/17.11 tff(c_2401, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_domain), true, ifeq(iext(P_99, uri_rdfs_range, uri_rdf_Property), true, true, true), true)=true))). % 27.00/17.11 tff(c_5861, 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))). % 27.00/17.11 tff(c_9695, 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))). % 27.00/17.11 tff(c_22504, plain, (![D_518]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_518), true, icext(D_518, uri_rdf_nil), true)=true))). % 27.00/17.11 tff(c_9254, 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))). % 27.00/17.11 tff(c_8891, 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))). % 27.00/17.11 tff(c_2236, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdf_type), true, ifeq(iext(P_99, uri_rdf__3, uri_rdf_Property), true, true, true), true)=true))). % 27.00/17.11 tff(c_8826, 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))). % 27.00/17.11 tff(c_22190, plain, (![D_509]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_509), true, icext(D_509, uri_rdf_value), true)=true))). % 27.00/17.11 tff(c_5166, 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))). % 27.00/17.11 tff(c_9846, 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))). % 27.00/17.11 tff(c_2365, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_domain), true, ifeq(iext(P_99, uri_rdfs_comment, uri_rdfs_Resource), true, true, true), true)=true))). % 27.00/17.11 tff(c_9256, 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))). % 27.00/17.11 tff(c_6159, 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))). % 27.00/17.11 tff(c_7571, 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))). % 27.00/17.11 tff(c_8375, 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))). % 27.00/17.11 tff(c_8959, 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))). % 27.00/17.11 tff(c_2431, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_subClassOf), true, ifeq(iext(P_99, uri_rdf_XMLLiteral, uri_rdfs_Literal), true, true, true), true)=true))). % 27.00/17.11 tff(c_5027, 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))). % 27.00/17.11 tff(c_8148, 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))). % 27.00/17.11 tff(c_6911, 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))). % 27.00/17.11 tff(c_9943, 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))). % 27.00/17.11 tff(c_4461, plain, (![Q_48, X_136]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, X_136, uri_rdfs_Resource), true)=true))). % 27.00/17.11 tff(c_2736, plain, (![R_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_seeAlso, R_104), true, iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, R_104), true)=true))). % 27.00/17.11 tff(c_2813, plain, (![E_107]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_107), true, iext(uri_rdfs_subClassOf, uri_rdf_Bag, E_107), true)=true))). % 27.00/17.11 tff(c_2810, plain, (![E_107]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_107), true, iext(uri_rdfs_subClassOf, uri_rdf_Alt, E_107), true)=true))). % 27.00/17.11 tff(c_2620, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_100), true, iext(Q_100, uri_rdf_subject, uri_rdfs_Resource), true)=true))). % 27.00/17.11 tff(c_2614, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_100), true, iext(Q_100, uri_rdf_predicate, uri_rdfs_Resource), true)=true))). % 27.00/17.11 tff(c_2812, plain, (![E_107]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_107), true, iext(uri_rdfs_subClassOf, uri_rdfs_Seq, E_107), true)=true))). % 27.00/17.11 tff(c_2643, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_100), true, iext(Q_100, uri_rdf_rest, uri_rdf_List), true)=true))). % 27.00/17.11 tff(c_21250, plain, (![D_481]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_481), true, icext(D_481, uri_rdf__3), true)=true))). % 27.03/17.11 tff(c_2621, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_100), true, iext(Q_100, uri_rdfs_subClassOf, uri_rdfs_Class), true)=true))). % 27.03/17.11 tff(c_2606, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_100), true, iext(Q_100, uri_rdf_rest, uri_rdf_Property), true)=true))). % 27.03/17.11 tff(c_2624, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_100), true, iext(Q_100, uri_rdf_rest, uri_rdf_List), true)=true))). % 27.03/17.11 tff(c_2609, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_100), true, iext(Q_100, uri_rdfs_label, uri_rdfs_Literal), true)=true))). % 27.03/17.11 tff(c_2635, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_100), true, iext(Q_100, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property), true)=true))). % 27.03/17.11 tff(c_2627, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_100), true, iext(Q_100, uri_rdfs_member, uri_rdfs_Resource), true)=true))). % 27.03/17.11 tff(c_2628, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_100), true, iext(Q_100, uri_rdf_type, uri_rdf_Property), true)=true))). % 27.03/17.11 tff(c_2593, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_100), true, iext(Q_100, uri_rdf_object, uri_rdfs_Statement), true)=true))). % 27.03/17.11 tff(c_2611, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_100), true, iext(Q_100, uri_rdfs_comment, uri_rdfs_Resource), true)=true))). % 27.03/17.11 tff(c_2592, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_100), true, iext(Q_100, uri_rdf__2, uri_rdfs_Resource), true)=true))). % 27.03/17.11 tff(c_2591, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_100), true, iext(Q_100, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true)=true))). % 27.03/17.11 tff(c_2623, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_100), true, iext(Q_100, uri_rdf_type, uri_rdfs_Resource), true)=true))). % 27.03/17.11 tff(c_2645, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_100), true, iext(Q_100, uri_rdfs_seeAlso, uri_rdfs_Resource), true)=true))). % 27.03/17.11 tff(c_2603, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_100), true, iext(Q_100, uri_rdfs_range, uri_rdfs_Class), true)=true))). % 27.03/17.11 tff(c_2637, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_100), true, iext(Q_100, uri_rdf__1, uri_rdf_Property), true)=true))). % 27.03/17.11 tff(c_2596, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_100), true, iext(Q_100, uri_rdf__3, uri_rdfs_Resource), true)=true))). % 27.03/17.11 tff(c_20860, plain, (![D_463]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_463), true, icext(D_463, uri_rdf_object), true)=true))). % 27.03/17.11 tff(c_2601, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_100), true, iext(Q_100, uri_rdf__1, uri_rdfs_Resource), true)=true))). % 27.03/17.11 tff(c_2617, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_100), true, iext(Q_100, uri_rdfs_range, uri_rdf_Property), true)=true))). % 27.03/17.11 tff(c_2638, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_100), true, iext(Q_100, uri_rdfs_Datatype, uri_rdfs_Class), true)=true))). % 27.03/17.11 tff(c_2602, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_100), true, iext(Q_100, uri_rdf__1, uri_rdfs_Resource), true)=true))). % 27.03/17.11 tff(c_2597, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_100), true, iext(Q_100, uri_rdf_value, uri_rdfs_Resource), true)=true))). % 27.03/17.11 tff(c_2626, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_100), true, iext(Q_100, uri_rdfs_subClassOf, uri_rdfs_Class), true)=true))). % 27.03/17.11 tff(c_2648, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_100), true, iext(Q_100, uri_rdf_value, uri_rdfs_Resource), true)=true))). % 27.03/17.11 tff(c_2636, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_100), true, iext(Q_100, uri_rdf__2, uri_rdf_Property), true)=true))). % 27.03/17.11 tff(c_2595, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_100), true, iext(Q_100, uri_rdf__3, uri_rdfs_Resource), true)=true))). % 27.03/17.11 tff(c_2608, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_100), true, iext(Q_100, uri_rdf__2, uri_rdfs_ContainerMembershipProperty), true)=true))). % 27.03/17.11 tff(c_2642, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_100), true, iext(Q_100, uri_rdf__3, uri_rdfs_ContainerMembershipProperty), true)=true))). % 27.03/17.11 tff(c_2618, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_100), true, iext(Q_100, uri_rdf_subject, uri_rdfs_Statement), true)=true))). % 27.03/17.11 tff(c_2598, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_100), true, iext(Q_100, uri_rdf_nil, uri_rdf_List), true)=true))). % 27.03/17.11 tff(c_2646, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_100), true, iext(Q_100, uri_rdfs_domain, uri_rdfs_Class), true)=true))). % 27.03/17.11 tff(c_2814, plain, (![E_107]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, E_107), true, iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, E_107), true)=true))). % 27.03/17.11 tff(c_2640, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_100), true, iext(Q_100, uri_rdf_value, uri_rdf_Property), true)=true))). % 27.03/17.11 tff(c_2613, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_100), true, iext(Q_100, uri_rdf_subject, uri_rdf_Property), true)=true))). % 27.03/17.11 tff(c_2644, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_100), true, iext(Q_100, uri_rdfs_seeAlso, uri_rdfs_Resource), true)=true))). % 27.03/17.11 tff(c_2633, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_100), true, iext(Q_100, uri_rdf_first, uri_rdfs_Resource), true)=true))). % 27.03/17.11 tff(c_2622, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_100), true, iext(Q_100, uri_rdf_XMLLiteral, uri_rdfs_Literal), true)=true))). % 27.03/17.11 tff(c_2607, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_100), true, iext(Q_100, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso), true)=true))). % 27.03/17.11 tff(c_2647, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_100), true, iext(Q_100, uri_rdfs_subPropertyOf, uri_rdf_Property), true)=true))). % 27.03/17.11 tff(c_2605, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_100), true, iext(Q_100, uri_rdfs_member, uri_rdfs_Resource), true)=true))). % 27.03/17.11 tff(c_11757, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_label), true)=true))). % 27.03/17.11 tff(c_11756, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_label), true)=true))). % 27.03/17.11 tff(c_11821, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_predicate), true)=true))). % 27.03/17.11 tff(c_11822, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_predicate), true)=true))). % 27.03/17.11 tff(c_11691, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_comment), true)=true))). % 27.03/17.11 tff(c_2599, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_100), true, iext(Q_100, uri_rdfs_subPropertyOf, uri_rdf_Property), true)=true))). % 27.03/17.11 tff(c_11692, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_comment), true)=true))). % 27.03/17.11 tff(c_11620, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Resource), true)=true))). % 27.03/17.11 tff(c_11520, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_member), true)=true))). % 27.03/17.11 tff(c_13240, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_List), true)=true))). % 27.03/17.11 tff(c_13239, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdf_List), true)=true))). % 27.03/17.11 tff(c_2815, plain, (![E_107]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, E_107), true, iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, E_107), true)=true))). % 27.03/17.11 tff(c_11329, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Statement), true)=true))). % 27.03/17.11 tff(c_11419, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Statement), true)=true))). % 27.03/17.11 tff(c_2619, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_100), true, iext(Q_100, uri_rdf_type, uri_rdfs_Class), true)=true))). % 27.03/17.11 tff(c_19957, plain, (![D_423]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_423), true, icext(D_423, uri_rdf__2), true)=true))). % 27.03/17.11 tff(c_2631, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_100), true, iext(Q_100, uri_rdfs_domain, uri_rdf_Property), true)=true))). % 27.03/17.11 tff(c_19856, plain, (![D_420]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_420), true, icext(D_420, uri_rdf_subject), true)=true))). % 27.03/17.11 tff(c_2632, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_100), true, iext(Q_100, uri_rdf_Property, uri_rdfs_Class), true)=true))). % 27.03/17.11 tff(c_19688, plain, (![C_88, X_60]: (ifeq(icext(C_88, X_60), true, true, true)=true))). % 27.03/17.11 tff(c_2625, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_100), true, iext(Q_100, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true)=true))). % 27.03/17.11 tff(c_19290, plain, (![D_412, X_413]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, D_412), true, icext(D_412, X_413), true)=true))). % 27.03/17.11 tff(c_2604, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_100), true, iext(Q_100, uri_rdf__1, uri_rdfs_ContainerMembershipProperty), true)=true))). % 27.03/17.12 tff(c_7066, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_value), true)=true))). % 27.03/17.12 tff(c_18917, plain, (![X_406, Y_407]: (ifeq(iext(uri_rdfs_range, X_406, Y_407), true, icext(uri_rdfs_Class, Y_407), true)=true))). % 27.03/17.12 tff(c_6522, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_first), true)=true))). % 27.03/17.12 tff(c_2630, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_100), true, iext(Q_100, uri_rdfs_Seq, uri_rdfs_Container), true)=true))). % 27.03/17.12 tff(c_8377, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Seq), true)=true))). % 27.03/17.12 tff(c_18816, plain, (![X_399, Y_400]: (ifeq(iext(uri_rdfs_comment, X_399, Y_400), true, icext(uri_rdfs_Literal, Y_400), true)=true))). % 27.03/17.12 tff(c_8508, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_subClassOf), true)=true))). % 27.03/17.12 tff(c_7955, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_range), true)=true))). % 27.03/17.12 tff(c_8443, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_XMLLiteral), true)=true))). % 27.03/17.12 tff(c_2610, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_100), true, iext(Q_100, uri_rdf_object, uri_rdf_Property), true)=true))). % 27.03/17.12 tff(c_8150, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__2), true)=true))). % 27.03/17.12 tff(c_8509, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_subClassOf), true)=true))). % 27.03/17.12 tff(c_18615, plain, (![X_389, Y_390]: (ifeq(iext(uri_rdf_rest, X_389, Y_390), true, icext(uri_rdf_List, X_389), true)=true))). % 27.03/17.12 tff(c_2639, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_100), true, iext(Q_100, uri_rdf_first, uri_rdf_List), true)=true))). % 27.03/17.12 tff(c_9423, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_Alt), true)=true))). % 27.03/17.12 tff(c_18190, plain, (![X_383, Y_384]: (ifeq(iext(uri_rdfs_subPropertyOf, X_383, Y_384), true, icext(uri_rdf_Property, Y_384), true)=true))). % 27.03/17.12 tff(c_5863, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_subPropertyOf), true)=true))). % 27.03/17.12 tff(c_9257, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__2), true)=true))). % 27.03/17.12 tff(c_2612, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_100), true, iext(Q_100, uri_rdf_Alt, uri_rdfs_Container), true)=true))). % 27.03/17.12 tff(c_8895, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_member), true)=true))). % 27.03/17.12 tff(c_17629, plain, (![X_375, Y_376]: (ifeq(iext(uri_rdf_type, X_375, Y_376), true, icext(uri_rdfs_Class, Y_376), true)=true))). % 27.03/17.12 tff(c_8604, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_seeAlso), true)=true))). % 27.03/17.12 tff(c_2590, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_100), true, iext(Q_100, uri_rdf__3, uri_rdf_Property), true)=true))). % 27.03/17.12 tff(c_8308, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_subject), true)=true))). % 27.03/17.12 tff(c_7005, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_Bag), true)=true))). % 27.03/17.12 tff(c_17504, plain, (![X_367, Y_368]: (ifeq(iext(uri_rdf_subject, X_367, Y_368), true, icext(uri_rdfs_Statement, X_367), true)=true))). % 27.03/17.12 tff(c_6267, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_type), true)=true))). % 27.03/17.12 tff(c_8960, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Class), true)=true))). % 27.03/17.12 tff(c_2811, plain, (![E_107]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Literal, E_107), true, iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, E_107), true)=true))). % 27.03/17.12 tff(c_6521, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_first), true)=true))). % 27.03/17.12 tff(c_16874, plain, (![X_358, Y_359]: (ifeq(iext(uri_rdfs_subClassOf, X_358, Y_359), true, icext(uri_rdfs_Class, Y_359), true)=true))). % 27.03/17.12 tff(c_9357, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_ContainerMembershipProperty), true)=true))). % 27.03/17.12 tff(c_2615, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_100), true, iext(Q_100, uri_rdfs_label, uri_rdfs_Resource), true)=true))). % 27.03/17.12 tff(c_16456, plain, (![X_352, Y_353]: (ifeq(iext(uri_rdfs_subPropertyOf, X_352, Y_353), true, icext(uri_rdf_Property, X_352), true)=true))). % 27.03/17.12 tff(c_2641, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_100), true, iext(Q_100, uri_rdf_first, uri_rdf_Property), true)=true))). % 27.03/17.12 tff(c_5168, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_domain), true)=true))). % 27.03/17.12 tff(c_16111, plain, (![X_346, Y_347]: (ifeq(iext(uri_rdfs_domain, X_346, Y_347), true, icext(uri_rdfs_Class, Y_347), true)=true))). % 27.03/17.12 tff(c_5730, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_object), true)=true))). % 27.03/17.12 tff(c_2634, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_100), true, iext(Q_100, uri_rdf_Bag, uri_rdfs_Container), true)=true))). % 27.03/17.12 tff(c_7954, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_range), true)=true))). % 27.03/17.12 tff(c_16010, plain, (![X_339, Y_340]: (ifeq(iext(uri_rdf_predicate, X_339, Y_340), true, icext(uri_rdfs_Statement, X_339), true)=true))). % 27.03/17.12 tff(c_5633, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Literal), true)=true))). % 27.03/17.12 tff(c_7067, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_value), true)=true))). % 27.03/17.12 tff(c_2629, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_100), true, iext(Q_100, uri_rdf_XMLLiteral, uri_rdfs_Datatype), true)=true))). % 27.03/17.12 tff(c_9696, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__1), true)=true))). % 27.03/17.12 tff(c_5098, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdf_Property), true)=true))). % 27.03/17.12 tff(c_15849, plain, (![X_330, Y_331]: (ifeq(iext(uri_rdf_first, X_330, Y_331), true, icext(uri_rdf_List, X_330), true)=true))). % 27.03/17.12 tff(c_8309, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_subject), true)=true))). % 27.03/17.12 tff(c_6266, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_type), true)=true))). % 27.03/17.12 tff(c_2594, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_100), true, iext(Q_100, uri_rdf_predicate, uri_rdfs_Statement), true)=true))). % 27.03/17.12 tff(c_6583, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Datatype), true)=true))). % 27.03/17.12 tff(c_5862, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_subPropertyOf), true)=true))). % 27.03/17.12 tff(c_6406, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__3), true)=true))). % 27.03/17.12 tff(c_15364, plain, (![X_320, Y_321]: (ifeq(iext(uri_rdfs_range, X_320, Y_321), true, icext(uri_rdf_Property, X_320), true)=true))). % 27.03/17.12 tff(c_8215, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_isDefinedBy), true)=true))). % 27.03/17.12 tff(c_6160, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Container), true)=true))). % 27.03/17.12 tff(c_2600, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_100), true, iext(Q_100, uri_rdf__2, uri_rdfs_Resource), true)=true))). % 27.03/17.12 tff(c_5167, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_domain), true)=true))). % 27.03/17.12 tff(c_5731, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_object), true)=true))). % 27.03/17.12 tff(c_15198, plain, (![X_311, Y_312]: (ifeq(iext(uri_rdf_rest, X_311, Y_312), true, icext(uri_rdf_List, Y_312), true)=true))). % 27.03/17.12 tff(c_4600, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__3), true)=true))). % 27.03/17.12 tff(c_4540, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_rest), true)=true))). % 27.03/17.12 tff(c_2616, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_100), true, iext(Q_100, uri_rdfs_comment, uri_rdfs_Literal), true)=true))). % 27.03/17.12 tff(c_5030, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Resource), true)=true))). % 27.03/17.12 tff(c_9697, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__1), true)=true))). % 27.03/17.12 tff(c_4539, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_rest), true)=true))). % 27.03/17.12 tff(c_4463, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_29), true, icext(C_29, uri_rdfs_Resource), true)=true))). % 27.03/17.12 tff(c_4462, plain, (![C_19, X_136]: (ifeq(iext(uri_rdfs_domain, uri_rdf_type, C_19), true, icext(C_19, X_136), true)=true))). % 27.03/17.12 tff(c_14700, plain, (![X_294, Y_295]: (ifeq(iext(uri_rdfs_label, X_294, Y_295), true, icext(uri_rdfs_Literal, Y_295), true)=true))). % 27.03/17.12 tff(c_1799, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_92), true, icext(C_92, uri_rdf_List), true)=true))). % 27.03/17.12 tff(c_2211, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdfs_domain), true)=true))). % 27.03/17.12 tff(c_2207, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdf_rest), true)=true))). % 27.03/17.12 tff(c_2189, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdfs_isDefinedBy), true)=true))). % 27.03/17.12 tff(c_1826, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_92), true, icext(C_92, uri_rdfs_Literal), true)=true))). % 27.03/17.12 tff(c_2180, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdfs_range), true)=true))). % 27.03/17.12 tff(c_2168, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_96), true, icext(C_96, uri_rdfs_isDefinedBy), true)=true))). % 27.03/17.12 tff(c_2197, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdf_first), true)=true))). % 27.03/17.12 tff(c_2190, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdfs_subClassOf), true)=true))). % 27.03/17.12 tff(c_2188, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdf_rest), true)=true))). % 27.03/17.12 tff(c_1855, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_92), true, icext(C_92, uri_rdf_Property), true)=true))). % 27.03/17.12 tff(c_2198, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_96), true, icext(C_96, uri_rdf_Bag), true)=true))). % 27.03/17.12 tff(c_2150, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdf_predicate), true)=true))). % 27.03/17.12 tff(c_1850, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_92), true, icext(C_92, uri_rdf_List), true)=true))). % 27.03/17.12 tff(c_2147, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdfs_isDefinedBy), true)=true))). % 27.03/17.12 tff(c_13975, plain, (![X_274, Y_275]: (ifeq(iext(uri_rdfs_domain, X_274, Y_275), true, icext(uri_rdf_Property, X_274), true)=true))). % 27.03/17.12 tff(c_2184, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdfs_subClassOf), true)=true))). % 27.03/17.12 tff(c_2157, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdfs_subPropertyOf), true)=true))). % 27.03/17.12 tff(c_2185, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_96), true, icext(C_96, uri_rdf_XMLLiteral), true)=true))). % 27.03/17.12 tff(c_1842, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_92), true, icext(C_92, uri_rdf_Property), true)=true))). % 27.03/17.12 tff(c_1835, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_92), true, icext(C_92, uri_rdfs_Datatype), true)=true))). % 27.03/17.12 tff(c_1838, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_92), true, icext(C_92, uri_rdfs_Class), true)=true))). % 27.03/17.12 tff(c_1836, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_92), true, icext(C_92, uri_rdfs_Container), true)=true))). % 27.03/17.12 tff(c_1845, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_92), true, icext(C_92, uri_rdfs_Class), true)=true))). % 27.03/17.12 tff(c_2213, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdf_value), true)=true))). % 27.03/17.12 tff(c_1831, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdfs_Class), true)=true))). % 27.03/17.12 tff(c_2179, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdfs_comment), true)=true))). % 27.03/17.12 tff(c_1810, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_92), true, icext(C_92, uri_rdfs_ContainerMembershipProperty), true)=true))). % 27.03/17.12 tff(c_2181, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdf_subject), true)=true))). % 27.03/17.12 tff(c_13510, plain, (![X_256, Y_257]: (ifeq(iext(uri_rdf_object, X_256, Y_257), true, icext(uri_rdfs_Statement, X_256), true)=true))). % 27.03/17.12 tff(c_1809, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_92), true, icext(C_92, uri_rdfs_seeAlso), true)=true))). % 27.03/17.12 tff(c_2199, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_96), true, icext(C_96, uri_rdfs_ContainerMembershipProperty), true)=true))). % 27.03/17.12 tff(c_2163, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdfs_range), true)=true))). % 27.03/17.12 tff(c_1854, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_92), true, icext(C_92, uri_rdfs_Class), true)=true))). % 27.03/17.12 tff(c_2203, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdf_first), true)=true))). % 27.03/17.12 tff(c_2159, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdf__2), true)=true))). % 27.03/17.12 tff(c_2202, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_96), true, icext(C_96, uri_rdfs_Datatype), true)=true))). % 27.03/17.12 tff(c_2170, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdfs_label), true)=true))). % 27.03/17.12 tff(c_13241, plain, (![X_33]: (ifeq(icext(uri_rdf_List, X_33), true, icext(uri_rdf_List, X_33), true)=true))). % 27.03/17.12 tff(c_13181, plain, (iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdf_List)=true)). % 27.03/17.12 tff(c_13061, plain, (iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdfs_Resource)=true)). % 27.03/17.12 tff(c_13013, plain, (iext(uri_rdf_type, uri_rdf_List, uri_rdfs_Class)=true)). % 27.03/17.12 tff(c_12863, plain, (ic(uri_rdf_List)=true)). % 27.03/17.12 tff(c_12797, plain, (icext(uri_rdfs_Class, uri_rdf_List)=true)). % 27.03/17.12 tff(c_1846, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdf_List), true)=true))). % 27.03/17.12 tff(c_11330, plain, (![X_33]: (ifeq(icext(uri_rdfs_Statement, X_33), true, icext(uri_rdfs_Statement, X_33), true)=true))). % 27.03/17.12 tff(c_5635, plain, (![X_33]: (ifeq(icext(uri_rdfs_Literal, X_33), true, icext(uri_rdfs_Literal, X_33), true)=true))). % 27.03/17.12 tff(c_12023, plain, (![X_227, Y_228]: (ifeq(iext(uri_rdfs_subClassOf, X_227, Y_228), true, icext(uri_rdfs_Class, X_227), true)=true))). % 27.03/17.12 tff(c_8444, plain, (![X_33]: (ifeq(icext(uri_rdf_XMLLiteral, X_33), true, icext(uri_rdf_XMLLiteral, X_33), true)=true))). % 27.03/17.12 tff(c_5100, plain, (![X_33]: (ifeq(icext(uri_rdf_Property, X_33), true, icext(uri_rdf_Property, X_33), true)=true))). % 27.03/17.12 tff(c_6162, plain, (![X_33]: (ifeq(icext(uri_rdfs_Container, X_33), true, icext(uri_rdfs_Container, X_33), true)=true))). % 27.03/17.12 tff(c_1819, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_92), true, icext(C_92, uri_rdfs_Literal), true)=true))). % 27.03/17.12 tff(c_7006, plain, (![X_33]: (ifeq(icext(uri_rdf_Bag, X_33), true, icext(uri_rdf_Bag, X_33), true)=true))). % 27.03/17.12 tff(c_6584, plain, (![X_33]: (ifeq(icext(uri_rdfs_Datatype, X_33), true, icext(uri_rdfs_Datatype, X_33), true)=true))). % 27.03/17.12 tff(c_9358, plain, (![X_33]: (ifeq(icext(uri_rdfs_ContainerMembershipProperty, X_33), true, icext(uri_rdfs_ContainerMembershipProperty, X_33), true)=true))). % 27.03/17.12 tff(c_9424, plain, (![X_33]: (ifeq(icext(uri_rdf_Alt, X_33), true, icext(uri_rdf_Alt, X_33), true)=true))). % 27.03/17.12 tff(c_8962, plain, (![X_33]: (ifeq(icext(uri_rdfs_Class, X_33), true, icext(uri_rdfs_Class, X_33), true)=true))). % 27.03/17.12 tff(c_8378, plain, (![X_33]: (ifeq(icext(uri_rdfs_Seq, X_33), true, icext(uri_rdfs_Seq, X_33), true)=true))). % 27.03/17.12 tff(c_11832, plain, (iext(uri_rdf_type, uri_rdfs_Resource, uri_rdfs_Class)=true)). % 27.03/17.12 tff(c_2187, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdf_type), true)=true))). % 27.03/17.12 tff(c_11767, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_predicate, uri_rdf_predicate)=true)). % 27.03/17.12 tff(c_11702, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_label, uri_rdfs_label)=true)). % 27.03/17.12 tff(c_11636, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_comment, uri_rdfs_comment)=true)). % 27.03/17.12 tff(c_11563, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Resource, uri_rdfs_Resource)=true)). % 27.03/17.13 tff(c_2153, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdf__3), true)=true))). % 27.03/17.13 tff(c_11463, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_member, uri_rdfs_member)=true)). % 27.03/17.13 tff(c_11365, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Statement, uri_rdfs_Resource)=true)). % 27.03/17.13 tff(c_11274, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Statement, uri_rdfs_Statement)=true)). % 27.03/17.13 tff(c_11226, plain, (iext(uri_rdf_type, uri_rdfs_Container, uri_rdfs_Class)=true)). % 27.03/17.13 tff(c_2162, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdf__1), true)=true))). % 27.03/17.13 tff(c_11146, plain, (iext(uri_rdf_type, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Class)=true)). % 27.03/17.13 tff(c_11099, plain, (iext(uri_rdf_type, uri_rdf_Alt, uri_rdfs_Class)=true)). % 27.03/17.13 tff(c_11023, plain, (iext(uri_rdf_type, uri_rdfs_Class, uri_rdfs_Class)=true)). % 27.03/17.13 tff(c_2195, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdfs_domain), true)=true))). % 27.03/17.13 tff(c_10976, plain, (iext(uri_rdf_type, uri_rdf_Bag, uri_rdfs_Class)=true)). % 27.03/17.13 tff(c_10929, plain, (iext(uri_rdf_type, uri_rdfs_Datatype, uri_rdfs_Class)=true)). % 27.03/17.13 tff(c_10857, plain, (iext(uri_rdf_type, uri_rdfs_Seq, uri_rdfs_Class)=true)). % 27.03/17.13 tff(c_10810, plain, (iext(uri_rdf_type, uri_rdfs_Literal, uri_rdfs_Class)=true)). % 27.03/17.13 tff(c_10763, plain, (iext(uri_rdf_type, uri_rdf_XMLLiteral, uri_rdfs_Class)=true)). % 27.03/17.13 tff(c_10720, plain, (ip(uri_rdfs_comment)=true)). % 27.03/17.13 tff(c_10663, plain, (iext(uri_rdf_type, uri_rdfs_comment, uri_rdf_Property)=true)). % 27.03/17.13 tff(c_10621, plain, (ip(uri_rdfs_label)=true)). % 27.03/17.13 tff(c_10563, plain, (iext(uri_rdf_type, uri_rdfs_label, uri_rdf_Property)=true)). % 27.03/17.13 tff(c_10516, plain, (iext(uri_rdf_type, uri_rdfs_Statement, uri_rdfs_Class)=true)). % 27.03/17.13 tff(c_2148, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdf__2), true)=true))). % 27.03/17.13 tff(c_10353, plain, (ic(uri_rdfs_Statement)=true)). % 27.03/17.13 tff(c_10299, plain, (icext(uri_rdfs_Class, uri_rdfs_Statement)=true)). % 27.03/17.13 tff(c_10257, plain, (ip(uri_rdf_predicate)=true)). % 27.03/17.13 tff(c_1793, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdfs_Statement), true)=true))). % 27.03/17.13 tff(c_10180, plain, (iext(uri_rdf_type, uri_rdf_predicate, uri_rdf_Property)=true)). % 27.03/17.13 tff(c_10125, plain, (iext(uri_rdf_type, uri_rdfs_member, uri_rdf_Property)=true)). % 27.03/17.13 tff(c_2212, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdfs_subPropertyOf), true)=true))). % 27.03/17.13 tff(c_9955, plain, (icext(uri_rdf_Property, uri_rdfs_domain)=true)). % 27.03/17.13 tff(c_9876, plain, (iext(uri_rdf_type, uri_rdfs_domain, uri_rdf_Property)=true)). % 27.03/17.13 tff(c_2183, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdf_subject), true)=true))). % 27.03/17.13 tff(c_9793, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Resource)=true)). % 27.03/17.13 tff(c_9710, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Container, uri_rdfs_Resource)=true)). % 27.03/17.13 tff(c_9642, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__1, uri_rdf__1)=true)). % 27.03/17.13 tff(c_2210, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdfs_seeAlso), true)=true))). % 27.03/17.13 tff(c_9493, plain, (icext(uri_rdf_Property, uri_rdfs_subClassOf)=true)). % 27.03/17.13 tff(c_9439, plain, (iext(uri_rdf_type, uri_rdfs_subClassOf, uri_rdf_Property)=true)). % 27.03/17.13 tff(c_9368, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdf_Alt)=true)). % 27.03/17.13 tff(c_9302, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdfs_ContainerMembershipProperty)=true)). % 27.03/17.13 tff(c_9203, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__2, uri_rdfs_member)=true)). % 27.03/17.13 tff(c_1465, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_subClassOf, S_5, O_6), true, true, true)=true))). % 27.03/17.13 tff(c_1812, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_92), true, icext(C_92, uri_rdf_Property), true)=true))). % 27.03/17.13 tff(c_8906, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdfs_Class)=true)). % 27.03/17.13 tff(c_8840, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__1, uri_rdfs_member)=true)). % 27.03/17.13 tff(c_8759, plain, (iext(uri_rdf_type, uri_rdfs_seeAlso, uri_rdf_Property)=true)). % 27.03/17.13 tff(c_2166, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdfs_member), true)=true))). % 27.03/17.13 tff(c_801, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_range, S_5, O_6), true, true, true)=true))). % 27.03/17.13 tff(c_3046, plain, (![S_5, O_6]: (ifeq(iext(uri_rdf_rest, S_5, O_6), true, true, true)=true))). % 27.03/17.13 tff(c_8550, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_seeAlso, uri_rdfs_seeAlso)=true)). % 27.03/17.13 tff(c_2174, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_96), true, icext(C_96, uri_rdf_Alt), true)=true))). % 27.03/17.13 tff(c_8454, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, uri_rdfs_subClassOf)=true)). % 27.03/17.13 tff(c_8389, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdf_XMLLiteral)=true)). % 27.03/17.13 tff(c_8322, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Seq)=true)). % 27.03/17.13 tff(c_8254, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_subject, uri_rdf_subject)=true)). % 27.03/17.13 tff(c_8160, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, uri_rdfs_isDefinedBy)=true)). % 27.03/17.13 tff(c_8095, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__2, uri_rdf__2)=true)). % 27.03/17.13 tff(c_8019, plain, (icext(uri_rdf_Property, uri_rdfs_isDefinedBy)=true)). % 27.03/17.13 tff(c_7965, plain, (iext(uri_rdf_type, uri_rdfs_isDefinedBy, uri_rdf_Property)=true)). % 27.03/17.13 tff(c_7900, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_range, uri_rdfs_range)=true)). % 27.03/17.13 tff(c_2182, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdf_type), true)=true))). % 27.03/17.13 tff(c_7754, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Resource)=true)). % 27.03/17.13 tff(c_7658, plain, (icext(uri_rdf_Property, uri_rdf_predicate)=true)). % 27.03/17.13 tff(c_2176, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdf_predicate), true)=true))). % 27.03/17.13 tff(c_1537, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_subPropertyOf, S_5, O_6), true, true, true)=true))). % 27.03/17.13 tff(c_7518, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Resource)=true)). % 27.03/17.13 tff(c_2151, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdf__3), true)=true))). % 27.03/17.13 tff(c_7240, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdfs_Resource)=true)). % 27.03/17.13 tff(c_2194, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_96), true, icext(C_96, uri_rdfs_Seq), true)=true))). % 27.03/17.13 tff(c_944, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_domain, S_5, O_6), true, true, true)=true))). % 27.03/17.13 tff(c_7016, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_value, uri_rdf_value)=true)). % 27.03/17.13 tff(c_6954, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdf_Bag)=true)). % 27.03/17.13 tff(c_6863, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Resource)=true)). % 27.03/17.13 tff(c_6778, plain, (icext(uri_rdf_Property, uri_rdfs_comment)=true)). % 27.03/17.13 tff(c_2173, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdfs_comment), true)=true))). % 27.03/17.13 tff(c_6671, plain, (icext(uri_rdf_Property, uri_rdfs_range)=true)). % 27.03/17.13 tff(c_6594, plain, (iext(uri_rdf_type, uri_rdfs_range, uri_rdf_Property)=true)). % 27.03/17.13 tff(c_1820, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdf_Property), true)=true))). % 27.03/17.13 tff(c_6532, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Datatype)=true)). % 27.03/17.13 tff(c_6471, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_first, uri_rdf_first)=true)). % 27.03/17.13 tff(c_2155, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdf_value), true)=true))). % 27.03/17.13 tff(c_6348, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__3, uri_rdf__3)=true)). % 27.03/17.13 tff(c_6296, plain, (icext(uri_rdf_Property, uri_rdfs_seeAlso)=true)). % 27.03/17.13 tff(c_2209, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdfs_seeAlso), true)=true))). % 27.03/17.13 tff(c_6212, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_type, uri_rdf_type)=true)). % 27.03/17.13 tff(c_6110, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Container, uri_rdfs_Container)=true)). % 27.03/17.13 tff(c_1857, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_92), true, icext(C_92, uri_rdfs_Resource), true)=true))). % 27.03/17.13 tff(c_6003, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Resource)=true)). % 27.03/17.13 tff(c_5901, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdfs_Resource)=true)). % 27.03/17.13 tff(c_2149, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdf_object), true)=true))). % 27.03/17.13 tff(c_5812, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf)=true)). % 27.03/17.13 tff(c_5760, plain, (icext(uri_rdf_Property, uri_rdfs_member)=true)). % 27.03/17.13 tff(c_2191, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdfs_member), true)=true))). % 27.03/17.13 tff(c_5677, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_object, uri_rdf_object)=true)). % 27.03/17.13 tff(c_5577, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdfs_Literal)=true)). % 27.03/17.13 tff(c_2160, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdf__1), true)=true))). % 27.03/17.13 tff(c_5483, plain, (icext(uri_rdf_Property, uri_rdfs_label)=true)). % 27.03/17.13 tff(c_5425, plain, (icext(uri_rdf_Property, uri_rdfs_subPropertyOf)=true)). % 27.03/17.13 tff(c_2178, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdfs_label), true)=true))). % 27.03/17.13 tff(c_5372, plain, (iext(uri_rdf_type, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 27.03/17.13 tff(c_1790, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdfs_Resource), true)=true))). % 27.03/17.13 tff(c_3129, plain, (![S_5, O_6]: (ifeq(iext(uri_rdf_object, S_5, O_6), true, true, true)=true))). % 27.03/17.13 tff(c_5117, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, uri_rdfs_domain)=true)). % 27.03/17.13 tff(c_1506, plain, (![X_89]: (ifeq(icext(uri_rdf_Bag, X_89), true, icext(uri_rdfs_Container, X_89), true)=true))). % 27.03/17.13 tff(c_5048, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdf_Property)=true)). % 27.03/17.13 tff(c_4979, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Resource)=true)). % 27.03/17.13 tff(c_1503, plain, (![X_89]: (ifeq(icext(uri_rdf_Alt, X_89), true, icext(uri_rdfs_Container, X_89), true)=true))). % 27.03/17.13 tff(c_1508, plain, (![X_89]: (ifeq(icext(uri_rdfs_Datatype, X_89), true, icext(uri_rdfs_Class, X_89), true)=true))). % 27.03/17.13 tff(c_4822, plain, (icext(uri_rdfs_Class, uri_rdfs_Resource)=true)). % 27.03/17.13 tff(c_1507, plain, (![X_89]: (ifeq(icext(uri_rdfs_ContainerMembershipProperty, X_89), true, icext(uri_rdf_Property, X_89), true)=true))). % 27.03/17.13 tff(c_4715, plain, (ic(uri_rdfs_Resource)=true)). % 27.03/17.13 tff(c_4654, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdfs_Resource)=true)). % 27.03/17.13 tff(c_1504, plain, (![X_89]: (ifeq(icext(uri_rdf_XMLLiteral, X_89), true, icext(uri_rdfs_Literal, X_89), true)=true))). % 27.03/17.13 tff(c_4610, plain, (ip(uri_rdfs_member)=true)). % 27.03/17.13 tff(c_4550, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__3, uri_rdfs_member)=true)). % 27.03/17.13 tff(c_4489, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_rest, uri_rdf_rest)=true)). % 27.03/17.13 tff(c_1505, plain, (![X_89]: (ifeq(icext(uri_rdfs_Seq, X_89), true, icext(uri_rdfs_Container, X_89), true)=true))). % 27.03/17.13 tff(c_1816, plain, (![X_93, Y_94]: (ifeq(iext(uri_rdf_predicate, X_93, Y_94), true, true, true)=true))). % 27.03/17.13 tff(c_4421, plain, (![X_135]: (iext(uri_rdf_type, X_135, uri_rdfs_Resource)=true))). % 27.03/17.13 tff(c_1839, plain, (![X_93, Y_94]: (ifeq(iext(uri_rdf_first, X_93, Y_94), true, true, true)=true))). % 27.03/17.13 tff(c_2158, plain, (![X_97, Y_98]: (ifeq(iext(uri_rdf__2, X_97, Y_98), true, true, true)=true))). % 27.03/17.13 tff(c_2172, plain, (![X_97, Y_98]: (ifeq(iext(uri_rdfs_comment, X_97, Y_98), true, true, true)=true))). % 27.03/17.13 tff(c_1823, plain, (![X_93, Y_94]: (ifeq(iext(uri_rdf_subject, X_93, Y_94), true, true, true)=true))). % 27.03/17.13 tff(c_1852, plain, (![X_93, Y_94]: (ifeq(iext(uri_rdfs_seeAlso, X_93, Y_94), true, true, true)=true))). % 27.03/17.13 tff(c_2152, plain, (![X_97, Y_98]: (ifeq(iext(uri_rdf__3, X_97, Y_98), true, true, true)=true))). % 27.03/17.13 tff(c_2154, plain, (![X_97, Y_98]: (ifeq(iext(uri_rdf_value, X_97, Y_98), true, true, true)=true))). % 27.03/17.13 tff(c_1829, plain, (![X_93, Y_94]: (ifeq(iext(uri_rdfs_isDefinedBy, X_93, Y_94), true, true, true)=true))). % 27.03/17.13 tff(c_1802, plain, (![X_93, Y_94]: (ifeq(iext(uri_rdf__1, X_93, Y_94), true, true, true)=true))). % 27.03/17.13 tff(c_4294, plain, (icext(uri_rdfs_Class, uri_rdf_Alt)=true)). % 27.03/17.13 tff(c_4241, plain, (icext(uri_rdfs_Class, uri_rdfs_Class)=true)). % 27.03/17.13 tff(c_2165, plain, (![X_97, Y_98]: (ifeq(iext(uri_rdfs_member, X_97, Y_98), true, true, true)=true))). % 27.03/17.13 tff(c_4195, plain, (icext(uri_rdfs_Class, uri_rdfs_Seq)=true)). % 27.03/17.13 tff(c_4132, plain, (icext(uri_rdfs_Class, uri_rdfs_Container)=true)). % 27.03/17.13 tff(c_4088, plain, (icext(uri_rdfs_Class, uri_rdfs_Literal)=true)). % 27.03/17.13 tff(c_4029, plain, (icext(uri_rdfs_Class, uri_rdf_Bag)=true)). % 27.03/17.13 tff(c_2177, plain, (![X_97, Y_98]: (ifeq(iext(uri_rdfs_label, X_97, Y_98), true, true, true)=true))). % 27.03/17.13 tff(c_3983, plain, (icext(uri_rdfs_Class, uri_rdfs_Datatype)=true)). % 27.03/17.13 tff(c_3937, plain, (icext(uri_rdfs_Class, uri_rdfs_ContainerMembershipProperty)=true)). % 27.03/17.13 tff(c_3841, plain, (icext(uri_rdfs_Class, uri_rdf_XMLLiteral)=true)). % 27.03/17.13 tff(c_2186, plain, (![X_97, Y_98]: (ifeq(iext(uri_rdf_type, X_97, Y_98), true, true, true)=true))). % 27.03/17.13 tff(c_3785, plain, (icext(uri_rdfs_Class, uri_rdf_Property)=true)). % 27.03/17.13 tff(c_3746, plain, (icext(uri_rdf_Property, uri_rdf__3)=true)). % 27.03/17.13 tff(c_3707, plain, (icext(uri_rdf_Property, uri_rdf_rest)=true)). % 27.03/17.13 tff(c_3664, plain, (icext(uri_rdf_Property, uri_rdf_type)=true)). % 27.03/17.13 tff(c_3617, plain, (icext(uri_rdf_List, uri_rdf_nil)=true)). % 27.03/17.13 tff(c_3573, plain, (icext(uri_rdf_Property, uri_rdf_value)=true)). % 27.03/17.13 tff(c_3533, plain, (icext(uri_rdf_Property, uri_rdf__1)=true)). % 27.03/17.13 tff(c_3496, plain, (icext(uri_rdf_Property, uri_rdf__2)=true)). % 27.03/17.13 tff(c_3426, plain, (icext(uri_rdf_Property, uri_rdf_object)=true)). % 27.03/17.13 tff(c_3416, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__3)=true)). % 27.03/17.13 tff(c_3373, plain, (icext(uri_rdfs_Datatype, uri_rdf_XMLLiteral)=true)). % 27.03/17.13 tff(c_3332, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__2)=true)). % 27.03/17.13 tff(c_3277, plain, (icext(uri_rdf_Property, uri_rdf_first)=true)). % 27.03/17.13 tff(c_3237, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__1)=true)). % 27.03/17.13 tff(c_3196, plain, (icext(uri_rdf_Property, uri_rdf_subject)=true)). % 27.03/17.13 tff(c_3155, plain, (ip(uri_rdf__3)=true)). % 27.03/17.13 tff(c_3103, plain, (ip(uri_rdf_object)=true)). % 27.03/17.13 tff(c_3059, plain, (ic(uri_rdfs_Seq)=true)). % 27.03/17.13 tff(c_3022, plain, (ip(uri_rdf_rest)=true)). % 27.03/17.13 tff(c_2979, plain, (ip(uri_rdf_subject)=true)). % 27.03/17.13 tff(c_2938, plain, (ip(uri_rdf_first)=true)). % 27.03/17.13 tff(c_2893, plain, (ic(uri_rdf_XMLLiteral)=true)). % 27.03/17.13 tff(c_182, plain, (tuple(iext(uri_rdfs_subClassOf, uri_owl_Class, uri_owl_Thing), iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_owl_Class), iext(uri_rdf_type, uri_owl_Class, uri_owl_Class), iext(uri_rdf_type, uri_owl_Class, uri_owl_Thing), iext(uri_owl_equivalentClass, uri_owl_Class, uri_rdfs_Class))!=tuple(true, true, true, true, true))). % 27.03/17.13 tff(c_2848, plain, (ic(uri_rdf_Property)=true)). % 27.03/17.13 tff(c_2742, plain, (ip(uri_rdf_value)=true)). % 27.03/17.13 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))). % 27.03/17.13 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))). % 27.03/17.13 tff(c_2681, plain, (ip(uri_rdfs_seeAlso)=true)). % 27.03/17.13 tff(c_2219, plain, (ic(uri_rdf_Alt)=true)). % 27.03/17.13 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))). % 27.03/17.13 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))). % 27.03/17.13 tff(c_1867, plain, (ic(uri_rdfs_Literal)=true)). % 27.03/17.13 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))). % 27.03/17.13 tff(c_1513, plain, (ip(uri_rdfs_subPropertyOf)=true)). % 27.03/17.13 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))). % 27.03/17.13 tff(c_1441, plain, (ip(uri_rdfs_subClassOf)=true)). % 27.03/17.13 tff(c_1402, plain, (ip(uri_rdf__2)=true)). % 27.03/17.13 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))). % 27.03/17.13 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))). % 27.03/17.13 tff(c_1295, plain, (ip(uri_rdf__1)=true)). % 27.03/17.13 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))). % 27.03/17.13 tff(c_1195, plain, (ic(uri_rdfs_ContainerMembershipProperty)=true)). % 27.03/17.13 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))). % 27.03/17.13 tff(c_1160, plain, (ic(uri_rdf_Bag)=true)). % 27.03/17.13 tff(c_170, plain, (![P_51]: (ifeq(ip(P_51), true, iext(uri_rdfs_subPropertyOf, P_51, P_51), true)=true))). % 27.03/17.13 tff(c_1105, plain, (ic(uri_rdfs_Class)=true)). % 27.03/17.14 tff(c_156, plain, (![C_39]: (ifeq(ic(C_39), true, iext(uri_rdfs_subClassOf, C_39, C_39), true)=true))). % 27.03/17.14 tff(c_28, plain, (![P_9]: (ifeq(ip(P_9), true, iext(uri_rdf_type, P_9, uri_rdf_Property), true)=true))). % 27.03/17.14 tff(c_991, plain, (ic(uri_rdfs_Datatype)=true)). % 27.03/17.14 tff(c_152, plain, (![C_37, D_38]: (ifeq(iext(uri_rdfs_subClassOf, C_37, D_38), true, ic(C_37), true)=true))). % 27.03/17.14 tff(c_926, plain, (ip(uri_rdfs_domain)=true)). % 27.03/17.14 tff(c_162, plain, (![P_43, Q_44]: (ifeq(iext(uri_rdfs_subPropertyOf, P_43, Q_44), true, ip(Q_44), true)=true))). % 27.03/17.14 tff(c_861, plain, (ip(uri_rdf_type)=true)). % 27.03/17.14 tff(c_30, plain, (![P_10]: (ifeq(iext(uri_rdf_type, P_10, uri_rdf_Property), true, ip(P_10), true)=true))). % 27.03/17.14 tff(c_789, plain, (ip(uri_rdfs_range)=true)). % 27.03/17.14 tff(c_4, plain, (![P_4, S_5, O_6]: (ifeq(iext(P_4, S_5, O_6), true, ip(P_4), true)=true))). % 27.03/17.14 tff(c_564, plain, (ic(uri_rdfs_Container)=true)). % 27.03/17.14 tff(c_150, plain, (![C_35, D_36]: (ifeq(iext(uri_rdfs_subClassOf, C_35, D_36), true, ic(D_36), true)=true))). % 27.03/17.14 tff(c_519, plain, (ip(uri_rdfs_isDefinedBy)=true)). % 27.03/17.14 tff(c_164, plain, (![P_45, Q_46]: (ifeq(iext(uri_rdfs_subPropertyOf, P_45, Q_46), true, ip(P_45), true)=true))). % 27.03/17.14 tff(c_58, plain, (![C_15]: (ifeq(ic(C_15), true, iext(uri_rdfs_subClassOf, C_15, uri_rdfs_Resource), true)=true))). % 27.03/17.14 tff(c_122, plain, (![X_26]: (ifeq(icext(uri_rdfs_Literal, X_26), true, lv(X_26), true)=true))). % 27.03/17.14 tff(c_124, plain, (![X_27]: (ifeq(lv(X_27), true, icext(uri_rdfs_Literal, X_27), true)=true))). % 27.03/17.14 tff(c_116, plain, (![X_23]: (ifeq(icext(uri_rdfs_Class, X_23), true, ic(X_23), true)=true))). % 27.03/17.14 tff(c_114, plain, (![X_22]: (ifeq(ic(X_22), true, icext(uri_rdfs_Class, X_22), true)=true))). % 27.03/17.14 tff(c_452, plain, (![X_60]: (icext(uri_rdfs_Resource, X_60)=true))). % 27.03/17.14 tff(c_187, plain, (![X_8]: (ifeq(lv(X_8), true, true, true)=true))). % 27.03/17.14 tff(c_2, plain, (![A_1, B_2, C_3]: (ifeq(A_1, A_1, B_2, C_3)=B_2))). % 27.03/17.14 tff(c_20, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdf_Property)=true)). % 27.03/17.14 tff(c_40, plain, (iext(uri_rdfs_domain, uri_rdfs_isDefinedBy, uri_rdfs_Resource)=true)). % 27.03/17.14 tff(c_88, plain, (iext(uri_rdfs_range, uri_rdf__2, uri_rdfs_Resource)=true)). % 27.03/17.14 tff(c_134, plain, (iext(uri_rdfs_domain, uri_rdf_object, uri_rdfs_Statement)=true)). % 27.03/17.14 tff(c_138, plain, (iext(uri_rdfs_domain, uri_rdf_predicate, uri_rdfs_Statement)=true)). % 27.03/17.14 tff(c_90, plain, (iext(uri_rdfs_range, uri_rdf__3, uri_rdfs_Resource)=true)). % 27.03/17.14 tff(c_84, plain, (iext(uri_rdfs_domain, uri_rdf__3, uri_rdfs_Resource)=true)). % 27.03/17.14 tff(c_178, plain, (iext(uri_rdfs_domain, uri_rdf_value, uri_rdfs_Resource)=true)). % 27.03/17.14 tff(c_12, plain, (iext(uri_rdf_type, uri_rdf_nil, uri_rdf_List)=true)). % 27.03/17.14 tff(c_160, plain, (iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 27.03/17.14 tff(c_82, plain, (iext(uri_rdfs_domain, uri_rdf__2, uri_rdfs_Resource)=true)). % 27.03/17.14 tff(c_86, plain, (iext(uri_rdfs_range, uri_rdf__1, uri_rdfs_Resource)=true)). % 27.03/17.14 tff(c_80, plain, (iext(uri_rdfs_domain, uri_rdf__1, uri_rdfs_Resource)=true)). % 27.03/17.14 tff(c_132, plain, (iext(uri_rdfs_range, uri_rdfs_range, uri_rdfs_Class)=true)). % 27.03/17.14 tff(c_92, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdfs_ContainerMembershipProperty)=true)). % 27.03/17.14 tff(c_76, plain, (iext(uri_rdfs_domain, uri_rdfs_member, uri_rdfs_Resource)=true)). % 27.03/17.14 tff(c_14, plain, (iext(uri_rdf_type, uri_rdf_rest, uri_rdf_Property)=true)). % 27.03/17.14 tff(c_44, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso)=true)). % 27.03/17.14 tff(c_94, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdfs_ContainerMembershipProperty)=true)). % 27.03/17.14 tff(c_48, plain, (iext(uri_rdfs_range, uri_rdfs_label, uri_rdfs_Literal)=true)). % 27.03/17.14 tff(c_22, plain, (iext(uri_rdf_type, uri_rdf_object, uri_rdf_Property)=true)). % 27.03/17.14 tff(c_36, plain, (iext(uri_rdfs_domain, uri_rdfs_comment, uri_rdfs_Resource)=true)). % 27.03/17.14 tff(c_68, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Container)=true)). % 27.03/17.14 tff(c_26, plain, (iext(uri_rdf_type, uri_rdf_subject, uri_rdf_Property)=true)). % 27.03/17.14 tff(c_140, plain, (iext(uri_rdfs_range, uri_rdf_predicate, uri_rdfs_Resource)=true)). % 27.03/17.14 tff(c_46, plain, (iext(uri_rdfs_domain, uri_rdfs_label, uri_rdfs_Resource)=true)). % 27.03/17.14 tff(c_38, plain, (iext(uri_rdfs_range, uri_rdfs_comment, uri_rdfs_Literal)=true)). % 27.03/17.14 tff(c_128, plain, (iext(uri_rdfs_domain, uri_rdfs_range, uri_rdf_Property)=true)). % 27.03/17.14 tff(c_142, plain, (iext(uri_rdfs_domain, uri_rdf_subject, uri_rdfs_Statement)=true)). % 27.03/17.14 tff(c_176, plain, (iext(uri_rdfs_range, uri_rdf_type, uri_rdfs_Class)=true)). % 27.03/17.14 tff(c_144, plain, (iext(uri_rdfs_range, uri_rdf_subject, uri_rdfs_Resource)=true)). % 27.03/17.14 tff(c_154, plain, (iext(uri_rdfs_range, uri_rdfs_subClassOf, uri_rdfs_Class)=true)). % 27.03/17.14 tff(c_100, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Literal)=true)). % 27.03/17.14 tff(c_174, plain, (iext(uri_rdfs_domain, uri_rdf_type, uri_rdfs_Resource)=true)). % 27.03/17.14 tff(c_64, plain, (iext(uri_rdfs_domain, uri_rdf_rest, uri_rdf_List)=true)). % 27.03/17.14 tff(c_42, plain, (iext(uri_rdfs_range, uri_rdfs_isDefinedBy, uri_rdfs_Resource)=true)). % 27.03/17.14 tff(c_146, plain, (iext(uri_rdfs_domain, uri_rdfs_subClassOf, uri_rdfs_Class)=true)). % 27.03/17.14 tff(c_78, plain, (iext(uri_rdfs_range, uri_rdfs_member, uri_rdfs_Resource)=true)). % 27.03/17.14 tff(c_34, plain, (iext(uri_rdf_type, uri_rdf_type, uri_rdf_Property)=true)). % 27.03/17.14 tff(c_102, plain, (iext(uri_rdf_type, uri_rdf_XMLLiteral, uri_rdfs_Datatype)=true)). % 27.03/17.14 tff(c_98, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Container)=true)). % 27.03/17.14 tff(c_108, plain, (iext(uri_rdfs_domain, uri_rdfs_domain, uri_rdf_Property)=true)). % 27.03/17.14 tff(c_126, plain, (iext(uri_rdf_type, uri_rdf_Property, uri_rdfs_Class)=true)). % 27.03/17.14 tff(c_62, plain, (iext(uri_rdfs_range, uri_rdf_first, uri_rdfs_Resource)=true)). % 27.03/17.14 tff(c_70, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Container)=true)). % 27.03/17.14 tff(c_74, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property)=true)). % 27.03/17.14 tff(c_18, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdf_Property)=true)). % 27.03/17.14 tff(c_16, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdf_Property)=true)). % 27.03/17.14 tff(c_106, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Class)=true)). % 27.03/17.14 tff(c_60, plain, (iext(uri_rdfs_domain, uri_rdf_first, uri_rdf_List)=true)). % 27.03/17.14 tff(c_24, plain, (iext(uri_rdf_type, uri_rdf_value, uri_rdf_Property)=true)). % 27.03/17.14 tff(c_10, plain, (iext(uri_rdf_type, uri_rdf_first, uri_rdf_Property)=true)). % 27.03/17.14 tff(c_96, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdfs_ContainerMembershipProperty)=true)). % 27.03/17.14 tff(c_66, plain, (iext(uri_rdfs_range, uri_rdf_rest, uri_rdf_List)=true)). % 27.03/17.14 tff(c_50, plain, (iext(uri_rdfs_domain, uri_rdfs_seeAlso, uri_rdfs_Resource)=true)). % 27.03/17.14 tff(c_52, plain, (iext(uri_rdfs_range, uri_rdfs_seeAlso, uri_rdfs_Resource)=true)). % 27.03/17.14 tff(c_112, plain, (iext(uri_rdfs_range, uri_rdfs_domain, uri_rdfs_Class)=true)). % 27.03/17.14 tff(c_168, plain, (iext(uri_rdfs_range, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 27.03/17.14 tff(c_180, plain, (iext(uri_rdfs_range, uri_rdf_value, uri_rdfs_Resource)=true)). % 27.03/17.14 tff(c_6, plain, (![X_7]: (ir(X_7)=true))). % 27.03/17.14 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 27.03/17.14 %------------------------------------------------------------------------------