%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SWB013+4 : TPTP v9.0.0. Released v5.2.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 : n009.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:50 PM UTC 2025
% Result : CounterSatisfiable 14.30s 5.18s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : SWB013+4 : TPTP v9.0.0. Released v5.2.0.
% 0.07/0.14 % 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.35 % Computer : n009.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Wed Apr 9 00:56:41 EDT 2025
% 0.13/0.36 % CPUTime :
% 14.30/5.18
% 14.30/5.18 % SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 14.30/5.18
% 14.30/5.18 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 14.30/5.19 %$ iext > icext > lv > ir > ip > ic > #nlpp > 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 > #skF_5 > #skF_2 > #skF_3 > #skF_1 > #skF_4
% 14.30/5.19
% 14.30/5.19 %Foreground sorts:
% 14.30/5.19
% 14.30/5.19
% 14.30/5.19 %Background operators:
% 14.30/5.19
% 14.30/5.19
% 14.30/5.19 %Foreground operators:
% 14.30/5.19 tff(uri_rdfs_Datatype, type, uri_rdfs_Datatype: $i).
% 14.30/5.19 tff(uri_rdfs_ContainerMembershipProperty, type, uri_rdfs_ContainerMembershipProperty: $i).
% 14.30/5.19 tff(uri_rdfs_Resource, type, uri_rdfs_Resource: $i).
% 14.30/5.19 tff(uri_rdf_Property, type, uri_rdf_Property: $i).
% 14.30/5.19 tff(uri_rdf_subject, type, uri_rdf_subject: $i).
% 14.30/5.19 tff(uri_rdf_type, type, uri_rdf_type: $i).
% 14.30/5.19 tff(uri_owl_onProperty, type, uri_owl_onProperty: $i).
% 14.30/5.19 tff(uri_rdfs_subPropertyOf, type, uri_rdfs_subPropertyOf: $i).
% 14.30/5.19 tff(uri_ex_Clique, type, uri_ex_Clique: $i).
% 14.30/5.19 tff(uri_rdfs_seeAlso, type, uri_rdfs_seeAlso: $i).
% 14.30/5.19 tff(uri_rdfs_range, type, uri_rdfs_range: $i).
% 14.30/5.19 tff(uri_rdf_XMLLiteral, type, uri_rdf_XMLLiteral: $i).
% 14.30/5.19 tff(uri_rdf_List, type, uri_rdf_List: $i).
% 14.30/5.19 tff(uri_ex_JoesGang, type, uri_ex_JoesGang: $i).
% 14.30/5.19 tff(uri_rdf_first, type, uri_rdf_first: $i).
% 14.30/5.19 tff(uri_rdf_predicate, type, uri_rdf_predicate: $i).
% 14.30/5.19 tff(uri_owl_inverseOf, type, uri_owl_inverseOf: $i).
% 14.30/5.19 tff(uri_ex_bob, type, uri_ex_bob: $i).
% 14.30/5.19 tff(uri_rdf__3, type, uri_rdf__3: $i).
% 14.30/5.19 tff(icext, type, icext: ($i * $i) > $o).
% 14.30/5.19 tff(uri_rdf_value, type, uri_rdf_value: $i).
% 14.30/5.19 tff(ip, type, ip: $i > $o).
% 14.30/5.19 tff(uri_ex_sameCliqueAs, type, uri_ex_sameCliqueAs: $i).
% 14.30/5.19 tff(uri_rdfs_Statement, type, uri_rdfs_Statement: $i).
% 14.30/5.19 tff(uri_rdf__1, type, uri_rdf__1: $i).
% 14.30/5.19 tff(lv, type, lv: $i > $o).
% 14.30/5.19 tff(ir, type, ir: $i > $o).
% 14.30/5.19 tff(uri_owl_Restriction, type, uri_owl_Restriction: $i).
% 14.30/5.19 tff('#skF_5', type, '#skF_5': $i).
% 14.30/5.19 tff(uri_ex_alice, type, uri_ex_alice: $i).
% 14.30/5.19 tff(uri_rdf_rest, type, uri_rdf_rest: $i).
% 14.30/5.19 tff(uri_rdfs_label, type, uri_rdfs_label: $i).
% 14.30/5.19 tff(uri_rdfs_Container, type, uri_rdfs_Container: $i).
% 14.30/5.19 tff(ic, type, ic: $i > $o).
% 14.30/5.19 tff('#skF_2', type, '#skF_2': $i).
% 14.30/5.19 tff(uri_owl_propertyChainAxiom, type, uri_owl_propertyChainAxiom: $i).
% 14.30/5.19 tff('#skF_3', type, '#skF_3': $i).
% 14.30/5.19 tff('#skF_1', type, '#skF_1': $i).
% 14.30/5.19 tff(uri_owl_ObjectProperty, type, uri_owl_ObjectProperty: $i).
% 14.30/5.19 tff(uri_rdfs_subClassOf, type, uri_rdfs_subClassOf: $i).
% 14.30/5.19 tff(uri_owl_sameAs, type, uri_owl_sameAs: $i).
% 14.30/5.19 tff(uri_rdf_object, type, uri_rdf_object: $i).
% 14.30/5.19 tff(uri_rdfs_Class, type, uri_rdfs_Class: $i).
% 14.30/5.19 tff(uri_rdfs_Seq, type, uri_rdfs_Seq: $i).
% 14.30/5.19 tff(uri_owl_Class, type, uri_owl_Class: $i).
% 14.30/5.19 tff(iext, type, iext: ($i * $i * $i) > $o).
% 14.30/5.19 tff(uri_rdfs_member, type, uri_rdfs_member: $i).
% 14.30/5.19 tff(uri_rdf_Bag, type, uri_rdf_Bag: $i).
% 14.30/5.19 tff(uri_rdf__2, type, uri_rdf__2: $i).
% 14.30/5.19 tff(uri_foaf_knows, type, uri_foaf_knows: $i).
% 14.30/5.19 tff('#skF_4', type, '#skF_4': $i).
% 14.30/5.19 tff(uri_rdfs_comment, type, uri_rdfs_comment: $i).
% 14.30/5.19 tff(uri_rdfs_Literal, type, uri_rdfs_Literal: $i).
% 14.30/5.19 tff(uri_owl_someValuesFrom, type, uri_owl_someValuesFrom: $i).
% 14.30/5.19 tff(uri_rdf_Alt, type, uri_rdf_Alt: $i).
% 14.30/5.19 tff(uri_rdf_nil, type, uri_rdf_nil: $i).
% 14.30/5.19 tff(uri_rdfs_isDefinedBy, type, uri_rdfs_isDefinedBy: $i).
% 14.30/5.19 tff(uri_rdfs_domain, type, uri_rdfs_domain: $i).
% 14.30/5.19
% 14.30/5.19 %Saturated clause set:
% 14.30/5.20 tff(c_9653, plain, (![C_28, C_405]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, C_405) | ~iext(uri_rdfs_subClassOf, C_405, uri_ex_Clique)))).
% 14.30/5.20 tff(c_8024, plain, (![C_28, C_388]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, C_388) | ~iext(uri_rdfs_subClassOf, C_388, uri_rdfs_ContainerMembershipProperty)))).
% 14.30/5.20 tff(c_10057, plain, (![C_28, C_408]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, C_408) | ~iext(uri_rdfs_subClassOf, C_408, uri_rdf_Alt)))).
% 14.30/5.20 tff(c_8445, plain, (![Q_32, C_396]: (iext(Q_32, C_396, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_396, uri_rdf_Bag)))).
% 14.30/5.20 tff(c_9654, plain, (![Q_32, C_405]: (iext(Q_32, C_405, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_405, uri_ex_Clique)))).
% 14.30/5.20 tff(c_8025, plain, (![Q_32, C_388]: (iext(Q_32, C_388, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_388, uri_rdfs_ContainerMembershipProperty)))).
% 14.30/5.20 tff(c_9249, plain, (![Q_32, C_402]: (iext(Q_32, C_402, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_402, uri_rdfs_Datatype)))).
% 14.30/5.20 tff(c_10058, plain, (![Q_32, C_408]: (iext(Q_32, C_408, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_408, uri_rdf_Alt)))).
% 14.30/5.20 tff(c_8846, plain, (![Q_32, C_399]: (iext(Q_32, C_399, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_399, uri_rdf_XMLLiteral)))).
% 14.30/5.20 tff(c_9248, plain, (![C_28, C_402]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, C_402) | ~iext(uri_rdfs_subClassOf, C_402, uri_rdfs_Datatype)))).
% 14.30/5.20 tff(c_8845, plain, (![C_28, C_399]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, C_399) | ~iext(uri_rdfs_subClassOf, C_399, uri_rdf_XMLLiteral)))).
% 14.30/5.20 tff(c_8444, plain, (![C_28, C_396]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, C_396) | ~iext(uri_rdfs_subClassOf, C_396, uri_rdf_Bag)))).
% 14.30/5.20 tff(c_4771, plain, (![Q_32, C_294]: (iext(Q_32, C_294, uri_rdfs_Literal) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_294, uri_rdf_XMLLiteral)))).
% 14.30/5.20 tff(c_6402, plain, (![C_28, C_349]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Container) | ~iext(uri_rdfs_subClassOf, C_28, C_349) | ~iext(uri_rdfs_subClassOf, C_349, uri_rdf_Alt)))).
% 14.30/5.20 tff(c_5993, plain, (![C_28, C_343]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Container) | ~iext(uri_rdfs_subClassOf, C_28, C_343) | ~iext(uri_rdfs_subClassOf, C_343, uri_rdf_Bag)))).
% 14.30/5.20 tff(c_10584, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdf_Bag))).
% 14.30/5.20 tff(c_6403, plain, (![Q_32, C_349]: (iext(Q_32, C_349, uri_rdfs_Container) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_349, uri_rdf_Alt)))).
% 14.30/5.20 tff(c_10564, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdf_Alt))).
% 14.30/5.20 tff(c_5994, plain, (![Q_32, C_343]: (iext(Q_32, C_343, uri_rdfs_Container) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_343, uri_rdf_Bag)))).
% 14.30/5.20 tff(c_10544, plain, (~iext(uri_rdfs_subPropertyOf, uri_owl_onProperty, uri_ex_sameCliqueAs))).
% 14.30/5.20 tff(c_10543, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_member, uri_ex_sameCliqueAs))).
% 14.30/5.20 tff(c_10542, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_seeAlso, uri_ex_sameCliqueAs))).
% 14.30/5.20 tff(c_10541, plain, (~iext(uri_rdfs_subPropertyOf, uri_owl_someValuesFrom, uri_ex_sameCliqueAs))).
% 14.30/5.20 tff(c_3334, plain, (![P_38, P_236]: (iext(uri_rdfs_subPropertyOf, P_38, uri_owl_sameAs) | ~iext(uri_rdfs_subPropertyOf, P_38, P_236) | ~iext(uri_rdfs_subPropertyOf, P_236, uri_ex_sameCliqueAs)))).
% 14.30/5.20 tff(c_10520, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_member, uri_rdfs_isDefinedBy))).
% 14.30/5.20 tff(c_10519, plain, (~iext(uri_rdfs_subPropertyOf, uri_owl_sameAs, uri_rdfs_isDefinedBy))).
% 14.30/5.20 tff(c_10518, plain, (~iext(uri_rdfs_subPropertyOf, uri_owl_onProperty, uri_rdfs_isDefinedBy))).
% 14.30/5.20 tff(c_4427, plain, (![P_38, P_291]: (iext(uri_rdfs_subPropertyOf, P_38, uri_rdfs_seeAlso) | ~iext(uri_rdfs_subPropertyOf, P_38, P_291) | ~iext(uri_rdfs_subPropertyOf, P_291, uri_rdfs_isDefinedBy)))).
% 14.30/5.20 tff(c_10497, plain, (~iext(uri_rdfs_subPropertyOf, uri_owl_propertyChainAxiom, uri_rdfs_isDefinedBy))).
% 14.30/5.20 tff(c_10496, plain, (~iext(uri_rdfs_subPropertyOf, uri_owl_inverseOf, uri_ex_sameCliqueAs))).
% 14.30/5.20 tff(c_10495, plain, (~iext(uri_rdfs_subPropertyOf, uri_owl_propertyChainAxiom, uri_ex_sameCliqueAs))).
% 14.30/5.20 tff(c_10494, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Container, uri_rdf_XMLLiteral))).
% 14.30/5.20 tff(c_10493, plain, (~iext(uri_rdfs_subPropertyOf, uri_owl_inverseOf, uri_rdfs_isDefinedBy))).
% 14.30/5.20 tff(c_4770, plain, (![C_28, C_294]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Literal) | ~iext(uri_rdfs_subClassOf, C_28, C_294) | ~iext(uri_rdfs_subClassOf, C_294, uri_rdf_XMLLiteral)))).
% 14.30/5.20 tff(c_10408, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdf_first, uri_rdfs_isDefinedBy))).
% 14.30/5.20 tff(c_3333, plain, (![Q_32, P_236]: (iext(Q_32, P_236, uri_owl_sameAs) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_32) | ~iext(uri_rdfs_subPropertyOf, P_236, uri_ex_sameCliqueAs)))).
% 14.30/5.20 tff(c_10388, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdf_rest, uri_ex_sameCliqueAs))).
% 14.30/5.20 tff(c_4426, plain, (![Q_32, P_291]: (iext(Q_32, P_291, uri_rdfs_seeAlso) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_32) | ~iext(uri_rdfs_subPropertyOf, P_291, uri_rdfs_isDefinedBy)))).
% 14.30/5.20 tff(c_7517, plain, (![Q_32, D_378]: (iext(Q_32, D_378, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~icext(uri_rdfs_Datatype, D_378)))).
% 14.30/5.20 tff(c_7516, plain, (![C_28, D_378]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, D_378) | ~icext(uri_rdfs_Datatype, D_378)))).
% 14.30/5.20 tff(c_10253, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdf_rest, uri_rdfs_isDefinedBy))).
% 14.30/5.20 tff(c_10252, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, uri_ex_sameCliqueAs))).
% 14.30/5.20 tff(c_6976, plain, (![Q_32]: (iext(Q_32, uri_rdf_XMLLiteral, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32)))).
% 14.30/5.21 tff(c_10232, plain, (~iext(uri_rdfs_subPropertyOf, uri_owl_someValuesFrom, uri_rdfs_isDefinedBy))).
% 14.30/5.21 tff(c_6944, plain, (![Q_32]: (iext(Q_32, uri_rdf_Alt, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32)))).
% 14.30/5.21 tff(c_1613, plain, (![Q_83, P_10]: (iext(Q_83, P_10, uri_rdfs_member) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_83) | ~icext(uri_rdfs_ContainerMembershipProperty, P_10)))).
% 14.30/5.21 tff(c_10193, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, uri_rdfs_isDefinedBy))).
% 14.30/5.21 tff(c_10192, plain, (~icext(uri_rdfs_Datatype, uri_rdfs_Container))).
% 14.30/5.21 tff(c_1720, plain, (![C_87, D_11]: (iext(uri_rdfs_subClassOf, C_87, uri_rdfs_Literal) | ~iext(uri_rdfs_subClassOf, C_87, D_11) | ~icext(uri_rdfs_Datatype, D_11)))).
% 14.30/5.21 tff(c_10107, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, uri_ex_sameCliqueAs))).
% 14.30/5.21 tff(c_10106, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, uri_rdfs_isDefinedBy))).
% 14.30/5.21 tff(c_7134, plain, (![Q_32]: (iext(Q_32, uri_rdfs_Seq, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32)))).
% 14.30/5.21 tff(c_10086, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdf_type, uri_rdfs_isDefinedBy))).
% 14.30/5.21 tff(c_1611, plain, (![Q_83, X_7, C_8]: (iext(Q_83, X_7, C_8) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83) | ~icext(C_8, X_7)))).
% 14.30/5.21 tff(c_10066, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, uri_rdfs_isDefinedBy))).
% 14.30/5.21 tff(c_9683, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_owl_sameAs))).
% 14.30/5.21 tff(c_6943, plain, (![C_28]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, uri_rdf_Alt)))).
% 14.30/5.21 tff(c_9682, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdfs_seeAlso))).
% 14.30/5.21 tff(c_1432, plain, (![P_80, P_10]: (iext(uri_rdfs_subPropertyOf, P_80, uri_rdfs_member) | ~iext(uri_rdfs_subPropertyOf, P_80, P_10) | ~icext(uri_rdfs_ContainerMembershipProperty, P_10)))).
% 14.30/5.21 tff(c_9662, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, uri_ex_sameCliqueAs))).
% 14.30/5.21 tff(c_9279, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy))).
% 14.30/5.21 tff(c_7101, plain, (![C_28]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, uri_ex_Clique)))).
% 14.30/5.21 tff(c_9278, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, uri_ex_sameCliqueAs))).
% 14.30/5.21 tff(c_1612, plain, (![Q_83, D_11]: (iext(Q_83, D_11, uri_rdfs_Literal) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_83) | ~icext(uri_rdfs_Datatype, D_11)))).
% 14.30/5.21 tff(c_9258, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdf_type, uri_ex_sameCliqueAs))).
% 14.30/5.21 tff(c_9257, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdf_first, uri_ex_sameCliqueAs))).
% 14.30/5.21 tff(c_7059, plain, (![C_28]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Datatype)))).
% 14.30/5.21 tff(c_8874, plain, (~iext(uri_rdfs_subClassOf, '#skF_1', uri_rdf_Bag))).
% 14.30/5.21 tff(c_8854, plain, (~iext(uri_rdfs_subClassOf, '#skF_1', uri_rdf_Alt))).
% 14.30/5.21 tff(c_1615, plain, (![Q_83, C_9]: (iext(Q_83, C_9, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_83) | ~ic(C_9)))).
% 14.30/5.21 tff(c_6975, plain, (![C_28]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, uri_rdf_XMLLiteral)))).
% 14.30/5.21 tff(c_1617, plain, (![Q_83, P_6]: (iext(Q_83, P_6, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83) | ~ip(P_6)))).
% 14.30/5.21 tff(c_6911, plain, (![C_28]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, uri_rdf_Bag)))).
% 14.30/5.21 tff(c_8064, plain, (![D_394]: (icext(uri_rdfs_Class, D_394) | ~icext(uri_rdfs_Datatype, D_394)))).
% 14.30/5.21 tff(c_1076, plain, (![C_72, D_11]: (icext(C_72, D_11) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_72) | ~icext(uri_rdfs_Datatype, D_11)))).
% 14.30/5.21 tff(c_7133, plain, (![C_28]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Seq)))).
% 14.30/5.21 tff(c_8036, plain, (![P_390]: (icext(uri_rdf_Property, P_390) | ~icext(uri_rdfs_ContainerMembershipProperty, P_390)))).
% 14.30/5.21 tff(c_1077, plain, (![C_72, P_10]: (icext(C_72, P_10) | ~iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_72) | ~icext(uri_rdfs_ContainerMembershipProperty, P_10)))).
% 14.30/5.21 tff(c_7022, plain, (![C_28]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, uri_rdfs_ContainerMembershipProperty)))).
% 14.30/5.21 tff(c_1616, plain, (![Q_83, C_27]: (iext(Q_83, C_27, C_27) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_83) | ~ic(C_27)))).
% 14.30/5.21 tff(c_7023, plain, (![Q_32]: (iext(Q_32, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32)))).
% 14.30/5.21 tff(c_7102, plain, (![Q_32]: (iext(Q_32, uri_ex_Clique, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32)))).
% 14.30/5.21 tff(c_1614, plain, (![Q_83, P_37]: (iext(Q_83, P_37, P_37) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_83) | ~ip(P_37)))).
% 14.30/5.21 tff(c_7060, plain, (![Q_32]: (iext(Q_32, uri_rdfs_Datatype, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32)))).
% 14.30/5.21 tff(c_7549, plain, (![C_76]: (icext(C_76, uri_rdfs_member) | ~iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_76)))).
% 14.30/5.21 tff(c_6912, plain, (![Q_32]: (iext(Q_32, uri_rdf_Bag, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32)))).
% 14.30/5.21 tff(c_6863, plain, (![D_11]: (iext(uri_rdfs_subClassOf, D_11, uri_rdfs_Resource) | ~icext(uri_rdfs_Datatype, D_11)))).
% 14.30/5.21 tff(c_6885, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Resource))).
% 14.30/5.21 tff(c_6888, plain, (iext(uri_rdfs_subClassOf, uri_ex_Clique, uri_rdfs_Resource))).
% 14.30/5.21 tff(c_1075, plain, (![C_72, X_7, C_8]: (icext(C_72, X_7) | ~iext(uri_rdfs_domain, uri_rdf_type, C_72) | ~icext(C_8, X_7)))).
% 14.30/5.21 tff(c_6882, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Resource))).
% 14.30/5.21 tff(c_6879, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Resource))).
% 14.30/5.21 tff(c_6876, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Resource))).
% 14.30/5.21 tff(c_6873, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Resource))).
% 14.30/5.21 tff(c_6870, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Resource))).
% 14.30/5.21 tff(c_1721, plain, (![C_87, C_9]: (iext(uri_rdfs_subClassOf, C_87, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_87, C_9) | ~ic(C_9)))).
% 14.30/5.21 tff(c_6587, plain, (![C_369, X_370]: (icext(uri_rdfs_Class, C_369) | ~icext(C_369, X_370)))).
% 14.30/5.21 tff(c_1335, plain, (![C_76, C_8, X_7]: (icext(C_76, C_8) | ~iext(uri_rdfs_range, uri_rdf_type, C_76) | ~icext(C_8, X_7)))).
% 14.30/5.21 tff(c_1905, plain, (![D_24, P_92]: (icext(D_24, P_92) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24) | ~ip(P_92)))).
% 14.30/5.21 tff(c_6554, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdf_Alt))).
% 14.30/5.21 tff(c_6547, plain, (![C_76]: (icext(C_76, uri_rdfs_Resource) | ~iext(uri_rdfs_range, uri_rdfs_subClassOf, C_76)))).
% 14.30/5.21 tff(c_6517, plain, (~iext(uri_rdfs_subClassOf, uri_owl_Restriction, uri_rdf_Alt))).
% 14.30/5.21 tff(c_1338, plain, (![C_76, P_37]: (icext(C_76, P_37) | ~iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_76) | ~ip(P_37)))).
% 14.30/5.21 tff(c_6516, plain, (~iext(uri_rdfs_subClassOf, uri_ex_Clique, uri_rdf_Alt))).
% 14.30/5.22 tff(c_6515, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdf_Alt))).
% 14.54/5.22 tff(c_1081, plain, (![C_72, P_6]: (icext(C_72, P_6) | ~iext(uri_rdfs_domain, uri_rdf_type, C_72) | ~ip(P_6)))).
% 14.54/5.22 tff(c_900, plain, (![D_69, X_16]: (icext(D_69, X_16) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_69) | ~ic(X_16)))).
% 14.54/5.22 tff(c_6480, plain, (~iext(uri_rdfs_subClassOf, uri_owl_ObjectProperty, uri_rdf_Alt))).
% 14.54/5.22 tff(c_6475, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdf_Bag))).
% 14.54/5.22 tff(c_1079, plain, (![C_72, C_9]: (icext(C_72, C_9) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_72) | ~ic(C_9)))).
% 14.54/5.22 tff(c_6474, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdf_Alt))).
% 14.54/5.22 tff(c_1340, plain, (![C_76, C_27]: (icext(C_76, C_27) | ~iext(uri_rdfs_range, uri_rdfs_subClassOf, C_76) | ~ic(C_27)))).
% 14.54/5.22 tff(c_6469, plain, (~iext(uri_rdfs_subClassOf, uri_owl_Class, uri_rdf_Alt))).
% 14.54/5.22 tff(c_6439, plain, (~iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdf_Alt))).
% 14.54/5.22 tff(c_899, plain, (![D_69, X_18]: (icext(D_69, X_18) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Literal, D_69) | ~lv(X_18)))).
% 14.54/5.22 tff(c_6438, plain, (~iext(uri_rdfs_subClassOf, uri_ex_JoesGang, uri_rdf_Alt))).
% 14.54/5.22 tff(c_6437, plain, (~iext(uri_rdfs_subClassOf, uri_owl_ObjectProperty, uri_rdf_Bag))).
% 14.54/5.22 tff(c_6432, plain, (~iext(uri_rdfs_subClassOf, uri_ex_Clique, uri_rdf_Bag))).
% 14.54/5.22 tff(c_1078, plain, (![C_72, P_37]: (icext(C_72, P_37) | ~iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_72) | ~ip(P_37)))).
% 14.54/5.22 tff(c_1675, plain, (![Q_83]: (iext(Q_83, uri_rdf_object, uri_rdfs_Statement) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))).
% 14.54/5.22 tff(c_6412, plain, (~iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdf_Alt))).
% 14.54/5.22 tff(c_6411, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Resource, uri_rdf_Alt))).
% 14.54/5.22 tff(c_1724, plain, (![C_87]: (iext(uri_rdfs_subClassOf, C_87, uri_rdfs_Container) | ~iext(uri_rdfs_subClassOf, C_87, uri_rdf_Alt)))).
% 14.54/5.22 tff(c_6104, plain, (~iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdf_Bag))).
% 14.54/5.22 tff(c_6084, plain, (~iext(uri_rdfs_subClassOf, uri_owl_Class, uri_rdf_Bag))).
% 14.54/5.22 tff(c_1660, plain, (![Q_83]: (iext(Q_83, uri_rdf_subject, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))).
% 14.54/5.22 tff(c_6064, plain, (~iext(uri_rdfs_subClassOf, uri_ex_JoesGang, uri_rdf_Bag))).
% 14.54/5.22 tff(c_1622, plain, (![Q_83]: (iext(Q_83, '#skF_5', '#skF_2') | ~iext(uri_rdfs_subPropertyOf, uri_rdf_first, Q_83)))).
% 14.54/5.22 tff(c_6063, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdf_Bag))).
% 14.54/5.22 tff(c_1694, plain, (![Q_83]: (iext(Q_83, uri_rdf_rest, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))).
% 14.54/5.22 tff(c_6043, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdf_Bag))).
% 14.54/5.22 tff(c_1693, plain, (![Q_83]: (iext(Q_83, uri_ex_Clique, '#skF_1') | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_83)))).
% 14.54/5.22 tff(c_6023, plain, (~iext(uri_rdfs_subClassOf, uri_owl_Restriction, uri_rdf_Bag))).
% 14.54/5.22 tff(c_1690, plain, (![Q_83]: (iext(Q_83, uri_rdf_nil, uri_rdf_List) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))).
% 14.54/5.22 tff(c_6003, plain, (~iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdf_Bag))).
% 14.54/5.22 tff(c_6002, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Resource, uri_rdf_Bag))).
% 14.54/5.22 tff(c_1723, plain, (![C_87]: (iext(uri_rdfs_subClassOf, C_87, uri_rdfs_Container) | ~iext(uri_rdfs_subClassOf, C_87, uri_rdf_Bag)))).
% 14.54/5.22 tff(c_1691, plain, (![Q_83]: (iext(Q_83, uri_rdfs_subPropertyOf, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))).
% 14.54/5.22 tff(c_1678, plain, (![Q_83]: (iext(Q_83, uri_rdf_subject, uri_rdfs_Statement) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))).
% 14.54/5.22 tff(c_1642, plain, (![Q_83]: (iext(Q_83, uri_rdf_Property, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))).
% 14.54/5.22 tff(c_1639, plain, (![Q_83]: (iext(Q_83, uri_rdf_type, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))).
% 14.54/5.22 tff(c_1648, plain, (![Q_83]: (iext(Q_83, uri_rdf_type, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))).
% 14.54/5.22 tff(c_1668, plain, (![Q_83]: (iext(Q_83, uri_rdfs_subClassOf, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))).
% 14.54/5.22 tff(c_1663, plain, (![Q_83]: (iext(Q_83, uri_rdfs_Datatype, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_83)))).
% 14.54/5.22 tff(c_1655, plain, (![Q_83]: (iext(Q_83, uri_rdfs_range, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))).
% 14.54/5.22 tff(c_1681, plain, (![Q_83]: (iext(Q_83, uri_rdf__1, uri_rdfs_ContainerMembershipProperty) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))).
% 14.54/5.22 tff(c_1692, plain, (![Q_83]: (iext(Q_83, uri_foaf_knows, uri_owl_ObjectProperty) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))).
% 14.54/5.22 tff(c_1625, plain, (![Q_83]: (iext(Q_83, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_83)))).
% 14.54/5.22 tff(c_1662, plain, (![Q_83]: (iext(Q_83, uri_rdf_object, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))).
% 14.54/5.22 tff(c_5467, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdfs_subPropertyOf))).
% 14.54/5.22 tff(c_1629, plain, (![Q_83]: (iext(Q_83, uri_ex_Clique, uri_owl_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))).
% 14.54/5.22 tff(c_1695, plain, (![Q_83]: (iext(Q_83, uri_ex_sameCliqueAs, uri_owl_sameAs) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_83)))).
% 14.54/5.22 tff(c_1651, plain, (![Q_83]: (iext(Q_83, uri_rdfs_comment, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))).
% 14.54/5.22 tff(c_1672, plain, (![Q_83]: (iext(Q_83, uri_rdfs_Seq, uri_rdfs_Container) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_83)))).
% 14.54/5.22 tff(c_1684, plain, (![Q_83]: (iext(Q_83, uri_rdf_type, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))).
% 14.54/5.22 tff(c_1624, plain, (![Q_83]: (iext(Q_83, uri_rdf_value, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))).
% 14.54/5.22 tff(c_1659, plain, (![Q_83]: (iext(Q_83, uri_rdf_first, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))).
% 14.54/5.22 tff(c_1640, plain, (![Q_83]: (iext(Q_83, uri_rdf_value, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))).
% 14.54/5.22 tff(c_1680, plain, (![Q_83]: (iext(Q_83, uri_rdf__3, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))).
% 14.54/5.22 tff(c_1632, plain, (![Q_83]: (iext(Q_83, uri_ex_bob, uri_ex_JoesGang) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))).
% 14.54/5.22 tff(c_1630, plain, (![Q_83]: (iext(Q_83, uri_rdfs_label, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))).
% 14.54/5.22 tff(c_1679, plain, (![Q_83]: (iext(Q_83, uri_rdfs_domain, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))).
% 14.54/5.22 tff(c_1627, plain, (![Q_83]: (iext(Q_83, uri_ex_JoesGang, uri_ex_Clique) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))).
% 14.54/5.22 tff(c_5219, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_owl_onProperty))).
% 14.54/5.22 tff(c_1619, plain, (![Q_83]: (iext(Q_83, '#skF_1', uri_ex_sameCliqueAs) | ~iext(uri_rdfs_subPropertyOf, uri_owl_onProperty, Q_83)))).
% 14.54/5.22 tff(c_1621, plain, (![Q_83]: (iext(Q_83, '#skF_5', uri_rdf_nil) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_rest, Q_83)))).
% 14.54/5.22 tff(c_1653, plain, (![Q_83]: (iext(Q_83, uri_rdfs_seeAlso, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))).
% 14.54/5.22 tff(c_1650, plain, (![Q_83]: (iext(Q_83, '#skF_3', uri_rdf_type) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_first, Q_83)))).
% 14.54/5.22 tff(c_1634, plain, (![Q_83]: (iext(Q_83, uri_rdf_Alt, uri_rdfs_Container) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_83)))).
% 14.54/5.23 tff(c_1652, plain, (![Q_83]: (iext(Q_83, uri_rdfs_range, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))).
% 14.54/5.23 tff(c_5104, plain, (~iext(uri_rdfs_subClassOf, '#skF_1', uri_rdf_XMLLiteral))).
% 14.54/5.23 tff(c_1657, plain, (![Q_83]: (iext(Q_83, uri_rdf__2, uri_rdfs_ContainerMembershipProperty) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))).
% 14.54/5.23 tff(c_1635, plain, (![Q_83]: (iext(Q_83, '#skF_3', '#skF_4') | ~iext(uri_rdfs_subPropertyOf, uri_rdf_rest, Q_83)))).
% 14.54/5.23 tff(c_1688, plain, (![Q_83]: (iext(Q_83, uri_rdfs_domain, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))).
% 14.54/5.23 tff(c_1620, plain, (![Q_83]: (iext(Q_83, uri_rdf__2, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))).
% 14.54/5.23 tff(c_1728, plain, (![C_87]: (iext(uri_rdfs_subClassOf, C_87, uri_rdfs_Container) | ~iext(uri_rdfs_subClassOf, C_87, uri_rdfs_Seq)))).
% 14.54/5.23 tff(c_1658, plain, (![Q_83]: (iext(Q_83, uri_rdf_first, uri_rdf_List) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))).
% 14.54/5.23 tff(c_1673, plain, (![Q_83]: (iext(Q_83, uri_rdf_rest, uri_rdf_List) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))).
% 14.54/5.23 tff(c_1623, plain, (![Q_83]: (iext(Q_83, uri_rdfs_member, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))).
% 14.54/5.23 tff(c_4962, plain, (~iext(uri_rdfs_subClassOf, uri_owl_ObjectProperty, uri_rdf_XMLLiteral))).
% 14.54/5.23 tff(c_1647, plain, (![Q_83]: (iext(Q_83, uri_rdf_first, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))).
% 14.54/5.23 tff(c_4942, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_owl_someValuesFrom))).
% 14.54/5.23 tff(c_4922, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdf_XMLLiteral))).
% 14.54/5.23 tff(c_1618, plain, (![Q_83]: (iext(Q_83, '#skF_1', uri_ex_Clique) | ~iext(uri_rdfs_subPropertyOf, uri_owl_someValuesFrom, Q_83)))).
% 14.54/5.23 tff(c_4921, plain, (~iext(uri_rdfs_subClassOf, uri_ex_Clique, uri_rdf_XMLLiteral))).
% 14.54/5.23 tff(c_1674, plain, (![Q_83]: (iext(Q_83, uri_rdf_rest, uri_rdf_List) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))).
% 14.54/5.23 tff(c_4901, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_owl_inverseOf))).
% 14.54/5.23 tff(c_1644, plain, (![Q_83]: (iext(Q_83, '#skF_2', uri_rdf_type) | ~iext(uri_rdfs_subPropertyOf, uri_owl_inverseOf, Q_83)))).
% 14.54/5.23 tff(c_4862, plain, (~iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdf_XMLLiteral))).
% 14.54/5.23 tff(c_1643, plain, (![Q_83]: (iext(Q_83, uri_rdf_XMLLiteral, uri_rdfs_Literal) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_83)))).
% 14.54/5.23 tff(c_4861, plain, (~iext(uri_rdfs_subClassOf, uri_owl_Class, uri_rdf_XMLLiteral))).
% 14.54/5.23 tff(c_1685, plain, (![Q_83]: (iext(Q_83, uri_rdf__2, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))).
% 14.54/5.23 tff(c_4841, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdf_XMLLiteral))).
% 14.54/5.23 tff(c_1683, plain, (![Q_83]: (iext(Q_83, uri_rdfs_subClassOf, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))).
% 14.54/5.23 tff(c_4821, plain, (~iext(uri_rdfs_subClassOf, uri_owl_Restriction, uri_rdf_XMLLiteral))).
% 14.54/5.23 tff(c_1667, plain, (![Q_83]: (iext(Q_83, uri_rdf__1, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))).
% 14.54/5.23 tff(c_4801, plain, (~iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdf_XMLLiteral))).
% 14.54/5.23 tff(c_4800, plain, (~iext(uri_rdfs_subClassOf, uri_ex_JoesGang, uri_rdf_XMLLiteral))).
% 14.54/5.23 tff(c_4780, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdf_XMLLiteral))).
% 14.54/5.23 tff(c_1654, plain, (![Q_83]: (iext(Q_83, uri_rdf_subject, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))).
% 14.54/5.23 tff(c_4779, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Resource, uri_rdf_XMLLiteral))).
% 14.54/5.23 tff(c_1725, plain, (![C_87]: (iext(uri_rdfs_subClassOf, C_87, uri_rdfs_Literal) | ~iext(uri_rdfs_subClassOf, C_87, uri_rdf_XMLLiteral)))).
% 14.54/5.23 tff(c_1649, plain, (![Q_83]: (iext(Q_83, uri_rdf__1, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))).
% 14.54/5.23 tff(c_1626, plain, (![Q_83]: (iext(Q_83, uri_rdf__1, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))).
% 14.54/5.23 tff(c_1434, plain, (![P_80]: (iext(uri_rdfs_subPropertyOf, P_80, uri_rdfs_seeAlso) | ~iext(uri_rdfs_subPropertyOf, P_80, uri_rdfs_isDefinedBy)))).
% 14.54/5.23 tff(c_1664, plain, (![Q_83]: (iext(Q_83, uri_rdfs_label, uri_rdfs_Literal) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))).
% 14.54/5.23 tff(c_1641, plain, (![Q_83]: (iext(Q_83, uri_rdfs_subPropertyOf, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))).
% 14.54/5.23 tff(c_1631, plain, (![Q_83]: (iext(Q_83, uri_rdf__3, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))).
% 14.54/5.23 tff(c_1682, plain, (![Q_83]: (iext(Q_83, uri_rdf_predicate, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))).
% 14.54/5.23 tff(c_1669, plain, (![Q_83]: (iext(Q_83, uri_rdf_XMLLiteral, uri_rdfs_Datatype) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))).
% 14.54/5.23 tff(c_4225, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdf_rest))).
% 14.54/5.23 tff(c_1689, plain, (![Q_83]: (iext(Q_83, '#skF_1', uri_owl_Restriction) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))).
% 14.54/5.23 tff(c_1687, plain, (![Q_83]: (iext(Q_83, '#skF_4', '#skF_5') | ~iext(uri_rdfs_subPropertyOf, uri_rdf_rest, Q_83)))).
% 14.54/5.23 tff(c_1671, plain, (![Q_83]: (iext(Q_83, uri_rdf_predicate, uri_rdfs_Statement) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))).
% 14.54/5.23 tff(c_1726, plain, (![C_87]: (iext(uri_rdfs_subClassOf, C_87, uri_rdf_Property) | ~iext(uri_rdfs_subClassOf, C_87, uri_rdfs_ContainerMembershipProperty)))).
% 14.54/5.23 tff(c_1676, plain, (![Q_83]: (iext(Q_83, uri_rdf__2, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))).
% 14.54/5.23 tff(c_1638, plain, (![Q_83]: (iext(Q_83, uri_rdfs_isDefinedBy, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))).
% 14.54/5.23 tff(c_1637, plain, (![Q_83]: (iext(Q_83, uri_rdfs_comment, uri_rdfs_Literal) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))).
% 14.54/5.23 tff(c_4141, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdf_first))).
% 14.54/5.23 tff(c_1677, plain, (![Q_83]: (iext(Q_83, uri_ex_sameCliqueAs, uri_ex_Clique) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))).
% 14.54/5.23 tff(c_1636, plain, (![Q_83]: (iext(Q_83, '#skF_4', uri_ex_sameCliqueAs) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_first, Q_83)))).
% 14.54/5.23 tff(c_1656, plain, (![Q_83]: (iext(Q_83, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_83)))).
% 14.54/5.23 tff(c_1646, plain, (![Q_83]: (iext(Q_83, uri_rdfs_seeAlso, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))).
% 14.54/5.23 tff(c_1661, plain, (![Q_83]: (iext(Q_83, uri_rdf__3, uri_rdfs_ContainerMembershipProperty) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))).
% 14.54/5.23 tff(c_4065, plain, (~icext(uri_rdfs_Datatype, '#skF_1'))).
% 14.54/5.23 tff(c_3027, plain, (![D_24]: (icext(D_24, uri_ex_JoesGang) | ~iext(uri_rdfs_subClassOf, '#skF_1', D_24)))).
% 14.54/5.23 tff(c_4044, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdfs_subClassOf))).
% 14.54/5.23 tff(c_1633, plain, (![Q_83]: (iext(Q_83, uri_rdf_Bag, uri_rdfs_Container) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_83)))).
% 14.54/5.23 tff(c_1931, plain, (![D_24]: (icext(D_24, uri_rdfs_subPropertyOf) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 14.54/5.23 tff(c_1973, plain, (![D_24]: (icext(D_24, uri_rdfs_Class) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 14.54/5.23 tff(c_2100, plain, (![D_24]: (icext(D_24, uri_rdfs_seeAlso) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 14.54/5.23 tff(c_2003, plain, (![D_24]: (icext(D_24, '#skF_5') | ~iext(uri_rdfs_subClassOf, uri_rdf_List, D_24)))).
% 14.54/5.23 tff(c_2027, plain, (![D_24]: (icext(D_24, uri_rdfs_Literal) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 14.54/5.23 tff(c_2370, plain, (![D_24]: (icext(D_24, uri_rdfs_Statement) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 14.54/5.23 tff(c_2112, plain, (![D_24]: (icext(D_24, uri_rdf_predicate) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 14.54/5.23 tff(c_2431, plain, (![D_24]: (icext(D_24, uri_owl_Restriction) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 14.54/5.23 tff(c_2450, plain, (![D_24]: (icext(D_24, uri_rdfs_domain) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 14.54/5.23 tff(c_1628, plain, (![Q_83]: (iext(Q_83, uri_rdfs_isDefinedBy, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))).
% 14.54/5.23 tff(c_2043, plain, (![D_24]: (icext(D_24, '#skF_4') | ~iext(uri_rdfs_subClassOf, uri_rdf_List, D_24)))).
% 14.54/5.23 tff(c_2123, plain, (![D_24]: (icext(D_24, uri_rdfs_Datatype) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 14.54/5.23 tff(c_2085, plain, (![D_24]: (icext(D_24, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 14.54/5.23 tff(c_2507, plain, (![D_24]: (icext(D_24, uri_rdfs_comment) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 14.54/5.23 tff(c_1942, plain, (![D_24]: (icext(D_24, uri_rdf_List) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 14.54/5.23 tff(c_2188, plain, (![D_24]: (icext(D_24, uri_rdfs_member) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 14.54/5.23 tff(c_2218, plain, (![D_24]: (icext(D_24, uri_owl_ObjectProperty) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 14.54/5.23 tff(c_3693, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_owl_propertyChainAxiom))).
% 14.54/5.23 tff(c_1665, plain, (![Q_83]: (iext(Q_83, uri_foaf_knows, '#skF_3') | ~iext(uri_rdfs_subPropertyOf, uri_owl_propertyChainAxiom, Q_83)))).
% 14.54/5.23 tff(c_2282, plain, (![D_24]: (icext(D_24, uri_rdfs_subClassOf) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 14.54/5.23 tff(c_2299, plain, (![D_24]: (icext(D_24, uri_ex_Clique) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 14.54/5.23 tff(c_2169, plain, (![D_24]: (icext(D_24, uri_owl_sameAs) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 14.54/5.23 tff(c_2201, plain, (![D_24]: (icext(D_24, uri_rdfs_range) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 14.54/5.23 tff(c_2760, plain, (![D_24]: (icext(D_24, uri_rdf_Alt) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 14.54/5.23 tff(c_2148, plain, (![D_24]: (icext(D_24, uri_rdfs_ContainerMembershipProperty) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 14.54/5.23 tff(c_2320, plain, (![D_24]: (icext(D_24, uri_rdfs_isDefinedBy) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 14.54/5.23 tff(c_3537, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdfs_domain))).
% 14.54/5.24 tff(c_1645, plain, (![Q_83]: (iext(Q_83, uri_rdf_value, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))).
% 14.54/5.24 tff(c_2347, plain, (![D_24]: (icext(D_24, '#skF_3') | ~iext(uri_rdfs_subClassOf, uri_rdf_List, D_24)))).
% 14.54/5.24 tff(c_2014, plain, (![D_24]: (icext(D_24, uri_rdf_XMLLiteral) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 14.54/5.24 tff(c_1993, plain, (![D_24]: (icext(D_24, '#skF_1') | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 14.54/5.24 tff(c_2628, plain, (![D_24]: (icext(D_24, uri_owl_Class) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 14.54/5.24 tff(c_2242, plain, (![D_24]: (icext(D_24, uri_rdfs_Seq) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 14.54/5.24 tff(c_2488, plain, (![D_24]: (icext(D_24, uri_ex_sameCliqueAs) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 14.54/5.24 tff(c_2609, plain, (![D_24]: (icext(D_24, uri_rdf_Bag) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 14.54/5.24 tff(c_1954, plain, (![D_24]: (icext(D_24, uri_rdfs_Container) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 14.54/5.24 tff(c_2652, plain, (![D_24]: (icext(D_24, uri_ex_JoesGang) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 14.54/5.24 tff(c_1435, plain, (![P_80]: (iext(uri_rdfs_subPropertyOf, P_80, uri_owl_sameAs) | ~iext(uri_rdfs_subPropertyOf, P_80, uri_ex_sameCliqueAs)))).
% 14.54/5.24 tff(c_2344, plain, (![D_24]: (icext(D_24, uri_rdfs_label) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 14.54/5.24 tff(c_1763, plain, (![D_24]: (icext(D_24, uri_rdf_rest) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 14.54/5.24 tff(c_1784, plain, (![D_24]: (icext(D_24, uri_rdf__3) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 14.54/5.24 tff(c_3242, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdf_type))).
% 14.54/5.24 tff(c_1766, plain, (![D_24]: (icext(D_24, uri_rdf__1) | ~iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_24)))).
% 14.54/5.24 tff(c_1769, plain, (![D_24]: (icext(D_24, uri_rdf_first) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 14.54/5.24 tff(c_1760, plain, (![D_24]: (icext(D_24, uri_ex_alice) | ~iext(uri_rdfs_subClassOf, uri_ex_JoesGang, D_24)))).
% 14.54/5.24 tff(c_3168, plain, (~icext(uri_rdfs_Datatype, uri_owl_Restriction))).
% 14.54/5.24 tff(c_1729, plain, (![C_87]: (iext(uri_rdfs_subClassOf, C_87, '#skF_1') | ~iext(uri_rdfs_subClassOf, C_87, uri_ex_Clique)))).
% 14.54/5.24 tff(c_1787, plain, (![D_24]: (icext(D_24, '#skF_1') | ~iext(uri_rdfs_subClassOf, uri_owl_Restriction, D_24)))).
% 14.54/5.24 tff(c_3147, plain, (~icext(uri_rdfs_Datatype, uri_rdfs_Datatype))).
% 14.54/5.24 tff(c_3121, plain, (~icext(uri_rdfs_Datatype, uri_rdf_List))).
% 14.54/5.24 tff(c_1790, plain, (![D_24]: (icext(D_24, uri_rdf_XMLLiteral) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, D_24)))).
% 14.54/5.24 tff(c_1799, plain, (![D_24]: (icext(D_24, uri_rdf_nil) | ~iext(uri_rdfs_subClassOf, uri_rdf_List, D_24)))).
% 14.54/5.24 tff(c_1778, plain, (![D_24]: (icext(D_24, uri_rdf_subject) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 14.54/5.24 tff(c_1670, plain, (![Q_83]: (iext(Q_83, uri_ex_alice, uri_ex_JoesGang) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))).
% 14.54/5.24 tff(c_1751, plain, (![D_24]: (icext(D_24, uri_rdf_value) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 14.54/5.24 tff(c_3049, plain, (~icext(uri_rdfs_Datatype, uri_owl_ObjectProperty))).
% 14.54/5.24 tff(c_1757, plain, (![D_24]: (icext(D_24, uri_foaf_knows) | ~iext(uri_rdfs_subClassOf, uri_owl_ObjectProperty, D_24)))).
% 14.54/5.24 tff(c_3028, plain, (~icext(uri_rdfs_Datatype, uri_ex_Clique))).
% 14.54/5.24 tff(c_3024, plain, (icext('#skF_1', uri_ex_JoesGang))).
% 14.54/5.24 tff(c_1793, plain, (![D_24]: (icext(D_24, uri_ex_JoesGang) | ~iext(uri_rdfs_subClassOf, uri_ex_Clique, D_24)))).
% 14.54/5.24 tff(c_2989, plain, (~icext(uri_rdfs_Datatype, uri_ex_JoesGang))).
% 14.54/5.24 tff(c_1666, plain, (![Q_83]: (iext(Q_83, uri_rdfs_member, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))).
% 14.54/5.24 tff(c_1772, plain, (![D_24]: (icext(D_24, uri_ex_bob) | ~iext(uri_rdfs_subClassOf, uri_ex_JoesGang, D_24)))).
% 14.54/5.24 tff(c_2968, plain, (~icext(uri_rdfs_Datatype, uri_rdfs_Class))).
% 14.54/5.24 tff(c_1808, plain, (![D_24]: (icext(D_24, uri_rdf_Property) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 14.54/5.24 tff(c_1775, plain, (![D_24]: (icext(D_24, uri_rdf__2) | ~iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_24)))).
% 14.54/5.24 tff(c_2922, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdfs_range))).
% 14.54/5.24 tff(c_1796, plain, (![D_24]: (icext(D_24, uri_rdf__2) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 14.54/5.24 tff(c_1727, plain, (![C_87]: (iext(uri_rdfs_subClassOf, C_87, uri_rdfs_Class) | ~iext(uri_rdfs_subClassOf, C_87, uri_rdfs_Datatype)))).
% 14.54/5.24 tff(c_2893, plain, (~icext(uri_rdfs_Datatype, uri_rdfs_ContainerMembershipProperty))).
% 14.54/5.24 tff(c_1745, plain, (![D_24]: (icext(D_24, uri_rdf__3) | ~iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_24)))).
% 14.54/5.24 tff(c_2867, plain, (~icext(uri_rdfs_Datatype, uri_owl_Class))).
% 14.54/5.24 tff(c_1781, plain, (![D_24]: (icext(D_24, uri_ex_Clique) | ~iext(uri_rdfs_subClassOf, uri_owl_Class, D_24)))).
% 14.54/5.24 tff(c_1748, plain, (![D_24]: (icext(D_24, uri_rdf_object) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 14.54/5.24 tff(c_1802, plain, (![D_24]: (icext(D_24, uri_rdf_type) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 14.54/5.24 tff(c_2795, plain, (~icext(uri_rdfs_Datatype, uri_rdf_Property))).
% 14.54/5.24 tff(c_1686, plain, (![Q_83]: (iext(Q_83, uri_rdf__3, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))).
% 14.54/5.24 tff(c_1754, plain, (![D_24]: (icext(D_24, uri_rdf__1) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 14.54/5.24 tff(c_1094, plain, (![C_72]: (icext(C_72, uri_rdfs_label) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_72)))).
% 14.54/5.24 tff(c_1397, plain, (![C_76]: (icext(C_76, uri_rdf_List) | ~iext(uri_rdfs_range, uri_rdfs_range, C_76)))).
% 14.54/5.24 tff(c_2754, plain, (icext(uri_rdfs_Class, uri_rdf_Alt))).
% 14.54/5.24 tff(c_1098, plain, (![C_72]: (icext(C_72, uri_rdf_Alt) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_72)))).
% 14.54/5.24 tff(c_1093, plain, (![C_72]: (icext(C_72, uri_ex_Clique) | ~iext(uri_rdfs_domain, uri_rdf_type, C_72)))).
% 14.54/5.24 tff(c_1115, plain, (![C_72]: (icext(C_72, uri_rdfs_comment) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_72)))).
% 14.54/5.24 tff(c_1147, plain, (![C_72]: (icext(C_72, uri_rdfs_subClassOf) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_72)))).
% 14.54/5.24 tff(c_1095, plain, (![C_72]: (icext(C_72, uri_rdf__3) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_72)))).
% 14.54/5.24 tff(c_1096, plain, (![C_72]: (icext(C_72, uri_ex_bob) | ~iext(uri_rdfs_domain, uri_rdf_type, C_72)))).
% 14.54/5.24 tff(c_1359, plain, (![C_76]: (icext(C_76, '#skF_4') | ~iext(uri_rdfs_range, uri_rdf_rest, C_76)))).
% 14.54/5.24 tff(c_1092, plain, (![C_72]: (icext(C_72, uri_rdfs_isDefinedBy) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_72)))).
% 14.54/5.24 tff(c_1349, plain, (![C_76]: (icext(C_76, uri_rdfs_seeAlso) | ~iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_76)))).
% 14.54/5.24 tff(c_1089, plain, (![C_72]: (icext(C_72, uri_rdfs_isDefinedBy) | ~iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_72)))).
% 14.54/5.24 tff(c_1139, plain, (![C_72]: (icext(C_72, uri_rdf_object) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_72)))).
% 14.54/5.24 tff(c_1126, plain, (![C_72]: (icext(C_72, uri_rdf_object) | ~iext(uri_rdfs_domain, uri_rdf_type, C_72)))).
% 14.54/5.24 tff(c_1142, plain, (![C_72]: (icext(C_72, uri_rdf_subject) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_72)))).
% 14.54/5.24 tff(c_1351, plain, (![C_76]: (icext(C_76, uri_ex_Clique) | ~iext(uri_rdfs_range, uri_rdf_type, C_76)))).
% 14.54/5.24 tff(c_1087, plain, (![C_72]: (icext(C_72, uri_rdfs_member) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_72)))).
% 14.54/5.24 tff(c_1374, plain, (![C_76]: (icext(C_76, uri_rdf_type) | ~iext(uri_rdfs_range, uri_rdf_first, C_76)))).
% 14.54/5.24 tff(c_1387, plain, (![C_76]: (icext(C_76, uri_rdfs_Class) | ~iext(uri_rdfs_range, uri_rdfs_subClassOf, C_76)))).
% 14.54/5.24 tff(c_2653, plain, (ic(uri_ex_JoesGang))).
% 14.54/5.24 tff(c_2646, plain, (icext(uri_rdfs_Class, uri_ex_JoesGang))).
% 14.54/5.24 tff(c_1356, plain, (![C_76]: (icext(C_76, uri_ex_JoesGang) | ~iext(uri_rdfs_range, uri_rdf_type, C_76)))).
% 14.54/5.24 tff(c_1113, plain, (![C_72]: (icext(C_72, uri_rdf__1) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_72)))).
% 14.54/5.24 tff(c_1088, plain, (![C_72]: (icext(C_72, uri_rdf_value) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_72)))).
% 14.54/5.24 tff(c_2629, plain, (ic(uri_owl_Class))).
% 14.54/5.24 tff(c_2622, plain, (icext(uri_rdfs_Class, uri_owl_Class))).
% 14.54/5.24 tff(c_1353, plain, (![C_76]: (icext(C_76, uri_owl_Class) | ~iext(uri_rdfs_range, uri_rdf_type, C_76)))).
% 14.54/5.24 tff(c_1366, plain, (![C_76]: (icext(C_76, uri_rdfs_Class) | ~iext(uri_rdfs_range, uri_rdf_type, C_76)))).
% 14.54/5.24 tff(c_2603, plain, (icext(uri_rdfs_Class, uri_rdf_Bag))).
% 14.54/5.24 tff(c_1097, plain, (![C_72]: (icext(C_72, uri_rdf_Bag) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_72)))).
% 14.54/5.24 tff(c_1110, plain, (![C_72]: (icext(C_72, uri_rdfs_seeAlso) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_72)))).
% 14.54/5.24 tff(c_1099, plain, (![C_72]: (icext(C_72, '#skF_3') | ~iext(uri_rdfs_domain, uri_rdf_rest, C_72)))).
% 14.54/5.24 tff(c_1134, plain, (![C_72]: (icext(C_72, uri_ex_alice) | ~iext(uri_rdfs_domain, uri_rdf_type, C_72)))).
% 14.54/5.24 tff(c_1091, plain, (![C_72]: (icext(C_72, uri_ex_JoesGang) | ~iext(uri_rdfs_domain, uri_rdf_type, C_72)))).
% 14.54/5.24 tff(c_1385, plain, (![C_76]: (icext(C_76, uri_rdfs_ContainerMembershipProperty) | ~iext(uri_rdfs_range, uri_rdf_type, C_76)))).
% 14.54/5.24 tff(c_1106, plain, (![C_72]: (icext(C_72, uri_rdf_Property) | ~iext(uri_rdfs_domain, uri_rdf_type, C_72)))).
% 14.54/5.24 tff(c_1155, plain, (![C_72]: (icext(C_72, uri_rdfs_subPropertyOf) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_72)))).
% 14.54/5.24 tff(c_1109, plain, (![C_72]: (icext(C_72, uri_rdf_value) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_72)))).
% 14.54/5.24 tff(c_1141, plain, (![C_72]: (icext(C_72, uri_ex_sameCliqueAs) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_72)))).
% 14.54/5.25 tff(c_1111, plain, (![C_72]: (icext(C_72, uri_rdf_first) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_72)))).
% 14.54/5.25 tff(c_1345, plain, (![C_76]: (icext(C_76, uri_rdf_nil) | ~iext(uri_rdfs_range, uri_rdf_rest, C_76)))).
% 14.54/5.25 tff(c_1393, plain, (![C_76]: (icext(C_76, uri_rdfs_Datatype) | ~iext(uri_rdfs_range, uri_rdf_type, C_76)))).
% 14.54/5.25 tff(c_1360, plain, (![C_76]: (icext(C_76, uri_ex_sameCliqueAs) | ~iext(uri_rdfs_range, uri_rdf_first, C_76)))).
% 14.54/5.25 tff(c_1116, plain, (![C_72]: (icext(C_72, uri_rdfs_range) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_72)))).
% 14.54/5.25 tff(c_1086, plain, (![C_72]: (icext(C_72, '#skF_5') | ~iext(uri_rdfs_domain, uri_rdf_first, C_72)))).
% 14.54/5.25 tff(c_1083, plain, (![C_72]: (icext(C_72, '#skF_1') | ~iext(uri_rdfs_domain, uri_owl_onProperty, C_72)))).
% 14.54/5.25 tff(c_2506, plain, (ip(uri_rdfs_comment))).
% 14.54/5.25 tff(c_2500, plain, (icext(uri_rdf_Property, uri_rdfs_comment))).
% 14.54/5.25 tff(c_1101, plain, (![C_72]: (icext(C_72, uri_rdfs_comment) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_72)))).
% 14.54/5.25 tff(c_1343, plain, (![C_76]: (icext(C_76, uri_ex_sameCliqueAs) | ~iext(uri_rdfs_range, uri_owl_onProperty, C_76)))).
% 14.54/5.25 tff(c_1153, plain, (![C_72]: (icext(C_72, '#skF_1') | ~iext(uri_rdfs_domain, uri_rdf_type, C_72)))).
% 14.54/5.25 tff(c_2480, plain, (icext(uri_rdf_Property, uri_ex_sameCliqueAs))).
% 14.54/5.25 tff(c_1159, plain, (![C_72]: (icext(C_72, uri_ex_sameCliqueAs) | ~iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_72)))).
% 14.54/5.25 tff(c_1407, plain, (![C_76]: (icext(C_76, uri_rdfs_Class) | ~iext(uri_rdfs_range, uri_rdfs_domain, C_76)))).
% 14.54/5.25 tff(c_2469, plain, (~icext(uri_rdfs_Datatype, uri_rdfs_Resource))).
% 14.54/5.25 tff(c_901, plain, (![D_69, X_17]: (icext(D_69, X_17) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Resource, D_69)))).
% 14.54/5.25 tff(c_2437, plain, (icext(uri_rdf_Property, uri_rdfs_domain))).
% 14.54/5.25 tff(c_1152, plain, (![C_72]: (icext(C_72, uri_rdfs_domain) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_72)))).
% 14.54/5.25 tff(c_1143, plain, (![C_72]: (icext(C_72, uri_rdfs_domain) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_72)))).
% 14.54/5.25 tff(c_2432, plain, (ic(uri_owl_Restriction))).
% 14.54/5.25 tff(c_2425, plain, (icext(uri_rdfs_Class, uri_owl_Restriction))).
% 14.54/5.25 tff(c_1413, plain, (![C_76]: (icext(C_76, uri_owl_Restriction) | ~iext(uri_rdfs_range, uri_rdf_type, C_76)))).
% 14.54/5.25 tff(c_1112, plain, (![C_72]: (icext(C_72, uri_rdf_type) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_72)))).
% 14.54/5.25 tff(c_1135, plain, (![C_72]: (icext(C_72, uri_rdf_predicate) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_72)))).
% 14.54/5.25 tff(c_1398, plain, (![C_76]: (icext(C_76, uri_rdf_List) | ~iext(uri_rdfs_range, uri_rdfs_domain, C_76)))).
% 14.54/5.25 tff(c_1157, plain, (![C_72]: (icext(C_72, uri_ex_Clique) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_72)))).
% 14.54/5.25 tff(c_1346, plain, (![C_76]: (icext(C_76, '#skF_2') | ~iext(uri_rdfs_range, uri_rdf_first, C_76)))).
% 14.54/5.25 tff(c_1104, plain, (![C_72]: (icext(C_72, uri_rdf_value) | ~iext(uri_rdfs_domain, uri_rdf_type, C_72)))).
% 14.54/5.25 tff(c_1156, plain, (![C_72]: (icext(C_72, uri_foaf_knows) | ~iext(uri_rdfs_domain, uri_rdf_type, C_72)))).
% 14.54/5.25 tff(c_1342, plain, (![C_76]: (icext(C_76, uri_ex_Clique) | ~iext(uri_rdfs_range, uri_owl_someValuesFrom, C_76)))).
% 14.54/5.25 tff(c_1154, plain, (![C_72]: (icext(C_72, uri_rdf_nil) | ~iext(uri_rdfs_domain, uri_rdf_type, C_72)))).
% 14.54/5.25 tff(c_2371, plain, (ic(uri_rdfs_Statement))).
% 14.54/5.25 tff(c_2364, plain, (icext(uri_rdfs_Class, uri_rdfs_Statement))).
% 14.54/5.25 tff(c_1402, plain, (![C_76]: (icext(C_76, uri_rdfs_Statement) | ~iext(uri_rdfs_range, uri_rdfs_domain, C_76)))).
% 14.54/5.25 tff(c_1122, plain, (![C_72]: (icext(C_72, uri_rdf_first) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_72)))).
% 14.54/5.25 tff(c_1084, plain, (![C_72]: (icext(C_72, uri_rdf__2) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_72)))).
% 14.54/5.25 tff(c_2337, plain, (icext(uri_rdf_List, '#skF_3'))).
% 14.54/5.25 tff(c_2343, plain, (ip(uri_rdfs_label))).
% 14.54/5.25 tff(c_2332, plain, (icext(uri_rdf_Property, uri_rdfs_label))).
% 14.54/5.25 tff(c_1114, plain, (![C_72]: (icext(C_72, '#skF_3') | ~iext(uri_rdfs_domain, uri_rdf_first, C_72)))).
% 14.54/5.25 tff(c_1128, plain, (![C_72]: (icext(C_72, uri_rdfs_label) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_72)))).
% 14.54/5.25 tff(c_1368, plain, (![C_76]: (icext(C_76, uri_rdf_type) | ~iext(uri_rdfs_range, uri_owl_inverseOf, C_76)))).
% 14.54/5.25 tff(c_1133, plain, (![C_72]: (icext(C_72, uri_rdf_XMLLiteral) | ~iext(uri_rdfs_domain, uri_rdf_type, C_72)))).
% 14.54/5.25 tff(c_2312, plain, (icext(uri_rdf_Property, uri_rdfs_isDefinedBy))).
% 14.54/5.25 tff(c_1102, plain, (![C_72]: (icext(C_72, uri_rdfs_isDefinedBy) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_72)))).
% 14.54/5.25 tff(c_1118, plain, (![C_72]: (icext(C_72, uri_rdf_subject) | ~iext(uri_rdfs_domain, uri_rdf_type, C_72)))).
% 14.54/5.25 tff(c_2287, plain, (icext(uri_rdfs_Class, uri_ex_Clique))).
% 14.54/5.25 tff(c_1090, plain, (![C_72]: (icext(C_72, uri_rdf__1) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_72)))).
% 14.54/5.25 tff(c_1401, plain, (![C_76]: (icext(C_76, uri_ex_Clique) | ~iext(uri_rdfs_range, uri_rdfs_range, C_76)))).
% 14.54/5.25 tff(c_2274, plain, (icext(uri_rdf_Property, uri_rdfs_subClassOf))).
% 14.54/5.25 tff(c_1132, plain, (![C_72]: (icext(C_72, uri_rdfs_subClassOf) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_72)))).
% 14.54/5.25 tff(c_1145, plain, (![C_72]: (icext(C_72, uri_rdf__1) | ~iext(uri_rdfs_domain, uri_rdf_type, C_72)))).
% 14.54/5.25 tff(c_1103, plain, (![C_72]: (icext(C_72, uri_rdf_type) | ~iext(uri_rdfs_domain, uri_rdf_type, C_72)))).
% 14.54/5.25 tff(c_1121, plain, (![C_72]: (icext(C_72, uri_rdf__2) | ~iext(uri_rdfs_domain, uri_rdf_type, C_72)))).
% 14.54/5.25 tff(c_1389, plain, (![C_76]: (icext(C_76, '#skF_3') | ~iext(uri_rdfs_range, uri_owl_propertyChainAxiom, C_76)))).
% 14.54/5.25 tff(c_1367, plain, (![C_76]: (icext(C_76, uri_rdfs_Literal) | ~iext(uri_rdfs_range, uri_rdfs_subClassOf, C_76)))).
% 14.54/5.25 tff(c_2236, plain, (icext(uri_rdfs_Class, uri_rdfs_Seq))).
% 14.54/5.25 tff(c_1136, plain, (![C_72]: (icext(C_72, uri_rdfs_Seq) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_72)))).
% 14.54/5.25 tff(c_1149, plain, (![C_72]: (icext(C_72, uri_rdf__2) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_72)))).
% 14.54/5.25 tff(c_1148, plain, (![C_72]: (icext(C_72, uri_rdf_type) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_72)))).
% 14.54/5.25 tff(c_2219, plain, (ic(uri_owl_ObjectProperty))).
% 14.54/5.25 tff(c_2212, plain, (icext(uri_rdfs_Class, uri_owl_ObjectProperty))).
% 14.54/5.25 tff(c_1416, plain, (![C_76]: (icext(C_76, uri_owl_ObjectProperty) | ~iext(uri_rdfs_range, uri_rdf_type, C_76)))).
% 14.54/5.25 tff(c_1372, plain, (![C_76]: (icext(C_76, uri_rdfs_Resource) | ~iext(uri_rdfs_range, uri_rdfs_domain, C_76)))).
% 14.54/5.25 tff(c_2193, plain, (icext(uri_rdf_Property, uri_rdfs_range))).
% 14.54/5.25 tff(c_1119, plain, (![C_72]: (icext(C_72, uri_rdfs_range) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_72)))).
% 14.54/5.25 tff(c_2180, plain, (icext(uri_rdf_Property, uri_rdfs_member))).
% 14.54/5.25 tff(c_1130, plain, (![C_72]: (icext(C_72, uri_rdfs_member) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_72)))).
% 14.54/5.25 tff(c_1415, plain, (![C_76]: (icext(C_76, uri_rdf_Property) | ~iext(uri_rdfs_range, uri_rdfs_range, C_76)))).
% 14.54/5.25 tff(c_2161, plain, (icext(uri_rdf_Property, uri_owl_sameAs))).
% 14.54/5.25 tff(c_1419, plain, (![C_76]: (icext(C_76, uri_owl_sameAs) | ~iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_76)))).
% 14.54/5.25 tff(c_1100, plain, (![C_72]: (icext(C_72, '#skF_4') | ~iext(uri_rdfs_domain, uri_rdf_first, C_72)))).
% 14.54/5.25 tff(c_2136, plain, (icext(uri_rdfs_Class, uri_rdfs_ContainerMembershipProperty))).
% 14.54/5.25 tff(c_1124, plain, (![C_72]: (icext(C_72, uri_rdf_subject) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_72)))).
% 14.54/5.25 tff(c_1120, plain, (![C_72]: (icext(C_72, uri_rdfs_ContainerMembershipProperty) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_72)))).
% 14.54/5.25 tff(c_1085, plain, (![C_72]: (icext(C_72, '#skF_5') | ~iext(uri_rdfs_domain, uri_rdf_rest, C_72)))).
% 14.54/5.25 tff(c_2117, plain, (icext(uri_rdfs_Class, uri_rdfs_Datatype))).
% 14.54/5.25 tff(c_2111, plain, (ip(uri_rdf_predicate))).
% 14.54/5.25 tff(c_1127, plain, (![C_72]: (icext(C_72, uri_rdfs_Datatype) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_72)))).
% 14.54/5.25 tff(c_2105, plain, (icext(uri_rdf_Property, uri_rdf_predicate))).
% 14.54/5.25 tff(c_1146, plain, (![C_72]: (icext(C_72, uri_rdf_predicate) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_72)))).
% 14.54/5.25 tff(c_2092, plain, (icext(uri_rdf_Property, uri_rdfs_seeAlso))).
% 14.54/5.25 tff(c_1117, plain, (![C_72]: (icext(C_72, uri_rdfs_seeAlso) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_72)))).
% 14.54/5.25 tff(c_2079, plain, (icext(uri_rdfs_Class, uri_rdfs_Resource))).
% 14.54/5.25 tff(c_1409, plain, (![C_76]: (icext(C_76, uri_rdfs_Resource) | ~iext(uri_rdfs_range, uri_rdfs_range, C_76)))).
% 14.54/5.25 tff(c_1123, plain, (![C_72]: (icext(C_72, uri_rdf_first) | ~iext(uri_rdfs_domain, uri_rdf_type, C_72)))).
% 14.54/5.25 tff(c_1363, plain, (![C_76]: (icext(C_76, uri_rdf_Property) | ~iext(uri_rdfs_range, uri_rdf_type, C_76)))).
% 14.54/5.25 tff(c_1380, plain, (![C_76]: (icext(C_76, uri_rdf_Property) | ~iext(uri_rdfs_range, uri_rdfs_subClassOf, C_76)))).
% 14.54/5.25 tff(c_1412, plain, (![C_76]: (icext(C_76, uri_rdf_Property) | ~iext(uri_rdfs_range, uri_rdfs_domain, C_76)))).
% 14.54/5.25 tff(c_1108, plain, (![C_72]: (icext(C_72, '#skF_2') | ~iext(uri_rdfs_domain, uri_owl_inverseOf, C_72)))).
% 14.54/5.25 tff(c_1144, plain, (![C_72]: (icext(C_72, uri_rdf__3) | ~iext(uri_rdfs_domain, uri_rdf_type, C_72)))).
% 14.54/5.25 tff(c_2034, plain, (icext(uri_rdf_List, '#skF_4'))).
% 14.54/5.25 tff(c_1138, plain, (![C_72]: (icext(C_72, uri_rdf_rest) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_72)))).
% 14.54/5.25 tff(c_1151, plain, (![C_72]: (icext(C_72, '#skF_4') | ~iext(uri_rdfs_domain, uri_rdf_rest, C_72)))).
% 14.54/5.25 tff(c_2021, plain, (icext(uri_rdfs_Class, uri_rdfs_Literal))).
% 14.54/5.25 tff(c_1388, plain, (![C_76]: (icext(C_76, uri_rdfs_Literal) | ~iext(uri_rdfs_range, uri_rdfs_range, C_76)))).
% 14.54/5.25 tff(c_2008, plain, (icext(uri_rdfs_Class, uri_rdf_XMLLiteral))).
% 14.54/5.25 tff(c_1107, plain, (![C_72]: (icext(C_72, uri_rdf_XMLLiteral) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_72)))).
% 14.54/5.25 tff(c_2000, plain, (icext(uri_rdf_List, '#skF_5'))).
% 14.54/5.25 tff(c_1411, plain, (![C_76]: (icext(C_76, '#skF_5') | ~iext(uri_rdfs_range, uri_rdf_rest, C_76)))).
% 14.54/5.25 tff(c_1987, plain, (icext(uri_rdfs_Class, '#skF_1'))).
% 14.54/5.25 tff(c_1417, plain, (![C_76]: (icext(C_76, '#skF_1') | ~iext(uri_rdfs_range, uri_rdfs_subClassOf, C_76)))).
% 14.54/5.26 tff(c_1082, plain, (![C_72]: (icext(C_72, '#skF_1') | ~iext(uri_rdfs_domain, uri_owl_someValuesFrom, C_72)))).
% 14.54/5.26 tff(c_1150, plain, (![C_72]: (icext(C_72, uri_rdf__3) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_72)))).
% 14.54/5.26 tff(c_1967, plain, (icext(uri_rdfs_Class, uri_rdfs_Class))).
% 14.54/5.26 tff(c_1379, plain, (![C_76]: (icext(C_76, uri_rdfs_Class) | ~iext(uri_rdfs_range, uri_rdfs_range, C_76)))).
% 14.54/5.26 tff(c_1158, plain, (![C_72]: (icext(C_72, uri_rdf_rest) | ~iext(uri_rdfs_domain, uri_rdf_type, C_72)))).
% 14.54/5.26 tff(c_1948, plain, (icext(uri_rdfs_Class, uri_rdfs_Container))).
% 14.54/5.26 tff(c_1396, plain, (![C_76]: (icext(C_76, uri_rdfs_Container) | ~iext(uri_rdfs_range, uri_rdfs_subClassOf, C_76)))).
% 14.54/5.26 tff(c_1943, plain, (ic(uri_rdf_List))).
% 14.54/5.26 tff(c_1936, plain, (icext(uri_rdfs_Class, uri_rdf_List))).
% 14.54/5.26 tff(c_1414, plain, (![C_76]: (icext(C_76, uri_rdf_List) | ~iext(uri_rdfs_range, uri_rdf_type, C_76)))).
% 14.54/5.26 tff(c_1923, plain, (icext(uri_rdf_Property, uri_rdfs_subPropertyOf))).
% 14.54/5.26 tff(c_1105, plain, (![C_72]: (icext(C_72, uri_rdfs_subPropertyOf) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_72)))).
% 14.54/5.26 tff(c_1129, plain, (![C_72]: (icext(C_72, uri_foaf_knows) | ~iext(uri_rdfs_domain, uri_owl_propertyChainAxiom, C_72)))).
% 14.54/5.26 tff(c_1137, plain, (![C_72]: (icext(C_72, uri_rdf_rest) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_72)))).
% 14.54/5.26 tff(c_865, plain, (![D_66]: (ic(D_66) | ~icext(uri_rdfs_Datatype, D_66)))).
% 14.54/5.26 tff(c_829, plain, (![P_6]: (icext(uri_rdf_Property, P_6) | ~ip(P_6)))).
% 14.54/5.26 tff(c_758, plain, (![P_63]: (ip(P_63) | ~icext(uri_rdfs_ContainerMembershipProperty, P_63)))).
% 14.54/5.26 tff(c_1880, plain, (ip(uri_rdfs_member))).
% 14.54/5.26 tff(c_886, plain, (![X_67]: (ip(X_67) | ~icext(uri_rdf_Property, X_67)))).
% 14.54/5.26 tff(c_1828, plain, (ic(uri_rdfs_Resource))).
% 14.54/5.26 tff(c_835, plain, (icext(uri_rdfs_Class, uri_rdf_Property))).
% 14.54/5.26 tff(c_833, plain, (icext(uri_rdf_Property, uri_rdf_type))).
% 14.54/5.26 tff(c_848, plain, (icext(uri_rdf_List, uri_rdf_nil))).
% 14.54/5.26 tff(c_844, plain, (icext(uri_rdf_Property, uri_rdf__2))).
% 14.54/5.26 tff(c_830, plain, (icext(uri_ex_Clique, uri_ex_JoesGang))).
% 14.54/5.26 tff(c_842, plain, (icext(uri_rdfs_Datatype, uri_rdf_XMLLiteral))).
% 14.54/5.26 tff(c_847, plain, (icext(uri_owl_Restriction, '#skF_1'))).
% 14.54/5.26 tff(c_845, plain, (icext(uri_rdf_Property, uri_rdf__3))).
% 14.54/5.26 tff(c_831, plain, (icext(uri_owl_Class, uri_ex_Clique))).
% 14.54/5.26 tff(c_836, plain, (icext(uri_rdf_Property, uri_rdf_subject))).
% 14.54/5.26 tff(c_837, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__2))).
% 14.54/5.26 tff(c_832, plain, (icext(uri_ex_JoesGang, uri_ex_bob))).
% 14.54/5.26 tff(c_838, plain, (icext(uri_rdf_Property, uri_rdf_first))).
% 14.54/5.26 tff(c_846, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__1))).
% 14.54/5.26 tff(c_850, plain, (icext(uri_rdf_Property, uri_rdf_rest))).
% 14.54/5.26 tff(c_843, plain, (icext(uri_ex_JoesGang, uri_ex_alice))).
% 14.54/5.26 tff(c_849, plain, (icext(uri_owl_ObjectProperty, uri_foaf_knows))).
% 14.54/5.26 tff(c_841, plain, (icext(uri_rdf_Property, uri_rdf__1))).
% 14.54/5.26 tff(c_834, plain, (icext(uri_rdf_Property, uri_rdf_value))).
% 14.54/5.26 tff(c_840, plain, (icext(uri_rdf_Property, uri_rdf_object))).
% 14.54/5.26 tff(c_839, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__3))).
% 14.54/5.26 tff(c_674, plain, (ic(uri_rdfs_Literal))).
% 14.54/5.26 tff(c_706, plain, (ic(uri_rdf_Bag))).
% 14.54/5.26 tff(c_597, plain, (ip(uri_owl_propertyChainAxiom))).
% 14.54/5.26 tff(c_294, plain, (ip(uri_rdf_object))).
% 14.54/5.26 tff(c_675, plain, (ic(uri_rdf_Property))).
% 14.54/5.26 tff(c_296, plain, (ip(uri_rdf__2))).
% 14.54/5.26 tff(c_156, plain, (![C_28, E_30, D_29]: (iext(uri_rdfs_subClassOf, C_28, E_30) | ~iext(uri_rdfs_subClassOf, D_29, E_30) | ~iext(uri_rdfs_subClassOf, C_28, D_29)))).
% 14.54/5.26 tff(c_160, plain, (![Q_32, X_35, Y_36, P_31]: (iext(Q_32, X_35, Y_36) | ~iext(P_31, X_35, Y_36) | ~iext(uri_rdfs_subPropertyOf, P_31, Q_32)))).
% 14.54/5.26 tff(c_708, plain, (ic(uri_rdf_XMLLiteral))).
% 14.54/5.26 tff(c_170, plain, (![P_38, R_40, Q_39]: (iext(uri_rdfs_subPropertyOf, P_38, R_40) | ~iext(uri_rdfs_subPropertyOf, Q_39, R_40) | ~iext(uri_rdfs_subPropertyOf, P_38, Q_39)))).
% 14.54/5.26 tff(c_128, plain, (![C_20, Y_22, P_19, X_21]: (icext(C_20, Y_22) | ~iext(P_19, X_21, Y_22) | ~iext(uri_rdfs_range, P_19, C_20)))).
% 14.54/5.26 tff(c_295, plain, (ip(uri_rdf__1))).
% 14.54/5.26 tff(c_108, plain, (![C_13, X_14, P_12, Y_15]: (icext(C_13, X_14) | ~iext(P_12, X_14, Y_15) | ~iext(uri_rdfs_domain, P_12, C_13)))).
% 14.54/5.26 tff(c_540, plain, (ip(uri_owl_onProperty))).
% 14.54/5.26 tff(c_146, plain, (![D_24, X_26, C_23]: (icext(D_24, X_26) | ~icext(C_23, X_26) | ~iext(uri_rdfs_subClassOf, C_23, D_24)))).
% 14.54/5.26 tff(c_54, plain, (![X_7, C_8]: (iext(uri_rdf_type, X_7, C_8) | ~icext(C_8, X_7)))).
% 14.54/5.26 tff(c_102, plain, (![D_11]: (iext(uri_rdfs_subClassOf, D_11, uri_rdfs_Literal) | ~icext(uri_rdfs_Datatype, D_11)))).
% 14.54/5.26 tff(c_539, plain, (ip(uri_owl_someValuesFrom))).
% 14.54/5.26 tff(c_52, plain, (![C_8, X_7]: (icext(C_8, X_7) | ~iext(uri_rdf_type, X_7, C_8)))).
% 14.54/5.26 tff(c_560, plain, (ip(uri_rdf_first))).
% 14.54/5.26 tff(c_70, plain, (![P_10]: (iext(uri_rdfs_subPropertyOf, P_10, uri_rdfs_member) | ~icext(uri_rdfs_ContainerMembershipProperty, P_10)))).
% 14.54/5.26 tff(c_571, plain, (ip(uri_owl_inverseOf))).
% 14.54/5.26 tff(c_168, plain, (![P_37]: (iext(uri_rdfs_subPropertyOf, P_37, P_37) | ~ip(P_37)))).
% 14.54/5.26 tff(c_707, plain, (ic(uri_rdf_Alt))).
% 14.54/5.26 tff(c_676, plain, (ic(uri_rdfs_Class))).
% 14.54/5.26 tff(c_56, plain, (![C_9]: (iext(uri_rdfs_subClassOf, C_9, uri_rdfs_Resource) | ~ic(C_9)))).
% 14.54/5.26 tff(c_709, plain, (ic(uri_rdfs_ContainerMembershipProperty))).
% 14.54/5.26 tff(c_710, plain, (ic(uri_rdfs_Datatype))).
% 14.54/5.26 tff(c_711, plain, (ic(uri_rdfs_Seq))).
% 14.54/5.26 tff(c_712, plain, (ic(uri_ex_Clique))).
% 14.54/5.26 tff(c_297, plain, (ip(uri_rdf__3))).
% 14.54/5.26 tff(c_150, plain, (![C_23, D_24]: (ic(C_23) | ~iext(uri_rdfs_subClassOf, C_23, D_24)))).
% 14.54/5.26 tff(c_677, plain, (ic(uri_rdfs_Container))).
% 14.54/5.26 tff(c_678, plain, (ic('#skF_1'))).
% 14.54/5.26 tff(c_148, plain, (![D_24, C_23]: (ic(D_24) | ~iext(uri_rdfs_subClassOf, C_23, D_24)))).
% 14.54/5.26 tff(c_572, plain, (ip(uri_rdfs_domain))).
% 14.54/5.26 tff(c_624, plain, (ip(uri_rdfs_range))).
% 14.54/5.26 tff(c_298, plain, (ip(uri_rdf_rest))).
% 14.54/5.26 tff(c_154, plain, (![C_27]: (iext(uri_rdfs_subClassOf, C_27, C_27) | ~ic(C_27)))).
% 14.54/5.26 tff(c_634, plain, (ip(uri_rdfs_subClassOf))).
% 14.54/5.26 tff(c_637, plain, (ip(uri_rdfs_subPropertyOf))).
% 14.54/5.26 tff(c_292, plain, (ip(uri_rdf_subject))).
% 14.54/5.26 tff(c_2, plain, (![P_2, S_1, O_3]: (ip(P_2) | ~iext(P_2, S_1, O_3)))).
% 14.54/5.26 tff(c_291, plain, (ip(uri_rdf_value))).
% 14.54/5.26 tff(c_290, plain, (ip(uri_rdf_type))).
% 14.54/5.26 tff(c_26, plain, (![P_6]: (ip(P_6) | ~iext(uri_rdf_type, P_6, uri_rdf_Property)))).
% 14.54/5.26 tff(c_256, plain, (ip(uri_ex_sameCliqueAs))).
% 14.54/5.26 tff(c_255, plain, (ip(uri_rdfs_isDefinedBy))).
% 14.54/5.26 tff(c_28, plain, (![P_6]: (iext(uri_rdf_type, P_6, uri_rdf_Property) | ~ip(P_6)))).
% 14.54/5.26 tff(c_164, plain, (![P_31, Q_32]: (ip(P_31) | ~iext(uri_rdfs_subPropertyOf, P_31, Q_32)))).
% 14.54/5.26 tff(c_247, plain, (ip(uri_owl_sameAs))).
% 14.54/5.26 tff(c_246, plain, (ip(uri_rdfs_seeAlso))).
% 14.54/5.26 tff(c_162, plain, (![Q_32, P_31]: (ip(Q_32) | ~iext(uri_rdfs_subPropertyOf, P_31, Q_32)))).
% 14.54/5.26 tff(c_114, plain, (![X_16]: (ic(X_16) | ~icext(uri_rdfs_Class, X_16)))).
% 14.54/5.26 tff(c_120, plain, (![X_18]: (icext(uri_rdfs_Literal, X_18) | ~lv(X_18)))).
% 14.54/5.26 tff(c_122, plain, (![X_18]: (lv(X_18) | ~icext(uri_rdfs_Literal, X_18)))).
% 14.54/5.26 tff(c_112, plain, (![X_16]: (icext(uri_rdfs_Class, X_16) | ~ic(X_16)))).
% 14.54/5.26 tff(c_206, plain, (iext(uri_owl_someValuesFrom, '#skF_1', uri_ex_Clique))).
% 14.54/5.26 tff(c_208, plain, (iext(uri_owl_onProperty, '#skF_1', uri_ex_sameCliqueAs))).
% 14.54/5.26 tff(c_80, plain, (iext(uri_rdfs_domain, uri_rdf__2, uri_rdfs_Resource))).
% 14.54/5.26 tff(c_190, plain, (iext(uri_rdf_rest, '#skF_5', uri_rdf_nil))).
% 14.54/5.26 tff(c_192, plain, (iext(uri_rdf_first, '#skF_5', '#skF_2'))).
% 14.54/5.26 tff(c_74, plain, (iext(uri_rdfs_domain, uri_rdfs_member, uri_rdfs_Resource))).
% 14.54/5.26 tff(c_178, plain, (iext(uri_rdfs_range, uri_rdf_value, uri_rdfs_Resource))).
% 14.54/5.26 tff(c_42, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso))).
% 14.54/5.26 tff(c_84, plain, (iext(uri_rdfs_range, uri_rdf__1, uri_rdfs_Resource))).
% 14.54/5.26 tff(c_186, plain, (iext(uri_rdf_type, uri_ex_JoesGang, uri_ex_Clique))).
% 14.54/5.26 tff(c_40, plain, (iext(uri_rdfs_range, uri_rdfs_isDefinedBy, uri_rdfs_Resource))).
% 14.54/5.26 tff(c_218, plain, (iext(uri_rdf_type, uri_ex_Clique, uri_owl_Class))).
% 14.54/5.26 tff(c_44, plain, (iext(uri_rdfs_domain, uri_rdfs_label, uri_rdfs_Resource))).
% 14.54/5.26 tff(c_82, plain, (iext(uri_rdfs_domain, uri_rdf__3, uri_rdfs_Resource))).
% 14.54/5.26 tff(c_182, plain, (iext(uri_rdf_type, uri_ex_bob, uri_ex_JoesGang))).
% 14.54/5.26 tff(c_68, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Container))).
% 14.54/5.26 tff(c_66, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Container))).
% 14.54/5.26 tff(c_198, plain, (iext(uri_rdf_rest, '#skF_3', '#skF_4'))).
% 14.54/5.26 tff(c_196, plain, (iext(uri_rdf_first, '#skF_4', uri_ex_sameCliqueAs))).
% 14.54/5.26 tff(c_36, plain, (iext(uri_rdfs_range, uri_rdfs_comment, uri_rdfs_Literal))).
% 14.54/5.26 tff(c_38, plain, (iext(uri_rdfs_domain, uri_rdfs_isDefinedBy, uri_rdfs_Resource))).
% 14.54/5.26 tff(c_32, plain, (iext(uri_rdf_type, uri_rdf_type, uri_rdf_Property))).
% 14.54/5.26 tff(c_22, plain, (iext(uri_rdf_type, uri_rdf_value, uri_rdf_Property))).
% 14.54/5.26 tff(c_158, plain, (iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, uri_rdf_Property))).
% 14.54/5.26 tff(c_124, plain, (iext(uri_rdf_type, uri_rdf_Property, uri_rdfs_Class))).
% 14.54/5.26 tff(c_98, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Literal))).
% 14.54/5.26 tff(c_188, plain, (iext(uri_owl_inverseOf, '#skF_2', uri_rdf_type))).
% 14.54/5.26 tff(c_176, plain, (iext(uri_rdfs_domain, uri_rdf_value, uri_rdfs_Resource))).
% 14.54/5.26 tff(c_48, plain, (iext(uri_rdfs_domain, uri_rdfs_seeAlso, uri_rdfs_Resource))).
% 14.54/5.26 tff(c_60, plain, (iext(uri_rdfs_range, uri_rdf_first, uri_rdfs_Resource))).
% 14.54/5.26 tff(c_172, plain, (iext(uri_rdfs_domain, uri_rdf_type, uri_rdfs_Resource))).
% 14.54/5.26 tff(c_78, plain, (iext(uri_rdfs_domain, uri_rdf__1, uri_rdfs_Resource))).
% 14.54/5.26 tff(c_200, plain, (iext(uri_rdf_first, '#skF_3', uri_rdf_type))).
% 14.54/5.26 tff(c_34, plain, (iext(uri_rdfs_domain, uri_rdfs_comment, uri_rdfs_Resource))).
% 14.54/5.26 tff(c_126, plain, (iext(uri_rdfs_domain, uri_rdfs_range, uri_rdf_Property))).
% 14.54/5.26 tff(c_50, plain, (iext(uri_rdfs_range, uri_rdfs_seeAlso, uri_rdfs_Resource))).
% 14.54/5.26 tff(c_24, plain, (iext(uri_rdf_type, uri_rdf_subject, uri_rdf_Property))).
% 14.54/5.26 tff(c_130, plain, (iext(uri_rdfs_range, uri_rdfs_range, uri_rdfs_Class))).
% 14.54/5.26 tff(c_72, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property))).
% 14.54/5.26 tff(c_92, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdfs_ContainerMembershipProperty))).
% 14.54/5.26 tff(c_58, plain, (iext(uri_rdfs_domain, uri_rdf_first, uri_rdf_List))).
% 14.54/5.26 tff(c_8, plain, (iext(uri_rdf_type, uri_rdf_first, uri_rdf_Property))).
% 14.54/5.26 tff(c_142, plain, (iext(uri_rdfs_range, uri_rdf_subject, uri_rdfs_Resource))).
% 14.54/5.26 tff(c_94, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdfs_ContainerMembershipProperty))).
% 14.54/5.26 tff(c_20, plain, (iext(uri_rdf_type, uri_rdf_object, uri_rdf_Property))).
% 14.54/5.26 tff(c_104, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Class))).
% 14.54/5.26 tff(c_46, plain, (iext(uri_rdfs_range, uri_rdfs_label, uri_rdfs_Literal))).
% 14.54/5.26 tff(c_202, plain, (iext(uri_owl_propertyChainAxiom, uri_foaf_knows, '#skF_3'))).
% 14.54/5.27 tff(c_76, plain, (iext(uri_rdfs_range, uri_rdfs_member, uri_rdfs_Resource))).
% 14.54/5.27 tff(c_14, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdf_Property))).
% 14.54/5.27 tff(c_152, plain, (iext(uri_rdfs_range, uri_rdfs_subClassOf, uri_rdfs_Class))).
% 14.54/5.27 tff(c_100, plain, (iext(uri_rdf_type, uri_rdf_XMLLiteral, uri_rdfs_Datatype))).
% 14.54/5.27 tff(c_184, plain, (iext(uri_rdf_type, uri_ex_alice, uri_ex_JoesGang))).
% 14.54/5.27 tff(c_136, plain, (iext(uri_rdfs_domain, uri_rdf_predicate, uri_rdfs_Statement))).
% 14.54/5.27 tff(c_96, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Container))).
% 14.54/5.27 tff(c_64, plain, (iext(uri_rdfs_range, uri_rdf_rest, uri_rdf_List))).
% 14.54/5.27 tff(c_62, plain, (iext(uri_rdfs_domain, uri_rdf_rest, uri_rdf_List))).
% 14.54/5.27 tff(c_132, plain, (iext(uri_rdfs_domain, uri_rdf_object, uri_rdfs_Statement))).
% 14.54/5.27 tff(c_16, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdf_Property))).
% 14.54/5.27 tff(c_214, plain, (iext(uri_rdfs_range, uri_ex_sameCliqueAs, uri_ex_Clique))).
% 14.54/5.27 tff(c_140, plain, (iext(uri_rdfs_domain, uri_rdf_subject, uri_rdfs_Statement))).
% 14.54/5.27 tff(c_110, plain, (iext(uri_rdfs_range, uri_rdfs_domain, uri_rdfs_Class))).
% 14.54/5.27 tff(c_18, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdf_Property))).
% 14.54/5.27 tff(c_90, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdfs_ContainerMembershipProperty))).
% 14.54/5.27 tff(c_138, plain, (iext(uri_rdfs_range, uri_rdf_predicate, uri_rdfs_Resource))).
% 14.54/5.27 tff(c_144, plain, (iext(uri_rdfs_domain, uri_rdfs_subClassOf, uri_rdfs_Class))).
% 14.54/5.27 tff(c_174, plain, (iext(uri_rdfs_range, uri_rdf_type, uri_rdfs_Class))).
% 14.54/5.27 tff(c_86, plain, (iext(uri_rdfs_range, uri_rdf__2, uri_rdfs_Resource))).
% 14.54/5.27 tff(c_88, plain, (iext(uri_rdfs_range, uri_rdf__3, uri_rdfs_Resource))).
% 14.54/5.27 tff(c_194, plain, (iext(uri_rdf_rest, '#skF_4', '#skF_5'))).
% 14.54/5.27 tff(c_106, plain, (iext(uri_rdfs_domain, uri_rdfs_domain, uri_rdf_Property))).
% 14.54/5.27 tff(c_180, plain, (~iext(uri_foaf_knows, uri_ex_alice, uri_ex_bob))).
% 14.54/5.27 tff(c_210, plain, (iext(uri_rdf_type, '#skF_1', uri_owl_Restriction))).
% 14.54/5.27 tff(c_10, plain, (iext(uri_rdf_type, uri_rdf_nil, uri_rdf_List))).
% 14.54/5.27 tff(c_166, plain, (iext(uri_rdfs_range, uri_rdfs_subPropertyOf, uri_rdf_Property))).
% 14.54/5.27 tff(c_204, plain, (iext(uri_rdf_type, uri_foaf_knows, uri_owl_ObjectProperty))).
% 14.54/5.27 tff(c_212, plain, (iext(uri_rdfs_subClassOf, uri_ex_Clique, '#skF_1'))).
% 14.54/5.27 tff(c_12, plain, (iext(uri_rdf_type, uri_rdf_rest, uri_rdf_Property))).
% 14.54/5.27 tff(c_216, plain, (iext(uri_rdfs_subPropertyOf, uri_ex_sameCliqueAs, uri_owl_sameAs))).
% 14.54/5.27 tff(c_224, plain, (![X_17]: (icext(uri_rdfs_Resource, X_17)))).
% 14.54/5.27 tff(c_4, plain, (![X_4]: (ir(X_4)))).
% 14.54/5.27 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 14.54/5.27
%------------------------------------------------------------------------------