%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SWB021-10 : TPTP v9.0.0. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n024.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:53 PM UTC 2025 % Result : Satisfiable 35.02s 22.96s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SWB021-10 : TPTP v9.0.0. Released v7.5.0. % 0.03/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 : n024.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:59:51 EDT 2025 % 0.13/0.34 % CPUTime : % 35.02/22.95 % 35.02/22.96 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 35.02/22.96 % 35.02/22.96 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 35.02/22.98 %$ ifeq > iext > icext > #nlpp > lv > ir > ip > ic > uri_rdfs_subPropertyOf > uri_rdfs_subClassOf > uri_rdfs_seeAlso > uri_rdfs_range > uri_rdfs_member > uri_rdfs_label > uri_rdfs_isDefinedBy > uri_rdfs_domain > uri_rdfs_comment > uri_rdfs_Statement > uri_rdfs_Seq > uri_rdfs_Resource > uri_rdfs_Literal > uri_rdfs_Datatype > uri_rdfs_ContainerMembershipProperty > uri_rdfs_Container > uri_rdfs_Class > uri_rdf_value > uri_rdf_type > uri_rdf_subject > uri_rdf_rest > uri_rdf_predicate > uri_rdf_object > uri_rdf_nil > uri_rdf_first > uri_rdf__3 > uri_rdf__2 > uri_rdf__1 > uri_rdf_XMLLiteral > uri_rdf_Property > uri_rdf_List > uri_rdf_Bag > uri_rdf_Alt > uri_owl_unionOf > uri_owl_oneOf > uri_owl_equivalentClass > uri_ex_w3 > uri_ex_w2 > uri_ex_w1 > uri_ex_c4 > uri_ex_c3 > uri_ex_c2 > uri_ex_c1 > true > sK9_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l12 > sK8_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l11 > sK7_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l22 > sK6_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l21 > sK5_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l32 > sK4_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l31 > sK3_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l33 > sK2_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l42 > sK1_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l41 % 35.02/22.98 % 35.02/22.98 %Foreground sorts: % 35.02/22.98 % 35.02/22.98 % 35.02/22.98 %Background operators: % 35.02/22.98 % 35.02/22.98 % 35.02/22.98 %Foreground operators: % 35.02/22.98 tff(sK7_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l22, type, sK7_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l22: $i). % 35.02/22.98 tff(uri_rdfs_Datatype, type, uri_rdfs_Datatype: $i). % 35.02/22.98 tff(uri_rdfs_ContainerMembershipProperty, type, uri_rdfs_ContainerMembershipProperty: $i). % 35.02/22.98 tff(uri_owl_oneOf, type, uri_owl_oneOf: $i). % 35.02/22.98 tff(uri_rdfs_Resource, type, uri_rdfs_Resource: $i). % 35.02/22.98 tff(uri_rdf_Property, type, uri_rdf_Property: $i). % 35.02/22.98 tff(uri_rdf_subject, type, uri_rdf_subject: $i). % 35.02/22.98 tff(uri_owl_equivalentClass, type, uri_owl_equivalentClass: $i). % 35.02/22.98 tff(uri_rdf_type, type, uri_rdf_type: $i). % 35.02/22.98 tff(uri_rdfs_subPropertyOf, type, uri_rdfs_subPropertyOf: $i). % 35.02/22.98 tff(uri_ex_c4, type, uri_ex_c4: $i). % 35.02/22.98 tff(sK5_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l32, type, sK5_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l32: $i). % 35.02/22.98 tff(uri_rdfs_seeAlso, type, uri_rdfs_seeAlso: $i). % 35.02/22.98 tff(icext, type, icext: ($i * $i) > $i). % 35.02/22.98 tff(uri_rdfs_range, type, uri_rdfs_range: $i). % 35.02/22.98 tff(uri_rdf_XMLLiteral, type, uri_rdf_XMLLiteral: $i). % 35.02/22.98 tff(uri_rdf_List, type, uri_rdf_List: $i). % 35.02/22.98 tff(sK2_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l42, type, sK2_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l42: $i). % 35.02/22.98 tff(uri_rdf_first, type, uri_rdf_first: $i). % 35.02/22.98 tff(uri_rdf_predicate, type, uri_rdf_predicate: $i). % 35.02/22.98 tff(uri_ex_c2, type, uri_ex_c2: $i). % 35.02/22.98 tff(ir, type, ir: $i > $i). % 35.02/22.98 tff(lv, type, lv: $i > $i). % 35.02/22.98 tff(uri_rdf__3, type, uri_rdf__3: $i). % 35.02/22.98 tff(uri_ex_c3, type, uri_ex_c3: $i). % 35.02/22.98 tff(uri_rdf_value, type, uri_rdf_value: $i). % 35.02/22.98 tff(ic, type, ic: $i > $i). % 35.02/22.98 tff(uri_ex_w3, type, uri_ex_w3: $i). % 35.02/22.98 tff(sK6_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l21, type, sK6_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l21: $i). % 35.02/22.98 tff(uri_rdfs_Statement, type, uri_rdfs_Statement: $i). % 35.02/22.98 tff(uri_rdf__1, type, uri_rdf__1: $i). % 35.02/22.98 tff(iext, type, iext: ($i * $i * $i) > $i). % 35.02/22.98 tff(sK9_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l12, type, sK9_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l12: $i). % 35.02/22.98 tff(sK8_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l11, type, sK8_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l11: $i). % 35.02/22.98 tff(uri_owl_unionOf, type, uri_owl_unionOf: $i). % 35.02/22.98 tff(uri_rdf_rest, type, uri_rdf_rest: $i). % 35.02/22.98 tff(uri_rdfs_label, type, uri_rdfs_label: $i). % 35.02/22.98 tff(uri_rdfs_Container, type, uri_rdfs_Container: $i). % 35.02/22.98 tff(uri_rdfs_subClassOf, type, uri_rdfs_subClassOf: $i). % 35.02/22.98 tff(uri_ex_w1, type, uri_ex_w1: $i). % 35.02/22.98 tff(uri_rdf_object, type, uri_rdf_object: $i). % 35.02/22.98 tff(ip, type, ip: $i > $i). % 35.02/22.98 tff(uri_rdfs_Class, type, uri_rdfs_Class: $i). % 35.02/22.98 tff(uri_rdfs_Seq, type, uri_rdfs_Seq: $i). % 35.02/22.98 tff(uri_ex_c1, type, uri_ex_c1: $i). % 35.02/22.98 tff(uri_rdfs_member, type, uri_rdfs_member: $i). % 35.02/22.98 tff(uri_rdf_Bag, type, uri_rdf_Bag: $i). % 35.02/22.98 tff(uri_rdf__2, type, uri_rdf__2: $i). % 35.02/22.98 tff(uri_ex_w2, type, uri_ex_w2: $i). % 35.02/22.98 tff(uri_rdfs_comment, type, uri_rdfs_comment: $i). % 35.02/22.98 tff(uri_rdfs_Literal, type, uri_rdfs_Literal: $i). % 35.02/22.98 tff(true, type, true: $i). % 35.02/22.98 tff(uri_rdf_Alt, type, uri_rdf_Alt: $i). % 35.02/22.98 tff(uri_rdf_nil, type, uri_rdf_nil: $i). % 35.02/22.98 tff(sK1_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l41, type, sK1_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l41: $i). % 35.02/22.98 tff(sK3_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l33, type, sK3_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l33: $i). % 35.02/22.98 tff(uri_rdfs_isDefinedBy, type, uri_rdfs_isDefinedBy: $i). % 35.02/22.98 tff(sK4_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l31, type, sK4_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l31: $i). % 35.02/22.98 tff(uri_rdfs_domain, type, uri_rdfs_domain: $i). % 35.02/22.98 tff(ifeq, type, ifeq: ($i * $i * $i * $i) > $i). % 35.02/22.98 % 35.02/22.98 %Saturated clause set: % 35.02/22.98 tff(c_15037, 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))). % 35.02/22.98 tff(c_74759, plain, (![X_1307, Y_1308]: (ifeq(iext(uri_rdf_predicate, X_1307, Y_1308), true, iext(uri_rdf_predicate, X_1307, Y_1308), true)=true))). % 35.02/22.98 tff(c_17192, 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))). % 35.02/22.98 tff(c_14984, 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))). % 35.02/22.98 tff(c_74490, plain, (![X_1301, Y_1302]: (ifeq(iext(uri_rdfs_comment, X_1301, Y_1302), true, iext(uri_rdfs_comment, X_1301, Y_1302), true)=true))). % 35.02/22.98 tff(c_74342, plain, (![X_1296, Y_1297]: (ifeq(iext(uri_rdfs_label, X_1296, Y_1297), true, iext(uri_rdfs_label, X_1296, Y_1297), true)=true))). % 35.02/22.98 tff(c_17920, 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))). % 35.02/22.98 tff(c_6796, 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))). % 35.02/22.98 tff(c_14915, 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))). % 35.02/22.98 tff(c_14808, 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))). % 35.02/22.98 tff(c_6799, 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))). % 35.02/22.98 tff(c_73676, plain, (![X_1286, Y_1287]: (ifeq(iext(uri_rdfs_member, X_1286, Y_1287), true, iext(uri_rdfs_member, X_1286, Y_1287), true)=true))). % 35.02/22.98 tff(c_73536, plain, (![C_1284]: (ifeq(iext(uri_rdfs_subClassOf, C_1284, uri_rdf_List), true, iext(uri_rdfs_subClassOf, C_1284, uri_rdfs_Resource), true)=true))). % 35.02/22.98 tff(c_73397, plain, (![C_1282]: (ifeq(iext(uri_rdfs_subClassOf, C_1282, uri_rdfs_Statement), true, iext(uri_rdfs_subClassOf, C_1282, uri_rdfs_Resource), true)=true))). % 35.02/22.98 tff(c_14543, 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))). % 35.02/22.98 tff(c_14609, 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))). % 35.02/22.98 tff(c_14014, 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))). % 35.02/22.98 tff(c_14183, 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))). % 35.02/22.98 tff(c_7331, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_owl_unionOf, Y_21), true, true, true), true)=true))). % 35.02/22.98 tff(c_6449, 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))). % 35.02/22.98 tff(c_13928, 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))). % 35.02/22.98 tff(c_13231, 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))). % 35.02/22.98 tff(c_13357, 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))). % 35.02/22.98 tff(c_8693, 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))). % 35.02/22.98 tff(c_7334, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_owl_unionOf), true, true, true), true)=true))). % 35.02/22.98 tff(c_13404, 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))). % 35.02/22.98 tff(c_13451, 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))). % 35.02/22.98 tff(c_8449, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_owl_oneOf, Y_21), true, true, true), true)=true))). % 35.02/22.98 tff(c_5589, 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))). % 35.02/22.98 tff(c_8452, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_owl_oneOf), true, true, true), true)=true))). % 35.02/22.98 tff(c_13499, 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))). % 35.02/22.98 tff(c_5592, 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))). % 35.02/22.98 tff(c_13880, 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))). % 35.02/22.98 tff(c_8696, 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))). % 35.02/22.98 tff(c_13546, 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))). % 35.02/22.98 tff(c_13309, 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))). % 35.02/22.98 tff(c_6446, 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))). % 35.02/22.98 tff(c_13833, 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))). % 35.02/22.99 tff(c_17056, 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))). % 35.02/22.99 tff(c_12906, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, sK2_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l42, uri_rdf_List), true, true, true), true)=true))). % 35.02/22.99 tff(c_13088, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, sK6_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l21, uri_rdf_List), true, true, true), true)=true))). % 35.02/22.99 tff(c_14487, 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))). % 35.02/22.99 tff(c_12611, 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))). % 35.02/22.99 tff(c_13136, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, sK1_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l41, uri_rdf_List), true, true, true), true)=true))). % 35.02/22.99 tff(c_12715, 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))). % 35.02/22.99 tff(c_13183, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, sK4_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l31, uri_rdf_List), true, true, true), true)=true))). % 35.02/22.99 tff(c_16634, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, sK5_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l32, uri_rdf_List), true, true, true), true)=true))). % 35.02/22.99 tff(c_12666, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, sK7_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l22, uri_rdf_List), true, true, true), true)=true))). % 35.02/22.99 tff(c_18105, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, sK8_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l11, uri_rdf_List), true, true, true), true)=true))). % 35.02/22.99 tff(c_12839, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, sK9_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l12, uri_rdf_List), true, true, true), true)=true))). % 35.02/22.99 tff(c_16142, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, sK3_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l33, uri_rdf_List), true, true, true), true)=true))). % 35.02/22.99 tff(c_17683, 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))). % 35.02/22.99 tff(c_68681, plain, (![X_1230, Y_1231]: (ifeq(iext(uri_rdf_value, X_1230, Y_1231), true, iext(uri_rdf_value, X_1230, Y_1231), true)=true))). % 35.02/22.99 tff(c_4795, 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))). % 35.02/22.99 tff(c_8395, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_owl_oneOf, uri_rdf_Property), true, true, true), true)=true))). % 35.02/22.99 tff(c_10148, 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))). % 35.02/22.99 tff(c_68276, plain, (![X_1222, Y_1223]: (ifeq(iext(uri_rdfs_seeAlso, X_1222, Y_1223), true, iext(uri_rdfs_seeAlso, X_1222, Y_1223), true)=true))). % 35.02/22.99 tff(c_68209, plain, (![P_1220]: (ifeq(iext(uri_rdfs_subPropertyOf, P_1220, uri_rdf__1), true, iext(uri_rdfs_subPropertyOf, P_1220, uri_rdfs_member), true)=true))). % 35.02/22.99 tff(c_5169, 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))). % 35.02/22.99 tff(c_68061, plain, (![X_1215, Y_1216]: (ifeq(iext(uri_rdf__3, X_1215, Y_1216), true, iext(uri_rdfs_member, X_1215, Y_1216), true)=true))). % 35.02/22.99 tff(c_67922, plain, (![C_1213]: (ifeq(iext(uri_rdfs_subClassOf, C_1213, uri_rdfs_Seq), true, iext(uri_rdfs_subClassOf, C_1213, uri_rdfs_Resource), true)=true))). % 35.02/22.99 tff(c_7524, 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))). % 35.02/22.99 tff(c_11922, 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))). % 35.02/22.99 tff(c_11160, 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))). % 35.02/22.99 tff(c_4607, 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))). % 35.02/22.99 tff(c_7213, 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))). % 35.02/22.99 tff(c_67237, plain, (![P_1205]: (ifeq(iext(uri_rdfs_subPropertyOf, P_1205, uri_rdf__3), true, iext(uri_rdfs_subPropertyOf, P_1205, uri_rdfs_member), true)=true))). % 35.02/22.99 tff(c_10216, 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))). % 35.02/22.99 tff(c_4647, 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))). % 35.02/22.99 tff(c_7442, 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))). % 35.02/22.99 tff(c_5275, 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))). % 35.02/22.99 tff(c_66595, plain, (![C_1198]: (ifeq(iext(uri_rdfs_subClassOf, C_1198, uri_rdfs_Datatype), true, iext(uri_rdfs_subClassOf, C_1198, uri_rdfs_Resource), true)=true))). % 35.02/22.99 tff(c_11775, 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))). % 35.02/22.99 tff(c_8982, 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))). % 35.02/22.99 tff(c_4564, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, uri_rdfs_Literal), true, true, true), true)=true))). % 35.02/22.99 tff(c_7032, 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))). % 35.02/22.99 tff(c_11653, 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))). % 35.02/22.99 tff(c_9827, 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))). % 35.02/22.99 tff(c_65029, plain, (![X_1187, Y_1188]: (ifeq(iext(uri_rdf_type, X_1187, Y_1188), true, iext(uri_rdf_type, X_1187, Y_1188), true)=true))). % 35.02/22.99 tff(c_9370, 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))). % 35.19/22.99 tff(c_5471, 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))). % 35.19/22.99 tff(c_11225, 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))). % 35.19/22.99 tff(c_4747, 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))). % 35.19/22.99 tff(c_7681, 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))). % 35.19/22.99 tff(c_6363, 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))). % 35.19/22.99 tff(c_11093, 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))). % 35.19/22.99 tff(c_64125, plain, (![X_1175, Y_1176]: (ifeq(iext(uri_rdf_object, X_1175, Y_1176), true, iext(uri_rdf_object, X_1175, Y_1176), true)=true))). % 35.19/22.99 tff(c_11026, 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))). % 35.19/22.99 tff(c_63978, plain, (![X_1170, Y_1171]: (ifeq(iext(uri_rdfs_isDefinedBy, X_1170, Y_1171), true, iext(uri_rdfs_isDefinedBy, X_1170, Y_1171), true)=true))). % 35.19/22.99 tff(c_8898, 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))). % 35.19/22.99 tff(c_7274, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_owl_unionOf, uri_rdf_Property), true, true, true), true)=true))). % 35.19/22.99 tff(c_63422, plain, (![X_1164, Y_1165]: (ifeq(iext(uri_rdfs_range, X_1164, Y_1165), true, iext(uri_rdfs_range, X_1164, Y_1165), true)=true))). % 35.19/22.99 tff(c_11860, 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))). % 35.19/22.99 tff(c_4840, 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))). % 35.19/22.99 tff(c_9891, 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))). % 35.19/22.99 tff(c_62876, plain, (![C_1158]: (ifeq(iext(uri_rdfs_subClassOf, C_1158, uri_rdfs_Container), true, iext(uri_rdfs_subClassOf, C_1158, uri_rdfs_Resource), true)=true))). % 35.19/22.99 tff(c_8827, 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))). % 35.19/22.99 tff(c_62548, plain, (![P_1153]: (ifeq(iext(uri_rdfs_subPropertyOf, P_1153, uri_rdf__2), true, iext(uri_rdfs_subPropertyOf, P_1153, uri_rdfs_member), true)=true))). % 35.19/22.99 tff(c_4604, 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))). % 35.19/22.99 tff(c_62520, plain, (![X_1149, Y_1150]: (ifeq(iext(uri_rdf_subject, X_1149, Y_1150), true, iext(uri_rdf_subject, X_1149, Y_1150), true)=true))). % 35.19/22.99 tff(c_4843, 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))). % 35.19/23.00 tff(c_10810, 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))). % 35.19/23.00 tff(c_62239, plain, (![X_1142, Y_1143]: (ifeq(iext(uri_rdf__1, X_1142, Y_1143), true, iext(uri_rdfs_member, X_1142, Y_1143), true)=true))). % 35.19/23.00 tff(c_10481, 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))). % 35.19/23.00 tff(c_4887, 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))). % 35.19/23.00 tff(c_11722, 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))). % 35.19/23.00 tff(c_61833, plain, (![X_1134, Y_1135]: (ifeq(iext(uri_rdf__2, X_1134, Y_1135), true, iext(uri_rdf__2, X_1134, Y_1135), true)=true))). % 35.19/23.00 tff(c_61502, plain, (![X_1130, Y_1131]: (ifeq(iext(uri_rdfs_domain, X_1130, Y_1131), true, iext(uri_rdfs_domain, X_1130, Y_1131), true)=true))). % 35.19/23.00 tff(c_61362, plain, (![C_1128]: (ifeq(iext(uri_rdfs_subClassOf, C_1128, uri_rdfs_ContainerMembershipProperty), true, iext(uri_rdfs_subClassOf, C_1128, uri_rdfs_Resource), true)=true))). % 35.19/23.00 tff(c_61221, plain, (![C_1126]: (ifeq(iext(uri_rdfs_subClassOf, C_1126, uri_rdf_Alt), true, iext(uri_rdfs_subClassOf, C_1126, uri_rdfs_Resource), true)=true))). % 35.19/23.00 tff(c_61073, plain, (![C_1124]: (ifeq(iext(uri_rdfs_subClassOf, C_1124, uri_rdfs_Class), true, iext(uri_rdfs_subClassOf, C_1124, uri_rdfs_Resource), true)=true))). % 35.19/23.00 tff(c_6654, 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))). % 35.19/23.00 tff(c_4744, 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))). % 35.19/23.00 tff(c_4699, 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))). % 35.19/23.00 tff(c_4798, 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))). % 35.19/23.00 tff(c_60506, plain, (![X_1113, Y_1114]: (ifeq(iext(uri_owl_unionOf, X_1113, Y_1114), true, iext(uri_owl_unionOf, X_1113, Y_1114), true)=true))). % 35.19/23.00 tff(c_59911, plain, (![X_1109, Y_1110]: (ifeq(iext(uri_rdfs_subClassOf, X_1109, Y_1110), true, iext(uri_rdfs_subClassOf, X_1109, Y_1110), true)=true))). % 35.19/23.00 tff(c_10959, 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))). % 35.19/23.00 tff(c_12465, 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))). % 35.19/23.00 tff(c_10681, 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))). % 35.19/23.00 tff(c_4506, 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))). % 35.19/23.00 tff(c_4702, 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))). % 35.19/23.00 tff(c_12282, 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))). % 35.19/23.00 tff(c_10279, 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))). % 35.19/23.00 tff(c_11385, 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))). % 35.19/23.00 tff(c_8050, 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))). % 35.19/23.00 tff(c_11319, 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))). % 35.19/23.00 tff(c_7615, 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))). % 35.19/23.00 tff(c_4561, 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))). % 35.19/23.00 tff(c_11588, 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))). % 35.19/23.00 tff(c_57733, plain, (![X_1085, Y_1086]: (ifeq(iext(uri_owl_oneOf, X_1085, Y_1086), true, iext(uri_owl_oneOf, X_1085, Y_1086), true)=true))). % 35.19/23.00 tff(c_7984, 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))). % 35.19/23.00 tff(c_57115, plain, (![X_1077, Y_1078]: (ifeq(iext(uri_rdf_rest, X_1077, Y_1078), true, iext(uri_rdf_rest, X_1077, Y_1078), true)=true))). % 35.19/23.00 tff(c_6225, 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))). % 35.19/23.00 tff(c_56968, plain, (![C_1075]: (ifeq(iext(uri_rdfs_subClassOf, C_1075, uri_rdfs_Literal), true, iext(uri_rdfs_subClassOf, C_1075, uri_rdfs_Resource), true)=true))). % 35.19/23.00 tff(c_56828, plain, (![C_1073]: (ifeq(iext(uri_rdfs_subClassOf, C_1073, uri_rdf_XMLLiteral), true, iext(uri_rdfs_subClassOf, C_1073, uri_rdfs_Resource), true)=true))). % 35.19/23.00 tff(c_10031, 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))). % 35.19/23.00 tff(c_6560, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_owl_oneOf, uri_owl_oneOf), true, true, true), true)=true))). % 35.19/23.00 tff(c_9239, 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))). % 35.19/23.00 tff(c_56214, plain, (![X_1064, Y_1065]: (ifeq(iext(uri_rdf__2, X_1064, Y_1065), true, iext(uri_rdfs_member, X_1064, Y_1065), true)=true))). % 35.19/23.00 tff(c_56044, plain, (![X_1060, Y_1061]: (ifeq(iext(uri_rdf_first, X_1060, Y_1061), true, iext(uri_rdf_first, X_1060, Y_1061), true)=true))). % 35.19/23.00 tff(c_4650, 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))). % 35.19/23.00 tff(c_55884, plain, (![X_1054, Y_1055]: (ifeq(iext(uri_rdf__3, X_1054, Y_1055), true, iext(uri_rdf__3, X_1054, Y_1055), true)=true))). % 35.19/23.00 tff(c_8639, 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))). % 35.19/23.00 tff(c_4509, 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))). % 35.19/23.00 tff(c_4890, 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))). % 35.19/23.00 tff(c_55337, plain, (![C_1047]: (ifeq(iext(uri_rdfs_subClassOf, C_1047, uri_rdf_Bag), true, iext(uri_rdfs_subClassOf, C_1047, uri_rdfs_Resource), true)=true))). % 35.19/23.00 tff(c_54810, plain, (![X_1043, Y_1044]: (ifeq(iext(uri_rdfs_subPropertyOf, X_1043, Y_1044), true, iext(uri_rdfs_subPropertyOf, X_1043, Y_1044), true)=true))). % 35.19/23.00 tff(c_8587, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_owl_unionOf, uri_owl_unionOf), true, true, true), true)=true))). % 35.19/23.00 tff(c_54543, plain, (![C_1040]: (ifeq(iext(uri_rdfs_subClassOf, C_1040, uri_rdf_Property), true, iext(uri_rdfs_subClassOf, C_1040, uri_rdfs_Resource), true)=true))). % 35.19/23.00 tff(c_54515, plain, (![X_1036, Y_1037]: (ifeq(iext(uri_rdf__1, X_1036, Y_1037), true, iext(uri_rdf__1, X_1036, Y_1037), true)=true))). % 35.19/23.00 tff(c_5052, plain, (![P_47, X_132]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, X_132, uri_rdfs_Resource), true, true, true), true)=true))). % 35.19/23.00 tff(c_16481, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_List), true, ifeq(iext(P_28, X_30, sK5_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l32), true, true, true), true)=true))). % 35.19/23.00 tff(c_11461, 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))). % 35.19/23.00 tff(c_9477, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_List), true, ifeq(iext(P_18, sK7_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l22, Y_21), true, true, true), true)=true))). % 35.19/23.00 tff(c_17636, 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))). % 35.19/23.00 tff(c_14264, 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))). % 35.19/23.00 tff(c_6864, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_List), true, ifeq(iext(P_28, X_30, sK2_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l42), true, true, true), true)=true))). % 35.19/23.00 tff(c_12117, 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))). % 35.19/23.00 tff(c_9480, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_List), true, ifeq(iext(P_28, X_30, sK7_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l22), true, true, true), true)=true))). % 35.19/23.00 tff(c_6312, 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))). % 35.19/23.00 tff(c_14267, 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))). % 35.19/23.00 tff(c_9316, 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))). % 35.19/23.00 tff(c_16478, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_List), true, ifeq(iext(P_18, sK5_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l32, Y_21), true, true, true), true)=true))). % 35.19/23.00 tff(c_10568, 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))). % 35.19/23.00 tff(c_7085, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_List), true, ifeq(iext(P_18, sK6_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l21, Y_21), true, true, true), true)=true))). % 35.19/23.00 tff(c_13618, 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))). % 35.19/23.00 tff(c_10358, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_List), true, ifeq(iext(P_18, sK9_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l12, Y_21), true, true, true), true)=true))). % 35.19/23.00 tff(c_12951, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_List), true, ifeq(iext(P_18, sK4_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l31, Y_21), true, true, true), true)=true))). % 35.19/23.00 tff(c_9313, 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))). % 35.19/23.01 tff(c_16902, 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))). % 35.19/23.01 tff(c_10361, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_List), true, ifeq(iext(P_28, X_30, sK9_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l12), true, true, true), true)=true))). % 35.19/23.01 tff(c_12114, 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))). % 35.19/23.01 tff(c_18058, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_List), true, ifeq(iext(P_18, sK8_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l11, Y_21), true, true, true), true)=true))). % 35.19/23.01 tff(c_6309, 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))). % 35.19/23.01 tff(c_15965, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_List), true, ifeq(iext(P_18, sK3_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l33, Y_21), true, true, true), true)=true))). % 35.19/23.01 tff(c_11464, 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))). % 35.19/23.01 tff(c_16899, 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))). % 35.19/23.01 tff(c_18061, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_List), true, ifeq(iext(P_28, X_30, sK8_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l11), true, true, true), true)=true))). % 35.19/23.01 tff(c_12954, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_List), true, ifeq(iext(P_28, X_30, sK4_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l31), true, true, true), true)=true))). % 35.19/23.01 tff(c_10565, 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))). % 35.19/23.01 tff(c_13621, 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))). % 35.19/23.01 tff(c_10758, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_List), true, ifeq(iext(P_28, X_30, sK1_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l41), true, true, true), true)=true))). % 35.19/23.01 tff(c_10755, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_List), true, ifeq(iext(P_18, sK1_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l41, Y_21), true, true, true), true)=true))). % 35.19/23.01 tff(c_7088, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_List), true, ifeq(iext(P_28, X_30, sK6_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l21), true, true, true), true)=true))). % 35.19/23.01 tff(c_17639, 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))). % 35.19/23.01 tff(c_6861, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_List), true, ifeq(iext(P_18, sK2_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l42, Y_21), true, true, true), true)=true))). % 35.19/23.01 tff(c_15968, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_List), true, ifeq(iext(P_28, X_30, sK3_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l33), true, true, true), true)=true))). % 35.19/23.01 tff(c_4381, 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))). % 35.19/23.01 tff(c_3851, 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))). % 35.19/23.01 tff(c_3991, 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))). % 35.19/23.01 tff(c_4421, 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))). % 35.19/23.01 tff(c_4172, 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))). % 35.19/23.01 tff(c_4460, 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))). % 35.19/23.01 tff(c_3946, 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))). % 35.19/23.01 tff(c_4037, 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))). % 35.19/23.01 tff(c_4378, 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))). % 35.19/23.01 tff(c_3895, 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))). % 35.19/23.01 tff(c_4457, 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))). % 35.19/23.01 tff(c_4300, 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))). % 35.19/23.01 tff(c_4217, 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))). % 35.19/23.01 tff(c_4339, 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))). % 35.19/23.01 tff(c_4214, 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))). % 35.19/23.01 tff(c_4132, 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))). % 35.19/23.01 tff(c_4040, 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))). % 35.19/23.01 tff(c_4175, 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))). % 35.19/23.01 tff(c_4093, 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))). % 35.19/23.01 tff(c_3854, 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))). % 35.19/23.01 tff(c_4264, 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))). % 35.19/23.01 tff(c_4303, 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))). % 35.19/23.01 tff(c_4090, 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))). % 35.19/23.01 tff(c_3943, 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))). % 35.19/23.01 tff(c_4418, 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))). % 35.19/23.01 tff(c_3892, 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))). % 35.19/23.01 tff(c_4342, 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))). % 35.19/23.01 tff(c_3988, 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))). % 35.19/23.01 tff(c_4135, 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))). % 35.19/23.01 tff(c_4261, 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))). % 35.19/23.01 tff(c_1775, plain, (![P_93, X_95, X_61]: (ifeq(iext(uri_rdfs_range, P_93, uri_rdfs_Resource), true, ifeq(iext(P_93, X_95, X_61), true, true, true), true)=true))). % 35.19/23.01 tff(c_2217, plain, (![P_97, X_61, Y_100]: (ifeq(iext(uri_rdfs_domain, P_97, uri_rdfs_Resource), true, ifeq(iext(P_97, X_61, Y_100), true, true, true), true)=true))). % 35.19/23.01 tff(c_2794, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdf_type), true, ifeq(iext(P_101, uri_rdf__2, uri_rdf_Property), true, true, true), true)=true))). % 35.19/23.01 tff(c_2653, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdf_type), true, ifeq(iext(P_101, uri_rdf_type, uri_rdf_Property), true, true, true), true)=true))). % 35.19/23.01 tff(c_3052, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdfs_domain), true, ifeq(iext(P_101, uri_rdf_first, uri_rdf_List), true, true, true), true)=true))). % 35.19/23.01 tff(c_2725, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdf_rest), true, ifeq(iext(P_101, sK9_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l12, uri_rdf_nil), true, true, true), true)=true))). % 35.19/23.01 tff(c_3016, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdfs_range), true, ifeq(iext(P_101, uri_rdfs_subPropertyOf, uri_rdf_Property), true, true, true), true)=true))). % 35.19/23.01 tff(c_43171, plain, (![C_889]: (ifeq(iext(uri_rdfs_subClassOf, C_889, uri_rdfs_Seq), true, iext(uri_rdfs_subClassOf, C_889, uri_rdfs_Container), true)=true))). % 35.19/23.01 tff(c_2836, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdfs_range), true, ifeq(iext(P_101, uri_rdfs_seeAlso, uri_rdfs_Resource), true, true, true), true)=true))). % 35.19/23.01 tff(c_3088, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdf_first), true, ifeq(iext(P_101, sK1_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l41, uri_ex_c1), true, true, true), true)=true))). % 35.19/23.01 tff(c_2683, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdf_type), true, ifeq(iext(P_101, uri_rdf_first, uri_rdf_Property), true, true, true), true)=true))). % 35.19/23.01 tff(c_3004, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdfs_range), true, ifeq(iext(P_101, uri_rdf_value, uri_rdfs_Resource), true, true, true), true)=true))). % 35.19/23.01 tff(c_2719, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdf_type), true, ifeq(iext(P_101, uri_rdf_Property, uri_rdfs_Class), true, true, true), true)=true))). % 35.19/23.01 tff(c_3100, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdfs_domain), true, ifeq(iext(P_101, uri_rdfs_domain, uri_rdf_Property), true, true, true), true)=true))). % 35.19/23.01 tff(c_3082, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdf_type), true, ifeq(iext(P_101, uri_rdf_rest, uri_rdf_Property), true, true, true), true)=true))). % 35.19/23.01 tff(c_3118, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdf_first), true, ifeq(iext(P_101, sK3_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l33, uri_ex_w3), true, true, true), true)=true))). % 35.19/23.01 tff(c_2671, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdfs_range), true, ifeq(iext(P_101, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true, true, true), true)=true))). % 35.19/23.01 tff(c_2986, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdfs_subClassOf), true, ifeq(iext(P_101, uri_rdfs_Datatype, uri_rdfs_Class), true, true, true), true)=true))). % 35.19/23.01 tff(c_3010, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdfs_range), true, ifeq(iext(P_101, uri_rdfs_subClassOf, uri_rdfs_Class), true, true, true), true)=true))). % 35.19/23.01 tff(c_2884, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdf_first), true, ifeq(iext(P_101, sK6_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l21, uri_ex_w2), true, true, true), true)=true))). % 35.19/23.01 tff(c_2782, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdf_type), true, ifeq(iext(P_101, uri_rdf_object, uri_rdf_Property), true, true, true), true)=true))). % 35.19/23.01 tff(c_2734, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdfs_subPropertyOf), true, ifeq(iext(P_101, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso), true, true, true), true)=true))). % 35.19/23.01 tff(c_2689, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdfs_domain), true, ifeq(iext(P_101, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true, true, true), true)=true))). % 35.19/23.01 tff(c_3034, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdfs_range), true, ifeq(iext(P_101, uri_rdf_first, uri_rdfs_Resource), true, true, true), true)=true))). % 35.19/23.01 tff(c_2770, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdf_rest), true, ifeq(iext(P_101, sK3_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l33, uri_rdf_nil), true, true, true), true)=true))). % 35.19/23.01 tff(c_2902, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdfs_range), true, ifeq(iext(P_101, uri_rdf_rest, uri_rdf_List), true, true, true), true)=true))). % 35.19/23.01 tff(c_2962, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdfs_range), true, ifeq(iext(P_101, uri_rdf_subject, uri_rdfs_Resource), true, true, true), true)=true))). % 35.19/23.01 tff(c_2695, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdfs_subClassOf), true, ifeq(iext(P_101, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property), true, true, true), true)=true))). % 35.19/23.01 tff(c_2758, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdfs_range), true, ifeq(iext(P_101, uri_rdfs_member, uri_rdfs_Resource), true, true, true), true)=true))). % 35.19/23.01 tff(c_2818, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdfs_domain), true, ifeq(iext(P_101, uri_rdfs_member, uri_rdfs_Resource), true, true, true), true)=true))). % 35.19/23.01 tff(c_3076, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdf_type), true, ifeq(iext(P_101, uri_rdf_XMLLiteral, uri_rdfs_Datatype), true, true, true), true)=true))). % 35.19/23.01 tff(c_2926, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdfs_domain), true, ifeq(iext(P_101, uri_rdfs_subClassOf, uri_rdfs_Class), true, true, true), true)=true))). % 35.19/23.01 tff(c_40177, plain, (![X_861, Y_862]: (ifeq(iext(uri_rdfs_isDefinedBy, X_861, Y_862), true, iext(uri_rdfs_seeAlso, X_861, Y_862), true)=true))). % 35.19/23.01 tff(c_2896, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_owl_oneOf), true, ifeq(iext(P_101, uri_ex_c2, sK6_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l21), true, true, true), true)=true))). % 35.19/23.01 tff(c_2908, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdfs_subClassOf), true, ifeq(iext(P_101, uri_rdf_Alt, uri_rdfs_Container), true, true, true), true)=true))). % 35.19/23.01 tff(c_39886, plain, (![C_857]: (ifeq(iext(uri_rdfs_subClassOf, C_857, uri_rdf_XMLLiteral), true, iext(uri_rdfs_subClassOf, C_857, uri_rdfs_Literal), true)=true))). % 35.19/23.01 tff(c_2752, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdf_first), true, ifeq(iext(P_101, sK2_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l42, uri_ex_c2), true, true, true), true)=true))). % 35.19/23.01 tff(c_2992, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdfs_domain), true, ifeq(iext(P_101, uri_rdf_predicate, uri_rdfs_Statement), true, true, true), true)=true))). % 35.19/23.01 tff(c_2998, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdf_type), true, ifeq(iext(P_101, uri_rdf__1, uri_rdf_Property), true, true, true), true)=true))). % 35.19/23.01 tff(c_2932, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdfs_domain), true, ifeq(iext(P_101, uri_rdf__2, uri_rdfs_Resource), true, true, true), true)=true))). % 35.19/23.01 tff(c_39346, plain, (![C_851]: (ifeq(iext(uri_rdfs_subClassOf, C_851, uri_rdfs_ContainerMembershipProperty), true, iext(uri_rdfs_subClassOf, C_851, uri_rdf_Property), true)=true))). % 35.19/23.01 tff(c_2890, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdfs_range), true, ifeq(iext(P_101, uri_rdfs_range, uri_rdfs_Class), true, true, true), true)=true))). % 35.19/23.01 tff(c_3070, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdf_type), true, ifeq(iext(P_101, uri_rdf__3, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 35.19/23.01 tff(c_3064, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdf_rest), true, ifeq(iext(P_101, sK8_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l11, sK9_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l12), true, true, true), true)=true))). % 35.19/23.01 tff(c_2740, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdfs_domain), true, ifeq(iext(P_101, uri_rdfs_range, uri_rdf_Property), true, true, true), true)=true))). % 35.19/23.02 tff(c_2950, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdfs_domain), true, ifeq(iext(P_101, uri_rdfs_label, uri_rdfs_Resource), true, true, true), true)=true))). % 35.19/23.02 tff(c_2848, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdf_type), true, ifeq(iext(P_101, uri_rdf__2, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 35.19/23.02 tff(c_2800, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdf_rest), true, ifeq(iext(P_101, sK7_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l22, uri_rdf_nil), true, true, true), true)=true))). % 35.19/23.02 tff(c_2968, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdfs_range), true, ifeq(iext(P_101, uri_rdfs_comment, uri_rdfs_Literal), true, true, true), true)=true))). % 35.19/23.02 tff(c_2842, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdfs_range), true, ifeq(iext(P_101, uri_rdf__1, uri_rdfs_Resource), true, true, true), true)=true))). % 35.19/23.02 tff(c_3112, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdf_rest), true, ifeq(iext(P_101, sK4_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l31, sK5_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l32), true, true, true), true)=true))). % 35.19/23.02 tff(c_2677, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdfs_domain), true, ifeq(iext(P_101, uri_rdf_object, uri_rdfs_Statement), true, true, true), true)=true))). % 35.19/23.02 tff(c_2707, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdf_type), true, ifeq(iext(P_101, uri_rdf_subject, uri_rdf_Property), true, true, true), true)=true))). % 35.19/23.02 tff(c_2812, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdf_type), true, ifeq(iext(P_101, uri_rdf_nil, uri_rdf_List), true, true, true), true)=true))). % 35.19/23.02 tff(c_2872, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdfs_range), true, ifeq(iext(P_101, uri_rdf_type, uri_rdfs_Class), true, true, true), true)=true))). % 35.19/23.02 tff(c_2980, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_owl_oneOf), true, ifeq(iext(P_101, uri_ex_c1, sK8_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l11), true, true, true), true)=true))). % 35.19/23.02 tff(c_3094, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_owl_oneOf), true, ifeq(iext(P_101, uri_ex_c3, sK4_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l31), true, true, true), true)=true))). % 35.19/23.02 tff(c_3028, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdf_rest), true, ifeq(iext(P_101, sK6_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l21, sK7_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l22), true, true, true), true)=true))). % 35.19/23.02 tff(c_2824, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdfs_subClassOf), true, ifeq(iext(P_101, uri_rdf_Bag, uri_rdfs_Container), true, true, true), true)=true))). % 35.19/23.02 tff(c_2764, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdfs_range), true, ifeq(iext(P_101, uri_rdfs_label, uri_rdfs_Literal), true, true, true), true)=true))). % 35.19/23.02 tff(c_2647, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdf_rest), true, ifeq(iext(P_101, sK1_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l41, sK2_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l42), true, true, true), true)=true))). % 35.19/23.02 tff(c_36861, plain, (![D_829]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_829), true, icext(D_829, uri_rdfs_Resource), true)=true))). % 35.19/23.02 tff(c_2746, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdfs_domain), true, ifeq(iext(P_101, uri_rdf_type, uri_rdfs_Resource), true, true, true), true)=true))). % 35.19/23.02 tff(c_36669, plain, (![D_826]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_826), true, icext(D_826, uri_rdfs_subClassOf), true)=true))). % 35.19/23.02 tff(c_36602, plain, (![D_824]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_824), true, icext(D_824, uri_owl_oneOf), true)=true))). % 35.19/23.02 tff(c_2665, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdf_first), true, ifeq(iext(P_101, sK4_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l31, uri_ex_w1), true, true, true), true)=true))). % 35.19/23.02 tff(c_36415, plain, (![D_821]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_821), true, icext(D_821, uri_rdfs_domain), true)=true))). % 35.19/23.02 tff(c_36349, plain, (![D_819]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_819), true, icext(D_819, uri_owl_unionOf), true)=true))). % 35.19/23.02 tff(c_36283, plain, (![D_817]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_817), true, icext(D_817, uri_rdfs_subPropertyOf), true)=true))). % 35.19/23.02 tff(c_3130, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdf_first), true, ifeq(iext(P_101, sK9_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l12, uri_ex_w2), true, true, true), true)=true))). % 35.19/23.02 tff(c_35961, plain, (![D_813]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_813), true, icext(D_813, uri_rdfs_Literal), true)=true))). % 35.19/23.02 tff(c_2806, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdfs_domain), true, ifeq(iext(P_101, uri_rdf__3, uri_rdfs_Resource), true, true, true), true)=true))). % 35.19/23.02 tff(c_35867, plain, (![D_811]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_811), true, icext(D_811, uri_rdfs_Class), true)=true))). % 35.19/23.02 tff(c_35801, plain, (![D_809]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_809), true, icext(D_809, uri_rdfs_ContainerMembershipProperty), true)=true))). % 35.19/23.02 tff(c_35615, plain, (![D_806]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_806), true, icext(D_806, uri_rdfs_Seq), true)=true))). % 35.19/23.02 tff(c_3058, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdfs_range), true, ifeq(iext(P_101, uri_rdfs_domain, uri_rdfs_Class), true, true, true), true)=true))). % 35.19/23.02 tff(c_35549, plain, (![D_804]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_804), true, icext(D_804, uri_rdfs_Datatype), true)=true))). % 35.19/23.02 tff(c_35483, plain, (![D_802]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_802), true, icext(D_802, uri_rdf_Alt), true)=true))). % 35.19/23.02 tff(c_35280, plain, (![D_799]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_799), true, icext(D_799, uri_rdf_XMLLiteral), true)=true))). % 35.19/23.02 tff(c_2974, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdfs_domain), true, ifeq(iext(P_101, uri_rdf_value, uri_rdfs_Resource), true, true, true), true)=true))). % 35.19/23.02 tff(c_35214, plain, (![D_797]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_797), true, icext(D_797, uri_rdfs_Container), true)=true))). % 35.19/23.02 tff(c_35147, plain, (![D_795]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_795), true, icext(D_795, uri_rdf_Bag), true)=true))). % 35.19/23.02 tff(c_35079, plain, (![D_793]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_793), true, icext(D_793, sK2_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l42), true)=true))). % 35.19/23.02 tff(c_35013, plain, (![D_791]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_791), true, icext(D_791, sK6_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l21), true)=true))). % 35.19/23.02 tff(c_34947, plain, (![D_789]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_789), true, icext(D_789, sK1_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l41), true)=true))). % 35.19/23.02 tff(c_2788, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdfs_domain), true, ifeq(iext(P_101, uri_rdfs_seeAlso, uri_rdfs_Resource), true, true, true), true)=true))). % 35.19/23.02 tff(c_34752, plain, (![D_786]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_786), true, icext(D_786, uri_rdfs_member), true)=true))). % 35.19/23.02 tff(c_34686, plain, (![D_784]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_784), true, icext(D_784, sK7_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l22), true)=true))). % 35.19/23.02 tff(c_34495, plain, (![D_781]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_781), true, icext(D_781, uri_rdfs_seeAlso), true)=true))). % 35.19/23.02 tff(c_2854, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdfs_domain), true, ifeq(iext(P_101, uri_rdf_rest, uri_rdf_List), true, true, true), true)=true))). % 35.19/23.02 tff(c_34429, plain, (![D_779]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_779), true, icext(D_779, uri_rdfs_label), true)=true))). % 35.19/23.02 tff(c_34363, plain, (![D_777]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_777), true, icext(D_777, sK5_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l32), true)=true))). % 35.19/23.02 tff(c_34296, plain, (![D_775]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_775), true, icext(D_775, uri_rdfs_range), true)=true))). % 35.19/23.02 tff(c_34230, plain, (![D_773]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_773), true, icext(D_773, uri_rdfs_comment), true)=true))). % 35.19/23.02 tff(c_34164, plain, (![D_771]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_771), true, icext(D_771, uri_rdf_List), true)=true))). % 35.19/23.02 tff(c_15056, 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))). % 35.19/23.02 tff(c_3022, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdfs_range), true, ifeq(iext(P_101, uri_rdf__3, uri_rdfs_Resource), true, true, true), true)=true))). % 35.19/23.02 tff(c_17944, 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))). % 35.19/23.02 tff(c_17216, 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))). % 35.19/23.02 tff(c_33878, plain, (![D_763]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_763), true, icext(D_763, sK3_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l33), true)=true))). % 35.19/23.02 tff(c_15008, 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))). % 35.19/23.02 tff(c_14942, 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))). % 35.19/23.02 tff(c_2776, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdf_first), true, ifeq(iext(P_101, sK5_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l32, uri_ex_w2), true, true, true), true)=true))). % 35.19/23.02 tff(c_14838, 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))). % 35.19/23.02 tff(c_33573, plain, (![D_754]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_754), true, icext(D_754, uri_rdfs_isDefinedBy), true)=true))). % 35.19/23.02 tff(c_14570, 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))). % 35.19/23.02 tff(c_14041, 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))). % 35.19/23.02 tff(c_14636, 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))). % 35.19/23.02 tff(c_3124, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdf_first), true, ifeq(iext(P_101, sK7_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l22, uri_ex_w3), true, true, true), true)=true))). % 35.19/23.02 tff(c_14039, 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))). % 35.19/23.02 tff(c_33251, plain, (![D_745]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_745), true, icext(D_745, uri_rdfs_Statement), true)=true))). % 35.19/23.02 tff(c_14634, 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))). % 35.19/23.02 tff(c_14210, 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))). % 35.19/23.02 tff(c_13565, 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))). % 35.19/23.02 tff(c_2701, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdfs_domain), true, ifeq(iext(P_101, uri_rdfs_comment, uri_rdfs_Resource), true, true, true), true)=true))). % 35.19/23.02 tff(c_13423, 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))). % 35.19/23.02 tff(c_13250, 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))). % 35.19/23.02 tff(c_13899, 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))). % 35.19/23.02 tff(c_32962, plain, (![D_736]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_736), true, icext(D_736, sK9_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l12), true)=true))). % 35.19/23.02 tff(c_13328, 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))). % 35.19/23.02 tff(c_13376, 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))). % 35.19/23.02 tff(c_13470, 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))). % 35.19/23.02 tff(c_2659, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdf_rest), true, ifeq(iext(P_101, sK2_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l42, uri_rdf_nil), true, true, true), true)=true))). % 35.19/23.02 tff(c_13947, 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))). % 35.19/23.02 tff(c_13518, 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))). % 35.19/23.02 tff(c_13852, 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))). % 35.19/23.02 tff(c_32682, plain, (![D_727]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_727), true, icext(D_727, uri_rdf_predicate), true)=true))). % 35.19/23.02 tff(c_14506, 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))). % 35.19/23.02 tff(c_13107, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, sK6_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l21, uri_rdf_List), true)=true))). % 35.19/23.02 tff(c_17708, 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))). % 35.19/23.02 tff(c_2878, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdf_type), true, ifeq(iext(P_101, uri_rdf_value, uri_rdf_Property), true, true, true), true)=true))). % 35.19/23.02 tff(c_13202, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, sK4_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l31, uri_rdf_List), true)=true))). % 35.19/23.02 tff(c_12858, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, sK9_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l12, uri_rdf_List), true)=true))). % 35.19/23.02 tff(c_12925, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, sK2_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l42, uri_rdf_List), true)=true))). % 35.19/23.02 tff(c_32406, plain, (![D_718]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_718), true, icext(D_718, sK4_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l31), true)=true))). % 35.19/23.02 tff(c_12685, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, sK7_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l22, uri_rdf_List), true)=true))). % 35.19/23.02 tff(c_16653, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, sK5_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l32, uri_rdf_List), true)=true))). % 35.19/23.02 tff(c_12636, 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))). % 35.19/23.02 tff(c_3106, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdfs_subClassOf), true, ifeq(iext(P_101, uri_rdfs_Seq, uri_rdfs_Container), true, true, true), true)=true))). % 35.19/23.02 tff(c_13155, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, sK1_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l41, uri_rdf_List), true)=true))). % 35.19/23.02 tff(c_16161, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, sK3_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l33, uri_rdf_List), true)=true))). % 35.19/23.02 tff(c_12740, 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))). % 35.19/23.02 tff(c_18124, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, sK8_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l11, uri_rdf_List), true)=true))). % 35.19/23.02 tff(c_17081, 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))). % 35.19/23.02 tff(c_10172, 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))). % 35.19/23.02 tff(c_7469, 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))). % 35.19/23.02 tff(c_7546, 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))). % 35.19/23.02 tff(c_2920, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdf_type), true, ifeq(iext(P_101, uri_rdf__1, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 35.19/23.02 tff(c_11117, 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))). % 35.19/23.02 tff(c_11409, 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))). % 35.19/23.02 tff(c_11050, 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))). % 35.19/23.02 tff(c_31866, plain, (![D_700]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_700), true, icext(D_700, sK8_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l11), true)=true))). % 35.19/23.02 tff(c_7642, 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))). % 35.19/23.02 tff(c_11884, 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))). % 35.19/23.02 tff(c_2938, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdfs_domain), true, ifeq(iext(P_101, uri_rdfs_subPropertyOf, uri_rdf_Property), true, true, true), true)=true))). % 35.19/23.02 tff(c_9392, 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))). % 35.19/23.02 tff(c_11612, 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))). % 35.19/23.02 tff(c_7056, 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))). % 35.19/23.02 tff(c_10056, 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))). % 35.19/23.02 tff(c_31475, plain, (![C_688]: (ifeq(iext(uri_rdfs_subClassOf, C_688, uri_rdf_Alt), true, iext(uri_rdfs_subClassOf, C_688, uri_rdfs_Container), true)=true))). % 35.19/23.02 tff(c_10309, 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))). % 35.19/23.03 tff(c_31316, plain, (![D_683]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, D_683), true, icext(D_683, uri_rdf_XMLLiteral), true)=true))). % 35.19/23.03 tff(c_11949, 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))). % 35.19/23.03 tff(c_8923, 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))). % 35.19/23.03 tff(c_6250, 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))). % 35.19/23.03 tff(c_2944, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdfs_range), true, ifeq(iext(P_101, uri_rdf__2, uri_rdfs_Resource), true, true, true), true)=true))). % 35.19/23.03 tff(c_9261, 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))). % 35.19/23.03 tff(c_10240, 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))). % 35.19/23.03 tff(c_5194, 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))). % 35.19/23.03 tff(c_31026, plain, (![D_674]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_674), true, icext(D_674, uri_rdf_type), true)=true))). % 35.19/23.03 tff(c_12492, 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))). % 35.19/23.03 tff(c_9851, 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))). % 35.19/23.03 tff(c_12307, 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))). % 35.19/23.03 tff(c_2866, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdf_first), true, ifeq(iext(P_101, sK8_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l11, uri_ex_w1), true, true, true), true)=true))). % 35.19/23.03 tff(c_30681, plain, (![D_665]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_665), true, icext(D_665, uri_rdf_first), true)=true))). % 35.19/23.03 tff(c_6388, 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))). % 35.19/23.03 tff(c_30611, plain, (![P_662]: (ifeq(iext(uri_rdfs_subPropertyOf, P_662, uri_rdfs_isDefinedBy), true, iext(uri_rdfs_subPropertyOf, P_662, uri_rdfs_seeAlso), true)=true))). % 35.19/23.03 tff(c_11680, 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))). % 35.19/23.03 tff(c_12309, 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))). % 35.19/23.03 tff(c_30479, plain, (![D_657]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_657), true, icext(D_657, uri_rdf_nil), true)=true))). % 35.19/23.03 tff(c_12490, 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))). % 35.19/23.03 tff(c_7708, 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))). % 35.19/23.03 tff(c_3040, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdf_rest), true, ifeq(iext(P_101, sK5_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l32, sK3_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l33), true, true, true), true)=true))). % 35.19/23.03 tff(c_11746, 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))). % 35.19/23.03 tff(c_30162, plain, (![D_648]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_648), true, icext(D_648, uri_rdf_object), true)=true))). % 35.19/23.03 tff(c_9918, 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))). % 35.19/23.03 tff(c_7057, 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))). % 35.19/23.03 tff(c_3046, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdfs_domain), true, ifeq(iext(P_101, uri_rdf_subject, uri_rdfs_Statement), true, true, true), true)=true))). % 35.19/23.03 tff(c_11343, 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))). % 35.19/23.03 tff(c_11249, 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))). % 35.19/23.03 tff(c_8664, 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))). % 35.19/23.03 tff(c_11800, 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))). % 35.19/23.03 tff(c_10706, 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))). % 35.19/23.03 tff(c_29801, plain, (![C_636]: (ifeq(iext(uri_rdfs_subClassOf, C_636, uri_rdfs_Datatype), true, iext(uri_rdfs_subClassOf, C_636, uri_rdfs_Class), true)=true))). % 35.19/23.03 tff(c_6678, 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))). % 35.19/23.03 tff(c_11947, 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))). % 35.19/23.03 tff(c_29670, plain, (![D_631]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_631), true, icext(D_631, uri_rdf_Property), true)=true))). % 35.19/23.03 tff(c_8854, 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))). % 35.19/23.03 tff(c_10508, 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))). % 35.19/23.03 tff(c_2860, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdfs_range), true, ifeq(iext(P_101, uri_rdf_predicate, uri_rdfs_Resource), true, true, true), true)=true))). % 35.19/23.03 tff(c_11048, 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))). % 35.19/23.03 tff(c_7299, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_owl_unionOf, uri_rdf_Property), true)=true))). % 35.19/23.03 tff(c_8077, 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))). % 35.19/23.03 tff(c_6583, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_owl_oneOf, uri_owl_oneOf), true)=true))). % 35.19/23.03 tff(c_2956, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdfs_subClassOf), true, ifeq(iext(P_101, uri_rdf_XMLLiteral, uri_rdfs_Literal), true, true, true), true)=true))). % 35.19/23.03 tff(c_9916, 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))). % 35.19/23.03 tff(c_10834, 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))). % 35.19/23.03 tff(c_8075, 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))). % 35.19/23.03 tff(c_29063, plain, (![D_613]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_613), true, icext(D_613, uri_rdf__2), true)=true))). % 35.19/23.03 tff(c_28957, plain, (![C_610]: (ifeq(iext(uri_rdfs_subClassOf, C_610, uri_rdf_Bag), true, iext(uri_rdfs_subClassOf, C_610, uri_rdfs_Container), true)=true))). % 35.19/23.03 tff(c_11184, 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))). % 35.19/23.03 tff(c_9009, 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))). % 35.19/23.03 tff(c_7240, 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))). % 35.19/23.03 tff(c_10238, 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))). % 35.19/23.03 tff(c_7467, 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))). % 35.19/23.03 tff(c_2914, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdfs_domain), true, ifeq(iext(P_101, uri_rdf__1, uri_rdfs_Resource), true, true, true), true)=true))). % 35.19/23.03 tff(c_5496, 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))). % 35.19/23.03 tff(c_10058, 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))). % 35.19/23.03 tff(c_8420, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_owl_oneOf, uri_rdf_Property), true)=true))). % 35.19/23.03 tff(c_28531, plain, (![D_596]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_596), true, icext(D_596, uri_rdf__3), true)=true))). % 35.19/23.03 tff(c_8011, 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))). % 35.19/23.03 tff(c_8610, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_owl_unionOf, uri_owl_unionOf), true)=true))). % 35.19/23.03 tff(c_6679, 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))). % 35.19/23.03 tff(c_2713, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_owl_unionOf), true, ifeq(iext(P_101, uri_ex_c4, sK1_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l41), true, true, true), true)=true))). % 35.19/23.03 tff(c_10984, 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))). % 35.19/23.03 tff(c_28198, plain, (![D_587]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_587), true, icext(D_587, uri_rdf__1), true)=true))). % 35.19/23.03 tff(c_5297, 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))). % 35.19/23.03 tff(c_9394, 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))). % 35.19/23.03 tff(c_7706, 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))). % 35.19/23.03 tff(c_2830, plain, (![P_101]: (ifeq(iext(uri_rdfs_subPropertyOf, P_101, uri_rdf_type), true, ifeq(iext(P_101, uri_rdf__3, uri_rdf_Property), true, true, true), true)=true))). % 35.19/23.03 tff(c_5072, plain, (![Q_48, X_132]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, X_132, uri_rdfs_Resource), true)=true))). % 35.19/23.03 tff(c_3213, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_first, Q_102), true, iext(Q_102, sK9_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l12, uri_ex_w2), true)=true))). % 35.19/23.03 tff(c_3177, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_102), true, iext(Q_102, uri_rdf__1, uri_rdfs_Resource), true)=true))). % 35.19/23.03 tff(c_3179, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_102), true, iext(Q_102, uri_rdfs_subClassOf, uri_rdfs_Class), true)=true))). % 35.19/23.03 tff(c_3207, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_owl_oneOf, Q_102), true, iext(Q_102, uri_ex_c3, sK4_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l31), true)=true))). % 35.19/23.03 tff(c_3138, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_102), true, iext(Q_102, uri_rdf_object, uri_rdfs_Statement), true)=true))). % 35.19/23.03 tff(c_3196, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_rest, Q_102), true, iext(Q_102, sK6_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l21, sK7_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l22), true)=true))). % 35.19/23.03 tff(c_3205, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_102), true, iext(Q_102, uri_rdf_rest, uri_rdf_Property), true)=true))). % 35.19/23.03 tff(c_3203, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_102), true, iext(Q_102, uri_rdf__3, uri_rdfs_ContainerMembershipProperty), true)=true))). % 35.19/23.03 tff(c_3157, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_102), true, iext(Q_102, uri_rdf__2, uri_rdf_Property), true)=true))). % 35.19/23.03 tff(c_3141, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_102), true, iext(Q_102, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property), true)=true))). % 35.19/23.03 tff(c_3156, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_102), true, iext(Q_102, uri_rdfs_seeAlso, uri_rdfs_Resource), true)=true))). % 35.19/23.03 tff(c_3191, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_102), true, iext(Q_102, uri_rdf__1, uri_rdf_Property), true)=true))). % 35.19/23.03 tff(c_3137, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_102), true, iext(Q_102, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true)=true))). % 35.19/23.03 tff(c_3166, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_102), true, iext(Q_102, uri_rdf__2, uri_rdfs_ContainerMembershipProperty), true)=true))). % 35.19/23.03 tff(c_3181, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_102), true, iext(Q_102, uri_rdfs_subPropertyOf, uri_rdf_Property), true)=true))). % 35.19/23.03 tff(c_3180, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_102), true, iext(Q_102, uri_rdf__2, uri_rdfs_Resource), true)=true))). % 35.19/23.03 tff(c_3165, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_102), true, iext(Q_102, uri_rdf__1, uri_rdfs_Resource), true)=true))). % 35.19/23.03 tff(c_3160, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_102), true, iext(Q_102, uri_rdf_nil, uri_rdf_List), true)=true))). % 35.19/23.03 tff(c_3189, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_102), true, iext(Q_102, uri_rdfs_Datatype, uri_rdfs_Class), true)=true))). % 35.19/23.03 tff(c_3164, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_102), true, iext(Q_102, uri_rdfs_seeAlso, uri_rdfs_Resource), true)=true))). % 35.19/23.03 tff(c_3186, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_102), true, iext(Q_102, uri_rdfs_comment, uri_rdfs_Literal), true)=true))). % 35.19/23.03 tff(c_3149, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_102), true, iext(Q_102, uri_rdf_type, uri_rdfs_Resource), true)=true))). % 35.19/23.03 tff(c_3150, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_first, Q_102), true, iext(Q_102, sK2_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l42, uri_ex_c2), true)=true))). % 35.19/23.03 tff(c_3197, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_102), true, iext(Q_102, uri_rdf_first, uri_rdfs_Resource), true)=true))). % 35.19/23.03 tff(c_3390, plain, (![E_109]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_109), true, iext(uri_rdfs_subClassOf, uri_rdfs_Seq, E_109), true)=true))). % 35.19/23.03 tff(c_3142, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_102), true, iext(Q_102, uri_rdfs_comment, uri_rdfs_Resource), true)=true))). % 35.19/23.03 tff(c_3163, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_102), true, iext(Q_102, uri_rdf__3, uri_rdf_Property), true)=true))). % 35.19/23.03 tff(c_3173, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_102), true, iext(Q_102, uri_rdfs_range, uri_rdfs_Class), true)=true))). % 35.19/23.03 tff(c_3175, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_102), true, iext(Q_102, uri_rdf_rest, uri_rdf_List), true)=true))). % 35.19/23.03 tff(c_3136, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_first, Q_102), true, iext(Q_102, sK4_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l31, uri_ex_w1), true)=true))). % 35.19/23.03 tff(c_3199, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_102), true, iext(Q_102, uri_rdf_subject, uri_rdfs_Statement), true)=true))). % 35.19/23.03 tff(c_3192, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_102), true, iext(Q_102, uri_rdf_value, uri_rdfs_Resource), true)=true))). % 35.19/23.03 tff(c_3133, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_rest, Q_102), true, iext(Q_102, sK1_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l41, sK2_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l42), true)=true))). % 35.19/23.03 tff(c_3187, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_102), true, iext(Q_102, uri_rdf_value, uri_rdfs_Resource), true)=true))). % 35.19/23.03 tff(c_3385, plain, (![E_109]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, E_109), true, iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, E_109), true)=true))). % 35.19/23.03 tff(c_3155, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_102), true, iext(Q_102, uri_rdf_object, uri_rdf_Property), true)=true))). % 35.19/23.03 tff(c_3204, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_102), true, iext(Q_102, uri_rdf_XMLLiteral, uri_rdfs_Datatype), true)=true))). % 35.19/23.03 tff(c_3178, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_102), true, iext(Q_102, uri_rdf__1, uri_rdfs_ContainerMembershipProperty), true)=true))). % 35.19/23.03 tff(c_3184, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_102), true, iext(Q_102, uri_rdf_XMLLiteral, uri_rdfs_Literal), true)=true))). % 35.19/23.03 tff(c_3188, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_owl_oneOf, Q_102), true, iext(Q_102, uri_ex_c1, sK8_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l11), true)=true))). % 35.19/23.03 tff(c_3176, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_102), true, iext(Q_102, uri_rdf_Alt, uri_rdfs_Container), true)=true))). % 35.19/23.03 tff(c_3211, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_first, Q_102), true, iext(Q_102, sK3_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l33, uri_ex_w3), true)=true))). % 35.19/23.03 tff(c_3185, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_102), true, iext(Q_102, uri_rdf_subject, uri_rdfs_Resource), true)=true))). % 35.19/23.03 tff(c_3206, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_first, Q_102), true, iext(Q_102, sK1_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l41, uri_ex_c1), true)=true))). % 35.19/23.03 tff(c_3202, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_rest, Q_102), true, iext(Q_102, sK8_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l11, sK9_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l12), true)=true))). % 35.19/23.03 tff(c_3135, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_rest, Q_102), true, iext(Q_102, sK2_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l42, uri_rdf_nil), true)=true))). % 35.19/23.03 tff(c_3152, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_102), true, iext(Q_102, uri_rdfs_label, uri_rdfs_Literal), true)=true))). % 35.19/23.03 tff(c_3210, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_rest, Q_102), true, iext(Q_102, sK4_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l31, sK5_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l32), true)=true))). % 35.19/23.03 tff(c_3167, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_102), true, iext(Q_102, uri_rdf_rest, uri_rdf_List), true)=true))). % 35.19/23.03 tff(c_3144, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_owl_unionOf, Q_102), true, iext(Q_102, uri_ex_c4, sK1_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l41), true)=true))). % 35.19/23.03 tff(c_3162, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_102), true, iext(Q_102, uri_rdf_Bag, uri_rdfs_Container), true)=true))). % 35.19/23.03 tff(c_3311, plain, (![R_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_seeAlso, R_106), true, iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, R_106), true)=true))). % 35.19/23.03 tff(c_3159, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_102), true, iext(Q_102, uri_rdf__3, uri_rdfs_Resource), true)=true))). % 35.19/23.03 tff(c_3389, plain, (![E_109]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, E_109), true, iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, E_109), true)=true))). % 35.19/23.03 tff(c_3146, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_rest, Q_102), true, iext(Q_102, sK9_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l12, uri_rdf_nil), true)=true))). % 35.19/23.03 tff(c_26777, plain, (![D_523]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_523), true, icext(D_523, uri_rdf_subject), true)=true))). % 35.19/23.03 tff(c_3193, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_102), true, iext(Q_102, uri_rdfs_subClassOf, uri_rdfs_Class), true)=true))). % 35.19/23.03 tff(c_3154, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_first, Q_102), true, iext(Q_102, sK5_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l32, uri_ex_w2), true)=true))). % 35.19/23.03 tff(c_3139, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_102), true, iext(Q_102, uri_rdf_first, uri_rdf_Property), true)=true))). % 35.19/23.03 tff(c_3168, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_102), true, iext(Q_102, uri_rdf_predicate, uri_rdfs_Resource), true)=true))). % 35.19/23.03 tff(c_3195, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_102), true, iext(Q_102, uri_rdf__3, uri_rdfs_Resource), true)=true))). % 35.19/23.03 tff(c_3194, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_102), true, iext(Q_102, uri_rdfs_subPropertyOf, uri_rdf_Property), true)=true))). % 35.19/23.03 tff(c_3388, plain, (![E_109]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Literal, E_109), true, iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, E_109), true)=true))). % 35.19/23.03 tff(c_26560, plain, (![D_514]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_514), true, icext(D_514, uri_rdf__2), true)=true))). % 35.19/23.04 tff(c_3172, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_first, Q_102), true, iext(Q_102, sK6_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l21, uri_ex_w2), true)=true))). % 35.19/23.04 tff(c_3134, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_102), true, iext(Q_102, uri_rdf_type, uri_rdf_Property), true)=true))). % 35.19/23.04 tff(c_3151, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_102), true, iext(Q_102, uri_rdfs_member, uri_rdfs_Resource), true)=true))). % 35.19/23.04 tff(c_17945, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_predicate), true)=true))). % 35.19/23.04 tff(c_17217, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_label), true)=true))). % 35.19/23.04 tff(c_15010, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_comment), true)=true))). % 35.19/23.04 tff(c_15009, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_comment), true)=true))). % 35.19/23.04 tff(c_17946, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_predicate), true)=true))). % 35.19/23.04 tff(c_17218, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_label), true)=true))). % 35.19/23.04 tff(c_14839, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Resource), true)=true))). % 35.19/23.04 tff(c_3158, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_rest, Q_102), true, iext(Q_102, sK7_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l22, uri_rdf_nil), true)=true))). % 35.19/23.04 tff(c_14943, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_member), true)=true))). % 35.19/23.04 tff(c_26210, plain, (![D_500]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_500), true, icext(D_500, uri_rdf_rest), true)=true))). % 35.19/23.04 tff(c_14572, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_List), true)=true))). % 35.19/23.04 tff(c_3148, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_102), true, iext(Q_102, uri_rdfs_range, uri_rdf_Property), true)=true))). % 35.19/23.04 tff(c_14571, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdf_List), true)=true))). % 35.19/23.04 tff(c_14212, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Statement), true)=true))). % 35.19/23.04 tff(c_14042, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Statement), true)=true))). % 35.19/23.04 tff(c_3208, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_102), true, iext(Q_102, uri_rdfs_domain, uri_rdf_Property), true)=true))). % 35.19/23.04 tff(c_3145, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_102), true, iext(Q_102, uri_rdf_Property, uri_rdfs_Class), true)=true))). % 35.19/23.04 tff(c_3174, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_owl_oneOf, Q_102), true, iext(Q_102, uri_ex_c2, sK6_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l21), true)=true))). % 35.19/23.04 tff(c_3153, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_rest, Q_102), true, iext(Q_102, sK3_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l33, uri_rdf_nil), true)=true))). % 35.19/23.04 tff(c_3147, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_102), true, iext(Q_102, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso), true)=true))). % 35.19/23.04 tff(c_25889, plain, (![D_488]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_488), true, icext(D_488, uri_rdf_value), true)=true))). % 35.19/23.04 tff(c_3143, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_102), true, iext(Q_102, uri_rdf_subject, uri_rdf_Property), true)=true))). % 35.19/23.04 tff(c_25786, plain, (![D_485]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_485), true, icext(D_485, uri_rdf__1), true)=true))). % 35.19/23.04 tff(c_11614, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_subject), true)=true))). % 35.19/23.04 tff(c_3182, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_102), true, iext(Q_102, uri_rdf__2, uri_rdfs_Resource), true)=true))). % 35.19/23.04 tff(c_5299, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_range), true)=true))). % 35.19/23.04 tff(c_9262, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_object), true)=true))). % 35.19/23.04 tff(c_11251, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_domain), true)=true))). % 35.19/23.04 tff(c_25578, plain, (![D_478]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_478), true, icext(D_478, uri_rdf__3), true)=true))). % 35.19/23.04 tff(c_10510, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_XMLLiteral), true)=true))). % 35.19/23.04 tff(c_8925, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_first), true)=true))). % 35.19/23.04 tff(c_3161, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_102), true, iext(Q_102, uri_rdfs_member, uri_rdfs_Resource), true)=true))). % 35.19/23.04 tff(c_25035, plain, (![D_471, X_472]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, D_471), true, icext(D_471, X_472), true)=true))). % 35.19/23.04 tff(c_8612, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_owl_unionOf), true)=true))). % 35.19/23.04 tff(c_10835, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_value), true)=true))). % 35.19/23.04 tff(c_3212, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_first, Q_102), true, iext(Q_102, sK7_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l22, uri_ex_w3), true)=true))). % 35.19/23.04 tff(c_10241, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__1), true)=true))). % 35.19/23.04 tff(c_24744, plain, (![C_90, X_61]: (ifeq(icext(C_90, X_61), true, true, true)=true))). % 35.19/23.04 tff(c_6585, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_owl_oneOf), true)=true))). % 35.19/23.04 tff(c_3387, plain, (![E_109]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_109), true, iext(uri_rdfs_subClassOf, uri_rdf_Alt, E_109), true)=true))). % 35.19/23.04 tff(c_11118, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__3), true)=true))). % 35.19/23.04 tff(c_24264, plain, (![X_458, Y_459]: (ifeq(iext(uri_rdfs_domain, X_458, Y_459), true, icext(uri_rdf_Property, X_458), true)=true))). % 35.19/23.04 tff(c_10174, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_subPropertyOf), true)=true))). % 35.19/23.04 tff(c_3201, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_102), true, iext(Q_102, uri_rdfs_domain, uri_rdfs_Class), true)=true))). % 35.19/23.04 tff(c_11250, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_domain), true)=true))). % 35.19/23.04 tff(c_23999, plain, (![X_451, Y_452]: (ifeq(iext(uri_rdf_first, X_451, Y_452), true, icext(uri_rdf_List, X_451), true)=true))). % 35.19/23.04 tff(c_8611, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_owl_unionOf), true)=true))). % 35.19/23.04 tff(c_7709, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdf_Property), true)=true))). % 35.19/23.04 tff(c_3200, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_102), true, iext(Q_102, uri_rdf_first, uri_rdf_List), true)=true))). % 35.19/23.04 tff(c_8856, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_Bag), true)=true))). % 35.19/23.04 tff(c_23710, plain, (![X_443, Y_444]: (ifeq(iext(uri_rdf_rest, X_443, Y_444), true, icext(uri_rdf_List, Y_444), true)=true))). % 35.19/23.04 tff(c_11186, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_type), true)=true))). % 35.19/23.04 tff(c_5196, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Seq), true)=true))). % 35.19/23.04 tff(c_7547, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_subClassOf), true)=true))). % 35.19/23.04 tff(c_3209, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_102), true, iext(Q_102, uri_rdfs_Seq, uri_rdfs_Container), true)=true))). % 35.19/23.04 tff(c_7548, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_subClassOf), true)=true))). % 35.19/23.04 tff(c_23181, plain, (![X_434, Y_435]: (ifeq(iext(uri_rdfs_subPropertyOf, X_434, Y_435), true, icext(uri_rdf_Property, Y_435), true)=true))). % 35.19/23.04 tff(c_10173, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_subPropertyOf), true)=true))). % 35.19/23.04 tff(c_3386, plain, (![E_109]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_109), true, iext(uri_rdfs_subClassOf, uri_rdf_Bag, E_109), true)=true))). % 35.19/23.04 tff(c_7643, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Container), true)=true))). % 35.19/23.04 tff(c_23064, plain, (![X_427, Y_428]: (ifeq(iext(uri_rdfs_comment, X_427, Y_428), true, icext(uri_rdfs_Literal, Y_428), true)=true))). % 35.19/23.04 tff(c_8924, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_first), true)=true))). % 35.19/23.04 tff(c_11119, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__3), true)=true))). % 35.19/23.04 tff(c_3198, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_rest, Q_102), true, iext(Q_102, sK5_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l32, sK3_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l33), true)=true))). % 35.19/23.04 tff(c_11410, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_seeAlso), true)=true))). % 35.19/23.04 tff(c_22623, plain, (![X_419, Y_420]: (ifeq(iext(uri_rdfs_range, X_419, Y_420), true, icext(uri_rdf_Property, X_419), true)=true))). % 35.19/23.04 tff(c_10836, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_value), true)=true))). % 35.19/23.04 tff(c_7242, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_Alt), true)=true))). % 35.19/23.04 tff(c_3171, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_102), true, iext(Q_102, uri_rdf_value, uri_rdf_Property), true)=true))). % 35.19/23.04 tff(c_22522, plain, (![X_412, Y_413]: (ifeq(iext(uri_rdf_subject, X_412, Y_413), true, icext(uri_rdfs_Statement, X_412), true)=true))). % 35.19/23.04 tff(c_11886, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_rest), true)=true))). % 35.19/23.04 tff(c_3169, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_first, Q_102), true, iext(Q_102, sK8_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l11, uri_ex_w1), true)=true))). % 35.19/23.04 tff(c_11885, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_rest), true)=true))). % 35.19/23.04 tff(c_9395, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__2), true)=true))). % 35.19/23.04 tff(c_22393, plain, (![X_404, Y_405]: (ifeq(iext(uri_rdfs_label, X_404, Y_405), true, icext(uri_rdfs_Literal, Y_405), true)=true))). % 35.19/23.04 tff(c_3183, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_102), true, iext(Q_102, uri_rdfs_label, uri_rdfs_Resource), true)=true))). % 35.19/23.04 tff(c_11345, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__2), true)=true))). % 35.19/23.04 tff(c_8078, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Literal), true)=true))). % 35.19/23.04 tff(c_9853, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__1), true)=true))). % 35.19/23.04 tff(c_21747, plain, (![X_396, Y_397]: (ifeq(iext(uri_rdf_type, X_396, Y_397), true, icext(uri_rdfs_Class, Y_397), true)=true))). % 35.19/23.04 tff(c_10242, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_member), true)=true))). % 35.19/23.04 tff(c_11185, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_type), true)=true))). % 35.19/23.04 tff(c_11748, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_isDefinedBy), true)=true))). % 35.19/23.04 tff(c_3170, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_102), true, iext(Q_102, uri_rdf_type, uri_rdfs_Class), true)=true))). % 35.19/23.04 tff(c_11682, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Datatype), true)=true))). % 35.19/23.04 tff(c_8012, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Class), true)=true))). % 35.19/23.04 tff(c_21270, plain, (![X_386, Y_387]: (ifeq(iext(uri_rdfs_range, X_386, Y_387), true, icext(uri_rdfs_Class, Y_387), true)=true))). % 35.19/23.04 tff(c_6252, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_ContainerMembershipProperty), true)=true))). % 35.19/23.04 tff(c_11613, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_subject), true)=true))). % 35.19/23.04 tff(c_3190, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_102), true, iext(Q_102, uri_rdf_predicate, uri_rdfs_Statement), true)=true))). % 35.19/23.04 tff(c_9263, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_object), true)=true))). % 35.19/23.04 tff(c_20993, plain, (![X_378, Y_379]: (ifeq(iext(uri_rdf_rest, X_378, Y_379), true, icext(uri_rdf_List, X_378), true)=true))). % 35.19/23.04 tff(c_12311, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Resource), true)=true))). % 35.19/23.04 tff(c_6584, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_owl_oneOf), true)=true))). % 35.19/23.04 tff(c_3140, plain, (![Q_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_102), true, iext(Q_102, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true)=true))). % 35.19/23.04 tff(c_5298, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_range), true)=true))). % 35.19/23.04 tff(c_5073, plain, (![C_19, X_132]: (ifeq(iext(uri_rdfs_domain, uri_rdf_type, C_19), true, icext(C_19, X_132), true)=true))). % 35.19/23.04 tff(c_5074, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_29), true, icext(C_29, uri_rdfs_Resource), true)=true))). % 35.19/23.04 tff(c_20231, plain, (![X_367, Y_368]: (ifeq(iext(uri_rdfs_subPropertyOf, X_367, Y_368), true, icext(uri_rdf_Property, X_367), true)=true))). % 35.19/23.04 tff(c_19589, plain, (![X_358, Y_359]: (ifeq(iext(uri_rdfs_subClassOf, X_358, Y_359), true, icext(uri_rdfs_Class, X_358), true)=true))). % 35.19/23.04 tff(c_2537, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_98), true, icext(C_98, uri_rdfs_range), true)=true))). % 35.19/23.04 tff(c_2589, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_98), true, icext(C_98, uri_rdf_value), true)=true))). % 35.19/23.04 tff(c_2581, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_98), true, icext(C_98, uri_rdf_subject), true)=true))). % 35.19/23.04 tff(c_2582, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_98), true, icext(C_98, uri_rdfs_comment), true)=true))). % 35.19/23.04 tff(c_2156, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_94), true, icext(C_94, uri_rdfs_Datatype), true)=true))). % 35.19/23.04 tff(c_2569, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_98), true, icext(C_98, uri_rdf_Alt), true)=true))). % 35.19/23.04 tff(c_2104, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_94), true, icext(C_94, uri_rdf_List), true)=true))). % 35.19/23.04 tff(c_2606, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_98), true, icext(C_98, uri_rdfs_Seq), true)=true))). % 35.19/23.04 tff(c_2096, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_94), true, icext(C_94, uri_rdfs_Literal), true)=true))). % 35.19/23.04 tff(c_2138, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_94), true, icext(C_94, uri_rdfs_Class), true)=true))). % 35.19/23.04 tff(c_2577, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_98), true, icext(C_98, uri_rdf__2), true)=true))). % 35.19/23.04 tff(c_2558, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_98), true, icext(C_98, uri_rdf__1), true)=true))). % 35.19/23.04 tff(c_2561, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_98), true, icext(C_98, uri_rdf_predicate), true)=true))). % 35.19/23.04 tff(c_2525, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_98), true, icext(C_98, uri_rdf_object), true)=true))). % 35.19/23.04 tff(c_18598, plain, (![X_334, Y_335]: (ifeq(iext(uri_rdfs_subClassOf, X_334, Y_335), true, icext(uri_rdfs_Class, Y_335), true)=true))). % 35.19/23.04 tff(c_2090, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_94), true, icext(C_94, uri_rdfs_seeAlso), true)=true))). % 35.19/23.04 tff(c_2593, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdf_rest, C_98), true, icext(C_98, sK6_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l21), true)=true))). % 35.19/23.04 tff(c_2132, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_94), true, icext(C_94, uri_rdfs_Literal), true)=true))). % 35.19/23.04 tff(c_2584, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_98), true, icext(C_98, uri_rdf_value), true)=true))). % 35.19/23.04 tff(c_2539, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_98), true, icext(C_98, uri_rdf_type), true)=true))). % 35.19/23.04 tff(c_2599, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdf_rest, C_98), true, icext(C_98, sK8_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l11), true)=true))). % 35.19/23.04 tff(c_2536, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_98), true, icext(C_98, uri_rdfs_isDefinedBy), true)=true))). % 35.19/23.04 tff(c_2595, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdf_rest, C_98), true, icext(C_98, sK5_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l32), true)=true))). % 35.19/23.04 tff(c_2551, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_98), true, icext(C_98, uri_rdf__3), true)=true))). % 35.19/23.04 tff(c_2075, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_rdf_rest, C_94), true, icext(C_94, sK2_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l42), true)=true))). % 35.19/23.04 tff(c_2573, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_98), true, icext(C_98, uri_rdfs_subClassOf), true)=true))). % 35.19/23.04 tff(c_2541, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_98), true, icext(C_98, uri_rdfs_member), true)=true))). % 35.19/23.04 tff(c_2591, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_98), true, icext(C_98, uri_rdfs_subPropertyOf), true)=true))). % 35.19/23.04 tff(c_2604, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_owl_oneOf, C_98), true, icext(C_98, uri_ex_c3), true)=true))). % 35.19/23.04 tff(c_18088, plain, (iext(uri_rdf_type, sK8_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l11, uri_rdf_List)=true)). % 35.19/23.04 tff(c_18032, plain, (icext(uri_rdf_List, sK8_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l11)=true)). % 35.19/23.04 tff(c_2563, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_98), true, icext(C_98, uri_rdf_type), true)=true))). % 35.19/23.04 tff(c_2562, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdf_first, C_98), true, icext(C_98, sK8_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l11), true)=true))). % 35.19/23.04 tff(c_2592, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_98), true, icext(C_98, uri_rdf__3), true)=true))). % 35.19/23.04 tff(c_17891, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_predicate, uri_rdf_predicate)=true)). % 35.19/23.04 tff(c_2159, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_owl_oneOf, C_94), true, icext(C_94, sK4_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l31), true)=true))). % 35.19/23.04 tff(c_17719, plain, (ip(uri_rdf_predicate)=true)). % 35.19/23.04 tff(c_17666, plain, (iext(uri_rdf_type, uri_rdf_predicate, uri_rdf_Property)=true)). % 35.19/23.04 tff(c_17610, plain, (icext(uri_rdf_Property, uri_rdf_predicate)=true)). % 35.19/23.04 tff(c_2605, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_98), true, icext(C_98, uri_rdfs_domain), true)=true))). % 35.19/23.04 tff(c_2587, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_98), true, icext(C_98, uri_rdf_predicate), true)=true))). % 35.19/23.04 tff(c_2542, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_98), true, icext(C_98, uri_rdfs_label), true)=true))). % 35.19/23.04 tff(c_2586, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_98), true, icext(C_98, uri_rdfs_Datatype), true)=true))). % 35.19/23.04 tff(c_2597, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_98), true, icext(C_98, uri_rdf_first), true)=true))). % 35.19/23.04 tff(c_17283, plain, (![X_303, Y_304]: (ifeq(iext(uri_rdf_predicate, X_303, Y_304), true, icext(uri_rdfs_Statement, X_303), true)=true))). % 35.19/23.04 tff(c_2122, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_94), true, icext(C_94, uri_rdf_List), true)=true))). % 35.19/23.04 tff(c_2596, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_98), true, icext(C_98, uri_rdf_subject), true)=true))). % 35.19/23.04 tff(c_2093, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_rdf_first, C_94), true, icext(C_94, uri_ex_c2), true)=true))). % 35.19/23.04 tff(c_2119, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_rdf_first, C_94), true, icext(C_94, uri_ex_w2), true)=true))). % 35.19/23.04 tff(c_2590, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_98), true, icext(C_98, uri_rdfs_subClassOf), true)=true))). % 35.19/23.04 tff(c_2544, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdf_first, C_98), true, icext(C_98, sK5_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l32), true)=true))). % 35.19/23.04 tff(c_17163, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_label, uri_rdfs_label)=true)). % 35.19/23.04 tff(c_17121, plain, (ip(uri_rdfs_label)=true)). % 35.19/23.04 tff(c_2528, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_98), true, icext(C_98, uri_rdfs_isDefinedBy), true)=true))). % 35.19/23.04 tff(c_17039, plain, (iext(uri_rdf_type, uri_rdfs_label, uri_rdf_Property)=true)). % 35.19/23.04 tff(c_16873, plain, (icext(uri_rdf_Property, uri_rdfs_label)=true)). % 35.19/23.04 tff(c_2579, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_98), true, icext(C_98, uri_rdfs_label), true)=true))). % 35.19/23.04 tff(c_2088, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_94), true, icext(C_94, uri_rdfs_Class), true)=true))). % 35.19/23.04 tff(c_2555, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_98), true, icext(C_98, uri_rdf_Bag), true)=true))). % 35.19/23.04 tff(c_2087, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_owl_unionOf, C_94), true, icext(C_94, sK1_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l41), true)=true))). % 35.19/23.04 tff(c_2520, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdf_rest, C_98), true, icext(C_98, sK1_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l41), true)=true))). % 35.19/23.04 tff(c_2549, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdf_rest, C_98), true, icext(C_98, sK7_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l22), true)=true))). % 35.19/23.04 tff(c_2150, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_rdf_rest, C_94), true, icext(C_94, sK3_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l33), true)=true))). % 35.19/23.05 tff(c_2163, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_rdf_first, C_94), true, icext(C_94, uri_ex_w3), true)=true))). % 35.19/23.05 tff(c_2585, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_owl_oneOf, C_98), true, icext(C_98, uri_ex_c1), true)=true))). % 35.19/23.05 tff(c_16617, plain, (iext(uri_rdf_type, sK5_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l32, uri_rdf_List)=true)). % 35.19/23.05 tff(c_16455, plain, (icext(uri_rdf_List, sK5_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l32)=true)). % 35.19/23.05 tff(c_2162, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_rdf_rest, C_94), true, icext(C_94, sK5_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l32), true)=true))). % 35.19/23.05 tff(c_2084, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_94), true, icext(C_94, uri_rdf_Property), true)=true))). % 35.19/23.05 tff(c_2598, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_98), true, icext(C_98, uri_rdfs_domain), true)=true))). % 35.19/23.05 tff(c_2543, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdf_rest, C_98), true, icext(C_98, sK3_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l33), true)=true))). % 35.19/23.05 tff(c_2576, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_98), true, icext(C_98, uri_rdfs_subPropertyOf), true)=true))). % 35.19/23.05 tff(c_16179, plain, (![X_275, Y_276]: (ifeq(iext(uri_rdf_object, X_275, Y_276), true, icext(uri_rdfs_Statement, X_275), true)=true))). % 35.19/23.05 tff(c_2147, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_rdf_rest, C_94), true, icext(C_94, sK7_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l22), true)=true))). % 35.19/23.05 tff(c_2610, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdf_first, C_98), true, icext(C_98, sK9_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l12), true)=true))). % 35.19/23.05 tff(c_2126, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_94), true, icext(C_94, uri_rdfs_Class), true)=true))). % 35.19/23.05 tff(c_2116, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_rdf_first, C_94), true, icext(C_94, uri_ex_w1), true)=true))). % 35.19/23.05 tff(c_16125, plain, (iext(uri_rdf_type, sK3_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l33, uri_rdf_List)=true)). % 35.19/23.05 tff(c_2121, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_owl_oneOf, C_94), true, icext(C_94, sK6_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l21), true)=true))). % 35.19/23.05 tff(c_15942, plain, (icext(uri_rdf_List, sK3_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l33)=true)). % 35.19/23.05 tff(c_2608, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdf_first, C_98), true, icext(C_98, sK3_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l33), true)=true))). % 35.19/23.05 tff(c_2523, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdf_first, C_98), true, icext(C_98, sK4_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l31), true)=true))). % 35.19/23.05 tff(c_2568, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_98), true, icext(C_98, uri_rdf_rest), true)=true))). % 35.19/23.05 tff(c_2580, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_98), true, icext(C_98, uri_rdf_XMLLiteral), true)=true))). % 35.19/23.05 tff(c_15294, plain, (![X_256, Y_257]: (ifeq(iext(uri_rdfs_domain, X_256, Y_257), true, icext(uri_rdfs_Class, Y_257), true)=true))). % 35.19/23.05 tff(c_14213, plain, (![X_33]: (ifeq(icext(uri_rdfs_Statement, X_33), true, icext(uri_rdfs_Statement, X_33), true)=true))). % 35.19/23.05 tff(c_14573, plain, (![X_33]: (ifeq(icext(uri_rdf_List, X_33), true, icext(uri_rdf_List, X_33), true)=true))). % 35.19/23.05 tff(c_11683, plain, (![X_33]: (ifeq(icext(uri_rdfs_Datatype, X_33), true, icext(uri_rdfs_Datatype, X_33), true)=true))). % 35.19/23.05 tff(c_9012, plain, (![X_33]: (ifeq(icext(uri_rdf_Property, X_33), true, icext(uri_rdf_Property, X_33), true)=true))). % 35.19/23.05 tff(c_10511, plain, (![X_33]: (ifeq(icext(uri_rdf_XMLLiteral, X_33), true, icext(uri_rdf_XMLLiteral, X_33), true)=true))). % 35.19/23.05 tff(c_8857, plain, (![X_33]: (ifeq(icext(uri_rdf_Bag, X_33), true, icext(uri_rdf_Bag, X_33), true)=true))). % 35.19/23.05 tff(c_7645, plain, (![X_33]: (ifeq(icext(uri_rdfs_Container, X_33), true, icext(uri_rdfs_Container, X_33), true)=true))). % 35.19/23.05 tff(c_7243, plain, (![X_33]: (ifeq(icext(uri_rdf_Alt, X_33), true, icext(uri_rdf_Alt, X_33), true)=true))). % 35.19/23.05 tff(c_10312, plain, (![X_33]: (ifeq(icext(uri_rdfs_Literal, X_33), true, icext(uri_rdfs_Literal, X_33), true)=true))). % 35.19/23.05 tff(c_8014, plain, (![X_33]: (ifeq(icext(uri_rdfs_Class, X_33), true, icext(uri_rdfs_Class, X_33), true)=true))). % 35.19/23.05 tff(c_6253, plain, (![X_33]: (ifeq(icext(uri_rdfs_ContainerMembershipProperty, X_33), true, icext(uri_rdfs_ContainerMembershipProperty, X_33), true)=true))). % 35.19/23.05 tff(c_2522, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdf_rest, C_98), true, icext(C_98, sK2_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l42), true)=true))). % 35.19/23.05 tff(c_5197, plain, (![X_33]: (ifeq(icext(uri_rdfs_Seq, X_33), true, icext(uri_rdfs_Seq, X_33), true)=true))). % 35.19/23.05 tff(c_15020, plain, (iext(uri_rdf_type, uri_rdfs_Resource, uri_rdfs_Class)=true)). % 35.19/23.05 tff(c_14955, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_comment, uri_rdfs_comment)=true)). % 35.19/23.05 tff(c_14857, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_member, uri_rdfs_member)=true)). % 35.19/23.05 tff(c_14782, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Resource, uri_rdfs_Resource)=true)). % 35.19/23.05 tff(c_14583, plain, (iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdfs_Resource)=true)). % 35.19/23.05 tff(c_14517, plain, (iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdf_List)=true)). % 35.19/23.05 tff(c_14445, plain, (iext(uri_rdf_type, uri_rdf_List, uri_rdfs_Class)=true)). % 35.19/23.05 tff(c_2144, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_94), true, icext(C_94, uri_rdf_Property), true)=true))). % 35.19/23.05 tff(c_14302, plain, (ic(uri_rdf_List)=true)). % 35.19/23.05 tff(c_14244, plain, (icext(uri_rdfs_Class, uri_rdf_List)=true)). % 35.19/23.05 tff(c_2113, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_94), true, icext(C_94, uri_rdf_List), true)=true))). % 35.19/23.05 tff(c_14157, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Statement, uri_rdfs_Statement)=true)). % 35.19/23.05 tff(c_13988, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Statement, uri_rdfs_Resource)=true)). % 35.19/23.05 tff(c_2571, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_98), true, icext(C_98, uri_rdf__1), true)=true))). % 35.19/23.05 tff(c_13911, plain, (iext(uri_rdf_type, uri_rdfs_Literal, uri_rdfs_Class)=true)). % 35.19/23.05 tff(c_13863, plain, (iext(uri_rdf_type, uri_rdf_Bag, uri_rdfs_Class)=true)). % 35.19/23.05 tff(c_13791, plain, (iext(uri_rdf_type, uri_rdfs_Statement, uri_rdfs_Class)=true)). % 35.19/23.05 tff(c_2091, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_94), true, icext(C_94, uri_rdf_Property), true)=true))). % 35.19/23.05 tff(c_13656, plain, (ic(uri_rdfs_Statement)=true)). % 35.19/23.05 tff(c_13598, plain, (icext(uri_rdfs_Class, uri_rdfs_Statement)=true)). % 35.19/23.05 tff(c_2081, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_94), true, icext(C_94, uri_rdfs_Statement), true)=true))). % 35.19/23.05 tff(c_13529, plain, (iext(uri_rdf_type, uri_rdf_XMLLiteral, uri_rdfs_Class)=true)). % 35.19/23.05 tff(c_13482, plain, (iext(uri_rdf_type, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Class)=true)). % 35.19/23.05 tff(c_13434, plain, (iext(uri_rdf_type, uri_rdf_Alt, uri_rdfs_Class)=true)). % 35.19/23.05 tff(c_13387, plain, (iext(uri_rdf_type, uri_rdfs_Container, uri_rdfs_Class)=true)). % 35.19/23.05 tff(c_13340, plain, (iext(uri_rdf_type, uri_rdfs_Class, uri_rdfs_Class)=true)). % 35.19/23.05 tff(c_13292, plain, (iext(uri_rdf_type, uri_rdfs_Seq, uri_rdfs_Class)=true)). % 35.19/23.05 tff(c_2089, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_rdf_rest, C_94), true, icext(C_94, uri_rdf_nil), true)=true))). % 35.19/23.05 tff(c_13214, plain, (iext(uri_rdf_type, uri_rdfs_Datatype, uri_rdfs_Class)=true)). % 35.19/23.05 tff(c_13166, plain, (iext(uri_rdf_type, sK4_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l31, uri_rdf_List)=true)). % 35.19/23.05 tff(c_13119, plain, (iext(uri_rdf_type, sK1_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l41, uri_rdf_List)=true)). % 35.19/23.05 tff(c_13071, plain, (iext(uri_rdf_type, sK6_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l21, uri_rdf_List)=true)). % 35.19/23.05 tff(c_12936, plain, (icext(uri_rdf_List, sK4_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l31)=true)). % 35.19/23.05 tff(c_12869, plain, (iext(uri_rdf_type, sK2_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l42, uri_rdf_List)=true)). % 35.19/23.05 tff(c_2607, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdf_rest, C_98), true, icext(C_98, sK4_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l31), true)=true))). % 35.19/23.05 tff(c_12822, plain, (iext(uri_rdf_type, sK9_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l12, uri_rdf_List)=true)). % 35.19/23.05 tff(c_12780, plain, (ip(uri_rdfs_comment)=true)). % 35.19/23.05 tff(c_2154, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_rdf_rest, C_94), true, icext(C_94, sK9_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l12), true)=true))). % 35.19/23.05 tff(c_12698, plain, (iext(uri_rdf_type, uri_rdfs_comment, uri_rdf_Property)=true)). % 35.19/23.05 tff(c_12649, plain, (iext(uri_rdf_type, sK7_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l22, uri_rdf_List)=true)). % 35.19/23.05 tff(c_12593, plain, (iext(uri_rdf_type, uri_rdfs_member, uri_rdf_Property)=true)). % 35.19/23.05 tff(c_12439, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Container, uri_rdfs_Resource)=true)). % 35.19/23.05 tff(c_1571, plain, (![S_5, O_6]: (ifeq(iext(uri_owl_oneOf, S_5, O_6), true, true, true)=true))). % 35.19/23.05 tff(c_12256, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Resource)=true)). % 35.19/23.05 tff(c_2173, plain, (![S_5, O_6]: (ifeq(iext(uri_rdf_rest, S_5, O_6), true, true, true)=true))). % 35.19/23.05 tff(c_12094, plain, (icext(uri_rdf_Property, uri_rdfs_member)=true)). % 35.19/23.05 tff(c_2554, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_98), true, icext(C_98, uri_rdfs_member), true)=true))). % 35.19/23.05 tff(c_11896, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdfs_Resource)=true)). % 35.19/23.05 tff(c_11831, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_rest, uri_rdf_rest)=true)). % 35.19/23.05 tff(c_2137, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_owl_oneOf, C_94), true, icext(C_94, sK8_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l11), true)=true))). % 35.19/23.05 tff(c_11758, plain, (iext(uri_rdf_type, uri_rdfs_range, uri_rdf_Property)=true)). % 35.19/23.05 tff(c_11693, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, uri_rdfs_isDefinedBy)=true)). % 35.19/23.05 tff(c_11627, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Datatype)=true)). % 35.19/23.05 tff(c_11559, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_subject, uri_rdf_subject)=true)). % 35.19/23.05 tff(c_11441, plain, (icext(uri_rdf_Property, uri_rdfs_comment)=true)). % 35.19/23.05 tff(c_2531, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_98), true, icext(C_98, uri_rdfs_comment), true)=true))). % 35.19/23.05 tff(c_11356, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_seeAlso, uri_rdfs_seeAlso)=true)). % 35.19/23.05 tff(c_11290, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__2, uri_rdf__2)=true)). % 35.19/23.05 tff(c_2146, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_94), true, icext(C_94, uri_rdfs_Resource), true)=true))). % 35.19/23.05 tff(c_11196, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, uri_rdfs_domain)=true)). % 35.19/23.05 tff(c_11131, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_type, uri_rdf_type)=true)). % 35.19/23.05 tff(c_11064, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__3, uri_rdf__3)=true)). % 35.19/23.05 tff(c_10997, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__3, uri_rdfs_member)=true)). % 35.19/23.05 tff(c_10917, plain, (iext(uri_rdf_type, uri_rdfs_isDefinedBy, uri_rdf_Property)=true)). % 35.19/23.05 tff(c_2125, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_94), true, icext(C_94, uri_rdfs_ContainerMembershipProperty), true)=true))). % 35.19/23.05 tff(c_10781, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_value, uri_rdf_value)=true)). % 35.19/23.05 tff(c_10740, plain, (icext(uri_rdf_List, sK1_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l41)=true)). % 35.19/23.05 tff(c_2603, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdf_first, C_98), true, icext(C_98, sK1_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l41), true)=true))). % 35.19/23.05 tff(c_10664, plain, (iext(uri_rdf_type, uri_rdfs_seeAlso, uri_rdf_Property)=true)). % 35.19/23.05 tff(c_10545, plain, (icext(uri_rdf_Property, uri_rdfs_range)=true)). % 35.19/23.05 tff(c_2566, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_98), true, icext(C_98, uri_rdfs_range), true)=true))). % 35.19/23.05 tff(c_10455, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdf_XMLLiteral)=true)). % 35.19/23.05 tff(c_10343, plain, (icext(uri_rdf_List, sK9_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l12)=true)). % 35.19/23.05 tff(c_2535, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdf_rest, C_98), true, icext(C_98, sK9_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l12), true)=true))). % 35.19/23.05 tff(c_10253, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdfs_Literal)=true)). % 35.19/23.05 tff(c_10187, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__1, uri_rdfs_member)=true)). % 35.19/23.05 tff(c_10119, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf)=true)). % 35.19/23.05 tff(c_10005, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Resource)=true)). % 35.19/23.05 tff(c_9865, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Resource)=true)). % 35.19/23.05 tff(c_9798, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__1, uri_rdf__1)=true)). % 35.19/23.05 tff(c_2567, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_owl_oneOf, C_98), true, icext(C_98, uri_ex_c2), true)=true))). % 35.19/23.05 tff(c_3721, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_subPropertyOf, S_5, O_6), true, true, true)=true))). % 35.19/23.05 tff(c_9462, plain, (icext(uri_rdf_List, sK7_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l22)=true)). % 35.19/23.05 tff(c_2609, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdf_first, C_98), true, icext(C_98, sK7_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l22), true)=true))). % 35.19/23.05 tff(c_9405, plain, (ip(uri_rdfs_member)=true)). % 35.19/23.05 tff(c_9341, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__2, uri_rdfs_member)=true)). % 35.19/23.05 tff(c_9293, plain, (icext(uri_rdf_Property, uri_rdfs_isDefinedBy)=true)). % 35.19/23.05 tff(c_2524, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_98), true, icext(C_98, uri_rdfs_isDefinedBy), true)=true))). % 35.19/23.05 tff(c_9212, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_object, uri_rdf_object)=true)). % 35.19/23.05 tff(c_8935, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdf_Property)=true)). % 35.19/23.05 tff(c_2158, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_rdf_first, C_94), true, icext(C_94, uri_ex_c1), true)=true))). % 35.19/23.05 tff(c_8867, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_first, uri_rdf_first)=true)). % 35.19/23.05 tff(c_8801, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdf_Bag)=true)). % 35.19/23.05 tff(c_2547, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_98), true, icext(C_98, uri_rdfs_seeAlso), true)=true))). % 35.19/23.05 tff(c_8676, plain, (icext(uri_rdf_Property, uri_rdfs_subPropertyOf)=true)). % 35.19/23.05 tff(c_8622, plain, (iext(uri_rdf_type, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 35.19/23.05 tff(c_8558, plain, (iext(uri_rdfs_subPropertyOf, uri_owl_unionOf, uri_owl_unionOf)=true)). % 35.19/23.05 tff(c_2085, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_94), true, icext(C_94, uri_rdfs_Resource), true)=true))). % 35.19/23.05 tff(c_8432, plain, (icext(uri_rdf_Property, uri_owl_oneOf)=true)). % 35.19/23.05 tff(c_8378, plain, (iext(uri_rdf_type, uri_owl_oneOf, uri_rdf_Property)=true)). % 35.19/23.05 tff(c_2120, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_94), true, icext(C_94, uri_rdfs_Class), true)=true))). % 35.19/23.05 tff(c_1481, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_domain, S_5, O_6), true, true, true)=true))). % 35.19/23.05 tff(c_1651, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_range, S_5, O_6), true, true, true)=true))). % 35.19/23.05 tff(c_2106, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_94), true, icext(C_94, uri_rdfs_Container), true)=true))). % 35.19/23.05 tff(c_8024, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdfs_Resource)=true)). % 35.19/23.05 tff(c_7958, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdfs_Class)=true)). % 35.19/23.05 tff(c_2594, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_98), true, icext(C_98, uri_rdf_first), true)=true))). % 35.19/23.05 tff(c_7655, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdfs_Resource)=true)). % 35.19/23.05 tff(c_7589, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Container, uri_rdfs_Container)=true)). % 35.19/23.05 tff(c_2529, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_98), true, icext(C_98, uri_rdfs_ContainerMembershipProperty), true)=true))). % 35.19/23.05 tff(c_7497, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, uri_rdfs_subClassOf)=true)). % 35.19/23.05 tff(c_7416, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Resource)=true)). % 35.19/23.05 tff(c_7314, plain, (icext(uri_rdf_Property, uri_owl_unionOf)=true)). % 35.19/23.05 tff(c_7257, plain, (iext(uri_rdf_type, uri_owl_unionOf, uri_rdf_Property)=true)). % 35.19/23.05 tff(c_7163, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdf_Alt)=true)). % 35.19/23.05 tff(c_2560, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_98), true, icext(C_98, uri_rdf_rest), true)=true))). % 35.19/23.05 tff(c_1734, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_subClassOf, S_5, O_6), true, true, true)=true))). % 35.19/23.05 tff(c_7070, plain, (icext(uri_rdf_List, sK6_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l21)=true)). % 35.19/23.05 tff(c_6989, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Resource)=true)). % 35.19/23.05 tff(c_2565, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdf_first, C_98), true, icext(C_98, sK6_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l21), true)=true))). % 35.19/23.05 tff(c_6846, plain, (icext(uri_rdf_List, sK2_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l42)=true)). % 35.19/23.05 tff(c_2540, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdf_first, C_98), true, icext(C_98, sK2_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l42), true)=true))). % 35.19/23.05 tff(c_6779, plain, (icext(uri_rdfs_Class, uri_rdfs_Resource)=true)). % 35.19/23.05 tff(c_6715, plain, (ic(uri_rdfs_Resource)=true)). % 35.19/23.05 tff(c_2101, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_94), true, icext(C_94, uri_rdf_Property), true)=true))). % 35.19/23.05 tff(c_6630, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Resource)=true)). % 35.19/23.05 tff(c_6531, plain, (iext(uri_rdfs_subPropertyOf, uri_owl_oneOf, uri_owl_oneOf)=true)). % 35.19/23.05 tff(c_2533, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_owl_unionOf, C_98), true, icext(C_98, uri_ex_c4), true)=true))). % 35.19/23.05 tff(c_3680, plain, (![S_5, O_6]: (ifeq(iext(uri_rdf_object, S_5, O_6), true, true, true)=true))). % 35.19/23.05 tff(c_6429, plain, (icext(uri_rdf_Property, uri_rdfs_domain)=true)). % 35.19/23.05 tff(c_2575, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_98), true, icext(C_98, uri_rdf__2), true)=true))). % 35.19/23.05 tff(c_6346, plain, (iext(uri_rdf_type, uri_rdfs_domain, uri_rdf_Property)=true)). % 35.19/23.05 tff(c_6291, plain, (icext(uri_rdf_Property, uri_rdfs_seeAlso)=true)). % 35.19/23.05 tff(c_2557, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_98), true, icext(C_98, uri_rdfs_seeAlso), true)=true))). % 35.19/23.05 tff(c_3268, plain, (![S_5, O_6]: (ifeq(iext(uri_owl_unionOf, S_5, O_6), true, true, true)=true))). % 35.19/23.05 tff(c_6201, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdfs_ContainerMembershipProperty)=true)). % 35.19/23.05 tff(c_1724, plain, (![X_91]: (ifeq(icext(uri_rdf_Bag, X_91), true, icext(uri_rdfs_Container, X_91), true)=true))). % 35.19/23.05 tff(c_1728, plain, (![X_91]: (ifeq(icext(uri_rdfs_Seq, X_91), true, icext(uri_rdfs_Container, X_91), true)=true))). % 35.19/23.05 tff(c_1727, plain, (![X_91]: (ifeq(icext(uri_rdfs_Datatype, X_91), true, icext(uri_rdfs_Class, X_91), true)=true))). % 35.19/23.05 tff(c_5572, plain, (icext(uri_rdf_Property, uri_rdfs_subClassOf)=true)). % 35.19/23.05 tff(c_1723, plain, (![X_91]: (ifeq(icext(uri_rdfs_ContainerMembershipProperty, X_91), true, icext(uri_rdf_Property, X_91), true)=true))). % 35.19/23.05 tff(c_5454, plain, (iext(uri_rdf_type, uri_rdfs_subClassOf, uri_rdf_Property)=true)). % 35.19/23.05 tff(c_1725, plain, (![X_91]: (ifeq(icext(uri_rdf_Alt, X_91), true, icext(uri_rdfs_Container, X_91), true)=true))). % 35.19/23.05 tff(c_5248, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_range, uri_rdfs_range)=true)). % 35.19/23.05 tff(c_1726, plain, (![X_91]: (ifeq(icext(uri_rdf_XMLLiteral, X_91), true, icext(uri_rdfs_Literal, X_91), true)=true))). % 35.19/23.05 tff(c_5145, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Seq)=true)). % 35.19/23.05 tff(c_2133, plain, (![X_95, Y_96]: (ifeq(iext(uri_rdf_subject, X_95, Y_96), true, true, true)=true))). % 35.19/23.05 tff(c_2145, plain, (![X_95, Y_96]: (ifeq(iext(uri_rdf__3, X_95, Y_96), true, true, true)=true))). % 35.19/23.05 tff(c_2148, plain, (![X_95, Y_96]: (ifeq(iext(uri_rdf_first, X_95, Y_96), true, true, true)=true))). % 35.19/23.05 tff(c_2114, plain, (![X_95, Y_96]: (ifeq(iext(uri_rdf_predicate, X_95, Y_96), true, true, true)=true))). % 35.19/23.05 tff(c_5032, plain, (![X_131]: (iext(uri_rdf_type, X_131, uri_rdfs_Resource)=true))). % 35.19/23.05 tff(c_2094, plain, (![X_95, Y_96]: (ifeq(iext(uri_rdfs_member, X_95, Y_96), true, true, true)=true))). % 35.19/23.05 tff(c_2141, plain, (![X_95, Y_96]: (ifeq(iext(uri_rdf_value, X_95, Y_96), true, true, true)=true))). % 35.19/23.05 tff(c_2574, plain, (![X_99, Y_100]: (ifeq(iext(uri_rdf__2, X_99, Y_100), true, true, true)=true))). % 35.19/23.05 tff(c_2527, plain, (![X_99, Y_100]: (ifeq(iext(uri_rdfs_isDefinedBy, X_99, Y_100), true, true, true)=true))). % 35.19/23.05 tff(c_2530, plain, (![X_99, Y_100]: (ifeq(iext(uri_rdfs_comment, X_99, Y_100), true, true, true)=true))). % 35.19/23.05 tff(c_2538, plain, (![X_99, Y_100]: (ifeq(iext(uri_rdf_type, X_99, Y_100), true, true, true)=true))). % 35.19/23.05 tff(c_4873, plain, (icext(uri_rdfs_Class, uri_rdfs_ContainerMembershipProperty)=true)). % 35.19/23.05 tff(c_4826, plain, (icext(uri_rdfs_Class, uri_rdfs_Seq)=true)). % 35.19/23.05 tff(c_4776, plain, (icext(uri_rdfs_Class, uri_rdf_Alt)=true)). % 35.19/23.05 tff(c_2108, plain, (![X_95, Y_96]: (ifeq(iext(uri_rdfs_seeAlso, X_95, Y_96), true, true, true)=true))). % 35.19/23.05 tff(c_4730, plain, (icext(uri_rdfs_Class, uri_rdfs_Container)=true)). % 35.19/23.05 tff(c_4687, plain, (icext(uri_rdfs_Class, uri_rdfs_Class)=true)). % 35.19/23.05 tff(c_2578, plain, (![X_99, Y_100]: (ifeq(iext(uri_rdfs_label, X_99, Y_100), true, true, true)=true))). % 35.19/23.05 tff(c_4635, plain, (icext(uri_rdfs_Class, uri_rdf_Bag)=true)). % 35.19/23.05 tff(c_4592, plain, (icext(uri_rdfs_Class, uri_rdf_XMLLiteral)=true)). % 35.19/23.05 tff(c_4542, plain, (icext(uri_rdfs_Class, uri_rdfs_Literal)=true)). % 35.19/23.05 tff(c_2570, plain, (![X_99, Y_100]: (ifeq(iext(uri_rdf__1, X_99, Y_100), true, true, true)=true))). % 35.19/23.05 tff(c_4494, plain, (icext(uri_rdfs_Class, uri_rdfs_Datatype)=true)). % 35.19/23.05 tff(c_4443, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__2)=true)). % 35.19/23.05 tff(c_4404, plain, (icext(uri_rdf_Property, uri_rdf__2)=true)). % 35.19/23.05 tff(c_4363, plain, (icext(uri_rdf_Property, uri_rdf__3)=true)). % 35.19/23.05 tff(c_4325, plain, (icext(uri_rdf_Property, uri_rdf_rest)=true)). % 35.19/23.05 tff(c_4286, plain, (icext(uri_rdf_Property, uri_rdf_value)=true)). % 35.19/23.05 tff(c_4247, plain, (icext(uri_rdf_List, uri_rdf_nil)=true)). % 35.19/23.05 tff(c_4200, plain, (icext(uri_rdfs_Datatype, uri_rdf_XMLLiteral)=true)). % 35.19/23.05 tff(c_4158, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__3)=true)). % 35.19/23.05 tff(c_4117, plain, (icext(uri_rdf_Property, uri_rdf_first)=true)). % 35.19/23.05 tff(c_4076, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__1)=true)). % 35.19/23.05 tff(c_4021, plain, (icext(uri_rdf_Property, uri_rdf__1)=true)). % 35.19/23.05 tff(c_3976, plain, (icext(uri_rdf_Property, uri_rdf_subject)=true)). % 35.19/23.05 tff(c_3929, plain, (icext(uri_rdfs_Class, uri_rdf_Property)=true)). % 35.19/23.05 tff(c_3880, plain, (icext(uri_rdf_Property, uri_rdf_object)=true)). % 35.19/23.05 tff(c_3839, plain, (icext(uri_rdf_Property, uri_rdf_type)=true)). % 35.19/23.05 tff(c_3796, plain, (ip(uri_rdf__2)=true)). % 35.19/23.05 tff(c_3753, plain, (ic(uri_rdf_XMLLiteral)=true)). % 35.19/23.05 tff(c_3709, plain, (ip(uri_rdfs_subPropertyOf)=true)). % 35.19/23.05 tff(c_3666, plain, (ip(uri_rdf_object)=true)). % 35.19/23.05 tff(c_3631, plain, (ic(uri_rdfs_Class)=true)). % 35.19/23.05 tff(c_3595, plain, (ic(uri_rdf_Alt)=true)). % 35.19/23.05 tff(c_3559, plain, (ic(uri_rdf_Property)=true)). % 35.19/23.05 tff(c_3517, plain, (ip(uri_rdf__1)=true)). % 35.19/23.06 tff(c_3475, plain, (ic(uri_rdf_Bag)=true)). % 35.19/23.06 tff(c_3429, plain, (ip(uri_rdf__3)=true)). % 35.19/23.06 tff(c_3317, plain, (ic(uri_rdfs_Datatype)=true)). % 35.19/23.06 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))). % 35.19/23.06 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))). % 35.19/23.06 tff(c_3256, plain, (ip(uri_owl_unionOf)=true)). % 35.19/23.06 tff(c_3217, plain, (ip(uri_rdf_value)=true)). % 35.19/23.06 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))). % 35.19/23.06 tff(c_2200, plain, (ic(uri_rdfs_Container)=true)). % 35.19/23.06 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))). % 35.19/23.06 tff(c_1757, plain, (ip(uri_rdf_rest)=true)). % 35.19/23.06 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))). % 35.19/23.06 tff(c_1685, plain, (ip(uri_rdfs_subClassOf)=true)). % 35.19/23.06 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))). % 35.19/23.06 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))). % 35.19/23.06 tff(c_1639, plain, (ip(uri_rdfs_range)=true)). % 35.19/23.06 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))). % 35.19/23.06 tff(c_1594, plain, (ic(uri_rdfs_ContainerMembershipProperty)=true)). % 35.19/23.06 tff(c_1504, plain, (ip(uri_owl_oneOf)=true)). % 35.19/23.06 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))). % 35.19/23.06 tff(c_1414, plain, (ip(uri_rdfs_domain)=true)). % 35.19/23.06 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))). % 35.19/23.06 tff(c_1375, plain, (ip(uri_rdf_first)=true)). % 35.19/23.06 tff(c_4, plain, (![P_4, S_5, O_6]: (ifeq(iext(P_4, S_5, O_6), true, ip(P_4), true)=true))). % 35.19/23.06 tff(c_1039, plain, (ic(uri_rdfs_Seq)=true)). % 35.19/23.06 tff(c_152, plain, (![C_37, D_38]: (ifeq(iext(uri_rdfs_subClassOf, C_37, D_38), true, ic(C_37), true)=true))). % 35.19/23.06 tff(c_971, plain, (ic(uri_rdfs_Literal)=true)). % 35.19/23.06 tff(c_935, plain, (ip(uri_rdf_subject)=true)). % 35.19/23.06 tff(c_150, plain, (![C_35, D_36]: (ifeq(iext(uri_rdfs_subClassOf, C_35, D_36), true, ic(D_36), true)=true))). % 35.19/23.06 tff(c_874, plain, (ip(uri_rdf_type)=true)). % 35.19/23.06 tff(c_30, plain, (![P_10]: (ifeq(iext(uri_rdf_type, P_10, uri_rdf_Property), true, ip(P_10), true)=true))). % 35.19/23.06 tff(c_58, plain, (![C_15]: (ifeq(ic(C_15), true, iext(uri_rdfs_subClassOf, C_15, uri_rdfs_Resource), true)=true))). % 35.19/23.06 tff(c_771, plain, (ip(uri_rdfs_seeAlso)=true)). % 35.19/23.06 tff(c_156, plain, (![C_39]: (ifeq(ic(C_39), true, iext(uri_rdfs_subClassOf, C_39, C_39), true)=true))). % 35.19/23.06 tff(c_162, plain, (![P_43, Q_44]: (ifeq(iext(uri_rdfs_subPropertyOf, P_43, Q_44), true, ip(Q_44), true)=true))). % 35.19/23.06 tff(c_693, plain, (ip(uri_rdfs_isDefinedBy)=true)). % 35.19/23.06 tff(c_28, plain, (![P_9]: (ifeq(ip(P_9), true, iext(uri_rdf_type, P_9, uri_rdf_Property), true)=true))). % 35.19/23.06 tff(c_164, plain, (![P_45, Q_46]: (ifeq(iext(uri_rdfs_subPropertyOf, P_45, Q_46), true, ip(P_45), true)=true))). % 35.19/23.06 tff(c_170, plain, (![P_51]: (ifeq(ip(P_51), true, iext(uri_rdfs_subPropertyOf, P_51, P_51), true)=true))). % 35.19/23.06 tff(c_124, plain, (![X_27]: (ifeq(lv(X_27), true, icext(uri_rdfs_Literal, X_27), true)=true))). % 35.19/23.06 tff(c_114, plain, (![X_22]: (ifeq(ic(X_22), true, icext(uri_rdfs_Class, X_22), true)=true))). % 35.19/23.06 tff(c_116, plain, (![X_23]: (ifeq(icext(uri_rdfs_Class, X_23), true, ic(X_23), true)=true))). % 35.19/23.06 tff(c_122, plain, (![X_26]: (ifeq(icext(uri_rdfs_Literal, X_26), true, lv(X_26), true)=true))). % 35.19/23.06 tff(c_591, plain, (![X_61]: (icext(uri_rdfs_Resource, X_61)=true))). % 35.19/23.06 tff(c_229, plain, (![X_8]: (ifeq(lv(X_8), true, true, true)=true))). % 35.19/23.06 tff(c_2, plain, (![A_1, B_2, C_3]: (ifeq(A_1, A_1, B_2, C_3)=B_2))). % 35.19/23.06 tff(c_190, plain, (iext(uri_rdf_rest, sK1_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l41, sK2_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l42)=true)). % 35.19/23.06 tff(c_34, plain, (iext(uri_rdf_type, uri_rdf_type, uri_rdf_Property)=true)). % 35.19/23.06 tff(c_192, plain, (iext(uri_rdf_rest, sK2_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l42, uri_rdf_nil)=true)). % 35.19/23.06 tff(c_214, plain, (iext(uri_rdf_first, sK4_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l31, uri_ex_w1)=true)). % 35.19/23.06 tff(c_42, plain, (iext(uri_rdfs_range, uri_rdfs_isDefinedBy, uri_rdfs_Resource)=true)). % 35.19/23.06 tff(c_134, plain, (iext(uri_rdfs_domain, uri_rdf_object, uri_rdfs_Statement)=true)). % 35.19/23.06 tff(c_10, plain, (iext(uri_rdf_type, uri_rdf_first, uri_rdf_Property)=true)). % 35.19/23.06 tff(c_40, plain, (iext(uri_rdfs_domain, uri_rdfs_isDefinedBy, uri_rdfs_Resource)=true)). % 35.19/23.06 tff(c_74, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property)=true)). % 35.19/23.06 tff(c_36, plain, (iext(uri_rdfs_domain, uri_rdfs_comment, uri_rdfs_Resource)=true)). % 35.19/23.06 tff(c_26, plain, (iext(uri_rdf_type, uri_rdf_subject, uri_rdf_Property)=true)). % 35.19/23.06 tff(c_182, plain, (iext(uri_owl_unionOf, uri_ex_c4, sK1_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l41)=true)). % 35.19/23.06 tff(c_126, plain, (iext(uri_rdf_type, uri_rdf_Property, uri_rdfs_Class)=true)). % 35.19/23.06 tff(c_206, plain, (iext(uri_rdf_rest, sK9_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l12, uri_rdf_nil)=true)). % 35.19/23.06 tff(c_44, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso)=true)). % 35.19/23.06 tff(c_128, plain, (iext(uri_rdfs_domain, uri_rdfs_range, uri_rdf_Property)=true)). % 35.19/23.06 tff(c_174, plain, (iext(uri_rdfs_domain, uri_rdf_type, uri_rdfs_Resource)=true)). % 35.19/23.06 tff(c_210, plain, (iext(uri_rdf_first, sK2_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l42, uri_ex_c2)=true)). % 35.19/23.06 tff(c_78, plain, (iext(uri_rdfs_range, uri_rdfs_member, uri_rdfs_Resource)=true)). % 35.19/23.06 tff(c_48, plain, (iext(uri_rdfs_range, uri_rdfs_label, uri_rdfs_Literal)=true)). % 35.19/23.06 tff(c_194, plain, (iext(uri_rdf_rest, sK3_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l33, uri_rdf_nil)=true)). % 35.19/23.06 tff(c_216, plain, (iext(uri_rdf_first, sK5_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l32, uri_ex_w2)=true)). % 35.19/23.06 tff(c_22, plain, (iext(uri_rdf_type, uri_rdf_object, uri_rdf_Property)=true)). % 35.19/23.06 tff(c_50, plain, (iext(uri_rdfs_domain, uri_rdfs_seeAlso, uri_rdfs_Resource)=true)). % 35.19/23.06 tff(c_18, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdf_Property)=true)). % 35.19/23.06 tff(c_202, plain, (iext(uri_rdf_rest, sK7_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l22, uri_rdf_nil)=true)). % 35.19/23.06 tff(c_84, plain, (iext(uri_rdfs_domain, uri_rdf__3, uri_rdfs_Resource)=true)). % 35.19/23.06 tff(c_12, plain, (iext(uri_rdf_type, uri_rdf_nil, uri_rdf_List)=true)). % 35.19/23.06 tff(c_76, plain, (iext(uri_rdfs_domain, uri_rdfs_member, uri_rdfs_Resource)=true)). % 35.19/23.06 tff(c_70, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Container)=true)). % 35.19/23.06 tff(c_20, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdf_Property)=true)). % 35.19/23.06 tff(c_52, plain, (iext(uri_rdfs_range, uri_rdfs_seeAlso, uri_rdfs_Resource)=true)). % 35.19/23.06 tff(c_86, plain, (iext(uri_rdfs_range, uri_rdf__1, uri_rdfs_Resource)=true)). % 35.19/23.06 tff(c_94, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdfs_ContainerMembershipProperty)=true)). % 35.19/23.06 tff(c_64, plain, (iext(uri_rdfs_domain, uri_rdf_rest, uri_rdf_List)=true)). % 35.19/23.06 tff(c_140, plain, (iext(uri_rdfs_range, uri_rdf_predicate, uri_rdfs_Resource)=true)). % 35.19/23.06 tff(c_222, plain, (iext(uri_rdf_first, sK8_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l11, uri_ex_w1)=true)). % 35.19/23.06 tff(c_176, plain, (iext(uri_rdfs_range, uri_rdf_type, uri_rdfs_Class)=true)). % 35.19/23.06 tff(c_24, plain, (iext(uri_rdf_type, uri_rdf_value, uri_rdf_Property)=true)). % 35.19/23.06 tff(c_218, plain, (iext(uri_rdf_first, sK6_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l21, uri_ex_w2)=true)). % 35.19/23.06 tff(c_132, plain, (iext(uri_rdfs_range, uri_rdfs_range, uri_rdfs_Class)=true)). % 35.19/23.06 tff(c_184, plain, (iext(uri_owl_oneOf, uri_ex_c2, sK6_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l21)=true)). % 35.19/23.06 tff(c_66, plain, (iext(uri_rdfs_range, uri_rdf_rest, uri_rdf_List)=true)). % 35.19/23.06 tff(c_68, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Container)=true)). % 35.19/23.06 tff(c_80, plain, (iext(uri_rdfs_domain, uri_rdf__1, uri_rdfs_Resource)=true)). % 35.19/23.06 tff(c_92, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdfs_ContainerMembershipProperty)=true)). % 35.19/23.06 tff(c_146, plain, (iext(uri_rdfs_domain, uri_rdfs_subClassOf, uri_rdfs_Class)=true)). % 35.19/23.06 tff(c_226, plain, (iext(uri_owl_equivalentClass, uri_ex_c3, uri_ex_c4)!=true)). % 35.19/23.06 tff(c_82, plain, (iext(uri_rdfs_domain, uri_rdf__2, uri_rdfs_Resource)=true)). % 35.19/23.06 tff(c_160, plain, (iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 35.19/23.06 tff(c_88, plain, (iext(uri_rdfs_range, uri_rdf__2, uri_rdfs_Resource)=true)). % 35.19/23.06 tff(c_46, plain, (iext(uri_rdfs_domain, uri_rdfs_label, uri_rdfs_Resource)=true)). % 35.19/23.06 tff(c_100, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Literal)=true)). % 35.19/23.06 tff(c_144, plain, (iext(uri_rdfs_range, uri_rdf_subject, uri_rdfs_Resource)=true)). % 35.19/23.06 tff(c_38, plain, (iext(uri_rdfs_range, uri_rdfs_comment, uri_rdfs_Literal)=true)). % 35.19/23.06 tff(c_178, plain, (iext(uri_rdfs_domain, uri_rdf_value, uri_rdfs_Resource)=true)). % 35.19/23.06 tff(c_186, plain, (iext(uri_owl_oneOf, uri_ex_c1, sK8_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l11)=true)). % 35.19/23.06 tff(c_106, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Class)=true)). % 35.19/23.06 tff(c_138, plain, (iext(uri_rdfs_domain, uri_rdf_predicate, uri_rdfs_Statement)=true)). % 35.19/23.06 tff(c_16, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdf_Property)=true)). % 35.19/23.06 tff(c_180, plain, (iext(uri_rdfs_range, uri_rdf_value, uri_rdfs_Resource)=true)). % 35.19/23.06 tff(c_154, plain, (iext(uri_rdfs_range, uri_rdfs_subClassOf, uri_rdfs_Class)=true)). % 35.19/23.06 tff(c_168, plain, (iext(uri_rdfs_range, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 35.19/23.06 tff(c_90, plain, (iext(uri_rdfs_range, uri_rdf__3, uri_rdfs_Resource)=true)). % 35.19/23.06 tff(c_200, plain, (iext(uri_rdf_rest, sK6_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l21, sK7_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l22)=true)). % 35.19/23.06 tff(c_62, plain, (iext(uri_rdfs_range, uri_rdf_first, uri_rdfs_Resource)=true)). % 35.19/23.06 tff(c_198, plain, (iext(uri_rdf_rest, sK5_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l32, sK3_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l33)=true)). % 35.19/23.06 tff(c_142, plain, (iext(uri_rdfs_domain, uri_rdf_subject, uri_rdfs_Statement)=true)). % 35.19/23.06 tff(c_60, plain, (iext(uri_rdfs_domain, uri_rdf_first, uri_rdf_List)=true)). % 35.19/23.06 tff(c_112, plain, (iext(uri_rdfs_range, uri_rdfs_domain, uri_rdfs_Class)=true)). % 35.19/23.06 tff(c_204, plain, (iext(uri_rdf_rest, sK8_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l11, sK9_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l12)=true)). % 35.19/23.06 tff(c_96, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdfs_ContainerMembershipProperty)=true)). % 35.19/23.06 tff(c_102, plain, (iext(uri_rdf_type, uri_rdf_XMLLiteral, uri_rdfs_Datatype)=true)). % 35.19/23.06 tff(c_14, plain, (iext(uri_rdf_type, uri_rdf_rest, uri_rdf_Property)=true)). % 35.19/23.06 tff(c_208, plain, (iext(uri_rdf_first, sK1_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l41, uri_ex_c1)=true)). % 35.19/23.06 tff(c_188, plain, (iext(uri_owl_oneOf, uri_ex_c3, sK4_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l31)=true)). % 35.19/23.06 tff(c_108, plain, (iext(uri_rdfs_domain, uri_rdfs_domain, uri_rdf_Property)=true)). % 35.19/23.06 tff(c_98, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Container)=true)). % 35.19/23.06 tff(c_196, plain, (iext(uri_rdf_rest, sK4_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l31, sK5_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l32)=true)). % 35.19/23.06 tff(c_212, plain, (iext(uri_rdf_first, sK3_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l33, uri_ex_w3)=true)). % 35.19/23.06 tff(c_220, plain, (iext(uri_rdf_first, sK7_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l22, uri_ex_w3)=true)). % 35.19/23.06 tff(c_224, plain, (iext(uri_rdf_first, sK9_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l12, uri_ex_w2)=true)). % 35.19/23.06 tff(c_6, plain, (![X_7]: (ir(X_7)=true))). % 35.19/23.06 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 35.19/23.06 %------------------------------------------------------------------------------