%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SWB025-10 : TPTP v9.0.0. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n026.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 40.21s 27.52s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.12 % Problem : SWB025-10 : TPTP v9.0.0. Released v7.5.0. % 0.08/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.12/0.34 % Computer : n026.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Wed Apr 9 01:02:08 EDT 2025 % 0.12/0.34 % CPUTime : % 40.21/27.52 % 40.21/27.52 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 40.21/27.52 % 40.21/27.52 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 40.21/27.54 %$ ifeq > iext > tuple > icext > #nlpp > lv > ir > ip > ic > uri_rdfs_subPropertyOf > uri_rdfs_subClassOf > uri_rdfs_seeAlso > uri_rdfs_range > uri_rdfs_member > uri_rdfs_label > uri_rdfs_isDefinedBy > uri_rdfs_domain > uri_rdfs_comment > uri_rdfs_Statement > uri_rdfs_Seq > uri_rdfs_Resource > uri_rdfs_Literal > uri_rdfs_Datatype > uri_rdfs_ContainerMembershipProperty > uri_rdfs_Container > uri_rdfs_Class > uri_rdf_value > uri_rdf_type > uri_rdf_subject > uri_rdf_rest > uri_rdf_predicate > uri_rdf_object > uri_rdf_nil > uri_rdf_first > uri_rdf__3 > uri_rdf__2 > uri_rdf__1 > uri_rdf_XMLLiteral > uri_rdf_Property > uri_rdf_List > uri_rdf_Bag > uri_rdf_Alt > uri_owl_propertyChainAxiom > uri_owl_inverseOf > uri_ex_hasUncle > uri_ex_hasFather > uri_ex_hasCousin > uri_ex_dave > uri_ex_charly > uri_ex_bob > uri_ex_alice > true > sK5_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l12 > sK4_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l11 > sK3_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l22 > sK2_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l21 > sK1_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l3 % 40.21/27.54 % 40.21/27.54 %Foreground sorts: % 40.21/27.54 % 40.21/27.54 % 40.21/27.54 %Background operators: % 40.21/27.54 % 40.21/27.54 % 40.21/27.54 %Foreground operators: % 40.21/27.54 tff(uri_rdfs_Datatype, type, uri_rdfs_Datatype: $i). % 40.21/27.54 tff(uri_rdfs_ContainerMembershipProperty, type, uri_rdfs_ContainerMembershipProperty: $i). % 40.21/27.54 tff(uri_rdfs_Resource, type, uri_rdfs_Resource: $i). % 40.21/27.54 tff(uri_rdf_Property, type, uri_rdf_Property: $i). % 40.21/27.54 tff(uri_rdf_subject, type, uri_rdf_subject: $i). % 40.21/27.54 tff(uri_rdf_type, type, uri_rdf_type: $i). % 40.21/27.54 tff(uri_rdfs_subPropertyOf, type, uri_rdfs_subPropertyOf: $i). % 40.21/27.54 tff(sK4_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l11, type, sK4_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l11: $i). % 40.21/27.54 tff(uri_rdfs_seeAlso, type, uri_rdfs_seeAlso: $i). % 40.21/27.54 tff(icext, type, icext: ($i * $i) > $i). % 40.21/27.54 tff(uri_ex_hasUncle, type, uri_ex_hasUncle: $i). % 40.21/27.54 tff(uri_rdfs_range, type, uri_rdfs_range: $i). % 40.21/27.54 tff(uri_rdf_XMLLiteral, type, uri_rdf_XMLLiteral: $i). % 40.21/27.54 tff(uri_rdf_List, type, uri_rdf_List: $i). % 40.21/27.54 tff(uri_rdf_first, type, uri_rdf_first: $i). % 40.21/27.54 tff(uri_ex_charly, type, uri_ex_charly: $i). % 40.21/27.54 tff(uri_rdf_predicate, type, uri_rdf_predicate: $i). % 40.21/27.54 tff(uri_ex_hasCousin, type, uri_ex_hasCousin: $i). % 40.21/27.54 tff(tuple, type, tuple: ($i * $i) > $i). % 40.21/27.54 tff(ir, type, ir: $i > $i). % 40.21/27.54 tff(lv, type, lv: $i > $i). % 40.21/27.54 tff(uri_owl_inverseOf, type, uri_owl_inverseOf: $i). % 40.21/27.54 tff(uri_ex_bob, type, uri_ex_bob: $i). % 40.21/27.54 tff(uri_rdf__3, type, uri_rdf__3: $i). % 40.21/27.54 tff(sK5_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l12, type, sK5_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l12: $i). % 40.21/27.54 tff(uri_rdf_value, type, uri_rdf_value: $i). % 40.21/27.54 tff(ic, type, ic: $i > $i). % 40.21/27.54 tff(uri_rdfs_Statement, type, uri_rdfs_Statement: $i). % 40.21/27.54 tff(uri_ex_hasFather, type, uri_ex_hasFather: $i). % 40.21/27.54 tff(uri_rdf__1, type, uri_rdf__1: $i). % 40.21/27.54 tff(sK2_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l21, type, sK2_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l21: $i). % 40.21/27.54 tff(iext, type, iext: ($i * $i * $i) > $i). % 40.21/27.54 tff(sK1_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l3, type, sK1_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l3: $i). % 40.21/27.54 tff(uri_ex_alice, type, uri_ex_alice: $i). % 40.21/27.54 tff(uri_rdf_rest, type, uri_rdf_rest: $i). % 40.21/27.54 tff(uri_rdfs_label, type, uri_rdfs_label: $i). % 40.21/27.54 tff(uri_rdfs_Container, type, uri_rdfs_Container: $i). % 40.21/27.54 tff(uri_owl_propertyChainAxiom, type, uri_owl_propertyChainAxiom: $i). % 40.21/27.54 tff(uri_rdfs_subClassOf, type, uri_rdfs_subClassOf: $i). % 40.21/27.54 tff(sK3_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l22, type, sK3_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l22: $i). % 40.21/27.54 tff(uri_rdf_object, type, uri_rdf_object: $i). % 40.21/27.54 tff(ip, type, ip: $i > $i). % 40.21/27.54 tff(uri_rdfs_Class, type, uri_rdfs_Class: $i). % 40.21/27.54 tff(uri_rdfs_Seq, type, uri_rdfs_Seq: $i). % 40.21/27.54 tff(uri_ex_dave, type, uri_ex_dave: $i). % 40.21/27.54 tff(uri_rdfs_member, type, uri_rdfs_member: $i). % 40.21/27.54 tff(uri_rdf_Bag, type, uri_rdf_Bag: $i). % 40.21/27.54 tff(uri_rdf__2, type, uri_rdf__2: $i). % 40.21/27.54 tff(uri_rdfs_comment, type, uri_rdfs_comment: $i). % 40.21/27.54 tff(uri_rdfs_Literal, type, uri_rdfs_Literal: $i). % 40.21/27.54 tff(true, type, true: $i). % 40.21/27.54 tff(uri_rdf_Alt, type, uri_rdf_Alt: $i). % 40.21/27.54 tff(uri_rdf_nil, type, uri_rdf_nil: $i). % 40.21/27.54 tff(uri_rdfs_isDefinedBy, type, uri_rdfs_isDefinedBy: $i). % 40.21/27.54 tff(uri_rdfs_domain, type, uri_rdfs_domain: $i). % 40.21/27.54 tff(ifeq, type, ifeq: ($i * $i * $i * $i) > $i). % 40.21/27.54 % 40.21/27.54 %Saturated clause set: % 40.21/27.54 tff(c_15899, 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))). % 40.21/27.54 tff(c_81678, plain, (![X_1339, Y_1340]: (ifeq(iext(uri_rdfs_comment, X_1339, Y_1340), true, iext(uri_rdfs_comment, X_1339, Y_1340), true)=true))). % 40.21/27.54 tff(c_20726, 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))). % 40.21/27.54 tff(c_15846, 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))). % 40.21/27.54 tff(c_81380, plain, (![X_1333, Y_1334]: (ifeq(iext(uri_rdf_predicate, X_1333, Y_1334), true, iext(uri_rdf_predicate, X_1333, Y_1334), true)=true))). % 40.21/27.54 tff(c_15781, 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))). % 40.21/27.54 tff(c_81217, plain, (![X_1328, Y_1329]: (ifeq(iext(uri_rdfs_label, X_1328, Y_1329), true, iext(uri_rdfs_label, X_1328, Y_1329), true)=true))). % 40.21/27.55 tff(c_5851, 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))). % 40.21/27.55 tff(c_80910, plain, (![X_1322, Y_1323]: (ifeq(iext(uri_rdfs_member, X_1322, Y_1323), true, iext(uri_rdfs_member, X_1322, Y_1323), true)=true))). % 40.21/27.55 tff(c_5848, 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))). % 40.21/27.55 tff(c_15704, 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))). % 40.21/27.55 tff(c_15638, 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))). % 40.21/27.55 tff(c_15287, 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))). % 40.21/27.55 tff(c_15445, 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))). % 40.21/27.55 tff(c_15354, 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))). % 40.21/27.55 tff(c_79941, plain, (![C_1313]: (ifeq(iext(uri_rdfs_subClassOf, C_1313, uri_rdfs_Statement), true, iext(uri_rdfs_subClassOf, C_1313, uri_rdfs_Resource), true)=true))). % 40.21/27.55 tff(c_15100, 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))). % 40.21/27.55 tff(c_79662, plain, (![C_1310]: (ifeq(iext(uri_rdfs_subClassOf, C_1310, uri_rdf_List), true, iext(uri_rdfs_subClassOf, C_1310, uri_rdfs_Resource), true)=true))). % 40.21/27.55 tff(c_5221, 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))). % 40.21/27.55 tff(c_14814, 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))). % 40.21/27.55 tff(c_5389, 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))). % 40.21/27.55 tff(c_6004, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_owl_inverseOf, Y_21), true, true, true), true)=true))). % 40.21/27.55 tff(c_7666, 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))). % 40.21/27.55 tff(c_10479, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_ex_hasFather, Y_21), true, true, true), true)=true))). % 40.21/27.55 tff(c_15042, 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))). % 40.21/27.55 tff(c_5224, 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))). % 40.21/27.55 tff(c_6720, 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))). % 40.21/27.55 tff(c_14365, 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))). % 40.21/27.55 tff(c_5392, 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))). % 40.21/27.55 tff(c_10482, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_ex_hasFather), true, true, true), true)=true))). % 40.21/27.55 tff(c_12904, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_ex_hasUncle, Y_21), true, true, true), true)=true))). % 40.21/27.55 tff(c_10737, 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))). % 40.21/27.55 tff(c_14765, 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))). % 40.21/27.55 tff(c_12712, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_ex_hasCousin), true, true, true), true)=true))). % 40.21/27.55 tff(c_7663, 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))). % 40.21/27.55 tff(c_10734, 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))). % 40.21/27.55 tff(c_14698, 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))). % 40.21/27.55 tff(c_12709, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_ex_hasCousin, Y_21), true, true, true), true)=true))). % 40.21/27.55 tff(c_6007, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_owl_inverseOf), true, true, true), true)=true))). % 40.21/27.55 tff(c_6723, 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))). % 40.21/27.55 tff(c_14930, 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))). % 40.21/27.55 tff(c_7200, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_owl_propertyChainAxiom), true, true, true), true)=true))). % 40.21/27.55 tff(c_12907, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_ex_hasUncle), true, true, true), true)=true))). % 40.21/27.55 tff(c_14313, 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))). % 40.21/27.55 tff(c_14883, 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))). % 40.21/27.55 tff(c_7197, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_owl_propertyChainAxiom, Y_21), true, true, true), true)=true))). % 40.21/27.55 tff(c_14977, 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))). % 40.21/27.55 tff(c_18230, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, sK2_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l21, uri_rdf_List), true, true, true), true)=true))). % 40.21/27.55 tff(c_14240, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, sK4_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l11, uri_rdf_List), true, true, true), true)=true))). % 40.21/27.55 tff(c_14193, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, sK5_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l12, uri_rdf_List), true, true, true), true)=true))). % 40.21/27.55 tff(c_13992, 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))). % 40.21/27.55 tff(c_20468, 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))). % 40.21/27.55 tff(c_14650, 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))). % 40.21/27.55 tff(c_17386, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, sK3_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l22, uri_rdf_List), true, true, true), true)=true))). % 40.21/27.55 tff(c_13937, 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))). % 40.21/27.55 tff(c_13865, 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))). % 40.21/27.55 tff(c_14093, 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))). % 40.21/27.55 tff(c_5335, 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))). % 40.21/27.55 tff(c_10937, 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))). % 40.21/27.55 tff(c_8601, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_ex_hasFather, uri_ex_hasFather), true, true, true), true)=true))). % 40.21/27.55 tff(c_73568, plain, (![X_1243, Y_1244]: (ifeq(iext(uri_rdf__3, X_1243, Y_1244), true, iext(uri_rdfs_member, X_1243, Y_1244), true)=true))). % 40.21/27.55 tff(c_11445, 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))). % 40.21/27.55 tff(c_4355, 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))). % 40.21/27.56 tff(c_11619, 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))). % 40.21/27.56 tff(c_4604, 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))). % 40.21/27.56 tff(c_10150, 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))). % 40.21/27.56 tff(c_13792, 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))). % 40.21/27.56 tff(c_72639, plain, (![C_1234]: (ifeq(iext(uri_rdfs_subClassOf, C_1234, uri_rdf_Bag), true, iext(uri_rdfs_subClassOf, C_1234, uri_rdfs_Resource), true)=true))). % 40.21/27.56 tff(c_72486, plain, (![C_1230]: (ifeq(iext(uri_rdfs_subClassOf, C_1230, uri_rdfs_ContainerMembershipProperty), true, iext(uri_rdfs_subClassOf, C_1230, uri_rdfs_Resource), true)=true))). % 40.21/27.56 tff(c_72473, plain, (![X_1228, Y_1229]: (ifeq(iext(uri_rdfs_seeAlso, X_1228, Y_1229), true, iext(uri_rdfs_seeAlso, X_1228, Y_1229), true)=true))). % 40.41/27.56 tff(c_11000, 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))). % 40.41/27.56 tff(c_4512, 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))). % 40.41/27.56 tff(c_6227, 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))). % 40.41/27.56 tff(c_4661, 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))). % 40.41/27.56 tff(c_71873, plain, (![X_1218, Y_1219]: (ifeq(iext(uri_rdf_object, X_1218, Y_1219), true, iext(uri_rdf_object, X_1218, Y_1219), true)=true))). % 40.41/27.56 tff(c_7780, 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))). % 40.41/27.56 tff(c_4413, 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))). % 40.41/27.56 tff(c_6428, 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))). % 40.41/27.56 tff(c_12601, 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))). % 40.41/27.56 tff(c_71291, plain, (![X_1209, Y_1210]: (ifeq(iext(uri_rdf__3, X_1209, Y_1210), true, iext(uri_rdf__3, X_1209, Y_1210), true)=true))). % 40.41/27.56 tff(c_71152, plain, (![C_1207]: (ifeq(iext(uri_rdfs_subClassOf, C_1207, uri_rdf_Alt), true, iext(uri_rdfs_subClassOf, C_1207, uri_rdfs_Resource), true)=true))). % 40.41/27.56 tff(c_70541, plain, (![X_1203, Y_1204]: (ifeq(iext(uri_rdfs_subClassOf, X_1203, Y_1204), true, iext(uri_rdfs_subClassOf, X_1203, Y_1204), true)=true))). % 40.41/27.56 tff(c_4509, 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))). % 40.41/27.56 tff(c_70341, plain, (![X_1197, Y_1198]: (ifeq(iext(uri_ex_hasUncle, X_1197, Y_1198), true, iext(uri_ex_hasUncle, X_1197, Y_1198), true)=true))). % 40.41/27.56 tff(c_6551, 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))). % 40.41/27.56 tff(c_4710, 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))). % 40.41/27.56 tff(c_8342, 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))). % 40.41/27.56 tff(c_6986, 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))). % 40.41/27.56 tff(c_69426, plain, (![C_1188]: (ifeq(iext(uri_rdfs_subClassOf, C_1188, uri_rdfs_Literal), true, iext(uri_rdfs_subClassOf, C_1188, uri_rdfs_Resource), true)=true))). % 40.41/27.56 tff(c_5943, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_owl_inverseOf, uri_rdf_Property), true, true, true), true)=true))). % 40.41/27.56 tff(c_8284, 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))). % 40.41/27.56 tff(c_4410, 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))). % 40.41/27.56 tff(c_10328, 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))). % 40.41/27.56 tff(c_68008, plain, (![X_1177, Y_1178]: (ifeq(iext(uri_rdfs_subPropertyOf, X_1177, Y_1178), true, iext(uri_rdfs_subPropertyOf, X_1177, Y_1178), true)=true))). % 40.41/27.56 tff(c_11512, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_owl_propertyChainAxiom, uri_owl_propertyChainAxiom), true, true, true), true)=true))). % 40.41/27.56 tff(c_4713, 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))). % 40.41/27.56 tff(c_13183, 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))). % 40.41/27.56 tff(c_12049, 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))). % 40.41/27.56 tff(c_4758, 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))). % 40.41/27.56 tff(c_67232, plain, (![P_1168]: (ifeq(iext(uri_rdfs_subPropertyOf, P_1168, uri_rdf__1), true, iext(uri_rdfs_subPropertyOf, P_1168, uri_rdfs_member), true)=true))). % 40.41/27.56 tff(c_67206, plain, (![X_1164, Y_1165]: (ifeq(iext(uri_rdfs_isDefinedBy, X_1164, Y_1165), true, iext(uri_rdfs_isDefinedBy, X_1164, Y_1165), true)=true))). % 40.41/27.56 tff(c_7609, 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))). % 40.41/27.56 tff(c_9656, 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))). % 40.41/27.56 tff(c_66869, plain, (![P_1160]: (ifeq(iext(uri_rdfs_subPropertyOf, P_1160, uri_rdf__3), true, iext(uri_rdfs_subPropertyOf, P_1160, uri_rdfs_member), true)=true))). % 40.41/27.56 tff(c_7401, 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))). % 40.41/27.56 tff(c_66259, plain, (![C_1155]: (ifeq(iext(uri_rdfs_subClassOf, C_1155, uri_rdfs_Datatype), true, iext(uri_rdfs_subClassOf, C_1155, uri_rdfs_Resource), true)=true))). % 40.41/27.56 tff(c_4456, 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))). % 40.41/27.56 tff(c_8938, 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))). % 40.41/27.56 tff(c_65821, plain, (![C_1150]: (ifeq(iext(uri_rdfs_subClassOf, C_1150, uri_rdf_XMLLiteral), true, iext(uri_rdfs_subClassOf, C_1150, uri_rdfs_Resource), true)=true))). % 40.41/27.56 tff(c_5639, 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))). % 40.41/27.56 tff(c_10597, 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))). % 40.41/27.56 tff(c_7487, 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))). % 40.41/27.56 tff(c_64881, plain, (![X_1140, Y_1141]: (ifeq(iext(uri_owl_propertyChainAxiom, X_1140, Y_1141), true, iext(uri_owl_propertyChainAxiom, X_1140, Y_1141), true)=true))). % 40.41/27.56 tff(c_12362, 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))). % 40.41/27.56 tff(c_4755, 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))). % 40.41/27.56 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_Container), true, true, true), true)=true))). % 40.41/27.56 tff(c_5438, 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))). % 40.41/27.56 tff(c_63829, plain, (![P_1129]: (ifeq(iext(uri_rdfs_subPropertyOf, P_1129, uri_rdf__2), true, iext(uri_rdfs_subPropertyOf, P_1129, uri_rdfs_member), true)=true))). % 40.41/27.56 tff(c_63666, plain, (![C_1127]: (ifeq(iext(uri_rdfs_subClassOf, C_1127, uri_rdfs_Container), true, iext(uri_rdfs_subClassOf, C_1127, uri_rdfs_Resource), true)=true))). % 40.41/27.56 tff(c_63518, plain, (![C_1125]: (ifeq(iext(uri_rdfs_subClassOf, C_1125, uri_rdf_Property), true, iext(uri_rdfs_subClassOf, C_1125, uri_rdfs_Resource), true)=true))). % 40.41/27.56 tff(c_11132, 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))). % 40.41/27.56 tff(c_62975, plain, (![X_1116, Y_1117]: (ifeq(iext(uri_ex_hasFather, X_1116, Y_1117), true, iext(uri_ex_hasFather, X_1116, Y_1117), true)=true))). % 40.41/27.56 tff(c_62962, plain, (![X_1114, Y_1115]: (ifeq(iext(uri_rdf__1, X_1114, Y_1115), true, iext(uri_rdfs_member, X_1114, Y_1115), true)=true))). % 40.41/27.56 tff(c_62480, plain, (![C_1110]: (ifeq(iext(uri_rdfs_subClassOf, C_1110, uri_rdfs_Class), true, iext(uri_rdfs_subClassOf, C_1110, uri_rdfs_Resource), true)=true))). % 40.41/27.56 tff(c_10066, 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))). % 40.41/27.56 tff(c_6666, 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))). % 40.41/27.56 tff(c_13372, 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))). % 40.41/27.56 tff(c_61709, plain, (![X_1101, Y_1102]: (ifeq(iext(uri_rdf__2, X_1101, Y_1102), true, iext(uri_rdfs_member, X_1101, Y_1102), true)=true))). % 40.41/27.56 tff(c_61665, plain, (![X_1097, Y_1098]: (ifeq(iext(uri_owl_inverseOf, X_1097, Y_1098), true, iext(uri_owl_inverseOf, X_1097, Y_1098), true)=true))). % 40.41/27.56 tff(c_13037, 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))). % 40.41/27.57 tff(c_61163, plain, (![X_1090, Y_1091]: (ifeq(iext(uri_rdf_value, X_1090, Y_1091), true, iext(uri_rdf_value, X_1090, Y_1091), true)=true))). % 40.41/27.57 tff(c_60384, plain, (![X_1086, Y_1087]: (ifeq(iext(uri_rdf_type, X_1086, Y_1087), true, iext(uri_rdf_type, X_1086, Y_1087), true)=true))). % 40.41/27.57 tff(c_4453, 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))). % 40.41/27.57 tff(c_7940, 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))). % 40.41/27.57 tff(c_60065, plain, (![X_1079, Y_1080]: (ifeq(iext(uri_rdf_subject, X_1079, Y_1080), true, iext(uri_rdf_subject, X_1079, Y_1080), true)=true))). % 40.41/27.57 tff(c_10425, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_ex_hasFather, uri_rdf_Property), true, true, true), true)=true))). % 40.41/27.57 tff(c_10876, 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))). % 40.41/27.57 tff(c_59260, plain, (![X_1071, Y_1072]: (ifeq(iext(uri_rdfs_domain, X_1071, Y_1072), true, iext(uri_rdfs_domain, X_1071, Y_1072), true)=true))). % 40.41/27.57 tff(c_13551, 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))). % 40.41/27.57 tff(c_12655, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_ex_hasCousin, uri_rdf_Property), true, true, true), true)=true))). % 40.41/27.57 tff(c_12263, 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))). % 40.41/27.57 tff(c_58693, plain, (![X_1063, Y_1064]: (ifeq(iext(uri_rdf__2, X_1063, Y_1064), true, iext(uri_rdf__2, X_1063, Y_1064), true)=true))). % 40.41/27.57 tff(c_12533, 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))). % 40.41/27.57 tff(c_9224, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_ex_hasCousin, uri_ex_hasCousin), true, true, true), true)=true))). % 40.41/27.57 tff(c_57486, plain, (![X_1052, Y_1053]: (ifeq(iext(uri_rdfs_range, X_1052, Y_1053), true, iext(uri_rdfs_range, X_1052, Y_1053), true)=true))). % 40.41/27.57 tff(c_56925, plain, (![X_1045, Y_1046]: (ifeq(iext(uri_rdf_first, X_1045, Y_1046), true, iext(uri_rdf_first, X_1045, Y_1046), true)=true))). % 40.41/27.57 tff(c_12850, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_ex_hasUncle, uri_rdf_Property), true, true, true), true)=true))). % 40.41/27.57 tff(c_56898, plain, (![X_1041, Y_1042]: (ifeq(iext(uri_rdf__1, X_1041, Y_1042), true, iext(uri_rdf__1, X_1041, Y_1042), true)=true))). % 40.41/27.57 tff(c_4601, 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))). % 40.41/27.57 tff(c_5167, 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))). % 40.41/27.57 tff(c_7143, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_owl_propertyChainAxiom, uri_rdf_Property), true, true, true), true)=true))). % 40.41/27.57 tff(c_4358, 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))). % 40.41/27.57 tff(c_55605, plain, (![X_1026, Y_1027]: (ifeq(iext(uri_ex_hasCousin, X_1026, Y_1027), true, iext(uri_ex_hasCousin, X_1026, Y_1027), true)=true))). % 40.41/27.57 tff(c_5727, 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))). % 40.41/27.57 tff(c_55301, plain, (![X_1020, Y_1021]: (ifeq(iext(uri_rdf_rest, X_1020, Y_1021), true, iext(uri_rdf_rest, X_1020, Y_1021), true)=true))). % 40.41/27.57 tff(c_5033, 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))). % 40.41/27.57 tff(c_11197, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_owl_inverseOf, uri_owl_inverseOf), true, true, true), true)=true))). % 40.41/27.57 tff(c_54892, plain, (![C_1016]: (ifeq(iext(uri_rdfs_subClassOf, C_1016, uri_rdfs_Seq), true, iext(uri_rdfs_subClassOf, C_1016, uri_rdfs_Resource), true)=true))). % 40.41/27.57 tff(c_4558, 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))). % 40.41/27.57 tff(c_10680, 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))). % 40.41/27.57 tff(c_8737, 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))). % 40.41/27.57 tff(c_5109, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_ex_hasUncle, uri_ex_hasUncle), true, true, true), true)=true))). % 40.41/27.57 tff(c_12197, 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))). % 40.41/27.57 tff(c_13462, 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))). % 40.41/27.57 tff(c_4664, 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))). % 40.41/27.57 tff(c_4898, plain, (![P_47, X_133]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, X_133, uri_rdfs_Resource), true, true, true), true)=true))). % 40.41/27.57 tff(c_14438, 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))). % 40.41/27.57 tff(c_11700, 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))). % 40.41/27.57 tff(c_14435, 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))). % 40.41/27.57 tff(c_17233, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_List), true, ifeq(iext(P_28, X_30, sK3_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l22), true, true, true), true)=true))). % 40.41/27.57 tff(c_17230, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_List), true, ifeq(iext(P_18, sK3_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l22, Y_21), true, true, true), true)=true))). % 40.41/27.57 tff(c_13607, 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))). % 40.41/27.57 tff(c_18057, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_List), true, ifeq(iext(P_18, sK2_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l21, Y_21), true, true, true), true)=true))). % 40.41/27.57 tff(c_8419, 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))). % 40.41/27.57 tff(c_6072, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_List), true, ifeq(iext(P_18, sK4_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l11, Y_21), true, true, true), true)=true))). % 40.41/27.57 tff(c_13610, 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))). % 40.41/27.57 tff(c_6815, 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))). % 40.41/27.57 tff(c_6347, 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))). % 40.41/27.57 tff(c_6818, 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))). % 40.41/27.57 tff(c_20420, 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))). % 40.41/27.57 tff(c_11697, 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))). % 40.41/27.57 tff(c_6075, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_List), true, ifeq(iext(P_28, X_30, sK4_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l11), true, true, true), true)=true))). % 40.41/27.57 tff(c_6928, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_List), true, ifeq(iext(P_28, X_30, sK5_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l12), true, true, true), true)=true))). % 40.41/27.57 tff(c_8422, 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))). % 40.41/27.57 tff(c_6925, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_List), true, ifeq(iext(P_18, sK5_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l12, Y_21), true, true, true), true)=true))). % 40.41/27.57 tff(c_20417, 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))). % 40.41/27.57 tff(c_18060, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_List), true, ifeq(iext(P_28, X_30, sK2_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l21), true, true, true), true)=true))). % 40.41/27.57 tff(c_6350, 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))). % 40.41/27.57 tff(c_4092, 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))). % 40.41/27.57 tff(c_4199, 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))). % 40.41/27.57 tff(c_4038, 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))). % 40.41/27.57 tff(c_3912, 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))). % 40.41/27.57 tff(c_3955, 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))). % 40.41/27.57 tff(c_3813, 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))). % 40.41/27.57 tff(c_3915, 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))). % 40.41/27.57 tff(c_3810, 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))). % 40.41/27.57 tff(c_4155, 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))). % 40.41/27.57 tff(c_4281, 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))). % 40.41/27.57 tff(c_4118, 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))). % 40.41/27.57 tff(c_4278, 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))). % 40.41/27.57 tff(c_3735, 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))). % 40.41/27.57 tff(c_3992, 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))). % 40.41/27.57 tff(c_4241, 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))). % 40.41/27.57 tff(c_4089, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_rdf_rest, Y_21), true, true, true), true)=true))). % 40.41/27.57 tff(c_3870, 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))). % 40.41/27.57 tff(c_3772, 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))). % 40.41/27.57 tff(c_3769, 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))). % 40.41/27.57 tff(c_3989, 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))). % 40.41/27.57 tff(c_4196, 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))). % 40.41/27.57 tff(c_4121, 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))). % 40.41/27.57 tff(c_4035, 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))). % 40.41/27.57 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_type), true, true, true), true)=true))). % 40.41/27.58 tff(c_4238, 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))). % 40.41/27.58 tff(c_4317, 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))). % 40.41/27.58 tff(c_4320, 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))). % 40.41/27.58 tff(c_3867, 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))). % 40.41/27.58 tff(c_3732, 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))). % 40.41/27.58 tff(c_3952, 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))). % 40.41/27.58 tff(c_2208, plain, (![P_95, X_60, Y_98]: (ifeq(iext(uri_rdfs_domain, P_95, uri_rdfs_Resource), true, ifeq(iext(P_95, X_60, Y_98), true, true, true), true)=true))). % 40.41/27.58 tff(c_1832, plain, (![P_91, X_93, X_60]: (ifeq(iext(uri_rdfs_range, P_91, uri_rdfs_Resource), true, ifeq(iext(P_91, X_93, X_60), true, true, true), true)=true))). % 40.41/27.58 tff(c_2956, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_subClassOf), true, ifeq(iext(P_99, uri_rdf_XMLLiteral, uri_rdfs_Literal), true, true, true), true)=true))). % 40.41/27.58 tff(c_2992, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_range), true, ifeq(iext(P_99, uri_rdfs_domain, uri_rdfs_Class), true, true, true), true)=true))). % 40.41/27.58 tff(c_2857, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdf_type), true, ifeq(iext(P_99, uri_rdf_first, uri_rdf_Property), true, true, true), true)=true))). % 40.41/27.58 tff(c_2986, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_domain), true, ifeq(iext(P_99, uri_rdf_type, uri_rdfs_Resource), true, true, true), true)=true))). % 40.41/27.58 tff(c_3016, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdf_type), true, ifeq(iext(P_99, uri_rdf__3, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 40.41/27.58 tff(c_2881, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdf_rest), true, ifeq(iext(P_99, sK2_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l21, sK3_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l22), true, true, true), true)=true))). % 40.41/27.58 tff(c_2773, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_domain), true, ifeq(iext(P_99, uri_rdfs_subPropertyOf, uri_rdf_Property), true, true, true), true)=true))). % 40.41/27.58 tff(c_2779, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_range), true, ifeq(iext(P_99, uri_rdf_first, uri_rdfs_Resource), true, true, true), true)=true))). % 40.41/27.58 tff(c_3022, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_range), true, ifeq(iext(P_99, uri_rdfs_range, uri_rdfs_Class), true, true, true), true)=true))). % 40.41/27.58 tff(c_3064, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdf_first), true, ifeq(iext(P_99, sK5_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l12, uri_ex_hasFather), true, true, true), true)=true))). % 40.41/27.58 tff(c_2920, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_domain), true, ifeq(iext(P_99, uri_rdf_value, uri_rdfs_Resource), true, true, true), true)=true))). % 40.41/27.58 tff(c_2647, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_owl_propertyChainAxiom), true, ifeq(iext(P_99, uri_ex_hasUncle, sK4_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l11), true, true, true), true)=true))). % 40.41/27.58 tff(c_2914, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_subPropertyOf), true, ifeq(iext(P_99, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso), true, true, true), true)=true))). % 40.41/27.58 tff(c_42130, plain, (![C_878]: (ifeq(iext(uri_rdfs_subClassOf, C_878, uri_rdfs_Datatype), true, iext(uri_rdfs_subClassOf, C_878, uri_rdfs_Class), true)=true))). % 40.41/27.58 tff(c_2671, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_ex_hasFather), true, ifeq(iext(P_99, uri_ex_alice, uri_ex_dave), true, true, true), true)=true))). % 40.41/27.58 tff(c_2737, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdf_type), true, ifeq(iext(P_99, uri_rdf__1, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 40.41/27.58 tff(c_2641, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_domain), true, ifeq(iext(P_99, uri_rdfs_subClassOf, uri_rdfs_Class), true, true, true), true)=true))). % 40.41/27.58 tff(c_41670, plain, (![P_873]: (ifeq(iext(uri_rdfs_subPropertyOf, P_873, uri_rdfs_isDefinedBy), true, iext(uri_rdfs_subPropertyOf, P_873, uri_rdfs_seeAlso), true)=true))). % 40.41/27.58 tff(c_2932, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_range), true, ifeq(iext(P_99, uri_rdf_rest, uri_rdf_List), true, true, true), true)=true))). % 40.41/27.58 tff(c_2725, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_range), true, ifeq(iext(P_99, uri_rdf_type, uri_rdfs_Class), true, true, true), true)=true))). % 40.41/27.58 tff(c_3058, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdf_rest), true, ifeq(iext(P_99, sK5_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l12, uri_rdf_nil), true, true, true), true)=true))). % 40.41/27.58 tff(c_2980, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdf_type), true, ifeq(iext(P_99, uri_rdf_value, uri_rdf_Property), true, true, true), true)=true))). % 40.41/27.58 tff(c_2755, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_range), true, ifeq(iext(P_99, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true, true, true), true)=true))). % 40.41/27.58 tff(c_2887, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_range), true, ifeq(iext(P_99, uri_rdf__1, uri_rdfs_Resource), true, true, true), true)=true))). % 40.41/27.58 tff(c_2785, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_range), true, ifeq(iext(P_99, uri_rdfs_seeAlso, uri_rdfs_Resource), true, true, true), true)=true))). % 40.41/27.58 tff(c_2653, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_range), true, ifeq(iext(P_99, uri_rdfs_comment, uri_rdfs_Literal), true, true, true), true)=true))). % 40.41/27.58 tff(c_2713, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdf_rest), true, ifeq(iext(P_99, sK4_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l11, sK5_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l12), true, true, true), true)=true))). % 40.41/27.58 tff(c_2689, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdf_rest), true, ifeq(iext(P_99, sK3_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l22, uri_rdf_nil), true, true, true), true)=true))). % 40.41/27.58 tff(c_40238, plain, (![C_861]: (ifeq(iext(uri_rdfs_subClassOf, C_861, uri_rdfs_ContainerMembershipProperty), true, iext(uri_rdfs_subClassOf, C_861, uri_rdf_Property), true)=true))). % 40.41/27.58 tff(c_2731, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_domain), true, ifeq(iext(P_99, uri_rdfs_domain, uri_rdf_Property), true, true, true), true)=true))). % 40.41/27.58 tff(c_2827, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_domain), true, ifeq(iext(P_99, uri_rdfs_seeAlso, uri_rdfs_Resource), true, true, true), true)=true))). % 40.41/27.58 tff(c_2761, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdf_type), true, ifeq(iext(P_99, uri_rdf_type, uri_rdf_Property), true, true, true), true)=true))). % 40.41/27.58 tff(c_2809, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdf_type), true, ifeq(iext(P_99, uri_rdf_XMLLiteral, uri_rdfs_Datatype), true, true, true), true)=true))). % 40.41/27.58 tff(c_3010, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_range), true, ifeq(iext(P_99, uri_rdf__2, uri_rdfs_Resource), true, true, true), true)=true))). % 40.41/27.58 tff(c_2926, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_domain), true, ifeq(iext(P_99, uri_rdf_rest, uri_rdf_List), true, true, true), true)=true))). % 40.41/27.58 tff(c_39351, plain, (![C_853]: (ifeq(iext(uri_rdfs_subClassOf, C_853, uri_rdf_XMLLiteral), true, iext(uri_rdfs_subClassOf, C_853, uri_rdfs_Literal), true)=true))). % 40.41/27.58 tff(c_2749, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_domain), true, ifeq(iext(P_99, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true, true, true), true)=true))). % 40.41/27.58 tff(c_2623, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_ex_hasUncle), true, ifeq(iext(P_99, uri_ex_bob, uri_ex_dave), true, true, true), true)=true))). % 40.41/27.58 tff(c_2719, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdf_type), true, ifeq(iext(P_99, uri_rdf__1, uri_rdf_Property), true, true, true), true)=true))). % 40.41/27.58 tff(c_2659, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdf_type), true, ifeq(iext(P_99, uri_rdf_rest, uri_rdf_Property), true, true, true), true)=true))). % 40.41/27.58 tff(c_2938, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_domain), true, ifeq(iext(P_99, uri_rdfs_comment, uri_rdfs_Resource), true, true, true), true)=true))). % 40.41/27.58 tff(c_2797, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_domain), true, ifeq(iext(P_99, uri_rdfs_label, uri_rdfs_Resource), true, true, true), true)=true))). % 40.41/27.58 tff(c_2962, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdf_type), true, ifeq(iext(P_99, uri_rdf__2, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 40.41/27.58 tff(c_2683, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_subClassOf), true, ifeq(iext(P_99, uri_rdf_Bag, uri_rdfs_Container), true, true, true), true)=true))). % 40.41/27.58 tff(c_2701, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdf_type), true, ifeq(iext(P_99, uri_rdf_object, uri_rdf_Property), true, true, true), true)=true))). % 40.41/27.58 tff(c_2869, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_domain), true, ifeq(iext(P_99, uri_rdf_object, uri_rdfs_Statement), true, true, true), true)=true))). % 40.41/27.58 tff(c_2767, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_subClassOf), true, ifeq(iext(P_99, uri_rdfs_Seq, uri_rdfs_Container), true, true, true), true)=true))). % 40.41/27.58 tff(c_2677, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdf_type), true, ifeq(iext(P_99, uri_rdf_subject, uri_rdf_Property), true, true, true), true)=true))). % 40.41/27.58 tff(c_2629, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_domain), true, ifeq(iext(P_99, uri_rdf_predicate, uri_rdfs_Statement), true, true, true), true)=true))). % 40.41/27.58 tff(c_2950, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_range), true, ifeq(iext(P_99, uri_rdf__3, uri_rdfs_Resource), true, true, true), true)=true))). % 40.41/27.58 tff(c_2791, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_subClassOf), true, ifeq(iext(P_99, uri_rdf_Alt, uri_rdfs_Container), true, true, true), true)=true))). % 40.41/27.58 tff(c_2665, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdf_type), true, ifeq(iext(P_99, uri_rdf__3, uri_rdf_Property), true, true, true), true)=true))). % 40.41/27.58 tff(c_2851, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_domain), true, ifeq(iext(P_99, uri_rdfs_range, uri_rdf_Property), true, true, true), true)=true))). % 40.41/27.58 tff(c_2974, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_range), true, ifeq(iext(P_99, uri_rdfs_subClassOf, uri_rdfs_Class), true, true, true), true)=true))). % 40.41/27.58 tff(c_36816, plain, (![D_833]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_833), true, icext(D_833, uri_rdfs_Resource), true)=true))). % 40.41/27.58 tff(c_2833, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_domain), true, ifeq(iext(P_99, uri_rdf__1, uri_rdfs_Resource), true, true, true), true)=true))). % 40.41/27.58 tff(c_36606, plain, (![D_830]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_830), true, icext(D_830, uri_rdfs_subClassOf), true)=true))). % 40.41/27.58 tff(c_36540, plain, (![D_828]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_828), true, icext(D_828, uri_rdfs_seeAlso), true)=true))). % 40.41/27.58 tff(c_36473, plain, (![D_826]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_826), true, icext(D_826, uri_ex_hasCousin), true)=true))). % 40.41/27.58 tff(c_3052, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_owl_inverseOf), true, ifeq(iext(P_99, sK1_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l3, uri_ex_hasFather), true, true, true), true)=true))). % 40.41/27.58 tff(c_36272, plain, (![D_823]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_823), true, icext(D_823, uri_rdfs_domain), true)=true))). % 40.41/27.58 tff(c_36205, plain, (![D_821]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_821), true, icext(D_821, uri_rdfs_subPropertyOf), true)=true))). % 40.41/27.58 tff(c_36138, plain, (![C_819]: (ifeq(iext(uri_rdfs_subClassOf, C_819, uri_rdfs_Seq), true, iext(uri_rdfs_subClassOf, C_819, uri_rdfs_Container), true)=true))). % 40.41/27.58 tff(c_36072, plain, (![D_817]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_817), true, icext(D_817, uri_owl_inverseOf), true)=true))). % 40.41/27.58 tff(c_36006, plain, (![D_815]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_815), true, icext(D_815, uri_ex_hasUncle), true)=true))). % 40.41/27.58 tff(c_35800, plain, (![D_812]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_812), true, icext(D_812, uri_owl_propertyChainAxiom), true)=true))). % 40.41/27.58 tff(c_2968, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_subClassOf), true, ifeq(iext(P_99, uri_rdfs_Datatype, uri_rdfs_Class), true, true, true), true)=true))). % 40.41/27.58 tff(c_35734, plain, (![D_810]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_810), true, icext(D_810, uri_ex_hasFather), true)=true))). % 40.41/27.58 tff(c_35668, plain, (![D_808]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_808), true, icext(D_808, uri_rdfs_range), true)=true))). % 40.41/27.58 tff(c_2707, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdf_first), true, ifeq(iext(P_99, sK4_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l11, uri_ex_hasCousin), true, true, true), true)=true))). % 40.41/27.58 tff(c_35466, plain, (![D_805]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_805), true, icext(D_805, uri_rdf_Alt), true)=true))). % 40.41/27.58 tff(c_35400, plain, (![D_803]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_803), true, icext(D_803, uri_rdfs_ContainerMembershipProperty), true)=true))). % 40.41/27.58 tff(c_35326, plain, (![D_801]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_801), true, icext(D_801, uri_rdf_XMLLiteral), true)=true))). % 40.41/27.58 tff(c_35258, plain, (![D_799]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_799), true, icext(D_799, uri_rdf_Bag), true)=true))). % 40.41/27.58 tff(c_35192, plain, (![D_797]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_797), true, icext(D_797, uri_rdfs_Container), true)=true))). % 40.41/27.58 tff(c_3046, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_domain), true, ifeq(iext(P_99, uri_rdf__3, uri_rdfs_Resource), true, true, true), true)=true))). % 40.41/27.58 tff(c_34950, plain, (![D_794]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_794), true, icext(D_794, uri_rdfs_Class), true)=true))). % 40.41/27.58 tff(c_34884, plain, (![D_792]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_792), true, icext(D_792, uri_rdfs_Datatype), true)=true))). % 40.41/27.58 tff(c_34857, plain, (![X_788, Y_789]: (ifeq(iext(uri_rdfs_isDefinedBy, X_788, Y_789), true, iext(uri_rdfs_seeAlso, X_788, Y_789), true)=true))). % 40.41/27.58 tff(c_34788, plain, (![D_786]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_786), true, icext(D_786, uri_rdfs_Seq), true)=true))). % 40.41/27.58 tff(c_34722, plain, (![D_784]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_784), true, icext(D_784, uri_rdfs_Literal), true)=true))). % 40.41/27.58 tff(c_2944, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_domain), true, ifeq(iext(P_99, uri_rdf_first, uri_rdf_List), true, true, true), true)=true))). % 40.41/27.58 tff(c_34521, plain, (![D_781]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_781), true, icext(D_781, sK3_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l22), true)=true))). % 40.41/27.58 tff(c_34455, plain, (![D_779]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_779), true, icext(D_779, uri_rdfs_comment), true)=true))). % 40.41/27.58 tff(c_34389, plain, (![D_777]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_777), true, icext(D_777, uri_rdfs_Statement), true)=true))). % 40.41/27.58 tff(c_3028, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_range), true, ifeq(iext(P_99, uri_rdfs_label, uri_rdfs_Literal), true, true, true), true)=true))). % 40.41/27.58 tff(c_34187, plain, (![D_774]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_774), true, icext(D_774, uri_rdf_List), true)=true))). % 40.41/27.58 tff(c_34121, plain, (![D_772]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_772), true, icext(D_772, uri_rdfs_label), true)=true))). % 40.41/27.58 tff(c_33920, plain, (![D_769]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_769), true, icext(D_769, uri_rdfs_isDefinedBy), true)=true))). % 40.41/27.58 tff(c_2695, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_subClassOf), true, ifeq(iext(P_99, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property), true, true, true), true)=true))). % 40.41/27.58 tff(c_33852, plain, (![D_767]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_767), true, icext(D_767, sK2_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l21), true)=true))). % 40.41/27.58 tff(c_15918, 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))). % 40.41/27.58 tff(c_2875, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdf_first), true, ifeq(iext(P_99, sK3_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l22, sK1_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l3), true, true, true), true)=true))). % 40.41/27.58 tff(c_20751, 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))). % 40.41/27.58 tff(c_15870, 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))). % 40.41/27.58 tff(c_33537, plain, (![D_758]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_758), true, icext(D_758, sK5_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l12), true)=true))). % 40.41/27.59 tff(c_15805, 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))). % 40.41/27.59 tff(c_2743, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdf_type), true, ifeq(iext(P_99, uri_rdf__2, uri_rdf_Property), true, true, true), true)=true))). % 40.41/27.59 tff(c_15665, 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))). % 40.41/27.59 tff(c_15734, 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))). % 40.41/27.59 tff(c_15381, 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))). % 40.41/27.59 tff(c_33225, plain, (![D_749]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_749), true, icext(D_749, uri_rdf_predicate), true)=true))). % 40.41/27.59 tff(c_15314, 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))). % 40.41/27.59 tff(c_15470, 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))). % 40.41/27.59 tff(c_15472, 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))). % 40.41/27.59 tff(c_2893, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_owl_propertyChainAxiom), true, ifeq(iext(P_99, uri_ex_hasCousin, sK2_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l21), true, true, true), true)=true))). % 40.41/27.59 tff(c_15127, 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))). % 40.41/27.59 tff(c_15125, 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))). % 40.41/27.59 tff(c_32900, plain, (![D_740]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_740), true, icext(D_740, uri_rdfs_member), true)=true))). % 40.41/27.59 tff(c_32802, plain, (![C_737]: (ifeq(iext(uri_rdfs_subClassOf, C_737, uri_rdf_Alt), true, iext(uri_rdfs_subClassOf, C_737, uri_rdfs_Container), true)=true))). % 40.41/27.59 tff(c_14384, 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))). % 40.41/27.59 tff(c_14949, 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))). % 40.41/27.59 tff(c_14996, 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))). % 40.41/27.59 tff(c_32687, plain, (![D_732]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_732), true, icext(D_732, sK4_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l11), true)=true))). % 40.41/27.59 tff(c_14833, 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))). % 40.41/27.59 tff(c_14332, 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))). % 40.41/27.59 tff(c_14717, 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))). % 40.41/27.59 tff(c_3004, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_range), true, ifeq(iext(P_99, uri_rdfs_member, uri_rdfs_Resource), true, true, true), true)=true))). % 40.41/27.59 tff(c_14784, 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))). % 40.41/27.59 tff(c_15061, 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))). % 40.41/27.59 tff(c_14902, 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))). % 40.41/27.59 tff(c_13884, 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))). % 40.41/27.59 tff(c_13962, 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))). % 40.41/27.59 tff(c_14259, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, sK4_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l11, uri_rdf_List), true)=true))). % 40.41/27.59 tff(c_14017, 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))). % 40.41/27.59 tff(c_14118, 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))). % 40.41/27.59 tff(c_2815, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_ex_hasCousin), true, ifeq(iext(P_99, uri_ex_alice, uri_ex_bob), true, true, true), true)=true))). % 40.41/27.59 tff(c_14212, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, sK5_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l12, uri_rdf_List), true)=true))). % 40.41/27.59 tff(c_14669, 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))). % 40.41/27.59 tff(c_18249, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, sK2_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l21, uri_rdf_List), true)=true))). % 40.41/27.59 tff(c_17405, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, sK3_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l22, uri_rdf_List), true)=true))). % 40.41/27.59 tff(c_20494, 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))). % 40.41/27.59 tff(c_9678, 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))). % 40.41/27.59 tff(c_13486, 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))). % 40.41/27.59 tff(c_12389, 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))). % 40.41/27.59 tff(c_5968, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_owl_inverseOf, uri_rdf_Property), true)=true))). % 40.41/27.59 tff(c_5360, 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))). % 40.41/27.59 tff(c_31972, plain, (![D_706]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_706), true, icext(D_706, uri_rdf__3), true)=true))). % 40.41/27.59 tff(c_12387, 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))). % 40.41/27.59 tff(c_12290, 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))). % 40.41/27.59 tff(c_2821, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_domain), true, ifeq(iext(P_99, uri_rdf_subject, uri_rdfs_Statement), true, true, true), true)=true))). % 40.41/27.59 tff(c_12557, 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))). % 40.41/27.59 tff(c_11470, 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))). % 40.41/27.59 tff(c_12680, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_ex_hasCousin, uri_rdf_Property), true)=true))). % 40.41/27.59 tff(c_31644, plain, (![D_697]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_697), true, icext(D_697, uri_rdf__3), true)=true))). % 40.41/27.59 tff(c_12076, 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))). % 40.41/27.59 tff(c_9249, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_ex_hasCousin, uri_ex_hasCousin), true)=true))). % 40.41/27.59 tff(c_6252, 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))). % 40.41/27.59 tff(c_2635, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_domain), true, ifeq(iext(P_99, uri_rdfs_member, uri_rdfs_Resource), true, true, true), true)=true))). % 40.41/27.59 tff(c_10353, 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))). % 40.41/27.59 tff(c_31295, plain, (![D_688]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_688), true, icext(D_688, uri_rdf__2), true)=true))). % 40.41/27.59 tff(c_12625, 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))). % 40.41/27.59 tff(c_8366, 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))). % 40.41/27.59 tff(c_2863, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_range), true, ifeq(iext(P_99, uri_rdfs_subPropertyOf, uri_rdf_Property), true, true, true), true)=true))). % 40.58/27.59 tff(c_10705, 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))). % 40.58/27.59 tff(c_13064, 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))). % 40.58/27.59 tff(c_12875, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_ex_hasUncle, uri_rdf_Property), true)=true))). % 40.58/27.59 tff(c_6691, 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))). % 40.58/27.59 tff(c_8367, 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))). % 40.58/27.59 tff(c_11024, 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))). % 40.58/27.59 tff(c_2899, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdf_type), true, ifeq(iext(P_99, uri_rdf_Property, uri_rdfs_Class), true, true, true), true)=true))). % 40.58/27.59 tff(c_7634, 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))). % 40.58/27.59 tff(c_6251, 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))). % 40.58/27.59 tff(c_13208, 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))). % 40.58/27.59 tff(c_13210, 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))). % 40.58/27.59 tff(c_11220, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_owl_inverseOf, uri_owl_inverseOf), true)=true))). % 40.58/27.59 tff(c_9680, 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))). % 40.58/27.59 tff(c_3040, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_domain), true, ifeq(iext(P_99, uri_rdf__2, uri_rdfs_Resource), true, true, true), true)=true))). % 40.58/27.59 tff(c_7426, 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))). % 40.58/27.59 tff(c_13062, 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))). % 40.58/27.59 tff(c_30332, plain, (![D_661]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, D_661), true, icext(D_661, uri_rdf_XMLLiteral), true)=true))). % 40.58/27.59 tff(c_5466, 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))). % 40.58/27.59 tff(c_2803, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_range), true, ifeq(iext(P_99, uri_rdf_subject, uri_rdfs_Resource), true, true, true), true)=true))). % 40.58/27.59 tff(c_10175, 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))). % 40.58/27.59 tff(c_6575, 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))). % 40.58/27.59 tff(c_5752, 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))). % 40.58/27.59 tff(c_8306, 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))). % 40.58/27.59 tff(c_5751, 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))). % 40.58/27.59 tff(c_2998, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_range), true, ifeq(iext(P_99, uri_rdf_value, uri_rdfs_Resource), true, true, true), true)=true))). % 40.58/27.59 tff(c_10625, 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))). % 40.58/27.59 tff(c_7512, 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))). % 40.58/27.59 tff(c_29658, plain, (![D_643]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_643), true, icext(D_643, uri_rdf_rest), true)=true))). % 40.58/27.59 tff(c_12224, 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))). % 40.58/27.59 tff(c_2905, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdfs_range), true, ifeq(iext(P_99, uri_rdf_predicate, uri_rdfs_Resource), true, true, true), true)=true))). % 40.58/27.59 tff(c_6453, 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))). % 40.58/27.59 tff(c_11022, 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))). % 40.58/27.59 tff(c_10898, 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))). % 40.58/27.59 tff(c_8626, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_ex_hasFather, uri_ex_hasFather), true)=true))). % 40.58/27.59 tff(c_7965, 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))). % 40.58/27.59 tff(c_29263, plain, (![C_631]: (ifeq(iext(uri_rdfs_subClassOf, C_631, uri_rdf_Bag), true, iext(uri_rdfs_subClassOf, C_631, uri_rdfs_Container), true)=true))). % 40.58/27.59 tff(c_7168, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_owl_propertyChainAxiom, uri_rdf_Property), true)=true))). % 40.58/27.59 tff(c_7967, 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))). % 40.58/27.59 tff(c_11535, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_owl_propertyChainAxiom, uri_owl_propertyChainAxiom), true)=true))). % 40.58/27.59 tff(c_10450, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_ex_hasFather, uri_rdf_Property), true)=true))). % 40.58/27.59 tff(c_13396, 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))). % 40.58/27.59 tff(c_5055, 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))). % 40.58/27.59 tff(c_7008, 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))). % 40.58/27.59 tff(c_5192, 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))). % 40.58/27.59 tff(c_3034, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_ex_hasFather), true, ifeq(iext(P_99, uri_ex_bob, uri_ex_charly), true, true, true), true)=true))). % 40.58/27.59 tff(c_5664, 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))). % 40.58/27.59 tff(c_10355, 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))). % 40.58/27.59 tff(c_10959, 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))). % 40.58/27.59 tff(c_5131, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_ex_hasUncle, uri_ex_hasUncle), true)=true))). % 40.58/27.59 tff(c_13816, 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))). % 40.58/27.59 tff(c_2839, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdf_first), true, ifeq(iext(P_99, sK2_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l21, uri_ex_hasUncle), true, true, true), true)=true))). % 40.58/27.59 tff(c_8962, 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))). % 40.58/27.59 tff(c_8760, 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))). % 40.58/27.59 tff(c_8963, 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))). % 40.58/27.59 tff(c_7802, 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))). % 40.58/27.59 tff(c_11644, 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))). % 40.58/27.59 tff(c_11469, 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))). % 40.58/27.59 tff(c_11156, 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))). % 40.58/27.59 tff(c_10089, 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))). % 40.58/27.59 tff(c_2845, plain, (![P_99]: (ifeq(iext(uri_rdfs_subPropertyOf, P_99, uri_rdf_type), true, ifeq(iext(P_99, uri_rdf_nil, uri_rdf_List), true, true, true), true)=true))). % 40.58/27.60 tff(c_13575, 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))). % 40.58/27.60 tff(c_10897, 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))). % 40.58/27.60 tff(c_4917, plain, (![Q_48, X_133]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, X_133, uri_rdfs_Resource), true)=true))). % 40.58/27.60 tff(c_27935, plain, (![D_590]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_590), true, icext(D_590, uri_rdf_Property), true)=true))). % 40.58/27.60 tff(c_3067, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_ex_hasUncle, Q_100), true, iext(Q_100, uri_ex_bob, uri_ex_dave), true)=true))). % 40.58/27.60 tff(c_3112, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_owl_propertyChainAxiom, Q_100), true, iext(Q_100, uri_ex_hasCousin, sK2_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l21), true)=true))). % 40.58/27.60 tff(c_3123, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_100), true, iext(Q_100, uri_rdf__2, uri_rdfs_ContainerMembershipProperty), true)=true))). % 40.58/27.60 tff(c_3133, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_100), true, iext(Q_100, uri_rdfs_range, uri_rdfs_Class), true)=true))). % 40.58/27.60 tff(c_3113, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_100), true, iext(Q_100, uri_rdf_Property, uri_rdfs_Class), true)=true))). % 40.58/27.60 tff(c_3091, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_100), true, iext(Q_100, uri_rdfs_Seq, uri_rdfs_Container), true)=true))). % 40.58/27.60 tff(c_3104, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_100), true, iext(Q_100, uri_rdf_nil, uri_rdf_List), true)=true))). % 40.58/27.60 tff(c_3130, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_100), true, iext(Q_100, uri_rdfs_member, uri_rdfs_Resource), true)=true))). % 40.58/27.60 tff(c_3115, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_100), true, iext(Q_100, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso), true)=true))). % 40.58/27.60 tff(c_3090, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_100), true, iext(Q_100, uri_rdf_type, uri_rdf_Property), true)=true))). % 40.58/27.60 tff(c_3128, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_100), true, iext(Q_100, uri_rdfs_domain, uri_rdfs_Class), true)=true))). % 40.58/27.60 tff(c_3072, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_100), true, iext(Q_100, uri_rdfs_comment, uri_rdfs_Literal), true)=true))). % 40.58/27.60 tff(c_3080, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_100), true, iext(Q_100, uri_rdf_object, uri_rdf_Property), true)=true))). % 40.58/27.60 tff(c_3086, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_100), true, iext(Q_100, uri_rdf__1, uri_rdfs_ContainerMembershipProperty), true)=true))). % 40.58/27.60 tff(c_3081, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_first, Q_100), true, iext(Q_100, sK4_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l11, uri_ex_hasCousin), true)=true))). % 40.58/27.60 tff(c_3096, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_100), true, iext(Q_100, uri_rdfs_label, uri_rdfs_Resource), true)=true))). % 40.58/27.60 tff(c_27594, plain, (![D_572]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_572), true, icext(D_572, uri_rdf_subject), true)=true))). % 40.58/27.60 tff(c_3107, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_100), true, iext(Q_100, uri_rdfs_subPropertyOf, uri_rdf_Property), true)=true))). % 40.58/27.60 tff(c_3097, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_100), true, iext(Q_100, uri_rdf_subject, uri_rdfs_Resource), true)=true))). % 40.58/27.60 tff(c_3082, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_rest, Q_100), true, iext(Q_100, sK4_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l11, sK5_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l12), true)=true))). % 40.58/27.60 tff(c_3120, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_100), true, iext(Q_100, uri_rdf_first, uri_rdf_List), true)=true))). % 40.58/27.60 tff(c_3088, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_100), true, iext(Q_100, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true)=true))). % 40.58/27.60 tff(c_3216, plain, (![E_104]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_104), true, iext(uri_rdfs_subClassOf, uri_rdfs_Seq, E_104), true)=true))). % 40.58/27.60 tff(c_3083, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_100), true, iext(Q_100, uri_rdf__1, uri_rdf_Property), true)=true))). % 40.58/27.60 tff(c_3101, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_100), true, iext(Q_100, uri_rdfs_seeAlso, uri_rdfs_Resource), true)=true))). % 40.58/27.60 tff(c_3106, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_100), true, iext(Q_100, uri_rdf_first, uri_rdf_Property), true)=true))). % 40.58/27.60 tff(c_3075, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_ex_hasFather, Q_100), true, iext(Q_100, uri_ex_alice, uri_ex_dave), true)=true))). % 40.58/27.60 tff(c_3219, plain, (![E_104]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, E_104), true, iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, E_104), true)=true))). % 40.58/27.60 tff(c_3134, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_100), true, iext(Q_100, uri_rdfs_label, uri_rdfs_Literal), true)=true))). % 40.58/27.60 tff(c_3098, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_100), true, iext(Q_100, uri_rdf_XMLLiteral, uri_rdfs_Datatype), true)=true))). % 40.58/27.60 tff(c_3089, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_100), true, iext(Q_100, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true)=true))). % 40.58/27.60 tff(c_3109, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_first, Q_100), true, iext(Q_100, sK3_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l22, sK1_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l3), true)=true))). % 40.58/27.60 tff(c_3103, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_first, Q_100), true, iext(Q_100, sK2_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l21, uri_ex_hasUncle), true)=true))). % 40.58/27.60 tff(c_3214, plain, (![E_104]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_104), true, iext(uri_rdfs_subClassOf, uri_rdf_Bag, E_104), true)=true))). % 40.58/27.60 tff(c_3076, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_100), true, iext(Q_100, uri_rdf_subject, uri_rdf_Property), true)=true))). % 40.58/27.60 tff(c_3215, plain, (![E_104]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, E_104), true, iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, E_104), true)=true))). % 40.58/27.60 tff(c_3069, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_100), true, iext(Q_100, uri_rdfs_member, uri_rdfs_Resource), true)=true))). % 40.58/27.60 tff(c_3118, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_100), true, iext(Q_100, uri_rdf_rest, uri_rdf_List), true)=true))). % 40.58/27.60 tff(c_3100, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_100), true, iext(Q_100, uri_rdf_subject, uri_rdfs_Statement), true)=true))). % 40.58/27.60 tff(c_3087, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_100), true, iext(Q_100, uri_rdf__2, uri_rdf_Property), true)=true))). % 40.58/27.60 tff(c_3068, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_100), true, iext(Q_100, uri_rdf_predicate, uri_rdfs_Statement), true)=true))). % 40.58/27.60 tff(c_3102, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_100), true, iext(Q_100, uri_rdf__1, uri_rdfs_Resource), true)=true))). % 40.58/27.60 tff(c_27041, plain, (![D_545]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_545), true, icext(D_545, uri_rdf_nil), true)=true))). % 40.58/27.60 tff(c_3074, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_100), true, iext(Q_100, uri_rdf__3, uri_rdf_Property), true)=true))). % 40.58/27.60 tff(c_3121, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_100), true, iext(Q_100, uri_rdf__3, uri_rdfs_Resource), true)=true))). % 40.58/27.60 tff(c_3127, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_100), true, iext(Q_100, uri_rdf_type, uri_rdfs_Resource), true)=true))). % 40.58/27.60 tff(c_3093, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_100), true, iext(Q_100, uri_rdf_first, uri_rdfs_Resource), true)=true))). % 40.58/27.60 tff(c_3070, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_100), true, iext(Q_100, uri_rdfs_subClassOf, uri_rdfs_Class), true)=true))). % 40.58/27.60 tff(c_3092, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_100), true, iext(Q_100, uri_rdfs_subPropertyOf, uri_rdf_Property), true)=true))). % 40.58/27.60 tff(c_3073, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_100), true, iext(Q_100, uri_rdf_rest, uri_rdf_Property), true)=true))). % 40.58/27.60 tff(c_26831, plain, (![D_536]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_536), true, icext(D_536, uri_rdf__1), true)=true))). % 40.58/27.60 tff(c_3125, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_100), true, iext(Q_100, uri_rdfs_subClassOf, uri_rdfs_Class), true)=true))). % 40.58/27.60 tff(c_3272, plain, (![R_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_seeAlso, R_107), true, iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, R_107), true)=true))). % 40.58/27.60 tff(c_3085, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_100), true, iext(Q_100, uri_rdfs_domain, uri_rdf_Property), true)=true))). % 40.58/27.60 tff(c_3129, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_100), true, iext(Q_100, uri_rdf_value, uri_rdfs_Resource), true)=true))). % 40.58/27.60 tff(c_3132, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_100), true, iext(Q_100, uri_rdf__3, uri_rdfs_ContainerMembershipProperty), true)=true))). % 40.58/27.60 tff(c_3131, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_100), true, iext(Q_100, uri_rdf__2, uri_rdfs_Resource), true)=true))). % 40.58/27.60 tff(c_3099, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_ex_hasCousin, Q_100), true, iext(Q_100, uri_ex_alice, uri_ex_bob), true)=true))). % 40.58/27.60 tff(c_26620, plain, (![D_527]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_527), true, icext(D_527, uri_rdf_type), true)=true))). % 40.58/27.60 tff(c_3140, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_first, Q_100), true, iext(Q_100, sK5_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l12, uri_ex_hasFather), true)=true))). % 40.58/27.60 tff(c_3117, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_100), true, iext(Q_100, uri_rdf_rest, uri_rdf_List), true)=true))). % 40.58/27.60 tff(c_3218, plain, (![E_104]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Literal, E_104), true, iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, E_104), true)=true))). % 40.58/27.60 tff(c_3108, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_100), true, iext(Q_100, uri_rdf_object, uri_rdfs_Statement), true)=true))). % 40.58/27.60 tff(c_15871, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_predicate), true)=true))). % 40.58/27.60 tff(c_15872, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_predicate), true)=true))). % 40.58/27.60 tff(c_26427, plain, (![D_519]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_519), true, icext(D_519, uri_rdf_value), true)=true))). % 40.58/27.60 tff(c_20752, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_label), true)=true))). % 40.58/27.60 tff(c_20753, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_label), true)=true))). % 40.58/27.60 tff(c_15807, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_comment), true)=true))). % 40.58/27.60 tff(c_3105, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_100), true, iext(Q_100, uri_rdfs_range, uri_rdf_Property), true)=true))). % 40.58/27.60 tff(c_15806, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_comment), true)=true))). % 40.58/27.60 tff(c_15666, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_member), true)=true))). % 40.58/27.60 tff(c_26216, plain, (![D_511]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_511), true, icext(D_511, uri_rdf_object), true)=true))). % 40.58/27.60 tff(c_15735, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Resource), true)=true))). % 40.58/27.60 tff(c_3071, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_owl_propertyChainAxiom, Q_100), true, iext(Q_100, uri_ex_hasUncle, sK4_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l11), true)=true))). % 40.58/27.60 tff(c_15316, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_List), true)=true))). % 40.58/27.60 tff(c_15128, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdf_List), true)=true))). % 40.58/27.60 tff(c_26041, plain, (![D_505]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_505), true, icext(D_505, uri_rdf__2), true)=true))). % 40.58/27.60 tff(c_15383, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Statement), true)=true))). % 40.58/27.60 tff(c_15473, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Statement), true)=true))). % 40.58/27.60 tff(c_3094, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_100), true, iext(Q_100, uri_rdfs_seeAlso, uri_rdfs_Resource), true)=true))). % 40.58/27.60 tff(c_3136, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_100), true, iext(Q_100, uri_rdf__2, uri_rdfs_Resource), true)=true))). % 40.58/27.60 tff(c_3078, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_rest, Q_100), true, iext(Q_100, sK3_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l22, uri_rdf_nil), true)=true))). % 40.58/27.60 tff(c_25824, plain, (![D_498]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_498), true, icext(D_498, uri_rdf__1), true)=true))). % 40.58/27.60 tff(c_3116, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_100), true, iext(Q_100, uri_rdf_value, uri_rdfs_Resource), true)=true))). % 40.58/27.60 tff(c_6577, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_subject), true)=true))). % 40.58/27.60 tff(c_7009, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_domain), true)=true))). % 40.58/27.60 tff(c_11158, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__1), true)=true))). % 40.58/27.60 tff(c_3119, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_100), true, iext(Q_100, uri_rdfs_comment, uri_rdfs_Resource), true)=true))). % 40.58/27.60 tff(c_7514, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Seq), true)=true))). % 40.58/27.60 tff(c_8628, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_ex_hasFather), true)=true))). % 40.58/27.60 tff(c_25575, plain, (![D_489]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_489), true, icext(D_489, uri_rdf_first), true)=true))). % 40.58/27.60 tff(c_10091, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_isDefinedBy), true)=true))). % 40.58/27.60 tff(c_3138, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_owl_inverseOf, Q_100), true, iext(Q_100, sK1_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l3, uri_ex_hasFather), true)=true))). % 40.58/27.60 tff(c_9250, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_ex_hasCousin), true)=true))). % 40.58/27.60 tff(c_25322, plain, (![C_88, X_60]: (ifeq(icext(C_88, X_60), true, true, true)=true))). % 40.58/27.60 tff(c_13487, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_range), true)=true))). % 40.58/27.60 tff(c_5057, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_subPropertyOf), true)=true))). % 40.58/27.60 tff(c_3077, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_100), true, iext(Q_100, uri_rdf_Bag, uri_rdfs_Container), true)=true))). % 40.58/27.60 tff(c_24801, plain, (![D_477, X_478]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, D_477), true, icext(D_477, X_478), true)=true))). % 40.58/27.60 tff(c_7803, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_value), true)=true))). % 40.58/27.60 tff(c_8761, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_seeAlso), true)=true))). % 40.58/27.60 tff(c_3137, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_100), true, iext(Q_100, uri_rdf__3, uri_rdfs_Resource), true)=true))). % 40.58/27.60 tff(c_8964, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Class), true)=true))). % 40.58/27.60 tff(c_24391, plain, (![X_469, Y_470]: (ifeq(iext(uri_rdfs_domain, X_469, Y_470), true, icext(uri_rdfs_Class, Y_470), true)=true))). % 40.58/27.60 tff(c_10961, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_rest), true)=true))). % 40.58/27.60 tff(c_8627, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_ex_hasFather), true)=true))). % 40.58/27.60 tff(c_3111, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_100), true, iext(Q_100, uri_rdf__1, uri_rdfs_Resource), true)=true))). % 40.58/27.60 tff(c_7804, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_value), true)=true))). % 40.58/27.60 tff(c_24257, plain, (![X_461, Y_462]: (ifeq(iext(uri_rdfs_label, X_461, Y_462), true, icext(uri_rdfs_Literal, Y_462), true)=true))). % 40.58/27.60 tff(c_6455, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Datatype), true)=true))). % 40.58/27.60 tff(c_3126, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_100), true, iext(Q_100, uri_rdf_value, uri_rdf_Property), true)=true))). % 40.58/27.60 tff(c_8307, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_object), true)=true))). % 40.58/27.60 tff(c_10627, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_Bag), true)=true))). % 40.58/27.60 tff(c_24132, plain, (![X_453, Y_454]: (ifeq(iext(uri_rdf_object, X_453, Y_454), true, icext(uri_rdfs_Statement, X_453), true)=true))). % 40.58/27.60 tff(c_10960, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_rest), true)=true))). % 40.58/27.60 tff(c_3124, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_100), true, iext(Q_100, uri_rdfs_Datatype, uri_rdfs_Class), true)=true))). % 40.58/27.60 tff(c_11537, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_owl_propertyChainAxiom), true)=true))). % 40.58/27.60 tff(c_8308, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_object), true)=true))). % 40.58/27.60 tff(c_23919, plain, (![X_445, Y_446]: (ifeq(iext(uri_rdf_rest, X_445, Y_446), true, icext(uri_rdf_List, Y_446), true)=true))). % 40.58/27.60 tff(c_9251, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_ex_hasCousin), true)=true))). % 40.58/27.60 tff(c_11222, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_owl_inverseOf), true)=true))). % 40.58/27.60 tff(c_13577, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_subClassOf), true)=true))). % 40.58/27.60 tff(c_3217, plain, (![E_104]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_104), true, iext(uri_rdfs_subClassOf, uri_rdf_Alt, E_104), true)=true))). % 40.58/27.60 tff(c_23782, plain, (![X_437, Y_438]: (ifeq(iext(uri_rdfs_comment, X_437, Y_438), true, icext(uri_rdfs_Literal, Y_438), true)=true))). % 40.58/27.60 tff(c_12225, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdf_Property), true)=true))). % 40.58/27.61 tff(c_3122, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_100), true, iext(Q_100, uri_rdf_XMLLiteral, uri_rdfs_Literal), true)=true))). % 40.58/27.61 tff(c_12292, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_ContainerMembershipProperty), true)=true))). % 40.58/27.61 tff(c_23385, plain, (![X_430, Y_431]: (ifeq(iext(uri_rdfs_range, X_430, Y_431), true, icext(uri_rdfs_Class, Y_431), true)=true))). % 40.58/27.61 tff(c_5666, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_Alt), true)=true))). % 40.58/27.61 tff(c_3139, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_rest, Q_100), true, iext(Q_100, sK5_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l12, uri_rdf_nil), true)=true))). % 40.58/27.61 tff(c_5056, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_subPropertyOf), true)=true))). % 40.58/27.61 tff(c_11157, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__1), true)=true))). % 40.58/27.61 tff(c_5132, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_ex_hasUncle), true)=true))). % 40.58/27.61 tff(c_23220, plain, (![X_421, Y_422]: (ifeq(iext(uri_rdf_predicate, X_421, Y_422), true, icext(uri_rdfs_Statement, X_421), true)=true))). % 40.58/27.61 tff(c_6576, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_subject), true)=true))). % 40.58/27.61 tff(c_12078, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_XMLLiteral), true)=true))). % 40.58/27.61 tff(c_3114, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_100), true, iext(Q_100, uri_rdf_predicate, uri_rdfs_Resource), true)=true))). % 40.58/27.61 tff(c_22682, plain, (![X_414, Y_415]: (ifeq(iext(uri_rdfs_subPropertyOf, X_414, Y_415), true, icext(uri_rdf_Property, Y_415), true)=true))). % 40.58/27.61 tff(c_9682, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_member), true)=true))). % 40.58/27.61 tff(c_11536, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_owl_propertyChainAxiom), true)=true))). % 40.58/27.61 tff(c_10899, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__3), true)=true))). % 40.58/27.61 tff(c_3110, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_rest, Q_100), true, iext(Q_100, sK2_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l21, sK3_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l22), true)=true))). % 40.58/27.61 tff(c_7427, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Container), true)=true))). % 40.58/27.61 tff(c_12558, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_first), true)=true))). % 40.58/27.61 tff(c_11221, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_owl_inverseOf), true)=true))). % 40.58/27.61 tff(c_22481, plain, (![X_403, Y_404]: (ifeq(iext(uri_rdf_subject, X_403, Y_404), true, icext(uri_rdfs_Statement, X_403), true)=true))). % 40.58/27.61 tff(c_12559, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_first), true)=true))). % 40.58/27.61 tff(c_3084, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_100), true, iext(Q_100, uri_rdf_type, uri_rdfs_Class), true)=true))). % 40.58/27.61 tff(c_7010, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_domain), true)=true))). % 40.58/27.61 tff(c_22000, plain, (![X_396, Y_397]: (ifeq(iext(uri_rdfs_domain, X_396, Y_397), true, icext(uri_rdf_Property, X_396), true)=true))). % 40.58/27.61 tff(c_13398, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__2), true)=true))). % 40.58/27.61 tff(c_5133, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_ex_hasUncle), true)=true))). % 40.58/27.61 tff(c_3095, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_100), true, iext(Q_100, uri_rdf_Alt, uri_rdfs_Container), true)=true))). % 40.58/27.61 tff(c_21823, plain, (![X_389, Y_390]: (ifeq(iext(uri_rdf_first, X_389, Y_390), true, icext(uri_rdf_List, X_389), true)=true))). % 40.58/27.61 tff(c_12626, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_type), true)=true))). % 40.58/27.61 tff(c_13488, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_range), true)=true))). % 40.58/27.61 tff(c_3079, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_100), true, iext(Q_100, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property), true)=true))). % 40.58/27.61 tff(c_13066, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Resource), true)=true))). % 40.58/27.61 tff(c_13576, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_subClassOf), true)=true))). % 40.58/27.61 tff(c_21602, plain, (![X_380, Y_381]: (ifeq(iext(uri_rdf_rest, X_380, Y_381), true, icext(uri_rdf_List, X_380), true)=true))). % 40.58/27.61 tff(c_12627, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_type), true)=true))). % 40.58/27.61 tff(c_13397, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__2), true)=true))). % 40.58/27.61 tff(c_3135, plain, (![Q_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_ex_hasFather, Q_100), true, iext(Q_100, uri_ex_bob, uri_ex_charly), true)=true))). % 40.58/27.61 tff(c_5467, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Literal), true)=true))). % 40.58/27.61 tff(c_13818, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__3), true)=true))). % 40.58/27.61 tff(c_4919, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_29), true, icext(C_29, uri_rdfs_Resource), true)=true))). % 40.58/27.61 tff(c_21085, plain, (![X_370, Y_371]: (ifeq(iext(uri_rdfs_range, X_370, Y_371), true, icext(uri_rdf_Property, X_370), true)=true))). % 40.58/27.61 tff(c_4918, plain, (![C_19, X_133]: (ifeq(iext(uri_rdfs_domain, uri_rdf_type, C_19), true, icext(C_19, X_133), true)=true))). % 40.58/27.61 tff(c_2522, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdfs_label), true)=true))). % 40.58/27.61 tff(c_2114, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdfs_Class), true)=true))). % 40.58/27.61 tff(c_2495, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_owl_propertyChainAxiom, C_96), true, icext(C_96, uri_ex_hasUncle), true)=true))). % 40.58/27.61 tff(c_2528, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdfs_seeAlso), true)=true))). % 40.58/27.61 tff(c_20694, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_label, uri_rdfs_label)=true)). % 40.58/27.61 tff(c_2493, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdfs_member), true)=true))). % 40.58/27.61 tff(c_20509, plain, (ip(uri_rdfs_label)=true)). % 40.58/27.61 tff(c_20448, plain, (iext(uri_rdf_type, uri_rdfs_label, uri_rdf_Property)=true)). % 40.58/27.61 tff(c_20388, plain, (icext(uri_rdf_Property, uri_rdfs_label)=true)). % 40.58/27.61 tff(c_2565, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdfs_label), true)=true))). % 40.58/27.61 tff(c_2568, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdf__2), true)=true))). % 40.58/27.61 tff(c_2152, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_92), true, icext(C_92, uri_rdf_List), true)=true))). % 40.58/27.61 tff(c_19781, plain, (![X_349, Y_350]: (ifeq(iext(uri_rdf_type, X_349, Y_350), true, icext(uri_rdfs_Class, Y_350), true)=true))). % 40.58/27.61 tff(c_2523, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdf_subject), true)=true))). % 40.58/27.61 tff(c_2491, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdf_predicate), true)=true))). % 40.58/27.61 tff(c_2564, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdfs_range), true)=true))). % 40.58/27.61 tff(c_2501, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_96), true, icext(C_96, uri_rdf_Bag), true)=true))). % 40.58/27.61 tff(c_2158, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdf_rest, C_92), true, icext(C_92, sK3_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l22), true)=true))). % 40.58/27.61 tff(c_2192, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_owl_inverseOf, C_92), true, icext(C_92, uri_ex_hasFather), true)=true))). % 40.58/27.61 tff(c_2111, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_ex_hasUncle, C_92), true, icext(C_92, uri_ex_dave), true)=true))). % 40.58/27.61 tff(c_2552, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_96), true, icext(C_96, uri_rdf_XMLLiteral), true)=true))). % 40.58/27.61 tff(c_2518, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdf_first), true)=true))). % 40.58/27.61 tff(c_2153, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdf_Property), true)=true))). % 40.58/27.61 tff(c_2513, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdfs_isDefinedBy), true)=true))). % 40.58/27.61 tff(c_2161, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_owl_propertyChainAxiom, C_92), true, icext(C_92, sK2_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l21), true)=true))). % 40.58/27.61 tff(c_2516, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_96), true, icext(C_96, uri_rdfs_Seq), true)=true))). % 40.58/27.61 tff(c_2125, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdf_first, C_92), true, icext(C_92, uri_ex_hasCousin), true)=true))). % 40.58/27.61 tff(c_2136, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_92), true, icext(C_92, uri_rdfs_Container), true)=true))). % 40.58/27.61 tff(c_18703, plain, (![X_326, Y_327]: (ifeq(iext(uri_rdfs_subClassOf, X_326, Y_327), true, icext(uri_rdfs_Class, X_326), true)=true))). % 40.58/27.61 tff(c_2571, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_owl_inverseOf, C_96), true, icext(C_96, sK1_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l3), true)=true))). % 40.58/27.61 tff(c_2573, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdf_first, C_96), true, icext(C_96, sK5_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l12), true)=true))). % 40.58/27.61 tff(c_2155, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_92), true, icext(C_92, uri_rdf_Property), true)=true))). % 40.58/27.61 tff(c_2520, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_96), true, icext(C_96, uri_rdf_Alt), true)=true))). % 40.58/27.61 tff(c_2175, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_92), true, icext(C_92, uri_rdfs_Class), true)=true))). % 40.58/27.61 tff(c_2562, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdf__2), true)=true))). % 40.58/27.61 tff(c_2546, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdf_rest), true)=true))). % 40.58/27.61 tff(c_2502, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdf_rest, C_96), true, icext(C_96, sK3_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l22), true)=true))). % 40.58/27.61 tff(c_2496, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdfs_comment), true)=true))). % 40.58/27.61 tff(c_2547, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdf_rest), true)=true))). % 40.58/27.61 tff(c_2531, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdf_first, C_96), true, icext(C_96, sK2_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l21), true)=true))). % 40.58/27.61 tff(c_2123, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_92), true, icext(C_92, uri_rdf_Property), true)=true))). % 40.58/27.61 tff(c_2165, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_92), true, icext(C_92, uri_rdfs_seeAlso), true)=true))). % 40.58/27.61 tff(c_2545, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdf_value), true)=true))). % 40.58/27.61 tff(c_2535, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdfs_subPropertyOf), true)=true))). % 40.58/27.61 tff(c_18213, plain, (iext(uri_rdf_type, sK2_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l21, uri_rdf_List)=true)). % 40.58/27.61 tff(c_2525, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_ex_hasCousin, C_96), true, icext(C_96, uri_ex_alice), true)=true))). % 40.58/27.61 tff(c_18034, plain, (icext(uri_rdf_List, sK2_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l21)=true)). % 40.58/27.61 tff(c_2538, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdf_rest, C_96), true, icext(C_96, sK2_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l21), true)=true))). % 40.58/27.61 tff(c_17679, plain, (![X_305, Y_306]: (ifeq(iext(uri_rdfs_subPropertyOf, X_305, Y_306), true, icext(uri_rdf_Property, X_305), true)=true))). % 40.58/27.61 tff(c_2543, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_96), true, icext(C_96, uri_rdfs_isDefinedBy), true)=true))). % 40.58/27.61 tff(c_2173, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_92), true, icext(C_92, uri_rdfs_Literal), true)=true))). % 40.58/27.61 tff(c_2570, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdf__3), true)=true))). % 40.58/27.61 tff(c_2170, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdf_List), true)=true))). % 40.58/27.61 tff(c_17369, plain, (iext(uri_rdf_type, sK3_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l22, uri_rdf_List)=true)). % 40.58/27.61 tff(c_17207, plain, (icext(uri_rdf_List, sK3_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l22)=true)). % 40.58/27.61 tff(c_2537, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdf_first, C_96), true, icext(C_96, sK3_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l22), true)=true))). % 40.58/27.61 tff(c_2194, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdf_first, C_92), true, icext(C_92, uri_ex_hasFather), true)=true))). % 40.58/27.61 tff(c_2540, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_owl_propertyChainAxiom, C_96), true, icext(C_96, uri_ex_hasCousin), true)=true))). % 40.58/27.61 tff(c_2128, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_92), true, icext(C_92, uri_rdfs_Class), true)=true))). % 40.58/27.61 tff(c_2550, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdf_first), true)=true))). % 40.58/27.61 tff(c_2115, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_owl_propertyChainAxiom, C_92), true, icext(C_92, sK4_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l11), true)=true))). % 40.58/27.61 tff(c_2119, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_ex_hasFather, C_92), true, icext(C_92, uri_ex_dave), true)=true))). % 40.58/27.61 tff(c_2147, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_ex_hasCousin, C_92), true, icext(C_92, uri_ex_bob), true)=true))). % 40.58/27.61 tff(c_2526, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdf_subject), true)=true))). % 40.58/27.61 tff(c_2536, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdf_object), true)=true))). % 40.58/27.61 tff(c_2193, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdf_rest, C_92), true, icext(C_92, uri_rdf_nil), true)=true))). % 40.58/27.61 tff(c_2551, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdf__3), true)=true))). % 40.58/27.61 tff(c_2519, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdfs_seeAlso), true)=true))). % 40.58/27.61 tff(c_16239, plain, (![X_273, Y_274]: (ifeq(iext(uri_rdfs_subClassOf, X_273, Y_274), true, icext(uri_rdfs_Class, Y_274), true)=true))). % 40.58/27.61 tff(c_15317, plain, (![X_33]: (ifeq(icext(uri_rdf_List, X_33), true, icext(uri_rdf_List, X_33), true)=true))). % 40.58/27.61 tff(c_15384, plain, (![X_33]: (ifeq(icext(uri_rdfs_Statement, X_33), true, icext(uri_rdfs_Statement, X_33), true)=true))). % 40.58/27.61 tff(c_12079, plain, (![X_33]: (ifeq(icext(uri_rdf_XMLLiteral, X_33), true, icext(uri_rdf_XMLLiteral, X_33), true)=true))). % 40.58/27.61 tff(c_2560, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdf_value), true)=true))). % 40.58/27.61 tff(c_12227, plain, (![X_33]: (ifeq(icext(uri_rdf_Property, X_33), true, icext(uri_rdf_Property, X_33), true)=true))). % 40.58/27.61 tff(c_10628, plain, (![X_33]: (ifeq(icext(uri_rdf_Bag, X_33), true, icext(uri_rdf_Bag, X_33), true)=true))). % 40.58/27.61 tff(c_5469, plain, (![X_33]: (ifeq(icext(uri_rdfs_Literal, X_33), true, icext(uri_rdfs_Literal, X_33), true)=true))). % 40.58/27.61 tff(c_5667, plain, (![X_33]: (ifeq(icext(uri_rdf_Alt, X_33), true, icext(uri_rdf_Alt, X_33), true)=true))). % 40.58/27.61 tff(c_7515, plain, (![X_33]: (ifeq(icext(uri_rdfs_Seq, X_33), true, icext(uri_rdfs_Seq, X_33), true)=true))). % 40.58/27.61 tff(c_12293, plain, (![X_33]: (ifeq(icext(uri_rdfs_ContainerMembershipProperty, X_33), true, icext(uri_rdfs_ContainerMembershipProperty, X_33), true)=true))). % 40.58/27.61 tff(c_10178, plain, (![X_33]: (ifeq(icext(uri_rdfs_Class, X_33), true, icext(uri_rdfs_Class, X_33), true)=true))). % 40.58/27.61 tff(c_7429, plain, (![X_33]: (ifeq(icext(uri_rdfs_Container, X_33), true, icext(uri_rdfs_Container, X_33), true)=true))). % 40.58/27.61 tff(c_2508, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdf_type), true)=true))). % 40.58/27.61 tff(c_6456, plain, (![X_33]: (ifeq(icext(uri_rdfs_Datatype, X_33), true, icext(uri_rdfs_Datatype, X_33), true)=true))). % 40.58/27.61 tff(c_15882, plain, (iext(uri_rdf_type, uri_rdfs_Resource, uri_rdfs_Class)=true)). % 40.58/27.61 tff(c_15817, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_predicate, uri_rdf_predicate)=true)). % 40.58/27.61 tff(c_15751, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_comment, uri_rdfs_comment)=true)). % 40.58/27.61 tff(c_15678, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Resource, uri_rdfs_Resource)=true)). % 40.58/27.61 tff(c_15584, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_member, uri_rdfs_member)=true)). % 40.58/27.61 tff(c_2559, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdfs_domain), true)=true))). % 40.58/27.61 tff(c_15419, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Statement, uri_rdfs_Resource)=true)). % 40.58/27.61 tff(c_2555, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdfs_subClassOf), true)=true))). % 40.58/27.61 tff(c_15328, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Statement, uri_rdfs_Statement)=true)). % 40.58/27.61 tff(c_15261, plain, (iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdf_List)=true)). % 40.58/27.61 tff(c_2499, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_ex_hasFather, C_96), true, icext(C_96, uri_ex_alice), true)=true))). % 40.58/27.61 tff(c_15074, plain, (iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdfs_Resource)=true)). % 40.58/27.61 tff(c_15025, plain, (iext(uri_rdf_type, uri_rdfs_Datatype, uri_rdfs_Class)=true)). % 40.58/27.61 tff(c_2566, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_ex_hasFather, C_96), true, icext(C_96, uri_ex_bob), true)=true))). % 40.58/27.61 tff(c_14960, plain, (iext(uri_rdf_type, uri_rdf_Bag, uri_rdfs_Class)=true)). % 40.58/27.61 tff(c_14913, plain, (iext(uri_rdf_type, uri_rdfs_Class, uri_rdfs_Class)=true)). % 40.58/27.61 tff(c_14866, plain, (iext(uri_rdf_type, uri_rdfs_Literal, uri_rdfs_Class)=true)). % 40.58/27.61 tff(c_2157, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdf_first, C_92), true, icext(C_92, sK1_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l3), true)=true))). % 40.58/27.61 tff(c_14797, plain, (iext(uri_rdf_type, uri_rdf_Alt, uri_rdfs_Class)=true)). % 40.58/27.61 tff(c_14748, plain, (iext(uri_rdf_type, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Class)=true)). % 40.58/27.61 tff(c_2490, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_ex_hasUncle, C_96), true, icext(C_96, uri_ex_bob), true)=true))). % 40.58/27.61 tff(c_14681, plain, (iext(uri_rdf_type, uri_rdfs_Seq, uri_rdfs_Class)=true)). % 40.58/27.61 tff(c_14633, plain, (iext(uri_rdf_type, uri_rdf_List, uri_rdfs_Class)=true)). % 40.58/27.61 tff(c_2533, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdfs_range), true)=true))). % 40.58/27.61 tff(c_14473, plain, (ic(uri_rdf_List)=true)). % 40.58/27.61 tff(c_14415, plain, (icext(uri_rdfs_Class, uri_rdf_List)=true)). % 40.58/27.61 tff(c_2168, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_92), true, icext(C_92, uri_rdf_List), true)=true))). % 40.58/27.61 tff(c_14348, plain, (iext(uri_rdf_type, uri_rdf_XMLLiteral, uri_rdfs_Class)=true)). % 40.58/27.61 tff(c_14271, plain, (iext(uri_rdf_type, uri_rdfs_Container, uri_rdfs_Class)=true)). % 40.58/27.61 tff(c_2151, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdf_first, C_92), true, icext(C_92, uri_ex_hasUncle), true)=true))). % 40.58/27.61 tff(c_14223, plain, (iext(uri_rdf_type, sK4_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l11, uri_rdf_List)=true)). % 40.58/27.61 tff(c_14176, plain, (iext(uri_rdf_type, sK5_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l12, uri_rdf_List)=true)). % 40.58/27.61 tff(c_14133, plain, (ip(uri_rdf_predicate)=true)). % 40.58/27.61 tff(c_14076, plain, (iext(uri_rdf_type, uri_rdf_predicate, uri_rdf_Property)=true)). % 40.58/27.61 tff(c_14032, plain, (ip(uri_rdfs_comment)=true)). % 40.58/27.61 tff(c_13975, plain, (iext(uri_rdf_type, uri_rdfs_comment, uri_rdf_Property)=true)). % 40.58/27.61 tff(c_13920, plain, (iext(uri_rdf_type, uri_rdfs_member, uri_rdf_Property)=true)). % 40.58/27.61 tff(c_2517, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdfs_subPropertyOf), true)=true))). % 40.58/27.61 tff(c_13848, plain, (iext(uri_rdf_type, uri_rdfs_Statement, uri_rdfs_Class)=true)). % 40.58/27.61 tff(c_717, plain, (![S_69, O_70]: (ifeq(iext(uri_rdf_rest, S_69, O_70), true, true, true)=true))). % 40.58/27.61 tff(c_13763, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__3, uri_rdf__3)=true)). % 40.58/27.61 tff(c_2509, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdfs_domain), true)=true))). % 40.58/27.61 tff(c_13587, plain, (icext(uri_rdf_Property, uri_rdf_predicate)=true)). % 40.58/27.61 tff(c_13502, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, uri_rdfs_subClassOf)=true)). % 40.58/27.61 tff(c_2542, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdf_predicate), true)=true))). % 40.58/27.62 tff(c_13433, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_range, uri_rdfs_range)=true)). % 40.58/27.62 tff(c_13343, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__2, uri_rdf__2)=true)). % 40.58/27.62 tff(c_3622, plain, (![S_5, O_6]: (ifeq(iext(uri_ex_hasUncle, S_5, O_6), true, true, true)=true))). % 40.58/27.62 tff(c_2146, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_92), true, icext(C_92, uri_rdfs_Datatype), true)=true))). % 40.58/27.62 tff(c_13157, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Resource)=true)). % 40.58/27.62 tff(c_13011, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdfs_Resource)=true)). % 40.58/27.62 tff(c_12887, plain, (icext(uri_rdf_Property, uri_ex_hasUncle)=true)). % 40.58/27.62 tff(c_12833, plain, (iext(uri_rdf_type, uri_ex_hasUncle, uri_rdf_Property)=true)). % 40.58/27.62 tff(c_1208, plain, (![S_5, O_6]: (ifeq(iext(uri_ex_hasFather, S_5, O_6), true, true, true)=true))). % 40.58/27.62 tff(c_12692, plain, (icext(uri_rdf_Property, uri_ex_hasCousin)=true)). % 40.58/27.62 tff(c_12637, plain, (iext(uri_rdf_type, uri_ex_hasCousin, uri_rdf_Property)=true)). % 40.58/27.62 tff(c_12572, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_type, uri_rdf_type)=true)). % 40.58/27.62 tff(c_12479, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_first, uri_rdf_first)=true)). % 40.58/27.62 tff(c_2572, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdf_rest, C_96), true, icext(C_96, sK5_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l12), true)=true))). % 40.58/27.62 tff(c_12336, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Resource)=true)). % 40.58/27.62 tff(c_2539, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdf__1), true)=true))). % 40.58/27.62 tff(c_12237, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdfs_ContainerMembershipProperty)=true)). % 40.58/27.62 tff(c_12171, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdf_Property)=true)). % 40.58/27.62 tff(c_1459, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_subClassOf, S_5, O_6), true, true, true)=true))). % 40.58/27.62 tff(c_11998, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdf_XMLLiteral)=true)). % 40.58/27.62 tff(c_2503, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_96), true, icext(C_96, uri_rdfs_ContainerMembershipProperty), true)=true))). % 40.58/27.62 tff(c_3310, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_subPropertyOf, S_5, O_6), true, true, true)=true))). % 40.58/27.62 tff(c_11677, plain, (icext(uri_rdf_Property, uri_rdfs_comment)=true)). % 40.58/27.62 tff(c_2549, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdfs_comment), true)=true))). % 40.58/27.62 tff(c_11602, plain, (iext(uri_rdf_type, uri_rdfs_isDefinedBy, uri_rdf_Property)=true)). % 40.58/27.62 tff(c_11483, plain, (iext(uri_rdfs_subPropertyOf, uri_owl_propertyChainAxiom, uri_owl_propertyChainAxiom)=true)). % 40.58/27.62 tff(c_11421, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Resource)=true)). % 40.58/27.62 tff(c_2189, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_ex_hasFather, C_92), true, icext(C_92, uri_ex_charly), true)=true))). % 40.58/27.62 tff(c_11168, plain, (iext(uri_rdfs_subPropertyOf, uri_owl_inverseOf, uri_owl_inverseOf)=true)). % 40.58/27.62 tff(c_11103, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__1, uri_rdf__1)=true)). % 40.58/27.62 tff(c_1559, plain, (![S_5, O_6]: (ifeq(iext(uri_owl_propertyChainAxiom, S_5, O_6), true, true, true)=true))). % 40.58/27.62 tff(c_10971, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__2, uri_rdfs_member)=true)). % 40.58/27.62 tff(c_10910, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_rest, uri_rdf_rest)=true)). % 40.58/27.62 tff(c_10824, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__3, uri_rdfs_member)=true)). % 40.58/27.62 tff(c_2162, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_92), true, icext(C_92, uri_rdfs_Class), true)=true))). % 40.58/27.62 tff(c_10717, plain, (icext(uri_rdf_Property, uri_rdfs_domain)=true)). % 40.58/27.62 tff(c_10663, plain, (iext(uri_rdf_type, uri_rdfs_domain, uri_rdf_Property)=true)). % 40.58/27.62 tff(c_2116, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_92), true, icext(C_92, uri_rdfs_Literal), true)=true))). % 40.58/27.62 tff(c_10569, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdf_Bag)=true)). % 40.58/27.62 tff(c_10462, plain, (icext(uri_rdf_Property, uri_ex_hasFather)=true)). % 40.58/27.62 tff(c_10408, plain, (iext(uri_rdf_type, uri_ex_hasFather, uri_rdf_Property)=true)). % 40.58/27.62 tff(c_10302, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Container, uri_rdfs_Resource)=true)). % 40.58/27.62 tff(c_10126, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdfs_Class)=true)). % 40.58/27.62 tff(c_2506, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdf_rest, C_96), true, icext(C_96, sK4_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l11), true)=true))). % 40.58/27.62 tff(c_10037, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, uri_rdfs_isDefinedBy)=true)). % 40.58/27.62 tff(c_9692, plain, (ip(uri_rdfs_member)=true)). % 40.58/27.62 tff(c_9627, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__1, uri_rdfs_member)=true)). % 40.58/27.62 tff(c_971, plain, (![S_5, O_6]: (ifeq(iext(uri_owl_inverseOf, S_5, O_6), true, true, true)=true))). % 40.58/27.62 tff(c_2558, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdf_type), true)=true))). % 40.58/27.62 tff(c_9193, plain, (iext(uri_rdfs_subPropertyOf, uri_ex_hasCousin, uri_ex_hasCousin)=true)). % 40.58/27.62 tff(c_8914, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdfs_Resource)=true)). % 40.58/27.62 tff(c_2164, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_92), true, icext(C_92, uri_rdfs_Resource), true)=true))). % 40.58/27.62 tff(c_1176, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_range, S_5, O_6), true, true, true)=true))). % 40.58/27.62 tff(c_8708, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_seeAlso, uri_rdfs_seeAlso)=true)). % 40.58/27.62 tff(c_2117, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_92), true, icext(C_92, uri_rdf_Property), true)=true))). % 40.58/27.62 tff(c_8570, plain, (iext(uri_rdfs_subPropertyOf, uri_ex_hasFather, uri_ex_hasFather)=true)). % 40.58/27.62 tff(c_8399, plain, (icext(uri_rdf_Property, uri_rdfs_isDefinedBy)=true)). % 40.58/27.62 tff(c_2514, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdfs_isDefinedBy), true)=true))). % 40.58/27.62 tff(c_8318, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Resource)=true)). % 40.58/27.62 tff(c_8257, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_object, uri_rdf_object)=true)). % 40.58/27.62 tff(c_2494, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdfs_subClassOf), true)=true))). % 40.58/27.62 tff(c_1607, plain, (![S_5, O_6]: (ifeq(iext(uri_ex_hasCousin, S_5, O_6), true, true, true)=true))). % 40.58/27.62 tff(c_7914, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Resource)=true)). % 40.58/27.62 tff(c_7753, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_value, uri_rdf_value)=true)). % 40.58/27.62 tff(c_7646, plain, (icext(uri_rdf_Property, uri_rdfs_subClassOf)=true)). % 40.58/27.62 tff(c_7592, plain, (iext(uri_rdf_type, uri_rdfs_subClassOf, uri_rdf_Property)=true)). % 40.58/27.62 tff(c_7439, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Seq)=true)). % 40.58/27.62 tff(c_2554, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_96), true, icext(C_96, uri_rdfs_Datatype), true)=true))). % 40.58/27.62 tff(c_7377, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Container, uri_rdfs_Container)=true)). % 40.58/27.62 tff(c_7180, plain, (icext(uri_rdf_Property, uri_owl_propertyChainAxiom)=true)). % 40.58/27.62 tff(c_7126, plain, (iext(uri_rdf_type, uri_owl_propertyChainAxiom, uri_rdf_Property)=true)). % 40.58/27.62 tff(c_2530, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdf__1), true)=true))). % 40.58/27.62 tff(c_6959, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, uri_rdfs_domain)=true)). % 40.58/27.62 tff(c_6910, plain, (icext(uri_rdf_List, sK5_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l12)=true)). % 40.58/27.62 tff(c_2126, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdf_rest, C_92), true, icext(C_92, sK5_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l12), true)=true))). % 40.58/27.62 tff(c_6846, plain, (ic(uri_rdfs_Statement)=true)). % 40.58/27.62 tff(c_6797, plain, (icext(uri_rdfs_Class, uri_rdfs_Statement)=true)). % 40.58/27.62 tff(c_2156, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdfs_Statement), true)=true))). % 40.58/27.62 tff(c_6703, plain, (icext(uri_rdf_Property, uri_rdfs_range)=true)). % 40.58/27.62 tff(c_6649, plain, (iext(uri_rdf_type, uri_rdfs_range, uri_rdf_Property)=true)). % 40.58/27.62 tff(c_2178, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdfs_Resource), true)=true))). % 40.58/27.62 tff(c_2598, plain, (![S_5, O_6]: (ifeq(iext(uri_rdf_object, S_5, O_6), true, true, true)=true))). % 40.58/27.62 tff(c_6522, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_subject, uri_rdf_subject)=true)). % 40.58/27.62 tff(c_2174, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_92), true, icext(C_92, uri_rdfs_ContainerMembershipProperty), true)=true))). % 40.58/27.62 tff(c_6404, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Datatype)=true)). % 40.58/27.62 tff(c_6327, plain, (icext(uri_rdf_Property, uri_rdfs_member)=true)). % 40.58/27.62 tff(c_2561, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdfs_member), true)=true))). % 40.58/27.62 tff(c_6203, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdfs_Resource)=true)). % 40.58/27.62 tff(c_6057, plain, (icext(uri_rdf_List, sK4_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l11)=true)). % 40.58/27.62 tff(c_2505, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdf_first, C_96), true, icext(C_96, sK4_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l11), true)=true))). % 40.58/27.62 tff(c_5987, plain, (icext(uri_rdf_Property, uri_owl_inverseOf)=true)). % 40.58/27.62 tff(c_5880, plain, (iext(uri_rdf_type, uri_owl_inverseOf, uri_rdf_Property)=true)). % 40.58/27.62 tff(c_1792, plain, (![X_89]: (ifeq(icext(uri_rdfs_Datatype, X_89), true, icext(uri_rdfs_Class, X_89), true)=true))). % 40.58/27.62 tff(c_5834, plain, (icext(uri_rdfs_Class, uri_rdfs_Resource)=true)). % 40.58/27.62 tff(c_5771, plain, (ic(uri_rdfs_Resource)=true)). % 40.58/27.62 tff(c_1790, plain, (![X_89]: (ifeq(icext(uri_rdf_Alt, X_89), true, icext(uri_rdfs_Container, X_89), true)=true))). % 40.58/27.62 tff(c_5703, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Resource)=true)). % 40.58/27.62 tff(c_5615, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdf_Alt)=true)). % 40.58/27.62 tff(c_1787, plain, (![X_89]: (ifeq(icext(uri_rdf_Bag, X_89), true, icext(uri_rdfs_Container, X_89), true)=true))). % 40.58/27.62 tff(c_1788, plain, (![X_89]: (ifeq(icext(uri_rdfs_ContainerMembershipProperty, X_89), true, icext(uri_rdf_Property, X_89), true)=true))). % 40.58/27.62 tff(c_5414, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdfs_Literal)=true)). % 40.58/27.62 tff(c_5375, plain, (icext(uri_rdf_Property, uri_rdfs_subPropertyOf)=true)). % 40.58/27.62 tff(c_5311, plain, (iext(uri_rdf_type, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 40.58/27.62 tff(c_1791, plain, (![X_89]: (ifeq(icext(uri_rdf_XMLLiteral, X_89), true, icext(uri_rdfs_Literal, X_89), true)=true))). % 40.58/27.62 tff(c_1285, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_domain, S_5, O_6), true, true, true)=true))). % 40.58/27.62 tff(c_5207, plain, (icext(uri_rdf_Property, uri_rdfs_seeAlso)=true)). % 40.58/27.62 tff(c_5150, plain, (iext(uri_rdf_type, uri_rdfs_seeAlso, uri_rdf_Property)=true)). % 40.58/27.62 tff(c_1789, plain, (![X_89]: (ifeq(icext(uri_rdfs_Seq, X_89), true, icext(uri_rdfs_Container, X_89), true)=true))). % 40.58/27.62 tff(c_5082, plain, (iext(uri_rdfs_subPropertyOf, uri_ex_hasUncle, uri_ex_hasUncle)=true)). % 40.58/27.62 tff(c_5006, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf)=true)). % 40.58/27.62 tff(c_2163, plain, (![X_93, Y_94]: (ifeq(iext(uri_rdf_predicate, X_93, Y_94), true, true, true)=true))). % 40.58/27.62 tff(c_2548, plain, (![X_97, Y_98]: (ifeq(iext(uri_rdfs_comment, X_97, Y_98), true, true, true)=true))). % 40.58/27.62 tff(c_2557, plain, (![X_97, Y_98]: (ifeq(iext(uri_rdf_type, X_97, Y_98), true, true, true)=true))). % 40.58/27.62 tff(c_4878, plain, (![X_132]: (iext(uri_rdf_type, X_132, uri_rdfs_Resource)=true))). % 40.58/27.62 tff(c_2569, plain, (![X_97, Y_98]: (ifeq(iext(uri_rdf__3, X_97, Y_98), true, true, true)=true))). % 40.58/27.62 tff(c_2527, plain, (![X_97, Y_98]: (ifeq(iext(uri_rdfs_seeAlso, X_97, Y_98), true, true, true)=true))). % 40.58/27.62 tff(c_2138, plain, (![X_93, Y_94]: (ifeq(iext(uri_rdf_first, X_93, Y_94), true, true, true)=true))). % 40.58/27.62 tff(c_2184, plain, (![X_93, Y_94]: (ifeq(iext(uri_rdf__2, X_93, Y_94), true, true, true)=true))). % 40.58/27.62 tff(c_2159, plain, (![X_93, Y_94]: (ifeq(iext(uri_rdf__1, X_93, Y_94), true, true, true)=true))). % 40.58/27.62 tff(c_2144, plain, (![X_93, Y_94]: (ifeq(iext(uri_rdf_subject, X_93, Y_94), true, true, true)=true))). % 40.58/27.62 tff(c_2182, plain, (![X_93, Y_94]: (ifeq(iext(uri_rdfs_member, X_93, Y_94), true, true, true)=true))). % 40.58/27.62 tff(c_2133, plain, (![X_93, Y_94]: (ifeq(iext(uri_rdfs_isDefinedBy, X_93, Y_94), true, true, true)=true))). % 40.58/27.62 tff(c_4741, plain, (icext(uri_rdfs_Class, uri_rdfs_Datatype)=true)). % 40.58/27.62 tff(c_4696, plain, (icext(uri_rdfs_Class, uri_rdf_Bag)=true)). % 40.58/27.62 tff(c_4649, plain, (icext(uri_rdfs_Class, uri_rdfs_Literal)=true)). % 40.58/27.62 tff(c_4589, plain, (icext(uri_rdfs_Class, uri_rdfs_Class)=true)). % 40.58/27.62 tff(c_4544, plain, (icext(uri_rdfs_Class, uri_rdfs_Container)=true)). % 40.58/27.62 tff(c_4495, plain, (icext(uri_rdfs_Class, uri_rdf_XMLLiteral)=true)). % 40.58/27.62 tff(c_2521, plain, (![X_97, Y_98]: (ifeq(iext(uri_rdfs_label, X_97, Y_98), true, true, true)=true))). % 40.58/27.62 tff(c_4441, plain, (icext(uri_rdfs_Class, uri_rdfs_ContainerMembershipProperty)=true)). % 40.58/27.62 tff(c_4398, plain, (icext(uri_rdfs_Class, uri_rdfs_Seq)=true)). % 40.58/27.62 tff(c_2544, plain, (![X_97, Y_98]: (ifeq(iext(uri_rdf_value, X_97, Y_98), true, true, true)=true))). % 40.58/27.62 tff(c_4343, plain, (icext(uri_rdfs_Class, uri_rdf_Alt)=true)). % 40.58/27.62 tff(c_4303, plain, (icext(uri_rdf_Property, uri_rdf_first)=true)). % 40.58/27.62 tff(c_4264, plain, (icext(uri_rdf_Property, uri_rdf_value)=true)). % 40.58/27.62 tff(c_4224, plain, (icext(uri_rdf_Property, uri_rdf_subject)=true)). % 40.58/27.62 tff(c_4182, plain, (icext(uri_rdf_Property, uri_rdf__3)=true)). % 40.58/27.62 tff(c_4143, plain, (icext(uri_rdf_Property, uri_rdf_type)=true)). % 40.58/27.62 tff(c_4077, plain, (icext(uri_rdf_Property, uri_rdf__2)=true)). % 40.58/27.62 tff(c_4067, plain, (icext(uri_rdf_Property, uri_rdf_rest)=true)). % 40.58/27.62 tff(c_4021, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__1)=true)). % 40.58/27.62 tff(c_3976, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__2)=true)). % 40.58/27.62 tff(c_3940, plain, (icext(uri_rdf_List, uri_rdf_nil)=true)). % 40.58/27.62 tff(c_3900, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__3)=true)). % 40.58/27.62 tff(c_3853, plain, (icext(uri_rdfs_Class, uri_rdf_Property)=true)). % 40.58/27.62 tff(c_3798, plain, (icext(uri_rdfs_Datatype, uri_rdf_XMLLiteral)=true)). % 40.58/27.62 tff(c_3757, plain, (icext(uri_rdf_Property, uri_rdf__1)=true)). % 40.58/27.62 tff(c_3720, plain, (icext(uri_rdf_Property, uri_rdf_object)=true)). % 40.58/27.62 tff(c_3677, plain, (ic(uri_rdfs_Seq)=true)). % 40.58/27.62 tff(c_3640, plain, (ic(uri_rdf_Property)=true)). % 40.58/27.62 tff(c_3601, plain, (ip(uri_ex_hasUncle)=true)). % 40.58/27.62 tff(c_3559, plain, (ip(uri_rdf__2)=true)). % 40.58/27.62 tff(c_3523, plain, (ip(uri_rdfs_isDefinedBy)=true)). % 40.58/27.62 tff(c_3488, plain, (ic(uri_rdfs_Class)=true)). % 40.58/27.62 tff(c_3450, plain, (ic(uri_rdf_Alt)=true)). % 40.58/27.62 tff(c_3415, plain, (ic(uri_rdf_XMLLiteral)=true)). % 40.58/27.62 tff(c_3371, plain, (ip(uri_rdf__3)=true)). % 40.58/27.62 tff(c_3329, plain, (ip(uri_rdf__1)=true)). % 40.58/27.62 tff(c_3289, plain, (ip(uri_rdfs_subPropertyOf)=true)). % 40.58/27.62 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))). % 40.58/27.62 tff(c_3146, plain, (ic(uri_rdfs_Literal)=true)). % 40.58/27.62 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))). % 40.58/27.62 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))). % 40.58/27.62 tff(c_2577, plain, (ip(uri_rdf_object)=true)). % 40.58/27.62 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))). % 40.58/27.62 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))). % 40.58/27.62 tff(c_1749, plain, (ic(uri_rdfs_Datatype)=true)). % 40.58/27.62 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))). % 40.58/27.62 tff(c_1714, plain, (ic(uri_rdf_Bag)=true)). % 40.58/27.62 tff(c_212, plain, (tuple(iext(uri_ex_hasCousin, uri_ex_bob, uri_ex_alice), iext(uri_ex_hasUncle, uri_ex_alice, uri_ex_charly))!=tuple(true, true))). % 40.58/27.62 tff(c_1677, plain, (ip(uri_rdf_subject)=true)). % 40.58/27.62 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))). % 40.58/27.62 tff(c_1586, plain, (ip(uri_ex_hasCousin)=true)). % 40.58/27.62 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))). % 40.58/27.62 tff(c_1487, plain, (ip(uri_owl_propertyChainAxiom)=true)). % 40.58/27.62 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))). % 40.58/27.62 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))). % 40.58/27.62 tff(c_1438, plain, (ip(uri_rdfs_subClassOf)=true)). % 40.58/27.62 tff(c_58, plain, (![C_15]: (ifeq(ic(C_15), true, iext(uri_rdfs_subClassOf, C_15, uri_rdfs_Resource), true)=true))). % 40.58/27.62 tff(c_1385, plain, (ic(uri_rdfs_Container)=true)). % 40.58/27.62 tff(c_164, plain, (![P_45, Q_46]: (ifeq(iext(uri_rdfs_subPropertyOf, P_45, Q_46), true, ip(P_45), true)=true))). % 40.58/27.62 tff(c_1300, plain, (ic(uri_rdfs_ContainerMembershipProperty)=true)). % 40.58/27.62 tff(c_1264, plain, (ip(uri_rdfs_domain)=true)). % 40.58/27.62 tff(c_156, plain, (![C_39]: (ifeq(ic(C_39), true, iext(uri_rdfs_subClassOf, C_39, C_39), true)=true))). % 40.58/27.62 tff(c_152, plain, (![C_37, D_38]: (ifeq(iext(uri_rdfs_subClassOf, C_37, D_38), true, ic(C_37), true)=true))). % 40.58/27.62 tff(c_1190, plain, (ip(uri_ex_hasFather)=true)). % 40.58/27.62 tff(c_1133, plain, (ip(uri_rdfs_range)=true)). % 40.58/27.62 tff(c_150, plain, (![C_35, D_36]: (ifeq(iext(uri_rdfs_subClassOf, C_35, D_36), true, ic(D_36), true)=true))). % 40.58/27.62 tff(c_1044, plain, (ip(uri_rdf_type)=true)). % 40.58/27.62 tff(c_28, plain, (![P_9]: (ifeq(ip(P_9), true, iext(uri_rdf_type, P_9, uri_rdf_Property), true)=true))). % 40.58/27.62 tff(c_1015, plain, (ip(uri_rdfs_seeAlso)=true)). % 40.58/27.62 tff(c_162, plain, (![P_43, Q_44]: (ifeq(iext(uri_rdfs_subPropertyOf, P_43, Q_44), true, ip(Q_44), true)=true))). % 40.58/27.62 tff(c_959, plain, (ip(uri_owl_inverseOf)=true)). % 40.58/27.62 tff(c_4, plain, (![P_4, S_5, O_6]: (ifeq(iext(P_4, S_5, O_6), true, ip(P_4), true)=true))). % 40.58/27.62 tff(c_681, plain, (ip(uri_rdf_first)=true)). % 40.58/27.62 tff(c_657, plain, (ip(uri_rdf_value)=true)). % 40.58/27.62 tff(c_170, plain, (![P_51]: (ifeq(ip(P_51), true, iext(uri_rdfs_subPropertyOf, P_51, P_51), true)=true))). % 40.58/27.62 tff(c_626, plain, (ip(uri_rdf_rest)=true)). % 40.58/27.62 tff(c_30, plain, (![P_10]: (ifeq(iext(uri_rdf_type, P_10, uri_rdf_Property), true, ip(P_10), true)=true))). % 40.58/27.62 tff(c_124, plain, (![X_27]: (ifeq(lv(X_27), true, icext(uri_rdfs_Literal, X_27), true)=true))). % 40.58/27.62 tff(c_122, plain, (![X_26]: (ifeq(icext(uri_rdfs_Literal, X_26), true, lv(X_26), true)=true))). % 40.58/27.62 tff(c_116, plain, (![X_23]: (ifeq(icext(uri_rdfs_Class, X_23), true, ic(X_23), true)=true))). % 40.58/27.62 tff(c_114, plain, (![X_22]: (ifeq(ic(X_22), true, icext(uri_rdfs_Class, X_22), true)=true))). % 40.58/27.62 tff(c_542, plain, (![X_60]: (icext(uri_rdfs_Resource, X_60)=true))). % 40.58/27.62 tff(c_217, plain, (![X_8]: (ifeq(lv(X_8), true, true, true)=true))). % 40.58/27.62 tff(c_2, plain, (![A_1, B_2, C_3]: (ifeq(A_1, A_1, B_2, C_3)=B_2))). % 40.58/27.62 tff(c_208, plain, (iext(uri_ex_hasUncle, uri_ex_bob, uri_ex_dave)=true)). % 40.58/27.62 tff(c_138, plain, (iext(uri_rdfs_domain, uri_rdf_predicate, uri_rdfs_Statement)=true)). % 40.58/27.62 tff(c_76, plain, (iext(uri_rdfs_domain, uri_rdfs_member, uri_rdfs_Resource)=true)). % 40.58/27.62 tff(c_146, plain, (iext(uri_rdfs_domain, uri_rdfs_subClassOf, uri_rdfs_Class)=true)). % 40.58/27.62 tff(c_188, plain, (iext(uri_owl_propertyChainAxiom, uri_ex_hasUncle, sK4_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l11)=true)). % 40.58/27.62 tff(c_38, plain, (iext(uri_rdfs_range, uri_rdfs_comment, uri_rdfs_Literal)=true)). % 40.58/27.62 tff(c_14, plain, (iext(uri_rdf_type, uri_rdf_rest, uri_rdf_Property)=true)). % 40.58/27.62 tff(c_20, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdf_Property)=true)). % 40.58/27.62 tff(c_186, plain, (iext(uri_ex_hasFather, uri_ex_alice, uri_ex_dave)=true)). % 40.58/27.62 tff(c_26, plain, (iext(uri_rdf_type, uri_rdf_subject, uri_rdf_Property)=true)). % 40.58/27.62 tff(c_70, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Container)=true)). % 40.58/27.62 tff(c_194, plain, (iext(uri_rdf_rest, sK3_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l22, uri_rdf_nil)=true)). % 40.58/27.62 tff(c_74, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property)=true)). % 40.58/27.62 tff(c_22, plain, (iext(uri_rdf_type, uri_rdf_object, uri_rdf_Property)=true)). % 40.58/27.62 tff(c_204, plain, (iext(uri_rdf_first, sK4_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l11, uri_ex_hasCousin)=true)). % 40.58/27.62 tff(c_196, plain, (iext(uri_rdf_rest, sK4_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l11, sK5_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l12)=true)). % 40.58/27.62 tff(c_16, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdf_Property)=true)). % 40.58/27.62 tff(c_176, plain, (iext(uri_rdfs_range, uri_rdf_type, uri_rdfs_Class)=true)). % 40.58/27.62 tff(c_108, plain, (iext(uri_rdfs_domain, uri_rdfs_domain, uri_rdf_Property)=true)). % 40.58/27.63 tff(c_92, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdfs_ContainerMembershipProperty)=true)). % 40.58/27.63 tff(c_18, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdf_Property)=true)). % 40.58/27.63 tff(c_40, plain, (iext(uri_rdfs_domain, uri_rdfs_isDefinedBy, uri_rdfs_Resource)=true)). % 40.58/27.63 tff(c_42, plain, (iext(uri_rdfs_range, uri_rdfs_isDefinedBy, uri_rdfs_Resource)=true)). % 40.58/27.63 tff(c_34, plain, (iext(uri_rdf_type, uri_rdf_type, uri_rdf_Property)=true)). % 40.58/27.63 tff(c_98, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Container)=true)). % 40.58/27.63 tff(c_160, plain, (iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 40.58/27.63 tff(c_62, plain, (iext(uri_rdfs_range, uri_rdf_first, uri_rdfs_Resource)=true)). % 40.58/27.63 tff(c_52, plain, (iext(uri_rdfs_range, uri_rdfs_seeAlso, uri_rdfs_Resource)=true)). % 40.58/27.63 tff(c_68, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Container)=true)). % 40.58/27.63 tff(c_46, plain, (iext(uri_rdfs_domain, uri_rdfs_label, uri_rdfs_Resource)=true)). % 40.58/27.63 tff(c_144, plain, (iext(uri_rdfs_range, uri_rdf_subject, uri_rdfs_Resource)=true)). % 40.58/27.63 tff(c_102, plain, (iext(uri_rdf_type, uri_rdf_XMLLiteral, uri_rdfs_Datatype)=true)). % 40.58/27.63 tff(c_210, plain, (iext(uri_ex_hasCousin, uri_ex_alice, uri_ex_bob)=true)). % 40.58/27.63 tff(c_142, plain, (iext(uri_rdfs_domain, uri_rdf_subject, uri_rdfs_Statement)=true)). % 40.58/27.63 tff(c_50, plain, (iext(uri_rdfs_domain, uri_rdfs_seeAlso, uri_rdfs_Resource)=true)). % 40.58/27.63 tff(c_80, plain, (iext(uri_rdfs_domain, uri_rdf__1, uri_rdfs_Resource)=true)). % 40.58/27.63 tff(c_200, plain, (iext(uri_rdf_first, sK2_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l21, uri_ex_hasUncle)=true)). % 40.58/27.63 tff(c_12, plain, (iext(uri_rdf_type, uri_rdf_nil, uri_rdf_List)=true)). % 40.58/27.63 tff(c_128, plain, (iext(uri_rdfs_domain, uri_rdfs_range, uri_rdf_Property)=true)). % 40.58/27.63 tff(c_10, plain, (iext(uri_rdf_type, uri_rdf_first, uri_rdf_Property)=true)). % 40.58/27.63 tff(c_168, plain, (iext(uri_rdfs_range, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 40.58/27.63 tff(c_134, plain, (iext(uri_rdfs_domain, uri_rdf_object, uri_rdfs_Statement)=true)). % 40.58/27.63 tff(c_202, plain, (iext(uri_rdf_first, sK3_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l22, sK1_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l3)=true)). % 40.58/27.63 tff(c_192, plain, (iext(uri_rdf_rest, sK2_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l21, sK3_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l22)=true)). % 40.58/27.63 tff(c_86, plain, (iext(uri_rdfs_range, uri_rdf__1, uri_rdfs_Resource)=true)). % 40.58/27.63 tff(c_190, plain, (iext(uri_owl_propertyChainAxiom, uri_ex_hasCousin, sK2_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l21)=true)). % 40.58/27.63 tff(c_126, plain, (iext(uri_rdf_type, uri_rdf_Property, uri_rdfs_Class)=true)). % 40.58/27.63 tff(c_140, plain, (iext(uri_rdfs_range, uri_rdf_predicate, uri_rdfs_Resource)=true)). % 40.58/27.63 tff(c_44, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso)=true)). % 40.58/27.63 tff(c_178, plain, (iext(uri_rdfs_domain, uri_rdf_value, uri_rdfs_Resource)=true)). % 40.58/27.63 tff(c_64, plain, (iext(uri_rdfs_domain, uri_rdf_rest, uri_rdf_List)=true)). % 40.58/27.63 tff(c_66, plain, (iext(uri_rdfs_range, uri_rdf_rest, uri_rdf_List)=true)). % 40.58/27.63 tff(c_36, plain, (iext(uri_rdfs_domain, uri_rdfs_comment, uri_rdfs_Resource)=true)). % 40.58/27.63 tff(c_60, plain, (iext(uri_rdfs_domain, uri_rdf_first, uri_rdf_List)=true)). % 40.58/27.63 tff(c_90, plain, (iext(uri_rdfs_range, uri_rdf__3, uri_rdfs_Resource)=true)). % 40.58/27.63 tff(c_100, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Literal)=true)). % 40.58/27.63 tff(c_94, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdfs_ContainerMembershipProperty)=true)). % 40.58/27.63 tff(c_106, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Class)=true)). % 40.58/27.63 tff(c_154, plain, (iext(uri_rdfs_range, uri_rdfs_subClassOf, uri_rdfs_Class)=true)). % 40.58/27.63 tff(c_24, plain, (iext(uri_rdf_type, uri_rdf_value, uri_rdf_Property)=true)). % 40.58/27.63 tff(c_174, plain, (iext(uri_rdfs_domain, uri_rdf_type, uri_rdfs_Resource)=true)). % 40.58/27.63 tff(c_112, plain, (iext(uri_rdfs_range, uri_rdfs_domain, uri_rdfs_Class)=true)). % 40.58/27.63 tff(c_180, plain, (iext(uri_rdfs_range, uri_rdf_value, uri_rdfs_Resource)=true)). % 40.58/27.63 tff(c_78, plain, (iext(uri_rdfs_range, uri_rdfs_member, uri_rdfs_Resource)=true)). % 40.58/27.63 tff(c_88, plain, (iext(uri_rdfs_range, uri_rdf__2, uri_rdfs_Resource)=true)). % 40.58/27.63 tff(c_96, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdfs_ContainerMembershipProperty)=true)). % 40.58/27.63 tff(c_132, plain, (iext(uri_rdfs_range, uri_rdfs_range, uri_rdfs_Class)=true)). % 40.58/27.63 tff(c_48, plain, (iext(uri_rdfs_range, uri_rdfs_label, uri_rdfs_Literal)=true)). % 40.58/27.63 tff(c_184, plain, (iext(uri_ex_hasFather, uri_ex_bob, uri_ex_charly)=true)). % 40.58/27.63 tff(c_82, plain, (iext(uri_rdfs_domain, uri_rdf__2, uri_rdfs_Resource)=true)). % 40.58/27.63 tff(c_84, plain, (iext(uri_rdfs_domain, uri_rdf__3, uri_rdfs_Resource)=true)). % 40.58/27.63 tff(c_182, plain, (iext(uri_owl_inverseOf, sK1_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l3, uri_ex_hasFather)=true)). % 40.58/27.63 tff(c_198, plain, (iext(uri_rdf_rest, sK5_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l12, uri_rdf_nil)=true)). % 40.58/27.63 tff(c_206, plain, (iext(uri_rdf_first, sK5_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties_BNODE_l12, uri_ex_hasFather)=true)). % 40.58/27.63 tff(c_6, plain, (![X_7]: (ir(X_7)=true))). % 40.58/27.63 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 40.58/27.63 %------------------------------------------------------------------------------