%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SWB013-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/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n013.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:49 PM UTC 2025 % Result : Satisfiable 43.17s 30.88s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SWB013-10 : TPTP v9.0.0. Released v7.3.0. % 0.11/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.13/0.34 % Computer : n013.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:55:47 EDT 2025 % 0.13/0.34 % CPUTime : % 43.17/30.88 % 43.17/30.88 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 43.17/30.88 % 43.17/30.88 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 43.23/30.90 %$ 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_someValuesFrom > uri_owl_sameAs > uri_owl_propertyChainAxiom > uri_owl_onProperty > uri_owl_inverseOf > uri_owl_Restriction > uri_owl_ObjectProperty > uri_owl_Class > uri_foaf_knows > uri_ex_sameCliqueAs > uri_ex_bob > uri_ex_alice > uri_ex_JoesGang > uri_ex_Clique > true > sK5_testcase_premise_fullish_013_Cliques_BNODE_r > sK4_testcase_premise_fullish_013_Cliques_BNODE_l3 > sK3_testcase_premise_fullish_013_Cliques_BNODE_i > sK2_testcase_premise_fullish_013_Cliques_BNODE_l2 > sK1_testcase_premise_fullish_013_Cliques_BNODE_l1 % 43.23/30.90 % 43.23/30.90 %Foreground sorts: % 43.23/30.90 % 43.23/30.90 % 43.23/30.90 %Background operators: % 43.23/30.90 % 43.23/30.90 % 43.23/30.90 %Foreground operators: % 43.23/30.90 tff(uri_rdfs_Datatype, type, uri_rdfs_Datatype: $i). % 43.23/30.90 tff(uri_rdfs_ContainerMembershipProperty, type, uri_rdfs_ContainerMembershipProperty: $i). % 43.23/30.90 tff(uri_rdfs_Resource, type, uri_rdfs_Resource: $i). % 43.23/30.90 tff(uri_rdf_Property, type, uri_rdf_Property: $i). % 43.23/30.90 tff(uri_rdf_subject, type, uri_rdf_subject: $i). % 43.23/30.90 tff(uri_rdf_type, type, uri_rdf_type: $i). % 43.23/30.90 tff(uri_owl_onProperty, type, uri_owl_onProperty: $i). % 43.23/30.90 tff(uri_rdfs_subPropertyOf, type, uri_rdfs_subPropertyOf: $i). % 43.23/30.90 tff(uri_ex_Clique, type, uri_ex_Clique: $i). % 43.23/30.90 tff(uri_rdfs_seeAlso, type, uri_rdfs_seeAlso: $i). % 43.23/30.90 tff(icext, type, icext: ($i * $i) > $i). % 43.23/30.90 tff(uri_rdfs_range, type, uri_rdfs_range: $i). % 43.23/30.90 tff(uri_rdf_XMLLiteral, type, uri_rdf_XMLLiteral: $i). % 43.23/30.90 tff(uri_rdf_List, type, uri_rdf_List: $i). % 43.23/30.90 tff(sK3_testcase_premise_fullish_013_Cliques_BNODE_i, type, sK3_testcase_premise_fullish_013_Cliques_BNODE_i: $i). % 43.23/30.90 tff(uri_ex_JoesGang, type, uri_ex_JoesGang: $i). % 43.23/30.90 tff(uri_rdf_first, type, uri_rdf_first: $i). % 43.23/30.90 tff(uri_rdf_predicate, type, uri_rdf_predicate: $i). % 43.23/30.90 tff(sK1_testcase_premise_fullish_013_Cliques_BNODE_l1, type, sK1_testcase_premise_fullish_013_Cliques_BNODE_l1: $i). % 43.23/30.90 tff(ir, type, ir: $i > $i). % 43.23/30.90 tff(lv, type, lv: $i > $i). % 43.23/30.90 tff(uri_owl_inverseOf, type, uri_owl_inverseOf: $i). % 43.23/30.90 tff(uri_ex_bob, type, uri_ex_bob: $i). % 43.23/30.90 tff(uri_rdf__3, type, uri_rdf__3: $i). % 43.23/30.90 tff(uri_rdf_value, type, uri_rdf_value: $i). % 43.23/30.90 tff(uri_ex_sameCliqueAs, type, uri_ex_sameCliqueAs: $i). % 43.23/30.90 tff(ic, type, ic: $i > $i). % 43.23/30.90 tff(uri_rdfs_Statement, type, uri_rdfs_Statement: $i). % 43.23/30.90 tff(uri_rdf__1, type, uri_rdf__1: $i). % 43.23/30.90 tff(iext, type, iext: ($i * $i * $i) > $i). % 43.23/30.90 tff(uri_owl_Restriction, type, uri_owl_Restriction: $i). % 43.23/30.90 tff(uri_ex_alice, type, uri_ex_alice: $i). % 43.23/30.90 tff(uri_rdf_rest, type, uri_rdf_rest: $i). % 43.23/30.90 tff(uri_rdfs_label, type, uri_rdfs_label: $i). % 43.23/30.90 tff(uri_rdfs_Container, type, uri_rdfs_Container: $i). % 43.23/30.90 tff(uri_owl_propertyChainAxiom, type, uri_owl_propertyChainAxiom: $i). % 43.23/30.90 tff(uri_owl_ObjectProperty, type, uri_owl_ObjectProperty: $i). % 43.23/30.90 tff(uri_rdfs_subClassOf, type, uri_rdfs_subClassOf: $i). % 43.23/30.90 tff(uri_owl_sameAs, type, uri_owl_sameAs: $i). % 43.23/30.90 tff(uri_rdf_object, type, uri_rdf_object: $i). % 43.23/30.90 tff(sK2_testcase_premise_fullish_013_Cliques_BNODE_l2, type, sK2_testcase_premise_fullish_013_Cliques_BNODE_l2: $i). % 43.23/30.90 tff(ip, type, ip: $i > $i). % 43.23/30.90 tff(uri_rdfs_Class, type, uri_rdfs_Class: $i). % 43.23/30.90 tff(uri_rdfs_Seq, type, uri_rdfs_Seq: $i). % 43.23/30.90 tff(uri_owl_Class, type, uri_owl_Class: $i). % 43.23/30.90 tff(uri_rdfs_member, type, uri_rdfs_member: $i). % 43.23/30.90 tff(uri_rdf_Bag, type, uri_rdf_Bag: $i). % 43.23/30.90 tff(uri_rdf__2, type, uri_rdf__2: $i). % 43.23/30.90 tff(sK4_testcase_premise_fullish_013_Cliques_BNODE_l3, type, sK4_testcase_premise_fullish_013_Cliques_BNODE_l3: $i). % 43.23/30.90 tff(uri_foaf_knows, type, uri_foaf_knows: $i). % 43.23/30.90 tff(uri_rdfs_comment, type, uri_rdfs_comment: $i). % 43.23/30.90 tff(uri_rdfs_Literal, type, uri_rdfs_Literal: $i). % 43.23/30.90 tff(true, type, true: $i). % 43.23/30.90 tff(uri_owl_someValuesFrom, type, uri_owl_someValuesFrom: $i). % 43.23/30.90 tff(uri_rdf_Alt, type, uri_rdf_Alt: $i). % 43.23/30.90 tff(uri_rdf_nil, type, uri_rdf_nil: $i). % 43.23/30.90 tff(sK5_testcase_premise_fullish_013_Cliques_BNODE_r, type, sK5_testcase_premise_fullish_013_Cliques_BNODE_r: $i). % 43.23/30.90 tff(uri_rdfs_isDefinedBy, type, uri_rdfs_isDefinedBy: $i). % 43.23/30.90 tff(uri_rdfs_domain, type, uri_rdfs_domain: $i). % 43.23/30.90 tff(ifeq, type, ifeq: ($i * $i * $i * $i) > $i). % 43.23/30.90 % 43.23/30.90 %Saturated clause set: % 43.23/30.90 tff(c_17484, 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))). % 43.23/30.90 tff(c_17810, 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))). % 43.23/30.90 tff(c_17487, 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))). % 43.23/30.90 tff(c_102076, plain, (![X_1555, Y_1556]: (ifeq(iext(uri_rdfs_label, X_1555, Y_1556), true, iext(uri_rdfs_label, X_1555, Y_1556), true)=true))). % 43.23/30.90 tff(c_17748, 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))). % 43.23/30.90 tff(c_101907, plain, (![X_1550, Y_1551]: (ifeq(iext(uri_rdf_predicate, X_1550, Y_1551), true, iext(uri_rdf_predicate, X_1550, Y_1551), true)=true))). % 43.23/30.90 tff(c_17356, 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))). % 43.23/30.90 tff(c_17429, 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))). % 43.23/30.90 tff(c_19622, 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))). % 43.23/30.90 tff(c_6078, 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))). % 43.23/30.90 tff(c_6075, 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))). % 43.23/30.90 tff(c_17650, 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))). % 43.23/30.90 tff(c_19687, 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))). % 43.23/30.90 tff(c_100716, plain, (![X_1537, Y_1538]: (ifeq(iext(uri_rdfs_member, X_1537, Y_1538), true, iext(uri_rdfs_member, X_1537, Y_1538), true)=true))). % 43.23/30.90 tff(c_100688, plain, (![X_1533, Y_1534]: (ifeq(iext(uri_rdfs_comment, X_1533, Y_1534), true, iext(uri_rdfs_comment, X_1533, Y_1534), true)=true))). % 43.23/30.90 tff(c_22885, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_owl_Restriction, uri_owl_Restriction), true, true, true), true)=true))). % 43.23/30.90 tff(c_100361, plain, (![C_1530]: (ifeq(iext(uri_rdfs_subClassOf, C_1530, uri_owl_ObjectProperty), true, iext(uri_rdfs_subClassOf, C_1530, uri_rdfs_Resource), true)=true))). % 43.23/30.90 tff(c_22951, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_owl_Restriction, uri_rdfs_Resource), true, true, true), true)=true))). % 43.23/30.90 tff(c_100029, plain, (![C_1527]: (ifeq(iext(uri_rdfs_subClassOf, C_1527, uri_rdfs_Statement), true, iext(uri_rdfs_subClassOf, C_1527, uri_rdfs_Resource), true)=true))). % 43.23/30.90 tff(c_20135, 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))). % 43.23/30.90 tff(c_18388, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_owl_ObjectProperty, uri_rdfs_Resource), true, true, true), true)=true))). % 43.23/30.90 tff(c_99551, plain, (![C_1523]: (ifeq(iext(uri_rdfs_subClassOf, C_1523, uri_ex_JoesGang), true, iext(uri_rdfs_subClassOf, C_1523, uri_rdfs_Resource), true)=true))). % 43.23/30.90 tff(c_18322, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_owl_ObjectProperty, uri_owl_ObjectProperty), true, true, true), true)=true))). % 43.23/30.90 tff(c_24384, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_owl_Class, uri_owl_Class), true, true, true), true)=true))). % 43.23/30.90 tff(c_24450, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_owl_Class, uri_rdfs_Resource), true, true, true), true)=true))). % 43.23/30.91 tff(c_20069, 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))). % 43.23/30.91 tff(c_17072, 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))). % 43.23/30.91 tff(c_98659, plain, (![C_1516]: (ifeq(iext(uri_rdfs_subClassOf, C_1516, uri_rdf_List), true, iext(uri_rdfs_subClassOf, C_1516, uri_rdfs_Resource), true)=true))). % 43.23/30.91 tff(c_21198, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_ex_JoesGang, uri_rdfs_Resource), true, true, true), true)=true))). % 43.23/30.91 tff(c_17138, 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))). % 43.23/30.91 tff(c_21107, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_ex_JoesGang, uri_ex_JoesGang), true, true, true), true)=true))). % 43.23/30.91 tff(c_98040, plain, (![C_1511]: (ifeq(iext(uri_rdfs_subClassOf, C_1511, uri_owl_Restriction), true, iext(uri_rdfs_subClassOf, C_1511, uri_rdfs_Resource), true)=true))). % 43.23/30.91 tff(c_97853, plain, (![C_1509]: (ifeq(iext(uri_rdfs_subClassOf, C_1509, uri_owl_Class), true, iext(uri_rdfs_subClassOf, C_1509, uri_rdfs_Resource), true)=true))). % 43.23/30.91 tff(c_16848, 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))). % 43.23/30.91 tff(c_14703, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_ex_sameCliqueAs), true, true, true), true)=true))). % 43.23/30.91 tff(c_16503, 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))). % 43.23/30.91 tff(c_17025, 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))). % 43.23/30.91 tff(c_16406, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_ex_Clique, uri_rdfs_Class), true, true, true), true)=true))). % 43.23/30.91 tff(c_11103, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_owl_onProperty), true, true, true), true)=true))). % 43.23/30.91 tff(c_16895, 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))). % 43.23/30.91 tff(c_7546, 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))). % 43.23/30.91 tff(c_6719, 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))). % 43.23/30.91 tff(c_14706, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_ex_sameCliqueAs, Y_21), true, true, true), true)=true))). % 43.23/30.91 tff(c_11745, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_owl_sameAs, Y_21), true, true, true), true)=true))). % 43.23/30.91 tff(c_12460, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_owl_inverseOf, Y_21), true, true, true), true)=true))). % 43.23/30.91 tff(c_12638, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_owl_propertyChainAxiom, Y_21), true, true, true), true)=true))). % 43.23/30.91 tff(c_16671, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, sK5_testcase_premise_fullish_013_Cliques_BNODE_r, uri_rdfs_Class), true, true, true), true)=true))). % 43.23/30.91 tff(c_16624, 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))). % 43.23/30.91 tff(c_11742, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_owl_sameAs), true, true, true), true)=true))). % 43.23/30.91 tff(c_8141, 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))). % 43.23/30.91 tff(c_10398, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_owl_someValuesFrom, Y_21), true, true, true), true)=true))). % 43.23/30.91 tff(c_16550, 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))). % 43.23/30.91 tff(c_12214, 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))). % 43.23/30.91 tff(c_12217, 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))). % 43.23/30.91 tff(c_16453, 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))). % 43.23/30.91 tff(c_7543, 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))). % 43.23/30.91 tff(c_16753, 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))). % 43.23/30.91 tff(c_8138, 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))). % 43.23/30.91 tff(c_16800, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_ex_JoesGang, sK5_testcase_premise_fullish_013_Cliques_BNODE_r), true, true, true), true)=true))). % 43.23/30.91 tff(c_12457, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_owl_inverseOf), true, true, true), true)=true))). % 43.23/30.91 tff(c_6716, 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))). % 43.23/30.91 tff(c_12635, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_owl_propertyChainAxiom), true, true, true), true)=true))). % 43.23/30.91 tff(c_11106, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_owl_onProperty, Y_21), true, true, true), true)=true))). % 43.23/30.91 tff(c_16946, 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))). % 43.23/30.91 tff(c_10395, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_owl_someValuesFrom), true, true, true), true)=true))). % 43.23/30.91 tff(c_21781, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, sK1_testcase_premise_fullish_013_Cliques_BNODE_l1, uri_rdf_List), true, true, true), true)=true))). % 43.23/30.91 tff(c_18275, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_owl_ObjectProperty, uri_rdfs_Class), true, true, true), true)=true))). % 43.23/30.91 tff(c_22813, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_owl_Restriction, uri_rdfs_Class), true, true, true), true)=true))). % 43.23/30.91 tff(c_16120, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, sK4_testcase_premise_fullish_013_Cliques_BNODE_l3, uri_rdf_List), true, true, true), true)=true))). % 43.23/30.91 tff(c_20022, 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))). % 43.23/30.91 tff(c_16167, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, sK2_testcase_premise_fullish_013_Cliques_BNODE_l2, uri_rdf_List), true, true, true), true)=true))). % 43.23/30.91 tff(c_24337, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_owl_Class, uri_rdfs_Class), true, true, true), true)=true))). % 43.23/30.91 tff(c_20920, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_ex_JoesGang, uri_rdfs_Class), true, true, true), true)=true))). % 43.23/30.91 tff(c_16286, 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))). % 43.23/30.91 tff(c_16239, 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))). % 43.23/30.91 tff(c_91707, plain, (![X_1443, Y_1444]: (ifeq(iext(uri_rdf_subject, X_1443, Y_1444), true, iext(uri_rdf_subject, X_1443, Y_1444), true)=true))). % 43.23/30.91 tff(c_5245, 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))). % 43.23/30.91 tff(c_9989, 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))). % 43.23/30.91 tff(c_11688, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_owl_sameAs, uri_rdf_Property), true, true, true), true)=true))). % 43.23/30.91 tff(c_13144, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_ex_Clique, uri_ex_Clique), true, true, true), true)=true))). % 43.23/30.91 tff(c_8575, 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))). % 43.23/30.91 tff(c_90967, plain, (![X_1433, Y_1434]: (ifeq(iext(uri_rdf__3, X_1433, Y_1434), true, iext(uri_rdfs_member, X_1433, Y_1434), true)=true))). % 43.23/30.91 tff(c_90892, plain, (![X_1429, Y_1430]: (ifeq(iext(uri_rdf_first, X_1429, Y_1430), true, iext(uri_rdf_first, X_1429, Y_1430), true)=true))). % 43.23/30.91 tff(c_8059, 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))). % 43.23/30.91 tff(c_5062, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, uri_ex_Clique, Y_21), true, true, true), true)=true))). % 43.23/30.91 tff(c_15118, 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))). % 43.23/30.92 tff(c_15248, 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))). % 43.23/30.92 tff(c_90283, plain, (![X_1420, Y_1421]: (ifeq(iext(uri_rdf__1, X_1420, Y_1421), true, iext(uri_rdfs_member, X_1420, Y_1421), true)=true))). % 43.23/30.92 tff(c_13233, 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))). % 43.23/30.92 tff(c_5716, 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))). % 43.23/30.92 tff(c_89671, plain, (![X_1414, Y_1415]: (ifeq(iext(uri_rdfs_range, X_1414, Y_1415), true, iext(uri_rdfs_range, X_1414, Y_1415), true)=true))). % 43.23/30.92 tff(c_89484, plain, (![C_1412]: (ifeq(iext(uri_rdfs_subClassOf, C_1412, uri_rdfs_Seq), true, iext(uri_rdfs_subClassOf, C_1412, uri_rdfs_Resource), true)=true))). % 43.23/30.92 tff(c_6152, 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))). % 43.23/30.92 tff(c_15182, 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))). % 43.23/30.92 tff(c_9010, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_owl_onProperty, uri_owl_onProperty), true, true, true), true)=true))). % 43.23/30.92 tff(c_14883, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_owl_inverseOf, uri_owl_inverseOf), true, true, true), true)=true))). % 43.23/30.92 tff(c_14174, 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))). % 43.23/30.92 tff(c_5102, 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))). % 43.23/30.92 tff(c_11462, 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))). % 43.23/30.92 tff(c_7656, 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))). % 43.23/30.92 tff(c_14649, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_ex_sameCliqueAs, uri_rdf_Property), true, true, true), true)=true))). % 43.23/30.92 tff(c_5105, 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))). % 43.23/30.92 tff(c_87858, plain, (![C_1398]: (ifeq(iext(uri_rdfs_subClassOf, C_1398, uri_rdfs_ContainerMembershipProperty), true, iext(uri_rdfs_subClassOf, C_1398, uri_rdfs_Resource), true)=true))). % 43.23/30.92 tff(c_14000, 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))). % 43.23/30.92 tff(c_6339, 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))). % 43.23/30.92 tff(c_11226, 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))). % 43.23/30.92 tff(c_87345, plain, (![P_1391]: (ifeq(iext(uri_rdfs_subPropertyOf, P_1391, uri_rdf__3), true, iext(uri_rdfs_subPropertyOf, P_1391, uri_rdfs_member), true)=true))). % 43.23/30.92 tff(c_87324, plain, (![X_1389, Y_1390]: (ifeq(iext(uri_owl_inverseOf, X_1389, Y_1390), true, iext(uri_owl_inverseOf, X_1389, Y_1390), true)=true))). % 43.23/30.92 tff(c_16058, 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))). % 43.23/30.92 tff(c_14449, 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))). % 43.23/30.92 tff(c_86996, plain, (![X_1383, Y_1384]: (ifeq(iext(uri_owl_propertyChainAxiom, X_1383, Y_1384), true, iext(uri_owl_propertyChainAxiom, X_1383, Y_1384), true)=true))). % 43.23/30.92 tff(c_86968, plain, (![X_1379, Y_1380]: (ifeq(iext(uri_rdf__3, X_1379, Y_1380), true, iext(uri_rdf__3, X_1379, Y_1380), true)=true))). % 43.23/30.92 tff(c_86781, plain, (![C_1377]: (ifeq(iext(uri_rdfs_subClassOf, C_1377, uri_rdf_Bag), true, iext(uri_rdfs_subClassOf, C_1377, uri_rdfs_Resource), true)=true))). % 43.23/30.92 tff(c_86754, plain, (![X_1373, Y_1374]: (ifeq(iext(uri_rdfs_isDefinedBy, X_1373, Y_1374), true, iext(uri_rdfs_isDefinedBy, X_1373, Y_1374), true)=true))). % 43.23/30.92 tff(c_5154, 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))). % 43.23/30.92 tff(c_9696, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_owl_someValuesFrom, uri_owl_someValuesFrom), true, true, true), true)=true))). % 43.23/30.92 tff(c_5396, 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))). % 43.23/30.92 tff(c_14280, 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))). % 43.23/30.92 tff(c_11858, 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))). % 43.23/30.92 tff(c_7492, 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))). % 43.23/30.92 tff(c_19496, 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))). % 43.23/30.92 tff(c_84728, plain, (![X_1360, Y_1361]: (ifeq(iext(uri_rdf_type, X_1360, Y_1361), true, iext(uri_rdf_type, X_1360, Y_1361), true)=true))). % 43.23/30.92 tff(c_84685, plain, (![X_1356, Y_1357]: (ifeq(iext(uri_owl_onProperty, X_1356, Y_1357), true, iext(uri_owl_onProperty, X_1356, Y_1357), true)=true))). % 43.23/30.92 tff(c_84498, plain, (![C_1354]: (ifeq(iext(uri_rdfs_subClassOf, C_1354, uri_rdf_XMLLiteral), true, iext(uri_rdfs_subClassOf, C_1354, uri_rdfs_Resource), true)=true))). % 43.23/30.92 tff(c_83811, plain, (![X_1350, Y_1351]: (ifeq(iext(uri_rdfs_subPropertyOf, X_1350, Y_1351), true, iext(uri_rdfs_subPropertyOf, X_1350, Y_1351), true)=true))). % 43.23/30.92 tff(c_13298, 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))). % 43.23/30.92 tff(c_5248, 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))). % 43.23/30.92 tff(c_82618, plain, (![C_1341]: (ifeq(iext(uri_rdfs_subClassOf, C_1341, uri_rdfs_Literal), true, iext(uri_rdfs_subClassOf, C_1341, uri_rdfs_Resource), true)=true))). % 43.23/30.92 tff(c_11025, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_owl_onProperty, uri_rdf_Property), true, true, true), true)=true))). % 43.23/30.92 tff(c_8509, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_ex_sameCliqueAs, uri_ex_sameCliqueAs), true, true, true), true)=true))). % 43.23/30.92 tff(c_5299, 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))). % 43.23/30.92 tff(c_5302, 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))). % 43.23/30.92 tff(c_5203, 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))). % 43.23/30.92 tff(c_13638, 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))). % 43.23/30.92 tff(c_4916, 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))). % 43.23/30.92 tff(c_12403, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_owl_inverseOf, uri_rdf_Property), true, true, true), true)=true))). % 43.23/30.92 tff(c_81156, plain, (![C_1327]: (ifeq(iext(uri_rdfs_subClassOf, C_1327, uri_rdf_Alt), true, iext(uri_rdfs_subClassOf, C_1327, uri_rdfs_Resource), true)=true))). % 43.23/30.92 tff(c_6923, 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))). % 43.23/30.92 tff(c_7152, 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))). % 43.23/30.92 tff(c_6022, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, sK5_testcase_premise_fullish_013_Cliques_BNODE_r), true, ifeq(iext(P_28, X_30, uri_ex_JoesGang), true, true, true), true)=true))). % 43.23/30.92 tff(c_80541, plain, (![C_1321]: (ifeq(iext(uri_rdfs_subClassOf, C_1321, uri_ex_Clique), true, iext(uri_rdfs_subClassOf, C_1321, uri_rdfs_Resource), true)=true))). % 43.23/30.92 tff(c_9901, 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))). % 43.23/30.92 tff(c_5779, 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))). % 43.23/30.92 tff(c_12341, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_owl_sameAs, uri_owl_sameAs), true, true, true), true)=true))). % 43.23/30.92 tff(c_5015, 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))). % 43.23/30.92 tff(c_9068, 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))). % 43.23/30.92 tff(c_5200, 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))). % 43.23/30.92 tff(c_79121, plain, (![C_1309]: (ifeq(iext(uri_rdfs_subClassOf, C_1309, uri_rdfs_Datatype), true, iext(uri_rdfs_subClassOf, C_1309, uri_rdfs_Resource), true)=true))). % 43.23/30.92 tff(c_12160, 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))). % 43.23/30.92 tff(c_15881, 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))). % 43.23/30.92 tff(c_9431, 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))). % 43.23/30.92 tff(c_5059, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, uri_ex_Clique), true, true, true), true)=true))). % 43.23/30.92 tff(c_15342, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_rdfs_isDefinedBy, uri_rdfs_isDefinedBy), true, true, true), true)=true))). % 43.23/30.92 tff(c_5900, 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))). % 43.23/30.92 tff(c_15406, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_ex_Clique, uri_rdfs_Resource), true, true, true), true)=true))). % 43.23/30.92 tff(c_10179, 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))). % 43.23/30.92 tff(c_9225, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, sK5_testcase_premise_fullish_013_Cliques_BNODE_r, uri_rdfs_Resource), true, true, true), true)=true))). % 43.23/30.92 tff(c_6247, 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))). % 43.38/30.92 tff(c_76829, plain, (![X_1290, Y_1291]: (ifeq(iext(uri_rdfs_domain, X_1290, Y_1291), true, iext(uri_rdfs_domain, X_1290, Y_1291), true)=true))). % 43.38/30.93 tff(c_4961, 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))). % 43.38/30.93 tff(c_76802, plain, (![X_1286, Y_1287]: (ifeq(iext(uri_owl_sameAs, X_1286, Y_1287), true, iext(uri_owl_sameAs, X_1286, Y_1287), true)=true))). % 43.38/30.93 tff(c_10962, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_owl_propertyChainAxiom, uri_owl_propertyChainAxiom), true, true, true), true)=true))). % 43.38/30.93 tff(c_76409, plain, (![X_1280, Y_1281]: (ifeq(iext(uri_rdf_object, X_1280, Y_1281), true, iext(uri_rdf_object, X_1280, Y_1281), true)=true))). % 43.38/30.93 tff(c_75914, plain, (![X_1273, Y_1274]: (ifeq(iext(uri_rdf__2, X_1273, Y_1274), true, iext(uri_rdf__2, X_1273, Y_1274), true)=true))). % 43.38/30.93 tff(c_4913, 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))). % 43.38/30.93 tff(c_75718, plain, (![X_1267, Y_1268]: (ifeq(iext(uri_owl_someValuesFrom, X_1267, Y_1268), true, iext(uri_owl_someValuesFrom, X_1267, Y_1268), true)=true))). % 43.38/30.93 tff(c_13084, 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))). % 43.38/30.93 tff(c_5012, 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))). % 43.38/30.93 tff(c_75201, plain, (![C_1262]: (ifeq(iext(uri_rdfs_subClassOf, C_1262, uri_rdfs_Container), true, iext(uri_rdfs_subClassOf, C_1262, uri_rdfs_Resource), true)=true))). % 43.38/30.93 tff(c_75173, plain, (![X_1258, Y_1259]: (ifeq(iext(uri_rdf__2, X_1258, Y_1259), true, iext(uri_rdfs_member, X_1258, Y_1259), true)=true))). % 43.38/30.93 tff(c_12019, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, sK5_testcase_premise_fullish_013_Cliques_BNODE_r, sK5_testcase_premise_fullish_013_Cliques_BNODE_r), true, true, true), true)=true))). % 43.38/30.93 tff(c_5399, 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))). % 43.38/30.93 tff(c_13835, 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))). % 43.38/30.93 tff(c_10587, 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))). % 43.38/30.93 tff(c_19402, 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))). % 43.38/30.93 tff(c_73912, plain, (![C_1248]: (ifeq(iext(uri_rdfs_subClassOf, C_1248, sK5_testcase_premise_fullish_013_Cliques_BNODE_r), true, iext(uri_rdfs_subClassOf, C_1248, uri_rdfs_Resource), true)=true))). % 43.38/30.93 tff(c_73659, plain, (![X_1243, Y_1244]: (ifeq(iext(uri_rdfs_seeAlso, X_1243, Y_1244), true, iext(uri_rdfs_seeAlso, X_1243, Y_1244), true)=true))). % 43.38/30.93 tff(c_12581, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_owl_propertyChainAxiom, uri_rdf_Property), true, true, true), true)=true))). % 43.38/30.93 tff(c_73331, plain, (![P_1239]: (ifeq(iext(uri_rdfs_subPropertyOf, P_1239, uri_rdf__1), true, iext(uri_rdfs_subPropertyOf, P_1239, uri_rdfs_member), true)=true))). % 43.38/30.93 tff(c_73098, plain, (![C_1235]: (ifeq(iext(uri_rdfs_subClassOf, C_1235, uri_rdfs_Class), true, iext(uri_rdfs_subClassOf, C_1235, uri_rdfs_Resource), true)=true))). % 43.38/30.93 tff(c_73061, plain, (![X_1233, Y_1234]: (ifeq(iext(uri_rdf_rest, X_1233, Y_1234), true, iext(uri_rdf_rest, X_1233, Y_1234), true)=true))). % 43.38/30.93 tff(c_6603, 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))). % 43.38/30.93 tff(c_71852, plain, (![X_1222, Y_1223]: (ifeq(iext(uri_ex_sameCliqueAs, X_1222, Y_1223), true, iext(uri_ex_sameCliqueAs, X_1222, Y_1223), true)=true))). % 43.38/30.93 tff(c_71825, plain, (![X_1218, Y_1219]: (ifeq(iext(uri_rdf__1, X_1218, Y_1219), true, iext(uri_rdf__1, X_1218, Y_1219), true)=true))). % 43.38/30.93 tff(c_5157, 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))). % 43.38/30.93 tff(c_10344, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_owl_someValuesFrom, uri_rdf_Property), true, true, true), true)=true))). % 43.38/30.93 tff(c_5344, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, sK5_testcase_premise_fullish_013_Cliques_BNODE_r), true, true, true), true)=true))). % 43.38/30.93 tff(c_7395, 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))). % 43.38/30.93 tff(c_70393, plain, (![X_1208, Y_1209]: (ifeq(iext(uri_rdfs_subClassOf, X_1208, Y_1209), true, iext(uri_rdfs_subClassOf, X_1208, Y_1209), true)=true))). % 43.38/30.93 tff(c_70365, plain, (![X_1204, Y_1205]: (ifeq(iext(uri_rdf_value, X_1204, Y_1205), true, iext(uri_rdf_value, X_1204, Y_1205), true)=true))). % 43.38/30.93 tff(c_7302, 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))). % 43.38/30.93 tff(c_4958, 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))). % 43.38/30.93 tff(c_12824, 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))). % 43.38/30.93 tff(c_11621, 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))). % 43.38/30.93 tff(c_5347, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, sK5_testcase_premise_fullish_013_Cliques_BNODE_r, Y_21), true, true, true), true)=true))). % 43.38/30.93 tff(c_6025, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, sK5_testcase_premise_fullish_013_Cliques_BNODE_r), true, ifeq(iext(P_18, uri_ex_JoesGang, Y_21), true, true, true), true)=true))). % 43.38/30.93 tff(c_14946, 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))). % 43.38/30.93 tff(c_66535, plain, (![C_1176]: (ifeq(iext(uri_rdfs_subClassOf, C_1176, uri_rdf_Property), true, iext(uri_rdfs_subClassOf, C_1176, uri_rdfs_Resource), true)=true))). % 43.38/30.93 tff(c_66327, plain, (![P_1173]: (ifeq(iext(uri_rdfs_subPropertyOf, P_1173, uri_rdf__2), true, iext(uri_rdfs_subPropertyOf, P_1173, uri_rdfs_member), true)=true))). % 43.38/30.93 tff(c_11524, 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))). % 43.38/30.93 tff(c_19781, 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))). % 43.38/30.93 tff(c_15613, 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))). % 43.38/30.93 tff(c_19778, 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))). % 43.38/30.93 tff(c_15610, 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))). % 43.38/30.93 tff(c_6999, 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))). % 43.38/30.93 tff(c_6678, 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))). % 43.38/30.93 tff(c_12778, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_List), true, ifeq(iext(P_18, sK4_testcase_premise_fullish_013_Cliques_BNODE_l3, Y_21), true, true, true), true)=true))). % 43.38/30.93 tff(c_20792, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, uri_ex_JoesGang, Y_21), true, true, true), true)=true))). % 43.38/30.93 tff(c_21737, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_List), true, ifeq(iext(P_18, sK1_testcase_premise_fullish_013_Cliques_BNODE_l1, Y_21), true, true, true), true)=true))). % 43.38/30.93 tff(c_6675, 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))). % 43.38/30.93 tff(c_5605, plain, (![P_47, X_139]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, X_139, uri_rdfs_Resource), true, true, true), true)=true))). % 43.38/30.93 tff(c_12775, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_List), true, ifeq(iext(P_28, X_30, sK4_testcase_premise_fullish_013_Cliques_BNODE_l3), true, true, true), true)=true))). % 43.38/30.93 tff(c_15835, 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_013_Cliques_BNODE_l2), true, true, true), true)=true))). % 43.38/30.93 tff(c_8658, 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))). % 43.38/30.93 tff(c_20789, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, uri_ex_JoesGang), true, true, true), true)=true))). % 43.38/30.93 tff(c_18034, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, uri_owl_ObjectProperty), true, true, true), true)=true))). % 43.38/30.93 tff(c_24063, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, uri_owl_Class, Y_21), true, true, true), true)=true))). % 43.38/30.93 tff(c_22577, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, uri_owl_Restriction), true, true, true), true)=true))). % 43.38/30.93 tff(c_22580, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, uri_owl_Restriction, Y_21), true, true, true), true)=true))). % 43.38/30.93 tff(c_15838, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_List), true, ifeq(iext(P_18, sK2_testcase_premise_fullish_013_Cliques_BNODE_l2, Y_21), true, true, true), true)=true))). % 43.38/30.93 tff(c_7002, 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))). % 43.38/30.93 tff(c_8661, 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))). % 43.38/30.93 tff(c_24060, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, uri_owl_Class), true, true, true), true)=true))). % 43.38/30.93 tff(c_18037, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, uri_owl_ObjectProperty, Y_21), true, true, true), true)=true))). % 43.38/30.93 tff(c_21734, 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_013_Cliques_BNODE_l1), true, true, true), true)=true))). % 43.38/30.93 tff(c_4855, 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))). % 43.38/30.93 tff(c_4400, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_ex_JoesGang), true, ifeq(iext(P_28, X_30, uri_ex_alice), true, true, true), true)=true))). % 43.38/30.93 tff(c_4772, 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))). % 43.38/30.93 tff(c_4564, 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))). % 43.38/30.93 tff(c_4239, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_owl_ObjectProperty), true, ifeq(iext(P_28, X_30, uri_foaf_knows), true, true, true), true)=true))). % 43.38/30.93 tff(c_19079, 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))). % 43.38/30.93 tff(c_4067, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_ex_JoesGang), true, ifeq(iext(P_28, X_30, uri_ex_bob), true, true, true), true)=true))). % 43.38/30.93 tff(c_4242, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_owl_ObjectProperty), true, ifeq(iext(P_18, uri_foaf_knows, Y_21), true, true, true), true)=true))). % 43.38/30.93 tff(c_4204, 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))). % 43.38/30.93 tff(c_4598, 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))). % 43.38/30.93 tff(c_4323, 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))). % 43.38/30.93 tff(c_4445, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_ex_Clique), true, ifeq(iext(P_18, uri_ex_JoesGang, Y_21), true, true, true), true)=true))). % 43.38/30.93 tff(c_19039, 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))). % 43.38/30.93 tff(c_4362, 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))). % 43.38/30.93 tff(c_4527, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_owl_Restriction), true, ifeq(iext(P_18, sK5_testcase_premise_fullish_013_Cliques_BNODE_r, Y_21), true, true, true), true)=true))). % 43.38/30.93 tff(c_4115, 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))). % 43.38/30.93 tff(c_4524, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_owl_Restriction), true, ifeq(iext(P_28, X_30, sK5_testcase_premise_fullish_013_Cliques_BNODE_r), true, true, true), true)=true))). % 43.38/30.93 tff(c_4814, 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))). % 43.38/30.93 tff(c_4112, 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))). % 43.38/30.93 tff(c_4070, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_ex_JoesGang), true, ifeq(iext(P_18, uri_ex_bob, Y_21), true, true, true), true)=true))). % 43.38/30.93 tff(c_4276, 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))). % 43.38/30.93 tff(c_4030, 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))). % 43.38/30.93 tff(c_4683, 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))). % 43.38/30.93 tff(c_4811, 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))). % 43.38/30.94 tff(c_4279, 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))). % 43.38/30.94 tff(c_4442, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_ex_Clique), true, ifeq(iext(P_28, X_30, uri_ex_JoesGang), true, true, true), true)=true))). % 43.38/30.94 tff(c_4365, 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))). % 43.38/30.94 tff(c_4775, 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))). % 43.38/30.94 tff(c_4033, 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))). % 43.38/30.94 tff(c_4201, 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))). % 43.38/30.94 tff(c_4686, 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))). % 43.38/30.94 tff(c_4641, 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))). % 43.38/30.94 tff(c_4644, 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))). % 43.38/30.94 tff(c_4403, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_ex_JoesGang), true, ifeq(iext(P_18, uri_ex_alice, Y_21), true, true, true), true)=true))). % 43.38/30.94 tff(c_4320, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_rdf_first), true, true, true), true)=true))). % 43.38/30.94 tff(c_19036, 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))). % 43.38/30.94 tff(c_4601, 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))). % 43.38/30.94 tff(c_4164, 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))). % 43.38/30.94 tff(c_4161, 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))). % 43.38/30.94 tff(c_4481, 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))). % 43.38/30.94 tff(c_4484, 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))). % 43.38/30.94 tff(c_19082, 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))). % 43.38/30.94 tff(c_4561, 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))). % 43.38/30.94 tff(c_4729, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_owl_Class), true, ifeq(iext(P_18, uri_ex_Clique, Y_21), true, true, true), true)=true))). % 43.38/30.94 tff(c_4852, 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))). % 43.38/30.94 tff(c_4726, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_owl_Class), true, ifeq(iext(P_28, X_30, uri_ex_Clique), true, true, true), true)=true))). % 43.38/30.94 tff(c_2199, plain, (![P_96, X_98, X_61]: (ifeq(iext(uri_rdfs_range, P_96, uri_rdfs_Resource), true, ifeq(iext(P_96, X_98, X_61), true, true, true), true)=true))). % 43.38/30.94 tff(c_1794, plain, (![P_92, X_61, Y_95]: (ifeq(iext(uri_rdfs_domain, P_92, uri_rdfs_Resource), true, ifeq(iext(P_92, X_61, Y_95), true, true, true), true)=true))). % 43.38/30.94 tff(c_3282, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_subClassOf), true, ifeq(iext(P_106, uri_ex_Clique, sK5_testcase_premise_fullish_013_Cliques_BNODE_r), true, true, true), true)=true))). % 43.38/30.94 tff(c_3276, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_foaf_knows, uri_owl_ObjectProperty), true, true, true), true)=true))). % 43.38/30.94 tff(c_3015, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_subClassOf), true, ifeq(iext(P_106, uri_rdf_Bag, uri_rdfs_Container), true, true, true), true)=true))). % 43.38/30.94 tff(c_3264, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_ex_sameCliqueAs, uri_ex_Clique), true, true, true), true)=true))). % 43.38/30.94 tff(c_3009, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdfs_member, uri_rdfs_Resource), true, true, true), true)=true))). % 43.38/30.94 tff(c_2895, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_subPropertyOf), true, ifeq(iext(P_106, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso), true, true, true), true)=true))). % 43.38/30.94 tff(c_3138, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf_Property, uri_rdfs_Class), true, true, true), true)=true))). % 43.38/30.94 tff(c_3069, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdf_value, uri_rdfs_Resource), true, true, true), true)=true))). % 43.38/30.94 tff(c_2937, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdfs_range, uri_rdfs_Class), true, true, true), true)=true))). % 43.38/30.94 tff(c_2979, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdfs_label, uri_rdfs_Resource), true, true, true), true)=true))). % 43.38/30.94 tff(c_3132, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf__3, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 43.38/30.94 tff(c_2838, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf_type, uri_rdf_Property), true, true, true), true)=true))). % 43.38/30.94 tff(c_3144, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdf_subject, uri_rdfs_Resource), true, true, true), true)=true))). % 43.38/30.94 tff(c_2949, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdf__1, uri_rdfs_Resource), true, true, true), true)=true))). % 43.38/30.94 tff(c_2880, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_subClassOf), true, ifeq(iext(P_106, uri_rdfs_Seq, uri_rdfs_Container), true, true, true), true)=true))). % 43.38/30.94 tff(c_3057, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdfs_seeAlso, uri_rdfs_Resource), true, true, true), true)=true))). % 43.38/30.94 tff(c_2913, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdf_value, uri_rdfs_Resource), true, true, true), true)=true))). % 43.38/30.94 tff(c_3198, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf_value, uri_rdf_Property), true, true, true), true)=true))). % 43.38/30.94 tff(c_3210, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdf_object, uri_rdfs_Statement), true, true, true), true)=true))). % 43.38/30.94 tff(c_3021, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdf__2, uri_rdfs_Resource), true, true, true), true)=true))). % 43.38/30.94 tff(c_3180, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_first), true, ifeq(iext(P_106, sK1_testcase_premise_fullish_013_Cliques_BNODE_l1, uri_rdf_type), true, true, true), true)=true))). % 43.38/30.94 tff(c_2997, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdfs_member, uri_rdfs_Resource), true, true, true), true)=true))). % 43.38/30.94 tff(c_2973, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_rest), true, ifeq(iext(P_106, sK2_testcase_premise_fullish_013_Cliques_BNODE_l2, sK4_testcase_premise_fullish_013_Cliques_BNODE_l3), true, true, true), true)=true))). % 43.38/30.94 tff(c_3120, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_subClassOf), true, ifeq(iext(P_106, uri_rdf_Alt, uri_rdfs_Container), true, true, true), true)=true))). % 43.38/30.94 tff(c_2919, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdfs_comment, uri_rdfs_Literal), true, true, true), true)=true))). % 43.38/30.94 tff(c_3081, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_ex_bob, uri_ex_JoesGang), true, true, true), true)=true))). % 43.38/30.94 tff(c_2967, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdfs_domain, uri_rdfs_Class), true, true, true), true)=true))). % 43.38/30.94 tff(c_3108, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf__2, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 43.38/30.94 tff(c_2991, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf_first, uri_rdf_Property), true, true, true), true)=true))). % 43.38/30.94 tff(c_3156, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdf_predicate, uri_rdfs_Statement), true, true, true), true)=true))). % 43.38/30.94 tff(c_49208, plain, (![C_993]: (ifeq(iext(uri_rdfs_subClassOf, C_993, uri_rdf_Alt), true, iext(uri_rdfs_subClassOf, C_993, uri_rdfs_Container), true)=true))). % 43.38/30.94 tff(c_3003, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdfs_domain, uri_rdf_Property), true, true, true), true)=true))). % 43.38/30.94 tff(c_3192, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_rest), true, ifeq(iext(P_106, sK1_testcase_premise_fullish_013_Cliques_BNODE_l1, sK2_testcase_premise_fullish_013_Cliques_BNODE_l2), true, true, true), true)=true))). % 43.38/30.94 tff(c_3204, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_first), true, ifeq(iext(P_106, sK4_testcase_premise_fullish_013_Cliques_BNODE_l3, sK3_testcase_premise_fullish_013_Cliques_BNODE_i), true, true, true), true)=true))). % 43.38/30.94 tff(c_3186, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf__3, uri_rdf_Property), true, true, true), true)=true))). % 43.38/30.94 tff(c_48449, plain, (![C_986]: (ifeq(iext(uri_rdfs_subClassOf, C_986, uri_rdfs_ContainerMembershipProperty), true, iext(uri_rdfs_subClassOf, C_986, uri_rdf_Property), true)=true))). % 43.38/30.94 tff(c_2868, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdfs_subClassOf, uri_rdfs_Class), true, true, true), true)=true))). % 43.38/30.94 tff(c_3150, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_first), true, ifeq(iext(P_106, sK2_testcase_premise_fullish_013_Cliques_BNODE_l2, uri_ex_sameCliqueAs), true, true, true), true)=true))). % 43.38/30.94 tff(c_2955, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf_object, uri_rdf_Property), true, true, true), true)=true))). % 43.38/30.94 tff(c_3096, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_subPropertyOf), true, ifeq(iext(P_106, uri_ex_sameCliqueAs, uri_owl_sameAs), true, true, true), true)=true))). % 43.38/30.94 tff(c_3039, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdfs_label, uri_rdfs_Literal), true, true, true), true)=true))). % 43.38/30.94 tff(c_3114, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdfs_subPropertyOf, uri_rdf_Property), true, true, true), true)=true))). % 43.38/30.94 tff(c_2943, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdf__1, uri_rdfs_Resource), true, true, true), true)=true))). % 43.38/30.94 tff(c_3168, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_subClassOf), true, ifeq(iext(P_106, uri_rdf_XMLLiteral, uri_rdfs_Literal), true, true, true), true)=true))). % 43.38/30.94 tff(c_3270, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_ex_JoesGang, uri_ex_Clique), true, true, true), true)=true))). % 43.38/30.94 tff(c_47260, plain, (![C_976]: (ifeq(iext(uri_rdfs_subClassOf, C_976, uri_rdfs_Datatype), true, iext(uri_rdfs_subClassOf, C_976, uri_rdfs_Class), true)=true))). % 43.38/30.94 tff(c_47193, plain, (![C_974]: (ifeq(iext(uri_rdfs_subClassOf, C_974, uri_rdf_Bag), true, iext(uri_rdfs_subClassOf, C_974, uri_rdfs_Container), true)=true))). % 43.38/30.94 tff(c_3063, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_owl_inverseOf), true, ifeq(iext(P_106, sK3_testcase_premise_fullish_013_Cliques_BNODE_i, uri_rdf_type), true, true, true), true)=true))). % 43.38/30.94 tff(c_47002, plain, (![P_971]: (ifeq(iext(uri_rdfs_subPropertyOf, P_971, uri_ex_sameCliqueAs), true, iext(uri_rdfs_subPropertyOf, P_971, uri_owl_sameAs), true)=true))). % 43.38/30.94 tff(c_2886, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true, true, true), true)=true))). % 43.38/30.94 tff(c_3222, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, sK5_testcase_premise_fullish_013_Cliques_BNODE_r, uri_owl_Restriction), true, true, true), true)=true))). % 43.38/30.94 tff(c_3228, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdfs_subPropertyOf, uri_rdf_Property), true, true, true), true)=true))). % 43.38/30.94 tff(c_46499, plain, (![D_966]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_966), true, icext(D_966, uri_rdfs_member), true)=true))). % 43.38/30.94 tff(c_46288, plain, (![D_963]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_963), true, icext(D_963, uri_rdfs_Resource), true)=true))). % 43.38/30.94 tff(c_3102, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdf_rest, uri_rdf_List), true, true, true), true)=true))). % 43.38/30.94 tff(c_46222, plain, (![D_961]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_961), true, icext(D_961, uri_rdfs_subPropertyOf), true)=true))). % 43.38/30.94 tff(c_46156, plain, (![D_959]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_959), true, icext(D_959, uri_owl_propertyChainAxiom), true)=true))). % 43.38/30.94 tff(c_45950, plain, (![D_956]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_956), true, icext(D_956, uri_owl_onProperty), true)=true))). % 43.38/30.94 tff(c_3246, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf_rest, uri_rdf_Property), true, true, true), true)=true))). % 43.38/30.94 tff(c_45884, plain, (![D_954]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_954), true, icext(D_954, uri_rdfs_seeAlso), true)=true))). % 43.38/30.94 tff(c_45818, plain, (![D_952]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_952), true, icext(D_952, uri_owl_sameAs), true)=true))). % 43.38/30.94 tff(c_45767, plain, (![C_950]: (ifeq(iext(uri_rdfs_subClassOf, C_950, uri_ex_Clique), true, iext(uri_rdfs_subClassOf, C_950, sK5_testcase_premise_fullish_013_Cliques_BNODE_r), true)=true))). % 43.38/30.94 tff(c_45701, plain, (![D_948]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_948), true, icext(D_948, uri_owl_inverseOf), true)=true))). % 43.38/30.94 tff(c_45635, plain, (![D_946]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_946), true, icext(D_946, uri_ex_sameCliqueAs), true)=true))). % 43.38/30.94 tff(c_45569, plain, (![D_944]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_944), true, icext(D_944, uri_owl_someValuesFrom), true)=true))). % 43.38/30.94 tff(c_3174, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_ex_alice, uri_ex_JoesGang), true, true, true), true)=true))). % 43.38/30.94 tff(c_45363, plain, (![D_941]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_941), true, icext(D_941, uri_rdfs_range), true)=true))). % 43.38/30.94 tff(c_45297, plain, (![D_939]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_939), true, icext(D_939, uri_rdfs_subClassOf), true)=true))). % 43.38/30.94 tff(c_45231, plain, (![D_937]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_937), true, icext(D_937, uri_rdfs_ContainerMembershipProperty), true)=true))). % 43.38/30.94 tff(c_2850, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdfs_range, uri_rdf_Property), true, true, true), true)=true))). % 43.38/30.94 tff(c_45021, plain, (![D_934]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_934), true, icext(D_934, uri_rdfs_Literal), true)=true))). % 43.38/30.94 tff(c_44953, plain, (![D_932]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_932), true, icext(D_932, uri_rdfs_Seq), true)=true))). % 43.38/30.94 tff(c_2931, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf__2, uri_rdf_Property), true, true, true), true)=true))). % 43.38/30.94 tff(c_44747, plain, (![D_929]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_929), true, icext(D_929, uri_rdf_Alt), true)=true))). % 43.38/30.94 tff(c_44680, plain, (![D_927]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_927), true, icext(D_927, uri_rdfs_Datatype), true)=true))). % 43.38/30.94 tff(c_3216, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdf_type, uri_rdfs_Resource), true, true, true), true)=true))). % 43.38/30.94 tff(c_44459, plain, (![D_924]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_924), true, icext(D_924, sK5_testcase_premise_fullish_013_Cliques_BNODE_r), true)=true))). % 43.38/30.94 tff(c_44373, plain, (![D_922]: (ifeq(iext(uri_rdfs_subClassOf, sK5_testcase_premise_fullish_013_Cliques_BNODE_r, D_922), true, icext(D_922, uri_ex_JoesGang), true)=true))). % 43.38/30.94 tff(c_3075, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_subClassOf), true, ifeq(iext(P_106, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property), true, true, true), true)=true))). % 43.38/30.95 tff(c_44139, plain, (![D_919]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_919), true, icext(D_919, uri_rdfs_Class), true)=true))). % 43.38/30.95 tff(c_44072, plain, (![D_917]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_917), true, icext(D_917, uri_rdf_Bag), true)=true))). % 43.38/30.95 tff(c_43858, plain, (![D_914]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_914), true, icext(D_914, uri_rdf_XMLLiteral), true)=true))). % 43.38/30.95 tff(c_3234, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdf_subject, uri_rdfs_Statement), true, true, true), true)=true))). % 43.38/30.95 tff(c_43792, plain, (![D_912]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_912), true, icext(D_912, uri_rdfs_Container), true)=true))). % 43.38/30.95 tff(c_43716, plain, (![D_910]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_910), true, icext(D_910, uri_ex_Clique), true)=true))). % 43.38/30.95 tff(c_3252, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf_XMLLiteral, uri_rdfs_Datatype), true, true, true), true)=true))). % 43.38/30.95 tff(c_43510, plain, (![D_907]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_907), true, icext(D_907, uri_owl_Restriction), true)=true))). % 43.38/30.95 tff(c_43444, plain, (![D_905]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_905), true, icext(D_905, uri_rdfs_Statement), true)=true))). % 43.38/30.95 tff(c_43378, plain, (![D_903]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_903), true, icext(D_903, sK4_testcase_premise_fullish_013_Cliques_BNODE_l3), true)=true))). % 43.38/30.95 tff(c_3258, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf__1, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 43.38/30.95 tff(c_43172, plain, (![D_900]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_900), true, icext(D_900, uri_rdfs_domain), true)=true))). % 43.38/30.95 tff(c_43106, plain, (![D_898]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_898), true, icext(D_898, uri_owl_ObjectProperty), true)=true))). % 43.38/30.95 tff(c_43040, plain, (![D_896]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_896), true, icext(D_896, uri_owl_Class), true)=true))). % 43.38/30.95 tff(c_2985, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_ex_Clique, uri_owl_Class), true, true, true), true)=true))). % 43.38/30.95 tff(c_42834, plain, (![D_893]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_893), true, icext(D_893, uri_rdfs_label), true)=true))). % 43.38/30.95 tff(c_42767, plain, (![D_891]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_891), true, icext(D_891, sK1_testcase_premise_fullish_013_Cliques_BNODE_l1), true)=true))). % 43.38/30.95 tff(c_42700, plain, (![C_889]: (ifeq(iext(uri_rdfs_subClassOf, C_889, uri_rdfs_Seq), true, iext(uri_rdfs_subClassOf, C_889, uri_rdfs_Container), true)=true))). % 43.38/30.95 tff(c_42618, plain, (![D_887]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_887), true, icext(D_887, uri_ex_JoesGang), true)=true))). % 43.38/30.95 tff(c_42552, plain, (![D_885]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_885), true, icext(D_885, uri_rdfs_isDefinedBy), true)=true))). % 43.38/30.95 tff(c_17829, 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))). % 43.38/30.95 tff(c_42486, plain, (![P_882]: (ifeq(iext(uri_rdfs_subPropertyOf, P_882, uri_rdfs_isDefinedBy), true, iext(uri_rdfs_subPropertyOf, P_882, uri_rdfs_seeAlso), true)=true))). % 43.38/30.95 tff(c_17779, 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))). % 43.38/30.95 tff(c_42359, plain, (![D_877]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_877), true, icext(D_877, uri_rdf_List), true)=true))). % 43.38/30.95 tff(c_19718, 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))). % 43.38/30.95 tff(c_19653, 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))). % 43.38/30.95 tff(c_2844, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf__1, uri_rdf_Property), true, true, true), true)=true))). % 43.38/30.95 tff(c_17454, 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))). % 43.38/30.95 tff(c_17393, 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))). % 43.38/30.95 tff(c_42042, plain, (![D_868]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_868), true, icext(D_868, sK2_testcase_premise_fullish_013_Cliques_BNODE_l2), true)=true))). % 43.38/30.95 tff(c_17684, 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))). % 43.38/30.95 tff(c_2874, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_rest), true, ifeq(iext(P_106, sK4_testcase_premise_fullish_013_Cliques_BNODE_l3, uri_rdf_nil), true, true, true), true)=true))). % 43.38/30.95 tff(c_20169, 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))). % 43.38/30.95 tff(c_21233, plain, (![E_41]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, E_41), true, iext(uri_rdfs_subClassOf, uri_ex_JoesGang, E_41), true)=true))). % 43.38/30.95 tff(c_41689, plain, (![D_859]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_859), true, icext(D_859, uri_rdf__3), true)=true))). % 43.38/30.95 tff(c_22919, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_owl_Restriction, uri_owl_Restriction), true)=true))). % 43.38/30.95 tff(c_20103, 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))). % 43.38/30.95 tff(c_21232, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_ex_JoesGang, uri_rdfs_Resource), true)=true))). % 43.38/30.95 tff(c_24418, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_owl_Class, uri_owl_Class), true)=true))). % 43.38/30.95 tff(c_24484, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_owl_Class, uri_rdfs_Resource), true)=true))). % 43.38/30.95 tff(c_41506, plain, (![D_851]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_851), true, icext(D_851, uri_rdf_value), true)=true))). % 43.38/30.95 tff(c_17172, 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))). % 43.38/30.95 tff(c_20170, 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))). % 43.38/30.95 tff(c_3033, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_owl_someValuesFrom), true, ifeq(iext(P_106, sK5_testcase_premise_fullish_013_Cliques_BNODE_r, uri_ex_Clique), true, true, true), true)=true))). % 43.38/30.95 tff(c_24485, plain, (![E_41]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, E_41), true, iext(uri_rdfs_subClassOf, uri_owl_Class, E_41), true)=true))). % 43.38/30.95 tff(c_17106, 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))). % 43.38/30.95 tff(c_41157, plain, (![D_842]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_842), true, icext(D_842, uri_rdf__2), true)=true))). % 43.38/30.95 tff(c_18423, plain, (![E_41]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, E_41), true, iext(uri_rdfs_subClassOf, uri_owl_ObjectProperty, E_41), true)=true))). % 43.38/30.95 tff(c_18356, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_owl_ObjectProperty, uri_owl_ObjectProperty), true)=true))). % 43.38/30.95 tff(c_22985, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_owl_Restriction, uri_rdfs_Resource), true)=true))). % 43.38/30.95 tff(c_3087, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdfs_seeAlso, uri_rdfs_Resource), true, true, true), true)=true))). % 43.38/30.95 tff(c_17173, 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))). % 43.38/30.95 tff(c_22986, plain, (![E_41]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, E_41), true, iext(uri_rdfs_subClassOf, uri_owl_Restriction, E_41), true)=true))). % 43.38/30.95 tff(c_21141, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_ex_JoesGang, uri_ex_JoesGang), true)=true))). % 43.38/30.95 tff(c_40835, plain, (![D_833]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_833), true, icext(D_833, uri_rdf_first), true)=true))). % 43.38/30.95 tff(c_18422, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_owl_ObjectProperty, uri_rdfs_Resource), true)=true))). % 43.38/30.95 tff(c_40788, plain, (![X_828, Y_829]: (ifeq(iext(uri_rdfs_isDefinedBy, X_828, Y_829), true, iext(uri_rdfs_seeAlso, X_828, Y_829), true)=true))). % 43.38/30.95 tff(c_16643, 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))). % 43.38/30.95 tff(c_16569, 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))). % 43.38/30.95 tff(c_16690, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, sK5_testcase_premise_fullish_013_Cliques_BNODE_r, uri_rdfs_Class), true)=true))). % 43.38/30.95 tff(c_16819, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_ex_JoesGang, sK5_testcase_premise_fullish_013_Cliques_BNODE_r), true)=true))). % 43.38/30.95 tff(c_16867, 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))). % 43.38/30.95 tff(c_40626, plain, (![C_820]: (ifeq(iext(uri_rdfs_subClassOf, C_820, uri_rdf_XMLLiteral), true, iext(uri_rdfs_subClassOf, C_820, uri_rdfs_Literal), true)=true))). % 43.38/30.95 tff(c_16472, 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))). % 43.38/30.95 tff(c_16522, 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))). % 43.38/30.95 tff(c_16965, 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))). % 43.38/30.95 tff(c_17044, 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))). % 43.38/30.95 tff(c_16914, 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))). % 43.38/30.95 tff(c_16425, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_ex_Clique, uri_rdfs_Class), true)=true))). % 43.38/30.95 tff(c_16772, 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))). % 43.38/30.95 tff(c_18294, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_owl_ObjectProperty, uri_rdfs_Class), true)=true))). % 43.38/30.95 tff(c_2820, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdf__3, uri_rdfs_Resource), true, true, true), true)=true))). % 43.38/30.95 tff(c_24356, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_owl_Class, uri_rdfs_Class), true)=true))). % 43.38/30.95 tff(c_20041, 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))). % 43.38/30.95 tff(c_22832, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_owl_Restriction, uri_rdfs_Class), true)=true))). % 43.38/30.95 tff(c_16139, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, sK4_testcase_premise_fullish_013_Cliques_BNODE_l3, uri_rdf_List), true)=true))). % 43.38/30.95 tff(c_16311, 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))). % 43.38/30.95 tff(c_16186, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, sK2_testcase_premise_fullish_013_Cliques_BNODE_l2, uri_rdf_List), true)=true))). % 43.38/30.95 tff(c_21800, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, sK1_testcase_premise_fullish_013_Cliques_BNODE_l1, uri_rdf_List), true)=true))). % 43.38/30.95 tff(c_20939, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_ex_JoesGang, uri_rdfs_Class), true)=true))). % 43.38/30.95 tff(c_2856, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdf_type, uri_rdfs_Class), true, true, true), true)=true))). % 43.38/30.95 tff(c_16258, 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))). % 43.38/30.95 tff(c_12859, 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))). % 43.38/30.95 tff(c_39972, plain, (![D_797]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_797), true, icext(D_797, uri_rdf_subject), true)=true))). % 43.38/30.95 tff(c_15149, 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))). % 43.38/30.95 tff(c_11257, 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))). % 43.38/30.95 tff(c_11050, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_owl_onProperty, uri_rdf_Property), true)=true))). % 43.38/30.95 tff(c_7517, 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))). % 43.38/30.95 tff(c_10621, 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))). % 43.38/30.95 tff(c_14971, 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))). % 43.38/30.95 tff(c_2961, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_owl_propertyChainAxiom), true, ifeq(iext(P_106, uri_foaf_knows, sK1_testcase_premise_fullish_013_Cliques_BNODE_l1), true, true, true), true)=true))). % 43.38/30.95 tff(c_13669, 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))). % 43.38/30.95 tff(c_15373, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_rdfs_isDefinedBy, uri_rdfs_isDefinedBy), true)=true))). % 43.38/30.95 tff(c_7429, 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))). % 43.38/30.95 tff(c_13115, 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))). % 43.38/30.95 tff(c_7690, 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))). % 43.38/30.95 tff(c_3126, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdf_first, uri_rdfs_Resource), true, true, true), true)=true))). % 43.38/30.95 tff(c_14484, 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))). % 43.38/30.95 tff(c_15912, 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))). % 43.38/30.95 tff(c_14209, 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))). % 43.38/30.95 tff(c_39164, plain, (![D_771]: (ifeq(iext(uri_rdfs_subClassOf, uri_ex_Clique, D_771), true, icext(D_771, uri_ex_JoesGang), true)=true))). % 43.38/30.95 tff(c_12428, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_owl_inverseOf, uri_rdf_Property), true)=true))). % 43.38/30.95 tff(c_8607, 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))). % 43.38/30.95 tff(c_11493, 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))). % 43.38/30.95 tff(c_3162, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true, true, true), true)=true))). % 43.38/30.95 tff(c_9932, 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))). % 43.38/30.95 tff(c_6185, 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))). % 43.38/30.95 tff(c_11494, 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))). % 43.38/30.95 tff(c_12053, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, sK5_testcase_premise_fullish_013_Cliques_BNODE_r, sK5_testcase_premise_fullish_013_Cliques_BNODE_r), true)=true))). % 43.38/30.95 tff(c_11713, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_owl_sameAs, uri_rdf_Property), true)=true))). % 43.38/30.95 tff(c_7428, 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))). % 43.38/30.95 tff(c_2832, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdfs_comment, uri_rdfs_Resource), true, true, true), true)=true))). % 43.38/30.95 tff(c_15440, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_ex_Clique, uri_rdfs_Resource), true)=true))). % 43.38/30.95 tff(c_38507, plain, (![D_753]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_753), true, icext(D_753, uri_rdf_object), true)=true))). % 43.38/30.95 tff(c_7187, 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))). % 43.38/30.95 tff(c_10993, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_owl_propertyChainAxiom, uri_owl_propertyChainAxiom), true)=true))). % 43.38/30.95 tff(c_2814, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdf_first, uri_rdf_List), true, true, true), true)=true))). % 43.38/30.95 tff(c_7336, 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))). % 43.38/30.95 tff(c_14315, 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))). % 43.38/30.95 tff(c_5810, 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))). % 43.38/30.95 tff(c_38175, plain, (![D_744]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_744), true, icext(D_744, uri_rdf_nil), true)=true))). % 43.38/30.95 tff(c_13332, 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))). % 43.38/30.95 tff(c_12606, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_owl_propertyChainAxiom, uri_rdf_Property), true)=true))). % 43.38/30.96 tff(c_12185, 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))). % 43.38/30.96 tff(c_2901, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_owl_onProperty), true, ifeq(iext(P_106, sK5_testcase_premise_fullish_013_Cliques_BNODE_r, uri_ex_sameCliqueAs), true, true, true), true)=true))). % 43.38/30.96 tff(c_11892, 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))). % 43.38/30.96 tff(c_9258, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, sK5_testcase_premise_fullish_013_Cliques_BNODE_r, uri_rdfs_Resource), true)=true))). % 43.38/30.96 tff(c_8084, 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))). % 43.38/30.96 tff(c_37860, plain, (![D_735]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_735), true, icext(D_735, uri_rdfs_comment), true)=true))). % 43.38/30.96 tff(c_37802, plain, (![X_730, Y_731]: (ifeq(iext(uri_ex_sameCliqueAs, X_730, Y_731), true, iext(uri_owl_sameAs, X_730, Y_731), true)=true))). % 43.38/30.96 tff(c_14031, 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))). % 43.38/30.96 tff(c_15441, plain, (![E_41]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, E_41), true, iext(uri_rdfs_subClassOf, uri_ex_Clique, E_41), true)=true))). % 43.38/30.96 tff(c_37659, plain, (![D_725]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_725), true, icext(D_725, uri_rdf__3), true)=true))). % 43.38/30.96 tff(c_14914, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_owl_inverseOf, uri_owl_inverseOf), true)=true))). % 43.38/30.96 tff(c_3027, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdf__2, uri_rdfs_Resource), true, true, true), true)=true))). % 43.38/30.96 tff(c_14483, 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))). % 43.38/30.96 tff(c_12372, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_owl_sameAs, uri_owl_sameAs), true)=true))). % 43.38/30.96 tff(c_10210, 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))). % 43.38/30.96 tff(c_5746, 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))). % 43.38/30.96 tff(c_11893, 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))). % 43.38/30.96 tff(c_11558, 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))). % 43.38/30.96 tff(c_2826, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf_subject, uri_rdf_Property), true, true, true), true)=true))). % 43.38/30.96 tff(c_14674, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_ex_sameCliqueAs, uri_rdf_Property), true)=true))). % 43.38/30.96 tff(c_15282, 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))). % 43.38/30.96 tff(c_36992, plain, (![D_707]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_707), true, icext(D_707, uri_rdf__1), true)=true))). % 43.38/30.96 tff(c_15216, 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))). % 43.38/30.96 tff(c_9102, 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))). % 43.38/30.96 tff(c_13267, 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))). % 43.38/30.96 tff(c_2862, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdf_rest, uri_rdf_List), true, true, true), true)=true))). % 43.38/30.96 tff(c_7689, 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))). % 43.38/30.96 tff(c_6628, 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))). % 43.38/30.96 tff(c_15913, 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))). % 43.38/30.96 tff(c_36659, plain, (![D_698]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_698), true, icext(D_698, uri_rdf__2), true)=true))). % 43.38/30.96 tff(c_9727, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_owl_someValuesFrom, uri_owl_someValuesFrom), true)=true))). % 43.38/30.96 tff(c_14314, 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))). % 43.38/30.96 tff(c_2907, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf_nil, uri_rdf_List), true, true, true), true)=true))). % 43.38/30.96 tff(c_16089, 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))). % 43.38/30.96 tff(c_9259, plain, (![E_41]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, E_41), true, iext(uri_rdfs_subClassOf, sK5_testcase_premise_fullish_013_Cliques_BNODE_r, E_41), true)=true))). % 43.38/30.96 tff(c_7335, 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))). % 43.38/30.96 tff(c_11656, 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))). % 43.38/30.96 tff(c_10620, 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))). % 43.38/30.96 tff(c_3240, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdf__3, uri_rdfs_Resource), true, true, true), true)=true))). % 43.38/30.96 tff(c_10026, 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))). % 43.38/30.96 tff(c_9040, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_owl_onProperty, uri_owl_onProperty), true)=true))). % 43.38/30.96 tff(c_13333, 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))). % 43.38/30.96 tff(c_9101, 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))). % 43.38/30.96 tff(c_2925, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdfs_subClassOf, uri_rdfs_Class), true, true, true), true)=true))). % 43.38/30.96 tff(c_13866, 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))). % 43.38/30.96 tff(c_6948, 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))). % 43.38/30.96 tff(c_6277, 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))). % 43.38/30.96 tff(c_13177, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_ex_Clique, uri_ex_Clique), true)=true))). % 43.38/30.96 tff(c_10369, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_owl_someValuesFrom, uri_rdf_Property), true)=true))). % 43.38/30.96 tff(c_3045, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdf_predicate, uri_rdfs_Resource), true, true, true), true)=true))). % 43.38/30.96 tff(c_9463, 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))). % 43.38/30.96 tff(c_8540, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_ex_sameCliqueAs, uri_ex_sameCliqueAs), true)=true))). % 43.38/30.96 tff(c_11258, 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))). % 43.38/30.96 tff(c_5934, 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))). % 43.38/30.96 tff(c_5933, 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))). % 43.38/30.96 tff(c_6369, 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))). % 43.38/30.96 tff(c_19521, 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))). % 43.38/30.96 tff(c_3051, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_subClassOf), true, ifeq(iext(P_106, uri_rdfs_Datatype, uri_rdfs_Class), true, true, true), true)=true))). % 43.38/30.96 tff(c_19427, 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))). % 43.38/30.96 tff(c_5625, plain, (![Q_48, X_139]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, X_139, uri_rdfs_Resource), true)=true))). % 43.38/30.96 tff(c_3358, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf_rest, uri_rdf_Property), true)=true))). % 43.38/30.96 tff(c_3348, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf__3, uri_rdf_Property), true)=true))). % 43.38/30.96 tff(c_2644, plain, (![R_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_owl_sameAs, R_101), true, iext(uri_rdfs_subPropertyOf, uri_ex_sameCliqueAs, R_101), true)=true))). % 43.38/30.96 tff(c_3343, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdf_predicate, uri_rdfs_Statement), true)=true))). % 43.38/30.96 tff(c_3332, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdfs_seeAlso, uri_rdfs_Resource), true)=true))). % 43.38/30.96 tff(c_2749, plain, (![E_104]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_104), true, iext(uri_rdfs_subClassOf, uri_rdf_Alt, E_104), true)=true))). % 43.38/30.96 tff(c_3335, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf__2, uri_rdfs_ContainerMembershipProperty), true)=true))). % 43.38/30.96 tff(c_3340, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf_Property, uri_rdfs_Class), true)=true))). % 43.38/30.96 tff(c_3313, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_rest, Q_107), true, iext(Q_107, sK2_testcase_premise_fullish_013_Cliques_BNODE_l2, sK4_testcase_premise_fullish_013_Cliques_BNODE_l3), true)=true))). % 43.38/30.96 tff(c_3315, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_ex_Clique, uri_owl_Class), true)=true))). % 43.38/30.96 tff(c_34703, plain, (![D_643]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, D_643), true, icext(D_643, uri_rdf_XMLLiteral), true)=true))). % 43.38/30.96 tff(c_2748, plain, (![E_104]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, E_104), true, iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, E_104), true)=true))). % 43.38/30.96 tff(c_3290, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdfs_comment, uri_rdfs_Resource), true)=true))). % 43.38/30.96 tff(c_3336, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdfs_subPropertyOf, uri_rdf_Property), true)=true))). % 43.38/30.96 tff(c_3316, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf_first, uri_rdf_Property), true)=true))). % 43.38/30.96 tff(c_3352, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdf_object, uri_rdfs_Statement), true)=true))). % 43.38/30.96 tff(c_3304, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdfs_comment, uri_rdfs_Literal), true)=true))). % 43.38/30.96 tff(c_3325, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdf_predicate, uri_rdfs_Resource), true)=true))). % 43.38/30.96 tff(c_34494, plain, (![D_634]: (ifeq(iext(uri_rdfs_subClassOf, uri_owl_Restriction, D_634), true, icext(D_634, sK5_testcase_premise_fullish_013_Cliques_BNODE_r), true)=true))). % 43.38/30.96 tff(c_3334, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdf_rest, uri_rdf_List), true)=true))). % 43.38/30.96 tff(c_3288, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdf__3, uri_rdfs_Resource), true)=true))). % 43.38/30.96 tff(c_3345, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_107), true, iext(Q_107, uri_rdf_XMLLiteral, uri_rdfs_Literal), true)=true))). % 43.38/30.96 tff(c_3341, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdf_subject, uri_rdfs_Resource), true)=true))). % 43.38/30.96 tff(c_3298, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_107), true, iext(Q_107, uri_rdfs_Seq, uri_rdfs_Container), true)=true))). % 43.38/30.96 tff(c_3299, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true)=true))). % 43.38/30.96 tff(c_3364, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_107), true, iext(Q_107, uri_ex_Clique, sK5_testcase_premise_fullish_013_Cliques_BNODE_r), true)=true))). % 43.38/30.96 tff(c_2750, plain, (![E_104]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Literal, E_104), true, iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, E_104), true)=true))). % 43.38/30.96 tff(c_3360, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf__1, uri_rdfs_ContainerMembershipProperty), true)=true))). % 43.38/30.96 tff(c_3297, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_rest, Q_107), true, iext(Q_107, sK4_testcase_premise_fullish_013_Cliques_BNODE_l3, uri_rdf_nil), true)=true))). % 43.38/30.96 tff(c_3292, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf__1, uri_rdf_Property), true)=true))). % 43.38/30.96 tff(c_3324, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdfs_label, uri_rdfs_Literal), true)=true))). % 43.38/30.96 tff(c_3287, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdf_first, uri_rdf_List), true)=true))). % 43.38/30.96 tff(c_3295, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdf_rest, uri_rdf_List), true)=true))). % 43.38/30.96 tff(c_3323, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_owl_someValuesFrom, Q_107), true, iext(Q_107, sK5_testcase_premise_fullish_013_Cliques_BNODE_r, uri_ex_Clique), true)=true))). % 43.38/30.96 tff(c_3333, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_107), true, iext(Q_107, uri_ex_sameCliqueAs, uri_owl_sameAs), true)=true))). % 43.38/30.96 tff(c_34144, plain, (![D_616]: (ifeq(iext(uri_rdfs_subClassOf, uri_owl_ObjectProperty, D_616), true, icext(D_616, uri_foaf_knows), true)=true))). % 43.38/30.96 tff(c_3362, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_ex_JoesGang, uri_ex_Clique), true)=true))). % 43.38/30.96 tff(c_3294, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdf_type, uri_rdfs_Class), true)=true))). % 43.38/30.96 tff(c_3300, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_107), true, iext(Q_107, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso), true)=true))). % 43.38/30.96 tff(c_3314, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdfs_label, uri_rdfs_Resource), true)=true))). % 43.38/30.96 tff(c_3359, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf_XMLLiteral, uri_rdfs_Datatype), true)=true))). % 43.38/30.96 tff(c_3346, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_ex_alice, uri_ex_JoesGang), true)=true))). % 43.38/30.96 tff(c_3303, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdf_value, uri_rdfs_Resource), true)=true))). % 43.38/30.96 tff(c_33959, plain, (![D_607]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_607), true, icext(D_607, uri_rdf_Property), true)=true))). % 43.38/30.96 tff(c_3328, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_owl_inverseOf, Q_107), true, iext(Q_107, sK3_testcase_premise_fullish_013_Cliques_BNODE_i, uri_rdf_type), true)=true))). % 43.38/30.96 tff(c_3344, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true)=true))). % 43.38/30.96 tff(c_3310, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf_object, uri_rdf_Property), true)=true))). % 43.38/30.96 tff(c_3350, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf_value, uri_rdf_Property), true)=true))). % 43.38/30.96 tff(c_3351, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_first, Q_107), true, iext(Q_107, sK4_testcase_premise_fullish_013_Cliques_BNODE_l3, sK3_testcase_premise_fullish_013_Cliques_BNODE_i), true)=true))). % 43.38/30.96 tff(c_3356, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdf_subject, uri_rdfs_Statement), true)=true))). % 43.38/30.96 tff(c_3330, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_107), true, iext(Q_107, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property), true)=true))). % 43.38/30.96 tff(c_3320, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_107), true, iext(Q_107, uri_rdf_Bag, uri_rdfs_Container), true)=true))). % 43.38/30.96 tff(c_3311, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_owl_propertyChainAxiom, Q_107), true, iext(Q_107, uri_foaf_knows, sK1_testcase_premise_fullish_013_Cliques_BNODE_l1), true)=true))). % 43.38/30.96 tff(c_3353, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdf_type, uri_rdfs_Resource), true)=true))). % 43.38/30.96 tff(c_2746, plain, (![E_104]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_104), true, iext(uri_rdfs_subClassOf, uri_rdf_Bag, E_104), true)=true))). % 43.38/30.96 tff(c_3361, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_ex_sameCliqueAs, uri_ex_Clique), true)=true))). % 43.38/30.96 tff(c_3312, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdfs_domain, uri_rdfs_Class), true)=true))). % 43.38/30.96 tff(c_3307, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdfs_range, uri_rdfs_Class), true)=true))). % 43.38/30.96 tff(c_3338, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdf_first, uri_rdfs_Resource), true)=true))). % 43.38/30.96 tff(c_3306, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf__2, uri_rdf_Property), true)=true))). % 43.38/30.96 tff(c_2643, plain, (![R_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_seeAlso, R_101), true, iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, R_101), true)=true))). % 43.38/30.96 tff(c_17782, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_label), true)=true))). % 43.38/30.96 tff(c_17783, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_label), true)=true))). % 43.38/30.96 tff(c_3363, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_foaf_knows, uri_owl_ObjectProperty), true)=true))). % 43.38/30.96 tff(c_19656, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_predicate), true)=true))). % 43.38/30.96 tff(c_19657, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_predicate), true)=true))). % 43.38/30.96 tff(c_33473, plain, (![D_583]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_583), true, icext(D_583, uri_rdf_predicate), true)=true))). % 43.38/30.96 tff(c_17688, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_member), true)=true))). % 43.38/30.96 tff(c_3355, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdfs_subPropertyOf, uri_rdf_Property), true)=true))). % 43.38/30.96 tff(c_17397, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Resource), true)=true))). % 43.38/30.96 tff(c_19722, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_comment), true)=true))). % 43.38/30.96 tff(c_19721, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_comment), true)=true))). % 43.38/30.96 tff(c_33282, plain, (![D_576]: (ifeq(iext(uri_rdfs_subClassOf, uri_ex_JoesGang, D_576), true, icext(D_576, uri_ex_alice), true)=true))). % 43.38/30.96 tff(c_3305, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdfs_subClassOf, uri_rdfs_Class), true)=true))). % 43.38/30.96 tff(c_17109, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Statement), true)=true))). % 43.38/30.96 tff(c_33167, plain, (![D_572]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_572), true, icext(D_572, uri_rdf_rest), true)=true))). % 43.38/30.96 tff(c_18359, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_owl_ObjectProperty), true)=true))). % 43.38/30.96 tff(c_20173, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdf_List), true)=true))). % 43.38/30.96 tff(c_3302, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf_nil, uri_rdf_List), true)=true))). % 43.38/30.97 tff(c_20106, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_List), true)=true))). % 43.38/30.97 tff(c_18426, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_owl_ObjectProperty), true)=true))). % 43.38/30.97 tff(c_17110, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Statement), true)=true))). % 43.38/30.97 tff(c_24421, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_owl_Class), true)=true))). % 43.38/30.97 tff(c_21144, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_ex_JoesGang), true)=true))). % 43.38/30.97 tff(c_3321, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdf__2, uri_rdfs_Resource), true)=true))). % 43.38/30.97 tff(c_21145, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_ex_JoesGang), true)=true))). % 43.38/30.97 tff(c_32839, plain, (![D_560]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_560), true, icext(D_560, uri_rdf_type), true)=true))). % 43.38/30.97 tff(c_24488, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_owl_Class), true)=true))). % 43.38/30.97 tff(c_22922, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_owl_Restriction), true)=true))). % 43.38/30.97 tff(c_3331, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_ex_bob, uri_ex_JoesGang), true)=true))). % 43.38/30.97 tff(c_22923, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_owl_Restriction), true)=true))). % 43.38/30.97 tff(c_2751, plain, (![E_104]: (ifeq(iext(uri_rdfs_subClassOf, sK5_testcase_premise_fullish_013_Cliques_BNODE_r, E_104), true, iext(uri_rdfs_subClassOf, uri_ex_Clique, E_104), true)=true))). % 43.38/30.97 tff(c_3326, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_107), true, iext(Q_107, uri_rdfs_Datatype, uri_rdfs_Class), true)=true))). % 43.38/30.97 tff(c_32608, plain, (![D_552]: (ifeq(iext(uri_rdfs_subClassOf, uri_owl_Class, D_552), true, icext(D_552, uri_ex_Clique), true)=true))). % 43.38/30.97 tff(c_16820, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_29), true, icext(C_29, sK5_testcase_premise_fullish_013_Cliques_BNODE_r), true)=true))). % 43.38/30.97 tff(c_3301, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_owl_onProperty, Q_107), true, iext(Q_107, sK5_testcase_premise_fullish_013_Cliques_BNODE_r, uri_ex_sameCliqueAs), true)=true))). % 43.38/30.97 tff(c_32493, plain, (![D_548]: (ifeq(iext(uri_rdfs_subClassOf, uri_ex_JoesGang, D_548), true, icext(D_548, uri_ex_bob), true)=true))). % 43.38/30.97 tff(c_2747, plain, (![E_104]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, E_104), true, iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, E_104), true)=true))). % 43.38/30.97 tff(c_3327, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdfs_seeAlso, uri_rdfs_Resource), true)=true))). % 43.38/30.97 tff(c_5749, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_seeAlso), true)=true))). % 43.38/30.97 tff(c_13269, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_XMLLiteral), true)=true))). % 43.38/30.97 tff(c_3317, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdfs_member, uri_rdfs_Resource), true)=true))). % 43.38/30.97 tff(c_11659, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Seq), true)=true))). % 43.38/30.97 tff(c_6279, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_type), true)=true))). % 43.38/30.97 tff(c_3289, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf_subject, uri_rdf_Property), true)=true))). % 43.38/30.97 tff(c_13118, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__2), true)=true))). % 43.38/30.97 tff(c_32160, plain, (![D_537]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_537), true, icext(D_537, uri_rdf__1), true)=true))). % 43.38/30.97 tff(c_5813, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_range), true)=true))). % 43.38/30.97 tff(c_14918, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_owl_inverseOf), true)=true))). % 43.38/30.97 tff(c_3342, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_first, Q_107), true, iext(Q_107, sK2_testcase_premise_fullish_013_Cliques_BNODE_l2, uri_ex_sameCliqueAs), true)=true))). % 43.38/30.97 tff(c_6280, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_type), true)=true))). % 43.38/30.97 tff(c_15285, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_Alt), true)=true))). % 43.38/30.97 tff(c_31494, plain, (![D_528, X_529]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, D_528), true, icext(D_528, X_529), true)=true))). % 43.38/30.97 tff(c_15376, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_isDefinedBy), true)=true))). % 43.38/30.97 tff(c_3309, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdf__1, uri_rdfs_Resource), true)=true))). % 43.38/30.97 tff(c_9935, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_value), true)=true))). % 43.38/30.97 tff(c_31177, plain, (![C_89, X_61]: (ifeq(icext(C_89, X_61), true, true, true)=true))). % 43.38/30.97 tff(c_13179, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_ex_Clique), true)=true))). % 43.38/30.97 tff(c_3319, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdfs_member, uri_rdfs_Resource), true)=true))). % 43.38/30.97 tff(c_15219, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_ContainerMembershipProperty), true)=true))). % 43.38/30.97 tff(c_11497, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__1), true)=true))). % 43.38/30.97 tff(c_31040, plain, (![X_515, Y_516]: (ifeq(iext(uri_rdf_subject, X_515, Y_516), true, icext(uri_rdfs_Statement, X_515), true)=true))). % 43.38/30.97 tff(c_6371, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_subClassOf), true)=true))). % 43.38/30.97 tff(c_10214, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_subject), true)=true))). % 43.38/30.97 tff(c_3308, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdf__1, uri_rdfs_Resource), true)=true))). % 43.38/30.97 tff(c_15153, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_first), true)=true))). % 43.38/30.97 tff(c_30898, plain, (![X_507, Y_508]: (ifeq(iext(uri_ex_sameCliqueAs, X_507, Y_508), true, icext(uri_ex_Clique, Y_508), true)=true))). % 43.38/30.97 tff(c_3354, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, sK5_testcase_premise_fullish_013_Cliques_BNODE_r, uri_owl_Restriction), true)=true))). % 43.38/30.97 tff(c_9731, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_owl_someValuesFrom), true)=true))). % 43.38/30.97 tff(c_13673, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_domain), true)=true))). % 43.38/30.97 tff(c_30741, plain, (![X_500, Y_501]: (ifeq(iext(uri_rdf_first, X_500, Y_501), true, icext(uri_rdf_List, X_500), true)=true))). % 43.38/30.97 tff(c_8610, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__1), true)=true))). % 43.38/30.97 tff(c_9467, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_subPropertyOf), true)=true))). % 43.38/30.97 tff(c_10213, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_subject), true)=true))). % 43.38/30.97 tff(c_2745, plain, (![E_104]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_104), true, iext(uri_rdfs_subClassOf, uri_rdfs_Seq, E_104), true)=true))). % 43.38/30.97 tff(c_9042, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_owl_onProperty), true)=true))). % 43.38/30.97 tff(c_10996, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_owl_propertyChainAxiom), true)=true))). % 43.38/30.97 tff(c_30188, plain, (![X_490, Y_491]: (ifeq(iext(uri_rdfs_range, X_490, Y_491), true, icext(uri_rdfs_Class, Y_491), true)=true))). % 43.38/30.97 tff(c_3339, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf__3, uri_rdfs_ContainerMembershipProperty), true)=true))). % 43.38/30.97 tff(c_14035, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_object), true)=true))). % 43.38/30.97 tff(c_29783, plain, (![X_484, Y_485]: (ifeq(iext(uri_rdfs_domain, X_484, Y_485), true, icext(uri_rdfs_Class, Y_485), true)=true))). % 43.38/30.97 tff(c_10997, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_owl_propertyChainAxiom), true)=true))). % 43.38/30.97 tff(c_3293, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdfs_range, uri_rdf_Property), true)=true))). % 43.38/30.97 tff(c_13672, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_domain), true)=true))). % 43.38/30.97 tff(c_28801, plain, (![X_476, Y_477]: (ifeq(iext(uri_rdfs_subClassOf, X_476, Y_477), true, icext(uri_rdfs_Class, X_476), true)=true))). % 43.38/30.97 tff(c_6187, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Datatype), true)=true))). % 43.38/30.97 tff(c_3357, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdf__3, uri_rdfs_Resource), true)=true))). % 43.38/30.97 tff(c_16093, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_rest), true)=true))). % 43.38/30.97 tff(c_12056, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, sK5_testcase_premise_fullish_013_Cliques_BNODE_r), true)=true))). % 43.38/30.97 tff(c_27998, plain, (![X_467, Y_468]: (ifeq(iext(uri_rdfs_subClassOf, X_467, Y_468), true, icext(uri_rdfs_Class, Y_468), true)=true))). % 43.38/30.97 tff(c_7692, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Literal), true)=true))). % 43.38/30.97 tff(c_3347, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_first, Q_107), true, iext(Q_107, sK1_testcase_premise_fullish_013_Cliques_BNODE_l1, uri_rdf_type), true)=true))). % 43.38/30.97 tff(c_5814, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_range), true)=true))). % 43.38/30.97 tff(c_9730, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_owl_someValuesFrom), true)=true))). % 43.38/30.97 tff(c_27421, plain, (![X_459, Y_460]: (ifeq(iext(uri_rdfs_subPropertyOf, X_459, Y_460), true, icext(uri_rdf_Property, Y_460), true)=true))). % 43.38/30.97 tff(c_16092, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_rest), true)=true))). % 43.38/30.97 tff(c_3349, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_rest, Q_107), true, iext(Q_107, sK1_testcase_premise_fullish_013_Cliques_BNODE_l1, sK2_testcase_premise_fullish_013_Cliques_BNODE_l2), true)=true))). % 43.38/30.97 tff(c_12863, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdf_Property), true)=true))). % 43.38/30.97 tff(c_15916, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__2), true)=true))). % 43.38/30.97 tff(c_11561, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_Bag), true)=true))). % 43.38/30.97 tff(c_27200, plain, (![X_450, Y_451]: (ifeq(iext(uri_rdf_rest, X_450, Y_451), true, icext(uri_rdf_List, Y_451), true)=true))). % 43.38/30.97 tff(c_6372, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_subClassOf), true)=true))). % 43.38/30.97 tff(c_12376, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_owl_sameAs), true)=true))). % 43.38/30.97 tff(c_3291, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf_type, uri_rdf_Property), true)=true))). % 43.38/30.97 tff(c_8542, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_ex_sameCliqueAs), true)=true))). % 43.38/30.97 tff(c_26625, plain, (![X_442, Y_443]: (ifeq(iext(uri_rdfs_subPropertyOf, X_442, Y_443), true, icext(uri_rdf_Property, X_442), true)=true))). % 43.38/30.97 tff(c_9043, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_owl_onProperty), true)=true))). % 43.38/30.97 tff(c_14213, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Class), true)=true))). % 43.38/30.97 tff(c_3318, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdfs_domain, uri_rdf_Property), true)=true))). % 43.38/30.97 tff(c_11895, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Resource), true)=true))). % 43.38/30.97 tff(c_26486, plain, (![X_434, Y_435]: (ifeq(iext(uri_rdfs_label, X_434, Y_435), true, icext(uri_rdfs_Literal, Y_435), true)=true))). % 43.38/30.97 tff(c_15152, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_first), true)=true))). % 43.38/30.97 tff(c_3337, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_107), true, iext(Q_107, uri_rdf_Alt, uri_rdfs_Container), true)=true))). % 43.38/30.97 tff(c_13869, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__3), true)=true))). % 43.38/30.97 tff(c_14034, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_object), true)=true))). % 43.38/30.97 tff(c_25969, plain, (![X_426, Y_427]: (ifeq(iext(uri_rdfs_domain, X_426, Y_427), true, icext(uri_rdf_Property, X_426), true)=true))). % 43.38/30.97 tff(c_14318, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Container), true)=true))). % 43.38/30.97 tff(c_14917, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_owl_inverseOf), true)=true))). % 43.38/30.97 tff(c_3329, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdf_value, uri_rdfs_Resource), true)=true))). % 43.38/30.97 tff(c_9936, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_value), true)=true))). % 43.38/30.97 tff(c_15915, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_member), true)=true))). % 43.38/30.97 tff(c_25811, plain, (![X_417, Y_418]: (ifeq(iext(uri_rdf_predicate, X_417, Y_418), true, icext(uri_rdfs_Statement, X_417), true)=true))). % 43.38/30.97 tff(c_9466, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_subPropertyOf), true)=true))). % 43.38/30.97 tff(c_3322, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdf__2, uri_rdfs_Resource), true)=true))). % 43.38/30.97 tff(c_13870, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__3), true)=true))). % 43.38/30.97 tff(c_25041, plain, (![X_410, Y_411]: (ifeq(iext(uri_rdf_type, X_410, Y_411), true, icext(uri_rdfs_Class, Y_411), true)=true))). % 43.38/30.97 tff(c_5626, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_29), true, icext(C_29, uri_rdfs_Resource), true)=true))). % 43.38/30.97 tff(c_5627, plain, (![C_19, X_139]: (ifeq(iext(uri_rdfs_domain, uri_rdf_type, C_19), true, icext(C_19, X_139), true)=true))). % 43.38/30.97 tff(c_24423, plain, (![X_33]: (ifeq(icext(uri_owl_Class, X_33), true, icext(uri_owl_Class, X_33), true)=true))). % 43.38/30.97 tff(c_3296, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdfs_subClassOf, uri_rdfs_Class), true)=true))). % 43.38/30.97 tff(c_24433, plain, (iext(uri_rdfs_subClassOf, uri_owl_Class, uri_rdfs_Resource)=true)). % 43.38/30.97 tff(c_24367, plain, (iext(uri_rdfs_subClassOf, uri_owl_Class, uri_owl_Class)=true)). % 43.38/30.97 tff(c_24291, plain, (iext(uri_rdf_type, uri_owl_Class, uri_rdfs_Class)=true)). % 43.38/30.97 tff(c_2112, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdf__1), true)=true))). % 43.38/30.97 tff(c_24100, plain, (ic(uri_owl_Class)=true)). % 43.38/30.97 tff(c_24034, plain, (icext(uri_rdfs_Class, uri_owl_Class)=true)). % 43.38/30.97 tff(c_2523, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_97), true, icext(C_97, uri_owl_Class), true)=true))). % 43.38/30.97 tff(c_2096, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_range), true)=true))). % 43.38/30.97 tff(c_2167, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf_subject), true)=true))). % 43.38/30.97 tff(c_2118, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdf_rest, C_93), true, icext(C_93, sK2_testcase_premise_fullish_013_Cliques_BNODE_l2), true)=true))). % 43.38/30.97 tff(c_2108, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_comment), true)=true))). % 43.38/30.97 tff(c_2503, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdf_rest, C_97), true, icext(C_97, uri_rdf_nil), true)=true))). % 43.38/30.97 tff(c_2141, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_seeAlso), true)=true))). % 43.38/30.97 tff(c_2508, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_owl_onProperty, C_97), true, icext(C_97, uri_ex_sameCliqueAs), true)=true))). % 43.38/30.97 tff(c_2088, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf_first), true)=true))). % 43.38/30.97 tff(c_2175, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_93), true, icext(C_93, uri_ex_Clique), true)=true))). % 43.38/30.97 tff(c_23578, plain, (![X_381, Y_382]: (ifeq(iext(uri_rdf_object, X_381, Y_382), true, icext(uri_rdfs_Statement, X_381), true)=true))). % 43.38/30.97 tff(c_2521, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdf_rest, C_97), true, icext(C_97, sK4_testcase_premise_fullish_013_Cliques_BNODE_l3), true)=true))). % 43.38/30.97 tff(c_2127, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_93), true, icext(C_93, uri_rdf_Bag), true)=true))). % 43.38/30.97 tff(c_2562, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdf_first, C_97), true, icext(C_97, uri_rdf_type), true)=true))). % 43.38/30.97 tff(c_2168, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdf__3), true)=true))). % 43.38/30.97 tff(c_2566, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdf_first, C_97), true, icext(C_97, sK3_testcase_premise_fullish_013_Cliques_BNODE_i), true)=true))). % 43.38/30.97 tff(c_2101, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_93), true, icext(C_93, uri_rdfs_Seq), true)=true))). % 43.38/30.97 tff(c_2547, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_97), true, icext(C_97, uri_rdf_List), true)=true))). % 43.38/30.97 tff(c_2164, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf_type), true)=true))). % 43.38/30.97 tff(c_2134, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_93), true, icext(C_93, uri_rdfs_Datatype), true)=true))). % 43.38/30.97 tff(c_2145, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_subPropertyOf), true)=true))). % 43.38/30.97 tff(c_2533, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_owl_someValuesFrom, C_97), true, icext(C_97, uri_ex_Clique), true)=true))). % 43.38/30.97 tff(c_2143, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdf_rest), true)=true))). % 43.38/30.97 tff(c_22451, plain, (![X_358, Y_359]: (ifeq(iext(uri_rdf_rest, X_358, Y_359), true, icext(uri_rdf_List, X_358), true)=true))). % 43.38/30.97 tff(c_2107, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf_value), true)=true))). % 43.38/30.97 tff(c_2172, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_ex_sameCliqueAs), true)=true))). % 43.38/30.97 tff(c_22924, plain, (![X_33]: (ifeq(icext(uri_owl_Restriction, X_33), true, icext(uri_owl_Restriction, X_33), true)=true))). % 43.38/30.97 tff(c_22934, plain, (iext(uri_rdfs_subClassOf, uri_owl_Restriction, uri_rdfs_Resource)=true)). % 43.38/30.97 tff(c_22868, plain, (iext(uri_rdfs_subClassOf, uri_owl_Restriction, uri_owl_Restriction)=true)). % 43.38/30.97 tff(c_2138, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_93), true, icext(C_93, uri_rdfs_ContainerMembershipProperty), true)=true))). % 43.38/30.97 tff(c_22796, plain, (iext(uri_rdf_type, uri_owl_Restriction, uri_rdfs_Class)=true)). % 43.38/30.97 tff(c_22614, plain, (ic(uri_owl_Restriction)=true)). % 43.38/30.97 tff(c_22551, plain, (icext(uri_rdfs_Class, uri_owl_Restriction)=true)). % 43.38/30.97 tff(c_2569, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_97), true, icext(C_97, uri_owl_Restriction), true)=true))). % 43.38/30.97 tff(c_2580, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_97), true, icext(C_97, sK5_testcase_premise_fullish_013_Cliques_BNODE_r), true)=true))). % 43.38/30.97 tff(c_2133, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdf_predicate), true)=true))). % 43.38/30.97 tff(c_2097, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdf_type), true)=true))). % 43.38/30.97 tff(c_2135, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_seeAlso), true)=true))). % 43.38/30.97 tff(c_2131, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_owl_someValuesFrom, C_93), true, icext(C_93, sK5_testcase_premise_fullish_013_Cliques_BNODE_r), true)=true))). % 43.38/30.97 tff(c_2557, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdf_first, C_97), true, icext(C_97, uri_ex_sameCliqueAs), true)=true))). % 43.38/30.97 tff(c_2155, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_93), true, icext(C_93, uri_rdf_XMLLiteral), true)=true))). % 43.38/30.97 tff(c_2093, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_comment), true)=true))). % 43.38/30.97 tff(c_2130, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf__2), true)=true))). % 43.38/30.97 tff(c_2142, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_93), true, icext(C_93, uri_ex_sameCliqueAs), true)=true))). % 43.38/30.97 tff(c_2554, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_97), true, icext(C_97, uri_rdfs_Class), true)=true))). % 43.38/30.97 tff(c_2537, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_97), true, icext(C_97, uri_rdfs_Class), true)=true))). % 43.38/30.97 tff(c_2157, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdf_first, C_93), true, icext(C_93, sK1_testcase_premise_fullish_013_Cliques_BNODE_l1), true)=true))). % 43.38/30.97 tff(c_21629, plain, (![X_332, Y_333]: (ifeq(iext(uri_rdfs_comment, X_332, Y_333), true, icext(uri_rdfs_Literal, Y_333), true)=true))). % 43.38/30.97 tff(c_2152, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf_predicate), true)=true))). % 43.38/30.97 tff(c_2136, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_owl_inverseOf, C_93), true, icext(C_93, sK3_testcase_premise_fullish_013_Cliques_BNODE_i), true)=true))). % 43.38/30.97 tff(c_2146, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_93), true, icext(C_93, uri_rdf_Alt), true)=true))). % 43.38/30.97 tff(c_2147, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdf_first), true)=true))). % 43.38/30.97 tff(c_2111, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_range), true)=true))). % 43.38/30.97 tff(c_21764, plain, (iext(uri_rdf_type, sK1_testcase_premise_fullish_013_Cliques_BNODE_l1, uri_rdf_List)=true)). % 43.38/30.97 tff(c_21708, plain, (icext(uri_rdf_List, sK1_testcase_premise_fullish_013_Cliques_BNODE_l1)=true)). % 43.38/30.98 tff(c_2159, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdf_rest, C_93), true, icext(C_93, sK1_testcase_premise_fullish_013_Cliques_BNODE_l1), true)=true))). % 43.38/30.98 tff(c_2098, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf_rest), true)=true))). % 43.38/30.98 tff(c_2534, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_97), true, icext(C_97, uri_rdfs_Literal), true)=true))). % 43.38/30.98 tff(c_2103, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_93), true, icext(C_93, uri_rdfs_isDefinedBy), true)=true))). % 43.38/30.98 tff(c_2540, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_owl_inverseOf, C_97), true, icext(C_97, uri_rdf_type), true)=true))). % 43.38/30.98 tff(c_2501, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdf_List), true)=true))). % 43.38/30.98 tff(c_2126, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_member), true)=true))). % 43.38/30.98 tff(c_2150, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdf_subject), true)=true))). % 43.38/30.98 tff(c_21146, plain, (![X_33]: (ifeq(icext(uri_ex_JoesGang, X_33), true, icext(uri_ex_JoesGang, X_33), true)=true))). % 43.38/30.98 tff(c_21181, plain, (iext(uri_rdfs_subClassOf, uri_ex_JoesGang, uri_rdfs_Resource)=true)). % 43.38/30.98 tff(c_2564, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdf_rest, C_97), true, icext(C_97, sK2_testcase_premise_fullish_013_Cliques_BNODE_l2), true)=true))). % 43.38/30.98 tff(c_21090, plain, (iext(uri_rdfs_subClassOf, uri_ex_JoesGang, uri_ex_JoesGang)=true)). % 43.38/30.98 tff(c_20903, plain, (iext(uri_rdf_type, uri_ex_JoesGang, uri_rdfs_Class)=true)). % 43.38/30.98 tff(c_20862, plain, (ic(uri_ex_JoesGang)=true)). % 43.38/30.98 tff(c_20763, plain, (icext(uri_rdfs_Class, uri_ex_JoesGang)=true)). % 43.38/30.98 tff(c_2561, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_97), true, icext(C_97, uri_ex_JoesGang), true)=true))). % 43.38/30.98 tff(c_2116, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_owl_propertyChainAxiom, C_93), true, icext(C_93, uri_foaf_knows), true)=true))). % 43.38/30.98 tff(c_2114, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf__1), true)=true))). % 43.38/30.98 tff(c_17111, plain, (![X_33]: (ifeq(icext(uri_rdfs_Statement, X_33), true, icext(uri_rdfs_Statement, X_33), true)=true))). % 43.38/30.98 tff(c_18361, plain, (![X_33]: (ifeq(icext(uri_owl_ObjectProperty, X_33), true, icext(uri_owl_ObjectProperty, X_33), true)=true))). % 43.38/30.98 tff(c_20108, plain, (![X_33]: (ifeq(icext(uri_rdf_List, X_33), true, icext(uri_rdf_List, X_33), true)=true))). % 43.38/30.98 tff(c_13181, plain, (![X_33]: (ifeq(icext(uri_ex_Clique, X_33), true, icext(uri_ex_Clique, X_33), true)=true))). % 43.38/30.98 tff(c_6189, plain, (![X_33]: (ifeq(icext(uri_rdfs_Datatype, X_33), true, icext(uri_rdfs_Datatype, X_33), true)=true))). % 43.38/30.98 tff(c_11661, plain, (![X_33]: (ifeq(icext(uri_rdfs_Seq, X_33), true, icext(uri_rdfs_Seq, X_33), true)=true))). % 43.38/30.98 tff(c_18917, plain, (![X_296, Y_297]: (ifeq(iext(uri_rdfs_range, X_296, Y_297), true, icext(uri_rdf_Property, X_296), true)=true))). % 43.38/30.98 tff(c_7192, plain, (![X_33]: (ifeq(icext(uri_rdfs_Container, X_33), true, icext(uri_rdfs_Container, X_33), true)=true))). % 43.38/30.98 tff(c_15287, plain, (![X_33]: (ifeq(icext(uri_rdf_Alt, X_33), true, icext(uri_rdf_Alt, X_33), true)=true))). % 43.38/30.98 tff(c_20118, plain, (iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdfs_Resource)=true)). % 43.38/30.98 tff(c_20052, plain, (iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdf_List)=true)). % 43.38/30.98 tff(c_20005, plain, (iext(uri_rdf_type, uri_rdf_List, uri_rdfs_Class)=true)). % 43.38/30.98 tff(c_2546, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_97), true, icext(C_97, uri_owl_sameAs), true)=true))). % 43.38/30.98 tff(c_19814, plain, (ic(uri_rdf_List)=true)). % 43.38/30.98 tff(c_19752, plain, (icext(uri_rdfs_Class, uri_rdf_List)=true)). % 43.38/30.98 tff(c_2509, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_97), true, icext(C_97, uri_rdf_List), true)=true))). % 43.38/30.98 tff(c_19667, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_comment, uri_rdfs_comment)=true)). % 43.38/30.98 tff(c_19602, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_predicate, uri_rdf_predicate)=true)). % 43.38/30.98 tff(c_19561, plain, (ip(uri_rdf_predicate)=true)). % 43.38/30.98 tff(c_19479, plain, (iext(uri_rdf_type, uri_rdf_predicate, uri_rdf_Property)=true)). % 43.38/30.98 tff(c_19438, plain, (ip(uri_rdfs_comment)=true)). % 43.38/30.98 tff(c_19360, plain, (iext(uri_rdf_type, uri_rdfs_comment, uri_rdf_Property)=true)). % 43.38/30.98 tff(c_2124, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_member), true)=true))). % 43.38/30.98 tff(c_19010, plain, (icext(uri_rdf_Property, uri_rdf_predicate)=true)). % 43.38/30.98 tff(c_19003, plain, (icext(uri_rdf_Property, uri_rdfs_comment)=true)). % 43.38/30.98 tff(c_15221, plain, (![X_33]: (ifeq(icext(uri_rdfs_ContainerMembershipProperty, X_33), true, icext(uri_rdfs_ContainerMembershipProperty, X_33), true)=true))). % 43.38/30.98 tff(c_10030, plain, (![X_33]: (ifeq(icext(uri_rdfs_Literal, X_33), true, icext(uri_rdfs_Literal, X_33), true)=true))). % 43.38/30.98 tff(c_12864, plain, (![X_33]: (ifeq(icext(uri_rdf_Property, X_33), true, icext(uri_rdf_Property, X_33), true)=true))). % 43.38/30.98 tff(c_18371, plain, (iext(uri_rdfs_subClassOf, uri_owl_ObjectProperty, uri_rdfs_Resource)=true)). % 43.38/30.98 tff(c_18305, plain, (iext(uri_rdfs_subClassOf, uri_owl_ObjectProperty, uri_owl_ObjectProperty)=true)). % 43.38/30.98 tff(c_18233, plain, (iext(uri_rdf_type, uri_owl_ObjectProperty, uri_rdfs_Class)=true)). % 43.38/30.98 tff(c_2512, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdfs_Class), true)=true))). % 43.38/30.98 tff(c_18074, plain, (ic(uri_owl_ObjectProperty)=true)). % 43.38/30.98 tff(c_18008, plain, (icext(uri_rdfs_Class, uri_owl_ObjectProperty)=true)). % 43.38/30.98 tff(c_2579, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_97), true, icext(C_97, uri_owl_ObjectProperty), true)=true))). % 43.38/30.98 tff(c_11563, plain, (![X_33]: (ifeq(icext(uri_rdf_Bag, X_33), true, icext(uri_rdf_Bag, X_33), true)=true))). % 43.38/30.98 tff(c_12057, plain, (![X_33]: (ifeq(icext(sK5_testcase_premise_fullish_013_Cliques_BNODE_r, X_33), true, icext(sK5_testcase_premise_fullish_013_Cliques_BNODE_r, X_33), true)=true))). % 43.38/30.98 tff(c_13271, plain, (![X_33]: (ifeq(icext(uri_rdf_XMLLiteral, X_33), true, icext(uri_rdf_XMLLiteral, X_33), true)=true))). % 43.38/30.98 tff(c_14214, plain, (![X_33]: (ifeq(icext(uri_rdfs_Class, X_33), true, icext(uri_rdfs_Class, X_33), true)=true))). % 43.38/30.98 tff(c_17793, plain, (iext(uri_rdf_type, uri_rdfs_Resource, uri_rdfs_Class)=true)). % 43.38/30.98 tff(c_17699, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_label, uri_rdfs_label)=true)). % 43.38/30.98 tff(c_17630, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_member, uri_rdfs_member)=true)). % 43.38/30.98 tff(c_17467, plain, (icext(uri_rdf_Property, uri_rdfs_member)=true)). % 43.38/30.98 tff(c_17412, plain, (iext(uri_rdf_type, uri_rdfs_member, uri_rdf_Property)=true)). % 43.38/30.98 tff(c_17339, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Resource, uri_rdfs_Resource)=true)). % 43.38/30.98 tff(c_2104, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_owl_onProperty, C_93), true, icext(C_93, sK5_testcase_premise_fullish_013_Cliques_BNODE_r), true)=true))). % 43.38/30.98 tff(c_17121, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Statement, uri_rdfs_Resource)=true)). % 43.38/30.98 tff(c_17055, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Statement, uri_rdfs_Statement)=true)). % 43.38/30.98 tff(c_17008, plain, (iext(uri_rdf_type, uri_rdf_Bag, uri_rdfs_Class)=true)). % 43.38/30.98 tff(c_2499, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdf_Property), true)=true))). % 43.38/30.98 tff(c_16928, plain, (iext(uri_rdf_type, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Class)=true)). % 43.38/30.98 tff(c_16878, plain, (iext(uri_rdf_type, uri_rdf_XMLLiteral, uri_rdfs_Class)=true)). % 43.38/30.98 tff(c_16830, plain, (iext(uri_rdf_type, uri_rdfs_Container, uri_rdfs_Class)=true)). % 43.38/30.98 tff(c_16783, plain, (iext(uri_rdf_type, uri_ex_JoesGang, sK5_testcase_premise_fullish_013_Cliques_BNODE_r)=true)). % 43.38/30.98 tff(c_16736, plain, (iext(uri_rdf_type, uri_rdfs_Literal, uri_rdfs_Class)=true)). % 43.38/30.98 tff(c_2090, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf__3), true)=true))). % 43.38/30.98 tff(c_16654, plain, (iext(uri_rdf_type, sK5_testcase_premise_fullish_013_Cliques_BNODE_r, uri_rdfs_Class)=true)). % 43.38/30.98 tff(c_16582, plain, (iext(uri_rdf_type, uri_rdfs_Datatype, uri_rdfs_Class)=true)). % 43.38/30.98 tff(c_2100, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdf_rest, C_93), true, icext(C_93, sK4_testcase_premise_fullish_013_Cliques_BNODE_l3), true)=true))). % 43.38/30.98 tff(c_16533, plain, (iext(uri_rdf_type, uri_rdf_Alt, uri_rdfs_Class)=true)). % 43.38/30.98 tff(c_16486, plain, (iext(uri_rdf_type, uri_rdfs_Seq, uri_rdfs_Class)=true)). % 43.38/30.98 tff(c_16436, plain, (iext(uri_rdf_type, uri_rdfs_Class, uri_rdfs_Class)=true)). % 43.38/30.98 tff(c_16389, plain, (iext(uri_rdf_type, uri_ex_Clique, uri_rdfs_Class)=true)). % 43.38/30.98 tff(c_2543, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_97), true, icext(C_97, uri_rdf_Property), true)=true))). % 43.38/30.98 tff(c_16322, plain, (ip(uri_rdfs_label)=true)). % 43.38/30.98 tff(c_16269, plain, (iext(uri_rdf_type, uri_rdfs_label, uri_rdf_Property)=true)). % 43.38/30.98 tff(c_16197, plain, (iext(uri_rdf_type, uri_rdfs_Statement, uri_rdfs_Class)=true)). % 43.38/30.98 tff(c_16150, plain, (iext(uri_rdf_type, sK2_testcase_premise_fullish_013_Cliques_BNODE_l2, uri_rdf_List)=true)). % 43.38/30.98 tff(c_16103, plain, (iext(uri_rdf_type, sK4_testcase_premise_fullish_013_Cliques_BNODE_l3, uri_rdf_List)=true)). % 43.38/30.98 tff(c_16037, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_rest, uri_rdf_rest)=true)). % 43.38/30.98 tff(c_15861, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__2, uri_rdfs_member)=true)). % 43.38/30.98 tff(c_15820, plain, (icext(uri_rdf_List, sK2_testcase_premise_fullish_013_Cliques_BNODE_l2)=true)). % 43.38/30.98 tff(c_2151, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdf_first, C_93), true, icext(C_93, sK2_testcase_premise_fullish_013_Cliques_BNODE_l2), true)=true))). % 43.38/30.98 tff(c_15648, plain, (ic(uri_rdfs_Statement)=true)). % 43.38/30.98 tff(c_15590, plain, (icext(uri_rdfs_Class, uri_rdfs_Statement)=true)). % 43.38/30.98 tff(c_2567, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdfs_Statement), true)=true))). % 43.38/30.98 tff(c_15389, plain, (iext(uri_rdfs_subClassOf, uri_ex_Clique, uri_rdfs_Resource)=true)). % 43.38/30.98 tff(c_15297, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, uri_rdfs_isDefinedBy)=true)). % 43.38/30.98 tff(c_2553, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_97), true, icext(C_97, uri_rdfs_ContainerMembershipProperty), true)=true))). % 43.38/30.98 tff(c_15231, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdf_Alt)=true)). % 43.38/30.98 tff(c_15165, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdfs_ContainerMembershipProperty)=true)). % 43.38/30.98 tff(c_15098, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_first, uri_rdf_first)=true)). % 43.38/30.98 tff(c_1611, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_subClassOf, S_5, O_6), true, true, true)=true))). % 43.38/30.98 tff(c_14929, plain, (iext(uri_rdf_type, uri_rdfs_isDefinedBy, uri_rdf_Property)=true)). % 43.38/30.98 tff(c_14834, plain, (iext(uri_rdfs_subPropertyOf, uri_owl_inverseOf, uri_owl_inverseOf)=true)). % 43.38/30.98 tff(c_2578, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_97), true, icext(C_97, uri_ex_Clique), true)=true))). % 43.38/30.98 tff(c_14686, plain, (icext(uri_rdf_Property, uri_ex_sameCliqueAs)=true)). % 43.38/30.98 tff(c_14632, plain, (iext(uri_rdf_type, uri_ex_sameCliqueAs, uri_rdf_Property)=true)). % 43.38/30.98 tff(c_2577, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_97), true, icext(C_97, uri_ex_Clique), true)=true))). % 43.38/30.98 tff(c_14432, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Resource)=true)). % 43.38/30.98 tff(c_14234, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Container, uri_rdfs_Resource)=true)). % 43.38/30.98 tff(c_2128, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdf__2), true)=true))). % 43.38/30.98 tff(c_3588, plain, (![S_5, O_6]: (ifeq(iext(uri_owl_inverseOf, S_5, O_6), true, true, true)=true))). % 43.38/30.98 tff(c_14155, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdfs_Class)=true)). % 43.38/30.98 tff(c_13979, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_object, uri_rdf_object)=true)). % 43.38/30.98 tff(c_3964, plain, (![S_5, O_6]: (ifeq(iext(uri_owl_sameAs, S_5, O_6), true, true, true)=true))). % 43.38/30.98 tff(c_13815, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__3, uri_rdf__3)=true)). % 43.38/30.98 tff(c_2500, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_97), true, icext(C_97, uri_rdfs_Class), true)=true))). % 43.38/30.98 tff(c_13618, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, uri_rdfs_domain)=true)). % 43.38/30.98 tff(c_2120, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_label), true)=true))). % 43.38/30.98 tff(c_13281, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdfs_Resource)=true)). % 43.38/30.98 tff(c_13216, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdf_XMLLiteral)=true)). % 43.38/30.98 tff(c_2109, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_subClassOf), true)=true))). % 43.38/30.98 tff(c_13129, plain, (iext(uri_rdfs_subClassOf, uri_ex_Clique, uri_ex_Clique)=true)). % 43.38/30.98 tff(c_13064, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__2, uri_rdf__2)=true)). % 43.38/30.98 tff(c_1377, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_range, S_5, O_6), true, true, true)=true))). % 43.38/30.98 tff(c_2507, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_97), true, icext(C_97, uri_rdfs_seeAlso), true)=true))). % 43.38/30.98 tff(c_12805, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdf_Property)=true)). % 43.38/30.98 tff(c_12760, plain, (icext(uri_rdf_List, sK4_testcase_premise_fullish_013_Cliques_BNODE_l3)=true)). % 43.38/30.98 tff(c_2161, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdf_first, C_93), true, icext(C_93, sK4_testcase_premise_fullish_013_Cliques_BNODE_l3), true)=true))). % 43.38/30.98 tff(c_12618, plain, (icext(uri_rdf_Property, uri_owl_propertyChainAxiom)=true)). % 43.38/30.98 tff(c_12564, plain, (iext(uri_rdf_type, uri_owl_propertyChainAxiom, uri_rdf_Property)=true)). % 43.38/30.98 tff(c_12440, plain, (icext(uri_rdf_Property, uri_owl_inverseOf)=true)). % 43.38/30.98 tff(c_12386, plain, (iext(uri_rdf_type, uri_owl_inverseOf, uri_rdf_Property)=true)). % 43.38/30.98 tff(c_12321, plain, (iext(uri_rdfs_subPropertyOf, uri_owl_sameAs, uri_owl_sameAs)=true)). % 43.38/30.98 tff(c_12197, plain, (icext(uri_rdf_Property, uri_rdfs_range)=true)). % 43.38/30.98 tff(c_12143, plain, (iext(uri_rdf_type, uri_rdfs_range, uri_rdf_Property)=true)). % 43.38/30.98 tff(c_12002, plain, (iext(uri_rdfs_subClassOf, sK5_testcase_premise_fullish_013_Cliques_BNODE_r, sK5_testcase_premise_fullish_013_Cliques_BNODE_r)=true)). % 43.38/30.98 tff(c_11841, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Resource)=true)). % 43.38/30.98 tff(c_11725, plain, (icext(uri_rdf_Property, uri_owl_sameAs)=true)). % 43.38/30.98 tff(c_11671, plain, (iext(uri_rdf_type, uri_owl_sameAs, uri_rdf_Property)=true)). % 43.38/30.98 tff(c_11602, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Seq)=true)). % 43.38/30.98 tff(c_2099, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_subClassOf), true)=true))). % 43.38/30.98 tff(c_11507, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdf_Bag)=true)). % 43.38/30.98 tff(c_11442, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__1, uri_rdfs_member)=true)). % 43.38/30.98 tff(c_2519, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_owl_propertyChainAxiom, C_97), true, icext(C_97, sK1_testcase_premise_fullish_013_Cliques_BNODE_l1), true)=true))). % 43.38/30.98 tff(c_11294, plain, (ip(uri_rdfs_member)=true)). % 43.38/30.98 tff(c_11206, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__3, uri_rdfs_member)=true)). % 43.38/30.98 tff(c_11086, plain, (icext(uri_rdf_Property, uri_owl_onProperty)=true)). % 43.38/30.98 tff(c_2162, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf_object), true)=true))). % 43.38/30.98 tff(c_11008, plain, (iext(uri_rdf_type, uri_owl_onProperty, uri_rdf_Property)=true)). % 43.38/30.98 tff(c_10942, plain, (iext(uri_rdfs_subPropertyOf, uri_owl_propertyChainAxiom, uri_owl_propertyChainAxiom)=true)). % 43.38/30.98 tff(c_2560, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_97), true, icext(C_97, uri_rdfs_Literal), true)=true))). % 43.38/30.98 tff(c_10572, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdfs_Resource)=true)). % 43.38/30.98 tff(c_10380, plain, (icext(uri_rdf_Property, uri_owl_someValuesFrom)=true)). % 43.38/30.98 tff(c_10327, plain, (iext(uri_rdf_type, uri_owl_someValuesFrom, uri_rdf_Property)=true)). % 43.38/30.98 tff(c_3730, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_subPropertyOf, S_5, O_6), true, true, true)=true))). % 43.38/30.98 tff(c_2598, plain, (![S_5, O_6]: (ifeq(iext(uri_ex_sameCliqueAs, S_5, O_6), true, true, true)=true))). % 43.38/30.98 tff(c_10159, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_subject, uri_rdf_subject)=true)). % 43.38/30.98 tff(c_9972, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdfs_Literal)=true)). % 43.38/30.98 tff(c_2117, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_domain), true)=true))). % 43.38/30.98 tff(c_9881, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_value, uri_rdf_value)=true)). % 43.38/30.98 tff(c_2545, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdfs_Resource), true)=true))). % 43.38/30.98 tff(c_9676, plain, (iext(uri_rdfs_subPropertyOf, uri_owl_someValuesFrom, uri_owl_someValuesFrom)=true)). % 43.38/30.98 tff(c_3846, plain, (![S_5, O_6]: (ifeq(iext(uri_rdf_object, S_5, O_6), true, true, true)=true))). % 43.38/30.98 tff(c_2137, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdf_value), true)=true))). % 43.38/30.98 tff(c_9409, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf)=true)). % 43.38/30.98 tff(c_9210, plain, (iext(uri_rdfs_subClassOf, sK5_testcase_premise_fullish_013_Cliques_BNODE_r, uri_rdfs_Resource)=true)). % 43.38/30.98 tff(c_2102, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_isDefinedBy), true)=true))). % 43.38/30.98 tff(c_9053, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Resource)=true)). % 43.38/30.98 tff(c_8992, plain, (iext(uri_rdfs_subPropertyOf, uri_owl_onProperty, uri_owl_onProperty)=true)). % 43.38/30.98 tff(c_3772, plain, (![S_5, O_6]: (ifeq(iext(uri_owl_propertyChainAxiom, S_5, O_6), true, true, true)=true))). % 43.38/30.98 tff(c_2575, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_97), true, icext(C_97, uri_rdfs_Datatype), true)=true))). % 43.38/30.98 tff(c_8640, plain, (icext(uri_rdf_Property, uri_rdfs_label)=true)). % 43.38/30.98 tff(c_2132, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_label), true)=true))). % 43.38/30.98 tff(c_8553, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__1, uri_rdf__1)=true)). % 43.38/30.98 tff(c_8489, plain, (iext(uri_rdfs_subPropertyOf, uri_ex_sameCliqueAs, uri_ex_sameCliqueAs)=true)). % 43.38/30.98 tff(c_8123, plain, (icext(uri_rdf_Property, uri_rdfs_subClassOf)=true)). % 43.38/30.98 tff(c_8042, plain, (iext(uri_rdf_type, uri_rdfs_subClassOf, uri_rdf_Property)=true)). % 43.38/30.98 tff(c_1463, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_domain, S_5, O_6), true, true, true)=true))). % 43.38/30.98 tff(c_2549, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_97), true, icext(C_97, uri_rdf_Property), true)=true))). % 43.38/30.98 tff(c_7641, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdfs_Resource)=true)). % 43.38/30.98 tff(c_2166, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_subPropertyOf), true)=true))). % 43.38/30.98 tff(c_7528, plain, (icext(uri_rdf_Property, uri_rdfs_subPropertyOf)=true)). % 43.38/30.98 tff(c_7475, plain, (iext(uri_rdf_type, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 43.38/30.98 tff(c_7380, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Resource)=true)). % 43.38/30.98 tff(c_7287, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Resource)=true)). % 43.38/30.98 tff(c_2550, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_97), true, icext(C_97, uri_rdfs_Container), true)=true))). % 43.38/30.98 tff(c_7133, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Container, uri_rdfs_Container)=true)). % 43.38/30.98 tff(c_2539, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_97), true, icext(C_97, uri_rdfs_Resource), true)=true))). % 43.38/30.98 tff(c_6981, plain, (icext(uri_rdf_Property, uri_rdfs_domain)=true)). % 43.38/30.98 tff(c_2125, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_domain), true)=true))). % 43.38/30.98 tff(c_6906, plain, (iext(uri_rdf_type, uri_rdfs_domain, uri_rdf_Property)=true)). % 43.38/30.98 tff(c_2498, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_97), true, icext(C_97, uri_rdf_Property), true)=true))). % 43.38/30.98 tff(c_6701, plain, (icext(uri_rdf_Property, uri_rdfs_seeAlso)=true)). % 43.38/30.98 tff(c_6657, plain, (icext(uri_rdf_Property, uri_rdfs_isDefinedBy)=true)). % 43.38/30.98 tff(c_2154, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_isDefinedBy), true)=true))). % 43.38/30.98 tff(c_6586, plain, (iext(uri_rdf_type, uri_rdfs_seeAlso, uri_rdf_Property)=true)). % 43.38/30.98 tff(c_1777, plain, (![X_90]: (ifeq(icext(uri_rdf_XMLLiteral, X_90), true, icext(uri_rdfs_Literal, X_90), true)=true))). % 43.38/30.98 tff(c_3423, plain, (![S_5, O_6]: (ifeq(iext(uri_owl_onProperty, S_5, O_6), true, true, true)=true))). % 43.38/30.98 tff(c_1774, plain, (![X_90]: (ifeq(icext(uri_rdfs_Datatype, X_90), true, icext(uri_rdfs_Class, X_90), true)=true))). % 43.38/30.98 tff(c_2664, plain, (![S_5, O_6]: (ifeq(iext(uri_rdf_rest, S_5, O_6), true, true, true)=true))). % 43.38/30.98 tff(c_6321, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, uri_rdfs_subClassOf)=true)). % 43.38/30.98 tff(c_6229, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_type, uri_rdf_type)=true)). % 43.38/30.98 tff(c_1776, plain, (![X_90]: (ifeq(icext(uri_rdf_Alt, X_90), true, icext(uri_rdfs_Container, X_90), true)=true))). % 43.38/30.98 tff(c_6137, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Datatype)=true)). % 43.38/30.98 tff(c_3548, plain, (![S_5, O_6]: (ifeq(iext(uri_owl_someValuesFrom, S_5, O_6), true, true, true)=true))). % 43.38/30.98 tff(c_6054, plain, (icext(uri_rdfs_Class, uri_rdfs_Resource)=true)). % 43.38/30.98 tff(c_1772, plain, (![X_90]: (ifeq(icext(uri_rdfs_Seq, X_90), true, icext(uri_rdfs_Container, X_90), true)=true))). % 43.38/30.98 tff(c_6007, plain, (icext(sK5_testcase_premise_fullish_013_Cliques_BNODE_r, uri_ex_JoesGang)=true)). % 43.38/30.98 tff(c_1778, plain, (![X_90]: (ifeq(icext(uri_ex_Clique, X_90), true, icext(sK5_testcase_premise_fullish_013_Cliques_BNODE_r, X_90), true)=true))). % 43.38/30.98 tff(c_5946, plain, (ic(uri_rdfs_Resource)=true)). % 43.38/30.98 tff(c_5885, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Resource)=true)). % 43.38/30.98 tff(c_1775, plain, (![X_90]: (ifeq(icext(uri_rdfs_ContainerMembershipProperty, X_90), true, icext(uri_rdf_Property, X_90), true)=true))). % 43.38/30.98 tff(c_5759, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_range, uri_rdfs_range)=true)). % 43.38/30.98 tff(c_5698, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_seeAlso, uri_rdfs_seeAlso)=true)). % 43.38/30.98 tff(c_1773, plain, (![X_90]: (ifeq(icext(uri_rdf_Bag, X_90), true, icext(uri_rdfs_Container, X_90), true)=true))). % 43.38/30.98 tff(c_5585, plain, (![X_138]: (iext(uri_rdf_type, X_138, uri_rdfs_Resource)=true))). % 43.38/30.98 tff(c_2535, plain, (![X_98, Y_99]: (ifeq(iext(uri_rdf_predicate, X_98, Y_99), true, true, true)=true))). % 43.38/30.98 tff(c_2530, plain, (![X_98, Y_99]: (ifeq(iext(uri_rdf__2, X_98, Y_99), true, true, true)=true))). % 43.38/30.98 tff(c_2092, plain, (![X_94, Y_95]: (ifeq(iext(uri_rdfs_comment, X_94, Y_95), true, true, true)=true))). % 43.38/30.98 tff(c_2551, plain, (![X_98, Y_99]: (ifeq(iext(uri_rdf_first, X_98, Y_99), true, true, true)=true))). % 43.38/30.98 tff(c_2515, plain, (![X_98, Y_99]: (ifeq(iext(uri_rdf__1, X_98, Y_99), true, true, true)=true))). % 43.38/30.98 tff(c_2089, plain, (![X_94, Y_95]: (ifeq(iext(uri_rdf__3, X_94, Y_95), true, true, true)=true))). % 43.38/30.98 tff(c_2163, plain, (![X_94, Y_95]: (ifeq(iext(uri_rdf_type, X_94, Y_95), true, true, true)=true))). % 43.38/30.98 tff(c_2140, plain, (![X_94, Y_95]: (ifeq(iext(uri_rdfs_seeAlso, X_94, Y_95), true, true, true)=true))). % 43.38/30.98 tff(c_5384, plain, (icext(uri_rdfs_Class, uri_rdfs_Literal)=true)). % 43.38/30.98 tff(c_2505, plain, (![X_98, Y_99]: (ifeq(iext(uri_rdfs_isDefinedBy, X_98, Y_99), true, true, true)=true))). % 43.38/30.98 tff(c_5330, plain, (icext(uri_rdfs_Class, sK5_testcase_premise_fullish_013_Cliques_BNODE_r)=true)). % 43.38/30.98 tff(c_5285, plain, (icext(uri_rdfs_Class, uri_rdfs_Class)=true)). % 43.38/30.98 tff(c_2106, plain, (![X_94, Y_95]: (ifeq(iext(uri_rdf_value, X_94, Y_95), true, true, true)=true))). % 43.38/30.98 tff(c_5231, plain, (icext(uri_rdfs_Class, uri_rdf_Alt)=true)). % 43.38/30.98 tff(c_5186, plain, (icext(uri_rdfs_Class, uri_rdfs_Container)=true)). % 43.38/30.99 tff(c_5140, plain, (icext(uri_rdfs_Class, uri_rdf_XMLLiteral)=true)). % 43.38/30.99 tff(c_2119, plain, (![X_94, Y_95]: (ifeq(iext(uri_rdfs_label, X_94, Y_95), true, true, true)=true))). % 43.38/30.99 tff(c_5090, plain, (icext(uri_rdfs_Class, uri_rdf_Bag)=true)). % 43.38/30.99 tff(c_5047, plain, (icext(uri_rdfs_Class, uri_ex_Clique)=true)). % 43.38/30.99 tff(c_4993, plain, (icext(uri_rdfs_Class, uri_rdfs_ContainerMembershipProperty)=true)). % 43.38/30.99 tff(c_2555, plain, (![X_98, Y_99]: (ifeq(iext(uri_rdf_subject, X_98, Y_99), true, true, true)=true))). % 43.38/30.99 tff(c_4944, plain, (icext(uri_rdfs_Class, uri_rdfs_Datatype)=true)). % 43.38/30.99 tff(c_4901, plain, (icext(uri_rdfs_Class, uri_rdfs_Seq)=true)). % 43.38/30.99 tff(c_2123, plain, (![X_94, Y_95]: (ifeq(iext(uri_rdfs_member, X_94, Y_95), true, true, true)=true))). % 43.38/30.99 tff(c_4838, plain, (icext(uri_rdf_Property, uri_rdf_value)=true)). % 43.38/30.99 tff(c_4797, plain, (icext(uri_rdf_Property, uri_rdf__2)=true)). % 43.38/30.99 tff(c_4758, plain, (icext(uri_rdf_Property, uri_rdf_subject)=true)). % 43.38/30.99 tff(c_4712, plain, (icext(uri_owl_Class, uri_ex_Clique)=true)). % 43.38/30.99 tff(c_4668, plain, (icext(uri_rdf_List, uri_rdf_nil)=true)). % 43.38/30.99 tff(c_4627, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__1)=true)). % 43.38/30.99 tff(c_4586, plain, (icext(uri_rdf_Property, uri_rdf_type)=true)). % 43.38/30.99 tff(c_4548, plain, (icext(uri_rdf_Property, uri_rdf__3)=true)). % 43.38/30.99 tff(c_4510, plain, (icext(uri_owl_Restriction, sK5_testcase_premise_fullish_013_Cliques_BNODE_r)=true)). % 43.38/30.99 tff(c_4467, plain, (icext(uri_rdfs_Datatype, uri_rdf_XMLLiteral)=true)). % 43.38/30.99 tff(c_4430, plain, (icext(uri_ex_Clique, uri_ex_JoesGang)=true)). % 43.38/30.99 tff(c_4388, plain, (icext(uri_ex_JoesGang, uri_ex_alice)=true)). % 43.38/30.99 tff(c_4350, plain, (icext(uri_rdf_Property, uri_rdf__1)=true)). % 43.38/30.99 tff(c_4308, plain, (icext(uri_rdf_Property, uri_rdf_first)=true)). % 43.38/30.99 tff(c_4264, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__2)=true)). % 43.38/30.99 tff(c_4227, plain, (icext(uri_owl_ObjectProperty, uri_foaf_knows)=true)). % 43.38/30.99 tff(c_4189, plain, (icext(uri_rdf_Property, uri_rdf_rest)=true)). % 43.38/30.99 tff(c_4149, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__3)=true)). % 43.38/30.99 tff(c_4100, plain, (icext(uri_rdfs_Class, uri_rdf_Property)=true)). % 43.38/30.99 tff(c_4055, plain, (icext(uri_ex_JoesGang, uri_ex_bob)=true)). % 43.38/30.99 tff(c_4018, plain, (icext(uri_rdf_Property, uri_rdf_object)=true)). % 43.38/30.99 tff(c_3981, plain, (ic(uri_rdf_Alt)=true)). % 43.38/30.99 tff(c_3940, plain, (ip(uri_owl_sameAs)=true)). % 43.38/30.99 tff(c_3900, plain, (ic(uri_rdfs_Class)=true)). % 43.38/30.99 tff(c_3864, plain, (ip(uri_rdf_value)=true)). % 43.38/30.99 tff(c_3820, plain, (ip(uri_rdf_object)=true)). % 43.38/30.99 tff(c_3784, plain, (ic(uri_rdfs_ContainerMembershipProperty)=true)). % 43.38/30.99 tff(c_3748, plain, (ip(uri_owl_propertyChainAxiom)=true)). % 43.38/30.99 tff(c_3706, plain, (ip(uri_rdfs_subPropertyOf)=true)). % 43.38/30.99 tff(c_3670, plain, (ip(uri_rdfs_isDefinedBy)=true)). % 43.38/30.99 tff(c_3634, plain, (ic(uri_ex_Clique)=true)). % 43.38/30.99 tff(c_3598, plain, (ic(sK5_testcase_premise_fullish_013_Cliques_BNODE_r)=true)). % 43.38/30.99 tff(c_3564, plain, (ip(uri_owl_inverseOf)=true)). % 43.38/30.99 tff(c_3523, plain, (ip(uri_owl_someValuesFrom)=true)). % 43.38/30.99 tff(c_3483, plain, (ip(uri_rdf__3)=true)). % 43.38/30.99 tff(c_3443, plain, (ip(uri_rdf__2)=true)). % 43.38/30.99 tff(c_3399, plain, (ip(uri_owl_onProperty)=true)). % 43.38/30.99 tff(c_2791, plain, (ip(uri_rdf__1)=true)). % 43.38/30.99 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))). % 43.38/30.99 tff(c_2755, plain, (ip(uri_rdfs_seeAlso)=true)). % 43.38/30.99 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))). % 43.38/30.99 tff(c_2611, plain, (ip(uri_rdf_rest)=true)). % 43.38/30.99 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))). % 43.38/30.99 tff(c_2181, plain, (ip(uri_ex_sameCliqueAs)=true)). % 43.38/30.99 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))). % 43.38/30.99 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))). % 43.38/30.99 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))). % 43.38/30.99 tff(c_1698, plain, (ic(uri_rdfs_Literal)=true)). % 43.38/30.99 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))). % 43.38/30.99 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))). % 43.38/30.99 tff(c_1587, plain, (ip(uri_rdfs_subClassOf)=true)). % 43.38/30.99 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))). % 43.38/30.99 tff(c_1475, plain, (ip(uri_rdf_subject)=true)). % 43.38/30.99 tff(c_1433, plain, (ip(uri_rdfs_domain)=true)). % 43.38/30.99 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))). % 43.38/30.99 tff(c_58, plain, (![C_15]: (ifeq(ic(C_15), true, iext(uri_rdfs_subClassOf, C_15, uri_rdfs_Resource), true)=true))). % 43.38/30.99 tff(c_1305, plain, (ip(uri_rdfs_range)=true)). % 43.38/30.99 tff(c_30, plain, (![P_10]: (ifeq(iext(uri_rdf_type, P_10, uri_rdf_Property), true, ip(P_10), true)=true))). % 43.38/30.99 tff(c_170, plain, (![P_51]: (ifeq(ip(P_51), true, iext(uri_rdfs_subPropertyOf, P_51, P_51), true)=true))). % 43.38/30.99 tff(c_1254, plain, (ip(uri_rdf_first)=true)). % 43.38/30.99 tff(c_156, plain, (![C_39]: (ifeq(ic(C_39), true, iext(uri_rdfs_subClassOf, C_39, C_39), true)=true))). % 43.38/30.99 tff(c_28, plain, (![P_9]: (ifeq(ip(P_9), true, iext(uri_rdf_type, P_9, uri_rdf_Property), true)=true))). % 43.38/30.99 tff(c_1153, plain, (ip(uri_rdf_type)=true)). % 43.38/30.99 tff(c_1124, plain, (ic(uri_rdf_XMLLiteral)=true)). % 43.38/30.99 tff(c_162, plain, (![P_43, Q_44]: (ifeq(iext(uri_rdfs_subPropertyOf, P_43, Q_44), true, ip(Q_44), true)=true))). % 43.38/30.99 tff(c_1066, plain, (ic(uri_rdf_Property)=true)). % 43.38/30.99 tff(c_4, plain, (![P_4, S_5, O_6]: (ifeq(iext(P_4, S_5, O_6), true, ip(P_4), true)=true))). % 43.38/30.99 tff(c_788, plain, (ic(uri_rdfs_Container)=true)). % 43.38/30.99 tff(c_717, plain, (ic(uri_rdf_Bag)=true)). % 43.38/30.99 tff(c_150, plain, (![C_35, D_36]: (ifeq(iext(uri_rdfs_subClassOf, C_35, D_36), true, ic(D_36), true)=true))). % 43.38/30.99 tff(c_678, plain, (ic(uri_rdfs_Datatype)=true)). % 43.38/30.99 tff(c_164, plain, (![P_45, Q_46]: (ifeq(iext(uri_rdfs_subPropertyOf, P_45, Q_46), true, ip(P_45), true)=true))). % 43.38/30.99 tff(c_652, plain, (ic(uri_rdfs_Seq)=true)). % 43.38/30.99 tff(c_152, plain, (![C_37, D_38]: (ifeq(iext(uri_rdfs_subClassOf, C_37, D_38), true, ic(C_37), true)=true))). % 43.38/30.99 tff(c_114, plain, (![X_22]: (ifeq(ic(X_22), true, icext(uri_rdfs_Class, X_22), true)=true))). % 43.38/30.99 tff(c_122, plain, (![X_26]: (ifeq(icext(uri_rdfs_Literal, X_26), true, lv(X_26), true)=true))). % 43.38/30.99 tff(c_124, plain, (![X_27]: (ifeq(lv(X_27), true, icext(uri_rdfs_Literal, X_27), true)=true))). % 43.38/30.99 tff(c_116, plain, (![X_23]: (ifeq(icext(uri_rdfs_Class, X_23), true, ic(X_23), true)=true))). % 43.38/30.99 tff(c_573, plain, (![X_61]: (icext(uri_rdfs_Resource, X_61)=true))). % 43.38/30.99 tff(c_223, plain, (![X_8]: (ifeq(lv(X_8), true, true, true)=true))). % 43.38/30.99 tff(c_2, plain, (![A_1, B_2, C_3]: (ifeq(A_1, A_1, B_2, C_3)=B_2))). % 43.38/30.99 tff(c_60, plain, (iext(uri_rdfs_domain, uri_rdf_first, uri_rdf_List)=true)). % 43.38/30.99 tff(c_84, plain, (iext(uri_rdfs_domain, uri_rdf__3, uri_rdfs_Resource)=true)). % 43.38/30.99 tff(c_26, plain, (iext(uri_rdf_type, uri_rdf_subject, uri_rdf_Property)=true)). % 43.38/30.99 tff(c_36, plain, (iext(uri_rdfs_domain, uri_rdfs_comment, uri_rdfs_Resource)=true)). % 43.38/30.99 tff(c_34, plain, (iext(uri_rdf_type, uri_rdf_type, uri_rdf_Property)=true)). % 43.38/30.99 tff(c_16, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdf_Property)=true)). % 43.38/30.99 tff(c_128, plain, (iext(uri_rdfs_domain, uri_rdfs_range, uri_rdf_Property)=true)). % 43.38/30.99 tff(c_176, plain, (iext(uri_rdfs_range, uri_rdf_type, uri_rdfs_Class)=true)). % 43.38/30.99 tff(c_64, plain, (iext(uri_rdfs_domain, uri_rdf_rest, uri_rdf_List)=true)). % 43.38/30.99 tff(c_154, plain, (iext(uri_rdfs_range, uri_rdfs_subClassOf, uri_rdfs_Class)=true)). % 43.38/30.99 tff(c_196, plain, (iext(uri_rdf_rest, sK4_testcase_premise_fullish_013_Cliques_BNODE_l3, uri_rdf_nil)=true)). % 43.38/30.99 tff(c_98, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Container)=true)). % 43.38/30.99 tff(c_42, plain, (iext(uri_rdfs_range, uri_rdfs_isDefinedBy, uri_rdfs_Resource)=true)). % 43.38/30.99 tff(c_44, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso)=true)). % 43.38/30.99 tff(c_188, plain, (iext(uri_owl_onProperty, sK5_testcase_premise_fullish_013_Cliques_BNODE_r, uri_ex_sameCliqueAs)=true)). % 43.38/30.99 tff(c_12, plain, (iext(uri_rdf_type, uri_rdf_nil, uri_rdf_List)=true)). % 43.38/30.99 tff(c_178, plain, (iext(uri_rdfs_domain, uri_rdf_value, uri_rdfs_Resource)=true)). % 43.38/30.99 tff(c_38, plain, (iext(uri_rdfs_range, uri_rdfs_comment, uri_rdfs_Literal)=true)). % 43.38/30.99 tff(c_146, plain, (iext(uri_rdfs_domain, uri_rdfs_subClassOf, uri_rdfs_Class)=true)). % 43.38/30.99 tff(c_18, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdf_Property)=true)). % 43.38/30.99 tff(c_132, plain, (iext(uri_rdfs_range, uri_rdfs_range, uri_rdfs_Class)=true)). % 43.38/30.99 tff(c_86, plain, (iext(uri_rdfs_range, uri_rdf__1, uri_rdfs_Resource)=true)). % 43.38/30.99 tff(c_80, plain, (iext(uri_rdfs_domain, uri_rdf__1, uri_rdfs_Resource)=true)). % 43.38/30.99 tff(c_22, plain, (iext(uri_rdf_type, uri_rdf_object, uri_rdf_Property)=true)). % 43.38/30.99 tff(c_184, plain, (iext(uri_owl_propertyChainAxiom, uri_foaf_knows, sK1_testcase_premise_fullish_013_Cliques_BNODE_l1)=true)). % 43.38/30.99 tff(c_112, plain, (iext(uri_rdfs_range, uri_rdfs_domain, uri_rdfs_Class)=true)). % 43.38/30.99 tff(c_220, plain, (iext(uri_foaf_knows, uri_ex_alice, uri_ex_bob)!=true)). % 43.38/30.99 tff(c_194, plain, (iext(uri_rdf_rest, sK2_testcase_premise_fullish_013_Cliques_BNODE_l2, sK4_testcase_premise_fullish_013_Cliques_BNODE_l3)=true)). % 43.38/30.99 tff(c_46, plain, (iext(uri_rdfs_domain, uri_rdfs_label, uri_rdfs_Resource)=true)). % 43.38/30.99 tff(c_208, plain, (iext(uri_rdf_type, uri_ex_Clique, uri_owl_Class)=true)). % 43.38/30.99 tff(c_10, plain, (iext(uri_rdf_type, uri_rdf_first, uri_rdf_Property)=true)). % 43.38/30.99 tff(c_76, plain, (iext(uri_rdfs_domain, uri_rdfs_member, uri_rdfs_Resource)=true)). % 43.38/30.99 tff(c_108, plain, (iext(uri_rdfs_domain, uri_rdfs_domain, uri_rdf_Property)=true)). % 43.38/30.99 tff(c_78, plain, (iext(uri_rdfs_range, uri_rdfs_member, uri_rdfs_Resource)=true)). % 43.38/30.99 tff(c_70, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Container)=true)). % 43.38/30.99 tff(c_88, plain, (iext(uri_rdfs_range, uri_rdf__2, uri_rdfs_Resource)=true)). % 43.38/30.99 tff(c_82, plain, (iext(uri_rdfs_domain, uri_rdf__2, uri_rdfs_Resource)=true)). % 43.38/30.99 tff(c_186, plain, (iext(uri_owl_someValuesFrom, sK5_testcase_premise_fullish_013_Cliques_BNODE_r, uri_ex_Clique)=true)). % 43.38/30.99 tff(c_48, plain, (iext(uri_rdfs_range, uri_rdfs_label, uri_rdfs_Literal)=true)). % 43.38/30.99 tff(c_140, plain, (iext(uri_rdfs_range, uri_rdf_predicate, uri_rdfs_Resource)=true)). % 43.38/30.99 tff(c_106, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Class)=true)). % 43.38/30.99 tff(c_52, plain, (iext(uri_rdfs_range, uri_rdfs_seeAlso, uri_rdfs_Resource)=true)). % 43.38/30.99 tff(c_182, plain, (iext(uri_owl_inverseOf, sK3_testcase_premise_fullish_013_Cliques_BNODE_i, uri_rdf_type)=true)). % 43.38/30.99 tff(c_180, plain, (iext(uri_rdfs_range, uri_rdf_value, uri_rdfs_Resource)=true)). % 43.38/30.99 tff(c_74, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property)=true)). % 43.38/30.99 tff(c_210, plain, (iext(uri_rdf_type, uri_ex_bob, uri_ex_JoesGang)=true)). % 43.38/30.99 tff(c_50, plain, (iext(uri_rdfs_domain, uri_rdfs_seeAlso, uri_rdfs_Resource)=true)). % 43.38/30.99 tff(c_216, plain, (iext(uri_rdfs_subPropertyOf, uri_ex_sameCliqueAs, uri_owl_sameAs)=true)). % 43.38/30.99 tff(c_66, plain, (iext(uri_rdfs_range, uri_rdf_rest, uri_rdf_List)=true)). % 43.38/30.99 tff(c_94, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdfs_ContainerMembershipProperty)=true)). % 43.38/30.99 tff(c_168, plain, (iext(uri_rdfs_range, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 43.38/30.99 tff(c_68, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Container)=true)). % 43.38/30.99 tff(c_62, plain, (iext(uri_rdfs_range, uri_rdf_first, uri_rdfs_Resource)=true)). % 43.38/30.99 tff(c_96, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdfs_ContainerMembershipProperty)=true)). % 43.38/30.99 tff(c_126, plain, (iext(uri_rdf_type, uri_rdf_Property, uri_rdfs_Class)=true)). % 43.38/30.99 tff(c_144, plain, (iext(uri_rdfs_range, uri_rdf_subject, uri_rdfs_Resource)=true)). % 43.38/30.99 tff(c_200, plain, (iext(uri_rdf_first, sK2_testcase_premise_fullish_013_Cliques_BNODE_l2, uri_ex_sameCliqueAs)=true)). % 43.38/30.99 tff(c_138, plain, (iext(uri_rdfs_domain, uri_rdf_predicate, uri_rdfs_Statement)=true)). % 43.38/30.99 tff(c_40, plain, (iext(uri_rdfs_domain, uri_rdfs_isDefinedBy, uri_rdfs_Resource)=true)). % 43.38/30.99 tff(c_100, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Literal)=true)). % 43.38/30.99 tff(c_212, plain, (iext(uri_rdf_type, uri_ex_alice, uri_ex_JoesGang)=true)). % 43.38/30.99 tff(c_198, plain, (iext(uri_rdf_first, sK1_testcase_premise_fullish_013_Cliques_BNODE_l1, uri_rdf_type)=true)). % 43.38/30.99 tff(c_20, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdf_Property)=true)). % 43.38/30.99 tff(c_192, plain, (iext(uri_rdf_rest, sK1_testcase_premise_fullish_013_Cliques_BNODE_l1, sK2_testcase_premise_fullish_013_Cliques_BNODE_l2)=true)). % 43.38/30.99 tff(c_24, plain, (iext(uri_rdf_type, uri_rdf_value, uri_rdf_Property)=true)). % 43.38/30.99 tff(c_202, plain, (iext(uri_rdf_first, sK4_testcase_premise_fullish_013_Cliques_BNODE_l3, sK3_testcase_premise_fullish_013_Cliques_BNODE_i)=true)). % 43.38/30.99 tff(c_134, plain, (iext(uri_rdfs_domain, uri_rdf_object, uri_rdfs_Statement)=true)). % 43.38/30.99 tff(c_174, plain, (iext(uri_rdfs_domain, uri_rdf_type, uri_rdfs_Resource)=true)). % 43.38/30.99 tff(c_204, plain, (iext(uri_rdf_type, sK5_testcase_premise_fullish_013_Cliques_BNODE_r, uri_owl_Restriction)=true)). % 43.38/30.99 tff(c_160, plain, (iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 43.38/30.99 tff(c_142, plain, (iext(uri_rdfs_domain, uri_rdf_subject, uri_rdfs_Statement)=true)). % 43.38/30.99 tff(c_90, plain, (iext(uri_rdfs_range, uri_rdf__3, uri_rdfs_Resource)=true)). % 43.38/30.99 tff(c_14, plain, (iext(uri_rdf_type, uri_rdf_rest, uri_rdf_Property)=true)). % 43.38/30.99 tff(c_102, plain, (iext(uri_rdf_type, uri_rdf_XMLLiteral, uri_rdfs_Datatype)=true)). % 43.38/30.99 tff(c_92, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdfs_ContainerMembershipProperty)=true)). % 43.38/30.99 tff(c_190, plain, (iext(uri_rdfs_range, uri_ex_sameCliqueAs, uri_ex_Clique)=true)). % 43.38/30.99 tff(c_206, plain, (iext(uri_rdf_type, uri_ex_JoesGang, uri_ex_Clique)=true)). % 43.38/30.99 tff(c_214, plain, (iext(uri_rdf_type, uri_foaf_knows, uri_owl_ObjectProperty)=true)). % 43.38/30.99 tff(c_218, plain, (iext(uri_rdfs_subClassOf, uri_ex_Clique, sK5_testcase_premise_fullish_013_Cliques_BNODE_r)=true)). % 43.38/30.99 tff(c_6, plain, (![X_7]: (ir(X_7)=true))). % 43.38/30.99 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 43.38/30.99 %------------------------------------------------------------------------------