%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SWB020-10 : TPTP v9.0.0. Released v7.3.0. % Transfm : none % Format : tptp:raw % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n004.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Apr 9 09:15:53 PM UTC 2025 % Result : Satisfiable 53.00s 39.82s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : SWB020-10 : TPTP v9.0.0. Released v7.3.0. % 0.12/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.13/0.34 % Computer : n004.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Wed Apr 9 00:59:22 EDT 2025 % 0.13/0.34 % CPUTime : % 52.97/39.82 % 53.00/39.82 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 53.00/39.82 % 53.00/39.82 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 53.00/39.85 %$ ifeq > iext > icext > #nlpp > lv > ir > ip > ic > uri_rdfs_subPropertyOf > uri_rdfs_subClassOf > uri_rdfs_seeAlso > uri_rdfs_range > uri_rdfs_member > uri_rdfs_label > uri_rdfs_isDefinedBy > uri_rdfs_domain > uri_rdfs_comment > uri_rdfs_Statement > uri_rdfs_Seq > uri_rdfs_Resource > uri_rdfs_Literal > uri_rdfs_Datatype > uri_rdfs_ContainerMembershipProperty > uri_rdfs_Container > uri_rdfs_Class > uri_rdf_value > uri_rdf_type > uri_rdf_subject > uri_rdf_rest > uri_rdf_predicate > uri_rdf_object > uri_rdf_nil > uri_rdf_first > uri_rdf__3 > uri_rdf__2 > uri_rdf__1 > uri_rdf_XMLLiteral > uri_rdf_Property > uri_rdf_List > uri_rdf_Bag > uri_rdf_Alt > uri_owl_unionOf > uri_owl_intersectionOf > uri_owl_disjointWith > uri_owl_complementOf > uri_ex_d > uri_ex_c3 > uri_ex_c2 > uri_ex_c1 > uri_ex_c > true > sK7_testcase_premise_fullish_020_Logical_Complications_BNODE_li1 > sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs > sK5_testcase_premise_fullish_020_Logical_Complications_BNODE_li2 > sK4_testcase_premise_fullish_020_Logical_Complications_BNODE_xc > sK3_testcase_premise_fullish_020_Logical_Complications_BNODE_lu2 > sK2_testcase_premise_fullish_020_Logical_Complications_BNODE_lu1 > sK1_testcase_premise_fullish_020_Logical_Complications_BNODE_lu3 % 53.00/39.85 % 53.00/39.85 %Foreground sorts: % 53.00/39.85 % 53.00/39.85 % 53.00/39.85 %Background operators: % 53.00/39.85 % 53.00/39.85 % 53.00/39.85 %Foreground operators: % 53.00/39.85 tff(sK5_testcase_premise_fullish_020_Logical_Complications_BNODE_li2, type, sK5_testcase_premise_fullish_020_Logical_Complications_BNODE_li2: $i). % 53.00/39.85 tff(uri_rdfs_Datatype, type, uri_rdfs_Datatype: $i). % 53.00/39.85 tff(uri_owl_complementOf, type, uri_owl_complementOf: $i). % 53.00/39.85 tff(uri_rdfs_ContainerMembershipProperty, type, uri_rdfs_ContainerMembershipProperty: $i). % 53.00/39.85 tff(uri_rdfs_Resource, type, uri_rdfs_Resource: $i). % 53.00/39.85 tff(uri_rdf_Property, type, uri_rdf_Property: $i). % 53.00/39.85 tff(uri_rdf_subject, type, uri_rdf_subject: $i). % 53.00/39.85 tff(uri_rdf_type, type, uri_rdf_type: $i). % 53.00/39.85 tff(sK3_testcase_premise_fullish_020_Logical_Complications_BNODE_lu2, type, sK3_testcase_premise_fullish_020_Logical_Complications_BNODE_lu2: $i). % 53.00/39.85 tff(uri_rdfs_subPropertyOf, type, uri_rdfs_subPropertyOf: $i). % 53.00/39.85 tff(uri_rdfs_seeAlso, type, uri_rdfs_seeAlso: $i). % 53.00/39.85 tff(icext, type, icext: ($i * $i) > $i). % 53.00/39.85 tff(uri_rdfs_range, type, uri_rdfs_range: $i). % 53.00/39.85 tff(uri_rdf_XMLLiteral, type, uri_rdf_XMLLiteral: $i). % 53.00/39.85 tff(uri_rdf_List, type, uri_rdf_List: $i). % 53.00/39.85 tff(uri_rdf_first, type, uri_rdf_first: $i). % 53.00/39.85 tff(uri_rdf_predicate, type, uri_rdf_predicate: $i). % 53.00/39.85 tff(uri_owl_intersectionOf, type, uri_owl_intersectionOf: $i). % 53.00/39.85 tff(uri_ex_c2, type, uri_ex_c2: $i). % 53.00/39.85 tff(ir, type, ir: $i > $i). % 53.00/39.85 tff(lv, type, lv: $i > $i). % 53.00/39.85 tff(uri_ex_c, type, uri_ex_c: $i). % 53.00/39.85 tff(sK2_testcase_premise_fullish_020_Logical_Complications_BNODE_lu1, type, sK2_testcase_premise_fullish_020_Logical_Complications_BNODE_lu1: $i). % 53.00/39.85 tff(uri_rdf__3, type, uri_rdf__3: $i). % 53.00/39.85 tff(uri_ex_c3, type, uri_ex_c3: $i). % 53.00/39.85 tff(uri_rdf_value, type, uri_rdf_value: $i). % 53.00/39.85 tff(sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs, type, sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs: $i). % 53.00/39.85 tff(sK7_testcase_premise_fullish_020_Logical_Complications_BNODE_li1, type, sK7_testcase_premise_fullish_020_Logical_Complications_BNODE_li1: $i). % 53.00/39.85 tff(ic, type, ic: $i > $i). % 53.00/39.85 tff(uri_rdfs_Statement, type, uri_rdfs_Statement: $i). % 53.00/39.85 tff(uri_owl_disjointWith, type, uri_owl_disjointWith: $i). % 53.00/39.85 tff(uri_rdf__1, type, uri_rdf__1: $i). % 53.00/39.85 tff(iext, type, iext: ($i * $i * $i) > $i). % 53.00/39.85 tff(uri_owl_unionOf, type, uri_owl_unionOf: $i). % 53.00/39.85 tff(uri_rdf_rest, type, uri_rdf_rest: $i). % 53.00/39.85 tff(uri_rdfs_label, type, uri_rdfs_label: $i). % 53.00/39.85 tff(uri_rdfs_Container, type, uri_rdfs_Container: $i). % 53.00/39.85 tff(uri_rdfs_subClassOf, type, uri_rdfs_subClassOf: $i). % 53.00/39.85 tff(uri_rdf_object, type, uri_rdf_object: $i). % 53.00/39.85 tff(ip, type, ip: $i > $i). % 53.00/39.85 tff(uri_rdfs_Class, type, uri_rdfs_Class: $i). % 53.00/39.85 tff(uri_rdfs_Seq, type, uri_rdfs_Seq: $i). % 53.00/39.85 tff(sK4_testcase_premise_fullish_020_Logical_Complications_BNODE_xc, type, sK4_testcase_premise_fullish_020_Logical_Complications_BNODE_xc: $i). % 53.00/39.85 tff(uri_ex_c1, type, uri_ex_c1: $i). % 53.00/39.85 tff(uri_rdfs_member, type, uri_rdfs_member: $i). % 53.00/39.85 tff(uri_rdf_Bag, type, uri_rdf_Bag: $i). % 53.00/39.85 tff(uri_rdf__2, type, uri_rdf__2: $i). % 53.00/39.85 tff(sK1_testcase_premise_fullish_020_Logical_Complications_BNODE_lu3, type, sK1_testcase_premise_fullish_020_Logical_Complications_BNODE_lu3: $i). % 53.00/39.85 tff(uri_rdfs_comment, type, uri_rdfs_comment: $i). % 53.00/39.85 tff(uri_rdfs_Literal, type, uri_rdfs_Literal: $i). % 53.00/39.85 tff(true, type, true: $i). % 53.00/39.85 tff(uri_rdf_Alt, type, uri_rdf_Alt: $i). % 53.00/39.85 tff(uri_rdf_nil, type, uri_rdf_nil: $i). % 53.00/39.85 tff(uri_ex_d, type, uri_ex_d: $i). % 53.00/39.85 tff(uri_rdfs_isDefinedBy, type, uri_rdfs_isDefinedBy: $i). % 53.00/39.85 tff(uri_rdfs_domain, type, uri_rdfs_domain: $i). % 53.00/39.85 tff(ifeq, type, ifeq: ($i * $i * $i * $i) > $i). % 53.00/39.85 % 53.00/39.85 %Saturated clause set: % 53.00/39.86 tff(c_14580, 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))). % 53.00/39.86 tff(c_85016, plain, (![X_1368, Y_1369]: (ifeq(iext(uri_rdf_predicate, X_1368, Y_1369), true, iext(uri_rdf_predicate, X_1368, Y_1369), true)=true))). % 53.00/39.86 tff(c_15772, 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))). % 53.00/39.86 tff(c_17164, 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))). % 53.00/39.86 tff(c_14517, 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))). % 53.00/39.86 tff(c_84596, plain, (![X_1361, Y_1362]: (ifeq(iext(uri_rdfs_label, X_1361, Y_1362), true, iext(uri_rdfs_label, X_1361, Y_1362), true)=true))). % 53.00/39.86 tff(c_84569, plain, (![X_1357, Y_1358]: (ifeq(iext(uri_rdfs_comment, X_1357, Y_1358), true, iext(uri_rdfs_comment, X_1357, Y_1358), true)=true))). % 53.00/39.86 tff(c_5661, 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))). % 53.00/39.86 tff(c_5658, 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))). % 53.00/39.86 tff(c_83989, plain, (![X_1348, Y_1349]: (ifeq(iext(uri_rdfs_member, X_1348, Y_1349), true, iext(uri_rdfs_member, X_1348, Y_1349), true)=true))). % 53.00/39.86 tff(c_14129, 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))). % 53.00/39.86 tff(c_14447, 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))). % 53.00/39.86 tff(c_13906, 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))). % 53.00/39.86 tff(c_13671, 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))). % 53.00/39.86 tff(c_83434, plain, (![C_1343]: (ifeq(iext(uri_rdfs_subClassOf, C_1343, uri_rdfs_Statement), true, iext(uri_rdfs_subClassOf, C_1343, uri_rdfs_Resource), true)=true))). % 53.00/39.86 tff(c_13817, 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))). % 53.00/39.86 tff(c_13972, 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))). % 53.00/39.86 tff(c_83012, plain, (![C_1339]: (ifeq(iext(uri_rdfs_subClassOf, C_1339, uri_rdf_List), true, iext(uri_rdfs_subClassOf, C_1339, uri_rdfs_Resource), true)=true))). % 53.00/39.86 tff(c_12956, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_ex_d, uri_rdfs_Class), true, true, true), true)=true))). % 53.00/39.86 tff(c_10846, 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))). % 53.00/39.86 tff(c_13244, 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))). % 53.00/39.86 tff(c_13195, 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))). % 53.00/39.86 tff(c_11075, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_owl_unionOf, Y_21), true, true, true), true)=true))). % 53.00/39.86 tff(c_11973, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_owl_complementOf, Y_21), true, true, true), true)=true))). % 53.00/39.86 tff(c_13545, 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))). % 53.00/39.86 tff(c_13075, 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))). % 53.00/39.86 tff(c_9801, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_owl_intersectionOf), true, true, true), true)=true))). % 53.00/39.86 tff(c_8296, 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))). % 53.00/39.87 tff(c_11970, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_owl_complementOf), true, true, true), true)=true))). % 53.00/39.87 tff(c_13122, 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))). % 53.00/39.87 tff(c_6103, 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))). % 53.00/39.87 tff(c_11072, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_owl_unionOf), true, true, true), true)=true))). % 53.00/39.87 tff(c_8299, 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))). % 53.00/39.87 tff(c_7784, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_owl_disjointWith), true, true, true), true)=true))). % 53.00/39.87 tff(c_7787, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_owl_disjointWith, Y_21), true, true, true), true)=true))). % 53.00/39.87 tff(c_13592, 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))). % 53.00/39.87 tff(c_9804, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_owl_intersectionOf, Y_21), true, true, true), true)=true))). % 53.00/39.87 tff(c_6106, 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))). % 53.00/39.87 tff(c_11736, 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))). % 53.00/39.87 tff(c_12792, 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))). % 53.00/39.87 tff(c_12861, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs, uri_rdfs_Class), true, true, true), true)=true))). % 53.00/39.87 tff(c_13028, 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))). % 53.00/39.87 tff(c_10849, 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))). % 53.00/39.87 tff(c_11739, 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))). % 53.00/39.87 tff(c_12909, 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))). % 53.00/39.87 tff(c_13356, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, sK2_testcase_premise_fullish_020_Logical_Complications_BNODE_lu1, uri_rdf_List), true, true, true), true)=true))). % 53.00/39.87 tff(c_12219, 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))). % 53.00/39.87 tff(c_17041, 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))). % 53.00/39.87 tff(c_12334, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, sK5_testcase_premise_fullish_020_Logical_Complications_BNODE_li2, uri_rdf_List), true, true, true), true)=true))). % 53.00/39.87 tff(c_16313, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, sK7_testcase_premise_fullish_020_Logical_Complications_BNODE_li1, uri_rdf_List), true, true, true), true)=true))). % 53.00/39.87 tff(c_15548, 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))). % 53.00/39.87 tff(c_14369, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, sK1_testcase_premise_fullish_020_Logical_Complications_BNODE_lu3, uri_rdf_List), true, true, true), true)=true))). % 53.00/39.87 tff(c_12615, 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))). % 53.00/39.87 tff(c_12717, 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))). % 53.00/39.87 tff(c_12662, 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))). % 53.00/39.87 tff(c_7638, 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))). % 53.00/39.87 tff(c_77531, plain, (![P_1281]: (ifeq(iext(uri_rdfs_subPropertyOf, P_1281, uri_rdf__3), true, iext(uri_rdfs_subPropertyOf, P_1281, uri_rdfs_member), true)=true))). % 53.00/39.87 tff(c_77178, plain, (![X_1279, Y_1280]: (ifeq(iext(uri_rdfs_subPropertyOf, X_1279, Y_1280), true, iext(uri_rdfs_subPropertyOf, X_1279, Y_1280), true)=true))). % 53.00/39.87 tff(c_4670, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, uri_ex_d), true, true, true), true)=true))). % 53.00/39.87 tff(c_76321, plain, (![X_1273, Y_1274]: (ifeq(iext(uri_rdfs_subClassOf, X_1273, Y_1274), true, iext(uri_rdfs_subClassOf, X_1273, Y_1274), true)=true))). % 53.00/39.87 tff(c_2699, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_subPropertyOf), true, ifeq(iext(P_105, uri_rdfs_isDefinedBy, uri_rdfs_isDefinedBy), true, true, true), true)=true))). % 53.00/39.87 tff(c_4885, 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))). % 53.00/39.87 tff(c_6822, 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))). % 53.00/39.87 tff(c_74711, plain, (![C_1260]: (ifeq(iext(uri_rdfs_subClassOf, C_1260, uri_rdfs_Class), true, iext(uri_rdfs_subClassOf, C_1260, uri_rdfs_Resource), true)=true))). % 53.00/39.87 tff(c_7883, 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))). % 53.00/39.87 tff(c_5360, 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))). % 53.00/39.88 tff(c_74538, plain, (![X_1255, Y_1256]: (ifeq(iext(uri_owl_complementOf, X_1255, Y_1256), true, iext(uri_owl_complementOf, X_1255, Y_1256), true)=true))). % 53.00/39.88 tff(c_5041, 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))). % 53.00/39.88 tff(c_11331, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_owl_unionOf, uri_owl_unionOf), true, true, true), true)=true))). % 53.00/39.88 tff(c_4830, 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))). % 53.00/39.88 tff(c_9585, 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))). % 53.00/39.88 tff(c_11891, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_owl_complementOf, uri_rdf_Property), true, true, true), true)=true))). % 53.00/39.88 tff(c_4575, 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))). % 53.00/39.88 tff(c_11657, 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))). % 53.00/39.88 tff(c_10327, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs, uri_rdfs_Resource), true, true, true), true)=true))). % 53.00/39.88 tff(c_7292, 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))). % 53.00/39.88 tff(c_9110, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_ex_d, uri_rdfs_Resource), true, true, true), true)=true))). % 53.00/39.88 tff(c_4932, 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))). % 53.00/39.88 tff(c_8814, 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))). % 53.00/39.88 tff(c_8162, 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))). % 53.00/39.88 tff(c_4784, 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))). % 53.00/39.88 tff(c_9369, 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))). % 53.00/39.88 tff(c_5475, 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))). % 53.00/39.88 tff(c_70913, plain, (![C_1224]: (ifeq(iext(uri_rdfs_subClassOf, C_1224, uri_rdfs_Datatype), true, iext(uri_rdfs_subClassOf, C_1224, uri_rdfs_Resource), true)=true))). % 53.00/39.88 tff(c_4833, 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))). % 53.00/39.88 tff(c_11408, 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))). % 53.00/39.88 tff(c_70477, plain, (![C_1219]: (ifeq(iext(uri_rdfs_subClassOf, C_1219, sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs), true, iext(uri_rdfs_subClassOf, C_1219, uri_rdfs_Resource), true)=true))). % 53.00/39.88 tff(c_70450, plain, (![X_1215, Y_1216]: (ifeq(iext(uri_rdf_object, X_1215, Y_1216), true, iext(uri_rdf_object, X_1215, Y_1216), true)=true))). % 53.00/39.88 tff(c_6045, 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))). % 53.00/39.88 tff(c_4618, 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))). % 53.00/39.88 tff(c_9648, 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))). % 53.00/39.88 tff(c_69276, plain, (![X_1203, Y_1204]: (ifeq(iext(uri_rdf_rest, X_1203, Y_1204), true, iext(uri_rdf_rest, X_1203, Y_1204), true)=true))). % 53.00/39.88 tff(c_68967, plain, (![P_1199]: (ifeq(iext(uri_rdfs_subPropertyOf, P_1199, uri_rdf__1), true, iext(uri_rdfs_subPropertyOf, P_1199, uri_rdfs_member), true)=true))). % 53.00/39.88 tff(c_10416, 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))). % 53.00/39.88 tff(c_10544, 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))). % 53.00/39.88 tff(c_68372, plain, (![X_1193, Y_1194]: (ifeq(iext(uri_rdfs_domain, X_1193, Y_1194), true, iext(uri_rdfs_domain, X_1193, Y_1194), true)=true))). % 53.00/39.88 tff(c_11265, 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))). % 53.00/39.88 tff(c_15058, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, sK3_testcase_premise_fullish_020_Logical_Complications_BNODE_lu2, uri_rdf_List), true, true, true), true)=true))). % 53.00/39.88 tff(c_67957, plain, (![C_1189]: (ifeq(iext(uri_rdfs_subClassOf, C_1189, uri_rdf_Bag), true, iext(uri_rdfs_subClassOf, C_1189, uri_rdfs_Resource), true)=true))). % 53.00/39.88 tff(c_67930, plain, (![X_1185, Y_1186]: (ifeq(iext(uri_rdf_value, X_1185, Y_1186), true, iext(uri_rdf_value, X_1185, Y_1186), true)=true))). % 53.00/39.88 tff(c_4621, 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))). % 53.00/39.88 tff(c_10474, 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))). % 53.00/39.88 tff(c_4578, 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))). % 53.00/39.88 tff(c_10192, 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))). % 53.00/39.88 tff(c_6170, 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))). % 53.00/39.88 tff(c_66747, plain, (![C_1174]: (ifeq(iext(uri_rdfs_subClassOf, C_1174, uri_rdfs_Literal), true, iext(uri_rdfs_subClassOf, C_1174, uri_rdfs_Resource), true)=true))). % 53.00/39.88 tff(c_5731, 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))). % 53.00/39.88 tff(c_8000, 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))). % 53.00/39.88 tff(c_66460, plain, (![X_1168, Y_1169]: (ifeq(iext(uri_rdfs_seeAlso, X_1168, Y_1169), true, iext(uri_rdfs_seeAlso, X_1168, Y_1169), true)=true))). % 53.00/39.88 tff(c_6478, 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))). % 53.00/39.88 tff(c_7572, 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))). % 53.00/39.88 tff(c_6924, 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))). % 53.00/39.88 tff(c_7411, 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))). % 53.00/39.88 tff(c_5949, 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))). % 53.00/39.88 tff(c_9721, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_owl_intersectionOf, uri_rdf_Property), true, true, true), true)=true))). % 53.00/39.88 tff(c_8520, 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))). % 53.00/39.88 tff(c_4535, 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))). % 53.00/39.88 tff(c_64242, 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))). % 53.00/39.88 tff(c_5879, 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))). % 53.00/39.89 tff(c_63820, plain, (![C_1146]: (ifeq(iext(uri_rdfs_subClassOf, C_1146, uri_rdfs_Container), true, iext(uri_rdfs_subClassOf, C_1146, uri_rdfs_Resource), true)=true))). % 53.00/39.89 tff(c_4977, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs, Y_21), true, true, true), true)=true))). % 53.00/39.89 tff(c_8063, 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))). % 53.00/39.89 tff(c_63284, plain, (![X_1137, Y_1138]: (ifeq(iext(uri_rdf__3, X_1137, Y_1138), true, iext(uri_rdfs_member, X_1137, Y_1138), true)=true))). % 53.00/39.89 tff(c_11017, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_owl_unionOf, uri_rdf_Property), true, true, true), true)=true))). % 53.00/39.89 tff(c_9940, 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))). % 53.00/39.89 tff(c_4929, 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))). % 53.00/39.89 tff(c_62770, plain, (![X_1129, Y_1130]: (ifeq(iext(uri_rdf_first, X_1129, Y_1130), true, iext(uri_rdf_first, X_1129, Y_1130), true)=true))). % 53.00/39.89 tff(c_5791, 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))). % 53.00/39.89 tff(c_6606, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs, sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs), true, true, true), true)=true))). % 53.00/39.89 tff(c_4726, 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))). % 53.00/39.89 tff(c_61865, plain, (![X_1117, Y_1118]: (ifeq(iext(uri_owl_disjointWith, X_1117, Y_1118), true, iext(uri_owl_disjointWith, X_1117, Y_1118), true)=true))). % 53.00/39.89 tff(c_11474, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_owl_intersectionOf, uri_owl_intersectionOf), true, true, true), true)=true))). % 53.00/39.89 tff(c_61707, plain, (![X_1112, Y_1113]: (ifeq(iext(uri_rdfs_isDefinedBy, X_1112, Y_1113), true, iext(uri_rdfs_isDefinedBy, X_1112, Y_1113), true)=true))). % 53.00/39.89 tff(c_10637, 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))). % 53.00/39.89 tff(c_60933, plain, (![X_1105, Y_1106]: (ifeq(iext(uri_rdfs_range, X_1105, Y_1106), true, iext(uri_rdfs_range, X_1105, Y_1106), true)=true))). % 53.00/39.89 tff(c_60100, plain, (![X_1099, Y_1100]: (ifeq(iext(uri_rdf_type, X_1099, Y_1100), true, iext(uri_rdf_type, X_1099, Y_1100), true)=true))). % 53.00/39.89 tff(c_60079, plain, (![X_1097, Y_1098]: (ifeq(iext(uri_owl_intersectionOf, X_1097, Y_1098), true, iext(uri_owl_intersectionOf, X_1097, Y_1098), true)=true))). % 53.00/39.89 tff(c_8746, 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))). % 53.00/39.89 tff(c_59786, plain, (![C_1094]: (ifeq(iext(uri_rdfs_subClassOf, C_1094, uri_rdf_Property), true, iext(uri_rdfs_subClassOf, C_1094, uri_rdfs_Resource), true)=true))). % 53.00/39.89 tff(c_59759, plain, (![X_1090, Y_1091]: (ifeq(iext(uri_rdf__3, X_1090, Y_1091), true, iext(uri_rdf__3, X_1090, Y_1091), true)=true))). % 53.00/39.89 tff(c_4787, 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))). % 53.00/39.89 tff(c_4723, 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))). % 53.00/39.89 tff(c_10768, 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))). % 53.00/39.89 tff(c_58971, plain, (![X_1079, Y_1080]: (ifeq(iext(uri_owl_unionOf, X_1079, Y_1080), true, iext(uri_owl_unionOf, X_1079, Y_1080), true)=true))). % 53.00/39.89 tff(c_58817, plain, (![C_1077]: (ifeq(iext(uri_rdfs_subClassOf, C_1077, uri_ex_d), true, iext(uri_rdfs_subClassOf, C_1077, uri_rdfs_Resource), true)=true))). % 53.00/39.89 tff(c_58240, plain, (![X_1069, Y_1070]: (ifeq(iext(uri_rdf__1, X_1069, Y_1070), true, iext(uri_rdfs_member, X_1069, Y_1070), true)=true))). % 53.00/39.89 tff(c_7711, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_owl_disjointWith, uri_rdf_Property), true, true, true), true)=true))). % 53.00/39.89 tff(c_6279, 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))). % 53.00/39.89 tff(c_8647, 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))). % 53.00/39.89 tff(c_57813, plain, (![X_1062, Y_1063]: (ifeq(iext(uri_rdf__1, X_1062, Y_1063), true, iext(uri_rdf__1, X_1062, Y_1063), true)=true))). % 53.00/39.89 tff(c_4882, 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))). % 53.00/39.89 tff(c_7197, 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))). % 53.00/39.89 tff(c_7107, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_owl_disjointWith, uri_owl_disjointWith), true, true, true), true)=true))). % 53.00/39.89 tff(c_9172, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_ex_d, uri_ex_d), true, true, true), true)=true))). % 53.00/39.89 tff(c_7507, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_owl_complementOf, uri_owl_complementOf), true, true, true), true)=true))). % 53.00/39.89 tff(c_9310, 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))). % 53.00/39.89 tff(c_55785, plain, (![C_1045]: (ifeq(iext(uri_rdfs_subClassOf, C_1045, uri_rdf_Alt), true, iext(uri_rdfs_subClassOf, C_1045, uri_rdfs_Resource), true)=true))). % 53.00/39.89 tff(c_4974, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs), true, true, true), true)=true))). % 53.00/39.89 tff(c_55160, plain, (![C_1039]: (ifeq(iext(uri_rdfs_subClassOf, C_1039, uri_rdfs_Seq), true, iext(uri_rdfs_subClassOf, C_1039, uri_rdfs_Resource), true)=true))). % 53.00/39.89 tff(c_54986, plain, (![X_1033, Y_1034]: (ifeq(iext(uri_rdf__2, X_1033, Y_1034), true, iext(uri_rdfs_member, X_1033, Y_1034), true)=true))). % 53.00/39.89 tff(c_5044, 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))). % 53.00/39.89 tff(c_8224, 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))). % 53.00/39.89 tff(c_54322, plain, (![P_1026]: (ifeq(iext(uri_rdfs_subPropertyOf, P_1026, uri_rdf__2), true, iext(uri_rdfs_subPropertyOf, P_1026, uri_rdfs_member), true)=true))). % 53.00/39.89 tff(c_4532, 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))). % 53.00/39.89 tff(c_7018, 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))). % 53.00/39.89 tff(c_53708, plain, (![C_1021]: (ifeq(iext(uri_rdfs_subClassOf, C_1021, uri_rdfs_ContainerMembershipProperty), true, iext(uri_rdfs_subClassOf, C_1021, uri_rdfs_Resource), true)=true))). % 53.00/39.89 tff(c_8977, 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))). % 53.00/39.89 tff(c_12127, 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))). % 53.00/39.89 tff(c_4673, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, uri_ex_d, Y_21), true, true, true), true)=true))). % 53.00/39.89 tff(c_53269, plain, (![X_1013, Y_1014]: (ifeq(iext(uri_rdf__2, X_1013, Y_1014), true, iext(uri_rdf__2, X_1013, Y_1014), true)=true))). % 53.00/39.89 tff(c_53242, plain, (![X_1009, Y_1010]: (ifeq(iext(uri_rdf_subject, X_1009, Y_1010), true, iext(uri_rdf_subject, X_1009, Y_1010), true)=true))). % 53.00/39.89 tff(c_6696, 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))). % 53.00/39.89 tff(c_8461, 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))). % 53.00/39.89 tff(c_13312, 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_020_Logical_Complications_BNODE_lu1), true, true, true), true)=true))). % 53.00/39.89 tff(c_16142, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_List), true, ifeq(iext(P_18, sK7_testcase_premise_fullish_020_Logical_Complications_BNODE_li1, Y_21), true, true, true), true)=true))). % 53.00/39.89 tff(c_14199, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_List), true, ifeq(iext(P_28, X_30, sK1_testcase_premise_fullish_020_Logical_Complications_BNODE_lu3), true, true, true), true)=true))). % 53.00/39.89 tff(c_6426, 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))). % 53.00/39.89 tff(c_16865, 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))). % 53.00/39.89 tff(c_6423, 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))). % 53.00/39.89 tff(c_6693, 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))). % 53.00/39.89 tff(c_10028, 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))). % 53.00/39.89 tff(c_10031, 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))). % 53.00/39.90 tff(c_7834, 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))). % 53.00/39.90 tff(c_8458, 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))). % 53.00/39.90 tff(c_13315, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_List), true, ifeq(iext(P_18, sK2_testcase_premise_fullish_020_Logical_Complications_BNODE_lu1, Y_21), true, true, true), true)=true))). % 53.00/39.90 tff(c_8341, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_List), true, ifeq(iext(P_18, sK5_testcase_premise_fullish_020_Logical_Complications_BNODE_li2, Y_21), true, true, true), true)=true))). % 53.00/39.90 tff(c_12387, 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))). % 53.00/39.90 tff(c_15504, 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))). % 53.00/39.90 tff(c_15501, 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))). % 53.00/39.90 tff(c_5147, plain, (![P_47, X_132]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, X_132, uri_rdfs_Resource), true, true, true), true)=true))). % 53.00/39.90 tff(c_7831, 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))). % 53.00/39.90 tff(c_16868, 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))). % 53.00/39.90 tff(c_16139, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_List), true, ifeq(iext(P_28, X_30, sK7_testcase_premise_fullish_020_Logical_Complications_BNODE_li1), true, true, true), true)=true))). % 53.00/39.90 tff(c_12384, 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))). % 53.00/39.90 tff(c_8338, 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_020_Logical_Complications_BNODE_li2), true, true, true), true)=true))). % 53.00/39.90 tff(c_14202, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_List), true, ifeq(iext(P_18, sK1_testcase_premise_fullish_020_Logical_Complications_BNODE_lu3, Y_21), true, true, true), true)=true))). % 53.00/39.90 tff(c_4055, 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))). % 53.00/39.90 tff(c_4016, 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))). % 53.00/39.90 tff(c_4092, 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))). % 53.00/39.90 tff(c_3970, 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))). % 53.00/39.90 tff(c_4183, 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))). % 53.00/39.90 tff(c_14892, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_List), true, ifeq(iext(P_18, sK3_testcase_premise_fullish_020_Logical_Complications_BNODE_lu2, Y_21), true, true, true), true)=true))). % 53.00/39.90 tff(c_4351, 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))). % 53.00/39.90 tff(c_3892, 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))). % 53.00/39.90 tff(c_4227, 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))). % 53.00/39.90 tff(c_3973, 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))). % 53.00/39.90 tff(c_4304, 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))). % 53.00/39.90 tff(c_4180, 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))). % 53.00/39.90 tff(c_4089, 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))). % 53.00/39.90 tff(c_4427, 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))). % 53.00/39.90 tff(c_4224, 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))). % 53.00/39.90 tff(c_4132, 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))). % 53.00/39.90 tff(c_4430, 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))). % 53.00/39.90 tff(c_4267, 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))). % 53.00/39.90 tff(c_3895, 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))). % 53.00/39.90 tff(c_3929, 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))). % 53.00/39.90 tff(c_3932, 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))). % 53.00/39.90 tff(c_4469, 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))). % 53.00/39.90 tff(c_4388, 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))). % 53.00/39.90 tff(c_14889, 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_020_Logical_Complications_BNODE_lu2), true, true, true), true)=true))). % 53.00/39.90 tff(c_4129, 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))). % 53.00/39.90 tff(c_4270, 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))). % 53.00/39.90 tff(c_4348, 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))). % 53.00/39.90 tff(c_4466, 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))). % 53.00/39.90 tff(c_4013, 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))). % 53.00/39.90 tff(c_4052, 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))). % 53.00/39.90 tff(c_4391, 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))). % 53.00/39.90 tff(c_4307, 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))). % 53.00/39.90 tff(c_1747, plain, (![P_91, X_60, Y_94]: (ifeq(iext(uri_rdfs_domain, P_91, uri_rdfs_Resource), true, ifeq(iext(P_91, X_60, Y_94), true, true, true), true)=true))). % 53.00/39.90 tff(c_2133, plain, (![P_95, X_97, X_60]: (ifeq(iext(uri_rdfs_range, P_95, uri_rdfs_Resource), true, ifeq(iext(P_95, X_97, X_60), true, true, true), true)=true))). % 53.00/39.90 tff(c_2843, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_domain), true, ifeq(iext(P_105, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true, true, true), true)=true))). % 53.00/39.90 tff(c_3044, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_subPropertyOf), true, ifeq(iext(P_105, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso), true, true, true), true)=true))). % 53.00/39.90 tff(c_3074, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdf_rest), true, ifeq(iext(P_105, sK1_testcase_premise_fullish_020_Logical_Complications_BNODE_lu3, uri_rdf_nil), true, true, true), true)=true))). % 53.00/39.90 tff(c_42856, plain, (![C_884]: (ifeq(iext(uri_rdfs_subClassOf, C_884, uri_rdf_XMLLiteral), true, iext(uri_rdfs_subClassOf, C_884, uri_rdfs_Literal), true)=true))). % 53.00/39.90 tff(c_2711, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_range), true, ifeq(iext(P_105, uri_rdf_type, uri_rdfs_Class), true, true, true), true)=true))). % 53.00/39.90 tff(c_2903, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_domain), true, ifeq(iext(P_105, uri_rdf_value, uri_rdfs_Resource), true, true, true), true)=true))). % 53.00/39.90 tff(c_3140, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdf_first), true, ifeq(iext(P_105, sK5_testcase_premise_fullish_020_Logical_Complications_BNODE_li2, sK4_testcase_premise_fullish_020_Logical_Complications_BNODE_xc), true, true, true), true)=true))). % 53.00/39.90 tff(c_2819, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdf_type), true, ifeq(iext(P_105, uri_rdf__2, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 53.00/39.90 tff(c_2747, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_domain), true, ifeq(iext(P_105, uri_rdfs_subClassOf, uri_rdfs_Class), true, true, true), true)=true))). % 53.00/39.90 tff(c_3035, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_owl_disjointWith), true, ifeq(iext(P_105, uri_ex_d, uri_ex_c1), true, true, true), true)=true))). % 53.00/39.90 tff(c_3134, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdf_rest), true, ifeq(iext(P_105, sK7_testcase_premise_fullish_020_Logical_Complications_BNODE_li1, sK5_testcase_premise_fullish_020_Logical_Complications_BNODE_li2), true, true, true), true)=true))). % 53.00/39.90 tff(c_2753, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_subClassOf), true, ifeq(iext(P_105, uri_rdf_Bag, uri_rdfs_Container), true, true, true), true)=true))). % 53.00/39.90 tff(c_3011, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_subClassOf), true, ifeq(iext(P_105, uri_rdf_Alt, uri_rdfs_Container), true, true, true), true)=true))). % 53.00/39.90 tff(c_41622, plain, (![C_873]: (ifeq(iext(uri_rdfs_subClassOf, C_873, uri_ex_d), true, iext(uri_rdfs_subClassOf, C_873, sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs), true)=true))). % 53.00/39.90 tff(c_2801, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdf_type), true, ifeq(iext(P_105, uri_rdf__3, uri_rdf_Property), true, true, true), true)=true))). % 53.00/39.90 tff(c_3068, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdf_rest), true, ifeq(iext(P_105, sK3_testcase_premise_fullish_020_Logical_Complications_BNODE_lu2, sK1_testcase_premise_fullish_020_Logical_Complications_BNODE_lu3), true, true, true), true)=true))). % 53.00/39.90 tff(c_2933, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_range), true, ifeq(iext(P_105, uri_rdf__1, uri_rdfs_Resource), true, true, true), true)=true))). % 53.00/39.90 tff(c_3098, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_subClassOf), true, ifeq(iext(P_105, uri_rdf_XMLLiteral, uri_rdfs_Literal), true, true, true), true)=true))). % 53.00/39.90 tff(c_3023, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_domain), true, ifeq(iext(P_105, uri_rdf_first, uri_rdf_List), true, true, true), true)=true))). % 53.00/39.91 tff(c_3116, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdf_type), true, ifeq(iext(P_105, uri_rdf__3, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 53.00/39.91 tff(c_3110, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_range), true, ifeq(iext(P_105, uri_rdfs_range, uri_rdfs_Class), true, true, true), true)=true))). % 53.00/39.91 tff(c_2969, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_domain), true, ifeq(iext(P_105, uri_rdfs_range, uri_rdf_Property), true, true, true), true)=true))). % 53.00/39.91 tff(c_3092, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_range), true, ifeq(iext(P_105, uri_rdf__2, uri_rdfs_Resource), true, true, true), true)=true))). % 53.00/39.91 tff(c_3128, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_owl_complementOf), true, ifeq(iext(P_105, sK4_testcase_premise_fullish_020_Logical_Complications_BNODE_xc, uri_ex_c2), true, true, true), true)=true))). % 53.00/39.91 tff(c_2909, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_range), true, ifeq(iext(P_105, uri_rdfs_label, uri_rdfs_Literal), true, true, true), true)=true))). % 53.00/39.91 tff(c_40141, plain, (![X_858, Y_859]: (ifeq(iext(uri_rdfs_isDefinedBy, X_858, Y_859), true, iext(uri_rdfs_seeAlso, X_858, Y_859), true)=true))). % 53.00/39.91 tff(c_2855, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_domain), true, ifeq(iext(P_105, uri_rdf_rest, uri_rdf_List), true, true, true), true)=true))). % 53.00/39.91 tff(c_3146, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_subClassOf), true, ifeq(iext(P_105, uri_ex_d, sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs), true, true, true), true)=true))). % 53.00/39.91 tff(c_2963, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_range), true, ifeq(iext(P_105, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true, true, true), true)=true))). % 53.00/39.91 tff(c_2741, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdf_type), true, ifeq(iext(P_105, uri_rdf_rest, uri_rdf_Property), true, true, true), true)=true))). % 53.00/39.91 tff(c_2915, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdf_type), true, ifeq(iext(P_105, uri_rdf_object, uri_rdf_Property), true, true, true), true)=true))). % 53.00/39.91 tff(c_2729, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_range), true, ifeq(iext(P_105, uri_rdfs_subPropertyOf, uri_rdf_Property), true, true, true), true)=true))). % 53.00/39.91 tff(c_2837, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_range), true, ifeq(iext(P_105, uri_rdfs_seeAlso, uri_rdfs_Resource), true, true, true), true)=true))). % 53.00/39.91 tff(c_2891, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdf_rest), true, ifeq(iext(P_105, sK2_testcase_premise_fullish_020_Logical_Complications_BNODE_lu1, sK3_testcase_premise_fullish_020_Logical_Complications_BNODE_lu2), true, true, true), true)=true))). % 53.00/39.91 tff(c_2807, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_domain), true, ifeq(iext(P_105, uri_rdfs_label, uri_rdfs_Resource), true, true, true), true)=true))). % 53.00/39.91 tff(c_2765, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_range), true, ifeq(iext(P_105, uri_rdf_subject, uri_rdfs_Resource), true, true, true), true)=true))). % 53.00/39.91 tff(c_3029, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_range), true, ifeq(iext(P_105, uri_rdfs_subClassOf, uri_rdfs_Class), true, true, true), true)=true))). % 53.00/39.91 tff(c_2987, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_range), true, ifeq(iext(P_105, uri_rdf_rest, uri_rdf_List), true, true, true), true)=true))). % 53.00/39.91 tff(c_38465, plain, (![C_844]: (ifeq(iext(uri_rdfs_subClassOf, C_844, uri_rdf_Bag), true, iext(uri_rdfs_subClassOf, C_844, uri_rdfs_Container), true)=true))). % 53.00/39.91 tff(c_2921, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_domain), true, ifeq(iext(P_105, uri_rdfs_subPropertyOf, uri_rdf_Property), true, true, true), true)=true))). % 53.00/39.91 tff(c_2771, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_domain), true, ifeq(iext(P_105, uri_rdfs_member, uri_rdfs_Resource), true, true, true), true)=true))). % 53.00/39.91 tff(c_38121, plain, (![C_840]: (ifeq(iext(uri_rdfs_subClassOf, C_840, uri_rdfs_Seq), true, iext(uri_rdfs_subClassOf, C_840, uri_rdfs_Container), true)=true))). % 53.00/39.91 tff(c_2717, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdf_first), true, ifeq(iext(P_105, sK3_testcase_premise_fullish_020_Logical_Complications_BNODE_lu2, uri_ex_c2), true, true, true), true)=true))). % 53.00/39.91 tff(c_3062, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdf_type), true, ifeq(iext(P_105, uri_rdf_value, uri_rdf_Property), true, true, true), true)=true))). % 53.00/39.91 tff(c_2813, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_domain), true, ifeq(iext(P_105, uri_rdfs_domain, uri_rdf_Property), true, true, true), true)=true))). % 53.00/39.91 tff(c_37676, plain, (![C_835]: (ifeq(iext(uri_rdfs_subClassOf, C_835, uri_rdfs_Datatype), true, iext(uri_rdfs_subClassOf, C_835, uri_rdfs_Class), true)=true))). % 53.00/39.91 tff(c_2879, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdf_type), true, ifeq(iext(P_105, uri_rdf_nil, uri_rdf_List), true, true, true), true)=true))). % 53.00/39.91 tff(c_37495, plain, (![P_832]: (ifeq(iext(uri_rdfs_subPropertyOf, P_832, uri_rdfs_isDefinedBy), true, iext(uri_rdfs_subPropertyOf, P_832, uri_rdfs_seeAlso), true)=true))). % 53.00/39.91 tff(c_37444, plain, (![C_830]: (ifeq(iext(uri_rdfs_subClassOf, C_830, uri_rdfs_ContainerMembershipProperty), true, iext(uri_rdfs_subClassOf, C_830, uri_rdf_Property), true)=true))). % 53.00/39.91 tff(c_2861, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_subClassOf), true, ifeq(iext(P_105, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property), true, true, true), true)=true))). % 53.00/39.91 tff(c_2939, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_domain), true, ifeq(iext(P_105, uri_rdf__2, uri_rdfs_Resource), true, true, true), true)=true))). % 53.00/39.91 tff(c_2723, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdf_type), true, ifeq(iext(P_105, uri_rdf_subject, uri_rdf_Property), true, true, true), true)=true))). % 53.00/39.91 tff(c_2735, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_range), true, ifeq(iext(P_105, uri_rdf_value, uri_rdfs_Resource), true, true, true), true)=true))). % 53.00/39.91 tff(c_2759, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_range), true, ifeq(iext(P_105, uri_rdfs_domain, uri_rdfs_Class), true, true, true), true)=true))). % 53.00/39.91 tff(c_36708, plain, (![D_823]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_823), true, icext(D_823, uri_rdfs_Resource), true)=true))). % 53.00/39.91 tff(c_36511, plain, (![D_820]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_820), true, icext(D_820, uri_rdfs_seeAlso), true)=true))). % 53.00/39.91 tff(c_2975, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdf_first), true, ifeq(iext(P_105, sK2_testcase_premise_fullish_020_Logical_Complications_BNODE_lu1, uri_ex_c1), true, true, true), true)=true))). % 53.00/39.91 tff(c_36444, plain, (![D_818]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_818), true, icext(D_818, uri_owl_complementOf), true)=true))). % 53.00/39.91 tff(c_36378, plain, (![D_816]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_816), true, icext(D_816, uri_owl_unionOf), true)=true))). % 53.00/39.91 tff(c_3080, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_range), true, ifeq(iext(P_105, uri_rdfs_member, uri_rdfs_Resource), true, true, true), true)=true))). % 53.00/39.91 tff(c_36173, plain, (![D_813]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_813), true, icext(D_813, uri_rdfs_isDefinedBy), true)=true))). % 53.00/39.91 tff(c_36107, plain, (![D_811]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_811), true, icext(D_811, uri_rdfs_subClassOf), true)=true))). % 53.00/39.91 tff(c_35905, plain, (![D_808]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_808), true, icext(D_808, uri_owl_intersectionOf), true)=true))). % 53.00/39.91 tff(c_3017, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_subClassOf), true, ifeq(iext(P_105, uri_rdfs_Datatype, uri_rdfs_Class), true, true, true), true)=true))). % 53.00/39.91 tff(c_35839, plain, (![D_806]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_806), true, icext(D_806, uri_owl_disjointWith), true)=true))). % 53.00/39.91 tff(c_35773, plain, (![D_804]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_804), true, icext(D_804, uri_rdfs_range), true)=true))). % 53.00/39.91 tff(c_2993, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_range), true, ifeq(iext(P_105, uri_rdf__3, uri_rdfs_Resource), true, true, true), true)=true))). % 53.00/39.91 tff(c_35567, plain, (![D_801]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_801), true, icext(D_801, uri_rdf_Bag), true)=true))). % 53.00/39.91 tff(c_35500, plain, (![D_799]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_799), true, icext(D_799, uri_rdfs_Seq), true)=true))). % 53.00/39.91 tff(c_35434, plain, (![D_797]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_797), true, icext(D_797, sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs), true)=true))). % 53.00/39.91 tff(c_3104, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_domain), true, ifeq(iext(P_105, uri_rdf_type, uri_rdfs_Resource), true, true, true), true)=true))). % 53.00/39.91 tff(c_35233, plain, (![D_794]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_794), true, icext(D_794, uri_rdfs_Container), true)=true))). % 53.00/39.91 tff(c_35164, plain, (![D_792]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_792), true, icext(D_792, uri_rdf_Alt), true)=true))). % 53.00/39.91 tff(c_3005, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_range), true, ifeq(iext(P_105, uri_rdf_predicate, uri_rdfs_Resource), true, true, true), true)=true))). % 53.00/39.91 tff(c_34963, plain, (![D_789]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_789), true, icext(D_789, uri_rdfs_Datatype), true)=true))). % 53.00/39.91 tff(c_34895, plain, (![D_787]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_787), true, icext(D_787, uri_rdfs_Literal), true)=true))). % 53.00/39.91 tff(c_2849, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_domain), true, ifeq(iext(P_105, uri_rdfs_comment, uri_rdfs_Resource), true, true, true), true)=true))). % 53.00/39.91 tff(c_34666, plain, (![D_784]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_784), true, icext(D_784, uri_rdfs_Class), true)=true))). % 53.00/39.91 tff(c_34599, plain, (![D_782]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_782), true, icext(D_782, uri_ex_d), true)=true))). % 53.00/39.91 tff(c_3086, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_domain), true, ifeq(iext(P_105, uri_rdf__1, uri_rdfs_Resource), true, true, true), true)=true))). % 53.00/39.91 tff(c_34384, plain, (![D_779]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_779), true, icext(D_779, uri_rdf_XMLLiteral), true)=true))). % 53.00/39.91 tff(c_34317, plain, (![D_777]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_777), true, icext(D_777, uri_rdfs_ContainerMembershipProperty), true)=true))). % 53.00/39.91 tff(c_34120, plain, (![D_774]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_774), true, icext(D_774, sK5_testcase_premise_fullish_020_Logical_Complications_BNODE_li2), true)=true))). % 53.00/39.91 tff(c_2957, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdf_type), true, ifeq(iext(P_105, uri_rdf_Property, uri_rdfs_Class), true, true, true), true)=true))). % 53.00/39.91 tff(c_34054, plain, (![D_772]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_772), true, icext(D_772, sK7_testcase_premise_fullish_020_Logical_Complications_BNODE_li1), true)=true))). % 53.00/39.91 tff(c_33987, plain, (![D_770]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_770), true, icext(D_770, uri_rdf_List), true)=true))). % 53.00/39.91 tff(c_2795, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_owl_unionOf), true, ifeq(iext(P_105, uri_ex_c, sK2_testcase_premise_fullish_020_Logical_Complications_BNODE_lu1), true, true, true), true)=true))). % 53.00/39.91 tff(c_33791, plain, (![D_767]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_767), true, icext(D_767, uri_rdfs_subPropertyOf), true)=true))). % 53.00/39.91 tff(c_33724, plain, (![D_765]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_765), true, icext(D_765, uri_rdfs_member), true)=true))). % 53.00/39.91 tff(c_33658, plain, (![D_763]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_763), true, icext(D_763, uri_rdfs_domain), true)=true))). % 53.00/39.91 tff(c_14599, 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))). % 53.00/39.91 tff(c_17195, 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))). % 53.00/39.91 tff(c_33538, plain, (![D_758]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_758), true, icext(D_758, uri_rdfs_label), true)=true))). % 53.00/39.91 tff(c_14548, 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))). % 53.00/39.91 tff(c_15803, 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))). % 53.00/39.91 tff(c_2951, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdf_first), true, ifeq(iext(P_105, sK7_testcase_premise_fullish_020_Logical_Complications_BNODE_li1, uri_ex_c), true, true, true), true)=true))). % 53.00/39.91 tff(c_14166, 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))). % 53.00/39.91 tff(c_33223, plain, (![D_749]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_749), true, icext(D_749, sK1_testcase_premise_fullish_020_Logical_Complications_BNODE_lu3), true)=true))). % 53.00/39.91 tff(c_14481, 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))). % 53.00/39.91 tff(c_14006, 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))). % 53.00/39.91 tff(c_2873, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_domain), true, ifeq(iext(P_105, uri_rdfs_seeAlso, uri_rdfs_Resource), true, true, true), true)=true))). % 53.00/39.91 tff(c_13706, 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))). % 53.00/39.91 tff(c_13851, 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))). % 53.00/39.91 tff(c_14007, 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))). % 53.00/39.91 tff(c_32907, plain, (![D_740]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_740), true, icext(D_740, uri_rdf_predicate), true)=true))). % 53.00/39.91 tff(c_13705, 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))). % 53.00/39.91 tff(c_32820, 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))). % 53.00/39.91 tff(c_13940, 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))). % 53.00/39.91 tff(c_32677, plain, (![D_732]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_732), true, icext(D_732, sK2_testcase_premise_fullish_020_Logical_Complications_BNODE_lu1), true)=true))). % 53.00/39.91 tff(c_12975, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_ex_d, uri_rdfs_Class), true)=true))). % 53.00/39.91 tff(c_13214, 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))). % 53.00/39.92 tff(c_13564, 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))). % 53.00/39.92 tff(c_2927, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdf_type), true, ifeq(iext(P_105, uri_rdf__2, uri_rdf_Property), true, true, true), true)=true))). % 53.00/39.92 tff(c_12811, 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))). % 53.00/39.92 tff(c_13047, 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))). % 53.00/39.92 tff(c_13094, 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))). % 53.00/39.92 tff(c_32391, plain, (![D_723]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_723), true, icext(D_723, uri_rdfs_comment), true)=true))). % 53.00/39.92 tff(c_13141, 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))). % 53.00/39.92 tff(c_13263, 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))). % 53.00/39.92 tff(c_12880, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs, uri_rdfs_Class), true)=true))). % 53.00/39.92 tff(c_2867, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdf_type), true, ifeq(iext(P_105, uri_rdf_XMLLiteral, uri_rdfs_Datatype), true, true, true), true)=true))). % 53.00/39.92 tff(c_12928, 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))). % 53.00/39.92 tff(c_13611, 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))). % 53.39/39.92 tff(c_16332, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, sK7_testcase_premise_fullish_020_Logical_Complications_BNODE_li1, uri_rdf_List), true)=true))). % 53.39/39.92 tff(c_17067, 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))). % 53.39/39.92 tff(c_15573, 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))). % 53.39/39.92 tff(c_14388, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, sK1_testcase_premise_fullish_020_Logical_Complications_BNODE_lu3, uri_rdf_List), true)=true))). % 53.39/39.92 tff(c_13375, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, sK2_testcase_premise_fullish_020_Logical_Complications_BNODE_lu1, uri_rdf_List), true)=true))). % 53.39/39.92 tff(c_12353, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, sK5_testcase_premise_fullish_020_Logical_Complications_BNODE_li2, uri_rdf_List), true)=true))). % 53.39/39.92 tff(c_2825, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdf_type), true, ifeq(iext(P_105, uri_rdf__1, uri_rdf_Property), true, true, true), true)=true))). % 53.39/39.92 tff(c_12736, 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))). % 53.39/39.92 tff(c_12244, 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))). % 53.39/39.92 tff(c_12687, 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))). % 53.39/39.92 tff(c_31846, plain, (![D_705]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_705), true, icext(D_705, uri_rdfs_Statement), true)=true))). % 53.39/39.92 tff(c_12634, 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))). % 53.39/39.92 tff(c_6957, 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))). % 53.39/39.92 tff(c_3122, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_domain), true, ifeq(iext(P_105, uri_rdf__3, uri_rdfs_Resource), true, true, true), true)=true))). % 53.39/39.92 tff(c_9975, 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))). % 53.39/39.92 tff(c_9335, 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))). % 53.39/39.92 tff(c_6855, 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))). % 53.39/39.92 tff(c_10441, 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))). % 53.39/39.92 tff(c_10508, 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))). % 53.39/39.92 tff(c_2945, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdf_rest), true, ifeq(iext(P_105, sK5_testcase_premise_fullish_020_Logical_Complications_BNODE_li2, uri_rdf_nil), true, true, true), true)=true))). % 53.39/39.92 tff(c_6313, 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))). % 53.39/39.92 tff(c_7137, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_owl_disjointWith, uri_owl_disjointWith), true)=true))). % 53.39/39.92 tff(c_11297, 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))). % 53.39/39.92 tff(c_9143, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_ex_d, uri_rdfs_Resource), true)=true))). % 53.39/39.92 tff(c_9205, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_ex_d, uri_ex_d), true)=true))). % 53.39/39.92 tff(c_8552, 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))). % 53.39/39.92 tff(c_8097, 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))). % 53.39/39.92 tff(c_3056, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_owl_intersectionOf), true, ifeq(iext(P_105, sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs, sK7_testcase_premise_fullish_020_Logical_Complications_BNODE_li1), true, true, true), true)=true))). % 53.39/39.92 tff(c_7442, 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))). % 53.39/39.92 tff(c_10223, 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))). % 53.39/39.92 tff(c_30927, plain, (![D_678]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_678), true, icext(D_678, uri_rdf_nil), true)=true))). % 53.39/39.92 tff(c_9682, 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))). % 53.39/39.92 tff(c_10575, 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))). % 53.39/39.92 tff(c_11916, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_owl_complementOf, uri_rdf_Property), true)=true))). % 53.39/39.92 tff(c_2885, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_domain), true, ifeq(iext(P_105, uri_rdf_predicate, uri_rdfs_Statement), true, true, true), true)=true))). % 53.39/39.92 tff(c_11440, 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))). % 53.39/39.92 tff(c_11042, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_owl_unionOf, uri_rdf_Property), true)=true))). % 53.39/39.92 tff(c_6856, 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))). % 53.39/39.92 tff(c_9974, 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))). % 53.39/39.92 tff(c_8681, 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))). % 53.39/39.92 tff(c_7052, 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))). % 53.39/39.92 tff(c_2783, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_range), true, ifeq(iext(P_105, uri_rdfs_comment, uri_rdfs_Literal), true, true, true), true)=true))). % 53.39/39.92 tff(c_3151, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_106), true, iext(Q_106, uri_rdfs_isDefinedBy, uri_rdfs_isDefinedBy), true)=true))). % 53.39/39.92 tff(c_9400, 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))). % 53.39/39.92 tff(c_10362, plain, (![E_41]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, E_41), true, iext(uri_rdfs_subClassOf, sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs, E_41), true)=true))). % 53.39/39.92 tff(c_30336, plain, (![D_660]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_660), true, icext(D_660, uri_rdf_type), true)=true))). % 53.39/39.92 tff(c_5910, 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))). % 53.39/39.92 tff(c_2777, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdf_first), true, ifeq(iext(P_105, sK1_testcase_premise_fullish_020_Logical_Complications_BNODE_lu3, uri_ex_c3), true, true, true), true)=true))). % 53.39/39.92 tff(c_8193, 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))). % 53.39/39.92 tff(c_8680, 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))). % 53.39/39.92 tff(c_8551, 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))). % 53.39/39.92 tff(c_30005, plain, (![D_651]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, D_651), true, icext(D_651, uri_rdf_XMLLiteral), true)=true))). % 53.39/39.92 tff(c_8845, 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))). % 53.39/39.92 tff(c_11362, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_owl_unionOf, uri_owl_unionOf), true)=true))). % 53.39/39.92 tff(c_2999, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdf_type), true, ifeq(iext(P_105, uri_rdf__1, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 53.39/39.92 tff(c_7914, 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))). % 53.39/39.92 tff(c_6312, 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))). % 53.39/39.92 tff(c_29682, plain, (![D_642]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_642), true, icext(D_642, uri_rdf__3), true)=true))). % 53.39/39.92 tff(c_8249, 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))). % 53.39/39.92 tff(c_7538, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_owl_complementOf, uri_owl_complementOf), true)=true))). % 53.39/39.92 tff(c_5508, 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))). % 53.39/39.92 tff(c_2897, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdf_type), true, ifeq(iext(P_105, uri_rdf_first, uri_rdf_Property), true, true, true), true)=true))). % 53.39/39.92 tff(c_7325, 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))). % 53.39/39.92 tff(c_9144, plain, (![E_41]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, E_41), true, iext(uri_rdfs_subClassOf, uri_ex_d, E_41), true)=true))). % 53.39/39.92 tff(c_10793, 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))). % 53.39/39.92 tff(c_7736, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_owl_disjointWith, uri_rdf_Property), true)=true))). % 53.39/39.92 tff(c_8777, 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))). % 53.39/39.92 tff(c_5393, 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))). % 53.39/39.92 tff(c_9683, 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))). % 53.39/39.92 tff(c_9616, 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))). % 53.39/39.92 tff(c_11296, 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))). % 53.39/39.92 tff(c_7229, 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))). % 53.39/39.92 tff(c_2981, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_subClassOf), true, ifeq(iext(P_105, uri_rdfs_Seq, uri_rdfs_Container), true, true, true), true)=true))). % 53.39/39.92 tff(c_6070, 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))). % 53.39/39.92 tff(c_8034, 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))). % 53.39/39.92 tff(c_28862, plain, (![D_616]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_616), true, icext(D_616, sK3_testcase_premise_fullish_020_Logical_Complications_BNODE_lu2), true)=true))). % 53.39/39.92 tff(c_12161, 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))). % 53.39/39.92 tff(c_9746, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_owl_intersectionOf, uri_rdf_Property), true)=true))). % 53.39/39.92 tff(c_2705, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_domain), true, ifeq(iext(P_105, uri_rdf_subject, uri_rdfs_Statement), true, true, true), true)=true))). % 53.39/39.92 tff(c_7673, 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))). % 53.39/39.92 tff(c_7051, 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))). % 53.39/39.92 tff(c_28535, plain, (![D_607]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_607), true, icext(D_607, uri_rdf__1), true)=true))). % 53.39/39.92 tff(c_15077, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, sK3_testcase_premise_fullish_020_Logical_Complications_BNODE_lu2, uri_rdf_List), true)=true))). % 53.39/39.92 tff(c_3050, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdf_type), true, ifeq(iext(P_105, uri_rdf_type, uri_rdf_Property), true, true, true), true)=true))). % 53.39/39.92 tff(c_7603, 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))). % 53.39/39.92 tff(c_9011, 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))). % 53.39/39.92 tff(c_5761, 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))). % 53.39/39.92 tff(c_28191, plain, (![D_598]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_598), true, icext(D_598, uri_rdf__2), true)=true))). % 53.39/39.92 tff(c_10361, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs, uri_rdfs_Resource), true)=true))). % 53.39/39.92 tff(c_10672, 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))). % 53.39/39.92 tff(c_6508, 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))). % 53.39/39.92 tff(c_2831, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_range), true, ifeq(iext(P_105, uri_rdf_first, uri_rdfs_Resource), true, true, true), true)=true))). % 53.39/39.92 tff(c_6203, 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))). % 53.39/39.92 tff(c_6641, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs, sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs), true)=true))). % 53.39/39.92 tff(c_11682, 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))). % 53.39/39.92 tff(c_5828, 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))). % 53.39/39.92 tff(c_5983, 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))). % 53.39/39.92 tff(c_8096, 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))). % 53.39/39.92 tff(c_27672, plain, (![D_581]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_581), true, icext(D_581, uri_rdf_value), true)=true))). % 53.39/39.92 tff(c_11505, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_owl_intersectionOf, uri_owl_intersectionOf), true)=true))). % 53.39/39.92 tff(c_11439, 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))). % 53.39/39.92 tff(c_2789, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_domain), true, ifeq(iext(P_105, uri_rdf_object, uri_rdfs_Statement), true, true, true), true)=true))). % 53.39/39.92 tff(c_7672, 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))). % 53.39/39.92 tff(c_10671, 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))). % 53.39/39.92 tff(c_5509, 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))). % 53.39/39.92 tff(c_5166, plain, (![Q_48, X_132]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, X_132, uri_rdfs_Resource), true)=true))). % 53.39/39.92 tff(c_3198, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_106), true, iext(Q_106, uri_rdfs_Seq, uri_rdfs_Container), true)=true))). % 53.39/39.92 tff(c_3172, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_106), true, iext(Q_106, uri_rdf__1, uri_rdf_Property), true)=true))). % 53.39/39.92 tff(c_3199, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_106), true, iext(Q_106, uri_rdf_rest, uri_rdf_List), true)=true))). % 53.39/39.92 tff(c_3164, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_first, Q_106), true, iext(Q_106, sK1_testcase_premise_fullish_020_Logical_Complications_BNODE_lu3, uri_ex_c3), true)=true))). % 53.39/39.92 tff(c_3210, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_owl_intersectionOf, Q_106), true, iext(Q_106, sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs, sK7_testcase_premise_fullish_020_Logical_Complications_BNODE_li1), true)=true))). % 53.39/39.92 tff(c_2579, plain, (![E_100]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_100), true, iext(uri_rdfs_subClassOf, uri_rdf_Bag, E_100), true)=true))). % 53.39/39.92 tff(c_3195, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_106), true, iext(Q_106, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true)=true))). % 53.39/39.92 tff(c_3222, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_owl_complementOf, Q_106), true, iext(Q_106, sK4_testcase_premise_fullish_020_Logical_Complications_BNODE_xc, uri_ex_c2), true)=true))). % 53.39/39.92 tff(c_2580, plain, (![E_100]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, E_100), true, iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, E_100), true)=true))). % 53.39/39.92 tff(c_3161, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_106), true, iext(Q_106, uri_rdfs_domain, uri_rdfs_Class), true)=true))). % 53.39/39.92 tff(c_3193, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_first, Q_106), true, iext(Q_106, sK7_testcase_premise_fullish_020_Logical_Complications_BNODE_li1, uri_ex_c), true)=true))). % 53.39/39.92 tff(c_3175, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_106), true, iext(Q_106, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true)=true))). % 53.39/39.92 tff(c_3168, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_106), true, iext(Q_106, uri_rdf__3, uri_rdf_Property), true)=true))). % 53.39/39.92 tff(c_3217, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_106), true, iext(Q_106, uri_rdf_XMLLiteral, uri_rdfs_Literal), true)=true))). % 53.39/39.92 tff(c_3208, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_106), true, iext(Q_106, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso), true)=true))). % 53.39/39.92 tff(c_26852, plain, (![D_553]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_553), true, icext(D_553, uri_rdf__1), true)=true))). % 53.39/39.92 tff(c_3223, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_rest, Q_106), true, iext(Q_106, sK7_testcase_premise_fullish_020_Logical_Complications_BNODE_li1, sK5_testcase_premise_fullish_020_Logical_Complications_BNODE_li2), true)=true))). % 53.39/39.93 tff(c_3204, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_106), true, iext(Q_106, uri_rdfs_Datatype, uri_rdfs_Class), true)=true))). % 53.39/39.93 tff(c_3177, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_106), true, iext(Q_106, uri_rdf_rest, uri_rdf_List), true)=true))). % 53.39/39.93 tff(c_3202, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_106), true, iext(Q_106, uri_rdf_predicate, uri_rdfs_Resource), true)=true))). % 53.39/39.93 tff(c_3155, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_106), true, iext(Q_106, uri_rdf_subject, uri_rdf_Property), true)=true))). % 53.39/39.93 tff(c_3218, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_106), true, iext(Q_106, uri_rdf_type, uri_rdfs_Resource), true)=true))). % 53.39/39.93 tff(c_3181, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_106), true, iext(Q_106, uri_rdf_nil, uri_rdf_List), true)=true))). % 53.39/39.93 tff(c_26663, plain, (![D_544]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_544), true, icext(D_544, uri_rdf_first), true)=true))). % 53.39/39.93 tff(c_3183, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_rest, Q_106), true, iext(Q_106, sK2_testcase_premise_fullish_020_Logical_Complications_BNODE_lu1, sK3_testcase_premise_fullish_020_Logical_Complications_BNODE_lu2), true)=true))). % 53.39/39.93 tff(c_3209, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_106), true, iext(Q_106, uri_rdf_type, uri_rdf_Property), true)=true))). % 53.39/39.93 tff(c_3196, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_106), true, iext(Q_106, uri_rdfs_range, uri_rdf_Property), true)=true))). % 53.39/39.93 tff(c_3211, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_106), true, iext(Q_106, uri_rdf_value, uri_rdf_Property), true)=true))). % 53.39/39.93 tff(c_3173, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_106), true, iext(Q_106, uri_rdf_first, uri_rdfs_Resource), true)=true))). % 53.39/39.93 tff(c_3190, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_106), true, iext(Q_106, uri_rdf__1, uri_rdfs_Resource), true)=true))). % 53.39/39.93 tff(c_3194, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_106), true, iext(Q_106, uri_rdf_Property, uri_rdfs_Class), true)=true))). % 53.39/39.93 tff(c_3206, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_106), true, iext(Q_106, uri_rdfs_subClassOf, uri_rdfs_Class), true)=true))). % 53.39/39.93 tff(c_3220, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_106), true, iext(Q_106, uri_rdf__3, uri_rdfs_ContainerMembershipProperty), true)=true))). % 53.39/39.93 tff(c_3201, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_106), true, iext(Q_106, uri_rdf__1, uri_rdfs_ContainerMembershipProperty), true)=true))). % 53.39/39.93 tff(c_3213, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_rest, Q_106), true, iext(Q_106, sK1_testcase_premise_fullish_020_Logical_Complications_BNODE_lu3, uri_rdf_nil), true)=true))). % 53.39/39.93 tff(c_3205, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_106), true, iext(Q_106, uri_rdf_first, uri_rdf_List), true)=true))). % 53.39/39.93 tff(c_2584, plain, (![E_100]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Literal, E_100), true, iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, E_100), true)=true))). % 53.39/39.93 tff(c_3214, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_106), true, iext(Q_106, uri_rdfs_member, uri_rdfs_Resource), true)=true))). % 53.39/39.93 tff(c_3184, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_106), true, iext(Q_106, uri_rdf_first, uri_rdf_Property), true)=true))). % 53.39/39.93 tff(c_3162, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_106), true, iext(Q_106, uri_rdf_subject, uri_rdfs_Resource), true)=true))). % 53.39/39.93 tff(c_26298, plain, (![D_526]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_526), true, icext(D_526, uri_rdf_subject), true)=true))). % 53.39/39.93 tff(c_3191, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_106), true, iext(Q_106, uri_rdf__2, uri_rdfs_Resource), true)=true))). % 53.39/39.93 tff(c_3185, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_106), true, iext(Q_106, uri_rdf_value, uri_rdfs_Resource), true)=true))). % 53.39/39.93 tff(c_3166, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_106), true, iext(Q_106, uri_rdf_object, uri_rdfs_Statement), true)=true))). % 53.39/39.93 tff(c_3224, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_first, Q_106), true, iext(Q_106, sK5_testcase_premise_fullish_020_Logical_Complications_BNODE_li2, sK4_testcase_premise_fullish_020_Logical_Complications_BNODE_xc), true)=true))). % 53.39/39.93 tff(c_2582, plain, (![E_100]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_100), true, iext(uri_rdfs_subClassOf, uri_rdf_Alt, E_100), true)=true))). % 53.39/39.93 tff(c_2581, plain, (![E_100]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_100), true, iext(uri_rdfs_subClassOf, uri_rdfs_Seq, E_100), true)=true))). % 53.39/39.93 tff(c_3153, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_106), true, iext(Q_106, uri_rdf_type, uri_rdfs_Class), true)=true))). % 53.39/39.93 tff(c_26085, plain, (![D_517]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_517), true, icext(D_517, uri_rdf_object), true)=true))). % 53.39/39.93 tff(c_3180, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_106), true, iext(Q_106, uri_rdfs_seeAlso, uri_rdfs_Resource), true)=true))). % 53.39/39.93 tff(c_3158, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_106), true, iext(Q_106, uri_rdf_rest, uri_rdf_Property), true)=true))). % 53.39/39.93 tff(c_3225, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_106), true, iext(Q_106, uri_ex_d, sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs), true)=true))). % 53.39/39.93 tff(c_3221, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_106), true, iext(Q_106, uri_rdf__3, uri_rdfs_Resource), true)=true))). % 53.39/39.93 tff(c_3156, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_106), true, iext(Q_106, uri_rdfs_subPropertyOf, uri_rdf_Property), true)=true))). % 53.39/39.93 tff(c_3216, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_106), true, iext(Q_106, uri_rdf__2, uri_rdfs_Resource), true)=true))). % 53.39/39.93 tff(c_3197, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_first, Q_106), true, iext(Q_106, sK2_testcase_premise_fullish_020_Logical_Complications_BNODE_lu1, uri_ex_c1), true)=true))). % 53.39/39.93 tff(c_3203, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_106), true, iext(Q_106, uri_rdf_Alt, uri_rdfs_Container), true)=true))). % 53.39/39.93 tff(c_3215, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_106), true, iext(Q_106, uri_rdf__1, uri_rdfs_Resource), true)=true))). % 53.39/39.93 tff(c_3157, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_106), true, iext(Q_106, uri_rdf_value, uri_rdfs_Resource), true)=true))). % 53.39/39.93 tff(c_3179, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_106), true, iext(Q_106, uri_rdf_XMLLiteral, uri_rdfs_Datatype), true)=true))). % 53.39/39.93 tff(c_3154, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_first, Q_106), true, iext(Q_106, sK3_testcase_premise_fullish_020_Logical_Complications_BNODE_lu2, uri_ex_c2), true)=true))). % 53.39/39.93 tff(c_14552, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_label), true)=true))). % 53.39/39.93 tff(c_14551, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_label), true)=true))). % 53.39/39.93 tff(c_25733, plain, (![D_501]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_501), true, icext(D_501, uri_rdf_Property), true)=true))). % 53.39/39.93 tff(c_15806, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_comment), true)=true))). % 53.39/39.93 tff(c_15807, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_comment), true)=true))). % 53.39/39.93 tff(c_17198, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_predicate), true)=true))). % 53.39/39.93 tff(c_3219, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_106), true, iext(Q_106, uri_rdfs_range, uri_rdfs_Class), true)=true))). % 53.39/39.93 tff(c_17199, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_predicate), true)=true))). % 53.39/39.93 tff(c_14485, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_member), true)=true))). % 53.39/39.93 tff(c_14170, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Resource), true)=true))). % 53.39/39.93 tff(c_3171, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_106), true, iext(Q_106, uri_rdf__2, uri_rdfs_ContainerMembershipProperty), true)=true))). % 53.39/39.93 tff(c_13854, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_List), true)=true))). % 53.39/39.93 tff(c_13709, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdf_List), true)=true))). % 53.39/39.93 tff(c_13943, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Statement), true)=true))). % 53.39/39.93 tff(c_13944, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Statement), true)=true))). % 53.39/39.93 tff(c_3188, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_106), true, iext(Q_106, uri_rdfs_subPropertyOf, uri_rdf_Property), true)=true))). % 53.39/39.93 tff(c_2676, plain, (![R_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_seeAlso, R_103), true, iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, R_103), true)=true))). % 53.39/39.93 tff(c_3187, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_106), true, iext(Q_106, uri_rdf_object, uri_rdf_Property), true)=true))). % 53.39/39.93 tff(c_3189, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_106), true, iext(Q_106, uri_rdf__2, uri_rdf_Property), true)=true))). % 53.39/39.93 tff(c_25256, plain, (![D_483]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_483), true, icext(D_483, uri_rdf__3), true)=true))). % 53.39/39.93 tff(c_3165, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_106), true, iext(Q_106, uri_rdfs_comment, uri_rdfs_Literal), true)=true))). % 53.39/39.93 tff(c_25161, plain, (![D_480]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_480), true, icext(D_480, uri_rdf__2), true)=true))). % 53.39/39.93 tff(c_6959, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_XMLLiteral), true)=true))). % 53.39/39.93 tff(c_2583, plain, (![E_100]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, E_100), true, iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, E_100), true)=true))). % 53.39/39.93 tff(c_7918, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_value), true)=true))). % 53.39/39.93 tff(c_25010, plain, (![D_475]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_475), true, icext(D_475, uri_rdf_rest), true)=true))). % 53.39/39.93 tff(c_3152, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_106), true, iext(Q_106, uri_rdf_subject, uri_rdfs_Statement), true)=true))). % 53.39/39.93 tff(c_9013, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Seq), true)=true))). % 53.39/39.93 tff(c_8196, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_subClassOf), true)=true))). % 53.39/39.93 tff(c_9403, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__2), true)=true))). % 53.39/39.93 tff(c_3160, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_106), true, iext(Q_106, uri_rdf_Bag, uri_rdfs_Container), true)=true))). % 53.39/39.93 tff(c_8848, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__1), true)=true))). % 53.39/39.93 tff(c_10512, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Container), true)=true))). % 53.39/39.93 tff(c_24376, plain, (![D_464, X_465]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, D_464), true, icext(D_464, X_465), true)=true))). % 53.39/39.93 tff(c_9620, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_type), true)=true))). % 53.39/39.93 tff(c_7232, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_domain), true)=true))). % 53.39/39.93 tff(c_3167, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_owl_unionOf, Q_106), true, iext(Q_106, uri_ex_c, sK2_testcase_premise_fullish_020_Logical_Complications_BNODE_lu1), true)=true))). % 53.39/39.93 tff(c_8780, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_first), true)=true))). % 53.39/39.93 tff(c_5763, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_range), true)=true))). % 53.39/39.93 tff(c_24068, plain, (![C_88, X_60]: (ifeq(icext(C_88, X_60), true, true, true)=true))). % 53.39/39.93 tff(c_11508, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_owl_intersectionOf), true)=true))). % 53.39/39.93 tff(c_3176, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_106), true, iext(Q_106, uri_rdfs_comment, uri_rdfs_Resource), true)=true))). % 53.39/39.93 tff(c_7233, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_domain), true)=true))). % 53.39/39.93 tff(c_23555, plain, (![X_450, Y_451]: (ifeq(iext(uri_rdfs_subPropertyOf, X_450, Y_451), true, icext(uri_rdf_Property, X_450), true)=true))). % 53.39/39.93 tff(c_3186, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_106), true, iext(Q_106, uri_rdfs_label, uri_rdfs_Literal), true)=true))). % 53.39/39.93 tff(c_7140, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_owl_disjointWith), true)=true))). % 53.39/39.93 tff(c_10226, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_object), true)=true))). % 53.39/39.93 tff(c_23070, plain, (![X_443, Y_444]: (ifeq(iext(uri_rdfs_domain, X_443, Y_444), true, icext(uri_rdf_Property, X_443), true)=true))). % 53.39/39.93 tff(c_7917, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_value), true)=true))). % 53.39/39.93 tff(c_8036, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_ContainerMembershipProperty), true)=true))). % 53.39/39.93 tff(c_3169, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_106), true, iext(Q_106, uri_rdfs_label, uri_rdfs_Resource), true)=true))). % 53.39/39.93 tff(c_8849, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__1), true)=true))). % 53.39/39.93 tff(c_22275, plain, (![X_434, Y_435]: (ifeq(iext(uri_rdfs_subClassOf, X_434, Y_435), true, icext(uri_rdfs_Class, X_434), true)=true))). % 53.39/39.93 tff(c_6858, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdf_Property), true)=true))). % 53.39/39.93 tff(c_8197, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_subClassOf), true)=true))). % 53.39/39.93 tff(c_3159, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_106), true, iext(Q_106, uri_rdfs_subClassOf, uri_rdfs_Class), true)=true))). % 53.39/39.93 tff(c_8781, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_first), true)=true))). % 53.39/39.93 tff(c_22146, plain, (![X_426, Y_427]: (ifeq(iext(uri_rdfs_label, X_426, Y_427), true, icext(uri_rdfs_Literal, Y_427), true)=true))). % 53.39/39.93 tff(c_7445, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_subject), true)=true))). % 53.39/39.93 tff(c_10578, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_rest), true)=true))). % 53.39/39.93 tff(c_3178, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_106), true, iext(Q_106, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property), true)=true))). % 53.39/39.93 tff(c_11300, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__3), true)=true))). % 53.39/39.93 tff(c_21617, plain, (![X_418, Y_419]: (ifeq(iext(uri_rdfs_subPropertyOf, X_418, Y_419), true, icext(uri_rdf_Property, Y_419), true)=true))). % 53.39/39.93 tff(c_10227, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_object), true)=true))). % 53.39/39.93 tff(c_9207, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_ex_d), true)=true))). % 53.39/39.93 tff(c_3207, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_owl_disjointWith, Q_106), true, iext(Q_106, uri_ex_d, uri_ex_c1), true)=true))). % 53.39/39.93 tff(c_21428, plain, (![X_411, Y_412]: (ifeq(iext(uri_rdf_first, X_411, Y_412), true, icext(uri_rdf_List, X_411), true)=true))). % 53.39/39.93 tff(c_7542, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_owl_complementOf), true)=true))). % 53.39/39.93 tff(c_10365, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs), true)=true))). % 53.39/39.93 tff(c_3192, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_rest, Q_106), true, iext(Q_106, sK5_testcase_premise_fullish_020_Logical_Complications_BNODE_li2, uri_rdf_nil), true)=true))). % 53.39/39.93 tff(c_11365, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_owl_unionOf), true)=true))). % 53.39/39.93 tff(c_7541, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_owl_complementOf), true)=true))). % 53.39/39.93 tff(c_12164, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Datatype), true)=true))). % 53.39/39.93 tff(c_21255, plain, (![X_401, Y_402]: (ifeq(iext(uri_rdf_predicate, X_401, Y_402), true, icext(uri_rdfs_Statement, X_401), true)=true))). % 53.39/39.93 tff(c_2412, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_96), true, icext(C_96, uri_rdfs_isDefinedBy), true)=true))). % 53.39/39.93 tff(c_3200, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_106), true, iext(Q_106, uri_rdf__3, uri_rdfs_Resource), true)=true))). % 53.39/39.93 tff(c_9619, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_type), true)=true))). % 53.39/39.93 tff(c_7139, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_owl_disjointWith), true)=true))). % 53.39/39.93 tff(c_20809, plain, (![X_393, Y_394]: (ifeq(iext(uri_rdfs_range, X_393, Y_394), true, icext(uri_rdfs_Class, Y_394), true)=true))). % 53.39/39.93 tff(c_7676, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Literal), true)=true))). % 53.39/39.93 tff(c_7446, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_subject), true)=true))). % 53.39/39.93 tff(c_3174, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_106), true, iext(Q_106, uri_rdfs_seeAlso, uri_rdfs_Resource), true)=true))). % 53.39/39.93 tff(c_6510, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__3), true)=true))). % 53.39/39.93 tff(c_10579, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_rest), true)=true))). % 53.39/39.93 tff(c_5985, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_Bag), true)=true))). % 53.39/39.93 tff(c_20523, plain, (![X_383, Y_384]: (ifeq(iext(uri_rdf_rest, X_383, Y_384), true, icext(uri_rdf_List, X_383), true)=true))). % 53.39/39.93 tff(c_5395, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_Alt), true)=true))). % 53.39/39.93 tff(c_2585, plain, (![E_100]: (ifeq(iext(uri_rdfs_subClassOf, sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs, E_100), true, iext(uri_rdfs_subClassOf, uri_ex_d, E_100), true)=true))). % 53.39/39.93 tff(c_11509, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_owl_intersectionOf), true)=true))). % 53.39/39.93 tff(c_7607, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_subPropertyOf), true)=true))). % 53.39/39.93 tff(c_20382, plain, (![X_375, Y_376]: (ifeq(iext(uri_rdf_object, X_375, Y_376), true, icext(uri_rdfs_Statement, X_375), true)=true))). % 53.39/39.93 tff(c_7606, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_subPropertyOf), true)=true))). % 53.39/39.93 tff(c_10675, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Class), true)=true))). % 53.39/39.93 tff(c_3170, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_106), true, iext(Q_106, uri_rdfs_domain, uri_rdf_Property), true)=true))). % 53.39/39.93 tff(c_5764, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_range), true)=true))). % 53.39/39.93 tff(c_19686, plain, (![X_366, Y_367]: (ifeq(iext(uri_rdfs_subClassOf, X_366, Y_367), true, icext(uri_rdfs_Class, Y_367), true)=true))). % 53.39/39.93 tff(c_11366, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_owl_unionOf), true)=true))). % 53.39/39.93 tff(c_3182, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_106), true, iext(Q_106, uri_rdf_predicate, uri_rdfs_Statement), true)=true))). % 53.39/39.93 tff(c_11443, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__2), true)=true))). % 53.39/39.93 tff(c_19253, plain, (![X_359, Y_360]: (ifeq(iext(uri_rdfs_range, X_359, Y_360), true, icext(uri_rdf_Property, X_359), true)=true))). % 53.39/39.93 tff(c_11299, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_member), true)=true))). % 53.39/39.93 tff(c_5914, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_seeAlso), true)=true))). % 53.39/39.93 tff(c_3163, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_106), true, iext(Q_106, uri_rdfs_member, uri_rdfs_Resource), true)=true))). % 53.39/39.93 tff(c_19143, plain, (![X_352, Y_353]: (ifeq(iext(uri_rdf_subject, X_352, Y_353), true, icext(uri_rdfs_Statement, X_352), true)=true))). % 53.39/39.93 tff(c_10364, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Resource), true)=true))). % 53.39/39.93 tff(c_5168, plain, (![C_19, X_132]: (ifeq(iext(uri_rdfs_domain, uri_rdf_type, C_19), true, icext(C_19, X_132), true)=true))). % 53.39/39.93 tff(c_5167, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_29), true, icext(C_29, uri_rdfs_Resource), true)=true))). % 53.39/39.93 tff(c_3212, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_rest, Q_106), true, iext(Q_106, sK3_testcase_premise_fullish_020_Logical_Complications_BNODE_lu2, sK1_testcase_premise_fullish_020_Logical_Complications_BNODE_lu3), true)=true))). % 53.39/39.93 tff(c_2032, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdf_first, C_92), true, icext(C_92, sK3_testcase_premise_fullish_020_Logical_Complications_BNODE_lu2), true)=true))). % 53.39/39.93 tff(c_2464, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdf_first, C_96), true, icext(C_96, uri_ex_c1), true)=true))). % 53.39/39.93 tff(c_18382, plain, (![X_335, Y_336]: (ifeq(iext(uri_rdfs_domain, X_335, Y_336), true, icext(uri_rdfs_Class, Y_336), true)=true))). % 53.39/39.93 tff(c_2476, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_owl_disjointWith, C_96), true, icext(C_96, uri_ex_c1), true)=true))). % 53.39/39.93 tff(c_2097, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdf_rest, C_92), true, icext(C_92, sK3_testcase_premise_fullish_020_Logical_Complications_BNODE_lu2), true)=true))). % 53.39/39.93 tff(c_2448, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdf_rest, C_96), true, icext(C_96, sK3_testcase_premise_fullish_020_Logical_Complications_BNODE_lu2), true)=true))). % 53.39/39.93 tff(c_2106, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdfs_range), true)=true))). % 53.39/39.93 tff(c_2109, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdf__3), true)=true))). % 53.39/39.93 tff(c_2101, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdf__1), true)=true))). % 53.39/39.93 tff(c_2495, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdf_first, C_96), true, icext(C_96, sK4_testcase_premise_fullish_020_Logical_Complications_BNODE_xc), true)=true))). % 53.39/39.93 tff(c_2102, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdf__2), true)=true))). % 53.39/39.93 tff(c_2076, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdf__2), true)=true))). % 53.39/39.93 tff(c_2444, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_96), true, icext(C_96, uri_rdfs_Datatype), true)=true))). % 53.39/39.94 tff(c_2077, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdf_rest, C_92), true, icext(C_92, sK5_testcase_premise_fullish_020_Logical_Complications_BNODE_li2), true)=true))). % 53.39/39.94 tff(c_2481, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdf_rest, C_96), true, icext(C_96, sK1_testcase_premise_fullish_020_Logical_Complications_BNODE_lu3), true)=true))). % 53.39/39.94 tff(c_2037, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdfs_subClassOf), true)=true))). % 53.39/39.94 tff(c_2496, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_96), true, icext(C_96, sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs), true)=true))). % 53.39/39.94 tff(c_17962, plain, (![X_318, Y_319]: (ifeq(iext(uri_rdfs_comment, X_318, Y_319), true, icext(uri_rdfs_Literal, Y_319), true)=true))). % 53.39/39.94 tff(c_2466, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_96), true, icext(C_96, uri_rdf_List), true)=true))). % 53.39/39.94 tff(c_2038, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_92), true, icext(C_92, uri_rdf_Bag), true)=true))). % 53.39/39.94 tff(c_2463, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdf_Property), true)=true))). % 53.39/39.94 tff(c_2045, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdf_object), true)=true))). % 53.39/39.94 tff(c_2065, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdf_predicate), true)=true))). % 53.39/39.94 tff(c_2477, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_96), true, icext(C_96, uri_rdfs_seeAlso), true)=true))). % 53.39/39.94 tff(c_2066, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdf_rest, C_92), true, icext(C_92, sK2_testcase_premise_fullish_020_Logical_Complications_BNODE_lu1), true)=true))). % 53.39/39.94 tff(c_2092, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_owl_disjointWith, C_92), true, icext(C_92, uri_ex_d), true)=true))). % 53.39/39.94 tff(c_2089, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_92), true, icext(C_92, uri_rdfs_Datatype), true)=true))). % 53.39/39.94 tff(c_2422, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_96), true, icext(C_96, uri_rdfs_Container), true)=true))). % 53.39/39.94 tff(c_2085, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdf__3), true)=true))). % 53.39/39.94 tff(c_16620, plain, (![X_289, Y_290]: (ifeq(iext(uri_rdf_type, X_289, Y_290), true, icext(uri_rdfs_Class, Y_290), true)=true))). % 53.39/39.94 tff(c_2049, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdfs_label), true)=true))). % 53.39/39.94 tff(c_2417, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_96), true, icext(C_96, uri_rdf_Property), true)=true))). % 53.39/39.94 tff(c_2040, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdf_subject), true)=true))). % 53.39/39.94 tff(c_2043, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdf_first, C_92), true, icext(C_92, sK1_testcase_premise_fullish_020_Logical_Complications_BNODE_lu3), true)=true))). % 53.39/39.94 tff(c_2091, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdfs_subClassOf), true)=true))). % 53.39/39.94 tff(c_2421, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdfs_Class), true)=true))). % 53.39/39.94 tff(c_17144, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_predicate, uri_rdf_predicate)=true)). % 53.39/39.94 tff(c_2460, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_96), true, icext(C_96, uri_rdfs_Class), true)=true))). % 53.39/39.94 tff(c_17078, plain, (ip(uri_rdf_predicate)=true)). % 53.39/39.94 tff(c_17021, plain, (iext(uri_rdf_type, uri_rdf_predicate, uri_rdf_Property)=true)). % 53.39/39.94 tff(c_16822, plain, (icext(uri_rdf_Property, uri_rdf_predicate)=true)). % 53.39/39.94 tff(c_2493, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_owl_complementOf, C_96), true, icext(C_96, uri_ex_c2), true)=true))). % 53.39/39.94 tff(c_2087, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdf_predicate), true)=true))). % 53.39/39.94 tff(c_2080, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdfs_isDefinedBy), true)=true))). % 53.39/39.94 tff(c_2113, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_92), true, icext(C_92, uri_ex_d), true)=true))). % 53.39/39.94 tff(c_2110, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_owl_complementOf, C_92), true, icext(C_92, sK4_testcase_premise_fullish_020_Logical_Complications_BNODE_xc), true)=true))). % 53.39/39.94 tff(c_2088, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_92), true, icext(C_92, uri_rdf_Alt), true)=true))). % 53.39/39.94 tff(c_2095, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_owl_intersectionOf, C_92), true, icext(C_92, sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs), true)=true))). % 53.39/39.94 tff(c_2482, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdf_rest, C_96), true, icext(C_96, uri_rdf_nil), true)=true))). % 53.39/39.94 tff(c_2078, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdf_first, C_92), true, icext(C_92, sK7_testcase_premise_fullish_020_Logical_Complications_BNODE_li1), true)=true))). % 53.39/39.94 tff(c_2044, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdfs_comment), true)=true))). % 53.39/39.94 tff(c_16296, plain, (iext(uri_rdf_type, sK7_testcase_premise_fullish_020_Logical_Complications_BNODE_li1, uri_rdf_List)=true)). % 53.39/39.94 tff(c_16085, plain, (icext(uri_rdf_List, sK7_testcase_premise_fullish_020_Logical_Complications_BNODE_li1)=true)). % 53.39/39.94 tff(c_2112, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdf_first, C_92), true, icext(C_92, sK5_testcase_premise_fullish_020_Logical_Complications_BNODE_li2), true)=true))). % 53.39/39.94 tff(c_2111, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdf_rest, C_92), true, icext(C_92, sK7_testcase_premise_fullish_020_Logical_Complications_BNODE_li1), true)=true))). % 53.39/39.94 tff(c_2053, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdf_first), true)=true))). % 53.39/39.94 tff(c_2060, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_92), true, icext(C_92, uri_rdfs_ContainerMembershipProperty), true)=true))). % 53.39/39.94 tff(c_2084, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdf_rest), true)=true))). % 53.39/39.94 tff(c_2090, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdf_first), true)=true))). % 53.39/39.94 tff(c_2031, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdf_type), true)=true))). % 53.39/39.94 tff(c_2081, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdfs_range), true)=true))). % 53.39/39.94 tff(c_2479, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_owl_intersectionOf, C_96), true, icext(C_96, sK7_testcase_premise_fullish_020_Logical_Complications_BNODE_li1), true)=true))). % 53.39/39.94 tff(c_2074, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdf__1), true)=true))). % 53.39/39.94 tff(c_2099, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdfs_member), true)=true))). % 53.39/39.94 tff(c_2063, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdfs_seeAlso), true)=true))). % 53.39/39.94 tff(c_15752, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_comment, uri_rdfs_comment)=true)). % 53.39/39.94 tff(c_15584, plain, (ip(uri_rdfs_comment)=true)). % 53.39/39.94 tff(c_15531, plain, (iext(uri_rdf_type, uri_rdfs_comment, uri_rdf_Property)=true)). % 53.39/39.94 tff(c_15475, plain, (icext(uri_rdf_Property, uri_rdfs_comment)=true)). % 53.39/39.94 tff(c_2058, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdfs_comment), true)=true))). % 53.39/39.94 tff(c_13856, plain, (![X_33]: (ifeq(icext(uri_rdf_List, X_33), true, icext(uri_rdf_List, X_33), true)=true))). % 53.39/39.94 tff(c_13945, plain, (![X_33]: (ifeq(icext(uri_rdfs_Statement, X_33), true, icext(uri_rdfs_Statement, X_33), true)=true))). % 53.39/39.94 tff(c_12166, plain, (![X_33]: (ifeq(icext(uri_rdfs_Datatype, X_33), true, icext(uri_rdfs_Datatype, X_33), true)=true))). % 53.39/39.94 tff(c_14854, plain, (![X_256, Y_257]: (ifeq(iext(uri_rdf_rest, X_256, Y_257), true, icext(uri_rdf_List, Y_257), true)=true))). % 53.39/39.94 tff(c_5397, plain, (![X_33]: (ifeq(icext(uri_rdf_Alt, X_33), true, icext(uri_rdf_Alt, X_33), true)=true))). % 53.39/39.94 tff(c_5833, plain, (![X_33]: (ifeq(icext(uri_rdfs_Literal, X_33), true, icext(uri_rdfs_Literal, X_33), true)=true))). % 53.39/39.94 tff(c_7329, plain, (![X_33]: (ifeq(icext(uri_rdf_Property, X_33), true, icext(uri_rdf_Property, X_33), true)=true))). % 53.39/39.94 tff(c_2072, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdfs_subPropertyOf), true)=true))). % 53.39/39.94 tff(c_15041, plain, (iext(uri_rdf_type, sK3_testcase_premise_fullish_020_Logical_Complications_BNODE_lu2, uri_rdf_List)=true)). % 53.39/39.94 tff(c_14876, plain, (icext(uri_rdf_List, sK3_testcase_premise_fullish_020_Logical_Complications_BNODE_lu2)=true)). % 53.39/39.94 tff(c_8038, plain, (![X_33]: (ifeq(icext(uri_rdfs_ContainerMembershipProperty, X_33), true, icext(uri_rdfs_ContainerMembershipProperty, X_33), true)=true))). % 53.39/39.94 tff(c_6961, plain, (![X_33]: (ifeq(icext(uri_rdf_XMLLiteral, X_33), true, icext(uri_rdf_XMLLiteral, X_33), true)=true))). % 53.39/39.94 tff(c_10513, plain, (![X_33]: (ifeq(icext(uri_rdfs_Container, X_33), true, icext(uri_rdfs_Container, X_33), true)=true))). % 53.39/39.94 tff(c_2083, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_92), true, icext(C_92, uri_rdfs_Seq), true)=true))). % 53.39/39.94 tff(c_9015, plain, (![X_33]: (ifeq(icext(uri_rdfs_Seq, X_33), true, icext(uri_rdfs_Seq, X_33), true)=true))). % 53.39/39.94 tff(c_6207, plain, (![X_33]: (ifeq(icext(uri_rdfs_Class, X_33), true, icext(uri_rdfs_Class, X_33), true)=true))). % 53.39/39.94 tff(c_6646, plain, (![X_33]: (ifeq(icext(sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs, X_33), true, icext(sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs, X_33), true)=true))). % 53.39/39.94 tff(c_5987, plain, (![X_33]: (ifeq(icext(uri_rdf_Bag, X_33), true, icext(uri_rdf_Bag, X_33), true)=true))). % 53.39/39.94 tff(c_9209, plain, (![X_33]: (ifeq(icext(uri_ex_d, X_33), true, icext(uri_ex_d, X_33), true)=true))). % 53.39/39.94 tff(c_14563, plain, (iext(uri_rdf_type, uri_rdfs_Resource, uri_rdfs_Class)=true)). % 53.39/39.94 tff(c_14497, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_label, uri_rdfs_label)=true)). % 53.39/39.94 tff(c_14427, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_member, uri_rdfs_member)=true)). % 53.39/39.94 tff(c_2105, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdf_type), true)=true))). % 53.39/39.94 tff(c_14352, plain, (iext(uri_rdf_type, sK1_testcase_premise_fullish_020_Logical_Complications_BNODE_lu3, uri_rdf_List)=true)). % 53.39/39.94 tff(c_14182, plain, (icext(uri_rdf_List, sK1_testcase_premise_fullish_020_Logical_Complications_BNODE_lu3)=true)). % 53.39/39.94 tff(c_14092, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Resource, uri_rdfs_Resource)=true)). % 53.39/39.94 tff(c_2098, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdf_rest, C_92), true, icext(C_92, sK1_testcase_premise_fullish_020_Logical_Complications_BNODE_lu3), true)=true))). % 53.39/39.94 tff(c_13955, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Statement, uri_rdfs_Resource)=true)). % 53.39/39.94 tff(c_13889, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Statement, uri_rdfs_Statement)=true)). % 53.39/39.94 tff(c_2459, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdf_first, C_96), true, icext(C_96, uri_ex_c), true)=true))). % 53.39/39.94 tff(c_13800, plain, (iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdf_List)=true)). % 53.39/39.94 tff(c_13654, plain, (iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdfs_Resource)=true)). % 53.39/39.94 tff(c_13575, plain, (iext(uri_rdf_type, uri_rdf_Alt, uri_rdfs_Class)=true)). % 53.39/39.94 tff(c_13528, plain, (iext(uri_rdf_type, uri_rdf_XMLLiteral, uri_rdfs_Class)=true)). % 53.39/39.94 tff(c_13339, plain, (iext(uri_rdf_type, sK2_testcase_premise_fullish_020_Logical_Complications_BNODE_lu1, uri_rdf_List)=true)). % 53.39/39.94 tff(c_13294, plain, (icext(uri_rdf_List, sK2_testcase_premise_fullish_020_Logical_Complications_BNODE_lu1)=true)). % 53.39/39.94 tff(c_2082, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdf_first, C_92), true, icext(C_92, sK2_testcase_premise_fullish_020_Logical_Complications_BNODE_lu1), true)=true))). % 53.39/39.94 tff(c_13227, plain, (iext(uri_rdf_type, uri_rdfs_Class, uri_rdfs_Class)=true)). % 53.39/39.94 tff(c_13178, plain, (iext(uri_rdf_type, uri_rdfs_Literal, uri_rdfs_Class)=true)). % 53.39/39.94 tff(c_2473, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_96), true, icext(C_96, uri_rdfs_Class), true)=true))). % 53.39/39.94 tff(c_13105, plain, (iext(uri_rdf_type, uri_rdf_Bag, uri_rdfs_Class)=true)). % 53.39/39.94 tff(c_13058, plain, (iext(uri_rdf_type, uri_rdfs_Container, uri_rdfs_Class)=true)). % 53.39/39.94 tff(c_13011, plain, (iext(uri_rdf_type, uri_rdfs_Seq, uri_rdfs_Class)=true)). % 53.39/39.94 tff(c_2446, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_96), true, icext(C_96, uri_rdf_List), true)=true))). % 53.39/39.94 tff(c_12939, plain, (iext(uri_rdf_type, uri_ex_d, uri_rdfs_Class)=true)). % 53.39/39.94 tff(c_12892, plain, (iext(uri_rdf_type, uri_rdfs_Datatype, uri_rdfs_Class)=true)). % 53.39/39.94 tff(c_12823, plain, (iext(uri_rdf_type, sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs, uri_rdfs_Class)=true)). % 53.39/39.94 tff(c_2415, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdf_first, C_96), true, icext(C_96, uri_ex_c2), true)=true))). % 53.39/39.94 tff(c_12775, plain, (iext(uri_rdf_type, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Class)=true)). % 53.39/39.94 tff(c_2488, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_96), true, icext(C_96, uri_rdfs_Literal), true)=true))). % 53.39/39.94 tff(c_12700, plain, (iext(uri_rdf_type, uri_rdf_List, uri_rdfs_Class)=true)). % 53.39/39.94 tff(c_12645, plain, (iext(uri_rdf_type, uri_rdfs_member, uri_rdf_Property)=true)). % 53.39/39.94 tff(c_12598, plain, (iext(uri_rdf_type, uri_rdfs_Statement, uri_rdfs_Class)=true)). % 53.39/39.94 tff(c_2428, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_96), true, icext(C_96, uri_rdfs_Literal), true)=true))). % 53.39/39.94 tff(c_12422, plain, (ic(uri_rdfs_Statement)=true)). % 53.39/39.94 tff(c_12364, plain, (icext(uri_rdfs_Class, uri_rdfs_Statement)=true)). % 53.39/39.94 tff(c_12297, plain, (iext(uri_rdf_type, sK5_testcase_premise_fullish_020_Logical_Complications_BNODE_li2, uri_rdf_List)=true)). % 53.39/39.94 tff(c_2413, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdfs_Statement), true)=true))). % 53.39/39.94 tff(c_12255, plain, (ip(uri_rdfs_label)=true)). % 53.39/39.94 tff(c_12202, plain, (iext(uri_rdf_type, uri_rdfs_label, uri_rdf_Property)=true)). % 53.39/39.94 tff(c_2059, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdf_rest), true)=true))). % 53.39/39.94 tff(c_12110, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Datatype)=true)). % 53.39/39.94 tff(c_11928, plain, (icext(uri_rdf_Property, uri_owl_complementOf)=true)). % 53.39/39.94 tff(c_2490, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_96), true, icext(C_96, uri_rdfs_Class), true)=true))). % 53.39/39.94 tff(c_11874, plain, (iext(uri_rdf_type, uri_owl_complementOf, uri_rdf_Property)=true)). % 53.39/39.94 tff(c_11719, plain, (icext(uri_rdf_Property, uri_rdfs_subClassOf)=true)). % 53.39/39.94 tff(c_2056, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdfs_isDefinedBy), true)=true))). % 53.39/39.94 tff(c_11640, plain, (iext(uri_rdf_type, uri_rdfs_subClassOf, uri_rdf_Property)=true)). % 53.39/39.94 tff(c_1536, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_range, S_5, O_6), true, true, true)=true))). % 53.39/39.94 tff(c_11454, plain, (iext(uri_rdfs_subPropertyOf, uri_owl_intersectionOf, uri_owl_intersectionOf)=true)). % 53.39/39.94 tff(c_11388, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__2, uri_rdfs_member)=true)). % 53.39/39.94 tff(c_3619, plain, (![S_5, O_6]: (ifeq(iext(uri_owl_unionOf, S_5, O_6), true, true, true)=true))). % 53.39/39.94 tff(c_11311, plain, (iext(uri_rdfs_subPropertyOf, uri_owl_unionOf, uri_owl_unionOf)=true)). % 53.39/39.94 tff(c_11245, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__3, uri_rdfs_member)=true)). % 53.39/39.94 tff(c_2046, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_owl_unionOf, C_92), true, icext(C_92, uri_ex_c), true)=true))). % 53.39/39.94 tff(c_3581, plain, (![S_5, O_6]: (ifeq(iext(uri_owl_disjointWith, S_5, O_6), true, true, true)=true))). % 53.39/39.94 tff(c_11055, plain, (icext(uri_rdf_Property, uri_owl_unionOf)=true)). % 53.39/39.94 tff(c_11000, plain, (iext(uri_rdf_type, uri_owl_unionOf, uri_rdf_Property)=true)). % 53.39/39.94 tff(c_3294, plain, (![S_5, O_6]: (ifeq(iext(uri_owl_intersectionOf, S_5, O_6), true, true, true)=true))). % 53.39/39.94 tff(c_10805, plain, (icext(uri_rdf_Property, uri_rdfs_range)=true)). % 53.39/39.94 tff(c_2443, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_96), true, icext(C_96, uri_rdf_Property), true)=true))). % 53.39/39.94 tff(c_10751, plain, (iext(uri_rdf_type, uri_rdfs_range, uri_rdf_Property)=true)). % 53.39/39.94 tff(c_10620, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdfs_Resource)=true)). % 53.39/39.94 tff(c_2093, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_92), true, icext(C_92, uri_rdfs_isDefinedBy), true)=true))). % 53.39/39.94 tff(c_10524, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_rest, uri_rdf_rest)=true)). % 53.39/39.94 tff(c_10456, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Container, uri_rdfs_Container)=true)). % 53.39/39.94 tff(c_10399, plain, (iext(uri_rdf_type, uri_rdfs_domain, uri_rdf_Property)=true)). % 53.39/39.94 tff(c_10309, plain, (iext(uri_rdfs_subClassOf, sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs, uri_rdfs_Resource)=true)). % 53.39/39.94 tff(c_1492, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_domain, S_5, O_6), true, true, true)=true))). % 53.39/39.94 tff(c_10172, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_object, uri_rdf_object)=true)). % 53.39/39.94 tff(c_10008, plain, (icext(uri_rdf_Property, uri_rdfs_member)=true)). % 53.39/39.94 tff(c_2042, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdfs_member), true)=true))). % 53.39/39.94 tff(c_9923, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Container, uri_rdfs_Resource)=true)). % 53.39/39.94 tff(c_9784, plain, (icext(uri_rdf_Property, uri_owl_intersectionOf)=true)). % 53.39/39.94 tff(c_2103, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_92), true, icext(C_92, uri_rdf_XMLLiteral), true)=true))). % 53.39/39.94 tff(c_9704, plain, (iext(uri_rdf_type, uri_owl_intersectionOf, uri_rdf_Property)=true)). % 53.39/39.94 tff(c_9631, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Resource)=true)). % 53.39/39.94 tff(c_9540, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_type, uri_rdf_type)=true)). % 53.39/39.94 tff(c_2035, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdf_value), true)=true))). % 53.39/39.94 tff(c_1639, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_subClassOf, S_5, O_6), true, true, true)=true))). % 53.39/39.94 tff(c_2039, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdfs_domain), true)=true))). % 53.39/39.94 tff(c_9349, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__2, uri_rdf__2)=true)). % 53.39/39.94 tff(c_9293, plain, (iext(uri_rdf_type, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 53.39/39.94 tff(c_9157, plain, (iext(uri_rdfs_subClassOf, uri_ex_d, uri_ex_d)=true)). % 53.39/39.94 tff(c_9095, plain, (iext(uri_rdfs_subClassOf, uri_ex_d, uri_rdfs_Resource)=true)). % 53.39/39.94 tff(c_8960, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Seq)=true)). % 53.39/39.94 tff(c_2478, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_96), true, icext(C_96, uri_rdf_Property), true)=true))). % 53.39/39.94 tff(c_8794, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__1, uri_rdf__1)=true)). % 53.39/39.94 tff(c_8701, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_first, uri_rdf_first)=true)). % 53.39/39.94 tff(c_8632, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Resource)=true)). % 53.39/39.94 tff(c_8564, plain, (ip(uri_rdfs_member)=true)). % 53.39/39.94 tff(c_2069, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdf_value), true)=true))). % 53.39/39.94 tff(c_8500, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__1, uri_rdfs_member)=true)). % 53.39/39.94 tff(c_8438, plain, (icext(uri_rdf_Property, uri_rdfs_domain)=true)). % 53.39/39.94 tff(c_2050, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdfs_domain), true)=true))). % 53.39/39.94 tff(c_2596, plain, (![S_5, O_6]: (ifeq(iext(uri_rdf_rest, S_5, O_6), true, true, true)=true))). % 53.39/39.94 tff(c_8323, plain, (icext(uri_rdf_List, sK5_testcase_premise_fullish_020_Logical_Complications_BNODE_li2)=true)). % 53.39/39.94 tff(c_8261, plain, (icext(uri_rdf_Property, uri_rdfs_isDefinedBy)=true)). % 53.39/39.94 tff(c_2494, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdf_rest, C_96), true, icext(C_96, sK5_testcase_premise_fullish_020_Logical_Complications_BNODE_li2), true)=true))). % 53.39/39.94 tff(c_8207, plain, (iext(uri_rdf_type, uri_rdfs_isDefinedBy, uri_rdf_Property)=true)). % 53.39/39.94 tff(c_8142, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, uri_rdfs_subClassOf)=true)). % 53.39/39.94 tff(c_2450, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdfs_Resource), true)=true))). % 53.39/39.94 tff(c_8048, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Resource)=true)). % 53.39/39.94 tff(c_7983, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdfs_ContainerMembershipProperty)=true)). % 53.39/39.94 tff(c_2491, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_96), true, icext(C_96, uri_rdfs_ContainerMembershipProperty), true)=true))). % 53.39/39.94 tff(c_7863, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_value, uri_rdf_value)=true)). % 53.39/39.94 tff(c_7811, plain, (icext(uri_rdf_Property, uri_rdfs_label)=true)). % 53.39/39.94 tff(c_7748, plain, (icext(uri_rdf_Property, uri_owl_disjointWith)=true)). % 53.39/39.94 tff(c_2070, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdfs_label), true)=true))). % 53.39/39.94 tff(c_7694, plain, (iext(uri_rdf_type, uri_owl_disjointWith, uri_rdf_Property)=true)). % 53.39/39.94 tff(c_7621, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdfs_Resource)=true)). % 53.39/39.94 tff(c_7552, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf)=true)). % 53.39/39.95 tff(c_7487, plain, (iext(uri_rdfs_subPropertyOf, uri_owl_complementOf, uri_owl_complementOf)=true)). % 53.39/39.95 tff(c_2054, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdfs_seeAlso), true)=true))). % 53.39/39.95 tff(c_7391, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_subject, uri_rdf_subject)=true)). % 53.39/39.95 tff(c_2437, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_96), true, icext(C_96, uri_rdfs_Resource), true)=true))). % 53.39/39.95 tff(c_7277, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdf_Property)=true)). % 53.39/39.95 tff(c_3698, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_subPropertyOf, S_5, O_6), true, true, true)=true))). % 53.39/39.95 tff(c_7175, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, uri_rdfs_domain)=true)). % 53.39/39.95 tff(c_2427, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdf_first, C_96), true, icext(C_96, uri_ex_c3), true)=true))). % 53.39/39.95 tff(c_7089, plain, (iext(uri_rdfs_subPropertyOf, uri_owl_disjointWith, uri_owl_disjointWith)=true)). % 53.39/39.95 tff(c_7003, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Resource)=true)). % 53.39/39.95 tff(c_6909, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdf_XMLLiteral)=true)). % 53.39/39.95 tff(c_6807, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdfs_Resource)=true)). % 53.39/39.95 tff(c_2030, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdf_subject), true)=true))). % 53.39/39.95 tff(c_6729, plain, (ic(uri_rdf_List)=true)). % 53.39/39.95 tff(c_6675, plain, (icext(uri_rdfs_Class, uri_rdf_List)=true)). % 53.39/39.95 tff(c_2474, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdf_List), true)=true))). % 53.39/39.95 tff(c_6587, plain, (iext(uri_rdfs_subClassOf, sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs, sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs)=true)). % 53.39/39.95 tff(c_6460, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__3, uri_rdf__3)=true)). % 53.39/39.95 tff(c_6405, plain, (icext(uri_rdf_Property, uri_rdfs_subPropertyOf)=true)). % 53.39/39.95 tff(c_2034, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdfs_subPropertyOf), true)=true))). % 53.39/39.95 tff(c_6264, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Resource)=true)). % 53.39/39.95 tff(c_2430, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_owl_unionOf, C_96), true, icext(C_96, sK2_testcase_premise_fullish_020_Logical_Complications_BNODE_lu1), true)=true))). % 53.39/39.95 tff(c_6155, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdfs_Class)=true)). % 53.39/39.95 tff(c_3356, plain, (![S_5, O_6]: (ifeq(iext(uri_rdf_object, S_5, O_6), true, true, true)=true))). % 53.39/39.95 tff(c_6088, plain, (icext(uri_rdf_Property, uri_rdfs_seeAlso)=true)). % 53.39/39.95 tff(c_1701, plain, (![X_89]: (ifeq(icext(uri_rdf_Bag, X_89), true, icext(uri_rdfs_Container, X_89), true)=true))). % 53.39/39.95 tff(c_6028, plain, (iext(uri_rdf_type, uri_rdfs_seeAlso, uri_rdf_Property)=true)). % 53.39/39.95 tff(c_5932, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdf_Bag)=true)). % 53.39/39.95 tff(c_1706, plain, (![X_89]: (ifeq(icext(uri_rdf_XMLLiteral, X_89), true, icext(uri_rdfs_Literal, X_89), true)=true))). % 53.39/39.95 tff(c_5859, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_seeAlso, uri_rdfs_seeAlso)=true)). % 53.39/39.95 tff(c_5774, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdfs_Literal)=true)). % 53.39/39.95 tff(c_5713, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_range, uri_rdfs_range)=true)). % 53.39/39.95 tff(c_1703, plain, (![X_89]: (ifeq(icext(uri_rdfs_Seq, X_89), true, icext(uri_rdfs_Container, X_89), true)=true))). % 53.39/39.95 tff(c_1402, plain, (![S_5, O_6]: (ifeq(iext(uri_owl_complementOf, S_5, O_6), true, true, true)=true))). % 53.39/39.95 tff(c_5643, plain, (icext(uri_rdfs_Class, uri_rdfs_Resource)=true)). % 53.39/39.95 tff(c_1707, plain, (![X_89]: (ifeq(icext(uri_ex_d, X_89), true, icext(sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs, X_89), true)=true))). % 53.39/39.95 tff(c_5570, plain, (ic(uri_rdfs_Resource)=true)). % 53.39/39.95 tff(c_1702, plain, (![X_89]: (ifeq(icext(uri_rdfs_ContainerMembershipProperty, X_89), true, icext(uri_rdf_Property, X_89), true)=true))). % 53.39/39.95 tff(c_5460, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Resource)=true)). % 53.39/39.95 tff(c_1704, plain, (![X_89]: (ifeq(icext(uri_rdf_Alt, X_89), true, icext(uri_rdfs_Container, X_89), true)=true))). % 53.39/39.95 tff(c_5345, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdf_Alt)=true)). % 53.39/39.95 tff(c_1705, plain, (![X_89]: (ifeq(icext(uri_rdfs_Datatype, X_89), true, icext(uri_rdfs_Class, X_89), true)=true))). % 53.39/39.95 tff(c_2068, plain, (![X_93, Y_94]: (ifeq(iext(uri_rdf_value, X_93, Y_94), true, true, true)=true))). % 53.39/39.95 tff(c_2100, plain, (![X_93, Y_94]: (ifeq(iext(uri_rdf__1, X_93, Y_94), true, true, true)=true))). % 53.39/39.95 tff(c_2104, plain, (![X_93, Y_94]: (ifeq(iext(uri_rdf_type, X_93, Y_94), true, true, true)=true))). % 53.39/39.95 tff(c_5129, plain, (![X_131]: (iext(uri_rdf_type, X_131, uri_rdfs_Resource)=true))). % 53.39/39.95 tff(c_2048, plain, (![X_93, Y_94]: (ifeq(iext(uri_rdfs_label, X_93, Y_94), true, true, true)=true))). % 53.39/39.95 tff(c_2108, plain, (![X_93, Y_94]: (ifeq(iext(uri_rdf__3, X_93, Y_94), true, true, true)=true))). % 53.39/39.95 tff(c_2041, plain, (![X_93, Y_94]: (ifeq(iext(uri_rdfs_member, X_93, Y_94), true, true, true)=true))). % 53.39/39.95 tff(c_2470, plain, (![X_97, Y_98]: (ifeq(iext(uri_rdf_predicate, X_97, Y_98), true, true, true)=true))). % 53.39/39.95 tff(c_2424, plain, (![X_97, Y_98]: (ifeq(iext(uri_rdf_subject, X_97, Y_98), true, true, true)=true))). % 53.39/39.95 tff(c_2486, plain, (![X_97, Y_98]: (ifeq(iext(uri_rdf__2, X_97, Y_98), true, true, true)=true))). % 53.39/39.95 tff(c_5027, plain, (icext(uri_rdfs_Class, uri_rdfs_ContainerMembershipProperty)=true)). % 53.39/39.95 tff(c_2436, plain, (![X_97, Y_98]: (ifeq(iext(uri_rdf_first, X_97, Y_98), true, true, true)=true))). % 53.39/39.95 tff(c_4960, plain, (icext(uri_rdfs_Class, sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs)=true)). % 53.39/39.95 tff(c_4917, plain, (icext(uri_rdfs_Class, uri_rdf_XMLLiteral)=true)). % 53.39/39.95 tff(c_4861, plain, (icext(uri_rdfs_Class, uri_rdfs_Datatype)=true)). % 53.39/39.95 tff(c_2438, plain, (![X_97, Y_98]: (ifeq(iext(uri_rdfs_seeAlso, X_97, Y_98), true, true, true)=true))). % 53.39/39.95 tff(c_4816, plain, (icext(uri_rdfs_Class, uri_rdfs_Class)=true)). % 53.39/39.95 tff(c_4770, plain, (icext(uri_rdfs_Class, uri_rdfs_Container)=true)). % 53.39/39.95 tff(c_2055, plain, (![X_93, Y_94]: (ifeq(iext(uri_rdfs_isDefinedBy, X_93, Y_94), true, true, true)=true))). % 53.39/39.95 tff(c_4709, plain, (icext(uri_rdfs_Class, uri_rdf_Bag)=true)). % 53.39/39.95 tff(c_4649, plain, (icext(uri_rdfs_Class, uri_ex_d)=true)). % 53.39/39.95 tff(c_2057, plain, (![X_93, Y_94]: (ifeq(iext(uri_rdfs_comment, X_93, Y_94), true, true, true)=true))). % 53.39/39.95 tff(c_4606, plain, (icext(uri_rdfs_Class, uri_rdfs_Literal)=true)). % 53.39/39.95 tff(c_4563, plain, (icext(uri_rdfs_Class, uri_rdfs_Seq)=true)). % 53.39/39.95 tff(c_4508, plain, (icext(uri_rdfs_Class, uri_rdf_Alt)=true)). % 53.39/39.95 tff(c_4451, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__3)=true)). % 53.39/39.95 tff(c_4413, plain, (icext(uri_rdf_Property, uri_rdf_value)=true)). % 53.39/39.95 tff(c_4374, plain, (icext(uri_rdf_Property, uri_rdf_type)=true)). % 53.39/39.95 tff(c_4336, plain, (icext(uri_rdf_Property, uri_rdf_subject)=true)). % 53.39/39.95 tff(c_4292, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__1)=true)). % 53.39/39.95 tff(c_4255, plain, (icext(uri_rdf_Property, uri_rdf__3)=true)). % 53.39/39.95 tff(c_4210, plain, (icext(uri_rdf_Property, uri_rdf__1)=true)). % 53.39/39.95 tff(c_4166, plain, (icext(uri_rdfs_Datatype, uri_rdf_XMLLiteral)=true)). % 53.39/39.95 tff(c_4117, plain, (icext(uri_rdfs_Class, uri_rdf_Property)=true)). % 53.39/39.95 tff(c_4077, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__2)=true)). % 53.39/39.95 tff(c_4037, plain, (icext(uri_rdf_Property, uri_rdf_rest)=true)). % 53.39/39.95 tff(c_3999, plain, (icext(uri_rdf_Property, uri_rdf_object)=true)). % 53.39/39.95 tff(c_3958, plain, (icext(uri_rdf_List, uri_rdf_nil)=true)). % 53.39/39.95 tff(c_3917, plain, (icext(uri_rdf_Property, uri_rdf__2)=true)). % 53.39/39.95 tff(c_3880, plain, (icext(uri_rdf_Property, uri_rdf_first)=true)). % 53.39/39.95 tff(c_3803, plain, (ip(uri_rdf__3)=true)). % 53.39/39.95 tff(c_3761, plain, (ip(uri_rdf_value)=true)). % 53.39/39.95 tff(c_3726, plain, (ic(uri_ex_d)=true)). % 53.39/39.95 tff(c_3683, plain, (ip(uri_rdfs_subPropertyOf)=true)). % 53.39/39.95 tff(c_3643, plain, (ip(uri_rdf__2)=true)). % 53.39/39.95 tff(c_3604, plain, (ip(uri_owl_unionOf)=true)). % 53.39/39.95 tff(c_3566, plain, (ip(uri_owl_disjointWith)=true)). % 53.39/39.95 tff(c_3531, plain, (ic(uri_rdfs_Datatype)=true)). % 53.39/39.95 tff(c_3491, plain, (ip(uri_rdf_subject)=true)). % 53.39/39.95 tff(c_3455, plain, (ic(uri_rdfs_ContainerMembershipProperty)=true)). % 53.39/39.95 tff(c_3418, plain, (ic(uri_rdf_XMLLiteral)=true)). % 53.39/39.95 tff(c_3378, plain, (ip(uri_rdf_first)=true)). % 53.39/39.95 tff(c_3339, plain, (ip(uri_rdf_object)=true)). % 53.39/39.95 tff(c_3279, plain, (ic(uri_rdfs_Seq)=true)). % 53.39/39.95 tff(c_3269, plain, (ip(uri_owl_intersectionOf)=true)). % 53.39/39.95 tff(c_3229, plain, (ip(uri_rdf__1)=true)). % 53.39/39.95 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))). % 53.39/39.95 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))). % 53.39/39.95 tff(c_2618, plain, (ic(uri_rdf_Alt)=true)). % 53.39/39.95 tff(c_2506, plain, (ip(uri_rdf_rest)=true)). % 53.39/39.95 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))). % 53.39/39.95 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))). % 53.39/39.95 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))). % 53.39/39.95 tff(c_1660, plain, (ic(uri_rdf_Bag)=true)). % 53.39/39.95 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))). % 53.39/39.95 tff(c_1624, plain, (ip(uri_rdfs_subClassOf)=true)). % 53.39/39.95 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))). % 53.39/39.95 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))). % 53.39/39.95 tff(c_1521, plain, (ip(uri_rdfs_range)=true)). % 53.39/39.95 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))). % 53.39/39.95 tff(c_1477, plain, (ip(uri_rdfs_domain)=true)). % 53.39/39.95 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))). % 53.39/39.95 tff(c_1387, plain, (ip(uri_owl_complementOf)=true)). % 53.39/39.95 tff(c_1303, plain, (ip(uri_rdf_type)=true)). % 53.39/39.95 tff(c_30, plain, (![P_10]: (ifeq(iext(uri_rdf_type, P_10, uri_rdf_Property), true, ip(P_10), true)=true))). % 53.39/39.95 tff(c_1216, plain, (ip(uri_rdfs_seeAlso)=true)). % 53.39/39.95 tff(c_152, plain, (![C_37, D_38]: (ifeq(iext(uri_rdfs_subClassOf, C_37, D_38), true, ic(C_37), true)=true))). % 53.39/39.95 tff(c_1184, plain, (ic(uri_rdfs_Class)=true)). % 53.39/39.95 tff(c_4, plain, (![P_4, S_5, O_6]: (ifeq(iext(P_4, S_5, O_6), true, ip(P_4), true)=true))). % 53.39/39.95 tff(c_901, plain, (ic(uri_rdf_Property)=true)). % 53.39/39.95 tff(c_162, plain, (![P_43, Q_44]: (ifeq(iext(uri_rdfs_subPropertyOf, P_43, Q_44), true, ip(Q_44), true)=true))). % 53.39/39.95 tff(c_844, plain, (ic(uri_rdfs_Literal)=true)). % 53.39/39.95 tff(c_812, plain, (ic(sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs)=true)). % 53.39/39.95 tff(c_58, plain, (![C_15]: (ifeq(ic(C_15), true, iext(uri_rdfs_subClassOf, C_15, uri_rdfs_Resource), true)=true))). % 53.39/39.95 tff(c_765, plain, (ic(uri_rdfs_Container)=true)). % 53.39/39.95 tff(c_150, plain, (![C_35, D_36]: (ifeq(iext(uri_rdfs_subClassOf, C_35, D_36), true, ic(D_36), true)=true))). % 53.39/39.95 tff(c_712, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, uri_rdfs_isDefinedBy)=true)). % 53.39/39.95 tff(c_679, plain, (ip(uri_rdfs_isDefinedBy)=true)). % 53.39/39.95 tff(c_170, plain, (![P_51]: (ifeq(ip(P_51), true, iext(uri_rdfs_subPropertyOf, P_51, P_51), true)=true))). % 53.39/39.95 tff(c_164, plain, (![P_45, Q_46]: (ifeq(iext(uri_rdfs_subPropertyOf, P_45, Q_46), true, ip(P_45), true)=true))). % 53.39/39.95 tff(c_156, plain, (![C_39]: (ifeq(ic(C_39), true, iext(uri_rdfs_subClassOf, C_39, C_39), true)=true))). % 53.39/39.95 tff(c_28, plain, (![P_9]: (ifeq(ip(P_9), true, iext(uri_rdf_type, P_9, uri_rdf_Property), true)=true))). % 53.39/39.95 tff(c_114, plain, (![X_22]: (ifeq(ic(X_22), true, icext(uri_rdfs_Class, X_22), true)=true))). % 53.39/39.95 tff(c_124, plain, (![X_27]: (ifeq(lv(X_27), true, icext(uri_rdfs_Literal, X_27), true)=true))). % 53.39/39.95 tff(c_122, plain, (![X_26]: (ifeq(icext(uri_rdfs_Literal, X_26), true, lv(X_26), true)=true))). % 53.39/39.95 tff(c_542, plain, (![X_60]: (icext(uri_rdfs_Resource, X_60)=true))). % 53.39/39.95 tff(c_116, plain, (![X_23]: (ifeq(icext(uri_rdfs_Class, X_23), true, ic(X_23), true)=true))). % 53.39/39.95 tff(c_217, plain, (![X_8]: (ifeq(lv(X_8), true, true, true)=true))). % 53.39/39.95 tff(c_2, plain, (![A_1, B_2, C_3]: (ifeq(A_1, A_1, B_2, C_3)=B_2))). % 53.39/39.95 tff(c_142, plain, (iext(uri_rdfs_domain, uri_rdf_subject, uri_rdfs_Statement)=true)). % 53.39/39.95 tff(c_176, plain, (iext(uri_rdfs_range, uri_rdf_type, uri_rdfs_Class)=true)). % 53.39/39.95 tff(c_212, plain, (iext(uri_rdfs_subClassOf, uri_ex_d, uri_ex_c3)!=true)). % 53.39/39.95 tff(c_204, plain, (iext(uri_rdf_first, sK3_testcase_premise_fullish_020_Logical_Complications_BNODE_lu2, uri_ex_c2)=true)). % 53.39/39.95 tff(c_26, plain, (iext(uri_rdf_type, uri_rdf_subject, uri_rdf_Property)=true)). % 53.39/39.95 tff(c_168, plain, (iext(uri_rdfs_range, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 53.39/39.95 tff(c_180, plain, (iext(uri_rdfs_range, uri_rdf_value, uri_rdfs_Resource)=true)). % 53.39/39.95 tff(c_14, plain, (iext(uri_rdf_type, uri_rdf_rest, uri_rdf_Property)=true)). % 53.39/39.95 tff(c_146, plain, (iext(uri_rdfs_domain, uri_rdfs_subClassOf, uri_rdfs_Class)=true)). % 53.39/39.95 tff(c_70, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Container)=true)). % 53.39/39.95 tff(c_112, plain, (iext(uri_rdfs_range, uri_rdfs_domain, uri_rdfs_Class)=true)). % 53.39/39.95 tff(c_144, plain, (iext(uri_rdfs_range, uri_rdf_subject, uri_rdfs_Resource)=true)). % 53.39/39.95 tff(c_76, plain, (iext(uri_rdfs_domain, uri_rdfs_member, uri_rdfs_Resource)=true)). % 53.39/39.95 tff(c_200, plain, (iext(uri_rdf_first, sK1_testcase_premise_fullish_020_Logical_Complications_BNODE_lu3, uri_ex_c3)=true)). % 53.39/39.95 tff(c_38, plain, (iext(uri_rdfs_range, uri_rdfs_comment, uri_rdfs_Literal)=true)). % 53.39/39.95 tff(c_134, plain, (iext(uri_rdfs_domain, uri_rdf_object, uri_rdfs_Statement)=true)). % 53.39/39.95 tff(c_188, plain, (iext(uri_owl_unionOf, uri_ex_c, sK2_testcase_premise_fullish_020_Logical_Complications_BNODE_lu1)=true)). % 53.39/39.95 tff(c_20, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdf_Property)=true)). % 53.39/39.95 tff(c_46, plain, (iext(uri_rdfs_domain, uri_rdfs_label, uri_rdfs_Resource)=true)). % 53.39/39.95 tff(c_108, plain, (iext(uri_rdfs_domain, uri_rdfs_domain, uri_rdf_Property)=true)). % 53.39/39.95 tff(c_94, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdfs_ContainerMembershipProperty)=true)). % 53.39/39.95 tff(c_16, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdf_Property)=true)). % 53.39/39.95 tff(c_62, plain, (iext(uri_rdfs_range, uri_rdf_first, uri_rdfs_Resource)=true)). % 53.39/39.95 tff(c_52, plain, (iext(uri_rdfs_range, uri_rdfs_seeAlso, uri_rdfs_Resource)=true)). % 53.39/39.95 tff(c_40, plain, (iext(uri_rdfs_domain, uri_rdfs_isDefinedBy, uri_rdfs_Resource)=true)). % 53.39/39.95 tff(c_36, plain, (iext(uri_rdfs_domain, uri_rdfs_comment, uri_rdfs_Resource)=true)). % 53.39/39.95 tff(c_64, plain, (iext(uri_rdfs_domain, uri_rdf_rest, uri_rdf_List)=true)). % 53.39/39.95 tff(c_74, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property)=true)). % 53.39/39.95 tff(c_102, plain, (iext(uri_rdf_type, uri_rdf_XMLLiteral, uri_rdfs_Datatype)=true)). % 53.39/39.95 tff(c_50, plain, (iext(uri_rdfs_domain, uri_rdfs_seeAlso, uri_rdfs_Resource)=true)). % 53.39/39.95 tff(c_12, plain, (iext(uri_rdf_type, uri_rdf_nil, uri_rdf_List)=true)). % 53.39/39.95 tff(c_138, plain, (iext(uri_rdfs_domain, uri_rdf_predicate, uri_rdfs_Statement)=true)). % 53.39/39.95 tff(c_192, plain, (iext(uri_rdf_rest, sK2_testcase_premise_fullish_020_Logical_Complications_BNODE_lu1, sK3_testcase_premise_fullish_020_Logical_Complications_BNODE_lu2)=true)). % 53.39/39.95 tff(c_10, plain, (iext(uri_rdf_type, uri_rdf_first, uri_rdf_Property)=true)). % 53.39/39.95 tff(c_178, plain, (iext(uri_rdfs_domain, uri_rdf_value, uri_rdfs_Resource)=true)). % 53.39/39.95 tff(c_48, plain, (iext(uri_rdfs_range, uri_rdfs_label, uri_rdfs_Literal)=true)). % 53.39/39.95 tff(c_22, plain, (iext(uri_rdf_type, uri_rdf_object, uri_rdf_Property)=true)). % 53.39/39.95 tff(c_160, plain, (iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 53.39/39.95 tff(c_18, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdf_Property)=true)). % 53.39/39.95 tff(c_86, plain, (iext(uri_rdfs_range, uri_rdf__1, uri_rdfs_Resource)=true)). % 53.39/39.95 tff(c_82, plain, (iext(uri_rdfs_domain, uri_rdf__2, uri_rdfs_Resource)=true)). % 53.39/39.95 tff(c_196, plain, (iext(uri_rdf_rest, sK5_testcase_premise_fullish_020_Logical_Complications_BNODE_li2, uri_rdf_nil)=true)). % 53.39/39.95 tff(c_208, plain, (iext(uri_rdf_first, sK7_testcase_premise_fullish_020_Logical_Complications_BNODE_li1, uri_ex_c)=true)). % 53.39/39.95 tff(c_126, plain, (iext(uri_rdf_type, uri_rdf_Property, uri_rdfs_Class)=true)). % 53.39/39.95 tff(c_42, plain, (iext(uri_rdfs_range, uri_rdfs_isDefinedBy, uri_rdfs_Resource)=true)). % 53.39/39.95 tff(c_128, plain, (iext(uri_rdfs_domain, uri_rdfs_range, uri_rdf_Property)=true)). % 53.39/39.95 tff(c_202, plain, (iext(uri_rdf_first, sK2_testcase_premise_fullish_020_Logical_Complications_BNODE_lu1, uri_ex_c1)=true)). % 53.39/39.95 tff(c_98, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Container)=true)). % 53.39/39.95 tff(c_66, plain, (iext(uri_rdfs_range, uri_rdf_rest, uri_rdf_List)=true)). % 53.39/39.95 tff(c_90, plain, (iext(uri_rdfs_range, uri_rdf__3, uri_rdfs_Resource)=true)). % 53.39/39.95 tff(c_92, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdfs_ContainerMembershipProperty)=true)). % 53.39/39.95 tff(c_140, plain, (iext(uri_rdfs_range, uri_rdf_predicate, uri_rdfs_Resource)=true)). % 53.39/39.95 tff(c_68, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Container)=true)). % 53.39/39.95 tff(c_106, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Class)=true)). % 53.39/39.95 tff(c_60, plain, (iext(uri_rdfs_domain, uri_rdf_first, uri_rdf_List)=true)). % 53.39/39.95 tff(c_154, plain, (iext(uri_rdfs_range, uri_rdfs_subClassOf, uri_rdfs_Class)=true)). % 53.39/39.95 tff(c_186, plain, (iext(uri_owl_disjointWith, uri_ex_d, uri_ex_c1)=true)). % 53.39/39.95 tff(c_44, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso)=true)). % 53.39/39.95 tff(c_34, plain, (iext(uri_rdf_type, uri_rdf_type, uri_rdf_Property)=true)). % 53.39/39.95 tff(c_184, plain, (iext(uri_owl_intersectionOf, sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs, sK7_testcase_premise_fullish_020_Logical_Complications_BNODE_li1)=true)). % 53.39/39.95 tff(c_24, plain, (iext(uri_rdf_type, uri_rdf_value, uri_rdf_Property)=true)). % 53.39/39.95 tff(c_194, plain, (iext(uri_rdf_rest, sK3_testcase_premise_fullish_020_Logical_Complications_BNODE_lu2, sK1_testcase_premise_fullish_020_Logical_Complications_BNODE_lu3)=true)). % 53.39/39.95 tff(c_190, plain, (iext(uri_rdf_rest, sK1_testcase_premise_fullish_020_Logical_Complications_BNODE_lu3, uri_rdf_nil)=true)). % 53.39/39.95 tff(c_78, plain, (iext(uri_rdfs_range, uri_rdfs_member, uri_rdfs_Resource)=true)). % 53.39/39.95 tff(c_80, plain, (iext(uri_rdfs_domain, uri_rdf__1, uri_rdfs_Resource)=true)). % 53.39/39.95 tff(c_88, plain, (iext(uri_rdfs_range, uri_rdf__2, uri_rdfs_Resource)=true)). % 53.39/39.95 tff(c_100, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Literal)=true)). % 53.39/39.95 tff(c_174, plain, (iext(uri_rdfs_domain, uri_rdf_type, uri_rdfs_Resource)=true)). % 53.39/39.95 tff(c_132, plain, (iext(uri_rdfs_range, uri_rdfs_range, uri_rdfs_Class)=true)). % 53.39/39.95 tff(c_96, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdfs_ContainerMembershipProperty)=true)). % 53.39/39.95 tff(c_84, plain, (iext(uri_rdfs_domain, uri_rdf__3, uri_rdfs_Resource)=true)). % 53.39/39.95 tff(c_182, plain, (iext(uri_owl_complementOf, sK4_testcase_premise_fullish_020_Logical_Complications_BNODE_xc, uri_ex_c2)=true)). % 53.39/39.95 tff(c_198, plain, (iext(uri_rdf_rest, sK7_testcase_premise_fullish_020_Logical_Complications_BNODE_li1, sK5_testcase_premise_fullish_020_Logical_Complications_BNODE_li2)=true)). % 53.39/39.95 tff(c_206, plain, (iext(uri_rdf_first, sK5_testcase_premise_fullish_020_Logical_Complications_BNODE_li2, sK4_testcase_premise_fullish_020_Logical_Complications_BNODE_xc)=true)). % 53.39/39.95 tff(c_210, plain, (iext(uri_rdfs_subClassOf, uri_ex_d, sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs)=true)). % 53.39/39.95 tff(c_6, plain, (![X_7]: (ir(X_7)=true))). % 53.39/39.95 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 53.39/39.95 %------------------------------------------------------------------------------