%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SWB022-10 : TPTP v9.0.0. Released v7.3.0. % Transfm : none % Format : tptp:raw % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n020.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Apr 9 09:15:54 PM UTC 2025 % Result : Satisfiable 40.99s 29.25s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SWB022-10 : TPTP v9.0.0. Released v7.3.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 : n020.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Wed Apr 9 00:59:49 EDT 2025 % 0.13/0.34 % CPUTime : % 40.99/29.24 % 40.99/29.25 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 40.99/29.25 % 40.99/29.25 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 41.10/29.28 %$ ifeq > tuple > iext > icext > #nlpp > lv > ir > ip > ic > uri_skos_memberList > uri_skos_member > uri_skos_OrderedCollection > 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_propertyChainAxiom > uri_ex_Z > uri_ex_Y > uri_ex_X > uri_ex_MyOrderedCollection > true > sK8_testcase_premise_fullish_022_List_Member_Access_BNODE_l11 > sK7_testcase_premise_fullish_022_List_Member_Access_BNODE_l21 > sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL > sK5_testcase_premise_fullish_022_List_Member_Access_BNODE_l12 > sK4_testcase_premise_fullish_022_List_Member_Access_BNODE_l22 > sK3_testcase_premise_fullish_022_List_Member_Access_BNODE_l32 > sK2_testcase_premise_fullish_022_List_Member_Access_BNODE_l31 > sK1_testcase_premise_fullish_022_List_Member_Access_BNODE_l33 % 41.10/29.28 % 41.10/29.28 %Foreground sorts: % 41.10/29.28 % 41.10/29.28 % 41.10/29.28 %Background operators: % 41.10/29.28 % 41.10/29.28 % 41.10/29.28 %Foreground operators: % 41.10/29.28 tff(uri_rdfs_Datatype, type, uri_rdfs_Datatype: $i). % 41.10/29.28 tff(uri_skos_memberList, type, uri_skos_memberList: $i). % 41.10/29.28 tff(uri_rdfs_ContainerMembershipProperty, type, uri_rdfs_ContainerMembershipProperty: $i). % 41.10/29.28 tff(uri_rdfs_Resource, type, uri_rdfs_Resource: $i). % 41.10/29.28 tff(uri_rdf_Property, type, uri_rdf_Property: $i). % 41.10/29.28 tff(uri_rdf_subject, type, uri_rdf_subject: $i). % 41.10/29.28 tff(tuple, type, tuple: ($i * $i * $i) > $i). % 41.10/29.28 tff(sK8_testcase_premise_fullish_022_List_Member_Access_BNODE_l11, type, sK8_testcase_premise_fullish_022_List_Member_Access_BNODE_l11: $i). % 41.10/29.28 tff(uri_rdf_type, type, uri_rdf_type: $i). % 41.10/29.28 tff(sK2_testcase_premise_fullish_022_List_Member_Access_BNODE_l31, type, sK2_testcase_premise_fullish_022_List_Member_Access_BNODE_l31: $i). % 41.10/29.28 tff(uri_rdfs_subPropertyOf, type, uri_rdfs_subPropertyOf: $i). % 41.10/29.28 tff(uri_rdfs_seeAlso, type, uri_rdfs_seeAlso: $i). % 41.10/29.28 tff(icext, type, icext: ($i * $i) > $i). % 41.10/29.28 tff(uri_rdfs_range, type, uri_rdfs_range: $i). % 41.10/29.28 tff(uri_rdf_XMLLiteral, type, uri_rdf_XMLLiteral: $i). % 41.10/29.28 tff(uri_rdf_List, type, uri_rdf_List: $i). % 41.10/29.28 tff(uri_rdf_first, type, uri_rdf_first: $i). % 41.10/29.28 tff(uri_ex_Y, type, uri_ex_Y: $i). % 41.10/29.28 tff(uri_rdf_predicate, type, uri_rdf_predicate: $i). % 41.10/29.28 tff(ir, type, ir: $i > $i). % 41.10/29.28 tff(lv, type, lv: $i > $i). % 41.10/29.28 tff(uri_rdf__3, type, uri_rdf__3: $i). % 41.10/29.28 tff(uri_rdf_value, type, uri_rdf_value: $i). % 41.10/29.28 tff(uri_skos_member, type, uri_skos_member: $i). % 41.10/29.28 tff(ic, type, ic: $i > $i). % 41.10/29.28 tff(uri_rdfs_Statement, type, uri_rdfs_Statement: $i). % 41.10/29.28 tff(uri_rdf__1, type, uri_rdf__1: $i). % 41.10/29.28 tff(iext, type, iext: ($i * $i * $i) > $i). % 41.10/29.28 tff(uri_skos_OrderedCollection, type, uri_skos_OrderedCollection: $i). % 41.10/29.28 tff(sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL, type, sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL: $i). % 41.10/29.28 tff(sK1_testcase_premise_fullish_022_List_Member_Access_BNODE_l33, type, sK1_testcase_premise_fullish_022_List_Member_Access_BNODE_l33: $i). % 41.10/29.28 tff(uri_rdf_rest, type, uri_rdf_rest: $i). % 41.10/29.28 tff(uri_rdfs_label, type, uri_rdfs_label: $i). % 41.10/29.28 tff(uri_rdfs_Container, type, uri_rdfs_Container: $i). % 41.10/29.28 tff(uri_owl_propertyChainAxiom, type, uri_owl_propertyChainAxiom: $i). % 41.10/29.28 tff(uri_rdfs_subClassOf, type, uri_rdfs_subClassOf: $i). % 41.10/29.28 tff(sK3_testcase_premise_fullish_022_List_Member_Access_BNODE_l32, type, sK3_testcase_premise_fullish_022_List_Member_Access_BNODE_l32: $i). % 41.10/29.28 tff(uri_rdf_object, type, uri_rdf_object: $i). % 41.10/29.28 tff(ip, type, ip: $i > $i). % 41.10/29.28 tff(uri_rdfs_Class, type, uri_rdfs_Class: $i). % 41.10/29.28 tff(uri_rdfs_Seq, type, uri_rdfs_Seq: $i). % 41.10/29.28 tff(uri_ex_X, type, uri_ex_X: $i). % 41.10/29.28 tff(uri_rdfs_member, type, uri_rdfs_member: $i). % 41.10/29.28 tff(uri_rdf_Bag, type, uri_rdf_Bag: $i). % 41.10/29.28 tff(uri_rdf__2, type, uri_rdf__2: $i). % 41.10/29.28 tff(sK7_testcase_premise_fullish_022_List_Member_Access_BNODE_l21, type, sK7_testcase_premise_fullish_022_List_Member_Access_BNODE_l21: $i). % 41.10/29.28 tff(uri_ex_Z, type, uri_ex_Z: $i). % 41.10/29.28 tff(uri_rdfs_comment, type, uri_rdfs_comment: $i). % 41.10/29.28 tff(sK5_testcase_premise_fullish_022_List_Member_Access_BNODE_l12, type, sK5_testcase_premise_fullish_022_List_Member_Access_BNODE_l12: $i). % 41.10/29.28 tff(uri_rdfs_Literal, type, uri_rdfs_Literal: $i). % 41.10/29.28 tff(true, type, true: $i). % 41.10/29.28 tff(uri_rdf_Alt, type, uri_rdf_Alt: $i). % 41.10/29.28 tff(uri_rdf_nil, type, uri_rdf_nil: $i). % 41.10/29.28 tff(uri_rdfs_isDefinedBy, type, uri_rdfs_isDefinedBy: $i). % 41.10/29.28 tff(uri_rdfs_domain, type, uri_rdfs_domain: $i). % 41.10/29.28 tff(uri_ex_MyOrderedCollection, type, uri_ex_MyOrderedCollection: $i). % 41.10/29.28 tff(sK4_testcase_premise_fullish_022_List_Member_Access_BNODE_l22, type, sK4_testcase_premise_fullish_022_List_Member_Access_BNODE_l22: $i). % 41.10/29.28 tff(ifeq, type, ifeq: ($i * $i * $i * $i) > $i). % 41.10/29.28 % 41.10/29.28 %Saturated clause set: % 41.10/29.28 tff(c_14048, 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))). % 41.10/29.28 tff(c_14045, 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))). % 41.10/29.28 tff(c_14505, 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))). % 41.10/29.28 tff(c_80611, plain, (![X_1346, Y_1347]: (ifeq(iext(uri_rdfs_comment, X_1346, Y_1347), true, iext(uri_rdfs_comment, X_1346, Y_1347), true)=true))). % 41.10/29.28 tff(c_14443, 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))). % 41.10/29.28 tff(c_80457, plain, (![X_1341, Y_1342]: (ifeq(iext(uri_rdfs_label, X_1341, Y_1342), true, iext(uri_rdfs_label, X_1341, Y_1342), true)=true))). % 41.10/29.28 tff(c_18739, 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))). % 41.10/29.28 tff(c_14378, 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))). % 41.10/29.28 tff(c_80180, plain, (![X_1335, Y_1336]: (ifeq(iext(uri_rdf_predicate, X_1335, Y_1336), true, iext(uri_rdf_predicate, X_1335, Y_1336), true)=true))). % 41.10/29.28 tff(c_80019, plain, (![X_1329, Y_1330]: (ifeq(iext(uri_rdfs_member, X_1329, Y_1330), true, iext(uri_rdfs_member, X_1329, Y_1330), true)=true))). % 41.10/29.28 tff(c_5356, 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))). % 41.10/29.28 tff(c_14212, 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))). % 41.10/29.28 tff(c_14288, 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))). % 41.10/29.28 tff(c_5353, 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))). % 41.10/29.29 tff(c_13991, 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))). % 41.10/29.29 tff(c_16439, 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))). % 41.10/29.29 tff(c_17903, 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))). % 41.10/29.29 tff(c_17621, 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))). % 41.10/29.29 tff(c_15767, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_skos_OrderedCollection, uri_rdfs_Resource), true, true, true), true)=true))). % 41.10/29.29 tff(c_16373, 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))). % 41.10/29.29 tff(c_78575, plain, (![C_1317]: (ifeq(iext(uri_rdfs_subClassOf, C_1317, uri_rdfs_Statement), true, iext(uri_rdfs_subClassOf, C_1317, uri_rdfs_Resource), true)=true))). % 41.10/29.29 tff(c_78428, plain, (![C_1315]: (ifeq(iext(uri_rdfs_subClassOf, C_1315, uri_skos_OrderedCollection), true, iext(uri_rdfs_subClassOf, C_1315, uri_rdfs_Resource), true)=true))). % 41.10/29.29 tff(c_15701, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_skos_OrderedCollection, uri_skos_OrderedCollection), true, true, true), true)=true))). % 41.10/29.29 tff(c_78155, plain, (![C_1312]: (ifeq(iext(uri_rdfs_subClassOf, C_1312, uri_rdf_List), true, iext(uri_rdfs_subClassOf, C_1312, uri_rdfs_Resource), true)=true))). % 41.10/29.29 tff(c_8515, 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))). % 41.10/29.29 tff(c_5643, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL), true, true, true), true)=true))). % 41.10/29.29 tff(c_13868, 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))). % 41.10/29.29 tff(c_5993, 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))). % 41.10/29.29 tff(c_8844, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_owl_propertyChainAxiom), true, true, true), true)=true))). % 41.10/29.29 tff(c_5996, 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))). % 41.10/29.29 tff(c_13699, 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))). % 41.10/29.29 tff(c_13376, 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))). % 41.10/29.29 tff(c_13915, 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))). % 41.10/29.29 tff(c_13747, 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))). % 41.10/29.29 tff(c_13329, 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))). % 41.10/29.29 tff(c_13821, 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))). % 41.10/29.29 tff(c_13424, 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))). % 41.10/29.29 tff(c_11571, 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))). % 41.10/29.29 tff(c_12851, 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))). % 41.10/29.29 tff(c_9910, 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))). % 41.10/29.29 tff(c_7186, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_skos_memberList, Y_21), true, true, true), true)=true))). % 41.10/29.29 tff(c_5646, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL, Y_21), true, true, true), true)=true))). % 41.10/29.29 tff(c_10625, 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))). % 41.10/29.29 tff(c_8512, 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))). % 41.10/29.29 tff(c_8847, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_owl_propertyChainAxiom, Y_21), true, true, true), true)=true))). % 41.10/29.29 tff(c_11568, 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))). % 41.10/29.29 tff(c_10622, 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))). % 41.10/29.29 tff(c_9907, 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))). % 41.10/29.29 tff(c_7183, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_skos_memberList), true, true, true), true)=true))). % 41.10/29.29 tff(c_18491, 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))). % 41.10/29.29 tff(c_17565, 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))). % 41.10/29.29 tff(c_12654, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, sK3_testcase_premise_fullish_022_List_Member_Access_BNODE_l32, uri_rdf_List), true, true, true), true)=true))). % 41.10/29.29 tff(c_12802, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, sK4_testcase_premise_fullish_022_List_Member_Access_BNODE_l22, uri_rdf_List), true, true, true), true)=true))). % 41.10/29.29 tff(c_13532, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, sK1_testcase_premise_fullish_022_List_Member_Access_BNODE_l33, uri_rdf_List), true, true, true), true)=true))). % 41.10/29.29 tff(c_12701, 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))). % 41.10/29.29 tff(c_13162, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, sK5_testcase_premise_fullish_022_List_Member_Access_BNODE_l12, uri_rdf_List), true, true, true), true)=true))). % 41.10/29.29 tff(c_12530, 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))). % 41.10/29.30 tff(c_15644, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_skos_OrderedCollection, uri_rdfs_Class), true, true, true), true)=true))). % 41.10/29.30 tff(c_13053, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, sK2_testcase_premise_fullish_022_List_Member_Access_BNODE_l31, uri_rdf_List), true, true, true), true)=true))). % 41.10/29.30 tff(c_16317, 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))). % 41.10/29.30 tff(c_73292, plain, (![C_1258]: (ifeq(iext(uri_rdfs_subClassOf, C_1258, uri_rdfs_Literal), true, iext(uri_rdfs_subClassOf, C_1258, uri_rdfs_Resource), true)=true))). % 41.10/29.30 tff(c_5912, 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))). % 41.10/29.30 tff(c_11432, 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))). % 41.10/29.30 tff(c_9088, 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))). % 41.10/29.30 tff(c_4584, 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))). % 41.10/29.30 tff(c_8653, 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))). % 41.10/29.30 tff(c_5832, 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))). % 41.10/29.30 tff(c_72199, plain, (![X_1247, Y_1248]: (ifeq(iext(uri_rdfs_range, X_1247, Y_1248), true, iext(uri_rdfs_range, X_1247, Y_1248), true)=true))). % 41.10/29.30 tff(c_8787, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_owl_propertyChainAxiom, uri_rdf_Property), true, true, true), true)=true))). % 41.10/29.30 tff(c_9849, 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))). % 41.10/29.30 tff(c_71872, plain, (![P_1243]: (ifeq(iext(uri_rdfs_subPropertyOf, P_1243, uri_rdf__3), true, iext(uri_rdfs_subPropertyOf, P_1243, uri_rdfs_member), true)=true))). % 41.10/29.30 tff(c_71045, plain, (![X_1239, Y_1240]: (ifeq(iext(uri_rdf_type, X_1239, Y_1240), true, iext(uri_rdf_type, X_1239, Y_1240), true)=true))). % 41.10/29.30 tff(c_17518, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, sK8_testcase_premise_fullish_022_List_Member_Access_BNODE_l11, uri_rdf_List), true, true, true), true)=true))). % 41.10/29.30 tff(c_11723, 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))). % 41.10/29.30 tff(c_9785, 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))). % 41.10/29.30 tff(c_12161, 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))). % 41.10/29.30 tff(c_8235, 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))). % 41.10/29.30 tff(c_70387, plain, (![X_1230, Y_1231]: (ifeq(iext(uri_rdf_object, X_1230, Y_1231), true, iext(uri_rdf_object, X_1230, Y_1231), true)=true))). % 41.10/29.30 tff(c_4534, 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))). % 41.10/29.30 tff(c_69958, plain, (![C_1225]: (ifeq(iext(uri_rdfs_subClassOf, C_1225, uri_rdfs_Class), true, iext(uri_rdfs_subClassOf, C_1225, uri_rdfs_Resource), true)=true))). % 41.10/29.30 tff(c_10113, 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))). % 41.10/29.30 tff(c_5513, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL, uri_rdf_Property), true, true, true), true)=true))). % 41.10/29.30 tff(c_10364, 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))). % 41.10/29.30 tff(c_4874, 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))). % 41.10/29.30 tff(c_4722, 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))). % 41.10/29.30 tff(c_12069, 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))). % 41.10/29.30 tff(c_4679, 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))). % 41.10/29.30 tff(c_68978, plain, (![C_1214]: (ifeq(iext(uri_rdfs_subClassOf, C_1214, uri_rdfs_Container), true, iext(uri_rdfs_subClassOf, C_1214, uri_rdfs_Resource), true)=true))). % 41.10/29.30 tff(c_4725, 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))). % 41.10/29.30 tff(c_68696, plain, (![X_1208, Y_1209]: (ifeq(iext(uri_rdf_first, X_1208, Y_1209), true, iext(uri_rdf_first, X_1208, Y_1209), true)=true))). % 41.10/29.30 tff(c_9612, 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))). % 41.10/29.30 tff(c_6072, 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))). % 41.10/29.30 tff(c_5455, 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))). % 41.10/29.30 tff(c_68249, plain, (![P_1203]: (ifeq(iext(uri_rdfs_subPropertyOf, P_1203, uri_rdf__1), true, iext(uri_rdfs_subPropertyOf, P_1203, uri_rdfs_member), true)=true))). % 41.10/29.30 tff(c_68102, plain, (![C_1201]: (ifeq(iext(uri_rdfs_subClassOf, C_1201, uri_rdf_Alt), true, iext(uri_rdfs_subClassOf, C_1201, uri_rdfs_Resource), true)=true))). % 41.10/29.30 tff(c_68075, plain, (![X_1197, Y_1198]: (ifeq(iext(uri_rdf__2, X_1197, Y_1198), true, iext(uri_rdfs_member, X_1197, Y_1198), true)=true))). % 41.10/29.30 tff(c_4815, 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))). % 41.10/29.30 tff(c_67894, plain, (![X_1191, Y_1192]: (ifeq(iext(sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL, X_1191, Y_1192), true, iext(sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL, X_1191, Y_1192), true)=true))). % 41.10/29.30 tff(c_7126, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_skos_memberList, uri_rdf_Property), true, true, true), true)=true))). % 41.10/29.30 tff(c_67622, plain, (![C_1188]: (ifeq(iext(uri_rdfs_subClassOf, C_1188, uri_rdfs_ContainerMembershipProperty), true, iext(uri_rdfs_subClassOf, C_1188, uri_rdfs_Resource), true)=true))). % 41.10/29.30 tff(c_67475, plain, (![C_1186]: (ifeq(iext(uri_rdfs_subClassOf, C_1186, uri_rdfs_Seq), true, iext(uri_rdfs_subClassOf, C_1186, uri_rdfs_Resource), true)=true))). % 41.10/29.30 tff(c_8455, 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))). % 41.10/29.30 tff(c_4581, 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))). % 41.10/29.30 tff(c_67173, plain, (![X_1179, Y_1180]: (ifeq(iext(uri_rdf__3, X_1179, Y_1180), true, iext(uri_rdfs_member, X_1179, Y_1180), true)=true))). % 41.10/29.30 tff(c_10908, 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))). % 41.10/29.31 tff(c_67021, plain, (![X_1174, Y_1175]: (ifeq(iext(uri_rdf__1, X_1174, Y_1175), true, iext(uri_rdf__1, X_1174, Y_1175), true)=true))). % 41.10/29.31 tff(c_4631, 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))). % 41.10/29.31 tff(c_9147, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_skos_memberList, uri_skos_memberList), true, true, true), true)=true))). % 41.10/29.31 tff(c_11145, 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))). % 41.10/29.31 tff(c_11489, 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))). % 41.10/29.31 tff(c_11323, 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))). % 41.10/29.31 tff(c_66310, plain, (![X_1164, Y_1165]: (ifeq(iext(uri_owl_propertyChainAxiom, X_1164, Y_1165), true, iext(uri_owl_propertyChainAxiom, X_1164, Y_1165), true)=true))). % 41.10/29.31 tff(c_66281, plain, (![X_1160, Y_1161]: (ifeq(iext(uri_rdf__2, X_1160, Y_1161), true, iext(uri_rdf__2, X_1160, Y_1161), true)=true))). % 41.10/29.31 tff(c_8035, 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))). % 41.10/29.31 tff(c_4765, 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))). % 41.10/29.31 tff(c_6362, 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))). % 41.10/29.31 tff(c_65209, plain, (![X_1152, Y_1153]: (ifeq(iext(uri_rdfs_subPropertyOf, X_1152, Y_1153), true, iext(uri_rdfs_subPropertyOf, X_1152, Y_1153), true)=true))). % 41.10/29.31 tff(c_6847, 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))). % 41.10/29.31 tff(c_12437, 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))). % 41.10/29.31 tff(c_6933, 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))). % 41.10/29.31 tff(c_63576, plain, (![X_1141, Y_1142]: (ifeq(iext(uri_rdfs_subClassOf, X_1141, Y_1142), true, iext(uri_rdfs_subClassOf, X_1141, Y_1142), true)=true))). % 41.10/29.31 tff(c_10567, 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))). % 41.10/29.31 tff(c_10293, 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))). % 41.10/29.31 tff(c_63258, plain, (![P_1137]: (ifeq(iext(uri_rdfs_subPropertyOf, P_1137, uri_rdf__2), true, iext(uri_rdfs_subPropertyOf, P_1137, uri_rdfs_member), true)=true))). % 41.10/29.31 tff(c_10042, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_owl_propertyChainAxiom, uri_owl_propertyChainAxiom), true, true, true), true)=true))). % 41.10/29.31 tff(c_10746, 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))). % 41.10/29.31 tff(c_7971, 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))). % 41.26/29.31 tff(c_62736, plain, (![C_1132]: (ifeq(iext(uri_rdfs_subClassOf, C_1132, uri_rdfs_Datatype), true, iext(uri_rdfs_subClassOf, C_1132, uri_rdfs_Resource), true)=true))). % 41.26/29.31 tff(c_10975, 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))). % 41.26/29.31 tff(c_4812, 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))). % 41.26/29.31 tff(c_62418, plain, (![X_1125, Y_1126]: (ifeq(iext(uri_skos_memberList, X_1125, Y_1126), true, iext(uri_skos_memberList, X_1125, Y_1126), true)=true))). % 41.26/29.31 tff(c_4484, 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))). % 41.26/29.31 tff(c_12258, 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))). % 41.26/29.31 tff(c_62004, plain, (![C_1120]: (ifeq(iext(uri_rdfs_subClassOf, C_1120, uri_rdf_XMLLiteral), true, iext(uri_rdfs_subClassOf, C_1120, uri_rdfs_Resource), true)=true))). % 41.26/29.31 tff(c_7686, 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))). % 41.26/29.31 tff(c_61541, plain, (![X_1113, Y_1114]: (ifeq(iext(uri_rdfs_isDefinedBy, X_1113, Y_1114), true, iext(uri_rdfs_isDefinedBy, X_1113, Y_1114), true)=true))). % 41.26/29.31 tff(c_4682, 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))). % 41.26/29.31 tff(c_6202, 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))). % 41.26/29.31 tff(c_6694, 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))). % 41.26/29.31 tff(c_60511, plain, (![X_1103, Y_1104]: (ifeq(iext(uri_rdfs_domain, X_1103, Y_1104), true, iext(uri_rdfs_domain, X_1103, Y_1104), true)=true))). % 41.26/29.31 tff(c_60364, plain, (![C_1101]: (ifeq(iext(uri_rdfs_subClassOf, C_1101, uri_rdf_Bag), true, iext(uri_rdfs_subClassOf, C_1101, uri_rdfs_Resource), true)=true))). % 41.26/29.31 tff(c_5172, 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))). % 41.26/29.31 tff(c_59896, plain, (![X_1094, Y_1095]: (ifeq(iext(uri_rdf_subject, X_1094, Y_1095), true, iext(uri_rdf_subject, X_1094, Y_1095), true)=true))). % 41.26/29.31 tff(c_7514, 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))). % 41.26/29.31 tff(c_8369, 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))). % 41.26/29.31 tff(c_59196, plain, (![X_1086, Y_1087]: (ifeq(iext(uri_rdf_rest, X_1086, Y_1087), true, iext(uri_rdf_rest, X_1086, Y_1087), true)=true))). % 41.26/29.31 tff(c_59169, plain, (![X_1082, Y_1083]: (ifeq(iext(uri_rdf__3, X_1082, Y_1083), true, iext(uri_rdf__3, X_1082, Y_1083), true)=true))). % 41.26/29.31 tff(c_4768, 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))). % 41.26/29.31 tff(c_4628, 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))). % 41.26/29.31 tff(c_9320, 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))). % 41.26/29.31 tff(c_10842, 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))). % 41.26/29.31 tff(c_5718, 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))). % 41.26/29.31 tff(c_9540, 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))). % 41.26/29.31 tff(c_57743, plain, (![X_1066, Y_1067]: (ifeq(iext(uri_rdf__1, X_1066, Y_1067), true, iext(uri_rdfs_member, X_1066, Y_1067), true)=true))). % 41.26/29.31 tff(c_4531, 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))). % 41.26/29.31 tff(c_17258, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, sK7_testcase_premise_fullish_022_List_Member_Access_BNODE_l21, uri_rdf_List), true, true, true), true)=true))). % 41.26/29.31 tff(c_6533, 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))). % 41.26/29.31 tff(c_56551, plain, (![X_1052, Y_1053]: (ifeq(iext(uri_rdfs_seeAlso, X_1052, Y_1053), true, iext(uri_rdfs_seeAlso, X_1052, Y_1053), true)=true))). % 41.26/29.32 tff(c_4487, 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))). % 41.26/29.32 tff(c_6772, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL, sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL), true, true, true), true)=true))). % 41.26/29.32 tff(c_55582, plain, (![C_1043]: (ifeq(iext(uri_rdfs_subClassOf, C_1043, uri_rdf_Property), true, iext(uri_rdfs_subClassOf, C_1043, uri_rdfs_Resource), true)=true))). % 41.26/29.32 tff(c_4877, 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))). % 41.26/29.32 tff(c_11074, 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))). % 41.26/29.32 tff(c_55288, plain, (![X_1036, Y_1037]: (ifeq(iext(uri_rdf_value, X_1036, Y_1037), true, iext(uri_rdf_value, X_1036, Y_1037), true)=true))). % 41.26/29.32 tff(c_16097, 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))). % 41.26/29.32 tff(c_17317, 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))). % 41.26/29.32 tff(c_15454, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, uri_skos_OrderedCollection, Y_21), true, true, true), true)=true))). % 41.26/29.32 tff(c_8115, 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_022_List_Member_Access_BNODE_l22), true, true, true), true)=true))). % 41.26/29.32 tff(c_5083, plain, (![P_47, X_138]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, X_138, uri_rdfs_Resource), true, true, true), true)=true))). % 41.26/29.32 tff(c_6441, 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))). % 41.26/29.32 tff(c_6438, 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))). % 41.26/29.32 tff(c_11786, 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))). % 41.26/29.32 tff(c_7767, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_List), true, ifeq(iext(P_18, sK3_testcase_premise_fullish_022_List_Member_Access_BNODE_l32, Y_21), true, true, true), true)=true))). % 41.26/29.32 tff(c_18443, 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))). % 41.26/29.32 tff(c_7296, 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))). % 41.26/29.32 tff(c_16100, 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))). % 41.26/29.32 tff(c_12916, 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_022_List_Member_Access_BNODE_l31), true, true, true), true)=true))). % 41.26/29.32 tff(c_13119, 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_022_List_Member_Access_BNODE_l12), true, true, true), true)=true))). % 41.26/29.32 tff(c_11783, 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))). % 41.26/29.32 tff(c_17314, 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))). % 41.26/29.32 tff(c_13489, 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_022_List_Member_Access_BNODE_l33), true, true, true), true)=true))). % 41.26/29.32 tff(c_27438, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL), true, ifeq(iext(P_47, uri_ex_MyOrderedCollection, sK2_testcase_premise_fullish_022_List_Member_Access_BNODE_l31), true, true, true), true)=true))). % 41.26/29.32 tff(c_18446, 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))). % 41.26/29.32 tff(c_13122, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_List), true, ifeq(iext(P_18, sK5_testcase_premise_fullish_022_List_Member_Access_BNODE_l12, Y_21), true, true, true), true)=true))). % 41.26/29.32 tff(c_7764, 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_022_List_Member_Access_BNODE_l32), true, true, true), true)=true))). % 41.26/29.32 tff(c_7299, 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))). % 41.26/29.32 tff(c_13492, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_List), true, ifeq(iext(P_18, sK1_testcase_premise_fullish_022_List_Member_Access_BNODE_l33, Y_21), true, true, true), true)=true))). % 41.26/29.32 tff(c_8118, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_List), true, ifeq(iext(P_18, sK4_testcase_premise_fullish_022_List_Member_Access_BNODE_l22, Y_21), true, true, true), true)=true))). % 41.26/29.32 tff(c_12919, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_List), true, ifeq(iext(P_18, sK2_testcase_premise_fullish_022_List_Member_Access_BNODE_l31, Y_21), true, true, true), true)=true))). % 41.26/29.32 tff(c_15451, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, uri_skos_OrderedCollection), true, true, true), true)=true))). % 41.26/29.32 tff(c_4391, 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))). % 41.26/29.32 tff(c_3885, 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))). % 41.26/29.32 tff(c_3923, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_skos_OrderedCollection), true, ifeq(iext(P_28, X_30, uri_ex_MyOrderedCollection), true, true, true), true)=true))). % 41.26/29.32 tff(c_3960, 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))). % 41.26/29.32 tff(c_16936, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_List), true, ifeq(iext(P_18, sK7_testcase_premise_fullish_022_List_Member_Access_BNODE_l21, Y_21), true, true, true), true)=true))). % 41.26/29.32 tff(c_4048, 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))). % 41.26/29.32 tff(c_4177, 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))). % 41.26/29.32 tff(c_4180, 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))). % 41.26/29.32 tff(c_3926, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_skos_OrderedCollection), true, ifeq(iext(P_18, uri_ex_MyOrderedCollection, Y_21), true, true, true), true)=true))). % 41.26/29.32 tff(c_4433, 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))). % 41.26/29.32 tff(c_4089, 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))). % 41.26/29.32 tff(c_4003, 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))). % 41.26/29.32 tff(c_4224, 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))). % 41.26/29.32 tff(c_3882, 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))). % 41.26/29.32 tff(c_3841, 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))). % 41.26/29.32 tff(c_4302, 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))). % 41.26/29.32 tff(c_3797, 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))). % 41.26/29.32 tff(c_4342, 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))). % 41.26/29.32 tff(c_4430, 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))). % 41.26/29.32 tff(c_4137, 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))). % 41.26/29.32 tff(c_16973, 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_022_List_Member_Access_BNODE_l11), true, true, true), true)=true))). % 41.26/29.32 tff(c_16933, 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_022_List_Member_Access_BNODE_l21), true, true, true), true)=true))). % 41.26/29.32 tff(c_4221, 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))). % 41.26/29.32 tff(c_3963, 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))). % 41.26/29.32 tff(c_16976, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_List), true, ifeq(iext(P_18, sK8_testcase_premise_fullish_022_List_Member_Access_BNODE_l11, Y_21), true, true, true), true)=true))). % 41.26/29.32 tff(c_3800, 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))). % 41.26/29.32 tff(c_4345, 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))). % 41.26/29.32 tff(c_4051, 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))). % 41.26/29.32 tff(c_4000, 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))). % 41.26/29.32 tff(c_4305, 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))). % 41.26/29.32 tff(c_4263, 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))). % 41.26/29.32 tff(c_4260, 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))). % 41.26/29.32 tff(c_3838, 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))). % 41.26/29.33 tff(c_4394, 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))). % 41.26/29.33 tff(c_4086, 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))). % 41.26/29.33 tff(c_4134, 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))). % 41.26/29.33 tff(c_2240, plain, (![P_95, X_97, X_60]: (ifeq(iext(uri_rdfs_range, P_95, uri_rdfs_Resource), true, ifeq(iext(P_95, X_97, X_60), true, true, true), true)=true))). % 41.26/29.33 tff(c_1833, plain, (![P_91, X_60, Y_94]: (ifeq(iext(uri_rdfs_domain, P_91, uri_rdfs_Resource), true, ifeq(iext(P_91, X_60, Y_94), true, true, true), true)=true))). % 41.26/29.33 tff(c_2970, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdf_type, uri_rdfs_Class), true, true, true), true)=true))). % 41.26/29.33 tff(c_3036, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdf_first, uri_rdfs_Resource), true, true, true), true)=true))). % 41.26/29.33 tff(c_2808, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true, true, true), true)=true))). % 41.26/29.33 tff(c_2769, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_rdf_type, uri_rdf_Property), true, true, true), true)=true))). % 41.26/29.33 tff(c_3012, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdf_rest, uri_rdf_List), true, true, true), true)=true))). % 41.26/29.33 tff(c_3099, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_rdf__1, uri_rdf_Property), true, true, true), true)=true))). % 41.26/29.33 tff(c_2910, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdfs_domain, uri_rdf_Property), true, true, true), true)=true))). % 41.26/29.33 tff(c_3111, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_rdf_value, uri_rdf_Property), true, true, true), true)=true))). % 41.26/29.33 tff(c_3018, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdf_predicate, uri_rdfs_Statement), true, true, true), true)=true))). % 41.26/29.33 tff(c_2793, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdf__1, uri_rdfs_Resource), true, true, true), true)=true))). % 41.26/29.33 tff(c_2745, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdf__2, uri_rdfs_Resource), true, true, true), true)=true))). % 41.26/29.33 tff(c_2826, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdf__3, uri_rdfs_Resource), true, true, true), true)=true))). % 41.26/29.33 tff(c_2733, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_rdf__3, uri_rdf_Property), true, true, true), true)=true))). % 41.26/29.33 tff(c_43247, plain, (![P_892]: (ifeq(iext(uri_rdfs_subPropertyOf, P_892, uri_skos_memberList), true, iext(uri_rdfs_subPropertyOf, P_892, sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL), true)=true))). % 41.26/29.33 tff(c_2787, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdf_type, uri_rdfs_Resource), true, true, true), true)=true))). % 41.26/29.33 tff(c_2781, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_rdf_first, uri_rdf_Property), true, true, true), true)=true))). % 41.26/29.33 tff(c_3042, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_rdf__2, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 41.26/29.33 tff(c_3123, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdf_object, uri_rdfs_Statement), true, true, true), true)=true))). % 41.26/29.33 tff(c_42675, plain, (![C_886]: (ifeq(iext(uri_rdfs_subClassOf, C_886, uri_rdf_Alt), true, iext(uri_rdfs_subClassOf, C_886, uri_rdfs_Container), true)=true))). % 41.26/29.33 tff(c_2838, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdf_subject, uri_rdfs_Resource), true, true, true), true)=true))). % 41.26/29.33 tff(c_2982, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdf_value, uri_rdfs_Resource), true, true, true), true)=true))). % 41.26/29.33 tff(c_2820, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdfs_comment, uri_rdfs_Resource), true, true, true), true)=true))). % 41.26/29.33 tff(c_2844, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdfs_subClassOf, uri_rdfs_Class), true, true, true), true)=true))). % 41.26/29.33 tff(c_2964, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdfs_label, uri_rdfs_Literal), true, true, true), true)=true))). % 41.26/29.33 tff(c_2946, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdfs_member, uri_rdfs_Resource), true, true, true), true)=true))). % 41.26/29.33 tff(c_2988, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_subClassOf), true, ifeq(iext(P_102, uri_rdf_Bag, uri_rdfs_Container), true, true, true), true)=true))). % 41.26/29.33 tff(c_3069, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_subClassOf), true, ifeq(iext(P_102, uri_rdfs_Seq, uri_rdfs_Container), true, true, true), true)=true))). % 41.26/29.33 tff(c_2856, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_rdf_XMLLiteral, uri_rdfs_Datatype), true, true, true), true)=true))). % 41.26/29.33 tff(c_2832, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdf_value, uri_rdfs_Resource), true, true, true), true)=true))). % 41.26/29.33 tff(c_2763, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdfs_subClassOf, uri_rdfs_Class), true, true, true), true)=true))). % 41.26/29.33 tff(c_2814, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_rdf_nil, uri_rdf_List), true, true, true), true)=true))). % 41.26/29.33 tff(c_2934, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_rdf_subject, uri_rdf_Property), true, true, true), true)=true))). % 41.26/29.33 tff(c_40953, plain, (![P_871]: (ifeq(iext(uri_rdfs_subPropertyOf, P_871, uri_rdfs_isDefinedBy), true, iext(uri_rdfs_subPropertyOf, P_871, uri_rdfs_seeAlso), true)=true))). % 41.26/29.33 tff(c_2739, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdf_rest, uri_rdf_List), true, true, true), true)=true))). % 41.26/29.33 tff(c_3159, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_rdf_rest, uri_rdf_Property), true, true, true), true)=true))). % 41.26/29.33 tff(c_40672, plain, (![X_865, Y_866]: (ifeq(iext(uri_rdfs_isDefinedBy, X_865, Y_866), true, iext(uri_rdfs_seeAlso, X_865, Y_866), true)=true))). % 41.26/29.33 tff(c_2916, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdf_subject, uri_rdfs_Statement), true, true, true), true)=true))). % 41.26/29.33 tff(c_3165, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_rest), true, ifeq(iext(P_102, sK3_testcase_premise_fullish_022_List_Member_Access_BNODE_l32, sK1_testcase_premise_fullish_022_List_Member_Access_BNODE_l33), true, true, true), true)=true))). % 41.26/29.33 tff(c_3051, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_subPropertyOf), true, ifeq(iext(P_102, uri_skos_memberList, sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL), true, true, true), true)=true))). % 41.26/29.33 tff(c_3153, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdf__2, uri_rdfs_Resource), true, true, true), true)=true))). % 41.26/29.33 tff(c_2775, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_rdf_Property, uri_rdfs_Class), true, true, true), true)=true))). % 41.26/29.33 tff(c_39971, plain, (![C_858]: (ifeq(iext(uri_rdfs_subClassOf, C_858, uri_rdf_Bag), true, iext(uri_rdfs_subClassOf, C_858, uri_rdfs_Container), true)=true))). % 41.26/29.33 tff(c_2868, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdfs_range, uri_rdfs_Class), true, true, true), true)=true))). % 41.26/29.33 tff(c_2976, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdf__1, uri_rdfs_Resource), true, true, true), true)=true))). % 41.26/29.33 tff(c_2850, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdfs_comment, uri_rdfs_Literal), true, true, true), true)=true))). % 41.26/29.33 tff(c_2994, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdfs_seeAlso, uri_rdfs_Resource), true, true, true), true)=true))). % 41.26/29.33 tff(c_2862, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_ex_MyOrderedCollection, uri_skos_OrderedCollection), true, true, true), true)=true))). % 41.26/29.33 tff(c_2952, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_rest), true, ifeq(iext(P_102, sK1_testcase_premise_fullish_022_List_Member_Access_BNODE_l33, uri_rdf_nil), true, true, true), true)=true))). % 41.26/29.33 tff(c_2904, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdfs_seeAlso, uri_rdfs_Resource), true, true, true), true)=true))). % 41.26/29.33 tff(c_3141, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdfs_subPropertyOf, uri_rdf_Property), true, true, true), true)=true))). % 41.26/29.33 tff(c_3129, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_rest), true, ifeq(iext(P_102, sK7_testcase_premise_fullish_022_List_Member_Access_BNODE_l21, sK4_testcase_premise_fullish_022_List_Member_Access_BNODE_l22), true, true, true), true)=true))). % 41.26/29.33 tff(c_3057, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_first), true, ifeq(iext(P_102, sK7_testcase_premise_fullish_022_List_Member_Access_BNODE_l21, sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL), true, true, true), true)=true))). % 41.26/29.33 tff(c_2928, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_subClassOf), true, ifeq(iext(P_102, uri_rdf_Alt, uri_rdfs_Container), true, true, true), true)=true))). % 41.26/29.33 tff(c_2922, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_rest), true, ifeq(iext(P_102, sK4_testcase_premise_fullish_022_List_Member_Access_BNODE_l22, uri_rdf_nil), true, true, true), true)=true))). % 41.26/29.33 tff(c_2898, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdf_first, uri_rdf_List), true, true, true), true)=true))). % 41.26/29.33 tff(c_3105, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_subClassOf), true, ifeq(iext(P_102, uri_rdf_XMLLiteral, uri_rdfs_Literal), true, true, true), true)=true))). % 41.26/29.33 tff(c_2874, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdfs_domain, uri_rdfs_Class), true, true, true), true)=true))). % 41.26/29.33 tff(c_3024, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_first), true, ifeq(iext(P_102, sK4_testcase_premise_fullish_022_List_Member_Access_BNODE_l22, uri_rdf_rest), true, true, true), true)=true))). % 41.26/29.33 tff(c_2886, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_subClassOf), true, ifeq(iext(P_102, uri_rdfs_Datatype, uri_rdfs_Class), true, true, true), true)=true))). % 41.26/29.33 tff(c_2802, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_subPropertyOf), true, ifeq(iext(P_102, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso), true, true, true), true)=true))). % 41.26/29.33 tff(c_37630, plain, (![C_838]: (ifeq(iext(uri_rdfs_subClassOf, C_838, uri_rdf_XMLLiteral), true, iext(uri_rdfs_subClassOf, C_838, uri_rdfs_Literal), true)=true))). % 41.26/29.33 tff(c_37564, plain, (![D_836]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_836), true, icext(D_836, uri_rdfs_member), true)=true))). % 41.26/29.33 tff(c_37364, plain, (![D_833]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_833), true, icext(D_833, uri_rdfs_Resource), true)=true))). % 41.26/29.33 tff(c_3171, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdf__3, uri_rdfs_Resource), true, true, true), true)=true))). % 41.26/29.33 tff(c_37298, plain, (![D_831]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_831), true, icext(D_831, uri_rdfs_range), true)=true))). % 41.26/29.33 tff(c_37232, plain, (![D_829]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_829), true, icext(D_829, uri_owl_propertyChainAxiom), true)=true))). % 41.26/29.34 tff(c_37041, plain, (![D_826]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_826), true, icext(D_826, uri_rdfs_subPropertyOf), true)=true))). % 41.26/29.34 tff(c_2727, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_rdf_object, uri_rdf_Property), true, true, true), true)=true))). % 41.26/29.34 tff(c_36975, plain, (![D_824]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_824), true, icext(D_824, uri_rdfs_subClassOf), true)=true))). % 41.26/29.34 tff(c_36909, plain, (![D_822]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_822), true, icext(D_822, uri_rdfs_isDefinedBy), true)=true))). % 41.26/29.34 tff(c_36709, plain, (![D_819]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_819), true, icext(D_819, uri_rdfs_domain), true)=true))). % 41.26/29.34 tff(c_3075, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdfs_member, uri_rdfs_Resource), true, true, true), true)=true))). % 41.26/29.34 tff(c_36643, plain, (![D_817]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_817), true, icext(D_817, uri_skos_memberList), true)=true))). % 41.26/29.34 tff(c_36577, plain, (![D_815]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_815), true, icext(D_815, sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL), true)=true))). % 41.26/29.34 tff(c_3000, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdfs_label, uri_rdfs_Resource), true, true, true), true)=true))). % 41.26/29.34 tff(c_36372, plain, (![D_812]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_812), true, icext(D_812, uri_rdf_XMLLiteral), true)=true))). % 41.26/29.34 tff(c_36306, plain, (![D_810]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_810), true, icext(D_810, uri_rdf_Bag), true)=true))). % 41.26/29.34 tff(c_36236, plain, (![D_808]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_808), true, icext(D_808, uri_rdfs_Seq), true)=true))). % 41.26/29.34 tff(c_36170, plain, (![D_806]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_806), true, icext(D_806, uri_rdfs_Datatype), true)=true))). % 41.26/29.34 tff(c_36101, plain, (![C_804]: (ifeq(iext(uri_rdfs_subClassOf, C_804, uri_rdfs_Seq), true, iext(uri_rdfs_subClassOf, C_804, uri_rdfs_Container), true)=true))). % 41.26/29.34 tff(c_36036, plain, (![D_802]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_802), true, icext(D_802, uri_rdf_Alt), true)=true))). % 41.26/29.34 tff(c_35942, plain, (![D_800]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_800), true, icext(D_800, uri_rdfs_Class), true)=true))). % 41.26/29.34 tff(c_35876, plain, (![D_798]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_798), true, icext(D_798, uri_rdfs_ContainerMembershipProperty), true)=true))). % 41.26/29.34 tff(c_3189, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_first), true, ifeq(iext(P_102, sK3_testcase_premise_fullish_022_List_Member_Access_BNODE_l32, uri_ex_Y), true, true, true), true)=true))). % 41.26/29.34 tff(c_35684, plain, (![D_795]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_795), true, icext(D_795, uri_rdfs_Literal), true)=true))). % 41.26/29.34 tff(c_35618, plain, (![D_793]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_793), true, icext(D_793, uri_rdfs_Container), true)=true))). % 41.26/29.34 tff(c_35548, plain, (![D_791]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_791), true, icext(D_791, uri_rdfs_comment), true)=true))). % 41.26/29.34 tff(c_35482, plain, (![D_789]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_789), true, icext(D_789, uri_rdfs_Statement), true)=true))). % 41.26/29.34 tff(c_35416, plain, (![D_787]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_787), true, icext(D_787, uri_skos_OrderedCollection), true)=true))). % 41.26/29.34 tff(c_3087, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_first), true, ifeq(iext(P_102, sK1_testcase_premise_fullish_022_List_Member_Access_BNODE_l33, uri_ex_Z), true, true, true), true)=true))). % 41.26/29.34 tff(c_35225, plain, (![D_784]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_784), true, icext(D_784, uri_rdfs_seeAlso), true)=true))). % 41.26/29.34 tff(c_35159, plain, (![D_782]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_782), true, icext(D_782, uri_rdfs_label), true)=true))). % 41.26/29.34 tff(c_35093, plain, (![D_780]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_780), true, icext(D_780, sK1_testcase_premise_fullish_022_List_Member_Access_BNODE_l33), true)=true))). % 41.26/29.34 tff(c_3030, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_owl_propertyChainAxiom), true, ifeq(iext(P_102, uri_skos_member, sK8_testcase_premise_fullish_022_List_Member_Access_BNODE_l11), true, true, true), true)=true))). % 41.26/29.34 tff(c_34902, plain, (![D_777]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_777), true, icext(D_777, sK2_testcase_premise_fullish_022_List_Member_Access_BNODE_l31), true)=true))). % 41.26/29.34 tff(c_34836, plain, (![D_775]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_775), true, icext(D_775, sK4_testcase_premise_fullish_022_List_Member_Access_BNODE_l22), true)=true))). % 41.26/29.34 tff(c_14524, 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))). % 41.26/29.34 tff(c_3117, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_owl_propertyChainAxiom), true, ifeq(iext(P_102, sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL, sK7_testcase_premise_fullish_022_List_Member_Access_BNODE_l21), true, true, true), true)=true))). % 41.26/29.34 tff(c_14474, 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))). % 41.26/29.34 tff(c_18771, 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))). % 41.26/29.34 tff(c_34531, plain, (![D_766]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_766), true, icext(D_766, uri_rdf_predicate), true)=true))). % 41.26/29.34 tff(c_14409, 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))). % 41.26/29.34 tff(c_3006, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_first), true, ifeq(iext(P_102, sK5_testcase_premise_fullish_022_List_Member_Access_BNODE_l12, uri_rdf_first), true, true, true), true)=true))). % 41.26/29.34 tff(c_14318, 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))). % 41.26/29.34 tff(c_14246, 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))). % 41.26/29.34 tff(c_14016, 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))). % 41.26/29.34 tff(c_34229, plain, (![D_757]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_757), true, icext(D_757, sK5_testcase_premise_fullish_022_List_Member_Access_BNODE_l12), true)=true))). % 41.26/29.34 tff(c_15792, plain, (![E_41]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, E_41), true, iext(uri_rdfs_subClassOf, uri_skos_OrderedCollection, E_41), true)=true))). % 41.26/29.34 tff(c_16400, 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))). % 41.26/29.34 tff(c_16466, 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))). % 41.26/29.34 tff(c_2940, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdfs_subPropertyOf, uri_rdf_Property), true, true, true), true)=true))). % 41.26/29.34 tff(c_17648, 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))). % 41.26/29.34 tff(c_33894, plain, (![D_748]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_748), true, icext(D_748, sK3_testcase_premise_fullish_022_List_Member_Access_BNODE_l32), true)=true))). % 41.26/29.34 tff(c_17646, 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))). % 41.26/29.34 tff(c_15794, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_skos_OrderedCollection, uri_rdfs_Resource), true)=true))). % 41.26/29.34 tff(c_15728, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_skos_OrderedCollection, uri_skos_OrderedCollection), true)=true))). % 41.26/29.34 tff(c_3195, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_first), true, ifeq(iext(P_102, sK8_testcase_premise_fullish_022_List_Member_Access_BNODE_l11, sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL), true, true, true), true)=true))). % 41.26/29.34 tff(c_16464, 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))). % 41.26/29.34 tff(c_17930, 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))). % 41.26/29.34 tff(c_33584, plain, (![D_739]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_739), true, icext(D_739, uri_rdf_List), true)=true))). % 41.26/29.34 tff(c_13718, 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))). % 41.26/29.34 tff(c_33514, plain, (![C_736]: (ifeq(iext(uri_rdfs_subClassOf, C_736, uri_rdfs_ContainerMembershipProperty), true, iext(uri_rdfs_subClassOf, C_736, uri_rdf_Property), true)=true))). % 41.26/29.34 tff(c_12870, 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))). % 41.26/29.34 tff(c_13766, 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))). % 41.26/29.34 tff(c_13395, 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))). % 41.26/29.34 tff(c_13934, 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))). % 41.26/29.34 tff(c_13443, 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))). % 41.26/29.34 tff(c_13348, 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))). % 41.26/29.34 tff(c_13840, 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))). % 41.26/29.34 tff(c_13887, 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))). % 41.26/29.34 tff(c_3177, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_rdf__1, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 41.26/29.34 tff(c_12673, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, sK3_testcase_premise_fullish_022_List_Member_Access_BNODE_l32, uri_rdf_List), true)=true))). % 41.26/29.34 tff(c_12726, 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))). % 41.26/29.34 tff(c_13072, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, sK2_testcase_premise_fullish_022_List_Member_Access_BNODE_l31, uri_rdf_List), true)=true))). % 41.26/29.34 tff(c_12821, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, sK4_testcase_premise_fullish_022_List_Member_Access_BNODE_l22, uri_rdf_List), true)=true))). % 41.26/29.34 tff(c_18516, 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))). % 41.26/29.34 tff(c_12555, 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))). % 41.26/29.34 tff(c_13181, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, sK5_testcase_premise_fullish_022_List_Member_Access_BNODE_l12, uri_rdf_List), true)=true))). % 41.26/29.34 tff(c_15663, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_skos_OrderedCollection, uri_rdfs_Class), true)=true))). % 41.26/29.34 tff(c_2880, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true, true, true), true)=true))). % 41.26/29.34 tff(c_17584, 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))). % 41.26/29.34 tff(c_13551, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, sK1_testcase_premise_fullish_022_List_Member_Access_BNODE_l33, uri_rdf_List), true)=true))). % 41.26/29.34 tff(c_16336, 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))). % 41.26/29.34 tff(c_32898, plain, (![D_713]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_713), true, icext(D_713, uri_rdf_type), true)=true))). % 41.26/29.34 tff(c_8066, 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))). % 41.26/29.34 tff(c_6802, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL, sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL), true)=true))). % 41.26/29.34 tff(c_7718, 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))). % 41.26/29.34 tff(c_17537, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, sK8_testcase_premise_fullish_022_List_Member_Access_BNODE_l11, uri_rdf_List), true)=true))). % 41.26/29.35 tff(c_12285, 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))). % 41.26/29.35 tff(c_32700, plain, (![D_705]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_705), true, icext(D_705, uri_rdf__2), true)=true))). % 41.26/29.35 tff(c_6560, 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))). % 41.26/29.35 tff(c_10778, 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))). % 41.26/29.35 tff(c_12096, 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))). % 41.26/29.35 tff(c_2751, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdfs_range, uri_rdf_Property), true, true, true), true)=true))). % 41.26/29.35 tff(c_11459, 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))). % 41.26/29.35 tff(c_5937, 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))). % 41.26/29.35 tff(c_10138, 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))). % 41.26/29.35 tff(c_9637, 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))). % 41.26/29.35 tff(c_12283, 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))). % 41.26/29.35 tff(c_7717, 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))). % 41.26/29.35 tff(c_6958, 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))). % 41.26/29.35 tff(c_3147, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdf_predicate, uri_rdfs_Resource), true, true, true), true)=true))). % 41.26/29.35 tff(c_6874, 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))). % 41.26/29.35 tff(c_8480, 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))). % 41.26/29.35 tff(c_11105, 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))). % 41.26/29.35 tff(c_6721, 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))). % 41.26/29.35 tff(c_11172, 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))). % 41.26/29.35 tff(c_12468, 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))). % 41.26/29.35 tff(c_10939, 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))). % 41.26/29.35 tff(c_10391, 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))). % 41.26/29.35 tff(c_5482, 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))). % 41.26/29.35 tff(c_31955, plain, (![D_679]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_679), true, icext(D_679, uri_rdf_nil), true)=true))). % 41.26/29.35 tff(c_6232, 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))). % 41.26/29.35 tff(c_5857, 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))). % 41.26/29.35 tff(c_2892, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_subClassOf), true, ifeq(iext(P_102, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property), true, true, true), true)=true))). % 41.26/29.35 tff(c_9347, 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))). % 41.26/29.35 tff(c_10777, 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))). % 41.26/29.35 tff(c_17277, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, sK7_testcase_premise_fullish_022_List_Member_Access_BNODE_l21, uri_rdf_List), true)=true))). % 41.26/29.35 tff(c_8260, 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))). % 41.26/29.35 tff(c_10389, 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))). % 41.40/29.35 tff(c_9177, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_skos_memberList, uri_skos_memberList), true)=true))). % 41.40/29.35 tff(c_11006, 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))). % 41.40/29.35 tff(c_3093, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_rest), true, ifeq(iext(P_102, sK5_testcase_premise_fullish_022_List_Member_Access_BNODE_l12, uri_rdf_nil), true, true, true), true)=true))). % 41.40/29.35 tff(c_5748, 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))). % 41.40/29.35 tff(c_11748, 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))). % 41.40/29.35 tff(c_31352, plain, (![D_661]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_661), true, icext(D_661, uri_rdf_Property), true)=true))). % 41.40/29.35 tff(c_11354, 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))). % 41.40/29.35 tff(c_5199, 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))). % 41.40/29.35 tff(c_3135, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_skos_memberList), true, ifeq(iext(P_102, uri_ex_MyOrderedCollection, sK2_testcase_premise_fullish_022_List_Member_Access_BNODE_l31), true, true, true), true)=true))). % 41.40/29.35 tff(c_10324, 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))). % 41.40/29.35 tff(c_8812, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_owl_propertyChainAxiom, uri_rdf_Property), true)=true))). % 41.40/29.35 tff(c_5197, 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))). % 41.40/29.35 tff(c_9115, 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))). % 41.40/29.35 tff(c_3183, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_rest), true, ifeq(iext(P_102, sK2_testcase_premise_fullish_022_List_Member_Access_BNODE_l31, sK3_testcase_premise_fullish_022_List_Member_Access_BNODE_l32), true, true, true), true)=true))). % 41.40/29.35 tff(c_11170, 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))). % 41.40/29.35 tff(c_6103, 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))). % 41.40/29.35 tff(c_6960, 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))). % 41.40/29.35 tff(c_11514, 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))). % 41.40/29.35 tff(c_8400, 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))). % 41.40/29.35 tff(c_10592, 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))). % 41.40/29.35 tff(c_3063, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_rest), true, ifeq(iext(P_102, sK8_testcase_premise_fullish_022_List_Member_Access_BNODE_l11, sK5_testcase_premise_fullish_022_List_Member_Access_BNODE_l12), true, true, true), true)=true))). % 41.40/29.35 tff(c_5538, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL, uri_rdf_Property), true)=true))). % 41.40/29.35 tff(c_10073, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_owl_propertyChainAxiom, uri_owl_propertyChainAxiom), true)=true))). % 41.40/29.35 tff(c_30429, plain, (![D_634]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_634), true, icext(D_634, uri_rdf_rest), true)=true))). % 41.40/29.35 tff(c_8683, 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))). % 41.40/29.35 tff(c_30371, plain, (![X_629, Y_630]: (ifeq(iext(uri_skos_memberList, X_629, Y_630), true, iext(sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL, X_629, Y_630), true)=true))). % 41.40/29.35 tff(c_5859, 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))). % 41.40/29.35 tff(c_6102, 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))). % 41.40/29.35 tff(c_9874, 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))). % 41.40/29.35 tff(c_6558, 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))). % 41.40/29.35 tff(c_9816, 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))). % 41.40/29.35 tff(c_3081, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_rdf__3, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 41.40/29.35 tff(c_7151, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_skos_memberList, uri_rdf_Property), true)=true))). % 41.40/29.35 tff(c_9571, 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))). % 41.40/29.35 tff(c_7541, 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))). % 41.40/29.35 tff(c_29937, plain, (![D_615]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_615), true, icext(D_615, uri_rdf_value), true)=true))). % 41.40/29.35 tff(c_9639, 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))). % 41.40/29.35 tff(c_29866, plain, (![C_612]: (ifeq(iext(uri_rdfs_subClassOf, C_612, uri_rdfs_Datatype), true, iext(uri_rdfs_subClassOf, C_612, uri_rdfs_Class), true)=true))). % 41.40/29.35 tff(c_11750, 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))). % 41.40/29.35 tff(c_8002, 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))). % 41.40/29.35 tff(c_6389, 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))). % 41.40/29.35 tff(c_29734, plain, (![D_607]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_607), true, icext(D_607, uri_rdf__1), true)=true))). % 41.40/29.35 tff(c_10873, 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))). % 41.40/29.35 tff(c_12192, 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))). % 41.40/29.35 tff(c_2958, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_first), true, ifeq(iext(P_102, sK2_testcase_premise_fullish_022_List_Member_Access_BNODE_l31, uri_ex_X), true, true, true), true)=true))). % 41.40/29.35 tff(c_10140, 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))). % 41.40/29.35 tff(c_2757, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_rdf__2, uri_rdf_Property), true, true, true), true)=true))). % 41.40/29.35 tff(c_27452, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL, Q_48), true, iext(Q_48, uri_ex_MyOrderedCollection, sK2_testcase_premise_fullish_022_List_Member_Access_BNODE_l31), true)=true))). % 41.40/29.35 tff(c_29060, plain, (![D_589]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_589), true, icext(D_589, uri_rdf__3), true)=true))). % 41.40/29.35 tff(c_5103, plain, (![Q_48, X_138]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, X_138, uri_rdfs_Resource), true)=true))). % 41.40/29.35 tff(c_3209, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_rdf_first, uri_rdf_Property), true)=true))). % 41.40/29.35 tff(c_3213, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true)=true))). % 41.40/29.35 tff(c_3217, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdf_value, uri_rdfs_Resource), true)=true))). % 41.40/29.35 tff(c_3228, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdf_first, uri_rdf_List), true)=true))). % 41.40/29.35 tff(c_3344, plain, (![E_107]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_107), true, iext(uri_rdfs_subClassOf, uri_rdf_Alt, E_107), true)=true))). % 41.40/29.35 tff(c_3254, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_first, Q_103), true, iext(Q_103, sK7_testcase_premise_fullish_022_List_Member_Access_BNODE_l21, sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL), true)=true))). % 41.40/29.35 tff(c_28713, plain, (![D_579]: (ifeq(iext(uri_rdfs_subClassOf, uri_skos_OrderedCollection, D_579), true, icext(D_579, uri_ex_MyOrderedCollection), true)=true))). % 41.40/29.35 tff(c_3248, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdf_predicate, uri_rdfs_Statement), true)=true))). % 41.40/29.35 tff(c_3260, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_rest, Q_103), true, iext(Q_103, sK5_testcase_premise_fullish_022_List_Member_Access_BNODE_l12, uri_rdf_nil), true)=true))). % 41.40/29.35 tff(c_3230, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdfs_domain, uri_rdf_Property), true)=true))). % 41.40/29.35 tff(c_3255, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_rest, Q_103), true, iext(Q_103, sK8_testcase_premise_fullish_022_List_Member_Access_BNODE_l11, sK5_testcase_premise_fullish_022_List_Member_Access_BNODE_l12), true)=true))). % 41.40/29.35 tff(c_3271, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_rdf_rest, uri_rdf_Property), true)=true))). % 41.40/29.35 tff(c_3347, plain, (![E_107]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Literal, E_107), true, iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, E_107), true)=true))). % 41.40/29.35 tff(c_3241, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdf__1, uri_rdfs_Resource), true)=true))). % 41.40/29.35 tff(c_28507, plain, (![D_570]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_570), true, icext(D_570, sK7_testcase_premise_fullish_022_List_Member_Access_BNODE_l21), true)=true))). % 41.40/29.36 tff(c_3251, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdf_first, uri_rdfs_Resource), true)=true))). % 41.40/29.36 tff(c_3269, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdf_predicate, uri_rdfs_Resource), true)=true))). % 41.40/29.36 tff(c_3218, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdf_subject, uri_rdfs_Resource), true)=true))). % 41.40/29.36 tff(c_3220, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdfs_comment, uri_rdfs_Literal), true)=true))). % 41.40/29.36 tff(c_3200, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_rdf_object, uri_rdf_Property), true)=true))). % 41.40/29.36 tff(c_3224, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdfs_domain, uri_rdfs_Class), true)=true))). % 41.40/29.36 tff(c_3264, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_owl_propertyChainAxiom, Q_103), true, iext(Q_103, sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL, sK7_testcase_premise_fullish_022_List_Member_Access_BNODE_l21), true)=true))). % 41.40/29.36 tff(c_3211, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdf__1, uri_rdfs_Resource), true)=true))). % 41.40/29.36 tff(c_3221, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_rdf_XMLLiteral, uri_rdfs_Datatype), true)=true))). % 41.40/29.36 tff(c_3222, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_ex_MyOrderedCollection, uri_skos_OrderedCollection), true)=true))). % 41.40/29.36 tff(c_3268, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdfs_subPropertyOf, uri_rdf_Property), true)=true))). % 41.40/29.36 tff(c_3262, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_103), true, iext(Q_103, uri_rdf_XMLLiteral, uri_rdfs_Literal), true)=true))). % 41.40/29.36 tff(c_2673, plain, (![R_100]: (ifeq(iext(uri_rdfs_subPropertyOf, sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL, R_100), true, iext(uri_rdfs_subPropertyOf, uri_skos_memberList, R_100), true)=true))). % 41.40/29.36 tff(c_3215, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdfs_comment, uri_rdfs_Resource), true)=true))). % 41.40/29.36 tff(c_3274, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_rdf__1, uri_rdfs_ContainerMembershipProperty), true)=true))). % 41.40/29.36 tff(c_3247, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdf_rest, uri_rdf_List), true)=true))). % 41.40/29.36 tff(c_3239, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdfs_label, uri_rdfs_Literal), true)=true))). % 41.40/29.36 tff(c_3270, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdf__2, uri_rdfs_Resource), true)=true))). % 41.40/29.36 tff(c_3263, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_rdf_value, uri_rdf_Property), true)=true))). % 41.40/29.36 tff(c_3249, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_first, Q_103), true, iext(Q_103, sK4_testcase_premise_fullish_022_List_Member_Access_BNODE_l22, uri_rdf_rest), true)=true))). % 41.40/29.36 tff(c_3259, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_first, Q_103), true, iext(Q_103, sK1_testcase_premise_fullish_022_List_Member_Access_BNODE_l33, uri_ex_Z), true)=true))). % 41.40/29.36 tff(c_3265, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdf_object, uri_rdfs_Statement), true)=true))). % 41.40/29.36 tff(c_3256, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_103), true, iext(Q_103, uri_rdfs_Seq, uri_rdfs_Container), true)=true))). % 41.40/29.36 tff(c_3203, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdf__2, uri_rdfs_Resource), true)=true))). % 41.40/29.36 tff(c_3223, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdfs_range, uri_rdfs_Class), true)=true))). % 41.40/29.36 tff(c_27991, plain, (![D_543]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_543), true, icext(D_543, sK8_testcase_premise_fullish_022_List_Member_Access_BNODE_l11), true)=true))). % 41.40/29.36 tff(c_3277, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_first, Q_103), true, iext(Q_103, sK8_testcase_premise_fullish_022_List_Member_Access_BNODE_l11, sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL), true)=true))). % 41.40/29.36 tff(c_3208, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_rdf_Property, uri_rdfs_Class), true)=true))). % 41.40/29.36 tff(c_3276, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_first, Q_103), true, iext(Q_103, sK3_testcase_premise_fullish_022_List_Member_Access_BNODE_l32, uri_ex_Y), true)=true))). % 41.40/29.36 tff(c_2672, plain, (![R_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_seeAlso, R_100), true, iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, R_100), true)=true))). % 41.40/29.36 tff(c_3243, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_103), true, iext(Q_103, uri_rdf_Bag, uri_rdfs_Container), true)=true))). % 41.40/29.36 tff(c_3210, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdf_type, uri_rdfs_Resource), true)=true))). % 41.40/29.36 tff(c_3252, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_rdf__2, uri_rdfs_ContainerMembershipProperty), true)=true))). % 41.40/29.36 tff(c_27811, plain, (![D_534]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_534), true, icext(D_534, uri_rdf_object), true)=true))). % 41.40/29.36 tff(c_3253, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_103), true, iext(Q_103, uri_skos_memberList, sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL), true)=true))). % 41.40/29.36 tff(c_3225, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true)=true))). % 41.40/29.36 tff(c_3242, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdf_value, uri_rdfs_Resource), true)=true))). % 41.40/29.36 tff(c_3202, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdf_rest, uri_rdf_List), true)=true))). % 41.40/29.36 tff(c_3257, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdfs_member, uri_rdfs_Resource), true)=true))). % 41.40/29.36 tff(c_3234, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_rdf_subject, uri_rdf_Property), true)=true))). % 41.40/29.36 tff(c_3237, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_rest, Q_103), true, iext(Q_103, sK1_testcase_premise_fullish_022_List_Member_Access_BNODE_l33, uri_rdf_nil), true)=true))). % 41.40/29.36 tff(c_27593, plain, (![D_525]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_525), true, icext(D_525, uri_rdf__3), true)=true))). % 41.40/29.36 tff(c_3226, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_103), true, iext(Q_103, uri_rdfs_Datatype, uri_rdfs_Class), true)=true))). % 41.40/29.36 tff(c_3258, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_rdf__3, uri_rdfs_ContainerMembershipProperty), true)=true))). % 41.40/29.36 tff(c_3227, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_103), true, iext(Q_103, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property), true)=true))). % 41.40/29.36 tff(c_3214, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_rdf_nil, uri_rdf_List), true)=true))). % 41.40/29.36 tff(c_3273, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdf__3, uri_rdfs_Resource), true)=true))). % 41.40/29.36 tff(c_27454, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL, C_19), true, icext(C_19, uri_ex_MyOrderedCollection), true)=true))). % 41.40/29.36 tff(c_27453, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL, C_29), true, icext(C_29, sK2_testcase_premise_fullish_022_List_Member_Access_BNODE_l31), true)=true))). % 41.40/29.36 tff(c_27418, plain, (iext(sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL, uri_ex_MyOrderedCollection, sK2_testcase_premise_fullish_022_List_Member_Access_BNODE_l31)=true)). % 41.40/29.36 tff(c_3267, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_skos_memberList, Q_103), true, iext(Q_103, uri_ex_MyOrderedCollection, sK2_testcase_premise_fullish_022_List_Member_Access_BNODE_l31), true)=true))). % 41.40/29.36 tff(c_3201, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_rdf__3, uri_rdf_Property), true)=true))). % 41.40/29.36 tff(c_3342, plain, (![E_107]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, E_107), true, iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, E_107), true)=true))). % 41.40/29.36 tff(c_3261, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_rdf__1, uri_rdf_Property), true)=true))). % 41.40/29.36 tff(c_3235, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdfs_subPropertyOf, uri_rdf_Property), true)=true))). % 41.40/29.36 tff(c_14477, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_label), true)=true))). % 41.40/29.36 tff(c_14478, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_label), true)=true))). % 41.40/29.36 tff(c_18774, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_predicate), true)=true))). % 41.40/29.36 tff(c_18775, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_predicate), true)=true))). % 41.40/29.36 tff(c_14412, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_comment), true)=true))). % 41.40/29.36 tff(c_3236, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdfs_member, uri_rdfs_Resource), true)=true))). % 41.40/29.36 tff(c_14413, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_comment), true)=true))). % 41.40/29.36 tff(c_14250, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_member), true)=true))). % 41.40/29.36 tff(c_14320, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Resource), true)=true))). % 41.40/29.36 tff(c_15796, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_skos_OrderedCollection), true)=true))). % 41.40/29.36 tff(c_3240, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdf_type, uri_rdfs_Class), true)=true))). % 41.40/29.36 tff(c_17931, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Statement), true)=true))). % 41.40/29.36 tff(c_26949, plain, (![D_499]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_499), true, icext(D_499, uri_rdf__2), true)=true))). % 41.40/29.36 tff(c_17932, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Statement), true)=true))). % 41.40/29.36 tff(c_3205, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_rdf__2, uri_rdf_Property), true)=true))). % 41.40/29.36 tff(c_16402, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdf_List), true)=true))). % 41.40/29.36 tff(c_15729, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_skos_OrderedCollection), true)=true))). % 41.40/29.36 tff(c_26790, plain, (![D_493]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_493), true, icext(D_493, uri_rdf_subject), true)=true))). % 41.40/29.36 tff(c_16401, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_List), true)=true))). % 41.40/29.36 tff(c_3245, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdfs_label, uri_rdfs_Resource), true)=true))). % 41.40/29.36 tff(c_26666, plain, (![D_489]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_489), true, icext(D_489, uri_rdf__1), true)=true))). % 41.40/29.36 tff(c_3212, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_103), true, iext(Q_103, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso), true)=true))). % 41.40/29.36 tff(c_26563, plain, (![D_486]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, D_486), true, icext(D_486, uri_rdf_XMLLiteral), true)=true))). % 41.40/29.36 tff(c_3204, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdfs_range, uri_rdf_Property), true)=true))). % 41.40/29.36 tff(c_3250, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_owl_propertyChainAxiom, Q_103), true, iext(Q_103, uri_skos_member, sK8_testcase_premise_fullish_022_List_Member_Access_BNODE_l11), true)=true))). % 41.40/29.36 tff(c_26448, plain, (![D_482]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_482), true, icext(D_482, uri_rdf_first), true)=true))). % 41.40/29.36 tff(c_3231, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdf_subject, uri_rdfs_Statement), true)=true))). % 41.40/29.36 tff(c_3246, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_first, Q_103), true, iext(Q_103, sK5_testcase_premise_fullish_022_List_Member_Access_BNODE_l12, uri_rdf_first), true)=true))). % 41.40/29.36 tff(c_10876, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_range), true)=true))). % 41.40/29.36 tff(c_7542, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_Bag), true)=true))). % 41.40/29.36 tff(c_8005, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_object), true)=true))). % 41.40/29.36 tff(c_8004, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_object), true)=true))). % 41.40/29.36 tff(c_9574, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_isDefinedBy), true)=true))). % 41.40/29.36 tff(c_3275, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_rest, Q_103), true, iext(Q_103, sK2_testcase_premise_fullish_022_List_Member_Access_BNODE_l31, sK3_testcase_premise_fullish_022_List_Member_Access_BNODE_l32), true)=true))). % 41.40/29.36 tff(c_8069, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_value), true)=true))). % 41.40/29.36 tff(c_9348, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_Alt), true)=true))). % 41.40/29.36 tff(c_9819, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__2), true)=true))). % 41.40/29.36 tff(c_25979, plain, (![C_88, X_60]: (ifeq(icext(C_88, X_60), true, true, true)=true))). % 41.40/29.36 tff(c_10327, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_domain), true)=true))). % 41.40/29.36 tff(c_8070, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_value), true)=true))). % 41.40/29.36 tff(c_3232, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_rest, Q_103), true, iext(Q_103, sK4_testcase_premise_fullish_022_List_Member_Access_BNODE_l22, uri_rdf_nil), true)=true))). % 41.40/29.36 tff(c_7721, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__1), true)=true))). % 41.40/29.36 tff(c_25418, plain, (![D_461, X_462]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, D_461), true, icext(D_461, X_462), true)=true))). % 41.40/29.36 tff(c_11460, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_XMLLiteral), true)=true))). % 41.40/29.36 tff(c_3345, plain, (![E_107]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_107), true, iext(uri_rdfs_subClassOf, uri_rdf_Bag, E_107), true)=true))). % 41.40/29.36 tff(c_5750, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_subClassOf), true)=true))). % 41.40/29.36 tff(c_10328, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_domain), true)=true))). % 41.40/29.36 tff(c_24989, plain, (![X_453, Y_454]: (ifeq(iext(uri_rdfs_domain, X_453, Y_454), true, icext(uri_rdfs_Class, Y_454), true)=true))). % 41.40/29.36 tff(c_5861, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Literal), true)=true))). % 41.40/29.36 tff(c_6722, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Seq), true)=true))). % 41.40/29.36 tff(c_3266, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_rest, Q_103), true, iext(Q_103, sK7_testcase_premise_fullish_022_List_Member_Access_BNODE_l21, sK4_testcase_premise_fullish_022_List_Member_Access_BNODE_l22), true)=true))). % 41.40/29.36 tff(c_6235, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_rest), true)=true))). % 41.40/29.36 tff(c_24155, plain, (![X_444, Y_445]: (ifeq(iext(uri_rdfs_subClassOf, X_444, Y_445), true, icext(uri_rdfs_Class, X_444), true)=true))). % 41.40/29.37 tff(c_3207, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_rdf_type, uri_rdf_Property), true)=true))). % 41.40/29.37 tff(c_10781, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__3), true)=true))). % 41.40/29.37 tff(c_24064, plain, (![X_438, Y_439]: (ifeq(iext(uri_rdf_subject, X_438, Y_439), true, icext(uri_rdfs_Statement, X_438), true)=true))). % 41.40/29.37 tff(c_3219, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdfs_subClassOf, uri_rdfs_Class), true)=true))). % 41.40/29.37 tff(c_11358, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_first), true)=true))). % 41.40/29.37 tff(c_23639, plain, (![X_432, Y_433]: (ifeq(iext(uri_rdfs_range, X_432, Y_433), true, icext(uri_rdf_Property, X_432), true)=true))). % 41.40/29.37 tff(c_10877, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_range), true)=true))). % 41.40/29.37 tff(c_11010, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_subject), true)=true))). % 41.40/29.37 tff(c_3206, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdfs_subClassOf, uri_rdfs_Class), true)=true))). % 41.40/29.37 tff(c_5484, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Container), true)=true))). % 41.40/29.37 tff(c_10393, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdf_Property), true)=true))). % 41.40/29.37 tff(c_23486, plain, (![X_423, Y_424]: (ifeq(iext(uri_rdfs_label, X_423, Y_424), true, icext(uri_rdfs_Literal, Y_424), true)=true))). % 41.40/29.37 tff(c_6805, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL), true)=true))). % 41.40/29.37 tff(c_5751, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_subClassOf), true)=true))). % 41.40/29.37 tff(c_3343, plain, (![E_107]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, E_107), true, iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, E_107), true)=true))). % 41.40/29.37 tff(c_11357, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_first), true)=true))). % 41.40/29.37 tff(c_22973, plain, (![X_415, Y_416]: (ifeq(iext(uri_rdfs_domain, X_415, Y_416), true, icext(uri_rdf_Property, X_415), true)=true))). % 41.40/29.37 tff(c_12097, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Datatype), true)=true))). % 41.40/29.37 tff(c_3229, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdfs_seeAlso, uri_rdfs_Resource), true)=true))). % 41.40/29.37 tff(c_9116, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_ContainerMembershipProperty), true)=true))). % 41.40/29.37 tff(c_22863, plain, (![X_408, Y_409]: (ifeq(iext(uri_rdf_predicate, X_408, Y_409), true, icext(uri_rdfs_Statement, X_408), true)=true))). % 41.40/29.37 tff(c_9820, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__2), true)=true))). % 41.40/29.37 tff(c_3238, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_first, Q_103), true, iext(Q_103, sK2_testcase_premise_fullish_022_List_Member_Access_BNODE_l31, uri_ex_X), true)=true))). % 41.40/29.37 tff(c_22650, plain, (![X_402, Y_403]: (ifeq(iext(uri_rdf_rest, X_402, Y_403), true, icext(uri_rdf_List, X_402), true)=true))). % 41.40/29.37 tff(c_8403, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__1), true)=true))). % 41.40/29.37 tff(c_3346, plain, (![E_107]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_107), true, iext(uri_rdfs_subClassOf, uri_rdfs_Seq, E_107), true)=true))). % 41.40/29.37 tff(c_10942, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__3), true)=true))). % 41.40/29.37 tff(c_10076, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_owl_propertyChainAxiom), true)=true))). % 41.40/29.37 tff(c_22201, plain, (![X_394, Y_395]: (ifeq(iext(uri_rdfs_range, X_394, Y_395), true, icext(uri_rdfs_Class, Y_395), true)=true))). % 41.40/29.37 tff(c_10077, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_owl_propertyChainAxiom), true)=true))). % 41.40/29.37 tff(c_12196, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_subPropertyOf), true)=true))). % 41.40/29.37 tff(c_3233, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_103), true, iext(Q_103, uri_rdf_Alt, uri_rdfs_Container), true)=true))). % 41.40/29.37 tff(c_11752, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Class), true)=true))). % 41.40/29.37 tff(c_22072, plain, (![X_386, Y_387]: (ifeq(iext(uri_rdf_object, X_386, Y_387), true, icext(uri_rdfs_Statement, X_386), true)=true))). % 41.40/29.37 tff(c_11109, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_seeAlso), true)=true))). % 41.40/29.37 tff(c_11009, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_subject), true)=true))). % 41.40/29.37 tff(c_3244, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdfs_seeAlso, uri_rdfs_Resource), true)=true))). % 41.40/29.37 tff(c_12195, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_subPropertyOf), true)=true))). % 41.40/29.37 tff(c_6234, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_rest), true)=true))). % 41.40/29.37 tff(c_21790, plain, (![X_377, Y_378]: (ifeq(iext(uri_rdf_rest, X_377, Y_378), true, icext(uri_rdf_List, Y_378), true)=true))). % 41.40/29.37 tff(c_6561, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Resource), true)=true))). % 41.40/29.37 tff(c_7720, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_member), true)=true))). % 41.40/29.37 tff(c_12471, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_type), true)=true))). % 41.40/29.37 tff(c_3216, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdf__3, uri_rdfs_Resource), true)=true))). % 41.40/29.37 tff(c_21252, plain, (![X_369, Y_370]: (ifeq(iext(uri_rdfs_subPropertyOf, X_369, Y_370), true, icext(uri_rdf_Property, Y_370), true)=true))). % 41.40/29.37 tff(c_12472, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_type), true)=true))). % 41.40/29.37 tff(c_9179, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_skos_memberList), true)=true))). % 41.40/29.37 tff(c_3272, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_rest, Q_103), true, iext(Q_103, sK3_testcase_premise_fullish_022_List_Member_Access_BNODE_l32, sK1_testcase_premise_fullish_022_List_Member_Access_BNODE_l33), true)=true))). % 41.40/29.37 tff(c_5104, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_29), true, icext(C_29, uri_rdfs_Resource), true)=true))). % 41.40/29.37 tff(c_5105, plain, (![C_19, X_138]: (ifeq(iext(uri_rdfs_domain, uri_rdf_type, C_19), true, icext(C_19, X_138), true)=true))). % 41.40/29.37 tff(c_20874, plain, (![X_358, Y_359]: (ifeq(iext(uri_rdfs_comment, X_358, Y_359), true, icext(uri_rdfs_Literal, Y_359), true)=true))). % 41.40/29.37 tff(c_2605, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_skos_memberList, C_96), true, icext(C_96, sK2_testcase_premise_fullish_022_List_Member_Access_BNODE_l31), true)=true))). % 41.40/29.37 tff(c_2204, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_skos_memberList, C_92), true, icext(C_92, uri_ex_MyOrderedCollection), true)=true))). % 41.40/29.37 tff(c_2186, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdf_first, C_92), true, icext(C_92, sK4_testcase_premise_fullish_022_List_Member_Access_BNODE_l22), true)=true))). % 41.40/29.37 tff(c_2176, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdf_type), true)=true))). % 41.40/29.37 tff(c_2173, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdf_rest, C_92), true, icext(C_92, sK1_testcase_premise_fullish_022_List_Member_Access_BNODE_l33), true)=true))). % 41.40/29.37 tff(c_2185, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdf_predicate), true)=true))). % 41.40/29.37 tff(c_2175, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdfs_label), true)=true))). % 41.40/29.37 tff(c_2191, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdf_first, C_92), true, icext(C_92, sK7_testcase_premise_fullish_022_List_Member_Access_BNODE_l21), true)=true))). % 41.40/29.37 tff(c_2159, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdfs_isDefinedBy), true)=true))). % 41.40/29.37 tff(c_2203, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdf_rest, C_92), true, icext(C_92, sK7_testcase_premise_fullish_022_List_Member_Access_BNODE_l21), true)=true))). % 41.40/29.37 tff(c_2196, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdf_first, C_92), true, icext(C_92, sK1_testcase_premise_fullish_022_List_Member_Access_BNODE_l33), true)=true))). % 41.40/29.37 tff(c_20059, plain, (![X_338, Y_339]: (ifeq(iext(uri_rdf_type, X_338, Y_339), true, icext(uri_rdfs_Class, Y_339), true)=true))). % 41.40/29.37 tff(c_2129, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdf_rest), true)=true))). % 41.40/29.37 tff(c_2165, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdfs_domain), true)=true))). % 41.40/29.37 tff(c_2209, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdf_rest, C_92), true, icext(C_92, sK3_testcase_premise_fullish_022_List_Member_Access_BNODE_l32), true)=true))). % 41.40/29.37 tff(c_2205, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdfs_subPropertyOf), true)=true))). % 41.40/29.37 tff(c_2150, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdf_value), true)=true))). % 41.40/29.37 tff(c_2143, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdfs_isDefinedBy), true)=true))). % 41.40/29.37 tff(c_2194, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdfs_member), true)=true))). % 41.40/29.37 tff(c_2139, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdf_type), true)=true))). % 41.40/29.37 tff(c_2592, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdf_rest, C_96), true, icext(C_96, sK5_testcase_premise_fullish_022_List_Member_Access_BNODE_l12), true)=true))). % 41.40/29.37 tff(c_2192, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdf_rest, C_92), true, icext(C_92, sK8_testcase_premise_fullish_022_List_Member_Access_BNODE_l11), true)=true))). % 41.40/29.37 tff(c_2156, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdfs_range), true)=true))). % 41.40/29.37 tff(c_2554, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_96), true, icext(C_96, uri_rdfs_Datatype), true)=true))). % 41.40/29.37 tff(c_2179, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_92), true, icext(C_92, uri_rdf_Bag), true)=true))). % 41.40/29.37 tff(c_2568, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_96), true, icext(C_96, uri_rdf_Property), true)=true))). % 41.40/29.37 tff(c_2193, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_92), true, icext(C_92, uri_rdfs_Seq), true)=true))). % 41.40/29.37 tff(c_2142, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_92), true, icext(C_92, uri_rdfs_isDefinedBy), true)=true))). % 41.40/29.37 tff(c_2157, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdfs_domain), true)=true))). % 41.40/29.37 tff(c_18847, plain, (![X_312, Y_313]: (ifeq(iext(uri_rdfs_subClassOf, X_312, Y_313), true, icext(uri_rdfs_Class, Y_313), true)=true))). % 41.40/29.37 tff(c_2172, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdfs_member), true)=true))). % 41.40/29.37 tff(c_2146, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdfs_comment), true)=true))). % 41.40/29.37 tff(c_2571, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdf_first, C_96), true, icext(C_96, uri_ex_X), true)=true))). % 41.40/29.37 tff(c_2586, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_owl_propertyChainAxiom, C_96), true, icext(C_96, sK8_testcase_premise_fullish_022_List_Member_Access_BNODE_l11), true)=true))). % 41.40/29.37 tff(c_2539, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_96), true, icext(C_96, uri_rdfs_Class), true)=true))). % 41.40/29.37 tff(c_2585, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdf_first, C_96), true, icext(C_96, uri_rdf_rest), true)=true))). % 41.40/29.37 tff(c_2174, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdf_first, C_92), true, icext(C_92, sK2_testcase_premise_fullish_022_List_Member_Access_BNODE_l31), true)=true))). % 41.40/29.37 tff(c_2210, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdf__3), true)=true))). % 41.40/29.37 tff(c_18716, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_predicate, uri_rdf_predicate)=true)). % 41.40/29.37 tff(c_2583, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_96), true, icext(C_96, uri_rdf_List), true)=true))). % 41.40/29.37 tff(c_18531, plain, (ip(uri_rdf_predicate)=true)). % 41.40/29.37 tff(c_18474, plain, (iext(uri_rdf_type, uri_rdf_predicate, uri_rdf_Property)=true)). % 41.40/29.37 tff(c_18414, plain, (icext(uri_rdf_Property, uri_rdf_predicate)=true)). % 41.40/29.37 tff(c_2206, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdf_predicate), true)=true))). % 41.40/29.37 tff(c_2559, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_96), true, icext(C_96, uri_rdfs_Class), true)=true))). % 41.40/29.37 tff(c_2132, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdfs_range), true)=true))). % 41.40/29.37 tff(c_2177, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdf__1), true)=true))). % 41.40/29.37 tff(c_2164, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdfs_seeAlso), true)=true))). % 41.40/29.37 tff(c_2131, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdf__2), true)=true))). % 41.40/29.37 tff(c_2141, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdf__1), true)=true))). % 41.40/29.37 tff(c_16879, plain, (![X_282, Y_283]: (ifeq(iext(uri_rdf_first, X_282, Y_283), true, icext(uri_rdf_List, X_282), true)=true))). % 41.40/29.37 tff(c_2533, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdf_List), true)=true))). % 41.40/29.37 tff(c_2187, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_owl_propertyChainAxiom, C_92), true, icext(C_92, uri_skos_member), true)=true))). % 41.40/29.37 tff(c_2170, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdfs_subPropertyOf), true)=true))). % 41.40/29.37 tff(c_2166, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdf_subject), true)=true))). % 41.40/29.37 tff(c_2213, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdf_first, C_92), true, icext(C_92, sK3_testcase_premise_fullish_022_List_Member_Access_BNODE_l32), true)=true))). % 41.40/29.37 tff(c_2214, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdf_first, C_92), true, icext(C_92, sK8_testcase_premise_fullish_022_List_Member_Access_BNODE_l11), true)=true))). % 41.40/29.37 tff(c_17933, plain, (![X_33]: (ifeq(icext(uri_rdfs_Statement, X_33), true, icext(uri_rdfs_Statement, X_33), true)=true))). % 41.40/29.37 tff(c_17877, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Statement, uri_rdfs_Statement)=true)). % 41.40/29.37 tff(c_2600, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_96), true, icext(C_96, uri_rdfs_Literal), true)=true))). % 41.40/29.37 tff(c_17595, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Statement, uri_rdfs_Resource)=true)). % 41.40/29.37 tff(c_17548, plain, (iext(uri_rdf_type, uri_rdfs_Statement, uri_rdfs_Class)=true)). % 41.40/29.37 tff(c_17501, plain, (iext(uri_rdf_type, sK8_testcase_premise_fullish_022_List_Member_Access_BNODE_l11, uri_rdf_List)=true)). % 41.40/29.37 tff(c_17350, plain, (ic(uri_rdfs_Statement)=true)). % 41.40/29.37 tff(c_17288, plain, (icext(uri_rdfs_Class, uri_rdfs_Statement)=true)). % 41.40/29.37 tff(c_17221, plain, (iext(uri_rdf_type, sK7_testcase_premise_fullish_022_List_Member_Access_BNODE_l21, uri_rdf_List)=true)). % 41.40/29.37 tff(c_2584, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdfs_Statement), true)=true))). % 41.40/29.37 tff(c_16915, plain, (icext(uri_rdf_List, sK8_testcase_premise_fullish_022_List_Member_Access_BNODE_l11)=true)). % 41.40/29.37 tff(c_16912, plain, (icext(uri_rdf_List, sK7_testcase_premise_fullish_022_List_Member_Access_BNODE_l21)=true)). % 41.40/29.37 tff(c_2563, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdf_Property), true)=true))). % 41.40/29.37 tff(c_2183, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdf_first, C_92), true, icext(C_92, sK5_testcase_premise_fullish_022_List_Member_Access_BNODE_l12), true)=true))). % 41.40/29.37 tff(c_2560, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_96), true, icext(C_96, uri_rdf_Property), true)=true))). % 41.40/29.37 tff(c_2207, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdf__2), true)=true))). % 41.40/29.37 tff(c_2188, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdf_first), true)=true))). % 41.40/29.37 tff(c_16403, plain, (![X_33]: (ifeq(icext(uri_rdf_List, X_33), true, icext(uri_rdf_List, X_33), true)=true))). % 41.40/29.37 tff(c_16413, plain, (iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdfs_Resource)=true)). % 41.40/29.37 tff(c_16347, plain, (iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdf_List)=true)). % 41.40/29.37 tff(c_16300, plain, (iext(uri_rdf_type, uri_rdf_List, uri_rdfs_Class)=true)). % 41.40/29.37 tff(c_2151, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdf_subject), true)=true))). % 41.40/29.37 tff(c_16133, plain, (ic(uri_rdf_List)=true)). % 41.40/29.37 tff(c_16071, plain, (icext(uri_rdfs_Class, uri_rdf_List)=true)). % 41.40/29.37 tff(c_2546, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_96), true, icext(C_96, uri_rdf_List), true)=true))). % 41.40/29.37 tff(c_2602, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_owl_propertyChainAxiom, C_96), true, icext(C_96, sK7_testcase_premise_fullish_022_List_Member_Access_BNODE_l21), true)=true))). % 41.40/29.37 tff(c_2161, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_92), true, icext(C_92, uri_rdfs_ContainerMembershipProperty), true)=true))). % 41.40/29.37 tff(c_2552, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdfs_Class), true)=true))). % 41.40/29.37 tff(c_15731, plain, (![X_33]: (ifeq(icext(uri_skos_OrderedCollection, X_33), true, icext(uri_skos_OrderedCollection, X_33), true)=true))). % 41.40/29.37 tff(c_15741, plain, (iext(uri_rdfs_subClassOf, uri_skos_OrderedCollection, uri_rdfs_Resource)=true)). % 41.40/29.37 tff(c_15675, plain, (iext(uri_rdfs_subClassOf, uri_skos_OrderedCollection, uri_skos_OrderedCollection)=true)). % 41.40/29.37 tff(c_15627, plain, (iext(uri_rdf_type, uri_skos_OrderedCollection, uri_rdfs_Class)=true)). % 41.40/29.37 tff(c_15492, plain, (ic(uri_skos_OrderedCollection)=true)). % 41.40/29.37 tff(c_15425, plain, (icext(uri_rdfs_Class, uri_skos_OrderedCollection)=true)). % 41.40/29.37 tff(c_2555, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_96), true, icext(C_96, uri_skos_OrderedCollection), true)=true))). % 41.40/29.37 tff(c_2180, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdfs_seeAlso), true)=true))). % 41.40/29.38 tff(c_14751, plain, (![X_251, Y_252]: (ifeq(iext(uri_rdfs_subPropertyOf, X_251, Y_252), true, icext(uri_rdf_Property, X_251), true)=true))). % 41.40/29.38 tff(c_2167, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdf_rest, C_92), true, icext(C_92, sK4_testcase_premise_fullish_022_List_Member_Access_BNODE_l22), true)=true))). % 41.40/29.38 tff(c_6877, plain, (![X_33]: (ifeq(icext(uri_rdfs_Class, X_33), true, icext(uri_rdfs_Class, X_33), true)=true))). % 41.40/29.38 tff(c_12099, plain, (![X_33]: (ifeq(icext(uri_rdfs_Datatype, X_33), true, icext(uri_rdfs_Datatype, X_33), true)=true))). % 41.40/29.38 tff(c_2152, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdfs_subClassOf), true)=true))). % 41.40/29.38 tff(c_5485, plain, (![X_33]: (ifeq(icext(uri_rdfs_Container, X_33), true, icext(uri_rdfs_Container, X_33), true)=true))). % 41.40/29.38 tff(c_8686, plain, (![X_33]: (ifeq(icext(uri_rdfs_Literal, X_33), true, icext(uri_rdfs_Literal, X_33), true)=true))). % 41.40/29.38 tff(c_11462, plain, (![X_33]: (ifeq(icext(uri_rdf_XMLLiteral, X_33), true, icext(uri_rdf_XMLLiteral, X_33), true)=true))). % 41.40/29.38 tff(c_7544, plain, (![X_33]: (ifeq(icext(uri_rdf_Bag, X_33), true, icext(uri_rdf_Bag, X_33), true)=true))). % 41.40/29.38 tff(c_6392, plain, (![X_33]: (ifeq(icext(uri_rdf_Property, X_33), true, icext(uri_rdf_Property, X_33), true)=true))). % 41.40/29.38 tff(c_9350, plain, (![X_33]: (ifeq(icext(uri_rdf_Alt, X_33), true, icext(uri_rdf_Alt, X_33), true)=true))). % 41.40/29.38 tff(c_6724, plain, (![X_33]: (ifeq(icext(uri_rdfs_Seq, X_33), true, icext(uri_rdfs_Seq, X_33), true)=true))). % 41.40/29.38 tff(c_9118, plain, (![X_33]: (ifeq(icext(uri_rdfs_ContainerMembershipProperty, X_33), true, icext(uri_rdfs_ContainerMembershipProperty, X_33), true)=true))). % 41.40/29.38 tff(c_2199, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_92), true, icext(C_92, uri_rdf_XMLLiteral), true)=true))). % 41.40/29.38 tff(c_14488, plain, (iext(uri_rdf_type, uri_rdfs_Resource, uri_rdfs_Class)=true)). % 41.40/29.38 tff(c_14423, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_label, uri_rdfs_label)=true)). % 41.40/29.38 tff(c_14358, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_comment, uri_rdfs_comment)=true)). % 41.40/29.38 tff(c_2566, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_96), true, icext(C_96, uri_rdfs_Container), true)=true))). % 41.40/29.38 tff(c_14262, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Resource, uri_rdfs_Resource)=true)). % 41.40/29.38 tff(c_14192, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_member, uri_rdfs_member)=true)). % 41.40/29.38 tff(c_2184, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdf_rest), true)=true))). % 41.40/29.38 tff(c_14028, plain, (icext(uri_rdf_Property, uri_rdfs_member)=true)). % 41.40/29.38 tff(c_13974, plain, (iext(uri_rdf_type, uri_rdfs_member, uri_rdf_Property)=true)). % 41.40/29.38 tff(c_2160, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_92), true, icext(C_92, uri_rdfs_Datatype), true)=true))). % 41.40/29.38 tff(c_13898, plain, (iext(uri_rdf_type, uri_rdfs_Datatype, uri_rdfs_Class)=true)). % 41.40/29.38 tff(c_13851, plain, (iext(uri_rdf_type, uri_rdfs_Container, uri_rdfs_Class)=true)). % 41.40/29.38 tff(c_13779, plain, (iext(uri_rdf_type, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Class)=true)). % 41.40/29.38 tff(c_13730, plain, (iext(uri_rdf_type, uri_rdf_Bag, uri_rdfs_Class)=true)). % 41.40/29.38 tff(c_13657, plain, (iext(uri_rdf_type, uri_rdfs_Class, uri_rdfs_Class)=true)). % 41.40/29.38 tff(c_2202, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdf_object), true)=true))). % 41.40/29.38 tff(c_13515, plain, (iext(uri_rdf_type, sK1_testcase_premise_fullish_022_List_Member_Access_BNODE_l33, uri_rdf_List)=true)). % 41.40/29.38 tff(c_13474, plain, (icext(uri_rdf_List, sK1_testcase_premise_fullish_022_List_Member_Access_BNODE_l33)=true)). % 41.40/29.38 tff(c_2612, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdf_rest, C_96), true, icext(C_96, sK1_testcase_premise_fullish_022_List_Member_Access_BNODE_l33), true)=true))). % 41.40/29.38 tff(c_13407, plain, (iext(uri_rdf_type, uri_rdf_Alt, uri_rdfs_Class)=true)). % 41.40/29.38 tff(c_13359, plain, (iext(uri_rdf_type, uri_rdfs_Literal, uri_rdfs_Class)=true)). % 41.40/29.38 tff(c_13287, plain, (iext(uri_rdf_type, uri_rdf_XMLLiteral, uri_rdfs_Class)=true)). % 41.40/29.38 tff(c_2553, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_96), true, icext(C_96, uri_rdfs_Literal), true)=true))). % 41.40/29.38 tff(c_13145, plain, (iext(uri_rdf_type, sK5_testcase_premise_fullish_022_List_Member_Access_BNODE_l12, uri_rdf_List)=true)). % 41.40/29.38 tff(c_13104, plain, (icext(uri_rdf_List, sK5_testcase_premise_fullish_022_List_Member_Access_BNODE_l12)=true)). % 41.40/29.38 tff(c_2197, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdf_rest, C_92), true, icext(C_92, sK5_testcase_premise_fullish_022_List_Member_Access_BNODE_l12), true)=true))). % 41.40/29.38 tff(c_13036, plain, (iext(uri_rdf_type, sK2_testcase_premise_fullish_022_List_Member_Access_BNODE_l31, uri_rdf_List)=true)). % 41.40/29.38 tff(c_12901, plain, (icext(uri_rdf_List, sK2_testcase_premise_fullish_022_List_Member_Access_BNODE_l31)=true)). % 41.40/29.38 tff(c_2212, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdf_rest, C_92), true, icext(C_92, sK2_testcase_premise_fullish_022_List_Member_Access_BNODE_l31), true)=true))). % 41.40/29.38 tff(c_12834, plain, (iext(uri_rdf_type, uri_rdfs_Seq, uri_rdfs_Class)=true)). % 41.40/29.38 tff(c_12785, plain, (iext(uri_rdf_type, sK4_testcase_premise_fullish_022_List_Member_Access_BNODE_l22, uri_rdf_List)=true)). % 41.40/29.38 tff(c_12741, plain, (ip(uri_rdfs_label)=true)). % 41.40/29.38 tff(c_12684, plain, (iext(uri_rdf_type, uri_rdfs_label, uri_rdf_Property)=true)). % 41.40/29.38 tff(c_12637, plain, (iext(uri_rdf_type, sK3_testcase_premise_fullish_022_List_Member_Access_BNODE_l32, uri_rdf_List)=true)). % 41.40/29.38 tff(c_2134, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdfs_subClassOf), true)=true))). % 41.40/29.38 tff(c_12570, plain, (ip(uri_rdfs_comment)=true)). % 41.40/29.38 tff(c_12513, plain, (iext(uri_rdf_type, uri_rdfs_comment, uri_rdf_Property)=true)). % 41.40/29.38 tff(c_2148, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdf__3), true)=true))). % 41.40/29.38 tff(c_12417, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_type, uri_rdf_type)=true)). % 41.40/29.38 tff(c_12232, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Resource)=true)). % 41.40/29.38 tff(c_2162, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdf_first), true)=true))). % 41.40/29.38 tff(c_12141, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf)=true)). % 41.40/29.38 tff(c_945, plain, (![S_74, O_75]: (ifeq(iext(uri_rdf_rest, S_74, O_75), true, true, true)=true))). % 41.40/29.38 tff(c_12042, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Datatype)=true)). % 41.40/29.38 tff(c_11763, plain, (icext(uri_rdf_Property, uri_rdfs_comment)=true)). % 41.40/29.38 tff(c_11677, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdfs_Resource)=true)). % 41.40/29.38 tff(c_2153, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdfs_comment), true)=true))). % 41.40/29.38 tff(c_11551, plain, (icext(uri_rdf_Property, uri_rdfs_domain)=true)). % 41.40/29.38 tff(c_2168, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_92), true, icext(C_92, uri_rdf_Alt), true)=true))). % 41.40/29.38 tff(c_11472, plain, (iext(uri_rdf_type, uri_rdfs_domain, uri_rdf_Property)=true)). % 41.40/29.38 tff(c_11406, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdf_XMLLiteral)=true)). % 41.40/29.38 tff(c_1718, plain, (![S_5, O_6]: (ifeq(iext(uri_skos_memberList, S_5, O_6), true, true, true)=true))). % 41.40/29.38 tff(c_11303, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_first, uri_rdf_first)=true)). % 41.40/29.38 tff(c_11119, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Resource)=true)). % 41.40/29.38 tff(c_11029, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_seeAlso, uri_rdfs_seeAlso)=true)). % 41.40/29.38 tff(c_2590, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_96), true, icext(C_96, sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL), true)=true))). % 41.40/29.38 tff(c_3723, plain, (![S_5, O_6]: (ifeq(iext(sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL, S_5, O_6), true, true, true)=true))). % 41.40/29.38 tff(c_10955, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_subject, uri_rdf_subject)=true)). % 41.40/29.38 tff(c_10888, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__3, uri_rdf__3)=true)). % 41.40/29.38 tff(c_10822, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_range, uri_rdfs_range)=true)). % 41.40/29.38 tff(c_10726, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__3, uri_rdfs_member)=true)). % 41.40/29.38 tff(c_10605, plain, (icext(uri_rdf_Property, uri_rdfs_subClassOf)=true)). % 41.40/29.38 tff(c_10550, plain, (iext(uri_rdf_type, uri_rdfs_subClassOf, uri_rdf_Property)=true)). % 41.40/29.38 tff(c_10338, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdfs_Resource)=true)). % 41.40/29.38 tff(c_10248, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, uri_rdfs_domain)=true)). % 41.40/29.38 tff(c_10087, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Container, uri_rdfs_Resource)=true)). % 41.40/29.38 tff(c_10022, plain, (iext(uri_rdfs_subPropertyOf, uri_owl_propertyChainAxiom, uri_owl_propertyChainAxiom)=true)). % 41.40/29.38 tff(c_2588, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_96), true, icext(C_96, uri_rdfs_Resource), true)=true))). % 41.40/29.38 tff(c_9890, plain, (icext(uri_rdf_Property, uri_rdfs_subPropertyOf)=true)). % 41.40/29.38 tff(c_9832, plain, (iext(uri_rdf_type, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 41.40/29.38 tff(c_9765, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__2, uri_rdf__2)=true)). % 41.40/29.38 tff(c_2596, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_96), true, icext(C_96, uri_rdfs_ContainerMembershipProperty), true)=true))). % 41.40/29.38 tff(c_9586, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Resource)=true)). % 41.40/29.38 tff(c_9520, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, uri_rdfs_isDefinedBy)=true)). % 41.40/29.38 tff(c_2201, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_owl_propertyChainAxiom, C_92), true, icext(C_92, sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL), true)=true))). % 41.40/29.38 tff(c_1807, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_subPropertyOf, S_5, O_6), true, true, true)=true))). % 41.40/29.38 tff(c_9294, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdf_Alt)=true)). % 41.40/29.38 tff(c_2591, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdf_first, C_96), true, icext(C_96, sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL), true)=true))). % 41.40/29.38 tff(c_9129, plain, (iext(uri_rdfs_subPropertyOf, uri_skos_memberList, uri_skos_memberList)=true)). % 41.40/29.38 tff(c_9062, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdfs_ContainerMembershipProperty)=true)). % 41.40/29.38 tff(c_1300, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_range, S_5, O_6), true, true, true)=true))). % 41.40/29.38 tff(c_8827, plain, (icext(uri_rdf_Property, uri_owl_propertyChainAxiom)=true)). % 41.40/29.38 tff(c_8769, plain, (iext(uri_rdf_type, uri_owl_propertyChainAxiom, uri_rdf_Property)=true)). % 41.40/29.38 tff(c_8627, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdfs_Literal)=true)). % 41.40/29.38 tff(c_8495, plain, (icext(uri_rdf_Property, uri_rdfs_isDefinedBy)=true)). % 41.40/29.38 tff(c_8414, plain, (iext(uri_rdf_type, uri_rdfs_isDefinedBy, uri_rdf_Property)=true)). % 41.40/29.38 tff(c_2178, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdf_value), true)=true))). % 41.40/29.38 tff(c_8349, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__1, uri_rdf__1)=true)). % 41.40/29.38 tff(c_8194, plain, (iext(uri_rdf_type, uri_rdfs_seeAlso, uri_rdf_Property)=true)). % 41.40/29.38 tff(c_2570, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdf_rest, C_96), true, icext(C_96, uri_rdf_nil), true)=true))). % 41.40/29.38 tff(c_8100, plain, (icext(uri_rdf_List, sK4_testcase_premise_fullish_022_List_Member_Access_BNODE_l22)=true)). % 41.40/29.38 tff(c_2604, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdf_rest, C_96), true, icext(C_96, sK4_testcase_premise_fullish_022_List_Member_Access_BNODE_l22), true)=true))). % 41.40/29.38 tff(c_8015, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_value, uri_rdf_value)=true)). % 41.40/29.38 tff(c_7951, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_object, uri_rdf_object)=true)). % 41.40/29.38 tff(c_2190, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_92), true, icext(C_92, uri_skos_memberList), true)=true))). % 41.40/29.38 tff(c_7749, plain, (icext(uri_rdf_List, sK3_testcase_premise_fullish_022_List_Member_Access_BNODE_l32)=true)). % 41.40/29.38 tff(c_2616, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdf_rest, C_96), true, icext(C_96, sK3_testcase_premise_fullish_022_List_Member_Access_BNODE_l32), true)=true))). % 41.40/29.38 tff(c_7666, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__1, uri_rdfs_member)=true)). % 41.40/29.38 tff(c_1625, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_domain, S_5, O_6), true, true, true)=true))). % 41.40/29.38 tff(c_7488, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdf_Bag)=true)). % 41.40/29.38 tff(c_7278, plain, (icext(uri_rdf_Property, uri_rdfs_seeAlso)=true)). % 41.40/29.38 tff(c_2543, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_96), true, icext(C_96, uri_rdfs_seeAlso), true)=true))). % 41.40/29.38 tff(c_7166, plain, (icext(uri_rdf_Property, uri_skos_memberList)=true)). % 41.40/29.38 tff(c_7109, plain, (iext(uri_rdf_type, uri_skos_memberList, uri_rdf_Property)=true)). % 41.40/29.38 tff(c_2537, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_96), true, icext(C_96, uri_rdfs_Class), true)=true))). % 41.40/29.38 tff(c_6887, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Resource)=true)). % 41.40/29.38 tff(c_2597, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdf_first, C_96), true, icext(C_96, uri_ex_Z), true)=true))). % 41.40/29.38 tff(c_6821, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdfs_Class)=true)). % 41.40/29.38 tff(c_6734, plain, (iext(uri_rdfs_subPropertyOf, sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL, sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL)=true)). % 41.40/29.38 tff(c_2617, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdf_first, C_96), true, icext(C_96, uri_ex_Y), true)=true))). % 41.40/29.38 tff(c_6668, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Seq)=true)). % 41.40/29.38 tff(c_2582, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdf_first, C_96), true, icext(C_96, uri_rdf_first), true)=true))). % 41.40/29.38 tff(c_6507, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Resource)=true)). % 41.40/29.38 tff(c_6420, plain, (icext(uri_rdf_Property, uri_rdfs_label)=true)). % 41.40/29.38 tff(c_2182, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdfs_label), true)=true))). % 41.40/29.38 tff(c_6336, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdf_Property)=true)). % 41.40/29.38 tff(c_3526, plain, (![S_5, O_6]: (ifeq(iext(uri_owl_propertyChainAxiom, S_5, O_6), true, true, true)=true))). % 41.40/29.38 tff(c_2547, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdfs_Resource), true)=true))). % 41.40/29.38 tff(c_6184, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_rest, uri_rdf_rest)=true)). % 41.40/29.38 tff(c_6142, plain, (ip(uri_rdfs_member)=true)). % 41.40/29.38 tff(c_6054, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__2, uri_rdfs_member)=true)). % 41.40/29.38 tff(c_5976, plain, (icext(uri_rdf_Property, uri_rdfs_range)=true)). % 41.40/29.38 tff(c_2536, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_96), true, icext(C_96, uri_rdf_Property), true)=true))). % 41.40/29.38 tff(c_5895, plain, (iext(uri_rdf_type, uri_rdfs_range, uri_rdf_Property)=true)). % 41.40/29.38 tff(c_5806, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdfs_Resource)=true)). % 41.40/29.38 tff(c_1779, plain, (![X_89]: (ifeq(icext(uri_rdf_Alt, X_89), true, icext(uri_rdfs_Container, X_89), true)=true))). % 41.40/29.38 tff(c_948, plain, (![S_74, O_75]: (ifeq(iext(uri_rdf_object, S_74, O_75), true, true, true)=true))). % 41.40/29.38 tff(c_5700, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, uri_rdfs_subClassOf)=true)). % 41.40/29.38 tff(c_1780, plain, (![X_89]: (ifeq(icext(uri_rdf_Bag, X_89), true, icext(uri_rdfs_Container, X_89), true)=true))). % 41.40/29.38 tff(c_5626, plain, (icext(uri_rdf_Property, sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL)=true)). % 41.40/29.38 tff(c_1778, plain, (![X_89]: (ifeq(icext(uri_rdfs_ContainerMembershipProperty, X_89), true, icext(uri_rdf_Property, X_89), true)=true))). % 41.40/29.38 tff(c_5496, plain, (iext(uri_rdf_type, sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL, uri_rdf_Property)=true)). % 41.40/29.38 tff(c_5429, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Container, uri_rdfs_Container)=true)). % 41.40/29.38 tff(c_1782, plain, (![X_89]: (ifeq(icext(uri_rdf_XMLLiteral, X_89), true, icext(uri_rdfs_Literal, X_89), true)=true))). % 41.40/29.38 tff(c_5336, plain, (icext(uri_rdfs_Class, uri_rdfs_Resource)=true)). % 41.40/29.38 tff(c_1781, plain, (![X_89]: (ifeq(icext(uri_rdfs_Seq, X_89), true, icext(uri_rdfs_Container, X_89), true)=true))). % 41.40/29.38 tff(c_5253, plain, (ic(uri_rdfs_Resource)=true)). % 41.40/29.38 tff(c_1777, plain, (![X_89]: (ifeq(icext(uri_rdfs_Datatype, X_89), true, icext(uri_rdfs_Class, X_89), true)=true))). % 41.40/29.38 tff(c_5146, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Resource)=true)). % 41.40/29.38 tff(c_1407, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_subClassOf, S_5, O_6), true, true, true)=true))). % 41.40/29.38 tff(c_5063, plain, (![X_137]: (iext(uri_rdf_type, X_137, uri_rdfs_Resource)=true))). % 41.40/29.38 tff(c_2587, plain, (![X_97, Y_98]: (ifeq(iext(uri_rdf_first, X_97, Y_98), true, true, true)=true))). % 41.40/29.38 tff(c_2550, plain, (![X_97, Y_98]: (ifeq(iext(uri_rdf_subject, X_97, Y_98), true, true, true)=true))). % 41.40/29.38 tff(c_2594, plain, (![X_97, Y_98]: (ifeq(iext(uri_rdfs_member, X_97, Y_98), true, true, true)=true))). % 41.40/29.38 tff(c_2158, plain, (![X_93, Y_94]: (ifeq(iext(uri_rdfs_isDefinedBy, X_93, Y_94), true, true, true)=true))). % 41.40/29.38 tff(c_2138, plain, (![X_93, Y_94]: (ifeq(iext(uri_rdf_type, X_93, Y_94), true, true, true)=true))). % 41.40/29.38 tff(c_2607, plain, (![X_97, Y_98]: (ifeq(iext(uri_rdf_predicate, X_97, Y_98), true, true, true)=true))). % 41.40/29.38 tff(c_2145, plain, (![X_93, Y_94]: (ifeq(iext(uri_rdfs_comment, X_93, Y_94), true, true, true)=true))). % 41.40/29.38 tff(c_2576, plain, (![X_97, Y_98]: (ifeq(iext(uri_rdf_value, X_97, Y_98), true, true, true)=true))). % 41.40/29.38 tff(c_2181, plain, (![X_93, Y_94]: (ifeq(iext(uri_rdfs_label, X_93, Y_94), true, true, true)=true))). % 41.40/29.38 tff(c_2140, plain, (![X_93, Y_94]: (ifeq(iext(uri_rdf__1, X_93, Y_94), true, true, true)=true))). % 41.40/29.38 tff(c_4860, plain, (icext(uri_rdfs_Class, uri_rdf_Alt)=true)). % 41.40/29.38 tff(c_4798, plain, (icext(uri_rdfs_Class, uri_rdfs_Literal)=true)). % 41.40/29.38 tff(c_4753, plain, (icext(uri_rdfs_Class, uri_rdfs_Class)=true)). % 41.40/29.38 tff(c_4710, plain, (icext(uri_rdfs_Class, uri_rdfs_Datatype)=true)). % 41.40/29.38 tff(c_4667, plain, (icext(uri_rdfs_Class, uri_rdfs_Container)=true)). % 41.40/29.38 tff(c_2579, plain, (![X_97, Y_98]: (ifeq(iext(uri_rdfs_seeAlso, X_97, Y_98), true, true, true)=true))). % 41.40/29.38 tff(c_4614, plain, (icext(uri_rdfs_Class, uri_rdf_Bag)=true)). % 41.40/29.38 tff(c_4569, plain, (icext(uri_rdfs_Class, uri_rdfs_ContainerMembershipProperty)=true)). % 41.40/29.38 tff(c_2130, plain, (![X_93, Y_94]: (ifeq(iext(uri_rdf__2, X_93, Y_94), true, true, true)=true))). % 41.40/29.38 tff(c_4519, plain, (icext(uri_rdfs_Class, uri_rdfs_Seq)=true)). % 41.40/29.38 tff(c_4470, plain, (icext(uri_rdfs_Class, uri_rdf_XMLLiteral)=true)). % 41.40/29.38 tff(c_2613, plain, (![X_97, Y_98]: (ifeq(iext(uri_rdf__3, X_97, Y_98), true, true, true)=true))). % 41.40/29.38 tff(c_4416, plain, (icext(uri_rdf_Property, uri_rdf__3)=true)). % 41.40/29.38 tff(c_4377, plain, (icext(uri_rdf_Property, uri_rdf__1)=true)). % 41.40/29.38 tff(c_4327, plain, (icext(uri_rdfs_Class, uri_rdf_Property)=true)). % 41.40/29.38 tff(c_4288, plain, (icext(uri_rdf_Property, uri_rdf_object)=true)). % 41.40/29.38 tff(c_4248, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__1)=true)). % 41.40/29.38 tff(c_4207, plain, (icext(uri_rdf_Property, uri_rdf_rest)=true)). % 41.40/29.38 tff(c_4163, plain, (icext(uri_rdfs_Datatype, uri_rdf_XMLLiteral)=true)). % 41.40/29.38 tff(c_4120, plain, (icext(uri_rdf_Property, uri_rdf_subject)=true)). % 41.40/29.38 tff(c_4074, plain, (icext(uri_rdf_Property, uri_rdf_value)=true)). % 41.40/29.38 tff(c_4034, plain, (icext(uri_rdf_List, uri_rdf_nil)=true)). % 41.40/29.38 tff(c_3988, plain, (icext(uri_rdf_Property, uri_rdf__2)=true)). % 41.40/29.38 tff(c_3947, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__2)=true)). % 41.40/29.38 tff(c_3911, plain, (icext(uri_skos_OrderedCollection, uri_ex_MyOrderedCollection)=true)). % 41.40/29.38 tff(c_3870, plain, (icext(uri_rdf_Property, uri_rdf_type)=true)). % 41.40/29.38 tff(c_3826, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__3)=true)). % 41.40/29.38 tff(c_3785, plain, (icext(uri_rdf_Property, uri_rdf_first)=true)). % 41.40/29.38 tff(c_3745, plain, (ip(uri_rdf__2)=true)). % 41.40/29.38 tff(c_3705, plain, (ip(sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL)=true)). % 41.40/29.38 tff(c_3669, plain, (ic(uri_rdfs_Seq)=true)). % 41.40/29.38 tff(c_3630, plain, (ic(uri_rdfs_Class)=true)). % 41.40/29.38 tff(c_3592, plain, (ic(uri_rdf_Bag)=true)). % 41.40/29.38 tff(c_3545, plain, (ic(uri_rdf_XMLLiteral)=true)). % 41.40/29.38 tff(c_3508, plain, (ip(uri_owl_propertyChainAxiom)=true)). % 41.40/29.38 tff(c_3473, plain, (ip(uri_rdfs_isDefinedBy)=true)). % 41.40/29.38 tff(c_3433, plain, (ic(uri_rdf_Property)=true)). % 41.40/29.38 tff(c_3398, plain, (ic(uri_rdfs_Datatype)=true)). % 41.40/29.38 tff(c_3351, plain, (ip(uri_rdf__3)=true)). % 41.40/29.38 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))). % 41.40/29.38 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))). % 41.40/29.38 tff(c_2677, plain, (ip(uri_rdfs_seeAlso)=true)). % 41.40/29.38 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))). % 41.40/29.38 tff(c_2222, plain, (ip(uri_rdf_subject)=true)). % 41.40/29.38 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))). % 41.40/29.38 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))). % 41.40/29.38 tff(c_220, plain, (tuple(iext(uri_skos_member, uri_ex_MyOrderedCollection, uri_ex_Y), iext(uri_skos_member, uri_ex_MyOrderedCollection, uri_ex_X), iext(uri_skos_member, uri_ex_MyOrderedCollection, uri_ex_Z))!=tuple(true, true, true))). % 41.40/29.39 tff(c_1789, plain, (ip(uri_rdfs_subPropertyOf)=true)). % 41.40/29.39 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))). % 41.40/29.39 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))). % 41.40/29.39 tff(c_1700, plain, (ip(uri_skos_memberList)=true)). % 41.40/29.39 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))). % 41.40/29.39 tff(c_1607, plain, (ip(uri_rdfs_domain)=true)). % 41.40/29.39 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))). % 41.40/29.39 tff(c_1565, plain, (ic(uri_rdfs_Container)=true)). % 41.40/29.39 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))). % 41.40/29.39 tff(c_1470, plain, (ic(uri_rdfs_Literal)=true)). % 41.40/29.39 tff(c_150, plain, (![C_35, D_36]: (ifeq(iext(uri_rdfs_subClassOf, C_35, D_36), true, ic(D_36), true)=true))). % 41.40/29.39 tff(c_1368, plain, (ip(uri_rdfs_subClassOf)=true)). % 41.40/29.39 tff(c_156, plain, (![C_39]: (ifeq(ic(C_39), true, iext(uri_rdfs_subClassOf, C_39, C_39), true)=true))). % 41.40/29.39 tff(c_164, plain, (![P_45, Q_46]: (ifeq(iext(uri_rdfs_subPropertyOf, P_45, Q_46), true, ip(P_45), true)=true))). % 41.40/29.39 tff(c_1285, plain, (ip(uri_rdfs_range)=true)). % 41.40/29.39 tff(c_1232, plain, (ip(uri_rdf_type)=true)). % 41.40/29.39 tff(c_170, plain, (![P_51]: (ifeq(ip(P_51), true, iext(uri_rdfs_subPropertyOf, P_51, P_51), true)=true))). % 41.40/29.39 tff(c_913, plain, (ic(uri_rdfs_ContainerMembershipProperty)=true)). % 41.40/29.39 tff(c_4, plain, (![P_4, S_5, O_6]: (ifeq(iext(P_4, S_5, O_6), true, ip(P_4), true)=true))). % 41.40/29.39 tff(c_884, plain, (ic(uri_rdf_Alt)=true)). % 41.40/29.39 tff(c_162, plain, (![P_43, Q_44]: (ifeq(iext(uri_rdfs_subPropertyOf, P_43, Q_44), true, ip(Q_44), true)=true))). % 41.40/29.39 tff(c_829, plain, (ip(uri_rdf_first)=true)). % 41.40/29.39 tff(c_152, plain, (![C_37, D_38]: (ifeq(iext(uri_rdfs_subClassOf, C_37, D_38), true, ic(C_37), true)=true))). % 41.40/29.39 tff(c_773, plain, (ip(uri_rdf__1)=true)). % 41.40/29.39 tff(c_28, plain, (![P_9]: (ifeq(ip(P_9), true, iext(uri_rdf_type, P_9, uri_rdf_Property), true)=true))). % 41.40/29.39 tff(c_699, plain, (ip(uri_rdf_value)=true)). % 41.40/29.39 tff(c_58, plain, (![C_15]: (ifeq(ic(C_15), true, iext(uri_rdfs_subClassOf, C_15, uri_rdfs_Resource), true)=true))). % 41.40/29.39 tff(c_671, plain, (ip(uri_rdf_rest)=true)). % 41.40/29.39 tff(c_650, plain, (ip(uri_rdf_object)=true)). % 41.40/29.39 tff(c_30, plain, (![P_10]: (ifeq(iext(uri_rdf_type, P_10, uri_rdf_Property), true, ip(P_10), true)=true))). % 41.40/29.39 tff(c_116, plain, (![X_23]: (ifeq(icext(uri_rdfs_Class, X_23), true, ic(X_23), true)=true))). % 41.40/29.39 tff(c_124, plain, (![X_27]: (ifeq(lv(X_27), true, icext(uri_rdfs_Literal, X_27), true)=true))). % 41.40/29.39 tff(c_122, plain, (![X_26]: (ifeq(icext(uri_rdfs_Literal, X_26), true, lv(X_26), true)=true))). % 41.40/29.39 tff(c_114, plain, (![X_22]: (ifeq(ic(X_22), true, icext(uri_rdfs_Class, X_22), true)=true))). % 41.40/29.39 tff(c_566, plain, (![X_60]: (icext(uri_rdfs_Resource, X_60)=true))). % 41.40/29.39 tff(c_223, plain, (![X_8]: (ifeq(lv(X_8), true, true, true)=true))). % 41.40/29.39 tff(c_2, plain, (![A_1, B_2, C_3]: (ifeq(A_1, A_1, B_2, C_3)=B_2))). % 41.40/29.39 tff(c_22, plain, (iext(uri_rdf_type, uri_rdf_object, uri_rdf_Property)=true)). % 41.40/29.39 tff(c_20, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdf_Property)=true)). % 41.40/29.39 tff(c_64, plain, (iext(uri_rdfs_domain, uri_rdf_rest, uri_rdf_List)=true)). % 41.40/29.39 tff(c_82, plain, (iext(uri_rdfs_domain, uri_rdf__2, uri_rdfs_Resource)=true)). % 41.40/29.39 tff(c_128, plain, (iext(uri_rdfs_domain, uri_rdfs_range, uri_rdf_Property)=true)). % 41.40/29.39 tff(c_18, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdf_Property)=true)). % 41.40/29.39 tff(c_154, plain, (iext(uri_rdfs_range, uri_rdfs_subClassOf, uri_rdfs_Class)=true)). % 41.40/29.39 tff(c_34, plain, (iext(uri_rdf_type, uri_rdf_type, uri_rdf_Property)=true)). % 41.40/29.39 tff(c_126, plain, (iext(uri_rdf_type, uri_rdf_Property, uri_rdfs_Class)=true)). % 41.40/29.39 tff(c_10, plain, (iext(uri_rdf_type, uri_rdf_first, uri_rdf_Property)=true)). % 41.40/29.39 tff(c_174, plain, (iext(uri_rdfs_domain, uri_rdf_type, uri_rdfs_Resource)=true)). % 41.40/29.39 tff(c_80, plain, (iext(uri_rdfs_domain, uri_rdf__1, uri_rdfs_Resource)=true)). % 41.40/29.39 tff(c_44, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso)=true)). % 41.40/29.39 tff(c_42, plain, (iext(uri_rdfs_range, uri_rdfs_isDefinedBy, uri_rdfs_Resource)=true)). % 41.40/29.39 tff(c_12, plain, (iext(uri_rdf_type, uri_rdf_nil, uri_rdf_List)=true)). % 41.40/29.39 tff(c_36, plain, (iext(uri_rdfs_domain, uri_rdfs_comment, uri_rdfs_Resource)=true)). % 41.40/29.39 tff(c_84, plain, (iext(uri_rdfs_domain, uri_rdf__3, uri_rdfs_Resource)=true)). % 41.40/29.39 tff(c_178, plain, (iext(uri_rdfs_domain, uri_rdf_value, uri_rdfs_Resource)=true)). % 41.40/29.39 tff(c_144, plain, (iext(uri_rdfs_range, uri_rdf_subject, uri_rdfs_Resource)=true)). % 41.40/29.39 tff(c_146, plain, (iext(uri_rdfs_domain, uri_rdfs_subClassOf, uri_rdfs_Class)=true)). % 41.40/29.39 tff(c_38, plain, (iext(uri_rdfs_range, uri_rdfs_comment, uri_rdfs_Literal)=true)). % 41.40/29.39 tff(c_102, plain, (iext(uri_rdf_type, uri_rdf_XMLLiteral, uri_rdfs_Datatype)=true)). % 41.40/29.39 tff(c_216, plain, (iext(uri_rdf_type, uri_ex_MyOrderedCollection, uri_skos_OrderedCollection)=true)). % 41.40/29.39 tff(c_132, plain, (iext(uri_rdfs_range, uri_rdfs_range, uri_rdfs_Class)=true)). % 41.40/29.39 tff(c_112, plain, (iext(uri_rdfs_range, uri_rdfs_domain, uri_rdfs_Class)=true)). % 41.40/29.39 tff(c_40, plain, (iext(uri_rdfs_domain, uri_rdfs_isDefinedBy, uri_rdfs_Resource)=true)). % 41.40/29.39 tff(c_106, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Class)=true)). % 41.40/29.39 tff(c_74, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property)=true)). % 41.40/29.39 tff(c_60, plain, (iext(uri_rdfs_domain, uri_rdf_first, uri_rdf_List)=true)). % 41.40/29.39 tff(c_50, plain, (iext(uri_rdfs_domain, uri_rdfs_seeAlso, uri_rdfs_Resource)=true)). % 41.40/29.39 tff(c_108, plain, (iext(uri_rdfs_domain, uri_rdfs_domain, uri_rdf_Property)=true)). % 41.40/29.39 tff(c_142, plain, (iext(uri_rdfs_domain, uri_rdf_subject, uri_rdfs_Statement)=true)). % 41.40/29.39 tff(c_194, plain, (iext(uri_rdf_rest, sK4_testcase_premise_fullish_022_List_Member_Access_BNODE_l22, uri_rdf_nil)=true)). % 41.40/29.39 tff(c_68, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Container)=true)). % 41.40/29.39 tff(c_26, plain, (iext(uri_rdf_type, uri_rdf_subject, uri_rdf_Property)=true)). % 41.40/29.39 tff(c_168, plain, (iext(uri_rdfs_range, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 41.40/29.39 tff(c_76, plain, (iext(uri_rdfs_domain, uri_rdfs_member, uri_rdfs_Resource)=true)). % 41.40/29.39 tff(c_188, plain, (iext(uri_rdf_rest, sK1_testcase_premise_fullish_022_List_Member_Access_BNODE_l33, uri_rdf_nil)=true)). % 41.40/29.39 tff(c_204, plain, (iext(uri_rdf_first, sK2_testcase_premise_fullish_022_List_Member_Access_BNODE_l31, uri_ex_X)=true)). % 41.40/29.39 tff(c_48, plain, (iext(uri_rdfs_range, uri_rdfs_label, uri_rdfs_Literal)=true)). % 41.40/29.39 tff(c_176, plain, (iext(uri_rdfs_range, uri_rdf_type, uri_rdfs_Class)=true)). % 41.40/29.39 tff(c_86, plain, (iext(uri_rdfs_range, uri_rdf__1, uri_rdfs_Resource)=true)). % 41.40/29.39 tff(c_180, plain, (iext(uri_rdfs_range, uri_rdf_value, uri_rdfs_Resource)=true)). % 41.40/29.39 tff(c_70, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Container)=true)). % 41.40/29.39 tff(c_52, plain, (iext(uri_rdfs_range, uri_rdfs_seeAlso, uri_rdfs_Resource)=true)). % 41.40/29.39 tff(c_46, plain, (iext(uri_rdfs_domain, uri_rdfs_label, uri_rdfs_Resource)=true)). % 41.40/29.39 tff(c_210, plain, (iext(uri_rdf_first, sK5_testcase_premise_fullish_022_List_Member_Access_BNODE_l12, uri_rdf_first)=true)). % 41.40/29.39 tff(c_66, plain, (iext(uri_rdfs_range, uri_rdf_rest, uri_rdf_List)=true)). % 41.40/29.39 tff(c_138, plain, (iext(uri_rdfs_domain, uri_rdf_predicate, uri_rdfs_Statement)=true)). % 41.40/29.39 tff(c_208, plain, (iext(uri_rdf_first, sK4_testcase_premise_fullish_022_List_Member_Access_BNODE_l22, uri_rdf_rest)=true)). % 41.40/29.39 tff(c_184, plain, (iext(uri_owl_propertyChainAxiom, uri_skos_member, sK8_testcase_premise_fullish_022_List_Member_Access_BNODE_l11)=true)). % 41.40/29.39 tff(c_62, plain, (iext(uri_rdfs_range, uri_rdf_first, uri_rdfs_Resource)=true)). % 41.40/29.39 tff(c_94, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdfs_ContainerMembershipProperty)=true)). % 41.40/29.39 tff(c_218, plain, (iext(uri_rdfs_subPropertyOf, uri_skos_memberList, sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL)=true)). % 41.40/29.39 tff(c_212, plain, (iext(uri_rdf_first, sK7_testcase_premise_fullish_022_List_Member_Access_BNODE_l21, sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL)=true)). % 41.40/29.39 tff(c_200, plain, (iext(uri_rdf_rest, sK8_testcase_premise_fullish_022_List_Member_Access_BNODE_l11, sK5_testcase_premise_fullish_022_List_Member_Access_BNODE_l12)=true)). % 41.40/29.39 tff(c_98, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Container)=true)). % 41.40/29.39 tff(c_78, plain, (iext(uri_rdfs_range, uri_rdfs_member, uri_rdfs_Resource)=true)). % 41.40/29.39 tff(c_96, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdfs_ContainerMembershipProperty)=true)). % 41.40/29.39 tff(c_202, plain, (iext(uri_rdf_first, sK1_testcase_premise_fullish_022_List_Member_Access_BNODE_l33, uri_ex_Z)=true)). % 41.40/29.39 tff(c_196, plain, (iext(uri_rdf_rest, sK5_testcase_premise_fullish_022_List_Member_Access_BNODE_l12, uri_rdf_nil)=true)). % 41.40/29.39 tff(c_16, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdf_Property)=true)). % 41.40/29.39 tff(c_100, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Literal)=true)). % 41.40/29.39 tff(c_24, plain, (iext(uri_rdf_type, uri_rdf_value, uri_rdf_Property)=true)). % 41.40/29.39 tff(c_182, plain, (iext(uri_owl_propertyChainAxiom, sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL, sK7_testcase_premise_fullish_022_List_Member_Access_BNODE_l21)=true)). % 41.40/29.39 tff(c_134, plain, (iext(uri_rdfs_domain, uri_rdf_object, uri_rdfs_Statement)=true)). % 41.40/29.39 tff(c_198, plain, (iext(uri_rdf_rest, sK7_testcase_premise_fullish_022_List_Member_Access_BNODE_l21, sK4_testcase_premise_fullish_022_List_Member_Access_BNODE_l22)=true)). % 41.40/29.39 tff(c_186, plain, (iext(uri_skos_memberList, uri_ex_MyOrderedCollection, sK2_testcase_premise_fullish_022_List_Member_Access_BNODE_l31)=true)). % 41.40/29.39 tff(c_160, plain, (iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 41.40/29.39 tff(c_140, plain, (iext(uri_rdfs_range, uri_rdf_predicate, uri_rdfs_Resource)=true)). % 41.40/29.39 tff(c_88, plain, (iext(uri_rdfs_range, uri_rdf__2, uri_rdfs_Resource)=true)). % 41.40/29.39 tff(c_14, plain, (iext(uri_rdf_type, uri_rdf_rest, uri_rdf_Property)=true)). % 41.40/29.39 tff(c_192, plain, (iext(uri_rdf_rest, sK3_testcase_premise_fullish_022_List_Member_Access_BNODE_l32, sK1_testcase_premise_fullish_022_List_Member_Access_BNODE_l33)=true)). % 41.40/29.39 tff(c_90, plain, (iext(uri_rdfs_range, uri_rdf__3, uri_rdfs_Resource)=true)). % 41.40/29.39 tff(c_92, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdfs_ContainerMembershipProperty)=true)). % 41.40/29.39 tff(c_190, plain, (iext(uri_rdf_rest, sK2_testcase_premise_fullish_022_List_Member_Access_BNODE_l31, sK3_testcase_premise_fullish_022_List_Member_Access_BNODE_l32)=true)). % 41.40/29.39 tff(c_206, plain, (iext(uri_rdf_first, sK3_testcase_premise_fullish_022_List_Member_Access_BNODE_l32, uri_ex_Y)=true)). % 41.40/29.39 tff(c_214, plain, (iext(uri_rdf_first, sK8_testcase_premise_fullish_022_List_Member_Access_BNODE_l11, sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL)=true)). % 41.40/29.39 tff(c_6, plain, (![X_7]: (ir(X_7)=true))). % 41.40/29.39 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 41.40/29.39 %------------------------------------------------------------------------------