%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SWB024-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 : n023.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:55 PM UTC 2025 % Result : Satisfiable 38.99s 27.77s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SWB024-10 : TPTP v9.0.0. Released v7.3.0. % 0.07/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.13/0.33 % Computer : n023.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % 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 01:01:39 EDT 2025 % 0.13/0.34 % CPUTime : % 38.99/27.77 % 38.99/27.77 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 38.99/27.77 % 38.99/27.77 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 38.99/27.79 %$ ifeq > iext > tuple > literal_typed > icext > #nlpp > lv > ir > ip > ic > uri_xsd_nonNegativeInteger > 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_onProperty > uri_owl_minCardinality > uri_owl_TransitiveProperty > uri_owl_Restriction > uri_ex_hasAncestor > uri_ex_bob > uri_ex_alice > uri_ex_Person > true > sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z > dat_str_1 % 38.99/27.79 % 38.99/27.79 %Foreground sorts: % 38.99/27.79 % 38.99/27.79 % 38.99/27.79 %Background operators: % 38.99/27.79 % 38.99/27.79 % 38.99/27.79 %Foreground operators: % 38.99/27.79 tff(uri_rdfs_Datatype, type, uri_rdfs_Datatype: $i). % 38.99/27.79 tff(uri_rdfs_ContainerMembershipProperty, type, uri_rdfs_ContainerMembershipProperty: $i). % 38.99/27.79 tff(uri_rdfs_Resource, type, uri_rdfs_Resource: $i). % 38.99/27.79 tff(uri_rdf_Property, type, uri_rdf_Property: $i). % 38.99/27.79 tff(uri_rdf_subject, type, uri_rdf_subject: $i). % 38.99/27.79 tff(uri_rdf_type, type, uri_rdf_type: $i). % 38.99/27.79 tff(uri_owl_onProperty, type, uri_owl_onProperty: $i). % 38.99/27.79 tff(uri_rdfs_subPropertyOf, type, uri_rdfs_subPropertyOf: $i). % 38.99/27.79 tff(literal_typed, type, literal_typed: ($i * $i) > $i). % 38.99/27.79 tff(uri_rdfs_seeAlso, type, uri_rdfs_seeAlso: $i). % 38.99/27.79 tff(icext, type, icext: ($i * $i) > $i). % 38.99/27.79 tff(uri_rdfs_range, type, uri_rdfs_range: $i). % 38.99/27.79 tff(uri_rdf_XMLLiteral, type, uri_rdf_XMLLiteral: $i). % 38.99/27.79 tff(uri_rdf_List, type, uri_rdf_List: $i). % 38.99/27.79 tff(uri_rdf_first, type, uri_rdf_first: $i). % 38.99/27.79 tff(uri_rdf_predicate, type, uri_rdf_predicate: $i). % 38.99/27.79 tff(tuple, type, tuple: ($i * $i) > $i). % 38.99/27.79 tff(ir, type, ir: $i > $i). % 38.99/27.79 tff(uri_ex_Person, type, uri_ex_Person: $i). % 38.99/27.79 tff(lv, type, lv: $i > $i). % 38.99/27.79 tff(uri_ex_bob, type, uri_ex_bob: $i). % 38.99/27.79 tff(uri_rdf__3, type, uri_rdf__3: $i). % 38.99/27.79 tff(uri_rdf_value, type, uri_rdf_value: $i). % 38.99/27.79 tff(ic, type, ic: $i > $i). % 38.99/27.79 tff(uri_rdfs_Statement, type, uri_rdfs_Statement: $i). % 38.99/27.79 tff(uri_ex_hasAncestor, type, uri_ex_hasAncestor: $i). % 38.99/27.79 tff(uri_rdf__1, type, uri_rdf__1: $i). % 38.99/27.79 tff(uri_owl_TransitiveProperty, type, uri_owl_TransitiveProperty: $i). % 38.99/27.79 tff(iext, type, iext: ($i * $i * $i) > $i). % 38.99/27.79 tff(uri_owl_Restriction, type, uri_owl_Restriction: $i). % 38.99/27.79 tff(uri_ex_alice, type, uri_ex_alice: $i). % 38.99/27.79 tff(uri_rdf_rest, type, uri_rdf_rest: $i). % 38.99/27.79 tff(uri_rdfs_label, type, uri_rdfs_label: $i). % 38.99/27.79 tff(uri_rdfs_Container, type, uri_rdfs_Container: $i). % 38.99/27.79 tff(uri_rdfs_subClassOf, type, uri_rdfs_subClassOf: $i). % 38.99/27.79 tff(uri_rdf_object, type, uri_rdf_object: $i). % 38.99/27.79 tff(ip, type, ip: $i > $i). % 38.99/27.79 tff(uri_rdfs_Class, type, uri_rdfs_Class: $i). % 38.99/27.79 tff(uri_rdfs_Seq, type, uri_rdfs_Seq: $i). % 38.99/27.79 tff(dat_str_1, type, dat_str_1: $i). % 38.99/27.79 tff(uri_rdfs_member, type, uri_rdfs_member: $i). % 38.99/27.79 tff(uri_rdf_Bag, type, uri_rdf_Bag: $i). % 38.99/27.79 tff(uri_rdf__2, type, uri_rdf__2: $i). % 38.99/27.79 tff(uri_rdfs_comment, type, uri_rdfs_comment: $i). % 38.99/27.79 tff(uri_rdfs_Literal, type, uri_rdfs_Literal: $i). % 38.99/27.79 tff(true, type, true: $i). % 38.99/27.79 tff(uri_xsd_nonNegativeInteger, type, uri_xsd_nonNegativeInteger: $i). % 38.99/27.79 tff(uri_rdf_Alt, type, uri_rdf_Alt: $i). % 38.99/27.79 tff(uri_rdf_nil, type, uri_rdf_nil: $i). % 38.99/27.79 tff(uri_owl_minCardinality, type, uri_owl_minCardinality: $i). % 38.99/27.79 tff(uri_rdfs_isDefinedBy, type, uri_rdfs_isDefinedBy: $i). % 38.99/27.79 tff(uri_rdfs_domain, type, uri_rdfs_domain: $i). % 38.99/27.79 tff(ifeq, type, ifeq: ($i * $i * $i * $i) > $i). % 38.99/27.79 tff(sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, type, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z: $i). % 38.99/27.79 % 38.99/27.79 %Saturated clause set: % 38.99/27.79 tff(c_16027, 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))). % 38.99/27.79 tff(c_15622, 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))). % 38.99/27.79 tff(c_15625, 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))). % 38.99/27.79 tff(c_83122, plain, (![X_1356, Y_1357]: (ifeq(iext(uri_rdf_predicate, X_1356, Y_1357), true, iext(uri_rdf_predicate, X_1356, Y_1357), true)=true))). % 38.99/27.79 tff(c_83094, plain, (![X_1352, Y_1353]: (ifeq(iext(uri_rdfs_comment, X_1352, Y_1353), true, iext(uri_rdfs_comment, X_1352, Y_1353), true)=true))). % 38.99/27.79 tff(c_83067, plain, (![X_1348, Y_1349]: (ifeq(iext(uri_rdfs_label, X_1348, Y_1349), true, iext(uri_rdfs_label, X_1348, Y_1349), true)=true))). % 38.99/27.79 tff(c_15940, 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))). % 38.99/27.79 tff(c_16901, 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))). % 38.99/27.79 tff(c_15875, 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))). % 38.99/27.79 tff(c_15568, 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))). % 38.99/27.79 tff(c_5488, 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))). % 38.99/27.79 tff(c_15468, 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))). % 38.99/27.79 tff(c_82272, plain, (![X_1337, Y_1338]: (ifeq(iext(uri_rdfs_member, X_1337, Y_1338), true, iext(uri_rdfs_member, X_1337, Y_1338), true)=true))). % 38.99/27.79 tff(c_5485, 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))). % 38.99/27.79 tff(c_15806, 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))). % 38.99/27.79 tff(c_81691, plain, (![C_1332]: (ifeq(iext(uri_rdfs_subClassOf, C_1332, uri_owl_TransitiveProperty), true, iext(uri_rdfs_subClassOf, C_1332, uri_rdfs_Resource), true)=true))). % 38.99/27.79 tff(c_81520, plain, (![C_1330]: (ifeq(iext(uri_rdfs_subClassOf, C_1330, uri_rdfs_Statement), true, iext(uri_rdfs_subClassOf, C_1330, uri_rdfs_Resource), true)=true))). % 38.99/27.79 tff(c_81349, plain, (![C_1328]: (ifeq(iext(uri_rdfs_subClassOf, C_1328, uri_owl_Restriction), true, iext(uri_rdfs_subClassOf, C_1328, uri_rdfs_Resource), true)=true))). % 38.99/27.79 tff(c_17302, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_owl_Restriction, uri_rdfs_Resource), true, true, true), true)=true))). % 38.99/27.79 tff(c_14822, 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))). % 38.99/27.79 tff(c_15110, 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))). % 38.99/27.79 tff(c_17522, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_owl_Restriction, uri_owl_Restriction), true, true, true), true)=true))). % 38.99/27.79 tff(c_15401, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_owl_TransitiveProperty, uri_owl_TransitiveProperty), true, true, true), true)=true))). % 38.99/27.79 tff(c_15306, 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))). % 38.99/27.79 tff(c_14626, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_owl_TransitiveProperty, uri_rdfs_Resource), true, true, true), true)=true))). % 38.99/27.79 tff(c_80280, plain, (![C_1319]: (ifeq(iext(uri_rdfs_subClassOf, C_1319, uri_rdf_List), true, iext(uri_rdfs_subClassOf, C_1319, uri_rdfs_Resource), true)=true))). % 38.99/27.80 tff(c_15044, 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))). % 38.99/27.80 tff(c_13360, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_owl_onProperty), true, true, true), true)=true))). % 38.99/27.80 tff(c_14280, 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))). % 38.99/27.80 tff(c_14328, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_ex_Person, uri_rdfs_Class), true, true, true), true)=true))). % 38.99/27.80 tff(c_14232, 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))). % 38.99/27.80 tff(c_14083, 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))). % 38.99/27.80 tff(c_14379, 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))). % 38.99/27.80 tff(c_10103, 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))). % 38.99/27.80 tff(c_11244, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_ex_hasAncestor), true, true, true), true)=true))). % 38.99/27.80 tff(c_5628, 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))). % 38.99/27.80 tff(c_10100, 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))). % 38.99/27.80 tff(c_14181, 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))). % 38.99/27.80 tff(c_13363, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_owl_onProperty, Y_21), true, true, true), true)=true))). % 38.99/27.80 tff(c_14427, 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))). % 38.99/27.80 tff(c_14007, 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))). % 39.17/27.80 tff(c_8729, 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))). % 39.17/27.80 tff(c_14500, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, uri_rdfs_Class), true, true, true), true)=true))). % 39.17/27.80 tff(c_11718, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_owl_minCardinality), true, true, true), true)=true))). % 39.17/27.80 tff(c_14548, 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))). % 39.17/27.80 tff(c_11721, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_owl_minCardinality, Y_21), true, true, true), true)=true))). % 39.17/27.80 tff(c_13960, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_ex_alice, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z), true, true, true), true)=true))). % 39.17/27.80 tff(c_11247, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_ex_hasAncestor, Y_21), true, true, true), true)=true))). % 39.17/27.80 tff(c_13913, 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))). % 39.17/27.80 tff(c_8732, 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))). % 39.17/27.80 tff(c_5625, 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))). % 39.17/27.80 tff(c_14132, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_ex_bob, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z), true, true, true), true)=true))). % 39.17/27.80 tff(c_16798, 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))). % 39.17/27.80 tff(c_13811, 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))). % 39.17/27.80 tff(c_13544, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_owl_TransitiveProperty, uri_rdfs_Class), true, true, true), true)=true))). % 39.17/27.80 tff(c_13691, 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))). % 39.17/27.80 tff(c_17255, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_owl_Restriction, uri_rdfs_Class), true, true, true), true)=true))). % 39.17/27.80 tff(c_13591, 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))). % 39.17/27.80 tff(c_13738, 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))). % 39.17/27.80 tff(c_12935, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_ex_hasAncestor, uri_ex_hasAncestor), true, true, true), true)=true))). % 39.17/27.80 tff(c_10603, 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))). % 39.17/27.80 tff(c_8983, 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))). % 39.17/27.80 tff(c_75457, plain, (![C_1269]: (ifeq(iext(uri_rdfs_subClassOf, C_1269, uri_rdf_Bag), true, iext(uri_rdfs_subClassOf, C_1269, uri_rdfs_Resource), true)=true))). % 39.17/27.80 tff(c_75277, plain, (![C_1267]: (ifeq(iext(uri_rdfs_subClassOf, C_1267, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z), true, iext(uri_rdfs_subClassOf, C_1267, uri_rdfs_Resource), true)=true))). % 39.17/27.80 tff(c_4564, 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))). % 39.17/27.80 tff(c_4412, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z), true, true, true), true)=true))). % 39.17/27.80 tff(c_4613, 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))). % 39.17/27.80 tff(c_74676, plain, (![C_1259]: (ifeq(iext(uri_rdfs_subClassOf, C_1259, uri_rdfs_Datatype), true, iext(uri_rdfs_subClassOf, C_1259, uri_rdfs_Resource), true)=true))). % 39.17/27.80 tff(c_8489, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_ex_Person, uri_ex_Person), true, true, true), true)=true))). % 39.17/27.80 tff(c_74379, plain, (![C_1256]: (ifeq(iext(uri_rdfs_subClassOf, C_1256, uri_rdfs_ContainerMembershipProperty), true, iext(uri_rdfs_subClassOf, C_1256, uri_rdfs_Resource), true)=true))). % 39.17/27.80 tff(c_13306, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_owl_onProperty, uri_rdf_Property), true, true, true), true)=true))). % 39.17/27.80 tff(c_8559, 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))). % 39.17/27.80 tff(c_9895, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_owl_onProperty, uri_owl_onProperty), true, true, true), true)=true))). % 39.17/27.80 tff(c_12352, 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))). % 39.17/27.80 tff(c_73705, plain, (![C_1250]: (ifeq(iext(uri_rdfs_subClassOf, C_1250, uri_ex_Person), true, iext(uri_rdfs_subClassOf, C_1250, uri_rdfs_Resource), true)=true))). % 39.17/27.80 tff(c_73510, plain, (![C_1248]: (ifeq(iext(uri_rdfs_subClassOf, C_1248, uri_rdfs_Container), true, iext(uri_rdfs_subClassOf, C_1248, uri_rdfs_Resource), true)=true))). % 39.17/27.80 tff(c_11959, 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))). % 39.17/27.80 tff(c_9829, 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))). % 39.17/27.80 tff(c_7048, 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))). % 39.17/27.80 tff(c_9688, 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))). % 39.17/27.80 tff(c_7985, 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))). % 39.17/27.80 tff(c_72696, plain, (![C_1241]: (ifeq(iext(uri_rdfs_subClassOf, C_1241, uri_rdfs_Literal), true, iext(uri_rdfs_subClassOf, C_1241, uri_rdfs_Resource), true)=true))). % 39.17/27.80 tff(c_4514, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, uri_ex_Person), true, true, true), true)=true))). % 39.17/27.80 tff(c_71948, plain, (![X_1235, Y_1236]: (ifeq(iext(uri_rdfs_subPropertyOf, X_1235, Y_1236), true, iext(uri_rdfs_subPropertyOf, X_1235, Y_1236), true)=true))). % 39.17/27.80 tff(c_8223, 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))). % 39.17/27.80 tff(c_12042, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_owl_minCardinality, uri_owl_minCardinality), true, true, true), true)=true))). % 39.17/27.80 tff(c_4660, 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))). % 39.17/27.80 tff(c_71381, plain, (![C_1229]: (ifeq(iext(uri_rdfs_subClassOf, C_1229, uri_rdfs_Class), true, iext(uri_rdfs_subClassOf, C_1229, uri_rdfs_Resource), true)=true))). % 39.17/27.81 tff(c_4462, 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))). % 39.17/27.81 tff(c_11193, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_ex_hasAncestor, uri_rdf_Property), true, true, true), true)=true))). % 39.17/27.81 tff(c_70776, plain, (![X_1220, Y_1221]: (ifeq(iext(uri_rdf_subject, X_1220, Y_1221), true, iext(uri_rdf_subject, X_1220, Y_1221), true)=true))). % 39.17/27.81 tff(c_70001, plain, (![X_1216, Y_1217]: (ifeq(iext(uri_rdfs_subClassOf, X_1216, Y_1217), true, iext(uri_rdfs_subClassOf, X_1216, Y_1217), true)=true))). % 39.17/27.81 tff(c_69940, plain, (![X_1211, Y_1212]: (ifeq(iext(uri_rdfs_isDefinedBy, X_1211, Y_1212), true, iext(uri_rdfs_isDefinedBy, X_1211, Y_1212), true)=true))). % 39.17/27.81 tff(c_69907, plain, (![P_1210]: (ifeq(iext(uri_rdfs_subPropertyOf, P_1210, uri_rdf__1), true, iext(uri_rdfs_subPropertyOf, P_1210, uri_rdfs_member), true)=true))). % 39.17/27.81 tff(c_69880, plain, (![X_1206, Y_1207]: (ifeq(iext(uri_rdf__1, X_1206, Y_1207), true, iext(uri_rdf__1, X_1206, Y_1207), true)=true))). % 39.17/27.81 tff(c_69837, plain, (![X_1202, Y_1203]: (ifeq(iext(uri_owl_onProperty, X_1202, Y_1203), true, iext(uri_owl_onProperty, X_1202, Y_1203), true)=true))). % 39.17/27.81 tff(c_6076, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z), true, ifeq(iext(P_18, uri_ex_bob, Y_21), true, true, true), true)=true))). % 39.17/27.81 tff(c_5892, 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))). % 39.17/27.81 tff(c_4657, 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))). % 39.17/27.81 tff(c_9985, 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))). % 39.17/27.81 tff(c_7751, 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))). % 39.17/27.81 tff(c_7170, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, uri_rdfs_Resource), true, true, true), true)=true))). % 39.17/27.81 tff(c_4415, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, Y_21), true, true, true), true)=true))). % 39.17/27.81 tff(c_68485, plain, (![X_1186, Y_1187]: (ifeq(iext(uri_rdf__1, X_1186, Y_1187), true, iext(uri_rdfs_member, X_1186, Y_1187), true)=true))). % 39.17/27.81 tff(c_6118, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z), true, ifeq(iext(P_18, uri_ex_alice, Y_21), true, true, true), true)=true))). % 39.17/27.81 tff(c_6073, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z), true, ifeq(iext(P_28, X_30, uri_ex_bob), true, true, true), true)=true))). % 39.17/27.81 tff(c_9456, 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))). % 39.17/27.81 tff(c_7656, 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))). % 39.17/27.81 tff(c_67374, plain, (![X_1172, Y_1173]: (ifeq(iext(uri_rdf_value, X_1172, Y_1173), true, iext(uri_rdf_value, X_1172, Y_1173), true)=true))). % 39.17/27.81 tff(c_6520, 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))). % 39.17/27.81 tff(c_5574, 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))). % 39.17/27.81 tff(c_11100, 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))). % 39.17/27.81 tff(c_66085, plain, (![X_1159, Y_1160]: (ifeq(iext(uri_rdf__2, X_1159, Y_1160), true, iext(uri_rdfs_member, X_1159, Y_1160), true)=true))). % 39.17/27.81 tff(c_66059, plain, (![X_1155, Y_1156]: (ifeq(iext(uri_rdf__2, X_1155, Y_1156), true, iext(uri_rdf__2, X_1155, Y_1156), true)=true))). % 39.17/27.81 tff(c_10809, 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))). % 39.17/27.81 tff(c_10883, 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))). % 39.17/27.81 tff(c_65406, plain, (![X_1146, Y_1147]: (ifeq(iext(uri_rdfs_seeAlso, X_1146, Y_1147), true, iext(uri_rdfs_seeAlso, X_1146, Y_1147), true)=true))). % 39.17/27.81 tff(c_6872, 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))). % 39.17/27.81 tff(c_13118, 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))). % 39.17/27.81 tff(c_4561, 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))). % 39.17/27.81 tff(c_8678, 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))). % 39.17/27.81 tff(c_10969, 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))). % 39.17/27.81 tff(c_4921, 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))). % 39.17/27.81 tff(c_7389, 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))). % 39.17/27.81 tff(c_4459, 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))). % 39.17/27.81 tff(c_4827, 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))). % 39.17/27.81 tff(c_7495, 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))). % 39.17/27.81 tff(c_61929, plain, (![X_1119, Y_1120]: (ifeq(iext(uri_rdf_type, X_1119, Y_1120), true, iext(uri_rdf_type, X_1119, Y_1120), true)=true))). % 39.17/27.81 tff(c_6434, 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))). % 39.17/27.81 tff(c_7587, 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))). % 39.17/27.81 tff(c_9045, 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))). % 39.17/27.81 tff(c_8622, 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))). % 39.17/27.81 tff(c_13025, 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))). % 39.17/27.81 tff(c_6115, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z), true, ifeq(iext(P_28, X_30, uri_ex_alice), true, true, true), true)=true))). % 39.17/27.81 tff(c_6624, 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))). % 39.17/27.81 tff(c_5347, 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))). % 39.17/27.81 tff(c_10255, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_ex_Person, uri_rdfs_Resource), true, true, true), true)=true))). % 39.17/27.81 tff(c_7824, 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))). % 39.17/27.81 tff(c_7917, 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))). % 39.17/27.81 tff(c_60515, plain, (![X_1103, Y_1104]: (ifeq(iext(uri_rdf__3, X_1103, Y_1104), true, iext(uri_rdf__3, X_1103, Y_1104), true)=true))). % 39.17/27.81 tff(c_60344, plain, (![C_1101]: (ifeq(iext(uri_rdfs_subClassOf, C_1101, uri_rdf_Alt), true, iext(uri_rdfs_subClassOf, C_1101, uri_rdfs_Resource), true)=true))). % 39.17/27.81 tff(c_60165, plain, (![C_1099]: (ifeq(iext(uri_rdfs_subClassOf, C_1099, uri_rdf_Property), true, iext(uri_rdfs_subClassOf, C_1099, uri_rdfs_Resource), true)=true))). % 39.17/27.81 tff(c_4872, 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))). % 39.17/27.81 tff(c_11893, 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))). % 39.17/27.81 tff(c_4771, 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))). % 39.17/27.81 tff(c_8423, 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))). % 39.17/27.81 tff(c_9550, 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))). % 39.17/27.81 tff(c_59431, plain, (![P_1090]: (ifeq(iext(uri_rdfs_subPropertyOf, P_1090, uri_rdf__2), true, iext(uri_rdfs_subPropertyOf, P_1090, uri_rdfs_member), true)=true))). % 39.17/27.81 tff(c_6365, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z), true, true, true), true)=true))). % 39.17/27.81 tff(c_4824, 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))). % 39.17/27.81 tff(c_58182, plain, (![C_1080]: (ifeq(iext(uri_rdfs_subClassOf, C_1080, uri_rdf_XMLLiteral), true, iext(uri_rdfs_subClassOf, C_1080, uri_rdfs_Resource), true)=true))). % 39.17/27.81 tff(c_58058, plain, (![X_1075, Y_1076]: (ifeq(iext(uri_rdf__3, X_1075, Y_1076), true, iext(uri_rdfs_member, X_1075, Y_1076), true)=true))). % 39.17/27.81 tff(c_4610, 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))). % 39.17/27.81 tff(c_4924, 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))). % 39.17/27.81 tff(c_57451, plain, (![X_1067, Y_1068]: (ifeq(iext(uri_rdfs_range, X_1067, Y_1068), true, iext(uri_rdfs_range, X_1067, Y_1068), true)=true))). % 39.17/27.81 tff(c_57425, plain, (![X_1063, Y_1064]: (ifeq(iext(uri_rdf_rest, X_1063, Y_1064), true, iext(uri_rdf_rest, X_1063, Y_1064), true)=true))). % 39.17/27.81 tff(c_4517, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, uri_ex_Person, Y_21), true, true, true), true)=true))). % 39.17/27.81 tff(c_57256, plain, (![X_1057, Y_1058]: (ifeq(iext(uri_rdf_first, X_1057, Y_1058), true, iext(uri_rdf_first, X_1057, Y_1058), true)=true))). % 39.17/27.81 tff(c_56924, plain, (![X_1053, Y_1054]: (ifeq(iext(uri_rdfs_domain, X_1053, Y_1054), true, iext(uri_rdfs_domain, X_1053, Y_1054), true)=true))). % 39.17/27.81 tff(c_56754, plain, (![C_1051]: (ifeq(iext(uri_rdfs_subClassOf, C_1051, uri_rdfs_Seq), true, iext(uri_rdfs_subClassOf, C_1051, uri_rdfs_Resource), true)=true))). % 39.17/27.81 tff(c_9356, 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))). % 39.17/27.81 tff(c_55729, plain, (![X_1040, Y_1041]: (ifeq(iext(uri_rdf_object, X_1040, Y_1041), true, iext(uri_rdf_object, X_1040, Y_1041), true)=true))). % 39.17/27.81 tff(c_4774, 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))). % 39.17/27.81 tff(c_11667, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_owl_minCardinality, uri_rdf_Property), true, true, true), true)=true))). % 39.17/27.82 tff(c_11422, 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))). % 39.17/27.82 tff(c_12104, 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))). % 39.17/27.82 tff(c_4869, 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))). % 39.17/27.82 tff(c_10049, 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))). % 39.17/27.82 tff(c_54897, plain, (![X_1028, Y_1029]: (ifeq(iext(uri_owl_minCardinality, X_1028, Y_1029), true, iext(uri_owl_minCardinality, X_1028, Y_1029), true)=true))). % 39.17/27.82 tff(c_8285, 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))). % 39.17/27.82 tff(c_4716, 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))). % 39.17/27.82 tff(c_53512, plain, (![X_1014, Y_1015]: (ifeq(iext(uri_ex_hasAncestor, X_1014, Y_1015), true, iext(uri_ex_hasAncestor, X_1014, Y_1015), true)=true))). % 39.17/27.82 tff(c_4719, 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))). % 39.17/27.82 tff(c_53194, plain, (![P_1009]: (ifeq(iext(uri_rdfs_subPropertyOf, P_1009, uri_rdf__3), true, iext(uri_rdfs_subPropertyOf, P_1009, uri_rdfs_member), true)=true))). % 39.17/27.82 tff(c_11612, 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))). % 39.17/27.82 tff(c_16617, 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))). % 39.17/27.82 tff(c_8792, 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))). % 39.17/27.82 tff(c_8795, 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))). % 39.17/27.82 tff(c_5028, plain, (![P_47, X_135]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, X_135, uri_rdfs_Resource), true, true, true), true)=true))). % 39.17/27.82 tff(c_7237, 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))). % 39.17/27.82 tff(c_7240, 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))). % 39.17/27.82 tff(c_16620, 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))). % 39.17/27.82 tff(c_16997, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, uri_owl_Restriction, Y_21), true, true, true), true)=true))). % 39.17/27.82 tff(c_12535, 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))). % 39.17/27.82 tff(c_12420, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, uri_owl_TransitiveProperty, Y_21), true, true, true), true)=true))). % 39.17/27.82 tff(c_6230, 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))). % 39.17/27.82 tff(c_8076, 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))). % 39.17/27.82 tff(c_6227, 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))). % 39.17/27.82 tff(c_16994, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, uri_owl_Restriction), true, true, true), true)=true))). % 39.17/27.82 tff(c_10429, 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))). % 39.17/27.82 tff(c_9211, 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))). % 39.17/27.82 tff(c_12417, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, uri_owl_TransitiveProperty), true, true, true), true)=true))). % 39.17/27.82 tff(c_12538, 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))). % 39.17/27.82 tff(c_9208, 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))). % 39.17/27.82 tff(c_8073, 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))). % 39.17/27.82 tff(c_10432, 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))). % 39.17/27.82 tff(c_4198, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_ex_Person), true, ifeq(iext(P_18, uri_ex_bob, Y_21), true, true, true), true)=true))). % 39.17/27.82 tff(c_3784, 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))). % 39.17/27.82 tff(c_3690, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_owl_Restriction), true, ifeq(iext(P_28, X_30, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z), true, true, true), true)=true))). % 39.17/27.82 tff(c_4081, 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))). % 39.17/27.82 tff(c_4006, 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))). % 39.17/27.82 tff(c_3883, 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))). % 39.17/27.82 tff(c_3693, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_owl_Restriction), true, ifeq(iext(P_18, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, Y_21), true, true, true), true)=true))). % 39.17/27.82 tff(c_3619, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_ex_Person), true, ifeq(iext(P_18, uri_ex_alice, Y_21), true, true, true), true)=true))). % 39.17/27.82 tff(c_3727, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_owl_TransitiveProperty), true, ifeq(iext(P_28, X_30, uri_ex_hasAncestor), true, true, true), true)=true))). % 39.17/27.82 tff(c_3919, 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))). % 39.17/27.82 tff(c_4239, 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))). % 39.17/27.82 tff(c_3781, 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))). % 39.17/27.82 tff(c_3880, 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))). % 39.17/27.82 tff(c_3656, 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))). % 39.17/27.82 tff(c_4368, 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))). % 39.17/27.82 tff(c_4118, 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))). % 39.17/27.82 tff(c_4242, 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))). % 39.17/27.82 tff(c_4371, 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))). % 39.17/27.82 tff(c_4043, 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))). % 39.17/27.82 tff(c_3653, 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))). % 39.17/27.82 tff(c_3964, 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))). % 39.17/27.82 tff(c_4121, 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))). % 39.17/27.82 tff(c_3616, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_ex_Person), true, ifeq(iext(P_28, X_30, uri_ex_alice), true, true, true), true)=true))). % 39.17/27.82 tff(c_3843, 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))). % 39.17/27.82 tff(c_4003, 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))). % 39.17/27.82 tff(c_4325, 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))). % 39.17/27.82 tff(c_4161, 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))). % 39.17/27.82 tff(c_4283, 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))). % 39.17/27.82 tff(c_3922, 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))). % 39.17/27.82 tff(c_4328, 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))). % 39.17/27.82 tff(c_3846, 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))). % 39.17/27.82 tff(c_3730, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_owl_TransitiveProperty), true, ifeq(iext(P_18, uri_ex_hasAncestor, Y_21), true, true, true), true)=true))). % 39.17/27.82 tff(c_2654, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_owl_minCardinality), true, ifeq(iext(P_108, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, literal_typed(dat_str_1, uri_xsd_nonNegativeInteger)), true, true, true), true)=true))). % 39.17/27.82 tff(c_4040, 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))). % 39.17/27.82 tff(c_3967, 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))). % 39.17/27.82 tff(c_4158, 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))). % 39.17/27.82 tff(c_4195, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_ex_Person), true, ifeq(iext(P_28, X_30, uri_ex_bob), true, true, true), true)=true))). % 39.17/27.82 tff(c_4286, 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))). % 39.17/27.82 tff(c_4078, 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))). % 39.17/27.82 tff(c_1719, plain, (![P_94, X_62, Y_97]: (ifeq(iext(uri_rdfs_domain, P_94, uri_rdfs_Resource), true, ifeq(iext(P_94, X_62, Y_97), true, true, true), true)=true))). % 39.17/27.82 tff(c_2096, plain, (![P_98, X_100, X_62]: (ifeq(iext(uri_rdfs_range, P_98, uri_rdfs_Resource), true, ifeq(iext(P_98, X_100, X_62), true, true, true), true)=true))). % 39.17/27.82 tff(c_2786, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_domain), true, ifeq(iext(P_108, uri_rdfs_range, uri_rdf_Property), true, true, true), true)=true))). % 39.17/27.82 tff(c_2909, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_subPropertyOf), true, ifeq(iext(P_108, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso), true, true, true), true)=true))). % 39.17/27.82 tff(c_42813, plain, (![P_879]: (ifeq(iext(uri_rdfs_subPropertyOf, P_879, uri_rdfs_isDefinedBy), true, iext(uri_rdfs_subPropertyOf, P_879, uri_rdfs_seeAlso), true)=true))). % 39.17/27.82 tff(c_2708, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_range), true, ifeq(iext(P_108, uri_rdf_type, uri_rdfs_Class), true, true, true), true)=true))). % 39.17/27.82 tff(c_2834, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_range), true, ifeq(iext(P_108, uri_rdf__2, uri_rdfs_Resource), true, true, true), true)=true))). % 39.17/27.82 tff(c_2816, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_domain), true, ifeq(iext(P_108, uri_rdfs_comment, uri_rdfs_Resource), true, true, true), true)=true))). % 39.17/27.82 tff(c_2762, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_range), true, ifeq(iext(P_108, uri_rdfs_range, uri_rdfs_Class), true, true, true), true)=true))). % 39.17/27.82 tff(c_2900, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_domain), true, ifeq(iext(P_108, uri_rdfs_subClassOf, uri_rdfs_Class), true, true, true), true)=true))). % 39.17/27.82 tff(c_2672, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_ex_hasAncestor), true, ifeq(iext(P_108, uri_ex_alice, uri_ex_bob), true, true, true), true)=true))). % 39.17/27.82 tff(c_2945, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_subClassOf), true, ifeq(iext(P_108, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property), true, true, true), true)=true))). % 39.17/27.82 tff(c_2792, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_domain), true, ifeq(iext(P_108, uri_rdf_subject, uri_rdfs_Statement), true, true, true), true)=true))). % 39.17/27.82 tff(c_2969, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_range), true, ifeq(iext(P_108, uri_rdf_predicate, uri_rdfs_Resource), true, true, true), true)=true))). % 39.17/27.82 tff(c_3011, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_subClassOf), true, ifeq(iext(P_108, uri_rdf_Alt, uri_rdfs_Container), true, true, true), true)=true))). % 39.17/27.82 tff(c_2732, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdf_type), true, ifeq(iext(P_108, uri_rdf__1, uri_rdf_Property), true, true, true), true)=true))). % 39.17/27.82 tff(c_41361, plain, (![C_866]: (ifeq(iext(uri_rdfs_subClassOf, C_866, uri_rdfs_Datatype), true, iext(uri_rdfs_subClassOf, C_866, uri_rdfs_Class), true)=true))). % 39.17/27.82 tff(c_41311, plain, (![C_864]: (ifeq(iext(uri_rdfs_subClassOf, C_864, uri_rdfs_ContainerMembershipProperty), true, iext(uri_rdfs_subClassOf, C_864, uri_rdf_Property), true)=true))). % 39.17/27.82 tff(c_2768, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdf_type), true, ifeq(iext(P_108, uri_rdf_XMLLiteral, uri_rdfs_Datatype), true, true, true), true)=true))). % 39.17/27.82 tff(c_2744, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_domain), true, ifeq(iext(P_108, uri_rdf_first, uri_rdf_List), true, true, true), true)=true))). % 39.17/27.82 tff(c_2957, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_range), true, ifeq(iext(P_108, uri_rdf_value, uri_rdfs_Resource), true, true, true), true)=true))). % 39.17/27.82 tff(c_2951, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_domain), true, ifeq(iext(P_108, uri_rdf__2, uri_rdfs_Resource), true, true, true), true)=true))). % 39.17/27.82 tff(c_2720, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdf_type), true, ifeq(iext(P_108, uri_rdf__3, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 39.17/27.82 tff(c_2774, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdf_type), true, ifeq(iext(P_108, uri_rdf_Property, uri_rdfs_Class), true, true, true), true)=true))). % 39.17/27.82 tff(c_2963, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdf_type), true, ifeq(iext(P_108, uri_rdf_value, uri_rdf_Property), true, true, true), true)=true))). % 39.17/27.83 tff(c_3023, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_range), true, ifeq(iext(P_108, uri_rdfs_member, uri_rdfs_Resource), true, true, true), true)=true))). % 39.17/27.83 tff(c_2714, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdf_type), true, ifeq(iext(P_108, uri_rdf_object, uri_rdf_Property), true, true, true), true)=true))). % 39.17/27.83 tff(c_2846, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_range), true, ifeq(iext(P_108, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true, true, true), true)=true))). % 39.17/27.83 tff(c_2858, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_range), true, ifeq(iext(P_108, uri_rdf__3, uri_rdfs_Resource), true, true, true), true)=true))). % 39.17/27.83 tff(c_2993, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdf_type), true, ifeq(iext(P_108, uri_rdf_type, uri_rdf_Property), true, true, true), true)=true))). % 39.17/27.83 tff(c_39738, plain, (![X_848, Y_849]: (ifeq(iext(uri_rdfs_isDefinedBy, X_848, Y_849), true, iext(uri_rdfs_seeAlso, X_848, Y_849), true)=true))). % 39.17/27.83 tff(c_2678, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_range), true, ifeq(iext(P_108, uri_rdfs_subClassOf, uri_rdfs_Class), true, true, true), true)=true))). % 39.17/27.83 tff(c_2804, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_domain), true, ifeq(iext(P_108, uri_rdf_type, uri_rdfs_Resource), true, true, true), true)=true))). % 39.17/27.83 tff(c_2894, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdf_type), true, ifeq(iext(P_108, uri_rdf__3, uri_rdf_Property), true, true, true), true)=true))). % 39.17/27.83 tff(c_2756, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdf_type), true, ifeq(iext(P_108, uri_rdf__1, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 39.17/27.83 tff(c_2750, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_range), true, ifeq(iext(P_108, uri_rdfs_label, uri_rdfs_Literal), true, true, true), true)=true))). % 39.17/27.83 tff(c_39053, plain, (![C_841]: (ifeq(iext(uri_rdfs_subClassOf, C_841, uri_ex_Person), true, iext(uri_rdfs_subClassOf, C_841, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z), true)=true))). % 39.17/27.83 tff(c_2810, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_domain), true, ifeq(iext(P_108, uri_rdfs_member, uri_rdfs_Resource), true, true, true), true)=true))). % 39.17/27.83 tff(c_3041, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_range), true, ifeq(iext(P_108, uri_rdfs_subPropertyOf, uri_rdf_Property), true, true, true), true)=true))). % 39.17/27.83 tff(c_2870, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdf_type), true, ifeq(iext(P_108, uri_rdf__2, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 39.17/27.83 tff(c_2666, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdf_type), true, ifeq(iext(P_108, uri_rdf_nil, uri_rdf_List), true, true, true), true)=true))). % 39.17/27.83 tff(c_2981, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_range), true, ifeq(iext(P_108, uri_rdf_rest, uri_rdf_List), true, true, true), true)=true))). % 39.17/27.83 tff(c_3035, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_domain), true, ifeq(iext(P_108, uri_rdf_object, uri_rdfs_Statement), true, true, true), true)=true))). % 39.17/27.83 tff(c_2927, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_range), true, ifeq(iext(P_108, uri_rdf_first, uri_rdfs_Resource), true, true, true), true)=true))). % 39.17/27.83 tff(c_3017, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_subClassOf), true, ifeq(iext(P_108, uri_rdfs_Datatype, uri_rdfs_Class), true, true, true), true)=true))). % 39.17/27.83 tff(c_3053, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_subClassOf), true, ifeq(iext(P_108, uri_ex_Person, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z), true, true, true), true)=true))). % 39.17/27.83 tff(c_37720, plain, (![C_829]: (ifeq(iext(uri_rdfs_subClassOf, C_829, uri_rdf_XMLLiteral), true, iext(uri_rdfs_subClassOf, C_829, uri_rdfs_Literal), true)=true))). % 39.17/27.83 tff(c_3047, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_owl_onProperty), true, ifeq(iext(P_108, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, uri_ex_hasAncestor), true, true, true), true)=true))). % 39.17/27.83 tff(c_37654, plain, (![D_827]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_827), true, icext(D_827, uri_rdfs_member), true)=true))). % 39.17/27.83 tff(c_37587, plain, (![D_825]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_825), true, icext(D_825, uri_rdfs_Resource), true)=true))). % 39.17/27.83 tff(c_2738, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_domain), true, ifeq(iext(P_108, uri_rdf_rest, uri_rdf_List), true, true, true), true)=true))). % 39.17/27.83 tff(c_37392, plain, (![D_822]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_822), true, icext(D_822, uri_owl_minCardinality), true)=true))). % 39.17/27.83 tff(c_37326, plain, (![D_820]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_820), true, icext(D_820, uri_rdfs_isDefinedBy), true)=true))). % 39.17/27.83 tff(c_37259, plain, (![D_818]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_818), true, icext(D_818, uri_owl_onProperty), true)=true))). % 39.17/27.83 tff(c_2852, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_domain), true, ifeq(iext(P_108, uri_rdf__1, uri_rdfs_Resource), true, true, true), true)=true))). % 39.17/27.83 tff(c_37051, plain, (![D_815]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_815), true, icext(D_815, uri_ex_hasAncestor), true)=true))). % 39.17/27.83 tff(c_36985, plain, (![D_813]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_813), true, icext(D_813, uri_rdfs_subPropertyOf), true)=true))). % 39.17/27.83 tff(c_36919, plain, (![D_811]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_811), true, icext(D_811, uri_rdfs_range), true)=true))). % 39.17/27.83 tff(c_36852, plain, (![D_809]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_809), true, icext(D_809, uri_rdfs_Seq), true)=true))). % 39.17/27.83 tff(c_36786, plain, (![D_807]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_807), true, icext(D_807, uri_rdfs_Container), true)=true))). % 39.17/27.83 tff(c_36718, plain, (![C_805]: (ifeq(iext(uri_rdfs_subClassOf, C_805, uri_rdf_Alt), true, iext(uri_rdfs_subClassOf, C_805, uri_rdfs_Container), true)=true))). % 39.17/27.83 tff(c_36643, plain, (![D_803]: (ifeq(iext(uri_rdfs_subClassOf, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, D_803), true, icext(D_803, uri_ex_alice), true)=true))). % 39.17/27.83 tff(c_36575, plain, (![D_801]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_801), true, icext(D_801, uri_rdfs_Datatype), true)=true))). % 39.17/27.83 tff(c_36479, plain, (![D_799]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_799), true, icext(D_799, uri_rdfs_Class), true)=true))). % 39.17/27.83 tff(c_36285, plain, (![D_796]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_796), true, icext(D_796, uri_rdf_Alt), true)=true))). % 39.17/27.83 tff(c_3005, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_range), true, ifeq(iext(P_108, uri_rdfs_domain, uri_rdfs_Class), true, true, true), true)=true))). % 39.17/27.83 tff(c_36217, plain, (![D_794]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_794), true, icext(D_794, uri_rdf_Bag), true)=true))). % 39.17/27.83 tff(c_36151, plain, (![D_792]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_792), true, icext(D_792, uri_rdfs_Literal), true)=true))). % 39.17/27.83 tff(c_3029, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_subClassOf), true, ifeq(iext(P_108, uri_rdf_Bag, uri_rdfs_Container), true, true, true), true)=true))). % 39.17/27.83 tff(c_35952, plain, (![D_789]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_789), true, icext(D_789, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z), true)=true))). % 39.17/27.83 tff(c_35878, plain, (![D_787]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_787), true, icext(D_787, uri_rdf_XMLLiteral), true)=true))). % 39.17/27.83 tff(c_35812, plain, (![D_785]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_785), true, icext(D_785, uri_rdfs_ContainerMembershipProperty), true)=true))). % 39.17/27.83 tff(c_35745, plain, (![D_783]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_783), true, icext(D_783, uri_ex_Person), true)=true))). % 39.17/27.83 tff(c_35670, plain, (![D_781]: (ifeq(iext(uri_rdfs_subClassOf, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, D_781), true, icext(D_781, uri_ex_bob), true)=true))). % 39.17/27.83 tff(c_35603, plain, (![C_779]: (ifeq(iext(uri_rdfs_subClassOf, C_779, uri_rdfs_Seq), true, iext(uri_rdfs_subClassOf, C_779, uri_rdfs_Container), true)=true))). % 39.17/27.83 tff(c_35537, plain, (![D_777]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_777), true, icext(D_777, uri_rdfs_label), true)=true))). % 39.17/27.83 tff(c_35471, plain, (![D_775]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_775), true, icext(D_775, uri_rdf_predicate), true)=true))). % 39.17/27.83 tff(c_35405, plain, (![D_773]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_773), true, icext(D_773, uri_rdfs_seeAlso), true)=true))). % 39.17/27.83 tff(c_2822, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_domain), true, ifeq(iext(P_108, uri_rdf__3, uri_rdfs_Resource), true, true, true), true)=true))). % 39.17/27.83 tff(c_35205, plain, (![D_770]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_770), true, icext(D_770, uri_owl_Restriction), true)=true))). % 39.17/27.83 tff(c_35139, plain, (![D_768]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_768), true, icext(D_768, uri_rdfs_Statement), true)=true))). % 39.17/27.83 tff(c_35073, plain, (![D_766]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_766), true, icext(D_766, uri_owl_TransitiveProperty), true)=true))). % 39.17/27.83 tff(c_2864, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_range), true, ifeq(iext(P_108, uri_rdfs_seeAlso, uri_rdfs_Resource), true, true, true), true)=true))). % 39.17/27.83 tff(c_34873, plain, (![D_763]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_763), true, icext(D_763, uri_rdfs_subClassOf), true)=true))). % 39.17/27.83 tff(c_34807, plain, (![D_761]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_761), true, icext(D_761, uri_rdfs_domain), true)=true))). % 39.17/27.83 tff(c_34741, plain, (![D_759]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_759), true, icext(D_759, uri_rdfs_comment), true)=true))). % 39.17/27.83 tff(c_2888, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_range), true, ifeq(iext(P_108, uri_rdf__1, uri_rdfs_Resource), true, true, true), true)=true))). % 39.17/27.83 tff(c_34541, plain, (![D_756]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_756), true, icext(D_756, uri_rdf_List), true)=true))). % 39.17/27.83 tff(c_34475, plain, (![D_754]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_754), true, icext(D_754, uri_rdf_first), true)=true))). % 39.17/27.83 tff(c_16046, 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))). % 39.17/27.83 tff(c_2975, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdf_type), true, ifeq(iext(P_108, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, uri_owl_Restriction), true, true, true), true)=true))). % 39.17/27.83 tff(c_15906, 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))). % 39.17/27.83 tff(c_16932, 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))). % 39.17/27.83 tff(c_15971, 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))). % 39.17/27.83 tff(c_15505, 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))). % 39.17/27.83 tff(c_34110, plain, (![C_742]: (ifeq(iext(uri_rdfs_subClassOf, C_742, uri_rdf_Bag), true, iext(uri_rdfs_subClassOf, C_742, uri_rdfs_Container), true)=true))). % 39.17/27.83 tff(c_15840, 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))). % 39.17/27.83 tff(c_15593, 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))). % 39.17/27.83 tff(c_33991, plain, (![D_737]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_737), true, icext(D_737, uri_rdf_Property), true)=true))). % 39.17/27.83 tff(c_15435, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_owl_TransitiveProperty, uri_owl_TransitiveProperty), true)=true))). % 39.17/27.83 tff(c_15144, 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))). % 39.17/27.83 tff(c_2921, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_domain), true, ifeq(iext(P_108, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true, true, true), true)=true))). % 39.17/27.83 tff(c_15078, 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))). % 39.17/27.83 tff(c_14660, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_owl_TransitiveProperty, uri_rdfs_Resource), true)=true))). % 39.17/27.83 tff(c_14856, 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))). % 39.17/27.83 tff(c_15145, 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))). % 39.17/27.83 tff(c_14661, plain, (![E_41]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, E_41), true, iext(uri_rdfs_subClassOf, uri_owl_TransitiveProperty, E_41), true)=true))). % 39.17/27.83 tff(c_2933, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_domain), true, ifeq(iext(P_108, uri_rdfs_subPropertyOf, uri_rdf_Property), true, true, true), true)=true))). % 39.17/27.83 tff(c_14857, 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))). % 39.17/27.83 tff(c_17556, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_owl_Restriction, uri_owl_Restriction), true)=true))). % 39.17/27.83 tff(c_15340, 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))). % 39.17/27.83 tff(c_33348, plain, (![D_719]: (ifeq(iext(uri_rdfs_subClassOf, uri_owl_TransitiveProperty, D_719), true, icext(D_719, uri_ex_hasAncestor), true)=true))). % 39.17/27.83 tff(c_17336, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_owl_Restriction, uri_rdfs_Resource), true)=true))). % 39.17/27.83 tff(c_17337, plain, (![E_41]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, E_41), true, iext(uri_rdfs_subClassOf, uri_owl_Restriction, E_41), true)=true))). % 39.17/27.83 tff(c_14519, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, uri_rdfs_Class), true)=true))). % 39.17/27.83 tff(c_2684, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_subClassOf), true, ifeq(iext(P_108, uri_rdf_XMLLiteral, uri_rdfs_Literal), true, true, true), true)=true))). % 39.17/27.83 tff(c_14446, 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))). % 39.17/27.83 tff(c_14567, 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))). % 39.17/27.83 tff(c_14200, 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))). % 39.17/27.83 tff(c_33050, plain, (![D_710]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_710), true, icext(D_710, uri_rdf_value), true)=true))). % 39.17/27.83 tff(c_14398, 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))). % 39.17/27.83 tff(c_14026, 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))). % 39.17/27.83 tff(c_14151, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_ex_bob, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z), true)=true))). % 39.17/27.83 tff(c_2939, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdf_type), true, ifeq(iext(P_108, uri_rdf_subject, uri_rdf_Property), true, true, true), true)=true))). % 39.17/27.83 tff(c_13979, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_ex_alice, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z), true)=true))). % 39.17/27.83 tff(c_14251, 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))). % 39.17/27.83 tff(c_14102, 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))). % 39.17/27.83 tff(c_14347, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_ex_Person, uri_rdfs_Class), true)=true))). % 39.17/27.83 tff(c_13932, 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))). % 39.17/27.83 tff(c_14299, 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))). % 39.17/27.83 tff(c_13710, 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))). % 39.17/27.83 tff(c_13616, 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))). % 39.17/27.83 tff(c_2660, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_domain), true, ifeq(iext(P_108, uri_rdf_predicate, uri_rdfs_Statement), true, true, true), true)=true))). % 39.17/27.83 tff(c_13563, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_owl_TransitiveProperty, uri_rdfs_Class), true)=true))). % 39.17/27.83 tff(c_16823, 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))). % 39.17/27.83 tff(c_13757, 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))). % 39.17/27.83 tff(c_32515, plain, (![D_692]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_692), true, icext(D_692, uri_rdf__2), true)=true))). % 39.17/27.83 tff(c_13836, 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))). % 39.17/27.83 tff(c_17274, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_owl_Restriction, uri_rdfs_Class), true)=true))). % 39.17/27.83 tff(c_9723, 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))). % 39.17/27.83 tff(c_2798, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_range), true, ifeq(iext(P_108, uri_rdfs_comment, uri_rdfs_Literal), true, true, true), true)=true))). % 39.17/27.83 tff(c_8523, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_ex_Person, uri_ex_Person), true)=true))). % 39.17/27.84 tff(c_10846, 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))). % 39.17/27.84 tff(c_11218, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_ex_hasAncestor, uri_rdf_Property), true)=true))). % 39.17/27.84 tff(c_7204, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, uri_rdfs_Resource), true)=true))). % 39.17/27.84 tff(c_10017, 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))). % 39.17/27.84 tff(c_6903, 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))). % 39.17/27.84 tff(c_2726, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdf_type), true, ifeq(iext(P_108, uri_ex_bob, uri_ex_Person), true, true, true), true)=true))). % 39.17/27.84 tff(c_12138, 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))). % 39.17/27.84 tff(c_6399, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z), true)=true))). % 39.17/27.84 tff(c_9860, 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))). % 39.17/27.84 tff(c_7079, 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))). % 39.17/27.84 tff(c_7529, 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))). % 39.17/27.84 tff(c_2828, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdf_type), true, ifeq(iext(P_108, uri_ex_hasAncestor, uri_owl_TransitiveProperty), true, true, true), true)=true))). % 39.17/27.84 tff(c_8457, 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))). % 39.17/27.84 tff(c_13152, 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))). % 39.17/27.84 tff(c_8254, 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))). % 39.17/27.84 tff(c_31648, plain, (![D_665]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_665), true, icext(D_665, uri_rdf_subject), true)=true))). % 39.17/27.84 tff(c_9584, 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))). % 39.17/27.84 tff(c_9014, 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))). % 39.17/27.84 tff(c_11003, 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))). % 39.17/27.84 tff(c_2882, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_domain), true, ifeq(iext(P_108, uri_rdfs_domain, uri_rdf_Property), true, true, true), true)=true))). % 39.17/27.84 tff(c_8703, 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))). % 39.17/27.84 tff(c_11637, 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))). % 39.17/27.84 tff(c_7618, 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))). % 39.17/27.84 tff(c_11131, 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))). % 39.17/27.84 tff(c_11456, 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))). % 39.17/27.84 tff(c_2840, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_range), true, ifeq(iext(P_108, uri_rdf_subject, uri_rdfs_Resource), true, true, true), true)=true))). % 39.17/27.84 tff(c_7855, 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))). % 39.17/27.84 tff(c_10290, plain, (![E_41]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, E_41), true, iext(uri_rdfs_subClassOf, uri_ex_Person, E_41), true)=true))). % 39.17/27.84 tff(c_31012, plain, (![D_647]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, D_647), true, icext(D_647, uri_rdf_XMLLiteral), true)=true))). % 39.17/27.84 tff(c_11927, 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))). % 39.17/27.84 tff(c_5923, 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))). % 39.17/27.84 tff(c_2915, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_domain), true, ifeq(iext(P_108, uri_rdfs_label, uri_rdfs_Resource), true, true, true), true)=true))). % 39.17/27.84 tff(c_6555, 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))). % 39.17/27.84 tff(c_30674, plain, (![D_638]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_638), true, icext(D_638, uri_rdf__1), true)=true))). % 39.17/27.84 tff(c_8590, 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))). % 39.17/27.84 tff(c_6554, 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))). % 39.17/27.84 tff(c_2987, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdf_type), true, ifeq(iext(P_108, uri_rdf_rest, uri_rdf_Property), true, true, true), true)=true))). % 39.17/27.84 tff(c_7423, 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))). % 39.17/27.84 tff(c_7951, 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))). % 39.17/27.84 tff(c_6465, 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))). % 39.17/27.84 tff(c_12966, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_ex_hasAncestor, uri_ex_hasAncestor), true)=true))). % 39.17/27.84 tff(c_10638, 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))). % 39.17/27.84 tff(c_8320, 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))). % 39.17/27.84 tff(c_9926, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_owl_onProperty, uri_owl_onProperty), true)=true))). % 39.17/27.84 tff(c_2876, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_domain), true, ifeq(iext(P_108, uri_rdfs_seeAlso, uri_rdfs_Resource), true, true, true), true)=true))). % 39.17/27.84 tff(c_8647, 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))). % 39.17/27.84 tff(c_7424, 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))). % 39.17/27.84 tff(c_9080, 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))). % 39.17/27.84 tff(c_30060, plain, (![D_620]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_620), true, icext(D_620, uri_rdf__3), true)=true))). % 39.17/27.84 tff(c_10914, 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))). % 39.17/27.84 tff(c_2702, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_domain), true, ifeq(iext(P_108, uri_rdf_value, uri_rdfs_Resource), true, true, true), true)=true))). % 39.17/27.84 tff(c_5381, 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))). % 39.17/27.84 tff(c_10637, 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))). % 39.17/27.84 tff(c_6655, 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))). % 39.17/27.84 tff(c_29713, plain, (![D_611]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_611), true, icext(D_611, uri_rdf__1), true)=true))). % 39.17/27.84 tff(c_9490, 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))). % 39.17/27.84 tff(c_2999, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdf_type), true, ifeq(iext(P_108, uri_ex_alice, uri_ex_Person), true, true, true), true)=true))). % 39.17/27.84 tff(c_8019, 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))). % 39.17/27.84 tff(c_11457, 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))). % 39.17/27.84 tff(c_5380, 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))). % 39.17/27.84 tff(c_12073, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_owl_minCardinality, uri_owl_minCardinality), true)=true))). % 39.17/27.84 tff(c_7785, 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))). % 39.17/27.84 tff(c_8319, 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))). % 39.17/27.84 tff(c_2690, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdf_type), true, ifeq(iext(P_108, uri_rdf__2, uri_rdf_Property), true, true, true), true)=true))). % 39.17/27.84 tff(c_11984, 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))). % 39.17/27.84 tff(c_29080, plain, (![D_593]: (ifeq(iext(uri_rdfs_subClassOf, uri_owl_Restriction, D_593), true, icext(D_593, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z), true)=true))). % 39.17/27.84 tff(c_13331, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_owl_onProperty, uri_rdf_Property), true)=true))). % 39.17/27.84 tff(c_10016, 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))). % 39.17/27.84 tff(c_7205, plain, (![E_41]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, E_41), true, iext(uri_rdfs_subClassOf, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, E_41), true)=true))). % 39.17/27.84 tff(c_2696, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdf_type), true, ifeq(iext(P_108, uri_rdf_first, uri_rdf_Property), true, true, true), true)=true))). % 39.17/27.84 tff(c_10289, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_ex_Person, uri_rdfs_Resource), true)=true))). % 39.17/27.84 tff(c_9585, 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))). % 39.17/27.84 tff(c_10074, 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))). % 39.17/27.84 tff(c_2780, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_subClassOf), true, ifeq(iext(P_108, uri_rdfs_Seq, uri_rdfs_Container), true, true, true), true)=true))). % 39.17/27.84 tff(c_9079, 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))). % 39.17/27.84 tff(c_9387, 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))). % 39.17/27.84 tff(c_5599, 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))). % 39.17/27.84 tff(c_28407, plain, (![D_575]: (ifeq(iext(uri_rdfs_subClassOf, uri_ex_Person, D_575), true, icext(D_575, uri_ex_alice), true)=true))). % 39.17/27.84 tff(c_13056, 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))). % 39.17/27.84 tff(c_9388, 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))). % 39.17/27.84 tff(c_12383, 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))). % 39.17/27.84 tff(c_3058, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_owl_minCardinality, Q_109), true, iext(Q_109, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, literal_typed(dat_str_1, uri_xsd_nonNegativeInteger)), true)=true))). % 39.17/27.84 tff(c_11692, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_owl_minCardinality, uri_rdf_Property), true)=true))). % 39.17/27.84 tff(c_7687, 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))). % 39.17/27.84 tff(c_28200, plain, (![D_566]: (ifeq(iext(uri_rdfs_subClassOf, uri_ex_Person, D_566), true, icext(D_566, uri_ex_bob), true)=true))). % 39.17/27.84 tff(c_9722, 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))). % 39.17/27.84 tff(c_12139, 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))). % 39.17/27.84 tff(c_2354, plain, (![C_99]: (ifeq(iext(uri_rdfs_range, uri_owl_minCardinality, C_99), true, icext(C_99, literal_typed(dat_str_1, uri_xsd_nonNegativeInteger)), true)=true))). % 39.17/27.84 tff(c_10915, 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))). % 39.17/27.84 tff(c_5047, plain, (![Q_48, X_135]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, X_135, uri_rdfs_Resource), true)=true))). % 39.17/27.84 tff(c_27840, plain, (![D_556]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_556), true, icext(D_556, uri_rdf_object), true)=true))). % 39.17/27.84 tff(c_3076, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_109), true, iext(Q_109, uri_rdfs_range, uri_rdfs_Class), true)=true))). % 39.17/27.84 tff(c_3086, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_109), true, iext(Q_109, uri_rdf__3, uri_rdfs_Resource), true)=true))). % 39.17/27.84 tff(c_2540, plain, (![E_103]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, E_103), true, iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, E_103), true)=true))). % 39.17/27.84 tff(c_3114, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_109), true, iext(Q_109, uri_rdf_type, uri_rdf_Property), true)=true))). % 39.17/27.84 tff(c_3118, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_109), true, iext(Q_109, uri_rdfs_Datatype, uri_rdfs_Class), true)=true))). % 39.17/27.84 tff(c_3111, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_109), true, iext(Q_109, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, uri_owl_Restriction), true)=true))). % 39.17/27.84 tff(c_3061, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_ex_hasAncestor, Q_109), true, iext(Q_109, uri_ex_alice, uri_ex_bob), true)=true))). % 39.17/27.84 tff(c_3097, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_109), true, iext(Q_109, uri_rdf__1, uri_rdfs_Resource), true)=true))). % 39.17/27.84 tff(c_3106, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_109), true, iext(Q_109, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property), true)=true))). % 39.17/27.84 tff(c_3071, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_109), true, iext(Q_109, uri_rdf__1, uri_rdf_Property), true)=true))). % 39.17/27.84 tff(c_3123, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_owl_onProperty, Q_109), true, iext(Q_109, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, uri_ex_hasAncestor), true)=true))). % 39.17/27.84 tff(c_3122, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_109), true, iext(Q_109, uri_rdfs_subPropertyOf, uri_rdf_Property), true)=true))). % 39.17/27.84 tff(c_3059, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_109), true, iext(Q_109, uri_rdf_predicate, uri_rdfs_Statement), true)=true))). % 39.17/27.84 tff(c_3120, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_109), true, iext(Q_109, uri_rdf_Bag, uri_rdfs_Container), true)=true))). % 39.17/27.84 tff(c_3068, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_109), true, iext(Q_109, uri_rdf_object, uri_rdf_Property), true)=true))). % 39.17/27.84 tff(c_3109, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_109), true, iext(Q_109, uri_rdf_value, uri_rdf_Property), true)=true))). % 39.17/27.84 tff(c_27471, plain, (![D_538]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_538), true, icext(D_538, uri_rdf_rest), true)=true))). % 39.17/27.84 tff(c_3099, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_109), true, iext(Q_109, uri_rdfs_subClassOf, uri_rdfs_Class), true)=true))). % 39.17/27.84 tff(c_3104, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_109), true, iext(Q_109, uri_rdfs_subPropertyOf, uri_rdf_Property), true)=true))). % 39.17/27.84 tff(c_3119, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_109), true, iext(Q_109, uri_rdfs_member, uri_rdfs_Resource), true)=true))). % 39.17/27.84 tff(c_3088, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_109), true, iext(Q_109, uri_rdf__2, uri_rdfs_Resource), true)=true))). % 39.17/27.84 tff(c_3112, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_109), true, iext(Q_109, uri_rdf_rest, uri_rdf_List), true)=true))). % 39.17/27.84 tff(c_3101, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_109), true, iext(Q_109, uri_rdfs_label, uri_rdfs_Resource), true)=true))). % 39.17/27.84 tff(c_2542, plain, (![E_103]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, E_103), true, iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, E_103), true)=true))). % 39.17/27.84 tff(c_27249, plain, (![D_529]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_529), true, icext(D_529, uri_rdf_type), true)=true))). % 39.17/27.84 tff(c_3113, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_109), true, iext(Q_109, uri_rdf_rest, uri_rdf_Property), true)=true))). % 39.17/27.84 tff(c_3091, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_109), true, iext(Q_109, uri_rdf__1, uri_rdfs_Resource), true)=true))). % 39.17/27.84 tff(c_3095, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_109), true, iext(Q_109, uri_rdfs_seeAlso, uri_rdfs_Resource), true)=true))). % 39.17/27.84 tff(c_3121, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_109), true, iext(Q_109, uri_rdf_object, uri_rdfs_Statement), true)=true))). % 39.17/27.84 tff(c_3117, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_109), true, iext(Q_109, uri_rdf_Alt, uri_rdfs_Container), true)=true))). % 39.17/27.84 tff(c_3103, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_109), true, iext(Q_109, uri_rdf_first, uri_rdfs_Resource), true)=true))). % 39.17/27.84 tff(c_3094, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_109), true, iext(Q_109, uri_rdf__2, uri_rdfs_ContainerMembershipProperty), true)=true))). % 39.17/27.84 tff(c_3082, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_109), true, iext(Q_109, uri_rdfs_comment, uri_rdfs_Literal), true)=true))). % 39.17/27.84 tff(c_3090, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_109), true, iext(Q_109, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true)=true))). % 39.17/27.84 tff(c_3066, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_109), true, iext(Q_109, uri_rdf_value, uri_rdfs_Resource), true)=true))). % 39.17/27.84 tff(c_3064, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_109), true, iext(Q_109, uri_rdf__2, uri_rdf_Property), true)=true))). % 39.17/27.84 tff(c_3093, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_109), true, iext(Q_109, uri_rdfs_seeAlso, uri_rdfs_Resource), true)=true))). % 39.17/27.84 tff(c_3063, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_109), true, iext(Q_109, uri_rdf_XMLLiteral, uri_rdfs_Literal), true)=true))). % 39.17/27.84 tff(c_3115, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_109), true, iext(Q_109, uri_ex_alice, uri_ex_Person), true)=true))). % 39.17/27.84 tff(c_3067, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_109), true, iext(Q_109, uri_rdf_type, uri_rdfs_Class), true)=true))). % 39.17/27.84 tff(c_3110, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_109), true, iext(Q_109, uri_rdf_predicate, uri_rdfs_Resource), true)=true))). % 39.17/27.84 tff(c_26887, plain, (![D_511]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_511), true, icext(D_511, uri_rdf_nil), true)=true))). % 39.17/27.85 tff(c_3070, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_109), true, iext(Q_109, uri_ex_bob, uri_ex_Person), true)=true))). % 39.17/27.85 tff(c_3079, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_109), true, iext(Q_109, uri_rdfs_Seq, uri_rdfs_Container), true)=true))). % 39.17/27.85 tff(c_3069, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_109), true, iext(Q_109, uri_rdf__3, uri_rdfs_ContainerMembershipProperty), true)=true))). % 39.17/27.85 tff(c_3083, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_109), true, iext(Q_109, uri_rdf_type, uri_rdfs_Resource), true)=true))). % 39.17/27.85 tff(c_3087, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_109), true, iext(Q_109, uri_ex_hasAncestor, uri_owl_TransitiveProperty), true)=true))). % 39.17/27.85 tff(c_3077, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_109), true, iext(Q_109, uri_rdf_XMLLiteral, uri_rdfs_Datatype), true)=true))). % 39.17/27.85 tff(c_2538, plain, (![E_103]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Literal, E_103), true, iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, E_103), true)=true))). % 39.17/27.85 tff(c_3105, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_109), true, iext(Q_109, uri_rdf_subject, uri_rdf_Property), true)=true))). % 39.17/27.85 tff(c_2596, plain, (![R_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_seeAlso, R_106), true, iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, R_106), true)=true))). % 39.17/27.85 tff(c_3100, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_109), true, iext(Q_109, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso), true)=true))). % 39.17/27.85 tff(c_3116, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_109), true, iext(Q_109, uri_rdfs_domain, uri_rdfs_Class), true)=true))). % 39.17/27.85 tff(c_3080, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_109), true, iext(Q_109, uri_rdfs_range, uri_rdf_Property), true)=true))). % 39.17/27.85 tff(c_16935, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_comment), true)=true))). % 39.17/27.85 tff(c_15975, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_label), true)=true))). % 39.17/27.85 tff(c_15974, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_label), true)=true))). % 39.17/27.85 tff(c_15910, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_predicate), true)=true))). % 39.17/27.85 tff(c_15909, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_predicate), true)=true))). % 39.17/27.85 tff(c_16936, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_comment), true)=true))). % 39.17/27.85 tff(c_15509, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Resource), true)=true))). % 39.17/27.85 tff(c_3065, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_109), true, iext(Q_109, uri_rdf_first, uri_rdf_Property), true)=true))). % 39.17/27.85 tff(c_15844, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_member), true)=true))). % 39.17/27.85 tff(c_15148, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdf_List), true)=true))). % 39.17/27.85 tff(c_3074, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_109), true, iext(Q_109, uri_rdfs_label, uri_rdfs_Literal), true)=true))). % 39.17/27.85 tff(c_15438, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_owl_TransitiveProperty), true)=true))). % 39.17/27.85 tff(c_15082, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Statement), true)=true))). % 39.17/27.85 tff(c_15081, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Statement), true)=true))). % 39.17/27.85 tff(c_14664, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_owl_TransitiveProperty), true)=true))). % 39.17/27.85 tff(c_3075, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_109), true, iext(Q_109, uri_rdf__1, uri_rdfs_ContainerMembershipProperty), true)=true))). % 39.17/27.85 tff(c_17340, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_owl_Restriction), true)=true))). % 39.17/27.85 tff(c_15343, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_List), true)=true))). % 39.17/27.85 tff(c_17559, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_owl_Restriction), true)=true))). % 39.17/27.85 tff(c_2539, plain, (![E_103]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_103), true, iext(uri_rdfs_subClassOf, uri_rdfs_Seq, E_103), true)=true))). % 39.17/27.85 tff(c_14152, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_29), true, icext(C_29, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z), true)=true))). % 39.17/27.85 tff(c_3062, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_109), true, iext(Q_109, uri_rdfs_subClassOf, uri_rdfs_Class), true)=true))). % 39.17/27.85 tff(c_26047, plain, (![D_475]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_475), true, icext(D_475, uri_rdf__2), true)=true))). % 39.17/27.85 tff(c_2544, plain, (![E_103]: (ifeq(iext(uri_rdfs_subClassOf, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, E_103), true, iext(uri_rdfs_subClassOf, uri_ex_Person, E_103), true)=true))). % 39.17/27.85 tff(c_9018, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_subject), true)=true))). % 39.17/27.85 tff(c_7082, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_rest), true)=true))). % 39.17/27.85 tff(c_3072, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_109), true, iext(Q_109, uri_rdf_rest, uri_rdf_List), true)=true))). % 39.17/27.85 tff(c_6468, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_subClassOf), true)=true))). % 39.17/27.85 tff(c_9864, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_seeAlso), true)=true))). % 39.17/27.85 tff(c_3060, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_109), true, iext(Q_109, uri_rdf_nil, uri_rdf_List), true)=true))). % 39.17/27.85 tff(c_25784, plain, (![D_466]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_466), true, icext(D_466, uri_rdf__3), true)=true))). % 39.17/27.85 tff(c_9930, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_owl_onProperty), true)=true))). % 39.17/27.85 tff(c_8526, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_ex_Person), true)=true))). % 39.17/27.85 tff(c_2543, plain, (![E_103]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_103), true, iext(uri_rdfs_subClassOf, uri_rdf_Bag, E_103), true)=true))). % 39.17/27.85 tff(c_7858, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_type), true)=true))). % 39.17/27.85 tff(c_9017, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_subject), true)=true))). % 39.17/27.85 tff(c_25451, plain, (![C_91, X_62]: (ifeq(icext(C_91, X_62), true, true, true)=true))). % 39.17/27.85 tff(c_3107, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_109), true, iext(Q_109, uri_rdf__2, uri_rdfs_Resource), true)=true))). % 39.17/27.85 tff(c_11930, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Datatype), true)=true))). % 39.17/27.85 tff(c_24925, plain, (![D_453, X_454]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, D_453), true, icext(D_453, X_454), true)=true))). % 39.17/27.85 tff(c_6558, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Container), true)=true))). % 39.17/27.85 tff(c_3102, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_109), true, iext(Q_109, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true)=true))). % 39.17/27.85 tff(c_8593, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_first), true)=true))). % 39.17/27.85 tff(c_8022, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_Bag), true)=true))). % 39.17/27.85 tff(c_24783, plain, (![X_445, Y_446]: (ifeq(iext(uri_rdf_first, X_445, Y_446), true, icext(uri_rdf_List, X_445), true)=true))). % 39.17/27.85 tff(c_7955, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Class), true)=true))). % 39.17/27.85 tff(c_3096, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_109), true, iext(Q_109, uri_rdfs_domain, uri_rdf_Property), true)=true))). % 39.17/27.85 tff(c_11135, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_subPropertyOf), true)=true))). % 39.17/27.85 tff(c_6906, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_range), true)=true))). % 39.17/27.85 tff(c_7859, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_type), true)=true))). % 39.17/27.85 tff(c_24268, plain, (![X_436, Y_437]: (ifeq(iext(uri_rdfs_range, X_436, Y_437), true, icext(uri_rdf_Property, X_436), true)=true))). % 39.17/27.85 tff(c_7621, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__1), true)=true))). % 39.17/27.85 tff(c_9929, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_owl_onProperty), true)=true))). % 39.17/27.85 tff(c_3124, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_109), true, iext(Q_109, uri_ex_Person, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z), true)=true))). % 39.17/27.85 tff(c_9493, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_Alt), true)=true))). % 39.17/27.85 tff(c_8258, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_object), true)=true))). % 39.17/27.85 tff(c_13060, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_value), true)=true))). % 39.17/27.85 tff(c_23695, plain, (![X_426, Y_427]: (ifeq(iext(uri_rdfs_subPropertyOf, X_426, Y_427), true, icext(uri_rdf_Property, X_426), true)=true))). % 39.17/27.85 tff(c_13059, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_value), true)=true))). % 39.17/27.85 tff(c_3085, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_109), true, iext(Q_109, uri_rdfs_comment, uri_rdfs_Resource), true)=true))). % 39.17/27.85 tff(c_6658, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__3), true)=true))). % 39.17/27.85 tff(c_23221, plain, (![X_419, Y_420]: (ifeq(iext(uri_rdfs_domain, X_419, Y_420), true, icext(uri_rdf_Property, X_419), true)=true))). % 39.17/27.85 tff(c_10918, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__1), true)=true))). % 39.17/27.85 tff(c_3098, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_109), true, iext(Q_109, uri_rdf__3, uri_rdf_Property), true)=true))). % 39.17/27.85 tff(c_8594, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_first), true)=true))). % 39.17/27.85 tff(c_22495, plain, (![X_411, Y_412]: (ifeq(iext(uri_rdfs_subClassOf, X_411, Y_412), true, icext(uri_rdfs_Class, Y_412), true)=true))). % 39.17/27.85 tff(c_11460, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Literal), true)=true))). % 39.17/27.85 tff(c_7690, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_isDefinedBy), true)=true))). % 39.17/27.85 tff(c_3089, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_109), true, iext(Q_109, uri_rdf_subject, uri_rdfs_Resource), true)=true))). % 39.17/27.85 tff(c_7083, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_rest), true)=true))). % 39.17/27.85 tff(c_7532, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Seq), true)=true))). % 39.17/27.85 tff(c_22341, plain, (![X_402, Y_403]: (ifeq(iext(uri_rdf_object, X_402, Y_403), true, icext(uri_rdfs_Statement, X_402), true)=true))). % 39.17/27.85 tff(c_3108, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_109), true, iext(Q_109, uri_rdf_value, uri_rdfs_Resource), true)=true))). % 39.17/27.85 tff(c_12386, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__2), true)=true))). % 39.17/27.85 tff(c_5926, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_domain), true)=true))). % 39.17/27.85 tff(c_21899, plain, (![X_395, Y_396]: (ifeq(iext(uri_rdfs_range, X_395, Y_396), true, icext(uri_rdfs_Class, Y_396), true)=true))). % 39.17/27.85 tff(c_11006, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_ContainerMembershipProperty), true)=true))). % 39.17/27.85 tff(c_11134, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_subPropertyOf), true)=true))). % 39.17/27.85 tff(c_3078, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_109), true, iext(Q_109, uri_rdf_Property, uri_rdfs_Class), true)=true))). % 39.17/27.85 tff(c_12387, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__2), true)=true))). % 39.17/27.85 tff(c_21766, plain, (![X_387, Y_388]: (ifeq(iext(uri_rdfs_label, X_387, Y_388), true, icext(uri_rdfs_Literal, Y_388), true)=true))). % 39.17/27.85 tff(c_6467, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_subClassOf), true)=true))). % 39.17/27.85 tff(c_6403, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z), true)=true))). % 39.17/27.85 tff(c_3081, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_109), true, iext(Q_109, uri_rdf_subject, uri_rdfs_Statement), true)=true))). % 39.17/27.85 tff(c_12142, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdf_Property), true)=true))). % 39.17/27.85 tff(c_8257, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_object), true)=true))). % 39.17/27.85 tff(c_21229, plain, (![X_378, Y_379]: (ifeq(iext(uri_rdfs_subPropertyOf, X_378, Y_379), true, icext(uri_rdf_Property, Y_379), true)=true))). % 39.17/27.85 tff(c_12077, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_owl_minCardinality), true)=true))). % 39.17/27.85 tff(c_3073, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_109), true, iext(Q_109, uri_rdf_first, uri_rdf_List), true)=true))). % 39.17/27.85 tff(c_6907, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_range), true)=true))). % 39.17/27.85 tff(c_12076, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_owl_minCardinality), true)=true))). % 39.17/27.85 tff(c_20804, plain, (![X_370, Y_371]: (ifeq(iext(uri_rdfs_domain, X_370, Y_371), true, icext(uri_rdfs_Class, Y_371), true)=true))). % 39.17/27.85 tff(c_13155, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_XMLLiteral), true)=true))). % 39.17/27.85 tff(c_10917, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_member), true)=true))). % 39.17/27.85 tff(c_2541, plain, (![E_103]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_103), true, iext(uri_rdfs_subClassOf, uri_rdf_Alt, E_103), true)=true))). % 39.17/27.85 tff(c_20687, plain, (![X_363, Y_364]: (ifeq(iext(uri_rdfs_comment, X_363, Y_364), true, icext(uri_rdfs_Literal, Y_364), true)=true))). % 39.17/27.85 tff(c_12970, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_ex_hasAncestor), true)=true))). % 39.17/27.85 tff(c_3092, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_109), true, iext(Q_109, uri_rdf__3, uri_rdfs_Resource), true)=true))). % 39.17/27.85 tff(c_5927, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_domain), true)=true))). % 39.17/27.85 tff(c_11459, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Resource), true)=true))). % 39.17/27.85 tff(c_19993, plain, (![X_355, Y_356]: (ifeq(iext(uri_rdf_type, X_355, Y_356), true, icext(uri_rdfs_Class, Y_356), true)=true))). % 39.17/27.85 tff(c_12969, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_ex_hasAncestor), true)=true))). % 39.17/27.85 tff(c_3084, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_109), true, iext(Q_109, uri_rdfs_member, uri_rdfs_Resource), true)=true))). % 39.17/27.85 tff(c_6659, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__3), true)=true))). % 39.17/27.85 tff(c_5048, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_29), true, icext(C_29, uri_rdfs_Resource), true)=true))). % 39.17/27.85 tff(c_5049, plain, (![C_19, X_135]: (ifeq(iext(uri_rdfs_domain, uri_rdf_type, C_19), true, icext(C_19, X_135), true)=true))). % 39.17/27.85 tff(c_19591, plain, (![X_345, Y_346]: (ifeq(iext(uri_rdf_rest, X_345, Y_346), true, icext(uri_rdf_List, Y_346), true)=true))). % 39.17/27.85 tff(c_19529, plain, (![X_340, Y_341]: (ifeq(iext(uri_rdf_subject, X_340, Y_341), true, icext(uri_rdfs_Statement, X_340), true)=true))). % 39.17/27.85 tff(c_1989, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_95), true, icext(C_95, uri_rdf_value), true)=true))). % 39.17/27.85 tff(c_2035, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_95), true, icext(C_95, uri_rdfs_subPropertyOf), true)=true))). % 39.17/27.85 tff(c_2039, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_95), true, icext(C_95, uri_rdf__2), true)=true))). % 39.17/27.85 tff(c_2053, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_95), true, icext(C_95, uri_rdf_object), true)=true))). % 39.17/27.85 tff(c_2005, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_95), true, icext(C_95, uri_rdfs_comment), true)=true))). % 39.17/27.85 tff(c_2370, plain, (![C_99]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_99), true, icext(C_99, uri_rdfs_Literal), true)=true))). % 39.17/27.85 tff(c_2003, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_95), true, icext(C_95, uri_rdfs_range), true)=true))). % 39.17/27.85 tff(c_2429, plain, (![C_99]: (ifeq(iext(uri_rdfs_range, uri_owl_onProperty, C_99), true, icext(C_99, uri_ex_hasAncestor), true)=true))). % 39.17/27.85 tff(c_2055, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_owl_onProperty, C_95), true, icext(C_95, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z), true)=true))). % 39.17/27.85 tff(c_18284, plain, (![X_317, Y_318]: (ifeq(iext(uri_rdfs_subClassOf, X_317, Y_318), true, icext(uri_rdfs_Class, X_317), true)=true))). % 39.17/27.85 tff(c_2009, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_95), true, icext(C_95, uri_rdfs_member), true)=true))). % 39.17/27.85 tff(c_2373, plain, (![C_99]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_99), true, icext(C_99, uri_rdfs_Datatype), true)=true))). % 39.17/27.85 tff(c_2368, plain, (![C_99]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_99), true, icext(C_99, uri_rdf_List), true)=true))). % 39.17/27.85 tff(c_2054, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_95), true, icext(C_95, uri_rdfs_subPropertyOf), true)=true))). % 39.17/27.85 tff(c_2366, plain, (![C_99]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_99), true, icext(C_99, uri_ex_Person), true)=true))). % 39.17/27.85 tff(c_2423, plain, (![C_99]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_99), true, icext(C_99, uri_rdfs_Class), true)=true))). % 39.17/27.85 tff(c_2033, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_95), true, icext(C_95, uri_rdfs_isDefinedBy), true)=true))). % 39.17/27.85 tff(c_2020, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_95), true, icext(C_95, uri_rdf__3), true)=true))). % 39.17/27.85 tff(c_1983, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_ex_hasAncestor, C_95), true, icext(C_95, uri_ex_alice), true)=true))). % 39.17/27.85 tff(c_2049, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_95), true, icext(C_95, uri_rdf_Alt), true)=true))). % 39.17/27.85 tff(c_2029, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_95), true, icext(C_95, uri_rdfs_isDefinedBy), true)=true))). % 39.17/27.85 tff(c_2357, plain, (![C_99]: (ifeq(iext(uri_rdfs_range, uri_ex_hasAncestor, C_99), true, icext(C_99, uri_ex_bob), true)=true))). % 39.17/27.85 tff(c_2052, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_95), true, icext(C_95, uri_rdf_Bag), true)=true))). % 39.17/27.85 tff(c_2017, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_95), true, icext(C_95, uri_rdfs_isDefinedBy), true)=true))). % 39.17/27.85 tff(c_1990, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_95), true, icext(C_95, uri_rdf_type), true)=true))). % 39.17/27.85 tff(c_17773, plain, (![X_295, Y_296]: (ifeq(iext(uri_rdf_rest, X_295, Y_296), true, icext(uri_rdf_List, X_295), true)=true))). % 39.17/27.85 tff(c_2359, plain, (![C_99]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_99), true, icext(C_99, uri_rdfs_Literal), true)=true))). % 39.17/27.85 tff(c_2376, plain, (![C_99]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_99), true, icext(C_99, uri_rdf_Property), true)=true))). % 39.17/27.85 tff(c_2021, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_95), true, icext(C_95, uri_rdfs_seeAlso), true)=true))). % 39.17/27.85 tff(c_2417, plain, (![C_99]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_99), true, icext(C_99, uri_rdf_List), true)=true))). % 39.17/27.85 tff(c_2051, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_95), true, icext(C_95, uri_rdfs_member), true)=true))). % 39.17/27.85 tff(c_2040, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_95), true, icext(C_95, uri_rdf_value), true)=true))). % 39.17/27.85 tff(c_1995, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_95), true, icext(C_95, uri_rdf_rest), true)=true))). % 39.17/27.85 tff(c_2037, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_95), true, icext(C_95, uri_rdfs_ContainerMembershipProperty), true)=true))). % 39.17/27.85 tff(c_2044, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_95), true, icext(C_95, uri_rdf_rest), true)=true))). % 39.17/27.85 tff(c_2048, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_95), true, icext(C_95, uri_rdfs_domain), true)=true))). % 39.17/27.85 tff(c_1999, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_95), true, icext(C_95, uri_rdfs_range), true)=true))). % 39.17/27.85 tff(c_2409, plain, (![C_99]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_99), true, icext(C_99, uri_rdf_Property), true)=true))). % 39.17/27.85 tff(c_2056, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_95), true, icext(C_95, uri_ex_Person), true)=true))). % 39.17/27.85 tff(c_17561, plain, (![X_33]: (ifeq(icext(uri_owl_Restriction, X_33), true, icext(uri_owl_Restriction, X_33), true)=true))). % 39.17/27.85 tff(c_17505, plain, (iext(uri_rdfs_subClassOf, uri_owl_Restriction, uri_owl_Restriction)=true)). % 39.17/27.85 tff(c_17285, plain, (iext(uri_rdfs_subClassOf, uri_owl_Restriction, uri_rdfs_Resource)=true)). % 39.17/27.85 tff(c_17209, plain, (iext(uri_rdf_type, uri_owl_Restriction, uri_rdfs_Class)=true)). % 39.17/27.85 tff(c_2013, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_95), true, icext(C_95, uri_rdf__3), true)=true))). % 39.17/27.85 tff(c_17034, plain, (ic(uri_owl_Restriction)=true)). % 39.17/27.85 tff(c_16968, plain, (icext(uri_rdfs_Class, uri_owl_Restriction)=true)). % 39.17/27.85 tff(c_2416, plain, (![C_99]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_99), true, icext(C_99, uri_owl_Restriction), true)=true))). % 39.17/27.85 tff(c_16881, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_comment, uri_rdfs_comment)=true)). % 39.17/27.85 tff(c_16839, plain, (ip(uri_rdfs_comment)=true)). % 39.17/27.85 tff(c_16781, plain, (iext(uri_rdf_type, uri_rdfs_comment, uri_rdf_Property)=true)). % 39.17/27.85 tff(c_16591, plain, (icext(uri_rdf_Property, uri_rdfs_comment)=true)). % 39.17/27.85 tff(c_2011, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_95), true, icext(C_95, uri_rdfs_comment), true)=true))). % 39.17/27.85 tff(c_15345, plain, (![X_33]: (ifeq(icext(uri_rdf_List, X_33), true, icext(uri_rdf_List, X_33), true)=true))). % 39.17/27.85 tff(c_15083, plain, (![X_33]: (ifeq(icext(uri_rdfs_Statement, X_33), true, icext(uri_rdfs_Statement, X_33), true)=true))). % 39.17/27.85 tff(c_15440, plain, (![X_33]: (ifeq(icext(uri_owl_TransitiveProperty, X_33), true, icext(uri_owl_TransitiveProperty, X_33), true)=true))). % 39.17/27.85 tff(c_7790, plain, (![X_33]: (ifeq(icext(uri_rdf_Property, X_33), true, icext(uri_rdf_Property, X_33), true)=true))). % 39.17/27.86 tff(c_8462, plain, (![X_33]: (ifeq(icext(uri_rdfs_Container, X_33), true, icext(uri_rdfs_Container, X_33), true)=true))). % 39.17/27.86 tff(c_6404, plain, (![X_33]: (ifeq(icext(sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, X_33), true, icext(sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, X_33), true)=true))). % 39.17/27.86 tff(c_16066, plain, (![X_263, Y_264]: (ifeq(iext(uri_rdf_predicate, X_263, Y_264), true, icext(uri_rdfs_Statement, X_263), true)=true))). % 39.17/27.86 tff(c_10851, plain, (![X_33]: (ifeq(icext(uri_rdfs_Literal, X_33), true, icext(uri_rdfs_Literal, X_33), true)=true))). % 39.17/27.86 tff(c_7534, plain, (![X_33]: (ifeq(icext(uri_rdfs_Seq, X_33), true, icext(uri_rdfs_Seq, X_33), true)=true))). % 39.17/27.86 tff(c_7956, plain, (![X_33]: (ifeq(icext(uri_rdfs_Class, X_33), true, icext(uri_rdfs_Class, X_33), true)=true))). % 39.17/27.86 tff(c_11008, plain, (![X_33]: (ifeq(icext(uri_rdfs_ContainerMembershipProperty, X_33), true, icext(uri_rdfs_ContainerMembershipProperty, X_33), true)=true))). % 39.17/27.86 tff(c_13157, plain, (![X_33]: (ifeq(icext(uri_rdf_XMLLiteral, X_33), true, icext(uri_rdf_XMLLiteral, X_33), true)=true))). % 39.17/27.86 tff(c_9495, plain, (![X_33]: (ifeq(icext(uri_rdf_Alt, X_33), true, icext(uri_rdf_Alt, X_33), true)=true))). % 39.17/27.86 tff(c_8528, plain, (![X_33]: (ifeq(icext(uri_ex_Person, X_33), true, icext(uri_ex_Person, X_33), true)=true))). % 39.17/27.86 tff(c_11932, plain, (![X_33]: (ifeq(icext(uri_rdfs_Datatype, X_33), true, icext(uri_rdfs_Datatype, X_33), true)=true))). % 39.17/27.86 tff(c_8024, plain, (![X_33]: (ifeq(icext(uri_rdf_Bag, X_33), true, icext(uri_rdf_Bag, X_33), true)=true))). % 39.17/27.86 tff(c_15985, plain, (iext(uri_rdf_type, uri_rdfs_Resource, uri_rdfs_Class)=true)). % 39.17/27.86 tff(c_1996, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_95), true, icext(C_95, uri_rdf_first), true)=true))). % 39.17/27.86 tff(c_15920, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_label, uri_rdfs_label)=true)). % 39.17/27.86 tff(c_15855, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_predicate, uri_rdf_predicate)=true)). % 39.17/27.86 tff(c_15785, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_member, uri_rdfs_member)=true)). % 39.17/27.86 tff(c_15605, plain, (icext(uri_rdf_Property, uri_rdfs_member)=true)). % 39.17/27.86 tff(c_15551, plain, (iext(uri_rdf_type, uri_rdfs_member, uri_rdf_Property)=true)). % 39.17/27.86 tff(c_2015, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_95), true, icext(C_95, uri_rdf__2), true)=true))). % 39.17/27.86 tff(c_15451, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Resource, uri_rdfs_Resource)=true)). % 39.17/27.86 tff(c_15384, plain, (iext(uri_rdfs_subClassOf, uri_owl_TransitiveProperty, uri_owl_TransitiveProperty)=true)). % 39.17/27.86 tff(c_15289, plain, (iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdf_List)=true)). % 39.17/27.86 tff(c_15093, plain, (iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdfs_Resource)=true)). % 39.17/27.86 tff(c_15027, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Statement, uri_rdfs_Statement)=true)). % 39.17/27.86 tff(c_1985, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_95), true, icext(C_95, uri_rdf_XMLLiteral), true)=true))). % 39.17/27.86 tff(c_14805, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Statement, uri_rdfs_Resource)=true)). % 39.17/27.86 tff(c_14609, plain, (iext(uri_rdfs_subClassOf, uri_owl_TransitiveProperty, uri_rdfs_Resource)=true)). % 39.17/27.86 tff(c_14531, plain, (iext(uri_rdf_type, uri_rdf_Bag, uri_rdfs_Class)=true)). % 39.17/27.86 tff(c_14483, plain, (iext(uri_rdf_type, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, uri_rdfs_Class)=true)). % 39.17/27.86 tff(c_2422, plain, (![C_99]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_99), true, icext(C_99, uri_rdfs_Container), true)=true))). % 39.17/27.86 tff(c_14410, plain, (iext(uri_rdf_type, uri_rdfs_Class, uri_rdfs_Class)=true)). % 39.17/27.86 tff(c_14362, plain, (iext(uri_rdf_type, uri_rdf_Alt, uri_rdfs_Class)=true)). % 39.17/27.86 tff(c_14311, plain, (iext(uri_rdf_type, uri_ex_Person, uri_rdfs_Class)=true)). % 39.17/27.86 tff(c_14263, plain, (iext(uri_rdf_type, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Class)=true)). % 39.17/27.86 tff(c_14215, plain, (iext(uri_rdf_type, uri_rdfs_Literal, uri_rdfs_Class)=true)). % 39.17/27.86 tff(c_14164, plain, (iext(uri_rdf_type, uri_rdfs_Datatype, uri_rdfs_Class)=true)). % 39.17/27.86 tff(c_14115, plain, (iext(uri_rdf_type, uri_ex_bob, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)=true)). % 39.17/27.86 tff(c_14066, plain, (iext(uri_rdf_type, uri_rdfs_Seq, uri_rdfs_Class)=true)). % 39.17/27.86 tff(c_2019, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_95), true, icext(C_95, uri_rdf__1), true)=true))). % 39.17/27.86 tff(c_13990, plain, (iext(uri_rdf_type, uri_rdfs_Container, uri_rdfs_Class)=true)). % 39.17/27.86 tff(c_13943, plain, (iext(uri_rdf_type, uri_ex_alice, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)=true)). % 39.17/27.86 tff(c_13896, plain, (iext(uri_rdf_type, uri_rdf_XMLLiteral, uri_rdfs_Class)=true)). % 39.17/27.86 tff(c_13851, plain, (ip(uri_rdfs_label)=true)). % 39.17/27.86 tff(c_13794, plain, (iext(uri_rdf_type, uri_rdfs_label, uri_rdf_Property)=true)). % 39.17/27.86 tff(c_2374, plain, (![C_99]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_99), true, icext(C_99, uri_rdfs_Class), true)=true))). % 39.17/27.86 tff(c_13721, plain, (iext(uri_rdf_type, uri_rdfs_Statement, uri_rdfs_Class)=true)). % 39.17/27.86 tff(c_13674, plain, (iext(uri_rdf_type, uri_rdf_List, uri_rdfs_Class)=true)). % 39.17/27.86 tff(c_13631, plain, (ip(uri_rdf_predicate)=true)). % 39.17/27.86 tff(c_13574, plain, (iext(uri_rdf_type, uri_rdf_predicate, uri_rdf_Property)=true)). % 39.17/27.86 tff(c_13527, plain, (iext(uri_rdf_type, uri_owl_TransitiveProperty, uri_rdfs_Class)=true)). % 39.17/27.86 tff(c_13343, plain, (icext(uri_rdf_Property, uri_owl_onProperty)=true)). % 39.17/27.86 tff(c_13289, plain, (iext(uri_rdf_type, uri_owl_onProperty, uri_rdf_Property)=true)). % 39.17/27.86 tff(c_2401, plain, (![C_99]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_99), true, icext(C_99, uri_rdfs_Class), true)=true))). % 39.17/27.86 tff(c_939, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_range, S_5, O_6), true, true, true)=true))). % 39.17/27.86 tff(c_13076, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdf_XMLLiteral)=true)). % 39.17/27.86 tff(c_2413, plain, (![C_99]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_99), true, icext(C_99, uri_rdf_Property), true)=true))). % 39.17/27.86 tff(c_12980, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_value, uri_rdf_value)=true)). % 39.17/27.86 tff(c_1984, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_95), true, icext(C_95, uri_rdfs_subClassOf), true)=true))). % 39.17/27.86 tff(c_12915, plain, (iext(uri_rdfs_subPropertyOf, uri_ex_hasAncestor, uri_ex_hasAncestor)=true)). % 39.17/27.86 tff(c_978, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_domain, S_5, O_6), true, true, true)=true))). % 39.17/27.86 tff(c_12573, plain, (ic(uri_rdf_List)=true)). % 39.17/27.86 tff(c_12515, plain, (icext(uri_rdfs_Class, uri_rdf_List)=true)). % 39.17/27.86 tff(c_2356, plain, (![C_99]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_99), true, icext(C_99, uri_rdf_List), true)=true))). % 39.17/27.86 tff(c_12455, plain, (ic(uri_owl_TransitiveProperty)=true)). % 39.17/27.86 tff(c_12397, plain, (icext(uri_rdfs_Class, uri_owl_TransitiveProperty)=true)). % 39.17/27.86 tff(c_12313, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__2, uri_rdf__2)=true)). % 39.17/27.86 tff(c_2383, plain, (![C_99]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_99), true, icext(C_99, uri_owl_TransitiveProperty), true)=true))). % 39.17/27.86 tff(c_12087, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdfs_Resource)=true)). % 39.17/27.86 tff(c_12022, plain, (iext(uri_rdfs_subPropertyOf, uri_owl_minCardinality, uri_owl_minCardinality)=true)). % 39.17/27.86 tff(c_1981, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_95), true, icext(C_95, uri_rdf_predicate), true)=true))). % 39.17/27.86 tff(c_11942, plain, (iext(uri_rdf_type, uri_rdfs_domain, uri_rdf_Property)=true)). % 39.17/27.86 tff(c_11876, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Datatype)=true)). % 39.17/27.86 tff(c_11703, plain, (icext(uri_rdf_Property, uri_owl_minCardinality)=true)). % 39.17/27.86 tff(c_11650, plain, (iext(uri_rdf_type, uri_owl_minCardinality, uri_rdf_Property)=true)). % 39.17/27.86 tff(c_11595, plain, (iext(uri_rdf_type, uri_rdfs_seeAlso, uri_rdf_Property)=true)). % 39.17/27.86 tff(c_2002, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_95), true, icext(C_95, uri_rdfs_Seq), true)=true))). % 39.17/27.86 tff(c_11405, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdfs_Resource)=true)). % 39.17/27.86 tff(c_2026, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_95), true, icext(C_95, uri_rdf__1), true)=true))). % 39.17/27.86 tff(c_11229, plain, (icext(uri_rdf_Property, uri_ex_hasAncestor)=true)). % 39.17/27.86 tff(c_11176, plain, (iext(uri_rdf_type, uri_ex_hasAncestor, uri_rdf_Property)=true)). % 39.17/27.86 tff(c_1980, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_owl_minCardinality, C_95), true, icext(C_95, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z), true)=true))). % 39.17/27.86 tff(c_11080, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf)=true)). % 39.17/27.86 tff(c_2430, plain, (![C_99]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_99), true, icext(C_99, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z), true)=true))). % 39.17/27.86 tff(c_1606, plain, (![S_5, O_6]: (ifeq(iext(uri_ex_hasAncestor, S_5, O_6), true, true, true)=true))). % 39.17/27.86 tff(c_3359, plain, (![S_5, O_6]: (ifeq(iext(uri_owl_minCardinality, S_5, O_6), true, true, true)=true))). % 39.17/27.86 tff(c_10928, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdfs_ContainerMembershipProperty)=true)). % 39.17/27.86 tff(c_2371, plain, (![C_99]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_99), true, icext(C_99, uri_rdfs_ContainerMembershipProperty), true)=true))). % 39.17/27.86 tff(c_10863, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__1, uri_rdfs_member)=true)). % 39.17/27.86 tff(c_10792, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdfs_Literal)=true)). % 39.17/27.86 tff(c_2428, plain, (![C_99]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_99), true, icext(C_99, uri_rdf_Property), true)=true))). % 39.17/27.86 tff(c_10562, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Resource)=true)). % 39.17/27.86 tff(c_2007, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_95), true, icext(C_95, uri_rdf_type), true)=true))). % 39.17/27.86 tff(c_10411, plain, (icext(uri_rdf_Property, uri_rdfs_domain)=true)). % 39.17/27.86 tff(c_2025, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_95), true, icext(C_95, uri_rdfs_domain), true)=true))). % 39.17/27.86 tff(c_10238, plain, (iext(uri_rdfs_subClassOf, uri_ex_Person, uri_rdfs_Resource)=true)). % 39.17/27.86 tff(c_10085, plain, (icext(uri_rdf_Property, uri_rdfs_isDefinedBy)=true)). % 39.17/27.86 tff(c_10032, plain, (iext(uri_rdf_type, uri_rdfs_isDefinedBy, uri_rdf_Property)=true)). % 39.17/27.86 tff(c_9940, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__3, uri_rdfs_member)=true)). % 39.17/27.86 tff(c_2016, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_95), true, icext(C_95, uri_rdf_subject), true)=true))). % 39.17/27.86 tff(c_9875, plain, (iext(uri_rdfs_subPropertyOf, uri_owl_onProperty, uri_owl_onProperty)=true)). % 39.17/27.86 tff(c_9809, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_seeAlso, uri_rdfs_seeAlso)=true)). % 39.17/27.86 tff(c_9671, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Resource)=true)). % 39.17/27.86 tff(c_9533, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Resource)=true)). % 39.17/27.86 tff(c_2024, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_95), true, icext(C_95, uri_rdfs_seeAlso), true)=true))). % 39.17/27.86 tff(c_9439, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdf_Alt)=true)). % 39.17/27.86 tff(c_9400, plain, (ip(uri_rdfs_member)=true)). % 39.17/27.86 tff(c_9336, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__2, uri_rdfs_member)=true)). % 39.17/27.86 tff(c_2034, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_95), true, icext(C_95, uri_rdf_first), true)=true))). % 39.17/27.86 tff(c_9190, plain, (icext(uri_rdf_Property, uri_rdfs_seeAlso)=true)). % 39.17/27.86 tff(c_2402, plain, (![C_99]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_99), true, icext(C_99, uri_rdfs_seeAlso), true)=true))). % 39.17/27.86 tff(c_9028, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Resource)=true)). % 39.17/27.86 tff(c_8963, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_subject, uri_rdf_subject)=true)). % 39.17/27.86 tff(c_2372, plain, (![C_99]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_99), true, icext(C_99, uri_rdfs_Class), true)=true))). % 39.17/27.86 tff(c_8774, plain, (icext(uri_rdf_Property, uri_rdf_predicate)=true)). % 39.17/27.86 tff(c_2042, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_95), true, icext(C_95, uri_rdf_predicate), true)=true))). % 39.17/27.86 tff(c_8714, plain, (icext(uri_rdf_Property, uri_rdfs_subPropertyOf)=true)). % 39.17/27.86 tff(c_8661, plain, (iext(uri_rdf_type, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 39.17/27.86 tff(c_8605, plain, (iext(uri_rdf_type, uri_rdfs_subClassOf, uri_rdf_Property)=true)). % 39.17/27.86 tff(c_8539, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_first, uri_rdf_first)=true)). % 39.17/27.86 tff(c_8472, plain, (iext(uri_rdfs_subClassOf, uri_ex_Person, uri_ex_Person)=true)). % 39.17/27.86 tff(c_8381, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Container, uri_rdfs_Container)=true)). % 39.17/27.86 tff(c_2004, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_95), true, icext(C_95, uri_rdf_subject), true)=true))). % 39.17/27.86 tff(c_8268, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Resource)=true)). % 39.17/27.86 tff(c_8203, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_object, uri_rdf_object)=true)). % 39.17/27.86 tff(c_8110, plain, (ic(uri_rdfs_Statement)=true)). % 39.17/27.86 tff(c_8053, plain, (icext(uri_rdfs_Class, uri_rdfs_Statement)=true)). % 39.17/27.86 tff(c_2355, plain, (![C_99]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_99), true, icext(C_99, uri_rdfs_Statement), true)=true))). % 39.17/27.86 tff(c_7968, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdf_Bag)=true)). % 39.17/27.86 tff(c_7900, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdfs_Class)=true)). % 39.17/27.86 tff(c_1997, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_95), true, icext(C_95, uri_rdfs_label), true)=true))). % 39.17/27.86 tff(c_7804, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_type, uri_rdf_type)=true)). % 39.17/27.86 tff(c_7706, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdf_Property)=true)). % 39.17/27.86 tff(c_7636, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, uri_rdfs_isDefinedBy)=true)). % 39.17/27.86 tff(c_7544, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__1, uri_rdf__1)=true)). % 39.17/27.86 tff(c_2050, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_95), true, icext(C_95, uri_rdfs_Datatype), true)=true))). % 39.17/27.86 tff(c_7478, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Seq)=true)). % 39.17/27.86 tff(c_7372, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Resource)=true)). % 39.17/27.86 tff(c_2425, plain, (![C_99]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_99), true, icext(C_99, uri_rdfs_Resource), true)=true))). % 39.17/27.86 tff(c_7219, plain, (icext(uri_rdf_Property, uri_rdfs_subClassOf)=true)). % 39.17/27.86 tff(c_7134, plain, (iext(uri_rdfs_subClassOf, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, uri_rdfs_Resource)=true)). % 39.17/27.86 tff(c_2028, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_95), true, icext(C_95, uri_rdfs_subClassOf), true)=true))). % 39.17/27.86 tff(c_2576, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_subPropertyOf, S_5, O_6), true, true, true)=true))). % 39.17/27.86 tff(c_7028, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_rest, uri_rdf_rest)=true)). % 39.17/27.86 tff(c_2379, plain, (![C_99]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_99), true, icext(C_99, uri_rdfs_Resource), true)=true))). % 39.17/27.86 tff(c_6852, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_range, uri_rdfs_range)=true)). % 39.17/27.86 tff(c_3234, plain, (![S_5, O_6]: (ifeq(iext(uri_owl_onProperty, S_5, O_6), true, true, true)=true))). % 39.17/27.86 tff(c_6604, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__3, uri_rdf__3)=true)). % 39.17/27.86 tff(c_6479, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Container, uri_rdfs_Resource)=true)). % 39.17/27.86 tff(c_6414, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, uri_rdfs_subClassOf)=true)). % 39.17/27.86 tff(c_6348, plain, (iext(uri_rdfs_subClassOf, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)=true)). % 39.17/27.86 tff(c_6209, plain, (icext(uri_rdf_Property, uri_rdfs_label)=true)). % 39.17/27.86 tff(c_2031, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_95), true, icext(C_95, uri_rdfs_label), true)=true))). % 39.17/27.86 tff(c_6100, plain, (icext(sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, uri_ex_alice)=true)). % 39.17/27.86 tff(c_6058, plain, (icext(sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, uri_ex_bob)=true)). % 39.17/27.86 tff(c_1667, plain, (![X_92]: (ifeq(icext(uri_ex_Person, X_92), true, icext(sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, X_92), true)=true))). % 39.17/27.86 tff(c_871, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_subClassOf, S_5, O_6), true, true, true)=true))). % 39.17/27.86 tff(c_2077, plain, (![S_5, O_6]: (ifeq(iext(uri_rdf_object, S_5, O_6), true, true, true)=true))). % 39.17/27.86 tff(c_1690, plain, (![S_5, O_6]: (ifeq(iext(uri_rdf_rest, S_5, O_6), true, true, true)=true))). % 39.17/27.86 tff(c_5872, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, uri_rdfs_domain)=true)). % 39.17/27.86 tff(c_1664, plain, (![X_92]: (ifeq(icext(uri_rdf_Alt, X_92), true, icext(uri_rdfs_Container, X_92), true)=true))). % 39.17/27.86 tff(c_1666, plain, (![X_92]: (ifeq(icext(uri_rdf_Bag, X_92), true, icext(uri_rdfs_Container, X_92), true)=true))). % 39.17/27.86 tff(c_1665, plain, (![X_92]: (ifeq(icext(uri_rdfs_Datatype, X_92), true, icext(uri_rdfs_Class, X_92), true)=true))). % 39.17/27.86 tff(c_5610, plain, (icext(uri_rdf_Property, uri_rdfs_range)=true)). % 39.17/27.86 tff(c_5557, plain, (iext(uri_rdf_type, uri_rdfs_range, uri_rdf_Property)=true)). % 39.17/27.86 tff(c_1661, plain, (![X_92]: (ifeq(icext(uri_rdf_XMLLiteral, X_92), true, icext(uri_rdfs_Literal, X_92), true)=true))). % 39.17/27.86 tff(c_5471, plain, (icext(uri_rdfs_Class, uri_rdfs_Resource)=true)). % 39.17/27.86 tff(c_5393, plain, (ic(uri_rdfs_Resource)=true)). % 39.17/27.86 tff(c_5325, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdfs_Resource)=true)). % 39.17/27.86 tff(c_1662, plain, (![X_92]: (ifeq(icext(uri_rdfs_Seq, X_92), true, icext(uri_rdfs_Container, X_92), true)=true))). % 39.17/27.86 tff(c_1663, plain, (![X_92]: (ifeq(icext(uri_rdfs_ContainerMembershipProperty, X_92), true, icext(uri_rdf_Property, X_92), true)=true))). % 39.17/27.86 tff(c_2030, plain, (![X_96, Y_97]: (ifeq(iext(uri_rdfs_label, X_96, Y_97), true, true, true)=true))). % 39.17/27.86 tff(c_2414, plain, (![X_100, Y_101]: (ifeq(iext(uri_rdf_predicate, X_100, Y_101), true, true, true)=true))). % 39.17/27.86 tff(c_2006, plain, (![X_96, Y_97]: (ifeq(iext(uri_rdf_type, X_96, Y_97), true, true, true)=true))). % 39.17/27.86 tff(c_5010, plain, (![X_134]: (iext(uri_rdf_type, X_134, uri_rdfs_Resource)=true))). % 39.17/27.86 tff(c_2386, plain, (![X_100, Y_101]: (ifeq(iext(uri_rdf_subject, X_100, Y_101), true, true, true)=true))). % 39.17/27.86 tff(c_2010, plain, (![X_96, Y_97]: (ifeq(iext(uri_rdfs_comment, X_96, Y_97), true, true, true)=true))). % 39.17/27.86 tff(c_2398, plain, (![X_100, Y_101]: (ifeq(iext(uri_rdf__1, X_100, Y_101), true, true, true)=true))). % 39.17/27.86 tff(c_2038, plain, (![X_96, Y_97]: (ifeq(iext(uri_rdf__2, X_96, Y_97), true, true, true)=true))). % 39.17/27.86 tff(c_2388, plain, (![X_100, Y_101]: (ifeq(iext(uri_rdfs_isDefinedBy, X_100, Y_101), true, true, true)=true))). % 39.17/27.86 tff(c_2411, plain, (![X_100, Y_101]: (ifeq(iext(uri_rdf_value, X_100, Y_101), true, true, true)=true))). % 39.17/27.86 tff(c_4900, plain, (icext(uri_rdfs_Class, uri_rdfs_ContainerMembershipProperty)=true)). % 39.17/27.86 tff(c_2393, plain, (![X_100, Y_101]: (ifeq(iext(uri_rdfs_seeAlso, X_100, Y_101), true, true, true)=true))). % 39.17/27.86 tff(c_4855, plain, (icext(uri_rdfs_Class, uri_rdf_XMLLiteral)=true)). % 39.17/27.86 tff(c_4810, plain, (icext(uri_rdfs_Class, uri_rdfs_Literal)=true)). % 39.17/27.86 tff(c_2424, plain, (![X_100, Y_101]: (ifeq(iext(uri_rdfs_member, X_100, Y_101), true, true, true)=true))). % 39.17/27.86 tff(c_4757, plain, (icext(uri_rdfs_Class, uri_rdfs_Datatype)=true)). % 39.17/27.86 tff(c_4702, plain, (icext(uri_rdfs_Class, uri_rdf_Alt)=true)). % 39.17/27.86 tff(c_4643, plain, (icext(uri_rdfs_Class, uri_rdfs_Class)=true)). % 39.17/27.86 tff(c_4596, plain, (icext(uri_rdfs_Class, uri_rdfs_Container)=true)). % 39.17/27.86 tff(c_1614, plain, (tuple(true, iext(uri_ex_hasAncestor, uri_ex_bob, uri_ex_bob))!=tuple(true, true))). % 39.17/27.86 tff(c_4549, plain, (icext(uri_rdfs_Class, uri_rdfs_Seq)=true)). % 39.17/27.86 tff(c_4502, plain, (icext(uri_rdfs_Class, uri_ex_Person)=true)). % 39.17/27.86 tff(c_2012, plain, (![X_96, Y_97]: (ifeq(iext(uri_rdf__3, X_96, Y_97), true, true, true)=true))). % 39.17/27.86 tff(c_4447, plain, (icext(uri_rdfs_Class, uri_rdf_Bag)=true)). % 39.17/27.86 tff(c_4400, plain, (icext(uri_rdfs_Class, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)=true)). % 39.17/27.86 tff(c_2405, plain, (![X_100, Y_101]: (ifeq(iext(uri_rdf_first, X_100, Y_101), true, true, true)=true))). % 39.17/27.86 tff(c_4354, plain, (icext(uri_rdf_Property, uri_rdf__3)=true)). % 39.17/27.86 tff(c_4311, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__1)=true)). % 39.17/27.86 tff(c_4269, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__2)=true)). % 39.17/27.86 tff(c_4225, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__3)=true)). % 39.17/27.86 tff(c_4182, plain, (icext(uri_ex_Person, uri_ex_bob)=true)). % 39.17/27.86 tff(c_4144, plain, (icext(uri_rdf_Property, uri_rdf__1)=true)). % 39.17/27.86 tff(c_4104, plain, (icext(uri_rdf_Property, uri_rdf_subject)=true)). % 39.17/27.86 tff(c_4066, plain, (icext(uri_rdf_Property, uri_rdf_type)=true)). % 39.17/27.86 tff(c_4028, plain, (icext(uri_rdf_List, uri_rdf_nil)=true)). % 39.17/27.86 tff(c_3989, plain, (icext(uri_rdf_Property, uri_rdf_object)=true)). % 39.17/27.86 tff(c_3948, plain, (icext(uri_rdf_Property, uri_rdf_first)=true)). % 39.17/27.86 tff(c_3905, plain, (icext(uri_rdfs_Datatype, uri_rdf_XMLLiteral)=true)). % 39.17/27.86 tff(c_3868, plain, (icext(uri_rdf_Property, uri_rdf__2)=true)). % 39.17/27.86 tff(c_3829, plain, (icext(uri_rdf_Property, uri_rdf_value)=true)). % 39.17/27.86 tff(c_3769, plain, (icext(uri_rdfs_Class, uri_rdf_Property)=true)). % 39.17/27.86 tff(c_3715, plain, (icext(uri_owl_TransitiveProperty, uri_ex_hasAncestor)=true)). % 39.17/27.86 tff(c_3678, plain, (icext(uri_owl_Restriction, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)=true)). % 39.17/27.86 tff(c_3641, plain, (icext(uri_rdf_Property, uri_rdf_rest)=true)). % 39.17/27.86 tff(c_3604, plain, (icext(uri_ex_Person, uri_ex_alice)=true)). % 39.17/27.86 tff(c_3567, plain, (ic(uri_rdfs_Class)=true)). % 39.17/27.86 tff(c_3527, plain, (ic(uri_rdf_Bag)=true)). % 39.17/27.86 tff(c_3490, plain, (ic(uri_rdfs_Seq)=true)). % 39.17/27.86 tff(c_3454, plain, (ip(uri_rdfs_isDefinedBy)=true)). % 39.17/27.86 tff(c_3418, plain, (ic(uri_rdf_Alt)=true)). % 39.17/27.86 tff(c_3378, plain, (ip(uri_rdf_subject)=true)). % 39.17/27.86 tff(c_3331, plain, (ip(uri_owl_minCardinality)=true)). % 39.17/27.86 tff(c_3280, plain, (ic(uri_rdfs_Literal)=true)). % 39.17/27.86 tff(c_3243, plain, (ic(uri_rdfs_Datatype)=true)). % 39.17/27.86 tff(c_3206, plain, (ip(uri_owl_onProperty)=true)). % 39.17/27.86 tff(c_3170, plain, (ip(uri_rdf_first)=true)). % 39.17/27.86 tff(c_3135, plain, (ic(uri_rdf_Property)=true)). % 39.17/27.86 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))). % 39.17/27.86 tff(c_2603, plain, (ip(uri_rdf__2)=true)). % 39.17/27.86 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))). % 39.17/27.86 tff(c_2549, plain, (ip(uri_rdfs_subPropertyOf)=true)). % 39.17/27.86 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))). % 39.17/27.86 tff(c_2435, plain, (ip(uri_rdfs_seeAlso)=true)). % 39.17/27.86 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))). % 39.17/27.86 tff(c_1702, plain, (ip(uri_rdf_object)=true)). % 39.17/27.86 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))). % 39.17/27.86 tff(c_1624, plain, (ip(uri_rdf_rest)=true)). % 39.17/27.86 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))). % 39.17/27.86 tff(c_198, plain, (![BNODE_x_55]: (tuple(iext(uri_ex_hasAncestor, uri_ex_alice, BNODE_x_55), iext(uri_ex_hasAncestor, uri_ex_bob, BNODE_x_55))!=tuple(true, true)))). % 39.17/27.86 tff(c_1579, plain, (ip(uri_ex_hasAncestor)=true)). % 39.17/27.86 tff(c_1475, plain, (ip(uri_rdf__3)=true)). % 39.17/27.86 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))). % 39.17/27.86 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))). % 39.17/27.86 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))). % 39.17/27.86 tff(c_1417, plain, (ic(uri_rdfs_Container)=true)). % 39.17/27.86 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))). % 39.17/27.87 tff(c_1285, plain, (ic(sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)=true)). % 39.17/27.87 tff(c_156, plain, (![C_39]: (ifeq(ic(C_39), true, iext(uri_rdfs_subClassOf, C_39, C_39), true)=true))). % 39.17/27.87 tff(c_1199, plain, (ip(uri_rdf_value)=true)). % 39.17/27.87 tff(c_150, plain, (![C_35, D_36]: (ifeq(iext(uri_rdfs_subClassOf, C_35, D_36), true, ic(D_36), true)=true))). % 39.17/27.87 tff(c_1162, plain, (ip(uri_rdf__1)=true)). % 39.17/27.87 tff(c_28, plain, (![P_9]: (ifeq(ip(P_9), true, iext(uri_rdf_type, P_9, uri_rdf_Property), true)=true))). % 39.17/27.87 tff(c_1044, plain, (ip(uri_rdf_type)=true)). % 39.17/27.87 tff(c_164, plain, (![P_45, Q_46]: (ifeq(iext(uri_rdfs_subPropertyOf, P_45, Q_46), true, ip(P_45), true)=true))). % 39.17/27.87 tff(c_986, plain, (ic(uri_ex_Person)=true)). % 39.17/27.87 tff(c_162, plain, (![P_43, Q_44]: (ifeq(iext(uri_rdfs_subPropertyOf, P_43, Q_44), true, ip(Q_44), true)=true))). % 39.17/27.87 tff(c_947, plain, (ip(uri_rdfs_domain)=true)). % 39.17/27.87 tff(c_170, plain, (![P_51]: (ifeq(ip(P_51), true, iext(uri_rdfs_subPropertyOf, P_51, P_51), true)=true))). % 39.17/27.87 tff(c_924, plain, (ip(uri_rdfs_range)=true)). % 39.17/27.87 tff(c_30, plain, (![P_10]: (ifeq(iext(uri_rdf_type, P_10, uri_rdf_Property), true, ip(P_10), true)=true))). % 39.17/27.87 tff(c_859, plain, (ip(uri_rdfs_subClassOf)=true)). % 39.17/27.87 tff(c_4, plain, (![P_4, S_5, O_6]: (ifeq(iext(P_4, S_5, O_6), true, ip(P_4), true)=true))). % 39.17/27.87 tff(c_622, plain, (ic(uri_rdfs_ContainerMembershipProperty)=true)). % 39.17/27.87 tff(c_593, plain, (ic(uri_rdf_XMLLiteral)=true)). % 39.17/27.87 tff(c_152, plain, (![C_37, D_38]: (ifeq(iext(uri_rdfs_subClassOf, C_37, D_38), true, ic(C_37), true)=true))). % 39.17/27.87 tff(c_58, plain, (![C_15]: (ifeq(ic(C_15), true, iext(uri_rdfs_subClassOf, C_15, uri_rdfs_Resource), true)=true))). % 39.17/27.87 tff(c_114, plain, (![X_22]: (ifeq(ic(X_22), true, icext(uri_rdfs_Class, X_22), true)=true))). % 39.17/27.87 tff(c_116, plain, (![X_23]: (ifeq(icext(uri_rdfs_Class, X_23), true, ic(X_23), true)=true))). % 39.17/27.87 tff(c_122, plain, (![X_26]: (ifeq(icext(uri_rdfs_Literal, X_26), true, lv(X_26), true)=true))). % 39.17/27.87 tff(c_124, plain, (![X_27]: (ifeq(lv(X_27), true, icext(uri_rdfs_Literal, X_27), true)=true))). % 39.17/27.87 tff(c_507, plain, (![X_62]: (icext(uri_rdfs_Resource, X_62)=true))). % 39.17/27.87 tff(c_182, plain, (iext(uri_owl_minCardinality, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, literal_typed(dat_str_1, uri_xsd_nonNegativeInteger))=true)). % 39.17/27.87 tff(c_201, plain, (![X_8]: (ifeq(lv(X_8), true, true, true)=true))). % 39.17/27.87 tff(c_2, plain, (![A_1, B_2, C_3]: (ifeq(A_1, A_1, B_2, C_3)=B_2))). % 39.17/27.87 tff(c_138, plain, (iext(uri_rdfs_domain, uri_rdf_predicate, uri_rdfs_Statement)=true)). % 39.17/27.87 tff(c_12, plain, (iext(uri_rdf_type, uri_rdf_nil, uri_rdf_List)=true)). % 39.17/27.87 tff(c_194, plain, (iext(uri_ex_hasAncestor, uri_ex_alice, uri_ex_bob)=true)). % 39.17/27.87 tff(c_154, plain, (iext(uri_rdfs_range, uri_rdfs_subClassOf, uri_rdfs_Class)=true)). % 39.17/27.87 tff(c_100, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Literal)=true)). % 39.17/27.87 tff(c_18, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdf_Property)=true)). % 39.17/27.87 tff(c_10, plain, (iext(uri_rdf_type, uri_rdf_first, uri_rdf_Property)=true)). % 39.17/27.87 tff(c_178, plain, (iext(uri_rdfs_domain, uri_rdf_value, uri_rdfs_Resource)=true)). % 39.17/27.87 tff(c_176, plain, (iext(uri_rdfs_range, uri_rdf_type, uri_rdfs_Class)=true)). % 39.17/27.87 tff(c_22, plain, (iext(uri_rdf_type, uri_rdf_object, uri_rdf_Property)=true)). % 39.17/27.87 tff(c_96, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdfs_ContainerMembershipProperty)=true)). % 39.17/27.87 tff(c_188, plain, (iext(uri_rdf_type, uri_ex_bob, uri_ex_Person)=true)). % 39.17/27.87 tff(c_16, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdf_Property)=true)). % 39.17/27.87 tff(c_64, plain, (iext(uri_rdfs_domain, uri_rdf_rest, uri_rdf_List)=true)). % 39.17/27.87 tff(c_60, plain, (iext(uri_rdfs_domain, uri_rdf_first, uri_rdf_List)=true)). % 39.17/27.87 tff(c_48, plain, (iext(uri_rdfs_range, uri_rdfs_label, uri_rdfs_Literal)=true)). % 39.17/27.87 tff(c_92, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdfs_ContainerMembershipProperty)=true)). % 39.17/27.87 tff(c_132, plain, (iext(uri_rdfs_range, uri_rdfs_range, uri_rdfs_Class)=true)). % 39.17/27.87 tff(c_102, plain, (iext(uri_rdf_type, uri_rdf_XMLLiteral, uri_rdfs_Datatype)=true)). % 39.17/27.87 tff(c_126, plain, (iext(uri_rdf_type, uri_rdf_Property, uri_rdfs_Class)=true)). % 39.17/27.87 tff(c_98, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Container)=true)). % 39.17/27.87 tff(c_128, plain, (iext(uri_rdfs_domain, uri_rdfs_range, uri_rdf_Property)=true)). % 39.17/27.87 tff(c_142, plain, (iext(uri_rdfs_domain, uri_rdf_subject, uri_rdfs_Statement)=true)). % 39.17/27.87 tff(c_38, plain, (iext(uri_rdfs_range, uri_rdfs_comment, uri_rdfs_Literal)=true)). % 39.17/27.87 tff(c_174, plain, (iext(uri_rdfs_domain, uri_rdf_type, uri_rdfs_Resource)=true)). % 39.17/27.87 tff(c_76, plain, (iext(uri_rdfs_domain, uri_rdfs_member, uri_rdfs_Resource)=true)). % 39.17/27.87 tff(c_36, plain, (iext(uri_rdfs_domain, uri_rdfs_comment, uri_rdfs_Resource)=true)). % 39.17/27.87 tff(c_84, plain, (iext(uri_rdfs_domain, uri_rdf__3, uri_rdfs_Resource)=true)). % 39.17/27.87 tff(c_192, plain, (iext(uri_rdf_type, uri_ex_hasAncestor, uri_owl_TransitiveProperty)=true)). % 39.17/27.87 tff(c_88, plain, (iext(uri_rdfs_range, uri_rdf__2, uri_rdfs_Resource)=true)). % 39.17/27.87 tff(c_144, plain, (iext(uri_rdfs_range, uri_rdf_subject, uri_rdfs_Resource)=true)). % 39.17/27.87 tff(c_42, plain, (iext(uri_rdfs_range, uri_rdfs_isDefinedBy, uri_rdfs_Resource)=true)). % 39.17/27.87 tff(c_80, plain, (iext(uri_rdfs_domain, uri_rdf__1, uri_rdfs_Resource)=true)). % 39.17/27.87 tff(c_90, plain, (iext(uri_rdfs_range, uri_rdf__3, uri_rdfs_Resource)=true)). % 39.17/27.87 tff(c_52, plain, (iext(uri_rdfs_range, uri_rdfs_seeAlso, uri_rdfs_Resource)=true)). % 39.17/27.87 tff(c_94, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdfs_ContainerMembershipProperty)=true)). % 39.17/27.87 tff(c_50, plain, (iext(uri_rdfs_domain, uri_rdfs_seeAlso, uri_rdfs_Resource)=true)). % 39.17/27.87 tff(c_108, plain, (iext(uri_rdfs_domain, uri_rdfs_domain, uri_rdf_Property)=true)). % 39.17/27.87 tff(c_86, plain, (iext(uri_rdfs_range, uri_rdf__1, uri_rdfs_Resource)=true)). % 39.17/27.87 tff(c_20, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdf_Property)=true)). % 39.17/27.87 tff(c_146, plain, (iext(uri_rdfs_domain, uri_rdfs_subClassOf, uri_rdfs_Class)=true)). % 39.17/27.87 tff(c_44, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso)=true)). % 39.17/27.87 tff(c_46, plain, (iext(uri_rdfs_domain, uri_rdfs_label, uri_rdfs_Resource)=true)). % 39.17/27.87 tff(c_40, plain, (iext(uri_rdfs_domain, uri_rdfs_isDefinedBy, uri_rdfs_Resource)=true)). % 39.17/27.87 tff(c_62, plain, (iext(uri_rdfs_range, uri_rdf_first, uri_rdfs_Resource)=true)). % 39.17/27.87 tff(c_160, plain, (iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 39.17/27.87 tff(c_26, plain, (iext(uri_rdf_type, uri_rdf_subject, uri_rdf_Property)=true)). % 39.17/27.87 tff(c_74, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property)=true)). % 39.17/27.87 tff(c_82, plain, (iext(uri_rdfs_domain, uri_rdf__2, uri_rdfs_Resource)=true)). % 39.17/27.87 tff(c_180, plain, (iext(uri_rdfs_range, uri_rdf_value, uri_rdfs_Resource)=true)). % 39.17/27.87 tff(c_24, plain, (iext(uri_rdf_type, uri_rdf_value, uri_rdf_Property)=true)). % 39.17/27.87 tff(c_140, plain, (iext(uri_rdfs_range, uri_rdf_predicate, uri_rdfs_Resource)=true)). % 39.17/27.87 tff(c_186, plain, (iext(uri_rdf_type, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, uri_owl_Restriction)=true)). % 39.17/27.87 tff(c_66, plain, (iext(uri_rdfs_range, uri_rdf_rest, uri_rdf_List)=true)). % 39.17/27.87 tff(c_14, plain, (iext(uri_rdf_type, uri_rdf_rest, uri_rdf_Property)=true)). % 39.17/27.87 tff(c_34, plain, (iext(uri_rdf_type, uri_rdf_type, uri_rdf_Property)=true)). % 39.17/27.87 tff(c_190, plain, (iext(uri_rdf_type, uri_ex_alice, uri_ex_Person)=true)). % 39.17/27.87 tff(c_112, plain, (iext(uri_rdfs_range, uri_rdfs_domain, uri_rdfs_Class)=true)). % 39.17/27.87 tff(c_68, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Container)=true)). % 39.17/27.87 tff(c_106, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Class)=true)). % 39.17/27.87 tff(c_78, plain, (iext(uri_rdfs_range, uri_rdfs_member, uri_rdfs_Resource)=true)). % 39.17/27.87 tff(c_70, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Container)=true)). % 39.17/27.87 tff(c_134, plain, (iext(uri_rdfs_domain, uri_rdf_object, uri_rdfs_Statement)=true)). % 39.17/27.87 tff(c_168, plain, (iext(uri_rdfs_range, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 39.17/27.87 tff(c_184, plain, (iext(uri_owl_onProperty, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, uri_ex_hasAncestor)=true)). % 39.17/27.87 tff(c_196, plain, (iext(uri_rdfs_subClassOf, uri_ex_Person, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)=true)). % 39.17/27.87 tff(c_6, plain, (![X_7]: (ir(X_7)=true))). % 39.17/27.87 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 39.17/27.87 %------------------------------------------------------------------------------